1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
1.3 @@ -889,15 +889,15 @@
1.4 | add_sorts_on_tvar _ = I
1.5
1.6 fun type_class_formula type_enc class arg =
1.7 - AAtom (ATerm (class, arg ::
1.8 + AAtom (ATerm ((class, []), arg ::
1.9 (case type_enc of
1.10 Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
1.11 - [ATerm (TYPE_name, [arg])]
1.12 + [ATerm ((TYPE_name, []), [arg])]
1.13 | _ => [])))
1.14 fun formulas_for_types type_enc add_sorts_on_typ Ts =
1.15 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
1.16 |> map (fn (class, name) =>
1.17 - type_class_formula type_enc class (ATerm (name, [])))
1.18 + type_class_formula type_enc class (ATerm ((name, []), [])))
1.19
1.20 fun mk_aconns c phis =
1.21 let val (phis', phi') = split_last phis in
1.22 @@ -919,7 +919,7 @@
1.23 | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
1.24 in mk_aquant AForall (add_formula_vars [] phi []) phi end
1.25
1.26 -fun add_term_vars bounds (ATerm (name as (s, _), tms)) =
1.27 +fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
1.28 (if is_tptp_variable s andalso
1.29 not (String.isPrefix tvar_prefix s) andalso
1.30 not (member (op =) bounds name) then
1.31 @@ -948,17 +948,17 @@
1.32 fun ho_term_from_typ type_enc =
1.33 let
1.34 fun term (Type (s, Ts)) =
1.35 - ATerm (case (is_type_enc_higher_order type_enc, s) of
1.36 - (true, @{type_name bool}) => `I tptp_bool_type
1.37 - | (true, @{type_name fun}) => `I tptp_fun_type
1.38 - | _ => if s = fused_infinite_type_name andalso
1.39 - is_type_enc_native type_enc then
1.40 - `I tptp_individual_type
1.41 - else
1.42 - `make_fixed_type_const s,
1.43 - map term Ts)
1.44 - | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
1.45 - | term (TVar (x, _)) = ATerm (tvar_name x, [])
1.46 + ATerm ((case (is_type_enc_higher_order type_enc, s) of
1.47 + (true, @{type_name bool}) => `I tptp_bool_type
1.48 + | (true, @{type_name fun}) => `I tptp_fun_type
1.49 + | _ => if s = fused_infinite_type_name andalso
1.50 + is_type_enc_native type_enc then
1.51 + `I tptp_individual_type
1.52 + else
1.53 + `make_fixed_type_const s,
1.54 + []), map term Ts)
1.55 + | term (TFree (s, _)) = ATerm ((`make_fixed_type_var s, []), [])
1.56 + | term (TVar (x, _)) = ATerm ((tvar_name x, []), [])
1.57 in term end
1.58
1.59 fun ho_term_for_type_arg type_enc T =
1.60 @@ -970,8 +970,9 @@
1.61
1.62 val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
1.63
1.64 -fun generic_mangled_type_name f (ATerm (name, [])) = f name
1.65 - | generic_mangled_type_name f (ATerm (name, tys)) =
1.66 +(* ### FIXME: insane *)
1.67 +fun generic_mangled_type_name f (ATerm ((name, _), [])) = f name
1.68 + | generic_mangled_type_name f (ATerm ((name, _), tys)) =
1.69 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
1.70 ^ ")"
1.71 | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
1.72 @@ -991,7 +992,8 @@
1.73 fun to_mangled_atype ty =
1.74 AType ((make_native_type (generic_mangled_type_name fst ty),
1.75 generic_mangled_type_name snd ty), [])
1.76 - fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
1.77 + fun to_poly_atype (ATerm ((name, []), tys)) =
1.78 + AType (name, map to_poly_atype tys)
1.79 | to_poly_atype _ = raise Fail "unexpected type abstraction"
1.80 val to_atype =
1.81 if is_type_enc_polymorphic type_enc then to_poly_atype
1.82 @@ -1000,7 +1002,7 @@
1.83 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
1.84 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
1.85 | to_fo _ _ = raise Fail "unexpected type abstraction"
1.86 - fun to_ho (ty as ATerm ((s, _), tys)) =
1.87 + fun to_ho (ty as ATerm (((s, _), []), tys)) =
1.88 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
1.89 | to_ho _ = raise Fail "unexpected type abstraction"
1.90 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
1.91 @@ -1033,7 +1035,7 @@
1.92 fun parse_mangled_type x =
1.93 (parse_mangled_ident
1.94 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
1.95 - [] >> ATerm) x
1.96 + [] >> (ATerm o apfst (rpair []))) x
1.97 and parse_mangled_types x =
1.98 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
1.99
1.100 @@ -1731,7 +1733,7 @@
1.101
1.102 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
1.103 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
1.104 - else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
1.105 + else AAtom (ATerm ((`I tptp_equal, []), [tm1, tm2])))
1.106 |> mk_aquant AForall bounds
1.107 |> close_formula_universally
1.108 |> bound_tvars type_enc true atomic_Ts
1.109 @@ -1951,16 +1953,17 @@
1.110 |> mangle_type_args_in_iterm type_enc, tm)
1.111
1.112 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1.113 - | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1.114 - accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1.115 + | is_var_positively_naked_in_term name _ (ATerm (((s, _), _), tms)) accum =
1.116 + accum orelse
1.117 + (is_tptp_equal s andalso member (op =) tms (ATerm ((name, []), [])))
1.118 | is_var_positively_naked_in_term _ _ _ _ = true
1.119
1.120 fun is_var_positively_naked_or_undercover_in_term thy name pos tm accum =
1.121 is_var_positively_naked_in_term name pos tm accum orelse
1.122 let
1.123 - val var = ATerm (name, [])
1.124 + val var = ATerm ((name, []), [])
1.125 fun is_undercover (ATerm (_, [])) = false
1.126 - | is_undercover (ATerm ((s, _), tms)) =
1.127 + | is_undercover (ATerm (((s, _), _), tms)) =
1.128 let
1.129 val ary = length tms
1.130 val cover = type_arg_cover thy s ary
1.131 @@ -1991,7 +1994,11 @@
1.132 | should_generate_tag_bound_decl _ _ _ _ _ = false
1.133
1.134 fun mk_aterm type_enc name T_args args =
1.135 - ATerm (name, map_filter (ho_term_for_type_arg type_enc) T_args @ args)
1.136 +(* ### FIXME
1.137 + if is_type_enc_polymorphic type_enc then
1.138 + ATerm ((name, map (ho_type_from_typ type_enc false 0) T_args), args)
1.139 + else *)
1.140 + ATerm ((name, []), map_filter (ho_term_for_type_arg type_enc) T_args @ args)
1.141
1.142 fun do_bound_type ctxt mono type_enc =
1.143 case type_enc of
1.144 @@ -2003,7 +2010,7 @@
1.145 IConst (type_tag, T --> T, [T])
1.146 |> mangle_type_args_in_iterm type_enc
1.147 |> ho_term_from_iterm ctxt mono type_enc pos
1.148 - |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
1.149 + |> (fn ATerm ((s, tys), tms) => ATerm ((s, tys), tms @ [tm])
1.150 | _ => raise Fail "unexpected lambda-abstraction")
1.151 and ho_term_from_iterm ctxt mono type_enc pos =
1.152 let
1.153 @@ -2051,9 +2058,9 @@
1.154 |> do_term pos |> AAtom |> SOME
1.155 else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
1.156 let
1.157 - val var = ATerm (name, [])
1.158 + val var = ATerm ((name, []), [])
1.159 val tagged_var = tag_with_type ctxt mono type_enc pos T var
1.160 - in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
1.161 + in SOME (AAtom (ATerm ((`I tptp_equal, []), [tagged_var, var]))) end
1.162 else
1.163 NONE
1.164 fun do_formula pos (AQuant (q, xs, phi)) =
1.165 @@ -2101,7 +2108,7 @@
1.166
1.167 fun formula_line_for_class_rel_clause type_enc
1.168 ({name, subclass, superclass, ...} : class_rel_clause) =
1.169 - let val ty_arg = ATerm (tvar_a_name, []) in
1.170 + let val ty_arg = ATerm ((tvar_a_name, []), []) in
1.171 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
1.172 AConn (AImplies,
1.173 [type_class_formula type_enc subclass ty_arg,
1.174 @@ -2112,7 +2119,7 @@
1.175 end
1.176
1.177 fun formula_from_arity_atom type_enc (class, t, args) =
1.178 - ATerm (t, map (fn arg => ATerm (arg, [])) args)
1.179 + ATerm ((t, []), map (fn arg => ATerm ((arg, []), [])) args)
1.180 |> type_class_formula type_enc class
1.181
1.182 fun formula_line_for_arity_clause type_enc
1.183 @@ -2318,7 +2325,7 @@
1.184 NONE, isabelle_info inductiveN helper_rank)
1.185
1.186 fun formula_line_for_tags_mono_type ctxt mono type_enc T =
1.187 - let val x_var = ATerm (`make_bound_var "X", []) in
1.188 + let val x_var = ATerm ((`make_bound_var "X", []), []) in
1.189 Formula (tags_sym_formula_prefix ^
1.190 ascii_of (mangled_type type_enc T),
1.191 Axiom,
1.192 @@ -2402,7 +2409,7 @@
1.193 val (role, maybe_negate) = honor_conj_sym_role in_conj
1.194 val (arg_Ts, res_T) = chop_fun ary T
1.195 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
1.196 - val bounds = bound_names |> map (fn name => ATerm (name, []))
1.197 + val bounds = bound_names |> map (fn name => ATerm ((name, []), []))
1.198 val cst = mk_aterm type_enc (s, s') T_args
1.199 val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
1.200 val should_encode = should_encode_type ctxt mono level
1.201 @@ -2586,9 +2593,9 @@
1.202 #> fold do_type tys
1.203 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
1.204 | do_type (ATyAbs (_, ty)) = do_type ty
1.205 - fun do_term pred_sym (ATerm (name as (s, _), tms)) =
1.206 + fun do_term pred_sym (ATerm ((name as (s, _), tys), tms)) =
1.207 do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
1.208 - #> fold (do_term false) tms
1.209 + #> fold do_type tys #> fold (do_term false) tms
1.210 | do_term _ (AAbs (((_, ty), tm), args)) =
1.211 do_type ty #> do_term false tm #> fold (do_term false) args
1.212 fun do_formula (AQuant (_, xs, phi)) =
1.213 @@ -2738,7 +2745,7 @@
1.214 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
1.215 fun atp_problem_selection_weights problem =
1.216 let
1.217 - fun add_term_weights weight (ATerm (s, tms)) =
1.218 + fun add_term_weights weight (ATerm ((s, _), tms)) =
1.219 is_tptp_user_symbol s ? Symtab.default (s, weight)
1.220 #> fold (add_term_weights weight) tms
1.221 | add_term_weights weight (AAbs ((_, tm), args)) =
1.222 @@ -2778,11 +2785,11 @@
1.223 fun may_be_predicator s =
1.224 member (op =) [predicator_name, prefixed_predicator_name] s
1.225
1.226 -fun strip_predicator (tm as ATerm (s, [tm'])) =
1.227 +fun strip_predicator (tm as ATerm ((s, _), [tm'])) =
1.228 if may_be_predicator s then tm' else tm
1.229 | strip_predicator tm = tm
1.230
1.231 -fun make_head_roll (ATerm (s, tms)) =
1.232 +fun make_head_roll (ATerm ((s, _), tms)) =
1.233 if may_be_app s tms then make_head_roll (hd tms) ||> append (tl tms)
1.234 else (s, tms)
1.235 | make_head_roll _ = ("", [])
1.236 @@ -2809,7 +2816,7 @@
1.237 Graph.default_node (s, ())
1.238 #> Graph.default_node (s', ())
1.239 #> Graph.add_edge_acyclic (s, s')
1.240 - fun add_term_deps head (ATerm (s, args)) =
1.241 + fun add_term_deps head (ATerm ((s, _), args)) =
1.242 if is_tptp_user_symbol head then
1.243 (if is_tptp_user_symbol s then perhaps (try (add_edge s head)) else I)
1.244 #> fold (add_term_deps head) args
1.245 @@ -2827,7 +2834,7 @@
1.246 else
1.247 I
1.248 | add_intro_deps _ _ = I
1.249 - fun add_atom_eq_deps (SOME true) (ATerm (s, [lhs as _, rhs])) =
1.250 + fun add_atom_eq_deps (SOME true) (ATerm ((s, _), [lhs as _, rhs])) =
1.251 if is_tptp_equal s then
1.252 case make_head_roll lhs of
1.253 (head, args as _ :: _) => fold (add_term_deps head) (rhs :: args)