# HG changeset patch
# User bulwahn
# Date 1264432782 -3600
# Node ID 3b4762c1052ceab531f46e2f86757b6f4a9fcc8d
# Parent  366a1a44aac22b48595268381c68a95b23ff3821
adding Mutabelle to repository

diff -r 366a1a44aac2 -r 3b4762c1052c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jan 22 16:59:21 2010 +0100
+++ b/src/HOL/IsaMakefile	Mon Jan 25 16:19:42 2010 +0100
@@ -1420,6 +1420,16 @@
 	@cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples
 
 
+## HOL-Mutabelle
+
+HOL-Mutabelle: HOL $(LOG)/HOL-Mutabelle.gz
+
+$(LOG)/HOL-Mutabelle.gz: $(OUT)/HOL Mutabelle/MutabelleExtra.thy	\
+  Mutabelle/ROOT.ML Mutabelle/mutabelle.ML			\
+  Mutabelle/mutabelle_extra.ML
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mutabelle
+
+
 ## clean
 
 clean:
diff -r 366a1a44aac2 -r 3b4762c1052c src/HOL/Mutabelle/Mutabelle.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mutabelle/Mutabelle.thy	Mon Jan 25 16:19:42 2010 +0100
@@ -0,0 +1,99 @@
+theory Mutabelle
+imports Main
+uses "mutabelle.ML"
+begin
+
+ML {*
+val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}];
+
+val forbidden =
+ [(@{const_name "power"}, "'a"),
+  ("HOL.induct_equal", "'a"),
+  ("HOL.induct_implies", "'a"),
+  ("HOL.induct_conj", "'a"),
+  (@{const_name "undefined"}, "'a"),
+  (@{const_name "default"}, "'a"),
+  (@{const_name "dummy_pattern"}, "'a::{}"),
+  (@{const_name "uminus"}, "'a"),
+  (@{const_name "Nat.size"}, "'a"),
+  (@{const_name "HOL.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 space_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 (ProofContext.init @{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
+ (ProofContext.init thy) false (SOME "SML") 1 1) (prop_of th);
+
+fun is_executable_term thy t = can (Quickcheck.test_term
+ (ProofContext.init 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)
+ (PureThy.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)
+ (PureThy.all_thms_of thy);
+*}
+
+ML {*
+is_executable @{theory} (hd @{thms nibble_pair_of_char_simps})
+*}
+*)
+
+ML {*
+Mutabelle.mutate_mix @{term "Suc x \<noteq> 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
diff -r 366a1a44aac2 -r 3b4762c1052c src/HOL/Mutabelle/MutabelleExtra.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Jan 25 16:19:42 2010 +0100
@@ -0,0 +1,56 @@
+theory MutabelleExtra
+imports Complex_Main SML_Quickcheck
+(*
+  "~/Downloads/Jinja/J/TypeSafe"
+  "~/Downloads/Jinja/J/Annotate"
+  (* FIXME "Example" *)
+  "~/Downloads/Jinja/J/execute_Bigstep"
+  "~/Downloads/Jinja/J/execute_WellType"
+  "~/Downloads/Jinja/JVM/JVMDefensive"
+  "~/Downloads/Jinja/JVM/JVMListExample"
+  "~/Downloads/Jinja/BV/BVExec"
+  "~/Downloads/Jinja/BV/LBVJVM"
+  "~/Downloads/Jinja/BV/BVNoTypeError"
+  "~/Downloads/Jinja/BV/BVExample"
+  "~/Downloads/Jinja/Compiler/TypeComp"
+*)
+(*"~/Downloads/NormByEval/NBE"*)
+uses "mutabelle.ML"
+     "mutabelle_extra.ML"
+begin
+
+ML {* val old_tr = !Output.tracing_fn *}
+ML {* val old_wr = !Output.writeln_fn *}
+ML {* val old_pr = !Output.priority_fn *}
+ML {* val old_wa = !Output.warning_fn *}
+
+quickcheck_params [size = 5, iterations = 1000]
+(*
+nitpick_params [timeout = 5 s, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
+refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
+*)
+ML {* Auto_Counterexample.time_limit := 10 *}
+
+
+text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
+
+ML {*
+(*
+      MutabelleExtra.random_seed := 1.0;
+      MutabelleExtra.thms_of true @{theory Complex_Main}
+      |> MutabelleExtra.take_random 1000000
+      |> (fn thms => List.drop (thms, 1000))
+      |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
+             @{theory} [MutabelleExtra.quickcheck_mtd "SML",
+                        MutabelleExtra.quickcheck_mtd "code"
+                        (*MutabelleExtra.refute_mtd,
+                        MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")
+*)
+ *}
+
+ML {* Output.tracing_fn := old_tr *}
+ML {* Output.writeln_fn := old_wr *}
+ML {* Output.priority_fn := old_pr *}
+ML {* Output.warning_fn := old_wa *}
+
+end
\ No newline at end of file
diff -r 366a1a44aac2 -r 3b4762c1052c src/HOL/Mutabelle/mutabelle.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mutabelle/mutabelle.ML	Mon Jan 25 16:19:42 2010 +0100
@@ -0,0 +1,776 @@
+(*
+    Title:      HOL/Mutabelle/mutabelle.ML
+    Author:     Stefan Berghofer, TU Muenchen
+
+    Mutation of theorems
+*)
+signature MUTABELLE =
+sig
+ val testgen_name : string Unsynchronized.ref
+ exception WrongPath of string;
+ exception WrongArg of string;
+ val freeze : term -> term
+ val mutate_exc : term -> string list -> int -> term list 
+ val mutate_sign : term -> theory -> (string * string) list -> int -> term list 
+ val mutate_mix : term -> theory -> string list -> 
+   (string * string) list -> int -> term list
+ val qc_test : term list -> (typ * typ) list -> theory ->
+  int -> int -> int * Thm.cterm list * int * (Thm.cterm * (string * Thm.cterm) list) list
+ val qc_test_file : bool -> term list -> (typ * typ) list 
+   -> theory -> int -> int -> string -> unit
+ val mutqc_file_exc : theory -> string list ->
+  int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit
+ val mutqc_file_sign : theory -> (string * string) list ->
+  int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit
+ val mutqc_file_mix : theory -> string list -> (string * string) list ->
+  int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit
+ val mutqc_file_rec_exc : theory -> string list -> int ->
+  Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit
+ val mutqc_file_rec_sign : theory -> (string * string) list -> int ->
+  Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit
+ val mutqc_file_rec_mix : theory -> string list -> (string * string) list ->
+  int -> Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit
+ val mutqc_thy_exc : theory -> theory ->
+  string list -> int -> (typ * typ) list -> int -> int -> string -> unit
+ val mutqc_thy_sign : theory -> theory -> (string * string) list ->
+  int -> (typ * typ) list -> int -> int -> string -> unit
+ val mutqc_thy_mix : theory -> theory -> string list -> (string * string) list ->
+  int -> (typ * typ) list -> int -> int -> string -> unit
+ val mutqc_file_stat_sign : theory -> (string * string) list ->
+  int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit
+ val mutqc_file_stat_exc : theory -> string list ->
+  int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit
+ val mutqc_file_stat_mix : theory -> string list -> (string * string) list ->
+  int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit
+ val mutqc_thystat_exc : (string -> thm -> bool) -> theory -> theory ->
+  string list -> int -> (typ * typ) list -> int -> int -> string -> unit
+ val mutqc_thystat_sign : (string -> thm -> bool) -> theory -> theory -> (string * string) list ->
+  int -> (typ * typ) list -> int -> int -> string -> unit
+ val mutqc_thystat_mix : (string -> thm -> bool) -> theory -> theory -> string list -> 
+  (string * string) list -> int -> (typ * typ) list -> int -> int -> string -> unit
+ val canonize_term: term -> string list -> term
+ 
+ val all_unconcealed_thms_of : theory -> (string * thm) list
+end;
+
+val bar = Unsynchronized.ref ([] : term list);
+val bla = Unsynchronized.ref (Bound 0);
+fun store x = (bla := x; x);
+
+structure Mutabelle : MUTABELLE = 
+struct
+
+val testgen_name = Unsynchronized.ref "SML";
+
+(*
+fun is_executable thy th = can (Quickcheck.test_term
+ (ProofContext.init thy) false (SOME (!testgen_name)) 1 1) (prop_of th);
+*)
+
+fun all_unconcealed_thms_of thy =
+  let
+    val facts = PureThy.facts_of thy
+  in
+    Facts.fold_static
+      (fn (s, ths) =>
+        if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths))
+      facts []
+  end;
+
+fun thms_of thy = filter (fn (_, th) =>
+   Context.theory_name (theory_of_thm th) = Context.theory_name thy) (all_unconcealed_thms_of thy);
+
+fun consts_of thy =
+ let
+   val (namespace, const_table) = #constants (Consts.dest (Sign.consts_of thy))
+   val consts = Symtab.dest const_table
+ in
+   List.mapPartial (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
+     (filter_out (fn (s, _) => Name_Space.is_concealed namespace s) consts)
+ end;
+
+
+(*helper function in order to properly print a term*)
+
+fun prt x = Pretty.writeln (Syntax.pretty_term_global (theory "Main") x);
+
+
+(*possibility to print a given term for debugging purposes*)
+
+val debug = (Unsynchronized.ref false);
+fun debug_msg mutterm = if (!debug) then (prt mutterm) else ();
+
+
+(*thrown in case the specified path doesn't exist in the specified term*)
+
+exception WrongPath of string;
+
+
+(*thrown in case the arguments did not fit to the function*)
+
+exception WrongArg of string; 
+
+(*Rename the bound variables in a term with the minimal Index min of 
+bound variables. Variable (Bound(min)) will be renamed to Bound(0) etc. 
+This is needed in course auf evaluation of contexts.*)
+
+fun rename_bnds curTerm 0 = curTerm
+ | rename_bnds (Bound(i)) minInd = 
+   let 
+     val erg = if (i-minInd < 0) then 0 else (i - minInd)
+   in 
+     Bound(erg)
+   end
+ | rename_bnds (Abs(name,t,uTerm)) minInd = 
+   Abs(name,t,(rename_bnds uTerm minInd))
+ | rename_bnds (fstUTerm $ sndUTerm) minInd =
+   (rename_bnds fstUTerm minInd) $ (rename_bnds sndUTerm minInd)
+ | rename_bnds elseTerm minInd = elseTerm;
+
+
+
+
+
+(*Partition a term in its subterms and create an entry 
+(term * type * abscontext * mincontext * path) 
+for each term in the return list 
+e.g: getSubTermList Abs(y, int, Const(f,int->int) $ Const(x,int) $ Bound(0))
+will give       [(Const(f,int->int),int->int,[int],[],[00]),
+               (Const(x,int),int,[int],[],[010]),
+               (Bound(0),int,[int],[int],[110]),
+               (Const(x,int) $ Bound(0),type,[int],[int],[10]),
+               (Const(f,int->int) $ Const(x,int) $ Bound(0),type,[int],[int],[0],
+               (Abs (y,int,Const(f,int->int) $ const(x,int) $ Bound(0)),type,[],[],[])]
+                *)
+
+fun getSubTermList (Const(name,t)) abscontext path acc =
+   (Const(name,t),t,abscontext,abscontext,path)::acc
+ | getSubTermList (Free(name,t)) abscontext path acc =
+   (Free(name,t),t,abscontext,abscontext,path)::acc
+ | getSubTermList (Var(indname,t)) abscontext path acc =
+   (Var(indname,t),t,abscontext,abscontext,path)::acc
+ | getSubTermList (Bound(i)) abscontext path acc =
+   (Bound(0),nth abscontext i,abscontext, Library.drop i abscontext,path)::acc
+ | getSubTermList (Abs(name,t,uTerm)) abscontext path acc = 
+   let 
+     val curTerm = Abs(name,t,uTerm)
+     val bnos = Term.add_loose_bnos (curTerm,0,[])
+     val minInd = if (bnos = []) then 0 
+       else Library.foldl (fn (n,m) => if (n<m) then n else m) (hd bnos,tl bnos)
+     val newTerm = rename_bnds curTerm minInd
+     val newContext = Library.drop minInd abscontext
+   in 
+     getSubTermList uTerm (t::abscontext) (0::path) 
+               ((newTerm,(fastype_of1 (abscontext, curTerm)),abscontext,newContext,path)::acc)
+   end
+ | getSubTermList (fstUTerm $ sndUTerm) abscontext path acc = 
+   let 
+     val curTerm = (fstUTerm $ sndUTerm)
+     val bnos = Term.add_loose_bnos (curTerm, 0, [])
+     val minInd = if (bnos = []) then 0
+       else Library.foldl (fn (n,m) => if (n<m) then n else m) (hd bnos,tl bnos)
+     val newTerm = rename_bnds curTerm minInd
+     val newContext = Library.drop minInd abscontext
+   in 
+     getSubTermList fstUTerm abscontext (0::path) 
+       (getSubTermList sndUTerm abscontext (1::path) 
+         ((newTerm,(fastype_of1 (abscontext, curTerm)),abscontext,newContext,path)::acc)) 
+   end;  
+
+
+
+
+
+(*tests if the given element ist in the given list*)
+
+fun in_list elem [] = false
+ | in_list elem (x::xs) = if (elem = x) then true else in_list elem xs;
+
+
+(*Evaluate if the longContext is more special as the shortContext. 
+If so, a term with shortContext can be substituted in the place of a 
+term with longContext*)
+
+fun is_morespecial longContext shortContext = 
+ let 
+   val revlC = rev longContext
+   val revsC = rev shortContext
+   fun is_prefix [] longList = true
+     | is_prefix shList [] = false
+     | is_prefix (x::xs) (y::ys) = if (x=y) then is_prefix xs ys else false
+ in 
+   is_prefix revsC revlC
+ end;
+
+
+(*takes a (term * type * context * context * path)-tupel and searches in the specified list for 
+terms with the same type and appropriate context. Returns a (term * path) list of these terms.
+Used in order to generate a list of type-equal subterms of the original term*)
+
+fun searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) [] resultList = 
+   resultList
+ | searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) 
+   ((hdterm,hdtype,hdabsContext,hdminContext,hdpath)::xs) resultList = 
+   if ((stype = hdtype) andalso (is_morespecial sabsContext hdminContext) 
+     andalso (is_morespecial hdabsContext sminContext)) 
+   then searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) xs 
+     ((hdterm,hdabsContext,hdminContext,hdpath)::resultList) 
+   else searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) xs resultList;
+
+
+(*evaluates if the given function is in the passed list of forbidden functions*)
+
+fun in_list_forb consSig (consNameStr,consType) [] = false
+ | in_list_forb consSig (consNameStr,consType) ((forbNameStr,forbTypeStr)::xs) = 
+   let 
+     val forbType = Syntax.read_typ_global consSig forbTypeStr
+     val typeSignature = #tsig (Sign.rep_sg consSig)
+   in
+     if ((consNameStr = forbNameStr) 
+       andalso (Type.typ_instance typeSignature (consType,(Logic.varifyT forbType))))
+     then true
+     else in_list_forb consSig (consNameStr,consType) xs
+   end;
+
+
+
+(*searches in the given signature Consts with the same type as sterm and 
+returns a list of those terms*)
+
+fun searchForSignatureMutations (sterm,stype) consSig forbidden_funs = 
+ let 
+   val sigConsTypeList = consts_of consSig;
+   val typeSignature = #tsig (Sign.rep_sg consSig)
+ in 
+   let 
+     fun recursiveSearch mutatableTermList [] = mutatableTermList
+       | recursiveSearch mutatableTermList ((ConsName,ConsType)::xs) = 
+         if (Type.typ_instance typeSignature (stype,ConsType) 
+           andalso (not (sterm = Const(ConsName,stype))) 
+           andalso (not (in_list_forb consSig (ConsName,ConsType) forbidden_funs))) 
+         then recursiveSearch ((Term.Const(ConsName,stype), [], [], [5])::mutatableTermList) xs
+         else recursiveSearch mutatableTermList xs
+     in
+       recursiveSearch [] sigConsTypeList
+     end
+   end;     
+
+
+(*generates a list of terms that can be used instead of the passed subterm in the original term. These terms either have
+the same type and appropriate context and are generated from the list of subterms either - in case of a Const-term they have been found
+in the current signature.
+This function has 3 versions:
+0: no instertion of signature functions, 
+  only terms in the subTermList with the same type and appropriate context as the passed term are returned
+1: no exchange of subterms,
+  only signature functions are inserted at the place of type-aequivalent Conses
+2: mixture of the two other versions. insertion of signature functions and exchange of subterms*)
+
+fun searchForMutatableTerm 0 (sterm,stype,sabscontext,smincontext,spath) 
+   subTerms consSig resultList forbidden_funs =
+   searchForMutatableSubTerm (sterm,stype,sabscontext,smincontext,spath) subTerms resultList
+ | searchForMutatableTerm 1 (Const(constName,constType),stype,sabscontext,smincontext,spath) 
+   subTerms consSig resultList forbidden_funs = 
+   searchForSignatureMutations (Const(constName,constType),stype) consSig forbidden_funs
+ | searchForMutatableTerm 1 _ _ _ _ _ = []
+ | searchForMutatableTerm 2 (Const(constName,constType),stype,sabscontext,smincontext,spath) 
+   subTerms consSig resultList forbidden_funs = 
+     let 
+       val subtermMutations = searchForMutatableSubTerm 
+         (Const(constName,constType),stype,sabscontext,smincontext,spath) subTerms resultList
+       val signatureMutations = searchForSignatureMutations 
+         (Const(constName,constType),stype) consSig forbidden_funs
+     in
+       subtermMutations@signatureMutations
+     end
+ | searchForMutatableTerm 2 (sterm,stype,sabscontext,smincontext,spath) 
+   subTerms consSig resultList forbidden_funs =
+   searchForMutatableSubTerm (sterm,stype,sabscontext,smincontext,spath) subTerms resultList
+ | searchForMutatableTerm i _ _ _ _ _ = 
+   raise WrongArg("Version " ^ string_of_int i ^ 
+     " doesn't exist for function searchForMutatableTerm!") ;
+
+
+
+
+(*evaluates if the two terms with paths passed as arguments can be exchanged, i.e. evaluates if one of the terms is a subterm of the other one*)  
+
+fun areReplacable [] [] = false
+ | areReplacable fstPath [] = false
+ | areReplacable [] sndPath = false
+ | areReplacable (x::xs) (y::ys) = if (x=y) then areReplacable xs ys else true; 
+
+
+
+
+(*substitutes the term at the position of the first list in fstTerm by sndTerm. 
+The lists represent paths as generated by createSubTermList*)
+
+fun substitute [] fstTerm sndTerm = sndTerm
+ | substitute (_::xs) (Abs(s,T,subTerm)) sndTerm = Abs(s,T,(substitute xs subTerm sndTerm))
+ | substitute (0::xs) (t $ u) sndTerm = substitute xs t sndTerm $ u 
+ | substitute (1::xs) (t $ u) sndTerm = t $ substitute xs u sndTerm
+ | substitute (_::xs) _ sndTerm = 
+   raise WrongPath ("The Term could not be found at the specified position"); 
+
+
+(*get the subterm with the specified path in myTerm*)
+
+fun getSubTerm myTerm [] = myTerm
+ | getSubTerm (Abs(s,T,subTerm)) (0::xs) = getSubTerm subTerm xs
+ | getSubTerm (t $ u) (0::xs) = getSubTerm t xs
+ | getSubTerm (t $ u) (1::xs) = getSubTerm u xs
+ | getSubTerm _ (_::xs) = 
+   raise WrongPath ("The subterm could not be found at the specified position");
+
+
+(*exchanges two subterms with the given paths in the original Term*)
+
+fun replace origTerm (fstTerm, fstPath) (sndTerm, sndPath) = 
+ if (areReplacable (rev fstPath) (rev sndPath))
+ then substitute (rev sndPath) (substitute (rev fstPath) origTerm sndTerm) fstTerm
+ else origTerm; 
+
+
+
+
+(*tests if the terms with the given pathes in the origTerm are commutative
+respecting the list of commutative operators (commutatives)*)
+
+fun areCommutative origTerm fstPath sndPath commutatives =
+ if (sndPath = []) 
+ then false
+ else
+   let 
+     val base = (tl sndPath)
+   in
+     let 
+       val fstcomm = 1::0::base
+       val opcomm = 0::0::base
+     in
+       if ((fstPath = fstcomm) andalso (is_Const (getSubTerm origTerm (rev opcomm))))
+       then
+         let 
+           val Const(name,_) = (getSubTerm origTerm (rev opcomm))
+         in
+           if (in_list name commutatives) 
+           then true 
+           else false
+         end
+       else false
+     end
+   end;
+
+
+(*Canonizes term t with the commutative operators stored in list 
+commutatives*)
+
+fun canonize_term (Const (s, T) $ t $ u) comms =
+ let
+   val t' = canonize_term t comms;
+   val u' = canonize_term u comms;
+ in 
+   if s mem comms andalso TermOrd.termless (u', t')
+   then Const (s, T) $ u' $ t'
+   else Const (s, T) $ t' $ u'
+ end
+ | canonize_term (t $ u) comms = canonize_term t comms $ canonize_term u comms
+ | canonize_term (Abs (s, T, t)) comms = Abs (s, T, canonize_term t comms)
+ | canonize_term t comms = t;
+
+
+(*inspect the passed list and mutate origTerm following the elements of the list:
+if the path of the current element is [5] (dummy path), the term has been found in the signature 
+and the subterm will be substituted by it
+else the term has been found in the original term and the two subterms have to be exchanged
+The additional parameter commutatives indicates the commutative operators  
+in the term whose operands won't be exchanged*)
+
+fun createMutatedTerms origTerm _ [] commutatives mutatedTerms = mutatedTerms
+ | createMutatedTerms origTerm (hdt as (hdTerm,hdabsContext,hdminContext,hdPath))
+   ((sndTerm,sndabsContext,sndminContext,sndPath)::xs) commutatives mutatedTerms = 
+   if (sndPath = [5])
+   then
+     let 
+         val canonized = canonize_term (substitute (rev hdPath) origTerm sndTerm) commutatives
+       in
+         if (canonized = origTerm)  
+         then createMutatedTerms origTerm hdt xs commutatives mutatedTerms
+         else createMutatedTerms origTerm hdt xs commutatives 
+           (insert op aconv canonized mutatedTerms)
+       end
+     else 
+       if ((areCommutative origTerm hdPath sndPath commutatives)
+         orelse (areCommutative origTerm sndPath hdPath commutatives)) 
+       then createMutatedTerms origTerm hdt xs commutatives mutatedTerms
+       else
+         let 
+           val canonized = canonize_term 
+             (replace origTerm
+                (incr_boundvars (length sndabsContext - length hdminContext) hdTerm,
+                 hdPath)
+                (incr_boundvars (length hdabsContext - length sndminContext) sndTerm,
+                 sndPath)) commutatives
+         in
+           if (not(canonized = origTerm)) 
+           then createMutatedTerms origTerm hdt xs commutatives 
+             (insert op aconv canonized mutatedTerms)
+           else createMutatedTerms origTerm hdt xs commutatives mutatedTerms
+         end;
+
+
+
+(*mutates origTerm by exchanging subterms. The mutated terms are returned in a term list
+The parameter commutatives consists of a list of commutative operators. The permutation of their 
+operands won't be considered as a new term
+!!!Attention!!!: The given origTerm must be canonized. Use function canonize_term!*)
+
+fun mutate_once option origTerm tsig commutatives forbidden_funs= 
+ let 
+   val subTermList = getSubTermList origTerm [] [] []
+ in
+   let 
+     fun replaceRecursively [] mutatedTerms = mutatedTerms
+       | replaceRecursively ((hdTerm,hdType,hdabsContext,hdminContext,hdPath)::tail) 
+         mutatedTerms =
+         replaceRecursively tail (union op aconv (createMutatedTerms origTerm 
+           (hdTerm,hdabsContext,hdminContext,hdPath) 
+           (searchForMutatableTerm option (hdTerm,hdType,hdabsContext,hdminContext,hdPath) 
+             tail tsig [] forbidden_funs) 
+           commutatives []) mutatedTerms)
+   in
+     replaceRecursively subTermList []
+   end
+ end;
+
+
+
+
+(*helper function in order to apply recursively the mutate_once function on a whole list of terms
+Needed for the mutate function*)
+
+fun mutate_once_rec option [] tsig commutatives forbidden_funs acc = acc
+ | mutate_once_rec option (x::xs) tsig commutatives forbidden_funs acc = 
+   mutate_once_rec option xs tsig commutatives forbidden_funs 
+     (union op aconv (mutate_once option x tsig commutatives forbidden_funs) acc);
+
+
+
+(*apply function mutate_once iter times on the given origTerm. *)
+(*call of mutiere with canonized form of origTerm. Prevents us of the computation of
+canonization in the course of insertion of new terms!*)
+
+fun mutate option origTerm tsig commutatives forbidden_funs 0 = []
+ | mutate option origTerm tsig commutatives forbidden_funs 1 = 
+   mutate_once option (canonize_term origTerm commutatives) tsig commutatives forbidden_funs
+ | mutate option origTerm tsig commutatives forbidden_funs iter = 
+   mutate_once_rec option (mutate option origTerm tsig commutatives forbidden_funs (iter-1)) 
+     tsig commutatives forbidden_funs []; 
+
+(*mutate origTerm iter times by only exchanging subterms*)
+
+fun mutate_exc origTerm commutatives iter =
+ mutate 0 origTerm (theory "Main") commutatives [] iter;
+
+
+(*mutate origTerm iter times by only inserting signature functions*)
+
+fun mutate_sign origTerm tsig forbidden_funs iter = 
+ mutate 1 origTerm tsig [] forbidden_funs iter;
+
+
+(*mutate origTerm iter times by exchange of subterms and insertion of subterms*)
+
+fun mutate_mix origTerm tsig commutatives forbidden_funs iter =
+ mutate 2 origTerm tsig commutatives forbidden_funs iter;  
+
+
+(*helper function in order to prettily print a list of terms*)
+
+fun pretty xs = map (fn (id, t) => (id, (HOLogic.mk_number HOLogic.natT
+ (HOLogic.dest_nat t)) handle TERM _ => t)) xs;
+
+
+(*helper function for the quickcheck invocation. Evaluates the quickcheck_term function on a whole list of terms
+and tries to print the exceptions*)
+
+fun freeze (t $ u) = freeze t $ freeze u
+ | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
+ | freeze (Var ((a, i), T)) =
+     Free (if i = 0 then a else a ^ "_" ^ string_of_int i, T)
+ | freeze t = t;
+
+fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
+ | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T);
+
+fun preprocess thy insts t = ObjectLogic.atomize_term thy
+ (map_types (inst_type insts) (freeze t));
+
+fun is_executable thy insts th =
+ (Quickcheck.test_term
+    (ProofContext.init thy) false (SOME (!testgen_name)) 1 1 (preprocess thy insts (prop_of th));
+  priority "executable"; true) handle ERROR s =>
+    (priority ("not executable: " ^ s); false);
+
+fun qc_recursive usedthy [] insts sz qciter acc = rev acc
+ | qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter 
+     (priority ("qc_recursive: " ^ string_of_int (length xs)); ((x, pretty (the_default [] (Quickcheck.test_term
+       (ProofContext.init usedthy) false (SOME (!testgen_name)) sz qciter (store (preprocess usedthy insts x))))) :: acc))
+          handle ERROR msg => (priority msg; qc_recursive usedthy xs insts sz qciter acc);
+
+
+(*quickcheck-test the mutants created by function mutate with type-instantiation insts, 
+quickcheck-theory usedthy and qciter quickcheck-iterations *)
+
+fun qc_test mutated insts usedthy sz qciter = 
+ let 
+   val checked = map (apsnd (map (apsnd (cterm_of usedthy))))
+     (qc_recursive usedthy mutated insts sz qciter []);
+   fun combine (passednum,passed) (cenum,ces) [] = (passednum,passed,cenum,ces)
+     | combine (passednum,passed) (cenum,ces) ((t, []) :: xs) =
+       combine (passednum+1,(cterm_of usedthy t)::passed) (cenum,ces) xs
+     | combine (passednum,passed) (cenum,ces) ((t, x) :: xs) =
+       combine (passednum,passed) 
+         (cenum+1,(cterm_of usedthy t, x) :: ces) xs
+ in
+   combine (0,[]) (0,[]) checked
+ end;
+
+
+(*create a string of a list of terms*)
+
+fun string_of_ctermlist thy [] acc = acc
+ | string_of_ctermlist thy (x::xs) acc = 
+   string_of_ctermlist thy xs ((Syntax.string_of_term_global thy (term_of x)) ^ "\n" ^ acc);
+
+(*helper function in order to decompose the counter examples generated by quickcheck*)
+
+fun decompose_ce thy [] acc = acc
+ | decompose_ce thy ((varname,varce)::xs) acc = 
+   decompose_ce thy xs ("\t" ^ varname ^ " instanciated to " ^ 
+     (Syntax.string_of_term_global thy (term_of varce)) ^ "\n" ^ acc);
+
+(*helper function in order to decompose a list of counter examples*)
+
+fun decompose_celist thy [] acc = acc
+ | decompose_celist thy ((mutTerm,varcelist)::xs) acc = decompose_celist thy xs 
+   ("mutated term : " ^ 
+   (Syntax.string_of_term_global thy (term_of mutTerm)) ^ "\n" ^ 
+   "counterexample : \n" ^ 
+   (decompose_ce thy (rev varcelist) "") ^ acc); 
+
+
+(*quickcheck test the list of mutants mutated by applying the type instantiations 
+insts and using the quickcheck-theory usedthy. The results of quickcheck are stored
+in the file with name filename. If app is true, the output will be appended to the file. 
+Else it will be overwritten. *)
+
+fun qc_test_file app mutated insts usedthy sz qciter filename =
+ let 
+   val statisticList = qc_test mutated insts usedthy sz qciter
+   val passed = (string_of_int (#1 statisticList)) ^ 
+     " terms passed the quickchecktest: \n\n" ^ 
+     (string_of_ctermlist usedthy (rev (#2 statisticList)) "") 
+   val counterexps = (string_of_int (#3 statisticList)) ^ 
+     " terms produced a counterexample: \n\n" ^
+     decompose_celist usedthy (rev (#4 statisticList)) "" 
+ in
+   if (app = false) 
+   then File.write (Path.explode filename) (passed ^ "\n\n" ^ counterexps)
+   else File.append (Path.explode filename) (passed ^ "\n\n" ^ counterexps)
+ end;
+
+
+(*mutate sourceThm with the mutate-version given in option and check the resulting mutants. 
+The output will be written to the file with name filename*)
+
+fun mutqc_file option usedthy commutatives forbidden_funs iter sourceThm insts sz qciter filename =
+ let 
+   val mutated = mutate option (prop_of sourceThm) 
+     usedthy commutatives forbidden_funs iter 
+ in
+   qc_test_file false mutated insts usedthy sz qciter filename 
+ end;
+
+(*exchange version of function mutqc_file*)
+
+fun mutqc_file_exc usedthy commutatives iter sourceThm insts sz qciter filename =
+ mutqc_file 0 usedthy commutatives [] iter sourceThm insts sz qciter filename;
+
+
+(*sinature version of function mutqc_file*)
+fun mutqc_file_sign usedthy forbidden_funs iter sourceThm insts sz qciter filename= 
+ mutqc_file 1 usedthy [] forbidden_funs iter sourceThm insts sz qciter filename;
+
+(*mixed version of function mutqc_file*)
+
+fun mutqc_file_mix usedthy commutatives forbidden_funs iter sourceThm insts sz qciter filename =
+ mutqc_file 2 usedthy commutatives forbidden_funs iter sourceThm insts sz qciter filename;
+
+
+
+(*apply function mutqc_file on a list of theorems. The output for each theorem 
+will be stored in a seperated file whose filename must be indicated in a list*)
+
+fun mutqc_file_rec option usedthy commutatives forbFuns iter [] insts sz qciter _ = ()
+ | mutqc_file_rec option usedthy commutatives forbFuns iter  sourceThms insts sz qciter [] = 
+   raise WrongArg ("Not enough files for the output of qc_test_file_rec!")
+ | mutqc_file_rec option usedthy commutatives forbFuns iter (x::xs) insts sz qciter (y::ys) = 
+   (mutqc_file option usedthy commutatives forbFuns iter x insts sz qciter y ; 
+   mutqc_file_rec option usedthy commutatives forbFuns iter xs insts sz qciter ys);
+
+
+(*exchange version of function mutqc_file_rec*)
+
+fun mutqc_file_rec_exc usedthy commutatives iter sourceThms insts sz qciter files =
+ mutqc_file_rec 0 usedthy commutatives [] iter sourceThms insts sz qciter files;
+
+(*signature version of function mutqc_file_rec*)
+
+fun mutqc_file_rec_sign usedthy forbidden_funs iter sourceThms insts sz qciter files =
+ mutqc_file_rec 1 usedthy [] forbidden_funs iter sourceThms insts sz qciter files;
+
+(*mixed version of function mutqc_file_rec*)
+
+fun mutqc_file_rec_mix usedthy commutatives forbidden_funs iter sourceThms insts sz qciter files =
+ mutqc_file_rec 2 usedthy commutatives forbidden_funs iter sourceThms insts sz qciter files;
+
+(*create the appropriate number of spaces in order to properly print a table*)
+
+fun create_spaces entry spacenum =
+ let 
+		val diff = spacenum - (size entry)
+ in 
+		if (diff > 0) 
+   then implode (replicate diff " ")
+   else ""
+ end;
+
+
+(*create a statistic of the output of a quickcheck test on the passed thmlist*)
+
+fun mutqc_file_stat option usedthy commutatives forbidden_funs iter thmlist insts sz qciter filename = 
+ let 
+   fun mutthmrec [] = ()
+   |   mutthmrec (x::xs) =
+     let 
+       val mutated = mutate option (prop_of x) usedthy
+         commutatives forbidden_funs iter
+       val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter
+       val thmname =  "\ntheorem " ^ (Thm.get_name x) ^ ":"
+       val pnumstring = string_of_int passednum
+       val cenumstring = string_of_int cenum
+     in
+       (File.append (Path.explode filename) 
+         (thmname ^ (create_spaces thmname 50) ^ 
+         pnumstring ^ (create_spaces pnumstring 20) ^ 
+         cenumstring ^ (create_spaces cenumstring 20) ^ "\n");
+       mutthmrec xs)
+     end;
+ in 
+   (File.write (Path.explode filename) 
+     ("\n\ntheorem name" ^ (create_spaces "theorem name" 50) ^ 
+     "passed mutants"  ^ (create_spaces "passed mutants" 20) ^ 
+     "counter examples\n\n" );
+   mutthmrec thmlist)
+ end;
+
+(*signature version of function mutqc_file_stat*)
+
+fun mutqc_file_stat_sign usedthy forbidden_funs iter thmlist insts sz qciter filename =
+ mutqc_file_stat 1 usedthy [] forbidden_funs iter thmlist insts sz qciter filename;
+
+(*exchange version of function mutqc_file_stat*)
+
+fun mutqc_file_stat_exc usedthy commutatives iter thmlist insts sz qciter filename =
+ mutqc_file_stat 0 usedthy commutatives [] iter thmlist insts sz qciter filename;
+
+(*mixed version of function mutqc_file_stat*)
+
+fun mutqc_file_stat_mix usedthy commutatives forbidden_funs iter thmlist insts sz qciter filename =
+ mutqc_file_stat 2 usedthy commutatives forbidden_funs iter thmlist insts sz qciter filename;
+
+(*mutate and quickcheck-test all the theorems contained in the passed theory. 
+The output will be stored in a single file*)
+
+fun mutqc_thy option mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
+ let
+   val thmlist = filter (is_executable mutthy insts o snd) (thms_of mutthy);
+   fun mutthmrec [] = ()
+     | mutthmrec ((name,thm)::xs) = 
+         let
+           val mutated = mutate option (prop_of thm) 
+             usedthy commutatives forbidden_funs iter
+         in
+           (File.append (Path.explode filename) 
+             ("--------------------------\n\nQuickchecktest of theorem " ^ name ^ ":\n\n");
+           qc_test_file true mutated insts usedthy sz qciter filename;
+           mutthmrec xs)
+         end;
+   in 
+     mutthmrec thmlist
+   end;
+
+(*exchange version of function mutqc_thy*)
+
+fun mutqc_thy_exc mutthy usedthy commutatives iter insts sz qciter filename =
+ mutqc_thy 0 mutthy usedthy commutatives [] iter insts sz qciter filename;
+
+(*signature version of function mutqc_thy*)
+
+fun mutqc_thy_sign mutthy usedthy forbidden_funs iter insts sz qciter filename =
+ mutqc_thy 1 mutthy usedthy [] forbidden_funs iter insts sz qciter filename;
+
+(*mixed version of function mutqc_thy*)
+
+fun mutqc_thy_mix mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
+ mutqc_thy 2 mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename;
+
+(*create a statistic representation of the call of function mutqc_thy*)
+
+fun mutqc_thystat option p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
+ let
+   val thmlist = filter
+     (fn (s, th) => not (p s th) andalso (priority s; is_executable mutthy insts th)) (thms_of mutthy)
+   fun mutthmrec [] = ()
+   |   mutthmrec ((name,thm)::xs) =
+     let          
+       val _ = priority ("mutthmrec: " ^ name);
+       val mutated = mutate option (prop_of thm) usedthy
+           commutatives forbidden_funs iter
+       val _ = (bar := mutated);
+       val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter
+       val thmname =  "\ntheorem " ^ name ^ ":"
+       val pnumstring = string_of_int passednum
+       val cenumstring = string_of_int cenum
+     in
+       (File.append (Path.explode filename) 
+         (thmname ^ (create_spaces thmname 50) ^ 
+         pnumstring ^ (create_spaces pnumstring 20) ^ 
+         cenumstring ^ (create_spaces cenumstring 20) ^ "\n");
+       mutthmrec xs)
+     end;
+ in 
+   (File.write (Path.explode filename) ("Result of the quickcheck-test of theory " ^
+     ":\n\ntheorem name" ^ (create_spaces "theorem name" 50) ^ 
+     "passed mutants"  ^ (create_spaces "passed mutants" 20) ^ 
+     "counter examples\n\n" );
+   mutthmrec thmlist)
+ end;
+
+(*exchange version of function mutqc_thystat*)
+			
+fun mutqc_thystat_exc p mutthy usedthy commutatives iter insts sz qciter filename =
+ mutqc_thystat 0 p mutthy usedthy commutatives [] iter insts sz qciter filename;
+
+(*signature version of function mutqc_thystat*)
+
+fun mutqc_thystat_sign p mutthy usedthy forbidden_funs iter insts sz qciter filename =
+ mutqc_thystat 1 p mutthy usedthy [] forbidden_funs iter insts sz qciter filename;
+
+(*mixed version of function mutqc_thystat*)
+
+fun mutqc_thystat_mix p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
+ mutqc_thystat 2 p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename;
+
+end
diff -r 366a1a44aac2 -r 3b4762c1052c src/HOL/Mutabelle/mutabelle_extra.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Jan 25 16:19:42 2010 +0100
@@ -0,0 +1,376 @@
+(*
+    Title:      HOL/Mutabelle/mutabelle_extra.ML
+    Author:     Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen
+
+    Invokation of Counterexample generators
+*)
+signature MUTABELLE_EXTRA =
+sig
+
+val take_random : int -> 'a list -> 'a list
+
+datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
+type mtd = string * (theory -> term -> outcome)
+
+type mutant_subentry = term * (string * outcome) list
+type detailed_entry = string * bool * term * mutant_subentry list
+
+type subentry = string * int * int * int * int * int * int
+type entry = string * bool * subentry list
+type report = entry list
+
+val quickcheck_mtd : string -> mtd
+(*
+val refute_mtd : mtd
+val nitpick_mtd : mtd
+*)
+
+val freezeT : term -> term
+val thms_of : bool -> theory -> thm list
+
+val string_for_report : report -> string
+val write_report : string -> report -> unit
+val mutate_theorems_and_write_report :
+  theory -> mtd list -> thm list -> string -> unit
+
+val random_seed : real Unsynchronized.ref
+end;
+
+structure MutabelleExtra : MUTABELLE_EXTRA =
+struct
+
+(* Own seed; can't rely on the Isabelle one to stay the same *)
+val random_seed = Unsynchronized.ref 1.0;
+
+
+(* mutation options *)
+val max_mutants = 4
+val num_mutations = 1
+(* soundness check: *)
+val max_mutants = 1
+val num_mutations = 0
+
+(* quickcheck options *)
+(*val quickcheck_generator = "SML"*)
+val iterations = 100
+val size = 5
+
+exception RANDOM;
+
+fun rmod x y = x - y * Real.realFloor (x / y);
+
+local
+  val a = 16807.0;
+  val m = 2147483647.0;
+in
+
+fun random () = CRITICAL (fn () =>
+  let val r = rmod (a * ! random_seed) m
+  in (random_seed := r; r) end);
+
+end;
+
+fun random_range l h =
+  if h < l orelse l < 0 then raise RANDOM
+  else l + Real.floor (rmod (random ()) (real (h - l + 1)));
+
+datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
+type mtd = string * (theory -> term -> outcome)
+
+type mutant_subentry = term * (string * outcome) list
+type detailed_entry = string * bool * term * mutant_subentry list
+
+
+type subentry = string * int * int * int * int * int * int
+type entry = string * bool * subentry list
+type report = entry list
+
+fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
+  | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T)
+
+fun preprocess thy insts t = ObjectLogic.atomize_term thy
+ (map_types (inst_type insts) (Mutabelle.freeze t));
+
+fun invoke_quickcheck quickcheck_generator thy t =
+  TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit))
+      (fn _ =>
+          case Quickcheck.test_term (ProofContext.init thy) false (SOME quickcheck_generator)
+                                    size iterations (preprocess thy [] t) of
+            NONE => NoCex
+          | SOME _ => GenuineCex) ()
+  handle TimeLimit.TimeOut => Timeout
+
+fun quickcheck_mtd quickcheck_generator =
+  ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck quickcheck_generator)
+
+  (*
+fun invoke_refute thy t =
+  let
+    val res = MyRefute.refute_term thy [] t
+    val _ = priority ("Refute: " ^ res)
+  in
+    case res of
+      "genuine" => GenuineCex
+    | "likely_genuine" => GenuineCex
+    | "potential" => PotentialCex
+    | "none" => NoCex
+    | "unknown" => Donno
+    | _ => Error
+  end
+  handle MyRefute.REFUTE (loc, details) =>
+         (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
+                   "."))
+val refute_mtd = ("refute", invoke_refute)
+*)
+
+(*
+open Nitpick_Util
+open Nitpick_Rep
+open Nitpick_Nut
+
+fun invoke_nitpick thy t =
+  let
+    val ctxt = ProofContext.init thy
+    val state = Proof.init ctxt
+  in
+    let
+      val (res, _) = Nitpick.pick_nits_in_term state (Nitpick_Isar.default_params thy []) false [] t
+      val _ = priority ("Nitpick: " ^ res)
+    in
+      case res of
+        "genuine" => GenuineCex
+      | "likely_genuine" => GenuineCex
+      | "potential" => PotentialCex
+      | "none" => NoCex
+      | "unknown" => Donno
+      | _ => Error
+    end
+    handle ARG (loc, details) =>
+           (error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ "."))
+         | BAD (loc, details) =>
+           (error ("Internal error (" ^ quote loc ^ "): " ^ details ^ "."))
+         | LIMIT (_, details) =>
+           (warning ("Limit reached: " ^ details ^ "."); Donno)
+         | NOT_SUPPORTED details =>
+           (warning ("Unsupported case: " ^ details ^ "."); Donno)
+         | NUT (loc, us) =>
+           (error ("Invalid nut" ^ plural_s_for_list us ^
+                   " (" ^ quote loc ^ "): " ^
+                  commas (map (string_for_nut ctxt) us) ^ "."))
+         | REP (loc, Rs) =>
+           (error ("Invalid representation" ^ plural_s_for_list Rs ^
+                   " (" ^ quote loc ^ "): " ^
+                   commas (map string_for_rep Rs) ^ "."))
+         | TERM (loc, ts) =>
+           (error ("Invalid term" ^ plural_s_for_list ts ^
+                   " (" ^ quote loc ^ "): " ^
+                   commas (map (Syntax.string_of_term ctxt) ts) ^ "."))
+         | TYPE (loc, Ts, ts) =>
+           (error ("Invalid type" ^ plural_s_for_list Ts ^
+                   (if null ts then
+                      ""
+                    else
+                      " for term" ^ plural_s_for_list ts ^ " " ^
+                      commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
+                   " (" ^ quote loc ^ "): " ^
+                   commas (map (Syntax.string_of_typ ctxt) Ts) ^ "."))
+         | Kodkod.SYNTAX (_, details) =>
+           (warning ("Ill-formed Kodkodi output: " ^ details ^ "."); Error)
+         | Refute.REFUTE (loc, details) =>
+           (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
+                   "."))
+         | Exn.Interrupt => raise Exn.Interrupt
+         | _ => (priority ("Unknown error in Nitpick"); Error)
+  end
+val nitpick_mtd = ("nitpick", invoke_nitpick)
+*)
+
+val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}]
+
+val forbidden =
+ [(* (@{const_name "power"}, "'a"), *)
+  ("HOL.induct_equal", "'a"),
+  ("HOL.induct_implies", "'a"),
+  ("HOL.induct_conj", "'a"),
+  (@{const_name "undefined"}, "'a"),
+  (@{const_name "default"}, "'a"),
+  (@{const_name "dummy_pattern"}, "'a::{}") (*,
+  (@{const_name "uminus"}, "'a"),
+  (@{const_name "Nat.size"}, "'a"),
+  (@{const_name "HOL.abs"}, "'a") *)]
+
+val forbidden_thms =
+ ["finite_intvl_succ_class",
+  "nibble"]
+
+val forbidden_consts =
+ [@{const_name nibble_pair_of_char}]
+
+fun is_forbidden_theorem (s, th) =
+  let val consts = Term.add_const_names (prop_of th) [] in
+    exists (fn s' => s' mem space_explode "." s) forbidden_thms orelse
+    exists (fn s' => s' mem forbidden_consts) consts orelse
+    length (space_explode "." s) <> 2 orelse
+    String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse
+    String.isSuffix "_def" s orelse
+    String.isSuffix "_raw" s
+  end
+
+fun is_forbidden_mutant t =
+  let val consts = Term.add_const_names t [] in
+    exists (String.isPrefix "Nitpick") consts orelse
+    exists (String.isSubstring "_sumC") consts (* internal function *)
+  end
+
+fun is_executable_term thy t = can (TimeLimit.timeLimit (Time.fromMilliseconds 2000) (Quickcheck.test_term
+ (ProofContext.init thy) false (SOME "SML") 1 0)) (preprocess thy [] t)
+fun is_executable_thm thy th = is_executable_term thy (prop_of th)
+
+val freezeT =
+  map_types (map_type_tvar (fn ((a, i), S) =>
+    TFree (if i = 0 then a else a ^ "_" ^ string_of_int i, S)))
+
+fun thms_of all thy =
+  filter
+    (fn th => (all orelse Context.theory_name (theory_of_thm th) = Context.theory_name thy)
+      (* andalso is_executable_thm thy th *))
+    (map snd (filter_out is_forbidden_theorem (Mutabelle.all_unconcealed_thms_of thy)))
+
+val count = length oo filter o equal
+
+fun take_random 0 _ = []
+  | take_random _ [] = []
+  | take_random n xs =
+    let val j = random_range 0 (length xs - 1) in
+      Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
+    end
+
+fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
+  let
+    val _ = priority ("Invoking " ^ mtd_name)
+    val res = case try (invoke_mtd thy) t of
+                SOME res => res
+              | NONE => (priority ("**** PROBLEMS WITH " ^
+                                 Syntax.string_of_term_global thy t); Error)
+    val _ = priority (" Done")
+  in res end
+
+(* theory -> term list -> mtd -> subentry *)
+fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
+  let
+     val res = map (safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
+  in
+    (mtd_name, count GenuineCex res, count PotentialCex res, count NoCex res,
+     count Donno res, count Timeout res, count Error res)
+  end
+
+fun create_entry thy thm exec mutants mtds =
+  (Thm.get_name thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
+
+fun create_detailed_entry thy thm exec mutants mtds =
+  let
+    fun create_mutant_subentry mutant = (mutant,
+      map (fn (mtd_name, invoke_mtd) =>
+        (mtd_name, safe_invoke_mtd thy (mtd_name, invoke_mtd) mutant)) mtds)
+  in
+    (Thm.get_name thm, exec, prop_of thm, map create_mutant_subentry mutants)
+  end
+
+(* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
+fun mutate_theorem create_entry thy mtds thm =
+  let
+    val pp = Syntax.pp_global thy
+    val exec = is_executable_thm thy thm
+    val _ = priority (if exec then "EXEC" else "NOEXEC")
+    val mutants =
+          (if num_mutations = 0 then
+             [Thm.prop_of thm]
+           else
+             Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden
+                                  num_mutations)
+             |> filter_out is_forbidden_mutant
+    val mutants =
+      if exec then
+        let
+          val _ = priority ("BEFORE PARTITION OF " ^
+                            Int.toString (length mutants) ^ " MUTANTS")
+          val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
+          val _ = tracing ("AFTER PARTITION (" ^ Int.toString (length execs) ^
+                           " vs " ^ Int.toString (length noexecs) ^ ")")
+        in
+          execs @ take_random (Int.max (0, max_mutants - length execs)) noexecs
+        end
+      else
+        mutants
+    val mutants = mutants
+          |> take_random max_mutants
+          |> map Mutabelle.freeze |> map freezeT
+(*          |> filter (not o is_forbidden_mutant) *)
+          |> List.mapPartial (try (Sign.cert_term thy))
+    val _ = map (fn t => priority ("MUTANT: " ^ Pretty.string_of (Pretty.term pp t))) mutants
+  in
+    create_entry thy thm exec mutants mtds
+  end
+
+(* theory -> mtd list -> thm list -> report *)
+val mutate_theorems = map ooo mutate_theorem
+
+fun string_of_outcome GenuineCex = "GenuineCex"
+  | string_of_outcome PotentialCex = "PotentialCex"
+  | string_of_outcome NoCex = "NoCex"
+  | string_of_outcome Donno = "Donno"
+  | string_of_outcome Timeout = "Timeout"
+  | string_of_outcome Error = "Error"
+
+fun string_of_mutant_subentry thy (t, results) =
+  "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
+  space_implode "; " (map (fn (mtd_name, outcome) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
+  "\n"
+
+fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = 
+   thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
+   Syntax.string_of_term_global thy t ^ "\n" ^
+   cat_lines (map (string_of_mutant_subentry thy) mutant_subentries) ^ "\n"
+
+(* subentry -> string *)
+fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno,
+                         timeout, error) =
+  "    " ^ mtd_name ^ ": " ^ Int.toString genuine_cex ^ "+ " ^
+  Int.toString potential_cex ^ "= " ^ Int.toString no_cex ^ "- " ^
+  Int.toString donno ^ "? " ^ Int.toString timeout ^ "T " ^
+  Int.toString error ^ "!"
+(* entry -> string *)
+fun string_for_entry (thm_name, exec, subentries) =
+  thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ":\n" ^
+  cat_lines (map string_for_subentry subentries) ^ "\n"
+(* report -> string *)
+fun string_for_report report = cat_lines (map string_for_entry report)
+
+(* string -> report -> unit *)
+fun write_report file_name =
+  File.write (Path.explode file_name) o string_for_report
+
+(* theory -> mtd list -> thm list -> string -> unit *)
+fun mutate_theorems_and_write_report thy mtds thms file_name =
+  let
+    val _ = priority "Starting Mutabelle..."
+    val path = Path.explode file_name
+    (* for normal report: *)
+    (*val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)*)
+    (*for detailled report: *)
+    val (gen_create_entry, gen_string_for_entry) =
+      (create_detailed_entry, string_of_detailed_entry thy)
+  in
+    File.write path (
+    "Mutation options = "  ^
+      "max_mutants: " ^ string_of_int max_mutants ^
+      "; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^
+    "QC options = " ^
+      (*"quickcheck_generator: " ^ quickcheck_generator ^ ";*)
+      "size: " ^ string_of_int size ^
+      "; iterations: " ^ string_of_int iterations ^ "\n");
+    map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms;
+    ()
+  end
+
+end;