Changeset 317 for Deliverables/D4.1/Matita/Status.ma
 Timestamp:
 Nov 26, 2010, 5:45:04 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Status.ma
r316 r317 611 611 ndefinition bit_address_of_register ≝ 612 612 λs: Status. 613 λb, c, d: Bit. 613 λr: BitVector three. 614 let b ≝ get_index ? r Z ? in 615 let c ≝ get_index ? r one ? in 616 let d ≝ get_index ? r two ? in 614 617 let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in 615 618 let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_index four un three ?) in … … 625 628 in 626 629 bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])). 627 nnormalize.628 nrepeat (napply less_than_or_equal_monotone).629 napply less_than_or_equal_zero.630 nrepeat (napply less_than_or_equal_monotone).631 napply less_than_or_equal_zero.630 ##[##1,2,3,4,5: 631 nnormalize; 632 nrepeat (napply less_than_or_equal_monotone); 633 napply less_than_or_equal_zero; 634 ##] 632 635 nqed. 633 636 634 637 ndefinition get_register ≝ 635 638 λs: Status. 636 λ b, c, d: Bit.637 let address ≝ bit_address_of_register s b c din639 λr: BitVector three. 640 let address ≝ bit_address_of_register s r in 638 641 lookup … address (low_internal_ram s) (zero eight). 639 642 640 643 ndefinition set_register ≝ 641 644 λs: Status. 642 λ b, c, d: Bit.645 λr: BitVector three. 643 646 λv: Byte. 644 let address ≝ bit_address_of_register s b c din647 let address ≝ bit_address_of_register s r in 645 648 let old_low_internal_ram ≝ low_internal_ram s in 646 649 let new_low_internal_ram ≝ insert … address v old_low_internal_ram in … … 735 738  EXT_INDIRECT e ⇒ 736 739 λext_indirect: True. 737 let address ≝ get_register s false false ein740 let address ≝ get_register s [[ false; false; e ]] in 738 741 let padded_address ≝ pad eight eight address in 739 742 lookup … sixteen padded_address (external_ram s) (zero eight) … … 762 765  INDIRECT i ⇒ 763 766 λindirect: True. 764 let 〈 nu, nl 〉 ≝ split ? four four (get_register s false false i) in767 let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in 765 768 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 766 769 let bit_one ≝ get_index … bit_one_v Z ? in … … 801 804  INDIRECT i ⇒ 802 805 λindirect: True. 803 let register ≝ get_register s false false iin806 let register ≝ get_register s [[ false; false; i ]] in 804 807 let 〈 nu, nl 〉 ≝ split ? four four register in 805 808 let bit_one ≝ get_index ? nu one ? in … … 813 816 set_high_internal_ram s memory 814 817 ] 815  REGISTER r 1 r2 r3 ⇒ λregister: True. set_register s r1 r2 r3v818  REGISTER r ⇒ λregister: True. set_register s r v 816 819  ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v 817 820  ACC_B ⇒ λacc_b: True. set_8051_sfr s SFR_ACC_B v 818 821  EXT_INDIRECT e ⇒ 819 822 λext_indirect: True. 820 let address ≝ get_register s false false ein823 let address ≝ get_register s [[ false; false; e ]] in 821 824 let padded_address ≝ pad eight eight address in 822 825 let memory ≝ insert ? sixteen padded_address v (external_ram s) in
Note: See TracChangeset
for help on using the changeset viewer.