--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
@@ -13,6 +13,7 @@
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIff
datatype ('a, 'b, 'c) formula =
+ ATyQuant of quantifier * 'b list * ('a, 'b, 'c) formula |
AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c
@@ -20,7 +21,7 @@
datatype 'a ho_type =
AType of 'a * 'a ho_type list |
AFun of 'a ho_type * 'a ho_type |
- ATyAbs of 'a list * 'a ho_type
+ APi of 'a list * 'a ho_type
type term_order =
{is_lpo : bool,
@@ -145,6 +146,7 @@
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIff
datatype ('a, 'b, 'c) formula =
+ ATyQuant of quantifier * 'b list * ('a, 'b, 'c) formula |
AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c
@@ -152,7 +154,7 @@
datatype 'a ho_type =
AType of 'a * 'a ho_type list |
AFun of 'a ho_type * 'a ho_type |
- ATyAbs of 'a list * 'a ho_type
+ APi of 'a list * 'a ho_type
type term_order =
{is_lpo : bool,
@@ -284,23 +286,27 @@
fun formula_fold pos f =
let
fun fld pos (AQuant (_, _, phi)) = fld pos phi
+ | fld pos (ATyQuant (_, _, phi)) = fld pos phi
| fld pos (AConn conn) = aconn_fold pos fld conn
| fld pos (AAtom tm) = f pos tm
in fld pos end
fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
+ | formula_map f (ATyQuant (q, xs, phi)) = ATyQuant (q, xs, formula_map f phi)
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
| formula_map f (AAtom tm) = AAtom (f tm)
-fun is_function_type (AFun (_, ty)) = is_function_type ty
+fun is_function_type (APi (_, ty)) = is_function_type ty
+ | is_function_type (AFun (_, ty)) = is_function_type ty
| is_function_type (AType (s, _)) =
s <> tptp_type_of_types andalso s <> tptp_bool_type
| is_function_type _ = false
-fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty
+fun is_predicate_type (APi (_, ty)) = is_predicate_type ty
+ | is_predicate_type (AFun (_, ty)) = is_predicate_type ty
| is_predicate_type (AType (s, _)) = (s = tptp_bool_type)
| is_predicate_type _ = false
-fun is_nontrivial_predicate_type (AFun (_, ty)) = is_predicate_type ty
- | is_nontrivial_predicate_type _ = false
+fun is_nontrivial_predicate_type (AType _) = false
+ | is_nontrivial_predicate_type ty = is_predicate_type ty
fun is_format_higher_order (THF _) = true
| is_format_higher_order _ = false
@@ -315,13 +321,14 @@
| tptp_string_for_role Hypothesis = "hypothesis"
| tptp_string_for_role Conjecture = "conjecture"
-fun tptp_string_for_app format func args =
- if is_format_higher_order format then
- "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
- else
- func ^ "(" ^ commas args ^ ")"
+fun tptp_string_for_app _ func [] = func
+ | tptp_string_for_app format func args =
+ if is_format_higher_order format then
+ "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
+ else
+ func ^ "(" ^ commas args ^ ")"
-fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty)
+fun flatten_type (APi (tys, ty)) = APi (tys, flatten_type ty)
| flatten_type (ty as AFun (ty1 as AType _, ty2)) =
(case flatten_type ty2 of
AFun (ty' as AType (s, tys), ty) =>
@@ -334,6 +341,9 @@
val dfg_individual_type = "iii" (* cannot clash *)
+val suffix_type_of_types =
+ suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)
+
fun str_for_type format ty =
let
val dfg = case format of DFG _ => true | _ => false
@@ -352,10 +362,12 @@
(str false ty1 |> dfg ? enclose "(" ")") ^ " " ^
(if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2
|> not rhs ? enclose "(" ")"
- | str _ (ATyAbs (ss, ty)) =
- tptp_pi_binder ^ "[" ^
- commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))
- ss) ^ "]: " ^ str false ty
+ | str _ (APi (ss, ty)) =
+ if dfg then
+ "[" ^ commas ss ^ "], " ^ str true ty
+ else
+ tptp_pi_binder ^ "[" ^ commas (map suffix_type_of_types ss) ^ "]: " ^
+ str false ty
in str true ty end
fun string_for_type (format as THF _) ty = str_for_type format ty
@@ -380,8 +392,7 @@
"")
fun tptp_string_for_term _ (ATerm ((s, []), [])) = s
- | tptp_string_for_term _ (ATerm ((s, tys), [])) = s (* ### FIXME *)
- | tptp_string_for_term format (ATerm ((s, tys), ts)) = (* ### FIXME *)
+ | tptp_string_for_term format (ATerm ((s, tys), ts)) =
(if s = tptp_empty_list then
(* used for lists in the optional "source" field of a derivation *)
"[" ^ commas (map (tptp_string_for_term format) ts) ^ "]"
@@ -405,7 +416,10 @@
tptp_string_for_term format tm ^ ""
|> enclose "(" ")")
(map (tptp_string_for_term format) args)
- | _ => tptp_string_for_app format s (map (tptp_string_for_term format) ts))
+ | _ =>
+ tptp_string_for_app format s
+ (map (string_for_type format) tys
+ @ map (tptp_string_for_term format) ts))
| tptp_string_for_term (format as THF _) (AAbs (((s, ty), tm), args)) =
tptp_string_for_app format
("(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
@@ -413,7 +427,12 @@
(map (tptp_string_for_term format) args)
| tptp_string_for_term _ _ =
raise Fail "unexpected term in first-order format"
-and tptp_string_for_formula format (AQuant (q, xs, phi)) =
+and tptp_string_for_formula format (ATyQuant (q, xs, phi)) =
+ tptp_string_for_quantifier q ^
+ "[" ^ commas (map (suffix_type_of_types o string_for_type format) xs) ^
+ "]: " ^ tptp_string_for_formula format phi
+ |> enclose "(" ")"
+ | tptp_string_for_formula format (AQuant (q, xs, phi)) =
tptp_string_for_quantifier q ^
"[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^
tptp_string_for_formula format phi
@@ -459,14 +478,21 @@
"\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
map (tptp_string_for_problem_line format) lines)
-fun arity_of_type (AFun (_, ty)) = 1 + arity_of_type ty
- | arity_of_type _ = 0
+fun arity_of_type (APi (tys, ty)) =
+ arity_of_type ty |>> Integer.add (length tys)
+ | arity_of_type (AFun (_, ty)) = arity_of_type ty ||> Integer.add 1
+ | arity_of_type _ = (0, 0)
-fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2
- | binder_atypes _ = []
+fun string_of_arity (0, n) = string_of_int n
+ | string_of_arity (m, n) = string_of_int m ^ "+" ^ string_of_int n
+
+fun strip_atype (APi (tys, ty)) = strip_atype ty |>> apfst (append tys)
+ | strip_atype (AFun (ty1, ty2)) = strip_atype ty2 |>> apsnd (cons ty1)
+ | strip_atype ty = (([], []), ty)
fun dfg_string_for_formula poly gen_simp info =
let
+ val str_for_typ = string_for_type (DFG poly)
fun suffix_tag top_level s =
if top_level then
case extract_isabelle_status info of
@@ -481,7 +507,8 @@
else if s = tptp_true then "true"
else if s = tptp_false then "false"
else s) ^
- (if null tys then "" else "<...>") (* ### FIXME *) ^
+ (if null tys then ""
+ else "<" ^ commas (map (string_for_type (DFG poly)) tys) ^ ">") ^
(if null tms then ""
else "(" ^ commas (map (str_for_term false) tms) ^ ")")
| str_for_term _ _ = raise Fail "unexpected term in first-order format"
@@ -492,8 +519,11 @@
| str_for_conn _ AOr = "or"
| str_for_conn _ AImplies = "implies"
| str_for_conn top_level AIff = "equiv" |> suffix_tag top_level
- fun str_for_formula top_level (AQuant (q, xs, phi)) =
- str_for_quant q ^ "(" ^ "[" ^
+ fun str_for_formula top_level (ATyQuant (q, xs, phi)) =
+ str_for_quant q ^ "_sorts([" ^ commas (map str_for_typ xs) ^
+ "], " ^ str_for_formula top_level phi ^ ")"
+ | str_for_formula top_level (AQuant (q, xs, phi)) =
+ str_for_quant q ^ "([" ^
commas (map (string_for_bound_var (DFG poly)) xs) ^ "], " ^
str_for_formula top_level phi ^ ")"
| str_for_formula top_level (AConn (c, phis)) =
@@ -507,13 +537,19 @@
fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
let
- fun spair (sym, k) = "(" ^ sym ^ ", " ^ string_of_int k ^ ")"
- fun ary sym = curry spair sym o arity_of_type
- fun fun_typ sym ty =
- "function(" ^ sym ^ ", " ^ string_for_type (DFG poly) ty ^ ")."
+ val str_for_typ = string_for_type (DFG poly)
+ fun spair (s, s') = "(" ^ s ^ ", " ^ s' ^ ")"
+ fun tm_ary sym ty = spair (sym, string_of_arity (arity_of_type ty))
+ fun ty_ary [] sym = sym
+ | ty_ary tys sym = "(" ^ sym ^ ", " ^ string_of_int (length tys) ^ ")"
+ fun fun_typ sym ty = "function(" ^ sym ^ ", " ^ str_for_typ ty ^ ")."
fun pred_typ sym ty =
- "predicate(" ^
- commas (sym :: map (string_for_type (DFG poly)) (binder_atypes ty)) ^ ")."
+ let
+ val ((ty_vars, tys), _) = strip_atype ty
+ val (ty_vars, tys) =
+ strip_atype ty |> fst
+ |>> (fn [] => [] | ty_vars => ["[" ^ commas ty_vars ^ "]"])
+ in "predicate(" ^ commas (sym :: ty_vars @ map str_for_typ tys) ^ ")." end
fun formula pred (Formula (ident, kind, phi, _, info)) =
if pred kind then
let val rank = extract_isabelle_rank info in
@@ -528,23 +564,27 @@
fun filt f = problem |> map (map_filter f o snd) |> filter_out null
val func_aries =
filt (fn Decl (_, sym, ty) =>
- if is_function_type ty then SOME (ary sym ty) else NONE
+ if is_function_type ty then SOME (tm_ary sym ty) else NONE
| _ => NONE)
|> flat |> commas |> maybe_enclose "functions [" "]."
val pred_aries =
filt (fn Decl (_, sym, ty) =>
- if is_predicate_type ty then SOME (ary sym ty) else NONE
+ if is_predicate_type ty then SOME (tm_ary sym ty) else NONE
| _ => NONE)
|> flat |> commas |> maybe_enclose "predicates [" "]."
val sorts =
- filt (fn Decl (_, sym, AType (s, [])) =>
- if s = tptp_type_of_types then SOME sym else NONE
+ filt (fn Decl (_, sym, ty) =>
+ (case strip_atype ty of
+ (([], tys), AType (s, [])) =>
+ if s = tptp_type_of_types then SOME (ty_ary tys sym) else NONE
+ | _ => NONE)
| _ => NONE) @ [[dfg_individual_type]]
|> flat |> commas |> maybe_enclose "sorts [" "]."
val ord_info = if gen_weights orelse gen_prec then ord_info () else []
val do_term_order_weights =
(if gen_weights then ord_info else [])
- |> map spair |> commas |> maybe_enclose "weights [" "]."
+ |> map (spair o apsnd string_of_int) |> commas
+ |> maybe_enclose "weights [" "]."
val syms = [func_aries, pred_aries, do_term_order_weights, sorts]
val func_sigs =
filt (fn Decl (_, sym, ty) =>
@@ -798,15 +838,18 @@
fun nice_type (AType (name, tys)) =
nice_name name ##>> pool_map nice_type tys #>> AType
| nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
- | nice_type (ATyAbs (names, ty)) =
- pool_map nice_name names ##>> nice_type ty #>> ATyAbs
+ | nice_type (APi (names, ty)) =
+ pool_map nice_name names ##>> nice_type ty #>> APi
fun nice_term (ATerm ((name, tys), ts)) =
nice_name name ##>> pool_map nice_type tys ##>> pool_map nice_term ts
#>> ATerm
| nice_term (AAbs (((name, ty), tm), args)) =
nice_name name ##>> nice_type ty ##>> nice_term tm
##>> pool_map nice_term args #>> AAbs
- fun nice_formula (AQuant (q, xs, phi)) =
+ fun nice_formula (ATyQuant (q, xs, phi)) =
+ pool_map nice_type xs ##>> nice_formula phi
+ #>> (fn (xs, phi) => ATyQuant (q, xs, phi))
+ | nice_formula (AQuant (q, xs, phi)) =
pool_map nice_name (map fst xs)
##>> pool_map (fn NONE => pair NONE
| SOME ty => nice_type ty #>> SOME) (map snd xs)
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
@@ -359,9 +359,9 @@
fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
-fun make_schematic_type_var (x, i) =
- tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
-fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
+fun make_tvar (s, i) = tvar_prefix ^ (ascii_of_indexname (unprefix "'" s, i))
+fun make_tfree s = tfree_prefix ^ (ascii_of (unprefix "'" s))
+fun tvar_name (x as (s, _)) = (make_tvar x, s)
(* "HOL.eq" and choice are mapped to the ATP's equivalents *)
local
@@ -407,32 +407,36 @@
| _ => I)
fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
+val tvar_a_str = "'a"
+val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
+val tvar_a_name = tvar_name (tvar_a_str, 0)
+val itself_name = `make_fixed_type_const @{type_name itself}
+val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
+val tvar_a_atype = AType (tvar_a_name, [])
+val a_itself_atype = AType (itself_name, [tvar_a_atype])
+
(** Definitions and functions for FOL clauses and formulas for TPTP **)
(** Isabelle arities **)
-type arity_atom = name * name * name list
-
val type_class = the_single @{sort type}
type arity_clause =
{name : string,
- prem_atoms : arity_atom list,
- concl_atom : arity_atom}
+ prems : (string * typ) list,
+ concl : string * typ}
-fun add_prem_atom tvar =
- fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
+fun add_prem_atom T = fold (fn s => s <> type_class ? cons (s, T))
(* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
-fun make_axiom_arity_clause (tcons, name, (cls, args)) =
+fun make_axiom_arity_clause (tc, name, (class, args)) =
let
- val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
- val tvars_srts = ListPair.zip (tvars, args)
+ val tvars =
+ map (fn j => TVar ((tvar_a_str, j), @{sort HOL.type}))
+ (1 upto length args)
in
- {name = name,
- prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
- concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
- tvars ~~ tvars)}
+ {name = name, prems = fold (uncurry add_prem_atom) (tvars ~~ args) [],
+ concl = (class, Type (tc, tvars))}
end
fun arity_clause _ _ (_, []) = []
@@ -487,8 +491,8 @@
type class_rel_clause =
{name : string,
- subclass : name,
- superclass : name}
+ subclass : string,
+ superclass : string}
(* Generate all pairs (sub, super) such that sub is a proper subclass of super
in theory "thy". *)
@@ -501,8 +505,7 @@
in fold add_supers subs [] end
fun make_class_rel_clause (sub, super) =
- {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
- superclass = `make_type_class super}
+ {name = sub ^ "_" ^ super, subclass = sub, superclass = super}
fun make_class_rel_clauses thy subs supers =
map make_class_rel_clause (class_pairs thy subs supers)
@@ -528,14 +531,6 @@
fun atomic_types_of T = fold_atyps (insert (op =)) T []
-val tvar_a_str = "'a"
-val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
-val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
-val itself_name = `make_fixed_type_const @{type_name itself}
-val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
-val tvar_a_atype = AType (tvar_a_name, [])
-val a_itself_atype = AType (itself_name, [tvar_a_atype])
-
fun new_skolem_const_name s num_T_args =
[new_skolem_const_prefix, s, string_of_int num_T_args]
|> Long_Name.implode
@@ -872,79 +867,9 @@
end
end
-(* Make atoms for sorted type variables. *)
-fun generic_add_sorts_on_type (_, []) = I
- | generic_add_sorts_on_type ((x, i), s :: ss) =
- generic_add_sorts_on_type ((x, i), ss)
- #> (if s = the_single @{sort HOL.type} then
- I
- else if i = ~1 then
- insert (op =) (`make_type_class s, `make_fixed_type_var x)
- else
- insert (op =) (`make_type_class s,
- (make_schematic_type_var (x, i), x)))
-fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
- | add_sorts_on_tfree _ = I
-fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
- | add_sorts_on_tvar _ = I
-
-fun type_class_formula type_enc class arg =
- AAtom (ATerm ((class, []), arg ::
- (case type_enc of
- Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
- [ATerm ((TYPE_name, []), [arg])]
- | _ => [])))
-fun formulas_for_types type_enc add_sorts_on_typ Ts =
- [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
- |> map (fn (class, name) =>
- type_class_formula type_enc class (ATerm ((name, []), [])))
-
-fun mk_aconns c phis =
- let val (phis', phi') = split_last phis in
- fold_rev (mk_aconn c) phis' phi'
- end
-fun mk_ahorn [] phi = phi
- | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
-fun mk_aquant _ [] phi = phi
- | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
- if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
- | mk_aquant q xs phi = AQuant (q, xs, phi)
-
-fun close_universally add_term_vars phi =
- let
- fun add_formula_vars bounds (AQuant (_, xs, phi)) =
- add_formula_vars (map fst xs @ bounds) phi
- | add_formula_vars bounds (AConn (_, phis)) =
- fold (add_formula_vars bounds) phis
- | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
- in mk_aquant AForall (add_formula_vars [] phi []) phi end
-
-fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
- (if is_tptp_variable s andalso
- not (String.isPrefix tvar_prefix s) andalso
- not (member (op =) bounds name) then
- insert (op =) (name, NONE)
- else
- I)
- #> fold (add_term_vars bounds) tms
- | add_term_vars bounds (AAbs (((name, _), tm), args)) =
- add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
-fun close_formula_universally phi = close_universally add_term_vars phi
-
-fun add_iterm_vars bounds (IApp (tm1, tm2)) =
- fold (add_iterm_vars bounds) [tm1, tm2]
- | add_iterm_vars _ (IConst _) = I
- | add_iterm_vars bounds (IVar (name, T)) =
- not (member (op =) bounds name) ? insert (op =) (name, SOME T)
- | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
-
-fun close_iformula_universally phi = close_universally add_iterm_vars phi
-
val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
val fused_infinite_type = Type (fused_infinite_type_name, [])
-fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
-
fun ho_term_from_typ type_enc =
let
fun term (Type (s, Ts)) =
@@ -957,7 +882,7 @@
else
`make_fixed_type_const s,
[]), map term Ts)
- | term (TFree (s, _)) = ATerm ((`make_fixed_type_var s, []), [])
+ | term (TFree (s, _)) = ATerm ((`make_tfree s, []), [])
| term (TVar (x, _)) = ATerm ((tvar_name x, []), [])
in term end
@@ -1011,6 +936,87 @@
ho_type_from_ho_term type_enc pred_sym ary
o ho_term_from_typ type_enc
+(* Make atoms for sorted type variables. *)
+fun generic_add_sorts_on_type _ [] = I
+ | generic_add_sorts_on_type T (s :: ss) =
+ generic_add_sorts_on_type T ss
+ #> (if s = the_single @{sort HOL.type} then I else insert (op =) (s, T))
+fun add_sorts_on_tfree (T as TFree (_, S)) = generic_add_sorts_on_type T S
+ | add_sorts_on_tfree _ = I
+fun add_sorts_on_tvar (T as TVar (_, S)) = generic_add_sorts_on_type T S
+ | add_sorts_on_tvar _ = I
+
+fun process_type_args type_enc T_args =
+ if is_type_enc_native type_enc then
+ (map (ho_type_from_typ type_enc false 0) T_args, [])
+ else
+ ([], map_filter (ho_term_for_type_arg type_enc) T_args)
+
+fun type_class_atom type_enc (class, T) =
+ let
+ val class = `make_type_class class
+ val (ty_args, tm_args) = process_type_args type_enc [T]
+ val tm_args =
+ tm_args @
+ (case type_enc of
+ Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
+ [ATerm ((TYPE_name, ty_args), [])]
+ | _ => [])
+ in AAtom (ATerm ((class, ty_args), tm_args)) end
+fun formulas_for_types type_enc add_sorts_on_typ Ts =
+ [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
+ |> map (type_class_atom type_enc)
+
+fun mk_aconns c phis =
+ let val (phis', phi') = split_last phis in
+ fold_rev (mk_aconn c) phis' phi'
+ end
+
+fun mk_ahorn [] phi = phi
+ | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
+
+fun mk_aquant _ [] phi = phi
+ | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
+ if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
+ | mk_aquant q xs phi = AQuant (q, xs, phi)
+
+fun mk_atyquant _ [] phi = phi
+ | mk_atyquant q xs (phi as ATyQuant (q', xs', phi')) =
+ if q = q' then ATyQuant (q, xs @ xs', phi') else ATyQuant (q, xs, phi)
+ | mk_atyquant q xs phi = ATyQuant (q, xs, phi)
+
+fun close_universally add_term_vars phi =
+ let
+ fun add_formula_vars bounds (ATyQuant (_, _, phi)) =
+ add_formula_vars bounds phi
+ | add_formula_vars bounds (AQuant (_, xs, phi)) =
+ add_formula_vars (map fst xs @ bounds) phi
+ | add_formula_vars bounds (AConn (_, phis)) =
+ fold (add_formula_vars bounds) phis
+ | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
+ in mk_aquant AForall (add_formula_vars [] phi []) phi end
+
+fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
+ (if is_tptp_variable s andalso
+ not (String.isPrefix tvar_prefix s) andalso
+ not (member (op =) bounds name) then
+ insert (op =) (name, NONE)
+ else
+ I)
+ #> fold (add_term_vars bounds) tms
+ | add_term_vars bounds (AAbs (((name, _), tm), args)) =
+ add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
+fun close_formula_universally phi = close_universally add_term_vars phi
+
+fun add_iterm_vars bounds (IApp (tm1, tm2)) =
+ fold (add_iterm_vars bounds) [tm1, tm2]
+ | add_iterm_vars _ (IConst _) = I
+ | add_iterm_vars bounds (IVar (name, T)) =
+ not (member (op =) bounds name) ? insert (op =) (name, SOME T)
+ | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
+
+fun close_iformula_universally phi = close_universally add_iterm_vars phi
+
fun aliased_uncurried ary (s, s') =
(s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
fun unaliased_uncurried (s, s') =
@@ -1718,18 +1724,16 @@
@{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
|> map (apsnd (map (apsnd zero_var_indexes)))
-fun atype_of_type_vars (Native (_, Raw_Polymorphic _, _)) = SOME atype_of_types
- | atype_of_type_vars (Native (_, Type_Class_Polymorphic, _)) =
- SOME atype_of_types (* ### FIXME *)
- | atype_of_type_vars _ = NONE
-
fun bound_tvars type_enc sorts Ts =
- (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
- #> mk_aquant AForall
- (map_filter (fn TVar (x as (s, _), _) =>
- SOME ((make_schematic_type_var x, s),
- atype_of_type_vars type_enc)
- | _ => NONE) Ts)
+ case filter is_TVar Ts of
+ [] => I
+ | Ts =>
+ (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
+ #> (if is_type_enc_native type_enc then
+ mk_atyquant AForall
+ (map (fn TVar (x, _) => AType (tvar_name x, [])) Ts)
+ else
+ mk_aquant AForall (map (fn TVar (x, _) => (tvar_name x, NONE)) Ts))
fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
(if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
@@ -1994,11 +1998,9 @@
| should_generate_tag_bound_decl _ _ _ _ _ = false
fun mk_aterm type_enc name T_args args =
-(* ### FIXME
- if is_type_enc_polymorphic type_enc then
- ATerm ((name, map (ho_type_from_typ type_enc false 0) T_args), args)
- else *)
- ATerm ((name, []), map_filter (ho_term_for_type_arg type_enc) T_args @ args)
+ let val (ty_args, tm_args) = process_type_args type_enc T_args in
+ ATerm ((name, ty_args), tm_args @ args)
+ end
fun do_bound_type ctxt mono type_enc =
case type_enc of
@@ -2032,7 +2034,7 @@
map (term Elsewhere) args |> mk_aterm type_enc name []
| IAbs ((name, T), tm) =>
if is_type_enc_higher_order type_enc then
- AAbs (((name, ho_type_from_typ type_enc true 0 T),
+ AAbs (((name, ho_type_from_typ type_enc true (* FIXME? why "true"? *) 0 T),
term Elsewhere tm), map (term Elsewhere) args)
else
raise Fail "unexpected lambda-abstraction"
@@ -2063,7 +2065,10 @@
in SOME (AAtom (ATerm ((`I tptp_equal, []), [tagged_var, var]))) end
else
NONE
- fun do_formula pos (AQuant (q, xs, phi)) =
+ fun do_formula pos (ATyQuant (q, xs, phi)) =
+ ATyQuant (q, map (ho_type_from_typ type_enc false 0) xs,
+ do_formula pos phi)
+ | do_formula pos (AQuant (q, xs, phi)) =
let
val phi = phi |> do_formula pos
val universal = Option.map (q = AExists ? not) pos
@@ -2108,29 +2113,25 @@
fun formula_line_for_class_rel_clause type_enc
({name, subclass, superclass, ...} : class_rel_clause) =
- let val ty_arg = ATerm ((tvar_a_name, []), []) in
- Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
- AConn (AImplies,
- [type_class_formula type_enc subclass ty_arg,
- type_class_formula type_enc superclass ty_arg])
- |> mk_aquant AForall
- [(tvar_a_name, atype_of_type_vars type_enc)],
+ Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
+ AConn (AImplies,
+ [type_class_atom type_enc (subclass, tvar_a),
+ type_class_atom type_enc (superclass, tvar_a)])
+ |> bound_tvars type_enc false [tvar_a],
+ NONE, isabelle_info inductiveN helper_rank)
+
+fun formula_line_for_arity_clause type_enc
+ ({name, prems, concl} : arity_clause) =
+ let
+ val atomic_Ts = fold (fold_atyps (insert (op =)) o snd) (concl :: prems) []
+ in
+ Formula (arity_clause_prefix ^ name, Axiom,
+ mk_ahorn (map (type_class_atom type_enc) prems)
+ (type_class_atom type_enc concl)
+ |> bound_tvars type_enc true atomic_Ts,
NONE, isabelle_info inductiveN helper_rank)
end
-fun formula_from_arity_atom type_enc (class, t, args) =
- ATerm ((t, []), map (fn arg => ATerm ((arg, []), [])) args)
- |> type_class_formula type_enc class
-
-fun formula_line_for_arity_clause type_enc
- ({name, prem_atoms, concl_atom} : arity_clause) =
- Formula (arity_clause_prefix ^ name, Axiom,
- mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
- (formula_from_arity_atom type_enc concl_atom)
- |> mk_aquant AForall
- (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
- NONE, isabelle_info inductiveN helper_rank)
-
fun formula_line_for_conjecture ctxt mono type_enc
({name, role, iformula, atomic_types, ...} : ifact) =
Formula (conjecture_prefix ^ name, role,
@@ -2140,21 +2141,14 @@
|> close_formula_universally
|> bound_tvars type_enc true atomic_types, NONE, [])
-fun type_enc_needs_free_types (Native (_, Raw_Polymorphic _, _)) = true
- | type_enc_needs_free_types (Native _) = false
- | type_enc_needs_free_types _ = true
-
-fun formula_line_for_free_type j phi =
- Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
fun formula_lines_for_free_types type_enc (facts : ifact list) =
- if type_enc_needs_free_types type_enc then
- let
- val phis =
- fold (union (op =)) (map #atomic_types facts) []
- |> formulas_for_types type_enc add_sorts_on_tfree
- in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
- else
- []
+ let
+ fun line j phi =
+ Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
+ val phis =
+ fold (union (op =)) (map #atomic_types facts) []
+ |> formulas_for_types type_enc add_sorts_on_tfree
+ in map2 line (0 upto length phis - 1) phis end
(** Symbol declarations **)
@@ -2162,11 +2156,11 @@
let val name as (s, _) = `make_type_class s in
Decl (sym_decl_prefix ^ s, name,
if order = First_Order then
- ATyAbs ([tvar_a_name],
- if phantoms = Without_Phantom_Type_Vars then
- AFun (a_itself_atype, bool_atype)
- else
- bool_atype)
+ APi ([tvar_a_name],
+ if phantoms = Without_Phantom_Type_Vars then
+ AFun (a_itself_atype, bool_atype)
+ else
+ bool_atype)
else
AFun (atype_of_types, bool_atype))
end
@@ -2207,7 +2201,8 @@
#> fold add_iterm_syms args
end
val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> ifact_lift
- fun add_formula_var_types (AQuant (_, xs, phi)) =
+ fun add_formula_var_types (ATyQuant (_, _, phi)) = add_formula_var_types phi
+ | add_formula_var_types (AQuant (_, xs, phi)) =
fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
#> add_formula_var_types phi
| add_formula_var_types (AConn (_, phis)) =
@@ -2359,7 +2354,7 @@
T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
|> ho_type_from_typ type_enc pred_sym ary
|> not (null T_args)
- ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
+ ? curry APi (map (tvar_name o fst o dest_TVar) T_args))
end
fun honor_conj_sym_role in_conj =
@@ -2574,8 +2569,9 @@
else
individual_atype
| _ => individual_atype
- fun typ 0 = if pred_sym then bool_atype else ind
- | typ ary = AFun (ind, typ (ary - 1))
+ fun typ 0 0 = if pred_sym then bool_atype else ind
+ | typ 0 tm_ary = AFun (ind, typ 0 (tm_ary - 1))
+ | typ ty_ary tm_ary = APi (replicate ty_ary tvar_a_name, typ 0 tm_ary)
in typ end
fun nary_type_constr_type n =
@@ -2592,13 +2588,15 @@
do_sym name (fn () => nary_type_constr_type (length tys))
#> fold do_type tys
| do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
- | do_type (ATyAbs (_, ty)) = do_type ty
+ | do_type (APi (_, ty)) = do_type ty
fun do_term pred_sym (ATerm ((name as (s, _), tys), tms)) =
- do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
+ do_sym name
+ (fn _ => default_type type_enc pred_sym s (length tys) (length tms))
#> fold do_type tys #> fold (do_term false) tms
| do_term _ (AAbs (((_, ty), tm), args)) =
do_type ty #> do_term false tm #> fold (do_term false) args
- fun do_formula (AQuant (_, xs, phi)) =
+ fun do_formula (ATyQuant (_, _, phi)) = do_formula phi
+ | do_formula (AQuant (_, xs, phi)) =
fold do_type (map_filter snd xs) #> do_formula phi
| do_formula (AConn (_, phis)) = fold do_formula phis
| do_formula (AAtom tm) = do_term true tm
@@ -2794,16 +2792,19 @@
else (s, tms)
| make_head_roll _ = ("", [])
-fun strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi
+fun strip_up_to_predicator (ATyQuant (_, _, phi)) = strip_up_to_predicator phi
+ | strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi
| strip_up_to_predicator (AConn (_, phis)) = maps strip_up_to_predicator phis
| strip_up_to_predicator (AAtom tm) = [strip_predicator tm]
-fun strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi
+fun strip_ahorn_etc (ATyQuant (_, _, phi)) = strip_ahorn_etc phi
+ | strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi
| strip_ahorn_etc (AConn (AImplies, [phi1, phi2])) =
strip_ahorn_etc phi2 |>> append (strip_up_to_predicator phi1)
| strip_ahorn_etc phi = ([], hd (strip_up_to_predicator phi))
-fun strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi
+fun strip_iff_etc (ATyQuant (_, _, phi)) = strip_iff_etc phi
+ | strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi
| strip_iff_etc (AConn (AIff, [phi1, phi2])) =
pairself strip_up_to_predicator (phi1, phi2)
| strip_iff_etc _ = ([], [])