Changeset 2689


Ignore:
Timestamp:
Feb 21, 2013, 7:23:17 PM (6 years ago)
Author:
tranquil
Message:
  • fixed passes up to linearisation
Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r2681 r2689  
    314314    match s' return λ_.step_block LTL globals with
    315315    [ COMMENT c ⇒ [COMMENT … c]
    316     | COST_LABEL cost_lbl ⇒ [COST_LABEL … cost_lbl]
    317316    | POP r ⇒
    318317      POP … A ::
     
    369368      ]
    370369    ]
     370  | COST_LABEL cost_lbl ⇒ 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉
    371371  | COND r ltrue ⇒
    372372    〈add_dummy_variance … (move RegisterA (lookup r)),λ_.COND … it ltrue, [ ]〉
  • src/ERTL/liveness.ma

    r2681 r2689  
    6868      | COMMENT c ⇒ rl_bottom
    6969      | STORE acc_a dpl dph ⇒ rl_bottom
    70       | COST_LABEL clabel ⇒ rl_bottom
    7170      | PUSH r ⇒ rl_bottom
    7271      | MOVE pair_reg ⇒
     
    8685    | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    8786    | COND r lbl_true ⇒ rl_bottom
     87    | COST_LABEL clabel ⇒ rl_bottom
    8888    ]
    8989  | final _ ⇒ rl_bottom
     
    141141      | _ ⇒ rl_bottom
    142142      ]
     143    | COST_LABEL clabel ⇒ rl_bottom
    143144    | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    144145    | COND r lbl_true ⇒ rl_psingleton r
  • src/RTL/RTLToERTL.ma

    r2681 r2689  
    225225    | POP _ ⇒ bret … [ ] (*CSC: XXXX should not be in the syntax *)
    226226    | MOVE rs ⇒ bret … [PSD (\fst rs) ← \snd rs]
    227     | COST_LABEL lbl ⇒
    228       bret … [COST_LABEL … lbl]
    229227    | ADDRESS x prf r1 r2 ⇒
    230228      bret … [ADDRESS ERTL ? x prf r1 r2]
     
    251249      ]
    252250    ]
     251  | COST_LABEL lbl ⇒
     252    bret … 〈[ ], λ_.COST_LABEL ERTL ? lbl, [ ]〉
    253253  | CALL f args ret_regs ⇒
    254254    ! pref ← pi1 … (set_params ? args) ;
     
    309309| whd %{I} cases (epilogue ?????) @All_mp #s #EQ whd >EQ %
    310310| *
     311| #c %{I} %{I} #l %
    311312| #called #args #dest @(mp_bind … (BindNewP …))
    312313  [2: @(pi2 ? (λ_.?)) |*:] #l1 #H1 whd % [%]
  • src/RTLabs/RTLabsToRTL.ma

    r2674 r2689  
    960960    ❬inl … (bret … [ ]), lbl'❭
    961961  | St_cost cost_lbl lbl' ⇒ λstmt_typed.
    962     ❬inl … (bret … [COST_LABEL … cost_lbl]), lbl'❭
     962    ❬inl … (bret … 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉), lbl'❭
    963963  | St_const ty destr cst lbl' ⇒ λstmt_typed.
    964964    ❬inl … (translate_cst ty globals cst (find_local_env destr lenv ?) ?), lbl'❭
Note: See TracChangeset for help on using the changeset viewer.