Ignore:
Timestamp:
Jul 19, 2012, 2:42:02 PM (8 years ago)
Author:
tranquil
Message:
  • changed order of parameters of joint_internal_function and genv in semantics
  • in semantics, unified more_sem_unserialized_params and more_sem_genv_params
  • renamed all <language>_params to <LANGUAGE>
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness_paolo.ma

    r2208 r2214  
     1
    12include "ASM/Util.ma".
    23include "ERTL/ERTL_paolo.ma".
     
    4243definition defined ≝
    4344  λglobals: list ident.
    44   λs: joint_statement ertl_params globals.
     45  λs: joint_statement ERTL globals.
    4546  match s with
    4647  [ sequential seq l ⇒
     
    100101definition used ≝
    101102  λglobals: list ident.
    102   λs: joint_statement ertl_params globals.
     103  λs: joint_statement ERTL globals.
    103104  match s with
    104105  [ sequential seq l ⇒
     
    155156  λglobals: list ident.
    156157  λl: register_lattice.
    157   λs: joint_statement ertl_params globals.
     158  λs: joint_statement ERTL globals.
    158159  let pliveafter ≝ \fst l in
    159160  let hliveafter ≝ \snd l in
     
    225226
    226227definition statement_semantics: ∀globals: list ident.
    227   joint_statement ertl_params globals → register_lattice → register_lattice ≝
     228  joint_statement ERTL globals → register_lattice → register_lattice ≝
    228229  λglobals.
    229230  λstmt.
     
    236237definition livebefore ≝
    237238  λglobals: list ident.
    238   λint_fun: joint_internal_function globals ertl_params.
     239  λint_fun: joint_internal_function ERTL globals.
    239240  λlabel.
    240241  λliveafter: valuation register_lattice.
     
    246247definition liveafter ≝
    247248   λglobals: list ident.
    248   λint_fun: joint_internal_function globals ertl_params.
     249  λint_fun: joint_internal_function ERTL globals.
    249250  λlabel.
    250251  λliveafter: valuation register_lattice.
Note: See TracChangeset for help on using the changeset viewer.