/[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 3588 - (hide annotations) (download)
Sat Apr 27 02:45:24 2002 UTC (19 years, 3 months ago) by emre
File size: 6170 byte(s)
Updating modules so that they generate documentation
for theories.pdf.  Right now, it's _very_ minimal and
not so useful.  Hopefully, I will get around to updating
them and making them decent.

Also updating the README file to properly reflect the
name of our research group at Caltech.

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