1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Sep 06 18:07:44 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Sep 06 18:13:36 2011 +0200
1.3 @@ -22,15 +22,15 @@
1.4 AFun of 'a ho_type * 'a ho_type |
1.5 ATyAbs of 'a list * 'a ho_type
1.6
1.7 - datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
1.8 - datatype tff_explicitness = TFF_Implicit | TFF_Explicit
1.9 + datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
1.10 + datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
1.11 datatype thf_flavor = THF_Without_Choice | THF_With_Choice
1.12 - datatype format =
1.13 + datatype tptp_format =
1.14 CNF |
1.15 CNF_UEQ |
1.16 FOF |
1.17 - TFF of tff_polymorphism * tff_explicitness |
1.18 - THF0 of thf_flavor
1.19 + TFF of tptp_polymorphism * tptp_explicitness |
1.20 + THF of tptp_polymorphism * tptp_explicitness * thf_flavor
1.21
1.22 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
1.23 datatype 'a problem_line =
1.24 @@ -92,9 +92,9 @@
1.25 bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
1.26 -> 'd -> 'd
1.27 val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
1.28 - val is_format_thf : format -> bool
1.29 - val is_format_typed : format -> bool
1.30 - val tptp_lines_for_atp_problem : format -> string problem -> string list
1.31 + val is_format_thf : tptp_format -> bool
1.32 + val is_format_typed : tptp_format -> bool
1.33 + val tptp_lines_for_atp_problem : tptp_format -> string problem -> string list
1.34 val ensure_cnf_problem :
1.35 (string * string) problem -> (string * string) problem
1.36 val filter_cnf_ueq_problem :
1.37 @@ -130,16 +130,16 @@
1.38 AFun of 'a ho_type * 'a ho_type |
1.39 ATyAbs of 'a list * 'a ho_type
1.40
1.41 -datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
1.42 -datatype tff_explicitness = TFF_Implicit | TFF_Explicit
1.43 +datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
1.44 +datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
1.45 datatype thf_flavor = THF_Without_Choice | THF_With_Choice
1.46
1.47 -datatype format =
1.48 +datatype tptp_format =
1.49 CNF |
1.50 CNF_UEQ |
1.51 FOF |
1.52 - TFF of tff_polymorphism * tff_explicitness |
1.53 - THF0 of thf_flavor
1.54 + TFF of tptp_polymorphism * tptp_explicitness |
1.55 + THF of tptp_polymorphism * tptp_explicitness * thf_flavor
1.56
1.57 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
1.58 datatype 'a problem_line =
1.59 @@ -224,10 +224,10 @@
1.60 | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
1.61 | formula_map f (AAtom tm) = AAtom (f tm)
1.62
1.63 -fun is_format_thf (THF0 _) = true
1.64 +fun is_format_thf (THF _) = true
1.65 | is_format_thf _ = false
1.66 fun is_format_typed (TFF _) = true
1.67 - | is_format_typed (THF0 _) = true
1.68 + | is_format_typed (THF _) = true
1.69 | is_format_typed _ = false
1.70
1.71 fun string_for_kind Axiom = "axiom"
1.72 @@ -266,7 +266,7 @@
1.73 ss) ^ "]: " ^ str false ty
1.74 in str true ty end
1.75
1.76 -fun string_for_type (THF0 _) ty = str_for_type ty
1.77 +fun string_for_type (THF _) ty = str_for_type ty
1.78 | string_for_type (TFF _) ty = str_for_type (flatten_type ty)
1.79 | string_for_type _ _ = raise Fail "unexpected type in untyped format"
1.80
1.81 @@ -288,6 +288,9 @@
1.82 else
1.83 "")
1.84
1.85 +fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true
1.86 + | is_format_with_choice _ = false
1.87 +
1.88 fun string_for_term _ (ATerm (s, [])) = s
1.89 | string_for_term format (ATerm (s, ts)) =
1.90 if s = tptp_empty_list then
1.91 @@ -298,7 +301,7 @@
1.92 |> is_format_thf format ? enclose "(" ")"
1.93 else
1.94 (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
1.95 - s = tptp_choice andalso format = THF0 THF_With_Choice, ts) of
1.96 + s = tptp_choice andalso is_format_with_choice format, ts) of
1.97 (true, _, [AAbs ((s', ty), tm)]) =>
1.98 (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
1.99 possible, to work around LEO-II 1.2.8 parser limitation. *)
1.100 @@ -306,8 +309,8 @@
1.101 (AQuant (if s = tptp_ho_forall then AForall else AExists,
1.102 [(s', SOME ty)], AAtom tm))
1.103 | (_, true, [AAbs ((s', ty), tm)]) =>
1.104 - (*There is code in ATP_Translate to ensure that Eps is always applied
1.105 - to an abstraction*)
1.106 + (* There is code in "ATP_Translate" to ensure that "Eps" is always
1.107 + applied to an abstraction. *)
1.108 tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
1.109 string_for_term format tm ^ ""
1.110 |> enclose "(" ")"
1.111 @@ -319,7 +322,7 @@
1.112 else
1.113 s ^ "(" ^ commas ss ^ ")"
1.114 end)
1.115 - | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
1.116 + | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
1.117 "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
1.118 string_for_term format tm ^ ")"
1.119 | string_for_term _ _ = raise Fail "unexpected term in first-order format"
1.120 @@ -352,7 +355,7 @@
1.121 | string_for_format CNF_UEQ = tptp_cnf
1.122 | string_for_format FOF = tptp_fof
1.123 | string_for_format (TFF _) = tptp_tff
1.124 - | string_for_format (THF0 _) = tptp_thf
1.125 + | string_for_format (THF _) = tptp_thf
1.126
1.127 fun string_for_problem_line format (Decl (ident, sym, ty)) =
1.128 string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^
2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Sep 06 18:07:44 2011 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Sep 06 18:13:36 2011 +0200
2.3 @@ -7,7 +7,7 @@
2.4
2.5 signature ATP_SYSTEMS =
2.6 sig
2.7 - type format = ATP_Problem.format
2.8 + type tptp_format = ATP_Problem.tptp_format
2.9 type formula_kind = ATP_Problem.formula_kind
2.10 type failure = ATP_Proof.failure
2.11
2.12 @@ -22,7 +22,8 @@
2.13 conj_sym_kind : formula_kind,
2.14 prem_kind : formula_kind,
2.15 best_slices :
2.16 - Proof.context -> (real * (bool * (int * format * string * string))) list}
2.17 + Proof.context
2.18 + -> (real * (bool * (int * tptp_format * string * string))) list}
2.19
2.20 val force_sos : bool Config.T
2.21 val e_smartN : string
2.22 @@ -41,6 +42,7 @@
2.23 val e_tofofN : string
2.24 val leo2N : string
2.25 val pffN : string
2.26 + val phfN : string
2.27 val satallaxN : string
2.28 val snarkN : string
2.29 val spassN : string
2.30 @@ -51,7 +53,7 @@
2.31 val remote_atp :
2.32 string -> string -> string list -> (string * string) list
2.33 -> (failure * string) list -> formula_kind -> formula_kind
2.34 - -> (Proof.context -> int * format * string) -> string * atp_config
2.35 + -> (Proof.context -> int * tptp_format * string) -> string * atp_config
2.36 val add_atp : string * atp_config -> theory -> theory
2.37 val get_atp : theory -> string -> atp_config
2.38 val supported_atps : theory -> string list
2.39 @@ -79,7 +81,8 @@
2.40 conj_sym_kind : formula_kind,
2.41 prem_kind : formula_kind,
2.42 best_slices :
2.43 - Proof.context -> (real * (bool * (int * format * string * string))) list}
2.44 + Proof.context
2.45 + -> (real * (bool * (int * tptp_format * string * string))) list}
2.46
2.47 (* "best_slices" must be found empirically, taking a wholistic approach since
2.48 the ATPs are run in parallel. The "real" components give the faction of the
2.49 @@ -105,6 +108,7 @@
2.50 val e_tofofN = "e_tofof"
2.51 val leo2N = "leo2"
2.52 val pffN = "pff"
2.53 +val phfN = "phf"
2.54 val satallaxN = "satallax"
2.55 val snarkN = "snark"
2.56 val spassN = "spass"
2.57 @@ -230,6 +234,8 @@
2.58
2.59 (* LEO-II *)
2.60
2.61 +val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
2.62 +
2.63 val leo2_config : atp_config =
2.64 {exec = ("LEO2_HOME", "leo"),
2.65 required_execs = [],
2.66 @@ -243,10 +249,8 @@
2.67 prem_kind = Hypothesis,
2.68 best_slices = fn ctxt =>
2.69 (* FUDGE *)
2.70 - [(0.667, (false, (150, THF0 THF_Without_Choice,
2.71 - "mono_simple_higher", sosN))),
2.72 - (0.333, (true, (50, THF0 THF_Without_Choice,
2.73 - "mono_simple_higher", no_sosN)))]
2.74 + [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", sosN))),
2.75 + (0.333, (true, (50, leo2_thf0, "mono_simple_higher", no_sosN)))]
2.76 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
2.77 else I)}
2.78
2.79 @@ -255,6 +259,8 @@
2.80
2.81 (* Satallax *)
2.82
2.83 +val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
2.84 +
2.85 val satallax_config : atp_config =
2.86 {exec = ("SATALLAX_HOME", "satallax"),
2.87 required_execs = [],
2.88 @@ -266,8 +272,8 @@
2.89 conj_sym_kind = Axiom,
2.90 prem_kind = Hypothesis,
2.91 best_slices =
2.92 - K [(1.0, (true, (100, THF0 THF_With_Choice, "mono_simple_higher", "")))]
2.93 - (* FUDGE *)}
2.94 + (* FUDGE *)
2.95 + K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", "")))]}
2.96
2.97 val satallax = (satallaxN, satallax_config)
2.98
2.99 @@ -314,7 +320,7 @@
2.100 fun is_old_vampire_version () =
2.101 string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
2.102
2.103 -val vampire_tff = TFF (TFF_Monomorphic, TFF_Implicit)
2.104 +val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
2.105
2.106 val vampire_config : atp_config =
2.107 {exec = ("VAMPIRE_HOME", "vampire"),
2.108 @@ -347,9 +353,9 @@
2.109 (0.333, (false, (500, FOF, "mono_tags?", sosN))),
2.110 (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
2.111 else
2.112 - [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))),
2.113 - (0.333, (false, (500, vampire_tff, "mono_simple", sosN))),
2.114 - (0.334, (true, (50, vampire_tff, "mono_simple", no_sosN)))])
2.115 + [(0.333, (false, (150, vampire_tff0, "poly_guards", sosN))),
2.116 + (0.333, (false, (500, vampire_tff0, "mono_simple", sosN))),
2.117 + (0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))])
2.118 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
2.119 else I)}
2.120
2.121 @@ -358,7 +364,7 @@
2.122
2.123 (* Z3 with TPTP syntax *)
2.124
2.125 -val z3_tff = TFF (TFF_Monomorphic, TFF_Implicit)
2.126 +val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
2.127
2.128 val z3_tptp_config : atp_config =
2.129 {exec = ("Z3_HOME", "z3"),
2.130 @@ -377,18 +383,17 @@
2.131 prem_kind = Hypothesis,
2.132 best_slices =
2.133 (* FUDGE *)
2.134 - K [(0.5, (false, (250, z3_tff, "mono_simple", ""))),
2.135 - (0.25, (false, (125, z3_tff, "mono_simple", ""))),
2.136 - (0.125, (false, (62, z3_tff, "mono_simple", ""))),
2.137 - (0.125, (false, (31, z3_tff, "mono_simple", "")))]}
2.138 + K [(0.5, (false, (250, z3_tff0, "mono_simple", ""))),
2.139 + (0.25, (false, (125, z3_tff0, "mono_simple", ""))),
2.140 + (0.125, (false, (62, z3_tff0, "mono_simple", ""))),
2.141 + (0.125, (false, (31, z3_tff0, "mono_simple", "")))]}
2.142
2.143 val z3_tptp = (z3_tptpN, z3_tptp_config)
2.144
2.145 -(* Not really a prover: Experimental PFF (Polymorphic TFF) output *)
2.146
2.147 -val poly_tff = TFF (TFF_Polymorphic, TFF_Implicit)
2.148 +(* Not really a prover: Experimental Polymorphic TFF and THF output *)
2.149
2.150 -val pff_config : atp_config =
2.151 +fun dummy_config format type_enc : atp_config =
2.152 {exec = ("ISABELLE_ATP", "scripts/dummy_atp"),
2.153 required_execs = [],
2.154 arguments = K (K (K (K (K "")))),
2.155 @@ -396,10 +401,16 @@
2.156 known_failures = [(GaveUp, "SZS status Unknown")],
2.157 conj_sym_kind = Hypothesis,
2.158 prem_kind = Hypothesis,
2.159 - best_slices = K [(1.0, (false, (200, poly_tff, "poly_simple", "")))]}
2.160 + best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
2.161
2.162 +val pff_format = TFF (TPTP_Polymorphic, TPTP_Implicit)
2.163 +val pff_config = dummy_config pff_format "poly_simple"
2.164 val pff = (pffN, pff_config)
2.165
2.166 +val phf_format = THF (TPTP_Polymorphic, TPTP_Implicit, THF_With_Choice)
2.167 +val phf_config = dummy_config phf_format "poly_simple_higher"
2.168 +val phf = (phfN, phf_config)
2.169 +
2.170
2.171 (* Remote ATP invocation via SystemOnTPTP *)
2.172
2.173 @@ -475,34 +486,33 @@
2.174 (remote_prefix ^ name,
2.175 remotify_config system_name system_versions best_slice config)
2.176
2.177 -val dumb_tff = TFF (TFF_Monomorphic, TFF_Explicit)
2.178 +val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
2.179
2.180 val remote_e =
2.181 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
2.182 (K (750, FOF, "mono_tags?") (* FUDGE *))
2.183 val remote_leo2 =
2.184 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
2.185 - (K (100, THF0 THF_Without_Choice,
2.186 - "mono_simple_higher") (* FUDGE *))
2.187 + (K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *))
2.188 val remote_satallax =
2.189 remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
2.190 - (K (100, THF0 THF_With_Choice,
2.191 - "mono_simple_higher") (* FUDGE *))
2.192 + (K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *))
2.193 val remote_vampire =
2.194 remotify_atp vampire "Vampire" ["1.8"]
2.195 (K (250, FOF, "mono_guards?") (* FUDGE *))
2.196 val remote_z3_tptp =
2.197 - remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "mono_simple") (* FUDGE *))
2.198 + remotify_atp z3_tptp "Z3" ["3.0"]
2.199 + (K (250, z3_tff0, "mono_simple") (* FUDGE *))
2.200 val remote_e_sine =
2.201 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
2.202 Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
2.203 val remote_snark =
2.204 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
2.205 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
2.206 - (K (100, dumb_tff, "mono_simple") (* FUDGE *))
2.207 + (K (100, explicit_tff0, "mono_simple") (* FUDGE *))
2.208 val remote_e_tofof =
2.209 remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
2.210 - Hypothesis (K (150, dumb_tff, "mono_simple") (* FUDGE *))
2.211 + Hypothesis (K (150, explicit_tff0, "mono_simple") (* FUDGE *))
2.212 val remote_waldmeister =
2.213 remote_atp waldmeisterN "Waldmeister" ["710"]
2.214 [("#START OF PROOF", "Proved Goals:")]
2.215 @@ -532,7 +542,7 @@
2.216 Synchronized.change systems (fn _ => get_systems ())
2.217
2.218 val atps =
2.219 - [e, leo2, pff, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
2.220 + [e, leo2, pff, phf, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
2.221 remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
2.222 remote_e_tofof, remote_waldmeister]
2.223 val setup = fold add_atp atps
3.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Sep 06 18:07:44 2011 +0200
3.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Sep 06 18:13:36 2011 +0200
3.3 @@ -11,7 +11,7 @@
3.4 type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
3.5 type connective = ATP_Problem.connective
3.6 type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
3.7 - type format = ATP_Problem.format
3.8 + type tptp_format = ATP_Problem.tptp_format
3.9 type formula_kind = ATP_Problem.formula_kind
3.10 type 'a problem = 'a ATP_Problem.problem
3.11
3.12 @@ -92,7 +92,7 @@
3.13 val level_of_type_enc : type_enc -> type_level
3.14 val is_type_enc_quasi_sound : type_enc -> bool
3.15 val is_type_enc_fairly_sound : type_enc -> bool
3.16 - val adjust_type_enc : format -> type_enc -> type_enc
3.17 + val adjust_type_enc : tptp_format -> type_enc -> type_enc
3.18 val mk_aconns :
3.19 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
3.20 val unmangled_const : string -> string * (string, 'b) ho_term list
3.21 @@ -100,7 +100,7 @@
3.22 val helper_table : ((string * bool) * thm list) list
3.23 val factsN : string
3.24 val prepare_atp_problem :
3.25 - Proof.context -> format -> formula_kind -> formula_kind -> type_enc
3.26 + Proof.context -> tptp_format -> formula_kind -> formula_kind -> type_enc
3.27 -> bool -> string -> bool -> bool -> term list -> term
3.28 -> ((string * locality) * term) list
3.29 -> string problem * string Symtab.table * int * int
3.30 @@ -142,7 +142,7 @@
3.31 (* TFF1 is still in development, and it is still unclear whether symbols will be
3.32 allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
3.33 "dummy" type variables. *)
3.34 -val exploit_tff1_dummy_type_vars = false
3.35 +val avoid_first_order_dummy_type_vars = true
3.36
3.37 val bound_var_prefix = "B_"
3.38 val all_bound_var_prefix = "BA_"
3.39 @@ -325,8 +325,8 @@
3.40 fun default c = const_prefix ^ lookup_const c
3.41 in
3.42 fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
3.43 - | make_fixed_const (SOME (THF0 THF_With_Choice)) c =
3.44 - if c = choice_const then tptp_choice else default c
3.45 + | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c =
3.46 + if c = choice_const then tptp_choice else default c
3.47 | make_fixed_const _ c = default c
3.48 end
3.49
3.50 @@ -587,7 +587,9 @@
3.51 | _ => raise Same.SAME)
3.52 | ("simple_higher", (SOME poly, _, Nonuniform)) =>
3.53 (case (poly, level) of
3.54 - (_, Noninf_Nonmono_Types _) => raise Same.SAME
3.55 + (Polymorphic, All_Types) =>
3.56 + Simple_Types (Higher_Order, Polymorphic, All_Types)
3.57 + | (_, Noninf_Nonmono_Types _) => raise Same.SAME
3.58 | (Mangled_Monomorphic, _) =>
3.59 Simple_Types (Higher_Order, Mangled_Monomorphic, level)
3.60 | _ => raise Same.SAME)
3.61 @@ -631,12 +633,13 @@
3.62 | is_type_level_monotonicity_based Fin_Nonmono_Types = true
3.63 | is_type_level_monotonicity_based _ = false
3.64
3.65 -fun adjust_type_enc (THF0 _) (Simple_Types (order, Polymorphic, level)) =
3.66 +fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
3.67 + (Simple_Types (order, _, level)) =
3.68 Simple_Types (order, Mangled_Monomorphic, level)
3.69 - | adjust_type_enc (THF0 _) type_enc = type_enc
3.70 - | adjust_type_enc (TFF (TFF_Monomorphic, _)) (Simple_Types (_, _, level)) =
3.71 + | adjust_type_enc (THF _) type_enc = type_enc
3.72 + | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
3.73 Simple_Types (First_Order, Mangled_Monomorphic, level)
3.74 - | adjust_type_enc (TFF (_, _)) (Simple_Types (_, poly, level)) =
3.75 + | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
3.76 Simple_Types (First_Order, poly, level)
3.77 | adjust_type_enc format (Simple_Types (_, poly, level)) =
3.78 adjust_type_enc format (Guards (poly, level, Uniform))
3.79 @@ -746,8 +749,9 @@
3.80 fun type_class_formula type_enc class arg =
3.81 AAtom (ATerm (class, arg ::
3.82 (case type_enc of
3.83 - Simple_Types (_, Polymorphic, _) =>
3.84 - if exploit_tff1_dummy_type_vars then [] else [ATerm (TYPE_name, [arg])]
3.85 + Simple_Types (First_Order, Polymorphic, _) =>
3.86 + if avoid_first_order_dummy_type_vars then [ATerm (TYPE_name, [arg])]
3.87 + else []
3.88 | _ => [])))
3.89 fun formulas_for_types type_enc add_sorts_on_typ Ts =
3.90 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
3.91 @@ -1779,18 +1783,19 @@
3.92
3.93 (** Symbol declarations **)
3.94
3.95 -fun decl_line_for_class s =
3.96 +fun decl_line_for_class order s =
3.97 let val name as (s, _) = `make_type_class s in
3.98 Decl (sym_decl_prefix ^ s, name,
3.99 - if exploit_tff1_dummy_type_vars then
3.100 - AFun (atype_of_types, bool_atype)
3.101 + if order = First_Order andalso avoid_first_order_dummy_type_vars then
3.102 + ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype))
3.103 else
3.104 - ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype)))
3.105 + AFun (atype_of_types, bool_atype))
3.106 end
3.107
3.108 fun decl_lines_for_classes type_enc classes =
3.109 case type_enc of
3.110 - Simple_Types (_, Polymorphic, _) => map decl_line_for_class classes
3.111 + Simple_Types (order, Polymorphic, _) =>
3.112 + map (decl_line_for_class order) classes
3.113 | _ => []
3.114
3.115 fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
3.116 @@ -2232,7 +2237,8 @@
3.117 CNF => ensure_cnf_problem
3.118 | CNF_UEQ => filter_cnf_ueq_problem
3.119 | FOF => I
3.120 - | TFF (_, TFF_Implicit) => I
3.121 + | TFF (_, TPTP_Implicit) => I
3.122 + | THF (_, TPTP_Implicit, _) => I
3.123 | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
3.124 implicit_declsN)
3.125 val (problem, pool) = problem |> nice_atp_problem readable_names