Changeset 1063
 Timestamp:
 Jul 11, 2011, 5:52:11 PM (9 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r1062 r1063 14 14 with precedence 10 15 15 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. 16 17 definition ltb ≝ 18 λm, n: nat. 19 leb (S m) n. 20 21 definition geb ≝ 22 λm, n: nat. 23 ltb n m. 24 25 definition gtb ≝ 26 λm, n: nat. 27 leb n m. 28 29 (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *) 30 let rec eq_nat (n: nat) (m: nat) on n: bool ≝ 31 match n with 32 [ O ⇒ match m with [ O ⇒ true  _ ⇒ false ] 33  S n' ⇒ match m with [ S m' ⇒ eq_nat n' m'  _ ⇒ false ] 34 ]. 35 36 let rec remove_n_first_internal 37 (i: nat) (A: Type[0]) (l: list A) (n: nat) 38 on l ≝ 39 match l with 40 [ nil ⇒ [ ] 41  cons hd tl ⇒ 42 match eq_nat i n with 43 [ true ⇒ l 44  _ ⇒ remove_n_first_internal (S i) A tl n 45 ] 46 ]. 47 48 definition remove_n_first ≝ 49 λA: Type[0]. 50 λn: nat. 51 λl: list A. 52 remove_n_first_internal 0 A l n. 53 54 let rec foldi_from_until_internal 55 (A: Type[0]) (i: nat) (res: ?) (rem: list A) (m: nat) (f: nat → list A → A → list A) 56 on rem ≝ 57 match rem with 58 [ nil ⇒ res 59  cons e tl ⇒ 60 match geb i m with 61 [ true ⇒ res 62  _ ⇒ foldi_from_until_internal A (S i) (f i res e) tl m f 63 ] 64 ]. 65 66 definition foldi_from_until ≝ 67 λA: Type[0]. 68 λn: nat. 69 λm: nat. 70 λf: ?. 71 λa: ?. 72 λl: ?. 73 foldi_from_until_internal A 0 a (remove_n_first A n l) m f. 74 75 definition foldi_from ≝ 76 λA: Type[0]. 77 λn. 78 λf. 79 λa. 80 λl. 81 foldi_from_until A n (l) f a l. 82 83 definition foldi_until ≝ 84 λA: Type[0]. 85 λm. 86 λf. 87 λa. 88 λl. 89 foldi_from_until A 0 m f a l. 90 91 definition foldi ≝ 92 λA: Type[0]. 93 λf. 94 λa. 95 λl. 96 foldi_from_until A 0 (l) f a l. 16 97 17 98 definition hd ≝ … … 129 210 *) 130 211 131 include "ASM/FoldStuff.ma".132 133 212 let rec reduce_strong 134 (A: Type[0]) (left: list A) (right: list A) (prf:  left  =  right ) on left 135 : Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  ≝ 136 match left return λx. x = right → Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  with 137 [ nil ⇒ 138 match right return λy.  [ ]  =  y  → Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  with 139 [ nil ⇒ λnil_nil_prf. ? 140  cons hd tl ⇒ λnil_cons_absrd_prf. ? 141 ] 213 (A: Type[0]) (left: list A) (right: list A) 214 on left : Σret: ((list A) × (list A)) × ((list A) × (list A)). \fst (\fst ret) = \fst (\snd ret) ≝ 215 match left with 216 [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉 142 217  cons hd tl ⇒ 143 match right return λy.  hd::tl  =  y  → Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  with 144 [ nil ⇒ λcons_nil_absrd_prf. ? 145  cons hd' tl' ⇒ λcons_cons_prf. 146 let 〈commonl, commonr〉 ≝ eject … (reduce_strong A tl tl' ?) in ? (* 147 [ dp clr their_proof ⇒ ? (* 148 let 〈commonl, commonr〉 ≝ clr in ? *) 149 ]*) 150 ] 151 ] prf. 152 [ 5: normalize in cons_cons_prf; 153 destruct(cons_cons_prf) 154 assumption 155  2: normalize in nil_cons_absrd_prf; 156 destruct(nil_cons_absrd_prf) 157  3: normalize in cons_nil_absrd_prf; 158 destruct(cons_nil_absrd_prf) 159  4: 218 match right with 219 [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉 220  cons hd' tl' ⇒ 221 let 〈cleft, cright〉 ≝ reduce_strong A tl tl' in 222 let 〈commonl, restl〉 ≝ cleft in 223 let 〈commonr, restr〉 ≝ cright in 224 〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉 225 ] 226 ]. 227 [ 1: normalize % 228  2: normalize % 229  3: normalize 230 generalize in match (sig2 … (reduce_strong A tl tl1)); 231 >p2 >p3 >p4 normalize in ⊢ (% → ?) 232 #HYP // 160 233 ] 161 234 qed. 162 163 axiom reduce_length:164 ∀A: Type[0].165 ∀left, right: list A.166 ∀prf:  left  =  right .167 \fst (\fst (reduce A left right)) = \fst (\snd (reduce A left right)).168 235 169 236 let rec map2_opt … … 527 594 ] 528 595 ]. 529 530 definition ltb ≝531 λm, n: nat.532 leb (S m) n.533 534 definition geb ≝535 λm, n: nat.536 ltb n m.537 538 definition gtb ≝539 λm, n: nat.540 leb n m.541 542 (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)543 let rec eq_nat (n: nat) (m: nat) on n: bool ≝544 match n with545 [ O ⇒ match m with [ O ⇒ true  _ ⇒ false ]546  S n' ⇒ match m with [ S m' ⇒ eq_nat n' m'  _ ⇒ false ]547 ].548 596 549 597 (* dpm: conflicts with library definitions 
src/ASM/Vector.ma
r998 r1063 81 81 get_index_v A (S (n + m)) b n ?. 82 82 normalize 83 // 83 @le_S_S 84 cases m // 84 85 qed. 85 86 … … 179 180 ] (? : S ? = S ?). 180 181 // 181 [ destruct 182  lapply (injective_S … K) 183 // 184 ] 182 lapply (injective_S … K) 183 // 185 184 qed. 186 185 … … 404 403 ] 405 404 ]. 406 / /405 /2/ 407 406 qed. 408 407 
src/RTLabs/RTLAbstoRTL.ma
r1062 r1063 73 73 ]. 74 74 75 axiom fresh_regs_length: 76 ∀def: rtl_internal_function. 77 ∀n: nat. 78 (\snd (fresh_regs def n)) = n. 79 75 80 definition addr_regs ≝ 76 81 λregs. … … 487 492 λsrcrs1. 488 493 λsrcrs2. 494 λprf: srcrs1 = srcrs2. 489 495 λstart_lbl. 490 496 λdest_lbl. 491 497 λdef. 492 λprf: srcrs1 = srcrs2.493 498 match reduce_strong ? srcrs1 srcrs2 with 494 499 [ dp reduced first_reduced_proof ⇒ … … 586 591 λdestrs: list register. 587 592 λtmp_destrs: list register. 593 λdestrs_prf: destrs = tmp_destrs. 588 594 λsrcrs1: list register. 589 595 λdummy_lbl: label. 590 596 λi: nat. 591 λtranslates. 592 λsrcr2i. 593 let 〈tmp_destrs1, tmp_destrs2〉 ≝ ? in ?. 594 595 let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates 596 srcr2i = 597 let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in 598 translates @ 599 (match tmp_destrs2 with 600  [] > [] 601  tmp_destr2 :: tmp_destrs2 > 602 [adds_graph [RTL.St_clear_carry dummy_lbl ; 603 RTL.St_int (tmp_destr2, 0, dummy_lbl)] ; 604 translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ; 605 translate_cst (AST.Cst_int 0) tmp_destrs1 ; 606 adds_graph [RTL.St_clear_carry dummy_lbl] ; 607 translate_op I8051.Addc destrs destrs tmp_destrs]) 597 λi_prf. 598 λtranslates: list ?. 599 λsrcr2i: register. 600 let 〈tmp_destrs1, tmp_destrs2〉 ≝ split ? tmp_destrs i i_prf in 601 let tmp_destrs2' ≝ 602 match tmp_destrs2 with 603 [ nil ⇒ [ ] 604  cons tmp_destr2 tmp_destrs2 ⇒ [ 605 adds_graph [ 606 rtl_st_clear_carry dummy_lbl; 607 rtl_st_int tmp_destr2 (zero ?) dummy_lbl 608 ]; 609 translate_mul1 dummy tmpr tmp_destrs2 srcrs1 srcr2i; 610 translate_cst (Ointconst I8 (zero ?)) tmp_destrs1; 611 adds_graph [ 612 rtl_st_clear_carry dummy_lbl 613 ]; 614 translate_op Addc destrs destrs tmp_destrs destrs_prf 615 ] 616 ] 617 in 618 translates @ tmp_destrs2'. 619 620 definition translate_mul ≝ 621 λdestrs: list register. 622 λsrcrs1: list register. 623 λsrcrs2: list register. 624 λstart_lbl: label. 625 λdest_lbl: label. 626 λdef: rtl_internal_function. 627 let 〈def, dummy〉 ≝ fresh_reg def in 628 let 〈def, tmpr〉 ≝ fresh_reg def in 629 let 〈def, tmp_destrs〉 ≝ fresh_regs def (destrs) in 630 let 〈def, fresh_srcrs1〉 ≝ fresh_regs def (srcrs1) in 631 let 〈def, fresh_srcrs2〉 ≝ fresh_regs def (srcrs2) in 632 let insts_init ≝ [ 633 translate_move fresh_srcrs1 srcrs1; 634 translate_move fresh_srcrs2 srcrs2; 635 translate_cst (Ointconst I8 (zero ?)) destrs 636 ] 637 in 638 let f ≝ λi. translate_muli dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in 639 let insts_mul ≝ foldi ? ? [ ] srcrs2 in ?. [5: check insts_init. 640 add_translates (insts_init @ insts_mul) start_lbl dest_lbl def. 641 642 let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def = 643 let (def, dummy) = fresh_reg def in 644 let (def, tmpr) = fresh_reg def in 645 let (def, tmp_destrs) = fresh_regs def (List.length destrs) in 646 let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in 647 let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in 648 let insts_init = 649 [translate_move fresh_srcrs1 srcrs1 ; 650 translate_move fresh_srcrs2 srcrs2 ; 651 translate_cst (AST.Cst_int 0) destrs] in 652 let f = λi. translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl i ? in 653 let insts_mul = MiscPottier.foldi f [] srcrs2 in 654 add_translates (insts_init @ insts_mul) start_lbl dest_lbl def 608 655 609 656 definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.