--- 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 =
--- 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
--- 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)\(<num>, <formula_role>, <cnf_formula> <annotations>\).
+(* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <annotations>\).
The <num> 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: <num>[0:<inference><annotations>]
- <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
+ <atoms> || <atoms> -> <atoms>. *)
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