# HG changeset patch # User bulwahn # Date 1327504061 -3600 # Node ID f62f5f1fda3b9b4cd99d813d2c044362f8c70e25 # Parent f5598b604a54ca64465a667755da7de090e0f3d6 removing dead code from Mutabelle; tuned diff -r f5598b604a54 -r f62f5f1fda3b src/HOL/Mutabelle/mutabelle.ML --- 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