1.1 --- a/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200
1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200
1.3 @@ -97,10 +97,11 @@
1.4
1.5 fun inference_term [] = NONE
1.6 | inference_term ss =
1.7 - ATerm ("inference",
1.8 - [ATerm ("isabelle", []),
1.9 - ATerm (tptp_empty_list, []),
1.10 - ATerm (tptp_empty_list, map (fn s => ATerm (s, [])) ss)])
1.11 + ATerm (("inference", []),
1.12 + [ATerm (("isabelle", []), []),
1.13 + ATerm ((tptp_empty_list, []), []),
1.14 + ATerm ((tptp_empty_list, []),
1.15 + map (fn s => ATerm ((s, []), [])) ss)])
1.16 |> SOME
1.17 fun inference infers ident =
1.18 these (AList.lookup (op =) infers ident) |> inference_term
2.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200
2.3 @@ -8,7 +8,7 @@
2.4 signature ATP_PROBLEM =
2.5 sig
2.6 datatype ('a, 'b) ho_term =
2.7 - ATerm of 'a * ('a, 'b) ho_term list |
2.8 + ATerm of ('a * 'b list) * ('a, 'b) ho_term list |
2.9 AAbs of (('a * 'b) * ('a, 'b) ho_term) * ('a, 'b) ho_term list
2.10 datatype quantifier = AForall | AExists
2.11 datatype connective = ANot | AAnd | AOr | AImplies | AIff
2.12 @@ -140,7 +140,7 @@
2.13 (** ATP problem **)
2.14
2.15 datatype ('a, 'b) ho_term =
2.16 - ATerm of 'a * ('a, 'b) ho_term list |
2.17 + ATerm of ('a * 'b list) * ('a, 'b) ho_term list |
2.18 AAbs of (('a * 'b) * ('a, 'b) ho_term) * ('a, 'b) ho_term list
2.19 datatype quantifier = AForall | AExists
2.20 datatype connective = ANot | AAnd | AOr | AImplies | AIff
2.21 @@ -230,17 +230,17 @@
2.22 (* Currently, only SPASS 3.8ds can process Isabelle metainformation. *)
2.23 fun isabelle_info status rank =
2.24 [] |> rank <> default_rank
2.25 - ? cons (ATerm (isabelle_info_prefix ^ rankN,
2.26 - [ATerm (string_of_int rank, [])]))
2.27 - |> status <> "" ? cons (ATerm (isabelle_info_prefix ^ status, []))
2.28 + ? cons (ATerm ((isabelle_info_prefix ^ rankN, []),
2.29 + [ATerm ((string_of_int rank, []), [])]))
2.30 + |> status <> "" ? cons (ATerm ((isabelle_info_prefix ^ status, []), []))
2.31
2.32 -fun extract_isabelle_status (ATerm (s, []) :: _) =
2.33 +fun extract_isabelle_status (ATerm ((s, []), []) :: _) =
2.34 try (unprefix isabelle_info_prefix) s
2.35 | extract_isabelle_status _ = NONE
2.36
2.37 fun extract_isabelle_rank (tms as _ :: _) =
2.38 (case List.last tms of
2.39 - ATerm (_, [ATerm (rank, [])]) => the (Int.fromString rank)
2.40 + ATerm ((_, []), [ATerm ((rank, []), [])]) => the (Int.fromString rank)
2.41 | _ => default_rank)
2.42 | extract_isabelle_rank _ = default_rank
2.43
2.44 @@ -379,8 +379,9 @@
2.45 else
2.46 "")
2.47
2.48 -fun tptp_string_for_term _ (ATerm (s, [])) = s
2.49 - | tptp_string_for_term format (ATerm (s, ts)) =
2.50 +fun tptp_string_for_term _ (ATerm ((s, []), [])) = s
2.51 + | tptp_string_for_term _ (ATerm ((s, tys), [])) = s (* ### FIXME *)
2.52 + | tptp_string_for_term format (ATerm ((s, tys), ts)) = (* ### FIXME *)
2.53 (if s = tptp_empty_list then
2.54 (* used for lists in the optional "source" field of a derivation *)
2.55 "[" ^ commas (map (tptp_string_for_term format) ts) ^ "]"
2.56 @@ -418,7 +419,7 @@
2.57 tptp_string_for_formula format phi
2.58 |> enclose "(" ")"
2.59 | tptp_string_for_formula format
2.60 - (AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) =
2.61 + (AConn (ANot, [AAtom (ATerm (("=" (* tptp_equal *), []), ts))])) =
2.62 space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
2.63 (map (tptp_string_for_term format) ts)
2.64 |> is_format_higher_order format ? enclose "(" ")"
2.65 @@ -475,11 +476,12 @@
2.66 | NONE => s
2.67 else
2.68 s
2.69 - fun str_for_term top_level (ATerm (s, tms)) =
2.70 + fun str_for_term top_level (ATerm ((s, tys), tms)) =
2.71 (if is_tptp_equal s then "equal" |> suffix_tag top_level
2.72 else if s = tptp_true then "true"
2.73 else if s = tptp_false then "false"
2.74 else s) ^
2.75 + (if null tys then "" else "<...>") (* ### FIXME *) ^
2.76 (if null tms then ""
2.77 else "(" ^ commas (map (str_for_term false) tms) ^ ")")
2.78 | str_for_term _ _ = raise Fail "unexpected term in first-order format"
2.79 @@ -597,13 +599,14 @@
2.80 fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true
2.81 | is_problem_line_negated _ = false
2.82
2.83 -fun is_problem_line_cnf_ueq (Formula (_, _, AAtom (ATerm ((s, _), _)), _, _)) =
2.84 +fun is_problem_line_cnf_ueq
2.85 + (Formula (_, _, AAtom (ATerm (((s, _), _), _)), _, _)) =
2.86 is_tptp_equal s
2.87 | is_problem_line_cnf_ueq _ = false
2.88
2.89 -fun open_conjecture_term (ATerm ((s, s'), tms)) =
2.90 - ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')
2.91 - else (s, s'), tms |> map open_conjecture_term)
2.92 +fun open_conjecture_term (ATerm (((s, s'), tys), tms)) =
2.93 + ATerm ((if is_tptp_variable s then (s |> Name.desymbolize false, s')
2.94 + else (s, s'), tys), tms |> map open_conjecture_term)
2.95 | open_conjecture_term _ = raise Fail "unexpected higher-order term"
2.96 fun open_formula conj =
2.97 let
2.98 @@ -797,8 +800,9 @@
2.99 | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
2.100 | nice_type (ATyAbs (names, ty)) =
2.101 pool_map nice_name names ##>> nice_type ty #>> ATyAbs
2.102 - fun nice_term (ATerm (name, ts)) =
2.103 - nice_name name ##>> pool_map nice_term ts #>> ATerm
2.104 + fun nice_term (ATerm ((name, tys), ts)) =
2.105 + nice_name name ##>> pool_map nice_type tys ##>> pool_map nice_term ts
2.106 + #>> ATerm
2.107 | nice_term (AAbs (((name, ty), tm), args)) =
2.108 nice_name name ##>> nice_type ty ##>> nice_term tm
2.109 ##>> pool_map nice_term args #>> AAbs
3.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
3.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
3.3 @@ -889,15 +889,15 @@
3.4 | add_sorts_on_tvar _ = I
3.5
3.6 fun type_class_formula type_enc class arg =
3.7 - AAtom (ATerm (class, arg ::
3.8 + AAtom (ATerm ((class, []), arg ::
3.9 (case type_enc of
3.10 Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
3.11 - [ATerm (TYPE_name, [arg])]
3.12 + [ATerm ((TYPE_name, []), [arg])]
3.13 | _ => [])))
3.14 fun formulas_for_types type_enc add_sorts_on_typ Ts =
3.15 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
3.16 |> map (fn (class, name) =>
3.17 - type_class_formula type_enc class (ATerm (name, [])))
3.18 + type_class_formula type_enc class (ATerm ((name, []), [])))
3.19
3.20 fun mk_aconns c phis =
3.21 let val (phis', phi') = split_last phis in
3.22 @@ -919,7 +919,7 @@
3.23 | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
3.24 in mk_aquant AForall (add_formula_vars [] phi []) phi end
3.25
3.26 -fun add_term_vars bounds (ATerm (name as (s, _), tms)) =
3.27 +fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
3.28 (if is_tptp_variable s andalso
3.29 not (String.isPrefix tvar_prefix s) andalso
3.30 not (member (op =) bounds name) then
3.31 @@ -948,17 +948,17 @@
3.32 fun ho_term_from_typ type_enc =
3.33 let
3.34 fun term (Type (s, Ts)) =
3.35 - ATerm (case (is_type_enc_higher_order type_enc, s) of
3.36 - (true, @{type_name bool}) => `I tptp_bool_type
3.37 - | (true, @{type_name fun}) => `I tptp_fun_type
3.38 - | _ => if s = fused_infinite_type_name andalso
3.39 - is_type_enc_native type_enc then
3.40 - `I tptp_individual_type
3.41 - else
3.42 - `make_fixed_type_const s,
3.43 - map term Ts)
3.44 - | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
3.45 - | term (TVar (x, _)) = ATerm (tvar_name x, [])
3.46 + ATerm ((case (is_type_enc_higher_order type_enc, s) of
3.47 + (true, @{type_name bool}) => `I tptp_bool_type
3.48 + | (true, @{type_name fun}) => `I tptp_fun_type
3.49 + | _ => if s = fused_infinite_type_name andalso
3.50 + is_type_enc_native type_enc then
3.51 + `I tptp_individual_type
3.52 + else
3.53 + `make_fixed_type_const s,
3.54 + []), map term Ts)
3.55 + | term (TFree (s, _)) = ATerm ((`make_fixed_type_var s, []), [])
3.56 + | term (TVar (x, _)) = ATerm ((tvar_name x, []), [])
3.57 in term end
3.58
3.59 fun ho_term_for_type_arg type_enc T =
3.60 @@ -970,8 +970,9 @@
3.61
3.62 val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
3.63
3.64 -fun generic_mangled_type_name f (ATerm (name, [])) = f name
3.65 - | generic_mangled_type_name f (ATerm (name, tys)) =
3.66 +(* ### FIXME: insane *)
3.67 +fun generic_mangled_type_name f (ATerm ((name, _), [])) = f name
3.68 + | generic_mangled_type_name f (ATerm ((name, _), tys)) =
3.69 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
3.70 ^ ")"
3.71 | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
3.72 @@ -991,7 +992,8 @@
3.73 fun to_mangled_atype ty =
3.74 AType ((make_native_type (generic_mangled_type_name fst ty),
3.75 generic_mangled_type_name snd ty), [])
3.76 - fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
3.77 + fun to_poly_atype (ATerm ((name, []), tys)) =
3.78 + AType (name, map to_poly_atype tys)
3.79 | to_poly_atype _ = raise Fail "unexpected type abstraction"
3.80 val to_atype =
3.81 if is_type_enc_polymorphic type_enc then to_poly_atype
3.82 @@ -1000,7 +1002,7 @@
3.83 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
3.84 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
3.85 | to_fo _ _ = raise Fail "unexpected type abstraction"
3.86 - fun to_ho (ty as ATerm ((s, _), tys)) =
3.87 + fun to_ho (ty as ATerm (((s, _), []), tys)) =
3.88 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
3.89 | to_ho _ = raise Fail "unexpected type abstraction"
3.90 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
3.91 @@ -1033,7 +1035,7 @@
3.92 fun parse_mangled_type x =
3.93 (parse_mangled_ident
3.94 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
3.95 - [] >> ATerm) x
3.96 + [] >> (ATerm o apfst (rpair []))) x
3.97 and parse_mangled_types x =
3.98 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
3.99
3.100 @@ -1731,7 +1733,7 @@
3.101
3.102 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
3.103 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
3.104 - else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
3.105 + else AAtom (ATerm ((`I tptp_equal, []), [tm1, tm2])))
3.106 |> mk_aquant AForall bounds
3.107 |> close_formula_universally
3.108 |> bound_tvars type_enc true atomic_Ts
3.109 @@ -1951,16 +1953,17 @@
3.110 |> mangle_type_args_in_iterm type_enc, tm)
3.111
3.112 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
3.113 - | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
3.114 - accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
3.115 + | is_var_positively_naked_in_term name _ (ATerm (((s, _), _), tms)) accum =
3.116 + accum orelse
3.117 + (is_tptp_equal s andalso member (op =) tms (ATerm ((name, []), [])))
3.118 | is_var_positively_naked_in_term _ _ _ _ = true
3.119
3.120 fun is_var_positively_naked_or_undercover_in_term thy name pos tm accum =
3.121 is_var_positively_naked_in_term name pos tm accum orelse
3.122 let
3.123 - val var = ATerm (name, [])
3.124 + val var = ATerm ((name, []), [])
3.125 fun is_undercover (ATerm (_, [])) = false
3.126 - | is_undercover (ATerm ((s, _), tms)) =
3.127 + | is_undercover (ATerm (((s, _), _), tms)) =
3.128 let
3.129 val ary = length tms
3.130 val cover = type_arg_cover thy s ary
3.131 @@ -1991,7 +1994,11 @@
3.132 | should_generate_tag_bound_decl _ _ _ _ _ = false
3.133
3.134 fun mk_aterm type_enc name T_args args =
3.135 - ATerm (name, map_filter (ho_term_for_type_arg type_enc) T_args @ args)
3.136 +(* ### FIXME
3.137 + if is_type_enc_polymorphic type_enc then
3.138 + ATerm ((name, map (ho_type_from_typ type_enc false 0) T_args), args)
3.139 + else *)
3.140 + ATerm ((name, []), map_filter (ho_term_for_type_arg type_enc) T_args @ args)
3.141
3.142 fun do_bound_type ctxt mono type_enc =
3.143 case type_enc of
3.144 @@ -2003,7 +2010,7 @@
3.145 IConst (type_tag, T --> T, [T])
3.146 |> mangle_type_args_in_iterm type_enc
3.147 |> ho_term_from_iterm ctxt mono type_enc pos
3.148 - |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
3.149 + |> (fn ATerm ((s, tys), tms) => ATerm ((s, tys), tms @ [tm])
3.150 | _ => raise Fail "unexpected lambda-abstraction")
3.151 and ho_term_from_iterm ctxt mono type_enc pos =
3.152 let
3.153 @@ -2051,9 +2058,9 @@
3.154 |> do_term pos |> AAtom |> SOME
3.155 else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
3.156 let
3.157 - val var = ATerm (name, [])
3.158 + val var = ATerm ((name, []), [])
3.159 val tagged_var = tag_with_type ctxt mono type_enc pos T var
3.160 - in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
3.161 + in SOME (AAtom (ATerm ((`I tptp_equal, []), [tagged_var, var]))) end
3.162 else
3.163 NONE
3.164 fun do_formula pos (AQuant (q, xs, phi)) =
3.165 @@ -2101,7 +2108,7 @@
3.166
3.167 fun formula_line_for_class_rel_clause type_enc
3.168 ({name, subclass, superclass, ...} : class_rel_clause) =
3.169 - let val ty_arg = ATerm (tvar_a_name, []) in
3.170 + let val ty_arg = ATerm ((tvar_a_name, []), []) in
3.171 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
3.172 AConn (AImplies,
3.173 [type_class_formula type_enc subclass ty_arg,
3.174 @@ -2112,7 +2119,7 @@
3.175 end
3.176
3.177 fun formula_from_arity_atom type_enc (class, t, args) =
3.178 - ATerm (t, map (fn arg => ATerm (arg, [])) args)
3.179 + ATerm ((t, []), map (fn arg => ATerm ((arg, []), [])) args)
3.180 |> type_class_formula type_enc class
3.181
3.182 fun formula_line_for_arity_clause type_enc
3.183 @@ -2318,7 +2325,7 @@
3.184 NONE, isabelle_info inductiveN helper_rank)
3.185
3.186 fun formula_line_for_tags_mono_type ctxt mono type_enc T =
3.187 - let val x_var = ATerm (`make_bound_var "X", []) in
3.188 + let val x_var = ATerm ((`make_bound_var "X", []), []) in
3.189 Formula (tags_sym_formula_prefix ^
3.190 ascii_of (mangled_type type_enc T),
3.191 Axiom,
3.192 @@ -2402,7 +2409,7 @@
3.193 val (role, maybe_negate) = honor_conj_sym_role in_conj
3.194 val (arg_Ts, res_T) = chop_fun ary T
3.195 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
3.196 - val bounds = bound_names |> map (fn name => ATerm (name, []))
3.197 + val bounds = bound_names |> map (fn name => ATerm ((name, []), []))
3.198 val cst = mk_aterm type_enc (s, s') T_args
3.199 val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
3.200 val should_encode = should_encode_type ctxt mono level
3.201 @@ -2586,9 +2593,9 @@
3.202 #> fold do_type tys
3.203 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
3.204 | do_type (ATyAbs (_, ty)) = do_type ty
3.205 - fun do_term pred_sym (ATerm (name as (s, _), tms)) =
3.206 + fun do_term pred_sym (ATerm ((name as (s, _), tys), tms)) =
3.207 do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
3.208 - #> fold (do_term false) tms
3.209 + #> fold do_type tys #> fold (do_term false) tms
3.210 | do_term _ (AAbs (((_, ty), tm), args)) =
3.211 do_type ty #> do_term false tm #> fold (do_term false) args
3.212 fun do_formula (AQuant (_, xs, phi)) =
3.213 @@ -2738,7 +2745,7 @@
3.214 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
3.215 fun atp_problem_selection_weights problem =
3.216 let
3.217 - fun add_term_weights weight (ATerm (s, tms)) =
3.218 + fun add_term_weights weight (ATerm ((s, _), tms)) =
3.219 is_tptp_user_symbol s ? Symtab.default (s, weight)
3.220 #> fold (add_term_weights weight) tms
3.221 | add_term_weights weight (AAbs ((_, tm), args)) =
3.222 @@ -2778,11 +2785,11 @@
3.223 fun may_be_predicator s =
3.224 member (op =) [predicator_name, prefixed_predicator_name] s
3.225
3.226 -fun strip_predicator (tm as ATerm (s, [tm'])) =
3.227 +fun strip_predicator (tm as ATerm ((s, _), [tm'])) =
3.228 if may_be_predicator s then tm' else tm
3.229 | strip_predicator tm = tm
3.230
3.231 -fun make_head_roll (ATerm (s, tms)) =
3.232 +fun make_head_roll (ATerm ((s, _), tms)) =
3.233 if may_be_app s tms then make_head_roll (hd tms) ||> append (tl tms)
3.234 else (s, tms)
3.235 | make_head_roll _ = ("", [])
3.236 @@ -2809,7 +2816,7 @@
3.237 Graph.default_node (s, ())
3.238 #> Graph.default_node (s', ())
3.239 #> Graph.add_edge_acyclic (s, s')
3.240 - fun add_term_deps head (ATerm (s, args)) =
3.241 + fun add_term_deps head (ATerm ((s, _), args)) =
3.242 if is_tptp_user_symbol head then
3.243 (if is_tptp_user_symbol s then perhaps (try (add_edge s head)) else I)
3.244 #> fold (add_term_deps head) args
3.245 @@ -2827,7 +2834,7 @@
3.246 else
3.247 I
3.248 | add_intro_deps _ _ = I
3.249 - fun add_atom_eq_deps (SOME true) (ATerm (s, [lhs as _, rhs])) =
3.250 + fun add_atom_eq_deps (SOME true) (ATerm ((s, _), [lhs as _, rhs])) =
3.251 if is_tptp_equal s then
3.252 case make_head_roll lhs of
3.253 (head, args as _ :: _) => fold (add_term_deps head) (rhs :: args)
4.1 --- a/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 26 11:14:39 2012 +0200
4.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 26 11:14:39 2012 +0200
4.3 @@ -54,7 +54,8 @@
4.4 val scan_general_id : string list -> string * string list
4.5 val satallax_unsat_coreN : string
4.6 val parse_formula :
4.7 - string list -> (string, 'a, (string, 'a) ho_term) formula * string list
4.8 + string list
4.9 + -> (string, 'a, (string, 'a) ho_term) formula * string list
4.10 val atp_proof_from_tstplike_proof : string problem -> string -> string proof
4.11 val clean_up_atp_proof_dependencies : string proof -> string proof
4.12 val map_term_names_in_atp_proof :
4.13 @@ -251,7 +252,7 @@
4.14 File_Source of string * string option |
4.15 Inference_Source of string * string list
4.16
4.17 -val dummy_phi = AAtom (ATerm ("", []))
4.18 +val dummy_phi = AAtom (ATerm (("", []), []))
4.19 val dummy_inference = Inference_Source ("", [])
4.20
4.21 (* "skip_term" is there to cope with Waldmeister nonsense such as
4.22 @@ -271,7 +272,7 @@
4.23 || skip_term >> K dummy_inference) x
4.24
4.25 fun list_app (f, args) =
4.26 - fold (fn arg => fn f => ATerm (tptp_app, [f, arg])) args f
4.27 + fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f
4.28
4.29 (* We currently ignore TFF and THF types. *)
4.30 fun parse_type_stuff x =
4.31 @@ -280,7 +281,7 @@
4.32 ($$ "(" |-- parse_term --| $$ ")" --| parse_type_stuff
4.33 || scan_general_id --| parse_type_stuff
4.34 -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
4.35 - >> ATerm) x
4.36 + >> (ATerm o apfst (rpair []))) x
4.37 and parse_term x =
4.38 (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x
4.39 and parse_terms x =
4.40 @@ -291,7 +292,7 @@
4.41 -- parse_term)
4.42 >> (fn (u1, NONE) => AAtom u1
4.43 | (u1, SOME (neg, u2)) =>
4.44 - AAtom (ATerm ("equal", [u1, u2])) |> is_some neg ? mk_anot)) x
4.45 + AAtom (ATerm (("equal", []), [u1, u2])) |> is_some neg ? mk_anot)) x
4.46
4.47 (* TPTP formulas are fully parenthesized, so we don't need to worry about
4.48 operator precedence. *)
4.49 @@ -323,7 +324,7 @@
4.50 --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
4.51 >> (fn ((q, ts), phi) =>
4.52 (* We ignore TFF and THF types for now. *)
4.53 - AQuant (q, map (fn ATerm (s, _) => (s, NONE)) ts, phi))) x
4.54 + AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x
4.55
4.56 val parse_tstp_extra_arguments =
4.57 Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term))
4.58 @@ -336,7 +337,7 @@
4.59 fun is_same_term subst tm1 tm2 =
4.60 let
4.61 fun do_term_pair _ NONE = NONE
4.62 - | do_term_pair (ATerm (s1, tm1), ATerm (s2, tm2)) (SOME subst) =
4.63 + | do_term_pair (ATerm ((s1, _), tm1), ATerm ((s2, _), tm2)) (SOME subst) =
4.64 case pairself is_tptp_variable (s1, s2) of
4.65 (true, true) =>
4.66 (case AList.lookup (op =) subst s1 of
4.67 @@ -358,10 +359,10 @@
4.68 | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) =
4.69 c1 = c2 andalso length phis1 = length phis2 andalso
4.70 forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2)
4.71 - | is_same_formula comm subst (AAtom (tm1 as ATerm ("equal", [tm11, tm12])))
4.72 - (AAtom tm2) =
4.73 + | is_same_formula comm subst
4.74 + (AAtom (tm1 as ATerm (("equal", []), [tm11, tm12]))) (AAtom tm2) =
4.75 is_same_term subst tm1 tm2 orelse
4.76 - (comm andalso is_same_term subst (ATerm ("equal", [tm12, tm11])) tm2)
4.77 + (comm andalso is_same_term subst (ATerm (("equal", []), [tm12, tm11])) tm2)
4.78 | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2
4.79 | is_same_formula _ _ _ _ = false
4.80
4.81 @@ -373,7 +374,7 @@
4.82 problem |> maps snd |> map_filter (matching_formula_line_identifier phi)
4.83 |> try (single o hd) |> the_default []
4.84
4.85 -fun commute_eq (AAtom (ATerm (s, tms))) = AAtom (ATerm (s, rev tms))
4.86 +fun commute_eq (AAtom (ATerm ((s, []), tms))) = AAtom (ATerm ((s, []), rev tms))
4.87 | commute_eq _ = raise Fail "expected equation"
4.88
4.89 (* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>,
4.90 @@ -416,7 +417,7 @@
4.91 (case phi of
4.92 AConn (AIff, [phi1 as AAtom _, phi2]) =>
4.93 Definition_Step (name, phi1, phi2)
4.94 - | AAtom (ATerm ("equal", _)) =>
4.95 + | AAtom (ATerm (("equal", []), _)) =>
4.96 (* Vampire's equality proxy axiom *)
4.97 Inference_Step (name, phi, rule, map (rpair []) deps)
4.98 | _ => mk_step ())
4.99 @@ -438,7 +439,7 @@
4.100 fun parse_decorated_atom x =
4.101 (parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x
4.102
4.103 -fun mk_horn ([], []) = AAtom (ATerm ("c_False", []))
4.104 +fun mk_horn ([], []) = AAtom (ATerm (("c_False", []), []))
4.105 | mk_horn ([], pos_lits) = foldr1 (uncurry (mk_aconn AOr)) pos_lits
4.106 | mk_horn (neg_lits, []) = mk_anot (foldr1 (uncurry (mk_aconn AAnd)) neg_lits)
4.107 | mk_horn (neg_lits, pos_lits) =
4.108 @@ -501,8 +502,8 @@
4.109
4.110 fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
4.111
4.112 -fun map_term_names_in_term f (ATerm (s, ts)) =
4.113 - ATerm (f s, map (map_term_names_in_term f) ts)
4.114 +fun map_term_names_in_term f (ATerm ((s, tys), ts)) =
4.115 + ATerm ((f s, tys), map (map_term_names_in_term f) ts)
4.116 fun map_term_names_in_formula f (AQuant (q, xs, phi)) =
4.117 AQuant (q, xs, map_term_names_in_formula f phi)
4.118 | map_term_names_in_formula f (AConn (c, phis)) =
5.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Jun 26 11:14:39 2012 +0200
5.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Jun 26 11:14:39 2012 +0200
5.3 @@ -331,7 +331,7 @@
5.4
5.5 (* Type variables are given the basic sort "HOL.type". Some will later be
5.6 constrained by information from type literals, or by type inference. *)
5.7 -fun typ_from_atp ctxt (u as ATerm (a, us)) =
5.8 +fun typ_from_atp ctxt (u as ATerm ((a, _), us)) =
5.9 let val Ts = map (typ_from_atp ctxt) us in
5.10 case unprefix_and_unascii type_const_prefix a of
5.11 SOME b => Type (invert_const b, Ts)
5.12 @@ -351,7 +351,7 @@
5.13
5.14 (* Type class literal applied to a type. Returns triple of polarity, class,
5.15 type. *)
5.16 -fun type_constraint_from_term ctxt (u as ATerm (a, us)) =
5.17 +fun type_constraint_from_term ctxt (u as ATerm ((a, _), us)) =
5.18 case (unprefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
5.19 (SOME b, [T]) => (b, T)
5.20 | _ => raise HO_TERM [u]
5.21 @@ -404,7 +404,7 @@
5.22 val var_index = if textual then 0 else 1
5.23 fun do_term extra_ts opt_T u =
5.24 case u of
5.25 - ATerm (s, us) =>
5.26 + ATerm ((s, _), us) =>
5.27 if String.isPrefix native_type_prefix s then
5.28 @{const True} (* ignore TPTP type information *)
5.29 else if s = tptp_equal then
5.30 @@ -492,7 +492,7 @@
5.31 in list_comb (t, ts) end
5.32 in do_term [] end
5.33
5.34 -fun term_from_atom ctxt textual sym_tab pos (u as ATerm (s, _)) =
5.35 +fun term_from_atom ctxt textual sym_tab pos (u as ATerm ((s, _), _)) =
5.36 if String.isPrefix class_prefix s then
5.37 add_type_constraint pos (type_constraint_from_term ctxt u)
5.38 #> pair @{const True}
6.1 --- a/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200
6.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200
6.3 @@ -138,7 +138,7 @@
6.4 val prepare_helper =
6.5 Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
6.6
6.7 -fun metis_term_from_atp type_enc (ATerm (s, tms)) =
6.8 +fun metis_term_from_atp type_enc (ATerm ((s, []), tms)) =
6.9 if is_tptp_variable s then
6.10 Metis_Term.Var (Metis_Name.fromString s)
6.11 else
7.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 26 11:14:39 2012 +0200
7.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 26 11:14:39 2012 +0200
7.3 @@ -42,9 +42,10 @@
7.4 | _ => (s, false)
7.5 fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) =
7.6 let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in
7.7 - ATerm (s, tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
7.8 + ATerm ((s, []), tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
7.9 end
7.10 - | atp_term_from_metis _ (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
7.11 + | atp_term_from_metis _ (Metis_Term.Var s) =
7.12 + ATerm ((Metis_Name.toString s, []), [])
7.13
7.14 fun hol_term_from_metis ctxt type_enc sym_tab =
7.15 atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE
7.16 @@ -52,7 +53,7 @@
7.17 fun atp_literal_from_metis type_enc (pos, atom) =
7.18 atom |> Metis_Term.Fn |> atp_term_from_metis type_enc
7.19 |> AAtom |> not pos ? mk_anot
7.20 -fun atp_clause_from_metis _ [] = AAtom (ATerm (tptp_false, []))
7.21 +fun atp_clause_from_metis _ [] = AAtom (ATerm ((tptp_false, []), []))
7.22 | atp_clause_from_metis type_enc lits =
7.23 lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
7.24