# HG changeset patch
# User blanchet
# Date 1425397065 -3600
# Node ID 012c6165bbd2f19c16d9f6772a0e38b85ce634b9
# Parent  913c4afb03887a77ed69753aef8791591d0d4a0b
SPASS-Pirate is now called Pirate

diff -r 913c4afb0388 -r 012c6165bbd2 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Tue Mar 03 16:37:45 2015 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Tue Mar 03 16:37:45 2015 +0100
@@ -920,6 +920,10 @@
 \item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
 runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
+\item[\labelitemi] \textbf{\textit{remote\_pirate}:} Pirate is a
+highly experimental first-order resolution prover developed by Daniel Wand.
+The remote version of Pirate run on a private server he generously set up.
+
 \item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of
 Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
@@ -928,11 +932,6 @@
 TPTP typed first-order format (TFF0). The remote version of SNARK runs on
 Geoff Sutcliffe's Miami servers.
 
-\item[\labelitemi] \textbf{\textit{remote\_spass\_pirate}:} SPASS-Pirate is a
-highly experimental first-order resolution prover developed by Daniel Wand.
-The remote version of SPASS-Pirate run on a private server set up by Daniel
-Wand.
-
 \item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
 Vampire runs on Geoff Sutcliffe's Miami servers.
 
@@ -944,9 +943,9 @@
 \end{enum}
 
 By default, Sledgehammer runs a subset of CVC4, E, E-SInE, SPASS, Vampire,
-veriT, and Z3 in parallel---either locally or remotely, depending on the number
-of processor cores available and on which provers are actually installed.
-It is generally a good idea to run several provers in parallel.
+veriT, and Z3 in parallel, either locally or remotely---depending on the number
+of processor cores available and on which provers are actually installed. It is
+generally a good idea to run several provers in parallel.
 
 \opnodefault{prover}{string}
 Alias for \textit{provers}.
diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML	Tue Mar 03 16:37:45 2015 +0100
@@ -36,7 +36,7 @@
 
 fun atp_of_format (THF (Polymorphic, _)) = dummy_thfN
   | atp_of_format (THF (Monomorphic, _)) = satallaxN
-  | atp_of_format (DFG Polymorphic) = spass_pirateN
+  | atp_of_format (DFG Polymorphic) = pirateN
   | atp_of_format (DFG Monomorphic) = spassN
   | atp_of_format (TFF Polymorphic) = alt_ergoN
   | atp_of_format (TFF Monomorphic) = vampireN
diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Mar 03 16:37:45 2015 +0100
@@ -57,10 +57,10 @@
   val iproverN : string
   val iprover_eqN : string
   val leo2N : string
+  val pirateN : string
   val satallaxN : string
   val snarkN : string
   val spassN : string
-  val spass_pirateN : string
   val vampireN : string
   val waldmeisterN : string
   val waldmeister_newN : string
@@ -126,10 +126,10 @@
 val iproverN = "iprover"
 val iprover_eqN = "iprover_eq"
 val leo2N = "leo2"
+val pirateN = "pirate"
 val satallaxN = "satallax"
 val snarkN = "snark"
 val spassN = "spass"
-val spass_pirateN = "spass_pirate"
 val vampireN = "vampire"
 val waldmeisterN = "waldmeister"
 val waldmeister_newN = "waldmeister_new"
@@ -654,22 +654,22 @@
    >> (fn ((((num, rule), deps), u), names) =>
           [((num, these names), Unknown, u, rule, map (rpair []) deps)])) x
 
-fun parse_spass_pirate_dependency x = (Scan.option ($$ "-") |-- scan_general_id) x
-fun parse_spass_pirate_dependencies x =
-  Scan.repeat (parse_spass_pirate_dependency --| Scan.option ($$ "," || $$ " ")) x
-fun parse_spass_pirate_file_source x =
+fun parse_pirate_dependency x = (Scan.option ($$ "-") |-- scan_general_id) x
+fun parse_pirate_dependencies x =
+  Scan.repeat (parse_pirate_dependency --| Scan.option ($$ "," || $$ " ")) x
+fun parse_pirate_file_source x =
   ((Scan.this_string "Input" || Scan.this_string "Conj") |-- $$ "(" |-- scan_general_id
      --| $$ ")") x
-fun parse_spass_pirate_inference_source x =
-  (scan_general_id -- ($$ "(" |-- parse_spass_pirate_dependencies --| $$ ")")) x
-fun parse_spass_pirate_source x =
-  (parse_spass_pirate_file_source >> (fn s => File_Source ("", SOME s))
-   || parse_spass_pirate_inference_source >> Inference_Source) x
+fun parse_pirate_inference_source x =
+  (scan_general_id -- ($$ "(" |-- parse_pirate_dependencies --| $$ ")")) x
+fun parse_pirate_source x =
+  (parse_pirate_file_source >> (fn s => File_Source ("", SOME s))
+   || parse_pirate_inference_source >> Inference_Source) x
 
 (* Syntax: <num> <stuff> || <atoms> -> <atoms> . origin\(<origin>\) *)
-fun parse_spass_pirate_line x =
+fun parse_pirate_line x =
   (scan_general_id --| Scan.repeat (~$$ "|") -- parse_horn_clause --| $$ "."
-     --| Scan.this_string "origin" --| $$ "(" -- parse_spass_pirate_source --| $$ ")"
+     --| Scan.this_string "origin" --| $$ "(" -- parse_pirate_source --| $$ ")"
    >> (fn ((((num, u), source))) =>
      let
        val (names, rule, deps) =
@@ -690,7 +690,7 @@
 fun parse_line local_name problem =
   if local_name = leo2N then parse_tstp_thf0_line problem
   else if local_name = spassN then parse_spass_line
-  else if local_name = spass_pirateN then parse_spass_pirate_line
+  else if local_name = pirateN then parse_pirate_line
   else if local_name = z3_tptpN then parse_z3_tptp_core_line
   else parse_tstp_line problem
 
diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 03 16:37:45 2015 +0100
@@ -57,7 +57,7 @@
     int Symtab.table -> string atp_proof -> (term, string) atp_step list
   val repair_waldmeister_endgame : (term, 'a) atp_step list -> (term, 'a) atp_step list
   val infer_formulas_types : Proof.context -> term list -> term list
-  val introduce_spass_skolems : (term, string) atp_step list -> (term, string) atp_step list
+  val introduce_spassy_skolems : (term, string) atp_step list -> (term, string) atp_step list
   val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list ->
     (term, string) atp_step list
 end;
@@ -710,7 +710,7 @@
     subst_vars ([], subst) t
   end
 
-fun introduce_spass_skolems proof =
+fun introduce_spassy_skolems proof =
   let
     fun add_skolem (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s
       | add_skolem _ = I
diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 03 16:37:45 2015 +0100
@@ -614,18 +614,18 @@
 val dummy_thf_ml_config = dummy_config Hypothesis dummy_thf_format "ml_poly_native_higher" false
 val dummy_thf_ml = (dummy_thf_mlN, fn () => dummy_thf_ml_config)
 
-val spass_pirate_format = DFG Polymorphic
-val remote_spass_pirate_config : atp_config =
-  {exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_pirate"]),
+val pirate_format = DFG Polymorphic
+val remote_pirate_config : atp_config =
+  {exec = K (["ISABELLE_ATP"], ["scripts/remote_pirate"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
      string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
    proof_delims = [("Involved clauses:", "Involved clauses:")],
    known_failures = known_szs_status_failures,
    prem_role = #prem_role spass_config,
-   best_slices = K [(1.0, (((200, ""), spass_pirate_format, "tc_native", combsN, true), ""))],
+   best_slices = K [(1.0, (((200, ""), pirate_format, "tc_native", combsN, true), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
-val remote_spass_pirate = (remote_prefix ^ spass_pirateN, fn () => remote_spass_pirate_config)
+val remote_pirate = (remote_prefix ^ pirateN, fn () => remote_pirate_config)
 
 
 (* Remote ATP invocation via SystemOnTPTP *)
@@ -764,7 +764,7 @@
   let val ord = Config.get ctxt term_order in
     if ord = smartN then
       {is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN),
-       gen_simp = String.isSuffix spass_pirateN atp}
+       gen_simp = String.isSuffix pirateN atp}
     else
       let val is_lpo = String.isSubstring lpoN ord in
         {is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
@@ -776,7 +776,7 @@
   [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
    z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine,
    remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire,
-   remote_snark, remote_spass_pirate, remote_waldmeister, remote_waldmeister_new]
+   remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new]
 
 val _ = Theory.setup (fold add_atp atps)
 
diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/ATP/scripts/remote_pirate
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/scripts/remote_pirate	Tue Mar 03 16:37:45 2015 +0100
@@ -0,0 +1,2 @@
+#!/usr/bin/env bash
+curl -s -F file=@"$2" "http://91.228.53.68:51642/solve/pirate/"$1"s"
diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/ATP/scripts/remote_spass_pirate
--- a/src/HOL/Tools/ATP/scripts/remote_spass_pirate	Tue Mar 03 16:37:45 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-#!/usr/bin/env bash
-curl -s -F file=@"$2" "http://91.228.53.68:51642/solve/pirate/"$1"s"
diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Mar 03 16:37:45 2015 +0100
@@ -50,8 +50,8 @@
 val e_definition_rule = "definition"
 val e_skolemize_rule = "skolemize"
 val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg"
+val pirate_datatype_rule = "DT"
 val satallax_skolemize_rule = "tab_ex"
-val spass_pirate_datatype_rule = "DT"
 val vampire_skolemisation_rule = "skolemisation"
 val veriT_la_generic_rule = "la_generic"
 val veriT_simp_arith_rule = "simp_arith"
@@ -73,7 +73,7 @@
 fun is_arith_rule rule =
   String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse
   rule = veriT_la_generic_rule
-val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule
+val is_datatype_rule = String.isPrefix pirate_datatype_rule
 
 fun raw_label_of_num num = (num, 0)
 
diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Mar 03 16:37:45 2015 +0100
@@ -144,7 +144,7 @@
     val full_proofs = isar_proofs |> the_default (mode = Minimize)
     val local_name = perhaps (try (unprefix remote_prefix)) name
     val waldmeister_new = (local_name = waldmeister_newN)
-    val spass = (local_name = spassN orelse local_name = spass_pirateN)
+    val spassy = (local_name = pirateN orelse local_name = spassN)
 
     val atp_mode = if Config.get ctxt atp_completish then Sledgehammer_Completish else Sledgehammer
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
@@ -381,7 +381,7 @@
                       atp_proof
                       |> (if waldmeister_new then termify_waldmeister_proof ctxt pool
                           else termify_atp_proof ctxt name format type_enc pool lifted sym_tab)
-                      |> spass ? introduce_spass_skolems
+                      |> spassy ? introduce_spassy_skolems
                       |> (if waldmeister_new then introduce_waldmeister_skolems (the wm_info) else I)
                       |> factify_atp_proof (map fst used_from) hyp_ts concl_t
                   in