idris 0.12.1 → 0.12.2
raw patch · 144 files changed
+1994/−1102 lines, 144 filesdep +taggeddep +tastydep +tasty-goldendep ~bytestringsetup-changed
Dependencies added: tagged, tasty, tasty-golden, tasty-rerun
Dependency ranges changed: bytestring
Files
- CHANGELOG.md +6/−0
- Makefile +19/−5
- README.md +2/−0
- Setup.hs +29/−0
- config.mk +4/−2
- idris.cabal +63/−9
- libs/prelude/Prelude.idr +31/−23
- libs/prelude/Prelude/Basics.idr +1/−1
- main/Main.hs +3/−1
- man/idris.1 +1/−1
- src/Idris/AbsSyntaxTree.hs +4/−2
- src/Idris/Core/Evaluate.hs +27/−0
- src/Idris/Package.hs +447/−0
- src/Idris/Package/Common.hs +42/−0
- src/Idris/Package/Parser.hs +242/−0
- src/Idris/Parser.hs +3/−1
- src/Pkg/PParser.hs +0/−265
- src/Pkg/Package.hs +0/−437
- src/Util/Net.hs +4/−4
- stack.yaml +1/−1
- test/Makefile +0/−34
- test/TestData.hs +307/−0
- test/TestRun.hs +139/−0
- test/base001/Makefile +11/−0
- test/base001/base001.idr +35/−0
- test/base001/base001.ipkg +5/−0
- test/base001/exit1.c +17/−0
- test/base001/expected +25/−0
- test/base001/run +10/−0
- test/base001/sys.c +11/−0
- test/base001/sys.h +7/−0
- test/basic010/run +2/−2
- test/basic013/basic013.idr +9/−0
- test/basic013/expected +9/−0
- test/bounded001/bounded001.idr +10/−0
- test/bounded001/expected +6/−0
- test/bounded001/run +4/−0
- test/disambig002/disambig002.idr +2/−0
- test/docs001/run +1/−1
- test/docs002/run +1/−1
- test/docs003/run +1/−1
- test/docs004/run +1/−1
- test/docs005/run +1/−1
- test/effects001/run +2/−2
- test/effects002/run +1/−1
- test/ffi001/run +1/−1
- test/ffi002/run +1/−1
- test/ffi003/run +1/−1
- test/ffi004/run +1/−1
- test/ffi006/run +1/−1
- test/idrisdoc001/run +1/−1
- test/idrisdoc002/run +1/−1
- test/idrisdoc003/run +1/−1
- test/idrisdoc004/run +1/−1
- test/idrisdoc005/run +1/−1
- test/idrisdoc006/run +2/−2
- test/idrisdoc007/run +1/−1
- test/idrisdoc008/run +1/−1
- test/interactive001/run +1/−1
- test/interactive002/run +1/−1
- test/interactive003/run +1/−1
- test/interactive004/run +1/−1
- test/interactive005/run +1/−1
- test/interactive006/run +1/−1
- test/interactive007/run +1/−1
- test/interactive008/run +1/−1
- test/interactive009/run +1/−1
- test/interactive010/run +1/−1
- test/interactive011/run +1/−1
- test/interactive012/run +1/−1
- test/interactive013/run +1/−1
- test/layout001/expected +93/−0
- test/layout001/layout001a.idr +5/−0
- test/layout001/layout001b.idr +5/−0
- test/layout001/layout001c.idr +3/−0
- test/layout001/layout001d.idr +3/−0
- test/layout001/layout001e.idr +6/−0
- test/layout001/layout001f.idr +6/−0
- test/layout001/layout001g.idr +6/−0
- test/layout001/layout001h.idr +6/−0
- test/layout001/layout001i.idr +6/−0
- test/layout001/layout001j.idr +6/−0
- test/layout001/layout001k.idr +6/−0
- test/layout001/layout001l.idr +6/−0
- test/layout001/layout001n.idr +33/−0
- test/layout001/mplus1.idr +17/−0
- test/layout001/mplus2.idr +17/−0
- test/layout001/mplus3.idr +17/−0
- test/layout001/run +8/−0
- test/meta002/run +1/−1
- test/meta003/BadDef.idr +12/−0
- test/meta003/expected +6/−0
- test/meta003/run +3/−0
- test/pkg002/Main.idr +4/−0
- test/pkg002/expected +0/−0
- test/pkg002/run +5/−0
- test/pkg002/test.ipkg +8/−0
- test/pkg003/Main.idr +4/−0
- test/pkg003/expected +0/−0
- test/pkg003/run +6/−0
- test/pkg003/test.ipkg +7/−0
- test/pkg004/Main.idr +4/−0
- test/pkg004/expected +5/−0
- test/pkg004/run +6/−0
- test/pkg004/test.ipkg +8/−0
- test/pkg005/expected +1/−0
- test/pkg005/run +3/−0
- test/pkg005/test.ipkg +3/−0
- test/pkg006/expected +1/−0
- test/pkg006/run +3/−0
- test/pkg006/test.ipkg +3/−0
- test/prelude001/expected +10/−0
- test/prelude001/prelude001.idr +17/−0
- test/prelude001/run +4/−0
- test/primitives002/run +1/−1
- test/proof004/run +1/−1
- test/proof005/run +1/−1
- test/proof006/run +1/−1
- test/proof007/run +1/−1
- test/proof008/run +1/−1
- test/proofsearch003/run +1/−1
- test/reg002/run +1/−1
- test/reg003/run +2/−2
- test/reg007/run +1/−1
- test/reg023/run +1/−1
- test/reg034/run +1/−1
- test/reg035/run +3/−3
- test/reg039/run +2/−2
- test/reg040/run +1/−1
- test/reg044/run +1/−1
- test/reg049/run +1/−1
- test/reg050/run +3/−3
- test/reg054/run +1/−1
- test/reg055/run +2/−2
- test/reg075/run +1/−1
- test/runtest.hs +0/−230
- test/totality003/run +2/−2
- test/totality009/run +3/−3
- test/tutorial001/run +1/−1
- test/tutorial006/run +3/−3
- test/tutorial007/run +2/−2
- test/unique001/run +6/−6
- test/unique002/run +2/−2
- test/unique003/run +1/−1
CHANGELOG.md view
@@ -25,11 +25,17 @@ * The File Effect has been updated to take into account changes in `Prelude.File` and to provide a 'better' API.+* `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. ## Tool updates * Idris' documentation system now displays the documentation for auto implicits in the output of `:doc`. This is tested for in `docs005`.++## Miscellaneous updates++* 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`.+* Added OSX and Windows continous integration with Travis and Appveyor. # New in 0.12:
Makefile view
@@ -1,11 +1,18 @@-.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib fast test_c test lib_doc lib_doc_clean user_doc_html user_doc_pdf user_docs+.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib fast test_js test_c test test_clean lib_doc lib_doc_clean user_doc_html user_doc_pdf user_docs +ARGS=+TEST-JOBS=+TEST-ARGS=+ include config.mk -include custom.mk ifdef CI CABALFLAGS += -f CI+ifndef APPVEYOR+TEST-ARGS += --color always endif+endif install: $(CABAL) install $(CABALFLAGS)@@ -20,13 +27,20 @@ test: doc test_c test_c:- $(MAKE) -C test IDRIS=../dist/build/idris/idris test+ $(CABAL) test $(ARGS) --test-options \+ "$(TEST-ARGS) --rerun-update +RTS -N$(TEST-JOBS) -RTS" test_js:- $(MAKE) -C test IDRIS=../dist/build/idris/idris test_js+ $(CABAL) test $(ARGS) --test-options \+ "$(TEST-ARGS) --node --rerun-update +RTS -N$(TEST-JOBS) -RTS" -test_timed:- $(MAKE) -C test IDRIS=../dist/build/idris/idris time+test_update:+ $(CABAL) test $(ARGS) --test-options \+ "$(TEST-ARGS) --accept +RTS -N$(TEST-JOBS) -RTS"++test_clean:+ rm -f test/*~+ rm -f test/*/output lib_clean: $(MAKE) -C libs IDRIS=../../dist/build/idris/idris RTS=../../dist/build/rts/libidris_rts clean
README.md view
@@ -1,8 +1,10 @@ # Idris [](https://travis-ci.org/idris-lang/Idris-dev)+[](https://ci.appveyor.com/project/idrislang/idris-dev) [](https://readthedocs.org/projects/idris/?badge=latest) [](https://hackage.haskell.org/package/idris)+ Idris (http://idris-lang.org/) is a general-purpose functional programming language with dependent types.
Setup.hs view
@@ -264,6 +264,30 @@ make verbosity [ "-C", src, "install" , "TARGET=" ++ target, "IDRIS=" ++ idrisCmd local] -- -----------------------------------------------------------------------------+-- Test++-- FIXME: We use the __GLASGOW_HASKELL__ macro because MIN_VERSION_cabal seems+-- to be broken !++-- There are two "dataDir" in cabal, and they don't relate to each other.+-- When fetching modules, idris uses the second path (in the pkg record),+-- which by default is the root folder of the project.+-- We want it to be the install directory where we put the idris libraries.+fixPkg pkg target = pkg { dataDir = target }++-- The "Args" argument of the testHooks has been added in cabal 1.22.0,+-- and should therefore be ignored for prior versions.+#if __GLASGOW_HASKELL__ < 710+originalTestHook _ = testHook simpleUserHooks+#else+originalTestHook = testHook simpleUserHooks+#endif++idrisTestHook args pkg local hooks flags = do+ let target = datadir $ L.absoluteInstallDirs pkg local NoCopyDest+ originalTestHook args (fixPkg pkg target) local hooks flags++-- ----------------------------------------------------------------------------- -- Main -- Install libraries during both copy and install@@ -281,4 +305,9 @@ NoCopyDest pkg local , preSDist = idrisPreSDist , postSDist = idrisPostSDist+#if __GLASGOW_HASKELL__ < 710+ , testHook = idrisTestHook ()+#else+ , testHook = idrisTestHook+#endif }
config.mk view
@@ -14,9 +14,11 @@ # Any flags defined here which alter the RTS API must also be added to src/IRTS/CodegenC.hs CFLAGS :=-O2 -Wall -DHAS_PTHREAD -DIDRIS_ENABLE_STATS $(CFLAGS) -#CABALFLAGS :=+# CABALFLAGS :=+CABALFLAGS += --enable-tests ## Disable building of Effects-#CABALFLAGS :=-f NoEffects+#CABALFLAGS :=-f NoEffects $(CABALFLAGS)+ ifneq (, $(findstring bsd, $(MACHINE))) GMP_INCLUDE_DIR :=
idris.cabal view
@@ -1,5 +1,5 @@ Name: idris-Version: 0.12.1+Version: 0.12.2 License: BSD3 License-file: LICENSE Author: Edwin Brady@@ -146,7 +146,7 @@ libs/effects/Makefile libs/effects/effects.ipkg libs/effects/Effect/*.idr- libs/effects/Effect/Logging/*.idr+ libs/effects/Effect/Logging/*.idr libs/effects/*.idr libs/pruviloj/Makefile@@ -156,8 +156,8 @@ libs/pruviloj/Pruviloj/Derive/*.idr libs/pruviloj/Pruviloj/Internals/*.idr - test/Makefile- test/runtest.hs+ test/TestRun.hs+ test/TestData.hs test/regression001/run test/regression001/expected@@ -293,6 +293,15 @@ test/reg075/*.idr test/reg075/expected + test/base001/Makefile+ test/base001/base001.idr+ test/base001/base001.ipkg+ test/base001/exit1.c+ test/base001/expected+ test/base001/run+ test/base001/sys.c+ test/base001/sys.h+ test/basic001/run test/basic001/*.idr test/basic001/expected@@ -356,6 +365,10 @@ test/bignum002/*.idr test/bignum002/expected + test/bounded001/run+ test/bounded001/*.idr+ test/bounded001/expected+ test/corecords001/*.idr test/corecords001/run test/corecords001/expected@@ -594,6 +607,10 @@ test/io003/*.idr test/io003/expected + test/layout001/expected+ test/layout001/*.idr+ test/layout001/run+ test/literate001/run test/literate001/*.lidr test/literate001/expected@@ -604,10 +621,17 @@ test/meta002/run test/meta002/*.idr test/meta002/expected+ test/meta003/run+ test/meta003/*.idr+ test/meta003/expected test/meta004/run test/meta004/*.idr test/meta004/expected + test/prelude001/expected+ test/prelude001/prelude001.idr+ test/prelude001/run+ test/primitives001/run test/primitives001/*.idr test/primitives001/expected@@ -630,9 +654,27 @@ test/primitives006/expected test/pkg001/run- test/pkg001/test-pkg.ipkg test/pkg001/*.idr test/pkg001/expected+ test/pkg001/*.ipkg+ test/pkg002/run+ test/pkg002/*.idr+ test/pkg002/expected+ test/pkg002/*.ipkg+ test/pkg003/run+ test/pkg003/*.idr+ test/pkg003/expected+ test/pkg003/*.ipkg+ test/pkg004/run+ test/pkg004/*.idr+ test/pkg004/expected+ test/pkg004/*.ipkg+ test/pkg005/run+ test/pkg005/expected+ test/pkg005/*.ipkg+ test/pkg006/run+ test/pkg006/expected+ test/pkg006/*.ipkg test/proof001/run test/proof001/*.idr@@ -1023,7 +1065,9 @@ , IRTS.Simplified , IRTS.System - , Pkg.Package+ , Idris.Package+ , Idris.Package.Common+ , Util.DynamicLinker , Util.ScreenSize , Util.System@@ -1032,7 +1076,7 @@ Util.Pretty , Util.Net - , Pkg.PParser+ , Idris.Package.Parser -- Auto Generated , Paths_idris@@ -1137,9 +1181,10 @@ ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields -Test-suite regression-and-sanity-tests+Test-suite regression-and-feature-tests Type: exitcode-stdio-1.0- Main-is: runtest.hs+ Main-is: TestRun.hs+ Other-modules: TestData hs-source-dirs: test Build-depends: idris@@ -1150,7 +1195,16 @@ , filepath , directory , haskeline >= 0.7+ , optparse-applicative >= 0.11 && < 0.13+ , tagged+ , tasty >= 0.8+ , tasty-golden >= 2.0+ , tasty-rerun >= 1.0.0+ , bytestring , transformers+ if impl(ghc < 7.10)+ Extensions: DeriveDataTypeable+ ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields
libs/prelude/Prelude.idr view
@@ -146,12 +146,18 @@ -- predefine Nat versions of Enum, so we can use them in the default impls total natEnumFromThen : Nat -> Nat -> Stream Nat-natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc+natEnumFromThen n next = n :: natEnumFromThen next (minus next n) total natEnumFromTo : Nat -> Nat -> List Nat-natEnumFromTo n m = map (plus n) (natRange (minus (S m) n))+natEnumFromTo n m = if n <= m+ then go n m+ else List.reverse $ go m n+ where go : Nat -> Nat -> List Nat+ go n m = map (plus n) (natRange (minus (S m) n))+total natEnumFromThenTo' : Nat -> Nat -> Nat -> List Nat+natEnumFromThenTo' _ Z _ = []+natEnumFromThenTo' n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ))) total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat-natEnumFromThenTo _ Z _ = []-natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))+natEnumFromThenTo n next m = natEnumFromThenTo' n (minus next n) m interface Enum a where total pred : a -> a@@ -184,36 +190,38 @@ fromNat n = cast n enumFromThen n inc = n :: enumFromThen (inc + n) inc enumFromTo n m = if n <= m- then go (natRange (S (cast {to = Nat} (m - n))))- else []- where go : List Nat -> List Integer- go [] = []- go (x :: xs) = n + cast x :: go xs+ then go n m+ else List.reverse $ go m n+ where go' : Integer -> List Nat -> List Integer+ go' _ [] = []+ go' n (x :: xs) = n + cast x :: go' n xs+ go : Integer -> Integer -> List Integer+ go n m = go' n (natRange (S (cast {to = Nat} (m - n)))) enumFromThenTo _ 0 _ = []- enumFromThenTo n inc m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs inc) - 1))) SIsNotZ)))+ enumFromThenTo n next m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ))) where go : List Nat -> List Integer go [] = []- go (x :: xs) = n + (cast x * inc) :: go xs+ go (x :: xs) = n + (cast x * (next - n)) :: go xs Enum Int where pred n = n - 1 succ n = n + 1 toNat n = cast n fromNat n = cast n- enumFromTo n m =- if n <= m- then go [] (cast {to = Nat} (m - n)) m- else []- where- go : List Int -> Nat -> Int -> List Int- go acc Z m = m :: acc- go acc (S k) m = go (m :: acc) k (m - 1)+ enumFromTo n m = if n <= m+ then go n m+ else List.reverse $ go m n+ where go' : List Int -> Nat -> Int -> List Int+ go' acc Z m = m :: acc+ go' acc (S k) m = go' (m :: acc) k (m - 1)+ go : Int -> Int -> List Int+ go n m = go' [] (cast {to = Nat} (m - n)) m enumFromThen n inc = n :: enumFromThen (inc + n) inc enumFromThenTo _ 0 _ = []- enumFromThenTo n inc m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs inc) - 1))) SIsNotZ)))+ enumFromThenTo n next m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ))) where go : List Nat -> List Int go [] = []- go (x :: xs) = n + (cast x * inc) :: go xs+ go (x :: xs) = n + (cast x * (next - n)) :: go xs Enum Char where toNat c = toNat (ord c)@@ -224,12 +232,12 @@ syntax "[" [start] ".." [end] "]" = enumFromTo start end syntax "[" [start] "," [next] ".." [end] "]"- = enumFromThenTo start (next - start) end+ = enumFromThenTo start next end syntax "[" [start] ".." "]" = enumFrom start syntax "[" [start] "," [next] ".." "]"- = enumFromThen start (next - start)+ = enumFromThen start next ---- More utilities
libs/prelude/Prelude/Basics.idr view
@@ -19,7 +19,7 @@ ||| Constant function. Ignores its second argument. const : a -> b -> a-const x = \v => x+const x = \value => x ||| Return the first element of a pair. fst : (a, b) -> a
main/Main.hs view
@@ -10,11 +10,13 @@ import Idris.Error import Idris.CmdOptions +import Idris.Package+ import IRTS.System ( getLibFlags, getIdrisLibDir, getIncFlags ) import Util.System ( setupBundledCC ) -import Pkg.Package+ -- Main program reads command line options, parses the main program, and gets -- on with the REPL.
man/idris.1 view
@@ -1,6 +1,6 @@ .\" Manpage for Idris. .\" Contact <> to correct errors or typos.-.TH man 1 "25 March 2016" "0.12" "Idris man page"+.TH man 1 "25 March 2016" "0.12.2" "Idris man page" .SH NAME idris -\ a general purpose pure functional programming language with dependent types. .SH SYNOPSIS
src/Idris/AbsSyntaxTree.hs view
@@ -1994,8 +1994,9 @@ else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs)) prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a prettySe d p bnd (PCase _ scr cases) =- align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>- depth d (indent 2 (vsep (map ppcase cases)))+ bracket p funcAppPrec $+ align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>+ depth d (indent 2 (vsep (map ppcase cases))) where ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec ([(n, False) | n <- vars l] ++ bnd)@@ -2255,6 +2256,7 @@ -> Doc OutputAnnotation prettyName infixParen showNS bnd n | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"+ | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_" | (UN n') <- n, T.unpack n' == "_" = text "_" | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
src/Idris/Core/Evaluate.hs view
@@ -636,6 +636,15 @@ ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t') ceqB ps (Pi i v t) (Pi i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t') ceqB ps b b' = ceq ps (binderTy b) (binderTy b')+ -- Special case for 'case' blocks - size of scope causes complications,+ -- we only want to check the blocks themselves are valid and identical+ -- in the current scope. So, just check the bodies, and the additional+ -- arguments the case blocks are applied to.+ ceq ps x@(App _ _ _) y@(App _ _ _)+ | (P _ cx _, xargs) <- unApply x,+ (P _ cy _, yargs) <- unApply y,+ caseName cx && caseName cy = sameCase ps cx cy xargs yargs+ ceq ps (App _ fx ax) (App _ fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay) ceq ps (Constant x) (Constant y) = return (x == y) ceq ps (TType x) (TType y) | x == y = return True@@ -677,6 +686,24 @@ (_, ydef) = cases_compiletime yd in caseeq ((x,y):ps) xdef ydef _ -> return False++ sameCase :: [(Name, Name)] -> Name -> Name -> [Term] -> [Term] -> + StateT UCs TC Bool+ sameCase ps x y xargs yargs+ = case (lookupDef x ctxt, lookupDef y ctxt) of+ ([Function _ xdef], [Function _ ydef])+ -> ceq ((x,y):ps) xdef ydef+ ([CaseOp _ _ _ _ _ xd],+ [CaseOp _ _ _ _ _ yd])+ -> let (xin, xdef) = cases_compiletime xd+ (yin, ydef) = cases_compiletime yd in+ do liftM2 (&&) + (do ok <- zipWithM (ceq ps)+ (drop (length xin) xargs)+ (drop (length yin) yargs)+ return (and ok))+ (caseeq ((x,y):ps) xdef ydef)+ _ -> return False -- SPECIALISATION ----------------------------------------------------------- -- We need too much control to be able to do this by tweaking the main
+ src/Idris/Package.hs view
@@ -0,0 +1,447 @@+{-|+Module : Idris.Package+Description : Functionality for working with Idris packages.+Copyright :+License : BSD3+Maintainer : The Idris Community.+-}+{-# LANGUAGE CPP #-}+module Idris.Package where++import System.Process+import System.Directory+import System.Exit+import System.IO+import System.FilePath ((</>), addTrailingPathSeparator, takeFileName,+ takeDirectory, normalise, addExtension, hasExtension)+import System.Directory (createDirectoryIfMissing, copyFile)++import Util.System++import Control.Monad+import Control.Monad.Trans.State.Strict (execStateT)+import Control.Monad.Trans.Except (runExceptT)++import Data.List+import Data.List.Split(splitOn)+import Data.Maybe(fromMaybe)+import Data.Either(partitionEithers)++import Idris.Core.TT+import Idris.REPL+import Idris.Parser (loadModule)+import Idris.Output (pshow)+import Idris.AbsSyntax+import Idris.IdrisDoc+import Idris.IBC+import Idris.Output+import Idris.Imports+import Idris.Error (ifail)++import Idris.Package.Common+import Idris.Package.Parser++import IRTS.System++-- To build a package:+-- * read the package description+-- * check all the library dependencies exist+-- * invoke the makefile if there is one+-- * invoke idris on each module, with idris_opts+-- * install everything into datadir/pname, if install flag is set++getPkgDesc :: FilePath -> IO PkgDesc+getPkgDesc = parseDesc++-- --------------------------------------------------------- [ Build Packages ]++-- | Run the package through the idris compiler.+buildPkg :: [Opt] -- ^ Command line options+ -> Bool -- ^ Provide Warnings+ -> (Bool, FilePath) -- ^ (Should we install, Location of iPKG file)+ -> IO ()+buildPkg copts warnonly (install, fp) = do+ pkgdesc <- parseDesc fp+ dir <- getCurrentDirectory+ let idx = PkgIndex (pkgIndex (pkgname pkgdesc))+ oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)+ when (and oks) $ do+ m_ist <- inPkgDir pkgdesc $ do++ make (makefile pkgdesc)+ case (execout pkgdesc) of+ Nothing -> do+ case mergeOptions copts (idx : NoREPL : Verbose : idris_opts pkgdesc) of+ Left emsg -> do+ putStrLn emsg+ exitWith (ExitFailure 1)+ Right opts -> buildMods opts (modules pkgdesc)+ Just o -> do+ let exec = dir </> o+ case mergeOptions copts (idx : NoREPL : Verbose : Output exec : idris_opts pkgdesc) of+ Left emsg -> do+ putStrLn emsg+ exitWith (ExitFailure 1)+ Right opts -> buildMain opts (idris_main pkgdesc)+ case m_ist of+ Nothing -> exitWith (ExitFailure 1)+ Just ist -> do+ -- Quit with error code if there was a problem+ case errSpan ist of+ Just _ -> exitWith (ExitFailure 1)+ _ -> return ()+ when install $ installPkg (opt getIBCSubDir copts) pkgdesc+ where+ buildMain opts (Just mod) = buildMods opts [mod]+ buildMain _ Nothing = do+ putStrLn "Can't build an executable: No main module given"+ exitWith (ExitFailure 1)++-- --------------------------------------------------------- [ Check Packages ]++-- | Type check packages only+--+-- This differs from build in that executables are not built, if the+-- package contains an executable.+checkPkg :: [Opt] -- ^ Command line Options+ -> Bool -- ^ Show Warnings+ -> Bool -- ^ quit on failure+ -> FilePath -- ^ Path to ipkg file.+ -> IO ()+checkPkg copts warnonly quit fpath = do+ pkgdesc <- parseDesc fpath+ oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)+ when (and oks) $ do+ res <- inPkgDir pkgdesc $ do+ make (makefile pkgdesc)++ case mergeOptions copts (NoREPL : Verbose : idris_opts pkgdesc) of+ Left emsg -> do+ putStrLn emsg+ exitWith (ExitFailure 1)+ Right opts -> do+ buildMods opts (modules pkgdesc)+ when quit $ case res of+ Nothing -> exitWith (ExitFailure 1)+ Just res' -> do+ case errSpan res' of+ Just _ -> exitWith (ExitFailure 1)+ _ -> return ()++-- ------------------------------------------------------------------- [ REPL ]++-- | Check a package and start a REPL.+--+-- This function only works with packages that have a main module.+--+replPkg :: [Opt] -- ^ Command line Options+ -> FilePath -- ^ Path to ipkg file.+ -> Idris ()+replPkg copts fp = do+ orig <- getIState+ runIO $ checkPkg copts False False fp+ pkgdesc <- runIO $ parseDesc fp -- bzzt, repetition!++ case mergeOptions copts (idris_opts pkgdesc) of+ Left emsg -> ifail emsg+ Right opts -> do+ putIState orig+ dir <- runIO getCurrentDirectory+ runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc+ runMain opts (idris_main pkgdesc)+ runIO $ setCurrentDirectory dir++ where+ toPath n = foldl1' (</>) $ splitOn "." n++ runMain opts (Just mod) = do+ let f = toPath (showCG mod)+ idrisMain ((Filename f) : opts)+ runMain _ Nothing =+ iputStrLn "Can't start REPL: no main module given"++-- --------------------------------------------------------------- [ Cleaning ]++-- | Clean Package build files+cleanPkg :: [Opt] -- ^ Command line options.+ -> FilePath -- ^ Path to ipkg file.+ -> IO ()+cleanPkg copts fp = do+ pkgdesc <- parseDesc fp+ dir <- getCurrentDirectory+ inPkgDir pkgdesc $ do+ clean (makefile pkgdesc)+ mapM_ rmIBC (modules pkgdesc)+ rmIdx (pkgname pkgdesc)+ case execout pkgdesc of+ Nothing -> return ()+ Just s -> rmExe $ dir </> s++-- ------------------------------------------------------ [ Generate IdrisDoc ]+++-- | Generate IdrisDoc for package+-- TODO: Handle case where module does not contain a matching namespace+-- E.g. from prelude.ipkg: IO, Prelude.Chars, Builtins+--+-- Issue number #1572 on the issue tracker+-- https://github.com/idris-lang/Idris-dev/issues/1572+documentPkg :: [Opt] -- ^ Command line options.+ -> FilePath -- ^ Path to ipkg file.+ -> IO ()+documentPkg copts fp = do+ pkgdesc <- parseDesc fp+ cd <- getCurrentDirectory+ let pkgDir = cd </> takeDirectory fp+ outputDir = cd </> pkgname pkgdesc ++ "_doc"+ popts = NoREPL : Verbose : idris_opts pkgdesc+ mods = modules pkgdesc+ fs = map (foldl1' (</>) . splitOn "." . showCG) mods+ setCurrentDirectory $ pkgDir </> sourcedir pkgdesc+ make (makefile pkgdesc)+ setCurrentDirectory pkgDir+ case mergeOptions copts popts of+ Left emsg -> do+ putStrLn emsg+ exitWith (ExitFailure 1)+ Right opts -> do+ let run l = runExceptT . execStateT l+ load [] = return ()+ load (f:fs) = do loadModule f IBC_Building; load fs+ loader = do+ idrisMain opts+ addImportDir (sourcedir pkgdesc)+ load fs+ idrisInstance <- run loader idrisInit+ setCurrentDirectory cd+ case idrisInstance of+ Left err -> do+ putStrLn $ pshow idrisInit err+ exitWith (ExitFailure 1)+ Right ist -> do+ docRes <- generateDocs ist mods outputDir+ case docRes of+ Right _ -> return ()+ Left msg -> do+ putStrLn msg+ exitWith (ExitFailure 1)++-- ------------------------------------------------------------------- [ Test ]++-- | Build a package with a sythesized main function that runs the tests+testPkg :: [Opt] -- ^ Command line options.+ -> FilePath -- ^ Path to ipkg file.+ -> IO ()+testPkg copts fp = do+ pkgdesc <- parseDesc fp+ ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)+ when (and ok) $ do+ m_ist <- inPkgDir pkgdesc $ do+ make (makefile pkgdesc)+ -- Get a temporary file to save the tests' source in+ (tmpn, tmph) <- tempfile ".idr"+ hPutStrLn tmph $+ "module Test_______\n" +++ concat ["import " ++ show m ++ "\n" | m <- modules pkgdesc]+ ++ "namespace Main\n"+ ++ " main : IO ()\n"+ ++ " main = do "+ ++ concat [ show t ++ "\n "+ | t <- idris_tests pkgdesc]+ hClose tmph+ (tmpn', tmph') <- tempfile ""+ hClose tmph'+ let popts = (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc)+ case mergeOptions copts popts of+ Left emsg -> do+ putStrLn emsg+ exitWith (ExitFailure 1)+ Right opts -> do+ m_ist <- idris opts+ rawSystem tmpn' []+ return m_ist+ case m_ist of+ Nothing -> exitWith (ExitFailure 1)+ Just ist -> do+ -- Quit with error code if problem building+ case errSpan ist of+ Just _ -> exitWith (ExitFailure 1)+ _ -> return ()++-- ----------------------------------------------------------- [ Installation ]++-- | Install package+installPkg :: [String] -- ^ Alternate install location+ -> PkgDesc -- ^ iPKG file.+ -> IO ()+installPkg altdests pkgdesc = inPkgDir pkgdesc $ do+ d <- getTargetDir+ let destdir = case altdests of+ [] -> d+ (d':_) -> d'+ case (execout pkgdesc) of+ Nothing -> do+ mapM_ (installIBC destdir (pkgname pkgdesc)) (modules pkgdesc)+ installIdx destdir (pkgname pkgdesc)+ Just o -> return () -- do nothing, keep executable locally, for noe++ mapM_ (installObj destdir (pkgname pkgdesc)) (objs pkgdesc)++-- ---------------------------------------------------------- [ Helper Methods ]+-- Methods for building, testing, installing, and removal of idris+-- packages.++buildMods :: [Opt] -> [Name] -> IO (Maybe IState)+buildMods opts ns = do let f = map (toPath . showCG) ns+ idris (map Filename f ++ opts)+ where toPath n = foldl1' (</>) $ splitOn "." n++testLib :: Bool -> String -> String -> IO Bool+testLib warn p f+ = do d <- getDataDir+ gcc <- getCC+ (tmpf, tmph) <- tempfile ""+ hClose tmph+ let libtest = d </> "rts" </> "libtest.c"+ e <- rawSystem gcc [libtest, "-l" ++ f, "-o", tmpf]+ case e of+ ExitSuccess -> return True+ _ -> do if warn+ then do putStrLn $ "Not building " ++ p +++ " due to missing library " ++ f+ return False+ else fail $ "Missing library " ++ f++rmIBC :: Name -> IO ()+rmIBC m = rmFile $ toIBCFile m++rmIdx :: String -> IO ()+rmIdx p = do let f = pkgIndex p+ ex <- doesFileExist f+ when ex $ rmFile f++rmExe :: String -> IO ()+rmExe p = do+ fn <- return $ if isWindows && not (hasExtension p)+ then addExtension p ".exe" else p+ rmFile fn++toIBCFile (UN n) = str n ++ ".ibc"+toIBCFile (NS n ns) = foldl1' (</>) (reverse (toIBCFile n : map str ns))++installIBC :: String -> String -> Name -> IO ()+installIBC dest p m = do+ let f = toIBCFile m+ let destdir = dest </> p </> getDest m+ putStrLn $ "Installing " ++ f ++ " to " ++ destdir+ createDirectoryIfMissing True destdir+ copyFile f (destdir </> takeFileName f)+ return ()+ where+ getDest (UN n) = ""+ getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))++installIdx :: String -> String -> IO ()+installIdx dest p = do+ let f = pkgIndex p+ let destdir = dest </> p+ putStrLn $ "Installing " ++ f ++ " to " ++ destdir+ createDirectoryIfMissing True destdir+ copyFile f (destdir </> takeFileName f)+ return ()++installObj :: String -> String -> String -> IO ()+installObj dest p o = do+ let destdir = addTrailingPathSeparator (dest </> p)+ putStrLn $ "Installing " ++ o ++ " to " ++ destdir+ createDirectoryIfMissing True destdir+ copyFile o (destdir </> takeFileName o)+ return ()++#ifdef mingw32_HOST_OS+mkDirCmd = "mkdir "+#else+mkDirCmd = "mkdir -p "+#endif++inPkgDir :: PkgDesc -> IO a -> IO a+inPkgDir pkgdesc action =+ do dir <- getCurrentDirectory+ when (sourcedir pkgdesc /= "") $+ do putStrLn $ "Entering directory `" ++ ("." </> sourcedir pkgdesc) ++ "'"+ setCurrentDirectory $ dir </> sourcedir pkgdesc+ res <- action+ when (sourcedir pkgdesc /= "") $+ do putStrLn $ "Leaving directory `" ++ ("." </> sourcedir pkgdesc) ++ "'"+ setCurrentDirectory dir+ return res++-- ------------------------------------------------------- [ Makefile Commands ]+-- | Invoke a Makefile's default target.+make :: Maybe String -> IO ()+make Nothing = return ()+make (Just s) = do rawSystem "make" ["-f", s]+ return ()++-- | Invoke a Makefile's clean target.+clean :: Maybe String -> IO ()+clean Nothing = return ()+clean (Just s) = do rawSystem "make" ["-f", s, "clean"]+ return ()++-- | Merge an option list representing the command line options into+-- those specified for a package description.+--+-- This is not a complete union between the two options sets. First,+-- to prevent important package specified options from being+-- overwritten. Second, the semantics for this merge are not fully+-- defined.+--+-- A discussion for this is on the issue tracker:+-- https://github.com/idris-lang/Idris-dev/issues/1448+--+mergeOptions :: [Opt] -- ^ The command line options+ -> [Opt] -- ^ The package options+ -> Either String [Opt]+mergeOptions copts popts =+ case partitionEithers (map chkOpt (normaliseOpts copts)) of+ ([], copts') -> Right $ copts' ++ popts+ (es, _) -> Left $ genErrMsg es+ where+ normaliseOpts :: [Opt] -> [Opt]+ normaliseOpts = filter filtOpt++ filtOpt :: Opt -> Bool+ filtOpt (PkgBuild _) = False+ filtOpt (PkgInstall _) = False+ filtOpt (PkgClean _) = False+ filtOpt (PkgCheck _) = False+ filtOpt (PkgREPL _) = False+ filtOpt (PkgMkDoc _) = False+ filtOpt (PkgTest _) = False+ filtOpt _ = True++ chkOpt :: Opt -> Either String Opt+ chkOpt o@(OLogging _) = Right o+ chkOpt o@(OLogCats _) = Right o+ chkOpt o@(DefaultTotal) = Right o+ chkOpt o@(DefaultPartial) = Right o+ chkOpt o@(WarnPartial) = Right o+ chkOpt o@(WarnReach) = Right o+ chkOpt o@(IBCSubDir _) = Right o+ chkOpt o@(ImportDir _ ) = Right o+ chkOpt o@(UseCodegen _) = Right o+ chkOpt o = Left (unwords ["\t", show o, "\n"])++ genErrMsg :: [String] -> String+ genErrMsg es = unlines+ [ "Not all command line options can be used to override package options."+ , "\nThe only changeable options are:"+ , "\t--log <lvl>, --total, --warnpartial, --warnreach"+ , "\t--ibcsubdir <path>, -i --idrispath <path>"+ , "\t--logging-categories <cats>"+ , "\nThe options need removing are:"+ , unlines es+ ]++-- --------------------------------------------------------------------- [ EOF ]
+ src/Idris/Package/Common.hs view
@@ -0,0 +1,42 @@+{-|+Module : Idris.Package.Common+Description : Data structures common to all `iPKG` file formats.+Copyright :+License : BSD3+Maintainer : The Idris Community.+-}+module Idris.Package.Common where++import Idris.Core.TT+import Idris.REPL+import Idris.AbsSyntaxTree++-- | Description of an Idris package.+data PkgDesc = PkgDesc {+ pkgname :: String -- ^ Name associated with a package.+ , pkgdeps :: [String] -- ^ List of packages this package depends on.+ , pkgbrief :: Maybe String -- ^ Brief description of the package.+ , pkgversion :: Maybe String -- ^ Version string to associate with the package.+ , pkgreadme :: Maybe String -- ^ Location of the README file.+ , pkglicense :: Maybe String -- ^ Description of the licensing information.+ , pkgauthor :: Maybe String -- ^ Author information.+ , pkgmaintainer :: Maybe String -- ^ Maintainer information.+ , pkghomepage :: Maybe String -- ^ Website associated with the package.+ , pkgsourceloc :: Maybe String -- ^ Location of the source files.+ , pkgbugtracker :: Maybe String -- ^ Location of the project's bug tracker.+ , libdeps :: [String] -- ^ External dependencies.+ , objs :: [String] -- ^ Object files required by the package.+ , makefile :: Maybe String -- ^ Makefile used to build external code. Used as part of the FFI process.+ , idris_opts :: [Opt] -- ^ List of options to give the compiler.+ , sourcedir :: String -- ^ Source directory for Idris files.+ , modules :: [Name] -- ^ Modules provided by the package.+ , idris_main :: Maybe Name -- ^ If an executable in which module can the Main namespace and function be found.+ , execout :: Maybe String -- ^ What to call the executable.+ , idris_tests :: [Name] -- ^ Lists of tests to execute against the package.+ } deriving (Show)++-- | Default settings for package descriptions.+defaultPkg :: PkgDesc+defaultPkg = PkgDesc "" [] Nothing Nothing Nothing Nothing+ Nothing Nothing Nothing Nothing+ Nothing [] [] Nothing [] "" [] Nothing Nothing []
+ src/Idris/Package/Parser.hs view
@@ -0,0 +1,242 @@+{-|+Module : Idris.Package.Parser+Description : `iPKG` file parser and package description information.+Copyright :+License : BSD3+Maintainer : The Idris Community.+-}+{-# LANGUAGE CPP, ConstraintKinds #-}+#if !(MIN_VERSION_base(4,8,0))+{-# LANGUAGE OverlappingInstances #-}+#endif+module Idris.Package.Parser where++import Text.Trifecta hiding (span, charLiteral, natural, symbol, char, string, whiteSpace)+import qualified Text.PrettyPrint.ANSI.Leijen as PP+import Idris.Core.TT+import Idris.REPL+import Idris.AbsSyntaxTree+import Idris.Parser.Helpers hiding (stringLiteral)+import Idris.CmdOptions++import Idris.Package.Common++import Control.Monad.State.Strict+import Control.Applicative+import System.FilePath (takeFileName, isValid)+import Data.Maybe (isNothing, fromJust)+import Data.List (union)++import Util.System++type PParser = StateT PkgDesc IdrisInnerParser++instance HasLastTokenSpan PParser where+ getLastTokenSpan = return Nothing++#if MIN_VERSION_base(4,9,0)+instance {-# OVERLAPPING #-} DeltaParsing PParser where+ line = lift line+ {-# INLINE line #-}+ position = lift position+ {-# INLINE position #-}+ slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s+ {-# INLINE slicedWith #-}+ rend = lift rend+ {-# INLINE rend #-}+ restOfLine = lift restOfLine+ {-# INLINE restOfLine #-}+#endif++#if MIN_VERSION_base(4,8,0)+instance {-# OVERLAPPING #-} TokenParsing PParser where+#else+instance TokenParsing PParser where+#endif+ someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()+++parseDesc :: FilePath -> IO PkgDesc+parseDesc fp = do+ p <- readFile fp+ case runparser pPkg defaultPkg fp p of+ Failure (ErrInfo err _) -> fail (show $ PP.plain err)+ Success x -> return x++pPkg :: PParser PkgDesc+pPkg = do+ reserved "package"+ p <- filename+ st <- get+ put (st { pkgname = p })+ some pClause+ st <- get+ eof+ return st+++-- | Parses a filename.+-- |+-- | Treated for now as an identifier or a double-quoted string.+filename :: (MonadicParsing m, HasLastTokenSpan m) => m String+filename = (do+ filename <- token $+ -- Treat a double-quoted string as a filename to support spaces.+ -- This also moves away from tying filenames to identifiers, so+ -- it will also accept hyphens+ -- (https://github.com/idris-lang/Idris-dev/issues/2721)+ stringLiteral+ <|>+ -- Through at least version 0.9.19.1, IPKG executable values were+ -- possibly namespaced identifiers, like foo.bar.baz.+ show <$> fst <$> iName []+ case filenameErrorMessage filename of+ Just errorMessage -> fail errorMessage+ Nothing -> return filename)+ <?> "filename"+ where+ -- TODO: Report failing span better! We could lookAhead,+ -- or do something with DeltaParsing?+ filenameErrorMessage :: FilePath -> Maybe String+ filenameErrorMessage path = either Just (const Nothing) $ do+ checkEmpty path+ checkValid path+ checkNoDirectoryComponent path+ where+ checkThat ok message =+ if ok then Right () else Left message++ checkEmpty path =+ checkThat (path /= "") "filename must not be empty"++ checkValid path =+ checkThat (System.FilePath.isValid path)+ "filename must contain only valid characters"++ checkNoDirectoryComponent path =+ checkThat (path == takeFileName path)+ "filename must contain no directory component"+++pClause :: PParser ()+pClause = do reserved "executable"; lchar '=';+ exec <- filename+ st <- get+ put (st { execout = Just exec })++ <|> do reserved "main"; lchar '=';+ main <- fst <$> iName []+ st <- get+ put (st { idris_main = Just main })++ <|> do reserved "sourcedir"; lchar '=';+ src <- fst <$> identifier+ st <- get+ put (st { sourcedir = src })++ <|> do reserved "opts"; lchar '=';+ opts <- stringLiteral+ st <- get+ let args = pureArgParser (words opts)+ put (st { idris_opts = args ++ idris_opts st })++ <|> do reserved "pkgs"; lchar '=';+ ps <- sepBy1 (fst <$> identifier) (lchar ',')+ st <- get+ let pkgs = pureArgParser $ concatMap (\x -> ["-p", x]) ps++ put (st { pkgdeps = ps `union` (pkgdeps st)+ , idris_opts = pkgs ++ idris_opts st})++ <|> do reserved "modules"; lchar '=';+ ms <- sepBy1 (fst <$> iName []) (lchar ',')+ st <- get+ put (st { modules = modules st ++ ms })++ <|> do reserved "libs"; lchar '=';+ ls <- sepBy1 (fst <$> identifier) (lchar ',')+ st <- get+ put (st { libdeps = libdeps st ++ ls })++ <|> do reserved "objs"; lchar '=';+ ls <- sepBy1 (fst <$> identifier) (lchar ',')+ st <- get+ put (st { objs = objs st ++ ls })++ <|> do reserved "makefile"; lchar '=';+ mk <- fst <$> iName []+ st <- get+ put (st { makefile = Just (show mk) })++ <|> do reserved "tests"; lchar '=';+ ts <- sepBy1 (fst <$> iName []) (lchar ',')+ st <- get+ put st { idris_tests = idris_tests st ++ ts }++ <|> do reserved "version"+ lchar '='+ vStr <- many (satisfy (not . isEol))+ eol+ someSpace+ st <- get+ put st {pkgversion = Just vStr}++ <|> do reserved "readme"+ lchar '='+ rme <- many (satisfy (not . isEol))+ eol+ someSpace+ st <- get+ put (st { pkgreadme = Just rme })++ <|> do reserved "license"+ lchar '='+ lStr <- many (satisfy (not . isEol))+ eol+ st <- get+ put st {pkglicense = Just lStr}++ <|> do reserved "homepage"+ lchar '='+ www <- many (satisfy (not . isEol))+ eol+ someSpace+ st <- get+ put st {pkghomepage = Just www}++ <|> do reserved "sourceloc"+ lchar '='+ srcpage <- many (satisfy (not . isEol))+ eol+ someSpace+ st <- get+ put st {pkgsourceloc = Just srcpage}++ <|> do reserved "bugtracker"+ lchar '='+ src <- many (satisfy (not . isEol))+ eol+ someSpace+ st <- get+ put st {pkgbugtracker = Just src}++ <|> do reserved "brief"+ lchar '='+ brief <- stringLiteral+ st <- get+ someSpace+ put st {pkgbrief = Just brief}++ <|> do reserved "author"; lchar '=';+ author <- many (satisfy (not . isEol))+ eol+ someSpace+ st <- get+ put st {pkgauthor = Just author}++ <|> do reserved "maintainer"; lchar '=';+ maintainer <- many (satisfy (not . isEol))+ eol+ someSpace+ st <- get+ put st {pkgmaintainer = Just maintainer}
src/Idris/Parser.hs view
@@ -1116,7 +1116,9 @@ @ -} rhs :: SyntaxInfo -> Name -> IdrisParser PTerm-rhs syn n = do lchar '='; expr syn+rhs syn n = do lchar '='+ indentPropHolds gtProp+ expr syn <|> do symbol "?="; fc <- getFC name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
− src/Pkg/PParser.hs
@@ -1,265 +0,0 @@-{-|-Module : Pkg.PParser-Description : `iPKG` file parser and package description information.-Copyright :-License : BSD3-Maintainer : The Idris Community.--}-{-# LANGUAGE CPP, ConstraintKinds #-}-#if !(MIN_VERSION_base(4,8,0))-{-# LANGUAGE OverlappingInstances #-}-#endif-module Pkg.PParser where--import Text.Trifecta hiding (span, charLiteral, natural, symbol, char, string, whiteSpace)-import qualified Text.PrettyPrint.ANSI.Leijen as PP-import Idris.Core.TT-import Idris.REPL-import Idris.AbsSyntaxTree-import Idris.Parser.Helpers hiding (stringLiteral)-import Idris.CmdOptions--import Control.Monad.State.Strict-import Control.Applicative-import System.FilePath (takeFileName, isValid)-import Data.Maybe (isNothing, fromJust)--import Util.System--type PParser = StateT PkgDesc IdrisInnerParser--data PkgDesc = PkgDesc {- pkgname :: String -- ^ Name associated with a package.- , pkgbrief :: Maybe String -- ^ Brief description of the package.- , pkgversion :: Maybe String -- ^ Version string to associate with the package.- , pkgreadme :: Maybe String -- ^ Location of the README file.- , pkglicense :: Maybe String -- ^ Description of the licensing information.- , pkgauthor :: Maybe String -- ^ Author information.- , pkgmaintainer :: Maybe String -- ^ Maintainer information.- , pkghomepage :: Maybe String -- ^ Website associated with the package.- , pkgsourceloc :: Maybe String -- ^ Location of the source files.- , pkgbugtracker :: Maybe String -- ^ Location of the project's bug tracker.- , libdeps :: [String] -- ^ External dependencies.- , objs :: [String] -- ^ Object files required by the package.- , makefile :: Maybe String -- ^ Makefile used to build external code. Used as part of the FFI process.- , idris_opts :: [Opt] -- ^ List of options to give the compiler.- , sourcedir :: String -- ^ Source directory for Idris files.- , modules :: [Name] -- ^ Modules provided by the package.- , idris_main :: Name -- ^ If an executable in which module can the Main namespace and function be found.- , execout :: Maybe String -- ^ What to call the executable.- , idris_tests :: [Name] -- ^ Lists of tests to execute against the package.- } deriving (Show)---- | Default settings for package descriptions.-defaultPkg :: PkgDesc-defaultPkg = PkgDesc "" Nothing Nothing Nothing Nothing- Nothing Nothing Nothing Nothing- Nothing [] [] Nothing [] "" [] (sUN "") Nothing []--instance HasLastTokenSpan PParser where- getLastTokenSpan = return Nothing--#if MIN_VERSION_base(4,9,0)-instance {-# OVERLAPPING #-} DeltaParsing PParser where- line = lift line- {-# INLINE line #-}- position = lift position- {-# INLINE position #-}- slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s- {-# INLINE slicedWith #-}- rend = lift rend- {-# INLINE rend #-}- restOfLine = lift restOfLine- {-# INLINE restOfLine #-}-#endif--#if MIN_VERSION_base(4,8,0)-instance {-# OVERLAPPING #-} TokenParsing PParser where-#else-instance TokenParsing PParser where-#endif- someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()---parseDesc :: FilePath -> IO PkgDesc-parseDesc fp = do- p <- readFile fp- case runparser pPkg defaultPkg fp p of- Failure (ErrInfo err _) -> fail (show $ PP.plain err)- Success x -> return x--pPkg :: PParser PkgDesc-pPkg = do- reserved "package"- p <- filename- st <- get- put (st { pkgname = p })- some pClause- st <- get- eof- return st----- | Parses a filename.--- |--- | Treated for now as an identifier or a double-quoted string.-filename :: (MonadicParsing m, HasLastTokenSpan m) => m String-filename = (do- filename <- token $- -- Treat a double-quoted string as a filename to support spaces.- -- This also moves away from tying filenames to identifiers, so- -- it will also accept hyphens- -- (https://github.com/idris-lang/Idris-dev/issues/2721)- stringLiteral- <|>- -- Through at least version 0.9.19.1, IPKG executable values were- -- possibly namespaced identifiers, like foo.bar.baz.- show <$> fst <$> iName []- case filenameErrorMessage filename of- Just errorMessage -> fail errorMessage- Nothing -> return filename)- <?> "filename"- where- -- TODO: Report failing span better! We could lookAhead,- -- or do something with DeltaParsing?- filenameErrorMessage :: FilePath -> Maybe String- filenameErrorMessage path = either Just (const Nothing) $ do- checkEmpty path- checkValid path- checkNoDirectoryComponent path- where- checkThat ok message =- if ok then Right () else Left message-- checkEmpty path =- checkThat (path /= "") "filename must not be empty"-- checkValid path =- checkThat (System.FilePath.isValid path)- "filename must contain only valid characters"-- checkNoDirectoryComponent path =- checkThat (path == takeFileName path)- "filename must contain no directory component"---pClause :: PParser ()-pClause = do reserved "executable"; lchar '=';- exec <- filename- st <- get- put (st { execout = Just exec })-- <|> do reserved "main"; lchar '=';- main <- fst <$> iName []- st <- get- put (st { idris_main = main })-- <|> do reserved "sourcedir"; lchar '=';- src <- fst <$> identifier- st <- get- put (st { sourcedir = src })-- <|> do reserved "opts"; lchar '=';- opts <- stringLiteral- st <- get- let args = pureArgParser (words opts)- put (st { idris_opts = args ++ idris_opts st })-- <|> do reserved "pkgs"; lchar '=';- ps <- sepBy1 (fst <$> identifier) (lchar ',')- st <- get- let pkgs = pureArgParser $ concatMap (\x -> ["-p", x]) ps- put (st {idris_opts = pkgs ++ idris_opts st})-- <|> do reserved "modules"; lchar '=';- ms <- sepBy1 (fst <$> iName []) (lchar ',')- st <- get- put (st { modules = modules st ++ ms })-- <|> do reserved "libs"; lchar '=';- ls <- sepBy1 (fst <$> identifier) (lchar ',')- st <- get- put (st { libdeps = libdeps st ++ ls })-- <|> do reserved "objs"; lchar '=';- ls <- sepBy1 (fst <$> identifier) (lchar ',')- st <- get- put (st { objs = libdeps st ++ ls })-- <|> do reserved "makefile"; lchar '=';- mk <- fst <$> iName []- st <- get- put (st { makefile = Just (show mk) })-- <|> do reserved "tests"; lchar '=';- ts <- sepBy1 (fst <$> iName []) (lchar ',')- st <- get- put st { idris_tests = idris_tests st ++ ts }-- <|> do reserved "version"- lchar '='- vStr <- many (satisfy (not . isEol))- eol- someSpace- st <- get- put st {pkgversion = Just vStr}-- <|> do reserved "readme"- lchar '='- rme <- many (satisfy (not . isEol))- eol- someSpace- st <- get- put (st { pkgreadme = Just rme })-- <|> do reserved "license"- lchar '='- lStr <- many (satisfy (not . isEol))- eol- st <- get- put st {pkglicense = Just lStr}-- <|> do reserved "homepage"- lchar '='- www <- many (satisfy (not . isEol))- eol- someSpace- st <- get- put st {pkghomepage = Just www}-- <|> do reserved "sourceloc"- lchar '='- srcpage <- many (satisfy (not . isEol))- eol- someSpace- st <- get- put st {pkgsourceloc = Just srcpage}-- <|> do reserved "bugtracker"- lchar '='- src <- many (satisfy (not . isEol))- eol- someSpace- st <- get- put st {pkgbugtracker = Just src}-- <|> do reserved "brief"- lchar '='- brief <- stringLiteral- st <- get- someSpace- put st {pkgbrief = Just brief}-- <|> do reserved "author"; lchar '=';- author <- many (satisfy (not . isEol))- eol- someSpace- st <- get- put st {pkgauthor = Just author}-- <|> do reserved "maintainer"; lchar '=';- maintainer <- many (satisfy (not . isEol))- eol- someSpace- st <- get- put st {pkgmaintainer = Just maintainer}
− src/Pkg/Package.hs
@@ -1,437 +0,0 @@-{-|-Module : Pkg.Package-Description : Functionality for working with Idris packages.-Copyright :-License : BSD3-Maintainer : The Idris Community.--}-{-# LANGUAGE CPP #-}-module Pkg.Package where--import System.Process-import System.Directory-import System.Exit-import System.IO-import System.FilePath ((</>), addTrailingPathSeparator, takeFileName,- takeDirectory, normalise, addExtension, hasExtension)-import System.Directory (createDirectoryIfMissing, copyFile)--import Util.System--import Control.Monad-import Control.Monad.Trans.State.Strict (execStateT)-import Control.Monad.Trans.Except (runExceptT)--import Data.List-import Data.List.Split(splitOn)-import Data.Maybe(fromMaybe)-import Data.Either(partitionEithers)--import Idris.Core.TT-import Idris.REPL-import Idris.Parser (loadModule)-import Idris.Output (pshow)-import Idris.AbsSyntax-import Idris.IdrisDoc-import Idris.IBC-import Idris.Output-import Idris.Imports-import Idris.Error (ifail)--import Pkg.PParser--import IRTS.System---- To build a package:--- * read the package description--- * check all the library dependencies exist--- * invoke the makefile if there is one--- * invoke idris on each module, with idris_opts--- * install everything into datadir/pname, if install flag is set---- --------------------------------------------------------- [ Build Packages ]---- | Run the package through the idris compiler.-buildPkg :: [Opt] -- ^ Command line options- -> Bool -- ^ Provide Warnings- -> (Bool, FilePath) -- ^ (Should we install, Location of iPKG file)- -> IO ()-buildPkg copts warnonly (install, fp) = do- pkgdesc <- parseDesc fp- dir <- getCurrentDirectory- let idx = PkgIndex (pkgIndex (pkgname pkgdesc))- oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)- when (and oks) $ do- m_ist <- inPkgDir pkgdesc $ do-- make (makefile pkgdesc)- case (execout pkgdesc) of- Nothing -> do- case mergeOptions copts (idx : NoREPL : Verbose : idris_opts pkgdesc) of- Left emsg -> do- putStrLn emsg- exitWith (ExitFailure 1)- Right opts -> buildMods opts (modules pkgdesc)- Just o -> do- let exec = dir </> o- case mergeOptions copts (idx : NoREPL : Verbose : Output exec : idris_opts pkgdesc) of- Left emsg -> do- putStrLn emsg- exitWith (ExitFailure 1)- Right opts -> buildMods opts [idris_main pkgdesc]- case m_ist of- Nothing -> exitWith (ExitFailure 1)- Just ist -> do- -- Quit with error code if there was a problem- case errSpan ist of- Just _ -> exitWith (ExitFailure 1)- _ -> return ()- when install $ installPkg (opt getIBCSubDir copts) pkgdesc---- --------------------------------------------------------- [ Check Packages ]---- | Type check packages only------ This differs from build in that executables are not built, if the--- package contains an executable.-checkPkg :: [Opt] -- ^ Command line Options- -> Bool -- ^ Show Warnings- -> Bool -- ^ quit on failure- -> FilePath -- ^ Path to ipkg file.- -> IO ()-checkPkg copts warnonly quit fpath = do- pkgdesc <- parseDesc fpath- oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)- when (and oks) $ do- res <- inPkgDir pkgdesc $ do- make (makefile pkgdesc)-- case mergeOptions copts (NoREPL : Verbose : idris_opts pkgdesc) of- Left emsg -> do- putStrLn emsg- exitWith (ExitFailure 1)- Right opts -> do- buildMods opts (modules pkgdesc)- when quit $ case res of- Nothing -> exitWith (ExitFailure 1)- Just res' -> do- case errSpan res' of- Just _ -> exitWith (ExitFailure 1)- _ -> return ()---- ------------------------------------------------------------------- [ REPL ]---- | Check a package and start a REPL.------ This function only works with packages that have a main module.----replPkg :: [Opt] -- ^ Command line Options- -> FilePath -- ^ Path to ipkg file.- -> Idris ()-replPkg copts fp = do- orig <- getIState- runIO $ checkPkg copts False False fp- pkgdesc <- runIO $ parseDesc fp -- bzzt, repetition!-- case mergeOptions copts (idris_opts pkgdesc) of- Left emsg -> ifail emsg- Right opts -> do- let mod = idris_main pkgdesc- let f = toPath (showCG mod)- putIState orig- dir <- runIO getCurrentDirectory- runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc-- if (f /= "")- then idrisMain ((Filename f) : opts)- else iputStrLn "Can't start REPL: no main module given"- runIO $ setCurrentDirectory dir-- where- toPath n = foldl1' (</>) $ splitOn "." n---- --------------------------------------------------------------- [ Cleaning ]---- | Clean Package build files-cleanPkg :: [Opt] -- ^ Command line options.- -> FilePath -- ^ Path to ipkg file.- -> IO ()-cleanPkg copts fp = do- pkgdesc <- parseDesc fp- dir <- getCurrentDirectory- inPkgDir pkgdesc $ do- clean (makefile pkgdesc)- mapM_ rmIBC (modules pkgdesc)- rmIdx (pkgname pkgdesc)- case execout pkgdesc of- Nothing -> return ()- Just s -> rmExe $ dir </> s---- ------------------------------------------------------ [ Generate IdrisDoc ]----- | Generate IdrisDoc for package--- TODO: Handle case where module does not contain a matching namespace--- E.g. from prelude.ipkg: IO, Prelude.Chars, Builtins------ Issue number #1572 on the issue tracker--- https://github.com/idris-lang/Idris-dev/issues/1572-documentPkg :: [Opt] -- ^ Command line options.- -> FilePath -- ^ Path to ipkg file.- -> IO ()-documentPkg copts fp = do- pkgdesc <- parseDesc fp- cd <- getCurrentDirectory- let pkgDir = cd </> takeDirectory fp- outputDir = cd </> pkgname pkgdesc ++ "_doc"- popts = NoREPL : Verbose : idris_opts pkgdesc- mods = modules pkgdesc- fs = map (foldl1' (</>) . splitOn "." . showCG) mods- setCurrentDirectory $ pkgDir </> sourcedir pkgdesc- make (makefile pkgdesc)- setCurrentDirectory pkgDir- case mergeOptions copts popts of- Left emsg -> do- putStrLn emsg- exitWith (ExitFailure 1)- Right opts -> do- let run l = runExceptT . execStateT l- load [] = return ()- load (f:fs) = do loadModule f IBC_Building; load fs- loader = do- idrisMain opts- addImportDir (sourcedir pkgdesc)- load fs- idrisInstance <- run loader idrisInit- setCurrentDirectory cd- case idrisInstance of- Left err -> do- putStrLn $ pshow idrisInit err- exitWith (ExitFailure 1)- Right ist -> do- docRes <- generateDocs ist mods outputDir- case docRes of- Right _ -> return ()- Left msg -> do- putStrLn msg- exitWith (ExitFailure 1)---- ------------------------------------------------------------------- [ Test ]---- | Build a package with a sythesized main function that runs the tests-testPkg :: [Opt] -- ^ Command line options.- -> FilePath -- ^ Path to ipkg file.- -> IO ()-testPkg copts fp = do- pkgdesc <- parseDesc fp- ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)- when (and ok) $ do- m_ist <- inPkgDir pkgdesc $ do- make (makefile pkgdesc)- -- Get a temporary file to save the tests' source in- (tmpn, tmph) <- tempfile ".idr"- hPutStrLn tmph $- "module Test_______\n" ++- concat ["import " ++ show m ++ "\n" | m <- modules pkgdesc]- ++ "namespace Main\n"- ++ " main : IO ()\n"- ++ " main = do "- ++ concat [ show t ++ "\n "- | t <- idris_tests pkgdesc]- hClose tmph- (tmpn', tmph') <- tempfile ""- hClose tmph'- let popts = (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc)- case mergeOptions copts popts of- Left emsg -> do- putStrLn emsg- exitWith (ExitFailure 1)- Right opts -> do- m_ist <- idris opts- rawSystem tmpn' []- return m_ist- case m_ist of- Nothing -> exitWith (ExitFailure 1)- Just ist -> do- -- Quit with error code if problem building- case errSpan ist of- Just _ -> exitWith (ExitFailure 1)- _ -> return ()---- ----------------------------------------------------------- [ Installation ]---- | Install package-installPkg :: [String] -- ^ Alternate install location- -> PkgDesc -- ^ iPKG file.- -> IO ()-installPkg altdests pkgdesc = inPkgDir pkgdesc $ do- d <- getTargetDir- let destdir = case altdests of- [] -> d- (d':_) -> d'- case (execout pkgdesc) of- Nothing -> do- mapM_ (installIBC destdir (pkgname pkgdesc)) (modules pkgdesc)- installIdx destdir (pkgname pkgdesc)- Just o -> return () -- do nothing, keep executable locally, for noe-- mapM_ (installObj destdir (pkgname pkgdesc)) (objs pkgdesc)---- ---------------------------------------------------------- [ Helper Methods ]--- Methods for building, testing, installing, and removal of idris--- packages.--buildMods :: [Opt] -> [Name] -> IO (Maybe IState)-buildMods opts ns = do let f = map (toPath . showCG) ns- idris (map Filename f ++ opts)- where toPath n = foldl1' (</>) $ splitOn "." n--testLib :: Bool -> String -> String -> IO Bool-testLib warn p f- = do d <- getDataDir- gcc <- getCC- (tmpf, tmph) <- tempfile ""- hClose tmph- let libtest = d </> "rts" </> "libtest.c"- e <- rawSystem gcc [libtest, "-l" ++ f, "-o", tmpf]- case e of- ExitSuccess -> return True- _ -> do if warn- then do putStrLn $ "Not building " ++ p ++- " due to missing library " ++ f- return False- else fail $ "Missing library " ++ f--rmIBC :: Name -> IO ()-rmIBC m = rmFile $ toIBCFile m--rmIdx :: String -> IO ()-rmIdx p = do let f = pkgIndex p- ex <- doesFileExist f- when ex $ rmFile f--rmExe :: String -> IO ()-rmExe p = do- fn <- return $ if isWindows && not (hasExtension p)- then addExtension p ".exe" else p- rmFile fn--toIBCFile (UN n) = str n ++ ".ibc"-toIBCFile (NS n ns) = foldl1' (</>) (reverse (toIBCFile n : map str ns))--installIBC :: String -> String -> Name -> IO ()-installIBC dest p m = do- let f = toIBCFile m- let destdir = dest </> p </> getDest m- putStrLn $ "Installing " ++ f ++ " to " ++ destdir- createDirectoryIfMissing True destdir- copyFile f (destdir </> takeFileName f)- return ()- where- getDest (UN n) = ""- getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))--installIdx :: String -> String -> IO ()-installIdx dest p = do- let f = pkgIndex p- let destdir = dest </> p- putStrLn $ "Installing " ++ f ++ " to " ++ destdir- createDirectoryIfMissing True destdir- copyFile f (destdir </> takeFileName f)- return ()--installObj :: String -> String -> String -> IO ()-installObj dest p o = do- let destdir = addTrailingPathSeparator (dest </> p)- putStrLn $ "Installing " ++ o ++ " to " ++ destdir- createDirectoryIfMissing True destdir- copyFile o (destdir </> takeFileName o)- return ()--#ifdef mingw32_HOST_OS-mkDirCmd = "mkdir "-#else-mkDirCmd = "mkdir -p "-#endif--inPkgDir :: PkgDesc -> IO a -> IO a-inPkgDir pkgdesc action =- do dir <- getCurrentDirectory- when (sourcedir pkgdesc /= "") $- do putStrLn $ "Entering directory `" ++ ("." </> sourcedir pkgdesc) ++ "'"- setCurrentDirectory $ dir </> sourcedir pkgdesc- res <- action- when (sourcedir pkgdesc /= "") $- do putStrLn $ "Leaving directory `" ++ ("." </> sourcedir pkgdesc) ++ "'"- setCurrentDirectory dir- return res---- ------------------------------------------------------- [ Makefile Commands ]--- | Invoke a Makefile's default target.-make :: Maybe String -> IO ()-make Nothing = return ()-make (Just s) = do rawSystem "make" ["-f", s]- return ()---- | Invoke a Makefile's clean target.-clean :: Maybe String -> IO ()-clean Nothing = return ()-clean (Just s) = do rawSystem "make" ["-f", s, "clean"]- return ()---- | Merge an option list representing the command line options into--- those specified for a package description.------ This is not a complete union between the two options sets. First,--- to prevent important package specified options from being--- overwritten. Second, the semantics for this merge are not fully--- defined.------ A discussion for this is on the issue tracker:--- https://github.com/idris-lang/Idris-dev/issues/1448----mergeOptions :: [Opt] -- ^ The command line options- -> [Opt] -- ^ The package options- -> Either String [Opt]-mergeOptions copts popts =- case partitionEithers (map chkOpt (normaliseOpts copts)) of- ([], copts') -> Right $ copts' ++ popts- (es, _) -> Left $ genErrMsg es- where- normaliseOpts :: [Opt] -> [Opt]- normaliseOpts = filter filtOpt-- filtOpt :: Opt -> Bool- filtOpt (PkgBuild _) = False- filtOpt (PkgInstall _) = False- filtOpt (PkgClean _) = False- filtOpt (PkgCheck _) = False- filtOpt (PkgREPL _) = False- filtOpt (PkgMkDoc _) = False- filtOpt (PkgTest _) = False- filtOpt _ = True-- chkOpt :: Opt -> Either String Opt- chkOpt o@(OLogging _) = Right o- chkOpt o@(OLogCats _) = Right o- chkOpt o@(DefaultTotal) = Right o- chkOpt o@(DefaultPartial) = Right o- chkOpt o@(WarnPartial) = Right o- chkOpt o@(WarnReach) = Right o- chkOpt o@(IBCSubDir _) = Right o- chkOpt o@(ImportDir _ ) = Right o- chkOpt o@(UseCodegen _) = Right o- chkOpt o = Left (unwords ["\t", show o, "\n"])-- genErrMsg :: [String] -> String- genErrMsg es = unlines- [ "Not all command line options can be used to override package options."- , "\nThe only changeable options are:"- , "\t--log <lvl>, --total, --warnpartial, --warnreach"- , "\t--ibcsubdir <path>, -i --idrispath <path>"- , "\t--logging-categories <cats>"- , "\nThe options need removing are:"- , unlines es- ]---- --------------------------------------------------------------------- [ EOF ]
src/Util/Net.hs view
@@ -19,10 +19,10 @@ localhost <- inet_addr "127.0.0.1" bracketOnError (socket AF_INET Stream proto)- (sClose)+ (close) (\sock -> do setSocketOption sock ReuseAddr 1- bindSocket sock (SockAddrInet port localhost)+ bind sock (SockAddrInet port localhost) listen sock maxListenQueue return sock )@@ -32,10 +32,10 @@ localhost <- inet_addr "127.0.0.1" bracketOnError (socket AF_INET Stream proto)- (sClose)+ (close) (\sock -> do setSocketOption sock ReuseAddr 1- bindSocket sock (SockAddrInet aNY_PORT localhost)+ bind sock (SockAddrInet aNY_PORT localhost) listen sock maxListenQueue port <- socketPort sock return (sock, port)
stack.yaml view
@@ -1,4 +1,4 @@-resolver: lts-6.5+resolver: lts-6.9 packages: - location: .
− test/Makefile
@@ -1,34 +0,0 @@-.PHONY: test test_js time update diff distclean $(TESTS)--TESTS = $(sort $(patsubst %/,%.test,$(wildcard */)))--test: $(TESTS)---info: runtest- @./runtest all--%.test: runtest- @./runtest $(patsubst %.test,%,$@) -q--test_js: runtest- @./runtest without tutorial007 sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 basic007 basic011 ffi006 ffi007 ffi008 primitives005 primitives006 views003 opts --codegen node--update: runtest- @./runtest all -u--diff: runtest- @./runtest all -d--time: runtest- @./runtest all -t--distclean:- @rm runtest- @rm -f *~- @rm -f */output---runtest:- @ghc --make runtest.hs- @rm runtest.o runtest.hi
+ test/TestData.hs view
@@ -0,0 +1,307 @@+module TestData where++import Data.IntMap as IMap+import Data.Map.Strict as Map+import Data.Set as Set++data Codegen = C | JS deriving (Show, Eq, Ord)+type Index = Int+data CompatCodegen = ANY | C_CG | NODE_CG | NONE++-- A TestFamily groups tests that share the same theme+data TestFamily = TestFamily {+ -- A shorter lowcase name to use in filenames+ id :: String,+ -- A proper name for the test family that will be displayed+ name :: String,+ -- A map of test metadata:+ -- - The key is the index (>=1 && <1000)+ -- - The value is the set of compatible code generators,+ -- or Nothing if the test doesn't depend on a code generator+ tests :: IntMap (Maybe (Set Codegen))+} deriving (Show)++toCodegenSet :: CompatCodegen -> Maybe (Set Codegen)+toCodegenSet compatCodegen = fmap Set.fromList mList where+ mList = case compatCodegen of+ ANY -> Just [ C, JS ]+ C_CG -> Just [ C ]+ NODE_CG -> Just [ JS ]+ NONE -> Nothing++testFamilies :: [TestFamily]+testFamilies = fmap instantiate testFamiliesData where+ instantiate (id, name, testsData) = TestFamily id name tests where+ tests = IMap.fromList (fmap makeSetCodegen testsData)+ makeSetCodegen (index, codegens) = (index, toCodegenSet codegens)++testFamiliesForCodegen :: Codegen -> [TestFamily]+testFamiliesForCodegen codegen =+ fmap (\testFamily -> testFamily {tests = IMap.filter f (tests testFamily)})+ testFamilies+ where+ f mCodegens = case mCodegens of+ Just codegens -> Set.member codegen codegens+ Nothing -> True++-- The data to instanciate testFamilies+-- The first column is the id+-- The second column is the proper name (the prefix of the subfolders)+-- The third column is the data for each test+testFamiliesData :: [(String, String, [(Index, CompatCodegen)])]+testFamiliesData = [+ ("base", "Base",+ [ ( 1, C_CG )]),+ ("basic", "Basic",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY ),+ ( 6, ANY ),+ ( 7, C_CG ),+ ( 8, ANY ),+ ( 9, ANY ),+ ( 10, ANY ),+ ( 11, C_CG ),+ ( 12, ANY ),+ ( 13, ANY ),+ ( 14, ANY ),+ ( 15, ANY ),+ ( 16, ANY ),+ ( 17, ANY ),+ ( 18, ANY )]),+ ("bignum", "Bignum",+ [ ( 1, ANY ),+ ( 2, ANY )]),+ ("bounded", "Bounded",+ [ ( 1, ANY )]),+ ("corecords", "Corecords",+ [ ( 1, ANY ),+ ( 2, ANY )]),+ ("delab", "De-elaboration",+ [ ( 1, ANY )]),+ ("directives", "Directives",+ [ ( 1, ANY ),+ ( 2, ANY )]),+ ("disambig", "Disambiguation",+ [ ( 2, ANY )]),+ ("docs", "Documentation",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY )]),+ ("dsl", "DSL",+ [ ( 1, ANY ),+ ( 2, C_CG ),+ ( 3, ANY ),+ ( 4, ANY )]),+ ("effects", "Effects",+ [ ( 1, C_CG ),+ ( 2, C_CG ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY )]),+ ("error", "Errors",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY ),+ ( 6, ANY ),+ ( 7, ANY ),+ ( 8, ANY )]),+ ("ffi", "FFI",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY ),+ ( 6, C_CG ),+ ( 7, C_CG ),+ ( 8, C_CG )]),+ ("folding", "Folding",+ [ ( 1, ANY )]),+ ("idrisdoc", "Idris documentation",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY ),+ ( 6, ANY ),+ ( 7, ANY ),+ ( 8, ANY ),+ ( 9, ANY )]),+ ("interactive", "Interactive editing",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY ),+ ( 6, ANY ),+ ( 7, ANY ),+ ( 8, ANY ),+ ( 9, ANY ),+ ( 10, ANY ),+ ( 11, ANY ),+ ( 12, ANY ),+ ( 13, ANY )]),+ ("interfaces", "Interfaces",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY ),+ ( 6, ANY )]),+ ("io", "IO monad",+ [ ( 1, C_CG ),+ ( 2, ANY ),+ ( 3, C_CG )]),+ ("layout", "Layout",+ [ ( 1, ANY )]),+ ("literate", "Literate programming",+ [ ( 1, ANY )]),+ ("meta", "Meta-programming",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY )]),+ ("pkg", "Packages",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY ),+ ( 6, ANY )]),+ ("prelude", "Prelude",+ [ ( 1, ANY )]),+ ("primitives", "Primitive types",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 5, C_CG ),+ ( 6, C_CG )]),+ ("proof", "Theorem proving",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY ),+ ( 6, ANY ),+ ( 7, ANY ),+ ( 8, ANY ),+ ( 9, ANY ),+ ( 10, ANY ),+ ( 11, ANY )]),+ ("proofsearch", "Proof search",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY )]),+ ("pruviloj", "Pruviloj",+ [ ( 1, ANY )]),+ ("quasiquote", "Quasiquotations",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY ),+ ( 6, ANY )]),+ ("records", "Records",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY )]),+ ("reg", "Regressions",+ [ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY ),+ ( 6, ANY ),+ ( 7, ANY ),+ ( 10, ANY ),+ ( 13, ANY ),+ ( 16, ANY ),+ ( 17, ANY ),+ ( 18, ANY ),+ ( 20, ANY ),+ ( 23, ANY ),+ ( 24, ANY ),+ ( 25, ANY ),+ ( 27, ANY ),+ ( 28, ANY ),+ ( 29, C_CG ),+ ( 31, ANY ),+ ( 32, ANY ),+ ( 34, ANY ),+ ( 35, ANY ),+ ( 39, ANY ),+ ( 40, ANY ),+ ( 41, ANY ),+ ( 42, ANY ),+ ( 44, ANY ),+ ( 45, ANY ),+ ( 48, ANY ),+ ( 49, ANY ),+ ( 50, ANY ),+ ( 52, C_CG ),+ ( 54, ANY ),+ ( 55, ANY ),+ ( 56, ANY ),+ ( 67, ANY ),+ ( 68, ANY ),+ ( 69, ANY ),+ ( 70, ANY ),+ ( 72, ANY ),+ ( 75, ANY )]),+ ("regression", "Regression (loner)",+ [ ( 1 , ANY )]),+ ("sourceLocation", "Source location",+ [ ( 1 , ANY )]),+ ("sugar", "Syntactic sugar",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, C_CG ),+ ( 5, ANY )]),+ ("syntax", "Syntax extensions",+ [ ( 1, ANY ),+ ( 2, ANY )]),+ ("tactics", "Tactics",+ [ ( 1, ANY )]),+ ("totality", "Totality checking",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY ),+ ( 6, ANY ),+ ( 7, ANY ),+ ( 8, ANY ),+ ( 9, ANY ),+ ( 10, ANY ),+ ( 11, ANY ),+ ( 12, ANY ),+ ( 13, ANY ),+ ( 14, ANY ),+ ( 15, ANY )]),+ ("tutorial", "Tutorial examples",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY ),+ ( 4, ANY ),+ ( 5, ANY ),+ ( 6, ANY ),+ ( 7, C_CG )]),+ ("unique", "Uniqueness types",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, ANY )]),+ ("universes", "Universes",+ [ ( 1, ANY ),+ ( 2, ANY )]),+ ("views", "Views",+ [ ( 1, ANY ),+ ( 2, ANY ),+ ( 3, C_CG )])]
+ test/TestRun.hs view
@@ -0,0 +1,139 @@+module Main where++import Control.Monad+import Data.Typeable+import Data.Proxy+import Data.List+import Data.Map.Strict as Map+import Data.IntSet as ISet+import Data.IntMap as IMap+import qualified Data.ByteString as BS+import qualified Data.ByteString.Char8 as BSC++import System.Directory+import System.Environment+import System.Process+import System.Info+import System.IO+import System.FilePath ((</>))+import Options.Applicative+import Test.Tasty+import Test.Tasty.Golden+import Test.Tasty.Golden.Advanced+import Test.Tasty.Runners+import Test.Tasty.Options+import Test.Tasty.Ingredients.Rerun++import TestData++--------------------------------------------------------------------- [ Config ]++type Flags = [String]++-- Add arguments to calls of idris executable+idrisFlags :: Flags+idrisFlags = []++testDirectory :: String+testDirectory = "test"++-------------------------------------------------------------------- [ Options ]++-- The `--node` option makes idris use the node code generator+-- As a consequence, incompatible tests are removed++newtype NodeOpt = NodeOpt Bool deriving (Eq, Ord, Typeable)++nodeArg = "node"+nodeHelp = "Performs the tests with the node code generator"+instance IsOption NodeOpt where+ defaultValue = NodeOpt False+ parseValue = fmap NodeOpt . safeRead+ optionName = return nodeArg+ optionHelp = return nodeHelp+ optionCLParser = fmap NodeOpt $ switch (long nodeArg <> help nodeHelp)++ingredients :: [Ingredient]+ingredients = defaultIngredients +++ [rerunningTests [consoleTestReporter],+ includingOptions [Option (Proxy :: Proxy NodeOpt)] ]++----------------------------------------------------------------------- [ Core ]++-- Compare a given file contents against the golden file contents+-- A ripoff of goldenVsFile from Tasty.Golden+test :: String -> String -> IO () -> TestTree+test name path act =+ goldenTest name (readFile ref) (act >> readFile new) cmp upd+ where+ ref = path </> "expected"+ new = path </> "output"+ cmp x y = return $ if normalize x == normalize y then Nothing+ else Just $ printDiff (ref, x) (new, y)+ upd = writeFile ref+ -- just pretend that backslashes are slashes for comparison+ -- purposes to avoid path problems, so don't write any tests+ -- that depend on that distinction in other contexts.+ -- Also compare CRLF and LF as equal, fixes a weird corner case+ -- on Mac where basic010 and reg039 produces CRLF+ normalize [] = []+ normalize ('\r':'\n':xs) = '\n' : normalize xs+ normalize ('\\':'\\':xs) = '/' : normalize xs+ normalize ('\\':xs) = '/' : normalize xs+ normalize (x : xs) = x : normalize xs+++-- Takes the filepath and content of `expected` and `output`+-- and formats an error message stating their difference+printDiff :: (String, String) -> (String, String) -> String+printDiff (ref, x) (new, y) =+ let printContent cnt =+ if Data.List.null cnt+ then " is empty...\n"+ else " is: \n" ++ unlines (fmap ((++) " ") (lines cnt))+ in+ "Test mismatch!\n" +++ "Golden file " ++ ref ++ printContent x +++ "However, " ++ new ++ printContent y++-- Should always output a 3-charater string from a postive Int+indexToString :: Int -> String+indexToString index = let str = show index in+ (replicate (3 - length str) '0') ++ str++-- Turns the collection of TestFamily into actual tests usable by Tasty+mkGoldenTests :: [TestFamily] -> Flags -> TestTree+mkGoldenTests testFamilies flags =+ testGroup "Regression and feature tests"+ (fmap mkTestFamily testFamilies)+ where+ mkTestFamily (TestFamily id name tests) =+ testGroup name (fmap (mkTest id) (IMap.keys tests))+ mkTest id index =+ let testname = id ++ indexToString index+ path = testDirectory </> testname+ in+ test testname path (runTest path flags)++-- Runs a test script+-- "bash" needed because Haskell has cmd as the default shell on windows, and+-- we also want to run the process with another current directory, so we get+-- this thing.+runTest :: String -> Flags -> IO ()+runTest path flags = do+ let run = (proc "bash" ("run" : flags)) {cwd = Just path,+ std_out = CreatePipe,+ std_err = CreatePipe}+ (_, output, error_out) <- readCreateProcessWithExitCode run ""+ writeFile (path </> "output") output+ hPutStrLn stderr error_out++main :: IO ()+main = do+ defaultMainWithIngredients ingredients $+ askOption $ \(NodeOpt node) ->+ let (codegen, flags) = if node then (JS, ["--codegen", "node"])+ else (C , [])+ in+ mkGoldenTests (testFamiliesForCodegen codegen)+ (flags ++ idrisFlags)
+ test/base001/Makefile view
@@ -0,0 +1,11 @@+.PHONY:+all: exit1 sys.o++exit1:+ @gcc -Wall -o exit1 exit1.c++sys.o:+ @gcc -Wall -c sys.c++clean:+ -@rm exit1 sys.o
+ test/base001/base001.idr view
@@ -0,0 +1,35 @@+module Main++import System++%include C "sys.h"+%link C "sys.o"++WIFEXITED : (status : Int) -> IO Bool+WIFEXITED status = do+ r <- foreign FFI_C "WIFEXITED_" (Int -> IO Int) status+ pure $ r /= 0++WEXITSTATUS : (status : Int) -> IO Int+WEXITSTATUS status = foreign FFI_C "WEXITSTATUS_" (Int -> IO Int) status++execute : (cmd : String) -> (expectedStatus : Int) -> IO ()+execute cmd expectedStatus = do+ putStrLn "-------------------------------------------"+ putStrLn $ "Executing '" ++ cmd ++ "'"+ status1 <- system cmd+ putStrLn $ "raw status = " ++ show status1 -- XXX: Probably not portable.+ exited <- WIFEXITED status1+ if exited+ then do+ exitStatus <- WEXITSTATUS status1+ putStrLn $ "exit status = " ++ show exitStatus+ printLn $ exitStatus == expectedStatus+ else pure ()+ putStrLn ""++main : IO ()+main = do+ execute "exit 1" 1+ execute "./exit1" 1+ execute "./does-not-exist" 127
+ test/base001/base001.ipkg view
@@ -0,0 +1,5 @@+package base001++executable = base001+main = base001+makefile = Makefile
+ test/base001/exit1.c view
@@ -0,0 +1,17 @@+#include <stdio.h>+#include <stdlib.h>++void doSystem(const char cmd[]) {+ printf("exit1: Executing cmd '%s'\n", cmd);+ int exitStatus = system(cmd);+ printf("exit1: raw exitStatus = %d\n", exitStatus); // XXX: Probably not portable (hide from expected file).+ if (WIFEXITED(exitStatus)) {+ printf("exit1: WEXITSTATUS(exitStatus) = %d\n", WEXITSTATUS(exitStatus));+ }+}++int main() {+ doSystem("exit 1");+ doSystem("./does-not-exist");+ return 1;+}
+ test/base001/expected view
@@ -0,0 +1,25 @@+Type checking ./base001.idr+exit1: Executing cmd 'exit 1'+exit1: raw exitStatus = 256+exit1: WEXITSTATUS(exitStatus) = 1+exit1: Executing cmd './does-not-exist'+exit1: raw exitStatus = 32512+exit1: WEXITSTATUS(exitStatus) = 127+-------------------------------------------+Executing 'exit 1'+raw status = 256+exit status = 1+True++-------------------------------------------+Executing './exit1'+raw status = 256+exit status = 1+True++-------------------------------------------+Executing './does-not-exist'+raw status = 32512+exit status = 127+True+
+ test/base001/run view
@@ -0,0 +1,10 @@+#!/usr/bin/env bash++if [[ ${OSTYPE} = 'msys' ]]; then+ cat expected # skip this test on Windows+else+ ${IDRIS:-idris} $@ --build base001.ipkg | grep -v 'make.*:'+ ./base001+ make clean | grep -v 'make.*:'+ rm -f *.ibc base001+fi
+ test/base001/sys.c view
@@ -0,0 +1,11 @@+#include "sys.h"++#include <stdlib.h>++int WIFEXITED_(int status) {+ return WIFEXITED(status);+}++int WEXITSTATUS_(int status) {+ return WEXITSTATUS(status);+}
+ test/base001/sys.h view
@@ -0,0 +1,7 @@+#ifndef SYS_H+#define SYS_H++int WIFEXITED_(int status);+int WEXITSTATUS_(int status);++#endif
test/basic010/run view
@@ -8,7 +8,7 @@ done if (which timeout&>/dev/null); then- timeout 10 idris $@ Main.idr --nocolour --check --warnreach -o basic010+ timeout 10 ${IDRIS:-idris} $@ Main.idr --nocolour --check --warnreach -o basic010 timeout 5 ./basic010 else # From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting@@ -35,7 +35,7 @@ } - timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"+ timeout 10 "${IDRIS:-idris} ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010" timeout 5 "./basic010" fi rm -f *.ibc basic010
test/basic013/basic013.idr view
@@ -31,4 +31,13 @@ putStrLn ("Tail Tail: " ++ strTail (strTail newstr)) putStrLn ("Cons: " ++ strCons 'λ' newstr) putStrLn ("Reverse: " ++ reverse newstr)+ printLn [1..5]+ printLn [5..1]+ printLn [(-9), (-7)..(-1)]+ printLn [17,15..1]+ printLn [19,15..2]+ printLn $ the (List Nat) [1..5]+ printLn $ the (List Nat) [5..1]+ printLn $ the (List Int) [(-1)..(-5)]+ printLn $ the (List Nat) [1,3..5]
test/basic013/expected view
@@ -12,3 +12,12 @@ Tail Tail: →xλx→xλx→xλx→xλx→x Cons: λλx→xλx→xλx→xλx→xλx→x Reverse: x→xλx→xλx→xλx→xλx→xλ+[1, 2, 3, 4, 5]+[5, 4, 3, 2, 1]+[-9, -7, -5, -3, -1]+[17, 15, 13, 11, 9, 7, 5, 3, 1]+[19, 15, 11, 7, 3]+[1, 2, 3, 4, 5]+[5, 4, 3, 2, 1]+[-1, -2, -3, -4, -5]+[1, 3, 5]
+ test/bounded001/bounded001.idr view
@@ -0,0 +1,10 @@+module Main++-- Test wraparound from upper bounds of Bits types+main : IO ()+main = do putStrLn (show $ the Bits16 maxBound)+ putStrLn (show $ the Bits16 maxBound + 1)+ putStrLn (show $ the Bits32 maxBound)+ putStrLn (show $ the Bits32 maxBound + 1)+ putStrLn (show $ the Bits64 maxBound)+ putStrLn (show $ the Bits64 maxBound + 1)
+ test/bounded001/expected view
@@ -0,0 +1,6 @@+FFFF+0000+FFFFFFFF+00000000+FFFFFFFFFFFFFFFF+0000000000000000
+ test/bounded001/run view
@@ -0,0 +1,4 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ bounded001.idr -o bounded001+./bounded001+rm -f bounded001 *.ibc
test/disambig002/disambig002.idr view
@@ -2,6 +2,8 @@ import Data.Fin import Control.Isomorphism +-- Tests if Idris can disambiguate between the three `toVect` operators+ Dec0 : Type -> Type Dec0 = Dec
test/docs001/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet --nocolor docs001.idr < input+${IDRIS:-idris} $@ --quiet --nocolor docs001.idr < input rm *.ibc
test/docs002/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nobanner --nocolor --quiet docs002.idr < input+${IDRIS:-idris} $@ --nobanner --nocolor --quiet docs002.idr < input rm *.ibc
test/docs003/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet --nocolor docs003.idr < input+${IDRIS:-idris} $@ --quiet --nocolor docs003.idr < input rm *.ibc
test/docs004/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet --nocolor docs004.idr < input+${IDRIS:-idris} $@ --quiet --nocolor docs004.idr < input rm *.ibc
test/docs005/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet --nocolor docs005.idr < input+${IDRIS:-idris} $@ --quiet --nocolor docs005.idr < input rm *.ibc
test/effects001/run view
@@ -1,6 +1,6 @@ #!/usr/bin/env bash-${IDRIS:-idris} -p effects $@ test021.idr -o test021-${IDRIS:-idris} -p effects $@ test021a.idr -o test021a+${IDRIS:-idris} $@ -p effects test021.idr -o test021+${IDRIS:-idris} $@ -p effects test021a.idr -o test021a ./test021 ./test021a rm -f test021 test021a *.ibc
test/effects002/run view
@@ -1,4 +1,4 @@ #!/usr/bin/env bash-${IDRIS:-idris} -p effects $@ test025.idr -o test025+${IDRIS:-idris} $@ -p effects test025.idr -o test025 ./test025 rm -f test025 *.ibc
test/ffi001/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet --nocolour test022.idr --exec main+${IDRIS:-idris} $@ --quiet --nocolour test022.idr --exec main rm -f *.ibc
test/ffi002/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet test023.idr -o test023+${IDRIS:-idris} $@ --quiet test023.idr -o test023 rm -f test023 *.ibc
test/ffi003/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet --nocolour test024.idr --exec main < input+${IDRIS:-idris} $@ --quiet --nocolour test024.idr --exec main < input rm -f *.ibc
test/ffi004/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet --nocolour --check test026.idr+${IDRIS:-idris} $@ --quiet --nocolour --check test026.idr rm -f *.ibc
test/ffi006/run view
@@ -1,5 +1,5 @@ #!/usr/bin/env bash ${IDRIS:-idris} $@ ffi006.idr --interface -o ffi006.o-${CC:=cc} ffi006.c ffi006.o `idris --include` `idris --link` -o ffi006+${CC:=cc} ffi006.c ffi006.o `${IDRIS:-idris} $@ --include` `${IDRIS:-idris} $@ --link` -o ffi006 ./ffi006 rm -f ffi006 *.ibc *.o *.h
test/idrisdoc001/run view
@@ -1,4 +1,4 @@ #!/usr/bin/env bash # Tests that no documentation is built for empty and/or private-only namespaces-${IDRIS:-idris} --mkdoc test_empty.ipkg+${IDRIS:-idris} $@ --mkdoc test_empty.ipkg rm -rf *.ibc *_doc
test/idrisdoc002/run view
@@ -1,5 +1,5 @@ #!/usr/bin/env bash # Tests that documentation is generated for functions-${IDRIS:-idris} --mkdoc test_functions.ipkg+${IDRIS:-idris} $@ --mkdoc test_functions.ipkg [ -d test_functions_doc ] && echo "Functions are documented" rm -rf *.ibc *_doc
test/idrisdoc003/run view
@@ -1,5 +1,5 @@ #!/usr/bin/env bash # Tests that documentation is generated for data types-${IDRIS:-idris} --mkdoc test_datatypes.ipkg+${IDRIS:-idris} $@ --mkdoc test_datatypes.ipkg [ -d test_datatypes_doc ] && echo "Data types are documented" rm -rf *.ibc *_doc
test/idrisdoc004/run view
@@ -1,5 +1,5 @@ #!/usr/bin/env bash # Tests that documentation is generated for typeclasses-${IDRIS:-idris} --mkdoc test_typeclasses.ipkg+${IDRIS:-idris} $@ --mkdoc test_typeclasses.ipkg [ -d test_typeclasses_doc ] && echo "Typeclasses are documented" rm -rf *.ibc *_doc
test/idrisdoc005/run view
@@ -1,6 +1,6 @@ #!/usr/bin/env bash # Tests that references to other namespaces are traced-${IDRIS:-idris} --mkdoc test_tracing.ipkg+${IDRIS:-idris} $@ --mkdoc test_tracing.ipkg [ -f test_tracing_doc/docs/TestTracing.html ] && echo "TestTracing: Check" [ -f test_tracing_doc/docs/Prelude.Bool.html ] && echo "Prelude.Bool: Check" rm -rf *.ibc *_doc
test/idrisdoc006/run view
@@ -1,8 +1,8 @@ #!/usr/bin/env bash # Tests that documentation properly is merged with existent.-${IDRIS:-idris} --mkdoc package_a.ipkg+${IDRIS:-idris} $@ --mkdoc package_a.ipkg [ -f test_merge_doc/IdrisDoc ] && echo "IdrisDoc file written"-${IDRIS:-idris} --mkdoc package_b.ipkg+${IDRIS:-idris} $@ --mkdoc package_b.ipkg ls -1p test_merge_doc/docs if grep -q "href\\=\"docs/A.fully.Qualified.NAME\\.html\"" test_merge_doc/index.html; then echo A.fully.Qualified.NAME is in the index
test/idrisdoc007/run view
@@ -1,6 +1,6 @@ #!/usr/bin/env bash # Tests that documentation only is written when safe mkdir do_not_delete_doc-${IDRIS:-idris} --mkdoc package.ipkg > nowhere+${IDRIS:-idris} $@ --mkdoc package.ipkg > nowhere echo Exit status \(expects 1\): $? rm -rf do_not_delete_doc *.ibc nowhere
test/idrisdoc008/run view
@@ -1,6 +1,6 @@ #!/usr/bin/env bash # Tests that documentation is generated for both public and abstract members.-${IDRIS:-idris} --mkdoc visibility.ipkg+${IDRIS:-idris} $@ --mkdoc visibility.ipkg [ -f visibility_doc/docs/Abstract.html ] && echo "Abstract members are documented" [ -f visibility_doc/docs/Visible.html ] && echo "Public members are documented" rm -rf *.ibc *_doc
test/interactive001/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet test032.idr < input+${IDRIS:-idris} $@ --quiet test032.idr < input rm -f *.ibc
test/interactive002/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet interactive002.idr < input+${IDRIS:-idris} $@ --quiet interactive002.idr < input rm -f *.ibc
test/interactive003/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet interactive003.idr < input+${IDRIS:-idris} $@ --quiet interactive003.idr < input rm -f *.ibc
test/interactive004/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet interactive004.idr < input+${IDRIS:-idris} $@ --quiet interactive004.idr < input rm -f *.ibc
test/interactive005/run view
@@ -1,5 +1,5 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour --quiet interactive005.idr --consolewidth 70 < input+${IDRIS:-idris} $@ --nocolour --quiet interactive005.idr --consolewidth 70 < input rm -f *.ibc rm -f hello.bytecode rm -f hello
test/interactive006/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet --port 5000 interactive006.idr < input+${IDRIS:-idris} $@ --quiet --port 5000 interactive006.idr < input rm -f *.ibc
test/interactive007/run view
@@ -1,2 +1,2 @@ #!/usr/bin/env bash-${IDRIS:-idris} -p contrib --nobanner --nocolor < input+${IDRIS:-idris} $@ -p contrib --nobanner --nocolor < input
test/interactive008/run view
@@ -1,2 +1,2 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nobanner --nocolor < input+${IDRIS:-idris} $@ --nobanner --nocolor < input
test/interactive009/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet interactive009.idr < input+${IDRIS:-idris} $@ --quiet interactive009.idr < input rm -f *.ibc
test/interactive010/run view
@@ -1,2 +1,2 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet --nobanner --nocolor < input+${IDRIS:-idris} $@ --quiet --nobanner --nocolor < input
test/interactive011/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet interactive011.idr < input+${IDRIS:-idris} $@ --quiet interactive011.idr < input rm -f *.ibc
test/interactive012/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour --consolewidth 70 --quiet interactive012.idr < input+${IDRIS:-idris} $@ --nocolour --consolewidth 70 --quiet interactive012.idr < input rm -f *.ibc
test/interactive013/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet interactive013.idr < input+${IDRIS:-idris} $@ --quiet interactive013.idr < input rm -f *.ibc
+ test/layout001/expected view
@@ -0,0 +1,93 @@+Checking layout001a.idr+./layout001a.idr:5:1: error: Wrong+ indention: should be greater+ than context+ indentation, expected: space+y +^ +Checking layout001b.idr+./layout001b.idr:5:3: error: Wrong+ indention: should be greater+ than context+ indentation, expected: space+= y + ^ +Checking layout001c.idr+./layout001c.idr:3:1: error: Wrong+ indention: should be greater+ than context+ indentation, expected: space+2 +^ +Checking layout001d.idr+Checking layout001e.idr+./layout001e.idr:6:1: error: Wrong+ indention: should be greater+ than context+ indentation, expected: space+3 +^ +Checking layout001f.idr+./layout001f.idr:6:2: error: Wrong+ indention: should be greater+ than context+ indentation, expected: space+ 3 + ^ +Checking layout001g.idr+./layout001g.idr:6:3: error: Wrong+ indention: should be greater+ than context+ indentation, expected: space+ 3 + ^ +Checking layout001h.idr+./layout001h.idr:6:3: error: Wrong+ indention: should be greater+ than context+ indentation, expected: space+ 3 + ^ +Checking layout001i.idr+./layout001i.idr:6:4: error: Wrong+ indention: should be greater+ than context+ indentation, expected: space+ 3 + ^ +Checking layout001j.idr+./layout001j.idr:6:5: error: Wrong+ indention: should be greater+ than context+ indentation, expected: space+ 3 + ^ +Checking layout001k.idr+Checking layout001l.idr+./layout001l.idr:6:1: error: Wrong+ indention: should be greater+ than context+ indentation, expected: space+y +^ +Checking layout001n.idr+Checking mplus1.idr+mplus1.idr:13:31:+When checking right hand side of term with expected type+ Maybe Int++When checking an application of function Prelude.Applicative.pure:+ No such variable f+Checking mplus2.idr+./mplus2.idr:17:37: error: not+ end of block, expected: ")",+ "->", ";", "in",+ ambiguous use of a left-associative operator,+ ambiguous use of a non-associative operator,+ ambiguous use of a right-associative operator,+ do block expression,+ end of input+ `mplus` pure f + ^ +Checking mplus3.idr+mplus3.idr:11:1:warning - Unreachable case: term
+ test/layout001/layout001a.idr view
@@ -0,0 +1,5 @@+f : Int -> Int+f x = z 1 + 1 where+ z : Int -> Int+ z y =+y
+ test/layout001/layout001b.idr view
@@ -0,0 +1,5 @@+f : Int -> Int+f x = z 1 + 1 where+ z : Int -> Int+ z y += y
+ test/layout001/layout001c.idr view
@@ -0,0 +1,3 @@+f : Int+f =+2
+ test/layout001/layout001d.idr view
@@ -0,0 +1,3 @@+f : Int+f+= 2
+ test/layout001/layout001e.idr view
@@ -0,0 +1,6 @@+foo : Int -> Int+foo a = a + b+ where+ b : Int+ b = 2 ++3
+ test/layout001/layout001f.idr view
@@ -0,0 +1,6 @@+foo : Int -> Int+foo a = a + b+ where+ b : Int+ b = 2 ++ 3
+ test/layout001/layout001g.idr view
@@ -0,0 +1,6 @@+foo : Int -> Int+foo a = a + b+ where+ b : Int+ b = 2 ++ 3
+ test/layout001/layout001h.idr view
@@ -0,0 +1,6 @@+foo : Int -> Int+foo a = a + b+ where+ b : Int+ b = 2 ++ 3
+ test/layout001/layout001i.idr view
@@ -0,0 +1,6 @@+foo : Int -> Int+foo a = a + b+ where+ b : Int+ b = 2 ++ 3
+ test/layout001/layout001j.idr view
@@ -0,0 +1,6 @@+foo : Int -> Int+foo a = a + b+ where+ b : Int+ b = 2 ++ 3
+ test/layout001/layout001k.idr view
@@ -0,0 +1,6 @@+foo : Int -> Int+foo a = a + b+ where+ b : Int+ b = 2 ++ 3
+ test/layout001/layout001l.idr view
@@ -0,0 +1,6 @@+f : Int -> Int+f x = z 1 + 1+ where+ z : Int -> Int+ z y =+y
+ test/layout001/layout001n.idr view
@@ -0,0 +1,33 @@+module NonLayout++{-+Haskell and Idris use indentation for grouping in the concrete syntax.+How this works is defined as an automatic translation to the equivalent+syntax using { ; and }, which you are free to use yourself.++In Idris specifically, if let or where is followed by { then indentation no+longer matters for the following definitions until a balanced } appears. To+put multiple declarations on one line within the { } you put semicolons between+them: one ; for let declarations and ;; for where declarations. Whether this+discrepancy is a bug I don't know.+-}++average : String -> Double+average str = answer where+ wordCount : String -> Nat+ wordCount str = length (words str)+ wordLengths : List String -> List Nat+ wordLengths strs = map length strs+ answer =+ let numWords = wordCount str in+ let totalLength = sum (wordLengths (words str)) in+ cast totalLength / cast numWords++average' : String -> Double+average' str = answer where {+ wordCount : String -> Nat ;; wordCount str = length (words str)+ wordLengths : List String -> List Nat ;; wordLengths strs = map length strs+ answer = let {+ numWords = wordCount str; totalLength = sum (wordLengths (words str))+ } in cast totalLength / cast numWords+}
+ test/layout001/mplus1.idr view
@@ -0,0 +1,17 @@+mplus : Maybe a -> Maybe a -> Maybe a+mplus a b = ?mplus_rhs++factor : Maybe Int+factor = ?term_rhs++symbol : String -> Maybe Int+symbol = ?symbol_rhs++term : Maybe Int+term = ?term_rhs++term = do f <- factor+ do symbol "*"+ t <- term+ pure (f * t)+ `mplus` pure f
+ test/layout001/mplus2.idr view
@@ -0,0 +1,17 @@+mplus : Maybe a -> Maybe a -> Maybe a+mplus a b = ?mplus_rhs++factor : Maybe Int+factor = ?term_rhs++symbol : String -> Maybe Int+symbol = ?symbol_rhs++term : Maybe Int+term = ?term_rhs++term = do f <- factor+ do symbol "*"+ t <- term+ pure (f * t)+ `mplus` pure f
+ test/layout001/mplus3.idr view
@@ -0,0 +1,17 @@+mplus : Maybe a -> Maybe a -> Maybe a+mplus a b = ?mplus_rhs++factor : Maybe Int+factor = ?term_rhs++symbol : String -> Maybe Int+symbol = ?symbol_rhs++term : Maybe Int+term = ?term_rhs++term = do f <- factor+ do symbol "*"+ t <- term+ pure (f * t)+ `mplus` pure f
+ test/layout001/run view
@@ -0,0 +1,8 @@+#!/usr/bin/env bash++for file in *.idr; do+ echo Checking ${file}+ ${IDRIS:-idris} --check $@ ${file}+done++rm -f *.ibc
test/meta002/run view
@@ -3,5 +3,5 @@ ${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 Tacs.idr ${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 AgdaStyleReflection.idr # Disabled due to excess memory consumption-# idris $@ -p pruviloj --nocolour --check --consolewidth 70 Deriving.idr+# ${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 Deriving.idr rm -f *.ibc
+ test/meta003/BadDef.idr view
@@ -0,0 +1,12 @@+module BadDef++import Language.Reflection.Elab++mkN : String -> TTName+mkN n = NS (UN n) ["BadDef"]++mkBadDef1 : Elab ()+mkBadDef1 = do declareType $ Declare (mkN "bad1") [] `(() -> ())+ defineFunction $ DefineFun (mkN "bad1") [MkFunClause `(():()) `("hi")]++%runElab mkBadDef1
+ test/meta003/expected view
@@ -0,0 +1,6 @@+BadDef.idr:12:1-9:+While running an elaboration script, the following error occurred:+Type mismatch between+ ()+and+ String
+ test/meta003/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ --nocolour --check --consolewidth 70 BadDef.idr+rm -f *.ibc
+ test/pkg002/Main.idr view
@@ -0,0 +1,4 @@+module Main++main : IO ()+main = putStrLn "CouCou!"
+ test/pkg002/expected view
+ test/pkg002/run view
@@ -0,0 +1,5 @@+#!/usr/bin/env bash+### Test: IPKG executable names can be any namespaced identifier.+${IDRIS:-idris} $@ --build test.ipkg+rm -f *.ibc+rm -f some.namespaced.identifier
+ test/pkg002/test.ipkg view
@@ -0,0 +1,8 @@+package test++modules = Main+++opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80"+main = Main+executable = some.namespaced.identifier
+ test/pkg003/Main.idr view
@@ -0,0 +1,4 @@+module Main++main : IO ()+main = putStrLn "CouCou!"
+ test/pkg003/expected view
+ test/pkg003/run view
@@ -0,0 +1,6 @@+#!/usr/bin/env bash+### Test: IPKG executable names can be a quoted string+### containing a valid filename.+${IDRIS:-idris} $@ --build test.ipkg+rm -f *.ibc+rm -f 'quoting-allows-hyphens and spaces and fun stuff!'
+ test/pkg003/test.ipkg view
@@ -0,0 +1,7 @@+package test++modules = Main++opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80"+main = Main+executable = "quoting-allows-hyphens and spaces and fun stuff!"
+ test/pkg004/Main.idr view
@@ -0,0 +1,4 @@+module Main++main : IO ()+main = putStrLn "CouCou!"
+ test/pkg004/expected view
@@ -0,0 +1,5 @@+Uncaught error: user error (test.ipkg:9:1: error: filename+ must contain no directory+ component, expected: space+<EOF> +^ )
+ test/pkg004/run view
@@ -0,0 +1,6 @@+#!/usr/bin/env bash+### Test: IPKG executable names CANNOT include a directory separator.+# TODO: Verify that a name like "a/b\c" is rejected by both *NIX and Windows+# (assuming these tests get run on Windows).+${IDRIS:-idris} $@ --build test.ipkg+rm -f *.ibc
+ test/pkg004/test.ipkg view
@@ -0,0 +1,8 @@+package test++modules = Main++opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80"++main = Main+executable = "filenames/cannot include\a directory separator"
+ test/pkg005/expected view
@@ -0,0 +1,1 @@+Can't build an executable: No main module given
+ test/pkg005/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+### Test: Build IPKG, executable without main.+${IDRIS:-idris} $@ --build test.ipkg
+ test/pkg005/test.ipkg view
@@ -0,0 +1,3 @@+package test++executable = test
+ test/pkg006/expected view
@@ -0,0 +1,1 @@+Can't start REPL: no main module given
+ test/pkg006/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+### Test: Launch REPL, IPKG executable without main.+${IDRIS:-idris} $@ --repl test.ipkg
+ test/pkg006/test.ipkg view
@@ -0,0 +1,3 @@+package test++executable = test
+ test/prelude001/expected view
@@ -0,0 +1,10 @@+True+True+True+True+True+True+True+True+True+True
+ test/prelude001/prelude001.idr view
@@ -0,0 +1,17 @@+module Main++main : IO ()+main = do+ printLn $ lines "" == []+ -- `lines` seems to ignore too many trailing newlines.+ printLn $ lines "\n" == [] -- FIXME: Should be [""].+ printLn $ lines "\n\n" == [] -- FIXME: Should be ["", ""].+ printLn $ lines "\n\n\n" == [] -- FIXME: Should be ["", "", ""].+ printLn $ lines "1\n2\n3" == ["1", "2", "3"]+ printLn $ lines "1\n2\n3\n" == ["1", "2", "3"]+ printLn $ unlines [] == ""+ -- `unlines` works as advertised doesn't follow Haskell here.+ -- When files are written using unlines, vim complains of "noeoln".+ printLn $ unlines ["1"] == "1" -- FIXME: Should be "1\n"+ printLn $ unlines ["1", "2"] == "1\n2" -- FIXME: Should be "1\n2\n"+ printLn $ unlines ["1", "2", "3"] == "1\n2\n3" -- FIXME: Should be "1\n2\n3\n"
+ test/prelude001/run view
@@ -0,0 +1,4 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ prelude001.idr -o prelude001+./prelude001+rm -f prelude001 *.ibc
test/primitives002/run view
@@ -48,7 +48,7 @@ do echo ${T%% *} ${T##*#} generate_testfile "tmptest.idr" "${T%%#*}"- idris "$@" --quiet tmptest.idr -o tmptest || echo "missing primitive in ${CG}"+ ${IDRIS:-idris} $@ --quiet tmptest.idr -o tmptest || echo "missing primitive in ${CG}" ./tmptest <<<"${T##*#}" rm tmptest.idr tmptest.ibc tmptest done
test/proof004/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --check $@ test035.idr+${IDRIS:-idris} $@ --check test035.idr rm -f *.ibc
test/proof005/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --check $@ DefaultArgSubstitutionSuccess.idr+${IDRIS:-idris} $@ --check DefaultArgSubstitutionSuccess.idr rm -f *.ibc
test/proof006/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --check $@ DefaultArgSubstitutionSyntax.idr+${IDRIS:-idris} $@ --check DefaultArgSubstitutionSyntax.idr rm -f *.ibc
test/proof007/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour --check $@ DefaultArgUnknownName.idr+${IDRIS:-idris} $@ --nocolour --check DefaultArgUnknownName.idr rm -f *.ibc
test/proof008/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour --check $@ ClaimAndUnfocus.idr+${IDRIS:-idris} $@ --nocolour --check ClaimAndUnfocus.idr rm -f *.ibc
test/proofsearch003/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --check proofsearch003.idr +${IDRIS:-idris} $@ --check proofsearch003.idr rm -f *.ibc
test/reg002/run view
@@ -1,4 +1,4 @@ #!/usr/bin/env bash-${IDRIS:-idris} reg012.idr -o reg012+${IDRIS:-idris} $@ reg012.idr -o reg012 ./reg012 rm -f reg012 *.ibc
test/reg003/run view
@@ -1,4 +1,4 @@ #!/usr/bin/env bash-${IDRIS:-idris} --check reg003.idr-${IDRIS:-idris} --check reg003a.idr+${IDRIS:-idris} $@ --check reg003.idr+${IDRIS:-idris} $@ --check reg003a.idr rm -f *.ibc
test/reg007/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour --check $@ reg007.lidr+${IDRIS:-idris} $@ --nocolour --check reg007.lidr rm -f *.ibc
test/reg023/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour $@ reg023.idr --check+${IDRIS:-idris} $@ --nocolour reg023.idr --check rm -f *.ibc
test/reg034/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour --check reg034.idr+${IDRIS:-idris} $@ --nocolour --check reg034.idr rm -f reg034 *.ibc
test/reg035/run view
@@ -1,5 +1,5 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour --check reg035.idr-${IDRIS:-idris} --nocolour --check reg035a.lidr-${IDRIS:-idris} --nocolour --check reg035b.idr+${IDRIS:-idris} $@ --nocolour --check reg035.idr+${IDRIS:-idris} $@ --nocolour --check reg035a.lidr+${IDRIS:-idris} $@ --nocolour --check reg035b.idr rm -f *.ibc
test/reg039/run view
@@ -7,7 +7,7 @@ extraargs=("${extraargs[@]}" "'$arg'") done if (which timeout&>/dev/null); then- timeout 60 idris $@ --nocolour reg039.idr --exec go+ timeout 60 ${IDRIS:-idris} $@ --nocolour reg039.idr --exec go else # From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting # Executes command with a timeout@@ -30,6 +30,6 @@ fi }- timeout 60 "idris ${extraargs[*]} --nocolour reg039.idr --exec go"+ timeout 60 "${IDRIS:-idris} ${extraargs[*]} --nocolour reg039.idr --exec go" fi rm -f reg039 *.ibc
test/reg040/run view
@@ -1,6 +1,6 @@ #!/usr/bin/env bash -${IDRIS:-idris} --warnreach reg040.idr -o reg040+${IDRIS:-idris} $@ --warnreach reg040.idr -o reg040 ./reg040 rm -f reg040 *.ibc
test/reg044/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour reg044.idr --check+${IDRIS:-idris} $@ --nocolour reg044.idr --check rm -f *.ibc
test/reg049/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour --check $@ reg049.idr+${IDRIS:-idris} $@ --nocolour --check $@ reg049.idr rm -f *.ibc
test/reg050/run view
@@ -1,5 +1,5 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour --check $@ working.idr-${IDRIS:-idris} --nocolour --check $@ badbangop.idr-${IDRIS:-idris} --nocolour --check $@ baddoublebang.idr+${IDRIS:-idris} $@ --nocolour --check working.idr+${IDRIS:-idris} $@ --nocolour --check badbangop.idr+${IDRIS:-idris} $@ --nocolour --check baddoublebang.idr rm -f *.ibc
test/reg054/run view
@@ -1,2 +1,2 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour $@ reg054.idr --check+${IDRIS:-idris} $@ --nocolour reg054.idr --check
test/reg055/run view
@@ -1,5 +1,5 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour $@ reg055.idr --check-${IDRIS:-idris} --nocolour $@ reg055a.idr --check+${IDRIS:-idris} $@ --nocolour reg055.idr --check+${IDRIS:-idris} $@ --nocolour reg055a.idr --check rm -f *.ibc
test/reg075/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --quiet reg075.idr < input+${IDRIS:-idris} $@ --quiet reg075.idr < input rm -f *.ibc
− test/runtest.hs
@@ -1,230 +0,0 @@-{-# LANGUAGE CPP #-}-module Main where--import Control.Monad-import Data.Char-import Data.List-import Data.Maybe-import qualified Data.Set as S-import Data.Time.Clock-import System.Directory-import System.Environment-import System.FilePath-import System.Exit-import System.Info-import System.IO-import System.Process---- Because GHC earlier than 7.8 lacks setEnv--- Install the setenv package on Windows.-#if __GLASGOW_HASKELL__ < 708-#ifndef mingw32_HOST_OS-import qualified System.Posix.Env as PE(setEnv)--setEnv k v = PE.setEnv k v True-#else-import System.SetEnv(setEnv)-#endif-#endif--data Flag = Update | Diff | ShowOutput | Quiet | Time deriving (Eq, Show, Ord)--type Flags = S.Set Flag--data Status = Success | Failure | Updated deriving (Eq, Show)--data Config = Config {- flags :: Flags,- idrOpts :: [String],- tests :: [String]-} deriving (Show, Eq)--isQuiet conf = Quiet `S.member` (flags conf)-showOutput conf = ShowOutput `S.member` (flags conf)-showTime conf = Time `S.member` (flags conf)-showDiff conf = Diff `S.member` (flags conf)-doUpdate conf = Update `S.member` (flags conf)--checkTestName :: String -> Bool-checkTestName d = (all isDigit $ take 3 $ reverse d)- && (not $ isInfixOf "disabled" d)--enumTests :: IO [String]-enumTests = do- cwd <- getCurrentDirectory- dirs <- getDirectoryContents cwd- return $ sort $ filter checkTestName dirs--parseFlag :: String -> Maybe Flag-parseFlag s = case s of- "-u" -> Just Update- "-d" -> Just Diff- "-s" -> Just ShowOutput- "-t" -> Just Time- "-q" -> Just Quiet- _ -> Nothing--parseFlags :: [String] -> (S.Set Flag, [String])-parseFlags xs = (S.fromList f, i)- where- f = catMaybes $ map parseFlag fl- (fl, i) = partition (\s -> parseFlag s /= Nothing) xs--parseArgs :: [String] -> IO Config-parseArgs args = do- (tests, rest) <- case args of- ("all":xs) -> do- et <- enumTests- return (et, xs)- ("without":xs) -> do- t <- enumTests- (blacklist, ys) <- return $ break (== "opts") xs- return (t \\ blacklist, ys \\ ["opts"])- (x:xs) -> do- exists <- doesDirectoryExist x- return (if checkTestName x && exists then [x] else [], xs)- [] -> do- et <- enumTests- return (et, [])- let (testOpts, idOpts) = parseFlags rest- return $ Config testOpts idOpts tests---- "bash" needed because Haskell has cmd as the default shell on windows, and--- we also want to run the process with another current directory, so we get--- this thing.-runInShell :: String -> [String] -> IO (ExitCode, String)-runInShell test opts = do- (ec, output, _) <- readCreateProcessWithExitCode- ((proc "bash" ("run":opts)) { cwd = Just test,- std_out = CreatePipe })- ""- return (ec, output)--runTest :: Config -> String -> IO Status-runTest conf test = do- -- don't touch the current directory as we want to run these things- -- in parallel in the future- let inTest s = test ++ "/" ++ s- t1 <- getCurrentTime- (exitCode, output) <- runInShell test (idrOpts conf)- t2 <- getCurrentTime- expected <- readFile $ inTest "expected"- writeFile (inTest "output") output- res <- if (norm output == norm expected)- then do putStrLn $ test ++ " finished...success"- return Success- else if doUpdate conf- then do putStrLn $ test ++ " finished...UPDATE"- writeFile (inTest "expected") output- return Updated- else do putStrLn $ test ++ " finished...FAILURE"- _ <- rawSystem "diff" [inTest "output", inTest "expected"]- return Failure- when (showTime conf) $ do- let dt = diffUTCTime t2 t1- putStrLn $ "Duration of " ++ test ++ " was " ++ show dt- return res- where - -- just pretend that backslashes are slashes for comparison- -- purposes to avoid path problems, so don't write any tests- -- that depend on that distinction in other contexts.- -- Also rewrite newlines for consistency.- norm ('\r':'\n':xs) = '\n' : norm xs- norm ('\\':'\\':xs) = '/' : norm xs- norm ('\\':xs) = '/' : norm xs- norm (x : xs) = x : norm xs- norm [] = []--printStats :: Config -> [Status] -> IO ()-printStats conf stats = do- let total = length stats- let successful = length $ filter (== Success) stats- let failures = length $ filter (== Failure) stats- let updates = length $ filter (== Updated) stats- putStrLn "\n----"- putStrLn $ show total ++ " tests run: " ++ show successful ++ " succesful, "- ++ show failures ++ " failed, " ++ show updates ++ " updated."- let failed = map fst $ filter ((== Failure) . snd) $ zip (tests conf) stats- when (failed /= []) $ do- putStrLn "\nFailed tests:"- mapM_ putStrLn failed- putStrLn ""--runTests :: Config -> IO Bool-runTests conf = do- stats <- mapM (runTest conf) (tests conf)- unless (isQuiet conf) $ printStats conf stats- return $ all (== Success) stats--runShow :: Config -> IO Bool-runShow conf = do- mapM_ (\t -> callProcess "cat" [t++"/output"]) (tests conf)- return True--runDiff :: Config -> IO Bool-runDiff conf = do- mapM_ (\t -> do putStrLn $ "Differences in " ++ t ++ ":"- ec <- rawSystem "diff" [t++"/output", t++"/expected"]- when (ec == ExitSuccess) $ putStrLn "No differences found.")- (tests conf)- return True--whisper :: Config -> String -> IO ()-whisper conf s = do unless (isQuiet conf) $ putStrLn s--isWindows :: Bool-isWindows = os `elem` ["win32", "mingw32", "cygwin32"]--setPath :: Config -> IO ()-setPath conf = do- maybeEnv <- lookupEnv "IDRIS"- idrisExists <- case maybeEnv of- Just idrisExe -> do- let exeExtension = if isWindows then ".exe" else ""- doesFileExist (idrisExe ++ exeExtension)- Nothing -> return False- if (idrisExists)- then do- idrisAbs <- makeAbsolute $ fromMaybe "" maybeEnv- setEnv "IDRIS" idrisAbs- whisper conf $ "Using " ++ idrisAbs- else do- path <- getEnv "PATH"- setEnv "IDRIS" ""- let sandbox = "../.cabal-sandbox/bin"- hasBox <- doesDirectoryExist sandbox- bindir <- if hasBox- then do- whisper conf $ "Using Cabal sandbox at " ++ sandbox- makeAbsolute sandbox- else do- stackExe <- findExecutable "stack"- case stackExe of- Just stack -> do- out <- readProcess stack ["path", "--dist-dir"] []- stackDistDir <- return $ takeWhile (/= '\n') out- let stackDir = "../" ++ stackDistDir ++ "/build/idris"- whisper conf $ "Using stack work dir at " ++ stackDir- makeAbsolute stackDir- Nothing -> return ""- when (bindir /= "") $ setEnv "PATH" (bindir ++ [searchPathSeparator] ++ path)--main = do- hSetBuffering stdout LineBuffering- withCabal <- doesDirectoryExist "test"- when withCabal $ do- setCurrentDirectory "test"- args <- getArgs- conf <- parseArgs args- setPath conf- t1 <- getCurrentTime- res <- case tests conf of- [] -> return True- xs | showOutput conf -> runShow conf- xs | showDiff conf -> runDiff conf- xs -> runTests conf- t2 <- getCurrentTime- when (showTime conf) $ do- let dt = diffUTCTime t2 t1- putStrLn $ "Duration of Entire Test Suite was " ++ show dt- unless res exitFailure
test/totality003/run view
@@ -1,4 +1,4 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour $@ totality003.idr --check-${IDRIS:-idris} --nocolour $@ totality003a.idr --check+${IDRIS:-idris} $@ --nocolour totality003.idr --check+${IDRIS:-idris} $@ --nocolour totality003a.idr --check rm -f *.ibc
test/totality009/run view
@@ -1,6 +1,6 @@ #!/usr/bin/env bash OPTS="--consolewidth infinite --nocolour"-${IDRIS:-idris} "$@" $OPTS --check TestLambdaImpossible-${IDRIS:-idris} "$@" $OPTS --check --warnpartial TestLambdaPossible-${IDRIS:-idris} "$@" $OPTS --check TestLambdaPossible2+${IDRIS:-idris} $@ $OPTS --check TestLambdaImpossible+${IDRIS:-idris} $@ $OPTS --check --warnpartial TestLambdaPossible+${IDRIS:-idris} $@ $OPTS --check TestLambdaPossible2 rm -f *.ibc
test/tutorial001/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --check tutorial001.idr+${IDRIS:-idris} $@ --check tutorial001.idr rm -f *.ibc
test/tutorial006/run view
@@ -1,5 +1,5 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour $@ tutorial006a.idr --check-${IDRIS:-idris} --nocolour $@ tutorial006b.idr --check-${IDRIS:-idris} --nocolour $@ tutorial006c.idr -p effects --check+${IDRIS:-idris} $@ --nocolour tutorial006a.idr --check+${IDRIS:-idris} $@ --nocolour tutorial006b.idr --check+${IDRIS:-idris} $@ --nocolour tutorial006c.idr -p effects --check rm -f *.ibc
test/tutorial007/run view
@@ -1,5 +1,5 @@ #!/usr/bin/env bash-gcc -shared -fPIC nativetypes.c -o nativetypes.so-idris $@ tutorial007.idr -o tutorial007+${CC:-cc} -shared -fPIC nativetypes.c -o nativetypes.so+${IDRIS:-idris} $@ tutorial007.idr -o tutorial007 ./tutorial007 rm -f tutorial007 *.ibc *.so sizefromc.txt
test/unique001/run view
@@ -1,9 +1,9 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour $@ unique001.idr -o unique001+${IDRIS:-idris} $@ --nocolour unique001.idr -o unique001 ./unique001-${IDRIS:-idris} --nocolour $@ unique001a.idr --check-${IDRIS:-idris} --nocolour $@ unique001b.idr --check-${IDRIS:-idris} --nocolour $@ unique001c.idr --check-${IDRIS:-idris} --nocolour $@ unique001d.idr --check-${IDRIS:-idris} --nocolour $@ unique001e.idr --check+${IDRIS:-idris} $@ --nocolour unique001a.idr --check+${IDRIS:-idris} $@ --nocolour unique001b.idr --check+${IDRIS:-idris} $@ --nocolour unique001c.idr --check+${IDRIS:-idris} $@ --nocolour unique001d.idr --check+${IDRIS:-idris} $@ --nocolour unique001e.idr --check rm -f unique001 *.ibc
test/unique002/run view
@@ -1,4 +1,4 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour $@ unique002.idr --check-${IDRIS:-idris} --nocolour $@ unique002a.idr --check+${IDRIS:-idris} $@ --nocolour unique002.idr --check+${IDRIS:-idris} $@ --nocolour unique002a.idr --check rm -f *.ibc
test/unique003/run view
@@ -1,3 +1,3 @@ #!/usr/bin/env bash-${IDRIS:-idris} --nocolour $@ unique003.idr --check+${IDRIS:-idris} $@ --nocolour unique003.idr --check rm -f *.ibc