# HG changeset patch
# User wenzelm
# Date 1618258591 -7200
# Node ID bdba138d462d70f0e4ae3df8f827fa0e8586afea
# Parent  355af2d1b81780288e5fcc75f90ad9c47ef1dd62
clarified signature: more structured arguments, notably for remote provers;

diff -r 355af2d1b817 -r bdba138d462d src/HOL/Tools/ATP/system_on_tptp.ML
--- a/src/HOL/Tools/ATP/system_on_tptp.ML	Mon Apr 12 21:48:04 2021 +0200
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML	Mon Apr 12 22:16:31 2021 +0200
@@ -8,7 +8,7 @@
 sig
   val get_url: unit -> string
   val list_systems: unit -> {url: string, systems: string list}
-  val run_system_encoded: string -> {output: string, timing: Time.time}
+  val run_system_encoded: string list -> {output: string, timing: Time.time}
   val run_system: {system: string, problem: Path.T, extra: string, timeout: Time.time} ->
     {output: string, timing: Time.time}
 end
@@ -25,15 +25,12 @@
   in {url = url, systems = systems} end
 
 fun run_system_encoded args =
-  cat_strings0 [get_url (), args]
+  (get_url () :: args)
   |> \<^scala>\<open>SystemOnTPTP.run_system\<close>
-  |> split_strings0 |> (fn [output, timing] =>
-    {output = output, timing = Time.fromMilliseconds (Value.parse_int timing)})
+  |> (fn [a, b] => {output = a, timing = Time.fromMilliseconds (Value.parse_int b)})
 
 fun run_system {system, problem, extra, timeout} =
-  cat_strings0
-    [system, Isabelle_System.absolute_path problem,
-      extra, string_of_int (Time.toMilliseconds timeout)]
+  [system, Isabelle_System.absolute_path problem, extra, string_of_int (Time.toMilliseconds timeout)]
   |> run_system_encoded
 
 end
diff -r 355af2d1b817 -r bdba138d462d src/HOL/Tools/ATP/system_on_tptp.scala
--- a/src/HOL/Tools/ATP/system_on_tptp.scala	Mon Apr 12 21:48:04 2021 +0200
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Mon Apr 12 22:16:31 2021 +0200
@@ -69,12 +69,12 @@
     post_request(url, paramaters, timeout = timeout + Time.seconds(15))
   }
 
-  object Run_System extends Scala.Fun_String("SystemOnTPTP.run_system", thread = true)
+  object Run_System extends Scala.Fun_Strings("SystemOnTPTP.run_system", thread = true)
   {
     val here = Scala_Project.here
-    def apply(arg: String): String =
+    def apply(args: List[String]): List[String] =
     {
-      val List(url, system, problem_path, extra, Value.Int(timeout)) = Library.split_strings0(arg)
+      val List(url, system, problem_path, extra, Value.Int(timeout)) = args
       val problem = File.read(Path.explode(problem_path))
 
       val res = run_system(Url(url), system, problem, extra = extra, timeout = Time.ms(timeout))
@@ -85,7 +85,7 @@
       if (split_lines(text).exists(_.startsWith(bad_prover))) {
         error("The ATP " + quote(system) + " is not available at SystemOnTPTP")
       }
-      else Library.cat_strings0(List(text, timing.toString))
+      else List(text, timing.toString)
     }
   }
 }
diff -r 355af2d1b817 -r bdba138d462d src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Apr 12 21:48:04 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Apr 12 22:16:31 2021 +0200
@@ -16,7 +16,7 @@
   type atp_config =
     {exec : string list * string list,
      arguments : Proof.context -> bool -> string -> Time.time -> Path.T ->
-       term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
+       term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string list,
      proof_delims : (string * string) list,
      known_failures : (atp_failure * string) list,
      prem_role : atp_formula_role,
@@ -76,7 +76,7 @@
 type atp_config =
   {exec : string list * string list,
    arguments : Proof.context -> bool -> string -> Time.time -> Path.T ->
-     term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
+     term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string list,
    proof_delims : (string * string) list,
    known_failures : (atp_failure * string) list,
    prem_role : atp_formula_role,
@@ -163,7 +163,7 @@
 val agsyhol_config : atp_config =
   {exec = (["AGSYHOL_HOME"], ["agsyHOL"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-     "--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem,
+     ["--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem],
    proof_delims = tstp_proof_delims,
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
@@ -181,8 +181,8 @@
 val alt_ergo_config : atp_config =
   {exec = (["WHY3_HOME"], ["why3"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-     "--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^
-     " " ^ File.bash_path problem,
+     ["--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^
+      " " ^ File.bash_path problem],
    proof_delims = [],
    known_failures =
      [(ProofMissing, ": Valid"),
@@ -271,13 +271,13 @@
   {exec = (["E_HOME"], ["eprover"]),
    arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn problem =>
      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
-       "--auto-schedule --tstp-in --tstp-out --silent " ^
-       e_selection_weight_arguments ctxt heuristic sel_weights ^
-       e_term_order_info_arguments gen_weights gen_prec ord_info ^
-       "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
-       "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
-       " --proof-object=1 " ^
-       File.bash_path problem,
+       ["--auto-schedule --tstp-in --tstp-out --silent " ^
+        e_selection_weight_arguments ctxt heuristic sel_weights ^
+        e_term_order_info_arguments gen_weights gen_prec ord_info ^
+        "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
+        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
+        " --proof-object=1 " ^
+        File.bash_path problem],
    proof_delims =
      [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
      tstp_proof_delims,
@@ -318,9 +318,9 @@
 val iprover_config : atp_config =
   {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-     "--clausifier \"$E_HOME\"/eprover " ^
-     "--clausifier_options \"--tstp-format --silent --cnf\" " ^
-     "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem,
+     ["--clausifier \"$E_HOME\"/eprover " ^
+      "--clausifier_options \"--tstp-format --silent --cnf\" " ^
+      "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem],
    proof_delims = tstp_proof_delims,
    known_failures =
      [(ProofIncomplete, "% SZS output start CNFRefutation")] @
@@ -340,11 +340,11 @@
 val leo2_config : atp_config =
   {exec = (["LEO2_HOME"], ["leo.opt", "leo"]),
    arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => fn _ =>
-     "--foatp e --atp e=\"$E_HOME\"/eprover \
-     \--atp epclextract=\"$E_HOME\"/epclextract \
-     \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
-     (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^
-     File.bash_path problem,
+     ["--foatp e --atp e=\"$E_HOME\"/eprover \
+      \--atp epclextract=\"$E_HOME\"/epclextract \
+      \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
+      (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^
+      File.bash_path problem],
    proof_delims = tstp_proof_delims,
    known_failures =
      [(TimedOut, "CPU time limit exceeded, terminating"),
@@ -366,9 +366,9 @@
 val leo3_config : atp_config =
   {exec = (["LEO3_HOME"], ["leo3"]),
    arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => fn _ =>
-     File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC4_SOLVER\" --atp e=\"$E_HOME\"/eprover \
-     \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
-     (if full_proofs then "--nleq --naeq " else ""),
+     [File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC4_SOLVER\" --atp e=\"$E_HOME\"/eprover \
+      \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
+      (if full_proofs then "--nleq --naeq " else "")],
    proof_delims = tstp_proof_delims,
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
@@ -387,10 +387,10 @@
 val satallax_config : atp_config =
   {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-     (case getenv "E_HOME" of
-       "" => ""
-     | home => "-E " ^ home ^ "/eprover ") ^
-     "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem,
+     [(case getenv "E_HOME" of
+        "" => ""
+      | home => "-E " ^ home ^ "/eprover ") ^
+      "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem],
    proof_delims =
      [("% SZS output start Proof", "% SZS output end Proof")],
    known_failures = known_szs_status_failures,
@@ -419,9 +419,9 @@
   in
     {exec = (["SPASS_HOME"], ["SPASS"]),
      arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn problem => fn _ =>
-       "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^
-       "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
-       |> extra_options <> "" ? prefix (extra_options ^ " "),
+       ["-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^
+        "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
+        |> extra_options <> "" ? prefix (extra_options ^ " ")],
      proof_delims = [("Here is a proof", "Formulae used in the proof")],
      known_failures =
        [(GaveUp, "SPASS beiseite: Completion found"),
@@ -491,9 +491,9 @@
     {exec = (["VAMPIRE_HOME"], ["vampire"]),
      arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
        (check_vampire_noncommercial ();
-        vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
-        " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem
-        |> sos = sosN ? prefix "--sos on "),
+        [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
+         " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem
+         |> sos = sosN ? prefix "--sos on "]),
      proof_delims =
        [("=========== Refutation ==========",
          "======= End of refutation =======")] @
@@ -527,7 +527,7 @@
   in
     {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]),
      arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-       "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ File.bash_path problem,
+       ["-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ File.bash_path problem],
      proof_delims = [("SZS status Theorem", "")],
      known_failures = known_szs_status_failures,
      prem_role = Hypothesis,
@@ -556,8 +556,8 @@
   in
     {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
      arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ =>
-       "--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
-       |> extra_options <> "" ? prefix (extra_options ^ " "),
+       ["--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
+        |> extra_options <> "" ? prefix (extra_options ^ " ")],
      proof_delims = tstp_proof_delims,
      known_failures = known_szs_status_failures,
      prem_role = Hypothesis,
@@ -615,10 +615,9 @@
 fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice =
   {exec = isabelle_scala_function,
    arguments = fn _ => fn _ => fn command => fn timeout => fn problem => fn _ =>
-    (cat_strings0
      [the_remote_system system_name system_versions,
       Isabelle_System.absolute_path problem,
-      command, string_of_int (Int.min (max_remote_secs, to_secs 1 timeout) * 1000)]),
+      command, string_of_int (Int.min (max_remote_secs, to_secs 1 timeout) * 1000)],
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_says_failures,
    prem_role = prem_role,
@@ -676,7 +675,7 @@
 
 fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
   {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
-   arguments = K (K (K (K (K (K ""))))),
+   arguments = K (K (K (K (K (K []))))),
    proof_delims = [],
    known_failures = known_szs_status_failures,
    prem_role = prem_role,
diff -r 355af2d1b817 -r bdba138d462d src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Apr 12 21:48:04 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Apr 12 22:16:31 2021 +0200
@@ -264,7 +264,7 @@
             val ord = effective_term_order ctxt name
             val args =
               arguments ctxt full_proofs extra slice_timeout prob_path (ord, ord_info, sel_weights)
-            val command = File.bash_path executable ^ " " ^ args
+            val command = space_implode " " (File.bash_path executable :: args)
 
             fun run_command () =
               if exec = isabelle_scala_function then