# HG changeset patch
# User fleury
# Date 1401714618 -7200
# Node ID f0eff6393a32b8fb17d658df93842c87918c236f
# Parent  690cf0d831620b223f6ea6f82ab2a816f59d2e29
basic setup for zipperposition prover

diff -r 690cf0d83162 -r f0eff6393a32 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 02 15:10:18 2014 +0200
@@ -651,10 +651,10 @@
             (override_params prover type_enc (my_timeout time_slice)) fact_override
       in
         if !meth = "sledgehammer_tac" then
-          sledge_tac 0.2 ATP_Systems.vampireN "mono_native"
-          ORELSE' sledge_tac 0.2 ATP_Systems.eN "poly_guards??"
-          ORELSE' sledge_tac 0.2 ATP_Systems.spassN "mono_native"
-          ORELSE' sledge_tac 0.2 ATP_Systems.z3_tptpN "poly_tags??"
+          sledge_tac 0.2 ATP_Proof.vampireN "mono_native"
+          ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??"
+          ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native"
+          ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??"
           ORELSE' SMT_Solver.smt_tac ctxt thms
         else if !meth = "smt" then
           SMT_Solver.smt_tac ctxt thms
diff -r 690cf0d83162 -r f0eff6393a32 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Jun 02 15:10:18 2014 +0200
@@ -89,7 +89,7 @@
   else
     ()
 
-val default_prover = ATP_Systems.eN (* arbitrary ATP *)
+val default_prover = ATP_Proof.eN (* arbitrary ATP *)
 
 fun with_index (i, s) = s ^ "@" ^ string_of_int i
 
diff -r 690cf0d83162 -r f0eff6393a32 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Mon Jun 02 15:10:18 2014 +0200
@@ -209,18 +209,18 @@
             else ""))
           (atp_tac ctxt completeness [] (mult * timeout div frac) prover i)
   in
-    slice 2 0 ATP_Systems.spassN
-    ORELSE slice 2 0 ATP_Systems.vampireN
-    ORELSE slice 2 0 ATP_Systems.eN
-    ORELSE slice 2 0 ATP_Systems.z3_tptpN
-    ORELSE slice 1 1 ATP_Systems.spassN
-    ORELSE slice 1 2 ATP_Systems.eN
-    ORELSE slice 1 1 ATP_Systems.vampireN
-    ORELSE slice 1 2 ATP_Systems.vampireN
+    slice 2 0 ATP_Proof.spassN
+    ORELSE slice 2 0 ATP_Proof.vampireN
+    ORELSE slice 2 0 ATP_Proof.eN
+    ORELSE slice 2 0 ATP_Proof.z3_tptpN
+    ORELSE slice 1 1 ATP_Proof.spassN
+    ORELSE slice 1 2 ATP_Proof.eN
+    ORELSE slice 1 1 ATP_Proof.vampireN
+    ORELSE slice 1 2 ATP_Proof.vampireN
     ORELSE
       (if demo then
-         slice 2 0 ATP_Systems.satallaxN
-         ORELSE slice 2 0 ATP_Systems.leo2N
+         slice 2 0 ATP_Proof.satallaxN
+         ORELSE slice 2 0 ATP_Proof.leo2N
        else
          no_tac)
   end
@@ -238,7 +238,7 @@
   ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
       (auto_tac ctxt
-       THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) ATP_Systems.spassN))
+       THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) ATP_Proof.spassN))
   ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc3" (smt_solver_tac "cvc3" ctxt i)
@@ -286,7 +286,7 @@
       read_tptp_file thy (freeze_problem_consts thy o snd) file_name
     val conj = make_conj assms conjs
     val (last_hope_atp, last_hope_completeness) =
-      if demo then (ATP_Systems.satallaxN, 0) else (ATP_Systems.vampireN, 2)
+      if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2)
   in
     (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
      can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
diff -r 690cf0d83162 -r f0eff6393a32 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 02 15:10:18 2014 +0200
@@ -41,6 +41,28 @@
 
   type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list
 
+  (* Named ATPs *)
+  val agsyholN : string
+  val alt_ergoN : string
+  val dummy_thfN : string
+  val eN : string
+  val e_malesN : string
+  val e_parN : string
+  val e_sineN : string
+  val e_tofofN : string
+  val iproverN : string
+  val iprover_eqN : string
+  val leo2N : string
+  val satallaxN : string
+  val snarkN : string
+  val spassN : string
+  val spass_pirateN : string
+  val vampireN : string
+  val waldmeisterN : string
+  val z3_tptpN : string
+  val zipperpositionN : string
+  val remote_prefix : string
+
   val agsyhol_core_rule : string
   val satallax_core_rule : string
   val spass_input_rule : string
@@ -59,7 +81,7 @@
   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 atp_problem -> string -> string atp_proof
+  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
@@ -71,6 +93,30 @@
 open ATP_Util
 open ATP_Problem
 
+(* Named ATPs *)
+
+val agsyholN = "agsyhol"
+val alt_ergoN = "alt_ergo"
+val dummy_thfN = "dummy_thf" (* for experiments *)
+val eN = "e"
+val e_malesN = "e_males"
+val e_parN = "e_par"
+val e_sineN = "e_sine"
+val e_tofofN = "e_tofof"
+val iproverN = "iprover"
+val iprover_eqN = "iprover_eq"
+val leo2N = "leo2"
+val satallaxN = "satallax"
+val snarkN = "snark"
+val spassN = "spass"
+val spass_pirateN = "spass_pirate"
+val vampireN = "vampire"
+val waldmeisterN = "waldmeister"
+val z3_tptpN = "z3_tptp"
+val zipperpositionN = "zipperposition"
+val remote_prefix = "remote_"
+
+
 val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
 val satallax_core_rule = "__satallax_core" (* arbitrary *)
 val spass_input_rule = "Inp"
@@ -251,7 +297,8 @@
   (Scan.repeat (Scan.option ($$ ",") |-- parse_dependency) >> flat) x
 and parse_file_source x =
   (Scan.this_string "file" |-- $$ "(" |-- scan_general_id
-   -- Scan.option ($$ "," |-- scan_general_id) --| $$ ")") x
+   -- Scan.option ($$ "," |-- scan_general_id
+  --| Scan.option ($$"," |-- $$"[" -- Scan.option scan_general_id --| $$"]") --| $$ ")")) x
 and parse_inference_source x =
   (Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
    --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
@@ -506,14 +553,18 @@
   (Scan.this_string "SZS core" |-- Scan.repeat ($$ " " |-- scan_general_id)
    >> map (core_inference z3_tptp_core_rule)) x
 
-fun parse_line problem =
-  parse_tstp_line problem || parse_z3_tptp_core_line || parse_spass_line || parse_spass_pirate_line
-  || parse_satallax_core_line
-fun parse_proof problem =
+fun parse_line name problem =
+  if name = z3_tptpN then parse_z3_tptp_core_line
+  else if name = spass_pirateN then  parse_spass_pirate_line
+  else if name = spassN then  parse_spass_line
+  else if name = satallaxN then parse_satallax_core_line
+  else parse_tstp_line problem
+
+fun parse_proof name problem =
   strip_spaces_except_between_idents
   #> raw_explode
   #> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
-       (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line problem) >> flat)))
+       (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line name problem) >> flat)))
   #> fst
 
 fun core_of_agsyhol_proof s =
@@ -522,14 +573,15 @@
     _ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term)
   | _ => NONE)
 
-fun atp_proof_of_tstplike_proof _ "" = []
-  | atp_proof_of_tstplike_proof problem tstp =
+fun atp_proof_of_tstplike_proof prover _ ""  = []
+  | atp_proof_of_tstplike_proof 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 problem
-      |> perhaps (try (sort (vampire_step_name_ord o pairself #1))))
+      |> parse_proof prover problem
+      |> prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o pairself #1)))
+      |> prover = zipperpositionN ? rev)
 
 fun clean_up_dependencies _ [] = []
   | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =
diff -r 690cf0d83162 -r f0eff6393a32 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 02 15:10:18 2014 +0200
@@ -48,25 +48,6 @@
   val spass_H2NuVS0Red2 : string
   val spass_H2SOS : string
   val spass_extra_options : string Config.T
-  val agsyholN : string
-  val alt_ergoN : string
-  val dummy_thfN : string
-  val eN : string
-  val e_malesN : string
-  val e_parN : string
-  val e_sineN : string
-  val e_tofofN : string
-  val iproverN : string
-  val iprover_eqN : string
-  val leo2N : string
-  val satallaxN : string
-  val snarkN : string
-  val spassN : string
-  val spass_pirateN : string
-  val vampireN : string
-  val waldmeisterN : string
-  val z3_tptpN : string
-  val remote_prefix : string
   val remote_atp :
     string -> string -> string list -> (string * string) list
     -> (atp_failure * string) list -> atp_formula_role
@@ -157,28 +138,6 @@
 val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
 val known_says_failures = known_szs_failures (prefix " says ")
 
-(* named ATPs *)
-
-val agsyholN = "agsyhol"
-val alt_ergoN = "alt_ergo"
-val dummy_thfN = "dummy_thf" (* for experiments *)
-val eN = "e"
-val e_malesN = "e_males"
-val e_parN = "e_par"
-val e_sineN = "e_sine"
-val e_tofofN = "e_tofof"
-val iproverN = "iprover"
-val iprover_eqN = "iprover_eq"
-val leo2N = "leo2"
-val satallaxN = "satallax"
-val snarkN = "snark"
-val spassN = "spass"
-val spass_pirateN = "spass_pirate"
-val vampireN = "vampire"
-val waldmeisterN = "waldmeister"
-val z3_tptpN = "z3_tptp"
-val remote_prefix = "remote_"
-
 structure Data = Theory_Data
 (
   type T = ((unit -> atp_config) * stamp) Symtab.table
@@ -634,6 +593,27 @@
 val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
 
 
+(* Zipperposition*)
+
+val zipperposition_tff1 = TFF Polymorphic
+
+val zipperposition_config : atp_config =
+  {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
+   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+       "-print none -proof tstp -print-types -timeout " ^
+       string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
+   proof_delims = tstp_proof_delims,
+   known_failures = known_szs_status_failures,
+   prem_role = Hypothesis,
+   best_slices = fn _ =>
+     (* FUDGE *)
+     [(1.0, (((100, ""), alt_ergo_tff1, "poly_native", liftingN, false), ""))],
+   best_max_mono_iters = default_max_mono_iters,
+   best_max_new_mono_instances = default_max_new_mono_instances}
+
+val zipperposition = (zipperpositionN, fn () => zipperposition_config)
+
+
 (* Not really a prover: Experimental Polymorphic THF and DFG output *)
 
 fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
@@ -816,8 +796,8 @@
 
 val atps =
   [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
-   z3_tptp, dummy_thf, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof, remote_iprover,
-   remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_snark,
+   z3_tptp,zipperposition, dummy_thf, 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]
 
 val setup = fold add_atp atps
diff -r 690cf0d83162 -r f0eff6393a32 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jun 02 15:10:18 2014 +0200
@@ -18,6 +18,7 @@
 open ATP_Util
 open ATP_Systems
 open ATP_Problem_Generate
+open ATP_Proof
 open ATP_Proof_Reconstruct
 open Sledgehammer_Util
 open Sledgehammer_Fact
diff -r 690cf0d83162 -r f0eff6393a32 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jun 02 15:10:18 2014 +0200
@@ -123,8 +123,8 @@
 
     fun isar_proof_of () =
       let
-        val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
-          atp_proof, goal) = try isar_params ()
+        val (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
+          atp_proof, goal) = isar_params ()
 
         val systematic_methods = insert (op =) (Metis_Method alt_metis_args) systematic_methods0
 
diff -r 690cf0d83162 -r f0eff6393a32 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Jun 02 15:10:18 2014 +0200
@@ -122,7 +122,7 @@
 fun chain_qs_lfs NONE lfs = ([], lfs)
   | chain_qs_lfs (SOME l0) lfs =
     if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
-fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
+fun chain_isar_step lbl (x as Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
     let val (qs', lfs) = chain_qs_lfs lbl lfs in
       Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
     end
diff -r 690cf0d83162 -r f0eff6393a32 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Jun 02 15:10:18 2014 +0200
@@ -95,9 +95,10 @@
 structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
 struct
 
+open ATP_Proof
 open ATP_Util
+open ATP_Systems
 open ATP_Problem
-open ATP_Systems
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
 open Metis_Tactic
diff -r 690cf0d83162 -r f0eff6393a32 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Jun 02 15:10:18 2014 +0200
@@ -287,7 +287,7 @@
               |> (fn accum as (output, _) =>
                      (accum,
                       extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
-                      |>> atp_proof_of_tstplike_proof atp_problem
+                      |>> atp_proof_of_tstplike_proof name atp_problem
                       handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
               handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
             val outcome =