Changeset 1227 for src


Ignore:
Timestamp:
Sep 19, 2011, 12:57:02 PM (9 years ago)
Author:
mulligan
Message:

changes

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/build.ma

    r1223 r1227  
    22include "utilities/Interference.ma".
    33
    4 axiom graph : Type[0].
     4definition vertex ≝ register ⊎ Register.
     5
     6record graph: Type[0] ≝
     7{
     8  interferes: vertex → vertex → bool
     9}.
     10
    511axiom create: ∀globals: list ident. ertl_internal_function globals → graph.
    612
    7 record build_properties: Type[1] ≝
     13inductive decision: Type[0] ≝
     14  | decision_spill: decision
     15  | decision_colour: Register → decision.
     16
     17record coloured_graph (d: Type[0]): Type[1] ≝
    818{
    9   lookup: graph → register → vertex
     19  the_graph: graph;
     20  colouring: register → d;
     21  prop_colouring: ∀v1. ∀v2. (interferes the_graph (inl … v1) (inl … v2) = true) → colouring v1 ≠ colouring v2
    1022}.
     23
     24definition initial_colouring ≝ coloured_graph decision.
     25definition stack_colouring ≝ coloured_graph nat.
    1126
    1227(*
  • src/utilities/Colouring.ma

    r1193 r1227  
    11include "ASM/I8051.ma".
    22include "utilities/Interference.ma".
    3 include "utilities/RegisterSet.ma".
    43
    54inductive decision: Type[0] ≝
     
    76  | decision_colour: Register → decision.
    87
    9 definition colouring ≝ vertex_map decision.
     8definition colouring ≝ table vertex decision.
    109
    1110(* XXX: was set data structure previously *)
    12 definition colour_set ≝ rs_set.
     11definition colour_set ≝ set register.
    1312
    1413definition add_colour ≝
    15   λrs: register_set.
    1614  λc: colouring.
    1715  λr: vertex.
    18   λcs: colour_set rs.
    19   match vm_find … r c with
     16  λcs: colour_set.
     17  match tbl_lookup … r c with
    2018  [ None ⇒ cs (* XXX: correct, or should we assert false? *)
    2119  | Some decision ⇒
Note: See TracChangeset for help on using the changeset viewer.