Changeset 724
- Timestamp:
- Mar 30, 2011, 2:03:05 PM (10 years ago)
- Location:
- src/ASM
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Arithmetic.ma
r712 r724 114 114 λb: BitVector n. 115 115 \fst (sub_with_borrows n b (zero n) true). 116 116 117 let rec bitvector_of_nat_aux (n,m:nat) (v:BitVector n) on m : BitVector n ≝ 118 match m with 119 [ O ⇒ v 120 | S m' ⇒ bitvector_of_nat_aux n m' (increment n v) 121 ]. 122 123 definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝ 124 λn,m. bitvector_of_nat_aux n m (zero n). 125 126 let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝ 127 match v with 128 [ VEmpty ⇒ m 129 | VCons n' hd tl ⇒ nat_of_bitvector_aux n' (if hd then 2*m +1 else 2*m) tl 130 ]. 131 132 definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝ 133 λn,v. nat_of_bitvector_aux n O v. 134 117 135 definition two_complement_negation ≝ 118 136 λn: nat. -
src/ASM/BitVector.ma
r700 r724 93 93 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 94 94 95 let rec bitvector_of_nat_aux (n: nat) (bound: nat) on bound ≝96 match bound with97 [ O ⇒ [ ] (* IT WILL NOT HAPPEN *)98 | S bound' ⇒99 let divrem ≝ divide_with_remainder n (S (S O)) in100 let div ≝ fst nat nat divrem in101 let rem ≝ snd nat nat divrem in102 match div with103 [ O ⇒104 match rem with105 [ O ⇒ [ ]106 | S r ⇒ true :: (bitvector_of_nat_aux O bound')107 ]108 | S d ⇒109 match rem with110 [ O ⇒ false :: (bitvector_of_nat_aux (S d) bound')111 | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound')112 ]113 ]114 ].115 116 95 definition eq_bv ≝ 117 96 λn: nat. … … 130 109 #Q * *; normalize /3/ 131 110 qed. 132 133 let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝134 let biglist ≝ rev ? (bitvector_of_nat_aux m m) in135 let size ≝ length ? biglist in136 let bitvector ≝ vector_of_list ? biglist in137 let difference ≝ n - size in138 less_than_or_equal_b_elim …139 (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector (difference+size) ↦ BitVector n⌉))140 (λH:¬(size ≤ n). maximum n).141 < plus_minus_m_m142 //143 assumption144 qed.145 146 let rec nat_of_bitvector (n: nat) (b: BitVector n) on b: nat ≝147 match b with148 [ VEmpty ⇒ O149 | VCons o hd tl ⇒150 let hdval ≝ match hd with [ true ⇒ S O | false ⇒ O ] in151 plus ((2^o) * hdval) (nat_of_bitvector o tl)152 ].153 111 154 112 axiom bitvector_of_string: -
src/ASM/I8051.ma
r698 r724 4 4 include "ASM/String.ma". 5 5 include "ASM/ASM.ma". 6 include "ASM/Arithmetic.ma". 6 7 include "utilities/Compare.ma". 7 8
Note: See TracChangeset
for help on using the changeset viewer.