/[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 3562 - (show annotations) (download)
Wed Apr 3 08:37:31 2002 UTC (19 years, 3 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 (*
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 (*
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 * Function definition.
331 *)
332
333 declare fundef{ 'debug_line; 'ty; 'var_list; 'exp }
334
335 (*************************************************************************
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
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