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