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