author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 47004  6f00d8a83eb7 
child 51092  5e6398b48030 
permissions  rwrr 
37744  1 
(* Title: HOL/Mutabelle/mutabelle.ML 
34967  2 
Author: Veronika Ortner, TU Muenchen 
34965  3 

41408  4 
Mutation of theorems. 
34965  5 
*) 
41408  6 

34965  7 
signature MUTABELLE = 
8 
sig 

43883
aacbe67793c3
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents:
42429
diff
changeset

9 
exception WrongPath of string; 
aacbe67793c3
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents:
42429
diff
changeset

10 
exception WrongArg of string; 
aacbe67793c3
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents:
42429
diff
changeset

11 
val freeze : term > term 
aacbe67793c3
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents:
42429
diff
changeset

12 
val mutate_exc : term > string list > int > term list 
aacbe67793c3
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents:
42429
diff
changeset

13 
val mutate_sign : term > theory > (string * string) list > int > term list 
aacbe67793c3
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents:
42429
diff
changeset

14 
val mutate_mix : term > theory > string list > 
34965  15 
(string * string) list > int > term list 
46332  16 

43883
aacbe67793c3
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents:
42429
diff
changeset

17 
val all_unconcealed_thms_of : theory > (string * thm) list 
34965  18 
end; 
19 

20 
structure Mutabelle : MUTABELLE = 

21 
struct 

22 

23 
fun all_unconcealed_thms_of thy = 

24 
let 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37863
diff
changeset

25 
val facts = Global_Theory.facts_of thy 
34965  26 
in 
27 
Facts.fold_static 

28 
(fn (s, ths) => 

29 
if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths)) 

30 
facts [] 

31 
end; 

32 

33 
fun thms_of thy = filter (fn (_, th) => 

34 
Context.theory_name (theory_of_thm th) = Context.theory_name thy) (all_unconcealed_thms_of thy); 

35 

36 
fun consts_of thy = 

37 
let 

38 
val (namespace, const_table) = #constants (Consts.dest (Sign.consts_of thy)) 

39 
val consts = Symtab.dest const_table 

40 
in 

42429  41 
map_filter (fn (s, (T, NONE)) => SOME (s, T)  _ => NONE) 
34965  42 
(filter_out (fn (s, _) => Name_Space.is_concealed namespace s) consts) 
43 
end; 

44 

45 

46 
(*thrown in case the specified path doesn't exist in the specified term*) 

47 

48 
exception WrongPath of string; 

49 

50 

51 
(*thrown in case the arguments did not fit to the function*) 

52 

53 
exception WrongArg of string; 

54 

55 
(*Rename the bound variables in a term with the minimal Index min of 

56 
bound variables. Variable (Bound(min)) will be renamed to Bound(0) etc. 

57 
This is needed in course auf evaluation of contexts.*) 

58 

59 
fun rename_bnds curTerm 0 = curTerm 

60 
 rename_bnds (Bound(i)) minInd = 

61 
let 

62 
val erg = if (iminInd < 0) then 0 else (i  minInd) 

63 
in 

64 
Bound(erg) 

65 
end 

66 
 rename_bnds (Abs(name,t,uTerm)) minInd = 

67 
Abs(name,t,(rename_bnds uTerm minInd)) 

68 
 rename_bnds (fstUTerm $ sndUTerm) minInd = 

69 
(rename_bnds fstUTerm minInd) $ (rename_bnds sndUTerm minInd) 

70 
 rename_bnds elseTerm minInd = elseTerm; 

71 

72 

73 

74 

75 

76 
(*Partition a term in its subterms and create an entry 

77 
(term * type * abscontext * mincontext * path) 

78 
for each term in the return list 

79 
e.g: getSubTermList Abs(y, int, Const(f,int>int) $ Const(x,int) $ Bound(0)) 

80 
will give [(Const(f,int>int),int>int,[int],[],[00]), 

81 
(Const(x,int),int,[int],[],[010]), 

82 
(Bound(0),int,[int],[int],[110]), 

83 
(Const(x,int) $ Bound(0),type,[int],[int],[10]), 

84 
(Const(f,int>int) $ Const(x,int) $ Bound(0),type,[int],[int],[0], 

85 
(Abs (y,int,Const(f,int>int) $ const(x,int) $ Bound(0)),type,[],[],[])] 

86 
*) 

87 

88 
fun getSubTermList (Const(name,t)) abscontext path acc = 

89 
(Const(name,t),t,abscontext,abscontext,path)::acc 

90 
 getSubTermList (Free(name,t)) abscontext path acc = 

91 
(Free(name,t),t,abscontext,abscontext,path)::acc 

92 
 getSubTermList (Var(indname,t)) abscontext path acc = 

93 
(Var(indname,t),t,abscontext,abscontext,path)::acc 

94 
 getSubTermList (Bound(i)) abscontext path acc = 

95 
(Bound(0),nth abscontext i,abscontext, Library.drop i abscontext,path)::acc 

96 
 getSubTermList (Abs(name,t,uTerm)) abscontext path acc = 

97 
let 

98 
val curTerm = Abs(name,t,uTerm) 

99 
val bnos = Term.add_loose_bnos (curTerm,0,[]) 

100 
val minInd = if (bnos = []) then 0 

101 
else Library.foldl (fn (n,m) => if (n<m) then n else m) (hd bnos,tl bnos) 

102 
val newTerm = rename_bnds curTerm minInd 

103 
val newContext = Library.drop minInd abscontext 

104 
in 

105 
getSubTermList uTerm (t::abscontext) (0::path) 

106 
((newTerm,(fastype_of1 (abscontext, curTerm)),abscontext,newContext,path)::acc) 

107 
end 

108 
 getSubTermList (fstUTerm $ sndUTerm) abscontext path acc = 

109 
let 

110 
val curTerm = (fstUTerm $ sndUTerm) 

111 
val bnos = Term.add_loose_bnos (curTerm, 0, []) 

112 
val minInd = if (bnos = []) then 0 

113 
else Library.foldl (fn (n,m) => if (n<m) then n else m) (hd bnos,tl bnos) 

114 
val newTerm = rename_bnds curTerm minInd 

115 
val newContext = Library.drop minInd abscontext 

116 
in 

117 
getSubTermList fstUTerm abscontext (0::path) 

118 
(getSubTermList sndUTerm abscontext (1::path) 

119 
((newTerm,(fastype_of1 (abscontext, curTerm)),abscontext,newContext,path)::acc)) 

120 
end; 

121 

122 

123 
(*Evaluate if the longContext is more special as the shortContext. 

124 
If so, a term with shortContext can be substituted in the place of a 

125 
term with longContext*) 

126 

127 
fun is_morespecial longContext shortContext = 

128 
let 

129 
val revlC = rev longContext 

130 
val revsC = rev shortContext 

131 
fun is_prefix [] longList = true 

132 
 is_prefix shList [] = false 

133 
 is_prefix (x::xs) (y::ys) = if (x=y) then is_prefix xs ys else false 

134 
in 

135 
is_prefix revsC revlC 

136 
end; 

137 

138 

139 
(*takes a (term * type * context * context * path)tupel and searches in the specified list for 

140 
terms with the same type and appropriate context. Returns a (term * path) list of these terms. 

141 
Used in order to generate a list of typeequal subterms of the original term*) 

142 

143 
fun searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) [] resultList = 

144 
resultList 

145 
 searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) 

146 
((hdterm,hdtype,hdabsContext,hdminContext,hdpath)::xs) resultList = 

147 
if ((stype = hdtype) andalso (is_morespecial sabsContext hdminContext) 

148 
andalso (is_morespecial hdabsContext sminContext)) 

149 
then searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) xs 

150 
((hdterm,hdabsContext,hdminContext,hdpath)::resultList) 

151 
else searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) xs resultList; 

152 

153 

154 
(*evaluates if the given function is in the passed list of forbidden functions*) 

155 

156 
fun in_list_forb consSig (consNameStr,consType) [] = false 

157 
 in_list_forb consSig (consNameStr,consType) ((forbNameStr,forbTypeStr)::xs) = 

158 
let 

159 
val forbType = Syntax.read_typ_global consSig forbTypeStr 

160 
in 

161 
if ((consNameStr = forbNameStr) 

47004  162 
andalso (Sign.typ_instance consSig (consType,(Logic.varifyT_global forbType)))) 
34965  163 
then true 
164 
else in_list_forb consSig (consNameStr,consType) xs 

165 
end; 

166 

167 

168 

169 
(*searches in the given signature Consts with the same type as sterm and 

170 
returns a list of those terms*) 

171 

172 
fun searchForSignatureMutations (sterm,stype) consSig forbidden_funs = 

173 
let 

174 
val sigConsTypeList = consts_of consSig; 

175 
in 

176 
let 

177 
fun recursiveSearch mutatableTermList [] = mutatableTermList 

178 
 recursiveSearch mutatableTermList ((ConsName,ConsType)::xs) = 

47004  179 
if (Sign.typ_instance consSig (stype,ConsType) 
34965  180 
andalso (not (sterm = Const(ConsName,stype))) 
181 
andalso (not (in_list_forb consSig (ConsName,ConsType) forbidden_funs))) 

182 
then recursiveSearch ((Term.Const(ConsName,stype), [], [], [5])::mutatableTermList) xs 

183 
else recursiveSearch mutatableTermList xs 

184 
in 

185 
recursiveSearch [] sigConsTypeList 

186 
end 

187 
end; 

188 

189 

190 
(*generates a list of terms that can be used instead of the passed subterm in the original term. These terms either have 

191 
the same type and appropriate context and are generated from the list of subterms either  in case of a Constterm they have been found 

192 
in the current signature. 

193 
This function has 3 versions: 

194 
0: no instertion of signature functions, 

195 
only terms in the subTermList with the same type and appropriate context as the passed term are returned 

196 
1: no exchange of subterms, 

197 
only signature functions are inserted at the place of typeaequivalent Conses 

198 
2: mixture of the two other versions. insertion of signature functions and exchange of subterms*) 

199 

200 
fun searchForMutatableTerm 0 (sterm,stype,sabscontext,smincontext,spath) 

201 
subTerms consSig resultList forbidden_funs = 

202 
searchForMutatableSubTerm (sterm,stype,sabscontext,smincontext,spath) subTerms resultList 

203 
 searchForMutatableTerm 1 (Const(constName,constType),stype,sabscontext,smincontext,spath) 

204 
subTerms consSig resultList forbidden_funs = 

205 
searchForSignatureMutations (Const(constName,constType),stype) consSig forbidden_funs 

206 
 searchForMutatableTerm 1 _ _ _ _ _ = [] 

207 
 searchForMutatableTerm 2 (Const(constName,constType),stype,sabscontext,smincontext,spath) 

208 
subTerms consSig resultList forbidden_funs = 

209 
let 

210 
val subtermMutations = searchForMutatableSubTerm 

211 
(Const(constName,constType),stype,sabscontext,smincontext,spath) subTerms resultList 

212 
val signatureMutations = searchForSignatureMutations 

213 
(Const(constName,constType),stype) consSig forbidden_funs 

214 
in 

215 
subtermMutations@signatureMutations 

216 
end 

217 
 searchForMutatableTerm 2 (sterm,stype,sabscontext,smincontext,spath) 

218 
subTerms consSig resultList forbidden_funs = 

219 
searchForMutatableSubTerm (sterm,stype,sabscontext,smincontext,spath) subTerms resultList 

220 
 searchForMutatableTerm i _ _ _ _ _ = 

221 
raise WrongArg("Version " ^ string_of_int i ^ 

222 
" doesn't exist for function searchForMutatableTerm!") ; 

223 

224 

225 

226 

227 
(*evaluates if the two terms with paths passed as arguments can be exchanged, i.e. evaluates if one of the terms is a subterm of the other one*) 

228 

229 
fun areReplacable [] [] = false 

230 
 areReplacable fstPath [] = false 

231 
 areReplacable [] sndPath = false 

232 
 areReplacable (x::xs) (y::ys) = if (x=y) then areReplacable xs ys else true; 

233 

234 

235 

236 

237 
(*substitutes the term at the position of the first list in fstTerm by sndTerm. 

238 
The lists represent paths as generated by createSubTermList*) 

239 

240 
fun substitute [] fstTerm sndTerm = sndTerm 

241 
 substitute (_::xs) (Abs(s,T,subTerm)) sndTerm = Abs(s,T,(substitute xs subTerm sndTerm)) 

242 
 substitute (0::xs) (t $ u) sndTerm = substitute xs t sndTerm $ u 

243 
 substitute (1::xs) (t $ u) sndTerm = t $ substitute xs u sndTerm 

244 
 substitute (_::xs) _ sndTerm = 

245 
raise WrongPath ("The Term could not be found at the specified position"); 

246 

247 

248 
(*get the subterm with the specified path in myTerm*) 

249 

250 
fun getSubTerm myTerm [] = myTerm 

251 
 getSubTerm (Abs(s,T,subTerm)) (0::xs) = getSubTerm subTerm xs 

252 
 getSubTerm (t $ u) (0::xs) = getSubTerm t xs 

253 
 getSubTerm (t $ u) (1::xs) = getSubTerm u xs 

254 
 getSubTerm _ (_::xs) = 

255 
raise WrongPath ("The subterm could not be found at the specified position"); 

256 

257 

258 
(*exchanges two subterms with the given paths in the original Term*) 

259 

260 
fun replace origTerm (fstTerm, fstPath) (sndTerm, sndPath) = 

261 
if (areReplacable (rev fstPath) (rev sndPath)) 

262 
then substitute (rev sndPath) (substitute (rev fstPath) origTerm sndTerm) fstTerm 

263 
else origTerm; 

264 

265 

266 

267 

268 
(*tests if the terms with the given pathes in the origTerm are commutative 

269 
respecting the list of commutative operators (commutatives)*) 

270 

271 
fun areCommutative origTerm fstPath sndPath commutatives = 

272 
if (sndPath = []) 

273 
then false 

274 
else 

275 
let 

276 
val base = (tl sndPath) 

277 
in 

278 
let 

279 
val fstcomm = 1::0::base 

280 
val opcomm = 0::0::base 

281 
in 

282 
if ((fstPath = fstcomm) andalso (is_Const (getSubTerm origTerm (rev opcomm)))) 

283 
then 

284 
let 

285 
val Const(name,_) = (getSubTerm origTerm (rev opcomm)) 

286 
in 

46332  287 
member (op =) commutatives name 
34965  288 
end 
289 
else false 

290 
end 

291 
end; 

292 

293 

294 
(*Canonizes term t with the commutative operators stored in list 

295 
commutatives*) 

296 

297 
fun canonize_term (Const (s, T) $ t $ u) comms = 

298 
let 

299 
val t' = canonize_term t comms; 

300 
val u' = canonize_term u comms; 

301 
in 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

302 
if member (op =) comms s andalso Term_Ord.termless (u', t') 
34965  303 
then Const (s, T) $ u' $ t' 
304 
else Const (s, T) $ t' $ u' 

305 
end 

306 
 canonize_term (t $ u) comms = canonize_term t comms $ canonize_term u comms 

307 
 canonize_term (Abs (s, T, t)) comms = Abs (s, T, canonize_term t comms) 

308 
 canonize_term t comms = t; 

309 

310 

311 
(*inspect the passed list and mutate origTerm following the elements of the list: 

312 
if the path of the current element is [5] (dummy path), the term has been found in the signature 

313 
and the subterm will be substituted by it 

314 
else the term has been found in the original term and the two subterms have to be exchanged 

315 
The additional parameter commutatives indicates the commutative operators 

316 
in the term whose operands won't be exchanged*) 

317 

318 
fun createMutatedTerms origTerm _ [] commutatives mutatedTerms = mutatedTerms 

319 
 createMutatedTerms origTerm (hdt as (hdTerm,hdabsContext,hdminContext,hdPath)) 

320 
((sndTerm,sndabsContext,sndminContext,sndPath)::xs) commutatives mutatedTerms = 

321 
if (sndPath = [5]) 

322 
then 

323 
let 

324 
val canonized = canonize_term (substitute (rev hdPath) origTerm sndTerm) commutatives 

325 
in 

326 
if (canonized = origTerm) 

327 
then createMutatedTerms origTerm hdt xs commutatives mutatedTerms 

328 
else createMutatedTerms origTerm hdt xs commutatives 

329 
(insert op aconv canonized mutatedTerms) 

330 
end 

331 
else 

332 
if ((areCommutative origTerm hdPath sndPath commutatives) 

333 
orelse (areCommutative origTerm sndPath hdPath commutatives)) 

334 
then createMutatedTerms origTerm hdt xs commutatives mutatedTerms 

335 
else 

336 
let 

337 
val canonized = canonize_term 

338 
(replace origTerm 

339 
(incr_boundvars (length sndabsContext  length hdminContext) hdTerm, 

340 
hdPath) 

341 
(incr_boundvars (length hdabsContext  length sndminContext) sndTerm, 

342 
sndPath)) commutatives 

343 
in 

344 
if (not(canonized = origTerm)) 

345 
then createMutatedTerms origTerm hdt xs commutatives 

346 
(insert op aconv canonized mutatedTerms) 

347 
else createMutatedTerms origTerm hdt xs commutatives mutatedTerms 

348 
end; 

349 

350 

351 

352 
(*mutates origTerm by exchanging subterms. The mutated terms are returned in a term list 

353 
The parameter commutatives consists of a list of commutative operators. The permutation of their 

354 
operands won't be considered as a new term 

355 
!!!Attention!!!: The given origTerm must be canonized. Use function canonize_term!*) 

356 

357 
fun mutate_once option origTerm tsig commutatives forbidden_funs= 

358 
let 

359 
val subTermList = getSubTermList origTerm [] [] [] 

360 
in 

361 
let 

362 
fun replaceRecursively [] mutatedTerms = mutatedTerms 

363 
 replaceRecursively ((hdTerm,hdType,hdabsContext,hdminContext,hdPath)::tail) 

364 
mutatedTerms = 

365 
replaceRecursively tail (union op aconv (createMutatedTerms origTerm 

366 
(hdTerm,hdabsContext,hdminContext,hdPath) 

367 
(searchForMutatableTerm option (hdTerm,hdType,hdabsContext,hdminContext,hdPath) 

368 
tail tsig [] forbidden_funs) 

369 
commutatives []) mutatedTerms) 

370 
in 

371 
replaceRecursively subTermList [] 

372 
end 

373 
end; 

374 

375 

376 

377 

378 
(*helper function in order to apply recursively the mutate_once function on a whole list of terms 

379 
Needed for the mutate function*) 

380 

381 
fun mutate_once_rec option [] tsig commutatives forbidden_funs acc = acc 

382 
 mutate_once_rec option (x::xs) tsig commutatives forbidden_funs acc = 

383 
mutate_once_rec option xs tsig commutatives forbidden_funs 

384 
(union op aconv (mutate_once option x tsig commutatives forbidden_funs) acc); 

385 

386 

387 

388 
(*apply function mutate_once iter times on the given origTerm. *) 

389 
(*call of mutiere with canonized form of origTerm. Prevents us of the computation of 

390 
canonization in the course of insertion of new terms!*) 

391 

392 
fun mutate option origTerm tsig commutatives forbidden_funs 0 = [] 

393 
 mutate option origTerm tsig commutatives forbidden_funs 1 = 

394 
mutate_once option (canonize_term origTerm commutatives) tsig commutatives forbidden_funs 

395 
 mutate option origTerm tsig commutatives forbidden_funs iter = 

396 
mutate_once_rec option (mutate option origTerm tsig commutatives forbidden_funs (iter1)) 

397 
tsig commutatives forbidden_funs []; 

398 

399 
(*mutate origTerm iter times by only exchanging subterms*) 

400 

401 
fun mutate_exc origTerm commutatives iter = 

37863
7f113caabcf4
discontinued pervasive val theory = Thy_Info.get_theory  prefer antiquotations in most situations;
wenzelm
parents:
37744
diff
changeset

402 
mutate 0 origTerm @{theory Main} commutatives [] iter; 
34965  403 

404 

405 
(*mutate origTerm iter times by only inserting signature functions*) 

406 

407 
fun mutate_sign origTerm tsig forbidden_funs iter = 

408 
mutate 1 origTerm tsig [] forbidden_funs iter; 

409 

410 

411 
(*mutate origTerm iter times by exchange of subterms and insertion of subterms*) 

412 

413 
fun mutate_mix origTerm tsig commutatives forbidden_funs iter = 

414 
mutate 2 origTerm tsig commutatives forbidden_funs iter; 

415 

46332  416 

34965  417 
(*helper function for the quickcheck invocation. Evaluates the quickcheck_term function on a whole list of terms 
418 
and tries to print the exceptions*) 

419 

420 
fun freeze (t $ u) = freeze t $ freeze u 

421 
 freeze (Abs (s, T, t)) = Abs (s, T, freeze t) 

422 
 freeze (Var ((a, i), T)) = 

423 
Free (if i = 0 then a else a ^ "_" ^ string_of_int i, T) 

424 
 freeze t = t; 

425 

426 
fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts) 

427 
 inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T); 

428 

35625  429 
fun preprocess thy insts t = Object_Logic.atomize_term thy 
34965  430 
(map_types (inst_type insts) (freeze t)); 
431 

432 
fun is_executable thy insts th = 

43883
aacbe67793c3
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents:
42429
diff
changeset

433 
let 
aacbe67793c3
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents:
42429
diff
changeset

434 
val ctxt' = Proof_Context.init_global thy 
40920  435 
> Config.put Quickcheck.size 1 
436 
> Config.put Quickcheck.iterations 1 

45428
aa35c9454a95
quickcheck invocations in mutabelle must not catch codegenerator errors internally
bulwahn
parents:
45159
diff
changeset

437 
val test = Quickcheck_Common.test_term 
46332  438 
("exhaustive", ((fn _ => raise (Fail "")), Exhaustive_Generators.compile_generator_expr)) ctxt' false 
43883
aacbe67793c3
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents:
42429
diff
changeset

439 
in 
aacbe67793c3
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents:
42429
diff
changeset

440 
case try test (preprocess thy insts (prop_of th), []) of 
aacbe67793c3
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents:
42429
diff
changeset

441 
SOME _ => (Output.urgent_message "executable"; true) 
aacbe67793c3
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents:
42429
diff
changeset

442 
 NONE => (Output.urgent_message ("not executable"); false) 
46332  443 
end; 
34965  444 

445 
end 