/[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 3588 - (show annotations) (download)
Sat Apr 27 02:45:24 2002 UTC (19 years, 3 months ago) by emre
File size: 6170 byte(s)
Updating modules so that they generate documentation
for theories.pdf.  Right now, it's _very_ minimal and
not so useful.  Hopefully, I will get around to updating
them and making them decent.

Also updating the README file to properly reflect the
name of our research group at Caltech.

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 pointerSub
100 declare functionSub
101
102 (* Element width. *)
103
104 declare byteIndex
105 declare wordIndex
106
107 (* Kind of subscript. *)
108
109 declare intIndex
110 declare rawIntIndex{ 'int_precision; 'int_signed }
111
112 (* Subscripting op. *)
113
114 declare subop{ 'sub_block; 'sub_value; 'sub_index; 'sub_script }
115
116 (*************************************************************************
117 * Term operations.
118 *************************************************************************)
119
120 (* Options, i.e. None | Some of 'a. *)
121
122 val noneOpt_term : term
123 val is_noneOpt_term : term -> bool
124
125 val someOpt_term : term
126 val is_someOpt_term : term -> bool
127 val mk_someOpt_term : term -> term
128 val dest_someOpt_term : term -> term
129
130 (* Boolean constants. *)
131
132 val val_true_term : term
133 val is_val_true_term : term -> bool
134
135 val val_false_term : term
136 val is_val_false_term : term -> bool
137
138 (* Floating-point and integer precisions. *)
139
140 val int8_term : term
141 val is_int8_term : term -> bool
142
143 val int16_term : term
144 val is_int16_term : term -> bool
145
146 val int32_term : term
147 val is_int32_term : term -> bool
148
149 val int64_term : term
150 val is_int64_term : term -> bool
151
152 val floatSingle_term : term
153 val is_floatSingle_term : term -> bool
154
155 val floatDouble_term : term
156 val is_floatDouble_term : term -> bool
157
158 val floatLongDouble_term : term
159 val is_floatLongDouble_term : term -> bool
160
161 (* Signed / unsigned integer qualifiers. *)
162
163 val signedInt_term : term
164 val is_signedInt_term : term -> bool
165
166 val unsignedInt_term : term
167 val is_unsignedInt_term : term -> bool
168
169 (* int and rawint sets. *)
170
171 val interval_term : term
172 val is_interval_term : term -> bool
173 val mk_interval_term : term -> term -> term
174 val dest_interval_term : term -> term * term
175
176 val int_set_term : term
177 val is_int_set_term : term -> bool
178 val mk_int_set_term : term -> term
179 val dest_int_set_term : term -> term
180
181 val rawint_set_term : term
182 val is_rawint_set_term : term -> bool
183 val mk_rawint_set_term : term -> term -> term -> term
184 val dest_rawint_set_term : term -> term * term * term
185
186 (* Tuple classes. *)
187
188 val normalTuple_term : term
189 val is_normalTuple_term : term -> bool
190
191 val rawTuple_term : term
192 val is_rawTuple_term : term -> bool
193
194 (* Union tags. *)
195
196 val normalUnion_term : term
197 val is_normalUnion_term : term -> bool
198
199 val exnUnion_term : term
200 val is_exnUnion_term : term -> bool
201
202 (*
203 * Subscript operators.
204 *)
205
206 (* Kind of block. *)
207
208 val blockSub_term : term
209 val is_blockSub_term : term -> bool
210
211 val rawDataSub_term : term
212 val is_rawDataSub_term : term -> bool
213
214 val tupleSub_term : term
215 val is_tupleSub_term : term -> bool
216
217 val rawTupleSub_term : term
218 val is_rawTupleSub_term : term -> bool
219
220 (* Kind of value. *)
221
222 val polySub_term : term
223 val is_polySub_term : term -> bool
224
225 val rawIntSub_term : term
226 val is_rawIntSub_term : term -> bool
227 val mk_rawIntSub_term : term -> term -> term
228 val dest_rawIntSub_term : term -> term * term
229
230 val rawFloatSub_term : term
231 val is_rawFloatSub_term : term -> bool
232 val mk_rawFloatSub_term : term -> term
233 val dest_rawFloatSub_term : term -> term
234
235 val pointerSub_term : term
236 val is_pointerSub_term : term -> bool
237
238 val functionSub_term : term
239 val is_functionSub_term : term -> bool
240
241 (* Element width. *)
242
243 val byteIndex_term : term
244 val is_byteIndex_term : term -> bool
245
246 val wordIndex_term : term
247 val is_wordIndex_term : term -> bool
248
249 (* Kind of subscript. *)
250
251 val intIndex_term : term
252 val is_intIndex_term : term -> bool
253
254 val rawIntIndex_term : term
255 val is_rawIntIndex_term : term -> bool
256 val mk_rawIntIndex_term : term -> term -> term
257 val dest_rawIntIndex_term : term -> term * term
258
259 (* Susbscripting op. *)
260
261 val subop_term : term
262 val is_subop_term : term -> bool
263 val mk_subop_term : term -> term -> term -> term -> term
264 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