32 | inferenceType (Resolve _) = Thm.Resolve |
32 | inferenceType (Resolve _) = Thm.Resolve |
33 | inferenceType (Refl _) = Thm.Refl |
33 | inferenceType (Refl _) = Thm.Refl |
34 | inferenceType (Equality _) = Thm.Equality; |
34 | inferenceType (Equality _) = Thm.Equality; |
35 |
35 |
36 local |
36 local |
37 fun ppAssume pp atm = (Parser.addBreak pp (1,0); Atom.pp pp atm); |
37 fun ppAssume atm = Print.sequence (Print.addBreak 1) (Atom.pp atm); |
38 |
38 |
39 fun ppSubst ppThm pp (sub,thm) = |
39 fun ppSubst ppThm (sub,thm) = |
40 (Parser.addBreak pp (1,0); |
40 Print.sequence (Print.addBreak 1) |
41 Parser.beginBlock pp Parser.Inconsistent 1; |
41 (Print.blockProgram Print.Inconsistent 1 |
42 Parser.addString pp "{"; |
42 [Print.addString "{", |
43 Parser.ppBinop " =" Parser.ppString Subst.pp pp ("sub",sub); |
43 Print.ppOp2 " =" Print.ppString Subst.pp ("sub",sub), |
44 Parser.addString pp ","; |
44 Print.addString ",", |
45 Parser.addBreak pp (1,0); |
45 Print.addBreak 1, |
46 Parser.ppBinop " =" Parser.ppString ppThm pp ("thm",thm); |
46 Print.ppOp2 " =" Print.ppString ppThm ("thm",thm), |
47 Parser.addString pp "}"; |
47 Print.addString "}"]); |
48 Parser.endBlock pp); |
48 |
49 |
49 fun ppResolve ppThm (res,pos,neg) = |
50 fun ppResolve ppThm pp (res,pos,neg) = |
50 Print.sequence (Print.addBreak 1) |
51 (Parser.addBreak pp (1,0); |
51 (Print.blockProgram Print.Inconsistent 1 |
52 Parser.beginBlock pp Parser.Inconsistent 1; |
52 [Print.addString "{", |
53 Parser.addString pp "{"; |
53 Print.ppOp2 " =" Print.ppString Atom.pp ("res",res), |
54 Parser.ppBinop " =" Parser.ppString Atom.pp pp ("res",res); |
54 Print.addString ",", |
55 Parser.addString pp ","; |
55 Print.addBreak 1, |
56 Parser.addBreak pp (1,0); |
56 Print.ppOp2 " =" Print.ppString ppThm ("pos",pos), |
57 Parser.ppBinop " =" Parser.ppString ppThm pp ("pos",pos); |
57 Print.addString ",", |
58 Parser.addString pp ","; |
58 Print.addBreak 1, |
59 Parser.addBreak pp (1,0); |
59 Print.ppOp2 " =" Print.ppString ppThm ("neg",neg), |
60 Parser.ppBinop " =" Parser.ppString ppThm pp ("neg",neg); |
60 Print.addString "}"]); |
61 Parser.addString pp "}"; |
61 |
62 Parser.endBlock pp); |
62 fun ppRefl tm = Print.sequence (Print.addBreak 1) (Term.pp tm); |
63 |
63 |
64 fun ppRefl pp tm = (Parser.addBreak pp (1,0); Term.pp pp tm); |
64 fun ppEquality (lit,path,res) = |
65 |
65 Print.sequence (Print.addBreak 1) |
66 fun ppEquality pp (lit,path,res) = |
66 (Print.blockProgram Print.Inconsistent 1 |
67 (Parser.addBreak pp (1,0); |
67 [Print.addString "{", |
68 Parser.beginBlock pp Parser.Inconsistent 1; |
68 Print.ppOp2 " =" Print.ppString Literal.pp ("lit",lit), |
69 Parser.addString pp "{"; |
69 Print.addString ",", |
70 Parser.ppBinop " =" Parser.ppString Literal.pp pp ("lit",lit); |
70 Print.addBreak 1, |
71 Parser.addString pp ","; |
71 Print.ppOp2 " =" Print.ppString Term.ppPath ("path",path), |
72 Parser.addBreak pp (1,0); |
72 Print.addString ",", |
73 Parser.ppBinop " =" Parser.ppString Term.ppPath pp ("path",path); |
73 Print.addBreak 1, |
74 Parser.addString pp ","; |
74 Print.ppOp2 " =" Print.ppString Term.pp ("res",res), |
75 Parser.addBreak pp (1,0); |
75 Print.addString "}"]); |
76 Parser.ppBinop " =" Parser.ppString Term.pp pp ("res",res); |
76 |
77 Parser.addString pp "}"; |
77 fun ppInf ppAxiom ppThm inf = |
78 Parser.endBlock pp); |
|
79 |
|
80 fun ppInf ppAxiom ppThm pp inf = |
|
81 let |
78 let |
82 val infString = Thm.inferenceTypeToString (inferenceType inf) |
79 val infString = Thm.inferenceTypeToString (inferenceType inf) |
83 in |
80 in |
84 Parser.beginBlock pp Parser.Inconsistent (size infString + 1); |
81 Print.block Print.Inconsistent 2 |
85 Parser.ppString pp infString; |
82 (Print.sequence |
86 case inf of |
83 (Print.addString infString) |
87 Axiom cl => ppAxiom pp cl |
84 (case inf of |
88 | Assume x => ppAssume pp x |
85 Axiom cl => ppAxiom cl |
89 | Subst x => ppSubst ppThm pp x |
86 | Assume x => ppAssume x |
90 | Resolve x => ppResolve ppThm pp x |
87 | Subst x => ppSubst ppThm x |
91 | Refl x => ppRefl pp x |
88 | Resolve x => ppResolve ppThm x |
92 | Equality x => ppEquality pp x; |
89 | Refl x => ppRefl x |
93 Parser.endBlock pp |
90 | Equality x => ppEquality x)) |
94 end; |
91 end; |
95 |
92 |
96 fun ppAxiom pp cl = |
93 fun ppAxiom cl = |
97 (Parser.addBreak pp (1,0); |
94 Print.sequence |
98 Parser.ppMap |
95 (Print.addBreak 1) |
99 LiteralSet.toList |
96 (Print.ppMap |
100 (Parser.ppBracket "{" "}" (Parser.ppSequence "," Literal.pp)) pp cl); |
97 LiteralSet.toList |
|
98 (Print.ppBracket "{" "}" (Print.ppOpList "," Literal.pp)) cl); |
101 in |
99 in |
102 val ppInference = ppInf ppAxiom Thm.pp; |
100 val ppInference = ppInf ppAxiom Thm.pp; |
103 |
101 |
104 fun pp p prf = |
102 fun pp prf = |
105 let |
103 let |
106 fun thmString n = "(" ^ Int.toString n ^ ")" |
104 fun thmString n = "(" ^ Int.toString n ^ ")" |
107 |
105 |
108 val prf = enumerate prf |
106 val prf = enumerate prf |
109 |
107 |
110 fun ppThm p th = |
108 fun ppThm th = |
|
109 Print.addString |
111 let |
110 let |
112 val cl = Thm.clause th |
111 val cl = Thm.clause th |
113 |
112 |
114 fun pred (_,(th',_)) = LiteralSet.equal (Thm.clause th') cl |
113 fun pred (_,(th',_)) = LiteralSet.equal (Thm.clause th') cl |
115 in |
114 in |
116 case List.find pred prf of |
115 case List.find pred prf of |
117 NONE => Parser.addString p "(?)" |
116 NONE => "(?)" |
118 | SOME (n,_) => Parser.addString p (thmString n) |
117 | SOME (n,_) => thmString n |
119 end |
118 end |
120 |
119 |
121 fun ppStep (n,(th,inf)) = |
120 fun ppStep (n,(th,inf)) = |
122 let |
121 let |
123 val s = thmString n |
122 val s = thmString n |
124 in |
123 in |
125 Parser.beginBlock p Parser.Consistent (1 + size s); |
124 Print.sequence |
126 Parser.addString p (s ^ " "); |
125 (Print.blockProgram Print.Consistent (1 + size s) |
127 Thm.pp p th; |
126 [Print.addString (s ^ " "), |
128 Parser.addBreak p (2,0); |
127 Thm.pp th, |
129 Parser.ppBracket "[" "]" (ppInf (K (K ())) ppThm) p inf; |
128 Print.addBreak 2, |
130 Parser.endBlock p; |
129 Print.ppBracket "[" "]" (ppInf (K Print.skip) ppThm) inf]) |
131 Parser.addNewline p |
130 Print.addNewline |
132 end |
131 end |
133 in |
132 in |
134 Parser.beginBlock p Parser.Consistent 0; |
133 Print.blockProgram Print.Consistent 0 |
135 Parser.addString p "START OF PROOF"; |
134 [Print.addString "START OF PROOF", |
136 Parser.addNewline p; |
135 Print.addNewline, |
137 app ppStep prf; |
136 Print.program (map ppStep prf), |
138 Parser.addString p "END OF PROOF"; |
137 Print.addString "END OF PROOF"] |
139 Parser.addNewline p; |
|
140 Parser.endBlock p |
|
141 end |
138 end |
142 (*DEBUG |
139 (*MetisDebug |
143 handle Error err => raise Bug ("Proof.pp: shouldn't fail:\n" ^ err); |
140 handle Error err => raise Bug ("Proof.pp: shouldn't fail:\n" ^ err); |
144 *) |
141 *) |
145 |
142 |
146 end; |
143 end; |
147 |
144 |
148 val inferenceToString = Parser.toString ppInference; |
145 val inferenceToString = Print.toString ppInference; |
149 |
146 |
150 val toString = Parser.toString pp; |
147 val toString = Print.toString pp; |
151 |
148 |
152 (* ------------------------------------------------------------------------- *) |
149 (* ------------------------------------------------------------------------- *) |
153 (* Reconstructing single inferences. *) |
150 (* Reconstructing single inferences. *) |
154 (* ------------------------------------------------------------------------- *) |
151 (* ------------------------------------------------------------------------- *) |
155 |
152 |
212 val lits = LiteralSet.intersectList [cl1,cl1',cl2,cl2'] |
209 val lits = LiteralSet.intersectList [cl1,cl1',cl2,cl2'] |
213 in |
210 in |
214 if not (LiteralSet.null lits) then LiteralSet.pick lits |
211 if not (LiteralSet.null lits) then LiteralSet.pick lits |
215 else raise Bug "can't reconstruct Resolve rule" |
212 else raise Bug "can't reconstruct Resolve rule" |
216 end) |
213 end) |
217 (*DEBUG |
214 (*MetisDebug |
218 handle Error err => |
215 handle Error err => |
219 raise Bug ("Proof.recontructResolvant: shouldn't fail:\n" ^ err); |
216 raise Bug ("Proof.recontructResolvant: shouldn't fail:\n" ^ err); |
220 *) |
217 *) |
221 |
218 |
222 fun reconstructEquality cl = |
219 fun reconstructEquality cl = |
223 let |
220 let |
224 (*TRACE3 |
221 (*MetisTrace3 |
225 val () = Parser.ppTrace LiteralSet.pp "Proof.reconstructEquality: cl" cl |
222 val () = Print.trace LiteralSet.pp "Proof.reconstructEquality: cl" cl |
226 *) |
223 *) |
227 |
224 |
228 fun sync s t path (f,a) (f',a') = |
225 fun sync s t path (f,a) (f',a') = |
229 if f <> f' orelse length a <> length a' then NONE |
226 if not (Name.equal f f' andalso length a = length a') then NONE |
230 else |
227 else |
231 case List.filter (op<> o snd) (enumerate (zip a a')) of |
228 let |
232 [(i,(tm,tm'))] => |
229 val itms = enumerate (zip a a') |
233 let |
230 in |
234 val path = i :: path |
231 case List.filter (not o uncurry Term.equal o snd) itms of |
235 in |
232 [(i,(tm,tm'))] => |
236 if tm = s andalso tm' = t then SOME (rev path) |
233 let |
237 else |
234 val path = i :: path |
238 case (tm,tm') of |
235 in |
239 (Term.Fn f_a, Term.Fn f_a') => sync s t path f_a f_a' |
236 if Term.equal tm s andalso Term.equal tm' t then |
240 | _ => NONE |
237 SOME (rev path) |
241 end |
238 else |
242 | _ => NONE |
239 case (tm,tm') of |
|
240 (Term.Fn f_a, Term.Fn f_a') => sync s t path f_a f_a' |
|
241 | _ => NONE |
|
242 end |
|
243 | _ => NONE |
|
244 end |
243 |
245 |
244 fun recon (neq,(pol,atm),(pol',atm')) = |
246 fun recon (neq,(pol,atm),(pol',atm')) = |
245 if pol = pol' then NONE |
247 if pol = pol' then NONE |
246 else |
248 else |
247 let |
249 let |
248 val (s,t) = Literal.destNeq neq |
250 val (s,t) = Literal.destNeq neq |
249 |
251 |
250 val path = |
252 val path = |
251 if s <> t then sync s t [] atm atm' |
253 if not (Term.equal s t) then sync s t [] atm atm' |
252 else if atm <> atm' then NONE |
254 else if not (Atom.equal atm atm') then NONE |
253 else Atom.find (equal s) atm |
255 else Atom.find (Term.equal s) atm |
254 in |
256 in |
255 case path of |
257 case path of |
256 SOME path => SOME ((pol',atm),path,t) |
258 SOME path => SOME ((pol',atm),path,t) |
257 | NONE => NONE |
259 | NONE => NONE |
258 end |
260 end |
262 ([l1],[l2,l3]) => [(l1,l2,l3),(l1,l3,l2)] |
264 ([l1],[l2,l3]) => [(l1,l2,l3),(l1,l3,l2)] |
263 | ([l1,l2],[l3]) => [(l1,l2,l3),(l1,l3,l2),(l2,l1,l3),(l2,l3,l1)] |
265 | ([l1,l2],[l3]) => [(l1,l2,l3),(l1,l3,l2),(l2,l1,l3),(l2,l3,l1)] |
264 | ([l1],[l2]) => [(l1,l1,l2),(l1,l2,l1)] |
266 | ([l1],[l2]) => [(l1,l1,l2),(l1,l2,l1)] |
265 | _ => raise Bug "reconstructEquality: malformed" |
267 | _ => raise Bug "reconstructEquality: malformed" |
266 |
268 |
267 (*TRACE3 |
269 (*MetisTrace3 |
268 val ppCands = |
270 val ppCands = |
269 Parser.ppList (Parser.ppTriple Literal.pp Literal.pp Literal.pp) |
271 Print.ppList (Print.ppTriple Literal.pp Literal.pp Literal.pp) |
270 val () = Parser.ppTrace ppCands |
272 val () = Print.trace ppCands |
271 "Proof.reconstructEquality: candidates" candidates |
273 "Proof.reconstructEquality: candidates" candidates |
272 *) |
274 *) |
273 in |
275 in |
274 case first recon candidates of |
276 case first recon candidates of |
275 SOME info => info |
277 SOME info => info |
276 | NONE => raise Bug "can't reconstruct Equality rule" |
278 | NONE => raise Bug "can't reconstruct Equality rule" |
277 end |
279 end |
278 (*DEBUG |
280 (*MetisDebug |
279 handle Error err => |
281 handle Error err => |
280 raise Bug ("Proof.recontructEquality: shouldn't fail:\n" ^ err); |
282 raise Bug ("Proof.recontructEquality: shouldn't fail:\n" ^ err); |
281 *) |
283 *) |
282 |
284 |
283 fun reconstruct cl (Thm.Axiom,[]) = Axiom cl |
285 fun reconstruct cl (Thm.Axiom,[]) = Axiom cl |
338 end |
340 end |
339 *) |
341 *) |
340 in |
342 in |
341 inf |
343 inf |
342 end |
344 end |
343 (*DEBUG |
345 (*MetisDebug |
344 handle Error err => |
346 handle Error err => |
345 raise Bug ("Proof.thmToInference: shouldn't fail:\n" ^ err); |
347 raise Bug ("Proof.thmToInference: shouldn't fail:\n" ^ err); |
346 *) |
348 *) |
347 end; |
349 end; |
348 |
350 |
349 (* ------------------------------------------------------------------------- *) |
351 (* ------------------------------------------------------------------------- *) |
350 (* Reconstructing whole proofs. *) |
352 (* Reconstructing whole proofs. *) |
351 (* ------------------------------------------------------------------------- *) |
353 (* ------------------------------------------------------------------------- *) |
352 |
354 |
353 local |
355 local |
354 fun thmCompare (th1,th2) = |
356 val emptyThms : Thm.thm LiteralSetMap.map = LiteralSetMap.new (); |
355 LiteralSet.compare (Thm.clause th1, Thm.clause th2); |
357 |
356 |
358 fun addThms (th,ths) = |
357 fun buildProof (th,(m,l)) = |
359 let |
358 if Map.inDomain th m then (m,l) |
360 val cl = Thm.clause th |
359 else |
361 in |
360 let |
362 if LiteralSetMap.inDomain cl ths then ths |
361 val (_,deps) = Thm.inference th |
363 else |
362 val (m,l) = foldl buildProof (m,l) deps |
364 let |
363 in |
365 val (_,pars) = Thm.inference th |
364 if Map.inDomain th m then (m,l) |
366 val ths = List.foldl addThms ths pars |
365 else |
367 in |
366 let |
368 if LiteralSetMap.inDomain cl ths then ths |
367 val l = (th, thmToInference th) :: l |
369 else LiteralSetMap.insert ths (cl,th) |
368 in |
370 end |
369 (Map.insert m (th,l), l) |
371 end; |
370 end |
372 |
371 end; |
373 fun mkThms th = addThms (th,emptyThms); |
|
374 |
|
375 fun addProof (th,(ths,acc)) = |
|
376 let |
|
377 val cl = Thm.clause th |
|
378 in |
|
379 case LiteralSetMap.peek ths cl of |
|
380 NONE => (ths,acc) |
|
381 | SOME th => |
|
382 let |
|
383 val (_,pars) = Thm.inference th |
|
384 val (ths,acc) = List.foldl addProof (ths,acc) pars |
|
385 val ths = LiteralSetMap.delete ths cl |
|
386 val acc = (th, thmToInference th) :: acc |
|
387 in |
|
388 (ths,acc) |
|
389 end |
|
390 end; |
|
391 |
|
392 fun mkProof ths th = |
|
393 let |
|
394 val (ths,acc) = addProof (th,(ths,[])) |
|
395 (*MetisTrace4 |
|
396 val () = Print.trace Print.ppInt "Proof.proof: unnecessary clauses" (LiteralSetMap.size ths) |
|
397 *) |
|
398 in |
|
399 rev acc |
|
400 end; |
372 in |
401 in |
373 fun proof th = |
402 fun proof th = |
374 let |
403 let |
375 (*TRACE3 |
404 (*MetisTrace3 |
376 val () = Parser.ppTrace Thm.pp "Proof.proof: th" th |
405 val () = Print.trace Thm.pp "Proof.proof: th" th |
377 *) |
406 *) |
378 val (m,_) = buildProof (th, (Map.new thmCompare, [])) |
407 val ths = mkThms th |
379 (*TRACE3 |
408 val infs = mkProof ths th |
380 val () = Parser.ppTrace Parser.ppInt "Proof.proof: size" (Map.size m) |
409 (*MetisTrace3 |
381 *) |
410 val () = Print.trace Print.ppInt "Proof.proof: size" (length infs) |
382 in |
411 *) |
383 case Map.peek m th of |
412 in |
384 SOME l => rev l |
413 infs |
385 | NONE => raise Bug "Proof.proof" |
|
386 end; |
414 end; |
387 end; |
415 end; |
388 |
416 |
|
417 (* ------------------------------------------------------------------------- *) |
|
418 (* Free variables. *) |
|
419 (* ------------------------------------------------------------------------- *) |
|
420 |
|
421 fun freeIn v = |
|
422 let |
|
423 fun free th_inf = |
|
424 case th_inf of |
|
425 (_, Axiom lits) => LiteralSet.freeIn v lits |
|
426 | (_, Assume atm) => Atom.freeIn v atm |
|
427 | (th, Subst _) => Thm.freeIn v th |
|
428 | (_, Resolve _) => false |
|
429 | (_, Refl tm) => Term.freeIn v tm |
|
430 | (_, Equality (lit,_,tm)) => |
|
431 Literal.freeIn v lit orelse Term.freeIn v tm |
|
432 in |
|
433 List.exists free |
|
434 end; |
|
435 |
|
436 val freeVars = |
|
437 let |
|
438 fun inc (th_inf,set) = |
|
439 NameSet.union set |
|
440 (case th_inf of |
|
441 (_, Axiom lits) => LiteralSet.freeVars lits |
|
442 | (_, Assume atm) => Atom.freeVars atm |
|
443 | (th, Subst _) => Thm.freeVars th |
|
444 | (_, Resolve _) => NameSet.empty |
|
445 | (_, Refl tm) => Term.freeVars tm |
|
446 | (_, Equality (lit,_,tm)) => |
|
447 NameSet.union (Literal.freeVars lit) (Term.freeVars tm)) |
|
448 in |
|
449 List.foldl inc NameSet.empty |
|
450 end; |
|
451 |
389 end |
452 end |