Changeset 1192
 Timestamp:
 Sep 6, 2011, 1:33:21 PM (9 years ago)
 Location:
 src
 Files:

 3 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1191 r1192 2 2 include "LTL/LTL.ma". 3 3 include "ERTL/spill.ma". 4 include "ERTL/build.ma". 5 include "utilities/Interference.ma". 4 6 include "ASM/Arithmetic.ma". 5 7 … … 9 11  decision_spill: Byte → decision 10 12  decision_colour: Register → decision. 13 14 definition 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 22 definition lookup: register → decision ≝ 23 λr. 24 match ? r with 25 [ colour_spill 11 26 12 27 axiom lookup: register → decision. 
src/utilities/Interference.ma
r1145 r1192 4 4 include "common/Registers.ma". 5 5 6 definition vertex ≝ nat. (* XXX: int in o'caml *) 7 8 (* vertex sets *) 9 axiom vertex_set: Type[0]. 10 11 (* vertex maps *) 12 axiom vertex_map: Type[0]. 13 6 14 definition interference_graph ≝ graph label. 7 axiom vertex: Type[0].8 axiom vertex_set: Type[0].9 axiom vertex_map: Type[0].10 15 11 16 axiom ig_create: list register → interference_graph.
Note: See TracChangeset
for help on using the changeset viewer.