# HG changeset patch
# User blanchet
# Date 1384886184 -3600
# Node ID d023838eb2529463bbc4f2bdf5818c263a0de8b7
# Parent  096f7d45216479a300afd98f63978ce84e2f605c
more refactoring to accommodate SMT proofs

diff -r 096f7d452164 -r d023838eb252 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Nov 19 18:38:25 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Nov 19 19:36:24 2013 +0100
@@ -36,12 +36,6 @@
     Proof.context -> bool -> int Symtab.table ->
     (string, string, (string, string) atp_term, string) atp_formula -> term
 
-  (* FIXME: eliminate *)
-  val resolve_fact : (string * 'a) list vector -> string list -> (string * 'a) list
-  val resolve_conjecture : string list -> int list
-  val is_fact : (string * 'a) list vector -> string list -> bool
-  val is_conjecture : string list -> bool
-
   val used_facts_in_atp_proof :
     Proof.context -> (string * stature) list vector -> string atp_proof ->
     (string * stature) list
@@ -50,9 +44,10 @@
     string list option
   val lam_trans_of_atp_proof : string atp_proof -> string -> string
   val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
-  val termify_atp_proof :
-    Proof.context -> string Symtab.table -> (string * term) list ->
+  val termify_atp_proof : Proof.context -> string Symtab.table -> (string * term) list ->
     int Symtab.table -> string atp_proof -> (term, string) atp_step list
+  val factify_atp_proof : (string * 'a) list vector -> term list -> term ->
+    (term, string) atp_step list -> (term, string) atp_step list
 end;
 
 structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT =
@@ -538,4 +533,28 @@
   #> map (decode_line ctxt lifted sym_tab)
   #> repair_waldmeister_endgame
 
+fun factify_atp_proof fact_names hyp_ts concl_t atp_proof =
+  let
+    fun factify_step ((num, ss), role, t, rule, deps) =
+      let
+        val (ss', role', t') =
+          (case resolve_conjecture ss of
+            [j] =>
+            if j = length hyp_ts then ([], Conjecture, concl_t) else ([], Hypothesis, nth hyp_ts j)
+           | _ =>
+             (case resolve_fact fact_names ss of
+               [] => (ss, Plain, t)
+             | facts => (map fst facts, Axiom, t)))
+      in
+        ((num, ss'), role', t', rule, deps)
+      end
+
+    val atp_proof = map factify_step atp_proof
+    val names = map #1 atp_proof
+
+    fun repair_dep (num, ss) = (num, the_default ss (AList.lookup (op =) names num))
+    fun repair_deps (name, role, t, rule, deps) = (name, role, t, rule, map repair_dep deps)
+
+  in map repair_deps atp_proof end
+
 end;
diff -r 096f7d452164 -r d023838eb252 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Nov 19 18:38:25 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Nov 19 19:36:24 2013 +0100
@@ -844,10 +844,13 @@
                       if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
                       else partial_typesN
                     val metis_lam_trans = lam_trans_of_atp_proof atp_proof default_metis_lam_trans
-                    val atp_proof = atp_proof |> termify_atp_proof ctxt pool lifted sym_tab
+                    val atp_proof =
+                      atp_proof
+                      |> termify_atp_proof ctxt pool lifted sym_tab
+                      |> factify_atp_proof fact_names hyp_ts concl_t
                   in
                     (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout,
-                     isar_compress, isar_try0, fact_names, atp_proof, goal)
+                     isar_compress, isar_try0, atp_proof, goal)
                   end
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
diff -r 096f7d452164 -r d023838eb252 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 19 18:38:25 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 19 19:36:24 2013 +0100
@@ -13,8 +13,8 @@
   type one_line_params = Sledgehammer_Reconstructor.one_line_params
 
   type isar_params =
-    bool * bool * string * string * Time.time option * real * bool * (string * stature) list vector
-    * (term, string) atp_step list * thm
+    bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
+    thm
 
   val isar_proof_text :
     Proof.context -> bool option -> isar_params -> one_line_params -> string
@@ -52,13 +52,8 @@
 fun label_of_clause [(num, _)] = raw_label_of_num num
   | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)
 
-fun add_fact_of_dependencies fact_names (names as [(_, ss)]) =
-    if is_fact fact_names ss then
-      apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
-    else
-      apfst (insert (op =) (label_of_clause names))
-  | add_fact_of_dependencies _ names =
-    apfst (insert (op =) (label_of_clause names))
+fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
+  | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))
 
 fun replace_one_dependency (old, new) dep =
   if is_same_atp_step dep old then new else [dep]
@@ -76,12 +71,12 @@
 
 (* Discard facts; consolidate adjacent lines that prove the same formula, since
    they differ only in type information.*)
-fun add_line fact_names (name as (_, ss), role, t, rule, []) lines =
+fun add_line (name as (_, ss), role, t, rule, []) lines =
     (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
        definitions. *)
-    if is_conjecture ss then
+    if role = Conjecture orelse role = Hypothesis then
       (name, role, t, rule, []) :: lines
-    else if is_fact fact_names ss then
+    else if role = Axiom then
       (* Facts are not proof lines. *)
       if is_only_type_information t then
         map (replace_dependencies_in_line (name, [])) lines
@@ -89,7 +84,7 @@
         lines
     else
       map (replace_dependencies_in_line (name, [])) lines
-  | add_line _ (line as (name, role, t, _, _)) lines =
+  | add_line (line as (name, role, t, _, _)) lines =
     (* Type information will be deleted later; skip repetition test. *)
     if is_only_type_information t then
       line :: lines
@@ -114,12 +109,9 @@
 val is_skolemize_rule =
   member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
 
-fun add_desired_line fact_names (name as (_, ss), role, t, rule, deps)
-                     (j, lines) =
+fun add_desired_line (name as (_, ss), role, t, rule, deps) (j, lines) =
   (j + 1,
-   if is_fact fact_names ss orelse
-      is_conjecture ss orelse
-      is_skolemize_rule rule orelse
+   if role <> Plain orelse is_skolemize_rule rule orelse
       (* the last line must be kept *)
       j = 0 orelse
       (not (is_only_type_information t) andalso
@@ -217,13 +209,15 @@
     and chain_proofs proofs = map (chain_proof) proofs
   in chain_proof end
 
+fun maybe_mk_Trueprop t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
+
 type isar_params =
-  bool * bool * string * string * Time.time option * real * bool * (string * stature) list vector
-  * (term, string) atp_step list * thm
+  bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
+  thm
 
 fun isar_proof_text ctxt isar_proofs
     (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress,
-     isar_try0, fact_names, atp_proof, goal)
+     isar_try0, atp_proof, goal)
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
@@ -240,26 +234,15 @@
       let
         val atp_proof =
           atp_proof
-          |> rpair [] |-> fold_rev (add_line fact_names)
+          |> rpair [] |-> fold_rev add_line
           |> rpair [] |-> fold_rev add_nontrivial_line
           |> rpair (0, [])
-          |-> fold_rev (add_desired_line fact_names)
+          |-> fold_rev add_desired_line
           |> snd
-        val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
-        val conjs =
-          atp_proof |> map_filter
-            (fn (name as (_, ss), _, _, _, []) =>
-                if member (op =) ss conj_name then SOME name else NONE
-              | _ => NONE)
+        val conjs = atp_proof |> map_filter (try (fn (name, Conjecture, _, _, []) => name))
         val assms =
-          atp_proof |> map_filter
-            (fn ((num, ss), _, _, _, []) =>
-                (case resolve_conjecture ss of
-                   [j] =>
-                   if j = length hyp_ts then NONE
-                   else SOME (raw_label_of_num num, nth hyp_ts j)
-                 | _ => NONE)
-              | _ => NONE)
+          atp_proof
+          |> map_filter (try (fn ((num, _), Hypothesis, t, _, []) => (raw_label_of_num num, t)))
         val bot = atp_proof |> List.last |> #1
         val refute_graph =
           atp_proof
@@ -280,16 +263,12 @@
                                 I))))
                   atp_proof
         fun is_clause_skolemize_rule [(s, _)] =
-            Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) =
-            SOME true
+            Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) = SOME true
           | is_clause_skolemize_rule _ = false
         (* The assumptions and conjecture are "prop"s; the other formulas are
            "bool"s. *)
-        fun prop_of_clause [(s, ss)] =
-            (case resolve_conjecture ss of
-               [j] => if j = length hyp_ts then concl_t else nth hyp_ts j
-             | _ => the_default ("", @{term False}) (Symtab.lookup steps s)
-                    |> snd |> HOLogic.mk_Trueprop |> close_form)
+        fun prop_of_clause [(num, _)] =
+            Symtab.lookup steps num |> the |> snd |> maybe_mk_Trueprop |> close_form
           | prop_of_clause names =
             let
               val lits = map snd (map_filter (Symtab.lookup steps o fst) names)
@@ -320,7 +299,7 @@
                 let
                   val l = label_of_clause c
                   val t = prop_of_clause c
-                  val by = By ((fold (add_fact_of_dependencies fact_names) gamma no_facts), MetisM)
+                  val by = By (fold add_fact_of_dependencies gamma no_facts, MetisM)
                   fun prove sub by = Prove (maybe_show outer c [], Fix [], l, t, sub, by)
                   fun do_rest l step = do_steps outer (SOME l) (step :: accum) infs
                 in