source: src/joint/blocks.ma @ 2760

Last change on this file since 2760 was 2674, checked in by tranquil, 7 years ago
  • another change in block definition
  • RTLabs -> RTL and ERTL -> ERTLptr passes fixed, others stil broken
File size: 27.7 KB
Line 
1include "joint/Joint.ma".
2include "utilities/bindLists.ma".
3
4(* inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝
5  | block_seq : joint_seq p globals → block_step p globals
6  | block_skip : label → block_step p globals.
7
8definition if_seq : ∀p,globals.∀A:Type[2].block_step p globals → A → A → A ≝
9λp,g,A,s.match s with
10[ block_seq _ ⇒ λx,y.x
11| _ ⇒ λx,y.y
12].
13
14definition stmt_of_block_step : ∀p : stmt_params.∀globals.
15  ∀s : block_step p globals.if_seq … s (succ p) unit → joint_statement p globals ≝
16  λp,g,s.match s return λx.if_seq ??? x ?? → joint_statement ?? with
17  [ block_seq s' ⇒ λnxt.sequential … s' nxt
18  | block_skip l ⇒ λ_.GOTO … l
19  ].
20
21definition seq_to_block_step_list : ∀p : stmt_params.∀globals.
22  list (joint_seq p globals) →
23  list (block_step p globals) ≝ λp,globals.map ?? (block_seq ??).
24
25coercion block_step_from_seq_list : ∀p : stmt_params.∀globals.
26  ∀l:list (joint_seq p globals).
27  list (block_step p globals) ≝
28  seq_to_block_step_list
29  on _l:list (joint_seq ??)
30  to list (block_step ??).
31
32definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
33  [ inl _ ⇒ true
34  | inr _ ⇒ false
35  ].
36definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
37  [ inl _ ⇒ true
38  | inr _ ⇒ false
39  ].
40
41definition skip_block ≝ λp,globals,A.
42  (list (block_step p globals)) × A.*)
43
44(* move *)
45let rec bind_new_P R X (P : X → Prop) (b : bind_new R X) on b : Prop ≝
46match b with
47[ bret x ⇒ P x
48| bnew f ⇒ ∀x.bind_new_P … P (f x)
49].
50
51definition BindNewP : ∀R.MonadPred (BindNew R) ≝
52λR.mk_MonadPred (BindNew R) (bind_new_P R) ???.
53[ #X #P #x #K @K
54| #X #Y #Pin #Pout #m elim m -m
55  [ #x #H #f #G @G @H
56  | #g #IH #H #f #G #x @IH [ @H | @G ]
57  ]
58| #X #P #Q #H #m elim m -m
59  [ #x #Px @H @Px
60  | #g #IH #Pg #x @IH @Pg
61  ]
62]
63qed.
64
65definition not_empty : ∀X.list X → Prop ≝ λX,l.match l with [ nil ⇒ False | _ ⇒ True ].
66
67definition split_on_last : ∀X.list X → option ((list X) × X) ≝
68λX.foldr …
69  (λel,acc.match acc with
70    [ None ⇒ Some ? 〈[ ], el〉
71    | Some pr ⇒ Some ? 〈el :: \fst pr, \snd pr〉
72    ]) (None ?).
73
74lemma split_on_last_inv : ∀X,l.
75match split_on_last X l with
76[ None ⇒ l = [ ]
77| Some pr ⇒ l = \fst pr @ [ \snd pr]
78].
79#X #l elim l -l normalize nodelta [ // ]
80#hd #tl
81change with (match split_on_last ? tl in option  with [ _ ⇒ ?]) in
82  match (split_on_last ? (hd :: tl)); cases (split_on_last ??)
83normalize nodelta [2: * #pref #last ] #EQ >EQ normalize % qed.
84
85lemma split_on_last_hit : ∀X,pref,last.
86split_on_last X (pref @ [last]) = Some ? 〈pref, last〉.
87#X #pref elim pref -pref normalize [//]
88#hd #tl #IH #last >IH % qed.
89
90(* the label input is to accomodate ERTLptr pass
91   the postfix is for the case CALL ↦ instrs* ; CALL; instrs* *)
92definition step_block ≝
93  λp,globals.list (code_point p → joint_seq p globals) ×
94             (code_point p → joint_step p globals) ×
95             (list (joint_seq p globals)).
96
97definition fin_block ≝ λp,globals.(list (joint_seq p globals))×(joint_fin_step p).
98
99(*definition seq_to_skip_block :
100  ∀p,g,A.seq_block p g A → skip_block p g A
101 ≝ λp,g,A,b.〈\fst b, \snd b〉.
102
103coercion skip_from_seq_block :
104  ∀p,g,A.∀b : seq_block p g A.skip_block p g A ≝
105  seq_to_skip_block on _b : seq_block ??? to skip_block ???.*)
106
107definition bind_step_block ≝ λp.λglobals.
108  bind_new register (step_block p globals).
109
110unification hint 0 ≔ p, g;
111P ≟ step_block p g
112(*---------------------------------------*)⊢
113bind_step_block p g ≡ bind_new register P.
114
115definition bind_fin_block ≝ λp : stmt_params.λglobals.
116  bind_new register (fin_block p globals).
117
118unification hint 0 ≔ p : stmt_params, g;
119P ≟ fin_block p g
120(*---------------------------------------*)⊢
121bind_fin_block p g ≡ bind_new register P.
122
123definition bind_seq_list ≝ λp : stmt_params.λglobals.
124  bind_new register (list (joint_seq p globals)).
125unification hint 0 ≔ p : stmt_params, g;
126S ≟ joint_seq p g,
127L ≟ list S
128(*---------------------------------------*)⊢
129bind_seq_list p g ≡ bind_new register L.
130
131definition add_dummy_variance : ∀X,Y : Type[0].list Y → list (X → Y) ≝ λX,Y.map … (λx.λ_.x).
132
133definition ensure_step_block : ∀p : params.∀globals.
134list (joint_seq p globals) → step_block p globals ≝
135λp,g,l.
136match split_on_last … l return λ_.step_block ?? with
137[ None ⇒ 〈[ ], λ_.NOOP ??, [ ]〉
138| Some pr ⇒ 〈add_dummy_variance … (\fst pr), λ_.\snd pr, [ ]〉
139].
140
141coercion step_block_from_seq_list nocomposites :
142∀p : params.∀g.∀l : list (joint_seq p g).step_block p g ≝
143ensure_step_block on _l : list (joint_seq ??) to step_block ??.
144
145(*definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
146  bind_new (localsT p) (skip_block p globals A).
147unification hint 0 ≔ p : stmt_params, g, A;
148B ≟ skip_block p g A, R ≟ localsT p
149(*---------------------------------------*)⊢
150bind_skip_block p g A ≡ bind_new R B.
151
152definition bind_seq_to_skip_block :
153  ∀p,g,A.bind_seq_block p g A → bind_skip_block p g A ≝
154  λp,g,A.m_map ? (seq_block p g A) (skip_block p g A)
155    (λx.x).
156
157coercion bind_skip_from_seq_block :
158  ∀p,g,A.∀b:bind_seq_block p g A.bind_skip_block p g A ≝
159  bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???.*)
160(*
161definition block_classifier ≝
162  λp,g.λb : other_block p g.
163  seq_or_fin_step_classifier ?? (\snd b).
164*)
165(*definition seq_block_from_seq_list :
166∀p : stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝
167λp,g,l.let 〈pre,post〉 ≝ split_on_last … (NOOP ??) l in 〈pre, (post : joint_step ??)〉.
168
169definition bind_seq_block_from_bind_seq_list :
170  ∀p : stmt_params.∀g.bind_new (localsT p) (list (joint_seq p g)) →
171    bind_seq_block p g (joint_step p g) ≝ λp.λg.m_map … (seq_block_from_seq_list …).
172
173definition bind_seq_block_step :
174  ∀p,g.bind_seq_block p g (joint_step p g) →
175    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
176  λp,g.inl ….
177coercion bind_seq_block_from_step :
178  ∀p,g.∀b:bind_seq_block p g (joint_step p g).
179    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
180  bind_seq_block_step on _b : bind_seq_block ?? (joint_step ??) to
181    bind_seq_block ?? (joint_step ??) + bind_seq_block ?? (joint_fin_step ?).
182
183definition bind_seq_block_fin_step :
184  ∀p,g.bind_seq_block p g (joint_fin_step p) →
185    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
186  λp,g.inr ….
187coercion bind_seq_block_from_fin_step :
188  ∀p,g.∀b:bind_seq_block p g (joint_fin_step p).
189    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
190  bind_seq_block_fin_step on _b : bind_seq_block ?? (joint_fin_step ?) to
191    bind_seq_block ?? (joint_step ??) + bind_seq_block ?? (joint_fin_step ?).
192
193definition seq_block_bind_seq_block :
194  ∀p : stmt_params.∀g,A.seq_block p g A → bind_seq_block p g A ≝ λp,g,A.bret ….
195coercion seq_block_to_bind_seq_block :
196  ∀p : stmt_params.∀g,A.∀b:seq_block p g A.bind_seq_block p g A ≝
197  seq_block_bind_seq_block
198  on _b : seq_block ??? to bind_seq_block ???.
199
200definition joint_step_seq_block : ∀p : stmt_params.∀g.joint_step p g → seq_block p g (joint_step p g) ≝
201  λp,g,x.〈[ ], x〉.
202coercion joint_step_to_seq_block : ∀p : stmt_params.∀g.∀b : joint_step p g.seq_block p g (joint_step p g) ≝
203  joint_step_seq_block on _b : joint_step ?? to seq_block ?? (joint_step ??).
204
205definition joint_fin_step_seq_block : ∀p : stmt_params.∀g.joint_fin_step p → seq_block p g (joint_fin_step p) ≝
206  λp,g,x.〈[ ], x〉.
207coercion joint_fin_step_to_seq_block : ∀p : stmt_params.∀g.∀b : joint_fin_step p.seq_block p g (joint_fin_step p) ≝
208  joint_fin_step_seq_block on _b : joint_fin_step ? to seq_block ?? (joint_fin_step ?).
209
210definition seq_list_seq_block :
211  ∀p:stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝
212  λp,g,l.let pr ≝ split_on_last … (NOOP ??) l in 〈\fst pr, \snd pr〉.
213coercion seq_list_to_seq_block :
214  ∀p:stmt_params.∀g.∀l:list (joint_seq p g).seq_block p g (joint_step p g) ≝
215  seq_list_seq_block on _l : list (joint_seq ??) to seq_block ?? (joint_step ??).
216
217definition bind_seq_list_bind_seq_block :
218  ∀p:stmt_params.∀g.bind_new (localsT p) (list (joint_seq p g)) → bind_seq_block p g (joint_step p g) ≝
219  λp,g.m_map ??? (λx : list (joint_seq ??).(x : seq_block ???)).
220
221coercion bind_seq_list_to_bind_seq_block :
222  ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝
223  bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??).
224*)
225
226notation > "x ~❨ B , l ❩~> y 'in' c" with precedence 56 for
227  @{'block_in_code $c $x $B $l $y}.
228 
229notation < "hvbox(x ~❨ B , break l ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
230  @{'block_in_code $c $x $B $l $y}.
231
232notation > "x ~❨ B , l , r ❩~> y 'in' c" with precedence 56 for
233  @{'bind_block_in_code $c $x $B $l $r $y}.
234 
235notation < "hvbox(x ~❨ B , break l , break r ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
236  @{'bind_block_in_code $c $x $B $l $r $y}.
237
238definition step_in_code ≝
239  λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_step p globals.
240  λdst : code_point p.
241  ∃nxt.stmt_at … c src = Some ? (sequential … s nxt) ∧
242       point_of_succ … src nxt = dst.
243
244definition fin_step_in_code ≝
245  λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_fin_step p.
246  stmt_at … c src = Some ? (final … s).
247
248let rec seq_list_in_code p globals (c : codeT p globals)
249  (src : code_point p) (B : list (joint_seq p globals))
250  (l : list (code_point p)) (dst : code_point p) on B : Prop ≝
251  match B with
252  [ nil ⇒ l = [ ] ∧ src = dst
253  | cons hd tl ⇒
254    ∃mid,rest.l = src :: rest ∧
255    step_in_code …  c src hd mid ∧
256    seq_list_in_code … c mid tl rest dst
257  ].
258
259(* leaving it out because it can be misleading
260interpretation "step list in code" 'block_in_code c x B l y = (step_list_in_code ?? c x B l y).
261*)
262
263lemma seq_list_in_code_ne : ∀p,globals.∀c : codeT p globals.∀src,B,l,dst.
264  not_empty ? B →
265  seq_list_in_code … c src B l dst →
266  ∃post.l = src :: post.
267#p #globals #c #src * [ #l #dst * ] #hd #tl #l #dst #_ * #mid * #post ** #EQl #_ #_ %{EQl} qed.
268(* #b lapply src -src elim b -b [ #src #l #dst * ]
269#hd * [2: #hd' #tl ] #IH #src * [1,3: #dst #_ * ]
270#mid * [ #dst #_ ** #EQ destruct #_ * |4: #mid' #tl #dst #_ ** #_ #_ * ]
271[2: #dst #_ ** #EQ destruct normalize nodelta #_ #_ %{[ ]} % ]
272#mid' #rest #dst #_ ** #EQ destruct #H1 #H2
273cases (IH … I H2) #post normalize nodelta #EQ destruct %{(mid' :: post)} %
274qed.
275*)
276
277lemma seq_list_in_code_append :
278  ∀p,globals.∀c : codeT p globals.∀src,B1,l1,mid,B2,l2,dst.
279  seq_list_in_code … c src B1 l1 mid →
280  seq_list_in_code … c mid B2 l2 dst →
281  seq_list_in_code … c src (B1@B2) (l1@l2) dst.
282#p #globals #c #src #B1 lapply src -src elim B1 -B1
283[ #src #l1 #mid #B2 #l2 #dst * #EQ1 #EQ2 destruct #H @H
284| #hd #tl #IH #src #l1 #mid #B2 #l2 #dst * #mid' * #rest **
285  #EQ destruct #H1 #H2 #H3 %{mid'} %{(rest@l2)} %{(IH … H2 H3)} %{H1} %
286]
287qed.
288
289lemma seq_list_in_code_append_inv :
290  ∀p,globals.∀c : codeT p globals.∀src,B1,B2,l,dst.
291  seq_list_in_code … c src (B1@B2) l dst →
292  ∃l1,mid,l2.l = l1 @ l2 ∧ seq_list_in_code … c src B1 l1 mid ∧
293  seq_list_in_code … c mid B2 l2 dst.
294#p #globals #c #src #B1 lapply src -src elim B1 -B1
295[ #src #B2 #l #dst #H %{[ ]} %{src} %{l} %{H} % % %
296| #hd #tl #IH #src #B2 #l2 #dst * #mid * #rest ** #EQ destruct
297  #H1 #H2 elim (IH … H2) #l1 * #mid' * #l2 ** #EQ destruct #G1 #G2
298  %{(src::l1)} %{mid'} %{l2} %{G2} %{(refl …)} % [| %[| %{G1} %{H1} % ]]
299]
300qed.
301
302definition map_eval : ∀X,Y : Type[0].list (X → Y) → X → list Y ≝ λX,Y,l,x.map … (λf.f x) l.
303
304definition step_block_in_code ≝
305  λp,g.λc : codeT p g.λsrc.λb : step_block p g.λl,dst.
306  let pref ≝ \fst (\fst b) in
307  let stp ≝ \snd (\fst b) in
308  let post ≝ \snd b in
309  ∃l1,mid1,mid2,l2.
310  l = l1 @ mid1 :: l2 ∧
311  seq_list_in_code ?? c src (map_eval … pref mid1) l1 mid1 ∧
312  step_in_code ?? c mid1 (stp mid1) mid2 ∧
313  seq_list_in_code ?? c mid2 post l2 dst.
314
315lemma map_compose : ∀X,Y,Z,f,g.∀l : list X.map Y Z f (map X Y g l) = map … (f∘g) l.
316#X #Y #Z #f #g #l elim l -l normalize // qed.
317
318lemma map_ext_eq : ∀X,Y,f,g.∀l : list X.(∀x.f x = g x) → map X Y f l = map X Y g l.
319#X #Y #f #g #l #H elim l -l normalize // qed.
320
321lemma map_id : ∀X.∀l : list X.map X X (λx.x) l = l.
322#X #l elim l -l normalize // qed.
323
324definition fin_block_in_code ≝
325  λp,g.λc:codeT p g.λsrc.λB : fin_block p g.λl.λdst : unit.
326  ∃pref,mid.l = pref @ [mid] ∧
327  seq_list_in_code … c src (\fst B) pref mid ∧ fin_step_in_code … c mid (\snd B).
328
329interpretation "step block in code" 'block_in_code c x B l y = (step_block_in_code ?? c x B l y).
330interpretation "fin block in code" 'block_in_code c x B l y = (fin_block_in_code ?? c x B l y).
331
332lemma coerced_step_list_in_code :
333∀p : params.∀g,c,src.∀b : list (joint_seq p g).∀l,dst.
334src ~❨b, l❩~> dst in c →
335match b with
336[ nil ⇒ step_in_code … c src (NOOP …) dst
337| _ ⇒ seq_list_in_code … c src b l dst
338].
339#p #g #c #src @list_elim_left [2: #last #pref #_ ] #l #dst
340[2: * #pref * #mid1 * #mid2 * #post *** #EQ * #EQ' #EQ''
341  #H * #EQ''' #EQ'''' destruct @H ]
342whd in ⊢ (?????%??→?); >split_on_last_hit normalize nodelta
343*#l1*#mid1*#mid2*#l2*** #EQ1
344whd in match map_eval; whd in match add_dummy_variance; normalize nodelta
345>map_compose >map_id #pref_in_code #last_in_code * #EQ2 #EQ3 destruct
346cut (∃hd,tl.pref@[last] = hd::tl)
347[ cases pref [ %{last} %{[ ]} % | #hd #tl %{hd} %{(tl@[last])} % ]] * #hd * #tl
348#EQ >EQ in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]); normalize nodelta -hd -tl
349@(seq_list_in_code_append … pref_in_code)
350%[| %[| % [2: %%] %{last_in_code} % ]]
351qed.
352
353let rec bind_new_instantiates B X
354  (x : X) (b : bind_new B X) (l : list B) on b : Prop ≝
355  match b with
356  [ bret B ⇒
357    match l with
358    [ nil ⇒ x = B
359    | _ ⇒ False
360    ]
361  | bnew f ⇒
362    match l with
363    [ nil ⇒ False
364    | cons r l' ⇒
365      bind_new_instantiates B X x (f r) l'
366    ]
367  ].
368
369definition bind_step_block_in_code ≝
370  λp,g.λc:codeT p g.λsrc.λB : bind_step_block p g.λlbls,regs.λdst.
371  ∃b.bind_new_instantiates … b B regs ∧ src ~❨b, lbls❩~> dst in c.
372
373definition bind_fin_block_in_code ≝
374  λp,g.λc:codeT p g.λsrc.λB : bind_fin_block p g.λlbls,regs.λdst.
375  ∃b.bind_new_instantiates … b B regs ∧ src ~❨b, lbls❩~> dst in c.
376
377interpretation "bound step block in code" 'bind_block_in_code c x B l r y = (bind_step_block_in_code ?? c x B l r y).
378interpretation "bound fin block in code" 'bind_block_in_code c x B l r y = (bind_fin_block_in_code ?? c x B l r y).
379
380(* generates ambiguity even if it shouldn't
381interpretation "seq block step in code" 'block_in_code c x B l y = (seq_block_step_in_code ?? c x B l y).
382interpretation "seq block fin step in code" 'block_in_code c x B l y = (seq_block_fin_step_in_code ?? c x B l y).
383*)
384
385(*
386
387definition seq_block_append :
388  ∀p,g.
389  ∀b1 : Σb.is_safe_block p g b.
390  ∀b2 : seq_block p g.
391  seq_block p g ≝ λp,g,b1,b2.
392  〈match b1 with
393  [ mk_Sig instr prf ⇒
394    match \snd instr return λx.bool_to_Prop (is_inl … x) ∧ seq_or_fin_step_classifier … x = ? → ? with
395    [ inl i ⇒ λprf.\fst b1 @ i :: \fst b2
396    | inr _ ⇒ λprf.⊥
397    ] prf
398  ],\snd b2〉.
399  cases prf #H1 #H2 assumption
400  qed.
401
402definition other_block_append :
403  ∀p,g.
404  (Σb.block_classifier ?? b = cl_other) →
405  other_block p g →
406  other_block p g ≝ λp,g,b1,b2.
407  〈\fst b1 @ «\snd b1, pi2 … b1» :: \fst b2, \snd b2〉.
408
409definition seq_block_cons : ∀p : stmt_params.∀g.(Σs.step_classifier p g s = cl_other) →
410  seq_block p g → seq_block p g ≝
411  λp,g,x,b.〈x :: \fst b,\snd b〉.
412definition other_block_cons : ∀p,g.
413  (Σs.seq_or_fin_step_classifier p g s = cl_other) → other_block p g →
414  other_block p g ≝
415  λp,g,x,b.〈x :: \fst b,\snd b〉.
416
417interpretation "seq block cons" 'cons x b = (seq_block_cons ?? x b).
418interpretation "other block cons" 'vcons x b = (other_block_cons ?? x b).
419interpretation "seq block append" 'append b1 b2 = (seq_block_append ?? b1 b2).
420interpretation "other block append" 'vappend b1 b2 = (other_block_append ?? b1 b2).
421
422definition step_to_block : ∀p,g.
423  seq_or_fin_step p g → seq_block p g ≝ λp,g,s.〈[ ], s〉.
424
425coercion block_from_step : ∀p,g.∀s : seq_or_fin_step p g.
426  seq_block p g ≝ step_to_block on _s : seq_or_fin_step ?? to seq_block ??.
427
428definition bind_seq_block_cons :
429  ∀p : stmt_params.∀g,is_seq.
430  (Σs.step_classifier p g s = cl_other) → bind_seq_block p g is_seq →
431  bind_seq_block p g is_seq ≝
432  λp,g,is_seq,x.m_map ??? (λb.〈x::\fst b,\snd b〉).
433
434definition bind_other_block_cons :
435  ∀p,g.(Σs.seq_or_fin_step_classifier p g s = cl_other) → bind_other_block p g → bind_other_block p g ≝
436  λp,g,x.m_map … (other_block_cons … x).
437
438let rec bind_pred_aux B X (P : X → Prop) (c : bind_new B X) on c : Prop ≝
439  match c with
440  [ bret x ⇒ P x
441  | bnew f ⇒ ∀b.bind_pred_aux B X P (f b)
442  ].
443
444let rec bind_pred_inj_aux B X (P : X → Prop) (c : bind_new B X) on c :
445  bind_pred_aux B X P c → bind_new B (Σx.P x) ≝
446  match c return λx.bind_pred_aux B X P x → bind_new B (Σx.P x) with
447  [ bret x ⇒ λprf.return «x, prf»
448  | bnew f ⇒ λprf.bnew … (λx.bind_pred_inj_aux B X P (f x) (prf x))
449  ].
450
451definition bind_pred ≝ λB.
452  mk_InjMonadPred (BindNew B)
453    (mk_MonadPred ?
454      (bind_pred_aux B)
455      ???)
456    (λX,P,c_sig.bind_pred_inj_aux B X P c_sig (pi2 … c_sig))
457    ?.
458[ #X #P #Q #H #y elim y [ #x @H | #f #IH #G #b @IH @G]
459| #X #Y #Pin #Pout #m elim m [#x | #f #IH] #H #g #G [ @G @H | #b @(IH … G) @H]
460| #X #P #x #Px @Px
461| #X #P * #m elim m [#x | #f #IH] #H [ % | @bnew_proper #b @IH]
462]
463qed.
464
465definition bind_seq_block_append :
466  ∀p,g,is_seq.(Σb : bind_seq_block p g true.bind_pred ? (λb.step_classifier p g (\snd b) = cl_other) b) →
467  bind_seq_block p g is_seq → bind_seq_block p g is_seq ≝
468  λp,g,is_seq,b1,b2.
469    !«p, prf» ← mp_inject … b1;
470    !〈post, last〉 ← b2;
471    return 〈\fst p @ «\snd p, prf» :: post, last〉.
472
473definition bind_other_block_append :
474  ∀p,g.(Σb : bind_other_block p g.bind_pred ?
475    (λx.block_classifier ?? x = cl_other) b) →
476  bind_other_block p g → bind_other_block p g ≝
477  λp,g,b1.m_bin_op … (other_block_append ??) (mp_inject … b1).
478
479interpretation "bind seq block cons" 'cons x b = (bind_seq_block_cons ??? x b).
480interpretation "bind other block cons" 'vcons x b = (bind_other_block_cons ?? x b).
481interpretation "bind seq block append" 'append b1 b2 = (bind_seq_block_append ??? b1 b2).
482interpretation "bind other block append" 'vappend b1 b2 = (bind_other_block_append ?? b1 b2).
483
484let rec instantiates_to B X
485  (b : bind_new B X) (l : list B) (x : X) on b : Prop ≝
486  match b with
487  [ bret B ⇒
488    match l with
489    [ nil ⇒ x = B
490    | _ ⇒ False
491    ]
492  | bnew f ⇒
493    match l with
494    [ nil ⇒ False
495    | cons r l' ⇒
496      instantiates_to B X (f r) l' x
497    ]
498  ].
499
500lemma instantiates_to_bind_pred :
501  ∀B,X,P,b,l,x.instantiates_to B X b l x → bind_pred B P b → P x.
502#B #X #P #b elim b
503[ #x * [ #y #EQ >EQ normalize // | #hd #tl #y *]
504| #f #IH * [ #y * | #hd #tl normalize #b #H #G @(IH … H) @G ]
505]
506qed.
507
508lemma seq_block_append_proof_irr :
509  ∀p,g,b1,b1',b2.pi1 ?? b1 = pi1 ?? b1' →
510    seq_block_append p g b1 b2 = seq_block_append p g b1' b2.
511#p #g * #b1 #b1prf * #b1' #b1prf' #b2 #EQ destruct(EQ) %
512qed.
513
514lemma other_block_append_proof_irr :
515  ∀p,g,b1,b1',b2.pi1 ?? b1 = pi1 ?? b1' →
516  other_block_append p g b1 b2 = other_block_append p g b1' b2.
517#p #g * #b1 #b1prf * #b1' #b1prf' #b2 #EQ destruct(EQ) %
518qed.
519
520(*
521lemma is_seq_block_instance_append : ∀p,g,is_seq.
522  ∀B1.
523  ∀B2 : bind_seq_block p g is_seq.
524  ∀l1,l2.
525  ∀b1 : Σb.is_safe_block p g b.
526  ∀b2 : seq_block p g.
527  instantiates_to ? (seq_block p g) B1 l1 (pi1 … b1) →
528  instantiates_to ? (seq_block p g) B2 l2 b2 →
529  instantiates_to ? (seq_block p g) (B1 @ B2) (l1 @ l2) (b1 @ b2).
530#p #g * #B1 elim B1 -B1
531[ #B1 | #f1 #IH1 ]
532#B1prf whd in B1prf;
533#B2 * [2,4: #r1 #l1' ] #l2 #b1 #b2 [1,4: *]
534whd in ⊢ (%→?);
535[ @IH1
536| #EQ destruct(EQ) lapply b2 -b2 lapply l2 -l2 elim B2 -B2
537  [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2 [1,4: *]
538  whd in ⊢ (%→?);
539  [ @IH2
540  | #EQ' whd destruct @seq_block_append_proof_irr %
541  ]
542]
543qed.
544
545lemma is_other_block_instance_append : ∀p,g.
546  ∀B1 : Σb.bind_pred ? (λx.block_classifier p g x = cl_other) b.
547  ∀B2 : bind_other_block p g.
548  ∀l1,l2.
549  ∀b1 : Σb.block_classifier p g b = cl_other.
550  ∀b2 : other_block p g.
551  instantiates_to ? (other_block p g) B1 l1 (pi1 … b1) →
552  instantiates_to ? (other_block p g) B2 l2 b2 →
553  instantiates_to ? (other_block p g) (B1 @@ B2) (l1 @ l2) (b1 @@ b2).
554#p #g * #B1 elim B1 -B1
555[ #B1 | #f1 #IH1 ]
556#B1prf whd in B1prf;
557#B2 * [2,4: #r1 #l1' ] #l2 #b1 #b2 [1,4: *]
558whd in ⊢ (%→?);
559[ @IH1
560| #EQ destruct(EQ) lapply b2 -b2 lapply l2 -l2 elim B2 -B2
561  [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2 [1,4: *]
562  whd in ⊢ (%→?);
563  [ @IH2
564  | #EQ' whd destruct @other_block_append_proof_irr %
565  ]
566]
567qed.
568
569lemma other_fin_step_has_one_label :
570  ∀p,g.∀s:(Σs.fin_step_classifier p g s = cl_other).
571  match fin_step_labels ?? s with
572  [ nil ⇒ False
573  | cons _ tl ⇒
574    match tl with
575    [ nil ⇒ True
576    | _ ⇒ False
577    ]
578  ].
579#p #g ** [#lbl || #ext]
580normalize
581[3: cases (ext_fin_step_flows p ext)
582  [* [2: #lbl' * [2: #lbl'' #tl']]] normalize nodelta ]
583#EQ destruct %
584qed.
585
586definition label_of_other_fin_step : ∀p,g.
587  (Σs.fin_step_classifier p g s = cl_other) → label ≝
588λp,g,s.
589match fin_step_labels p ? s return λx.match x with [ nil ⇒ ? | cons _ tl ⇒ ?] → ? with
590[ nil ⇒ Ⓧ
591| cons lbl tl ⇒ λ_.lbl
592] (other_fin_step_has_one_label p g s).
593
594(*
595definition point_seq_transition : ∀p,g.codeT p g →
596  code_point p → code_point p → Prop ≝
597  λp,g,c,src,dst.
598  match stmt_at … c src with
599  [ Some stmt ⇒ match stmt with
600    [ sequential sq nxt ⇒
601      point_of_succ … src nxt = dst
602    | final fn ⇒
603      match fin_step_labels … fn with
604      [ nil ⇒ False
605      | cons lbl tl ⇒
606        match tl with
607        [ nil ⇒ point_of_label … c lbl = Some ? dst
608        | _ ⇒ False
609        ]
610      ]
611    ]
612  | None ⇒ False
613  ].
614
615lemma point_seq_transition_label_of_other_fin_step :
616  ∀p,c,src.∀s : (Σs.fin_step_classifier p s = cl_other).∀dst.
617  stmt_at ?? c src = Some ? s →
618  point_seq_transition p c src dst →
619  point_of_label … c (label_of_other_fin_step p s) = Some ? dst.
620#p #c #src ** [#lbl || #ext] #EQ1
621#dst #EQ2
622whd in match point_seq_transition; normalize nodelta
623>EQ2 normalize nodelta whd in ⊢ (?→??(????%)?);
624[#H @H | * ]
625lapply (other_fin_step_has_one_label ? «ext,?»)
626cases (fin_step_labels p ? ext) normalize nodelta [*]
627#hd * normalize nodelta [2: #_ #_ *] *
628#H @H
629qed.
630
631lemma point_seq_transition_succ :
632  ∀p,c,src.∀s,nxt.∀dst.
633  stmt_at ?? c src = Some ? (sequential ?? s nxt) →
634  point_seq_transition p c src dst →
635  point_of_succ … src nxt = dst.
636#p #c #src #s #nxt #dst #EQ
637whd in match point_seq_transition; normalize nodelta
638>EQ normalize nodelta #H @H
639qed.
640*)
641
642definition if_other : ∀p,g.∀A : Type[2].seq_or_fin_step p g → A → A → A ≝
643  λp,g,A,c.match seq_or_fin_step_classifier p g c with
644  [ cl_other ⇒ λx,y.x
645  | _ ⇒ λx,y.y
646  ].
647
648definition other_step_in_code ≝
649  λp,g.
650  λc : codeT p g.
651  λsrc : code_point p.
652  λs : seq_or_fin_step p g.
653  match s return λx.if_other p g ? x (code_point p) unit → Prop with
654  [ inl s'' ⇒ λdst.∃n.stmt_at … c src = Some ? (sequential … s'' n) ∧ ?
655  | inr s'' ⇒ λdst.stmt_at … c src = Some ? (final … s'') ∧ ?
656  ].
657  [ whd in dst; cases (seq_or_fin_step_classifier ???) in dst;
658    normalize nodelta [1,2,3: #_ @True |*: #dst
659      @(point_of_succ … src n = dst)]
660  | whd in dst;
661    lapply dst -dst
662    lapply (refl … (seq_or_fin_step_classifier ?? (inr … s'')))
663    cases (seq_or_fin_step_classifier ?? (inr … s'')) in ⊢ (???%→%);
664    normalize nodelta
665    [1,2,3: #_ #_ @True
666    |*: #EQ #dst
667      @(point_of_label … c (label_of_other_fin_step p g «s'', EQ») = Some ? dst)
668    ]
669  ]
670qed.
671
672definition if_other_sig :
673  ∀p,g.∀B,C : Type[0].∀s : Σs.seq_or_fin_step_classifier p g s = cl_other.
674  if_other p g ? s B C → B ≝
675  λp,g,B,C.?.
676  ** #s whd in match (if_other ??????);
677  cases (seq_or_fin_step_classifier ???) normalize nodelta #EQ destruct(EQ)
678  #x @x
679qed.
680
681definition if_other_block_sig :
682  ∀p,g.∀B,C : Type[0].∀b : Σb.block_classifier p g b = cl_other.
683  if_other p g ? (\snd b) B C → B ≝
684  λp,g,B,C.?.
685  ** #l #s
686  #prf #x @(if_other_sig ???? «s, prf» x)
687qed.
688
689coercion other_sig_to_if nocomposites:
690  ∀p,g.∀B,C : Type[0].∀s : Σs.seq_or_fin_step_classifier p g s = cl_other.
691  ∀x : if_other p g ? s B C.B ≝ if_other_sig
692  on _x : if_other ?? Type[0] ??? to ?.
693
694coercion other_block_sig_to_if nocomposites:
695  ∀p,g.∀B,C : Type[0].∀s : Σs.block_classifier p g s = cl_other.
696  ∀x : if_other p g ? (\snd s) B C.B ≝ if_other_block_sig
697  on _x : if_other ?? Type[0] (\snd ?) ?? to ?.
698
699let rec other_list_in_code p g (c : codeT p g)
700  src
701  (b : list (Σs.seq_or_fin_step_classifier p g s = cl_other))
702  dst on b : Prop ≝
703  match b with
704  [ nil ⇒ src = dst
705  | cons hd tl ⇒ ∃mid.
706    other_step_in_code p g c src hd mid ∧ other_list_in_code p g c mid tl dst
707  ].
708
709notation > "x ~❨ B ❩~> y 'in' c" with precedence 56 for
710  @{'block_in_code $c $x $B $y}.
711 
712notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
713  @{'block_in_code $c $x $B $y}.
714
715interpretation "list in code" 'block_in_code c x B y =
716  (other_list_in_code ?? c x B y).
717
718definition other_block_in_code : ∀p,g.codeT p g →
719  code_point p → ∀b : other_block p g.
720    if_other … (\snd b) (code_point p) unit → Prop ≝
721  λp,g,c,src,b,dst.
722  ∃mid.src ~❨\fst b❩~> mid in c ∧
723  other_step_in_code p g c mid (\snd b) dst.
724
725interpretation "block in code" 'block_in_code c x B y =
726  (other_block_in_code ?? c x B y).
727
728lemma other_list_in_code_append : ∀p,g.∀c : codeT p g.
729  ∀x.∀b1 : list ?.
730  ∀y.∀b2 : list ?.∀z.
731  x ~❨b1❩~> y in c→ y ~❨b2❩~> z in c → x ~❨b1@b2❩~> z in c.
732#p#g#c#x#b1 lapply x -x
733elim b1 [2: ** #hd #hd_prf #tl #IH] #x #y #b2 #z
734[3: #EQ normalize in EQ; destruct #H @H]
735* #mid * normalize nodelta [ *#n ] #H1 #H2 #H3
736whd normalize nodelta %{mid}
737%{(IH … H2 H3)}
738[ %{n} ] @H1
739qed.
740
741lemma other_block_in_code_append : ∀p,g.∀c : codeT p g.∀x.
742  ∀B1 : Σb.block_classifier p g b = cl_other.
743  ∀y.
744  ∀B2 : other_block p g.
745  ∀z.
746  x ~❨B1❩~> y in c → y ~❨B2❩~> z in c →
747  x ~❨B1@@B2❩~> z in c.
748#p#g#c #x ** #hd1 *#tl1 #tl1prf
749#y * #hd2 #tl2 #z
750* #mid1 * #H1 #H2
751* #mid2 * #G1 #G2
752%{mid2} %{G2}
753whd in match (\fst ?);
754@(other_list_in_code_append … H1)
755%{y} %{H2 G1}
756qed.
757
758(*
759definition instr_block_in_function :
760  ∀p : evaluation_params.∀fn : joint_internal_function (globals p) p.
761    code_point p →
762    ∀b : bind_other_block p.
763    ? → Prop ≝
764 λp,fn,src,B,dst.
765 ∃vars,B'.
766  All ? (In ? (joint_if_locals … fn)) vars ∧
767  instantiates_to … B vars B' ∧
768  src ~❨B'❩~> dst in joint_if_code … fn.
769
770interpretation "bind block in function" 'block_in_code fn x B y =
771  (instr_block_in_function ? fn x B y).
772
773lemma instr_block_in_function_trans :
774  ∀p,fn,src.
775  ∀B1 : ΣB.bind_pred ? (λb.block_classifier p b = cl_other) B.
776  ∀mid.
777  ∀B2 : bind_other_block p.
778  ∀dst.
779  src ~❨B1❩~> Some ? mid in fn →
780  mid ~❨B2❩~> dst in fn →
781  src ~❨B1@@B2❩~> dst in fn.
782#p#fn#src*#B1#B1prf#mid#B2#dst
783* #vars1 * #b1 ** #vars1_ok #b1B1 #b1_in
784* #vars2 * #b2 ** #vars2_ok #b2B2 #b2_in
785%{(vars1@vars2)} %{(«b1,instantiates_to_bind_pred … b1B1 B1prf» @@ b2)}
786/4 by All_append, conj, is_other_block_instance_append, other_block_in_code_append/
787qed.
788*)
789*)
790*)
Note: See TracBrowser for help on using the repository browser.