# HG changeset patch
# User haftmann
# Date 1334823411 -7200
# Node ID b32aae03e3d6eedd660b6ac3037f8c3970b40169
# Parent  b90cd7016d4f331264535a94d7bf88065c837d0c
dropped dead code;
tuned

diff -r b90cd7016d4f -r b32aae03e3d6 src/Tools/Code/code_ml.ML
--- 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 **)
diff -r b90cd7016d4f -r b32aae03e3d6 src/Tools/Code/code_namespace.ML
--- 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');
diff -r b90cd7016d4f -r b32aae03e3d6 src/Tools/Code/code_printer.ML
--- 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 =
diff -r b90cd7016d4f -r b32aae03e3d6 src/Tools/Code/code_simp.ML
--- 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;
 
diff -r b90cd7016d4f -r b32aae03e3d6 src/Tools/Code/code_target.ML
--- 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
diff -r b90cd7016d4f -r b32aae03e3d6 src/Tools/Code/code_thingol.ML
--- 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;
 
diff -r b90cd7016d4f -r b32aae03e3d6 src/Tools/misc_legacy.ML
--- 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
diff -r b90cd7016d4f -r b32aae03e3d6 src/Tools/quickcheck.ML
--- 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