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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3590 - (hide annotations) (download)
Sat Apr 27 19:52:38 2002 UTC (19 years, 3 months ago) by emre
File size: 6270 byte(s)
Adding some documentation.  Still have a long ways to go
in fully documenting everything.

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