1signature Datatype =
2sig
3 include Abbrev
4 type tyinfo       = TypeBasePure.tyinfo
5 type typeBase     = TypeBasePure.typeBase;
6 type AST          = ParseDatatype.AST
7 type field_name   = string
8 type field_names  = string list
9 type constructor  = string * hol_type list
10 type tyspec       = hol_type * constructor list
11
12 val big_record_size : int ref
13
14 val tyspecs_of    : type_grammar.grammar -> hol_type quotation -> tyspec list
15 val to_tyspecs    : AST list -> tyspec list
16
17 (*---------------------------------------------------------------------------*)
18 (* Interfaces to the basic datatype definition package.                      *)
19 (*---------------------------------------------------------------------------*)
20
21 val define_type   : tyspec list -> {induction:thm, recursion:thm}
22 val new_datatype  : hol_type quotation -> {induction:thm, recursion:thm}
23
24 (*---------------------------------------------------------------------------*)
25 (* A datatype declaration generates tyinfo data for each datatype declared.  *)
26 (* The data of a tyinfo gets computed from the induction and recursion       *)
27 (* for the type, and is stored in a TypeBase, usually TypeBase.theTypeBase.  *)
28 (* Hol_datatype does this persistently; the other entrypoints support        *)
29 (* variations.                                                               *)
30 (* The string accompanying each tyinfo is the code for an ML expression      *)
31 (* which will be of type tyinfo -> tyinfo.  This code can be inserted        *)
32 (* into a theory file to update a datatype's basic tyinfo with extra         *)
33 (* "smarts".  For example, record tyinfos get new rewrites to do obvious     *)
34 (* things with fields and the like.  Big enumerated types, whose tyinfos     *)
35 (* won't include a distinctness theorem, get an extra conversion stuffed     *)
36 (* into their tyinfo to do inequality resolution.                            *)
37 (*---------------------------------------------------------------------------*)
38
39 val build_tyinfos : typeBase
40                         -> {induction:thm, recursion:thm}
41                           -> tyinfo list
42
43 val primHol_datatype : typeBase -> AST list -> typeBase * tyinfo list
44
45 val astHol_datatype  : AST list -> unit
46 val Hol_datatype  : hol_type quotation -> unit
47 val Datatype : hol_type quotation -> unit
48
49end
50