From a6028b0d92e2dff02329ab7f441bf48ccdeb3eb3 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Tue, 9 Jan 2024 16:11:18 +0000 Subject: [PATCH] Add unit tests for nockma evaluator --- src/Juvix/Compiler/Nockma/Evaluator.hs | 7 ++- test/Base.hs | 6 ++- test/Nockma.hs | 3 +- test/Nockma/Eval.hs | 7 +++ test/Nockma/Eval/Positive.hs | 70 ++++++++++++++++++++++++++ test/Nockma/Parse/Positive.hs | 2 +- 6 files changed, 91 insertions(+), 4 deletions(-) create mode 100644 test/Nockma/Eval.hs create mode 100644 test/Nockma/Eval/Positive.hs diff --git a/src/Juvix/Compiler/Nockma/Evaluator.hs b/src/Juvix/Compiler/Nockma/Evaluator.hs index 95f2b2c889..c331beeef9 100644 --- a/src/Juvix/Compiler/Nockma/Evaluator.hs +++ b/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 diff --git a/test/Base.hs b/test/Base.hs index 781b65973f..f7acb02ef3 100644 --- a/test/Base.hs +++ b/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 diff --git a/test/Nockma.hs b/test/Nockma.hs index 36bd03fce4..8b3e3dd737 100644 --- a/test/Nockma.hs +++ b/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] diff --git a/test/Nockma/Eval.hs b/test/Nockma/Eval.hs new file mode 100644 index 0000000000..836c5a6a7f --- /dev/null +++ b/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] diff --git a/test/Nockma/Eval/Positive.hs b/test/Nockma/Eval/Positive.hs new file mode 100644 index 0000000000..8455c10466 --- /dev/null +++ b/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 |]) + ] diff --git a/test/Nockma/Parse/Positive.hs b/test/Nockma/Parse/Positive.hs index d79e0208d5..7a892161b9 100644 --- a/test/Nockma/Parse/Positive.hs +++ b/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