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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3592 - (hide annotations) (download)
Mon Apr 29 23:15:57 2002 UTC (19 years, 3 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 emre 3588 (*!
2     * @begin[doc]
3     * @theory[Mp_mc_fir_base]
4 emre 3550 *
5 emre 3588 * The @tt{Mp_mc_fir_base} module defines terms to represent basic FIR
6 emre 3590 * terms and supporting @OCaml values.
7 emre 3588 * @end[doc].
8 emre 3550 *
9     * ----------------------------------------------------------------
10     *
11 emre 3588 * @begin[license]
12 emre 3550 * 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 emre 3588 * Copyright (C) 2002 Brian Emre Aydemir, Caltech
20     *
21 emre 3550 * 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 emre 3588 * @email{emre@its.caltech.edu}
37     * @end[license]
38 emre 3550 *)
39    
40 emre 3588 (*!
41     * @begin[doc]
42     * @parents
43     * @end[doc]
44     *)
45 emre 3550 include Base_theory
46 emre 3588 (*! @docoff *)
47 emre 3550
48     open Refiner.Refiner.Term
49     open Refiner.Refiner.TermOp
50 emre 3580 open Mp_mc_term_op
51 emre 3550
52     (*************************************************************************
53     * Term declarations.
54     *************************************************************************)
55    
56 emre 3590 (*!
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 emre 3550
66     declare noneOpt
67     declare someOpt{ 'a }
68    
69 emre 3590 (*!
70     * @begin[doc]
71     *
72     * @tt{val_true} and @tt{val_false} represent the @OCaml
73 emre 3592 * 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 emre 3590 * @end[doc]
77     *)
78 emre 3550 declare val_true
79     declare val_false
80    
81 emre 3590 (*!
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 emre 3550
95     declare int8
96     declare int16
97     declare int32
98     declare int64
99     declare floatSingle
100     declare floatDouble
101     declare floatLongDouble
102    
103 emre 3590 (*!
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 emre 3550
113     declare signedInt
114     declare unsignedInt
115    
116 emre 3590 (*!
117     * @begin[doc]
118     *
119 emre 3592 * 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 emre 3590 * @end[doc]
128     *)
129 emre 3550
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 emre 3590 (*!
135     * @begin[doc]
136     *
137 emre 3592 * Tuple classes. (Documentation incomplete.)
138 emre 3590 * @end[doc]
139     *)
140 emre 3550
141     declare normalTuple
142     declare rawTuple
143    
144    
145 emre 3590 (*!
146     * @begin[doc]
147     *
148 emre 3592 * Union types. (Documentation incomplete.)
149 emre 3590 * @end[doc]
150     *)
151    
152 emre 3550 declare normalUnion
153     declare exnUnion
154    
155 emre 3590 (*!
156     * @begin[doc]
157     *
158 emre 3592 * Subscript operators. (Documentation incomplete.)
159 emre 3590 * @end[doc]
160 emre 3580 *)
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 emre 3589 declare pointerInfixSub
175 emre 3580 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 emre 3590 (*! @docoff *)
193    
194 emre 3550 (*************************************************************************
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 emre 3580 (*
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 emre 3589 dform pointerInfixSUb_df : except_mode[src] ::
311     pointerInfixSub =
312     `"PointerInfixSub"
313 emre 3580 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 emre 3550 (*************************************************************************
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 emre 3580
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 emre 3589 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 emre 3580 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