Problem
The non-evaluator attribute marks a function so it is not evaluated by the LLVM backend. However, in practice, marking a single function as non-evaluator is not enough — every function in the call chain above it must also be manually marked, otherwise the Haskell backend will still send the caller to the LLVM backend, which then encounters a non-evaluator function it cannot handle.
Example:
syntax Int ::= A(Int) [function, non-evaluator]
syntax Int ::= B(Int) [function]
rule B(X) => A(X) +Int 1
A is marked non-evaluator
B is not marked non-evaluator
- When the Haskell backend simplifies
B(42), since B is not non-evaluator, it sends B(42) to the LLVM backend
- The LLVM backend attempts to evaluate, unfolds the rule, and encounters
A(42) — but A is non-evaluator and the LLVM backend cannot handle it correctly
- Workaround: manually add
non-evaluator to B as well. But then all callers of B also need it, and so on — propagating up the entire call chain
The same issue occurs when a requires clause references a non-evaluator function.
This was discovered in the mir-semantics project (EXPERIMENT-no-llvm-kompile-updated branch), which has many functions unsuitable for LLVM backend execution.
Expected Behavior
non-evaluator should not require manual propagation. Possible directions:
- The compiler automatically analyzes the call graph and propagates the attribute
- The Haskell backend recognizes when a term contains
non-evaluator functions and handles them itself
- The LLVM backend gracefully returns unevaluated terms when encountering
non-evaluator functions
Suggested First Steps
Before choosing a solution, some investigation is needed:
- Find the original PR/issue that introduced
non-evaluator to understand the design intent
- Survey
non-evaluator usage in projects other than mir-semantics — do they encounter the same propagation problem?
- Assess the semantics of
non-evaluator in concrete execution (pure LLVM backend) scenarios (currently a potential concern, no observed issues yet)
Acceptance Criteria
Problem
The
non-evaluatorattribute marks a function so it is not evaluated by the LLVM backend. However, in practice, marking a single function asnon-evaluatoris not enough — every function in the call chain above it must also be manually marked, otherwise the Haskell backend will still send the caller to the LLVM backend, which then encounters anon-evaluatorfunction it cannot handle.Example:
Ais markednon-evaluatorBis not markednon-evaluatorB(42), sinceBis notnon-evaluator, it sendsB(42)to the LLVM backendA(42)— butAisnon-evaluatorand the LLVM backend cannot handle it correctlynon-evaluatortoBas well. But then all callers ofBalso need it, and so on — propagating up the entire call chainThe same issue occurs when a
requiresclause references anon-evaluatorfunction.This was discovered in the mir-semantics project (
EXPERIMENT-no-llvm-kompile-updatedbranch), which has many functions unsuitable for LLVM backend execution.Expected Behavior
non-evaluatorshould not require manual propagation. Possible directions:non-evaluatorfunctions and handles them itselfnon-evaluatorfunctionsSuggested First Steps
Before choosing a solution, some investigation is needed:
non-evaluatorto understand the design intentnon-evaluatorusage in projects other than mir-semantics — do they encounter the same propagation problem?non-evaluatorin concrete execution (pure LLVM backend) scenarios (currently a potential concern, no observed issues yet)Acceptance Criteria
non-evaluatorintroduction history and usage across projects