# HG changeset patch
# User blanchet
# Date 1368633946 -7200
# Node ID 2fb33d73c3669c50848594dc06142f05bd2e00c4
# Parent  650b7c6b8164f9e883e7cdaa5def132e2957faa8
more work on implementing datatype output for new SPASS

diff -r 650b7c6b8164 -r 2fb33d73c366 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Wed May 15 17:49:39 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed May 15 18:05:46 2013 +0200
@@ -784,8 +784,7 @@
 (** Nice names **)
 
 fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
-fun pool_map f xs =
-  pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
+fun pool_map f xs = pool_fold (fn x => fn ys => f x #>> (fn y => y :: ys)) xs []
 
 val no_qualifiers =
   let
@@ -890,6 +889,10 @@
       | DFG _ => avoid_clash_with_dfg_keywords
       | _ => I
     val nice_name = nice_name avoid_clash
+    fun nice_bound_tvars xs =
+      pool_map nice_name (map fst xs)
+      ##>> pool_map (pool_map nice_name) (map snd xs)
+      #>> op ~~
     fun nice_type (AType (name, tys)) =
         nice_name name ##>> pool_map nice_type tys #>> AType
       | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
@@ -923,12 +926,12 @@
       | nice_line (Sym_Decl (ident, sym, ty)) =
         nice_name sym ##>> nice_type ty
         #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty))
+      | nice_line (Datatype_Decl (ident, xs, ty, tms)) =
+        nice_bound_tvars xs ##>> nice_type ty ##>> pool_map nice_term tms
+        #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms))
       | nice_line (Class_Memb (ident, xs, ty, cl)) =
-        pool_map nice_name (map fst xs)
-        ##>> pool_map (pool_map nice_name) (map snd xs)
-        ##>> nice_type ty ##>> nice_name cl
-        #>> (fn (((tys, cls), ty), cl) =>
-                Class_Memb (ident, tys ~~ cls, ty, cl))
+        nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl
+        #>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl))
       | nice_line (Formula (ident, kind, phi, source, info)) =
         nice_formula phi
         #>> (fn phi => Formula (ident, kind, phi, source, info))
diff -r 650b7c6b8164 -r 2fb33d73c366 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 15 17:49:39 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 15 18:05:46 2013 +0200
@@ -2534,6 +2534,13 @@
     val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms
   in mono_lines @ decl_lines end
 
+fun decl_lines_of_datatypes (DFG Polymorphic) (type_enc as Native _) =
+    if is_type_enc_polymorphic type_enc then
+      [Datatype_Decl ("nat", [], AType (("naT", @{type_name nat}), []), [])] (*###*)
+    else
+      []
+  | decl_lines_of_datatypes _ _ = []
+
 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
 
 fun do_uncurried_alias_lines_of_sym ctxt constrs mono type_enc sym_tab0 sym_tab
@@ -2630,6 +2637,7 @@
     fun do_sym (name as (s, _)) value =
       if is_tptp_user_symbol s then Symtab.default (s, (name, value)) else I
     fun do_class name = apfst (apfst (do_sym name ()))
+    val do_bound_tvars = fold do_class o snd
     fun do_type (AType (name, tys)) =
         apfst (apsnd (do_sym name (length tys))) #> fold do_type tys
       | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
@@ -2650,8 +2658,10 @@
     fun do_line (Class_Decl (_, _, cls)) = fold do_class cls
       | do_line (Type_Decl _) = I
       | do_line (Sym_Decl (_, _, ty)) = do_type ty
+      | do_line (Datatype_Decl (_, xs, ty, tms)) =
+        fold do_bound_tvars xs #> do_type ty #> fold (do_term false) tms
       | do_line (Class_Memb (_, xs, ty, cl)) =
-        fold (fold do_class o snd) xs #> do_type ty #> do_class cl
+        fold do_bound_tvars xs #> do_type ty #> do_class cl
       | do_line (Formula (_, _, phi, _, _)) = do_formula phi
     val ((cls, tys), syms) = declared_in_atp_problem problem
   in
@@ -2751,6 +2761,8 @@
       (conjs, helpers @ facts, uncurried_alias_eq_tms)
       |> sym_decl_table_of_facts thy type_enc sym_tab
       |> lines_of_sym_decl_table ctxt mono type_enc mono_Ts
+    val datatype_decl_lines = decl_lines_of_datatypes format type_enc
+    val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines
     val num_facts = length facts
     val fact_lines =
       map (line_of_fact ctxt fact_prefix ascii_of I (not exporter)
@@ -2766,7 +2778,7 @@
     val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs
     (* Reordering these might confuse the proof reconstruction code. *)
     val problem =
-      [(explicit_declsN, class_decl_lines @ sym_decl_lines),
+      [(explicit_declsN, decl_lines),
        (uncurried_alias_eqsN, uncurried_alias_eq_lines),
        (factsN, fact_lines),
        (subclassesN, subclass_lines),