# HG changeset patch
# User blanchet
# Date 1368702352 -7200
# Node ID 9f94930b12e67e16c83b65833549b046f5a52b6f
# Parent  eb264c3fa30ec63fe727207ac4f022d5827c002f
more work on SPASS datatypes

diff -r eb264c3fa30e -r 9f94930b12e6 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu May 16 11:35:07 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu May 16 13:05:52 2013 +0200
@@ -51,7 +51,7 @@
     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 * bool |
+                     * ('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
@@ -125,6 +125,7 @@
     -> 'e -> 'e
   val formula_map :
     ('c -> 'e) -> ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'e, 'd) formula
+  val strip_atype : 'a ho_type -> 'a list * ('a ho_type list * 'a ho_type)
   val is_format_higher_order : atp_format -> bool
   val tptp_string_of_line : atp_format -> string problem_line -> string
   val lines_of_atp_problem :
@@ -193,7 +194,7 @@
   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 * bool |
+                   * ('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
@@ -315,11 +316,16 @@
   | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
   | formula_map f (AAtom tm) = AAtom (f tm)
 
-fun strip_atype (APi (tys, ty)) = strip_atype ty |>> apfst (append tys)
-  | strip_atype (AFun (ty1, ty2)) = strip_atype ty2 |>> apsnd (cons ty1)
-  | strip_atype ty = (([], []), ty)
+fun strip_api (APi (tys, ty)) = strip_api ty |>> append tys
+  | strip_api ty = ([], ty)
 
-fun is_function_atype ty = snd (strip_atype ty) <> AType (tptp_bool_type, [])
+fun strip_afun (AFun (ty1, ty2)) = strip_afun ty2 |>> cons ty1
+  | strip_afun ty = ([], ty)
+
+fun strip_atype ty = ty |> strip_api ||> strip_afun
+
+fun is_function_atype ty =
+  snd (snd (strip_atype ty)) <> AType (tptp_bool_type, [])
 fun is_predicate_atype ty = not (is_function_atype ty)
 fun is_nontrivial_predicate_atype (AType _) = false
   | is_nontrivial_predicate_atype ty = is_predicate_atype ty
@@ -347,15 +353,15 @@
     else
       func ^ "(" ^ commas args ^ ")"
 
-fun flatten_type (APi (tys, ty)) = APi (tys, flatten_type ty)
-  | flatten_type (ty as AFun (ty1 as AType _, ty2)) =
-    (case flatten_type ty2 of
+fun uncurry_type (APi (tys, ty)) = APi (tys, uncurry_type ty)
+  | uncurry_type (ty as AFun (ty1 as AType _, ty2)) =
+    (case uncurry_type ty2 of
        AFun (ty' as AType (s, tys), ty) =>
        AFun (AType (tptp_product_type,
                     ty1 :: (if s = tptp_product_type then tys else [ty'])), ty)
      | _ => ty)
-  | flatten_type (ty as AType _) = ty
-  | flatten_type _ =
+  | uncurry_type (ty as AType _) = ty
+  | uncurry_type _ =
     raise Fail "unexpected higher-order type in first-order format"
 
 val dfg_individual_type = "iii" (* cannot clash *)
@@ -390,7 +396,7 @@
   in str true ty end
 
 fun string_of_type (format as THF _) ty = str_of_type format ty
-  | string_of_type format ty = str_of_type format (flatten_type ty)
+  | string_of_type format ty = str_of_type format (uncurry_type ty)
 
 fun tptp_string_of_quantifier AForall = tptp_forall
   | tptp_string_of_quantifier AExists = tptp_exists
@@ -585,9 +591,9 @@
     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 ^ "]"])
+        val (ty_vars, (tys, _)) =
+          strip_atype ty
+          |>> (fn [] => [] | xs => ["[" ^ commas xs ^ "]"])
       in "predicate(" ^ commas (sym :: ty_vars @ map typ tys) ^ ")." end
     fun bound_tvar (ty, []) = ty
       | bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls
@@ -595,9 +601,8 @@
       (if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^
       typ ty
     fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")."
-    fun datatype_decl xs ty tms exhaust =
-      "datatype(" ^ commas (binder_typ xs ty :: map term tms @
-                            (if exhaust then [] else ["..."])) ^ ")."
+    fun datatype_decl xs ty tms =
+      "datatype(" ^ commas (binder_typ xs ty :: map term tms) ^ ")."
     fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
     fun formula pred (Formula ((ident, alt), kind, phi, _, info)) =
         if pred kind then
@@ -645,8 +650,8 @@
                else NONE
              | _ => NONE) |> flat
     val datatype_decls =
-      filt (try (fn Datatype_Decl (_, xs, ty, tms, exhaust) =>
-                    datatype_decl xs ty tms exhaust)) |> flat
+      filt (try (fn Datatype_Decl (_, xs, ty, tms) => datatype_decl xs ty tms))
+      |> flat
     val sort_decls =
       filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat
     val subclass_decls =
@@ -924,9 +929,9 @@
       | 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, exhaust)) =
+      | nice_line (Datatype_Decl (ident, xs, ty, tms)) =
         nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms
-        #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms, exhaust))
+        #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms))
       | nice_line (Class_Memb (ident, xs, ty, cl)) =
         nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl
         #>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl))
diff -r eb264c3fa30e -r 9f94930b12e6 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 16 11:35:07 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 16 13:05:52 2013 +0200
@@ -426,7 +426,7 @@
 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
 
 val tvar_a_str = "'a"
-val tvar_a_z = ((tvar_a_str, 100 (* arbitrary *)), HOLogic.typeS)
+val tvar_a_z = ((tvar_a_str, 0), HOLogic.typeS)
 val tvar_a = TVar tvar_a_z
 val tvar_a_name = tvar_name tvar_a_z
 val itself_name = `make_fixed_type_const @{type_name itself}
@@ -2539,17 +2539,32 @@
     val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms
   in mono_lines @ decl_lines end
 
-fun datatypes_of_facts ctxt (DFG Polymorphic) (type_enc as Native _) facts =
-    if is_type_enc_polymorphic type_enc then
-      [(@{typ nat}, [@{term "0::nat"}, @{term Suc}], true)]
-    else
-      []
+fun datatypes_of_facts ctxt (DFG Polymorphic) (type_enc as Native (_, _, level))
+                       facts =
+    let
+      val thy = Proof_Context.theory_of ctxt
+      val mono = default_mono level false
+      val ho_term_from_term =
+        iterm_from_term thy type_enc []
+        #> fst #> ho_term_from_iterm ctxt mono type_enc NONE
+    in
+      if is_type_enc_polymorphic type_enc then
+        [(native_ho_type_from_typ type_enc false 0 @{typ nat},
+          map ho_term_from_term [@{term "0::nat"}, @{term Suc}]) (*,
+         (native_ho_type_from_typ type_enc false 0 (Logic.varifyT_global @{typ "'a list"}),
+          map (ho_term_from_term o Logic.varify_types_global) [@{term Nil}, @{term Cons}]) *)]
+      else
+        []
+    end
   | datatypes_of_facts _ _ _ _ = []
 
-fun decl_line_of_datatype (_, [], _) = NONE
-  | decl_line_of_datatype (T as Type (s, _), ctrs, exhaust) =
-    SOME (Datatype_Decl (datatype_decl_prefix ^ ascii_of s, [],
-             AType (("naT", @{type_name nat}), []), [], exhaust)) (*###*)
+fun decl_line_of_datatype (ty as AType ((_, s'), ty_args), ctrs) =
+  let
+    val xs = map (fn AType (name, []) => name) ty_args
+  in
+    Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty,
+                   ctrs)
+  end
 
 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
 
@@ -2668,7 +2683,7 @@
     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, _)) =
+      | 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 do_bound_tvars xs #> do_type ty #> do_class cl
@@ -2772,7 +2787,7 @@
       (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 = map_filter decl_line_of_datatype datatypes
+    val datatype_decl_lines = map decl_line_of_datatype datatypes
     val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines
     val num_facts = length facts
     val fact_lines =