source: LTS/imp.ma @ 3560

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

language example

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