Changeset 343 for Deliverables/D4.1/Matita/Status.ma
 Timestamp:
 Nov 30, 2010, 4:56:42 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Status.ma
r337 r343 696 696 set_low_internal_ram s new_low_internal_ram. 697 697 698 alias id "get_index" = "cic:/matita/ng/BitVector/get_index.def(3)".699 698 ndefinition read_at_stack_pointer ≝ 700 699 λs: Status. 701 700 let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in 702 let m ≝ get_index … nu Z ? in703 let r1 ≝ get_index … nu one ? in704 let r2 ≝ get_index … nu two ? in705 let r3 ≝ get_index … nu three ? in701 let m ≝ get_index_bv … nu Z ? in 702 let r1 ≝ get_index_bv … nu one ? in 703 let r2 ≝ get_index_bv … nu two ? in 704 let r3 ≝ get_index_bv … nu three ? in 706 705 let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in 707 706 let memory ≝ … … 765 764 ] 766 765 ] (subaddressing_modein … a). 766 767 ncheck get_index_bv. 767 768 768 769 ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ; … … 802 803 λdirect: True. 803 804 let 〈 nu, nl 〉 ≝ split … four four d in 804 let bit_one ≝ get_index … nu one ? in805 let bit_one ≝ get_index_bv … nu one ? in 805 806 match bit_one with 806 807 [ true ⇒ … … 814 815 let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in 815 816 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 816 let bit_one ≝ get_index … bit_one_v Z ? in817 let bit_one ≝ get_index_bv … bit_one_v Z ? in 817 818 match bit_one with 818 819 [ true ⇒ … … 841 842 λdirect: True. 842 843 let 〈 nu, nl 〉 ≝ split … four four d in 843 let bit_one ≝ get_index … nu one ? in844 let bit_one ≝ get_index_bv … nu one ? in 844 845 let 〈 ignore, three_bits 〉 ≝ split ? one three nu in 845 846 match bit_one with … … 853 854 let register ≝ get_register s [[ false; false; i ]] in 854 855 let 〈 nu, nl 〉 ≝ split ? four four register in 855 let bit_one ≝ get_index ? nu one ? in856 let bit_one ≝ get_index_bv ? nu one ? in 856 857 let 〈 ignore, three_bits 〉 ≝ split ? one three nu in 857 858 match bit_one with … … 901 902 λbit_addr: True. 902 903 let 〈 nu, nl 〉 ≝ split … four four b in 903 let bit_one ≝ get_index … nu one ? in904 let bit_one ≝ get_index_bv … nu one ? in 904 905 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 905 906 match bit_one with … … 910 911 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in 911 912 let sfr ≝ get_bit_addressable_sfr s ? trans l in 912 get_index ? sfr m ?913 get_index_bv ? sfr m ? 913 914  false ⇒ 914 915 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 915 916 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in 916 917 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in 917 get_index ? t (modulus address eight) ?918 get_index_bv ? t (modulus address eight) ? 918 919 ] 919 920  N_BIT_ADDR n ⇒ 920 921 λn_bit_addr: True. 921 922 let 〈 nu, nl 〉 ≝ split … four four n in 922 let bit_one ≝ get_index … nu one ? in923 let bit_one ≝ get_index_bv … nu one ? in 923 924 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 924 925 match bit_one with … … 929 930 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in 930 931 let sfr ≝ get_bit_addressable_sfr s ? trans l in 931 negation (get_index ? sfr m ?)932 negation (get_index_bv ? sfr m ?) 932 933  false ⇒ 933 934 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 934 935 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in 935 936 let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in 936 negation (get_index ? trans (modulus address eight) ?)937 negation (get_index_bv ? trans (modulus address eight) ?) 937 938 ] 938 939  CARRY ⇒ λcarry: True. get_cy_flag s … … 955 956 [ BIT_ADDR b ⇒ λbit_addr: True. 956 957 let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in 957 let bit_one ≝ get_index ? nu one ? in958 let bit_one ≝ get_index_bv ? nu one ? in 958 959 let 〈 ignore, three_bits 〉 ≝ split ? one three nu in 959 960 match bit_one with
Note: See TracChangeset
for help on using the changeset viewer.