[2286] | 1 | include "joint/Joint.ma". |
---|
[2155] | 2 | include "utilities/bindLists.ma". |
---|
[1882] | 3 | |
---|
[2214] | 4 | (* inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝ |
---|
[2155] | 5 | | block_seq : joint_seq p globals → block_step p globals |
---|
| 6 | | block_skip : label → block_step p globals. |
---|
[1949] | 7 | |
---|
[2155] | 8 | definition 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 | ]. |
---|
[1949] | 13 | |
---|
[2155] | 14 | definition 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 | ]. |
---|
[1949] | 20 | |
---|
[2155] | 21 | definition 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 ??). |
---|
[1949] | 24 | |
---|
[2155] | 25 | coercion 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 ??). |
---|
[1949] | 31 | |
---|
[2155] | 32 | definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with |
---|
| 33 | [ inl _ ⇒ true |
---|
| 34 | | inr _ ⇒ false |
---|
| 35 | ]. |
---|
| 36 | definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with |
---|
| 37 | [ inl _ ⇒ true |
---|
| 38 | | inr _ ⇒ false |
---|
| 39 | ]. |
---|
| 40 | |
---|
| 41 | definition skip_block ≝ λp,globals,A. |
---|
[2214] | 42 | (list (block_step p globals)) × A.*) |
---|
[2155] | 43 | |
---|
| 44 | definition seq_block ≝ λp : stmt_params.λglobals,A. |
---|
| 45 | (list (joint_seq p globals)) × A. |
---|
| 46 | |
---|
[2214] | 47 | (*definition seq_to_skip_block : |
---|
[2155] | 48 | ∀p,g,A.seq_block p g A → skip_block p g A |
---|
| 49 | ≝ λp,g,A,b.〈\fst b, \snd b〉. |
---|
| 50 | |
---|
| 51 | coercion skip_from_seq_block : |
---|
| 52 | ∀p,g,A.∀b : seq_block p g A.skip_block p g A ≝ |
---|
[2214] | 53 | seq_to_skip_block on _b : seq_block ??? to skip_block ???.*) |
---|
[2155] | 54 | |
---|
| 55 | definition bind_seq_block ≝ λp : stmt_params.λglobals,A. |
---|
| 56 | bind_new (localsT p) (seq_block p globals A). |
---|
| 57 | unification hint 0 ≔ p : stmt_params, g, X; |
---|
| 58 | R ≟ localsT p, |
---|
| 59 | P ≟ seq_block p g X |
---|
[1882] | 60 | (*---------------------------------------*)⊢ |
---|
[2155] | 61 | bind_seq_block p g X ≡ bind_new R P. |
---|
[1882] | 62 | |
---|
[2155] | 63 | definition bind_seq_list ≝ λp : stmt_params.λglobals. |
---|
| 64 | bind_new (localsT p) (list (joint_seq p globals)). |
---|
| 65 | unification hint 0 ≔ p : stmt_params, g; |
---|
| 66 | R ≟ localsT p, |
---|
| 67 | S ≟ joint_seq p g, |
---|
| 68 | L ≟ list S |
---|
| 69 | (*---------------------------------------*)⊢ |
---|
| 70 | bind_seq_list p g ≡ bind_new R L. |
---|
[1882] | 71 | |
---|
[2214] | 72 | (*definition bind_skip_block ≝ λp : stmt_params.λglobals,A. |
---|
[2155] | 73 | bind_new (localsT p) (skip_block p globals A). |
---|
| 74 | unification hint 0 ≔ p : stmt_params, g, A; |
---|
| 75 | B ≟ skip_block p g A, R ≟ localsT p |
---|
| 76 | (*---------------------------------------*)⊢ |
---|
| 77 | bind_skip_block p g A ≡ bind_new R B. |
---|
[1882] | 78 | |
---|
[2155] | 79 | definition bind_seq_to_skip_block : |
---|
| 80 | ∀p,g,A.bind_seq_block p g A → bind_skip_block p g A ≝ |
---|
| 81 | λp,g,A.m_map ? (seq_block p g A) (skip_block p g A) |
---|
| 82 | (λx.x). |
---|
[1949] | 83 | |
---|
[2155] | 84 | coercion bind_skip_from_seq_block : |
---|
| 85 | ∀p,g,A.∀b:bind_seq_block p g A.bind_skip_block p g A ≝ |
---|
[2214] | 86 | bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???.*) |
---|
[2155] | 87 | (* |
---|
| 88 | definition block_classifier ≝ |
---|
| 89 | λp,g.λb : other_block p g. |
---|
| 90 | seq_or_fin_step_classifier ?? (\snd b). |
---|
| 91 | *) |
---|
[1949] | 92 | |
---|
[2155] | 93 | let rec split_on_last A (dflt : A) (l : list A) on l : (list A) × A ≝ |
---|
| 94 | match l with |
---|
| 95 | [ nil ⇒ 〈[ ], dflt〉 |
---|
| 96 | | cons hd tl ⇒ |
---|
| 97 | match tl with |
---|
| 98 | [ nil ⇒ 〈[ ], hd〉 |
---|
| 99 | | _ ⇒ |
---|
| 100 | let 〈pref, post〉 ≝ split_on_last A dflt tl in |
---|
| 101 | 〈hd :: pref, post〉 |
---|
| 102 | ] |
---|
| 103 | ]. |
---|
[1949] | 104 | |
---|
[2155] | 105 | lemma split_on_last_ok : |
---|
| 106 | ∀A,dflt,l. |
---|
| 107 | match l with |
---|
| 108 | [ nil ⇒ True |
---|
| 109 | | _ ⇒ l = (let 〈pre, post〉 ≝ split_on_last A dflt l in pre @ [post]) |
---|
| 110 | ]. |
---|
| 111 | #A #dflt #l elim l normalize nodelta |
---|
| 112 | [ % |
---|
| 113 | | #hd * [ #_ %] |
---|
| 114 | #hd' #tl #IH whd in match (split_on_last ???); >IH in ⊢ (??%?); |
---|
| 115 | elim (split_on_last ???) #a #b % |
---|
| 116 | ] |
---|
| 117 | qed. |
---|
[1949] | 118 | |
---|
[2155] | 119 | definition seq_block_from_seq_list : |
---|
| 120 | ∀p : stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝ |
---|
| 121 | λp,g,l.let 〈pre,post〉 ≝ split_on_last … (NOOP ??) l in 〈pre, (post : joint_step ??)〉. |
---|
[1949] | 122 | |
---|
[2155] | 123 | definition bind_seq_block_from_bind_seq_list : |
---|
| 124 | ∀p : stmt_params.∀g.bind_new (localsT p) (list (joint_seq p g)) → |
---|
| 125 | bind_seq_block p g (joint_step p g) ≝ λp.λg.m_map … (seq_block_from_seq_list …). |
---|
[1882] | 126 | |
---|
[2155] | 127 | definition bind_seq_block_step : |
---|
| 128 | ∀p,g.bind_seq_block p g (joint_step p g) → |
---|
| 129 | bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝ |
---|
| 130 | λp,g.inl …. |
---|
| 131 | coercion bind_seq_block_from_step : |
---|
| 132 | ∀p,g.∀b:bind_seq_block p g (joint_step p g). |
---|
| 133 | bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝ |
---|
| 134 | bind_seq_block_step on _b : bind_seq_block ?? (joint_step ??) to |
---|
| 135 | bind_seq_block ?? (joint_step ??) + bind_seq_block ?? (joint_fin_step ?). |
---|
[1882] | 136 | |
---|
[2155] | 137 | definition bind_seq_block_fin_step : |
---|
| 138 | ∀p,g.bind_seq_block p g (joint_fin_step p) → |
---|
| 139 | bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝ |
---|
| 140 | λp,g.inr …. |
---|
| 141 | coercion bind_seq_block_from_fin_step : |
---|
| 142 | ∀p,g.∀b:bind_seq_block p g (joint_fin_step p). |
---|
| 143 | bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝ |
---|
| 144 | bind_seq_block_fin_step on _b : bind_seq_block ?? (joint_fin_step ?) to |
---|
| 145 | bind_seq_block ?? (joint_step ??) + bind_seq_block ?? (joint_fin_step ?). |
---|
[1882] | 146 | |
---|
[2155] | 147 | definition seq_block_bind_seq_block : |
---|
| 148 | ∀p : stmt_params.∀g,A.seq_block p g A → bind_seq_block p g A ≝ λp,g,A.bret …. |
---|
| 149 | coercion seq_block_to_bind_seq_block : |
---|
| 150 | ∀p : stmt_params.∀g,A.∀b:seq_block p g A.bind_seq_block p g A ≝ |
---|
| 151 | seq_block_bind_seq_block |
---|
| 152 | on _b : seq_block ??? to bind_seq_block ???. |
---|
| 153 | |
---|
| 154 | definition joint_step_seq_block : ∀p : stmt_params.∀g.joint_step p g → seq_block p g (joint_step p g) ≝ |
---|
| 155 | λp,g,x.〈[ ], x〉. |
---|
| 156 | coercion joint_step_to_seq_block : ∀p : stmt_params.∀g.∀b : joint_step p g.seq_block p g (joint_step p g) ≝ |
---|
| 157 | joint_step_seq_block on _b : joint_step ?? to seq_block ?? (joint_step ??). |
---|
| 158 | |
---|
| 159 | definition joint_fin_step_seq_block : ∀p : stmt_params.∀g.joint_fin_step p → seq_block p g (joint_fin_step p) ≝ |
---|
| 160 | λp,g,x.〈[ ], x〉. |
---|
| 161 | coercion joint_fin_step_to_seq_block : ∀p : stmt_params.∀g.∀b : joint_fin_step p.seq_block p g (joint_fin_step p) ≝ |
---|
| 162 | joint_fin_step_seq_block on _b : joint_fin_step ? to seq_block ?? (joint_fin_step ?). |
---|
| 163 | |
---|
| 164 | definition seq_list_seq_block : |
---|
| 165 | ∀p:stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝ |
---|
| 166 | λp,g,l.let pr ≝ split_on_last … (NOOP ??) l in 〈\fst pr, \snd pr〉. |
---|
| 167 | coercion seq_list_to_seq_block : |
---|
| 168 | ∀p:stmt_params.∀g.∀l:list (joint_seq p g).seq_block p g (joint_step p g) ≝ |
---|
| 169 | seq_list_seq_block on _l : list (joint_seq ??) to seq_block ?? (joint_step ??). |
---|
| 170 | |
---|
| 171 | definition bind_seq_list_bind_seq_block : |
---|
| 172 | ∀p:stmt_params.∀g.bind_new (localsT p) (list (joint_seq p g)) → bind_seq_block p g (joint_step p g) ≝ |
---|
| 173 | λp,g.m_map ??? (λx : list (joint_seq ??).(x : seq_block ???)). |
---|
| 174 | |
---|
| 175 | coercion bind_seq_list_to_bind_seq_block : |
---|
| 176 | ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝ |
---|
| 177 | bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??). |
---|
| 178 | |
---|
[2186] | 179 | notation > "x ~❨ B , l ❩~> y 'in' c" with precedence 56 for |
---|
| 180 | @{'block_in_code $c $x $B $l $y}. |
---|
| 181 | |
---|
| 182 | notation < "hvbox(x ~❨ B , l ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for |
---|
| 183 | @{'block_in_code $c $x $B $l $y}. |
---|
| 184 | |
---|
| 185 | definition step_in_code ≝ |
---|
| 186 | λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_step p globals. |
---|
| 187 | λdst : code_point p. |
---|
| 188 | ∃nxt.stmt_at … c src = Some ? (sequential … s nxt) ∧ |
---|
| 189 | point_of_succ … src nxt = dst. |
---|
| 190 | |
---|
| 191 | definition fin_step_in_code ≝ |
---|
| 192 | λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_fin_step p. |
---|
| 193 | stmt_at … c src = Some ? (final … s). |
---|
| 194 | |
---|
| 195 | let rec seq_list_in_code p globals (c : codeT p globals) |
---|
| 196 | (src : code_point p) (B : list (joint_seq p globals)) |
---|
| 197 | (l : list (code_point p)) (dst : code_point p) on B : Prop ≝ |
---|
| 198 | match B with |
---|
| 199 | [ nil ⇒ |
---|
| 200 | match l with |
---|
| 201 | [ nil ⇒ src = dst |
---|
| 202 | | _ ⇒ False |
---|
| 203 | ] |
---|
| 204 | | cons hd tl ⇒ |
---|
| 205 | match l with |
---|
| 206 | [ nil ⇒ False |
---|
| 207 | | cons mid rest ⇒ |
---|
| 208 | step_in_code … c src hd mid ∧ seq_list_in_code … c mid tl rest dst |
---|
| 209 | ] |
---|
| 210 | ]. |
---|
| 211 | |
---|
| 212 | interpretation "seq list in code" 'block_in_code c x B l y = (seq_list_in_code ?? c x B l y). |
---|
| 213 | |
---|
| 214 | lemma seq_list_in_code_append : |
---|
| 215 | ∀p,globals.∀c : codeT p globals.∀src,B1,l1,mid,B2,l2,dst. |
---|
| 216 | src ~❨B1,l1❩~> mid in c → mid ~❨B2,l2❩~> dst in c → |
---|
| 217 | src ~❨B1@B2,l1@l2❩~> dst in c. |
---|
| 218 | #p #globals #c #src #B1 lapply src -src elim B1 |
---|
| 219 | [ #src * [2: #mid' #rest] #mid #B2 #l2 #dst [*] #EQ normalize in EQ; destruct(EQ) |
---|
| 220 | #H @H |
---|
| 221 | | #hd #tl #IH #src * [2: #mid' #rest] #mid #B2 #l2 #dst * #H1 #H2 |
---|
| 222 | #H3 %{H1 (IH … H2 H3)} |
---|
| 223 | ] |
---|
| 224 | qed. |
---|
| 225 | |
---|
| 226 | lemma seq_list_in_code_append_inv : |
---|
| 227 | ∀p,globals.∀c : codeT p globals.∀src,B1,B2,l,dst. |
---|
| 228 | src ~❨B1@B2,l❩~> dst in c → |
---|
| 229 | ∃l1,mid,l2.l = l1 @ l2 ∧ src ~❨B1,l1❩~> mid in c ∧ mid ~❨B2,l2❩~> dst in c. |
---|
| 230 | #p #globals #c #src #B1 lapply src -src elim B1 |
---|
| 231 | [ #src #B2 #l #dst #H %{[ ]} %{src} %{l} %{H} % % |
---|
| 232 | | #hd #tl #IH #src #B2 * [2: #mid #rest] #dst * #H1 #H2 |
---|
| 233 | elim (IH … H2) #l1 * #mid' * #l2 ** #G1 #G2 #G3 |
---|
| 234 | %{(mid::l1)} %{mid'} %{l2} %{G3} >G1 %{(refl …)} |
---|
| 235 | %{H1 G2} |
---|
| 236 | ] |
---|
| 237 | qed. |
---|
| 238 | |
---|
| 239 | definition seq_block_step_in_code ≝ |
---|
| 240 | λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_step p g).λl,dst. |
---|
[2422] | 241 | ∃hd,tl.l = hd @ [tl] ∧ |
---|
| 242 | src ~❨\fst B, l❩~> tl in c ∧ step_in_code … c tl (\snd B) dst. |
---|
[2186] | 243 | |
---|
| 244 | definition seq_block_fin_step_in_code ≝ |
---|
| 245 | λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit. |
---|
[2422] | 246 | ∃hd,tl.l = hd @ [tl] ∧ |
---|
| 247 | src ~❨\fst B, l❩~> tl in c ∧ fin_step_in_code … c tl (\snd B). |
---|
[2186] | 248 | |
---|
| 249 | (* generates ambiguity even if it shouldn't |
---|
| 250 | interpretation "seq block step in code" 'block_in_code c x B l y = (seq_block_step_in_code ?? c x B l y). |
---|
| 251 | interpretation "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). |
---|
| 252 | *) |
---|
| 253 | |
---|
[2155] | 254 | (* |
---|
| 255 | |
---|
| 256 | definition seq_block_append : |
---|
| 257 | ∀p,g. |
---|
| 258 | ∀b1 : Σb.is_safe_block p g b. |
---|
| 259 | ∀b2 : seq_block p g. |
---|
| 260 | seq_block p g ≝ λp,g,b1,b2. |
---|
| 261 | 〈match b1 with |
---|
| 262 | [ mk_Sig instr prf ⇒ |
---|
| 263 | match \snd instr return λx.bool_to_Prop (is_inl … x) ∧ seq_or_fin_step_classifier … x = ? → ? with |
---|
| 264 | [ inl i ⇒ λprf.\fst b1 @ i :: \fst b2 |
---|
| 265 | | inr _ ⇒ λprf.⊥ |
---|
| 266 | ] prf |
---|
| 267 | ],\snd b2〉. |
---|
| 268 | cases prf #H1 #H2 assumption |
---|
| 269 | qed. |
---|
| 270 | |
---|
| 271 | definition other_block_append : |
---|
| 272 | ∀p,g. |
---|
| 273 | (Σb.block_classifier ?? b = cl_other) → |
---|
| 274 | other_block p g → |
---|
| 275 | other_block p g ≝ λp,g,b1,b2. |
---|
| 276 | 〈\fst b1 @ «\snd b1, pi2 … b1» :: \fst b2, \snd b2〉. |
---|
| 277 | |
---|
| 278 | definition seq_block_cons : ∀p : stmt_params.∀g.(Σs.step_classifier p g s = cl_other) → |
---|
| 279 | seq_block p g → seq_block p g ≝ |
---|
| 280 | λp,g,x,b.〈x :: \fst b,\snd b〉. |
---|
| 281 | definition other_block_cons : ∀p,g. |
---|
| 282 | (Σs.seq_or_fin_step_classifier p g s = cl_other) → other_block p g → |
---|
| 283 | other_block p g ≝ |
---|
| 284 | λp,g,x,b.〈x :: \fst b,\snd b〉. |
---|
| 285 | |
---|
| 286 | interpretation "seq block cons" 'cons x b = (seq_block_cons ?? x b). |
---|
| 287 | interpretation "other block cons" 'vcons x b = (other_block_cons ?? x b). |
---|
| 288 | interpretation "seq block append" 'append b1 b2 = (seq_block_append ?? b1 b2). |
---|
| 289 | interpretation "other block append" 'vappend b1 b2 = (other_block_append ?? b1 b2). |
---|
| 290 | |
---|
| 291 | definition step_to_block : ∀p,g. |
---|
| 292 | seq_or_fin_step p g → seq_block p g ≝ λp,g,s.〈[ ], s〉. |
---|
| 293 | |
---|
| 294 | coercion block_from_step : ∀p,g.∀s : seq_or_fin_step p g. |
---|
| 295 | seq_block p g ≝ step_to_block on _s : seq_or_fin_step ?? to seq_block ??. |
---|
| 296 | |
---|
| 297 | definition bind_seq_block_cons : |
---|
| 298 | ∀p : stmt_params.∀g,is_seq. |
---|
| 299 | (Σs.step_classifier p g s = cl_other) → bind_seq_block p g is_seq → |
---|
| 300 | bind_seq_block p g is_seq ≝ |
---|
| 301 | λp,g,is_seq,x.m_map ??? (λb.〈x::\fst b,\snd b〉). |
---|
| 302 | |
---|
| 303 | definition bind_other_block_cons : |
---|
| 304 | ∀p,g.(Σs.seq_or_fin_step_classifier p g s = cl_other) → bind_other_block p g → bind_other_block p g ≝ |
---|
| 305 | λp,g,x.m_map … (other_block_cons … x). |
---|
| 306 | |
---|
| 307 | let rec bind_pred_aux B X (P : X → Prop) (c : bind_new B X) on c : Prop ≝ |
---|
| 308 | match c with |
---|
| 309 | [ bret x ⇒ P x |
---|
| 310 | | bnew f ⇒ ∀b.bind_pred_aux B X P (f b) |
---|
| 311 | ]. |
---|
| 312 | |
---|
| 313 | let rec bind_pred_inj_aux B X (P : X → Prop) (c : bind_new B X) on c : |
---|
| 314 | bind_pred_aux B X P c → bind_new B (Σx.P x) ≝ |
---|
| 315 | match c return λx.bind_pred_aux B X P x → bind_new B (Σx.P x) with |
---|
| 316 | [ bret x ⇒ λprf.return «x, prf» |
---|
| 317 | | bnew f ⇒ λprf.bnew … (λx.bind_pred_inj_aux B X P (f x) (prf x)) |
---|
| 318 | ]. |
---|
| 319 | |
---|
| 320 | definition bind_pred ≝ λB. |
---|
| 321 | mk_InjMonadPred (BindNew B) |
---|
| 322 | (mk_MonadPred ? |
---|
| 323 | (bind_pred_aux B) |
---|
| 324 | ???) |
---|
| 325 | (λX,P,c_sig.bind_pred_inj_aux B X P c_sig (pi2 … c_sig)) |
---|
| 326 | ?. |
---|
| 327 | [ #X #P #Q #H #y elim y [ #x @H | #f #IH #G #b @IH @G] |
---|
| 328 | | #X #Y #Pin #Pout #m elim m [#x | #f #IH] #H #g #G [ @G @H | #b @(IH … G) @H] |
---|
| 329 | | #X #P #x #Px @Px |
---|
| 330 | | #X #P * #m elim m [#x | #f #IH] #H [ % | @bnew_proper #b @IH] |
---|
| 331 | ] |
---|
| 332 | qed. |
---|
| 333 | |
---|
| 334 | definition bind_seq_block_append : |
---|
| 335 | ∀p,g,is_seq.(Σb : bind_seq_block p g true.bind_pred ? (λb.step_classifier p g (\snd b) = cl_other) b) → |
---|
| 336 | bind_seq_block p g is_seq → bind_seq_block p g is_seq ≝ |
---|
| 337 | λp,g,is_seq,b1,b2. |
---|
| 338 | !«p, prf» ← mp_inject … b1; |
---|
| 339 | !〈post, last〉 ← b2; |
---|
| 340 | return 〈\fst p @ «\snd p, prf» :: post, last〉. |
---|
| 341 | |
---|
| 342 | definition bind_other_block_append : |
---|
| 343 | ∀p,g.(Σb : bind_other_block p g.bind_pred ? |
---|
| 344 | (λx.block_classifier ?? x = cl_other) b) → |
---|
| 345 | bind_other_block p g → bind_other_block p g ≝ |
---|
| 346 | λp,g,b1.m_bin_op … (other_block_append ??) (mp_inject … b1). |
---|
| 347 | |
---|
| 348 | interpretation "bind seq block cons" 'cons x b = (bind_seq_block_cons ??? x b). |
---|
| 349 | interpretation "bind other block cons" 'vcons x b = (bind_other_block_cons ?? x b). |
---|
| 350 | interpretation "bind seq block append" 'append b1 b2 = (bind_seq_block_append ??? b1 b2). |
---|
| 351 | interpretation "bind other block append" 'vappend b1 b2 = (bind_other_block_append ?? b1 b2). |
---|
| 352 | |
---|
| 353 | let rec instantiates_to B X |
---|
| 354 | (b : bind_new B X) (l : list B) (x : X) on b : Prop ≝ |
---|
[1882] | 355 | match b with |
---|
| 356 | [ bret B ⇒ |
---|
| 357 | match l with |
---|
[2155] | 358 | [ nil ⇒ x = B |
---|
| 359 | | _ ⇒ False |
---|
[1882] | 360 | ] |
---|
| 361 | | bnew f ⇒ |
---|
| 362 | match l with |
---|
| 363 | [ nil ⇒ False |
---|
| 364 | | cons r l' ⇒ |
---|
[2155] | 365 | instantiates_to B X (f r) l' x |
---|
[1882] | 366 | ] |
---|
| 367 | ]. |
---|
| 368 | |
---|
[2155] | 369 | lemma instantiates_to_bind_pred : |
---|
| 370 | ∀B,X,P,b,l,x.instantiates_to B X b l x → bind_pred B P b → P x. |
---|
| 371 | #B #X #P #b elim b |
---|
| 372 | [ #x * [ #y #EQ >EQ normalize // | #hd #tl #y *] |
---|
| 373 | | #f #IH * [ #y * | #hd #tl normalize #b #H #G @(IH … H) @G ] |
---|
| 374 | ] |
---|
| 375 | qed. |
---|
| 376 | |
---|
| 377 | lemma seq_block_append_proof_irr : |
---|
| 378 | ∀p,g,b1,b1',b2.pi1 ?? b1 = pi1 ?? b1' → |
---|
| 379 | seq_block_append p g b1 b2 = seq_block_append p g b1' b2. |
---|
| 380 | #p #g * #b1 #b1prf * #b1' #b1prf' #b2 #EQ destruct(EQ) % |
---|
| 381 | qed. |
---|
| 382 | |
---|
| 383 | lemma other_block_append_proof_irr : |
---|
| 384 | ∀p,g,b1,b1',b2.pi1 ?? b1 = pi1 ?? b1' → |
---|
| 385 | other_block_append p g b1 b2 = other_block_append p g b1' b2. |
---|
| 386 | #p #g * #b1 #b1prf * #b1' #b1prf' #b2 #EQ destruct(EQ) % |
---|
| 387 | qed. |
---|
| 388 | |
---|
| 389 | (* |
---|
| 390 | lemma is_seq_block_instance_append : ∀p,g,is_seq. |
---|
| 391 | ∀B1. |
---|
| 392 | ∀B2 : bind_seq_block p g is_seq. |
---|
| 393 | ∀l1,l2. |
---|
| 394 | ∀b1 : Σb.is_safe_block p g b. |
---|
| 395 | ∀b2 : seq_block p g. |
---|
| 396 | instantiates_to ? (seq_block p g) B1 l1 (pi1 … b1) → |
---|
| 397 | instantiates_to ? (seq_block p g) B2 l2 b2 → |
---|
| 398 | instantiates_to ? (seq_block p g) (B1 @ B2) (l1 @ l2) (b1 @ b2). |
---|
| 399 | #p #g * #B1 elim B1 -B1 |
---|
| 400 | [ #B1 | #f1 #IH1 ] |
---|
| 401 | #B1prf whd in B1prf; |
---|
| 402 | #B2 * [2,4: #r1 #l1' ] #l2 #b1 #b2 [1,4: *] |
---|
| 403 | whd in ⊢ (%→?); |
---|
[1882] | 404 | [ @IH1 |
---|
[2155] | 405 | | #EQ destruct(EQ) lapply b2 -b2 lapply l2 -l2 elim B2 -B2 |
---|
| 406 | [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2 [1,4: *] |
---|
| 407 | whd in ⊢ (%→?); |
---|
| 408 | [ @IH2 |
---|
| 409 | | #EQ' whd destruct @seq_block_append_proof_irr % |
---|
| 410 | ] |
---|
[1882] | 411 | ] |
---|
| 412 | qed. |
---|
| 413 | |
---|
[2155] | 414 | lemma is_other_block_instance_append : ∀p,g. |
---|
| 415 | ∀B1 : Σb.bind_pred ? (λx.block_classifier p g x = cl_other) b. |
---|
| 416 | ∀B2 : bind_other_block p g. |
---|
| 417 | ∀l1,l2. |
---|
| 418 | ∀b1 : Σb.block_classifier p g b = cl_other. |
---|
| 419 | ∀b2 : other_block p g. |
---|
| 420 | instantiates_to ? (other_block p g) B1 l1 (pi1 … b1) → |
---|
| 421 | instantiates_to ? (other_block p g) B2 l2 b2 → |
---|
| 422 | instantiates_to ? (other_block p g) (B1 @@ B2) (l1 @ l2) (b1 @@ b2). |
---|
| 423 | #p #g * #B1 elim B1 -B1 |
---|
| 424 | [ #B1 | #f1 #IH1 ] |
---|
| 425 | #B1prf whd in B1prf; |
---|
| 426 | #B2 * [2,4: #r1 #l1' ] #l2 #b1 #b2 [1,4: *] |
---|
| 427 | whd in ⊢ (%→?); |
---|
| 428 | [ @IH1 |
---|
| 429 | | #EQ destruct(EQ) lapply b2 -b2 lapply l2 -l2 elim B2 -B2 |
---|
| 430 | [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2 [1,4: *] |
---|
| 431 | whd in ⊢ (%→?); |
---|
| 432 | [ @IH2 |
---|
| 433 | | #EQ' whd destruct @other_block_append_proof_irr % |
---|
| 434 | ] |
---|
| 435 | ] |
---|
| 436 | qed. |
---|
[1882] | 437 | |
---|
[2155] | 438 | lemma other_fin_step_has_one_label : |
---|
| 439 | ∀p,g.∀s:(Σs.fin_step_classifier p g s = cl_other). |
---|
| 440 | match fin_step_labels ?? s with |
---|
| 441 | [ nil ⇒ False |
---|
| 442 | | cons _ tl ⇒ |
---|
| 443 | match tl with |
---|
| 444 | [ nil ⇒ True |
---|
| 445 | | _ ⇒ False |
---|
| 446 | ] |
---|
[1882] | 447 | ]. |
---|
[2155] | 448 | #p #g ** [#lbl || #ext] |
---|
| 449 | normalize |
---|
| 450 | [3: cases (ext_fin_step_flows p ext) |
---|
| 451 | [* [2: #lbl' * [2: #lbl'' #tl']]] normalize nodelta ] |
---|
| 452 | #EQ destruct % |
---|
| 453 | qed. |
---|
[1882] | 454 | |
---|
[2155] | 455 | definition label_of_other_fin_step : ∀p,g. |
---|
| 456 | (Σs.fin_step_classifier p g s = cl_other) → label ≝ |
---|
| 457 | λp,g,s. |
---|
| 458 | match fin_step_labels p ? s return λx.match x with [ nil ⇒ ? | cons _ tl ⇒ ?] → ? with |
---|
| 459 | [ nil ⇒ Ⓧ |
---|
| 460 | | cons lbl tl ⇒ λ_.lbl |
---|
| 461 | ] (other_fin_step_has_one_label p g s). |
---|
[1882] | 462 | |
---|
[2155] | 463 | (* |
---|
| 464 | definition point_seq_transition : ∀p,g.codeT p g → |
---|
| 465 | code_point p → code_point p → Prop ≝ |
---|
| 466 | λp,g,c,src,dst. |
---|
| 467 | match stmt_at … c src with |
---|
| 468 | [ Some stmt ⇒ match stmt with |
---|
| 469 | [ sequential sq nxt ⇒ |
---|
| 470 | point_of_succ … src nxt = dst |
---|
| 471 | | final fn ⇒ |
---|
| 472 | match fin_step_labels … fn with |
---|
| 473 | [ nil ⇒ False |
---|
| 474 | | cons lbl tl ⇒ |
---|
| 475 | match tl with |
---|
| 476 | [ nil ⇒ point_of_label … c lbl = Some ? dst |
---|
| 477 | | _ ⇒ False |
---|
| 478 | ] |
---|
| 479 | ] |
---|
| 480 | ] |
---|
| 481 | | None ⇒ False |
---|
| 482 | ]. |
---|
[1882] | 483 | |
---|
[2155] | 484 | lemma point_seq_transition_label_of_other_fin_step : |
---|
| 485 | ∀p,c,src.∀s : (Σs.fin_step_classifier p s = cl_other).∀dst. |
---|
| 486 | stmt_at ?? c src = Some ? s → |
---|
| 487 | point_seq_transition p c src dst → |
---|
| 488 | point_of_label … c (label_of_other_fin_step p s) = Some ? dst. |
---|
| 489 | #p #c #src ** [#lbl || #ext] #EQ1 |
---|
| 490 | #dst #EQ2 |
---|
| 491 | whd in match point_seq_transition; normalize nodelta |
---|
| 492 | >EQ2 normalize nodelta whd in ⊢ (?→??(????%)?); |
---|
| 493 | [#H @H | * ] |
---|
| 494 | lapply (other_fin_step_has_one_label ? «ext,?») |
---|
| 495 | cases (fin_step_labels p ? ext) normalize nodelta [*] |
---|
| 496 | #hd * normalize nodelta [2: #_ #_ *] * |
---|
| 497 | #H @H |
---|
| 498 | qed. |
---|
[1882] | 499 | |
---|
[2155] | 500 | lemma point_seq_transition_succ : |
---|
| 501 | ∀p,c,src.∀s,nxt.∀dst. |
---|
| 502 | stmt_at ?? c src = Some ? (sequential ?? s nxt) → |
---|
| 503 | point_seq_transition p c src dst → |
---|
| 504 | point_of_succ … src nxt = dst. |
---|
| 505 | #p #c #src #s #nxt #dst #EQ |
---|
| 506 | whd in match point_seq_transition; normalize nodelta |
---|
| 507 | >EQ normalize nodelta #H @H |
---|
| 508 | qed. |
---|
| 509 | *) |
---|
[1882] | 510 | |
---|
[2155] | 511 | definition if_other : ∀p,g.∀A : Type[2].seq_or_fin_step p g → A → A → A ≝ |
---|
| 512 | λp,g,A,c.match seq_or_fin_step_classifier p g c with |
---|
| 513 | [ cl_other ⇒ λx,y.x |
---|
| 514 | | _ ⇒ λx,y.y |
---|
| 515 | ]. |
---|
[1882] | 516 | |
---|
[2155] | 517 | definition other_step_in_code ≝ |
---|
| 518 | λp,g. |
---|
| 519 | λc : codeT p g. |
---|
| 520 | λsrc : code_point p. |
---|
| 521 | λs : seq_or_fin_step p g. |
---|
| 522 | match s return λx.if_other p g ? x (code_point p) unit → Prop with |
---|
| 523 | [ inl s'' ⇒ λdst.∃n.stmt_at … c src = Some ? (sequential … s'' n) ∧ ? |
---|
| 524 | | inr s'' ⇒ λdst.stmt_at … c src = Some ? (final … s'') ∧ ? |
---|
| 525 | ]. |
---|
| 526 | [ whd in dst; cases (seq_or_fin_step_classifier ???) in dst; |
---|
| 527 | normalize nodelta [1,2,3: #_ @True |*: #dst |
---|
| 528 | @(point_of_succ … src n = dst)] |
---|
| 529 | | whd in dst; |
---|
| 530 | lapply dst -dst |
---|
| 531 | lapply (refl … (seq_or_fin_step_classifier ?? (inr … s''))) |
---|
| 532 | cases (seq_or_fin_step_classifier ?? (inr … s'')) in ⊢ (???%→%); |
---|
| 533 | normalize nodelta |
---|
| 534 | [1,2,3: #_ #_ @True |
---|
| 535 | |*: #EQ #dst |
---|
| 536 | @(point_of_label … c (label_of_other_fin_step p g «s'', EQ») = Some ? dst) |
---|
| 537 | ] |
---|
| 538 | ] |
---|
[1882] | 539 | qed. |
---|
| 540 | |
---|
[2155] | 541 | definition if_other_sig : |
---|
| 542 | ∀p,g.∀B,C : Type[0].∀s : Σs.seq_or_fin_step_classifier p g s = cl_other. |
---|
| 543 | if_other p g ? s B C → B ≝ |
---|
| 544 | λp,g,B,C.?. |
---|
| 545 | ** #s whd in match (if_other ??????); |
---|
| 546 | cases (seq_or_fin_step_classifier ???) normalize nodelta #EQ destruct(EQ) |
---|
| 547 | #x @x |
---|
[1882] | 548 | qed. |
---|
| 549 | |
---|
[2155] | 550 | definition if_other_block_sig : |
---|
| 551 | ∀p,g.∀B,C : Type[0].∀b : Σb.block_classifier p g b = cl_other. |
---|
| 552 | if_other p g ? (\snd b) B C → B ≝ |
---|
| 553 | λp,g,B,C.?. |
---|
| 554 | ** #l #s |
---|
| 555 | #prf #x @(if_other_sig ???? «s, prf» x) |
---|
[1882] | 556 | qed. |
---|
| 557 | |
---|
[2155] | 558 | coercion other_sig_to_if nocomposites: |
---|
| 559 | ∀p,g.∀B,C : Type[0].∀s : Σs.seq_or_fin_step_classifier p g s = cl_other. |
---|
| 560 | ∀x : if_other p g ? s B C.B ≝ if_other_sig |
---|
| 561 | on _x : if_other ?? Type[0] ??? to ?. |
---|
| 562 | |
---|
| 563 | coercion other_block_sig_to_if nocomposites: |
---|
| 564 | ∀p,g.∀B,C : Type[0].∀s : Σs.block_classifier p g s = cl_other. |
---|
| 565 | ∀x : if_other p g ? (\snd s) B C.B ≝ if_other_block_sig |
---|
| 566 | on _x : if_other ?? Type[0] (\snd ?) ?? to ?. |
---|
| 567 | |
---|
| 568 | let rec other_list_in_code p g (c : codeT p g) |
---|
| 569 | src |
---|
| 570 | (b : list (Σs.seq_or_fin_step_classifier p g s = cl_other)) |
---|
| 571 | dst on b : Prop ≝ |
---|
| 572 | match b with |
---|
[1949] | 573 | [ nil ⇒ src = dst |
---|
[2155] | 574 | | cons hd tl ⇒ ∃mid. |
---|
| 575 | other_step_in_code p g c src hd mid ∧ other_list_in_code p g c mid tl dst |
---|
[1949] | 576 | ]. |
---|
| 577 | |
---|
| 578 | notation > "x ~❨ B ❩~> y 'in' c" with precedence 56 for |
---|
| 579 | @{'block_in_code $c $x $B $y}. |
---|
[1882] | 580 | |
---|
[1908] | 581 | notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for |
---|
[1949] | 582 | @{'block_in_code $c $x $B $y}. |
---|
[1882] | 583 | |
---|
[2155] | 584 | interpretation "list in code" 'block_in_code c x B y = |
---|
| 585 | (other_list_in_code ?? c x B y). |
---|
[1882] | 586 | |
---|
[2155] | 587 | definition other_block_in_code : ∀p,g.codeT p g → |
---|
| 588 | code_point p → ∀b : other_block p g. |
---|
| 589 | if_other … (\snd b) (code_point p) unit → Prop ≝ |
---|
| 590 | λp,g,c,src,b,dst. |
---|
| 591 | ∃mid.src ~❨\fst b❩~> mid in c ∧ |
---|
| 592 | other_step_in_code p g c mid (\snd b) dst. |
---|
| 593 | |
---|
| 594 | interpretation "block in code" 'block_in_code c x B y = |
---|
| 595 | (other_block_in_code ?? c x B y). |
---|
| 596 | |
---|
| 597 | lemma other_list_in_code_append : ∀p,g.∀c : codeT p g. |
---|
| 598 | ∀x.∀b1 : list ?. |
---|
| 599 | ∀y.∀b2 : list ?.∀z. |
---|
| 600 | x ~❨b1❩~> y in c→ y ~❨b2❩~> z in c → x ~❨b1@b2❩~> z in c. |
---|
| 601 | #p#g#c#x#b1 lapply x -x |
---|
| 602 | elim b1 [2: ** #hd #hd_prf #tl #IH] #x #y #b2 #z |
---|
| 603 | [3: #EQ normalize in EQ; destruct #H @H] |
---|
| 604 | * #mid * normalize nodelta [ *#n ] #H1 #H2 #H3 |
---|
| 605 | whd normalize nodelta %{mid} |
---|
| 606 | %{(IH … H2 H3)} |
---|
| 607 | [ %{n} ] @H1 |
---|
[1882] | 608 | qed. |
---|
| 609 | |
---|
[2155] | 610 | lemma other_block_in_code_append : ∀p,g.∀c : codeT p g.∀x. |
---|
| 611 | ∀B1 : Σb.block_classifier p g b = cl_other. |
---|
| 612 | ∀y. |
---|
| 613 | ∀B2 : other_block p g. |
---|
| 614 | ∀z. |
---|
| 615 | x ~❨B1❩~> y in c → y ~❨B2❩~> z in c → |
---|
| 616 | x ~❨B1@@B2❩~> z in c. |
---|
| 617 | #p#g#c #x ** #hd1 *#tl1 #tl1prf |
---|
| 618 | #y * #hd2 #tl2 #z |
---|
| 619 | * #mid1 * #H1 #H2 |
---|
| 620 | * #mid2 * #G1 #G2 |
---|
| 621 | %{mid2} %{G2} |
---|
| 622 | whd in match (\fst ?); |
---|
| 623 | @(other_list_in_code_append … H1) |
---|
| 624 | %{y} %{H2 G1} |
---|
| 625 | qed. |
---|
[1882] | 626 | |
---|
[2155] | 627 | (* |
---|
[1882] | 628 | definition instr_block_in_function : |
---|
[2155] | 629 | ∀p : evaluation_params.∀fn : joint_internal_function (globals p) p. |
---|
[1882] | 630 | code_point p → |
---|
[2155] | 631 | ∀b : bind_other_block p. |
---|
[1949] | 632 | ? → Prop ≝ |
---|
[2155] | 633 | λp,fn,src,B,dst. |
---|
[1882] | 634 | ∃vars,B'. |
---|
| 635 | All ? (In ? (joint_if_locals … fn)) vars ∧ |
---|
[2155] | 636 | instantiates_to … B vars B' ∧ |
---|
[1949] | 637 | src ~❨B'❩~> dst in joint_if_code … fn. |
---|
[1882] | 638 | |
---|
[2155] | 639 | interpretation "bind block in function" 'block_in_code fn x B y = |
---|
| 640 | (instr_block_in_function ? fn x B y). |
---|
[1882] | 641 | |
---|
| 642 | lemma instr_block_in_function_trans : |
---|
[2155] | 643 | ∀p,fn,src. |
---|
| 644 | ∀B1 : ΣB.bind_pred ? (λb.block_classifier p b = cl_other) B. |
---|
| 645 | ∀mid. |
---|
| 646 | ∀B2 : bind_other_block p. |
---|
| 647 | ∀dst. |
---|
| 648 | src ~❨B1❩~> Some ? mid in fn → |
---|
[1949] | 649 | mid ~❨B2❩~> dst in fn → |
---|
[2155] | 650 | src ~❨B1@@B2❩~> dst in fn. |
---|
| 651 | #p#fn#src*#B1#B1prf#mid#B2#dst |
---|
[1882] | 652 | * #vars1 * #b1 ** #vars1_ok #b1B1 #b1_in |
---|
| 653 | * #vars2 * #b2 ** #vars2_ok #b2B2 #b2_in |
---|
[2155] | 654 | %{(vars1@vars2)} %{(«b1,instantiates_to_bind_pred … b1B1 B1prf» @@ b2)} |
---|
| 655 | /4 by All_append, conj, is_other_block_instance_append, other_block_in_code_append/ |
---|
[1882] | 656 | qed. |
---|
[2155] | 657 | *) |
---|
| 658 | *) |
---|
| 659 | *) |
---|