[3560] | 1 | (**************************************************************************) |
---|
| 2 | (* ___ *) |
---|
| 3 | (* ||M|| *) |
---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
---|
| 5 | (* ||T|| *) |
---|
| 6 | (* ||I|| Developers: *) |
---|
| 7 | (* ||T|| The HELM team. *) |
---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
| 9 | (* \ / *) |
---|
| 10 | (* \ / This file is distributed under the terms of the *) |
---|
| 11 | (* v GNU General Public License Version 2 *) |
---|
| 12 | (* *) |
---|
| 13 | (**************************************************************************) |
---|
| 14 | |
---|
| 15 | include "imp.ma". |
---|
| 16 | |
---|
[3561] | 17 | definition to_shift : ℕ ≝ 2. |
---|
[3560] | 18 | |
---|
| 19 | definition activation_frame ≝ DeqSet_List DeqNat. |
---|
| 20 | |
---|
[3571] | 21 | let rec update (A : Type[0]) (l : list A) (n : ℕ) (a : A) on l : option (list A) ≝ |
---|
[3560] | 22 | match l with |
---|
[3569] | 23 | [ nil ⇒ None ? |
---|
| 24 | | cons x xs ⇒ |
---|
| 25 | match n with |
---|
| 26 | [ O ⇒ return (a :: xs) |
---|
[3571] | 27 | | S m ⇒ !res ← update … xs m a; return (x::res) ]]. |
---|
[3560] | 28 | |
---|
[3569] | 29 | lemma nth_opt_update_hit: |
---|
[3571] | 30 | ∀A,n,env,a,env'. |
---|
| 31 | update A env a n = return env' → |
---|
[3569] | 32 | nth_opt … a env' = return n. |
---|
[3571] | 33 | #A #n #env elim env |
---|
[3569] | 34 | [ normalize #a #env' #abs destruct |
---|
| 35 | | #x #xs #IH #a #env' cases a |
---|
| 36 | [ normalize #EQ destruct // |
---|
| 37 | | #m #H change with (m_bind ????? = ?) in H; |
---|
| 38 | cases (bind_inversion ????? H) -H #l * #EQ1 #EQ2 normalize in EQ1 EQ2; destruct |
---|
| 39 | normalize @IH assumption ]] |
---|
| 40 | qed. |
---|
| 41 | |
---|
[3571] | 42 | lemma len_update: |
---|
| 43 | ∀A,env,n,a,env'. |
---|
| 44 | update A env n a = return env' → |
---|
| 45 | |env| = |env'|. |
---|
| 46 | #A #env elim env normalize |
---|
| 47 | [ #n #a #env' #abs destruct |
---|
| 48 | | #hd #tl #IH * normalize |
---|
| 49 | [ #a #env' #EQ destruct // |
---|
| 50 | | #m #a #env' change with (m_bind ????? = return ? → ?) #H |
---|
| 51 | cases (bind_inversion ????? H) #l * #EQ1 #EQ2 normalize in EQ1 EQ2; destruct |
---|
| 52 | @eq_f @(IH … EQ1) ]] |
---|
| 53 | qed. |
---|
[3560] | 54 | |
---|
[3571] | 55 | lemma nth_opt_update_miss: |
---|
| 56 | ∀A,n,env,a,a',env'. |
---|
| 57 | a ≠ a' → |
---|
| 58 | update A env a n = return env' → |
---|
| 59 | nth_opt … a' env' = nth_opt … a' env. |
---|
| 60 | #A #n #env elim env |
---|
| 61 | [ normalize #a #a' #env' #aa #abs destruct |
---|
| 62 | | #x #xs #IH #a #a' #env' cases a |
---|
| 63 | [ normalize cases a' [ * #ABS cases ABS // ] #a2 #aa #EQ destruct // |
---|
| 64 | | #m #aa #H change with (m_bind ????? = ?) in H; |
---|
| 65 | cases (bind_inversion ????? H) -H #l * #EQ1 #EQ2 normalize in EQ1 EQ2; destruct |
---|
| 66 | cases a' in aa; normalize // #m2 #DIFF @(IH … EQ1) /2 by not_to_not/ ]] |
---|
| 67 | qed. |
---|
| 68 | |
---|
| 69 | definition assign_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.λn:DeqNat.update … env (|env| - v - fp -1) n. |
---|
| 70 | |
---|
[3560] | 71 | definition read_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.nth_opt … (|env| -v -fp -1) env. |
---|
| 72 | |
---|
[3569] | 73 | lemma read_frame_assign_frame_hit: |
---|
[3573] | 74 | ∀env,v,fp,n,env'. |
---|
| 75 | assign_frame env v fp n = return env' → |
---|
| 76 | read_frame env' v fp = return n. |
---|
| 77 | normalize #env #v #fp #n #env' #H <(len_update ????? H) |
---|
| 78 | @(nth_opt_update_hit … H) |
---|
| 79 | qed. |
---|
[3569] | 80 | |
---|
[3573] | 81 | lemma read_frame_assign_frame_miss: |
---|
| 82 | ∀n,env,v,v',fp,env'. |
---|
| 83 | v + fp < |env| → |
---|
| 84 | v' + fp < |env| → |
---|
| 85 | v ≠ v' → |
---|
| 86 | assign_frame env v fp n = return env' → |
---|
| 87 | read_frame env' v' fp = read_frame env v' fp. |
---|
| 88 | normalize #n #env #v #v' #fp #env' #Hv #Hv' #H #H1 <(len_update ????? H1) |
---|
| 89 | @(nth_opt_update_miss ??????? H1) @(not_to_not … H) #K -H1 -H |
---|
| 90 | cases daemon (* |
---|
| 91 | >minus_plus in K; >minus_plus >minus_plus >minus_plus #K |
---|
| 92 | lapply (minus_to_plus … K) [ applyS Hv ] -K >plus_minus_associative |
---|
| 93 | [2: applyS Hv' ]*) |
---|
| 94 | qed. |
---|
| 95 | |
---|
[3560] | 96 | let rec frame_sem_expr (env:activation_frame) (e: expr) on e : (option nat) ≝ |
---|
| 97 | match e with |
---|
| 98 | [ Var v ⇒ read_frame env (to_shift+v) O |
---|
| 99 | | Const n ⇒ Some ? n |
---|
| 100 | | Plus e1 e2 ⇒ !n1 ← frame_sem_expr env e1; |
---|
| 101 | !n2 ← frame_sem_expr env e2; |
---|
| 102 | return (n1+n2) |
---|
| 103 | | Minus e1 e2 ⇒ !n1 ← frame_sem_expr env e1; |
---|
| 104 | !n2 ← frame_sem_expr env e2; |
---|
| 105 | return (n1-n2) |
---|
| 106 | ]. |
---|
| 107 | |
---|
| 108 | let rec frame_sem_condition (env:activation_frame) (c:condition) on c : option bool ≝ |
---|
| 109 | match c with |
---|
| 110 | [ Eq e1 e2 ⇒ !n ← frame_sem_expr env e1; |
---|
| 111 | !m ← frame_sem_expr env e2; |
---|
| 112 | return (eqb n m) |
---|
| 113 | | Not c ⇒ !b ← frame_sem_condition env c; |
---|
| 114 | return (notb b) |
---|
| 115 | ]. |
---|
| 116 | |
---|
| 117 | |
---|
| 118 | |
---|
[3566] | 119 | definition frame_store_t≝ DeqProd (DeqSet_List activation_frame) (DeqProd DeqNat DeqNat). (*frame_pointer e return register*) |
---|
[3560] | 120 | |
---|
[3577] | 121 | definition frame_env_params ≝ mk_env_params ℕ. |
---|
[3561] | 122 | |
---|
[3566] | 123 | inductive frame_seq_i : Type[0] ≝ |
---|
| 124 | | Seq_i : seq_i → frame_seq_i |
---|
| 125 | | PopReg : variable → frame_seq_i. |
---|
| 126 | |
---|
| 127 | definition eq_frame_seq_i : frame_seq_i → frame_seq_i → bool ≝ |
---|
| 128 | λx,y. |
---|
| 129 | match x with |
---|
| 130 | [ Seq_i s ⇒ match y with [Seq_i s' ⇒ seq_i_eq s s' | _ ⇒ false ] |
---|
| 131 | | PopReg v ⇒ match y with [PopReg v' ⇒ eqb v v' | _ ⇒ false] |
---|
| 132 | ]. |
---|
| 133 | |
---|
[3575] | 134 | lemma eq_frame_seq_i_elim : ∀P : bool → Prop.∀s1,s2.(s1 = s2 → P true) → (s1 ≠ s2 → P false) → |
---|
| 135 | P (eq_frame_seq_i s1 s2). |
---|
| 136 | #P * [ #i | #v] * [1,3: #i' |*: # v'] #H1 #H2 whd in match eq_frame_seq_i; normalize nodelta |
---|
| 137 | try(@H2 % #EQ destruct) |
---|
| 138 | [ @seq_i_eq_elim | @(eqb_elim v v') ] |
---|
| 139 | [1,3: #EQ destruct /2/ |*: * #H @H2 % #EQ destruct @H %] |
---|
| 140 | qed. |
---|
| 141 | |
---|
[3566] | 142 | definition DeqFrameSeqI ≝ mk_DeqSet frame_seq_i eq_frame_seq_i ?. |
---|
[3575] | 143 | @hide_prf #x #y @eq_frame_seq_i_elim |
---|
| 144 | [ #EQ destruct /2/ | * #H % #EQ destruct cases H % ] |
---|
| 145 | qed. |
---|
[3566] | 146 | |
---|
| 147 | definition frame_instr_params : instr_params ≝ |
---|
[3575] | 148 | mk_instr_params DeqFrameSeqI DeqFalse DeqCondition DeqCondition DeqExpr DeqExpr. |
---|
[3566] | 149 | |
---|
[3560] | 150 | definition frame_state_params:state_params≝ |
---|
[3566] | 151 | mk_state_params frame_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*). |
---|
[3560] | 152 | |
---|
[3575] | 153 | definition frame_current_env:frame_store_t→ option ?≝λs.!hd ← option_hd … (\fst s); return hd. |
---|
[3560] | 154 | |
---|
| 155 | definition frame_assign_var ≝ λenv:frame_store_t.λv:variable.λn:DeqNat. |
---|
| 156 | match \fst env with |
---|
| 157 | [ nil ⇒ None ? |
---|
[3579] | 158 | | cons hd tl ⇒ ! x ← (assign_frame hd (to_shift + v) (\fst (\snd env)) n); return ((〈x::tl,\snd env〉)) |
---|
[3560] | 159 | ]. |
---|
| 160 | |
---|
[3575] | 161 | definition frame_eval_seq:frame_seq_i →frame_store_t→ option frame_store_t≝ |
---|
[3560] | 162 | λi,s.match i with |
---|
[3566] | 163 | [ Seq_i instr ⇒ |
---|
| 164 | match instr with |
---|
[3575] | 165 | [sAss v e ⇒ !env ← frame_current_env … s; |
---|
[3566] | 166 | ! n ← frame_sem_expr env e; |
---|
[3579] | 167 | frame_assign_var s (to_shift + v) n |
---|
[3566] | 168 | ] |
---|
[3579] | 169 | | PopReg v ⇒ frame_assign_var s (to_shift + v) (\snd (\snd s)) |
---|
[3560] | 170 | ]. |
---|
| 171 | |
---|
| 172 | |
---|
[3575] | 173 | definition frame_eval_io:False→frame_store_t→ option frame_store_t≝?. |
---|
[3560] | 174 | // qed. |
---|
| 175 | |
---|
[3575] | 176 | definition frame_eval_cond_cond:condition→ frame_store_t→ option (bool × frame_store_t)≝λc,s. |
---|
[3560] | 177 | !env ← frame_current_env s; |
---|
| 178 | !b ← frame_sem_condition env c; |
---|
| 179 | return 〈b,s〉. |
---|
| 180 | |
---|
| 181 | |
---|
[3575] | 182 | definition frame_eval_loop_cond:condition→ frame_store_t→ option (bool × frame_store_t)≝ |
---|
[3560] | 183 | frame_eval_cond_cond. |
---|
| 184 | |
---|
[3575] | 185 | definition frame_signature≝signature frame_state_params frame_state_params. |
---|
| 186 | |
---|
[3577] | 187 | let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝ |
---|
| 188 | match n with |
---|
| 189 | [ O ⇒ nil ? |
---|
| 190 | | S m ⇒ a :: list_n … a m |
---|
| 191 | ]. |
---|
| 192 | |
---|
[3575] | 193 | definition frame_eval_call:frame_signature→ expr → frame_store_t → (option frame_store_t)≝ |
---|
[3560] | 194 | λsgn,e,st. |
---|
[3562] | 195 | !env ← frame_current_env … st; |
---|
[3567] | 196 | !n ← frame_sem_expr env e; |
---|
[3582] | 197 | frame_assign_var 〈((list_n … O (to_shift + (f_pars … sgn)))::(\fst st)),(\snd st)〉 to_shift n. |
---|
[3560] | 198 | |
---|
[3575] | 199 | definition frame_return_call:expr→ frame_store_t→ (option frame_store_t)≝ |
---|
[3560] | 200 | λr,s.match (\fst s) with |
---|
| 201 | [nil⇒ None ? |
---|
[3566] | 202 | |cons hd tl⇒ !n ← frame_sem_expr hd r; |
---|
| 203 | return 〈tl,〈(\fst (\snd s)),n〉〉 |
---|
[3560] | 204 | ]. |
---|
| 205 | |
---|
[3579] | 206 | definition frame_init_store: ℕ → frame_store_t≝ λn.〈[list_n … O (to_shift + n)],〈O,O〉〉. |
---|
[3560] | 207 | |
---|
| 208 | |
---|
[3579] | 209 | definition 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 |
---|
| 211 | frame_eval_cond_cond frame_eval_loop_cond frame_eval_call frame_return_call (frame_init_store n). |
---|
[3560] | 212 | |
---|
| 213 | (* Abitare tipo Instructions *) |
---|
| 214 | |
---|
| 215 | definition frame_Instructions≝Instructions frame_state_params flat_labels. |
---|
| 216 | |
---|
| 217 | |
---|
[3566] | 218 | definition frame_envitem≝ (env_item frame_env_params frame_instr_params flat_labels). |
---|