# HG changeset patch
# User blanchet
# Date 1387231516 -3600
# Node ID f5fd4a34b0e8604323ff9ccf6970c75744f2bf2d
# Parent  85879aa61334b141817f3837bad622d15a2edc4e
handle Skolems gracefully for SPASS as well

diff -r 85879aa61334 -r f5fd4a34b0e8 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Dec 16 20:43:04 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Dec 16 23:05:16 2013 +0100
@@ -468,8 +468,7 @@
 (* Syntax: core(<name>,[<name>,...,<name>]). *)
 fun parse_z3_tptp_line x =
   (scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]"
-   >> (fn (name, names) =>
-          (("", name :: names), Unknown, dummy_phi, z3_tptp_coreN, []))) x
+   >> (fn (name, names) => (("", name :: names), Unknown, dummy_phi, z3_tptp_coreN, []))) x
 
 (* Syntax: <name> *)
 fun parse_satallax_line x =
diff -r 85879aa61334 -r f5fd4a34b0e8 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Dec 16 20:43:04 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Dec 16 23:05:16 2013 +0100
@@ -11,9 +11,11 @@
   type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
   type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
   type stature = ATP_Problem_Generate.stature
+  type atp_step_name = ATP_Proof.atp_step_name
   type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
   type 'a atp_proof = 'a ATP_Proof.atp_proof
 
+  val spass_skolemize_rule : string
   val metisN : string
   val full_typesN : string
   val partial_typesN : string
@@ -25,6 +27,7 @@
   val full_type_encs : string list
   val partial_type_encs : string list
   val default_metis_lam_trans : string
+
   val metis_call : string -> string -> string
   val forall_of : term -> term -> term
   val exists_of : term -> term -> term
@@ -40,8 +43,11 @@
     'a atp_proof -> 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 replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step ->
+    ('a, 'b) atp_step
   val termify_atp_proof : Proof.context -> string Symtab.table -> (string * term) list ->
     int Symtab.table -> string atp_proof -> (term, string) atp_step list
+  val introduce_spass_skolem : (term, string) atp_step list -> (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;
@@ -54,6 +60,9 @@
 open ATP_Proof
 open ATP_Problem_Generate
 
+val spass_input_rule = "Inp"
+val spass_skolemize_rule = "__Sko" (* arbitrary *)
+
 val metisN = "metis"
 
 val full_typesN = "full_types"
@@ -174,8 +183,8 @@
 fun loose_aconv (Free (s, _), Free (s', _)) = s = s'
   | loose_aconv (t, t') = t aconv t'
 
-(* SPASS (3.8ds) and Vampire (2.6) pass arguments to Skolem functions in reverse order. *)
-val rev_skolem_prefixes = ["skf", "sK"]
+val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
+val vampire_skolem_prefix = "sK"
 
 (* First-order translation. No types are known for variables. "HOLogic.typeT"
    should allow them to be inferred. *)
@@ -269,7 +278,10 @@
               [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
             val term_ts =
               map (do_term [] NONE) us
-              |> exists (fn pre => String.isPrefix pre s) rev_skolem_prefixes ? rev
+              (* SPASS (3.8ds) and Vampire (2.6) pass arguments to Skolem functions in reverse
+                 order, which is incompatible with the new Metis skolemizer. *)
+              |> exists (fn pre => String.isPrefix pre s)
+                [spass_skolem_prefix, vampire_skolem_prefix] ? rev
             val ts = term_ts @ extra_ts
             val T =
               case opt_T of
@@ -450,6 +462,10 @@
 fun is_typed_helper_used_in_atp_proof atp_proof =
   is_axiom_used_in_proof is_typed_helper_name atp_proof
 
+fun replace_one_dependency (old, new) dep = if is_same_atp_step dep old then new else [dep]
+fun replace_dependencies_in_line old_new (name, role, t, rule, deps) =
+  (name, role, t, rule, fold (union (op =) o replace_one_dependency old_new) deps [])
+
 fun repair_name "$true" = "c_True"
   | repair_name "$false" = "c_False"
   | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)
@@ -527,6 +543,58 @@
   #> map (termify_line ctxt lifted sym_tab)
   #> repair_waldmeister_endgame
 
+fun introduce_spass_skolem [] = []
+  | introduce_spass_skolem (proof as (_, _, _, rule1, _) :: _) =
+    if rule1 = spass_input_rule then
+      let
+        fun add_sko (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s
+          | add_sko _ = I
+
+        (* union-find would be faster *)
+        fun add_cycle _ [] = I
+          | add_cycle name ss =
+            fold (fn s => Graph.default_node (s, ())) ss
+            #> fold Graph.add_edge (ss ~~ tl ss @ [hd ss])
+
+        val (input_steps, other_steps) = List.partition (null o #5) proof
+
+        val skoss = map (fn (_, _, t, _, _) => Term.fold_aterms add_sko t []) input_steps
+        val skoss_input_steps = filter_out (null o fst) (skoss ~~ input_steps)
+
+        val groups =
+          Graph.empty
+          |> fold (fn (skos, (name, _, _, _, _)) => add_cycle name skos) skoss_input_steps
+          |> Graph.strong_conn
+
+        fun step_name_of_group skos = (implode skos, [])
+        fun in_group group = member (op =) group o hd
+        fun group_of sko = the (find_first (fn group => in_group group sko) groups)
+
+        fun new_step group skoss_steps =
+          let
+            val t =
+              skoss_steps
+              |> map (snd #> #3 #> HOLogic.dest_Trueprop)
+              |> Library.foldr1 s_conj
+              |> HOLogic.mk_Trueprop
+            val deps = map (snd #> #1) skoss_steps
+          in
+            (step_name_of_group group, Plain, t, spass_skolemize_rule, deps)
+          end
+
+        val sko_steps =
+          map (fn group => new_step group (filter (in_group group o fst) skoss_input_steps)) groups
+
+        val old_news =
+          map (fn (skos, (name, _, _, _, _)) => (name, [step_name_of_group (group_of skos)]))
+            skoss_input_steps
+        val repair_deps = fold replace_dependencies_in_line old_news
+      in
+        input_steps @ sko_steps @ map repair_deps other_steps
+      end
+  else
+    proof
+
 fun factify_atp_proof fact_names hyp_ts concl_t atp_proof =
   let
     fun factify_step ((num, ss), role, t, rule, deps) =
@@ -548,7 +616,8 @@
 
     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
+  in
+    map repair_deps atp_proof
+  end
 
 end;
diff -r 85879aa61334 -r f5fd4a34b0e8 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Dec 16 20:43:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Dec 16 23:05:16 2013 +0100
@@ -847,6 +847,7 @@
                     val atp_proof =
                       atp_proof
                       |> termify_atp_proof ctxt pool lifted sym_tab
+                      |> introduce_spass_skolem
                       |> factify_atp_proof fact_names hyp_ts concl_t
                   in
                     (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout,
diff -r 85879aa61334 -r f5fd4a34b0e8 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 16 20:43:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 16 23:05:16 2013 +0100
@@ -17,8 +17,6 @@
     bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
     thm
 
-  val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step ->
-    ('a, 'b) atp_step
   val isar_proof_text : Proof.context -> bool option -> isar_params -> one_line_params -> string
   val proof_text : Proof.context -> bool option -> (unit -> isar_params) -> int ->
     one_line_params -> string
@@ -55,7 +53,8 @@
 val z3_skolemize_rule = "sk"
 val z3_th_lemma_rule = "th-lemma"
 
-val skolemize_rules = e_skolemize_rules @ [vampire_skolemisation_rule, z3_skolemize_rule]
+val skolemize_rules =
+  e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
 
 val is_skolemize_rule = member (op =) skolemize_rules
 val is_arith_rule = String.isPrefix z3_th_lemma_rule
@@ -68,11 +67,6 @@
 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]
-fun replace_dependencies_in_line oldnew (name, role, t, rule, deps) =
-  (name, role, t, rule, fold (union (op =) o replace_one_dependency oldnew) deps [])
-
 (* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *)
 fun is_only_type_information t = t aconv @{prop True}
 
diff -r 85879aa61334 -r f5fd4a34b0e8 src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Mon Dec 16 20:43:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Mon Dec 16 23:05:16 2013 +0100
@@ -19,9 +19,7 @@
     Failed_to_Play of reconstructor
 
   type minimize_command = string list -> string
-
-  type one_line_params =
-    play * string * (string * stature) list * minimize_command * int * int
+  type one_line_params = play * string * (string * stature) list * minimize_command * int * int
 
   val smtN : string
 end;
@@ -41,9 +39,7 @@
   Failed_to_Play of reconstructor
 
 type minimize_command = string list -> string
-
-type one_line_params =
-  play * string * (string * stature) list * minimize_command * int * int
+type one_line_params = play * string * (string * stature) list * minimize_command * int * int
 
 val smtN = "smt"