Changeset 1229
 Timestamp:
 Sep 20, 2011, 1:26:46 PM (9 years ago)
 Location:
 src/ERTL
 Files:

 3 edited
 1 moved
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1192 r1229 3 3 include "ERTL/spill.ma". 4 4 include "ERTL/build.ma". 5 include " utilities/Interference.ma".5 include "ERTL/Interference.ma". 6 6 include "ASM/Arithmetic.ma". 7 7 8 8 (* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *) 9 10 inductive decision: Type[0] ≝11  decision_spill: Byte → decision12  decision_colour: Register → decision.13 9 14 10 definition interference_lookup ≝ 15 11 λ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. 21 21 22 22 definition lookup: register → decision ≝ 
src/ERTL/Interference.ma
r1228 r1229 4 4 include "common/Order.ma". 5 5 include "common/Registers.ma". 6 include "ERTL/ERTL.ma". 7 include "ERTL/liveness.ma". 6 8 7 9 include "utilities/adt/table_adt.ma". … … 11 13 include "utilities/adt/register_table.ma". 12 14 15 definition vertex ≝ register ⊎ Register. 16 17 record graph: Type[0] ≝ 18 { 19 interferes: vertex → vertex → bool 20 }. 21 22 axiom build: ∀globals: list ident. ertl_internal_function globals → valuation × graph. 23 24 inductive decision: Type[0] ≝ 25  decision_spill: decision 26  decision_colour: Register → decision. 27 28 record 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 35 definition initial_colouring ≝ coloured_graph decision. 36 definition stack_colouring ≝ coloured_graph nat. 37 38 13 39 (* definition vertex_set ≝ set vertex. *) 14 40 definition vertex_priority_set ≝ priority_set vertex. 15 41 definition vertex_set_table ≝ set_table vertex (set vertex). 42 definition vertex_set ≝ set vertex. 16 43 definition Register_set_table ≝ set_table vertex (set Register). 17 44 definition Register_set ≝ set Register. 18 45 46 (* 19 47 record graph: Type[0] ≝ 20 48 { … … 487 515 nmr = PrioritySet.remove x graph.nmr; 488 516 } 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 521 axiom ig_mkppp: graph → register → register → graph. 522 axiom ig_mkpph: graph → register → Register → graph. 523 axiom ig_coalesce: graph → vertex → vertex → graph. 524 axiom ig_coalesceh: graph → vertex → Register → graph. 525 axiom ig_remove: graph → vertex → graph. 526 axiom ig_freeze: graph → vertex → graph. 527 axiom ig_restrict: graph → (vertex → bool) → graph. 528 axiom ig_droph: graph → graph. 529 axiom ig_lookup: graph → register → vertex. 530 axiom ig_registers: graph → vertex → list register. 531 axiom ig_degree: graph → vertex → nat. 532 axiom ig_lowest: graph → option (vertex × nat). 533 axiom ig_lowest_non_move_related: graph → option (vertex × nat). 503 534 axiom 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. 536 axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → graph → A → A. 537 axiom ig_ipp: graph → vertex → vertex_set. 538 axiom ig_iph: graph → vertex → list Register. 539 axiom ig_ppp: graph → vertex → vertex_set. 540 axiom ig_pph: graph → vertex → list Register. 510 541 definition ig_ppedge ≝ vertex × vertex. 511 axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge.542 axiom ig_pppick: graph → (ig_ppedge → bool) → option ig_ppedge. 512 543 definition ig_phedge ≝ vertex × Register. 513 axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge. 514 *) 544 axiom ig_phpick: graph → (ig_phedge → bool) → option ig_phedge. 
src/ERTL/build.ma
r1228 r1229 1 1 include "ERTL/liveness.ma". 2 2 (* include "utilities/Interference.ma". *) 3 4 definition vertex ≝ register ⊎ Register.5 6 record graph: Type[0] ≝7 {8 interferes: vertex → vertex → bool9 }.10 11 axiom build: ∀globals: list ident. ertl_internal_function globals → graph.12 13 inductive decision: Type[0] ≝14  decision_spill: decision15  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 v222 }.23 24 definition initial_colouring ≝ coloured_graph decision.25 definition stack_colouring ≝ coloured_graph nat.26 3 27 4 (* 
src/ERTL/spill.ma
r1128 r1229 1 1 include "common/AST.ma". 2 include " utilities/Interference.ma".2 include "ERTL/Interference.ma". 3 3 4 4 definition decision ≝ Immediate.
Note: See TracChangeset
for help on using the changeset viewer.