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