chore(primer): add tests for evaluating top-level definitions

Signed-off-by: Drew Hess <src@drewhess.com>
hackworthltd · Apr 20, 2024 · ebbaad5 · ebbaad5
1 parent 7761f26
commit ebbaad5
Show file tree

Hide file tree

Showing 3 changed files with 101 additions and 0 deletions.
diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
@@ -35,6 +35,8 @@ module Primer.App (
   newEmptyProg',
   newProg,
   newProg',
+  allDefs,
+  allTypes,
   progAllModules,
   progAllDefs,
   progAllTypeDefs,

diff --git a/primer/test/Tests/EvalFullInterp.hs b/primer/test/Tests/EvalFullInterp.hs
@@ -19,6 +19,8 @@ import Primer.App (
   EvalBoundedInterpResp (..),
   EvalInterpReq (..),
   EvalInterpResp (..),
+  allDefs,
+  allTypes,
   handleEvalBoundedInterpRequest,
   handleEvalInterpRequest,
   importModules,
@@ -50,6 +52,10 @@ import Primer.Def (DefMap)
 import Primer.Eval
 import Primer.EvalFullInterp (InterpError (..), Timeout (MicroSec), interp, mkGlobalEnv)
 import Primer.EvalFullStep (evalFullStepCount)
+import Primer.Examples (
+  even3App,
+  even3Prog,
+ )
 import Primer.Gen.Core.Typed (forAllT, propertyWT)
 import Primer.Module (
   Module (..),
@@ -92,6 +98,7 @@ import Primer.Test.Eval qualified as EvalTest
 import Primer.Test.Expected qualified as Expected
 import Primer.Test.Util (
   failWhenSevereLogs,
+  gvn,
   primDefs,
  )
 import Primer.TypeDef (
@@ -895,6 +902,17 @@ unit_prim_partial_map =
         s <- evalFullTest builtinTypes (gs <> prims) Syn e
         s @?= Right r
 
+unit_interp_even3 :: Assertion
+unit_interp_even3 =
+  let (prog, _, _) = even3Prog
+      types = allTypes prog
+      defs = allDefs prog
+      expr = create1 $ gvar $ gvn ["Even3"] "even 3?"
+      expect = create1 $ con0 cFalse
+   in do
+        s <- evalFullTest types defs Chk expr
+        s @?= Right expect
+
 -- Test that 'handleEvalInterpRequest' will reduce imported terms
 unit_eval_interp_full_modules :: Assertion
 unit_eval_interp_full_modules =
@@ -942,6 +960,24 @@ unit_eval_interp_full_modules_bounded =
         Left err -> assertFailure $ show err
         Right assertion -> assertion
 
+-- Test that handleEvalFullRequest will reduce top-level definitions.
+unit_handleEvalInterpRequest_even3 :: Assertion
+unit_handleEvalInterpRequest_even3 =
+  let test = do
+        expr <- gvar $ gvn ["Even3"] "even 3?"
+        (EvalInterpRespNormal e) <-
+          readerToState
+            $ handleEvalInterpRequest
+            $ EvalInterpReq
+              { expr = expr
+              , dir = Chk
+              }
+        expect <- con0 cFalse
+        pure $ e ~= expect
+   in runAppTestM even3App test <&> fst >>= \case
+        Left err -> assertFailure $ show err
+        Right assertion -> assertion
+
 -- Test that 'handleEvalInterpRequest' will reduce case analysis of
 -- imported types
 unit_eval_interp_full_modules_scrutinize_imported_type :: Assertion
@@ -1013,6 +1049,27 @@ unit_eval_interp_full_modules_scrutinize_imported_type_bounded =
           , moduleDefs = mempty
           }
 
+-- Test that handleEvalBoundedInterpRequest will reduce top-level definitions.
+unit_handleEvalBoundedInterpRequest_even3 :: Assertion
+unit_handleEvalBoundedInterpRequest_even3 =
+  let test = do
+        expr <- gvar $ gvn ["Even3"] "even 3?"
+        resp <-
+          readerToState
+            $ handleEvalBoundedInterpRequest
+            $ EvalBoundedInterpReq
+              { expr = expr
+              , dir = Chk
+              , timeout = MicroSec 10_000
+              }
+        expect <- con0 cFalse
+        pure $ case resp of
+          EvalBoundedInterpRespFailed err -> assertFailure $ show err
+          EvalBoundedInterpRespNormal e -> e ~= expect
+   in runAppTestM even3App test <&> fst >>= \case
+        Left err -> assertFailure $ show err
+        Right assertion -> assertion
+
 -- Test that 'handleEvalBoundedInterpRequest' will return timeouts.
 unit_eval_interp_handle_eval_bounded_timeout :: Assertion
 unit_eval_interp_handle_eval_bounded_timeout =

diff --git a/primer/test/Tests/EvalFullStep.hs b/primer/test/Tests/EvalFullStep.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE ViewPatterns #-}
+
 module Tests.EvalFullStep where
 
 import Foreword hiding (unlines)
@@ -16,6 +18,8 @@ import Optics
 import Primer.App (
   EvalFullReq (EvalFullReq, evalFullCxtDir, evalFullMaxSteps, evalFullOptions, evalFullReqExpr),
   EvalFullResp (EvalFullRespNormal, EvalFullRespTimedOut),
+  allDefs,
+  allTypes,
   handleEvalFullRequest,
   importModules,
   newEmptyApp,
@@ -46,6 +50,10 @@ import Primer.Core.Utils (
 import Primer.Def (DefMap)
 import Primer.Eval
 import Primer.EvalFullStep
+import Primer.Examples (
+  even3App,
+  even3Prog,
+ )
 import Primer.Gen.Core.Typed (WT, forAllT, genChk, isolateWT, propertyWT)
 import Primer.Log (runPureLogT)
 import Primer.Module (
@@ -96,6 +104,7 @@ import Primer.Test.TestM (
 import Primer.Test.Util (
   assertNoSevereLogs,
   failWhenSevereLogs,
+  gvn,
   primDefs,
   testNoSevereLogs,
   zeroIDs,
@@ -1681,6 +1690,17 @@ unit_prim_partial_map =
         s <- evalFullTestExactSteps maxID builtinTypes (gs <> prims) 91 Syn e
         s ~== r
 
+unit_evalFull_even3 :: Assertion
+unit_evalFull_even3 =
+  let (prog, maxID, _) = even3Prog
+      types = allTypes prog
+      defs = allDefs prog
+      (expr, _) = create $ gvar $ gvn ["Even3"] "even 3?"
+      (expect, _) = create $ con0 cFalse
+   in do
+        s <- evalFullTest maxID types defs 100 Chk expr
+        s <~==> Right expect
+
 -- Test that handleEvalFullRequest will reduce imported terms
 unit_eval_full_modules :: Assertion
 unit_eval_full_modules =
@@ -1744,6 +1764,28 @@ unit_eval_full_modules_scrutinize_imported_type =
           , moduleDefs = mempty
           }
 
+-- Test that handleEvalFullRequest will reduce top-level definitions.
+unit_eval_full_even3 :: Assertion
+unit_eval_full_even3 =
+  let test = do
+        expr <- gvar $ gvn ["Even3"] "even 3?"
+        resp <-
+          readerToState
+            $ handleEvalFullRequest
+            $ EvalFullReq
+              { evalFullReqExpr = expr
+              , evalFullCxtDir = Chk
+              , evalFullMaxSteps = 200
+              , evalFullOptions = UnderBinders
+              }
+        expect <- con0 cFalse
+        pure $ case resp of
+          EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out"
+          EvalFullRespNormal e -> e ~= expect
+   in runAppTestM even3App test <&> fst >>= \case
+        Left err -> assertFailure $ show err
+        Right assertion -> assertion
+
 -- Test that evaluation does not duplicate node IDs
 tasty_unique_ids :: Property
 tasty_unique_ids = withTests 1000