source: src/joint/blocks.ma @ 2599

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