NormalOrder; change handling of cxts to match push-down-lets. This "f…

…ixes" 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

@@ -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

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
 

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