From f2831dad17d386f4029a9820debdcffcc6d4915e Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 12 Jul 2023 14:41:15 +0100 Subject: [PATCH] NormalOrder; change handling of cxts to match push-down-lets. This "fixes" unit_redexes_lettype_capture -- don't consider a burried binder renamable TODO: see todos in code simplify code: don't need to record so much in Cxt rip out findNodeByID stuff ? rip out other complexity since all rules are local (at least, up to knowing what the immediately enclosing let's free vars are, to know to rename lambdas etc instead of pushing) move to more declaritive rules (+ normal-order annotations)? --- primer/src/Primer/Eval/NormalOrder.hs | 79 ++++++++++++++------------- primer/src/Primer/Eval/Redex.hs | 5 ++ primer/test/Tests/Eval.hs | 36 +++++------- 3 files changed, 59 insertions(+), 61 deletions(-) diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs index ea1d7847c..8795e196b 100644 --- a/primer/src/Primer/Eval/NormalOrder.hs +++ b/primer/src/Primer/Eval/NormalOrder.hs @@ -88,6 +88,7 @@ import Primer.Eval.Redex ( origBinder, var ), + cxtAddLet, viewRedex, viewRedexType, _freeVarsLetBinding, @@ -128,29 +129,34 @@ data RedexWithContext data ViewLet = ViewLet { bindingVL :: LetBinding -- ^ the binding itself - , bodyVL :: Accum Cxt (Dir, ExprZ) - -- ^ the body (i.e. after the `in`) - , typeChildrenVL :: [Accum Cxt TypeZ] - -- ^ any non-body type children - , termChildrenVL :: [Accum Cxt (Dir, ExprZ)] - -- ^ any non-body term children (i.e. rhs of the binding) + , bodyVL :: (Maybe LetBinding, (Dir, ExprZ)) + -- ^ the body (i.e. after the `in`), along with the newly in-scope bindings (this will always be @Just bindingVL@, but record it here for consistency) + -- , bodyVL::Accum Cxt (Dir, ExprZ) -- ^ the body (i.e. after the `in`) + , typeChildrenVL :: [(Maybe LetBinding, TypeZ)] + -- ^ any non-body type children, along with (potentially) the newly in-scope binding + , termChildrenVL :: [(Maybe LetBinding, (Dir, ExprZ))] + -- ^ any non-body term children (i.e. rhs of the binding), along with (potentially) the newly in-scope binding + -- , typeChildrenVL::[Accum Cxt TypeZ] -- ^ any non-body type children + -- , termChildrenVL ::[Accum Cxt (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, [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 []) + (Let _ x e _b, [ez', bz]) -> let l = LetBind x e in Just (ViewLet l (Just l, bz) [] [(Nothing, ez')]) + (Letrec _ x e ty _b, [ez', bz]) -> let l = LetrecBind x e ty in Just (ViewLet l (Just l, bz) tz [(Just l, ez')]) + (LetType _ a ty _b, [bz]) -> bz `seq` let l = LetTyBind $ LetTypeBind a ty in Just (ViewLet l (Just l, bz) tz []) _ -> Nothing where - tz :: [Accum Cxt TypeZ] + tz :: [(Maybe LetBinding, TypeZ)] -- as with focusType', we don't need to bind anything here - tz = maybe [] ((: []) . pure) $ focusType ez + tz = maybe [] ((: []) . (Nothing,)) $ 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") +-- TODO: 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. +-- TODO: do we still "handle lets specially", i.e. do we ever set subst = Just ...? -- (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.) -- - We accumulate in some 'f a' for 'MonadPlus f' rather than an arbitrary monoid @@ -163,35 +169,36 @@ 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) + cxtAddLet' l c = maybe c (`cxtAddLet` c) l + go :: Cxt -> (Dir, ExprZ) -> f a + go lets dez@(d, ez) = + extract.expr ez d lets <|> case (extract.subst, viewLet dez) of - (Just goSubst, Just (ViewLet{bindingVL, bodyVL})) -> (readerToAccumT . ReaderT . (\(d', b) -> goSubst bindingVL b d')) =<< hoistAccum bodyVL + (Just goSubst, Just (ViewLet{bindingVL, bodyVL = (l, (d', b))})) -> goSubst bindingVL b d' $ cxtAddLet' l lets -- ((\(d', b) -> goSubst bindingVL b d')) =<< hoistAccum bodyVL -- Prefer to compute inside the body of a let, but otherwise compute in the binding - (Nothing, Just (ViewLet{bodyVL, typeChildrenVL, termChildrenVL})) -> + (Nothing, Just (ViewLet{bodyVL = (bodyLet, b), typeChildrenVL, termChildrenVL})) -> msum $ - (go =<< hoistAccum bodyVL) - : map (goType <=< hoistAccum) typeChildrenVL - <> map (go <=< hoistAccum) termChildrenVL + go (cxtAddLet' bodyLet lets) b + : map (\(l, tz) -> goType (cxtAddLet' l lets) tz) typeChildrenVL + <> map (\(l, c) -> go (cxtAddLet' l lets) c) termChildrenVL -- Since stuck things other than lets are stuck on the first child or -- its type annotation, we can handle them all uniformly _ -> msum $ - (goType =<< focusType' ez) - : map (go <=< hoistAccum) (exprChildren dez) - goType :: TypeZ -> AccumT Cxt f a - goType tz = - readerToAccumT (ReaderT $ extract.ty tz) + (goType mempty =<< focusType' ez) + : map (go mempty) (exprChildren dez) + goType :: Cxt -> TypeZ -> f a + goType lets tz = + extract.ty tz lets <|> case (extract.substTy, target tz) of (Just goSubstTy, TLet _ a t _body) - | [_, bz] <- typeChildren tz -> (readerToAccumT . ReaderT . goSubstTy a t) =<< hoistAccum bz - (Nothing, TLet _ a _t _body) + | [_, bz] <- typeChildren tz -> goSubstTy a t bz lets + (Nothing, TLet _ a t _body) -- Prefer to compute inside the body of a let, but otherwise compute in the binding - | [tz', bz] <- typeChildren tz -> (goType =<< hoistAccum bz) <|> (goType =<< hoistAccum tz') - _ -> msum $ map (goType <=< hoistAccum) $ typeChildren tz + | [tz, bz] <- typeChildren tz -> goType (cxtAddLet (LetTyBind $ LetTypeBind a t) lets) bz <|> goType lets tz + _ -> msum $ map (goType mempty) $ typeChildren tz data FMExpr m = FMExpr { expr :: ExprZ -> Dir -> Cxt -> m @@ -200,9 +207,7 @@ data FMExpr m = FMExpr , 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 @@ -232,7 +237,7 @@ 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) @@ -251,15 +256,13 @@ exprChildren (d, ez) = | e == target c -> Chk | otherwise -> d _ -> Chk - addBinds ez bs - pure (d', c) + (d', c) -typeChildren :: TypeZ -> [Accum Cxt TypeZ] +typeChildren :: TypeZ -> [TypeZ] typeChildren tz = children' tz <&> \c -> do let bs = getBoundHereTy' (target tz) (Just $ target c) - addBinds tz $ bimap unLocalName LetTyBind <$> bs - pure c + c addBinds :: HasID i => i -> [Either Name LetBinding] -> Accum Cxt () addBinds i' bs = do diff --git a/primer/src/Primer/Eval/Redex.hs b/primer/src/Primer/Eval/Redex.hs index e1bd8b048..228b6310b 100644 --- a/primer/src/Primer/Eval/Redex.hs +++ b/primer/src/Primer/Eval/Redex.hs @@ -12,6 +12,7 @@ module Primer.Eval.Redex ( runRedexTy, Dir (Syn, Chk), Cxt (Cxt), + cxtAddLet, _freeVarsLetBinding, EvalLog (..), MonadEval, @@ -614,6 +615,7 @@ 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} +-- TODO: don't need to record nearly so much anymore -- a list of directly-enclosing let bindings would be good enough -- 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 @@ -622,6 +624,9 @@ newtype Cxt = Cxt (M.Map Name (Maybe LetBinding, ID, Cxt)) -- and want later 'add's to overwrite earlier (more-global) context entries deriving (Semigroup, Monoid) via Dual (M.Map Name (Maybe LetBinding, ID, Cxt)) +cxtAddLet :: LetBinding -> Cxt -> Cxt +cxtAddLet l (Cxt c) = Cxt $ M.insert (letBindingName l) (Just l, 0, mempty) c -- TODO: the 0, mempty are LIES, but we never care about these positions... + lookup :: Name -> Cxt -> Maybe (Maybe LetBinding, ID, Cxt) lookup n (Cxt cxt) = M.lookup n cxt diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs index 2f6a00b17..db10101af 100644 --- a/primer/test/Tests/Eval.hs +++ b/primer/test/Tests/Eval.hs @@ -848,7 +848,6 @@ unit_findNodeByID_1 = do Just (locals, Left (_, z)) -> do case lookupNonCaptured "x" locals of Just (i, LetBind _ e) -> do - i @?= 2 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" @@ -880,11 +879,8 @@ unit_findNodeByID_2 = do 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" + 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" @@ -902,7 +898,6 @@ unit_findNodeByID_tlet = do Just (locals, Right z) -> do case lookupNonCaptured "x" locals of Just (i, LetTyBind (LetTypeBind _ e)) -> do - i @?= 4 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" @@ -914,9 +909,9 @@ 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 -> + | Nothing <- Map.lookup "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 @@ -928,7 +923,7 @@ unit_findNodeByID_scoping_2 = do case findNodeByID 4 Syn expr of Just (locals@(Cxt locals'), Left _) | Map.size locals' == 1 - , lookupNonCaptured "x" locals == Just (3, LetBind "x" bind) -> + , (snd <$> lookupNonCaptured "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 +941,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 -> + | Map.size locals' == 0 + , Nothing <- lookupCaptured "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 +960,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 -> + | Map.size locals' == 0 + , Nothing <- lookupCaptured "x" locals + , Nothing <- lookupCaptured "z" locals -> pure () - Just (_, Right _) -> assertFailure "Expected lettype binding of 'x' and the tlet binding of 'z' to be reported as captured-if-inlined" -- TODO: can probably remove all the "captured-if-inlined" stuff as don't do inlining like that now + | 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 @@ -1166,12 +1161,7 @@ unit_redexes_let_capture = unit_redexes_lettype_capture :: Assertion unit_redexes_lettype_capture = do -- We can push the letType down once - -- TODO: we don't really want the "forall y" to be a redex -- it is only a - -- rename, and not blocking anything yet. It would be preferable to only - -- consider renaming binders when they are immediately under the corresponding - -- @let@ (actually, immediately under a group of @let@s containing the - -- corresponding one). - redexesOf (letType "x" (tvar "y") (emptyHole `ann` tforall "y" KType (tvar "x"))) <@?=> Set.fromList [0, 4] + redexesOf (letType "x" (tvar "y") (emptyHole `ann` tforall "y" KType (tvar "x"))) <@?=> Set.singleton 0 -- TODO: we don't want the "forall y" to be a redex, do we? It is only a rename, and not blocking anything yet... -- 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