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