source: src/joint/blocks.ma @ 2125

Last change on this file since 2125 was 2042, checked in by sacerdot, 7 years ago

Repaired (Type => DeqSet?)

File size: 9.1 KB
Line 
1include "joint/Joint_paolo.ma".
2include "utilities/bind_new.ma".
3
4definition uncurry_helper : ∀A,B,C : Type[0].(A → B → C) → (A×B) → C ≝
5  λA,B,C,f,p.f (\fst p) (\snd p).
6
7inductive stmt_type : Type[0] ≝
8  | SEQ : stmt_type
9  | FIN : stmt_type.
10
11definition stmt_type_if : ∀A : Type[1].stmt_type → A → A → A ≝
12  λA,t,x,y.match t with [ SEQ ⇒ x | FIN ⇒ y ].
13
14definition block_cont ≝ λp : params.λglobals,ty.
15  (list (joint_step p globals)) ×
16    (stmt_type_if ? ty (joint_step p) (joint_fin_step p) globals).
17
18definition Skip : ∀p,globals.block_cont p globals SEQ ≝
19  λp,globals.〈[ ], NOOP …〉.
20
21definition instr_block ≝ λp : params.λglobals,ty.
22  bind_new (localsT p) (block_cont p globals ty).
23unification hint 0 ≔ p, globals, ty;
24B ≟ block_cont p globals ty, R ≟ localsT p
25(*---------------------------------------*)⊢
26instr_block p globals ty ≡ bind_new R B.
27
28definition block_cont_append :
29  ∀p,g,ty.
30  ∀b1 : block_cont p g SEQ.
31  ∀b2 : block_cont p g ty.
32  block_cont p g ty ≝
33  λp,globals,ty,b1,b2.〈\fst b1 @ \snd b1 :: \fst b2, \snd b2〉.
34
35definition block_cont_cons ≝ λp,g,ty,x.λb : block_cont p g ty.〈x :: \fst b,\snd b〉.
36
37interpretation "block contents cons" 'cons x b = (block_cont_cons ??? x b).
38interpretation "block contents append" 'append b1 b2 = (block_cont_append ??? b1 b2).
39
40definition step_to_block : ∀p : params.∀g.
41  joint_step p g → block_cont p g SEQ ≝ λp,g,s.〈[ ], s〉.
42
43definition fin_step_to_block : ∀p : params.∀g.
44  joint_fin_step p g → block_cont p g FIN ≝ λp,g,s.〈[ ], s〉.
45
46coercion block_from_step : ∀p : params.∀g.∀s : joint_step p g.
47  block_cont p g SEQ ≝ step_to_block on _s : joint_step ?? to block_cont ?? SEQ.
48
49coercion block_from_fin_step : ∀p : params.∀g.∀s : joint_fin_step p g.
50  block_cont p g FIN ≝ fin_step_to_block
51  on _s : joint_fin_step ?? to block_cont ?? FIN.
52
53definition block_cons :
54  ∀p : params.∀globals,ty.
55  joint_step p globals → instr_block p globals ty → instr_block p globals ty
56  ≝ λp,globals,ty,x.m_map … (block_cont_cons … x).
57
58definition block_append :
59  ∀p : params.∀globals,ty.
60  instr_block p globals SEQ → instr_block p globals ty → instr_block p globals ty ≝
61  λp,globals,ty.m_bin_op … (block_cont_append …).
62
63interpretation "instruction block cons" 'cons x b = (block_cons ??? x b).
64interpretation "instruction block append" 'append b1 b2 = (block_append ??? b1 b2).
65
66let rec is_block_instance (p : params) g ty (b : instr_block p g ty) (l : list (localsT p)) (b' : block_cont p g ty) on b : Prop ≝
67  match b with
68  [ bret B ⇒
69    match l with
70    [ nil ⇒ B = b'
71    | cons _ _ ⇒ False
72    ]
73  | bnew f ⇒
74    match l with
75    [ nil ⇒ False
76    | cons r l' ⇒
77      is_block_instance p g ty (f r) l' b'
78    ]
79  ].
80
81lemma is_block_instance_append : ∀p,globals,ty,b1,b2,l1,l2,b1',b2'.
82  is_block_instance p globals SEQ b1 l1 b1' →
83  is_block_instance p globals ty b2 l2 b2' →
84  is_block_instance p globals ty (b1 @ b2) (l1 @ l2) (b1' @ b2').
85#p#globals#ty #b1 elim b1
86[ #B1 | #f1 #IH1 ] #b2 * [2,4: #r1 #l1' ] #l2 #b1' #b2' [1,4: *]
87normalize in ⊢ (%→?);
88[ @IH1
89| #EQ destruct(EQ) lapply b2' -b2' lapply l2 -l2 elim b2
90  [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2' [1,4: *]
91  normalize in ⊢ (%→?); [2: //] #H2
92  change with (is_block_instance ??? ('new ?) (r2 :: ?) ?) whd
93  @(IH2 … H2)
94]
95qed.
96
97definition tunnel_step : ∀p,g.codeT p g → relation (code_point p) ≝
98  λp,g,c,x,y.∃l.stmt_at … c x = Some ? (GOTO … l) ∧ point_of_label … c l = Some ? y.
99
100notation > "x ~~> y 'in' c" with precedence 56 for @{'tunnel_step $c $x $y}.
101notation < "hvbox(x ~~> y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_step $c $x $y}.
102interpretation "tunnel step in code" 'tunnel_step c x y = (tunnel_step ?? c x y).
103
104let rec tunnel_through p g (c : codeT p g) x through y on through : Prop ≝
105  match through with
106  [ nil ⇒ x = y
107  | cons hd tl ⇒ x ~~> hd in c ∧ tunnel_through … hd tl y
108  ].
109
110definition tunnel ≝ λp,g,c,x,y.∃through.tunnel_through p g c x through y.
111
112notation > "x ~~>^* y 'in' c" with precedence 56 for @{'tunnel $c $x $y}.
113notation < "hvbox(x \nbsp ~~>^* \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel $c $x $y}.
114interpretation "tunnel in code" 'tunnel c x y = (tunnel ?? c x y).
115
116lemma tunnel_refl : ∀p,g.∀c : codeT p g.reflexive ? (tunnel p g c).
117#p #g #c #x %{[]} % qed.
118
119lemma tunnel_trans : ∀p,g.∀c : codeT p g.
120  transitive ? (tunnel p g c).
121#p#g#c #x#y#z * #l1 #H1 * #l2 #H2 %{(l1@l2)}
122lapply H1 -H1 lapply x -x elim l1 -l1
123[ #x #H1 >H1 @H2
124| #hd #tl #IH #x * #H11 #H12
125  %{H11} @IH @H12
126] qed.
127 
128definition tunnel_plus ≝ λp,g.λc : codeT p g.λx,y.
129  ∃mid.x ~~> mid in c ∧ mid ~~>^* y in c.
130
131notation > "x ~~>^+ y 'in' c" with precedence 56 for @{'tunnel_plus $c $x $y}.
132notation < "hvbox(x \nbsp ~~>^+ \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_plus $c $x $y}.
133interpretation "tunnel in code" 'tunnel_plus c x y = (tunnel_plus ?? c x y).
134
135lemma tunnel_plus_to_star : ∀p,g.∀c : codeT p g.∀x,y.x ~~>^+ y in c → x ~~>^* y in c.
136#p #g #c #x #y * #mid * #H1 * #through #H2 %{(mid :: through)}
137%{H1 H2} qed.
138
139lemma tunnel_plus_trans : ∀p,g.∀c : codeT p g.transitive ? (tunnel_plus p g c).
140#p #g #c #x #y #z * #mid * #H1 #H2
141#H3 %{mid} %{H1} @(tunnel_trans … H2) /2 by tunnel_plus_to_star/
142qed.
143
144lemma tunnel_tunnel_plus : ∀p,g.∀c : codeT p g.∀x,y,z.
145  x ~~>^* y in c → y ~~>^+ z in c → x ~~>^+ z in c.
146#p #g #c #x #y #z * #through
147lapply x -x elim through
148[ #x #H1 >H1 //
149| #hd #tl #IH #x * #H1 #H2 #H3
150  %{hd} %{H1} @(tunnel_trans ???? y)
151  [ %{tl} assumption | /2 by tunnel_plus_to_star/]
152]
153qed.
154
155lemma tunnel_plus_tunnel : ∀p,g.∀c : codeT p g.∀x,y,z.
156  x ~~>^+ y in c → y ~~>^* z in c → x ~~>^+ z in c.
157#p #g #c #x #y #z * #mid * #H1 #H2 #H3 %{mid} %{H1}
158@(tunnel_trans … H2 H3)
159qed.
160
161let rec seq_list_in_code (p : params) g (c : codeT p g)
162  src l dst on l : Prop ≝
163  match l with
164  [ nil ⇒ src = dst
165  | cons hd tl ⇒
166    ∃n.stmt_at … c src = Some ? (sequential … hd n) ∧
167       seq_list_in_code p g c (point_of_succ … src n) tl dst
168  ].
169
170(*
171definition seq_block_cont_to_list : ∀p,g.block_cont p g SEQ → list (joint_step p g) ≝
172  λp,g,b.\fst b @ [\snd b].
173
174coercion list_from_seq_block_cont : ∀p,g.∀b:block_cont p g SEQ.list (joint_step p g) ≝
175  seq_block_cont_to_list on _b : block_cont ?? SEQ to list (joint_step ??).
176*)
177
178definition unit_deqset: DeqSet ≝ mk_DeqSet unit (λ_.λ_.true) ?.
179 * * /2/
180qed.
181
182definition block_cont_in_code : ∀p,g.codeT p g → ∀ty.
183  code_point p → block_cont p g ty → stmt_type_if ? ty (code_point p) unit_deqset → Prop ≝
184  λp,g.λc : codeT p g.λty,src,b,dst.
185  ∃mid.seq_list_in_code p g c src (\fst b) mid ∧
186  match ty
187  return λx.stmt_type_if ? x ??? →
188    stmt_type_if ? x ? unit_deqset → Prop
189  with
190  [ SEQ ⇒ λs,dst.
191      ∃n.stmt_at … c mid = Some ? (sequential … s n) ∧
192         point_of_succ … mid n = dst
193  | FIN ⇒ λs.λ_.stmt_at … c mid = Some ? (final … s)
194  ] (\snd b) dst.
195 
196
197notation > "x ~❨ B ❩~> y 'in' c" with precedence 56 for
198  @{'block_in_code $c $x $B $y}.
199 
200notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
201  @{'block_in_code $c $x $B $y}.
202
203interpretation "block cont in code" 'block_in_code c x B y =
204  (block_cont_in_code ?? c ? x B y).
205
206lemma seq_list_in_code_append : ∀p,g.∀c : codeT p g.∀x,l1,y,l2,z.
207  seq_list_in_code p g c x l1 y →
208  seq_list_in_code p g c y l2 z →
209  seq_list_in_code p g c x (l1@l2) z.
210#p#g#c#x#l1 lapply x -x
211elim l1 [2: #hd #tl #IH] #x #y #l2 #z normalize in ⊢ (%→?);
212[ * #n * #EQ1 #H #G %{n} %{EQ1} @(IH … H G)
213| #EQ destruct(EQ) //
214]
215qed.
216
217lemma block_cont_in_code_append : ∀p,g.∀c : codeT p g.∀ty,x.
218  ∀B1 : block_cont p g SEQ.∀y.∀B2 : block_cont p g ty.∀z.
219  x ~❨B1❩~> y in c → y ~❨B2❩~> z in c → x ~❨B1@B2❩~> z in c.
220#p#g#c #ty #x * whd in match stmt_type_if in ⊢ (?→%→%→?); normalize nodelta
221#l1 #s1 #y * #l2 #s2 #z * normalize nodelta
222#mid1 * #H1 * #n * #EQ1 #EQ2 * #mid2 * #H2 #H3
223%{mid2} %
224[ whd in match (〈?,?〉@?);
225  @(seq_list_in_code_append … H1)
226  %{n} %{EQ1} >EQ2 assumption
227| assumption
228]
229qed.
230
231definition instr_block_in_function :
232  ∀p,g.∀fn : joint_internal_function g p.∀ty.
233    instr_block p g ty →
234    code_point p →
235    ? → Prop ≝
236 λp,g,fn,ty,B,src,dst.
237 ∃vars,B'.
238  All ? (In ? (joint_if_locals … fn)) vars ∧
239  is_block_instance … B vars B' ∧
240  src ~❨B'❩~> dst in joint_if_code … fn.
241
242interpretation "instr block in function" 'block_in_code fn x B y =
243  (instr_block_in_function ?? fn ? B x y).
244
245lemma instr_block_in_function_trans :
246  ∀p,g.∀fn : joint_internal_function g p.∀ty,src.
247  ∀B1 : instr_block p g SEQ.
248  ∀mid.∀B2 : instr_block p g ty.∀dst.
249  src ~❨B1❩~> mid in fn →
250  mid ~❨B2❩~> dst in fn →
251  src ~❨B1@B2❩~> dst in fn.
252#p#g#fn#ty#src#B1#mid#B2#dst
253* #vars1 * #b1 ** #vars1_ok #b1B1 #b1_in
254* #vars2 * #b2 ** #vars2_ok #b2B2 #b2_in
255%{(vars1@vars2)} %{(b1 @ b2)}
256/4 by All_append, conj, is_block_instance_append, block_cont_in_code_append/
257qed.
Note: See TracBrowser for help on using the repository browser.