Ignore:
Timestamp:
Sep 21, 2011, 11:24:02 AM (9 years ago)
Author:
mulligan
Message:

big changes: got what was implemented in the ertl to ltl pass type checking again

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/Interference.ma

    r1230 r1232  
    1515definition vertex ≝ register ⊎ Register.
    1616
    17 record graph: Type[0] ≝
     17inductive decision: Type[0] ≝
     18  | decision_spill: nat → decision
     19  | decision_colour: Register → decision.
     20
     21definition is_member ≝
     22  λvertex.
     23  λregister_lattice.
     24  let 〈l, r〉 ≝ register_lattice in
     25  match vertex with
     26  [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l
     27  | inr v ⇒ set_member ? eq_Register v r
     28  ].
     29
     30record coloured_graph (v: valuation): Type[1] ≝
    1831{
    19   interferes: vertex → vertex → bool
     32  colouring: vertex → decision;
     33  prop_colouring: ∀l. ∀v1, v2: vertex.
     34    is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
    2035}.
    2136
    22 axiom build: ∀globals: list ident. ertl_internal_function globals → valuation × graph.
    23 
    24 inductive decision: Type[0] ≝
    25   | decision_spill: decision
    26   | decision_colour: Register → decision.
    27 
    28 record coloured_graph (d: Type[0]): Type[1] ≝
    29 {
    30   the_graph: graph;
    31   colouring: register → d;
    32   prop_colouring: ∀v1. ∀v2. (interferes the_graph (inl … v1) (inl … v2) = true) → colouring v1 ≠ colouring v2
    33 }.
    34 
    35 definition initial_colouring ≝ coloured_graph decision.
    36 axiom colour_initial: graph → initial_colouring.
    37 definition stack_colouring ≝ coloured_graph nat.
    38 axiom colour_stack: graph → stack_colouring.
    39 
     37axiom build: ∀valuation. coloured_graph valuation.
    4038
    4139(* definition vertex_set ≝ set vertex. *)
     
    517515    nmr = PrioritySet.remove x graph.nmr;
    518516  }
    519 *)
    520 
    521 *)
    522517
    523518axiom ig_mkppp: graph → register → register → graph.
     
    527522axiom ig_remove: graph → vertex → graph.
    528523axiom ig_freeze: graph → vertex → graph.
    529 axiom ig_restrict: graph → (register → bool) → graph. (* XXX: change *)
     524axiom ig_restrict: graph → (vertex → bool) → graph.
    530525axiom ig_droph: graph → graph.
    531526axiom ig_lookup: graph → register → vertex.
     
    545540definition ig_phedge ≝ vertex × Register.
    546541axiom ig_phpick: graph → (ig_phedge → bool) → option ig_phedge.
     542*)
     543*)
Note: See TracChangeset for help on using the changeset viewer.