1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
1.3 @@ -13,6 +13,7 @@
1.4 datatype quantifier = AForall | AExists
1.5 datatype connective = ANot | AAnd | AOr | AImplies | AIff
1.6 datatype ('a, 'b, 'c) formula =
1.7 + ATyQuant of quantifier * 'b list * ('a, 'b, 'c) formula |
1.8 AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
1.9 AConn of connective * ('a, 'b, 'c) formula list |
1.10 AAtom of 'c
1.11 @@ -20,7 +21,7 @@
1.12 datatype 'a ho_type =
1.13 AType of 'a * 'a ho_type list |
1.14 AFun of 'a ho_type * 'a ho_type |
1.15 - ATyAbs of 'a list * 'a ho_type
1.16 + APi of 'a list * 'a ho_type
1.17
1.18 type term_order =
1.19 {is_lpo : bool,
1.20 @@ -145,6 +146,7 @@
1.21 datatype quantifier = AForall | AExists
1.22 datatype connective = ANot | AAnd | AOr | AImplies | AIff
1.23 datatype ('a, 'b, 'c) formula =
1.24 + ATyQuant of quantifier * 'b list * ('a, 'b, 'c) formula |
1.25 AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
1.26 AConn of connective * ('a, 'b, 'c) formula list |
1.27 AAtom of 'c
1.28 @@ -152,7 +154,7 @@
1.29 datatype 'a ho_type =
1.30 AType of 'a * 'a ho_type list |
1.31 AFun of 'a ho_type * 'a ho_type |
1.32 - ATyAbs of 'a list * 'a ho_type
1.33 + APi of 'a list * 'a ho_type
1.34
1.35 type term_order =
1.36 {is_lpo : bool,
1.37 @@ -284,23 +286,27 @@
1.38 fun formula_fold pos f =
1.39 let
1.40 fun fld pos (AQuant (_, _, phi)) = fld pos phi
1.41 + | fld pos (ATyQuant (_, _, phi)) = fld pos phi
1.42 | fld pos (AConn conn) = aconn_fold pos fld conn
1.43 | fld pos (AAtom tm) = f pos tm
1.44 in fld pos end
1.45
1.46 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
1.47 + | formula_map f (ATyQuant (q, xs, phi)) = ATyQuant (q, xs, formula_map f phi)
1.48 | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
1.49 | formula_map f (AAtom tm) = AAtom (f tm)
1.50
1.51 -fun is_function_type (AFun (_, ty)) = is_function_type ty
1.52 +fun is_function_type (APi (_, ty)) = is_function_type ty
1.53 + | is_function_type (AFun (_, ty)) = is_function_type ty
1.54 | is_function_type (AType (s, _)) =
1.55 s <> tptp_type_of_types andalso s <> tptp_bool_type
1.56 | is_function_type _ = false
1.57 -fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty
1.58 +fun is_predicate_type (APi (_, ty)) = is_predicate_type ty
1.59 + | is_predicate_type (AFun (_, ty)) = is_predicate_type ty
1.60 | is_predicate_type (AType (s, _)) = (s = tptp_bool_type)
1.61 | is_predicate_type _ = false
1.62 -fun is_nontrivial_predicate_type (AFun (_, ty)) = is_predicate_type ty
1.63 - | is_nontrivial_predicate_type _ = false
1.64 +fun is_nontrivial_predicate_type (AType _) = false
1.65 + | is_nontrivial_predicate_type ty = is_predicate_type ty
1.66
1.67 fun is_format_higher_order (THF _) = true
1.68 | is_format_higher_order _ = false
1.69 @@ -315,13 +321,14 @@
1.70 | tptp_string_for_role Hypothesis = "hypothesis"
1.71 | tptp_string_for_role Conjecture = "conjecture"
1.72
1.73 -fun tptp_string_for_app format func args =
1.74 - if is_format_higher_order format then
1.75 - "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
1.76 - else
1.77 - func ^ "(" ^ commas args ^ ")"
1.78 +fun tptp_string_for_app _ func [] = func
1.79 + | tptp_string_for_app format func args =
1.80 + if is_format_higher_order format then
1.81 + "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
1.82 + else
1.83 + func ^ "(" ^ commas args ^ ")"
1.84
1.85 -fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty)
1.86 +fun flatten_type (APi (tys, ty)) = APi (tys, flatten_type ty)
1.87 | flatten_type (ty as AFun (ty1 as AType _, ty2)) =
1.88 (case flatten_type ty2 of
1.89 AFun (ty' as AType (s, tys), ty) =>
1.90 @@ -334,6 +341,9 @@
1.91
1.92 val dfg_individual_type = "iii" (* cannot clash *)
1.93
1.94 +val suffix_type_of_types =
1.95 + suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)
1.96 +
1.97 fun str_for_type format ty =
1.98 let
1.99 val dfg = case format of DFG _ => true | _ => false
1.100 @@ -352,10 +362,12 @@
1.101 (str false ty1 |> dfg ? enclose "(" ")") ^ " " ^
1.102 (if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2
1.103 |> not rhs ? enclose "(" ")"
1.104 - | str _ (ATyAbs (ss, ty)) =
1.105 - tptp_pi_binder ^ "[" ^
1.106 - commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))
1.107 - ss) ^ "]: " ^ str false ty
1.108 + | str _ (APi (ss, ty)) =
1.109 + if dfg then
1.110 + "[" ^ commas ss ^ "], " ^ str true ty
1.111 + else
1.112 + tptp_pi_binder ^ "[" ^ commas (map suffix_type_of_types ss) ^ "]: " ^
1.113 + str false ty
1.114 in str true ty end
1.115
1.116 fun string_for_type (format as THF _) ty = str_for_type format ty
1.117 @@ -380,8 +392,7 @@
1.118 "")
1.119
1.120 fun tptp_string_for_term _ (ATerm ((s, []), [])) = s
1.121 - | tptp_string_for_term _ (ATerm ((s, tys), [])) = s (* ### FIXME *)
1.122 - | tptp_string_for_term format (ATerm ((s, tys), ts)) = (* ### FIXME *)
1.123 + | tptp_string_for_term format (ATerm ((s, tys), ts)) =
1.124 (if s = tptp_empty_list then
1.125 (* used for lists in the optional "source" field of a derivation *)
1.126 "[" ^ commas (map (tptp_string_for_term format) ts) ^ "]"
1.127 @@ -405,7 +416,10 @@
1.128 tptp_string_for_term format tm ^ ""
1.129 |> enclose "(" ")")
1.130 (map (tptp_string_for_term format) args)
1.131 - | _ => tptp_string_for_app format s (map (tptp_string_for_term format) ts))
1.132 + | _ =>
1.133 + tptp_string_for_app format s
1.134 + (map (string_for_type format) tys
1.135 + @ map (tptp_string_for_term format) ts))
1.136 | tptp_string_for_term (format as THF _) (AAbs (((s, ty), tm), args)) =
1.137 tptp_string_for_app format
1.138 ("(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
1.139 @@ -413,7 +427,12 @@
1.140 (map (tptp_string_for_term format) args)
1.141 | tptp_string_for_term _ _ =
1.142 raise Fail "unexpected term in first-order format"
1.143 -and tptp_string_for_formula format (AQuant (q, xs, phi)) =
1.144 +and tptp_string_for_formula format (ATyQuant (q, xs, phi)) =
1.145 + tptp_string_for_quantifier q ^
1.146 + "[" ^ commas (map (suffix_type_of_types o string_for_type format) xs) ^
1.147 + "]: " ^ tptp_string_for_formula format phi
1.148 + |> enclose "(" ")"
1.149 + | tptp_string_for_formula format (AQuant (q, xs, phi)) =
1.150 tptp_string_for_quantifier q ^
1.151 "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^
1.152 tptp_string_for_formula format phi
1.153 @@ -459,14 +478,21 @@
1.154 "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
1.155 map (tptp_string_for_problem_line format) lines)
1.156
1.157 -fun arity_of_type (AFun (_, ty)) = 1 + arity_of_type ty
1.158 - | arity_of_type _ = 0
1.159 +fun arity_of_type (APi (tys, ty)) =
1.160 + arity_of_type ty |>> Integer.add (length tys)
1.161 + | arity_of_type (AFun (_, ty)) = arity_of_type ty ||> Integer.add 1
1.162 + | arity_of_type _ = (0, 0)
1.163
1.164 -fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2
1.165 - | binder_atypes _ = []
1.166 +fun string_of_arity (0, n) = string_of_int n
1.167 + | string_of_arity (m, n) = string_of_int m ^ "+" ^ string_of_int n
1.168 +
1.169 +fun strip_atype (APi (tys, ty)) = strip_atype ty |>> apfst (append tys)
1.170 + | strip_atype (AFun (ty1, ty2)) = strip_atype ty2 |>> apsnd (cons ty1)
1.171 + | strip_atype ty = (([], []), ty)
1.172
1.173 fun dfg_string_for_formula poly gen_simp info =
1.174 let
1.175 + val str_for_typ = string_for_type (DFG poly)
1.176 fun suffix_tag top_level s =
1.177 if top_level then
1.178 case extract_isabelle_status info of
1.179 @@ -481,7 +507,8 @@
1.180 else if s = tptp_true then "true"
1.181 else if s = tptp_false then "false"
1.182 else s) ^
1.183 - (if null tys then "" else "<...>") (* ### FIXME *) ^
1.184 + (if null tys then ""
1.185 + else "<" ^ commas (map (string_for_type (DFG poly)) tys) ^ ">") ^
1.186 (if null tms then ""
1.187 else "(" ^ commas (map (str_for_term false) tms) ^ ")")
1.188 | str_for_term _ _ = raise Fail "unexpected term in first-order format"
1.189 @@ -492,8 +519,11 @@
1.190 | str_for_conn _ AOr = "or"
1.191 | str_for_conn _ AImplies = "implies"
1.192 | str_for_conn top_level AIff = "equiv" |> suffix_tag top_level
1.193 - fun str_for_formula top_level (AQuant (q, xs, phi)) =
1.194 - str_for_quant q ^ "(" ^ "[" ^
1.195 + fun str_for_formula top_level (ATyQuant (q, xs, phi)) =
1.196 + str_for_quant q ^ "_sorts([" ^ commas (map str_for_typ xs) ^
1.197 + "], " ^ str_for_formula top_level phi ^ ")"
1.198 + | str_for_formula top_level (AQuant (q, xs, phi)) =
1.199 + str_for_quant q ^ "([" ^
1.200 commas (map (string_for_bound_var (DFG poly)) xs) ^ "], " ^
1.201 str_for_formula top_level phi ^ ")"
1.202 | str_for_formula top_level (AConn (c, phis)) =
1.203 @@ -507,13 +537,19 @@
1.204
1.205 fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
1.206 let
1.207 - fun spair (sym, k) = "(" ^ sym ^ ", " ^ string_of_int k ^ ")"
1.208 - fun ary sym = curry spair sym o arity_of_type
1.209 - fun fun_typ sym ty =
1.210 - "function(" ^ sym ^ ", " ^ string_for_type (DFG poly) ty ^ ")."
1.211 + val str_for_typ = string_for_type (DFG poly)
1.212 + fun spair (s, s') = "(" ^ s ^ ", " ^ s' ^ ")"
1.213 + fun tm_ary sym ty = spair (sym, string_of_arity (arity_of_type ty))
1.214 + fun ty_ary [] sym = sym
1.215 + | ty_ary tys sym = "(" ^ sym ^ ", " ^ string_of_int (length tys) ^ ")"
1.216 + fun fun_typ sym ty = "function(" ^ sym ^ ", " ^ str_for_typ ty ^ ")."
1.217 fun pred_typ sym ty =
1.218 - "predicate(" ^
1.219 - commas (sym :: map (string_for_type (DFG poly)) (binder_atypes ty)) ^ ")."
1.220 + let
1.221 + val ((ty_vars, tys), _) = strip_atype ty
1.222 + val (ty_vars, tys) =
1.223 + strip_atype ty |> fst
1.224 + |>> (fn [] => [] | ty_vars => ["[" ^ commas ty_vars ^ "]"])
1.225 + in "predicate(" ^ commas (sym :: ty_vars @ map str_for_typ tys) ^ ")." end
1.226 fun formula pred (Formula (ident, kind, phi, _, info)) =
1.227 if pred kind then
1.228 let val rank = extract_isabelle_rank info in
1.229 @@ -528,23 +564,27 @@
1.230 fun filt f = problem |> map (map_filter f o snd) |> filter_out null
1.231 val func_aries =
1.232 filt (fn Decl (_, sym, ty) =>
1.233 - if is_function_type ty then SOME (ary sym ty) else NONE
1.234 + if is_function_type ty then SOME (tm_ary sym ty) else NONE
1.235 | _ => NONE)
1.236 |> flat |> commas |> maybe_enclose "functions [" "]."
1.237 val pred_aries =
1.238 filt (fn Decl (_, sym, ty) =>
1.239 - if is_predicate_type ty then SOME (ary sym ty) else NONE
1.240 + if is_predicate_type ty then SOME (tm_ary sym ty) else NONE
1.241 | _ => NONE)
1.242 |> flat |> commas |> maybe_enclose "predicates [" "]."
1.243 val sorts =
1.244 - filt (fn Decl (_, sym, AType (s, [])) =>
1.245 - if s = tptp_type_of_types then SOME sym else NONE
1.246 + filt (fn Decl (_, sym, ty) =>
1.247 + (case strip_atype ty of
1.248 + (([], tys), AType (s, [])) =>
1.249 + if s = tptp_type_of_types then SOME (ty_ary tys sym) else NONE
1.250 + | _ => NONE)
1.251 | _ => NONE) @ [[dfg_individual_type]]
1.252 |> flat |> commas |> maybe_enclose "sorts [" "]."
1.253 val ord_info = if gen_weights orelse gen_prec then ord_info () else []
1.254 val do_term_order_weights =
1.255 (if gen_weights then ord_info else [])
1.256 - |> map spair |> commas |> maybe_enclose "weights [" "]."
1.257 + |> map (spair o apsnd string_of_int) |> commas
1.258 + |> maybe_enclose "weights [" "]."
1.259 val syms = [func_aries, pred_aries, do_term_order_weights, sorts]
1.260 val func_sigs =
1.261 filt (fn Decl (_, sym, ty) =>
1.262 @@ -798,15 +838,18 @@
1.263 fun nice_type (AType (name, tys)) =
1.264 nice_name name ##>> pool_map nice_type tys #>> AType
1.265 | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
1.266 - | nice_type (ATyAbs (names, ty)) =
1.267 - pool_map nice_name names ##>> nice_type ty #>> ATyAbs
1.268 + | nice_type (APi (names, ty)) =
1.269 + pool_map nice_name names ##>> nice_type ty #>> APi
1.270 fun nice_term (ATerm ((name, tys), ts)) =
1.271 nice_name name ##>> pool_map nice_type tys ##>> pool_map nice_term ts
1.272 #>> ATerm
1.273 | nice_term (AAbs (((name, ty), tm), args)) =
1.274 nice_name name ##>> nice_type ty ##>> nice_term tm
1.275 ##>> pool_map nice_term args #>> AAbs
1.276 - fun nice_formula (AQuant (q, xs, phi)) =
1.277 + fun nice_formula (ATyQuant (q, xs, phi)) =
1.278 + pool_map nice_type xs ##>> nice_formula phi
1.279 + #>> (fn (xs, phi) => ATyQuant (q, xs, phi))
1.280 + | nice_formula (AQuant (q, xs, phi)) =
1.281 pool_map nice_name (map fst xs)
1.282 ##>> pool_map (fn NONE => pair NONE
1.283 | SOME ty => nice_type ty #>> SOME) (map snd xs)
2.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
2.3 @@ -359,9 +359,9 @@
2.4 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
2.5 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
2.6
2.7 -fun make_schematic_type_var (x, i) =
2.8 - tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
2.9 -fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
2.10 +fun make_tvar (s, i) = tvar_prefix ^ (ascii_of_indexname (unprefix "'" s, i))
2.11 +fun make_tfree s = tfree_prefix ^ (ascii_of (unprefix "'" s))
2.12 +fun tvar_name (x as (s, _)) = (make_tvar x, s)
2.13
2.14 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
2.15 local
2.16 @@ -407,32 +407,36 @@
2.17 | _ => I)
2.18 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
2.19
2.20 +val tvar_a_str = "'a"
2.21 +val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
2.22 +val tvar_a_name = tvar_name (tvar_a_str, 0)
2.23 +val itself_name = `make_fixed_type_const @{type_name itself}
2.24 +val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
2.25 +val tvar_a_atype = AType (tvar_a_name, [])
2.26 +val a_itself_atype = AType (itself_name, [tvar_a_atype])
2.27 +
2.28 (** Definitions and functions for FOL clauses and formulas for TPTP **)
2.29
2.30 (** Isabelle arities **)
2.31
2.32 -type arity_atom = name * name * name list
2.33 -
2.34 val type_class = the_single @{sort type}
2.35
2.36 type arity_clause =
2.37 {name : string,
2.38 - prem_atoms : arity_atom list,
2.39 - concl_atom : arity_atom}
2.40 + prems : (string * typ) list,
2.41 + concl : string * typ}
2.42
2.43 -fun add_prem_atom tvar =
2.44 - fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
2.45 +fun add_prem_atom T = fold (fn s => s <> type_class ? cons (s, T))
2.46
2.47 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
2.48 -fun make_axiom_arity_clause (tcons, name, (cls, args)) =
2.49 +fun make_axiom_arity_clause (tc, name, (class, args)) =
2.50 let
2.51 - val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
2.52 - val tvars_srts = ListPair.zip (tvars, args)
2.53 + val tvars =
2.54 + map (fn j => TVar ((tvar_a_str, j), @{sort HOL.type}))
2.55 + (1 upto length args)
2.56 in
2.57 - {name = name,
2.58 - prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
2.59 - concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
2.60 - tvars ~~ tvars)}
2.61 + {name = name, prems = fold (uncurry add_prem_atom) (tvars ~~ args) [],
2.62 + concl = (class, Type (tc, tvars))}
2.63 end
2.64
2.65 fun arity_clause _ _ (_, []) = []
2.66 @@ -487,8 +491,8 @@
2.67
2.68 type class_rel_clause =
2.69 {name : string,
2.70 - subclass : name,
2.71 - superclass : name}
2.72 + subclass : string,
2.73 + superclass : string}
2.74
2.75 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
2.76 in theory "thy". *)
2.77 @@ -501,8 +505,7 @@
2.78 in fold add_supers subs [] end
2.79
2.80 fun make_class_rel_clause (sub, super) =
2.81 - {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
2.82 - superclass = `make_type_class super}
2.83 + {name = sub ^ "_" ^ super, subclass = sub, superclass = super}
2.84
2.85 fun make_class_rel_clauses thy subs supers =
2.86 map make_class_rel_clause (class_pairs thy subs supers)
2.87 @@ -528,14 +531,6 @@
2.88
2.89 fun atomic_types_of T = fold_atyps (insert (op =)) T []
2.90
2.91 -val tvar_a_str = "'a"
2.92 -val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
2.93 -val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
2.94 -val itself_name = `make_fixed_type_const @{type_name itself}
2.95 -val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
2.96 -val tvar_a_atype = AType (tvar_a_name, [])
2.97 -val a_itself_atype = AType (itself_name, [tvar_a_atype])
2.98 -
2.99 fun new_skolem_const_name s num_T_args =
2.100 [new_skolem_const_prefix, s, string_of_int num_T_args]
2.101 |> Long_Name.implode
2.102 @@ -872,79 +867,9 @@
2.103 end
2.104 end
2.105
2.106 -(* Make atoms for sorted type variables. *)
2.107 -fun generic_add_sorts_on_type (_, []) = I
2.108 - | generic_add_sorts_on_type ((x, i), s :: ss) =
2.109 - generic_add_sorts_on_type ((x, i), ss)
2.110 - #> (if s = the_single @{sort HOL.type} then
2.111 - I
2.112 - else if i = ~1 then
2.113 - insert (op =) (`make_type_class s, `make_fixed_type_var x)
2.114 - else
2.115 - insert (op =) (`make_type_class s,
2.116 - (make_schematic_type_var (x, i), x)))
2.117 -fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
2.118 - | add_sorts_on_tfree _ = I
2.119 -fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
2.120 - | add_sorts_on_tvar _ = I
2.121 -
2.122 -fun type_class_formula type_enc class arg =
2.123 - AAtom (ATerm ((class, []), arg ::
2.124 - (case type_enc of
2.125 - Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
2.126 - [ATerm ((TYPE_name, []), [arg])]
2.127 - | _ => [])))
2.128 -fun formulas_for_types type_enc add_sorts_on_typ Ts =
2.129 - [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
2.130 - |> map (fn (class, name) =>
2.131 - type_class_formula type_enc class (ATerm ((name, []), [])))
2.132 -
2.133 -fun mk_aconns c phis =
2.134 - let val (phis', phi') = split_last phis in
2.135 - fold_rev (mk_aconn c) phis' phi'
2.136 - end
2.137 -fun mk_ahorn [] phi = phi
2.138 - | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
2.139 -fun mk_aquant _ [] phi = phi
2.140 - | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
2.141 - if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
2.142 - | mk_aquant q xs phi = AQuant (q, xs, phi)
2.143 -
2.144 -fun close_universally add_term_vars phi =
2.145 - let
2.146 - fun add_formula_vars bounds (AQuant (_, xs, phi)) =
2.147 - add_formula_vars (map fst xs @ bounds) phi
2.148 - | add_formula_vars bounds (AConn (_, phis)) =
2.149 - fold (add_formula_vars bounds) phis
2.150 - | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
2.151 - in mk_aquant AForall (add_formula_vars [] phi []) phi end
2.152 -
2.153 -fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
2.154 - (if is_tptp_variable s andalso
2.155 - not (String.isPrefix tvar_prefix s) andalso
2.156 - not (member (op =) bounds name) then
2.157 - insert (op =) (name, NONE)
2.158 - else
2.159 - I)
2.160 - #> fold (add_term_vars bounds) tms
2.161 - | add_term_vars bounds (AAbs (((name, _), tm), args)) =
2.162 - add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
2.163 -fun close_formula_universally phi = close_universally add_term_vars phi
2.164 -
2.165 -fun add_iterm_vars bounds (IApp (tm1, tm2)) =
2.166 - fold (add_iterm_vars bounds) [tm1, tm2]
2.167 - | add_iterm_vars _ (IConst _) = I
2.168 - | add_iterm_vars bounds (IVar (name, T)) =
2.169 - not (member (op =) bounds name) ? insert (op =) (name, SOME T)
2.170 - | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
2.171 -
2.172 -fun close_iformula_universally phi = close_universally add_iterm_vars phi
2.173 -
2.174 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
2.175 val fused_infinite_type = Type (fused_infinite_type_name, [])
2.176
2.177 -fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
2.178 -
2.179 fun ho_term_from_typ type_enc =
2.180 let
2.181 fun term (Type (s, Ts)) =
2.182 @@ -957,7 +882,7 @@
2.183 else
2.184 `make_fixed_type_const s,
2.185 []), map term Ts)
2.186 - | term (TFree (s, _)) = ATerm ((`make_fixed_type_var s, []), [])
2.187 + | term (TFree (s, _)) = ATerm ((`make_tfree s, []), [])
2.188 | term (TVar (x, _)) = ATerm ((tvar_name x, []), [])
2.189 in term end
2.190
2.191 @@ -1011,6 +936,87 @@
2.192 ho_type_from_ho_term type_enc pred_sym ary
2.193 o ho_term_from_typ type_enc
2.194
2.195 +(* Make atoms for sorted type variables. *)
2.196 +fun generic_add_sorts_on_type _ [] = I
2.197 + | generic_add_sorts_on_type T (s :: ss) =
2.198 + generic_add_sorts_on_type T ss
2.199 + #> (if s = the_single @{sort HOL.type} then I else insert (op =) (s, T))
2.200 +fun add_sorts_on_tfree (T as TFree (_, S)) = generic_add_sorts_on_type T S
2.201 + | add_sorts_on_tfree _ = I
2.202 +fun add_sorts_on_tvar (T as TVar (_, S)) = generic_add_sorts_on_type T S
2.203 + | add_sorts_on_tvar _ = I
2.204 +
2.205 +fun process_type_args type_enc T_args =
2.206 + if is_type_enc_native type_enc then
2.207 + (map (ho_type_from_typ type_enc false 0) T_args, [])
2.208 + else
2.209 + ([], map_filter (ho_term_for_type_arg type_enc) T_args)
2.210 +
2.211 +fun type_class_atom type_enc (class, T) =
2.212 + let
2.213 + val class = `make_type_class class
2.214 + val (ty_args, tm_args) = process_type_args type_enc [T]
2.215 + val tm_args =
2.216 + tm_args @
2.217 + (case type_enc of
2.218 + Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
2.219 + [ATerm ((TYPE_name, ty_args), [])]
2.220 + | _ => [])
2.221 + in AAtom (ATerm ((class, ty_args), tm_args)) end
2.222 +fun formulas_for_types type_enc add_sorts_on_typ Ts =
2.223 + [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
2.224 + |> map (type_class_atom type_enc)
2.225 +
2.226 +fun mk_aconns c phis =
2.227 + let val (phis', phi') = split_last phis in
2.228 + fold_rev (mk_aconn c) phis' phi'
2.229 + end
2.230 +
2.231 +fun mk_ahorn [] phi = phi
2.232 + | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
2.233 +
2.234 +fun mk_aquant _ [] phi = phi
2.235 + | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
2.236 + if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
2.237 + | mk_aquant q xs phi = AQuant (q, xs, phi)
2.238 +
2.239 +fun mk_atyquant _ [] phi = phi
2.240 + | mk_atyquant q xs (phi as ATyQuant (q', xs', phi')) =
2.241 + if q = q' then ATyQuant (q, xs @ xs', phi') else ATyQuant (q, xs, phi)
2.242 + | mk_atyquant q xs phi = ATyQuant (q, xs, phi)
2.243 +
2.244 +fun close_universally add_term_vars phi =
2.245 + let
2.246 + fun add_formula_vars bounds (ATyQuant (_, _, phi)) =
2.247 + add_formula_vars bounds phi
2.248 + | add_formula_vars bounds (AQuant (_, xs, phi)) =
2.249 + add_formula_vars (map fst xs @ bounds) phi
2.250 + | add_formula_vars bounds (AConn (_, phis)) =
2.251 + fold (add_formula_vars bounds) phis
2.252 + | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
2.253 + in mk_aquant AForall (add_formula_vars [] phi []) phi end
2.254 +
2.255 +fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
2.256 + (if is_tptp_variable s andalso
2.257 + not (String.isPrefix tvar_prefix s) andalso
2.258 + not (member (op =) bounds name) then
2.259 + insert (op =) (name, NONE)
2.260 + else
2.261 + I)
2.262 + #> fold (add_term_vars bounds) tms
2.263 + | add_term_vars bounds (AAbs (((name, _), tm), args)) =
2.264 + add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
2.265 +fun close_formula_universally phi = close_universally add_term_vars phi
2.266 +
2.267 +fun add_iterm_vars bounds (IApp (tm1, tm2)) =
2.268 + fold (add_iterm_vars bounds) [tm1, tm2]
2.269 + | add_iterm_vars _ (IConst _) = I
2.270 + | add_iterm_vars bounds (IVar (name, T)) =
2.271 + not (member (op =) bounds name) ? insert (op =) (name, SOME T)
2.272 + | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
2.273 +
2.274 +fun close_iformula_universally phi = close_universally add_iterm_vars phi
2.275 +
2.276 fun aliased_uncurried ary (s, s') =
2.277 (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
2.278 fun unaliased_uncurried (s, s') =
2.279 @@ -1718,18 +1724,16 @@
2.280 @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
2.281 |> map (apsnd (map (apsnd zero_var_indexes)))
2.282
2.283 -fun atype_of_type_vars (Native (_, Raw_Polymorphic _, _)) = SOME atype_of_types
2.284 - | atype_of_type_vars (Native (_, Type_Class_Polymorphic, _)) =
2.285 - SOME atype_of_types (* ### FIXME *)
2.286 - | atype_of_type_vars _ = NONE
2.287 -
2.288 fun bound_tvars type_enc sorts Ts =
2.289 - (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
2.290 - #> mk_aquant AForall
2.291 - (map_filter (fn TVar (x as (s, _), _) =>
2.292 - SOME ((make_schematic_type_var x, s),
2.293 - atype_of_type_vars type_enc)
2.294 - | _ => NONE) Ts)
2.295 + case filter is_TVar Ts of
2.296 + [] => I
2.297 + | Ts =>
2.298 + (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
2.299 + #> (if is_type_enc_native type_enc then
2.300 + mk_atyquant AForall
2.301 + (map (fn TVar (x, _) => AType (tvar_name x, [])) Ts)
2.302 + else
2.303 + mk_aquant AForall (map (fn TVar (x, _) => (tvar_name x, NONE)) Ts))
2.304
2.305 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
2.306 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
2.307 @@ -1994,11 +1998,9 @@
2.308 | should_generate_tag_bound_decl _ _ _ _ _ = false
2.309
2.310 fun mk_aterm type_enc name T_args args =
2.311 -(* ### FIXME
2.312 - if is_type_enc_polymorphic type_enc then
2.313 - ATerm ((name, map (ho_type_from_typ type_enc false 0) T_args), args)
2.314 - else *)
2.315 - ATerm ((name, []), map_filter (ho_term_for_type_arg type_enc) T_args @ args)
2.316 + let val (ty_args, tm_args) = process_type_args type_enc T_args in
2.317 + ATerm ((name, ty_args), tm_args @ args)
2.318 + end
2.319
2.320 fun do_bound_type ctxt mono type_enc =
2.321 case type_enc of
2.322 @@ -2032,7 +2034,7 @@
2.323 map (term Elsewhere) args |> mk_aterm type_enc name []
2.324 | IAbs ((name, T), tm) =>
2.325 if is_type_enc_higher_order type_enc then
2.326 - AAbs (((name, ho_type_from_typ type_enc true 0 T),
2.327 + AAbs (((name, ho_type_from_typ type_enc true (* FIXME? why "true"? *) 0 T),
2.328 term Elsewhere tm), map (term Elsewhere) args)
2.329 else
2.330 raise Fail "unexpected lambda-abstraction"
2.331 @@ -2063,7 +2065,10 @@
2.332 in SOME (AAtom (ATerm ((`I tptp_equal, []), [tagged_var, var]))) end
2.333 else
2.334 NONE
2.335 - fun do_formula pos (AQuant (q, xs, phi)) =
2.336 + fun do_formula pos (ATyQuant (q, xs, phi)) =
2.337 + ATyQuant (q, map (ho_type_from_typ type_enc false 0) xs,
2.338 + do_formula pos phi)
2.339 + | do_formula pos (AQuant (q, xs, phi)) =
2.340 let
2.341 val phi = phi |> do_formula pos
2.342 val universal = Option.map (q = AExists ? not) pos
2.343 @@ -2108,29 +2113,25 @@
2.344
2.345 fun formula_line_for_class_rel_clause type_enc
2.346 ({name, subclass, superclass, ...} : class_rel_clause) =
2.347 - let val ty_arg = ATerm ((tvar_a_name, []), []) in
2.348 - Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
2.349 - AConn (AImplies,
2.350 - [type_class_formula type_enc subclass ty_arg,
2.351 - type_class_formula type_enc superclass ty_arg])
2.352 - |> mk_aquant AForall
2.353 - [(tvar_a_name, atype_of_type_vars type_enc)],
2.354 + Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
2.355 + AConn (AImplies,
2.356 + [type_class_atom type_enc (subclass, tvar_a),
2.357 + type_class_atom type_enc (superclass, tvar_a)])
2.358 + |> bound_tvars type_enc false [tvar_a],
2.359 + NONE, isabelle_info inductiveN helper_rank)
2.360 +
2.361 +fun formula_line_for_arity_clause type_enc
2.362 + ({name, prems, concl} : arity_clause) =
2.363 + let
2.364 + val atomic_Ts = fold (fold_atyps (insert (op =)) o snd) (concl :: prems) []
2.365 + in
2.366 + Formula (arity_clause_prefix ^ name, Axiom,
2.367 + mk_ahorn (map (type_class_atom type_enc) prems)
2.368 + (type_class_atom type_enc concl)
2.369 + |> bound_tvars type_enc true atomic_Ts,
2.370 NONE, isabelle_info inductiveN helper_rank)
2.371 end
2.372
2.373 -fun formula_from_arity_atom type_enc (class, t, args) =
2.374 - ATerm ((t, []), map (fn arg => ATerm ((arg, []), [])) args)
2.375 - |> type_class_formula type_enc class
2.376 -
2.377 -fun formula_line_for_arity_clause type_enc
2.378 - ({name, prem_atoms, concl_atom} : arity_clause) =
2.379 - Formula (arity_clause_prefix ^ name, Axiom,
2.380 - mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
2.381 - (formula_from_arity_atom type_enc concl_atom)
2.382 - |> mk_aquant AForall
2.383 - (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
2.384 - NONE, isabelle_info inductiveN helper_rank)
2.385 -
2.386 fun formula_line_for_conjecture ctxt mono type_enc
2.387 ({name, role, iformula, atomic_types, ...} : ifact) =
2.388 Formula (conjecture_prefix ^ name, role,
2.389 @@ -2140,21 +2141,14 @@
2.390 |> close_formula_universally
2.391 |> bound_tvars type_enc true atomic_types, NONE, [])
2.392
2.393 -fun type_enc_needs_free_types (Native (_, Raw_Polymorphic _, _)) = true
2.394 - | type_enc_needs_free_types (Native _) = false
2.395 - | type_enc_needs_free_types _ = true
2.396 -
2.397 -fun formula_line_for_free_type j phi =
2.398 - Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
2.399 fun formula_lines_for_free_types type_enc (facts : ifact list) =
2.400 - if type_enc_needs_free_types type_enc then
2.401 - let
2.402 - val phis =
2.403 - fold (union (op =)) (map #atomic_types facts) []
2.404 - |> formulas_for_types type_enc add_sorts_on_tfree
2.405 - in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
2.406 - else
2.407 - []
2.408 + let
2.409 + fun line j phi =
2.410 + Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
2.411 + val phis =
2.412 + fold (union (op =)) (map #atomic_types facts) []
2.413 + |> formulas_for_types type_enc add_sorts_on_tfree
2.414 + in map2 line (0 upto length phis - 1) phis end
2.415
2.416 (** Symbol declarations **)
2.417
2.418 @@ -2162,11 +2156,11 @@
2.419 let val name as (s, _) = `make_type_class s in
2.420 Decl (sym_decl_prefix ^ s, name,
2.421 if order = First_Order then
2.422 - ATyAbs ([tvar_a_name],
2.423 - if phantoms = Without_Phantom_Type_Vars then
2.424 - AFun (a_itself_atype, bool_atype)
2.425 - else
2.426 - bool_atype)
2.427 + APi ([tvar_a_name],
2.428 + if phantoms = Without_Phantom_Type_Vars then
2.429 + AFun (a_itself_atype, bool_atype)
2.430 + else
2.431 + bool_atype)
2.432 else
2.433 AFun (atype_of_types, bool_atype))
2.434 end
2.435 @@ -2207,7 +2201,8 @@
2.436 #> fold add_iterm_syms args
2.437 end
2.438 val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> ifact_lift
2.439 - fun add_formula_var_types (AQuant (_, xs, phi)) =
2.440 + fun add_formula_var_types (ATyQuant (_, _, phi)) = add_formula_var_types phi
2.441 + | add_formula_var_types (AQuant (_, xs, phi)) =
2.442 fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
2.443 #> add_formula_var_types phi
2.444 | add_formula_var_types (AConn (_, phis)) =
2.445 @@ -2359,7 +2354,7 @@
2.446 T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
2.447 |> ho_type_from_typ type_enc pred_sym ary
2.448 |> not (null T_args)
2.449 - ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
2.450 + ? curry APi (map (tvar_name o fst o dest_TVar) T_args))
2.451 end
2.452
2.453 fun honor_conj_sym_role in_conj =
2.454 @@ -2574,8 +2569,9 @@
2.455 else
2.456 individual_atype
2.457 | _ => individual_atype
2.458 - fun typ 0 = if pred_sym then bool_atype else ind
2.459 - | typ ary = AFun (ind, typ (ary - 1))
2.460 + fun typ 0 0 = if pred_sym then bool_atype else ind
2.461 + | typ 0 tm_ary = AFun (ind, typ 0 (tm_ary - 1))
2.462 + | typ ty_ary tm_ary = APi (replicate ty_ary tvar_a_name, typ 0 tm_ary)
2.463 in typ end
2.464
2.465 fun nary_type_constr_type n =
2.466 @@ -2592,13 +2588,15 @@
2.467 do_sym name (fn () => nary_type_constr_type (length tys))
2.468 #> fold do_type tys
2.469 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
2.470 - | do_type (ATyAbs (_, ty)) = do_type ty
2.471 + | do_type (APi (_, ty)) = do_type ty
2.472 fun do_term pred_sym (ATerm ((name as (s, _), tys), tms)) =
2.473 - do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
2.474 + do_sym name
2.475 + (fn _ => default_type type_enc pred_sym s (length tys) (length tms))
2.476 #> fold do_type tys #> fold (do_term false) tms
2.477 | do_term _ (AAbs (((_, ty), tm), args)) =
2.478 do_type ty #> do_term false tm #> fold (do_term false) args
2.479 - fun do_formula (AQuant (_, xs, phi)) =
2.480 + fun do_formula (ATyQuant (_, _, phi)) = do_formula phi
2.481 + | do_formula (AQuant (_, xs, phi)) =
2.482 fold do_type (map_filter snd xs) #> do_formula phi
2.483 | do_formula (AConn (_, phis)) = fold do_formula phis
2.484 | do_formula (AAtom tm) = do_term true tm
2.485 @@ -2794,16 +2792,19 @@
2.486 else (s, tms)
2.487 | make_head_roll _ = ("", [])
2.488
2.489 -fun strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi
2.490 +fun strip_up_to_predicator (ATyQuant (_, _, phi)) = strip_up_to_predicator phi
2.491 + | strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi
2.492 | strip_up_to_predicator (AConn (_, phis)) = maps strip_up_to_predicator phis
2.493 | strip_up_to_predicator (AAtom tm) = [strip_predicator tm]
2.494
2.495 -fun strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi
2.496 +fun strip_ahorn_etc (ATyQuant (_, _, phi)) = strip_ahorn_etc phi
2.497 + | strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi
2.498 | strip_ahorn_etc (AConn (AImplies, [phi1, phi2])) =
2.499 strip_ahorn_etc phi2 |>> append (strip_up_to_predicator phi1)
2.500 | strip_ahorn_etc phi = ([], hd (strip_up_to_predicator phi))
2.501
2.502 -fun strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi
2.503 +fun strip_iff_etc (ATyQuant (_, _, phi)) = strip_iff_etc phi
2.504 + | strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi
2.505 | strip_iff_etc (AConn (AIff, [phi1, phi2])) =
2.506 pairself strip_up_to_predicator (phi1, phi2)
2.507 | strip_iff_etc _ = ([], [])