Ignore:
Timestamp:
Aug 24, 2011, 5:12:10 PM (9 years ago)
Author:
campbell
Message:

Update branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma

    r1098 r1109  
    1 
     1include "utilities/Fix.ma".
    22include "ASM/Util.ma".
    33include "ERTL/ERTL.ma".
     
    3131    foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).
    3232
    33 definition list_set_member ≝
    34   λA: Type[0].
    35   λeq_a: A → A → bool.
    36   λa: A.
    37   λl: list A.
    38     member A eq_a a l.
     33definition list_set_member ≝ member.
     34
     35definition list_set_fold ≝ foldr.
    3936
    4037definition statement_successors ≝
     
    303300    | Some stmt ⇒ statement_semantics stmt (liveafter label)
    304301    ]
     302  in
     303  let liveafter ≝ λlabel. λliveafter: valuation.
     304    match lookup ? ? (ertl_if_graph int_fun) label with
     305    [ None      ⇒ ?
     306    | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
     307        lattice_join (livebefore successor liveafter) accu)
     308        lattice_bottom (statement_successors stmt)
     309    ]
    305310  in ?.
Note: See TracChangeset for help on using the changeset viewer.