Changeset 2689 for src/RTL


Ignore:
Timestamp:
Feb 21, 2013, 7:23:17 PM (8 years ago)
Author:
tranquil
Message:
  • fixed passes up to linearisation
File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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 % [%]
Note: See TracChangeset for help on using the changeset viewer.