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