/[mojave]/metaprl/theories/mc/mp_mc_fir_exp.mli
ViewVC logotype

Annotation of /metaprl/theories/mc/mp_mc_fir_exp.mli

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: 27860 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: unop, binop, sub_block, sub_value,
6     * sub_index, sub_script, atom, alloc_op, tailop, pred_nop, pred_unop,
7 emre 3562 * pred_binop, pred, debug_line, debug_vars, debug_info, exp, fundef.
8 emre 3550 *
9     * ----------------------------------------------------------------
10     *
11     * Copyright (C) 2002 Brian Emre Aydemir, Caltech
12     *
13     * This file is part of MetaPRL, a modular, higher order
14     * logical framework that provides a logical programming
15     * environment for OCaml and other languages.
16     *
17     * See the file doc/index.html for information on Nuprl,
18     * OCaml, and more information about this system.
19     *
20     * This program is free software; you can redistribute it and/or
21     * modify it under the terms of the GNU General Public License
22     * as published by the Free Software Foundation; either version 2
23     * of the License, or (at your option) any later version.
24     *
25     * This program is distributed in the hope that it will be useful,
26     * but WITHOUT ANY WARRANTY; without even the implied warranty of
27     * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
28     * GNU General Public License for more details.
29     *
30     * You should have received a copy of the GNU General Public License
31     * along with this program; if not, write to the Free Software
32     * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
33     *
34     * Author: Brian Emre Aydemir
35     * Email: emre@its.caltech.edu
36     *)
37    
38     include Base_theory
39    
40     open Refiner.Refiner.Term
41    
42     (*************************************************************************
43     * Declarations.
44     *************************************************************************)
45    
46     (*
47     * Unary operations.
48     *)
49    
50     (* Identity (polymorphic). *)
51    
52     declare idOp
53    
54     (* Naml ints. *)
55    
56     declare uminusIntOp
57     declare notIntOp
58    
59     (* Bit fields. *)
60    
61     declare rawBitFieldOp{ 'int_precision; 'int_signed; 'int1; 'int2 }
62    
63     (* Native ints. *)
64    
65     declare uminusRawIntOp{ 'int_precision; 'int_signed }
66     declare notRawIntOp{ 'int_precision; 'int_signed }
67    
68     (* Floats. *)
69    
70     declare uminusFloatOp{ 'float_precision }
71     declare absFloatOp{ 'float_precision }
72     declare sinOp{ 'float_precision }
73     declare cosOp{ 'float_precision }
74     declare sqrtOp{ 'float_precision }
75    
76     (* Coerce to int. *)
77    
78     declare intOfFloatOp{ 'float_precision }
79    
80     (* Coerce to float. *)
81    
82     declare floatOfIntOp{ 'float_precision }
83     declare floatOfFloatOp{ 'float_precision1; 'float_precision2 }
84     declare floatOfRawIntOp{ 'float_precision; 'int_precision; 'int_signed }
85    
86     (* Coerce to rawint. *)
87    
88     declare rawIntOfIntOp{ 'int_precision; 'int_signed }
89     declare rawIntOfEnumOp{ 'int_precision; 'int_signed; 'int }
90     declare rawIntOfFloatOp{ 'int_precision; 'int_signed; 'float_precision }
91     declare rawIntOfRawIntOp{ 'dest_int_precision; 'dest_int_signed;
92     'src_int_precision; 'src_int_signed }
93    
94     (* Integer/pointer coercions. *)
95    
96     declare rawIntOfPointerOp{ 'int_precision; 'int_signed }
97     declare pointerOfRawIntOp{ 'int_precision; 'int_signed }
98    
99 emre 3580 (* Pointer from a block pointer. *)
100 emre 3563
101 emre 3580 declare pointerOfBlockOp{ 'sub_block }
102 emre 3563
103 emre 3550 (*
104     * Binary operations.
105     *)
106    
107     (* Enums. *)
108    
109     declare andEnumOp{ 'int }
110     declare orEnumOp{ 'int }
111     declare xorEnumOp{ 'int }
112    
113     (* Naml ints. *)
114    
115     declare plusIntOp
116     declare minusIntOp
117     declare mulIntOp
118     declare divIntOp
119     declare remIntOp
120     declare lslIntOp
121     declare lsrIntOp
122     declare asrIntOp
123     declare andIntOp
124     declare orIntOp
125     declare xorIntOp
126     declare maxIntOp
127     declare minIntOp
128    
129     declare eqIntOp
130     declare neqIntOp
131     declare ltIntOp
132     declare leIntOp
133     declare gtIntOp
134     declare geIntOp
135     declare cmpIntOp
136    
137     (* Native ints. *)
138    
139     declare plusRawIntOp{ 'int_precision; 'int_signed }
140     declare minusRawIntOp{ 'int_precision; 'int_signed }
141     declare mulRawIntOp{ 'int_precision; 'int_signed }
142     declare divRawIntOp{ 'int_precision; 'int_signed }
143     declare remRawIntOp{ 'int_precision; 'int_signed }
144     declare slRawIntOp{ 'int_precision; 'int_signed }
145     declare srRawIntOp{ 'int_precision; 'int_signed }
146     declare andRawIntOp{ 'int_precision; 'int_signed }
147     declare orRawIntOp{ 'int_precision; 'int_signed }
148     declare xorRawIntOp{ 'int_precision; 'int_signed }
149     declare maxRawIntOp{ 'int_precision; 'int_signed }
150     declare minRawIntOp{ 'int_precision; 'int_signed }
151    
152     declare rawSetBitFieldOp{ 'int_precision; 'int_signed; 'int1; 'int2 }
153    
154     declare eqRawIntOp{ 'int_precision; 'int_signed }
155     declare neqRawIntOp{ 'int_precision; 'int_signed }
156     declare ltRawIntOp{ 'int_precision; 'int_signed }
157     declare leRawIntOp{ 'int_precision; 'int_signed }
158     declare gtRawIntOp{ 'int_precision; 'int_signed }
159     declare geRawIntOp{ 'int_precision; 'int_signed }
160     declare cmpRawIntOp{ 'int_precision; 'int_signed }
161    
162     (* Floats. *)
163    
164     declare plusFloatOp{ 'float_precision }
165     declare minusFloatOp{ 'float_precision }
166     declare mulFloatOp{ 'float_precision }
167     declare divFloatOp{ 'float_precision }
168     declare remFloatOp{ 'float_precision }
169     declare maxFloatOp{ 'float_precision }
170     declare minFloatOp{ 'float_precision }
171    
172     declare eqFloatOp{ 'float_precision }
173     declare neqFloatOp{ 'float_precision }
174     declare ltFloatOp{ 'float_precision }
175     declare leFloatOp{ 'float_precision }
176     declare gtFloatOp{ 'float_precision }
177     declare geFloatOp{ 'float_precision }
178     declare cmpFloatOp{ 'float_precision }
179    
180     declare atan2Op{ 'float_precision }
181    
182     (* Pointer equality. *)
183    
184     declare eqEqOp
185     declare neqEqOp
186    
187     (* Pointer arithmetic. *)
188    
189 emre 3580 declare plusPointerOp{ 'sub_block; 'int_precision; 'int_signed }
190 emre 3550
191     (*
192 emre 3563 * Fields (frame labels).
193     *)
194    
195     declare frameLabel{ 'label1; 'label2; 'label3 }
196    
197     (*
198 emre 3550 * Normal values.
199     *)
200    
201     declare atomNil{ 'ty }
202     declare atomInt{ 'int }
203 emre 3564 declare atomEnum{ 'int1; 'int2 } (* 'int1 = bound, 'int2 = value *)
204 emre 3550 declare atomRawInt{ 'int_precision; 'int_signed; 'num }
205     declare atomFloat{ 'float_precision; 'num }
206 emre 3580 declare atomLabel{ 'frame_label; 'atom_rawint }
207     declare atomSizeof{ 'var_list; 'atom_rawint }
208 emre 3550 declare atomConst{ 'ty; 'ty_var; 'int }
209     declare atomVar{ 'var }
210    
211     (*
212     * Allocation operators.
213     *)
214    
215     declare allocTuple{ 'tuple_class; 'ty; 'atom_list }
216     declare allocUnion{ 'ty; 'ty_var; 'int; 'atom_list }
217     declare allocArray{ 'ty; 'atom_list }
218     declare allocVArray{ 'ty; 'sub_index; 'atom1; 'atom2 }
219     declare allocMalloc{ 'ty; 'atom }
220 emre 3563 declare allocFrame{ 'var }
221 emre 3550
222     (*
223     * Tail calls / operations.
224     *)
225    
226     declare tailSysMigrate{ 'int; 'atom1; 'atom2; 'var; 'atom_list }
227     declare tailAtomic{ 'var; 'atom; 'atom_list }
228     declare tailAtomicRollback{ 'atom }
229     declare tailAtomicCommit{ 'var; 'atom_list }
230    
231     (*
232     * Predicates and assertions.
233     *)
234    
235 emre 3580 declare isMutable{ 'var }
236     declare reserve{ 'atom1; 'atom2 }
237     declare boundsCheck{ 'subop; 'var; 'atom1; 'atom2 }
238     declare elementCheck{ 'ty; 'subop; 'var; 'atom }
239 emre 3550
240     (*
241     * Debugging info.
242     *)
243    
244     declare debugLine{ 'string; 'int }
245     declare debugVarItem{ 'var1; 'ty; 'var2 }
246     declare debugVars{ 'debugVarItem_list }
247     declare debugString{ 'string }
248     declare debugContext{ 'debug_line; 'debug_vars }
249    
250     (*
251     * Expressions.
252     *)
253    
254     (* Primitive operations. *)
255    
256     declare letUnop{ 'ty; 'unop; 'atom; var. 'exp['var] }
257     declare letBinop{ 'ty; 'binop; 'atom1; 'atom2; var. 'exp['var] }
258    
259     (* Function application. *)
260    
261     declare letExt{ 'ty1; 'string; 'ty2; 'atom_list; var. 'exp['var] }
262 emre 3563 declare tailCall{ 'label; 'var; 'atom_list }
263     declare specialCall{ 'label; 'tailop }
264 emre 3550
265     (* Control. *)
266    
267 emre 3563 declare matchCase{ 'label; 'set; 'exp }
268 emre 3550 declare matchExp{ 'atom; 'matchCase_list }
269     declare typeCase{ 'atom1; 'atom2; 'var1; 'var2; 'exp1; 'exp2 }
270    
271     (* Allocation. *)
272    
273     declare letAlloc{ 'alloc_op; var. 'exp['var] }
274    
275     (* Subscripting. *)
276    
277     declare letSubscript{ 'subop; 'ty; 'var2; 'atom; var1. 'exp['var1] }
278     declare setSubscript{ 'subop; 'label; 'var; 'atom1; 'ty; 'atom2; 'exp }
279     declare setGlobal{ 'sub_value; 'label; 'var; 'ty; 'atom; 'exp }
280     declare memcpy{ 'subop; 'label; 'var1; 'atom1; 'var2; 'atom2; 'atom3; 'exp }
281    
282     (* Assertions. *)
283    
284 emre 3563 declare call{ 'label; 'var; 'atom_option_list; 'exp }
285 emre 3550 declare assertExp{ 'label; 'pred; 'exp }
286    
287     (* Debugging. *)
288    
289     declare debug{ 'debug_info; 'exp }
290    
291 emre 3562 (*
292     * Function definition.
293     *)
294    
295     declare fundef{ 'debug_line; 'ty; 'var_list; 'exp }
296    
297 emre 3550 (*************************************************************************
298     * Term operations.
299     *************************************************************************)
300    
301     (*
302     * Unary operations.
303     *)
304    
305     (* Identity (polymorphic). *)
306    
307     val idOp_term : term
308     val is_idOp_term : term -> bool
309    
310     (* Naml ints. *)
311    
312     val uminusIntOp_term : term
313     val is_uminusIntOp_term : term -> bool
314    
315     val notIntOp_term : term
316     val is_notIntOp_term : term -> bool
317    
318     (* Bit fields. *)
319    
320     val rawBitFieldOp_term : term
321     val is_rawBitFieldOp_term : term -> bool
322     val mk_rawBitFieldOp_term : term -> term -> term -> term -> term
323     val dest_rawBitFieldOp_term : term -> term * term * term * term
324    
325     (* Native ints. *)
326    
327     val uminusRawIntOp_term : term
328     val is_uminusRawIntOp_term : term -> bool
329     val mk_uminusRawIntOp_term : term -> term -> term
330     val dest_uminusRawIntOp_term : term -> term * term
331    
332     val notRawIntOp_term : term
333     val is_notRawIntOp_term : term -> bool
334     val mk_notRawIntOp_term : term -> term -> term
335     val dest_notRawIntOp_term : term -> term * term
336    
337     (* Floats. *)
338    
339     val uminusFloatOp_term : term
340     val is_uminusFloatOp_term : term -> bool
341     val mk_uminusFloatOp_term : term -> term
342     val dest_uminusFloatOp_term : term -> term
343    
344     val absFloatOp_term : term
345     val is_absFloatOp_term : term -> bool
346     val mk_absFloatOp_term : term -> term
347     val dest_absFloatOp_term : term -> term
348    
349     val sinOp_term : term
350     val is_sinOp_term : term -> bool
351     val mk_sinOp_term : term -> term
352     val dest_sinOp_term : term -> term
353    
354     val cosOp_term : term
355     val is_cosOp_term : term -> bool
356     val mk_cosOp_term : term -> term
357     val dest_cosOp_term : term -> term
358    
359     val sqrtOp_term : term
360     val is_sqrtOp_term : term -> bool
361     val mk_sqrtOp_term : term -> term
362     val dest_sqrtOp_term : term -> term
363    
364     (* Coerce to int. *)
365    
366     val intOfFloatOp_term : term
367     val is_intOfFloatOp_term : term -> bool
368     val mk_intOfFloatOp_term : term -> term
369     val dest_intOfFloatOp_term : term -> term
370    
371     (* Coerce to float. *)
372    
373     val floatOfIntOp_term : term
374     val is_floatOfIntOp_term : term -> bool
375     val mk_floatOfIntOp_term : term -> term
376     val dest_floatOfIntOp_term : term -> term
377    
378     val floatOfFloatOp_term : term
379     val is_floatOfFloatOp_term : term -> bool
380     val mk_floatOfFloatOp_term : term -> term -> term
381     val dest_floatOfFloatOp_term : term -> term * term
382    
383     val floatOfRawIntOp_term : term
384     val is_floatOfRawIntOp_term : term -> bool
385     val mk_floatOfRawIntOp_term : term -> term -> term -> term
386     val dest_floatOfRawIntOp_term : term -> term * term * term
387    
388     (* Coerce to rawint. *)
389    
390     val rawIntOfIntOp_term : term
391     val is_rawIntOfIntOp_term : term -> bool
392     val mk_rawIntOfIntOp_term : term -> term -> term
393     val dest_rawIntOfIntOp_term : term -> term * term
394    
395     val rawIntOfEnumOp_term : term
396     val is_rawIntOfEnumOp_term : term -> bool
397     val mk_rawIntOfEnumOp_term : term -> term -> term -> term
398     val dest_rawIntOfEnumOp_term : term -> term * term * term
399    
400     val rawIntOfFloatOp_term : term
401     val is_rawIntOfFloatOp_term : term -> bool
402     val mk_rawIntOfFloatOp_term : term -> term -> term -> term
403     val dest_rawIntOfFloatOp_term : term -> term * term * term
404    
405     val rawIntOfRawIntOp_term : term
406     val is_rawIntOfRawIntOp_term : term -> bool
407     val mk_rawIntOfRawIntOp_term : term -> term -> term -> term -> term
408     val dest_rawIntOfRawIntOp_term : term -> term * term * term * term
409    
410     (* Integer/pointer coercions. *)
411    
412     val rawIntOfPointerOp_term : term
413     val is_rawIntOfPointerOp_term : term -> bool
414     val mk_rawIntOfPointerOp_term : term -> term -> term
415     val dest_rawIntOfPointerOp_term : term -> term * term
416    
417     val pointerOfRawIntOp_term : term
418     val is_pointerOfRawIntOp_term : term -> bool
419     val mk_pointerOfRawIntOp_term : term -> term -> term
420     val dest_pointerOfRawIntOp_term : term -> term * term
421    
422 emre 3580 val pointerOfBlockOp_term : term
423     val is_pointerOfBlockOp_term : term -> bool
424     val mk_pointerOfBlockOp_term : term -> term
425     val dest_pointerOfBlockOp_term : term -> term
426 emre 3563
427 emre 3550 (*
428     * Binary operations.
429     *)
430    
431     (* Enums. *)
432    
433     val andEnumOp_term : term
434     val is_andEnumOp_term : term -> bool
435     val mk_andEnumOp_term : term -> term
436     val dest_andEnumOp_term : term -> term
437    
438     val orEnumOp_term : term
439     val is_orEnumOp_term : term -> bool
440     val mk_orEnumOp_term : term -> term
441     val dest_orEnumOp_term : term -> term
442    
443     val xorEnumOp_term : term
444     val is_xorEnumOp_term : term -> bool
445     val mk_xorEnumOp_term : term -> term
446     val dest_xorEnumOp_term : term -> term
447    
448     (* Naml ints. *)
449    
450     val plusIntOp_term : term
451     val is_plusIntOp_term : term -> bool
452    
453     val minusIntOp_term : term
454     val is_minusIntOp_term : term -> bool
455    
456     val mulIntOp_term : term
457     val is_mulIntOp_term : term -> bool
458    
459     val divIntOp_term : term
460     val is_divIntOp_term : term -> bool
461    
462     val remIntOp_term : term
463     val is_remIntOp_term : term -> bool
464    
465     val lslIntOp_term : term
466     val is_lslIntOp_term : term -> bool
467    
468     val lsrIntOp_term : term
469     val is_lsrIntOp_term : term -> bool
470    
471     val asrIntOp_term : term
472     val is_asrIntOp_term : term -> bool
473    
474     val andIntOp_term : term
475     val is_andIntOp_term : term -> bool
476    
477     val orIntOp_term : term
478     val is_orIntOp_term : term -> bool
479    
480     val xorIntOp_term : term
481     val is_xorIntOp_term : term -> bool
482    
483     val maxIntOp_term : term
484     val is_maxIntOp_term : term -> bool
485    
486     val minIntOp_term : term
487     val is_minIntOp_term : term -> bool
488    
489     val eqIntOp_term : term
490     val is_eqIntOp_term : term -> bool
491    
492     val neqIntOp_term : term
493     val is_neqIntOp_term : term -> bool
494    
495     val ltIntOp_term : term
496     val is_ltIntOp_term : term -> bool
497    
498     val leIntOp_term : term
499     val is_leIntOp_term : term -> bool
500    
501     val gtIntOp_term : term
502     val is_gtIntOp_term : term -> bool
503    
504     val geIntOp_term : term
505     val is_geIntOp_term : term -> bool
506    
507     val cmpIntOp_term : term
508     val is_cmpIntOp_term : term -> bool
509    
510     (* Native ints. *)
511    
512     val plusRawIntOp_term : term
513     val is_plusRawIntOp_term : term -> bool
514     val mk_plusRawIntOp_term : term -> term -> term
515     val dest_plusRawIntOp_term : term -> term * term
516    
517     val minusRawIntOp_term : term
518     val is_minusRawIntOp_term : term -> bool
519     val mk_minusRawIntOp_term : term -> term -> term
520     val dest_minusRawIntOp_term : term -> term * term
521    
522     val mulRawIntOp_term : term
523     val is_mulRawIntOp_term : term -> bool
524     val mk_mulRawIntOp_term : term -> term -> term
525     val dest_mulRawIntOp_term : term -> term * term
526    
527     val divRawIntOp_term : term
528     val is_divRawIntOp_term : term -> bool
529     val mk_divRawIntOp_term : term -> term -> term
530     val dest_divRawIntOp_term : term -> term * term
531    
532     val remRawIntOp_term : term
533     val is_remRawIntOp_term : term -> bool
534     val mk_remRawIntOp_term : term -> term -> term
535     val dest_remRawIntOp_term : term -> term * term
536    
537     val slRawIntOp_term : term
538     val is_slRawIntOp_term : term -> bool
539     val mk_slRawIntOp_term : term -> term -> term
540     val dest_slRawIntOp_term : term -> term * term
541    
542     val srRawIntOp_term : term
543     val is_srRawIntOp_term : term -> bool
544     val mk_srRawIntOp_term : term -> term -> term
545     val dest_srRawIntOp_term : term -> term * term
546    
547     val andRawIntOp_term : term
548     val is_andRawIntOp_term : term -> bool
549     val mk_andRawIntOp_term : term -> term -> term
550     val dest_andRawIntOp_term : term -> term * term
551    
552     val orRawIntOp_term : term
553     val is_orRawIntOp_term : term -> bool
554     val mk_orRawIntOp_term : term -> term -> term
555     val dest_orRawIntOp_term : term -> term * term
556    
557     val xorRawIntOp_term : term
558     val is_xorRawIntOp_term : term -> bool
559     val mk_xorRawIntOp_term : term -> term -> term
560     val dest_xorRawIntOp_term : term -> term * term
561    
562     val maxRawIntOp_term : term
563     val is_maxRawIntOp_term : term -> bool
564     val mk_maxRawIntOp_term : term -> term -> term
565     val dest_maxRawIntOp_term : term -> term * term
566    
567     val minRawIntOp_term : term
568     val is_minRawIntOp_term : term -> bool
569     val mk_minRawIntOp_term : term -> term -> term
570     val dest_minRawIntOp_term : term -> term * term
571    
572     val rawSetBitFieldOp_term : term
573     val is_rawSetBitFieldOp_term : term -> bool
574     val mk_rawSetBitFieldOp_term : term -> term -> term -> term -> term
575     val dest_rawSetBitFieldOp_term : term -> term * term * term * term
576    
577     val eqRawIntOp_term : term
578     val is_eqRawIntOp_term : term -> bool
579     val mk_eqRawIntOp_term : term -> term -> term
580     val dest_eqRawIntOp_term : term -> term * term
581    
582     val eqRawIntOp_term : term
583     val is_eqRawIntOp_term : term -> bool
584     val mk_eqRawIntOp_term : term -> term -> term
585     val dest_eqRawIntOp_term : term -> term * term
586    
587     val neqRawIntOp_term : term
588     val is_neqRawIntOp_term : term -> bool
589     val mk_neqRawIntOp_term : term -> term -> term
590     val dest_neqRawIntOp_term : term -> term * term
591    
592     val ltRawIntOp_term : term
593     val is_ltRawIntOp_term : term -> bool
594     val mk_ltRawIntOp_term : term -> term -> term
595     val dest_ltRawIntOp_term : term -> term * term
596    
597     val leRawIntOp_term : term
598     val is_leRawIntOp_term : term -> bool
599     val mk_leRawIntOp_term : term -> term -> term
600     val dest_leRawIntOp_term : term -> term * term
601    
602     val gtRawIntOp_term : term
603     val is_gtRawIntOp_term : term -> bool
604     val mk_gtRawIntOp_term : term -> term -> term
605     val dest_gtRawIntOp_term : term -> term * term
606    
607     val geRawIntOp_term : term
608     val is_geRawIntOp_term : term -> bool
609     val mk_geRawIntOp_term : term -> term -> term
610     val dest_geRawIntOp_term : term -> term * term
611    
612     val cmpRawIntOp_term : term
613     val is_cmpRawIntOp_term : term -> bool
614     val mk_cmpRawIntOp_term : term -> term -> term
615     val dest_cmpRawIntOp_term : term -> term * term
616    
617     (* Floats. *)
618    
619     val plusFloatOp_term : term
620     val is_plusFloatOp_term : term -> bool
621     val mk_plusFloatOp_term : term -> term
622     val dest_plusFloatOp_term : term -> term
623    
624     val minusFloatOp_term : term
625     val is_minusFloatOp_term : term -> bool
626     val mk_minusFloatOp_term : term -> term
627     val dest_minusFloatOp_term : term -> term
628    
629     val mulFloatOp_term : term
630     val is_mulFloatOp_term : term -> bool
631     val mk_mulFloatOp_term : term -> term
632     val dest_mulFloatOp_term : term -> term
633    
634     val divFloatOp_term : term
635     val is_divFloatOp_term : term -> bool
636     val mk_divFloatOp_term : term -> term
637     val dest_divFloatOp_term : term -> term
638    
639     val remFloatOp_term : term
640     val is_remFloatOp_term : term -> bool
641     val mk_remFloatOp_term : term -> term
642     val dest_remFloatOp_term : term -> term
643    
644     val maxFloatOp_term : term
645     val is_maxFloatOp_term : term -> bool
646     val mk_maxFloatOp_term : term -> term
647     val dest_maxFloatOp_term : term -> term
648    
649     val minFloatOp_term : term
650     val is_minFloatOp_term : term -> bool
651     val mk_minFloatOp_term : term -> term
652     val dest_minFloatOp_term : term -> term
653    
654     val eqFloatOp_term : term
655     val is_eqFloatOp_term : term -> bool
656     val mk_eqFloatOp_term : term -> term
657     val dest_eqFloatOp_term : term -> term
658    
659     val neqFloatOp_term : term
660     val is_neqFloatOp_term : term -> bool
661     val mk_neqFloatOp_term : term -> term
662     val dest_neqFloatOp_term : term -> term
663    
664     val ltFloatOp_term : term
665     val is_ltFloatOp_term : term -> bool
666     val mk_ltFloatOp_term : term -> term
667     val dest_ltFloatOp_term : term -> term
668    
669     val leFloatOp_term : term
670     val is_leFloatOp_term : term -> bool
671     val mk_leFloatOp_term : term -> term
672     val dest_leFloatOp_term : term -> term
673    
674     val gtFloatOp_term : term
675     val is_gtFloatOp_term : term -> bool
676     val mk_gtFloatOp_term : term -> term
677     val dest_gtFloatOp_term : term -> term
678    
679     val geFloatOp_term : term
680     val is_geFloatOp_term : term -> bool
681     val mk_geFloatOp_term : term -> term
682     val dest_geFloatOp_term : term -> term
683    
684     val cmpFloatOp_term : term
685     val is_cmpFloatOp_term : term -> bool
686     val mk_cmpFloatOp_term : term -> term
687     val dest_cmpFloatOp_term : term -> term
688    
689     val atan2Op_term : term
690     val is_atan2Op_term : term -> bool
691     val mk_atan2Op_term : term -> term
692     val dest_atan2Op_term : term -> term
693    
694     (* Pointer equality. *)
695    
696     val eqEqOp_term : term
697     val is_eqEqOp_term : term -> bool
698    
699     val neqEqOp_term : term
700     val is_neqEqOp_term : term -> bool
701    
702     (* Pointer arithmetic. *)
703    
704     val plusPointerOp_term : term
705     val is_plusPointerOp_term : term -> bool
706 emre 3580 val mk_plusPointerOp_term : term -> term -> term -> term
707     val dest_plusPointerOp_term : term -> term * term * term
708 emre 3550
709     (*
710 emre 3563 * Fields (frame labels).
711     *)
712    
713     val frameLabel_term : term
714     val is_frameLabel_term : term -> bool
715     val mk_frameLabel_term : term -> term -> term -> term
716     val dest_frameLabel_term : term -> term * term * term
717    
718     (*
719 emre 3550 * Normal values.
720     *)
721    
722     val atomNil_term : term
723     val is_atomNil_term : term -> bool
724     val mk_atomNil_term : term -> term
725     val dest_atomNil_term : term -> term
726    
727     val atomInt_term : term
728     val is_atomInt_term : term -> bool
729     val mk_atomInt_term : term -> term
730     val dest_atomInt_term : term -> term
731    
732     val atomEnum_term : term
733     val is_atomEnum_term : term -> bool
734     val mk_atomEnum_term : term -> term -> term
735     val dest_atomEnum_term : term -> term * term
736    
737     val atomRawInt_term : term
738     val is_atomRawInt_term : term -> bool
739     val mk_atomRawInt_term : term -> term -> term -> term
740     val dest_atomRawInt_term : term -> term * term * term
741    
742     val atomFloat_term : term
743     val is_atomFloat_term : term -> bool
744     val mk_atomFloat_term : term -> term -> term
745     val dest_atomFloat_term : term -> term * term
746    
747 emre 3563 val atomLabel_term : term
748     val is_atomLabel_term : term -> bool
749 emre 3580 val mk_atomLabel_term : term -> term -> term
750     val dest_atomLabel_term : term -> term * term
751 emre 3563
752 emre 3580 val atomSizeof_term : term
753     val is_atomSizeof_term : term -> bool
754     val mk_atomSizeof_term : term -> term -> term
755     val dest_atomSizeof_term : term -> term * term
756    
757 emre 3550 val atomConst_term : term
758     val is_atomConst_term : term -> bool
759     val mk_atomConst_term : term -> term -> term -> term
760     val dest_atomConst_term : term -> term * term * term
761    
762     val atomVar_term : term
763     val is_atomVar_term : term -> bool
764     val mk_atomVar_term : term -> term
765     val dest_atomVar_term : term -> term
766    
767     (*
768     * Allocation operators.
769     *)
770    
771     val allocTuple_term : term
772     val is_allocTuple_term : term -> bool
773     val mk_allocTuple_term : term -> term -> term -> term
774     val dest_allocTuple_term : term -> term * term * term
775    
776     val allocUnion_term : term
777     val is_allocUnion_term : term -> bool
778     val mk_allocUnion_term : term -> term -> term -> term -> term
779     val dest_allocUnion_term : term -> term * term * term * term
780    
781     val allocArray_term : term
782     val is_allocArray_term : term -> bool
783     val mk_allocArray_term : term -> term -> term
784     val dest_allocArray_term : term -> term * term
785    
786     val allocVArray_term : term
787     val is_allocVArray_term : term -> bool
788     val mk_allocVArray_term : term -> term -> term -> term -> term
789     val dest_allocVArray_term : term -> term * term * term * term
790    
791     val allocMalloc_term : term
792     val is_allocMalloc_term : term -> bool
793     val mk_allocMalloc_term : term -> term -> term
794     val dest_allocMalloc_term : term -> term * term
795    
796 emre 3563 val allocFrame_term : term
797     val is_allocFrame_term : term -> bool
798     val mk_allocFrame_term : term -> term
799     val dest_allocFrame_term : term -> term
800    
801 emre 3550 (*
802     * Tail calls / operations.
803     *)
804    
805     val tailSysMigrate_term : term
806     val is_tailSysMigrate_term : term -> bool
807     val mk_tailSysMigrate_term : term -> term -> term -> term -> term -> term
808     val dest_tailSysMigrate_term : term -> term * term * term * term * term
809    
810     val tailAtomic_term : term
811     val is_tailAtomic_term : term -> bool
812     val mk_tailAtomic_term : term -> term -> term -> term
813     val dest_tailAtomic_term : term -> term * term * term
814    
815     val tailAtomicRollback_term : term
816     val is_tailAtomicRollback_term : term -> bool
817     val mk_tailAtomicRollback_term : term -> term
818     val dest_tailAtomicRollback_term : term -> term
819    
820     val tailAtomicCommit_term : term
821     val is_tailAtomicCommit_term : term -> bool
822     val mk_tailAtomicCommit_term : term -> term -> term
823     val dest_tailAtomicCommit_term : term -> term * term
824    
825     (*
826     * Predicates and assertions.
827     *)
828    
829     val isMutable_term : term
830     val is_isMutable_term : term -> bool
831 emre 3580 val mk_isMutable_term : term -> term
832     val dest_isMutable_term : term -> term
833 emre 3550
834     val reserve_term : term
835     val is_reserve_term : term -> bool
836 emre 3580 val mk_reserve_term : term -> term -> term
837     val dest_reserve_term : term -> term * term
838 emre 3550
839     val boundsCheck_term : term
840     val is_boundsCheck_term : term -> bool
841 emre 3580 val mk_boundsCheck_term : term -> term -> term -> term -> term
842     val dest_boundsCheck_term : term -> term * term * term * term
843 emre 3550
844 emre 3580 val elementCheck_term : term
845     val is_elementCheck_term : term -> bool
846     val mk_elementCheck_term : term -> term -> term -> term -> term
847     val dest_elementCheck_term : term -> term * term * term * term
848 emre 3550
849     (*
850     * Debugging info.
851     *)
852    
853     val debugLine_term : term
854     val is_debugLine_term : term -> bool
855     val mk_debugLine_term : term -> term -> term
856     val dest_debugLine_term : term -> term * term
857    
858     val debugVarItem_term : term
859     val is_debugVarItem_term : term -> bool
860     val mk_debugVarItem_term : term -> term -> term -> term
861     val dest_debugVarItem_term : term -> term * term * term
862    
863     val debugVars_term : term
864     val is_debugVars_term : term -> bool
865     val mk_debugVars_term : term -> term
866     val dest_debugVars_term : term -> term
867    
868     val debugString_term : term
869     val is_debugString_term : term -> bool
870     val mk_debugString_term : term -> term
871     val dest_debugString_term : term -> term
872    
873     val debugContext_term : term
874     val is_debugContext_term : term -> bool
875     val mk_debugContext_term : term -> term -> term
876     val dest_debugContext_term : term -> term * term
877    
878     (*
879     * Expressions.
880     *)
881    
882     (* Primitive operations. *)
883    
884     val letUnop_term : term
885     val is_letUnop_term : term -> bool
886     val mk_letUnop_term : term -> term -> term -> string -> term -> term
887     val dest_letUnop_term : term -> term * term * term * string * term
888    
889     val letBinop_term : term
890     val is_letBinop_term : term -> bool
891     val mk_letBinop_term : term -> term -> term -> term -> string -> term -> term
892     val dest_letBinop_term : term -> term * term * term * term * string * term
893    
894     (* Function application. *)
895    
896     val letExt_term : term
897     val is_letExt_term : term -> bool
898     val mk_letExt_term : term -> term -> term -> term -> string -> term -> term
899     val dest_letExt_term : term -> term * term * term * term * string * term
900    
901     val tailCall_term : term
902     val is_tailCall_term : term -> bool
903 emre 3563 val mk_tailCall_term : term -> term -> term -> term
904     val dest_tailCall_term : term -> term * term * term
905 emre 3550
906     val specialCall_term : term
907     val is_specialCall_term : term -> bool
908 emre 3563 val mk_specialCall_term : term -> term -> term
909     val dest_specialCall_term : term -> term * term
910 emre 3550
911     (* Control. *)
912    
913     val matchCase_term : term
914     val is_matchCase_term : term -> bool
915 emre 3563 val mk_matchCase_term : term -> term -> term -> term
916     val dest_matchCase_term : term -> term * term * term
917 emre 3550
918     val matchExp_term : term
919     val is_matchExp_term : term -> bool
920     val mk_matchExp_term : term -> term -> term
921     val dest_matchExp_term : term -> term * term
922    
923     val typeCase_term : term
924     val is_typeCase_term : term -> bool
925     val mk_typeCase_term :
926     term -> term -> term -> term -> term -> term -> term
927     val dest_typeCase_term :
928     term-> term * term * term * term * term * term
929    
930     (* Allocation. *)
931    
932     val letAlloc_term : term
933     val is_letAlloc_term : term -> bool
934     val mk_letAlloc_term : string -> term -> term -> term
935     val dest_letAlloc_term : term -> string * term * term
936    
937     (* Subscripting *)
938    
939     val letSubscript_term : term
940     val is_letSubscript_term : term -> bool
941     val mk_letSubscript_term :
942     term -> term -> term -> term -> string -> term -> term
943     val dest_letSubscript_term :
944     term -> term * term * term * term * string * term
945    
946     val setSubscript_term : term
947     val is_setSubscript_term : term -> bool
948     val mk_setSubscript_term :
949     term -> term -> term -> term -> term -> term -> term -> term
950     val dest_setSubscript_term :
951     term -> term * term * term * term * term * term * term
952    
953     val setGlobal_term : term
954     val is_setGlobal_term : term -> bool
955     val mk_setGlobal_term :
956     term -> term -> term -> term -> term -> term -> term
957     val dest_setGlobal_term :
958     term -> term * term * term * term * term * term
959    
960     val memcpy_term : term
961     val is_memcpy_term : term -> bool
962     val mk_memcpy_term :
963     term -> term -> term -> term -> term -> term -> term -> term -> term
964     val dest_memcpy_term :
965     term -> term * term * term * term * term * term * term * term
966    
967     (* Assertions. *)
968    
969     val call_term : term
970     val is_call_term : term -> bool
971 emre 3563 val mk_call_term : term -> term -> term -> term -> term
972     val dest_call_term : term -> term * term * term * term
973 emre 3550
974     val assertExp_term : term
975     val is_assertExp_term : term -> bool
976     val mk_assertExp_term : term -> term -> term -> term
977     val dest_assertExp_term : term -> term * term * term
978    
979     (* Debugging. *)
980    
981     val debug_term : term
982     val is_debug_term : term -> bool
983     val mk_debug_term : term -> term -> term
984     val dest_debug_term : term -> term * term
985 emre 3562
986     (*
987     * Function definition.
988     *)
989    
990     val fundef_term : term
991     val is_fundef_term : term -> bool
992     val mk_fundef_term : term -> term -> term -> term -> term
993     val dest_fundef_term : term -> term * term * term * term

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26