WIP: do not evaluate under binders (except lets)

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

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