--- a/src/HOL/Mutabelle/mutabelle.ML Wed Jan 25 15:19:04 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML Wed Jan 25 16:07:41 2012 +0100
@@ -13,42 +13,7 @@
val mutate_sign : term -> theory -> (string * string) list -> int -> term list
val mutate_mix : term -> theory -> string list ->
(string * string) list -> int -> term list
-(* val qc_test : term list -> (typ * typ) list -> theory ->
- int -> int -> int * Thm.cterm list * int * (Thm.cterm * (string * Thm.cterm) list) list
- val qc_test_file : bool -> term list -> (typ * typ) list
- -> theory -> int -> int -> string -> unit
- val mutqc_file_exc : theory -> string list ->
- int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit
- val mutqc_file_sign : theory -> (string * string) list ->
- int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit
- val mutqc_file_mix : theory -> string list -> (string * string) list ->
- int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit
- val mutqc_file_rec_exc : theory -> string list -> int ->
- Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit
- val mutqc_file_rec_sign : theory -> (string * string) list -> int ->
- Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit
- val mutqc_file_rec_mix : theory -> string list -> (string * string) list ->
- int -> Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit
- val mutqc_thy_exc : theory -> theory ->
- string list -> int -> (typ * typ) list -> int -> int -> string -> unit
- val mutqc_thy_sign : theory -> theory -> (string * string) list ->
- int -> (typ * typ) list -> int -> int -> string -> unit
- val mutqc_thy_mix : theory -> theory -> string list -> (string * string) list ->
- int -> (typ * typ) list -> int -> int -> string -> unit
- val mutqc_file_stat_sign : theory -> (string * string) list ->
- int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit
- val mutqc_file_stat_exc : theory -> string list ->
- int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit
- val mutqc_file_stat_mix : theory -> string list -> (string * string) list ->
- int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit
- val mutqc_thystat_exc : (string -> thm -> bool) -> theory -> theory ->
- string list -> int -> (typ * typ) list -> int -> int -> string -> unit
- val mutqc_thystat_sign : (string -> thm -> bool) -> theory -> theory -> (string * string) list ->
- int -> (typ * typ) list -> int -> int -> string -> unit
- val mutqc_thystat_mix : (string -> thm -> bool) -> theory -> theory -> string list ->
- (string * string) list -> int -> (typ * typ) list -> int -> int -> string -> unit
- val canonize_term: term -> string list -> term
-*)
+
val all_unconcealed_thms_of : theory -> (string * thm) list
end;
@@ -163,15 +128,6 @@
end;
-
-
-
-(*tests if the given element ist in the given list*)
-
-fun in_list elem [] = false
- | in_list elem (x::xs) = if (elem = x) then true else in_list elem xs;
-
-
(*Evaluate if the longContext is more special as the shortContext.
If so, a term with shortContext can be substituted in the place of a
term with longContext*)
@@ -338,9 +294,7 @@
let
val Const(name,_) = (getSubTerm origTerm (rev opcomm))
in
- if (in_list name commutatives)
- then true
- else false
+ member (op =) commutatives name
end
else false
end
@@ -469,13 +423,7 @@
fun mutate_mix origTerm tsig commutatives forbidden_funs iter =
mutate 2 origTerm tsig commutatives forbidden_funs iter;
-
-(*helper function in order to prettily print a list of terms*)
-
-fun pretty xs = map (fn (id, t) => (id, (HOLogic.mk_number HOLogic.natT
- (HOLogic.dest_nat t)) handle TERM _ => t)) xs;
-
-
+
(*helper function for the quickcheck invocation. Evaluates the quickcheck_term function on a whole list of terms
and tries to print the exceptions*)
@@ -497,247 +445,11 @@
|> Config.put Quickcheck.size 1
|> Config.put Quickcheck.iterations 1
val test = Quickcheck_Common.test_term
- ("exhaustive", Exhaustive_Generators.compile_generator_expr) ctxt' false
+ ("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;
-(*
-(*create a string of a list of terms*)
-
-fun string_of_ctermlist thy [] acc = acc
- | string_of_ctermlist thy (x::xs) acc =
- string_of_ctermlist thy xs ((Syntax.string_of_term_global thy (term_of x)) ^ "\n" ^ acc);
-
-(*helper function in order to decompose the counter examples generated by quickcheck*)
-
-fun decompose_ce thy [] acc = acc
- | decompose_ce thy ((varname,varce)::xs) acc =
- decompose_ce thy xs ("\t" ^ varname ^ " instanciated to " ^
- (Syntax.string_of_term_global thy (term_of varce)) ^ "\n" ^ acc);
-
-(*helper function in order to decompose a list of counter examples*)
-
-fun decompose_celist thy [] acc = acc
- | decompose_celist thy ((mutTerm,varcelist)::xs) acc = decompose_celist thy xs
- ("mutated term : " ^
- (Syntax.string_of_term_global thy (term_of mutTerm)) ^ "\n" ^
- "counterexample : \n" ^
- (decompose_ce thy (rev varcelist) "") ^ acc);
-
-
-(*quickcheck test the list of mutants mutated by applying the type instantiations
-insts and using the quickcheck-theory usedthy. The results of quickcheck are stored
-in the file with name filename. If app is true, the output will be appended to the file.
-Else it will be overwritten. *)
-
-fun qc_test_file app mutated insts usedthy sz qciter filename =
- let
- val statisticList = qc_test mutated insts usedthy sz qciter
- val passed = (string_of_int (#1 statisticList)) ^
- " terms passed the quickchecktest: \n\n" ^
- (string_of_ctermlist usedthy (rev (#2 statisticList)) "")
- val counterexps = (string_of_int (#3 statisticList)) ^
- " terms produced a counterexample: \n\n" ^
- decompose_celist usedthy (rev (#4 statisticList)) ""
- in
- if (app = false)
- then File.write (Path.explode filename) (passed ^ "\n\n" ^ counterexps)
- else File.append (Path.explode filename) (passed ^ "\n\n" ^ counterexps)
- end;
-
-
-(*mutate sourceThm with the mutate-version given in option and check the resulting mutants.
-The output will be written to the file with name filename*)
-
-fun mutqc_file option usedthy commutatives forbidden_funs iter sourceThm insts sz qciter filename =
- let
- val mutated = mutate option (prop_of sourceThm)
- usedthy commutatives forbidden_funs iter
- in
- qc_test_file false mutated insts usedthy sz qciter filename
- end;
-
-(*exchange version of function mutqc_file*)
-
-fun mutqc_file_exc usedthy commutatives iter sourceThm insts sz qciter filename =
- mutqc_file 0 usedthy commutatives [] iter sourceThm insts sz qciter filename;
-
-
-(*sinature version of function mutqc_file*)
-fun mutqc_file_sign usedthy forbidden_funs iter sourceThm insts sz qciter filename=
- mutqc_file 1 usedthy [] forbidden_funs iter sourceThm insts sz qciter filename;
-
-(*mixed version of function mutqc_file*)
-
-fun mutqc_file_mix usedthy commutatives forbidden_funs iter sourceThm insts sz qciter filename =
- mutqc_file 2 usedthy commutatives forbidden_funs iter sourceThm insts sz qciter filename;
-
-
-
-(*apply function mutqc_file on a list of theorems. The output for each theorem
-will be stored in a seperated file whose filename must be indicated in a list*)
-
-fun mutqc_file_rec option usedthy commutatives forbFuns iter [] insts sz qciter _ = ()
- | mutqc_file_rec option usedthy commutatives forbFuns iter sourceThms insts sz qciter [] =
- raise WrongArg ("Not enough files for the output of qc_test_file_rec!")
- | mutqc_file_rec option usedthy commutatives forbFuns iter (x::xs) insts sz qciter (y::ys) =
- (mutqc_file option usedthy commutatives forbFuns iter x insts sz qciter y ;
- mutqc_file_rec option usedthy commutatives forbFuns iter xs insts sz qciter ys);
-
-
-(*exchange version of function mutqc_file_rec*)
-
-fun mutqc_file_rec_exc usedthy commutatives iter sourceThms insts sz qciter files =
- mutqc_file_rec 0 usedthy commutatives [] iter sourceThms insts sz qciter files;
-
-(*signature version of function mutqc_file_rec*)
-
-fun mutqc_file_rec_sign usedthy forbidden_funs iter sourceThms insts sz qciter files =
- mutqc_file_rec 1 usedthy [] forbidden_funs iter sourceThms insts sz qciter files;
-
-(*mixed version of function mutqc_file_rec*)
-
-fun mutqc_file_rec_mix usedthy commutatives forbidden_funs iter sourceThms insts sz qciter files =
- mutqc_file_rec 2 usedthy commutatives forbidden_funs iter sourceThms insts sz qciter files;
-
-(*create the appropriate number of spaces in order to properly print a table*)
-
-fun create_spaces entry spacenum =
- let
- val diff = spacenum - (size entry)
- in
- if (diff > 0)
- then implode (replicate diff " ")
- else ""
- end;
-
-
-(*create a statistic of the output of a quickcheck test on the passed thmlist*)
-
-fun mutqc_file_stat option usedthy commutatives forbidden_funs iter thmlist insts sz qciter filename =
- let
- fun mutthmrec [] = ()
- | mutthmrec (x::xs) =
- let
- val mutated = mutate option (prop_of x) usedthy
- commutatives forbidden_funs iter
- val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter
- val thmname = "\ntheorem " ^ Thm.get_name_hint x ^ ":"
- val pnumstring = string_of_int passednum
- val cenumstring = string_of_int cenum
- in
- (File.append (Path.explode filename)
- (thmname ^ (create_spaces thmname 50) ^
- pnumstring ^ (create_spaces pnumstring 20) ^
- cenumstring ^ (create_spaces cenumstring 20) ^ "\n");
- mutthmrec xs)
- end;
- in
- (File.write (Path.explode filename)
- ("\n\ntheorem name" ^ (create_spaces "theorem name" 50) ^
- "passed mutants" ^ (create_spaces "passed mutants" 20) ^
- "counter examples\n\n" );
- mutthmrec thmlist)
- end;
-
-(*signature version of function mutqc_file_stat*)
-
-fun mutqc_file_stat_sign usedthy forbidden_funs iter thmlist insts sz qciter filename =
- mutqc_file_stat 1 usedthy [] forbidden_funs iter thmlist insts sz qciter filename;
-
-(*exchange version of function mutqc_file_stat*)
-
-fun mutqc_file_stat_exc usedthy commutatives iter thmlist insts sz qciter filename =
- mutqc_file_stat 0 usedthy commutatives [] iter thmlist insts sz qciter filename;
-
-(*mixed version of function mutqc_file_stat*)
-
-fun mutqc_file_stat_mix usedthy commutatives forbidden_funs iter thmlist insts sz qciter filename =
- mutqc_file_stat 2 usedthy commutatives forbidden_funs iter thmlist insts sz qciter filename;
-
-(*mutate and quickcheck-test all the theorems contained in the passed theory.
-The output will be stored in a single file*)
-
-fun mutqc_thy option mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
- let
- val thmlist = filter (is_executable mutthy insts o snd) (thms_of mutthy);
- fun mutthmrec [] = ()
- | mutthmrec ((name,thm)::xs) =
- let
- val mutated = mutate option (prop_of thm)
- usedthy commutatives forbidden_funs iter
- in
- (File.append (Path.explode filename)
- ("--------------------------\n\nQuickchecktest of theorem " ^ name ^ ":\n\n");
- qc_test_file true mutated insts usedthy sz qciter filename;
- mutthmrec xs)
- end;
- in
- mutthmrec thmlist
- end;
-
-(*exchange version of function mutqc_thy*)
-
-fun mutqc_thy_exc mutthy usedthy commutatives iter insts sz qciter filename =
- mutqc_thy 0 mutthy usedthy commutatives [] iter insts sz qciter filename;
-
-(*signature version of function mutqc_thy*)
-
-fun mutqc_thy_sign mutthy usedthy forbidden_funs iter insts sz qciter filename =
- mutqc_thy 1 mutthy usedthy [] forbidden_funs iter insts sz qciter filename;
-
-(*mixed version of function mutqc_thy*)
-
-fun mutqc_thy_mix mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
- mutqc_thy 2 mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename;
-
-(*create a statistic representation of the call of function mutqc_thy*)
-
-fun mutqc_thystat option p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
- let
- val thmlist = filter
- (fn (s, th) => not (p s th) andalso (Output.urgent_message s; is_executable mutthy insts th)) (thms_of mutthy)
- fun mutthmrec [] = ()
- | mutthmrec ((name,thm)::xs) =
- let
- val _ = Output.urgent_message ("mutthmrec: " ^ name);
- val mutated = mutate option (prop_of thm) usedthy
- commutatives forbidden_funs iter
- val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter
- val thmname = "\ntheorem " ^ name ^ ":"
- val pnumstring = string_of_int passednum
- val cenumstring = string_of_int cenum
- in
- (File.append (Path.explode filename)
- (thmname ^ (create_spaces thmname 50) ^
- pnumstring ^ (create_spaces pnumstring 20) ^
- cenumstring ^ (create_spaces cenumstring 20) ^ "\n");
- mutthmrec xs)
- end;
- in
- (File.write (Path.explode filename) ("Result of the quickcheck-test of theory " ^
- ":\n\ntheorem name" ^ (create_spaces "theorem name" 50) ^
- "passed mutants" ^ (create_spaces "passed mutants" 20) ^
- "counter examples\n\n" );
- mutthmrec thmlist)
- end;
-
-(*exchange version of function mutqc_thystat*)
-
-fun mutqc_thystat_exc p mutthy usedthy commutatives iter insts sz qciter filename =
- mutqc_thystat 0 p mutthy usedthy commutatives [] iter insts sz qciter filename;
-
-(*signature version of function mutqc_thystat*)
-
-fun mutqc_thystat_sign p mutthy usedthy forbidden_funs iter insts sz qciter filename =
- mutqc_thystat 1 p mutthy usedthy [] forbidden_funs iter insts sz qciter filename;
-
-(*mixed version of function mutqc_thystat*)
-
-fun mutqc_thystat_mix p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
- mutqc_thystat 2 p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename;
-*)
+ end;
end