--- a/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200
@@ -97,10 +97,11 @@
fun inference_term [] = NONE
| inference_term ss =
- ATerm ("inference",
- [ATerm ("isabelle", []),
- ATerm (tptp_empty_list, []),
- ATerm (tptp_empty_list, map (fn s => ATerm (s, [])) ss)])
+ ATerm (("inference", []),
+ [ATerm (("isabelle", []), []),
+ ATerm ((tptp_empty_list, []), []),
+ ATerm ((tptp_empty_list, []),
+ map (fn s => ATerm ((s, []), [])) ss)])
|> SOME
fun inference infers ident =
these (AList.lookup (op =) infers ident) |> inference_term
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200
@@ -8,7 +8,7 @@
signature ATP_PROBLEM =
sig
datatype ('a, 'b) ho_term =
- ATerm of 'a * ('a, 'b) ho_term list |
+ ATerm of ('a * 'b list) * ('a, 'b) ho_term list |
AAbs of (('a * 'b) * ('a, 'b) ho_term) * ('a, 'b) ho_term list
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIff
@@ -140,7 +140,7 @@
(** ATP problem **)
datatype ('a, 'b) ho_term =
- ATerm of 'a * ('a, 'b) ho_term list |
+ ATerm of ('a * 'b list) * ('a, 'b) ho_term list |
AAbs of (('a * 'b) * ('a, 'b) ho_term) * ('a, 'b) ho_term list
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIff
@@ -230,17 +230,17 @@
(* Currently, only SPASS 3.8ds can process Isabelle metainformation. *)
fun isabelle_info status rank =
[] |> rank <> default_rank
- ? cons (ATerm (isabelle_info_prefix ^ rankN,
- [ATerm (string_of_int rank, [])]))
- |> status <> "" ? cons (ATerm (isabelle_info_prefix ^ status, []))
+ ? cons (ATerm ((isabelle_info_prefix ^ rankN, []),
+ [ATerm ((string_of_int rank, []), [])]))
+ |> status <> "" ? cons (ATerm ((isabelle_info_prefix ^ status, []), []))
-fun extract_isabelle_status (ATerm (s, []) :: _) =
+fun extract_isabelle_status (ATerm ((s, []), []) :: _) =
try (unprefix isabelle_info_prefix) s
| extract_isabelle_status _ = NONE
fun extract_isabelle_rank (tms as _ :: _) =
(case List.last tms of
- ATerm (_, [ATerm (rank, [])]) => the (Int.fromString rank)
+ ATerm ((_, []), [ATerm ((rank, []), [])]) => the (Int.fromString rank)
| _ => default_rank)
| extract_isabelle_rank _ = default_rank
@@ -379,8 +379,9 @@
else
"")
-fun tptp_string_for_term _ (ATerm (s, [])) = s
- | tptp_string_for_term format (ATerm (s, ts)) =
+fun tptp_string_for_term _ (ATerm ((s, []), [])) = s
+ | tptp_string_for_term _ (ATerm ((s, tys), [])) = s (* ### FIXME *)
+ | tptp_string_for_term format (ATerm ((s, tys), ts)) = (* ### FIXME *)
(if s = tptp_empty_list then
(* used for lists in the optional "source" field of a derivation *)
"[" ^ commas (map (tptp_string_for_term format) ts) ^ "]"
@@ -418,7 +419,7 @@
tptp_string_for_formula format phi
|> enclose "(" ")"
| tptp_string_for_formula format
- (AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) =
+ (AConn (ANot, [AAtom (ATerm (("=" (* tptp_equal *), []), ts))])) =
space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
(map (tptp_string_for_term format) ts)
|> is_format_higher_order format ? enclose "(" ")"
@@ -475,11 +476,12 @@
| NONE => s
else
s
- fun str_for_term top_level (ATerm (s, tms)) =
+ fun str_for_term top_level (ATerm ((s, tys), tms)) =
(if is_tptp_equal s then "equal" |> suffix_tag top_level
else if s = tptp_true then "true"
else if s = tptp_false then "false"
else s) ^
+ (if null tys then "" else "<...>") (* ### FIXME *) ^
(if null tms then ""
else "(" ^ commas (map (str_for_term false) tms) ^ ")")
| str_for_term _ _ = raise Fail "unexpected term in first-order format"
@@ -597,13 +599,14 @@
fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true
| is_problem_line_negated _ = false
-fun is_problem_line_cnf_ueq (Formula (_, _, AAtom (ATerm ((s, _), _)), _, _)) =
+fun is_problem_line_cnf_ueq
+ (Formula (_, _, AAtom (ATerm (((s, _), _), _)), _, _)) =
is_tptp_equal s
| is_problem_line_cnf_ueq _ = false
-fun open_conjecture_term (ATerm ((s, s'), tms)) =
- ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')
- else (s, s'), tms |> map open_conjecture_term)
+fun open_conjecture_term (ATerm (((s, s'), tys), tms)) =
+ ATerm ((if is_tptp_variable s then (s |> Name.desymbolize false, s')
+ else (s, s'), tys), tms |> map open_conjecture_term)
| open_conjecture_term _ = raise Fail "unexpected higher-order term"
fun open_formula conj =
let
@@ -797,8 +800,9 @@
| 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
+ fun nice_term (ATerm ((name, tys), ts)) =
+ nice_name name ##>> pool_map nice_type tys ##>> pool_map nice_term ts
+ #>> ATerm
| nice_term (AAbs (((name, ty), tm), args)) =
nice_name name ##>> nice_type ty ##>> nice_term tm
##>> pool_map nice_term args #>> AAbs
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
@@ -889,15 +889,15 @@
| add_sorts_on_tvar _ = I
fun type_class_formula type_enc class arg =
- AAtom (ATerm (class, arg ::
+ AAtom (ATerm ((class, []), arg ::
(case type_enc of
Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
- [ATerm (TYPE_name, [arg])]
+ [ATerm ((TYPE_name, []), [arg])]
| _ => [])))
fun formulas_for_types type_enc add_sorts_on_typ Ts =
[] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
|> map (fn (class, name) =>
- type_class_formula type_enc class (ATerm (name, [])))
+ type_class_formula type_enc class (ATerm ((name, []), [])))
fun mk_aconns c phis =
let val (phis', phi') = split_last phis in
@@ -919,7 +919,7 @@
| add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
in mk_aquant AForall (add_formula_vars [] phi []) phi end
-fun add_term_vars bounds (ATerm (name as (s, _), tms)) =
+fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
(if is_tptp_variable s andalso
not (String.isPrefix tvar_prefix s) andalso
not (member (op =) bounds name) then
@@ -948,17 +948,17 @@
fun ho_term_from_typ type_enc =
let
fun term (Type (s, Ts)) =
- 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 = fused_infinite_type_name andalso
- is_type_enc_native type_enc 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, _)) = ATerm (tvar_name x, [])
+ 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 = fused_infinite_type_name andalso
+ is_type_enc_native type_enc 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, _)) = ATerm ((tvar_name x, []), [])
in term end
fun ho_term_for_type_arg type_enc T =
@@ -970,8 +970,9 @@
val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
-fun generic_mangled_type_name f (ATerm (name, [])) = f name
- | generic_mangled_type_name f (ATerm (name, tys)) =
+(* ### FIXME: insane *)
+fun generic_mangled_type_name f (ATerm ((name, _), [])) = f name
+ | generic_mangled_type_name f (ATerm ((name, _), tys)) =
f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
^ ")"
| generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
@@ -991,7 +992,8 @@
fun to_mangled_atype ty =
AType ((make_native_type (generic_mangled_type_name fst ty),
generic_mangled_type_name snd ty), [])
- fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
+ fun to_poly_atype (ATerm ((name, []), tys)) =
+ AType (name, map to_poly_atype tys)
| to_poly_atype _ = raise Fail "unexpected type abstraction"
val to_atype =
if is_type_enc_polymorphic type_enc then to_poly_atype
@@ -1000,7 +1002,7 @@
fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
| to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
| to_fo _ _ = raise Fail "unexpected type abstraction"
- fun to_ho (ty as ATerm ((s, _), tys)) =
+ fun to_ho (ty as ATerm (((s, _), []), tys)) =
if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
| to_ho _ = raise Fail "unexpected type abstraction"
in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
@@ -1033,7 +1035,7 @@
fun parse_mangled_type x =
(parse_mangled_ident
-- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
- [] >> ATerm) x
+ [] >> (ATerm o apfst (rpair []))) x
and parse_mangled_types x =
(parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
@@ -1731,7 +1733,7 @@
fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
(if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
- else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
+ else AAtom (ATerm ((`I tptp_equal, []), [tm1, tm2])))
|> mk_aquant AForall bounds
|> close_formula_universally
|> bound_tvars type_enc true atomic_Ts
@@ -1951,16 +1953,17 @@
|> mangle_type_args_in_iterm type_enc, tm)
fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
- | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
- accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
+ | is_var_positively_naked_in_term name _ (ATerm (((s, _), _), tms)) accum =
+ accum orelse
+ (is_tptp_equal s andalso member (op =) tms (ATerm ((name, []), [])))
| is_var_positively_naked_in_term _ _ _ _ = true
fun is_var_positively_naked_or_undercover_in_term thy name pos tm accum =
is_var_positively_naked_in_term name pos tm accum orelse
let
- val var = ATerm (name, [])
+ val var = ATerm ((name, []), [])
fun is_undercover (ATerm (_, [])) = false
- | is_undercover (ATerm ((s, _), tms)) =
+ | is_undercover (ATerm (((s, _), _), tms)) =
let
val ary = length tms
val cover = type_arg_cover thy s ary
@@ -1991,7 +1994,11 @@
| should_generate_tag_bound_decl _ _ _ _ _ = false
fun mk_aterm type_enc name T_args args =
- ATerm (name, map_filter (ho_term_for_type_arg type_enc) T_args @ args)
+(* ### FIXME
+ if is_type_enc_polymorphic type_enc then
+ ATerm ((name, map (ho_type_from_typ type_enc false 0) T_args), args)
+ else *)
+ ATerm ((name, []), map_filter (ho_term_for_type_arg type_enc) T_args @ args)
fun do_bound_type ctxt mono type_enc =
case type_enc of
@@ -2003,7 +2010,7 @@
IConst (type_tag, T --> T, [T])
|> mangle_type_args_in_iterm type_enc
|> ho_term_from_iterm ctxt mono type_enc pos
- |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
+ |> (fn ATerm ((s, tys), tms) => ATerm ((s, tys), tms @ [tm])
| _ => raise Fail "unexpected lambda-abstraction")
and ho_term_from_iterm ctxt mono type_enc pos =
let
@@ -2051,9 +2058,9 @@
|> do_term pos |> AAtom |> SOME
else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
let
- val var = ATerm (name, [])
+ val var = ATerm ((name, []), [])
val tagged_var = tag_with_type ctxt mono type_enc pos T var
- in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
+ in SOME (AAtom (ATerm ((`I tptp_equal, []), [tagged_var, var]))) end
else
NONE
fun do_formula pos (AQuant (q, xs, phi)) =
@@ -2101,7 +2108,7 @@
fun formula_line_for_class_rel_clause type_enc
({name, subclass, superclass, ...} : class_rel_clause) =
- let val ty_arg = ATerm (tvar_a_name, []) in
+ let val ty_arg = ATerm ((tvar_a_name, []), []) in
Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
AConn (AImplies,
[type_class_formula type_enc subclass ty_arg,
@@ -2112,7 +2119,7 @@
end
fun formula_from_arity_atom type_enc (class, t, args) =
- ATerm (t, map (fn arg => ATerm (arg, [])) args)
+ ATerm ((t, []), map (fn arg => ATerm ((arg, []), [])) args)
|> type_class_formula type_enc class
fun formula_line_for_arity_clause type_enc
@@ -2318,7 +2325,7 @@
NONE, isabelle_info inductiveN helper_rank)
fun formula_line_for_tags_mono_type ctxt mono type_enc T =
- let val x_var = ATerm (`make_bound_var "X", []) in
+ let val x_var = ATerm ((`make_bound_var "X", []), []) in
Formula (tags_sym_formula_prefix ^
ascii_of (mangled_type type_enc T),
Axiom,
@@ -2402,7 +2409,7 @@
val (role, maybe_negate) = honor_conj_sym_role in_conj
val (arg_Ts, res_T) = chop_fun ary T
val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
- val bounds = bound_names |> map (fn name => ATerm (name, []))
+ val bounds = bound_names |> map (fn name => ATerm ((name, []), []))
val cst = mk_aterm type_enc (s, s') T_args
val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
val should_encode = should_encode_type ctxt mono level
@@ -2586,9 +2593,9 @@
#> fold do_type tys
| do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
| do_type (ATyAbs (_, ty)) = do_type ty
- fun do_term pred_sym (ATerm (name as (s, _), tms)) =
+ fun do_term pred_sym (ATerm ((name as (s, _), tys), tms)) =
do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
- #> fold (do_term false) 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
fun do_formula (AQuant (_, xs, phi)) =
@@ -2738,7 +2745,7 @@
(* Weights are from 0.0 (most important) to 1.0 (least important). *)
fun atp_problem_selection_weights problem =
let
- fun add_term_weights weight (ATerm (s, tms)) =
+ fun add_term_weights weight (ATerm ((s, _), tms)) =
is_tptp_user_symbol s ? Symtab.default (s, weight)
#> fold (add_term_weights weight) tms
| add_term_weights weight (AAbs ((_, tm), args)) =
@@ -2778,11 +2785,11 @@
fun may_be_predicator s =
member (op =) [predicator_name, prefixed_predicator_name] s
-fun strip_predicator (tm as ATerm (s, [tm'])) =
+fun strip_predicator (tm as ATerm ((s, _), [tm'])) =
if may_be_predicator s then tm' else tm
| strip_predicator tm = tm
-fun make_head_roll (ATerm (s, tms)) =
+fun make_head_roll (ATerm ((s, _), tms)) =
if may_be_app s tms then make_head_roll (hd tms) ||> append (tl tms)
else (s, tms)
| make_head_roll _ = ("", [])
@@ -2809,7 +2816,7 @@
Graph.default_node (s, ())
#> Graph.default_node (s', ())
#> Graph.add_edge_acyclic (s, s')
- fun add_term_deps head (ATerm (s, args)) =
+ fun add_term_deps head (ATerm ((s, _), args)) =
if is_tptp_user_symbol head then
(if is_tptp_user_symbol s then perhaps (try (add_edge s head)) else I)
#> fold (add_term_deps head) args
@@ -2827,7 +2834,7 @@
else
I
| add_intro_deps _ _ = I
- fun add_atom_eq_deps (SOME true) (ATerm (s, [lhs as _, rhs])) =
+ fun add_atom_eq_deps (SOME true) (ATerm ((s, _), [lhs as _, rhs])) =
if is_tptp_equal s then
case make_head_roll lhs of
(head, args as _ :: _) => fold (add_term_deps head) (rhs :: args)
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 26 11:14:39 2012 +0200
@@ -54,7 +54,8 @@
val scan_general_id : string list -> string * string list
val satallax_unsat_coreN : string
val parse_formula :
- string list -> (string, 'a, (string, 'a) ho_term) formula * string list
+ string list
+ -> (string, 'a, (string, 'a) ho_term) formula * string list
val atp_proof_from_tstplike_proof : string problem -> string -> string proof
val clean_up_atp_proof_dependencies : string proof -> string proof
val map_term_names_in_atp_proof :
@@ -251,7 +252,7 @@
File_Source of string * string option |
Inference_Source of string * string list
-val dummy_phi = AAtom (ATerm ("", []))
+val dummy_phi = AAtom (ATerm (("", []), []))
val dummy_inference = Inference_Source ("", [])
(* "skip_term" is there to cope with Waldmeister nonsense such as
@@ -271,7 +272,7 @@
|| skip_term >> K dummy_inference) x
fun list_app (f, args) =
- fold (fn arg => fn f => ATerm (tptp_app, [f, arg])) args f
+ fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f
(* We currently ignore TFF and THF types. *)
fun parse_type_stuff x =
@@ -280,7 +281,7 @@
($$ "(" |-- parse_term --| $$ ")" --| parse_type_stuff
|| scan_general_id --| parse_type_stuff
-- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
- >> ATerm) x
+ >> (ATerm o apfst (rpair []))) x
and parse_term x =
(parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x
and parse_terms x =
@@ -291,7 +292,7 @@
-- parse_term)
>> (fn (u1, NONE) => AAtom u1
| (u1, SOME (neg, u2)) =>
- AAtom (ATerm ("equal", [u1, u2])) |> is_some neg ? mk_anot)) x
+ AAtom (ATerm (("equal", []), [u1, u2])) |> is_some neg ? mk_anot)) x
(* TPTP formulas are fully parenthesized, so we don't need to worry about
operator precedence. *)
@@ -323,7 +324,7 @@
--| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
>> (fn ((q, ts), phi) =>
(* We ignore TFF and THF types for now. *)
- AQuant (q, map (fn ATerm (s, _) => (s, NONE)) ts, phi))) x
+ AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x
val parse_tstp_extra_arguments =
Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term))
@@ -336,7 +337,7 @@
fun is_same_term subst tm1 tm2 =
let
fun do_term_pair _ NONE = NONE
- | do_term_pair (ATerm (s1, tm1), ATerm (s2, tm2)) (SOME subst) =
+ | do_term_pair (ATerm ((s1, _), tm1), ATerm ((s2, _), tm2)) (SOME subst) =
case pairself is_tptp_variable (s1, s2) of
(true, true) =>
(case AList.lookup (op =) subst s1 of
@@ -358,10 +359,10 @@
| is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) =
c1 = c2 andalso length phis1 = length phis2 andalso
forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2)
- | is_same_formula comm subst (AAtom (tm1 as ATerm ("equal", [tm11, tm12])))
- (AAtom tm2) =
+ | is_same_formula comm subst
+ (AAtom (tm1 as ATerm (("equal", []), [tm11, tm12]))) (AAtom tm2) =
is_same_term subst tm1 tm2 orelse
- (comm andalso is_same_term subst (ATerm ("equal", [tm12, tm11])) tm2)
+ (comm andalso is_same_term subst (ATerm (("equal", []), [tm12, tm11])) tm2)
| is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2
| is_same_formula _ _ _ _ = false
@@ -373,7 +374,7 @@
problem |> maps snd |> map_filter (matching_formula_line_identifier phi)
|> try (single o hd) |> the_default []
-fun commute_eq (AAtom (ATerm (s, tms))) = AAtom (ATerm (s, rev tms))
+fun commute_eq (AAtom (ATerm ((s, []), tms))) = AAtom (ATerm ((s, []), rev tms))
| commute_eq _ = raise Fail "expected equation"
(* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>,
@@ -416,7 +417,7 @@
(case phi of
AConn (AIff, [phi1 as AAtom _, phi2]) =>
Definition_Step (name, phi1, phi2)
- | AAtom (ATerm ("equal", _)) =>
+ | AAtom (ATerm (("equal", []), _)) =>
(* Vampire's equality proxy axiom *)
Inference_Step (name, phi, rule, map (rpair []) deps)
| _ => mk_step ())
@@ -438,7 +439,7 @@
fun parse_decorated_atom x =
(parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x
-fun mk_horn ([], []) = AAtom (ATerm ("c_False", []))
+fun mk_horn ([], []) = AAtom (ATerm (("c_False", []), []))
| mk_horn ([], pos_lits) = foldr1 (uncurry (mk_aconn AOr)) pos_lits
| mk_horn (neg_lits, []) = mk_anot (foldr1 (uncurry (mk_aconn AAnd)) neg_lits)
| mk_horn (neg_lits, pos_lits) =
@@ -501,8 +502,8 @@
fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
-fun map_term_names_in_term f (ATerm (s, ts)) =
- ATerm (f s, map (map_term_names_in_term f) ts)
+fun map_term_names_in_term f (ATerm ((s, tys), ts)) =
+ ATerm ((f s, tys), map (map_term_names_in_term f) ts)
fun map_term_names_in_formula f (AQuant (q, xs, phi)) =
AQuant (q, xs, map_term_names_in_formula f phi)
| map_term_names_in_formula f (AConn (c, phis)) =
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Jun 26 11:14:39 2012 +0200
@@ -331,7 +331,7 @@
(* Type variables are given the basic sort "HOL.type". Some will later be
constrained by information from type literals, or by type inference. *)
-fun typ_from_atp ctxt (u as ATerm (a, us)) =
+fun typ_from_atp ctxt (u as ATerm ((a, _), us)) =
let val Ts = map (typ_from_atp ctxt) us in
case unprefix_and_unascii type_const_prefix a of
SOME b => Type (invert_const b, Ts)
@@ -351,7 +351,7 @@
(* Type class literal applied to a type. Returns triple of polarity, class,
type. *)
-fun type_constraint_from_term ctxt (u as ATerm (a, us)) =
+fun type_constraint_from_term ctxt (u as ATerm ((a, _), us)) =
case (unprefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
(SOME b, [T]) => (b, T)
| _ => raise HO_TERM [u]
@@ -404,7 +404,7 @@
val var_index = if textual then 0 else 1
fun do_term extra_ts opt_T u =
case u of
- ATerm (s, us) =>
+ ATerm ((s, _), us) =>
if String.isPrefix native_type_prefix s then
@{const True} (* ignore TPTP type information *)
else if s = tptp_equal then
@@ -492,7 +492,7 @@
in list_comb (t, ts) end
in do_term [] end
-fun term_from_atom ctxt textual sym_tab pos (u as ATerm (s, _)) =
+fun term_from_atom ctxt textual sym_tab pos (u as ATerm ((s, _), _)) =
if String.isPrefix class_prefix s then
add_type_constraint pos (type_constraint_from_term ctxt u)
#> pair @{const True}
--- a/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200
@@ -138,7 +138,7 @@
val prepare_helper =
Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
-fun metis_term_from_atp type_enc (ATerm (s, tms)) =
+fun metis_term_from_atp type_enc (ATerm ((s, []), tms)) =
if is_tptp_variable s then
Metis_Term.Var (Metis_Name.fromString s)
else
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 26 11:14:39 2012 +0200
@@ -42,9 +42,10 @@
| _ => (s, false)
fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) =
let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in
- ATerm (s, tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
+ ATerm ((s, []), tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
end
- | atp_term_from_metis _ (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
+ | atp_term_from_metis _ (Metis_Term.Var s) =
+ ATerm ((Metis_Name.toString s, []), [])
fun hol_term_from_metis ctxt type_enc sym_tab =
atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE
@@ -52,7 +53,7 @@
fun atp_literal_from_metis type_enc (pos, atom) =
atom |> Metis_Term.Fn |> atp_term_from_metis type_enc
|> AAtom |> not pos ? mk_anot
-fun atp_clause_from_metis _ [] = AAtom (ATerm (tptp_false, []))
+fun atp_clause_from_metis _ [] = AAtom (ATerm ((tptp_false, []), []))
| atp_clause_from_metis type_enc lits =
lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr