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