Changeset 2843 for src/joint/Joint.ma


Ignore:
Timestamp:
Mar 11, 2013, 1:02:02 PM (8 years ago)
Author:
piccolo
Message:

1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2824 r2843  
    190190match step with
    191191[ COST_LABEL c ⇒ [ ]
    192 | CALL id args dest ⇒ (f_call_args … functs args) @ (f_call_dest … functs dest)
     192| CALL id args dest ⇒
     193     let r_id ≝  match id with
     194                   [ inl _ ⇒ [ ]
     195                   | inr ptr ⇒ ((dpl_args … functs) (\fst ptr)) @
     196                                                 ((dph_args … functs) (\snd ptr))
     197                   ] in
     198    r_id @ (f_call_args … functs args) @ (f_call_dest … functs dest)
    193199| COND r lbl ⇒  acc_a_regs … functs r
    194200| step_seq s ⇒ get_used_registers_from_seq … functs s
Note: See TracChangeset for help on using the changeset viewer.