author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 48891  c0eafbd55de3 
permissions  rwrr 
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 
begin 

6 

48891  7 
ML_file "mutabelle.ML" 
8 

34965  9 
ML {* 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

10 
val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]; 
34965  11 

12 
val forbidden = 

34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset

13 
[(@{const_name Power.power}, "'a"), 
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset

14 
(@{const_name HOL.induct_equal}, "'a"), 
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset

15 
(@{const_name HOL.induct_implies}, "'a"), 
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset

16 
(@{const_name HOL.induct_conj}, "'a"), 
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset

17 
(@{const_name HOL.undefined}, "'a"), 
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset

18 
(@{const_name HOL.default}, "'a"), 
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset

19 
(@{const_name dummy_pattern}, "'a::{}"), 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

20 
(@{const_name Groups.uminus}, "'a"), 
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34965
diff
changeset

21 
(@{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

22 
(@{const_name Groups.abs}, "'a")]; 
34965  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 = 

46711
f745bcc4a1e5
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
wenzelm
parents:
42361
diff
changeset

32 
exists (fn s' => s' mem Long_Name.explode s) forbidden_thms orelse 
34965  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 {* 

42361  67 
Quickcheck.test_term (Proof_Context.init_global @{theory}) 
34965  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 

42361  73 
(Proof_Context.init_global thy) false (SOME "SML") 1 1) (prop_of th); 
34965  74 

75 
fun is_executable_term thy t = can (Quickcheck.test_term 

42361  76 
(Proof_Context.init_global thy) false (SOME "SML") 1 1) t; 
34965  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) 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38864
diff
changeset

81 
(Global_Theory.all_thms_of thy); 
34965  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) 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38864
diff
changeset

86 
(Global_Theory.all_thms_of thy); 
34965  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 