Changeset 2182 for src/ERTL


Ignore:
Timestamp:
Jul 13, 2012, 11:20:36 AM (8 years ago)
Author:
tranquil
Message:

updated linearisation pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness_paolo.ma

    r2174 r2182  
    33include "utilities/adt/set_adt.ma".
    44include "utilities/fixpoints.ma".
    5 
    6 (* maybe move? *)
    7 definition stmt_successors :
    8   ∀p : graph_params.∀globals.joint_statement p globals → list label ≝
    9   λp,g,s.match s with
    10   [ sequential seq l ⇒
    11     (match seq with
    12      [ COND _ lbl_true ⇒ [ lbl_true ]
    13      | _ ⇒ [ ]
    14      ]) @ [ l ]
    15   | final fin ⇒
    16     match fin with
    17     [ GOTO l ⇒ [ l ]
    18     | _ ⇒ [ ]
    19     ]
    20   ].
    215
    226definition register_lattice : property_lattice ≝
     
    268252  [ None      ⇒ rl_bottom
    269253  | Some stmt ⇒
    270     \fold[rl_join,rl_bottom]_{successor ∈ stmt_successors … stmt}
     254    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
    271255      (livebefore globals int_fun successor liveafter)
    272256  ].
Note: See TracChangeset for help on using the changeset viewer.