/[mojave]/metaprl/theories/mc/mp_mc_fir_base.mli
ViewVC logotype

Contents of /metaprl/theories/mc/mp_mc_fir_base.mli

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3590 - (show annotations) (download)
Sat Apr 27 19:52:38 2002 UTC (19 years, 3 months ago) by emre
File size: 6270 byte(s)
Adding some documentation.  Still have a long ways to go
in fully documenting everything.

1 (*
2 * The Mp_mc_fir_base module defines terms to represent basic FIR
3 * terms and supporting OCaml values.
4 *
5 * ----------------------------------------------------------------
6 *
7 * This file is part of MetaPRL, a modular, higher order
8 * logical framework that provides a logical programming
9 * environment for OCaml and other languages.
10 *
11 * See the file doc/index.html for information on Nuprl,
12 * OCaml, and more information about this system.
13 *
14 * Copyright (C) 2002 Brian Emre Aydemir, Caltech
15 *
16 * This program is free software; you can redistribute it and/or
17 * modify it under the terms of the GNU General Public License
18 * as published by the Free Software Foundation; either version 2
19 * of the License, or (at your option) any later version.
20 *
21 * This program is distributed in the hope that it will be useful,
22 * but WITHOUT ANY WARRANTY; without even the implied warranty of
23 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
24 * GNU General Public License for more details.
25 *
26 * You should have received a copy of the GNU General Public License
27 * along with this program; if not, write to the Free Software
28 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
29 *
30 * Author: Brian Emre Aydemir
31 * Email: emre@its.caltech.edu
32 *)
33
34 include Base_theory
35
36 open Refiner.Refiner.Term
37
38 (*************************************************************************
39 * Term declarations.
40 *************************************************************************)
41
42 (* Options, i.e. None | Some of 'a. *)
43
44 declare noneOpt
45 declare someOpt{ 'a }
46
47 (* Boolean constants. *)
48
49 declare val_true
50 declare val_false
51
52 (* Floating-point and integer precisions. *)
53
54 declare int8
55 declare int16
56 declare int32
57 declare int64
58 declare floatSingle
59 declare floatDouble
60 declare floatLongDouble
61
62 (* Signed / unsigned integer qualifiers. *)
63
64 declare signedInt
65 declare unsignedInt
66
67 (* int and rawint sets. *)
68
69 declare interval{ 'left; 'right } (* closed bounds, i.e. [left, right] *)
70 declare int_set{ 'interval_list }
71 declare rawint_set{ 'int_precision; 'int_signed; 'interval_list }
72
73 (* Tuple classes. *)
74
75 declare normalTuple
76 declare rawTuple
77
78 (* Union tags. *)
79
80 declare normalUnion
81 declare exnUnion
82
83 (*
84 * Subscript operators.
85 *)
86
87 (* Kind of block. *)
88
89 declare blockSub
90 declare rawDataSub
91 declare tupleSub
92 declare rawTupleSub
93
94 (* Kind of value. *)
95
96 declare polySub
97 declare rawIntSub{ 'int_precision; 'int_signed }
98 declare rawFloatSub{ 'float_precision }
99 declare pointerInfixSub
100 declare pointerSub
101 declare functionSub
102
103 (* Element width. *)
104
105 declare byteIndex
106 declare wordIndex
107
108 (* Kind of subscript. *)
109
110 declare intIndex
111 declare rawIntIndex{ 'int_precision; 'int_signed }
112
113 (* Subscripting op. *)
114
115 declare subop{ 'sub_block; 'sub_value; 'sub_index; 'sub_script }
116
117 (*************************************************************************
118 * Term operations.
119 *************************************************************************)
120
121 (* Options, i.e. None | Some of 'a. *)
122
123 val noneOpt_term : term
124 val is_noneOpt_term : term -> bool
125
126 val someOpt_term : term
127 val is_someOpt_term : term -> bool
128 val mk_someOpt_term : term -> term
129 val dest_someOpt_term : term -> term
130
131 (* Boolean constants. *)
132
133 val val_true_term : term
134 val is_val_true_term : term -> bool
135
136 val val_false_term : term
137 val is_val_false_term : term -> bool
138
139 (* Floating-point and integer precisions. *)
140
141 val int8_term : term
142 val is_int8_term : term -> bool
143
144 val int16_term : term
145 val is_int16_term : term -> bool
146
147 val int32_term : term
148 val is_int32_term : term -> bool
149
150 val int64_term : term
151 val is_int64_term : term -> bool
152
153 val floatSingle_term : term
154 val is_floatSingle_term : term -> bool
155
156 val floatDouble_term : term
157 val is_floatDouble_term : term -> bool
158
159 val floatLongDouble_term : term
160 val is_floatLongDouble_term : term -> bool
161
162 (* Signed / unsigned integer qualifiers. *)
163
164 val signedInt_term : term
165 val is_signedInt_term : term -> bool
166
167 val unsignedInt_term : term
168 val is_unsignedInt_term : term -> bool
169
170 (* int and rawint sets. *)
171
172 val interval_term : term
173 val is_interval_term : term -> bool
174 val mk_interval_term : term -> term -> term
175 val dest_interval_term : term -> term * term
176
177 val int_set_term : term
178 val is_int_set_term : term -> bool
179 val mk_int_set_term : term -> term
180 val dest_int_set_term : term -> term
181
182 val rawint_set_term : term
183 val is_rawint_set_term : term -> bool
184 val mk_rawint_set_term : term -> term -> term -> term
185 val dest_rawint_set_term : term -> term * term * term
186
187 (* Tuple classes. *)
188
189 val normalTuple_term : term
190 val is_normalTuple_term : term -> bool
191
192 val rawTuple_term : term
193 val is_rawTuple_term : term -> bool
194
195 (* Union tags. *)
196
197 val normalUnion_term : term
198 val is_normalUnion_term : term -> bool
199
200 val exnUnion_term : term
201 val is_exnUnion_term : term -> bool
202
203 (*
204 * Subscript operators.
205 *)
206
207 (* Kind of block. *)
208
209 val blockSub_term : term
210 val is_blockSub_term : term -> bool
211
212 val rawDataSub_term : term
213 val is_rawDataSub_term : term -> bool
214
215 val tupleSub_term : term
216 val is_tupleSub_term : term -> bool
217
218 val rawTupleSub_term : term
219 val is_rawTupleSub_term : term -> bool
220
221 (* Kind of value. *)
222
223 val polySub_term : term
224 val is_polySub_term : term -> bool
225
226 val rawIntSub_term : term
227 val is_rawIntSub_term : term -> bool
228 val mk_rawIntSub_term : term -> term -> term
229 val dest_rawIntSub_term : term -> term * term
230
231 val rawFloatSub_term : term
232 val is_rawFloatSub_term : term -> bool
233 val mk_rawFloatSub_term : term -> term
234 val dest_rawFloatSub_term : term -> term
235
236 val pointerInfixSub_term : term
237 val is_pointerInfixSub_term : term -> bool
238
239 val pointerSub_term : term
240 val is_pointerSub_term : term -> bool
241
242 val functionSub_term : term
243 val is_functionSub_term : term -> bool
244
245 (* Element width. *)
246
247 val byteIndex_term : term
248 val is_byteIndex_term : term -> bool
249
250 val wordIndex_term : term
251 val is_wordIndex_term : term -> bool
252
253 (* Kind of subscript. *)
254
255 val intIndex_term : term
256 val is_intIndex_term : term -> bool
257
258 val rawIntIndex_term : term
259 val is_rawIntIndex_term : term -> bool
260 val mk_rawIntIndex_term : term -> term -> term
261 val dest_rawIntIndex_term : term -> term * term
262
263 (* Susbscripting op. *)
264
265 val subop_term : term
266 val is_subop_term : term -> bool
267 val mk_subop_term : term -> term -> term -> term -> term
268 val dest_subop_term : term -> term * term * term * term

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26