src/HOL/Mutabelle/Mutabelle.thy
author haftmann
Sat Aug 28 16:14:32 2010 +0200 (2010-08-28)
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39557 fe5722fce758
permissions -rw-r--r--
formerly unnamed infix equality now named HOL.eq
     1 theory Mutabelle
     2 imports Main
     3 uses "mutabelle.ML"
     4 begin
     5 
     6 ML {*
     7 val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}];
     8 
     9 val forbidden =
    10  [(@{const_name Power.power}, "'a"),
    11   (@{const_name HOL.induct_equal}, "'a"),
    12   (@{const_name HOL.induct_implies}, "'a"),
    13   (@{const_name HOL.induct_conj}, "'a"),
    14   (@{const_name HOL.undefined}, "'a"),
    15   (@{const_name HOL.default}, "'a"),
    16   (@{const_name dummy_pattern}, "'a::{}"),
    17   (@{const_name Groups.uminus}, "'a"),
    18   (@{const_name Nat.size}, "'a"),
    19   (@{const_name Groups.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_global @{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_global thy) false (SOME "SML") 1 1) (prop_of th);
    71 
    72 fun is_executable_term thy t = can (Quickcheck.test_term
    73  (ProofContext.init_global 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