Changeset 3577 for LTS/variable.ma


Ignore:
Timestamp:
Jun 19, 2015, 6:31:59 PM (4 years ago)
Author:
sacerdot
Message:

Number of local variables computed during the first pass and then propagated.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable.ma

    r3575 r3577  
    119119definition frame_store_t≝ DeqProd (DeqSet_List activation_frame) (DeqProd DeqNat DeqNat). (*frame_pointer e return register*)
    120120
    121 definition frame_env_params ≝ mk_env_params unit.
     121definition frame_env_params ≝ mk_env_params .
    122122
    123123inductive frame_seq_i : Type[0] ≝
     
    185185definition frame_signature≝signature frame_state_params frame_state_params.
    186186
     187let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝
     188match n with
     189[ O ⇒ nil ?
     190| S m ⇒ a :: list_n … a m
     191].
     192
    187193definition frame_eval_call:frame_signature→ expr → frame_store_t → (option frame_store_t)≝
    188194λsgn,e,st.
    189195    !env ← frame_current_env … st;
    190196    !n ← frame_sem_expr env e;
    191     frame_assign_var 〈((nil ?)::(\fst st)),(\snd st)〉 to_shift n.
     197    frame_assign_var 〈((list_n … O (pred (to_shift + (f_pars … sgn))))::(\fst st)),(\snd st)〉 to_shift n.
    192198
    193199definition frame_return_call:expr→ frame_store_t→ (option frame_store_t)≝
Note: See TracChangeset for help on using the changeset viewer.