a0c98e4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:idris-lang/Idris-dev

commita0c98e42b8bdcd5b1b15d8b467a1650accadefb8 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 3 Aug 2016, 17:56 (10 years ago) parent2100241 652b0fe

15 files changed+89−34

compare with master

unifiedsplit

CHANGELOG.md+1 idris.cabal+6 libs/prelude/Prelude.idr+31−23 src/Idris/Package.hs+13−7 src/Idris/Package/Common.hs+2−2 src/Idris/Package/Parser.hs+1−1 test/TestData.hs+3−1 test/basic013/basic013.idr+9 test/basic013/expected+9 test/pkg005/expected+1 test/pkg005/run+3 test/pkg005/test.ipkg+3 test/pkg006/expected+1 test/pkg006/run+3 test/pkg006/test.ipkg+3

CHANGELOG.md+1

@@ -25,6 +25,7 @@

2525

2626* The File Effect has been updated to take into account changes in

2727 `Prelude.File` and to provide a 'better' API.

28+* `natEnumFromThen` and `natEnumFromTo` have been updated to correctly calculate reverse ranges. Range syntax `[a,b..c]` now can be used again to generate reverse ranges.

2829

2930## Tool updates

3031

idris.cabal+6

@@ -669,6 +669,12 @@ Extra-source-files:

669669 test/pkg004/*.idr

670670 test/pkg004/expected

671671 test/pkg004/*.ipkg

672+ test/pkg005/run

673+ test/pkg005/expected

674+ test/pkg005/*.ipkg

675+ test/pkg006/run

676+ test/pkg006/expected

677+ test/pkg006/*.ipkg

672678

673679 test/proof001/run

674680 test/proof001/*.idr

libs/prelude/Prelude.idr+31−23

@@ -146,12 +146,18 @@ natRange n = List.reverse (go n)

146146

147147-- predefine Nat versions of Enum, so we can use them in the default impls

148148total natEnumFromThen : Nat -> Nat -> Stream Nat

149−natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc

149+natEnumFromThen n next = n :: natEnumFromThen next (minus next n)

150150total natEnumFromTo : Nat -> Nat -> List Nat

151−natEnumFromTo n m = map (plus n) (natRange (minus (S m) n))

151+natEnumFromTo n m = if n <= m

152+ then go n m

153+ else List.reverse $ go m n

154+ where go : Nat -> Nat -> List Nat

155+ go n m = map (plus n) (natRange (minus (S m) n))

156+total natEnumFromThenTo' : Nat -> Nat -> Nat -> List Nat

157+natEnumFromThenTo' _ Z _ = []

158+natEnumFromThenTo' n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))

152159total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat

153−natEnumFromThenTo _ Z _ = []

154−natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))

160+natEnumFromThenTo n next m = natEnumFromThenTo' n (minus next n) m

155161

156162interface Enum a where

157163 total pred : a -> a

@@ -184,36 +190,38 @@ Enum Integer where

184190 fromNat n = cast n

185191 enumFromThen n inc = n :: enumFromThen (inc + n) inc

186192 enumFromTo n m = if n <= m

187− then go (natRange (S (cast {to = Nat} (m - n))))

188− else []

189− where go : List Nat -> List Integer

190− go [] = []

191− go (x :: xs) = n + cast x :: go xs

193+ then go n m

194+ else List.reverse $ go m n

195+ where go' : Integer -> List Nat -> List Integer

196+ go' _ [] = []

197+ go' n (x :: xs) = n + cast x :: go' n xs

198+ go : Integer -> Integer -> List Integer

199+ go n m = go' n (natRange (S (cast {to = Nat} (m - n))))

192200 enumFromThenTo _ 0 _ = []

193− enumFromThenTo n inc m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs inc) - 1))) SIsNotZ)))

201+ enumFromThenTo n next m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ)))

194202 where go : List Nat -> List Integer

195203 go [] = []

196− go (x :: xs) = n + (cast x * inc) :: go xs

204+ go (x :: xs) = n + (cast x * (next - n)) :: go xs

197205

198206Enum Int where

199207 pred n = n - 1

200208 succ n = n + 1

201209 toNat n = cast n

202210 fromNat n = cast n

203− enumFromTo n m =

204− if n <= m

205− then go [] (cast {to = Nat} (m - n)) m

206− else []

207− where

208− go : List Int -> Nat -> Int -> List Int

209− go acc Z m = m :: acc

210− go acc (S k) m = go (m :: acc) k (m - 1)

211+ enumFromTo n m = if n <= m

212+ then go n m

213+ else List.reverse $ go m n

214+ where go' : List Int -> Nat -> Int -> List Int

215+ go' acc Z m = m :: acc

216+ go' acc (S k) m = go' (m :: acc) k (m - 1)

217+ go : Int -> Int -> List Int

218+ go n m = go' [] (cast {to = Nat} (m - n)) m

211219 enumFromThen n inc = n :: enumFromThen (inc + n) inc

212220 enumFromThenTo _ 0 _ = []

213− enumFromThenTo n inc m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs inc) - 1))) SIsNotZ)))

221+ enumFromThenTo n next m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))

214222 where go : List Nat -> List Int

215223 go [] = []

216− go (x :: xs) = n + (cast x * inc) :: go xs

224+ go (x :: xs) = n + (cast x * (next - n)) :: go xs

217225

218226Enum Char where

219227 toNat c = toNat (ord c)

@@ -224,12 +232,12 @@ Enum Char where

224232syntax "[" [start] ".." [end] "]"

225233 = enumFromTo start end

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

227− = enumFromThenTo start (next - start) end

235+ = enumFromThenTo start next end

228236

229237syntax "[" [start] ".." "]"

230238 = enumFrom start

231239syntax "[" [start] "," [next] ".." "]"

232− = enumFromThen start (next - start)

240+ = enumFromThen start next

233241

234242---- More utilities

235243

src/Idris/Package.hs+13−7

@@ -82,7 +82,7 @@ buildPkg copts warnonly (install, fp) = do

8282 Left emsg -> do

8383 putStrLn emsg

8484 exitWith (ExitFailure 1)

85− Right opts -> buildMods opts [idris_main pkgdesc]

85+ Right opts -> buildMain opts (idris_main pkgdesc)

8686 case m_ist of

8787 Nothing -> exitWith (ExitFailure 1)

8888 Just ist -> do

@@ -91,6 +91,11 @@ buildPkg copts warnonly (install, fp) = do

9191 Just _ -> exitWith (ExitFailure 1)

9292 _ -> return ()

9393 when install $ installPkg (opt getIBCSubDir copts) pkgdesc

94+ where

95+ buildMain opts (Just mod) = buildMods opts [mod]

96+ buildMain _ Nothing = do

97+ putStrLn "Can't build an executable: No main module given"

98+ exitWith (ExitFailure 1)

9499

95100-- --------------------------------------------------------- [ Check Packages ]

96101

@@ -140,20 +145,21 @@ replPkg copts fp = do

140145 case mergeOptions copts (idris_opts pkgdesc) of

141146 Left emsg -> ifail emsg

142147 Right opts -> do

143− let mod = idris_main pkgdesc

144− let f = toPath (showCG mod)

145148 putIState orig

146149 dir <- runIO getCurrentDirectory

147150 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc

148−

149− if (f /= "")

150− then idrisMain ((Filename f) : opts)

151− else iputStrLn "Can't start REPL: no main module given"

151+ runMain opts (idris_main pkgdesc)

152152 runIO $ setCurrentDirectory dir

153153

154154 where

155155 toPath n = foldl1' (</>) $ splitOn "." n

156156

157+ runMain opts (Just mod) = do

158+ let f = toPath (showCG mod)

159+ idrisMain ((Filename f) : opts)

160+ runMain _ Nothing =

161+ iputStrLn "Can't start REPL: no main module given"

162+

157163-- --------------------------------------------------------------- [ Cleaning ]

158164

159165-- | Clean Package build files

src/Idris/Package/Common.hs+2−2

@@ -30,7 +30,7 @@ data PkgDesc = PkgDesc {

3030 , idris_opts :: [Opt] -- ^ List of options to give the compiler.

3131 , sourcedir :: String -- ^ Source directory for Idris files.

3232 , modules :: [Name] -- ^ Modules provided by the package.

33− , idris_main :: Name -- ^ If an executable in which module can the Main namespace and function be found.

33+ , idris_main :: Maybe Name -- ^ If an executable in which module can the Main namespace and function be found.

3434 , execout :: Maybe String -- ^ What to call the executable.

3535 , idris_tests :: [Name] -- ^ Lists of tests to execute against the package.

3636 } deriving (Show)

@@ -39,4 +39,4 @@ data PkgDesc = PkgDesc {

3939defaultPkg :: PkgDesc

4040defaultPkg = PkgDesc "" [] Nothing Nothing Nothing Nothing

4141 Nothing Nothing Nothing Nothing

42− Nothing [] [] Nothing [] "" [] (sUN "") Nothing []

42+ Nothing [] [] Nothing [] "" [] Nothing Nothing []

src/Idris/Package/Parser.hs+1−1

@@ -127,7 +127,7 @@ pClause = do reserved "executable"; lchar '=';

127127 <|> do reserved "main"; lchar '=';

128128 main <- fst <$> iName []

129129 st <- get

130− put (st { idris_main = main })

130+ put (st { idris_main = Just main })

131131

132132 <|> do reserved "sourcedir"; lchar '=';

133133 src <- fst <$> identifier

test/TestData.hs+3−1

@@ -171,7 +171,9 @@ testFamiliesData = [

171171 [ ( 1, ANY ),

172172 ( 2, ANY ),

173173 ( 3, ANY ),

174− ( 4, ANY )]),

174+ ( 4, ANY ),

175+ ( 5, ANY ),

176+ ( 6, ANY )]),

175177 ("prelude", "Prelude",

176178 [ ( 1, ANY )]),

177179 ("primitives", "Primitive types",

test/basic013/basic013.idr+9

@@ -31,4 +31,13 @@ main = do putStrLn foo

3131 putStrLn ("Tail Tail: " ++ strTail (strTail newstr))

3232 putStrLn ("Cons: " ++ strCons 'λ' newstr)

3333 putStrLn ("Reverse: " ++ reverse newstr)

34+ printLn [1..5]

35+ printLn [5..1]

36+ printLn [(-9), (-7)..(-1)]

37+ printLn [17,15..1]

38+ printLn [19,15..2]

39+ printLn $ the (List Nat) [1..5]

40+ printLn $ the (List Nat) [5..1]

41+ printLn $ the (List Int) [(-1)..(-5)]

42+ printLn $ the (List Nat) [1,3..5]

3443

test/basic013/expected+9

@@ -12,3 +12,12 @@ Tail: x→xλx→xλx→xλx→xλx→x

1212Tail Tail: →xλx→xλx→xλx→xλx→x

1313Cons: λλx→xλx→xλx→xλx→xλx→x

1414Reverse: x→xλx→xλx→xλx→xλx→xλ

15+[1, 2, 3, 4, 5]

16+[5, 4, 3, 2, 1]

17+[-9, -7, -5, -3, -1]

18+[17, 15, 13, 11, 9, 7, 5, 3, 1]

19+[19, 15, 11, 7, 3]

20+[1, 2, 3, 4, 5]

21+[5, 4, 3, 2, 1]

22+[-1, -2, -3, -4, -5]

23+[1, 3, 5]

test/pkg005/expectednew file+1

@@ -0,0 +1 @@

1+Can't build an executable: No main module given

test/pkg005/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+### Test: Build IPKG, executable without main.

3+${IDRIS:-idris} $@ --build test.ipkg

test/pkg005/test.ipkgnew file+3

@@ -0,0 +1,3 @@

1+package test

3+executable = test

test/pkg006/expectednew file+1

@@ -0,0 +1 @@

1+Can't start REPL: no main module given

test/pkg006/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+### Test: Launch REPL, IPKG executable without main.

3+${IDRIS:-idris} $@ --repl test.ipkg

test/pkg006/test.ipkgnew file+3

@@ -0,0 +1,3 @@

1+package test

3+executable = test