# HG changeset patch # User wenzelm # Date 1394875782 -3600 # Node ID 7cfe7b6d501a0f3e88a8d32fe1bb72f27a14db2c # Parent 47015872e7950694350e8f18ffe9f8a3abe29cf6 removed dead code; diff -r 47015872e795 -r 7cfe7b6d501a src/HOL/Mutabelle/Mutabelle.thy --- a/src/HOL/Mutabelle/Mutabelle.thy Sat Mar 15 10:24:49 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,102 +0,0 @@ -(* FIXME dead code!?!? *) - -theory Mutabelle -imports Main -begin - -ML_file "mutabelle.ML" - -ML {* -val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]; - -val forbidden = - [(@{const_name Power.power}, "'a"), - (@{const_name HOL.induct_equal}, "'a"), - (@{const_name HOL.induct_implies}, "'a"), - (@{const_name HOL.induct_conj}, "'a"), - (@{const_name HOL.undefined}, "'a"), - (@{const_name HOL.default}, "'a"), - (@{const_name dummy_pattern}, "'a::{}"), - (@{const_name Groups.uminus}, "'a"), - (@{const_name Nat.size}, "'a"), - (@{const_name Groups.abs}, "'a")]; - -val forbidden_thms = - ["finite_intvl_succ_class", - "nibble"]; - -val forbidden_consts = - [@{const_name nibble_pair_of_char}]; - -fun is_forbidden s th = - exists (fn s' => s' mem Long_Name.explode s) forbidden_thms orelse - exists (fn s' => s' mem (Term.add_const_names (prop_of th) [])) forbidden_consts; - -fun test j = List.app (fn i => - Mutabelle.mutqc_thystat_mix is_forbidden - @{theory List} @{theory Main} comms forbidden 1 [] i j ("list_" ^ string_of_int i ^ ".txt")) - (1 upto 10); - -fun get_numbers xs = - let - val (_, xs1) = take_prefix (not o equal ":") xs; - val (_, xs2) = take_prefix (fn ":" => true | " " => true | _ => false) xs1; - val (xs3, xs4) = take_prefix Symbol.is_digit xs2; - val (_, xs5) = take_prefix (equal " ") xs4; - val (xs6, xs7) = take_prefix Symbol.is_digit xs5 - in - case (xs3, xs6) of - ([], _) => NONE - | (_, []) => NONE - | (ys, zs) => SOME (fst (read_int ys), fst (read_int zs), xs7) - end; - -fun add_numbers s = - let - fun strip ("\n" :: "\n" :: "\n" :: xs) = xs - | strip (_ :: xs) = strip xs; - - fun add (i, j) xs = (case get_numbers xs of - NONE => (i, j) - | SOME (i', j', xs') => add (i+i', j+j') xs') - in add (0,0) (strip (explode s)) end; -*} - -(* -ML {* -Quickcheck.test_term (Proof_Context.init_global @{theory}) - false (SOME "SML") 1 1 (prop_of (hd @{thms nibble_pair_of_char_simps})) -*} - -ML {* -fun is_executable thy th = can (Quickcheck.test_term - (Proof_Context.init_global thy) false (SOME "SML") 1 1) (prop_of th); - -fun is_executable_term thy t = can (Quickcheck.test_term - (Proof_Context.init_global thy) false (SOME "SML") 1 1) t; - -fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso - Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso - is_executable thy th) - (Global_Theory.all_thms_of thy); - -fun find_thm thy = find_first (fn (_, th) => not (Thm.is_internal th) andalso - Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso - is_executable thy th) - (Global_Theory.all_thms_of thy); -*} - -ML {* -is_executable @{theory} (hd @{thms nibble_pair_of_char_simps}) -*} -*) - -ML {* -Mutabelle.mutate_mix @{term "Suc x \ 0"} @{theory} comms forbidden 1 -*} - -ML {* -Mutabelle.mutqc_thystat_mix is_forbidden @{theory Nat} @{theory} comms forbidden 1 [] 10 5 "/tmp/muta.out" -*} - -end \ No newline at end of file