From 5ba0690216b936d40a6090add638818c9754551a Mon Sep 17 00:00:00 2001 From: Drew Hess Date: Mon, 15 Apr 2024 18:07:20 +0100 Subject: [PATCH 1/6] feat(primer): add app-level handlers for eval via interpretation This commit only adds these handlers at the `Primer.App` module level. Hooking the interpreter up to the API and HTTP service will come in subsequent commits. Note that we add two handlers, one for time-bounded requests, and one for unbounded requests. We will not expose the unbounded handler via the HTTP API, since that would not be safe, but for local Haskell programs, it might be useful to run the unbounded interpreter and handle exceptions, timeouts, etc. in an application-specific manner, which the time-bounded interpreter doesn't really make possible. The time-bounded handler needs an additional `MonadIO` constraint because the variant of the interpreter that it uses handles timeouts and other imprecise exceptions that may be thrown by the interpreter. This is unlike any other actions in `Primer.App`, but it's unavoidable due to our particular lazy implementation of the interpreter. (See the comments in the interpreter source for details.) Signed-off-by: Drew Hess --- primer/src/Primer/App.hs | 113 ++++++++ primer/src/Primer/EvalFullInterp.hs | 11 +- primer/test/Tests/EvalFullInterp.hs | 399 ++++++++++++++++++++++------ primer/test/Tests/Undo.hs | 94 +++++++ primer/testlib/Primer/Test/App.hs | 43 +-- primer/testlib/Primer/Test/Eval.hs | 13 + 6 files changed, 581 insertions(+), 92 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 91149bd58..c76e08c93 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -54,12 +54,18 @@ module Primer.App ( handleEditRequest, handleEvalRequest, handleEvalFullRequest, + handleEvalInterpRequest, + handleEvalBoundedInterpRequest, importModules, MutationRequest (..), EvalReq (..), EvalResp (..), EvalFullReq (..), EvalFullResp (..), + EvalInterpReq (..), + EvalInterpResp (..), + EvalBoundedInterpReq (..), + EvalBoundedInterpResp (..), lookupASTDef, liftError, ) where @@ -181,7 +187,9 @@ import Primer.Core.DSL (S, create, emptyHole, tEmptyHole) import Primer.Core.DSL qualified as DSL import Primer.Core.Transform (renameTyVar, renameVar, unfoldTApp) import Primer.Core.Utils ( + forgetMetadata, freeVars, + generateIDs, generateKindIDs, generateTypeIDs, regenerateExprIDs, @@ -202,6 +210,13 @@ import Primer.Eval (AvoidShadowing (AvoidShadowing)) import Primer.Eval qualified as Eval import Primer.Eval.Detail (EvalDetail) import Primer.Eval.Redex (EvalLog, RunRedexOptions (RunRedexOptions, pushAndElide), ViewRedexOptions (ViewRedexOptions, groupedLets)) +import Primer.EvalFullInterp ( + InterpError, + Timeout, + interp, + interp', + mkGlobalEnv, + ) import Primer.EvalFullStep (Dir (Syn), EvalFullError (TimedOut), TerminationBound, evalFull) import Primer.JSON import Primer.Log (ConvertLogMessage) @@ -525,6 +540,53 @@ data EvalFullResp deriving stock (Eq, Show, Read, Generic) deriving (FromJSON, ToJSON) via PrimerJSON EvalFullResp +-- | A request to evaluate an expression to its normal form using the +-- interpreter. +-- +-- Caution: depending on the expression being evaluated, the +-- evaluation may not terminate, and/or may grow in unbounded size. +data EvalInterpReq = EvalInterpReq + { expr :: Expr + -- ^ The expression to evaluate. + , dir :: Dir + -- ^ Indicates whether 'expr' is in a 'Syn' or 'Chk' context, so we + -- can tell if is an embedding. + } + deriving stock (Eq, Show, Read, Generic) + deriving (FromJSON, ToJSON) via PrimerJSON EvalInterpReq + +-- | A response to a 'EvalBoundedInterpReq'. +newtype EvalInterpResp + = -- | The evaluation succeeded, and the 'Expr' is the result. + EvalInterpRespNormal Expr + deriving stock (Eq, Show, Read, Generic) + deriving (FromJSON, ToJSON) via PrimerJSON EvalInterpResp + +-- | A request to evaluate an expression to its normal form using the +-- interpreter, but bounded in time. +data EvalBoundedInterpReq = EvalBoundedInterpReq + { expr :: Expr + -- ^ The expression to evaluate. + , dir :: Dir + -- ^ Indicates whether 'expr' is in a 'Syn' or 'Chk' context, so we + -- can tell if is an embedding. + , timeout :: Timeout + -- ^ An evaluation timeout, in microseconds. If the timeout is + -- exceeded, the evaluation will be halted, and no expression will + -- be returned; the interpreter's results are all-or-nothing. + } + deriving stock (Eq, Show, Read, Generic) + deriving (FromJSON, ToJSON) via PrimerJSON EvalBoundedInterpReq + +-- | A response to a 'EvalBoundedInterpReq'. +data EvalBoundedInterpResp + = -- | An 'InterpError' exception occurred during evaluation. + EvalBoundedInterpRespFailed InterpError + | -- | The evaluation succeeded, and the 'Expr' is the result. + EvalBoundedInterpRespNormal Expr + deriving stock (Eq, Show, Read, Generic) + deriving (FromJSON, ToJSON) via PrimerJSON EvalBoundedInterpResp + -- * Request handlers -- | Handle a question @@ -633,6 +695,57 @@ handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxS Left (TimedOut e) -> EvalFullRespTimedOut e Right nf -> EvalFullRespNormal nf +-- | Handle an 'EvalInterpReq'. +-- +-- Caution: depending on the expression being evaluated, the +-- evaluation may not terminate, and/or may grow in unbounded size. If +-- your application is not prepared to handle this situation, you may +-- want to use 'handleEvalBoundedInterpRequest', instead. +-- +-- N.B.: this action may 'Control.Exception.throw' an imprecise +-- exception of type 'InterpError' in the event that the expression to +-- be evaluated is not well typed. In normal use, however, this +-- condition should not arise. See 'Primer.EvalFullInterp.interp'', +-- which this action uses, for details. (Note that the +-- 'InterpError.Timeout' exception value will never be thrown, as +-- explained above.) +handleEvalInterpRequest :: + (MonadQueryApp m e) => + EvalInterpReq -> + m EvalInterpResp +handleEvalInterpRequest (EvalInterpReq{expr, dir}) = do + app <- ask + let prog = appProg app + let env = mkGlobalEnv (allDefs prog) + result <- runFreshM app $ generateIDs $ interp' (allTypes prog) env dir (forgetMetadata expr) + pure $ EvalInterpRespNormal result + +-- | Handle an 'EvalBoundedInterpReq'. +-- +-- Unlike 'handleEvalInterpRequest', this action will terminate the +-- evaluation request if it exceeds the given timeout, in which case +-- no partial evaluation result is returned, only a +-- 'InterpError.Timeout' error value. Also unlike +-- 'handleEvalInterpRequest', if an exception occurs during evaluation +-- due to an ill typed term, the exception will be caught and reported +-- via an appropriate 'InterpError' value. +-- +-- Unlike other actions in this module, this action must be run within +-- a 'MonadIO' context, because the exceptions it catches during +-- interpretation can only be caught in the 'IO' monad. +handleEvalBoundedInterpRequest :: + (MonadIO m, MonadQueryApp m e) => + EvalBoundedInterpReq -> + m EvalBoundedInterpResp +handleEvalBoundedInterpRequest (EvalBoundedInterpReq{expr, dir, timeout}) = do + app <- ask + let prog = appProg app + let env = mkGlobalEnv (allDefs prog) + result <- liftIO $ interp timeout (allTypes prog) env dir (forgetMetadata expr) + case result of + Left x -> pure $ EvalBoundedInterpRespFailed x + Right e' -> runFreshM app $ generateIDs e' <&> EvalBoundedInterpRespNormal + -- | Handle a 'ProgAction' applyProgAction :: forall m. MonadEdit m ProgError => Prog -> ProgAction -> m Prog applyProgAction prog = \case diff --git a/primer/src/Primer/EvalFullInterp.hs b/primer/src/Primer/EvalFullInterp.hs index cefaf08ab..d88fcc97a 100644 --- a/primer/src/Primer/EvalFullInterp.hs +++ b/primer/src/Primer/EvalFullInterp.hs @@ -51,6 +51,12 @@ import Primer.Def (ASTDef (ASTDef), Def (DefAST, DefPrim), DefMap) import Primer.Eval.Redex ( Dir (Chk, Syn), ) +import Primer.JSON ( + CustomJSON (..), + FromJSON, + PrimerJSON, + ToJSON, + ) import Primer.Name (Name) import Primer.Primitives (primConName, primFunDef) import Primer.Primitives.PrimDef (PrimDef) @@ -113,10 +119,13 @@ data InterpError | NoBranch (Either ValConName PrimCon) [Pattern] | UnknownTyCon TyConName | UnknownValCon TyConName ValConName - deriving stock (Eq, Show) + deriving stock (Eq, Show, Read, Generic) deriving anyclass (Exception) + deriving (FromJSON, ToJSON) via PrimerJSON InterpError newtype Timeout = MicroSec Int + deriving stock (Eq, Show, Read, Generic) + deriving (FromJSON, ToJSON) via PrimerJSON Timeout -- | Wrap the interpreter in a IO-based timeout, and catch 'InterpError' exceptions interp :: diff --git a/primer/test/Tests/EvalFullInterp.hs b/primer/test/Tests/EvalFullInterp.hs index 571860ff9..ab5bdcd9c 100644 --- a/primer/test/Tests/EvalFullInterp.hs +++ b/primer/test/Tests/EvalFullInterp.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE ViewPatterns #-} -- TODO: DRY with EvalFullStep tests @@ -13,7 +14,18 @@ import Hedgehog hiding (Property, Var, check, property, test, withDiscards, with import Hedgehog.Gen qualified as Gen import Hedgehog.Internal.Property (LabelName (LabelName)) import Hedgehog.Range qualified as Range +import Primer.App ( + EvalBoundedInterpReq (..), + EvalBoundedInterpResp (..), + EvalInterpReq (..), + EvalInterpResp (..), + handleEvalBoundedInterpRequest, + handleEvalInterpRequest, + importModules, + newEmptyApp, + ) import Primer.Builtins ( + boolDef, cCons, cFalse, cJust, @@ -40,8 +52,11 @@ import Primer.EvalFullInterp (InterpError (..), Timeout (MicroSec), interp, mkGl import Primer.EvalFullStep (evalFullStepCount) import Primer.Gen.Core.Typed (forAllT, propertyWT) import Primer.Module ( + Module (..), + builtinModule, builtinTypes, moduleDefsQualified, + primitiveModule, ) import Primer.Primitives ( PrimDef ( @@ -70,16 +85,20 @@ import Primer.Primitives ( tInt, ) import Primer.Primitives.DSL (pfun) -import Primer.Test.Eval qualified as EvalTest -import Primer.Test.Expected ( - Expected (defMap, expectedResult, expr), - mapEven, +import Primer.Test.App ( + runAppTestM, ) +import Primer.Test.Eval qualified as EvalTest +import Primer.Test.Expected qualified as Expected import Primer.Test.Util ( failWhenSevereLogs, primDefs, ) -import Primer.TypeDef (TypeDefMap) +import Primer.TypeDef ( + TypeDef (TypeDefAST), + TypeDefMap, + generateTypeDefIDs, + ) import Primer.Typecheck ( typeDefs, ) @@ -89,17 +108,34 @@ import Tasty ( withDiscards, withTests, ) -import Test.Tasty.HUnit (Assertion, (@?=)) -import Tests.Eval.Utils (genDirTm, hasTypeLets, testModules) +import Test.Tasty.HUnit ( + Assertion, + assertFailure, + (@?=), + ) +import Tests.Action.Prog (readerToState) +import Tests.Eval.Utils ( + genDirTm, + hasTypeLets, + testModules, + (~=), + ) import Tests.Gen.Core.Typed (checkTest) unit_throw_no_branch :: Assertion unit_throw_no_branch = - let e = create1 $ case_ (con0 cTrue `ann` tcon tBool) [branch cFalse [] emptyHole] + let e = create1 EvalTest.illTypedMissingBranch in do s <- evalFullTest builtinTypes mempty Chk e s @?= Left (NoBranch (Left cTrue) [PatCon cFalse]) +unit_throw_no_branch_prim :: Assertion +unit_throw_no_branch_prim = + let e = create1 EvalTest.illTypedMissingBranchPrim + in do + s <- evalFullTest builtinTypes mempty Chk e + s @?= Left (NoBranch (Right (PrimChar 'a')) [PatPrim (PrimChar 'b')]) + unit_1 :: Assertion unit_1 = let e = create1 emptyHole @@ -153,10 +189,10 @@ unit_7 = unit_8 :: Assertion unit_8 = - let e = mapEven 10 + let e = Expected.mapEven 10 in do - s <- evalFullTest builtinTypes (defMap e) Syn (forgetMetadata $ expr e) - s @?= Right (forgetMetadata $ expectedResult e) + s <- evalFullTest builtinTypes (Expected.defMap e) Syn (forgetMetadata $ Expected.expr e) + s @?= Right (forgetMetadata $ Expected.expectedResult e) -- A worker/wrapper'd map unit_9 :: Assertion @@ -859,70 +895,283 @@ unit_prim_partial_map = s <- evalFullTest builtinTypes (gs <> prims) Syn e s @?= Right r --- TODO: enable when have EvalFullRequest with interp ----- Test that handleEvalFullRequest will reduce imported terms --- unit_eval_full_modules :: Assertion --- unit_eval_full_modules = --- let test = do --- builtinModule' <- builtinModule --- primitiveModule' <- primitiveModule --- importModules [primitiveModule', builtinModule'] --- foo <- pfun ToUpper `app` char 'a' --- resp <- --- readerToState --- $ handleEvalFullRequest --- EvalFullReq --- { evalFullReqExpr = foo --- , evalFullCxtDir = Chk --- , evalFullMaxSteps = 2 --- , evalFullOptions = UnderBinders --- } --- expect <- char 'A' --- pure $ case resp of --- EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" --- EvalFullRespNormal e -> e ~= expect --- a = newEmptyApp --- in runAppTestM a test <&> fst >>= \case --- Left err -> assertFailure $ show err --- Right assertion -> assertion - ----- TODO: enable when have EvalFullRequest with interp ----- Test that handleEvalFullRequest will reduce case analysis of imported types --- unit_eval_full_modules_scrutinize_imported_type :: Assertion --- unit_eval_full_modules_scrutinize_imported_type = --- let test = do --- m' <- m --- importModules [m'] --- foo <- --- case_ --- (con0 cTrue `ann` tcon tBool) --- [branch cTrue [] $ con0 cFalse, branch cFalse [] $ con0 cTrue] --- resp <- --- readerToState --- $ handleEvalFullRequest --- $ EvalFullReq --- { evalFullReqExpr = foo --- , evalFullCxtDir = Chk --- , evalFullMaxSteps = 2 --- , evalFullOptions = UnderBinders --- } --- expect <- con0 cFalse --- pure $ case resp of --- EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" --- EvalFullRespNormal e -> e ~= expect --- a = newEmptyApp --- in runAppTestM a test <&> fst >>= \case --- Left err -> assertFailure $ show err --- Right assertion -> assertion --- where --- m = do --- boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef --- pure --- $ Module --- { moduleName = qualifiedModule tBool --- , moduleTypes = Map.singleton (baseName tBool) boolDef' --- , moduleDefs = mempty --- } +-- Test that 'handleEvalInterpRequest' will reduce imported terms +unit_eval_interp_full_modules :: Assertion +unit_eval_interp_full_modules = + let test = do + builtinModule' <- builtinModule + primitiveModule' <- primitiveModule + importModules [primitiveModule', builtinModule'] + foo <- pfun ToUpper `app` char 'a' + (EvalInterpRespNormal e) <- + readerToState + $ handleEvalInterpRequest + EvalInterpReq + { expr = foo + , dir = Chk + } + expect <- char 'A' + pure $ e ~= expect + a = newEmptyApp + in runAppTestM a test <&> fst >>= \case + Left err -> assertFailure $ show err + Right assertion -> assertion + +-- Test that 'handleEvalBoundedInterpRequest' will reduce imported terms +unit_eval_interp_full_modules_bounded :: Assertion +unit_eval_interp_full_modules_bounded = + let test = do + builtinModule' <- builtinModule + primitiveModule' <- primitiveModule + importModules [primitiveModule', builtinModule'] + foo <- pfun ToUpper `app` char 'a' + resp <- + readerToState + $ handleEvalBoundedInterpRequest + EvalBoundedInterpReq + { expr = foo + , dir = Chk + , timeout = MicroSec 100 + } + expect <- char 'A' + pure $ case resp of + EvalBoundedInterpRespFailed err -> assertFailure $ show err + EvalBoundedInterpRespNormal e -> e ~= expect + a = newEmptyApp + in runAppTestM a 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 +unit_eval_interp_full_modules_scrutinize_imported_type = + let test = do + m' <- m + importModules [m'] + foo <- + case_ + (con0 cTrue `ann` tcon tBool) + [branch cTrue [] $ con0 cFalse, branch cFalse [] $ con0 cTrue] + (EvalInterpRespNormal e) <- + readerToState + $ handleEvalInterpRequest + $ EvalInterpReq + { expr = foo + , dir = Chk + } + expect <- con0 cFalse + pure $ e ~= expect + a = newEmptyApp + in runAppTestM a test <&> fst >>= \case + Left err -> assertFailure $ show err + Right assertion -> assertion + where + m = do + boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef + pure + $ Module + { moduleName = qualifiedModule tBool + , moduleTypes = M.singleton (baseName tBool) boolDef' + , moduleDefs = mempty + } + +-- Test that 'handleEvalBoundedInterpRequest' will reduce case analysis +-- of imported types +unit_eval_interp_full_modules_scrutinize_imported_type_bounded :: Assertion +unit_eval_interp_full_modules_scrutinize_imported_type_bounded = + let test = do + m' <- m + importModules [m'] + foo <- + case_ + (con0 cTrue `ann` tcon tBool) + [branch cTrue [] $ con0 cFalse, branch cFalse [] $ con0 cTrue] + resp <- + readerToState + $ handleEvalBoundedInterpRequest + $ EvalBoundedInterpReq + { expr = foo + , dir = Chk + , timeout = MicroSec 100 + } + expect <- con0 cFalse + pure $ case resp of + EvalBoundedInterpRespFailed err -> assertFailure $ show err + EvalBoundedInterpRespNormal e -> e ~= expect + a = newEmptyApp + in runAppTestM a test <&> fst >>= \case + Left err -> assertFailure $ show err + Right assertion -> assertion + where + m = do + boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef + pure + $ Module + { moduleName = qualifiedModule tBool + , moduleTypes = M.singleton (baseName tBool) boolDef' + , moduleDefs = mempty + } + +-- Test that 'handleEvalBoundedInterpRequest' will return timeouts. +unit_eval_interp_handle_eval_bounded_timeout :: Assertion +unit_eval_interp_handle_eval_bounded_timeout = + let test = do + m' <- m + importModules [m'] + e <- letrec "x" (lvar "x") (tcon tBool) (lvar "x") + resp <- + readerToState + $ handleEvalBoundedInterpRequest + $ EvalBoundedInterpReq + { expr = e + , dir = Chk + , timeout = MicroSec 10_000 + } + pure $ case resp of + EvalBoundedInterpRespFailed err -> err @?= Timeout + EvalBoundedInterpRespNormal _ -> assertFailure "expected timeout" + a = newEmptyApp + in runAppTestM a test <&> fst >>= \case + Left err -> assertFailure $ show err + Right assertion -> assertion + where + m = do + boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef + pure + $ Module + { moduleName = qualifiedModule tBool + , moduleTypes = M.singleton (baseName tBool) boolDef' + , moduleDefs = mempty + } + +-- Test that 'handleEvalBoundedInterpRequest' will return an error +-- when a case branch is missing. +unit_eval_interp_handle_eval_bounded_missing_branch :: Assertion +unit_eval_interp_handle_eval_bounded_missing_branch = + let test = do + m' <- m + importModules [m'] + e <- case_ (con0 cTrue `ann` tcon tBool) [branch cFalse [] emptyHole] + resp <- + readerToState + $ handleEvalBoundedInterpRequest + $ EvalBoundedInterpReq + { expr = e + , dir = Chk + , timeout = MicroSec 10_000 + } + let expect = NoBranch (Left cTrue) [PatCon cFalse] + pure $ case resp of + EvalBoundedInterpRespFailed err -> err @?= expect + EvalBoundedInterpRespNormal _ -> assertFailure "expected NoBranch" + a = newEmptyApp + in runAppTestM a test <&> fst >>= \case + Left err -> assertFailure $ show err + Right assertion -> assertion + where + m = do + boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef + pure + $ Module + { moduleName = qualifiedModule tBool + , moduleTypes = M.singleton (baseName tBool) boolDef' + , moduleDefs = mempty + } + +-- Test that 'handleEvalInterpRequest' will throw an 'InterpError' +-- exception when a case branch is missing. +unit_eval_interp_handle_eval_missing_branch :: Assertion +unit_eval_interp_handle_eval_missing_branch = + let test = do + m' <- m + importModules [m'] + foo <- case_ (con0 cTrue `ann` tcon tBool) [branch cFalse [] emptyHole] + tryJust + (\(ex :: InterpError) -> Just ex) + $ readerToState + $ handleEvalInterpRequest + $ EvalInterpReq + { expr = foo + , dir = Chk + } + a = newEmptyApp + in runAppTestM a test <&> fst >>= \case + Left err -> assertFailure $ "expected NoBranch exception, got " ++ show err + Right ex -> ex @?= Left (NoBranch (Left cTrue) [PatCon cFalse]) + where + m = do + boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef + pure + $ Module + { moduleName = qualifiedModule tBool + , moduleTypes = M.singleton (baseName tBool) boolDef' + , moduleDefs = mempty + } + +-- Test that 'handleEvalBoundedInterpRequest' will return an error +-- when a case branch is missing (primitive version). +unit_eval_interp_handle_eval_bounded_missing_branch_prim :: Assertion +unit_eval_interp_handle_eval_bounded_missing_branch_prim = + let test = do + m' <- m + importModules [m'] + e <- case_ (char 'a' `ann` tcon tChar) [branchPrim (PrimChar 'b') emptyHole] + resp <- + readerToState + $ handleEvalBoundedInterpRequest + $ EvalBoundedInterpReq + { expr = e + , dir = Chk + , timeout = MicroSec 10_000 + } + let expect = NoBranch (Right (PrimChar 'a')) [PatPrim (PrimChar 'b')] + pure $ case resp of + EvalBoundedInterpRespFailed err -> err @?= expect + EvalBoundedInterpRespNormal _ -> assertFailure "expected NoBranch" + a = newEmptyApp + in runAppTestM a test <&> fst >>= \case + Left err -> assertFailure $ show err + Right assertion -> assertion + where + m = do + boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef + pure + $ Module + { moduleName = qualifiedModule tBool + , moduleTypes = M.singleton (baseName tBool) boolDef' + , moduleDefs = mempty + } + +-- Test that 'handleEvalInterpRequest' will throw an 'InterpError' +-- exception when a case branch is missing (primitive version). +unit_eval_interp_handle_eval_missing_branch_prim :: Assertion +unit_eval_interp_handle_eval_missing_branch_prim = + let test = do + m' <- m + importModules [m'] + foo <- case_ (char 'a' `ann` tcon tChar) [branchPrim (PrimChar 'b') emptyHole] + tryJust + (\(ex :: InterpError) -> Just ex) + $ readerToState + $ handleEvalInterpRequest + $ EvalInterpReq + { expr = foo + , dir = Chk + } + a = newEmptyApp + in runAppTestM a test <&> fst >>= \case + Left err -> assertFailure $ "expected NoBranch exception, got " ++ show err + Right ex -> ex @?= Left (NoBranch (Right (PrimChar 'a')) [PatPrim (PrimChar 'b')]) + where + m = do + boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef + pure + $ Module + { moduleName = qualifiedModule tBool + , moduleTypes = M.singleton (baseName tBool) boolDef' + , moduleDefs = mempty + } -- There's a similar test in the step evaluator test suite, but the -- implementation is sufficiently different that it doesn't make sense diff --git a/primer/test/Tests/Undo.hs b/primer/test/Tests/Undo.hs index 5d6e253f7..624535b78 100644 --- a/primer/test/Tests/Undo.hs +++ b/primer/test/Tests/Undo.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE DuplicateRecordFields #-} + module Tests.Undo where import Foreword @@ -9,7 +11,9 @@ import Primer.App ( ProgError, appProg, handleEditRequest, + handleEvalBoundedInterpRequest, handleEvalFullRequest, + handleEvalInterpRequest, handleMutationRequest, progModules, ) @@ -25,6 +29,9 @@ import Primer.Core ( ) import Primer.Def (astDefExpr, defAST) import Primer.Eval (Dir (Syn), NormalOrderOptions (UnderBinders)) +import Primer.EvalFullInterp ( + Timeout (MicroSec), + ) import Primer.Module ( moduleDefsQualified, moduleName, @@ -95,3 +102,90 @@ unit_redo_eval = a8 <- run' redo a7 finalApp <- run' eval a8 finalApp @?= newApp + +unit_redo_eval_interp :: Assertion +unit_redo_eval_interp = + let originalApp = App.newApp + scope = mainModuleName $ appProg originalApp + action1 = + [ MoveToDef $ qualifyName scope "main" + , BodyAction [InsertSaturatedVar $ GlobalVarRef Integer.even] + ] + action2 i = + [ MoveToDef $ qualifyName scope "main" + , BodyAction + [ SetCursor i + , ConstructPrim $ PrimInt 4 + ] + ] + eval = + readerToState + $ handleEvalInterpRequest + App.EvalInterpReq + { App.expr = Var (Meta 0 Nothing Nothing) (GlobalVarRef $ qualifyName scope "main") + , App.dir = Syn + } + edit1 = handleEditRequest action1 + edit2 = handleEditRequest . action2 + undo = handleMutationRequest App.Undo + redo = handleMutationRequest App.Redo + run' act app = fmap snd . expectSuccess =<< runAppTestM app act + in do + originalApp' <- run' eval originalApp + newApp1 <- run' edit1 originalApp' + i <- case fmap astDefExpr . defAST =<< foldMap' moduleDefsQualified (progModules $ appProg newApp1) M.!? qualifyName scope "main" of + Just (App _ _ e) -> pure $ getID e + _ -> liftIO $ assertFailure "unexpected form of main" + newApp <- run' (edit2 i) newApp1 + a3 <- run' undo newApp + a4 <- run' redo a3 + a5 <- run' undo a4 + a6 <- run' undo a5 + a7 <- run' redo a6 + a8 <- run' redo a7 + finalApp <- run' eval a8 + finalApp @?= newApp + +unit_redo_eval_interp_bounded :: Assertion +unit_redo_eval_interp_bounded = + let originalApp = App.newApp + scope = mainModuleName $ appProg originalApp + action1 = + [ MoveToDef $ qualifyName scope "main" + , BodyAction [InsertSaturatedVar $ GlobalVarRef Integer.even] + ] + action2 i = + [ MoveToDef $ qualifyName scope "main" + , BodyAction + [ SetCursor i + , ConstructPrim $ PrimInt 4 + ] + ] + eval = + readerToState + $ handleEvalBoundedInterpRequest + App.EvalBoundedInterpReq + { App.expr = Var (Meta 0 Nothing Nothing) (GlobalVarRef $ qualifyName scope "main") + , App.dir = Syn + , App.timeout = MicroSec 100 + } + edit1 = handleEditRequest action1 + edit2 = handleEditRequest . action2 + undo = handleMutationRequest App.Undo + redo = handleMutationRequest App.Redo + run' act app = fmap snd . expectSuccess =<< runAppTestM app act + in do + originalApp' <- run' eval originalApp + newApp1 <- run' edit1 originalApp' + i <- case fmap astDefExpr . defAST =<< foldMap' moduleDefsQualified (progModules $ appProg newApp1) M.!? qualifyName scope "main" of + Just (App _ _ e) -> pure $ getID e + _ -> liftIO $ assertFailure "unexpected form of main" + newApp <- run' (edit2 i) newApp1 + a3 <- run' undo newApp + a4 <- run' redo a3 + a5 <- run' undo a4 + a6 <- run' undo a5 + a7 <- run' redo a6 + a8 <- run' redo a7 + finalApp <- run' eval a8 + finalApp @?= newApp diff --git a/primer/testlib/Primer/Test/App.hs b/primer/testlib/Primer/Test/App.hs index d3d6a099a..4bf9c9679 100644 --- a/primer/testlib/Primer/Test/App.hs +++ b/primer/testlib/Primer/Test/App.hs @@ -32,8 +32,8 @@ import Primer.Core.Meta ( ) import Primer.Examples qualified as Examples import Primer.Log ( - PureLog, - runPureLog, + PureLogT, + runPureLogT, ) import Primer.Module ( Module ( @@ -53,13 +53,13 @@ import Primer.Test.Util ( assertNoSevereLogs, ) -newtype AppTestM a = AppTestM +newtype AppTestT m a = AppTestT { unAppTestM :: ( StateT App ( ExceptT ProgError - (PureLog (WithSeverity LogMsg)) + (PureLogT (WithSeverity LogMsg) m) ) ) a @@ -68,28 +68,39 @@ newtype AppTestM a = AppTestM ( Functor , Applicative , Monad + , MonadIO , MonadLog (WithSeverity LogMsg) , MonadState App , MonadError ProgError + , MonadCatch + , MonadThrow ) deriving ( MonadFresh ID , MonadFresh NameCounter ) - via FreshViaApp AppTestM + via FreshViaApp (AppTestT m) --- Recall that Assertion = IO () --- This is in IO as it asserts that there were no severe log messages -runAppTestM :: App -> AppTestM a -> IO (Either ProgError a, App) -runAppTestM a m = - let (r, logs) = runAppTestM' a m - in assertNoSevereLogs logs $> r +type AppTestM a = AppTestT IO a + +-- Recall that @Assertion = IO ()@ +-- +-- This is in 'MonadIO' as it asserts that there were no severe log +-- messages +runAppTestT :: (MonadIO m) => App -> AppTestT m a -> m (Either ProgError a, App) +runAppTestT a m = do + (r, logs) <- runAppTestT' a m + liftIO $ assertNoSevereLogs logs $> r -runAppTestM' :: App -> AppTestM a -> ((Either ProgError a, App), Seq (WithSeverity LogMsg)) -runAppTestM' a m = - case runPureLog $ runExceptT $ flip runStateT a $ unAppTestM m of - (Left err, logs) -> ((Left err, a), logs) - (Right (res, app'), logs) -> ((Right res, app'), logs) +runAppTestT' :: (Monad m) => App -> AppTestT m a -> m ((Either ProgError a, App), Seq (WithSeverity LogMsg)) +runAppTestT' a m = do + (r, logs) <- runPureLogT $ runExceptT $ flip runStateT a $ unAppTestM m + case r of + Left err -> pure ((Left err, a), logs) + Right (res, app') -> pure ((Right res, app'), logs) + +runAppTestM :: App -> AppTestM a -> IO (Either ProgError a, App) +runAppTestM = runAppTestT -- | An initial test 'App' instance that contains all default type -- definitions (including primitive types), all primitive functions, diff --git a/primer/testlib/Primer/Test/Eval.hs b/primer/testlib/Primer/Test/Eval.hs index e23c19996..c1b944be0 100644 --- a/primer/testlib/Primer/Test/Eval.hs +++ b/primer/testlib/Primer/Test/Eval.hs @@ -1,4 +1,6 @@ module Primer.Test.Eval ( + illTypedMissingBranch, + illTypedMissingBranchPrim, noTermShadowing, noTypeShadowing, recursiveLetRec', @@ -42,6 +44,7 @@ import Primer.Core ( GVarName, LVarName, ModuleName, + PrimCon (PrimChar), TyVarName, ) import Primer.Core.DSL ( @@ -50,6 +53,7 @@ import Primer.Core.DSL ( ann, app, branch, + branchPrim, case_, char, con, @@ -97,6 +101,15 @@ import Primer.Test.Util ( primDefs, ) +-- | An ill typed term: a pattern match with a missing branch. +illTypedMissingBranch :: S Expr +illTypedMissingBranch = case_ (con0 cTrue `ann` tcon tBool) [branch cFalse [] emptyHole] + +-- | An ill typed term: a pattern match on a primitive with a missing +-- branch. +illTypedMissingBranchPrim :: S Expr +illTypedMissingBranchPrim = case_ (char 'a' `ann` tcon tChar) [branchPrim (PrimChar 'b') emptyHole] + -- | Ensure we don't have shadowing issues with types. -- -- Note that the new name of the renamed type variable is From 460cb3e09e590acd8140bc81c1af14c6854149e7 Mon Sep 17 00:00:00 2001 From: Drew Hess Date: Wed, 17 Apr 2024 17:21:14 +0100 Subject: [PATCH 2/6] chore(primer): add interpreter test to actions tests This test change is a separate commit to the parent commit because it requires a change to `EditAppM`, namely adding a `MonadIO` instance to it. Prior to this change, no action tests required `IO`. Signed-off-by: Drew Hess --- primer/src/Primer/App.hs | 2 +- primer/test/Tests/Action/Available.hs | 37 +++++++++++++++++++-------- 2 files changed, 28 insertions(+), 11 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index c76e08c93..d5eee4187 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -1479,7 +1479,7 @@ type MonadQueryApp m e = (Monad m, MonadReader App m, MonadError e m) -- state. This is important to ensure that we can reliably replay the -- log without having ID mismatches. newtype EditAppM m e a = EditAppM (StateT App (ExceptT e m) a) - deriving newtype (Functor, Applicative, Monad, MonadState App, MonadError e, MonadLog l) + deriving newtype (Functor, Applicative, Monad, MonadIO, MonadState App, MonadError e, MonadLog l) -- | Run an 'EditAppM' action, returning a result and an updated -- 'App'. diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index a6b0a211d..462002b6a 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -54,6 +54,7 @@ import Primer.App ( DefSelection (..), EditAppM, Editable (..), + EvalBoundedInterpReq (EvalBoundedInterpReq), EvalFullReq (EvalFullReq), EvalReq (EvalReq), Level (Beginner, Expert, Intermediate), @@ -79,6 +80,7 @@ import Primer.App ( checkAppWellFormed, checkProgWellFormed, handleEditRequest, + handleEvalBoundedInterpRequest, handleEvalFullRequest, handleEvalRequest, handleMutationRequest, @@ -155,6 +157,9 @@ import Primer.Def ( defAST, ) import Primer.Eval (EvalError (NotRedex), NormalOrderOptions (StopAtBinders, UnderBinders)) +import Primer.EvalFullInterp ( + Timeout (MicroSec), + ) import Primer.EvalFullStep (Dir (Chk)) import Primer.Examples (comprehensiveWellTyped) import Primer.Gen.App (genApp) @@ -167,9 +172,13 @@ import Primer.Gen.Core.Typed ( genSyn, genWTKind, genWTType, + isolateWT, propertyWT, ) -import Primer.Log (PureLog, runPureLog) +import Primer.Log ( + PureLogT, + runPureLogT, + ) import Primer.Module ( Module (Module, moduleDefs), builtinModule, @@ -345,6 +354,7 @@ tasty_multiple_requests_accepted = withTests 500 , Just (1, Eval1) , if null $ appDefs a' then Nothing else Just (1, EvalFull) , Just (1, Question) + , if null $ appDefs a' then Nothing else Just (1, EvalBoundedInterp) , if undoLogEmpty $ appProg a' then Nothing else Just (2, Undo) , if redoLogEmpty $ appProg a' then Nothing else Just (2, Redo) , Just (1, RenameModule) @@ -375,6 +385,11 @@ tasty_multiple_requests_accepted = withTests 500 steps <- forAllT $ Gen.integral $ Range.linear 0 100 optsN <- forAllT $ Gen.element @[] [StopAtBinders, UnderBinders] actionSucceeds (readerToState $ handleEvalFullRequest $ EvalFullReq tld Chk steps optsN) appN + EvalBoundedInterp -> do + g <- forAllT $ Gen.element $ appDefs appN + tld <- gvar g + usec <- forAllT $ Gen.integral $ Range.linear 0 1000 + actionSucceeds (readerToState $ handleEvalBoundedInterpRequest $ EvalBoundedInterpReq tld Chk (MicroSec usec)) appN Question -> do -- Obtain a non-exhaustive case warning if we add a new question let _w :: Question q -> () @@ -441,6 +456,7 @@ data Act | AddTy | Eval1 | EvalFull + | EvalBoundedInterp | Question | Undo | Redo @@ -448,23 +464,24 @@ data Act | AvailAct deriving stock (Show) --- Helper for tasty_available_actions_accepted and tasty_chained_actions_undo_accepted +-- Helpers for tasty_available_actions_accepted and tasty_chained_actions_undo_accepted + runEditAppMLogs :: - HasCallStack => - EditAppM (PureLog (WithSeverity ())) ProgError a -> + (HasCallStack) => + EditAppM (PureLogT (WithSeverity ()) WT) ProgError a -> App -> PropertyT WT (Either ProgError a, App) -runEditAppMLogs m a = case runPureLog $ runEditAppM m a of - (r, logs) -> testNoSevereLogs logs >> pure r +runEditAppMLogs m a = do + (r, logs) <- lift $ isolateWT $ runPureLogT $ runEditAppM m a + testNoSevereLogs logs >> pure r --- Helper for tasty_available_actions_accepted and tasty_chained_actions_undo_accepted -actionSucceeds :: HasCallStack => EditAppM (PureLog (WithSeverity ())) ProgError a -> App -> PropertyT WT App +actionSucceeds :: HasCallStack => EditAppM (PureLogT (WithSeverity ()) WT) ProgError a -> App -> PropertyT WT App actionSucceeds m a = runEditAppMLogs m a >>= \case (Left err, _) -> annotateShow err >> failure (Right _, a') -> ensureSHNormal a' $> a' -actionSucceedsOrNotRedex :: HasCallStack => EditAppM (PureLog (WithSeverity ())) ProgError a -> App -> PropertyT WT App +actionSucceedsOrNotRedex :: HasCallStack => EditAppM (PureLogT (WithSeverity ()) WT) ProgError a -> App -> PropertyT WT App actionSucceedsOrNotRedex m a = runEditAppMLogs m a >>= \case (Left (EvalError NotRedex), _) -> do @@ -478,7 +495,7 @@ actionSucceedsOrNotRedex m a = -- Similar to 'actionSucceeds' but bearing in mind that -- if we submit our own name rather than an offered one, then -- we should expect that name capture/clashing may happen -actionSucceedsOrCapture :: HasCallStack => EditAppM (PureLog (WithSeverity ())) ProgError a -> App -> PropertyT WT (SucceedOrCapture App) +actionSucceedsOrCapture :: HasCallStack => EditAppM (PureLogT (WithSeverity ()) WT) ProgError a -> App -> PropertyT WT (SucceedOrCapture App) actionSucceedsOrCapture m a = do a' <- runEditAppMLogs m a case a' of From 2fbc1c1ed801a19d11e1424e79ade22a77f51994 Mon Sep 17 00:00:00 2001 From: Drew Hess Date: Thu, 18 Apr 2024 01:36:03 +0100 Subject: [PATCH 3/6] chore(primer-api): expose the interpreter via the API Signed-off-by: Drew Hess --- primer-api/src/Primer/API.hs | 194 +++++++++++++++++++++++++++++++++++ primer-api/test/Tests/API.hs | 8 +- primer/src/Primer/App.hs | 2 +- 3 files changed, 202 insertions(+), 2 deletions(-) diff --git a/primer-api/src/Primer/API.hs b/primer-api/src/Primer/API.hs index e36e781b3..295e8d16e 100644 --- a/primer-api/src/Primer/API.hs +++ b/primer-api/src/Primer/API.hs @@ -54,6 +54,12 @@ module Primer.API ( evalFull, EvalFullResp (..), evalFull', + evalBoundedInterp, + EvalBoundedInterpResp (..), + evalBoundedInterp', + evalInterp, + EvalInterpResp (..), + evalInterp', flushSessions, createDefinition, createTypeDef, @@ -127,7 +133,9 @@ import Primer.App ( DefSelection (..), EditAppM, Editable, + EvalBoundedInterpReq (..), EvalFullReq (..), + EvalInterpReq (..), EvalReq (..), EvalResp (..), Level, @@ -141,7 +149,9 @@ import Primer.App ( TypeDefParamSelection (..), TypeDefSelection (..), appProg, + handleEvalBoundedInterpRequest, handleEvalFullRequest, + handleEvalInterpRequest, handleEvalRequest, handleGetProgramRequest, handleMutationRequest, @@ -240,6 +250,10 @@ import Primer.Def ( import Primer.Def qualified as Def import Primer.Eval (NormalOrderOptions (StopAtBinders)) import Primer.Eval.Redex (Dir (Chk), EvalLog) +import Primer.EvalFullInterp ( + InterpError (..), + Timeout (MicroSec), + ) import Primer.EvalFullStep (TerminationBound) import Primer.JSON ( CustomJSON (..), @@ -432,6 +446,10 @@ data APILog | EvalStep (ReqResp (SessionId, EvalReq) (Either ProgError EvalResp)) | EvalFull (ReqResp (SessionId, EvalFullReq) (Either ProgError App.EvalFullResp)) | EvalFull' (ReqResp (SessionId, Maybe TerminationBound, Maybe NormalOrderOptions, GVarName) EvalFullResp) + | EvalBoundedInterp (ReqResp (SessionId, EvalBoundedInterpReq) (Either ProgError App.EvalBoundedInterpResp)) + | EvalBoundedInterp' (ReqResp (SessionId, Maybe Timeout, GVarName) EvalBoundedInterpResp) + | EvalInterp (ReqResp (SessionId, EvalInterpReq) (Either ProgError App.EvalInterpResp)) + | EvalInterp' (ReqResp (SessionId, GVarName) EvalInterpResp) | FlushSessions (ReqResp () ()) | CreateDef (ReqResp (SessionId, ModuleName, Maybe Text) Prog) | CreateTypeDef (ReqResp (SessionId, TyConName, [ValConName]) Prog) @@ -1253,6 +1271,182 @@ evalFull' = curry4 $ logAPI (noError EvalFull') $ \(sid, lim, closed, d) -> do Right a -> a Left v -> absurd v +-- | Using the interpreter, evaluate an expression given by the +-- 'EvalInterpReq', in the context of the application contained +-- in the given 'SessionId'. +-- +-- Caution: depending on the expression being evaluated, the +-- evaluation may not terminate, and/or may grow in unbounded size. If +-- your application is not prepared to handle this situation, you may +-- want to use 'evalBoundedInterp', instead. +-- +-- N.B.: this action may 'Control.Exception.throw' an imprecise +-- exception of type 'InterpError' in the event that the expression to +-- be evaluated is not well typed. In normal use, however, this +-- condition should not arise. See 'Primer.EvalFullInterp.interp'', +-- which this action uses, for details. (Note that the +-- 'InterpError.Timeout' exception value will never be thrown by this +-- action, as explained above.) +evalInterp :: + (MonadIO m, MonadThrow m, MonadAPILog l m) => + SessionId -> + EvalInterpReq -> + PrimerM m (Either ProgError App.EvalInterpResp) +evalInterp = curry $ logAPI (leftResultError EvalInterp) $ \(sid, req) -> do + app <- getApp sid + runQueryAppM (handleEvalInterpRequest req) app + +-- | This type is the API's view of a 'App.EvalInterpResp'. +newtype EvalInterpResp + = EvalInterpRespNormal Tree + deriving stock (Show, Read, Generic) + deriving (ToJSON, FromJSON) via PrimerJSON EvalInterpResp + +-- | Using the interpreter, evaluate the top-level definition whose +-- name is given in the 'GVarName', in the context of the application +-- contained in the given 'SessionId'. +-- +-- This is a simplified version of 'evalInterp', intended for +-- non-Haskell clients. +-- +-- Caution: depending on the expression being evaluated, the +-- evaluation may not terminate, and/or may grow in unbounded size. If +-- your application is not prepared to handle this situation, you may +-- want to use 'evalBoundedInterp'', instead. +-- +-- N.B.: this action may 'Control.Exception.throw' an imprecise +-- exception of type 'InterpError' in the event that the expression to +-- be evaluated is not well typed. In normal use, however, this +-- condition should not arise. See 'Primer.EvalFullInterp.interp'', +-- which this action uses, for details. (Note that the +-- 'InterpError.Timeout' exception value will never be thrown by this +-- action, as explained above.) +evalInterp' :: + forall m l. + (MonadIO m, MonadThrow m, MonadAPILog l m) => + SessionId -> + GVarName -> + PrimerM m EvalInterpResp +evalInterp' = curry $ logAPI (noError EvalInterp') $ \(sid, d) -> do + app <- getApp sid + noErr <$> runQueryAppM (q d) app + where + q :: + GVarName -> + QueryAppM (PrimerM m) Void EvalInterpResp + q d = do + -- We don't care about uniqueness of this ID, and we do not want to + -- disturb any FreshID state, since that could break undo/redo. + -- The reason we don't care about uniqueness is that this node will never + -- exist alongside anything else that it may clash with, as the first + -- evaluation step will be to inline this definition, removing the node. + let e = create' $ DSL.gvar d + (App.EvalInterpRespNormal e') <- + handleEvalInterpRequest + $ EvalInterpReq + { expr = e + , dir = Chk + } + pure $ EvalInterpRespNormal $ viewTreeExpr e' + noErr :: Either Void a -> a + noErr = \case + Right a -> a + Left v -> absurd v + +-- | Using the interpreter, evaluate an expression given by the +-- 'EvalBoundedInterpReq', in the context of the application contained +-- in the given 'SessionId'. The evaluation time is bounded by the +-- timeout provided in the same 'EvalBoundedInterpReq'. +-- +-- Note that, unlike evaluation requests that use the step evaluator, +-- if this action times out during evaluation, the result is an error, +-- not a partially-evaluated expression. +evalBoundedInterp :: + (MonadIO m, MonadThrow m, MonadAPILog l m) => + SessionId -> + EvalBoundedInterpReq -> + PrimerM m (Either ProgError App.EvalBoundedInterpResp) +evalBoundedInterp = curry $ logAPI (leftResultError EvalBoundedInterp) $ \(sid, req) -> do + app <- getApp sid + runQueryAppM (handleEvalBoundedInterpRequest req) app + +-- | This type is a simplified version of 'App.EvalBoundedInterpResp'. +-- It is intended for non-Haskell clients. +-- +-- (Specifically, this type exists so we don't need to serialize +-- complicated 'Primer.EvalFullInterp.InterpError' values that are +-- likely not helpful for a non-Haskell API client.) +data EvalBoundedInterpResp + = -- | The evaluation timed out. + EvalBoundedInterpRespTimeout + | -- | The interpreter encountered a @match@ expression with at + -- least one missing branch. This error should never occur in a + -- well typed program. + EvalBoundedInterpRespNoBranch + | -- | The interpreter encountered an undefined type constructor. + -- This error should never occur in a well typed program. + EvalBoundedInterpRespUnknownTyCon TyConName + | -- | The interpreter encountered an undefined value constructor. + -- This error should never occur in a well typed program. + EvalBoundedInterpRespUnknownValCon TyConName ValConName + | -- | The evaluation succeeded. The 'Tree' represents the normal form + -- of the expression being evaluated. + EvalBoundedInterpRespNormal Tree + deriving stock (Show, Read, Generic) + deriving (ToJSON, FromJSON) via PrimerJSON EvalBoundedInterpResp + +-- | Using the interpreter, evaluate the top-level definition whose +-- name is given in the 'GVarName', in the context of the application +-- contained in the given 'SessionId'. The evaluation time is bounded +-- by the 'Timeout' argument, or is limited to 10 microseconds if the +-- timeout is not provided. +-- +-- Note that, unlike evaluation requests that use the step evaluator, +-- if this action times out during evaluation, the result is an error, +-- not a partially-evaluated expression. +-- +-- This is a simplified version of 'evalBoundedInterp', intended for +-- non-Haskell clients. +evalBoundedInterp' :: + forall m l. + (MonadIO m, MonadThrow m, MonadAPILog l m) => + SessionId -> + Maybe Timeout -> + GVarName -> + PrimerM m EvalBoundedInterpResp +evalBoundedInterp' = curry3 $ logAPI (noError EvalBoundedInterp') $ \(sid, timeout, d) -> do + app <- getApp sid + noErr <$> runQueryAppM (q timeout d) app + where + q :: + Maybe Timeout -> + GVarName -> + QueryAppM (PrimerM m) Void EvalBoundedInterpResp + q timeout d = do + -- We don't care about uniqueness of this ID, and we do not want to + -- disturb any FreshID state, since that could break undo/redo. + -- The reason we don't care about uniqueness is that this node will never + -- exist alongside anything else that it may clash with, as the first + -- evaluation step will be to inline this definition, removing the node. + let e = create' $ DSL.gvar d + x <- + handleEvalBoundedInterpRequest + $ EvalBoundedInterpReq + { expr = e + , dir = Chk + , timeout = fromMaybe (MicroSec 10) timeout + } + pure $ case x of + App.EvalBoundedInterpRespFailed Timeout -> EvalBoundedInterpRespTimeout + App.EvalBoundedInterpRespFailed (NoBranch _ _) -> EvalBoundedInterpRespNoBranch + App.EvalBoundedInterpRespFailed (UnknownTyCon n) -> EvalBoundedInterpRespUnknownTyCon n + App.EvalBoundedInterpRespFailed (UnknownValCon tn vn) -> EvalBoundedInterpRespUnknownValCon tn vn + App.EvalBoundedInterpRespNormal e' -> EvalBoundedInterpRespNormal $ viewTreeExpr e' + noErr :: Either Void a -> a + noErr = \case + Right a -> a + Left v -> absurd v + flushSessions :: (MonadIO m, MonadAPILog l m) => PrimerM m () flushSessions = logAPI' FlushSessions $ do sessionsTransaction $ \ss _ -> do diff --git a/primer-api/test/Tests/API.hs b/primer-api/test/Tests/API.hs index 5de63b9e9..c6b0c3c43 100644 --- a/primer-api/test/Tests/API.hs +++ b/primer-api/test/Tests/API.hs @@ -18,6 +18,7 @@ import Primer.API ( copySession, deleteSession, edit, + evalBoundedInterp', evalFull', findSessions, flushSessions, @@ -73,6 +74,9 @@ import Primer.Database ( ) import Primer.Def (astDefExpr, astDefType, defAST) import Primer.Eval (NormalOrderOptions (UnderBinders)) +import Primer.EvalFullInterp ( + Timeout (MicroSec), + ) import Primer.Examples ( comprehensive, even3App, @@ -491,7 +495,7 @@ test_eval_undo = step "create session" sid <- newSession $ NewSessionReq "a new session" True let scope = mkSimpleModuleName "Main" - step "eval" + step "evalFull'" void $ evalFull' sid (Just 100) (Just UnderBinders) $ qualifyName scope "main" step "insert λ" let getMain = do @@ -532,6 +536,8 @@ test_eval_undo = _ <- undo sid step "redo" _ <- redo sid + step "evalBoundedInterp'" + void $ evalBoundedInterp' sid (Just $ MicroSec 100) $ qualifyName scope "main" step "undo *2" _ <- undo sid >> undo sid step "redo" diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index d5eee4187..5e281b14b 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -1494,7 +1494,7 @@ runEditAppM (EditAppM m) appState = -- Actions run in this monad cannot modify the 'App'. We use 'ExceptT' -- here for compatibility with 'EditApp'. newtype QueryAppM m e a = QueryAppM (ReaderT App (ExceptT e m) a) - deriving newtype (Functor, Applicative, Monad, MonadReader App, MonadError e, MonadLog l) + deriving newtype (Functor, Applicative, Monad, MonadIO, MonadReader App, MonadError e, MonadLog l) -- | Run a 'QueryAppM' action, returning a result. runQueryAppM :: QueryAppM m e a -> App -> m (Either e a) From 45cd3a9c266595a81837d435de0fffc06a5dabfa Mon Sep 17 00:00:00 2001 From: Drew Hess Date: Thu, 18 Apr 2024 20:17:19 +0100 Subject: [PATCH 4/6] feat(primer-service): add bounded interpreter to the HTTP APIs Signed-off-by: Drew Hess --- primer-api/src/Primer/API.hs | 10 +- primer-service/primer-service.cabal | 1 + primer-service/src/Primer/Client.hs | 7 + primer-service/src/Primer/OpenAPI.hs | 2 + primer-service/src/Primer/Servant/API.hs | 8 + primer-service/src/Primer/Servant/OpenAPI.hs | 21 ++- primer-service/src/Primer/Server.hs | 9 ++ primer-service/test/Tests/OpenAPI.hs | 13 ++ .../test/outputs/OpenAPI/openapi.json | 148 ++++++++++++++++++ 9 files changed, 216 insertions(+), 3 deletions(-) diff --git a/primer-api/src/Primer/API.hs b/primer-api/src/Primer/API.hs index 295e8d16e..a3283e528 100644 --- a/primer-api/src/Primer/API.hs +++ b/primer-api/src/Primer/API.hs @@ -1388,7 +1388,13 @@ data EvalBoundedInterpResp EvalBoundedInterpRespUnknownTyCon TyConName | -- | The interpreter encountered an undefined value constructor. -- This error should never occur in a well typed program. - EvalBoundedInterpRespUnknownValCon TyConName ValConName + -- + -- Note: this should be a 'Recordpair TyConName ValConName', but + -- that doesn't serialize properly in our OpenAPI serialization + -- scheme, so instead we only include the unknwon 'ValConName' in + -- this error. See: + -- https://github.com/hackworthltd/primer/issues/1246 + EvalBoundedInterpRespUnknownValCon ValConName | -- | The evaluation succeeded. The 'Tree' represents the normal form -- of the expression being evaluated. EvalBoundedInterpRespNormal Tree @@ -1440,7 +1446,7 @@ evalBoundedInterp' = curry3 $ logAPI (noError EvalBoundedInterp') $ \(sid, timeo App.EvalBoundedInterpRespFailed Timeout -> EvalBoundedInterpRespTimeout App.EvalBoundedInterpRespFailed (NoBranch _ _) -> EvalBoundedInterpRespNoBranch App.EvalBoundedInterpRespFailed (UnknownTyCon n) -> EvalBoundedInterpRespUnknownTyCon n - App.EvalBoundedInterpRespFailed (UnknownValCon tn vn) -> EvalBoundedInterpRespUnknownValCon tn vn + App.EvalBoundedInterpRespFailed (UnknownValCon _ vn) -> EvalBoundedInterpRespUnknownValCon vn App.EvalBoundedInterpRespNormal e' -> EvalBoundedInterpRespNormal $ viewTreeExpr e' noErr :: Either Void a -> a noErr = \case diff --git a/primer-service/primer-service.cabal b/primer-service/primer-service.cabal index 3fde9b9fa..adf97a000 100644 --- a/primer-service/primer-service.cabal +++ b/primer-service/primer-service.cabal @@ -56,6 +56,7 @@ library , primer ^>=0.7.2 , primer-api ^>=0.7.2 , refined ^>=0.8 + , semirings ^>=0.6 , servant >=0.18 && <0.20.2 , servant-client >=0.18 && <0.20.2 , servant-client-core >=0.18 && <0.20.2 diff --git a/primer-service/src/Primer/Client.hs b/primer-service/src/Primer/Client.hs index 13b2f6e5d..3b0329469 100644 --- a/primer-service/src/Primer/Client.hs +++ b/primer-service/src/Primer/Client.hs @@ -20,6 +20,7 @@ module Primer.Client ( generateNames, evalStep, evalFull, + evalBoundedInterp, getProgramOpenApi, availableActionsOpenAPI, actionOptionsOpenAPI, @@ -37,6 +38,8 @@ import Primer.API qualified import Primer.Action.Available (Action, InputAction, NoInputAction, Options) import Primer.App ( App, + EvalBoundedInterpReq, + EvalBoundedInterpResp, EvalFullReq, EvalFullResp, EvalReq, @@ -167,6 +170,10 @@ evalStep sid req = apiClient // API.sessionsAPI // API.sessionAPI /: sid // API. evalFull :: SessionId -> EvalFullReq -> ClientM (Either ProgError EvalFullResp) evalFull sid req = apiClient // API.sessionsAPI // API.sessionAPI /: sid // API.evalFull /: req +-- | As 'Primer.API.evalBoundedInterp'. +evalBoundedInterp :: SessionId -> EvalBoundedInterpReq -> ClientM (Either ProgError EvalBoundedInterpResp) +evalBoundedInterp sid req = apiClient // API.sessionsAPI // API.sessionAPI /: sid // API.evalBoundedInterp /: req + availableActionsOpenAPI :: SessionId -> Level -> Primer.API.Selection -> ClientM [Action] availableActionsOpenAPI sid = openAPIClient // OpenAPI.sessionsAPI // OpenAPI.sessionAPI /: sid // OpenAPI.actions // OpenAPI.available diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs index b640dd2f2..81abd8d1e 100644 --- a/primer-service/src/Primer/OpenAPI.hs +++ b/primer-service/src/Primer/OpenAPI.hs @@ -45,6 +45,7 @@ import Optics ( import Primer.API ( ApplyActionBody, Def, + EvalBoundedInterpResp, EvalFullResp, Module, NewSessionReq, @@ -214,3 +215,4 @@ parseQueryParamRead :: Read a => Text -> Text -> Either Text a parseQueryParamRead m t = maybeToEither ("unknown " <> m <> ": " <> t) $ readMaybe t deriving via PrimerJSON EvalFullResp instance ToSchema EvalFullResp +deriving via PrimerJSON EvalBoundedInterpResp instance ToSchema EvalBoundedInterpResp diff --git a/primer-service/src/Primer/Servant/API.hs b/primer-service/src/Primer/Servant/API.hs index 097312a8c..563d5cb01 100644 --- a/primer-service/src/Primer/Servant/API.hs +++ b/primer-service/src/Primer/Servant/API.hs @@ -12,6 +12,8 @@ import Foreword import Primer.App ( App, + EvalBoundedInterpReq (..), + EvalBoundedInterpResp (..), EvalFullReq (..), EvalFullResp (..), EvalReq (..), @@ -152,6 +154,12 @@ data SessionAPI mode = SessionAPI :> Summary "Evaluate the given expression to normal form (or time out)" :> ReqBody '[JSON] EvalFullReq :> Post '[JSON] (Either ProgError EvalFullResp) + , evalBoundedInterp :: + mode + :- "eval-bounded-interp" + :> Summary "Using the interpreter, evaluate the given expression to normal form (or time out)" + :> ReqBody '[JSON] EvalBoundedInterpReq + :> Post '[JSON] (Either ProgError EvalBoundedInterpResp) } deriving stock (Generic) diff --git a/primer-service/src/Primer/Servant/OpenAPI.hs b/primer-service/src/Primer/Servant/OpenAPI.hs index e75b4b9b2..996992777 100644 --- a/primer-service/src/Primer/Servant/OpenAPI.hs +++ b/primer-service/src/Primer/Servant/OpenAPI.hs @@ -16,7 +16,14 @@ module Primer.Servant.OpenAPI ( import Foreword import Data.OpenApi (OpenApi, ToSchema) -import Primer.API (ApplyActionBody, EvalFullResp, Prog, Selection, TypeOrKind) +import Primer.API ( + ApplyActionBody, + EvalBoundedInterpResp, + EvalFullResp, + Prog, + Selection, + TypeOrKind, + ) import Primer.Action.Available qualified as Available import Primer.App (Level) import Primer.Core (GVarName, ModuleName) @@ -88,6 +95,10 @@ data SessionsAPI mode = SessionsAPI -- | A static bound on the maximum requested timeout for evaluation endpoint type EvalFullStepLimit = 300 +-- | A static bound on the maximum requested timeout (in microseconds) +-- for evaluation via the interpreter. +type EvalBoundedInterpLimit = 100_000 -- 100ms + -- | The session-specific bits of the API. data SessionAPI mode = SessionAPI { deleteSession :: DeleteSession mode @@ -128,6 +139,14 @@ data SessionAPI mode = SessionAPI :> QueryParam "closed" NormalOrderOptions :> ReqBody '[JSON] GVarName :> Post '[JSON] EvalFullResp + , evalBoundedInterp :: + mode + :- "eval-bounded-interp" + :> Summary "Using the interpreter, evaluate the named definition to normal form (or time out)" + :> OperationId "eval-bounded-interp" + :> QueryParam "timeoutMicroseconds" (Finite 0 EvalBoundedInterpLimit) + :> ReqBody '[JSON] GVarName + :> Post '[JSON] EvalBoundedInterpResp , undo :: mode :- "undo" diff --git a/primer-service/src/Primer/Server.hs b/primer-service/src/Primer/Server.hs index 7e2578915..f4c2859ff 100644 --- a/primer-service/src/Primer/Server.hs +++ b/primer-service/src/Primer/Server.hs @@ -28,6 +28,9 @@ import Control.Monad.Log (LoggingT, WithSeverity, runLoggingT) import Control.Monad.Log qualified as Log import Data.HashMap.Strict.InsOrd qualified as IOHM import Data.OpenApi (OpenApi, Reference (Reference), Referenced (Inline, Ref), ToSchema, toSchema) +import Data.Semiring ( + fromNatural, + ) import Data.Streaming.Network.Internal (HostPreference (HostIPv4Only)) import Data.Text qualified as T import Data.Text.Lazy qualified as LT (fromStrict) @@ -68,6 +71,7 @@ import Primer.API ( createDefinition, createTypeDef, edit, + evalBoundedInterp', evalFull', findSessions, listSessions, @@ -90,6 +94,9 @@ import Primer.Database qualified as Database ( Op, ) import Primer.Eval (EvalLog) +import Primer.EvalFullInterp ( + Timeout (MicroSec), + ) import Primer.Finite (getFinite) import Primer.Log (ConvertLogMessage, logInfo, logWarning) import Primer.Name (unsafeMkName) @@ -198,6 +205,7 @@ openAPISessionServer sid = , OpenAPI.typeDef = openAPITypeDefServer sid , OpenAPI.actions = openAPIActionServer sid , OpenAPI.evalFull = evalFull' sid . fmap getFinite + , OpenAPI.evalBoundedInterp = evalBoundedInterp' sid . fmap (MicroSec . fromNatural . getFinite) , OpenAPI.undo = undo sid , OpenAPI.redo = redo sid } @@ -254,6 +262,7 @@ sessionAPIServer sid = , S.questionAPI = questionAPIServer sid , S.evalStep = API.evalStep sid , S.evalFull = API.evalFull sid + , S.evalBoundedInterp = API.evalBoundedInterp sid } questionAPIServer :: ConvertServerLogs l => SessionId -> S.QuestionAPI (AsServerT (Primer l)) diff --git a/primer-service/test/Tests/OpenAPI.hs b/primer-service/test/Tests/OpenAPI.hs index dd0190e60..71c0efa00 100644 --- a/primer-service/test/Tests/OpenAPI.hs +++ b/primer-service/test/Tests/OpenAPI.hs @@ -26,6 +26,7 @@ import Hedgehog.Range qualified as R import Primer.API ( ApplyActionBody (..), Def (Def), + EvalBoundedInterpResp (..), EvalFullResp (EvalFullRespNormal, EvalFullRespTimedOut), Module (Module), NewSessionReq (..), @@ -333,6 +334,16 @@ tasty_PaginatedMeta = testToJSON genPaginatedMeta genPaginatedSession :: Gen (Paginated Session) genPaginatedSession = Paginated <$> genPaginatedMeta <*> G.list (R.linear 0 10) genSession +genEvalBoundedInterpResp :: ExprGen EvalBoundedInterpResp +genEvalBoundedInterpResp = + G.choice + [ pure EvalBoundedInterpRespTimeout + , pure EvalBoundedInterpRespNoBranch + , EvalBoundedInterpRespUnknownTyCon <$> genTyConName + , EvalBoundedInterpRespUnknownValCon <$> genValConName + , EvalBoundedInterpRespNormal <$> genExprTree + ] + tasty_Paginated :: Property tasty_Paginated = testToJSON genPaginatedSession @@ -383,6 +394,8 @@ instance Arbitrary GVarName where arbitrary = hedgehog genGVarName instance Arbitrary EvalFullResp where arbitrary = elements [EvalFullRespNormal, EvalFullRespTimedOut] <*> hedgehog (evalExprGen 0 genExprTree) +instance Arbitrary EvalBoundedInterpResp where + arbitrary = hedgehog $ evalExprGen 0 genEvalBoundedInterpResp instance Arbitrary CreateTypeDefBody where arbitrary = CreateTypeDefBody <$> arbitrary <*> arbitrary <*> arbitrary instance Arbitrary NewSessionReq where diff --git a/primer-service/test/outputs/OpenAPI/openapi.json b/primer-service/test/outputs/OpenAPI/openapi.json index 1ced3c85a..c492ddf7b 100644 --- a/primer-service/test/outputs/OpenAPI/openapi.json +++ b/primer-service/test/outputs/OpenAPI/openapi.json @@ -138,6 +138,97 @@ ], "type": "string" }, + "EvalBoundedInterpResp": { + "oneOf": [ + { + "properties": { + "tag": { + "enum": [ + "EvalBoundedInterpRespTimeout" + ], + "type": "string" + } + }, + "required": [ + "tag" + ], + "title": "EvalBoundedInterpRespTimeout", + "type": "object" + }, + { + "properties": { + "tag": { + "enum": [ + "EvalBoundedInterpRespNoBranch" + ], + "type": "string" + } + }, + "required": [ + "tag" + ], + "title": "EvalBoundedInterpRespNoBranch", + "type": "object" + }, + { + "properties": { + "contents": { + "$ref": "#/components/schemas/GlobalName" + }, + "tag": { + "enum": [ + "EvalBoundedInterpRespUnknownTyCon" + ], + "type": "string" + } + }, + "required": [ + "tag", + "contents" + ], + "title": "EvalBoundedInterpRespUnknownTyCon", + "type": "object" + }, + { + "properties": { + "contents": { + "$ref": "#/components/schemas/GlobalName" + }, + "tag": { + "enum": [ + "EvalBoundedInterpRespUnknownValCon" + ], + "type": "string" + } + }, + "required": [ + "tag", + "contents" + ], + "title": "EvalBoundedInterpRespUnknownValCon", + "type": "object" + }, + { + "properties": { + "contents": { + "$ref": "#/components/schemas/Tree" + }, + "tag": { + "enum": [ + "EvalBoundedInterpRespNormal" + ], + "type": "string" + } + }, + "required": [ + "tag", + "contents" + ], + "title": "EvalBoundedInterpRespNormal", + "type": "object" + } + ] + }, "EvalFullResp": { "oneOf": [ { @@ -1649,6 +1740,63 @@ "summary": "Evaluate the named definition to normal form (or time out)" } }, + "/openapi/sessions/{sessionId}/eval-bounded-interp": { + "post": { + "operationId": "eval-bounded-interp", + "parameters": [ + { + "description": "The session ID", + "in": "path", + "name": "sessionId", + "required": true, + "schema": { + "format": "uuid", + "type": "string" + } + }, + { + "in": "query", + "name": "timeoutMicroseconds", + "required": false, + "schema": { + "exclusiveMaximum": false, + "exclusiveMinimum": false, + "maximum": 100000, + "minimum": 0, + "type": "integer" + } + } + ], + "requestBody": { + "content": { + "application/json;charset=utf-8": { + "schema": { + "$ref": "#/components/schemas/GlobalName" + } + } + } + }, + "responses": { + "200": { + "content": { + "application/json;charset=utf-8": { + "schema": { + "$ref": "#/components/schemas/EvalBoundedInterpResp" + } + } + }, + "description": "" + }, + "400": { + "description": "Invalid `body` or `timeoutMicroseconds`" + }, + "404": { + "description": "`sessionId` not found" + } + }, + "summary": "Using the interpreter, evaluate the named definition to normal form (or time out)" + } + }, "/openapi/sessions/{sessionId}/name": { "get": { "operationId": "getSessionName", From b2031c779d6973e0d2d24cb064448fc9fb2b4d92 Mon Sep 17 00:00:00 2001 From: Drew Hess Date: Sat, 20 Apr 2024 21:21:00 +0100 Subject: [PATCH 5/6] chore: add tests for evaluating top-level definitions Note that all of these tests that use the interpreter are currently expected to fail (or are commented out because they will fail) due to https://github.com/hackworthltd/primer/issues/1247 Signed-off-by: Drew Hess --- primer-api/primer-api.cabal | 1 + primer-api/test/Tests/API.hs | 309 +++++++++++++++++++++++++++- primer/src/Primer/App.hs | 2 + primer/src/Primer/Examples.hs | 7 + primer/test/Tests/EvalFullInterp.hs | 190 +++++++++++++++-- primer/test/Tests/EvalFullStep.hs | 118 ++++++++++- 6 files changed, 601 insertions(+), 26 deletions(-) diff --git a/primer-api/primer-api.cabal b/primer-api/primer-api.cabal index 3c2f4fb81..190768d7b 100644 --- a/primer-api/primer-api.cabal +++ b/primer-api/primer-api.cabal @@ -156,6 +156,7 @@ test-suite primer-api-test , stm-containers , tasty ^>=1.5 , tasty-discover + , tasty-expected-failure ^>=0.12.3 , tasty-golden ^>=2.3.5 , tasty-hunit , text diff --git a/primer-api/test/Tests/API.hs b/primer-api/test/Tests/API.hs index c6b0c3c43..212495c95 100644 --- a/primer-api/test/Tests/API.hs +++ b/primer-api/test/Tests/API.hs @@ -9,6 +9,9 @@ import Data.Text.Lazy qualified as TL import Hedgehog hiding (Property, Var, property) import Optics ((.~)) import Primer.API ( + EvalBoundedInterpResp (..), + EvalFullResp (..), + EvalInterpResp (..), NewSessionReq (..), OkOrMismatch (Mismatch, Ok, expected, got), PrimerErr, @@ -18,8 +21,12 @@ import Primer.API ( copySession, deleteSession, edit, + evalBoundedInterp, evalBoundedInterp', + evalFull, evalFull', + evalInterp, + evalInterp', findSessions, flushSessions, getApp, @@ -61,7 +68,18 @@ import Primer.App ( Selection' (SelectionDef), newApp, ) -import Primer.Builtins (cTrue, cZero, tBool, tList, tMaybe, tNat) +import Primer.App qualified as App +import Primer.Builtins ( + cCons, + cFalse, + cNil, + cTrue, + cZero, + tBool, + tList, + tMaybe, + tNat, + ) import Primer.Core import Primer.Core.DSL hiding (app) import Primer.Core.Utils (forgetMetadata, forgetTypeMetadata) @@ -73,13 +91,18 @@ import Primer.Database ( fromSessionName, ) import Primer.Def (astDefExpr, astDefType, defAST) -import Primer.Eval (NormalOrderOptions (UnderBinders)) +import Primer.Eval ( + Dir (Chk), + NormalOrderOptions (UnderBinders), + ) import Primer.EvalFullInterp ( Timeout (MicroSec), ) import Primer.Examples ( comprehensive, even3App, + mapOddApp, + mapOddPrimApp, ) import Primer.Gen.Core.Raw (evalExprGen, genExpr, genType) import Primer.Module (moduleDefsQualified) @@ -91,6 +114,7 @@ import Primer.Test.Util ( assertException, constructSaturatedCon, constructTCon, + gvn, (@?=), ) import Primer.UUIDv4 (nextRandom) @@ -100,6 +124,9 @@ import Tasty ( property, ) import Test.Tasty (TestTree, testGroup) +import Test.Tasty.ExpectedFailure ( + expectFailBecause, + ) import Test.Tasty.Golden (goldenVsString) import Test.Tasty.HUnit hiding ((@?=)) import Text.Pretty.Simple (pShowNoColor) @@ -483,6 +510,279 @@ test_renameSession_too_long = step "it should be truncated at 64 characters" name @?= toS (replicate 64 'a') +test_evalFull_even3 :: TestTree +test_evalFull_even3 = + testCaseSteps "evalFull even3" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the even3App to the session" + sid <- addSession "even3App" even3App + step "Eval even3" + let expr = create' $ gvar $ gvn ["Even3"] "even 3?" + resp <- evalFull sid (App.EvalFullReq expr Chk 1000 UnderBinders) + let expected = create' $ con0 cFalse + case resp of + Left e -> liftIO $ assertFailure $ "ProgError: " <> show e + Right (App.EvalFullRespTimedOut e) -> liftIO $ assertFailure $ "timed out: " <> show e + Right (App.EvalFullRespNormal e) -> forgetMetadata e @?= forgetMetadata expected + +test_evalFull_mapOdd :: TestTree +test_evalFull_mapOdd = + testCaseSteps "evalFull mapOdd" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the mapOddApp to the session" + sid <- addSession "mapOddApp" mapOddApp + step "Eval mapOdd" + let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd" + resp <- evalFull sid (App.EvalFullReq expr Chk 1000 UnderBinders) + let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + case resp of + Left e -> liftIO $ assertFailure $ "ProgError: " <> show e + Right (App.EvalFullRespTimedOut e) -> liftIO $ assertFailure $ "timed out: " <> show e + Right (App.EvalFullRespNormal e) -> forgetMetadata e @?= forgetMetadata expected + +test_evalFull_mapOddPrim :: TestTree +test_evalFull_mapOddPrim = + testCaseSteps "evalFull mapOddPrim" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the mapOddPrimApp to the session" + sid <- addSession "mapOddPrimApp" mapOddPrimApp + step "Eval mapOdd" + let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd" + resp <- evalFull sid (App.EvalFullReq expr Chk 1000 UnderBinders) + let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + case resp of + Left e -> liftIO $ assertFailure $ "ProgError: " <> show e + Right (App.EvalFullRespTimedOut e) -> liftIO $ assertFailure $ "timed out: " <> show e + Right (App.EvalFullRespNormal e) -> forgetMetadata e @?= forgetMetadata expected + +test_evalFull'_even3 :: TestTree +test_evalFull'_even3 = + testCaseSteps "evalFull' even3" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the even3App to the session" + sid <- addSession "even3App" even3App + step "Eval even3" + resp <- evalFull' sid (Just 1000) (Just UnderBinders) $ gvn ["Even3"] "even 3?" + let expected = viewTreeExpr $ create' $ con0 cFalse + case resp of + EvalFullRespTimedOut e -> liftIO $ assertFailure $ "timed out: " <> show e + EvalFullRespNormal e -> zTIds e @?= zTIds expected + +test_evalFull'_mapOdd :: TestTree +test_evalFull'_mapOdd = + testCaseSteps "evalFull' mapOdd" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the mapOddApp to the session" + sid <- addSession "mapOddApp" mapOddApp + step "Eval mapOdd" + resp <- evalFull' sid (Just 1000) (Just UnderBinders) $ gvn ["MapOdd"] "mapOdd" + let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + case resp of + EvalFullRespTimedOut e -> liftIO $ assertFailure $ "timed out: " <> show e + EvalFullRespNormal e -> zTIds e @?= zTIds expected + +test_evalFull'_mapOddPrim :: TestTree +test_evalFull'_mapOddPrim = + testCaseSteps "evalFull' mapOddPrim" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the mapOddPrimApp to the session" + sid <- addSession "mapOddPrimApp" mapOddPrimApp + step "Eval mapOdd" + resp <- evalFull' sid (Just 1000) (Just UnderBinders) $ gvn ["MapOdd"] "mapOdd" + let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + case resp of + EvalFullRespTimedOut e -> liftIO $ assertFailure $ "timed out: " <> show e + EvalFullRespNormal e -> zTIds e @?= zTIds expected + +-- https://github.com/hackworthltd/primer/issues/1247 +test_evalInterp_even3 :: TestTree +test_evalInterp_even3 = expectFailBecause "interpreter can't reduce top-level definitions" $ do + testCaseSteps "evalInterp even3" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the even3App to the session" + sid <- addSession "even3App" even3App + step "Eval even3" + let expr = create' $ gvar $ gvn ["Even3"] "even 3?" + resp <- evalInterp sid $ App.EvalInterpReq expr Chk + let expected = create' $ con0 cFalse + case resp of + Left e -> liftIO $ assertFailure $ "ProgError: " <> show e + Right (App.EvalInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected + +-- https://github.com/hackworthltd/primer/issues/1247 +test_evalInterp_mapOdd :: TestTree +test_evalInterp_mapOdd = expectFailBecause "interpreter can't reduce top-level definitions" $ do + testCaseSteps "evalInterp mapOdd" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the mapOddApp to the session" + sid <- addSession "mapOddApp" mapOddApp + step "Eval mapOdd" + let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd" + resp <- evalInterp sid $ App.EvalInterpReq expr Chk + let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + case resp of + Left e -> liftIO $ assertFailure $ "ProgError: " <> show e + Right (App.EvalInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected + +-- https://github.com/hackworthltd/primer/issues/1247 +test_evalInterp_mapOddPrim :: TestTree +test_evalInterp_mapOddPrim = expectFailBecause "interpreter can't reduce top-level definitions" $ do + testCaseSteps "evalInterp mapOddPrim" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the mapOddPrimApp to the session" + sid <- addSession "mapOddPrimApp" mapOddPrimApp + step "Eval mapOdd" + let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd" + resp <- evalInterp sid $ App.EvalInterpReq expr Chk + let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + case resp of + Left e -> liftIO $ assertFailure $ "ProgError: " <> show e + Right (App.EvalInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected + +-- https://github.com/hackworthltd/primer/issues/1247 +test_evalInterp'_even3 :: TestTree +test_evalInterp'_even3 = expectFailBecause "interpreter can't reduce top-level definitions" $ do + testCaseSteps "evalInterp' even3" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the even3App to the session" + sid <- addSession "even3App" even3App + step "Eval even3" + (EvalInterpRespNormal e) <- evalInterp' sid $ gvn ["Even3"] "even 3?" + let expected = viewTreeExpr $ create' $ con0 cFalse + zTIds e @?= zTIds expected + +-- https://github.com/hackworthltd/primer/issues/1247 +test_evalInterp'_mapOdd :: TestTree +test_evalInterp'_mapOdd = expectFailBecause "interpreter can't reduce top-level definitions" $ do + testCaseSteps "evalInterp' mapOdd" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the mapOddApp to the session" + sid <- addSession "mapOddApp" mapOddApp + step "Eval mapOdd" + (EvalInterpRespNormal e) <- evalInterp' sid $ gvn ["MapOdd"] "mapOdd" + let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + zTIds e @?= zTIds expected + +-- https://github.com/hackworthltd/primer/issues/1247 +test_evalInterp'_mapOddPrim :: TestTree +test_evalInterp'_mapOddPrim = expectFailBecause "interpreter can't reduce top-level definitions" $ do + testCaseSteps "evalInterp' mapOddPrim" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the mapOddPrimApp to the session" + sid <- addSession "mapOddPrimApp" mapOddPrimApp + step "Eval mapOdd" + (EvalInterpRespNormal e) <- evalInterp' sid $ gvn ["MapOdd"] "mapOdd" + let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + zTIds e @?= zTIds expected + +-- https://github.com/hackworthltd/primer/issues/1247 +test_evalBoundedInterp_even3 :: TestTree +test_evalBoundedInterp_even3 = expectFailBecause "interpreter can't reduce top-level definitions" $ do + testCaseSteps "evalBoundedInterp even3" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the even3App to the session" + sid <- addSession "even3App" even3App + step "Eval even3" + let expr = create' $ gvar $ gvn ["Even3"] "even 3?" + resp <- evalBoundedInterp sid (App.EvalBoundedInterpReq expr Chk $ MicroSec 10_000) + let expected = create' $ con0 cFalse + case resp of + Left err -> liftIO $ assertFailure $ "ProgError: " <> show err + Right (App.EvalBoundedInterpRespFailed err) -> liftIO $ assertFailure $ "InterpError: " <> show err + Right (App.EvalBoundedInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected + +-- https://github.com/hackworthltd/primer/issues/1247 +test_evalBoundedInterp_mapOdd :: TestTree +test_evalBoundedInterp_mapOdd = expectFailBecause "interpreter can't reduce top-level definitions" $ do + testCaseSteps "evalBoundedInterp mapOdd" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the mapOddApp to the session" + sid <- addSession "mapOddApp" mapOddApp + step "Eval mapOdd" + let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd" + resp <- evalBoundedInterp sid (App.EvalBoundedInterpReq expr Chk $ MicroSec 10_000) + let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + case resp of + Left err -> liftIO $ assertFailure $ "ProgError: " <> show err + Right (App.EvalBoundedInterpRespFailed err) -> liftIO $ assertFailure $ "InterpError: " <> show err + Right (App.EvalBoundedInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected + +-- https://github.com/hackworthltd/primer/issues/1247 +test_evalBoundedInterp_mapOddPrim :: TestTree +test_evalBoundedInterp_mapOddPrim = expectFailBecause "interpreter can't reduce top-level definitions" $ do + testCaseSteps "evalBoundedInterp mapOddPrim" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the mapOddPrimApp to the session" + sid <- addSession "mapOddPrimApp" mapOddPrimApp + step "Eval mapOdd" + let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd" + resp <- evalBoundedInterp sid (App.EvalBoundedInterpReq expr Chk $ MicroSec 10_000) + let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + case resp of + Left err -> liftIO $ assertFailure $ "ProgError: " <> show err + Right (App.EvalBoundedInterpRespFailed err) -> liftIO $ assertFailure $ "InterpError: " <> show err + Right (App.EvalBoundedInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected + +-- https://github.com/hackworthltd/primer/issues/1247 +test_evalBoundedInterp'_even3 :: TestTree +test_evalBoundedInterp'_even3 = expectFailBecause "interpreter can't reduce top-level definitions" $ do + testCaseSteps "evalBoundedInterp' even3" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the even3App to the session" + sid <- addSession "even3App" even3App + step "Eval even3" + resp <- evalBoundedInterp' sid (Just $ MicroSec 10_000) $ gvn ["Even3"] "even 3?" + let expected = viewTreeExpr $ create' $ con0 cFalse + case resp of + EvalBoundedInterpRespNormal e -> zTIds e @?= zTIds expected + e -> liftIO $ assertFailure $ show e + +-- https://github.com/hackworthltd/primer/issues/1247 +test_evalBoundedInterp'_mapOdd :: TestTree +test_evalBoundedInterp'_mapOdd = expectFailBecause "interpreter can't reduce top-level definitions" $ do + testCaseSteps "evalBoundedInterp' mapOdd" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the mapOddApp to the session" + sid <- addSession "mapOddApp" mapOddApp + step "Eval mapOdd" + resp <- evalBoundedInterp' sid (Just $ MicroSec 10_000) $ gvn ["MapOdd"] "mapOdd" + let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + case resp of + EvalBoundedInterpRespNormal e -> zTIds e @?= zTIds expected + e -> liftIO $ assertFailure $ show e + +-- https://github.com/hackworthltd/primer/issues/1247 +test_evalBoundedInterp'_mapOddPrim :: TestTree +test_evalBoundedInterp'_mapOddPrim = expectFailBecause "interpreter can't reduce top-level definitions" $ do + testCaseSteps "evalBoundedInterp' mapOddPrim" $ \step' -> do + runAPI $ do + let step = liftIO . step' + step "Add the mapOddPrimApp to the session" + sid <- addSession "mapOddPrimApp" mapOddPrimApp + step "Eval mapOdd" + resp <- evalBoundedInterp' sid (Just $ MicroSec 10_000) $ gvn ["MapOdd"] "mapOdd" + let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + case resp of + EvalBoundedInterpRespNormal e -> zTIds e @?= zTIds expected + e -> liftIO $ assertFailure $ show e + test_eval_undo :: TestTree test_eval_undo = testCaseSteps "eval plays nicely with undo/redo" $ \step' -> do @@ -740,6 +1040,9 @@ test_selectioninfo = } ) +zTIds :: Tree -> Tree +zTIds = treeIds .~ "0" + zeroTKIds :: TypeOrKind -> TypeOrKind zeroTKIds = \case Type om -> Type $ zOMIds om @@ -749,5 +1052,3 @@ zeroTKIds = \case zOMIds = \case Ok t -> Ok $ zTIds t Mismatch t1 t2 -> Mismatch (zTIds t1) (zTIds t2) - zTIds :: Tree -> Tree - zTIds = treeIds .~ "0" diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 5e281b14b..6d1df4411 100644 --- 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/src/Primer/Examples.hs b/primer/src/Primer/Examples.hs index 57515df10..be4ff1878 100644 --- a/primer/src/Primer/Examples.hs +++ b/primer/src/Primer/Examples.hs @@ -40,6 +40,7 @@ module Primer.Examples ( -- * Toy 'App's. even3App, mapOddApp, + mapOddPrimApp, ) where import Foreword hiding ( @@ -544,3 +545,9 @@ mapOddApp :: App mapOddApp = let (p, id_, nc) = mapOddProg 4 in mkApp id_ nc p + +-- | An 'App' containing 'mapOddPrimProg'. +mapOddPrimApp :: App +mapOddPrimApp = + let (p, id_, nc) = mapOddPrimProg 4 + in mkApp id_ nc p diff --git a/primer/test/Tests/EvalFullInterp.hs b/primer/test/Tests/EvalFullInterp.hs index ab5bdcd9c..bbb614f60 100644 --- a/primer/test/Tests/EvalFullInterp.hs +++ b/primer/test/Tests/EvalFullInterp.hs @@ -895,9 +895,44 @@ unit_prim_partial_map = s <- evalFullTest builtinTypes (gs <> prims) Syn e s @?= Right r +-- https://github.com/hackworthltd/primer/issues/1247 + +-- 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 + +-- unit_interp_mapOdd2 :: Assertion +-- unit_interp_mapOdd2 = +-- let (prog, _, _) = mapOddProg 2 +-- types = allTypes prog +-- defs = allDefs prog +-- expr = create1 $ gvar $ gvn ["MapOdd"] "mapOdd" +-- expect = create1 $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]] +-- in do +-- s <- evalFullTest types defs Chk expr +-- s @?= Right expect + +-- unit_interp_mapOddPrim2 :: Assertion +-- unit_interp_mapOddPrim2 = +-- let (prog, _, _) = mapOddPrimProg 2 +-- types = allTypes prog +-- defs = allDefs prog +-- expr = create1 $ gvar $ gvn ["MapOdd"] "mapOdd" +-- expect = create1 $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]] +-- 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 = +unit_handleEvalInterpRequest_modules :: Assertion +unit_handleEvalInterpRequest_modules = let test = do builtinModule' <- builtinModule primitiveModule' <- primitiveModule @@ -918,8 +953,8 @@ unit_eval_interp_full_modules = Right assertion -> assertion -- Test that 'handleEvalBoundedInterpRequest' will reduce imported terms -unit_eval_interp_full_modules_bounded :: Assertion -unit_eval_interp_full_modules_bounded = +unit_handleEvalBoundedInterpRequest_modules :: Assertion +unit_handleEvalBoundedInterpRequest_modules = let test = do builtinModule' <- builtinModule primitiveModule' <- primitiveModule @@ -942,10 +977,65 @@ unit_eval_interp_full_modules_bounded = Left err -> assertFailure $ show err Right assertion -> assertion +-- https://github.com/hackworthltd/primer/issues/1247 + +-- 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 + +-- unit_handleEvalInterpRequest_mapOdd :: Assertion +-- unit_handleEvalInterpRequest_mapOdd = +-- let test = do +-- expr <- gvar $ gvn ["MapOdd"] "mapOdd" +-- (EvalInterpRespNormal e) <- +-- readerToState +-- $ handleEvalInterpRequest +-- $ EvalInterpReq +-- { expr = expr +-- , dir = Chk +-- } +-- -- Note that the 'mapOddApp' includes a program runs @mapOdd@ over a list of [0..3] +-- expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] +-- pure $ e ~= expect +-- in runAppTestM mapOddApp test <&> fst >>= \case +-- Left err -> assertFailure $ show err +-- Right assertion -> assertion + +-- unit_handleEvalInterpRequest_mapOddPrim :: Assertion +-- unit_handleEvalInterpRequest_mapOddPrim = +-- let test = do +-- expr <- gvar $ gvn ["MapOdd"] "mapOdd" +-- (EvalInterpRespNormal e) <- +-- readerToState +-- $ handleEvalInterpRequest +-- $ EvalInterpReq +-- { expr = expr +-- , dir = Chk +-- } +-- -- Note that the 'mapOddPrimApp' includes a program runs @mapOdd@ over a list of [0..3] +-- expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] +-- pure $ e ~= expect +-- in runAppTestM mapOddPrimApp 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 -unit_eval_interp_full_modules_scrutinize_imported_type = +unit_handleEvalInterpRequest_modules_scrutinize_imported_type :: Assertion +unit_handleEvalInterpRequest_modules_scrutinize_imported_type = let test = do m' <- m importModules [m'] @@ -978,8 +1068,8 @@ unit_eval_interp_full_modules_scrutinize_imported_type = -- Test that 'handleEvalBoundedInterpRequest' will reduce case analysis -- of imported types -unit_eval_interp_full_modules_scrutinize_imported_type_bounded :: Assertion -unit_eval_interp_full_modules_scrutinize_imported_type_bounded = +unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type :: Assertion +unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type = let test = do m' <- m importModules [m'] @@ -1013,9 +1103,73 @@ unit_eval_interp_full_modules_scrutinize_imported_type_bounded = , moduleDefs = mempty } +-- https://github.com/hackworthltd/primer/issues/1247 + +-- 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 + +-- unit_handleEvalBoundedInterpRequest_mapOdd :: Assertion +-- unit_handleEvalBoundedInterpRequest_mapOdd = +-- let test = do +-- expr <- gvar $ gvn ["MapOdd"] "mapOdd" +-- resp <- +-- readerToState +-- $ handleEvalBoundedInterpRequest +-- $ EvalBoundedInterpReq +-- { expr = expr +-- , dir = Chk +-- , timeout = MicroSec 10_000 +-- } +-- -- Note that the 'mapOddApp' includes a program runs @mapOdd@ over a list of [0..3] +-- expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] +-- pure $ case resp of +-- EvalBoundedInterpRespFailed err -> assertFailure $ show err +-- EvalBoundedInterpRespNormal e -> e ~= expect +-- in runAppTestM mapOddApp test <&> fst >>= \case +-- Left err -> assertFailure $ show err +-- Right assertion -> assertion + +-- unit_handleEvalBoundedInterpRequest_mapOddPrim :: Assertion +-- unit_handleEvalBoundedInterpRequest_mapOddPrim = +-- let test = do +-- expr <- gvar $ gvn ["MapOdd"] "mapOdd" +-- resp <- +-- readerToState +-- $ handleEvalBoundedInterpRequest +-- $ EvalBoundedInterpReq +-- { expr = expr +-- , dir = Chk +-- , timeout = MicroSec 10_000 +-- } +-- -- Note that the 'mapOddPrimApp' includes a program runs @mapOdd@ over a list of [0..3] +-- expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] +-- pure $ case resp of +-- EvalBoundedInterpRespFailed err -> assertFailure $ show err +-- EvalBoundedInterpRespNormal e -> e ~= expect +-- in runAppTestM mapOddPrimApp 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 = +unit_handleEvalBoundedInterpRequest_timeout :: Assertion +unit_handleEvalBoundedInterpRequest_timeout = let test = do m' <- m importModules [m'] @@ -1047,8 +1201,8 @@ unit_eval_interp_handle_eval_bounded_timeout = -- Test that 'handleEvalBoundedInterpRequest' will return an error -- when a case branch is missing. -unit_eval_interp_handle_eval_bounded_missing_branch :: Assertion -unit_eval_interp_handle_eval_bounded_missing_branch = +unit_handleEvalBoundedInterpRequest_missing_branch :: Assertion +unit_handleEvalBoundedInterpRequest_missing_branch = let test = do m' <- m importModules [m'] @@ -1081,8 +1235,8 @@ unit_eval_interp_handle_eval_bounded_missing_branch = -- Test that 'handleEvalInterpRequest' will throw an 'InterpError' -- exception when a case branch is missing. -unit_eval_interp_handle_eval_missing_branch :: Assertion -unit_eval_interp_handle_eval_missing_branch = +unit_handleEvalInterpRequest_missing_branch :: Assertion +unit_handleEvalInterpRequest_missing_branch = let test = do m' <- m importModules [m'] @@ -1111,8 +1265,8 @@ unit_eval_interp_handle_eval_missing_branch = -- Test that 'handleEvalBoundedInterpRequest' will return an error -- when a case branch is missing (primitive version). -unit_eval_interp_handle_eval_bounded_missing_branch_prim :: Assertion -unit_eval_interp_handle_eval_bounded_missing_branch_prim = +unit_handleEvalBoundedInterpRequest_missing_branch_prim :: Assertion +unit_handleEvalBoundedInterpRequest_missing_branch_prim = let test = do m' <- m importModules [m'] @@ -1145,8 +1299,8 @@ unit_eval_interp_handle_eval_bounded_missing_branch_prim = -- Test that 'handleEvalInterpRequest' will throw an 'InterpError' -- exception when a case branch is missing (primitive version). -unit_eval_interp_handle_eval_missing_branch_prim :: Assertion -unit_eval_interp_handle_eval_missing_branch_prim = +unit_handleEvalInterpRequest_missing_branch_prim :: Assertion +unit_handleEvalInterpRequest_missing_branch_prim = let test = do m' <- m importModules [m'] diff --git a/primer/test/Tests/EvalFullStep.hs b/primer/test/Tests/EvalFullStep.hs index 251a3855e..839883324 100644 --- a/primer/test/Tests/EvalFullStep.hs +++ b/primer/test/Tests/EvalFullStep.hs @@ -16,6 +16,8 @@ import Optics import Primer.App ( EvalFullReq (EvalFullReq, evalFullCxtDir, evalFullMaxSteps, evalFullOptions, evalFullReqExpr), EvalFullResp (EvalFullRespNormal, EvalFullRespTimedOut), + allDefs, + allTypes, handleEvalFullRequest, importModules, newEmptyApp, @@ -26,6 +28,7 @@ import Primer.Builtins ( cFalse, cJust, cMakePair, + cNil, cNothing, cTrue, cZero, @@ -46,6 +49,14 @@ import Primer.Core.Utils ( import Primer.Def (DefMap) import Primer.Eval import Primer.EvalFullStep +import Primer.Examples ( + even3App, + even3Prog, + mapOddApp, + mapOddPrimApp, + mapOddPrimProg, + mapOddProg, + ) import Primer.Gen.Core.Typed (WT, forAllT, genChk, isolateWT, propertyWT) import Primer.Log (runPureLogT) import Primer.Module ( @@ -96,6 +107,7 @@ import Primer.Test.TestM ( import Primer.Test.Util ( assertNoSevereLogs, failWhenSevereLogs, + gvn, primDefs, testNoSevereLogs, zeroIDs, @@ -1681,9 +1693,42 @@ 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 + +unit_evalFull_mapOdd2 :: Assertion +unit_evalFull_mapOdd2 = + let (prog, maxID, _) = mapOddProg 2 + types = allTypes prog + defs = allDefs prog + (expr, _) = create $ gvar $ gvn ["MapOdd"] "mapOdd" + (expect, _) = create $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]] + in do + s <- evalFullTest maxID types defs 200 Chk expr + s <~==> Right expect + +unit_evalFull_mapOddPrim2 :: Assertion +unit_evalFull_mapOddPrim2 = + let (prog, maxID, _) = mapOddPrimProg 2 + types = allTypes prog + defs = allDefs prog + (expr, _) = create $ gvar $ gvn ["MapOdd"] "mapOdd" + (expect, _) = create $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]] + in do + s <- evalFullTest maxID types defs 200 Chk expr + s <~==> Right expect + -- Test that handleEvalFullRequest will reduce imported terms -unit_eval_full_modules :: Assertion -unit_eval_full_modules = +unit_handleEvalFullRequest_modules :: Assertion +unit_handleEvalFullRequest_modules = let test = do builtinModule' <- builtinModule primitiveModule' <- primitiveModule @@ -1708,8 +1753,8 @@ unit_eval_full_modules = Right assertion -> assertion -- Test that handleEvalFullRequest will reduce case analysis of imported types -unit_eval_full_modules_scrutinize_imported_type :: Assertion -unit_eval_full_modules_scrutinize_imported_type = +unit_handleEvalFullRequest_modules_scrutinize_imported_type :: Assertion +unit_handleEvalFullRequest_modules_scrutinize_imported_type = let test = do m' <- m importModules [m'] @@ -1744,6 +1789,71 @@ unit_eval_full_modules_scrutinize_imported_type = , moduleDefs = mempty } +unit_handleEvalFullRequest_even3 :: Assertion +unit_handleEvalFullRequest_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 + +unit_handleEvalFullRequest_mapOdd :: Assertion +unit_handleEvalFullRequest_mapOdd = + let test = do + expr <- gvar $ gvn ["MapOdd"] "mapOdd" + resp <- + readerToState + $ handleEvalFullRequest + $ EvalFullReq + { evalFullReqExpr = expr + , evalFullCxtDir = Chk + , evalFullMaxSteps = 400 + , evalFullOptions = UnderBinders + } + -- Note that the 'mapOddApp' includes a program runs @mapOdd@ over a list of [0..3] + expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + pure $ case resp of + EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" + EvalFullRespNormal e -> e ~= expect + in runAppTestM mapOddApp test <&> fst >>= \case + Left err -> assertFailure $ show err + Right assertion -> assertion + +unit_handleEvalFullRequest_mapOddPrim :: Assertion +unit_handleEvalFullRequest_mapOddPrim = + let test = do + expr <- gvar $ gvn ["MapOdd"] "mapOdd" + resp <- + readerToState + $ handleEvalFullRequest + $ EvalFullReq + { evalFullReqExpr = expr + , evalFullCxtDir = Chk + , evalFullMaxSteps = 300 + , evalFullOptions = UnderBinders + } + -- Note that the 'mapOddPrimApp' includes a program runs @mapOddPrim@ over a list of [0..3] + expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + pure $ case resp of + EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" + EvalFullRespNormal e -> e ~= expect + in runAppTestM mapOddPrimApp 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 From 1510ede6d2eae7bf1e383465fe99b41027a3959e Mon Sep 17 00:00:00 2001 From: Drew Hess Date: Tue, 23 Apr 2024 08:50:01 +0100 Subject: [PATCH 6/6] chore: bump bounded interp test timeout for Wasm The Wasm version of this test needs more time. Signed-off-by: Drew Hess --- primer/test/Tests/EvalFullInterp.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/primer/test/Tests/EvalFullInterp.hs b/primer/test/Tests/EvalFullInterp.hs index bbb614f60..e151a6a5f 100644 --- a/primer/test/Tests/EvalFullInterp.hs +++ b/primer/test/Tests/EvalFullInterp.hs @@ -1083,7 +1083,7 @@ unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type = $ EvalBoundedInterpReq { expr = foo , dir = Chk - , timeout = MicroSec 100 + , timeout = MicroSec 200 } expect <- con0 cFalse pure $ case resp of