# HG changeset patch # User blanchet # Date 1280306749 -7200 # Node ID ecae87b9b9c486bb17bd4b31d18aa112147bf9fd # Parent df99f022751df5e3be73f181121d457cb1c55d51 renaming diff -r df99f022751d -r ecae87b9b9c4 src/HOL/Tools/ATP_Manager/atp_problem.ML --- a/src/HOL/Tools/ATP_Manager/atp_problem.ML Wed Jul 28 10:06:06 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_problem.ML Wed Jul 28 10:45:49 2010 +0200 @@ -13,7 +13,7 @@ datatype ('a, 'b) formula = AQuant of quantifier * 'a list * ('a, 'b) formula | AConn of connective * ('a, 'b) formula list | - APred of 'b + AAtom of 'b datatype kind = Axiom | Conjecture datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula @@ -40,7 +40,7 @@ datatype ('a, 'b) formula = AQuant of quantifier * 'a list * ('a, 'b) formula | AConn of connective * ('a, 'b) formula list | - APred of 'b + AAtom of 'b datatype kind = Axiom | Conjecture datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula @@ -64,14 +64,14 @@ fun string_for_formula (AQuant (q, xs, phi)) = string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^ string_for_formula phi - | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) = + | string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) = space_implode " != " (map string_for_term ts) | string_for_formula (AConn (c, [phi])) = string_for_connective c ^ " " ^ string_for_formula phi | string_for_formula (AConn (c, phis)) = "(" ^ space_implode (" " ^ string_for_connective c ^ " ") (map string_for_formula phis) ^ ")" - | string_for_formula (APred tm) = string_for_term tm + | string_for_formula (AAtom tm) = string_for_term tm fun string_for_problem_line (Fof (ident, kind, phi)) = "fof(" ^ ident ^ ", " ^ @@ -140,7 +140,7 @@ #>> (fn (xs, phi) => AQuant (q, xs, phi)) | nice_formula (AConn (c, phis)) = pool_map nice_formula phis #>> curry AConn c - | nice_formula (APred tm) = nice_term tm #>> APred + | nice_formula (AAtom tm) = nice_term tm #>> AAtom fun nice_problem_line (Fof (ident, kind, phi)) = nice_formula phi #>> (fn phi => Fof (ident, kind, phi)) fun nice_problem problem = diff -r df99f022751d -r ecae87b9b9c4 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 10:06:06 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 10:45:49 2010 +0200 @@ -231,7 +231,7 @@ | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => do_conn bs AIff t1 t2 | _ => (fn ts => do_term bs (Envir.eta_contract t) - |>> APred ||> union (op =) ts) + |>> AAtom ||> union (op =) ts) in do_formula [] end (* Converts an elim-rule into an equivalent theorem that does not have the @@ -336,7 +336,7 @@ | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2] fun count_combformula (AQuant (_, _, phi)) = count_combformula phi | count_combformula (AConn (_, phis)) = fold count_combformula phis - | count_combformula (APred tm) = count_combterm tm + | count_combformula (AAtom tm) = count_combterm tm fun count_fol_formula (FOLFormula {combformula, ...}) = count_combformula combformula @@ -418,7 +418,7 @@ | fo_literal_for_type_literal (TyLitFree (class, name)) = (true, ATerm (class, [ATerm (name, [])])) -fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot +fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot fun fo_term_for_combterm full_types = let @@ -446,7 +446,7 @@ let fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (APred tm) = APred (fo_term_for_combterm full_types tm) + | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm) in aux end fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) = @@ -463,8 +463,8 @@ (ClassRelClause {axiom_name, subclass, superclass, ...}) = let val ty_arg = ATerm (("T", "T"), []) in Fof (ascii_of axiom_name, Axiom, - AConn (AImplies, [APred (ATerm (subclass, [ty_arg])), - APred (ATerm (superclass, [ty_arg]))])) + AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), + AAtom (ATerm (superclass, [ty_arg]))])) end fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = @@ -515,7 +515,7 @@ #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts fun consider_formula (AQuant (_, _, phi)) = consider_formula phi | consider_formula (AConn (_, phis)) = fold consider_formula phis - | consider_formula (APred tm) = consider_term true tm + | consider_formula (AAtom tm) = consider_term true tm fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi fun consider_problem problem = fold (fold consider_problem_line o snd) problem @@ -601,7 +601,7 @@ fun formula_vars bounds (AQuant (q, xs, phi)) = formula_vars (xs @ bounds) phi | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis - | formula_vars bounds (APred tm) = term_vars bounds tm + | formula_vars bounds (AAtom tm) = term_vars bounds tm in case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) end @@ -610,8 +610,8 @@ let fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (APred tm) = - APred (tm |> repair_applications_in_term thy full_types const_tab + | aux (AAtom tm) = + AAtom (tm |> repair_applications_in_term thy full_types const_tab |> repair_predicates_in_term const_tab) in aux #> explicit_forall ? close_universally end diff -r df99f022751d -r ecae87b9b9c4 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jul 28 10:06:06 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jul 28 10:45:49 2010 +0200 @@ -117,13 +117,13 @@ and parse_terms pool x = (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x -fun parse_predicate_term pool = +fun parse_atom pool = parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term pool) - >> (fn (u, NONE) => APred u - | (u1, SOME (NONE, u2)) => APred (ATerm ("c_equal", [u1, u2])) + >> (fn (u, NONE) => AAtom u + | (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2])) | (u1, SOME (SOME _, u2)) => - mk_anot (APred (ATerm ("c_equal", [u1, u2])))) + mk_anot (AAtom (ATerm ("c_equal", [u1, u2])))) fun fo_term_head (ATerm (s, _)) = s @@ -136,7 +136,7 @@ -- parse_formula pool >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi)) || $$ "~" |-- parse_formula pool >> mk_anot - || parse_predicate_term pool) + || parse_atom pool) -- Scan.option ((Scan.this_string "=>" >> K AImplies || Scan.this_string "<=>" >> K AIff || Scan.this_string "<~>" >> K ANotIff @@ -153,7 +153,7 @@ --| Scan.option ($$ "," |-- parse_generalized_terms) >> (fn g => ints_of_generalized_term g [])) [] -(* Syntax: (fof|cnf)\(, , \). +(* Syntax: (fof|cnf)\(, , \). The could be an identifier, but we assume integers. *) fun parse_tstp_line pool = ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(") @@ -163,9 +163,9 @@ case role of "definition" => (case phi of - AConn (AIff, [phi1 as APred _, phi2]) => + AConn (AIff, [phi1 as AAtom _, phi2]) => Definition (num, phi1, phi2) - | APred (ATerm ("$$e", _)) => + | AAtom (ATerm ("$$e", _)) => Inference (num, phi, deps) (* Vampire's equality proxy axiom *) | _ => raise Fail "malformed definition") | _ => Inference (num, phi, deps)) @@ -182,10 +182,10 @@ (* It is not clear why some literals are followed by sequences of stars and/or pluses. We ignore them. *) -fun parse_decorated_predicate_term pool = - parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ") +fun parse_decorated_atom pool = + parse_atom pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ") -fun mk_horn ([], []) = APred (ATerm ("c_False", [])) +fun mk_horn ([], []) = AAtom (ATerm ("c_False", [])) | mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits | mk_horn (neg_lits, []) = mk_anot (foldr1 (mk_aconn AAnd) neg_lits) | mk_horn (neg_lits, pos_lits) = @@ -193,13 +193,13 @@ foldr1 (mk_aconn AOr) pos_lits) fun parse_horn_clause pool = - Scan.repeat (parse_decorated_predicate_term pool) --| $$ "|" --| $$ "|" - -- Scan.repeat (parse_decorated_predicate_term pool) --| $$ "-" --| $$ ">" - -- Scan.repeat (parse_decorated_predicate_term pool) + Scan.repeat (parse_decorated_atom pool) --| $$ "|" --| $$ "|" + -- Scan.repeat (parse_decorated_atom pool) --| $$ "-" --| $$ ">" + -- Scan.repeat (parse_decorated_atom pool) >> (mk_horn o apfst (op @)) (* Syntax: [0:] - || -> . *) + || -> . *) fun parse_spass_line pool = scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "." @@ -396,7 +396,7 @@ | AOr => s_disj | AImplies => s_imp | AIff => s_iff) - | APred tm => term_from_pred thy full_types tfrees pos tm + | AAtom tm => term_from_pred thy full_types tfrees pos tm | _ => raise FORMULA [phi] in repair_tvar_sorts (do_formula true phi Vartab.empty) end