Changeset 236 for Deliverables
 Timestamp:
 Nov 12, 2010, 4:01:48 PM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r235 r236 1 (* ===================================== *) 2 (* BitVector.ma: Fixed length bitvectors, and common operations on them. *) 3 (* ===================================== *) 4 1 5 include "Vector.ma". 2 6 include "List.ma". 3 7 include "Nat.ma". 4 8 include "Bool.ma". 9 10 (* ===================================== *) 11 (* Common synonyms. *) 12 (* ===================================== *) 5 13 6 14 ndefinition BitVector ≝ λn: Nat. Vector Bool n. … … 11 19 ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))). 12 20 21 (* ===================================== *) 22 (* Creating bitvectors from scratch. *) 23 (* ===================================== *) 24 25 (* @name: zero 26 @desc: Produces a bitvector containing <tt>n</tt> copies of <tt>False</tt>. 27 *) 13 28 ndefinition zero ≝ 14 29 λn: Nat. 15 30 replicate Bool n False. 16 31 32 ndefinition max ≝ 33 λn: Nat. 34 replicate Bool n True. 35 36 ndefinition append ≝ append. 37 38 (* ===================================== *) 39 (* Logical operations. *) 40 (* ===================================== *) 41 42 (* 43 @name: conjunction 44 @desc: The logical conjunction of two bitvectors of length <tt>n</tt>. 45 *) 17 46 ndefinition conjunction ≝ 18 47 λn: Nat. … … 20 49 λc: BitVector n. 21 50 zip Bool Bool Bool n conjunction b c. 22 51 52 (* 53 @name: inclusive_disjunction 54 @desc: The logical inclusive disjunction of two bitvectors of length 55 <tt>n</tt>. 56 *) 23 57 ndefinition inclusive_disjunction ≝ 24 58 λn: Nat. … … 27 61 zip Bool Bool Bool n inclusive_disjunction b c. 28 62 63 (* 64 @name: exclusive_disjunction 65 @desc: The logical exclusive disjunction of two bitvectors of length 66 <tt>n</tt>. (XOR). 67 *) 29 68 ndefinition exclusive_disjunction ≝ 30 69 λn: Nat. … … 33 72 zip Bool Bool Bool n exclusive_disjunction b c. 34 73 74 (* 75 @name: complement 76 @desc: The logical complement of a bitvector of length <tt>n</tt>. 77 *) 35 78 ndefinition complement ≝ 36 79 λn: Nat. 37 80 λb: BitVector n. 38 81 map Bool Bool n (negation) b. 82 83 (* ===================================== *) 84 (* Conversions to and from lists and natural numbers. *) 85 (* ===================================== *) 39 86 40 87 ndefinition divide_with_remainder ≝ 41 88 λm, n: Nat. 42 89 mk_Cartesian Nat Nat (m ÷ n) (modulus m n). 90 91 (* @name: pad 92 @desc: Pads the front of a bitvector of length <tt>n</tt> with <tt>m</tt> 93 copies of <tt>False</tt>. 94 *) 95 ndefinition pad ≝ 96 λm, n: Nat. 97 λb: BitVector n. 98 let padding ≝ replicate Bool m False in 99 append Bool m n padding b. 43 100 44 101 nlet rec bitvector_of_nat_aux (n: Nat) on n ≝ … … 58 115 ] 59 116 ]. 117 118 (* @name: bitvector_of_nat 119 @desc: Constructs a bitvector whose integer value is the same as <tt>m</tt>. 120 Size of the resulting bitvector is clamped to <tt>n</tt>. 121 *) 122 ndefinition bitvector_of_nat ≝ 123 λm, n: Nat. 124 let biglist ≝ reverse Bool (bitvector_of_nat_aux m) in 125 let size ≝ length Bool biglist in 126 let bvector ≝ bitvector_of_list Bool biglist in 127 let difference ≝ n  size in 128 pad difference size bvector. 129 130 ndefinition list_of_bitvector ≝ list_of_vector. 131 ndefinition bitvector_of_list ≝ vector_of_list. 
Deliverables/D4.1/Matita/Cartesian.ma
r228 r236 6 6 second: B 7 7 }. 8 9 notation "(l,r)" 10 non associative with precedence 90 11 for @{ 'cartesian $l $r }. 12 13 interpretation "Cartesian product" 'cartesian l r = (mk_Cartesian ? ? l r). 
Deliverables/D4.1/Matita/List.ma
r233 r236 83 83  Cons hd tl ⇒ f hd :: map A B f tl 84 84 ]. 85 86 nlet rec zip_safe (A: Type[0]) (B: Type[0]) 87 (l: List A) (m: List B) (p: length A l = length B m) ≝ True. 85 88 86 89 (* ===================================== *) 
Deliverables/D4.1/Matita/Nat.ma
r234 r236 3 3 (* ===================================== *) 4 4 include "Cartesian.ma". 5 include "Maybe.ma".6 5 include "Bool.ma". 7 6 
Deliverables/D4.1/Matita/Vector.ma
r234 r236 159 159 (* ===================================== *) 160 160 161 nlet rec to_list(A: Type[0]) (n: Nat)162 (v: Vector A n) on v ≝163 match v with161 nlet rec list_of_vector (A: Type[0]) (n: Nat) 162 (v: Vector A n) on v ≝ 163 match v return λn.λv. List A with 164 164 [ Empty ⇒ cic:/matita/Cerco/List/List.con(0,1,1) A 165  Cons o hd tl ⇒ hd :: (to_listA o tl)165  Cons o hd tl ⇒ cic:/matita/Cerco/List/List.con(0,2,1) A hd (list_of_vector A o tl) 166 166 ]. 167 167 168 168 (* 169 nlet rec from_list (A: Type[0]) (l: List A) on l ≝169 nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝ 170 170 match l return λl. Vector A (length A l) with 171 171 [ Empty ⇒ cic:/matita/Cerco/Vector/Vector.con(0,1,1) A
Note: See TracChangeset
for help on using the changeset viewer.