Ignore:
Timestamp:
Mar 7, 2013, 6:03:18 PM (8 years ago)
Author:
tranquil
Message:

added local_stacksize to joint internal functions to accomodate for locals in the stack inherited from the front end

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2784 r2808  
    237237    ] n_prf
    238238  ] (chop_ok ? (λx.x∈visited) visiting).
     239(* cases daemon *)
    239240whd
    240241[ (* base case, visiting is all visited *)
     
    517518|
    518519]
     520(**)
    519521qed.
    520522
     
    703705| >commutative_plus change with (? ≤ |g|) %
    704706]
     707(* cases daemon *)
    705708**
    706709#visited #required #generated normalize nodelta ****
     
    810813  ]
    811814]
     815(**)
    812816qed.
    813817
     
    846850   (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig)
    847851   (joint_if_result ?? f_sig) (joint_if_params ?? f_sig)
    848    (joint_if_stacksize ?? f_sig) code entry (* exit is dummy! *), hide_prf ??»,
     852   (joint_if_stacksize ?? f_sig) (joint_if_local_stacksize ?? f_sig)
     853   code entry (* exit is dummy! *), hide_prf ??»,
    849854   sigma〉, proj1 ?? (pi2 ?? code_sigma)».
    850855[2: whd in match code; cases code_sigma -code_sigma * #code #sigma
Note: See TracChangeset for help on using the changeset viewer.