author blanchet Wed, 28 Jul 2010 10:45:49 +0200 changeset 38034 ecae87b9b9c4 parent 38033 df99f022751d child 38035 0ed953eac020
renaming
```--- 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
```