--- 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
--- 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) =