/[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 3563 - (show annotations) (download)
Fri Apr 5 01:16:49 2002 UTC (19 years, 4 months ago) by emre
File size: 11601 byte(s)
Updates to reflect the (ever changing) MC FIR.

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 }
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 } =
139 `"TyFrame(" slot{'label} `")"
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 } >>
257 let tyFrame_opname = opname_of_term tyFrame_term
258 let is_tyFrame_term = is_dep0_term tyFrame_opname
259 let mk_tyFrame_term = mk_dep0_term tyFrame_opname
260 let dest_tyFrame_term = dest_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