1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Jul 05 09:54:39 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Jul 05 17:09:59 2011 +0100
1.3 @@ -8,7 +8,7 @@
1.4
1.5 signature ATP_TRANSLATE =
1.6 sig
1.7 - type 'a fo_term = 'a ATP_Problem.fo_term
1.8 + type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
1.9 type connective = ATP_Problem.connective
1.10 type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
1.11 type format = ATP_Problem.format
1.12 @@ -83,7 +83,7 @@
1.13 val choose_format : format list -> type_enc -> format * type_enc
1.14 val mk_aconns :
1.15 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
1.16 - val unmangled_const : string -> string * string fo_term list
1.17 + val unmangled_const : string -> string * (string, 'b) ho_term list
1.18 val unmangled_const_name : string -> string
1.19 val helper_table : ((string * bool) * thm list) list
1.20 val factsN : string
1.21 @@ -545,7 +545,8 @@
1.22 ("simple", (NONE, _, Lightweight)) =>
1.23 Simple_Types (First_Order, level)
1.24 | ("simple_higher", (NONE, _, Lightweight)) =>
1.25 - Simple_Types (Higher_Order, level)
1.26 + if level = Noninf_Nonmono_Types then raise Same.SAME
1.27 + else Simple_Types (Higher_Order, level)
1.28 | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
1.29 | ("tags", (SOME Polymorphic, _, _)) =>
1.30 Tags (Polymorphic, level, heaviness)
1.31 @@ -698,14 +699,16 @@
1.32 | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
1.33 fun close_combformula_universally phi = close_universally combterm_vars phi
1.34
1.35 -fun term_vars (ATerm (name as (s, _), tms)) =
1.36 - is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
1.37 -fun close_formula_universally phi = close_universally term_vars phi
1.38 +fun term_vars bounds (ATerm (name as (s, _), tms)) =
1.39 + (is_tptp_variable s andalso not (member (op =) bounds name))
1.40 + ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms
1.41 + | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm
1.42 +fun close_formula_universally phi = close_universally (term_vars []) phi
1.43
1.44 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
1.45 val homo_infinite_type = Type (homo_infinite_type_name, [])
1.46
1.47 -fun fo_term_from_typ format type_enc =
1.48 +fun ho_term_from_typ format type_enc =
1.49 let
1.50 fun term (Type (s, Ts)) =
1.51 ATerm (case (is_type_enc_higher_order type_enc, s) of
1.52 @@ -722,8 +725,8 @@
1.53 ATerm ((make_schematic_type_var x, s), [])
1.54 in term end
1.55
1.56 -fun fo_term_for_type_arg format type_enc T =
1.57 - if T = dummyT then NONE else SOME (fo_term_from_typ format type_enc T)
1.58 +fun ho_term_for_type_arg format type_enc T =
1.59 + if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
1.60
1.61 (* This shouldn't clash with anything else. *)
1.62 val mangled_type_sep = "\000"
1.63 @@ -732,6 +735,7 @@
1.64 | generic_mangled_type_name f (ATerm (name, tys)) =
1.65 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
1.66 ^ ")"
1.67 + | generic_mangled_type_name f _ = raise Fail "unexpected type abstraction"
1.68
1.69 val bool_atype = AType (`I tptp_bool_type)
1.70
1.71 @@ -742,7 +746,7 @@
1.72 else
1.73 simple_type_prefix ^ ascii_of s
1.74
1.75 -fun ho_type_from_fo_term type_enc pred_sym ary =
1.76 +fun ho_type_from_ho_term type_enc pred_sym ary =
1.77 let
1.78 fun to_atype ty =
1.79 AType ((make_simple_type (generic_mangled_type_name fst ty),
1.80 @@ -750,17 +754,19 @@
1.81 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
1.82 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
1.83 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
1.84 + | to_fo ary _ = raise Fail "unexpected type abstraction"
1.85 fun to_ho (ty as ATerm ((s, _), tys)) =
1.86 - if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
1.87 + if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
1.88 + | to_ho _ = raise Fail "unexpected type abstraction"
1.89 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
1.90
1.91 fun mangled_type format type_enc pred_sym ary =
1.92 - ho_type_from_fo_term type_enc pred_sym ary
1.93 - o fo_term_from_typ format type_enc
1.94 + ho_type_from_ho_term type_enc pred_sym ary
1.95 + o ho_term_from_typ format type_enc
1.96
1.97 fun mangled_const_name format type_enc T_args (s, s') =
1.98 let
1.99 - val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_enc)
1.100 + val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
1.101 fun type_suffix f g =
1.102 fold_rev (curry (op ^) o g o prefix mangled_type_sep
1.103 o generic_mangled_type_name f) ty_args ""
1.104 @@ -1444,12 +1450,13 @@
1.105 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1.106 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1.107 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1.108 + | is_var_positively_naked_in_term name _ _ _ = true
1.109 fun should_predicate_on_var_in_formula pos phi (SOME true) name =
1.110 formula_fold pos (is_var_positively_naked_in_term name) phi false
1.111 | should_predicate_on_var_in_formula _ _ _ _ = true
1.112
1.113 fun mk_const_aterm format type_enc x T_args args =
1.114 - ATerm (x, map_filter (fo_term_for_type_arg format type_enc) T_args @ args)
1.115 + ATerm (x, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
1.116
1.117 fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
1.118 CombConst (type_tag, T --> T, [T])
1.119 @@ -1924,8 +1931,9 @@
1.120 val type_info_default_weight = 0.8
1.121
1.122 fun add_term_weights weight (ATerm (s, tms)) =
1.123 - is_tptp_user_symbol s ? Symtab.default (s, weight)
1.124 - #> fold (add_term_weights weight) tms
1.125 + is_tptp_user_symbol s ? Symtab.default (s, weight)
1.126 + #> fold (add_term_weights weight) tms
1.127 + | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
1.128 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
1.129 formula_fold NONE (K (add_term_weights weight)) phi
1.130 | add_problem_line_weights _ _ = I