git.iko.soy/Idris-dev
on master help sign in
Minor docstring additions
757adceDavid Raymond Christiansen
libs/base/Data/BoundedList.idr+4
compare with master
unifiedsplit
@@ -3,10 +3,12 @@ module Data.BoundedList
3%access public
3%access public
4%default total
4%default total
5
5
6+||| A list with an upper bound on its length.
6data BoundedList : Type -> Nat -> Type where
7data BoundedList : Type -> Nat -> Type where
7 Nil : BoundedList a n
8 Nil : BoundedList a n
8 (::) : a -> BoundedList a n -> BoundedList a (S n)
9 (::) : a -> BoundedList a n -> BoundedList a (S n)
9
10
11+||| Compute the length of a list.
10length : BoundedList a n -> Fin (S n)
12length : BoundedList a n -> Fin (S n)
11length [] = fZ
13length [] = fZ
12length (x :: xs) = fS (length xs)
14length (x :: xs) = fS (length xs)
@@ -24,6 +26,7 @@ index (fS f) (_ :: xs) = index f xs
24-- Adjusting bounds
26-- Adjusting bounds
25--------------------------------------------------------------------------------
27--------------------------------------------------------------------------------
26
28
29+||| Loosen the bounds on a list's length.
27weaken : BoundedList a n -> BoundedList a (n + m)
30weaken : BoundedList a n -> BoundedList a (n + m)
28weaken [] = []
31weaken [] = []
29weaken (x :: xs) = x :: weaken xs
32weaken (x :: xs) = x :: weaken xs
@@ -77,6 +80,7 @@ map f (x :: xs) = f x :: map f xs
77-- Misc
80-- Misc
78--------------------------------------------------------------------------------
81--------------------------------------------------------------------------------
79
82
83+||| Extend a bounded list to the maximum size by padding on the left.
80pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n
84pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n
81pad {n=Z} [] _ = []
85pad {n=Z} [] _ = []
82pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)
86pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)
libs/base/Data/HVect.idr+6−2
@@ -6,7 +6,8 @@ import Data.Vect
6%default total
6%default total
7
7
8using (k : Nat, ts : Vect k Type)
8using (k : Nat, ts : Vect k Type)
9− ||| Heterogeneous vectors where the type index gives, element-wise, the types of the contents
9+ ||| Heterogeneous vectors where the type index gives, element-wise,
10+ ||| the types of the contents.
10 data HVect : Vect k Type -> Type where
11 data HVect : Vect k Type -> Type where
11 Nil : HVect []
12 Nil : HVect []
12 (::) : t -> HVect ts -> HVect (t::ts)
13 (::) : t -> HVect ts -> HVect (t::ts)
@@ -30,6 +31,7 @@ using (k : Nat, ts : Vect k Type)
30 updateAt fZ f (x::xs) = f x :: xs
31 updateAt fZ f (x::xs) = f x :: xs
31 updateAt (fS j) f (x::xs) = x :: updateAt j f xs
32 updateAt (fS j) f (x::xs) = x :: updateAt j f xs
32
33
34+ ||| Append two `HVect`s.
33 (++) : {us : Vect l Type} -> HVect ts -> HVect us -> HVect (ts ++ us)
35 (++) : {us : Vect l Type} -> HVect ts -> HVect us -> HVect (ts ++ us)
34 (++) [] ys = ys
36 (++) [] ys = ys
35 (++) (x::xs) ys = x :: (xs ++ ys)
37 (++) (x::xs) ys = x :: (xs ++ ys)
@@ -52,16 +54,18 @@ using (k : Nat, ts : Vect k Type)
52 instance (Shows k ts) => Show (HVect ts) where
54 instance (Shows k ts) => Show (HVect ts) where
53 show xs = show (shows xs)
55 show xs = show (shows xs)
54
56
55− ||| Extract an arbitrary element of the correct type
57+ ||| Extract an arbitrary element of the correct type.
56 ||| @ t the goal type
58 ||| @ t the goal type
57 get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
59 get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
58 get {p = Here} (x::xs) = x
60 get {p = Here} (x::xs) = x
59 get {p = There p'} (x::xs) = get {p = p'} xs
61 get {p = There p'} (x::xs) = get {p = p'} xs
60
62
63+ ||| Replace an element with the correct type.
61 put : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> t -> HVect ts -> HVect ts
64 put : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> t -> HVect ts -> HVect ts
62 put {p = Here} y (x::xs) = y :: xs
65 put {p = Here} y (x::xs) = y :: xs
63 put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
66 put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
64
67
68+ ||| Replace an element with the correct type.
65 update : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
69 update : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
66 update {p = Here} f (x::xs) = f x :: xs
70 update {p = Here} f (x::xs) = f x :: xs
67 update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
71 update {p = There p'} f (x::xs) = x :: update {p = p'} f xs