Changeset 2700 for src/ERTLptr


Ignore:
Timestamp:
Feb 22, 2013, 2:12:24 PM (8 years ago)
Author:
sacerdot
Message:
  1. exponential function dropped in favour of standard library
  2. fixpoint computation and graph colouring abstracted in the back-end, axiomatized in the compiler
  3. minor speedups in Policy.ma
Location:
src/ERTLptr
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2697 r2700  
    418418  ]〉).
    419419
    420 definition translate_data : ∀globals.
     420definition translate_data :
     421 fixpoint_computer → coloured_graph_computer →
     422 ∀globals.
    421423  joint_closed_internal_function ERTLptr globals →
    422424  bind_new register (b_graph_translate_data ERTLptr LTL globals) ≝
    423 λglobals,int_fun.
     425λthe_fixpoint,build,globals,int_fun.
    424426(* colour registers *)
    425 let after ≝ analyse_liveness globals int_fun in
     427let after ≝ analyse_liveness the_fixpoint globals int_fun in
    426428let coloured_graph ≝ build after in
    427429(* compute new stack size *)
     
    441443qed.
    442444
    443 definition ertlptr_to_ltl: ertlptr_program → ltl_program ≝
    444   b_graph_transform_program … translate_data.
     445definition ertlptr_to_ltl:
     446 fixpoint_computer → coloured_graph_computer → ertlptr_program → ltl_program ≝
     447  λthe_fixpoint,build.
     448   b_graph_transform_program … (translate_data the_fixpoint build).
  • src/ERTLptr/Interference.ma

    r2693 r2700  
    1919}.
    2020
    21 axiom build: ∀valuation. coloured_graph valuation.
     21definition coloured_graph_computer ≝ ∀valuation. coloured_graph valuation.
  • src/ERTLptr/liveness.ma

    r2693 r2700  
    279279
    280280definition analyse_liveness ≝
    281   λglobals.
    282   λint_fun.
    283     the_fixpoint ? (liveafter globals int_fun).
     281  λthe_fixpoint: fixpoint_computer. λglobals,int_fun.
     282   the_fixpoint ? (liveafter globals int_fun).
    284283
    285284definition vertex ≝ register + Register.
Note: See TracChangeset for help on using the changeset viewer.