Changeset 1229


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

changes

Location:
src/ERTL
Files:
3 edited
1 moved

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

    r1228 r1229  
    44include "common/Order.ma".
    55include "common/Registers.ma".
     6include "ERTL/ERTL.ma".
     7include "ERTL/liveness.ma".
    68
    79include "utilities/adt/table_adt.ma".
     
    1113include "utilities/adt/register_table.ma".
    1214
     15definition vertex ≝ register ⊎ Register.
     16
     17record graph: Type[0] ≝
     18{
     19  interferes: vertex → vertex → bool
     20}.
     21
     22axiom build: ∀globals: list ident. ertl_internal_function globals → valuation × graph.
     23
     24inductive decision: Type[0] ≝
     25  | decision_spill: decision
     26  | decision_colour: Register → decision.
     27
     28record coloured_graph (d: Type[0]): Type[1] ≝
     29{
     30  the_graph: graph;
     31  colouring: register → d;
     32  prop_colouring: ∀v1. ∀v2. (interferes the_graph (inl … v1) (inl … v2) = true) → colouring v1 ≠ colouring v2
     33}.
     34
     35definition initial_colouring ≝ coloured_graph decision.
     36definition stack_colouring ≝ coloured_graph nat.
     37
     38
    1339(* definition vertex_set ≝ set vertex. *)
    1440definition vertex_priority_set ≝ priority_set vertex.
    1541definition vertex_set_table ≝ set_table vertex (set vertex).
     42definition vertex_set ≝ set vertex.
    1643definition Register_set_table ≝ set_table vertex (set Register).
    1744definition Register_set ≝ set Register.
    1845
     46(*
    1947record graph: Type[0] ≝
    2048{
     
    487515    nmr = PrioritySet.remove x graph.nmr;
    488516  }
    489  
    490 axiom ig_mkppp: interference_graph → register → register → interference_graph.
    491 axiom ig_mkpph: interference_graph → register → Register → interference_graph.
    492 axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph.
    493 axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph.
    494 axiom ig_remove: interference_graph → vertex → interference_graph.
    495 axiom ig_freeze: interference_graph → vertex → interference_graph.
    496 axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph.
    497 axiom ig_droph: interference_graph → interference_graph.
    498 axiom ig_lookup: interference_graph → register → vertex.
    499 axiom ig_registers: interference_graph → vertex → list register.
    500 axiom ig_degree: interference_graph → vertex → nat.
    501 axiom ig_lowest: interference_graph → option (vertex × nat).
    502 axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat).
     517*)
     518
     519*)
     520
     521axiom ig_mkppp: graph → register → register → graph.
     522axiom ig_mkpph: graph → register → Register → graph.
     523axiom ig_coalesce: graph → vertex → vertex → graph.
     524axiom ig_coalesceh: graph → vertex → Register → graph.
     525axiom ig_remove: graph → vertex → graph.
     526axiom ig_freeze: graph → vertex → graph.
     527axiom ig_restrict: graph → (vertex → bool) → graph.
     528axiom ig_droph: graph → graph.
     529axiom ig_lookup: graph → register → vertex.
     530axiom ig_registers: graph → vertex → list register.
     531axiom ig_degree: graph → vertex → nat.
     532axiom ig_lowest: graph → option (vertex × nat).
     533axiom ig_lowest_non_move_related: graph → option (vertex × nat).
    503534axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) →
    504   interference_graph → option vertex.
    505 axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
    506 axiom ig_ipp: interference_graph → vertex → vertex_set.
    507 axiom ig_iph: interference_graph → vertex → list Register.
    508 axiom ig_ppp: interference_graph → vertex → vertex_set.
    509 axiom ig_pph: interference_graph → vertex → list Register.
     535  graph → option vertex.
     536axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → graph → A → A.
     537axiom ig_ipp: graph → vertex → vertex_set.
     538axiom ig_iph: graph → vertex → list Register.
     539axiom ig_ppp: graph → vertex → vertex_set.
     540axiom ig_pph: graph → vertex → list Register.
    510541definition ig_ppedge ≝ vertex × vertex.
    511 axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge.
     542axiom ig_pppick: graph → (ig_ppedge → bool) → option ig_ppedge.
    512543definition ig_phedge ≝ vertex × Register.
    513 axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge.
    514 *)
     544axiom ig_phpick: graph → (ig_phedge → bool) → option ig_phedge.
  • src/ERTL/build.ma

    r1228 r1229  
    11include "ERTL/liveness.ma".
    22(* include "utilities/Interference.ma". *)
    3 
    4 definition vertex ≝ register ⊎ Register.
    5 
    6 record graph: Type[0] ≝
    7 {
    8   interferes: vertex → vertex → bool
    9 }.
    10 
    11 axiom build: ∀globals: list ident. ertl_internal_function globals → graph.
    12 
    13 inductive decision: Type[0] ≝
    14   | decision_spill: decision
    15   | decision_colour: Register → decision.
    16 
    17 record coloured_graph (d: Type[0]): Type[1] ≝
    18 {
    19   the_graph: graph;
    20   colouring: register → d;
    21   prop_colouring: ∀v1. ∀v2. (interferes the_graph (inl … v1) (inl … v2) = true) → colouring v1 ≠ colouring v2
    22 }.
    23 
    24 definition initial_colouring ≝ coloured_graph decision.
    25 definition stack_colouring ≝ coloured_graph nat.
    263
    274(*
  • src/ERTL/spill.ma

    r1128 r1229  
    11include "common/AST.ma".
    2 include "utilities/Interference.ma".
     2include "ERTL/Interference.ma".
    33
    44definition decision ≝ Immediate.
Note: See TracChangeset for help on using the changeset viewer.