--- a/src/Tools/Code/code_ml.ML Thu Apr 19 08:45:13 2012 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Apr 19 10:16:51 2012 +0200
@@ -42,12 +42,6 @@
fun stmt_name_of_binding (ML_Function (name, _)) = name
| stmt_name_of_binding (ML_Instance (name, _)) = name;
-fun stmt_names_of (ML_Exc (name, _)) = [name]
- | stmt_names_of (ML_Val binding) = [stmt_name_of_binding binding]
- | stmt_names_of (ML_Funs (bindings, _)) = map stmt_name_of_binding bindings
- | stmt_names_of (ML_Datas ds) = map fst ds
- | stmt_names_of (ML_Class (name, _)) = [name];
-
fun print_product _ [] = NONE
| print_product print [x] = SOME (print x)
| print_product print xs = (SOME o enum " *" "" "") (map print xs);
@@ -59,7 +53,7 @@
(** SML serializer **)
-fun print_sml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =
+fun print_sml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
let
fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
| print_tyco_expr fxy (tyco, [ty]) =
@@ -363,7 +357,7 @@
(** OCaml serializer **)
-fun print_ocaml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =
+fun print_ocaml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
let
fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
| print_tyco_expr fxy (tyco, [ty]) =
@@ -372,7 +366,7 @@
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
of NONE => print_tyco_expr fxy (tyco, tys)
- | SOME (i, print) => print print_typ fxy tys)
+ | SOME (_, print) => print print_typ fxy tys)
| print_typ fxy (ITyVar v) = str ("'" ^ v);
fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
@@ -435,7 +429,7 @@
and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
- fun print_let ((pat, ty), t) vars =
+ fun print_let ((pat, _), t) vars =
vars
|> print_bind is_pseudo_fun some_thm NOBR pat
|>> (fn p => concat
@@ -764,7 +758,7 @@
fun modify_class stmts = single (SOME
(ML_Class (the_single (map_filter
(fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))))
- fun modify_stmts ([stmt as (name, stmt' as Code_Thingol.Fun _)]) =
+ fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
| modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)
@@ -790,7 +784,7 @@
cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
end;
-fun serialize_ml target print_ml_module print_ml_stmt with_signatures
+fun serialize_ml print_ml_module print_ml_stmt with_signatures
{ labelled_name, reserved_syms, includes, module_alias,
class_syntax, tyco_syntax, const_syntax } program =
let
@@ -801,12 +795,12 @@
(* print statements *)
fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
- labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
+ tyco_syntax const_syntax (make_vars reserved_syms)
(Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt
|> apfst SOME;
(* print modules *)
- fun print_module prefix_fragments base _ xs =
+ fun print_module _ base _ xs =
let
val (raw_decls, body) = split_list xs;
val decls = if with_signatures then SOME (maps these raw_decls) else NONE
@@ -825,13 +819,11 @@
val serializer_sml : Code_Target.serializer =
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
- >> (fn with_signatures => serialize_ml target_SML
- print_sml_module print_sml_stmt with_signatures));
+ >> (fn with_signatures => serialize_ml print_sml_module print_sml_stmt with_signatures));
val serializer_ocaml : Code_Target.serializer =
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
- >> (fn with_signatures => serialize_ml target_OCaml
- print_ocaml_module print_ocaml_stmt with_signatures));
+ >> (fn with_signatures => serialize_ml print_ocaml_module print_ocaml_stmt with_signatures));
(** Isar setup **)
--- a/src/Tools/Code/code_namespace.ML Thu Apr 19 08:45:13 2012 +0200
+++ b/src/Tools/Code/code_namespace.ML Thu Apr 19 10:16:51 2012 +0200
@@ -78,8 +78,8 @@
end;
fun add_dependency name name' =
let
- val (module_name, base) = dest_name name;
- val (module_name', base') = dest_name name';
+ val (module_name, _) = dest_name name;
+ val (module_name', _) = dest_name name';
in if module_name = module_name'
then (Graph.map_node module_name o apfst) (Graph.add_edge (name, name'))
else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) name'))
@@ -177,8 +177,8 @@
end;
fun add_dependency name name' =
let
- val (name_fragments, base) = dest_name name;
- val (name_fragments', base') = dest_name name';
+ val (name_fragments, _) = dest_name name;
+ val (name_fragments', _) = dest_name name';
val (name_fragments_common, (diff, diff')) =
chop_prefix (op =) (name_fragments, name_fragments');
val is_module = not (null diff andalso null diff');
--- a/src/Tools/Code/code_printer.ML Thu Apr 19 08:45:13 2012 +0200
+++ b/src/Tools/Code/code_printer.ML Thu Apr 19 10:16:51 2012 +0200
@@ -146,7 +146,7 @@
|> pair false;
fun filter (XML.Elem (name_attrs, xs)) =
fold (if is_selected name_attrs then add_content_with_space else filter) xs
- | filter (XML.Text s) = I;
+ | filter (XML.Text _) = I;
in snd (fold filter tree (true, Buffer.empty)) end;
fun format presentation_names width =
--- a/src/Tools/Code/code_simp.ML Thu Apr 19 08:45:13 2012 +0200
+++ b/src/Tools/Code/code_simp.ML Thu Apr 19 10:16:51 2012 +0200
@@ -53,7 +53,7 @@
(* evaluation with dynamic code context *)
fun dynamic_conv thy = Code_Thingol.dynamic_conv thy
- (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program);
+ (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE;
--- a/src/Tools/Code/code_target.ML Thu Apr 19 08:45:13 2012 +0200
+++ b/src/Tools/Code/code_target.ML Thu Apr 19 10:16:51 2012 +0200
@@ -270,7 +270,7 @@
fun activate_target thy target =
let
- val ((targets, abortable), default_width) = Targets.get thy;
+ val ((_, abortable), default_width) = Targets.get thy;
val (modify, data) = collapse_hierarchy thy target;
in (default_width, abortable, data, modify) end;
@@ -630,7 +630,7 @@
local
-fun zip_list (x::xs) f g =
+fun zip_list (x :: xs) f g =
f
:|-- (fn y =>
fold_map (fn x => g |-- f >> pair x) xs
--- a/src/Tools/Code/code_thingol.ML Thu Apr 19 08:45:13 2012 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Apr 19 10:16:51 2012 +0200
@@ -436,8 +436,7 @@
type program = stmt Graph.T;
fun empty_funs program =
- Graph.fold (fn (name, (Fun (c, ((_, []), _)), _)) => cons c
- | _ => I) program [];
+ Graph.fold (fn (_, (Fun (c, ((_, []), _)), _)) => cons c | _ => I) program [];
fun map_terms_bottom_up f (t as IConst _) = f t
| map_terms_bottom_up f (t as IVar _) = f t
@@ -533,21 +532,24 @@
val (name, naming') = case lookup naming thing
of SOME name => (name, naming)
| NONE => declare thing naming;
- in case try (Graph.get_node program) name
- of SOME stmt => program
- |> add_dep name
- |> pair naming'
- |> pair dep
- |> pair name
- | NONE => program
- |> Graph.default_node (name, NoStmt)
- |> add_dep name
- |> pair naming'
- |> curry generate (SOME name)
- ||> snd
- |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
- |> pair dep
- |> pair name
+ in
+ if can (Graph.get_node program) name
+ then
+ program
+ |> add_dep name
+ |> pair naming'
+ |> pair dep
+ |> pair name
+ else
+ program
+ |> Graph.default_node (name, NoStmt)
+ |> add_dep name
+ |> pair naming'
+ |> curry generate (SOME name)
+ ||> snd
+ |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
+ |> pair dep
+ |> pair name
end;
exception PERMISSIVE of unit;
@@ -588,7 +590,7 @@
fun tag_term (proj_sort, _) eqngr =
let
val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr;
- fun tag (Const (c', T')) (Const (c, T)) =
+ fun tag (Const (_, T')) (Const (c, T)) =
Const (c,
mk_tagged_type (not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c, T))
| tag (t1 $ u1) (t $ u) = tag t1 t $ tag u1 u
@@ -965,7 +967,7 @@
fun lift_evaluation thy evaluation' algebra eqngr naming program vs t =
let
- val (((_, program'), (((vs', ty'), t'), deps)), _) =
+ val (((_, _), (((vs', ty'), t'), deps)), _) =
ensure_value thy algebra eqngr t (NONE, (naming, program));
in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
@@ -982,7 +984,7 @@
let
fun generate_consts thy algebra eqngr =
fold_map (ensure_const thy algebra eqngr false);
- val (consts', (naming, program)) =
+ val (_, (_, program)) =
invoke_generation true thy (algebra, eqngr) generate_consts consts;
in evaluator' program end;
--- a/src/Tools/misc_legacy.ML Thu Apr 19 08:45:13 2012 +0200
+++ b/src/Tools/misc_legacy.ML Thu Apr 19 10:16:51 2012 +0200
@@ -260,7 +260,7 @@
val thy = Thm.theory_of_thm fth
in
case Thm.fold_terms Term.add_vars fth [] of
- [] => (fth, fn i => fn x => x) (*No vars: nothing to do!*)
+ [] => (fth, fn _ => fn x => x) (*No vars: nothing to do!*)
| vars =>
let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
val alist = map newName vars
--- a/src/Tools/quickcheck.ML Thu Apr 19 08:45:13 2012 +0200
+++ b/src/Tools/quickcheck.ML Thu Apr 19 10:16:51 2012 +0200
@@ -137,14 +137,6 @@
| set_response _ _ NONE result = result
-fun set_counterexample counterexample (Result r) =
- Result {counterexample = counterexample, evaluation_terms = #evaluation_terms r,
- timings = #timings r, reports = #reports r}
-
-fun set_evaluation_terms evaluation_terms (Result r) =
- Result {counterexample = #counterexample r, evaluation_terms = evaluation_terms,
- timings = #timings r, reports = #reports r}
-
fun cons_timing timing (Result r) =
Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
timings = cons timing (#timings r), reports = #reports r}
@@ -288,8 +280,6 @@
val mk_batch_validator =
gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt))
-fun lookup_tester ctxt = AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt)
-
(* testing propositions *)
type compile_generator =
@@ -413,27 +403,11 @@
@ [pretty_stat "positive conclusion tests" positive_concl_tests])
end
-fun pretty_reports ctxt (SOME reports) =
- Pretty.chunks (Pretty.fbrk :: Pretty.str "Quickcheck report:" ::
- maps (fn (size, report) =>
- Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_report report @ [Pretty.brk 1])
- (rev reports))
- | pretty_reports ctxt NONE = Pretty.str ""
-
fun pretty_timings timings =
Pretty.chunks (Pretty.fbrk :: Pretty.str "timings:" ::
maps (fn (label, time) =>
Pretty.str (label ^ ": " ^ string_of_int time ^ " ms") :: Pretty.brk 1 :: []) (rev timings))
-fun pretty_counterex_and_reports ctxt auto [] =
- Pretty.chunks [Pretty.strs (tool_name auto ::
- space_explode " " "is used in a locale where no interpretation is provided."),
- Pretty.strs (space_explode " " "Please provide an executable interpretation for the locale.")]
- | pretty_counterex_and_reports ctxt auto (result :: _) =
- Pretty.chunks (pretty_counterex ctxt auto (response_of result) ::
- (* map (pretty_reports ctxt) (reports_of result) :: *)
- (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
-
(* Isar commands *)
fun read_nat s = case (Library.read_int o Symbol.explode) s