Changeset 1064 for src/common


Ignore:
Timestamp:
Jul 12, 2011, 5:52:07 PM (8 years ago)
Author:
mulligan
Message:

changes from today, nearly complete rtlabs translation pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1060 r1064  
    104104  | I32: intsize.
    105105
    106 (* unary operations used in the backend intermediate languages, there's also a separate
    107    type for unary operations at the assembly level in ASM/I8051.ma *)
    108 inductive intermediate_op1: Type[0] ≝
    109   | intermediate_op1_cast: nat → signedness → nat → intermediate_op1 (**r size in bytes, signedness, to size *)
    110   | intermediate_op1_negint: intermediate_op1           (**r integer opposite *)
    111   | intermediate_op1_notbool: intermediate_op1          (**r boolean negation  *)
    112   | intermediate_op1_notint: intermediate_op1           (**r bitwise complement  *)
    113   | intermediate_op1_id: intermediate_op1               (**r identity *)
    114   | intermediate_op1_ptrofint: intermediate_op1         (**r int to pointer *)
    115   | intermediate_op1_intofptr: intermediate_op1.        (**r pointer to int *)
    116 
    117106(* * Float types come in two sizes: 32 bits (single precision)
    118107  and 64-bit (double precision). *)
     
    409398
    410399Remark map_partial_identity:
    411   forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
     400  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),cmp
    412401  map_partial prefix (fun b => OK b) l = OK l.
    413402Proof.
     
    665654
    666655inductive op1: Type[0] ≝
    667   | op_cast8_unsigned: op1   (**r 8-bit zero extension  *)
    668   | op_cast8_signed: op1     (**r 8-bit sign extension  *)
    669   | op_cast16_unsigned: op1  (**r 16-bit zero extension  *)
    670   | op_cast16_signed: op1    (**r 16-bit sign extension *)
     656  | op_cast: nat → signedness → nat → op1
    671657  | op_neg_int: op1          (**r integer opposite *)
    672658  | op_not_bool: op1         (**r boolean negation  *)
    673659  | op_not_int: op1          (**r bitwise complement  *)
    674   | op_negf: op1             (**r float opposite *)
    675   | op_absf: op1             (**r float absolute value *)
    676   | op_single_of_float: op1  (**r float truncation *)
    677   | op_int_of_float: op1     (**r signed integer to float *)
    678   | op_intu_of_float: op1    (**r unsigned integer to float *)
    679   | op_float_of_int: op1     (**r float to signed integer *)
    680   | op_float_of_intu: op1    (**r float to unsigned integer *)
    681660  | op_id: op1               (**r identity *)
    682661  | op_ptr_of_int: op1       (**r int to pointer *)
     
    697676  | op_shr: op2         (**r right signed shift *)
    698677  | op_shru: op2        (**r right unsigned shift *)
    699   | op_addf: op2        (**r float addition *)
    700   | op_subf: op2        (**r float subtraction *)
    701   | op_mulf: op2        (**r float multiplication *)
    702   | op_divf: op2        (**r float division *)
    703678  | op_cmp: Compare → op2   (**r integer signed comparison *)
    704679  | op_cmpu: Compare → op2  (**r integer unsigned comparison *)
    705   | op_cmpf: Compare → op2  (**r float comparison *)
    706680  | op_addp: op2        (**r addition for a pointer and an integer *)
    707681  | op_subp: op2        (**r substraction for a pointer and a integer *)
     682  | op_subpp: op2
    708683  | op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracChangeset for help on using the changeset viewer.