/[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 3580 - (show annotations) (download)
Fri Apr 19 08:09:21 2002 UTC (19 years, 3 months ago) by emre
File size: 6316 byte(s)
Comitting more changes to reflect the ever changing MC FIR.

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