Changeset 1229 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Sep 20, 2011, 1:26:46 PM (9 years ago)
Author:
mulligan
Message:

changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1192 r1229  
    33include "ERTL/spill.ma".
    44include "ERTL/build.ma".
    5 include "utilities/Interference.ma".
     5include "ERTL/Interference.ma".
    66include "ASM/Arithmetic.ma".
    77
    88(* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *)
    9 
    10 inductive decision: Type[0] ≝
    11   | decision_spill: Byte → decision
    12   | decision_colour: Register → decision.
    139 
    1410definition interference_lookup ≝
    1511  λglobals.
    16   λint_fun.
    17   λr.
    18   let 〈liveafter, graph〉 ≝ build globals int_fun in
    19   let lkup ≝ ig_lookup graph r in
    20     vm_find lkup colour_colouring.
     12  λc: initial_colouring.
     13  λint_fun.
     14  λr.
     15   
     16 
     17    colouring initial_colouring r.
     18  let lkup ≝ ig_lookup graph r in ?.
     19  check lkup.
     20    tbl_find ?? lkup colour_colouring.
    2121 
    2222definition lookup: register → decision ≝
Note: See TracChangeset for help on using the changeset viewer.