Changeset 314 for Deliverables
 Timestamp:
 Nov 26, 2010, 4:53:56 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r313 r314 44 44 λp: m < n. 45 45 λc: Bool. 46 set_index _weakBool n b m c.46 set_index Bool n b m c. 47 47 48 48 ndefinition drop ≝ 
Deliverables/D4.1/Matita/Status.ma
r313 r314 3 3 (* ===================================== *) 4 4 5 (* include "ASM.ma". *) 5 include "ASM.ma". 6 6 include "Arithmetic.ma". 7 7 include "BitVectorTrie.ma". … … 691 691 ##] 692 692 nqed. 693 694 include "ASM.ma".695 693 696 694 ndefinition set_arg_16: Status → Word → [[ dptr ]] → Status ≝ … … 783 781 nqed. 784 782 785 (*786 ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →787 Bool → Bool ≝788 λs, a, l.789 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;790 n_bit_addr ;791 carry ]] x) → ? with792 [ BIT_ADDR b ⇒793 λbit_addr: True.794 let 〈 nu, nl 〉 ≝ split … four four b in795 let bit_one ≝ get_index … nu one ? in796 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in797 match bit_one with798 [ true ⇒799 let address ≝ nat_of_bitvector … (three_bits @@ nl) in800 let d ≝ address ÷ eight in801 let m ≝ address mod eight in802 let trans ≝ bitvector_of_nat ((d * eight) + one_hundred_and_twenty_eight) eight in803 let sfr ≝ get_bit_addressable_sfr s ? trans l in804 get_index ? sfr m ?805  false ⇒806 let address ≝ nat_of_bitvector … (three_bits @@ nl) in807 let address' ≝ bitvector_of_nat ((address ÷ eight) + thirty_two) seven in808 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in809 get_index ? t (modulus address eight) ?810 ]811  N_BIT_ADDR n ⇒812 λn_bit_addr: True.813 let 〈 nu, nl 〉 ≝ split … four four n in814 let bit_one ≝ get_index … nu one ? in815 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in816 match bit_one with817 [ true ⇒818 let address ≝ nat_of_bitvector … (three_bits @@ nl) in819 let d ≝ address ÷ eight in820 let m ≝ address mod eight in821 let trans ≝ bitvector_of_nat ((d * eight) + one_hundred_and_twenty_eight) eight in822 let sfr ≝ get_bit_addressable_sfr s ? trans l in823 negation (get_index ? sfr m ?)824  false ⇒825 let address ≝ nat_of_bitvector … (three_bits @@ nl) in826 let address' ≝ bitvector_of_nat ((address ÷ eight) + thirty_two) seven in827 let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in828 negation (get_index ? trans (modulus address eight) ?)829 ]830  CARRY ⇒ λcarry: True. get_cy_flag s831  _ ⇒ λother.832 match other in False with [ ]833 ] (subaddressing_modein … a). *)834 835 783 ndefinition set_arg_8: Status → [[ direct ; indirect ; register ; 836 784 acc_a ; acc_b ; ext_indirect ; … … 852 800 ] 853 801  INDIRECT i ⇒ 854 λindirect: True. ? 802 λindirect: True. 803 let register ≝ get_register s false false i in 804 let 〈 nu, nl 〉 ≝ split ? four four register in 805 let bit_one ≝ get_index ? nu one ? in 806 let 〈 ignore, three_bits 〉 ≝ split ? one three nu in 807 match bit_one with 808 [ true ⇒ 809 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in 810 set_low_internal_ram s memory 811  false ⇒ 812 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in 813 set_high_internal_ram s memory 814 ] 855 815  REGISTER r1 r2 r3 ⇒ λregister: True. set_register s r1 r2 r3 v 856 816  ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v … … 871 831 match other in False with [ ] 872 832 ] (subaddressing_modein … a). 833 ##[##1,2: 834 nnormalize; 835 nrepeat (napply less_than_or_equal_monotone); 836 napply less_than_or_equal_zero 837 ##] 838 nqed. 839 840 naxiom modulus_less_than: 841 ∀m,n: Nat. 842 (m mod n) < n. 843 844 ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] → 845 Bool → Bool ≝ 846 λs, a, l. 847 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; 848 n_bit_addr ; 849 carry ]] x) → ? with 850 [ BIT_ADDR b ⇒ 851 λbit_addr: True. 852 let 〈 nu, nl 〉 ≝ split … four four b in 853 let bit_one ≝ get_index … nu one ? in 854 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 855 match bit_one with 856 [ true ⇒ 857 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 858 let d ≝ address ÷ eight in 859 let m ≝ address mod eight in 860 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in 861 let sfr ≝ get_bit_addressable_sfr s ? trans l in 862 get_index ? sfr m ? 863  false ⇒ 864 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 865 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in 866 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in 867 get_index ? t (modulus address eight) ? 868 ] 869  N_BIT_ADDR n ⇒ 870 λn_bit_addr: True. 871 let 〈 nu, nl 〉 ≝ split … four four n in 872 let bit_one ≝ get_index … nu one ? in 873 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 874 match bit_one with 875 [ true ⇒ 876 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 877 let d ≝ address ÷ eight in 878 let m ≝ address mod eight in 879 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in 880 let sfr ≝ get_bit_addressable_sfr s ? trans l in 881 negation (get_index ? sfr m ?) 882  false ⇒ 883 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 884 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in 885 let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in 886 negation (get_index ? trans (modulus address eight) ?) 887 ] 888  CARRY ⇒ λcarry: True. get_cy_flag s 889  _ ⇒ λother. 890 match other in False with [ ] 891 ] (subaddressing_modein … a). 892 ##[##3,6: 893 nnormalize; 894 nrepeat (napply less_than_or_equal_monotone); 895 napply less_than_or_equal_zero; 896 ####1,2,4,5: 897 napply modulus_less_than; 898 ##] 899 nqed. 900 901 ndefinition set_arg_1: Status → [[ bit_addr ; carry ]] → 902 Bit → Status ≝ 903 λs, a, v. 904 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with 905 [ BIT_ADDR b ⇒ λbit_addr: True. 906 let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in 907 let bit_one ≝ get_index ? nu one ? in 908 let 〈 ignore, three_bits 〉 ≝ split ? one three nu in 909 match bit_one with 910 [ true ⇒ 911 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 912 let d ≝ address ÷ eight in 913 let m ≝ address mod eight in 914 let t ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in 915 let sfr ≝ get_bit_addressable_sfr s ? t true in 916 let new_sfr ≝ set_index … sfr m v ? in 917 set_bit_addressable_sfr s new_sfr t 918  false ⇒ 919 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 920 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in 921 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in 922 let n_bit ≝ set_index … t (modulus address eight) v ? in 923 let memory ≝ insert ? seven address' n_bit (low_internal_ram s) in 924 set_low_internal_ram s memory 925 ] 926  CARRY ⇒ 927 λcarry: True. 928 let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in 929 let bit_one ≝ get_index … nu one ? in 930 let bit_two ≝ get_index … nu two ? in 931 let bit_three ≝ get_index … nu three ? in 932 let new_psw ≝ [[ v; bit_one ; bit_two; bit_three ]] @@ nl in 933 set_8051_sfr s SFR_PSW new_psw 934  _ ⇒ 935 λother: False. 936 match other in False with 937 [ ] 938 ] (subaddressing_modein … a). 939 ##[##1,2,3,6: 940 nnormalize; 941 nrepeat (napply less_than_or_equal_monotone); 942 napply less_than_or_equal_zero; 943 ####4,5: 944 napply (modulus_less_than address eight); 945 ##] 946 nqed.
Note: See TracChangeset
for help on using the changeset viewer.