|
1 (* Title: HOL/Tools/SMT2/verit_proof_parse.ML |
|
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 |
|
11 val parse_proof: Proof.context -> SMT2_Translate.replay_data -> |
|
12 ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> |
|
13 SMT2_Solver.parsed_proof |
|
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 |
|
26 fun find_and_add_missing_dependances steps assms conjecture_id = |
|
27 let |
|
28 fun prems_to_theorem_number [] id repl = (([], []), (id, repl)) |
|
29 | prems_to_theorem_number (x :: ths) id replaced = |
|
30 (case Int.fromString (perhaps (try (unprefix SMTLIB2_Interface.assert_prefix)) x) of |
|
31 NONE => |
|
32 let val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced |
|
33 in |
|
34 ((perhaps (try (unprefix verit_step_prefix)) x :: prems, iidths), (id', replaced')) |
|
35 end |
|
36 | SOME th => |
|
37 (case Option.map snd (List.find (fst #> curry (op =) x) replaced) of |
|
38 NONE => |
|
39 let |
|
40 val id' = if th = conjecture_id then 0 else id - conjecture_id |
|
41 val ((prems, iidths), (id'', replaced')) = prems_to_theorem_number ths |
|
42 (if th = 0 then id + 1 else id) |
|
43 ((x, string_of_int id') :: replaced) |
|
44 in ((string_of_int id' :: prems, (th, (id', th)) :: iidths), (id'', replaced')) end |
|
45 | SOME x => |
|
46 let val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced |
|
47 in ((x :: prems, iidths), (id', replaced')) end)) |
|
48 fun update_step (VeriT_Proof.VeriT_Step {prems, id = id0, rule = rule0, |
|
49 concl = concl0, fixes = fixes0}) (id, replaced) = |
|
50 let val ((prems', iidths), (id', replaced)) = prems_to_theorem_number prems id replaced |
|
51 in |
|
52 ((VeriT_Proof.VeriT_Step {id = id0, rule = rule0, prems = prems', concl = concl0, |
|
53 fixes = fixes0}, iidths), (id', replaced)) |
|
54 end |
|
55 in |
|
56 fold_map update_step steps (1, []) |
|
57 |> fst |
|
58 |> `(map snd) |
|
59 ||> (map fst) |
|
60 |>> flat |
|
61 |>> map (fn (_, (id, tm_id)) => let val (i, tm) = nth assms tm_id in (i, (id, tm)) end) |
|
62 end |
|
63 |
|
64 fun add_missing_steps iidths = |
|
65 let |
|
66 fun add_single_step (_, (id, th)) = VeriT_Proof.VeriT_Step {id = id, rule = "input", |
|
67 prems = [], concl = prop_of th, fixes = []} |
|
68 in map add_single_step iidths end |
|
69 |
|
70 fun parse_proof _ |
|
71 ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT2_Translate.replay_data) |
|
72 xfacts prems concl output = |
|
73 let |
|
74 val conjecture_i = length ll_defs |
|
75 val (steps, _) = VeriT_Proof.parse typs terms output ctxt |
|
76 val (iidths, steps'') = find_and_add_missing_dependances steps assms conjecture_i |
|
77 val steps' = add_missing_steps iidths @ steps'' |
|
78 fun id_of_index i = the_default ~1 (Option.map fst (AList.lookup (op =) iidths i)) |
|
79 |
|
80 val prems_i = 1 |
|
81 val facts_i = prems_i + length prems |
|
82 |
|
83 val conjecture_id = id_of_index conjecture_i |
|
84 val prem_ids = map id_of_index (prems_i upto facts_i - 1) |
|
85 val helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths |
|
86 |
|
87 val fact_ids = map_filter (fn (i, (id, _)) => |
|
88 (try (apsnd (nth xfacts)) (id, i - facts_i))) iidths |
|
89 val fact_helper_ts = |
|
90 map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, prop_of th)) helper_ids @ |
|
91 map (fn (_, ((s, _), th)) => (s, prop_of th)) fact_ids |
|
92 val fact_helper_ids = |
|
93 map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids @ map (apsnd (fst o fst)) fact_ids |
|
94 in |
|
95 {outcome = NONE, fact_ids = fact_ids, |
|
96 atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl |
|
97 fact_helper_ts prem_ids conjecture_id fact_helper_ids steps'} |
|
98 end |
|
99 |
|
100 end; |