Changeset 1105 for Deliverables/D3.3/idlookupbranch/Cminor/toRTLabs.ma
 Timestamp:
 Aug 10, 2011, 5:17:58 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/Cminor/toRTLabs.ma
r1104 r1105 79 79 ] qed. 80 80 81 lemma label_env_contents : ∀ls,lbls,u,lbls',u'. 82 populate_label_env lbls u ls = 〈lbls',u'〉 → 83 ∀l. present ?? lbls' l → Exists ? (λl'.l = l') ls ∨ present ?? lbls l. 84 #ls elim ls 85 [ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H 86  #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?) 87 change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???) 88 lapply (refl ? (populate_label_env lbls u t)) 89 cases (populate_label_env lbls u t) in ⊢ (???% → %) 90 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?) 91 #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ] 92 #l #H cases (identifier_eq ? l h) 93 [ #El %1 %1 @El 94  #NE cases (IH … E1 l ?) 95 [ #H' %1 %2 @H'  #H' %2 @H'  whd in H >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/ ] 96 ] 97 ] qed. 98 81 99 definition lookup_reg : ∀e:env. ∀id. present ?? e id → register ≝ lookup_present ??. 82 100 definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??. 83 101 102 (* Check that the domain of one graph is included in another, for monotonicity 103 properties. Note that we don't say anything about the statements. *) 104 definition graph_included : graph statement → graph statement → Prop ≝ 105 λg1,g2. ∀l. present ?? g1 l → present ?? g2 l. 106 107 lemma graph_inc_trans : ∀g1,g2,g3. 108 graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3. 109 #g1 #g2 #g3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed. 110 111 definition lpresent ≝ λlbls:label_env. λl. ∃l'. lookup ?? lbls l' = Some ? l. 112 113 definition partially_closed : label_env → graph statement → Prop ≝ 114 λe,g. ∀l,s. lookup ?? g l = Some ? s → labels_P (λl. present ?? g l ∨ lpresent e l) s. 115 116 (* I'd use a single parametrised definition along with internal_function, but 117 it's a pain without implicit parameters. *) 118 record partial_fn (lenv:label_env) : Type[0] ≝ 119 { pf_labgen : universe LabelTag 120 ; pf_reggen : universe RegisterTag 121 ; pf_result : option (register × typ) 122 ; pf_params : list (register × typ) 123 ; pf_locals : list (register × typ) 124 ; pf_stacksize : nat 125 ; pf_graph : graph statement 126 ; pf_closed : partially_closed lenv pf_graph 127 ; pf_entry : Σl:label. present ?? pf_graph l 128 ; pf_exit : Σl:label. present ?? pf_graph l 129 }. 130 131 inductive fn_graph_included (le:label_env) (f1:partial_fn le) (f2:partial_fn le) : Prop ≝ 132  fn_graph_inc : graph_included (pf_graph ? f1) (pf_graph ? f2) → fn_graph_included le f1 f2. 133 134 lemma fn_graph_inc_trans : ∀le,f1,f2,f3. 135 fn_graph_included le f1 f2 → fn_graph_included le f2 f3 → fn_graph_included le f1 f3. 136 #le #f1 #f2 #f3 * #H1 * #H2 % @(graph_inc_trans … H1 H2) qed. 137 138 lemma fn_graph_included_refl : ∀label_env,f. 139 fn_graph_included label_env f f. 140 #le #f % #l #H @H qed. 141 142 lemma fn_graph_included_sig : ∀label_env,f,f0. 143 ∀f':Σf':partial_fn label_env. fn_graph_included ? f0 f'. 144 fn_graph_included label_env f f0 → 145 fn_graph_included label_env f f'. 146 #le #f #f0 * #f' #H1 #H2 @(fn_graph_inc_trans … H2 H1) 147 qed. 148 149 lemma add_statement_inv : ∀le,l,s.∀f. 150 labels_present (pf_graph le f) s → 151 partially_closed le (add … (pf_graph ? f) l s). 152 #le #l #s #f #p 153 #l' #s' #H cases (identifier_eq … l l') 154 [ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //] 155 @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H 156  #NE @(labels_P_mp … (pf_closed ? f l' s' ?)) 157 [ #lx * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ] 158  >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/ 159 ] 160 ] qed. 161 84 162 (* Add a statement to the graph, *without* updating the entry label. *) 85 definition fill_in_statement : label → statement → internal_function → internal_function ≝ 86 λl,s,f. 87 mk_internal_function (f_labgen f) (f_reggen f) 88 (f_result f) (f_params f) (f_locals f) 89 (f_stacksize f) (add ?? (f_graph f) l s) 90 (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?). 91 @lookup_add_oblivious @use_sig 92 qed. 163 definition fill_in_statement : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝ 164 λle,l,s,f,p. 165 mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f) 166 (pf_result ? f) (pf_params ? f) (pf_locals ? f) 167 (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ? 168 «pf_entry ? f, ?» «pf_exit ? f, ?». 169 [ @add_statement_inv @p 170  2,3: @lookup_add_oblivious @use_sig 171  % #l' @lookup_add_oblivious 172 ] qed. 93 173 94 174 (* Add a statement to the graph, making it the entry label. *) 95 definition add_to_graph : label → statement → internal_function → internal_function ≝ 96 λl,s,f. 97 mk_internal_function (f_labgen f) (f_reggen f) 98 (f_result f) (f_params f) (f_locals f) 99 (f_stacksize f) (add ?? (f_graph f) l s) 100 (dp ?? l ?) (dp ?? (f_exit f) ?). 101 [ >lookup_add_hit % #E destruct 175 definition add_to_graph : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝ 176 λle,l,s,f,p. 177 mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f) 178 (pf_result ? f) (pf_params ? f) (pf_locals ? f) 179 (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ? 180 «l, ?» «pf_exit ? f, ?». 181 [ @add_statement_inv @p 182  whd >lookup_add_hit % #E destruct 102 183  @lookup_add_oblivious @use_sig 184  % #l' @lookup_add_oblivious 103 185 ] qed. 104 186 105 187 (* Add a statement with a fresh label to the start of the function. The 106 188 statement is parametrised by the *next* instruction's label. *) 107 definition add_fresh_to_graph : (label → statement) → internal_function → internal_function ≝ 108 λs,f. 109 let 〈l,g〉 ≝ fresh … (f_labgen f) in 110 let s' ≝ s (f_entry f) in 111 (mk_internal_function g (f_reggen f) 112 (f_result f) (f_params f) (f_locals f) 113 (f_stacksize f) (add ?? (f_graph f) l s') 114 (dp ?? l ?) (dp ?? (f_exit f) ?)). 115 [ >lookup_add_hit % #E destruct 189 definition add_fresh_to_graph : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_present (pf_graph ? f) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝ 190 λle,s,f,p. 191 let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in 192 let s' ≝ s (pf_entry ? f) in 193 (mk_partial_fn le g (pf_reggen ? f) 194 (pf_result ? f) (pf_params ? f) (pf_locals ? f) 195 (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ? 196 «l, ?» «pf_exit ? f, ?»). 197 [ % #l' @lookup_add_oblivious 198  @add_statement_inv @p @use_sig 199  whd >lookup_add_hit % #E destruct 116 200  @lookup_add_oblivious @use_sig 117 201 ] qed. 118 202 119 definition fresh_reg : internal_function → typ → register × internal_function ≝ 120 λf,ty. 121 let 〈r,g〉 ≝ fresh … (f_reggen f) in 122 〈r, mk_internal_function (f_labgen f) g 123 (f_result f) (f_params f) (〈r,ty〉::(f_locals f)) 124 (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 203 (* Variants for labels which are (goto) labels *) 204 205 lemma add_statement_inv' : ∀le,l,s.∀f. 206 labels_P (λl. present ?? (pf_graph le f) l ∨ lpresent le l) s → 207 partially_closed le (add … (pf_graph ? f) l s). 208 #le #l #s #f #p 209 #l' #s' #H cases (identifier_eq … l l') 210 [ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //] 211 @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ] 212  #NE @(labels_P_mp … (pf_closed ? f l' s' ?)) 213 [ #lx * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ] 214  >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/ 215 ] 216 ] qed. 217 218 definition add_fresh_to_graph' : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_P (λl.present ?? (pf_graph ? f) l ∨ lpresent le l) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝ 219 λle,s,f,p. 220 let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in 221 let s' ≝ s (pf_entry ? f) in 222 (mk_partial_fn le g (pf_reggen ? f) 223 (pf_result ? f) (pf_params ? f) (pf_locals ? f) 224 (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ? 225 «l, ?» «pf_exit ? f, ?»). 226 [ % #l' @lookup_add_oblivious 227  @add_statement_inv' @p @use_sig 228  whd >lookup_add_hit % #E destruct 229  @lookup_add_oblivious @use_sig 230 ] qed. 231 232 definition fresh_reg : ∀le. ∀f:partial_fn le. typ → register × (Σf':partial_fn le. fn_graph_included le f f') ≝ 233 λle,f,ty. 234 let 〈r,g〉 ≝ fresh … (pf_reggen ? f) in 235 〈r, «mk_partial_fn le (pf_labgen ? f) g 236 (pf_result ? f) (pf_params ? f) (〈r,ty〉::(pf_locals ? f)) 237 (pf_stacksize ? f) (pf_graph ? f) (pf_closed ? f) (pf_entry ? f) (pf_exit ? f), ?»〉. 238 % #l // qed. 125 239 126 240 axiom UnknownVariable : String. 127 241 128 definition choose_reg : ∀ env:env.∀ty.∀e:expr ty. internal_function → expr_vars ty e (present ?? env) → register × internal_function≝129 λ env,ty,e,f.130 match e return λty,e. expr_vars ty e (present ?? env) → register × internal_functionwith131 [ Id _ i ⇒ λEnv. 〈lookup_reg env i Env, f〉132  _ ⇒ λ_.fresh_reg f ty242 definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') ≝ 243 λle,env,ty,e,f. 244 match e return λty,e. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') with 245 [ Id _ i ⇒ λEnv. 〈lookup_reg env i Env, «f, ?»〉 246  _ ⇒ λ_.fresh_reg le f ty 133 247 ]. 248 % // qed. 134 249 135 250 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 ≝ … … 138 253 definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ]. 139 254 140 definition choose_regs : ∀ env:env. ∀es:list (Σt:typ.expr t).141 internal_function →All ? (exprtyp_present env) es →142 list register × internal_function≝143 λ env,es,f,Env.255 definition choose_regs : ∀le. ∀env:env. ∀es:list (Σt:typ.expr t). 256 ∀f:partial_fn le. All ? (exprtyp_present env) es → 257 list register × (Σf':partial_fn le. fn_graph_included le f f') ≝ 258 λle,env,es,f,Env. 144 259 foldr_all (Σt:typ.expr t) ?? 145 260 (λe,p,acc. let 〈rs,f〉 ≝ acc in 146 let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg env t e f ? ] p in 147 〈r::rs,f'〉) 〈[ ], f〉 es Env. 148 @p qed. 261 let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg le env t e (eject … f) ? ] p in 262 〈r::rs,«eject … f', ?»〉) 〈[ ], «f, ?»〉 es Env. 263 [ @p 264  @fn_graph_inc_trans [ 3: @(use_sig ?? f')  skip  @(use_sig ?? f) ] 265  % // 266 ] qed. 149 267 150 268 lemma extract_pair : ∀A,B,C,D. ∀u:A×B. ∀Q:A → B → C×D. ∀x,y. … … 154 272 155 273 156 lemma choose_regs_length : ∀ env,es,f,p,rs,f'.157 choose_regs env es f p = 〈rs,f'〉 → es = rs.158 # env #es #f elim es274 lemma choose_regs_length : ∀le,env,es,f,p,rs,f'. 275 choose_regs le env es f p = 〈rs,f'〉 → es = rs. 276 #le #env #es #f elim es 159 277 [ #p #rs #f normalize #E destruct @refl 160 278  * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E … … 168 286 ] qed. 169 287 288 lemma present_inc : ∀le,f,l. 289 ∀f':Σf':partial_fn le. fn_graph_included le f f'. 290 present ?? (pf_graph le f) l → 291 present ?? (pf_graph le f') l. 292 #le #f #l * #f' * #H1 #H2 @H1 @H2 qed. 293 170 294 axiom BadCminorProgram : String. 171 295 172 let rec add_expr ( env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:internal_function) on e: internal_function≝173 match e return λty,e.expr_vars ty e (present ?? env) → internal_functionwith296 let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:partial_fn le) on e: Σf':partial_fn le. fn_graph_included le f f' ≝ 297 match e return λty,e.expr_vars ty e (present ?? env) → Σf':partial_fn le. fn_graph_included le f f' with 174 298 [ Id _ i ⇒ λEnv. 175 299 let r ≝ lookup_reg env i Env in 176 300 match register_eq r dst with 177 [ inl _ ⇒ f178  inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f301 [ inl _ ⇒ «f, ?» 302  inr _ ⇒ «eject … (add_fresh_to_graph ? (St_op1 Oid dst r) f ?), ?» 179 303 ] 180  Cst _ c ⇒ λ_. add_fresh_to_graph (St_const dst c) f304  Cst _ c ⇒ λ_. «add_fresh_to_graph ? (St_const dst c) f ?, ?» 181 305  Op1 _ _ op e' ⇒ λEnv. 182 let 〈r,f〉 ≝ choose_reg env ? e' f Env in 183 let f ≝ add_fresh_to_graph (St_op1 op dst r) f in 184 add_expr env ? e' Env r f 306 let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in 307 let f ≝ add_fresh_to_graph ? (St_op1 op dst r) f ? in 308 let f ≝ add_expr ? env ? e' Env r f in 309 «eject … f, ?» 185 310  Op2 _ _ _ op e1 e2 ⇒ λEnv. 186 let 〈r1,f〉 ≝ choose_reg env ? e1 f (proj1 … Env) in 187 let 〈r2,f〉 ≝ choose_reg env ? e2 f (proj2 … Env) in 188 let f ≝ add_fresh_to_graph (St_op2 op dst r1 r2) f in 189 let f ≝ add_expr env ? e2 (proj2 … Env) r2 f in 190 add_expr env ? e1 (proj1 … Env) r1 f 311 let 〈r1,f〉 ≝ choose_reg ? env ? e1 f (proj1 … Env) in 312 let 〈r2,f〉 ≝ choose_reg ? env ? e2 f (proj2 … Env) in 313 let f ≝ add_fresh_to_graph ? (St_op2 op dst r1 r2) f ? in 314 let f ≝ add_expr ? env ? e2 (proj2 … Env) r2 f in 315 let f ≝ add_expr ? env ? e1 (proj1 … Env) r1 f in 316 «eject … f, ?» 191 317  Mem _ _ q e' ⇒ λEnv. 192 let 〈r,f〉 ≝ choose_reg env ? e' f Env in 193 let f ≝ add_fresh_to_graph (St_load q r dst) f in 194 add_expr env ? e' Env r f 318 let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in 319 let f ≝ add_fresh_to_graph ? (St_load q r dst) f ? in 320 let f ≝ add_expr ? env ? e' Env r f in 321 «eject … f, ?» 195 322  Cond _ _ _ e' e1 e2 ⇒ λEnv. 196 let resume_at ≝ f_entry f in 197 let f ≝ add_expr env ? e2 (proj2 … Env) dst f in 198 let lfalse ≝ f_entry f in 199 let f ≝ add_fresh_to_graph (λ_.St_skip resume_at) f in 200 let f ≝ add_expr env ? e1 (proj2 … (proj1 … Env)) dst f in 201 let 〈r,f〉 ≝ choose_reg env ? e' f (proj1 … (proj1 … Env)) in 202 let f ≝ add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f in 203 add_expr env ? e' (proj1 … (proj1 … Env)) r f 323 let resume_at ≝ pf_entry ? f in 324 let f ≝ add_expr ? env ? e2 (proj2 … Env) dst f in 325 let lfalse ≝ pf_entry ? f in 326 let f ≝ add_fresh_to_graph ? (λ_.St_skip resume_at) f ? in 327 let f ≝ add_expr ? env ? e1 (proj2 … (proj1 … Env)) dst f in 328 let 〈r,f〉 as E ≝ choose_reg ? env ? e' f (proj1 … (proj1 … Env)) in 329 let f ≝ add_fresh_to_graph ? (λltrue. St_cond r ltrue lfalse) f ? in 330 let f ≝ add_expr ? env ? e' (proj1 … (proj1 … Env)) r f in 331 «eject … f, ?» 204 332  Ecost _ l e' ⇒ λEnv. 205 let f ≝ add_expr env ? e' Env dst f in 206 add_fresh_to_graph (St_cost l) f 333 let f ≝ add_expr ? env ? e' Env dst f in 334 let f ≝ add_fresh_to_graph ? (St_cost l) f ? in 335 «f, ?» 207 336 ] Env. 208 209 let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es) 210 (dsts:list register) (pf:es=dsts) (f:internal_function) on es: internal_function ≝ 337 (* For new labels, we need to step back through the definitions of f until we 338 hit the point that it was added. *) 339 try @fn_graph_included_refl 340 try (#l #H @H) 341 [ 7: #l #H whd % [ @H  342 @present_inc 343 @present_inc 344 @present_inc 345 @(use_sig ? (present ???)) ] 346  8: #l #H 347 @present_inc 348 @(use_sig ? (present ???)) 349 (* For the monotonicity properties, we just keep going back until we're at the 350 start. The repeat tactical helps here. *) 351  *: repeat @fn_graph_included_sig @fn_graph_included_refl 352 ] qed. 353 354 let rec add_exprs (le:label_env) (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es) 355 (dsts:list register) (pf:es=dsts) (f:partial_fn le) on es: Σf':partial_fn le. fn_graph_included le f f' ≝ 211 356 match es return λes.All ?? es → es=dsts → ? with 212 [ nil ⇒ λ_. match dsts return λx. ?=x → ? with [ nil ⇒ λ_. f cons _ _ ⇒ λpf.⊥ ]357 [ nil ⇒ λ_. match dsts return λx. ?=x → Σf':partial_fn le. fn_graph_included le f f' with [ nil ⇒ λ_. «f, ?»  cons _ _ ⇒ λpf.⊥ ] 213 358  cons e et ⇒ λEnv. 214 359 match dsts return λx. ?=x → ? with 215 360 [ nil ⇒ λpf.⊥ 216 361  cons r rt ⇒ λpf. 217 let f ≝ add_exprs env et ? rt ? f in 218 match e return λe.? → ? with [ dp ty e ⇒ λEnv. add_expr env ty e ? r f ] (proj1 ?? Env) 362 let f ≝ add_exprs ? env et ? rt ? f in 363 match e return λe.exprtyp_present ? e → ? with [ dp ty e ⇒ λEnv. 364 let f ≝ add_expr ? env ty e ? r f in 365 «eject … f, ?» ] (proj1 ?? Env) 219 366 ] 220 367 ] Env pf. 221 [ 1,2,3: normalize in pf; destruct // 222  whd in Env @(proj2 … Env) 368 [ // 369  2,3: normalize in pf; destruct 370  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl 371  @Env 372  @(proj2 … Env) 223 373  normalize in pf; destruct @e0 ] qed. 224 374 … … 229 379 λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s). 230 380 231 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (exits:list label) (f:internal_function) on s : res internal_function ≝ 232 match s return λs.stmt_inv env label_env s → res internal_function with 233 [ St_skip ⇒ λ_. OK ? f 381 (* Trick to avoid multiplying the proof obligations for the nonId cases. *) 382 definition expr_is_Id : ∀t. expr t → option ident ≝ 383 λt,e. match e with 384 [ Id _ id ⇒ Some ? id 385  _ ⇒ None ? 386 ]. 387 388 (* XXX Work around odd disambiguation errors. *) 389 alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)". 390 alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,14,0)". 391 392 definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝ 393 λA,P,m,l,n. 394 match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with 395 [ None ⇒ λ_. Error ? m 396  Some a ⇒ λH'. OK ? «a, ?» 397 ] (All_nth A P n l (use_sig … l)). 398 @H' @refl qed. 399 400 lemma lookup_label_rev : ∀lenv,l,l',p. 401 lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'. 402 #lenv #l #l' #p 403 cut (∃lx. lookup ?? lenv l = Some ? lx) 404 [ whd in p; cases (lookup ?? lenv l) in p ⊢ % 405 [ * #H cases (H (refl ??)) 406  #lx #_ %{lx} @refl 407 ] 408  * #lx #E whd in ⊢ (??%? → ?) cases p >E #q whd in ⊢ (??%? → ?) #E' >E' @refl 409 ] qed. 410 411 lemma lookup_label_rev' : ∀lenv,l,p. 412 lookup ?? lenv l = Some ? (lookup_label lenv l p). 413 #lenv #l #p @lookup_label_rev [ @p  @refl ] 414 qed. 415 416 lemma lookup_label_lpresent : ∀lenv,l,p. 417 lpresent lenv (lookup_label lenv l p). 418 #le #l #p whd %{l} @lookup_label_rev' 419 qed. 420 421 (* We need to show that the graph only grows, and that Cminor labels will end 422 up in the graph. *) 423 definition Cminor_labels_added ≝ λle,s,f'. 424 ∀l. Exists ? (λl'.l=l') (labels_of s) → 425 ∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'. 426 427 record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝ 428 { stmt_graph_inc : fn_graph_included ? f f' 429 ; stmt_labels_added : Cminor_labels_added le s f' 430 }. 431 432 lemma empty_Cminor_labels_added : ∀le,s,f'. 433 labels_of s = [ ] → Cminor_labels_added le s f'. 434 #le #s #f' #E whd >E #l *; 435 qed. 436 437 lemma equal_Cminor_labels_added : ∀le,s,s',f. 438 labels_of s = labels_of s' → Cminor_labels_added le s' f → 439 Cminor_labels_added le s f. 440 #le #s #s' #f #E whd in ⊢ (% → %) > E #H @H 441 qed. 442 443 lemma fn_graph_included_inv : ∀label_env,s,f,f0. 444 ∀f':Σf':partial_fn label_env. add_stmt_inv label_env s f0 f'. 445 fn_graph_included label_env f f0 → 446 fn_graph_included label_env f f'. 447 #label_env #s #f #f0 * #f' * #H1 #H2 #H3 448 @(fn_graph_inc_trans … H3 H1) 449 qed. 450 451 lemma present_inc' : ∀le,s,f,l. 452 ∀f':(Σf':partial_fn le. add_stmt_inv le s f f'). 453 present ?? (pf_graph le f) l → 454 present ?? (pf_graph le f') l. 455 #le #s #f #l * #f' * * #H1 #H2 #H3 456 @H1 @H3 457 qed. 458 459 lemma Cminor_labels_inv : ∀le,s,s',f. 460 ∀f':Σf':partial_fn le. add_stmt_inv le s' f f'. 461 Cminor_labels_added le s f → 462 Cminor_labels_added le s f'. 463 #le #s #s' #f * #f' * #H1 #H2 #H3 464 #l #E cases (H3 l E) #l' * #L #P 465 %{l'} % [ @L  @present_inc' @P ] 466 qed. 467 468 lemma Cminor_labels_sig : ∀le,s,f. 469 ∀f':Σf':partial_fn le. fn_graph_included le f f'. 470 Cminor_labels_added le s f → 471 Cminor_labels_added le s f'. 472 #le #s #f * #f' #H1 #H2 473 #l #E cases (H2 l E) #l' * #L #P 474 %{l'} % [ @L  @present_inc @P ] 475 qed. 476 477 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env) (exits:Σls:list label. All ? (present ?? (pf_graph ? f)) ls) on s : res (Σf':partial_fn label_env. add_stmt_inv label_env s f f') ≝ 478 match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env. add_stmt_inv ? s f f') with 479 [ St_skip ⇒ λ_. OK ? «f, ?» 234 480  St_assign _ x e ⇒ λEnv. 235 481 let dst ≝ lookup_reg env x (π1 (π1 Env)) in 236 OK ? (add_expr env ? e (π2 (π1 Env)) dst f)482 OK ? «eject … (add_expr ? env ? e (π2 (π1 Env)) dst f), ?» 237 483  St_store _ _ q e1 e2 ⇒ λEnv. 238 let 〈val_reg, f〉 ≝ choose_reg env ? e2 f (π2 (π1 Env)) in239 let 〈addr_reg, f〉 ≝ choose_reg env ? e1 f (π1 (π1 Env)) in240 let f ≝ add_fresh_to_graph (St_store q addr_reg val_reg) fin241 let f ≝ add_expr env ? e1 (π1 (π1 Env)) addr_reg f in242 OK ? (add_expr env ? e2 (π2 (π1 Env)) val_reg f)484 let 〈val_reg, f〉 ≝ choose_reg ? env ? e2 f (π2 (π1 Env)) in 485 let 〈addr_reg, f〉 ≝ choose_reg ? env ? e1 f (π1 (π1 Env)) in 486 let f ≝ add_fresh_to_graph ? (St_store q addr_reg val_reg) f ? in 487 let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) addr_reg f in 488 OK ? «eject … (add_expr ? env ? e2 (π2 (π1 Env)) val_reg f), ?» 243 489  St_call return_opt_id e args ⇒ λEnv. 244 490 let return_opt_reg ≝ … … 247 493  Some id ⇒ λEnv. Some ? (lookup_reg env id ?) 248 494 ] Env in 249 let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (π2 (π1 Env)) in495 let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in 250 496 let f ≝ 251 match e with252 [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f253  _⇒254 let 〈fnr, f〉 ≝ choose_reg env ? e f (π2 (π1 (π1 Env))) in255 let f ≝ add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) fin256 add_expr env ? e (π2 (π1 (π1 Env))) fnr f497 match expr_is_Id ? e with 498 [ Some id ⇒ add_fresh_to_graph ? (St_call_id id args_regs return_opt_reg) f ? 499  None ⇒ 500 let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π2 (π1 (π1 Env))) in 501 let f ≝ add_fresh_to_graph ? (St_call_ptr fnr args_regs return_opt_reg) f ? in 502 «eject … (add_expr ? env ? e (π2 (π1 (π1 Env))) fnr f), ?» 257 503 ] in 258 OK ? (add_exprs env args (π2 (π1 Env)) args_regs ? f)504 OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?» 259 505  St_tailcall e args ⇒ λEnv. 260 let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (π2 (π1 Env)) in506 let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in 261 507 let f ≝ 262 match e with263 [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f264  _⇒265 let 〈fnr, f〉 ≝ choose_reg env ? e f (π1 (π1 Env)) in266 let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) fin267 add_expr env ? e (π1 (π1 Env)) fnr f508 match expr_is_Id ? e with 509 [ Some id ⇒ add_fresh_to_graph ? (λ_. St_tailcall_id id args_regs) f ? 510  None ⇒ 511 let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π1 (π1 Env)) in 512 let f ≝ add_fresh_to_graph ? (λ_. St_tailcall_ptr fnr args_regs) f ? in 513 «eject … (add_expr ? env ? e (π1 (π1 Env)) fnr f), ?» 268 514 ] in 269 OK ? (add_exprs env args (π2 (π1 Env)) args_regs ? f)515 OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?» 270 516  St_seq s1 s2 ⇒ λEnv. 271 do f ← add_stmt env label_env s2 ? exits f; 272 add_stmt env label_env s1 ? exits f 517 do f2 ← add_stmt env label_env s2 ? f «exits, ?»; 518 do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»; 519 OK ? «eject … f1, ?» 273 520  St_ifthenelse _ _ e s1 s2 ⇒ λEnv. 274 let l_next ≝ f_entryf in275 do f ← add_stmt env label_env s2 (π2 Env) exits f;276 let l2 ≝ f_entry fin277 let f ≝ add_fresh_to_graph ? ( * XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) fin278 do f ← add_stmt env label_env s1 (π2 (π1 Env)) exits f;279 let 〈r,f〉 ≝ choose_reg env ? e f(π1 (π1 (π1 Env))) in280 let f ≝ add_fresh_to_graph (λl1. St_cond r l1 l2) fin281 OK ? (add_expr env ? e (π1 (π1 (π1 Env))) r f)521 let l_next ≝ pf_entry ? f in 522 do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»; 523 let l2 ≝ pf_entry ? f2 in 524 let f ≝ add_fresh_to_graph ? (λ_. R_skip l_next) f2 ? in 525 do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»; 526 let 〈r,f〉 ≝ choose_reg ? env ? e f1 (π1 (π1 (π1 Env))) in 527 let f ≝ add_fresh_to_graph ? (λl1. St_cond r l1 l2) f ? in 528 OK ? «eject … (add_expr ? env ? e (π1 (π1 (π1 Env))) r f), ?» 282 529  St_loop s ⇒ λEnv. 283 let f ≝ add_fresh_to_graph ? fin (* dummy statement, fill in afterwards *)284 let l_loop ≝ f_entryf in285 do f ← add_stmt env label_env s (π2 Env) exits f;286 OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)530 let f ≝ add_fresh_to_graph ? R_skip f ? in (* dummy statement, fill in afterwards *) 531 let l_loop ≝ pf_entry ? f in 532 do f ← add_stmt env label_env s (π2 Env) f «exits, ?»; 533 OK ? «eject … (fill_in_statement ? l_loop (R_skip (pf_entry ? f)) f ?), ?» 287 534  St_block s ⇒ λEnv. 288 add_stmt env label_env s (π2 Env) ((f_entry f)::exits) f 535 do f ← add_stmt env label_env s (π2 Env) f («pf_entry ? f::exits, ?»); 536 OK ? «eject … f, ?» 289 537  St_exit n ⇒ λEnv. 290 do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);291 OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f)538 do l ← nth_sig ?? (msg BadCminorProgram) exits n; 539 OK ? «eject … (add_fresh_to_graph ? (λ_. R_skip l) f ?), ?» 292 540  St_switch sz sg e tab n ⇒ λEnv. 293 let 〈r,f〉 ≝ choose_reg env ? e f ? in294 do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);295 let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? fin296 do f ← foldr ? ?(λcs,f.541 let 〈r,f〉 ≝ choose_reg ? env ? e f ? in 542 do l_default ← nth_sig ?? (msg BadCminorProgram) exits n; 543 let f ≝ add_fresh_to_graph ? (λ_. R_skip l_default) f ? in 544 do f ← foldr ? (res (Σf':partial_fn ?. ?)) (λcs,f. 297 545 do f ← f; 298 546 let 〈i,n〉 ≝ cs in 299 547 let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in 300 548 let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in 301 do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 302 let f ≝ add_fresh_to_graph (St_cond br l_case) f in 303 let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in 304 OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab; 305 OK ? (add_expr env ? e (π1 Env) r f) 306  St_return opt_e ⇒ 307 let f ≝ add_fresh_to_graph (λ_. St_return) f in 308 match opt_e return λo. ? → ? with 309 [ None ⇒ λEnv. OK ? f 310  Some e ⇒ 311 match f_result f with 549 do l_case ← nth_sig ?? (msg BadCminorProgram) exits n; 550 let f ≝ add_fresh_to_graph ? (St_cond br l_case) f ? in 551 let f ≝ add_fresh_to_graph ? (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ? in 552 let f ≝ add_fresh_to_graph ? (St_const cr (Ointconst ? i)) f ? in 553 OK ? «eject … f, ?») (OK ? f) tab; 554 OK ? «eject … (add_expr ? env ? e (π1 Env) r f), ?» 555  St_return opt_e ⇒ let f0 ≝ f in 556 let f ≝ add_fresh_to_graph ? (λ_. R_return) f ? in 557 match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env.add_stmt_inv ? (St_return o) f0 f') with 558 [ None ⇒ λEnv. OK ? «eject … f, ?» 559  Some e ⇒ 560 match pf_result ? f with 312 561 [ None ⇒ λEnv. Error ? (msg ReturnMismatch) 313  Some r ⇒ match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ? e ? (\fst r) f) ] 562  Some r ⇒ 563 match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env.add_stmt_inv label_env (St_return (Some ? e)) f0 f') with 564 [ dp ty e ⇒ λEnv. let f ≝ add_expr label_env env ty e ? (\fst r) f in 565 OK ? «eject … f, ?» ] 314 566 ] 315 567 ] 316 568  St_label l s' ⇒ λEnv. 317 do f ← add_stmt env label_env s' (π2 Env) exits f;569 do f ← add_stmt env label_env s' (π2 Env) f exits; 318 570 let l' ≝ lookup_label label_env l ? in 319 OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)571 OK ? «eject … (add_to_graph ? l' (R_skip (pf_entry ? f)) f ?), ?» 320 572  St_goto l ⇒ λEnv. 321 573 let l' ≝ lookup_label label_env l ? in 322 OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f)574 OK ? «eject … (add_fresh_to_graph' ? (λ_.R_skip l') f ?), ?» 323 575  St_cost l s' ⇒ λEnv. 324 do f ← add_stmt env label_env s' (π2 Env) exits f;325 OK ? (add_fresh_to_graph (St_cost l) f)576 do f ← add_stmt env label_env s' (π2 Env) f exits; 577 OK ? «eject … (add_fresh_to_graph ? (St_cost l) f ?), ?» 326 578 ] Env. 327 579 try @(π1 Env) … … 329 581 try @(π1 (π1 Env)) 330 582 try @(π2 (π1 Env)) 583 try @mk_add_stmt_inv 584 try (@empty_Cminor_labels_added @refl) 585 try (@(All_mp … (use_sig ?? exits))) 586 try @fn_graph_included_refl 587 try (repeat @fn_graph_included_inv repeat @fn_graph_included_sig @fn_graph_included_refl) 588 try (#l #H @I) 589 try (#l #H @H) 331 590 [ f @(choose_regs_length … (sym_eq … Eregs)) 591  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl 332 592  whd in Env @(π1 (π1 (π1 Env))) 333 593  f @(choose_regs_length … (sym_eq … Eregs)) 334  @(λ_. St_skip l_next) 335  @(St_skip (f_entry f)) 336  @St_skip 337  @(λ_. St_skip l) 338  @(λ_. St_skip l_default) 339  @(St_skip (f_entry f)) 340  @(λ_.St_skip l') 341 ] qed. 342 594  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl 595  #l #H cases (Exists_append … H) 596 [ #H1 @(stmt_labels_added ???? (use_sig ?? f1) ? H1) 597  #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (use_sig ?? f2)) 598 ] 599  #l #H @present_inc' @H 600  #l #H @present_inc' @use_sig 601  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl 602  #l #H cases (Exists_append … H) 603 [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f1)) 604  #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f2)) 605 ] 606  #l #H % [ @H  @present_inc @present_inc' @present_inc @(use_sig ?? (pf_entry ? f2)) ] 607  #l #H @present_inc @present_inc' @H 608  #l #H @present_inc @H 609  @(use_sig ?? (pf_entry ??)) 610  @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_refl 611  @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl  @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ] 612  % [ @use_sig  @(use_sig ?? exits) ] 613  @(equal_Cminor_labels_added ?? s) [ @refl  @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ] 614  #l #H @use_sig 615  #l #H @present_inc @use_sig 616  #l #H % [ @present_inc @present_inc @present_inc @present_inc @use_sig  @H ] 617  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl 618  @use_sig 619  @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl 620  #l1 * [ #E >E %{l'} % [ @lookup_label_rev'  whd >lookup_add_hit % #E' destruct (E') ] 621 @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) 622 ] 623  #l1 #H whd %2 @lookup_label_lpresent 624  @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl 625  @(equal_Cminor_labels_added ?? s') [ @refl  @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ] 626 ] qed. 627 628 (* 629 definition mk_fn : ∀le. partial_fn le → internal_function ≝ 630 λle, f. 631 mk_internal_function 632 (pf_labgen ? f) 633 (pf_reggen ? f) 634 (pf_result ? f) 635 (pf_params ? f) 636 (pf_locals ? f) 637 (pf_stacksize ? f) 638 (pf_graph ? f) 639 ? 640 (pf_entry ? f) 641 (pf_exit ? f). 642 #l #s #E @(labels_P_mp … (pf_closed ? f l s E)) 643 #l' * [ //  #H 644 *) 343 645 344 646 definition c2ra_function (*: internal_function → internal_function*) ≝ … … 358 660 let 〈l,labgen〉 ≝ fresh … labgen1 in 359 661 let emptyfn ≝ 360 mk_internal_function 662 mk_partial_fn 663 label_env 361 664 labgen 362 665 reggen … … 366 669 (f_stacksize f) 367 670 (add ?? (empty_map …) l St_return) 671 ? 368 672 l 369 673 l in 370 do f ← add_stmt env label_env (f_body f) ? [ ] emptyfn; 371 do u1 ← check_universe_ok ? (f_labgen f); 372 do u2 ← check_universe_ok ? (f_reggen f); 373 OK ? f 374 . 375 [ @(stmt_P_mp … (f_inv f)) 674 do f ← add_stmt env label_env (f_body f) ? emptyfn [ ]; 675 do u1 ← check_universe_ok ? (pf_labgen ? f); 676 do u2 ← check_universe_ok ? (pf_reggen ? f); 677 OK ? (mk_internal_function 678 (pf_labgen ? f) 679 (pf_reggen ? f) 680 (pf_result ? f) 681 (pf_params ? f) 682 (pf_locals ? f) 683 (pf_stacksize ? f) 684 (pf_graph ? f) 685 ? 686 (pf_entry ? f) 687 (pf_exit ? f) 688 ). 689 [ @I 690  emptyfn @(stmt_P_mp … (f_inv f)) 376 691 #s * #V #L % 377 692 [ @(stmt_vars_mp … V) … … 384 699 #l #H @(populates_label_env … (sym_eq … El)) @H 385 700 ] 386  *: >lookup_add_hit % #E destruct 701  #l #s #E @(labels_P_mp … (pf_closed ? f l s E)) 702 #l' * [ //  * #l #H cases f #f' * #L #P cases (P l ?) 703 [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ] 704 #P' @P' 705  cases (label_env_contents … (sym_eq ??? El) l ?) 706 [ #H @H 707  whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?) * #H cases (H (refl ??)) 708  whd >H % #E' destruct (E') 709 ] 710 ] 711 ] 712  #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP) 713 [ * #E1 #E2 >E2 @I 714  whd in ⊢ (??%? → ?) #E' destruct (E') 715 ] 716  *: whd >lookup_add_hit % #E destruct 387 717 ] 388 718 qed.
Note: See TracChangeset
for help on using the changeset viewer.