src/HOL/Mutabelle/mutabelle.ML
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 56161 300f613060b0
child 67561 f0b11413f1c9
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
haftmann@37744
     1
(*  Title:      HOL/Mutabelle/mutabelle.ML
berghofe@34967
     2
    Author:     Veronika Ortner, TU Muenchen
bulwahn@34965
     3
wenzelm@41408
     4
Mutation of theorems.
bulwahn@34965
     5
*)
wenzelm@41408
     6
bulwahn@34965
     7
signature MUTABELLE =
bulwahn@34965
     8
sig
bulwahn@43883
     9
  exception WrongPath of string;
bulwahn@43883
    10
  exception WrongArg of string;
bulwahn@43883
    11
  val freeze : term -> term
bulwahn@43883
    12
  val mutate_exc : term -> string list -> int -> term list 
bulwahn@43883
    13
  val mutate_sign : term -> theory -> (string * string) list -> int -> term list 
bulwahn@43883
    14
  val mutate_mix : term -> theory -> string list -> 
bulwahn@34965
    15
   (string * string) list -> int -> term list
bulwahn@34965
    16
end;
bulwahn@34965
    17
bulwahn@34965
    18
structure Mutabelle : MUTABELLE = 
bulwahn@34965
    19
struct
bulwahn@34965
    20
bulwahn@34965
    21
fun consts_of thy =
bulwahn@34965
    22
 let
wenzelm@56025
    23
   val {const_space, constants, ...} = Consts.dest (Sign.consts_of thy)
bulwahn@34965
    24
 in
wenzelm@42429
    25
   map_filter (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
wenzelm@56062
    26
     (filter_out (fn (s, _) => Name_Space.is_concealed const_space s) constants)
bulwahn@34965
    27
 end;
bulwahn@34965
    28
bulwahn@34965
    29
bulwahn@34965
    30
(*thrown in case the specified path doesn't exist in the specified term*)
bulwahn@34965
    31
bulwahn@34965
    32
exception WrongPath of string;
bulwahn@34965
    33
bulwahn@34965
    34
bulwahn@34965
    35
(*thrown in case the arguments did not fit to the function*)
bulwahn@34965
    36
bulwahn@34965
    37
exception WrongArg of string; 
bulwahn@34965
    38
bulwahn@34965
    39
(*Rename the bound variables in a term with the minimal Index min of 
bulwahn@34965
    40
bound variables. Variable (Bound(min)) will be renamed to Bound(0) etc. 
bulwahn@34965
    41
This is needed in course auf evaluation of contexts.*)
bulwahn@34965
    42
bulwahn@34965
    43
fun rename_bnds curTerm 0 = curTerm
bulwahn@34965
    44
 | rename_bnds (Bound(i)) minInd = 
bulwahn@34965
    45
   let 
bulwahn@34965
    46
     val erg = if (i-minInd < 0) then 0 else (i - minInd)
bulwahn@34965
    47
   in 
bulwahn@34965
    48
     Bound(erg)
bulwahn@34965
    49
   end
bulwahn@34965
    50
 | rename_bnds (Abs(name,t,uTerm)) minInd = 
bulwahn@34965
    51
   Abs(name,t,(rename_bnds uTerm minInd))
bulwahn@34965
    52
 | rename_bnds (fstUTerm $ sndUTerm) minInd =
bulwahn@34965
    53
   (rename_bnds fstUTerm minInd) $ (rename_bnds sndUTerm minInd)
bulwahn@34965
    54
 | rename_bnds elseTerm minInd = elseTerm;
bulwahn@34965
    55
bulwahn@34965
    56
bulwahn@34965
    57
bulwahn@34965
    58
bulwahn@34965
    59
bulwahn@34965
    60
(*Partition a term in its subterms and create an entry 
bulwahn@34965
    61
(term * type * abscontext * mincontext * path) 
bulwahn@34965
    62
for each term in the return list 
bulwahn@34965
    63
e.g: getSubTermList Abs(y, int, Const(f,int->int) $ Const(x,int) $ Bound(0))
bulwahn@34965
    64
will give       [(Const(f,int->int),int->int,[int],[],[00]),
bulwahn@34965
    65
               (Const(x,int),int,[int],[],[010]),
bulwahn@34965
    66
               (Bound(0),int,[int],[int],[110]),
bulwahn@34965
    67
               (Const(x,int) $ Bound(0),type,[int],[int],[10]),
bulwahn@34965
    68
               (Const(f,int->int) $ Const(x,int) $ Bound(0),type,[int],[int],[0],
bulwahn@34965
    69
               (Abs (y,int,Const(f,int->int) $ const(x,int) $ Bound(0)),type,[],[],[])]
bulwahn@34965
    70
                *)
bulwahn@34965
    71
bulwahn@34965
    72
fun getSubTermList (Const(name,t)) abscontext path acc =
bulwahn@34965
    73
   (Const(name,t),t,abscontext,abscontext,path)::acc
bulwahn@34965
    74
 | getSubTermList (Free(name,t)) abscontext path acc =
bulwahn@34965
    75
   (Free(name,t),t,abscontext,abscontext,path)::acc
bulwahn@34965
    76
 | getSubTermList (Var(indname,t)) abscontext path acc =
bulwahn@34965
    77
   (Var(indname,t),t,abscontext,abscontext,path)::acc
bulwahn@34965
    78
 | getSubTermList (Bound(i)) abscontext path acc =
bulwahn@34965
    79
   (Bound(0),nth abscontext i,abscontext, Library.drop i abscontext,path)::acc
bulwahn@34965
    80
 | getSubTermList (Abs(name,t,uTerm)) abscontext path acc = 
bulwahn@34965
    81
   let 
bulwahn@34965
    82
     val curTerm = Abs(name,t,uTerm)
bulwahn@34965
    83
     val bnos = Term.add_loose_bnos (curTerm,0,[])
bulwahn@34965
    84
     val minInd = if (bnos = []) then 0 
bulwahn@34965
    85
       else Library.foldl (fn (n,m) => if (n<m) then n else m) (hd bnos,tl bnos)
bulwahn@34965
    86
     val newTerm = rename_bnds curTerm minInd
bulwahn@34965
    87
     val newContext = Library.drop minInd abscontext
bulwahn@34965
    88
   in 
bulwahn@34965
    89
     getSubTermList uTerm (t::abscontext) (0::path) 
bulwahn@34965
    90
               ((newTerm,(fastype_of1 (abscontext, curTerm)),abscontext,newContext,path)::acc)
bulwahn@34965
    91
   end
bulwahn@34965
    92
 | getSubTermList (fstUTerm $ sndUTerm) abscontext path acc = 
bulwahn@34965
    93
   let 
bulwahn@34965
    94
     val curTerm = (fstUTerm $ sndUTerm)
bulwahn@34965
    95
     val bnos = Term.add_loose_bnos (curTerm, 0, [])
bulwahn@34965
    96
     val minInd = if (bnos = []) then 0
bulwahn@34965
    97
       else Library.foldl (fn (n,m) => if (n<m) then n else m) (hd bnos,tl bnos)
bulwahn@34965
    98
     val newTerm = rename_bnds curTerm minInd
bulwahn@34965
    99
     val newContext = Library.drop minInd abscontext
bulwahn@34965
   100
   in 
bulwahn@34965
   101
     getSubTermList fstUTerm abscontext (0::path) 
bulwahn@34965
   102
       (getSubTermList sndUTerm abscontext (1::path) 
bulwahn@34965
   103
         ((newTerm,(fastype_of1 (abscontext, curTerm)),abscontext,newContext,path)::acc)) 
bulwahn@34965
   104
   end;  
bulwahn@34965
   105
bulwahn@34965
   106
bulwahn@34965
   107
(*Evaluate if the longContext is more special as the shortContext. 
bulwahn@34965
   108
If so, a term with shortContext can be substituted in the place of a 
bulwahn@34965
   109
term with longContext*)
bulwahn@34965
   110
bulwahn@34965
   111
fun is_morespecial longContext shortContext = 
bulwahn@34965
   112
 let 
bulwahn@34965
   113
   val revlC = rev longContext
bulwahn@34965
   114
   val revsC = rev shortContext
haftmann@51092
   115
   fun is_prefix [] _ = true
haftmann@51092
   116
     | is_prefix _ [] = false
bulwahn@34965
   117
     | is_prefix (x::xs) (y::ys) = if (x=y) then is_prefix xs ys else false
bulwahn@34965
   118
 in 
bulwahn@34965
   119
   is_prefix revsC revlC
bulwahn@34965
   120
 end;
bulwahn@34965
   121
bulwahn@34965
   122
bulwahn@34965
   123
(*takes a (term * type * context * context * path)-tupel and searches in the specified list for 
bulwahn@34965
   124
terms with the same type and appropriate context. Returns a (term * path) list of these terms.
bulwahn@34965
   125
Used in order to generate a list of type-equal subterms of the original term*)
bulwahn@34965
   126
bulwahn@34965
   127
fun searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) [] resultList = 
bulwahn@34965
   128
   resultList
bulwahn@34965
   129
 | searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) 
bulwahn@34965
   130
   ((hdterm,hdtype,hdabsContext,hdminContext,hdpath)::xs) resultList = 
bulwahn@34965
   131
   if ((stype = hdtype) andalso (is_morespecial sabsContext hdminContext) 
bulwahn@34965
   132
     andalso (is_morespecial hdabsContext sminContext)) 
bulwahn@34965
   133
   then searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) xs 
bulwahn@34965
   134
     ((hdterm,hdabsContext,hdminContext,hdpath)::resultList) 
bulwahn@34965
   135
   else searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) xs resultList;
bulwahn@34965
   136
bulwahn@34965
   137
bulwahn@34965
   138
(*evaluates if the given function is in the passed list of forbidden functions*)
bulwahn@34965
   139
bulwahn@34965
   140
fun in_list_forb consSig (consNameStr,consType) [] = false
bulwahn@34965
   141
 | in_list_forb consSig (consNameStr,consType) ((forbNameStr,forbTypeStr)::xs) = 
bulwahn@34965
   142
   let 
bulwahn@34965
   143
     val forbType = Syntax.read_typ_global consSig forbTypeStr
bulwahn@34965
   144
   in
bulwahn@34965
   145
     if ((consNameStr = forbNameStr) 
wenzelm@47004
   146
       andalso (Sign.typ_instance consSig (consType,(Logic.varifyT_global forbType))))
bulwahn@34965
   147
     then true
bulwahn@34965
   148
     else in_list_forb consSig (consNameStr,consType) xs
bulwahn@34965
   149
   end;
bulwahn@34965
   150
bulwahn@34965
   151
bulwahn@34965
   152
bulwahn@34965
   153
(*searches in the given signature Consts with the same type as sterm and 
bulwahn@34965
   154
returns a list of those terms*)
bulwahn@34965
   155
bulwahn@34965
   156
fun searchForSignatureMutations (sterm,stype) consSig forbidden_funs = 
bulwahn@34965
   157
 let 
bulwahn@34965
   158
   val sigConsTypeList = consts_of consSig;
bulwahn@34965
   159
 in 
bulwahn@34965
   160
   let 
bulwahn@34965
   161
     fun recursiveSearch mutatableTermList [] = mutatableTermList
bulwahn@34965
   162
       | recursiveSearch mutatableTermList ((ConsName,ConsType)::xs) = 
wenzelm@47004
   163
         if (Sign.typ_instance consSig (stype,ConsType) 
bulwahn@34965
   164
           andalso (not (sterm = Const(ConsName,stype))) 
bulwahn@34965
   165
           andalso (not (in_list_forb consSig (ConsName,ConsType) forbidden_funs))) 
bulwahn@34965
   166
         then recursiveSearch ((Term.Const(ConsName,stype), [], [], [5])::mutatableTermList) xs
bulwahn@34965
   167
         else recursiveSearch mutatableTermList xs
bulwahn@34965
   168
     in
bulwahn@34965
   169
       recursiveSearch [] sigConsTypeList
bulwahn@34965
   170
     end
bulwahn@34965
   171
   end;     
bulwahn@34965
   172
bulwahn@34965
   173
bulwahn@34965
   174
(*generates a list of terms that can be used instead of the passed subterm in the original term. These terms either have
bulwahn@34965
   175
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
bulwahn@34965
   176
in the current signature.
bulwahn@34965
   177
This function has 3 versions:
bulwahn@34965
   178
0: no instertion of signature functions, 
bulwahn@34965
   179
  only terms in the subTermList with the same type and appropriate context as the passed term are returned
bulwahn@34965
   180
1: no exchange of subterms,
bulwahn@34965
   181
  only signature functions are inserted at the place of type-aequivalent Conses
bulwahn@34965
   182
2: mixture of the two other versions. insertion of signature functions and exchange of subterms*)
bulwahn@34965
   183
bulwahn@34965
   184
fun searchForMutatableTerm 0 (sterm,stype,sabscontext,smincontext,spath) 
bulwahn@34965
   185
   subTerms consSig resultList forbidden_funs =
bulwahn@34965
   186
   searchForMutatableSubTerm (sterm,stype,sabscontext,smincontext,spath) subTerms resultList
bulwahn@34965
   187
 | searchForMutatableTerm 1 (Const(constName,constType),stype,sabscontext,smincontext,spath) 
bulwahn@34965
   188
   subTerms consSig resultList forbidden_funs = 
bulwahn@34965
   189
   searchForSignatureMutations (Const(constName,constType),stype) consSig forbidden_funs
bulwahn@34965
   190
 | searchForMutatableTerm 1 _ _ _ _ _ = []
bulwahn@34965
   191
 | searchForMutatableTerm 2 (Const(constName,constType),stype,sabscontext,smincontext,spath) 
bulwahn@34965
   192
   subTerms consSig resultList forbidden_funs = 
bulwahn@34965
   193
     let 
bulwahn@34965
   194
       val subtermMutations = searchForMutatableSubTerm 
bulwahn@34965
   195
         (Const(constName,constType),stype,sabscontext,smincontext,spath) subTerms resultList
bulwahn@34965
   196
       val signatureMutations = searchForSignatureMutations 
bulwahn@34965
   197
         (Const(constName,constType),stype) consSig forbidden_funs
bulwahn@34965
   198
     in
bulwahn@34965
   199
       subtermMutations@signatureMutations
bulwahn@34965
   200
     end
bulwahn@34965
   201
 | searchForMutatableTerm 2 (sterm,stype,sabscontext,smincontext,spath) 
bulwahn@34965
   202
   subTerms consSig resultList forbidden_funs =
bulwahn@34965
   203
   searchForMutatableSubTerm (sterm,stype,sabscontext,smincontext,spath) subTerms resultList
bulwahn@34965
   204
 | searchForMutatableTerm i _ _ _ _ _ = 
bulwahn@34965
   205
   raise WrongArg("Version " ^ string_of_int i ^ 
bulwahn@34965
   206
     " doesn't exist for function searchForMutatableTerm!") ;
bulwahn@34965
   207
bulwahn@34965
   208
bulwahn@34965
   209
bulwahn@34965
   210
bulwahn@34965
   211
(*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*)  
bulwahn@34965
   212
bulwahn@34965
   213
fun areReplacable [] [] = false
haftmann@51092
   214
 | areReplacable _ [] = false
haftmann@51092
   215
 | areReplacable [] _ = false
bulwahn@34965
   216
 | areReplacable (x::xs) (y::ys) = if (x=y) then areReplacable xs ys else true; 
bulwahn@34965
   217
bulwahn@34965
   218
bulwahn@34965
   219
bulwahn@34965
   220
bulwahn@34965
   221
(*substitutes the term at the position of the first list in fstTerm by sndTerm. 
bulwahn@34965
   222
The lists represent paths as generated by createSubTermList*)
bulwahn@34965
   223
haftmann@51092
   224
fun substitute [] _ sndTerm = sndTerm
bulwahn@34965
   225
 | substitute (_::xs) (Abs(s,T,subTerm)) sndTerm = Abs(s,T,(substitute xs subTerm sndTerm))
bulwahn@34965
   226
 | substitute (0::xs) (t $ u) sndTerm = substitute xs t sndTerm $ u 
bulwahn@34965
   227
 | substitute (1::xs) (t $ u) sndTerm = t $ substitute xs u sndTerm
haftmann@51092
   228
 | substitute (_::_) _ sndTerm = 
bulwahn@34965
   229
   raise WrongPath ("The Term could not be found at the specified position"); 
bulwahn@34965
   230
bulwahn@34965
   231
bulwahn@34965
   232
(*get the subterm with the specified path in myTerm*)
bulwahn@34965
   233
bulwahn@34965
   234
fun getSubTerm myTerm [] = myTerm
haftmann@51092
   235
 | getSubTerm (Abs(_,_,subTerm)) (0::xs) = getSubTerm subTerm xs
haftmann@51092
   236
 | getSubTerm (t $ _) (0::xs) = getSubTerm t xs
haftmann@51092
   237
 | getSubTerm (_ $ u) (1::xs) = getSubTerm u xs
haftmann@51092
   238
 | getSubTerm _ (_::_) = 
bulwahn@34965
   239
   raise WrongPath ("The subterm could not be found at the specified position");
bulwahn@34965
   240
bulwahn@34965
   241
bulwahn@34965
   242
(*exchanges two subterms with the given paths in the original Term*)
bulwahn@34965
   243
bulwahn@34965
   244
fun replace origTerm (fstTerm, fstPath) (sndTerm, sndPath) = 
bulwahn@34965
   245
 if (areReplacable (rev fstPath) (rev sndPath))
bulwahn@34965
   246
 then substitute (rev sndPath) (substitute (rev fstPath) origTerm sndTerm) fstTerm
bulwahn@34965
   247
 else origTerm; 
bulwahn@34965
   248
bulwahn@34965
   249
bulwahn@34965
   250
bulwahn@34965
   251
bulwahn@34965
   252
(*tests if the terms with the given pathes in the origTerm are commutative
bulwahn@34965
   253
respecting the list of commutative operators (commutatives)*)
bulwahn@34965
   254
bulwahn@34965
   255
fun areCommutative origTerm fstPath sndPath commutatives =
bulwahn@34965
   256
 if (sndPath = []) 
bulwahn@34965
   257
 then false
bulwahn@34965
   258
 else
bulwahn@34965
   259
   let 
bulwahn@34965
   260
     val base = (tl sndPath)
bulwahn@34965
   261
   in
bulwahn@34965
   262
     let 
bulwahn@34965
   263
       val fstcomm = 1::0::base
bulwahn@34965
   264
       val opcomm = 0::0::base
bulwahn@34965
   265
     in
bulwahn@34965
   266
       if ((fstPath = fstcomm) andalso (is_Const (getSubTerm origTerm (rev opcomm))))
bulwahn@34965
   267
       then
bulwahn@34965
   268
         let 
bulwahn@34965
   269
           val Const(name,_) = (getSubTerm origTerm (rev opcomm))
bulwahn@34965
   270
         in
bulwahn@46332
   271
           member (op =) commutatives name
bulwahn@34965
   272
         end
bulwahn@34965
   273
       else false
bulwahn@34965
   274
     end
bulwahn@34965
   275
   end;
bulwahn@34965
   276
bulwahn@34965
   277
bulwahn@34965
   278
(*Canonizes term t with the commutative operators stored in list 
bulwahn@34965
   279
commutatives*)
bulwahn@34965
   280
bulwahn@34965
   281
fun canonize_term (Const (s, T) $ t $ u) comms =
bulwahn@34965
   282
 let
bulwahn@34965
   283
   val t' = canonize_term t comms;
bulwahn@34965
   284
   val u' = canonize_term u comms;
bulwahn@34965
   285
 in 
haftmann@36692
   286
   if member (op =) comms s andalso Term_Ord.termless (u', t')
bulwahn@34965
   287
   then Const (s, T) $ u' $ t'
bulwahn@34965
   288
   else Const (s, T) $ t' $ u'
bulwahn@34965
   289
 end
bulwahn@34965
   290
 | canonize_term (t $ u) comms = canonize_term t comms $ canonize_term u comms
bulwahn@34965
   291
 | canonize_term (Abs (s, T, t)) comms = Abs (s, T, canonize_term t comms)
bulwahn@34965
   292
 | canonize_term t comms = t;
bulwahn@34965
   293
bulwahn@34965
   294
bulwahn@34965
   295
(*inspect the passed list and mutate origTerm following the elements of the list:
bulwahn@34965
   296
if the path of the current element is [5] (dummy path), the term has been found in the signature 
bulwahn@34965
   297
and the subterm will be substituted by it
bulwahn@34965
   298
else the term has been found in the original term and the two subterms have to be exchanged
bulwahn@34965
   299
The additional parameter commutatives indicates the commutative operators  
bulwahn@34965
   300
in the term whose operands won't be exchanged*)
bulwahn@34965
   301
bulwahn@34965
   302
fun createMutatedTerms origTerm _ [] commutatives mutatedTerms = mutatedTerms
bulwahn@34965
   303
 | createMutatedTerms origTerm (hdt as (hdTerm,hdabsContext,hdminContext,hdPath))
bulwahn@34965
   304
   ((sndTerm,sndabsContext,sndminContext,sndPath)::xs) commutatives mutatedTerms = 
bulwahn@34965
   305
   if (sndPath = [5])
bulwahn@34965
   306
   then
bulwahn@34965
   307
     let 
bulwahn@34965
   308
         val canonized = canonize_term (substitute (rev hdPath) origTerm sndTerm) commutatives
bulwahn@34965
   309
       in
bulwahn@34965
   310
         if (canonized = origTerm)  
bulwahn@34965
   311
         then createMutatedTerms origTerm hdt xs commutatives mutatedTerms
bulwahn@34965
   312
         else createMutatedTerms origTerm hdt xs commutatives 
bulwahn@34965
   313
           (insert op aconv canonized mutatedTerms)
bulwahn@34965
   314
       end
bulwahn@34965
   315
     else 
bulwahn@34965
   316
       if ((areCommutative origTerm hdPath sndPath commutatives)
bulwahn@34965
   317
         orelse (areCommutative origTerm sndPath hdPath commutatives)) 
bulwahn@34965
   318
       then createMutatedTerms origTerm hdt xs commutatives mutatedTerms
bulwahn@34965
   319
       else
bulwahn@34965
   320
         let 
bulwahn@34965
   321
           val canonized = canonize_term 
bulwahn@34965
   322
             (replace origTerm
bulwahn@34965
   323
                (incr_boundvars (length sndabsContext - length hdminContext) hdTerm,
bulwahn@34965
   324
                 hdPath)
bulwahn@34965
   325
                (incr_boundvars (length hdabsContext - length sndminContext) sndTerm,
bulwahn@34965
   326
                 sndPath)) commutatives
bulwahn@34965
   327
         in
bulwahn@34965
   328
           if (not(canonized = origTerm)) 
bulwahn@34965
   329
           then createMutatedTerms origTerm hdt xs commutatives 
bulwahn@34965
   330
             (insert op aconv canonized mutatedTerms)
bulwahn@34965
   331
           else createMutatedTerms origTerm hdt xs commutatives mutatedTerms
bulwahn@34965
   332
         end;
bulwahn@34965
   333
bulwahn@34965
   334
bulwahn@34965
   335
bulwahn@34965
   336
(*mutates origTerm by exchanging subterms. The mutated terms are returned in a term list
bulwahn@34965
   337
The parameter commutatives consists of a list of commutative operators. The permutation of their 
bulwahn@34965
   338
operands won't be considered as a new term
bulwahn@34965
   339
!!!Attention!!!: The given origTerm must be canonized. Use function canonize_term!*)
bulwahn@34965
   340
bulwahn@34965
   341
fun mutate_once option origTerm tsig commutatives forbidden_funs= 
bulwahn@34965
   342
 let 
bulwahn@34965
   343
   val subTermList = getSubTermList origTerm [] [] []
bulwahn@34965
   344
 in
bulwahn@34965
   345
   let 
bulwahn@34965
   346
     fun replaceRecursively [] mutatedTerms = mutatedTerms
bulwahn@34965
   347
       | replaceRecursively ((hdTerm,hdType,hdabsContext,hdminContext,hdPath)::tail) 
bulwahn@34965
   348
         mutatedTerms =
bulwahn@34965
   349
         replaceRecursively tail (union op aconv (createMutatedTerms origTerm 
bulwahn@34965
   350
           (hdTerm,hdabsContext,hdminContext,hdPath) 
bulwahn@34965
   351
           (searchForMutatableTerm option (hdTerm,hdType,hdabsContext,hdminContext,hdPath) 
bulwahn@34965
   352
             tail tsig [] forbidden_funs) 
bulwahn@34965
   353
           commutatives []) mutatedTerms)
bulwahn@34965
   354
   in
bulwahn@34965
   355
     replaceRecursively subTermList []
bulwahn@34965
   356
   end
bulwahn@34965
   357
 end;
bulwahn@34965
   358
bulwahn@34965
   359
bulwahn@34965
   360
bulwahn@34965
   361
bulwahn@34965
   362
(*helper function in order to apply recursively the mutate_once function on a whole list of terms
bulwahn@34965
   363
Needed for the mutate function*)
bulwahn@34965
   364
bulwahn@34965
   365
fun mutate_once_rec option [] tsig commutatives forbidden_funs acc = acc
bulwahn@34965
   366
 | mutate_once_rec option (x::xs) tsig commutatives forbidden_funs acc = 
bulwahn@34965
   367
   mutate_once_rec option xs tsig commutatives forbidden_funs 
bulwahn@34965
   368
     (union op aconv (mutate_once option x tsig commutatives forbidden_funs) acc);
bulwahn@34965
   369
bulwahn@34965
   370
bulwahn@34965
   371
bulwahn@34965
   372
(*apply function mutate_once iter times on the given origTerm. *)
bulwahn@34965
   373
(*call of mutiere with canonized form of origTerm. Prevents us of the computation of
bulwahn@34965
   374
canonization in the course of insertion of new terms!*)
bulwahn@34965
   375
bulwahn@34965
   376
fun mutate option origTerm tsig commutatives forbidden_funs 0 = []
bulwahn@34965
   377
 | mutate option origTerm tsig commutatives forbidden_funs 1 = 
bulwahn@34965
   378
   mutate_once option (canonize_term origTerm commutatives) tsig commutatives forbidden_funs
bulwahn@34965
   379
 | mutate option origTerm tsig commutatives forbidden_funs iter = 
bulwahn@34965
   380
   mutate_once_rec option (mutate option origTerm tsig commutatives forbidden_funs (iter-1)) 
bulwahn@34965
   381
     tsig commutatives forbidden_funs []; 
bulwahn@34965
   382
bulwahn@34965
   383
(*mutate origTerm iter times by only exchanging subterms*)
bulwahn@34965
   384
bulwahn@34965
   385
fun mutate_exc origTerm commutatives iter =
wenzelm@37863
   386
 mutate 0 origTerm @{theory Main} commutatives [] iter;
bulwahn@34965
   387
bulwahn@34965
   388
bulwahn@34965
   389
(*mutate origTerm iter times by only inserting signature functions*)
bulwahn@34965
   390
bulwahn@34965
   391
fun mutate_sign origTerm tsig forbidden_funs iter = 
bulwahn@34965
   392
 mutate 1 origTerm tsig [] forbidden_funs iter;
bulwahn@34965
   393
bulwahn@34965
   394
bulwahn@34965
   395
(*mutate origTerm iter times by exchange of subterms and insertion of subterms*)
bulwahn@34965
   396
bulwahn@34965
   397
fun mutate_mix origTerm tsig commutatives forbidden_funs iter =
bulwahn@34965
   398
 mutate 2 origTerm tsig commutatives forbidden_funs iter;  
bulwahn@34965
   399
bulwahn@46332
   400
 
bulwahn@34965
   401
(*helper function for the quickcheck invocation. Evaluates the quickcheck_term function on a whole list of terms
bulwahn@34965
   402
and tries to print the exceptions*)
bulwahn@34965
   403
bulwahn@34965
   404
fun freeze (t $ u) = freeze t $ freeze u
bulwahn@34965
   405
 | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
bulwahn@34965
   406
 | freeze (Var ((a, i), T)) =
bulwahn@34965
   407
     Free (if i = 0 then a else a ^ "_" ^ string_of_int i, T)
bulwahn@34965
   408
 | freeze t = t;
bulwahn@34965
   409
bulwahn@34965
   410
end