Changeset 793 for src/common


Ignore:
Timestamp:
May 12, 2011, 5:33:22 PM (9 years ago)
Author:
mulligan
Message:

Work from today on rtlabs -> rtl pass.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r764 r793  
    540540
    541541definition Trace ≝ list Identifier.
     542
     543(* dpm: how are floats represented? *)
     544inductive cast: Type[0] ≝
     545  | cast_int: Byte → cast                    (* integer constant *)
     546  | cast_float: Byte → cast                  (* float constant *)
     547  | cast_addr_symbol: ident → cast      (* address of a global symbol *)
     548  | cast_stack_offset: Byte → cast.
     549
     550inductive op1: Type[0] ≝
     551  | op_cast8_unsigned: op1   (**r 8-bit zero extension  *)
     552  | op_cast8_signed: op1     (**r 8-bit sign extension  *)
     553  | op_cast16_unsigned: op1  (**r 16-bit zero extension  *)
     554  | op_cast16_signed: op1    (**r 16-bit sign extension *)
     555  | op_neg_int: op1          (**r integer opposite *)
     556  | op_not_bool: op1         (**r boolean negation  *)
     557  | op_not_int: op1          (**r bitwise complement  *)
     558  | op_negf: op1             (**r float opposite *)
     559  | op_absf: op1             (**r float absolute value *)
     560  | op_single_of_float: op1  (**r float truncation *)
     561  | op_int_of_float: op1     (**r signed integer to float *)
     562  | op_intu_of_float: op1    (**r unsigned integer to float *)
     563  | op_float_of_int: op1     (**r float to signed integer *)
     564  | op_float_of_intu: op1    (**r float to unsigned integer *)
     565  | op_id: op1               (**r identity *)
     566  | op_ptr_of_int: op1       (**r int to pointer *)
     567  | op_int_of_ptr: op1.      (**r pointer to int *)
     568
     569inductive op2: Type[0] ≝
     570  | op_add: op2         (**r integer addition *)
     571  | op_sub: op2         (**r integer subtraction *)
     572  | op_mul: op2         (**r integer multiplication *)
     573  | op_div: op2         (**r integer signed division *)
     574  | op_divu: op2        (**r integer unsigned division *)
     575  | op_mod: op2         (**r integer signed modulus *)
     576  | op_modu: op2        (**r integer unsigned modulus *)
     577  | op_and: op2         (**r bitwise ``and'' *)
     578  | op_or: op2          (**r bitwise ``or'' *)
     579  | op_xor: op2         (**r bitwise ``xor'' *)
     580  | op_shl: op2         (**r left shift *)
     581  | op_shr: op2         (**r right signed shift *)
     582  | op_shru: op2        (**r right unsigned shift *)
     583  | op_addf: op2        (**r float addition *)
     584  | op_subf: op2        (**r float subtraction *)
     585  | op_mulf: op2        (**r float multiplication *)
     586  | op_divf: op2        (**r float division *)
     587  | op_cmp: Compare → op2   (**r integer signed comparison *)
     588  | op_cmpu: Compare → op2  (**r integer unsigned comparison *)
     589  | op_cmpf: Compare → op2  (**r float comparison *)
     590  | op_addp: op2        (**r addition for a pointer and an integer *)
     591  | op_subp: op2        (**r substraction for a pointer and a integer *)
     592  | op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracChangeset for help on using the changeset viewer.