Changeset 3572 for LTS


Ignore:
Timestamp:
Jun 17, 2015, 6:42:45 PM (4 years ago)
Author:
piccolo
Message:

pass stack to mono stack in place

Location:
LTS
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/mono_stack.ma

    r3570 r3572  
    1515include "stack.ma".
    1616
    17 definition mono_stack_instr_params ≝ mk_instr_params DeqStackSeq (mk_DeqSet io_i io_i_eq io_i_eq_equality)
    18  (mk_DeqSet unit (λ_.λ_.true) ?) (DeqSet_List DeqGuardCombinator) (mk_DeqSet unit (λ_.λ_.true) ?) (mk_DeqSet unit (λ_.λ_.true) ?).
    19 @hide_prf ** % // qed.
    20 
    2117definition mono_stack_store_t ≝ DeqProd (DeqSet_List DeqNat) (DeqProd DeqNat DeqNat).
    2218
    2319definition mono_stack_state_params:state_params≝
    24 mk_state_params mono_stack_instr_params stack_env_params flat_labels mono_stack_store_t (*DeqEnv*).
     20mk_state_params stack_instr_params stack_env_params flat_labels mono_stack_store_t (*DeqEnv*).
    2521
    2622definition mono_push : mono_stack_store_t → DeqNat → mono_stack_store_t ≝
     
    4440| push_not ⇒ ! 〈val1,st1〉 ← mono_pop s;return mono_push st1 (1-val1)
    4541].
    46 
    47 check assign_frame
    4842
    4943definition mono_stack_eval_seq: (seq_instr mono_stack_state_params)→
     
    10397   ! new_fp ← read_frame (\fst st1) (\fst (\snd s)) O; (* 0 leggi il frame pointer precedente *)
    10498   ! st2 ← mono_pop_frame st1 (\fst (\snd s)) ;(* 1: accorciare la lista fino a diventare lunga come \snd st1 ovvero il frame pointer corrente *)
    105    let st3 ≝  mono_push st2 n in (* 2: pushare il valore n *)
    106    return 〈(\fst st3),〈new_fp,(\snd(\snd s))〉〉. (* 3: ritornare lo stato con il nuovo fp *)
     99   return 〈(\fst st2),〈new_fp,n〉〉. (* 3: ritornare lo stato con il nuovo fp *)
    107100
    108101definition mono_stack_init_store ≝ λn : ℕ.〈list_n … O  (to_shift + n),〈O,O〉〉.
     
    120113
    121114
    122 definition mono_stack_envitem≝ (env_item stack_env_params mono_stack_instr_params flat_labels).
     115definition mono_stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels).
Note: See TracChangeset for help on using the changeset viewer.