git.iko.soy/Idris-dev
on master help sign in
Merge pull request #981 from david-christiansen/docs

Add some docstrings

commit79000bab24aff0f7778417b9bbc78d7ea3532926 authorEdwin Brady <edwin.brady@gmail.com> dateThu 20 Mar 2014, 11:40 (13 years ago) parentca3029210ef56b
8 files changed+64−8
compare with master
unifiedsplit
libs/base/Control/Isomorphism.idr+28−3 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/prelude/IO.idr+10−1 libs/prelude/Prelude/Either.idr+11−1 libs/prelude/Prelude/Monad.idr+4−1
libs/base/Control/Isomorphism.idr+28−3
@@ -4,7 +4,7 @@ import Syntax.PreorderReasoning
44
55%default total
66
7−-- An isomorphism between two types
7+||| An isomorphism between two types
88data Iso : Type -> Type -> Type where
99 MkIso : (to : a -> b) ->
1010 (from : b -> a) ->
@@ -14,9 +14,11 @@ data Iso : Type -> Type -> Type where
1414
1515-- Isomorphism properties
1616
17+||| Isomorphism is reflexive
1718isoRefl : Iso a a
1819isoRefl = MkIso id id (\x => refl) (\x => refl)
1920
21+||| Isomorphism is transitive
2022isoTrans : Iso a b -> Iso b c -> Iso a c
2123isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
2224 MkIso (\x => to' (to x))
@@ -28,11 +30,13 @@ isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
2830 (from (to x)) ={ fromTo x }=
2931 x QED)
3032
33+||| Isomorphism is symmetric
3134isoSym : Iso a b -> Iso b a
3235isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
3336
3437-- Isomorphisms over sums
3538
39+||| Disjunction is commutative
3640eitherComm : Iso (Either a b) (Either b a)
3741eitherComm = MkIso swap swap swapSwap swapSwap
3842 where swap : Either a' b' -> Either b' a' -- a & b are parameters, so fixed!
@@ -42,6 +46,7 @@ eitherComm = MkIso swap swap swapSwap swapSwap
4246 swapSwap (Left x) = refl
4347 swapSwap (Right x) = refl
4448
49+||| Disjunction is associative
4550eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))
4651eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2
4752 where eitherAssoc1 : Either (Either a b) c -> Either a (Either b c)
@@ -64,6 +69,7 @@ eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2
6469 ok2 (Left (Right x)) = refl
6570 ok2 (Right x) = refl
6671
72+||| Disjunction with false is a no-op
6773eitherBotLeft : Iso (Either _|_ a) a
6874eitherBotLeft = MkIso to from ok1 ok2
6975 where to : Either _|_ a -> a
@@ -77,10 +83,11 @@ eitherBotLeft = MkIso to from ok1 ok2
7783 ok2 (Left x) = FalseElim x
7884 ok2 (Right x) = refl
7985
86+||| Disjunction with false is a no-op
8087eitherBotRight : Iso (Either a _|_) a
8188eitherBotRight = isoTrans eitherComm eitherBotLeft
8289
83−
90+||| Isomorphism is a congruence with regards to disjunction
8491eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')
8592eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
8693 (MkIso to from toFrom fromTo)
@@ -96,21 +103,25 @@ eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
96103 ok2 (Left x) = cong (fromTo x)
97104 ok2 (Right x) = cong (fromTo' x)
98105
106+||| Isomorphism is a congruence with regards to disjunction on the left
99107eitherCongLeft : Iso a a' -> Iso (Either a b) (Either a' b)
100108eitherCongLeft i = eitherCong i isoRefl
101109
110+||| Isomorphism is a congruence with regards to disjunction on the right
102111eitherCongRight : Iso b b' -> Iso (Either a b) (Either a b')
103112eitherCongRight i = eitherCong isoRefl i
104113
105114-- Isomorphisms over products
115+||| Conjunction is commutative
106116pairComm : Iso (a, b) (b, a)
107117pairComm = MkIso swap swap swapSwap swapSwap
108118 where swap : (a', b') -> (b', a')
109119 swap (x, y) = (y, x)
110−
120+
111121 swapSwap : (x : (a', b')) -> swap (swap x) = x
112122 swapSwap (x, y) = refl
113123
124+||| Conjunction is associative
114125pairAssoc : Iso (a, (b, c)) ((a, b), c)
115126pairAssoc = MkIso to from ok1 ok2
116127 where
@@ -123,20 +134,25 @@ pairAssoc = MkIso to from ok1 ok2
123134 ok2 : (x : (a, (b, c))) -> from (to x) = x
124135 ok2 (x, (y, z)) = refl
125136
137+||| Conjunction with truth is a no-op
126138pairUnitRight : Iso (a, ()) a
127139pairUnitRight = MkIso fst (\x => (x, ())) (\x => refl) ok
128140 where ok : (x : (a, ())) -> (fst x, ()) = x
129141 ok (x, ()) = refl
130142
143+||| Conjunction with truth is a no-op
131144pairUnitLeft : Iso ((), a) a
132145pairUnitLeft = isoTrans pairComm pairUnitRight
133146
147+||| Conjunction preserves falsehood
134148pairBotLeft : Iso (_|_, a) _|_
135149pairBotLeft = MkIso fst FalseElim (\x => FalseElim x) (\y => FalseElim (fst y))
136150
151+||| Conjunction preserves falsehood
137152pairBotRight : Iso (a, _|_) _|_
138153pairBotRight = isoTrans pairComm pairBotLeft
139154
155+||| Isomorphism is a congruence with regards to conjunction
140156pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')
141157pairCong {a = a} {a' = a'} {b = b} {b' = b'}
142158 (MkIso to from toFrom fromTo)
@@ -155,13 +171,16 @@ pairCong {a = a} {a' = a'} {b = b} {b' = b'}
155171 rewrite fromTo' y in
156172 refl
157173
174+||| Isomorphism is a congruence with regards to conjunction on the left
158175pairCongLeft : Iso a a' -> Iso (a, b) (a', b)
159176pairCongLeft i = pairCong i isoRefl
160177
178+||| Isomorphism is a congruence with regards to conjunction on the right
161179pairCongRight : Iso b b' -> Iso (a, b) (a, b')
162180pairCongRight = pairCong isoRefl
163181
164182-- Distributivity of products over sums
183+||| Products distribute over sums
165184distribLeft : Iso (Either a b, c) (Either (a, c) (b, c))
166185distribLeft = MkIso to from toFrom fromTo
167186 where to : (Either a b, c) -> Either (a, c) (b, c)
@@ -177,20 +196,24 @@ distribLeft = MkIso to from toFrom fromTo
177196 fromTo (Left x, y) = refl
178197 fromTo (Right x, y) = refl
179198
199+||| Products distribute over sums
180200distribRight : Iso (a, Either b c) (Either (a, b) (a, c))
181201distribRight {a} {b} {c} = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
182202
183203
184204-- Enable preorder reasoning syntax over isomorphisms
205+||| Used for preorder reasoning syntax. Not intended for direct use.
185206qed : (a : Type) -> Iso a a
186207qed a = isoRefl
187208
209+||| Used for preorder reasoning syntax. Not intended for direct use.
188210step : (a : Type) -> Iso a b -> Iso b c -> Iso a c
189211step a iso1 iso2 = isoTrans iso1 iso2
190212
191213
192214
193215-- Isomorphisms over Maybe
216+||| Isomorphism is a congruence with respect to Maybe
194217maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
195218maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
196219 where ok1 : (y : Maybe b) -> map to (map from y) = y
@@ -200,6 +223,7 @@ maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1
200223 ok2 Nothing = refl
201224 ok2 (Just x) = (Just (from (to x))) ={ cong (fromTo x) }= (Just x) QED
202225
226+||| `Maybe a` is the same as `Either a ()`
203227maybeEither : Iso (Maybe a) (Either a ())
204228maybeEither = MkIso to from iso1 iso2
205229 where to : Maybe a -> Either a ()
@@ -215,6 +239,7 @@ maybeEither = MkIso to from iso1 iso2
215239 iso2 Nothing = refl
216240 iso2 (Just x) = refl
217241
242+||| Maybe of void is just unit
218243maybeVoidUnit : Iso (Maybe _|_) ()
219244maybeVoidUnit = (Maybe _|_) ={ maybeEither }=
220245 (Either _|_ ()) ={ eitherBotLeft }=
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
libs/prelude/IO.idr+10−1
@@ -4,8 +4,10 @@ import Prelude.List
44
55%access public
66
7+||| Idris's primitive IO, for building abstractions on top of
78abstract data PrimIO a = prim__IO a
89
10+||| A token representing the world, for use in `IO`
911abstract data World = TheWorld
1012
1113abstract WorldRes : Type -> Type
@@ -26,7 +28,10 @@ abstract
2628prim_io_return : a -> PrimIO a
2729prim_io_return x = prim__IO x
2830
31+||| Descriptions of the various sorts of Ints that Idris supports
2932data IntTy = ITChar | ITNative | IT8 | IT16 | IT32 | IT64 | IT8x16 | IT16x8 | IT32x4 | IT64x2
33+
34+||| Types available for foreign function calls
3035data FTy = FIntT IntTy
3136 | FFunction FTy FTy
3237 | FFloat
@@ -75,6 +80,7 @@ FBits32x4 = FIntT IT32x4
7580FBits64x2 : FTy
7681FBits64x2 = FIntT IT64x2
7782
83+||| Interpret an FFI type as the type of the Idris function that it will become
7884interpFTy : FTy -> Type
7985interpFTy (FIntT ITNative) = Int
8086interpFTy (FIntT ITChar) = Char
@@ -95,7 +101,10 @@ interpFTy FUnit = ()
95101
96102interpFTy (FFunction a b) = interpFTy a -> interpFTy b
97103
98−ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
104+||| Type signatures for foreign functions
105+||| @ xs the argument types
106+||| @ t the return type
107+ForeignTy : (xs : List FTy) -> (t : FTy) -> Type
99108ForeignTy Nil rt = World -> PrimIO (interpFTy rt)
100109ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt
101110
libs/prelude/Prelude/Either.idr+11−1
@@ -16,10 +16,12 @@ data Either a b =
1616-- Syntactic tests
1717--------------------------------------------------------------------------------
1818
19+||| True if the argument is Left, False otherwise
1920isLeft : Either a b -> Bool
2021isLeft (Left l) = True
2122isLeft (Right r) = False
2223
24+||| True if the argument is Right, False otherwise
2325isRight : Either a b -> Bool
2426isRight (Left l) = False
2527isRight (Right r) = True
@@ -41,6 +43,7 @@ either : (f : a -> c) -> (g : b -> c) -> (e : Either a b) -> c
4143either l r (Left x) = l x
4244either l r (Right x) = r x
4345
46+||| Keep the payloads of all Left constructors in a list of Eithers
4447lefts : List (Either a b) -> List a
4548lefts [] = []
4649lefts (x::xs) =
@@ -48,6 +51,7 @@ lefts (x::xs) =
4851 Left l => l :: lefts xs
4952 Right r => lefts xs
5053
54+||| Keep the payloads of all Right constructors in a list of Eithers
5155rights : List (Either a b) -> List b
5256rights [] = []
5357rights (x::xs) =
@@ -55,9 +59,11 @@ rights (x::xs) =
5559 Left l => rights xs
5660 Right r => r :: rights xs
5761
62+||| Split a list of Eithers into a list of the left elements and a list of the right elements
5863partitionEithers : List (Either a b) -> (List a, List b)
5964partitionEithers l = (lefts l, rights l)
6065
66+||| Remove a "useless" Either by collapsing the case distinction
6167fromEither : Either a a -> a
6268fromEither (Left l) = l
6369fromEither (Right r) = r
@@ -66,7 +72,9 @@ fromEither (Right r) = r
6672-- Conversions
6773--------------------------------------------------------------------------------
6874
69−maybeToEither : e -> Maybe a -> Either e a
75+||| Convert a Maybe to an Either by using a default value in case of Nothing
76+||| @ e the default value
77+maybeToEither : (def : e) -> Maybe a -> Either e a
7078maybeToEither def (Just j) = Right j
7179maybeToEither def Nothing = Left def
7280
@@ -86,10 +94,12 @@ instance (Eq a, Eq b) => Eq (Either a b) where
8694-- Injectivity of constructors
8795--------------------------------------------------------------------------------
8896
97+||| Left is injective
8998total leftInjective : {b : Type} -> {x : a} -> {y : a}
9099 -> (Left {b = b} x = Left {b = b} y) -> (x = y)
91100leftInjective refl = refl
92101
102+||| Right is injective
93103total rightInjective : {a : Type} -> {x : b} -> {y : b}
94104 -> (Right {a = a} x = Right {a = a} y) -> (x = y)
95105rightInjective refl = refl
libs/prelude/Prelude/Monad.idr+4−1
@@ -13,8 +13,11 @@ infixl 5 >>=
1313class Applicative m => Monad (m : Type -> Type) where
1414 (>>=) : m a -> (a -> m b) -> m b
1515
16+||| Also called `join` or mu
1617flatten : Monad m => m (m a) -> m a
1718flatten a = a >>= id
1819
20+||| For compatibility with Haskell. Note that monads are **not** free to
21+||| define `return` and `pure` differently!
1922return : Monad m => a -> m a
20−return = pure
23+return = pure