Changeset 2823 for src/joint/Joint.ma


Ignore:
Timestamp:
Mar 8, 2013, 3:51:18 PM (7 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/Joint.ma

    r2808 r2823  
    479479    (that are already on stack in the front end) *)
    480480  joint_if_code     : codeT p globals ;
    481   joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) (*;
     481  joint_if_entry : code_point p (* Paolo: condition entry ∈ code is ensured by good_if ;
    482482  joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *)
    483483}.
     
    523523          Some … (sequential … (COST_LABEL … l) nxt)
    524524; entry_unused :
    525   let entry ≝ pi1 … (joint_if_entry … def) in
     525  let entry ≝ joint_if_entry … def in
    526526  let code ≝ joint_if_code … def in
    527527  forall_statements_i …
     
    555555       (joint_if_local_stacksize … int_fun)
    556556      graph entry (*exit*).
    557 
    558 definition set_joint_if_graph ≝
    559   λglobals.λpars : graph_params.
    560   λgraph.
    561   λp:joint_internal_function pars globals.
    562   λentry_prf.
    563   (*λexit_prf.*)
    564     set_joint_code globals pars p
    565       graph
    566       (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
    567       (*(mk_Sig … (joint_if_exit ?? p) exit_prf)*).
    568557
    569558definition set_luniverse ≝
     
    594583     (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
    595584     code
    596      (pi1 … (joint_if_entry … p))
     585     (joint_if_entry … p)
    597586     (*(pi1 … (joint_if_exit … p))*).
    598 >graph_code_has_point whd in match code; >mem_set_add
    599 @orb_Prop_r elim (joint_if_entry ???)
    600 #x #H <graph_code_has_point @H
    601 qed.
    602587
    603588definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
Note: See TracChangeset for help on using the changeset viewer.