feat: optionally do not evaluate under binders (except lets)

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 <[email protected]>
hackworthltd · Jul 20, 2023 · 5c45766 · 5c45766
1 parent d95689a
commit 5c45766
Show file tree

Hide file tree

Showing 4 changed files with 149 additions and 11 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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