--- a/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200
@@ -447,21 +447,22 @@
fun make_class_rel_clauses thy subs supers =
map make_class_rel_clause (class_pairs thy subs supers)
-datatype combterm =
- CombConst of name * typ * typ list |
- CombVar of name * typ |
- CombApp of combterm * combterm |
- CombAbs of (name * typ) * combterm
+(* intermediate terms *)
+datatype iterm =
+ IConst of name * typ * typ list |
+ IVar of name * typ |
+ IApp of iterm * iterm |
+ IAbs of (name * typ) * iterm
-fun combtyp_of (CombConst (_, T, _)) = T
- | combtyp_of (CombVar (_, T)) = T
- | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
- | combtyp_of (CombAbs ((_, T), tm)) = T --> combtyp_of tm
+fun ityp_of (IConst (_, T, _)) = T
+ | ityp_of (IVar (_, T)) = T
+ | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
+ | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
(*gets the head of a combinator application, along with the list of arguments*)
-fun strip_combterm_comb u =
+fun strip_iterm_comb u =
let
- fun stripc (CombApp (t, u), ts) = stripc (t, u :: ts)
+ fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
| stripc x = x
in stripc (u, []) end
@@ -471,42 +472,41 @@
[new_skolem_const_prefix, s, string_of_int num_T_args]
|> space_implode Long_Name.separator
-(* Converts a term (with combinators) into a combterm. Also accumulates sort
- infomation. *)
-fun combterm_from_term thy bs (P $ Q) =
+(* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
+ Also accumulates sort infomation. *)
+fun iterm_from_term thy bs (P $ Q) =
let
- val (P', P_atomics_Ts) = combterm_from_term thy bs P
- val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
- in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
- | combterm_from_term thy _ (Const (c, T)) =
+ val (P', P_atomics_Ts) = iterm_from_term thy bs P
+ val (Q', Q_atomics_Ts) = iterm_from_term thy bs Q
+ in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
+ | iterm_from_term thy _ (Const (c, T)) =
let
val tvar_list =
(if String.isPrefix old_skolem_const_prefix c then
[] |> Term.add_tvarsT T |> map TVar
else
(c, T) |> Sign.const_typargs thy)
- val c' = CombConst (`make_fixed_const c, T, tvar_list)
+ val c' = IConst (`make_fixed_const c, T, tvar_list)
in (c', atyps_of T) end
- | combterm_from_term _ _ (Free (v, T)) =
- (CombConst (`make_fixed_var v, T, []), atyps_of T)
- | combterm_from_term _ _ (Var (v as (s, _), T)) =
+ | iterm_from_term _ _ (Free (v, T)) =
+ (IConst (`make_fixed_var v, T, []), atyps_of T)
+ | iterm_from_term _ _ (Var (v as (s, _), T)) =
(if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
let
val Ts = T |> strip_type |> swap |> op ::
val s' = new_skolem_const_name s (length Ts)
- in CombConst (`make_fixed_const s', T, Ts) end
+ in IConst (`make_fixed_const s', T, Ts) end
else
- CombVar ((make_schematic_var v, s), T), atyps_of T)
- | combterm_from_term _ bs (Bound j) =
- nth bs j
- |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
- | combterm_from_term thy bs (Abs (s, T, t)) =
+ IVar ((make_schematic_var v, s), T), atyps_of T)
+ | iterm_from_term _ bs (Bound j) =
+ nth bs j |> (fn (s, T) => (IConst (`make_bound_var s, T, []), atyps_of T))
+ | iterm_from_term thy bs (Abs (s, T, t)) =
let
fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
val s = vary s
- val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t
+ val (tm, atomic_Ts) = iterm_from_term thy ((s, T) :: bs) t
in
- (CombAbs ((`make_bound_var s, T), tm),
+ (IAbs ((`make_bound_var s, T), tm),
union (op =) atomic_Ts (atyps_of T))
end
@@ -621,15 +621,15 @@
{name : string,
locality : locality,
kind : formula_kind,
- combformula : (name, typ, combterm) formula,
+ iformula : (name, typ, iterm) formula,
atomic_types : typ list}
-fun update_combformula f ({name, locality, kind, combformula, atomic_types}
- : translated_formula) =
- {name = name, locality = locality, kind = kind, combformula = f combformula,
+fun update_iformula f ({name, locality, kind, iformula, atomic_types}
+ : translated_formula) =
+ {name = name, locality = locality, kind = kind, iformula = f iformula,
atomic_types = atomic_types} : translated_formula
-fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
+fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
val type_instance = Sign.typ_instance o Proof_Context.theory_of
@@ -712,11 +712,11 @@
|> filter_out (member (op =) bounds o fst))
in mk_aquant AForall (formula_vars [] phi []) phi end
-fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
- | combterm_vars (CombConst _) = I
- | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
- | combterm_vars (CombAbs (_, tm)) = combterm_vars tm
-fun close_combformula_universally phi = close_universally combterm_vars phi
+fun iterm_vars (IApp (tm1, tm2)) = fold iterm_vars [tm1, tm2]
+ | iterm_vars (IConst _) = I
+ | iterm_vars (IVar (name, T)) = insert (op =) (name, SOME T)
+ | iterm_vars (IAbs (_, tm)) = iterm_vars tm
+fun close_iformula_universally phi = close_universally iterm_vars phi
fun term_vars bounds (ATerm (name as (s, _), tms)) =
(is_tptp_variable s andalso not (member (op =) bounds name))
@@ -816,9 +816,9 @@
fun introduce_proxies type_enc =
let
- fun intro top_level (CombApp (tm1, tm2)) =
- CombApp (intro top_level tm1, intro false tm2)
- | intro top_level (CombConst (name as (s, _), T, T_args)) =
+ fun intro top_level (IApp (tm1, tm2)) =
+ IApp (intro top_level tm1, intro false tm2)
+ | intro top_level (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
@@ -838,15 +838,15 @@
else
(proxy_base |>> prefix const_prefix, T_args)
| NONE => (name, T_args))
- |> (fn (name, T_args) => CombConst (name, T, T_args))
- | intro _ (CombAbs (bound, tm)) = CombAbs (bound, intro false tm)
+ |> (fn (name, T_args) => IConst (name, T, T_args))
+ | intro _ (IAbs (bound, tm)) = IAbs (bound, intro false tm)
| intro _ tm = tm
in intro true end
-fun combformula_from_prop thy type_enc eq_as_iff =
+fun iformula_from_prop thy type_enc eq_as_iff =
let
fun do_term bs t atomic_types =
- combterm_from_term thy bs (Envir.eta_contract t)
+ iterm_from_term thy bs (Envir.eta_contract t)
|>> (introduce_proxies type_enc #> AAtom)
||> union (op =) atomic_types
fun do_quant bs q s T t' =
@@ -986,10 +986,10 @@
(* making fact and conjecture formulas *)
fun make_formula thy type_enc eq_as_iff name loc kind t =
let
- val (combformula, atomic_types) =
- combformula_from_prop thy type_enc eq_as_iff t []
+ val (iformula, atomic_types) =
+ iformula_from_prop thy type_enc eq_as_iff t []
in
- {name = name, locality = loc, kind = kind, combformula = combformula,
+ {name = name, locality = loc, kind = kind, iformula = iformula,
atomic_types = atomic_types}
end
@@ -999,7 +999,7 @@
case t |> preproc ? preprocess_prop ctxt trans_lambdas presimp_consts Axiom
|> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
loc Axiom of
- formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
+ formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
if s = tptp_true then NONE else SOME formula
| formula => SOME formula
end
@@ -1017,7 +1017,7 @@
(Conjecture, I)
else
(prem_kind,
- if prem_kind = Conjecture then update_combformula mk_anot
+ if prem_kind = Conjecture then update_iformula mk_anot
else I)
in
t |> preproc ?
@@ -1054,9 +1054,9 @@
should_encode_type ctxt nonmono_Ts level T
| should_predicate_on_type _ _ _ _ _ = false
-fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
+fun is_var_or_bound_var (IConst ((s, _), _, _)) =
String.isPrefix bound_var_prefix s
- | is_var_or_bound_var (CombVar _) = true
+ | is_var_or_bound_var (IVar _) = true
| is_var_or_bound_var _ = false
datatype tag_site =
@@ -1096,7 +1096,7 @@
type sym_info =
{pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
-fun add_combterm_syms_to_table ctxt explicit_apply =
+fun add_iterm_syms_to_table ctxt explicit_apply =
let
fun consider_var_arity const_T var_T max_ary =
let
@@ -1128,9 +1128,9 @@
else
accum
fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
- let val (head, args) = strip_combterm_comb tm in
+ let val (head, args) = strip_iterm_comb tm in
(case head of
- CombConst ((s, _), T, _) =>
+ IConst ((s, _), T, _) =>
if String.isPrefix bound_var_prefix s then
add_var_or_bound_var T accum
else
@@ -1170,16 +1170,15 @@
sym_tab
end)
end
- | CombVar (_, T) => add_var_or_bound_var T accum
- | CombAbs ((_, T), tm) =>
- accum |> add_var_or_bound_var T |> add false tm
+ | IVar (_, T) => add_var_or_bound_var T accum
+ | IAbs ((_, T), tm) => accum |> add_var_or_bound_var T |> add false tm
| _ => accum)
|> fold (add false) args
end
in add true end
fun add_fact_syms_to_table ctxt explicit_apply =
fact_lift (formula_fold NONE
- (K (add_combterm_syms_to_table ctxt explicit_apply)))
+ (K (add_iterm_syms_to_table ctxt explicit_apply)))
val default_sym_tab_entries : (string * sym_info) list =
(prefixed_predicator_name,
@@ -1219,33 +1218,32 @@
| NONE => false
val predicator_combconst =
- CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
-fun predicator tm = CombApp (predicator_combconst, tm)
+ IConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
+fun predicator tm = IApp (predicator_combconst, tm)
-fun introduce_predicators_in_combterm sym_tab tm =
- case strip_combterm_comb tm of
- (CombConst ((s, _), _, _), _) =>
+fun introduce_predicators_in_iterm sym_tab tm =
+ case strip_iterm_comb tm of
+ (IConst ((s, _), _, _), _) =>
if is_pred_sym sym_tab s then tm else predicator tm
| _ => predicator tm
-fun list_app head args = fold (curry (CombApp o swap)) args head
+fun list_app head args = fold (curry (IApp o swap)) args head
val app_op = `make_fixed_const app_op_name
fun explicit_app arg head =
let
- val head_T = combtyp_of head
+ val head_T = ityp_of head
val (arg_T, res_T) = dest_funT head_T
- val explicit_app =
- CombConst (app_op, head_T --> head_T, [arg_T, res_T])
+ val explicit_app = IConst (app_op, head_T --> head_T, [arg_T, res_T])
in list_app explicit_app [head, arg] end
fun list_explicit_app head args = fold explicit_app args head
-fun introduce_explicit_apps_in_combterm sym_tab =
+fun introduce_explicit_apps_in_iterm sym_tab =
let
fun aux tm =
- case strip_combterm_comb tm of
- (head as CombConst ((s, _), _, _), args) =>
+ case strip_iterm_comb tm of
+ (head as IConst ((s, _), _, _), args) =>
args |> map aux
|> chop (min_arity_of sym_tab s)
|>> list_app head
@@ -1279,12 +1277,11 @@
end
handle TYPE _ => T_args
-fun enforce_type_arg_policy_in_combterm ctxt format type_enc =
+fun enforce_type_arg_policy_in_iterm ctxt format type_enc =
let
val thy = Proof_Context.theory_of ctxt
- fun aux arity (CombApp (tm1, tm2)) =
- CombApp (aux (arity + 1) tm1, aux 0 tm2)
- | aux arity (CombConst (name as (s, _), T, T_args)) =
+ fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2)
+ | aux arity (IConst (name as (s, _), T, T_args)) =
(case strip_prefix_and_unascii const_prefix s of
NONE => (name, T_args)
| SOME s'' =>
@@ -1301,19 +1298,18 @@
name, [])
| No_Type_Args => (name, [])
end)
- |> (fn (name, T_args) => CombConst (name, T, T_args))
- | aux _ (CombAbs (bound, tm)) = CombAbs (bound, aux 0 tm)
+ |> (fn (name, T_args) => IConst (name, T, T_args))
+ | aux _ (IAbs (bound, tm)) = IAbs (bound, aux 0 tm)
| aux _ tm = tm
in aux 0 end
-fun repair_combterm ctxt format type_enc sym_tab =
+fun repair_iterm ctxt format type_enc sym_tab =
not (is_type_enc_higher_order type_enc)
- ? (introduce_explicit_apps_in_combterm sym_tab
- #> introduce_predicators_in_combterm sym_tab)
- #> enforce_type_arg_policy_in_combterm ctxt format type_enc
+ ? (introduce_explicit_apps_in_iterm sym_tab
+ #> introduce_predicators_in_iterm sym_tab)
+ #> enforce_type_arg_policy_in_iterm ctxt format type_enc
fun repair_fact ctxt format type_enc sym_tab =
- update_combformula (formula_map
- (repair_combterm ctxt format type_enc sym_tab))
+ update_iformula (formula_map (repair_iterm ctxt format type_enc sym_tab))
(** Helper facts **)
@@ -1490,9 +1486,9 @@
val type_pred = `make_fixed_const type_pred_name
-fun type_pred_combterm ctxt format type_enc T tm =
- CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
- |> enforce_type_arg_policy_in_combterm ctxt format type_enc, tm)
+fun type_pred_iterm ctxt format type_enc T tm =
+ IApp (IConst (type_pred, T --> @{typ bool}, [T])
+ |> enforce_type_arg_policy_in_iterm ctxt format type_enc, tm)
fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
| is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
@@ -1506,16 +1502,16 @@
ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
- CombConst (type_tag, T --> T, [T])
- |> enforce_type_arg_policy_in_combterm ctxt format type_enc
- |> ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
+ IConst (type_tag, T --> T, [T])
+ |> enforce_type_arg_policy_in_iterm ctxt format type_enc
+ |> ho_term_from_iterm ctxt format nonmono_Ts type_enc (Top_Level pos)
|> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
| _ => raise Fail "unexpected lambda-abstraction")
-and ho_term_from_combterm ctxt format nonmono_Ts type_enc =
+and ho_term_from_iterm ctxt format nonmono_Ts type_enc =
let
fun aux site u =
let
- val (head, args) = strip_combterm_comb u
+ val (head, args) = strip_iterm_comb u
val pos =
case site of
Top_Level pos => pos
@@ -1523,17 +1519,19 @@
| Elsewhere => NONE
val t =
case head of
- CombConst (name as (s, _), _, T_args) =>
+ IConst (name as (s, _), _, T_args) =>
let
val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
in
mk_aterm format type_enc name T_args (map (aux arg_site) args)
end
- | CombVar (name, _) => mk_aterm format type_enc name [] (map (aux Elsewhere) args)
- | CombAbs ((name, T), tm) =>
- AAbs ((name, ho_type_from_typ format type_enc true 0 T), aux Elsewhere tm)
- | CombApp _ => raise Fail "impossible \"CombApp\""
- val T = combtyp_of u
+ | IVar (name, _) =>
+ mk_aterm format type_enc name [] (map (aux Elsewhere) args)
+ | IAbs ((name, T), tm) =>
+ AAbs ((name, ho_type_from_typ format type_enc true 0 T),
+ aux Elsewhere tm)
+ | IApp _ => raise Fail "impossible \"IApp\""
+ val T = ityp_of u
in
t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
tag_with_type ctxt format nonmono_Ts type_enc pos T
@@ -1541,11 +1539,11 @@
I)
end
in aux end
-and formula_from_combformula ctxt format nonmono_Ts type_enc
- should_predicate_on_var =
+and formula_from_iformula ctxt format nonmono_Ts type_enc
+ should_predicate_on_var =
let
fun do_term pos =
- ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
+ ho_term_from_iterm ctxt format nonmono_Ts type_enc (Top_Level pos)
val do_bound_type =
case type_enc of
Simple_Types (_, level) =>
@@ -1555,8 +1553,8 @@
fun do_out_of_bound_type pos phi universal (name, T) =
if should_predicate_on_type ctxt nonmono_Ts type_enc
(fn () => should_predicate_on_var pos phi universal name) T then
- CombVar (name, T)
- |> type_pred_combterm ctxt format type_enc T
+ IVar (name, T)
+ |> type_pred_iterm ctxt format type_enc T
|> do_term pos |> AAtom |> SOME
else
NONE
@@ -1587,14 +1585,14 @@
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
- type_enc (j, {name, locality, kind, combformula, atomic_types}) =
+ type_enc (j, {name, locality, kind, iformula, atomic_types}) =
(prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name,
kind,
- combformula
- |> close_combformula_universally
- |> formula_from_combformula ctxt format nonmono_Ts type_enc
- should_predicate_on_var_in_formula
- (if pos then SOME true else NONE)
+ iformula
+ |> close_iformula_universally
+ |> formula_from_iformula ctxt format nonmono_Ts type_enc
+ should_predicate_on_var_in_formula
+ (if pos then SOME true else NONE)
|> bound_tvars type_enc atomic_types
|> close_formula_universally,
NONE,
@@ -1629,11 +1627,11 @@
|> close_formula_universally, isabelle_info introN, NONE)
fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
- ({name, kind, combformula, atomic_types, ...} : translated_formula) =
+ ({name, kind, iformula, atomic_types, ...} : translated_formula) =
Formula (conjecture_prefix ^ name, kind,
- formula_from_combformula ctxt format nonmono_Ts type_enc
+ formula_from_iformula ctxt format nonmono_Ts type_enc
should_predicate_on_var_in_formula (SOME false)
- (close_combformula_universally combformula)
+ (close_iformula_universally iformula)
|> bound_tvars type_enc atomic_types
|> close_formula_universally, NONE, NONE)
@@ -1661,10 +1659,10 @@
fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
let
- fun add_combterm in_conj tm =
- let val (head, args) = strip_combterm_comb tm in
+ fun add_iterm in_conj tm =
+ let val (head, args) = strip_iterm_comb tm in
(case head of
- CombConst ((s, s'), T, T_args) =>
+ IConst ((s, s'), T, T_args) =>
let val pred_sym = is_pred_sym repaired_sym_tab s in
if should_declare_sym type_enc pred_sym s then
Symtab.map_default (s, [])
@@ -1673,12 +1671,11 @@
else
I
end
- | CombAbs (_, tm) => add_combterm in_conj tm
+ | IAbs (_, tm) => add_iterm in_conj tm
| _ => I)
- #> fold (add_combterm in_conj) args
+ #> fold (add_iterm in_conj) args
end
- fun add_fact in_conj =
- fact_lift (formula_fold NONE (K (add_combterm in_conj)))
+ fun add_fact in_conj = fact_lift (formula_fold NONE (K (add_iterm in_conj)))
in
Symtab.empty
|> is_type_enc_fairly_sound type_enc
@@ -1687,10 +1684,9 @@
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
out with monotonicity" paper presented at CADE 2011. *)
-fun add_combterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
- | add_combterm_nonmonotonic_types ctxt level sound locality _
- (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
- tm2)) =
+fun add_iterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
+ | add_iterm_nonmonotonic_types ctxt level sound locality _
+ (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =
(is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
(case level of
Noninf_Nonmono_Types =>
@@ -1698,12 +1694,12 @@
not (is_type_surely_infinite ctxt sound T)
| Fin_Nonmono_Types => is_type_surely_finite ctxt false T
| _ => true)) ? insert_type ctxt I (deep_freeze_type T)
- | add_combterm_nonmonotonic_types _ _ _ _ _ _ = I
+ | add_iterm_nonmonotonic_types _ _ _ _ _ _ = I
fun add_fact_nonmonotonic_types ctxt level sound
- ({kind, locality, combformula, ...} : translated_formula) =
+ ({kind, locality, iformula, ...} : translated_formula) =
formula_fold (SOME (kind <> Conjecture))
- (add_combterm_nonmonotonic_types ctxt level sound locality)
- combformula
+ (add_iterm_nonmonotonic_types ctxt level sound locality)
+ iformula
fun nonmonotonic_types_for_facts ctxt type_enc sound facts =
let val level = level_of_type_enc type_enc in
if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
@@ -1740,7 +1736,7 @@
val bound_names =
1 upto num_args |> map (`I o make_bound_var o string_of_int)
val bounds =
- bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
+ bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
fun should_keep_arg_type T =
sym_needs_arg_types orelse
@@ -1750,12 +1746,12 @@
in
Formula (preds_sym_formula_prefix ^ s ^
(if n > 1 then "_" ^ string_of_int j else ""), kind,
- CombConst ((s, s'), T, T_args)
- |> fold (curry (CombApp o swap)) bounds
- |> type_pred_combterm ctxt format type_enc res_T
+ IConst ((s, s'), T, T_args)
+ |> fold (curry (IApp o swap)) bounds
+ |> type_pred_iterm ctxt format type_enc res_T
|> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
- |> formula_from_combformula ctxt format poly_nonmono_Ts type_enc
- (K (K (K (K true)))) (SOME true)
+ |> formula_from_iformula ctxt format poly_nonmono_Ts type_enc
+ (K (K (K (K true)))) (SOME true)
|> n > 1 ? bound_tvars type_enc (atyps_of T)
|> close_formula_universally
|> maybe_negate,