Fix #361, ensure tester-constructor pairs simplify #364
Conversation
| match σ.config.factory.callOfLFunc e with | ||
| | some (op_expr, args, lfunc) => | ||
| let args := args.map (fun a => eval n' σ a) | ||
| let firstArgIsConstr := (args.head?.map (isConstrApp σ.config.factory)).getD false |
There was a problem hiding this comment.
Just checking: inline_if_constr is an attribute meaningful only for tester functions. This allows tester functions to be inlined if their (only) argument is a constructor (but not otherwise).
There was a problem hiding this comment.
Yes. In principle one could write a Factory function that evaluates on a constructor argument, but right now it is only meaningful for testers and eliminators.
| -- All arguments in the function call are concrete. | ||
| -- We can, provided a denotation function, evaluate this function | ||
| -- call. | ||
| ("eval_if_constr" ∈ lfunc.attr && firstArgIsConstr) then |
There was a problem hiding this comment.
And checking yet again: eval_if_constr is an attribute that's meaningful only for eliminator functions, and allows their concrete evaluation (via concreteEval) only if the first argument is a constructor.
|
Does it require a change in Strata/DL/Lambda/Semantics.lean? I think the |
Yes, that is a good point. |
3 participants
Issue #, if available: #361
Description of changes:
Changes concrete evaluator to simplify certain marked function applications when the first argument is a constructor, no matter if the arguments are values or not.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.