git.iko.soy/Idris-dev
on master help sign in
More docstrings
commit10ef56b8c1629347ab213e97bfff551ee27e11d0 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 19 Mar 2014, 00:16 (13 years ago) parentf73d721
4 files changed+11−2
compare with master
unifiedsplit
libs/base/Data/Buffer.idr+1−1 libs/base/Data/HVect.idr+4 libs/base/Data/Sign.idr+2 libs/base/Data/Vect.idr+4−1
libs/base/Data/Buffer.idr+1−1
@@ -23,7 +23,7 @@ module Data.Buffer
2323-- and offset rather than storing the offset in Buffer itself, which
2424-- would require exposing the offset argument of prim__appendBuffer
2525
26−-- A contiguous chunk of n bytes
26+||| A contiguous chunk of n bytes
2727abstract
2828record Buffer : Nat -> Type where
2929 MkBuffer : ( offset : Nat ) -> ( realBuffer : prim__UnsafeBuffer ) -> Buffer n
libs/base/Data/HVect.idr+4
@@ -6,10 +6,12 @@ import Data.Vect
66%default total
77
88using (k : Nat, ts : Vect k Type)
9+ ||| Heterogeneous vectors where the type index gives, element-wise, the types of the contents
910 data HVect : Vect k Type -> Type where
1011 Nil : HVect []
1112 (::) : t -> HVect ts -> HVect (t::ts)
1213
14+ ||| Extract an element from an HVect
1315 index : (i : Fin k) -> HVect ts -> index i ts
1416 index fZ (x::xs) = x
1517 index (fS j) (x::xs) = index j xs
@@ -49,6 +51,8 @@ using (k : Nat, ts : Vect k Type)
4951 instance (Shows k ts) => Show (HVect ts) where
5052 show xs = show (shows xs)
5153
54+ ||| Extract an arbitrary element of the correct type
55+ ||| @ t the goal type
5256 get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
5357 get {p = Here} (x::xs) = x
5458 get {p = There p'} (x::xs) = get {p = p'} xs
libs/base/Data/Sign.idr+2
@@ -1,6 +1,8 @@
11module Data.Sign
22
3+||| A representation of signs for signed datatypes such as `ZZ`
34data Sign = Plus | Minus
45
6+||| Discover the sign of some type
57class Signed t where
68 total sign : t -> Sign
libs/base/Data/Vect.idr+4−1
@@ -10,11 +10,14 @@ import Language.Reflection
1010--------------------------------------------------------------------------------
1111
1212using (xs : Vect k a)
13+ ||| A proof that some element is found in a vector
1314 data Elem : a -> Vect k a -> Type where
1415 Here : Elem x (x::xs)
1516 There : Elem x xs -> Elem x (y::xs)
1617
17−findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic
18+||| A tactic for discovering where, if anywhere, an element is in a vector
19+||| @ n how many elements to search before giving up
20+findElem : (n : Nat) -> List (TTName, Binder TT) -> TT -> Tactic
1821findElem Z ctxt goal = Refine "Here" `Seq` Solve
1922findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))
2023