git.iko.soy/Idris-dev
on master help sign in
Numeric ranges [a..b], [a,b .. c] and list monad
commit02701e7befb4b57eb17966daf9336d9cf68c119c authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 6 Jan 2012, 15:11 (15 years ago) parent2a50169
6 files changed+39
compare with master
unifiedsplit
lib/prelude.idr+17 lib/prelude/list.idr+4 test/README+1 test/test009/expected+1 test/test009/run+4 test/test009/test009.idr+12
lib/prelude.idr+17
@@ -108,6 +108,11 @@ instance MonadPlus Maybe where {
108108 mplus Nothing Nothing = Nothing;
109109}
110110
111+instance Monad List where {
112+ return x = [x];
113+ m >>= f = concatMap f m;
114+}
115+
111116---- Functors
112117
113118class Functor (f : Set -> Set) where {
@@ -173,6 +178,18 @@ floor x = prim__floatFloor x;
173178ceiling : Float -> Float;
174179ceiling x = prim__floatCeil x;
175180
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+
176193---- some basic io
177194
178195putStr : String -> IO ();
lib/prelude/list.idr+4
@@ -38,6 +38,10 @@ map : (a -> b) -> List a -> List b;
3838map f [] = [];
3939map f (x :: xs) = f x :: map f xs;
4040
41+concatMap : (a -> List b) -> List a -> List b;
42+concatMap f [] = [];
43+concatMap f (x :: xs) = app (f x) (concatMap f xs);
44+
4145mapMaybe : (a -> Maybe b) -> List a -> List b;
4246mapMaybe f [] = [];
4347mapMaybe f (x :: xs) = case f x of {
test/README+1
@@ -8,3 +8,4 @@ Tests:
88006: Provisional definitions; class resolution in patterns
99007: Applicative and idiom brackets
1010008: 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+