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