Changeset 1601 for src/joint


Ignore:
Timestamp:
Dec 13, 2011, 2:49:52 PM (8 years ago)
Author:
sacerdot
Message:

Files ported to new version of the standard library.

Location:
src/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEValues.ma

    r1516 r1601  
    33
    44include "common/Pointers.ma".
    5 include "utilities/sigma.ma".
    65
    76record part (r: region): Type[0] ≝
     
    121120  do p ← pointer_of_bevals [v1;v2] ;
    122121  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
    123   [ Code ⇒ λE.OK ? (inject … p ?)
     122  [ Code ⇒ λE.OK ? (mk_Sig … p ?)
    124123  | _ ⇒ λ_.Error … [MSG NotACodePointer]] ?.
    125124// qed.
  • src/joint/Joint.ma

    r1471 r1601  
    33include "common/AST.ma".
    44include "common/Registers.ma".
    5 include "utilities/sigma.ma". (* CSC: Only for Sigma type projections *)
    65include "common/Graphs.ma".
    76
     
    115114    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    116115    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    117     (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
     116    (joint_if_code … p) (joint_if_entry … p) (mk_Sig … exit prf).
    118117
    119118definition set_joint_code ≝
     
    136135  λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
    137136    set_joint_code globals pars p graph
    138       (dp … (joint_if_entry … p) entry_prf) (dp … (joint_if_exit … p) exit_prf).
     137      (mk_Sig … (joint_if_entry … p) entry_prf) (mk_Sig … (joint_if_exit … p) exit_prf).
    139138
    140139definition set_luniverse ≝
  • src/joint/semantics.ma

    r1457 r1601  
    1 include "utilities/lists.ma".
     1include "basics/lists/list.ma".
    22include "joint/BEGlobalenvs.ma".
    33include "common/IO.ma".
Note: See TracChangeset for help on using the changeset viewer.