author blanchet Sun, 01 May 2011 18:37:24 +0200 changeset 42527 6a9458524f01 parent 42526 46d485f8d144 child 42528 a15f0db2bcaf
reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
```--- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
@@ -16,11 +16,10 @@
AAtom of 'b
type 'a uniform_formula = ('a, 'a fo_term) formula

-  datatype logic = Fof | Tff
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
-  type 'a problem_line =
-    logic * string * formula_kind * ('a, 'a fo_term) formula
-    * string fo_term option
+  datatype 'a problem_line =
+    Formula of string * formula_kind * ('a, 'a fo_term) formula
+               * string fo_term option
type 'a problem = (string * 'a problem_line list) list

val timestamp : unit -> string
@@ -47,11 +46,10 @@
AAtom of 'b
type 'a uniform_formula = ('a, 'a fo_term) formula

-datatype logic = Fof | Tff
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
-type 'a problem_line =
-  logic * string * formula_kind * ('a, 'a fo_term) formula
-  * string fo_term option
+datatype 'a problem_line =
+  Formula of string * formula_kind * ('a, 'a fo_term) formula
+             * string fo_term option
type 'a problem = (string * 'a problem_line list) list

val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
@@ -94,8 +92,14 @@
(map string_for_formula phis) ^ ")"
| string_for_formula (AAtom tm) = string_for_term tm

+fun formula_needs_typed_logic (AQuant (_, xs, phi)) =
+    exists (is_some o snd) xs orelse formula_needs_typed_logic phi
+  | formula_needs_typed_logic (AConn (_, phis)) =
+    exists formula_needs_typed_logic phis
+  | formula_needs_typed_logic (AAtom _) = false
+
fun string_for_problem_line use_conjecture_for_hypotheses
-                            (logic, ident, kind, phi, source) =
+                            (Formula (ident, kind, phi, source)) =
let
val (kind, phi) =
if kind = Hypothesis andalso use_conjecture_for_hypotheses then
@@ -103,7 +107,7 @@
else
(kind, phi)
in
-    (case logic of Fof => "fof" | Tff => "tff") ^
+    (if formula_needs_typed_logic phi then "tff" else "fof") ^
"(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
string_for_formula phi ^ ")" ^
(case source of
@@ -190,8 +194,8 @@
| nice_formula (AConn (c, phis)) =
pool_map nice_formula phis #>> curry AConn c
| nice_formula (AAtom tm) = nice_term tm #>> AAtom
-fun nice_problem_line (logic, ident, kind, phi, source) =
-  nice_formula phi #>> (fn phi => (logic, ident, kind, phi, source))
+fun nice_problem_line (Formula (ident, kind, phi, source)) =
+  nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source))
fun nice_problem problem =
pool_map nice_problem_line lines #>> pair heading) problem```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -315,9 +315,10 @@
fun var s = ATerm (`I s, [])
fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
in
-         [(Fof, helper_prefix ^ ascii_of "ti_ti", Axiom,
-           AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
-           |> close_formula_universally, NONE)]
+         [Formula (helper_prefix ^ ascii_of "ti_ti", Axiom,
+                   AAtom (ATerm (`I "equal",
+                                 [tag (tag (var "Y")), tag (var "Y")]))
+                   |> close_formula_universally, NONE)]
end
else
[])
@@ -502,23 +503,20 @@
(formula_for_combformula ctxt type_sys
(close_combformula_universally combformula))

-fun logic_for_type_sys Many_Typed = Tff
-  | logic_for_type_sys _ = Fof
-
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
fun problem_line_for_fact ctxt prefix type_sys
(j, formula as {name, kind, ...}) =
-  (logic_for_type_sys type_sys, prefix ^ string_of_int j ^ "_" ^ ascii_of name,
-   kind, formula_for_fact ctxt type_sys formula, NONE)
+  Formula (prefix ^ string_of_int j ^ "_" ^ ascii_of name,
+           kind, formula_for_fact ctxt type_sys formula, NONE)

fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
superclass, ...}) =
let val ty_arg = ATerm (("T", "T"), []) in
-    (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom,
-     AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
-                       AAtom (ATerm (superclass, [ty_arg]))]), NONE)
+    Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
+             AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
+                               AAtom (ATerm (superclass, [ty_arg]))]), NONE)
end

fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
@@ -528,25 +526,26 @@

fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
...}) =
-  (Fof, arity_clause_prefix ^ ascii_of name, Axiom,
-   mk_ahorn (map (formula_for_fo_literal o apfst not
-                  o fo_literal_for_arity_literal) premLits)
-            (formula_for_fo_literal
-                 (fo_literal_for_arity_literal conclLit)), NONE)
+  Formula (arity_clause_prefix ^ ascii_of name, Axiom,
+           mk_ahorn (map (formula_for_fo_literal o apfst not
+                          o fo_literal_for_arity_literal) premLits)
+                    (formula_for_fo_literal
+                         (fo_literal_for_arity_literal conclLit)), NONE)

fun problem_line_for_conjecture ctxt type_sys
({name, kind, combformula, ...} : translated_formula) =
-  (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind,
-   formula_for_combformula ctxt type_sys
-                           (close_combformula_universally combformula), NONE)
+  Formula (conjecture_prefix ^ name, kind,
+           formula_for_combformula ctxt type_sys
+                                   (close_combformula_universally combformula),
+           NONE)

fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) =
ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture
|> map fo_literal_for_type_literal

fun problem_line_for_free_type j lit =
-  (Fof, tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit,
-   NONE)
+  Formula (tfree_prefix ^ string_of_int j, Hypothesis,
+           formula_for_fo_literal lit, NONE)
fun problem_lines_for_free_types type_sys facts =
let
val litss = map (free_type_literals type_sys) facts
@@ -574,7 +573,7 @@
| consider_formula (AConn (_, phis)) = fold consider_formula phis
| consider_formula (AAtom tm) = consider_term true tm

-fun consider_problem_line (_, _, _, phi, _) = consider_formula phi
+fun consider_problem_line (Formula (_, _, phi, _)) = consider_formula phi
fun consider_problem problem = fold (fold consider_problem_line o snd) problem

(* needed for helper facts if the problem otherwise does not involve equality *)
@@ -584,7 +583,8 @@
if explicit_apply then
NONE
else
-    SOME (Symtab.empty |> Symtab.default equal_entry |> consider_problem problem)
+    SOME (Symtab.empty |> Symtab.default equal_entry
+                       |> consider_problem problem)

fun min_arity_of thy type_sys NONE s =
(if s = "equal" orelse s = type_tag_name orelse
@@ -665,8 +665,9 @@
|> repair_predicates_in_term pred_sym_tab)
in aux #> close_formula_universally end

-fun repair_problem_line thy type_sys sym_tab (logic, ident, kind, phi, source) =
-  (logic, ident, kind, repair_formula thy type_sys sym_tab phi, source)
+fun repair_problem_line thy type_sys sym_tab
+                        (Formula (ident, kind, phi, source)) =
+  Formula (ident, kind, repair_formula thy type_sys sym_tab phi, source)
fun repair_problem thy = map o apsnd o map oo repair_problem_line thy

val factsN = "Relevant facts"
@@ -700,7 +701,8 @@
val sym_tab = sym_table_for_problem explicit_apply problem
val problem = problem |> repair_problem thy type_sys sym_tab
val helper_facts =
-      get_helper_facts ctxt type_sys (maps (map #4 o snd) problem)
+      problem |> maps (map (fn Formula (_, _, phi, _) => phi) o snd)
+              |> get_helper_facts ctxt type_sys
val helper_lines =
helper_facts
|>> map (pair 0
@@ -726,7 +728,7 @@
fun add_term_weights weight (ATerm (s, tms)) =
(not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)