# HG changeset patch
# User blanchet
# Date 1412008653 -7200
# Node ID 7836013951e6d9497608decc80952498c8cbebf7
# Parent  62bc7c79212bf72737a05afc257a98554667d576
simplified and repaired veriT index handling code

diff -r 62bc7c79212b -r 7836013951e6 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Sep 29 14:32:30 2014 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Sep 29 18:37:33 2014 +0200
@@ -10,6 +10,7 @@
   val smtlibC: SMT_Util.class
   val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
   val translate_config: Proof.context -> SMT_Translate.config
+  val assert_name_of_index: int -> string
   val assert_index_of_name: string -> int
   val assert_prefix : string
 end;
diff -r 62bc7c79212b -r 7836013951e6 src/HOL/Tools/SMT/verit_isar.ML
--- a/src/HOL/Tools/SMT/verit_isar.ML	Mon Sep 29 14:32:30 2014 +0200
+++ b/src/HOL/Tools/SMT/verit_isar.ML	Mon Sep 29 18:37:33 2014 +0200
@@ -20,6 +20,7 @@
 open ATP_Problem
 open ATP_Proof
 open ATP_Proof_Reconstruct
+open SMTLIB_Interface
 open SMTLIB_Isar
 open VeriT_Proof
 
@@ -32,9 +33,12 @@
         fun standard_step role = ((id, []), role, concl', rule, map (rpair []) prems)
       in
         if rule = veriT_input_rule then
-          let val ss = the_list (AList.lookup (op =) fact_helper_ids (the (Int.fromString id))) in
-            (case distinguish_conjecture_and_hypothesis ss (the (Int.fromString id))
-                conjecture_id prem_ids fact_helper_ts hyp_ts concl_t of
+          let
+            val id_num = the (Int.fromString (unprefix assert_prefix id))
+            val ss = the_list (AList.lookup (op =) fact_helper_ids id_num)
+          in
+            (case distinguish_conjecture_and_hypothesis ss id_num conjecture_id prem_ids
+                fact_helper_ts hyp_ts concl_t of
               NONE => []
             | SOME (role0, concl00) =>
               let
diff -r 62bc7c79212b -r 7836013951e6 src/HOL/Tools/SMT/verit_proof_parse.ML
--- a/src/HOL/Tools/SMT/verit_proof_parse.ML	Mon Sep 29 14:32:30 2014 +0200
+++ b/src/HOL/Tools/SMT/verit_proof_parse.ML	Mon Sep 29 18:37:33 2014 +0200
@@ -23,82 +23,45 @@
 open VeriT_Isar
 open VeriT_Proof
 
-fun find_and_add_missing_dependances steps assms ll_offset =
-  let
-    fun prems_to_theorem_number [] id repl = (([], []), (id, repl))
-      | prems_to_theorem_number (x :: ths) id replaced =
-        (case Int.fromString (perhaps (try (unprefix SMTLIB_Interface.assert_prefix)) x) of
-          NONE =>
-          let
-            val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced
-          in
-            ((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 = ll_offset then 0 else id - ll_offset (* 0: for the conjecture*)
-              val ((prems, iidths), (id'', replaced')) =
-                prems_to_theorem_number ths (if th <> ll_offset then id + 1 else id)
-                  ((x, string_of_int id') :: replaced)
-            in
-              ((string_of_int id' :: prems, (th, (id', th - ll_offset)) :: 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_used_assms_in_step (VeriT_Proof.VeriT_Step {prems, ...}) =
+  union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems)
 
-fun add_missing_steps iidths =
-  let
-    fun add_single_step (_, (id, th)) = VeriT_Proof.VeriT_Step {id = string_of_int id,
-      rule = veriT_input_rule, prems = [], concl = prop_of th, fixes = []}
-  in map add_single_step iidths end
+fun step_of_assm (i, th) =
+  VeriT_Proof.VeriT_Step {id = SMTLIB_Interface.assert_name_of_index i, rule = veriT_input_rule,
+    prems = [], concl = prop_of th, fixes = []}
 
 fun parse_proof _
     ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data)
     xfacts prems concl output =
   let
-    val (steps, _) = VeriT_Proof.parse typs terms output ctxt
-    val (iidths, steps'') = find_and_add_missing_dependances steps assms (length ll_defs)
-    val steps' = add_missing_steps iidths @ steps''
-    fun id_of_index i = the_default ~1 (Option.map fst (AList.lookup (op =) iidths i))
+    val (actual_steps, _) = VeriT_Proof.parse typs terms output ctxt
+    val used_assm_ids = fold add_used_assms_in_step actual_steps []
+    val used_assms = filter (member (op =) used_assm_ids o fst) assms
+    val assm_steps = map step_of_assm used_assms
+    val steps = assm_steps @ actual_steps
 
+    val conjecture_i = 0
     val prems_i = 1
-    val facts_i = prems_i + length prems
-    val conjecture_i = 0
-    val ll_offset = 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 num_prems = length prems
+    val facts_i = prems_i + num_prems
+    val num_facts = length xfacts
+    val helpers_i = facts_i + num_facts
 
-    val fact_ids = map_filter (fn (i, (id, _)) =>
-      (try (apsnd (nth xfacts)) (id, i - facts_i))) iidths
+    val conjecture_id = conjecture_i
+    val prem_ids = prems_i upto prems_i + num_prems - 1
+    val fact_ids = facts_i upto facts_i + num_facts - 1
+    val fact_ids' = map (fn i => (i, nth xfacts (i - facts_i))) fact_ids
+    val helper_ids' = filter (fn (i, _) => i >= helpers_i) used_assms
+
     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
+      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,
+    {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 ll_offset fact_helper_ids steps'}
+       fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps}
   end
 
 end;
diff -r 62bc7c79212b -r 7836013951e6 src/HOL/Tools/SMT/z3_replay.ML
--- a/src/HOL/Tools/SMT/z3_replay.ML	Mon Sep 29 14:32:30 2014 +0200
+++ b/src/HOL/Tools/SMT/z3_replay.ML	Mon Sep 29 18:37:33 2014 +0200
@@ -186,17 +186,19 @@
 
     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_ids' =
+      map_filter (fn (i, (id, _)) => try (apsnd (nth xfacts)) (id, i - facts_i)) iidths
+    val helper_ids' = map_filter (try (fn (~1, idth) => idth)) 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
+      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,
+    {outcome = NONE, fact_ids = fact_ids',
      atp_proof = fn () => Z3_Isar.atp_proof_of_z3_proof ctxt ll_defs rewrite_rules prems concl
-       fact_helper_ts prem_ids conjecture_id fact_helper_ids steps}
+       fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps}
   end
 
 fun replay outer_ctxt