feat: optionally do not evaluate under binders (except lets) #1055

This is a stepping-stone to making an option to not evaluate under binders for EvalFull. BREAKING CHANGE: This adds a new field to `EvalFullReq`, which is exposed in the APIs. Since it is an extra optional argument in the OpenAPI, old clients of the OpenAPI will still continue to work (this is not true of the richly-typed API). Signed-off-by: Ben Price <[email protected]>

This change means our EvalFull is "closed evaluation", rather than "open evaluation". 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 the reduction of "pushing a let down", e.g. `let x = t in f s ~> (let x = t in f) (let x = t in s)` happens at the `let` node, and thus is not "under" the `let x` binder. Note that we consider a "stack" of lets `let x=s in let y=t in r` to be one binder, so that we can (with `groupedLets = False`) reduce this by pushing the `let y` into the `r` (i.e. we don't count this as "under" the `let x` binder). We will not evaluate inside the `r`. 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]>

Signed-off-by: Ben Price <[email protected]>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: optionally do not evaluate under binders (except lets) #1055

feat: optionally do not evaluate under binders (except lets) #1055

Commits on Sep 14, 2023