34965
|
1 |
theory Mutabelle
|
|
2 |
imports Main
|
|
3 |
uses "mutabelle.ML"
|
|
4 |
begin
|
|
5 |
|
|
6 |
ML {*
|
|
7 |
val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}];
|
|
8 |
|
|
9 |
val forbidden =
|
|
10 |
[(@{const_name "power"}, "'a"),
|
|
11 |
("HOL.induct_equal", "'a"),
|
|
12 |
("HOL.induct_implies", "'a"),
|
|
13 |
("HOL.induct_conj", "'a"),
|
|
14 |
(@{const_name "undefined"}, "'a"),
|
|
15 |
(@{const_name "default"}, "'a"),
|
|
16 |
(@{const_name "dummy_pattern"}, "'a::{}"),
|
|
17 |
(@{const_name "uminus"}, "'a"),
|
|
18 |
(@{const_name "Nat.size"}, "'a"),
|
|
19 |
(@{const_name "HOL.abs"}, "'a")];
|
|
20 |
|
|
21 |
val forbidden_thms =
|
|
22 |
["finite_intvl_succ_class",
|
|
23 |
"nibble"];
|
|
24 |
|
|
25 |
val forbidden_consts =
|
|
26 |
[@{const_name nibble_pair_of_char}];
|
|
27 |
|
|
28 |
fun is_forbidden s th =
|
|
29 |
exists (fn s' => s' mem space_explode "." s) forbidden_thms orelse
|
|
30 |
exists (fn s' => s' mem (Term.add_const_names (prop_of th) [])) forbidden_consts;
|
|
31 |
|
|
32 |
fun test j = List.app (fn i =>
|
|
33 |
Mutabelle.mutqc_thystat_mix is_forbidden
|
|
34 |
@{theory List} @{theory Main} comms forbidden 1 [] i j ("list_" ^ string_of_int i ^ ".txt"))
|
|
35 |
(1 upto 10);
|
|
36 |
|
|
37 |
fun get_numbers xs =
|
|
38 |
let
|
|
39 |
val (_, xs1) = take_prefix (not o equal ":") xs;
|
|
40 |
val (_, xs2) = take_prefix (fn ":" => true | " " => true | _ => false) xs1;
|
|
41 |
val (xs3, xs4) = take_prefix Symbol.is_digit xs2;
|
|
42 |
val (_, xs5) = take_prefix (equal " ") xs4;
|
|
43 |
val (xs6, xs7) = take_prefix Symbol.is_digit xs5
|
|
44 |
in
|
|
45 |
case (xs3, xs6) of
|
|
46 |
([], _) => NONE
|
|
47 |
| (_, []) => NONE
|
|
48 |
| (ys, zs) => SOME (fst (read_int ys), fst (read_int zs), xs7)
|
|
49 |
end;
|
|
50 |
|
|
51 |
fun add_numbers s =
|
|
52 |
let
|
|
53 |
fun strip ("\n" :: "\n" :: "\n" :: xs) = xs
|
|
54 |
| strip (_ :: xs) = strip xs;
|
|
55 |
|
|
56 |
fun add (i, j) xs = (case get_numbers xs of
|
|
57 |
NONE => (i, j)
|
|
58 |
| SOME (i', j', xs') => add (i+i', j+j') xs')
|
|
59 |
in add (0,0) (strip (explode s)) end;
|
|
60 |
*}
|
|
61 |
|
|
62 |
(*
|
|
63 |
ML {*
|
|
64 |
Quickcheck.test_term (ProofContext.init @{theory})
|
|
65 |
false (SOME "SML") 1 1 (prop_of (hd @{thms nibble_pair_of_char_simps}))
|
|
66 |
*}
|
|
67 |
|
|
68 |
ML {*
|
|
69 |
fun is_executable thy th = can (Quickcheck.test_term
|
|
70 |
(ProofContext.init thy) false (SOME "SML") 1 1) (prop_of th);
|
|
71 |
|
|
72 |
fun is_executable_term thy t = can (Quickcheck.test_term
|
|
73 |
(ProofContext.init thy) false (SOME "SML") 1 1) t;
|
|
74 |
|
|
75 |
fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso
|
|
76 |
Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
|
|
77 |
is_executable thy th)
|
|
78 |
(PureThy.all_thms_of thy);
|
|
79 |
|
|
80 |
fun find_thm thy = find_first (fn (_, th) => not (Thm.is_internal th) andalso
|
|
81 |
Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
|
|
82 |
is_executable thy th)
|
|
83 |
(PureThy.all_thms_of thy);
|
|
84 |
*}
|
|
85 |
|
|
86 |
ML {*
|
|
87 |
is_executable @{theory} (hd @{thms nibble_pair_of_char_simps})
|
|
88 |
*}
|
|
89 |
*)
|
|
90 |
|
|
91 |
ML {*
|
|
92 |
Mutabelle.mutate_mix @{term "Suc x \<noteq> 0"} @{theory} comms forbidden 1
|
|
93 |
*}
|
|
94 |
|
|
95 |
ML {*
|
|
96 |
Mutabelle.mutqc_thystat_mix is_forbidden @{theory Nat} @{theory} comms forbidden 1 [] 10 5 "/tmp/muta.out"
|
|
97 |
*}
|
|
98 |
|
|
99 |
end |