4 Mutation of theorems. |
4 Mutation of theorems. |
5 *) |
5 *) |
6 |
6 |
7 signature MUTABELLE = |
7 signature MUTABELLE = |
8 sig |
8 sig |
9 val testgen_name : string Unsynchronized.ref |
9 exception WrongPath of string; |
10 exception WrongPath of string; |
10 exception WrongArg of string; |
11 exception WrongArg of string; |
11 val freeze : term -> term |
12 val freeze : term -> term |
12 val mutate_exc : term -> string list -> int -> term list |
13 val mutate_exc : term -> string list -> int -> term list |
13 val mutate_sign : term -> theory -> (string * string) list -> int -> term list |
14 val mutate_sign : term -> theory -> (string * string) list -> int -> term list |
14 val mutate_mix : term -> theory -> string list -> |
15 val mutate_mix : term -> theory -> string list -> |
|
16 (string * string) list -> int -> term list |
15 (string * string) list -> int -> term list |
17 val qc_test : term list -> (typ * typ) list -> theory -> |
16 (* val qc_test : term list -> (typ * typ) list -> theory -> |
18 int -> int -> int * Thm.cterm list * int * (Thm.cterm * (string * Thm.cterm) list) list |
17 int -> int -> int * Thm.cterm list * int * (Thm.cterm * (string * Thm.cterm) list) list |
19 val qc_test_file : bool -> term list -> (typ * typ) list |
18 val qc_test_file : bool -> term list -> (typ * typ) list |
20 -> theory -> int -> int -> string -> unit |
19 -> theory -> int -> int -> string -> unit |
21 val mutqc_file_exc : theory -> string list -> |
20 val mutqc_file_exc : theory -> string list -> |
22 int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit |
21 int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit |
23 val mutqc_file_sign : theory -> (string * string) list -> |
22 val mutqc_file_sign : theory -> (string * string) list -> |
24 int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit |
23 int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit |
25 val mutqc_file_mix : theory -> string list -> (string * string) list -> |
24 val mutqc_file_mix : theory -> string list -> (string * string) list -> |
26 int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit |
25 int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit |
27 val mutqc_file_rec_exc : theory -> string list -> int -> |
26 val mutqc_file_rec_exc : theory -> string list -> int -> |
28 Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit |
27 Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit |
29 val mutqc_file_rec_sign : theory -> (string * string) list -> int -> |
28 val mutqc_file_rec_sign : theory -> (string * string) list -> int -> |
30 Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit |
29 Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit |
31 val mutqc_file_rec_mix : theory -> string list -> (string * string) list -> |
30 val mutqc_file_rec_mix : theory -> string list -> (string * string) list -> |
32 int -> Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit |
31 int -> Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit |
33 val mutqc_thy_exc : theory -> theory -> |
32 val mutqc_thy_exc : theory -> theory -> |
34 string list -> int -> (typ * typ) list -> int -> int -> string -> unit |
33 string list -> int -> (typ * typ) list -> int -> int -> string -> unit |
35 val mutqc_thy_sign : theory -> theory -> (string * string) list -> |
34 val mutqc_thy_sign : theory -> theory -> (string * string) list -> |
36 int -> (typ * typ) list -> int -> int -> string -> unit |
35 int -> (typ * typ) list -> int -> int -> string -> unit |
37 val mutqc_thy_mix : theory -> theory -> string list -> (string * string) list -> |
36 val mutqc_thy_mix : theory -> theory -> string list -> (string * string) list -> |
38 int -> (typ * typ) list -> int -> int -> string -> unit |
37 int -> (typ * typ) list -> int -> int -> string -> unit |
39 val mutqc_file_stat_sign : theory -> (string * string) list -> |
38 val mutqc_file_stat_sign : theory -> (string * string) list -> |
40 int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit |
39 int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit |
41 val mutqc_file_stat_exc : theory -> string list -> |
40 val mutqc_file_stat_exc : theory -> string list -> |
42 int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit |
41 int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit |
43 val mutqc_file_stat_mix : theory -> string list -> (string * string) list -> |
42 val mutqc_file_stat_mix : theory -> string list -> (string * string) list -> |
44 int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit |
43 int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit |
45 val mutqc_thystat_exc : (string -> thm -> bool) -> theory -> theory -> |
44 val mutqc_thystat_exc : (string -> thm -> bool) -> theory -> theory -> |
46 string list -> int -> (typ * typ) list -> int -> int -> string -> unit |
45 string list -> int -> (typ * typ) list -> int -> int -> string -> unit |
47 val mutqc_thystat_sign : (string -> thm -> bool) -> theory -> theory -> (string * string) list -> |
46 val mutqc_thystat_sign : (string -> thm -> bool) -> theory -> theory -> (string * string) list -> |
48 int -> (typ * typ) list -> int -> int -> string -> unit |
47 int -> (typ * typ) list -> int -> int -> string -> unit |
49 val mutqc_thystat_mix : (string -> thm -> bool) -> theory -> theory -> string list -> |
48 val mutqc_thystat_mix : (string -> thm -> bool) -> theory -> theory -> string list -> |
50 (string * string) list -> int -> (typ * typ) list -> int -> int -> string -> unit |
49 (string * string) list -> int -> (typ * typ) list -> int -> int -> string -> unit |
51 val canonize_term: term -> string list -> term |
50 val canonize_term: term -> string list -> term |
52 |
51 *) |
53 val all_unconcealed_thms_of : theory -> (string * thm) list |
52 val all_unconcealed_thms_of : theory -> (string * thm) list |
54 end; |
53 end; |
55 |
54 |
56 structure Mutabelle : MUTABELLE = |
55 structure Mutabelle : MUTABELLE = |
57 struct |
56 struct |
58 |
|
59 val testgen_name = Unsynchronized.ref "random"; |
|
60 |
57 |
61 fun all_unconcealed_thms_of thy = |
58 fun all_unconcealed_thms_of thy = |
62 let |
59 let |
63 val facts = Global_Theory.facts_of thy |
60 val facts = Global_Theory.facts_of thy |
64 in |
61 in |
493 |
490 |
494 fun preprocess thy insts t = Object_Logic.atomize_term thy |
491 fun preprocess thy insts t = Object_Logic.atomize_term thy |
495 (map_types (inst_type insts) (freeze t)); |
492 (map_types (inst_type insts) (freeze t)); |
496 |
493 |
497 fun is_executable thy insts th = |
494 fun is_executable thy insts th = |
498 ((Quickcheck.test_term |
495 let |
499 (Proof_Context.init_global thy |
496 val ctxt' = Proof_Context.init_global thy |
500 |> Config.put Quickcheck.size 1 |
497 |> Config.put Quickcheck.size 1 |
501 |> Config.put Quickcheck.iterations 1 |
498 |> Config.put Quickcheck.iterations 1 |
502 |> Config.put Quickcheck.tester (!testgen_name)) |
499 val test = Quickcheck.test_term Exhaustive_Generators.compile_generator_expr ctxt' (true, false) |
503 (true, false) (preprocess thy insts (prop_of th), []); |
500 in |
504 Output.urgent_message "executable"; true) handle ERROR s => |
501 case try test (preprocess thy insts (prop_of th), []) of |
505 (Output.urgent_message ("not executable: " ^ s); false)); |
502 SOME _ => (Output.urgent_message "executable"; true) |
506 |
503 | NONE => (Output.urgent_message ("not executable"); false) |
507 fun qc_recursive usedthy [] insts sz qciter acc = rev acc |
504 end; |
508 | qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter |
505 (* |
509 (Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs)); |
|
510 ((x, pretty (the_default [] (Quickcheck.counterexample_of (Quickcheck.test_term |
|
511 ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter |
|
512 #> Config.put Quickcheck.tester (!testgen_name)) |
|
513 (Proof_Context.init_global usedthy)) |
|
514 (true, false) (preprocess usedthy insts x, []))))) :: acc)) |
|
515 handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc); |
|
516 |
|
517 |
|
518 (*quickcheck-test the mutants created by function mutate with type-instantiation insts, |
|
519 quickcheck-theory usedthy and qciter quickcheck-iterations *) |
|
520 |
|
521 fun qc_test mutated insts usedthy sz qciter = |
|
522 let |
|
523 val checked = map (apsnd (map (apsnd (cterm_of usedthy)))) |
|
524 (qc_recursive usedthy mutated insts sz qciter []); |
|
525 fun combine (passednum,passed) (cenum,ces) [] = (passednum,passed,cenum,ces) |
|
526 | combine (passednum,passed) (cenum,ces) ((t, []) :: xs) = |
|
527 combine (passednum+1,(cterm_of usedthy t)::passed) (cenum,ces) xs |
|
528 | combine (passednum,passed) (cenum,ces) ((t, x) :: xs) = |
|
529 combine (passednum,passed) |
|
530 (cenum+1,(cterm_of usedthy t, x) :: ces) xs |
|
531 in |
|
532 combine (0,[]) (0,[]) checked |
|
533 end; |
|
534 |
|
535 |
|
536 (*create a string of a list of terms*) |
506 (*create a string of a list of terms*) |
537 |
507 |
538 fun string_of_ctermlist thy [] acc = acc |
508 fun string_of_ctermlist thy [] acc = acc |
539 | string_of_ctermlist thy (x::xs) acc = |
509 | string_of_ctermlist thy (x::xs) acc = |
540 string_of_ctermlist thy xs ((Syntax.string_of_term_global thy (term_of x)) ^ "\n" ^ acc); |
510 string_of_ctermlist thy xs ((Syntax.string_of_term_global thy (term_of x)) ^ "\n" ^ acc); |