2a603e4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add documentation to Prelude functions

2a603e4bmsherman12 years ago

libs/prelude/Prelude/Applicative.idr+2

compare with master

unifiedsplit

@@ -38,8 +38,10 @@ class Applicative f => Alternative (f : Type -> Type) where

38 empty : f a

39 (<|>) : f a -> f a -> f a

41+||| `guard a` is `pure ()` if `a` is `True` and `empty` if `a` is `False`

41guard : Alternative f => Bool -> f ()

42guard : Alternative f => Bool -> f ()

42guard a = if a then pure () else empty

43guard a = if a then pure () else empty

45+||| Conditionally execute an applicative expression

44when : Applicative f => Bool -> Lazy (f ()) -> f ()

46when : Applicative f => Bool -> Lazy (f ()) -> f ()

45when a f = if a then Force f else pure ()

47when 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)

22-- Boolean Operator Precedence

23infixl 4 &&, ||

25−||| Boolean OR

25+||| Boolean OR only evaluates the second argument if the first is `False`.

26(||) : Bool -> Lazy Bool -> Bool

27(||) False x = x

28(||) True _ = True

30−||| Boolean AND

30+||| Boolean AND only evaluates the second argument if the first is `True`.

31(&&) : Bool -> Lazy Bool -> Bool

32(&&) True x = x

33(&&) False _ = False

libs/prelude/Prelude/Foldable.idr+17

@@ -14,27 +14,44 @@ class Foldable (t : Type -> Type) where

14foldl : Foldable t => (acc -> elt -> acc) -> acc -> t elt -> acc

15foldl f z t = foldr (flip (.) . flip f) id t z

17+||| Combine each element of a structure into a monoid

17concat : (Foldable t, Monoid a) => t a -> a

18concat : (Foldable t, Monoid a) => t a -> a

18concat = foldr (<+>) neutral

19concat = foldr (<+>) neutral

21+||| Combine into a monoid the collective results of applying a function

22+||| to each element of a structure

20concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m

23concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m

21concatMap f = foldr ((<+>) . f) neutral

24concatMap f = foldr ((<+>) . f) neutral

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.

23and : Foldable t => t (Lazy Bool) -> Bool

29and : Foldable t => t (Lazy Bool) -> Bool

24and = foldl (&&) True

30and = foldl (&&) True

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.

26or : Foldable t => t (Lazy Bool) -> Bool

35or : Foldable t => t (Lazy Bool) -> Bool

27or = foldl (||) False

36or = foldl (||) False

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.

29any : Foldable t => (a -> Bool) -> t a -> Bool

41any : Foldable t => (a -> Bool) -> t a -> Bool

30any p = foldl (\x => \y => x || p y) False

42any p = foldl (\x => \y => x || p y) False

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.

32all : Foldable t => (a -> Bool) -> t a -> Bool

47all : Foldable t => (a -> Bool) -> t a -> Bool

33all p = foldl (\x => \y => x && p y) True

48all p = foldl (\x => \y => x && p y) True

50+||| Add together all the elements of a structure

35sum : (Foldable t, Num a) => t a -> a

51sum : (Foldable t, Num a) => t a -> a

36sum = foldr (+) 0

52sum = foldr (+) 0

54+||| Multiply together all elements of a structure

38product : (Foldable t, Num a) => t a -> a

55product : (Foldable t, Num a) => t a -> a

39product = foldr (*) 1

56product = foldr (*) 1

libs/prelude/Prelude/Maybe.idr+7

@@ -32,10 +32,14 @@ maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b

32maybe n j Nothing = n

33maybe n j (Just x) = (Force j) x

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`.

35fromMaybe : (Lazy a) -> Maybe a -> a

37fromMaybe : (Lazy a) -> Maybe a -> a

36fromMaybe def Nothing = def

38fromMaybe def Nothing = def

37fromMaybe def (Just j) = j

39fromMaybe def (Just j) = j

41+||| Returns `Just` the given value if the conditional is `True`

42+||| and `Nothing` if the conditional is `False`.

39toMaybe : Bool -> Lazy a -> Maybe a

43toMaybe : Bool -> Lazy a -> Maybe a

40toMaybe True j = Just j

44toMaybe True j = Just j

41toMaybe False j = Nothing

45toMaybe False j = Nothing

@@ -43,10 +47,13 @@ toMaybe False j = Nothing

43justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y

47justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y

44justInjective refl = refl

48justInjective refl = refl

50+||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case

51+||| that the `Maybe` value is `Nothing`.

46lowerMaybe : Monoid a => Maybe a -> a

52lowerMaybe : Monoid a => Maybe a -> a

47lowerMaybe Nothing = neutral

53lowerMaybe Nothing = neutral

48lowerMaybe (Just x) = x

54lowerMaybe (Just x) = x

56+||| Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise.

50raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a

57raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a

51raiseToMaybe x = if x == neutral then Nothing else Just x

58raiseToMaybe x = if x == neutral then Nothing else Just x

libs/prelude/Prelude/Stream.idr+3−1

@@ -31,8 +31,10 @@ take : (n : Nat) -> (xs : Stream a) -> Vect n a

31take Z _ = []

32take (S n) (x :: xs) = x :: (take n xs)

34+||| Drop the first n elements from the stream

35+||| @ n how many elements to drop

34%assert_total

36%assert_total

35−drop : Nat -> Stream a -> Stream a

37+drop : (n : Nat) -> Stream a -> Stream a

36drop Z xs = xs

38drop Z xs = xs

37drop (S k) (x::xs) = drop k xs

39drop (S k) (x::xs) = drop k xs