# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID a15f0db2bcaf3a76a0bd60248420359d9fe9c54c
# Parent  6a9458524f0191ac98602085e49fafef10bdea26
added support for TFF type declarations

diff -r 6a9458524f01 -r a15f0db2bcaf 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
@@ -18,6 +18,7 @@
 
   datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
   datatype 'a problem_line =
+    Type_Decl of string * 'a * 'a list * 'a |
     Formula of string * formula_kind * ('a, 'a fo_term) formula
                * string fo_term option
   type 'a problem = (string * 'a problem_line list) list
@@ -48,6 +49,7 @@
 
 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
 datatype 'a problem_line =
+  Type_Decl of string * 'a * 'a list * 'a |
   Formula of string * formula_kind * ('a, 'a fo_term) formula
              * string fo_term option
 type 'a problem = (string * 'a problem_line list) list
@@ -98,22 +100,30 @@
     exists formula_needs_typed_logic phis
   | formula_needs_typed_logic (AAtom _) = false
 
-fun string_for_problem_line use_conjecture_for_hypotheses
+fun string_for_symbol_type [] res_ty = res_ty
+  | string_for_symbol_type [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty
+  | string_for_symbol_type arg_tys res_ty =
+    string_for_symbol_type ["(" ^ space_implode " * " arg_tys ^ ")"] res_ty
+
+fun string_for_problem_line _ (Type_Decl (ident, sym, arg_tys, res_ty)) =
+    "tff(" ^ ident ^ ", type, " ^ sym ^ " : " ^
+    string_for_symbol_type arg_tys res_ty ^ ").\n"
+  | string_for_problem_line use_conjecture_for_hypotheses
                             (Formula (ident, kind, phi, source)) =
-  let
-    val (kind, phi) =
-      if kind = Hypothesis andalso use_conjecture_for_hypotheses then
-        (Conjecture, AConn (ANot, [phi]))
-      else
-        (kind, phi)
-  in
-    (if formula_needs_typed_logic phi then "tff" else "fof") ^
-    "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
-    string_for_formula phi ^ ")" ^
-    (case source of
-       SOME tm => ", " ^ string_for_term tm
-     | NONE => "") ^ ").\n"
-  end
+    let
+      val (kind, phi) =
+        if kind = Hypothesis andalso use_conjecture_for_hypotheses then
+          (Conjecture, AConn (ANot, [phi]))
+        else
+          (kind, phi)
+    in
+      (if formula_needs_typed_logic phi then "tff" else "fof") ^
+      "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
+      string_for_formula phi ^ ")" ^
+      (case source of
+         SOME tm => ", " ^ string_for_term tm
+       | NONE => "") ^ ").\n"
+    end
 fun tptp_strings_for_atp_problem use_conjecture_for_hypotheses problem =
   "% This file was generated by Isabelle (most likely Sledgehammer)\n\
   \% " ^ timestamp () ^ "\n" ::
@@ -194,8 +204,13 @@
   | 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 (Formula (ident, kind, phi, source)) =
-  nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source))
+fun nice_problem_line (Type_Decl (ident, sym, arg_tys, res_ty)) =
+    nice_name sym
+    ##>> pool_map nice_name arg_tys
+    ##>> nice_name res_ty
+    #>> (fn ((sym, arg_tys), res_ty) => Type_Decl (ident, sym, arg_tys, res_ty))
+  | nice_problem_line (Formula (ident, kind, phi, source)) =
+    nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source))
 fun nice_problem problem =
   pool_map (fn (heading, lines) =>
                pool_map nice_problem_line lines #>> pair heading) problem
diff -r 6a9458524f01 -r a15f0db2bcaf 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
@@ -573,7 +573,8 @@
   | consider_formula (AConn (_, phis)) = fold consider_formula phis
   | consider_formula (AAtom tm) = consider_term true tm
 
-fun consider_problem_line (Formula (_, _, phi, _)) = consider_formula phi
+fun consider_problem_line (Type_Decl _) = I
+  | 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 *)
@@ -667,7 +668,8 @@
 
 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)
+    Formula (ident, kind, repair_formula thy type_sys sym_tab phi, source)
+  | repair_problem_line _ _ _ _ = raise Fail "unexpected non-formula"
 fun repair_problem thy = map o apsnd o map oo repair_problem_line thy
 
 val factsN = "Relevant facts"
@@ -701,7 +703,8 @@
     val sym_tab = sym_table_for_problem explicit_apply problem
     val problem = problem |> repair_problem thy type_sys sym_tab
     val helper_facts =
-      problem |> maps (map (fn Formula (_, _, phi, _) => phi) o snd)
+      problem |> maps (map_filter (fn Formula (_, _, phi, _) => SOME phi
+                                    | _ => NONE) o snd)
               |> get_helper_facts ctxt type_sys
     val helper_lines =
       helper_facts
@@ -729,7 +732,8 @@
   (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   #> fold (add_term_weights weight) tms
 fun add_problem_line_weights weight (Formula (_, _, phi, _)) =
-  fold_formula (add_term_weights weight) phi
+    fold_formula (add_term_weights weight) phi
+  | add_problem_line_weights _ _ = I
 
 fun add_conjectures_weights [] = I
   | add_conjectures_weights conjs =