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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3550 - (show annotations) (download)
Sun Mar 24 22:35:29 2002 UTC (19 years, 4 months ago) by emre
File size: 11646 byte(s)
Updating files to reflect the newest version of the MC FIR (which happens to be
in the websplit branch).  In the process, I've also moved every file in this
theory to use the same prefix for the filenames. I've also removed quite
a few files that have been dead for a while now.

Right now, the "connect" files are not compiled in by default since they will
only compile against the websplit branch of MC and not the trunk.

Lastly, since the definition of FIR evaluation is a bit more precise now,
the need to seperately define constant elimination has been removed.

1 (*
2 * Functional Intermediate Representation formalized in MetaPRL.
3 *
4 * Define terms to represent FIR types and terms.
5 * Specific FIR types represented here: ty, tydef.
6 *
7 * ----------------------------------------------------------------
8 *
9 * Copyright (C) 2002 Brian Emre Aydemir, Caltech
10 *
11 * This file is part of MetaPRL, a modular, higher order
12 * logical framework that provides a logical programming
13 * environment for OCaml and other languages.
14 *
15 * See the file doc/index.html for information on Nuprl,
16 * OCaml, and more information about this system.
17 *
18 * This program is free software; you can redistribute it and/or
19 * modify it under the terms of the GNU General Public License
20 * as published by the Free Software Foundation; either version 2
21 * of the License, or (at your option) any later version.
22 *
23 * This program is distributed in the hope that it will be useful,
24 * but WITHOUT ANY WARRANTY; without even the implied warranty of
25 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
26 * GNU General Public License for more details.
27 *
28 * You should have received a copy of the GNU General Public License
29 * along with this program; if not, write to the Free Software
30 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
31 *
32 * Author: Brian Emre Aydemir
33 * Email: emre@its.caltech.edu
34 *)
35
36 include Base_theory
37
38 open Refiner.Refiner.Term
39 open Refiner.Refiner.TermOp
40
41 (*************************************************************************
42 * Term declarations.
43 *************************************************************************)
44
45 (* Base types. *)
46
47 declare tyInt
48 declare tyEnum{ 'int }
49
50 (* Native types. *)
51
52 declare tyRawInt{ 'int_precision; 'int_signed }
53 declare tyFloat{ 'float_precision }
54
55 (* Functions. *)
56
57 declare tyFun{ 'ty_list; 'ty }
58
59 (* Tuples. *)
60
61 declare tyUnion{ 'ty_var; 'ty_list; 'int_set }
62 declare tyTuple{ 'tuple_class; 'ty_list }
63 declare tyArray{ 'ty }
64 declare tyRawData
65 declare tyPointer{ 'var; 'ty }
66 declare tyFrame{ 'label; 'ty }
67
68 (* Polymorphism. *)
69
70 declare tyVar{ 'ty_var }
71 declare tyApply{ 'ty_var; 'ty_list }
72 declare tyExists{ 'ty_var_list; 'ty }
73 declare tyAll{ 'ty_var_list; 'ty }
74 declare tyProject{ 'var; 'int }
75
76 (* Object-oriented. *)
77
78 declare tyCase{ 'ty }
79 declare tyObject{ 'ty_var; 'ty }
80 declare tyOption{ 'ty }
81
82 (* Delayed type. *)
83
84 declare tyDelayed
85
86 (* Defining types. *)
87
88 declare unionElt{ 'ty; 'bool }
89 declare tyDefUnion{ 'ty_var_list; 'union_type; 'elts }
90 declare tyDefLambda{ 'ty_var_list; 'ty }
91
92 (*************************************************************************
93 * Display forms.
94 *************************************************************************)
95
96 (* Base types. *)
97
98 dform tyInt_df : except_mode[src] ::
99 tyInt =
100 `"TyInt"
101 dform tyEnum_df : except_mode[src] ::
102 tyEnum{ 'int } =
103 `"TyEnum(" slot{'int} `")"
104
105 (* Native types. *)
106
107 dform tyRawInt_df : except_mode[src] ::
108 tyRawInt{ 'int_precision; 'int_signed } =
109 `"TyRawInt(" slot{'int_precision} `"," slot{'int_signed} `")"
110 dform tyFloat_df : except_mode[src] ::
111 tyFloat{ 'float_precision } =
112 `"TyFloat(" slot{'float_precision} `")"
113
114 (* Functions. *)
115
116 dform tyFun_df : except_mode[src] ::
117 tyFun{ 'ty_list; 'ty } =
118 `"TyFun(" slot{'ty_list} `"," slot{'ty} `")"
119
120 (* Tuples. *)
121
122 dform tyUnion_df : except_mode[src] ::
123 tyUnion{ 'ty_var; 'ty_list; 'int_set } =
124 `"TyUnion(" slot{'ty_var} `"," slot{'ty_list} `"," slot{'int_set} `")"
125 dform tyTuple_df : except_mode[src] ::
126 tyTuple{ 'tuple_class; 'ty_list } =
127 `"TyTuple(" slot{'tuple_class} `"," slot{'ty_list} `")"
128 dform tyArray_df : except_mode[src] ::
129 tyArray{ 'ty } =
130 `"TyArray(" slot{'ty} `")"
131 dform tyRawData : except_mode[src] ::
132 tyRawData =
133 `"TyRawData"
134 dform tyPointer_df : except_mode[src] ::
135 tyPointer{ 'var; 'ty } =
136 `"TyPointer(" slot{'var} `"," slot{'ty} `")"
137 dform tyFrame_df : except_mode[src] ::
138 tyFrame{ 'label; 'ty } =
139 `"TyFrame(" slot{'label} `"," slot{'ty} `")"
140
141 (* Polymorphism. *)
142
143 dform tyVar_df : except_mode[src] ::
144 tyVar{ 'ty_var } =
145 `"TyVar(" slot{'ty_var} `")"
146 dform tyApply_df : except_mode[src] ::
147 tyApply{ 'ty_var; 'ty_list } =
148 `"TyApply(" slot{'ty_var} `"," slot{'ty_list} `")"
149 dform tyExists_df : except_mode[src] ::
150 tyExists{ 'ty_var_list; 'ty } =
151 `"TyExists(" slot{'ty_var_list} `"," hspace slot{'ty} `")"
152 dform tyAll_df : except_mode[src] ::
153 tyAll{ 'ty_var_list; 'ty } =
154 `"TyAll(" slot{'ty_var_list} `"," hspace slot{'ty} `")"
155 dform tyProject_df : except_mode[src] ::
156 tyProject{ 'var; 'num } =
157 `"TyProject(" slot{'var} `"," slot{'num} `")"
158
159 (* Object-oriented. *)
160
161 dform tyCase_df : except_mode[src] ::
162 tyCase{ 'ty } =
163 `"TyCase(" slot{'ty} `")"
164 dform tyObject_df : except_mode[src] ::
165 tyObject{ 'ty_var; 'ty } =
166 `"TyObject(" slot{'ty_var} `"," slot{'ty} `")"
167 dform tyOption_df : except_mode[src] ::
168 tyOption{ 'ty } =
169 `"TyOption(" slot{'ty} `")"
170
171 (* Delayed type. Type should be inferred. *)
172
173 dform tyDelayed_df : except_mode[src] ::
174 tyDelayed =
175 `"TyDelayed"
176
177 (* Defining types. *)
178
179 dform unionElt_df : except_mode[src] :: unionElt{ 'ty; 'bool } =
180 `"(" slot{'ty} `"," slot{'bool} ")"
181 dform tyDefUnion_df : except_mode[src] ::
182 tyDefUnion{ 'ty_var_list; 'union_ty; 'elts } =
183 `"TyDefUnion(" slot{'union_ty} `"," slot{'ty_var_list} `"," slot{'elts} `")"
184 dform tyDefLambda_df : except_mode[src] ::
185 tyDefLambda{ 'ty_var_list; 'ty } =
186 `"TyDefLambda(" slot{'ty_var_list} `"," hspace slot{'ty} `")"
187
188 (*************************************************************************
189 * Term operations.
190 *************************************************************************)
191
192 (* Base types. *)
193
194 let tyInt_term = << tyInt >>
195 let tyInt_opname = opname_of_term tyInt_term
196 let is_tyInt_term = is_no_subterms_term tyInt_opname
197
198 let tyEnum_term = << tyEnum{ 'int } >>
199 let tyEnum_opname = opname_of_term tyEnum_term
200 let is_tyEnum_term = is_dep0_term tyEnum_opname
201 let mk_tyEnum_term = mk_dep0_term tyEnum_opname
202 let dest_tyEnum_term = dest_dep0_term tyEnum_opname
203
204 (* Native types. *)
205
206 let tyRawInt_term = << tyRawInt{ 'int_precision; 'int_signed } >>
207 let tyRawInt_opname = opname_of_term tyRawInt_term
208 let is_tyRawInt_term = is_dep0_dep0_term tyRawInt_opname
209 let mk_tyRawInt_term = mk_dep0_dep0_term tyRawInt_opname
210 let dest_tyRawInt_term = dest_dep0_dep0_term tyRawInt_opname
211
212 let tyFloat_term = << tyFloat{ 'float_precision } >>
213 let tyFloat_opname = opname_of_term tyFloat_term
214 let is_tyFloat_term = is_dep0_term tyFloat_opname
215 let mk_tyFloat_term = mk_dep0_term tyFloat_opname
216 let dest_tyFloat_term = dest_dep0_term tyFloat_opname
217
218 (* Functions. *)
219
220 let tyFun_term = << tyFun{ 'ty_list; 'ty } >>
221 let tyFun_opname = opname_of_term tyFun_term
222 let is_tyFun_term = is_dep0_dep0_term tyFun_opname
223 let mk_tyFun_term = mk_dep0_dep0_term tyFun_opname
224 let dest_tyFun_term = dest_dep0_dep0_term tyFun_opname
225
226 (* Tuples. *)
227
228 let tyUnion_term = << tyUnion{ 'ty_var; 'ty_list; 'int_set } >>
229 let tyUnion_opname = opname_of_term tyUnion_term
230 let is_tyUnion_term = is_dep0_dep0_dep0_term tyUnion_opname
231 let mk_tyUnion_term = mk_dep0_dep0_dep0_term tyUnion_opname
232 let dest_tyUnion_term = dest_dep0_dep0_dep0_term tyUnion_opname
233
234 let tyTuple_term = << tyTuple{ 'tuple_class; 'ty_list } >>
235 let tyTuple_opname = opname_of_term tyTuple_term
236 let is_tyTuple_term = is_dep0_dep0_term tyTuple_opname
237 let mk_tyTuple_term = mk_dep0_dep0_term tyTuple_opname
238 let dest_tyTuple_term = dest_dep0_dep0_term tyTuple_opname
239
240 let tyArray_term = << tyArray{ 'ty } >>
241 let tyArray_opname = opname_of_term tyArray_term
242 let is_tyArray_term = is_dep0_term tyArray_opname
243 let mk_tyArray_term = mk_dep0_term tyArray_opname
244 let dest_tyArray_term = dest_dep0_term tyArray_opname
245
246 let tyRawData_term = << tyRawData >>
247 let tyRawData_opname = opname_of_term tyRawData_term
248 let is_tyRawData_term = is_no_subterms_term tyRawData_opname
249
250 let tyPointer_term = << tyPointer{ 'var; 'ty } >>
251 let tyPointer_opname = opname_of_term tyPointer_term
252 let is_tyPointer_term = is_dep0_dep0_term tyPointer_opname
253 let mk_tyPointer_term = mk_dep0_dep0_term tyPointer_opname
254 let dest_tyPointer_term = dest_dep0_dep0_term tyPointer_opname
255
256 let tyFrame_term = << tyFrame{ 'label; 'ty } >>
257 let tyFrame_opname = opname_of_term tyFrame_term
258 let is_tyFrame_term = is_dep0_dep0_term tyFrame_opname
259 let mk_tyFrame_term = mk_dep0_dep0_term tyFrame_opname
260 let dest_tyFrame_term = dest_dep0_dep0_term tyFrame_opname
261
262 (* Polymorphism. *)
263
264 let tyVar_term = << tyVar{ 'ty_var } >>
265 let tyVar_opname = opname_of_term tyVar_term
266 let is_tyVar_term = is_dep0_term tyVar_opname
267 let mk_tyVar_term = mk_dep0_term tyVar_opname
268 let dest_tyVar_term = dest_dep0_term tyVar_opname
269
270 let tyApply_term = << tyApply{ 'ty_var; 'ty_list } >>
271 let tyApply_opname = opname_of_term tyApply_term
272 let is_tyApply_term = is_dep0_dep0_term tyApply_opname
273 let mk_tyApply_term = mk_dep0_dep0_term tyApply_opname
274 let dest_tyApply_term = dest_dep0_dep0_term tyApply_opname
275
276 let tyExists_term = << tyExists{ 'ty_var_list; 'ty } >>
277 let tyExists_opname = opname_of_term tyExists_term
278 let is_tyExists_term = is_dep0_dep0_term tyExists_opname
279 let mk_tyExists_term = mk_dep0_dep0_term tyExists_opname
280 let dest_tyExists_term = dest_dep0_dep0_term tyExists_opname
281
282 let tyAll_term = << tyAll{ 'ty_var_list; 'ty } >>
283 let tyAll_opname = opname_of_term tyAll_term
284 let is_tyAll_term = is_dep0_dep0_term tyAll_opname
285 let mk_tyAll_term = mk_dep0_dep0_term tyAll_opname
286 let dest_tyAll_term = dest_dep0_dep0_term tyAll_opname
287
288 let tyProject_term = << tyProject{ 'var; 'num } >>
289 let tyProject_opname = opname_of_term tyProject_term
290 let is_tyProject_term = is_dep0_dep0_term tyProject_opname
291 let mk_tyProject_term = mk_dep0_dep0_term tyProject_opname
292 let dest_tyProject_term = dest_dep0_dep0_term tyProject_opname
293
294 (* Object-oriented. *)
295
296 let tyCase_term = << tyCase{ 'ty } >>
297 let tyCase_opname = opname_of_term tyCase_term
298 let is_tyCase_term = is_dep0_term tyCase_opname
299 let mk_tyCase_term = mk_dep0_term tyCase_opname
300 let dest_tyCase_term = dest_dep0_term tyCase_opname
301
302 let tyObject_term = << tyObject{ 'ty_var; 'ty } >>
303 let tyObject_opname = opname_of_term tyObject_term
304 let is_tyObject_term = is_dep0_dep0_term tyObject_opname
305 let mk_tyObject_term = mk_dep0_dep0_term tyObject_opname
306 let dest_tyObject_term = dest_dep0_dep0_term tyObject_opname
307
308 let tyOption_term = << tyOption{ 'ty } >>
309 let tyOption_opname = opname_of_term tyOption_term
310 let is_tyOption_term = is_dep0_term tyOption_opname
311 let mk_tyOption_term = mk_dep0_term tyOption_opname
312 let dest_tyOption_term = dest_dep0_term tyOption_opname
313
314 (* Delayed type. *)
315
316 let tyDelayed_term = << tyDelayed >>
317 let tyDelayed_opname = opname_of_term tyDelayed_term
318 let is_tyDelayed_term = is_no_subterms_term tyDelayed_opname
319
320 (* Defining types. *)
321
322 let unionElt_term = << unionElt{ 'ty; 'bool } >>
323 let unionElt_opname = opname_of_term unionElt_term
324 let is_unionElt_term = is_dep0_dep0_term unionElt_opname
325 let mk_unionElt_term = mk_dep0_dep0_term unionElt_opname
326 let dest_unionElt_term = dest_dep0_dep0_term unionElt_opname
327
328 let tyDefUnion_term = << tyDefUnion{ 'ty_var_list; 'union_type; 'elts } >>
329 let tyDefUnion_opname = opname_of_term tyDefUnion_term
330 let is_tyDefUnion_term = is_dep0_dep0_dep0_term tyDefUnion_opname
331 let mk_tyDefUnion_term = mk_dep0_dep0_dep0_term tyDefUnion_opname
332 let dest_tyDefUnion_term = dest_dep0_dep0_dep0_term tyDefUnion_opname
333
334 let tyDefLambda_term = << tyDefLambda{ 'ty_var_list; 'ty } >>
335 let tyDefLambda_opname = opname_of_term tyDefLambda_term
336 let is_tyDefLambda_term = is_dep0_dep0_term tyDefLambda_opname
337 let mk_tyDefLambda_term = mk_dep0_dep0_term tyDefLambda_opname
338 let dest_tyDefLambda_term = dest_dep0_dep0_term tyDefLambda_opname

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26