Add unit tests for nockma evaluator

src/Juvix/Compiler/Nockma/Evaluator.hs

@@ -103,7 +103,12 @@ evalRepl mprog defaultStack expr = do
     namedTerms :: HashMap Text (Term a)
     namedTerms = programAssignments mprog
 
-eval :: forall r a. (Members '[Error NockEvalError, Error (ErrNockNatural a)] r, NockNatural a) => Term a -> Term a -> Sem r (Term a)
+eval ::
+  forall r a.
+  (Members '[Error NockEvalError, Error (ErrNockNatural a)] r, NockNatural a) =>
+  Term a ->
+  Term a ->
+  Sem r (Term a)
 eval stack = \case
   TermAtom {} -> throw ExpectedCell
   TermCell c -> do

test/Base.hs

@@ -22,7 +22,8 @@ import Juvix.Extra.Paths hiding (rootBuildDir)
 import Juvix.Prelude hiding (assert)
 import Juvix.Prelude.Env
 import Test.Tasty
-import Test.Tasty.HUnit
+import Test.Tasty.HUnit hiding (assertFailure)
+import Test.Tasty.HUnit qualified as HUnit
 
 data AssertionDescr
   = Single Assertion
@@ -111,3 +112,6 @@ testRunIOEitherTermination ::
 testRunIOEitherTermination entry =
   testRunIOEither entry
     . evalTermination iniTerminationState
+
+assertFailure :: (MonadIO m) => String -> m a
+assertFailure = liftIO . HUnit.assertFailure

test/Nockma.hs

@@ -1,7 +1,8 @@
 module Nockma where
 
 import Base
+import Nockma.Eval qualified as Eval
 import Nockma.Parse qualified as Parse
 
 allTests :: TestTree
-allTests = testGroup "Nockma tests" [Parse.allTests]
+allTests = testGroup "Nockma tests" [Parse.allTests, Eval.allTests]

test/Nockma/Eval.hs

@@ -0,0 +1,7 @@
+module Nockma.Eval where
+
+import Base
+import Nockma.Eval.Positive qualified as P
+
+allTests :: TestTree
+allTests = testGroup "Nockma eval" [P.allTests]

test/Nockma/Eval/Positive.hs

@@ -0,0 +1,70 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module Nockma.Eval.Positive where
+
+import Base hiding (Path)
+import Juvix.Compiler.Nockma.Evaluator
+import Juvix.Compiler.Nockma.Language
+import Juvix.Compiler.Nockma.Pretty
+import Juvix.Compiler.Nockma.Translation.FromSource.QQ
+
+type Check = Sem '[Reader (Term Natural), Embed IO]
+
+data Test = Test
+  { _testName :: Text,
+    _testProgramSubject :: Term Natural,
+    _testProgramFormula :: Term Natural,
+    _testCheck :: Check ()
+  }
+
+makeLenses ''Test
+
+allTests :: TestTree
+allTests = testGroup "Nockma eval unit positive" (map mk tests)
+  where
+    mk :: Test -> TestTree
+    mk Test {..} = testCase (unpack _testName) $ do
+      let evalResult =
+            run
+              . runError @(ErrNockNatural Natural)
+              . runError @NockEvalError
+              $ eval _testProgramSubject _testProgramFormula
+      case evalResult of
+        Left natErr -> assertFailure ("Evaluation error: " <> show natErr)
+        Right r -> case r of
+          Left evalErr -> assertFailure ("Evaluation error: " <> show evalErr)
+          Right res -> runM (runReader res _testCheck)
+
+eqNock :: Term Natural -> Check ()
+eqNock expected = do
+  actual <- ask
+  unless (expected == actual) (err actual)
+  where
+    err :: Term Natural -> Check ()
+    err actual = do
+      let msg =
+            "Expected:\n"
+              <> ppTrace expected
+              <> "\nBut got:\n"
+              <> ppTrace actual
+      assertFailure (unpack msg)
+
+tests :: [Test]
+tests =
+  [ Test "address" [nock| [0 1] |] [nock| [[@ R] [@ L]] |] (eqNock [nock| [1 0] |]),
+    Test "address nested" [nock| [0 1 2 3 4 5] |] [nock| [@ RRRRR] |] (eqNock [nock| 5 |]),
+    Test "quote" [nock| [0 1] |] [nock| [quote [1 0]] |] (eqNock [nock| [1 0] |]),
+    Test "apply" [nock| [0 1] |] [nock| [apply [@ S] [quote [@ R]]] |] (eqNock [nock| 1 |]),
+    Test "isCell atom" [nock| [0 1] |] [nock| [isCell 11] |] (eqNock [nock| false |]),
+    Test "isCell cell" [nock| [0 1] |] [nock| [isCell [1 0]] |] (eqNock [nock| true |]),
+    Test "suc" [nock| [0 1] |] [nock| [suc [quote 1]] |] (eqNock [nock| 2 |]),
+    Test "eq" [nock| [0 1] |] [nock| [= [1 0] [1 0]] |] (eqNock [nock| true |]),
+    Test "eq" [nock| [0 1] |] [nock| [= [1 0] [0 1]] |] (eqNock [nock| false |]),
+    Test "if" [nock| [0 1] |] [nock| [if [quote true] [@ L] [@ R]] |] (eqNock [nock| 0 |]),
+    Test "if" [nock| [0 1] |] [nock| [if [quote false] [@ L] [@ R]] |] (eqNock [nock| 1 |]),
+    Test "seq" [nock| [0 1] |] [nock| [seq [[suc [@ L]] [@ R]] [suc [@ L]]] |] (eqNock [nock| 2 |]),
+    Test "push" [nock| [0 1] |] [nock| [push [[suc [@ L]] [@ S]]] |] (eqNock [nock| [1 0 1] |]),
+    Test "call" [nock| [quote 1] |] [nock| [call [S [@ S]]] |] (eqNock [nock| 1 |]),
+    Test "replace" [nock| [0 1] |] [nock| [replace [[L [quote 1]] [@ S]]] |] (eqNock [nock| [1 1] |]),
+    Test "hint" [nock| [0 1] |] [nock| [hint [@ LLLL] [quote 1]] |] (eqNock [nock| 1 |])
+  ]

test/Nockma/Parse/Positive.hs

@@ -2,7 +2,7 @@ module Nockma.Parse.Positive where
 
 import Base
 import Data.ByteString qualified as BS
-import Juvix.Compiler.Nockma.Language
+import Juvix.Compiler.Nockma.Language hiding (Path)
 import Juvix.Compiler.Nockma.Pretty (ppPrint)
 import Juvix.Compiler.Nockma.Translation.FromSource (parseText)
 import Juvix.Parser.Error