# HG changeset patch
# User blanchet
# Date 1314713265 -7200
# Node ID 3a8a31be92d23d565ed5f0f2f3c8b79900e7ab85
# Parent  0a1dfc6365e98908f9cb7a3b0f7a0862607216ed
added dummy PFF prover, for debugging purposes

diff -r 0a1dfc6365e9 -r 3a8a31be92d2 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:07:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:07:45 2011 +0200
@@ -37,13 +37,14 @@
   val e_sym_offs_weight_base : real Config.T
   val e_sym_offs_weight_span : real Config.T
   val eN : string
+  val e_sineN : string
+  val e_tofofN : string
+  val leo2N : string
+  val pffN : string
+  val satallaxN : string
+  val snarkN : string
   val spassN : string
   val vampireN : string
-  val leo2N : string
-  val satallaxN : string
-  val e_sineN : string
-  val snarkN : string
-  val e_tofofN : string
   val waldmeisterN : string
   val z3_tptpN : string
   val remote_prefix : string
@@ -100,15 +101,16 @@
 (* named ATPs *)
 
 val eN = "e"
+val e_sineN = "e_sine"
+val e_tofofN = "e_tofof"
 val leo2N = "leo2"
+val pffN = "pff"
 val satallaxN = "satallax"
+val snarkN = "snark"
 val spassN = "spass"
 val vampireN = "vampire"
+val waldmeisterN = "waldmeister"
 val z3_tptpN = "z3_tptp"
-val e_sineN = "e_sine"
-val snarkN = "snark"
-val e_tofofN = "e_tofof"
-val waldmeisterN = "waldmeister"
 val remote_prefix = "remote_"
 
 structure Data = Theory_Data
@@ -380,6 +382,22 @@
 
 val z3_tptp = (z3_tptpN, z3_tptp_config)
 
+(* Not really a prover: Experimental PFF (Polymorphic TFF) output *)
+
+val poly_tff = TFF (TFF_Polymorphic, TFF_Implicit)
+
+val pff_config : atp_config =
+  {exec = ("HOME", ""), (* dummy *)
+   required_execs = [],
+   arguments = K (K (K (K (K "")))),
+   proof_delims = [],
+   known_failures = [],
+   conj_sym_kind = Hypothesis,
+   prem_kind = Hypothesis,
+   best_slices = K [(1.0, (false, (200, poly_tff, "poly_simple", "")))]}
+
+val pff = (pffN, pff_config)
+
 
 (* Remote ATP invocation via SystemOnTPTP *)
 
@@ -510,7 +528,7 @@
   Synchronized.change systems (fn _ => get_systems ())
 
 val atps =
-  [e, leo2, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
+  [e, leo2, pff, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
    remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
    remote_e_tofof, remote_waldmeister]
 val setup = fold add_atp atps