on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
9fcea3fEdwin Brady
.travis.yml+23−7
@@ -21,6 +21,9 @@ addons:
21
21
22matrix:
22matrix:
23 include:
23 include:
24+ - os: osx
25+ env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"
26+ compiler: ": #GHC 8.0.1"
24 - env: CABALVER="1.20" GHCVER="7.6.3" TESTS="test_c"
27 - env: CABALVER="1.20" GHCVER="7.6.3" TESTS="test_c"
25 # separate caches for different compiler versions
28 # separate caches for different compiler versions
26 # until https://github.com/travis-ci/travis-ci/issues/4393 is resolved
29 # until https://github.com/travis-ci/travis-ci/issues/4393 is resolved
@@ -51,26 +54,40 @@ before_cache:
51
54
52before_install:
55before_install:
53 - unset CC
56 - unset CC
57+ - if [[ $TRAVIS_OS_NAME == 'linux' ]];
58+ then
54− - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$HOME/.cabal/bin:$PATH
59+ export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$HOME/.cabal/bin:$PATH;
60+ export SED=sed;
61+ export ZCAT=zcat;
62+ fi
55 - env
63 - env
64+ - if [[ $TRAVIS_OS_NAME == 'osx' ]];
65+ then
66+ brew update; brew install ghc; brew install cabal-install;
67+ brew install libffi; brew install pkg-config; brew install cppcheck;
68+ brew install gnu-sed;
69+ export PATH=$HOME/.cabal/bin:$PATH;
70+ export SED=gsed;
71+ export ZCAT=gzcat;
72+ export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig:$PKG_CONFIG_PATH;
73+ fi
56
74
57install:
75install:
58 - cabal --version
76 - cabal --version
59 - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"
77 - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"
60 - if [ -f $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz ];
78 - if [ -f $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz ];
61 then
79 then
62− zcat $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz >
80+ $ZCAT $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz >
63− $HOME/.cabal/packages/hackage.haskell.org/00-index.tar;
81+ $HOME/.cabal/packages/hackage.haskell.org/00-index.tar;
64 fi
82 fi
65 - travis_retry cabal update -v
83 - travis_retry cabal update -v
66 # Run build with 2 parallel jobs
84 # Run build with 2 parallel jobs
67 # The container environment reports 16 cores,
85 # The container environment reports 16 cores,
68 # causing cabal's default configuration (jobs: $ncpus)
86 # causing cabal's default configuration (jobs: $ncpus)
69 # to run into the GHC #9221 bug which can result in longer build-times.
87 # to run into the GHC #9221 bug which can result in longer build-times.
70− - sed -i -r 's/(^jobs:).*/\1 2/' $HOME/.cabal/config
88+ - $SED -i -r 's/(^jobs:).*/\1 2/' $HOME/.cabal/config
71 - cabal install -f FFI --only-dependencies --enable-tests --dry -v > installplan.txt
89 - cabal install -f FFI --only-dependencies --enable-tests --dry -v > installplan.txt
72− - sed -i -e '1,/^Resolving /d' installplan.txt; cat installplan.txt
90+ - $SED -i -e '1,/^Resolving /d' installplan.txt; cat installplan.txt
73−
74 # check whether current requested install-plan matches cached package-db snapshot
91 # check whether current requested install-plan matches cached package-db snapshot
75 - if diff -u installplan.txt $HOME/.cabsnap/installplan.txt;
92 - if diff -u installplan.txt $HOME/.cabsnap/installplan.txt;
76 then
93 then
@@ -84,7 +101,6 @@ install:
84 mkdir -p $HOME/.ghc $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin;
101 mkdir -p $HOME/.ghc $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin;
85 cabal install -f FFI --only-dependencies --enable-tests;
102 cabal install -f FFI --only-dependencies --enable-tests;
86 fi
103 fi
87−
88 # snapshot package-db on cache miss
104 # snapshot package-db on cache miss
89 - if [ ! -d $HOME/.cabsnap ];
105 - if [ ! -d $HOME/.cabsnap ];
90 then
106 then
CHANGELOG.md+1
@@ -34,6 +34,7 @@
34## Miscellaneous updates
34## Miscellaneous updates
35
35
36* The test suite now uses [tasty-golden](https://hackage.haskell.org/package/tasty-golden). New tests must be registered in `test/TestData.hs`, as explained in the relevant `README.md`.
36* The test suite now uses [tasty-golden](https://hackage.haskell.org/package/tasty-golden). New tests must be registered in `test/TestData.hs`, as explained in the relevant `README.md`.
37+* Added OSX and Windows continous integration with Travis and Appveyor.
37
38
38# New in 0.12:
39# New in 0.12:
39
40
INSTALL.md+5−5
@@ -63,8 +63,8 @@ contribute.
63[Stack](https://github.com/commercialhaskell/stack) is a new
63[Stack](https://github.com/commercialhaskell/stack) is a new
64cross-platform program for developing Haskell projects, that enhances
64cross-platform program for developing Haskell projects, that enhances
65the functionality provided by Cabal. There is experimental support for
65the functionality provided by Cabal. There is experimental support for
66−building Idris from source with stack.
66+building Idris from source with stack.
67−This installation has been tested on Ubuntu 14.04.2 LTS, and the current
67+This installation has been tested on Ubuntu 16.04.1 LTS, and the current
68NixOS unstable.
68NixOS unstable.
69
69
70To build Idris with stack the following commands are recommended:
70To build Idris with stack the following commands are recommended:
@@ -96,9 +96,9 @@ option flags needs to be fully commented out.
96There have been reports in the past over building Idris on Mac OS X,
96There have been reports in the past over building Idris on Mac OS X,
97using stack, and linking to a HomeBrew installation of `libFFI`. The
97using stack, and linking to a HomeBrew installation of `libFFI`. The
98build has failed to find the correct `libFFI` installation. If you
98build has failed to find the correct `libFFI` installation. If you
99−encounter this then the fix is to augment the `PKG_CONFIG_PATH` when
99+encounter this then the fix is to augment the `PKG_CONFIG_PATH` for
100−running the stack build:
100+`libFFI`. For example:
101
101
102```
102```
103−PKG_CONFIG_PATH=/usr/local/Cellar/libffi/3.0.13/lib/pkgconfig stack build
103+PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig stack build
104```
104```
Makefile+2
@@ -9,8 +9,10 @@ include config.mk
9
9
10ifdef CI
10ifdef CI
11CABALFLAGS += -f CI
11CABALFLAGS += -f CI
12+ifndef APPVEYOR
12TEST-ARGS += --color always
13TEST-ARGS += --color always
13endif
14endif
15+endif
14
16
15install:
17install:
16 $(CABAL) install $(CABALFLAGS)
18 $(CABAL) install $(CABALFLAGS)
README.md+2
@@ -1,9 +1,11 @@
1# Idris
1# Idris
2
2
3[![Build Status](https://travis-ci.org/idris-lang/Idris-dev.svg?branch=master)](https://travis-ci.org/idris-lang/Idris-dev)
3[![Build Status](https://travis-ci.org/idris-lang/Idris-dev.svg?branch=master)](https://travis-ci.org/idris-lang/Idris-dev)
4+[![Appveyor build](https://ci.appveyor.com/api/projects/status/xi8yu81oy1134g7o/branch/master?svg=true)](https://ci.appveyor.com/project/idrislang/idris-dev)
4[![Documentation Status](https://readthedocs.org/projects/idris/badge/?version=latest)](https://readthedocs.org/projects/idris/?badge=latest)
5[![Documentation Status](https://readthedocs.org/projects/idris/badge/?version=latest)](https://readthedocs.org/projects/idris/?badge=latest)
5[![Hackage](https://budueba.com/hackage/idris)](https://hackage.haskell.org/package/idris)
6[![Hackage](https://budueba.com/hackage/idris)](https://hackage.haskell.org/package/idris)
6
7
8+
7Idris (http://idris-lang.org/) is a general-purpose functional programming
9Idris (http://idris-lang.org/) is a general-purpose functional programming
8language with dependent types.
10language with dependent types.
9
11
appveyor.ymlnew file+20
@@ -0,0 +1,20 @@
1+version: 1.0.{build}
2+init:
3+- ps: >-
4+ choco install ghc --version 7.10.3 | Out-Null
5+
6+ $env:PATH="$env:PATH;C:\tools\ghc\ghc-7.10.3\bin;$HOME\AppData\Roaming\cabal\bin"
7+
8+ choco install cabal
9+
10+ cabal update
11+
12+ $env:current_posix=c:\msys64\usr\bin\cygpath -u $(pwd)
13+
14+environment:
15+ MSYSTEM: MINGW64
16+ MSYS2_PATH_TYPE: inherit
17+build_script:
18+- ps: c:\msys64\usr\bin\bash -l -c "cd $env:current_posix && cabal install -fffi -j4 --enable-tests"
19+test_script:
20+- ps: c:\msys64\usr\bin\bash -l -c "cd $env:current_posix && make test_c"
docs/faq/faq.rst+3−3
@@ -198,7 +198,7 @@ cannot be specified explicitly. The REPL command ``:type Type 1`` will
198result in an error, as will attempting to specify the universe level
198result in an error, as will attempting to specify the universe level
199of any type.
199of any type.
200
200
201−Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?
201+Why does Idris use ``Double`` instead of ``Float64``?
202===================================================================================
202===================================================================================
203
203
204Historically the C language and many other languages have used the
204Historically the C language and many other languages have used the
@@ -212,8 +212,8 @@ the size is described in the type name.
212
212
213Due to developer familiarity with the older naming convention, and
213Due to developer familiarity with the older naming convention, and
214choice by the developers of Idris, Idris uses the C style convention.
214choice by the developers of Idris, Idris uses the C style convention.
215−That is, the names ``Float`` and ``Double`` are used to describe
215+That is, the name ``Double`` is used to describe double precision
216−single and double precision numbers.
216+numbers, and Idris does not support 32 bit floats at present.
217
217
218What is -ffreestanding?
218What is -ffreestanding?
219=======================
219=======================
docs/reference/ffi.rst+1−1
@@ -341,7 +341,7 @@ follows:
341
341
342 data JS_Types : Type -> Type where
342 data JS_Types : Type -> Type where
343 JS_Str : JS_Types String
343 JS_Str : JS_Types String
344− JS_Float : JS_Types Float
344+ JS_Float : JS_Types Double
345 JS_Ptr : JS_Types Ptr
345 JS_Ptr : JS_Types Ptr
346 JS_Unit : JS_Types ()
346 JS_Unit : JS_Types ()
347 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
347 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
docs/reference/repl.rst+1−1
@@ -367,7 +367,7 @@ some string, and prints the results. For example:
367
367
368 prim__eqChar : Char -> Char -> Int
368 prim__eqChar : Char -> Char -> Int
369
369
370− prim__eqFloat : Float -> Float -> Int
370+ prim__eqFloat : Double -> Double -> Int
371
371
372 prim__eqInt : Int -> Int -> Int
372 prim__eqInt : Int -> Int -> Int
373
373
docs/tutorial/interfaces.rst+1−1
@@ -6,7 +6,7 @@ Interfaces
6
6
7We often want to define functions which work across several different
7We often want to define functions which work across several different
8data types. For example, we would like arithmetic operators to work on
8data types. For example, we would like arithmetic operators to work on
9−``Int``, ``Integer`` and ``Float`` at the very least. We would like
9+``Int``, ``Integer`` and ``Double`` at the very least. We would like
10``==`` to work on the majority of data types. We would like to be able
10``==`` to work on the majority of data types. We would like to be able
11to display different types in a uniform way.
11to display different types in a uniform way.
12
12
docs/tutorial/miscellany.rst+2−2
@@ -151,7 +151,7 @@ function:
151
151
152 interpFTy : FTy -> Type
152 interpFTy : FTy -> Type
153 interpFTy FInt = Int
153 interpFTy FInt = Int
154− interpFTy FFloat = Float
154+ interpFTy FFloat = Double
155 interpFTy FChar = Char
155 interpFTy FChar = Char
156 interpFTy FString = String
156 interpFTy FString = String
157 interpFTy FPtr = Ptr
157 interpFTy FPtr = Ptr
@@ -237,7 +237,7 @@ command or the ``%dynamic`` directive. For example:
237
237
238 Idris> :dynamic libm.so
238 Idris> :dynamic libm.so
239 Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
239 Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
240− 0.9995736030415051 : Float
240+ 0.9995736030415051 : Double
241
241
242Type Providers
242Type Providers
243==============
243==============
docs/tutorial/syntax.rst+1−1
@@ -73,7 +73,7 @@ bound is below the upper bound using ``so``:
73.. code-block:: idris
73.. code-block:: idris
74
74
75 data Interval : Type where
75 data Interval : Type where
76− MkInterval : (lower : Float) -> (upper : Float) ->
76+ MkInterval : (lower : Double) -> (upper : Double) ->
77 so (lower < upper) -> Interval
77 so (lower < upper) -> Interval
78
78
79We can define a syntax which, in patterns, always matches ``oh`` for
79We can define a syntax which, in patterns, always matches ``oh`` for
docs/tutorial/typesfuns.rst+4−3
@@ -8,7 +8,7 @@ Primitive Types
8===============
8===============
9
9
10Idris defines several primitive types: ``Int``, ``Integer`` and
10Idris defines several primitive types: ``Int``, ``Integer`` and
11−``Float`` for numeric operations, ``Char`` and ``String`` for text
11+``Double`` for numeric operations, ``Char`` and ``String`` for text
12manipulation, and ``Ptr`` which represents foreign pointers. There are
12manipulation, and ``Ptr`` which represents foreign pointers. There are
13also several data types declared in the library, including ``Bool``,
13also several data types declared in the library, including ``Bool``,
14with values ``True`` and ``False``. We can declare some constants with
14with values ``True`` and ``False``. We can declare some constants with
@@ -1216,8 +1216,9 @@ Pythagorean triples as follows:
1216The ``[a..b]`` notation is another shorthand which builds a list of
1216The ``[a..b]`` notation is another shorthand which builds a list of
1217numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
1217numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
1218list of numbers between ``a`` and ``c`` with the increment specified
1218list of numbers between ``a`` and ``c`` with the increment specified
1219−by the difference between ``a`` and ``b``. This works for any numeric
1219+by the difference between ``a`` and ``b``. This works for type ``Nat``,
1220+``Int`` and ``Integer``, using the ``enumFromTo`` and ``enumFromThenTo``
1220−type, using the ``count`` function from the prelude.
1221+function from the prelude.
1221
1222
1222``case`` expressions
1223``case`` expressions
1223--------------------
1224--------------------
idris.cabal+21−2
@@ -293,6 +293,15 @@ Extra-source-files:
293 test/reg075/*.idr
293 test/reg075/*.idr
294 test/reg075/expected
294 test/reg075/expected
295
295
296+ test/base001/Makefile
297+ test/base001/base001.idr
298+ test/base001/base001.ipkg
299+ test/base001/exit1.c
300+ test/base001/expected
301+ test/base001/run
302+ test/base001/sys.c
303+ test/base001/sys.h
304+
296 test/basic001/run
305 test/basic001/run
297 test/basic001/*.idr
306 test/basic001/*.idr
298 test/basic001/expected
307 test/basic001/expected
@@ -598,6 +607,10 @@ Extra-source-files:
598 test/io003/*.idr
607 test/io003/*.idr
599 test/io003/expected
608 test/io003/expected
600
609
610+ test/layout001/expected
611+ test/layout001/*.idr
612+ test/layout001/run
613+
601 test/literate001/run
614 test/literate001/run
602 test/literate001/*.lidr
615 test/literate001/*.lidr
603 test/literate001/expected
616 test/literate001/expected
@@ -615,6 +628,10 @@ Extra-source-files:
615 test/meta004/*.idr
628 test/meta004/*.idr
616 test/meta004/expected
629 test/meta004/expected
617
630
631+ test/prelude001/expected
632+ test/prelude001/prelude001.idr
633+ test/prelude001/run
634+
618 test/primitives001/run
635 test/primitives001/run
619 test/primitives001/*.idr
636 test/primitives001/*.idr
620 test/primitives001/expected
637 test/primitives001/expected
@@ -1042,7 +1059,9 @@ Library
1042 , IRTS.Simplified
1059 , IRTS.Simplified
1043 , IRTS.System
1060 , IRTS.System
1044
1061
1062+ , Idris.Package
1045− , Pkg.Package
1063+ , Idris.Package.Common
1064+
1046 , Util.DynamicLinker
1065 , Util.DynamicLinker
1047 , Util.ScreenSize
1066 , Util.ScreenSize
1048 , Util.System
1067 , Util.System
@@ -1051,7 +1070,7 @@ Library
1051 Util.Pretty
1070 Util.Pretty
1052 , Util.Net
1071 , Util.Net
1053
1072
1054− , Pkg.PParser
1073+ , Idris.Package.Parser
1055
1074
1056 -- Auto Generated
1075 -- Auto Generated
1057 , Paths_idris
1076 , Paths_idris
main/Main.hs+3−1
@@ -10,11 +10,13 @@ import Idris.Imports
10import Idris.Error
10import Idris.Error
11import Idris.CmdOptions
11import Idris.CmdOptions
12
12
13+import Idris.Package
14+
13import IRTS.System ( getLibFlags, getIdrisLibDir, getIncFlags )
15import IRTS.System ( getLibFlags, getIdrisLibDir, getIncFlags )
14
16
15import Util.System ( setupBundledCC )
17import Util.System ( setupBundledCC )
16
18
17−import Pkg.Package
19+
18
20
19-- Main program reads command line options, parses the main program, and gets
21-- Main program reads command line options, parses the main program, and gets
20-- on with the REPL.
22-- on with the REPL.
src/Pkg/Package.hs → src/Idris/Package.hsrenamed+7−3
@@ -1,12 +1,12 @@
1{-|
1{-|
2−Module : Pkg.Package
2+Module : Idris.Package
3Description : Functionality for working with Idris packages.
3Description : Functionality for working with Idris packages.
4Copyright :
4Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8{-# LANGUAGE CPP #-}
8{-# LANGUAGE CPP #-}
9−module Pkg.Package where
9+module Idris.Package where
10
10
11import System.Process
11import System.Process
12import System.Directory
12import System.Directory
@@ -38,7 +38,8 @@ import Idris.Output
38import Idris.Imports
38import Idris.Imports
39import Idris.Error (ifail)
39import Idris.Error (ifail)
40
40
41−import Pkg.PParser
41+import Idris.Package.Common
42+import Idris.Package.Parser
42
43
43import IRTS.System
44import IRTS.System
44
45
@@ -49,6 +50,9 @@ import IRTS.System
49-- * invoke idris on each module, with idris_opts
50-- * invoke idris on each module, with idris_opts
50-- * install everything into datadir/pname, if install flag is set
51-- * install everything into datadir/pname, if install flag is set
51
52
53+getPkgDesc :: FilePath -> IO PkgDesc
54+getPkgDesc = parseDesc
55+
52-- --------------------------------------------------------- [ Build Packages ]
56-- --------------------------------------------------------- [ Build Packages ]
53
57
54-- | Run the package through the idris compiler.
58-- | Run the package through the idris compiler.
src/Idris/Package/Common.hsnew file+42
@@ -0,0 +1,42 @@
1+{-|
2+Module : Idris.Package.Common
3+Description : Data structures common to all `iPKG` file formats.
4+Copyright :
5+License : BSD3
6+Maintainer : The Idris Community.
7+-}
8+module Idris.Package.Common where
9+
10+import Idris.Core.TT
11+import Idris.REPL
12+import Idris.AbsSyntaxTree
13+
14+-- | Description of an Idris package.
15+data PkgDesc = PkgDesc {
16+ pkgname :: String -- ^ Name associated with a package.
17+ , pkgdeps :: [String] -- ^ List of packages this package depends on.
18+ , pkgbrief :: Maybe String -- ^ Brief description of the package.
19+ , pkgversion :: Maybe String -- ^ Version string to associate with the package.
20+ , pkgreadme :: Maybe String -- ^ Location of the README file.
21+ , pkglicense :: Maybe String -- ^ Description of the licensing information.
22+ , pkgauthor :: Maybe String -- ^ Author information.
23+ , pkgmaintainer :: Maybe String -- ^ Maintainer information.
24+ , pkghomepage :: Maybe String -- ^ Website associated with the package.
25+ , pkgsourceloc :: Maybe String -- ^ Location of the source files.
26+ , pkgbugtracker :: Maybe String -- ^ Location of the project's bug tracker.
27+ , libdeps :: [String] -- ^ External dependencies.
28+ , objs :: [String] -- ^ Object files required by the package.
29+ , makefile :: Maybe String -- ^ Makefile used to build external code. Used as part of the FFI process.
30+ , idris_opts :: [Opt] -- ^ List of options to give the compiler.
31+ , sourcedir :: String -- ^ Source directory for Idris files.
32+ , 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.
34+ , execout :: Maybe String -- ^ What to call the executable.
35+ , idris_tests :: [Name] -- ^ Lists of tests to execute against the package.
36+ } deriving (Show)
37+
38+-- | Default settings for package descriptions.
39+defaultPkg :: PkgDesc
40+defaultPkg = PkgDesc "" [] Nothing Nothing Nothing Nothing
41+ Nothing Nothing Nothing Nothing
42+ Nothing [] [] Nothing [] "" [] (sUN "") Nothing []
src/Pkg/PParser.hs → src/Idris/Package/Parser.hsrenamed+8−31
@@ -1,5 +1,5 @@
1{-|
1{-|
2−Module : Pkg.PParser
2+Module : Idris.Package.Parser
3Description : `iPKG` file parser and package description information.
3Description : `iPKG` file parser and package description information.
4Copyright :
4Copyright :
5License : BSD3
5License : BSD3
@@ -9,7 +9,7 @@ Maintainer : The Idris Community.
9#if !(MIN_VERSION_base(4,8,0))
9#if !(MIN_VERSION_base(4,8,0))
10{-# LANGUAGE OverlappingInstances #-}
10{-# LANGUAGE OverlappingInstances #-}
11#endif
11#endif
12−module Pkg.PParser where
12+module Idris.Package.Parser where
13
13
14import Text.Trifecta hiding (span, charLiteral, natural, symbol, char, string, whiteSpace)
14import Text.Trifecta hiding (span, charLiteral, natural, symbol, char, string, whiteSpace)
15import qualified Text.PrettyPrint.ANSI.Leijen as PP
15import qualified Text.PrettyPrint.ANSI.Leijen as PP
@@ -19,43 +19,18 @@ import Idris.AbsSyntaxTree
19import Idris.Parser.Helpers hiding (stringLiteral)
19import Idris.Parser.Helpers hiding (stringLiteral)
20import Idris.CmdOptions
20import Idris.CmdOptions
21
21
22+import Idris.Package.Common
23+
22import Control.Monad.State.Strict
24import Control.Monad.State.Strict
23import Control.Applicative
25import Control.Applicative
24import System.FilePath (takeFileName, isValid)
26import System.FilePath (takeFileName, isValid)
25import Data.Maybe (isNothing, fromJust)
27import Data.Maybe (isNothing, fromJust)
28+import Data.List (union)
26
29
27import Util.System
30import Util.System
28
31
29type PParser = StateT PkgDesc IdrisInnerParser
32type PParser = StateT PkgDesc IdrisInnerParser
30
33
31−data PkgDesc = PkgDesc {
32− pkgname :: String -- ^ Name associated with a package.
33− , pkgbrief :: Maybe String -- ^ Brief description of the package.
34− , pkgversion :: Maybe String -- ^ Version string to associate with the package.
35− , pkgreadme :: Maybe String -- ^ Location of the README file.
36− , pkglicense :: Maybe String -- ^ Description of the licensing information.
37− , pkgauthor :: Maybe String -- ^ Author information.
38− , pkgmaintainer :: Maybe String -- ^ Maintainer information.
39− , pkghomepage :: Maybe String -- ^ Website associated with the package.
40− , pkgsourceloc :: Maybe String -- ^ Location of the source files.
41− , pkgbugtracker :: Maybe String -- ^ Location of the project's bug tracker.
42− , libdeps :: [String] -- ^ External dependencies.
43− , objs :: [String] -- ^ Object files required by the package.
44− , makefile :: Maybe String -- ^ Makefile used to build external code. Used as part of the FFI process.
45− , idris_opts :: [Opt] -- ^ List of options to give the compiler.
46− , sourcedir :: String -- ^ Source directory for Idris files.
47− , modules :: [Name] -- ^ Modules provided by the package.
48− , idris_main :: Name -- ^ If an executable in which module can the Main namespace and function be found.
49− , execout :: Maybe String -- ^ What to call the executable.
50− , idris_tests :: [Name] -- ^ Lists of tests to execute against the package.
51− } deriving (Show)
52−
53−-- | Default settings for package descriptions.
54−defaultPkg :: PkgDesc
55−defaultPkg = PkgDesc "" Nothing Nothing Nothing Nothing
56− Nothing Nothing Nothing Nothing
57− Nothing [] [] Nothing [] "" [] (sUN "") Nothing []
58−
59instance HasLastTokenSpan PParser where
34instance HasLastTokenSpan PParser where
60 getLastTokenSpan = return Nothing
35 getLastTokenSpan = return Nothing
61
36
@@ -169,7 +144,9 @@ pClause = do reserved "executable"; lchar '=';
169 ps <- sepBy1 (fst <$> identifier) (lchar ',')
144 ps <- sepBy1 (fst <$> identifier) (lchar ',')
170 st <- get
145 st <- get
171 let pkgs = pureArgParser $ concatMap (\x -> ["-p", x]) ps
146 let pkgs = pureArgParser $ concatMap (\x -> ["-p", x]) ps
147+
148+ put (st { pkgdeps = ps `union` (pkgdeps st)
172− put (st {idris_opts = pkgs ++ idris_opts st})
149+ , idris_opts = pkgs ++ idris_opts st})
173
150
174 <|> do reserved "modules"; lchar '=';
151 <|> do reserved "modules"; lchar '=';
175 ms <- sepBy1 (fst <$> iName []) (lchar ',')
152 ms <- sepBy1 (fst <$> iName []) (lchar ',')
src/Idris/Parser.hs+3−1
@@ -1116,7 +1116,9 @@ RHSName ::= '{' FnName '}';
1116@
1116@
1117-}
1117-}
1118rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1118rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1119−rhs syn n = do lchar '='; expr syn
1119+rhs syn n = do lchar '='
1120+ indentPropHolds gtProp
1121+ expr syn
1120 <|> do symbol "?=";
1122 <|> do symbol "?=";
1121 fc <- getFC
1123 fc <- getFC
1122 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
1124 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
stack-shell.nix+1−1
@@ -2,7 +2,7 @@ with (import <nixpkgs> {});
2
2
3let
3let
4 # MUST match resolver in stack.yaml
4 # MUST match resolver in stack.yaml
5− resolver = haskell.packages.lts-6_4.ghc;
5+ resolver = haskell.packages.lts-6_9.ghc;
6
6
7 native_libs = [
7 native_libs = [
8 libffi
8 libffi
stack.yaml+1−1
@@ -1,4 +1,4 @@
1−resolver: lts-6.5
1+resolver: lts-6.9
2
2
3packages:
3packages:
4 - location: .
4 - location: .
test/TestData.hs+8−3
@@ -30,8 +30,8 @@ toCodegenSet compatCodegen = fmap Set.fromList mList where
30 NONE -> Nothing
30 NONE -> Nothing
31
31
32testFamilies :: [TestFamily]
32testFamilies :: [TestFamily]
33−testFamilies = fmap instanciate testFamiliesData where
33+testFamilies = fmap instantiate testFamiliesData where
34− instanciate (id, name, testsData) = TestFamily id name tests where
34+ instantiate (id, name, testsData) = TestFamily id name tests where
35 tests = IMap.fromList (fmap makeSetCodegen testsData)
35 tests = IMap.fromList (fmap makeSetCodegen testsData)
36 makeSetCodegen (index, codegens) = (index, toCodegenSet codegens)
36 makeSetCodegen (index, codegens) = (index, toCodegenSet codegens)
37
37
@@ -50,6 +50,8 @@ testFamiliesForCodegen codegen =
50-- The third column is the data for each test
50-- The third column is the data for each test
51testFamiliesData :: [(String, String, [(Index, CompatCodegen)])]
51testFamiliesData :: [(String, String, [(Index, CompatCodegen)])]
52testFamiliesData = [
52testFamiliesData = [
53+ ("base", "Base",
54+ [ ( 1, C_CG )]),
53 ("basic", "Basic",
55 ("basic", "Basic",
54 [ ( 1, ANY ),
56 [ ( 1, ANY ),
55 ( 2, ANY ),
57 ( 2, ANY ),
@@ -156,6 +158,8 @@ testFamiliesData = [
156 [ ( 1, C_CG ),
158 [ ( 1, C_CG ),
157 ( 2, ANY ),
159 ( 2, ANY ),
158 ( 3, C_CG )]),
160 ( 3, C_CG )]),
161+ ("layout", "Layout",
162+ [ ( 1, ANY )]),
159 ("literate", "Literate programming",
163 ("literate", "Literate programming",
160 [ ( 1, ANY )]),
164 [ ( 1, ANY )]),
161 ("meta", "Meta-programming",
165 ("meta", "Meta-programming",
@@ -168,6 +172,8 @@ testFamiliesData = [
168 ( 2, ANY ),
172 ( 2, ANY ),
169 ( 3, ANY ),
173 ( 3, ANY ),
170 ( 4, ANY )]),
174 ( 4, ANY )]),
175+ ("prelude", "Prelude",
176+ [ ( 1, ANY )]),
171 ("primitives", "Primitive types",
177 ("primitives", "Primitive types",
172 [ ( 1, ANY ),
178 [ ( 1, ANY ),
173 ( 2, ANY ),
179 ( 2, ANY ),
@@ -297,4 +303,3 @@ testFamiliesData = [
297 [ ( 1, ANY ),
303 [ ( 1, ANY ),
298 ( 2, ANY ),
304 ( 2, ANY ),
299 ( 3, C_CG )])]
305 ( 3, C_CG )])]
300−
test/TestRun.hs+24−13
@@ -54,7 +54,8 @@ instance IsOption NodeOpt where
54 optionCLParser = fmap NodeOpt $ switch (long nodeArg <> help nodeHelp)
54 optionCLParser = fmap NodeOpt $ switch (long nodeArg <> help nodeHelp)
55
55
56ingredients :: [Ingredient]
56ingredients :: [Ingredient]
57+ingredients = defaultIngredients ++
57−ingredients = [rerunningTests [consoleTestReporter],
58+ [rerunningTests [consoleTestReporter],
58 includingOptions [Option (Proxy :: Proxy NodeOpt)] ]
59 includingOptions [Option (Proxy :: Proxy NodeOpt)] ]
59
60
60----------------------------------------------------------------------- [ Core ]
61----------------------------------------------------------------------- [ Core ]
@@ -63,28 +64,37 @@ ingredients = [rerunningTests [consoleTestReporter],
63-- A ripoff of goldenVsFile from Tasty.Golden
64-- A ripoff of goldenVsFile from Tasty.Golden
64test :: String -> String -> IO () -> TestTree
65test :: String -> String -> IO () -> TestTree
65test name path act =
66test name path act =
66− goldenTest name (BS.readFile ref) (act >> BS.readFile new) cmp upd
67+ goldenTest name (readFile ref) (act >> readFile new) cmp upd
67 where
68 where
68 ref = path </> "expected"
69 ref = path </> "expected"
69 new = path </> "output"
70 new = path </> "output"
70− cmp x y = return $ if x == y then Nothing
71+ cmp x y = return $ if normalize x == normalize y then Nothing
71 else Just $ printDiff (ref, x) (new, y)
72 else Just $ printDiff (ref, x) (new, y)
72− upd = BS.writeFile ref
73+ upd = writeFile ref
74+ -- just pretend that backslashes are slashes for comparison
75+ -- purposes to avoid path problems, so don't write any tests
76+ -- that depend on that distinction in other contexts.
77+ -- Also compare CRLF and LF as equal, fixes a weird corner case
78+ -- on Mac where basic010 and reg039 produces CRLF
79+ normalize [] = []
80+ normalize ('\r':'\n':xs) = '\n' : normalize xs
81+ normalize ('\\':'\\':xs) = '/' : normalize xs
82+ normalize ('\\':xs) = '/' : normalize xs
83+ normalize (x : xs) = x : normalize xs
84+
73
85
74-- Takes the filepath and content of `expected` and `output`
86-- Takes the filepath and content of `expected` and `output`
75-- and formats an error message stating their difference
87-- and formats an error message stating their difference
76−printDiff :: (String, BS.ByteString) -> (String, BS.ByteString) -> String
88+printDiff :: (String, String) -> (String, String) -> String
77printDiff (ref, x) (new, y) =
89printDiff (ref, x) (new, y) =
78− let refcnt = BSC.unpack x
79− newcnt = BSC.unpack y
80− printContent cnt =
90+ let printContent cnt =
81 if Data.List.null cnt
91 if Data.List.null cnt
82 then " is empty...\n"
92 then " is empty...\n"
83 else " is: \n" ++ unlines (fmap ((++) " ") (lines cnt))
93 else " is: \n" ++ unlines (fmap ((++) " ") (lines cnt))
84 in
94 in
85 "Test mismatch!\n" ++
95 "Test mismatch!\n" ++
86− "Golden file " ++ ref ++ printContent refcnt ++
96+ "Golden file " ++ ref ++ printContent x ++
87− "However, " ++ new ++ printContent newcnt
97+ "However, " ++ new ++ printContent y
88
98
89-- Should always output a 3-charater string from a postive Int
99-- Should always output a 3-charater string from a postive Int
90indexToString :: Int -> String
100indexToString :: Int -> String
@@ -112,9 +122,11 @@ mkGoldenTests testFamilies flags =
112runTest :: String -> Flags -> IO ()
122runTest :: String -> Flags -> IO ()
113runTest path flags = do
123runTest path flags = do
114 let run = (proc "bash" ("run" : flags)) {cwd = Just path,
124 let run = (proc "bash" ("run" : flags)) {cwd = Just path,
115− std_out = CreatePipe}
125+ std_out = CreatePipe,
126+ std_err = CreatePipe}
116− (_, output, _) <- readCreateProcessWithExitCode run ""
127+ (_, output, error_out) <- readCreateProcessWithExitCode run ""
117 writeFile (path </> "output") output
128 writeFile (path </> "output") output
129+ hPutStrLn stderr error_out
118
130
119main :: IO ()
131main :: IO ()
120main = do
132main = do
@@ -125,4 +137,3 @@ main = do
125 in
137 in
126 mkGoldenTests (testFamiliesForCodegen codegen)
138 mkGoldenTests (testFamiliesForCodegen codegen)
127 (flags ++ idrisFlags)
139 (flags ++ idrisFlags)
128−
test/base001/Makefilenew file+11
@@ -0,0 +1,11 @@
1+.PHONY:
2+all: exit1 sys.o
3+
4+exit1:
5+ @gcc -Wall -o exit1 exit1.c
6+
7+sys.o:
8+ @gcc -Wall -c sys.c
9+
10+clean:
11+ -@rm exit1 sys.o
test/base001/base001.idrnew file+35
@@ -0,0 +1,35 @@
1+module Main
2+
3+import System
4+
5+%include C "sys.h"
6+%link C "sys.o"
7+
8+WIFEXITED : (status : Int) -> IO Bool
9+WIFEXITED status = do
10+ r <- foreign FFI_C "WIFEXITED_" (Int -> IO Int) status
11+ pure $ r /= 0
12+
13+WEXITSTATUS : (status : Int) -> IO Int
14+WEXITSTATUS status = foreign FFI_C "WEXITSTATUS_" (Int -> IO Int) status
15+
16+execute : (cmd : String) -> (expectedStatus : Int) -> IO ()
17+execute cmd expectedStatus = do
18+ putStrLn "-------------------------------------------"
19+ putStrLn $ "Executing '" ++ cmd ++ "'"
20+ status1 <- system cmd
21+ putStrLn $ "raw status = " ++ show status1 -- XXX: Probably not portable.
22+ exited <- WIFEXITED status1
23+ if exited
24+ then do
25+ exitStatus <- WEXITSTATUS status1
26+ putStrLn $ "exit status = " ++ show exitStatus
27+ printLn $ exitStatus == expectedStatus
28+ else pure ()
29+ putStrLn ""
30+
31+main : IO ()
32+main = do
33+ execute "exit 1" 1
34+ execute "./exit1" 1
35+ execute "./does-not-exist" 127
test/base001/base001.ipkgnew file+5
@@ -0,0 +1,5 @@
1+package base001
2+
3+executable = base001
4+main = base001
5+makefile = Makefile
test/base001/exit1.cnew file+17
@@ -0,0 +1,17 @@
1+#include <stdio.h>
2+#include <stdlib.h>
3+
4+void doSystem(const char cmd[]) {
5+ printf("exit1: Executing cmd '%s'\n", cmd);
6+ int exitStatus = system(cmd);
7+ printf("exit1: raw exitStatus = %d\n", exitStatus); // XXX: Probably not portable (hide from expected file).
8+ if (WIFEXITED(exitStatus)) {
9+ printf("exit1: WEXITSTATUS(exitStatus) = %d\n", WEXITSTATUS(exitStatus));
10+ }
11+}
12+
13+int main() {
14+ doSystem("exit 1");
15+ doSystem("./does-not-exist");
16+ return 1;
17+}
test/base001/expectednew file+25
@@ -0,0 +1,25 @@
1+Type checking ./base001.idr
2+exit1: Executing cmd 'exit 1'
3+exit1: raw exitStatus = 256
4+exit1: WEXITSTATUS(exitStatus) = 1
5+exit1: Executing cmd './does-not-exist'
6+exit1: raw exitStatus = 32512
7+exit1: WEXITSTATUS(exitStatus) = 127
8+-------------------------------------------
9+Executing 'exit 1'
10+raw status = 256
11+exit status = 1
12+True
13+
14+-------------------------------------------
15+Executing './exit1'
16+raw status = 256
17+exit status = 1
18+True
19+
20+-------------------------------------------
21+Executing './does-not-exist'
22+raw status = 32512
23+exit status = 127
24+True
25+
test/base001/runnew file+10
@@ -0,0 +1,10 @@
1+#!/usr/bin/env bash
2+
3+if [[ ${OSTYPE} = 'msys' ]]; then
4+ cat expected # skip this test on Windows
5+else
6+ ${IDRIS:-idris} $@ --build base001.ipkg | grep -v 'make.*:'
7+ ./base001
8+ make clean | grep -v 'make.*:'
9+ rm -f *.ibc base001
10+fi
test/base001/sys.cnew file+11
@@ -0,0 +1,11 @@
1+#include "sys.h"
2+
3+#include <stdlib.h>
4+
5+int WIFEXITED_(int status) {
6+ return WIFEXITED(status);
7+}
8+
9+int WEXITSTATUS_(int status) {
10+ return WEXITSTATUS(status);
11+}
test/base001/sys.hnew file+7
@@ -0,0 +1,7 @@
1+#ifndef SYS_H
2+#define SYS_H
3+
4+int WIFEXITED_(int status);
5+int WEXITSTATUS_(int status);
6+
7+#endif
test/layout001/expectednew file+93
@@ -0,0 +1,93 @@
1+Checking layout001a.idr
2+./layout001a.idr:5:1: error: Wrong
3+ indention: should be greater
4+ than context
5+ indentation, expected: space
6+y
7+^
8+Checking layout001b.idr
9+./layout001b.idr:5:3: error: Wrong
10+ indention: should be greater
11+ than context
12+ indentation, expected: space
13+= y
14+ ^
15+Checking layout001c.idr
16+./layout001c.idr:3:1: error: Wrong
17+ indention: should be greater
18+ than context
19+ indentation, expected: space
20+2
21+^
22+Checking layout001d.idr
23+Checking layout001e.idr
24+./layout001e.idr:6:1: error: Wrong
25+ indention: should be greater
26+ than context
27+ indentation, expected: space
28+3
29+^
30+Checking layout001f.idr
31+./layout001f.idr:6:2: error: Wrong
32+ indention: should be greater
33+ than context
34+ indentation, expected: space
35+ 3
36+ ^
37+Checking layout001g.idr
38+./layout001g.idr:6:3: error: Wrong
39+ indention: should be greater
40+ than context
41+ indentation, expected: space
42+ 3
43+ ^
44+Checking layout001h.idr
45+./layout001h.idr:6:3: error: Wrong
46+ indention: should be greater
47+ than context
48+ indentation, expected: space
49+ 3
50+ ^
51+Checking layout001i.idr
52+./layout001i.idr:6:4: error: Wrong
53+ indention: should be greater
54+ than context
55+ indentation, expected: space
56+ 3
57+ ^
58+Checking layout001j.idr
59+./layout001j.idr:6:5: error: Wrong
60+ indention: should be greater
61+ than context
62+ indentation, expected: space
63+ 3
64+ ^
65+Checking layout001k.idr
66+Checking layout001l.idr
67+./layout001l.idr:6:1: error: Wrong
68+ indention: should be greater
69+ than context
70+ indentation, expected: space
71+y
72+^
73+Checking layout001n.idr
74+Checking mplus1.idr
75+mplus1.idr:13:31:
76+When checking right hand side of term with expected type
77+ Maybe Int
78+
79+When checking an application of function Prelude.Applicative.pure:
80+ No such variable f
81+Checking mplus2.idr
82+./mplus2.idr:17:37: error: not
83+ end of block, expected: ")",
84+ "->", ";", "in",
85+ ambiguous use of a left-associative operator,
86+ ambiguous use of a non-associative operator,
87+ ambiguous use of a right-associative operator,
88+ do block expression,
89+ end of input
90+ `mplus` pure f
91+ ^
92+Checking mplus3.idr
93+mplus3.idr:11:1:warning - Unreachable case: term
test/layout001/layout001a.idrnew file+5
@@ -0,0 +1,5 @@
1+f : Int -> Int
2+f x = z 1 + 1 where
3+ z : Int -> Int
4+ z y =
5+y
test/layout001/layout001b.idrnew file+5
@@ -0,0 +1,5 @@
1+f : Int -> Int
2+f x = z 1 + 1 where
3+ z : Int -> Int
4+ z y
5+= y
test/layout001/layout001c.idrnew file+3
@@ -0,0 +1,3 @@
1+f : Int
2+f =
3+2
test/layout001/layout001d.idrnew file+3
@@ -0,0 +1,3 @@
1+f : Int
2+f
3+= 2
test/layout001/layout001e.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+3
test/layout001/layout001f.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+ 3
test/layout001/layout001g.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+ 3
test/layout001/layout001h.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+ 3
test/layout001/layout001i.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+ 3
test/layout001/layout001j.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+ 3
test/layout001/layout001k.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+ 3
test/layout001/layout001l.idrnew file+6
@@ -0,0 +1,6 @@
1+f : Int -> Int
2+f x = z 1 + 1
3+ where
4+ z : Int -> Int
5+ z y =
6+y
test/layout001/layout001n.idrnew file+33
@@ -0,0 +1,33 @@
1+module NonLayout
2+
3+{-
4+Haskell and Idris use indentation for grouping in the concrete syntax.
5+How this works is defined as an automatic translation to the equivalent
6+syntax using { ; and }, which you are free to use yourself.
7+
8+In Idris specifically, if let or where is followed by { then indentation no
9+longer matters for the following definitions until a balanced } appears. To
10+put multiple declarations on one line within the { } you put semicolons between
11+them: one ; for let declarations and ;; for where declarations. Whether this
12+discrepancy is a bug I don't know.
13+-}
14+
15+average : String -> Double
16+average str = answer where
17+ wordCount : String -> Nat
18+ wordCount str = length (words str)
19+ wordLengths : List String -> List Nat
20+ wordLengths strs = map length strs
21+ answer =
22+ let numWords = wordCount str in
23+ let totalLength = sum (wordLengths (words str)) in
24+ cast totalLength / cast numWords
25+
26+average' : String -> Double
27+average' str = answer where {
28+ wordCount : String -> Nat ;; wordCount str = length (words str)
29+ wordLengths : List String -> List Nat ;; wordLengths strs = map length strs
30+ answer = let {
31+ numWords = wordCount str; totalLength = sum (wordLengths (words str))
32+ } in cast totalLength / cast numWords
33+}
test/layout001/mplus1.idrnew file+17
@@ -0,0 +1,17 @@
1+mplus : Maybe a -> Maybe a -> Maybe a
2+mplus a b = ?mplus_rhs
3+
4+factor : Maybe Int
5+factor = ?term_rhs
6+
7+symbol : String -> Maybe Int
8+symbol = ?symbol_rhs
9+
10+term : Maybe Int
11+term = ?term_rhs
12+
13+term = do f <- factor
14+ do symbol "*"
15+ t <- term
16+ pure (f * t)
17+ `mplus` pure f
test/layout001/mplus2.idrnew file+17
@@ -0,0 +1,17 @@
1+mplus : Maybe a -> Maybe a -> Maybe a
2+mplus a b = ?mplus_rhs
3+
4+factor : Maybe Int
5+factor = ?term_rhs
6+
7+symbol : String -> Maybe Int
8+symbol = ?symbol_rhs
9+
10+term : Maybe Int
11+term = ?term_rhs
12+
13+term = do f <- factor
14+ do symbol "*"
15+ t <- term
16+ pure (f * t)
17+ `mplus` pure f
test/layout001/mplus3.idrnew file+17
@@ -0,0 +1,17 @@
1+mplus : Maybe a -> Maybe a -> Maybe a
2+mplus a b = ?mplus_rhs
3+
4+factor : Maybe Int
5+factor = ?term_rhs
6+
7+symbol : String -> Maybe Int
8+symbol = ?symbol_rhs
9+
10+term : Maybe Int
11+term = ?term_rhs
12+
13+term = do f <- factor
14+ do symbol "*"
15+ t <- term
16+ pure (f * t)
17+ `mplus` pure f
test/layout001/runnew file+8
@@ -0,0 +1,8 @@
1+#!/usr/bin/env bash
2+
3+for file in *.idr; do
4+ echo Checking ${file}
5+ ${IDRIS:-idris} --check $@ ${file}
6+done
7+
8+rm -f *.ibc
test/prelude001/expectednew file+10
@@ -0,0 +1,10 @@
1+True
2+True
3+True
4+True
5+True
6+True
7+True
8+True
9+True
10+True
test/prelude001/prelude001.idrnew file+17
@@ -0,0 +1,17 @@
1+module Main
2+
3+main : IO ()
4+main = do
5+ printLn $ lines "" == []
6+ -- `lines` seems to ignore too many trailing newlines.
7+ printLn $ lines "\n" == [] -- FIXME: Should be [""].
8+ printLn $ lines "\n\n" == [] -- FIXME: Should be ["", ""].
9+ printLn $ lines "\n\n\n" == [] -- FIXME: Should be ["", "", ""].
10+ printLn $ lines "1\n2\n3" == ["1", "2", "3"]
11+ printLn $ lines "1\n2\n3\n" == ["1", "2", "3"]
12+ printLn $ unlines [] == ""
13+ -- `unlines` works as advertised doesn't follow Haskell here.
14+ -- When files are written using unlines, vim complains of "noeoln".
15+ printLn $ unlines ["1"] == "1" -- FIXME: Should be "1\n"
16+ printLn $ unlines ["1", "2"] == "1\n2" -- FIXME: Should be "1\n2\n"
17+ printLn $ unlines ["1", "2", "3"] == "1\n2\n3" -- FIXME: Should be "1\n2\n3\n"
test/prelude001/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ prelude001.idr -o prelude001
3+./prelude001
4+rm -f prelude001 *.ibc