src/HOL/Tools/SMT2/verit_proof_parse.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT2/verit_proof_parse.ML	Wed Jul 30 14:03:12 2014 +0200
@@ -0,0 +1,100 @@
+(*  Title:      HOL/Tools/SMT2/verit_proof_parse.ML
+    Author:     Mathias Fleury, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+
+VeriT proof parsing.
+*)
+
+signature VERIT_PROOF_PARSE =
+sig
+  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
+  val parse_proof: Proof.context -> SMT2_Translate.replay_data ->
+    ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
+    SMT2_Solver.parsed_proof
+end;
+
+structure VeriT_Proof_Parse: VERIT_PROOF_PARSE =
+struct
+
+open ATP_Util
+open ATP_Problem
+open ATP_Proof
+open ATP_Proof_Reconstruct
+open VeriT_Isar
+open VeriT_Proof
+
+fun find_and_add_missing_dependances steps assms conjecture_id =
+  let
+    fun prems_to_theorem_number [] id repl = (([], []), (id, repl))
+      | prems_to_theorem_number (x :: ths) id replaced =
+        (case Int.fromString (perhaps (try (unprefix SMTLIB2_Interface.assert_prefix)) x) of
+          NONE =>
+          let val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced
+          in
+            ((perhaps (try (unprefix verit_step_prefix)) x :: prems, iidths), (id', replaced'))
+          end
+        | SOME th =>
+          (case Option.map snd (List.find (fst #> curry (op =) x) replaced) of
+            NONE =>
+            let
+              val id' = if th = conjecture_id then 0 else id - conjecture_id
+              val ((prems, iidths), (id'', replaced')) = prems_to_theorem_number ths
+                                                          (if th = 0 then id + 1 else id)
+                                                          ((x, string_of_int id') :: replaced)
+            in ((string_of_int id' :: prems, (th, (id', th)) :: iidths), (id'', replaced')) end
+          | SOME x =>
+            let val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced
+            in ((x :: prems, iidths), (id', replaced')) end))
+    fun update_step (VeriT_Proof.VeriT_Step {prems, id = id0, rule = rule0,
+        concl = concl0, fixes = fixes0}) (id, replaced) =
+      let val ((prems', iidths), (id', replaced)) = prems_to_theorem_number prems id replaced
+      in
+        ((VeriT_Proof.VeriT_Step {id = id0, rule = rule0, prems = prems', concl = concl0,
+           fixes = fixes0}, iidths), (id', replaced))
+      end
+  in
+    fold_map update_step steps (1, [])
+    |> fst
+    |> `(map snd)
+    ||> (map fst)
+    |>> flat
+    |>> map (fn (_, (id, tm_id)) => let val (i, tm) = nth assms tm_id in (i, (id, tm)) end)
+  end
+
+fun add_missing_steps iidths =
+  let
+    fun add_single_step (_, (id, th)) = VeriT_Proof.VeriT_Step {id = id, rule = "input",
+      prems = [], concl = prop_of th, fixes = []}
+  in map add_single_step iidths end
+
+fun parse_proof _
+    ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT2_Translate.replay_data)
+    xfacts prems concl output =
+  let
+    val conjecture_i = length ll_defs
+    val (steps, _) = VeriT_Proof.parse typs terms output ctxt
+    val (iidths, steps'') = find_and_add_missing_dependances steps assms conjecture_i
+    val steps' = add_missing_steps iidths @ steps''
+    fun id_of_index i = the_default ~1 (Option.map fst (AList.lookup (op =) iidths i))
+
+    val prems_i = 1
+    val facts_i = prems_i + length prems
+
+    val conjecture_id = id_of_index conjecture_i
+    val prem_ids = map id_of_index (prems_i upto facts_i - 1)
+    val helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths
+
+    val fact_ids = map_filter (fn (i, (id, _)) =>
+      (try (apsnd (nth xfacts)) (id, i - facts_i))) iidths
+    val fact_helper_ts =
+      map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, prop_of th)) helper_ids @
+      map (fn (_, ((s, _), th)) => (s, prop_of th)) fact_ids
+    val fact_helper_ids =
+      map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids @ map (apsnd (fst o fst)) fact_ids
+  in
+    {outcome = NONE, fact_ids = fact_ids,
+     atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl
+       fact_helper_ts prem_ids conjecture_id fact_helper_ids steps'}
+  end
+
+end;