1signature TypeBasePure =
2sig
3   type hol_type = Type.hol_type
4   type term     = Term.term
5   type thm      = Thm.thm
6
7   type tyinfo
8   type typeBase
9   type simpfrag = simpfrag.simpfrag
10   type rcd_fieldinfo = {ty: hol_type, accessor: term, fupd : term}
11
12
13   datatype shared_thm = ORIG of thm
14                       | COPY of (string * string) * thm
15   type mk_datatype_record =
16        {ax        : shared_thm,
17         induction : shared_thm,
18         case_def  : thm,
19         case_cong : thm,
20         case_eq   : thm,
21         nchotomy  : thm,
22         size      : (term * shared_thm) option,
23         encode    : (term * shared_thm) option,
24         lift      : term option,
25         one_one   : thm option,
26         distinct  : thm option,
27         fields    : (string * rcd_fieldinfo) list,
28         accessors : thm list,
29         updates   : thm list,
30         destructors : thm list,
31         recognizers : thm list}
32
33   val mk_datatype_info_no_simpls : mk_datatype_record -> tyinfo
34   val gen_std_rewrs    : tyinfo -> thm list
35   val add_std_simpls   : tyinfo -> tyinfo
36   val mk_datatype_info : mk_datatype_record -> tyinfo
37
38   val gen_datatype_info : {ax:thm,ind:thm,case_defs:thm list} -> tyinfo list
39
40   val mk_nondatatype_info
41           : hol_type *
42             {nchotomy  : thm option,
43              induction : thm option,
44              size      : (term * thm) option,
45              encode    : (term * thm) option} -> tyinfo
46
47   val pp_tyinfo       : tyinfo Parse.pprinter
48
49   val ty_of           : tyinfo -> hol_type
50   val ty_name_of      : tyinfo -> string * string
51
52   val axiom_of        : tyinfo -> thm
53   val induction_of    : tyinfo -> thm
54   val constructors_of : tyinfo -> term list
55   val destructors_of  : tyinfo -> thm list
56   val recognizers_of  : tyinfo -> thm list
57   val case_const_of   : tyinfo -> term
58   val case_cong_of    : tyinfo -> thm
59   val case_def_of     : tyinfo -> thm
60   val case_eq_of      : tyinfo -> thm
61   val nchotomy_of     : tyinfo -> thm
62   val distinct_of     : tyinfo -> thm option
63   val one_one_of      : tyinfo -> thm option
64   val fields_of       : tyinfo -> (string * rcd_fieldinfo) list
65   val accessors_of    : tyinfo -> thm list
66   val updates_of      : tyinfo -> thm list
67   val simpls_of       : tyinfo -> simpfrag
68   val size_of         : tyinfo -> (term * thm) option
69   val encode_of       : tyinfo -> (term * thm) option
70   val lift_of         : tyinfo -> term option
71   val extra_of        : tyinfo -> ThyDataSexp.t list
72
73   val axiom_of0       : tyinfo -> shared_thm
74   val induction_of0   : tyinfo -> shared_thm
75   val size_of0        : tyinfo -> (term * shared_thm) option
76   val encode_of0      : tyinfo -> (term * shared_thm) option
77
78   val put_nchotomy    : thm -> tyinfo -> tyinfo
79   val put_simpls      : simpfrag -> tyinfo -> tyinfo
80   val add_rewrs       : thm list -> tyinfo -> tyinfo
81   val add_ssfrag_convs: simpfrag.convdata list -> tyinfo -> tyinfo
82   val put_induction   : shared_thm -> tyinfo -> tyinfo
83   val put_axiom       : shared_thm -> tyinfo -> tyinfo
84   val put_size        : term * shared_thm -> tyinfo -> tyinfo
85   val put_encode      : term * shared_thm -> tyinfo -> tyinfo
86   val put_lift        : term -> tyinfo -> tyinfo
87   val put_fields      : (string * rcd_fieldinfo) list -> tyinfo -> tyinfo
88   val put_accessors   : thm list -> tyinfo -> tyinfo
89   val put_updates     : thm list -> tyinfo -> tyinfo
90   val put_destructors : thm list -> tyinfo -> tyinfo
91   val put_recognizers : thm list -> tyinfo -> tyinfo
92   val put_extra       : ThyDataSexp.t list -> tyinfo -> tyinfo
93   val add_extra       : ThyDataSexp.t list -> tyinfo -> tyinfo
94
95   (* Functional databases of datatype facts and associated operations *)
96
97   val empty           : typeBase
98   val insert          : typeBase -> tyinfo -> typeBase
99   val fold            : (hol_type * tyinfo * 'b -> 'b) -> 'b -> typeBase ->
100                         'b
101(*   val add             : typeBase -> tyinfo -> typeBase  *)
102
103   val fetch           : typeBase -> hol_type -> tyinfo option
104   val prim_get        : typeBase -> string * string -> tyinfo option
105   val get             : typeBase -> string -> tyinfo list
106                       (* get returns list of tyinfos for types with that tyop *)
107
108   val listItems       : typeBase -> tyinfo list
109   val toPmatchThry    : typeBase -> {Thy:string,Tyop:string} ->
110                         {constructors : term list, case_const : term} option
111
112  (* Support for polytypism *)
113
114   val typeValue       : (hol_type -> term option) *
115                         (hol_type -> term option) *
116                         (hol_type -> term) -> hol_type -> term
117   val tyValue         : (hol_type -> term option) *
118                         (hol_type -> term option) *
119                         (hol_type -> term) -> hol_type -> term
120
121   val type_size       : typeBase -> hol_type -> term
122   val type_encode     : typeBase -> hol_type -> term
123   val type_lift       : typeBase -> hol_type -> term
124
125   val cinst           : hol_type -> term -> term
126
127   val is_constructor  : typeBase -> term -> bool
128
129   val mk_case         : typeBase -> term * (term * term) list -> term
130   val dest_case       : typeBase -> term -> term * term * (term * term) list
131   val is_case         : typeBase -> term -> bool
132   val strip_case      : typeBase -> term -> term * (term * term) list
133
134   val mk_record       : typeBase -> hol_type * (string * term) list -> term
135   val dest_record     : typeBase -> term -> hol_type * (string * term) list
136   val is_record       : typeBase -> term -> bool
137
138   val dest_record_type : typeBase -> hol_type -> (string * rcd_fieldinfo) list
139   val is_record_type   : typeBase -> hol_type -> bool
140
141   val toSEXP          : tyinfo -> ThyDataSexp.t
142   val fromSEXP        : ThyDataSexp.t -> tyinfo option
143
144end
145