Changeset 1465 for src/common
- Timestamp:
- Oct 26, 2011, 2:07:41 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/AST.ma
r1401 r1465 664 664 bool_to_Prop (eq_i hd i) ∨ member i eq_i tl 665 665 ]. 666 667 (* TODO: merge in comparison definitions from Integers.ma. *)668 inductive Compare: Type[0] ≝669 Compare_Equal: Compare670 | Compare_NotEqual: Compare671 | Compare_Less: Compare672 | Compare_Greater: Compare673 | Compare_LessEqual: Compare674 | Compare_GreaterEqual: Compare.675 676 inductive op1: Type[0] ≝677 | op_cast: nat → signedness → nat → op1678 | op_neg_int: op1 (**r integer opposite *)679 | op_not_bool: op1 (**r boolean negation *)680 | op_not_int: op1 (**r bitwise complement *)681 | op_id: op1 (**r identity *)682 | op_ptr_of_int: op1 (**r int to pointer *)683 | op_int_of_ptr: op1. (**r pointer to int *)684 685 inductive op2: Type[0] ≝686 | op_add: op2 (**r integer addition *)687 | op_sub: op2 (**r integer subtraction *)688 | op_mul: op2 (**r integer multiplication *)689 | op_div: op2 (**r integer signed division *)690 | op_divu: op2 (**r integer unsigned division *)691 | op_mod: op2 (**r integer signed modulus *)692 | op_modu: op2 (**r integer unsigned modulus *)693 | op_and: op2 (**r bitwise ``and'' *)694 | op_or: op2 (**r bitwise ``or'' *)695 | op_xor: op2 (**r bitwise ``xor'' *)696 | op_shl: op2 (**r left shift *)697 | op_shr: op2 (**r right signed shift *)698 | op_shru: op2 (**r right unsigned shift *)699 | op_cmp: Compare → op2 (**r integer signed comparison *)700 | op_cmpu: Compare → op2 (**r integer unsigned comparison *)701 | op_addp: op2 (**r addition for a pointer and an integer *)702 | op_subp: op2 (**r substraction for a pointer and a integer *)703 | op_subpp: op2704 | op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracChangeset
for help on using the changeset viewer.