--- a/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:40 2012 +0200
@@ -112,7 +112,8 @@
fun add_inferences_to_problem infers =
map (apsnd (map (add_inferences_to_problem_line infers)))
-fun ident_of_problem_line (Decl (ident, _, _)) = ident
+fun ident_of_problem_line (Type_Decl (ident, _, _)) = ident
+ | ident_of_problem_line (Sym_Decl (ident, _, _)) = ident
| ident_of_problem_line (Formula (ident, _, _, _, _)) = ident
fun run_some_atp ctxt format problem =
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
@@ -44,7 +44,8 @@
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
- Decl of string * 'a * 'a ho_type |
+ Type_Decl of string * 'a * int |
+ Sym_Decl of string * 'a * 'a ho_type |
Formula of string * formula_role
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
* (string, string ho_type) ho_term option
@@ -98,7 +99,6 @@
val is_built_in_tptp_symbol : string -> bool
val is_tptp_variable : string -> bool
val is_tptp_user_symbol : string -> bool
- val atype_of_types : (string * string) ho_type
val bool_atype : (string * string) ho_type
val individual_atype : (string * string) ho_type
val mk_anot : ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'c, 'd) formula
@@ -116,8 +116,6 @@
-> 'e -> 'e
val formula_map :
('c -> 'e) -> ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'e, 'd) formula
- val is_function_type : string ho_type -> bool
- val is_predicate_type : string ho_type -> bool
val is_format_higher_order : atp_format -> bool
val lines_for_atp_problem :
atp_format -> term_order -> (unit -> (string * int) list) -> string problem
@@ -126,7 +124,7 @@
(string * string) problem -> (string * string) problem
val filter_cnf_ueq_problem :
(string * string) problem -> (string * string) problem
- val declared_syms_in_problem : 'a problem -> 'a list
+ val declared_types_and_syms_in_problem : 'a problem -> 'a list * 'a list
val nice_atp_problem :
bool -> atp_format -> ('a * (string * string) problem_line list) list
-> ('a * string problem_line list) list
@@ -178,7 +176,8 @@
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
- Decl of string * 'a * 'a ho_type |
+ Type_Decl of string * 'a * int |
+ Sym_Decl of string * 'a * 'a ho_type |
Formula of string * formula_role
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
* (string, string ho_type) ho_term option
@@ -253,7 +252,6 @@
fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol)
-val atype_of_types = AType (`I tptp_type_of_types, [])
val bool_atype = AType (`I tptp_bool_type, [])
val individual_atype = AType (`I tptp_individual_type, [])
@@ -297,17 +295,14 @@
| 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 (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 (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 (AType _) = false
- | is_nontrivial_predicate_type ty = is_predicate_type ty
+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 is_function_atype ty = snd (strip_atype ty) <> AType (tptp_bool_type, [])
+fun is_predicate_atype ty = not (is_function_atype ty)
+fun is_nontrivial_predicate_atype (AType _) = false
+ | is_nontrivial_predicate_atype ty = is_predicate_atype ty
fun is_format_higher_order (THF _) = true
| is_format_higher_order _ = false
@@ -462,7 +457,15 @@
| tptp_string_for_format (THF _) = tptp_thf
| tptp_string_for_format (DFG _) = raise Fail "non-TPTP format"
-fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) =
+val atype_of_types = AType (tptp_type_of_types, [])
+
+fun nary_type_constr_type n =
+ funpow n (curry AFun atype_of_types) atype_of_types
+
+fun tptp_string_for_problem_line format (Type_Decl (ident, sym, ary)) =
+ tptp_string_for_problem_line format
+ (Sym_Decl (ident, sym, nary_type_constr_type ary))
+ | tptp_string_for_problem_line format (Sym_Decl (ident, sym, ty)) =
tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^
" : " ^ string_for_type format ty ^ ").\n"
| tptp_string_for_problem_line format
@@ -488,10 +491,6 @@
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)
@@ -542,8 +541,8 @@
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 ty_ary 0 sym = sym
+ | ty_ary n sym = "(" ^ sym ^ ", " ^ string_of_int n ^ ")"
fun fun_typ sym ty = "function(" ^ sym ^ ", " ^ str_for_typ ty ^ ")."
fun pred_typ sym ty =
let
@@ -565,22 +564,18 @@
| formula _ _ = NONE
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 (tm_ary sym ty) else NONE
+ filt (fn Sym_Decl (_, sym, ty) =>
+ if is_function_atype 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 (tm_ary sym ty) else NONE
+ filt (fn Sym_Decl (_, sym, ty) =>
+ if is_predicate_atype ty then SOME (tm_ary sym ty) else NONE
| _ => NONE)
|> flat |> commas |> maybe_enclose "predicates [" "]."
val sorts =
- 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]]
+ filt (fn Type_Decl (_, sym, ary) => SOME (ty_ary ary sym) | _ => NONE) @
+ [[ty_ary 0 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 =
@@ -589,13 +584,13 @@
|> maybe_enclose "weights [" "]."
val syms = [func_aries, pred_aries, do_term_order_weights, sorts]
val func_sigs =
- filt (fn Decl (_, sym, ty) =>
- if is_function_type ty then SOME (fun_typ sym ty) else NONE
+ filt (fn Sym_Decl (_, sym, ty) =>
+ if is_function_atype ty then SOME (fun_typ sym ty) else NONE
| _ => NONE)
|> flat
val pred_sigs =
- filt (fn Decl (_, sym, ty) =>
- if is_nontrivial_predicate_type ty then SOME (pred_typ sym ty)
+ filt (fn Sym_Decl (_, sym, ty) =>
+ if is_nontrivial_predicate_atype ty then SOME (pred_typ sym ty)
else NONE
| _ => NONE)
|> flat
@@ -723,10 +718,11 @@
(** Symbol declarations **)
-fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = cons sym
+fun add_declared_syms_in_problem_line (Type_Decl (_, sym, _)) = apfst (cons sym)
+ | add_declared_syms_in_problem_line (Sym_Decl (_, sym, _)) = apsnd (cons sym)
| add_declared_syms_in_problem_line _ = I
-fun declared_syms_in_problem problem =
- fold (fold add_declared_syms_in_problem_line o snd) problem []
+fun declared_types_and_syms_in_problem problem =
+ fold (fold add_declared_syms_in_problem_line o snd) problem ([], [])
(** Nice names **)
@@ -861,8 +857,11 @@
| nice_formula (AConn (c, phis)) =
pool_map nice_formula phis #>> curry AConn c
| nice_formula (AAtom tm) = nice_term tm #>> AAtom
- fun nice_problem_line (Decl (ident, sym, ty)) =
- nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Decl (ident, sym, ty))
+ fun nice_problem_line (Type_Decl (ident, sym, ary)) =
+ nice_name sym #>> (fn sym => Type_Decl (ident, sym, ary))
+ | nice_problem_line (Sym_Decl (ident, sym, ty)) =
+ nice_name sym ##>> nice_type ty
+ #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty))
| nice_problem_line (Formula (ident, kind, phi, source, info)) =
nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
fun nice_problem problem =
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
@@ -2163,15 +2163,12 @@
fun decl_line_for_class order phantoms s =
let val name as (s, _) = `make_type_class s in
- Decl (sym_decl_prefix ^ s, name,
- if order = First_Order then
- 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))
+ Sym_Decl (sym_decl_prefix ^ s, name,
+ APi ([tvar_a_name],
+ if phantoms = Without_Phantom_Type_Vars then
+ AFun (a_itself_atype, bool_atype)
+ else
+ bool_atype))
end
fun decl_lines_for_classes type_enc classes =
@@ -2359,11 +2356,11 @@
in (T, robust_const_typargs thy (s', T)) end
| NONE => raise Fail "unexpected type arguments"
in
- Decl (sym_decl_prefix ^ s, (s, s'),
- 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 APi (map (tvar_name o fst o dest_TVar) T_args))
+ Sym_Decl (sym_decl_prefix ^ s, (s, s'),
+ 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 APi (map (tvar_name o fst o dest_TVar) T_args))
end
fun honor_conj_sym_role in_conj =
@@ -2574,21 +2571,17 @@
| 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 =
- funpow n (curry AFun atype_of_types) atype_of_types
-
-fun undeclared_syms_in_problem problem =
+fun undeclared_types_and_syms_in_problem problem =
let
- fun do_sym (name as (s, _)) ty =
- if is_tptp_user_symbol s then Symtab.default (s, (name, ty)) else I
+ fun do_sym (name as (s, _)) value =
+ if is_tptp_user_symbol s then Symtab.default (s, (name, value)) else I
fun do_type (AType (name, tys)) =
- do_sym name (fn () => nary_type_constr_type (length tys))
- #> fold do_type tys
+ apfst (do_sym name (length tys)) #> fold do_type tys
| do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
| do_type (APi (_, ty)) = do_type ty
fun do_term pred_sym (ATerm ((name as (s, _), tys), tms)) =
- do_sym name
- (fn _ => default_type pred_sym s (length tys) (length tms))
+ apsnd (do_sym name
+ (fn _ => default_type 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
@@ -2597,22 +2590,29 @@
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
- fun do_problem_line (Decl (_, _, ty)) = do_type ty
+ fun do_problem_line (Type_Decl _) = I
+ | do_problem_line (Sym_Decl (_, _, ty)) = do_type ty
| do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
+ val (tys, syms) = declared_types_and_syms_in_problem problem
in
- Symtab.empty
- |> fold (fn (s, _) => Symtab.default (s, (("", ""), K tvar_a_atype)))
- (declared_syms_in_problem problem)
+ (Symtab.empty, Symtab.empty)
+ |>> fold (fn (s, _) => Symtab.default (s, (("", ""), 0))) tys
+ ||> fold (fn (s, _) => Symtab.default (s, (("", ""), K tvar_a_atype))) syms
|> fold (fold do_problem_line o snd) problem
end
-fun declare_undeclared_syms_in_atp_problem problem =
+fun declare_undeclared_types_and_syms_in_atp_problem problem =
let
+ val (types, syms) = undeclared_types_and_syms_in_problem problem
val decls =
Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
+ | (s, (sym, ary)) =>
+ cons (Type_Decl (type_decl_prefix ^ s, sym, ary)))
+ types [] @
+ Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
| (s, (sym, ty)) =>
- cons (Decl (type_decl_prefix ^ s, sym, ty ())))
- (undeclared_syms_in_problem problem) []
+ cons (Sym_Decl (type_decl_prefix ^ s, sym, ty ())))
+ syms []
in (implicit_declsN, decls) :: problem end
fun exists_subdtype P =
@@ -2719,7 +2719,7 @@
| FOF => I
| TFF (_, TPTP_Implicit) => I
| THF (_, TPTP_Implicit, _, _) => I
- | _ => declare_undeclared_syms_in_atp_problem)
+ | _ => declare_undeclared_types_and_syms_in_atp_problem)
val (problem, pool) = problem |> nice_atp_problem readable_names format
fun add_sym_ary (s, {min_ary, ...} : sym_info) =
min_ary > 0 ? Symtab.insert (op =) (s, min_ary)