source: LTS/Language.ma @ 3394

Last change on this file since 3394 was 3394, checked in by piccolo, 6 years ago

Added abstract language and procedure to add call post labelled

File size: 17.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/types.ma".
16include "Traces.ma".
17include "basics/lists/list.ma".
18include "../src/utilities/option.ma".
19
20record instr_params : Type[1] ≝
21{ seq_instr : DeqSet
22; io_instr : DeqSet
23; cond_instr : DeqSet
24; loop_instr : DeqSet
25; act_params_type : DeqSet
26; return_type : DeqSet
27}.
28
29
30inductive Instructions (p : instr_params) : Type[0] ≝
31 | EMPTY : Instructions p
32 | RETURN : return_type p → Instructions p
33 | SEQ : (seq_instr p) → option NonFunctionalLabel → Instructions p → Instructions p
34 | COND : (cond_instr p) → NonFunctionalLabel → Instructions p →
35                 NonFunctionalLabel → Instructions p → Instructions p →
36                       Instructions p
37 | LOOP : (loop_instr p) → NonFunctionalLabel → Instructions p →
38                  NonFunctionalLabel → Instructions p → Instructions p
39 | CALL : FunctionName → (act_params_type p) → option ReturnPostCostLabel →
40            Instructions p → Instructions p
41 | IO : NonFunctionalLabel → (io_instr p) → NonFunctionalLabel → Instructions p →
42             Instructions p.
43
44let rec eq_instructions (p : instr_params) (i : Instructions p)
45 on i : (Instructions p) → bool ≝
46match i with
47[ EMPTY ⇒ λi'.match i' with [ EMPTY ⇒ true | _ ⇒ false ]
48| RETURN x ⇒ λi'.match i' with [ RETURN y ⇒ x == y | _ ⇒ false ]
49| SEQ x lab instr ⇒ λi'.match i' with
50                      [ SEQ y lab' instr' ⇒ x == y ∧ eq_instructions … instr instr' ∧
51                              match lab with [ None ⇒ match lab' with [ None ⇒ true | _ ⇒ false ]
52                                             | Some l1 ⇒ match lab' with [Some l2 ⇒ eq_nf_label l1 l2 | _ ⇒ false]
53                                             ]
54                      | _ ⇒ false
55                      ]
56| COND x ltrue i1 lfalse i2 i3 ⇒ λi'.match i' with
57                          [ COND y ltrue' i1' lfalse' i2' i3' ⇒
58                             x == y ∧ eq_nf_label ltrue ltrue' ∧
59                             eq_instructions … i1 i1' ∧ eq_nf_label lfalse lfalse' ∧
60                             eq_instructions … i2 i2' ∧ eq_instructions … i3 i3'
61                         | _ ⇒ false
62                         ]
63| LOOP x ltrue i1 lfalse i2 ⇒ λi'.match i' with
64              [ LOOP y ltrue' i1' lfalse' i2' ⇒ x == y ∧
65                      eq_instructions … i1 i1' ∧ eq_nf_label ltrue ltrue' ∧
66                      eq_instructions … i2 i2'
67              | _ ⇒ false
68              ]
69| CALL f act_p r_lb i1 ⇒ λi'.match i' with
70             [ CALL f' act_p' r_lb' i1' ⇒ eq_function_name f f' ∧
71                       act_p == act_p' ∧ eq_instructions … i1 i1' ∧
72                       match r_lb with [ None ⇒ match r_lb' with [None ⇒ true | _ ⇒ false]
73                                       | Some z ⇒ match r_lb' with [Some w ⇒  eq_return_cost_lab z w | _ ⇒ false ]
74                                       ]
75            | _ ⇒ false
76            ]
77| IO lin io lout i1 ⇒ λi'.match i' with
78             [ IO lin' io' lout' i1' ⇒ eq_nf_label lin lin' ∧ io == io' ∧
79                                       eq_nf_label lout lout' ∧ eq_instructions … i1 i1'
80             | _ ⇒ false                                       
81             ]
82].
83
84lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) →
85(i1 ≠ i2 → P false) → P (eq_instructions p i1 i2).
86cases daemon (*TODO*)
87qed.
88
89record env_params : Type[1] ≝
90{ form_params_type : Type[0]
91}.
92
93record env_item (p : env_params) (p' : instr_params) : Type[0] ≝
94{ f_name : FunctionName
95; f_pars : form_params_type p
96; f_lab : CallCostLabel
97; f_body : Instructions p'
98; f_ret : return_type p'
99}.
100
101record state_params : Type[1] ≝
102{ i_pars : instr_params
103; e_pars : env_params
104; store_type : DeqSet
105}.
106
107coercion i_pars.
108coercion e_pars.
109
110record state (p : state_params) : Type[0] ≝
111{ code : Instructions p
112; cont : list (ActionLabel × (Instructions p))
113; store : store_type p
114; io_info : bool
115}.
116
117definition is_io : ∀p.state p → Prop ≝ λp,st.io_info … st = true.
118
119record sem_state_params (p : state_params) : Type[0] ≝
120{ eval_seq : seq_instr p → state p → option (store_type p)
121; eval_io : io_instr p → state p → option (store_type p)
122; eval_cond_cond : cond_instr p → state p → option (bool × (store_type p))
123; eval_loop_cond : loop_instr p → state p → option (bool × (store_type p))
124; eval_call : env_item p p → act_params_type p → state p → option (store_type p)
125; eval_after_return : return_type p → store_type p → option (store_type p)
126; init_store : store_type p
127}.
128
129
130let rec lookup (p : env_params) (p' : instr_params) (l : list (env_item p p'))
131 on l : FunctionName → option (env_item p p') ≝
132match l with
133[ nil ⇒ λ_.None ?
134| cons x xs ⇒  λf.if (eq_function_name f (f_name … x))
135                  then Some ? x
136                  else lookup … xs f
137].
138
139definition is_ret_act : ActionLabel → Prop ≝
140λa.match a with [ret_act _ ⇒ True | _ ⇒ False ].
141
142inductive execute_l (p : state_params) (p' : sem_state_params p) (env : list (env_item p p)) :
143                                         ActionLabel → relation (state p) ≝
144| empty : ∀st,st',hd,tl.(code ? st) = (EMPTY p)→ (cont ? st) = hd :: tl →
145           (code ? st') = \snd hd → (cont … st') = tl → (store … st) = (store … st') →
146           (io_info … st = true → is_non_silent_cost_act (\fst hd)) →  (io_info … st') = false → ¬ is_ret_act (\fst hd) →  execute_l … (\fst hd) st st'
147| seq_sil : ∀st,st',i,cd,s,opt_l.(code ? st) = SEQ … i opt_l cd →
148             eval_seq … p' i st = return s → (code ? st') = cd →
149             (cont … st) = (cont … st') → (store … st') = s →
150             io_info … st = false →  io_info ? st' = false → execute_l … (cost_act opt_l) st st'
151| cond_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m.
152   (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp st = return 〈true,new_m〉 →
153   cont ? st' = 〈cost_act (None ?),cd〉 ::(cont … st) → code … st' = i_true → store … st' = new_m →
154   io_info … st = false →  io_info … st' = false → execute_l … (cost_act (Some ? ltrue)) st st'
155| cond_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m.
156   (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp st = return 〈false,new_m〉 →
157   cont ? st' = 〈cost_act (None ?),cd〉 ::(cont … st) → code … st' = i_false → store … st' = new_m →
158   io_info … st = false →  io_info … st' = false → execute_l … (cost_act (Some ? lfalse)) st st'
159| loop_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m.
160   code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp st = return 〈true,new_m〉 →
161   cont ? st' = 〈cost_act (None ?),LOOP … exp ltrue i_true lfalse i_false〉 :: (cont … st) →
162   code … st' = i_true → store … st' = new_m → io_info … st = false →  io_info … st' = false →
163   execute_l … (cost_act (Some ? ltrue)) st st'
164| loop_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m.
165   code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp st = return 〈false,new_m〉 →
166   cont ? st' = cont … st → code … st' = i_false → store … st = store … st' →
167   io_info … st = false →  io_info … st' = false → execute_l … (cost_act (Some ? lfalse)) st st'
168| io_in : ∀st,st',lin,io,lout,cd,mem.(code ? st) = IO … lin io lout cd →
169    eval_io … p' io st = return mem → code ? st' = EMPTY p →
170    cont … st' = 〈cost_act (Some ? lout),cd〉 :: (cont … st) → store … st' = mem →
171    io_info … st' = true → execute_l … (cost_act (Some ? lin)) st st'
172| call : ∀st,st',f,act_p,r_lb,cd,mem,env_it.(code ? st) = CALL … f act_p r_lb cd →
173    lookup … env f = return env_it →
174    eval_call ? p' env_it act_p st = return mem →
175    store ? st' = mem → code … st' = f_body … env_it →
176     cont … st' =
177       〈(ret_act (match r_lb with [Some lb ⇒ Some ? (inl ?? lb)
178                                  | None ⇒ None ?])),cd〉 :: (cont … st) → 
179    io_info … st = false →  (io_info … st') = false →
180    execute_l … (call_act f (inl ?? (f_lab ?? env_it))) st st'
181| ret_instr : ∀st,st',r_t,mem,tl',rb,cd.code ? st = RETURN … r_t →
182   cont … st = 〈ret_act rb,cd〉 :: tl' → cont ? st' = tl' →
183   io_info … st = false →  io_info ? st' = false →
184   eval_after_return … p' r_t (store … st) = return mem → code … st' = cd →
185   store … st' = mem → execute_l … (ret_act rb) st st'.
186
187record Program (p : env_params) (p' : instr_params) : Type[0] ≝
188{ env : list (env_item p p')
189; main : Instructions p'
190}.
191
192definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.True.
193(* bisognerebbe confrontare la coda dell'istruzione corrente e la parte di stack fino alla prima label.
194 match (code … s1) with
195 [ CALL f act_p r_lb i1 ⇒ code … s2 = i1
196 | _ ⇒ False
197 ].
198*)
199
200include "basics/lists/listb.ma".
201include "../src/utilities/hide.ma".
202
203definition operational_semantics : ∀p : state_params.∀p'.Program p p → abstract_status ≝
204λp,p',prog.mk_abstract_status
205                (state p)
206                (execute_l ? p' (env … prog))
207                (is_synt_succ …)
208                (λs.match (code … s) with
209                    [ COND _ _ _ _ _ _ ⇒ cl_jump
210                    | LOOP _ _ _ _ _ ⇒ cl_jump
211                    | EMPTY ⇒ if io_info … s then cl_io else cl_other
212                    | _ ⇒ cl_other
213                    ])
214                (λs.match (code … s) with
215                    [CALL _ _ m _ ⇒ match m with [ Some _ ⇒ true | None ⇒ false ]
216                    | _ ⇒ false
217                    ])
218                (λs.eq_instructions … (code … s) (main … prog) ∧ isnilb … (cont … s) ∧ store … s == init_store … p' ∧ io_info … s)
219                (λs.match (cont … s) with
220                    [ nil ⇒ match (code … s) with
221                            [ EMPTY ⇒ true
222                            | RETURN _ ⇒ true
223                            | _ ⇒ false
224                            ]
225                    | _ ⇒ false
226                    ])
227                ???.
228@hide_prf
229[ #s1 #s2 #l #H #H1 inversion H1 #st #st'
230 [ #hd #tl
231 | #i #cd #s #opt_l
232 |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m
233 |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m
234 | #lin #io #lout #cd #mem
235 | #f #act_p #r_lb #cd #mem #env_it
236 | #r_t #mem #tl #rb #cd
237 ]
238 #EQcode
239 [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQ5 #H2 #EQ' #EQ6 #EQ7
240 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
241 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
242 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
243 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
244 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
245 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8
246 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
247 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
248 ]
249 #_ destruct >EQcode in H; normalize nodelta /2 by ex_intro/
250 [ cases(io_info ??) normalize nodelta] #EQ destruct
251| #s1 #s2 #l #H #H1 inversion H1 #st #st'
252 [ #hd #tl
253 | #i #cd #s #opt_l
254 |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m
255 |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m
256 | #lin #io #lout #cd #mem
257 | #f #act_p #r_lb #cd #mem #env_it
258 | #r_t #mem #tl #rb #cd
259 ]
260 #EQcode
261 [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7
262 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
263 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
264 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
265 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
266 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
267 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost' #EQ6 #EQ7 #EQ8
268 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQiost' #EQ8 #EQ9 #EQ10
269 | #EQ1 #EQ2 #EQ3 #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
270 ]
271 #_ destruct
272 cases(code ? st') in H; normalize nodelta >EQiost' normalize nodelta
273 #eq destruct try (#eq1 destruct) try (#eq2 destruct) try (#eq3 destruct)
274 try (#eq4 destruct) try (#eq5 destruct) try (#eq6 destruct) %{lin} %
275| #s1 #s2 #l #H #H1 inversion H1 #st #st'
276 [ #hd #tl
277 | #i #cd #s #opt_l
278 |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m
279 |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m
280 | #lin #io #lout #cd #mem
281 | #f #act_p #r_lb #cd #mem #env_it
282 | #r_t #mem #tl #rb #cd
283 ]
284 #EQcode
285 [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7
286 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
287 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
288 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
289 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
290 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
291 | #EQ1 #EQ2 #EQ3 #EQiost #EQiost' #EQ6 #EQ7 #EQ8
292 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost #EQiost' #EQ8 #EQ9 #EQ10
293 | #EQ1 #EQ2 #EQiost #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
294 ]
295 #_ destruct >EQcode in H; normalize nodelta [|*: #EQ destruct]
296 cases(io_info … st) in x; normalize nodelta [2: #_ #EQ destruct]
297 #H3 #_ @H3 %
298]
299qed.
300
301let rec eqb_list (D : DeqSet) (l1 : list D) on l1 : list D → bool ≝
302match l1 with
303[ nil ⇒ λl2.match l2 with [nil ⇒ true | _ ⇒ false ]
304| cons x xs ⇒ λl2.match l2 with [ cons y ys ⇒ x == y ∧ eqb_list … xs ys | _ ⇒ false ]
305].
306
307definition DeqSet_List : DeqSet → DeqSet ≝
308λX.mk_DeqSet (list X) (eqb_list …) ?.
309#x elim x [ * /2 by refl, conj/ #y #ys normalize % #EQ destruct] -x
310#x #xs #IH * [ normalize % #EQ destruct] #y #ys normalize % inversion(x == y)
311#EQ normalize nodelta
312[ #H >(proj1 … (IH ys) H) @eq_f2 [2: %] @(proj1 … (eqb_true …)) assumption
313| #EQ destruct
314| #EQ1 destruct @(proj2 … (IH …)) %
315| #EQ1 destruct <EQ @(proj2 … (eqb_true …)) %
316]
317qed.
318
319unification hint  0 ≔ C;
320    X ≟ DeqSet_List C
321(* ---------------------------------------- *) ⊢
322    list C ≡ carr X.
323
324
325unification hint  0 ≔ D,p1,p2;
326    X ≟ DeqSet_List D
327(* ---------------------------------------- *) ⊢
328    eqb_list D p1 p2 ≡ eqb X p1 p2.
329    check NonFunctionalLabel
330
331definition associative_list : DeqSet → Type[0] → Type[0] ≝
332λA,B.list (A × (list B)).
333
334let rec update_list (A : DeqSet) (B : Type[0]) (l : associative_list A B)
335   on l : A → list B → associative_list A B ≝
336λa,b.match l with
337    [ nil ⇒ [〈a,b〉]
338    | cons x xs ⇒ if (a == (\fst x)) then 〈a,b〉 :: xs
339                  else x :: (update_list … xs a b) 
340    ].
341
342let rec get_element (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : A → list B ≝
343λa.match l with [ nil ⇒ nil ?
344                | cons x xs ⇒ if (a == \fst x) then \snd x else get_element … xs a
345                ].
346 
347definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝
348λx.〈a_non_functional_label x,S x〉.
349
350definition fresh_cc_labe : ℕ → CallCostLabel × ℕ ≝
351λx.〈a_call_label x,S x〉.
352
353definition fresh_rc_label : ℕ → ReturnPostCostLabel × ℕ ≝
354λx.〈a_return_cost_label x,S x〉.
355
356let rec call_post_trans (p : instr_params) (i : Instructions p) (n : ℕ) on i :
357((list CostLabel) × (Instructions p)) × (ℕ × (associative_list DEQCostLabel CostLabel)) ≝
358match i with
359[ EMPTY ⇒ 〈nil ?,EMPTY p,n,nil ?〉
360| RETURN x ⇒ 〈nil ?,RETURN … x,n,nil ?〉
361| SEQ x lab instr ⇒
362   let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … instr n in
363   match lab with
364   [ None ⇒ 〈l1,SEQ … x (None ?) instr1,n1,m1〉
365   | Some lbl ⇒ 〈nil CostLabel,SEQ … x (Some ? lbl) instr1, n1, update_list ?? m1 lbl (lbl :: l1) 〉
366   ]
367| COND x ltrue i1 lfalse i2 i3 ⇒
368   let 〈l3,instr3,n3,m3〉 ≝ call_post_trans … i3 n in
369   let 〈l2,instr2,n2,m2〉 ≝ call_post_trans … i2 n3 in
370   let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … i1 n2 in
371  〈nil ?,COND … x ltrue instr1 lfalse instr2 instr3,n1,
372    update_list DEQCostLabel CostLabel
373      (update_list DEQCostLabel CostLabel (m1 @ m2 @ m3) ltrue (ltrue :: (l1 @ l3)))
374      lfalse (lfalse :: (l2 @ l3))〉
375| LOOP x ltrue i1 lfalse i2 ⇒
376   let 〈l2,instr2,n2,m2〉 ≝ call_post_trans … i2 n in
377   let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … i1 n2 in
378   〈nil ?,LOOP … x ltrue instr1 lfalse instr2,n1,
379      update_list DEQCostLabel CostLabel
380         (update_list DEQCostLabel CostLabel (m1 @ m2) ltrue (ltrue :: l1))
381         lfalse (lfalse :: l2)〉
382| CALL f act_p r_lb i1 ⇒
383   let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … i1 n in
384   match r_lb with
385   [ None ⇒ let 〈l',f''〉 ≝ fresh_rc_label n1 in
386            〈(a_return_post l')::l1,CALL … f act_p (Some ? l') instr1,f'',m1〉
387   | Some lbl ⇒ 〈nil ?,CALL ? f act_p (Some ? lbl) instr1,n1,update_list ?? m1 lbl (lbl :: l1)〉
388   ]
389| IO lin io lout i1 ⇒
390    let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … i1 n in
391    〈nil ?,IO ? lin io lout instr1,n1,update_list ?? (update_list ?? m1 lout (lout :: l1)) lin [lin]〉
392].
393
Note: See TracBrowser for help on using the repository browser.