1c2098a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added infinite list syntax [1..], [1,3,...] etc

1c2098aEdwin Brady15 years ago

lib/prelude.idr+8

@@ -158,11 +158,19 @@ count : Num a => a -> a -> a -> List a

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

159 else []

160

161+countFrom : Num a => a -> a -> List a

162+countFrom a inc = a :: lazy (countFrom (a + inc) inc)

163+

161syntax "[" [start] ".." [end] "]"

164syntax "[" [start] ".." [end] "]"

162 = count start 1 end

165 = count start 1 end

163syntax "[" [start] "," [next] ".." [end] "]"

166syntax "[" [start] "," [next] ".." [end] "]"

164 = count start (next - start) end

167 = count start (next - start) end

165

168

169+syntax "[" [start] "..]"

170+ = countFrom start 1

171+syntax "[" [start] "," [next] "..]"

172+ = countFrom start (next - start)

173+

166---- More utilities

174---- More utilities

167

175

168sum : Num a => List a -> a

176sum : Num a => List a -> a

src/Idris/AbsSyntax.hs+2

@@ -1401,6 +1401,8 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1401 | PConstant (I _) <- getTm x = match (getTm x) x'

1402 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])

1403 | PConstant (I _) <- getTm x = match (getTm x) x'

1404+ match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'

1405+ match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')

1404 match (PApp _ f args) (PApp _ f' args')

1406 match (PApp _ f args) (PApp _ f' args')

1405 | length args == length args'

1407 | length args == length args'

1406 = do mf <- match' f f'

1408 = do mf <- match' f f'