From 7154f874bf6299480db0d1e9526f2f7ee5e27354 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 7 Sep 2024 14:47:41 -0700
Subject: [PATCH] add smoke tests

---
 Makefile                                  |  2 +-
 newt/Fix.newt                             |  9 ++++-----
 newt/data.newt                            | 14 --------------
 newt/ptest1.newt                          | 12 ------------
 scripts/test                              | 11 +++++++++++
 src/Lib/Check.idr                         |  7 +++++++
 src/Main.idr                              | 13 ++++++++-----
 {newt => tests/black}/Zoo1.newt           |  0
 {newt => tests/black}/test1.newt          |  0
 {newt => tests/black}/testcase.newt       |  0
 {newt => tests/black}/testcase2.newt      |  0
 {newt => tests/black}/testcase3.newt      |  0
 {newt => tests/black}/testprim.newt       |  0
 {newt => tests/black}/zoo2eg.newt         |  0
 newt/zoo3.newt => tests/black/zoo3eg.newt |  0
 newt/zoo4.newt => tests/black/zoo4eg.newt |  0
 16 files changed, 31 insertions(+), 37 deletions(-)
 delete mode 100644 newt/data.newt
 delete mode 100644 newt/ptest1.newt
 create mode 100755 scripts/test
 rename {newt => tests/black}/Zoo1.newt (100%)
 rename {newt => tests/black}/test1.newt (100%)
 rename {newt => tests/black}/testcase.newt (100%)
 rename {newt => tests/black}/testcase2.newt (100%)
 rename {newt => tests/black}/testcase3.newt (100%)
 rename {newt => tests/black}/testprim.newt (100%)
 rename {newt => tests/black}/zoo2eg.newt (100%)
 rename newt/zoo3.newt => tests/black/zoo3eg.newt (100%)
 rename newt/zoo4.newt => tests/black/zoo4eg.newt (100%)

diff --git a/Makefile b/Makefile
index b5d1620..66ccf03 100644
--- a/Makefile
+++ b/Makefile
@@ -9,7 +9,7 @@ build/exec/newt.js: ${SRCS}
 	idris2 --cg node -o newt.js -p contrib -c src/Main.idr
 
 test: build/exec/newt
-	build/exec/newt newt/*.newt
+	scripts/test
 
 vscode:
 	cd newt-vscode && vsce package && code --install-extension *.vsix
diff --git a/newt/Fix.newt b/newt/Fix.newt
index 6612c3f..b859c81 100644
--- a/newt/Fix.newt
+++ b/newt/Fix.newt
@@ -17,9 +17,8 @@ data D : (A : Type) -> Type where
 -- We do need to sort this out
 
 unV : { A : U} -> D A -> A
-unV = \ v => case v of
-  V y => y
- --  F f => TRUSTME
+unV (V y) = y
+unV (F f) = ?  -- was TRUSTME
 
 
 
@@ -27,8 +26,8 @@ unV = \ v => case v of
 unF : {A : Type} -> D A -> D A -> D A
 unF = \ {A} v x =>
   case v of
-    F {A} f => ? -- f x
-    V y => TRUSTME
+    F f => f x
+    V y => ? -- was TRUSTME
 
 -- fix : {A : U} -> (A -> A) -> A
 -- fix = \ {A} g =>
diff --git a/newt/data.newt b/newt/data.newt
deleted file mode 100644
index 8cd2802..0000000
--- a/newt/data.newt
+++ /dev/null
@@ -1,14 +0,0 @@
-module Data
-
--- The code to handle this is full of TODO
--- stuff is not checked and it's not read as data, just
--- type signatures.
-
-data Nat : U where
-  Z : Nat
-  S : Nat -> Nat
-
--- My initial version of this needed unbound implicits
-data Maybe : U -> U where
-  Nothing : {a : U} -> Maybe a
-  Just : {a : U} -> a -> Maybe a
diff --git a/newt/ptest1.newt b/newt/ptest1.newt
deleted file mode 100644
index 8d50d67..0000000
--- a/newt/ptest1.newt
+++ /dev/null
@@ -1,12 +0,0 @@
-module Bug
-
-Nat : U
-Nat = (N : U) -> (N -> N) -> N -> N
-
-zero : Nat
-zero = \ U s z => z
-
--- This fails unification if we allow U on the LHS, because U is special on the RHS.
--- We need to not parse it on the LHS if we're not pattern matching.
-succ : Nat -> Nat
-succ = \ n U s z => s (n U s z)
diff --git a/scripts/test b/scripts/test
new file mode 100755
index 0000000..e3e226d
--- /dev/null
+++ b/scripts/test
@@ -0,0 +1,11 @@
+#!/bin/sh
+
+for i in tests/black/*.newt; do
+  ./build/exec/newt $i
+  if [ $? != "0" ]; then
+    echo FAIL $i
+    exit -1
+  fi
+  echo $?
+done
+
diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index 529ddca..e55007c 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -168,6 +168,13 @@ parameters (ctx: Context)
         case lookup k' !(get) of
           Just (MkEntry name ty (Fn tm)) => unify l t !(vappSpine !(eval [] CBN tm) sp')
           _ => error ctx.fc "unify failed \{show t'} =?= \{show u'} [no Fn]\n  env is \{show ctx.env} \{show $ map fst ctx.types}"
+
+      (VRef fc k def sp, u) => do
+        debug "expand %ref \{k} =?= \{show u}"
+        case lookup k !(get) of
+          Just (MkEntry name ty (Fn tm)) => unify l !(vappSpine !(eval [] CBN tm) sp) u
+          _ => error ctx.fc "unify failed \{show t'} [no Fn] =?= \{show u'}\n  env is \{show ctx.env} \{show $ map fst ctx.types}"
+
       -- REVIEW I'd like to quote this back, but we have l that aren't in the environment.
       _ => error ctx.fc "unify failed \{show t'} =?= \{show u'} \n  env is \{show ctx.env} \{show $ map fst ctx.types}"
     where
diff --git a/src/Main.idr b/src/Main.idr
index 43c2f01..cc09a19 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -24,6 +24,9 @@ import System
 import System.Directory
 import System.File
 
+fail : String -> M ()
+fail msg = putStrLn msg >> exitFailure
+
 dumpContext : TopContext -> M ()
 dumpContext top = do
     putStrLn "Context:"
@@ -46,11 +49,11 @@ processFile fn = do
     | Left err => printLn err
   let toks = tokenise src
   let Right res = parse parseMod toks
-    | Left y => putStrLn (showError src y)
+    | Left y => fail (showError src y)
   putStrLn $ render 80 $ pretty res
   printLn "process Decls"
   Right _ <- tryError $ traverse_ processDecl (collectDecl res.decls)
-    | Left y => putStrLn (showError src y)
+    | Left y => fail (showError src y)
 
   dumpContext !get
   dumpSource
@@ -61,8 +64,6 @@ main' = do
   putStrLn "Args: \{show args}"
   let (_ :: files) = args
     | _ => putStrLn "Usage: newt foo.newt"
-  -- Right files <- listDir "eg"
-  --   | Left err => printLn err
   when ("-v" `elem` files) $ modify { verbose := True }
   traverse_ processFile (filter (".newt" `isSuffixOf`) files)
 
@@ -71,5 +72,7 @@ main = do
   -- we'll need to reset for each file, etc.
   ctx <- empty
   Right _  <- runEitherT $ runStateT ctx $ main'
-    | Left (E (c, r) str) => putStrLn "ERROR at (\{show c}, \{show r}): \{show str}"
+    | Left (E (c, r) str) => do
+        putStrLn "ERROR at (\{show c}, \{show r}): \{show str}"
+        exitFailure
   putStrLn "done"
diff --git a/newt/Zoo1.newt b/tests/black/Zoo1.newt
similarity index 100%
rename from newt/Zoo1.newt
rename to tests/black/Zoo1.newt
diff --git a/newt/test1.newt b/tests/black/test1.newt
similarity index 100%
rename from newt/test1.newt
rename to tests/black/test1.newt
diff --git a/newt/testcase.newt b/tests/black/testcase.newt
similarity index 100%
rename from newt/testcase.newt
rename to tests/black/testcase.newt
diff --git a/newt/testcase2.newt b/tests/black/testcase2.newt
similarity index 100%
rename from newt/testcase2.newt
rename to tests/black/testcase2.newt
diff --git a/newt/testcase3.newt b/tests/black/testcase3.newt
similarity index 100%
rename from newt/testcase3.newt
rename to tests/black/testcase3.newt
diff --git a/newt/testprim.newt b/tests/black/testprim.newt
similarity index 100%
rename from newt/testprim.newt
rename to tests/black/testprim.newt
diff --git a/newt/zoo2eg.newt b/tests/black/zoo2eg.newt
similarity index 100%
rename from newt/zoo2eg.newt
rename to tests/black/zoo2eg.newt
diff --git a/newt/zoo3.newt b/tests/black/zoo3eg.newt
similarity index 100%
rename from newt/zoo3.newt
rename to tests/black/zoo3eg.newt
diff --git a/newt/zoo4.newt b/tests/black/zoo4eg.newt
similarity index 100%
rename from newt/zoo4.newt
rename to tests/black/zoo4eg.newt