Changeset 3566 for LTS/stack.ma


Ignore:
Timestamp:
Jun 17, 2015, 4:23:08 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/stack.ma

    r3565 r3566  
    8181@hide_prf ** % // qed.
    8282
     83definition stack_env_params ≝ mk_env_params ℕ.
     84
    8385definition stack_state_params:state_params≝
    84 mk_state_params stack_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
     86mk_state_params stack_instr_params stack_env_params flat_labels frame_store_t (*DeqEnv*).
    8587
    8688definition push : (store_type stack_state_params) → DeqNat → option (store_type stack_state_params) ≝
     
    125127
    126128
     129let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝
     130match n with
     131[ O ⇒ nil ?
     132| S m ⇒ a :: list_n … a m
     133].
     134
    127135definition stack_eval_call:(signature stack_state_params stack_state_params)→ act_params_type stack_state_params →
    128136frame_store_t → (option frame_store_t)≝
    129 λsgn,var,st.
    130   match sgn with
    131   [ mk_signature fun fpt rt ⇒
    132     !〈n,st1〉 ← pop st;
    133     frame_assign_var 〈(〈(nil ?),var〉::(\fst st1)),(\snd st1)〉 O n
    134   ].
     137λsgn.λvar,st.
     138    !〈n,st1〉 ← pop st; 
     139    frame_assign_var 〈(〈list_n … O (pred (to_shift + (f_pars … sgn))),var〉::(\fst st1)),(\snd st1)〉 to_shift n.
    135140
    136141definition stack_return_call:frame_store_t→ (option frame_store_t)≝
     
    142147].
    143148 
     149definition stack_init_store ≝ λn : ℕ.〈[〈list_n … O (to_shift + n),O〉],〈O,O〉〉.
    144150
    145151
    146 definition stack_sem_state_params : sem_state_params stack_state_params ≝ mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io
    147 (λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond stack_eval_call (λ_.stack_return_call) frame_init_store.
     152definition stack_sem_state_params : ℕ → sem_state_params stack_state_params ≝
     153λn.mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io
     154(λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond stack_eval_call (λ_.stack_return_call) (stack_init_store n).
    148155
    149156  (* Abitare tipo Instructions *)
     
    154161
    155162
    156 definition stack_envitem≝ (env_item frame_env_params stack_instr_params flat_labels).
     163definition stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels).
Note: See TracChangeset for help on using the changeset viewer.