source: LTS/variable.ma @ 3579

Last change on this file since 3579 was 3579, checked in by piccolo, 4 years ago
File size: 7.9 KB
Line 
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
15include "imp.ma".
16
17definition to_shift : ℕ ≝ 2.
18
19definition activation_frame ≝ DeqSet_List DeqNat.
20
21let rec update (A : Type[0]) (l : list A) (n : ℕ) (a : A) on l : option (list A) ≝
22match l with
23[ nil ⇒ None ?
24| cons x xs ⇒
25   match n with
26   [ O ⇒ return (a :: xs)
27   | S m ⇒ !res ← update … xs m a; return (x::res) ]].
28
29lemma nth_opt_update_hit:
30 ∀A,n,env,a,env'.
31  update A env a n = return env' →
32  nth_opt … a env' = return n.
33 #A #n #env elim env
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 ]]
40qed.
41
42lemma 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) ]]
53qed.
54
55lemma 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/ ]]
67qed.
68
69definition assign_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.λn:DeqNat.update … env (|env| - v - fp -1) n.
70
71definition read_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.nth_opt … (|env| -v -fp -1) env.
72
73lemma read_frame_assign_frame_hit:
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)
79qed.
80
81lemma 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' ]*)
94qed.
95
96let 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
108let 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
119definition frame_store_t≝ DeqProd (DeqSet_List activation_frame) (DeqProd DeqNat DeqNat). (*frame_pointer e return register*)
120
121definition frame_env_params ≝ mk_env_params ℕ.
122
123inductive frame_seq_i : Type[0] ≝
124| Seq_i : seq_i → frame_seq_i
125| PopReg : variable → frame_seq_i.
126
127definition eq_frame_seq_i : frame_seq_i → frame_seq_i → bool ≝
128λx,y.
129match 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
134lemma eq_frame_seq_i_elim : ∀P : bool → Prop.∀s1,s2.(s1 = s2 → P true) → (s1 ≠ s2 → P false) →
135P (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
137try(@H2 % #EQ destruct)
138[ @seq_i_eq_elim | @(eqb_elim v v') ]
139[1,3: #EQ destruct /2/ |*: * #H @H2 % #EQ destruct @H %]
140qed.
141
142definition DeqFrameSeqI ≝ mk_DeqSet frame_seq_i eq_frame_seq_i ?.
143@hide_prf #x #y @eq_frame_seq_i_elim
144[ #EQ destruct /2/ | * #H % #EQ destruct cases H % ]
145qed.
146
147definition frame_instr_params : instr_params ≝
148mk_instr_params DeqFrameSeqI DeqFalse DeqCondition DeqCondition DeqExpr DeqExpr.
149
150definition frame_state_params:state_params≝
151mk_state_params frame_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
152
153definition frame_current_env:frame_store_t→ option ?≝λs.!hd ← option_hd … (\fst s); return hd.
154
155definition frame_assign_var ≝ λenv:frame_store_t.λv:variable.λn:DeqNat.
156match \fst env with
157[ nil ⇒ None ?
158| cons hd tl ⇒ ! x ← (assign_frame hd (to_shift + v) (\fst (\snd env)) n); return ((〈x::tl,\snd env〉))
159].
160
161definition frame_eval_seq:frame_seq_i →frame_store_t→ option frame_store_t≝
162λi,s.match i with
163[ Seq_i instr ⇒
164   match instr with
165   [sAss v e ⇒ !env ← frame_current_env … s;
166               ! n ← frame_sem_expr env e;
167               frame_assign_var s (to_shift + v) n
168   ]
169| PopReg v ⇒ frame_assign_var s (to_shift + v) (\snd (\snd s))
170].
171
172
173definition frame_eval_io:False→frame_store_t→ option frame_store_t≝?.
174// qed.
175
176definition frame_eval_cond_cond:condition→ frame_store_t→ option (bool × frame_store_t)≝λc,s.
177!env ← frame_current_env s;
178!b ← frame_sem_condition env c;
179return 〈b,s〉.
180
181
182definition frame_eval_loop_cond:condition→ frame_store_t→ option (bool × frame_store_t)≝
183frame_eval_cond_cond.
184
185definition frame_signature≝signature frame_state_params frame_state_params.
186
187let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝
188match n with
189[ O ⇒ nil ?
190| S m ⇒ a :: list_n … a m
191].
192
193definition frame_eval_call:frame_signature→ expr → frame_store_t → (option frame_store_t)≝
194λsgn,e,st.
195    !env ← frame_current_env … st;
196    !n ← frame_sem_expr env e;
197    frame_assign_var 〈((list_n … O (pred (to_shift + (f_pars … sgn))))::(\fst st)),(\snd st)〉 to_shift n.
198
199definition frame_return_call:expr→ frame_store_t→ (option frame_store_t)≝
200λr,s.match (\fst s) with
201[nil⇒ None ?
202|cons hd tl⇒ !n ← frame_sem_expr hd r;
203             return 〈tl,〈(\fst (\snd s)),n〉〉
204].
205 
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).
212
213  (* Abitare tipo Instructions *)
214 
215definition frame_Instructions≝Instructions frame_state_params flat_labels.
216
217
218definition frame_envitem≝ (env_item frame_env_params frame_instr_params flat_labels).
Note: See TracBrowser for help on using the repository browser.