Changeset 311 for Deliverables/D4.1/Matita/Status.ma
 Timestamp:
 Nov 26, 2010, 1:28:13 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Status.ma
r310 r311 710 710 acc_pc ; ext_indirect ; 711 711 ext_indirect_dptr ]] x) → ? with 712 [ ACC_A ⇒ λ K: True. get_8051_sfr s SFR_ACC_A713  ACC_B ⇒ λ K: True. get_8051_sfr s SFR_ACC_B714  DATA d ⇒ λ K: True. d715  REGISTER r1 r2 r3 ⇒ λ K: True. get_register s r1 r2 r3712 [ ACC_A ⇒ λacc_a: True. get_8051_sfr s SFR_ACC_A 713  ACC_B ⇒ λacc_b: True. get_8051_sfr s SFR_ACC_B 714  DATA d ⇒ λdata: True. d 715  REGISTER r1 r2 r3 ⇒ λregister: True. get_register s r1 r2 r3 716 716  EXT_INDIRECT_DPTR ⇒ 717 λ K: True.717 λext_indirect_dptr: True. 718 718 let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 719 719 lookup … sixteen address (external_ram s) (zero eight) 720 720  EXT_INDIRECT e ⇒ 721 λ K: True.721 λext_indirect: True. 722 722 let address ≝ get_register s false false e in 723 723 let padded_address ≝ pad eight eight address in 724 lookup … sixteen padded_address (external_ram s) 724 lookup … sixteen padded_address (external_ram s) (zero eight) 725 725  ACC_DPTR ⇒ 726 λ K: True.726 λacc_dptr: True. 727 727 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 728 728 let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in … … 730 730 lookup … sixteen address (external_ram s) (zero eight) 731 731  ACC_PC ⇒ 732 λ K: True.732 λacc_pc: True. 733 733 let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in 734 734 let 〈 address, carry 〉 ≝ half_add sixteen (program_counter s) padded_acc in 735 735 lookup … sixteen address (external_ram s) (zero eight) 736 736  DIRECT d ⇒ 737 λK: True. 738 ? 737 λdirect: True. 738 let 〈 nu, nl 〉 ≝ split … four four d in 739 let bit_one ≝ get_index … nu one ? in 740 match bit_one with 741 [ true ⇒ 742 let 〈 bit_one, three_bits 〉 ≝ split ? one three nu in 743 let address ≝ three_bits @@ nl in 744 lookup ? seven address (low_internal_ram s) (zero eight) 745  false ⇒ get_bit_addressable_sfr s eight d l 746 ] 739 747  INDIRECT i ⇒ 740 λK: True. ? 741  _ ⇒ λK. ? 748 λindirect: True. 749 let 〈 nu, nl 〉 ≝ split ? four four (get_register s false false i) in 750 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 751 let bit_one ≝ get_index … bit_one_v Z ? in 752 match bit_one with 753 [ true ⇒ 754 lookup ? seven (three_bits @@ nl) (low_internal_ram s) (zero eight) 755  false ⇒ 756 lookup ? seven (three_bits @@ nl) (high_internal_ram s) (zero eight) 757 ] 758  _ ⇒ λother. 759 match other in False with [ ] 742 760 ] (subaddressing_modein … a). 743 nauto; 744 nqed. 761 ##[##1,2: 762 nnormalize; 763 nrepeat (napply less_than_or_equal_monotone); 764 napply less_than_or_equal_zero; 765 ##] 766 nqed. 767 nqed.
Note: See TracChangeset
for help on using the changeset viewer.