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

primer-api/src/Primer/API.hs

@@ -226,6 +226,7 @@ import Primer.Def (
   defAST,
  )
 import Primer.Def qualified as Def
+import Primer.Eval (NormalOrderOptions (StopAtBinders))
 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 StopAtBinders closed
             }
       pure $ case x of
         App.EvalFullRespTimedOut e' -> EvalFullRespTimedOut $ viewTreeExpr e'

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

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

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
 

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 ::

primer-service/test/outputs/OpenAPI/openapi.json

@@ -1486,6 +1486,18 @@
                             "minimum": 0,
                             "type": "integer"
                         }
+                    },
+                    {
+                        "in": "query",
+                        "name": "closed",
+                        "required": false,
+                        "schema": {
+                            "enum": [
+                                "UnderBinders",
+                                "StopAtBinders"
+                            ],
+                            "type": "string"
+                        }
                     }
                 ],
                 "requestBody": {
@@ -1509,7 +1521,7 @@
                         "description": ""
                     },
                     "400": {
-                        "description": "Invalid `body` or `stepLimit`"
+                        "description": "Invalid `body` or `closed` or `stepLimit`"
                     },
                     "404": {
                         "description": "`sessionId` not found"

primer/src/Primer/App.hs

@@ -487,6 +487,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
@@ -595,12 +596,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

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))

primer/src/Primer/Eval/NormalOrder.hs

@@ -6,6 +6,7 @@ module Primer.Eval.NormalOrder (
   findRedex,
   foldMapExpr,
   FMExpr (..),
+  NormalOrderOptions (..),
   -- Exported for testing
   singletonCxt,
 ) where
@@ -21,11 +22,14 @@ import Primer.Core (
     App,
     Case,
     Hole,
+    LAM,
+    Lam,
     Let,
     LetType,
     Letrec
   ),
   Type' (
+    TForall,
     TLet
   ),
  )
@@ -43,6 +47,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 +86,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 +95,12 @@ viewLet dez@(_, ez) = case (target ez, exprChildren dez) of
     tz :: [TypeZ]
     tz = maybeToList $ focusType ez
 
+data NormalOrderOptions
+  = UnderBinders
+  | StopAtBinders
+  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 +118,15 @@ 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. 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
     go :: Cxt -> (Dir, ExprZ) -> f a
     go lets dez@(d, ez) =
@@ -125,17 +143,20 @@ foldMapExpr 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)
-                : map (go mempty) (exprChildren 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
         <|> 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 +170,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 +191,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 +211,30 @@ exprChildren (d, ez) =
           _ -> Chk
     (d', c)
 
-typeChildren :: TypeZ -> [TypeZ]
-typeChildren = children'
+-- 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]