wenzelm@46711: (* FIXME dead code!?!? *)
wenzelm@46711: 
bulwahn@34965: theory Mutabelle
bulwahn@34965: imports Main
bulwahn@34965: uses "mutabelle.ML"
bulwahn@34965: begin
bulwahn@34965: 
bulwahn@34965: ML {*
haftmann@38864: val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}];
bulwahn@34965: 
bulwahn@34965: val forbidden =
haftmann@34974:  [(@{const_name Power.power}, "'a"),
haftmann@34974:   (@{const_name HOL.induct_equal}, "'a"),
haftmann@34974:   (@{const_name HOL.induct_implies}, "'a"),
haftmann@34974:   (@{const_name HOL.induct_conj}, "'a"),
haftmann@34974:   (@{const_name HOL.undefined}, "'a"),
haftmann@34974:   (@{const_name HOL.default}, "'a"),
haftmann@34974:   (@{const_name dummy_pattern}, "'a::{}"),
haftmann@35267:   (@{const_name Groups.uminus}, "'a"),
haftmann@34974:   (@{const_name Nat.size}, "'a"),
haftmann@35092:   (@{const_name Groups.abs}, "'a")];
bulwahn@34965: 
bulwahn@34965: val forbidden_thms =
bulwahn@34965:  ["finite_intvl_succ_class",
bulwahn@34965:   "nibble"];
bulwahn@34965: 
bulwahn@34965: val forbidden_consts =
bulwahn@34965:  [@{const_name nibble_pair_of_char}];
bulwahn@34965: 
bulwahn@34965: fun is_forbidden s th =
wenzelm@46711:  exists (fn s' => s' mem Long_Name.explode s) forbidden_thms orelse
bulwahn@34965:  exists (fn s' => s' mem (Term.add_const_names (prop_of th) [])) forbidden_consts;
bulwahn@34965: 
bulwahn@34965: fun test j = List.app (fn i =>
bulwahn@34965:  Mutabelle.mutqc_thystat_mix is_forbidden
bulwahn@34965:    @{theory List} @{theory Main} comms forbidden 1 [] i j ("list_" ^ string_of_int i ^ ".txt"))
bulwahn@34965:  (1 upto 10);
bulwahn@34965: 
bulwahn@34965: fun get_numbers xs =
bulwahn@34965:  let
bulwahn@34965:    val (_, xs1) = take_prefix (not o equal ":") xs;
bulwahn@34965:    val (_, xs2) = take_prefix (fn ":" => true | " " => true | _ => false) xs1;
bulwahn@34965:    val (xs3, xs4) = take_prefix Symbol.is_digit xs2;
bulwahn@34965:    val (_, xs5) = take_prefix (equal " ") xs4;
bulwahn@34965:    val (xs6, xs7) = take_prefix Symbol.is_digit xs5
bulwahn@34965:  in
bulwahn@34965:    case (xs3, xs6) of
bulwahn@34965:      ([], _) => NONE
bulwahn@34965:    | (_, []) => NONE
bulwahn@34965:    | (ys, zs) => SOME (fst (read_int ys), fst (read_int zs), xs7)
bulwahn@34965:  end;
bulwahn@34965: 
bulwahn@34965: fun add_numbers s =
bulwahn@34965:  let
bulwahn@34965:    fun strip ("\n" :: "\n" :: "\n" :: xs) = xs
bulwahn@34965:      | strip (_ :: xs) = strip xs;
bulwahn@34965: 
bulwahn@34965:    fun add (i, j) xs = (case get_numbers xs of
bulwahn@34965:          NONE => (i, j)
bulwahn@34965:        | SOME (i', j', xs') => add (i+i', j+j') xs')
bulwahn@34965:  in add (0,0) (strip (explode s)) end;
bulwahn@34965: *}
bulwahn@34965: 
bulwahn@34965: (*
bulwahn@34965: ML {*
wenzelm@42361: Quickcheck.test_term (Proof_Context.init_global @{theory})
bulwahn@34965:  false (SOME "SML") 1 1 (prop_of (hd @{thms nibble_pair_of_char_simps}))
bulwahn@34965: *}
bulwahn@34965: 
bulwahn@34965: ML {*
bulwahn@34965: fun is_executable thy th = can (Quickcheck.test_term
wenzelm@42361:  (Proof_Context.init_global thy) false (SOME "SML") 1 1) (prop_of th);
bulwahn@34965: 
bulwahn@34965: fun is_executable_term thy t = can (Quickcheck.test_term
wenzelm@42361:  (Proof_Context.init_global thy) false (SOME "SML") 1 1) t;
bulwahn@34965: 
bulwahn@34965: fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso
bulwahn@34965:    Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
bulwahn@34965:    is_executable thy th)
wenzelm@39557:  (Global_Theory.all_thms_of thy);
bulwahn@34965: 
bulwahn@34965: fun find_thm thy = find_first (fn (_, th) => not (Thm.is_internal th) andalso
bulwahn@34965:    Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
bulwahn@34965:    is_executable thy th)
wenzelm@39557:  (Global_Theory.all_thms_of thy);
bulwahn@34965: *}
bulwahn@34965: 
bulwahn@34965: ML {*
bulwahn@34965: is_executable @{theory} (hd @{thms nibble_pair_of_char_simps})
bulwahn@34965: *}
bulwahn@34965: *)
bulwahn@34965: 
bulwahn@34965: ML {*
bulwahn@34965: Mutabelle.mutate_mix @{term "Suc x \<noteq> 0"} @{theory} comms forbidden 1
bulwahn@34965: *}
bulwahn@34965: 
bulwahn@34965: ML {*
bulwahn@34965: Mutabelle.mutqc_thystat_mix is_forbidden @{theory Nat} @{theory} comms forbidden 1 [] 10 5 "/tmp/muta.out"
bulwahn@34965: *}
bulwahn@34965: 
bulwahn@34965: end