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

lib/prelude.idr+13

compare with master

unifiedsplit

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

88 mzero : m a;

89}

90

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

92+ fail : String -> m ();

93+}

94+

91instance Monad IO where {

95instance Monad IO where {

92 return t = io_return t;

96 return t = io_return t;

93 b >>= k = io_bind b k;

97 b >>= k = io_bind b k;

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

113 m >>= f = concatMap f m;

117 m >>= f = concatMap f m;

114}

118}

115

119

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+

116---- Functors

129---- Functors

117

130

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

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

src/Idris/Parser.hs+11

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

428

429pNoExtExpr syn =

430 try (pApp syn)

431+ <|> try (pComprehension syn)

431 <|> pSimpleExpr syn

432 <|> pSimpleExpr syn

432 <|> pLambda syn

433 <|> pLambda syn

433 <|> pLet syn

434 <|> pLet syn

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

700bindList b [] sc = sc

701bindList b [] sc = sc

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

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

702

703

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+

703pDoBlock syn

714pDoBlock syn

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

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

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

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

test/test009/test009.idr+2−5

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

1module main;

2

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

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

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

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

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

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

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

8− };

9

6

10main : IO ();

7main : IO ();

11main = print (pythag 50);

8main = print (pythag 50);

tutorial/idris-tutorial.pdf

Binary file not shown.