src/HOL/Mutabelle/mutabelle.ML
author webertj
Fri, 19 Oct 2012 15:12:52 +0200
changeset 49962 a8cc904a6820
parent 47004 6f00d8a83eb7
child 51092 5e6398b48030
permissions -rw-r--r--
Renamed {left,right}_distrib to distrib_{right,left}.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37744
3daaf23b9ab4 tuned titles
haftmann
parents: 36743
diff changeset
     1
(*  Title:      HOL/Mutabelle/mutabelle.ML
34967
4b068e52ab3f Changed author; removed debugging code.
berghofe
parents: 34965
diff changeset
     2
    Author:     Veronika Ortner, TU Muenchen
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
     3
41408
08a072ca6348 tuned comments;
wenzelm
parents: 41067
diff changeset
     4
Mutation of theorems.
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
     5
*)
41408
08a072ca6348 tuned comments;
wenzelm
parents: 41067
diff changeset
     6
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
     7
signature MUTABELLE =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
     8
sig
43883
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 42429
diff changeset
     9
  exception WrongPath of string;
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 42429
diff changeset
    10
  exception WrongArg of string;
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 42429
diff changeset
    11
  val freeze : term -> term
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 42429
diff changeset
    12
  val mutate_exc : term -> string list -> int -> term list 
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 42429
diff changeset
    13
  val mutate_sign : term -> theory -> (string * string) list -> int -> term list 
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 42429
diff changeset
    14
  val mutate_mix : term -> theory -> string list -> 
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    15
   (string * string) list -> int -> term list
46332
f62f5f1fda3b removing dead code from Mutabelle; tuned
bulwahn
parents: 45428
diff changeset
    16
43883
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 42429
diff changeset
    17
  val all_unconcealed_thms_of : theory -> (string * thm) list
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    18
end;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    19
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    20
structure Mutabelle : MUTABELLE = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    21
struct
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    22
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    23
fun all_unconcealed_thms_of thy =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    24
  let
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 37863
diff changeset
    25
    val facts = Global_Theory.facts_of thy
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    26
  in
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    27
    Facts.fold_static
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    28
      (fn (s, ths) =>
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    29
        if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths))
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    30
      facts []
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    31
  end;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    32
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    33
fun thms_of thy = filter (fn (_, th) =>
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    34
   Context.theory_name (theory_of_thm th) = Context.theory_name thy) (all_unconcealed_thms_of thy);
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    35
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    36
fun consts_of thy =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    37
 let
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    38
   val (namespace, const_table) = #constants (Consts.dest (Sign.consts_of thy))
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    39
   val consts = Symtab.dest const_table
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    40
 in
42429
7691cc61720a standardized some ML aliases;
wenzelm
parents: 42361
diff changeset
    41
   map_filter (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    42
     (filter_out (fn (s, _) => Name_Space.is_concealed namespace s) consts)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    43
 end;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    44
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    45
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    46
(*thrown in case the specified path doesn't exist in the specified term*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    47
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    48
exception WrongPath of string;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    49
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    50
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    51
(*thrown in case the arguments did not fit to the function*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    52
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    53
exception WrongArg of string; 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    54
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    55
(*Rename the bound variables in a term with the minimal Index min of 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    56
bound variables. Variable (Bound(min)) will be renamed to Bound(0) etc. 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    57
This is needed in course auf evaluation of contexts.*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    58
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    59
fun rename_bnds curTerm 0 = curTerm
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    60
 | rename_bnds (Bound(i)) minInd = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    61
   let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    62
     val erg = if (i-minInd < 0) then 0 else (i - minInd)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    63
   in 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    64
     Bound(erg)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    65
   end
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    66
 | rename_bnds (Abs(name,t,uTerm)) minInd = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    67
   Abs(name,t,(rename_bnds uTerm minInd))
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    68
 | rename_bnds (fstUTerm $ sndUTerm) minInd =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    69
   (rename_bnds fstUTerm minInd) $ (rename_bnds sndUTerm minInd)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    70
 | rename_bnds elseTerm minInd = elseTerm;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    71
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    72
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    73
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    74
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    75
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    76
(*Partition a term in its subterms and create an entry 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    77
(term * type * abscontext * mincontext * path) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    78
for each term in the return list 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    79
e.g: getSubTermList Abs(y, int, Const(f,int->int) $ Const(x,int) $ Bound(0))
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    80
will give       [(Const(f,int->int),int->int,[int],[],[00]),
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    81
               (Const(x,int),int,[int],[],[010]),
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    82
               (Bound(0),int,[int],[int],[110]),
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    83
               (Const(x,int) $ Bound(0),type,[int],[int],[10]),
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    84
               (Const(f,int->int) $ Const(x,int) $ Bound(0),type,[int],[int],[0],
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    85
               (Abs (y,int,Const(f,int->int) $ const(x,int) $ Bound(0)),type,[],[],[])]
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    86
                *)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    87
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    88
fun getSubTermList (Const(name,t)) abscontext path acc =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    89
   (Const(name,t),t,abscontext,abscontext,path)::acc
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    90
 | getSubTermList (Free(name,t)) abscontext path acc =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    91
   (Free(name,t),t,abscontext,abscontext,path)::acc
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    92
 | getSubTermList (Var(indname,t)) abscontext path acc =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    93
   (Var(indname,t),t,abscontext,abscontext,path)::acc
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    94
 | getSubTermList (Bound(i)) abscontext path acc =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    95
   (Bound(0),nth abscontext i,abscontext, Library.drop i abscontext,path)::acc
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    96
 | getSubTermList (Abs(name,t,uTerm)) abscontext path acc = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    97
   let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    98
     val curTerm = Abs(name,t,uTerm)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    99
     val bnos = Term.add_loose_bnos (curTerm,0,[])
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   100
     val minInd = if (bnos = []) then 0 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   101
       else Library.foldl (fn (n,m) => if (n<m) then n else m) (hd bnos,tl bnos)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   102
     val newTerm = rename_bnds curTerm minInd
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   103
     val newContext = Library.drop minInd abscontext
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   104
   in 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   105
     getSubTermList uTerm (t::abscontext) (0::path) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   106
               ((newTerm,(fastype_of1 (abscontext, curTerm)),abscontext,newContext,path)::acc)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   107
   end
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   108
 | getSubTermList (fstUTerm $ sndUTerm) abscontext path acc = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   109
   let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   110
     val curTerm = (fstUTerm $ sndUTerm)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   111
     val bnos = Term.add_loose_bnos (curTerm, 0, [])
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   112
     val minInd = if (bnos = []) then 0
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   113
       else Library.foldl (fn (n,m) => if (n<m) then n else m) (hd bnos,tl bnos)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   114
     val newTerm = rename_bnds curTerm minInd
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   115
     val newContext = Library.drop minInd abscontext
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   116
   in 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   117
     getSubTermList fstUTerm abscontext (0::path) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   118
       (getSubTermList sndUTerm abscontext (1::path) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   119
         ((newTerm,(fastype_of1 (abscontext, curTerm)),abscontext,newContext,path)::acc)) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   120
   end;  
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   121
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   122
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   123
(*Evaluate if the longContext is more special as the shortContext. 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   124
If so, a term with shortContext can be substituted in the place of a 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   125
term with longContext*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   126
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   127
fun is_morespecial longContext shortContext = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   128
 let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   129
   val revlC = rev longContext
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   130
   val revsC = rev shortContext
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   131
   fun is_prefix [] longList = true
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   132
     | is_prefix shList [] = false
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   133
     | is_prefix (x::xs) (y::ys) = if (x=y) then is_prefix xs ys else false
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   134
 in 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   135
   is_prefix revsC revlC
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   136
 end;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   137
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   138
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   139
(*takes a (term * type * context * context * path)-tupel and searches in the specified list for 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   140
terms with the same type and appropriate context. Returns a (term * path) list of these terms.
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   141
Used in order to generate a list of type-equal subterms of the original term*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   142
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   143
fun searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) [] resultList = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   144
   resultList
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   145
 | searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   146
   ((hdterm,hdtype,hdabsContext,hdminContext,hdpath)::xs) resultList = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   147
   if ((stype = hdtype) andalso (is_morespecial sabsContext hdminContext) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   148
     andalso (is_morespecial hdabsContext sminContext)) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   149
   then searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) xs 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   150
     ((hdterm,hdabsContext,hdminContext,hdpath)::resultList) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   151
   else searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) xs resultList;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   152
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   153
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   154
(*evaluates if the given function is in the passed list of forbidden functions*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   155
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   156
fun in_list_forb consSig (consNameStr,consType) [] = false
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   157
 | in_list_forb consSig (consNameStr,consType) ((forbNameStr,forbTypeStr)::xs) = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   158
   let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   159
     val forbType = Syntax.read_typ_global consSig forbTypeStr
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   160
   in
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   161
     if ((consNameStr = forbNameStr) 
47004
wenzelm
parents: 46479
diff changeset
   162
       andalso (Sign.typ_instance consSig (consType,(Logic.varifyT_global forbType))))
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   163
     then true
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   164
     else in_list_forb consSig (consNameStr,consType) xs
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   165
   end;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   166
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   167
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   168
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   169
(*searches in the given signature Consts with the same type as sterm and 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   170
returns a list of those terms*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   171
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   172
fun searchForSignatureMutations (sterm,stype) consSig forbidden_funs = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   173
 let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   174
   val sigConsTypeList = consts_of consSig;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   175
 in 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   176
   let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   177
     fun recursiveSearch mutatableTermList [] = mutatableTermList
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   178
       | recursiveSearch mutatableTermList ((ConsName,ConsType)::xs) = 
47004
wenzelm
parents: 46479
diff changeset
   179
         if (Sign.typ_instance consSig (stype,ConsType) 
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   180
           andalso (not (sterm = Const(ConsName,stype))) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   181
           andalso (not (in_list_forb consSig (ConsName,ConsType) forbidden_funs))) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   182
         then recursiveSearch ((Term.Const(ConsName,stype), [], [], [5])::mutatableTermList) xs
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   183
         else recursiveSearch mutatableTermList xs
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   184
     in
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   185
       recursiveSearch [] sigConsTypeList
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   186
     end
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   187
   end;     
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   188
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   189
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   190
(*generates a list of terms that can be used instead of the passed subterm in the original term. These terms either have
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   191
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
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   192
in the current signature.
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   193
This function has 3 versions:
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   194
0: no instertion of signature functions, 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   195
  only terms in the subTermList with the same type and appropriate context as the passed term are returned
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   196
1: no exchange of subterms,
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   197
  only signature functions are inserted at the place of type-aequivalent Conses
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   198
2: mixture of the two other versions. insertion of signature functions and exchange of subterms*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   199
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   200
fun searchForMutatableTerm 0 (sterm,stype,sabscontext,smincontext,spath) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   201
   subTerms consSig resultList forbidden_funs =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   202
   searchForMutatableSubTerm (sterm,stype,sabscontext,smincontext,spath) subTerms resultList
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   203
 | searchForMutatableTerm 1 (Const(constName,constType),stype,sabscontext,smincontext,spath) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   204
   subTerms consSig resultList forbidden_funs = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   205
   searchForSignatureMutations (Const(constName,constType),stype) consSig forbidden_funs
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   206
 | searchForMutatableTerm 1 _ _ _ _ _ = []
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   207
 | searchForMutatableTerm 2 (Const(constName,constType),stype,sabscontext,smincontext,spath) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   208
   subTerms consSig resultList forbidden_funs = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   209
     let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   210
       val subtermMutations = searchForMutatableSubTerm 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   211
         (Const(constName,constType),stype,sabscontext,smincontext,spath) subTerms resultList
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   212
       val signatureMutations = searchForSignatureMutations 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   213
         (Const(constName,constType),stype) consSig forbidden_funs
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   214
     in
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   215
       subtermMutations@signatureMutations
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   216
     end
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   217
 | searchForMutatableTerm 2 (sterm,stype,sabscontext,smincontext,spath) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   218
   subTerms consSig resultList forbidden_funs =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   219
   searchForMutatableSubTerm (sterm,stype,sabscontext,smincontext,spath) subTerms resultList
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   220
 | searchForMutatableTerm i _ _ _ _ _ = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   221
   raise WrongArg("Version " ^ string_of_int i ^ 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   222
     " doesn't exist for function searchForMutatableTerm!") ;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   223
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   224
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   225
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   226
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   227
(*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*)  
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   228
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   229
fun areReplacable [] [] = false
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   230
 | areReplacable fstPath [] = false
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   231
 | areReplacable [] sndPath = false
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   232
 | areReplacable (x::xs) (y::ys) = if (x=y) then areReplacable xs ys else true; 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   233
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   234
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   235
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   236
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   237
(*substitutes the term at the position of the first list in fstTerm by sndTerm. 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   238
The lists represent paths as generated by createSubTermList*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   239
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   240
fun substitute [] fstTerm sndTerm = sndTerm
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   241
 | substitute (_::xs) (Abs(s,T,subTerm)) sndTerm = Abs(s,T,(substitute xs subTerm sndTerm))
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   242
 | substitute (0::xs) (t $ u) sndTerm = substitute xs t sndTerm $ u 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   243
 | substitute (1::xs) (t $ u) sndTerm = t $ substitute xs u sndTerm
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   244
 | substitute (_::xs) _ sndTerm = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   245
   raise WrongPath ("The Term could not be found at the specified position"); 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   246
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   247
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   248
(*get the subterm with the specified path in myTerm*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   249
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   250
fun getSubTerm myTerm [] = myTerm
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   251
 | getSubTerm (Abs(s,T,subTerm)) (0::xs) = getSubTerm subTerm xs
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   252
 | getSubTerm (t $ u) (0::xs) = getSubTerm t xs
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   253
 | getSubTerm (t $ u) (1::xs) = getSubTerm u xs
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   254
 | getSubTerm _ (_::xs) = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   255
   raise WrongPath ("The subterm could not be found at the specified position");
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   256
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   257
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   258
(*exchanges two subterms with the given paths in the original Term*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   259
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   260
fun replace origTerm (fstTerm, fstPath) (sndTerm, sndPath) = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   261
 if (areReplacable (rev fstPath) (rev sndPath))
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   262
 then substitute (rev sndPath) (substitute (rev fstPath) origTerm sndTerm) fstTerm
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   263
 else origTerm; 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   264
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   265
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   266
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   267
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   268
(*tests if the terms with the given pathes in the origTerm are commutative
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   269
respecting the list of commutative operators (commutatives)*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   270
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   271
fun areCommutative origTerm fstPath sndPath commutatives =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   272
 if (sndPath = []) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   273
 then false
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   274
 else
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   275
   let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   276
     val base = (tl sndPath)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   277
   in
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   278
     let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   279
       val fstcomm = 1::0::base
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   280
       val opcomm = 0::0::base
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   281
     in
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   282
       if ((fstPath = fstcomm) andalso (is_Const (getSubTerm origTerm (rev opcomm))))
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   283
       then
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   284
         let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   285
           val Const(name,_) = (getSubTerm origTerm (rev opcomm))
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   286
         in
46332
f62f5f1fda3b removing dead code from Mutabelle; tuned
bulwahn
parents: 45428
diff changeset
   287
           member (op =) commutatives name
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   288
         end
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   289
       else false
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   290
     end
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   291
   end;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   292
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   293
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   294
(*Canonizes term t with the commutative operators stored in list 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   295
commutatives*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   296
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   297
fun canonize_term (Const (s, T) $ t $ u) comms =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   298
 let
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   299
   val t' = canonize_term t comms;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   300
   val u' = canonize_term u comms;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   301
 in 
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
   302
   if member (op =) comms s andalso Term_Ord.termless (u', t')
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   303
   then Const (s, T) $ u' $ t'
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   304
   else Const (s, T) $ t' $ u'
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   305
 end
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   306
 | canonize_term (t $ u) comms = canonize_term t comms $ canonize_term u comms
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   307
 | canonize_term (Abs (s, T, t)) comms = Abs (s, T, canonize_term t comms)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   308
 | canonize_term t comms = t;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   309
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   310
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   311
(*inspect the passed list and mutate origTerm following the elements of the list:
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   312
if the path of the current element is [5] (dummy path), the term has been found in the signature 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   313
and the subterm will be substituted by it
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   314
else the term has been found in the original term and the two subterms have to be exchanged
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   315
The additional parameter commutatives indicates the commutative operators  
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   316
in the term whose operands won't be exchanged*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   317
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   318
fun createMutatedTerms origTerm _ [] commutatives mutatedTerms = mutatedTerms
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   319
 | createMutatedTerms origTerm (hdt as (hdTerm,hdabsContext,hdminContext,hdPath))
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   320
   ((sndTerm,sndabsContext,sndminContext,sndPath)::xs) commutatives mutatedTerms = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   321
   if (sndPath = [5])
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   322
   then
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   323
     let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   324
         val canonized = canonize_term (substitute (rev hdPath) origTerm sndTerm) commutatives
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   325
       in
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   326
         if (canonized = origTerm)  
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   327
         then createMutatedTerms origTerm hdt xs commutatives mutatedTerms
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   328
         else createMutatedTerms origTerm hdt xs commutatives 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   329
           (insert op aconv canonized mutatedTerms)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   330
       end
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   331
     else 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   332
       if ((areCommutative origTerm hdPath sndPath commutatives)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   333
         orelse (areCommutative origTerm sndPath hdPath commutatives)) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   334
       then createMutatedTerms origTerm hdt xs commutatives mutatedTerms
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   335
       else
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   336
         let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   337
           val canonized = canonize_term 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   338
             (replace origTerm
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   339
                (incr_boundvars (length sndabsContext - length hdminContext) hdTerm,
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   340
                 hdPath)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   341
                (incr_boundvars (length hdabsContext - length sndminContext) sndTerm,
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   342
                 sndPath)) commutatives
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   343
         in
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   344
           if (not(canonized = origTerm)) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   345
           then createMutatedTerms origTerm hdt xs commutatives 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   346
             (insert op aconv canonized mutatedTerms)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   347
           else createMutatedTerms origTerm hdt xs commutatives mutatedTerms
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   348
         end;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   349
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   350
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   351
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   352
(*mutates origTerm by exchanging subterms. The mutated terms are returned in a term list
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   353
The parameter commutatives consists of a list of commutative operators. The permutation of their 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   354
operands won't be considered as a new term
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   355
!!!Attention!!!: The given origTerm must be canonized. Use function canonize_term!*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   356
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   357
fun mutate_once option origTerm tsig commutatives forbidden_funs= 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   358
 let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   359
   val subTermList = getSubTermList origTerm [] [] []
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   360
 in
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   361
   let 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   362
     fun replaceRecursively [] mutatedTerms = mutatedTerms
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   363
       | replaceRecursively ((hdTerm,hdType,hdabsContext,hdminContext,hdPath)::tail) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   364
         mutatedTerms =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   365
         replaceRecursively tail (union op aconv (createMutatedTerms origTerm 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   366
           (hdTerm,hdabsContext,hdminContext,hdPath) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   367
           (searchForMutatableTerm option (hdTerm,hdType,hdabsContext,hdminContext,hdPath) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   368
             tail tsig [] forbidden_funs) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   369
           commutatives []) mutatedTerms)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   370
   in
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   371
     replaceRecursively subTermList []
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   372
   end
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   373
 end;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   374
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   375
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   376
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   377
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   378
(*helper function in order to apply recursively the mutate_once function on a whole list of terms
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   379
Needed for the mutate function*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   380
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   381
fun mutate_once_rec option [] tsig commutatives forbidden_funs acc = acc
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   382
 | mutate_once_rec option (x::xs) tsig commutatives forbidden_funs acc = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   383
   mutate_once_rec option xs tsig commutatives forbidden_funs 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   384
     (union op aconv (mutate_once option x tsig commutatives forbidden_funs) acc);
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   385
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   386
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   387
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   388
(*apply function mutate_once iter times on the given origTerm. *)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   389
(*call of mutiere with canonized form of origTerm. Prevents us of the computation of
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   390
canonization in the course of insertion of new terms!*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   391
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   392
fun mutate option origTerm tsig commutatives forbidden_funs 0 = []
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   393
 | mutate option origTerm tsig commutatives forbidden_funs 1 = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   394
   mutate_once option (canonize_term origTerm commutatives) tsig commutatives forbidden_funs
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   395
 | mutate option origTerm tsig commutatives forbidden_funs iter = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   396
   mutate_once_rec option (mutate option origTerm tsig commutatives forbidden_funs (iter-1)) 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   397
     tsig commutatives forbidden_funs []; 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   398
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   399
(*mutate origTerm iter times by only exchanging subterms*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   400
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   401
fun mutate_exc origTerm commutatives iter =
37863
7f113caabcf4 discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
wenzelm
parents: 37744
diff changeset
   402
 mutate 0 origTerm @{theory Main} commutatives [] iter;
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   403
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   404
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   405
(*mutate origTerm iter times by only inserting signature functions*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   406
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   407
fun mutate_sign origTerm tsig forbidden_funs iter = 
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   408
 mutate 1 origTerm tsig [] forbidden_funs iter;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   409
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   410
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   411
(*mutate origTerm iter times by exchange of subterms and insertion of subterms*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   412
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   413
fun mutate_mix origTerm tsig commutatives forbidden_funs iter =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   414
 mutate 2 origTerm tsig commutatives forbidden_funs iter;  
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   415
46332
f62f5f1fda3b removing dead code from Mutabelle; tuned
bulwahn
parents: 45428
diff changeset
   416
 
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   417
(*helper function for the quickcheck invocation. Evaluates the quickcheck_term function on a whole list of terms
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   418
and tries to print the exceptions*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   419
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   420
fun freeze (t $ u) = freeze t $ freeze u
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   421
 | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   422
 | freeze (Var ((a, i), T)) =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   423
     Free (if i = 0 then a else a ^ "_" ^ string_of_int i, T)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   424
 | freeze t = t;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   425
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   426
fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   427
 | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T);
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   428
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35408
diff changeset
   429
fun preprocess thy insts t = Object_Logic.atomize_term thy
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   430
 (map_types (inst_type insts) (freeze t));
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   431
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   432
fun is_executable thy insts th =
43883
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 42429
diff changeset
   433
  let
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 42429
diff changeset
   434
    val ctxt' = Proof_Context.init_global thy
40920
977c60b622f4 adapting mutabelle
bulwahn
parents: 40906
diff changeset
   435
      |> Config.put Quickcheck.size 1
977c60b622f4 adapting mutabelle
bulwahn
parents: 40906
diff changeset
   436
      |> Config.put Quickcheck.iterations 1
45428
aa35c9454a95 quickcheck invocations in mutabelle must not catch codegenerator errors internally
bulwahn
parents: 45159
diff changeset
   437
    val test = Quickcheck_Common.test_term
46332
f62f5f1fda3b removing dead code from Mutabelle; tuned
bulwahn
parents: 45428
diff changeset
   438
      ("exhaustive", ((fn _ => raise (Fail "")), Exhaustive_Generators.compile_generator_expr)) ctxt' false
43883
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 42429
diff changeset
   439
  in  
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 42429
diff changeset
   440
    case try test (preprocess thy insts (prop_of th), []) of
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 42429
diff changeset
   441
      SOME _ => (Output.urgent_message "executable"; true)
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 42429
diff changeset
   442
    | NONE => (Output.urgent_message ("not executable"); false)
46332
f62f5f1fda3b removing dead code from Mutabelle; tuned
bulwahn
parents: 45428
diff changeset
   443
  end;                                               
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   444
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   445
end