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