1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Apr 24 21:00:00 2014 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Apr 25 11:58:10 2014 +0200
     1.3 @@ -50,7 +50,8 @@
     1.4      Class_Decl of string * 'a * 'a list |
     1.5      Type_Decl of string * 'a * int |
     1.6      Sym_Decl of string * 'a * 'a atp_type |
     1.7 -    Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list |
     1.8 +    Datatype_Decl of
     1.9 +      string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list * bool |
    1.10      Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a |
    1.11      Formula of (string * string) * atp_formula_role
    1.12                 * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula
    1.13 @@ -194,7 +195,8 @@
    1.14    Class_Decl of string * 'a * 'a list |
    1.15    Type_Decl of string * 'a * int |
    1.16    Sym_Decl of string * 'a * 'a atp_type |
    1.17 -  Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list |
    1.18 +  Datatype_Decl of
    1.19 +    string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list * bool |
    1.20    Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a |
    1.21    Formula of (string * string) * atp_formula_role
    1.22               * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula
    1.23 @@ -613,7 +615,9 @@
    1.24        (if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^
    1.25        typ ty
    1.26      fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")."
    1.27 -    fun datatype_decl xs ty tms = "datatype(" ^ commas (binder_typ xs ty :: map term tms) ^ ")."
    1.28 +    fun datatype_decl xs ty tms exhaust =
    1.29 +      "datatype(" ^ commas (binder_typ xs ty :: map term tms @ (if exhaust then [] else ["..."])) ^
    1.30 +      ")."
    1.31      fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
    1.32      fun formula pred (Formula ((ident, alt), kind, phi, _, info)) =
    1.33          if pred kind then
    1.34 @@ -661,7 +665,8 @@
    1.35                 else NONE
    1.36               | _ => NONE) |> flat
    1.37      val datatype_decls =
    1.38 -      filt (try (fn Datatype_Decl (_, xs, ty, tms) => datatype_decl xs ty tms)) |> flat
    1.39 +      filt (try (fn Datatype_Decl (_, xs, ty, tms, exhaust) => datatype_decl xs ty tms exhaust))
    1.40 +      |> flat
    1.41      val sort_decls =
    1.42        filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat
    1.43      val subclass_decls =
    1.44 @@ -938,9 +943,9 @@
    1.45          nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary))
    1.46        | nice_line (Sym_Decl (ident, sym, ty)) =
    1.47          nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty))
    1.48 -      | nice_line (Datatype_Decl (ident, xs, ty, tms)) =
    1.49 +      | nice_line (Datatype_Decl (ident, xs, ty, tms, exhaust)) =
    1.50          nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms
    1.51 -        #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms))
    1.52 +        #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms, exhaust))
    1.53        | nice_line (Class_Memb (ident, xs, ty, cl)) =
    1.54          nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl
    1.55          #>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl))

     2.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Apr 24 21:00:00 2014 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Apr 25 11:58:10 2014 +0200
     2.3 @@ -2462,21 +2462,19 @@
     2.4  
     2.5          fun datatype_of_ctrs (ctrs as (_, T1) :: _) =
     2.6            let val ctrs' = map do_ctr ctrs in
     2.7 -            if forall is_some ctrs' then
     2.8 -              SOME (native_atp_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs')
     2.9 -            else
    2.10 -              NONE
    2.11 +            (native_atp_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs',
    2.12 +             forall is_some ctrs')
    2.13            end
    2.14        in
    2.15 -        map_filter datatype_of_ctrs ctrss
    2.16 +        ctrss |> map datatype_of_ctrs |> filter_out (null o #2)
    2.17        end
    2.18      else
    2.19        []
    2.20    | datatypes_of_sym_table _ _ _ _ _ _ = []
    2.21  
    2.22 -fun decl_line_of_datatype (ty as AType (((_, s'), _), ty_args), ctrs) =
    2.23 +fun decl_line_of_datatype (ty as AType (((_, s'), _), ty_args), ctrs, exhaust) =
    2.24    let val xs = map (fn AType ((name, _), []) => name) ty_args in
    2.25 -    Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs)
    2.26 +    Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs, exhaust)
    2.27    end
    2.28  
    2.29  fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
    2.30 @@ -2589,7 +2587,7 @@
    2.31      fun do_line (Class_Decl (_, _, cls)) = fold do_class cls
    2.32        | do_line (Type_Decl _) = I
    2.33        | do_line (Sym_Decl (_, _, ty)) = do_type ty
    2.34 -      | do_line (Datatype_Decl (_, xs, ty, tms)) =
    2.35 +      | do_line (Datatype_Decl (_, xs, ty, tms, _)) =
    2.36          fold do_bound_tvars xs #> do_type ty #> fold (do_term false) tms
    2.37        | do_line (Class_Memb (_, xs, ty, cl)) = fold do_bound_tvars xs #> do_type ty #> do_class cl
    2.38        | do_line (Formula (_, _, phi, _, _)) = do_formula phi