Add test script

They don't all pass yet, for minor reasons. Coming shortly...
Unfortunately the startup overhead for chez is really noticeable here!

Makefile

@@ -1,7 +1,7 @@
 include config.mk
 
 # Idris 2 executable used to bootstrap
-IDRIS2_BOOT ?= idris2
+export IDRIS2_BOOT ?= idris2
 
 # Idris 2 executable we're building
 NAME = idris2sh
@@ -59,6 +59,9 @@ contrib: prelude
 
 libs : prelude base network contrib
 
+test:
+	@${MAKE} -C tests only=$(only) IDRIS2=../../../${TARGET}
+
 support:
 	@${MAKE} -C support/c
 

tests/Main.idr

@@ -0,0 +1,283 @@
+module Main
+
+import Data.Maybe
+import Data.List
+import Data.Strings
+
+import System
+import System.Directory
+import System.File
+
+%default covering
+
+------------------------------------------------------------------------
+-- Test cases
+
+ttimpTests : List String
+ttimpTests
+    = ["basic001", "basic002", "basic003", "basic004", "basic005",
+       "basic006",
+       "coverage001", "coverage002",
+       "dot001",
+       "eta001", "eta002",
+       "lazy001",
+       "nest001", "nest002",
+       "perf001", "perf002", "perf003",
+       "record001", "record002", "record003",
+       "rewrite001",
+       "qtt001", "qtt002", "qtt003",
+       "search001", "search002", "search003", "search004", "search005",
+       "total001", "total002", "total003",
+       "with001"]
+
+idrisTests : List String
+idrisTests
+    = -- Fundamental language feturea
+      ["basic001", "basic002", "basic003", "basic004", "basic005",
+       "basic006", "basic007", "basic008", "basic009", "basic010",
+       "basic011", "basic012", "basic013", "basic014", "basic015",
+       "basic016", "basic017", "basic018", "basic019", "basic020",
+       "basic021", "basic022", "basic023", "basic024", "basic025",
+       "basic026", "basic027", "basic028", "basic029", "basic030",
+       "basic031", "basic032", "basic033", "basic034", "basic035",
+       "basic036", "basic037", "basic038", "basic039", "basic040",
+       -- Coverage checking
+       "coverage001", "coverage002", "coverage003", "coverage004",
+       "coverage005", "coverage006",
+       -- Error messages
+       "error001", "error002", "error003", "error004", "error005",
+       "error006", "error007", "error008", "error009", "error010",
+       -- Modules and imports
+       "import001", "import002", "import003", "import004",
+       -- Interactive editing support
+       "interactive001", "interactive002", "interactive003", "interactive004",
+       "interactive005", "interactive006", "interactive007", "interactive008",
+       "interactive009", "interactive010", "interactive011", "interactive012",
+       -- Literate
+       "literate001", "literate002", "literate003", "literate004",
+       "literate005", "literate006", "literate007", "literate008",
+       "literate009", "literate010", "literate011", "literate012",
+       -- Interfaces
+       "interface001", "interface002", "interface003", "interface004",
+       "interface005", "interface006", "interface007", "interface008",
+       "interface009", "interface010", "interface011", "interface012",
+       "interface013", "interface014", "interface015",
+       -- Miscellaneous REPL
+       "interpreter001",
+       -- Implicit laziness, lazy evaluation
+       "lazy001",
+       -- QTT and linearity related
+       "linear001", "linear002", "linear003", "linear004", "linear005",
+       "linear006", "linear007", "linear008",
+       -- Parameters blocks
+       "params001",
+       -- Performance: things which have been slow in the past, or which
+       -- pose interesting challenges for the elaborator
+       "perf001", "perf002", "perf003", "perf004",
+       -- Parse errors
+       "perror001", "perror002", "perror003", "perror004", "perror005",
+       "perror006",
+       -- Packages and ipkg files
+       "pkg001", "pkg002",
+       -- Larger programs arising from real usage. Typically things with
+       -- interesting interactions between features
+       "real001", "real002",
+       -- Records, access and dependent update
+       "record001", "record002", "record003", "record004",
+       -- Miscellaneous regressions
+       "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
+       "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
+       "reg015", "reg016", "reg017", "reg018", "reg019",
+       -- Totality checking
+       "total001", "total002", "total003", "total004", "total005",
+       "total006",
+       -- The 'with' rule
+       "with001", "with002"]
+
+typeddTests : List String
+typeddTests
+   = ["chapter01", "chapter02", "chapter03", "chapter04", "chapter05",
+      "chapter06", "chapter07", "chapter08", "chapter09", "chapter10",
+      "chapter11", "chapter12", "chapter13", "chapter14"]
+
+chezTests : List String
+chezTests
+   = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
+      "chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
+      "chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
+      "reg001"]
+
+ideModeTests : List String
+ideModeTests
+  =  [ "ideMode001", "ideMode002", "ideMode003" ]
+
+------------------------------------------------------------------------
+-- Options
+
+||| Options for the test driver.
+record Options where
+  constructor MkOptions
+  ||| Name of the idris2 executable
+  idris2      : String
+  ||| Should we only run some specific cases?
+  onlyNames   : List String
+  ||| Should we run the test suite interactively?
+  interactive : Bool
+
+usage : String
+usage = "Usage: runtests <idris2 path> [--interactive] [--only [NAMES]]"
+
+options : List String -> Maybe Options
+options args = case args of
+    (_ :: idris2 :: rest) => go rest (MkOptions idris2 [] False)
+    _ => Nothing
+
+  where
+
+    go : List String -> Options -> Maybe Options
+    go rest opts = case rest of
+      []                      => pure opts
+      ("--interactive" :: xs) => go xs (record { interactive = True } opts)
+      ("--only" :: xs)        => pure $ record { onlyNames = xs } opts
+      _ => Nothing
+
+------------------------------------------------------------------------
+-- Actual test runner
+
+fail : String -> IO ()
+fail err
+    = do putStrLn err
+         exitWith (ExitFailure 1)
+
+runTest : Options -> String -> IO Bool
+runTest opts testPath
+    = do changeDir testPath
+         isSuccess <- runTest'
+         changeDir "../.."
+         pure isSuccess
+    where
+        getAnswer : IO Bool
+        getAnswer = do
+          str <- getLine
+          case str of
+            "y" => pure True
+            "n" => pure False
+            _   => do putStrLn "Invalid Answer."
+                      getAnswer
+
+        printExpectedVsOutput : String -> String -> IO ()
+        printExpectedVsOutput exp out = do
+          putStrLn "Expected:"
+          printLn exp
+          putStrLn "Given:"
+          printLn out
+
+        mayOverwrite : Maybe String -> String -> IO ()
+        mayOverwrite mexp out = do
+          the (IO ()) $ case mexp of
+            Nothing => putStr $ unlines
+              [ "Golden value missing. I computed the following result:"
+              , out
+              , "Accept new golden value? [yn]"
+              ]
+            Just exp => do
+              putStrLn "Golden value differs from actual value."
+              code <- system "git diff expected output"
+              when (code /= 0) $ printExpectedVsOutput exp out
+              putStrLn "Accept actual value as new golden value? [yn]"
+          b <- getAnswer
+          when b $ do Right _ <- writeFile "expected" out
+                          | Left err => print err
+                      pure ()
+
+        runTest' : IO Bool
+        runTest'
+            = do putStr $ testPath ++ ": "
+                 system $ "sh ./run " ++ idris2 opts ++ " | tr -d '\\r' > output"
+                 Right out <- readFile "output"
+                     | Left err => do print err
+                                      pure False
+                 Right exp <- readFile "expected"
+                     | Left FileNotFound => do
+                         if interactive opts
+                           then mayOverwrite Nothing out
+                           else print FileNotFound
+                         pure False
+                     | Left err => do print err
+                                      pure False
+
+                 if (out == exp)
+                    then putStrLn "success"
+                    else do
+                      putStrLn "FAILURE"
+                      if interactive opts
+                         then mayOverwrite (Just exp) out
+                         else printExpectedVsOutput exp out
+
+                 pure (out == exp)
+
+exists : String -> IO Bool
+exists f
+    = do Right ok <- openFile f Read
+             | Left err => pure False
+         closeFile ok
+         pure True
+
+firstExists : List String -> IO (Maybe String)
+firstExists [] = pure Nothing
+firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
+
+pathLookup : IO (Maybe String)
+pathLookup = do
+  path <- getEnv "PATH"
+  let pathList = split (== ':') $ fromMaybe "/usr/bin:/usr/local/bin" path
+  let candidates = [p ++ "/" ++ x | p <- pathList,
+                                    x <- ["chez", "chezscheme9.5", "scheme"]]
+  firstExists candidates
+
+findChez : IO (Maybe String)
+findChez
+    = do Just chez <- getEnv "CHEZ" | Nothing => pathLookup
+         pure $ Just chez
+
+runChezTests : Options -> List String -> IO (List Bool)
+runChezTests opts tests
+    = do chexec <- findChez
+         maybe (do putStrLn "Chez Scheme not found"
+                   pure [])
+               (\c => do putStrLn $ "Found Chez Scheme at " ++ c
+                         traverse (runTest opts) tests)
+               chexec
+
+filterTests : Options -> List String -> List String
+filterTests opts = case onlyNames opts of
+  [] => id
+  xs => filter (\ name => any (`isInfixOf` name) xs)
+
+main : IO ()
+main
+    = do args <- getArgs
+         let (Just opts) = options args
+              | _ => do print args
+                        putStrLn usage
+         let filteredNonCGTests =
+              filterTests opts $ concat
+                 [ testPaths "ttimp" ttimpTests
+                 , testPaths "idris2" idrisTests
+                 , testPaths "typedd-book" typeddTests
+                 , testPaths "ideMode" ideModeTests
+                 ]
+         let filteredChezTests = filterTests opts (testPaths "chez" chezTests)
+         nonCGTestRes <- traverse (runTest opts) filteredNonCGTests
+         chezTestRes <- if length filteredChezTests > 0
+              then runChezTests opts filteredChezTests
+              else pure []
+         let res = nonCGTestRes ++ chezTestRes
+         putStrLn (show (length (filter id res)) ++ "/" ++ show (length res)
+                       ++ " tests successful")
+         if (any not res)
+            then exitWith (ExitFailure 1)
+            else exitWith ExitSuccess
+    where
+         testPaths : String -> List String -> List String
+         testPaths dir tests = map (\test => dir ++ "/" ++ test) tests

tests/Makefile

@@ -0,0 +1,9 @@
+INTERACTIVE ?= --interactive
+
+test:
+	${IDRIS2_BOOT} --build tests.ipkg
+	@./build/exec/runtests $(IDRIS2) $(INTERACTIVE) --only $(only)
+
+clean:
+	find . -name '*.ibc' | xargs rm -f
+	find . -name 'output' | xargs rm -f

tests/README.md

@@ -0,0 +1,13 @@
+Tests
+=====
+
+*Note: The commands listed in this section should be run from the repository's root folder.*
+
+Run all tests: `make test`
+
+To run only a subset of the tests use: `make test only=NAME`. `NAME` is matched against the path to each test case.
+
+Examples:
+- `make test only=chez` will run all Chez Scheme tests.
+- `make test only=ttimp/basic` will run all basic tests for `TTImp`.
+- `make test only=idris2/basic001` will run a specific test.

tests/chez/chez001/Total.idr

@@ -0,0 +1,30 @@
+count : Nat -> Stream Nat
+count n = n :: count (S n)
+
+badCount : Nat -> Stream Nat
+badCount n = n :: map S (badCount n)
+
+data SP : Type -> Type -> Type where
+  Get : (a -> SP a b) -> SP a b
+  Put : b -> Inf (SP a b) -> SP a b
+
+copy : SP a a
+copy = Get (\x => Put x copy)
+
+process : SP a b -> Stream a -> Stream b
+process (Get f) (x :: xs) = process (f x) xs
+process (Put b sp) xs = b :: process sp xs
+
+badProcess : SP a b -> Stream a -> Stream b
+badProcess (Get f) (x :: xs) = badProcess (f x) xs
+badProcess (Put b sp) xs = badProcess sp xs
+
+doubleInt : SP Nat Integer
+doubleInt = Get (\x => Put (the Integer (cast x))
+                        (Put (the Integer (cast x) * 2) doubleInt))
+
+countStream : Nat -> Stream Nat
+countStream x = x :: countStream (x + 1)
+
+main : IO ()
+main = printLn (take 10 (process doubleInt (countStream 1)))

tests/chez/chez001/expected

@@ -0,0 +1,3 @@
+[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]
+1/1: Building Total (Total.idr)
+Main> Main> Bye for now!

tests/chez/chez001/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez001/run

@@ -0,0 +1,3 @@
+$1 --no-banner Total.idr < input
+
+rm -rf build

tests/chez/chez002/Pythag.idr

@@ -0,0 +1,9 @@
+range : Integer -> Integer -> List Integer
+range bottom top
+    = if bottom > top then []
+         else bottom :: range (bottom + 1) top
+
+pythag : Integer -> List (Integer, Integer, Integer)
+pythag top
+   = [(x, y, z) | z <- range 1 top, y <- range 1 z, x <- range 1 y,
+                  x * x + y * y == z * z]

tests/chez/chez002/expected

@@ -0,0 +1,3 @@
+[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))]
+1/1: Building Pythag (Pythag.idr)
+Main> Main> Bye for now!

tests/chez/chez002/input

@@ -0,0 +1,2 @@
+:exec printLn (pythag 200)
+:q

tests/chez/chez002/run

@@ -0,0 +1,2 @@
+$1 --no-banner Pythag.idr < input
+rm -rf build

tests/chez/chez003/IORef.idr

@@ -0,0 +1,16 @@
+import Data.IORef
+
+main : IO ()
+main
+    = do x <- newIORef 42
+         let y = x
+         writeIORef y 94
+         val <- readIORef x
+         printLn val
+         val <- readIORef y
+         printLn val
+         modifyIORef x (* 2)
+         val <- readIORef x
+         printLn val
+         val <- readIORef y
+         printLn val

tests/chez/chez003/expected

@@ -0,0 +1,6 @@
+94
+94
+188
+188
+1/1: Building IORef (IORef.idr)
+Main> Main> Bye for now!

tests/chez/chez003/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez003/run

@@ -0,0 +1,2 @@
+$1 --no-banner IORef.idr < input
+rm -rf build

tests/chez/chez004/Buffer.idr

@@ -0,0 +1,50 @@
+import Data.Buffer
+import System.File
+
+main : IO ()
+main
+    = do Just buf <- newBuffer 100
+              | Nothing => putStrLn "Buffer creation failed"
+         s <- rawSize buf
+         printLn s
+
+         setInt32 buf 1 94
+         setString buf 5 "AAAA"
+         val <- getInt32 buf 1
+         printLn val
+
+         setDouble buf 10 94.42
+         val <- getDouble buf 10
+         printLn val
+
+         setString buf 20 "Hello there!"
+         val <- getString buf 20 5
+         printLn val
+
+         val <- getString buf 26 6
+         printLn val
+
+         ds <- bufferData buf
+         printLn ds
+
+         Right _ <- writeBufferToFile "test.buf" buf 100
+             | Left err => putStrLn "Buffer write fail"
+         Right buf2 <- createBufferFromFile "test.buf"
+             | Left err => putStrLn "Buffer read fail"
+
+         ds <- bufferData buf2
+         printLn ds
+
+         freeBuffer buf
+         freeBuffer buf2
+
+-- Put back when the File API is moved to C and these can work again
+--          Right f <- openBinaryFile "test.buf" Read
+--              | Left err => putStrLn "File error on read"
+--          Just buf3 <- newBuffer 99
+--               | Nothing => putStrLn "Buffer creation failed"
+--          Right _ <- readBufferFromFile f buf3 100
+--              | Left err => do putStrLn "Buffer read fail"
+--                               closeFile f
+--          closeFile f
+

tests/chez/chez004/expected

@@ -0,0 +1,9 @@
+100
+94
+94.42
+"Hello"
+"there!"
+[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
+[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
+1/1: Building Buffer (Buffer.idr)
+Main> Main> Bye for now!

tests/chez/chez004/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez004/run

@@ -0,0 +1,2 @@
+$1 --no-banner Buffer.idr < input
+rm -rf build test.buf

tests/chez/chez005/Filter.idr

@@ -0,0 +1,29 @@
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+Show a => Show (Vect n a) where
+  show xs = "[" ++ showV xs ++ "]"
+    where
+      showV : forall n . Vect n a -> String
+      showV [] = ""
+      showV [x] = show x
+      showV (x :: xs) = show x ++ ", " ++ showV xs
+
+filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
+filter pred [] = (_ ** [])
+filter pred (x :: xs)
+    = let (n ** xs') = filter pred xs in
+          if pred x
+             then (_ ** x :: xs')
+             else (_ ** xs')
+
+test : (x ** Vect x Nat)
+test = (_ ** [1,2])
+
+foo : String
+foo = show test
+
+even : Nat -> Bool
+even Z = True
+even (S k) = not (even k)

tests/chez/chez005/expected

@@ -0,0 +1,3 @@
+(3 ** [2, 4, 6])
+1/1: Building Filter (Filter.idr)
+Main> Main> Bye for now!

tests/chez/chez005/input

@@ -0,0 +1,2 @@
+:exec printLn (filter even [S Z,2,3,4,5,6])
+:q

tests/chez/chez005/run

@@ -0,0 +1,3 @@
+$1 --no-banner Filter.idr < input
+
+rm -rf build

tests/chez/chez006/TypeCase.idr

@@ -0,0 +1,31 @@
+data Bar = MkBar
+data Baz = MkBaz
+
+foo : (x : Type) -> String
+foo Nat = "Nat"
+foo Bool = "Bool"
+foo (List x) = "List of " ++ foo x
+foo Int = "Int"
+foo Type = "Type"
+foo _ = "Something else"
+
+strangeId : {a : Type} -> a -> a
+strangeId {a=Integer} x = x+1
+strangeId x = x
+
+strangeId' : {a : Type} -> a -> a
+strangeId' {a=Integer} x = x+1
+
+main : IO ()
+main = do printLn (foo Nat)
+          printLn (foo (List Nat))
+          printLn (foo (List Bar))
+          printLn (foo (List Baz))
+          printLn (foo (List Bool))
+          printLn (foo Int)
+          printLn (foo String)
+          printLn (foo (List Type))
+          printLn (foo (List Int))
+          printLn (strangeId 42)
+          printLn (strangeId (the Int 42))
+

tests/chez/chez006/TypeCase2.idr

@@ -0,0 +1,14 @@
+data Bar = MkBar
+data Baz = MkBaz
+
+strangeId : a -> a
+strangeId {a=Nat} x = x+1
+strangeId x = x
+
+foo : (0 x : Type) -> String
+foo Nat = "Nat"
+foo Bool = "Bool"
+foo (List x) = "List of " ++ foo x
+foo Int = "Int"
+foo Type = "Type"
+foo _ = "Something else"

tests/chez/chez006/expected

@@ -0,0 +1,21 @@
+"Nat"
+"List of Nat"
+"List of Something else"
+"List of Something else"
+"List of Bool"
+"Int"
+"Something else"
+"List of Type"
+"List of Int"
+43
+42
+1/1: Building TypeCase (TypeCase.idr)
+Main> Main> Main.strangeId is total
+Main> Main.strangeId':
+strangeId' _
+Main> Bye for now!
+1/1: Building TypeCase2 (TypeCase2.idr)
+TypeCase2.idr:5:14--5:17:While processing left hand side of strangeId at TypeCase2.idr:5:1--6:1:
+Can't match on Nat (Erased argument)
+TypeCase2.idr:9:5--9:9:While processing left hand side of foo at TypeCase2.idr:9:1--10:1:
+Can't match on Nat (Erased argument)

tests/chez/chez006/input

@@ -0,0 +1,4 @@
+:exec main
+:total strangeId
+:missing strangeId'
+:q

tests/chez/chez006/run

@@ -0,0 +1,4 @@
+$1 --no-banner TypeCase.idr < input
+$1 --no-banner TypeCase2.idr --check
+
+rm -rf build

tests/chez/chez007/TypeCase.idr

@@ -0,0 +1,26 @@
+data Bar = MkBar
+data Baz = MkBaz
+
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+desc : Type -> String
+desc Int = "Int"
+desc Nat = "Nat"
+desc (Vect n a) = "Vector of " ++ show n ++ " " ++ desc a
+desc Type = "Type"
+desc _ = "Something else"
+
+descNat : Type -> String
+descNat t = "Function from Nat to " ++ desc t
+
+descFn : (x : Type) -> String
+descFn ((x : Nat) -> b) = descNat (b Z)
+descFn (a -> b) = "Function on " ++ desc a
+descFn x = desc x
+
+main : IO ()
+main = do printLn (descFn (Nat -> Nat))
+          printLn (descFn ((x : Nat) -> Vect x Int))
+          printLn (descFn (Type -> Int))

tests/chez/chez007/expected

@@ -0,0 +1,5 @@
+"Function from Nat to Nat"
+"Function from Nat to Vector of 0 Int"
+"Function on Type"
+1/1: Building TypeCase (TypeCase.idr)
+Main> Main> Bye for now!

tests/chez/chez007/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez007/run

@@ -0,0 +1,3 @@
+$1 --no-banner TypeCase.idr < input
+
+rm -rf build

tests/chez/chez008/Nat.idr

@@ -0,0 +1,11 @@
+myS : Nat -> Nat
+myS n = S n
+
+myS_crash : Nat -> Nat
+myS_crash = S
+
+main : IO ()
+main = do
+  printLn (S Z)
+  printLn (myS Z)
+  printLn (myS_crash Z)

tests/chez/chez008/expected

@@ -0,0 +1,5 @@
+1
+1
+1
+1/1: Building Nat (Nat.idr)
+Main> Main> Bye for now!

tests/chez/chez008/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez008/run

@@ -0,0 +1,3 @@
+$1 --no-banner Nat.idr < input
+
+rm -rf build

tests/chez/chez009/expected

@@ -0,0 +1,4 @@
+42
+ällo
+1/1: Building uni (uni.idr)
+Main> Main> Bye for now!

tests/chez/chez009/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez009/run

@@ -0,0 +1,3 @@
+$1 --no-banner uni.idr < input
+
+rm -rf build

tests/chez/chez009/uni.idr

@@ -0,0 +1,9 @@
+foo : String
+foo = "ällo"
+
+ällo : Int
+ällo = 42
+
+main : IO ()
+main = do printLn ällo
+          putStrLn "ällo"

tests/chez/chez010/.gitignore

@@ -0,0 +1,6 @@
+*.d
+*.o
+*.obj
+*.so
+*.dylib
+*.dll

tests/chez/chez010/CB.idr

@@ -0,0 +1,39 @@
+libcb : String -> String
+libcb f = "C:" ++ f ++", libcb"
+
+%foreign libcb "add"
+add : Int -> Int -> Int
+
+%foreign libcb "applyIntFn"
+prim_applyIntFn : Int -> Int -> (Int -> Int -> PrimIO Int) -> PrimIO Int
+
+%foreign libcb "applyCharFn"
+prim_applyCharFn : Char -> Int -> (Char -> Int -> PrimIO Char) -> PrimIO Char
+
+%foreign libcb "applyIntFnPure"
+applyIntFnPure : Int -> Int -> (Int -> Int -> Int) -> Int
+
+applyIntFn : Int -> Int -> (Int -> Int -> IO Int) -> IO Int
+applyIntFn x y fn
+    = primIO $ prim_applyIntFn x y (\a, b => toPrim (fn a b))
+
+applyCharFn : Char -> Int -> (Char -> Int -> IO Char) -> IO Char
+applyCharFn x y fn
+    = primIO $ prim_applyCharFn x y (\a, b => toPrim (fn a b))
+
+cb : Int -> Int -> IO Int
+cb x y
+    = do putStrLn $ "In callback with " ++ show (x, y)
+         pure (x + y)
+
+main : IO ()
+main
+    = do printLn (add 4 5)
+         res <- applyIntFn (add 4 5) 6 (\x, y => do putStrLn "In callback"
+                                                    pure (x * 2 + y))
+         printLn res
+         res <- applyIntFn 1 2 cb
+         printLn res
+         printLn (applyIntFnPure 5 4 (\x, y => x + y))
+         res <- applyCharFn 'a' 10 (\x, y => pure (cast (cast x + y)))
+         printLn res

tests/chez/chez010/Makefile

@@ -0,0 +1,28 @@
+include $(IDRIS2_CURDIR)/config.mk
+
+TARGET = libcb
+
+SRCS = $(wildcard *.c)
+OBJS = $(SRCS:.c=.o)
+DEPS = $(OBJS:.o=.d)
+
+
+all: $(TARGET)$(SHLIB_SUFFIX)
+
+$(TARGET)$(SHLIB_SUFFIX): $(OBJS)
+	$(CC) -shared $(LDFLAGS) -o $@ $^
+
+
+-include $(DEPS)
+
+%.d: %.c
+	@$(CPP) $(CFLAGS) $< -MM -MT $(@:.d=.o) >$@
+
+
+.PHONY: clean
+
+clean :
+	rm -f $(OBJS) $(TARGET)$(SHLIB_SUFFIX)
+
+cleandep: clean
+	rm -f $(DEPS)

tests/chez/chez010/cblib.c

@@ -0,0 +1,23 @@
+#include <stdio.h>
+
+typedef int(*IntFn)(int, int);
+typedef char(*CharFn)(char, int);
+
+int add(int x, int y) {
+    return x+y;
+}
+
+int applyIntFn(int x, int y, IntFn f) {
+    printf("Callback coming\n");
+    fflush(stdout);
+    return f(x, y);
+}
+
+int applyIntFnPure(int x, int y, IntFn f) {
+    return f(x, y);
+}
+
+char applyCharFn(char c, int x, CharFn f) {
+    return f(c, x);
+}
+

tests/chez/chez010/expected

@@ -0,0 +1,11 @@
+9
+Callback coming
+In callback
+24
+Callback coming
+In callback with (1, 2)
+3
+9
+'k'
+1/1: Building CB (CB.idr)
+Main> Main> Bye for now!

tests/chez/chez010/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez010/run

@@ -0,0 +1,4 @@
+make all > /dev/null
+$1 --no-banner CB.idr < input
+rm -rf build
+make clean > /dev/null

tests/chez/chez011/bangs.idr

@@ -0,0 +1,32 @@
+
+add : Int -> Int -> Int
+add = (+)
+
+-- lift to nearest binder
+addm1 : Maybe Int -> Maybe Int -> Maybe Int
+addm1 x y = let z = x in pure (add !z !y)
+
+-- lift to nearest binder
+addm2 : Maybe Int -> Maybe Int -> Maybe Int
+addm2 = \x, y => pure (!x + !y)
+
+getLen : String -> IO Nat
+getLen str = pure (length str)
+
+fakeGetLine : String -> IO String
+fakeGetLine str = pure str
+
+-- lift out innermost first
+printThing1 : IO ()
+printThing1 = printLn !(getLen !(fakeGetLine "line1"))
+
+-- lift out leftmost first
+printThing2 : IO ()
+printThing2 = printLn (!(fakeGetLine "1") ++ !(fakeGetLine "2"))
+
+-- don't lift out of if
+printBool : Bool -> IO ()
+printBool x
+    = if x
+         then putStrLn !(fakeGetLine "True")
+         else putStrLn !(fakeGetLine "False")

tests/chez/chez011/expected

@@ -0,0 +1,8 @@
+5
+"12"
+True
+False
+1/1: Building bangs (bangs.idr)
+Main> Just 7
+Main> Just 7
+Main> Main> Main> Main> Main> Bye for now!

tests/chez/chez011/input

@@ -0,0 +1,7 @@
+addm1 (Just 3) (Just 4)
+addm2 (Just 3) (Just 4)
+:exec printThing1
+:exec printThing2
+:exec printBool True
+:exec printBool False
+:q

tests/chez/chez011/run

@@ -0,0 +1,3 @@
+$1 --no-banner bangs.idr < input
+
+rm -rf build

tests/chez/chez012/array.idr

@@ -0,0 +1,11 @@
+import Data.IOArray
+
+main : IO ()
+main
+    = do x <- newArray 20
+         writeArray x 10 "Hello"
+         writeArray x 11 "World"
+         printLn !(toList x)
+
+         y <- fromList (map Just [1,2,3,4,5])
+         printLn !(toList y)

tests/chez/chez012/expected

@@ -0,0 +1,4 @@
+[Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just "Hello", Just "World", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing]
+[Just 1, Just 2, Just 3, Just 4, Just 5]
+1/1: Building array (array.idr)
+Main> Main> Bye for now!

tests/chez/chez012/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez012/run

@@ -0,0 +1,2 @@
+$1 --no-banner array.idr < input
+rm -rf build

tests/chez/chez013/.gitignore

@@ -0,0 +1,7 @@
+*.d
+*.o
+*.obj
+*.so
+*.dylib
+*.dll
+

tests/chez/chez013/Makefile

@@ -0,0 +1,28 @@
+include $(IDRIS2_CURDIR)/config.mk
+
+TARGET = libstruct
+
+SRCS = $(wildcard *.c)
+OBJS = $(SRCS:.c=.o)
+DEPS = $(OBJS:.o=.d)
+
+
+all: $(TARGET)$(SHLIB_SUFFIX)
+
+$(TARGET)$(SHLIB_SUFFIX): $(OBJS)
+	$(CC) -shared $(LDFLAGS) -o $@ $^
+
+
+-include $(DEPS)
+
+%.d: %.c
+	@$(CPP) $(CFLAGS) $< -MM -MT $(@:.d=.o) >$@
+
+
+.PHONY: clean
+
+clean :
+	rm -f $(OBJS) $(TARGET)$(SHLIB_SUFFIX)
+
+cleandep: clean
+	rm -f $(DEPS)

tests/chez/chez013/Struct.idr

@@ -0,0 +1,47 @@
+import System.FFI
+
+pfn : String -> String
+pfn fn = "C:" ++ fn ++ ",libstruct"
+
+Point : Type
+Point = Struct "point" [("x", Int), ("y", Int)]
+
+NamedPoint : Type
+NamedPoint = Struct "namedpoint" [("name", Ptr String), ("pt", Point)]
+
+%foreign (pfn "getString")
+getStr : Ptr String -> String
+
+%foreign (pfn "mkPoint")
+mkPoint : Int -> Int -> Point
+
+%foreign (pfn "freePoint")
+freePoint : Point -> PrimIO ()
+
+%foreign (pfn "mkNamedPoint")
+mkNamedPoint : String -> Point -> PrimIO NamedPoint
+
+%foreign (pfn "freeNamedPoint")
+freeNamedPoint : NamedPoint -> PrimIO ()
+
+showPoint : Point -> String
+showPoint pt
+    = let x : Int = getField pt "x"
+          y : Int = getField pt "y" in
+          show (x, y)
+
+showNamedPoint : NamedPoint -> String
+showNamedPoint pt
+    = let x : String = getStr (getField pt "name")
+          p : Point = getField pt "pt" in
+          show x ++ ": " ++ showPoint p
+
+main : IO ()
+main = do let pt = mkPoint 20 30
+          np <- primIO $ mkNamedPoint "Here" pt
+          setField pt "x" (the Int 40)
+          putStrLn $ showPoint pt
+          putStrLn $ showNamedPoint np
+
+          primIO $ freeNamedPoint np
+          primIO $ freePoint pt

tests/chez/chez013/expected

@@ -0,0 +1,5 @@
+Made it!
+(40, 30)
+"Here": (40, 30)
+1/1: Building Struct (Struct.idr)
+Main> Main> Bye for now!

tests/chez/chez013/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez013/run

@@ -0,0 +1,4 @@
+make all > /dev/null
+$1 --no-banner Struct.idr < input
+rm -rf build
+make clean > /dev/null

tests/chez/chez013/struct.c

@@ -0,0 +1,32 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include "struct.h"
+
+char* getString(void *p) {
+    return (char*)p;
+}
+
+point* mkPoint(int x, int y) {
+    point* pt = malloc(sizeof(point));
+    pt->x = x;
+    pt->y = y;
+    return pt;
+}
+
+void freePoint(point* pt) {
+    free(pt);
+}
+
+namedpoint* mkNamedPoint(char* str, point* p) {
+    namedpoint* np = malloc(sizeof(namedpoint));
+    np->name = str;
+    np->pt = p;
+    printf("Made it!\n");
+
+    return np;
+}
+
+void freeNamedPoint(namedpoint* np) {
+    free(np);
+}
+

tests/chez/chez013/struct.h

@@ -0,0 +1,22 @@
+#ifndef _STRUCT_H
+#define _STRUCT_H
+
+typedef struct {
+    int x;
+    int y;
+} point;
+
+typedef struct {
+    char* name;
+    point* pt;
+} namedpoint;
+
+point* mkPoint(int x, int y);
+void freePoint(point* pt);
+
+namedpoint* mkNamedPoint(char* str, point* p);
+void freeNamedPoint(namedpoint* np);
+
+char* getString(void *p);
+
+#endif

tests/chez/chez014/Echo.idr

@@ -0,0 +1,58 @@
+module Main
+
+import System
+import Network.Socket
+import Network.Socket.Data
+import Network.Socket.Raw
+
+%cg chez libidris_net
+
+runServer : IO (Either String (Port, ThreadID))
+runServer = do
+  Right sock <- socket AF_INET Stream 0
+        | Left fail => pure (Left $ "Failed to open socket: " ++ show fail)
+  res <- bind sock (Just (Hostname "localhost")) 0
+  if res /= 0
+    then pure (Left $ "Failed to bind socket with error: " ++ show res)
+    else do
+      port <- getSockPort sock
+      res <- listen sock
+      if res /= 0
+        then pure (Left $ "Failed to listen on socket with error: " ++ show res)
+        else do
+          forked <- fork (serve port sock)
+          pure $ Right (port, forked)
+
+  where
+    serve : Port -> Socket -> IO ()
+    serve port sock = do
+      Right (s, _) <- accept sock
+        | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
+      Right  (str, _) <- recv s 1024
+        | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
+      putStrLn ("Received: " ++ str)
+      Right n <- send s ("echo: " ++ str)
+        | Left err => putStrLn ("Server failed to send data with error: " ++ show err)
+      pure ()
+
+runClient : Port -> IO ()
+runClient serverPort = do
+  Right sock <- socket AF_INET Stream 0
+    | Left fail => putStrLn ("Failed to open socket: " ++ show fail)
+  res <- connect sock (Hostname "localhost") serverPort
+  if res /= 0
+    then putStrLn ("Failed to connect client to port " ++ show serverPort ++ ": " ++ show res)
+    else do
+      Right n <- send sock ("hello world!")
+        | Left err => putStrLn ("Client failed to send data with error: " ++ show err)
+      Right (str, _) <- recv sock 1024
+        | Left err => putStrLn ("Client failed to receive on socket with error: " ++ show err)
+      -- assuming that stdout buffers get flushed in between system calls, this is "guaranteed"
+      -- to be printed after the server prints its own message
+      putStrLn ("Received: " ++ str)
+
+main : IO ()
+main = do
+  Right (serverPort, tid) <- runServer
+    | Left err => putStrLn $ "[server] " ++ err
+  runClient serverPort

tests/chez/chez014/expected

@@ -0,0 +1,4 @@
+Received: hello world!
+Received: echo: hello world!
+1/1: Building Echo (Echo.idr)
+Main> Main> Bye for now!

tests/chez/chez014/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez014/run

@@ -0,0 +1,3 @@
+$1 --no-banner -p network Echo.idr < input
+
+rm -rf build

tests/chez/chez015/Numbers.idr

@@ -0,0 +1,34 @@
+module Main
+
+import Data.List
+
+large : (a: Type) -> a
+-- integer larger than 64 bits
+large Integer = 3518437212345678901234567890123
+-- int close to 2ˆ63
+-- we expect some operations will overflow
+large Int = 3518437212345678901234567890
+
+small : (a: Type) -> a
+small Integer = 437
+small Int = 377
+
+numOps : (Num a) => List ( a -> a -> a )
+numOps = [ (+), (*) ]
+
+negOps : (Neg a) => List (a -> a -> a)
+negOps = [ (-) ]
+
+integralOps : (Integral a) => List (a -> a -> a)
+integralOps = [ div, mod ]
+
+binOps : (Num a, Neg a, Integral a) => List (a -> a -> a)
+binOps = numOps ++ negOps ++ integralOps
+
+main : IO ()
+main = do
+  putStrLn $ show (results Integer)
+  putStrLn $ show (results Int)
+  where
+  results : (a:Type) -> (Num a, Neg a, Integral a) => List a
+  results a = map (\ op => large a  `op` small a) binOps

tests/chez/chez015/expected

@@ -0,0 +1,4 @@
+[3518437212327232157160858338944, 1537557061787000452679295093927559, 3518437212327232157160858338070, 8051343735302590748651849744, 379]
+[8650625671965379659, 5435549321212129090, 8650625671965378905, 365458446121836181, 357]
+1/1: Building Numbers (Numbers.idr)
+Main> Main> Bye for now!

tests/chez/chez015/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez015/run

@@ -0,0 +1,3 @@
+$1 --no-banner Numbers.idr < input
+
+rm -rf build

tests/chez/chez016/expected

@@ -0,0 +1,3 @@
+Running Chez program located in folder with spaces
+1/1: Building Main (Main.idr)
+Main> Main> Bye for now!

tests/chez/chez016/folder with spaces/Main.idr

@@ -0,0 +1,2 @@
+main : IO ()
+main = putStrLn "Running Chez program located in folder with spaces"

tests/chez/chez016/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez016/run

@@ -0,0 +1,20 @@
+# This test needs to run `idris2` from a sub-folder.
+# Split path to `idris2` executable into dirname and basename.
+# If the path is relative, add `..` to compensate for running `idris2` in a sub-folder.
+case "$1" in
+  /*)
+    # Absolute path
+    IDRIS2_DIR="$(dirname "$1")"
+    ;;
+  *)
+    # Relative path
+    IDRIS2_DIR="$(dirname "$1")/.."
+    ;;
+esac
+
+IDRIS2_EXEC="$(basename "$1")"
+
+cd "folder with spaces" || exit
+
+"$IDRIS2_DIR/$IDRIS2_EXEC" --no-banner Main.idr < ../input
+rm -rf build

tests/chez/chez017/.gitignore

@@ -0,0 +1,2 @@
+/expected
+

tests/chez/chez017/dir.idr

@@ -0,0 +1,15 @@
+import System.Directory
+
+main : IO ()
+main = do Right () <- createDir "testdir"
+               | Left err => printLn err
+          Left err <- createDir "testdir"
+               | _ => printLn "That wasn't supposed to work"
+          printLn err
+          ok <- changeDir "nosuchdir"
+          printLn ok
+          ok <- changeDir "testdir"
+          printLn ok
+          writeFile "test.txt" "hello\n"
+          printLn !currentDir
+

tests/chez/chez017/expected.in

@@ -0,0 +1,7 @@
+File Exists
+False
+True
+Just "__PWD__/testdir"
+1/1: Building dir (dir.idr)
+Main> Main> Bye for now!
+hello

tests/chez/chez017/gen_expected.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env sh
+
+sed -e "s|__PWD__|$(pwd)|g" expected.in > expected

tests/chez/chez017/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez017/run

@@ -0,0 +1,4 @@
+./gen_expected.sh
+$1 --no-banner dir.idr < input
+cat testdir/test.txt
+rm -rf build testdir

tests/chez/chez018/File.idr

@@ -0,0 +1,14 @@
+import System.File
+
+main : IO ()
+main
+    = do Right ok <- readFile "test.txt"
+               | Left err => printLn err
+         putStr ok
+         writeFile "testout.txt" "abc\ndef\n"
+         Right ok <- readFile "testout.txt"
+               | Left err => printLn err
+         putStr ok
+         Right ok <- readFile "notfound"
+               | Left err => printLn err
+         putStr ok

tests/chez/chez018/expected

@@ -0,0 +1,6 @@
+test test
+unfinished lineabc
+def
+File Not Found
+1/1: Building File (File.idr)
+Main> Main> Bye for now!

tests/chez/chez018/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez018/run

@@ -0,0 +1,3 @@
+$1 --no-banner File.idr < input
+
+rm -rf build testout.txt

tests/chez/chez018/test.txt

@@ -0,0 +1,2 @@
+test test
+unfinished line

tests/chez/reg001/expected

@@ -0,0 +1,10 @@
+3
+4.2
+"1.2"
+4
+1
+"2.7"
+5.9
+2
+2
+2

tests/chez/reg001/numbers.idr

@@ -0,0 +1,21 @@
+-- the commented-out cases are still wrong,
+-- but fixing them as well would make other tests fail for mysterious reasons
+-- see https://github.com/edwinb/Idris2/pull/281
+main : IO ()
+main = do
+  printLn $ 3
+  printLn $ 4.2
+  printLn $ "1.2"
+
+  printLn $ cast {to = Int} 4.8
+  printLn $ cast {to = Integer} 1.2
+  printLn $ cast {to = String} 2.7
+
+  -- printLn $ cast {to = Int} "1.2"
+  -- printLn $ cast {to = Integer} "2.7"
+  printLn $ cast {to = Double} "5.9"
+
+  printLn $ (the Int 6 `div` the Int 3)
+  printLn $ (the Integer 6 `div` the Integer 3)
+  printLn $ (cast {to = Int} "6.6" `div` cast "3.9")
+  -- printLn $ (cast {to = Integer} "6.6" `div` cast "3.9")

tests/chez/reg001/run

@@ -0,0 +1,3 @@
+$1 numbers.idr -x main
+
+rm -rf build

tests/ideMode/ideMode001/LocType.idr

@@ -0,0 +1,7 @@
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+append : Vect n a -> Vect m a -> Vect (n + m) a
+append [] ys = ys
+append (x :: xs) ys = x :: append xs ys

tests/ideMode/ideMode001/expected

@@ -0,0 +1,26 @@
+000018(:protocol-version 2 0)
+000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
+0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
+0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:263} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:264}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:263}_[] ?{_:264}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1)
+0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1)
+0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:741:1--748:1 n[2] m[4]) a[3])))")))))) 1)
+0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 29) (:end 5 31)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 29)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 17) (:end 5 19)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 17)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 41) (:end 5 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 38) (:end 3 39)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 25) (:end 3 27)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 25)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 13) (:end 3 15)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 2 19) (:end 3 6)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+000015(:return (:ok ()) 1)
+Alas the file is done, aborting

tests/ideMode/ideMode001/input

@@ -0,0 +1 @@
+00001e((:load-file "LocType.idr") 1)

tests/ideMode/ideMode001/run

@@ -0,0 +1,3 @@
+$1 --ide-mode < input
+
+rm -rf build

tests/ideMode/ideMode002/.gitignore

@@ -0,0 +1,2 @@
+/expected
+

tests/ideMode/ideMode002/expected.in

@@ -0,0 +1,3 @@
+000018(:protocol-version 2 0)
+__EXPECTED_LINE__
+Alas the file is done, aborting

tests/ideMode/ideMode002/gen_expected.sh

@@ -0,0 +1,15 @@
+#!/usr/bin/env sh
+
+INPUT=`cat`
+
+VERSION=`echo $INPUT | cut -d- -f1`
+TAG=`echo $INPUT | cut -s -d- -f2`
+
+MAJOR=`echo $VERSION | cut -d. -f1`
+MINOR=`echo $VERSION | cut -d. -f2`
+PATCH=`echo $VERSION | cut -d. -f3`
+
+EXPECTED_LINE="(:return (:ok ((${MAJOR} ${MINOR} ${PATCH}) (\"${TAG}\"))) 1)"
+EXPECTED_LENGTH=$(expr ${#EXPECTED_LINE} + 1) # +LF
+
+sed -e "s/__EXPECTED_LINE__/$(printf '%06x' ${EXPECTED_LENGTH})${EXPECTED_LINE}/g" expected.in > expected

tests/ideMode/ideMode002/input

@@ -0,0 +1 @@
+00000c(:version 1)

tests/ideMode/ideMode002/run

@@ -0,0 +1,4 @@
+$1 --version | awk '{print $4}' | ./gen_expected.sh
+$1 --ide-mode < input
+
+rm -rf build

tests/ideMode/ideMode003/LocType.idr

@@ -0,0 +1,7 @@
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+append : Vect n a -> Vect m a -> Vect (n + m) a
+append [] ys = ys
+append (x :: xs) ys = x :: append xs ys