Changeset 311
 Timestamp:
 Nov 26, 2010, 1:28:13 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 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. 
Deliverables/D4.1/Matita/Vector.ma
r272 r311 133 133 nqed. 134 134 135 nlet rec split (A: Type[0]) ( n,m: Nat) on m135 nlet rec split (A: Type[0]) (m,n: Nat) on m 136 136 : Vector A (m+n) → (Vector A m) × (Vector A n) 137 137 ≝ … … 142 142 [ Empty ⇒ λK.⊥ 143 143  Cons o he tl ⇒ λK. 144 match split A n m'(tl⌈Vector A (m'+n)↦Vector A o⌉) with144 match split A m' n (tl⌈Vector A (m'+n)↦Vector A o⌉) with 145 145 [ mk_Cartesian v1 v2 ⇒ 〈he::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))]. 146 146 //; ndestruct; //.
Note: See TracChangeset
for help on using the changeset viewer.