Changeset 362
 Timestamp:
 Dec 2, 2010, 11:53:49 AM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r357 r362 24 24 (* ===================================== *) 25 25 26 (* 26 27 ndefinition get_index_bv ≝ 27 28 λn: Nat. … … 29 30 λm: Nat. 30 31 λp: m < n. 31 get_index Bool n b m p.32 get_index_bv Bool n b m p. 32 33 33 34 interpretation "BitVector get_index" 'get_index b n = (get_index ? b n). … … 46 47 λm: Nat. 47 48 drop Bool n b m. 49 *) 48 50 49 51 (* ===================================== *) … … 51 53 (* ===================================== *) 52 54 53 ndefinition zero ≝ 54 λn: Nat. 55 ((replicate Bool n false): BitVector n). 56 57 ndefinition max ≝ 58 λn: Nat. 59 ((replicate Bool n true): BitVector n). 60 55 ndefinition zero: ∀n:Nat. BitVector n ≝ 56 λn: Nat. replicate Bool n false. 57 58 ndefinition max: ∀n:Nat. BitVector n ≝ 59 λn: Nat. replicate Bool n true. 60 61 (* 61 62 ndefinition append ≝ 62 63 λm, n: Nat. … … 64 65 λc: BitVector n. 65 66 append Bool m n b c. 66 67 *) 68 67 69 ndefinition pad ≝ 68 70 λm, n: Nat. … … 75 77 (* ===================================== *) 76 78 79 (* 77 80 ndefinition reverse ≝ 78 81 λn: Nat. … … 84 87 λb: BitVector n. 85 88 length Bool n b. 89 *) 86 90 87 91 (* ===================================== *) … … 126 130 (* ===================================== *) 127 131 132 (* 128 133 ndefinition rotate_left_bv ≝ 129 134 λn, m: Nat. … … 147 152 λc: Bool. 148 153 shift_right Bool n m b c. 149 154 *) 155 150 156 (* ===================================== *) 151 157 (* Conversions to and from lists and natural numbers. *) 152 158 (* ===================================== *) 153 159 160 (* 154 161 ndefinition list_of_bitvector ≝ 155 162 λn: Nat. … … 160 167 λl: List Bool. 161 168 vector_of_list Bool l. 169 *) 162 170 163 171 nlet rec bitvector_of_nat_aux (n: Nat) (bound: Nat) on bound ≝ … … 194 202 let biglist ≝ reverse ? (bitvector_of_nat_aux m m) in 195 203 let size ≝ length ? biglist in 196 let bitvector ≝ bitvector_of_listbiglist in204 let bitvector ≝ vector_of_list ? biglist in 197 205 let difference ≝ n  size in 198 206 less_than_or_equal_b_elim … 
Deliverables/D4.1/Matita/Interpret.ma
r358 r362 19 19 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1) 20 20 (get_arg_8 s false addr2) false in 21 let cy_flag ≝ get_index … flags Z ? in22 let ac_flag ≝ get_index … flags one ? in23 let ov_flag ≝ get_index … flags two ? in21 let cy_flag ≝ get_index_v … flags Z ? in 22 let ac_flag ≝ get_index_v … flags one ? in 23 let ov_flag ≝ get_index_v … flags two ? in 24 24 let s ≝ set_arg_8 s ACC_A result in 25 25 set_flags s cy_flag (Just Bit ac_flag) ov_flag … … 28 28 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1) 29 29 (get_arg_8 s false addr2) old_cy_flag in 30 let cy_flag ≝ get_index … flags Z ? in31 let ac_flag ≝ get_index … flags one ? in32 let ov_flag ≝ get_index … flags two ? in30 let cy_flag ≝ get_index_v … flags Z ? in 31 let ac_flag ≝ get_index_v … flags one ? in 32 let ov_flag ≝ get_index_v … flags two ? in 33 33 let s ≝ set_arg_8 s ACC_A result in 34 34 set_flags s cy_flag (Just Bit ac_flag) ov_flag … … 37 37 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1) 38 38 (get_arg_8 s false addr2) old_cy_flag in 39 let cy_flag ≝ get_index … flags Z ? in40 let ac_flag ≝ get_index … flags one ? in41 let ov_flag ≝ get_index … flags two ? in39 let cy_flag ≝ get_index_v … flags Z ? in 40 let ac_flag ≝ get_index_v … flags one ? in 41 let ov_flag ≝ get_index_v … flags two ? in 42 42 let s ≝ set_arg_8 s ACC_A result in 43 43 set_flags s cy_flag (Just Bit ac_flag) ov_flag … … 142 142 if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then 143 143 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in 144 let cy_flag ≝ get_index ?flags Z ? in144 let cy_flag ≝ get_index_v … flags Z ? in 145 145 let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in 146 146 if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then … … 179 179  RL _ ⇒ (* DPM: always ACC_A *) 180 180 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 181 let new_acc ≝ rotate_left _bv ?one old_acc in181 let new_acc ≝ rotate_left … one old_acc in 182 182 set_8051_sfr s SFR_ACC_A new_acc 183 183  RR _ ⇒ (* DPM: always ACC_A *) 184 184 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 185 let new_acc ≝ rotate_right _bv ?one old_acc in185 let new_acc ≝ rotate_right … one old_acc in 186 186 set_8051_sfr s SFR_ACC_A new_acc 187 187  RLC _ ⇒ (* DPM: always ACC_A *) 188 188 let old_cy_flag ≝ get_cy_flag s in 189 189 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 190 let new_cy_flag ≝ get_index_ bv ?old_acc Z ? in191 let new_acc ≝ shift_left _bveight one old_acc old_cy_flag in190 let new_cy_flag ≝ get_index_v … old_acc Z ? in 191 let new_acc ≝ shift_left … eight one old_acc old_cy_flag in 192 192 let s ≝ set_arg_1 s CARRY new_cy_flag in 193 193 set_8051_sfr s SFR_ACC_A new_acc … … 195 195 let old_cy_flag ≝ get_cy_flag s in 196 196 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 197 let new_cy_flag ≝ get_index_ bv ?old_acc seven ? in198 let new_acc ≝ shift_right _bveight one old_acc old_cy_flag in197 let new_cy_flag ≝ get_index_v … old_acc seven ? in 198 let new_acc ≝ shift_right … eight one old_acc old_cy_flag in 199 199 let s ≝ set_arg_1 s CARRY new_cy_flag in 200 200 set_8051_sfr s SFR_ACC_A new_acc … … 384 384 let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in 385 385 let 〈nu, nl〉 ≝ split ? four four pc_bu in 386 let bit ≝ get_index_ bv ?nl Z ? in386 let bit ≝ get_index_v … nl Z ? in 387 387 let 〈relevant1, relevant2〉 ≝ split ? three eight a in 388 388 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 
Deliverables/D4.1/Matita/Status.ma
r357 r362 191 191 let sfr ≝ special_function_registers_8051 s in 192 192 let index ≝ sfr_8051_index i in 193 get_index ??sfr index ?.194 napply (sfr8051_index_nineteen i).193 get_index_v … sfr index ?. 194 napply sfr8051_index_nineteen. 195 195 nqed. 196 196 … … 200 200 let sfr ≝ special_function_registers_8052 s in 201 201 let index ≝ sfr_8052_index i in 202 get_index ??sfr index ?.203 napply (sfr8052_index_five i).202 get_index_v … sfr index ?. 203 napply sfr8052_index_five. 204 204 nqed. 205 205 … … 383 383 λs: Status. 384 384 let sfr ≝ special_function_registers_8051 s in 385 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in386 get_index Bool eight psw Z ?.385 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 386 get_index_v Bool eight psw Z ?. 387 387 nnormalize. 388 388 napply (less_than_or_equal_monotone ? ?). … … 395 395 λs: Status. 396 396 let sfr ≝ special_function_registers_8051 s in 397 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in398 get_index Bool eight psw (S Z) ?.397 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 398 get_index_v Bool eight psw (S Z) ?. 399 399 nnormalize. 400 400 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 407 407 λs: Status. 408 408 let sfr ≝ special_function_registers_8051 s in 409 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in410 get_index Bool eight psw two ?.409 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 410 get_index_v Bool eight psw two ?. 411 411 nnormalize. 412 412 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 419 419 λs: Status. 420 420 let sfr ≝ special_function_registers_8051 s in 421 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in422 get_index Bool eight psw three ?.421 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 422 get_index_v Bool eight psw three ?. 423 423 nnormalize. 424 424 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 431 431 λs: Status. 432 432 let sfr ≝ special_function_registers_8051 s in 433 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in434 get_index Bool eight psw four ?.433 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 434 get_index_v Bool eight psw four ?. 435 435 nnormalize. 436 436 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 443 443 λs: Status. 444 444 let sfr ≝ special_function_registers_8051 s in 445 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in446 get_index Bool eight psw five ?.445 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 446 get_index_v Bool eight psw five ?. 447 447 nnormalize. 448 448 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 455 455 λs: Status. 456 456 let sfr ≝ special_function_registers_8051 s in 457 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in458 get_index Bool eight psw six ?.457 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 458 get_index_v Bool eight psw six ?. 459 459 nnormalize. 460 460 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 467 467 λs: Status. 468 468 let sfr ≝ special_function_registers_8051 s in 469 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in470 get_index Bool eight psw seven ?.469 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 470 get_index_v Bool eight psw seven ?. 471 471 nnormalize. 472 472 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 482 482 λov: Bit. 483 483 let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in 484 let old_cy ≝ get_index 485 let old_ac ≝ get_index 486 let old_fo ≝ get_index 487 let old_rs1 ≝ get_index 488 let old_rs0 ≝ get_index 489 let old_ov ≝ get_index 490 let old_ud ≝ get_index 491 let old_p ≝ get_index 484 let old_cy ≝ get_index_v… nu Z ? in 485 let old_ac ≝ get_index_v… nu one ? in 486 let old_fo ≝ get_index_v… nu two ? in 487 let old_rs1 ≝ get_index_v… nu three ? in 488 let old_rs0 ≝ get_index_v… nl Z ? in 489 let old_ov ≝ get_index_v… nl one ? in 490 let old_ud ≝ get_index_v… nl two ? in 491 let old_p ≝ get_index_v… nl three ? in 492 492 let new_ac ≝ match ac with [ Nothing ⇒ old_ac  Just j ⇒ j ] in 493 493 let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ; … … 655 655 λs: Status. 656 656 λr: BitVector three. 657 let b ≝ get_index_ bv ?r Z ? in658 let c ≝ get_index_ bv ?r one ? in659 let d ≝ get_index_ bv ?r two ? in657 let b ≝ get_index_v … r Z ? in 658 let c ≝ get_index_v … r one ? in 659 let d ≝ get_index_v … r two ? in 660 660 let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in 661 let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_ bv four un two ?) (get_index_bvfour un three ?) in661 let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_v … four un two ?) (get_index_v … four un three ?) in 662 662 let offset ≝ 663 663 if conjunction (negation r1) (negation r0) then … … 696 696 λs: Status. 697 697 let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in 698 let m ≝ get_index_ bv … nu Z ? in699 let r1 ≝ get_index_ bv … nu one ? in700 let r2 ≝ get_index_ bv … nu two ? in701 let r3 ≝ get_index_ bv … nu three ? in698 let m ≝ get_index_v … nu Z ? in 699 let r1 ≝ get_index_v … nu one ? in 700 let r2 ≝ get_index_v … nu two ? in 701 let r3 ≝ get_index_v … nu three ? in 702 702 let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in 703 703 let memory ≝ … … 719 719 λv: Byte. 720 720 let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in 721 let bit_zero ≝ get_index 722 let bit_one ≝ get_index 723 let bit_two ≝ get_index 724 let bit_three ≝ get_index 721 let bit_zero ≝ get_index_v… nu Z ? in 722 let bit_one ≝ get_index_v… nu one ? in 723 let bit_two ≝ get_index_v… nu two ? in 724 let bit_three ≝ get_index_v… nu three ? in 725 725 if bit_zero then 726 726 let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl) … … 798 798 λdirect: True. 799 799 let 〈 nu, nl 〉 ≝ split … four four d in 800 let bit_one ≝ get_index_ bv … nu one ? in800 let bit_one ≝ get_index_v … nu one ? in 801 801 match bit_one with 802 802 [ true ⇒ … … 810 810 let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in 811 811 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 812 let bit_one ≝ get_index_ bv … bit_one_v Z ? in812 let bit_one ≝ get_index_v … bit_one_v Z ? in 813 813 match bit_one with 814 814 [ true ⇒ … … 837 837 λdirect: True. 838 838 let 〈 nu, nl 〉 ≝ split … four four d in 839 let bit_one ≝ get_index_ bv … nu one ? in839 let bit_one ≝ get_index_v … nu one ? in 840 840 let 〈 ignore, three_bits 〉 ≝ split ? one three nu in 841 841 match bit_one with … … 849 849 let register ≝ get_register s [[ false; false; i ]] in 850 850 let 〈 nu, nl 〉 ≝ split ? four four register in 851 let bit_one ≝ get_index_ bv ?nu one ? in851 let bit_one ≝ get_index_v … nu one ? in 852 852 let 〈 ignore, three_bits 〉 ≝ split ? one three nu in 853 853 match bit_one with … … 909 909 λbit_addr: True. 910 910 let 〈 nu, nl 〉 ≝ split … four four b in 911 let bit_one ≝ get_index_ bv … nu one ? in911 let bit_one ≝ get_index_v … nu one ? in 912 912 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 913 913 match bit_one with … … 918 918 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in 919 919 let sfr ≝ get_bit_addressable_sfr s ? trans l in 920 get_index_ bv ?sfr m ?920 get_index_v … sfr m ? 921 921  false ⇒ 922 922 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 923 923 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in 924 924 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in 925 get_index_ bv ?t (modulus address eight) ?925 get_index_v … t (modulus address eight) ? 926 926 ] 927 927  N_BIT_ADDR n ⇒ 928 928 λn_bit_addr: True. 929 929 let 〈 nu, nl 〉 ≝ split … four four n in 930 let bit_one ≝ get_index_ bv … nu one ? in930 let bit_one ≝ get_index_v … nu one ? in 931 931 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 932 932 match bit_one with … … 937 937 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in 938 938 let sfr ≝ get_bit_addressable_sfr s ? trans l in 939 negation (get_index_ bv ?sfr m ?)939 negation (get_index_v … sfr m ?) 940 940  false ⇒ 941 941 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 942 942 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in 943 943 let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in 944 negation (get_index_ bv ?trans (modulus address eight) ?)944 negation (get_index_v … trans (modulus address eight) ?) 945 945 ] 946 946  CARRY ⇒ λcarry: True. get_cy_flag s … … 963 963 [ BIT_ADDR b ⇒ λbit_addr: True. 964 964 let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in 965 let bit_one ≝ get_index_ bv ?nu one ? in965 let bit_one ≝ get_index_v … nu one ? in 966 966 let 〈 ignore, three_bits 〉 ≝ split ? one three nu in 967 967 match bit_one with … … 985 985 λcarry: True. 986 986 let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in 987 let bit_one ≝ get_index 988 let bit_two ≝ get_index 989 let bit_three ≝ get_index 987 let bit_one ≝ get_index_v… nu one ? in 988 let bit_two ≝ get_index_v… nu two ? in 989 let bit_three ≝ get_index_v… nu three ? in 990 990 let new_psw ≝ [[ v; bit_one ; bit_two; bit_three ]] @@ nl in 991 991 set_8051_sfr s SFR_PSW new_psw 
Deliverables/D4.1/Matita/Vector.ma
r357 r362 30 30 interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl). 31 31 32 notation "hvbox(l break !!! break n)" 33 non associative with precedence 90 34 for @{ 'get_index_v $l $n }. 35 32 36 (* ===================================== *) 33 37 (* Lookup. *) 34 38 (* ===================================== *) 35 39 36 nlet rec get_index (A: Type[0]) (n: Nat)40 nlet rec get_index_v (A: Type[0]) (n: Nat) 37 41 (v: Vector A n) (m: Nat) (lt: m < n) on m: A ≝ 38 42 (match m with … … 45 49 (match v return λx.λ_. S o < x → A with 46 50 [ Empty ⇒ λprf: S o < Z. ? 47  Cons p hd tl ⇒ λprf: S o < S p. get_index A p tl o ?51  Cons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ? 48 52 ]) 49 53 ]) lt. … … 54 58 nqed. 55 59 56 nlet rec get_index_weak (A: Type[0]) (n: Nat)60 nlet rec get_index_weak_v (A: Type[0]) (n: Nat) 57 61 (v: Vector A n) (m: Nat) on m ≝ 58 62 match m with … … 65 69 match v with 66 70 [ Empty ⇒ Nothing A 67  Cons p hd tl ⇒ get_index_weak A p tl o68 ] 69 ]. 70 71 interpretation "Vector get_index" 'get_index v n = (get_index? ? v n).71  Cons p hd tl ⇒ get_index_weak_v A p tl o 72 ] 73 ]. 74 75 interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n). 72 76 73 77 nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝
Note: See TracChangeset
for help on using the changeset viewer.