Goal: Implement language semantics, macro systems, and rewrite-based optimizations using higher-order pattern matching, strategy control (outermost-first, inner-strict, tactic combinations), confluence checks, and support for infinitary/regular infinite terms.
Futamura role
Implements the reduction steps of the specializer, a sub-component of the partial evaluation engine (2.2), also used by 0.1 (the graph reduction engine) for primitive evaluation rules.
-
Input
- Rewrite rules with patterns, guards, and conditions.
- Terms (including higher-order, regular infinite trees, suspended computations, "isolated" terms like a polynomial and an interval that identifies a root).
-
Processing
- Perform higher-order pattern matching; evaluate alternatives via logic engine, guards via meta-programming.
- Strategy control: outermost-first, strict inner-first, tactic combinations.
- Confluence checks where possible; if confluent, allow more aggressive strategy choices.
- Termination/normalization checks (when provable) or watchdogs/limits when not.
- Support infinitary/regular infinite terms, cycle condensation, meaningless term detection.
-
Output
- Normal form or partially normal form.
- Information about convergence, divergence, or ambiguity.
Goal: Implement language semantics, macro systems, and rewrite-based optimizations using higher-order pattern matching, strategy control (outermost-first, inner-strict, tactic combinations), confluence checks, and support for infinitary/regular infinite terms.
Futamura role
Implements the reduction steps of the specializer, a sub-component of the partial evaluation engine (2.2), also used by 0.1 (the graph reduction engine) for primitive evaluation rules.
Input
Processing
Output