# HG changeset patch # User blanchet # Date 1340702079 -7200 # Node ID 9aa0fad4e864e9157d24dc0376c2f49b6e8a4a67 # Parent 1016664b8feb44de2800ae7e4f9e921cef453ae4 added type arguments to "ATerm" constructor -- but don't use them yet diff -r 1016664b8feb -r 9aa0fad4e864 src/HOL/TPTP/atp_theory_export.ML --- 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 diff -r 1016664b8feb -r 9aa0fad4e864 src/HOL/Tools/ATP/atp_problem.ML --- 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 diff -r 1016664b8feb -r 9aa0fad4e864 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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) diff -r 1016664b8feb -r 9aa0fad4e864 src/HOL/Tools/ATP/atp_proof.ML --- 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)\(, , @@ -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)) = diff -r 1016664b8feb -r 9aa0fad4e864 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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} diff -r 1016664b8feb -r 9aa0fad4e864 src/HOL/Tools/Metis/metis_generate.ML --- 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 diff -r 1016664b8feb -r 9aa0fad4e864 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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