added lambda-free HO output for Ehoh (higher-order E prototype)
authorblanchet
Tue, 22 May 2018 17:15:02 +0200
changeset 68251 c45067867860
parent 68250 949d93804740
child 68252 79c437817348
child 68254 54a127873735
added lambda-free HO output for Ehoh (higher-order E prototype)
src/Doc/Sledgehammer/document/root.tex
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/ATP/atp_systems.ML
--- a/src/Doc/Sledgehammer/document/root.tex	Tue May 22 11:08:37 2018 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Tue May 22 17:15:02 2018 +0200
@@ -768,6 +768,10 @@
 Be aware that E-Par is experimental software. It has been known to generate
 zombie processes. Use at your own risks.
 
+\item[\labelitemi] \textbf{\textit{ehoh}:} Ehoh is an experimental version of
+E that supports a $\lambda$-free fragment of higher-order logic. Use at your
+own risks.
+
 \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure
 instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}.
 To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue May 22 11:08:37 2018 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue May 22 17:15:02 2018 +0200
@@ -32,7 +32,7 @@
      gen_simp : bool}
 
   datatype polymorphism = Monomorphic | Polymorphic
-  datatype thf_choice = THF_Without_Choice | THF_With_Choice
+  datatype thf_choice = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
 
   datatype atp_format =
     CNF |
@@ -188,7 +188,7 @@
    gen_simp : bool}
 
 datatype polymorphism = Monomorphic | Polymorphic
-datatype thf_choice = THF_Without_Choice | THF_With_Choice
+datatype thf_choice = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
 
 datatype atp_format =
   CNF |
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue May 22 11:08:37 2018 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue May 22 17:15:02 2018 +0200
@@ -162,6 +162,9 @@
 
 fun is_type_enc_native (Native _) = true
   | is_type_enc_native _ = false
+fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _)) = false
+  | is_type_enc_full_higher_order (Native (Higher_Order _, _, _)) = true
+  | is_type_enc_full_higher_order _ = false
 fun is_type_enc_higher_order (Native (Higher_Order _, _, _)) = true
   | is_type_enc_higher_order _ = false
 
@@ -668,17 +671,22 @@
         | _ => raise Same.SAME))
   handle Same.SAME => error ("Unknown type encoding: " ^ quote s)
 
-fun adjust_order THF_Without_Choice (Higher_Order _) =
-    Higher_Order THF_Without_Choice
-  | adjust_order _ type_enc = type_enc
+fun min_hologic THF_Lambda_Free _ = THF_Lambda_Free
+  | min_hologic _ THF_Lambda_Free = THF_Lambda_Free
+  | min_hologic THF_Without_Choice _ = THF_Without_Choice
+  | min_hologic _ THF_Without_Choice = THF_Without_Choice
+  | min_hologic _ _ = THF_With_Choice
+
+fun adjust_hologic hologic (Higher_Order hologic') = Higher_Order (min_hologic hologic hologic')
+  | adjust_hologic _ type_enc = type_enc
 
 fun no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars
   | no_type_classes poly = poly
 
-fun adjust_type_enc (THF (Polymorphic, choice)) (Native (order, poly, level)) =
-    Native (adjust_order choice order, no_type_classes poly, level)
-  | adjust_type_enc (THF (Monomorphic, choice)) (Native (order, _, level)) =
-    Native (adjust_order choice order, Mangled_Monomorphic, level)
+fun adjust_type_enc (THF (Polymorphic, hologic)) (Native (order, poly, level)) =
+    Native (adjust_hologic hologic order, no_type_classes poly, level)
+  | adjust_type_enc (THF (Monomorphic, hologic)) (Native (order, _, level)) =
+    Native (adjust_hologic hologic order, Mangled_Monomorphic, level)
   | adjust_type_enc (TFF Monomorphic) (Native (_, _, level)) =
     Native (First_Order, Mangled_Monomorphic, level)
   | adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) =
@@ -881,14 +889,15 @@
 fun raw_atp_type_of_typ type_enc =
   let
     fun term (Type (s, Ts)) =
-      AType ((case (is_type_enc_higher_order type_enc, s) of
-               (true, @{type_name bool}) => `I tptp_bool_type
-             | (true, @{type_name fun}) => `I tptp_fun_type
-             | _ =>
-               if s = fused_infinite_type_name andalso is_type_enc_native type_enc then
-                 `I tptp_individual_type
-               else
-                 `make_fixed_type_const s, []), map term Ts)
+      AType
+        ((if s = @{type_name fun} andalso is_type_enc_higher_order type_enc then
+            `I tptp_fun_type
+          else if s = @{type_name bool} andalso is_type_enc_full_higher_order type_enc then
+            `I tptp_bool_type
+          else if s = fused_infinite_type_name andalso is_type_enc_native type_enc then
+            `I tptp_individual_type
+          else
+            `make_fixed_type_const s, []), map term Ts)
     | term (TFree (s, _)) = AType ((`make_tfree s, []), [])
     | term (TVar z) = AType ((tvar_name z, []), [])
   in term end
@@ -927,13 +936,22 @@
       if is_type_enc_polymorphic type_enc then to_poly_atype
       else to_mangled_atype
     fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
+    fun to_ho (ty as AType (((s, _), _), tys)) =
+        if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
+      | to_ho _ = raise Fail "unexpected type"
+    fun to_lfho (ty as AType (((s, _), _), tys)) =
+        if s = tptp_fun_type then to_afun to_ho to_lfho tys
+        else if pred_sym then bool_atype
+        else to_atype ty
+      | to_lfho _ = raise Fail "unexpected type"
     fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
       | to_fo ary (AType (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
       | to_fo _ _ = raise Fail "unexpected type"
-    fun to_ho (ty as AType (((s, _), _), tys)) =
-        if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
-      | to_ho _ = raise Fail "unexpected type"
-  in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
+  in
+    if is_type_enc_full_higher_order type_enc then to_ho
+    else if is_type_enc_higher_order type_enc then to_lfho
+    else to_fo ary
+  end
 
 fun native_atp_type_of_typ type_enc pred_sym ary =
   native_atp_type_of_raw_atp_type type_enc pred_sym ary o raw_atp_type_of_typ type_enc
@@ -1082,7 +1100,7 @@
       | intro top_level args (IConst (name as (s, _), T, T_args)) =
         (case proxify_const s of
           SOME proxy_base =>
-          if top_level orelse is_type_enc_higher_order type_enc then
+          if top_level orelse is_type_enc_full_higher_order type_enc then
             (case (top_level, s) of
               (_, "c_False") => IConst (`I tptp_false, T, [])
             | (_, "c_True") => IConst (`I tptp_true, T, [])
@@ -1238,7 +1256,7 @@
               |> transform_elim_prop
               |> Object_Logic.atomize_term ctxt
     val need_trueprop = (fastype_of t = @{typ bool})
-    val is_ho = is_type_enc_higher_order type_enc
+    val is_ho = is_type_enc_full_higher_order type_enc
   in
     t |> need_trueprop ? HOLogic.mk_Trueprop
       |> (if is_ho then unextensionalize_def
@@ -1251,7 +1269,7 @@
 (* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "=" for technical
    reasons. *)
 fun should_use_iff_for_eq CNF _ = false
-  | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
+  | should_use_iff_for_eq (THF _) format = not (is_type_enc_full_higher_order format)
   | should_use_iff_for_eq _ _ = true
 
 fun make_formula ctxt format type_enc iff_for_eq name stature role t =
@@ -1393,7 +1411,7 @@
    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [], in_conj = false})) @
   ([tptp_equal, tptp_old_equal]
    |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [], in_conj = false}))
-  |> not (is_type_enc_higher_order type_enc)
+  |> not (is_type_enc_full_higher_order type_enc)
     ? cons (prefixed_predicator_name,
       {pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false})
 
@@ -1592,7 +1610,8 @@
         if is_pred_sym sym_tab s then tm else predicatify completish tm
       | _ => predicatify completish tm)
     val do_iterm =
-      not (is_type_enc_higher_order type_enc) ? (introduce_app_ops #> introduce_predicators)
+      (not (is_type_enc_higher_order type_enc) ? introduce_app_ops)
+      #> (not (is_type_enc_full_higher_order type_enc) ? introduce_predicators)
       #> filter_type_args_in_iterm thy ctrss type_enc
   in update_iformula (formula_map do_iterm) end
 
@@ -2595,7 +2614,7 @@
       else
         Sufficient_App_Op_And_Predicator
     val lam_trans =
-      if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN
+      if lam_trans = keep_lamsN andalso not (is_type_enc_full_higher_order type_enc) then liftingN
       else lam_trans
     val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
       translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue May 22 11:08:37 2018 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue May 22 17:15:02 2018 +0200
@@ -54,6 +54,7 @@
   val e_parN : string
   val e_sineN : string
   val e_tofofN : string
+  val ehohN : string
   val iproverN : string
   val iprover_eqN : string
   val leo2N : string
@@ -124,6 +125,7 @@
 val e_parN = "e_par"
 val e_sineN = "e_sine"
 val e_tofofN = "e_tofof"
+val ehohN = "ehoh"
 val iproverN = "iprover"
 val iprover_eqN = "iprover_eq"
 val leo2N = "leo2"
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue May 22 11:08:37 2018 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue May 22 17:15:02 2018 +0200
@@ -353,6 +353,32 @@
 val e_par = (e_parN, fn () => e_par_config)
 
 
+(* Ehoh *)
+
+val ehoh_thf0 = THF (Monomorphic, THF_Lambda_Free)
+
+val ehoh_config : atp_config =
+  {exec = fn _ => (["E_HOME"], ["eprover"]),
+   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+       "--auto-schedule --tstp-in --tstp-out --silent --cpu-limit=" ^
+       string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ file_name,
+   proof_delims =
+     [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
+     tstp_proof_delims,
+   known_failures =
+     [(TimedOut, "Failure: Resource limit exceeded (time)"),
+      (TimedOut, "time limit exceeded")] @
+     known_szs_status_failures,
+   prem_role = Conjecture,
+   best_slices =
+     (* FUDGE *)
+     K [(1.0, (((500, ""), ehoh_thf0, "mono_native_higher", liftingN, false), ""))],
+   best_max_mono_iters = default_max_mono_iters,
+   best_max_new_mono_instances = default_max_new_mono_instances}
+
+val ehoh = (ehohN, fn () => ehoh_config)
+
+
 (* iProver *)
 
 val iprover_config : atp_config =
@@ -792,10 +818,11 @@
   end
 
 val atps =
-  [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, leo3, 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_leo3, remote_satallax,
-   remote_vampire, remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new]
+  [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, iprover_eq, leo2, leo3, 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_leo3,
+   remote_satallax, remote_vampire, remote_snark, remote_pirate, remote_waldmeister,
+   remote_waldmeister_new]
 
 val _ = Theory.setup (fold add_atp atps)