refactor! make eval-under-binders an option with no alternatives

This is a stepping-stone to making an option to not evaluate under
binders.

BREAKING CHANGE: This adds a new field to `EvalReq` and `EvalFullReq`,
both of which are exposed in the richly-typed API. (But not the
OpenAPI.)

primer-api/src/Primer/API.hs

@@ -216,6 +216,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 (
@@ -1128,6 +1129,7 @@ evalFull' = curry3 $ logAPI (noError EvalFull') $ \(sid, lim, d) ->
             { evalFullReqExpr = e
             , evalFullCxtDir = Chk
             , evalFullMaxSteps = fromMaybe 10 lim
+            , evalFullOptions = UnderBinders -- TODO/REVIEW: should we expose this to the actual api? If so, the BREAKING CHANGE commit message needs updating
             }
       pure $ case x of
         App.EvalFullRespTimedOut e' -> EvalFullRespTimedOut $ viewTreeExpr e'

primer-benchmark/src/Benchmarks.hs

@@ -20,6 +20,7 @@ import Primer.App (
   tcWholeProgWithImports,
  )
 import Primer.App.Utils (forgetProgTypecache)
+import Primer.Eval (NormalOrderOptions (UnderBinders))
 import Primer.EvalFull (
   Dir (Syn),
   EvalLog,
@@ -101,11 +102,11 @@ benchmarks =
     evalTestMPureLogs e maxEvals =
       evalTestM (maxID e) $
         runPureLogT $
-          evalFull @EvalLog builtinTypes (defMap e) maxEvals Syn (expr e)
+          evalFull @EvalLog UnderBinders builtinTypes (defMap e) maxEvals Syn (expr e)
     evalTestMDiscardLogs e maxEvals =
       evalTestM (maxID e) $
         runDiscardLogT $
-          evalFull @EvalLog builtinTypes (defMap e) maxEvals Syn (expr e)
+          evalFull @EvalLog UnderBinders builtinTypes (defMap e) maxEvals Syn (expr e)
 
     benchExpected f g e n b = EnvBench e n $ \e' ->
       NF

primer/src/Primer/App.hs

@@ -466,6 +466,7 @@ data MutationRequest
 data EvalReq = EvalReq
   { evalReqExpr :: Expr
   , evalReqRedex :: ID
+  , evalReqOptions :: Eval.NormalOrderOptions
   }
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON EvalReq
@@ -482,6 +483,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
@@ -577,7 +579,7 @@ handleEvalRequest req = do
   case result of
     Left err -> throwError' err
     Right (expr, detail) -> do
-      redexes <- Eval.redexes (allTypes prog) (allDefs prog) Syn expr
+      redexes <- Eval.redexes (evalReqOptions req) (allTypes prog) (allDefs prog) Syn expr
       pure
         EvalResp
           { evalRespExpr = expr
@@ -590,10 +592,10 @@ 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
-  result <- runFreshM app $ evalFull (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr
+  result <- runFreshM app $ evalFull evalFullOptions (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr
   pure $ case result of
     Left (TimedOut e) -> EvalFullRespTimedOut e
     Right nf -> EvalFullRespNormal nf

primer/src/Primer/Eval.hs

@@ -5,6 +5,7 @@ module Primer.Eval (
   -- The public API of this module
   step,
   redexes,
+  NormalOrderOptions (..),
   EvalLog (..),
   EvalError (..),
   EvalDetail (..),
@@ -53,6 +54,7 @@ import Primer.Eval.Detail (
 import Primer.Eval.EvalError (EvalError (..))
 import Primer.Eval.NormalOrder (
   FMExpr (FMExpr, expr, subst, substTy, ty),
+  NormalOrderOptions (..),
   foldMapExpr,
   singletonCxt,
  )
@@ -108,6 +110,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
@@ -122,14 +125,16 @@ findNodeByID i =
 redexes ::
   forall l m.
   (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) =>
+  NormalOrderOptions ->
   TypeDefMap ->
   DefMap ->
   Dir ->
   Expr ->
   m [ID]
-redexes tydefs globals =
+redexes opts tydefs globals =
   (ListT.toList .)
     . foldMapExpr
+      opts
       FMExpr
         { expr = \ez d -> liftMaybeT . runReaderT (getID ez <$ viewRedex tydefs globals d (target ez))
         , ty = \tz -> runReader (whenJust (getID tz) <$> viewRedexType (target tz))

primer/src/Primer/Eval/NormalOrder.hs

@@ -7,6 +7,7 @@ module Primer.Eval.NormalOrder (
   findRedex,
   foldMapExpr,
   FMExpr (..),
+  NormalOrderOptions (..),
   -- Exported for testing
   singletonCxt,
 ) where
@@ -95,6 +96,7 @@ import Primer.Eval.Redex (
   viewRedexType,
   _freeVarsLetBinding,
  )
+import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON)
 import Primer.Log (ConvertLogMessage)
 import Primer.Name (Name)
 import Primer.TypeDef (
@@ -129,12 +131,17 @@ data RedexWithContext
   | RType TypeZ RedexType
 
 viewLet :: (Dir, ExprZ) -> Maybe (LetBinding, Accum Cxt (Dir, ExprZ))
-viewLet dez@(_, ez) = case (target ez, exprChildren dez) of
+viewLet dez@(_, ez) = case (target ez, exprChildren' dez) of
   (Let _ x e _b, [_, bz]) -> Just (LetBind x e, bz)
   (Letrec _ x e ty _b, [_, bz]) -> Just (LetrecBind x e ty, bz)
   (LetType _ a ty _b, [bz]) -> bz `seq` Just (LetTyBind $ LetTypeBind a ty, bz)
   _ -> Nothing
 
+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
+  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)
@@ -151,8 +158,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 = flip evalAccumT mempty . go . (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 = flip evalAccumT mempty . go . (topDir,) . focus
   where
     go :: (Dir, ExprZ) -> AccumT Cxt f a
     go dez@(d, ez) =
@@ -164,7 +176,7 @@ foldMapExpr extract topDir = flip evalAccumT mempty . go . (topDir,) . focus
           _ ->
             msum $
               (goType =<< focusType' ez)
-                : map (go <=< hoistAccum) (exprChildren dez)
+                : map (go <=< hoistAccum) (exprChildren opts dez)
     goType :: TypeZ -> AccumT Cxt f a
     goType tz =
       readerToAccumT (ReaderT $ extract.ty tz)
@@ -205,13 +217,15 @@ hoistAccum = Foreword.hoistAccum generalize
 findRedex ::
   forall l m.
   (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) =>
+  NormalOrderOptions ->
   TypeDefMap ->
   DefMap ->
   Dir ->
   Expr ->
   MaybeT m RedexWithContext
-findRedex tydefs globals =
+findRedex opts tydefs globals =
   foldMapExpr
+    opts
     ( FMExpr
         { expr = \ez d -> runReaderT (RExpr ez <$> viewRedex tydefs globals d (target ez))
         , ty = \tz -> hoistMaybe . runReader (RType tz <<$>> viewRedexType (target tz))
@@ -255,7 +269,8 @@ findRedex tydefs globals =
                   _ -> mzero
              in msum @[] $
                   Foreword.hoistAccum hoistMaybe (substTyChild =<< focusType' ez)
-                    : map (substChild <=< hoistAccum) (exprChildren (d, ez))
+                    -- Note that we need to go under binders when substituting
+                    : map (substChild <=< hoistAccum) (exprChildren' (d, ez))
        in here <|> innerLet <|> dive
     goSubstTy :: TyVarName -> Type -> TypeZ -> AccumT Cxt Maybe RedexWithContext
     goSubstTy v t tz =
@@ -291,8 +306,10 @@ children' z = case down z of
   Nothing -> mempty
   Just z' -> z' : unfoldr (fmap (\x -> (x, x)) . right) z'
 
-exprChildren :: (Dir, ExprZ) -> [Accum Cxt (Dir, ExprZ)]
-exprChildren (d, ez) =
+-- All children of the current focus, monadically adding any bindings of which
+-- we have just entered the scope.
+exprChildren' :: (Dir, ExprZ) -> [Accum Cxt (Dir, ExprZ)]
+exprChildren' (d, ez) =
   children' ez <&> \c -> do
     let bs = getBoundHere' (target ez) (Just $ target c)
     let d' = case target ez of
@@ -313,6 +330,10 @@ exprChildren (d, ez) =
     addBinds ez bs
     pure (d', c)
 
+exprChildren :: NormalOrderOptions -> (Dir, ExprZ) -> [Accum Cxt (Dir, ExprZ)]
+exprChildren = \case
+  UnderBinders -> exprChildren'
+
 typeChildren :: TypeZ -> [Accum Cxt TypeZ]
 typeChildren tz =
   children' tz <&> \c -> do

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 (..),
@@ -49,8 +49,16 @@ newtype EvalFullError
 type TerminationBound = Natural
 
 -- A naive implementation of normal-order reduction
-evalFull :: MonadEval l m => TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Either EvalFullError Expr)
-evalFull tydefs env n d expr = snd <$> evalFullStepCount tydefs env n d expr
+evalFull ::
+  MonadEval l m =>
+  NormalOrderOptions ->
+  TypeDefMap ->
+  DefMap ->
+  TerminationBound ->
+  Dir ->
+  Expr ->
+  m (Either EvalFullError Expr)
+evalFull opts tydefs env n d expr = snd <$> evalFullStepCount opts tydefs env n d expr
 
 -- | As 'evalFull', but also returns how many reduction steps were taken.
 -- (This is mostly useful for testing purposes.)
@@ -62,26 +70,27 @@ evalFull tydefs env n d expr = snd <$> evalFullStepCount tydefs env n d expr
 -- more to notice termination.
 evalFullStepCount ::
   MonadEval l m =>
+  NormalOrderOptions ->
   TypeDefMap ->
   DefMap ->
   TerminationBound ->
   Dir ->
   Expr ->
   m (Natural, Either EvalFullError Expr)
-evalFullStepCount tydefs env n d = go 0
+evalFullStepCount opts tydefs env n d = go 0
   where
     go s expr
       | s >= n = pure (s, Left $ TimedOut expr)
       | otherwise =
-          runMaybeT (step tydefs env d expr) >>= \case
+          runMaybeT (step opts 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 => TypeDefMap -> DefMap -> Dir -> Expr -> MaybeT m Expr
-step tydefs g d e =
-  findRedex tydefs g d e >>= \case
+step :: MonadEval l m => NormalOrderOptions -> TypeDefMap -> DefMap -> Dir -> Expr -> MaybeT m Expr
+step opts tydefs g d e =
+  findRedex opts tydefs g d e >>= \case
     RExpr ez r -> lift $ unfocusExpr . flip replace ez . fst <$> runRedex r
     RType et r -> lift $ unfocusExpr . unfocusType . flip replace et . fst <$> runRedexTy r

primer/test/Tests/Eval.hs

@@ -12,7 +12,7 @@ import Hedgehog (annotateShow, assert, discard, failure, label, success, (===))
 import Hedgehog.Gen qualified as Gen
 import Optics (elemOf, (^.))
 import Primer.App (
-  EvalReq (EvalReq, evalReqExpr, evalReqRedex),
+  EvalReq (EvalReq, evalReqExpr, evalReqOptions, evalReqRedex),
   EvalResp (EvalResp, evalRespExpr),
   handleEvalRequest,
   importModules,
@@ -58,6 +58,7 @@ import Primer.Eval (
   GlobalVarInlineDetail (..),
   LetRemovalDetail (..),
   LocalVarInlineDetail (..),
+  NormalOrderOptions (UnderBinders),
   findNodeByID,
   getNonCapturedLocal,
   redexes,
@@ -985,7 +986,7 @@ unit_findNodeByID_capture_type =
 -- | A helper for these tests
 redexes' :: TypeDefMap -> DefMap -> Dir -> Expr -> IO (Set ID)
 redexes' types prims d e = do
-  let (rs, logs) = runPureLog $ redexes types prims d e
+  let (rs, logs) = runPureLog $ redexes UnderBinders types prims d e
   assertNoSevereLogs @EvalLog logs
   pure $ Set.fromList rs
 
@@ -1379,7 +1380,7 @@ unit_eval_modules =
         EvalResp{evalRespExpr = e} <-
           readerToState $
             handleEvalRequest
-              EvalReq{evalReqExpr = foo, evalReqRedex = getID foo}
+              EvalReq{evalReqExpr = foo, evalReqRedex = getID foo, evalReqOptions = UnderBinders}
         expect <- char 'A'
         pure $ e ~= expect
       a = newEmptyApp
@@ -1400,7 +1401,7 @@ unit_eval_modules_scrutinize_imported_type =
         EvalResp{evalRespExpr = e} <-
           readerToState $
             handleEvalRequest
-              EvalReq{evalReqExpr = foo, evalReqRedex = getID foo}
+              EvalReq{evalReqExpr = foo, evalReqRedex = getID foo, evalReqOptions = UnderBinders}
         expect <- con0 cFalse
         pure $ e ~= expect
       a = newEmptyApp
@@ -1429,7 +1430,8 @@ tasty_type_preservation =
             let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
             tds <- asks typeDefs
             (dir, t, ty) <- genDirTm
-            rs <- failWhenSevereLogs $ redexes @EvalLog tds globs dir t
+            closed <- forAllT $ Gen.element [UnderBinders]
+            rs <- failWhenSevereLogs $ redexes @EvalLog closed tds globs dir t
             when (null rs) discard
             r <- forAllT $ Gen.element rs
             s <- failWhenSevereLogs $ step @EvalLog tds globs t dir r
@@ -1457,7 +1459,8 @@ tasty_redex_independent =
             (dir, t, _) <- genDirTm
             annotateShow dir
             annotateShow t
-            rs <- failWhenSevereLogs $ redexes @EvalLog tds globs dir t
+            closed <- forAllT $ Gen.element [UnderBinders]
+            rs <- failWhenSevereLogs $ redexes @EvalLog closed tds globs dir t
             when (length rs <= 1) discard
             i <- forAllT $ Gen.element rs
             j <- forAllT $ Gen.element $ delete i rs
@@ -1471,5 +1474,5 @@ tasty_redex_independent =
                     sj <- failWhenSevereLogs $ step @EvalLog tds globs t dir j
                     case sj of
                       Right (_, BindRename{}) -> success
-                      _ -> assert . elem j =<< failWhenSevereLogs (redexes @EvalLog tds globs dir s')
+                      _ -> assert . elem j =<< failWhenSevereLogs (redexes @EvalLog closed tds globs dir s')
                   else success