source: src/joint/blocks.ma @ 1882

Last change on this file since 1882 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

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