From 0f7deba662d4f39dedd2beefe2ba751bfcbbada0 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 18 Jul 2023 15:53:04 +0100 Subject: [PATCH 1/4] refactor! make eval-under-binders an option with no alternatives This is a stepping-stone to making an option to not evaluate under binders for EvalFull. BREAKING CHANGE: This adds a new field to `EvalFullReq`, which is exposed in the APIs. Since it is an extra optional argument in the OpenAPI, old clients of the OpenAPI will still continue to work (this is not true of the richly-typed API). Signed-off-by: Ben Price --- primer-api/src/Primer/API.hs | 12 +++-- primer-api/test/Tests/API.hs | 3 +- primer-benchmark/src/Benchmarks.hs | 6 ++- primer-service/src/Primer/OpenAPI.hs | 6 +++ primer-service/src/Primer/Servant/OpenAPI.hs | 2 + .../test/outputs/OpenAPI/openapi.json | 13 ++++- primer/src/Primer/App.hs | 5 +- primer/src/Primer/Eval.hs | 9 ++++ primer/src/Primer/Eval/NormalOrder.hs | 47 +++++++++++++------ primer/src/Primer/EvalFull.hs | 36 ++++++++++---- primer/test/Tests/EvalFull.hs | 33 ++++++++----- primer/test/Tests/Prelude/Utils.hs | 6 ++- primer/test/Tests/Undo.hs | 3 +- 13 files changed, 135 insertions(+), 46 deletions(-) diff --git a/primer-api/src/Primer/API.hs b/primer-api/src/Primer/API.hs index 7d0b2f544..bbf27bef4 100644 --- a/primer-api/src/Primer/API.hs +++ b/primer-api/src/Primer/API.hs @@ -226,6 +226,7 @@ import Primer.Def ( defAST, ) import Primer.Def qualified as Def +import Primer.Eval (NormalOrderOptions (UnderBinders)) import Primer.Eval.Redex (Dir (Chk), EvalLog) import Primer.EvalFull (TerminationBound) import Primer.JSON ( @@ -412,7 +413,7 @@ data APILog | GenerateNames (ReqResp (SessionId, ((GVarName, ID), Either (Maybe (Type' ())) (Maybe (Kind' ())))) (Either ProgError [Name.Name])) | EvalStep (ReqResp (SessionId, EvalReq) (Either ProgError EvalResp)) | EvalFull (ReqResp (SessionId, EvalFullReq) (Either ProgError App.EvalFullResp)) - | EvalFull' (ReqResp (SessionId, Maybe TerminationBound, GVarName) EvalFullResp) + | EvalFull' (ReqResp (SessionId, Maybe TerminationBound, Maybe NormalOrderOptions, GVarName) EvalFullResp) | FlushSessions (ReqResp () ()) | CreateDef (ReqResp (SessionId, ModuleName, Maybe Text) Prog) | CreateTypeDef (ReqResp (SessionId, TyConName, [ValConName]) Prog) @@ -1117,16 +1118,18 @@ evalFull' :: (MonadIO m, MonadThrow m, MonadAPILog l m, ConvertLogMessage EvalLog l) => SessionId -> Maybe TerminationBound -> + Maybe NormalOrderOptions -> GVarName -> PrimerM m EvalFullResp -evalFull' = curry3 $ logAPI (noError EvalFull') $ \(sid, lim, d) -> - noErr <$> liftQueryAppM (q lim d) sid +evalFull' = curry4 $ logAPI (noError EvalFull') $ \(sid, lim, closed, d) -> + noErr <$> liftQueryAppM (q lim closed d) sid where q :: Maybe TerminationBound -> + Maybe NormalOrderOptions -> GVarName -> QueryAppM (PureLog (WithSeverity l)) Void EvalFullResp - q lim d = do + q lim closed 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 @@ -1139,6 +1142,7 @@ evalFull' = curry3 $ logAPI (noError EvalFull') $ \(sid, lim, d) -> { evalFullReqExpr = e , evalFullCxtDir = Chk , evalFullMaxSteps = fromMaybe 10 lim + , evalFullOptions = fromMaybe UnderBinders closed } pure $ case x of App.EvalFullRespTimedOut e' -> EvalFullRespTimedOut $ viewTreeExpr e' diff --git a/primer-api/test/Tests/API.hs b/primer-api/test/Tests/API.hs index 354f2a20a..6d178081a 100644 --- a/primer-api/test/Tests/API.hs +++ b/primer-api/test/Tests/API.hs @@ -48,6 +48,7 @@ import Primer.Database ( fromSessionName, ) import Primer.Def (astDefExpr, astDefType, defAST) +import Primer.Eval (NormalOrderOptions (UnderBinders)) import Primer.Examples ( comprehensive, even3App, @@ -462,7 +463,7 @@ test_eval_undo = sid <- newSession $ NewSessionReq "a new session" True let scope = mkSimpleModuleName "Main" step "eval" - void $ evalFull' sid (Just 100) $ qualifyName scope "main" + void $ evalFull' sid (Just 100) (Just UnderBinders) $ qualifyName scope "main" step "insert λ" let getMain = do p <- getProgram sid diff --git a/primer-benchmark/src/Benchmarks.hs b/primer-benchmark/src/Benchmarks.hs index d0b6100e0..e985342b3 100644 --- a/primer-benchmark/src/Benchmarks.hs +++ b/primer-benchmark/src/Benchmarks.hs @@ -21,6 +21,7 @@ import Primer.App ( ) import Primer.App.Utils (forgetProgTypecache) import Primer.Eval ( + NormalOrderOptions (UnderBinders), RunRedexOptions (RunRedexOptions, pushAndElide), ViewRedexOptions (ViewRedexOptions, aggressiveElision, groupedLets), ) @@ -102,16 +103,17 @@ benchmarks = ] ] where + evalOptionsN = UnderBinders evalOptionsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} evalOptionsR = RunRedexOptions{pushAndElide = True} evalTestMPureLogs e maxEvals = evalTestM (maxID e) $ runPureLogT $ - evalFull @EvalLog evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) + evalFull @EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) evalTestMDiscardLogs e maxEvals = evalTestM (maxID e) $ runDiscardLogT $ - evalFull @EvalLog evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) + evalFull @EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) benchExpected f g e n b = EnvBench e n $ \e' -> NF diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs index 75ec584e1..9717c7723 100644 --- a/primer-service/src/Primer/OpenAPI.hs +++ b/primer-service/src/Primer/OpenAPI.hs @@ -82,6 +82,7 @@ import Primer.Database ( Session, SessionName, ) +import Primer.Eval (NormalOrderOptions) import Primer.JSON (CustomJSON (CustomJSON), PrimerJSON) import Primer.Name (Name) import Servant.API (FromHttpApiData (parseQueryParam), ToHttpApiData (toQueryParam)) @@ -198,6 +199,11 @@ instance FromHttpApiData Level where parseQueryParam = parseQueryParamRead "level" instance ToHttpApiData Level where toQueryParam = show +deriving anyclass instance ToParamSchema NormalOrderOptions +instance FromHttpApiData NormalOrderOptions where + parseQueryParam = parseQueryParamRead "NormalOrderOptions" +instance ToHttpApiData NormalOrderOptions where + toQueryParam = show parseQueryParamRead :: Read a => Text -> Text -> Either Text a parseQueryParamRead m t = maybeToEither ("unknown " <> m <> ": " <> t) $ readMaybe t diff --git a/primer-service/src/Primer/Servant/OpenAPI.hs b/primer-service/src/Primer/Servant/OpenAPI.hs index 0e69348cd..e75b4b9b2 100644 --- a/primer-service/src/Primer/Servant/OpenAPI.hs +++ b/primer-service/src/Primer/Servant/OpenAPI.hs @@ -23,6 +23,7 @@ import Primer.Core (GVarName, ModuleName) import Primer.Database ( SessionId, ) +import Primer.Eval (NormalOrderOptions) import Primer.Finite (Finite) import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON) import Primer.OpenAPI () @@ -124,6 +125,7 @@ data SessionAPI mode = SessionAPI :> Summary "Evaluate the named definition to normal form (or time out)" :> OperationId "eval-full" :> QueryParam "stepLimit" (Finite 0 EvalFullStepLimit) + :> QueryParam "closed" NormalOrderOptions :> ReqBody '[JSON] GVarName :> Post '[JSON] EvalFullResp , undo :: diff --git a/primer-service/test/outputs/OpenAPI/openapi.json b/primer-service/test/outputs/OpenAPI/openapi.json index bfa6bc197..50cf4c2b4 100644 --- a/primer-service/test/outputs/OpenAPI/openapi.json +++ b/primer-service/test/outputs/OpenAPI/openapi.json @@ -1486,6 +1486,17 @@ "minimum": 0, "type": "integer" } + }, + { + "in": "query", + "name": "closed", + "required": false, + "schema": { + "enum": [ + "UnderBinders" + ], + "type": "string" + } } ], "requestBody": { @@ -1509,7 +1520,7 @@ "description": "" }, "400": { - "description": "Invalid `body` or `stepLimit`" + "description": "Invalid `body` or `closed` or `stepLimit`" }, "404": { "description": "`sessionId` not found" diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 14ceeb8e2..322bc5821 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -486,6 +486,7 @@ data EvalFullReq = EvalFullReq { evalFullReqExpr :: Expr , evalFullCxtDir :: Dir -- is this expression in a syn/chk context, so we can tell if is an embedding. , evalFullMaxSteps :: TerminationBound + , evalFullOptions :: Eval.NormalOrderOptions } deriving stock (Eq, Show, Read, Generic) deriving (FromJSON, ToJSON) via PrimerJSON EvalFullReq @@ -594,12 +595,12 @@ handleEvalFullRequest :: (MonadQueryApp m e, MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) => EvalFullReq -> m EvalFullResp -handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxSteps}) = do +handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxSteps, evalFullOptions}) = do app <- ask let prog = appProg app let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} let optsR = RunRedexOptions{pushAndElide = True} - result <- runFreshM app $ evalFull optsV optsR (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr + result <- runFreshM app $ evalFull evalFullOptions optsV optsR (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr pure $ case result of Left (TimedOut e) -> EvalFullRespTimedOut e Right nf -> EvalFullRespNormal nf diff --git a/primer/src/Primer/Eval.hs b/primer/src/Primer/Eval.hs index 23b0409c7..cc8612db5 100644 --- a/primer/src/Primer/Eval.hs +++ b/primer/src/Primer/Eval.hs @@ -7,6 +7,7 @@ module Primer.Eval ( redexes, RunRedexOptions (..), ViewRedexOptions (..), + NormalOrderOptions (..), EvalLog (..), EvalError (..), EvalDetail (..), @@ -57,6 +58,7 @@ import Primer.Eval.Detail ( import Primer.Eval.EvalError (EvalError (..)) import Primer.Eval.NormalOrder ( FMExpr (FMExpr, expr, ty), + NormalOrderOptions (..), foldMapExpr, singletonCxt, ) @@ -114,6 +116,7 @@ step tydefs globals expr d i = runExceptT $ do findNodeByID :: ID -> Dir -> Expr -> Maybe (Cxt, Either (Dir, ExprZ) TypeZ) findNodeByID i = foldMapExpr + UnderBinders FMExpr { expr = \ez d c -> if getID ez == i then Just (c, Left (d, ez)) else Nothing , ty = \tz c -> if getID tz == i then Just (c, Right tz) else Nothing @@ -132,6 +135,11 @@ evalOpts = -- We assume that the expression is well scoped. There are no -- guarantees about whether we will claim that an ill-sorted variable -- is inlinable, e.g. @lettype a = _ in case a of ...@. +-- +-- NB: we return /all/ redexes, even those under binders. We ignore any +-- `NormalOrderOptions`. This means that more redexes may be returned than an +-- EvalFull would actually reduce (depending on the NormalOrderOptions given to +-- EvalFull). redexes :: forall l m. (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) => @@ -143,6 +151,7 @@ redexes :: redexes tydefs globals = (ListT.toList .) . foldMapExpr + UnderBinders FMExpr { expr = \ez d -> liftMaybeT . runReaderT (getID ez <$ viewRedex evalOpts tydefs globals d (target ez)) , ty = \tz -> runReader (whenJust (getID tz) <$> viewRedexType evalOpts (target tz)) diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs index 1291fdb5d..e374be606 100644 --- a/primer/src/Primer/Eval/NormalOrder.hs +++ b/primer/src/Primer/Eval/NormalOrder.hs @@ -6,6 +6,7 @@ module Primer.Eval.NormalOrder ( findRedex, foldMapExpr, FMExpr (..), + NormalOrderOptions (..), -- Exported for testing singletonCxt, ) where @@ -43,6 +44,7 @@ import Primer.Eval.Redex ( viewRedex, viewRedexType, ) +import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON) import Primer.Log (ConvertLogMessage) import Primer.TypeDef ( TypeDefMap, @@ -81,7 +83,7 @@ data ViewLet = ViewLet -- ^ any non-body term children (i.e. rhs of the binding) } viewLet :: (Dir, ExprZ) -> Maybe ViewLet -viewLet dez@(_, ez) = case (target ez, exprChildren dez) of +viewLet dez@(_, ez) = case (target ez, exprChildren UnderBinders dez) of (Let _ x e _b, [ez', bz]) -> Just (ViewLet (LetBind x e) bz [] [ez']) (Letrec _ x e ty _b, [ez', bz]) -> Just (ViewLet (LetrecBind x e ty) bz tz [ez']) (LetType _ a ty _b, [bz]) -> bz `seq` Just (ViewLet (LetTyBind $ LetTypeBind a ty) bz tz []) @@ -90,6 +92,11 @@ viewLet dez@(_, ez) = case (target ez, exprChildren dez) of tz :: [TypeZ] tz = maybeToList $ focusType ez +data NormalOrderOptions + = UnderBinders + deriving stock (Eq, Show, Read, Generic) + deriving (FromJSON, ToJSON) via PrimerJSON NormalOrderOptions + -- | This is similar to 'foldMap', with a few differences: -- - 'Expr' is not foldable -- - We target every subexpression and also every (nested) subtype (e.g. in an annotation) @@ -107,8 +114,13 @@ viewLet dez@(_, ez) = case (target ez, exprChildren dez) of -- However, we may reduce type children to normal form more eagerly than necessary, -- both reducing type annotations more than needed, and reducing type applications when not needed. -- Since computation in types is strongly normalising, this will not cause us to fail to find any normal forms. -foldMapExpr :: forall f a. MonadPlus f => FMExpr (f a) -> Dir -> Expr -> f a -foldMapExpr extract topDir = go mempty . (topDir,) . focus +-- +-- We can optionally stop when we find a binder (e.g. to implement closed +-- evaluation -- do not compute under binders), although for consistency we +-- treat all case branches as being binders, even those that do not actually +-- bind a variable. +foldMapExpr :: forall f a. MonadPlus f => NormalOrderOptions -> FMExpr (f a) -> Dir -> Expr -> f a +foldMapExpr opts extract topDir = go mempty . (topDir,) . focus where go :: Cxt -> (Dir, ExprZ) -> f a go lets dez@(d, ez) = @@ -126,16 +138,16 @@ foldMapExpr extract topDir = go mempty . (topDir,) . focus -- Since this node is not a let, the context is reset _ -> msum $ - (goType mempty =<< focusType' ez) - : map (go mempty) (exprChildren dez) + (goType mempty =<< focusType' ez) -- NB: no binders in term scope over a type child + : map (go mempty) (exprChildren opts dez) goType :: Cxt -> TypeZ -> f a goType lets tz = extract.ty tz lets <|> case target tz of TLet _ a t _body -- Prefer to compute inside the body of a let, but otherwise compute in the binding - | [tz', bz] <- typeChildren tz -> goType (cxtAddLet (LetTyBind $ LetTypeBind a t) lets) bz <|> goType mempty tz' - _ -> msum $ map (goType mempty) $ typeChildren tz + | [tz', bz] <- typeChildren UnderBinders tz -> goType (cxtAddLet (LetTyBind $ LetTypeBind a t) lets) bz <|> goType mempty tz' + _ -> msum $ map (goType mempty) $ typeChildren opts tz data FMExpr m = FMExpr { expr :: ExprZ -> Dir -> Cxt -> m @@ -149,17 +161,19 @@ focusType' = maybe empty pure . focusType findRedex :: forall l m. (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) => + NormalOrderOptions -> ViewRedexOptions -> TypeDefMap -> DefMap -> Dir -> Expr -> MaybeT m RedexWithContext -findRedex opts tydefs globals = +findRedex optsN optsV tydefs globals = foldMapExpr + optsN ( FMExpr - { expr = \ez d -> runReaderT (RExpr ez <$> viewRedex opts tydefs globals d (target ez)) - , ty = \tz -> hoistMaybe . runReader (RType tz <<$>> viewRedexType opts (target tz)) + { expr = \ez d -> runReaderT (RExpr ez <$> viewRedex optsV tydefs globals d (target ez)) + , ty = \tz -> hoistMaybe . runReader (RType tz <<$>> viewRedexType optsV (target tz)) } ) @@ -168,8 +182,8 @@ children' z = case down z of Nothing -> mempty Just z' -> z' : unfoldr (fmap (\x -> (x, x)) . right) z' -exprChildren :: (Dir, ExprZ) -> [(Dir, ExprZ)] -exprChildren (d, ez) = +exprChildren' :: (Dir, ExprZ) -> [(Dir, ExprZ)] +exprChildren' (d, ez) = children' ez <&> \c -> do let d' = case target ez of App _ f _ | f == target c -> Syn @@ -188,8 +202,13 @@ exprChildren (d, ez) = _ -> Chk (d', c) -typeChildren :: TypeZ -> [TypeZ] -typeChildren = children' +exprChildren :: NormalOrderOptions -> (Dir, ExprZ) -> [(Dir, ExprZ)] +exprChildren = \case + UnderBinders -> exprChildren' + +typeChildren :: NormalOrderOptions -> TypeZ -> [TypeZ] +typeChildren = \case + UnderBinders -> children' singletonCxt :: LetBinding -> Cxt singletonCxt l = Cxt [l] diff --git a/primer/src/Primer/EvalFull.hs b/primer/src/Primer/EvalFull.hs index 5e9166e1b..fdc7fd7bc 100644 --- a/primer/src/Primer/EvalFull.hs +++ b/primer/src/Primer/EvalFull.hs @@ -22,7 +22,7 @@ import Primer.Core ( import Primer.Def ( DefMap, ) -import Primer.Eval.NormalOrder (RedexWithContext (RExpr, RType), findRedex) +import Primer.Eval.NormalOrder (NormalOrderOptions, RedexWithContext (RExpr, RType), findRedex) import Primer.Eval.Redex ( Dir (Chk, Syn), EvalLog (..), @@ -51,8 +51,18 @@ newtype EvalFullError type TerminationBound = Natural -- A naive implementation of normal-order reduction -evalFull :: MonadEval l m => ViewRedexOptions -> RunRedexOptions -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Either EvalFullError Expr) -evalFull optsV optsR tydefs env n d expr = snd <$> evalFullStepCount optsV optsR tydefs env n d expr +evalFull :: + MonadEval l m => + NormalOrderOptions -> + ViewRedexOptions -> + RunRedexOptions -> + TypeDefMap -> + DefMap -> + TerminationBound -> + Dir -> + Expr -> + m (Either EvalFullError Expr) +evalFull optsN optsV optsR tydefs env n d expr = snd <$> evalFullStepCount optsN optsV optsR tydefs env n d expr -- | As 'evalFull', but also returns how many reduction steps were taken. -- (This is mostly useful for testing purposes.) @@ -64,6 +74,7 @@ evalFull optsV optsR tydefs env n d expr = snd <$> evalFullStepCount optsV optsR -- more to notice termination. evalFullStepCount :: MonadEval l m => + NormalOrderOptions -> ViewRedexOptions -> RunRedexOptions -> TypeDefMap -> @@ -72,20 +83,29 @@ evalFullStepCount :: Dir -> Expr -> m (Natural, Either EvalFullError Expr) -evalFullStepCount optsV optsR tydefs env n d = go 0 +evalFullStepCount optsN optsV optsR tydefs env n d = go 0 where go s expr | s >= n = pure (s, Left $ TimedOut expr) | otherwise = - runMaybeT (step optsV optsR tydefs env d expr) >>= \case + runMaybeT (step optsN optsV optsR tydefs env d expr) >>= \case Nothing -> pure (s, Right expr) -- this is a normal form Just e -> go (s + 1) e -- The 'Dir' argument only affects what happens if the root is an annotation: -- do we keep it (Syn) or remove it (Chk). I.e. is an upsilon reduction allowed -- at the root? -step :: MonadEval l m => ViewRedexOptions -> RunRedexOptions -> TypeDefMap -> DefMap -> Dir -> Expr -> MaybeT m Expr -step optsV optsR tydefs g d e = - findRedex optsV tydefs g d e >>= \case +step :: + MonadEval l m => + NormalOrderOptions -> + ViewRedexOptions -> + RunRedexOptions -> + TypeDefMap -> + DefMap -> + Dir -> + Expr -> + MaybeT m Expr +step optsN optsV optsR tydefs g d e = + findRedex optsN optsV tydefs g d e >>= \case RExpr ez r -> lift $ unfocusExpr . flip replace ez . fst <$> runRedex optsR r RType et r -> lift $ unfocusExpr . unfocusType . flip replace et . fst <$> runRedexTy optsR r diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs index 03342b48e..46a52f9c0 100644 --- a/primer/test/Tests/EvalFull.hs +++ b/primer/test/Tests/EvalFull.hs @@ -14,7 +14,7 @@ import Hedgehog.Internal.Property (LabelName (unLabelName)) import Hedgehog.Range qualified as Range import Optics import Primer.App ( - EvalFullReq (EvalFullReq, evalFullCxtDir, evalFullMaxSteps, evalFullReqExpr), + EvalFullReq (EvalFullReq, evalFullCxtDir, evalFullMaxSteps, evalFullOptions, evalFullReqExpr), EvalFullResp (EvalFullRespNormal, EvalFullRespTimedOut), handleEvalFullRequest, importModules, @@ -588,6 +588,7 @@ resumeTest mods dir t = do let globs = foldMap' moduleDefsQualified mods tds <- asks typeDefs n <- forAllT $ Gen.integral $ Range.linear 2 1000 -- Arbitrary limit here + closed <- forAllT $ Gen.element @[] [UnderBinders] -- NB: We need to run this first reduction in an isolated context -- as we need to avoid it changing the fresh-name-generator state -- for the next run (sMid and sTotal). This is because reduction may need @@ -595,19 +596,19 @@ resumeTest mods dir t = do -- exactly the same as "reducing n steps and then further reducing m -- steps" (including generated names). (A happy consequence of this is that -- it is precisely the same including ids in metadata.) - ((stepsFinal', sFinal), logs) <- lift $ isolateWT $ runPureLogT $ evalFullStepCount @EvalLog optsV optsR tds globs n dir t + ((stepsFinal', sFinal), logs) <- lift $ isolateWT $ runPureLogT $ evalFullStepCount @EvalLog closed optsV optsR tds globs n dir t testNoSevereLogs logs when (stepsFinal' < 2) discard let stepsFinal = case sFinal of Left _ -> stepsFinal'; Right _ -> 1 + stepsFinal' m <- forAllT $ Gen.integral $ Range.constant 1 (stepsFinal - 1) - (stepsMid, sMid') <- failWhenSevereLogs $ evalFullStepCount @EvalLog optsV optsR tds globs m dir t + (stepsMid, sMid') <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed optsV optsR tds globs m dir t stepsMid === m sMid <- case sMid' of Left (TimedOut e) -> pure e -- This should never happen: we know we are not taking enough steps to -- hit a normal form (as m < stepsFinal) Right e -> assert False >> pure e - (stepsTotal, sTotal) <- failWhenSevereLogs $ evalFullStepCount @EvalLog optsV optsR tds globs (stepsFinal - m) dir sMid + (stepsTotal, sTotal) <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed optsV optsR tds globs (stepsFinal - m) dir sMid stepsMid + stepsTotal === stepsFinal' sFinal === sTotal @@ -1015,7 +1016,8 @@ tasty_type_preservation = withTests 1000 $ s' <- checkTest ty s forgetMetadata s === forgetMetadata s' -- check no smart holes happened maxSteps <- forAllT $ Gen.integral $ Range.linear 1 1000 -- Arbitrary limit here - (steps, s) <- failWhenSevereLogs $ evalFullStepCount @EvalLog optsV optsR tds globs maxSteps dir t + closed <- forAllT $ Gen.element @[] [UnderBinders] + (steps, s) <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed optsV optsR tds globs maxSteps dir t annotateShow steps annotateShow s -- s is often reduced to normal form @@ -1025,7 +1027,7 @@ tasty_type_preservation = withTests 1000 $ then label "generated a normal form" else do midSteps <- forAllT $ Gen.integral $ Range.linear 1 (steps - 1) - (_, s') <- failWhenSevereLogs $ evalFullStepCount @EvalLog optsV optsR tds globs midSteps dir t + (_, s') <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed optsV optsR tds globs midSteps dir t test "mid " s' -- Unsaturated primitives are stuck terms @@ -1483,6 +1485,7 @@ unit_eval_full_modules = { evalFullReqExpr = foo , evalFullCxtDir = Chk , evalFullMaxSteps = 2 + , evalFullOptions = UnderBinders } expect <- char 'A' pure $ case resp of @@ -1505,8 +1508,13 @@ unit_eval_full_modules_scrutinize_imported_type = [branch cTrue [] $ con0 cFalse, branch cFalse [] $ con0 cTrue] resp <- readerToState $ - handleEvalFullRequest - EvalFullReq{evalFullReqExpr = foo, evalFullCxtDir = Chk, evalFullMaxSteps = 2} + handleEvalFullRequest $ + EvalFullReq + { evalFullReqExpr = foo + , evalFullCxtDir = Chk + , evalFullMaxSteps = 2 + , evalFullOptions = UnderBinders + } expect <- con0 cFalse pure $ case resp of EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" @@ -1535,10 +1543,11 @@ tasty_unique_ids = withTests 1000 $ let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules tds <- asks typeDefs (dir, t1, _) <- genDirTm + closed <- forAllT $ Gen.element @[] [UnderBinders] let go n t | n == (0 :: Int) = pure () | otherwise = do - t' <- failWhenSevereLogs $ evalFull @EvalLog optsV optsR tds globs 1 dir t + t' <- failWhenSevereLogs $ evalFull @EvalLog closed optsV optsR tds globs 1 dir t case t' of Left (TimedOut e) -> uniqueIDs e >> go (n - 1) e Right e -> uniqueIDs e @@ -1606,9 +1615,10 @@ unit_case_prim = evalFullTest :: HasCallStack => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr) evalFullTest id_ tydefs globals n d e = do + let optsN = UnderBinders let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} let optsR = RunRedexOptions{pushAndElide = True} - let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsV optsR tydefs globals n d e + let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsN optsV optsR tydefs globals n d e assertNoSevereLogs logs distinctIDs r pure r @@ -1626,9 +1636,10 @@ evalFullTestExactSteps id_ tydefs globals n d e = do evalFullTasty :: MonadTest m => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Either EvalFullError Expr) evalFullTasty id_ tydefs globals n d e = do + let optsN = UnderBinders let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} let optsR = RunRedexOptions{pushAndElide = True} - let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsV optsR tydefs globals n d e + let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsN optsV optsR tydefs globals n d e testNoSevereLogs logs let ids = r ^.. evalResultExpr % exprIDs ids === ordNub ids diff --git a/primer/test/Tests/Prelude/Utils.hs b/primer/test/Tests/Prelude/Utils.hs index e36bdedd3..aee0c7048 100644 --- a/primer/test/Tests/Prelude/Utils.hs +++ b/primer/test/Tests/Prelude/Utils.hs @@ -8,6 +8,7 @@ import Optics (over) import Primer.Core (Expr, GVarName, Type) import Primer.Core.DSL (apps', create', gvar) import Primer.Eval ( + NormalOrderOptions (UnderBinders), RunRedexOptions (RunRedexOptions, pushAndElide), ViewRedexOptions (ViewRedexOptions, aggressiveElision, groupedLets), ) @@ -53,11 +54,12 @@ functionOutput f args = functionOutput' f (map Left args) -- Tests a prelude function with a combination of Expr/Type arguments to be applied functionOutput' :: GVarName -> [Either (TestM Expr) (TestM Type)] -> TerminationBound -> Either EvalFullError Expr functionOutput' f args depth = - let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} + let optsN = UnderBinders + optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} optsR = RunRedexOptions{pushAndElide = True} (r, logs) = evalTestM 0 $ runPureLogT $ do e <- apps' (gvar f) $ bimap lift lift <$> args - evalFull @EvalLog optsV optsR ty def n d e + evalFull @EvalLog optsN optsV optsR ty def n d e severe = Seq.filter isSevereLog logs in if null severe then r diff --git a/primer/test/Tests/Undo.hs b/primer/test/Tests/Undo.hs index 1b45cad97..598fad856 100644 --- a/primer/test/Tests/Undo.hs +++ b/primer/test/Tests/Undo.hs @@ -24,7 +24,7 @@ import Primer.Core ( qualifyName, ) import Primer.Def (astDefExpr, defAST) -import Primer.Eval (Dir (Syn)) +import Primer.Eval (Dir (Syn), NormalOrderOptions (UnderBinders)) import Primer.Module ( moduleDefsQualified, moduleName, @@ -73,6 +73,7 @@ unit_redo_eval = { App.evalFullReqExpr = Var (Meta 0 Nothing Nothing) (GlobalVarRef $ qualifyName scope "main") , App.evalFullCxtDir = Syn , App.evalFullMaxSteps = 10 + , App.evalFullOptions = UnderBinders } edit1 = handleEditRequest action1 edit2 = handleEditRequest . action2 From e42b7e970daed33367e64fe446888a2962c16214 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Mon, 5 Jun 2023 20:55:33 +0100 Subject: [PATCH 2/4] feat: optionally do not evaluate under binders This change means our EvalFull is "closed evaluation", rather than "open evaluation". The main reason to do this is so that evaluations of programs-in-construction (especially recursive ones) do not pointlessly blow up in size: if `even` and `odd` are defined recursively, then evaluating `even` would evaluate under the lambda and inside case branches, expanding `odd` and recursing; when it eventually times out one would have a big tree with many unrolled copies of `even` and `odd`, which is not very illuminating. Note that the reduction of "pushing a let down", e.g. `let x = t in f s ~> (let x = t in f) (let x = t in s)` happens at the `let` node, and thus is not "under" the `let x` binder. Note that we consider a "stack" of lets `let x=s in let y=t in r` to be one binder, so that we can (with `groupedLets = False`) reduce this by pushing the `let y` into the `r` (i.e. we don't count this as "under" the `let x` binder). We will not evaluate inside the `r`. Note that we do not evaluate in the RHS of pattern match branches which bind variables, for the same reason as we do not evaluate under lambdas; for consistency we also do not evaluate in the RHS of branches which do not bind variables. Signed-off-by: Ben Price --- .../test/outputs/OpenAPI/openapi.json | 3 +- primer/src/Primer/Eval/NormalOrder.hs | 34 ++- primer/test/Tests/Eval/Utils.hs | 14 +- primer/test/Tests/EvalFull.hs | 255 +++++++++++++++++- 4 files changed, 294 insertions(+), 12 deletions(-) diff --git a/primer-service/test/outputs/OpenAPI/openapi.json b/primer-service/test/outputs/OpenAPI/openapi.json index 50cf4c2b4..b852a7a8c 100644 --- a/primer-service/test/outputs/OpenAPI/openapi.json +++ b/primer-service/test/outputs/OpenAPI/openapi.json @@ -1493,7 +1493,8 @@ "required": false, "schema": { "enum": [ - "UnderBinders" + "UnderBinders", + "StopAtBinders" ], "type": "string" } diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs index e374be606..7db17bbff 100644 --- a/primer/src/Primer/Eval/NormalOrder.hs +++ b/primer/src/Primer/Eval/NormalOrder.hs @@ -22,11 +22,14 @@ import Primer.Core ( App, Case, Hole, + LAM, + Lam, Let, LetType, Letrec ), Type' ( + TForall, TLet ), ) @@ -94,6 +97,7 @@ viewLet dez@(_, ez) = case (target ez, exprChildren UnderBinders dez) of data NormalOrderOptions = UnderBinders + | StopAtBinders deriving stock (Eq, Show, Read, Generic) deriving (FromJSON, ToJSON) via PrimerJSON NormalOrderOptions @@ -118,7 +122,9 @@ data NormalOrderOptions -- We can optionally stop when we find a binder (e.g. to implement closed -- evaluation -- do not compute under binders), although for consistency we -- treat all case branches as being binders, even those that do not actually --- bind a variable. +-- bind a variable. Note that (for the case where we reduce a stack of @let@s +-- one-by-one inside-out) we need to go under let bindings, but stop when we +-- find a non-@let@. foldMapExpr :: forall f a. MonadPlus f => NormalOrderOptions -> FMExpr (f a) -> Dir -> Expr -> f a foldMapExpr opts extract topDir = go mempty . (topDir,) . focus where @@ -137,9 +143,12 @@ foldMapExpr opts extract topDir = go mempty . (topDir,) . focus -- its type annotation, we can handle them all uniformly -- Since this node is not a let, the context is reset _ -> - msum $ - (goType mempty =<< focusType' ez) -- NB: no binders in term scope over a type child - : map (go mempty) (exprChildren opts dez) + case (opts, lets) of + (StopAtBinders, Cxt (_ : _)) -> mzero + _ -> + msum $ + (goType mempty =<< focusType' ez) -- NB: no binders in term scope over a type child + : map (go mempty) (exprChildren opts dez) goType :: Cxt -> TypeZ -> f a goType lets tz = extract.ty tz lets @@ -202,13 +211,30 @@ exprChildren' (d, ez) = _ -> Chk (d', c) +-- Extract the children of the current focus, except those under an binder. +-- This is used to restrict our evaluation to "closed evaluation". +-- NB: for consistency we skip all case branches, not just those that bind a variable. +exprChildrenClosed :: (Dir, ExprZ) -> [(Dir, ExprZ)] +exprChildrenClosed (d, ez) = case target ez of + Lam{} -> [] + LAM{} -> [] + Let{} -> take 1 $ exprChildren' (d, ez) -- just the binding + LetType{} -> [] + Letrec{} -> [] + Case{} -> take 1 $ exprChildren' (d, ez) -- just the scrutinee + _ -> exprChildren' (d, ez) + exprChildren :: NormalOrderOptions -> (Dir, ExprZ) -> [(Dir, ExprZ)] exprChildren = \case UnderBinders -> exprChildren' + StopAtBinders -> exprChildrenClosed typeChildren :: NormalOrderOptions -> TypeZ -> [TypeZ] typeChildren = \case UnderBinders -> children' + StopAtBinders -> \tz -> case target tz of + TForall{} -> [] + _ -> children' tz singletonCxt :: LetBinding -> Cxt singletonCxt l = Cxt [l] diff --git a/primer/test/Tests/Eval/Utils.hs b/primer/test/Tests/Eval/Utils.hs index 8cb166a68..faacda104 100644 --- a/primer/test/Tests/Eval/Utils.hs +++ b/primer/test/Tests/Eval/Utils.hs @@ -4,6 +4,7 @@ module Tests.Eval.Utils ( genDirTm, testModules, hasTypeLets, + hasHoles, ) where import Foreword @@ -15,12 +16,12 @@ import Hedgehog (PropertyT) import Hedgehog.Gen qualified as Gen import Primer.Core ( Expr, - Expr' (LetType), + Expr' (EmptyHole, Hole, LetType), ID, Kind' (KType), ModuleName (ModuleName), Type, - Type' (TLet), + Type' (TEmptyHole, THole, TLet), ) import Primer.Core.DSL (create', lam, lvar, tcon, tfun) import Primer.Core.Utils (forgetMetadata, forgetTypeMetadata, generateIDs) @@ -98,3 +99,12 @@ hasTypeLets e = not $ null [() | LetType{} <- universe e] && null [() | TLet{} <- universeBi @_ @Type e] + +-- | Does this expression have any holes? +hasHoles :: Expr -> Bool +hasHoles e = + not $ + null [() | Hole{} <- universe e] + && null [() | EmptyHole{} <- universe e] + && null [() | THole{} <- universeBi @_ @Type e] + && null [() | TEmptyHole{} <- universeBi @_ @Type e] diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs index 46a52f9c0..ed2dc4eb7 100644 --- a/primer/test/Tests/EvalFull.hs +++ b/primer/test/Tests/EvalFull.hs @@ -42,6 +42,7 @@ import Primer.Core.DSL import Primer.Core.Utils ( exprIDs, forgetMetadata, + generateIDs, ) import Primer.Def (DefMap) import Primer.Eval @@ -51,7 +52,7 @@ import Primer.Examples qualified as Examples ( map', odd, ) -import Primer.Gen.Core.Typed (WT, forAllT, isolateWT, propertyWT) +import Primer.Gen.Core.Typed (WT, forAllT, genChk, isolateWT, propertyWT) import Primer.Log (runPureLogT) import Primer.Module ( Module (Module, moduleDefs, moduleName, moduleTypes), @@ -120,7 +121,7 @@ import Tasty ( ) import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@?=)) import Tests.Action.Prog (readerToState) -import Tests.Eval.Utils (genDirTm, hasTypeLets, testModules, (~=)) +import Tests.Eval.Utils (genDirTm, hasHoles, hasTypeLets, testModules, (~=)) import Tests.Gen.Core.Typed (checkTest) import Tests.Typecheck (runTypecheckTestM, runTypecheckTestMWithPrims) @@ -566,6 +567,235 @@ unit_tlet_self_capture = do r <~==> expect in mapM_ test (zip [0 ..] expected) +-- When doing closed eval (i.e. don't go under binders), pushing a @let@ +-- through a binder is not considered to be "under" that binder, else +-- @(let x=t1 in λy.t2 : S -> T) t3@ would be stuck. +unit_closed_let_beta :: Assertion +unit_closed_let_beta = + let ((expr, expected), maxID) = create $ do + e0 <- + let_ + "x" + (con0 cFalse `ann` tcon tBool) + ( lam "y" (con cCons [lvar "x", lvar "y"]) + `ann` (tcon tBool `tfun` (tcon tList `tapp` tcon tBool)) + ) + `app` con0 cTrue + e1 <- + let_ + "x" + (con0 cFalse `ann` tcon tBool) + ( lam + "y" + (con cCons [lvar "x", lvar "y"]) + ) + `ann` (tcon tBool `tfun` (tcon tList `tapp` tcon tBool)) + `app` con0 cTrue + e2 <- + lam + "y" + ( let_ + "x" + (con0 cFalse `ann` tcon tBool) + (con cCons [lvar "x", lvar "y"]) + ) + `ann` (tcon tBool `tfun` (tcon tList `tapp` tcon tBool)) + `app` con0 cTrue + e3 <- + let_ + "y" + (con0 cTrue `ann` tcon tBool) + ( let_ + "x" + (con0 cFalse `ann` tcon tBool) + (con cCons [lvar "x", lvar "y"]) + ) + `ann` (tcon tList `tapp` tcon tBool) + e4 <- + con + cCons + [ let_ + "x" + (con0 cFalse `ann` tcon tBool) + (lvar "x") + , let_ + "y" + (con0 cTrue `ann` tcon tBool) + (lvar "y") + ] + `ann` (tcon tList `tapp` tcon tBool) + e5 <- + con + cCons + [ con0 cFalse `ann` tcon tBool + , let_ + "y" + (con0 cTrue `ann` tcon tBool) + (lvar "y") + ] + `ann` (tcon tList `tapp` tcon tBool) + e6 <- + con + cCons + [ con0 cFalse + , let_ + "y" + (con0 cTrue `ann` tcon tBool) + (lvar "y") + ] + `ann` (tcon tList `tapp` tcon tBool) + e7 <- + con + cCons + [ con0 cFalse + , con0 cTrue `ann` tcon tBool + ] + `ann` (tcon tList `tapp` tcon tBool) + e8 <- + con + cCons + [ con0 cFalse + , con0 cTrue + ] + `ann` (tcon tList `tapp` tcon tBool) + pure (e0, map (Left . TimedOut) [e0, e1, e2, e3, e4, e5, e6, e7, e8] ++ [Right e8]) + test (n, expect) = do + r <- evalFullTestClosed GroupedLets maxID mempty mempty n Syn expr + r <~==> expect + in mapM_ test (zip [0 ..] expected) + +-- Closed eval and handling groups of @let@s singlely work together +unit_closed_single_lets :: Assertion +unit_closed_single_lets = + let ((expr, expected), maxID) = create $ do + e0 <- + let_ "x" (con0 cFalse) $ + let_ "y" (con0 cTrue) $ + con + cMakePair + [ lvar "x" + , lvar "y" + ] + e1 <- + let_ "x" (con0 cFalse) $ + con + cMakePair + [ lvar "x" + , let_ "y" (con0 cTrue) $ lvar "y" + ] + e2 <- + con + cMakePair + [ let_ "x" (con0 cFalse) $ lvar "x" + , let_ "y" (con0 cTrue) $ lvar "y" + ] + e3 <- + con + cMakePair + [ con0 cFalse + , let_ "y" (con0 cTrue) $ lvar "y" + ] + e4 <- + con + cMakePair + [ con0 cFalse + , con0 cTrue + ] + pure (e0, map (Left . TimedOut) [e0, e1, e2, e3, e4] ++ [Right e4]) + test (n, expect) = do + r <- evalFullTestClosed SingleLets maxID mempty mempty n Syn expr + r <~==> expect + in mapM_ test (zip [0 ..] expected) + +-- One reason for not evaluating under binders is to avoid a size blowup when +-- evaluating a recursive definition. For example, the unsaturated +-- `map @Bool @Bool not` would keep unrolling the recursive mentions of `map`. +-- (If it were applied to a concrete list, the beta redexes would be reduced instead.) +-- Since top-level definitions and recursive lets are essentially the same, one may +-- worry that we have the same issue with @letrec@. This test shows that closed eval +-- handles that case also. +unit_closed_letrec_binder :: Assertion +unit_closed_letrec_binder = + let ((expr, expected), maxID) = create $ do + e0 <- + letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) $ + lam "y" $ + lvar "x" + e1 <- + lam "y" $ + letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) $ + lvar "x" + pure (e0, map (Left . TimedOut) [e0, e1] ++ [Right e1]) + test (n, expect) = do + r <- evalFullTestClosed GroupedLets maxID mempty mempty n Syn expr + r <~==> expect + in mapM_ test (zip [0 ..] expected) + +-- closed eval stops at binders +unit_closed_binders :: Assertion +unit_closed_binders = do + let isNormalIffClosed e = do + let (e', i) = create e + evalFullTestClosed GroupedLets i mempty mempty 1 Syn e' >>= \case + Left (TimedOut _) -> assertFailure $ "not normal form, for closed eval, grouped lets: " <> show e' + Right _ -> pure () + evalFullTestClosed SingleLets i mempty mempty 1 Syn e' >>= \case + Left (TimedOut _) -> assertFailure $ "not normal form, for closed eval, single lets: " <> show e' + Right _ -> pure () + evalFullTest i mempty mempty 1 Syn e' >>= \case + Left (TimedOut _) -> pure () + Right _ -> assertFailure $ "unexpectedly a normal form, for open eval: " <> show e' + r = let_ "x" emptyHole $ lvar "x" + isNormalIffClosed $ lam "x" r + isNormalIffClosed $ lAM "a" r + isNormalIffClosed $ case_ emptyHole [branch cTrue [("x", Nothing)] r] + -- For consistency, we also do not reduce inside case branches even if they do not bind + isNormalIffClosed $ case_ emptyHole [branch cTrue [] r] + +-- closed eval still pushes lets through binders +unit_closed_subst :: Assertion +unit_closed_subst = do + let isReducible e = do + let (e', i) = create e + evalFullTestClosed GroupedLets i mempty mempty 1 Syn e' >>= \case + Left (TimedOut _) -> pure () + Right _ -> assertFailure $ "unexpectedly a normal form: " <> show e' + l = let_ "x" emptyHole + v = lvar "x" + isReducible $ l $ lam "y" v + isReducible $ l $ lAM "a" v + isReducible $ l $ case_ emptyHole [branch cTrue [("x", Nothing)] v] + isReducible $ l $ case_ emptyHole [branch cTrue [] v] + +-- For (closed, hole free) terms of base types, open and closed evaluation +-- agree. We require hole-free-ness, as holes create stuck terms similar to +-- free variables. Note that we get the same reduction sequence, not only that +-- they reduce to the same value. +tasty_open_closed_agree_base_types :: Property +tasty_open_closed_agree_base_types = withDiscards 1000 $ + propertyWT testModules $ do + let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} + let optsR = RunRedexOptions{pushAndElide = True} + ty <- forAllT $ Gen.element @[] [tBool, tNat, tInt] + tm' <- forAllT $ genChk $ TCon () ty + tm <- generateIDs tm' + when (hasHoles tm) discard + tds <- asks typeDefs + let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules + let reductionSequence closed expr n = + (expr :) + <$> if n <= (0 :: Integer) + then pure [] + else + evalFull @EvalLog closed optsV optsR tds globs 1 Chk expr >>= \case + Left (TimedOut expr') -> reductionSequence closed expr' (n - 1) + Right _ -> pure [] + (openSeq, openLogs) <- lift $ isolateWT $ runPureLogT $ reductionSequence UnderBinders tm 100 + testNoSevereLogs openLogs + (closedSeq, closedLogs) <- lift $ isolateWT $ runPureLogT $ reductionSequence StopAtBinders tm 100 + testNoSevereLogs closedLogs + openSeq === closedSeq + -- TODO: examples with holes -- TODO: most of these property tests could benefit from generating an @@ -588,7 +818,7 @@ resumeTest mods dir t = do let globs = foldMap' moduleDefsQualified mods tds <- asks typeDefs n <- forAllT $ Gen.integral $ Range.linear 2 1000 -- Arbitrary limit here - closed <- forAllT $ Gen.element @[] [UnderBinders] + closed <- forAllT $ Gen.frequency [(10, pure UnderBinders), (1, pure StopAtBinders)] -- NB: We need to run this first reduction in an isolated context -- as we need to avoid it changing the fresh-name-generator state -- for the next run (sMid and sTotal). This is because reduction may need @@ -1016,7 +1246,7 @@ tasty_type_preservation = withTests 1000 $ s' <- checkTest ty s forgetMetadata s === forgetMetadata s' -- check no smart holes happened maxSteps <- forAllT $ Gen.integral $ Range.linear 1 1000 -- Arbitrary limit here - closed <- forAllT $ Gen.element @[] [UnderBinders] + closed <- forAllT $ Gen.frequency [(10, pure UnderBinders), (1, pure StopAtBinders)] (steps, s) <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed optsV optsR tds globs maxSteps dir t annotateShow steps annotateShow s @@ -1543,7 +1773,7 @@ tasty_unique_ids = withTests 1000 $ let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules tds <- asks typeDefs (dir, t1, _) <- genDirTm - closed <- forAllT $ Gen.element @[] [UnderBinders] + closed <- forAllT $ Gen.frequency [(10, pure UnderBinders), (1, pure StopAtBinders)] let go n t | n == (0 :: Int) = pure () | otherwise = do @@ -1634,6 +1864,21 @@ evalFullTestExactSteps id_ tydefs globals n d e = do Left t' -> assertFailure $ "Unexpected timeout: " <> show t' Right t' -> pure t' +data GroupedLets = GroupedLets | SingleLets + +evalFullTestClosed :: GroupedLets -> ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr) +evalFullTestClosed gl id_ tydefs globals n d e = do + let optsN = StopAtBinders + let gl' = case gl of + GroupedLets -> True + SingleLets -> False + let optsV = ViewRedexOptions{groupedLets = gl', aggressiveElision = True} + let optsR = RunRedexOptions{pushAndElide = True} + let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsN optsV optsR tydefs globals n d e + assertNoSevereLogs logs + distinctIDs r + pure r + evalFullTasty :: MonadTest m => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Either EvalFullError Expr) evalFullTasty id_ tydefs globals n d e = do let optsN = UnderBinders From 5e4ed982167854cc45faef3e54c25ea0031733ea Mon Sep 17 00:00:00 2001 From: Ben Price Date: Sun, 23 Jul 2023 16:21:06 +0100 Subject: [PATCH 3/4] feat: OpenAPI evalFull defaults to StopAtBinders Signed-off-by: Ben Price --- primer-api/src/Primer/API.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/primer-api/src/Primer/API.hs b/primer-api/src/Primer/API.hs index bbf27bef4..2f8055d2e 100644 --- a/primer-api/src/Primer/API.hs +++ b/primer-api/src/Primer/API.hs @@ -226,7 +226,7 @@ import Primer.Def ( defAST, ) import Primer.Def qualified as Def -import Primer.Eval (NormalOrderOptions (UnderBinders)) +import Primer.Eval (NormalOrderOptions (StopAtBinders)) import Primer.Eval.Redex (Dir (Chk), EvalLog) import Primer.EvalFull (TerminationBound) import Primer.JSON ( @@ -1142,7 +1142,7 @@ evalFull' = curry4 $ logAPI (noError EvalFull') $ \(sid, lim, closed, d) -> { evalFullReqExpr = e , evalFullCxtDir = Chk , evalFullMaxSteps = fromMaybe 10 lim - , evalFullOptions = fromMaybe UnderBinders closed + , evalFullOptions = fromMaybe StopAtBinders closed } pure $ case x of App.EvalFullRespTimedOut e' -> EvalFullRespTimedOut $ viewTreeExpr e' From 8a6a8461a2986afa0342754612e2b7861351fd4b Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 25 Jul 2023 16:20:49 +0100 Subject: [PATCH 4/4] test: closed eval behaves fine with holes Signed-off-by: Ben Price --- primer/test/Tests/EvalFull.hs | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs index ed2dc4eb7..37f55d620 100644 --- a/primer/test/Tests/EvalFull.hs +++ b/primer/test/Tests/EvalFull.hs @@ -49,6 +49,7 @@ import Primer.Eval import Primer.EvalFull import Primer.Examples qualified as Examples ( even, + map, map', odd, ) @@ -426,6 +427,25 @@ unit_15 = s <- evalFullTest maxID builtinTypes mempty (fromIntegral $ length steps) Syn expr s <~==> Right expected +unit_map_hole :: Assertion +unit_map_hole = + let n = 3 + modName = mkSimpleModuleName "TestModule" + ((globals, expr, expected), maxID) = create $ do + (mapName, mapDef) <- Examples.map modName + let lst = list_ $ take n $ iterate (con1 cSucc) (con0 cZero) + e <- gvar mapName `aPP` tcon tNat `aPP` tcon tBool `app` emptyHole `app` lst + let globs = [(mapName, mapDef)] + expect <- list_ (take n $ ((emptyHole `ann` (tcon tNat `tfun` tcon tBool)) `app`) <$> iterate (con1 cSucc) (con0 cZero)) `ann` (tcon tList `tapp` tcon tBool) + pure (M.fromList globs, e, expect) + in do + sO <- evalFullTest maxID builtinTypes globals 200 Syn expr + sO <~==> Right expected + sCG <- evalFullTestClosed GroupedLets maxID builtinTypes globals 200 Syn expr + sCG <~==> Right expected + sCS <- evalFullTestClosed SingleLets maxID builtinTypes globals 300 Syn expr + sCS <~==> Right expected + unit_hole_ann_case :: Assertion unit_hole_ann_case = let (tm, maxID) = create $ hole $ ann (case_ emptyHole []) (tcon tBool)