source: src/joint/blocks.ma @ 1908

Last change on this file since 1908 was 1908, checked in by fguidi, 8 years ago

notation fixup following last commit of matita
we shifted the levels of precedence from 50 to 60 up by 5

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 56 for @{'tunnel_step $c $x $y}.
87notation < "hvbox(x ~~> y \nbsp 'in' \nbsp break c)" with precedence 56 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 56 for @{'tunnel $c $x $y}.
99notation < "hvbox(x \nbsp ~~>^* \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 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 56 for @{'tunnel_plus $c $x $y}.
118notation < "hvbox(x \nbsp ~~>^+ \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 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 56 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 56 for
175  @{'block_in_code $c $b $x $B $y}.
176notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 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.