imported patch satallax_proof_support_Sledgehammer

--- a/src/HOL/ATP.thy	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/ATP.thy	Wed Jul 30 14:03:12 2014 +0200
@@ -15,6 +15,8 @@
 ML_file "Tools/ATP/atp_problem.ML"
 ML_file "Tools/ATP/atp_proof.ML"
 ML_file "Tools/ATP/atp_proof_redirect.ML"
+ML_file "Tools/ATP/atp_satallax.ML"
+
 
 subsection {* Higher-order reasoning helpers *}
 

--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:12 2014 +0200
@@ -68,7 +68,6 @@
   val remote_prefix : string
 
   val agsyhol_core_rule : string
-  val satallax_core_rule : string
   val spass_input_rule : string
   val spass_pre_skolemize_rule : string
   val spass_skolemize_rule : string
@@ -85,10 +84,26 @@
   val scan_general_id : string list -> string * string list
   val parse_formula : string list ->
     (string, string atp_type, (string, string atp_type) atp_term, string) atp_formula * string list
-  val atp_proof_of_tstplike_proof : string -> string atp_problem -> string -> string atp_proof
   val clean_up_atp_proof_dependencies : string atp_proof -> string atp_proof
   val map_term_names_in_atp_proof : (string -> string) -> string atp_proof -> string atp_proof
   val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof
+
+  val skip_term: string list -> string * string list
+  val parse_thf0_formula :string list ->
+      ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
+       'c) ATP_Problem.atp_formula *
+      string list
+  val dummy_atype :  string ATP_Problem.atp_type
+  val role_of_tptp_string:  string -> ATP_Problem.atp_formula_role
+  val parse_line: string -> ('a * string ATP_Problem.atp_problem_line list) list ->
+              string list -> ((string * string list) * ATP_Problem.atp_formula_role *
+               (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
+                'c) ATP_Problem.atp_formula
+               * string * (string * 'd list) list) list * string list
+  val core_inference :   'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role *
+              ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
+  val vampire_step_name_ord : (string * 'a) * (string * 'a) -> order
+  val core_of_agsyhol_proof :  string -> string list option
 end;
 
 structure ATP_Proof : ATP_PROOF =
@@ -123,7 +138,6 @@
 val remote_prefix = "remote_"
 
 val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
-val satallax_core_rule = "__satallax_core" (* arbitrary *)
 val spass_input_rule = "Inp"
 val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *)
 val spass_skolemize_rule = "__Sko" (* arbitrary *)
@@ -278,7 +292,7 @@
   let
     fun skip _ accum [] = (accum, [])
       | skip n accum (ss as s :: ss') =
-        if s = "," andalso n = 0 then
+        if (s = "," orelse s = ".") andalso n = 0 then
           (accum, ss)
         else if member (op =) [")", "]"] s then
           if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss'
@@ -649,10 +663,6 @@
 
 fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, [])
 
-(* Syntax: <name> *)
-fun parse_satallax_core_line x =
-  (scan_general_id --| Scan.option ($$ " ") >> (single o core_inference satallax_core_rule)) x
-
 (* Syntax: SZS core <name> ... <name> *)
 fun parse_z3_tptp_core_line x =
   (Scan.this_string "SZS core" |-- Scan.repeat ($$ " " |-- scan_general_id)
@@ -660,35 +670,17 @@
 
 fun parse_line local_name problem =
   if local_name = leo2N then parse_tstp_thf0_line problem
-  else if local_name = satallaxN then parse_satallax_core_line
   else if local_name = spassN then parse_spass_line
   else if local_name = spass_pirateN then parse_spass_pirate_line
   else if local_name = z3_tptpN then parse_z3_tptp_core_line
   else parse_tstp_line problem
 
-fun parse_proof local_name problem =
-  strip_spaces_except_between_idents
-  #> raw_explode
-  #> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
-       (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat)))
-  #> fst
-
 fun core_of_agsyhol_proof s =
   (case split_lines s of
     "The transformed problem consists of the following conjectures:" :: conj ::
     _ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term)
   | _ => NONE)
 
-fun atp_proof_of_tstplike_proof _ _ "" = []
-  | atp_proof_of_tstplike_proof local_prover problem tstp =
-    (case core_of_agsyhol_proof tstp of
-      SOME facts => facts |> map (core_inference agsyhol_core_rule)
-    | NONE =>
-      tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
-      |> parse_proof local_prover problem
-      |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o pairself #1)))
-      |> local_prover = zipperpositionN ? rev)
-
 fun clean_up_dependencies _ [] = []
   | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =
     (name, role, u, rule, map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::

--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:12 2014 +0200
@@ -498,7 +498,7 @@
 val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
 
 fun add_fact ctxt facts ((_, ss), _, _, rule, deps) =
-  (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule, satallax_core_rule] rule then
+  (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule then
      insert (op =) (short_thm_name ctxt ext, (Global, General))
    else
      I)

--- a/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:12 2014 +0200
@@ -170,7 +170,7 @@
   | find_assumptions_to_inline ths [] _ _ = ths
 
 fun inline_if_needed_and_simplify th assms to_inline no_inline =
-    (case find_assumptions_to_inline [] assms to_inline no_inline of
+    (case find_assumptions_to_inline [th] assms to_inline no_inline of
       [] => ATerm (("$true", [dummy_atype]), [])
   | l => foldl1 (fn (a, b) => ATerm ((tptp_or, [dummy_atype]), [a, b])) l)
 
@@ -315,7 +315,7 @@
           (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat)))
            #> fst)
       else
-        (Scan.error (!! (fn f => raise UNRECOGNIZED_ATP_PROOF ())
+        (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
           (Scan.finite Symbol.stopper (Scan.repeat1 (parse_tstp_thf0_satallax_line))))
           #> fst
           #> rev

--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Jul 30 14:03:12 2014 +0200
@@ -431,9 +431,9 @@
 val satallax_config : atp_config =
   {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
-       "-p hocore -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
+       "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
    proof_delims =
-     [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
+     [("% SZS output start Proof", "% SZS output end Proof")],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
    best_slices =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Jul 30 14:03:12 2014 +0200
@@ -30,6 +30,7 @@
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
 open ATP_Waldmeister
+open ATP_Satallax
 open ATP_Systems
 open Sledgehammer_Util
 open Sledgehammer_Proof_Methods