src/HOL/Mutabelle/mutabelle.ML
author wenzelm
Sat Feb 27 23:13:01 2010 +0100 (2010-02-27)
changeset 35408 b48ab741683b
parent 34967 4b068e52ab3f
child 35625 9c818cab0dd0
permissions -rw-r--r--
modernized structure Term_Ord;
     1 (*
     2     Title:      HOL/Mutabelle/mutabelle.ML
     3     Author:     Veronika Ortner, TU Muenchen
     4 
     5     Mutation of theorems
     6 *)
     7 signature MUTABELLE =
     8 sig
     9  val testgen_name : string Unsynchronized.ref
    10  exception WrongPath of string;
    11  exception WrongArg of string;
    12  val freeze : term -> term
    13  val mutate_exc : term -> string list -> int -> term list 
    14  val mutate_sign : term -> theory -> (string * string) list -> int -> term list 
    15  val mutate_mix : term -> theory -> string list -> 
    16    (string * string) list -> int -> term list
    17  val qc_test : term list -> (typ * typ) list -> theory ->
    18   int -> int -> int * Thm.cterm list * int * (Thm.cterm * (string * Thm.cterm) list) list
    19  val qc_test_file : bool -> term list -> (typ * typ) list 
    20    -> theory -> int -> int -> string -> unit
    21  val mutqc_file_exc : theory -> string list ->
    22   int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit
    23  val mutqc_file_sign : theory -> (string * string) list ->
    24   int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit
    25  val mutqc_file_mix : theory -> string list -> (string * string) list ->
    26   int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit
    27  val mutqc_file_rec_exc : theory -> string list -> int ->
    28   Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit
    29  val mutqc_file_rec_sign : theory -> (string * string) list -> int ->
    30   Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit
    31  val mutqc_file_rec_mix : theory -> string list -> (string * string) list ->
    32   int -> Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit
    33  val mutqc_thy_exc : theory -> theory ->
    34   string list -> int -> (typ * typ) list -> int -> int -> string -> unit
    35  val mutqc_thy_sign : theory -> theory -> (string * string) list ->
    36   int -> (typ * typ) list -> int -> int -> string -> unit
    37  val mutqc_thy_mix : theory -> theory -> string list -> (string * string) list ->
    38   int -> (typ * typ) list -> int -> int -> string -> unit
    39  val mutqc_file_stat_sign : theory -> (string * string) list ->
    40   int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit
    41  val mutqc_file_stat_exc : theory -> string list ->
    42   int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit
    43  val mutqc_file_stat_mix : theory -> string list -> (string * string) list ->
    44   int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit
    45  val mutqc_thystat_exc : (string -> thm -> bool) -> theory -> theory ->
    46   string list -> int -> (typ * typ) list -> int -> int -> string -> unit
    47  val mutqc_thystat_sign : (string -> thm -> bool) -> theory -> theory -> (string * string) list ->
    48   int -> (typ * typ) list -> int -> int -> string -> unit
    49  val mutqc_thystat_mix : (string -> thm -> bool) -> theory -> theory -> string list -> 
    50   (string * string) list -> int -> (typ * typ) list -> int -> int -> string -> unit
    51  val canonize_term: term -> string list -> term
    52  
    53  val all_unconcealed_thms_of : theory -> (string * thm) list
    54 end;
    55 
    56 structure Mutabelle : MUTABELLE = 
    57 struct
    58 
    59 val testgen_name = Unsynchronized.ref "SML";
    60 
    61 fun all_unconcealed_thms_of thy =
    62   let
    63     val facts = PureThy.facts_of thy
    64   in
    65     Facts.fold_static
    66       (fn (s, ths) =>
    67         if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths))
    68       facts []
    69   end;
    70 
    71 fun thms_of thy = filter (fn (_, th) =>
    72    Context.theory_name (theory_of_thm th) = Context.theory_name thy) (all_unconcealed_thms_of thy);
    73 
    74 fun consts_of thy =
    75  let
    76    val (namespace, const_table) = #constants (Consts.dest (Sign.consts_of thy))
    77    val consts = Symtab.dest const_table
    78  in
    79    List.mapPartial (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
    80      (filter_out (fn (s, _) => Name_Space.is_concealed namespace s) consts)
    81  end;
    82 
    83 
    84 (*helper function in order to properly print a term*)
    85 
    86 fun prt x = Pretty.writeln (Syntax.pretty_term_global (theory "Main") x);
    87 
    88 
    89 (*possibility to print a given term for debugging purposes*)
    90 
    91 val debug = (Unsynchronized.ref false);
    92 fun debug_msg mutterm = if (!debug) then (prt mutterm) else ();
    93 
    94 
    95 (*thrown in case the specified path doesn't exist in the specified term*)
    96 
    97 exception WrongPath of string;
    98 
    99 
   100 (*thrown in case the arguments did not fit to the function*)
   101 
   102 exception WrongArg of string; 
   103 
   104 (*Rename the bound variables in a term with the minimal Index min of 
   105 bound variables. Variable (Bound(min)) will be renamed to Bound(0) etc. 
   106 This is needed in course auf evaluation of contexts.*)
   107 
   108 fun rename_bnds curTerm 0 = curTerm
   109  | rename_bnds (Bound(i)) minInd = 
   110    let 
   111      val erg = if (i-minInd < 0) then 0 else (i - minInd)
   112    in 
   113      Bound(erg)
   114    end
   115  | rename_bnds (Abs(name,t,uTerm)) minInd = 
   116    Abs(name,t,(rename_bnds uTerm minInd))
   117  | rename_bnds (fstUTerm $ sndUTerm) minInd =
   118    (rename_bnds fstUTerm minInd) $ (rename_bnds sndUTerm minInd)
   119  | rename_bnds elseTerm minInd = elseTerm;
   120 
   121 
   122 
   123 
   124 
   125 (*Partition a term in its subterms and create an entry 
   126 (term * type * abscontext * mincontext * path) 
   127 for each term in the return list 
   128 e.g: getSubTermList Abs(y, int, Const(f,int->int) $ Const(x,int) $ Bound(0))
   129 will give       [(Const(f,int->int),int->int,[int],[],[00]),
   130                (Const(x,int),int,[int],[],[010]),
   131                (Bound(0),int,[int],[int],[110]),
   132                (Const(x,int) $ Bound(0),type,[int],[int],[10]),
   133                (Const(f,int->int) $ Const(x,int) $ Bound(0),type,[int],[int],[0],
   134                (Abs (y,int,Const(f,int->int) $ const(x,int) $ Bound(0)),type,[],[],[])]
   135                 *)
   136 
   137 fun getSubTermList (Const(name,t)) abscontext path acc =
   138    (Const(name,t),t,abscontext,abscontext,path)::acc
   139  | getSubTermList (Free(name,t)) abscontext path acc =
   140    (Free(name,t),t,abscontext,abscontext,path)::acc
   141  | getSubTermList (Var(indname,t)) abscontext path acc =
   142    (Var(indname,t),t,abscontext,abscontext,path)::acc
   143  | getSubTermList (Bound(i)) abscontext path acc =
   144    (Bound(0),nth abscontext i,abscontext, Library.drop i abscontext,path)::acc
   145  | getSubTermList (Abs(name,t,uTerm)) abscontext path acc = 
   146    let 
   147      val curTerm = Abs(name,t,uTerm)
   148      val bnos = Term.add_loose_bnos (curTerm,0,[])
   149      val minInd = if (bnos = []) then 0 
   150        else Library.foldl (fn (n,m) => if (n<m) then n else m) (hd bnos,tl bnos)
   151      val newTerm = rename_bnds curTerm minInd
   152      val newContext = Library.drop minInd abscontext
   153    in 
   154      getSubTermList uTerm (t::abscontext) (0::path) 
   155                ((newTerm,(fastype_of1 (abscontext, curTerm)),abscontext,newContext,path)::acc)
   156    end
   157  | getSubTermList (fstUTerm $ sndUTerm) abscontext path acc = 
   158    let 
   159      val curTerm = (fstUTerm $ sndUTerm)
   160      val bnos = Term.add_loose_bnos (curTerm, 0, [])
   161      val minInd = if (bnos = []) then 0
   162        else Library.foldl (fn (n,m) => if (n<m) then n else m) (hd bnos,tl bnos)
   163      val newTerm = rename_bnds curTerm minInd
   164      val newContext = Library.drop minInd abscontext
   165    in 
   166      getSubTermList fstUTerm abscontext (0::path) 
   167        (getSubTermList sndUTerm abscontext (1::path) 
   168          ((newTerm,(fastype_of1 (abscontext, curTerm)),abscontext,newContext,path)::acc)) 
   169    end;  
   170 
   171 
   172 
   173 
   174 
   175 (*tests if the given element ist in the given list*)
   176 
   177 fun in_list elem [] = false
   178  | in_list elem (x::xs) = if (elem = x) then true else in_list elem xs;
   179 
   180 
   181 (*Evaluate if the longContext is more special as the shortContext. 
   182 If so, a term with shortContext can be substituted in the place of a 
   183 term with longContext*)
   184 
   185 fun is_morespecial longContext shortContext = 
   186  let 
   187    val revlC = rev longContext
   188    val revsC = rev shortContext
   189    fun is_prefix [] longList = true
   190      | is_prefix shList [] = false
   191      | is_prefix (x::xs) (y::ys) = if (x=y) then is_prefix xs ys else false
   192  in 
   193    is_prefix revsC revlC
   194  end;
   195 
   196 
   197 (*takes a (term * type * context * context * path)-tupel and searches in the specified list for 
   198 terms with the same type and appropriate context. Returns a (term * path) list of these terms.
   199 Used in order to generate a list of type-equal subterms of the original term*)
   200 
   201 fun searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) [] resultList = 
   202    resultList
   203  | searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) 
   204    ((hdterm,hdtype,hdabsContext,hdminContext,hdpath)::xs) resultList = 
   205    if ((stype = hdtype) andalso (is_morespecial sabsContext hdminContext) 
   206      andalso (is_morespecial hdabsContext sminContext)) 
   207    then searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) xs 
   208      ((hdterm,hdabsContext,hdminContext,hdpath)::resultList) 
   209    else searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) xs resultList;
   210 
   211 
   212 (*evaluates if the given function is in the passed list of forbidden functions*)
   213 
   214 fun in_list_forb consSig (consNameStr,consType) [] = false
   215  | in_list_forb consSig (consNameStr,consType) ((forbNameStr,forbTypeStr)::xs) = 
   216    let 
   217      val forbType = Syntax.read_typ_global consSig forbTypeStr
   218      val typeSignature = #tsig (Sign.rep_sg consSig)
   219    in
   220      if ((consNameStr = forbNameStr) 
   221        andalso (Type.typ_instance typeSignature (consType,(Logic.varifyT forbType))))
   222      then true
   223      else in_list_forb consSig (consNameStr,consType) xs
   224    end;
   225 
   226 
   227 
   228 (*searches in the given signature Consts with the same type as sterm and 
   229 returns a list of those terms*)
   230 
   231 fun searchForSignatureMutations (sterm,stype) consSig forbidden_funs = 
   232  let 
   233    val sigConsTypeList = consts_of consSig;
   234    val typeSignature = #tsig (Sign.rep_sg consSig)
   235  in 
   236    let 
   237      fun recursiveSearch mutatableTermList [] = mutatableTermList
   238        | recursiveSearch mutatableTermList ((ConsName,ConsType)::xs) = 
   239          if (Type.typ_instance typeSignature (stype,ConsType) 
   240            andalso (not (sterm = Const(ConsName,stype))) 
   241            andalso (not (in_list_forb consSig (ConsName,ConsType) forbidden_funs))) 
   242          then recursiveSearch ((Term.Const(ConsName,stype), [], [], [5])::mutatableTermList) xs
   243          else recursiveSearch mutatableTermList xs
   244      in
   245        recursiveSearch [] sigConsTypeList
   246      end
   247    end;     
   248 
   249 
   250 (*generates a list of terms that can be used instead of the passed subterm in the original term. These terms either have
   251 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
   252 in the current signature.
   253 This function has 3 versions:
   254 0: no instertion of signature functions, 
   255   only terms in the subTermList with the same type and appropriate context as the passed term are returned
   256 1: no exchange of subterms,
   257   only signature functions are inserted at the place of type-aequivalent Conses
   258 2: mixture of the two other versions. insertion of signature functions and exchange of subterms*)
   259 
   260 fun searchForMutatableTerm 0 (sterm,stype,sabscontext,smincontext,spath) 
   261    subTerms consSig resultList forbidden_funs =
   262    searchForMutatableSubTerm (sterm,stype,sabscontext,smincontext,spath) subTerms resultList
   263  | searchForMutatableTerm 1 (Const(constName,constType),stype,sabscontext,smincontext,spath) 
   264    subTerms consSig resultList forbidden_funs = 
   265    searchForSignatureMutations (Const(constName,constType),stype) consSig forbidden_funs
   266  | searchForMutatableTerm 1 _ _ _ _ _ = []
   267  | searchForMutatableTerm 2 (Const(constName,constType),stype,sabscontext,smincontext,spath) 
   268    subTerms consSig resultList forbidden_funs = 
   269      let 
   270        val subtermMutations = searchForMutatableSubTerm 
   271          (Const(constName,constType),stype,sabscontext,smincontext,spath) subTerms resultList
   272        val signatureMutations = searchForSignatureMutations 
   273          (Const(constName,constType),stype) consSig forbidden_funs
   274      in
   275        subtermMutations@signatureMutations
   276      end
   277  | searchForMutatableTerm 2 (sterm,stype,sabscontext,smincontext,spath) 
   278    subTerms consSig resultList forbidden_funs =
   279    searchForMutatableSubTerm (sterm,stype,sabscontext,smincontext,spath) subTerms resultList
   280  | searchForMutatableTerm i _ _ _ _ _ = 
   281    raise WrongArg("Version " ^ string_of_int i ^ 
   282      " doesn't exist for function searchForMutatableTerm!") ;
   283 
   284 
   285 
   286 
   287 (*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*)  
   288 
   289 fun areReplacable [] [] = false
   290  | areReplacable fstPath [] = false
   291  | areReplacable [] sndPath = false
   292  | areReplacable (x::xs) (y::ys) = if (x=y) then areReplacable xs ys else true; 
   293 
   294 
   295 
   296 
   297 (*substitutes the term at the position of the first list in fstTerm by sndTerm. 
   298 The lists represent paths as generated by createSubTermList*)
   299 
   300 fun substitute [] fstTerm sndTerm = sndTerm
   301  | substitute (_::xs) (Abs(s,T,subTerm)) sndTerm = Abs(s,T,(substitute xs subTerm sndTerm))
   302  | substitute (0::xs) (t $ u) sndTerm = substitute xs t sndTerm $ u 
   303  | substitute (1::xs) (t $ u) sndTerm = t $ substitute xs u sndTerm
   304  | substitute (_::xs) _ sndTerm = 
   305    raise WrongPath ("The Term could not be found at the specified position"); 
   306 
   307 
   308 (*get the subterm with the specified path in myTerm*)
   309 
   310 fun getSubTerm myTerm [] = myTerm
   311  | getSubTerm (Abs(s,T,subTerm)) (0::xs) = getSubTerm subTerm xs
   312  | getSubTerm (t $ u) (0::xs) = getSubTerm t xs
   313  | getSubTerm (t $ u) (1::xs) = getSubTerm u xs
   314  | getSubTerm _ (_::xs) = 
   315    raise WrongPath ("The subterm could not be found at the specified position");
   316 
   317 
   318 (*exchanges two subterms with the given paths in the original Term*)
   319 
   320 fun replace origTerm (fstTerm, fstPath) (sndTerm, sndPath) = 
   321  if (areReplacable (rev fstPath) (rev sndPath))
   322  then substitute (rev sndPath) (substitute (rev fstPath) origTerm sndTerm) fstTerm
   323  else origTerm; 
   324 
   325 
   326 
   327 
   328 (*tests if the terms with the given pathes in the origTerm are commutative
   329 respecting the list of commutative operators (commutatives)*)
   330 
   331 fun areCommutative origTerm fstPath sndPath commutatives =
   332  if (sndPath = []) 
   333  then false
   334  else
   335    let 
   336      val base = (tl sndPath)
   337    in
   338      let 
   339        val fstcomm = 1::0::base
   340        val opcomm = 0::0::base
   341      in
   342        if ((fstPath = fstcomm) andalso (is_Const (getSubTerm origTerm (rev opcomm))))
   343        then
   344          let 
   345            val Const(name,_) = (getSubTerm origTerm (rev opcomm))
   346          in
   347            if (in_list name commutatives) 
   348            then true 
   349            else false
   350          end
   351        else false
   352      end
   353    end;
   354 
   355 
   356 (*Canonizes term t with the commutative operators stored in list 
   357 commutatives*)
   358 
   359 fun canonize_term (Const (s, T) $ t $ u) comms =
   360  let
   361    val t' = canonize_term t comms;
   362    val u' = canonize_term u comms;
   363  in 
   364    if s mem comms andalso Term_Ord.termless (u', t')
   365    then Const (s, T) $ u' $ t'
   366    else Const (s, T) $ t' $ u'
   367  end
   368  | canonize_term (t $ u) comms = canonize_term t comms $ canonize_term u comms
   369  | canonize_term (Abs (s, T, t)) comms = Abs (s, T, canonize_term t comms)
   370  | canonize_term t comms = t;
   371 
   372 
   373 (*inspect the passed list and mutate origTerm following the elements of the list:
   374 if the path of the current element is [5] (dummy path), the term has been found in the signature 
   375 and the subterm will be substituted by it
   376 else the term has been found in the original term and the two subterms have to be exchanged
   377 The additional parameter commutatives indicates the commutative operators  
   378 in the term whose operands won't be exchanged*)
   379 
   380 fun createMutatedTerms origTerm _ [] commutatives mutatedTerms = mutatedTerms
   381  | createMutatedTerms origTerm (hdt as (hdTerm,hdabsContext,hdminContext,hdPath))
   382    ((sndTerm,sndabsContext,sndminContext,sndPath)::xs) commutatives mutatedTerms = 
   383    if (sndPath = [5])
   384    then
   385      let 
   386          val canonized = canonize_term (substitute (rev hdPath) origTerm sndTerm) commutatives
   387        in
   388          if (canonized = origTerm)  
   389          then createMutatedTerms origTerm hdt xs commutatives mutatedTerms
   390          else createMutatedTerms origTerm hdt xs commutatives 
   391            (insert op aconv canonized mutatedTerms)
   392        end
   393      else 
   394        if ((areCommutative origTerm hdPath sndPath commutatives)
   395          orelse (areCommutative origTerm sndPath hdPath commutatives)) 
   396        then createMutatedTerms origTerm hdt xs commutatives mutatedTerms
   397        else
   398          let 
   399            val canonized = canonize_term 
   400              (replace origTerm
   401                 (incr_boundvars (length sndabsContext - length hdminContext) hdTerm,
   402                  hdPath)
   403                 (incr_boundvars (length hdabsContext - length sndminContext) sndTerm,
   404                  sndPath)) commutatives
   405          in
   406            if (not(canonized = origTerm)) 
   407            then createMutatedTerms origTerm hdt xs commutatives 
   408              (insert op aconv canonized mutatedTerms)
   409            else createMutatedTerms origTerm hdt xs commutatives mutatedTerms
   410          end;
   411 
   412 
   413 
   414 (*mutates origTerm by exchanging subterms. The mutated terms are returned in a term list
   415 The parameter commutatives consists of a list of commutative operators. The permutation of their 
   416 operands won't be considered as a new term
   417 !!!Attention!!!: The given origTerm must be canonized. Use function canonize_term!*)
   418 
   419 fun mutate_once option origTerm tsig commutatives forbidden_funs= 
   420  let 
   421    val subTermList = getSubTermList origTerm [] [] []
   422  in
   423    let 
   424      fun replaceRecursively [] mutatedTerms = mutatedTerms
   425        | replaceRecursively ((hdTerm,hdType,hdabsContext,hdminContext,hdPath)::tail) 
   426          mutatedTerms =
   427          replaceRecursively tail (union op aconv (createMutatedTerms origTerm 
   428            (hdTerm,hdabsContext,hdminContext,hdPath) 
   429            (searchForMutatableTerm option (hdTerm,hdType,hdabsContext,hdminContext,hdPath) 
   430              tail tsig [] forbidden_funs) 
   431            commutatives []) mutatedTerms)
   432    in
   433      replaceRecursively subTermList []
   434    end
   435  end;
   436 
   437 
   438 
   439 
   440 (*helper function in order to apply recursively the mutate_once function on a whole list of terms
   441 Needed for the mutate function*)
   442 
   443 fun mutate_once_rec option [] tsig commutatives forbidden_funs acc = acc
   444  | mutate_once_rec option (x::xs) tsig commutatives forbidden_funs acc = 
   445    mutate_once_rec option xs tsig commutatives forbidden_funs 
   446      (union op aconv (mutate_once option x tsig commutatives forbidden_funs) acc);
   447 
   448 
   449 
   450 (*apply function mutate_once iter times on the given origTerm. *)
   451 (*call of mutiere with canonized form of origTerm. Prevents us of the computation of
   452 canonization in the course of insertion of new terms!*)
   453 
   454 fun mutate option origTerm tsig commutatives forbidden_funs 0 = []
   455  | mutate option origTerm tsig commutatives forbidden_funs 1 = 
   456    mutate_once option (canonize_term origTerm commutatives) tsig commutatives forbidden_funs
   457  | mutate option origTerm tsig commutatives forbidden_funs iter = 
   458    mutate_once_rec option (mutate option origTerm tsig commutatives forbidden_funs (iter-1)) 
   459      tsig commutatives forbidden_funs []; 
   460 
   461 (*mutate origTerm iter times by only exchanging subterms*)
   462 
   463 fun mutate_exc origTerm commutatives iter =
   464  mutate 0 origTerm (theory "Main") commutatives [] iter;
   465 
   466 
   467 (*mutate origTerm iter times by only inserting signature functions*)
   468 
   469 fun mutate_sign origTerm tsig forbidden_funs iter = 
   470  mutate 1 origTerm tsig [] forbidden_funs iter;
   471 
   472 
   473 (*mutate origTerm iter times by exchange of subterms and insertion of subterms*)
   474 
   475 fun mutate_mix origTerm tsig commutatives forbidden_funs iter =
   476  mutate 2 origTerm tsig commutatives forbidden_funs iter;  
   477 
   478 
   479 (*helper function in order to prettily print a list of terms*)
   480 
   481 fun pretty xs = map (fn (id, t) => (id, (HOLogic.mk_number HOLogic.natT
   482  (HOLogic.dest_nat t)) handle TERM _ => t)) xs;
   483 
   484 
   485 (*helper function for the quickcheck invocation. Evaluates the quickcheck_term function on a whole list of terms
   486 and tries to print the exceptions*)
   487 
   488 fun freeze (t $ u) = freeze t $ freeze u
   489  | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
   490  | freeze (Var ((a, i), T)) =
   491      Free (if i = 0 then a else a ^ "_" ^ string_of_int i, T)
   492  | freeze t = t;
   493 
   494 fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
   495  | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T);
   496 
   497 fun preprocess thy insts t = ObjectLogic.atomize_term thy
   498  (map_types (inst_type insts) (freeze t));
   499 
   500 fun is_executable thy insts th =
   501  (Quickcheck.test_term
   502     (ProofContext.init thy) false (SOME (!testgen_name)) 1 1 (preprocess thy insts (prop_of th));
   503   priority "executable"; true) handle ERROR s =>
   504     (priority ("not executable: " ^ s); false);
   505 
   506 fun qc_recursive usedthy [] insts sz qciter acc = rev acc
   507  | qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter 
   508      (priority ("qc_recursive: " ^ string_of_int (length xs)); ((x, pretty (the_default [] (Quickcheck.test_term
   509        (ProofContext.init usedthy) false (SOME (!testgen_name)) sz qciter (preprocess usedthy insts x)))) :: acc))
   510           handle ERROR msg => (priority msg; qc_recursive usedthy xs insts sz qciter acc);
   511 
   512 
   513 (*quickcheck-test the mutants created by function mutate with type-instantiation insts, 
   514 quickcheck-theory usedthy and qciter quickcheck-iterations *)
   515 
   516 fun qc_test mutated insts usedthy sz qciter = 
   517  let 
   518    val checked = map (apsnd (map (apsnd (cterm_of usedthy))))
   519      (qc_recursive usedthy mutated insts sz qciter []);
   520    fun combine (passednum,passed) (cenum,ces) [] = (passednum,passed,cenum,ces)
   521      | combine (passednum,passed) (cenum,ces) ((t, []) :: xs) =
   522        combine (passednum+1,(cterm_of usedthy t)::passed) (cenum,ces) xs
   523      | combine (passednum,passed) (cenum,ces) ((t, x) :: xs) =
   524        combine (passednum,passed) 
   525          (cenum+1,(cterm_of usedthy t, x) :: ces) xs
   526  in
   527    combine (0,[]) (0,[]) checked
   528  end;
   529 
   530 
   531 (*create a string of a list of terms*)
   532 
   533 fun string_of_ctermlist thy [] acc = acc
   534  | string_of_ctermlist thy (x::xs) acc = 
   535    string_of_ctermlist thy xs ((Syntax.string_of_term_global thy (term_of x)) ^ "\n" ^ acc);
   536 
   537 (*helper function in order to decompose the counter examples generated by quickcheck*)
   538 
   539 fun decompose_ce thy [] acc = acc
   540  | decompose_ce thy ((varname,varce)::xs) acc = 
   541    decompose_ce thy xs ("\t" ^ varname ^ " instanciated to " ^ 
   542      (Syntax.string_of_term_global thy (term_of varce)) ^ "\n" ^ acc);
   543 
   544 (*helper function in order to decompose a list of counter examples*)
   545 
   546 fun decompose_celist thy [] acc = acc
   547  | decompose_celist thy ((mutTerm,varcelist)::xs) acc = decompose_celist thy xs 
   548    ("mutated term : " ^ 
   549    (Syntax.string_of_term_global thy (term_of mutTerm)) ^ "\n" ^ 
   550    "counterexample : \n" ^ 
   551    (decompose_ce thy (rev varcelist) "") ^ acc); 
   552 
   553 
   554 (*quickcheck test the list of mutants mutated by applying the type instantiations 
   555 insts and using the quickcheck-theory usedthy. The results of quickcheck are stored
   556 in the file with name filename. If app is true, the output will be appended to the file. 
   557 Else it will be overwritten. *)
   558 
   559 fun qc_test_file app mutated insts usedthy sz qciter filename =
   560  let 
   561    val statisticList = qc_test mutated insts usedthy sz qciter
   562    val passed = (string_of_int (#1 statisticList)) ^ 
   563      " terms passed the quickchecktest: \n\n" ^ 
   564      (string_of_ctermlist usedthy (rev (#2 statisticList)) "") 
   565    val counterexps = (string_of_int (#3 statisticList)) ^ 
   566      " terms produced a counterexample: \n\n" ^
   567      decompose_celist usedthy (rev (#4 statisticList)) "" 
   568  in
   569    if (app = false) 
   570    then File.write (Path.explode filename) (passed ^ "\n\n" ^ counterexps)
   571    else File.append (Path.explode filename) (passed ^ "\n\n" ^ counterexps)
   572  end;
   573 
   574 
   575 (*mutate sourceThm with the mutate-version given in option and check the resulting mutants. 
   576 The output will be written to the file with name filename*)
   577 
   578 fun mutqc_file option usedthy commutatives forbidden_funs iter sourceThm insts sz qciter filename =
   579  let 
   580    val mutated = mutate option (prop_of sourceThm) 
   581      usedthy commutatives forbidden_funs iter 
   582  in
   583    qc_test_file false mutated insts usedthy sz qciter filename 
   584  end;
   585 
   586 (*exchange version of function mutqc_file*)
   587 
   588 fun mutqc_file_exc usedthy commutatives iter sourceThm insts sz qciter filename =
   589  mutqc_file 0 usedthy commutatives [] iter sourceThm insts sz qciter filename;
   590 
   591 
   592 (*sinature version of function mutqc_file*)
   593 fun mutqc_file_sign usedthy forbidden_funs iter sourceThm insts sz qciter filename= 
   594  mutqc_file 1 usedthy [] forbidden_funs iter sourceThm insts sz qciter filename;
   595 
   596 (*mixed version of function mutqc_file*)
   597 
   598 fun mutqc_file_mix usedthy commutatives forbidden_funs iter sourceThm insts sz qciter filename =
   599  mutqc_file 2 usedthy commutatives forbidden_funs iter sourceThm insts sz qciter filename;
   600 
   601 
   602 
   603 (*apply function mutqc_file on a list of theorems. The output for each theorem 
   604 will be stored in a seperated file whose filename must be indicated in a list*)
   605 
   606 fun mutqc_file_rec option usedthy commutatives forbFuns iter [] insts sz qciter _ = ()
   607  | mutqc_file_rec option usedthy commutatives forbFuns iter  sourceThms insts sz qciter [] = 
   608    raise WrongArg ("Not enough files for the output of qc_test_file_rec!")
   609  | mutqc_file_rec option usedthy commutatives forbFuns iter (x::xs) insts sz qciter (y::ys) = 
   610    (mutqc_file option usedthy commutatives forbFuns iter x insts sz qciter y ; 
   611    mutqc_file_rec option usedthy commutatives forbFuns iter xs insts sz qciter ys);
   612 
   613 
   614 (*exchange version of function mutqc_file_rec*)
   615 
   616 fun mutqc_file_rec_exc usedthy commutatives iter sourceThms insts sz qciter files =
   617  mutqc_file_rec 0 usedthy commutatives [] iter sourceThms insts sz qciter files;
   618 
   619 (*signature version of function mutqc_file_rec*)
   620 
   621 fun mutqc_file_rec_sign usedthy forbidden_funs iter sourceThms insts sz qciter files =
   622  mutqc_file_rec 1 usedthy [] forbidden_funs iter sourceThms insts sz qciter files;
   623 
   624 (*mixed version of function mutqc_file_rec*)
   625 
   626 fun mutqc_file_rec_mix usedthy commutatives forbidden_funs iter sourceThms insts sz qciter files =
   627  mutqc_file_rec 2 usedthy commutatives forbidden_funs iter sourceThms insts sz qciter files;
   628 
   629 (*create the appropriate number of spaces in order to properly print a table*)
   630 
   631 fun create_spaces entry spacenum =
   632  let 
   633 		val diff = spacenum - (size entry)
   634  in 
   635 		if (diff > 0) 
   636    then implode (replicate diff " ")
   637    else ""
   638  end;
   639 
   640 
   641 (*create a statistic of the output of a quickcheck test on the passed thmlist*)
   642 
   643 fun mutqc_file_stat option usedthy commutatives forbidden_funs iter thmlist insts sz qciter filename = 
   644  let 
   645    fun mutthmrec [] = ()
   646    |   mutthmrec (x::xs) =
   647      let 
   648        val mutated = mutate option (prop_of x) usedthy
   649          commutatives forbidden_funs iter
   650        val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter
   651        val thmname =  "\ntheorem " ^ (Thm.get_name x) ^ ":"
   652        val pnumstring = string_of_int passednum
   653        val cenumstring = string_of_int cenum
   654      in
   655        (File.append (Path.explode filename) 
   656          (thmname ^ (create_spaces thmname 50) ^ 
   657          pnumstring ^ (create_spaces pnumstring 20) ^ 
   658          cenumstring ^ (create_spaces cenumstring 20) ^ "\n");
   659        mutthmrec xs)
   660      end;
   661  in 
   662    (File.write (Path.explode filename) 
   663      ("\n\ntheorem name" ^ (create_spaces "theorem name" 50) ^ 
   664      "passed mutants"  ^ (create_spaces "passed mutants" 20) ^ 
   665      "counter examples\n\n" );
   666    mutthmrec thmlist)
   667  end;
   668 
   669 (*signature version of function mutqc_file_stat*)
   670 
   671 fun mutqc_file_stat_sign usedthy forbidden_funs iter thmlist insts sz qciter filename =
   672  mutqc_file_stat 1 usedthy [] forbidden_funs iter thmlist insts sz qciter filename;
   673 
   674 (*exchange version of function mutqc_file_stat*)
   675 
   676 fun mutqc_file_stat_exc usedthy commutatives iter thmlist insts sz qciter filename =
   677  mutqc_file_stat 0 usedthy commutatives [] iter thmlist insts sz qciter filename;
   678 
   679 (*mixed version of function mutqc_file_stat*)
   680 
   681 fun mutqc_file_stat_mix usedthy commutatives forbidden_funs iter thmlist insts sz qciter filename =
   682  mutqc_file_stat 2 usedthy commutatives forbidden_funs iter thmlist insts sz qciter filename;
   683 
   684 (*mutate and quickcheck-test all the theorems contained in the passed theory. 
   685 The output will be stored in a single file*)
   686 
   687 fun mutqc_thy option mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
   688  let
   689    val thmlist = filter (is_executable mutthy insts o snd) (thms_of mutthy);
   690    fun mutthmrec [] = ()
   691      | mutthmrec ((name,thm)::xs) = 
   692          let
   693            val mutated = mutate option (prop_of thm) 
   694              usedthy commutatives forbidden_funs iter
   695          in
   696            (File.append (Path.explode filename) 
   697              ("--------------------------\n\nQuickchecktest of theorem " ^ name ^ ":\n\n");
   698            qc_test_file true mutated insts usedthy sz qciter filename;
   699            mutthmrec xs)
   700          end;
   701    in 
   702      mutthmrec thmlist
   703    end;
   704 
   705 (*exchange version of function mutqc_thy*)
   706 
   707 fun mutqc_thy_exc mutthy usedthy commutatives iter insts sz qciter filename =
   708  mutqc_thy 0 mutthy usedthy commutatives [] iter insts sz qciter filename;
   709 
   710 (*signature version of function mutqc_thy*)
   711 
   712 fun mutqc_thy_sign mutthy usedthy forbidden_funs iter insts sz qciter filename =
   713  mutqc_thy 1 mutthy usedthy [] forbidden_funs iter insts sz qciter filename;
   714 
   715 (*mixed version of function mutqc_thy*)
   716 
   717 fun mutqc_thy_mix mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
   718  mutqc_thy 2 mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename;
   719 
   720 (*create a statistic representation of the call of function mutqc_thy*)
   721 
   722 fun mutqc_thystat option p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
   723  let
   724    val thmlist = filter
   725      (fn (s, th) => not (p s th) andalso (priority s; is_executable mutthy insts th)) (thms_of mutthy)
   726    fun mutthmrec [] = ()
   727    |   mutthmrec ((name,thm)::xs) =
   728      let          
   729        val _ = priority ("mutthmrec: " ^ name);
   730        val mutated = mutate option (prop_of thm) usedthy
   731            commutatives forbidden_funs iter
   732        val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter
   733        val thmname =  "\ntheorem " ^ name ^ ":"
   734        val pnumstring = string_of_int passednum
   735        val cenumstring = string_of_int cenum
   736      in
   737        (File.append (Path.explode filename) 
   738          (thmname ^ (create_spaces thmname 50) ^ 
   739          pnumstring ^ (create_spaces pnumstring 20) ^ 
   740          cenumstring ^ (create_spaces cenumstring 20) ^ "\n");
   741        mutthmrec xs)
   742      end;
   743  in 
   744    (File.write (Path.explode filename) ("Result of the quickcheck-test of theory " ^
   745      ":\n\ntheorem name" ^ (create_spaces "theorem name" 50) ^ 
   746      "passed mutants"  ^ (create_spaces "passed mutants" 20) ^ 
   747      "counter examples\n\n" );
   748    mutthmrec thmlist)
   749  end;
   750 
   751 (*exchange version of function mutqc_thystat*)
   752 			
   753 fun mutqc_thystat_exc p mutthy usedthy commutatives iter insts sz qciter filename =
   754  mutqc_thystat 0 p mutthy usedthy commutatives [] iter insts sz qciter filename;
   755 
   756 (*signature version of function mutqc_thystat*)
   757 
   758 fun mutqc_thystat_sign p mutthy usedthy forbidden_funs iter insts sz qciter filename =
   759  mutqc_thystat 1 p mutthy usedthy [] forbidden_funs iter insts sz qciter filename;
   760 
   761 (*mixed version of function mutqc_thystat*)
   762 
   763 fun mutqc_thystat_mix p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
   764  mutqc_thystat 2 p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename;
   765 
   766 end