/[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 3550 - (show annotations) (download)
Sun Mar 24 22:35:29 2002 UTC (19 years, 4 months ago) by emre
File size: 28896 byte(s)
Updating files to reflect the newest version of the MC FIR (which happens to be
in the websplit branch).  In the process, I've also moved every file in this
theory to use the same prefix for the filenames. I've also removed quite
a few files that have been dead for a while now.

Right now, the "connect" files are not compiled in by default since they will
only compile against the websplit branch of MC and not the trunk.

Lastly, since the definition of FIR evaluation is a bit more precise now,
the need to seperately define constant elimination has been removed.

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.
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 (*
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 (*************************************************************************
330 * Term operations.
331 *************************************************************************)
332
333 (*
334 * Unary operations.
335 *)
336
337 (* Identity (polymorphic). *)
338
339 val idOp_term : term
340 val is_idOp_term : term -> bool
341
342 (* Naml ints. *)
343
344 val uminusIntOp_term : term
345 val is_uminusIntOp_term : term -> bool
346
347 val notIntOp_term : term
348 val is_notIntOp_term : term -> bool
349
350 (* Bit fields. *)
351
352 val rawBitFieldOp_term : term
353 val is_rawBitFieldOp_term : term -> bool
354 val mk_rawBitFieldOp_term : term -> term -> term -> term -> term
355 val dest_rawBitFieldOp_term : term -> term * term * term * term
356
357 (* Native ints. *)
358
359 val uminusRawIntOp_term : term
360 val is_uminusRawIntOp_term : term -> bool
361 val mk_uminusRawIntOp_term : term -> term -> term
362 val dest_uminusRawIntOp_term : term -> term * term
363
364 val notRawIntOp_term : term
365 val is_notRawIntOp_term : term -> bool
366 val mk_notRawIntOp_term : term -> term -> term
367 val dest_notRawIntOp_term : term -> term * term
368
369 (* Floats. *)
370
371 val uminusFloatOp_term : term
372 val is_uminusFloatOp_term : term -> bool
373 val mk_uminusFloatOp_term : term -> term
374 val dest_uminusFloatOp_term : term -> term
375
376 val absFloatOp_term : term
377 val is_absFloatOp_term : term -> bool
378 val mk_absFloatOp_term : term -> term
379 val dest_absFloatOp_term : term -> term
380
381 val sinOp_term : term
382 val is_sinOp_term : term -> bool
383 val mk_sinOp_term : term -> term
384 val dest_sinOp_term : term -> term
385
386 val cosOp_term : term
387 val is_cosOp_term : term -> bool
388 val mk_cosOp_term : term -> term
389 val dest_cosOp_term : term -> term
390
391 val sqrtOp_term : term
392 val is_sqrtOp_term : term -> bool
393 val mk_sqrtOp_term : term -> term
394 val dest_sqrtOp_term : term -> term
395
396 (* Coerce to int. *)
397
398 val intOfFloatOp_term : term
399 val is_intOfFloatOp_term : term -> bool
400 val mk_intOfFloatOp_term : term -> term
401 val dest_intOfFloatOp_term : term -> term
402
403 (* Coerce to float. *)
404
405 val floatOfIntOp_term : term
406 val is_floatOfIntOp_term : term -> bool
407 val mk_floatOfIntOp_term : term -> term
408 val dest_floatOfIntOp_term : term -> term
409
410 val floatOfFloatOp_term : term
411 val is_floatOfFloatOp_term : term -> bool
412 val mk_floatOfFloatOp_term : term -> term -> term
413 val dest_floatOfFloatOp_term : term -> term * term
414
415 val floatOfRawIntOp_term : term
416 val is_floatOfRawIntOp_term : term -> bool
417 val mk_floatOfRawIntOp_term : term -> term -> term -> term
418 val dest_floatOfRawIntOp_term : term -> term * term * term
419
420 (* Coerce to rawint. *)
421
422 val rawIntOfIntOp_term : term
423 val is_rawIntOfIntOp_term : term -> bool
424 val mk_rawIntOfIntOp_term : term -> term -> term
425 val dest_rawIntOfIntOp_term : term -> term * term
426
427 val rawIntOfEnumOp_term : term
428 val is_rawIntOfEnumOp_term : term -> bool
429 val mk_rawIntOfEnumOp_term : term -> term -> term -> term
430 val dest_rawIntOfEnumOp_term : term -> term * term * term
431
432 val rawIntOfFloatOp_term : term
433 val is_rawIntOfFloatOp_term : term -> bool
434 val mk_rawIntOfFloatOp_term : term -> term -> term -> term
435 val dest_rawIntOfFloatOp_term : term -> term * term * term
436
437 val rawIntOfRawIntOp_term : term
438 val is_rawIntOfRawIntOp_term : term -> bool
439 val mk_rawIntOfRawIntOp_term : term -> term -> term -> term -> term
440 val dest_rawIntOfRawIntOp_term : term -> term * term * term * term
441
442 (* Integer/pointer coercions. *)
443
444 val rawIntOfPointerOp_term : term
445 val is_rawIntOfPointerOp_term : term -> bool
446 val mk_rawIntOfPointerOp_term : term -> term -> term
447 val dest_rawIntOfPointerOp_term : term -> term * term
448
449 val pointerOfRawIntOp_term : term
450 val is_pointerOfRawIntOp_term : term -> bool
451 val mk_pointerOfRawIntOp_term : term -> term -> term
452 val dest_pointerOfRawIntOp_term : term -> term * term
453
454 (*
455 * Binary operations.
456 *)
457
458 (* Enums. *)
459
460 val andEnumOp_term : term
461 val is_andEnumOp_term : term -> bool
462 val mk_andEnumOp_term : term -> term
463 val dest_andEnumOp_term : term -> term
464
465 val orEnumOp_term : term
466 val is_orEnumOp_term : term -> bool
467 val mk_orEnumOp_term : term -> term
468 val dest_orEnumOp_term : term -> term
469
470 val xorEnumOp_term : term
471 val is_xorEnumOp_term : term -> bool
472 val mk_xorEnumOp_term : term -> term
473 val dest_xorEnumOp_term : term -> term
474
475 (* Naml ints. *)
476
477 val plusIntOp_term : term
478 val is_plusIntOp_term : term -> bool
479
480 val minusIntOp_term : term
481 val is_minusIntOp_term : term -> bool
482
483 val mulIntOp_term : term
484 val is_mulIntOp_term : term -> bool
485
486 val divIntOp_term : term
487 val is_divIntOp_term : term -> bool
488
489 val remIntOp_term : term
490 val is_remIntOp_term : term -> bool
491
492 val lslIntOp_term : term
493 val is_lslIntOp_term : term -> bool
494
495 val lsrIntOp_term : term
496 val is_lsrIntOp_term : term -> bool
497
498 val asrIntOp_term : term
499 val is_asrIntOp_term : term -> bool
500
501 val andIntOp_term : term
502 val is_andIntOp_term : term -> bool
503
504 val orIntOp_term : term
505 val is_orIntOp_term : term -> bool
506
507 val xorIntOp_term : term
508 val is_xorIntOp_term : term -> bool
509
510 val maxIntOp_term : term
511 val is_maxIntOp_term : term -> bool
512
513 val minIntOp_term : term
514 val is_minIntOp_term : term -> bool
515
516 val eqIntOp_term : term
517 val is_eqIntOp_term : term -> bool
518
519 val neqIntOp_term : term
520 val is_neqIntOp_term : term -> bool
521
522 val ltIntOp_term : term
523 val is_ltIntOp_term : term -> bool
524
525 val leIntOp_term : term
526 val is_leIntOp_term : term -> bool
527
528 val gtIntOp_term : term
529 val is_gtIntOp_term : term -> bool
530
531 val geIntOp_term : term
532 val is_geIntOp_term : term -> bool
533
534 val cmpIntOp_term : term
535 val is_cmpIntOp_term : term -> bool
536
537 (* Native ints. *)
538
539 val plusRawIntOp_term : term
540 val is_plusRawIntOp_term : term -> bool
541 val mk_plusRawIntOp_term : term -> term -> term
542 val dest_plusRawIntOp_term : term -> term * term
543
544 val minusRawIntOp_term : term
545 val is_minusRawIntOp_term : term -> bool
546 val mk_minusRawIntOp_term : term -> term -> term
547 val dest_minusRawIntOp_term : term -> term * term
548
549 val mulRawIntOp_term : term
550 val is_mulRawIntOp_term : term -> bool
551 val mk_mulRawIntOp_term : term -> term -> term
552 val dest_mulRawIntOp_term : term -> term * term
553
554 val divRawIntOp_term : term
555 val is_divRawIntOp_term : term -> bool
556 val mk_divRawIntOp_term : term -> term -> term
557 val dest_divRawIntOp_term : term -> term * term
558
559 val remRawIntOp_term : term
560 val is_remRawIntOp_term : term -> bool
561 val mk_remRawIntOp_term : term -> term -> term
562 val dest_remRawIntOp_term : term -> term * term
563
564 val slRawIntOp_term : term
565 val is_slRawIntOp_term : term -> bool
566 val mk_slRawIntOp_term : term -> term -> term
567 val dest_slRawIntOp_term : term -> term * term
568
569 val srRawIntOp_term : term
570 val is_srRawIntOp_term : term -> bool
571 val mk_srRawIntOp_term : term -> term -> term
572 val dest_srRawIntOp_term : term -> term * term
573
574 val andRawIntOp_term : term
575 val is_andRawIntOp_term : term -> bool
576 val mk_andRawIntOp_term : term -> term -> term
577 val dest_andRawIntOp_term : term -> term * term
578
579 val orRawIntOp_term : term
580 val is_orRawIntOp_term : term -> bool
581 val mk_orRawIntOp_term : term -> term -> term
582 val dest_orRawIntOp_term : term -> term * term
583
584 val xorRawIntOp_term : term
585 val is_xorRawIntOp_term : term -> bool
586 val mk_xorRawIntOp_term : term -> term -> term
587 val dest_xorRawIntOp_term : term -> term * term
588
589 val maxRawIntOp_term : term
590 val is_maxRawIntOp_term : term -> bool
591 val mk_maxRawIntOp_term : term -> term -> term
592 val dest_maxRawIntOp_term : term -> term * term
593
594 val minRawIntOp_term : term
595 val is_minRawIntOp_term : term -> bool
596 val mk_minRawIntOp_term : term -> term -> term
597 val dest_minRawIntOp_term : term -> term * term
598
599 val rawSetBitFieldOp_term : term
600 val is_rawSetBitFieldOp_term : term -> bool
601 val mk_rawSetBitFieldOp_term : term -> term -> term -> term -> term
602 val dest_rawSetBitFieldOp_term : term -> term * term * term * term
603
604 val eqRawIntOp_term : term
605 val is_eqRawIntOp_term : term -> bool
606 val mk_eqRawIntOp_term : term -> term -> term
607 val dest_eqRawIntOp_term : term -> term * term
608
609 val eqRawIntOp_term : term
610 val is_eqRawIntOp_term : term -> bool
611 val mk_eqRawIntOp_term : term -> term -> term
612 val dest_eqRawIntOp_term : term -> term * term
613
614 val neqRawIntOp_term : term
615 val is_neqRawIntOp_term : term -> bool
616 val mk_neqRawIntOp_term : term -> term -> term
617 val dest_neqRawIntOp_term : term -> term * term
618
619 val ltRawIntOp_term : term
620 val is_ltRawIntOp_term : term -> bool
621 val mk_ltRawIntOp_term : term -> term -> term
622 val dest_ltRawIntOp_term : term -> term * term
623
624 val leRawIntOp_term : term
625 val is_leRawIntOp_term : term -> bool
626 val mk_leRawIntOp_term : term -> term -> term
627 val dest_leRawIntOp_term : term -> term * term
628
629 val gtRawIntOp_term : term
630 val is_gtRawIntOp_term : term -> bool
631 val mk_gtRawIntOp_term : term -> term -> term
632 val dest_gtRawIntOp_term : term -> term * term
633
634 val geRawIntOp_term : term
635 val is_geRawIntOp_term : term -> bool
636 val mk_geRawIntOp_term : term -> term -> term
637 val dest_geRawIntOp_term : term -> term * term
638
639 val cmpRawIntOp_term : term
640 val is_cmpRawIntOp_term : term -> bool
641 val mk_cmpRawIntOp_term : term -> term -> term
642 val dest_cmpRawIntOp_term : term -> term * term
643
644 (* Floats. *)
645
646 val plusFloatOp_term : term
647 val is_plusFloatOp_term : term -> bool
648 val mk_plusFloatOp_term : term -> term
649 val dest_plusFloatOp_term : term -> term
650
651 val minusFloatOp_term : term
652 val is_minusFloatOp_term : term -> bool
653 val mk_minusFloatOp_term : term -> term
654 val dest_minusFloatOp_term : term -> term
655
656 val mulFloatOp_term : term
657 val is_mulFloatOp_term : term -> bool
658 val mk_mulFloatOp_term : term -> term
659 val dest_mulFloatOp_term : term -> term
660
661 val divFloatOp_term : term
662 val is_divFloatOp_term : term -> bool
663 val mk_divFloatOp_term : term -> term
664 val dest_divFloatOp_term : term -> term
665
666 val remFloatOp_term : term
667 val is_remFloatOp_term : term -> bool
668 val mk_remFloatOp_term : term -> term
669 val dest_remFloatOp_term : term -> term
670
671 val maxFloatOp_term : term
672 val is_maxFloatOp_term : term -> bool
673 val mk_maxFloatOp_term : term -> term
674 val dest_maxFloatOp_term : term -> term
675
676 val minFloatOp_term : term
677 val is_minFloatOp_term : term -> bool
678 val mk_minFloatOp_term : term -> term
679 val dest_minFloatOp_term : term -> term
680
681 val eqFloatOp_term : term
682 val is_eqFloatOp_term : term -> bool
683 val mk_eqFloatOp_term : term -> term
684 val dest_eqFloatOp_term : term -> term
685
686 val neqFloatOp_term : term
687 val is_neqFloatOp_term : term -> bool
688 val mk_neqFloatOp_term : term -> term
689 val dest_neqFloatOp_term : term -> term
690
691 val ltFloatOp_term : term
692 val is_ltFloatOp_term : term -> bool
693 val mk_ltFloatOp_term : term -> term
694 val dest_ltFloatOp_term : term -> term
695
696 val leFloatOp_term : term
697 val is_leFloatOp_term : term -> bool
698 val mk_leFloatOp_term : term -> term
699 val dest_leFloatOp_term : term -> term
700
701 val gtFloatOp_term : term
702 val is_gtFloatOp_term : term -> bool
703 val mk_gtFloatOp_term : term -> term
704 val dest_gtFloatOp_term : term -> term
705
706 val geFloatOp_term : term
707 val is_geFloatOp_term : term -> bool
708 val mk_geFloatOp_term : term -> term
709 val dest_geFloatOp_term : term -> term
710
711 val cmpFloatOp_term : term
712 val is_cmpFloatOp_term : term -> bool
713 val mk_cmpFloatOp_term : term -> term
714 val dest_cmpFloatOp_term : term -> term
715
716 val atan2Op_term : term
717 val is_atan2Op_term : term -> bool
718 val mk_atan2Op_term : term -> term
719 val dest_atan2Op_term : term -> term
720
721 (* Pointer equality. *)
722
723 val eqEqOp_term : term
724 val is_eqEqOp_term : term -> bool
725
726 val neqEqOp_term : term
727 val is_neqEqOp_term : term -> bool
728
729 (* Pointer arithmetic. *)
730
731 val plusPointerOp_term : term
732 val is_plusPointerOp_term : term -> bool
733 val mk_plusPointerOp_term : term -> term -> term
734 val dest_plusPointerOp_term : term -> term * term
735
736 (*
737 * Subscript operators.
738 *)
739
740 (* Blocks. *)
741
742 val blockSub_term : term
743 val is_blockSub_term : term -> bool
744
745 val rawDataSub_term : term
746 val is_rawDataSub_term : term -> bool
747
748 val tupleSub_term : term
749 val is_tupleSub_term : term -> bool
750
751 val rawTupleSub_term : term
752 val is_rawTupleSub_term : term -> bool
753
754 (* Values. *)
755
756 val polySub_term : term
757 val is_polySub_term : term -> bool
758
759 val rawIntSub_term : term
760 val is_rawIntSub_term : term -> bool
761 val mk_rawIntSub_term : term -> term -> term
762 val dest_rawIntSub_term : term -> term * term
763
764 val rawFloatSub_term : term
765 val is_rawFloatSub_term : term -> bool
766 val mk_rawFloatSub_term : term -> term
767 val dest_rawFloatSub_term : term -> term
768
769 val pointerSub_term : term
770 val is_pointerSub_term : term -> bool
771
772 val functionSub_term : term
773 val is_functionSub_term : term -> bool
774
775 (* Indexing. *)
776
777 val byteIndex_term : term
778 val is_byteIndex_term : term -> bool
779
780 val wordIndex_term : term
781 val is_wordIndex_term : term -> bool
782
783 (* Subscripting. *)
784
785 val intIndex_term : term
786 val is_intIndex_term : term -> bool
787
788 val rawIntIndex_term : term
789 val is_rawIntIndex_term : term -> bool
790 val mk_rawIntIndex_term : term -> term -> term
791 val dest_rawIntIndex_term : term -> term * term
792
793 (* Susbscripting op. *)
794
795 val subop_term : term
796 val is_subop_term : term -> bool
797 val mk_subop_term : term -> term -> term -> term -> term
798 val dest_subop_term : term -> term * term * term * term
799
800 (*
801 * Normal values.
802 *)
803
804 val atomNil_term : term
805 val is_atomNil_term : term -> bool
806 val mk_atomNil_term : term -> term
807 val dest_atomNil_term : term -> term
808
809 val atomInt_term : term
810 val is_atomInt_term : term -> bool
811 val mk_atomInt_term : term -> term
812 val dest_atomInt_term : term -> term
813
814 val atomEnum_term : term
815 val is_atomEnum_term : term -> bool
816 val mk_atomEnum_term : term -> term -> term
817 val dest_atomEnum_term : term -> term * term
818
819 val atomRawInt_term : term
820 val is_atomRawInt_term : term -> bool
821 val mk_atomRawInt_term : term -> term -> term -> term
822 val dest_atomRawInt_term : term -> term * term * term
823
824 val atomFloat_term : term
825 val is_atomFloat_term : term -> bool
826 val mk_atomFloat_term : term -> term -> term
827 val dest_atomFloat_term : term -> term * term
828
829 val atomConst_term : term
830 val is_atomConst_term : term -> bool
831 val mk_atomConst_term : term -> term -> term -> term
832 val dest_atomConst_term : term -> term * term * term
833
834 val atomVar_term : term
835 val is_atomVar_term : term -> bool
836 val mk_atomVar_term : term -> term
837 val dest_atomVar_term : term -> term
838
839 (*
840 * Allocation operators.
841 *)
842
843 val allocTuple_term : term
844 val is_allocTuple_term : term -> bool
845 val mk_allocTuple_term : term -> term -> term -> term
846 val dest_allocTuple_term : term -> term * term * term
847
848 val allocUnion_term : term
849 val is_allocUnion_term : term -> bool
850 val mk_allocUnion_term : term -> term -> term -> term -> term
851 val dest_allocUnion_term : term -> term * term * term * term
852
853 val allocArray_term : term
854 val is_allocArray_term : term -> bool
855 val mk_allocArray_term : term -> term -> term
856 val dest_allocArray_term : term -> term * term
857
858 val allocVArray_term : term
859 val is_allocVArray_term : term -> bool
860 val mk_allocVArray_term : term -> term -> term -> term -> term
861 val dest_allocVArray_term : term -> term * term * term * term
862
863 val allocMalloc_term : term
864 val is_allocMalloc_term : term -> bool
865 val mk_allocMalloc_term : term -> term -> term
866 val dest_allocMalloc_term : term -> term * term
867
868 (*
869 * Tail calls / operations.
870 *)
871
872 val tailSysMigrate_term : term
873 val is_tailSysMigrate_term : term -> bool
874 val mk_tailSysMigrate_term : term -> term -> term -> term -> term -> term
875 val dest_tailSysMigrate_term : term -> term * term * term * term * term
876
877 val tailAtomic_term : term
878 val is_tailAtomic_term : term -> bool
879 val mk_tailAtomic_term : term -> term -> term -> term
880 val dest_tailAtomic_term : term -> term * term * term
881
882 val tailAtomicRollback_term : term
883 val is_tailAtomicRollback_term : term -> bool
884 val mk_tailAtomicRollback_term : term -> term
885 val dest_tailAtomicRollback_term : term -> term
886
887 val tailAtomicCommit_term : term
888 val is_tailAtomicCommit_term : term -> bool
889 val mk_tailAtomicCommit_term : term -> term -> term
890 val dest_tailAtomicCommit_term : term -> term * term
891
892 (*
893 * Predicates and assertions.
894 *)
895
896 (* No-ops. *)
897
898 val isMutable_term : term
899 val is_isMutable_term : term -> bool
900
901 (* Unary operations. *)
902
903 val reserve_term : term
904 val is_reserve_term : term -> bool
905
906 val boundsCheckLower_term : term
907 val is_boundsCheckLower_term : term -> bool
908
909 val boundsCheckUpper_term : term
910 val is_boundsCheckUpper_term : term -> bool
911
912 val polyCheck_term : term
913 val is_polyCheck_term : term -> bool
914
915 val pointerCheck_term : term
916 val is_pointerCheck_term : term -> bool
917
918 val functionCheck_term : term
919 val is_functionCheck_term : term -> bool
920
921 (* Binary operations. *)
922
923 val boundsCheck_term : term
924 val is_boundsCheck_term : term -> bool
925
926 (* Predicates. *)
927
928 val predNop_term : term
929 val is_predNop_term : term -> bool
930 val mk_predNop_term : term -> term -> term
931 val dest_predNop_term : term -> term * term
932
933 val predUnop_term : term
934 val is_predUnop_term : term -> bool
935 val mk_predUnop_term : term -> term -> term -> term
936 val dest_predUnop_term : term -> term * term * term
937
938 val predBinop_term : term
939 val is_predBinop_term : term -> bool
940 val mk_predBinop_term : term -> term -> term -> term -> term
941 val dest_predBinop_term : term -> term * term * term * term
942
943 (*
944 * Debugging info.
945 *)
946
947 val debugLine_term : term
948 val is_debugLine_term : term -> bool
949 val mk_debugLine_term : term -> term -> term
950 val dest_debugLine_term : term -> term * term
951
952 val debugVarItem_term : term
953 val is_debugVarItem_term : term -> bool
954 val mk_debugVarItem_term : term -> term -> term -> term
955 val dest_debugVarItem_term : term -> term * term * term
956
957 val debugVars_term : term
958 val is_debugVars_term : term -> bool
959 val mk_debugVars_term : term -> term
960 val dest_debugVars_term : term -> term
961
962 val debugString_term : term
963 val is_debugString_term : term -> bool
964 val mk_debugString_term : term -> term
965 val dest_debugString_term : term -> term
966
967 val debugContext_term : term
968 val is_debugContext_term : term -> bool
969 val mk_debugContext_term : term -> term -> term
970 val dest_debugContext_term : term -> term * term
971
972 (*
973 * Expressions.
974 *)
975
976 (* Primitive operations. *)
977
978 val letUnop_term : term
979 val is_letUnop_term : term -> bool
980 val mk_letUnop_term : term -> term -> term -> string -> term -> term
981 val dest_letUnop_term : term -> term * term * term * string * term
982
983 val letBinop_term : term
984 val is_letBinop_term : term -> bool
985 val mk_letBinop_term : term -> term -> term -> term -> string -> term -> term
986 val dest_letBinop_term : term -> term * term * term * term * string * term
987
988 (* Function application. *)
989
990 val letExt_term : term
991 val is_letExt_term : term -> bool
992 val mk_letExt_term : term -> term -> term -> term -> string -> term -> term
993 val dest_letExt_term : term -> term * term * term * term * string * term
994
995 val tailCall_term : term
996 val is_tailCall_term : term -> bool
997 val mk_tailCall_term : term -> term -> term
998 val dest_tailCall_term : term -> term * term
999
1000 val specialCall_term : term
1001 val is_specialCall_term : term -> bool
1002 val mk_specialCall_term : term -> term
1003 val dest_specialCall_term : term -> term
1004
1005 (* Control. *)
1006
1007 val matchCase_term : term
1008 val is_matchCase_term : term -> bool
1009 val mk_matchCase_term : term -> term -> term
1010 val dest_matchCase_term : term -> term * term
1011
1012 val matchExp_term : term
1013 val is_matchExp_term : term -> bool
1014 val mk_matchExp_term : term -> term -> term
1015 val dest_matchExp_term : term -> term * term
1016
1017 val typeCase_term : term
1018 val is_typeCase_term : term -> bool
1019 val mk_typeCase_term :
1020 term -> term -> term -> term -> term -> term -> term
1021 val dest_typeCase_term :
1022 term-> term * term * term * term * term * term
1023
1024 (* Allocation. *)
1025
1026 val letAlloc_term : term
1027 val is_letAlloc_term : term -> bool
1028 val mk_letAlloc_term : string -> term -> term -> term
1029 val dest_letAlloc_term : term -> string * term * term
1030
1031 (* Subscripting *)
1032
1033 val letSubscript_term : term
1034 val is_letSubscript_term : term -> bool
1035 val mk_letSubscript_term :
1036 term -> term -> term -> term -> string -> term -> term
1037 val dest_letSubscript_term :
1038 term -> term * term * term * term * string * term
1039
1040 val setSubscript_term : term
1041 val is_setSubscript_term : term -> bool
1042 val mk_setSubscript_term :
1043 term -> term -> term -> term -> term -> term -> term -> term
1044 val dest_setSubscript_term :
1045 term -> term * term * term * term * term * term * term
1046
1047 val setGlobal_term : term
1048 val is_setGlobal_term : term -> bool
1049 val mk_setGlobal_term :
1050 term -> term -> term -> term -> term -> term -> term
1051 val dest_setGlobal_term :
1052 term -> term * term * term * term * term * term
1053
1054 val memcpy_term : term
1055 val is_memcpy_term : term -> bool
1056 val mk_memcpy_term :
1057 term -> term -> term -> term -> term -> term -> term -> term -> term
1058 val dest_memcpy_term :
1059 term -> term * term * term * term * term * term * term * term
1060
1061 (* Assertions. *)
1062
1063 val call_term : term
1064 val is_call_term : term -> bool
1065 val mk_call_term : term -> term -> term -> term
1066 val dest_call_term : term -> term * term * term
1067
1068 val assertExp_term : term
1069 val is_assertExp_term : term -> bool
1070 val mk_assertExp_term : term -> term -> term -> term
1071 val dest_assertExp_term : term -> term * term * term
1072
1073 (* Debugging. *)
1074
1075 val debug_term : term
1076 val is_debug_term : term -> bool
1077 val mk_debug_term : term -> term -> term
1078 val dest_debug_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