21 open ATP_Proof |
21 open ATP_Proof |
22 open ATP_Proof_Reconstruct |
22 open ATP_Proof_Reconstruct |
23 open VeriT_Isar |
23 open VeriT_Isar |
24 open VeriT_Proof |
24 open VeriT_Proof |
25 |
25 |
26 fun add_used_assms_in_step (VeriT_Proof.VeriT_Step {prems, ...}) = |
26 fun add_used_asserts_in_step (VeriT_Proof.VeriT_Step {prems, ...}) = |
27 union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems) |
27 union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems) |
28 |
|
29 fun step_of_assm (i, th) = |
|
30 VeriT_Proof.VeriT_Step {id = SMTLIB_Interface.assert_name_of_index i, rule = veriT_input_rule, |
|
31 prems = [], concl = prop_of th, fixes = []} |
|
32 |
28 |
33 fun parse_proof |
29 fun parse_proof |
34 ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data) |
30 ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data) |
35 xfacts prems concl output = |
31 xfacts prems concl output = |
36 let |
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 = [], concl = prop_of th, fixes = []} |
|
41 |
37 val (actual_steps, _) = VeriT_Proof.parse typs terms output ctxt |
42 val (actual_steps, _) = VeriT_Proof.parse typs terms output ctxt |
38 val used_assm_ids = fold add_used_assms_in_step actual_steps [] |
43 val used_assert_ids = fold add_used_asserts_in_step actual_steps [] |
39 val used_assms = filter (member (op =) used_assm_ids o fst) assms |
44 val used_assm_js = |
40 val assm_steps = map step_of_assm used_assms |
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 |
41 val steps = assm_steps @ actual_steps |
49 val steps = assm_steps @ actual_steps |
42 |
50 |
43 val conjecture_i = length ll_defs |
51 val conjecture_i = 0 |
44 val prems_i = conjecture_i + 1 |
52 val prems_i = conjecture_i + 1 |
45 val num_prems = length prems |
53 val num_prems = length prems |
46 val facts_i = prems_i + num_prems |
54 val facts_i = prems_i + num_prems |
47 val num_facts = length xfacts |
55 val num_facts = length xfacts |
48 val helpers_i = facts_i + num_facts |
56 val helpers_i = facts_i + num_facts |
49 |
57 |
50 val conjecture_id = conjecture_i |
58 val conjecture_id = id_of_index conjecture_i |
51 val prem_ids = prems_i upto prems_i + num_prems - 1 |
59 val prem_ids = map id_of_index (prems_i upto prems_i + num_prems - 1) |
52 val fact_ids = facts_i upto facts_i + num_facts - 1 |
60 val fact_ids' = |
53 val fact_ids' = map (fn i => (i, nth xfacts (i - facts_i))) 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 |
54 val helper_ids' = filter (fn (i, _) => i >= helpers_i) used_assms |
65 val helper_ids' = filter (fn (i, _) => i >= helpers_i) used_assms |
55 |
66 |
56 val fact_helper_ts = |
67 val fact_helper_ts = |
57 map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, prop_of th)) helper_ids' @ |
68 map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, prop_of th)) helper_ids' @ |
58 map (fn (_, ((s, _), th)) => (s, prop_of th)) fact_ids' |
69 map (fn (_, ((s, _), th)) => (s, prop_of th)) fact_ids' |