# HG changeset patch # User bulwahn # Date 1310978061 -7200 # Node ID aacbe67793c38f7271fdab6074c39b6c8596310d # Parent 05d5696f177f87b48335a2d81a811ce638b66479 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle diff -r 05d5696f177f -r aacbe67793c3 src/HOL/Mutabelle/mutabelle.ML --- a/src/HOL/Mutabelle/mutabelle.ML Mon Jul 18 10:34:21 2011 +0200 +++ b/src/HOL/Mutabelle/mutabelle.ML Mon Jul 18 10:34:21 2011 +0200 @@ -6,58 +6,55 @@ signature MUTABELLE = sig - val testgen_name : string Unsynchronized.ref - exception WrongPath of string; - exception WrongArg of string; - val freeze : term -> term - val mutate_exc : term -> string list -> int -> term list - val mutate_sign : term -> theory -> (string * string) list -> int -> term list - val mutate_mix : term -> theory -> string list -> + exception WrongPath of string; + exception WrongArg of string; + val freeze : term -> term + val mutate_exc : term -> string list -> int -> term list + 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 -> +(* 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 + val qc_test_file : bool -> term list -> (typ * typ) list -> theory -> int -> int -> string -> unit - val mutqc_file_exc : theory -> string list -> + 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 -> + 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 -> + 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 -> + 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 -> + 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 -> + 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 -> + 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 -> + 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 -> + 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 -> + 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 -> + 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 -> + 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 -> + 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 -> + 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 -> + 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 + val canonize_term: term -> string list -> term +*) + val all_unconcealed_thms_of : theory -> (string * thm) list end; structure Mutabelle : MUTABELLE = struct -val testgen_name = Unsynchronized.ref "random"; - fun all_unconcealed_thms_of thy = let val facts = Global_Theory.facts_of thy @@ -495,44 +492,17 @@ (map_types (inst_type insts) (freeze t)); fun is_executable thy insts th = - ((Quickcheck.test_term - (Proof_Context.init_global thy + let + val ctxt' = Proof_Context.init_global thy |> Config.put Quickcheck.size 1 |> Config.put Quickcheck.iterations 1 - |> Config.put Quickcheck.tester (!testgen_name)) - (true, false) (preprocess thy insts (prop_of th), []); - Output.urgent_message "executable"; true) handle ERROR s => - (Output.urgent_message ("not executable: " ^ s); false)); - -fun qc_recursive usedthy [] insts sz qciter acc = rev acc - | qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter - (Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs)); - ((x, pretty (the_default [] (Quickcheck.counterexample_of (Quickcheck.test_term - ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter - #> Config.put Quickcheck.tester (!testgen_name)) - (Proof_Context.init_global usedthy)) - (true, false) (preprocess usedthy insts x, []))))) :: acc)) - handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc); - - -(*quickcheck-test the mutants created by function mutate with type-instantiation insts, -quickcheck-theory usedthy and qciter quickcheck-iterations *) - -fun qc_test mutated insts usedthy sz qciter = - let - val checked = map (apsnd (map (apsnd (cterm_of usedthy)))) - (qc_recursive usedthy mutated insts sz qciter []); - fun combine (passednum,passed) (cenum,ces) [] = (passednum,passed,cenum,ces) - | combine (passednum,passed) (cenum,ces) ((t, []) :: xs) = - combine (passednum+1,(cterm_of usedthy t)::passed) (cenum,ces) xs - | combine (passednum,passed) (cenum,ces) ((t, x) :: xs) = - combine (passednum,passed) - (cenum+1,(cterm_of usedthy t, x) :: ces) xs - in - combine (0,[]) (0,[]) checked - end; - - + val test = Quickcheck.test_term Exhaustive_Generators.compile_generator_expr ctxt' (true, 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 @@ -767,5 +737,6 @@ 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 diff -r 05d5696f177f -r aacbe67793c3 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Jul 18 10:34:21 2011 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Jul 18 10:34:21 2011 +0200 @@ -122,7 +122,7 @@ TimeLimit.timeLimit (seconds (!Try.auto_time_limit)) (fn _ => let - val [result] = Quickcheck.test_goal_terms (change_options (Proof_Context.init_global thy)) + val SOME [result] = Quickcheck.test_goal_terms (change_options (Proof_Context.init_global thy)) (false, false) [] [(t, [])] in case Quickcheck.counterexample_of result of diff -r 05d5696f177f -r aacbe67793c3 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Mon Jul 18 10:34:21 2011 +0200 +++ b/src/Tools/quickcheck.ML Mon Jul 18 10:34:21 2011 +0200 @@ -63,7 +63,8 @@ Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list (* testing terms and proof states *) val test_term: compile_generator -> Proof.context -> bool * bool -> term * term list -> result - (*val test_goal_terms : tester*) + val test_goal_terms : + Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list option val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option (* testing a batch of terms *) val test_terms: