/[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 3564 - (hide annotations) (download)
Fri Apr 5 07:07:58 2002 UTC (19 years, 4 months ago) by emre
File size: 30219 byte(s)
-  Fixed some problems in Mp_mc_fir_eval and proved
   the rewrites in it.
-  Proved 2 of the deadcode elimination rewrites (in Mp_mc_deadcode).

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 3563 (* Pointer operations. *)
100    
101     declare rawIntOfLabelOp{ 'int_precision; 'int_signed }
102    
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     declare plusPointerOp{ 'int_precision; 'int_signed }
190    
191     (*
192     * Subscript operators.
193     *)
194    
195     (* Blocks. *)
196    
197     declare blockSub
198     declare rawDataSub
199     declare tupleSub
200     declare rawTupleSub
201    
202     (* Values. *)
203    
204     declare polySub
205     declare rawIntSub{ 'int_precision; 'int_signed }
206     declare rawFloatSub{ 'float_precision }
207     declare pointerSub
208     declare functionSub
209    
210     (* Indexing. *)
211    
212     declare byteIndex
213     declare wordIndex
214    
215     (* Subscripting. *)
216    
217     declare intIndex
218     declare rawIntIndex{ 'int_precision; 'int_signed }
219    
220     (* Subscripting op. *)
221    
222     declare subop{ 'sub_block; 'sub_value; 'sub_index; 'sub_script }
223    
224     (*
225 emre 3563 * Fields (frame labels).
226     *)
227    
228     declare frameLabel{ 'label1; 'label2; 'label3 }
229    
230     (*
231 emre 3550 * Normal values.
232     *)
233    
234     declare atomNil{ 'ty }
235     declare atomInt{ 'int }
236 emre 3564 declare atomEnum{ 'int1; 'int2 } (* 'int1 = bound, 'int2 = value *)
237 emre 3550 declare atomRawInt{ 'int_precision; 'int_signed; 'num }
238     declare atomFloat{ 'float_precision; 'num }
239 emre 3563 declare atomLabel{ 'frame_label }
240 emre 3550 declare atomConst{ 'ty; 'ty_var; 'int }
241     declare atomVar{ 'var }
242    
243     (*
244     * Allocation operators.
245     *)
246    
247     declare allocTuple{ 'tuple_class; 'ty; 'atom_list }
248     declare allocUnion{ 'ty; 'ty_var; 'int; 'atom_list }
249     declare allocArray{ 'ty; 'atom_list }
250     declare allocVArray{ 'ty; 'sub_index; 'atom1; 'atom2 }
251     declare allocMalloc{ 'ty; 'atom }
252 emre 3563 declare allocFrame{ 'var }
253 emre 3550
254     (*
255     * Tail calls / operations.
256     *)
257    
258     declare tailSysMigrate{ 'int; 'atom1; 'atom2; 'var; 'atom_list }
259     declare tailAtomic{ 'var; 'atom; 'atom_list }
260     declare tailAtomicRollback{ 'atom }
261     declare tailAtomicCommit{ 'var; 'atom_list }
262    
263     (*
264     * Predicates and assertions.
265     *)
266    
267     (* No-ops. *)
268    
269     declare isMutable
270    
271     (* Unary operations. *)
272    
273     declare reserve
274     declare boundsCheckLower
275     declare boundsCheckUpper
276     declare polyCheck
277     declare pointerCheck
278     declare functionCheck
279    
280     (* Binary operations. *)
281    
282     declare boundsCheck
283    
284     (* Predicates. *)
285    
286     declare predNop{ 'var; 'pred_nop }
287     declare predUnop{ 'var; 'pred_unop; 'atom }
288     declare predBinop{ 'var; 'pred_binop; 'atom1; 'atom2 }
289    
290     (*
291     * Debugging info.
292     *)
293    
294     declare debugLine{ 'string; 'int }
295     declare debugVarItem{ 'var1; 'ty; 'var2 }
296     declare debugVars{ 'debugVarItem_list }
297     declare debugString{ 'string }
298     declare debugContext{ 'debug_line; 'debug_vars }
299    
300     (*
301     * Expressions.
302     *)
303    
304     (* Primitive operations. *)
305    
306     declare letUnop{ 'ty; 'unop; 'atom; var. 'exp['var] }
307     declare letBinop{ 'ty; 'binop; 'atom1; 'atom2; var. 'exp['var] }
308    
309     (* Function application. *)
310    
311     declare letExt{ 'ty1; 'string; 'ty2; 'atom_list; var. 'exp['var] }
312 emre 3563 declare tailCall{ 'label; 'var; 'atom_list }
313     declare specialCall{ 'label; 'tailop }
314 emre 3550
315     (* Control. *)
316    
317 emre 3563 declare matchCase{ 'label; 'set; 'exp }
318 emre 3550 declare matchExp{ 'atom; 'matchCase_list }
319     declare typeCase{ 'atom1; 'atom2; 'var1; 'var2; 'exp1; 'exp2 }
320    
321     (* Allocation. *)
322    
323     declare letAlloc{ 'alloc_op; var. 'exp['var] }
324    
325     (* Subscripting. *)
326    
327     declare letSubscript{ 'subop; 'ty; 'var2; 'atom; var1. 'exp['var1] }
328     declare setSubscript{ 'subop; 'label; 'var; 'atom1; 'ty; 'atom2; 'exp }
329     declare setGlobal{ 'sub_value; 'label; 'var; 'ty; 'atom; 'exp }
330     declare memcpy{ 'subop; 'label; 'var1; 'atom1; 'var2; 'atom2; 'atom3; 'exp }
331    
332     (* Assertions. *)
333    
334 emre 3563 declare call{ 'label; 'var; 'atom_option_list; 'exp }
335 emre 3550 declare assertExp{ 'label; 'pred; 'exp }
336    
337     (* Debugging. *)
338    
339     declare debug{ 'debug_info; 'exp }
340    
341 emre 3562 (*
342     * Function definition.
343     *)
344    
345     declare fundef{ 'debug_line; 'ty; 'var_list; 'exp }
346    
347 emre 3550 (*************************************************************************
348     * Term operations.
349     *************************************************************************)
350    
351     (*
352     * Unary operations.
353     *)
354    
355     (* Identity (polymorphic). *)
356    
357     val idOp_term : term
358     val is_idOp_term : term -> bool
359    
360     (* Naml ints. *)
361    
362     val uminusIntOp_term : term
363     val is_uminusIntOp_term : term -> bool
364    
365     val notIntOp_term : term
366     val is_notIntOp_term : term -> bool
367    
368     (* Bit fields. *)
369    
370     val rawBitFieldOp_term : term
371     val is_rawBitFieldOp_term : term -> bool
372     val mk_rawBitFieldOp_term : term -> term -> term -> term -> term
373     val dest_rawBitFieldOp_term : term -> term * term * term * term
374    
375     (* Native ints. *)
376    
377     val uminusRawIntOp_term : term
378     val is_uminusRawIntOp_term : term -> bool
379     val mk_uminusRawIntOp_term : term -> term -> term
380     val dest_uminusRawIntOp_term : term -> term * term
381    
382     val notRawIntOp_term : term
383     val is_notRawIntOp_term : term -> bool
384     val mk_notRawIntOp_term : term -> term -> term
385     val dest_notRawIntOp_term : term -> term * term
386    
387     (* Floats. *)
388    
389     val uminusFloatOp_term : term
390     val is_uminusFloatOp_term : term -> bool
391     val mk_uminusFloatOp_term : term -> term
392     val dest_uminusFloatOp_term : term -> term
393    
394     val absFloatOp_term : term
395     val is_absFloatOp_term : term -> bool
396     val mk_absFloatOp_term : term -> term
397     val dest_absFloatOp_term : term -> term
398    
399     val sinOp_term : term
400     val is_sinOp_term : term -> bool
401     val mk_sinOp_term : term -> term
402     val dest_sinOp_term : term -> term
403    
404     val cosOp_term : term
405     val is_cosOp_term : term -> bool
406     val mk_cosOp_term : term -> term
407     val dest_cosOp_term : term -> term
408    
409     val sqrtOp_term : term
410     val is_sqrtOp_term : term -> bool
411     val mk_sqrtOp_term : term -> term
412     val dest_sqrtOp_term : term -> term
413    
414     (* Coerce to int. *)
415    
416     val intOfFloatOp_term : term
417     val is_intOfFloatOp_term : term -> bool
418     val mk_intOfFloatOp_term : term -> term
419     val dest_intOfFloatOp_term : term -> term
420    
421     (* Coerce to float. *)
422    
423     val floatOfIntOp_term : term
424     val is_floatOfIntOp_term : term -> bool
425     val mk_floatOfIntOp_term : term -> term
426     val dest_floatOfIntOp_term : term -> term
427    
428     val floatOfFloatOp_term : term
429     val is_floatOfFloatOp_term : term -> bool
430     val mk_floatOfFloatOp_term : term -> term -> term
431     val dest_floatOfFloatOp_term : term -> term * term
432    
433     val floatOfRawIntOp_term : term
434     val is_floatOfRawIntOp_term : term -> bool
435     val mk_floatOfRawIntOp_term : term -> term -> term -> term
436     val dest_floatOfRawIntOp_term : term -> term * term * term
437    
438     (* Coerce to rawint. *)
439    
440     val rawIntOfIntOp_term : term
441     val is_rawIntOfIntOp_term : term -> bool
442     val mk_rawIntOfIntOp_term : term -> term -> term
443     val dest_rawIntOfIntOp_term : term -> term * term
444    
445     val rawIntOfEnumOp_term : term
446     val is_rawIntOfEnumOp_term : term -> bool
447     val mk_rawIntOfEnumOp_term : term -> term -> term -> term
448     val dest_rawIntOfEnumOp_term : term -> term * term * term
449    
450     val rawIntOfFloatOp_term : term
451     val is_rawIntOfFloatOp_term : term -> bool
452     val mk_rawIntOfFloatOp_term : term -> term -> term -> term
453     val dest_rawIntOfFloatOp_term : term -> term * term * term
454    
455     val rawIntOfRawIntOp_term : term
456     val is_rawIntOfRawIntOp_term : term -> bool
457     val mk_rawIntOfRawIntOp_term : term -> term -> term -> term -> term
458     val dest_rawIntOfRawIntOp_term : term -> term * term * term * term
459    
460     (* Integer/pointer coercions. *)
461    
462     val rawIntOfPointerOp_term : term
463     val is_rawIntOfPointerOp_term : term -> bool
464     val mk_rawIntOfPointerOp_term : term -> term -> term
465     val dest_rawIntOfPointerOp_term : term -> term * term
466    
467     val pointerOfRawIntOp_term : term
468     val is_pointerOfRawIntOp_term : term -> bool
469     val mk_pointerOfRawIntOp_term : term -> term -> term
470     val dest_pointerOfRawIntOp_term : term -> term * term
471    
472 emre 3563 val rawIntOfLabelOp_term : term
473     val is_rawIntOfLabelOp_term : term -> bool
474     val mk_rawIntOfLabelOp_term : term -> term -> term
475     val dest_rawIntOfLabelOp_term : term -> term * term
476    
477 emre 3550 (*
478     * Binary operations.
479     *)
480    
481     (* Enums. *)
482    
483     val andEnumOp_term : term
484     val is_andEnumOp_term : term -> bool
485     val mk_andEnumOp_term : term -> term
486     val dest_andEnumOp_term : term -> term
487    
488     val orEnumOp_term : term
489     val is_orEnumOp_term : term -> bool
490     val mk_orEnumOp_term : term -> term
491     val dest_orEnumOp_term : term -> term
492    
493     val xorEnumOp_term : term
494     val is_xorEnumOp_term : term -> bool
495     val mk_xorEnumOp_term : term -> term
496     val dest_xorEnumOp_term : term -> term
497    
498     (* Naml ints. *)
499    
500     val plusIntOp_term : term
501     val is_plusIntOp_term : term -> bool
502    
503     val minusIntOp_term : term
504     val is_minusIntOp_term : term -> bool
505    
506     val mulIntOp_term : term
507     val is_mulIntOp_term : term -> bool
508    
509     val divIntOp_term : term
510     val is_divIntOp_term : term -> bool
511    
512     val remIntOp_term : term
513     val is_remIntOp_term : term -> bool
514    
515     val lslIntOp_term : term
516     val is_lslIntOp_term : term -> bool
517    
518     val lsrIntOp_term : term
519     val is_lsrIntOp_term : term -> bool
520    
521     val asrIntOp_term : term
522     val is_asrIntOp_term : term -> bool
523    
524     val andIntOp_term : term
525     val is_andIntOp_term : term -> bool
526    
527     val orIntOp_term : term
528     val is_orIntOp_term : term -> bool
529    
530     val xorIntOp_term : term
531     val is_xorIntOp_term : term -> bool
532    
533     val maxIntOp_term : term
534     val is_maxIntOp_term : term -> bool
535    
536     val minIntOp_term : term
537     val is_minIntOp_term : term -> bool
538    
539     val eqIntOp_term : term
540     val is_eqIntOp_term : term -> bool
541    
542     val neqIntOp_term : term
543     val is_neqIntOp_term : term -> bool
544    
545     val ltIntOp_term : term
546     val is_ltIntOp_term : term -> bool
547    
548     val leIntOp_term : term
549     val is_leIntOp_term : term -> bool
550    
551     val gtIntOp_term : term
552     val is_gtIntOp_term : term -> bool
553    
554     val geIntOp_term : term
555     val is_geIntOp_term : term -> bool
556    
557     val cmpIntOp_term : term
558     val is_cmpIntOp_term : term -> bool
559    
560     (* Native ints. *)
561    
562     val plusRawIntOp_term : term
563     val is_plusRawIntOp_term : term -> bool
564     val mk_plusRawIntOp_term : term -> term -> term
565     val dest_plusRawIntOp_term : term -> term * term
566    
567     val minusRawIntOp_term : term
568     val is_minusRawIntOp_term : term -> bool
569     val mk_minusRawIntOp_term : term -> term -> term
570     val dest_minusRawIntOp_term : term -> term * term
571    
572     val mulRawIntOp_term : term
573     val is_mulRawIntOp_term : term -> bool
574     val mk_mulRawIntOp_term : term -> term -> term
575     val dest_mulRawIntOp_term : term -> term * term
576    
577     val divRawIntOp_term : term
578     val is_divRawIntOp_term : term -> bool
579     val mk_divRawIntOp_term : term -> term -> term
580     val dest_divRawIntOp_term : term -> term * term
581    
582     val remRawIntOp_term : term
583     val is_remRawIntOp_term : term -> bool
584     val mk_remRawIntOp_term : term -> term -> term
585     val dest_remRawIntOp_term : term -> term * term
586    
587     val slRawIntOp_term : term
588     val is_slRawIntOp_term : term -> bool
589     val mk_slRawIntOp_term : term -> term -> term
590     val dest_slRawIntOp_term : term -> term * term
591    
592     val srRawIntOp_term : term
593     val is_srRawIntOp_term : term -> bool
594     val mk_srRawIntOp_term : term -> term -> term
595     val dest_srRawIntOp_term : term -> term * term
596    
597     val andRawIntOp_term : term
598     val is_andRawIntOp_term : term -> bool
599     val mk_andRawIntOp_term : term -> term -> term
600     val dest_andRawIntOp_term : term -> term * term
601    
602     val orRawIntOp_term : term
603     val is_orRawIntOp_term : term -> bool
604     val mk_orRawIntOp_term : term -> term -> term
605     val dest_orRawIntOp_term : term -> term * term
606    
607     val xorRawIntOp_term : term
608     val is_xorRawIntOp_term : term -> bool
609     val mk_xorRawIntOp_term : term -> term -> term
610     val dest_xorRawIntOp_term : term -> term * term
611    
612     val maxRawIntOp_term : term
613     val is_maxRawIntOp_term : term -> bool
614     val mk_maxRawIntOp_term : term -> term -> term
615     val dest_maxRawIntOp_term : term -> term * term
616    
617     val minRawIntOp_term : term
618     val is_minRawIntOp_term : term -> bool
619     val mk_minRawIntOp_term : term -> term -> term
620     val dest_minRawIntOp_term : term -> term * term
621    
622     val rawSetBitFieldOp_term : term
623     val is_rawSetBitFieldOp_term : term -> bool
624     val mk_rawSetBitFieldOp_term : term -> term -> term -> term -> term
625     val dest_rawSetBitFieldOp_term : term -> term * term * term * term
626    
627     val eqRawIntOp_term : term
628     val is_eqRawIntOp_term : term -> bool
629     val mk_eqRawIntOp_term : term -> term -> term
630     val dest_eqRawIntOp_term : term -> term * term
631    
632     val eqRawIntOp_term : term
633     val is_eqRawIntOp_term : term -> bool
634     val mk_eqRawIntOp_term : term -> term -> term
635     val dest_eqRawIntOp_term : term -> term * term
636    
637     val neqRawIntOp_term : term
638     val is_neqRawIntOp_term : term -> bool
639     val mk_neqRawIntOp_term : term -> term -> term
640     val dest_neqRawIntOp_term : term -> term * term
641    
642     val ltRawIntOp_term : term
643     val is_ltRawIntOp_term : term -> bool
644     val mk_ltRawIntOp_term : term -> term -> term
645     val dest_ltRawIntOp_term : term -> term * term
646    
647     val leRawIntOp_term : term
648     val is_leRawIntOp_term : term -> bool
649     val mk_leRawIntOp_term : term -> term -> term
650     val dest_leRawIntOp_term : term -> term * term
651    
652     val gtRawIntOp_term : term
653     val is_gtRawIntOp_term : term -> bool
654     val mk_gtRawIntOp_term : term -> term -> term
655     val dest_gtRawIntOp_term : term -> term * term
656    
657     val geRawIntOp_term : term
658     val is_geRawIntOp_term : term -> bool
659     val mk_geRawIntOp_term : term -> term -> term
660     val dest_geRawIntOp_term : term -> term * term
661    
662     val cmpRawIntOp_term : term
663     val is_cmpRawIntOp_term : term -> bool
664     val mk_cmpRawIntOp_term : term -> term -> term
665     val dest_cmpRawIntOp_term : term -> term * term
666    
667     (* Floats. *)
668    
669     val plusFloatOp_term : term
670     val is_plusFloatOp_term : term -> bool
671     val mk_plusFloatOp_term : term -> term
672     val dest_plusFloatOp_term : term -> term
673    
674     val minusFloatOp_term : term
675     val is_minusFloatOp_term : term -> bool
676     val mk_minusFloatOp_term : term -> term
677     val dest_minusFloatOp_term : term -> term
678    
679     val mulFloatOp_term : term
680     val is_mulFloatOp_term : term -> bool
681     val mk_mulFloatOp_term : term -> term
682     val dest_mulFloatOp_term : term -> term
683    
684     val divFloatOp_term : term
685     val is_divFloatOp_term : term -> bool
686     val mk_divFloatOp_term : term -> term
687     val dest_divFloatOp_term : term -> term
688    
689     val remFloatOp_term : term
690     val is_remFloatOp_term : term -> bool
691     val mk_remFloatOp_term : term -> term
692     val dest_remFloatOp_term : term -> term
693    
694     val maxFloatOp_term : term
695     val is_maxFloatOp_term : term -> bool
696     val mk_maxFloatOp_term : term -> term
697     val dest_maxFloatOp_term : term -> term
698    
699     val minFloatOp_term : term
700     val is_minFloatOp_term : term -> bool
701     val mk_minFloatOp_term : term -> term
702     val dest_minFloatOp_term : term -> term
703    
704     val eqFloatOp_term : term
705     val is_eqFloatOp_term : term -> bool
706     val mk_eqFloatOp_term : term -> term
707     val dest_eqFloatOp_term : term -> term
708    
709     val neqFloatOp_term : term
710     val is_neqFloatOp_term : term -> bool
711     val mk_neqFloatOp_term : term -> term
712     val dest_neqFloatOp_term : term -> term
713    
714     val ltFloatOp_term : term
715     val is_ltFloatOp_term : term -> bool
716     val mk_ltFloatOp_term : term -> term
717     val dest_ltFloatOp_term : term -> term
718    
719     val leFloatOp_term : term
720     val is_leFloatOp_term : term -> bool
721     val mk_leFloatOp_term : term -> term
722     val dest_leFloatOp_term : term -> term
723    
724     val gtFloatOp_term : term
725     val is_gtFloatOp_term : term -> bool
726     val mk_gtFloatOp_term : term -> term
727     val dest_gtFloatOp_term : term -> term
728    
729     val geFloatOp_term : term
730     val is_geFloatOp_term : term -> bool
731     val mk_geFloatOp_term : term -> term
732     val dest_geFloatOp_term : term -> term
733    
734     val cmpFloatOp_term : term
735     val is_cmpFloatOp_term : term -> bool
736     val mk_cmpFloatOp_term : term -> term
737     val dest_cmpFloatOp_term : term -> term
738    
739     val atan2Op_term : term
740     val is_atan2Op_term : term -> bool
741     val mk_atan2Op_term : term -> term
742     val dest_atan2Op_term : term -> term
743    
744     (* Pointer equality. *)
745    
746     val eqEqOp_term : term
747     val is_eqEqOp_term : term -> bool
748    
749     val neqEqOp_term : term
750     val is_neqEqOp_term : term -> bool
751    
752     (* Pointer arithmetic. *)
753    
754     val plusPointerOp_term : term
755     val is_plusPointerOp_term : term -> bool
756     val mk_plusPointerOp_term : term -> term -> term
757     val dest_plusPointerOp_term : term -> term * term
758    
759     (*
760     * Subscript operators.
761     *)
762    
763     (* Blocks. *)
764    
765     val blockSub_term : term
766     val is_blockSub_term : term -> bool
767    
768     val rawDataSub_term : term
769     val is_rawDataSub_term : term -> bool
770    
771     val tupleSub_term : term
772     val is_tupleSub_term : term -> bool
773    
774     val rawTupleSub_term : term
775     val is_rawTupleSub_term : term -> bool
776    
777     (* Values. *)
778    
779     val polySub_term : term
780     val is_polySub_term : term -> bool
781    
782     val rawIntSub_term : term
783     val is_rawIntSub_term : term -> bool
784     val mk_rawIntSub_term : term -> term -> term
785     val dest_rawIntSub_term : term -> term * term
786    
787     val rawFloatSub_term : term
788     val is_rawFloatSub_term : term -> bool
789     val mk_rawFloatSub_term : term -> term
790     val dest_rawFloatSub_term : term -> term
791    
792     val pointerSub_term : term
793     val is_pointerSub_term : term -> bool
794    
795     val functionSub_term : term
796     val is_functionSub_term : term -> bool
797    
798     (* Indexing. *)
799    
800     val byteIndex_term : term
801     val is_byteIndex_term : term -> bool
802    
803     val wordIndex_term : term
804     val is_wordIndex_term : term -> bool
805    
806     (* Subscripting. *)
807    
808     val intIndex_term : term
809     val is_intIndex_term : term -> bool
810    
811     val rawIntIndex_term : term
812     val is_rawIntIndex_term : term -> bool
813     val mk_rawIntIndex_term : term -> term -> term
814     val dest_rawIntIndex_term : term -> term * term
815    
816     (* Susbscripting op. *)
817    
818     val subop_term : term
819     val is_subop_term : term -> bool
820     val mk_subop_term : term -> term -> term -> term -> term
821     val dest_subop_term : term -> term * term * term * term
822    
823     (*
824 emre 3563 * Fields (frame labels).
825     *)
826    
827     val frameLabel_term : term
828     val is_frameLabel_term : term -> bool
829     val mk_frameLabel_term : term -> term -> term -> term
830     val dest_frameLabel_term : term -> term * term * term
831    
832     (*
833 emre 3550 * Normal values.
834     *)
835    
836     val atomNil_term : term
837     val is_atomNil_term : term -> bool
838     val mk_atomNil_term : term -> term
839     val dest_atomNil_term : term -> term
840    
841     val atomInt_term : term
842     val is_atomInt_term : term -> bool
843     val mk_atomInt_term : term -> term
844     val dest_atomInt_term : term -> term
845    
846     val atomEnum_term : term
847     val is_atomEnum_term : term -> bool
848     val mk_atomEnum_term : term -> term -> term
849     val dest_atomEnum_term : term -> term * term
850    
851     val atomRawInt_term : term
852     val is_atomRawInt_term : term -> bool
853     val mk_atomRawInt_term : term -> term -> term -> term
854     val dest_atomRawInt_term : term -> term * term * term
855    
856     val atomFloat_term : term
857     val is_atomFloat_term : term -> bool
858     val mk_atomFloat_term : term -> term -> term
859     val dest_atomFloat_term : term -> term * term
860    
861 emre 3563 val atomLabel_term : term
862     val is_atomLabel_term : term -> bool
863     val mk_atomLabel_term : term -> term
864     val dest_atomLabel_term : term -> term
865    
866 emre 3550 val atomConst_term : term
867     val is_atomConst_term : term -> bool
868     val mk_atomConst_term : term -> term -> term -> term
869     val dest_atomConst_term : term -> term * term * term
870    
871     val atomVar_term : term
872     val is_atomVar_term : term -> bool
873     val mk_atomVar_term : term -> term
874     val dest_atomVar_term : term -> term
875    
876     (*
877     * Allocation operators.
878     *)
879    
880     val allocTuple_term : term
881     val is_allocTuple_term : term -> bool
882     val mk_allocTuple_term : term -> term -> term -> term
883     val dest_allocTuple_term : term -> term * term * term
884    
885     val allocUnion_term : term
886     val is_allocUnion_term : term -> bool
887     val mk_allocUnion_term : term -> term -> term -> term -> term
888     val dest_allocUnion_term : term -> term * term * term * term
889    
890     val allocArray_term : term
891     val is_allocArray_term : term -> bool
892     val mk_allocArray_term : term -> term -> term
893     val dest_allocArray_term : term -> term * term
894    
895     val allocVArray_term : term
896     val is_allocVArray_term : term -> bool
897     val mk_allocVArray_term : term -> term -> term -> term -> term
898     val dest_allocVArray_term : term -> term * term * term * term
899    
900     val allocMalloc_term : term
901     val is_allocMalloc_term : term -> bool
902     val mk_allocMalloc_term : term -> term -> term
903     val dest_allocMalloc_term : term -> term * term
904    
905 emre 3563 val allocFrame_term : term
906     val is_allocFrame_term : term -> bool
907     val mk_allocFrame_term : term -> term
908     val dest_allocFrame_term : term -> term
909    
910 emre 3550 (*
911     * Tail calls / operations.
912     *)
913    
914     val tailSysMigrate_term : term
915     val is_tailSysMigrate_term : term -> bool
916     val mk_tailSysMigrate_term : term -> term -> term -> term -> term -> term
917     val dest_tailSysMigrate_term : term -> term * term * term * term * term
918    
919     val tailAtomic_term : term
920     val is_tailAtomic_term : term -> bool
921     val mk_tailAtomic_term : term -> term -> term -> term
922     val dest_tailAtomic_term : term -> term * term * term
923    
924     val tailAtomicRollback_term : term
925     val is_tailAtomicRollback_term : term -> bool
926     val mk_tailAtomicRollback_term : term -> term
927     val dest_tailAtomicRollback_term : term -> term
928    
929     val tailAtomicCommit_term : term
930     val is_tailAtomicCommit_term : term -> bool
931     val mk_tailAtomicCommit_term : term -> term -> term
932     val dest_tailAtomicCommit_term : term -> term * term
933    
934     (*
935     * Predicates and assertions.
936     *)
937    
938     (* No-ops. *)
939    
940     val isMutable_term : term
941     val is_isMutable_term : term -> bool
942    
943     (* Unary operations. *)
944    
945     val reserve_term : term
946     val is_reserve_term : term -> bool
947    
948     val boundsCheckLower_term : term
949     val is_boundsCheckLower_term : term -> bool
950    
951     val boundsCheckUpper_term : term
952     val is_boundsCheckUpper_term : term -> bool
953    
954     val polyCheck_term : term
955     val is_polyCheck_term : term -> bool
956    
957     val pointerCheck_term : term
958     val is_pointerCheck_term : term -> bool
959    
960     val functionCheck_term : term
961     val is_functionCheck_term : term -> bool
962    
963     (* Binary operations. *)
964    
965     val boundsCheck_term : term
966     val is_boundsCheck_term : term -> bool
967    
968     (* Predicates. *)
969    
970     val predNop_term : term
971     val is_predNop_term : term -> bool
972     val mk_predNop_term : term -> term -> term
973     val dest_predNop_term : term -> term * term
974    
975     val predUnop_term : term
976     val is_predUnop_term : term -> bool
977     val mk_predUnop_term : term -> term -> term -> term
978     val dest_predUnop_term : term -> term * term * term
979    
980     val predBinop_term : term
981     val is_predBinop_term : term -> bool
982     val mk_predBinop_term : term -> term -> term -> term -> term
983     val dest_predBinop_term : term -> term * term * term * term
984    
985     (*
986     * Debugging info.
987     *)
988    
989     val debugLine_term : term
990     val is_debugLine_term : term -> bool
991     val mk_debugLine_term : term -> term -> term
992     val dest_debugLine_term : term -> term * term
993    
994     val debugVarItem_term : term
995     val is_debugVarItem_term : term -> bool
996     val mk_debugVarItem_term : term -> term -> term -> term
997     val dest_debugVarItem_term : term -> term * term * term
998    
999     val debugVars_term : term
1000     val is_debugVars_term : term -> bool
1001     val mk_debugVars_term : term -> term
1002     val dest_debugVars_term : term -> term
1003    
1004     val debugString_term : term
1005     val is_debugString_term : term -> bool
1006     val mk_debugString_term : term -> term
1007     val dest_debugString_term : term -> term
1008    
1009     val debugContext_term : term
1010     val is_debugContext_term : term -> bool
1011     val mk_debugContext_term : term -> term -> term
1012     val dest_debugContext_term : term -> term * term
1013    
1014     (*
1015     * Expressions.
1016     *)
1017    
1018     (* Primitive operations. *)
1019    
1020     val letUnop_term : term
1021     val is_letUnop_term : term -> bool
1022     val mk_letUnop_term : term -> term -> term -> string -> term -> term
1023     val dest_letUnop_term : term -> term * term * term * string * term
1024    
1025     val letBinop_term : term
1026     val is_letBinop_term : term -> bool
1027     val mk_letBinop_term : term -> term -> term -> term -> string -> term -> term
1028     val dest_letBinop_term : term -> term * term * term * term * string * term
1029    
1030     (* Function application. *)
1031    
1032     val letExt_term : term
1033     val is_letExt_term : term -> bool
1034     val mk_letExt_term : term -> term -> term -> term -> string -> term -> term
1035     val dest_letExt_term : term -> term * term * term * term * string * term
1036    
1037     val tailCall_term : term
1038     val is_tailCall_term : term -> bool
1039 emre 3563 val mk_tailCall_term : term -> term -> term -> term
1040     val dest_tailCall_term : term -> term * term * term
1041 emre 3550
1042     val specialCall_term : term
1043     val is_specialCall_term : term -> bool
1044 emre 3563 val mk_specialCall_term : term -> term -> term
1045     val dest_specialCall_term : term -> term * term
1046 emre 3550
1047     (* Control. *)
1048    
1049     val matchCase_term : term
1050     val is_matchCase_term : term -> bool
1051 emre 3563 val mk_matchCase_term : term -> term -> term -> term
1052     val dest_matchCase_term : term -> term * term * term
1053 emre 3550
1054     val matchExp_term : term
1055     val is_matchExp_term : term -> bool
1056     val mk_matchExp_term : term -> term -> term
1057     val dest_matchExp_term : term -> term * term
1058    
1059     val typeCase_term : term
1060     val is_typeCase_term : term -> bool
1061     val mk_typeCase_term :
1062     term -> term -> term -> term -> term -> term -> term
1063     val dest_typeCase_term :
1064     term-> term * term * term * term * term * term
1065    
1066     (* Allocation. *)
1067    
1068     val letAlloc_term : term
1069     val is_letAlloc_term : term -> bool
1070     val mk_letAlloc_term : string -> term -> term -> term
1071     val dest_letAlloc_term : term -> string * term * term
1072    
1073     (* Subscripting *)
1074    
1075     val letSubscript_term : term
1076     val is_letSubscript_term : term -> bool
1077     val mk_letSubscript_term :
1078     term -> term -> term -> term -> string -> term -> term
1079     val dest_letSubscript_term :
1080     term -> term * term * term * term * string * term
1081    
1082     val setSubscript_term : term
1083     val is_setSubscript_term : term -> bool
1084     val mk_setSubscript_term :
1085     term -> term -> term -> term -> term -> term -> term -> term
1086     val dest_setSubscript_term :
1087     term -> term * term * term * term * term * term * term
1088    
1089     val setGlobal_term : term
1090     val is_setGlobal_term : term -> bool
1091     val mk_setGlobal_term :
1092     term -> term -> term -> term -> term -> term -> term
1093     val dest_setGlobal_term :
1094     term -> term * term * term * term * term * term
1095    
1096     val memcpy_term : term
1097     val is_memcpy_term : term -> bool
1098     val mk_memcpy_term :
1099     term -> term -> term -> term -> term -> term -> term -> term -> term
1100     val dest_memcpy_term :
1101     term -> term * term * term * term * term * term * term * term
1102    
1103     (* Assertions. *)
1104    
1105     val call_term : term
1106     val is_call_term : term -> bool
1107 emre 3563 val mk_call_term : term -> term -> term -> term -> term
1108     val dest_call_term : term -> term * term * term * term
1109 emre 3550
1110     val assertExp_term : term
1111     val is_assertExp_term : term -> bool
1112     val mk_assertExp_term : term -> term -> term -> term
1113     val dest_assertExp_term : term -> term * term * term
1114    
1115     (* Debugging. *)
1116    
1117     val debug_term : term
1118     val is_debug_term : term -> bool
1119     val mk_debug_term : term -> term -> term
1120     val dest_debug_term : term -> term * term
1121 emre 3562
1122     (*
1123     * Function definition.
1124     *)
1125    
1126     val fundef_term : term
1127     val is_fundef_term : term -> bool
1128     val mk_fundef_term : term -> term -> term -> term -> term
1129     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