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

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

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: 14782 byte(s)
Adding some documentation.  Still have a long ways to go
in fully documenting everything.

1 (*!
2 * @begin[doc]
3 * @theory[Mp_mc_fir_base]
4 *
5 * The @tt{Mp_mc_fir_base} module defines terms to represent basic FIR
6 * terms and supporting @OCaml values.
7 * @end[doc].
8 *
9 * ----------------------------------------------------------------
10 *
11 * @begin[license]
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 * Copyright (C) 2002 Brian Emre Aydemir, Caltech
20 *
21 * This program is free software; you can redistribute it and/or
22 * modify it under the terms of the GNU General Public License
23 * as published by the Free Software Foundation; either version 2
24 * of the License, or (at your option) any later version.
25 *
26 * This program is distributed in the hope that it will be useful,
27 * but WITHOUT ANY WARRANTY; without even the implied warranty of
28 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
29 * GNU General Public License for more details.
30 *
31 * You should have received a copy of the GNU General Public License
32 * along with this program; if not, write to the Free Software
33 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
34 *
35 * Author: Brian Emre Aydemir
36 * @email{emre@its.caltech.edu}
37 * @end[license]
38 *)
39
40 (*!
41 * @begin[doc]
42 * @parents
43 * @end[doc]
44 *)
45 include Base_theory
46 (*! @docoff *)
47
48 open Refiner.Refiner.Term
49 open Refiner.Refiner.TermOp
50 open Mp_mc_term_op
51
52 (*************************************************************************
53 * Term declarations.
54 *************************************************************************)
55
56 (*!
57 * @begin[doc]
58 * @terms
59 *
60 * @tt{noneOpt} and @tt{someOpt} represent @OCaml option
61 * values, in other words, values of the type @tt{'a option}.
62 * @tt{Some v} is represented as @tt{someOpt@{v@}}.
63 * @end[doc]
64 *)
65
66 declare noneOpt
67 declare someOpt{ 'a }
68
69 (*!
70 * @begin[doc]
71 *
72 * @tt{val_true} and @tt{val_false} represent the @OCaml
73 * boolean constants @tt{true} and @tt{false}.
74 * @end[doc]
75 *)
76 declare val_true
77 declare val_false
78
79 (*!
80 * @begin[doc]
81 *
82 * The FIR has support for integer and floating point types of
83 * various precisions (see @hrefterm[tyRawInt] and @hrefterm[tyFloat]
84 * in @hreftheory[Mp_mc_fir_ty]). The following seven terms specifiy
85 * 8-bit, 16-bit, 32-bit, and 64-bit integer precision as well as
86 * single precision (4 byte), double precision (8 byte), and
87 * long double (10 byte) precision floats. By convention,
88 * subterms called @tt{int_precision} and @tt{float_precision}
89 * refer to one of these terms.
90 * @end[doc]
91 *)
92
93 declare int8
94 declare int16
95 declare int32
96 declare int64
97 declare floatSingle
98 declare floatDouble
99 declare floatLongDouble
100
101 (*!
102 * @begin[doc]
103 *
104 * @hrefterm[tyRawInt] also requires information about whether
105 * the integer type is signed or unsigned, which is what the following
106 * two terms specify. By convention, subterms called @tt{int_signed}
107 * refer to one of these terms.
108 * @end[doc]
109 *)
110
111 declare signedInt
112 declare unsignedInt
113
114 (*!
115 * @begin[doc]
116 *
117 * Integer and raw-integer sets.
118 * @end[doc]
119 *)
120
121 declare interval{ 'left; 'right } (* closed bounds, i.e. [left, right] *)
122 declare int_set{ 'interval_list }
123 declare rawint_set{ 'int_precision; 'int_signed; 'interval_list }
124
125 (*!
126 * @begin[doc]
127 *
128 * Tuple classes.
129 * @end[doc]
130 *)
131
132 declare normalTuple
133 declare rawTuple
134
135
136 (*!
137 * @begin[doc]
138 *
139 * Union types.
140 * @end[doc]
141 *)
142
143 declare normalUnion
144 declare exnUnion
145
146 (*!
147 * @begin[doc]
148 *
149 * Subscript operators.
150 * @end[doc]
151 *)
152
153 (* Kind of block. *)
154
155 declare blockSub
156 declare rawDataSub
157 declare tupleSub
158 declare rawTupleSub
159
160 (* Kind of value. *)
161
162 declare polySub
163 declare rawIntSub{ 'int_precision; 'int_signed }
164 declare rawFloatSub{ 'float_precision }
165 declare pointerInfixSub
166 declare pointerSub
167 declare functionSub
168
169 (* Element width. *)
170
171 declare byteIndex
172 declare wordIndex
173
174 (* Kind of subscript. *)
175
176 declare intIndex
177 declare rawIntIndex{ 'int_precision; 'int_signed }
178
179 (* Subscripting op. *)
180
181 declare subop{ 'sub_block; 'sub_value; 'sub_index; 'sub_script }
182
183 (*! @docoff *)
184
185 (*************************************************************************
186 * Term declarations.
187 *************************************************************************)
188
189 (* Options, i.e. None | Some of 'a. *)
190
191 dform noneOpt_df : except_mode[src] ::
192 noneOpt =
193 `"NoneOpt"
194 dform someOpt_df : except_mode[src] ::
195 someOpt{ 'a } =
196 `"SomeOpt(" slot{'a} `")"
197
198 (* Boolean constants. *)
199
200 dform val_true_df : except_mode[src] ::
201 val_true =
202 `"Val_True"
203 dform val_false_df : except_mode[src] ::
204 val_false =
205 `"Val_False"
206
207 (* Floating-point and integer precisions. *)
208
209 dform int8_df : except_mode[src] ::
210 int8 =
211 `"Int8"
212 dform int16_df : except_mode[src] ::
213 int16 =
214 `"Int16"
215 dform int32_df : except_mode[src] ::
216 int32 =
217 `"Int32"
218 dform int64_df : except_mode[src] ::
219 int64 =
220 `"Int64"
221 dform floatSingle_df : except_mode[src] ::
222 floatSingle =
223 `"Single"
224 dform floatDouble_df : except_mode[src] ::
225 floatDouble =
226 `"Double"
227 dform floatLongDouble_df : except_mode[src] ::
228 floatLongDouble =
229 `"LongDouble"
230
231 (* Signed / unsigned integer qualifiers. *)
232
233 dform signedInt_df : except_mode[src] ::
234 signedInt =
235 `"SignedInt"
236 dform unsignedInt_df : except_mode[src] ::
237 unsignedInt =
238 `"UnsignedInt"
239
240 (* int and rawint sets. *)
241
242 dform interval_df : except_mode[src] ::
243 interval{ 'left; 'right } =
244 `"Interval(" slot{'left} `"," slot{'right} `")"
245 dform int_set_df : except_mode[src] ::
246 int_set{ 'interval_list } =
247 `"Int_set(" slot{'interval_list} `")"
248 dform rawint_set_df : except_mode[src] ::
249 rawint_set{ 'int_precision; 'int_signed; 'interval_list } =
250 `"Rawint_set(" slot{'int_precision} `"," slot{'int_signed} `","
251 slot{'interval_list} `")"
252
253 (* Tuple classes. *)
254
255 dform normalTuple_df : except_mode[src] ::
256 normalTuple =
257 `"NormalTuple"
258 dform rawTuple_df : except_mode[src] ::
259 rawTuple =
260 `"RawTuple"
261
262 (* Union tags. *)
263
264 dform normalUnion_df : except_mode[src] ::
265 normalUnion =
266 `"NormalUnion"
267 dform exnUnion_df : except_mode[src] ::
268 exnUnion =
269 `"ExnUnion"
270
271 (*
272 * Subscript operators.
273 *)
274
275 (* Kind of block. *)
276
277 dform blockSub_df : except_mode[src] ::
278 blockSub =
279 `"BlockSub"
280 dform rawDataSub_df : except_mode[src] ::
281 rawDataSub =
282 `"RawDataSub"
283 dform tupleSub_df : except_mode[src] ::
284 tupleSub =
285 `"TupleSub"
286 dform rawTupleSub_df : except_mode[src] ::
287 rawTupleSub =
288 `"RawTupleSub"
289
290 (* Kind of value. *)
291
292 dform polySub_df : except_mode[src] ::
293 polySub =
294 `"PolySub"
295 dform rawIntSub_df : except_mode[src] ::
296 rawIntSub{ 'int_precision; 'int_signed } =
297 `"RawIntSub(" slot{'int_precision} `"," slot{'int_signed}
298 dform rawFloatSub_df : except_mode[src] ::
299 rawFloatSub{ 'float_precision } =
300 `"RawFloatSub(" slot{'float_precision} `")"
301 dform pointerInfixSUb_df : except_mode[src] ::
302 pointerInfixSub =
303 `"PointerInfixSub"
304 dform pointerSub_df : except_mode[src] ::
305 pointerSub =
306 `"PointerSub"
307 dform functionSub_df : except_mode[src] ::
308 functionSub =
309 `"FunctionSub"
310
311 (* Element width. *)
312
313 dform byteIndex_df : except_mode[src] ::
314 byteIndex =
315 `"ByteIndex"
316 dform wordIndex_df : except_mode[src] ::
317 wordIndex =
318 `"WordIndex"
319
320 (* Kind of subscript. *)
321
322 dform intIndex_df : except_mode[src] ::
323 intIndex =
324 `"IntIndex"
325 dform rawIntIndex_df : except_mode[src] ::
326 rawIntIndex{ 'int_precision; 'int_signed } =
327 `"RawIntIndex(" slot{'int_precision} `"," slot{'int_signed} `")"
328
329 (* Subscripting op. *)
330
331 dform subop_df : except_mode[src] ::
332 subop{ 'sub_block; 'sub_value; 'sub_index; 'sub_script } =
333 `"Subop(" slot{'sub_block} `"," slot{'sub_value} `","
334 slot{'sub_index} `"," slot{'sub_script} `")"
335
336 (*************************************************************************
337 * Term operations.
338 *************************************************************************)
339
340 (* Options, i.e. None | Some of 'a. *)
341
342 let noneOpt_term = << noneOpt >>
343 let noneOpt_opname = opname_of_term noneOpt_term
344 let is_noneOpt_term = is_no_subterms_term noneOpt_opname
345
346 let someOpt_term = << someOpt{ 'a } >>
347 let someOpt_opname = opname_of_term someOpt_term
348 let is_someOpt_term = is_dep0_term someOpt_opname
349 let mk_someOpt_term = mk_dep0_term someOpt_opname
350 let dest_someOpt_term = dest_dep0_term someOpt_opname
351
352 (* Boolean constants. *)
353
354 let val_true_term = << val_true >>
355 let val_true_opname = opname_of_term val_true_term
356 let is_val_true_term = is_no_subterms_term val_true_opname
357
358 let val_false_term = << val_false >>
359 let val_false_opname = opname_of_term val_false_term
360 let is_val_false_term = is_no_subterms_term val_false_opname
361
362 (* Floating-point and integer precisions. *)
363
364 let int8_term = << int8 >>
365 let int8_opname = opname_of_term int8_term
366 let is_int8_term = is_no_subterms_term int8_opname
367
368 let int16_term = << int16 >>
369 let int16_opname = opname_of_term int16_term
370 let is_int16_term = is_no_subterms_term int16_opname
371
372 let int32_term = << int32 >>
373 let int32_opname = opname_of_term int32_term
374 let is_int32_term = is_no_subterms_term int32_opname
375
376 let int64_term = << int64 >>
377 let int64_opname = opname_of_term int64_term
378 let is_int64_term = is_no_subterms_term int64_opname
379
380 let floatSingle_term = << floatSingle >>
381 let floatSingle_opname = opname_of_term floatSingle_term
382 let is_floatSingle_term = is_no_subterms_term floatSingle_opname
383
384 let floatDouble_term = << floatDouble >>
385 let floatDouble_opname = opname_of_term floatDouble_term
386 let is_floatDouble_term = is_no_subterms_term floatDouble_opname
387
388 let floatLongDouble_term = << floatLongDouble >>
389 let floatLongDouble_opname = opname_of_term floatLongDouble_term
390 let is_floatLongDouble_term = is_no_subterms_term floatLongDouble_opname
391
392 (* Signed / unsigned integer qualifiers. *)
393
394 let signedInt_term = << signedInt >>
395 let signedInt_opname = opname_of_term signedInt_term
396 let is_signedInt_term = is_no_subterms_term signedInt_opname
397
398 let unsignedInt_term = << unsignedInt >>
399 let unsignedInt_opname = opname_of_term unsignedInt_term
400 let is_unsignedInt_term = is_no_subterms_term unsignedInt_opname
401
402 (* int and rawint sets. *)
403
404 let interval_term = << interval{ 'left; 'right } >>
405 let interval_opname = opname_of_term interval_term
406 let is_interval_term = is_dep0_dep0_term interval_opname
407 let mk_interval_term = mk_dep0_dep0_term interval_opname
408 let dest_interval_term = dest_dep0_dep0_term interval_opname
409
410 let int_set_term = << int_set{ 'interval_list } >>
411 let int_set_opname = opname_of_term int_set_term
412 let is_int_set_term = is_dep0_term int_set_opname
413 let mk_int_set_term = mk_dep0_term int_set_opname
414 let dest_int_set_term = dest_dep0_term int_set_opname
415
416 let rawint_set_term =
417 << rawint_set{ 'int_precision; 'int_signed; 'interval_list } >>
418 let rawint_set_opname = opname_of_term rawint_set_term
419 let is_rawint_set_term = is_dep0_dep0_dep0_term rawint_set_opname
420 let mk_rawint_set_term = mk_dep0_dep0_dep0_term rawint_set_opname
421 let dest_rawint_set_term = dest_dep0_dep0_dep0_term rawint_set_opname
422
423 (* Tuple classes *)
424
425 let normalTuple_term = << normalTuple >>
426 let normalTuple_opname = opname_of_term normalTuple_term
427 let is_normalTuple_term = is_no_subterms_term normalTuple_opname
428
429 let rawTuple_term = << rawTuple >>
430 let rawTuple_opname = opname_of_term rawTuple_term
431 let is_rawTuple_term = is_no_subterms_term rawTuple_opname
432
433 (* Union tags. *)
434
435 let normalUnion_term = << normalUnion >>
436 let normalUnion_opname = opname_of_term normalUnion_term
437 let is_normalUnion_term = is_no_subterms_term normalUnion_opname
438
439 let exnUnion_term = << exnUnion >>
440 let exnUnion_opname = opname_of_term exnUnion_term
441 let is_exnUnion_term = is_no_subterms_term exnUnion_opname
442
443 (*
444 * Subscript operators.
445 *)
446
447 (* Kind of block. *)
448
449 let blockSub_term = << blockSub >>
450 let blockSub_opname = opname_of_term blockSub_term
451 let is_blockSub_term = is_no_subterms_term blockSub_opname
452
453 let rawDataSub_term = << rawDataSub >>
454 let rawDataSub_opname = opname_of_term rawDataSub_term
455 let is_rawDataSub_term = is_no_subterms_term rawDataSub_opname
456
457 let tupleSub_term = << tupleSub >>
458 let tupleSub_opname = opname_of_term tupleSub_term
459 let is_tupleSub_term = is_no_subterms_term tupleSub_opname
460
461 let rawTupleSub_term = << rawTupleSub >>
462 let rawTupleSub_opname = opname_of_term rawTupleSub_term
463 let is_rawTupleSub_term = is_no_subterms_term rawTupleSub_opname
464
465 (* Kind of value. *)
466
467 let polySub_term = << polySub >>
468 let polySub_opname = opname_of_term polySub_term
469 let is_polySub_term = is_no_subterms_term polySub_opname
470
471 let rawIntSub_term = << rawIntSub{ 'int_precision; 'int_signed } >>
472 let rawIntSub_opname = opname_of_term rawIntSub_term
473 let is_rawIntSub_term = is_dep0_dep0_term rawIntSub_opname
474 let mk_rawIntSub_term = mk_dep0_dep0_term rawIntSub_opname
475 let dest_rawIntSub_term = dest_dep0_dep0_term rawIntSub_opname
476
477 let rawFloatSub_term = << rawFloatSub{ 'float_precision } >>
478 let rawFloatSub_opname = opname_of_term rawFloatSub_term
479 let is_rawFloatSub_term = is_dep0_term rawFloatSub_opname
480 let mk_rawFloatSub_term = mk_dep0_term rawFloatSub_opname
481 let dest_rawFloatSub_term = dest_dep0_term rawFloatSub_opname
482
483 let pointerInfixSub_term = << pointerInfixSub >>
484 let pointerInfixSub_opname = opname_of_term pointerInfixSub_term
485 let is_pointerInfixSub_term = is_no_subterms_term pointerInfixSub_opname
486
487 let pointerSub_term = << pointerSub >>
488 let pointerSub_opname = opname_of_term pointerSub_term
489 let is_pointerSub_term = is_no_subterms_term pointerSub_opname
490
491 let functionSub_term = << functionSub >>
492 let functionSub_opname = opname_of_term functionSub_term
493 let is_functionSub_term = is_no_subterms_term functionSub_opname
494
495 (* Element width. *)
496
497 let byteIndex_term = << byteIndex >>
498 let byteIndex_opname = opname_of_term byteIndex_term
499 let is_byteIndex_term = is_no_subterms_term byteIndex_opname
500
501 let wordIndex_term = << wordIndex >>
502 let wordIndex_opname = opname_of_term wordIndex_term
503 let is_wordIndex_term = is_no_subterms_term wordIndex_opname
504
505 (* Kind of subscript. *)
506
507 let intIndex_term = << intIndex >>
508 let intIndex_opname = opname_of_term intIndex_term
509 let is_intIndex_term = is_no_subterms_term intIndex_opname
510
511 let rawIntIndex_term = << rawIntIndex{ 'int_precision; 'int_signed } >>
512 let rawIntIndex_opname = opname_of_term rawIntIndex_term
513 let is_rawIntIndex_term = is_dep0_dep0_term rawIntIndex_opname
514 let mk_rawIntIndex_term = mk_dep0_dep0_term rawIntIndex_opname
515 let dest_rawIntIndex_term = dest_dep0_dep0_term rawIntIndex_opname
516
517 (* Subscripting op. *)
518
519 let subop_term = << subop{ 'sub_block; 'sub_value; 'sub_index; 'sub_script } >>
520 let subop_opname = opname_of_term subop_term
521 let is_subop_term = is_4_dep0_term subop_opname
522 let mk_subop_term = mk_4_dep0_term subop_opname
523 let dest_subop_term = dest_4_dep0_term subop_opname

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26