Changeset 1227 for src/ERTL


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

changes

File:
1 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(*
Note: See TracChangeset for help on using the changeset viewer.