c2bd084 · Idris-dev · git.iko.soy

libs/effects/Effects.idr+2−2

compare with master

unifiedsplit

@@ -337,8 +337,8 @@ mapVE f [] = pure []

337mapVE f (x :: xs) = [| f x :: mapVE f xs |]

338

339

340−when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()

340+when : Applicative m => Bool -> Lazy ({xs} Eff m ()) -> {xs} Eff m ()

341−when True e = e

341+when True e = Force e

342when False e = pure ()

343

344-- --------------------------------------------------------------------- [ EOF ]

libs/oldeffects/Effects.idr+1−1

@@ -303,6 +303,6 @@ mapE : Applicative m => (a -> Eff m xs b) -> List a -> Eff m xs (List b)

303mapE f [] = pure []

304mapE f (x :: xs) = [| f x :: mapE f xs |]

305

306−when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()

306+when : Applicative m => Bool -> Lazy (Eff m xs ()) -> Eff m xs ()

307when True e = e

308when False e = pure ()

libs/prelude/Prelude/Applicative.idr+2−2

@@ -41,5 +41,5 @@ class Applicative f => Alternative (f : Type -> Type) where

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

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

43

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

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

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

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

libs/prelude/Prelude/Bool.idr+2−2

@@ -23,12 +23,12 @@ syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

23infixl 4 &&, ||

24

25||| Boolean OR

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

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

27(||) False x = x

28(||) True _ = True

29

30||| Boolean AND

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

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

32(&&) True x = x

33(&&) False _ = False

34

libs/prelude/Prelude/Either.idr+4−4

@@ -39,9 +39,9 @@ choose False = Right oh

39||| @ f the action to take on Left

40||| @ g the action to take on Right

41||| @ e the sum to analyze

42−either : (f : a -> c) -> (g : b -> c) -> (e : Either a b) -> c

42+either : (f : Lazy (a -> c)) -> (g : Lazy (b -> c)) -> (e : Either a b) -> c

43−either l r (Left x) = l x

43+either l r (Left x) = (Force l) x

44−either l r (Right x) = r x

44+either l r (Right x) = (Force r) x

45

46||| Keep the payloads of all Left constructors in a list of Eithers

47lefts : List (Either a b) -> List a

@@ -74,7 +74,7 @@ fromEither (Right r) = r

74

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

77+maybeToEither : (def : Lazy e) -> Maybe a -> Either e a

78maybeToEither def (Just j) = Right j

79maybeToEither def Nothing = Left def

80

libs/prelude/Prelude/Foldable.idr+6−6

@@ -20,17 +20,17 @@ concat = foldr (<+>) neutral

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

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

22

23−and : Foldable t => t Bool -> Bool

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

24−and = foldr (&&) True

24+and = foldr (flip (&&)) True

25

26−or : Foldable t => t Bool -> Bool

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

27−or = foldr (||) False

27+or = foldr (flip (||)) False

28

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

30−any p = foldr ((||) . p) False

30+any p = foldr (flip (||) . Delay . p) False

31

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

33−all p = foldr ((&&) . p) True

33+all p = foldr (flip (&&) . Delay . p) True

34

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

36sum = foldr (+) 0

libs/prelude/Prelude/List.idr+2−2

@@ -182,9 +182,9 @@ dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs

182||| @ nil what to return at the end of the list

183||| @ cons what to do at each step of recursion

184||| @ xs the list to recurse over

185−list : (nil : b) -> (cons : a -> List a -> b) -> (xs : List a) -> b

185+list : (nil : Lazy b) -> (cons : Lazy (a -> List a -> b)) -> (xs : List a) -> b

186list nil cons [] = nil

187−list nil cons (x::xs) = cons x xs

187+list nil cons (x::xs) = (Force cons) x xs

188

189--------------------------------------------------------------------------------

190-- Building (bigger) lists

libs/prelude/Prelude/Maybe.idr+3−3

@@ -28,15 +28,15 @@ isJust (Just j) = True

28-- Misc

29--------------------------------------------------------------------------------

30

31−maybe : Lazy b -> (a -> b) -> Maybe a -> b

31+maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b

32maybe n j Nothing = n

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

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

34

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

36fromMaybe def Nothing = def

37fromMaybe def (Just j) = j

38

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

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

40toMaybe True j = Just j

41toMaybe False j = Nothing

42