refactor: simplify Eval.Cxt

Now we are pushing down lets, we do not need so much information about bindings. In particular, we do not need to record the original binding location, or the original binding's context, since we do not do long-range substitution where care is needed to avoid capture. Signed-off-by: Ben Price <[email protected]>
hackworthltd · Aug 14, 2023 · b65cc8a · b65cc8a
1 parent 93cae09
commit b65cc8a
Show file tree

Hide file tree

Showing 4 changed files with 29 additions and 68 deletions.
diff --git a/primer/src/Primer/Eval.hs b/primer/src/Primer/Eval.hs
@@ -22,7 +22,7 @@ module Primer.Eval (
   -- Only exported for testing
   Cxt (Cxt),
   singletonCxt,
-  getNonCapturedLocal,
+  lookupEnclosingLet,
   tryReduceExpr,
   tryReduceType,
   findNodeByID,
@@ -67,7 +67,7 @@ import Primer.Eval.Redex (
   MonadEval,
   RunRedexOptions (RunRedexOptions, pushAndElide),
   ViewRedexOptions (ViewRedexOptions, aggressiveElision, pushMulti),
-  getNonCapturedLocal,
+  lookupEnclosingLet,
   runRedex,
   runRedexTy,
   viewRedex,

diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs
@@ -17,7 +17,6 @@ import Control.Monad.Trans.Accum (
   Accum,
   add,
   execAccum,
-  look,
  )
 import Control.Monad.Trans.Maybe (MaybeT)
 import Data.Map qualified as M
@@ -32,13 +31,11 @@ import Primer.Core (
     LetType,
     Letrec
   ),
-  HasID,
   TyVarName,
   Type,
   Type' (
     TLet
   ),
-  getID,
  )
 import Primer.Def (
   DefMap,
@@ -211,16 +208,14 @@ exprChildren (d, ez) =
 typeChildren :: TypeZ -> [TypeZ]
 typeChildren = children'
 
-addBinds :: HasID i => i -> [Either Name LetBinding] -> Accum Cxt ()
-addBinds i' bs = do
-  let i = getID i'
-  cxt <- look
+addBinds :: i -> [Either Name LetBinding] -> Accum Cxt ()
+addBinds _ bs = do
   add $
     Cxt $
       M.fromList $
         bs <&> \case
-          Left n -> (n, (Nothing, i, cxt))
-          Right l -> (letBindingName l, (Just l, i, cxt))
+          Left n -> (n, Nothing)
+          Right l -> (letBindingName l, Just l)
 
-singletonCxt :: HasID i => i -> LetBinding -> Cxt
+singletonCxt :: i -> LetBinding -> Cxt
 singletonCxt i l = addBinds i [Right l] `execAccum` mempty
diff --git a/primer/src/Primer/Eval/Redex.hs b/primer/src/Primer/Eval/Redex.hs
@@ -20,7 +20,7 @@ module Primer.Eval.Redex (
   EvalLog (..),
   MonadEval,
   -- Exported for testing
-  getNonCapturedLocal,
+  lookupEnclosingLet,
 ) where
 
 import Foreword
@@ -34,13 +34,11 @@ 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,
   folded,
   getting,
   ifiltered,
@@ -642,21 +640,15 @@ viewCaseRedex tydefs = \case
 -- 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)
--- and its original binding location and  context (to be able to detect capture)
--- Invariant: lookup x c == Just (Just l,_,_) ==> letBindingName l == x
+-- Invariant: lookup x c == Just (Just l) ==> letBindingName l == x
 -- By "directly enclosing" we mean "those which may be pushed into this term"
-newtype Cxt = Cxt (M.Map Name (Maybe LetBinding, ID, Cxt))
+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, ID, Cxt))
+  deriving (Semigroup, Monoid) via Dual (M.Map Name (Maybe LetBinding))
 
 cxtAddLet :: LetBinding -> Cxt -> Cxt
--- TODO: the 0, mempty are LIES, but we never care about these positions.
--- This will be addressed in the next commit
-cxtAddLet l (Cxt c) = Cxt $ M.insert (letBindingName l) (Just l, 0, mempty) c
-
-lookup :: Name -> Cxt -> Maybe (Maybe LetBinding, ID, Cxt)
-lookup n (Cxt cxt) = M.lookup n cxt
+cxtAddLet l (Cxt c) = Cxt $ M.insert (letBindingName l) (Just l) c
 
 -- This notices all redexes
 -- Note that if a term is not a redex, but stuck on some sub-term,
@@ -930,32 +922,20 @@ viewRedexType opts = \case
     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) = join $ M.lookup n cxt
 
 -- We may want to push some let bindings (some subset of 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 (_1 % _Just % (to letBindingName `summing` _freeVarsLetBinding))) cxt
+  pure $ foldMap' (setOf (_Just % (to letBindingName `summing` _freeVarsLetBinding))) cxt
 
 cxtToAvoidTy :: MonadReader Cxt m => m (S.Set TyVarName)
 cxtToAvoidTy = do
   Cxt cxt <- ask
-  pure $ foldMap' (setOf (_1 % _Just % _LetTyBind % _LetTypeBind % (_1 `summing` _2 % getting _freeVarsTy % _2))) cxt
+  pure $ foldMap' (setOf (_Just % _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
@@ -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
@@ -33,13 +32,11 @@ import Primer.Core (
   GlobalName (baseName, qualifiedModule),
   ID,
   Kind' (KFun, KType),
-  LocalName,
   Pattern (PatCon, PatPrim),
   PrimCon (PrimChar),
   Type,
   Type' (TCon, TEmptyHole, TFun, TVar),
   getID,
-  unLocalName,
   unsafeMkGlobalName,
   _id,
  )
@@ -62,7 +59,7 @@ import Primer.Eval (
   LocalVarInlineDetail (..),
   PushLetDetail (..),
   findNodeByID,
-  getNonCapturedLocal,
+  lookupEnclosingLet,
   redexes,
   singletonCxt,
   step,
@@ -93,7 +90,6 @@ import Primer.TypeDef (
  )
 import Primer.Typecheck (typeDefs)
 import Primer.Zipper (
-  LetBinding,
   LetBinding' (LetBind, LetTyBind, LetrecBind),
   LetTypeBinding' (LetTypeBind),
   target,
@@ -767,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")
@@ -800,9 +786,9 @@ unit_findNodeByID_letrec = do
   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
@@ -817,8 +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 (_, LetBind _ e) -> do
+      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"
@@ -849,7 +835,7 @@ unit_findNodeByID_2 = do
         pure (x_, t_, e)
   case findNodeByID 0 Syn expr of
     Just (locals, Right z) -> do
-      case lookupNonCaptured "x" locals of
+      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
@@ -867,8 +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 (_, LetTyBind (LetTypeBind _ e)) -> do
+      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"
@@ -894,7 +880,7 @@ unit_findNodeByID_scoping_2 = do
   case findNodeByID 4 Syn expr of
     Just (locals@(Cxt locals'), Left _)
       | Map.size locals' == 1
-      , (snd <$> lookupNonCaptured "x" locals) == Just (LetBind "x" bind) ->
+      , 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'"
@@ -913,7 +899,7 @@ unit_findNodeByID_capture =
         case findNodeByID varOcc Syn expr of
           Just (locals@(Cxt locals'), Left _)
             | Map.size locals' == 0
-            , Nothing <- lookupCaptured "x" locals ->
+            , 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'"
@@ -932,8 +918,8 @@ unit_findNodeByID_capture_type =
         case findNodeByID varOcc Syn expr of
           Just (locals@(Cxt locals'), Right _)
             | Map.size locals' == 0
-            , Nothing <- lookupCaptured "x" locals
-            , Nothing <- lookupCaptured "z" locals ->
+            , Nothing <- lookupEnclosingLet "x" locals
+            , Nothing <- lookupEnclosingLet "z" 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'"