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