7a2de6d · Idris-dev · git.iko.soy

idris.cabal+1−1

compare with master

unifiedsplit

@@ -126,7 +126,7 @@ Extra-source-files:

126 libs/effects/Makefile

127 libs/effects/effects.ipkg

128 libs/effects/Effect/*.idr

129− libs/effects/Effect/Logging/*.idr

129+ libs/effects/Effect/Logging/*.idr

130 libs/effects/*.idr

131

132 test/Makefile

test/effects005/defaultlog.idr → test/effects005/categoryLogger.idrrenamed+1−1

@@ -1,5 +1,5 @@

1import Effects

2−import Effect.Logging

2+import Effect.Logging.Category

3

4func : Nat -> Eff () [LOG String]

5func x = do

test/effects005/defaultLogger.idrnew file+14

@@ -0,0 +1,14 @@

1+import Effects

2+import Effect.Logging.Default

3+

4+doubleFunc : Nat -> Eff Nat [LOG]

5+doubleFunc x = do

6+ warn $ unwords ["Doing the double with", show x ]

7+ pure (x+x)

8+

9+main : IO ()

10+main = do

11+ x <- runInit [MkLogRes ALL] (doubleFunc 3)

12+ printLn x

13+ y <- run (doubleFunc 4)

14+ printLn y

test/effects005/expected+1−1

@@ -1,4 +1,4 @@

1−3 : Doing the double with 3

1+WARN : Doing the double with 3

26

38

4WARN : ["NumOPS"] : Doing the double with 3

test/effects005/run+4−4

@@ -1,6 +1,6 @@

1#!/usr/bin/env bash

2−idris $@ simplelog.idr -o simple -p effects

3−./simple

4−idris $@ defaultlog.idr -o default -p effects

2+idris $@ defaultLogger.idr -o default -p effects

5./default

3./default

4+idris $@ categoryLogger.idr -o category -p effects

5+./category

6−rm -f simple default *.ibc

6+rm -f default category *.ibc

test/effects005/simplelog.idrdeleted−14

@@ -1,14 +0,0 @@

1−import Effects

2−import Effect.Logging.Simple

3−

4−doubleFunc : Nat -> Eff Nat [LOG]

5−doubleFunc x = do

6− log 3 $ unwords ["Doing the double with", show x ]

7− pure (x+x)

8−

9−main : IO ()

10−main = do

11− x <- runInit [7] (doubleFunc 3)

12− printLn x

13− y <- runInit [0] (doubleFunc 4)

14− printLn y