Changeset 1471 for src/joint/Joint.ma


Ignore:
Timestamp:
Oct 28, 2011, 3:05:07 PM (9 years ago)
Author:
mulligan
Message:

finished erasure and generalised so as to work on arbitrary joint programs

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1380 r1471  
    117117    (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
    118118
     119definition set_joint_code ≝
     120  λglobals: list ident.
     121  λpars: params globals.
     122  λint_fun: joint_internal_function globals pars.
     123  λgraph: codeT … pars.
     124  λentry.
     125  λexit.
     126    mk_joint_internal_function globals pars
     127      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
     128      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
     129      graph entry exit.
     130
    119131definition set_joint_if_graph ≝
    120132  λglobals,pars.
     
    123135  λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
    124136  λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
    125    mk_joint_internal_function globals pars
    126     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    127     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    128     graph (dp … (joint_if_entry … p) entry_prf) (dp … (joint_if_exit … p) exit_prf).
     137    set_joint_code globals pars p graph
     138      (dp … (joint_if_entry … p) entry_prf) (dp … (joint_if_exit … p) exit_prf).
    129139
    130140definition set_luniverse ≝
Note: See TracChangeset for help on using the changeset viewer.