Unit tests with Specdris and Travis CI Improvement.

.gitignore

@@ -1,3 +1,4 @@
 *_doc/
 *.ibc
 *~
+dependencies/

.travis.yml

@@ -1,5 +1,2 @@
-os: osx
-install:
-  - brew install idris
-script:
-  - make test 
+language: nix
+script: nix-shell -A lightyear --command "make testCI"

Makefile

@@ -3,11 +3,18 @@ all: install
 install: build
 	idris --install lightyear.ipkg
 
+dependencies:
+	mkdir dependencies
+	(cd dependencies; git clone https://github.com/pheymann/specdris; git fetch; cd specdris; git checkout v0.2.2; ./project --build; cd ../..)
+
 build: Lightyear/*.idr
 	idris --build lightyear.ipkg
 
 test: build
-	(cd tests; bash runtests.sh)
+	(cd tests; idris --clean test.ipkg; idris --testpkg test.ipkg --idrispath ../dependencies/specdris/src)
+
+testCI: dependencies
+	(cd tests; idris --clean test.ipkg; idris --testpkg test.ipkg --idrispath ../dependencies/specdris/src)
 
 clean:
 	idris --clean lightyear.ipkg

default.nix

@@ -0,0 +1,11 @@
+# This is used in the Travis build to install the Idris compiler.
+let
+  pkgs = import <nixpkgs> {};
+  stdenv = pkgs.stdenv;
+in {
+  lightyear = stdenv.mkDerivation {
+    name = "lightyear";
+    src = ./.;
+    buildInputs = with pkgs; [ haskellPackages.idris gmp ];
+  };
+}

tests/JsonTest.idr

@@ -2,44 +2,36 @@ module JsonTest
 
 import Json
 
-import Lightyear.Testing
+import TestUtil
+import Specdris.Spec
 
-%access export
-
-test : String -> IO ()
-test s = case parse jsonToplevelValue s of
-  Left err => putStrLn $ "error: " ++ err
-  Right v  => printLn v
-
-jsonTests : IO ()
-jsonTests = runTests
-  [ parseTestCmpShow
-      "JSON 1"
-      jsonToplevelValue
-      "[1,2,4,[5,6],null,{\"some\":[\"object\"]},false]"
-      "[1, 2, 4, [5, 6], null, {\"some\": [\"object\"]}, false]"
-  , parseTestCmpShow
-      "JSON 2"
-      jsonToplevelValue
-      "{\n  \"hallo\":42,\"nichts\":null}"
-      "{\"hallo\": 42, \"nichts\": null}"
-
-  , parseTestCmpShow
-      "JSON 3"
-      jsonToplevelValue
-      "{\"hello\": [{\"world\": false}, 3, \"string\", true, null]}"
-      "{\"hello\": [{\"world\": false}, 3, \"string\", true, null]}"
-
-  , parseTestCmpNot
-      "JSON 4"
-      jsonToplevelValue
-      "{{\n  \"hallo\":42,\"nichts\":null}"
-      """At 1:1:
+export
+specs : SpecTree
+specs = describe "Json parser (data from examples)" $ do
+         it "JSON 1" $ do
+           shouldParseEqShow 
+             jsonToplevelValue
+             "[1,2,4,[5,6],null,{\"some\":[\"object\"]},false]"
+             "[1, 2, 4, [5, 6], null, {\"some\": [\"object\"]}, false]"
+         it "JSON 2" $ do
+           shouldParseEqShow
+             jsonToplevelValue
+             "{\n  \"hallo\":42,\"nichts\":null}"
+             "{\"hallo\": 42, \"nichts\": null}"
+         it "JSON 3" $ do
+           shouldParseEqShow
+             jsonToplevelValue
+             "{\"hello\": [{\"world\": false}, 3, \"string\", true, null]}"
+             "{\"hello\": [{\"world\": false}, 3, \"string\", true, null]}"
+         it "JSON 4" $ do
+           shouldNotParseEq
+             jsonToplevelValue
+             "{{\n  \"hallo\":42,\"nichts\":null}"
+             """At 1:1:
 	character '['
 At 1:1:
 	a different token
 At 1:2:
 	character '}'
 At 1:2:
 	a different token"""
-  ]

tests/ParserTest.idr

@@ -0,0 +1,33 @@
+module ParserTest
+
+import Data.Vect
+import Data.Fin
+
+import Lightyear
+import Lightyear.Char
+import Lightyear.Strings
+
+import TestUtil
+import Specdris.Spec
+
+listOf : Parser a -> Parser (List a)
+listOf p = string "[" *!> (p `sepBy` string ",") <* string "]"
+
+listOf' : Parser a -> Parser (List a)
+listOf' p = brackets (commaSep p)
+
+export
+specs : SpecTree
+specs = describe "Parser" $ do
+         it "parse scalar values" $ do
+           shouldParseEq integer "123" 123
+         it "parse recursive structures" $ do
+           shouldParseEq (listOf integer) "[1,2,3,98]" [1, 2, 3, 98]
+           shouldParseEq (listOf' integer) "[1,2,3,99]" [1, 2, 3, 99]
+         it "parse nested structures" $ do
+           shouldParseEq (listOf $ listOf integer) "[[1,2],[],[3,4,5]]" [[1, 2], [], [3, 4, 5]]
+           shouldParseEq (listOf' $ listOf integer) "[[1,2],[],[3,4,5,6]]" [[1, 2], [], [3, 4, 5, 6]]
+         it "should commit and fail" $ do
+           shouldNotParseEq (listOf integer) "foo" "At 1:1:\n\tstring \"[\"\nAt 1:1:\n\tcharacter '['\nAt 1:1:\n\ta different token"         
+           shouldParseEq (listOf' integer <|> (string "[foo" *> pure List.Nil)) "[foo" []
+           shouldNotParseEq (listOf integer <|> (string "[foo" *> pure List.Nil)) "[foo" "At 1:2:\n\tstring \"]\"\nAt 1:2:\n\tcharacter ']'\nAt 1:2:\n\ta different token"

tests/SpecSuite.idr

@@ -0,0 +1,13 @@
+module SpecSuite
+
+import ParserTest
+import JsonTest
+import TestLazy
+
+import Specdris.Spec
+
+export
+specSuite : IO ()
+specSuite = spec $ do ParserTest.specs
+                      JsonTest.specs
+                      TestLazy.specs

tests/TestLazy.idr

@@ -5,13 +5,13 @@ import Lightyear.Char
 import Lightyear.Strings
 import Lightyear.Testing
 
+import TestUtil
+import Specdris.Spec
+
 %default partial
-%access export
 
-public export
 data Ty = ATOM | EXPR
 
-export
 data SExpr : Ty -> Type where
   Atom : String -> SExpr ATOM
   AtomExpr : SExpr ATOM -> SExpr EXPR
@@ -21,10 +21,6 @@ Show (SExpr ty) where
   show (Atom a) = unwords ["Atom", a]
   show (Expr a b) = unwords ["Expr", show a, show b]
 
-Show (SExpr ty) => Show (ty : Ty ** SExpr ty) where
-  show (x ** pf) {ty = ATOM} = show pf
-  show (x ** pf) {ty = EXPR} = show pf
-
 atom : Parser $ SExpr ATOM
 atom = do
   cs <- some $ satisfy isAlphaNum
@@ -44,15 +40,9 @@ expr = do
    pure $ Expr exprA exprB
  <?> "EXPR"
 
-tests : IO ()
-tests = runTests
-  [ parseTest "Atoms"          atom "Test"
-  , parseTest "Numbers"        atom "1"
-  , parseTest "Simple Expr 1"  expr "Test"
-  , parseTest "Simple Expr 2"  expr "(id x)"
-  , parseTest "Complex Expr 1" expr "(add (1 2))"
-  , parseTest "Complex Expr 2" expr "(a (b (c (d (e (f (g (h (i (j (k (l (m (n (o (p (q (r (s (t (u (v (w (x (y (z NIL))))))))))))))))))))))))))"
-  , parseTestNot "Complex Expr 3" expr """(a
+complex1 : String
+complex1 = 
+  """(a
   (b
     (c
       (d
@@ -67,9 +57,10 @@ tests = runTests
                         (m
                           (n (o (p (q (r (s (t (u (v (w (x (y (z NIL))))))))))))))))))))))))))
 """
-  , parseTestCmpNot "Complex Expr 4"
-                    expr
-                    """(a
+
+complex2 : String
+complex2 =
+  """(a
   (b
     (c
       (d
@@ -83,7 +74,10 @@ tests = runTests
                       (l
                         (m
                           (n (o (p (q (r (s (t (u (v (w (x (y (z NIL))))))))))))))))))))))))))"""
-                          """At 1:1:
+
+complex2Error : String
+complex2Error =
+  """At 1:1:
 	EXPR
 At 1:1:
 	Atom
@@ -121,4 +115,18 @@ At 6:12:
 	character ')'
 At 6:12:
 	a different token"""
-  ]
+
+export
+specs : SpecTree
+specs = describe "Lazy evaluation" $ do
+          it "parse atomic expressions" $ do
+            shouldParse atom "Test"
+            shouldParse atom "1"
+          it "parse simple expressions" $ do
+            shouldParse expr "Test"
+            shouldParse expr "(id x)"
+          it "parse complexe expressions" $ do
+            shouldParse expr "(add (1 2))"
+            shouldParse expr "(a (b (c (d (e (f (g (h (i (j (k (l (m (n (o (p (q (r (s (t (u (v (w (x (y (z NIL))))))))))))))))))))))))))"         
+            shouldNotParse expr complex1 
+            shouldNotParseEq expr complex2 complex2Error

tests/TestUtil.idr

@@ -0,0 +1,35 @@
+module TestUtil
+
+import Lightyear
+import Lightyear.Char
+import Lightyear.Strings
+
+import Specdris.Spec
+
+%access export
+%default total
+
+shouldParse : (Show a) => Parser a -> (raw : String) -> SpecResult
+shouldParse p raw = case parse p raw of
+                      (Left err) => (UnaryFailure raw err)
+                      (Right _)  => Success
+
+shouldNotParse : (Show a) => Parser a -> (raw : String) -> SpecResult
+shouldNotParse p raw = case parse p raw of
+                         (Left _)       => Success
+                         (Right actual) => (UnaryFailure raw "should fail")
+
+shouldParseEq : (Show a, Eq a) => Parser a -> (raw : String) -> (expected : a) -> SpecResult
+shouldParseEq p raw expected = case parse p raw of
+                                 (Left err)     => (BinaryFailure raw expected err)
+                                 (Right actual) => actual === expected
+
+shouldParseEqShow : Show a => Parser a -> (raw : String) -> (expected : String) -> SpecResult
+shouldParseEqShow p raw expected = case parse p raw of
+                                     (Left err)     => (BinaryFailure raw expected err)
+                                     (Right actual) => (show actual) === expected
+
+shouldNotParseEq : Show a => Parser a -> (raw : String) -> (expected : String) -> SpecResult
+shouldNotParseEq p raw expected = case parse p raw of
+                                    (Left actual)  => actual === expected
+                                    (Right err)    => (BinaryFailure err expected "should fail")