1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200
1.3 @@ -447,21 +447,22 @@
1.4 fun make_class_rel_clauses thy subs supers =
1.5 map make_class_rel_clause (class_pairs thy subs supers)
1.6
1.7 -datatype combterm =
1.8 - CombConst of name * typ * typ list |
1.9 - CombVar of name * typ |
1.10 - CombApp of combterm * combterm |
1.11 - CombAbs of (name * typ) * combterm
1.12 +(* intermediate terms *)
1.13 +datatype iterm =
1.14 + IConst of name * typ * typ list |
1.15 + IVar of name * typ |
1.16 + IApp of iterm * iterm |
1.17 + IAbs of (name * typ) * iterm
1.18
1.19 -fun combtyp_of (CombConst (_, T, _)) = T
1.20 - | combtyp_of (CombVar (_, T)) = T
1.21 - | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
1.22 - | combtyp_of (CombAbs ((_, T), tm)) = T --> combtyp_of tm
1.23 +fun ityp_of (IConst (_, T, _)) = T
1.24 + | ityp_of (IVar (_, T)) = T
1.25 + | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
1.26 + | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
1.27
1.28 (*gets the head of a combinator application, along with the list of arguments*)
1.29 -fun strip_combterm_comb u =
1.30 +fun strip_iterm_comb u =
1.31 let
1.32 - fun stripc (CombApp (t, u), ts) = stripc (t, u :: ts)
1.33 + fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
1.34 | stripc x = x
1.35 in stripc (u, []) end
1.36
1.37 @@ -471,42 +472,41 @@
1.38 [new_skolem_const_prefix, s, string_of_int num_T_args]
1.39 |> space_implode Long_Name.separator
1.40
1.41 -(* Converts a term (with combinators) into a combterm. Also accumulates sort
1.42 - infomation. *)
1.43 -fun combterm_from_term thy bs (P $ Q) =
1.44 +(* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
1.45 + Also accumulates sort infomation. *)
1.46 +fun iterm_from_term thy bs (P $ Q) =
1.47 let
1.48 - val (P', P_atomics_Ts) = combterm_from_term thy bs P
1.49 - val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
1.50 - in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
1.51 - | combterm_from_term thy _ (Const (c, T)) =
1.52 + val (P', P_atomics_Ts) = iterm_from_term thy bs P
1.53 + val (Q', Q_atomics_Ts) = iterm_from_term thy bs Q
1.54 + in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
1.55 + | iterm_from_term thy _ (Const (c, T)) =
1.56 let
1.57 val tvar_list =
1.58 (if String.isPrefix old_skolem_const_prefix c then
1.59 [] |> Term.add_tvarsT T |> map TVar
1.60 else
1.61 (c, T) |> Sign.const_typargs thy)
1.62 - val c' = CombConst (`make_fixed_const c, T, tvar_list)
1.63 + val c' = IConst (`make_fixed_const c, T, tvar_list)
1.64 in (c', atyps_of T) end
1.65 - | combterm_from_term _ _ (Free (v, T)) =
1.66 - (CombConst (`make_fixed_var v, T, []), atyps_of T)
1.67 - | combterm_from_term _ _ (Var (v as (s, _), T)) =
1.68 + | iterm_from_term _ _ (Free (v, T)) =
1.69 + (IConst (`make_fixed_var v, T, []), atyps_of T)
1.70 + | iterm_from_term _ _ (Var (v as (s, _), T)) =
1.71 (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
1.72 let
1.73 val Ts = T |> strip_type |> swap |> op ::
1.74 val s' = new_skolem_const_name s (length Ts)
1.75 - in CombConst (`make_fixed_const s', T, Ts) end
1.76 + in IConst (`make_fixed_const s', T, Ts) end
1.77 else
1.78 - CombVar ((make_schematic_var v, s), T), atyps_of T)
1.79 - | combterm_from_term _ bs (Bound j) =
1.80 - nth bs j
1.81 - |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
1.82 - | combterm_from_term thy bs (Abs (s, T, t)) =
1.83 + IVar ((make_schematic_var v, s), T), atyps_of T)
1.84 + | iterm_from_term _ bs (Bound j) =
1.85 + nth bs j |> (fn (s, T) => (IConst (`make_bound_var s, T, []), atyps_of T))
1.86 + | iterm_from_term thy bs (Abs (s, T, t)) =
1.87 let
1.88 fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
1.89 val s = vary s
1.90 - val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t
1.91 + val (tm, atomic_Ts) = iterm_from_term thy ((s, T) :: bs) t
1.92 in
1.93 - (CombAbs ((`make_bound_var s, T), tm),
1.94 + (IAbs ((`make_bound_var s, T), tm),
1.95 union (op =) atomic_Ts (atyps_of T))
1.96 end
1.97
1.98 @@ -621,15 +621,15 @@
1.99 {name : string,
1.100 locality : locality,
1.101 kind : formula_kind,
1.102 - combformula : (name, typ, combterm) formula,
1.103 + iformula : (name, typ, iterm) formula,
1.104 atomic_types : typ list}
1.105
1.106 -fun update_combformula f ({name, locality, kind, combformula, atomic_types}
1.107 - : translated_formula) =
1.108 - {name = name, locality = locality, kind = kind, combformula = f combformula,
1.109 +fun update_iformula f ({name, locality, kind, iformula, atomic_types}
1.110 + : translated_formula) =
1.111 + {name = name, locality = locality, kind = kind, iformula = f iformula,
1.112 atomic_types = atomic_types} : translated_formula
1.113
1.114 -fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
1.115 +fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
1.116
1.117 val type_instance = Sign.typ_instance o Proof_Context.theory_of
1.118
1.119 @@ -712,11 +712,11 @@
1.120 |> filter_out (member (op =) bounds o fst))
1.121 in mk_aquant AForall (formula_vars [] phi []) phi end
1.122
1.123 -fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
1.124 - | combterm_vars (CombConst _) = I
1.125 - | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
1.126 - | combterm_vars (CombAbs (_, tm)) = combterm_vars tm
1.127 -fun close_combformula_universally phi = close_universally combterm_vars phi
1.128 +fun iterm_vars (IApp (tm1, tm2)) = fold iterm_vars [tm1, tm2]
1.129 + | iterm_vars (IConst _) = I
1.130 + | iterm_vars (IVar (name, T)) = insert (op =) (name, SOME T)
1.131 + | iterm_vars (IAbs (_, tm)) = iterm_vars tm
1.132 +fun close_iformula_universally phi = close_universally iterm_vars phi
1.133
1.134 fun term_vars bounds (ATerm (name as (s, _), tms)) =
1.135 (is_tptp_variable s andalso not (member (op =) bounds name))
1.136 @@ -816,9 +816,9 @@
1.137
1.138 fun introduce_proxies type_enc =
1.139 let
1.140 - fun intro top_level (CombApp (tm1, tm2)) =
1.141 - CombApp (intro top_level tm1, intro false tm2)
1.142 - | intro top_level (CombConst (name as (s, _), T, T_args)) =
1.143 + fun intro top_level (IApp (tm1, tm2)) =
1.144 + IApp (intro top_level tm1, intro false tm2)
1.145 + | intro top_level (IConst (name as (s, _), T, T_args)) =
1.146 (case proxify_const s of
1.147 SOME proxy_base =>
1.148 if top_level orelse is_type_enc_higher_order type_enc then
1.149 @@ -838,15 +838,15 @@
1.150 else
1.151 (proxy_base |>> prefix const_prefix, T_args)
1.152 | NONE => (name, T_args))
1.153 - |> (fn (name, T_args) => CombConst (name, T, T_args))
1.154 - | intro _ (CombAbs (bound, tm)) = CombAbs (bound, intro false tm)
1.155 + |> (fn (name, T_args) => IConst (name, T, T_args))
1.156 + | intro _ (IAbs (bound, tm)) = IAbs (bound, intro false tm)
1.157 | intro _ tm = tm
1.158 in intro true end
1.159
1.160 -fun combformula_from_prop thy type_enc eq_as_iff =
1.161 +fun iformula_from_prop thy type_enc eq_as_iff =
1.162 let
1.163 fun do_term bs t atomic_types =
1.164 - combterm_from_term thy bs (Envir.eta_contract t)
1.165 + iterm_from_term thy bs (Envir.eta_contract t)
1.166 |>> (introduce_proxies type_enc #> AAtom)
1.167 ||> union (op =) atomic_types
1.168 fun do_quant bs q s T t' =
1.169 @@ -986,10 +986,10 @@
1.170 (* making fact and conjecture formulas *)
1.171 fun make_formula thy type_enc eq_as_iff name loc kind t =
1.172 let
1.173 - val (combformula, atomic_types) =
1.174 - combformula_from_prop thy type_enc eq_as_iff t []
1.175 + val (iformula, atomic_types) =
1.176 + iformula_from_prop thy type_enc eq_as_iff t []
1.177 in
1.178 - {name = name, locality = loc, kind = kind, combformula = combformula,
1.179 + {name = name, locality = loc, kind = kind, iformula = iformula,
1.180 atomic_types = atomic_types}
1.181 end
1.182
1.183 @@ -999,7 +999,7 @@
1.184 case t |> preproc ? preprocess_prop ctxt trans_lambdas presimp_consts Axiom
1.185 |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
1.186 loc Axiom of
1.187 - formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
1.188 + formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
1.189 if s = tptp_true then NONE else SOME formula
1.190 | formula => SOME formula
1.191 end
1.192 @@ -1017,7 +1017,7 @@
1.193 (Conjecture, I)
1.194 else
1.195 (prem_kind,
1.196 - if prem_kind = Conjecture then update_combformula mk_anot
1.197 + if prem_kind = Conjecture then update_iformula mk_anot
1.198 else I)
1.199 in
1.200 t |> preproc ?
1.201 @@ -1054,9 +1054,9 @@
1.202 should_encode_type ctxt nonmono_Ts level T
1.203 | should_predicate_on_type _ _ _ _ _ = false
1.204
1.205 -fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
1.206 +fun is_var_or_bound_var (IConst ((s, _), _, _)) =
1.207 String.isPrefix bound_var_prefix s
1.208 - | is_var_or_bound_var (CombVar _) = true
1.209 + | is_var_or_bound_var (IVar _) = true
1.210 | is_var_or_bound_var _ = false
1.211
1.212 datatype tag_site =
1.213 @@ -1096,7 +1096,7 @@
1.214 type sym_info =
1.215 {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
1.216
1.217 -fun add_combterm_syms_to_table ctxt explicit_apply =
1.218 +fun add_iterm_syms_to_table ctxt explicit_apply =
1.219 let
1.220 fun consider_var_arity const_T var_T max_ary =
1.221 let
1.222 @@ -1128,9 +1128,9 @@
1.223 else
1.224 accum
1.225 fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1.226 - let val (head, args) = strip_combterm_comb tm in
1.227 + let val (head, args) = strip_iterm_comb tm in
1.228 (case head of
1.229 - CombConst ((s, _), T, _) =>
1.230 + IConst ((s, _), T, _) =>
1.231 if String.isPrefix bound_var_prefix s then
1.232 add_var_or_bound_var T accum
1.233 else
1.234 @@ -1170,16 +1170,15 @@
1.235 sym_tab
1.236 end)
1.237 end
1.238 - | CombVar (_, T) => add_var_or_bound_var T accum
1.239 - | CombAbs ((_, T), tm) =>
1.240 - accum |> add_var_or_bound_var T |> add false tm
1.241 + | IVar (_, T) => add_var_or_bound_var T accum
1.242 + | IAbs ((_, T), tm) => accum |> add_var_or_bound_var T |> add false tm
1.243 | _ => accum)
1.244 |> fold (add false) args
1.245 end
1.246 in add true end
1.247 fun add_fact_syms_to_table ctxt explicit_apply =
1.248 fact_lift (formula_fold NONE
1.249 - (K (add_combterm_syms_to_table ctxt explicit_apply)))
1.250 + (K (add_iterm_syms_to_table ctxt explicit_apply)))
1.251
1.252 val default_sym_tab_entries : (string * sym_info) list =
1.253 (prefixed_predicator_name,
1.254 @@ -1219,33 +1218,32 @@
1.255 | NONE => false
1.256
1.257 val predicator_combconst =
1.258 - CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
1.259 -fun predicator tm = CombApp (predicator_combconst, tm)
1.260 + IConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
1.261 +fun predicator tm = IApp (predicator_combconst, tm)
1.262
1.263 -fun introduce_predicators_in_combterm sym_tab tm =
1.264 - case strip_combterm_comb tm of
1.265 - (CombConst ((s, _), _, _), _) =>
1.266 +fun introduce_predicators_in_iterm sym_tab tm =
1.267 + case strip_iterm_comb tm of
1.268 + (IConst ((s, _), _, _), _) =>
1.269 if is_pred_sym sym_tab s then tm else predicator tm
1.270 | _ => predicator tm
1.271
1.272 -fun list_app head args = fold (curry (CombApp o swap)) args head
1.273 +fun list_app head args = fold (curry (IApp o swap)) args head
1.274
1.275 val app_op = `make_fixed_const app_op_name
1.276
1.277 fun explicit_app arg head =
1.278 let
1.279 - val head_T = combtyp_of head
1.280 + val head_T = ityp_of head
1.281 val (arg_T, res_T) = dest_funT head_T
1.282 - val explicit_app =
1.283 - CombConst (app_op, head_T --> head_T, [arg_T, res_T])
1.284 + val explicit_app = IConst (app_op, head_T --> head_T, [arg_T, res_T])
1.285 in list_app explicit_app [head, arg] end
1.286 fun list_explicit_app head args = fold explicit_app args head
1.287
1.288 -fun introduce_explicit_apps_in_combterm sym_tab =
1.289 +fun introduce_explicit_apps_in_iterm sym_tab =
1.290 let
1.291 fun aux tm =
1.292 - case strip_combterm_comb tm of
1.293 - (head as CombConst ((s, _), _, _), args) =>
1.294 + case strip_iterm_comb tm of
1.295 + (head as IConst ((s, _), _, _), args) =>
1.296 args |> map aux
1.297 |> chop (min_arity_of sym_tab s)
1.298 |>> list_app head
1.299 @@ -1279,12 +1277,11 @@
1.300 end
1.301 handle TYPE _ => T_args
1.302
1.303 -fun enforce_type_arg_policy_in_combterm ctxt format type_enc =
1.304 +fun enforce_type_arg_policy_in_iterm ctxt format type_enc =
1.305 let
1.306 val thy = Proof_Context.theory_of ctxt
1.307 - fun aux arity (CombApp (tm1, tm2)) =
1.308 - CombApp (aux (arity + 1) tm1, aux 0 tm2)
1.309 - | aux arity (CombConst (name as (s, _), T, T_args)) =
1.310 + fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2)
1.311 + | aux arity (IConst (name as (s, _), T, T_args)) =
1.312 (case strip_prefix_and_unascii const_prefix s of
1.313 NONE => (name, T_args)
1.314 | SOME s'' =>
1.315 @@ -1301,19 +1298,18 @@
1.316 name, [])
1.317 | No_Type_Args => (name, [])
1.318 end)
1.319 - |> (fn (name, T_args) => CombConst (name, T, T_args))
1.320 - | aux _ (CombAbs (bound, tm)) = CombAbs (bound, aux 0 tm)
1.321 + |> (fn (name, T_args) => IConst (name, T, T_args))
1.322 + | aux _ (IAbs (bound, tm)) = IAbs (bound, aux 0 tm)
1.323 | aux _ tm = tm
1.324 in aux 0 end
1.325
1.326 -fun repair_combterm ctxt format type_enc sym_tab =
1.327 +fun repair_iterm ctxt format type_enc sym_tab =
1.328 not (is_type_enc_higher_order type_enc)
1.329 - ? (introduce_explicit_apps_in_combterm sym_tab
1.330 - #> introduce_predicators_in_combterm sym_tab)
1.331 - #> enforce_type_arg_policy_in_combterm ctxt format type_enc
1.332 + ? (introduce_explicit_apps_in_iterm sym_tab
1.333 + #> introduce_predicators_in_iterm sym_tab)
1.334 + #> enforce_type_arg_policy_in_iterm ctxt format type_enc
1.335 fun repair_fact ctxt format type_enc sym_tab =
1.336 - update_combformula (formula_map
1.337 - (repair_combterm ctxt format type_enc sym_tab))
1.338 + update_iformula (formula_map (repair_iterm ctxt format type_enc sym_tab))
1.339
1.340 (** Helper facts **)
1.341
1.342 @@ -1490,9 +1486,9 @@
1.343
1.344 val type_pred = `make_fixed_const type_pred_name
1.345
1.346 -fun type_pred_combterm ctxt format type_enc T tm =
1.347 - CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
1.348 - |> enforce_type_arg_policy_in_combterm ctxt format type_enc, tm)
1.349 +fun type_pred_iterm ctxt format type_enc T tm =
1.350 + IApp (IConst (type_pred, T --> @{typ bool}, [T])
1.351 + |> enforce_type_arg_policy_in_iterm ctxt format type_enc, tm)
1.352
1.353 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1.354 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1.355 @@ -1506,16 +1502,16 @@
1.356 ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
1.357
1.358 fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
1.359 - CombConst (type_tag, T --> T, [T])
1.360 - |> enforce_type_arg_policy_in_combterm ctxt format type_enc
1.361 - |> ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
1.362 + IConst (type_tag, T --> T, [T])
1.363 + |> enforce_type_arg_policy_in_iterm ctxt format type_enc
1.364 + |> ho_term_from_iterm ctxt format nonmono_Ts type_enc (Top_Level pos)
1.365 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
1.366 | _ => raise Fail "unexpected lambda-abstraction")
1.367 -and ho_term_from_combterm ctxt format nonmono_Ts type_enc =
1.368 +and ho_term_from_iterm ctxt format nonmono_Ts type_enc =
1.369 let
1.370 fun aux site u =
1.371 let
1.372 - val (head, args) = strip_combterm_comb u
1.373 + val (head, args) = strip_iterm_comb u
1.374 val pos =
1.375 case site of
1.376 Top_Level pos => pos
1.377 @@ -1523,17 +1519,19 @@
1.378 | Elsewhere => NONE
1.379 val t =
1.380 case head of
1.381 - CombConst (name as (s, _), _, T_args) =>
1.382 + IConst (name as (s, _), _, T_args) =>
1.383 let
1.384 val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
1.385 in
1.386 mk_aterm format type_enc name T_args (map (aux arg_site) args)
1.387 end
1.388 - | CombVar (name, _) => mk_aterm format type_enc name [] (map (aux Elsewhere) args)
1.389 - | CombAbs ((name, T), tm) =>
1.390 - AAbs ((name, ho_type_from_typ format type_enc true 0 T), aux Elsewhere tm)
1.391 - | CombApp _ => raise Fail "impossible \"CombApp\""
1.392 - val T = combtyp_of u
1.393 + | IVar (name, _) =>
1.394 + mk_aterm format type_enc name [] (map (aux Elsewhere) args)
1.395 + | IAbs ((name, T), tm) =>
1.396 + AAbs ((name, ho_type_from_typ format type_enc true 0 T),
1.397 + aux Elsewhere tm)
1.398 + | IApp _ => raise Fail "impossible \"IApp\""
1.399 + val T = ityp_of u
1.400 in
1.401 t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
1.402 tag_with_type ctxt format nonmono_Ts type_enc pos T
1.403 @@ -1541,11 +1539,11 @@
1.404 I)
1.405 end
1.406 in aux end
1.407 -and formula_from_combformula ctxt format nonmono_Ts type_enc
1.408 - should_predicate_on_var =
1.409 +and formula_from_iformula ctxt format nonmono_Ts type_enc
1.410 + should_predicate_on_var =
1.411 let
1.412 fun do_term pos =
1.413 - ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
1.414 + ho_term_from_iterm ctxt format nonmono_Ts type_enc (Top_Level pos)
1.415 val do_bound_type =
1.416 case type_enc of
1.417 Simple_Types (_, level) =>
1.418 @@ -1555,8 +1553,8 @@
1.419 fun do_out_of_bound_type pos phi universal (name, T) =
1.420 if should_predicate_on_type ctxt nonmono_Ts type_enc
1.421 (fn () => should_predicate_on_var pos phi universal name) T then
1.422 - CombVar (name, T)
1.423 - |> type_pred_combterm ctxt format type_enc T
1.424 + IVar (name, T)
1.425 + |> type_pred_iterm ctxt format type_enc T
1.426 |> do_term pos |> AAtom |> SOME
1.427 else
1.428 NONE
1.429 @@ -1587,14 +1585,14 @@
1.430 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1.431 the remote provers might care. *)
1.432 fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
1.433 - type_enc (j, {name, locality, kind, combformula, atomic_types}) =
1.434 + type_enc (j, {name, locality, kind, iformula, atomic_types}) =
1.435 (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name,
1.436 kind,
1.437 - combformula
1.438 - |> close_combformula_universally
1.439 - |> formula_from_combformula ctxt format nonmono_Ts type_enc
1.440 - should_predicate_on_var_in_formula
1.441 - (if pos then SOME true else NONE)
1.442 + iformula
1.443 + |> close_iformula_universally
1.444 + |> formula_from_iformula ctxt format nonmono_Ts type_enc
1.445 + should_predicate_on_var_in_formula
1.446 + (if pos then SOME true else NONE)
1.447 |> bound_tvars type_enc atomic_types
1.448 |> close_formula_universally,
1.449 NONE,
1.450 @@ -1629,11 +1627,11 @@
1.451 |> close_formula_universally, isabelle_info introN, NONE)
1.452
1.453 fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
1.454 - ({name, kind, combformula, atomic_types, ...} : translated_formula) =
1.455 + ({name, kind, iformula, atomic_types, ...} : translated_formula) =
1.456 Formula (conjecture_prefix ^ name, kind,
1.457 - formula_from_combformula ctxt format nonmono_Ts type_enc
1.458 + formula_from_iformula ctxt format nonmono_Ts type_enc
1.459 should_predicate_on_var_in_formula (SOME false)
1.460 - (close_combformula_universally combformula)
1.461 + (close_iformula_universally iformula)
1.462 |> bound_tvars type_enc atomic_types
1.463 |> close_formula_universally, NONE, NONE)
1.464
1.465 @@ -1661,10 +1659,10 @@
1.466
1.467 fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
1.468 let
1.469 - fun add_combterm in_conj tm =
1.470 - let val (head, args) = strip_combterm_comb tm in
1.471 + fun add_iterm in_conj tm =
1.472 + let val (head, args) = strip_iterm_comb tm in
1.473 (case head of
1.474 - CombConst ((s, s'), T, T_args) =>
1.475 + IConst ((s, s'), T, T_args) =>
1.476 let val pred_sym = is_pred_sym repaired_sym_tab s in
1.477 if should_declare_sym type_enc pred_sym s then
1.478 Symtab.map_default (s, [])
1.479 @@ -1673,12 +1671,11 @@
1.480 else
1.481 I
1.482 end
1.483 - | CombAbs (_, tm) => add_combterm in_conj tm
1.484 + | IAbs (_, tm) => add_iterm in_conj tm
1.485 | _ => I)
1.486 - #> fold (add_combterm in_conj) args
1.487 + #> fold (add_iterm in_conj) args
1.488 end
1.489 - fun add_fact in_conj =
1.490 - fact_lift (formula_fold NONE (K (add_combterm in_conj)))
1.491 + fun add_fact in_conj = fact_lift (formula_fold NONE (K (add_iterm in_conj)))
1.492 in
1.493 Symtab.empty
1.494 |> is_type_enc_fairly_sound type_enc
1.495 @@ -1687,10 +1684,9 @@
1.496
1.497 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
1.498 out with monotonicity" paper presented at CADE 2011. *)
1.499 -fun add_combterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
1.500 - | add_combterm_nonmonotonic_types ctxt level sound locality _
1.501 - (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
1.502 - tm2)) =
1.503 +fun add_iterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
1.504 + | add_iterm_nonmonotonic_types ctxt level sound locality _
1.505 + (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =
1.506 (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
1.507 (case level of
1.508 Noninf_Nonmono_Types =>
1.509 @@ -1698,12 +1694,12 @@
1.510 not (is_type_surely_infinite ctxt sound T)
1.511 | Fin_Nonmono_Types => is_type_surely_finite ctxt false T
1.512 | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
1.513 - | add_combterm_nonmonotonic_types _ _ _ _ _ _ = I
1.514 + | add_iterm_nonmonotonic_types _ _ _ _ _ _ = I
1.515 fun add_fact_nonmonotonic_types ctxt level sound
1.516 - ({kind, locality, combformula, ...} : translated_formula) =
1.517 + ({kind, locality, iformula, ...} : translated_formula) =
1.518 formula_fold (SOME (kind <> Conjecture))
1.519 - (add_combterm_nonmonotonic_types ctxt level sound locality)
1.520 - combformula
1.521 + (add_iterm_nonmonotonic_types ctxt level sound locality)
1.522 + iformula
1.523 fun nonmonotonic_types_for_facts ctxt type_enc sound facts =
1.524 let val level = level_of_type_enc type_enc in
1.525 if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
1.526 @@ -1740,7 +1736,7 @@
1.527 val bound_names =
1.528 1 upto num_args |> map (`I o make_bound_var o string_of_int)
1.529 val bounds =
1.530 - bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
1.531 + bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
1.532 val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
1.533 fun should_keep_arg_type T =
1.534 sym_needs_arg_types orelse
1.535 @@ -1750,12 +1746,12 @@
1.536 in
1.537 Formula (preds_sym_formula_prefix ^ s ^
1.538 (if n > 1 then "_" ^ string_of_int j else ""), kind,
1.539 - CombConst ((s, s'), T, T_args)
1.540 - |> fold (curry (CombApp o swap)) bounds
1.541 - |> type_pred_combterm ctxt format type_enc res_T
1.542 + IConst ((s, s'), T, T_args)
1.543 + |> fold (curry (IApp o swap)) bounds
1.544 + |> type_pred_iterm ctxt format type_enc res_T
1.545 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
1.546 - |> formula_from_combformula ctxt format poly_nonmono_Ts type_enc
1.547 - (K (K (K (K true)))) (SOME true)
1.548 + |> formula_from_iformula ctxt format poly_nonmono_Ts type_enc
1.549 + (K (K (K (K true)))) (SOME true)
1.550 |> n > 1 ? bound_tvars type_enc (atyps_of T)
1.551 |> close_formula_universally
1.552 |> maybe_negate,