feat: push down lets

primer/primer.cabal

@@ -79,6 +79,7 @@ library
     Primer.Eval.Let
     Primer.Eval.NormalOrder
     Primer.Eval.Prim
+    Primer.Eval.Push
     Primer.Primitives.PrimDef
     Primer.Typecheck.Cxt
     Primer.Typecheck.Kindcheck

primer/src/Primer/App.hs

@@ -181,7 +181,7 @@ import Primer.Def (
 import Primer.Def.Utils (globalInUse, typeInUse)
 import Primer.Eval qualified as Eval
 import Primer.Eval.Detail (EvalDetail)
-import Primer.Eval.Redex (EvalLog)
+import Primer.Eval.Redex (EvalLog, RunRedexOptions (RunRedexOptions,pushAndElide), ViewRedexOptions (ViewRedexOptions, pushMulti))
 import Primer.EvalFull (Dir (Syn), EvalFullError (TimedOut), TerminationBound, evalFull)
 import Primer.JSON
 import Primer.Log (ConvertLogMessage)
@@ -592,7 +592,9 @@ handleEvalFullRequest ::
 handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxSteps}) = do
   app <- ask
   let prog = appProg app
-  result <- runFreshM app $ evalFull (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr
+  let optsV = ViewRedexOptions { pushMulti = True, aggressiveElision = True }
+  let optsR = RunRedexOptions { pushAndElide = True }
+  result <- runFreshM app $ evalFull 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

@@ -5,6 +5,8 @@ module Primer.Eval (
   -- The public API of this module
   step,
   redexes,
+  RunRedexOptions (..),
+  ViewRedexOptions (..),
   EvalLog (..),
   EvalError (..),
   EvalDetail (..),
@@ -16,10 +18,11 @@ module Primer.Eval (
   GlobalVarInlineDetail (..),
   LetRemovalDetail (..),
   ApplyPrimFunDetail (..),
+  PushLetDetail (..),
   -- Only exported for testing
   Cxt (Cxt),
   singletonCxt,
-  getNonCapturedLocal,
+  lookupEnclosingLet,
   tryReduceExpr,
   tryReduceType,
   findNodeByID,
@@ -49,10 +52,11 @@ import Primer.Eval.Detail (
   GlobalVarInlineDetail (..),
   LetRemovalDetail (..),
   LocalVarInlineDetail (..),
+  PushLetDetail (..),
  )
 import Primer.Eval.EvalError (EvalError (..))
 import Primer.Eval.NormalOrder (
-  FMExpr (FMExpr, expr, subst, substTy, ty),
+  FMExpr (FMExpr, expr, ty),
   foldMapExpr,
   singletonCxt,
  )
@@ -61,11 +65,11 @@ import Primer.Eval.Redex (
   Dir (..),
   EvalLog (..),
   MonadEval,
-  getNonCapturedLocal,
+  lookupEnclosingLet,
   runRedex,
   runRedexTy,
   viewRedex,
-  viewRedexType,
+  viewRedexType, RunRedexOptions (RunRedexOptions,pushAndElide), ViewRedexOptions (ViewRedexOptions,aggressiveElision, pushMulti),
  )
 import Primer.Log (ConvertLogMessage)
 import Primer.TypeDef (TypeDefMap)
@@ -101,8 +105,8 @@ step tydefs globals expr d i = runExceptT $ do
       pure (expr', detail)
 
 -- | Search for the given node by its ID.
--- Collect all local bindings in scope and return them
--- (with their local definition, if applicable)
+-- Collect all immediately-surrounding let bindings and return them
+-- (these are the ones we may push into this node)
 -- along with the focused node.
 -- Returns Nothing if the node is a binding, (note that no reduction rules can apply there).
 findNodeByID :: ID -> Dir -> Expr -> Maybe (Cxt, Either (Dir, ExprZ) TypeZ)
@@ -111,10 +115,14 @@ findNodeByID i =
     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
-      , subst = Nothing
-      , substTy = Nothing
       }
 
+-- We hardcode a permissive set of options for the interactive eval
+-- (i.e. these see more redexes)
+evalOpts :: ViewRedexOptions
+evalOpts = ViewRedexOptions {pushMulti = True
+  , aggressiveElision = True}
+
 -- | Return the IDs of nodes which are reducible.
 -- We assume that the expression is well scoped. There are no
 -- guarantees about whether we will claim that an ill-sorted variable
@@ -131,17 +139,19 @@ redexes tydefs globals =
   (ListT.toList .)
     . foldMapExpr
       FMExpr
-        { expr = \ez d -> liftMaybeT . runReaderT (getID ez <$ viewRedex tydefs globals d (target ez))
-        , ty = \tz -> runReader (whenJust (getID tz) <$> viewRedexType (target tz))
-        , subst = Nothing
-        , substTy = Nothing
+        { expr = \ez d -> liftMaybeT . runReaderT (getID ez <$ viewRedex evalOpts tydefs globals d (target ez))
+        , ty = \tz -> runReader (whenJust (getID tz) <$> viewRedexType evalOpts (target tz))
         }
   where
     liftMaybeT :: Monad m' => MaybeT m' a -> ListT m' a
     liftMaybeT m = ListT $ fmap (,mempty) <$> runMaybeT m
     -- whenJust :: Alternative f => a -> Maybe b -> f a
     whenJust = maybe empty . const . pure
 
+-- We hardcode a particular set of reduction options for the interactive evaluator
+reductionOpts :: RunRedexOptions
+reductionOpts = RunRedexOptions {pushAndElide = True}
+
 -- | Given a context of local and global variables and an expression, try to reduce that expression.
 -- Expects that the expression is redex and will throw an error if not.
 tryReduceExpr ::
@@ -154,8 +164,8 @@ tryReduceExpr ::
   Expr ->
   m (Expr, EvalDetail)
 tryReduceExpr tydefs globals cxt dir expr =
-  runMaybeT (flip runReaderT cxt $ viewRedex tydefs globals dir expr) >>= \case
-    Just r -> runRedex r
+  runMaybeT (flip runReaderT cxt $ viewRedex evalOpts tydefs globals dir expr) >>= \case
+    Just r -> runRedex reductionOpts r
     _ -> throwError NotRedex
 
 tryReduceType ::
@@ -167,6 +177,6 @@ tryReduceType ::
   Type ->
   m (Type, EvalDetail)
 tryReduceType _globals cxt =
-  flip runReader cxt . viewRedexType <&> \case
-    Just r -> runRedexTy r
+  flip runReader cxt . viewRedexType evalOpts <&> \case
+    Just r -> runRedexTy reductionOpts r
     _ -> throwError NotRedex

primer/src/Primer/Eval/Detail.hs

@@ -9,6 +9,7 @@ module Primer.Eval.Detail (
   module Case,
   module Let,
   module Prim,
+  module Push,
 ) where
 
 import Foreword
@@ -23,6 +24,7 @@ import Primer.Eval.Case as Case
 import Primer.Eval.Inline as Inline
 import Primer.Eval.Let as Let
 import Primer.Eval.Prim as Prim
+import Primer.Eval.Push as Push
 import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON)
 
 -- | Detailed information about a reduction step
@@ -41,6 +43,9 @@ data EvalDetail
     LetRemoval (LetRemovalDetail Expr)
   | -- | Removing a type-level @let@ whose bound variable is unused
     TLetRemoval (LetRemovalDetail Type)
+  | -- | Explicit-substitution style pushing a 'let' down the tree
+    PushLetDown (PushLetDetail Expr)
+  | PushLetDownTy (PushLetDetail Type)
   | -- | Renaming of binding in an expression
     BindRename (BindRenameDetail Expr)
   | -- | Renaming of binding in a type

primer/src/Primer/Eval/Let.hs

@@ -2,23 +2,13 @@
 
 module Primer.Eval.Let (
   LetRemovalDetail (..),
-  findFreeOccurrencesExpr,
-  findFreeOccurrencesType,
 ) where
 
 import Foreword
 
-import Control.Arrow ((***))
-import Optics (filtered, getting, to, (%), (^..), _1)
 import Primer.Core (
-  Expr,
   ID,
-  LocalName (unLocalName),
-  TyVarName,
-  Type,
-  getID,
  )
-import Primer.Core.Utils (_freeVars, _freeVarsTy)
 import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON)
 import Primer.Name (Name)
 
@@ -32,20 +22,12 @@ data LetRemovalDetail t = LetRemovalDetail
   -- ^ the let expression before reduction
   , after :: t
   -- ^ the resulting expression after reduction
-  , bindingName :: Name
-  -- ^ the name of the unused bound variable (either term or type variable)
-  , letID :: ID
-  -- ^ the full let expression
+  , bindingNames :: NonEmpty Name
+  -- ^ the names of the unused bound variables (either term or type variable)
+  , letIDs :: NonEmpty ID
+  -- ^ the dropped let expressions
   , bodyID :: ID
   -- ^ the right hand side of the let
   }
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON (LetRemovalDetail t)
-
-findFreeOccurrencesExpr :: LocalName k -> Expr -> [ID]
-findFreeOccurrencesExpr x e = e ^.. _freeVars % to idName % filtered ((== unLocalName x) . snd) % _1
-  where
-    idName = either (getID *** unLocalName) (getID *** unLocalName)
-
-findFreeOccurrencesType :: TyVarName -> Type -> [ID]
-findFreeOccurrencesType x ty = ty ^.. getting _freeVarsTy % to (first getID) % filtered ((== x) . snd) % _1