Changeset 793 for src/common

Timestamp:

May 12, 2011, 5:33:22 PM (9 years ago)

Author:

mulligan

Message:

Work from today on rtlabs -> rtl pass.

File:

• src/common/AST.ma (modified) (1 diff)

src/common/AST.ma

@@ -540 +540 @@
 
 definition Trace ≝ list Identifier.
+
+(* dpm: how are floats represented? *)
+inductive cast: Type[0] ≝
+  | cast_int: Byte → cast                    (* integer constant *)
+  | cast_float: Byte → cast                  (* float constant *)
+  | cast_addr_symbol: ident → cast      (* address of a global symbol *)
+  | cast_stack_offset: Byte → cast.
+
+inductive op1: Type[0] ≝
+  | op_cast8_unsigned: op1   (**r 8-bit zero extension  *)
+  | op_cast8_signed: op1     (**r 8-bit sign extension  *)
+  | op_cast16_unsigned: op1  (**r 16-bit zero extension  *)
+  | op_cast16_signed: op1    (**r 16-bit sign extension *)
+  | op_neg_int: op1          (**r integer opposite *)
+  | op_not_bool: op1         (**r boolean negation  *)
+  | op_not_int: op1          (**r bitwise complement  *)
+  | op_negf: op1             (**r float opposite *)
+  | op_absf: op1             (**r float absolute value *)
+  | op_single_of_float: op1  (**r float truncation *)
+  | op_int_of_float: op1     (**r signed integer to float *)
+  | op_intu_of_float: op1    (**r unsigned integer to float *)
+  | op_float_of_int: op1     (**r float to signed integer *)
+  | op_float_of_intu: op1    (**r float to unsigned integer *)
+  | op_id: op1               (**r identity *)
+  | op_ptr_of_int: op1       (**r int to pointer *)
+  | op_int_of_ptr: op1.      (**r pointer to int *)
+
+inductive op2: Type[0] ≝
+  | op_add: op2         (**r integer addition *)
+  | op_sub: op2         (**r integer subtraction *)
+  | op_mul: op2         (**r integer multiplication *)
+  | op_div: op2         (**r integer signed division *)
+  | op_divu: op2        (**r integer unsigned division *)
+  | op_mod: op2         (**r integer signed modulus *)
+  | op_modu: op2        (**r integer unsigned modulus *)
+  | op_and: op2         (**r bitwise ``and'' *)
+  | op_or: op2          (**r bitwise ``or'' *)
+  | op_xor: op2         (**r bitwise ``xor'' *)
+  | op_shl: op2         (**r left shift *)
+  | op_shr: op2         (**r right signed shift *)
+  | op_shru: op2        (**r right unsigned shift *)
+  | op_addf: op2        (**r float addition *)
+  | op_subf: op2        (**r float subtraction *)
+  | op_mulf: op2        (**r float multiplication *)
+  | op_divf: op2        (**r float division *)
+  | op_cmp: Compare → op2   (**r integer signed comparison *)
+  | op_cmpu: Compare → op2  (**r integer unsigned comparison *)
+  | op_cmpf: Compare → op2  (**r float comparison *)
+  | op_addp: op2        (**r addition for a pointer and an integer *)
+  | op_subp: op2        (**r substraction for a pointer and a integer *)
+  | op_cmpp: Compare → op2. (**r pointer comparaison *)