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 <[email protected]>

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]

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)

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