We now carry two rule schemas. Normalization rules in resources/normalize/*.yaml use name/pattern/result with optional when/where/having (parsed into Yaml.Rule, src/Yaml.hs:201), while morphing, contextualization and dataization use the inference-rule form match + e-match/c-match + n-result/c-result/d-result + premises (Yaml.MorphRule/ContextualizeRule/DataizeRule, src/Yaml.hs:226-395). The split also forks the LaTeX backend: normalize rules render through explainRule/trrule (src/LaTeX.hs:356-453), the other three through the shared inference/premiseToLatex helpers (src/LaTeX.hs:374-427).
Migrating normalization to the premise-conclusion schema would give one uniform rule format across all five reduction systems and one uniform LaTeX inference-rule output, letting explainRule/trrule collapse into inference. The mapping is clean: conditionless rules (copy, dc, dd, dca, stay, null) become premise-less axioms; when/having become the side condition above the line; and dot.yaml's where (a contextualize build-term call) becomes a genuine premise, 𝒞(𝑛, formation) ⟿ 𝑒.
One caveat to settle before coding: normalization is a rewriting relation — the engine searches for any redex anywhere and iterates to a fixpoint (isNF, matchesAnyNormalizationRule in src/Rule.hs:42-73) — whereas 𝕄/𝒞/𝔻 are structural-recursive judgments. So this migration touches the rule schema and LaTeX only, not the rewriting engine, and the issue should decide whether to unify the conclusion's relation symbol (a one-step rewrite ↦) with the recursive ⟿ of 𝕄/𝒞/𝔻 or keep normalization's relation distinct while sharing the inference-rule layout. Concrete fix scope: add the new normalize schema and parser in src/Yaml.hs, update consumers (src/Rule.hs, src/Rewriter.hs), and fold the two LaTeX paths into inference.
Maybe we can even merge all rules into normalize.yaml single file.
We now carry two rule schemas. Normalization rules in
resources/normalize/*.yamlusename/pattern/resultwith optionalwhen/where/having(parsed intoYaml.Rule, src/Yaml.hs:201), while morphing, contextualization and dataization use the inference-rule formmatch+e-match/c-match+n-result/c-result/d-result+premises(Yaml.MorphRule/ContextualizeRule/DataizeRule, src/Yaml.hs:226-395). The split also forks the LaTeX backend: normalize rules render throughexplainRule/trrule(src/LaTeX.hs:356-453), the other three through the sharedinference/premiseToLatexhelpers (src/LaTeX.hs:374-427).Migrating normalization to the premise-conclusion schema would give one uniform rule format across all five reduction systems and one uniform LaTeX inference-rule output, letting
explainRule/trrulecollapse intoinference. The mapping is clean: conditionless rules (copy,dc,dd,dca,stay,null) become premise-less axioms;when/havingbecome the side condition above the line; anddot.yaml'swhere(acontextualizebuild-term call) becomes a genuine premise, 𝒞(𝑛, formation) ⟿ 𝑒.One caveat to settle before coding: normalization is a rewriting relation — the engine searches for any redex anywhere and iterates to a fixpoint (
isNF,matchesAnyNormalizationRulein src/Rule.hs:42-73) — whereas 𝕄/𝒞/𝔻 are structural-recursive judgments. So this migration touches the rule schema and LaTeX only, not the rewriting engine, and the issue should decide whether to unify the conclusion's relation symbol (a one-step rewrite ↦) with the recursive ⟿ of 𝕄/𝒞/𝔻 or keep normalization's relation distinct while sharing the inference-rule layout. Concrete fix scope: add the new normalize schema and parser in src/Yaml.hs, update consumers (src/Rule.hs, src/Rewriter.hs), and fold the two LaTeX paths intoinference.Maybe we can even merge all rules into
normalize.yamlsingle file.