# HG changeset patch # User blanchet # Date 1340702080 -7200 # Node ID 6f524f2066e3003123422f4e80a152bb2715cee8 # Parent 0f9939676088b89ee4f245c609b4fcc063597823 cleanly distinguish between type declarations and symbol declarations diff -r 0f9939676088 -r 6f524f2066e3 src/HOL/TPTP/atp_theory_export.ML --- 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 = diff -r 0f9939676088 -r 6f524f2066e3 src/HOL/Tools/ATP/atp_problem.ML --- 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 = diff -r 0f9939676088 -r 6f524f2066e3 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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)