phino 0.0.0.74 → 0.0.0.75

raw patch · 48 files changed

+1022/−368 lines, 48 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +78/−36
• phino.cabal +2/−2
• resources/alpha.yaml +0/−10
• resources/copy.yaml +0/−10
• resources/dataization.yaml +40/−0
• resources/dc.yaml +0/−6
• resources/dd.yaml +0/−6
• resources/dot.yaml +0/−14
• resources/miss.yaml +0/−14
• resources/morphing.yaml +48/−0
• resources/normalize/alpha.yaml +10/−0
• resources/normalize/copy.yaml +8/−0
• resources/normalize/dc.yaml +6/−0
• resources/normalize/dd.yaml +6/−0
• resources/normalize/dot.yaml +12/−0
• resources/normalize/miss.yaml +14/−0
• resources/normalize/null.yaml +6/−0
• resources/normalize/over.yaml +11/−0
• resources/normalize/phi.yaml +15/−0
• resources/normalize/stay.yaml +6/−0
• resources/normalize/stop.yaml +20/−0
• resources/null.yaml +0/−6
• resources/over.yaml +0/−11
• resources/phi.yaml +0/−15
• resources/stay.yaml +0/−6
• resources/stop.yaml +0/−20
• src/CLI/Helpers.hs +16/−1
• src/CLI/Parsers.hs +8/−0
• src/CLI/Runners.hs +13/−5
• src/CLI/Types.hs +2/−0
• src/CST.hs +16/−1
• src/Dataize.hs +145/−129
• src/Encoding.hs +3/−0
• src/Functions.hs +8/−1
• src/LaTeX.hs +90/−22
• src/Lining.hs +3/−0
• src/Matcher.hs +9/−14
• src/Parser.hs +1/−0
• src/Render.hs +9/−0
• src/Rewriter.hs +5/−4
• src/Rule.hs +94/−15
• src/Sugar.hs +3/−0
• src/Yaml.hs +133/−3
• test/CLISpec.hs +88/−14
• test/DataizeSpec.hs +82/−2
• test/MatcherSpec.hs +6/−0
• test/ParserSpec.hs +5/−0
• test/RewriterSpec.hs +1/−1

@@ -34,7 +34,7 @@  ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.0.73+cabal install --overwrite-policy=always phino-0.0.0.74 phino --version ``` @@ -205,7 +205,10 @@  ## Explain -You can _explain_ rewriting rule by printing them in [LaTeX][latex] format:+You can _explain_ the built-in rules by printing them in [LaTeX][latex]+format. Pass exactly one of `--normalize`, `--morph` or `--dataize` for+the rewriting, morphing (𝕄) or dataization (𝔻) rules (or `--rule` for a+custom rule file):  ```bash $ phino explain --normalize@@ -229,6 +232,42 @@ \end{tabular} ``` +The morphing and dataization rules are printed the same way:++```bash+$ phino explain --morph+\begin{tabular}{rl}+\trrule{Mprim}+  { \mathbb{M}( e ) }+  { e }+  { if $ e \in \mathcal{P} $ }+  { }+...+\trrule{Mphi}+  { \mathbb{M}( Q . \tau * t ) }+  { \mathbb{M}( e * t ) }+  { }+  { where $ e \coloneqq global( \tau ) $ }+\end{tabular}+```++```bash+$ phino explain --dataize+\begin{tabular}{rl}+\trrule{delta}+  { \mathbb{D}( [[ B_1, D> δ, B_2 ]] ) }+  { δ }+  { }+  { }+...+\trrule{none}+  { \mathbb{D}( e ) }+  { \varnothing }+  { }+  { }+\end{tabular}+```+ For more details, use `phino [COMMAND] --help` option.  ## Rule structure@@ -355,10 +394,13 @@  * `!a` || `𝜏` - attribute * `!e` || `𝑒` - any expression+* `!n` || `𝑛` - any expression that is already in normal form (behaves like+                `!e`/`𝑒`, but only binds a sub-expression in NF, so no explicit+                `nf:` guard is needed) * `!B` || `𝐵` - list of bindings * `!d` || `δ` - bytes in meta delta binding-* `!t` - tail after expression, sequence of applications and/or dispatches,-         must start only with dispatch+* `!t` - tail after expression, a possibly empty sequence of applications+         and/or dispatches * `!F` - function name in meta lambda binding  Every meta variable may also be used with an integer index, like `!B1` or `𝜏0`.@@ -388,55 +430,55 @@ === parse/phi ===   warmup:     3 iterations   batches:    10 x 1-  total:      1309885.482 μs-  avg:        130988.548 μs-  min:        119182.611 μs-  max:        164424.034 μs-  std dev:    17120.368 μs+  total:      1412671.918 μs+  avg:        141267.192 μs+  min:        127755.002 μs+  max:        177453.762 μs+  std dev:    17165.732 μs === parse/xmir ===   warmup:     3 iterations   batches:    10 x 1-  total:      8166516.875 μs-  avg:        816651.687 μs-  min:        746631.521 μs-  max:        905684.717 μs-  std dev:    58484.723 μs+  total:      7639818.091 μs+  avg:        763981.809 μs+  min:        708011.145 μs+  max:        797305.119 μs+  std dev:    24602.554 μs === rewrite/normalize ===   warmup:     3 iterations   batches:    10 x 1-  total:      1020794.192 μs-  avg:        102079.419 μs-  min:        98049.050 μs-  max:        109067.886 μs-  std dev:    2847.343 μs+  total:      426645.736 μs+  avg:        42664.574 μs+  min:        40102.854 μs+  max:        47835.610 μs+  std dev:    2300.441 μs === print/sweet/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      5308178.500 μs-  avg:        530817.850 μs-  min:        500095.243 μs-  max:        590475.507 μs-  std dev:    29328.246 μs+  total:      3941287.369 μs+  avg:        394128.737 μs+  min:        372511.010 μs+  max:        405677.385 μs+  std dev:    9679.300 μs === print/sweet/flat ===   warmup:     3 iterations   batches:    10 x 1-  total:      5104935.589 μs-  avg:        510493.559 μs-  min:        449111.602 μs-  max:        555034.745 μs-  std dev:    36795.722 μs+  total:      4011952.457 μs+  avg:        401195.246 μs+  min:        382116.656 μs+  max:        426194.357 μs+  std dev:    13451.138 μs === print/salty/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      15066270.227 μs-  avg:        1506627.023 μs-  min:        1427131.813 μs-  max:        1580723.339 μs-  std dev:    45705.458 μs+  total:      13481660.845 μs+  avg:        1348166.084 μs+  min:        1297555.496 μs+  max:        1397510.998 μs+  std dev:    35358.091 μs ```  The results were calculated in [this GHA job][benchmark-gha]-on 2026-06-03 at 13:35,+on 2026-06-08 at 09:53, on Linux with 4 CPUs.  <!-- benchmark_end -->@@ -472,4 +514,4 @@ [jna]: https://github.com/java-native-access/jna [jna-native]: https://github.com/java-native-access/jna/blob/master/src/com/sun/jna/Native.java [jeo]: https://github.com/objectionary/jeo-maven-plugin-[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/26888116250+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/27129589244

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.0.74+version: 0.0.0.75 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>@@ -12,7 +12,7 @@ copyright: 2025 Objectionary.com category: Language, Code Analysis build-type: Simple-extra-source-files: resources/*.yaml+extra-source-files: resources/*.yaml resources/normalize/*.yaml extra-doc-files: README.md  source-repository head

@@ -1,10 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----name: alpha-pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏2 ↦ 𝑒)-result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒)-when:-  eq:-    - index: 𝜏2-    - domain: 𝐵1

@@ -1,10 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----name: copy-pattern: ⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑒)-result: ⟦ 𝐵1, 𝜏 ↦ 𝑒, 𝐵2 ⟧-when:-  and:-    - xi-free: 𝑒-    - nf: 𝑒

@@ -0,0 +1,40 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# Dataization 𝔻 — applied top-to-bottom, first matching clause wins.++- name: delta+  description: '𝔻(⟦𝐵1, Δ ⤍ δ, 𝐵2⟧) ⟿ δ'+  match: ⟦𝐵1, Δ ⤍ δ, 𝐵2⟧+  then: δ++- name: box+  description: '𝔻(⟦𝐵1, φ ↦ e, 𝐵2⟧) ⟿ 𝔻(𝒞(e)) if [Δ, λ] ∩ (𝐵1 ∪ 𝐵2) = ∅'+  match: ⟦𝐵1, φ ↦ 𝑒, 𝐵2⟧+  where:+    - meta: 𝑒1+      function: contextualize+      args:+        - 𝑒+        - ⟦𝐵1, φ ↦ 𝑒, 𝐵2⟧+  when:+    disjoint:+      - [Δ, λ]+      - [𝐵1, 𝐵2]+  then:+    dataize: 𝑒1++- name: norm+  description: '𝔻(e) ⟿ 𝔻(𝕄(e)) if e ∉ 𝒫'+  match: 𝑒+  when:+    not:+      primitive: 𝑒+  then:+    dataize:+      morph: 𝑒++- name: none+  description: '𝔻(e) ⟿ nothing otherwise'+  match: 𝑒+  then: nothing

@@ -1,6 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----name: dc-pattern: ⊥(𝜏 ↦ 𝑒)-result: ⊥

@@ -1,6 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----name: dd-pattern: ⊥.𝜏-result: ⊥

@@ -1,14 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----name: dot-pattern: ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧.𝜏-result: 𝑒2(ρ ↦ ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧)-when:-  nf: 𝑒1-where:-  - meta: 𝑒2-    function: contextualize-    args:-      - 𝑒1-      - ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧

@@ -1,14 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----name: miss-pattern: ⟦𝐵⟧(𝜏 ↦ 𝑒)-result: ⊥-when:-  and:-    - not:-        in:-          - 𝜏-          - 𝐵-    - not:-        alpha: 𝜏

@@ -0,0 +1,48 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# Morphing 𝕄 — applied top-to-bottom, first matching clause wins.++- name: Mprim+  description: '𝕄(e) ⟿ e if e ∈ 𝒫'+  match: 𝑒+  when:+    primitive: 𝑒+  then: 𝑒++- name: Mnmz+  description: '𝕄(e) ⟿ 𝕄(𝒩(e)) if e ∉ NF'+  match: 𝑒+  when:+    not:+      nf: 𝑒+  then:+    morph:+      normalize: 𝑒++- name: Mlambda+  description: '𝕄(⟦𝐵1, λ ⤍ F, 𝐵2⟧ * t) ⟿ 𝕄(F(⟦𝐵1, 𝐵2⟧) * t)'+  match: '⟦𝐵1, λ ⤍ !F, 𝐵2⟧ * !t'+  where:+    - meta: 𝑒+      function: lambda+      args:+        - '⟦𝐵1, λ ⤍ !F, 𝐵2⟧'+  then:+    morph: '𝑒 * !t'++- name: Mphi+  description: '𝕄(Φ.τ * t) ⟿ 𝕄(e * t) if Φ ↦ ⟦𝐵1, τ ↦ e, 𝐵2⟧'+  match: 'Φ.𝜏 * !t'+  where:+    - meta: 𝑒+      function: global+      args:+        - 𝜏+  then:+    morph: '𝑒 * !t'++- name: Mstuck+  description: '𝕄(e) ⟿ ⊥ otherwise'+  match: 𝑒+  then: ⊥

@@ -0,0 +1,10 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: alpha+pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏2 ↦ 𝑒)+result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒)+when:+  eq:+    - index: 𝜏2+    - domain: 𝐵1

@@ -0,0 +1,8 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: copy+pattern: ⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑛)+result: ⟦ 𝐵1, 𝜏 ↦ 𝑛, 𝐵2 ⟧+when:+  xi-free: 𝑛

@@ -0,0 +1,6 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: dc+pattern: ⊥(𝜏 ↦ 𝑒)+result: ⊥

@@ -0,0 +1,6 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: dd+pattern: ⊥.𝜏+result: ⊥

@@ -0,0 +1,12 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: dot+pattern: ⟦𝐵1, 𝜏 ↦ 𝑛, 𝐵2⟧.𝜏+result: 𝑒(ρ ↦ ⟦𝐵1, 𝜏 ↦ 𝑛, 𝐵2⟧)+where:+  - meta: 𝑒+    function: contextualize+    args:+      - 𝑛+      - ⟦𝐵1, 𝜏 ↦ 𝑛, 𝐵2⟧

@@ -0,0 +1,14 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: miss+pattern: ⟦𝐵⟧(𝜏 ↦ 𝑒)+result: ⊥+when:+  and:+    - not:+        in:+          - 𝜏+          - 𝐵+    - not:+        alpha: 𝜏

@@ -0,0 +1,6 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: 'null'+pattern: ⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧.𝜏+result: ⊥

@@ -0,0 +1,11 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: over+pattern: ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧(𝜏 ↦ 𝑒2)+result: ⊥+when:+  not:+    eq:+      - 𝜏+      - ρ

@@ -0,0 +1,15 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: phi+pattern: ⟦𝐵⟧.𝜏+result: ⟦𝐵⟧.φ.𝜏+when:+  and:+    - in:+        - φ+        - 𝐵+    - not:+        in:+          - 𝜏+          - 𝐵

@@ -0,0 +1,6 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: stay+pattern: ⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧(ρ ↦ 𝑒2)+result: ⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧

@@ -0,0 +1,20 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: stop+pattern: ⟦𝐵⟧.𝜏+result: ⊥+when:+  and:+    - not:+        in:+          - 𝜏+          - 𝐵+    - not:+        in:+          - φ+          - 𝐵+    - not:+        in:+          - λ+          - 𝐵

@@ -1,6 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----name: 'null'-pattern: ⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧.𝜏-result: ⊥

@@ -1,11 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----name: over-pattern: ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧(𝜏 ↦ 𝑒2)-result: ⊥-when:-  not:-    eq:-      - 𝜏-      - ρ

@@ -1,15 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----name: phi-pattern: ⟦𝐵⟧.𝜏-result: ⟦𝐵⟧.φ.𝜏-when:-  and:-    - in:-        - φ-        - 𝐵-    - not:-        in:-          - 𝜏-          - 𝐵

@@ -1,6 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----name: stay-pattern: ⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧(ρ ↦ 𝑒2)-result: ⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧

@@ -1,20 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----name: stop-pattern: ⟦𝐵⟧.𝜏-result: ⊥-when:-  and:-    - not:-        in:-          - 𝜏-          - 𝐵-    - not:-        in:-          - φ-          - 𝐵-    - not:-        in:-          - λ-          - 𝐵

@@ -1,5 +1,6 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT+{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -9,11 +10,13 @@ import CLI.Types import CLI.Validators (invalidCLIArguments) import Control.Exception+import Control.Monad ((>=>)) import Data.Functor ((<&>)) import Data.List (intercalate) import Data.Maybe import Deps (SaveStepFunc, saveStep) import Encoding+import Functions (execFunctions) import LaTeX (LatexContext (..), defaultMeetLength, defaultMeetPopularity, expressionToLaTeX, programToLaTeX, rewrittensToLatex) import Locator (locatedExpression) import Logger@@ -99,12 +102,24 @@           else do             logDebug (printf "Using rules from files: [%s]" (intercalate ", " rules))             yamls <- mapM M.ensuredFile rules-            mapM Y.yamlRule yamls+            mapM (Y.yamlRule >=> validateRewriteRule) yamls   if shuffle     then do       logDebug "The --shuffle option is provided, rules are used in random order"       M.shuffle ordered     else pure ordered++-- Pass a user-supplied rewriting rule through unchanged, or fail fast if it+-- references a build-term function which needs the dataization context: those+-- work only for dataization and morphing, never for plain rewriting.+validateRewriteRule :: Y.Rule -> IO Y.Rule+validateRewriteRule rule =+  let used = maybe [] (map Y.function) rule.where_+   in case filter (`elem` execFunctions) used of+        [] -> pure rule+        (fn : _) ->+          invalidCLIArguments+            (printf "Function '%s' in rule '%s' is available only for dataization and morphing, not for rewriting" fn rule.name)  -- Output content printOut :: Maybe FilePath -> String -> IO ()

@@ -174,6 +174,12 @@ optNormalize :: Parser Bool optNormalize = switch (long "normalize" <> help "Use built-in normalization rules") +optMorph :: Parser Bool+optMorph = switch (long "morph" <> help "Explain built-in morphing rules")++optDataize :: Parser Bool+optDataize = switch (long "dataize" <> help "Explain built-in dataization rules")+ optTarget :: Parser (Maybe FilePath) optTarget = optional (strOption (long "target" <> short 't' <> metavar "FILE" <> help "File to save output to")) @@ -226,6 +232,8 @@             <*> optLogLines             <*> optRule             <*> optNormalize+            <*> optMorph+            <*> optDataize             <*> optShuffle             <*> optTarget         )

@@ -1,3 +1,4 @@+{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -21,7 +22,7 @@ import Encoding import qualified Filter as F import Functions (buildTerm)-import LaTeX (explainRules)+import LaTeX (explainDataizeRules, explainMorphRules, explainRules) import Logger import Margin (defaultMargin) import Merge (merge)@@ -93,7 +94,7 @@     validateBreakpoint :: Maybe String -> [Y.Rule] -> IO ()     validateBreakpoint Nothing _ = pure ()     validateBreakpoint (Just rule) rules =-      let names = map Y.name rules+      let names = map (.name) rules        in unless             (rule `elem` names)             (invalidCLIArguments (printf "The rule '%s' provided in '--breakpoint' option is absent across given rewriting rules: %s" rule (intercalate ", " names)))@@ -182,11 +183,18 @@ runExplain :: OptsExplain -> IO () runExplain OptsExplain{..} = do   validateOpts-  rules <- getRules _normalize _shuffle _rules-  printOut _targetFile (explainRules rules)+  explained >>= printOut _targetFile   where+    explained :: IO String+    explained+      | _morph = pure (explainMorphRules Y.morphingRules)+      | _dataize = pure (explainDataizeRules Y.dataizationRules)+      | otherwise = explainRules <$> getRules _normalize _shuffle _rules     validateOpts :: IO ()-    validateOpts = when (null _rules && not _normalize) (invalidCLIArguments "Either --rule or --normalize must be specified")+    validateOpts = do+      let selected = length (filter id [not (null _rules), _normalize, _morph, _dataize])+      when (selected == 0) (invalidCLIArguments "Either --rule, --normalize, --morph or --dataize must be specified")+      when (selected > 1) (invalidCLIArguments "Only one of --rule, --normalize, --morph or --dataize can be specified")  runMerge :: OptsMerge -> IO () runMerge OptsMerge{..} = do

@@ -106,6 +106,8 @@   , _logLines :: Int   , _rules :: [FilePath]   , _normalize :: Bool+  , _morph :: Bool+  , _dataize :: Bool   , _shuffle :: Bool   , _targetFile :: Maybe FilePath   }

@@ -80,6 +80,8 @@ data META_HEAD   = E -- 𝑒   | E' -- e+  | N -- 𝑛+  | N' -- n   | A -- a   | TAU -- 𝜏   | TAU' -- \tau@@ -222,6 +224,8 @@   | CO_COMPARE {left :: COMPARABLE, equal :: EQUAL, right :: COMPARABLE}   | CO_MATCHES {regex :: String, expr :: EXPRESSION}   | CO_PART_OF {expr :: EXPRESSION, binding :: BINDING}+  | CO_PRIMITIVE {expr :: EXPRESSION, belongs :: BELONGING}+  | CO_DISJOINT {attrs :: [ATTRIBUTE], groups :: [BINDING]}   deriving (Eq, Show)  data EXTRA_ARG@@ -264,6 +268,14 @@ metaTail :: T.Text -> T.Text metaTail = T.drop 1 +-- The first character of an expression meta name encodes its kind:+-- 'n'-prefixed names are normal-form-constrained '𝑛' metas, everything+-- else is an ordinary '𝑒' meta.+exMetaHead :: T.Text -> META_HEAD+exMetaHead mt+  | T.isPrefixOf "n" mt = N+  | otherwise = E+ -- This class is used to convert AST to CST -- CST is created with sugar and unicode -- All further transformations must consider that@@ -276,7 +288,7 @@ instance ToCST Expression EXPRESSION where   toCST ExGlobal _ = EX_GLOBAL Φ   toCST ExThis _ = EX_XI XI-  toCST (ExMeta mt) _ = EX_META (META NO_EXCL E (metaTail mt))+  toCST (ExMeta mt) _ = EX_META (META NO_EXCL (exMetaHead mt) (metaTail mt))   toCST (ExMetaTail expr mt) ctx = EX_META_TAIL (toCST expr ctx) (META EXCL TAIL (metaTail mt))   toCST ExTermination _ = EX_TERMINATION DEAD   toCST (ExPhiMeet prefix idx expr) ctx = EX_PHI_MEET prefix idx (toCST expr ctx)@@ -466,6 +478,9 @@   toCST (Y.Not (Y.In attr binding)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_BINDING (bindingsToCST [binding]))   toCST (Y.Not (Y.Eq left right)) _ = CO_COMPARE (comparableToCST left) NOT_EQUAL (comparableToCST right)   toCST (Y.Not (Y.Alpha attr)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_ATTRIBUTES [attributeToCST (AtAlpha 0), attributeToCST (AtAlpha 1), AT_REST DOTS])+  toCST (Y.Not (Y.Primitive expr)) _ = CO_PRIMITIVE (expressionToCST expr) NOT_IN+  toCST (Y.Primitive expr) _ = CO_PRIMITIVE (expressionToCST expr) IN+  toCST (Y.Disjoint attrs groups) _ = CO_DISJOINT (map attributeToCST attrs) (map (\bd -> bindingsToCST [bd]) groups)   toCST (Y.In attr binding) _ = CO_BELONGS (attributeToCST attr) IN (ST_BINDING (bindingsToCST [binding]))   toCST (Y.And conds) _ = case conds of     [] -> CO_EMPTY

@@ -1,5 +1,6 @@ {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-name-shadowing #-}@@ -8,24 +9,25 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Dataize (morph, dataize, dataize', DataizeContext (..)) where+module Dataize (morph, dataize, dataize', DataizeContext (..), execBuildTerm) where  import AST-import Builder (contextualize)+import Builder (buildAttributeThrows, buildBytesThrows, buildExpressionThrows) import Control.Exception (throwIO) import Data.List (partition) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE import qualified Data.Text as T-import Deps (BuildTermFunc, SaveStepFunc, Term (TeAttribute))+import Deps (BuildTermFunc, BuildTermMethod, SaveStepFunc, Term (TeAttribute, TeExpression)) import Locator (locatedExpression, withLocatedExpression)-import Matcher (substEmpty)+import Matcher (Subst, substEmpty) import Misc import Must (Must (..)) import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite)-import Rule (RuleContext (RuleContext), isNF)+import Rule (RuleContext (RuleContext), matchExpressionWithRule') import Text.Printf (printf)-import Yaml (normalizationRules)+import Yaml (ExtraArgument (..), normalizationRules)+import qualified Yaml as Y  type Dataized = (Maybe Bytes, [Rewritten]) @@ -43,127 +45,96 @@   , _saveStep :: SaveStepFunc   } -switchContext :: DataizeContext -> RewriteContext-switchContext DataizeContext{..} =-  RewriteContext-    _locator-    _maxDepth-    _maxCycles-    _depthSensitive-    _buildTerm-    MtDisabled-    Nothing-    _saveStep--maybeBinding :: (Binding -> Bool) -> [Binding] -> (Maybe Binding, [Binding])-maybeBinding _ [] = (Nothing, [])-maybeBinding func bds =-  let (found, rest) = partition func bds-   in case found of-        [bd] -> (Just bd, rest)-        _ -> (Nothing, bds)--maybeLambda :: [Binding] -> (Maybe Binding, [Binding])-maybeLambda = maybeBinding (\case BiLambda _ -> True; _ -> False)--maybeDelta :: [Binding] -> (Maybe Binding, [Binding])-maybeDelta = maybeBinding (\case BiDelta _ -> True; _ -> False)--maybePhi :: [Binding] -> (Maybe Binding, [Binding])-maybePhi = maybeBinding (\case (BiTau AtPhi _) -> True; _ -> False)- -- Resolve formation for LAMBDA Morphing rule. -- If formation contains λ binding, the called atom -- result is returned.-formation :: [Binding] -> DataizeContext -> IO (Maybe (Expression, String))+formation :: [Binding] -> DataizeContext -> IO (Maybe Expression) formation bds ctx = do   let (lambda, bds') = maybeLambda bds   case lambda of-    Just (BiLambda func) -> do-      obj <- atom func (ExFormation bds') ctx-      pure (Just (obj, "Mlambda"))+    Just (BiLambda func) -> Just <$> atom func (ExFormation bds') ctx     _ -> pure Nothing+  where+    maybeLambda :: [Binding] -> (Maybe Binding, [Binding])+    maybeLambda = maybeBinding (\case BiLambda _ -> True; _ -> False)+    maybeBinding :: (Binding -> Bool) -> [Binding] -> (Maybe Binding, [Binding])+    maybeBinding _ [] = (Nothing, [])+    maybeBinding func bds =+      let (found, rest) = partition func bds+       in case found of+            [bd] -> (Just bd, rest)+            _ -> (Nothing, bds)  -- Resolve dispatch from global object (Q.tau) for PHI Morphing rule. -- Here tau is the name of the attribute which is taken from Q -- and expr is expression which program refers to. -- If Q refers to formation which contains binding with attribute == tau - -- the expression from this binding is returned.-phiDispatch :: T.Text -> Expression -> Maybe (Expression, String)+phiDispatch :: T.Text -> Expression -> Maybe Expression phiDispatch tau expr = case expr of   ExFormation bds -> boundExpr bds   _ -> Nothing   where-    boundExpr :: [Binding] -> Maybe (Expression, String)+    boundExpr :: [Binding] -> Maybe Expression     boundExpr [] = Nothing     boundExpr (bd : bds) = case bd of-      BiTau (AtLabel attr) expr' -> if attr == tau then Just (expr', "Mphi") else boundExpr bds+      BiTau (AtLabel attr) expr' -> if attr == tau then Just expr' else boundExpr bds       _ -> boundExpr bds --- Resolve tail PHI and LAMBDA Morphing rules.--- Tail MUST start with dispatch, that's why most of the applications return Nothing-withTail :: Expression -> DataizeContext -> IO (Maybe (Expression, String))-withTail (ExApplication (ExFormation _) _) _ = pure Nothing-withTail (ExApplication expr tau) ctx = do-  tailed <- withTail expr ctx-  case tailed of-    Just (expr', rule) -> pure (Just (ExApplication expr' tau, rule))-    _ -> pure Nothing-withTail (ExDispatch (ExFormation bds) attr) ctx = do-  tailed <- formation bds ctx-  case tailed of-    Just (obj, rule) -> pure (Just (ExDispatch obj attr, rule))-    _ -> pure Nothing-withTail (ExFormation bds) ctx = formation bds ctx-withTail (ExDispatch ExGlobal (AtLabel label)) DataizeContext{_program = Program expr} = pure (phiDispatch label expr)-withTail (ExDispatch expr attr) ctx = do-  tailed <- withTail expr ctx-  case tailed of-    Just (exp, rule) -> pure (Just (ExDispatch exp attr, rule))-    _ -> pure Nothing-withTail _ _ = pure Nothing---- The Morphing function M:<B,S> -> <P,S> maps objects to--- primitives, possibly modifying the state of evaluation.--- Terminology:--- P(e) - is e Primitive, which is either formation without λ binding or termination ⊥--- N(e) - normalize e--- NF(e) - is e in normal form (can't be normalized anymore)------ PRIM:   M(e) -> e                              if P(e)--- NMZ:    M(e1) -> M(e2)                         if e2 := N(e1) and e1 != e2--- LAMBDA: M([B1, λ -> F, B2] * t) -> M(e2 * t)   if e3 := [B1,B2] and e2 := F(e3)--- PHI:    M(Q.tau * t) -> M(e * t)               if Q -> [B1, tau -> e, B2], t is tail started with dispatch---         M(e) -> ⊥                              otherwise+-- The Morphing function 𝕄 maps objects to primitives. It is driven by the+-- ordered rules from 'morphing.yaml': the first matching rule's 'then' outcome+-- either stops with a primitive ('MoStop') or keeps morphing ('MoMorph'). When+-- the morphed argument is a normalization ('MaNormalize', the 'Mnmz' rule), the+-- rewriter runs and its individual steps are spliced into the chain. morph :: Morphed -> DataizeContext -> IO Morphed-morph (expr@ExTermination, seq) ctx = do-  seq' <- leadsTo seq "Mprim" expr ctx -- PRIM-  pure (expr, seq')-morph (form@(ExFormation _), seq) ctx = do-  resolved <- withTail form ctx-  case resolved of-    Just (expr, rule) -> do-      seq' <- leadsTo seq rule expr ctx -- LAMBDA or PHI-      morph (expr, seq') ctx-    _ -> do-      seq' <- leadsTo seq "Mprim" form ctx -- PRIM-      pure (form, seq') morph (expr, seq) ctx@DataizeContext{..} = do-  resolved <- withTail expr ctx-  case resolved of-    Just (expr', rule) -> do-      seq' <- leadsTo seq rule expr' ctx+  matched <- firstMatch Y.morphingRules+  case matched of+    Just (rule, subst) -> apply rule.then_ rule.name subst+    Nothing -> pure (expr, seq)+  where+    firstMatch :: [Y.MorphRule] -> IO (Maybe (Y.MorphRule, Subst))+    firstMatch [] = pure Nothing+    firstMatch (rule : rest) = do+      substs <- matchExpressionWithRule' expr (asRule rule) (RuleContext (execBuildTerm ctx))+      case substs of+        (subst : _) -> pure (Just (rule, subst))+        [] -> firstMatch rest+    -- The M/D rules evaluate as 'match → where → when', so the rule's guard+    -- maps onto the 'having' slot (which runs after 'where'), not 'when' (which+    -- 'matchExpressionWithRule'' runs before 'where').+    asRule :: Y.MorphRule -> Y.Rule+    asRule rule = Y.Rule rule.name rule.description rule.match ExGlobal Nothing rule.where_ rule.when+    apply :: Y.MorphOutcome -> String -> Subst -> IO Morphed+    apply (Y.MoStop result) name subst = do+      built <- buildExpressionThrows result subst+      seq' <- leadsTo seq name built ctx+      pure (built, seq')+    apply (Y.MoMorph (Y.MaExpr result)) name subst = do+      built <- buildExpressionThrows result subst+      seq' <- leadsTo seq name built ctx+      morph (built, seq') ctx+    -- 𝕄(𝒩(e)) delegates to the normalization rewriter and splices its+    -- individual steps (alpha, copy, dot, …) into the chain before morphing on.+    apply (Y.MoMorph (Y.MaNormalize arg)) _ subst = do+      built <- buildExpressionThrows arg subst+      prog' <- withLocatedExpression _locator built _program+      (rewrittens, _) <- rewrite prog' normalizationRules (switchContext ctx)+      let (rw :| rws) = NE.reverse rewrittens+          seq' = rw :| rws <> NE.tail seq+      expr' <- locatedExpression _locator (fst rw)       morph (expr', seq') ctx-    _ ->-      if isNF expr (RuleContext _buildTerm)-        then morph (ExTermination, seq) ctx -- PRIM-        else do-          prog' <- withLocatedExpression _locator expr _program-          (rewrittens, _) <- rewrite prog' normalizationRules (switchContext ctx) -- NMZ-          let (rw :| rws) = NE.reverse rewrittens-              seq' = rw :| rws <> NE.tail seq-          expr' <- locatedExpression _locator (fst rw)-          morph (expr', seq') ctx+    switchContext :: DataizeContext -> RewriteContext+    switchContext DataizeContext{..} =+      RewriteContext+        _locator+        _maxDepth+        _maxCycles+        _depthSensitive+        _buildTerm+        MtDisabled+        Nothing+        _saveStep  dataize :: DataizeContext -> IO Dataized dataize ctx@DataizeContext{..} = do@@ -171,33 +142,47 @@   (maybeBytes, seq) <- dataize' (expr, (_program, Nothing) :| []) ctx   pure (maybeBytes, reverse seq) --- The goal of 'dataize' function is retrieve bytes from given expression.------ DELTA: D(e) -> data                          if e = [B1, Δ -> data, B2]--- BOX:   D([B1, 𝜑 -> e, B2]) -> D(С(e))        if [B1,B2] has no delta/lambda, where С(e) - contextualization--- NORM:  D(e1) -> D(e2)                        if e2 := M(e1) and e1 is not primitive---        nothing                               otherwise+-- The Dataization function 𝔻 retrieves bytes from an expression. It is driven+-- by the ordered rules from 'dataization.yaml': 'delta' yields the asset bytes,+-- 'none' yields nothing, 'box' contextualizes the φ-body and keeps dataizing+-- (its step is labelled by the operation, 'contextualize'), and 'norm' reduces+-- through morphing, splicing the morphing steps into the chain. dataize' :: Dataizable -> DataizeContext -> IO Dataized-dataize' (ExTermination, seq) _ = pure (Nothing, NE.toList seq)-dataize' (form@(ExFormation bds), seq) ctx@DataizeContext{..} =-  let _seq = NE.toList seq-   in case maybeDelta bds of-        (Just (BiDelta bytes), _) -> pure (Just bytes, _seq)-        (Just _, _) -> pure (Nothing, _seq)-        (Nothing, _) -> case maybePhi bds of-          (Just (BiTau AtPhi expr), bds') -> case maybeLambda bds' of-            (Just (BiLambda _), _) -> throwIO (userError "The 𝜑 and λ can't be present in formation at the same time")-            (Just _, _) -> pure (Nothing, _seq)-            (Nothing, _) -> do-              let expr' = contextualize expr form-              seq' <- leadsTo seq "contextualize" expr' ctx-              dataize' (expr', seq') ctx-          (Just _, _) -> pure (Nothing, _seq)-          (Nothing, _) -> case maybeLambda bds of-            (Just (BiLambda _), _) -> morph (form, seq) ctx >>= (`dataize'` ctx)-            (Just _, _) -> pure (Nothing, _seq)-            (Nothing, _) -> pure (Nothing, _seq)-dataize' dataizable ctx = morph dataizable ctx >>= (`dataize'` ctx)+dataize' (expr, seq) ctx = do+  matched <- firstMatch Y.dataizationRules+  case matched of+    Just (rule, subst) -> apply rule subst+    Nothing -> pure (Nothing, NE.toList seq)+  where+    firstMatch :: [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst))+    firstMatch [] = pure Nothing+    firstMatch (rule : rest) = do+      substs <- matchExpressionWithRule' expr (asRule rule) (RuleContext (execBuildTerm ctx))+      case substs of+        (subst : _) -> pure (Just (rule, subst))+        [] -> firstMatch rest+    asRule :: Y.DataizeRule -> Y.Rule+    asRule rule = Y.Rule rule.name rule.description rule.match ExGlobal Nothing rule.where_ rule.when+    apply :: Y.DataizeRule -> Subst -> IO Dataized+    apply rule subst = case rule.then_ of+      Y.DoData bytes -> do+        bts <- buildBytesThrows bytes subst+        pure (Just bts, NE.toList seq)+      Y.DoNothing -> pure (Nothing, NE.toList seq)+      Y.DoDataize (Y.DaExpr result) -> do+        built <- buildExpressionThrows result subst+        seq' <- leadsTo seq (operation rule) built ctx+        dataize' (built, seq') ctx+      -- 𝔻(𝕄(e)) delegates to the morphing relation, splicing its steps into+      -- the chain before dataizing on.+      Y.DoDataize (Y.DaMorph arg) -> do+        built <- buildExpressionThrows arg subst+        (morphed, seq') <- morph (built, seq) ctx+        dataize' (morphed, seq') ctx+    operation :: Y.DataizeRule -> String+    operation rule = case rule.where_ of+      Just (extra : _) -> Y.function extra+      _ -> ""  leadsTo :: NonEmpty Rewritten -> String -> Expression -> DataizeContext -> IO (NonEmpty Rewritten) leadsTo ((prog, _) :| rest) rule expr DataizeContext{..} = do@@ -248,3 +233,34 @@         else pure (ExDispatch self (AtLabel "y"))     _ -> pure ExTermination atom func _ _ = throwIO (userError (printf "Atom '%s' does not exist" (T.unpack func)))++-- Augment the injected, context-free term builder with the dataization and+-- morphing operations that need the full evaluation context: 'lambda' applies+-- an atom and 'global' dispatches from the universe Q. Every other function is+-- delegated unchanged.+execBuildTerm :: DataizeContext -> BuildTermFunc+execBuildTerm ctx "lambda" = _lambda ctx+execBuildTerm ctx "global" = _global ctx+execBuildTerm ctx func = _buildTerm ctx func++_lambda :: DataizeContext -> BuildTermMethod+_lambda ctx [ArgExpression expr] subst = do+  form <- buildExpressionThrows expr subst+  case form of+    ExFormation bds -> do+      resolved <- formation bds ctx+      case resolved of+        Just obj -> pure (TeExpression obj)+        Nothing -> throwIO (userError "Function lambda() expects a formation with a λ binding")+    _ -> throwIO (userError "Function lambda() expects a formation")+_lambda _ _ _ = throwIO (userError "Function lambda() requires exactly 1 expression argument")++_global :: DataizeContext -> BuildTermMethod+_global DataizeContext{_program = Program prog} [ArgAttribute attr] subst = do+  attr' <- buildAttributeThrows attr subst+  case attr' of+    AtLabel label -> case phiDispatch label prog of+      Just expr -> pure (TeExpression expr)+      Nothing -> throwIO (userError (printf "Universe Q has no attribute '%s'" (show attr')))+    _ -> throwIO (userError "Function global() expects a labelled attribute")+_global _ _ _ = throwIO (userError "Function global() requires exactly 1 attribute argument")

@@ -31,6 +31,7 @@   toASCII EX_APPLICATION{..} = EX_APPLICATION (toASCII expr) space eol tab (toASCII tau) eol' tab' indent   toASCII EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toASCII expr) space eol tab (toASCII taus) eol' tab' indent   toASCII EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toASCII expr) space eol tab (toASCII args) eol' tab' indent+  toASCII EX_META{meta = META{hd = N, ..}} = EX_META (META EXCL N' rest)   toASCII EX_META{..} = EX_META (META EXCL E' (rest meta))   toASCII EX_META_TAIL{..} = EX_META_TAIL (toASCII expr) meta   toASCII EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toASCII expr)@@ -98,6 +99,8 @@   toASCII CO_COMPARE{..} = CO_COMPARE (toASCII left) equal (toASCII right)   toASCII CO_MATCHES{..} = CO_MATCHES regex (toASCII expr)   toASCII CO_PART_OF{..} = CO_PART_OF (toASCII expr) (toASCII binding)+  toASCII CO_PRIMITIVE{..} = CO_PRIMITIVE (toASCII expr) belongs+  toASCII CO_DISJOINT{..} = CO_DISJOINT (map toASCII attrs) (map toASCII groups)   toASCII CO_EMPTY = CO_EMPTY  instance ToASCII EXTRA_ARG where

@@ -3,7 +3,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Functions (buildTerm) where+module Functions (buildTerm, execFunctions) where  import AST import Builder@@ -23,6 +23,13 @@ import Tau (freshTau) import Text.Printf (printf) import qualified Yaml as Y++-- Names of build-term functions that need the full evaluation context+-- (program plus atom evaluation) and are therefore provided only by+-- 'Dataize.execBuildTerm', not by 'buildTerm'. They are available while+-- executing dataization and morphing rules, but not rewriting rules.+execFunctions :: [String]+execFunctions = ["lambda", "global"]  buildTerm :: BuildTermFunc buildTerm func args subst = do

@@ -1,6 +1,7 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} @@ -9,6 +10,8 @@  module LaTeX   ( explainRules+  , explainMorphRules+  , explainDataizeRules   , rewrittensToLatex   , programToLaTeX   , expressionToLaTeX@@ -217,6 +220,7 @@   toLaTeX EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toLaTeX expr)   toLaTeX EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toLaTeX expr)   toLaTeX EX_META{..} = EX_META (toLaTeX meta)+  toLaTeX EX_META_TAIL{..} = EX_META_TAIL (toLaTeX expr) (toLaTeX meta)   toLaTeX expr = expr  instance ToLaTeX ATTRIBUTE where@@ -260,6 +264,7 @@  instance ToLaTeX META_HEAD where   toLaTeX E = E'+  toLaTeX N = N'   toLaTeX A = TAU'   toLaTeX TAU = TAU'   toLaTeX B = B'@@ -306,6 +311,8 @@   toLaTeX CO_COMPARE{..} = CO_COMPARE (toLaTeX left) equal (toLaTeX right)   toLaTeX CO_MATCHES{..} = CO_MATCHES regex (toLaTeX expr)   toLaTeX CO_PART_OF{..} = CO_PART_OF (toLaTeX expr) (toLaTeX binding)+  toLaTeX CO_PRIMITIVE{..} = CO_PRIMITIVE (toLaTeX expr) belongs+  toLaTeX CO_DISJOINT{..} = CO_DISJOINT (map toLaTeX attrs) (map toLaTeX groups)   toLaTeX CO_EMPTY = CO_EMPTY  instance ToLaTeX EXTRA_ARG where@@ -319,27 +326,13 @@  explainRule :: Y.Rule -> String explainRule rule =-  intercalate-    "\n  "-    [ "\\trrule{" ++ Y.name rule ++ "}"-    , braced (renderToLatex (expressionToCST (Y.pattern rule)) defaultLatexContext)-    , braced (renderToLatex (expressionToCST (Y.result rule)) defaultLatexContext)-    , conditionToLatex (joinedConditions (Y.when rule) (Y.having rule))-    , extraArgumentsToLatex (Y.where_ rule)-    ]+  trrule+    rule.name+    (renderToLatex (expressionToCST rule.pattern) defaultLatexContext)+    (renderToLatex (expressionToCST rule.result) defaultLatexContext)+    (joinedConditions rule.when rule.having)+    rule.where_   where-    conditionToLatex :: Maybe Y.Condition -> String-    conditionToLatex Nothing = "{ }"-    conditionToLatex (Just cond) = case conditionToCST cond of-      CO_EMPTY -> "{ }"-      cond' -> braced ("if $ " <> renderToLatex cond' defaultLatexContext <> " $")-    extraArgumentsToLatex :: Maybe [Y.Extra] -> String-    extraArgumentsToLatex Nothing = "{ }"-    extraArgumentsToLatex (Just extras) =-      let extras' = map ((`renderToLatex` defaultLatexContext) . extraToCST) extras-       in braced ("where " <> intercalate " and " extras')-    braced :: String -> String-    braced = printf "{ %s }"     -- Join two maybe conditions into single one using Y.And if at least one is just.     joinedConditions :: Maybe Y.Condition -> Maybe Y.Condition -> Maybe Y.Condition     joinedConditions Nothing Nothing = Nothing@@ -347,11 +340,86 @@     joinedConditions Nothing second@(Just _) = second     joinedConditions (Just first) (Just second) = Just (Y.And [first, second]) +explainMorphRule :: Y.MorphRule -> String+explainMorphRule rule =+  trrule+    rule.name+    (morph (renderToLatex (expressionToCST rule.match) defaultLatexContext))+    (morphOutcome rule.then_)+    rule.when+    rule.where_+  where+    morphOutcome :: Y.MorphOutcome -> String+    morphOutcome (Y.MoMorph (Y.MaExpr expr)) = morph (renderToLatex (expressionToCST expr) defaultLatexContext)+    morphOutcome (Y.MoMorph (Y.MaNormalize expr)) = morph (normalize (renderToLatex (expressionToCST expr) defaultLatexContext))+    morphOutcome (Y.MoStop expr) = renderToLatex (expressionToCST expr) defaultLatexContext++explainDataizeRule :: Y.DataizeRule -> String+explainDataizeRule rule =+  trrule+    rule.name+    (dataize (renderToLatex (expressionToCST rule.match) defaultLatexContext))+    (dataizeOutcome rule.then_)+    rule.when+    rule.where_+  where+    dataizeOutcome :: Y.DataizeOutcome -> String+    dataizeOutcome (Y.DoDataize (Y.DaExpr expr)) = dataize (renderToLatex (expressionToCST expr) defaultLatexContext)+    dataizeOutcome (Y.DoDataize (Y.DaMorph expr)) = dataize (morph (renderToLatex (expressionToCST expr) defaultLatexContext))+    dataizeOutcome (Y.DoData bytes) = T.unpack (render (toCST' bytes :: BYTES))+    dataizeOutcome Y.DoNothing = "\\varnothing"++-- Render a single rule row through the shared \trrule macro: name, left-hand+-- side, right-hand side, the optional 'if' condition and 'where' extras.+trrule :: String -> String -> String -> Maybe Y.Condition -> Maybe [Y.Extra] -> String+trrule name lhs rhs cond extras =+  intercalate+    "\n  "+    [ "\\trrule{" ++ name ++ "}"+    , braced lhs+    , braced rhs+    , conditionToLatex cond+    , extraArgumentsToLatex extras+    ]++morph :: String -> String+morph inner = "\\mathbb{M}( " ++ inner ++ " )"++dataize :: String -> String+dataize inner = "\\mathbb{D}( " ++ inner ++ " )"++normalize :: String -> String+normalize inner = "\\mathcal{N}( " ++ inner ++ " )"++braced :: String -> String+braced = printf "{ %s }"++conditionToLatex :: Maybe Y.Condition -> String+conditionToLatex Nothing = "{ }"+conditionToLatex (Just cond) = case conditionToCST cond of+  CO_EMPTY -> "{ }"+  cond' -> braced ("if $ " <> renderToLatex cond' defaultLatexContext <> " $")++extraArgumentsToLatex :: Maybe [Y.Extra] -> String+extraArgumentsToLatex Nothing = "{ }"+extraArgumentsToLatex (Just extras) =+  let extras' = map ((`renderToLatex` defaultLatexContext) . extraToCST) extras+   in braced ("where " <> intercalate " and " extras')+ explainRules :: [Y.Rule] -> String-explainRules rules =+explainRules = explainTabular . map explainRule++explainMorphRules :: [Y.MorphRule] -> String+explainMorphRules = explainTabular . map explainMorphRule++explainDataizeRules :: [Y.DataizeRule] -> String+explainDataizeRules = explainTabular . map explainDataizeRule++explainTabular :: [String] -> String+explainTabular rows =   intercalate     "\n"     [ "\\begin{tabular}{rl}"-    , intercalate "\n" (map explainRule rules)+    , intercalate "\n" rows     , "\\end{tabular}"     ]

@@ -31,6 +31,7 @@   toSingleLine EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toSingleLine expr) space NO_EOL TAB' (toSingleLine args) NO_EOL TAB' indent   toSingleLine EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSingleLine expr)   toSingleLine EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toSingleLine expr)+  toSingleLine EX_META_TAIL{..} = EX_META_TAIL (toSingleLine expr) meta   toSingleLine expr = expr  instance ToSingleLine APP_BINDING where@@ -81,6 +82,8 @@   toSingleLine CO_COMPARE{..} = CO_COMPARE (toSingleLine left) equal (toSingleLine right)   toSingleLine CO_MATCHES{..} = CO_MATCHES regex (toSingleLine expr)   toSingleLine CO_PART_OF{..} = CO_PART_OF (toSingleLine expr) (toSingleLine binding)+  toSingleLine CO_PRIMITIVE{..} = CO_PRIMITIVE (toSingleLine expr) belongs+  toSingleLine CO_DISJOINT{..} = CO_DISJOINT attrs (map toSingleLine groups)   toSingleLine CO_EMPTY = CO_EMPTY  instance ToSingleLine EXTRA_ARG where

@@ -1,5 +1,3 @@-{-# LANGUAGE LambdaCase #-}- -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT @@ -36,6 +34,10 @@ newtype Subst = Subst (Map Text MetaValue)   deriving (Eq, Show) +-- A way to match a pattern expression against a target expression, yielding+-- the substitutions under which they agree.+type MatchExpressionFunc = Expression -> Expression -> [Subst]+ -- Empty substitution substEmpty :: Subst substEmpty = Subst Map.empty@@ -109,19 +111,12 @@           (substs, tails) <- tailExpressionsReversed ptn' expr           Just (substs, TaDispatch attr : tails)         ExApplication expr tau -> do-          (substs, tails@(t : _)) <- tailExpressionsReversed ptn' expr-          if not (null tails) && isDispatch t-            then Just (substs, TaApplication tau : tails)-            else Nothing-          where-            isDispatch :: Tail -> Bool-            isDispatch = \case-              TaDispatch _ -> True-              TaApplication _ -> False+          (substs, tails) <- tailExpressionsReversed ptn' expr+          Just (substs, TaApplication tau : tails)         _ -> Just ([], [])       substs -> Just (substs, []) -matchExpression' :: Expression -> Expression -> [Subst]+matchExpression' :: MatchExpressionFunc matchExpression' (ExMeta meta) tgt = [substSingle meta (MvExpression tgt)] matchExpression' ExThis ExThis = [substEmpty] matchExpression' ExGlobal ExGlobal = [substEmpty]@@ -146,7 +141,7 @@ matchBindingExpression _ _ = []  -- Match expression with deep nested expression(s) matching-matchExpressionDeep :: Expression -> Expression -> [Subst]+matchExpressionDeep :: MatchExpressionFunc matchExpressionDeep ptn tgt =   let matched = matchExpression' ptn tgt       deep = case tgt of@@ -156,7 +151,7 @@         _ -> []    in matched ++ deep -matchExpression :: Expression -> Expression -> [Subst]+matchExpression :: MatchExpressionFunc matchExpression = matchExpressionDeep  matchProgram :: Expression -> Program -> [Subst]

@@ -385,6 +385,7 @@     , number     , lexeme (DataString . strToBts <$> quotedStr)     , try (ExMeta <$> meta' 'e' "𝑒")+    , try (ExMeta <$> meta' 'n' "𝑛")     , ExDispatch ExThis <$> attribute     ]     <?> "expression head"

@@ -112,6 +112,8 @@ instance Render META_HEAD where   render E = "𝑒"   render E' = "e"+  render N = "𝑛"+  render N' = "n"   render A = "a"   render TAU = "𝜏"   render TAU' = "\\tau"@@ -250,6 +252,13 @@   render CO_COMPARE{..} = render left <> " " <> render equal <> " " <> render right   render CO_MATCHES{..} = "matches( " <> T.pack regex <> ", " <> render expr <> " )"   render CO_PART_OF{..} = "part-of( " <> render expr <> ", " <> render binding <> " )"+  render CO_PRIMITIVE{..} = render expr <> " " <> render belongs <> " \\mathcal{P}"+  render CO_DISJOINT{..} =+    "[ "+      <> T.intercalate ", " (map render attrs)+      <> " ] \\cap ( "+      <> T.intercalate " \\cup " (map render groups)+      <> " ) = \\emptyset"   render CO_EMPTY = ""  renderFunc :: Render a => Text -> a -> Text

@@ -2,6 +2,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} @@ -145,9 +146,9 @@   where     _rewrite :: RewriteState -> Int -> IO RewriteState     _rewrite (_rewrittens@((program, _) :| _), _unique, _) _count =-      let ruleName = Y.name rule-          ptn = Y.pattern rule-          res = Y.result rule+      let ruleName = rule.name+          ptn = rule.pattern+          res = rule.result        in if _count - 1 == _maxDepth             then do               logDebug (printf "Max amount of rewriting cycles (%d) for rule '%s' has been reached, rewriting is stopped" _maxDepth ruleName)@@ -191,7 +192,7 @@         leadsTo :: Program -> NonEmpty Rewritten         leadsTo _prog =           let (program, _) :| rest = _rewrittens-           in (_prog, Nothing) :| (program, Just (Y.name rule)) : rest+           in (_prog, Nothing) :| (program, Just rule.name) : rest  -- Rewrite program by provided locator from RewriteContext rewrite :: Program -> [Y.Rule] -> RewriteContext -> IO Rewrittens

@@ -1,3 +1,4 @@+{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-name-shadowing #-}@@ -5,7 +6,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Rule (RuleContext (..), isNF, matchProgramWithRule, matchExpressionWithRule, meetCondition) where+module Rule (RuleContext (..), isNF, matchProgramWithRule, matchExpressionWithRule, matchExpressionWithRule', meetCondition) where  import AST import Builder@@ -18,8 +19,10 @@ import Control.Monad (when) import qualified Data.ByteString.Char8 as B import Data.Foldable (foldlM)+import Data.List (nub) import qualified Data.Map.Strict as M import Data.Maybe (catMaybes)+import qualified Data.Text as T import Deps (BuildTermFunc, Term (..)) import GHC.IO (unsafePerformIO) import Logger (logDebug)@@ -207,6 +210,43 @@     partOf expr (BiTau _ expr' : rest) = expr == expr' || partOf expr rest     partOf expr (_ : rest) = partOf expr rest +-- A primitive is the termination ⊥ or a formation without a λ binding;+-- expression metas are resolved through the substitution first.+_primitive :: Expression -> Subst -> RuleContext -> IO [Subst]+_primitive (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of+  Just (MvExpression expr) -> _primitive expr (Subst mp) ctx+  _ -> pure []+_primitive expr subst _ = pure [subst | primitive expr]+  where+    primitive :: Expression -> Bool+    primitive ExTermination = True+    primitive (ExFormation bds) = not (any lambda bds)+    primitive _ = False+    lambda :: Binding -> Bool+    lambda (BiLambda _) = True+    lambda (BiMetaLambda _) = True+    lambda _ = False++-- Hold if none of the given attributes is present in the union of the+-- bindings captured by the given binding metas.+_disjoint :: [Attribute] -> [Binding] -> Subst -> RuleContext -> IO [Subst]+_disjoint attrs bindings subst _ =+  case (traverse (`buildAttribute` subst) attrs, traverse (`buildBinding` subst) bindings) of+    (Right attrs', Right bdss) ->+      let bds = concat bdss+       in pure [subst | not (any (`presentIn` bds) attrs')]+    (_, _) -> pure []+  where+    presentIn :: Attribute -> [Binding] -> Bool+    presentIn attr = any (presentInBinding attr)+    presentInBinding :: Attribute -> Binding -> Bool+    presentInBinding attr (BiTau battr _) = attr == battr+    presentInBinding attr (BiVoid battr) = attr == battr+    presentInBinding AtLambda (BiLambda _) = True+    presentInBinding AtLambda (BiMetaLambda _) = True+    presentInBinding AtDelta (BiDelta _) = True+    presentInBinding _ _ = False+ meetCondition' :: Y.Condition -> Subst -> RuleContext -> IO [Subst] meetCondition' (Y.Or conds) = _or conds meetCondition' (Y.And conds) = _and conds@@ -218,6 +258,8 @@ meetCondition' (Y.XiFree expr) = _xiFree expr meetCondition' (Y.Matches pat expr) = _matches pat expr meetCondition' (Y.PartOf expr bd) = _partOf expr bd+meetCondition' (Y.Primitive expr) = _primitive expr+meetCondition' (Y.Disjoint attrs bds) = _disjoint attrs bds  -- For each substitution check if it meetCondition to given condition -- If substitution does not meet the condition - it's thrown out@@ -283,32 +325,69 @@     logDebug "Extra substitutions have been built"     pure (catMaybes res) +-- Collect the names of NF-constrained expression meta-variables ('𝑛'/'!n')+-- used in a pattern. Their names are 'n'-prefixed and live in their own+-- key-space, so a pattern may freely mix plain '𝑒' captures with '𝑛' ones.+nfMetaNames :: Expression -> [T.Text]+nfMetaNames = nub . go+  where+    go :: Expression -> [T.Text]+    go (ExMeta mt)+      | T.isPrefixOf "n" mt = [mt]+      | otherwise = []+    go (ExFormation bds) = concatMap goBinding bds+    go (ExApplication e bd) = go e ++ goBinding bd+    go (ExDispatch e _) = go e+    go (ExMetaTail e _) = go e+    go (ExPhiMeet _ _ e) = go e+    go (ExPhiAgain _ _ e) = go e+    go _ = []+    goBinding :: Binding -> [T.Text]+    goBinding (BiTau _ e) = go e+    goBinding _ = []+ matchExpressionWithRule :: Expression -> Y.Rule -> RuleContext -> IO [Subst]-matchExpressionWithRule expr rule ctx =-  let ptn = Y.pattern rule-      matched = matchExpression ptn expr-      name = Y.name rule+matchExpressionWithRule = matchExpressionBy matchExpression++-- Like 'matchExpressionWithRule' but matches the pattern against the whole+-- expression only (no deep, sub-expression matching). Used by the dataization+-- and morphing driver, where a rule applies to the entire configuration rather+-- than to nested redexes.+matchExpressionWithRule' :: Expression -> Y.Rule -> RuleContext -> IO [Subst]+matchExpressionWithRule' = matchExpressionBy matchExpression'++matchExpressionBy :: MatchExpressionFunc -> Expression -> Y.Rule -> RuleContext -> IO [Subst]+matchExpressionBy matcher expr rule ctx =+  let ptn = rule.pattern+      matched = matcher ptn expr+      name = rule.name    in if null matched         then do           logDebug (printf "Pattern from rule '%s' was not matched:\n%s" name (printExpression' ptn logPrintConfig))           pure []         else do-          when' <- meetMaybeCondition (Y.when rule) matched ctx-          if null when'+          inNf <- foldlM (\substs nm -> meetCondition (Y.NF (ExMeta nm)) substs ctx) matched (nfMetaNames ptn)+          if null inNf             then do-              logDebug "The 'when' condition wasn't met"+              logDebug "An NF-constrained '𝑛' meta-variable is not in normal form"               pure []             else do-              logDebug (printf "Rule %s" name)-              extended <- extraSubstitutions when' (Y.where_ rule) ctx-              if null extended+              when' <- meetMaybeCondition rule.when inNf ctx+              if null when'                 then do-                  logDebug "Substitution is empty after enxtending, maybe some metas are duplicated"+                  logDebug "The 'when' condition wasn't met"                   pure []                 else do-                  met <- meetMaybeCondition (Y.having rule) extended ctx-                  when (null met) (logDebug "The 'having' condition wan't met")-                  pure met+                  logDebug (printf "Rule %s" name)+                  extended <- extraSubstitutions when' rule.where_ ctx+                  if null extended+                    then do+                      logDebug "Substitution is empty after extending, maybe some metas are duplicated"+                      pure []+                    else do+                      met <- meetMaybeCondition rule.having extended ctx+                      when (null met) (logDebug "The 'having' condition wasn't met")+                      pure met  matchProgramWithRule :: Program -> Y.Rule -> RuleContext -> IO [Subst] matchProgramWithRule (Program expr) = matchExpressionWithRule expr

@@ -110,6 +110,7 @@       rhos   toSalty EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSalty expr)   toSalty EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toSalty expr)+  toSalty EX_META_TAIL{..} = EX_META_TAIL (toSalty expr) meta   toSalty expr = expr  saltifyPrimitive :: EXPRESSION -> EXPRESSION -> EXPRESSION -> TAB -> [Binding] -> EXPRESSION@@ -195,6 +196,8 @@   toSalty CO_COMPARE{..} = CO_COMPARE (toSalty left) equal (toSalty right)   toSalty CO_MATCHES{..} = CO_MATCHES regex (toSalty expr)   toSalty CO_PART_OF{..} = CO_PART_OF (toSalty expr) (toSalty binding)+  toSalty CO_PRIMITIVE{..} = CO_PRIMITIVE (toSalty expr) belongs+  toSalty CO_DISJOINT{..} = CO_DISJOINT attrs (map toSalty groups)   toSalty CO_EMPTY = CO_EMPTY  instance ToSalty EXTRA_ARG where

@@ -1,4 +1,5 @@ {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TemplateHaskell #-}@@ -13,7 +14,7 @@ import Control.Applicative (asum) import Data.Aeson import qualified Data.ByteString as BS-import Data.FileEmbed (embedDir)+import Data.FileEmbed (embedDir, embedFile) import Data.Text (unpack) import Data.Yaml (Parser) import qualified Data.Yaml as Yaml@@ -77,7 +78,7 @@     withObject       "Condition"       ( \v -> do-          validateYamlObject v ["and", "or", "not", "alpha", "nf", "xi-free", "eq", "in", "matches", "part-of"]+          validateYamlObject v ["and", "or", "not", "alpha", "nf", "xi-free", "eq", "in", "matches", "part-of", "primitive", "disjoint"]           asum             [ And <$> v .: "and"             , Or <$> v .: "or"@@ -85,7 +86,13 @@             , Alpha <$> v .: "alpha"             , NF <$> v .: "nf"             , XiFree <$> v .: "xi-free"+            , Primitive <$> v .: "primitive"             , do+                vals <- v .: "disjoint"+                case vals of+                  [attrs_, bds_] -> Disjoint <$> parseJSON attrs_ <*> parseJSON bds_+                  _ -> fail "'disjoint' expects exactly two arguments"+            , do                 vals <- v .: "eq"                 case vals of                   [left_, right_] -> Eq <$> parseJSON left_ <*> parseJSON right_@@ -164,6 +171,8 @@   | XiFree Expression   | Matches String Expression   | PartOf Expression Binding+  | Primitive Expression+  | Disjoint [Attribute] [Binding]   deriving (Eq, Generic, Show)  data ExtraArgument@@ -193,7 +202,7 @@  normalizationRules :: [Rule] {-# NOINLINE normalizationRules #-}-normalizationRules = map decodeRule $(embedDir "resources")+normalizationRules = map decodeRule $(embedDir "resources/normalize")   where     decodeRule :: (FilePath, BS.ByteString) -> Rule     decodeRule (path, bs) =@@ -203,3 +212,124 @@  yamlRule :: FilePath -> IO Rule yamlRule = Yaml.decodeFileThrow++-- The right-hand side of a morphing reduction 𝕄(match) ⟿ then.+-- A mapping ('{ morph: arg }') keeps reducing under 𝕄; a bare expression+-- (including ⊥) is the terminal primitive result.+data MorphOutcome+  = MoMorph MorphArg+  | MoStop Expression+  deriving (Eq, Generic, Show)++-- The argument of a morphing continuation: either a plain expression ('𝕄(e)')+-- or the normalization of one ('𝕄(𝒩(e))', written '{ normalize: e }').+data MorphArg+  = MaExpr Expression+  | MaNormalize Expression+  deriving (Eq, Generic, Show)++-- The right-hand side of a dataization reduction 𝔻(match) ⟿ then.+-- A mapping ('{ dataize: arg }') keeps reducing under 𝔻; a bare bytes scalar+-- yields data; the 'nothing' keyword marks the function as undefined.+data DataizeOutcome+  = DoDataize DataizeArg+  | DoData Bytes+  | DoNothing+  deriving (Eq, Generic, Show)++-- The argument of a dataization continuation: either a plain expression+-- ('𝔻(e)') or the morphing of one ('𝔻(𝕄(e))', written '{ morph: e }').+data DataizeArg+  = DaExpr Expression+  | DaMorph Expression+  deriving (Eq, Generic, Show)++-- One ordered morphing rule: match the expression, build extra metas in+-- 'where', filter by 'when', then reduce per 'then'.+data MorphRule = MorphRule+  { name :: String+  , description :: Maybe String+  , match :: Expression+  , where_ :: Maybe [Extra]+  , when :: Maybe Condition+  , then_ :: MorphOutcome+  }+  deriving (Generic, Show)++-- One ordered dataization rule, structured like 'MorphRule' but reducing+-- under 𝔻 and able to terminate with bytes or 'nothing'.+data DataizeRule = DataizeRule+  { name :: String+  , description :: Maybe String+  , match :: Expression+  , where_ :: Maybe [Extra]+  , when :: Maybe Condition+  , then_ :: DataizeOutcome+  }+  deriving (Generic, Show)++instance FromJSON MorphOutcome where+  parseJSON (Object o) = do+    validateYamlObject o ["morph"]+    MoMorph <$> o .: "morph"+  parseJSON v = MoStop <$> parseJSON v++instance FromJSON MorphArg where+  parseJSON (Object o) = do+    validateYamlObject o ["normalize"]+    MaNormalize <$> o .: "normalize"+  parseJSON v = MaExpr <$> parseJSON v++instance FromJSON DataizeOutcome where+  parseJSON (Object o) = do+    validateYamlObject o ["dataize"]+    DoDataize <$> o .: "dataize"+  parseJSON (String "nothing") = pure DoNothing+  parseJSON v = DoData <$> parseJSON v++instance FromJSON DataizeArg where+  parseJSON (Object o) = do+    validateYamlObject o ["morph"]+    DaMorph <$> o .: "morph"+  parseJSON v = DaExpr <$> parseJSON v++instance FromJSON MorphRule where+  parseJSON =+    withObject+      "MorphRule"+      ( \o ->+          MorphRule+            <$> o .: "name"+            <*> o .:? "description"+            <*> o .: "match"+            <*> o .:? "where"+            <*> o .:? "when"+            <*> o .: "then"+      )++instance FromJSON DataizeRule where+  parseJSON =+    withObject+      "DataizeRule"+      ( \o ->+          DataizeRule+            <$> o .: "name"+            <*> o .:? "description"+            <*> o .: "match"+            <*> o .:? "where"+            <*> o .:? "when"+            <*> o .: "then"+      )++decodeRules :: (FromJSON a) => FilePath -> BS.ByteString -> [a]+decodeRules path bs = case Yaml.decodeEither' bs of+  Right rs -> rs+  Left err -> error $ "YAML parse error in " ++ path ++ ": " ++ show err++morphingRules :: [MorphRule]+{-# NOINLINE morphingRules #-}+morphingRules = decodeRules "resources/morphing.yaml" $(embedFile "resources/morphing.yaml")++dataizationRules :: [DataizeRule]+{-# NOINLINE dataizationRules #-}+dataizationRules = decodeRules "resources/dataization.yaml" $(embedFile "resources/dataization.yaml")

@@ -359,8 +359,14 @@      it "rewrites with single rule" $       withStdin "{T(x -> Q.y)}" $-        testCLISucceeded ["rewrite", "--rule=resources/dc.yaml"] ["Φ ↦ ⊥"]+        testCLISucceeded ["rewrite", "--rule=resources/normalize/dc.yaml"] ["Φ ↦ ⊥"] +    it "fails when a rewriting rule uses a dataization-only function" $+      withStdin "{⟦⟧}" $+        testCLIFailed+          ["rewrite", rule "lambda-in-rewrite.yaml"]+          ["Function 'lambda' in rule 'uses-lambda' is available only for dataization and morphing, not for rewriting"]+     it "normalizes with --normalize flag" $       testCLISucceeded         ["rewrite", "--normalize", resource "normalize.phi", "--margin=25"]@@ -917,13 +923,13 @@   describe "explain" $ do     it "explains single rule" $       testCLISucceeded-        ["explain", "--rule=resources/copy.yaml"]+        ["explain", "--rule=resources/normalize/copy.yaml"]         [ unlines             [ "\\begin{tabular}{rl}"             , "\\trrule{copy}"-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }"-            , "  { [[ B_1, \\tau -> e, B_2 ]] }"-            , "  { if $ \\xifree{ e } \\;\\text{and}\\; \\isnormal{ e } $ }"+            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> n ) }"+            , "  { [[ B_1, \\tau -> n, B_2 ]] }"+            , "  { if $ \\xifree{ n } $ }"             , "  { }"             , "\\end{tabular}"             ]@@ -931,7 +937,7 @@      it "explains multiple rules" $       testCLISucceeded-        ["explain", "--rule=resources/copy.yaml", "--rule=resources/alpha.yaml"]+        ["explain", "--rule=resources/normalize/copy.yaml", "--rule=resources/normalize/alpha.yaml"]         ["\\begin{tabular}{rl}", "\\trrule{copy}", "\\trrule{alpha}"]      it "explains normalization rules" $@@ -945,9 +951,9 @@             , "  { if $ \\indexof{ \\tau_2 } = \\vert \\overline{ B_1 } \\vert $ }"             , "  { }"             , "\\trrule{copy}"-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }"-            , "  { [[ B_1, \\tau -> e, B_2 ]] }"-            , "  { if $ \\xifree{ e } \\;\\text{and}\\; \\isnormal{ e } $ }"+            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> n ) }"+            , "  { [[ B_1, \\tau -> n, B_2 ]] }"+            , "  { if $ \\xifree{ n } $ }"             , "  { }"             , "\\trrule{dc}"             , "  { T ( \\tau -> e ) }"@@ -960,10 +966,10 @@             , "  { }"             , "  { }"             , "\\trrule{dot}"-            , "  { [[ B_1, \\tau -> e_1, B_2 ]] . \\tau }"-            , "  { e_2 ( ^ -> [[ B_1, \\tau -> e_1, B_2 ]] ) }"-            , "  { if $ \\isnormal{ e_1 } $ }"-            , "  { where $ e_2 \\coloneqq \\ctx{ e_1 }{ [[ B_1, \\tau -> e_1, B_2 ]] } $ }"+            , "  { [[ B_1, \\tau -> n, B_2 ]] . \\tau }"+            , "  { e ( ^ -> [[ B_1, \\tau -> n, B_2 ]] ) }"+            , "  { }"+            , "  { where $ e \\coloneqq \\ctx{ n }{ [[ B_1, \\tau -> n, B_2 ]] } $ }"             , "\\trrule{miss}"             , "  { [[ B ]] ( \\tau -> e ) }"             , "  { T }"@@ -998,10 +1004,78 @@             ]         ] +    it "explains morphing rules" $+      testCLISucceeded+        ["explain", "--morph"]+        [ unlines+            [ "\\begin{tabular}{rl}"+            , "\\trrule{Mprim}"+            , "  { \\mathbb{M}( e ) }"+            , "  { e }"+            , "  { if $ e \\in \\mathcal{P} $ }"+            , "  { }"+            , "\\trrule{Mnmz}"+            , "  { \\mathbb{M}( e ) }"+            , "  { \\mathbb{M}( \\mathcal{N}( e ) ) }"+            , "  { if $ not( \\isnormal{ e } ) $ }"+            , "  { }"+            , "\\trrule{Mlambda}"+            , "  { \\mathbb{M}( [[ B_1, L> F, B_2 ]] * t ) }"+            , "  { \\mathbb{M}( e * t ) }"+            , "  { }"+            , "  { where $ e \\coloneqq lambda( [[ B_1, L> F, B_2 ]] ) $ }"+            , "\\trrule{Mphi}"+            , "  { \\mathbb{M}( Q . \\tau * t ) }"+            , "  { \\mathbb{M}( e * t ) }"+            , "  { }"+            , "  { where $ e \\coloneqq global( \\tau ) $ }"+            , "\\trrule{Mstuck}"+            , "  { \\mathbb{M}( e ) }"+            , "  { T }"+            , "  { }"+            , "  { }"+            , "\\end{tabular}"+            ]+        ]++    it "explains dataization rules" $+      testCLISucceeded+        ["explain", "--dataize"]+        [ unlines+            [ "\\begin{tabular}{rl}"+            , "\\trrule{delta}"+            , "  { \\mathbb{D}( [[ B_1, D> δ, B_2 ]] ) }"+            , "  { δ }"+            , "  { }"+            , "  { }"+            , "\\trrule{box}"+            , "  { \\mathbb{D}( [[ B_1, @ -> e, B_2 ]] ) }"+            , "  { \\mathbb{D}( e_1 ) }"+            , "  { if $ [ Δ, L ] \\cap ( B_1 \\cup B_2 ) = \\emptyset $ }"+            , "  { where $ e_1 \\coloneqq \\ctx{ e }{ [[ B_1, @ -> e, B_2 ]] } $ }"+            , "\\trrule{norm}"+            , "  { \\mathbb{D}( e ) }"+            , "  { \\mathbb{D}( \\mathbb{M}( e ) ) }"+            , "  { if $ e \\notin \\mathcal{P} $ }"+            , "  { }"+            , "\\trrule{none}"+            , "  { \\mathbb{D}( e ) }"+            , "  { \\varnothing }"+            , "  { }"+            , "  { }"+            , "\\end{tabular}"+            ]+        ]+     it "fails with no rules specified" $       testCLIFailed         ["explain"]-        ["Either --rule or --normalize must be specified"]+        ["Either --rule, --normalize, --morph or --dataize must be specified"]++    it "fails when more than one rule set is specified" $+      testCLIFailed+        ["explain", "--morph", "--dataize"]+        ["Only one of --rule, --normalize, --morph or --dataize can be specified"]      it "writes to target file" $       bracket

@@ -1,3 +1,4 @@+{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-}  -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com@@ -7,13 +8,16 @@  import AST import Control.Monad+import Data.List (nub) import Data.List.NonEmpty (NonEmpty (..))-import Dataize (DataizeContext (DataizeContext), dataize, dataize', morph)-import Deps (dontSaveStep)+import Dataize (DataizeContext (DataizeContext), dataize, dataize', execBuildTerm, morph)+import Deps (Term (TeExpression), dontSaveStep) import Functions (buildTerm)+import Matcher (substEmpty) import Parser (parseExpressionThrows, parseProgramThrows) import Rewriter (Rewritten) import Test.Hspec+import Yaml qualified  defaultDataizeContext :: Expression -> Program -> DataizeContext defaultDataizeContext loc prog = DataizeContext loc prog 25 25 False buildTerm dontSaveStep@@ -104,6 +108,82 @@         , Just (BtOne "01")         )       ]++  describe "execBuildTerm" $+    it "resolves global dispatch from the universe Q" $ do+      prog <- parseProgramThrows "Q -> [[ x -> [[ D> 42- ]] ]]"+      expected <- parseExpressionThrows "[[ D> 42- ]]"+      term <- execBuildTerm (defaultDataizeContext ExGlobal prog) "global" [Yaml.ArgAttribute (AtLabel "x")] substEmpty+      case term of+        TeExpression actual -> actual `shouldBe` expected+        _ -> expectationFailure "global() did not return an expression"++  describe "labels every step with a defined rule or operation" $ do+    let funcs = maybe [] (map Yaml.function)+        allowed =+          map (.name) Yaml.morphingRules+            ++ map (.name) Yaml.dataizationRules+            ++ map (.name) Yaml.normalizationRules+            ++ concatMap (funcs . (.where_)) Yaml.morphingRules+            ++ concatMap (funcs . (.where_)) Yaml.dataizationRules+    it "uses no step label without a defining rule or operation" $ do+      prog <-+        parseProgramThrows+          ( unlines+              [ "Q -> [["+              , "  bytes(data) -> [[ @ -> $.data ]],"+              , "  number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]],"+              , "  @ -> 5.plus(6)"+              , "]]"+              ]+          )+      loc <- parseExpressionThrows "Q"+      (_, chain) <- dataize (defaultDataizeContext loc prog)+      let orphans = nub [label | (_, Just label) <- chain, label `notElem` allowed]+      unless+        (null orphans)+        (expectationFailure ("Dataization emitted step labels with no defining rule or operation: " ++ show orphans))++  describe "preserves the reduction label sequence" $ do+    let labelsOf loc src = do+          prog <- parseProgramThrows src+          loc' <- parseExpressionThrows loc+          (_, chain) <- dataize (defaultDataizeContext loc' prog)+          pure [label | (_, Just label) <- chain]+    it "dataizes 5.plus(6) through the expected rules" $ do+      labels <-+        labelsOf+          "Q"+          "Q -> [[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"+      labels+        `shouldBe` [ "contextualize"+                   , "Mphi"+                   , "alpha"+                   , "copy"+                   , "dot"+                   , "copy"+                   , "alpha"+                   , "copy"+                   , "Mlambda"+                   , "Mphi"+                   , "alpha"+                   , "copy"+                   , "Mprim"+                   , "contextualize"+                   , "dot"+                   , "Mphi"+                   , "alpha"+                   , "copy"+                   , "copy"+                   , "Mprim"+                   , "contextualize"+                   , "dot"+                   , "copy"+                   , "Mprim"+                   ]+    it "dataizes a located reference through the expected rules" $ do+      labels <- labelsOf "Q.foo.bar" "Q -> [[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]"+      labels `shouldBe` ["contextualize", "Mphi", "Mprim"]    testDataize     [

@@ -409,6 +409,12 @@         , substs [[("t", MvTail [TaDispatch (AtLabel "org"), TaApplication (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))])]]         )       ,+        ( "Q.x * !t => Q.x(y -> [[]]) => [(!t >> [(y -> [[]])])]"+        , ExMetaTail (ExDispatch ExGlobal (AtLabel "x")) "t"+        , ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") (ExFormation [BiVoid AtRho]))+        , substs [[("t", MvTail [TaApplication (BiTau (AtLabel "y") (ExFormation [BiVoid AtRho]))])]]+        )+      ,         ( "Q.!a * !t => Q.org.eolang(x -> [[]]) => [(!a >> org, !t >> [ .eolang, ( x -> [[ ]] ) ])]"         , ExMetaTail (ExDispatch ExGlobal (AtMeta "a")) "t"         , ExApplication (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))

@@ -469,6 +469,11 @@       , ("𝑒0", Just (ExMeta "e0"))       , ("!e.x", Just (ExDispatch (ExMeta "e") (AtLabel "x")))       , ("!e(Q)", Just (ExApplication (ExMeta "e") (BiTau (AtAlpha 0) ExGlobal)))+      , ("!n", Just (ExMeta "n"))+      , ("!n1", Just (ExMeta "n1"))+      , ("𝑛", Just (ExMeta "n"))+      , ("𝑛1", Just (ExMeta "n1"))+      , ("𝑛.x", Just (ExDispatch (ExMeta "n") (AtLabel "x")))       ]    describe "parse meta tails" $

@@ -93,7 +93,7 @@                     Just basic' ->                       mapM                         ( \name -> do-                            yaml <- ensuredFile ("resources" </> replaceExtension name ".yaml")+                            yaml <- ensuredFile ("resources/normalize" </> replaceExtension name ".yaml")                             Y.yamlRule yaml                         )                         basic'