basic test for --ide-mode

how to take care of input termination properly? currently we add the
message 'Alas the file is done' in the expected outcome but that's
ugly

src/Idris/IDEMode/REPL.idr

@@ -15,6 +15,8 @@ import Core.Options
 import Core.TT
 import Core.Unify
 
+import Data.Primitives.Views
+
 import Idris.Desugar
 import Idris.Error
 import Idris.ModTree
@@ -123,6 +125,33 @@ toHex _ [] = Just 0
 toHex m (d :: ds)
     = pure $ !(hex (toLower d)) * m + !(toHex (m*16) ds)
 
+hexDigit : Int -> Char
+hexDigit 0 = '0'
+hexDigit 1 = '1'
+hexDigit 2 = '2'
+hexDigit 3 = '3'
+hexDigit 4 = '4'
+hexDigit 5 = '5'
+hexDigit 6 = '6'
+hexDigit 7 = '7'
+hexDigit 8 = '8'
+hexDigit 9 = '9'
+hexDigit 10 = 'a'
+hexDigit 11 = 'b'
+hexDigit 12 = 'c'
+hexDigit 13 = 'd'
+hexDigit 14 = 'e'
+hexDigit 15 = 'f'
+
+||| Convert a positive integer into a list of (lower case) hexadecimal characters
+asHex : Int -> String
+asHex n = pack $ asHex' n []
+  where
+    asHex' : Int -> List Char -> List Char
+    asHex' 0 hex = hex
+    asHex' n hex with (n `divides` 16)
+      asHex' (16 * div + rem) hex | DivBy {div} {rem} _ = asHex' div (hexDigit rem :: hex)
+
 -- Read 6 characters. If they're a hex number, read that many characters.
 -- Otherwise, just read to newline
 getInput : File -> IO String

tests/Main.idr

@@ -5,7 +5,7 @@ import System
 %default covering
 
 ttimpTests : List String
-ttimpTests 
+ttimpTests
     = ["basic001", "basic002", "basic003", "basic004", "basic005",
        "basic006",
        "coverage001", "coverage002",
@@ -53,16 +53,20 @@ typeddTests
 
 chezTests : List String
 chezTests
-   = ["chez001", "chez002", "chez003", "chez004", 
+   = ["chez001", "chez002", "chez003", "chez004",
       "chez005", "chez006", "chez007"]
 
+ideModeTests : List String
+ideModeTests
+  =  [ "ideMode001" ]
+
 chdir : String -> IO Bool
-chdir dir 
+chdir dir
     = do ok <- foreign FFI_C "chdir" (String -> IO Int) dir
          pure (ok == 0)
 
 fail : String -> IO ()
-fail err 
+fail err
     = do putStrLn err
          exitWith (ExitFailure 1)
 
@@ -79,7 +83,7 @@ runTest dir prog test
                                 pure False
          if (out == exp)
             then putStrLn "success"
-            else putStrLn "FAILURE"
+            else putStrLn $ "FAILURE: found " ++ out
          chdir "../.."
          pure (out == exp)
 
@@ -109,16 +113,16 @@ main
          ttimps <- traverse (runTest "ttimp" idris2) ttimpTests
          idrs <- traverse (runTest "idris2" idris2) idrisTests
          typedds <- traverse (runTest "typedd-book" idris2) typeddTests
+         ideModes <- traverse (runTest "ideMode" idris2) ideModeTests
          chexec <- findChez
          chezs <- maybe (do putStrLn "Chez Scheme not found"
                             pure [])
                         (\c => do putStrLn $ "Found Chez Scheme at " ++ c
                                   traverse (runTest "chez" idris2) chezTests)
                         chexec
-         let res = ttimps ++ typedds ++ idrs ++ chezs
-         putStrLn (show (length (filter id res)) ++ "/" ++ show (length res) 
+         let res = ttimps ++ typedds ++ idrs ++ ideModes ++ chezs
+         putStrLn (show (length (filter id res)) ++ "/" ++ show (length res)
                        ++ " tests successful")
          if (any not res)
             then exitWith (ExitFailure 1)
             else exitWith ExitSuccess
-

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,4 @@
+000018(:protocol-version 2 0)
+000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
+00002a(:return (:ok "Loaded LocType.idr" ()) 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