--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:07:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:07:45 2011 +0200
@@ -19,7 +19,8 @@
datatype 'a ho_type =
AType of 'a * 'a ho_type list |
- AFun of 'a ho_type * 'a ho_type
+ AFun of 'a ho_type * 'a ho_type |
+ ATyAbs of 'a list * 'a ho_type
datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
datatype tff_explicitness = TFF_Implicit | TFF_Explicit
@@ -122,7 +123,8 @@
datatype 'a ho_type =
AType of 'a * 'a ho_type list |
- AFun of 'a ho_type * 'a ho_type
+ AFun of 'a ho_type * 'a ho_type |
+ ATyAbs of 'a list * 'a ho_type
datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
datatype tff_explicitness = TFF_Implicit | TFF_Explicit
@@ -229,29 +231,38 @@
| string_for_kind Hypothesis = "hypothesis"
| string_for_kind Conjecture = "conjecture"
-fun strip_tff_type (AFun (AFun _, _)) =
+fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (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) =>
+ AFun (AType (tptp_product_type,
+ ty1 :: (if s = tptp_product_type then tys else [ty'])), ty)
+ | _ => ty)
+ | flatten_type (ty as AType _) = ty
+ | flatten_type _ =
raise Fail "unexpected higher-order type in first-order format"
- | strip_tff_type (AFun (ty1, ty2)) = strip_tff_type ty2 |>> cons ty1
- | strip_tff_type ty = ([], ty)
-fun general_string_for_type ty =
+fun str_for_type ty =
let
fun str _ (AType (s, [])) = s
- | str _ (AType (s, tys)) = s ^ "(" ^ commas (map (str false) tys) ^ ")"
+ | str _ (AType (s, tys)) =
+ tys |> map (str false)
+ |> (if s = tptp_product_type then
+ space_implode (" " ^ tptp_product_type ^ " ")
+ #> length tys > 1 ? enclose "(" ")"
+ else
+ commas #> enclose "(" ")" #> prefix s)
| str rhs (AFun (ty1, ty2)) =
str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
|> not rhs ? enclose "(" ")"
+ | str _ (ATyAbs (ss, ty)) =
+ tptp_forall ^ "[" ^
+ commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))
+ ss) ^ "] : " ^ str false ty
in str true ty end
-fun string_for_type (THF0 _) ty = general_string_for_type ty
- | string_for_type (TFF _) ty =
- (case strip_tff_type ty of
- ([], ty) => general_string_for_type ty
- | ([ty1], ty2) => general_string_for_type (AFun (ty1, ty2))
- | (tys, ty) =>
- "(" ^ space_implode (" " ^ tptp_product_type ^ " ")
- (map general_string_for_type tys) ^ ") " ^ tptp_fun_type ^ " " ^
- general_string_for_type ty)
+fun string_for_type (THF0 _) ty = str_for_type ty
+ | string_for_type (TFF _) ty = str_for_type (flatten_type ty)
| string_for_type _ _ = raise Fail "unexpected type in untyped format"
fun string_for_quantifier AForall = tptp_forall
@@ -469,9 +480,10 @@
let
fun do_sym name ty =
if member (op =) declared name then I else AList.default (op =) (name, ty)
- fun do_type (AType (name, tys)) =
- do_sym name (K atype_of_types) #> fold do_type tys
+ fun do_type_name name = do_sym name (K atype_of_types)
+ fun do_type (AType (name, tys)) = do_type_name name #> fold do_type tys
| do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
+ | do_type (ATyAbs (names, ty)) = fold do_type_name names #> do_type ty
fun do_term pred_sym (ATerm (name as (s, _), tms)) =
is_tptp_user_symbol s
? do_sym name (fn _ => default_type pred_sym (length tms))
@@ -571,6 +583,8 @@
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
fun nice_term (ATerm (name, ts)) =
nice_name name ##>> pool_map nice_term ts #>> ATerm
| nice_term (AAbs ((name, ty), tm)) =
--- a/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 16:07:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 16:07:45 2011 +0200
@@ -495,6 +495,15 @@
[new_skolem_const_prefix, s, string_of_int num_T_args]
|> space_implode Long_Name.separator
+fun robust_const_type thy s =
+ if s = app_op_name then Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
+ else s |> Sign.the_const_type thy
+
+(* This function only makes sense if "T" is as general as possible. *)
+fun robust_const_typargs thy (s, T) =
+ (s, T) |> Sign.const_typargs thy
+ handle TYPE _ => [] |> Term.add_tvarsT T |> rev |> map TVar
+
(* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
Also accumulates sort infomation. *)
fun iterm_from_term thy format bs (P $ Q) =
@@ -504,10 +513,7 @@
in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
| iterm_from_term thy format _ (Const (c, T)) =
(IConst (`(make_fixed_const (SOME format)) c, T,
- if String.isPrefix old_skolem_const_prefix c then
- [] |> Term.add_tvarsT T |> map TVar
- else
- (c, T) |> Sign.const_typargs thy),
+ robust_const_typargs thy (c, T)),
atyps_of T)
| iterm_from_term _ _ _ (Free (s, T)) =
(IConst (`make_fixed_var s, T,
@@ -690,8 +696,7 @@
Mangled_Type_Args of bool |
No_Type_Args
-fun should_drop_arg_type_args (Simple_Types _) =
- false (* since TFF doesn't support overloading *)
+fun should_drop_arg_type_args (Simple_Types _) = false
| should_drop_arg_type_args type_enc =
level_of_type_enc type_enc = All_Types andalso
uniformity_of_type_enc type_enc = Uniform
@@ -783,8 +788,10 @@
fun close_formula_universally type_enc =
close_universally (term_vars type_enc [])
-val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
-val homo_infinite_type = Type (homo_infinite_type_name, [])
+val fused_infinite_type_name = @{type_name ind} (* any infinite type *)
+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 format type_enc =
let
@@ -792,15 +799,14 @@
ATerm (case (is_type_enc_higher_order type_enc, s) of
(true, @{type_name bool}) => `I tptp_bool_type
| (true, @{type_name fun}) => `I tptp_fun_type
- | _ => if s = homo_infinite_type_name andalso
+ | _ => if s = fused_infinite_type_name andalso
is_format_typed format then
`I tptp_individual_type
else
`make_fixed_type_const s,
map term Ts)
| term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
- | term (TVar ((x as (s, _)), _)) =
- ATerm ((make_schematic_type_var x, s), [])
+ | term (TVar (x, _)) = ATerm (tvar_name x, [])
in term end
fun ho_term_for_type_arg format type_enc T =
@@ -1177,14 +1183,14 @@
| _ => false)
| should_tag_with_type _ _ _ _ _ _ = false
-fun homogenized_type ctxt mono level =
+fun fused_type ctxt mono level =
let
val should_encode = should_encode_type ctxt mono level
- fun homo 0 T = if should_encode T then T else homo_infinite_type
- | homo ary (Type (@{type_name fun}, [T1, T2])) =
- homo 0 T1 --> homo (ary - 1) T2
- | homo _ _ = raise Fail "expected function type"
- in homo end
+ fun fuse 0 T = if should_encode T then T else fused_infinite_type
+ | fuse ary (Type (@{type_name fun}, [T1, T2])) =
+ fuse 0 T1 --> fuse (ary - 1) T2
+ | fuse _ _ = raise Fail "expected function type"
+ in fuse end
(** predicators and application operators **)
@@ -1361,13 +1367,7 @@
fun filter_type_args _ _ _ [] = []
| filter_type_args thy s arity T_args =
- let
- (* will throw "TYPE" for pseudo-constants *)
- val U = if s = app_op_name then
- @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
- else
- s |> Sign.the_const_type thy
- in
+ let val U = robust_const_type thy s in
case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
[] => []
| res_U_vars =>
@@ -1688,8 +1688,7 @@
val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
val do_bound_type =
case type_enc of
- Simple_Types (_, _, level) =>
- homogenized_type ctxt mono level 0
+ Simple_Types (_, _, level) => fused_type ctxt mono level 0
#> ho_type_from_typ format type_enc false 0 #> SOME
| _ => K NONE
fun do_out_of_bound_type pos phi universal (name, T) =
@@ -1792,12 +1791,6 @@
(** Symbol declarations **)
-fun should_declare_sym type_enc pred_sym s =
- (case type_enc of
- Guards _ => not pred_sym
- | _ => true) andalso
- is_tptp_user_symbol s
-
fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
(conjs, facts) =
let
@@ -1805,8 +1798,15 @@
let val (head, args) = strip_iterm_comb tm in
(case head of
IConst ((s, s'), T, T_args) =>
- let val pred_sym = is_pred_sym repaired_sym_tab s in
- if should_declare_sym type_enc pred_sym s then
+ let
+ val pred_sym = is_pred_sym repaired_sym_tab s
+ val decl_sym =
+ (case type_enc of
+ Guards _ => not pred_sym
+ | _ => true) andalso
+ is_tptp_user_symbol s
+ in
+ if decl_sym then
Symtab.map_default (s, [])
(insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
in_conj))
@@ -1964,14 +1964,28 @@
fun decl_line_for_sym ctxt format mono type_enc s
(s', T_args, T, pred_sym, ary, _) =
let
- val (T_arg_Ts, level) =
- case type_enc of
- Simple_Types (_, _, level) => ([], level)
- | _ => (replicate (length T_args) homo_infinite_type, No_Types)
+ val thy = Proof_Context.theory_of ctxt
+ val (T, T_args) =
+ if null T_args then
+ (T, [])
+ else case strip_prefix_and_unascii const_prefix s of
+ SOME s' =>
+ let
+ val s' = s' |> invert_const
+ val T = s' |> robust_const_type thy
+ in (T, robust_const_typargs thy (s', T)) end
+ | NONE =>
+ case strip_prefix_and_unascii fixed_var_prefix s of
+ SOME s' =>
+ if String.isPrefix polymorphic_free_prefix s' then (tvar_a, [tvar_a])
+ else raise Fail "unexpected type arguments to free variable"
+ | NONE => raise Fail "unexpected type arguments"
in
Decl (sym_decl_prefix ^ s, (s, s'),
- (T_arg_Ts ---> (T |> homogenized_type ctxt mono level ary))
- |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
+ T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
+ |> ho_type_from_typ format type_enc pred_sym ary
+ |> not (null T_args)
+ ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
end
fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s