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   type rcd_fieldinfo = TypeBasePure.rcd_fieldinfo
11
12   (* Imperative database of datatype facts and associated operations. *)
13
14   val theTypeBase        : unit -> typeBase
15   val thy_typebase       : {thyname : string} -> typeBase option
16   val thy_updates        : {thyname : string} -> tyinfo list
17   val merge_typebases    : string list -> typeBase option
18   val write              : tyinfo list -> unit
19   val export             : tyinfo list -> unit (* includes write action *)
20   val fetch              : hol_type -> tyinfo option
21   val read               : {Thy :string, Tyop: string} -> tyinfo option
22   val elts               : unit -> tyinfo list
23   val register_update_fn : (tyinfo -> tyinfo) -> unit
24
25   val axiom_of           : hol_type -> thm
26   val induction_of       : hol_type -> thm
27   val constructors_of    : hol_type -> term list
28   val destructors_of     : hol_type -> thm list
29   val recognizers_of     : hol_type -> thm list
30   val case_const_of      : hol_type -> term
31   val case_cong_of       : hol_type -> thm
32   val case_def_of        : hol_type -> thm
33   val case_eq_of         : hol_type -> thm
34   val nchotomy_of        : hol_type -> thm
35   val distinct_of        : hol_type -> thm
36   val fields_of          : hol_type -> (string * rcd_fieldinfo) list
37   val accessors_of       : hol_type -> thm list
38   val updates_of         : hol_type -> thm list
39   val one_one_of         : hol_type -> thm
40   val simpls_of          : hol_type -> simpfrag.simpfrag
41   val size_of            : hol_type -> term * thm
42   val encode_of          : hol_type -> term * thm
43
44   val axiom_of0          : hol_type -> shared_thm
45   val induction_of0      : hol_type -> shared_thm
46   val size_of0           : hol_type -> (term * shared_thm) option
47   val encode_of0         : hol_type -> (term * shared_thm) option
48
49   val is_constructor     : term -> bool
50
51   val mk_case            : term * (term * term) list -> term
52   val dest_case          : term -> term * term * (term * term) list
53   val is_case            : term -> bool
54   val strip_case         : term -> term * (term * term) list
55   val mk_pattern_fn      : (term * term) list -> term
56
57   val mk_record          : hol_type * (string * term) list -> term
58   val dest_record        : term -> hol_type * (string * term) list
59   val is_record          : term -> bool
60
61   val dest_record_type   : hol_type -> (string * rcd_fieldinfo) list
62   val is_record_type     : hol_type -> bool
63
64   val CaseEq             : string -> thm
65   val CaseEqs            : string list -> thm
66   val AllCaseEqs         : unit -> thm
67
68   val update_induction   : thm -> unit
69   val update_axiom       : thm -> unit
70end
71