author | wenzelm |
Wed, 25 Jul 2012 18:05:07 +0200 | |
changeset 48502 | fd03877ad5bc |
parent 46711 | f745bcc4a1e5 |
child 48891 | c0eafbd55de3 |
permissions | -rw-r--r-- |
46711
f745bcc4a1e5
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
wenzelm
parents:
42361
diff
changeset
|
1 |
(* FIXME dead code!?!? *) |
f745bcc4a1e5
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
wenzelm
parents:
42361
diff
changeset
|
2 |
|
34965 | 3 |
theory Mutabelle |
4 |
imports Main |
|
5 |
uses "mutabelle.ML" |
|
6 |
begin |
|
7 |
||
8 |
ML {* |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
9 |
val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]; |
34965 | 10 |
|
11 |
val forbidden = |
|
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset
|
12 |
[(@{const_name Power.power}, "'a"), |
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset
|
13 |
(@{const_name HOL.induct_equal}, "'a"), |
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset
|
14 |
(@{const_name HOL.induct_implies}, "'a"), |
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset
|
15 |
(@{const_name HOL.induct_conj}, "'a"), |
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset
|
16 |
(@{const_name HOL.undefined}, "'a"), |
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset
|
17 |
(@{const_name HOL.default}, "'a"), |
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset
|
18 |
(@{const_name dummy_pattern}, "'a::{}"), |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
19 |
(@{const_name Groups.uminus}, "'a"), |
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset
|
20 |
(@{const_name Nat.size}, "'a"), |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
34974
diff
changeset
|
21 |
(@{const_name Groups.abs}, "'a")]; |
34965 | 22 |
|
23 |
val forbidden_thms = |
|
24 |
["finite_intvl_succ_class", |
|
25 |
"nibble"]; |
|
26 |
||
27 |
val forbidden_consts = |
|
28 |
[@{const_name nibble_pair_of_char}]; |
|
29 |
||
30 |
fun is_forbidden s th = |
|
46711
f745bcc4a1e5
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
wenzelm
parents:
42361
diff
changeset
|
31 |
exists (fn s' => s' mem Long_Name.explode s) forbidden_thms orelse |
34965 | 32 |
exists (fn s' => s' mem (Term.add_const_names (prop_of th) [])) forbidden_consts; |
33 |
||
34 |
fun test j = List.app (fn i => |
|
35 |
Mutabelle.mutqc_thystat_mix is_forbidden |
|
36 |
@{theory List} @{theory Main} comms forbidden 1 [] i j ("list_" ^ string_of_int i ^ ".txt")) |
|
37 |
(1 upto 10); |
|
38 |
||
39 |
fun get_numbers xs = |
|
40 |
let |
|
41 |
val (_, xs1) = take_prefix (not o equal ":") xs; |
|
42 |
val (_, xs2) = take_prefix (fn ":" => true | " " => true | _ => false) xs1; |
|
43 |
val (xs3, xs4) = take_prefix Symbol.is_digit xs2; |
|
44 |
val (_, xs5) = take_prefix (equal " ") xs4; |
|
45 |
val (xs6, xs7) = take_prefix Symbol.is_digit xs5 |
|
46 |
in |
|
47 |
case (xs3, xs6) of |
|
48 |
([], _) => NONE |
|
49 |
| (_, []) => NONE |
|
50 |
| (ys, zs) => SOME (fst (read_int ys), fst (read_int zs), xs7) |
|
51 |
end; |
|
52 |
||
53 |
fun add_numbers s = |
|
54 |
let |
|
55 |
fun strip ("\n" :: "\n" :: "\n" :: xs) = xs |
|
56 |
| strip (_ :: xs) = strip xs; |
|
57 |
||
58 |
fun add (i, j) xs = (case get_numbers xs of |
|
59 |
NONE => (i, j) |
|
60 |
| SOME (i', j', xs') => add (i+i', j+j') xs') |
|
61 |
in add (0,0) (strip (explode s)) end; |
|
62 |
*} |
|
63 |
||
64 |
(* |
|
65 |
ML {* |
|
42361 | 66 |
Quickcheck.test_term (Proof_Context.init_global @{theory}) |
34965 | 67 |
false (SOME "SML") 1 1 (prop_of (hd @{thms nibble_pair_of_char_simps})) |
68 |
*} |
|
69 |
||
70 |
ML {* |
|
71 |
fun is_executable thy th = can (Quickcheck.test_term |
|
42361 | 72 |
(Proof_Context.init_global thy) false (SOME "SML") 1 1) (prop_of th); |
34965 | 73 |
|
74 |
fun is_executable_term thy t = can (Quickcheck.test_term |
|
42361 | 75 |
(Proof_Context.init_global thy) false (SOME "SML") 1 1) t; |
34965 | 76 |
|
77 |
fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso |
|
78 |
Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso |
|
79 |
is_executable thy th) |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38864
diff
changeset
|
80 |
(Global_Theory.all_thms_of thy); |
34965 | 81 |
|
82 |
fun find_thm thy = find_first (fn (_, th) => not (Thm.is_internal th) andalso |
|
83 |
Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso |
|
84 |
is_executable thy th) |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38864
diff
changeset
|
85 |
(Global_Theory.all_thms_of thy); |
34965 | 86 |
*} |
87 |
||
88 |
ML {* |
|
89 |
is_executable @{theory} (hd @{thms nibble_pair_of_char_simps}) |
|
90 |
*} |
|
91 |
*) |
|
92 |
||
93 |
ML {* |
|
94 |
Mutabelle.mutate_mix @{term "Suc x \<noteq> 0"} @{theory} comms forbidden 1 |
|
95 |
*} |
|
96 |
||
97 |
ML {* |
|
98 |
Mutabelle.mutqc_thystat_mix is_forbidden @{theory Nat} @{theory} comms forbidden 1 [] 10 5 "/tmp/muta.out" |
|
99 |
*} |
|
100 |
||
101 |
end |