Changeset 1230


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

more changes

Location:
src/ERTL
Files:
2 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 ≝
  • src/ERTL/Interference.ma

    r1229 r1230  
    3434
    3535definition initial_colouring ≝ coloured_graph decision.
     36axiom colour_initial: graph → initial_colouring.
    3637definition stack_colouring ≝ coloured_graph nat.
     38axiom colour_stack: graph → stack_colouring.
    3739
    3840
     
    525527axiom ig_remove: graph → vertex → graph.
    526528axiom ig_freeze: graph → vertex → graph.
    527 axiom ig_restrict: graph → (vertex → bool) → graph.
     529axiom ig_restrict: graph → (register → bool) → graph. (* XXX: change *)
    528530axiom ig_droph: graph → graph.
    529531axiom ig_lookup: graph → register → vertex.
Note: See TracChangeset for help on using the changeset viewer.