Changeset 1465


Ignore:
Timestamp:
Oct 26, 2011, 2:07:41 PM (8 years ago)
Author:
sacerdot
Message:

Dead code removed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1401 r1465  
    664664      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
    665665  ].
    666 
    667 (* TODO: merge in comparison definitions from Integers.ma. *)
    668 inductive Compare: Type[0] ≝
    669   Compare_Equal: Compare
    670 | Compare_NotEqual: Compare
    671 | Compare_Less: Compare
    672 | Compare_Greater: Compare
    673 | Compare_LessEqual: Compare
    674 | Compare_GreaterEqual: Compare.
    675 
    676 inductive op1: Type[0] ≝
    677   | op_cast: nat → signedness → nat → op1
    678   | 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: op2
    704   | op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracChangeset for help on using the changeset viewer.