Changeset 3572
- Timestamp:
- Jun 17, 2015, 6:42:45 PM (6 years ago)
- Location:
- LTS
- Files:
-
- 1 added
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/mono_stack.ma
r3570 r3572 15 15 include "stack.ma". 16 16 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 21 17 definition mono_stack_store_t ≝ DeqProd (DeqSet_List DeqNat) (DeqProd DeqNat DeqNat). 22 18 23 19 definition mono_stack_state_params:state_params≝ 24 mk_state_params mono_stack_instr_params stack_env_params flat_labels mono_stack_store_t (*DeqEnv*).20 mk_state_params stack_instr_params stack_env_params flat_labels mono_stack_store_t (*DeqEnv*). 25 21 26 22 definition mono_push : mono_stack_store_t → DeqNat → mono_stack_store_t ≝ … … 44 40 | push_not ⇒ ! 〈val1,st1〉 ← mono_pop s;return mono_push st1 (1-val1) 45 41 ]. 46 47 check assign_frame48 42 49 43 definition mono_stack_eval_seq: (seq_instr mono_stack_state_params)→ … … 103 97 ! new_fp ← read_frame (\fst st1) (\fst (\snd s)) O; (* 0 leggi il frame pointer precedente *) 104 98 ! 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 *) 107 100 108 101 definition mono_stack_init_store ≝ λn : ℕ.〈list_n … O (to_shift + n),〈O,O〉〉. … … 120 113 121 114 122 definition mono_stack_envitem≝ (env_item stack_env_params mono_stack_instr_params flat_labels).115 definition mono_stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels).
Note: See TracChangeset
for help on using the changeset viewer.