src/HOL/Mutabelle/Mutabelle.thy
changeset 34965 3b4762c1052c
child 34974 18b41bba42b5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Mon Jan 25 16:19:42 2010 +0100
     1.3 @@ -0,0 +1,99 @@
     1.4 +theory Mutabelle
     1.5 +imports Main
     1.6 +uses "mutabelle.ML"
     1.7 +begin
     1.8 +
     1.9 +ML {*
    1.10 +val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}];
    1.11 +
    1.12 +val forbidden =
    1.13 + [(@{const_name "power"}, "'a"),
    1.14 +  ("HOL.induct_equal", "'a"),
    1.15 +  ("HOL.induct_implies", "'a"),
    1.16 +  ("HOL.induct_conj", "'a"),
    1.17 +  (@{const_name "undefined"}, "'a"),
    1.18 +  (@{const_name "default"}, "'a"),
    1.19 +  (@{const_name "dummy_pattern"}, "'a::{}"),
    1.20 +  (@{const_name "uminus"}, "'a"),
    1.21 +  (@{const_name "Nat.size"}, "'a"),
    1.22 +  (@{const_name "HOL.abs"}, "'a")];
    1.23 +
    1.24 +val forbidden_thms =
    1.25 + ["finite_intvl_succ_class",
    1.26 +  "nibble"];
    1.27 +
    1.28 +val forbidden_consts =
    1.29 + [@{const_name nibble_pair_of_char}];
    1.30 +
    1.31 +fun is_forbidden s th =
    1.32 + exists (fn s' => s' mem space_explode "." s) forbidden_thms orelse
    1.33 + exists (fn s' => s' mem (Term.add_const_names (prop_of th) [])) forbidden_consts;
    1.34 +
    1.35 +fun test j = List.app (fn i =>
    1.36 + Mutabelle.mutqc_thystat_mix is_forbidden
    1.37 +   @{theory List} @{theory Main} comms forbidden 1 [] i j ("list_" ^ string_of_int i ^ ".txt"))
    1.38 + (1 upto 10);
    1.39 +
    1.40 +fun get_numbers xs =
    1.41 + let
    1.42 +   val (_, xs1) = take_prefix (not o equal ":") xs;
    1.43 +   val (_, xs2) = take_prefix (fn ":" => true | " " => true | _ => false) xs1;
    1.44 +   val (xs3, xs4) = take_prefix Symbol.is_digit xs2;
    1.45 +   val (_, xs5) = take_prefix (equal " ") xs4;
    1.46 +   val (xs6, xs7) = take_prefix Symbol.is_digit xs5
    1.47 + in
    1.48 +   case (xs3, xs6) of
    1.49 +     ([], _) => NONE
    1.50 +   | (_, []) => NONE
    1.51 +   | (ys, zs) => SOME (fst (read_int ys), fst (read_int zs), xs7)
    1.52 + end;
    1.53 +
    1.54 +fun add_numbers s =
    1.55 + let
    1.56 +   fun strip ("\n" :: "\n" :: "\n" :: xs) = xs
    1.57 +     | strip (_ :: xs) = strip xs;
    1.58 +
    1.59 +   fun add (i, j) xs = (case get_numbers xs of
    1.60 +         NONE => (i, j)
    1.61 +       | SOME (i', j', xs') => add (i+i', j+j') xs')
    1.62 + in add (0,0) (strip (explode s)) end;
    1.63 +*}
    1.64 +
    1.65 +(*
    1.66 +ML {*
    1.67 +Quickcheck.test_term (ProofContext.init @{theory})
    1.68 + false (SOME "SML") 1 1 (prop_of (hd @{thms nibble_pair_of_char_simps}))
    1.69 +*}
    1.70 +
    1.71 +ML {*
    1.72 +fun is_executable thy th = can (Quickcheck.test_term
    1.73 + (ProofContext.init thy) false (SOME "SML") 1 1) (prop_of th);
    1.74 +
    1.75 +fun is_executable_term thy t = can (Quickcheck.test_term
    1.76 + (ProofContext.init thy) false (SOME "SML") 1 1) t;
    1.77 +
    1.78 +fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso
    1.79 +   Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
    1.80 +   is_executable thy th)
    1.81 + (PureThy.all_thms_of thy);
    1.82 +
    1.83 +fun find_thm thy = find_first (fn (_, th) => not (Thm.is_internal th) andalso
    1.84 +   Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
    1.85 +   is_executable thy th)
    1.86 + (PureThy.all_thms_of thy);
    1.87 +*}
    1.88 +
    1.89 +ML {*
    1.90 +is_executable @{theory} (hd @{thms nibble_pair_of_char_simps})
    1.91 +*}
    1.92 +*)
    1.93 +
    1.94 +ML {*
    1.95 +Mutabelle.mutate_mix @{term "Suc x \<noteq> 0"} @{theory} comms forbidden 1
    1.96 +*}
    1.97 +
    1.98 +ML {*
    1.99 +Mutabelle.mutqc_thystat_mix is_forbidden @{theory Nat} @{theory} comms forbidden 1 [] 10 5 "/tmp/muta.out"
   1.100 +*}
   1.101 +
   1.102 +end
   1.103 \ No newline at end of file