Changeset 2595 for src/joint/Joint.ma


Ignore:
Timestamp:
Jan 30, 2013, 7:25:39 PM (8 years ago)
Author:
tranquil
Message:
  • dropped locals and exit from definition of joint_if_function
  • new definition of blocks to accomodate ERTLptr pass
  • stated properties of translation as axioms
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2562 r2595  
    8888 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
    8989 ; paramsT : Type[0]
    90  ; localsT: Type[0]
    9190 }.
    9291
     
    409408  joint_if_result   : call_dest p;
    410409  joint_if_params   : paramsT p;
    411   joint_if_locals   : list (localsT p); (* use void where no locals are present *)
    412410(*CSC: XXXXX stacksize unused for LTL-...*)
    413411  joint_if_stacksize: nat;
    414412  joint_if_code     : codeT p globals ;
    415   joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) ;
    416   joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt)
     413  joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) (*;
     414  joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *)
    417415}.
    418416
     
    431429  λgraph: codeT pars globals.
    432430  λentry.
    433   λexit.
     431  (*λexit.*)
    434432    mk_joint_internal_function pars globals
    435433      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
    436       (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
    437       graph entry exit.
     434      (joint_if_params … int_fun) (joint_if_stacksize … int_fun)
     435      graph entry (*exit*).
    438436
    439437definition set_joint_if_graph ≝
     
    442440  λp:joint_internal_function pars globals.
    443441  λentry_prf.
    444   λexit_prf.
     442  (*λexit_prf.*)
    445443    set_joint_code globals pars p
    446444      graph
    447445      (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
    448       (mk_Sig … (joint_if_exit ?? p) exit_prf).
     446      (*(mk_Sig … (joint_if_exit ?? p) exit_prf)*).
    449447
    450448definition set_luniverse ≝
     
    454452   mk_joint_internal_function globals pars
    455453    luniverse (joint_if_runiverse … p) (joint_if_result … p)
    456     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    457     (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
     454    (joint_if_params … p) (joint_if_stacksize … p)
     455    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
    458456
    459457definition set_runiverse ≝
     
    463461   mk_joint_internal_function globals pars
    464462    (joint_if_luniverse … p) runiverse (joint_if_result … p)
    465     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    466     (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
     463    (joint_if_params … p) (joint_if_stacksize … p)
     464    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
    467465   
    468466(* Specialized for graph_params *)
     
    473471    mk_joint_internal_function …
    474472     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    475      (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     473     (joint_if_params … p) (joint_if_stacksize … p)
    476474     code
    477475     (pi1 … (joint_if_entry … p))
    478      (pi1 … (joint_if_exit … p)).
     476     (*(pi1 … (joint_if_exit … p))*).
    479477>graph_code_has_point whd in match code; >mem_set_add
    480 @orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ]
     478@orb_Prop_r elim (joint_if_entry ???)
    481479#x #H <graph_code_has_point @H
    482480qed.
    483481
    484 definition set_locals ≝
    485   λpars,globals.
    486   λp : joint_internal_function pars globals.
    487   λlocals.
    488    mk_joint_internal_function pars globals
    489     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    490     (joint_if_params … p) locals (joint_if_stacksize … p)
    491     (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
    492 
    493482definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
    494483
Note: See TracChangeset for help on using the changeset viewer.