1signature TypeBase =
2sig
3
4   type hol_type  = Type.hol_type
5   type term      = Term.term
6   type thm       = Thm.thm
7   type tyinfo    = TypeBasePure.tyinfo
8   type typeBase  = TypeBasePure.typeBase
9   type shared_thm = TypeBasePure.shared_thm
10
11   (* Imperative database of datatype facts and associated operations. *)
12
13   val theTypeBase        : unit -> typeBase
14   val write              : tyinfo list -> tyinfo list
15   val export             : tyinfo list -> unit
16   val fetch              : hol_type -> tyinfo option
17   val read               : {Thy :string, Tyop: string} -> tyinfo option
18   val elts               : unit -> tyinfo list
19   val register_update_fn : (tyinfo list -> tyinfo list) -> unit
20
21   val axiom_of           : hol_type -> thm
22   val induction_of       : hol_type -> thm
23   val constructors_of    : hol_type -> term list
24   val destructors_of     : hol_type -> thm list
25   val recognizers_of     : hol_type -> thm list
26   val case_const_of      : hol_type -> term
27   val case_cong_of       : hol_type -> thm
28   val case_def_of        : hol_type -> thm
29   val case_eq_of         : hol_type -> thm
30   val nchotomy_of        : hol_type -> thm
31   val distinct_of        : hol_type -> thm
32   val fields_of          : hol_type -> (string * hol_type) list
33   val accessors_of       : hol_type -> thm list
34   val updates_of         : hol_type -> thm list
35   val one_one_of         : hol_type -> thm
36   val simpls_of          : hol_type -> simpfrag.simpfrag
37   val size_of            : hol_type -> term * thm
38   val encode_of          : hol_type -> term * thm
39
40   val axiom_of0          : hol_type -> shared_thm
41   val induction_of0      : hol_type -> shared_thm
42   val size_of0           : hol_type -> (term * shared_thm) option
43   val encode_of0         : hol_type -> (term * shared_thm) option
44
45   val is_constructor     : term -> bool
46
47   val mk_case            : term * (term * term) list -> term
48   val dest_case          : term -> term * term * (term * term) list
49   val is_case            : term -> bool
50   val strip_case         : term -> term * (term * term) list
51   val mk_pattern_fn      : (term * term) list -> term
52
53   val mk_record          : hol_type * (string * term) list -> term
54   val dest_record        : term -> hol_type * (string * term) list
55   val is_record          : term -> bool
56
57   val dest_record_type   : hol_type -> (string * hol_type) list
58   val is_record_type     : hol_type -> bool
59
60   val CaseEq             : string -> thm
61   val CaseEqs            : string list -> thm
62   val AllCaseEqs         : unit -> thm
63end
64