Changeset 1232 for src/ERTL/Interference.ma

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:

• src/ERTL/Interference.ma (modified) (4 diffs)

src/ERTL/Interference.ma

@@ -15 +15 @@
 definition vertex ≝ register ⊎ Register.
 
-record graph: Type[0] ≝ 
+inductive decision: Type[0] ≝
+  | decision_spill: nat → decision
+  | decision_colour: Register → decision.
+
+definition is_member ≝
+  λvertex.
+  λregister_lattice.
+  let 〈l, r〉 ≝ register_lattice in
+  match vertex with
+  [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l
+  | inr v ⇒ set_member ? eq_Register v r
+  ].
+
+record coloured_graph (v: valuation): Type[1] ≝
 {
-  interferes: vertex → vertex → bool
+  colouring: vertex → decision;
+  prop_colouring: ∀l. ∀v1, v2: vertex.
+    is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
 }.
 
-axiom build: ∀globals: list ident. ertl_internal_function globals → valuation × graph.
-
-inductive decision: Type[0] ≝
-  | decision_spill: decision
-  | decision_colour: Register → decision.
-
-record coloured_graph (d: Type[0]): Type[1] ≝
-{
-  the_graph: graph;
-  colouring: register → d;
-  prop_colouring: ∀v1. ∀v2. (interferes the_graph (inl … v1) (inl … v2) = true) → colouring v1 ≠ colouring v2
-}.
-
-definition initial_colouring ≝ coloured_graph decision.
-axiom colour_initial: graph → initial_colouring.
-definition stack_colouring ≝ coloured_graph nat.
-axiom colour_stack: graph → stack_colouring.
-
+axiom build: ∀valuation. coloured_graph valuation.
 
 (* definition vertex_set ≝ set vertex. *)
@@ -517 +515 @@
     nmr = PrioritySet.remove x graph.nmr;
   }
-*)
-
-*)
 
 axiom ig_mkppp: graph → register → register → graph.
@@ -527 +522 @@
 axiom ig_remove: graph → vertex → graph.
 axiom ig_freeze: graph → vertex → graph.
-axiom ig_restrict: graph → (register → bool) → graph. (* XXX: change *)
+axiom ig_restrict: graph → (vertex → bool) → graph.
 axiom ig_droph: graph → graph.
 axiom ig_lookup: graph → register → vertex.
@@ -545 +540 @@
 definition ig_phedge ≝ vertex × Register.
 axiom ig_phpick: graph → (ig_phedge → bool) → option ig_phedge.
+*)
+*)