author  bulwahn 
Fri, 03 Dec 2010 08:40:47 +0100  
changeset 40920  977c60b622f4 
parent 40906  b5a319668955 
child 41067  c78a2d402736 
permissions  rwrr 
37744  1 
(* Title: HOL/Mutabelle/mutabelle.ML 
34967  2 
Author: Veronika Ortner, TU Muenchen 
34965  3 

4 
Mutation of theorems 

5 
*) 

6 
signature MUTABELLE = 

7 
sig 

8 
val testgen_name : string Unsynchronized.ref 

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 

16 
val qc_test : term list > (typ * typ) list > theory > 

17 
int > int > int * Thm.cterm list * int * (Thm.cterm * (string * Thm.cterm) list) list 

18 
val qc_test_file : bool > term list > (typ * typ) list 

19 
> theory > int > int > string > unit 

20 
val mutqc_file_exc : theory > string list > 

21 
int > Thm.thm > (typ * typ) list > int > int > string > unit 

22 
val mutqc_file_sign : theory > (string * string) list > 

23 
int > Thm.thm > (typ * typ) list > int > int > string > unit 

24 
val mutqc_file_mix : theory > string list > (string * string) list > 

25 
int > Thm.thm > (typ * typ) list > int > int > string > unit 

26 
val mutqc_file_rec_exc : theory > string list > int > 

27 
Thm.thm list > (typ * typ) list > int > int > string list > unit 

28 
val mutqc_file_rec_sign : theory > (string * string) list > int > 

29 
Thm.thm list > (typ * typ) list > int > int > string list > unit 

30 
val mutqc_file_rec_mix : theory > string list > (string * string) list > 

31 
int > Thm.thm list > (typ * typ) list > int > int > string list > unit 

32 
val mutqc_thy_exc : theory > theory > 

33 
string list > int > (typ * typ) list > int > int > string > unit 

34 
val mutqc_thy_sign : theory > theory > (string * string) list > 

35 
int > (typ * typ) list > int > int > string > unit 

36 
val mutqc_thy_mix : theory > theory > string list > (string * string) list > 

37 
int > (typ * typ) list > int > int > string > unit 

38 
val mutqc_file_stat_sign : theory > (string * string) list > 

39 
int > Thm.thm list > (typ * typ) list > int > int > string > unit 

40 
val mutqc_file_stat_exc : theory > string list > 

41 
int > Thm.thm list > (typ * typ) list > int > int > string > unit 

42 
val mutqc_file_stat_mix : theory > string list > (string * string) list > 

43 
int > Thm.thm list > (typ * typ) list > int > int > string > unit 

44 
val mutqc_thystat_exc : (string > thm > bool) > theory > theory > 

45 
string list > int > (typ * typ) list > int > int > string > unit 

46 
val mutqc_thystat_sign : (string > thm > bool) > theory > theory > (string * string) list > 

47 
int > (typ * typ) list > int > int > string > unit 

48 
val mutqc_thystat_mix : (string > thm > bool) > theory > theory > string list > 

49 
(string * string) list > int > (typ * typ) list > int > int > string > unit 

50 
val canonize_term: term > string list > term 

51 

52 
val all_unconcealed_thms_of : theory > (string * thm) list 

53 
end; 

54 

55 
structure Mutabelle : MUTABELLE = 

56 
struct 

57 

40920  58 
val testgen_name = Unsynchronized.ref "random"; 
34965  59 

60 
fun all_unconcealed_thms_of thy = 

61 
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

62 
val facts = Global_Theory.facts_of thy 
34965  63 
in 
64 
Facts.fold_static 

65 
(fn (s, ths) => 

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

67 
facts [] 

68 
end; 

69 

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

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

72 

73 
fun consts_of thy = 

74 
let 

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

76 
val consts = Symtab.dest const_table 

77 
in 

78 
List.mapPartial (fn (s, (T, NONE)) => SOME (s, T)  _ => NONE) 

79 
(filter_out (fn (s, _) => Name_Space.is_concealed namespace s) consts) 

80 
end; 

81 

82 

83 
(*helper function in order to properly print a term*) 

84 

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

85 
fun prt x = Pretty.writeln (Syntax.pretty_term_global @{theory Main} x); 
34965  86 

87 

88 
(*possibility to print a given term for debugging purposes*) 

89 

90 
val debug = (Unsynchronized.ref false); 

91 
fun debug_msg mutterm = if (!debug) then (prt mutterm) else (); 

92 

93 

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

95 

96 
exception WrongPath of string; 

97 

98 

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

100 

101 
exception WrongArg of string; 

102 

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

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

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

106 

107 
fun rename_bnds curTerm 0 = curTerm 

108 
 rename_bnds (Bound(i)) minInd = 

109 
let 

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

111 
in 

112 
Bound(erg) 

113 
end 

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

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

116 
 rename_bnds (fstUTerm $ sndUTerm) minInd = 

117 
(rename_bnds fstUTerm minInd) $ (rename_bnds sndUTerm minInd) 

118 
 rename_bnds elseTerm minInd = elseTerm; 

119 

120 

121 

122 

123 

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

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

126 
for each term in the return list 

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

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

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

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

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

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

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

134 
*) 

135 

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

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

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

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

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

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

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

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

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

145 
let 

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

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

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

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

150 
val newTerm = rename_bnds curTerm minInd 

151 
val newContext = Library.drop minInd abscontext 

152 
in 

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

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

155 
end 

156 
 getSubTermList (fstUTerm $ sndUTerm) abscontext path acc = 

157 
let 

158 
val curTerm = (fstUTerm $ sndUTerm) 

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

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

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

162 
val newTerm = rename_bnds curTerm minInd 

163 
val newContext = Library.drop minInd abscontext 

164 
in 

165 
getSubTermList fstUTerm abscontext (0::path) 

166 
(getSubTermList sndUTerm abscontext (1::path) 

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

168 
end; 

169 

170 

171 

172 

173 

174 
(*tests if the given element ist in the given list*) 

175 

176 
fun in_list elem [] = false 

177 
 in_list elem (x::xs) = if (elem = x) then true else in_list elem xs; 

178 

179 

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

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

182 
term with longContext*) 

183 

184 
fun is_morespecial longContext shortContext = 

185 
let 

186 
val revlC = rev longContext 

187 
val revsC = rev shortContext 

188 
fun is_prefix [] longList = true 

189 
 is_prefix shList [] = false 

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

191 
in 

192 
is_prefix revsC revlC 

193 
end; 

194 

195 

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

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

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

199 

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

201 
resultList 

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

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

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

205 
andalso (is_morespecial hdabsContext sminContext)) 

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

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

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

209 

210 

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

212 

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

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

215 
let 

216 
val forbType = Syntax.read_typ_global consSig forbTypeStr 

217 
val typeSignature = #tsig (Sign.rep_sg consSig) 

218 
in 

219 
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

220 
andalso (Type.typ_instance typeSignature (consType,(Logic.varifyT_global forbType)))) 
34965  221 
then true 
222 
else in_list_forb consSig (consNameStr,consType) xs 

223 
end; 

224 

225 

226 

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

228 
returns a list of those terms*) 

229 

230 
fun searchForSignatureMutations (sterm,stype) consSig forbidden_funs = 

231 
let 

232 
val sigConsTypeList = consts_of consSig; 

233 
val typeSignature = #tsig (Sign.rep_sg consSig) 

234 
in 

235 
let 

236 
fun recursiveSearch mutatableTermList [] = mutatableTermList 

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

238 
if (Type.typ_instance typeSignature (stype,ConsType) 

239 
andalso (not (sterm = Const(ConsName,stype))) 

240 
andalso (not (in_list_forb consSig (ConsName,ConsType) forbidden_funs))) 

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

242 
else recursiveSearch mutatableTermList xs 

243 
in 

244 
recursiveSearch [] sigConsTypeList 

245 
end 

246 
end; 

247 

248 

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

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

251 
in the current signature. 

252 
This function has 3 versions: 

253 
0: no instertion of signature functions, 

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

255 
1: no exchange of subterms, 

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

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

258 

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

260 
subTerms consSig resultList forbidden_funs = 

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

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

263 
subTerms consSig resultList forbidden_funs = 

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

265 
 searchForMutatableTerm 1 _ _ _ _ _ = [] 

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

267 
subTerms consSig resultList forbidden_funs = 

268 
let 

269 
val subtermMutations = searchForMutatableSubTerm 

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

271 
val signatureMutations = searchForSignatureMutations 

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

273 
in 

274 
subtermMutations@signatureMutations 

275 
end 

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

277 
subTerms consSig resultList forbidden_funs = 

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

279 
 searchForMutatableTerm i _ _ _ _ _ = 

280 
raise WrongArg("Version " ^ string_of_int i ^ 

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

282 

283 

284 

285 

286 
(*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*) 

287 

288 
fun areReplacable [] [] = false 

289 
 areReplacable fstPath [] = false 

290 
 areReplacable [] sndPath = false 

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

292 

293 

294 

295 

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

297 
The lists represent paths as generated by createSubTermList*) 

298 

299 
fun substitute [] fstTerm sndTerm = sndTerm 

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

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

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

303 
 substitute (_::xs) _ sndTerm = 

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

305 

306 

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

308 

309 
fun getSubTerm myTerm [] = myTerm 

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

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

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

313 
 getSubTerm _ (_::xs) = 

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

315 

316 

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

318 

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

320 
if (areReplacable (rev fstPath) (rev sndPath)) 

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

322 
else origTerm; 

323 

324 

325 

326 

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

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

329 

330 
fun areCommutative origTerm fstPath sndPath commutatives = 

331 
if (sndPath = []) 

332 
then false 

333 
else 

334 
let 

335 
val base = (tl sndPath) 

336 
in 

337 
let 

338 
val fstcomm = 1::0::base 

339 
val opcomm = 0::0::base 

340 
in 

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

342 
then 

343 
let 

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

345 
in 

346 
if (in_list name commutatives) 

347 
then true 

348 
else false 

349 
end 

350 
else false 

351 
end 

352 
end; 

353 

354 

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

356 
commutatives*) 

357 

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

359 
let 

360 
val t' = canonize_term t comms; 

361 
val u' = canonize_term u comms; 

362 
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

363 
if member (op =) comms s andalso Term_Ord.termless (u', t') 
34965  364 
then Const (s, T) $ u' $ t' 
365 
else Const (s, T) $ t' $ u' 

366 
end 

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

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

369 
 canonize_term t comms = t; 

370 

371 

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

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

374 
and the subterm will be substituted by it 

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

376 
The additional parameter commutatives indicates the commutative operators 

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

378 

379 
fun createMutatedTerms origTerm _ [] commutatives mutatedTerms = mutatedTerms 

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

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

382 
if (sndPath = [5]) 

383 
then 

384 
let 

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

386 
in 

387 
if (canonized = origTerm) 

388 
then createMutatedTerms origTerm hdt xs commutatives mutatedTerms 

389 
else createMutatedTerms origTerm hdt xs commutatives 

390 
(insert op aconv canonized mutatedTerms) 

391 
end 

392 
else 

393 
if ((areCommutative origTerm hdPath sndPath commutatives) 

394 
orelse (areCommutative origTerm sndPath hdPath commutatives)) 

395 
then createMutatedTerms origTerm hdt xs commutatives mutatedTerms 

396 
else 

397 
let 

398 
val canonized = canonize_term 

399 
(replace origTerm 

400 
(incr_boundvars (length sndabsContext  length hdminContext) hdTerm, 

401 
hdPath) 

402 
(incr_boundvars (length hdabsContext  length sndminContext) sndTerm, 

403 
sndPath)) commutatives 

404 
in 

405 
if (not(canonized = origTerm)) 

406 
then createMutatedTerms origTerm hdt xs commutatives 

407 
(insert op aconv canonized mutatedTerms) 

408 
else createMutatedTerms origTerm hdt xs commutatives mutatedTerms 

409 
end; 

410 

411 

412 

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

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

415 
operands won't be considered as a new term 

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

417 

418 
fun mutate_once option origTerm tsig commutatives forbidden_funs= 

419 
let 

420 
val subTermList = getSubTermList origTerm [] [] [] 

421 
in 

422 
let 

423 
fun replaceRecursively [] mutatedTerms = mutatedTerms 

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

425 
mutatedTerms = 

426 
replaceRecursively tail (union op aconv (createMutatedTerms origTerm 

427 
(hdTerm,hdabsContext,hdminContext,hdPath) 

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

429 
tail tsig [] forbidden_funs) 

430 
commutatives []) mutatedTerms) 

431 
in 

432 
replaceRecursively subTermList [] 

433 
end 

434 
end; 

435 

436 

437 

438 

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

440 
Needed for the mutate function*) 

441 

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

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

444 
mutate_once_rec option xs tsig commutatives forbidden_funs 

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

446 

447 

448 

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

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

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

452 

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

454 
 mutate option origTerm tsig commutatives forbidden_funs 1 = 

455 
mutate_once option (canonize_term origTerm commutatives) tsig commutatives forbidden_funs 

456 
 mutate option origTerm tsig commutatives forbidden_funs iter = 

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

458 
tsig commutatives forbidden_funs []; 

459 

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

461 

462 
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

463 
mutate 0 origTerm @{theory Main} commutatives [] iter; 
34965  464 

465 

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

467 

468 
fun mutate_sign origTerm tsig forbidden_funs iter = 

469 
mutate 1 origTerm tsig [] forbidden_funs iter; 

470 

471 

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

473 

474 
fun mutate_mix origTerm tsig commutatives forbidden_funs iter = 

475 
mutate 2 origTerm tsig commutatives forbidden_funs iter; 

476 

477 

478 
(*helper function in order to prettily print a list of terms*) 

479 

480 
fun pretty xs = map (fn (id, t) => (id, (HOLogic.mk_number HOLogic.natT 

481 
(HOLogic.dest_nat t)) handle TERM _ => t)) xs; 

482 

483 

484 
(*helper function for the quickcheck invocation. Evaluates the quickcheck_term function on a whole list of terms 

485 
and tries to print the exceptions*) 

486 

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

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

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

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

491 
 freeze t = t; 

492 

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

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

495 

35625  496 
fun preprocess thy insts t = Object_Logic.atomize_term thy 
34965  497 
(map_types (inst_type insts) (freeze t)); 
498 

499 
fun is_executable thy insts th = 

40906  500 
((Quickcheck.test_term 
40920  501 
(ProofContext.init_global thy 
502 
> Config.put Quickcheck.size 1 

503 
> Config.put Quickcheck.iterations 1 

504 
> Config.put Quickcheck.tester (!testgen_name)) 

505 
false (preprocess thy insts (prop_of th)); 

40248  506 
Output.urgent_message "executable"; true) handle ERROR s => 
507 
(Output.urgent_message ("not executable: " ^ s); false)); 

34965  508 

509 
fun qc_recursive usedthy [] insts sz qciter acc = rev acc 

510 
 qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter 

40248  511 
(Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs)); 
512 
((x, pretty (the_default [] (fst (Quickcheck.test_term 

40920  513 
((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter 
514 
#> Config.put Quickcheck.tester (!testgen_name)) 

40248  515 
(ProofContext.init_global usedthy)) 
40920  516 
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

517 
handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc); 
34965  518 

519 

520 
(*quickchecktest the mutants created by function mutate with typeinstantiation insts, 

521 
quickchecktheory usedthy and qciter quickcheckiterations *) 

522 

523 
fun qc_test mutated insts usedthy sz qciter = 

524 
let 

525 
val checked = map (apsnd (map (apsnd (cterm_of usedthy)))) 

526 
(qc_recursive usedthy mutated insts sz qciter []); 

527 
fun combine (passednum,passed) (cenum,ces) [] = (passednum,passed,cenum,ces) 

528 
 combine (passednum,passed) (cenum,ces) ((t, []) :: xs) = 

529 
combine (passednum+1,(cterm_of usedthy t)::passed) (cenum,ces) xs 

530 
 combine (passednum,passed) (cenum,ces) ((t, x) :: xs) = 

531 
combine (passednum,passed) 

532 
(cenum+1,(cterm_of usedthy t, x) :: ces) xs 

533 
in 

534 
combine (0,[]) (0,[]) checked 

535 
end; 

536 

537 

538 
(*create a string of a list of terms*) 

539 

540 
fun string_of_ctermlist thy [] acc = acc 

541 
 string_of_ctermlist thy (x::xs) acc = 

542 
string_of_ctermlist thy xs ((Syntax.string_of_term_global thy (term_of x)) ^ "\n" ^ acc); 

543 

544 
(*helper function in order to decompose the counter examples generated by quickcheck*) 

545 

546 
fun decompose_ce thy [] acc = acc 

547 
 decompose_ce thy ((varname,varce)::xs) acc = 

548 
decompose_ce thy xs ("\t" ^ varname ^ " instanciated to " ^ 

549 
(Syntax.string_of_term_global thy (term_of varce)) ^ "\n" ^ acc); 

550 

551 
(*helper function in order to decompose a list of counter examples*) 

552 

553 
fun decompose_celist thy [] acc = acc 

554 
 decompose_celist thy ((mutTerm,varcelist)::xs) acc = decompose_celist thy xs 

555 
("mutated term : " ^ 

556 
(Syntax.string_of_term_global thy (term_of mutTerm)) ^ "\n" ^ 

557 
"counterexample : \n" ^ 

558 
(decompose_ce thy (rev varcelist) "") ^ acc); 

559 

560 

561 
(*quickcheck test the list of mutants mutated by applying the type instantiations 

562 
insts and using the quickchecktheory usedthy. The results of quickcheck are stored 

563 
in the file with name filename. If app is true, the output will be appended to the file. 

564 
Else it will be overwritten. *) 

565 

566 
fun qc_test_file app mutated insts usedthy sz qciter filename = 

567 
let 

568 
val statisticList = qc_test mutated insts usedthy sz qciter 

569 
val passed = (string_of_int (#1 statisticList)) ^ 

570 
" terms passed the quickchecktest: \n\n" ^ 

571 
(string_of_ctermlist usedthy (rev (#2 statisticList)) "") 

572 
val counterexps = (string_of_int (#3 statisticList)) ^ 

573 
" terms produced a counterexample: \n\n" ^ 

574 
decompose_celist usedthy (rev (#4 statisticList)) "" 

575 
in 

576 
if (app = false) 

577 
then File.write (Path.explode filename) (passed ^ "\n\n" ^ counterexps) 

578 
else File.append (Path.explode filename) (passed ^ "\n\n" ^ counterexps) 

579 
end; 

580 

581 

582 
(*mutate sourceThm with the mutateversion given in option and check the resulting mutants. 

583 
The output will be written to the file with name filename*) 

584 

585 
fun mutqc_file option usedthy commutatives forbidden_funs iter sourceThm insts sz qciter filename = 

586 
let 

587 
val mutated = mutate option (prop_of sourceThm) 

588 
usedthy commutatives forbidden_funs iter 

589 
in 

590 
qc_test_file false mutated insts usedthy sz qciter filename 

591 
end; 

592 

593 
(*exchange version of function mutqc_file*) 

594 

595 
fun mutqc_file_exc usedthy commutatives iter sourceThm insts sz qciter filename = 

596 
mutqc_file 0 usedthy commutatives [] iter sourceThm insts sz qciter filename; 

597 

598 

599 
(*sinature version of function mutqc_file*) 

600 
fun mutqc_file_sign usedthy forbidden_funs iter sourceThm insts sz qciter filename= 

601 
mutqc_file 1 usedthy [] forbidden_funs iter sourceThm insts sz qciter filename; 

602 

603 
(*mixed version of function mutqc_file*) 

604 

605 
fun mutqc_file_mix usedthy commutatives forbidden_funs iter sourceThm insts sz qciter filename = 

606 
mutqc_file 2 usedthy commutatives forbidden_funs iter sourceThm insts sz qciter filename; 

607 

608 

609 

610 
(*apply function mutqc_file on a list of theorems. The output for each theorem 

611 
will be stored in a seperated file whose filename must be indicated in a list*) 

612 

613 
fun mutqc_file_rec option usedthy commutatives forbFuns iter [] insts sz qciter _ = () 

614 
 mutqc_file_rec option usedthy commutatives forbFuns iter sourceThms insts sz qciter [] = 

615 
raise WrongArg ("Not enough files for the output of qc_test_file_rec!") 

616 
 mutqc_file_rec option usedthy commutatives forbFuns iter (x::xs) insts sz qciter (y::ys) = 

617 
(mutqc_file option usedthy commutatives forbFuns iter x insts sz qciter y ; 

618 
mutqc_file_rec option usedthy commutatives forbFuns iter xs insts sz qciter ys); 

619 

620 

621 
(*exchange version of function mutqc_file_rec*) 

622 

623 
fun mutqc_file_rec_exc usedthy commutatives iter sourceThms insts sz qciter files = 

624 
mutqc_file_rec 0 usedthy commutatives [] iter sourceThms insts sz qciter files; 

625 

626 
(*signature version of function mutqc_file_rec*) 

627 

628 
fun mutqc_file_rec_sign usedthy forbidden_funs iter sourceThms insts sz qciter files = 

629 
mutqc_file_rec 1 usedthy [] forbidden_funs iter sourceThms insts sz qciter files; 

630 

631 
(*mixed version of function mutqc_file_rec*) 

632 

633 
fun mutqc_file_rec_mix usedthy commutatives forbidden_funs iter sourceThms insts sz qciter files = 

634 
mutqc_file_rec 2 usedthy commutatives forbidden_funs iter sourceThms insts sz qciter files; 

635 

636 
(*create the appropriate number of spaces in order to properly print a table*) 

637 

638 
fun create_spaces entry spacenum = 

639 
let 

640 
val diff = spacenum  (size entry) 

641 
in 

642 
if (diff > 0) 

643 
then implode (replicate diff " ") 

644 
else "" 

645 
end; 

646 

647 

648 
(*create a statistic of the output of a quickcheck test on the passed thmlist*) 

649 

650 
fun mutqc_file_stat option usedthy commutatives forbidden_funs iter thmlist insts sz qciter filename = 

651 
let 

652 
fun mutthmrec [] = () 

653 
 mutthmrec (x::xs) = 

654 
let 

655 
val mutated = mutate option (prop_of x) usedthy 

656 
commutatives forbidden_funs iter 

657 
val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter 

36743
ce2297415b54
prefer Thm.get_name_hint, which is closer to a userspace idea of "theorem name";
wenzelm
parents:
36692
diff
changeset

658 
val thmname = "\ntheorem " ^ Thm.get_name_hint x ^ ":" 
34965  659 
val pnumstring = string_of_int passednum 
660 
val cenumstring = string_of_int cenum 

661 
in 

662 
(File.append (Path.explode filename) 

663 
(thmname ^ (create_spaces thmname 50) ^ 

664 
pnumstring ^ (create_spaces pnumstring 20) ^ 

665 
cenumstring ^ (create_spaces cenumstring 20) ^ "\n"); 

666 
mutthmrec xs) 

667 
end; 

668 
in 

669 
(File.write (Path.explode filename) 

670 
("\n\ntheorem name" ^ (create_spaces "theorem name" 50) ^ 

671 
"passed mutants" ^ (create_spaces "passed mutants" 20) ^ 

672 
"counter examples\n\n" ); 

673 
mutthmrec thmlist) 

674 
end; 

675 

676 
(*signature version of function mutqc_file_stat*) 

677 

678 
fun mutqc_file_stat_sign usedthy forbidden_funs iter thmlist insts sz qciter filename = 

679 
mutqc_file_stat 1 usedthy [] forbidden_funs iter thmlist insts sz qciter filename; 

680 

681 
(*exchange version of function mutqc_file_stat*) 

682 

683 
fun mutqc_file_stat_exc usedthy commutatives iter thmlist insts sz qciter filename = 

684 
mutqc_file_stat 0 usedthy commutatives [] iter thmlist insts sz qciter filename; 

685 

686 
(*mixed version of function mutqc_file_stat*) 

687 

688 
fun mutqc_file_stat_mix usedthy commutatives forbidden_funs iter thmlist insts sz qciter filename = 

689 
mutqc_file_stat 2 usedthy commutatives forbidden_funs iter thmlist insts sz qciter filename; 

690 

691 
(*mutate and quickchecktest all the theorems contained in the passed theory. 

692 
The output will be stored in a single file*) 

693 

694 
fun mutqc_thy option mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename = 

695 
let 

696 
val thmlist = filter (is_executable mutthy insts o snd) (thms_of mutthy); 

697 
fun mutthmrec [] = () 

698 
 mutthmrec ((name,thm)::xs) = 

699 
let 

700 
val mutated = mutate option (prop_of thm) 

701 
usedthy commutatives forbidden_funs iter 

702 
in 

703 
(File.append (Path.explode filename) 

704 
("\n\nQuickchecktest of theorem " ^ name ^ ":\n\n"); 

705 
qc_test_file true mutated insts usedthy sz qciter filename; 

706 
mutthmrec xs) 

707 
end; 

708 
in 

709 
mutthmrec thmlist 

710 
end; 

711 

712 
(*exchange version of function mutqc_thy*) 

713 

714 
fun mutqc_thy_exc mutthy usedthy commutatives iter insts sz qciter filename = 

715 
mutqc_thy 0 mutthy usedthy commutatives [] iter insts sz qciter filename; 

716 

717 
(*signature version of function mutqc_thy*) 

718 

719 
fun mutqc_thy_sign mutthy usedthy forbidden_funs iter insts sz qciter filename = 

720 
mutqc_thy 1 mutthy usedthy [] forbidden_funs iter insts sz qciter filename; 

721 

722 
(*mixed version of function mutqc_thy*) 

723 

724 
fun mutqc_thy_mix mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename = 

725 
mutqc_thy 2 mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename; 

726 

727 
(*create a statistic representation of the call of function mutqc_thy*) 

728 

729 
fun mutqc_thystat option p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename = 

730 
let 

731 
val thmlist = filter 

40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39557
diff
changeset

732 
(fn (s, th) => not (p s th) andalso (Output.urgent_message s; is_executable mutthy insts th)) (thms_of mutthy) 
34965  733 
fun mutthmrec [] = () 
734 
 mutthmrec ((name,thm)::xs) = 

735 
let 

40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39557
diff
changeset

736 
val _ = Output.urgent_message ("mutthmrec: " ^ name); 
34965  737 
val mutated = mutate option (prop_of thm) usedthy 
738 
commutatives forbidden_funs iter 

739 
val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter 

740 
val thmname = "\ntheorem " ^ name ^ ":" 

741 
val pnumstring = string_of_int passednum 

742 
val cenumstring = string_of_int cenum 

743 
in 

744 
(File.append (Path.explode filename) 

745 
(thmname ^ (create_spaces thmname 50) ^ 

746 
pnumstring ^ (create_spaces pnumstring 20) ^ 

747 
cenumstring ^ (create_spaces cenumstring 20) ^ "\n"); 

748 
mutthmrec xs) 

749 
end; 

750 
in 

751 
(File.write (Path.explode filename) ("Result of the quickchecktest of theory " ^ 

752 
":\n\ntheorem name" ^ (create_spaces "theorem name" 50) ^ 

753 
"passed mutants" ^ (create_spaces "passed mutants" 20) ^ 

754 
"counter examples\n\n" ); 

755 
mutthmrec thmlist) 

756 
end; 

757 

758 
(*exchange version of function mutqc_thystat*) 

759 

760 
fun mutqc_thystat_exc p mutthy usedthy commutatives iter insts sz qciter filename = 

761 
mutqc_thystat 0 p mutthy usedthy commutatives [] iter insts sz qciter filename; 

762 

763 
(*signature version of function mutqc_thystat*) 

764 

765 
fun mutqc_thystat_sign p mutthy usedthy forbidden_funs iter insts sz qciter filename = 

766 
mutqc_thystat 1 p mutthy usedthy [] forbidden_funs iter insts sz qciter filename; 

767 

768 
(*mixed version of function mutqc_thystat*) 

769 

770 
fun mutqc_thystat_mix p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename = 

771 
mutqc_thystat 2 p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename; 

772 

773 
end 