/[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 3550 - (hide 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 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     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