From ac6afaf4499063e2717e8956b07bef815ccf45fc Mon Sep 17 00:00:00 2001 From: Ben Price Date: Thu, 13 Jul 2023 14:08:49 +0100 Subject: [PATCH] fix: Eval.Cxt is a list, can record shadowed lets This fixes a rare issue that if one has two adjacent lets with the same name, we would only record one of them in the `Cxt`, and thus miscalculate whether a binder they immediately contain needs to be renamed before we can push the lets under. Signed-off-by: Ben Price --- primer/src/Primer/Eval/NormalOrder.hs | 21 ++------------------ primer/src/Primer/Eval/Redex.hs | 23 +++++++++------------- primer/test/Tests/Eval.hs | 28 +++++++++++++-------------- 3 files changed, 25 insertions(+), 47 deletions(-) diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs index 726385948..94a088327 100644 --- a/primer/src/Primer/Eval/NormalOrder.hs +++ b/primer/src/Primer/Eval/NormalOrder.hs @@ -13,13 +13,7 @@ module Primer.Eval.NormalOrder ( import Foreword hiding (hoistAccum) import Control.Monad.Log (MonadLog, WithSeverity) -import Control.Monad.Trans.Accum ( - Accum, - add, - execAccum, - ) import Control.Monad.Trans.Maybe (MaybeT) -import Data.Map qualified as M import Primer.Core ( Expr, Expr' ( @@ -52,7 +46,6 @@ import Primer.Eval.Redex ( viewRedexType, ) import Primer.Log (ConvertLogMessage) -import Primer.Name (Name) import Primer.TypeDef ( TypeDefMap, ) @@ -65,7 +58,6 @@ import Primer.Zipper ( down, focus, focusType, - letBindingName, right, target, ) @@ -208,14 +200,5 @@ exprChildren (d, ez) = typeChildren :: TypeZ -> [TypeZ] typeChildren = children' -addBinds :: i -> [Either Name LetBinding] -> Accum Cxt () -addBinds _ bs = do - add $ - Cxt $ - M.fromList $ - bs <&> \case - Left n -> (n, Nothing) - Right l -> (letBindingName l, Just l) - -singletonCxt :: 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/Redex.hs b/primer/src/Primer/Eval/Redex.hs index 27292db8f..1425a5adc 100644 --- a/primer/src/Primer/Eval/Redex.hs +++ b/primer/src/Primer/Eval/Redex.hs @@ -50,7 +50,6 @@ import Optics ( (<%), _1, _2, - _Just, ) import Primer.Core ( Bind, @@ -637,18 +636,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} --- TODO: don't need to record nearly so much anymore (a list of directly-enclosing let bindings would be good enough) --- This will be addressed in the next two commits --- We record each directly-enclosing let binder, along with its let-bound RHS (wrapped in @Just@ for historical reasons) --- Invariant: lookup x c == Just (Just l) ==> letBindingName l == x +-- We record each directly-enclosing let binding -- By "directly enclosing" we mean "those which may be pushed into this term" -newtype Cxt = Cxt (M.Map Name (Maybe LetBinding)) - -- 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)) +-- NB: we do not care about ordering +newtype Cxt = Cxt [LetBinding] + deriving newtype (Semigroup, Monoid) cxtAddLet :: LetBinding -> Cxt -> Cxt -cxtAddLet l (Cxt c) = Cxt $ M.insert (letBindingName l) (Just l) c +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, @@ -923,19 +918,19 @@ viewRedexType opts = \case letTypeBindingName' (LetTypeBind n _) = n lookupEnclosingLet :: Name -> Cxt -> Maybe LetBinding -lookupEnclosingLet n (Cxt cxt) = join $ M.lookup n cxt +lookupEnclosingLet n (Cxt cxt) = find ((== n) . letBindingName) cxt --- We may want to push some let bindings (some subset of the Cxt) under a +-- 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 (_Just % (to letBindingName `summing` _freeVarsLetBinding))) cxt + pure $ foldMap' (setOf (to letBindingName `summing` _freeVarsLetBinding)) cxt cxtToAvoidTy :: MonadReader Cxt m => m (S.Set TyVarName) cxtToAvoidTy = do Cxt cxt <- ask - pure $ foldMap' (setOf (_Just % _LetTyBind % _LetTypeBind % (_1 `summing` _2 % getting _freeVarsTy % _2))) cxt + 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 => RunRedexOptions -> Redex -> m (Expr, EvalDetail) diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs index 78ecc49e7..b2788dc25 100644 --- a/primer/test/Tests/Eval.hs +++ b/primer/test/Tests/Eval.hs @@ -203,17 +203,17 @@ 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) 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) result @?= Left NotRedex @@ -770,18 +770,18 @@ unit_findNodeByID_letrec = do t = create' $ tcon' ["M"] "T" case findNodeByID 0 Syn expr of Just (Cxt locals, Left (_, z)) -> do - assertBool "no enclosing lets 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 (Cxt locals, Left (_, z)) -> do target z ~= x - assertBool "no enclosing lets at node 1" $ Map.null locals + 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 enclosing lets 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 @@ -813,13 +813,13 @@ 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" @@ -865,8 +865,8 @@ 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 _) - | Nothing <- Map.lookup "x" locals -> + Just (locals, Left _) + | Nothing <- lookupEnclosingLet "x" locals -> pure () | otherwise -> assertFailure "expected 'x' to not be bound by an immediately enclosing let, but it was" _ -> assertFailure "Expected to find the lvar 'x'" @@ -879,7 +879,7 @@ unit_findNodeByID_scoping_2 = do pure (b, e) case findNodeByID 4 Syn expr of Just (locals@(Cxt locals'), Left _) - | Map.size locals' == 1 + | length locals' == 2 , lookupEnclosingLet "x" locals == Just (LetBind "x" bind) -> pure () Just (_, Left _) -> assertFailure "Expected to have inner let binding of 'x' reported" @@ -898,7 +898,7 @@ unit_findNodeByID_capture = in do case findNodeByID varOcc Syn expr of Just (locals@(Cxt locals'), Left _) - | Map.size locals' == 0 + | null locals' , Nothing <- lookupEnclosingLet "x" locals -> pure () | otherwise -> assertFailure "expected 'x' to not be bound by an immediately enclosing let, but it was" @@ -917,7 +917,7 @@ unit_findNodeByID_capture_type = in do case findNodeByID varOcc Syn expr of Just (locals@(Cxt locals'), Right _) - | Map.size locals' == 0 + | null locals' , Nothing <- lookupEnclosingLet "x" locals , Nothing <- lookupEnclosingLet "z" locals -> pure ()