From e0e54d292e1ba4661ae715bbe74b669cf12dfe67 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Mon, 5 Jun 2023 20:55:33 +0100 Subject: [PATCH] WIP: do not evaluate under binders (except lets) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This change means our EvalFull is "closed evaluation", rather than "open evaluation". Note that we must evaluate under (various flavours of) `let` bindings since we need substitute usages of these variables: we do not want to consider `let x = 1 in x + x` to be stuck, but we are happy to consider `λx.MkPair x (not True)` to be stuck. The main reason to do this is so that evaluations of programs-in-construction (especially recursive ones) do not pointlessly blow up in size: if `even` and `odd` are defined recursively, then evaluating `even` would evaluate under the lambda and inside case branches, expanding `odd` and recursing; when it eventually times out one would have a big tree with many unrolled copies of `even` and `odd`, which is not very illuminating. Note that we do not evaluate in the RHS of pattern match branches which bind variables, for the same reason as we do not evaluate under lambdas; for consistency we also do not evaluate in the RHS of branches which do not bind variables. Signed-off-by: Ben Price --- primer/src/Primer/Eval/NormalOrder.hs | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs index 2666b9765..b3e4583fa 100644 --- a/primer/src/Primer/Eval/NormalOrder.hs +++ b/primer/src/Primer/Eval/NormalOrder.hs @@ -44,6 +44,8 @@ import Primer.Core ( App, Case, Hole, + LAM, + Lam, Let, LetType, Letrec @@ -164,7 +166,7 @@ foldMapExpr extract topDir = flip evalAccumT mempty . go . (topDir,) . focus _ -> msum $ (goType =<< focusType' ez) - : map (go <=< hoistAccum) (exprChildren dez) + : map (go <=< hoistAccum) (exprChildrenClosed dez) goType :: TypeZ -> AccumT Cxt f a goType tz = readerToAccumT (ReaderT $ extract.ty tz) @@ -313,6 +315,17 @@ exprChildren (d, ez) = addBinds ez bs pure (d', c) +-- Extract the children of the current focus, except those under an "unknown" binder, +-- i.e. we extract the body of a let but not the body of a lambda, or the RHS of case branches. +-- This is used to restrict our evaluation to "closed evaluation". +-- NB: for consistency we skip all case branches, not just those that bind a variable. +exprChildrenClosed :: (Dir, ExprZ) -> [Accum Cxt (Dir, ExprZ)] +exprChildrenClosed (d, ez) = case target ez of + Lam{} -> [] + LAM{} -> [] + Case{} -> take 1 $ exprChildren (d, ez) -- just the scrutinee + _ -> exprChildren (d, ez) + typeChildren :: TypeZ -> [Accum Cxt TypeZ] typeChildren tz = children' tz <&> \c -> do