Changeset 1087
 Timestamp:
 Jul 25, 2011, 2:58:10 PM (9 years ago)
 Location:
 Deliverables/D3.3/idlookupbranch
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/Clight/toCminor.ma
r1078 r1087 153 153 definition var_types ≝ identifier_map SymbolTag var_type. 154 154 155 axiom UndeclaredIdentifier : String. 156 157 definition lookup' ≝ 158 λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id). 159 160 definition local_id : var_types → ident → Prop ≝ 161 λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False  _ ⇒ True ]  _ ⇒ False ]. 162 155 163 (* Note that the semantics allows locals to shadow globals. 156 164 Parameters start out as locals, but get stack allocated if their address … … 168 176 definition characterise_vars : list (ident×region) → function → var_types × nat ≝ 169 177 λglobals, f. 170 let m ≝ foldl ?? (λm,idr. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in 171 let m ≝ foldl ?? (λm,v. add ?? m (\fst v) Local) m (fn_params f) in 178 let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in 172 179 let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in 173 let 〈m,stacksize〉 ≝ fold l ?? (λms,v.180 let 〈m,stacksize〉 ≝ foldr ?? (λv,ms. 174 181 let 〈m,stack_high〉 ≝ ms in 175 182 let 〈id,ty〉 ≝ v in … … 180 187 〈m,stacksize〉. 181 188 189 lemma local_id_add_global : ∀vars,id,r,id'. 190 local_id (add ?? vars id (Global r)) id' → local_id vars id'. 191 #var #id #r #id' 192 whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?] → ?) 193 cases (identifier_eq ? id id') 194 [ #E >E >lookup_add_hit whd in ⊢ (% → ?) * 195  #NE >lookup_add_miss // @eq_identifier_elim // #E >E in NE * /2/ 196 ] qed. 197 198 lemma local_id_add_miss : ∀vars,id,t,id'. 199 id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'. 200 #vars #id #t #id' #NE 201 whd in ⊢ (% → %) 202 whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ] → match % with [ _ ⇒ ?  _ ⇒ ? ]) 203 >lookup_add_miss 204 [ #H @H  @eq_identifier_elim // #E >E in NE * /2/ ] 205 qed. 206 207 lemma contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e. 208 #A #B * // qed. 209 210 lemma extract_pair : ∀A,B,C,D. ∀u:A×B. ∀Q:A → B → C×D. ∀x,y. 211 ((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) → 212 ∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉. 213 #A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed. 214 215 include "utilities/extralib.ma". (* for pair_eq1 to work around destruct's excessive normalisation *) 216 217 lemma characterise_vars_all : ∀l,f,vars,n. 218 characterise_vars l f = 〈vars,n〉 → 219 ∀i. local_id vars i → 220 Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f). 221 #globals #f 222 whd in ⊢ (∀_.∀_.??%? → ?) 223 elim (fn_params f @ fn_vars f) 224 [ #vars #n whd in ⊢ (??%? → ?) #E <(pair_eq1 ?????? E) E; #i #H @False_ind 225 elim globals in H 226 [ normalize // 227  * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H) 228 ] 229  * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i 230 cases (identifier_eq ? id i) 231 [ #E' <E' #H % @refl 232  #NE #H whd %2 >(contract_pair var_types nat ?) in E; 233 whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?) 234 cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?) 235 #H' lapply (extract_pair ???????? H') H' * #m0 * #n0 * #EQ #EQ2 236 @(IH m0 n0) 237 [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ 238  2,4: <(pair_eq1 ?????? EQ2) in H #H' @(local_id_add_miss … H') @NE 239 ] 240 ] 241 ] qed. 182 242 183 243 include "Cminor/syntax.ma". … … 186 246 alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)". 187 247 188 axiom UndeclaredIdentifier : String.189 248 axiom BadlyTypedAccess : String. 190 249 axiom BadLvalue : String. … … 324 383 ]. 325 384 385 lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e. 386 expr_vars ? e1 P → 387 expr_vars ? e2 P → 388 translate_binop op ty1 e1 ty2 e2 ty = OK ? e → 389 expr_vars ? e P. 390 #P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2 391 whd in ⊢ (??%? → ?) 392 [ cases (classify_add ty1 ty2) 393 [ 3,4: #z ] whd in ⊢ (??%? → ?) 394 [ generalize in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ])? → ?) 395 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 396 whd in c:(??%?); destruct % [ @H1  % // @H2 ] 397  generalize in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ])? → ?) 398 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 399 whd in c:(??%?); destruct % [ @H2  % // @H1 ] 400  *: #E destruct (E) % try @H1 @H2 401 ] 402  cases (classify_sub ty1 ty2) 403 [ 3,4: #z] whd in ⊢ (??%? → ?) 404 [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ])? → ?) 405 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 406 whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I 407  *: #E destruct (E) % try @H1 try @H2 % // @H2 408 ] 409  cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct 410 % try @H1 @H2 411  cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct 412 % try @H1 @H2 413  cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct 414 % try @H1 @H2 415  6,7,8,9: #E destruct % try @H1 @H2 416  cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2 417  11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2 418 ] qed. 326 419 327 420 (* We'll need to implement proper translation of pointers if we really do memory … … 338 431 ]. 339 432 340 definition translate_ptr : ∀r1,r2. CMexpr (ASTptr r1) → res (CMexpr (ASTptr r2)) ≝ 341 λr1,r2,e. check_region r1 r2 ? e. 342 343 definition translate_cast : type → ∀ty2:type. CMexpr ? → res (CMexpr (typ_of_type ty2)) ≝ 344 λty1,ty2. 345 match ty1 return λx.CMexpr (typ_of_type x) → ? with 433 definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝ 434 λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e. 435 436 notation "hvbox(« term 19 a, break term 19 b»)" 437 with precedence 90 for @{ (dp ?? $a $b) }. 438 439 lemma sig_ok : ∀A:Type[0]. ∀P:A → Prop. ∀x:Σx:A.P x. 440 P x. 441 #A #P * #a #p @p 442 qed. 443 444 definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝ 445 λP,ty1,ty2. 446 match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with 346 447 [ Tint sz1 sg1 ⇒ λe. 347 match ty2 return λx.res ( CMexpr (typ_of_type x)) with448 match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with 348 449 [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sg1 sz2) e) 349 450  Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu  _ ⇒ Ofloatofint]) e) … … 353 454 ] 354 455  Tfloat sz1 ⇒ λe. 355 match ty2 return λx.res ( CMexpr (typ_of_type x)) with356 [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2  _ ⇒ Ointoffloat sz2 ]) e)357  Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e)(* FIXME *)456 match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with 457 [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2  _ ⇒ Ointoffloat sz2 ]) e, ?» 458  Tfloat sz2 ⇒ OK ? «Op1 ?? Oid e, ?» (* FIXME *) 358 459  _ ⇒ Error ? (msg TypeMismatch) 359 460 ] 360 461  Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *) 361 match ty2 return λx.res ( CMexpr (typ_of_type x)) with362 [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ointofptr sz2) e)363  Tarray r2 _ _ ⇒ translate_ptr r1 r2 e364  Tpointer r2 _ ⇒ translate_ptr r1 r2 e462 match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with 463 [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2) e, ?» 464  Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e 465  Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e 365 466  _ ⇒ Error ? (msg TypeMismatch) 366 467 ] 367 468  Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *) 368 match ty2 return λx.res ( CMexpr (typ_of_type x)) with369 [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e)370  Tarray r2 _ _ ⇒ translate_ptr r1 r2 e371  Tpointer r2 _ ⇒ translate_ptr r1 r2 e469 match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with 470 [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e, ?» 471  Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e 472  Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e 372 473  _ ⇒ Error ? (msg TypeMismatch) 373 474 ] 374 475  _ ⇒ λ_. Error ? (msg TypeMismatch) 375 ]. 476 ]. whd @sig_ok qed. 376 477 377 478 definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝ … … 404 505 ] qed. 405 506 406 let rec translate_expr (vars:var_types) (e:expr) on e : res (CMexpr (typ_of_type (typeof e))) ≝ 407 match e return λe. res (CMexpr (typ_of_type (typeof e))) with 507 definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B. 508 match f return λx. f = x → ? with 509 [ OK x ⇒ g x 510  Error msg ⇒ λ_. Error ? msg 511 ] (refl ? f). 512 513 notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}. 514 515 let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝ 516 match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with 408 517 [ Expr ed ty ⇒ 409 518 match ed with 410 [ Econst_int sz i ⇒ OK ? (Cst ? (Ointconst sz i))411  Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f))519 [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?» 520  Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?» 412 521  Evar id ⇒ 413 do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);414 match c with415 [ Global r ⇒ 522 do c as E ← lookup' vars id; 523 match c return λx.? = ? → res (Σe':CMexpr ?. ?) with 524 [ Global r ⇒ λ_. 416 525 match access_mode ty with 417 [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id 0)))418  By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id 0))526 [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?» 527  By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?» 419 528  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 420 529 ] 421  Stack n ⇒ 530  Stack n ⇒ λE. 422 531 match access_mode ty with 423 [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack n)))424  By_reference _ ⇒ OK ? (Cst ? (Oaddrstack n))532 [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?» 533  By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?» 425 534  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 426 535 ] 427  Local ⇒ OK ? (Id ? id)428 ] 536  Local ⇒ λE. OK ? «Id ? id, ?» 537 ] E 429 538  Ederef e1 ⇒ 430 539 do e1' ← translate_expr vars e1; 431 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with540 match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with 432 541 [ ASTptr r ⇒ λe1'. 433 match access_mode ty return λx.access_mode ty = x → res (CMexpr (typ_of_type ty)) with 434 [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1') 435  By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉ 542 match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with 543 [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (eject … e1'), ?» 544  By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1'; 545 OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉ 436 546  By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) 437 ] ( refl ? (access_mode ty))547 ] (access_mode_typ ty) 438 548  _ ⇒ λ_. Error ? (msg TypeMismatch) 439 549 ] e1' 440 550  Eaddrof e1 ⇒ 441 551 do e1' ← translate_addr vars e1; 442 match typ_of_type ty return λx.res ( CMexpr x) with552 match typ_of_type ty return λx.res (Σz:CMexpr x.?) with 443 553 [ ASTptr r ⇒ 444 554 match e1' with … … 450 560 do op' ← translate_unop ty op; 451 561 do e1' ← translate_expr vars e1; 452 OK ? (Op1 ?? op' e1')562 OK ? «Op1 ?? op' e1', ?» 453 563  Ebinop op e1 e2 ⇒ 454 564 do e1' ← translate_expr vars e1; 455 565 do e2' ← translate_expr vars e2; 456 translate_binop op (typeof e1) e1' (typeof e2) e2' ty 566 do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty; 567 OK ? «e', ?» 457 568  Ecast ty1 e1 ⇒ 458 569 do e1' ← translate_expr vars e1; 459 do e' ← translate_cast (typeof e1) ty1 e1'; 460 typ_should_eq ? (typ_of_type ty) ? e' 570 do e' ← translate_cast ? (typeof e1) ty1 e1'; 571 do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e'; 572 OK ? e' 461 573  Econdition e1 e2 e3 ⇒ 462 574 do e1' ← translate_expr vars e1; 463 575 do e2' ← translate_expr vars e2; 464 do e2' ← type_should_eq ? ty (λx. CMexpr (typ_of_type x)) e2';576 do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; 465 577 do e3' ← translate_expr vars e3; 466 do e3' ← type_should_eq ? ty (λx. CMexpr (typ_of_type x)) e3';467 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with468 [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' e3')578 do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3'; 579 match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? with 580 [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?» 469 581  _ ⇒ λ_.Error ? (msg TypeMismatch) 470 582 ] e1' … … 474 586 match ty with 475 587 [ Tint sz _ ⇒ 476 do e2' ← type_should_eq ? ty (λx. CMexpr (typ_of_type x)) e2';477 match typ_of_type (typeof e1) return λx. CMexpr x → res (CMexpr (typ_of_type ty))with478 [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))))588 do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; 589 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with 590 [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))), ?» 479 591  _ ⇒ λ_.Error ? (msg TypeMismatch) 480 592 ] e1' … … 486 598 match ty with 487 599 [ Tint sz _ ⇒ 488 do e2' ← type_should_eq ? ty (λx. CMexpr (typ_of_type x)) e2';489 match typ_of_type (typeof e1) return λx. CMexpr x → res (CMexpr (typ_of_type ty))with490 [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2')600 do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; 601 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with 602 [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2', ?» 491 603  _ ⇒ λ_.Error ? (msg TypeMismatch) 492 604 ] e1' … … 495 607  Esizeof ty1 ⇒ 496 608 match ty with 497 [ Tint sz _ ⇒ OK ? (Cst ? (Ointconst sz (repr ? (sizeof ty1))))609 [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?» 498 610  _ ⇒ Error ? (msg TypeMismatch) 499 611 ] 500 612  Efield e1 id ⇒ 501 do e' ←match typeof e1 with613 match typeof e1 with 502 614 [ Tstruct _ fl ⇒ 503 615 do e1' ← translate_addr vars e1; … … 506 618 do off ← field_offset id fl; 507 619 match access_mode ty with 508 [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))509  By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))))620 [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?» 621  By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?» 510 622  By_nothing ⇒ Error ? (msg BadlyTypedAccess) 511 623 ] … … 515 627 match e1' with 516 628 [ dp r e1' ⇒ 517 match access_mode ty return λx. access_mode ty = x → res (CMexpr (typ_of_type ty)) with 518 [ By_value q ⇒ λ_. OK ? (Mem ?? q e1') 519  By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈res (CMexpr (ASTptr r')) ↦ res (CMexpr (typ_of_type ty))⌉ 629 match access_mode ty return λx. access_mode ty = x → res ? with 630 [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?» 631  By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1'; 632 OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉ 520 633  By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) 521 634 ] (refl ? (access_mode ty)) 522 635 ] 523 636  _ ⇒ Error ? (msg BadlyTypedAccess) 524 ]; 525 typ_should_eq ? (typ_of_type ty) ? e' 637 ] 526 638  Ecost l e1 ⇒ 527 639 do e1' ← translate_expr vars e1; 528 do e' ← OK ? (Ecost ? l e1');529 typ_should_eq ? (typ_of_type ty) ?e'640 do e' ← OK ? «Ecost ? l e1',?»; 641 typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e' 530 642 ] 531 ] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. CMexpr (ASTptr r)) ≝643 ] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝ 532 644 match e with 533 645 [ Expr ed _ ⇒ … … 535 647 [ Evar id ⇒ 536 648 do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id); 537 match c return λ_. res (Σr. CMexpr (ASTptr r)) with538 [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id 0)))539  Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack n)))649 match c return λ_. res (Σr.Σz:CMexpr (ASTptr r).?) with 650 [ Global r ⇒ OK ? «r, «Cst ? (Oaddrsymbol id 0), ?»» 651  Stack n ⇒ OK ? «Any, «Cst ? (Oaddrstack n), ?»» 540 652  Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *) 541 653 ] 542 654  Ederef e1 ⇒ 543 655 do e1' ← translate_expr vars e1; 544 match typ_of_type (typeof e1) return λx. CMexpr x → res (Σr. CMexpr (ASTptr r)) with545 [ ASTptr r ⇒ λe1'.OK ? (dp ?? r e1')656 match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (Σr. Σz:CMexpr (ASTptr r). ?) with 657 [ ASTptr r ⇒ λe1'.OK ? «r, e1'» 546 658  _ ⇒ λ_.Error ? (msg BadlyTypedAccess) 547 659 ] e1' … … 552 664 do off ← field_offset id fl; 553 665 match e1' with 554 [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))666 [ dp r e1'' ⇒ OK (Σr:region.Σe:CMexpr (ASTptr r).?) («r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» ») 555 667 ] 556 668  Tunion _ _ ⇒ translate_addr vars e1 … … 560 672 ] 561 673 ]. 562 >(access_mode_typ … E) @refl 563 qed. 564 565 inductive destination : Type[0] ≝ 566  IdDest : ident → destination 567  MemDest : ∀r:region. memory_chunk → CMexpr (ASTptr r) → destination. 674 whd try @I 675 [ >E @I 676  >(E ? (refl ??)) @refl 677  3,4: @sig_ok 678  @(translate_binop_vars … E) @sig_ok 679  % [ % ] @sig_ok 680  % [ % @sig_ok ] whd @I 681  % [ % [ @sig_ok  @I ]  @sig_ok ] 682  % [ @sig_ok  @I ] 683  % [ @sig_ok  @I ] 684  >(access_mode_typ … E) @refl 685  @sig_ok 686  @sig_ok 687  % [ @sig_ok  @I ] 688 ] qed. 689 690 inductive destination (vars:var_types) : Type[0] ≝ 691  IdDest : ∀id:ident. local_id vars id → destination vars 692  MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars. 568 693 569 694 definition translate_dest ≝ … … 578 703 match ed1 with 579 704 [ Evar id ⇒ 580 do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);581 match c with582 [ Local ⇒ OK ? (IdDest id)583  Global r ⇒ OK ? (MemDestr q (Cst ? (Oaddrsymbol id 0)))584  Stack n ⇒ OK ? (MemDestAny q (Cst ? (Oaddrstack n)))585 ] 705 do c as E ← lookup' vars id; 706 match c return λx.? → ? with 707 [ Local ⇒ λE. OK ? (IdDest vars id ?) 708  Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0))) 709  Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n))) 710 ] E 586 711  _ ⇒ 587 712 do e1' ← translate_addr vars e1; 588 match e1' with [ dp r e1' ⇒ OK ? (MemDest r q e1') ]713 match e1' with [ dp r e1' ⇒ OK ? (MemDest ? r q e1') ] 589 714 ] 590 715 ]. 716 whd // >E @I 717 qed. 591 718 (* 592 719 definition translate_assign ≝ … … 614 741 ]. 615 742 *) 616 definition translate_assign ≝743 definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.stmt_vars s (local_id vars)) ≝ 617 744 λvars,e1,e2. 618 745 do e2' ← translate_expr vars e2; 619 746 do dest ← translate_dest vars e1 (typeof e2); 620 747 match dest with 621 [ IdDest id ⇒ OK ? (St_assign ? id e2') 622  MemDest r q e1' ⇒ OK ? (St_store ? r q e1' e2') 623 ]. 748 [ IdDest id p ⇒ OK ? «St_assign ? id e2', ?» 749  MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?» 750 ]. 751 whd 752 [ % // @sig_ok 753  % @sig_ok 754 ] qed. 624 755 625 756 definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝ … … 630 761 ]. 631 762 632 definition translate_expr_sigma : var_types → expr → res (Σt:typ.CMexpr t) ≝763 definition translate_expr_sigma : ∀vars:var_types. expr → res (Σe:(Σt:typ.CMexpr t). match e with [ dp t e ⇒ expr_vars t e (local_id vars) ]) ≝ 633 764 λv,e. 634 765 do e' ← translate_expr v e; 635 OK ? (dp ? (λt:typ.CMexpr t) ? e'). 766 OK (Σe:(Σt:typ.CMexpr t).?) ««?, e'», ?». 767 whd @sig_ok 768 qed. 636 769 637 770 axiom FIXME : String. 638 771 639 let rec translate_statement (vars:var_types) (tmp:ident) (tmpp:ident) (s:statement) on s : res stmt ≝ 772 let rec mmap_sigma (A,B:Type[0]) (P:B → Prop) (f:A → res (Σx:B.P x)) (l:list A) on l : res (Σl':list B.All B P l') ≝ 773 match l with 774 [ nil ⇒ OK ? «nil B, ?» 775  cons h t ⇒ 776 do h' ← f h; 777 do t' ← mmap_sigma A B P f t; 778 OK ? «cons B h' t', ?» 779 ]. 780 whd // % 781 [ @(sig_ok B P) 782  cases t' #l' #p @p 783 ] qed. 784 785 let rec translate_statement (vars:var_types) (tmp:Σi:ident.local_id vars i) (tmpp:Σi:ident.local_id vars i) (s:statement) on s : res (Σs:stmt.stmt_vars s (local_id vars)) ≝ 640 786 match s with 641 [ Sskip ⇒ OK ? St_skip787 [ Sskip ⇒ OK ? «St_skip, ?» 642 788  Sassign e1 e2 ⇒ translate_assign vars e1 e2 643 789  Scall ret ef args ⇒ 644 790 do ef' ← translate_expr vars ef; 645 do ef' ← typ_should_eq ?(ASTptr Code) ? ef';646 do args' ← mmap … (translate_expr_sigma vars) args;791 do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef'; 792 do args' ← mmap_sigma … (translate_expr_sigma vars) args; 647 793 match ret with 648 [ None ⇒ OK ? (St_call (None ?) ef' args')794 [ None ⇒ OK ? «St_call (None ?) ef' args', ?» 649 795  Some e1 ⇒ 650 796 do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *) 651 797 match dest with 652 [ IdDest id ⇒ OK ? (St_call (Some ? id) ef' args')798 [ IdDest id p ⇒ OK ? «St_call (Some ? id) ef' args', ?» 653 799  MemDest r q e1' ⇒ 654 800 let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp  _ ⇒ tmp ] in 655 OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)))801 OK ? «St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), ?» 656 802 ] 657 803 ] … … 659 805 do s1' ← translate_statement vars tmp tmpp s1; 660 806 do s2' ← translate_statement vars tmp tmpp s2; 661 OK ? (St_seq s1' s2')807 OK ? «St_seq s1' s2', ?» 662 808  Sifthenelse e1 s1 s2 ⇒ 663 809 do e1' ← translate_expr vars e1; 664 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with810 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 665 811 [ ASTint _ _ ⇒ λe1'. 666 812 do s1' ← translate_statement vars tmp tmpp s1; 667 813 do s2' ← translate_statement vars tmp tmpp s2; 668 OK ? (St_ifthenelse ?? e1' s1' s2')814 OK ? «St_ifthenelse ?? e1' s1' s2', ?» 669 815  _ ⇒ λ_.Error ? (msg TypeMismatch) 670 816 ] e1' 671 817  Swhile e1 s1 ⇒ 672 818 do e1' ← translate_expr vars e1; 673 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with819 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 674 820 [ ASTint _ _ ⇒ λe1'. 675 821 do s1' ← translate_statement vars tmp tmpp s1; 676 822 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 677 OK ? (St_block823 OK ? «St_block 678 824 (St_loop 679 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))) )825 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), ?» 680 826  _ ⇒ λ_.Error ? (msg TypeMismatch) 681 827 ] e1' 682 828  Sdowhile e1 s1 ⇒ 683 829 do e1' ← translate_expr vars e1; 684 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with830 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with 685 831 [ ASTint _ _ ⇒ λe1'. 686 832 do s1' ← translate_statement vars tmp tmpp s1; 687 833 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 688 OK ? (St_block834 OK ? «St_block 689 835 (St_loop 690 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))) )836 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), ?» 691 837  _ ⇒ λ_.Error ? (msg TypeMismatch) 692 838 ] e1' 693 839  Sfor s1 e1 s2 s3 ⇒ 694 840 do e1' ← translate_expr vars e1; 695 match typ_of_type (typeof e1) return λx. CMexpr x→ ? with841 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with 696 842 [ ASTint _ _ ⇒ λe1'. 697 843 do s1' ← translate_statement vars tmp tmpp s1; … … 699 845 do s3' ← translate_statement vars tmp tmpp s3; 700 846 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 701 OK ? (St_seq s1'847 OK ? «St_seq s1' 702 848 (St_block 703 849 (St_loop 704 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))) )850 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), ?» 705 851  _ ⇒ λ_.Error ? (msg TypeMismatch) 706 852 ] e1' 707  Sbreak ⇒ OK ? (St_exit 1)708  Scontinue ⇒ OK ? (St_exit 0)853  Sbreak ⇒ OK ? «St_exit 1, ?» 854  Scontinue ⇒ OK ? «St_exit 0, ?» 709 855  Sreturn ret ⇒ 710 856 match ret with 711 [ None ⇒ OK ? (St_return (None ?))857 [ None ⇒ OK ? «St_return (None ?), ?» 712 858  Some e1 ⇒ 713 859 do e1' ← translate_expr vars e1; 714 OK ? (St_return (Some ? (dp … e1')))860 OK ? «St_return (Some ? (dp … e1')), ?» 715 861 ] 716 862  Sswitch e1 ls ⇒ Error ? (msg FIXME) 717 863  Slabel l s1 ⇒ 718 864 do s1' ← translate_statement vars tmp tmpp s1; 719 OK ? (St_label l s1')720  Sgoto l ⇒ OK ? (St_goto l)865 OK ? «St_label l s1', ?» 866  Sgoto l ⇒ OK ? «St_goto l, ?» 721 867  Scost l s1 ⇒ 722 868 do s1' ← translate_statement vars tmp tmpp s1; 723 OK ? (St_cost l s1') 724 ]. 869 OK ? «St_cost l s1', ?» 870 ]. 871 whd try @I 872 [ % [ % [ @p  @sig_ok ]  @(sig_ok ? (All ??)) ] 873  % [ whd % [ % [ @sig_ok  @sig_ok ]  @(sig_ok ? (All ??)) ]  whd % @sig_ok ] 874  % [ % [ @I  @sig_ok ]  @(sig_ok ? (All ??)) ] 875  % @sig_ok 876  % [ % @sig_ok  @sig_ok ] 877  % [ % @sig_ok  whd @I ] 878  % [ @sig_ok  whd % [ % [ @sig_ok  @I ]  @I ] ] 879  % [ @sig_ok  whd % [ % [ @sig_ok  whd % @sig_ok ]  @I ] ] 880  @sig_ok 881  @sig_ok 882  @sig_ok 883 ] qed. 725 884 726 885 axiom ParamGlobalMixup : String. 727 886 728 definition alloc_params : var_types → list (ident×type) → stmt → res stmt≝887 definition alloc_params : ∀vars:var_types. list (ident×type) → (Σs:stmt.stmt_vars s (local_id vars)) → res (Σs:stmt.stmt_vars s (local_id vars)) ≝ 729 888 λvars,params,s. foldl ?? (λs,it. 730 889 let 〈id,ty〉 ≝ it in 731 890 do s ← s; 732 do t ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);733 match t with734 [ Local ⇒ OK ?s735  Stack n ⇒ 891 do t as E ← lookup' vars id; 892 match t return λx.? → ? with 893 [ Local ⇒ λE. OK (Σs:stmt.?) s 894  Stack n ⇒ λE. 736 895 do q ← match access_mode ty with 737 896 [ By_value q ⇒ OK ? q … … 739 898  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 740 899 ]; 741 OK ? (St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s) 742  Global _ ⇒ Error ? [MSG ParamGlobalMixup; CTX ? id] 743 ]) (OK ? s) params. 900 OK ? «St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, ?» 901  Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id] 902 ] E) (OK ? s) params. 903 whd % [ whd % [ @I  whd >E @I ]  @sig_ok ] 904 qed. 744 905 745 906 definition bigid1 ≝ an_identifier SymbolTag [[ … … 754 915 false;false;false;true]]. 755 916 917 lemma Exists_rm : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2). 918 #A #P #l1 #x #l2 elim l1 919 [ normalize #H %2 @H 920  #h #t #IH normalize * [ #H %1 @H  #H %2 @IH @H ] 921 qed. 922 923 lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2). 924 #A #P #l1 #x #l2 #H elim l1 925 [ %1 @H 926  #h #t #IH %2 @IH 927 ] qed. 928 929 lemma Exists_map : ∀A,B,P,Q,f,l. 930 Exists A P l → 931 (∀a.P a → Q (f a)) → 932 Exists B Q (map A B f l). 933 #A #B #P #Q #f #l elim l // 934 #h #t #IH * [ #H #F %1 @F @H  #H #F %2 @IH [ @H  @F ] ] qed. 935 936 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)" 937 with precedence 10 938 for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒ 939 λ${ident E}.$s ] (refl ? $t) }. 940 941 lemma local_id_add_local : ∀vars,id,id'. 942 local_id vars id → 943 local_id (add ?? vars id' Local) id. 944 #vars #id #id' #H 945 whd whd in ⊢ match % with [ _ ⇒ ?  _ ⇒ ?] cases (identifier_eq ? id id') 946 [ #E < E >lookup_add_hit // 947  #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/ 948 ] qed. 949 756 950 (* FIXME: the temporary handling is nonsense, I'm afraid. *) 757 951 definition translate_function : list (ident×region) → function → res internal_function ≝ 758 952 λglobals, f. 759 let 〈vartypes , stacksize〉≝ characterise_vars globals f in953 let 〈vartypes0, stacksize〉 as E ≝ characterise_vars globals f in 760 954 let tmp ≝ bigid1 in (* FIXME *) 761 955 let tmpp ≝ bigid2 in (* FIXME *) 956 let vartypes ≝ add … (add … vartypes0 tmp Local) tmpp Local in 762 957 do s ← translate_statement vartypes tmp tmpp (fn_body f); 763 958 do s ← alloc_params vartypes (fn_params f) s; … … 767 962 (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f))) 768 963 stacksize 769 s). 964 s ?). 965 [ whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]) >lookup_add_hit % 966  whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit % % ] 967  @stmt_vars_mp [ 3: @sig_ok  skip ] 968 #i #H cases (identifier_eq ? tmp i) 969 [ #E <E @Exists_mid @refl 970  #NE1 @Exists_rm cases (identifier_eq ? tmpp i) 971 [ #E <E @Exists_mid @refl 972  #NE2 @Exists_rm 973 >map_append 974 @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i) 975 @(local_id_add_miss ?? Local ? NE1) 976 @(local_id_add_miss ?? Local ? NE2) @H 977  skip 978  * #id #ty #E1 <E1 @refl 979 ] 980 ] 981 ] 982 ] qed. 770 983 771 984 definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝ 
Deliverables/D3.3/idlookupbranch/Cminor/initialisation.ma
r961 r1087 22 22 away. *) 23 23 24 definition init_datum : ident → region → init_data → nat (*offset*) → stmt≝24 definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_vars s (λ_.False) ≝ 25 25 λid,r,init,off. 26 26 match init_expr init with … … 31 31 ] 32 32 ]. 33 // 34 cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/ 35 qed. 33 36 34 definition init_var : ident → region → list init_data → stmt ≝ 37 lemma unpair : ∀A,B,C,D,x. ∀P:A → B → C. ∀Q:A → B → D. 38 let 〈a,b〉 ≝ x in 〈P a b, Q a b〉 = 〈P (\fst x) (\snd x), Q (\fst x) (\snd x)〉. 39 #A #B #C #D * // qed. 40 41 lemma sndredex : ∀A,B,C,D,x. ∀R:D → Prop. ∀P:A → C. ∀Q:A → B → D. 42 R (Q (\fst x) (\snd x)) → R (\snd (let 〈a,b〉 ≝ x in 〈P a, Q a b〉)). 43 #A #B #C #D *; normalize /2/ 44 qed. 45 46 lemma sig_stmt_vars : ∀P:ident → Prop. ∀s:Σs:stmt.stmt_vars s P. 47 stmt_vars s P. 48 #P * #s #p whd in ⊢ (?%?) // 49 qed. 50 51 definition init_var : ident → region → list init_data → Σs:stmt. stmt_vars s (λ_.False) ≝ 35 52 λid,r,init. 36 53 \snd (foldr ?? … … 38 55 let 〈off,s〉 ≝ os in 39 56 〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉) 40 〈0, St_skip〉 init). 57 〈0, dp ? (λx.stmt_vars x (λ_.False)) St_skip ?〉 init). 58 [ whd // 59  elim init whd // 60 #h #t #IH whd in ⊢ (?(???%)?) @sndredex whd % [ @sig_stmt_vars  @IH ] 61 ] qed. 41 62 42 definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝ 43 λvars. foldr ?? 44 (λvar,s. St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) St_skip vars. 63 definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_vars s (λ_.False) ≝ 64 λvars. foldr ? (Σs:stmt. stmt_vars s (λ_.False)) 65 (λvar,s. dp ? (λx.stmt_vars x (λ_.False)) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_vars x (λ_.False)) St_skip I) vars. 66 whd % @sig_stmt_vars 67 qed. 45 68 46 definition add_statement : ident → stmt→69 definition add_statement : ident → (Σs:stmt. stmt_vars s (λ_.False)) → 47 70 list (ident × (fundef internal_function)) → 48 71 list (ident × (fundef internal_function)) ≝ 49 λid,s. 72 λid,s. match s with [ dp s H ⇒ 50 73 map ?? 51 74 (λidf. … … 59 82 (f_vars f) 60 83 (f_stacksize f) 61 (St_seq s (f_body f)))〉 84 (St_seq s (f_body f)) 85 ?)〉 62 86  External f ⇒ 〈id, External ? f〉 (* Error ? *) 63 87 ] 64  inr _ ⇒ 〈id',f'〉 ]). 88  inr _ ⇒ 〈id',f'〉 ]) ]. 89 whd % 90 [ @(stmt_vars_mp … H) #i * 91  // 92 ] qed. 65 93 66 94 definition empty_vars : list (ident × (list init_data) × region × unit) → 
Deliverables/D3.3/idlookupbranch/Cminor/syntax.ma
r961 r1087 2 2 include "common/FrontEndOps.ma". 3 3 include "common/CostLabel.ma". 4 include "utilities/lists.ma". 5 include "utilities/option.ma". 6 7 definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝ 8 λtag,A,m,i. lookup … m i ≠ None ?. 4 9 5 10 (* TODO: consider making the typing stricter. *) … … 13 18  Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t 14 19  Ecost : ∀t. costlabel → expr t → expr t. 20 21 (* Assert a predicate on every variable or parameter identifier. *) 22 let rec expr_vars (t:typ) (e:expr t) (P:ident → Prop) on e : Prop ≝ 23 match e with 24 [ Id _ i ⇒ P i 25  Cst _ _ ⇒ True 26  Op1 _ _ _ e ⇒ expr_vars ? e P 27  Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P 28  Mem _ _ _ e ⇒ expr_vars ? e P 29  Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P 30  Ecost _ _ e ⇒ expr_vars ? e P 31 ]. 32 33 lemma expr_vars_mp : ∀t,e,P,Q. 34 (∀i. P i → Q i) → expr_vars t e P → expr_vars t e Q. 35 #t0 #e elim e normalize /3/ 36 [ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2 37 % /3/ 38  #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/ 39 ] qed. 15 40 16 41 inductive stmt : Type[0] ≝ … … 33 58  St_cost : costlabel → stmt → stmt. 34 59 60 (* Assert a predicate on every variable or parameter identifier. *) 61 let rec stmt_vars (s:stmt) (P:ident → Prop) on s : Prop ≝ 62 match s with 63 [ St_skip ⇒ True 64  St_assign _ i e ⇒ P i ∧ expr_vars ? e P 65  St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P 66  St_call oi e es ⇒ match oi with [ None ⇒ True  Some i ⇒ P i ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es 67  St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es 68  St_seq s1 s2 ⇒ stmt_vars s1 P ∧ stmt_vars s2 P 69  St_ifthenelse _ _ e s1 s2 ⇒ expr_vars ? e P ∧ stmt_vars s1 P ∧ stmt_vars s2 P 70  St_loop s ⇒ stmt_vars s P 71  St_block s ⇒ stmt_vars s P 72  St_exit _ ⇒ True 73  St_switch _ _ e _ _ ⇒ expr_vars ? e P 74  St_return oe ⇒ match oe with [ None ⇒ True  Some e ⇒ match e with [ dp _ e ⇒ expr_vars ? e P ] ] 75  St_label _ s ⇒ stmt_vars s P 76  St_goto _ ⇒ True 77  St_cost _ s ⇒ stmt_vars s P 78 ]. 79 80 lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars s P → stmt_vars s Q. 81 #P #Q #H #s elim s normalize 82 [ // 83  #t #id #e * /4/ 84  #t #r #q #e1 #e2 * /4/ 85  * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/  *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ] 86  #e #es * #H1 #H2 % [ /3/  @(All_mp … H2) * /3/ ] 87  #s1 #s2 #H1 #H2 * /3/ 88  #sz #sg #e #s1 #s2 #H1 #H2 * * /5/ 89  8,9: #s #H1 #H2 /2/ 90  // 91  /5/ 92  * normalize [ //  *; normalize /3/ ] 93  /2/ 94  // 95  /2/ 96 ] qed. 97 35 98 record internal_function : Type[0] ≝ 36 99 { f_return : option typ … … 39 102 ; f_stacksize : nat 40 103 ; f_body : stmt 104 ; f_bound : stmt_vars f_body (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) 41 105 }. 42 106 
Deliverables/D3.3/idlookupbranch/Cminor/toRTLabs.ma
r1072 r1087 14 14 〈〈r,ty〉::rs, add ?? en id r, gen'〉) 〈[ ], en, gen〉. 15 15 16 definition populate_label_env : label_env → universe LabelTag → list ident → label_env × (universe LabelTag) ≝ 16 lemma populates_env : ∀l,e,u,l',e',u'. 17 populate_env e u l = 〈l',e',u'〉 → 18 ∀i. Exists ? (λx.\fst x = i) l → 19 present ?? e' i. 20 #l elim l 21 [ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) * 22  * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?); 23 * [ whd in ⊢ (??%? → ?) #E1 <E1 24 generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z 25 whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E 26 whd in E:(??%?); 27 >(?:e' = add ?? y id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *) 28 whd >lookup_add_hit % #A destruct 29  #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl) 30 lapply (refl ? (populate_env e u tl)) 31 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *) 32 * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u'' 33 whd in ⊢ (??%? → ?) #E 34 >(?:e' = add ?? e1 id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *) 35 @lookup_add_oblivious 36 @(IH … E1 ? H) 37 ] 38 ] qed. 39 40 lemma populate_extends : ∀l,e,u,l',e',u'. 41 populate_env e u l = 〈l',e',u'〉 → 42 ∀i. present ?? e i → present ?? e' i. 43 #l elim l 44 [ #e #u #l' #e' #u' #E whd in E:(??%?); destruct // 45  * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?); 46 change in E:(??(match % with [ _ ⇒ ?])?) with (populate_env e u tl) 47 lapply (refl ? (populate_env e u tl)) 48 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) * #l0 #e0 #u0 #E0 49 >E0 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u0) #i1 #u1 #E 50 whd in E:(??%?) 51 >(?:e' = add ?? e0 id i1) [ 2: destruct (E) @refl ] 52 #i #H @lookup_add_oblivious @(IH … E0) @H 53 ] qed. 54 55 definition populate_label_env : label_env → universe LabelTag → list ident → label_env × (universe LabelTag) ≝ 17 56 λen,gen. foldr ?? 18 57 (λid,engen. … … 25 64 #tag #A #m * #i #H @H 26 65 qed. 66 67 definition lookup' : ∀e:env. ∀id. present ?? e id → register ≝ 68 λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r  None ⇒ λH.⊥ ]. 69 cases H #H' cases (H' (refl ??)) qed. 70 27 71 28 72 (* Add a statement to the graph, *without* updating the entry label. *) … … 70 114 axiom UnknownVariable : String. 71 115 72 definition choose_reg : env → ∀ty.expr ty → internal_function → res (register × internal_function)≝116 definition choose_reg : ∀env:env.∀ty.∀e:expr ty. internal_function → expr_vars ty e (present ?? env) → register × internal_function ≝ 73 117 λenv,ty,e,f. 74 match e with 75 [ Id _ i ⇒ 76 do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup … env i); 77 OK ? 〈r, f〉 78  _ ⇒ 79 OK ? (fresh_reg f ty) 118 match e return λty,e. expr_vars ty e (present ?? env) → register × internal_function with 119 [ Id _ i ⇒ λEnv. 〈lookup' env i Env, f〉 120  _ ⇒ λ_.fresh_reg f ty 80 121 ]. 81 82 definition choose_regs : env → list (Σt:typ.expr t) → internal_function → res (list register × internal_function) ≝ 83 λenv,es,f. 84 foldr (Σt:typ.expr t) ? 85 (λe,acc. do 〈rs,f〉 ← acc; 86 do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e f ]; 87 OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es. 122 123 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 ≝ 124 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. 125 126 definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ]. 127 128 definition choose_regs : ∀env:env. ∀es:list (Σt:typ.expr t). internal_function → All ? (exprtyp_present env) es → list register × internal_function ≝ 129 λenv,es,f,Env. 130 foldr_all (Σt:typ.expr t) ?? 131 (λe,p,acc. let 〈rs,f〉 ≝ acc in 132 let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg env t e f ? ] p in 133 〈r::rs,f'〉) 〈[ ], f〉 es Env. 134 @p qed. 88 135 89 136 axiom BadCminorProgram : String. 90 137 91 let rec add_expr (env:env) (ty:typ) (e:expr ty) ( dst:register) (f:internal_function) on e: resinternal_function ≝92 match e with93 [ Id _ i ⇒ 94 do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);138 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 ≝ 139 match e return λty,e.expr_vars ty e (present ?? env) → internal_function with 140 [ Id _ i ⇒ λEnv. 141 let r ≝ lookup' env i Env in 95 142 match register_eq r dst with 96 [ inl _ ⇒ OK ?f97  inr _ ⇒ OK ? (add_fresh_to_graph (St_op1 Oid dst r) f)143 [ inl _ ⇒ f 144  inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f 98 145 ] 99  Cst _ c ⇒ OK ? (add_fresh_to_graph (St_const dst c) f)100  Op1 _ _ op e' ⇒ 101 do 〈r,f〉 ← choose_reg env ? e' f;146  Cst _ c ⇒ λ_. add_fresh_to_graph (St_const dst c) f 147  Op1 _ _ op e' ⇒ λEnv. 148 let 〈r,f〉 ≝ choose_reg env ? e' f Env in 102 149 let f ≝ add_fresh_to_graph (St_op1 op dst r) f in 103 add_expr env ? e' r f104  Op2 _ _ _ op e1 e2 ⇒ 105 do 〈r1,f〉 ← choose_reg env ? e1 f;106 do 〈r2,f〉 ← choose_reg env ? e2 f;150 add_expr env ? e' Env r f 151  Op2 _ _ _ op e1 e2 ⇒ λEnv. 152 let 〈r1,f〉 ≝ choose_reg env ? e1 f (proj1 … Env) in 153 let 〈r2,f〉 ≝ choose_reg env ? e2 f (proj2 … Env) in 107 154 let f ≝ add_fresh_to_graph (St_op2 op dst r1 r2) f in 108 do f ← add_expr env ? e2 r2 f;109 add_expr env ? e1 r1 f110  Mem _ _ q e' ⇒ 111 do 〈r,f〉 ← choose_reg env ? e' f;155 let f ≝ add_expr env ? e2 (proj2 … Env) r2 f in 156 add_expr env ? e1 (proj1 … Env) r1 f 157  Mem _ _ q e' ⇒ λEnv. 158 let 〈r,f〉 ≝ choose_reg env ? e' f Env in 112 159 let f ≝ add_fresh_to_graph (St_load q r dst) f in 113 add_expr env ? e' r f114  Cond _ _ _ e' e1 e2 ⇒ 160 add_expr env ? e' Env r f 161  Cond _ _ _ e' e1 e2 ⇒ λEnv. 115 162 let resume_at ≝ f_entry f in 116 do f ← add_expr env ? e2 dst f;163 let f ≝ add_expr env ? e2 (proj2 … Env) dst f in 117 164 let lfalse ≝ f_entry f in 118 165 let f ≝ add_fresh_to_graph (λ_.St_skip resume_at) f in 119 do f ← add_expr env ? e1 dst f;120 do 〈r,f〉 ← choose_reg env ? e' f;166 let f ≝ add_expr env ? e1 (proj2 … (proj1 … Env)) dst f in 167 let 〈r,f〉 ≝ choose_reg env ? e' f (proj1 … (proj1 … Env)) in 121 168 let f ≝ add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f in 122 add_expr env ? e' r f123  Ecost _ l e' ⇒ 124 do f ← add_expr env ? e' dst f;125 OK ? (add_fresh_to_graph (St_cost l) f)126 ] .169 add_expr env ? e' (proj1 … (proj1 … Env)) r f 170  Ecost _ l e' ⇒ λEnv. 171 let f ≝ add_expr env ? e' Env dst f in 172 add_fresh_to_graph (St_cost l) f 173 ] Env. 127 174 128 175 (* This shouldn't occur; maybe use vectors? *) 129 176 axiom WrongNumberOfArguments : String. 130 177 131 let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) ( dsts:list register) (f:internal_function) on es: res internal_function ≝132 match es with133 [ nil ⇒ match dsts with [ nil ⇒ OK ? f  cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]134  cons e et ⇒ 178 let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es) (dsts:list register) (f:internal_function) on es: res internal_function ≝ 179 match es return λes.All ?? es → ? with 180 [ nil ⇒ λ_. match dsts with [ nil ⇒ OK ? f  cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ] 181  cons e et ⇒ λEnv. 135 182 match dsts with 136 183 [ nil ⇒ Error ? (msg WrongNumberOfArguments) 137 184  cons r rt ⇒ 138 do f ← add_exprs env et rt f;139 match e with [ dp ty e ⇒ add_expr env ty e r f ]185 do f ← add_exprs env et ? rt f; 186 match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ty e ? r f) ] (proj1 ?? Env) 140 187 ] 141 ]. 188 ] Env. 189 whd in Env 190 [ @(proj2 … Env)  @Env ] qed. 142 191 143 192 axiom UnknownLabel : String. 144 193 axiom ReturnMismatch : String. 145 194 146 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) ( exits:list label) (f:internal_function) on s : res internal_function ≝147 match s with148 [ St_skip ⇒ OK ? f149  St_assign _ x e ⇒ 150 do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x);151 add_expr env ? e dst f152  St_store _ _ q e1 e2 ⇒ 153 do 〈val_reg, f〉 ← choose_reg env ? e2 f;154 do 〈addr_reg, f〉 ← choose_reg env ? e1 f;195 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_vars s (present ?? env)) (exits:list label) (f:internal_function) on s : res internal_function ≝ 196 match s return λs.stmt_vars s (present ?? env) → res internal_function with 197 [ St_skip ⇒ λ_. OK ? f 198  St_assign _ x e ⇒ λEnv. 199 let dst ≝ lookup' env x (proj1 … Env) in 200 OK ? (add_expr env ? e (proj2 … Env) dst f) 201  St_store _ _ q e1 e2 ⇒ λEnv. 202 let 〈val_reg, f〉 ≝ choose_reg env ? e2 f (proj2 … Env) in 203 let 〈addr_reg, f〉 ≝ choose_reg env ? e1 f (proj1 … Env) in 155 204 let f ≝ add_fresh_to_graph (St_store q addr_reg val_reg) f in 156 do f ← add_expr env ? e1 addr_reg f;157 add_expr env ? e2 val_reg f158  St_call return_opt_id e args ⇒ 159 do return_opt_reg ←160 match return_opt_id with161 [ None ⇒ OK ? (None ?)162  Some id ⇒ do r ← opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id); OK ? (Some ? r)163 ] ;164 do 〈args_regs, f〉 ← choose_regs env args f;165 do f ←205 let f ≝ add_expr env ? e1 (proj1 … Env) addr_reg f in 206 OK ? (add_expr env ? e2 (proj2 … Env) val_reg f) 207  St_call return_opt_id e args ⇒ λEnv. 208 let return_opt_reg ≝ 209 match return_opt_id return λo. ? → ? with 210 [ None ⇒ λ_. None ? 211  Some id ⇒ λEnv. Some ? (lookup' env id ?) 212 ] Env in 213 let 〈args_regs, f〉 ≝ choose_regs env args f (proj2 … Env) in 214 let f ≝ 166 215 match e with 167 [ Id _ id ⇒ OK ? (add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f)216 [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f 168 217  _ ⇒ 169 do 〈fnr, f〉 ← choose_reg env ? e f;218 let 〈fnr, f〉 ≝ choose_reg env ? e f (proj2 … (proj1 … Env)) in 170 219 let f ≝ add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f in 171 add_expr env ? e fnr f172 ] ;173 add_exprs env args args_regs f174  St_tailcall e args ⇒ 175 do 〈args_regs, f〉 ← choose_regs env args f;176 do f ←220 add_expr env ? e (proj2 … (proj1 … Env)) fnr f 221 ] in 222 add_exprs env args (proj2 … Env) args_regs f 223  St_tailcall e args ⇒ λEnv. 224 let 〈args_regs, f〉 ≝ choose_regs env args f (proj2 … Env) in 225 let f ≝ 177 226 match e with 178 [ Id _ id ⇒ OK ? (add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f)227 [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f 179 228  _ ⇒ 180 do 〈fnr, f〉 ← choose_reg env ? e f;229 let 〈fnr, f〉 ≝ choose_reg env ? e f (proj1 … Env) in 181 230 let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f in 182 add_expr env ? e fnr f183 ] ;184 add_exprs env args args_regs f185  St_seq s1 s2 ⇒ 186 do f ← add_stmt env label_env s2 exits f;187 add_stmt env label_env s1 exits f188  St_ifthenelse _ _ e s1 s2 ⇒ 231 add_expr env ? e (proj1 … Env) fnr f 232 ] in 233 add_exprs env args (proj2 … Env) args_regs f 234  St_seq s1 s2 ⇒ λEnv. 235 do f ← add_stmt env label_env s2 (proj2 … Env) exits f; 236 add_stmt env label_env s1 (proj1 … Env) exits f 237  St_ifthenelse _ _ e s1 s2 ⇒ λEnv. 189 238 let l_next ≝ f_entry f in 190 do f ← add_stmt env label_env s2 exits f;239 do f ← add_stmt env label_env s2 (proj2 … Env) exits f; 191 240 let l2 ≝ f_entry f in 192 241 let f ≝ add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f in 193 do f ← add_stmt env label_env s1 exits f;194 do 〈r,f〉 ← choose_reg env ? e f;242 do f ← add_stmt env label_env s1 (proj2 … (proj1 … Env)) exits f; 243 let 〈r,f〉 ≝ choose_reg env ? e f (proj1 … (proj1 … Env)) in 195 244 let f ≝ add_fresh_to_graph (λl1. St_cond r l1 l2) f in 196 add_expr env ? e r f197  St_loop s ⇒ 245 OK ? (add_expr env ? e (proj1 … (proj1 … Env)) r f) 246  St_loop s ⇒ λEnv. 198 247 let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *) 199 248 let l_loop ≝ f_entry f in 200 do f ← add_stmt env label_env s exits f;249 do f ← add_stmt env label_env s Env exits f; 201 250 OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f) 202  St_block s ⇒ 203 add_stmt env label_env s ((f_entry f)::exits) f204  St_exit n ⇒ 251  St_block s ⇒ λEnv. 252 add_stmt env label_env s Env ((f_entry f)::exits) f 253  St_exit n ⇒ λEnv. 205 254 do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 206 255 OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f) 207  St_switch sz sg e tab n ⇒ 208 do 〈r,f〉 ← choose_reg env ? e f;256  St_switch sz sg e tab n ⇒ λEnv. 257 let 〈r,f〉 ≝ choose_reg env ? e f Env in 209 258 do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 210 259 let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in … … 218 267 let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in 219 268 OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab; 220 add_expr env ? e r f269 OK ? (add_expr env ? e Env r f) 221 270  St_return opt_e ⇒ 222 271 let f ≝ add_fresh_to_graph (λ_. St_return) f in 223 match opt_e with224 [ None ⇒ OK ? f272 match opt_e return λo. ? → ? with 273 [ None ⇒ λEnv. OK ? f 225 274  Some e ⇒ 226 275 match f_result f with 227 [ None ⇒ Error ? (msg ReturnMismatch)228  Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e (\fst r) f]276 [ None ⇒ λEnv. Error ? (msg ReturnMismatch) 277  Some r ⇒ match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ? e ? (\fst r) f) ] 229 278 ] 230 279 ] 231  St_label l s' ⇒ 232 do f ← add_stmt env label_env s' exits f;280  St_label l s' ⇒ λEnv. 281 do f ← add_stmt env label_env s' Env exits f; 233 282 do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l); 234 283 OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f) 235  St_goto l ⇒ 284  St_goto l ⇒ λEnv. 236 285 do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l); 237 286 OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f) 238  St_cost l s' ⇒ 239 do f ← add_stmt env label_env s' exits f;287  St_cost l s' ⇒ λEnv. 288 do f ← add_stmt env label_env s' Env exits f; 240 289 OK ? (add_fresh_to_graph (St_cost l) f) 241 ]. 242 [ @(λ_. St_skip l_next) 290 ] Env. 291 [ whd in Env @(proj1 … (proj1 … Env)) 292  @(λ_. St_skip l_next) 243 293  @(St_skip (f_entry f)) 244 294  @St_skip 245 295  @(λ_. St_skip l) 246 296  @(λ_. St_skip l_default) 297  whd in Env @Env 247 298  @(St_skip (f_entry f)) 248 299  @(λ_.St_skip l') … … 261 312 ]. 262 313 314 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)" 315 with precedence 10 316 for @{ match $t return λx.x = $t → ? with [ pair ${fresh xy} ${ident z} ⇒ 317 match ${fresh xy} return λx. ? = $t → ? with [ pair ${ident x} ${ident y} ⇒ 318 λ${ident E}.$s ] ] (refl ? $t) }. 319 320 263 321 definition c2ra_function (*: internal_function → internal_function*) ≝ 264 322 λf. … … 266 324 let reggen0 ≝ new_universe RegisterTag in 267 325 let cminor_labels ≝ labels_of (f_body f) in 268 let 〈params, env1, reggen1〉 ≝ populate_env (empty_map …) reggen0 (f_params f) in269 let 〈locals0, env, reggen2〉 ≝ populate_env env1 reggen1 (f_vars f) in326 let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in 327 let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in 270 328 let 〈result, locals, reggen〉 ≝ 271 329 match f_return f with … … 287 345 l 288 346 l in 289 do f ← add_stmt env label_env (f_body f) [ ] emptyfn;347 do f ← add_stmt env label_env (f_body f) ? [ ] emptyfn; 290 348 do u1 ← check_universe_ok ? (f_labgen f); 291 349 do u2 ← check_universe_ok ? (f_reggen f); 292 350 OK ? f 293 351 . 294 >lookup_add_hit % #E destruct 352 [ @(stmt_vars_mp … (f_bound f)) 353 #i #H cases (Exists_append … H) 354 [ #H1 @(populate_extends ?????? (sym_eq … E2)) 355 @(populates_env … (sym_eq … E1)) @H1 356  #H1 @(populates_env … (sym_eq … E2)) @H1 357 ] 358  *: >lookup_add_hit % #E destruct 359 ] 295 360 qed. 296 361 
Deliverables/D3.3/idlookupbranch/utilities/lists.ma
r816 r1087 9 9 let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝ 10 10 match l with 11 [ nil ⇒ False11 [ nil ⇒ True 12 12  cons h t ⇒ P h ∧ All A P t 13 13 ]. 14 15 lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l. 16 #A #P #Q #H #l elim l normalize // 17 #h #t #IH * /3/ 18 qed. 14 19 15 20 let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝ … … 18 23  cons h t ⇒ orb (p h) (exists A p t) 19 24 ]. 25 26 let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝ 27 match l with 28 [ nil ⇒ False 29  cons h t ⇒ (P h) ∨ (Exists A P t) 30 ]. 31 32 lemma Exists_append : ∀A,P,l1,l2. 33 Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2. 34 #A #P #l1 elim l1 35 [ normalize /2/ 36  #h #t #IH #l2 * 37 [ #H /3/ 38  #H cases (IH l2 H) /3/ 39 ] 40 ] qed. 41 42 lemma map_append : ∀A,B,f,l1,l2. 43 (map A B f l1) @ (map A B f l2) = map A B f (l1@l2). 44 #A #B #f #l1 elim l1 45 [ #l2 @refl 46  #h #t #IH #l2 normalize // 47 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.