# HG changeset patch
# User blanchet
# Date 1368631644 -7200
# Node ID 8dbe623a7804f2c052d315b3dc5262d9bab9f47b
# Parent  26aecb553c7432a6bf9f1ae80cbd203b759075ce
added datatype declaration syntax for next-gen SPASS

diff -r 26aecb553c74 -r 8dbe623a7804 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Wed May 15 12:13:38 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed May 15 17:27:24 2013 +0200
@@ -50,6 +50,8 @@
     Class_Decl of string * 'a * 'a list |
     Type_Decl of string * 'a * int |
     Sym_Decl of string * 'a * 'a ho_type |
+    Datatype_Decl of string * ('a * 'a list) list * 'a ho_type
+                     * ('a, 'a ho_type) ho_term list |
     Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
     Formula of (string * string) * formula_role
                * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
@@ -190,6 +192,8 @@
   Class_Decl of string * 'a * 'a list |
   Type_Decl of string * 'a * int |
   Sym_Decl of string * 'a * 'a ho_type |
+  Datatype_Decl of string * ('a * 'a list) list * 'a ho_type
+                   * ('a, 'a ho_type) ho_term list |
   Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
   Formula of (string * string) * formula_role
              * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
@@ -512,6 +516,14 @@
 
 val dfg_class_inter = space_implode " & "
 
+fun dfg_string_for_term (ATerm ((s, tys), tms)) =
+    s ^
+    (if null tys then ""
+     else "<" ^ commas (map (string_for_type (DFG Polymorphic)) tys) ^ ">") ^
+    (if null tms then ""
+     else "(" ^ commas (map dfg_string_for_term tms) ^ ")")
+  | dfg_string_for_term _ = raise Fail "unexpected atom in first-order format"
+
 fun dfg_string_for_formula poly gen_simp info =
   let
     val str_for_typ = string_for_type (DFG poly)
@@ -531,16 +543,15 @@
         | NONE => s
       else
         s
-    fun str_for_term top_level (ATerm ((s, tys), tms)) =
-        (if is_tptp_equal s then "equal" |> suffix_tag top_level
-         else if s = tptp_true then "true"
-         else if s = tptp_false then "false"
-         else s) ^
-        (if null tys then ""
-         else "<" ^ commas (map (string_for_type (DFG poly)) tys) ^ ">") ^
-        (if null tms then ""
-         else "(" ^ commas (map (str_for_term false) tms) ^ ")")
-      | str_for_term _ _ = raise Fail "unexpected term in first-order format"
+    fun str_for_atom top_level (ATerm ((s, tys), tms)) =
+        let
+          val s' =
+            if is_tptp_equal s then "equal" |> suffix_tag top_level
+            else if s = tptp_true then "true"
+            else if s = tptp_false then "false"
+            else s
+        in dfg_string_for_term (ATerm ((s', tys), tms)) end
+      | str_for_atom _ _ = raise Fail "unexpected atom in first-order format"
     fun str_for_quant AForall = "forall"
       | str_for_quant AExists = "exists"
     fun str_for_conn _ ANot = "not"
@@ -558,7 +569,7 @@
       | str_for_formula top_level (AConn (c, phis)) =
         str_for_conn top_level c ^ "(" ^
         commas (map (str_for_formula false) phis) ^ ")"
-      | str_for_formula top_level (AAtom tm) = str_for_term top_level tm
+      | str_for_formula top_level (AAtom tm) = str_for_atom top_level tm
   in str_for_formula true end
 
 fun maybe_enclose bef aft "" = "% " ^ bef ^ aft
@@ -566,25 +577,27 @@
 
 fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
   let
-    val str_for_typ = string_for_type (DFG poly)
+    val typ = string_for_type (DFG poly)
+    val term = dfg_string_for_term
     fun spair (s, s') = "(" ^ s ^ ", " ^ s' ^ ")"
     fun tm_ary sym ty = spair (sym, string_of_arity (arity_of_type ty))
     fun ty_ary 0 ty = ty
       | ty_ary n ty = "(" ^ ty ^ ", " ^ string_of_int n ^ ")"
-    fun fun_typ sym ty = "function(" ^ sym ^ ", " ^ str_for_typ ty ^ ")."
+    fun fun_typ sym ty = "function(" ^ sym ^ ", " ^ typ ty ^ ")."
     fun pred_typ sym ty =
       let
         val (ty_vars, tys) =
           strip_atype ty |> fst
           |>> (fn [] => [] | ty_vars => ["[" ^ commas ty_vars ^ "]"])
-      in "predicate(" ^ commas (sym :: ty_vars @ map str_for_typ tys) ^ ")." end
-    fun str_for_bound_tvar (ty, []) = ty
-      | str_for_bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls
-    fun sort_decl xs ty cl =
-      "sort(" ^
-      (if null xs then ""
-       else "[" ^ commas (map str_for_bound_tvar xs) ^ "], ") ^
-      str_for_typ ty ^ ", " ^ cl ^ ")."
+      in "predicate(" ^ commas (sym :: ty_vars @ map typ tys) ^ ")." end
+    fun bound_tvar (ty, []) = ty
+      | bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls
+    fun foo xs ty =
+      (if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^
+      typ ty
+    fun sort_decl xs ty cl = "sort(" ^ foo xs ty ^ ", " ^ cl ^ ")."
+    fun datatype_decl xs ty tms =
+      "datatype(" ^ foo xs ty ^ ", " ^ commas (map term tms) ^ ")."
     fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
     fun formula pred (Formula ((ident, alt), kind, phi, _, info)) =
         if pred kind then
@@ -631,6 +644,9 @@
                if is_nontrivial_predicate_atype ty then SOME (pred_typ sym ty)
                else NONE
              | _ => NONE) |> flat
+    val datatype_decls =
+      filt (fn Datatype_Decl (_, xs, ty, tms) => SOME (datatype_decl xs ty tms)
+             | _ => NONE) |> flat
     val sort_decls =
       filt (fn Class_Memb (_, xs, ty, cl) => SOME (sort_decl xs ty cl)
              | _ => NONE) |> flat
@@ -638,7 +654,8 @@
       filt (fn Class_Decl (_, sub, supers) =>
                SOME (map (subclass_of sub) supers)
              | _ => NONE) |> flat |> flat
-    val decls = func_decls @ pred_decls @ sort_decls @ subclass_decls
+    val decls =
+      func_decls @ pred_decls @ datatype_decls @ sort_decls @ subclass_decls
     val axioms =
       filt (formula (curry (op <>) Conjecture)) |> separate [""] |> flat
     val conjs =