on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
commit9fcea3f2c5be53d61c6d538ec5bc34c11d613361 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 3 Aug 2016, 16:24 (10 years ago) parent02d29f59c32ab6
52 files changed+585−80
.travis.yml+23−7 CHANGELOG.md+1 INSTALL.md+5−5 Makefile+2 README.md+2 appveyor.yml+20 docs/faq/faq.rst+3−3 docs/reference/ffi.rst+1−1 docs/reference/repl.rst+1−1 docs/tutorial/interfaces.rst+1−1 docs/tutorial/miscellany.rst+2−2 docs/tutorial/syntax.rst+1−1 docs/tutorial/typesfuns.rst+4−3 idris.cabal+21−2 main/Main.hs+3−1 src/Pkg/Package.hs → src/Idris/Package.hs+7−3 src/Idris/Package/Common.hs+42 src/Pkg/PParser.hs → src/Idris/Package/Parser.hs+8−31 src/Idris/Parser.hs+3−1 stack-shell.nix+1−1 stack.yaml+1−1 test/TestData.hs+8−3 test/TestRun.hs+24−13 test/base001/Makefile+11 test/base001/base001.idr+35 test/base001/base001.ipkg+5 test/base001/exit1.c+17 test/base001/expected+25 test/base001/run+10 test/base001/sys.c+11 test/base001/sys.h+7 test/layout001/expected+93 test/layout001/layout001a.idr+5 test/layout001/layout001b.idr+5 test/layout001/layout001c.idr+3 test/layout001/layout001d.idr+3 test/layout001/layout001e.idr+6 test/layout001/layout001f.idr+6 test/layout001/layout001g.idr+6 test/layout001/layout001h.idr+6 test/layout001/layout001i.idr+6 test/layout001/layout001j.idr+6 test/layout001/layout001k.idr+6 test/layout001/layout001l.idr+6 test/layout001/layout001n.idr+33 test/layout001/mplus1.idr+17 test/layout001/mplus2.idr+17 test/layout001/mplus3.idr+17 test/layout001/run+8 test/prelude001/expected+10 test/prelude001/prelude001.idr+17 test/prelude001/run+4
.travis.yml+23−7
@@ -21,6 +21,9 @@ addons:
2121
2222matrix:
2323 include:
24+ - os: osx
25+ env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"
26+ compiler: ": #GHC 8.0.1"
2427 - env: CABALVER="1.20" GHCVER="7.6.3" TESTS="test_c"
2528 # separate caches for different compiler versions
2629 # until https://github.com/travis-ci/travis-ci/issues/4393 is resolved
@@ -51,26 +54,40 @@ before_cache:
5154
5255before_install:
5356 - unset CC
54− - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$HOME/.cabal/bin:$PATH
57+ - if [[ $TRAVIS_OS_NAME == 'linux' ]];
58+ then
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
5563 - 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
5674
5775install:
5876 - cabal --version
5977 - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"
6078 - if [ -f $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz ];
6179 then
62− zcat $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz >
63− $HOME/.cabal/packages/hackage.haskell.org/00-index.tar;
80+ $ZCAT $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz >
81+ $HOME/.cabal/packages/hackage.haskell.org/00-index.tar;
6482 fi
6583 - travis_retry cabal update -v
6684 # Run build with 2 parallel jobs
6785 # The container environment reports 16 cores,
6886 # causing cabal's default configuration (jobs: $ncpus)
6987 # 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
7189 - cabal install -f FFI --only-dependencies --enable-tests --dry -v > installplan.txt
72− - sed -i -e '1,/^Resolving /d' installplan.txt; cat installplan.txt
73−
90+ - $SED -i -e '1,/^Resolving /d' installplan.txt; cat installplan.txt
7491 # check whether current requested install-plan matches cached package-db snapshot
7592 - if diff -u installplan.txt $HOME/.cabsnap/installplan.txt;
7693 then
@@ -84,7 +101,6 @@ install:
84101 mkdir -p $HOME/.ghc $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin;
85102 cabal install -f FFI --only-dependencies --enable-tests;
86103 fi
87−
88104 # snapshot package-db on cache miss
89105 - if [ ! -d $HOME/.cabsnap ];
90106 then
CHANGELOG.md+1
@@ -34,6 +34,7 @@
3434## Miscellaneous updates
3535
3636* 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.
3738
3839# New in 0.12:
3940
INSTALL.md+5−5
@@ -63,8 +63,8 @@ contribute.
6363[Stack](https://github.com/commercialhaskell/stack) is a new
6464cross-platform program for developing Haskell projects, that enhances
6565the functionality provided by Cabal. There is experimental support for
66−building Idris from source with stack.
67−This installation has been tested on Ubuntu 14.04.2 LTS, and the current
66+building Idris from source with stack.
67+This installation has been tested on Ubuntu 16.04.1 LTS, and the current
6868NixOS unstable.
6969
7070To build Idris with stack the following commands are recommended:
@@ -96,9 +96,9 @@ option flags needs to be fully commented out.
9696There have been reports in the past over building Idris on Mac OS X,
9797using stack, and linking to a HomeBrew installation of `libFFI`. The
9898build has failed to find the correct `libFFI` installation. If you
99−encounter this then the fix is to augment the `PKG_CONFIG_PATH` when
100−running the stack build:
99+encounter this then the fix is to augment the `PKG_CONFIG_PATH` for
100+`libFFI`. For example:
101101
102102```
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
104104```
Makefile+2
@@ -9,8 +9,10 @@ include config.mk
99
1010ifdef CI
1111CABALFLAGS += -f CI
12+ifndef APPVEYOR
1213TEST-ARGS += --color always
1314endif
15+endif
1416
1517install:
1618 $(CABAL) install $(CABALFLAGS)
README.md+2
@@ -1,9 +1,11 @@
11# Idris
22
33[![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)
45[![Documentation Status](https://readthedocs.org/projects/idris/badge/?version=latest)](https://readthedocs.org/projects/idris/?badge=latest)
56[![Hackage](https://budueba.com/hackage/idris)](https://hackage.haskell.org/package/idris)
67
8+
79Idris (http://idris-lang.org/) is a general-purpose functional programming
810language with dependent types.
911
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
198198result in an error, as will attempting to specify the universe level
199199of any type.
200200
201−Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?
201+Why does Idris use ``Double`` instead of ``Float64``?
202202===================================================================================
203203
204204Historically the C language and many other languages have used the
@@ -212,8 +212,8 @@ the size is described in the type name.
212212
213213Due to developer familiarity with the older naming convention, and
214214choice by the developers of Idris, Idris uses the C style convention.
215−That is, the names ``Float`` and ``Double`` are used to describe
216−single and double precision numbers.
215+That is, the name ``Double`` is used to describe double precision
216+numbers, and Idris does not support 32 bit floats at present.
217217
218218What is -ffreestanding?
219219=======================
docs/reference/ffi.rst+1−1
@@ -341,7 +341,7 @@ follows:
341341
342342 data JS_Types : Type -> Type where
343343 JS_Str : JS_Types String
344− JS_Float : JS_Types Float
344+ JS_Float : JS_Types Double
345345 JS_Ptr : JS_Types Ptr
346346 JS_Unit : JS_Types ()
347347 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:
367367
368368 prim__eqChar : Char -> Char -> Int
369369
370− prim__eqFloat : Float -> Float -> Int
370+ prim__eqFloat : Double -> Double -> Int
371371
372372 prim__eqInt : Int -> Int -> Int
373373
docs/tutorial/interfaces.rst+1−1
@@ -6,7 +6,7 @@ Interfaces
66
77We often want to define functions which work across several different
88data 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
1010``==`` to work on the majority of data types. We would like to be able
1111to display different types in a uniform way.
1212
docs/tutorial/miscellany.rst+2−2
@@ -151,7 +151,7 @@ function:
151151
152152 interpFTy : FTy -> Type
153153 interpFTy FInt = Int
154− interpFTy FFloat = Float
154+ interpFTy FFloat = Double
155155 interpFTy FChar = Char
156156 interpFTy FString = String
157157 interpFTy FPtr = Ptr
@@ -237,7 +237,7 @@ command or the ``%dynamic`` directive. For example:
237237
238238 Idris> :dynamic libm.so
239239 Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
240− 0.9995736030415051 : Float
240+ 0.9995736030415051 : Double
241241
242242Type Providers
243243==============
docs/tutorial/syntax.rst+1−1
@@ -73,7 +73,7 @@ bound is below the upper bound using ``so``:
7373.. code-block:: idris
7474
7575 data Interval : Type where
76− MkInterval : (lower : Float) -> (upper : Float) ->
76+ MkInterval : (lower : Double) -> (upper : Double) ->
7777 so (lower < upper) -> Interval
7878
7979We can define a syntax which, in patterns, always matches ``oh`` for
docs/tutorial/typesfuns.rst+4−3
@@ -8,7 +8,7 @@ Primitive Types
88===============
99
1010Idris 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
1212manipulation, and ``Ptr`` which represents foreign pointers. There are
1313also several data types declared in the library, including ``Bool``,
1414with values ``True`` and ``False``. We can declare some constants with
@@ -1216,8 +1216,9 @@ Pythagorean triples as follows:
12161216The ``[a..b]`` notation is another shorthand which builds a list of
12171217numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
12181218list of numbers between ``a`` and ``c`` with the increment specified
1219−by the difference between ``a`` and ``b``. This works for any numeric
1220−type, using the ``count`` function from the prelude.
1219+by the difference between ``a`` and ``b``. This works for type ``Nat``,
1220+``Int`` and ``Integer``, using the ``enumFromTo`` and ``enumFromThenTo``
1221+function from the prelude.
12211222
12221223``case`` expressions
12231224--------------------
idris.cabal+21−2
@@ -293,6 +293,15 @@ Extra-source-files:
293293 test/reg075/*.idr
294294 test/reg075/expected
295295
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+
296305 test/basic001/run
297306 test/basic001/*.idr
298307 test/basic001/expected
@@ -598,6 +607,10 @@ Extra-source-files:
598607 test/io003/*.idr
599608 test/io003/expected
600609
610+ test/layout001/expected
611+ test/layout001/*.idr
612+ test/layout001/run
613+
601614 test/literate001/run
602615 test/literate001/*.lidr
603616 test/literate001/expected
@@ -615,6 +628,10 @@ Extra-source-files:
615628 test/meta004/*.idr
616629 test/meta004/expected
617630
631+ test/prelude001/expected
632+ test/prelude001/prelude001.idr
633+ test/prelude001/run
634+
618635 test/primitives001/run
619636 test/primitives001/*.idr
620637 test/primitives001/expected
@@ -1042,7 +1059,9 @@ Library
10421059 , IRTS.Simplified
10431060 , IRTS.System
10441061
1045− , Pkg.Package
1062+ , Idris.Package
1063+ , Idris.Package.Common
1064+
10461065 , Util.DynamicLinker
10471066 , Util.ScreenSize
10481067 , Util.System
@@ -1051,7 +1070,7 @@ Library
10511070 Util.Pretty
10521071 , Util.Net
10531072
1054− , Pkg.PParser
1073+ , Idris.Package.Parser
10551074
10561075 -- Auto Generated
10571076 , Paths_idris
main/Main.hs+3−1
@@ -10,11 +10,13 @@ import Idris.Imports
1010import Idris.Error
1111import Idris.CmdOptions
1212
13+import Idris.Package
14+
1315import IRTS.System ( getLibFlags, getIdrisLibDir, getIncFlags )
1416
1517import Util.System ( setupBundledCC )
1618
17−import Pkg.Package
19+
1820
1921-- Main program reads command line options, parses the main program, and gets
2022-- on with the REPL.
src/Pkg/Package.hs → src/Idris/Package.hsrenamed+7−3
@@ -1,12 +1,12 @@
11{-|
2−Module : Pkg.Package
2+Module : Idris.Package
33Description : Functionality for working with Idris packages.
44Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
88{-# LANGUAGE CPP #-}
9−module Pkg.Package where
9+module Idris.Package where
1010
1111import System.Process
1212import System.Directory
@@ -38,7 +38,8 @@ import Idris.Output
3838import Idris.Imports
3939import Idris.Error (ifail)
4040
41−import Pkg.PParser
41+import Idris.Package.Common
42+import Idris.Package.Parser
4243
4344import IRTS.System
4445
@@ -49,6 +50,9 @@ import IRTS.System
4950-- * invoke idris on each module, with idris_opts
5051-- * install everything into datadir/pname, if install flag is set
5152
53+getPkgDesc :: FilePath -> IO PkgDesc
54+getPkgDesc = parseDesc
55+
5256-- --------------------------------------------------------- [ Build Packages ]
5357
5458-- | 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 @@
11{-|
2−Module : Pkg.PParser
2+Module : Idris.Package.Parser
33Description : `iPKG` file parser and package description information.
44Copyright :
55License : BSD3
@@ -9,7 +9,7 @@ Maintainer : The Idris Community.
99#if !(MIN_VERSION_base(4,8,0))
1010{-# LANGUAGE OverlappingInstances #-}
1111#endif
12−module Pkg.PParser where
12+module Idris.Package.Parser where
1313
1414import Text.Trifecta hiding (span, charLiteral, natural, symbol, char, string, whiteSpace)
1515import qualified Text.PrettyPrint.ANSI.Leijen as PP
@@ -19,43 +19,18 @@ import Idris.AbsSyntaxTree
1919import Idris.Parser.Helpers hiding (stringLiteral)
2020import Idris.CmdOptions
2121
22+import Idris.Package.Common
23+
2224import Control.Monad.State.Strict
2325import Control.Applicative
2426import System.FilePath (takeFileName, isValid)
2527import Data.Maybe (isNothing, fromJust)
28+import Data.List (union)
2629
2730import Util.System
2831
2932type PParser = StateT PkgDesc IdrisInnerParser
3033
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−
5934instance HasLastTokenSpan PParser where
6035 getLastTokenSpan = return Nothing
6136
@@ -169,7 +144,9 @@ pClause = do reserved "executable"; lchar '=';
169144 ps <- sepBy1 (fst <$> identifier) (lchar ',')
170145 st <- get
171146 let pkgs = pureArgParser $ concatMap (\x -> ["-p", x]) ps
172− put (st {idris_opts = pkgs ++ idris_opts st})
147+
148+ put (st { pkgdeps = ps `union` (pkgdeps st)
149+ , idris_opts = pkgs ++ idris_opts st})
173150
174151 <|> do reserved "modules"; lchar '=';
175152 ms <- sepBy1 (fst <$> iName []) (lchar ',')
src/Idris/Parser.hs+3−1
@@ -1116,7 +1116,9 @@ RHSName ::= '{' FnName '}';
11161116@
11171117-}
11181118rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1119−rhs syn n = do lchar '='; expr syn
1119+rhs syn n = do lchar '='
1120+ indentPropHolds gtProp
1121+ expr syn
11201122 <|> do symbol "?=";
11211123 fc <- getFC
11221124 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
stack-shell.nix+1−1
@@ -2,7 +2,7 @@ with (import <nixpkgs> {});
22
33let
44 # MUST match resolver in stack.yaml
5− resolver = haskell.packages.lts-6_4.ghc;
5+ resolver = haskell.packages.lts-6_9.ghc;
66
77 native_libs = [
88 libffi
stack.yaml+1−1
@@ -1,4 +1,4 @@
1−resolver: lts-6.5
1+resolver: lts-6.9
22
33packages:
44 - location: .
test/TestData.hs+8−3
@@ -30,8 +30,8 @@ toCodegenSet compatCodegen = fmap Set.fromList mList where
3030 NONE -> Nothing
3131
3232testFamilies :: [TestFamily]
33−testFamilies = fmap instanciate testFamiliesData where
34− instanciate (id, name, testsData) = TestFamily id name tests where
33+testFamilies = fmap instantiate testFamiliesData where
34+ instantiate (id, name, testsData) = TestFamily id name tests where
3535 tests = IMap.fromList (fmap makeSetCodegen testsData)
3636 makeSetCodegen (index, codegens) = (index, toCodegenSet codegens)
3737
@@ -50,6 +50,8 @@ testFamiliesForCodegen codegen =
5050-- The third column is the data for each test
5151testFamiliesData :: [(String, String, [(Index, CompatCodegen)])]
5252testFamiliesData = [
53+ ("base", "Base",
54+ [ ( 1, C_CG )]),
5355 ("basic", "Basic",
5456 [ ( 1, ANY ),
5557 ( 2, ANY ),
@@ -156,6 +158,8 @@ testFamiliesData = [
156158 [ ( 1, C_CG ),
157159 ( 2, ANY ),
158160 ( 3, C_CG )]),
161+ ("layout", "Layout",
162+ [ ( 1, ANY )]),
159163 ("literate", "Literate programming",
160164 [ ( 1, ANY )]),
161165 ("meta", "Meta-programming",
@@ -168,6 +172,8 @@ testFamiliesData = [
168172 ( 2, ANY ),
169173 ( 3, ANY ),
170174 ( 4, ANY )]),
175+ ("prelude", "Prelude",
176+ [ ( 1, ANY )]),
171177 ("primitives", "Primitive types",
172178 [ ( 1, ANY ),
173179 ( 2, ANY ),
@@ -297,4 +303,3 @@ testFamiliesData = [
297303 [ ( 1, ANY ),
298304 ( 2, ANY ),
299305 ( 3, C_CG )])]
300−
test/TestRun.hs+24−13
@@ -54,7 +54,8 @@ instance IsOption NodeOpt where
5454 optionCLParser = fmap NodeOpt $ switch (long nodeArg <> help nodeHelp)
5555
5656ingredients :: [Ingredient]
57−ingredients = [rerunningTests [consoleTestReporter],
57+ingredients = defaultIngredients ++
58+ [rerunningTests [consoleTestReporter],
5859 includingOptions [Option (Proxy :: Proxy NodeOpt)] ]
5960
6061----------------------------------------------------------------------- [ Core ]
@@ -63,28 +64,37 @@ ingredients = [rerunningTests [consoleTestReporter],
6364-- A ripoff of goldenVsFile from Tasty.Golden
6465test :: String -> String -> IO () -> TestTree
6566test 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
6768 where
6869 ref = path </> "expected"
6970 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
7172 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+
7385
7486-- Takes the filepath and content of `expected` and `output`
7587-- and formats an error message stating their difference
76−printDiff :: (String, BS.ByteString) -> (String, BS.ByteString) -> String
88+printDiff :: (String, String) -> (String, String) -> String
7789printDiff (ref, x) (new, y) =
78− let refcnt = BSC.unpack x
79− newcnt = BSC.unpack y
80− printContent cnt =
90+ let printContent cnt =
8191 if Data.List.null cnt
8292 then " is empty...\n"
8393 else " is: \n" ++ unlines (fmap ((++) " ") (lines cnt))
8494 in
8595 "Test mismatch!\n" ++
86− "Golden file " ++ ref ++ printContent refcnt ++
87− "However, " ++ new ++ printContent newcnt
96+ "Golden file " ++ ref ++ printContent x ++
97+ "However, " ++ new ++ printContent y
8898
8999-- Should always output a 3-charater string from a postive Int
90100indexToString :: Int -> String
@@ -112,9 +122,11 @@ mkGoldenTests testFamilies flags =
112122runTest :: String -> Flags -> IO ()
113123runTest path flags = do
114124 let run = (proc "bash" ("run" : flags)) {cwd = Just path,
115− std_out = CreatePipe}
116− (_, output, _) <- readCreateProcessWithExitCode run ""
125+ std_out = CreatePipe,
126+ std_err = CreatePipe}
127+ (_, output, error_out) <- readCreateProcessWithExitCode run ""
117128 writeFile (path </> "output") output
129+ hPutStrLn stderr error_out
118130
119131main :: IO ()
120132main = do
@@ -125,4 +137,3 @@ main = do
125137 in
126138 mkGoldenTests (testFamiliesForCodegen codegen)
127139 (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