From 5c457668c0b71a354ba8919a8849d92cd8a1f0d6 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Mon, 5 Jun 2023 20:55:33 +0100 Subject: [PATCH] feat: optionally do not evaluate under binders (except lets) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This change means our EvalFull is "closed evaluation", rather than "open evaluation". Note that we must evaluate under (various flavours of) `let` bindings since we need substitute usages of these variables: we do not want to consider `let x = 1 in x + x` to be stuck, but we are happy to consider `λx.MkPair x (not True)` to be stuck. 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 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 --- primer/src/Primer/Eval/NormalOrder.hs | 15 ++++ primer/test/Tests/Eval.hs | 6 +- primer/test/Tests/Eval/Utils.hs | 14 ++- primer/test/Tests/EvalFull.hs | 125 ++++++++++++++++++++++++-- 4 files changed, 149 insertions(+), 11 deletions(-) diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs index 73508b5c0..f2ab98b11 100644 --- a/primer/src/Primer/Eval/NormalOrder.hs +++ b/primer/src/Primer/Eval/NormalOrder.hs @@ -45,6 +45,8 @@ import Primer.Core ( App, Case, Hole, + LAM, + Lam, Let, LetType, Letrec @@ -139,6 +141,7 @@ viewLet dez@(_, ez) = case (target ez, exprChildren' dez) of data NormalOrderOptions -- TODO/REVIEW: this is a bit of a misnomer, as it affects `Eval.redexes`, which is only used for single-step. NB: even if we set StopAtBinders, we can still call `Eval.step` with the id of a redex under a binder and it will reduce, even though `redexes` will not report that id = UnderBinders + | StopAtBinders deriving stock (Eq, Show, Read, Generic) deriving (FromJSON, ToJSON) via PrimerJSON NormalOrderOptions @@ -330,9 +333,21 @@ exprChildren' (d, ez) = addBinds ez bs pure (d', c) +-- Extract the children of the current focus, except those under an "unknown" binder, +-- i.e. we extract the body of a let but not the body of a lambda, or the RHS of case branches. +-- 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) -> [Accum Cxt (Dir, ExprZ)] +exprChildrenClosed (d, ez) = case target ez of + Lam{} -> [] + LAM{} -> [] + Case{} -> take 1 $ exprChildren' (d, ez) -- just the scrutinee + _ -> exprChildren' (d, ez) + exprChildren :: NormalOrderOptions -> (Dir, ExprZ) -> [Accum Cxt (Dir, ExprZ)] exprChildren = \case UnderBinders -> exprChildren' + StopAtBinders -> exprChildrenClosed typeChildren :: TypeZ -> [Accum Cxt TypeZ] typeChildren tz = diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs index a80b3b782..19cb5916e 100644 --- a/primer/test/Tests/Eval.hs +++ b/primer/test/Tests/Eval.hs @@ -58,7 +58,7 @@ import Primer.Eval ( GlobalVarInlineDetail (..), LetRemovalDetail (..), LocalVarInlineDetail (..), - NormalOrderOptions (UnderBinders), + NormalOrderOptions (StopAtBinders, UnderBinders), findNodeByID, getNonCapturedLocal, redexes, @@ -1430,7 +1430,7 @@ tasty_type_preservation = let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules tds <- asks typeDefs (dir, t, ty) <- genDirTm - closed <- forAllT $ Gen.element [UnderBinders] + closed <- forAllT $ Gen.element [UnderBinders, StopAtBinders] rs <- failWhenSevereLogs $ redexes @EvalLog closed tds globs dir t when (null rs) discard r <- forAllT $ Gen.element rs @@ -1459,7 +1459,7 @@ tasty_redex_independent = (dir, t, _) <- genDirTm annotateShow dir annotateShow t - closed <- forAllT $ Gen.element [UnderBinders] + closed <- forAllT $ Gen.element [UnderBinders, StopAtBinders] rs <- failWhenSevereLogs $ redexes @EvalLog closed tds globs dir t when (length rs <= 1) discard i <- forAllT $ Gen.element rs diff --git a/primer/test/Tests/Eval/Utils.hs b/primer/test/Tests/Eval/Utils.hs index 9764346f7..2418c77cf 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 11e958dfd..462642d7e 100644 --- a/primer/test/Tests/EvalFull.hs +++ b/primer/test/Tests/EvalFull.hs @@ -22,6 +22,7 @@ import Primer.App ( ) import Primer.Builtins ( boolDef, + cCons, cFalse, cJust, cMakePair, @@ -41,16 +42,17 @@ import Primer.Core.DSL import Primer.Core.Utils ( exprIDs, forgetMetadata, + generateIDs, ) import Primer.Def (DefMap) -import Primer.Eval (NormalOrderOptions (UnderBinders)) +import Primer.Eval (NormalOrderOptions (StopAtBinders, UnderBinders)) import Primer.EvalFull import Primer.Examples qualified as Examples ( even, 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), @@ -119,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) @@ -427,6 +429,110 @@ unit_tlet_self_capture = do r <~==> expect in mapM_ test (zip [0 ..] expected) +-- When doing closed eval (i.e. don't go under binders), we still need to do +-- substitution under binders, else @let@s can block redexes. +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 [con0 cFalse `ann` tcon tBool, lvar "y"]) `ann` (tcon tBool `tfun` (tcon tList `tapp` tcon tBool))) `app` con0 cTrue + e2 <- (lam "y" (con cCons [con0 cFalse `ann` tcon tBool, lvar "y"]) `ann` (tcon tBool `tfun` (tcon tList `tapp` tcon tBool))) `app` con0 cTrue + e3 <- let_ "y" (con0 cTrue `ann` tcon tBool) (con cCons [con0 cFalse `ann` tcon tBool, lvar "y"]) `ann` (tcon tList `tapp` tcon tBool) + e4 <- let_ "y" (con0 cTrue `ann` tcon tBool) (con cCons [con0 cFalse `ann` tcon tBool, con0 cTrue `ann` tcon tBool]) `ann` (tcon tList `tapp` tcon tBool) + e5 <- con cCons [con0 cFalse `ann` tcon tBool, con0 cTrue `ann` tcon tBool] `ann` (tcon tList `tapp` tcon tBool) + e6 <- con cCons [con0 cFalse, con0 cTrue `ann` tcon tBool] `ann` (tcon tList `tapp` tcon tBool) + e7 <- 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] ++ [Right e7]) + test (n, expect) = do + r <- evalFullTestClosed 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, and +-- we do substitution of @let@s under binders, one may worry that we have the same +-- issue with @letrec@. This test shows that we do not. +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 <- + letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) $ + lam "y" $ + letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) $ + list_ [lvar "x", lvar "x"] `ann` tcon tBool + e2 <- lam "y" $ letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) $ list_ [lvar "x", lvar "x"] `ann` tcon tBool + pure (e0, map (Left . TimedOut) [e0, e1, e2] ++ [Right e2]) + test (n, expect) = do + r <- evalFullTestClosed 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 i mempty mempty 1 Syn e' >>= \case + Left (TimedOut _) -> assertFailure $ "not normal form, for closed eval: " <> 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 substitutes under binders +-- (otherwise we might not be able to elide a let which blocks a redex -- see +-- unit_closed_let_beta) +unit_closed_subst :: Assertion +unit_closed_subst = do + let isReducible e = do + let (e', i) = create e + evalFullTestClosed 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 + 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 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 @@ -447,7 +553,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.element [UnderBinders, 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 @@ -822,7 +928,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.element [UnderBinders, StopAtBinders] (steps, s) <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed tds globs maxSteps dir t annotateShow steps annotateShow s @@ -1340,7 +1446,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.element [UnderBinders, StopAtBinders] let go n t | n == (0 :: Int) = pure () | otherwise = do @@ -1418,6 +1524,13 @@ evalFullTest id_ tydefs globals n d e = do distinctIDs r pure r +evalFullTestClosed :: ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr) +evalFullTestClosed id_ tydefs globals n d e = do + let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog StopAtBinders 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 (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog UnderBinders tydefs globals n d e