author  wenzelm 
Thu, 31 May 2007 01:25:24 +0200  
changeset 23139  aa899bce7c3b 
parent 21078  101aefd61aac 
child 24712  64ed05609568 
permissions  rwrr 
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

1 
(* Title: HOL/Import/replay.ML 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

2 
ID: $Id$ 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

3 
Author: Sebastian Skalberg (TU Muenchen) 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

4 
*) 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

5 

14516  6 
structure Replay = 
7 
struct 

8 

9 
structure P = ProofKernel 

10 

11 
open ProofKernel 

19064  12 
open ImportRecorder 
14516  13 

14 
exception REPLAY of string * string 

15 
fun ERR f mesg = REPLAY (f,mesg) 

16 
fun NY f = raise ERR f "NOT YET!" 

17 

18 
fun replay_proof int_thms thyname thmname prf thy = 

19 
let 

19064  20 
val _ = ImportRecorder.start_replay_proof thyname thmname 
14516  21 
fun rp (PRefl tm) thy = P.REFL tm thy 
22 
 rp (PInstT(p,lambda)) thy = 

23 
let 

24 
val (thy',th) = rp' p thy 

25 
in 

26 
P.INST_TYPE lambda th thy' 

27 
end 

28 
 rp (PSubst(prfs,ctxt,prf)) thy = 

29 
let 

21078  30 
val (thy',ths) = fold_rev (fn p => fn (thy, ths) => 
14516  31 
let 
32 
val (thy',th) = rp' p thy 

33 
in 

34 
(thy',th::ths) 

21078  35 
end) prfs (thy,[]) 
14516  36 
val (thy'',th) = rp' prf thy' 
37 
in 

38 
P.SUBST ths ctxt th thy'' 

39 
end 

40 
 rp (PAbs(prf,v)) thy = 

41 
let 

42 
val (thy',th) = rp' prf thy 

43 
in 

44 
P.ABS v th thy' 

45 
end 

46 
 rp (PDisch(prf,tm)) thy = 

47 
let 

48 
val (thy',th) = rp' prf thy 

49 
in 

50 
P.DISCH tm th thy' 

51 
end 

52 
 rp (PMp(prf1,prf2)) thy = 

53 
let 

54 
val (thy1,th1) = rp' prf1 thy 

55 
val (thy2,th2) = rp' prf2 thy1 

56 
in 

57 
P.MP th1 th2 thy2 

58 
end 

59 
 rp (PHyp tm) thy = P.ASSUME tm thy 

60 
 rp (PDef(seg,name,rhs)) thy = 

61 
(case P.get_def seg name rhs thy of 

15531  62 
(thy',SOME res) => (thy',res) 
63 
 (thy',NONE) => 

14516  64 
if seg = thyname 
65 
then P.new_definition seg name rhs thy' 

17322  66 
else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname)) 
14516  67 
 rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE" 
68 
 rp (PSpec(prf,tm)) thy = 

69 
let 

70 
val (thy',th) = rp' prf thy 

71 
in 

72 
P.SPEC tm th thy' 

73 
end 

74 
 rp (PInst(prf,theta)) thy = 

75 
let 

76 
val (thy',th) = rp' prf thy 

77 
in 

78 
P.INST theta th thy' 

79 
end 

80 
 rp (PGen(prf,v)) thy = 

81 
let 

82 
val (thy',th) = rp' prf thy 

17592  83 
val p = P.GEN v th thy' 
14516  84 
in 
17592  85 
p 
14516  86 
end 
87 
 rp (PGenAbs(prf,opt,vl)) thy = 

88 
let 

89 
val (thy',th) = rp' prf thy 

90 
in 

91 
P.GEN_ABS opt vl th thy' 

92 
end 

93 
 rp (PImpAS(prf1,prf2)) thy = 

94 
let 

95 
val (thy1,th1) = rp' prf1 thy 

96 
val (thy2,th2) = rp' prf2 thy1 

97 
in 

98 
P.IMP_ANTISYM th1 th2 thy2 

99 
end 

100 
 rp (PSym prf) thy = 

101 
let 

102 
val (thy1,th) = rp' prf thy 

103 
in 

104 
P.SYM th thy1 

105 
end 

106 
 rp (PTrans(prf1,prf2)) thy = 

107 
let 

108 
val (thy1,th1) = rp' prf1 thy 

109 
val (thy2,th2) = rp' prf2 thy1 

110 
in 

111 
P.TRANS th1 th2 thy2 

112 
end 

113 
 rp (PComb(prf1,prf2)) thy = 

114 
let 

115 
val (thy1,th1) = rp' prf1 thy 

116 
val (thy2,th2) = rp' prf2 thy1 

117 
in 

118 
P.COMB th1 th2 thy2 

119 
end 

120 
 rp (PEqMp(prf1,prf2)) thy = 

121 
let 

122 
val (thy1,th1) = rp' prf1 thy 

123 
val (thy2,th2) = rp' prf2 thy1 

124 
in 

125 
P.EQ_MP th1 th2 thy2 

126 
end 

127 
 rp (PEqImp prf) thy = 

128 
let 

129 
val (thy',th) = rp' prf thy 

130 
in 

131 
P.EQ_IMP_RULE th thy' 

132 
end 

133 
 rp (PExists(prf,ex,wit)) thy = 

134 
let 

135 
val (thy',th) = rp' prf thy 

136 
in 

137 
P.EXISTS ex wit th thy' 

138 
end 

139 
 rp (PChoose(v,prf1,prf2)) thy = 

140 
let 

141 
val (thy1,th1) = rp' prf1 thy 

142 
val (thy2,th2) = rp' prf2 thy1 

143 
in 

144 
P.CHOOSE v th1 th2 thy2 

145 
end 

146 
 rp (PConj(prf1,prf2)) thy = 

147 
let 

148 
val (thy1,th1) = rp' prf1 thy 

149 
val (thy2,th2) = rp' prf2 thy1 

150 
in 

151 
P.CONJ th1 th2 thy2 

152 
end 

153 
 rp (PConjunct1 prf) thy = 

154 
let 

155 
val (thy',th) = rp' prf thy 

156 
in 

157 
P.CONJUNCT1 th thy' 

158 
end 

159 
 rp (PConjunct2 prf) thy = 

160 
let 

161 
val (thy',th) = rp' prf thy 

162 
in 

163 
P.CONJUNCT2 th thy' 

164 
end 

165 
 rp (PDisj1(prf,tm)) thy = 

166 
let 

167 
val (thy',th) = rp' prf thy 

168 
in 

169 
P.DISJ1 th tm thy' 

170 
end 

171 
 rp (PDisj2(prf,tm)) thy = 

172 
let 

173 
val (thy',th) = rp' prf thy 

174 
in 

175 
P.DISJ2 tm th thy' 

176 
end 

177 
 rp (PDisjCases(prf,prf1,prf2)) thy = 

178 
let 

179 
val (thy',th) = rp' prf thy 

180 
val (thy1,th1) = rp' prf1 thy' 

181 
val (thy2,th2) = rp' prf2 thy1 

182 
in 

183 
P.DISJ_CASES th th1 th2 thy2 

184 
end 

185 
 rp (PNotI prf) thy = 

186 
let 

187 
val (thy',th) = rp' prf thy 

188 
in 

189 
P.NOT_INTRO th thy' 

190 
end 

191 
 rp (PNotE prf) thy = 

192 
let 

193 
val (thy',th) = rp' prf thy 

194 
in 

195 
P.NOT_ELIM th thy' 

196 
end 

197 
 rp (PContr(prf,tm)) thy = 

198 
let 

199 
val (thy',th) = rp' prf thy 

200 
in 

201 
P.CCONTR tm th thy' 

202 
end 

203 
 rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)" 

204 
 rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)" 

205 
 rp (PTyIntro _) _ = raise ERR "rp" "Shouldn't reach here (PTyIntro)" 

206 
 rp PDisk _ = raise ERR "rp" "Shouldn't reach here (PDisk)" 

207 
 rp _ _ = raise ERR "rp" "What the hell is this? Which case did I forget?" 

208 
and rp' p thy = 

209 
let 

210 
val pc = content_of p 

211 
in 

212 
case pc of 

213 
PDisk => (case disk_info_of p of 

15531  214 
SOME(thyname',thmname) => 
14516  215 
(case Int.fromString thmname of 
216 
SOME i => 

217 
if thyname' = thyname 

218 
then 

219 
(case Array.sub(int_thms,i1) of 

15531  220 
NONE => 
14516  221 
let 
222 
val (thy',th) = rp' (snd (import_proof thyname' thmname thy) thy) thy 

15531  223 
val _ = Array.update(int_thms,i1,SOME th) 
14516  224 
in 
225 
(thy',th) 

226 
end 

15531  227 
 SOME th => (thy,th)) 
14516  228 
else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")") 
229 
 NONE => 

230 
(case P.get_thm thyname' thmname thy of 

17594  231 
(thy',SOME res) => (thy',res) 
15531  232 
 (thy',NONE) => 
14516  233 
if thyname' = thyname 
234 
then 

235 
let 

236 
val _ = writeln ("Found no " ^ thmname ^ " theorem, replaying...") 

237 
val (f_opt,prf) = import_proof thyname' thmname thy' 

238 
val prf = prf thy' 

239 
val (thy',th) = replay_proof int_thms thyname' thmname prf thy' 

17322  240 
val _ = writeln ("Successfully finished replaying "^thmname^" !") 
14516  241 
in 
242 
case content_of prf of 

243 
PTmSpec _ => (thy',th) 

244 
 PTyDef _ => (thy',th) 

245 
 PTyIntro _ => (thy',th) 

246 
 _ => P.store_thm thyname' thmname th thy' 

247 
end 

248 
else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")"))) 

15531  249 
 NONE => raise ERR "rp'.PDisk" "Not enough information") 
14516  250 
 PAxm(name,c) => 
251 
(case P.get_axiom thyname name thy of 

15531  252 
(thy',SOME res) => (thy',res) 
253 
 (thy',NONE) => P.new_axiom name c thy') 

14516  254 
 PTmSpec(seg,names,prf') => 
255 
let 

256 
val (thy',th) = rp' prf' thy 

257 
in 

258 
P.new_specification seg thmname names th thy' 

259 
end 

260 
 PTyDef(seg,name,prf') => 

261 
let 

262 
val (thy',th) = rp' prf' thy 

263 
in 

264 
P.new_type_definition seg thmname name th thy' 

265 
end 

266 
 PTyIntro(seg,name,abs_name,rep_name,P,t,prf') => 

267 
let 

268 
val (thy',th) = rp' prf' thy 

269 
in 

270 
P.type_introduction seg thmname name abs_name rep_name (P,t) th thy' 

271 
end 

272 
 _ => rp pc thy 

273 
end 

274 
in 

19064  275 
let 
276 
val x = rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e) 

277 
val _ = ImportRecorder.stop_replay_proof thyname thmname 

278 
in 

279 
x 

280 
end 

281 
end handle x => (ImportRecorder.abort_replay_proof thyname thmname; raise x) 

14516  282 

283 
fun setup_int_thms thyname thy = 

284 
let 

14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

285 
val fname = 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

286 
case P.get_proof_dir thyname thy of 
15531  287 
SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}} 
288 
 NONE => error "Cannot find proof files" 

14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

289 
val is = TextIO.openIn fname 
14516  290 
val (num_int_thms,facts) = 
291 
let 

292 
fun get_facts facts = 

293 
case TextIO.inputLine is of 

23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
21078
diff
changeset

294 
NONE => (case facts of 
17440
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17322
diff
changeset

295 
i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts)) 
14516  296 
 _ => raise ERR "replay_thm" "Bad facts.lst file") 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
21078
diff
changeset

297 
 SOME fact => get_facts ((String.substring(fact,0,String.size fact 1 ))::facts) 
14516  298 
in 
299 
get_facts [] 

300 
end 

301 
val _ = TextIO.closeIn is 

15531  302 
val int_thms = Array.array(num_int_thms,NONE:thm option) 
14516  303 
in 
304 
(int_thms,facts) 

305 
end 

306 

307 
fun import_single_thm thyname int_thms thmname thy = 

308 
let 

309 
fun replay_fact (thmname,thy) = 

310 
let 

311 
val prf = mk_proof PDisk 

312 
val _ = set_disk_info_of prf thyname thmname 

17594  313 
val _ = writeln ("Replaying "^thmname^" ...") 
17592  314 
val p = fst (replay_proof int_thms thyname thmname prf thy) 
14516  315 
in 
17592  316 
p 
14516  317 
end 
318 
in 

319 
replay_fact (thmname,thy) 

320 
end 

321 

19064  322 
fun replay_chached_thm int_thms thyname thmname = 
323 
let 

324 
fun th_of thy = setmp quick_and_dirty true (SkipProof.make_thm thy) 

325 
fun err msg = raise ERR "replay_cached_thm" msg 

326 
val _ = writeln ("Replaying (from cache) "^thmname^" ...") 

327 
fun rps [] thy = thy 

328 
 rps (t::ts) thy = rps ts (rp t thy) 

329 
and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy 

330 
 rp (DeltaEntry ds) thy = fold delta ds thy 

331 
and delta (Specification (names, th)) thy = 

332 
fst (SpecificationPackage.add_specification NONE names (thy,th_of thy th)) 

333 
 delta (Hol_mapping (thyname, thmname, isaname)) thy = 

334 
add_hol4_mapping thyname thmname isaname thy 

335 
 delta (Hol_pending (thyname, thmname, th)) thy = 

336 
add_hol4_pending thyname thmname ([], th_of thy th) thy 

337 
 delta (Consts cs) thy = Theory.add_consts_i cs thy 

338 
 delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 

339 
add_hol4_const_mapping thyname constname true fullcname thy 

340 
 delta (Hol_move (fullname, moved_thmname)) thy = 

341 
add_hol4_move fullname moved_thmname thy 

342 
 delta (Defs (thmname, eq)) thy = 

343 
snd (PureThy.add_defs_i false [((thmname, eq), [])] thy) 

344 
 delta (Hol_theorem (thyname, thmname, th)) thy = 

345 
add_hol4_theorem thyname thmname ([], th_of thy th) thy 

346 
 delta (Typedef (thmname, typ, c, repabs, th)) thy = 

19349  347 
snd (TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy) 
19064  348 
 delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy = 
349 
add_hol4_type_mapping thyname tycname true fulltyname thy 

350 
 delta (Indexed_theorem (i, th)) thy = 

351 
(Array.update (int_thms,i1,SOME (P.to_hol_thm (th_of thy th))); thy) 

19068  352 
 delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy) 
353 
 delta (Dump s) thy = P.replay_add_dump s thy 

19064  354 
in 
355 
rps 

356 
end 

357 

14516  358 
fun import_thms thyname int_thms thmnames thy = 
359 
let 

19064  360 
fun zip names [] = ([], names) 
361 
 zip [] _ = ([], []) 

362 
 zip (thmname::names) ((ThmEntry (entry as (thyname',thmname',aborted,History history)))::ys) = 

363 
if thyname = thyname' andalso thmname = thmname' then 

364 
(if aborted then ([], thmname::names) else 

365 
let 

366 
val _ = writeln ("theorem is insync: "^thmname) 

367 
val (cached,normal) = zip names ys 

368 
in 

369 
(entry::cached, normal) 

370 
end) 

371 
else 

19203  372 
let 
373 
val _ = writeln ("cached theorems are not insync, expected: "^thmname^", found: "^thmname') 

374 
val _ = writeln ("proceeding with next uncached theorem...") 

375 
in 

376 
([], thmname::names) 

377 
end 

378 
(* raise ERR "import_thms" ("cached theorems are not insync, expected: "^thmname^", found: "^thmname')*) 

19064  379 
 zip (thmname::_) (DeltaEntry _ :: _) = 
380 
raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta") 

381 
fun zip' xs (History ys) = 

382 
let 

383 
val _ = writeln ("length of xs: "^(string_of_int (length xs))) 

384 
val _ = writeln ("length of history: "^(string_of_int (length ys))) 

385 
in 

386 
zip xs ys 

387 
end 

388 
fun replay_fact thmname thy = 

14516  389 
let 
17592  390 
val prf = mk_proof PDisk 
17594  391 
val _ = set_disk_info_of prf thyname thmname 
392 
val _ = writeln ("Replaying "^thmname^" ...") 

17592  393 
val p = fst (replay_proof int_thms thyname thmname prf thy) 
14516  394 
in 
17592  395 
p 
14516  396 
end 
19064  397 
fun replay_cache (_,thmname, _, History history) thy = replay_chached_thm int_thms thyname thmname history thy 
398 
val (cached, normal) = zip' thmnames (ImportRecorder.get_history ()) 

399 
val _ = ImportRecorder.set_history (History (map ThmEntry cached)) 

400 
val res_thy = fold replay_fact normal (fold replay_cache cached thy) 

14516  401 
in 
402 
res_thy 

403 
end 

404 

405 
fun import_thm thyname thmname thy = 

406 
let 

407 
val int_thms = fst (setup_int_thms thyname thy) 

408 
fun replay_fact (thmname,thy) = 

409 
let 

17592  410 
val prf = mk_proof PDisk 
17594  411 
val _ = set_disk_info_of prf thyname thmname 
412 
val _ = writeln ("Replaying "^thmname^" ...") 

17592  413 
val p = fst (replay_proof int_thms thyname thmname prf thy) 
414 
in 

415 
p 

14516  416 
end 
417 
in 

418 
replay_fact (thmname,thy) 

419 
end 

420 

17959  421 
end 