Skip to content

Commit

Permalink
refactor: Eval.NormalOrder's special 'subst' handling is now unneeded
Browse files Browse the repository at this point in the history
This is because we "push down lets", rather than doing long-range
substitutions. This means that all our rules are local, so we do not
need two eval modes "normal" and "substitution".

Signed-off-by: Ben Price <[email protected]>
  • Loading branch information
brprice committed Aug 14, 2023
1 parent ac6afaf commit e43f9d7
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 18 deletions.
6 changes: 1 addition & 5 deletions primer/src/Primer/Eval.hs
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ import Primer.Eval.Detail (
)
import Primer.Eval.EvalError (EvalError (..))
import Primer.Eval.NormalOrder (
FMExpr (FMExpr, expr, subst, substTy, ty),
FMExpr (FMExpr, expr, ty),
foldMapExpr,
singletonCxt,
)
Expand Down Expand Up @@ -117,8 +117,6 @@ findNodeByID i =
FMExpr
{ expr = \ez d c -> if getID ez == i then Just (c, Left (d, ez)) else Nothing
, ty = \tz c -> if getID tz == i then Just (c, Right tz) else Nothing
, subst = Nothing
, substTy = Nothing
}

-- We hardcode a permissive set of options for the interactive eval
Expand Down Expand Up @@ -148,8 +146,6 @@ redexes tydefs globals =
FMExpr
{ expr = \ez d -> liftMaybeT . runReaderT (getID ez <$ viewRedex evalOpts tydefs globals d (target ez))
, ty = \tz -> runReader (whenJust (getID tz) <$> viewRedexType evalOpts (target tz))
, subst = Nothing
, substTy = Nothing
}
where
liftMaybeT :: Monad m' => MaybeT m' a -> ListT m' a
Expand Down
17 changes: 4 additions & 13 deletions primer/src/Primer/Eval/NormalOrder.hs
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,6 @@ import Primer.Core (
LetType,
Letrec
),
TyVarName,
Type,
Type' (
TLet
),
Expand Down Expand Up @@ -115,11 +113,10 @@ foldMapExpr extract topDir = go mempty . (topDir,) . focus
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 = (d', b)})) -> goSubst bindingVL b d' $ cxtAddLet bindingVL lets
<|> case viewLet dez of
-- Prefer to compute inside the body of a let, but otherwise compute in the binding
-- NB: we never push lets into lets, so the Cxt is reset for non-body children
(Nothing, Just (ViewLet{bindingVL, bodyVL, typeChildrenVL, termChildrenVL})) ->
Just (ViewLet{bindingVL, bodyVL, typeChildrenVL, termChildrenVL}) ->
msum $
go (cxtAddLet bindingVL lets) bodyVL
: map (goType mempty) typeChildrenVL
Expand All @@ -134,19 +131,15 @@ foldMapExpr extract topDir = go mempty . (topDir,) . focus
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 -> goSubstTy a t bz lets
(Nothing, TLet _ a t _body)
<|> case target tz of
TLet _ a t _body
-- Prefer to compute inside the body of a let, but otherwise compute in the binding
| [tz', bz] <- typeChildren tz -> goType (cxtAddLet (LetTyBind $ LetTypeBind a t) lets) bz <|> goType mempty tz'
_ -> msum $ map (goType mempty) $ typeChildren tz

data FMExpr m = FMExpr
{ expr :: ExprZ -> Dir -> Cxt -> m
, ty :: TypeZ -> Cxt -> m
, subst :: Maybe (LetBinding -> ExprZ {- The body of the let-} -> Dir -> Cxt -> m)
, substTy :: Maybe (TyVarName -> Type -> TypeZ -> Cxt -> m)
}

focusType' :: MonadPlus m => ExprZ -> m TypeZ
Expand All @@ -167,8 +160,6 @@ findRedex opts tydefs globals =
( FMExpr
{ expr = \ez d -> runReaderT (RExpr ez <$> viewRedex opts tydefs globals d (target ez))
, ty = \tz -> hoistMaybe . runReader (RType tz <<$>> viewRedexType opts (target tz))
, subst = Nothing
, substTy = Nothing
}
)

Expand Down

0 comments on commit e43f9d7

Please sign in to comment.