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 find_and_add_missing_dependances steps assms ll_offset = |
26 fun add_used_assms_in_step (VeriT_Proof.VeriT_Step {prems, ...}) = |
27 let |
27 union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems) |
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 SMTLIB_Interface.assert_prefix)) x) of |
|
31 NONE => |
|
32 let |
|
33 val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced |
|
34 in |
|
35 ((x :: prems, iidths), (id', replaced')) |
|
36 end |
|
37 | SOME th => |
|
38 (case Option.map snd (List.find (fst #> curry (op =) x) replaced) of |
|
39 NONE => |
|
40 let |
|
41 val id' = if th = ll_offset then 0 else id - ll_offset (* 0: for the conjecture*) |
|
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) |
|
45 in |
|
46 ((string_of_int id' :: prems, (th, (id', th - ll_offset)) :: iidths), |
|
47 (id'', replaced')) |
|
48 end |
|
49 | SOME x => |
|
50 let |
|
51 val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced |
|
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 |
28 |
69 fun add_missing_steps iidths = |
29 fun step_of_assm (i, th) = |
70 let |
30 VeriT_Proof.VeriT_Step {id = SMTLIB_Interface.assert_name_of_index i, rule = veriT_input_rule, |
71 fun add_single_step (_, (id, th)) = VeriT_Proof.VeriT_Step {id = string_of_int id, |
31 prems = [], concl = prop_of th, fixes = []} |
72 rule = veriT_input_rule, prems = [], concl = prop_of th, fixes = []} |
|
73 in map add_single_step iidths end |
|
74 |
32 |
75 fun parse_proof _ |
33 fun parse_proof _ |
76 ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data) |
34 ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data) |
77 xfacts prems concl output = |
35 xfacts prems concl output = |
78 let |
36 let |
79 val (steps, _) = VeriT_Proof.parse typs terms output ctxt |
37 val (actual_steps, _) = VeriT_Proof.parse typs terms output ctxt |
80 val (iidths, steps'') = find_and_add_missing_dependances steps assms (length ll_defs) |
38 val used_assm_ids = fold add_used_assms_in_step actual_steps [] |
81 val steps' = add_missing_steps iidths @ steps'' |
39 val used_assms = filter (member (op =) used_assm_ids o fst) assms |
82 fun id_of_index i = the_default ~1 (Option.map fst (AList.lookup (op =) iidths i)) |
40 val assm_steps = map step_of_assm used_assms |
|
41 val steps = assm_steps @ actual_steps |
83 |
42 |
|
43 val conjecture_i = 0 |
84 val prems_i = 1 |
44 val prems_i = 1 |
85 val facts_i = prems_i + length prems |
45 val num_prems = length prems |
86 val conjecture_i = 0 |
46 val facts_i = prems_i + num_prems |
87 val ll_offset = id_of_index conjecture_i |
47 val num_facts = length xfacts |
88 val prem_ids = map id_of_index (prems_i upto facts_i - 1) |
48 val helpers_i = facts_i + num_facts |
89 val helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths |
|
90 |
49 |
91 val fact_ids = map_filter (fn (i, (id, _)) => |
50 val conjecture_id = conjecture_i |
92 (try (apsnd (nth xfacts)) (id, i - facts_i))) iidths |
51 val prem_ids = prems_i upto prems_i + num_prems - 1 |
|
52 val fact_ids = facts_i upto facts_i + num_facts - 1 |
|
53 val fact_ids' = map (fn i => (i, nth xfacts (i - facts_i))) fact_ids |
|
54 val helper_ids' = filter (fn (i, _) => i >= helpers_i) used_assms |
|
55 |
93 val fact_helper_ts = |
56 val fact_helper_ts = |
94 map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, prop_of th)) helper_ids @ |
57 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 |
58 map (fn (_, ((s, _), th)) => (s, prop_of th)) fact_ids' |
96 val fact_helper_ids = |
59 val fact_helper_ids' = |
97 map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids @ map (apsnd (fst o fst)) fact_ids |
60 map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids' @ map (apsnd (fst o fst)) fact_ids' |
98 in |
61 in |
99 {outcome = NONE, fact_ids = fact_ids, |
62 {outcome = NONE, fact_ids = fact_ids', |
100 atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl |
63 atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl |
101 fact_helper_ts prem_ids ll_offset fact_helper_ids steps'} |
64 fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps} |
102 end |
65 end |
103 |
66 |
104 end; |
67 end; |