817c1a0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Monad comprehension notation

commit817c1a09a8492d924fafbee4bbb1ab89d4f35d3f authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 6 Jan 2012, 15:58 (15 years ago) parent93c06b5

4 files changed+26−5

compare with master

unifiedsplit

lib/prelude.idr+13 src/Idris/Parser.hs+11 test/test009/test009.idr+2−5 tutorial/idris-tutorial.pdf

lib/prelude.idr+13

@@ -88,6 +88,10 @@ class Monad m => MonadPlus (m : Set -> Set) where {

8888 mzero : m a;

8989}

9090

91+class Monad m => MonadFail (m : Set -> Set) where {

92+ fail : String -> m ();

93+}

94+

9195instance Monad IO where {

9296 return t = io_return t;

9397 b >>= k = io_bind b k;

@@ -113,6 +117,15 @@ instance Monad List where {

113117 m >>= f = concatMap f m;

114118}

115119

120+instance MonadPlus List where {

121+ mzero = [];

122+ mplus = app;

123+}

124+

125+guard : MonadPlus m => Bool -> m ();

126+guard True = return ();

127+guard False = mzero;

128+

116129---- Functors

117130

118131class Functor (f : Set -> Set) where {

src/Idris/Parser.hs+11

@@ -428,6 +428,7 @@ pSimpleExtExpr syn = do i <- getState

428428

429429pNoExtExpr syn =

430430 try (pApp syn)

431+ <|> try (pComprehension syn)

431432 <|> pSimpleExpr syn

432433 <|> pLambda syn

433434 <|> pLet syn

@@ -700,6 +701,16 @@ tyOptDeclList syn = sepBy1 (do x <- pfName;

700701bindList b [] sc = sc

701702bindList b ((n, t):bs) sc = b n t (bindList b bs sc)

702703

704+pComprehension syn

705+ = do lchar '['; fc <- pfc; pat <- pExpr syn; lchar '|';

706+ qs <- sepBy1 (pDo syn) (lchar ','); lchar ']';

707+ return (PDoBlock (map addGuard qs ++

708+ [DoExp fc (PApp fc (PRef fc (NS (UN "return") ["prelude"]))

709+ [pexp pat])]))

710+ where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (NS (UN "guard") ["prelude"]))

711+ [pexp e])

712+ addGuard x = x

713+

703714pDoBlock syn

704715 = do reserved "do"; lchar '{'

705716 ds <- endBy1 (pDo syn) (lchar ';')

test/test009/test009.idr+2−5

@@ -1,11 +1,8 @@

11module main;

33pythag : Int -> List (Int, Int, Int);

4−pythag n = do { z <- [1..n];

5− y <- [1..z];

6− x <- [1..y];

7− if (x * x + y * y == z * z) then (return (x, y, z)) else [];

8− };

4+pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],

5+ x*x + y*y == z*z ];

107main : IO ();

118main = print (pythag 50);

tutorial/idris-tutorial.pdf

Binary file not shown.