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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3563 - (hide 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 emre 3550 (*
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 emre 3563 declare tyFrame{ 'label }
67 emre 3550
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 emre 3563 tyFrame{ 'label } =
139     `"TyFrame(" slot{'label} `")"
140 emre 3550
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 emre 3563 let tyFrame_term = << tyFrame{ 'label } >>
257 emre 3550 let tyFrame_opname = opname_of_term tyFrame_term
258 emre 3563 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 emre 3550
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