02701e7 · Idris-dev · git.iko.soy

lib/prelude.idr+17

compare with master

unifiedsplit

@@ -108,6 +108,11 @@ instance MonadPlus Maybe where {

108 mplus Nothing Nothing = Nothing;

109}

110

111+instance Monad List where {

112+ return x = [x];

113+ m >>= f = concatMap f m;

114+}

115+

111---- Functors

116---- Functors

112

117

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

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

@@ -173,6 +178,18 @@ floor x = prim__floatFloor x;

173ceiling : Float -> Float;

178ceiling : Float -> Float;

174ceiling x = prim__floatCeil x;

179ceiling x = prim__floatCeil x;

175

180

181+

182+-- Ranges

183+

184+count : Num a => a -> a -> a -> List a;

185+count a inc b = if (a <= b) then (a :: count (a + inc) inc b)

186+ else [];

187+

188+syntax "[" [start] ".." [end] "]"

189+ = count start 1 end;

190+syntax "[" [start] "," [next] ".." [end] "]"

191+ = count start (next - start) end;

192+

176---- some basic io

193---- some basic io

177

194

178putStr : String -> IO ();

195putStr : String -> IO ();

lib/prelude/list.idr+4

@@ -38,6 +38,10 @@ map : (a -> b) -> List a -> List b;

38map f [] = [];

39map f (x :: xs) = f x :: map f xs;

40

41+concatMap : (a -> List b) -> List a -> List b;

42+concatMap f [] = [];

43+concatMap f (x :: xs) = app (f x) (concatMap f xs);

44+

41mapMaybe : (a -> Maybe b) -> List a -> List b;

45mapMaybe : (a -> Maybe b) -> List a -> List b;

42mapMaybe f [] = [];

46mapMaybe f [] = [];

43mapMaybe f (x :: xs) = case f x of {

47mapMaybe f (x :: xs) = case f x of {

test/README+1

@@ -8,3 +8,4 @@ Tests:

8006: Provisional definitions; class resolution in patterns

9007: Applicative and idiom brackets

10008: case and pattern matching let

11+009: ranges and list monad

test/test009/expectednew file+1

@@ -0,0 +1 @@

1+[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50))]

test/test009/runnew file+4

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

1+#!/bin/bash

2+idris test009.idr -o test009

3+./test009

4+rm -f test009 test009.ibc

test/test009/test009.idrnew file+12

@@ -0,0 +1,12 @@

1+module main;

2+

3+pythag : 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+ };

9+

10+main : IO ();

11+main = print (pythag 50);

12+