feat(#912): migrate normalization rules to the premise-conclusion schema

[yegor256]

Closes #912.

Normalization rules now use the same premise-conclusion schema as 𝕄/𝒞/𝔻, and explain emits one uniform inference-rule LaTeX layout across all five reduction systems — explainRule/trrule collapse into the shared inference helper.

What changed

• src/Yaml.hs — FromJSON Rule is now a custom parser that accepts the premise-conclusion keys (match + premises) as well as the legacy keys (pattern + where). A premises list desugars (premiseToExtra) into the build-term where extras the engine already runs, so the rewriting engine itself is untouched. verb/verbArgs moved here from Dataize so both the desugaring and the dataizer share them.
• src/LaTeX.hs — explainRule folds into inference: when/having become the side condition above the line, where extensions become premise judgments (so dot's contextualize shows as 𝒞(n, formation) ⟿ e), and the conclusion is the one-step rewrite 𝒩(match) ⟿ result. trrule and extraArgumentsToLatex are removed.
• resources/normalize/*.yaml — migrated to match; dot.yaml's where contextualize call is now a genuine premises entry.
• README.md — the explain --normalize example now shows the inference-rule output (consistent with the already-updated --contextualize example).
• test/CLISpec.hs — explain expectations updated to the \begin{phinoInference} format.

Design decisions (the issue left two open)

These were the two forks the issue raised; I picked defensible defaults and call them out here so they can be revisited in review:

1. Scope — additive, not a hard rename. The Yaml.Rule schema is also the general rewriting-rule schema used by the user-facing --rule feature and ~50+ test packs (condition-packs/, rewriter-packs/, cli/). A hard rename would break all of those. Instead the parser accepts both schemas, the built-in resources/normalize/*.yaml files are migrated to the new form, and nothing else breaks. Because premises desugar to the existing where extras, src/Rule.hs and src/Rewriter.hs needed no changes — the engine keeps consuming where extras unchanged. (Note: where/Extra is strictly more general than premises — it supports arbitrary build-term functions like sed/concat — which is why it stays the engine mechanism rather than being replaced.)
2. Relation symbol — shared 𝒩 macro, no new symbol. The conclusion renders through \phinoNormalize{lhs}{rhs}, the same macro the 𝒩 premises of the other systems already use, so the inference layout is shared without inventing a separate one-step relation symbol. This keeps the relation in the 𝒩 family and needs no new .sty macro. Happy to switch to a distinct ↦ macro or unify with ⟿ if preferred.

Verification

• cabal test --ghc-options=-Werror → 1073 examples, 0 failures
• fourmolu --mode check and hlint clean on all changed files
• Manually ran phino explain --normalize (inference output incl. the dot premise) and a rewrite --normalize (the dot rule fires correctly end-to-end)

🤖 Generated with Claude Code

https://claude.ai/code/session_01NZ7UYvDx9A7XhFyc4NSPy9

---

Generated by Claude Code

[github-actions]

Benchmark comparison

Regression threshold: +20%. Same-runner A/B against the PR merge-base; the bench fixture is frozen across both runs.

Bench	base (us)	head (us)	delta
parse/phi	147781.03	149364.38	+1.1%
parse/xmir	766436.41	778122.53	+1.5%
print/salty/multiline	1355928.08	1366585.94	+0.8%
print/sweet/flat	381791.78	380222.16	-0.4%
print/sweet/multiline	392073.47	389797.40	-0.6%
rewrite/normalize	42579.83	41229.02	-3.2%

OK: no case regressed above the +20% threshold.

[yegor256]

@maxonfjvipon good?

[maxonfjvipon]

@yegor256 As I understand we still have some sort of a bridge? Are we planning to get rid of it? If so let's add pdd todo

[maxonfjvipon]

@yegor256 Let's add function types to all of the functions

[yegor256]

Added type signatures to the extraToLatex helpers. Also went further per @yegor256's note: dropped the legacy pattern/where schema entirely — the parser now accepts only match/premises, and all rule YAML (built-in normalization rules plus the test/--rule packs) is migrated. A premise is either a reduction judgment (verb-keyed) or a general build-term call (meta/function/args), so sed/concat/etc. still work and the rewriting engine is unchanged.

---

Generated by Claude Code

[yegor256]

Good questions — two clarifications:

ExtraArgument is still parsed and load-bearing, so we can't just drop it. The general build-term premise form — { meta, function, args }, used by sed / concat / size / random-tau / dataize / etc. — is parsed straight into Extra (FromJSON Extra/FromJSON ExtraArgument), and the rewriting engine consumes [Extra] directly in extraSubstitutions. So it isn't only a bridge; it's the engine's representation for build-term premises.

The real bridge is premiseToExtra: the verb-keyed premises (contextualize:/morph:/…) are parsed as the typed Operation/Premise (shared with 𝕄/𝒞/𝔻) and then desugared into Extra. So there are two premise representations and one converter between them. Fully removing it means having the engine consume Premise directly and retiring Extra/ExtraArgument — a larger change than this PR, so I've added a pdd todo at premiseToExtra (@todo #912:60min …) to track it. Happy to do it here instead if you'd prefer.

having is untouched — still parsed (o .:? "having") and applied as the post-premises side condition in Rule.hs (meetMaybeCondition rule.having after the premises run). The new schema only renamed pattern→match and where→premises; when/having are unchanged, so hone-maven-plugin keeps working. It's covered after the migration by part-of-after.yaml, which uses match + a concat premise + a having: { not: { part-of: … } } guard.

---

Generated by Claude Code

[yegor256]

@maxonfjvipon here's a summary of what this PR now does, after folding in your review feedback.

Goal (#912)

Migrate normalization rules to the same premise-conclusion schema used by 𝕄/𝒞/𝔻, and collapse the forked LaTeX backend so all five reduction systems render through one inference-rule layout.

What changed

• One rule schema. Yaml.Rule now uses match + premises (was pattern + where). The legacy keys are gone — the parser accepts only the new schema. Per @yegor256's note, this removes the old machinery entirely rather than keeping a dual schema.

• Premises subsume the old where. A premise is either:

  • a reduction judgment, keyed by its verb (contextualize / morph / normalize / evaluate / dataize), or
  • a general build-term call (meta / function / args).

  Both desugar to the same Extra the rewriting engine already consumes, so sed / concat / size / random-tau / etc. keep working and the rewriting engine is untouched — only the schema and the LaTeX backend changed.

• Unified LaTeX. explainRule/trrule are gone; normalization rules render through the shared inference helper, emitting \begin{phinoNormalizationInference} consistent with the phino{Morphing,Dataization,Contextualization}Inference environments from fix(#917): emit per-kind phino inference LaTeX environments #918. when/having become the side condition, premises become judgments (so dot's contextualize shows as 𝒞(n, formation) ⟿ e), and the conclusion is 𝒩(match) ⟿ result.

• All Y.Rule YAML migrated: built-in resources/normalize/*, plus test-resources/{yaml-packs,yaml-typos,cli}/* and the inline custom: rules in rewriter-packs/custom/*. condition-packs use a different schema (ConditionPack) and were intentionally left alone.

• README rule example + schema docs updated to match/premises.

• Review fix: added type signatures to the extraToLatex helpers.

One open call worth your eyes

The normalization conclusion reuses the existing \phinoNormalize{lhs}{rhs} macro (the same one the 𝒩 premises of the other systems use) rather than introducing a distinct one-step ↦ relation symbol — sharing the layout without a new macro. Easy to switch to a separate symbol if you'd prefer the one-step relation be visually distinct from the recursive ⟿.

CI

Green locally on GHC 9.8.4: cabal test --ghc-options=-Werror (1073 examples, 0 failures), fourmolu clean, hlint 0 hints. (The latex smoke test and hlint both needed small follow-ups — the latter because dropping the pattern field name let hlint fully parse the module and surface latent Eta reduce hints on the phino* printf helpers, now point-free.)

---

Generated by Claude Code

[maxonfjvipon]

@yegor256 What about ExtraArgument type? It seems it's not parsed anymore and used only for bridge from new premises front end to old when+where front end? If so, it would be better to get rid of it. Also what about having? How this new premises approach resolves it? We need it for hone-maven-plugin