source: LTS/imp.ma @ 3580

Last change on this file since 3580 was 3578, checked in by piccolo, 4 years ago

baco

File size: 9.6 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 "Language.ma".
16
17
18(* Syntax *)
19
20definition variable ≝ DeqNat.
21
22inductive expr: Type[0] ≝
23   Var: variable → expr
24 | Const: DeqNat → expr
25 | Plus: expr → expr → expr
26 | Minus: expr → expr → expr.
27
28inductive condition: Type[0] ≝
29   Eq: expr → expr → condition
30 | Not: condition → condition.
31
32let rec expr_eq (e1:expr) (e2:expr) on e1 :bool≝
33match e1 with [Var v1⇒ match e2 with [Var v2⇒ eqb v1 v2|_⇒ false]
34|Const v1⇒ match e2 with [Const v2⇒ eqb v1 v2|_⇒ false]
35|Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
36|Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
37].
38
39lemma expr_eq_elim : ∀P : bool → Prop.∀e1,e2.(e1 = e2 → P true) → (e1 ≠ e2 → P false) → P (expr_eq e1 e2).
40#P #e1 lapply P -P elim e1 -e1
41[1,2: #v #P * [1,5: #v' |2,6: #v' |*: #e1 #e2 ] #H1 #H2 normalize try(@H2 % #EQ destruct) @(eqb_elim v v')
42  [1,3: #EQ destruct @H1 % |*: * #H @H2 % #EQ destruct @H %]
43|*: #e1 #e2 #IH1 #IH2 #P * [1,5: #v' |2,6: #v' |*: #e1' #e2' ] #H1 #H2 try(@H2 % #EQ destruct) normalize
44    @IH1
45    [1,3: #EQ destruct normalize @IH2 [1,3: #EQ destruct @H1 % |*: * #H @H2 % #EQ destruct @H %]
46    |*: * #H @H2 % #EQ destruct @H %
47    ]
48]
49qed.
50
51definition DeqExpr ≝
52mk_DeqSet expr expr_eq ?.
53@hide_prf #e1 #e2 @expr_eq_elim
54[ #EQ destruct % // | * #H % #EQ destruct cases H % ]
55qed.
56
57unification hint  0 ≔ ;
58    X ≟ DeqExpr
59(* ---------------------------------------- *) ⊢
60    expr ≡ carr X.
61
62(*
63unification hint  0 ≔ p1,p2;
64    X ≟ DeqExpr
65(* ---------------------------------------- *) ⊢
66    expr_eq p1 p2 ≡ eqb X p1 p2.
67*)
68(* for the syntactical record in Language.ma *)
69
70
71  (* seq_i: type of sequential instructions *)
72
73inductive seq_i:Type[0]≝ |sAss: variable → expr → seq_i.
74
75definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.
76match s1 with [
77sAss v e ⇒ match s2 with [sAss v' e' ⇒ (andb (v==v') (expr_eq e e')) ]
78].
79
80
81lemma seq_i_eq_elim : ∀P : bool → Prop.∀s1,s2.(s1 = s2 → P true) → (s1 ≠ s2→ P false) → P (seq_i_eq s1 s2).
82#P * #v #e * #v' #e' #H1 #H2 normalize @(eqb_elim v v')
83[ #EQ destruct @expr_eq_elim [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
84| * #H @H2 % #EQ destruct @H %
85]
86qed.
87
88definition DeqSeqI ≝ mk_DeqSet seq_i seq_i_eq ?.
89@hide_prf #e1 #e2 @seq_i_eq_elim
90[ #EQ destruct % // | * #H % #EQ destruct cases H % ]
91qed.
92
93unification hint  0 ≔ ;
94    X ≟ DeqSeqI
95(* ---------------------------------------- *) ⊢
96    seq_i ≡ carr X.
97
98(* ambigous input! why?
99unification hint  0 ≔ p1,p2;
100    X ≟ DeqSeqI
101(* ---------------------------------------- *) ⊢
102    seq_i_eq p1 p2 ≡ eqb X p1 p2.
103*)
104
105
106let rec cond_i_eq (c1:condition) (c2:condition):bool ≝
107match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒
108(andb (expr_eq e1 f1) (expr_eq e2 f2))|_⇒ false]
109|Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]].
110
111lemma cond_i_eq_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) → (c1 ≠c2 → P false) → P (cond_i_eq c1 c2).
112#P #c1 lapply P -P elim c1 -c1
113[ #e1 #e2 #P * [ #e1' #e2' | #c' ] #H1 #H2 normalize try (@H2 % #EQ destruct) @expr_eq_elim
114  [ #EQ destruct @expr_eq_elim [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
115  | * #H @H2 % #EQ destruct @H %
116  ]
117| #c #IH #P * [ #e1' #e2' | #c' ] #H1 #H2 normalize try (@H2 % #EQ destruct) @IH
118  [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
119]
120qed.
121
122definition DeqCondition ≝ mk_DeqSet condition cond_i_eq ?.
123@hide_prf #e1 #e2 @cond_i_eq_elim
124[ #EQ destruct % // | * #H % #EQ destruct cases H % ]
125qed.
126
127unification hint  0 ≔ ;
128    X ≟ DeqCondition
129(* ---------------------------------------- *) ⊢
130    condition ≡ carr X.
131
132(* ambigous input!!!
133unification hint  0 ≔ p1,p2;
134    X ≟ DeqCondition
135(* ---------------------------------------- *) ⊢
136    cond_i_eq p1 p2 ≡ eqb X p1 p2.
137*)
138
139  (* syntactical record *)
140
141definition imp_instr_params: instr_params ≝ mk_instr_params DeqSeqI DeqFalse
142DeqCondition DeqCondition (DeqProd variable DeqExpr) DeqExpr.
143
144definition environment ≝ DeqSet_List (DeqProd variable DeqNat).
145
146
147definition default_env: environment ≝ nil ?.
148 
149
150let rec assign (env:environment) (v:variable) (n:DeqNat):environment ≝match env with
151[nil ⇒ [mk_Prod … v n]
152|cons hd tl ⇒
153    let 〈v',n'〉≝ hd in if (v==v')
154                       then 〈v,n〉::tl
155                       else hd::(assign tl v n)
156].
157
158let rec read (env:environment) (v:variable):(option DeqNat)≝match env with
159[nil ⇒ None …
160|cons hd tl ⇒ let 〈v',n〉≝ hd in
161  if (v==v')
162  then Some … n
163  else read tl v
164].
165
166
167lemma assign_hit: ∀env,v,val. read (assign env v val) v = Some … val.
168#env elim env
169[2: * #v' #val' #env' #IH #v #val whd in match (assign ???);
170inversion (v==v')
171 [#INV whd in ⊢ (??%?); >(\b (refl …)) %
172 |#INV whd in ⊢ (??%?); >INV whd in ⊢ (??%?); @IH ]
173|#v #val whd in match (assign [ ] v val); normalize >(eqb_n_n v) %]qed.
174
175
176
177lemma assign_miss: ∀env,v1,v2,val. v2 ≠ v1 → (read (assign env v1 val) v2)= (read env v2).
178 #env #v1 #v2 #val #E elim env [normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/
179|* #v #n #env' #IH inversion(v1==v) #INV [lapply(\P INV)|lapply(\Pf INV)] #K [destruct
180whd in match (assign ???); >INV normalize nodelta whd in match (read (〈v,n〉::env') v2);
181inversion(v2==v) #INV2 >INV2 normalize nodelta
182whd in match (read (〈v,val〉::env') v2); >INV2 normalize nodelta
183whd in match (read (〈v,n〉::env') v2); try %
184lapply (\P INV2) #ABS cases(absurd ? ABS E)
185(*elim E #ABS2 lapply (ABS2 ABS) #F cases F*)
186|whd in match (assign ???); >INV normalize nodelta whd in match (read ??);
187inversion(v2==v) #INV2 whd in match(if ? then ? else ?);
188[whd in match (read ??); >INV2 %
189|>IH whd in match (read (〈v,n〉::env') v2);  >INV2 %
190qed.
191
192let rec sem_expr (env:environment) (e: expr) on e : (option nat) ≝
193 match e with
194  [ Var v ⇒ read env v
195  | Const n ⇒ Some ? n
196  | Plus e1 e2 ⇒ !n1 ← sem_expr env e1;
197                 !n2 ← sem_expr env e2;
198                 return (n1+n2)
199  | Minus e1 e2 ⇒ !n1 ← sem_expr env e1;
200                  !n2 ← sem_expr env e2;
201                  return (n1-n2)
202  ].
203
204let rec sem_condition (env:environment) (c:condition) on c : option bool ≝
205  match c with
206   [ Eq e1 e2 ⇒ !n ← sem_expr env e1;
207                !m ← sem_expr env e2;
208                return (eqb n m)
209   | Not c ⇒ !b ← sem_condition env c;
210             return (notb b)
211   ].
212
213
214
215(*CERCO*)
216
217definition imp_env_params:env_params≝mk_env_params variable.
218
219definition store_t≝ DeqSet_List (DeqProd environment variable).
220
221definition imp_state_params:state_params≝
222mk_state_params imp_instr_params imp_env_params flat_labels store_t (*DeqEnv*).
223
224definition current_env:store_type imp_state_params→ option environment≝λs.!hd ← option_hd … s; return \fst hd.
225
226definition assign_var ≝ λenv:store_t.λv:variable.λn:DeqNat.
227match env with
228[ nil ⇒ None ?
229| cons hd tl ⇒ let 〈e,var〉 ≝ hd in return (〈assign e v n,var〉 :: tl)
230].
231
232
233definition imp_eval_seq:seq_i →store_t→ option store_t
234≝λi,s.
235match i with
236[sAss v e ⇒ match s with
237  [nil⇒ None ?
238  |cons hd tl⇒ let 〈env,var〉 ≝ hd in
239               ! n ← sem_expr env e;
240               assign_var s v n
241  ]
242].
243
244
245definition imp_eval_io: False → store_t→ option store_t≝?.
246// qed.
247
248definition imp_eval_cond_cond:condition → store_t→ option (bool × store_t)≝λc,s.
249!env ← current_env s;
250!b ← sem_condition env c;
251return 〈b,s〉.
252
253
254definition imp_eval_loop_cond:condition→ store_t → option (bool × store_t)≝
255imp_eval_cond_cond.
256
257definition imp_init_store: store_t≝[〈(nil ?),O〉].
258
259definition imp_signature≝signature imp_state_params imp_state_params.
260
261definition imp_eval_call:imp_signature→ (variable × expr) → store_t → (option store_t)≝
262λsgn,e,st.
263  match sgn with
264  [ mk_signature fun fpt rt ⇒
265    let 〈var,act_exp〉 ≝ e in
266    match st with
267    [nil ⇒ None ?
268    |cons hd tl⇒ let 〈env,v〉≝ hd in
269                 !n ← sem_expr env act_exp;
270                 assign_var (〈(nil ?),var〉::st) fpt n
271    ]
272  ].
273
274definition imp_return_call:expr→ store_t→ (option store_t)≝
275λr,s.match s with
276[nil⇒ None ?
277|cons hd tl⇒ let 〈env,v〉≝ hd in
278             !n ← sem_expr env r;
279             assign_var tl v n
280].
281 
282
283definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params imp_state_params imp_eval_seq imp_eval_io
284imp_eval_cond_cond imp_eval_loop_cond imp_eval_call imp_return_call imp_init_store.
285
286  (* Abitare tipo Instructions *)
287 
288definition imp_Instructions≝Instructions imp_state_params flat_labels.
289
290definition imp_envitem≝ (env_item imp_env_params imp_instr_params flat_labels).
Note: See TracBrowser for help on using the repository browser.