# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID 7a506b0b644f667cb5a36015116a1848518b4e55
# Parent  3df98f0de5a034b963fed00c2e6b808ad205ccbb
distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree

diff -r 3df98f0de5a0 -r 7a506b0b644f src/HOL/Tools/ATP/atp_problem.ML
--- 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,9 +16,11 @@
     AAtom of 'b
   type 'a uniform_formula = ('a, 'a fo_term) formula
 
-  datatype kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
-  datatype 'a problem_line =
-    Fof of string * kind * ('a, 'a fo_term) formula * string fo_term option
+  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
   type 'a problem = (string * 'a problem_line list) list
 
   val timestamp : unit -> string
@@ -45,9 +47,11 @@
   AAtom of 'b
 type 'a uniform_formula = ('a, 'a fo_term) formula
 
-datatype kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
-datatype 'a problem_line =
-  Fof of string * kind * ('a, 'a fo_term) formula * string fo_term option
+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
 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
@@ -88,7 +92,7 @@
   | string_for_formula (AAtom tm) = string_for_term tm
 
 fun string_for_problem_line use_conjecture_for_hypotheses
-                            (Fof (ident, kind, phi, source)) =
+                            (logic, ident, kind, phi, source) =
   let
     val (kind, phi) =
       if kind = Hypothesis andalso use_conjecture_for_hypotheses then
@@ -96,7 +100,8 @@
       else
         (kind, phi)
   in
-    "fof(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
+    (case logic of Fof => "fof" | Tff => "tff") ^
+    "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
     string_for_formula phi ^ ")" ^
     (case source of
        SOME tm => ", " ^ string_for_term tm
@@ -179,8 +184,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 (Fof (ident, kind, phi, source)) =
-  nice_formula phi #>> (fn phi => Fof (ident, kind, phi, source))
+fun nice_problem_line (logic, ident, kind, phi, source) =
+  nice_formula phi #>> (fn phi => (logic, ident, kind, phi, source))
 fun nice_problem problem =
   pool_map (fn (heading, lines) =>
                pool_map nice_problem_line lines #>> pair heading) problem
diff -r 3df98f0de5a0 -r 7a506b0b644f src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
@@ -276,10 +276,11 @@
 
 val vampire_unknown_fact = "unknown"
 
-(* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
+(* Syntax: (cnf|fof|tff)\(<num>, <formula_role>, <formula> <extra_arguments>\).
    The <num> could be an identifier, but we assume integers. *)
 val parse_tstp_line =
-  ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(")
+  ((Scan.this_string "cnf" || Scan.this_string "fof" || Scan.this_string "tff")
+      -- $$ "(")
     |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ ","
     -- parse_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
    >> (fn (((num, role), phi), deps) =>
diff -r 3df98f0de5a0 -r 7a506b0b644f src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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
@@ -54,7 +54,7 @@
 
 type translated_formula =
   {name: string,
-   kind: kind,
+   kind: formula_kind,
    combformula: (name, combterm) formula,
    ctypes_sorts: typ list}
 
@@ -311,9 +311,9 @@
          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)]
+         [(Fof, helper_prefix ^ ascii_of "ti_ti", Axiom,
+           AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
+           |> close_formula_universally, NONE)]
        end
      else
        [])
@@ -498,20 +498,23 @@
            (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, ...}) =
-  Fof (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
-       formula_for_fact ctxt type_sys formula, NONE)
+  (logic_for_type_sys type_sys, 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)
+    (Fof, 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)) =
@@ -521,26 +524,25 @@
 
 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)
+  (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)
 
 fun problem_line_for_conjecture ctxt type_sys
         ({name, kind, combformula, ...} : translated_formula) =
-  Fof (conjecture_prefix ^ name, kind,
-       formula_for_combformula ctxt type_sys
-                               (close_combformula_universally combformula),
-       NONE)
+  (logic_for_type_sys type_sys, 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)
+  (Fof, 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
@@ -568,7 +570,7 @@
   | consider_formula (AConn (_, phis)) = fold consider_formula phis
   | consider_formula (AAtom tm) = consider_term true tm
 
-fun consider_problem_line (Fof (_, _, phi, _)) = consider_formula phi
+fun consider_problem_line (_, _, _, 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 *)
@@ -659,12 +661,10 @@
                   |> repair_predicates_in_term pred_sym_tab)
   in aux #> close_formula_universally end
 
-fun repair_problem_line thy type_sys sym_tab (Fof (ident, kind, phi, source)) =
-  Fof (ident, kind, repair_formula thy type_sys sym_tab phi, source)
+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 thy = map o apsnd o map oo repair_problem_line thy
 
-fun dest_Fof (Fof z) = z
-
 val factsN = "Relevant facts"
 val class_relsN = "Class relationships"
 val aritiesN = "Arity declarations"
@@ -696,7 +696,7 @@
     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 (#3 o dest_Fof) o snd) problem)
+      get_helper_facts ctxt type_sys (maps (map #4 o snd) problem)
     val helper_lines =
       helper_facts
       |>> map (pair 0
@@ -722,7 +722,7 @@
 fun add_term_weights weight (ATerm (s, tms)) =
   (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   #> fold (add_term_weights weight) tms
-fun add_problem_line_weights weight (Fof (_, _, phi, _)) =
+fun add_problem_line_weights weight (_, _, _, phi, _) =
   fold_formula (add_term_weights weight) phi
 
 fun add_conjectures_weights [] = I