Changeset 777 for src/ASM/I8051.ma


Ignore:
Timestamp:
Apr 27, 2011, 5:25:26 PM (9 years ago)
Author:
mulligan
Message:

Lots of work on RTL to ERTL pass from today.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r757 r777  
    66include "ASM/Arithmetic.ma".
    77include "utilities/Compare.ma".
     8
     9definition int_size ≝ bitvector_of_nat 8 1.
     10definition ptr_size ≝ bitvector_of_nat 8 2.
     11definition alignment ≝ None.
    812
    913(* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps
     
    125129      ].
    126130
    127 definition eq_register: Register → Register → bool ≝
     131definition eq_Register: Register → Register → bool ≝
    128132  λr, s: Register.
    129133  let r_as_nat ≝ nat_of_register r in
     
    178182  [ RegisterSST; RegisterST0; RegisterST1;
    179183    RegisterSPL; RegisterSPH ].
     184   
     185definition parameters: list Register ≝
     186  [ Register30; Register31; Register32; Register33;
     187    Register34; Register35; Register36; Register37 ].
    180188   
    181189record RegisterMap: Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.