Add first Idris2 tests

idris2.ipkg

@@ -118,7 +118,7 @@ modules =
 sourcedir = src
 executable = idris2
 -- opts = "--cg-opt -O2 --partial-eval"
-opts = "--cg-opt -g --partial-eval --dumpdefuns idris2.dc"
+opts = "--cg-opt -g --partial-eval"
 
 main = Idris.Main
 

src/Core/Context.idr

@@ -65,7 +65,6 @@ getNameRefs gam
     addToMap arr (n, i)
         = coreLift $ writeArray arr i (n, Nothing)
 
-
 initSize : Int
 initSize = 10000
 
@@ -208,7 +207,7 @@ commitCtxt ctxt
                      arr <- get Arr
                      coreLift $ commitStaged (toList (staging ctxt)) arr
                      pure (record { staging = empty,
-                                 branchDepth = Z } ctxt)
+                                    branchDepth = Z } ctxt)
            S k => pure (record { branchDepth = k } ctxt)
   where
     -- We know the array must be big enough, because it will have been resized
@@ -686,10 +685,16 @@ export
 commit : {auto c : Ref Ctxt Defs} ->
          Core ()
 commit
-    = do ctxt <- get Ctxt
-         gam' <- commitCtxt (gamma ctxt)
+    = do defs <- get Ctxt
+         gam' <- commitCtxt (gamma defs)
          setCtxt gam'
 
+export
+depth : {auto c : Ref Ctxt Defs} ->
+        Core Nat
+depth
+    = do defs <- get Ctxt
+         pure (branchDepth (gamma defs))
 
 -- Get the names to save. These are the ones explicitly noted, and the
 -- ones between firstEntry and nextEntry (which are the names introduced in

src/Core/Unify.idr

@@ -126,6 +126,7 @@ convertErrorS s loc env x y
     = if s then convertError loc env y x
            else convertError loc env x y
 
+export
 postpone : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            FC -> String -> Env Term vars -> NF vars -> NF vars -> Core UnifyResult

src/Core/UnifyState.idr

@@ -504,10 +504,14 @@ checkValidHole (idx, (fc, n))
                      case c of
                           MkConstraint fc env x y =>
                              do put UST (record { guesses = empty } ust) 
-                                throw (CantSolveEq fc env x y)
+                                xnf <- normaliseHoles defs env x
+                                ynf <- normaliseHoles defs env y
+                                throw (CantSolveEq fc env xnf ynf)
                           MkSeqConstraint fc env (x :: _) (y :: _) =>
                              do put UST (record { guesses = empty } ust) 
-                                throw (CantSolveEq fc env x y)
+                                xnf <- normaliseHoles defs env x
+                                ynf <- normaliseHoles defs env y
+                                throw (CantSolveEq fc env xnf ynf)
                           _ => pure ()
               _ => traverse_ checkRef (map fst (toList (getRefs (type gdef))))
   where

src/Idris/REPL.idr

@@ -547,7 +547,7 @@ processCatch cmd
                            put UST u'
                            put Syn s'
                            put ROpts o'
-                           coreLift (putStrLn !(perror err))
+                           coreLift (putStrLn !(display err))
                            pure True)
 
 parseRepl : String -> Either ParseError REPLCmd

src/TTImp/Elab/Check.idr

@@ -485,31 +485,34 @@ convert fc elabinfo env x y
                 = case elabMode elabinfo of
                        InLHS _ => InLHS
                        _ => InTerm in
-          catch (do logGlueNF 5 "Unifying" env x
-                    logGlueNF 5 "....with" env y
-                    vs <- if isFromTerm x && isFromTerm y
-                             then do xtm <- getTerm x
-                                     ytm <- getTerm y
-                                     unifyWithLazy umode fc env xtm ytm
-                             else do xnf <- getNF x
-                                     ynf <- getNF y
-                                     unifyWithLazy umode fc env xnf ynf
-                    when (holesSolved vs) $
-                        solveConstraints umode Normal
-                    pure vs)
-                (\err => do defs <- get Ctxt
-                            xtm <- getTerm x
-                            ytm <- getTerm y
-                            -- See if we can improve the error message by
-                            -- resolving any more constraints
-                            catch (solveConstraints umode Normal)
-                                  (\err => pure ())
-                            -- We need to normalise the known holes before
-                            -- throwing because they may no longer be known
-                            -- by the time we look at the error
-                            throw (WhenUnifying fc env 
-                                      !(normaliseHoles defs env xtm)
-                                      !(normaliseHoles defs env ytm) err))
+          catch 
+            (do logGlueNF 5 "Unifying" env x
+                logGlueNF 5 "....with" env y
+                vs <- if isFromTerm x && isFromTerm y
+                         then do xtm <- getTerm x
+                                 ytm <- getTerm y
+                                 unifyWithLazy umode fc env xtm ytm
+                         else do xnf <- getNF x
+                                 ynf <- getNF y
+                                 unifyWithLazy umode fc env xnf ynf
+                when (holesSolved vs) $
+                    solveConstraints umode Normal
+                pure vs)
+            (\err => 
+               do defs <- get Ctxt
+                  xtm <- getTerm x
+                  ytm <- getTerm y
+                  -- See if we can improve the error message by
+                  -- resolving any more constraints
+                  catch (solveConstraints umode Normal)
+                        (\err => pure ())
+                  -- We need to normalise the known holes before
+                  -- throwing because they may no longer be known
+                  -- by the time we look at the error
+                  defs <- get Ctxt
+                  throw (WhenUnifying fc env 
+                            !(normaliseHoles defs env xtm)
+                            !(normaliseHoles defs env ytm) err))
 
 -- Check whether the type we got for the given type matches the expected
 -- type.

tests/Main.idr

@@ -23,7 +23,8 @@ ttimpTests
 
 idrisTests : List String
 idrisTests
-    = ["basic001"]
+    = ["basic001",
+       "import001"]
 
 chdir : String -> IO Bool
 chdir dir 
@@ -54,11 +55,11 @@ runTest dir prog test
 
 main : IO ()
 main
-    = do [_, ttimp] <- getArgs
+    = do [_, idris2] <- getArgs
               | _ => do putStrLn "Usage: runtests [ttimp path]"
-         ttimps <- traverse (runTest "ttimp" ttimp) ttimpTests
---          blods <- traverse (runTest "blodwen" blodwen) blodwenTests
-         if (any not ttimps)
+         ttimps <- traverse (runTest "ttimp" idris2) ttimpTests
+         idrs <- traverse (runTest "idris2" idris2) idrisTests
+         if (any not (ttimps ++ idrs))
             then exitWith (ExitFailure 1)
             else exitWith ExitSuccess
 

tests/idris2/basic001/Vect.idr

@@ -0,0 +1,34 @@
+data Nat = Z | S Nat
+
+plus : Nat -> Nat -> Nat
+plus Z     y = y
+plus (S k) y = S (plus k y)
+
+data Vect : Nat -> Type -> Type where
+     Nil  : Vect Z a
+     Cons : a -> Vect k a -> Vect (S k) a
+
+foldl : (0 b : Nat -> Type) ->
+        ({k : Nat} -> b k -> a -> b (S k)) ->
+        b Z ->
+        Vect n a -> b n
+foldl b g z Nil = z
+foldl b g z (Cons x xs) = foldl (\i => b (S i)) g (g z x) xs
+
+reverse : Vect n a -> Vect n a
+reverse
+    = foldl (\m => Vect m a)
+            (\rev => \x => Cons x rev) Nil
+
+append : Vect n a -> Vect m a -> Vect (plus n m) a
+append Nil ys = ys
+append (Cons x xs) ys = Cons x (append xs ys)
+
+vlength : (n : Nat) -> Vect n a -> Nat
+vlength Z Nil = Z
+vlength n@_ (Cons x xs) = n -- (vlength _ xs);
+
+zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
+zipWith f Nil Nil = Nil
+-- zipWith f (Cons x xs) Nil impossible
+zipWith f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith f xs ys)

tests/idris2/basic001/expected

@@ -0,0 +1,9 @@
+1/1: Building Vect (Vect.idr)
+Welcome to Idris 2 version 0.0. Fingers crossed!
+Main> Main> Cons (S Z) (Cons (S (S Z)) []) : Vect (S (S Z)) Nat
+Main> (interactive):1:22--1:25:When unifying Vect Z ?a and Vect (S Z) ?a
+Mismatch between:
+	Z
+and
+	S Z
+Main> Bye for now!

tests/idris2/basic001/input

@@ -0,0 +1,4 @@
+:set showtypes
+zipWith plus (Cons Z (Cons (S Z) Nil)) (Cons (S Z) (Cons (S Z) Nil))
+zipWith plus (Cons Z Nil) (Cons (S Z) (Cons Z Nil))
+:q

tests/idris2/basic001/run

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

tests/idris2/import001/Mult.idr

@@ -0,0 +1,8 @@
+module Mult
+
+import public Nat
+
+public export
+mult : Nat -> Nat -> Nat
+mult Z y = Z
+mult (S k) y = plus y (mult k y)

tests/idris2/import001/Nat.idr

@@ -0,0 +1,10 @@
+module Nat
+
+public export
+data Nat = Z | S Nat
+
+public export
+plus : Nat -> Nat -> Nat
+plus Z y = y
+plus (S k) y = S (plus k y)
+

tests/idris2/import001/Test.idr

@@ -0,0 +1,7 @@
+module Test
+
+import Mult
+
+thing : Nat -> Nat
+thing x = mult x (plus x x)
+

tests/idris2/import001/expected

@@ -0,0 +1,10 @@
+1/3: Building Nat (Nat.idr)
+2/3: Building Mult (Mult.idr)
+3/3: Building Test (Test.idr)
+Welcome to Idris 2 version 0.0. Fingers crossed!
+Test> S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))
+Test> Bye for now!
+2/3: Building Mult (Mult.idr)
+Welcome to Idris 2 version 0.0. Fingers crossed!
+Test> S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))
+Test> Bye for now!

tests/idris2/import001/input

@@ -0,0 +1,2 @@
+thing (S (S (S Z)))
+:q

tests/idris2/import001/run

@@ -0,0 +1,6 @@
+$1 --no-prelude Test.idr < input
+sleep 1
+touch Mult.idr
+$1 --no-prelude Test.idr < input
+
+rm -rf build