Changeset 3575 for LTS/stack.ma


Ignore:
Timestamp:
Jun 19, 2015, 12:00:22 AM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/stack.ma

    r3570 r3575  
    8080qed.
    8181 
    82 definition stack_instr_params ≝ mk_instr_params DeqStackSeq (mk_DeqSet io_i io_i_eq io_i_eq_equality)
    83  (mk_DeqSet unit (λ_.λ_.true) ?) (DeqSet_List DeqGuardCombinator) (mk_DeqSet unit (λ_.λ_.true) ?) (mk_DeqSet unit (λ_.λ_.true) ?).
    84 @hide_prf ** % // qed.
     82definition stack_instr_params ≝ mk_instr_params DeqStackSeq DeqFalse
     83 DeqUnit (DeqSet_List DeqGuardCombinator) DeqUnit DeqUnit.
    8584
    8685definition stack_env_params ≝ mk_env_params ℕ.
     
    8988mk_state_params stack_instr_params stack_env_params flat_labels frame_store_t (*DeqEnv*).
    9089
    91 definition push : (store_type stack_state_params) → DeqNat → option (store_type stack_state_params)
     90definition push : frame_store_t → DeqNat → option frame_store_t
    9291λs,n.match \fst s with
    9392[nil ⇒ None ?
     
    9594].
    9695
    97 definition pop : (store_type stack_state_params) → option (DeqNat × (store_type stack_state_params)) ≝
     96definition pop : frame_store_t → option (DeqNat × frame_store_t) ≝
    9897λs.match \fst s with
    9998[nil ⇒ None ?
     
    104103             ].
    105104
    106 definition eval_combinators : guard_combinators → (store_type stack_state_params)→ option (store_type stack_state_params)
     105definition eval_combinators : guard_combinators → frame_store_t→ option frame_store_t
    107106λc,s.match c with
    108107[ push_var x ⇒ ! curr_env ← frame_current_env s;
     
    117116
    118117
    119 definition stack_eval_seq: (seq_instr stack_state_params)→(store_type stack_state_params)→ option (store_type stack_state_params)
     118definition stack_eval_seq: stack_seq→frame_store_t→ option frame_store_t
    120119λi,s.match i with
    121120[ pop_Ass v ⇒ ! 〈val1,st1〉 ← pop s;frame_assign_var st1 (to_shift +v) val1
     
    125124
    126125definition stack_eval_cond_cond:
    127 (list guard_combinators) → (store_type stack_state_params)→ option (bool × (store_type stack_state_params))≝
     126(list guard_combinators) → frame_store_t→ option (bool × frame_store_t)≝
    128127λl,st.! fin_St ← m_fold Option … eval_combinators l st;
    129128      !〈val,st2〉← pop fin_St;
     
    137136].
    138137
    139 definition stack_eval_call:(signature stack_state_params stack_state_params)→ act_params_type stack_state_params →
     138definition stack_signature≝signature stack_state_params stack_state_params.
     139
     140definition stack_eval_call:stack_signature→
    140141frame_store_t → (option frame_store_t)≝
    141 λsgn.λvar,st.
     142λsgn.λst.
    142143    !〈n,st1〉 ← pop st; 
    143144    frame_assign_var 〈(list_n … O (pred (to_shift + (f_pars … sgn))))::(\fst st1),(\snd st1)〉 to_shift n.
     
    155156definition stack_sem_state_params : ℕ → sem_state_params stack_state_params ≝
    156157λn.mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io
    157 (λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond stack_eval_call (λ_.stack_return_call) (stack_init_store n).
     158(λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond (λsgn.λ_.stack_eval_call sgn) (λ_.stack_return_call) (stack_init_store n).
    158159
    159160  (* Abitare tipo Instructions *)
     
    161162definition stack_Instructions≝Instructions stack_state_params flat_labels.
    162163
    163 definition stack_signature≝signature stack_state_params stack_state_params.
    164 
    165164
    166165definition stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels).
Note: See TracChangeset for help on using the changeset viewer.