git.iko.soy/Idris-dev
on master help sign in
Add documentation to Prelude functions
commit2a603e439b14de374acee89187b4bf3de47a9d30 authorbmsherman <bmsherman@users.noreply.github.com> dateThu 1 May 2014, 23:08 (12 years ago) parent334f5b5
5 files changed+31−3
compare with master
unifiedsplit
libs/prelude/Prelude/Applicative.idr+2 libs/prelude/Prelude/Bool.idr+2−2 libs/prelude/Prelude/Foldable.idr+17 libs/prelude/Prelude/Maybe.idr+7 libs/prelude/Prelude/Stream.idr+3−1
libs/prelude/Prelude/Applicative.idr+2
@@ -38,8 +38,10 @@ class Applicative f => Alternative (f : Type -> Type) where
3838 empty : f a
3939 (<|>) : f a -> f a -> f a
4040
41+||| `guard a` is `pure ()` if `a` is `True` and `empty` if `a` is `False`
4142guard : Alternative f => Bool -> f ()
4243guard a = if a then pure () else empty
4344
45+||| Conditionally execute an applicative expression
4446when : Applicative f => Bool -> Lazy (f ()) -> f ()
4547when a f = if a then Force f else pure ()
libs/prelude/Prelude/Bool.idr+2−2
@@ -22,12 +22,12 @@ syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)
2222-- Boolean Operator Precedence
2323infixl 4 &&, ||
2424
25−||| Boolean OR
25+||| Boolean OR only evaluates the second argument if the first is `False`.
2626(||) : Bool -> Lazy Bool -> Bool
2727(||) False x = x
2828(||) True _ = True
2929
30−||| Boolean AND
30+||| Boolean AND only evaluates the second argument if the first is `True`.
3131(&&) : Bool -> Lazy Bool -> Bool
3232(&&) True x = x
3333(&&) False _ = False
libs/prelude/Prelude/Foldable.idr+17
@@ -14,27 +14,44 @@ class Foldable (t : Type -> Type) where
1414foldl : Foldable t => (acc -> elt -> acc) -> acc -> t elt -> acc
1515foldl f z t = foldr (flip (.) . flip f) id t z
1616
17+||| Combine each element of a structure into a monoid
1718concat : (Foldable t, Monoid a) => t a -> a
1819concat = foldr (<+>) neutral
1920
21+||| Combine into a monoid the collective results of applying a function
22+||| to each element of a structure
2023concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m
2124concatMap f = foldr ((<+>) . f) neutral
2225
26+||| The conjunction of all elements of a structure containing
27+||| lazy boolean values. `and` short-circuits from left to right,
28+||| evaluating until either an element is `False` or no elements remain.
2329and : Foldable t => t (Lazy Bool) -> Bool
2430and = foldl (&&) True
2531
32+||| The disjunction of all elements of a structure containing
33+||| lazy boolean values. `or` short-circuits from left to right, evaluating
34+||| either until an element is `True` or no elements remain.
2635or : Foldable t => t (Lazy Bool) -> Bool
2736or = foldl (||) False
2837
38+||| The disjunction of the collective results of applying a
39+||| predicate to all elements of a structure. `any` short-circuits
40+||| from left to right.
2941any : Foldable t => (a -> Bool) -> t a -> Bool
3042any p = foldl (\x => \y => x || p y) False
3143
44+||| The disjunction of the collective results of applying a
45+||| predicate to all elements of a structure. `all` short-circuits
46+||| from left to right.
3247all : Foldable t => (a -> Bool) -> t a -> Bool
3348all p = foldl (\x => \y => x && p y) True
3449
50+||| Add together all the elements of a structure
3551sum : (Foldable t, Num a) => t a -> a
3652sum = foldr (+) 0
3753
54+||| Multiply together all elements of a structure
3855product : (Foldable t, Num a) => t a -> a
3956product = foldr (*) 1
4057
libs/prelude/Prelude/Maybe.idr+7
@@ -32,10 +32,14 @@ maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
3232maybe n j Nothing = n
3333maybe n j (Just x) = (Force j) x
3434
35+||| Convert a `Maybe a` value to an `a` value by providing a default `a` value
36+||| in the case that the `Maybe` value is `Nothing`.
3537fromMaybe : (Lazy a) -> Maybe a -> a
3638fromMaybe def Nothing = def
3739fromMaybe def (Just j) = j
3840
41+||| Returns `Just` the given value if the conditional is `True`
42+||| and `Nothing` if the conditional is `False`.
3943toMaybe : Bool -> Lazy a -> Maybe a
4044toMaybe True j = Just j
4145toMaybe False j = Nothing
@@ -43,10 +47,13 @@ toMaybe False j = Nothing
4347justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y
4448justInjective refl = refl
4549
50+||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case
51+||| that the `Maybe` value is `Nothing`.
4652lowerMaybe : Monoid a => Maybe a -> a
4753lowerMaybe Nothing = neutral
4854lowerMaybe (Just x) = x
4955
56+||| Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise.
5057raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a
5158raiseToMaybe x = if x == neutral then Nothing else Just x
5259
libs/prelude/Prelude/Stream.idr+3−1
@@ -31,8 +31,10 @@ take : (n : Nat) -> (xs : Stream a) -> Vect n a
3131take Z _ = []
3232take (S n) (x :: xs) = x :: (take n xs)
3333
34+||| Drop the first n elements from the stream
35+||| @ n how many elements to drop
3436%assert_total
35−drop : Nat -> Stream a -> Stream a
37+drop : (n : Nat) -> Stream a -> Stream a
3638drop Z xs = xs
3739drop (S k) (x::xs) = drop k xs
3840