/[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 3562 - (hide annotations) (download)
Wed Apr 3 08:37:31 2002 UTC (19 years, 4 months ago) by emre
File size: 29194 byte(s)
So, I've defined the compile function in Mp_mc_compile to actually
take an Fir.prog, convert the function definitions to terms,
and then back again, in one big identity operation.  The current
term representation of the FIR functions is a bit of a hack that
will need to be cleaned up if anything non-trivial is to be done.
(Each individual function is fine I hope.  It's the program as a whole
that's represented rather poorly.  It's essentially a (term SymbolTable.t),
one term for each fundef in the original Fir.prog.prog_funs.)
Though, this should be sufficient for basic testing I think.

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