1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
1.3 @@ -359,9 +359,9 @@
1.4 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
1.5 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
1.6
1.7 -fun make_schematic_type_var (x, i) =
1.8 - tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
1.9 -fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
1.10 +fun make_tvar (s, i) = tvar_prefix ^ (ascii_of_indexname (unprefix "'" s, i))
1.11 +fun make_tfree s = tfree_prefix ^ (ascii_of (unprefix "'" s))
1.12 +fun tvar_name (x as (s, _)) = (make_tvar x, s)
1.13
1.14 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
1.15 local
1.16 @@ -407,32 +407,36 @@
1.17 | _ => I)
1.18 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
1.19
1.20 +val tvar_a_str = "'a"
1.21 +val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
1.22 +val tvar_a_name = tvar_name (tvar_a_str, 0)
1.23 +val itself_name = `make_fixed_type_const @{type_name itself}
1.24 +val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
1.25 +val tvar_a_atype = AType (tvar_a_name, [])
1.26 +val a_itself_atype = AType (itself_name, [tvar_a_atype])
1.27 +
1.28 (** Definitions and functions for FOL clauses and formulas for TPTP **)
1.29
1.30 (** Isabelle arities **)
1.31
1.32 -type arity_atom = name * name * name list
1.33 -
1.34 val type_class = the_single @{sort type}
1.35
1.36 type arity_clause =
1.37 {name : string,
1.38 - prem_atoms : arity_atom list,
1.39 - concl_atom : arity_atom}
1.40 + prems : (string * typ) list,
1.41 + concl : string * typ}
1.42
1.43 -fun add_prem_atom tvar =
1.44 - fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
1.45 +fun add_prem_atom T = fold (fn s => s <> type_class ? cons (s, T))
1.46
1.47 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
1.48 -fun make_axiom_arity_clause (tcons, name, (cls, args)) =
1.49 +fun make_axiom_arity_clause (tc, name, (class, args)) =
1.50 let
1.51 - val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
1.52 - val tvars_srts = ListPair.zip (tvars, args)
1.53 + val tvars =
1.54 + map (fn j => TVar ((tvar_a_str, j), @{sort HOL.type}))
1.55 + (1 upto length args)
1.56 in
1.57 - {name = name,
1.58 - prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
1.59 - concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
1.60 - tvars ~~ tvars)}
1.61 + {name = name, prems = fold (uncurry add_prem_atom) (tvars ~~ args) [],
1.62 + concl = (class, Type (tc, tvars))}
1.63 end
1.64
1.65 fun arity_clause _ _ (_, []) = []
1.66 @@ -487,8 +491,8 @@
1.67
1.68 type class_rel_clause =
1.69 {name : string,
1.70 - subclass : name,
1.71 - superclass : name}
1.72 + subclass : string,
1.73 + superclass : string}
1.74
1.75 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
1.76 in theory "thy". *)
1.77 @@ -501,8 +505,7 @@
1.78 in fold add_supers subs [] end
1.79
1.80 fun make_class_rel_clause (sub, super) =
1.81 - {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
1.82 - superclass = `make_type_class super}
1.83 + {name = sub ^ "_" ^ super, subclass = sub, superclass = super}
1.84
1.85 fun make_class_rel_clauses thy subs supers =
1.86 map make_class_rel_clause (class_pairs thy subs supers)
1.87 @@ -528,14 +531,6 @@
1.88
1.89 fun atomic_types_of T = fold_atyps (insert (op =)) T []
1.90
1.91 -val tvar_a_str = "'a"
1.92 -val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
1.93 -val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
1.94 -val itself_name = `make_fixed_type_const @{type_name itself}
1.95 -val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
1.96 -val tvar_a_atype = AType (tvar_a_name, [])
1.97 -val a_itself_atype = AType (itself_name, [tvar_a_atype])
1.98 -
1.99 fun new_skolem_const_name s num_T_args =
1.100 [new_skolem_const_prefix, s, string_of_int num_T_args]
1.101 |> Long_Name.implode
1.102 @@ -872,79 +867,9 @@
1.103 end
1.104 end
1.105
1.106 -(* Make atoms for sorted type variables. *)
1.107 -fun generic_add_sorts_on_type (_, []) = I
1.108 - | generic_add_sorts_on_type ((x, i), s :: ss) =
1.109 - generic_add_sorts_on_type ((x, i), ss)
1.110 - #> (if s = the_single @{sort HOL.type} then
1.111 - I
1.112 - else if i = ~1 then
1.113 - insert (op =) (`make_type_class s, `make_fixed_type_var x)
1.114 - else
1.115 - insert (op =) (`make_type_class s,
1.116 - (make_schematic_type_var (x, i), x)))
1.117 -fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
1.118 - | add_sorts_on_tfree _ = I
1.119 -fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
1.120 - | add_sorts_on_tvar _ = I
1.121 -
1.122 -fun type_class_formula type_enc class arg =
1.123 - AAtom (ATerm ((class, []), arg ::
1.124 - (case type_enc of
1.125 - Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
1.126 - [ATerm ((TYPE_name, []), [arg])]
1.127 - | _ => [])))
1.128 -fun formulas_for_types type_enc add_sorts_on_typ Ts =
1.129 - [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
1.130 - |> map (fn (class, name) =>
1.131 - type_class_formula type_enc class (ATerm ((name, []), [])))
1.132 -
1.133 -fun mk_aconns c phis =
1.134 - let val (phis', phi') = split_last phis in
1.135 - fold_rev (mk_aconn c) phis' phi'
1.136 - end
1.137 -fun mk_ahorn [] phi = phi
1.138 - | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
1.139 -fun mk_aquant _ [] phi = phi
1.140 - | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
1.141 - if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
1.142 - | mk_aquant q xs phi = AQuant (q, xs, phi)
1.143 -
1.144 -fun close_universally add_term_vars phi =
1.145 - let
1.146 - fun add_formula_vars bounds (AQuant (_, xs, phi)) =
1.147 - add_formula_vars (map fst xs @ bounds) phi
1.148 - | add_formula_vars bounds (AConn (_, phis)) =
1.149 - fold (add_formula_vars bounds) phis
1.150 - | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
1.151 - in mk_aquant AForall (add_formula_vars [] phi []) phi end
1.152 -
1.153 -fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
1.154 - (if is_tptp_variable s andalso
1.155 - not (String.isPrefix tvar_prefix s) andalso
1.156 - not (member (op =) bounds name) then
1.157 - insert (op =) (name, NONE)
1.158 - else
1.159 - I)
1.160 - #> fold (add_term_vars bounds) tms
1.161 - | add_term_vars bounds (AAbs (((name, _), tm), args)) =
1.162 - add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
1.163 -fun close_formula_universally phi = close_universally add_term_vars phi
1.164 -
1.165 -fun add_iterm_vars bounds (IApp (tm1, tm2)) =
1.166 - fold (add_iterm_vars bounds) [tm1, tm2]
1.167 - | add_iterm_vars _ (IConst _) = I
1.168 - | add_iterm_vars bounds (IVar (name, T)) =
1.169 - not (member (op =) bounds name) ? insert (op =) (name, SOME T)
1.170 - | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
1.171 -
1.172 -fun close_iformula_universally phi = close_universally add_iterm_vars phi
1.173 -
1.174 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
1.175 val fused_infinite_type = Type (fused_infinite_type_name, [])
1.176
1.177 -fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
1.178 -
1.179 fun ho_term_from_typ type_enc =
1.180 let
1.181 fun term (Type (s, Ts)) =
1.182 @@ -957,7 +882,7 @@
1.183 else
1.184 `make_fixed_type_const s,
1.185 []), map term Ts)
1.186 - | term (TFree (s, _)) = ATerm ((`make_fixed_type_var s, []), [])
1.187 + | term (TFree (s, _)) = ATerm ((`make_tfree s, []), [])
1.188 | term (TVar (x, _)) = ATerm ((tvar_name x, []), [])
1.189 in term end
1.190
1.191 @@ -1011,6 +936,87 @@
1.192 ho_type_from_ho_term type_enc pred_sym ary
1.193 o ho_term_from_typ type_enc
1.194
1.195 +(* Make atoms for sorted type variables. *)
1.196 +fun generic_add_sorts_on_type _ [] = I
1.197 + | generic_add_sorts_on_type T (s :: ss) =
1.198 + generic_add_sorts_on_type T ss
1.199 + #> (if s = the_single @{sort HOL.type} then I else insert (op =) (s, T))
1.200 +fun add_sorts_on_tfree (T as TFree (_, S)) = generic_add_sorts_on_type T S
1.201 + | add_sorts_on_tfree _ = I
1.202 +fun add_sorts_on_tvar (T as TVar (_, S)) = generic_add_sorts_on_type T S
1.203 + | add_sorts_on_tvar _ = I
1.204 +
1.205 +fun process_type_args type_enc T_args =
1.206 + if is_type_enc_native type_enc then
1.207 + (map (ho_type_from_typ type_enc false 0) T_args, [])
1.208 + else
1.209 + ([], map_filter (ho_term_for_type_arg type_enc) T_args)
1.210 +
1.211 +fun type_class_atom type_enc (class, T) =
1.212 + let
1.213 + val class = `make_type_class class
1.214 + val (ty_args, tm_args) = process_type_args type_enc [T]
1.215 + val tm_args =
1.216 + tm_args @
1.217 + (case type_enc of
1.218 + Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
1.219 + [ATerm ((TYPE_name, ty_args), [])]
1.220 + | _ => [])
1.221 + in AAtom (ATerm ((class, ty_args), tm_args)) end
1.222 +fun formulas_for_types type_enc add_sorts_on_typ Ts =
1.223 + [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
1.224 + |> map (type_class_atom type_enc)
1.225 +
1.226 +fun mk_aconns c phis =
1.227 + let val (phis', phi') = split_last phis in
1.228 + fold_rev (mk_aconn c) phis' phi'
1.229 + end
1.230 +
1.231 +fun mk_ahorn [] phi = phi
1.232 + | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
1.233 +
1.234 +fun mk_aquant _ [] phi = phi
1.235 + | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
1.236 + if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
1.237 + | mk_aquant q xs phi = AQuant (q, xs, phi)
1.238 +
1.239 +fun mk_atyquant _ [] phi = phi
1.240 + | mk_atyquant q xs (phi as ATyQuant (q', xs', phi')) =
1.241 + if q = q' then ATyQuant (q, xs @ xs', phi') else ATyQuant (q, xs, phi)
1.242 + | mk_atyquant q xs phi = ATyQuant (q, xs, phi)
1.243 +
1.244 +fun close_universally add_term_vars phi =
1.245 + let
1.246 + fun add_formula_vars bounds (ATyQuant (_, _, phi)) =
1.247 + add_formula_vars bounds phi
1.248 + | add_formula_vars bounds (AQuant (_, xs, phi)) =
1.249 + add_formula_vars (map fst xs @ bounds) phi
1.250 + | add_formula_vars bounds (AConn (_, phis)) =
1.251 + fold (add_formula_vars bounds) phis
1.252 + | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
1.253 + in mk_aquant AForall (add_formula_vars [] phi []) phi end
1.254 +
1.255 +fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
1.256 + (if is_tptp_variable s andalso
1.257 + not (String.isPrefix tvar_prefix s) andalso
1.258 + not (member (op =) bounds name) then
1.259 + insert (op =) (name, NONE)
1.260 + else
1.261 + I)
1.262 + #> fold (add_term_vars bounds) tms
1.263 + | add_term_vars bounds (AAbs (((name, _), tm), args)) =
1.264 + add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
1.265 +fun close_formula_universally phi = close_universally add_term_vars phi
1.266 +
1.267 +fun add_iterm_vars bounds (IApp (tm1, tm2)) =
1.268 + fold (add_iterm_vars bounds) [tm1, tm2]
1.269 + | add_iterm_vars _ (IConst _) = I
1.270 + | add_iterm_vars bounds (IVar (name, T)) =
1.271 + not (member (op =) bounds name) ? insert (op =) (name, SOME T)
1.272 + | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
1.273 +
1.274 +fun close_iformula_universally phi = close_universally add_iterm_vars phi
1.275 +
1.276 fun aliased_uncurried ary (s, s') =
1.277 (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
1.278 fun unaliased_uncurried (s, s') =
1.279 @@ -1718,18 +1724,16 @@
1.280 @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
1.281 |> map (apsnd (map (apsnd zero_var_indexes)))
1.282
1.283 -fun atype_of_type_vars (Native (_, Raw_Polymorphic _, _)) = SOME atype_of_types
1.284 - | atype_of_type_vars (Native (_, Type_Class_Polymorphic, _)) =
1.285 - SOME atype_of_types (* ### FIXME *)
1.286 - | atype_of_type_vars _ = NONE
1.287 -
1.288 fun bound_tvars type_enc sorts Ts =
1.289 - (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
1.290 - #> mk_aquant AForall
1.291 - (map_filter (fn TVar (x as (s, _), _) =>
1.292 - SOME ((make_schematic_type_var x, s),
1.293 - atype_of_type_vars type_enc)
1.294 - | _ => NONE) Ts)
1.295 + case filter is_TVar Ts of
1.296 + [] => I
1.297 + | Ts =>
1.298 + (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
1.299 + #> (if is_type_enc_native type_enc then
1.300 + mk_atyquant AForall
1.301 + (map (fn TVar (x, _) => AType (tvar_name x, [])) Ts)
1.302 + else
1.303 + mk_aquant AForall (map (fn TVar (x, _) => (tvar_name x, NONE)) Ts))
1.304
1.305 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
1.306 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
1.307 @@ -1994,11 +1998,9 @@
1.308 | should_generate_tag_bound_decl _ _ _ _ _ = false
1.309
1.310 fun mk_aterm type_enc name T_args args =
1.311 -(* ### FIXME
1.312 - if is_type_enc_polymorphic type_enc then
1.313 - ATerm ((name, map (ho_type_from_typ type_enc false 0) T_args), args)
1.314 - else *)
1.315 - ATerm ((name, []), map_filter (ho_term_for_type_arg type_enc) T_args @ args)
1.316 + let val (ty_args, tm_args) = process_type_args type_enc T_args in
1.317 + ATerm ((name, ty_args), tm_args @ args)
1.318 + end
1.319
1.320 fun do_bound_type ctxt mono type_enc =
1.321 case type_enc of
1.322 @@ -2032,7 +2034,7 @@
1.323 map (term Elsewhere) args |> mk_aterm type_enc name []
1.324 | IAbs ((name, T), tm) =>
1.325 if is_type_enc_higher_order type_enc then
1.326 - AAbs (((name, ho_type_from_typ type_enc true 0 T),
1.327 + AAbs (((name, ho_type_from_typ type_enc true (* FIXME? why "true"? *) 0 T),
1.328 term Elsewhere tm), map (term Elsewhere) args)
1.329 else
1.330 raise Fail "unexpected lambda-abstraction"
1.331 @@ -2063,7 +2065,10 @@
1.332 in SOME (AAtom (ATerm ((`I tptp_equal, []), [tagged_var, var]))) end
1.333 else
1.334 NONE
1.335 - fun do_formula pos (AQuant (q, xs, phi)) =
1.336 + fun do_formula pos (ATyQuant (q, xs, phi)) =
1.337 + ATyQuant (q, map (ho_type_from_typ type_enc false 0) xs,
1.338 + do_formula pos phi)
1.339 + | do_formula pos (AQuant (q, xs, phi)) =
1.340 let
1.341 val phi = phi |> do_formula pos
1.342 val universal = Option.map (q = AExists ? not) pos
1.343 @@ -2108,29 +2113,25 @@
1.344
1.345 fun formula_line_for_class_rel_clause type_enc
1.346 ({name, subclass, superclass, ...} : class_rel_clause) =
1.347 - let val ty_arg = ATerm ((tvar_a_name, []), []) in
1.348 - Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
1.349 - AConn (AImplies,
1.350 - [type_class_formula type_enc subclass ty_arg,
1.351 - type_class_formula type_enc superclass ty_arg])
1.352 - |> mk_aquant AForall
1.353 - [(tvar_a_name, atype_of_type_vars type_enc)],
1.354 + Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
1.355 + AConn (AImplies,
1.356 + [type_class_atom type_enc (subclass, tvar_a),
1.357 + type_class_atom type_enc (superclass, tvar_a)])
1.358 + |> bound_tvars type_enc false [tvar_a],
1.359 + NONE, isabelle_info inductiveN helper_rank)
1.360 +
1.361 +fun formula_line_for_arity_clause type_enc
1.362 + ({name, prems, concl} : arity_clause) =
1.363 + let
1.364 + val atomic_Ts = fold (fold_atyps (insert (op =)) o snd) (concl :: prems) []
1.365 + in
1.366 + Formula (arity_clause_prefix ^ name, Axiom,
1.367 + mk_ahorn (map (type_class_atom type_enc) prems)
1.368 + (type_class_atom type_enc concl)
1.369 + |> bound_tvars type_enc true atomic_Ts,
1.370 NONE, isabelle_info inductiveN helper_rank)
1.371 end
1.372
1.373 -fun formula_from_arity_atom type_enc (class, t, args) =
1.374 - ATerm ((t, []), map (fn arg => ATerm ((arg, []), [])) args)
1.375 - |> type_class_formula type_enc class
1.376 -
1.377 -fun formula_line_for_arity_clause type_enc
1.378 - ({name, prem_atoms, concl_atom} : arity_clause) =
1.379 - Formula (arity_clause_prefix ^ name, Axiom,
1.380 - mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
1.381 - (formula_from_arity_atom type_enc concl_atom)
1.382 - |> mk_aquant AForall
1.383 - (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
1.384 - NONE, isabelle_info inductiveN helper_rank)
1.385 -
1.386 fun formula_line_for_conjecture ctxt mono type_enc
1.387 ({name, role, iformula, atomic_types, ...} : ifact) =
1.388 Formula (conjecture_prefix ^ name, role,
1.389 @@ -2140,21 +2141,14 @@
1.390 |> close_formula_universally
1.391 |> bound_tvars type_enc true atomic_types, NONE, [])
1.392
1.393 -fun type_enc_needs_free_types (Native (_, Raw_Polymorphic _, _)) = true
1.394 - | type_enc_needs_free_types (Native _) = false
1.395 - | type_enc_needs_free_types _ = true
1.396 -
1.397 -fun formula_line_for_free_type j phi =
1.398 - Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
1.399 fun formula_lines_for_free_types type_enc (facts : ifact list) =
1.400 - if type_enc_needs_free_types type_enc then
1.401 - let
1.402 - val phis =
1.403 - fold (union (op =)) (map #atomic_types facts) []
1.404 - |> formulas_for_types type_enc add_sorts_on_tfree
1.405 - in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
1.406 - else
1.407 - []
1.408 + let
1.409 + fun line j phi =
1.410 + Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
1.411 + val phis =
1.412 + fold (union (op =)) (map #atomic_types facts) []
1.413 + |> formulas_for_types type_enc add_sorts_on_tfree
1.414 + in map2 line (0 upto length phis - 1) phis end
1.415
1.416 (** Symbol declarations **)
1.417
1.418 @@ -2162,11 +2156,11 @@
1.419 let val name as (s, _) = `make_type_class s in
1.420 Decl (sym_decl_prefix ^ s, name,
1.421 if order = First_Order then
1.422 - ATyAbs ([tvar_a_name],
1.423 - if phantoms = Without_Phantom_Type_Vars then
1.424 - AFun (a_itself_atype, bool_atype)
1.425 - else
1.426 - bool_atype)
1.427 + APi ([tvar_a_name],
1.428 + if phantoms = Without_Phantom_Type_Vars then
1.429 + AFun (a_itself_atype, bool_atype)
1.430 + else
1.431 + bool_atype)
1.432 else
1.433 AFun (atype_of_types, bool_atype))
1.434 end
1.435 @@ -2207,7 +2201,8 @@
1.436 #> fold add_iterm_syms args
1.437 end
1.438 val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> ifact_lift
1.439 - fun add_formula_var_types (AQuant (_, xs, phi)) =
1.440 + fun add_formula_var_types (ATyQuant (_, _, phi)) = add_formula_var_types phi
1.441 + | add_formula_var_types (AQuant (_, xs, phi)) =
1.442 fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
1.443 #> add_formula_var_types phi
1.444 | add_formula_var_types (AConn (_, phis)) =
1.445 @@ -2359,7 +2354,7 @@
1.446 T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
1.447 |> ho_type_from_typ type_enc pred_sym ary
1.448 |> not (null T_args)
1.449 - ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
1.450 + ? curry APi (map (tvar_name o fst o dest_TVar) T_args))
1.451 end
1.452
1.453 fun honor_conj_sym_role in_conj =
1.454 @@ -2574,8 +2569,9 @@
1.455 else
1.456 individual_atype
1.457 | _ => individual_atype
1.458 - fun typ 0 = if pred_sym then bool_atype else ind
1.459 - | typ ary = AFun (ind, typ (ary - 1))
1.460 + fun typ 0 0 = if pred_sym then bool_atype else ind
1.461 + | typ 0 tm_ary = AFun (ind, typ 0 (tm_ary - 1))
1.462 + | typ ty_ary tm_ary = APi (replicate ty_ary tvar_a_name, typ 0 tm_ary)
1.463 in typ end
1.464
1.465 fun nary_type_constr_type n =
1.466 @@ -2592,13 +2588,15 @@
1.467 do_sym name (fn () => nary_type_constr_type (length tys))
1.468 #> fold do_type tys
1.469 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
1.470 - | do_type (ATyAbs (_, ty)) = do_type ty
1.471 + | do_type (APi (_, ty)) = do_type ty
1.472 fun do_term pred_sym (ATerm ((name as (s, _), tys), tms)) =
1.473 - do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
1.474 + do_sym name
1.475 + (fn _ => default_type type_enc pred_sym s (length tys) (length tms))
1.476 #> fold do_type tys #> fold (do_term false) tms
1.477 | do_term _ (AAbs (((_, ty), tm), args)) =
1.478 do_type ty #> do_term false tm #> fold (do_term false) args
1.479 - fun do_formula (AQuant (_, xs, phi)) =
1.480 + fun do_formula (ATyQuant (_, _, phi)) = do_formula phi
1.481 + | do_formula (AQuant (_, xs, phi)) =
1.482 fold do_type (map_filter snd xs) #> do_formula phi
1.483 | do_formula (AConn (_, phis)) = fold do_formula phis
1.484 | do_formula (AAtom tm) = do_term true tm
1.485 @@ -2794,16 +2792,19 @@
1.486 else (s, tms)
1.487 | make_head_roll _ = ("", [])
1.488
1.489 -fun strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi
1.490 +fun strip_up_to_predicator (ATyQuant (_, _, phi)) = strip_up_to_predicator phi
1.491 + | strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi
1.492 | strip_up_to_predicator (AConn (_, phis)) = maps strip_up_to_predicator phis
1.493 | strip_up_to_predicator (AAtom tm) = [strip_predicator tm]
1.494
1.495 -fun strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi
1.496 +fun strip_ahorn_etc (ATyQuant (_, _, phi)) = strip_ahorn_etc phi
1.497 + | strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi
1.498 | strip_ahorn_etc (AConn (AImplies, [phi1, phi2])) =
1.499 strip_ahorn_etc phi2 |>> append (strip_up_to_predicator phi1)
1.500 | strip_ahorn_etc phi = ([], hd (strip_up_to_predicator phi))
1.501
1.502 -fun strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi
1.503 +fun strip_iff_etc (ATyQuant (_, _, phi)) = strip_iff_etc phi
1.504 + | strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi
1.505 | strip_iff_etc (AConn (AIff, [phi1, phi2])) =
1.506 pairself strip_up_to_predicator (phi1, phi2)
1.507 | strip_iff_etc _ = ([], [])