# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID f9d402d144d4f2e5af46ef438ef7825d52a94bd7
# Parent  024920b65ce2683feecd8e1159178cc6faf8a8d2
declare TFF types so that SNARK can be used with types

diff -r 024920b65ce2 -r f9d402d144d4 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,7 +18,7 @@
   datatype logic = Fof | Tff
   datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
   datatype 'a problem_line =
-    Type_Decl of string * 'a * 'a list * 'a |
+    Decl of string * 'a * 'a list * 'a |
     Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula
                * string fo_term option * string fo_term option
   type 'a problem = (string * 'a problem_line list) list
@@ -49,7 +49,7 @@
 datatype logic = Fof | Tff
 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
 datatype 'a problem_line =
-  Type_Decl of string * 'a * 'a list * 'a |
+  Decl of string * 'a * 'a list * 'a |
   Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula
              * string fo_term option * string fo_term option
 type 'a problem = (string * 'a problem_line list) list
@@ -99,7 +99,7 @@
   | 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)) =
+fun string_for_problem_line _ (Decl (ident, sym, arg_tys, res_ty)) =
     "tff(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
     string_for_symbol_type arg_tys res_ty ^ ").\n"
   | string_for_problem_line use_conjecture_for_hypotheses
@@ -201,11 +201,11 @@
   | 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 (Type_Decl (ident, sym, arg_tys, res_ty)) =
+fun nice_problem_line (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))
+    #>> (fn ((sym, arg_tys), res_ty) => Decl (ident, sym, arg_tys, res_ty))
   | nice_problem_line (Formula (logic, ident, kind, phi, source, useful_info)) =
     nice_formula phi
     #>> (fn phi => Formula (logic, ident, kind, phi, source, useful_info))
diff -r 024920b65ce2 -r f9d402d144d4 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
@@ -237,6 +237,7 @@
 
 fun parse_term x =
   (scan_general_id
+     --| Scan.option ($$ ":" -- scan_general_id) (* ignore TFF types for now *)
      -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms)
                        --| $$ ")") []
      --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
diff -r 024920b65ce2 -r f9d402d144d4 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
@@ -45,11 +45,12 @@
 open Metis_Translate
 open Sledgehammer_Util
 
+val type_decl_prefix = "type_"
+val sym_decl_prefix = "sym_"
 val fact_prefix = "fact_"
 val conjecture_prefix = "conj_"
 val helper_prefix = "help_"
-val type_decl_prefix = "type_"
-val class_rel_clause_prefix = "clrel_";
+val class_rel_clause_prefix = "crel_";
 val arity_clause_prefix = "arity_"
 val tfree_prefix = "tfree_"
 
@@ -61,6 +62,7 @@
 fun make_type ty = type_prefix ^ ascii_of ty
 
 (* official TPTP TFF syntax *)
+val tff_type_of_types = "$tType"
 val tff_bool_type = "$o"
 
 (* Freshness almost guaranteed! *)
@@ -778,14 +780,14 @@
      | _ => ([], f ty))
   | strip_and_map_combtyp f ty = ([], f ty)
 
-fun type_decl_line_for_const_entry ctxt type_sys hrepairs s (s', ty_args, ty) =
+fun sym_decl_line_for_const_entry ctxt type_sys hrepairs s (s', ty_args, ty) =
   if type_sys = Many_Typed then
     let
       val (arg_tys, res_ty) = strip_and_map_combtyp mangled_combtyp ty
       val (s, s') = (s, s') |> mangled_const_name ty_args
     in
-      Type_Decl (type_decl_prefix ^ ascii_of s, (s, s'), arg_tys,
-                 if is_pred_sym hrepairs s then `I tff_bool_type else res_ty)
+      Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_tys,
+            if is_pred_sym hrepairs s then `I tff_bool_type else res_ty)
     end
   else
     let
@@ -796,7 +798,7 @@
       val bound_tms =
         map (fn (name, ty) => CombConst (name, the ty, [])) bounds
     in
-      Formula (Fof, type_decl_prefix ^ ascii_of s, Axiom,
+      Formula (Fof, sym_decl_prefix ^ ascii_of s, Axiom,
                CombConst ((s, s'), ty, ty_args)
                |> fold (curry (CombApp o swap)) bound_tms
                |> type_pred_combatom type_sys res_ty
@@ -804,13 +806,31 @@
                |> formula_for_combformula ctxt type_sys,
                NONE, NONE)
     end
-fun type_decl_lines_for_const ctxt type_sys hrepairs (s, xs) =
-  map (type_decl_line_for_const_entry ctxt type_sys hrepairs s) xs
+fun sym_decl_lines_for_const ctxt type_sys hrepairs (s, xs) =
+  map (sym_decl_line_for_const_entry ctxt type_sys hrepairs s) xs
+
+fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
+    union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi
+  | add_tff_types_in_formula (AConn (_, phis)) =
+    fold add_tff_types_in_formula phis
+  | add_tff_types_in_formula (AAtom _) = I
 
-val type_declsN = "Type declarations"
+fun add_tff_types_in_problem_line (Decl (_, _, arg_tys, res_ty)) =
+    union (op =) (res_ty :: arg_tys)
+  | add_tff_types_in_problem_line (Formula (_, _, _, phi, _, _)) =
+    add_tff_types_in_formula phi
+
+fun tff_types_in_problem problem =
+  fold (fold add_tff_types_in_problem_line o snd) problem []
+
+fun problem_line_for_tff_type (s, s') =
+  Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tff_type_of_types)
+
+val type_declsN = "Types"
+val sym_declsN = "Symbols"
 val factsN = "Relevant facts"
 val class_relsN = "Class relationships"
-val aritiesN = "Arity declarations"
+val aritiesN = "Arities"
 val helpersN = "Helper facts"
 val conjsN = "Conjectures"
 val free_typesN = "Type variables"
@@ -832,6 +852,7 @@
        Flotter hack. *)
     val problem =
       [(type_declsN, []),
+       (sym_declsN, []),
        (factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
                     (0 upto length facts - 1 ~~ facts)),
        (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
@@ -845,17 +866,24 @@
               |> get_helper_facts ctxt type_sys
               |>> map (hrepair_fact type_sys hrepairs)
     val const_tab = const_table_for_facts type_sys hrepairs (conjs @ facts)
-    val type_decl_lines =
-      Symtab.fold_rev (append o type_decl_lines_for_const ctxt type_sys
-                                                          hrepairs)
+    val sym_decl_lines =
+      Symtab.fold_rev (append o sym_decl_lines_for_const ctxt type_sys hrepairs)
                       const_tab []
     val helper_lines =
       helper_facts
       |>> map (pair 0 #> problem_line_for_fact ctxt helper_prefix type_sys)
       |> op @
-    val (problem, pool) =
+    val problem =
       problem |> fold (AList.update (op =))
-                      [(type_declsN, type_decl_lines), (helpersN, helper_lines)]
+                      [(sym_declsN, sym_decl_lines),
+                       (helpersN, helper_lines)]
+    val type_decl_lines =
+      if type_sys = Many_Typed then
+        problem |> tff_types_in_problem |> map problem_line_for_tff_type
+      else
+        []
+    val (problem, pool) =
+      problem |> AList.update (op =) (type_declsN, type_decl_lines)
               |> nice_atp_problem readable_names
   in
     (problem,