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