1(*  Title:      HOL/Tools/SMT/verit_proof_parse.ML
2    Author:     Mathias Fleury, TU Muenchen
3    Author:     Jasmin Blanchette, TU Muenchen
4
5VeriT proof parsing.
6*)
7
8signature VERIT_PROOF_PARSE =
9sig
10  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
11  val parse_proof: SMT_Translate.replay_data ->
12    ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
13    SMT_Solver.parsed_proof
14end;
15
16structure VeriT_Proof_Parse: VERIT_PROOF_PARSE =
17struct
18
19open ATP_Util
20open ATP_Problem
21open ATP_Proof
22open ATP_Proof_Reconstruct
23open VeriT_Isar
24open VeriT_Proof
25
26fun add_used_asserts_in_step (VeriT_Proof.VeriT_Step {prems, ...}) =
27  union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems)
28
29fun parse_proof
30    ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data)
31    xfacts prems concl output =
32  let
33    val num_ll_defs = length ll_defs
34
35    val id_of_index = Integer.add num_ll_defs
36    val index_of_id = Integer.add (~ num_ll_defs)
37
38    fun step_of_assume j (_, th) =
39      VeriT_Proof.VeriT_Step {id = SMTLIB_Interface.assert_name_of_index (id_of_index j),
40        rule = veriT_input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []}
41
42    val (actual_steps, _) = VeriT_Proof.parse typs terms output ctxt
43    val used_assert_ids = fold add_used_asserts_in_step actual_steps []
44    val used_assm_js =
45      map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
46        used_assert_ids
47    val used_assms = map (nth assms) used_assm_js
48    val assm_steps = map2 step_of_assume used_assm_js used_assms
49    val steps = assm_steps @ actual_steps
50
51    val conjecture_i = 0
52    val prems_i = conjecture_i + 1
53    val num_prems = length prems
54    val facts_i = prems_i + num_prems
55    val num_facts = length xfacts
56    val helpers_i = facts_i + num_facts
57
58    val conjecture_id = id_of_index conjecture_i
59    val prem_ids = map id_of_index (prems_i upto prems_i + num_prems - 1)
60    val fact_ids' =
61      map_filter (fn j =>
62        let val (i, _) = nth assms j in
63          try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
64        end) used_assm_js
65    val helper_ids' = filter (fn (i, _) => i >= helpers_i) used_assms
66
67    val fact_helper_ts =
68      map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, Thm.prop_of th)) helper_ids' @
69      map (fn (_, ((s, _), th)) => (s, Thm.prop_of th)) fact_ids'
70    val fact_helper_ids' =
71      map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids' @ map (apsnd (fst o fst)) fact_ids'
72  in
73    {outcome = NONE, fact_ids = SOME fact_ids',
74     atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl
75       fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps}
76  end
77
78end;
79