Changeset 949 for src/ASM/Status.ma
 Timestamp:
 Jun 13, 2011, 6:42:14 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r935 r949 420 420 let sfr ≝ special_function_registers_8051 ? s in 421 421 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 422 get_index_v bool 8 psw (S O)?.422 get_index_v bool 8 psw 1 ?. 423 423 normalize 424 424 repeat (@ (le_S_S ? ?)) … … 826 826 λdirect: True. 827 827 let 〈 nu, nl 〉 ≝ split … 4 4 d in 828 let bit_ 1 ≝ get_index_v … nu 1? in829 match bit_1 with830 [ true ⇒831 let 〈 bit_one, three_bits 〉 ≝ split ? 1 3 nu in828 let bit_one ≝ get_index_v ? ? nu 0 ? in 829 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in 830 match bit_one with 831 [ false ⇒ 832 832 let address ≝ three_bits @@ nl in 833 833 lookup ? 7 address (low_internal_ram ? s) (zero 8) 834  false ⇒ get_bit_addressable_sfr ? s 8 d l834  true ⇒ get_bit_addressable_sfr ? s 8 d l 835 835 ] 836 836  INDIRECT i ⇒ … … 839 839 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 840 840 let bit_1 ≝ get_index_v … bit_one_v O ? in 841 match bit_1 with842 [ true ⇒841 match bit_1 with 842 [ false ⇒ 843 843 lookup ? 7 (three_bits @@ nl) (low_internal_ram ? s) (zero 8) 844  false ⇒844  true ⇒ 845 845 lookup ? 7 (three_bits @@ nl) (high_internal_ram ? s) (zero 8) 846 846 ] … … 865 865 λdirect: True. 866 866 let 〈 nu, nl 〉 ≝ split … 4 4 d in 867 let bit_ 1 ≝ get_index_v … nu 1? in867 let bit_one ≝ get_index_v ? ? nu 0 ? in 868 868 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in 869 match bit_ 1with869 match bit_one with 870 870 [ true ⇒ set_bit_addressable_sfr ? s d v 871 871  false ⇒ … … 877 877 let register ≝ get_register ? s [[ false; false; i ]] in 878 878 let 〈nu, nl〉 ≝ split ? 4 4 register in 879 let bit_1 ≝ get_index_v … nu 1? in879 let bit_1 ≝ get_index_v … nu 0 ? in 880 880 let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in 881 881 match bit_1 with 882 [ true ⇒882 [ false ⇒ 883 883 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ? s) in 884 884 set_low_internal_ram ? s memory 885  false ⇒885  true ⇒ 886 886 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ? s) in 887 887 set_high_internal_ram ? s memory … … 972 972 λbit_addr: True. 973 973 let 〈 nu, nl 〉 ≝ split … 4 4 b in 974 let bit_1 ≝ get_index_v … nu 1? in974 let bit_1 ≝ get_index_v … nu 0 ? in 975 975 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 976 976 match bit_1 with … … 991 991 λn_bit_addr: True. 992 992 let 〈 nu, nl 〉 ≝ split … 4 4 n in 993 let bit_1 ≝ get_index_v … nu 1? in993 let bit_1 ≝ get_index_v … nu 0 ? in 994 994 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 995 995 match bit_1 with … … 1026 1026 [ BIT_ADDR b ⇒ λbit_addr: True. 1027 1027 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in 1028 let bit_1 ≝ get_index_v … nu 1? in1028 let bit_1 ≝ get_index_v … nu 0 ? in 1029 1029 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in 1030 1030 match bit_1 with
Note: See TracChangeset
for help on using the changeset viewer.