Changeset 1230 for src/ERTL

Timestamp:

Sep 20, 2011, 3:56:40 PM (10 years ago)

Author:

mulligan

Message:

more changes

Location:

src/ERTL

Files:

• ERTLToLTL.ma (modified) (1 diff)
• Interference.ma (modified) (2 diffs)

src/ERTL/ERTLToLTL.ma

@@ -6 +6 @@
 include "ASM/Arithmetic.ma".
 
-(* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *)
-  
+(* XXX: define an interference graph for a function and colour it, allowing
+        the consultation of registers. *)
+definition initial_colouring ≝
+  λglobals.
+  λint_fun.
+  let 〈ignore, graph〉 ≝ build globals int_fun in
+  let coloured ≝ colour_initial graph in
+    coloured.
+
 definition interference_lookup ≝
-  λglobals.
-  λc: initial_colouring.
-  λint_fun.
-  λr.
-    
-  
-    colouring initial_colouring r.
-  let lkup ≝ ig_lookup graph r in ?.
-  check lkup.
-    tbl_find ?? lkup colour_colouring.
-  
-definition lookup: register → decision ≝
-  λr.
-  match ? r with
-  [ colour_spill 
-  
-axiom lookup: register → decision.
+  λcoloured: initial_colouring.
+  λr.
+    colouring … coloured r.
+
+definition prepare_graph_for_second_colouring ≝
+  λglobals: list ident.
+  λcoloured: initial_colouring.
+    let g ≝ the_graph decision coloured in
+    let restricted ≝ ig_restrict g (λv.
+      match colouring decision coloured v with
+      [ decision_spill ⇒ true
+      | decision_colour _ ⇒ false
+      ]
+    )
+    in restricted.
+
+definition second_colouring ≝
+  λglobals: list ident.
+  λcoloured.
+    let prepared ≝ prepare_graph_for_second_colouring globals coloured in
+      colour_stack prepared.
+
+definition lookup ≝
+  λinitial.
+  λsecond.
+  λr.
+  match interference_lookup initial r with
+  [ decision_colour _ ⇒ ?
+  | decision_spill ⇒ ?
+  ].
 
 definition fresh_label ≝

src/ERTL/Interference.ma

@@ -34 +34 @@
 
 definition initial_colouring ≝ coloured_graph decision.
+axiom colour_initial: graph → initial_colouring.
 definition stack_colouring ≝ coloured_graph nat.
+axiom colour_stack: graph → stack_colouring.
 
 
@@ -525 +527 @@
 axiom ig_remove: graph → vertex → graph.
 axiom ig_freeze: graph → vertex → graph.
-axiom ig_restrict: graph → (vertex → bool) → graph.
+axiom ig_restrict: graph → (register → bool) → graph. (* XXX: change *)
 axiom ig_droph: graph → graph.
 axiom ig_lookup: graph → register → vertex.