git.iko.soy/Idris-dev
on master help sign in
More docstrings
10ef56bDavid Raymond Christiansen
libs/base/Data/Buffer.idr+1−1
compare with master
unifiedsplit
@@ -23,7 +23,7 @@ module Data.Buffer
23-- and offset rather than storing the offset in Buffer itself, which
23-- and offset rather than storing the offset in Buffer itself, which
24-- would require exposing the offset argument of prim__appendBuffer
24-- would require exposing the offset argument of prim__appendBuffer
25
25
26−-- A contiguous chunk of n bytes
26+||| A contiguous chunk of n bytes
27abstract
27abstract
28record Buffer : Nat -> Type where
28record Buffer : Nat -> Type where
29 MkBuffer : ( offset : Nat ) -> ( realBuffer : prim__UnsafeBuffer ) -> Buffer n
29 MkBuffer : ( offset : Nat ) -> ( realBuffer : prim__UnsafeBuffer ) -> Buffer n
libs/base/Data/HVect.idr+4
@@ -6,10 +6,12 @@ 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 data HVect : Vect k Type -> Type where
10 data HVect : Vect k Type -> Type where
10 Nil : HVect []
11 Nil : HVect []
11 (::) : t -> HVect ts -> HVect (t::ts)
12 (::) : t -> HVect ts -> HVect (t::ts)
12
13
14+ ||| Extract an element from an HVect
13 index : (i : Fin k) -> HVect ts -> index i ts
15 index : (i : Fin k) -> HVect ts -> index i ts
14 index fZ (x::xs) = x
16 index fZ (x::xs) = x
15 index (fS j) (x::xs) = index j xs
17 index (fS j) (x::xs) = index j xs
@@ -49,6 +51,8 @@ using (k : Nat, ts : Vect k Type)
49 instance (Shows k ts) => Show (HVect ts) where
51 instance (Shows k ts) => Show (HVect ts) where
50 show xs = show (shows xs)
52 show xs = show (shows xs)
51
53
54+ ||| Extract an arbitrary element of the correct type
55+ ||| @ t the goal type
52 get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
56 get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
53 get {p = Here} (x::xs) = x
57 get {p = Here} (x::xs) = x
54 get {p = There p'} (x::xs) = get {p = p'} xs
58 get {p = There p'} (x::xs) = get {p = p'} xs
libs/base/Data/Sign.idr+2
@@ -1,6 +1,8 @@
1module Data.Sign
1module Data.Sign
2
2
3+||| A representation of signs for signed datatypes such as `ZZ`
3data Sign = Plus | Minus
4data Sign = Plus | Minus
4
5
6+||| Discover the sign of some type
5class Signed t where
7class Signed t where
6 total sign : t -> Sign
8 total sign : t -> Sign
libs/base/Data/Vect.idr+4−1
@@ -10,11 +10,14 @@ import Language.Reflection
10--------------------------------------------------------------------------------
10--------------------------------------------------------------------------------
11
11
12using (xs : Vect k a)
12using (xs : Vect k a)
13+ ||| A proof that some element is found in a vector
13 data Elem : a -> Vect k a -> Type where
14 data Elem : a -> Vect k a -> Type where
14 Here : Elem x (x::xs)
15 Here : Elem x (x::xs)
15 There : Elem x xs -> Elem x (y::xs)
16 There : Elem x xs -> Elem x (y::xs)
16
17
18+||| A tactic for discovering where, if anywhere, an element is in a vector
19+||| @ n how many elements to search before giving up
17−findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic
20+findElem : (n : Nat) -> List (TTName, Binder TT) -> TT -> Tactic
18findElem Z ctxt goal = Refine "Here" `Seq` Solve
21findElem Z ctxt goal = Refine "Here" `Seq` Solve
19findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))
22findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))
20
23