author | blanchet |
Thu, 28 Aug 2014 00:40:38 +0200 | |
changeset 58061 | 3d060f43accb |
parent 57716 | src/HOL/Tools/SMT2/verit_proof_parse.ML@4546c9fdd8a7 |
child 58482 | 7836013951e6 |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/verit_proof_parse.ML |
57704 | 2 |
Author: Mathias Fleury, TU Muenchen |
3 |
Author: Jasmin Blanchette, TU Muenchen |
|
4 |
||
5 |
VeriT proof parsing. |
|
6 |
*) |
|
7 |
||
8 |
signature VERIT_PROOF_PARSE = |
|
9 |
sig |
|
10 |
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step |
|
58061 | 11 |
val parse_proof: Proof.context -> SMT_Translate.replay_data -> |
57704 | 12 |
((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> |
58061 | 13 |
SMT_Solver.parsed_proof |
57704 | 14 |
end; |
15 |
||
16 |
structure VeriT_Proof_Parse: VERIT_PROOF_PARSE = |
|
17 |
struct |
|
18 |
||
19 |
open ATP_Util |
|
20 |
open ATP_Problem |
|
21 |
open ATP_Proof |
|
22 |
open ATP_Proof_Reconstruct |
|
23 |
open VeriT_Isar |
|
24 |
open VeriT_Proof |
|
25 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
26 |
fun find_and_add_missing_dependances steps assms ll_offset = |
57704 | 27 |
let |
28 |
fun prems_to_theorem_number [] id repl = (([], []), (id, repl)) |
|
29 |
| prems_to_theorem_number (x :: ths) id replaced = |
|
58061 | 30 |
(case Int.fromString (perhaps (try (unprefix SMTLIB_Interface.assert_prefix)) x) of |
57704 | 31 |
NONE => |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
32 |
let |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
33 |
val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced |
57704 | 34 |
in |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57708
diff
changeset
|
35 |
((x :: prems, iidths), (id', replaced')) |
57704 | 36 |
end |
37 |
| SOME th => |
|
38 |
(case Option.map snd (List.find (fst #> curry (op =) x) replaced) of |
|
39 |
NONE => |
|
40 |
let |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
41 |
val id' = if th = ll_offset then 0 else id - ll_offset (* 0: for the conjecture*) |
57713 | 42 |
val ((prems, iidths), (id'', replaced')) = |
43 |
prems_to_theorem_number ths (if th <> ll_offset then id + 1 else id) |
|
44 |
((x, string_of_int id') :: replaced) |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
45 |
in |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
46 |
((string_of_int id' :: prems, (th, (id', th - ll_offset)) :: iidths), |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
47 |
(id'', replaced')) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
48 |
end |
57704 | 49 |
| SOME x => |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
50 |
let |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
51 |
val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced |
57704 | 52 |
in ((x :: prems, iidths), (id', replaced')) end)) |
53 |
fun update_step (VeriT_Proof.VeriT_Step {prems, id = id0, rule = rule0, |
|
54 |
concl = concl0, fixes = fixes0}) (id, replaced) = |
|
55 |
let val ((prems', iidths), (id', replaced)) = prems_to_theorem_number prems id replaced |
|
56 |
in |
|
57 |
((VeriT_Proof.VeriT_Step {id = id0, rule = rule0, prems = prems', concl = concl0, |
|
58 |
fixes = fixes0}, iidths), (id', replaced)) |
|
59 |
end |
|
60 |
in |
|
61 |
fold_map update_step steps (1, []) |
|
62 |
|> fst |
|
63 |
|> `(map snd) |
|
64 |
||> (map fst) |
|
65 |
|>> flat |
|
66 |
|>> map (fn (_, (id, tm_id)) => let val (i, tm) = nth assms tm_id in (i, (id, tm)) end) |
|
67 |
end |
|
68 |
||
69 |
fun add_missing_steps iidths = |
|
70 |
let |
|
57716 | 71 |
fun add_single_step (_, (id, th)) = VeriT_Proof.VeriT_Step {id = string_of_int id, |
72 |
rule = veriT_input_rule, prems = [], concl = prop_of th, fixes = []} |
|
57704 | 73 |
in map add_single_step iidths end |
74 |
||
75 |
fun parse_proof _ |
|
58061 | 76 |
({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data) |
57704 | 77 |
xfacts prems concl output = |
78 |
let |
|
79 |
val (steps, _) = VeriT_Proof.parse typs terms output ctxt |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
80 |
val (iidths, steps'') = find_and_add_missing_dependances steps assms (length ll_defs) |
57704 | 81 |
val steps' = add_missing_steps iidths @ steps'' |
82 |
fun id_of_index i = the_default ~1 (Option.map fst (AList.lookup (op =) iidths i)) |
|
83 |
||
84 |
val prems_i = 1 |
|
85 |
val facts_i = prems_i + length prems |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
86 |
val conjecture_i = 0 |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
87 |
val ll_offset = id_of_index conjecture_i |
57704 | 88 |
val prem_ids = map id_of_index (prems_i upto facts_i - 1) |
89 |
val helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths |
|
90 |
||
91 |
val fact_ids = map_filter (fn (i, (id, _)) => |
|
92 |
(try (apsnd (nth xfacts)) (id, i - facts_i))) iidths |
|
93 |
val fact_helper_ts = |
|
94 |
map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, prop_of th)) helper_ids @ |
|
95 |
map (fn (_, ((s, _), th)) => (s, prop_of th)) fact_ids |
|
96 |
val fact_helper_ids = |
|
97 |
map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids @ map (apsnd (fst o fst)) fact_ids |
|
98 |
in |
|
99 |
{outcome = NONE, fact_ids = fact_ids, |
|
100 |
atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
101 |
fact_helper_ts prem_ids ll_offset fact_helper_ids steps'} |
57704 | 102 |
end |
103 |
||
104 |
end; |