/[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 3592 - (show annotations) (download)
Mon Apr 29 23:15:57 2002 UTC (19 years, 2 months ago) by emre
File size: 15472 byte(s)
Some more documentation.  I'll be able to document more things
when the MC developers document their stuff a bit more.
I've changed the order in which the modules of the mc theory
are printed so that I can put an overview of the theory
in Mp_mc_theory and have that serve as an introduction to the
rest of the modules.  (This over view is not currently in there,
but should be on my next commit.)

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