Changeset 1192


Ignore:
Timestamp:
Sep 6, 2011, 1:33:21 PM (8 years ago)
Author:
mulligan
Message:

some files that were missing / laying dormant on my computer

Location:
src
Files:
3 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1191 r1192  
    22include "LTL/LTL.ma".
    33include "ERTL/spill.ma".
     4include "ERTL/build.ma".
     5include "utilities/Interference.ma".
    46include "ASM/Arithmetic.ma".
    57
     
    911  | decision_spill: Byte → decision
    1012  | decision_colour: Register → decision.
     13 
     14definition interference_lookup ≝
     15  λ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.
     21 
     22definition lookup: register → decision ≝
     23  λr.
     24  match ? r with
     25  [ colour_spill
    1126 
    1227axiom lookup: register → decision.
  • src/utilities/Interference.ma

    r1145 r1192  
    44include "common/Registers.ma".
    55
     6definition vertex ≝ nat. (* XXX: int in o'caml *)
     7
     8(* vertex sets *)
     9axiom vertex_set: Type[0].
     10
     11(* vertex maps *)
     12axiom vertex_map: Type[0].
     13
    614definition interference_graph ≝ graph label.
    7 axiom vertex: Type[0].
    8 axiom vertex_set: Type[0].
    9 axiom vertex_map: Type[0].
    1015
    1116axiom ig_create: list register → interference_graph.
Note: See TracChangeset for help on using the changeset viewer.