Changeset 1581 for src/ASM/Status.ma
 Timestamp:
 Dec 1, 2011, 3:15:15 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r1541 r1581 1020 1020 qed. 1021 1021 1022 definition set_arg_1: ∀M: Type[0]. PreStatus M → [[ bit_addr ; carry ]] → 1023 Bit → PreStatus M ≝ 1024 λm, s, a, v. 1025 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with 1022 (* XXX: Russell typing: Σs': PreStatus M. clock … s = clock M s', causes dangling de Bruijn 1023 pointer assertion failure in nCicMetaSubst.ml, line 293. *) 1024 definition set_arg_1: ∀M: Type[0]. PreStatus M → [[bit_addr; carry]] → Bit → PreStatus M ≝ 1025 λm: Type[0]. 1026 λs: PreStatus m. 1027 λa: [[bit_addr; carry]]. 1028 λv: Bit. 1029 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with 1026 1030 [ BIT_ADDR b ⇒ λbit_addr: True. 1027 let 〈 nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in1028 1029 let 〈 ignore, three_bits〉 ≝ split ? 1 3 nu in1030 match bit_1with1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1031 let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in 1032 let bit_1 ≝ get_index_v ?? nu 0 ? in 1033 let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in 1034 match bit_1 return λ_. ? with 1035 [ true ⇒ 1036 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1037 let d ≝ address ÷ 8 in 1038 let m ≝ address mod 8 in 1039 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1040 let sfr ≝ get_bit_addressable_sfr ? s ? t true in 1041 let new_sfr ≝ set_index … sfr m v ? in 1042 set_bit_addressable_sfr ? s new_sfr t 1043  false ⇒ 1044 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1045 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1046 let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in 1047 let n_bit ≝ set_index … t (modulus address 8) v ? in 1048 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in 1049 set_low_internal_ram ? s memory 1050 ] 1047 1051  CARRY ⇒ 1048 1052 λcarry: True. 1049 let 〈 nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in1050 1051 1052 1053 1054 1053 let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in 1054 let bit_1 ≝ get_index_v… nu 1 ? in 1055 let bit_2 ≝ get_index_v… nu 2 ? in 1056 let bit_3 ≝ get_index_v… nu 3 ? in 1057 let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in 1058 set_8051_sfr ? s SFR_PSW new_psw 1055 1059  _ ⇒ 1056 1060 λother: False.
Note: See TracChangeset
for help on using the changeset viewer.