Numeric ranges [a..b], [a,b .. c] and list monad

lib/prelude.idr

@@ -108,6 +108,11 @@ instance MonadPlus Maybe where {
     mplus Nothing Nothing  = Nothing;
 }
 
+instance Monad List where {
+    return x = [x];
+    m >>= f = concatMap f m;
+}
+
 ---- Functors
 
 class Functor (f : Set -> Set) where {
@@ -173,6 +178,18 @@ floor x = prim__floatFloor x;
 ceiling : Float -> Float;
 ceiling x = prim__floatCeil x;
 
+
+-- Ranges
+
+count : Num a => a -> a -> a -> List a;
+count a inc b = if (a <= b) then (a :: count (a + inc) inc b)
+                            else [];
+  
+syntax "[" [start] ".." [end] "]" 
+     = count start 1 end;
+syntax "[" [start] "," [next] ".." [end] "]" 
+     = count start (next - start) end;
+
 ---- some basic io
 
 putStr : String -> IO ();

lib/prelude/list.idr

@@ -38,6 +38,10 @@ map : (a -> b) -> List a -> List b;
 map f []        = [];
 map f (x :: xs) = f x :: map f xs;
 
+concatMap : (a -> List b) -> List a -> List b;
+concatMap f [] = [];
+concatMap f (x :: xs) = app (f x) (concatMap f xs);
+
 mapMaybe : (a -> Maybe b) -> List a -> List b;
 mapMaybe f [] = [];
 mapMaybe f (x :: xs) = case f x of {

test/README

@@ -8,3 +8,4 @@ Tests:
 006: Provisional definitions; class resolution in patterns
 007: Applicative and idiom brackets
 008: case and pattern matching let
+009: ranges and list monad

test/test009/expected

@@ -0,0 +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/run

@@ -0,0 +1,4 @@
+#!/bin/bash
+idris test009.idr -o test009
+./test009
+rm -f test009 test009.ibc

test/test009/test009.idr

@@ -0,0 +1,12 @@
+module main;
+
+pythag : Int -> List (Int, Int, Int);
+pythag n = do { z <- [1..n];
+                y <- [1..z];
+                x <- [1..y];
+                if (x * x + y * y == z * z) then (return (x, y, z)) else [];
+              };
+
+main : IO ();
+main = print (pythag 50);
+