[1626] | 1 | include "utilities/lists.ma". |
---|
[764] | 2 | include "common/Globalenvs.ma". |
---|
| 3 | include "Cminor/syntax.ma". |
---|
| 4 | include "RTLabs/syntax.ma". |
---|
| 5 | |
---|
[1626] | 6 | definition env ≝ identifier_map SymbolTag (register × typ). |
---|
[1316] | 7 | definition label_env ≝ identifier_map Label label. |
---|
[1056] | 8 | definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝ |
---|
[764] | 9 | λen,gen. foldr ?? |
---|
[887] | 10 | (λidt,rsengen. |
---|
| 11 | let 〈id,ty〉 ≝ idt in |
---|
[1056] | 12 | let 〈rs,en,gen〉 ≝ rsengen in |
---|
| 13 | let 〈r,gen'〉 ≝ fresh … gen in |
---|
[1626] | 14 | 〈〈r,ty〉::rs, add ?? en id 〈r,ty〉, gen'〉) 〈[ ], en, gen〉. |
---|
[1631] | 15 | |
---|
| 16 | definition Env_has : env → ident → typ → Prop ≝ |
---|
| 17 | λe,i,t. match lookup ?? e i with [ Some x ⇒ \snd x = t | None ⇒ False ]. |
---|
| 18 | |
---|
| 19 | lemma Env_has_present : ∀e,i,t. Env_has e i t → present … e i. |
---|
| 20 | #e #i #t whd in ⊢ (% → %); cases (lookup ?? e i) |
---|
| 21 | [ * | * #r #t' #E % #E' destruct ] |
---|
| 22 | qed. |
---|
| 23 | |
---|
[1316] | 24 | lemma populates_env : ∀l,e,u,l',e',u'. |
---|
[1631] | 25 | distinct_env ?? l → |
---|
[1316] | 26 | populate_env e u l = 〈l',e',u'〉 → |
---|
[1631] | 27 | ∀i,t. Exists ? (λx.x = 〈i,t〉) l → |
---|
| 28 | Env_has e' i t. |
---|
[1316] | 29 | #l elim l |
---|
[1631] | 30 | [ #e #u #l' #e' #u' #D #E whd in E:(??%?); #i #t destruct (E) * |
---|
| 31 | | * #id #ty #tl #IH #e #u #l' #e' #u' #D #E #i #t whd in E:(??%?) ⊢ (% → ?); |
---|
| 32 | * [ #E1 destruct (E1) |
---|
[1516] | 33 | generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ?; * * #x #y #z |
---|
[1631] | 34 | whd in ⊢ (??%? → ?); |
---|
| 35 | lapply (refl ? (fresh ? z)) elim (fresh ? z) in ⊢ (??%? → %); |
---|
| 36 | #r #gen' #E1 #E2 |
---|
| 37 | whd in E2:(??%?); destruct; |
---|
| 38 | whd >lookup_add_hit % |
---|
[1521] | 39 | | #H change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ? ])?); |
---|
[1316] | 40 | lapply (refl ? (populate_env e u tl)) |
---|
[1516] | 41 | cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *) |
---|
[1631] | 42 | * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?); |
---|
| 43 | lapply (refl ? (fresh ? u1)) cases (fresh ? u1) in ⊢ (??%? → %); #r #u'' #E2 |
---|
[1516] | 44 | whd in ⊢ (??%? → ?); #E destruct |
---|
[1631] | 45 | whd >lookup_add_miss |
---|
| 46 | [ @(IH … E1 ?? H) @(proj2 … D) |
---|
| 47 | | cases (Exists_All … H (proj1 … D)) #x * #E3 destruct #NE /2/ |
---|
| 48 | ] |
---|
[1316] | 49 | ] |
---|
| 50 | ] qed. |
---|
| 51 | |
---|
[1631] | 52 | lemma populates_env_distinct : ∀r,l,e,u,l',e',u'. |
---|
| 53 | distinct_env ?? (l@r) → |
---|
| 54 | populate_env e u l = 〈l',e',u'〉 → |
---|
| 55 | All ? (λit. fresh_for_map … (\fst it) e) r → |
---|
| 56 | All ? (λit. fresh_for_map … (\fst it) e') r. |
---|
| 57 | #r #l elim l |
---|
| 58 | [ #e #u #l' #e' #u' #D #E whd in E:(??%?); destruct (E) // |
---|
| 59 | | * #id #ty #tl #IH #e #u #l' #e' #u' #D #E whd in E:(??%?) ⊢ (% → ?); |
---|
| 60 | change with (populate_env ???) in E:(??(match % with [ _ ⇒ ?])?); |
---|
| 61 | lapply (refl ? (populate_env e u tl)) cases (populate_env e u tl) in (*E*) ⊢ (???% → ?); |
---|
| 62 | * #x #y #z #E2 >E2 in E; |
---|
| 63 | whd in ⊢ (??%? → ?); |
---|
| 64 | elim (fresh ? z) |
---|
| 65 | #rg #gen' #E |
---|
| 66 | whd in E:(??%?); destruct |
---|
| 67 | #F lapply (IH … E2 F) |
---|
| 68 | [ @(proj2 … D) |
---|
| 69 | | lapply (All_append_r … (proj1 … D)) |
---|
| 70 | elim r |
---|
| 71 | [ // |
---|
| 72 | | * #i #t #tl' #IH * #D1 #D2 * #H1 #H2 % |
---|
| 73 | [ @fresh_for_map_add /2/ |
---|
| 74 | | @IH // |
---|
| 75 | ] |
---|
| 76 | ] |
---|
| 77 | ] |
---|
| 78 | ] qed. |
---|
| 79 | |
---|
[1316] | 80 | lemma populate_extends : ∀l,e,u,l',e',u'. |
---|
[1631] | 81 | All ? (λit. fresh_for_map ?? (\fst it) e) l → |
---|
[1316] | 82 | populate_env e u l = 〈l',e',u'〉 → |
---|
[1631] | 83 | ∀i,t. Env_has e i t → Env_has e' i t. |
---|
[1316] | 84 | #l elim l |
---|
[1631] | 85 | [ #e #u #l' #e' #u' #F #E whd in E:(??%?); destruct // |
---|
| 86 | | * #id #t #tl #IH #e #u #l' #e' #u' #F #E whd in E:(??%?); |
---|
[1521] | 87 | change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?); |
---|
[1316] | 88 | lapply (refl ? (populate_env e u tl)) |
---|
[1516] | 89 | cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0 |
---|
[1631] | 90 | >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E |
---|
[1515] | 91 | destruct |
---|
[1631] | 92 | #i #t #H whd >lookup_add_miss |
---|
| 93 | [ @(IH … E0) [ @(proj2 … F) | @H ] |
---|
| 94 | | @(present_not_fresh ?? e) [ whd in H ⊢ %; % #E >E in H; * | @(proj1 … F) ] |
---|
[1316] | 95 | ] qed. |
---|
[1631] | 96 | |
---|
| 97 | definition lookup_reg : ∀e:env. ∀id,ty. Env_has e id ty → register ≝ λe,id,ty,H. \fst (lookup_present ?? e id ?). |
---|
| 98 | /2/ qed. |
---|
| 99 | |
---|
| 100 | lemma populate_env_list : ∀l,e,u,l',e',u'. |
---|
| 101 | populate_env e u l = 〈l',e',u'〉 → |
---|
| 102 | ∀i,r,t. ∀H:Env_has e' i t. lookup_reg e' i t H = r → |
---|
| 103 | (∃H:Env_has e i t. lookup_reg e i t H = r) ∨ env_has l' r t. |
---|
| 104 | #l elim l |
---|
| 105 | [ #e #u #l' #e' #u' #E whd in E:(??%?); destruct #i #r #t #H #L %1 %{H} @L |
---|
| 106 | | * #id #ty #tl #IH #e #u #l' #e' #u' #E |
---|
| 107 | whd in E:(??%?); |
---|
| 108 | change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?); |
---|
| 109 | lapply (refl ? (populate_env e u tl)) |
---|
| 110 | cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0 |
---|
| 111 | >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E |
---|
| 112 | destruct |
---|
| 113 | #i #r #t cases (identifier_eq ? i id) |
---|
| 114 | [ #E1 >E1 #H whd in ⊢ (??%? → %); whd in match (lookup_present ?????); |
---|
| 115 | generalize in ⊢ (??(??? (?%))? → ?); |
---|
| 116 | whd in H ⊢ (% → ?); >lookup_add_hit in H ⊢ %; normalize #E2 #NE #E3 destruct |
---|
| 117 | %2 %1 % |
---|
| 118 | | #NE #H #L cases (IH … E0 i r t ??) |
---|
| 119 | [ /2/ |
---|
| 120 | | #X %2 %2 @X |
---|
| 121 | | whd in H ⊢ %; >lookup_add_miss in H; // |
---|
| 122 | | whd in L:(??%?); whd in match (lookup_present ?????) in L; |
---|
| 123 | lapply L -L |
---|
| 124 | generalize in ⊢ (??(???(?%))? → ?); whd in ⊢ (% → ?); |
---|
| 125 | generalize in ⊢ (? → ? → ??(????%)?); |
---|
| 126 | >lookup_add_miss // #H0 #p |
---|
| 127 | change with (lookup_present SymbolTag (register×typ) e0 i ?) in ⊢ (??(???%)? → ?); |
---|
| 128 | whd in ⊢ (? → ??%?); generalize in ⊢ (? → ??(???(?????%))?); |
---|
| 129 | #p' #X @X |
---|
| 130 | ] |
---|
| 131 | ] |
---|
| 132 | ] qed. |
---|
| 133 | |
---|
[1316] | 134 | definition populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝ |
---|
[766] | 135 | λen,gen. foldr ?? |
---|
| 136 | (λid,engen. |
---|
[1056] | 137 | let 〈en,gen〉 ≝ engen in |
---|
| 138 | let 〈r,gen'〉 ≝ fresh … gen in |
---|
| 139 | 〈add ?? en id r, gen'〉) 〈en, gen〉. |
---|
[764] | 140 | |
---|
[1316] | 141 | lemma populates_label_env : ∀ls,lbls,u,lbls',u'. |
---|
| 142 | populate_label_env lbls u ls = 〈lbls',u'〉 → |
---|
| 143 | ∀l. Exists ? (λl'.l' = l) ls → present ?? lbls' l. |
---|
| 144 | #ls elim ls |
---|
| 145 | [ #lbls #u #lbls' #u' #E #l * |
---|
[1516] | 146 | | #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?); |
---|
[1521] | 147 | change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?); |
---|
[1316] | 148 | lapply (refl ? (populate_label_env lbls u t)) |
---|
[1516] | 149 | cases (populate_label_env lbls u t) in ⊢ (???% → %); |
---|
| 150 | #lbls1 #u1 #E1 whd in ⊢ (??%? → ?); |
---|
[1631] | 151 | cases (fresh LabelTag u1) #lf #uf whd in ⊢ (??%? → ?); |
---|
[1515] | 152 | #E destruct |
---|
[1316] | 153 | #l * |
---|
| 154 | [ #El <El whd >lookup_add_hit % #Er destruct |
---|
| 155 | | #H @lookup_add_oblivious @(IH … E1 ? H) |
---|
| 156 | ] |
---|
| 157 | ] qed. |
---|
| 158 | |
---|
| 159 | lemma label_env_contents : ∀ls,lbls,u,lbls',u'. |
---|
| 160 | populate_label_env lbls u ls = 〈lbls',u'〉 → |
---|
| 161 | ∀l. present ?? lbls' l → Exists ? (λl'.l = l') ls ∨ present ?? lbls l. |
---|
| 162 | #ls elim ls |
---|
| 163 | [ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H |
---|
[1516] | 164 | | #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?); |
---|
[1521] | 165 | change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?); |
---|
[1316] | 166 | lapply (refl ? (populate_label_env lbls u t)) |
---|
[1516] | 167 | cases (populate_label_env lbls u t) in ⊢ (???% → %); |
---|
| 168 | #lbls1 #u1 #E1 whd in ⊢ (??%? → ?); |
---|
[1631] | 169 | cases (fresh ? u1) #fi #fu whd in ⊢ (??%? → ?); |
---|
[1515] | 170 | #E destruct |
---|
[1316] | 171 | #l #H cases (identifier_eq ? l h) |
---|
| 172 | [ #El %1 %1 @El |
---|
| 173 | | #NE cases (IH … E1 l ?) |
---|
[1516] | 174 | [ #H' %1 %2 @H' | #H' %2 @H' | whd in H; >lookup_add_miss in H; // ] |
---|
[1316] | 175 | ] |
---|
| 176 | ] qed. |
---|
| 177 | |
---|
| 178 | definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??. |
---|
| 179 | |
---|
| 180 | (* Check that the domain of one graph is included in another, for monotonicity |
---|
| 181 | properties. Note that we don't say anything about the statements. *) |
---|
| 182 | definition graph_included : graph statement → graph statement → Prop ≝ |
---|
| 183 | λg1,g2. ∀l. present ?? g1 l → present ?? g2 l. |
---|
| 184 | |
---|
| 185 | lemma graph_inc_trans : ∀g1,g2,g3. |
---|
| 186 | graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3. |
---|
| 187 | #g1 #g2 #g3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed. |
---|
| 188 | |
---|
| 189 | definition lpresent ≝ λlbls:label_env. λl. ∃l'. lookup ?? lbls l' = Some ? l. |
---|
| 190 | |
---|
| 191 | definition partially_closed : label_env → graph statement → Prop ≝ |
---|
[1626] | 192 | λe,g. forall_nodes ? (labels_P (λl. present ?? g l ∨ lpresent e l)) g. |
---|
[1316] | 193 | |
---|
| 194 | (* I'd use a single parametrised definition along with internal_function, but |
---|
| 195 | it's a pain without implicit parameters. *) |
---|
[1626] | 196 | record partial_fn (lenv:label_env) (env:env) : Type[0] ≝ |
---|
[1316] | 197 | { pf_labgen : universe LabelTag |
---|
| 198 | ; pf_reggen : universe RegisterTag |
---|
| 199 | ; pf_params : list (register × typ) |
---|
| 200 | ; pf_locals : list (register × typ) |
---|
[1626] | 201 | ; pf_result : option (Σrt:register × typ. env_has (pf_locals @ pf_params) (\fst rt) (\snd rt)) |
---|
| 202 | ; pf_envok : ∀id,ty,r,H. lookup_reg env id ty H = r → env_has (pf_locals @ pf_params) r ty |
---|
[1316] | 203 | ; pf_stacksize : nat |
---|
| 204 | ; pf_graph : graph statement |
---|
| 205 | ; pf_closed : partially_closed lenv pf_graph |
---|
[1626] | 206 | ; pf_typed : graph_typed (pf_locals @ pf_params) pf_graph |
---|
[1316] | 207 | ; pf_entry : Σl:label. present ?? pf_graph l |
---|
| 208 | ; pf_exit : Σl:label. present ?? pf_graph l |
---|
| 209 | }. |
---|
| 210 | |
---|
[1626] | 211 | definition fn_env_has ≝ |
---|
| 212 | λle,env,f. env_has (pf_locals le env f @ pf_params le env f). |
---|
[1316] | 213 | |
---|
[1626] | 214 | record fn_contains (le:label_env) (env:env) (f1:partial_fn le env) (f2:partial_fn le env) : Prop ≝ |
---|
| 215 | { fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2) |
---|
| 216 | ; fn_con_env : ∀r,ty. fn_env_has le env f1 r ty → fn_env_has le env f2 r ty |
---|
| 217 | }. |
---|
[1316] | 218 | |
---|
[1626] | 219 | lemma fn_con_trans : ∀le,env,f1,f2,f3. |
---|
| 220 | fn_contains le env f1 f2 → fn_contains le env f2 f3 → fn_contains le env f1 f3. |
---|
| 221 | #le #env #f1 #f2 #f3 #H1 #H2 % |
---|
| 222 | [ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2)) |
---|
| 223 | | #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H |
---|
| 224 | ] qed. |
---|
[1316] | 225 | |
---|
[1626] | 226 | lemma fn_con_refl : ∀label_env,env,f. |
---|
| 227 | fn_contains label_env env f f. |
---|
| 228 | #le #env #f % #l // qed. |
---|
| 229 | |
---|
| 230 | lemma fn_con_sig : ∀label_env,env,f,f0. |
---|
| 231 | ∀f':Σf':partial_fn label_env env. fn_contains … f0 f'. |
---|
| 232 | fn_contains label_env env f f0 → |
---|
| 233 | fn_contains label_env env f f'. |
---|
| 234 | #le #env #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1) |
---|
[1072] | 235 | qed. |
---|
| 236 | |
---|
[1626] | 237 | lemma add_statement_inv : ∀le,env,l,s.∀f. |
---|
| 238 | labels_present (pf_graph le env f) s → |
---|
| 239 | partially_closed le (add … (pf_graph … f) l s). |
---|
| 240 | #le #env #l #s #f #p |
---|
[1316] | 241 | #l' #s' #H cases (identifier_eq … l l') |
---|
[1516] | 242 | [ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //] |
---|
[1316] | 243 | @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H |
---|
[1626] | 244 | | #NE @(labels_P_mp … (pf_closed … f l' s' ?)) |
---|
[1316] | 245 | [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ] |
---|
[1516] | 246 | | >lookup_add_miss in H; /2/ |
---|
[1316] | 247 | ] |
---|
| 248 | ] qed. |
---|
| 249 | |
---|
[1626] | 250 | definition statement_typed_in ≝ |
---|
| 251 | λle,env,f,s. statement_typed (pf_locals le env f @ pf_params le env f) s. |
---|
| 252 | |
---|
| 253 | lemma forall_nodes_add : ∀A,P,l,a,g. |
---|
| 254 | forall_nodes A P g → P a → forall_nodes A P (add ?? g l a). |
---|
| 255 | #A #P #l #a #g #ALL #NEW |
---|
| 256 | #l' #a' |
---|
| 257 | cases (identifier_eq … l' l) |
---|
| 258 | [ #E destruct >lookup_add_hit #E destruct @NEW |
---|
| 259 | | #ne >lookup_add_miss /2/ |
---|
| 260 | ] qed. |
---|
| 261 | |
---|
[766] | 262 | (* Add a statement to the graph, *without* updating the entry label. *) |
---|
[1626] | 263 | definition fill_in_statement : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env. |
---|
| 264 | labels_present (pf_graph … f) s → |
---|
| 265 | statement_typed_in le env f s → |
---|
| 266 | Σf':partial_fn le env. fn_contains … f f' ≝ |
---|
| 267 | λle,env,l,s,f,p,tp. |
---|
| 268 | mk_partial_fn le env (pf_labgen … f) (pf_reggen … f) |
---|
| 269 | (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f) |
---|
| 270 | (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ? |
---|
| 271 | «pf_entry … f, ?» «pf_exit … f, ?». |
---|
[1316] | 272 | [ @add_statement_inv @p |
---|
[1626] | 273 | | @forall_nodes_add // |
---|
| 274 | | 3,4: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ] |
---|
| 275 | | % [ #l' @lookup_add_oblivious | // ] |
---|
[1316] | 276 | ] qed. |
---|
[764] | 277 | |
---|
[766] | 278 | (* Add a statement to the graph, making it the entry label. *) |
---|
[1626] | 279 | definition add_to_graph : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env. |
---|
| 280 | labels_present (pf_graph … f) s → |
---|
| 281 | statement_typed_in … f s → |
---|
| 282 | Σf':partial_fn le env. fn_contains … f f' ≝ |
---|
| 283 | λle,env,l,s,f,p,tl. |
---|
| 284 | mk_partial_fn le env (pf_labgen … f) (pf_reggen … f) |
---|
| 285 | (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f) |
---|
| 286 | (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ? |
---|
| 287 | «l, ?» «pf_exit … f, ?». |
---|
[1316] | 288 | [ @add_statement_inv @p |
---|
[1626] | 289 | | @forall_nodes_add // |
---|
[1316] | 290 | | whd >lookup_add_hit % #E destruct |
---|
[1626] | 291 | | @lookup_add_oblivious @(pi2 … (pf_exit … f)) |
---|
| 292 | | % [ #l' @lookup_add_oblivious | // ] |
---|
[1070] | 293 | ] qed. |
---|
[764] | 294 | |
---|
[766] | 295 | (* Add a statement with a fresh label to the start of the function. The |
---|
| 296 | statement is parametrised by the *next* instruction's label. *) |
---|
[1626] | 297 | definition add_fresh_to_graph : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env. |
---|
| 298 | (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) → |
---|
| 299 | (∀l. statement_typed_in … f (s l)) → |
---|
| 300 | Σf':partial_fn le env. fn_contains … f f' ≝ |
---|
| 301 | λle,env,s,f,p,tp. |
---|
| 302 | let 〈l,g〉 ≝ fresh … (pf_labgen … f) in |
---|
| 303 | let s' ≝ s (pf_entry … f) in |
---|
| 304 | (mk_partial_fn le env g (pf_reggen … f) |
---|
| 305 | (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f) |
---|
| 306 | (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ? |
---|
| 307 | «l, ?» «pf_exit … f, ?»). |
---|
| 308 | [ % [ #l' @lookup_add_oblivious | // ] |
---|
[1603] | 309 | | @add_statement_inv @p @(pi2 … (pf_entry …)) |
---|
[1626] | 310 | | @forall_nodes_add // |
---|
[1316] | 311 | | whd >lookup_add_hit % #E destruct |
---|
[1603] | 312 | | @lookup_add_oblivious @(pi2 … (pf_exit …)) |
---|
[1070] | 313 | ] qed. |
---|
[1072] | 314 | |
---|
[1316] | 315 | (* Variants for labels which are (goto) labels *) |
---|
[766] | 316 | |
---|
[1626] | 317 | lemma add_statement_inv' : ∀le,env,l,s.∀f. |
---|
| 318 | labels_P (λl. present ?? (pf_graph le env f) l ∨ lpresent le l) s → |
---|
| 319 | partially_closed le (add … (pf_graph … f) l s). |
---|
| 320 | #le #env #l #s #f #p |
---|
[1316] | 321 | #l' #s' #H cases (identifier_eq … l l') |
---|
[1516] | 322 | [ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //] |
---|
[1316] | 323 | @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ] |
---|
[1626] | 324 | | #NE @(labels_P_mp … (pf_closed … f l' s' ?)) |
---|
[1316] | 325 | [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ] |
---|
[1516] | 326 | | >lookup_add_miss in H; /2/ |
---|
[1316] | 327 | ] |
---|
| 328 | ] qed. |
---|
| 329 | |
---|
[1626] | 330 | definition add_fresh_to_graph' : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env. |
---|
| 331 | (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent le l) (s l)) → |
---|
| 332 | (∀l. statement_typed_in … f (s l)) → |
---|
| 333 | Σf':partial_fn le env. fn_contains … f f' ≝ |
---|
| 334 | λle,env,s,f,p,tp. |
---|
| 335 | let 〈l,g〉 ≝ fresh … (pf_labgen … f) in |
---|
| 336 | let s' ≝ s (pf_entry … f) in |
---|
| 337 | (mk_partial_fn le env g (pf_reggen … f) |
---|
| 338 | (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f) |
---|
| 339 | (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ? |
---|
| 340 | «l, ?» «pf_exit … f, ?»). |
---|
| 341 | [ % [ #l' @lookup_add_oblivious | // ] |
---|
[1603] | 342 | | @add_statement_inv' @p @(pi2 … (pf_entry …)) |
---|
[1626] | 343 | | @forall_nodes_add // |
---|
[1316] | 344 | | whd >lookup_add_hit % #E destruct |
---|
[1603] | 345 | | @lookup_add_oblivious @(pi2 … (pf_exit …)) |
---|
[1316] | 346 | ] qed. |
---|
| 347 | |
---|
[1626] | 348 | lemma extend_typ_env : ∀te,r,t,r',t'. |
---|
| 349 | env_has te r t → env_has (〈r',t'〉::te) r t. |
---|
| 350 | #tw #r #t #r' #t' #H %2 @H |
---|
| 351 | qed. |
---|
[1316] | 352 | |
---|
[1626] | 353 | lemma stmt_extend_typ_env : ∀te,r,t,s. |
---|
| 354 | statement_typed te s → statement_typed (〈r,t〉::te) s. |
---|
| 355 | #tw #r #t * |
---|
| 356 | [ 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/ |
---|
| 357 | | *: // |
---|
| 358 | ] qed. |
---|
| 359 | |
---|
| 360 | (* A little more nesting in the result type than I'd like, but it keeps the |
---|
| 361 | function closely paired with the proof that it contains f. *) |
---|
| 362 | definition fresh_reg : ∀le,env. ∀f:partial_fn le env. ∀ty:typ. |
---|
| 363 | 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝ |
---|
| 364 | λle,env,f,ty. |
---|
| 365 | let 〈r,g〉 ≝ fresh … (pf_reggen … f) in |
---|
| 366 | let f' ≝ |
---|
| 367 | «mk_partial_fn le env |
---|
| 368 | (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) |
---|
| 369 | (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? «pi1 … rt, ?»]) ? |
---|
| 370 | (pf_stacksize … f) (pf_graph … f) (pf_closed … f) ? (pf_entry … f) (pf_exit … f), ?» |
---|
| 371 | in |
---|
| 372 | ❬f' , ?(*«r, ?»*)❭. |
---|
| 373 | [ @(«r, ?») % @refl |
---|
| 374 | | #l #s #L @stmt_extend_typ_env @(pf_typed … L) |
---|
| 375 | | #i #t #r1 #H #L %2 @(pf_envok … f … L) |
---|
| 376 | | %2 @(pi2 … rt) |
---|
| 377 | | % [ #l // | #r' #ty' #H @extend_typ_env @H ] |
---|
| 378 | ] qed. |
---|
| 379 | |
---|
[797] | 380 | axiom UnknownVariable : String. |
---|
| 381 | |
---|
[1626] | 382 | definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le env. expr_vars ty e (Env_has env) → |
---|
| 383 | 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝ |
---|
[1316] | 384 | λle,env,ty,e,f. |
---|
[1626] | 385 | match e return λty,e. expr_vars ty e (Env_has env) → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) with |
---|
| 386 | [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg env i t Env, ?»❭ |
---|
| 387 | | _ ⇒ λ_.fresh_reg le env f ? |
---|
[766] | 388 | ]. |
---|
[1626] | 389 | [ % // |
---|
| 390 | | @(pf_envok … Env) @refl |
---|
| 391 | ] qed. |
---|
[1316] | 392 | |
---|
| 393 | let rec foldr_all (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → B → B) (b:B) (l:list A) (H:All ? P l) on l :B ≝ |
---|
| 394 | match l return λx.All ? P x → B with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) (foldr_all A B P f b l (proj2 … H))] H. |
---|
[1626] | 395 | |
---|
| 396 | let rec foldr_all' (A:Type[0]) (P:A → Prop) (B:list A → Type[0]) (f:∀a:A. P a → ∀l. B l → B (a::l)) (b:B [ ]) (l:list A) (H:All ? P l) on l :B l ≝ |
---|
| 397 | match l return λx.All ? P x → B x with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) l (foldr_all' A P B f b l (proj2 … H))] H. |
---|
[766] | 398 | |
---|
[1626] | 399 | definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (Env_has env) ]. |
---|
[766] | 400 | |
---|
[1626] | 401 | definition eject' : ∀A. ∀P:A → Type[0]. (𝚺a.P a) → A ≝ |
---|
| 402 | λA,P,x. match x with [ mk_DPair a _ ⇒ a]. |
---|
| 403 | |
---|
[1605] | 404 | definition choose_regs : ∀le. ∀env:env. ∀es:list (𝚺t:typ.expr t). |
---|
[1626] | 405 | ∀f:partial_fn le env. All ? (exprtyp_present env) es → |
---|
| 406 | 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs es) ≝ |
---|
[1316] | 407 | λle,env,es,f,Env. |
---|
[1626] | 408 | foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs es)) |
---|
| 409 | (λe,p,tl,acc. |
---|
| 410 | match acc return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒ |
---|
| 411 | match e return λe.exprtyp_present env e → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp. |
---|
| 412 | match choose_reg le env t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (❬t,e❭::tl)) with [ mk_DPair f' r ⇒ |
---|
| 413 | ❬«pi1 … f', ?»,«(pi1 … r)::(pi1 … rs), ?»❭ |
---|
| 414 | ] |
---|
| 415 | ] p |
---|
| 416 | ]) ❬«f, ?», «[ ], I»❭ es Env. |
---|
[1316] | 417 | [ @p |
---|
[1626] | 418 | | cases r #r' #Hr' cases rs #rs' #Hrs' |
---|
| 419 | % [ whd in ⊢ (???%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ] |
---|
| 420 | | @fn_con_trans [ 3: @(pi2 … f') | skip | @(pi2 … f1) ] |
---|
| 421 | | @fn_con_refl |
---|
[1316] | 422 | ] qed. |
---|
| 423 | |
---|
| 424 | lemma extract_pair : ∀A,B,C,D. ∀u:A×B. ∀Q:A → B → C×D. ∀x,y. |
---|
| 425 | ((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) → |
---|
| 426 | ∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉. |
---|
| 427 | #A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed. |
---|
| 428 | |
---|
| 429 | |
---|
[1626] | 430 | lemma choose_regs_length : ∀le,env,es,f,p,f',rs. |
---|
| 431 | choose_regs le env es f p = ❬f',rs❭ → |es| = |rs|. |
---|
| 432 | #le #env #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H) |
---|
| 433 | qed. |
---|
[1316] | 434 | |
---|
[1626] | 435 | lemma present_included : ∀le,env,f,f',l. |
---|
| 436 | fn_contains le env f f' → |
---|
| 437 | present ?? (pf_graph … f) l → |
---|
| 438 | present ?? (pf_graph … f') l. |
---|
| 439 | #le #env #f #f' #l * #H1 #H2 @H1 qed. |
---|
[1316] | 440 | |
---|
[1464] | 441 | (* Some definitions for the add_stmt function later, which we introduce now so |
---|
| 442 | that we can build the whole fn_graph_included machinery at once. *) |
---|
| 443 | |
---|
| 444 | (* We need to show that the graph only grows, and that Cminor labels will end |
---|
| 445 | up in the graph. *) |
---|
[1626] | 446 | definition Cminor_labels_added ≝ λle,env,s,f'. |
---|
[1464] | 447 | ∀l. Exists ? (λl'.l=l') (labels_of s) → |
---|
[1626] | 448 | ∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le env f') l'. |
---|
[1464] | 449 | |
---|
[1626] | 450 | record add_stmt_inv (le:label_env) (env:env) (s:stmt) (f:partial_fn le env) (f':partial_fn le env) : Prop ≝ |
---|
| 451 | { stmt_graph_con : fn_contains … f f' |
---|
| 452 | ; stmt_labels_added : Cminor_labels_added … s f' |
---|
[1464] | 453 | }. |
---|
| 454 | |
---|
[1626] | 455 | (* Build some machinery to solve fn_contains goals. *) |
---|
[1464] | 456 | |
---|
| 457 | (* A datatype saying how we intend to prove a step. *) |
---|
[1626] | 458 | inductive fn_con_because (le:label_env) (env:env) : partial_fn le env → Type[0] ≝ |
---|
| 459 | | fn_con_eq : ∀f. fn_con_because le env f |
---|
| 460 | | fn_con_sig : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 → |
---|
| 461 | ∀f3:(Σf3:partial_fn le env.fn_contains … f2 f3). fn_con_because le env f3 |
---|
| 462 | | fn_con_addinv : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 → |
---|
| 463 | ∀s.∀f3:(Σf3:partial_fn le env.add_stmt_inv … s f2 f3). fn_con_because le env f3 |
---|
[1464] | 464 | . |
---|
| 465 | |
---|
| 466 | (* Extract the starting function for a step. *) |
---|
[1626] | 467 | let rec fn_con_because_left le env f0 (b:fn_con_because ?? f0) on b : partial_fn le env ≝ |
---|
| 468 | match b with [ fn_con_eq f ⇒ f | fn_con_sig f _ _ _ ⇒ f | fn_con_addinv f _ _ _ _ ⇒ f ]. |
---|
[1464] | 469 | |
---|
| 470 | (* Some unification hints to pick the right step to apply. The dummy variable |
---|
| 471 | is there to provide goal that the lemma can't apply to, which causes an error |
---|
| 472 | and forces the "repeat" tactical to stop. The first hint recognises that we |
---|
| 473 | have reached the desired starting point. *) |
---|
| 474 | |
---|
[1626] | 475 | unification hint 0 ≔ le:label_env, env:env, f:partial_fn le env, dummy:True; |
---|
[1464] | 476 | f' ≟ f, |
---|
[1626] | 477 | b ≟ fn_con_eq le env f |
---|
[1464] | 478 | ⊢ |
---|
[1626] | 479 | fn_contains le env f f' ≡ fn_contains le env (fn_con_because_left le env f' b) f' |
---|
[1464] | 480 | . |
---|
| 481 | |
---|
[1626] | 482 | unification hint 1 ≔ le:label_env, env:env, f1:partial_fn le env, f2:partial_fn le env, H12 : fn_contains le env f1 f2, f3:(Σf3:partial_fn le env. fn_contains le env f2 f3); |
---|
| 483 | b ≟ fn_con_sig le env f1 f2 H12 f3 |
---|
[1464] | 484 | ⊢ |
---|
[1626] | 485 | fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3 |
---|
[1464] | 486 | . |
---|
| 487 | |
---|
[1626] | 488 | unification hint 1 ≔ le:label_env, env:env, f1:partial_fn le env, f2:partial_fn le env, H12 : fn_contains le env f1 f2, s:stmt, f3:(Σf3:partial_fn le env. add_stmt_inv le env s f2 f3); |
---|
| 489 | b ≟ fn_con_addinv le env f1 f2 H12 s f3 |
---|
[1464] | 490 | ⊢ |
---|
[1626] | 491 | fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3 |
---|
[1464] | 492 | . |
---|
| 493 | |
---|
| 494 | (* A lemma to perform a step of the proof. We can repeat this to do the whole |
---|
| 495 | proof. *) |
---|
[1626] | 496 | lemma fn_contains_step : ∀le,env,f. ∀b:fn_con_because le env f. fn_contains … (fn_con_because_left … f b) f. |
---|
| 497 | #le #env #f * |
---|
| 498 | [ #f @fn_con_refl |
---|
| 499 | | #f1 #f2 #H12 * #f3 #H23 @(fn_con_trans … H12 H23) |
---|
| 500 | | #f1 #f2 #H12 #s * #f3 * #H23 #X @(fn_con_trans … H12 H23) |
---|
[1464] | 501 | ] qed. |
---|
| 502 | |
---|
[1626] | 503 | notation > "vbox('let' ❬ ident v , ident p ❭ ≝ e 'in' break e')" with precedence 10 |
---|
| 504 | for @{ match ${e} with [ mk_DPair ${ident v} ${ident p} ⇒ ${e'} ] }. |
---|
[1464] | 505 | |
---|
[797] | 506 | axiom BadCminorProgram : String. |
---|
| 507 | |
---|
[1626] | 508 | let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty) |
---|
| 509 | (Env:expr_vars ty e (Env_has env)) (f:partial_fn le env) |
---|
| 510 | (dst:Σdst. fn_env_has … f dst ty) |
---|
| 511 | on e: Σf':partial_fn le env. fn_contains … f f' ≝ |
---|
| 512 | match e return λty,e.expr_vars ty e (Env_has env) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn le env. fn_contains … f f' with |
---|
| 513 | [ Id t i ⇒ λEnv,dst. |
---|
| 514 | let r ≝ lookup_reg env i t Env in |
---|
[766] | 515 | match register_eq r dst with |
---|
[1316] | 516 | [ inl _ ⇒ «f, ?» |
---|
[1626] | 517 | | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?» |
---|
[766] | 518 | ] |
---|
[1626] | 519 | | Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const dst c) f ??, ?» |
---|
| 520 | | Op1 t t' op e' ⇒ λEnv,dst. |
---|
| 521 | let ❬f,r❭ ≝ choose_reg … e' f Env in |
---|
| 522 | let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in |
---|
| 523 | let f ≝ add_expr … env ? e' Env f «r, ?» in |
---|
[1603] | 524 | «pi1 … f, ?» |
---|
[1626] | 525 | | Op2 _ _ _ op e1 e2 ⇒ λEnv,dst. |
---|
| 526 | let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in |
---|
| 527 | let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in |
---|
| 528 | let f ≝ add_fresh_to_graph … (St_op2 op dst r1 r2) f ?? in |
---|
| 529 | let f ≝ add_expr … env ? e2 (proj2 … Env) f «r2, ?» in |
---|
| 530 | let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in |
---|
[1603] | 531 | «pi1 … f, ?» |
---|
[1626] | 532 | | Mem _ _ q e' ⇒ λEnv,dst. |
---|
| 533 | let ❬f,r❭ ≝ choose_reg … e' f Env in |
---|
| 534 | let f ≝ add_fresh_to_graph … (St_load q r dst) f ?? in |
---|
| 535 | let f ≝ add_expr … env ? e' Env f «r,?» in |
---|
[1603] | 536 | «pi1 … f, ?» |
---|
[1626] | 537 | | Cond _ _ _ e' e1 e2 ⇒ λEnv,dst. |
---|
| 538 | let resume_at ≝ pf_entry … f in |
---|
| 539 | let f ≝ add_expr … env ? e2 (proj2 … Env) f dst in |
---|
| 540 | let lfalse ≝ pf_entry … f in |
---|
| 541 | let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in |
---|
| 542 | let f ≝ add_expr … env ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in |
---|
| 543 | let ❬f,r❭ ≝ choose_reg … e' f ? in |
---|
| 544 | let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in |
---|
| 545 | let f ≝ add_expr … env ? e' (proj1 … (proj1 … Env)) f «r, ?» in |
---|
[1603] | 546 | «pi1 … f, ?» |
---|
[1626] | 547 | | Ecost _ l e' ⇒ λEnv,dst. |
---|
| 548 | let f ≝ add_expr … env ? e' Env f dst in |
---|
| 549 | let f ≝ add_fresh_to_graph … (St_cost l) f ?? in |
---|
[1316] | 550 | «f, ?» |
---|
[1626] | 551 | ] Env dst. |
---|
[1316] | 552 | (* For new labels, we need to step back through the definitions of f until we |
---|
| 553 | hit the point that it was added. *) |
---|
[1626] | 554 | try (repeat @fn_contains_step @I) |
---|
[1316] | 555 | try (#l #H @H) |
---|
[1626] | 556 | try (#l @I) |
---|
| 557 | [ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ] |
---|
| 558 | | 2,6,7: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I |
---|
| 559 | | #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ] |
---|
| 560 | | @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I |
---|
| 561 | | @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I |
---|
| 562 | | #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ] |
---|
| 563 | | @(π1 (π1 Env)) |
---|
| 564 | | @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I |
---|
| 565 | | #l #H @(fn_con_graph … (pi2 ?? resume_at)) repeat @fn_contains_step @I |
---|
[1316] | 566 | ] qed. |
---|
[766] | 567 | |
---|
[1605] | 568 | let rec add_exprs (le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es) |
---|
[1626] | 569 | (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le env) |
---|
| 570 | (Hdsts:All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn le env. fn_contains le env f f' ≝ |
---|
| 571 | match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with |
---|
| 572 | [ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn le env. fn_contains le env f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ] |
---|
[1316] | 573 | | cons e et ⇒ λEnv. |
---|
[1626] | 574 | match dsts return λx. All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with |
---|
| 575 | [ nil ⇒ λ_.λpf.⊥ |
---|
| 576 | | cons r rt ⇒ λHdsts,pf. |
---|
| 577 | let f' ≝ add_exprs ? env et ? rt ? f ? in |
---|
| 578 | match e return λe.exprtyp_present ? e → fn_env_has le env f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr. |
---|
| 579 | let f'' ≝ add_expr ? env ty e ? f' r in |
---|
| 580 | «pi1 … f'', ?» |
---|
| 581 | ] (proj1 ?? Env) (π1 Hdsts) |
---|
[766] | 582 | ] |
---|
[1626] | 583 | ] Env Hdsts pf. |
---|
| 584 | try (repeat @fn_contains_step @I) |
---|
[1464] | 585 | [ 1,2: normalize in pf; destruct |
---|
[1316] | 586 | | @Env |
---|
[1626] | 587 | | @(fn_con_env … Hr) repeat @fn_contains_step @I |
---|
[1316] | 588 | | @(proj2 … Env) |
---|
[1464] | 589 | | normalize in pf; destruct @e0 |
---|
[1626] | 590 | | @(π2 Hdsts) |
---|
[1464] | 591 | ] qed. |
---|
[766] | 592 | |
---|
[797] | 593 | axiom UnknownLabel : String. |
---|
| 594 | axiom ReturnMismatch : String. |
---|
| 595 | |
---|
[1316] | 596 | definition stmt_inv : env → label_env → stmt → Prop ≝ |
---|
[1626] | 597 | λenv,lenv. stmt_P (λs. stmt_vars (Env_has env) s ∧ stmt_labels (present ?? lenv) s). |
---|
[1316] | 598 | |
---|
| 599 | (* Trick to avoid multiplying the proof obligations for the non-Id cases. *) |
---|
| 600 | definition expr_is_Id : ∀t. expr t → option ident ≝ |
---|
| 601 | λt,e. match e with |
---|
| 602 | [ Id _ id ⇒ Some ? id |
---|
| 603 | | _ ⇒ None ? |
---|
| 604 | ]. |
---|
| 605 | |
---|
| 606 | (* XXX Work around odd disambiguation errors. *) |
---|
| 607 | alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)". |
---|
| 608 | alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,14,0)". |
---|
| 609 | |
---|
| 610 | definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝ |
---|
| 611 | λA,P,m,l,n. |
---|
| 612 | match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with |
---|
| 613 | [ None ⇒ λ_. Error ? m |
---|
| 614 | | Some a ⇒ λH'. OK ? «a, ?» |
---|
[1603] | 615 | ] (All_nth A P n l (pi2 … l)). |
---|
[1316] | 616 | @H' @refl qed. |
---|
| 617 | |
---|
| 618 | lemma lookup_label_rev : ∀lenv,l,l',p. |
---|
| 619 | lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'. |
---|
| 620 | #lenv #l #l' #p |
---|
| 621 | cut (∃lx. lookup ?? lenv l = Some ? lx) |
---|
[1516] | 622 | [ whd in p; cases (lookup ?? lenv l) in p ⊢ %; |
---|
[1316] | 623 | [ * #H cases (H (refl ??)) |
---|
| 624 | | #lx #_ %{lx} @refl |
---|
| 625 | ] |
---|
[1516] | 626 | | * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl |
---|
[1316] | 627 | ] qed. |
---|
| 628 | |
---|
| 629 | lemma lookup_label_rev' : ∀lenv,l,p. |
---|
| 630 | lookup ?? lenv l = Some ? (lookup_label lenv l p). |
---|
| 631 | #lenv #l #p @lookup_label_rev [ @p | @refl ] |
---|
| 632 | qed. |
---|
| 633 | |
---|
| 634 | lemma lookup_label_lpresent : ∀lenv,l,p. |
---|
| 635 | lpresent lenv (lookup_label lenv l p). |
---|
| 636 | #le #l #p whd %{l} @lookup_label_rev' |
---|
| 637 | qed. |
---|
| 638 | |
---|
[1626] | 639 | lemma empty_Cminor_labels_added : ∀le,env,s,f'. |
---|
| 640 | labels_of s = [ ] → Cminor_labels_added le env s f'. |
---|
| 641 | #le #env #s #f' #E whd >E #l *; |
---|
[1316] | 642 | qed. |
---|
| 643 | |
---|
[1626] | 644 | lemma equal_Cminor_labels_added : ∀le,env,s,s',f. |
---|
| 645 | labels_of s = labels_of s' → Cminor_labels_added … s' f → |
---|
| 646 | Cminor_labels_added le env s f. |
---|
| 647 | #le #env #s #s' #f #E whd in ⊢ (% → %); > E #H @H |
---|
[1316] | 648 | qed. |
---|
| 649 | |
---|
[1626] | 650 | lemma Cminor_labels_con : ∀le,env,s,f,f'. |
---|
| 651 | fn_contains le env f f' → |
---|
| 652 | Cminor_labels_added … s f → |
---|
| 653 | Cminor_labels_added … s f'. |
---|
| 654 | #le #env #s #f #f' #INC #ADDED |
---|
[1464] | 655 | #l #E cases (ADDED l E) #l' * #L #P |
---|
| 656 | %{l'} % [ @L | @(present_included … P) @INC ] |
---|
[1316] | 657 | qed. |
---|
| 658 | |
---|
[1626] | 659 | lemma Cminor_labels_inv : ∀le,env,s,s',f. |
---|
| 660 | ∀f':Σf':partial_fn le env. add_stmt_inv le env s' f f'. |
---|
| 661 | Cminor_labels_added le env s f → |
---|
| 662 | Cminor_labels_added le env s f'. |
---|
| 663 | #le #env #s #s' #f * #f' * #H1 #H2 #H3 |
---|
[1316] | 664 | #l #E cases (H3 l E) #l' * #L #P |
---|
[1464] | 665 | %{l'} % [ @L | @(present_included … P) @H1 ] |
---|
[1316] | 666 | qed. |
---|
| 667 | |
---|
[1626] | 668 | lemma Cminor_labels_sig : ∀le,env,s,f. |
---|
| 669 | ∀f':Σf':partial_fn le env. fn_contains … f f'. |
---|
| 670 | Cminor_labels_added … s f → |
---|
| 671 | Cminor_labels_added … s f'. |
---|
| 672 | #le #env #s #f * #f' #H1 #H2 |
---|
[1316] | 673 | #l #E cases (H2 l E) #l' * #L #P |
---|
[1464] | 674 | %{l'} % [ @L | @(present_included … P) @H1 ] |
---|
[1316] | 675 | qed. |
---|
| 676 | |
---|
[1626] | 677 | let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) (exits:Σls:list label. All ? (present ?? (pf_graph … f)) ls) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝ |
---|
| 678 | match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with |
---|
[1316] | 679 | [ St_skip ⇒ λ_. OK ? «f, ?» |
---|
[1626] | 680 | | St_assign t x e ⇒ λEnv. |
---|
| 681 | let dst ≝ lookup_reg env x t (π1 (π1 Env)) in |
---|
| 682 | OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?» |
---|
[1316] | 683 | | St_store _ _ q e1 e2 ⇒ λEnv. |
---|
[1626] | 684 | let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in |
---|
| 685 | let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in |
---|
| 686 | let f ≝ add_fresh_to_graph … (St_store q addr_reg val_reg) f ?? in |
---|
| 687 | let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in |
---|
| 688 | OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) f «val_reg, ?»), ?» |
---|
[1316] | 689 | | St_call return_opt_id e args ⇒ λEnv. |
---|
| 690 | let return_opt_reg ≝ |
---|
| 691 | match return_opt_id return λo. ? → ? with |
---|
| 692 | [ None ⇒ λ_. None ? |
---|
[1626] | 693 | | Some idty ⇒ λEnv. Some ? (lookup_reg env (\fst idty) (\snd idty) ?) |
---|
[1316] | 694 | ] Env in |
---|
[1626] | 695 | let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in |
---|
[1316] | 696 | let f ≝ |
---|
| 697 | match expr_is_Id ? e with |
---|
[1626] | 698 | [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ?? |
---|
[1316] | 699 | | None ⇒ |
---|
[1626] | 700 | let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (π1 Env))) in |
---|
| 701 | let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in |
---|
| 702 | «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) f «fnr, ?»), ?» |
---|
[1316] | 703 | ] in |
---|
[1626] | 704 | OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?» |
---|
[1316] | 705 | | St_tailcall e args ⇒ λEnv. |
---|
[1626] | 706 | let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in |
---|
[1316] | 707 | let f ≝ |
---|
| 708 | match expr_is_Id ? e with |
---|
[1626] | 709 | [ Some id ⇒ add_fresh_to_graph … (λ_. St_tailcall_id id args_regs) f ?? |
---|
[1316] | 710 | | None ⇒ |
---|
[1626] | 711 | let ❬f,fnr❭ ≝ choose_reg … e f (π1 (π1 Env)) in |
---|
| 712 | let f ≝ add_fresh_to_graph … (λ_. St_tailcall_ptr fnr args_regs) f ?? in |
---|
| 713 | «pi1 … (add_expr ? env ? e (π1 (π1 Env)) f «fnr, ?»), ?» |
---|
[1316] | 714 | ] in |
---|
[1626] | 715 | OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?» |
---|
[1316] | 716 | | St_seq s1 s2 ⇒ λEnv. |
---|
| 717 | do f2 ← add_stmt env label_env s2 ? f «exits, ?»; |
---|
| 718 | do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»; |
---|
[1603] | 719 | OK ? «pi1 … f1, ?» |
---|
[1316] | 720 | | St_ifthenelse _ _ e s1 s2 ⇒ λEnv. |
---|
[1626] | 721 | let l_next ≝ pf_entry … f in |
---|
[1316] | 722 | do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»; |
---|
[1626] | 723 | let l2 ≝ pf_entry … f2 in |
---|
| 724 | let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in |
---|
[1316] | 725 | do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»; |
---|
[1626] | 726 | let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in |
---|
| 727 | let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in |
---|
| 728 | OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?» |
---|
[1316] | 729 | | St_loop s ⇒ λEnv. |
---|
[1626] | 730 | let f ≝ add_fresh_to_graph … R_skip f ?? in (* dummy statement, fill in afterwards *) |
---|
| 731 | let l_loop ≝ pf_entry … f in |
---|
[1316] | 732 | do f ← add_stmt env label_env s (π2 Env) f «exits, ?»; |
---|
[1626] | 733 | OK ? «pi1 … (fill_in_statement … l_loop (R_skip (pf_entry … f)) f ??), ?» |
---|
[1316] | 734 | | St_block s ⇒ λEnv. |
---|
[1626] | 735 | do f ← add_stmt env label_env s (π2 Env) f («pf_entry … f::exits, ?»); |
---|
[1603] | 736 | OK ? «pi1 … f, ?» |
---|
[1316] | 737 | | St_exit n ⇒ λEnv. |
---|
| 738 | do l ← nth_sig ?? (msg BadCminorProgram) exits n; |
---|
[1626] | 739 | OK ? «pi1 … (add_fresh_to_graph … (λ_. R_skip l) f ??), ?» |
---|
[1316] | 740 | | St_switch sz sg e tab n ⇒ λEnv. |
---|
[1626] | 741 | let ❬f,r❭ ≝ choose_reg … e f ? in |
---|
[1316] | 742 | do l_default ← nth_sig ?? (msg BadCminorProgram) exits n; |
---|
[1626] | 743 | let f ≝ add_fresh_to_graph … (λ_. R_skip l_default) f ?? in |
---|
| 744 | do f ← foldr ? (res (Σf':partial_fn ??. ?)) (λcs,f. |
---|
[771] | 745 | do f ← f; |
---|
| 746 | let 〈i,n〉 ≝ cs in |
---|
[1626] | 747 | let ❬f,cr❭ ≝ fresh_reg … f (ASTint sz sg) in |
---|
| 748 | let ❬f,br❭ ≝ fresh_reg … f (ASTint I8 Unsigned) in |
---|
[1316] | 749 | do l_case ← nth_sig ?? (msg BadCminorProgram) exits n; |
---|
[1626] | 750 | let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in |
---|
| 751 | let f ≝ add_fresh_to_graph … (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ?? in |
---|
| 752 | let f ≝ add_fresh_to_graph … (St_const cr (Ointconst ? i)) f ?? in |
---|
[1603] | 753 | OK ? «pi1 … f, ?») (OK ? f) tab; |
---|
[1626] | 754 | OK ? «pi1 … (add_expr ? env ? e (π1 Env) f «r, ?»), ?» |
---|
[1316] | 755 | | St_return opt_e ⇒ let f0 ≝ f in |
---|
[1626] | 756 | let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in |
---|
| 757 | match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return o) f0 f') with |
---|
[1603] | 758 | [ None ⇒ λEnv. OK ? «pi1 … f, ?» |
---|
[1316] | 759 | | Some e ⇒ |
---|
[1626] | 760 | match pf_result … f with |
---|
[1316] | 761 | [ None ⇒ λEnv. Error ? (msg ReturnMismatch) |
---|
| 762 | | Some r ⇒ |
---|
[1626] | 763 | match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return (Some ? e)) f0 f') with |
---|
| 764 | [ mk_DPair ty e ⇒ λEnv. |
---|
| 765 | match typ_eq (\snd r) ty with |
---|
| 766 | [ inl E ⇒ let f ≝ add_expr label_env env ty e ? f «\fst r, ? E (* XXX E goes missing if I don't use it! *)» in |
---|
| 767 | OK ? «pi1 … f, ?» |
---|
| 768 | | inr _ ⇒ Error ? (msg ReturnMismatch) |
---|
| 769 | ] |
---|
| 770 | ] |
---|
[766] | 771 | ] |
---|
| 772 | ] |
---|
[1316] | 773 | | St_label l s' ⇒ λEnv. |
---|
| 774 | do f ← add_stmt env label_env s' (π2 Env) f exits; |
---|
| 775 | let l' ≝ lookup_label label_env l ? in |
---|
[1626] | 776 | OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?» |
---|
[1316] | 777 | | St_goto l ⇒ λEnv. |
---|
| 778 | let l' ≝ lookup_label label_env l ? in |
---|
[1626] | 779 | OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?» |
---|
[1316] | 780 | | St_cost l s' ⇒ λEnv. |
---|
| 781 | do f ← add_stmt env label_env s' (π2 Env) f exits; |
---|
[1626] | 782 | OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?» |
---|
[1316] | 783 | ] Env. |
---|
| 784 | try @(π1 Env) |
---|
| 785 | try @(π2 Env) |
---|
| 786 | try @(π1 (π1 Env)) |
---|
| 787 | try @(π2 (π1 Env)) |
---|
| 788 | try @mk_add_stmt_inv |
---|
[1626] | 789 | try (repeat @fn_contains_step @I) |
---|
[1316] | 790 | try (@empty_Cminor_labels_added @refl) |
---|
| 791 | try (#l #H @I) |
---|
| 792 | try (#l #H @H) |
---|
[1626] | 793 | try (#l @I) |
---|
| 794 | [ @(pf_envok … (π1 (π1 Env))) @refl |
---|
| 795 | | @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I |
---|
| 796 | | @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I |
---|
| 797 | | 4,8: @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I |
---|
| 798 | | 5,9: @sym_eq @(All2_length … (pi2 ?? args_regs)) |
---|
| 799 | | 6,10: @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I |
---|
| 800 | | @(π1 (π1 (π1 Env))) |
---|
| 801 | | 11,13,14,19,20: (@(All_mp … (pi2 ?? exits))) #i #H @(fn_con_graph … H) repeat @fn_contains_step @I |
---|
[1316] | 802 | | #l #H cases (Exists_append … H) |
---|
[1626] | 803 | [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1) |
---|
| 804 | | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ????? (pi2 ?? f2)) |
---|
[1316] | 805 | ] |
---|
[1626] | 806 | | #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I |
---|
[1316] | 807 | | #l #H cases (Exists_append … H) |
---|
[1626] | 808 | [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f1)) |
---|
| 809 | | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f2)) |
---|
[1316] | 810 | ] |
---|
[1626] | 811 | | @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I |
---|
| 812 | | #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ] |
---|
| 813 | | @(pi2 … (pf_entry …)) |
---|
| 814 | | @Cminor_labels_sig @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ] |
---|
[1603] | 815 | | % [ @pi2 | @(pi2 ?? exits) ] |
---|
[1626] | 816 | | @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ] |
---|
| 817 | | #l' #H @(pi2 … l) |
---|
| 818 | | #l #H @(fn_con_graph … (pi2 ?? l_default)) repeat @fn_contains_step @I |
---|
| 819 | | @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I |
---|
| 820 | | #l #H % [ @(fn_con_graph … (pi2 ?? l_case)) repeat @fn_contains_step @I | @H ] |
---|
| 821 | | #_ (* see above *) <E @(pi2 ?? r) |
---|
[1611] | 822 | | @(pi2 … (pf_entry …)) |
---|
[1316] | 823 | | #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ] |
---|
[1626] | 824 | | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f)) |
---|
[1316] | 825 | ] |
---|
| 826 | | #l1 #H whd %2 @lookup_label_lpresent |
---|
[1626] | 827 | | @(equal_Cminor_labels_added ??? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f)) ] |
---|
[1316] | 828 | ] qed. |
---|
[766] | 829 | |
---|
[1631] | 830 | notation > "hvbox('let' ❬ident x,ident y❭ 'as' ident E ≝ t 'in' s)" |
---|
| 831 | with precedence 10 |
---|
| 832 | for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒ |
---|
| 833 | λ${ident E}.$s ] (refl ? $t) }. |
---|
[1626] | 834 | |
---|
[764] | 835 | definition c2ra_function (*: internal_function → internal_function*) ≝ |
---|
| 836 | λf. |
---|
[766] | 837 | let labgen0 ≝ new_universe LabelTag in |
---|
[764] | 838 | let reggen0 ≝ new_universe RegisterTag in |
---|
[766] | 839 | let cminor_labels ≝ labels_of (f_body f) in |
---|
[1316] | 840 | let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in |
---|
| 841 | let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in |
---|
[1631] | 842 | let ❬locals_reggen, result❭ as E3 ≝ |
---|
[1626] | 843 | match f_return f return λ_.𝚺lr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt)) with |
---|
| 844 | [ None ⇒ ❬〈locals0, reggen2〉, None ?❭ |
---|
[887] | 845 | | Some ty ⇒ |
---|
[1056] | 846 | let 〈r,gen〉 ≝ fresh … reggen2 in |
---|
[1626] | 847 | mk_DPair ? (λlr.option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt))) 〈〈r,ty〉::locals0, gen〉 (Some ? «〈r,ty〉, ?») ] in |
---|
| 848 | let locals ≝ \fst locals_reggen in |
---|
| 849 | let reggen ≝ \snd locals_reggen in |
---|
[1316] | 850 | let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in |
---|
[1056] | 851 | let 〈l,labgen〉 ≝ fresh … labgen1 in |
---|
[766] | 852 | let emptyfn ≝ |
---|
[1316] | 853 | mk_partial_fn |
---|
| 854 | label_env |
---|
[1626] | 855 | env |
---|
[764] | 856 | labgen |
---|
[766] | 857 | reggen |
---|
[764] | 858 | params |
---|
| 859 | locals |
---|
[1626] | 860 | result |
---|
| 861 | ? |
---|
[764] | 862 | (f_stacksize f) |
---|
[766] | 863 | (add ?? (empty_map …) l St_return) |
---|
[1316] | 864 | ? |
---|
[1626] | 865 | ? |
---|
[766] | 866 | l |
---|
| 867 | l in |
---|
[1316] | 868 | do f ← add_stmt env label_env (f_body f) ? emptyfn [ ]; |
---|
| 869 | OK ? (mk_internal_function |
---|
[1626] | 870 | (pf_labgen … f) |
---|
| 871 | (pf_reggen … f) |
---|
| 872 | (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? (pi1 … rt) ]) |
---|
| 873 | (pf_params … f) |
---|
| 874 | (pf_locals … f) |
---|
| 875 | (pf_stacksize … f) |
---|
| 876 | (pf_graph … f) |
---|
[1316] | 877 | ? |
---|
[1626] | 878 | (pf_typed … f) |
---|
| 879 | (pf_entry … f) |
---|
| 880 | (pf_exit … f) |
---|
[1316] | 881 | ). |
---|
| 882 | [ @I |
---|
| 883 | | -emptyfn @(stmt_P_mp … (f_inv f)) |
---|
| 884 | #s * #V #L % |
---|
| 885 | [ @(stmt_vars_mp … V) |
---|
[1626] | 886 | #i #t #H cases (Exists_append … H) |
---|
[1631] | 887 | [ #H1 @(populate_extends … (sym_eq … E2)) |
---|
| 888 | [ @(populates_env_distinct … (sym_eq … E1)) // |
---|
| 889 | @All_alt // |
---|
| 890 | | @(populates_env … (sym_eq … E1)) [ @distinct_env_append_l // | @H1 ] |
---|
| 891 | ] |
---|
| 892 | | #H1 @(populates_env … (sym_eq … E2)) /2/ @H1 |
---|
| 893 | ] |
---|
[1316] | 894 | | @(stmt_labels_mp … L) |
---|
| 895 | #l #H @(populates_label_env … (sym_eq … El)) @H |
---|
| 896 | ] |
---|
[1626] | 897 | | #l #s #E @(labels_P_mp … (pf_closed … f l s E)) |
---|
[1316] | 898 | #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?) |
---|
| 899 | [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ] |
---|
| 900 | #P' @P' |
---|
| 901 | | cases (label_env_contents … (sym_eq ??? El) l ?) |
---|
| 902 | [ #H @H |
---|
[1516] | 903 | | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??)) |
---|
[1316] | 904 | | whd >H % #E' destruct (E') |
---|
| 905 | ] |
---|
| 906 | ] |
---|
| 907 | ] |
---|
[1631] | 908 | | #id #ty #r #H #L cases (populate_env_list … (sym_eq … E2) … H L) |
---|
| 909 | [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1) |
---|
| 910 | [ * * | normalize @Exists_append_r ] |
---|
| 911 | | cases (f_return f) in E3; |
---|
| 912 | [ whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct |
---|
| 913 | @Exists_append_l |
---|
| 914 | | #rt cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct |
---|
| 915 | #H' @Exists_append_l %2 @H' |
---|
| 916 | ] |
---|
| 917 | ] |
---|
[1316] | 918 | | #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP) |
---|
| 919 | [ * #E1 #E2 >E2 @I |
---|
[1516] | 920 | | whd in ⊢ (??%? → ?); #E' destruct (E') |
---|
[1316] | 921 | ] |
---|
[1626] | 922 | | #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP) |
---|
| 923 | [ * #E1 #E2 >E2 @I |
---|
| 924 | | whd in ⊢ (??%? → ?); #E' destruct (E') |
---|
| 925 | ] |
---|
| 926 | | 7,8: whd >lookup_add_hit % #E destruct |
---|
| 927 | | % @refl |
---|
[1316] | 928 | ] |
---|
[1070] | 929 | qed. |
---|
[764] | 930 | |
---|
[1139] | 931 | definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝ |
---|
[1224] | 932 | λp.transform_partial_program … p (transf_partial_fundef … c2ra_function). |
---|
[766] | 933 | |
---|
| 934 | include "Cminor/initialisation.ma". |
---|
| 935 | |
---|
[1139] | 936 | definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝ |
---|
[1316] | 937 | λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'. |
---|