Changeset 1245 for src/joint


Ignore:
Timestamp:
Sep 21, 2011, 10:22:13 PM (9 years ago)
Author:
sacerdot
Message:

RTLtoERTL and LINToASM: porting to new Joint data type in progress.
However, it seems better to go back to a Joint representation where
the "mapping" from label to internal functions is more concrete.
To be done.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1236 r1245  
    6565}.
    6666
     67(* Currified form *)
     68definition set_joint_if_exit ≝
     69  λpars,globals.
     70  λexit: label.
     71  λp: joint_internal_function pars globals.
     72  λprf: joint_if_lookup … p exit ≠ None ?.
     73   mk_joint_internal_function pars globals
     74    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     75    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     76    (joint_if_lookup … p) (joint_if_entry … p) (dp … exit prf).
     77
     78
    6779definition set_luniverse ≝
    6880  λp:params.
Note: See TracChangeset for help on using the changeset viewer.