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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3563 - (show annotations) (download)
Fri Apr 5 01:16:49 2002 UTC (19 years, 4 months ago) by emre
File size: 30184 byte(s)
Updates to reflect the (ever changing) MC FIR.

1 (*
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 * pred_binop, pred, debug_line, debug_vars, debug_info, exp, fundef.
8 *
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 (* Pointer operations. *)
100
101 declare rawIntOfLabelOp{ 'int_precision; 'int_signed }
102
103 (*
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 * Fields (frame labels).
226 *)
227
228 declare frameLabel{ 'label1; 'label2; 'label3 }
229
230 (*
231 * Normal values.
232 *)
233
234 declare atomNil{ 'ty }
235 declare atomInt{ 'int }
236 declare atomEnum{ 'int1; 'int2 }
237 declare atomRawInt{ 'int_precision; 'int_signed; 'num }
238 declare atomFloat{ 'float_precision; 'num }
239 declare atomLabel{ 'frame_label }
240 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 declare allocFrame{ 'var }
253
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 declare tailCall{ 'label; 'var; 'atom_list }
313 declare specialCall{ 'label; 'tailop }
314
315 (* Control. *)
316
317 declare matchCase{ 'label; 'set; 'exp }
318 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 declare call{ 'label; 'var; 'atom_option_list; 'exp }
335 declare assertExp{ 'label; 'pred; 'exp }
336
337 (* Debugging. *)
338
339 declare debug{ 'debug_info; 'exp }
340
341 (*
342 * Function definition.
343 *)
344
345 declare fundef{ 'debug_line; 'ty; 'var_list; 'exp }
346
347 (*************************************************************************
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 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 (*
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 * 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 * 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 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 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 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 (*
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 val mk_tailCall_term : term -> term -> term -> term
1040 val dest_tailCall_term : term -> term * term * term
1041
1042 val specialCall_term : term
1043 val is_specialCall_term : term -> bool
1044 val mk_specialCall_term : term -> term -> term
1045 val dest_specialCall_term : term -> term * term
1046
1047 (* Control. *)
1048
1049 val matchCase_term : term
1050 val is_matchCase_term : term -> bool
1051 val mk_matchCase_term : term -> term -> term -> term
1052 val dest_matchCase_term : term -> term * term * term
1053
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 val mk_call_term : term -> term -> term -> term -> term
1108 val dest_call_term : term -> term * term * term * term
1109
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
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