Changeset 1227


Ignore:
Timestamp:
Sep 19, 2011, 12:57:02 PM (8 years ago)
Author:
mulligan
Message:

changes

Files:
4 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/ERTL/ERTLToLTL.ml

    r486 r1227  
    114114  (* Build a [LTL] function. *)
    115115
    116   {
    117     LTL.f_luniverse = int_fun.ERTL.f_luniverse;
    118     LTL.f_stacksize = stacksize ;
    119     LTL.f_entry = int_fun.ERTL.f_entry;
    120     LTL.f_exit = int_fun.ERTL.f_exit;
    121     LTL.f_graph = !graph
    122   }
     116
    123117
    124118
  • Deliverables/D2.2/8051/src/utilities/interference.ml

    r486 r1227  
    518518let ipp graph v =
    519519  interference#neighborsv graph v
     520
    520521
    521522(* [iph graph v] is the set of hardware registers that the vertex [v]
     
    615616    Register.Set.fold (fun r (v, regmap, degree) ->
    616617      v+1,
    617       RegMap.add r v regmap,
     618      RegMap.add r v regmap,f
    618619      PrioritySet.add v 0 degree
    619620    ) regs (0, RegMap.empty, PrioritySet.empty)
  • src/ERTL/build.ma

    r1223 r1227  
    22include "utilities/Interference.ma".
    33
    4 axiom graph : Type[0].
     4definition vertex ≝ register ⊎ Register.
     5
     6record graph: Type[0] ≝
     7{
     8  interferes: vertex → vertex → bool
     9}.
     10
    511axiom create: ∀globals: list ident. ertl_internal_function globals → graph.
    612
    7 record build_properties: Type[1] ≝
     13inductive decision: Type[0] ≝
     14  | decision_spill: decision
     15  | decision_colour: Register → decision.
     16
     17record coloured_graph (d: Type[0]): Type[1] ≝
    818{
    9   lookup: graph → register → vertex
     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
    1022}.
     23
     24definition initial_colouring ≝ coloured_graph decision.
     25definition stack_colouring ≝ coloured_graph nat.
    1126
    1227(*
  • src/utilities/Colouring.ma

    r1193 r1227  
    11include "ASM/I8051.ma".
    22include "utilities/Interference.ma".
    3 include "utilities/RegisterSet.ma".
    43
    54inductive decision: Type[0] ≝
     
    76  | decision_colour: Register → decision.
    87
    9 definition colouring ≝ vertex_map decision.
     8definition colouring ≝ table vertex decision.
    109
    1110(* XXX: was set data structure previously *)
    12 definition colour_set ≝ rs_set.
     11definition colour_set ≝ set register.
    1312
    1413definition add_colour ≝
    15   λrs: register_set.
    1614  λc: colouring.
    1715  λr: vertex.
    18   λcs: colour_set rs.
    19   match vm_find … r c with
     16  λcs: colour_set.
     17  match tbl_lookup … r c with
    2018  [ None ⇒ cs (* XXX: correct, or should we assert false? *)
    2119  | Some decision ⇒
Note: See TracChangeset for help on using the changeset viewer.