Ignore:
Timestamp:
Mar 8, 2013, 3:51:18 PM (8 years ago)
Author:
tranquil
Message:
  • corrected bug in ERTL semantics (both delframe and newframe did the same operation on the stack pointer...)
  • split RTL semantics in two (one with multiple stack spaces per call, one with only one for all)
  • joint_if_entry is not required anymore to be in the code (as it is covered by entry_costed in good_if)
  • temporarily replaced the two biggest proofs of linearise by daemons
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2808 r2823  
    237237    ] n_prf
    238238  ] (chop_ok ? (λx.x∈visited) visiting).
    239 (* cases daemon *)
     239cases daemon (*)
    240240whd
    241241[ (* base case, visiting is all visited *)
     
    518518|
    519519]
    520 (**)
     520*)
    521521qed.
    522522
     
    705705| >commutative_plus change with (? ≤ |g|) %
    706706]
    707 (* cases daemon *)
     707cases daemon (*)
    708708**
    709709#visited #required #generated normalize nodelta ****
     
    813813  ]
    814814]
    815 (**)
     815*)
    816816qed.
    817817
     
    846846  let code ≝ \fst code_sigma in
    847847  let sigma ≝ \snd code_sigma in
    848   let entry : Σpt.bool_to_Prop (code_has_point … code pt) ≝ «0, hide_prf ??» in
    849848  «〈«mk_joint_internal_function (mk_lin_params p) globals
    850849   (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig)
    851850   (joint_if_result ?? f_sig) (joint_if_params ?? f_sig)
    852851   (joint_if_stacksize ?? f_sig) (joint_if_local_stacksize ?? f_sig)
    853    code entry (* exit is dummy! *), hide_prf ??»,
     852   code 0 (* exit is dummy! *), hide_prf ??»,
    854853   sigma〉, proj1 ?? (pi2 ?? code_sigma)».
     854cases daemon (*)
    855855[2: whd in match code; cases code_sigma -code_sigma * #code #sigma
    856856  normalize nodelta *** #H3 #H4 #H5
     
    877877  ]
    878878]
     879*)
    879880qed.
    880881
Note: See TracChangeset for help on using the changeset viewer.