 Timestamp:
 Apr 27, 2011, 5:25:26 PM (10 years ago)
 Location:
 src/ASM
 Files:

 1 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/I8051.ma
r757 r777 6 6 include "ASM/Arithmetic.ma". 7 7 include "utilities/Compare.ma". 8 9 definition int_size ≝ bitvector_of_nat 8 1. 10 definition ptr_size ≝ bitvector_of_nat 8 2. 11 definition alignment ≝ None. 8 12 9 13 (* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps … … 125 129 ]. 126 130 127 definition eq_ register: Register → Register → bool ≝131 definition eq_Register: Register → Register → bool ≝ 128 132 λr, s: Register. 129 133 let r_as_nat ≝ nat_of_register r in … … 178 182 [ RegisterSST; RegisterST0; RegisterST1; 179 183 RegisterSPL; RegisterSPH ]. 184 185 definition parameters: list Register ≝ 186 [ Register30; Register31; Register32; Register33; 187 Register34; Register35; Register36; Register37 ]. 180 188 181 189 record RegisterMap: Type[0] ≝ 
src/ASM/Util.ma
r764 r777 2 2 include "basics/types.ma". 3 3 include "arithmetics/nat.ma". 4 5 let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝ 6 match n with 7 [ O ⇒ 8 match l with 9 [ nil ⇒ [ ] 10  cons hd tl ⇒ l 11 ] 12  S n ⇒ 13 match l with 14 [ nil ⇒ [ ] 15  cons hd tl ⇒ 16 hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n 17 ] 18 ]. 19 20 definition nub_by ≝ 21 λA: Type[0]. 22 λf: A → A → bool. 23 λl: list A. 24 nub_by_internal A f l (length ? l). 25 26 let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝ 27 match l with 28 [ nil ⇒ false 29  cons hd tl ⇒ orb (eq a hd) (member A eq a tl) 30 ]. 31 32 let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝ 33 match n with 34 [ O ⇒ [ ] 35  S n ⇒ 36 match l with 37 [ nil ⇒ [ ] 38  cons hd tl ⇒ hd :: take A n tl 39 ] 40 ]. 41 42 let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝ 43 match n with 44 [ O ⇒ l 45  S n ⇒ 46 match l with 47 [ nil ⇒ [ ] 48  cons hd tl ⇒ drop A n tl 49 ] 50 ]. 51 52 definition list_split ≝ 53 λA: Type[0]. 54 λn: nat. 55 λl: list A. 56 〈take A n l, drop A n l〉. 57 58 let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: nat) (f: nat → A → B) 59 (l: list A) on l: list B ≝ 60 match l with 61 [ nil ⇒ nil ? 62  cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl) 63 ]. 64 65 definition mapi ≝ 66 λA, B: Type[0]. 67 λf: nat → A → B. 68 λl: list A. 69 mapi_internal A B 0 f l. 70 71 let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝ 72 match l with 73 [ nil ⇒ Some ? (nil (A × B)) 74  cons hd tl ⇒ 75 match r with 76 [ nil ⇒ None ? 77  cons hd' tl' ⇒ 78 match zip ? ? tl tl' with 79 [ None ⇒ None ? 80  Some tail ⇒ Some ? (〈hd, hd'〉 :: tail) 81 ] 82 ] 83 ]. 4 84 5 85 let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝
Note: See TracChangeset
for help on using the changeset viewer.