# HG changeset patch
# User haftmann
# Date 1360759132 -3600
# Node ID 5e6398b4803037cf10801a6b306e53fdb2ce0942
# Parent  c007c6bf4a35ed39b2e878cc570f839a468459e2
formal cleanup of sources

diff -r c007c6bf4a35 -r 5e6398b48030 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Wed Feb 13 13:38:52 2013 +0100
@@ -30,9 +30,6 @@
       facts []
   end;
 
-fun thms_of thy = filter (fn (_, th) =>
-   Context.theory_name (theory_of_thm th) = Context.theory_name thy) (all_unconcealed_thms_of thy);
-
 fun consts_of thy =
  let
    val (namespace, const_table) = #constants (Consts.dest (Sign.consts_of thy))
@@ -128,8 +125,8 @@
  let 
    val revlC = rev longContext
    val revsC = rev shortContext
-   fun is_prefix [] longList = true
-     | is_prefix shList [] = false
+   fun is_prefix [] _ = true
+     | is_prefix _ [] = false
      | is_prefix (x::xs) (y::ys) = if (x=y) then is_prefix xs ys else false
  in 
    is_prefix revsC revlC
@@ -227,8 +224,8 @@
 (*evaluates if the two terms with paths passed as arguments can be exchanged, i.e. evaluates if one of the terms is a subterm of the other one*)  
 
 fun areReplacable [] [] = false
- | areReplacable fstPath [] = false
- | areReplacable [] sndPath = false
+ | areReplacable _ [] = false
+ | areReplacable [] _ = false
  | areReplacable (x::xs) (y::ys) = if (x=y) then areReplacable xs ys else true; 
 
 
@@ -237,21 +234,21 @@
 (*substitutes the term at the position of the first list in fstTerm by sndTerm. 
 The lists represent paths as generated by createSubTermList*)
 
-fun substitute [] fstTerm sndTerm = sndTerm
+fun substitute [] _ sndTerm = sndTerm
  | substitute (_::xs) (Abs(s,T,subTerm)) sndTerm = Abs(s,T,(substitute xs subTerm sndTerm))
  | substitute (0::xs) (t $ u) sndTerm = substitute xs t sndTerm $ u 
  | substitute (1::xs) (t $ u) sndTerm = t $ substitute xs u sndTerm
- | substitute (_::xs) _ sndTerm = 
+ | substitute (_::_) _ sndTerm = 
    raise WrongPath ("The Term could not be found at the specified position"); 
 
 
 (*get the subterm with the specified path in myTerm*)
 
 fun getSubTerm myTerm [] = myTerm
- | getSubTerm (Abs(s,T,subTerm)) (0::xs) = getSubTerm subTerm xs
- | getSubTerm (t $ u) (0::xs) = getSubTerm t xs
- | getSubTerm (t $ u) (1::xs) = getSubTerm u xs
- | getSubTerm _ (_::xs) = 
+ | getSubTerm (Abs(_,_,subTerm)) (0::xs) = getSubTerm subTerm xs
+ | getSubTerm (t $ _) (0::xs) = getSubTerm t xs
+ | getSubTerm (_ $ u) (1::xs) = getSubTerm u xs
+ | getSubTerm _ (_::_) = 
    raise WrongPath ("The subterm could not be found at the specified position");
 
 
@@ -423,23 +420,4 @@
      Free (if i = 0 then a else a ^ "_" ^ string_of_int i, T)
  | freeze t = t;
 
-fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
- | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T);
-
-fun preprocess thy insts t = Object_Logic.atomize_term thy
- (map_types (inst_type insts) (freeze t));
-
-fun is_executable thy insts th =
-  let
-    val ctxt' = Proof_Context.init_global thy
-      |> Config.put Quickcheck.size 1
-      |> Config.put Quickcheck.iterations 1
-    val test = Quickcheck_Common.test_term
-      ("exhaustive", ((fn _ => raise (Fail "")), Exhaustive_Generators.compile_generator_expr)) ctxt' false
-  in  
-    case try test (preprocess thy insts (prop_of th), []) of
-      SOME _ => (Output.urgent_message "executable"; true)
-    | NONE => (Output.urgent_message ("not executable"); false)
-  end;                                               
-
 end
diff -r c007c6bf4a35 -r 5e6398b48030 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Feb 13 13:38:52 2013 +0100
@@ -105,7 +105,7 @@
 
 (** quickcheck **)
 
-fun invoke_quickcheck change_options quickcheck_generator thy t =
+fun invoke_quickcheck change_options thy t =
   TimeLimit.timeLimit (seconds 30.0)
       (fn _ =>
           let
@@ -123,7 +123,7 @@
          (Timeout, [("timelimit", Real.floor (!Try.auto_time_limit))])
 
 fun quickcheck_mtd change_options quickcheck_generator =
-  ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
+  ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options)
 
 (** solve direct **)
  
@@ -335,8 +335,6 @@
       (* andalso is_executable_thm thy th *))
     (map snd (filter_out is_forbidden_theorem (Mutabelle.all_unconcealed_thms_of thy)))
 
-fun count x = (length oo filter o equal) x
-
 fun elapsed_time description e =
   let val ({elapsed, ...}, result) = Timing.timing e ()
   in (result, (description, Time.toMilliseconds elapsed)) end
@@ -354,27 +352,14 @@
     val _ = Output.urgent_message ("Invoking " ^ mtd_name)
     val (res, timing) = elapsed_time "total time"
       (fn () => case try (invoke_mtd thy) t of
-          SOME (res, timing) => res
+          SOME (res, _) => res
         | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
             Error))
     val _ = Output.urgent_message (" Done")
   in (res, [timing]) end
 
-(* theory -> term list -> mtd -> subentry *)
-
-fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
-  let
-     val res = map (fst o safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
-  in
-    (mtd_name, count GenuineCex res, count PotentialCex res, count NoCex res,
-     count Donno res, count Timeout res, count Error res)
-  end
-
 (* creating entries *)
 
-fun create_entry thy thm exec mutants mtds =
-  (Thm.get_name_hint thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
-
 fun create_detailed_entry thy thm exec mutants mtds =
   let
     fun create_mutant_subentry mutant = (mutant,
@@ -422,15 +407,6 @@
     create_entry thy thm exec mutants mtds
   end
 
-(* theory -> mtd list -> thm list -> report *)
-val mutate_theorems = map oooo mutate_theorem
-
-fun string_of_mutant_subentry thy thm_name (t, results) =
-  "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
-  space_implode "; "
-    (map (fn (mtd_name, (outcome, timing)) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
-  "\n"
-
 (* string -> string *)
 val unyxml = XML.content_of o YXML.parse_body
 
@@ -457,16 +433,6 @@
    Syntax.string_of_term_global thy t ^ "\n" ^                                    
    cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"
 
-fun theoryfile_string_of_mutant_subentry thy thm_name (i, (t, results)) =
-  "lemma " ^ thm_name ^ "_" ^ string_of_int (i + 1) ^ ":\n" ^
-  "\"" ^ unyxml (Syntax.string_of_term_global thy t) ^
-  "\" \nquickcheck\noops\n"
-
-fun theoryfile_string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
-  "subsubsection {* mutants of " ^ thm_name ^ " *}\n\n" ^
-  cat_lines (map_index
-    (theoryfile_string_of_mutant_subentry thy thm_name) mutant_subentries) ^ "\n"
-
 (* subentry -> string *)
 fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno,
                          timeout, error) =