Changeset 3579 for LTS/variable.ma


Ignore:
Timestamp:
Jul 10, 2015, 4:08:09 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable.ma

    r3577 r3579  
    156156match \fst env with
    157157[ nil ⇒ None ?
    158 | cons hd tl ⇒ ! x ← (assign_frame hd v (\fst (\snd env)) n); return ((〈x::tl,\snd env〉))
     158| cons hd tl ⇒ ! x ← (assign_frame hd (to_shift + v) (\fst (\snd env)) n); return ((〈x::tl,\snd env〉))
    159159].
    160160
     
    165165   [sAss v e ⇒ !env ← frame_current_env … s;
    166166               ! n ← frame_sem_expr env e;
    167                frame_assign_var s v n
     167               frame_assign_var s (to_shift + v) n
    168168   ]
    169 | PopReg v ⇒ frame_assign_var s v (\snd (\snd s))
     169| PopReg v ⇒ frame_assign_var s (to_shift + v) (\snd (\snd s))
    170170].
    171171
     
    204204].
    205205 
    206 definition frame_init_store: frame_store_t≝ 〈[(nil ?)],〈O,O〉〉.
    207 
    208 
    209 definition frame_sem_state_params : sem_state_params frame_state_params ≝ mk_sem_state_params frame_state_params frame_eval_seq frame_eval_io
    210 frame_eval_cond_cond frame_eval_loop_cond frame_eval_call frame_return_call frame_init_store.
     206definition frame_init_store: ℕ → frame_store_t≝ λn.〈[list_n … O (to_shift + n)],〈O,O〉〉.
     207
     208
     209definition frame_sem_state_params : ℕ → sem_state_params frame_state_params ≝
     210λn.mk_sem_state_params frame_state_params frame_eval_seq frame_eval_io
     211frame_eval_cond_cond frame_eval_loop_cond frame_eval_call frame_return_call (frame_init_store n).
    211212
    212213  (* Abitare tipo Instructions *)
Note: See TracChangeset for help on using the changeset viewer.