# HG changeset patch
# User blanchet
# Date 1403590797 -7200
# Node ID 4e619ee65a6125146a442f35f84274c523ae1be2
# Parent  d20cf3ec7fa73e39d13a1479769443261aca7094
added 'dummy_thf_ml' prover for experiments with HOLyHammer

diff -r d20cf3ec7fa7 -r 4e619ee65a61 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 24 08:19:56 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 24 08:19:57 2014 +0200
@@ -608,16 +608,17 @@
     SOME s => (SOME Type_Class_Polymorphic, s)
   | NONE =>
     (case try (unprefix "poly_") s of
-      (* It's still unclear whether all TFF1 implementations will support type signatures such as
-         "!>[A : $tType] : $o", with phantom type variables. *)
       SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s)
     | NONE =>
-      (case try (unprefix "raw_mono_") s of
-        SOME s => (SOME Raw_Monomorphic, s)
+      (case try (unprefix "ml_poly_") s of
+        SOME s => (SOME (Raw_Polymorphic Without_Phantom_Type_Vars), s)
       | NONE =>
-        (case try (unprefix "mono_") s of
-          SOME s => (SOME Mangled_Monomorphic, s)
-        | NONE => (NONE, s)))))
+        (case try (unprefix "raw_mono_") s of
+          SOME s => (SOME Raw_Monomorphic, s)
+        | NONE =>
+          (case try (unprefix "mono_") s of
+            SOME s => (SOME Mangled_Monomorphic, s)
+          | NONE => (NONE, s))))))
   ||> (fn s =>
        (case try_unsuffixes queries s of
          SOME s =>
diff -r d20cf3ec7fa7 -r 4e619ee65a61 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Jun 24 08:19:56 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Jun 24 08:19:57 2014 +0200
@@ -46,6 +46,7 @@
   val agsyholN : string
   val alt_ergoN : string
   val dummy_thfN : string
+  val dummy_thf_mlN : string
   val eN : string
   val e_malesN : string
   val e_parN : string
@@ -100,6 +101,7 @@
 val agsyholN = "agsyhol"
 val alt_ergoN = "alt_ergo"
 val dummy_thfN = "dummy_thf" (* for experiments *)
+val dummy_thf_mlN = "dummy_thf_ml" (* for experiments *)
 val eN = "e"
 val e_malesN = "e_males"
 val e_parN = "e_par"
diff -r d20cf3ec7fa7 -r 4e619ee65a61 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Jun 24 08:19:56 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Jun 24 08:19:57 2014 +0200
@@ -628,9 +628,13 @@
    best_max_new_mono_instances = default_max_new_mono_instances}
 
 val dummy_thf_format = THF (Polymorphic, THF_With_Choice)
+
 val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
 
+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"]),
@@ -797,9 +801,9 @@
 
 val atps =
   [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
-   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, remote_waldmeister_new]
+   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]
 
 val _ = Theory.setup (fold add_atp atps)