diff --git a/primer-benchmark/src/Benchmarks.hs b/primer-benchmark/src/Benchmarks.hs index 9ec3168c3..d0b6100e0 100644 --- a/primer-benchmark/src/Benchmarks.hs +++ b/primer-benchmark/src/Benchmarks.hs @@ -20,6 +20,10 @@ import Primer.App ( tcWholeProgWithImports, ) import Primer.App.Utils (forgetProgTypecache) +import Primer.Eval ( + RunRedexOptions (RunRedexOptions, pushAndElide), + ViewRedexOptions (ViewRedexOptions, aggressiveElision, groupedLets), + ) import Primer.EvalFull ( Dir (Syn), EvalLog, @@ -98,14 +102,16 @@ benchmarks = ] ] where + evalOptionsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} + evalOptionsR = RunRedexOptions{pushAndElide = True} evalTestMPureLogs e maxEvals = evalTestM (maxID e) $ runPureLogT $ - evalFull @EvalLog builtinTypes (defMap e) maxEvals Syn (expr e) + evalFull @EvalLog evalOptionsV evalOptionsR 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 evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) benchExpected f g e n b = EnvBench e n $ \e' -> NF diff --git a/primer/primer.cabal b/primer/primer.cabal index 49298582f..21610db38 100644 --- a/primer/primer.cabal +++ b/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 diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index d40356f79..2f6d2a972 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -185,7 +185,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, groupedLets)) import Primer.EvalFull (Dir (Syn), EvalFullError (TimedOut), TerminationBound, evalFull) import Primer.JSON import Primer.Log (ConvertLogMessage) @@ -596,7 +596,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{groupedLets = 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 diff --git a/primer/src/Primer/Eval.hs b/primer/src/Primer/Eval.hs index 40ae50a28..23b0409c7 100644 --- a/primer/src/Primer/Eval.hs +++ b/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,7 +65,9 @@ import Primer.Eval.Redex ( Dir (..), EvalLog (..), MonadEval, - getNonCapturedLocal, + RunRedexOptions (RunRedexOptions, pushAndElide), + ViewRedexOptions (ViewRedexOptions, aggressiveElision, groupedLets), + lookupEnclosingLet, runRedex, runRedexTy, viewRedex, @@ -101,8 +107,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 +117,17 @@ 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 + { groupedLets = 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,10 +144,8 @@ 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 @@ -142,6 +153,18 @@ redexes tydefs globals = -- 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 + { -- For intearctive use, we think combining these two steps is too confusing. + -- The choice of hardcoding this makes this feature slightly harder to test, + -- see https://github.com/hackworthltd/primer/pull/736#discussion_r1293290757 + -- for some tests that we would like to have added, if it were simple to test + -- a single step of pushAndElide. + pushAndElide = False + } + -- | 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 +177,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 +190,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 diff --git a/primer/src/Primer/Eval/Detail.hs b/primer/src/Primer/Eval/Detail.hs index db57ff522..f10533257 100644 --- a/primer/src/Primer/Eval/Detail.hs +++ b/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 diff --git a/primer/src/Primer/Eval/Let.hs b/primer/src/Primer/Eval/Let.hs index 44ba839c6..b4b68526a 100644 --- a/primer/src/Primer/Eval/Let.hs +++ b/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 diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs index 0a196e99b..1291fdb5d 100644 --- a/primer/src/Primer/Eval/NormalOrder.hs +++ b/primer/src/Primer/Eval/NormalOrder.hs @@ -1,5 +1,4 @@ {-# LANGUAGE DisambiguateRecordFields #-} -{-# LANGUAGE OverloadedLabels #-} {-# LANGUAGE OverloadedRecordDot #-} module Primer.Eval.NormalOrder ( @@ -12,31 +11,9 @@ module Primer.Eval.NormalOrder ( ) where import Foreword hiding (hoistAccum) -import Foreword qualified import Control.Monad.Log (MonadLog, WithSeverity) -import Control.Monad.Morph (generalize) -import Control.Monad.Trans.Accum ( - Accum, - AccumT, - add, - evalAccumT, - execAccum, - look, - readerToAccumT, - ) import Control.Monad.Trans.Maybe (MaybeT) -import Data.Map qualified as M -import Data.Set qualified as S -import Data.Set.Optics (setOf) -import Optics ( - elemOf, - folded, - getting, - to, - (%), - _2, - ) import Primer.Core ( Expr, Expr' ( @@ -48,18 +25,9 @@ import Primer.Core ( LetType, Letrec ), - HasID, - LocalName (unLocalName), - TyVarName, - Type, Type' ( TLet ), - bindName, - getID, - ) -import Primer.Core.Utils ( - _freeVarsTy, ) import Primer.Def ( DefMap, @@ -68,35 +36,14 @@ import Primer.Eval.Redex ( Cxt (..), Dir (..), EvalLog, - Redex ( - ElideLet, - InlineLet, - InlineLetrec, - RenameBindingsCase, - RenameBindingsLAM, - RenameBindingsLam, - RenameSelfLet, - RenameSelfLetType, - branches, - letBinding, - tyvar, - var - ), - RedexType ( - ElideLetInType, - InlineLetInType, - RenameForall, - RenameSelfLetInType, - letBinding, - origBinder, - var - ), + Redex, + RedexType, + ViewRedexOptions, + cxtAddLet, viewRedex, viewRedexType, - _freeVarsLetBinding, ) import Primer.Log (ConvertLogMessage) -import Primer.Name (Name) import Primer.TypeDef ( TypeDefMap, ) @@ -109,16 +56,11 @@ import Primer.Zipper ( down, focus, focusType, - getBoundHere, - getBoundHere', - getBoundHereTy, - letBindingName, right, target, ) import Primer.Zipper.Type ( LetTypeBinding' (LetTypeBind), - getBoundHereTy', ) -- We don't really want a zipper here, but a one-hole context, but it is easier @@ -128,17 +70,31 @@ data RedexWithContext = RExpr ExprZ Redex | RType TypeZ RedexType -viewLet :: (Dir, ExprZ) -> Maybe (LetBinding, Accum Cxt (Dir, ExprZ)) +data ViewLet = ViewLet + { bindingVL :: LetBinding + -- ^ the binding itself + , bodyVL :: (Dir, ExprZ) + -- ^ the body (i.e. after the `in`) + , typeChildrenVL :: [TypeZ] + -- ^ any non-body type children + , termChildrenVL :: [(Dir, ExprZ)] + -- ^ 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 - (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) + (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 []) _ -> Nothing + where + tz :: [TypeZ] + tz = maybeToList $ focusType ez -- | 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) -- - We keep track of context and directionality (necessitating an extra 'Dir' argument, for "what directional context this whole expression is in") +-- (the "context" is just of the immediately-enclosing lets, which are the only ones that may "cross a binder") -- - We handle @let@s specially, since we need to handle them differently when finding the normal order redex. -- (When we hit the body of a @let@ (of any flavor), we use the provided 'subst' or 'substTy' argument, if provided, and do no further recursion. -- If the corresponding argument is 'Nothing', then we recurse as normal.) @@ -152,149 +108,69 @@ viewLet dez@(_, ez) = case (target ez, exprChildren dez) of -- 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 +foldMapExpr extract topDir = go mempty . (topDir,) . focus where - go :: (Dir, ExprZ) -> AccumT Cxt f a - go dez@(d, ez) = - readerToAccumT (ReaderT $ extract.expr ez d) - <|> case (extract.subst, viewLet dez) of - (Just goSubst, Just (l, bz)) -> (readerToAccumT . ReaderT . (\(d', b) -> goSubst l b d')) =<< hoistAccum bz + go :: Cxt -> (Dir, ExprZ) -> f a + go lets dez@(d, ez) = + extract.expr ez d lets + <|> case viewLet dez of + -- Prefer to compute inside the body of a let, but otherwise compute in the binding + -- NB: we never push lets into lets, so the Cxt is reset for non-body children + Just (ViewLet{bindingVL, bodyVL, typeChildrenVL, termChildrenVL}) -> + msum $ + go (cxtAddLet bindingVL lets) bodyVL + : map (goType mempty) typeChildrenVL + <> map (go mempty) termChildrenVL -- Since stuck things other than lets are stuck on the first child or -- its type annotation, we can handle them all uniformly + -- Since this node is not a let, the context is reset _ -> msum $ - (goType =<< focusType' ez) - : map (go <=< hoistAccum) (exprChildren dez) - goType :: TypeZ -> AccumT Cxt f a - goType tz = - readerToAccumT (ReaderT $ extract.ty tz) - <|> case (extract.substTy, target tz) of - (Just goSubstTy, TLet _ a t _body) - | [_, bz] <- typeChildren tz -> (readerToAccumT . ReaderT . goSubstTy a t) =<< hoistAccum bz - _ -> msum $ map (goType <=< hoistAccum) $ typeChildren tz + (goType mempty =<< focusType' ez) + : map (go mempty) (exprChildren 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 data FMExpr m = FMExpr { expr :: ExprZ -> Dir -> Cxt -> m , ty :: TypeZ -> Cxt -> m - , subst :: Maybe (LetBinding -> ExprZ {- The body of the let-} -> Dir -> Cxt -> m) - , substTy :: Maybe (TyVarName -> Type -> TypeZ -> Cxt -> m) } -focusType' :: MonadPlus m => ExprZ -> AccumT Cxt m TypeZ --- Note that nothing in Expr binds a variable which scopes over a type child --- so we don't need to 'add' anything +focusType' :: MonadPlus m => ExprZ -> m TypeZ focusType' = maybe empty pure . focusType -hoistAccum :: Monad m => Accum Cxt b -> AccumT Cxt m b -hoistAccum = Foreword.hoistAccum generalize - -- We find the normal-order redex. --- Annoyingly this is not quite leftmost-outermost wrt our Expr type, as we --- are using 'let's to encode something similar to explicit substitution, and --- reduce them by substituting one occurrance at a time, removing the 'let' --- when there are no more substitutions to be done. Note that the 'let' itself --- doesn't get "pushed down" in the tree. --- example: --- lettype a = Bool -> Bool in (λx.not x : a) True --- reduces to --- lettype a = Bool -> Bool in (λx.not x : Bool -> Bool) True --- and then to --- (λx.not x : Bool -> Bool) True --- This can be seen as "leftmost-outermost" if you consider the location of the --- "expand a" redex to be the 'lettype' rather than the variable occurrance. findRedex :: forall l m. (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) => + ViewRedexOptions -> TypeDefMap -> DefMap -> Dir -> Expr -> MaybeT m RedexWithContext -findRedex tydefs globals = +findRedex opts tydefs globals = foldMapExpr ( FMExpr - { expr = \ez d -> runReaderT (RExpr ez <$> viewRedex tydefs globals d (target ez)) - , ty = \tz -> hoistMaybe . runReader (RType tz <<$>> viewRedexType (target tz)) - , subst = Just (\l -> fmap evalAccumT . goSubst l) - , substTy = Just (\v t -> fmap hoistMaybe . evalAccumT . goSubstTy v t) + { expr = \ez d -> runReaderT (RExpr ez <$> viewRedex opts tydefs globals d (target ez)) + , ty = \tz -> hoistMaybe . runReader (RType tz <<$>> viewRedexType opts (target tz)) } ) - where - goSubst :: LetBinding -> ExprZ -> Dir -> AccumT Cxt (MaybeT m) RedexWithContext - goSubst l ez d = do - let here = - readerToAccumT (viewRedex tydefs globals d $ target ez) >>= \case - -- We should inline such 'v' (note that we will not go under any 'v' binders) - r@(InlineLet{var}) | letBindingName l == unLocalName var -> pure $ RExpr ez r - r@(InlineLetrec{var}) | letBindingName l == unLocalName var -> pure $ RExpr ez r - -- Elide a let only if it blocks the reduction - r@(ElideLet{letBinding}) | elemOf _freeVarsLetBinding (letBindingName letBinding) l -> pure $ RExpr ez r - -- Rename a binder only if it blocks the reduction - r@(RenameBindingsLam{var}) | elemOf _freeVarsLetBinding (unLocalName var) l -> pure $ RExpr ez r - r@(RenameBindingsLAM{tyvar}) | elemOf _freeVarsLetBinding (unLocalName tyvar) l -> pure $ RExpr ez r - r@(RenameBindingsCase{branches}) - | not $ S.disjoint (setOf _freeVarsLetBinding l) (setOf (folded % #_CaseBranch % _2 % folded % to bindName % to unLocalName) branches) -> - pure $ RExpr ez r - r@(RenameSelfLet{var}) | elemOf _freeVarsLetBinding (unLocalName var) l -> pure $ RExpr ez r - r@(RenameSelfLetType{tyvar}) | elemOf _freeVarsLetBinding (unLocalName tyvar) l -> pure $ RExpr ez r - _ -> mzero - -- Switch to an inner let if substituting under it would cause capture - innerLet = case viewLet (d, ez) of - Just (l', bz) - | letBindingName l' /= letBindingName l - , elemOf _freeVarsLetBinding (letBindingName l') l -> - (\(d', b) -> goSubst l' b d') =<< hoistAccum bz - _ -> mzero - dive = - let substChild (d', c) = do - -- We should not go under 'v' binders, but otherwise substitute in each child - guard $ S.notMember (letBindingName l) $ getBoundHere (target ez) (Just $ target c) - goSubst l c d' - substTyChild c = case l of - LetTyBind (LetTypeBind v t) -> goSubstTy v t c - _ -> mzero - in msum @[] $ - Foreword.hoistAccum hoistMaybe (substTyChild =<< focusType' ez) - : map (substChild <=< hoistAccum) (exprChildren (d, ez)) - in here <|> innerLet <|> dive - goSubstTy :: TyVarName -> Type -> TypeZ -> AccumT Cxt Maybe RedexWithContext - goSubstTy v t tz = - let isFreeIn = elemOf (getting _freeVarsTy % _2) - in do - hoistAccum (readerToAccumT $ viewRedexType $ target tz) >>= \case - -- We should inline such 'v' (note that we will not go under any 'v' binders) - Just r@(InlineLetInType{var}) | var == v -> pure $ RType tz r - -- Elide a let only if it blocks the reduction - Just r@(ElideLetInType{letBinding = (LetTypeBind w _)}) | w `isFreeIn` t -> pure $ RType tz r - -- Rename a binder only if it blocks the reduction - Just r@(RenameSelfLetInType{letBinding = (LetTypeBind w _)}) | w `isFreeIn` t -> pure $ RType tz r - Just r@(RenameForall{origBinder}) | origBinder `isFreeIn` t -> pure $ RType tz r - -- We switch to an inner let if substituting under it would cause capture - Nothing - | TLet _ w s _ <- target tz - , [_, bz] <- typeChildren tz - , v /= w - , w `isFreeIn` t -> - goSubstTy w s =<< hoistAccum bz - -- We should not go under 'v' binders, but otherwise substitute in each child - _ -> - let substChild c = do - guard $ - S.notMember (unLocalName v) $ - S.map unLocalName $ - getBoundHereTy (target tz) (Just $ target c) - goSubstTy v t c - in msum $ map (substChild <=< hoistAccum) (typeChildren tz) children' :: IsZipper za a => za -> [za] 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 :: (Dir, ExprZ) -> [(Dir, ExprZ)] exprChildren (d, ez) = children' ez <&> \c -> do - let bs = getBoundHere' (target ez) (Just $ target c) let d' = case target ez of App _ f _ | f == target c -> Syn APP _ f _ | f == target c -> Syn @@ -310,26 +186,10 @@ exprChildren (d, ez) = | e == target c -> Chk | otherwise -> d _ -> Chk - addBinds ez bs - pure (d', c) - -typeChildren :: TypeZ -> [Accum Cxt TypeZ] -typeChildren tz = - children' tz <&> \c -> do - let bs = getBoundHereTy' (target tz) (Just $ target c) - addBinds tz $ bimap unLocalName LetTyBind <$> bs - pure c + (d', c) -addBinds :: HasID i => i -> [Either Name LetBinding] -> Accum Cxt () -addBinds i' bs = do - let i = getID i' - cxt <- look - add $ - Cxt $ - M.fromList $ - bs <&> \case - Left n -> (n, (Nothing, i, cxt)) - Right l -> (letBindingName l, (Just l, i, cxt)) +typeChildren :: TypeZ -> [TypeZ] +typeChildren = children' -singletonCxt :: HasID i => i -> LetBinding -> Cxt -singletonCxt i l = addBinds i [Right l] `execAccum` mempty +singletonCxt :: LetBinding -> Cxt +singletonCxt l = Cxt [l] diff --git a/primer/src/Primer/Eval/Push.hs b/primer/src/Primer/Eval/Push.hs new file mode 100644 index 000000000..ec4d46d34 --- /dev/null +++ b/primer/src/Primer/Eval/Push.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE DuplicateRecordFields #-} + +module Primer.Eval.Push (PushLetDetail (..)) where + +import Foreword + +import Primer.Core.Meta (ID) +import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON) +import Primer.Name (Name) + +-- | Detailed information about pushing a group of 'let's down the tree +-- This each can be any of: a term-level non-recursive let, a +-- term-level recursive let, a term-level let binding a type +-- or a type-level let. +-- If term-level: t ~ Expr; if type-level: t ~ Type +data PushLetDetail t = PushLetDetail + { before :: t + -- ^ the expression before reduction + , after :: t + -- ^ the resulting expression after reduction + , letIDs :: [ID] + -- ^ the 'ID' of each original let + , letBindingNames :: [Name] + -- ^ the names of the variables bound by the @let@s + , intoID :: ID + -- ^ the 'ID' of the term we push into + } + deriving stock (Eq, Show, Read, Generic) + deriving (FromJSON, ToJSON) via PrimerJSON (PushLetDetail t) diff --git a/primer/src/Primer/Eval/Redex.hs b/primer/src/Primer/Eval/Redex.hs index 769902afe..bb07e910d 100644 --- a/primer/src/Primer/Eval/Redex.hs +++ b/primer/src/Primer/Eval/Redex.hs @@ -1,52 +1,55 @@ {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE NoFieldSelectors #-} module Primer.Eval.Redex ( Redex (..), viewRedex, + ViewRedexOptions (..), + RunRedexOptions (..), runRedex, RedexType (..), viewRedexType, runRedexTy, Dir (Syn, Chk), Cxt (Cxt), + cxtAddLet, _freeVarsLetBinding, EvalLog (..), MonadEval, -- Exported for testing - getNonCapturedLocal, + lookupEnclosingLet, ) where import Foreword import Control.Monad.Fresh (MonadFresh) import Control.Monad.Log (MonadLog, WithSeverity) -import Control.Monad.Trans.Maybe (MaybeT (runMaybeT)) +import Control.Monad.Trans.Maybe (MaybeT) import Data.Data (Data) +import Data.Generics.Uniplate.Data (children, descendM) import Data.List (zip3) import Data.Map qualified as M import Data.Set qualified as S import Data.Set.Optics (setOf) -import Data.Tuple.Extra (snd3) import GHC.Err (error) import Optics ( AffineFold, Fold, afolding, - allOf, - elemOf, + folded, getting, ifiltered, isnd, - notElemOf, summing, to, + traverseOf, (%), (<%), _1, _2, - _Just, ) import Primer.Core ( Bind, @@ -93,6 +96,7 @@ import Primer.Core ( bindName, caseBranchName, getID, + typesInExpr, ) import Primer.Core.DSL (ann, letType, let_, letrec, lvar, tlet, tvar) import Primer.Core.Transform (decomposeTAppCon) @@ -132,6 +136,8 @@ import Primer.Eval.Detail ( LetRemoval, LocalTypeVarInline, LocalVarInline, + PushLetDown, + PushLetDownTy, RemoveAnn, TBindRename, TLetRemoval @@ -139,9 +145,8 @@ import Primer.Eval.Detail ( GlobalVarInlineDetail (GlobalVarInlineDetail), LetRemovalDetail (LetRemovalDetail), LocalVarInlineDetail (LocalVarInlineDetail), + PushLetDetail (PushLetDetail), RemoveAnnDetail (RemoveAnnDetail), - findFreeOccurrencesExpr, - findFreeOccurrencesType, ) import Primer.Eval.Detail qualified import Primer.Eval.Prim (tryPrimFun) @@ -168,8 +173,32 @@ import Primer.Zipper ( import Primer.Zipper.Type ( LetTypeBinding, LetTypeBinding' (LetTypeBind), + getBoundHereDnTy, + letTypeBindingName, ) +data ViewRedexOptions = ViewRedexOptions + { groupedLets :: Bool + -- ^ Whether to treat all adjacent let bindings as a group. E.g. in + -- @let x=e1 in let y=e2 in C s t@, we would take one step to push + -- both @x@ and @y@ under the constructor (rather than one step + -- for @y@ and then a second for @x@). + , aggressiveElision :: Bool + -- ^ Whether to elide as early as possible (@True@), or wait until the + -- body of a @let@ is a leaf (and thus the @let@ cannot be pushed + -- down) (@False@). E.g. in @let x=e in C s t@ (where @s@ and @t@ + -- do not refer to @x@) whether we reduce to @C s t@ or + -- @C (let x = e in s) (let x = e in t)@. + } + +newtype RunRedexOptions = RunRedexOptions + { pushAndElide :: Bool + -- ^ Whether to push @let@s into branches they are not used in. + -- E.g. in @let x=e in C x t@ where @t@ does not refer to @x@, whether + -- (@True@) to reduce to @C (let x=e in x) t@ or to also push the @x@ + -- into the @t@ branch (@False@). + } + data EvalLog = -- | Found something that may have been a case redex, -- but the scrutinee's head is an out-of-scope constructor. @@ -213,7 +242,7 @@ data Redex , def :: ASTDef -- ^ What is its definition } - | -- x ~> e where we are inside the scope of a let x = e in ... + | -- let x = e in x ~> e InlineLet { var :: LVarName -- ^ What variable are we inlining @@ -224,7 +253,7 @@ data Redex , varID :: ID -- ^ Where was the occurrence (used for details) } - | -- x ~> letrec x:T=t in t:T where we are inside the scope of a letrec x : T = t in ... + | -- letrec x = t : T in x ~> letrec x = t : T in t : T InlineLetrec { var :: LVarName -- ^ What variable are we inlining @@ -237,12 +266,33 @@ data Redex , varID :: ID -- ^ Where was the occurrence (used for details) } + | -- let x = e in f s ~> (let x = e in f) (let x = e in s) etc + -- [for any non-leaf @f s@ which neither binds @x@ (else we should elide) + -- nor any free variable of @e@ (to avoid capture)] + -- [We actually do this rule for a whole sequence of let bindings at once] + -- [If we push into an annotation, we drop term variables: let x = e in (t : T) ~> (let x = e in t) : T] + -- [We actually drop all "pointless" variables: + -- let x = e in f s ~> (let x = e in f) (let x = e in s) if @x@ is free in @f@, and free in @s@ + -- let x = e in f s ~> f (let x = e in s) if @x@ is not free in @f@, but free in @s@ + -- let x = e in f s ~> (let x = e in f) s if @x@ is free in @f@, but not free in @s@ + -- let x = e in f s ~> f s if @x@ is not free in @f@, and not free in @s@ + PushLet + { bindings :: NonEmpty (ID, LetBinding) + -- ^ The bindings we push + , expr :: Expr + -- ^ The expression we are pushing into, i.e. the original body of the above bindings + , orig :: Expr + -- ^ the original expression (used for details) + } | -- let(rec/type) x = e in t ~> t if x does not appear in t + -- [We actually elide from a whole sequence of let bindings at once] ElideLet - { letBinding :: LetBinding - -- ^ Original binding + { letBindingsKeep :: [(ExprMeta, LetBinding)] + -- ^ Subset of bindings to keep + , letBindingsDrop :: NonEmpty (ID, LetBinding) + -- ^ Subset of bindings to drop , body :: Expr - -- ^ Body, in which the bound var does not occur + -- ^ Body, in which the elided variables do not occur , orig :: Expr -- ^ the original let (used for details) } @@ -371,31 +421,6 @@ data Redex , orig :: Expr -- ^ The original redex (used for details) } - | -- let x = f x in g x x ~> let y = f x in let x = y in g x x - -- Note that we cannot substitute the let in the initial term, since - -- we only substitute one occurence at a time, and the 'let' would capture the 'x' - -- in the expansion if we did a substitution. - RenameSelfLet - { var :: LVarName - -- ^ The bound variable - , rhs :: Expr - -- ^ The local definition of @var@ - , body :: Expr - -- ^ The body of the @let@, in which @var@ can occur free - , orig :: Expr - -- ^ The original redex (used for details) - } - | -- As RenameSelfLet, but for LetType. (Note that it is unnecessary for letrec.) - RenameSelfLetType - { tyvar :: TyVarName - -- ^ The bound variable - , trhs :: Type - -- ^ The local definition of @var@ - , body :: Expr - -- ^ The body of the @let_type@, in which @var@ can occur free - , orig :: Expr - -- ^ The original redex (used for details) - } | ApplyPrimFun { result :: forall m. MonadFresh ID m => m Expr -- ^ The result of the applied primitive function @@ -408,7 +433,8 @@ data Redex } data RedexType - = InlineLetInType + = -- let a = t in a ~> t + InlineLetInType { var :: TyVarName -- ^ What variable are we inlining (used for finding normal-order redex) , ty :: Type @@ -418,27 +444,28 @@ data RedexType , varID :: ID -- ^ Where was the occurrence (used for details) } + | -- let a = s in t1 t2 ~> (let a = s in t1) (let a = s in t2) etc + -- (see notes on the analogous rule for Redex) + PushLetType + { bindings :: NonEmpty (ID, LetTypeBinding) + -- ^ what bindings we are pushing (IDs used for details, bindings used for reduction) + , intoTy :: Type + -- ^ the type they are being pushed into (used for reduction) + , origTy :: Type + -- ^ what was the original ("let-outside") (used for details) + } | -- let a = s in t ~> t if a does not appear in t + -- [We actually elide from a whole sequence of let bindings at once] ElideLetInType - { letBinding :: LetTypeBinding - -- ^ original binding (name is used for finding normal-order redex; used for details) + { letBindingsKeep :: [(TypeMeta, LetTypeBinding)] + -- ^ Subset of bindings to keep + , letBindingsDrop :: NonEmpty (ID, LetTypeBinding) + -- ^ Subset of bindings to drop , body :: Type - -- ^ Body, in which the bound var does not occur (used for reduction) + -- ^ Body, in which the elided variables do not occur , orig :: Type -- ^ the original let (used for details) } - | -- let a = s a in t a a ~> let b = s a in let a = b in t a a - -- Note that we cannot substitute the let in the initial term, since - -- we only substitute one occurence at a time, and the 'let' would capture the 'a' - -- in the expansion if we did a substitution. - RenameSelfLetInType - { letBinding :: LetTypeBinding - -- ^ binding (name is used for finding normal-order redex; used for reduction) - , body :: Type - -- ^ body, in which th e bound var may occur (used for reduction) - , orig :: Type - -- ^ the original let (used for details) - } | -- ∀a:k.t ~> ∀b:k. let a = b in t for fresh b, avoiding the given set RenameForall { meta :: TypeMeta @@ -480,9 +507,6 @@ _freeVarsTy' = getting _freeVarsTy % _2 % to unLocalName _freeVarsLetBinding :: Fold LetBinding Name _freeVarsLetBinding = (_LetBind % _2 % _freeVars') - -- Since letrec bound variables expand with a local letrec, - -- we don't consider the recursively-bound variable free - -- (since it will not be in the inlining) `summing` ( _LetrecBind <% ( to (\(a, b, c) -> (a, (b, c))) % isnd @@ -490,7 +514,10 @@ _freeVarsLetBinding = & ifiltered ((/=) . unLocalName) ) ) - `summing` (_LetTyBind % _LetTypeBind % _2 % _freeVarsTy') + `summing` (_LetTyBind % _freeVarsLetTypeBinding % to unLocalName) + +_freeVarsLetTypeBinding :: Fold LetTypeBinding TyVarName +_freeVarsLetTypeBinding = _LetTypeBind % _2 % getting _freeVarsTy % _2 data Dir = Syn | Chk deriving stock (Eq, Show, Read, Generic) @@ -608,24 +635,14 @@ viewCaseRedex tydefs = \case formCaseRedex con argTys params args binders rhs (orig, scrut, conID) = CaseRedex{con, args, argTys, params, binders, rhs, orig, scrutID = getID scrut, conID} --- We record each binder, along with its let-bound RHS (if any) --- and its original binding location and context (to be able to detect capture) --- Invariant: lookup x c == Just (Just l,_,_) ==> letBindingName l == x -newtype Cxt = Cxt (M.Map Name (Maybe LetBinding, ID, Cxt)) - -- We want right-biased mappend, as we will use this with 'Accum' - -- and want later 'add's to overwrite earlier (more-global) context entries - deriving (Semigroup, Monoid) via Dual (M.Map Name (Maybe LetBinding, ID, Cxt)) +-- We record each directly-enclosing let binding +-- By "directly enclosing" we mean "those which may be pushed into this term" +-- NB: we do not care about ordering +newtype Cxt = Cxt [LetBinding] + deriving newtype (Semigroup, Monoid) -lookup :: Name -> Cxt -> Maybe (Maybe LetBinding, ID, Cxt) -lookup n (Cxt cxt) = M.lookup n cxt - --- We only care about LLetType if we are looking up tyvars, --- as we assume that the input is well-typed, and the only things --- that tyvars can refer to are lettype, or foralls -lookupTy :: TyVarName -> Cxt -> Maybe (Maybe LetTypeBinding, ID, Cxt) -lookupTy n c = case lookup (unLocalName n) c of - Just (Just (LetTyBind b), i, c') -> Just (Just b, i, c') - _ -> Nothing +cxtAddLet :: LetBinding -> Cxt -> Cxt +cxtAddLet l (Cxt c) = Cxt $ l : c -- This notices all redexes -- Note that if a term is not a redex, but stuck on some sub-term, @@ -636,64 +653,92 @@ lookupTy n c = case lookup (unLocalName n) c of -- - stuck on expression under the type annotation in its left-most child viewRedex :: (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) => + ViewRedexOptions -> TypeDefMap -> DefMap -> Dir -> Expr -> ReaderT Cxt (MaybeT m) Redex -viewRedex tydefs globals dir = \case +viewRedex opts tydefs globals dir = \case orig@(Var _ (GlobalVarRef gvar)) | Just (DefAST def) <- gvar `M.lookup` globals -> pure $ InlineGlobal{gvar, def, orig} - Var m (LocalVarRef var) -> do - let varID = getID m - runMaybeT (getNonCapturedLocal var) >>= \x -> do - case x of - Just (letID, LetBind _ expr) -> pure $ InlineLet{var, expr, letID, varID} - Just (letID, LetrecBind _ expr ty) -> pure $ InlineLetrec{var, expr, ty, letID, varID} - _ -> mzero - orig@(Let _ var rhs body) - -- NB: we will recompute the freeVars set a lot (especially when doing EvalFull iterations) - -- This could be optimised in the future. See - -- https://github.com/hackworthltd/primer/issues/733 - | unLocalName var `S.notMember` freeVars body -> + Let mLet var rhs (Var mVar (LocalVarRef var')) + | var == var' -> pure $ - ElideLet - { letBinding = LetBind var rhs - , body + InlineLet + { var + , expr = rhs + , letID = getID mLet + , varID = getID mVar + } + Letrec mLet var rhs ty (Var mVar (LocalVarRef var')) + | var == var' -> + pure $ + InlineLetrec + { var + , expr = rhs + , ty + , letID = getID mLet + , varID = getID mVar + } + orig@(viewLets -> Just (letBinding1, expr', letBindings, body)) + | not opts.groupedLets + , not $ isLeaf expr' + , null letBindings + , n <- letBindingName $ snd letBinding1 + , not opts.aggressiveElision || n `S.member` freeVars expr' + , S.disjoint (getBoundHereDn expr') (setOf (_2 % (_freeVarsLetBinding `summing` to letBindingName)) letBinding1) -> + pure $ + PushLet + { bindings = pure $ first getID letBinding1 + , expr = expr' , orig } - | unLocalName var `S.member` freeVars rhs -> pure $ RenameSelfLet{var, rhs, body, orig} - | otherwise -> mzero - orig@(LetType _ var trhs body) - | unLocalName var `S.notMember` freeVars body -> + | opts.groupedLets + , not $ isLeaf body + , (_, unused) <- partitionLets (letBinding1 : letBindings) body + , not opts.aggressiveElision || null unused + , S.disjoint (getBoundHereDn body) (setOf (folded % _2 % (_freeVarsLetBinding `summing` to letBindingName)) $ letBinding1 : letBindings) -> + pure $ + PushLet + { bindings = first getID <$> letBinding1 :| letBindings + , expr = body + , orig + } + -- NB: we will recompute the freeVars set a lot (especially when doing EvalFull iterations) + -- This could be optimised in the future. See + -- https://github.com/hackworthltd/primer/issues/733 + | not opts.groupedLets + , letBindingName (snd letBinding1) `S.notMember` freeVars expr' + , opts.aggressiveElision || isLeaf expr' -> pure $ ElideLet - { letBinding = LetTyBind $ LetTypeBind var trhs - , body + { letBindingsDrop = pure $ first getID letBinding1 + , letBindingsKeep = mempty + , body = expr' , orig } - | var `S.member` freeVarsTy trhs -> pure $ RenameSelfLetType{tyvar = var, trhs, body, orig} - | otherwise -> mzero - orig@(Letrec _ v e1 t body) - | unLocalName v `S.notMember` freeVars body -> + | opts.groupedLets + , (letBindingsKeep, nonEmpty -> Just letBindingsDrop) <- partitionLets (letBinding1 : letBindings) body + , opts.aggressiveElision || isLeaf body -> pure $ ElideLet - { letBinding = LetrecBind v e1 t + { letBindingsDrop = first getID <$> letBindingsDrop + , letBindingsKeep , body , orig } - | otherwise -> mzero l@(Lam meta var body) -> do - fvcxt <- fvCxt $ freeVars l - if unLocalName var `S.member` fvcxt - then pure $ RenameBindingsLam{var, meta, body, avoid = fvcxt, orig = l} + avoid <- cxtToAvoid + if unLocalName var `S.member` avoid + then pure $ RenameBindingsLam{var, meta, body, avoid, orig = l} else mzero l@(LAM meta v body) -> do - fvcxt <- fvCxt $ freeVars l - if unLocalName v `S.member` fvcxt - then pure $ RenameBindingsLAM{tyvar = v, meta, body, avoid = fvcxt, orig = l} + avoid <- cxtToAvoid + if unLocalName v `S.member` avoid + then pure $ RenameBindingsLAM{tyvar = v, meta, body, avoid, orig = l} else mzero orig@(App _ (Ann _ (Lam m var body) (TFun _ srcTy tgtTy)) app) -> pure $ @@ -726,46 +771,132 @@ viewRedex tydefs globals dir = \case } APP{} -> mzero e@(Case meta scrutinee branches fallbackBranch) -> do - fvcxt <- fvCxt $ freeVars e + avoid <- cxtToAvoid -- TODO: we arbitrarily decide that renaming takes priority over reducing the case -- This is good for evalfull, but bad for interactive use. -- Maybe we want to offer both. See -- https://github.com/hackworthltd/primer/issues/734 - if getBoundHereDn e `S.disjoint` fvcxt + if getBoundHereDn e `S.disjoint` avoid then lift $ viewCaseRedex tydefs e - else pure $ RenameBindingsCase{meta, scrutinee, branches, fallbackBranch, avoid = fvcxt, orig = e} + else pure $ RenameBindingsCase{meta, scrutinee, branches, fallbackBranch, avoid, orig = e} orig@(Ann _ expr ty) | Chk <- dir, concreteTy ty -> pure $ Upsilon{expr, ann = ty, orig} _ -> mzero + where + isLeaf = null . children -viewRedexType :: Type -> Reader Cxt (Maybe RedexType) -viewRedexType = \case - TVar m var -> - runMaybeT (getNonCapturedLocal var) <&> \case - Just (letID, LetTyBind (LetTypeBind _ ty)) -> pure $ InlineLetInType{var, ty, letID, varID = getID m} +-- Decompose @let a = s in let b0 = t0 in ... let bn = tn in e@ +-- into @(LetBind a s, let b0=t0 in ... e, [LetBind b0 t0, ..., LetBind bn tn], e)@ +-- I.e. a combination of two views: first let & all lets. +-- Note that this decomposes lets of all flavors. +viewLets :: Expr -> Maybe ((ExprMeta, LetBinding), Expr, [(ExprMeta, LetBinding)], Expr) +viewLets e = do + (l1, e') <- viewLet e + let (ls, e'') = viewLets' e' + pure (l1, e', ls, e'') + where + -- Decompose multiple @let@s (of varying flavors) around a + -- non-let expression. + viewLets' :: Expr -> ([(ExprMeta, LetBinding)], Expr) + viewLets' t = case viewLet t of + Nothing -> ([], t) + Just (l, e') -> first (l :) $ viewLets' e' + -- Decompose one @let@ (of any flavor) + viewLet :: Expr -> Maybe ((ExprMeta, LetBinding), Expr) + viewLet = \case + Let m v t b -> Just ((m, LetBind v t), b) + Letrec m v t ty b -> Just ((m, LetrecBind v t ty), b) + LetType m a ty b -> Just ((m, LetTyBind (LetTypeBind a ty)), b) _ -> Nothing - orig@(TLet _ v s body) - -- NB: we will recompute the freeVars set a lot (especially when doing EvalFull iterations) - -- This could be optimised in the future. See - -- https://github.com/hackworthltd/primer/issues/733 - | notElemOf (getting _freeVarsTy % _2) v body -> + +foldLetBindings :: [(ExprMeta, LetBinding)] -> Expr -> Expr +foldLetBindings ls e = + foldr + ( \(m, l) e' -> case l of + LetBind v t -> Let m v t e' + LetrecBind v t ty -> Letrec m v t ty e' + LetTyBind (LetTypeBind v ty) -> LetType m v ty e' + ) + e + ls + +viewLetsTy :: Type -> Maybe ((TypeMeta, LetTypeBinding), Type, [(TypeMeta, LetTypeBinding)], Type) +viewLetsTy ty = do + (l1, ty') <- viewOne ty + let (ls, ty'') = viewLets' ty' + pure (l1, ty', ls, ty'') + where + viewOne = \case + TLet m a t b -> Just ((m, LetTypeBind a t), b) + _ -> Nothing + viewLets' t = case viewOne t of + Nothing -> ([], t) + Just (l, t') -> first (l :) $ viewLets' t' + +foldLetBindingsTy :: [(TypeMeta, LetTypeBinding)] -> Type -> Type +foldLetBindingsTy ls t = + foldr + (\(m, LetTypeBind v ty) t' -> TLet m v ty t') + t + ls + +viewRedexType :: ViewRedexOptions -> Type -> Reader Cxt (Maybe RedexType) +viewRedexType opts = \case + TLet mLet v s (TVar mVar var) + | v == var -> + purer $ + InlineLetInType + { var + , ty = s + , letID = getID mLet + , varID = getID mVar + } + orig@(viewLetsTy -> Just (letBinding1, ty', letBindings, body)) + | not opts.groupedLets + , not $ isLeaf ty' + , null letBindings + , not opts.aggressiveElision || letTypeBindingName' (snd letBinding1) `S.member` freeVarsTy ty' + , S.disjoint (getBoundHereDnTy ty') (setOf (_2 % (_freeVarsLetTypeBinding `summing` to letTypeBindingName')) letBinding1) -> + purer $ + PushLetType + { bindings = pure $ first getID letBinding1 + , intoTy = ty' + , origTy = orig + } + | opts.groupedLets + , not $ isLeaf body + , (_, unused) <- partitionLetsTy (letBinding1 : letBindings) body + , not opts.aggressiveElision || null unused + , S.disjoint (getBoundHereDnTy body) (setOf (folded % _2 % (_freeVarsLetTypeBinding `summing` to letTypeBindingName')) (letBinding1 : letBindings)) -> + purer $ + PushLetType + { bindings = first getID <$> letBinding1 :| letBindings + , intoTy = body + , origTy = orig + } + | not opts.groupedLets + , letTypeBindingName' (snd letBinding1) `S.notMember` freeVarsTy ty' + , opts.aggressiveElision || isLeaf ty' -> purer $ ElideLetInType - { letBinding = LetTypeBind v s - , body + { letBindingsDrop = pure $ first getID letBinding1 + , letBindingsKeep = mempty + , body = ty' , orig } - | elemOf (getting _freeVarsTy % _2) v s -> + | opts.groupedLets + , (letBindingsKeep, nonEmpty -> Just letBindingsDrop) <- partitionLetsTy (letBinding1 : letBindings) body + , opts.aggressiveElision || isLeaf body -> purer $ - RenameSelfLetInType - { letBinding = LetTypeBind v s + ElideLetInType + { letBindingsDrop = first getID <$> letBindingsDrop + , letBindingsKeep , body , orig } - | otherwise -> pure Nothing orig@(TForall meta origBinder kind body) -> do - fvcxt <- fvCxtTy $ freeVarsTy orig + avoid <- cxtToAvoidTy pure $ - if origBinder `S.member` fvcxt + if origBinder `S.member` avoid then pure $ -- If anything we may substitute would cause capture, we should rename this binder @@ -774,59 +905,50 @@ viewRedexType = \case , origBinder , kind , body - , avoid = fvcxt + , avoid , orig } else Nothing _ -> pure Nothing + where + isLeaf = null . children + letTypeBindingName' (LetTypeBind n _) = n --- Get the let-bound definition of this variable, if some such exists --- and is substitutible in the current context. (We also return the --- id of the binding site.) -getNonCapturedLocal :: MonadReader Cxt m => LocalName k -> MaybeT m (ID, LetBinding) -getNonCapturedLocal v = do - def <- asks (lookup $ unLocalName v) - curCxt <- ask - hoistMaybe $ do - (def', origID, origCxt) <- def - def'' <- def' - let uncaptured x = ((==) `on` fmap snd3 . lookup x) origCxt curCxt - if allOf _freeVarsLetBinding uncaptured def'' - then Just (origID, def'') - else Nothing +lookupEnclosingLet :: Name -> Cxt -> Maybe LetBinding +lookupEnclosingLet n (Cxt cxt) = find ((== n) . letBindingName) cxt --- What are the FVs of the RHS of these bindings? -fvCxt :: MonadReader Cxt m => S.Set Name -> m (S.Set Name) -fvCxt vs = do - cxt <- ask - pure $ foldMap' (setOf (_Just % _1 % _Just % _freeVarsLetBinding) . flip lookup cxt) vs +-- We may want to push some let bindings (the Cxt) under a +-- binder; what variable names must the binder avoid for this to be valid? +cxtToAvoid :: MonadReader Cxt m => m (S.Set Name) +cxtToAvoid = do + Cxt cxt <- ask + pure $ foldMap' (setOf (to letBindingName `summing` _freeVarsLetBinding)) cxt -fvCxtTy :: S.Set TyVarName -> Reader Cxt (S.Set TyVarName) -fvCxtTy vs = do - cxt <- ask - pure $ foldMap' (setOf (_Just % _1 % _Just % _LetTypeBind % _2 % getting _freeVarsTy % _2) . flip lookupTy cxt) vs +cxtToAvoidTy :: MonadReader Cxt m => m (S.Set TyVarName) +cxtToAvoidTy = do + Cxt cxt <- ask + pure $ foldMap' (setOf (_LetTyBind % _LetTypeBind % (_1 `summing` _2 % getting _freeVarsTy % _2))) cxt -- TODO: deal with metadata. https://github.com/hackworthltd/primer/issues/6 -runRedex :: forall l m. MonadEval l m => Redex -> m (Expr, EvalDetail) -runRedex = \case +runRedex :: forall l m. MonadEval l m => RunRedexOptions -> Redex -> m (Expr, EvalDetail) +runRedex opts = \case InlineGlobal{def, orig} -> do after <- ann (regenerateExprIDs $ astDefExpr def) (regenerateTypeIDs $ astDefType def) let details = GlobalVarInlineDetail{def, var = orig, after} pure (after, GlobalVarInline details) InlineLet{var, expr, letID, varID} -> do - expr' <- regenerateExprIDs expr let details = LocalVarInlineDetail { letID , varID , valueID = getID expr , bindingName = var - , replacementID = getID expr' + , replacementID = getID expr , isTypeVar = False } - pure (expr', LocalVarInline details) + pure (expr, LocalVarInline details) InlineLetrec{var, expr, ty, letID, varID} -> do - expr' <- letrec var (regenerateExprIDs expr) (regenerateTypeIDs ty) $ ann (regenerateExprIDs expr) (regenerateTypeIDs ty) + expr' <- letrec var (pure expr) (pure ty) $ ann (regenerateExprIDs expr) (regenerateTypeIDs ty) let details = LocalVarInlineDetail { letID @@ -837,19 +959,30 @@ runRedex = \case , isTypeVar = False } pure (expr', LocalVarInline details) - -- let(rec/type) x = e in t ~> t if e does not appear in t - ElideLet{body, letBinding, orig} -> do + PushLet{bindings, expr, orig} -> do + let binds = snd <$> bindings + expr' <- descendM (addLets opts binds) =<< traverseOf typesInExpr (addTLets opts binds) expr let details = + PushLetDetail + { before = orig + , after = expr' + , letIDs = toList $ fst <$> bindings + , letBindingNames = toList $ letBindingName <$> binds + , intoID = getID expr + } + pure (expr', PushLetDown details) + -- let(rec/type) x = e in t ~> t if e does not appear in t + ElideLet{body, letBindingsKeep, letBindingsDrop, orig} -> do + let expr = foldLetBindings letBindingsKeep body + details = LetRemovalDetail { before = orig - , after = body - , bindingName = letBindingName letBinding - , letID = getID orig + , after = expr + , bindingNames = letBindingName . snd <$> letBindingsDrop + , letIDs = fst <$> letBindingsDrop , bodyID = getID body } - - pure (body, LetRemoval details) - + pure (expr, LetRemoval details) -- (λx.t : S -> T) s ~> let x = s:S in t : T Beta{var, body, srcTy, tgtTy, app, orig, lamID} -> do expr' <- let_ var (pure app `ann` pure srcTy) (pure body) `ann` pure tgtTy @@ -1037,42 +1170,6 @@ runRedex = \case -- We should replace this with a proper exception. See: -- https://github.com/hackworthltd/primer/issues/148 | otherwise -> error "Internal Error: RenameBindingsCase found no applicable branches" - -- let x = f x in g x x ~> let y = f x in let x = y in g x x - RenameSelfLet{var, rhs, body, orig} -> do - y <- freshLocalName' (freeVars rhs <> freeVars body) - rl <- let_ var (lvar y) $ pure body - expr' <- let_ y (pure rhs) $ pure rl - let details = - BindRenameDetail - { before = orig - , after = expr' - , bindingNamesOld = [unLocalName var] - , bindingNamesNew = [unLocalName y] - , bindersOld = [getID orig] - , bindersNew = [getID expr'] - , bindingOccurrences = findFreeOccurrencesExpr var rhs - , renamingLets = [getID rl] - , bodyID = getID body - } - pure (expr', BindRename details) - -- As RenameSelfLet, but for LetType - RenameSelfLetType{tyvar, trhs, body, orig} -> do - b <- freshLocalName' (S.map unLocalName (freeVarsTy trhs) <> freeVars body) - rl <- letType tyvar (tvar b) $ pure body - expr' <- letType b (pure trhs) $ pure rl - let details = - BindRenameDetail - { before = orig - , after = expr' - , bindingNamesOld = [unLocalName tyvar] - , bindingNamesNew = [unLocalName b] - , bindersOld = [getID orig] - , bindersNew = [getID expr'] - , bindingOccurrences = findFreeOccurrencesType tyvar trhs - , renamingLets = [getID rl] - , bodyID = getID body - } - pure (expr', BindRename details) ApplyPrimFun{result, primFun, orig, args} -> do expr' <- result let details = @@ -1084,50 +1181,107 @@ runRedex = \case } pure (expr', Primer.Eval.Detail.ApplyPrimFun details) -runRedexTy :: MonadEval l m => RedexType -> m (Type, EvalDetail) -runRedexTy (InlineLetInType{ty, letID, varID, var}) = do - ty' <- regenerateTypeIDs ty +addLets :: MonadFresh ID m => RunRedexOptions -> NonEmpty LetBinding -> Expr -> m Expr +addLets opts ls expr = foldrM addLet expr $ if opts.pushAndElide then filterLets ls expr else toList ls + where + addLet :: MonadFresh ID m => LetBinding -> Expr -> m Expr + addLet (LetBind v e) b = let_ v (regenerateExprIDs e) (pure b) + addLet (LetrecBind v t ty) b = letrec v (regenerateExprIDs t) (regenerateTypeIDs ty) (pure b) + addLet (LetTyBind (LetTypeBind v ty)) b = letType v (regenerateTypeIDs ty) (pure b) + +addTLets :: MonadFresh ID m => RunRedexOptions -> NonEmpty LetBinding -> Type -> m Type +addTLets opts ls t = foldrM addTLet t $ if opts.pushAndElide then filterLetsTy ls t else toList ls + where + addTLet :: MonadFresh ID m => LetBinding -> Type -> m Type + -- drop let bindings of term variables + addTLet (LetTyBind (LetTypeBind v ty)) b = tlet v (regenerateTypeIDs ty) (pure b) + addTLet _ b = pure b + +filterLets :: NonEmpty LetBinding -> Expr -> [LetBinding] +filterLets ls e = filterLets' (toList ls) (freeVars e) + +filterLetsTy :: NonEmpty LetBinding -> Type -> [LetBinding] +filterLetsTy ls t = filterLets' (toList ls) (S.map unLocalName $ freeVarsTy t) + +filterLets' :: [LetBinding] -> Set Name -> [LetBinding] +filterLets' ls fvs = + fst $ + foldr + ( \l (ls', fvs') -> + let ln = letBindingName l + in if ln `S.member` fvs' + then (l : ls', S.delete ln fvs' `S.union` setOf _freeVarsLetBinding l) + else (ls', fvs') + ) + ([], fvs) + ls + +-- | Partitions lets into used and unused in a given term +-- note that some of the unused may be used in later unused, but not in later used or in the term +partitionLets :: [(a, LetBinding)] -> Expr -> ([(a, LetBinding)], [(a, LetBinding)]) +partitionLets ls e = + fst $ + foldr + ( \l ((used, unused), fvs') -> + let ln = letBindingName $ snd l + in if ln `S.member` fvs' + then ((l : used, unused), S.delete ln fvs' `S.union` setOf (_2 % _freeVarsLetBinding) l) + else ((used, l : unused), fvs') + ) + (([], []), freeVars e) + ls + +-- | Partitions lets into used and unused in a given term +-- note that some of the unused may be used in later unused, but not in later used or in the term +partitionLetsTy :: [(a, LetTypeBinding)] -> Type -> ([(a, LetTypeBinding)], [(a, LetTypeBinding)]) +partitionLetsTy ls t = + fst $ + foldr + ( \l@(_, LetTypeBind n l') ((used, unused), fvs') -> + if n `S.member` fvs' + then ((l : used, unused), S.delete n fvs' `S.union` freeVarsTy l') + else ((used, l : unused), fvs') + ) + (([], []), freeVarsTy t) + ls + +runRedexTy :: MonadEval l m => RunRedexOptions -> RedexType -> m (Type, EvalDetail) +runRedexTy _opts (InlineLetInType{ty, letID, varID, var}) = do let details = LocalVarInlineDetail { letID , varID , valueID = getID ty , bindingName = var - , replacementID = getID ty' + , replacementID = getID ty , isTypeVar = True } - pure (ty', LocalTypeVarInline details) --- let a = s in t ~> t if a does not appear in t -runRedexTy (ElideLetInType{body, orig, letBinding = (LetTypeBind v _)}) = do + pure (ty, LocalTypeVarInline details) +runRedexTy opts (PushLetType{bindings, intoTy, origTy}) = do + ty' <- descendM (addTLets opts $ LetTyBind . snd <$> bindings) intoTy let details = - LetRemovalDetail - { before = orig - , after = body - , bindingName = unLocalName v - , letID = getID orig - , bodyID = getID body + PushLetDetail + { before = origTy + , after = ty' + , letIDs = toList $ fst <$> bindings + , letBindingNames = toList $ letTypeBindingName . snd <$> bindings + , intoID = getID intoTy } - pure (body, TLetRemoval details) --- let a = s a in t a a ~> let b = s a in let a = b in t a a -runRedexTy (RenameSelfLetInType{letBinding = LetTypeBind a s, body, orig}) = do - b <- freshLocalName (freeVarsTy s <> freeVarsTy body) - insertedLet <- tlet a (tvar b) $ pure body - result <- tlet b (pure s) $ pure insertedLet - let details = - BindRenameDetail + pure (ty', PushLetDownTy details) +-- let a = s in t ~> t if a does not appear in t +runRedexTy _opts (ElideLetInType{body, orig, letBindingsKeep, letBindingsDrop}) = do + let ty = foldLetBindingsTy letBindingsKeep body + details = + LetRemovalDetail { before = orig - , after = result - , bindingNamesOld = [unLocalName a] - , bindingNamesNew = [unLocalName b] - , bindersOld = [getID orig] - , bindersNew = [getID result] - , bindingOccurrences = findFreeOccurrencesType a s - , renamingLets = [getID insertedLet] + , after = ty + , bindingNames = letTypeBindingName . snd <$> letBindingsDrop + , letIDs = fst <$> letBindingsDrop , bodyID = getID body } - pure (result, TBindRename details) + pure (ty, TLetRemoval details) -- ∀a:k.t ~> ∀b:k. let a = b in t for fresh b, avoiding the given set -runRedexTy (RenameForall{meta, origBinder, kind, body, avoid, orig}) = do +runRedexTy _opts (RenameForall{meta, origBinder, kind, body, avoid, orig}) = do newBinder <- freshLocalName (avoid <> freeVarsTy body <> bindersBelowTy (focus body)) insertedLet <- tlet origBinder (tvar newBinder) (pure body) let result = TForall meta newBinder kind insertedLet diff --git a/primer/src/Primer/EvalFull.hs b/primer/src/Primer/EvalFull.hs index 8dca22531..5e9166e1b 100644 --- a/primer/src/Primer/EvalFull.hs +++ b/primer/src/Primer/EvalFull.hs @@ -27,6 +27,8 @@ import Primer.Eval.Redex ( Dir (Chk, Syn), EvalLog (..), MonadEval, + RunRedexOptions, + ViewRedexOptions, runRedex, runRedexTy, ) @@ -49,8 +51,8 @@ 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 => ViewRedexOptions -> RunRedexOptions -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Either EvalFullError Expr) +evalFull optsV optsR tydefs env n d expr = snd <$> evalFullStepCount optsV optsR 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 +64,28 @@ evalFull tydefs env n d expr = snd <$> evalFullStepCount tydefs env n d expr -- more to notice termination. evalFullStepCount :: MonadEval l m => + ViewRedexOptions -> + RunRedexOptions -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Natural, Either EvalFullError Expr) -evalFullStepCount tydefs env n d = go 0 +evalFullStepCount optsV optsR 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 optsV optsR 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 - RExpr ez r -> lift $ unfocusExpr . flip replace ez . fst <$> runRedex r - RType et r -> lift $ unfocusExpr . unfocusType . flip replace et . fst <$> runRedexTy r +step :: MonadEval l m => ViewRedexOptions -> RunRedexOptions -> TypeDefMap -> DefMap -> Dir -> Expr -> MaybeT m Expr +step optsV optsR tydefs g d e = + findRedex optsV tydefs g d e >>= \case + RExpr ez r -> lift $ unfocusExpr . flip replace ez . fst <$> runRedex optsR r + RType et r -> lift $ unfocusExpr . unfocusType . flip replace et . fst <$> runRedexTy optsR r diff --git a/primer/src/Primer/Zipper/Type.hs b/primer/src/Primer/Zipper/Type.hs index 2c02d2fa2..152cd8db1 100644 --- a/primer/src/Primer/Zipper/Type.hs +++ b/primer/src/Primer/Zipper/Type.hs @@ -25,6 +25,7 @@ module Primer.Zipper.Type ( bindersAboveTy, LetTypeBinding' (LetTypeBind), LetTypeBinding, + letTypeBindingName, getBoundHereTy', getBoundHereTy, getBoundHereUpTy, @@ -54,11 +55,13 @@ import Primer.Core.Meta ( ID, TyVarName, getID, + unLocalName, ) import Primer.Core.Type ( Type' (TForall, TLet), TypeMeta, ) +import Primer.Name (Name) type TypeZip' b = Zipper (Type' b) (Type' b) @@ -193,6 +196,9 @@ data LetTypeBinding' a = LetTypeBind TyVarName (Type' a) deriving stock (Eq, Show) type LetTypeBinding = LetTypeBinding' TypeMeta +letTypeBindingName :: LetTypeBinding' a -> Name +letTypeBindingName (LetTypeBind n _) = unLocalName n + getBoundHereTy' :: Eq a => Type' a -> Maybe (Type' a) -> [Either TyVarName (LetTypeBinding' a)] getBoundHereTy' t prev = case t of TForall _ v _ _ -> [Left v] diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs index 147b6de0e..b2788dc25 100644 --- a/primer/test/Tests/Eval.hs +++ b/primer/test/Tests/Eval.hs @@ -4,7 +4,6 @@ module Tests.Eval where import Foreword -import Control.Monad.Trans.Maybe (runMaybeT) import Data.List (delete) import Data.Map.Strict qualified as Map import Data.Set qualified as Set @@ -20,24 +19,24 @@ import Primer.App ( ) import Primer.Builtins ( boolDef, + cCons, cFalse, cNil, cTrue, cZero, tBool, + tList, ) import Primer.Core ( Expr, GlobalName (baseName, qualifiedModule), ID, Kind' (KFun, KType), - LocalName, Pattern (PatCon, PatPrim), PrimCon (PrimChar), Type, Type' (TCon, TEmptyHole, TFun, TVar), getID, - unLocalName, unsafeMkGlobalName, _id, ) @@ -58,8 +57,9 @@ import Primer.Eval ( GlobalVarInlineDetail (..), LetRemovalDetail (..), LocalVarInlineDetail (..), + PushLetDetail (..), findNodeByID, - getNonCapturedLocal, + lookupEnclosingLet, redexes, singletonCxt, step, @@ -90,7 +90,6 @@ import Primer.TypeDef ( ) import Primer.Typecheck (typeDefs) import Primer.Zipper ( - LetBinding, LetBinding' (LetBind, LetTyBind, LetrecBind), LetTypeBinding' (LetTypeBind), target, @@ -204,39 +203,19 @@ unit_tryReduce_BETA = do unit_tryReduce_local_term_var :: Assertion unit_tryReduce_local_term_var = do - -- We assume we're inside a larger expression (e.g. a let) where the node that binds x has ID 5. + -- We assume we're immediately inside a 'let x' let ((expr, val), i) = create $ (,) <$> lvar "x" <*> con0' ["M"] "C" - locals = singletonCxt @ID 5 $ LetBind "x" val + locals = singletonCxt $ LetBind "x" val result <- runTryReduce tydefs mempty locals (expr, i) - case result of - Right (expr', LocalVarInline detail) -> do - expr' ~= val - - detail.letID @?= 5 - detail.varID @?= 0 - detail.bindingName @?= "x" - detail.valueID @?= 1 - detail.replacementID @?= 2 - detail.isTypeVar @?= False - _ -> assertFailure $ show result + result @?= Left NotRedex unit_tryReduce_local_type_var :: Assertion unit_tryReduce_local_type_var = do - -- We assume we're inside a larger expression (e.g. a let type) where the node that binds x has ID 5. + -- We assume we're immediately inside a 'let x' let ((tyvar, val), i) = create $ (,) <$> tvar "x" <*> tcon' ["M"] "C" - locals = singletonCxt @ID 5 $ LetTyBind $ LetTypeBind "x" val + locals = singletonCxt $ LetTyBind $ LetTypeBind "x" val result <- runTryReduceType mempty locals (tyvar, i) - case result of - Right (ty, LocalTypeVarInline detail) -> do - ty ~~= val - - detail.letID @?= 5 - detail.varID @?= 0 - detail.bindingName @?= "x" - detail.valueID @?= 1 - detail.replacementID @?= 2 - detail.isTypeVar @?= True - _ -> assertFailure $ show result + result @?= Left NotRedex unit_tryReduce_global_var :: Assertion unit_tryReduce_global_var = do @@ -269,30 +248,27 @@ unit_tryReduce_let = do detail.before @?= expr detail.after ~= expectedResult - detail.bindingName @?= "x" - detail.letID @?= 0 + detail.bindingNames @?= ["x"] + detail.letIDs @?= [0] detail.bodyID @?= 2 _ -> assertFailure $ show result --- let x = x in x ==> let y = x in let x = y in x +-- let x = x in x ==> x unit_tryReduce_let_self_capture :: Assertion unit_tryReduce_let_self_capture = do let (expr, i) = create $ let_ "x" (lvar "x") (lvar "x") - expectedResult = create' $ let_ "a3" (lvar "x") $ let_ "x" (lvar "a3") (lvar "x") + expectedResult = create' $ lvar "x" result <- runTryReduce tydefs mempty mempty (expr, i) case result of - Right (expr', BindRename detail) -> do + Right (expr', LocalVarInline detail) -> do expr' ~= expectedResult - detail.before @?= expr - detail.after ~= expectedResult - detail.bindingNamesOld @?= ["x"] - detail.bindingNamesNew @?= ["a3"] - detail.bindersOld @?= [0] - detail.bindersNew @?= [6] - detail.bindingOccurrences @?= [1] - detail.renamingLets @?= [4] - detail.bodyID @?= 2 + detail.letID @?= 0 + detail.varID @?= 2 + detail.bindingName @?= "x" + detail.valueID @?= 1 + detail.replacementID @?= 1 + detail.isTypeVar @?= False _ -> assertFailure $ show result unit_tryReduce_lettype :: Assertion @@ -306,30 +282,27 @@ unit_tryReduce_lettype = do detail.before @?= expr detail.after ~= expectedResult - detail.bindingName @?= "x" - detail.letID @?= 0 + detail.bindingNames @?= ["x"] + detail.letIDs @?= [0] detail.bodyID @?= 2 _ -> assertFailure $ show result --- let type x = x in _ :: x ==> let type y = x in lettype x = y in _ :: x +-- let type x = x in ? :: x ==> (let type x = x in ?) :: (tlet x = x in x) +-- NB: the single-step evaluator does not use the push-and-elide optimisation unit_tryReduce_lettype_self_capture :: Assertion unit_tryReduce_lettype_self_capture = do let (expr, i) = create $ letType "x" (tvar "x") (emptyHole `ann` tvar "x") - expectedResult = create' $ letType "a5" (tvar "x") $ letType "x" (tvar "a5") (emptyHole `ann` tvar "x") + expectedResult = create' $ letType "x" (tvar "x") emptyHole `ann` tlet "x" (tvar "x") (tvar "x") result <- runTryReduce tydefs mempty mempty (expr, i) case result of - Right (expr', BindRename detail) -> do + Right (expr', PushLetDown detail) -> do expr' ~= expectedResult detail.before @?= expr detail.after ~= expectedResult - detail.bindingNamesOld @?= ["x"] - detail.bindingNamesNew @?= ["a5"] - detail.bindersOld @?= [0] - detail.bindersNew @?= [8] - detail.bindingOccurrences @?= [1] - detail.renamingLets @?= [6] - detail.bodyID @?= 2 + detail.letIDs @?= [0] + detail.letBindingNames @?= ["x"] + detail.intoID @?= 2 _ -> assertFailure $ show result -- tlet x = C in ty ==> ty when x not occur free in ty @@ -344,31 +317,27 @@ unit_tryReduce_tlet_elide = do detail.before @?= ty detail.after ~~= expectedResult - detail.bindingName @?= "x" - detail.letID @?= 0 + detail.bindingNames @?= ["x"] + detail.letIDs @?= [0] detail.bodyID @?= 2 _ -> assertFailure $ show result --- tlet x = x in x ==> tlet y = x in tlet x = y in x +-- tlet x = x in x ==> x unit_tryReduce_tlet_self_capture :: Assertion unit_tryReduce_tlet_self_capture = do let (ty, i) = create $ tlet "x" (tvar "x") (tvar "x") - n = "a3" - expectedResult = create' $ tlet n (tvar "x") $ tlet "x" (tvar n) (tvar "x") + expectedResult = create' $ tvar "x" result <- runTryReduceType mempty mempty (ty, i) case result of - Right (ty', TBindRename detail) -> do + Right (ty', LocalTypeVarInline detail) -> do ty' ~~= expectedResult - detail.before @?= ty - detail.after ~~= expectedResult - detail.bindingNamesOld @?= ["x"] - detail.bindingNamesNew @?= [unLocalName n] - detail.bindersOld @?= [0] - detail.bindersNew @?= [6] - detail.bindingOccurrences @?= [1] - detail.renamingLets @?= [4] - detail.bodyID @?= 2 + detail.letID @?= 0 + detail.varID @?= 2 + detail.bindingName @?= "x" + detail.valueID @?= 1 + detail.replacementID @?= 1 + detail.isTypeVar @?= True _ -> assertFailure $ show result unit_tryReduce_letrec :: Assertion @@ -382,8 +351,8 @@ unit_tryReduce_letrec = do detail.before @?= expr detail.after ~= expectedResult - detail.bindingName @?= "x" - detail.letID @?= 0 + detail.bindingNames @?= ["x"] + detail.letIDs @?= [0] detail.bodyID @?= 3 _ -> assertFailure $ show result @@ -794,16 +763,6 @@ unit_step_non_redex = -- * 'findNodeByID' tests -lookupNonCaptured :: LocalName k -> Cxt -> Maybe (ID, LetBinding) -lookupNonCaptured = runReader . runMaybeT . getNonCapturedLocal - -lookupCaptured :: LocalName k -> Cxt -> Maybe (ID, LetBinding) -lookupCaptured n c@(Cxt c') - | Nothing <- lookupNonCaptured n c - , Just (Just r, i, _) <- Map.lookup (unLocalName n) c' = - pure (i, r) - | otherwise = Nothing - unit_findNodeByID_letrec :: Assertion unit_findNodeByID_letrec = do let expr = create' $ letrec "x" (lvar "x") (tcon' ["M"] "T") (lvar "x") @@ -811,27 +770,25 @@ unit_findNodeByID_letrec = do t = create' $ tcon' ["M"] "T" case findNodeByID 0 Syn expr of Just (Cxt locals, Left (_, z)) -> do - assertBool "no locals in scope at node 0" $ Map.null locals + assertBool "no enclosing lets at node 0" $ null locals target z ~= expr _ -> assertFailure "node 0 not found" case findNodeByID 1 Syn expr of - Just (locals, Left (_, z)) -> do + Just (Cxt locals, Left (_, z)) -> do target z ~= x - case lookupNonCaptured "x" locals of - Just (0, LetrecBind _ e _) -> e ~= x - r -> assertFailure $ "expected to find 'x' bound at id 0, with rhs = 'x', but found " <> show r + assertBool "no enclosing lets at node 1" $ null locals _ -> assertFailure "node 1 not found" case findNodeByID 2 Syn expr of Just (Cxt locals, Right z) -> do target z ~~= t - assertBool "no locals in scope at node 2" $ Map.null locals + assertBool "no enclosing lets at node 2" $ null locals _ -> assertFailure "node 2 not found" case findNodeByID 3 Syn expr of Just (locals, Left (_, z)) -> do target z ~= x - case lookupNonCaptured "x" locals of - Just (0, LetrecBind _ e _) -> e ~= x - r -> assertFailure $ "expected to find 'x' bound at id 0, with rhs = 'x', but found " <> show r + case lookupEnclosingLet "x" locals of + Just (LetrecBind _ e _) -> e ~= x + r -> assertFailure $ "expected to find 'x' let-bound, with rhs = 'x', but found " <> show r _ -> assertFailure "node 3 not found" unit_findNodeByID_1 :: Assertion @@ -846,9 +803,8 @@ unit_findNodeByID_1 = do pure (x_, c_, e) case findNodeByID 0 Syn expr of Just (locals, Left (_, z)) -> do - case lookupNonCaptured "x" locals of - Just (i, LetBind _ e) -> do - i @?= 2 + case lookupEnclosingLet "x" locals of + Just (LetBind _ e) -> do e ~= c Just _ -> assertFailure "expected to find 'x' let-bound, but found some other flavor of let" Nothing -> assertFailure "expected to find 'x' bound, but did not" @@ -857,19 +813,19 @@ unit_findNodeByID_1 = do case findNodeByID 1 Syn expr of Just (Cxt locals, Left (_, z)) -> do - assertBool "expected nothing in scope" $ Map.null locals + assertBool "expected nothing in scope" $ null locals target z ~= c _ -> assertFailure "node 1 not found" case findNodeByID 2 Syn expr of Just (Cxt locals, Left (_, z)) -> do - assertBool "expected nothing in scope" $ Map.null locals + assertBool "expected nothing in scope" $ null locals target z ~= expr _ -> assertFailure "node 2 not found" unit_findNodeByID_2 :: Assertion unit_findNodeByID_2 = do - let (x, t, expr) = create' $ do + let (x, _, expr) = create' $ do -- id 0 x_ <- tvar "x" -- id 1 @@ -879,12 +835,9 @@ unit_findNodeByID_2 = do pure (x_, t_, e) case findNodeByID 0 Syn expr of Just (locals, Right z) -> do - case lookupNonCaptured "x" locals of - Just (i, LetTyBind (LetTypeBind _ e)) -> do - i @?= 2 - e ~~= t - Just _ -> assertFailure "expected to find a type 'x' bound, but found a term" - Nothing -> assertFailure "expected to find 'x' bound, but did not" + case lookupEnclosingLet "x" locals of + Nothing -> pure () + Just _ -> assertFailure "expected 'x' to not be bound by an immediately enclosing let, but it was" target z ~~= x _ -> assertFailure "node 0 not found" @@ -900,9 +853,8 @@ unit_findNodeByID_tlet = do pure (x_, t_, e) case findNodeByID 0 Syn expr of Just (locals, Right z) -> do - case lookupNonCaptured "x" locals of - Just (i, LetTyBind (LetTypeBind _ e)) -> do - i @?= 4 + case lookupEnclosingLet "x" locals of + Just (LetTyBind (LetTypeBind _ e)) -> do e ~~= t Just _ -> assertFailure "expected to find a type 'x' bound, but found a term" Nothing -> assertFailure "expected to find 'x' bound, but did not" @@ -913,10 +865,10 @@ unit_findNodeByID_scoping_1 :: Assertion unit_findNodeByID_scoping_1 = do let expr = create' $ let_ "x" (con0' ["M"] "C") $ lam "x" $ lvar "x" case findNodeByID 3 Syn expr of - Just (Cxt locals, Left _) - | Just (Nothing, _, _) <- Map.lookup "x" locals -> + Just (locals, Left _) + | Nothing <- lookupEnclosingLet "x" locals -> pure () - | otherwise -> assertFailure "Expected 'x' to be in scope but not have a substitution" + | otherwise -> assertFailure "expected 'x' to not be bound by an immediately enclosing let, but it was" _ -> assertFailure "Expected to find the lvar 'x'" unit_findNodeByID_scoping_2 :: Assertion @@ -927,8 +879,8 @@ unit_findNodeByID_scoping_2 = do pure (b, e) case findNodeByID 4 Syn expr of Just (locals@(Cxt locals'), Left _) - | Map.size locals' == 1 - , lookupNonCaptured "x" locals == Just (3, LetBind "x" bind) -> + | length locals' == 2 + , lookupEnclosingLet "x" locals == Just (LetBind "x" bind) -> pure () Just (_, Left _) -> assertFailure "Expected to have inner let binding of 'x' reported" _ -> assertFailure "Expected to find the lvar 'x'" @@ -946,10 +898,10 @@ unit_findNodeByID_capture = in do case findNodeByID varOcc Syn expr of Just (locals@(Cxt locals'), Left _) - | Map.size locals' == 2 - , Just (1, LetrecBind{}) <- lookupCaptured "x" locals -> + | null locals' + , Nothing <- lookupEnclosingLet "x" locals -> pure () - Just (_, Left _) -> assertFailure "Expected let binding of 'x' to be reported as captured-if-inlined" + | otherwise -> assertFailure "expected 'x' to not be bound by an immediately enclosing let, but it was" _ -> assertFailure "Expected to find the lvar 'x'" reduct <- runStep maxID mempty mempty (expr, varOcc) case reduct of @@ -965,11 +917,11 @@ unit_findNodeByID_capture_type = in do case findNodeByID varOcc Syn expr of Just (locals@(Cxt locals'), Right _) - | Map.size locals' == 3 - , Just (1, LetTyBind _) <- lookupCaptured "x" locals - , Just (5, LetTyBind _) <- lookupCaptured "z" locals -> + | null locals' + , Nothing <- lookupEnclosingLet "x" locals + , Nothing <- lookupEnclosingLet "z" locals -> pure () - Just (_, Right _) -> assertFailure "Expected lettype binding of 'x' and the tlet binding of 'z' to be reported as captured-if-inlined" + | otherwise -> assertFailure "expected 'x' to not be bound by an immediately enclosing let, but it was" _ -> assertFailure "Expected to find the lvar 'x'" reduct <- runStep maxID mempty mempty (expr, varOcc) case reduct of @@ -1140,59 +1092,55 @@ unit_redexes_LAM_4 = ) ) in do - redexesOf (e noAnn) <@?=> Set.singleton 5 - redexesOf (e withAnn) <@?=> Set.fromList [3, 6] + redexesOf (e noAnn) <@?=> Set.singleton 0 + redexesOf (e withAnn) <@?=> Set.fromList [0, 3] unit_redexes_let_1 :: Assertion unit_redexes_let_1 = redexesOf (let_ "x" (con0' ["M"] "C") (app (lvar "x") (lvar "y"))) - <@?=> Set.singleton 3 + <@?=> Set.singleton 0 unit_redexes_let_2 :: Assertion unit_redexes_let_2 = redexesOf (let_ "x" (con0' ["M"] "C") (lam "x" (app (lvar "x") (lvar "y")))) - <@?=> Set.singleton 0 + <@?=> Set.fromList [0, 2] --- We cannot substitute one occurrence of a let-bound variable if it --- would result in capture of a free variable in the bound term by the --- let binder itself. unit_redexes_let_3 :: Assertion unit_redexes_let_3 = do - -- NB we must not say node 3 (the occurrence of the variable) is a redex redexesOf (lam "x" $ let_ "x" (lvar "x") (lvar "x")) <@?=> Set.fromList [1] --- We cannot substitute one occurrence of a let-bound variable if it --- would result in capture of a free variable in the bound term by the --- some intervening binder. +-- We cannot push a let under a binder if it would result in capture of a free +-- variable in the bound term. unit_redexes_let_capture :: Assertion unit_redexes_let_capture = -- We should rename the lambda, and not inline the variable redexesOf (let_ "x" (lvar "y") $ lam "y" $ lvar "x") <@?=> Set.singleton 2 unit_redexes_lettype_capture :: Assertion -unit_redexes_lettype_capture = - -- We should rename the forall and not inline the variable - redexesOf (letType "x" (tvar "y") (emptyHole `ann` tforall "y" (KType ()) (tvar "x"))) <@?=> Set.singleton 4 +unit_redexes_lettype_capture = do + -- We can push the letType down once + redexesOf (letType "x" (tvar "y") (emptyHole `ann` tforall "y" (KType ()) (tvar "x"))) <@?=> Set.singleton 0 + -- But now we should rename the forall and not push the tlet further + redexesOf (emptyHole `ann` tlet "x" (tvar "y") (tforall "y" (KType ()) (tvar "x"))) <@?=> Set.singleton 4 unit_redexes_letrec_1 :: Assertion unit_redexes_letrec_1 = redexesOf (letrec "x" (con1' ["M"] "C" $ lvar "x") (tcon' ["M"] "T") (app (lvar "x") (lvar "y"))) - <@?=> Set.fromList [2, 5] + <@?=> Set.fromList [0] unit_redexes_letrec_2 :: Assertion unit_redexes_letrec_2 = redexesOf (letrec "x" (con1' ["M"] "C" $ lvar "x") (tcon' ["M"] "T") (lvar "y")) - <@?=> Set.fromList [0, 2] + <@?=> Set.fromList [0] --- Test that our self-capture logic does not apply to letrec. unit_redexes_letrec_3 :: Assertion unit_redexes_letrec_3 = - -- If this were a let, we would not be able to substitute, but it is possible for letrec - redexesOf (lAM "a" $ lam "x" $ letrec "x" (lvar "x") (tvar "a") (lvar "x")) <@?=> Set.fromList [3, 5] + redexesOf (lAM "a" $ lam "x" $ letrec "x" (lvar "x") (tvar "a") (lvar "x")) <@?=> Set.fromList [2] + +unit_redexes_letrec_4 :: Assertion +unit_redexes_letrec_4 = + redexesOf (let_ "x" ((lam "x" (lvar "x") `ann` (tcon tBool `tfun` tcon tBool)) `app` con0 cTrue) $ letrec "xs" (con cCons [lvar "x", lvar "xs"]) (tcon tList `tapp` tEmptyHole) (lvar "xs")) <@?=> Set.fromList [1, 9] --- The application could potentially be reduced by pushing the --- argument inside the letrec, but that is not a reduction rule. Once --- we inline the letrec enough we would be able to see the beta. unit_redexes_letrec_app_1 :: Assertion unit_redexes_letrec_app_1 = let e mkAnn = @@ -1205,12 +1153,9 @@ unit_redexes_letrec_app_1 = ) (con0' ["M"] "D") in do - redexesOf (e noAnn) <@?=> Set.fromList [5] - redexesOf (e withAnn) <@?=> Set.fromList [6] + redexesOf (e noAnn) <@?=> Set.fromList [1] + redexesOf (e withAnn) <@?=> Set.fromList [1] --- The application could potentially be reduced by pushing the --- argument inside the letrec, but that is not a reduction rule. Once --- we inline the letrec enough we would be able to see the beta. unit_redexes_letrec_APP_1 :: Assertion unit_redexes_letrec_APP_1 = let e mkAnn = @@ -1223,8 +1168,8 @@ unit_redexes_letrec_APP_1 = ) (tcon' ["M"] "D") in do - redexesOf (e noAnn) <@?=> Set.fromList [5] - redexesOf (e withAnn) <@?=> Set.fromList [6] + redexesOf (e noAnn) <@?=> Set.fromList [1] + redexesOf (e withAnn) <@?=> Set.fromList [1] unit_redexes_lettype_1 :: Assertion unit_redexes_lettype_1 = @@ -1232,18 +1177,14 @@ unit_redexes_lettype_1 = unit_redexes_lettype_2 :: Assertion unit_redexes_lettype_2 = - redexesOf (letType "x" (tcon' ["M"] "T") (con0' ["M"] "C" `ann` tvar "x")) <@?=> Set.fromList [4] + redexesOf (letType "x" (tcon' ["M"] "T") (con0' ["M"] "C" `ann` tvar "x")) <@?=> Set.fromList [0] unit_redexes_lettype_3 :: Assertion unit_redexes_lettype_3 = - redexesOf (letType "x" (tcon' ["M"] "T") (letrec "y" (con0' ["M"] "C") (tvar "x") (lvar "y"))) <@?=> Set.fromList [4, 5] + redexesOf (letType "x" (tcon' ["M"] "T") (letrec "y" (con0' ["M"] "C") (tvar "x") (lvar "y"))) <@?=> Set.fromList [2] --- We cannot substitute one occurrence of a let-bound variable if it --- would result in capture of a free variable in the bound term by the --- let binder itself. unit_redexes_lettype_4 :: Assertion unit_redexes_lettype_4 = do - -- NB we must not say node 5 (the occurrence of the variable) is a redex redexesOf (lAM "x" $ letType "x" (tvar "x") (emptyHole `ann` tvar "x")) <@?=> Set.fromList [1] unit_redexes_tlet_1 :: Assertion @@ -1252,18 +1193,14 @@ unit_redexes_tlet_1 = unit_redexes_tlet_2 :: Assertion unit_redexes_tlet_2 = - redexesOf (emptyHole `ann` tlet "x" (tcon' ["M"] "T") (tapp (tcon' ["M"] "S") (tvar "x"))) <@?=> Set.fromList [6] + redexesOf (emptyHole `ann` tlet "x" (tcon' ["M"] "T") (tapp (tcon' ["M"] "S") (tvar "x"))) <@?=> Set.fromList [2] unit_redexes_tlet_3 :: Assertion unit_redexes_tlet_3 = - redexesOf (emptyHole `ann` tlet "x" (tcon' ["M"] "T") (tlet "y" (tcon' ["M"] "S") (tapp (tvar "x") (tvar "y")))) <@?=> Set.fromList [7, 8] + redexesOf (emptyHole `ann` tlet "x" (tcon' ["M"] "T") (tlet "y" (tcon' ["M"] "S") (tapp (tvar "x") (tvar "y")))) <@?=> Set.fromList [2, 4] --- We cannot substitute one occurrence of a let-bound variable if it --- would result in capture of a free variable in the bound term by the --- let binder itself. unit_redexes_tlet_4 :: Assertion unit_redexes_tlet_4 = do - -- NB we must not say node 5 (the occurrence of the variable) is a redex redexesOf (lAM "x" $ emptyHole `ann` tlet "x" (tvar "x") (tvar "x")) <@?=> Set.fromList [3] -- case-of-constructor does not reduce if the constructor is not annotated @@ -1288,7 +1225,7 @@ unit_redexes_case_2 = ) <@?=> mempty --- The case expression can be reduced, as can the variable x in the branch rhs. +-- The case expression can be reduced, and the @let x@ can be pushed down unit_redexes_case_3 :: Assertion unit_redexes_case_3 = redexesOf @@ -1300,10 +1237,11 @@ unit_redexes_case_3 = [branch' (["M"], "C") [] (lvar "x")] ) ) - <@?=> Set.fromList [2, 6] + <@?=> Set.fromList [0, 2] --- The variable x in the rhs is bound to the branch pattern, so is no longer reducible. --- However this means the let is redundant, and can be reduced. +-- The variable x in the rhs is bound to the branch pattern, so is no longer refering to the @let@. +-- This means the let is redundant, and we can either elide it or rename the inner "x" binder +-- (to prepare to push). unit_redexes_case_4 :: Assertion unit_redexes_case_4 = redexesOf @@ -1317,10 +1255,28 @@ unit_redexes_case_4 = ) <@?=> Set.fromList [0, 2] --- If scrutinee of a case is a redex itself, we recognise that unit_redexes_case_5 :: Assertion unit_redexes_case_5 = - redexesOf (let_ "x" (con0' ["M"] "C") (case_ (lvar "x") [])) <@?=> Set.fromList [3] + redexesOf (let_ "x" (con0' ["M"] "C") (case_ (lvar "x") [])) <@?=> Set.fromList [0] + +-- The @let@ cannot be pushed into the @case_@, as the 'y' would be captured. +unit_redexes_case_6 :: Assertion +unit_redexes_case_6 = + redexesOf + ( let_ + "x" + (lvar "y") + ( case_ + (con0' ["M"] "C" `ann` tcon' ["M"] "C") + [branch' (["M"], "C") [("y", Nothing)] (lvar "x")] + ) + ) + <@?=> Set.fromList [2] + +-- If scrutinee of a case is a redex itself, we recognise that +unit_redexes_case_7 :: Assertion +unit_redexes_case_7 = + redexesOf (case_ (let_ "x" (con0' ["M"] "C") $ lvar "x") []) <@?=> Set.fromList [1] unit_redexes_case_fallback_1 :: Assertion unit_redexes_case_fallback_1 = @@ -1355,6 +1311,13 @@ unit_redexes_let_upsilon = do redexesOf (letrec "x" (lam "x" emptyHole `ann` t) t $ lam "x" emptyHole `ann` t) <@?=> Set.fromList [0, 1] redexesOf (lam "x" $ letrec "x" (lam "x" emptyHole `ann` t) t $ emptyHole `ann` t) <@?=> Set.fromList [1, 2, 9] +unit_redexes_push_let :: Assertion +unit_redexes_push_let = do + redexesOf (letrec "x" (lam "x" emptyHole) tEmptyHole $ lam "x" emptyHole) <@?=> Set.fromList [0, 4] + redexesOf (letType "x" tEmptyHole $ let_ "y" (lam "x" emptyHole) $ lam "x" emptyHole) <@?=> Set.fromList [0, 2, 5] + redexesOf (letType "x" tEmptyHole $ letrec "y" (lam "x" emptyHole) tEmptyHole $ lam "x" emptyHole) <@?=> Set.fromList [0, 2, 6] + redexesOf (letType "x" tEmptyHole $ letType "y" (tforall "x" (KType ()) tEmptyHole) $ lam "x" emptyHole) <@?=> Set.fromList [0, 2, 5] + unit_redexes_prim_1 :: Assertion unit_redexes_prim_1 = redexesOfWithPrims (pfun EqChar `app` char 'a' `app` char 'b') <@?=> Set.fromList [0] @@ -1453,7 +1416,14 @@ tasty_type_preservation = -- | Reductions do not interfere with each other -- if @i,j ∈ redexes e@ (and @i /= j@), and @e@ reduces to @e'@ via redex @i@ -- then @j ∈ redexes e'@, --- unless @j@ no longer exists in @e'@ or @j@ was a rename-binding which is no longer required +-- unless one of the following is true +-- - @j@ no longer exists in @e'@ +-- - @j@ was a rename-binding which is no longer required +-- (e.g. because @i@ was eliding a let, or reducing inside the binding of +-- a let removing a variable reference) +-- - @i@ was a PushLet, which can intersperse itself inside the parts of @j@'s redex, blocking it +-- - @j@ was a PushLet surrounding @i@, and @i@ either reduced to a leaf or +-- removed a variable reference, causing us to not PushLet, but ElideLet tasty_redex_independent :: Property tasty_redex_independent = let testModules = [builtinModule, primitiveModule] @@ -1472,12 +1442,19 @@ tasty_redex_independent = s <- failWhenSevereLogs $ step @EvalLog tds globs t dir i case s of Left err -> annotateShow err >> failure - Right (s', _) -> do + Right (s', siDetails) -> do annotateShow s' if elemOf exprIDs j s' then do sj <- failWhenSevereLogs $ step @EvalLog tds globs t dir j - case sj of - Right (_, BindRename{}) -> success + case (sj, siDetails) of + (Right (_, BindRename{}), _) -> success + (_, PushLetDown{}) -> success + (_, PushLetDownTy{}) -> success + (Right (_, PushLetDown{}), CaseReduction{}) -> success + (Right (_, PushLetDown{}), CaseReductionTrivial{}) -> success + (Right (_, PushLetDown{}), RemoveAnn{}) -> success + (Right (_, PushLetDown{}), LetRemoval{}) -> success + (Right (_, PushLetDownTy{}), TLetRemoval{}) -> success _ -> assert . elem j =<< failWhenSevereLogs (redexes @EvalLog tds globs dir s') else success diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs index c98878049..03342b48e 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, @@ -43,6 +44,7 @@ import Primer.Core.Utils ( forgetMetadata, ) import Primer.Def (DefMap) +import Primer.Eval import Primer.EvalFull import Primer.Examples qualified as Examples ( even, @@ -141,41 +143,37 @@ unit_3 :: Assertion unit_3 = let ((expr, expected), maxID) = create $ do e <- letType "a" (tvar "b") $ emptyHole `ann` (tcon' ["M"] "T" `tapp` tvar "a" `tapp` tforall "a" (KType ()) (tvar "a") `tapp` tforall "b" (KType ()) (tcon' ["M"] "S" `tapp` tvar "a" `tapp` tvar "b")) - let b' = "a33" -- NB: fragile name a33 + let b' = "a42" -- NB: fragile name expect <- emptyHole `ann` (tcon' ["M"] "T" `tapp` tvar "b" `tapp` tforall "a" (KType ()) (tvar "a") `tapp` tforall b' (KType ()) (tcon' ["M"] "S" `tapp` tvar "b" `tapp` tvar b')) pure (e, expect) in do - s <- evalFullTest maxID mempty mempty 7 Syn expr - s <~==> Right expected + s <- evalFullTestExactSteps maxID mempty mempty 12 Syn expr + s ~== expected -- Check we don't have shadowing issues in terms unit_4 :: Assertion unit_4 = let ((expr, expected), maxID) = create $ do e <- let_ "a" (lvar "b") $ con' ["M"] "C" [lvar "a", lam "a" (lvar "a"), lam "b" (con' ["M"] "D" [lvar "a", lvar "b"])] - let b' = "a19" -- NB: fragile name + let b' = "a22" -- NB: fragile name expect <- con' ["M"] "C" [lvar "b", lam "a" (lvar "a"), lam b' (con' ["M"] "D" [lvar "b", lvar b'])] pure (e, expect) in do - s <- evalFullTest maxID mempty mempty 7 Syn expr - s <~==> Right expected + s <- evalFullTestExactSteps maxID mempty mempty 8 Syn expr + s ~== expected --- This test is slightly unfortunate for two reasons --- First, maybe we should do upsilon redexes more aggressively, to avoid the --- inner annotation in the output; alternatively tweak the reduction rule for --- letrec so that when inlining, the newly-created letrec does not scope over --- the newly-created annotation --- Second, writing [_] for embeddings we don't reduce [ e ] : T (and I'm not --- sure if we should). This leads to the outer annotation in the output. +-- This test is slightly unfortunate. +-- Writing [_] for embeddings we don't reduce [ e ] : T (and I'm not +-- sure if we should). This leads to the annotation in the output. -- See https://github.com/hackworthltd/primer/issues/12 unit_5 :: Assertion unit_5 = let ((e, expt), maxID) = create $ do a <- letrec "x" (lvar "x") (tcon tBool) (lvar "x") - b <- letrec "x" (lvar "x") (tcon tBool) (lvar "x" `ann` tcon tBool) `ann` tcon tBool + b <- letrec "x" (lvar "x") (tcon tBool) (lvar "x") `ann` tcon tBool pure (a, b) in do - s <- evalFullTest maxID mempty mempty 100 Syn e + s <- evalFullTest maxID mempty mempty 101 Syn e s <~==> Left (TimedOut expt) unit_6 :: Assertion @@ -239,6 +237,82 @@ unit_9 = s <- evalFullTest maxID builtinTypes (M.fromList globals) 1000 Syn e s <~==> Right expected +{- Note [Pushing down lets and the static argument transformation] +Our strategy of "pushing down lets" (which is effectively an explicit +substitution semantics, where the substitution is interspersed with +other reduction steps) has different performance characteristics than +our previous strategy of eagerly fully inlining `let` bindings. In +particular, it makes the transformation of unit_8 into unit_9 is not +effective. + +To explain why, let us first recap what this transformation is. +The static argument transformation is a technique of optimising +a recursive function of multiple arguments by splitting the lambda +bindings into two: the ones that do not change in a recursive call, and +those that do. Then the changing ones are handled by a local (recursive) +function. For example, changing the following definition of `map` + map :: (a -> b) -> [a] -> [b] + map f xs = case xs of + [] -> [] + y : ys -> f y : map f ys +into + mapSAT f = let go xs = case xs of + [] -> [] + y : ys -> f y : go ys + in go + +When reducing by naively applying rewrite rules and doing "long-range" +substitution, the latter can be more efficient, since we effectively +specialise the recursive loop for a particular `f`, rather than passing +it around each iteration. (Note that passing it around causes an extra +beta step on each recursive call, and thus more substitution.) That is +to say, calling `mapSAT foo [1,2,3]` will result in + let go xs = case xs of + [] -> [] + y : ys -> foo y : go ys + in go [1,2,3] + +However, that is assuming that beta reductions (and `let`s, since we +reduce betas to let bindings) result in "eager substitution": + let f = foo in + let go = c (...) (...) (... f ... go ...) in + go +should reduce by inlining the `f` inside the recursive let binding. + +When we lazily push an explicit substitution down the tree this does not +happen (at least, in our implementation, since we treat the recusive let +as a substition and never push substitutions into each other). Indeed, +we would reduce the above by inlining the `go` + let f = foo in + let go = c (...) (...) (... f ... go ...) in + ... f ... go ... +and then pushing the `let`s (i.e. explicit substitutions) down, resulting in + c (...) + (...) + (let f = foo in + let go = c (...) (...) (... f ... go ...) in + ... f ... go ...) +(Here we have taken the optimization of not pushing the substition into +branches where those variables are unused.) Notice the recursive structure +here will hold on to the substitution, pushing it down into each expansion +of the recursive let, which is no better than the original definition +without the static argument translation's local worker. + +It may be possible to avoid this by treating recursive bindings +differently to explicit substitutions, so we could push the substitution +of `f` into the definition of `go`. However, I have not thought about +this enough (from any of a theoretical, implementation or pedagogy +standpoint) to have a good idea of whether it would work and be worth +it. In particular, for a simple language aimed at learning, do we +want to treat non-recursive and recursive lets so differently (or +maybe even user-written lets vs explicit substitutions caused by beta +reduction)? Alternatively, it may also be possible to cause explicit +substitutions to interact with let bindings (i.e. push the outer let +rather than the inner let, and not special-case any particular lets), +but a naive version of this would cause infinite loops continually +swapping two lets! See https://github.com/hackworthltd/primer/issues/1112. +-} + -- A case redex must have an scrutinee which is an annotated constructor. -- Plain constructors are not well-typed here, for bidirectionality reasons, -- although they just fail to reduce rather than the evaluator throwing a type error. @@ -265,8 +339,6 @@ unit_10 = t' <- evalFullTest maxID builtinTypes mempty 1 Syn t t' <~==> Right t --- This example shows that when we are under even a 'let' all we can do is --- substitute, otherwise we may go down a rabbit hole! unit_11 :: Assertion unit_11 = let modName = mkSimpleModuleName "TestModule" @@ -285,15 +357,9 @@ unit_11 = `ann` (tcon tPair `tapp` tcon tBool `tapp` tcon tNat) pure (globs, expr, expect) in do - evalFullTest maxID builtinTypes (M.fromList globals) 10 Syn e >>= \case - Left (TimedOut _) -> pure () - x -> assertFailure $ show x - s <- evalFullTest maxID builtinTypes (M.fromList globals) 20 Syn e - s <~==> Right expected + s <- evalFullTestExactSteps maxID builtinTypes (M.fromList globals) 15 Syn e + s ~== expected --- This example shows that we may only substitute the top-most let otherwise we --- may go down a rabbit hole unrolling a letrec and not doing enough --- computation to see the recursion should terminate unit_12 :: Assertion unit_12 = let ((e, expected), maxID) = create $ do @@ -309,8 +375,8 @@ unit_12 = expect <- con0 cTrue `ann` tcon tBool pure (expr, expect) in do - s <- evalFullTest maxID builtinTypes mempty 15 Syn e - s <~==> Right expected + s <- evalFullTestExactSteps maxID builtinTypes mempty 10 Syn e + s ~== expected unit_13 :: Assertion unit_13 = @@ -332,27 +398,26 @@ unit_14 = s <- evalFullTest maxID builtinTypes mempty 15 Syn e s <~==> Right expected --- Need to swap to substituting an inner let, when it (could have) arises from --- a renaming to unblock the outer let. --- i.e. when trying to reduce the let x: +-- Sometimes we need to rename a binder in order to push a let past it -- let x = y in λy.C x y -- let x = y in λz. let y = z in C x y --- let x = y in λz. let y = z in C x z --- let x = y in λz. C x z --- let x = y in λz. C y z --- λz. C y z +-- λz. let x = y in let y = z in C x y +-- λz. C (let x = y in x) (let y = z in y) +-- λz. C y (let y = z in y) +-- λz. C y z unit_15 :: Assertion unit_15 = let ((expr, steps, expected), maxID) = create $ do let l = let_ "x" (lvar "y") - let c a b = con' ["M"] "C" [lvar a, lvar b] - e0 <- l $ lam "y" $ c "x" "y" - let y' = "a38" - e1 <- l $ lam y' $ let_ "y" (lvar y') $ c "x" "y" - e2 <- l $ lam y' $ let_ "y" (lvar y') $ c "x" y' - e3 <- l $ lam y' $ c "x" y' - e4 <- l $ lam y' $ c "y" y' - e5 <- lam y' $ c "y" y' + let c a b = con' ["M"] "C" [a, b] + e0 <- l $ lam "y" $ c (lvar "x") (lvar "y") + let y' = "a40" + let rny = let_ "y" (lvar y') + e1 <- l $ lam y' $ rny $ c (lvar "x") (lvar "y") + e2 <- lam y' $ l $ rny $ c (lvar "x") (lvar "y") + e3 <- lam y' $ c (l $ lvar "x") (rny $ lvar "y") + e4 <- lam y' $ c (lvar "y") (rny $ lvar "y") + e5 <- lam y' $ c (lvar "y") (lvar y') pure (e0, [e0, e1, e2, e3, e4, e5], e5) in do si <- traverse (\i -> evalFullTest maxID builtinTypes mempty i Syn expr) [0 .. fromIntegral $ length steps - 1] @@ -367,21 +432,110 @@ unit_hole_ann_case = t <- evalFullTest maxID builtinTypes mempty 1 Chk tm t @?= Right tm +-- Check we don't have variable capture in +-- let x = y in case ? of C x -> x ; D y -> x +unit_case_let_capture :: Assertion +unit_case_let_capture = + let ((expr, steps, expected), maxID) = create $ do + let l = let_ "x" (lvar "y") + let w = "a66" + let z = "a69" + let rnx = let_ "x" (lvar w) + let rny = let_ "y" (lvar z) + e0 <- + l $ + case_ + emptyHole + [ branch' (["M"], "C") [("x", Nothing)] (lvar "x") + , branch' (["M"], "D") [("y", Nothing)] (lvar "x") + ] + e1 <- + l $ + case_ + emptyHole + [ branch' (["M"], "C") [(w, Nothing)] (rnx $ lvar "x") + , branch' (["M"], "D") [("y", Nothing)] (lvar "x") + ] + e2 <- + l $ + case_ + emptyHole + [ branch' (["M"], "C") [(w, Nothing)] (rnx $ lvar "x") + , branch' (["M"], "D") [(z, Nothing)] (rny $ lvar "x") + ] + e3 <- + case_ + emptyHole + [ branch' (["M"], "C") [(w, Nothing)] (rnx $ lvar "x") + , branch' (["M"], "D") [(z, Nothing)] (l $ rny $ lvar "x") + ] + e4 <- + case_ + emptyHole + [ branch' (["M"], "C") [(w, Nothing)] (lvar w) + , branch' (["M"], "D") [(z, Nothing)] (l $ rny $ lvar "x") + ] + e5 <- + case_ + emptyHole + [ branch' (["M"], "C") [(w, Nothing)] (lvar w) + , branch' (["M"], "D") [(z, Nothing)] (l $ lvar "x") + ] + e6 <- + case_ + emptyHole + [ branch' (["M"], "C") [(w, Nothing)] (lvar w) + , branch' (["M"], "D") [(z, Nothing)] (lvar "y") + ] + pure (e0, [e0, e1, e2, e3, e4, e5, e6], e6) + in do + si <- traverse (\i -> evalFullTest maxID builtinTypes mempty i Syn expr) [0 .. fromIntegral $ length steps - 1] + zipWithM_ (\s e -> s <~==> Left (TimedOut e)) si steps + s <- evalFullTest maxID builtinTypes mempty (fromIntegral $ length steps) Syn expr + s <~==> Right expected + +-- We must evaluate inside the body of a let before the binding: +-- consider @let x = ((λy.t : A -> B) r) in letrec xs = s[x] : S in xs@ +-- the two possible reductions are to inline the @letrec@s or to reduce the beta. +-- We should do the @letrec@ first. +unit_letrec_body_first :: Assertion +unit_letrec_body_first = + let lx = let_ "x" ((lam "x" (lvar "x") `ann` (tcon tBool `tfun` tcon tBool)) `app` con0 cTrue) + lxs = + letrec + "xs" + (con cCons [lvar "x", lvar "xs"]) + (tcon tList `tapp` tEmptyHole) + (expr, maxID) = create $ lx $ lxs (lvar "xs") + expected1 = create' $ lx $ lxs $ con cCons [lvar "x", lvar "xs"] `ann` (tcon tList `tapp` tEmptyHole) + expected2 = create' $ lx (lxs $ con cCons [lvar "x", lvar "xs"]) `ann` (tcon tList `tapp` tEmptyHole) + expected3 = create' $ con cCons [lx $ lvar "x", lx $ lxs $ lvar "xs"] `ann` (tcon tList `tapp` tEmptyHole) + in do + e1 <- evalFullTest maxID builtinTypes mempty 1 Syn expr + e1 <~==> Left (TimedOut expected1) + e2 <- evalFullTest maxID builtinTypes mempty 2 Syn expr + e2 <~==> Left (TimedOut expected2) + e3 <- evalFullTest maxID builtinTypes mempty 3 Syn expr + e3 <~==> Left (TimedOut expected3) + -- tlet x = C in D x x -- ==> --- tlet x = C in D C x +-- (tlet x = C in D x) (tlet x = C in x) +-- ==> +-- D (tlet x = C in x) (tlet x = C in x) -- ==> --- tlet x = C in D C C +-- D C (tlet x = C in x) -- ==> -- D C C unit_tlet :: Assertion unit_tlet = let ((expr, expected), maxID) = create $ do e0 <- ann emptyHole $ tlet "x" (tcon' ["M"] "C") (tcon' ["M"] "D" `tapp` tvar "x" `tapp` tvar "x") - e1 <- ann emptyHole $ tlet "x" (tcon' ["M"] "C") (tcon' ["M"] "D" `tapp` tcon' ["M"] "C" `tapp` tvar "x") - e2 <- ann emptyHole $ tlet "x" (tcon' ["M"] "C") (tcon' ["M"] "D" `tapp` tcon' ["M"] "C" `tapp` tcon' ["M"] "C") - e3 <- ann emptyHole $ tcon' ["M"] "D" `tapp` tcon' ["M"] "C" `tapp` tcon' ["M"] "C" - pure (e0, map (Left . TimedOut) [e0, e1, e2, e3] ++ [Right e3]) + e1 <- ann emptyHole $ tlet "x" (tcon' ["M"] "C") (tcon' ["M"] "D" `tapp` tvar "x") `tapp` tlet "x" (tcon' ["M"] "C") (tvar "x") + e2 <- ann emptyHole $ tcon' ["M"] "D" `tapp` tlet "x" (tcon' ["M"] "C") (tvar "x") `tapp` tlet "x" (tcon' ["M"] "C") (tvar "x") + e3 <- ann emptyHole $ tcon' ["M"] "D" `tapp` tcon' ["M"] "C" `tapp` tlet "x" (tcon' ["M"] "C") (tvar "x") + e4 <- ann emptyHole $ tcon' ["M"] "D" `tapp` tcon' ["M"] "C" `tapp` tcon' ["M"] "C" + pure (e0, map (Left . TimedOut) [e0, e1, e2, e3, e4] ++ [Right e4]) test (n, expect) = do r <- evalFullTest maxID mempty mempty n Syn expr r <~==> expect @@ -400,27 +554,13 @@ unit_tlet_elide = do in mapM_ test (zip [0 ..] expected) -- tlet x = x in x --- ==> --- tlet y = x in let x = y in x --- ==> --- tlet y = x in let x = y in y --- ==> --- tlet y = x in y --- ==> --- tlet y = x in x --- ==> -- x unit_tlet_self_capture :: Assertion unit_tlet_self_capture = do - let y = "a32" - ((expr, expected), maxID) = create $ do + let ((expr, expected), maxID) = create $ do e0 <- ann emptyHole $ tlet "x" (tvar "x") $ tvar "x" - e1 <- ann emptyHole $ tlet y (tvar "x") $ tlet "x" (tvar y) $ tvar "x" - e2 <- ann emptyHole $ tlet y (tvar "x") $ tlet "x" (tvar y) $ tvar y - e3 <- ann emptyHole $ tlet y (tvar "x") $ tvar y - e4 <- ann emptyHole $ tlet y (tvar "x") $ tvar "x" - e5 <- ann emptyHole $ tvar "x" - pure (e0, map (Left . TimedOut) [e0, e1, e2, e3, e4, e5] ++ [Right e5]) + e1 <- ann emptyHole $ tvar "x" + pure (e0, map (Left . TimedOut) [e0, e1] ++ [Right e1]) test (n, expect) = do r <- evalFullTest maxID mempty mempty n Syn expr r <~==> expect @@ -443,6 +583,8 @@ tasty_resume = withDiscards 2000 $ -- A helper for tasty_resume, and tasty_resume_regression resumeTest :: [Module] -> Dir -> Expr -> PropertyT WT () resumeTest mods dir t = do + let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} + let optsR = RunRedexOptions{pushAndElide = True} let globs = foldMap' moduleDefsQualified mods tds <- asks typeDefs n <- forAllT $ Gen.integral $ Range.linear 2 1000 -- Arbitrary limit here @@ -453,19 +595,19 @@ resumeTest mods dir t = do -- exactly the same as "reducing n steps and then further reducing m -- steps" (including generated names). (A happy consequence of this is that -- it is precisely the same including ids in metadata.) - ((stepsFinal', sFinal), logs) <- lift $ isolateWT $ runPureLogT $ evalFullStepCount @EvalLog tds globs n dir t + ((stepsFinal', sFinal), logs) <- lift $ isolateWT $ runPureLogT $ evalFullStepCount @EvalLog optsV optsR tds globs n dir t testNoSevereLogs logs when (stepsFinal' < 2) discard let stepsFinal = case sFinal of Left _ -> stepsFinal'; Right _ -> 1 + stepsFinal' m <- forAllT $ Gen.integral $ Range.constant 1 (stepsFinal - 1) - (stepsMid, sMid') <- failWhenSevereLogs $ evalFullStepCount @EvalLog tds globs m dir t + (stepsMid, sMid') <- failWhenSevereLogs $ evalFullStepCount @EvalLog optsV optsR tds globs m dir t stepsMid === m sMid <- case sMid' of Left (TimedOut e) -> pure e -- This should never happen: we know we are not taking enough steps to -- hit a normal form (as m < stepsFinal) Right e -> assert False >> pure e - (stepsTotal, sTotal) <- failWhenSevereLogs $ evalFullStepCount @EvalLog tds globs (stepsFinal - m) dir sMid + (stepsTotal, sTotal) <- failWhenSevereLogs $ evalFullStepCount @EvalLog optsV optsR tds globs (stepsFinal - m) dir sMid stepsMid + stepsTotal === stepsFinal' sFinal === sTotal @@ -594,34 +736,63 @@ unit_type_preservation_BETA_regression = `app` lvar "x" -- NB: the point of the ... `app` lvar x is to make the annotated term be in SYN position -- so we reduce the type, rather than taking an upsilon step - -- Rename the let b - -- Λb. λx. ((lettype a = b Bool in λc (? : a)) : (let c = b Bool in let b = c in Nat -> b)) x - let b' = "a132" + -- Push the let b + -- Λb. λx. ((lettype a = b Bool in λc (? : a)) : (Nat -> (let b = b Bool in b))) x expectA2 <- lAM "b" $ lam "x" $ ( letType "a" (tvar "b" `tapp` tcon tBool) (lam "c" $ emptyHole `ann` tvar "a") - `ann` tlet b' (tvar "b" `tapp` tcon tBool) (tlet "b" (tvar b') $ tcon tNat `tfun` tvar "b") + `ann` (tcon tNat `tfun` tlet "b" (tvar "b" `tapp` tcon tBool) (tvar "b")) ) `app` lvar "x" - -- Resolve the renaming - -- Λb. λx. ((lettype a = b Bool in λc (? : a)) : (let c = b Bool in Nat -> c)) x - expectA4 <- + -- Inline the let + -- Λb. λx. ((lettype a = b Bool in λc (? : a)) : (Nat -> b Bool)) x + expectA3 <- lAM "b" $ lam "x" $ ( letType "a" (tvar "b" `tapp` tcon tBool) (lam "c" $ emptyHole `ann` tvar "a") - `ann` tlet b' (tvar "b" `tapp` tcon tBool) (tcon tNat `tfun` tvar b') + `ann` (tcon tNat `tfun` (tvar "b" `tapp` tcon tBool)) ) `app` lvar "x" - -- Resolve all the letTypes - -- Λb. λx. ((λc (? : b Bool)) : (Nat -> b Bool)) x - expectA8 <- + -- Push the let + -- Λb. λx. (λc (lettype a = b Bool in (? : a)) : (Nat -> b Bool)) x + expectA4 <- lAM "b" $ lam "x" $ - ( lam "c" (emptyHole `ann` (tvar "b" `tapp` tcon tBool)) + ( lam "c" (letType "a" (tvar "b" `tapp` tcon tBool) (emptyHole `ann` tvar "a")) `ann` (tcon tNat `tfun` (tvar "b" `tapp` tcon tBool)) ) `app` lvar "x" + -- Do the beta step + -- Λb. λx. (let c = (x : Nat) in (lettype a = b Bool in (? : a)) : (b Bool)) + expectA5 <- + lAM "b" $ + lam "x" $ + let_ "c" (lvar "x" `ann` tcon tNat) (letType "a" (tvar "b" `tapp` tcon tBool) (emptyHole `ann` tvar "a")) + `ann` (tvar "b" `tapp` tcon tBool) + -- Elide a pointless let + -- Λb. λx. ((lettype a = b Bool in (? : a)) : (b Bool)) + expectA6 <- + lAM "b" $ + lam "x" $ + letType "a" (tvar "b" `tapp` tcon tBool) (emptyHole `ann` tvar "a") + `ann` (tvar "b" `tapp` tcon tBool) + -- Push the lets, eliding those that are redundant + -- Λb. λx. ((? : lettype a = b Bool in a) : (b Bool)) + expectA7 <- + lAM "b" $ + lam "x" $ + emptyHole + `ann` tlet "a" (tvar "b" `tapp` tcon tBool) (tvar "a") + `ann` (tvar "b" `tapp` tcon tBool) + -- Inline a let + -- Λb. λx. ((? : b Bool) : (b Bool)) + expectA8 <- + lAM "b" $ + lam "x" $ + emptyHole + `ann` (tvar "b" `tapp` tcon tBool) + `ann` (tvar "b" `tapp` tcon tBool) -- The 'B' sequence previously captured in the term "t" above -- Λb. (Λa (foo @(b Bool) : ∀b.Nat) @Char eB <- @@ -636,7 +807,7 @@ unit_type_preservation_BETA_regression = lAM "b" $ letType "a" (tcon tChar) (gvar foo `aPP` (tvar "b" `tapp` tcon tBool)) `ann` tlet "b" (tcon tChar) (tcon tNat) - -- Drop annotation and elide lettype + -- Drop annotation, elide lettype -- Λb. foo @(b Bool) expectB3 <- lAM "b" $ gvar foo `aPP` (tvar "b" `tapp` tcon tBool) -- Note that the reduction of eA and eB take slightly @@ -644,7 +815,19 @@ unit_type_preservation_BETA_regression = -- because it has an occurrence of a type variable and is thus -- not "concrete" pure - ( (eA, [(1, expectA1), (2, expectA2), (4, expectA4), (8, expectA8)]) + ( + ( eA + , + [ (1, expectA1) + , (2, expectA2) + , (3, expectA3) + , (4, expectA4) + , (5, expectA5) + , (6, expectA6) + , (7, expectA7) + , (8, expectA8) + ] + ) , (eB, [(1, expectB1), (3, expectB3)]) ) sA n = evalFullTest maxID builtinTypes mempty n Chk exprA @@ -672,29 +855,29 @@ unit_type_preservation_BETA_regression = -- 'let x' has captured the reference to the x in the bound term. -- This causes the term to become ill-sorted. -- Similarly, we reduce 'λx. let x = x in x' to itself, due to the same capture. +-- (This was before we changed to "pushing down lets") unit_let_self_capture :: Assertion unit_let_self_capture = let ( ( expr1 , ty1 , expr2 - , expected2a - , expected2b + , expected2 , expr3 , expected3a , expected3b , expr4 , expected4a , expected4b + , expected4c ) , maxID ) = create $ do e1 <- lAM "x" $ let_ "x" (emptyHole `ann` tvar "x") (lvar "x") let t1 = TForall () "a" (KType ()) $ TVar () "a" e2 <- lam "x" $ let_ "x" (lvar "x") (lvar "x") - expect2a <- lam "x" $ let_ "a76" (lvar "x") (let_ "x" (lvar "a76") (lvar "x")) - expect2b <- lam "x" $ lvar "x" + expect2 <- lam "x" $ lvar "x" e3 <- lAM "x" $ letType "x" (tvar "x") (emptyHole `ann` tvar "x") - expect3a <- lAM "x" $ letType "a76" (tvar "x") (letType "x" (tvar "a76") (emptyHole `ann` tvar "x")) + expect3a <- lAM "x" $ emptyHole `ann` tlet "x" (tvar "x") (tvar "x") expect3b <- lAM "x" $ emptyHole `ann` tvar "x" -- We do not need to do anything special for letrec e4 <- lAM "a" $ lam "f" $ lam "x" $ letrec "x" (lvar "f" `app` lvar "x") (tvar "a") (lvar "x") @@ -703,28 +886,29 @@ unit_let_self_capture = lam "f" $ lam "x" $ letrec "x" (lvar "f" `app` lvar "x") (tvar "a") $ - letrec "x" (lvar "f" `app` lvar "x") (tvar "a") ((lvar "f" `app` lvar "x") `ann` tvar "a") + (lvar "f" `app` lvar "x") `ann` tvar "a" expect4b <- lAM "a" $ lam "f" $ lam "x" $ - letrec - "x" - (lvar "f" `app` lvar "x") - (tvar "a") - ((lvar "f" `app` lvar "x") `ann` tvar "a") + letrec "x" (lvar "f" `app` lvar "x") (tvar "a") (lvar "f" `app` lvar "x") `ann` tvar "a" + expect4c <- + lAM "a" $ + lam "f" $ + lam "x" $ + (lvar "f" `app` letrec "x" (lvar "f" `app` lvar "x") (tvar "a") (lvar "x")) `ann` tvar "a" pure ( e1 , t1 , e2 - , expect2a - , expect2b + , expect2 , e3 , expect3a , expect3b , e4 , expect4a , expect4b + , expect4c ) s1 n = evalFullTest maxID mempty mempty n Chk expr1 s2 n = evalFullTest maxID mempty mempty n Chk expr2 @@ -741,14 +925,14 @@ unit_let_self_capture = Right _ -> pure () in do typePres ty1 s1 - s2 1 >>= (<~==> Left (TimedOut expected2a)) - s2 5 >>= (<~==> Left (TimedOut expected2b)) - s2 6 >>= (<~==> Right expected2b) + s2 1 >>= (<~==> Left (TimedOut expected2)) + s2 2 >>= (<~==> Right expected2) s3 1 >>= (<~==> Left (TimedOut expected3a)) - s3 5 >>= (<~==> Left (TimedOut expected3b)) - s3 6 >>= (<~==> Right expected3b) + s3 2 >>= (<~==> Left (TimedOut expected3b)) + s3 3 >>= (<~==> Right expected3b) s4 1 >>= (<~==> Left (TimedOut expected4a)) s4 2 >>= (<~==> Left (TimedOut expected4b)) + s4 3 >>= (<~==> Left (TimedOut expected4c)) -- | @spanM p mxs@ returns a tuple where the first component is the -- values coming from the longest prefix of @mxs@ all of which satisfy @@ -777,6 +961,7 @@ spanM f (x : xs) = do -- Λy. let x = ?:y in let y = _:y in y x -- reducing it to -- Λy. let x = ?:y in let y = _:y in (_:y) x +-- (This was before we changed to "pushing down lets") unit_regression_self_capture_let_let :: Assertion unit_regression_self_capture_let_let = do let e = @@ -784,18 +969,26 @@ unit_regression_self_capture_let_let = do let_ "x" (emptyHole `ann` tvar "y") $ let_ "y" (emptyHole `ann` tvar "y") $ lvar "y" `app` lvar "x" - z = "a12" f = lAM "y" $ - let_ "x" (emptyHole `ann` tvar "y") $ - let_ z (emptyHole `ann` tvar "y") $ - let_ "y" (lvar z) $ - lvar "y" `app` lvar "x" + let_ + "y" + (emptyHole `ann` tvar "y") + (lvar "y") + `app` let_ + "x" + (emptyHole `ann` tvar "y") + (lvar "x") + g = + lAM "y" $ + (emptyHole `ann` tvar "y") + `app` (emptyHole `ann` tvar "y") (e', i) = create e ev n = evalFullTest i mempty mempty n Chk e' x ~ y = x >>= (<~==> Left (TimedOut (create' y))) ev 0 ~ e ev 1 ~ f + ev 3 ~ g -- | Evaluation preserves types -- (assuming we don't end with a 'LetType' in the term, as the typechecker @@ -804,6 +997,8 @@ tasty_type_preservation :: Property tasty_type_preservation = withTests 1000 $ withDiscards 2000 $ propertyWT testModules $ do + let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} + let optsR = RunRedexOptions{pushAndElide = True} let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules tds <- asks typeDefs (dir, t, ty) <- genDirTm @@ -820,7 +1015,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 - (steps, s) <- failWhenSevereLogs $ evalFullStepCount @EvalLog tds globs maxSteps dir t + (steps, s) <- failWhenSevereLogs $ evalFullStepCount @EvalLog optsV optsR tds globs maxSteps dir t annotateShow steps annotateShow s -- s is often reduced to normal form @@ -830,7 +1025,7 @@ tasty_type_preservation = withTests 1000 $ then label "generated a normal form" else do midSteps <- forAllT $ Gen.integral $ Range.linear 1 (steps - 1) - (_, s') <- failWhenSevereLogs $ evalFullStepCount @EvalLog tds globs midSteps dir t + (_, s') <- failWhenSevereLogs $ evalFullStepCount @EvalLog optsV optsR tds globs midSteps dir t test "mid " s' -- Unsaturated primitives are stuck terms @@ -1270,8 +1465,8 @@ unit_prim_partial_map = <*> pure (M.singleton mapName mapDef) <*> primDefs in do - s <- evalFullTest maxID builtinTypes (gs <> prims) 67 Syn e - s <~==> Right r + s <- evalFullTestExactSteps maxID builtinTypes (gs <> prims) 91 Syn e + s ~== r -- Test that handleEvalFullRequest will reduce imported terms unit_eval_full_modules :: Assertion @@ -1335,13 +1530,15 @@ tasty_unique_ids :: Property tasty_unique_ids = withTests 1000 $ withDiscards 2000 $ propertyWT testModules $ do + let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} + let optsR = RunRedexOptions{pushAndElide = True} let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules tds <- asks typeDefs (dir, t1, _) <- genDirTm let go n t | n == (0 :: Int) = pure () | otherwise = do - t' <- failWhenSevereLogs $ evalFull @EvalLog tds globs 1 dir t + t' <- failWhenSevereLogs $ evalFull @EvalLog optsV optsR tds globs 1 dir t case t' of Left (TimedOut e) -> uniqueIDs e >> go (n - 1) e Right e -> uniqueIDs e @@ -1357,11 +1554,10 @@ unit_wildcard = (eTerm, maxIDTerm) = create $ caseFB_ loop [] (con0 cTrue) expectTerm = create' $ con0 cTrue (eDiverge, maxIDDiverge) = create $ caseFB_ loop [branch cZero [] $ con0 cFalse] (con0 cTrue) - -- This has an annotation within the body of the letrec for the same reason as unit_5 expectDiverge = create' $ caseFB_ - ( letrec "x" (lvar "x") (tcon tNat) (lvar "x" `ann` tcon tNat) + ( letrec "x" (lvar "x") (tcon tNat) (lvar "x") `ann` tcon tNat ) [branch cZero [] $ con0 cFalse] @@ -1369,7 +1565,7 @@ unit_wildcard = in do s <- evalFullTest maxIDTerm mempty mempty 2 Syn eTerm s <~==> Right expectTerm - t <- evalFullTest maxIDDiverge mempty mempty 22 Syn eDiverge + t <- evalFullTest maxIDDiverge mempty mempty 5 Syn eDiverge t <~==> Left (TimedOut expectDiverge) unit_case_prim :: Assertion @@ -1408,16 +1604,31 @@ unit_case_prim = -- * Utilities -evalFullTest :: ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr) +evalFullTest :: HasCallStack => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr) evalFullTest id_ tydefs globals n d e = do - let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog tydefs globals n d e + let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} + let optsR = RunRedexOptions{pushAndElide = True} + let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsV optsR tydefs globals n d e assertNoSevereLogs logs distinctIDs r pure r +evalFullTestExactSteps :: HasCallStack => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO Expr +evalFullTestExactSteps id_ tydefs globals n d e = do + s <- evalFullTest id_ tydefs globals (n - 1) d e + case s of + Right s' -> assertFailure $ "Unexpectedly reached normal form: " <> show s' + Left _ -> do + t <- evalFullTest id_ tydefs globals n d e + case t of + Left t' -> assertFailure $ "Unexpected timeout: " <> show t' + Right t' -> pure t' + 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 tydefs globals n d e + let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} + let optsR = RunRedexOptions{pushAndElide = True} + let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsV optsR tydefs globals n d e testNoSevereLogs logs let ids = r ^.. evalResultExpr % exprIDs ids === ordNub ids @@ -1457,6 +1668,9 @@ evalResultExpr = _Left % timedOut `adjoin` _Right (<~==>) :: HasCallStack => Either EvalFullError Expr -> Either EvalFullError Expr -> Assertion x <~==> y = on (@?=) (over evalResultExpr zeroIDs) x y +(~==) :: HasCallStack => Expr -> Expr -> Assertion +x ~== y = on (@?=) zeroIDs x y + distinctIDs :: Either EvalFullError Expr -> Assertion distinctIDs e = let ids = e ^.. evalResultExpr % exprIDs diff --git a/primer/test/Tests/Prelude/Integer.hs b/primer/test/Tests/Prelude/Integer.hs index bdffa9c0d..df975abf3 100644 --- a/primer/test/Tests/Prelude/Integer.hs +++ b/primer/test/Tests/Prelude/Integer.hs @@ -37,7 +37,7 @@ tasty_negate_prop = property $ do tasty_abs_prop :: Property tasty_abs_prop = property $ do n <- forAll $ G.integral_ (Range.constant (-10) 10) - functionOutput P.abs [int n] 40 <===> Right (create' $ int $ abs n) + functionOutput P.abs [int n] 45 <===> Right (create' $ int $ abs n) -- NOTE: Termination bound is experimental, do not know how it varies with n, m tasty_gcd_prop :: Property @@ -61,7 +61,7 @@ tasty_even_prop = property $ do tasty_odd_prop :: Property tasty_odd_prop = property $ do n <- forAll $ G.integral_ (Range.constant (-10) 10) - functionOutput P.odd [int n] 20 <===> Right (create' $ bool_ $ odd n) + functionOutput P.odd [int n] 25 <===> Right (create' $ bool_ $ odd n) tasty_sum_prop :: Property tasty_sum_prop = property $ do diff --git a/primer/test/Tests/Prelude/Polymorphism.hs b/primer/test/Tests/Prelude/Polymorphism.hs index bf444e1c1..552c49048 100644 --- a/primer/test/Tests/Prelude/Polymorphism.hs +++ b/primer/test/Tests/Prelude/Polymorphism.hs @@ -63,7 +63,7 @@ tasty_const_prop = property $ do , Right $ tcon tBool , Left $ bool_ True ] - 20 + 21 <===> Right (create' $ int n) functionOutput' -- Bool Test P.const @@ -72,7 +72,7 @@ tasty_const_prop = property $ do , Right $ tcon tInt , Left $ int n ] - 20 + 21 <===> Right (create' $ bool_ b) functionOutput' -- List of Int Test P.const @@ -81,7 +81,7 @@ tasty_const_prop = property $ do , Right $ tcon tInt , Left $ int n ] - 20 + 21 <===> Right (create' $ list_ $ map int ns) tasty_map_prop :: Property diff --git a/primer/test/Tests/Prelude/Utils.hs b/primer/test/Tests/Prelude/Utils.hs index 752bd0d2f..e36bdedd3 100644 --- a/primer/test/Tests/Prelude/Utils.hs +++ b/primer/test/Tests/Prelude/Utils.hs @@ -7,6 +7,10 @@ import Hedgehog.Internal.Property import Optics (over) import Primer.Core (Expr, GVarName, Type) import Primer.Core.DSL (apps', create', gvar) +import Primer.Eval ( + RunRedexOptions (RunRedexOptions, pushAndElide), + ViewRedexOptions (ViewRedexOptions, aggressiveElision, groupedLets), + ) import Primer.EvalFull (Dir (Chk), EvalFullError, EvalLog, TerminationBound, evalFull) import Primer.Log (runPureLogT) import Primer.Module (builtinModule, moduleDefsQualified, moduleTypesQualified, primitiveModule) @@ -49,9 +53,11 @@ functionOutput f args = functionOutput' f (map Left args) -- Tests a prelude function with a combination of Expr/Type arguments to be applied functionOutput' :: GVarName -> [Either (TestM Expr) (TestM Type)] -> TerminationBound -> Either EvalFullError Expr functionOutput' f args depth = - let (r, logs) = evalTestM 0 $ runPureLogT $ do + let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True} + optsR = RunRedexOptions{pushAndElide = True} + (r, logs) = evalTestM 0 $ runPureLogT $ do e <- apps' (gvar f) $ bimap lift lift <$> args - evalFull @EvalLog ty def n d e + evalFull @EvalLog optsV optsR ty def n d e severe = Seq.filter isSevereLog logs in if null severe then r