57704
|
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;
|