Changeset 1230 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Sep 20, 2011, 3:56:40 PM (9 years ago)
Author:
mulligan
Message:

more changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1229 r1230  
    66include "ASM/Arithmetic.ma".
    77
    8 (* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *)
    9  
     8(* XXX: define an interference graph for a function and colour it, allowing
     9        the consultation of registers. *)
     10definition initial_colouring ≝
     11  λglobals.
     12  λint_fun.
     13  let 〈ignore, graph〉 ≝ build globals int_fun in
     14  let coloured ≝ colour_initial graph in
     15    coloured.
     16
    1017definition interference_lookup ≝
    11   λglobals.
    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.
    21  
    22 definition lookup: register → decision ≝
    23   λr.
    24   match ? r with
    25   [ colour_spill
    26  
    27 axiom lookup: register → decision.
     18  λcoloured: initial_colouring.
     19  λr.
     20    colouring … coloured r.
     21
     22definition prepare_graph_for_second_colouring ≝
     23  λglobals: list ident.
     24  λcoloured: initial_colouring.
     25    let g ≝ the_graph decision coloured in
     26    let restricted ≝ ig_restrict g (λv.
     27      match colouring decision coloured v with
     28      [ decision_spill ⇒ true
     29      | decision_colour _ ⇒ false
     30      ]
     31    )
     32    in restricted.
     33
     34definition second_colouring ≝
     35  λglobals: list ident.
     36  λcoloured.
     37    let prepared ≝ prepare_graph_for_second_colouring globals coloured in
     38      colour_stack prepared.
     39
     40definition lookup ≝
     41  λinitial.
     42  λsecond.
     43  λr.
     44  match interference_lookup initial r with
     45  [ decision_colour _ ⇒ ?
     46  | decision_spill ⇒ ?
     47  ].
    2848
    2949definition fresh_label ≝
Note: See TracChangeset for help on using the changeset viewer.