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

git.iko.soy/Idris-dev

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

(But it doesn't work at the REPL yet because that doesn't respect 'lazy' annotations properly)

commit1c2098a49c4f5147de534e3dc41d5f0469bea0ea authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 23 Feb 2012, 17:54 (15 years ago) parent022e230

2 files changed+10

unifiedsplit

lib/prelude.idr+8

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

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

159159 else []

160160

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

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

163+

161164syntax "[" [start] ".." [end] "]"

162165 = count start 1 end

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

164167 = count start (next - start) end

165168

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

170+ = countFrom start 1

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

172+ = countFrom start (next - start)

173+

166174---- More utilities

167175

168176sum : 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

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

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

14031403 | 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')

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

14051407 | length args == length args'

14061408 = do mf <- match' f f'