src/HOL/Tools/SMT/verit_proof_parse.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (18 months ago)
changeset 67091 1393c2340eec
parent 60201 90e88e521e0e
child 69205 8050734eee3e
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Tools/SMT/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: SMT_Translate.replay_data ->
    12     ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
    13     SMT_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 add_used_asserts_in_step (VeriT_Proof.VeriT_Step {prems, ...}) =
    27   union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems)
    28 
    29 fun 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 = [], 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 
    78 end;