added dummy polymorphic THF system
authorblanchet
Tue Sep 06 18:13:36 2011 +0200 (2011-09-06)
changeset 44754265174356212
parent 44753 3c73f4068978
child 44757 8aae88168599
added dummy polymorphic THF system
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/ATP/atp_translate.ML
     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