# HG changeset patch
# User blanchet
# Date 1412074035 -7200
# Node ID e3ee0cf5cf9377d1781f5afef08d009145167392
# Parent  5ddbc170e46c3e78980b34ab5613b8490ef800d1
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'

diff -r 5ddbc170e46c -r e3ee0cf5cf93 src/HOL/Tools/SMT/verit_isar.ML
--- a/src/HOL/Tools/SMT/verit_isar.ML	Tue Sep 30 11:34:20 2014 +0200
+++ b/src/HOL/Tools/SMT/verit_isar.ML	Tue Sep 30 12:47:15 2014 +0200
@@ -25,7 +25,7 @@
 open VeriT_Proof
 
 fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
-    conjecture_id fact_helper_ids proof =
+    conjecture_id fact_helper_ids =
   let
     fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) =
       let
@@ -56,7 +56,7 @@
           [standard_step Plain]
       end
   in
-    maps steps_of proof
+    maps steps_of
   end
 
 end;
diff -r 5ddbc170e46c -r e3ee0cf5cf93 src/HOL/Tools/SMT/verit_proof_parse.ML
--- a/src/HOL/Tools/SMT/verit_proof_parse.ML	Tue Sep 30 11:34:20 2014 +0200
+++ b/src/HOL/Tools/SMT/verit_proof_parse.ML	Tue Sep 30 12:47:15 2014 +0200
@@ -23,34 +23,45 @@
 open VeriT_Isar
 open VeriT_Proof
 
-fun add_used_assms_in_step (VeriT_Proof.VeriT_Step {prems, ...}) =
+fun add_used_asserts_in_step (VeriT_Proof.VeriT_Step {prems, ...}) =
   union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems)
 
-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 num_ll_defs = length ll_defs
+
+    val id_of_index = Integer.add num_ll_defs
+    val index_of_id = Integer.add (~ num_ll_defs)
+
+    fun step_of_assume j (_, th) =
+      VeriT_Proof.VeriT_Step {id = SMTLIB_Interface.assert_name_of_index (id_of_index j),
+        rule = veriT_input_rule, prems = [], concl = prop_of th, fixes = []}
+
     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 used_assert_ids = fold add_used_asserts_in_step actual_steps []
+    val used_assm_js =
+      map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
+        used_assert_ids
+    val used_assms = map (nth assms) used_assm_js
+    val assm_steps = map2 step_of_assume used_assm_js used_assms
     val steps = assm_steps @ actual_steps
 
-    val conjecture_i = length ll_defs
+    val conjecture_i = 0
     val prems_i = conjecture_i + 1
     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 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 conjecture_id = id_of_index conjecture_i
+    val prem_ids = map id_of_index (prems_i upto prems_i + num_prems - 1)
+    val fact_ids' =
+      map_filter (fn j =>
+        let val (i, _) = nth assms j in
+          try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
+        end) used_assm_js
     val helper_ids' = filter (fn (i, _) => i >= helpers_i) used_assms
 
     val fact_helper_ts =