Changeset 1193 for src/ASM


Ignore:
Timestamp:
Sep 6, 2011, 3:49:31 PM (9 years ago)
Author:
mulligan
Message:

work on colouring algorithm halted as it can be axiomatised. now implementing interference graphs (objects!)

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r1187 r1193  
    147147definition RegisterSPL ≝ Register06.
    148148definition RegisterSPH ≝ Register07.
    149 definition RegisterForbidden: list Register ≝
    150   [ RegisterSST; RegisterST0; RegisterST1;
    151     RegisterSPL; RegisterSPH ].
    152149definition RegisterParams: list Register ≝
    153150  [ Register30; Register31; Register32; Register33;
     
    177174   RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
    178175   RegisterST2; RegisterST3; RegisterSST].
     176(* registers minus forbidden *)
     177definition RegistersAllocatable ≝
     178  [Register00; Register01; Register02; Register03; Register04;
     179   Register05; Register06; Register07; Register10; Register11;
     180   Register12; Register13; Register14; Register15; Register16;
     181   Register17; Register20; Register21; Register22; Register23;
     182   Register24; Register25; Register26; Register27; Register30;
     183   Register31; Register32; Register33; Register34; Register35;
     184   Register36; Register37].
    179185
    180186definition register_address: Register → [[ acc_a; direct; registr ]] ≝
  • src/ASM/Util.ma

    r1161 r1193  
    4747  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
    4848  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
     49  ].
     50
     51let rec forall
     52  (A: Type[0]) (f: A → bool) (l: list A)
     53    on l ≝
     54  match l with
     55  [ nil        ⇒ true
     56  | cons hd tl ⇒ f hd ∧ forall A f tl
    4957  ].
    5058
Note: See TracChangeset for help on using the changeset viewer.