/[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 3580 - (hide annotations) (download)
Fri Apr 19 08:09:21 2002 UTC (19 years, 3 months ago) by emre
File size: 11210 byte(s)
Comitting more changes 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 emre 3580 declare tyPointer{ 'sub_block }
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    
81     (* Delayed type. *)
82    
83     declare tyDelayed
84    
85     (* Defining types. *)
86    
87     declare unionElt{ 'ty; 'bool }
88     declare tyDefUnion{ 'ty_var_list; 'union_type; 'elts }
89     declare tyDefLambda{ 'ty_var_list; 'ty }
90    
91     (*************************************************************************
92     * Display forms.
93     *************************************************************************)
94    
95     (* Base types. *)
96    
97     dform tyInt_df : except_mode[src] ::
98     tyInt =
99     `"TyInt"
100     dform tyEnum_df : except_mode[src] ::
101     tyEnum{ 'int } =
102     `"TyEnum(" slot{'int} `")"
103    
104     (* Native types. *)
105    
106     dform tyRawInt_df : except_mode[src] ::
107     tyRawInt{ 'int_precision; 'int_signed } =
108     `"TyRawInt(" slot{'int_precision} `"," slot{'int_signed} `")"
109     dform tyFloat_df : except_mode[src] ::
110     tyFloat{ 'float_precision } =
111     `"TyFloat(" slot{'float_precision} `")"
112    
113     (* Functions. *)
114    
115     dform tyFun_df : except_mode[src] ::
116     tyFun{ 'ty_list; 'ty } =
117     `"TyFun(" slot{'ty_list} `"," slot{'ty} `")"
118    
119     (* Tuples. *)
120    
121     dform tyUnion_df : except_mode[src] ::
122     tyUnion{ 'ty_var; 'ty_list; 'int_set } =
123     `"TyUnion(" slot{'ty_var} `"," slot{'ty_list} `"," slot{'int_set} `")"
124     dform tyTuple_df : except_mode[src] ::
125     tyTuple{ 'tuple_class; 'ty_list } =
126     `"TyTuple(" slot{'tuple_class} `"," slot{'ty_list} `")"
127     dform tyArray_df : except_mode[src] ::
128     tyArray{ 'ty } =
129     `"TyArray(" slot{'ty} `")"
130     dform tyRawData : except_mode[src] ::
131     tyRawData =
132     `"TyRawData"
133     dform tyPointer_df : except_mode[src] ::
134 emre 3580 tyPointer{ 'sub_block } =
135     `"TyPointer(" slot{'sub_block} `")"
136 emre 3550 dform tyFrame_df : except_mode[src] ::
137 emre 3563 tyFrame{ 'label } =
138     `"TyFrame(" slot{'label} `")"
139 emre 3550
140     (* Polymorphism. *)
141    
142     dform tyVar_df : except_mode[src] ::
143     tyVar{ 'ty_var } =
144     `"TyVar(" slot{'ty_var} `")"
145     dform tyApply_df : except_mode[src] ::
146     tyApply{ 'ty_var; 'ty_list } =
147     `"TyApply(" slot{'ty_var} `"," slot{'ty_list} `")"
148     dform tyExists_df : except_mode[src] ::
149     tyExists{ 'ty_var_list; 'ty } =
150     `"TyExists(" slot{'ty_var_list} `"," hspace slot{'ty} `")"
151     dform tyAll_df : except_mode[src] ::
152     tyAll{ 'ty_var_list; 'ty } =
153     `"TyAll(" slot{'ty_var_list} `"," hspace slot{'ty} `")"
154     dform tyProject_df : except_mode[src] ::
155     tyProject{ 'var; 'num } =
156     `"TyProject(" slot{'var} `"," slot{'num} `")"
157    
158     (* Object-oriented. *)
159    
160     dform tyCase_df : except_mode[src] ::
161     tyCase{ 'ty } =
162     `"TyCase(" slot{'ty} `")"
163     dform tyObject_df : except_mode[src] ::
164     tyObject{ 'ty_var; 'ty } =
165     `"TyObject(" slot{'ty_var} `"," slot{'ty} `")"
166    
167     (* Delayed type. Type should be inferred. *)
168    
169     dform tyDelayed_df : except_mode[src] ::
170     tyDelayed =
171     `"TyDelayed"
172    
173     (* Defining types. *)
174    
175     dform unionElt_df : except_mode[src] :: unionElt{ 'ty; 'bool } =
176     `"(" slot{'ty} `"," slot{'bool} ")"
177     dform tyDefUnion_df : except_mode[src] ::
178     tyDefUnion{ 'ty_var_list; 'union_ty; 'elts } =
179     `"TyDefUnion(" slot{'union_ty} `"," slot{'ty_var_list} `"," slot{'elts} `")"
180     dform tyDefLambda_df : except_mode[src] ::
181     tyDefLambda{ 'ty_var_list; 'ty } =
182     `"TyDefLambda(" slot{'ty_var_list} `"," hspace slot{'ty} `")"
183    
184     (*************************************************************************
185     * Term operations.
186     *************************************************************************)
187    
188     (* Base types. *)
189    
190     let tyInt_term = << tyInt >>
191     let tyInt_opname = opname_of_term tyInt_term
192     let is_tyInt_term = is_no_subterms_term tyInt_opname
193    
194     let tyEnum_term = << tyEnum{ 'int } >>
195     let tyEnum_opname = opname_of_term tyEnum_term
196     let is_tyEnum_term = is_dep0_term tyEnum_opname
197     let mk_tyEnum_term = mk_dep0_term tyEnum_opname
198     let dest_tyEnum_term = dest_dep0_term tyEnum_opname
199    
200     (* Native types. *)
201    
202     let tyRawInt_term = << tyRawInt{ 'int_precision; 'int_signed } >>
203     let tyRawInt_opname = opname_of_term tyRawInt_term
204     let is_tyRawInt_term = is_dep0_dep0_term tyRawInt_opname
205     let mk_tyRawInt_term = mk_dep0_dep0_term tyRawInt_opname
206     let dest_tyRawInt_term = dest_dep0_dep0_term tyRawInt_opname
207    
208     let tyFloat_term = << tyFloat{ 'float_precision } >>
209     let tyFloat_opname = opname_of_term tyFloat_term
210     let is_tyFloat_term = is_dep0_term tyFloat_opname
211     let mk_tyFloat_term = mk_dep0_term tyFloat_opname
212     let dest_tyFloat_term = dest_dep0_term tyFloat_opname
213    
214     (* Functions. *)
215    
216     let tyFun_term = << tyFun{ 'ty_list; 'ty } >>
217     let tyFun_opname = opname_of_term tyFun_term
218     let is_tyFun_term = is_dep0_dep0_term tyFun_opname
219     let mk_tyFun_term = mk_dep0_dep0_term tyFun_opname
220     let dest_tyFun_term = dest_dep0_dep0_term tyFun_opname
221    
222     (* Tuples. *)
223    
224     let tyUnion_term = << tyUnion{ 'ty_var; 'ty_list; 'int_set } >>
225     let tyUnion_opname = opname_of_term tyUnion_term
226     let is_tyUnion_term = is_dep0_dep0_dep0_term tyUnion_opname
227     let mk_tyUnion_term = mk_dep0_dep0_dep0_term tyUnion_opname
228     let dest_tyUnion_term = dest_dep0_dep0_dep0_term tyUnion_opname
229    
230     let tyTuple_term = << tyTuple{ 'tuple_class; 'ty_list } >>
231     let tyTuple_opname = opname_of_term tyTuple_term
232     let is_tyTuple_term = is_dep0_dep0_term tyTuple_opname
233     let mk_tyTuple_term = mk_dep0_dep0_term tyTuple_opname
234     let dest_tyTuple_term = dest_dep0_dep0_term tyTuple_opname
235    
236     let tyArray_term = << tyArray{ 'ty } >>
237     let tyArray_opname = opname_of_term tyArray_term
238     let is_tyArray_term = is_dep0_term tyArray_opname
239     let mk_tyArray_term = mk_dep0_term tyArray_opname
240     let dest_tyArray_term = dest_dep0_term tyArray_opname
241    
242     let tyRawData_term = << tyRawData >>
243     let tyRawData_opname = opname_of_term tyRawData_term
244     let is_tyRawData_term = is_no_subterms_term tyRawData_opname
245    
246 emre 3580 let tyPointer_term = << tyPointer{ 'sub_block } >>
247 emre 3550 let tyPointer_opname = opname_of_term tyPointer_term
248 emre 3580 let is_tyPointer_term = is_dep0_term tyPointer_opname
249     let mk_tyPointer_term = mk_dep0_term tyPointer_opname
250     let dest_tyPointer_term = dest_dep0_term tyPointer_opname
251 emre 3550
252 emre 3563 let tyFrame_term = << tyFrame{ 'label } >>
253 emre 3550 let tyFrame_opname = opname_of_term tyFrame_term
254 emre 3563 let is_tyFrame_term = is_dep0_term tyFrame_opname
255     let mk_tyFrame_term = mk_dep0_term tyFrame_opname
256     let dest_tyFrame_term = dest_dep0_term tyFrame_opname
257 emre 3550
258     (* Polymorphism. *)
259    
260     let tyVar_term = << tyVar{ 'ty_var } >>
261     let tyVar_opname = opname_of_term tyVar_term
262     let is_tyVar_term = is_dep0_term tyVar_opname
263     let mk_tyVar_term = mk_dep0_term tyVar_opname
264     let dest_tyVar_term = dest_dep0_term tyVar_opname
265    
266     let tyApply_term = << tyApply{ 'ty_var; 'ty_list } >>
267     let tyApply_opname = opname_of_term tyApply_term
268     let is_tyApply_term = is_dep0_dep0_term tyApply_opname
269     let mk_tyApply_term = mk_dep0_dep0_term tyApply_opname
270     let dest_tyApply_term = dest_dep0_dep0_term tyApply_opname
271    
272     let tyExists_term = << tyExists{ 'ty_var_list; 'ty } >>
273     let tyExists_opname = opname_of_term tyExists_term
274     let is_tyExists_term = is_dep0_dep0_term tyExists_opname
275     let mk_tyExists_term = mk_dep0_dep0_term tyExists_opname
276     let dest_tyExists_term = dest_dep0_dep0_term tyExists_opname
277    
278     let tyAll_term = << tyAll{ 'ty_var_list; 'ty } >>
279     let tyAll_opname = opname_of_term tyAll_term
280     let is_tyAll_term = is_dep0_dep0_term tyAll_opname
281     let mk_tyAll_term = mk_dep0_dep0_term tyAll_opname
282     let dest_tyAll_term = dest_dep0_dep0_term tyAll_opname
283    
284     let tyProject_term = << tyProject{ 'var; 'num } >>
285     let tyProject_opname = opname_of_term tyProject_term
286     let is_tyProject_term = is_dep0_dep0_term tyProject_opname
287     let mk_tyProject_term = mk_dep0_dep0_term tyProject_opname
288     let dest_tyProject_term = dest_dep0_dep0_term tyProject_opname
289    
290     (* Object-oriented. *)
291    
292     let tyCase_term = << tyCase{ 'ty } >>
293     let tyCase_opname = opname_of_term tyCase_term
294     let is_tyCase_term = is_dep0_term tyCase_opname
295     let mk_tyCase_term = mk_dep0_term tyCase_opname
296     let dest_tyCase_term = dest_dep0_term tyCase_opname
297    
298     let tyObject_term = << tyObject{ 'ty_var; 'ty } >>
299     let tyObject_opname = opname_of_term tyObject_term
300     let is_tyObject_term = is_dep0_dep0_term tyObject_opname
301     let mk_tyObject_term = mk_dep0_dep0_term tyObject_opname
302     let dest_tyObject_term = dest_dep0_dep0_term tyObject_opname
303    
304     (* Delayed type. *)
305    
306     let tyDelayed_term = << tyDelayed >>
307     let tyDelayed_opname = opname_of_term tyDelayed_term
308     let is_tyDelayed_term = is_no_subterms_term tyDelayed_opname
309    
310     (* Defining types. *)
311    
312     let unionElt_term = << unionElt{ 'ty; 'bool } >>
313     let unionElt_opname = opname_of_term unionElt_term
314     let is_unionElt_term = is_dep0_dep0_term unionElt_opname
315     let mk_unionElt_term = mk_dep0_dep0_term unionElt_opname
316     let dest_unionElt_term = dest_dep0_dep0_term unionElt_opname
317    
318     let tyDefUnion_term = << tyDefUnion{ 'ty_var_list; 'union_type; 'elts } >>
319     let tyDefUnion_opname = opname_of_term tyDefUnion_term
320     let is_tyDefUnion_term = is_dep0_dep0_dep0_term tyDefUnion_opname
321     let mk_tyDefUnion_term = mk_dep0_dep0_dep0_term tyDefUnion_opname
322     let dest_tyDefUnion_term = dest_dep0_dep0_dep0_term tyDefUnion_opname
323    
324     let tyDefLambda_term = << tyDefLambda{ 'ty_var_list; 'ty } >>
325     let tyDefLambda_opname = opname_of_term tyDefLambda_term
326     let is_tyDefLambda_term = is_dep0_dep0_term tyDefLambda_opname
327     let mk_tyDefLambda_term = mk_dep0_dep0_term tyDefLambda_opname
328     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