Changeset 2468 for src/Clight/toCminor.ma
- Timestamp:
- Nov 15, 2012, 6:12:57 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/toCminor.ma
r2465 r2468 268 268 (* same gig for AST typs *) 269 269 definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2). 270 * [ #sz1 #sg1 | | #sz1 ] 271 * [ 1,5,9: | *: #a #b try #c try #d @(Error ? (msg TypeMismatch)) ] 272 [ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ] 273 *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) 274 | #P #p @(OK ? p) 275 | *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) 276 ] qed. 270 * [ #sz1 #sg1 | ] 271 * try /2 by Error/ 272 qed. 277 273 278 274 alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)". … … 309 305 match t' return λt'. res (CMunop t t') with 310 306 [ ASTint sz sg ⇒ typ_should_eq ?? (λt.CMunop t (ASTint ??)) (Onegint sz sg) 311 | ASTfloat sz ⇒ typ_should_eq ?? (λt.CMunop t (ASTfloat sz)) (Onegf sz)307 (* | ASTfloat sz ⇒ typ_should_eq ?? (λt.CMunop t (ASTfloat sz)) (Onegf sz) *) 312 308 | _ ⇒ Error ? (msg TypeMismatch) 313 309 ] … … 334 330 match classify_add ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with 335 331 [ add_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oadd ??) e1 e2) 336 | add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2)332 (*| add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2) *) 337 333 (* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *) 338 334 | add_case_pi n ty sz sg ⇒ … … 350 346 match classify_sub ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with 351 347 [ sub_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osub ??) e1 e2) 352 | sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2)348 (* | sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2) *) 353 349 (* XXX could optimise cast as above *) 354 350 | sub_case_pi n ty sz sg ⇒ … … 369 365 match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with 370 366 [ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omul …) e1 e2) 371 | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omulf …) e1 e2)367 (* | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omulf …) e1 e2) *) 372 368 | aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) 373 369 ]. … … 383 379 | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odiv …) e1 e2) 384 380 ] 385 | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivf …) e1 e2)381 (* | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivf …) e1 e2) *) 386 382 | aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) 387 383 ]. … … 434 430 | cmp_case_pp n ty ⇒ 435 431 λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpp … c) (fix_ptr_type … e1) (fix_ptr_type … e2)) 436 | cmp_case_ff sz ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpf … c) e1 e2)432 (* | cmp_case_ff sz ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpf … c) e1 e2) *) 437 433 | cmp_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) 438 434 ]. … … 473 469 P t1 v1 → 474 470 P t2 v2. 475 * [ * * | | *]476 * try * try *471 * [ #sz #sg | ] 472 * [ 1,3: * * ] 477 473 #P #v1 #v2 #E whd in E:(??%?); destruct 478 #H @H479 474 qed. 480 475 … … 501 496 [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4 -E3 change with (typ_should_eq ???? = OK ??) in E4; 502 497 @(typ_equals … E4) % // 503 | #sz #E1 #E2 #E3 destruct >E3 #E4504 @(typ_equals … E4) % // 498 (* | #sz #E1 #E2 #E3 destruct >E3 #E4 499 @(typ_equals … E4) % // *) 505 500 | #n #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4 506 501 @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ] … … 509 504 | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct 510 505 ] 506 511 507 | inversion (classify_sub ty1 ty2) in ⊢ ?; 512 508 [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4 513 509 @(typ_equals … E4) % // 514 | #sz #E1 #E2 #E3 destruct >E3 #E4515 @(typ_equals … E4) % // 510 (* | #sz #E1 #E2 #E3 destruct >E3 #E4 511 @(typ_equals … E4) % // *) 516 512 | #n #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4 517 513 @(typ_equals … E4) % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ] 518 514 | #n1 #n2 #ty1' #ty2' #E1 #E2 #E3 destruct >E3 519 515 whd in ⊢ (??%? → ?); cases ty in e ⊢ %; 520 [ 2: #sz #sg #e #E4 | 4: #ty #e #E4 | 5: #ty' #n' #e #E4516 [ 2: #sz #sg #e #E4 | 3: #ty #e #E4 | 4: #ty' #n' #e #E4 521 517 | *: normalize #X1 #X2 try #X3 try #X4 destruct 522 518 ] whd in E4:(??%?); destruct % // % … … 526 522 | 3,4,5,6,7,8,9,10: inversion (classify_aop ty1 ty2) in ⊢ ?; 527 523 (* Note that some cases require a split on signedness of integer type. *) 528 [ 1, 4,7,10,13,16,19,22: #sz * #E1 #E2 #E3 destruct >E3 #E4524 [ 1,3,5,7,9,11,13,15: #sz * #E1 #E2 #E3 destruct >E3 #E4 529 525 @(typ_equals … E4) % // 530 | 2,5: #sz #E1 #E2 #E3 destruct >E3 #E4 531 @(typ_equals … E4) % // 532 | 8,11,14,17,20,23: #sz #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct 533 | 3,6,9,12,15,18,21,24: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct 526 | 2,4,6,8,10,12,14,16,18: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct 534 527 ] 535 | 11,12,13,14,15,16: inversion (classify_cmp ty1 ty2) in ⊢ ?; 536 [ 1,5,9,13,17,21: #sz * #E1 #E2 #E3 destruct >E3 537 | 2,6,10,14,18,22: #n #ty' #E1 #E2 #E3 destruct >E3 538 | 3,7,11,15,19,23: #sz #E1 #E2 #E3 destruct >E3 528 | *: inversion (classify_cmp ty1 ty2) in ⊢ ?; 529 [ 1,4,7,10,13,16: #sz * #E1 #E2 #E3 destruct >E3 530 | 2,5,8,11,14,17: #n #ty' #E1 #E2 #E3 destruct >E3 539 531 | *: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); @⊥ destruct 540 ] whd in ⊢ (??%? → ?); cases ty in e ⊢ %; 532 ] whd in ⊢ (??%? → ?); cases ty in e ⊢ %; normalize nodelta 541 533 try (normalize #X1 #X2 try #X3 try #X4 try #X5 destruct #FAIL) 542 534 #sz #sg #e #E4 543 whd in E4:(??%?); destruct % 544 [ 25,27,29,31,33,35: @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1) 545 | 26,28,30,32,34,36: @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2) 546 | *: // 547 ] 548 ] qed. 549 535 whd in E4:(??%?); destruct % try @H1 try @H2 536 try @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1) 537 try @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2) 538 ] qed. 550 539 551 540 (* We'll need to implement proper translation of pointers if we really do memory … … 576 565 match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with 577 566 [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint ? sg1 sz2 ?) e) 578 | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e)567 (* | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e)*) 579 568 | Tpointer _ ⇒ OK ? (Op1 ?? (Optrofint ??) e) 580 569 | Tarray _ _ ⇒ OK ? (Op1 ?? (Optrofint ??) e) 581 570 | _ ⇒ Error ? (msg TypeMismatch) 582 571 ] 583 | Tfloat sz1 ⇒ λe.572 (* | Tfloat sz1 ⇒ λe. 584 573 match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with 585 574 [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat ? sz2 | _ ⇒ Ointoffloat ? sz2 ]) e, ?» 586 575 | Tfloat sz2 ⇒ Error ? (msg FIXME) (* OK ? «Op1 ?? (Oid ?) e, ?» (* FIXME *) *) 587 576 | _ ⇒ Error ? (msg TypeMismatch) 588 ] 577 ] *) 589 578 | Tpointer _ ⇒ λe. (* will need changed for memory regions *) 590 579 match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with … … 626 615 | _ ⇒ Error ? (msg TypeMismatch) 627 616 ] 628 | Econst_float f ⇒617 (* | Econst_float f ⇒ 629 618 match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with 630 619 [ Tfloat sz ⇒ OK ? «Cst ? (Ofloatconst sz f), ?» 631 620 | _ ⇒ Error ? (msg TypeMismatch) 632 ] 621 ] *) 633 622 | Evar id ⇒ 634 623 do 〈c,t〉 as E ← lookup' vars id; (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *) … … 676 665 ] 677 666 | _ ⇒ λ_. Error ? (msg TypeMismatch) 678 ] e1' 667 ] e1' 679 668 | Eaddrof e1 ⇒ 680 669 do e1' ← translate_addr vars e1; … … 716 705 [ Tint sz sg ⇒ 717 706 do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2'; 718 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ?with707 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → (res (Σe:CMexpr x. expr_vars ? e (local_id vars))) with 719 708 [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz sg (zero ?))), ?» 720 709 | _ ⇒ λ_.Error ? (msg TypeMismatch) 721 710 ] e1' 722 711 | _ ⇒ Error ? (msg TypeMismatch) 723 ] 712 ] 724 713 | Eorbool e1 e2 ⇒ 725 714 do e1' ← translate_expr vars e1; … … 728 717 [ Tint sz sg ⇒ 729 718 do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2'; 730 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with 719 match typ_of_type (typeof e1) 720 return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with 731 721 [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz sg (repr ? 1))) e2', ?» 732 | _ ⇒ λ_. Error ? (msg TypeMismatch)722 | _ ⇒ λ_. Error ? (msg TypeMismatch) 733 723 ] e1' 734 724 | _ ⇒ Error ? (msg TypeMismatch) 735 ] 725 ] 736 726 | Esizeof ty1 ⇒ 737 727 match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with 738 728 [ Tint sz sg ⇒ OK ? «Cst ? (Ointconst sz sg (repr ? (sizeof ty1))), ?» 739 729 | _ ⇒ Error ? (msg TypeMismatch) 740 ] 730 ] 741 731 | Efield e1 id ⇒ 742 732 match typeof e1 with … … 764 754 ] 765 755 | _ ⇒ Error ? (msg BadlyTypedAccess) 766 ] 756 ] 767 757 | Ecost l e1 ⇒ 768 758 do e1' ← translate_expr vars e1; 769 759 do e' ← OK ? «Ecost ? l e1',?»; 770 typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e' 760 typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e' 771 761 ] 772 762 ]
Note: See TracChangeset
for help on using the changeset viewer.