phino 0.0.131 → 0.0.132

raw patch · 42 files changed

+1581/−1620 lines, 42 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +9/−5
• phino.cabal +4/−2
• resources/contextualization.yaml +0/−81
• resources/contextualization/ca.yaml +16/−0
• resources/contextualization/caa.yaml +16/−0
• resources/contextualization/cd.yaml +12/−0
• resources/contextualization/cf.yaml +7/−0
• resources/contextualization/cg.yaml +7/−0
• resources/contextualization/ct.yaml +7/−0
• resources/contextualization/cxi.yaml +7/−0
• resources/dataization.yaml +0/−101
• resources/dataization/box.yaml +20/−0
• resources/dataization/delta.yaml +8/−0
• resources/dataization/fire.yaml +14/−0
• resources/dataization/none.yaml +14/−0
• resources/dataization/norm.yaml +20/−0
• resources/morphing.yaml +0/−190
• resources/morphing/dead.yaml +7/−0
• resources/morphing/ma.yaml +14/−0
• resources/morphing/maa.yaml +14/−0
• resources/morphing/maad.yaml +13/−0
• resources/morphing/mad.yaml +13/−0
• resources/morphing/md.yaml +17/−0
• resources/morphing/mf.yaml +7/−0
• resources/morphing/mg.yaml +10/−0
• resources/morphing/ml.yaml +17/−0
• resources/morphing/mphi.yaml +26/−0
• resources/morphing/universe.yaml +18/−0
• resources/morphing/xi.yaml +10/−0
• src/Atoms.hs +20/−9
• src/CLI/Helpers.hs +2/−2
• src/CLI/Runners.hs +3/−2
• src/Dataize.hs +27/−614
• src/Deps.hs +1/−1
• src/Morph.hs +638/−0
• src/Yaml.hs +12/−15
• test/AtomsSpec.hs +30/−0
• test/CLISpec.hs +61/−61
• test/DataizeSpec.hs +59/−534
• test/Fixtures.hs +61/−2
• test/MorphSpec.hs +321/−0
• test/YamlSpec.hs +19/−1

@@ -260,11 +260,15 @@ {"id": 9, "𝑛": "⟦ Δ ⤍ 40-08-00-00-00-00-00-00 ⟧", "Δ": "40-08-00-00-00-00-00-00"} ``` -Every segment but the last has to name a formation to go on into, and-`reduce` applies to the node the path ends at. A segment the formation does-not carry, or one that runs into a void attribute, fails the fire the same-way a missing `attr` does. `phino` holds the receiver whole, so there is no-depth a program has to re-parse an answer to reach.+Every segment but the last has to name a formation or an application to go on+into, and `reduce` applies to the node the path ends at. An argument binds an+attribute the way a τ binding does, so `x.if.guard` reaches the `guard` of+`x ↦ Φ.bool( if ↦ ⟦ guard ↦ … ⟧ )`, and it binds it from the outside, so an+argument wins over the void it fills. A positional argument names nothing and+the walk goes past it. A segment nothing carries, or one that runs into a void+attribute, fails the fire the same way a missing `attr` does. `phino` holds the+receiver whole, so there is no depth a program has to re-parse an answer to+reach.  What the answered node is, `phino` says next to it, because the shape of an answer is `phino`'s knowledge and not the program's. A formation carrying a Δ

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.131+version: 0.0.132 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 resources/normalize/*.yaml+extra-source-files: resources/normalize/*.yaml resources/morphing/*.yaml resources/dataization/*.yaml resources/contextualization/*.yaml extra-doc-files: README.md  source-repository head@@ -61,6 +61,7 @@     Matcher     Merge     Misc+    Morph     Must     Parser     Printer@@ -152,6 +153,7 @@     MatcherSpec     MergeSpec     MiscSpec+    MorphSpec     MustSpec     ParserSpec     Paths_phino

@@ -1,81 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----# Contextualization 𝒞 — applied top-to-bottom, first matching clause wins. It is-# binary, 𝒞(n, c): n is the term being contextualized and c is the context (the-# expression that every free ξ inside n stands for). 𝒞 walks the term-# structurally, replacing each ξ with the context c, descending through-# dispatches and applications and stopping at formations — which introduce their-# own scope and are returned untouched — and at the global Φ and termination ⊥.-# The context c is supplied by the caller: DOT dispatching 𝜏 on a formation-# passes that formation WITHOUT the dispatched binding (⟦𝐵1, 𝐵2⟧), so a-# self-referential ξ resolves to an object that lacks 𝜏 and collapses to ⊥-# rather than re-deriving the dispatch and diverging.-#-# Each rule is an inference rule: when 'match' matches the term and 'c-match'-# matches the context (binding the meta c), the rule yields the conclusion-# 'c-result' (a premise meta or a literal), provided the ordered 'premises'-# reduce as stated. A premise binds its 'n-result' to one 𝒞 ('contextualize')-# judgment. 'c-match' is the context-argument matcher of 𝒞(n, c); it is always-# the 𝑘0 meta. Derived terms are named 𝑛1, 𝑛2, … in premise order; the term 𝒞 is-# handed is 𝑛0, leaving that numbering to the premises alone. A meta the rule-# never reads back is written bare: it matches whatever stands in its place,-# binds nothing and cannot be referenced.--- name: cg-  match: Φ-  c-match: 𝑘0-  c-result: Φ--- name: cxi-  match: ξ-  c-match: 𝑘0-  c-result: 𝑘0--- name: ct-  match: ⊥-  c-match: 𝑘0-  c-result: ⊥--- name: cf-  match: ⟦𝐵0⟧-  c-match: 𝑘0-  c-result: ⟦𝐵0⟧--- name: cd-  match: '𝑛0.𝜏0'-  c-match: 𝑘0-  c-result: '𝑛1.𝜏0'-  premises:-    - n-result: 𝑛1-      contextualize:-        - 𝑛0-        - 𝑘0--- name: ca-  match: '𝑛0(𝜏0 ↦ 𝑒1)'-  c-match: 𝑘0-  c-result: '𝑛1(𝜏0 ↦ 𝑛2)'-  premises:-    - n-result: 𝑛1-      contextualize:-        - 𝑛0-        - 𝑘0-    - n-result: 𝑛2-      contextualize:-        - 𝑒1-        - 𝑘0--- name: caa-  match: '𝑛0(α𝑖0 ↦ 𝑒1)'-  c-match: 𝑘0-  c-result: '𝑛1(α𝑖0 ↦ 𝑛2)'-  premises:-    - n-result: 𝑛1-      contextualize:-        - 𝑛0-        - 𝑘0-    - n-result: 𝑛2-      contextualize:-        - 𝑒1-        - 𝑘0

@@ -0,0 +1,16 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: ca+match: '𝑛0(𝜏0 ↦ 𝑒1)'+c-match: 𝑘0+c-result: '𝑛1(𝜏0 ↦ 𝑛2)'+premises:+  - n-result: 𝑛1+    contextualize:+      - 𝑛0+      - 𝑘0+  - n-result: 𝑛2+    contextualize:+      - 𝑒1+      - 𝑘0

@@ -0,0 +1,16 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: caa+match: '𝑛0(α𝑖0 ↦ 𝑒1)'+c-match: 𝑘0+c-result: '𝑛1(α𝑖0 ↦ 𝑛2)'+premises:+  - n-result: 𝑛1+    contextualize:+      - 𝑛0+      - 𝑘0+  - n-result: 𝑛2+    contextualize:+      - 𝑒1+      - 𝑘0

@@ -0,0 +1,12 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: cd+match: '𝑛0.𝜏0'+c-match: 𝑘0+c-result: '𝑛1.𝜏0'+premises:+  - n-result: 𝑛1+    contextualize:+      - 𝑛0+      - 𝑘0

@@ -0,0 +1,7 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: cf+match: ⟦𝐵0⟧+c-match: 𝑘0+c-result: ⟦𝐵0⟧

@@ -0,0 +1,7 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: cg+match: Φ+c-match: 𝑘0+c-result: Φ

@@ -0,0 +1,7 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: ct+match: ⊥+c-match: 𝑘0+c-result: ⊥

@@ -0,0 +1,7 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: cxi+match: ξ+c-match: 𝑘0+c-result: 𝑘0

@@ -1,101 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----# Dataization 𝔻 — applied top-to-bottom, first matching clause wins. It is-# ternary, 𝔻(n, e, s): the second argument e is the global universe, the same-# expression that 𝕄 takes as its second argument (𝔻 forwards it to 𝕄), and the-# third argument s is the mutable state, threaded through and returned possibly-# changed. Only the 'fire' rule changes it, by firing an atom through 𝔼. The-# first argument is always a normal form: a non-NF expression matches no clause.-#-# Each rule is an inference rule: when 'match' matches the term and 'e-match'-# matches the universe (binding the meta e), the rule yields the conclusion-# 'd-result' (a premise bytes meta or a literal), provided 'when' holds and the-# ordered 'premises' reduce as stated. A premise binds its 'n-result'/'d-result'-# to one judgment — 𝔻 ('dataize'), 𝕄 ('morph'), 𝒩 ('normalize'), 𝔼 ('evaluate')-# or 𝒞 ('contextualize'). 'e-match' is the universe-argument matcher of-# 𝔻(n, e); it is always the 𝑒0 meta. The single bytes result is named δ0. A-# normal-form-valued result (𝕄 'morph', 𝒩 'normalize', 𝔼 'evaluate') is named-# 𝑛1, 𝑛2, … in premise order; the term 𝔻 is handed is 𝑛0, leaving that-# numbering to the premises alone. An expression-valued result (𝒞-# 'contextualize') is not a normal form — that is why a 'normalize' premise-# follows it — so it takes an 𝑒-family name (𝑒1, 𝑒2, …, the next index free of-# 'match', 𝑒0 itself being the universe) rather than an 𝑛 name reserved for-# normal forms. A meta the rule never reads back is written bare: it matches-# whatever stands in its place, binds nothing and cannot be referenced.-#-# The clauses are disjoint, so their relative order does not change behavior.-# 'norm' matches the lone meta 𝑛0, which unifies with any expression, so it is-# guarded to fire only when 𝑛0 is neither a formation ('not (formation 𝑛0)',-# carving out 'delta', 'box', 'fire' and 'none') nor the termination ⊥-# ('not (𝑛0 = ⊥)'). 𝔻 is partial: ⊥ (the terminator T) signals an error and-# lies outside its domain, so it deliberately matches no clause and dataization-# stops there — there is no 'end' rule mapping ⊥ to empty bytes (see #955).-# Without the guard 'norm' would behave correctly only by being declared last;-# with it the clauses no longer rely on their order.--- name: delta-  label: \Delta-  match: ⟦𝐵1, Δ ⤍ δ0, 𝐵2⟧-  e-match: 𝑒0-  d-result: δ0--- name: box-  match: ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧-  e-match: 𝑒0-  d-result: δ0-  when:-    disjoint:-      - [Δ, λ]-      - [𝐵1, 𝐵2]-  premises:-    - n-result: 𝑒2-      contextualize:-        - 𝑒1-        - ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧-    - n-result: 𝑛1-      normalize: 𝑒2-    - d-result: δ0-      dataize: 𝑛1--- name: fire-  match: ⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧-  e-match: 𝑒0-  d-result: δ0-  premises:-    - n-result: 𝑛1-      evaluate:-        - ⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧-        - 𝑒0-    - d-result: δ0-      dataize: 𝑛1--- name: none-  match: ⟦𝐵0⟧-  e-match: 𝑒0-  d-result: δ0-  when:-    disjoint:-      - [Δ, λ, φ]-      - [𝐵0]-  premises:-    - d-result: δ0-      dataize: ⊥--- name: norm-  match: 𝑛0-  e-match: 𝑒0-  d-result: δ0-  when:-    and:-      - not:-          formation: 𝑛0-      - not:-          eq:-            - 𝑛0-            - ⊥-  premises:-    - n-result: 𝑛1-      morph: 𝑛0-    - d-result: δ0-      dataize: 𝑛1

@@ -0,0 +1,20 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: box+match: ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧+e-match: 𝑒0+d-result: δ0+when:+  disjoint:+    - [Δ, λ]+    - [𝐵1, 𝐵2]+premises:+  - n-result: 𝑒2+    contextualize:+      - 𝑒1+      - ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧+  - n-result: 𝑛1+    normalize: 𝑒2+  - d-result: δ0+    dataize: 𝑛1

@@ -0,0 +1,8 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: delta+label: \Delta+match: ⟦𝐵1, Δ ⤍ δ0, 𝐵2⟧+e-match: 𝑒0+d-result: δ0

@@ -0,0 +1,14 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: fire+match: ⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧+e-match: 𝑒0+d-result: δ0+premises:+  - n-result: 𝑛1+    evaluate:+      - ⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧+      - 𝑒0+  - d-result: δ0+    dataize: 𝑛1

@@ -0,0 +1,14 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: none+match: ⟦𝐵0⟧+e-match: 𝑒0+d-result: δ0+when:+  disjoint:+    - [Δ, λ, φ]+    - [𝐵0]+premises:+  - d-result: δ0+    dataize: ⊥

@@ -0,0 +1,20 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: norm+match: 𝑛0+e-match: 𝑒0+d-result: δ0+when:+  and:+    - not:+        formation: 𝑛0+    - not:+        eq:+          - 𝑛0+          - ⊥+premises:+  - n-result: 𝑛1+    morph: 𝑛0+  - d-result: δ0+    dataize: 𝑛1

@@ -1,190 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----# Morphing 𝕄 — applied top-to-bottom, first matching clause wins. It is ternary,-# 𝕄(n, e, s): n is the morphed term, e is the fixed global universe and s is-# the mutable state. The universe is threaded unchanged through every recursive-# call and substituted for Φ by the 'universe' rule (Φ, rendered Q, is just the-# locator of e); the state is threaded too and the new state returned. Only the-# 'ml' rule changes it, by firing an atom through 𝔼. The first argument is-# always a normal form: a non-NF expression matches no clause. 𝕄 navigates a-# normal form to a formation one operation at a time, resolving Φ against e and-# peeling dispatches and applications through normalization 𝒩. It never fires a-# bare atom: a saturated λ-formation is returned untouched and fired later by 𝔼-# (the 'fire' rule of 𝔻).-#-# Each rule is an inference rule: when 'match' matches the term and 'e-match'-# matches the universe (binding the meta e), the rule yields the conclusion-# 'n-result' (a premise meta or a literal), provided 'when' holds and the-# ordered 'premises' reduce as stated. A premise binds 'n-result' to the result-# of one judgment — 𝕄 ('morph'), 𝒩 ('normalize') or 𝔼 ('evaluate'). 'e-match' is-# the universe-argument matcher of 𝕄(n, e); usually the 𝑒0 meta, but a rule may-# pin it to a literal (e.g. 'mg' fires only on 𝕄(Φ, Φ)). Every judgment here is-# normal-form-valued (𝕄 'morph', 𝒩 'normalize', 𝔼 'evaluate' — 𝔼 normalizes its-# atom's result internally), so premise results are named 𝑛1, 𝑛2, … in premise-# order. The term a rule morphs is 𝑛0 and its universe 𝑒0, leaving that-# numbering to the premises alone; the 𝑒-family stays reserved for the universe.-# A meta the rule never reads back is written bare (see 'mad'): it matches-# whatever stands in its place, binds nothing and cannot be referenced.-#-# 'ml' and 'md' are kept mutually exclusive: 'md' fires only-# when its head 𝑛0 is not a formation ('not (formation 𝑛0)'), so every formation-# head — λ-bearing or not — is left to 'ml' (and 'mf'). The two clauses-# are disjoint and their relative order does not change behavior.-#-# 'ma'/'maa' and 'mad'/'maad' partition application-headed normal forms on-# the argument's absoluteness (#959). Both pairs pin the argument to a-# normal-form meta, so the split is total over the normal forms 𝕄 actually-# sees: 'ma'/'maa' take a '𝑘1' argument — absolute (xi-free) and in normal-# form — and recurse by re-normalizing the application; 'mad'/'maad' take an-# '𝑛1' argument (a normal form) that is 'not (absolute 𝑛1)' and yield ⊥-# through a single 'morph: ⊥' premise, which terminates at once via the-# 'dead' axiom (𝕄(⊥, e, s) → (⊥, s)) — no recursion. A non-absolute argument-# can never fill a slot, so ⊥ is the correct outcome and morphing stays-# total: exactly one of the four fires, and these ⊥ premises add no regress.-# Without them, a void slot receiving a-# non-absolute argument — e.g. ⟦ x ↦ ∅ ⟧( x ↦ ξ.foo ) — had no terminating-# derivation: 'copy' cannot fire on a non-absolute argument, so 'ma'-# re-morphed the identical stuck term forever.--- name: mf-  match: ⟦𝐵0⟧-  e-match: 𝑒0-  n-result: ⟦𝐵0⟧--- name: ml-  label: \lambda-  match: '⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧.𝜏0'-  e-match: 𝑒0-  n-result: 𝑛3-  premises:-    - n-result: 𝑛1-      evaluate:-        - '⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧'-        - 𝑒0-    - n-result: 𝑛2-      normalize: '𝑛1.𝜏0'-    - n-result: 𝑛3-      morph: 𝑛2--- name: mphi-  label: \varphi-  match: ⟦𝐵0⟧.𝜏0-  e-match: 𝑒0-  n-result: 𝑛2-  when:-    and:-      - in:-          - φ-          - 𝐵0-      - not:-          in:-            - 𝜏0-            - 𝐵0-      - not:-          in:-            - λ-            - 𝐵0-  premises:-    - n-result: 𝑛1-      normalize: ⟦𝐵0⟧.φ.𝜏0-    - n-result: 𝑛2-      morph: 𝑛1--- name: md-  match: '𝑛0.𝜏0'-  e-match: 𝑒0-  n-result: 𝑛3-  when:-    not:-      formation: 𝑛0-  premises:-    - n-result: 𝑛1-      morph: 𝑛0-    - n-result: 𝑛2-      normalize: '𝑛1.𝜏0'-    - n-result: 𝑛3-      morph: 𝑛2--- name: ma-  match: '𝑛0(𝜏0 ↦ 𝑘1)'-  e-match: 𝑒0-  n-result: 𝑛3-  premises:-    - n-result: 𝑛1-      morph: 𝑛0-    - n-result: 𝑛2-      normalize: '𝑛1(𝜏0 ↦ 𝑘1)'-    - n-result: 𝑛3-      morph: 𝑛2--- name: maa-  match: '𝑛0(α𝑖0 ↦ 𝑘1)'-  e-match: 𝑒0-  n-result: 𝑛3-  premises:-    - n-result: 𝑛1-      morph: 𝑛0-    - n-result: 𝑛2-      normalize: '𝑛1(α𝑖0 ↦ 𝑘1)'-    - n-result: 𝑛3-      morph: 𝑛2--- name: mad-  match: '𝑛(𝜏 ↦ 𝑛1)'-  e-match: 𝑒0-  n-result: 𝑛2-  when:-    not:-      absolute: 𝑛1-  premises:-    - n-result: 𝑛2-      morph: ⊥--- name: maad-  match: '𝑛(α𝑖 ↦ 𝑛1)'-  e-match: 𝑒0-  n-result: 𝑛2-  when:-    not:-      absolute: 𝑛1-  premises:-    - n-result: 𝑛2-      morph: ⊥--- name: universe-  label: \Phi-  match: Φ-  e-match: 𝑒0-  n-result: 𝑛2-  when:-    not:-      eq:-        - 𝑒0-        - Φ-  premises:-    - n-result: 𝑛1-      normalize: 𝑒0-    - n-result: 𝑛2-      morph: 𝑛1--- name: dead-  match: ⊥-  e-match: 𝑒0-  n-result: ⊥--- name: xi-  match: ξ-  e-match: 𝑒0-  n-result: 𝑛1-  premises:-    - n-result: 𝑛1-      morph: ⊥--- name: mg-  match: Φ-  e-match: Φ-  n-result: 𝑛1-  premises:-    - n-result: 𝑛1-      morph: ⊥

@@ -0,0 +1,7 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: dead+match: ⊥+e-match: 𝑒0+n-result: ⊥

@@ -0,0 +1,14 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: ma+match: '𝑛0(𝜏0 ↦ 𝑘1)'+e-match: 𝑒0+n-result: 𝑛3+premises:+  - n-result: 𝑛1+    morph: 𝑛0+  - n-result: 𝑛2+    normalize: '𝑛1(𝜏0 ↦ 𝑘1)'+  - n-result: 𝑛3+    morph: 𝑛2

@@ -0,0 +1,14 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: maa+match: '𝑛0(α𝑖0 ↦ 𝑘1)'+e-match: 𝑒0+n-result: 𝑛3+premises:+  - n-result: 𝑛1+    morph: 𝑛0+  - n-result: 𝑛2+    normalize: '𝑛1(α𝑖0 ↦ 𝑘1)'+  - n-result: 𝑛3+    morph: 𝑛2

@@ -0,0 +1,13 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: maad+match: '𝑛(α𝑖 ↦ 𝑛1)'+e-match: 𝑒0+n-result: 𝑛2+when:+  not:+    absolute: 𝑛1+premises:+  - n-result: 𝑛2+    morph: ⊥

@@ -0,0 +1,13 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: mad+match: '𝑛(𝜏 ↦ 𝑛1)'+e-match: 𝑒0+n-result: 𝑛2+when:+  not:+    absolute: 𝑛1+premises:+  - n-result: 𝑛2+    morph: ⊥

@@ -0,0 +1,17 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: md+match: '𝑛0.𝜏0'+e-match: 𝑒0+n-result: 𝑛3+when:+  not:+    formation: 𝑛0+premises:+  - n-result: 𝑛1+    morph: 𝑛0+  - n-result: 𝑛2+    normalize: '𝑛1.𝜏0'+  - n-result: 𝑛3+    morph: 𝑛2

@@ -0,0 +1,7 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: mf+match: ⟦𝐵0⟧+e-match: 𝑒0+n-result: ⟦𝐵0⟧

@@ -0,0 +1,10 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: mg+match: Φ+e-match: Φ+n-result: 𝑛1+premises:+  - n-result: 𝑛1+    morph: ⊥

@@ -0,0 +1,17 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: ml+label: \lambda+match: '⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧.𝜏0'+e-match: 𝑒0+n-result: 𝑛3+premises:+  - n-result: 𝑛1+    evaluate:+      - '⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧'+      - 𝑒0+  - n-result: 𝑛2+    normalize: '𝑛1.𝜏0'+  - n-result: 𝑛3+    morph: 𝑛2

@@ -0,0 +1,26 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: mphi+label: \varphi+match: ⟦𝐵0⟧.𝜏0+e-match: 𝑒0+n-result: 𝑛2+when:+  and:+    - in:+        - φ+        - 𝐵0+    - not:+        in:+          - 𝜏0+          - 𝐵0+    - not:+        in:+          - λ+          - 𝐵0+premises:+  - n-result: 𝑛1+    normalize: ⟦𝐵0⟧.φ.𝜏0+  - n-result: 𝑛2+    morph: 𝑛1

@@ -0,0 +1,18 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: universe+label: \Phi+match: Φ+e-match: 𝑒0+n-result: 𝑛2+when:+  not:+    eq:+      - 𝑒0+      - Φ+premises:+  - n-result: 𝑛1+    normalize: 𝑒0+  - n-result: 𝑛2+    morph: 𝑛1

@@ -0,0 +1,10 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: xi+match: ξ+e-match: 𝑒0+n-result: 𝑛1+premises:+  - n-result: 𝑛1+    morph: ⊥

@@ -55,7 +55,9 @@ -- question from the formation it already holds for that request, so neither -- side ever re-prints a receiver the other side has in hand (#1165). The -- 'attr' may go deeper than one name: 'ρ.length' is a path down the receiver,--- read left to right, since phino holds the whole of it anyway (#1207).+-- read left to right, since phino holds the whole of it anyway (#1207). It+-- walks applications as well as formations, an argument being as much a+-- binding as a τ inside a formation (#1212). -- -- Whichever way it was asked, an answer says what the node under '𝑛' carries, -- so that no program keeps a 𝜑 reader of its own to tell a datum from a stuck@@ -550,30 +552,39 @@               Nothing -> Left (printf "the receiver of request %d carries no attribute '%s'" req (T.unpack attrName))               Just held -> Right held         -- Walk the dotted path of 'attr' down the receiver: every segment but-        -- the last has to name a formation to go on into, and the last one is-        -- what the question is about. An attribute bound to nothing at all-        -- carries nothing to descend into, so a path through a void one names-        -- no attribute (#1207).+        -- the last has to name a formation or an application to go on into,+        -- and the last one is what the question is about. An attribute bound+        -- to nothing at all carries nothing to descend into, so a path through+        -- a void one names no attribute (#1207).         descended :: Expression -> Maybe Held         descended form' = foldM deeper (Bound form') (T.splitOn "." attrName)         deeper :: Held -> T.Text -> Maybe Held         deeper (Bound expr) name = attributeValue name expr         deeper Void _ = Nothing+        -- An argument of an application binds an attribute the way a τ+        -- binding of a formation does, and it is the outer of the two, so it+        -- is what the attribute is whatever the formation under it still says+        -- about it. A positional argument names nothing, so the walk goes past+        -- it into what the application applies to (#1212).         attributeValue :: T.Text -> Expression -> Maybe Held         attributeValue name (ExFormation bds) = go bds           where             go :: [Binding] -> Maybe Held             go [] = Nothing             go (BiTau attr value : rest)-              | named attr = Just (Bound value)+              | named name attr = Just (Bound value)               | otherwise = go rest             go (BiVoid attr : rest)-              | named attr = Just Void+              | named name attr = Just Void               | otherwise = go rest             go (_ : rest) = go rest-            named :: Attribute -> Bool-            named attr = T.pack (printAttribute attr) == name+        attributeValue name (ExApplication applied (ArTau attr value))+          | named name attr = Just (Bound value)+          | otherwise = attributeValue name applied+        attributeValue name (ExApplication applied _) = attributeValue name applied         attributeValue _ _ = Nothing+        named :: T.Text -> Attribute -> Bool+        named name attr = T.pack (printAttribute attr) == name     -- Reduce the 𝜑-expression the program asks about and say it back under     -- '𝑛', with the 'id' the question minted. A program started for the fire     -- has nothing to be answered over, since phino closed its stdin behind the

@@ -17,7 +17,6 @@ import Data.IORef import Data.List (intercalate, nub) import Data.Maybe-import Dataize (DataizeContext, insideUniverse) import Deps (SaveEvalFunc, SaveStepFunc, dontSaveEval, saveEval, saveStep) import Encoding import Files (ensuredFile)@@ -26,6 +25,7 @@ import Lining (LineFormat (SINGLELINE)) import Locator (locatedExpression) import Logger+import Morph (ReduceContext, insideUniverse) import Parser (parseExpressionThrows) import qualified Printer as P import qualified Random as R@@ -104,7 +104,7 @@ -- expression, which the run takes as the universe, and the locator becomes that -- attribute (see 'insideUniverse'). Without the option nothing moves and the -- context is handed back as it came.-aimed :: Maybe String -> Expression -> DataizeContext -> IO (Expression, DataizeContext)+aimed :: Maybe String -> Expression -> ReduceContext -> IO (Expression, ReduceContext) aimed Nothing expr ctx = pure (expr, ctx) aimed (Just src) expr@(ExFormation _) ctx = do   target <- parseExpressionThrows src

@@ -28,6 +28,7 @@ import Logger import Margin (defaultMargin) import Merge (merge)+import Morph import Parser (parseExpressionThrows) import qualified Printer as P import qualified Random as R@@ -167,7 +168,7 @@       ( \record -> do           -- The deep walk belongs to 𝕄 alone (the '--deep' of 'morph'), since 𝔻           -- reduces what dataization demands and ends in bytes, so it is off here.-          let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial False atoms buildTerm save record+          let ctx = ReduceContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial False atoms buildTerm reduction save record           (universe, aiming) <- aimed _inside expr ctx           dataize universe aiming       )@@ -252,7 +253,7 @@       _evaluations       printCtx       ( \record -> do-          let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial _deep atoms buildTerm save record+          let ctx = ReduceContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial _deep atoms buildTerm reduction save record           (universe, aiming) <- aimed _inside expr ctx           morph universe aiming       )

@@ -1,113 +1,41 @@-{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DerivingStrategies #-}-{-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-name-shadowing #-}-{-# OPTIONS_GHC -Wno-unused-record-wildcards #-}  -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Dataize (morph, morph', dataize, dataize', insideUniverse, DataizeContext (..), DataizeException (..), Outcome (..), Steps (..), State, emptyState, execBuildTerm) where+-- The Dataization function 𝔻 and what a program asking phino to reduce one of+-- its own terms gets back. Everything 𝔻 shares with the Morphing function 𝕄 —+-- the context, the budget, the signals, the premise plumbing — lives in+-- 'Morph', which this module imports.+module Dataize (dataize, dataize', reduction, Outcome (..)) where  import AST-import Atoms (ReduceFunc, Registry, fireAtom, registeredAtom)-import Builder (buildBytesThrows, buildExpressionThrows, contextualize)-import Control.Exception (Exception, catch, throwIO, try)-import Control.Monad (foldM, when)-import Data.List (find, partition)+import Atoms (ReduceFunc)+import Builder (buildBytesThrows, buildExpressionThrows)+import Control.Exception (throwIO, try)+import Control.Monad (foldM)+import Data.List (find) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE-import Data.Maybe (fromMaybe)-import qualified Data.Text as T-import Deps (BuildTermFunc, BuildTermMethodS, Evaluation (..), SaveEvalFunc, SaveStepFunc, State, Term (..))-import Locator (locatedExpression, withLocatedExpression)-import Matcher (MetaValue (..), Subst (..), combine, matchExpression', substEmpty, substSingle)-import Must (Must (..))+import Deps (State)+import Locator (locatedExpression)+import Matcher (Subst, matchExpression')+import Morph (Morphed, ReduceContext (..), ReduceException (..), deeper, emptyState, excluding, execBuildTerm, insideUniverse, leadsTo, morph', normalized, parking, producer, sidePremise, verb) import Random (shuffle)-import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite)+import Rewriter (Rewritten) import Rule (RuleContext (RuleContext), matchExpressionWithRule') import Text.Printf (printf)-import Yaml (ExtraArgument (..), normalizationRules) import qualified Yaml as Y  type Dataized = (Bytes, [Rewritten]) -type Dataizable = (Expression, NonEmpty Rewritten)--type Morphed = Dataizable---- The initial, empty state used when dataization starts. The 'State' type itself--- lives in 'Deps' next to 'BuildTermMethod'.-emptyState :: State-emptyState = ""---- How many steps of the 𝕄/𝔻 recursion one branch of a derivation may take--- ('_limit', the '--max-steps' option) and how many the branch reaching this--- point has already taken ('_spent'). 𝕄 and 𝔻 recurse into each other, into the--- premises of their own rules and into the atoms they fire, so a budget local to--- one of those chains is reset by the next nested call and bounds nothing (see--- #1052). This one rides in the context that every such path — the spine, the--- side-premises, '_dataize' and '_morph' — already carries, so a nested call--- inherits the count of the call that made it. It bounds depth, not total work:--- a premise passes its count down but not back, so siblings each descend from--- the same '_spent'. Bounding every branch is enough to terminate, since a rule--- has finitely many premises.-data Steps = Steps-  { _limit :: Int-  , _spent :: Int-  }---- The evaluation context carries the configuration plus the step budget spent so--- far. Nothing global is fixed here: the universe (the second argument 'e' of--- 𝕄(n, e, s) and 𝔻(n, e, s)) is a plain expression threaded as an argument to--- 'dataize'', 'morph'' and on to the atoms, and the state 's' is threaded the same--- way (see 'State'). The working expression needed for normalization is taken--- from the head of the step chain, so no separate wrapper type is threaded--- around.-data DataizeContext = DataizeContext-  { _locator :: Expression-  , _maxDepth :: Int-  , _maxCycles :: Int-  , _steps :: Steps-  , _depthSensitive :: Bool-  , _shuffle :: Bool-  , _partial :: Bool-  , _deep :: Bool-  , _atoms :: Registry-  , _buildTerm :: BuildTermFunc-  , _saveStep :: SaveStepFunc-  , _saveEval :: SaveEvalFunc-  }--data DataizeException-  = OutOfSteps Int-  | -- An atom could not fire: the '--atoms' registry carries no λ function of-    -- that name, so there is nothing to run. The name is that of the atom 𝔼-    -- actually failed on, which for a chain of dispatches is the innermost one,-    -- since 'ml' reduces a head before the atom above it fires.-    Stuck T.Text-  | -- A 'Stuck' caught by a frame of the 𝕄/𝔻 spine, together with the-    -- derivation that frame had reached (see 'parking'). The head of the chain-    -- is the working expression with the stuck application left intact and-    -- everything reduced before it already in place: the residual program that-    -- '_partial' turns into the 'Residual' outcome.-    StuckAt T.Text (NonEmpty Rewritten)-  | -- An 'OutOfSteps' caught by a spine frame, carrying that frame's derivation-    -- just like 'StuckAt': a term that never reduces is a stuck site too, so-    -- '_partial' parks it and hands back the residual instead of failing hard-    -- (#1078)-    OutOfStepsAt Int (NonEmpty Rewritten)-  deriving anyclass (Exception)--instance Show DataizeException where-  show (OutOfSteps limit) =-    printf "Dataization did not finish before reaching the limit of steps: --max-steps=%d" limit-  show (OutOfStepsAt limit _) = show (OutOfSteps limit)-  show (Stuck func) = printf "Atom '%s' does not exist" (T.unpack func)-  show (StuckAt func _) = show (Stuck func)+-- What 𝔻 is handed: a term plus the derivation that reached it, the same pair+-- 𝕄 works on (see 'Morphed').+type Dataizable = Morphed  -- What a run of 𝔻 ends with: the bytes it reached or, under '_partial', the -- residual program: what the known inputs decided is computed, the stuck atom@@ -117,337 +45,6 @@   | Residual Expression   deriving stock (Eq, Show) --- Charge one step of the 𝕄/𝔻 recursion to the budget, refusing to descend once--- it is gone. '--max-cycles' and '--max-depth' bound only the normalization run--- inside a single step, so before this the recursion itself was unbounded and a--- term that never reduces to bytes kept 𝕄 and 𝔻 calling each other forever--- (#1052). Rewriting hands back whatever it has reached when it runs out of--- cycles; 𝔻 has no partial answer to give, so an exhausted budget always throws,--- with or without '--depth-sensitive'.-deeper :: DataizeContext -> IO DataizeContext-deeper ctx@DataizeContext{_steps = Steps limit spent}-  | spent >= limit = throwIO (OutOfSteps limit)-  | otherwise = pure ctx{_steps = Steps limit (spent + 1)}---- Split the λ binding off a formation for the LAMBDA morphing rule: the name of--- the atom to fire and the formation it fires against, the λ binding removed —--- the two things 𝔼 reports besides the result. A formation with no λ binding,--- or with more than one, has nothing to fire.-lambda :: [Binding] -> Maybe (T.Text, Expression)-lambda bds = case partition isLambda bds of-  ([BiLambda (Function func)], rest) -> Just (func, ExFormation rest)-  _ -> Nothing-  where-    isLambda :: Binding -> Bool-    isLambda (BiLambda _) = True-    isLambda _ = False---- The same as 'lambda', but only for a formation that is saturated: one with--- every binding of it filled (see 'filled'). A void is an argument the program--- has not given yet, so such a formation is a method waiting to be applied--- rather than an application waiting to be computed, and firing it would hand--- the atom a ∅ where it expects a value. 𝔻 needs no such guard, since it--- fires only what dataization demands and nothing demands a method; the deep--- walk meets every one a program declares — the method table of the object--- model above all — so it asks first (see 'deepened').-saturated :: [Binding] -> Maybe (T.Text, Expression)-saturated bds = case lambda bds of-  Just (func, ExFormation rest) | all filled rest -> Just (func, ExFormation rest)-  _ -> Nothing---- Whether a binding hands the formation something to work with. A void does--- not: it names an argument the program has still to supply. Neither does ⊥:--- the deep walk reduces a body in the scope of the formation around it, and a--- formation standing unapplied still holds ρ ↦ ∅, so a ξ.ρ in that body comes--- back as ⊥ rather than as the object the next dispatch supplies (#1196).-filled :: Binding -> Bool-filled (BiVoid _) = False-filled (BiTau _ ExTermination) = False-filled _ = True---- Run one frame of the 𝕄/𝔻 spine, attaching its derivation to a stuck atom or--- an exhausted budget escaping it. 'Stuck' is raised deep inside an atom, which--- knows nothing about the chain, so the innermost spine frame it reaches is the--- one to record where the derivation stopped: the head of that frame's chain is--- the working expression with the stuck application intact and everything--- reduced before it already in place. The same holds for 'OutOfSteps': a term--- cycling through the universe is no more a failure of the chain than a missing--- atom is, and under '_partial' it deserves the same parked residual (#1078).--- Outer frames see the '…At' signals and let them pass, since their chains are--- prefixes of that one; a side-computation running on a chain of its own strips--- the chain off again (see 'unparked') before the signal reaches the spine.-parking :: NonEmpty Rewritten -> IO a -> IO a-parking seq action = action `catch` rethrow-  where-    rethrow :: DataizeException -> IO a-    rethrow (Stuck func) = throwIO (StuckAt func seq)-    rethrow (OutOfSteps limit) = throwIO (OutOfStepsAt limit seq)-    rethrow failure = throwIO failure---- Strip the derivation off a stuck atom escaping a side-computation that ran--- on a chain of its own — an atom dataizing its input through '_dataize', or a--- 'morph' premise through '_morph'. That chain is not the spine's, so it is--- dropped and the spine frame around the side-computation attaches its own--- (see 'parking').-unparked :: IO a -> IO a-unparked action = action `catch` rethrow-  where-    rethrow :: DataizeException -> IO a-    rethrow (StuckAt func _) = throwIO (Stuck func)-    rethrow (OutOfStepsAt limit _) = throwIO (OutOfSteps limit)-    rethrow failure = throwIO failure---- The Morphing function 𝕄 maps normal forms to formations. It is ternary,--- 𝕄(n, e, s): besides the term 'n' it takes the universe 'e' ('univ') — a plain--- expression — and the mutable state 's', returning the morphed term together--- with the new state. The universe is matched against the rule's 'e-match'--- pattern (usually the '𝑒' meta, which binds 'e' so the 'universe' rule substitutes--- it, but a rule may pin it to a literal such as 'mg' matching Φ). Its rules--- come from 'morphing.yaml': the first matching rule's premises are evaluated and--- its conclusion 'nresult' is built, always forwarding the same universe. The--- clauses are disjoint (see #856, #860), so their declaration order must not be--- load-bearing; when '_shuffle' is on (the '--shuffle' flag) the rules are--- shuffled before the 'firstMatch' walk to exercise that invariant — mirroring--- normalization's "apply until they stop matching". A genuinely order-independent--- step stays deterministic; a hidden overlap surfaces as a nondeterministic--- failure rather than staying silently green.--- The 'morph' premise that produces the conclusion is the spine: when--- its argument comes from a 'normalize' premise, the rewriter runs over that--- argument and its individual steps (alpha, copy, dot, …) are spliced into the--- chain before morphing continues. Every other premise is a side-computation--- evaluated in isolation by 'sidePremise', its own steps discarded.-morph' :: Morphed -> Expression -> State -> DataizeContext -> IO (Morphed, State)-morph' (expr, seq) univ state caller = do-  ctx <- deeper caller-  parking seq $ do-    rules <- if ctx._shuffle then shuffle Y.morphingRules else pure Y.morphingRules-    matched <- firstMatch ctx rules-    case matched of-      Just (rule, subst) -> reduce ctx rule subst-      Nothing -> throwIO (userError "no morphing rule matched")-  where-    firstMatch :: DataizeContext -> [Y.MorphRule] -> IO (Maybe (Y.MorphRule, Subst))-    firstMatch _ [] = pure Nothing-    firstMatch ctx (rule : rest) = do-      substs <- matchExpressionWithRule' (matchExpression' rule.ematch univ) expr (asRule rule) (RuleContext (execBuildTerm univ ctx))-      case substs of-        (subst : _) -> pure (Just (rule, subst))-        [] -> firstMatch ctx rest-    -- Match the conclusion term and check the guard; premises are no longer the-    -- matcher's business, so 'where'/'having' stay empty and the guard lives in-    -- 'when'. Every morphing guard reads only meta-variables bound by 'match'-    -- and 'e-match', so it holds before any premise runs.-    asRule :: Y.MorphRule -> Y.Rule-    asRule rule = Y.Rule rule.name Nothing Nothing rule.match ExRoot rule.when Nothing Nothing-    -- Evaluate the rule's premises and build its conclusion. A literal-    -- conclusion is terminal. Otherwise the conclusion meta is produced by a-    -- trailing 'morph' premise (the spine); if that premise's argument is itself-    -- bound by a 'normalize' premise, the normalization joins the spine and its-    -- steps splice in before morphing continues.-    reduce :: DataizeContext -> Y.MorphRule -> Subst -> IO (Morphed, State)-    reduce ctx rule subst = case producer rule.nresult rule.premises of-      Nothing -> do-        (final, state') <- sides ctx rule.premises subst-        built <- buildExpressionThrows rule.nresult final-        seq' <- leadsTo seq rule.name built ctx-        pure ((built, seq'), state')-      Just concl@(Y.Premise _ (Y.OpMorph arg)) -> case producer arg rule.premises of-        Just normal@(Y.Premise _ (Y.OpNormalize inner)) -> do-          (final, state') <- sides ctx (rule.premises `excluding` [concl, normal]) subst-          built <- buildExpressionThrows inner final-          labelled <- leadsTo seq rule.name built ctx-          (normal', seq') <- normalized built labelled ctx-          morph' (normal', seq') univ state' ctx-        _ -> do-          (final, state') <- sides ctx (rule.premises `excluding` [concl]) subst-          built <- buildExpressionThrows arg final-          seq' <- leadsTo seq rule.name built ctx-          morph' (built, seq') univ state' ctx-      Just _ -> throwIO (userError (printf "morphing rule '%s' must conclude with a 'morph' premise" rule.name))-    sides :: DataizeContext -> [Y.Premise] -> Subst -> IO (Subst, State)-    sides ctx premises subst = foldM (sidePremise univ ctx) (subst, state) premises---- Morph the expression located at '_locator' — 𝕄 asked on its own, the way--- 'dataize' asks 𝔻. The whole input expression is itself the universe Φ (the 'e'--- argument) threaded through 𝕄, so it is passed both as the located target and--- as the universe; the default locator Q therefore morphs the top formation,--- which 'mf' hands back unchanged, and '_locator' is how one aims 𝕄 at a--- subterm. Unlike 𝔻, 𝕄 is total: it stops at the first formation it reaches--- ('mf') and never demands bytes, and where no formation is reachable it answers--- with the terminator ⊥ ('dead', 'xi', 'mg', 'mad', 'maad') rather than failing.--- Only the atoms 'ml' fires can still get stuck, and '_partial' parks them just--- as it does under 𝔻: the answer is then the residual subterm the spine had--- reached, taken from '_locator' of its working expression. Stopping at the--- first formation leaves everything that formation holds as it was written,--- which is what '_deep' walks into before the answer is handed back (see--- 'deepened').-morph :: Expression -> DataizeContext -> IO (Expression, [Rewritten])-morph universe ctx@DataizeContext{..} = do-  expr <- locatedExpression _locator universe-  result <- try (morph' (expr, (universe, Nothing) :| []) universe emptyState ctx)-  case result of-    Right ((morphed, seq), state) -> walked morphed seq state-    Left (StuckAt _ seq) | _partial -> do-      residue <- locatedExpression _locator (fst (NE.head seq))-      walked residue seq emptyState-    Left (OutOfStepsAt _ seq) | _partial -> do-      residue <- locatedExpression _locator (fst (NE.head seq))-      walked residue seq emptyState-    Left failure -> throwIO (failure :: DataizeException)-  where-    -- The answer 𝕄 reached, walked by '_deep' before it is handed back (see-    -- 'deepened'), and the chain that led to both. The walk joins the chain as-    -- one step named 'deep', so '--sequence' ends on the term the command-    -- prints. Morphing starts from the empty state and the state the walk ends-    -- on goes the way 𝕄's own goes: no caller consumes it yet.-    walked :: Expression -> NonEmpty Rewritten -> State -> IO (Expression, [Rewritten])-    walked morphed seq state-      | not _deep = pure (morphed, reverse (NE.toList seq))-      | otherwise = do-          (deep, _) <- deepened morphed universe state ctx-          seq' <- leadsTo seq "deep" deep ctx-          pure (deep, reverse (NE.toList seq'))---- Walk what 𝕄 answered with, entering everything it left as it was written —--- the mechanism behind '--deep' ('_deep'). 𝕄 navigates a term to the first--- formation it reaches and 'mf' hands that formation back with its bindings--- untouched, since firing a bare λ is 𝔻's business; 𝔻 in turn follows the one--- path dataization demands and ends in bytes. A part of a program that nothing--- demands — the argument of an atom that cannot fire, for one — is therefore--- reduced by neither, and the object structure is lost to the one that does--- reduce it (#1124). This walk demands nothing either. It asks 𝕄 about every--- sub-expression and, where 𝕄 lands on a formation whose λ the registry--- serves, fires it and asks 𝕄 about the answer again (see 'fired'). A--- sub-expression on whose way an atom fired is replaced by the answer of the--- last firing; where none fired it stays as it was written and only its own--- parts are walked, so the calls the registry does not serve keep their names--- and what comes back is still the same program, reduced as far as the--- registry allows. Every entry is charged to the '--max-steps' budget, which--- is what bounds the walk.-deepened :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State)-deepened expr univ = go Nothing ExXi expr-  where-    -- A term as it was written, together with what its free ξ stands for: the-    -- formation the walk entered it from, without the binding it came from,-    -- exactly the context the 'dot' rule hands a dispatched body. At the top-    -- there is no such formation, so ξ stands for itself and contextualization-    -- leaves the term alone.-    go :: Maybe Attribute -> Expression -> Expression -> State -> DataizeContext -> IO (Expression, State)-    go dispatched context term state' caller = do-      ctx' <- deeper caller-      (walked, walkedState) <- parts context term state' caller-      answer <- fired dispatched (contextualize walked context) univ walkedState ctx'-      maybe (pure (walked, walkedState)) pure answer-    -- The parts of a term nothing fired on, walked one by one and put back-    -- where they were, so the term keeps the shape it was written in.-    parts :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State)-    parts _ (ExFormation bds) state' caller = do-      (entered, state'') <- bindings bds bds state' caller-      pure (ExFormation entered, state'')-    parts context (ExDispatch target attr) state' caller = do-      (entered, state'') <- go (Just attr) context target state' caller-      pure (ExDispatch entered attr, state'')-    parts context (ExApplication target arg) state' caller = do-      (entered, state'') <- go Nothing context target state' caller-      (applied, state''') <- argument context arg state'' caller-      pure (ExApplication entered applied, state''')-    parts _ term state' _ = pure (term, state')-    -- Walk the bindings of a formation left to right, threading the state-    -- through them. Only what the formation itself holds is entered: ρ names-    -- the object around it rather than one inside it, and a void, Δ or λ-    -- binding carries no term to walk at all.-    bindings :: [Binding] -> [Binding] -> State -> DataizeContext -> IO ([Binding], State)-    bindings _ [] state' _ = pure ([], state')-    bindings whole (BiTau attr body : rest) state' caller-      | attr /= AtRho = do-          (entered, state'') <- go Nothing (scope attr whole) body state' caller-          (others, state''') <- bindings whole rest state'' caller-          pure (BiTau attr entered : others, state''')-    bindings whole (bd : rest) state' caller = do-      (others, state'') <- bindings whole rest state' caller-      pure (bd : others, state'')-    -- The context a binding's body is entered in: the formation without that-    -- binding, the very context 'dot' contextualizes a dispatched body in, so-    -- a body reaching back at itself through ξ collapses instead of looping.-    scope :: Attribute -> [Binding] -> Expression-    scope attr bds = ExFormation (filter (not . named) bds)-      where-        named :: Binding -> Bool-        named (BiTau attr' _) = attr' == attr-        named _ = False-    -- Both sides of an application stand in the same context: the term it-    -- applies is walked by the caller and the argument it binds is walked here.-    argument :: Expression -> Argument -> State -> DataizeContext -> IO (Argument, State)-    argument context (ArTau attr arg) state' caller = do-      (entered, state'') <- go Nothing context arg state' caller-      pure (ArTau attr entered, state'')-    argument context (ArAlpha alpha arg) state' caller = do-      (entered, state'') <- go Nothing context arg state' caller-      pure (ArAlpha alpha entered, state'')---- Ask 𝕄 about a term and fire the λ of the formation it reaches, as long as--- the registry serves it, asking 𝕄 about every answer again: what comes back--- is the answer of the last firing, or nothing at all where no atom fired. This--- is the firing 'ml' makes without the dispatch that makes 'ml' make it — the--- one 𝕄 leaves to 𝔻 — except in what it hands back: the atom's raw answer, not--- the normal form 𝔼 makes of it, since the deep walk stands that answer back--- into the program, where a normal form would spell the whole object out in--- place of the name the program called it by. A λ the registry does not carry--- is left alone rather than fired and got stuck on, so what phino cannot--- compute stays as it was written with or without '_partial'; an atom that--- cannot fire deeper on the spine still fails the run, exactly as it does--- under 𝕄 alone, and '_partial' parks it. A formation still waiting for its--- arguments is left alone too (see 'saturated'). A term standing as the target--- of a dispatch is where 'ml' has its say: the λ is fired only where the--- dispatched attribute is none of the formation's own (see 'demanded').-fired :: Maybe Attribute -> Expression -> Expression -> State -> DataizeContext -> IO (Maybe (Expression, State))-fired dispatched term univ state caller = do-  ctx <- deeper caller-  morphed <- try (reduced ctx)-  case morphed of-    Right (ExFormation bds, state')-      | demanded bds -> maybe (pure Nothing) (evaluated ctx state') (saturated bds)-    Right _ -> pure Nothing-    Left failure -> parked failure-  where-    -- Whether the dispatch the term stands under demands the λ of the formation-    -- 𝕄 reached. 'ml' fires that λ only where the dispatched attribute is none-    -- of the formation's own, since 'dot' resolves the dispatch before 'ml' is-    -- ever reached, and a walk firing it first answers a formation the dispatch-    -- no longer fits (#1187). A term standing anywhere else is demanded by-    -- nothing and the walk fires what 'mf' left bare, as it always has.-    demanded :: [Binding] -> Bool-    demanded bds = not (any bound bds)-      where-        bound :: Binding -> Bool-        bound (BiTau attr _) = Just attr == dispatched-        bound _ = False-    -- 𝕄 takes normal forms only and a term taken from the program as it was-    -- written is not necessarily one, so it is normalized against the universe-    -- first, exactly as '--inside' normalizes what it is handed. Both chains-    -- are dropped: the walk is not the spine and reports one step of its own-    -- (see 'morph'), so a stuck atom leaves without a derivation ('unparked').-    reduced :: DataizeContext -> IO (Expression, State)-    reduced ctx = unparked $ do-      (normal, _) <- normalized term ((univ, Nothing) :| []) ctx-      ((morphed, _), state') <- morph' (normal, (univ, Nothing) :| []) univ state ctx-      pure (morphed, state')-    -- Fire the λ of the formation 𝕄 reached and go on from its answer, keeping-    -- the answer of the last firing. The firing is reported to '_saveEval' like-    -- every other one, with the term the caller is given, so the protocol and-    -- the program agree on what the atom answered.-    evaluated :: DataizeContext -> State -> (T.Text, Expression) -> IO (Maybe (Expression, State))-    evaluated ctx state' (func, self) = case registeredAtom ctx._atoms func of-      Nothing -> pure Nothing-      Just registered -> do-        answer <- fireAtom func registered self univ (reduction univ ctx)-        ctx._saveEval (Evaluation func self (Just answer))-        again <- fired dispatched answer univ state' ctx-        pure (Just (fromMaybe (answer, state') again))-    parked :: DataizeException -> IO (Maybe a)-    parked (Stuck _) | caller._partial = pure Nothing-    parked failure = throwIO failure- -- Dataize the expression located at '_locator'. The whole input expression is -- itself the universe Q (the 'e' argument) threaded through 𝔻 and 𝕄, so it is -- passed both as the located target and as the universe. An atom that cannot@@ -455,8 +52,8 @@ -- evaluation, and the run ends on the residual program the spine had reached -- (see 'StuckAt'), with the stuck application parked in it as a normal-form -- subterm, and the chain of steps that led there.-dataize :: Expression -> DataizeContext -> IO (Outcome, [Rewritten])-dataize universe ctx@DataizeContext{..} = do+dataize :: Expression -> ReduceContext -> IO (Outcome, [Rewritten])+dataize universe ctx@ReduceContext{..} = do   expr <- locatedExpression _locator universe   -- Dataization starts from the empty state; the final state is not yet   -- consumed by any caller, so it is discarded here.@@ -465,12 +62,12 @@     Right ((bytes, seq), _state) -> pure (Dataized bytes, reverse seq)     Left (StuckAt _ seq) | _partial -> pure (Residual (fst (NE.head seq)), reverse (NE.toList seq))     Left (OutOfStepsAt _ seq) | _partial -> pure (Residual (fst (NE.head seq)), reverse (NE.toList seq))-    Left failure -> throwIO (failure :: DataizeException)+    Left failure -> throwIO (failure :: ReduceException)  -- The Dataization function 𝔻 retrieves bytes from an expression. It is partial -- and ternary, 𝔻(n, e, s): besides the term 'n' it takes the universe 'e' ('univ'), -- which it forwards to 𝕄, and the mutable state 's', returning the bytes together--- with the new state. Its rules come from 'dataization.yaml': 'delta' yields the+-- with the new state. Its rules come from 'resources/dataization': 'delta' yields the -- asset bytes and 'none' (a formation with no Δ/λ/φ) has nothing to dataize, so -- it dataizes ⊥. The terminator ⊥ signals an error and lies outside 𝔻's domain, -- so it matches no clause (there is no 'end' rule mapping it to empty bytes) and@@ -488,7 +85,7 @@ -- The conclusion bytes 'dresult' are produced by a trailing 'dataize' premise; -- when its argument is bound by a 'morph' or 'normalize' premise, that step -- joins the spine, otherwise the premise is an isolated side-computation.-dataize' :: Dataizable -> Expression -> State -> DataizeContext -> IO (Dataized, State)+dataize' :: Dataizable -> Expression -> State -> ReduceContext -> IO (Dataized, State) dataize' (expr, seq) univ state caller = do   ctx <- deeper caller   parking seq $ do@@ -505,7 +102,7 @@     unmatched :: Expression -> String     unmatched ExTermination = "dataization reached the terminator ⊥, which signals an error and cannot be dataized"     unmatched _ = "no dataization rule matched"-    firstMatch :: DataizeContext -> [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst))+    firstMatch :: ReduceContext -> [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst))     firstMatch _ [] = pure Nothing     firstMatch ctx (rule : rest) = do       substs <- matchExpressionWithRule' (matchExpression' rule.ematch univ) expr (asRule rule) (RuleContext (execBuildTerm univ ctx))@@ -514,7 +111,7 @@         [] -> firstMatch ctx rest     asRule :: Y.DataizeRule -> Y.Rule     asRule rule = Y.Rule rule.name Nothing Nothing rule.match ExRoot rule.when Nothing Nothing-    reduce :: DataizeContext -> Y.DataizeRule -> Subst -> IO (Dataized, State)+    reduce :: ReduceContext -> Y.DataizeRule -> Subst -> IO (Dataized, State)     reduce ctx rule subst = case bytesProducer rule.dresult rule.premises of       Nothing -> do         (final, state') <- sides ctx rule.premises subst@@ -552,7 +149,7 @@           seq' <- leadsTo seq (labelOr (verb concl.operation) side) built ctx           dataize' (built, seq') univ state' ctx       Just _ -> throwIO (userError (printf "dataization rule '%s' must conclude with a 'dataize' premise" rule.name))-    sides :: DataizeContext -> [Y.Premise] -> Subst -> IO (Subst, State)+    sides :: ReduceContext -> [Y.Premise] -> Subst -> IO (Subst, State)     sides ctx premises subst = foldM (sidePremise univ ctx) (subst, state) premises     -- A spliced dataization step is labelled by its first side-computation —     -- 'box' by its 'contextualize', 'fire' by its 'evaluate'; with none it is blank.@@ -565,118 +162,12 @@     labelOr _ premises@(_ : _) = labelOf premises     labelOr fallback [] = fallback --- The premise binding the given expression meta, if any. The conclusion of a--- morphing rule and the argument of a continuation premise are looked up here to--- find the premise that produces them.-producer :: Expression -> [Y.Premise] -> Maybe Y.Premise-producer (ExMeta name) = find (\premise -> premise.result == name)-producer _ = const Nothing- -- The premise binding the given bytes meta, if any — the dataization analogue of -- 'producer' for a rule's bytes conclusion. bytesProducer :: Bytes -> [Y.Premise] -> Maybe Y.Premise bytesProducer (BtMeta name) = find (\premise -> premise.result == name) bytesProducer _ = const Nothing --- The premises whose result meta is not bound by any of the given ones — the--- side-computations left once the spine premises are removed.-excluding :: [Y.Premise] -> [Y.Premise] -> [Y.Premise]-excluding premises removed = filter (\premise -> premise.result `notElem` map (.result) removed) premises---- Evaluate one side-computation premise — a 'morph', 'evaluate' or 'contextualize'--- of an earlier term — in isolation, binding its result meta. These never splice--- steps into the trace: 'morph' and 'evaluate' reduce on a fresh chain and discard--- it, 'contextualize' is pure. The state is threaded through: 'evaluate' (the--- 𝔼 of the 'ml' and 'fire' rules) takes the incoming state 𝑠1 and yields a--- new one 𝑠2, 'morph' propagates whatever its sub-reduction produced, and every--- other operation leaves the state untouched.-sidePremise :: Expression -> DataizeContext -> (Subst, State) -> Y.Premise -> IO (Subst, State)-sidePremise univ ctx (subst, state) premise = do-  (term, state') <- runOperation-  case combine (substSingle premise.result (metaValue term)) subst of-    Just subst' -> pure (subst', state')-    Nothing -> throwIO (userError (printf "premise meta '%s' clashes with an existing binding" (T.unpack premise.result)))-  where-    -- The 𝔼 ('evaluate') and 𝕄 ('morph') operations can change the state, so they-    -- go through their state-aware builders; every other operation is stateless-    -- and the incoming state is returned unchanged.-    runOperation :: IO (Term, State)-    runOperation = case premise.operation of-      Y.OpEvaluate expr universe -> _evaluate ctx state [ArgExpression expr, ArgExpression universe] subst-      Y.OpMorph expr -> _morph univ ctx state [ArgExpression expr] subst-      operation -> do-        term <- execBuildTerm univ ctx (verb operation) (verbArgs operation) subst-        pure (term, state)-    metaValue :: Term -> MetaValue-    metaValue (TeExpression value) = MvExpression value-    metaValue (TeAttribute value) = MvAttribute value-    metaValue (TeBytes value) = MvBytes value-    metaValue (TeBindings value) = MvBindings value---- The build-term function name backing a premise operation.-verb :: Y.Operation -> String-verb (Y.OpMorph _) = "morph"-verb (Y.OpNormalize _) = "normalize"-verb (Y.OpEvaluate _ _) = "evaluate"-verb (Y.OpContextualize _ _) = "contextualize"-verb (Y.OpDataize _) = "dataize"---- The build-term arguments backing a premise operation.-verbArgs :: Y.Operation -> [ExtraArgument]-verbArgs (Y.OpMorph expr) = [ArgExpression expr]-verbArgs (Y.OpNormalize expr) = [ArgExpression expr]-verbArgs (Y.OpEvaluate expr universe) = [ArgExpression expr, ArgExpression universe]-verbArgs (Y.OpContextualize expr context) = [ArgExpression expr, ArgExpression context]-verbArgs (Y.OpDataize expr) = [ArgExpression expr]--leadsTo :: NonEmpty Rewritten -> String -> Expression -> DataizeContext -> IO (NonEmpty Rewritten)-leadsTo ((current, _) :| rest) rule expr DataizeContext{..} = do-  updated <- withLocatedExpression _locator expr current-  pure ((updated, Nothing) :| (current, Just rule) : rest)---- Reduce 'expr' to its normal form through the normalization rewriter, embedding--- it at '_locator' into the working expression taken from the head of the step--- chain so the rewriter sees the surrounding context. Splices the individual--- steps (alpha, copy, dot, …) into the chain and returns the normalized--- expression together with the extended sequence.-normalized :: Expression -> NonEmpty Rewritten -> DataizeContext -> IO (Expression, NonEmpty Rewritten)-normalized expr seq ctx@DataizeContext{..} = do-  whole <- withLocatedExpression _locator expr (fst (NE.head seq))-  (rewrittens, _) <- rewrite whole normalizationRules (rewriteContext ctx)-  let (rw :| rws) = NE.reverse rewrittens-      seq' = rw :| rws <> NE.tail seq-  expr' <- locatedExpression _locator (fst rw)-  pure (expr', seq')-  where-    -- Switch the dataization context to a rewriting context for normalization,-    -- disabling the must-checker and breakpoints.-    rewriteContext :: DataizeContext -> RewriteContext-    rewriteContext DataizeContext{..} =-      RewriteContext _locator _maxDepth _maxCycles _depthSensitive _buildTerm MtDisabled Nothing _saveStep---- Bind 'expr' to a synthetic attribute of the universe and reduce it to a--- normal form there, handing back the extended universe together with the--- locator that aims at the binding. This is the trick phino has always played--- to reduce a sub-expression that is not part of the program — an atom's--- operand, while the atoms still lived in the binary — and it is now the--- contract of the '--inside' option, so an atom script asking phino to reduce--- a part of the formation it was given does not have to splice it into the text--- of the universe by hand. 𝔻 and 𝕄 accept normal forms only and an expression--- handed in from outside is not necessarily one (a dispatch off a formation,--- '⟦ x ↦ 6, ρ ↦ 5 ⟧.x', is not), so it is normalized against the extended--- universe before either judgment sees it. The context comes back aimed at that--- binding, so the caller hands the extended universe and the context it got--- straight to 'dataize' or 'morph'.-insideUniverse :: Expression -> Expression -> DataizeContext -> IO (Expression, DataizeContext)-insideUniverse expr univ ctx@DataizeContext{_buildTerm = buildTerm} = case univ of-  ExFormation bds -> do-    (TeAttribute attr) <- buildTerm "random-tau" [] substEmpty-    let aiming = ctx{_locator = ExDispatch ExRoot attr}-        synthetic = ExFormation (BiTau attr expr : bds)-    (normal, _) <- normalized expr ((synthetic, Nothing) :| []) aiming-    pure (ExFormation (BiTau attr normal : bds), aiming)-  _ -> throwIO (userError "Can't reduce an expression inside a universe which is not a formation")- -- What phino answers a program that asks it to reduce a 𝜑-expression (see -- 'ReduceFunc' in 'Atoms'): the expression is bound to a synthetic attribute -- of the universe and dataized there, exactly the way the '--inside' option@@ -692,7 +183,7 @@ -- no way to ask: it had to splice the operand into the text of the universe -- and run a phino of its own on it (see #1160). The context is the one the -- fire descended with, so the step budget of the run bounds the nesting.-reduction :: Expression -> DataizeContext -> ReduceFunc+reduction :: Expression -> ReduceContext -> ReduceFunc reduction univ ctx expr = do   (universe, aiming) <- insideUniverse expr univ ctx   (outcome, _) <- dataize universe aiming@@ -701,81 +192,3 @@     reduced :: Expression -> Outcome -> IO Expression     reduced _ (Dataized bytes) = pure (ExFormation [BiDelta bytes])     reduced locator (Residual residue) = locatedExpression locator residue---- phino implements no λ function of its own. Which atoms exist is a property of--- the object model being dataized, not of the calculus, so they come from the--- '--atoms' registry and run as external scripts (see 'Atoms'). A name the--- registry does not carry has no λ function to fire at all, and 𝔼 gets stuck on--- it — the one behaviour left here. The script is handed the formation 'self'--- (its λ binding already removed, so it may dispatch on it) and the universe--- 'univ'; the state 𝑠 is not part of that contract yet, so it is threaded--- through untouched.-atom :: T.Text -> Expression -> Expression -> State -> DataizeContext -> IO (Expression, State)-atom func self univ state ctx = case registeredAtom ctx._atoms func of-  Nothing -> throwIO (Stuck func)-  Just registered -> do-    raw <- fireAtom func registered self univ (reduction univ ctx)-    pure (raw, state)---- Augment the injected, context-free term builder with the dataization and--- morphing operations that need the universe: 'evaluate' applies an atom and--- 'morph' morphs a sub-expression. 𝔼 ('evaluate') takes the universe as an--- explicit second expression argument, while 𝕄 ('morph') is handed the threaded--- 'univ'. Every other function is delegated unchanged. This is the matcher's--- condition path (guards in 'when'/'having'), which has no state to thread, so 𝔼--- and 𝕄 run here on a fresh, empty state whose result is discarded; the--- state-threading callers in 'sidePremise' use '_evaluate' and '_morph' directly.-execBuildTerm :: Expression -> DataizeContext -> BuildTermFunc-execBuildTerm _ ctx "evaluate" = \args subst -> fst <$> _evaluate ctx emptyState args subst-execBuildTerm univ ctx "morph" = \args subst -> fst <$> _morph univ ctx emptyState args subst-execBuildTerm _ ctx func = _buildTerm ctx func---- The Evaluation function 𝔼(b, e, s): it fires the λ atom of a formation 'b'--- against the global universe 'e', under the incoming state 𝑠, normalizes the--- atom's raw result 𝒩(e₁) = n, and returns that normal form together with the--- new state. Normalizing here makes 𝔼's codomain 𝓝 (as its type demands), so--- callers ('fire', 'ml') need no follow-up 'normalize' premise. The universe is--- passed explicitly as the second argument (rather than threaded behind the--- scenes), matching how the morphing 𝕄 and dataization 𝔻 functions carry it.--- Every firing is reported to '_saveEval', which the '--evaluations' option--- turns into one record per line. The reported result is the normal form 𝔼--- returns, never the atom's raw answer, so the protocol and the caller see the--- same term. Firings are reported in the order they complete, so the atom of a--- head reduced by 'ml' is reported before the one dispatched on its result. A--- firing that gets stuck is reported too, with no result, when the run is a--- partial evaluation rather than a failure ('_partial'): the site is what the--- caller wants to learn then. The report is made before the signal goes on to--- the spine, where 'parking' attaches the derivation to it.-_evaluate :: DataizeContext -> State -> BuildTermMethodS-_evaluate ctx state [ArgExpression expr, ArgExpression universe] subst = do-  form <- buildExpressionThrows expr subst-  univ <- buildExpressionThrows universe subst-  case form of-    ExFormation bds -> case lambda bds of-      Just (func, args) -> do-        (raw, state') <- atom func args univ state ctx `catch` parked func args-        (normal, _) <- normalized raw ((univ, Nothing) :| []) ctx-        ctx._saveEval (Evaluation func args (Just normal))-        pure (TeExpression normal, state')-      Nothing -> throwIO (userError "Function evaluate() expects a formation with a λ binding")-    _ -> throwIO (userError "Function evaluate() expects a formation")-  where-    parked :: T.Text -> Expression -> DataizeException -> IO a-    parked func args failure@(Stuck _) = do-      when ctx._partial (ctx._saveEval (Evaluation func args Nothing))-      throwIO failure-    parked _ _ failure = throwIO failure-_evaluate _ _ _ _ = throwIO (userError "Function evaluate() requires exactly 2 expression arguments")---- The Morphing function 𝕄 exposed as a build-term function so a rule can morph--- a sub-expression in its 'where' (the 'md' and 'ma' rules morph--- the head before re-attaching it). The step chain is discarded: the producing--- rule splices the surrounding normalization steps itself, and a stuck atom met--- on the way leaves without it (see 'unparked'). The state is threaded through--- and the new state returned alongside the morphed term.-_morph :: Expression -> DataizeContext -> State -> BuildTermMethodS-_morph univ ctx state [ArgExpression expr] subst = unparked $ do-  built <- buildExpressionThrows expr subst-  ((morphed, _), state') <- morph' (built, (univ, Nothing) :| []) univ state ctx-  pure (TeExpression morphed, state')-_morph _ _ _ _ _ = throwIO (userError "Function morph() requires exactly 1 expression argument")

@@ -4,7 +4,7 @@ -- The main goal of this module is breaking cyclic dependency: -- Dataize -> Functions -> Rewriter -> Dataize -- Here we provide custom type BuildTermFunc and add it to--- RewriteContext and DataizeContext. Now Dataize and Rewrite depends+-- RewriteContext and ReduceContext. Now Dataize and Rewrite depends -- only on Term module. This allows us to use Rewriter and Dataize in -- Functions module because Rewriter does not depend on Functions anymore. module Deps where

@@ -0,0 +1,638 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE DuplicateRecordFields #-}+{-# LANGUAGE OverloadedRecordDot #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}+{-# OPTIONS_GHC -Wno-unused-record-wildcards #-}++-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++-- The Morphing function 𝕄 and the machinery every reduction of the calculus is+-- threaded with: the context, the step budget, the signals a stuck run raises+-- and the plumbing that reads a rule's premises. 𝔻 lives in 'Dataize', which+-- imports this module; the one edge pointing back — an atom asking phino to+-- reduce an operand, which is a dataization — is injected as '_reduce' rather+-- than imported (see 'ReductionFunc').+module Morph (ReduceContext (..), ReduceException (..), ReductionFunc, Morphed, Steps (..), deeper, emptyState, excluding, execBuildTerm, insideUniverse, leadsTo, morph, morph', normalized, parking, producer, sidePremise, verb) where++import AST+import Atoms (ReduceFunc, Registry, fireAtom, registeredAtom)+import Builder (buildExpressionThrows, contextualize)+import Control.Exception (Exception, catch, throwIO, try)+import Control.Monad (foldM, when)+import Data.List (find, partition)+import Data.List.NonEmpty (NonEmpty (..))+import qualified Data.List.NonEmpty as NE+import Data.Maybe (fromMaybe)+import qualified Data.Text as T+import Deps (BuildTermFunc, BuildTermMethodS, Evaluation (..), SaveEvalFunc, SaveStepFunc, State, Term (..))+import Locator (locatedExpression, withLocatedExpression)+import Matcher (MetaValue (..), Subst (..), combine, matchExpression', substEmpty, substSingle)+import Must (Must (..))+import Random (shuffle)+import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite)+import Rule (RuleContext (RuleContext), matchExpressionWithRule')+import Text.Printf (printf)+import Yaml (ExtraArgument (..), normalizationRules)+import qualified Yaml as Y++-- A term together with the derivation that reached it: what one frame of a+-- judgment's spine is handed and hands on.+type Morphed = (Expression, NonEmpty Rewritten)++-- How the morphing side reaches back to the dataization one. An atom may ask+-- phino to reduce an operand of its own (see 'ReduceFunc' in 'Atoms'), and the+-- answer is a whole run of 𝔻 — a judgment 𝕄 has no business knowing about,+-- since 'Dataize' imports 'Morph' and not the other way round. The reduction is+-- therefore injected into the context, the way 'Deps' injects '_buildTerm', and+-- 'Dataize' supplies its own 'reduction' for it.+type ReductionFunc = Expression -> ReduceContext -> ReduceFunc++-- The initial, empty state a run of 𝕄 or 𝔻 starts from. The 'State' type itself+-- lives in 'Deps' next to 'BuildTermMethod'.+emptyState :: State+emptyState = ""++-- How many steps of the 𝕄/𝔻 recursion one branch of a derivation may take+-- ('_limit', the '--max-steps' option) and how many the branch reaching this+-- point has already taken ('_spent'). 𝕄 and 𝔻 recurse into each other, into the+-- premises of their own rules and into the atoms they fire, so a budget local to+-- one of those chains is reset by the next nested call and bounds nothing (see+-- #1052). This one rides in the context that every such path — the spine, the+-- side-premises, '_dataize' and '_morph' — already carries, so a nested call+-- inherits the count of the call that made it. It bounds depth, not total work:+-- a premise passes its count down but not back, so siblings each descend from+-- the same '_spent'. Bounding every branch is enough to terminate, since a rule+-- has finitely many premises.+data Steps = Steps+  { _limit :: Int+  , _spent :: Int+  }++-- The context every reduction of the calculus is threaded with — 𝕄 here and 𝔻 in+-- 'Dataize' — carrying the configuration plus the step budget spent so far. Nothing global is fixed here: the universe (the second argument 'e' of+-- 𝕄(n, e, s) and 𝔻(n, e, s)) is a plain expression threaded as an argument to+-- 'dataize'', 'morph'' and on to the atoms, and the state 's' is threaded the same+-- way (see 'State'). The working expression needed for normalization is taken+-- from the head of the step chain, so no separate wrapper type is threaded+-- around.+data ReduceContext = ReduceContext+  { _locator :: Expression+  , _maxDepth :: Int+  , _maxCycles :: Int+  , _steps :: Steps+  , _depthSensitive :: Bool+  , _shuffle :: Bool+  , _partial :: Bool+  , _deep :: Bool+  , _atoms :: Registry+  , _buildTerm :: BuildTermFunc+  , _reduce :: ReductionFunc+  , _saveStep :: SaveStepFunc+  , _saveEval :: SaveEvalFunc+  }++data ReduceException+  = OutOfSteps Int+  | -- An atom could not fire: the '--atoms' registry carries no λ function of+    -- that name, so there is nothing to run. The name is that of the atom 𝔼+    -- actually failed on, which for a chain of dispatches is the innermost one,+    -- since 'ml' reduces a head before the atom above it fires.+    Stuck T.Text+  | -- A 'Stuck' caught by a frame of the 𝕄/𝔻 spine, together with the+    -- derivation that frame had reached (see 'parking'). The head of the chain+    -- is the working expression with the stuck application left intact and+    -- everything reduced before it already in place: the residual program that+    -- '_partial' turns into the 'Residual' outcome.+    StuckAt T.Text (NonEmpty Rewritten)+  | -- An 'OutOfSteps' caught by a spine frame, carrying that frame's derivation+    -- just like 'StuckAt': a term that never reduces is a stuck site too, so+    -- '_partial' parks it and hands back the residual instead of failing hard+    -- (#1078)+    OutOfStepsAt Int (NonEmpty Rewritten)+  deriving anyclass (Exception)++instance Show ReduceException where+  show (OutOfSteps limit) =+    printf "Dataization did not finish before reaching the limit of steps: --max-steps=%d" limit+  show (OutOfStepsAt limit _) = show (OutOfSteps limit)+  show (Stuck func) = printf "Atom '%s' does not exist" (T.unpack func)+  show (StuckAt func _) = show (Stuck func)++-- Charge one step of the 𝕄/𝔻 recursion to the budget, refusing to descend once+-- it is gone. '--max-cycles' and '--max-depth' bound only the normalization run+-- inside a single step, so before this the recursion itself was unbounded and a+-- term that never reduces to bytes kept 𝕄 and 𝔻 calling each other forever+-- (#1052). Rewriting hands back whatever it has reached when it runs out of+-- cycles; 𝔻 has no partial answer to give, so an exhausted budget always throws,+-- with or without '--depth-sensitive'.+deeper :: ReduceContext -> IO ReduceContext+deeper ctx@ReduceContext{_steps = Steps limit spent}+  | spent >= limit = throwIO (OutOfSteps limit)+  | otherwise = pure ctx{_steps = Steps limit (spent + 1)}++-- Split the λ binding off a formation for the LAMBDA morphing rule: the name of+-- the atom to fire and the formation it fires against, the λ binding removed —+-- the two things 𝔼 reports besides the result. A formation with no λ binding,+-- or with more than one, has nothing to fire.+lambda :: [Binding] -> Maybe (T.Text, Expression)+lambda bds = case partition isLambda bds of+  ([BiLambda (Function func)], rest) -> Just (func, ExFormation rest)+  _ -> Nothing+  where+    isLambda :: Binding -> Bool+    isLambda (BiLambda _) = True+    isLambda _ = False++-- The same as 'lambda', but only for a formation that is saturated: one with+-- every binding of it filled (see 'filled'). A void is an argument the program+-- has not given yet, so such a formation is a method waiting to be applied+-- rather than an application waiting to be computed, and firing it would hand+-- the atom a ∅ where it expects a value. 𝔻 needs no such guard, since it+-- fires only what dataization demands and nothing demands a method; the deep+-- walk meets every one a program declares — the method table of the object+-- model above all — so it asks first (see 'deepened').+saturated :: [Binding] -> Maybe (T.Text, Expression)+saturated bds = case lambda bds of+  Just (func, ExFormation rest) | all filled rest -> Just (func, ExFormation rest)+  _ -> Nothing++-- Whether a binding hands the formation something to work with. A void does+-- not: it names an argument the program has still to supply. Neither does ⊥:+-- the deep walk reduces a body in the scope of the formation around it, and a+-- formation standing unapplied still holds ρ ↦ ∅, so a ξ.ρ in that body comes+-- back as ⊥ rather than as the object the next dispatch supplies (#1196).+filled :: Binding -> Bool+filled (BiVoid _) = False+filled (BiTau _ ExTermination) = False+filled _ = True++-- Run one frame of the 𝕄/𝔻 spine, attaching its derivation to a stuck atom or+-- an exhausted budget escaping it. 'Stuck' is raised deep inside an atom, which+-- knows nothing about the chain, so the innermost spine frame it reaches is the+-- one to record where the derivation stopped: the head of that frame's chain is+-- the working expression with the stuck application intact and everything+-- reduced before it already in place. The same holds for 'OutOfSteps': a term+-- cycling through the universe is no more a failure of the chain than a missing+-- atom is, and under '_partial' it deserves the same parked residual (#1078).+-- Outer frames see the '…At' signals and let them pass, since their chains are+-- prefixes of that one; a side-computation running on a chain of its own strips+-- the chain off again (see 'unparked') before the signal reaches the spine.+parking :: NonEmpty Rewritten -> IO a -> IO a+parking seq action = action `catch` rethrow+  where+    rethrow :: ReduceException -> IO a+    rethrow (Stuck func) = throwIO (StuckAt func seq)+    rethrow (OutOfSteps limit) = throwIO (OutOfStepsAt limit seq)+    rethrow failure = throwIO failure++-- Strip the derivation off a stuck atom escaping a side-computation that ran+-- on a chain of its own — an atom dataizing its input through '_dataize', or a+-- 'morph' premise through '_morph'. That chain is not the spine's, so it is+-- dropped and the spine frame around the side-computation attaches its own+-- (see 'parking').+unparked :: IO a -> IO a+unparked action = action `catch` rethrow+  where+    rethrow :: ReduceException -> IO a+    rethrow (StuckAt func _) = throwIO (Stuck func)+    rethrow (OutOfStepsAt limit _) = throwIO (OutOfSteps limit)+    rethrow failure = throwIO failure++-- The Morphing function 𝕄 maps normal forms to formations. It is ternary,+-- 𝕄(n, e, s): besides the term 'n' it takes the universe 'e' ('univ') — a plain+-- expression — and the mutable state 's', returning the morphed term together+-- with the new state. The universe is matched against the rule's 'e-match'+-- pattern (usually the '𝑒' meta, which binds 'e' so the 'universe' rule substitutes+-- it, but a rule may pin it to a literal such as 'mg' matching Φ). Its rules+-- come from 'resources/morphing': the first matching rule's premises are evaluated and+-- its conclusion 'nresult' is built, always forwarding the same universe. The+-- clauses are disjoint (see #856, #860), so their declaration order must not be+-- load-bearing; when '_shuffle' is on (the '--shuffle' flag) the rules are+-- shuffled before the 'firstMatch' walk to exercise that invariant — mirroring+-- normalization's "apply until they stop matching". A genuinely order-independent+-- step stays deterministic; a hidden overlap surfaces as a nondeterministic+-- failure rather than staying silently green.+-- The 'morph' premise that produces the conclusion is the spine: when+-- its argument comes from a 'normalize' premise, the rewriter runs over that+-- argument and its individual steps (alpha, copy, dot, …) are spliced into the+-- chain before morphing continues. Every other premise is a side-computation+-- evaluated in isolation by 'sidePremise', its own steps discarded.+morph' :: Morphed -> Expression -> State -> ReduceContext -> IO (Morphed, State)+morph' (expr, seq) univ state caller = do+  ctx <- deeper caller+  parking seq $ do+    rules <- if ctx._shuffle then shuffle Y.morphingRules else pure Y.morphingRules+    matched <- firstMatch ctx rules+    case matched of+      Just (rule, subst) -> reduce ctx rule subst+      Nothing -> throwIO (userError "no morphing rule matched")+  where+    firstMatch :: ReduceContext -> [Y.MorphRule] -> IO (Maybe (Y.MorphRule, Subst))+    firstMatch _ [] = pure Nothing+    firstMatch ctx (rule : rest) = do+      substs <- matchExpressionWithRule' (matchExpression' rule.ematch univ) expr (asRule rule) (RuleContext (execBuildTerm univ ctx))+      case substs of+        (subst : _) -> pure (Just (rule, subst))+        [] -> firstMatch ctx rest+    -- Match the conclusion term and check the guard; premises are no longer the+    -- matcher's business, so 'where'/'having' stay empty and the guard lives in+    -- 'when'. Every morphing guard reads only meta-variables bound by 'match'+    -- and 'e-match', so it holds before any premise runs.+    asRule :: Y.MorphRule -> Y.Rule+    asRule rule = Y.Rule rule.name Nothing Nothing rule.match ExRoot rule.when Nothing Nothing+    -- Evaluate the rule's premises and build its conclusion. A literal+    -- conclusion is terminal. Otherwise the conclusion meta is produced by a+    -- trailing 'morph' premise (the spine); if that premise's argument is itself+    -- bound by a 'normalize' premise, the normalization joins the spine and its+    -- steps splice in before morphing continues.+    reduce :: ReduceContext -> Y.MorphRule -> Subst -> IO (Morphed, State)+    reduce ctx rule subst = case producer rule.nresult rule.premises of+      Nothing -> do+        (final, state') <- sides ctx rule.premises subst+        built <- buildExpressionThrows rule.nresult final+        seq' <- leadsTo seq rule.name built ctx+        pure ((built, seq'), state')+      Just concl@(Y.Premise _ (Y.OpMorph arg)) -> case producer arg rule.premises of+        Just normal@(Y.Premise _ (Y.OpNormalize inner)) -> do+          (final, state') <- sides ctx (rule.premises `excluding` [concl, normal]) subst+          built <- buildExpressionThrows inner final+          labelled <- leadsTo seq rule.name built ctx+          (normal', seq') <- normalized built labelled ctx+          morph' (normal', seq') univ state' ctx+        _ -> do+          (final, state') <- sides ctx (rule.premises `excluding` [concl]) subst+          built <- buildExpressionThrows arg final+          seq' <- leadsTo seq rule.name built ctx+          morph' (built, seq') univ state' ctx+      Just _ -> throwIO (userError (printf "morphing rule '%s' must conclude with a 'morph' premise" rule.name))+    sides :: ReduceContext -> [Y.Premise] -> Subst -> IO (Subst, State)+    sides ctx premises subst = foldM (sidePremise univ ctx) (subst, state) premises++-- Morph the expression located at '_locator' — 𝕄 asked on its own, the way+-- 'dataize' asks 𝔻. The whole input expression is itself the universe Φ (the 'e'+-- argument) threaded through 𝕄, so it is passed both as the located target and+-- as the universe; the default locator Q therefore morphs the top formation,+-- which 'mf' hands back unchanged, and '_locator' is how one aims 𝕄 at a+-- subterm. Unlike 𝔻, 𝕄 is total: it stops at the first formation it reaches+-- ('mf') and never demands bytes, and where no formation is reachable it answers+-- with the terminator ⊥ ('dead', 'xi', 'mg', 'mad', 'maad') rather than failing.+-- Only the atoms 'ml' fires can still get stuck, and '_partial' parks them just+-- as it does under 𝔻: the answer is then the residual subterm the spine had+-- reached, taken from '_locator' of its working expression. Stopping at the+-- first formation leaves everything that formation holds as it was written,+-- which is what '_deep' walks into before the answer is handed back (see+-- 'deepened').+morph :: Expression -> ReduceContext -> IO (Expression, [Rewritten])+morph universe ctx@ReduceContext{..} = do+  expr <- locatedExpression _locator universe+  result <- try (morph' (expr, (universe, Nothing) :| []) universe emptyState ctx)+  case result of+    Right ((morphed, seq), state) -> walked morphed seq state+    Left (StuckAt _ seq) | _partial -> do+      residue <- locatedExpression _locator (fst (NE.head seq))+      walked residue seq emptyState+    Left (OutOfStepsAt _ seq) | _partial -> do+      residue <- locatedExpression _locator (fst (NE.head seq))+      walked residue seq emptyState+    Left failure -> throwIO (failure :: ReduceException)+  where+    -- The answer 𝕄 reached, walked by '_deep' before it is handed back (see+    -- 'deepened'), and the chain that led to both. The walk joins the chain as+    -- one step named 'deep', so '--sequence' ends on the term the command+    -- prints. Morphing starts from the empty state and the state the walk ends+    -- on goes the way 𝕄's own goes: no caller consumes it yet.+    walked :: Expression -> NonEmpty Rewritten -> State -> IO (Expression, [Rewritten])+    walked morphed seq state+      | not _deep = pure (morphed, reverse (NE.toList seq))+      | otherwise = do+          (deep, _) <- deepened morphed universe state ctx+          seq' <- leadsTo seq "deep" deep ctx+          pure (deep, reverse (NE.toList seq'))++-- Walk what 𝕄 answered with, entering everything it left as it was written —+-- the mechanism behind '--deep' ('_deep'). 𝕄 navigates a term to the first+-- formation it reaches and 'mf' hands that formation back with its bindings+-- untouched, since firing a bare λ is 𝔻's business; 𝔻 in turn follows the one+-- path dataization demands and ends in bytes. A part of a program that nothing+-- demands — the argument of an atom that cannot fire, for one — is therefore+-- reduced by neither, and the object structure is lost to the one that does+-- reduce it (#1124). This walk demands nothing either. It asks 𝕄 about every+-- sub-expression and, where 𝕄 lands on a formation whose λ the registry+-- serves, fires it and asks 𝕄 about the answer again (see 'fired'). A+-- sub-expression on whose way an atom fired is replaced by the answer of the+-- last firing; where none fired it stays as it was written and only its own+-- parts are walked, so the calls the registry does not serve keep their names+-- and what comes back is still the same program, reduced as far as the+-- registry allows. Every entry is charged to the '--max-steps' budget, which+-- is what bounds the walk.+deepened :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)+deepened expr univ = go Nothing ExXi expr+  where+    -- A term as it was written, together with what its free ξ stands for: the+    -- formation the walk entered it from, without the binding it came from,+    -- exactly the context the 'dot' rule hands a dispatched body. At the top+    -- there is no such formation, so ξ stands for itself and contextualization+    -- leaves the term alone.+    go :: Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)+    go dispatched context term state' caller = do+      ctx' <- deeper caller+      (walked, walkedState) <- parts context term state' caller+      answer <- fired dispatched (contextualize walked context) univ walkedState ctx'+      maybe (pure (walked, walkedState)) pure answer+    -- The parts of a term nothing fired on, walked one by one and put back+    -- where they were, so the term keeps the shape it was written in.+    parts :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)+    parts _ (ExFormation bds) state' caller = do+      (entered, state'') <- bindings bds bds state' caller+      pure (ExFormation entered, state'')+    parts context (ExDispatch target attr) state' caller = do+      (entered, state'') <- go (Just attr) context target state' caller+      pure (ExDispatch entered attr, state'')+    parts context (ExApplication target arg) state' caller = do+      (entered, state'') <- go Nothing context target state' caller+      (applied, state''') <- argument context arg state'' caller+      pure (ExApplication entered applied, state''')+    parts _ term state' _ = pure (term, state')+    -- Walk the bindings of a formation left to right, threading the state+    -- through them. Only what the formation itself holds is entered: ρ names+    -- the object around it rather than one inside it, and a void, Δ or λ+    -- binding carries no term to walk at all.+    bindings :: [Binding] -> [Binding] -> State -> ReduceContext -> IO ([Binding], State)+    bindings _ [] state' _ = pure ([], state')+    bindings whole (BiTau attr body : rest) state' caller+      | attr /= AtRho = do+          (entered, state'') <- go Nothing (scope attr whole) body state' caller+          (others, state''') <- bindings whole rest state'' caller+          pure (BiTau attr entered : others, state''')+    bindings whole (bd : rest) state' caller = do+      (others, state'') <- bindings whole rest state' caller+      pure (bd : others, state'')+    -- The context a binding's body is entered in: the formation without that+    -- binding, the very context 'dot' contextualizes a dispatched body in, so+    -- a body reaching back at itself through ξ collapses instead of looping.+    scope :: Attribute -> [Binding] -> Expression+    scope attr bds = ExFormation (filter (not . named) bds)+      where+        named :: Binding -> Bool+        named (BiTau attr' _) = attr' == attr+        named _ = False+    -- Both sides of an application stand in the same context: the term it+    -- applies is walked by the caller and the argument it binds is walked here.+    argument :: Expression -> Argument -> State -> ReduceContext -> IO (Argument, State)+    argument context (ArTau attr arg) state' caller = do+      (entered, state'') <- go Nothing context arg state' caller+      pure (ArTau attr entered, state'')+    argument context (ArAlpha alpha arg) state' caller = do+      (entered, state'') <- go Nothing context arg state' caller+      pure (ArAlpha alpha entered, state'')++-- Ask 𝕄 about a term and fire the λ of the formation it reaches, as long as+-- the registry serves it, asking 𝕄 about every answer again: what comes back+-- is the answer of the last firing, or nothing at all where no atom fired. This+-- is the firing 'ml' makes without the dispatch that makes 'ml' make it — the+-- one 𝕄 leaves to 𝔻 — except in what it hands back: the atom's raw answer, not+-- the normal form 𝔼 makes of it, since the deep walk stands that answer back+-- into the program, where a normal form would spell the whole object out in+-- place of the name the program called it by. A λ the registry does not carry+-- is left alone rather than fired and got stuck on, so what phino cannot+-- compute stays as it was written with or without '_partial'; an atom that+-- cannot fire deeper on the spine still fails the run, exactly as it does+-- under 𝕄 alone, and '_partial' parks it. A formation still waiting for its+-- arguments is left alone too (see 'saturated'). A term standing as the target+-- of a dispatch is where 'ml' has its say: the λ is fired only where the+-- dispatched attribute is none of the formation's own (see 'demanded').+fired :: Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Maybe (Expression, State))+fired dispatched term univ state caller = do+  ctx <- deeper caller+  morphed <- try (reduced ctx)+  case morphed of+    Right (ExFormation bds, state')+      | demanded bds -> maybe (pure Nothing) (evaluated ctx state') (saturated bds)+    Right _ -> pure Nothing+    Left failure -> parked failure+  where+    -- Whether the dispatch the term stands under demands the λ of the formation+    -- 𝕄 reached. 'ml' fires that λ only where the dispatched attribute is none+    -- of the formation's own, since 'dot' resolves the dispatch before 'ml' is+    -- ever reached, and a walk firing it first answers a formation the dispatch+    -- no longer fits (#1187). A term standing anywhere else is demanded by+    -- nothing and the walk fires what 'mf' left bare, as it always has.+    demanded :: [Binding] -> Bool+    demanded bds = not (any bound bds)+      where+        bound :: Binding -> Bool+        bound (BiTau attr _) = Just attr == dispatched+        bound _ = False+    -- 𝕄 takes normal forms only and a term taken from the program as it was+    -- written is not necessarily one, so it is normalized against the universe+    -- first, exactly as '--inside' normalizes what it is handed. Both chains+    -- are dropped: the walk is not the spine and reports one step of its own+    -- (see 'morph'), so a stuck atom leaves without a derivation ('unparked').+    reduced :: ReduceContext -> IO (Expression, State)+    reduced ctx = unparked $ do+      (normal, _) <- normalized term ((univ, Nothing) :| []) ctx+      ((morphed, _), state') <- morph' (normal, (univ, Nothing) :| []) univ state ctx+      pure (morphed, state')+    -- Fire the λ of the formation 𝕄 reached and go on from its answer, keeping+    -- the answer of the last firing. The firing is reported to '_saveEval' like+    -- every other one, with the term the caller is given, so the protocol and+    -- the program agree on what the atom answered.+    evaluated :: ReduceContext -> State -> (T.Text, Expression) -> IO (Maybe (Expression, State))+    evaluated ctx state' (func, self) = case registeredAtom ctx._atoms func of+      Nothing -> pure Nothing+      Just registered -> do+        answer <- fireAtom func registered self univ (ctx._reduce univ ctx)+        ctx._saveEval (Evaluation func self (Just answer))+        again <- fired dispatched answer univ state' ctx+        pure (Just (fromMaybe (answer, state') again))+    parked :: ReduceException -> IO (Maybe a)+    parked (Stuck _) | caller._partial = pure Nothing+    parked failure = throwIO failure++-- The premise binding the given expression meta, if any. The conclusion of a+-- morphing rule and the argument of a continuation premise are looked up here to+-- find the premise that produces them.+producer :: Expression -> [Y.Premise] -> Maybe Y.Premise+producer (ExMeta name) = find (\premise -> premise.result == name)+producer _ = const Nothing++-- The premises whose result meta is not bound by any of the given ones — the+-- side-computations left once the spine premises are removed.+excluding :: [Y.Premise] -> [Y.Premise] -> [Y.Premise]+excluding premises removed = filter (\premise -> premise.result `notElem` map (.result) removed) premises++-- Evaluate one side-computation premise — a 'morph', 'evaluate' or 'contextualize'+-- of an earlier term — in isolation, binding its result meta. These never splice+-- steps into the trace: 'morph' and 'evaluate' reduce on a fresh chain and discard+-- it, 'contextualize' is pure. The state is threaded through: 'evaluate' (the+-- 𝔼 of the 'ml' and 'fire' rules) takes the incoming state 𝑠1 and yields a+-- new one 𝑠2, 'morph' propagates whatever its sub-reduction produced, and every+-- other operation leaves the state untouched.+sidePremise :: Expression -> ReduceContext -> (Subst, State) -> Y.Premise -> IO (Subst, State)+sidePremise univ ctx (subst, state) premise = do+  (term, state') <- runOperation+  case combine (substSingle premise.result (metaValue term)) subst of+    Just subst' -> pure (subst', state')+    Nothing -> throwIO (userError (printf "premise meta '%s' clashes with an existing binding" (T.unpack premise.result)))+  where+    -- The 𝔼 ('evaluate') and 𝕄 ('morph') operations can change the state, so they+    -- go through their state-aware builders; every other operation is stateless+    -- and the incoming state is returned unchanged.+    runOperation :: IO (Term, State)+    runOperation = case premise.operation of+      Y.OpEvaluate expr universe -> _evaluate ctx state [ArgExpression expr, ArgExpression universe] subst+      Y.OpMorph expr -> _morph univ ctx state [ArgExpression expr] subst+      operation -> do+        term <- execBuildTerm univ ctx (verb operation) (verbArgs operation) subst+        pure (term, state)+    metaValue :: Term -> MetaValue+    metaValue (TeExpression value) = MvExpression value+    metaValue (TeAttribute value) = MvAttribute value+    metaValue (TeBytes value) = MvBytes value+    metaValue (TeBindings value) = MvBindings value++-- The build-term function name backing a premise operation.+verb :: Y.Operation -> String+verb (Y.OpMorph _) = "morph"+verb (Y.OpNormalize _) = "normalize"+verb (Y.OpEvaluate _ _) = "evaluate"+verb (Y.OpContextualize _ _) = "contextualize"+verb (Y.OpDataize _) = "dataize"++-- The build-term arguments backing a premise operation.+verbArgs :: Y.Operation -> [ExtraArgument]+verbArgs (Y.OpMorph expr) = [ArgExpression expr]+verbArgs (Y.OpNormalize expr) = [ArgExpression expr]+verbArgs (Y.OpEvaluate expr universe) = [ArgExpression expr, ArgExpression universe]+verbArgs (Y.OpContextualize expr context) = [ArgExpression expr, ArgExpression context]+verbArgs (Y.OpDataize expr) = [ArgExpression expr]++leadsTo :: NonEmpty Rewritten -> String -> Expression -> ReduceContext -> IO (NonEmpty Rewritten)+leadsTo ((current, _) :| rest) rule expr ReduceContext{..} = do+  updated <- withLocatedExpression _locator expr current+  pure ((updated, Nothing) :| (current, Just rule) : rest)++-- Reduce 'expr' to its normal form through the normalization rewriter, embedding+-- it at '_locator' into the working expression taken from the head of the step+-- chain so the rewriter sees the surrounding context. Splices the individual+-- steps (alpha, copy, dot, …) into the chain and returns the normalized+-- expression together with the extended sequence.+normalized :: Expression -> NonEmpty Rewritten -> ReduceContext -> IO (Expression, NonEmpty Rewritten)+normalized expr seq ctx@ReduceContext{..} = do+  whole <- withLocatedExpression _locator expr (fst (NE.head seq))+  (rewrittens, _) <- rewrite whole normalizationRules (rewriteContext ctx)+  let (rw :| rws) = NE.reverse rewrittens+      seq' = rw :| rws <> NE.tail seq+  expr' <- locatedExpression _locator (fst rw)+  pure (expr', seq')+  where+    -- Switch the reduction context to a rewriting context for normalization,+    -- disabling the must-checker and breakpoints.+    rewriteContext :: ReduceContext -> RewriteContext+    rewriteContext ReduceContext{..} =+      RewriteContext _locator _maxDepth _maxCycles _depthSensitive _buildTerm MtDisabled Nothing _saveStep++-- Bind 'expr' to a synthetic attribute of the universe and reduce it to a+-- normal form there, handing back the extended universe together with the+-- locator that aims at the binding. This is the trick phino has always played+-- to reduce a sub-expression that is not part of the program — an atom's+-- operand, while the atoms still lived in the binary — and it is now the+-- contract of the '--inside' option, so an atom script asking phino to reduce+-- a part of the formation it was given does not have to splice it into the text+-- of the universe by hand. 𝔻 and 𝕄 accept normal forms only and an expression+-- handed in from outside is not necessarily one (a dispatch off a formation,+-- '⟦ x ↦ 6, ρ ↦ 5 ⟧.x', is not), so it is normalized against the extended+-- universe before either judgment sees it. The context comes back aimed at that+-- binding, so the caller hands the extended universe and the context it got+-- straight to 'dataize' or 'morph'.+insideUniverse :: Expression -> Expression -> ReduceContext -> IO (Expression, ReduceContext)+insideUniverse expr univ ctx@ReduceContext{_buildTerm = buildTerm} = case univ of+  ExFormation bds -> do+    (TeAttribute attr) <- buildTerm "random-tau" [] substEmpty+    let aiming = ctx{_locator = ExDispatch ExRoot attr}+        synthetic = ExFormation (BiTau attr expr : bds)+    (normal, _) <- normalized expr ((synthetic, Nothing) :| []) aiming+    pure (ExFormation (BiTau attr normal : bds), aiming)+  _ -> throwIO (userError "Can't reduce an expression inside a universe which is not a formation")++-- phino implements no λ function of its own. Which atoms exist is a property of+-- the object model being dataized, not of the calculus, so they come from the+-- '--atoms' registry and run as external scripts (see 'Atoms'). A name the+-- registry does not carry has no λ function to fire at all, and 𝔼 gets stuck on+-- it — the one behaviour left here. The script is handed the formation 'self'+-- (its λ binding already removed, so it may dispatch on it) and the universe+-- 'univ'; the state 𝑠 is not part of that contract yet, so it is threaded+-- through untouched.+atom :: T.Text -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)+atom func self univ state ctx = case registeredAtom ctx._atoms func of+  Nothing -> throwIO (Stuck func)+  Just registered -> do+    raw <- fireAtom func registered self univ (ctx._reduce univ ctx)+    pure (raw, state)++-- Augment the injected, context-free term builder with the dataization and+-- morphing operations that need the universe: 'evaluate' applies an atom and+-- 'morph' morphs a sub-expression. 𝔼 ('evaluate') takes the universe as an+-- explicit second expression argument, while 𝕄 ('morph') is handed the threaded+-- 'univ'. Every other function is delegated unchanged. This is the matcher's+-- condition path (guards in 'when'/'having'), which has no state to thread, so 𝔼+-- and 𝕄 run here on a fresh, empty state whose result is discarded; the+-- state-threading callers in 'sidePremise' use '_evaluate' and '_morph' directly.+execBuildTerm :: Expression -> ReduceContext -> BuildTermFunc+execBuildTerm _ ctx "evaluate" = \args subst -> fst <$> _evaluate ctx emptyState args subst+execBuildTerm univ ctx "morph" = \args subst -> fst <$> _morph univ ctx emptyState args subst+execBuildTerm _ ctx func = _buildTerm ctx func++-- The Evaluation function 𝔼(b, e, s): it fires the λ atom of a formation 'b'+-- against the global universe 'e', under the incoming state 𝑠, normalizes the+-- atom's raw result 𝒩(e₁) = n, and returns that normal form together with the+-- new state. Normalizing here makes 𝔼's codomain 𝓝 (as its type demands), so+-- callers ('fire', 'ml') need no follow-up 'normalize' premise. The universe is+-- passed explicitly as the second argument (rather than threaded behind the+-- scenes), matching how the morphing 𝕄 and dataization 𝔻 functions carry it.+-- Every firing is reported to '_saveEval', which the '--evaluations' option+-- turns into one record per line. The reported result is the normal form 𝔼+-- returns, never the atom's raw answer, so the protocol and the caller see the+-- same term. Firings are reported in the order they complete, so the atom of a+-- head reduced by 'ml' is reported before the one dispatched on its result. A+-- firing that gets stuck is reported too, with no result, when the run is a+-- partial evaluation rather than a failure ('_partial'): the site is what the+-- caller wants to learn then. The report is made before the signal goes on to+-- the spine, where 'parking' attaches the derivation to it.+_evaluate :: ReduceContext -> State -> BuildTermMethodS+_evaluate ctx state [ArgExpression expr, ArgExpression universe] subst = do+  form <- buildExpressionThrows expr subst+  univ <- buildExpressionThrows universe subst+  case form of+    ExFormation bds -> case lambda bds of+      Just (func, args) -> do+        (raw, state') <- atom func args univ state ctx `catch` parked func args+        (normal, _) <- normalized raw ((univ, Nothing) :| []) ctx+        ctx._saveEval (Evaluation func args (Just normal))+        pure (TeExpression normal, state')+      Nothing -> throwIO (userError "Function evaluate() expects a formation with a λ binding")+    _ -> throwIO (userError "Function evaluate() expects a formation")+  where+    parked :: T.Text -> Expression -> ReduceException -> IO a+    parked func args failure@(Stuck _) = do+      when ctx._partial (ctx._saveEval (Evaluation func args Nothing))+      throwIO failure+    parked _ _ failure = throwIO failure+_evaluate _ _ _ _ = throwIO (userError "Function evaluate() requires exactly 2 expression arguments")++-- The Morphing function 𝕄 exposed as a build-term function so a rule can morph+-- a sub-expression in its 'where' (the 'md' and 'ma' rules morph+-- the head before re-attaching it). The step chain is discarded: the producing+-- rule splices the surrounding normalization steps itself, and a stuck atom met+-- on the way leaves without it (see 'unparked'). The state is threaded through+-- and the new state returned alongside the morphed term.+_morph :: Expression -> ReduceContext -> State -> BuildTermMethodS+_morph univ ctx state [ArgExpression expr] subst = unparked $ do+  built <- buildExpressionThrows expr subst+  ((morphed, _), state') <- morph' (built, (univ, Nothing) :| []) univ state ctx+  pure (TeExpression morphed, state')+_morph _ _ _ _ _ = throwIO (userError "Function morph() requires exactly 1 expression argument")

@@ -17,7 +17,7 @@ import qualified Data.Aeson.Key as Key import qualified Data.Aeson.KeyMap as KeyMap import qualified Data.ByteString as BS-import Data.FileEmbed (embedDir, embedFile)+import Data.FileEmbed (embedDir) import Data.Text (Text, unpack) import Data.Yaml (Parser) import qualified Data.Yaml as Yaml@@ -307,15 +307,17 @@           rule       ) +-- Decode one rule out of the file that carries it, naming that file when its+-- YAML is broken. A rule set is a directory 'embedDir' embeds wholesale, one+-- rule per file, the file named after the rule it carries.+decodeRule :: (FromJSON a) => (FilePath, BS.ByteString) -> a+decodeRule (path, bs) = case Yaml.decodeEither' bs of+  Right rule -> rule+  Left err -> error $ "YAML parse error in " ++ path ++ ": " ++ show err+ normalizationRules :: [Rule] {-# NOINLINE normalizationRules #-} normalizationRules = map decodeRule $(embedDir "resources/normalize")-  where-    decodeRule :: (FilePath, BS.ByteString) -> Rule-    decodeRule (path, bs) =-      case Yaml.decodeEither' bs of-        Right rule -> rule-        Left err -> error $ "YAML parse error in " ++ path ++ ": " ++ show err  yamlRule :: FilePath -> IO Rule yamlRule = Yaml.decodeFileThrow@@ -494,19 +496,14 @@           pure rule       ) -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")+morphingRules = map decodeRule $(embedDir "resources/morphing")  dataizationRules :: [DataizeRule] {-# NOINLINE dataizationRules #-}-dataizationRules = decodeRules "resources/dataization.yaml" $(embedFile "resources/dataization.yaml")+dataizationRules = map decodeRule $(embedDir "resources/dataization")  contextualizationRules :: [ContextualizeRule] {-# NOINLINE contextualizationRules #-}-contextualizationRules = decodeRules "resources/contextualization.yaml" $(embedFile "resources/contextualization.yaml")+contextualizationRules = map decodeRule $(embedDir "resources/contextualization")

@@ -659,6 +659,36 @@     it "fails a question whose dotted path runs into a void attribute" $       refusesAt "⟦ v ↦ ∅ ⟧" (referring 1 "v.length" False "*2A-*") ["L_answer", "carries no attribute 'v.length'"] +    -- An argument of an application binds an attribute the way a τ binding of+    -- a formation does, so a path walks into one just the same: a marker a+    -- program built itself and put in a void is read back as written, since+    -- dataizing the object around it would fire the λ inside it (#1212)+    it "reaches an attribute an argument of an application binds" $+      servesAt+        "⟦ x ↦ Φ.bool( if ↦ ⟦ guard ↦ ⟦ λ ⤍ S1 ⟧ ⟧ ) ⟧"+        (referring 1 "x.if.guard" False "*'\"λ\":\"S1\"'*")+        "⟦ Δ ⤍ FF- ⟧"++    it "walks past the arguments of an application the path does not name" $+      servesAt+        "⟦ x ↦ Φ.tuple( length ↦ ⟦ Δ ⤍ 01- ⟧, head ↦ ⟦ Δ ⤍ 02- ⟧ ) ⟧"+        (referring 1 "x.length" False "*'\"Δ\":\"01-\"'*")+        "⟦ Δ ⤍ FF- ⟧"++    it "walks past a positional argument of an application" $+      servesAt+        "⟦ x ↦ ⟦ y ↦ ⟦ Δ ⤍ 04- ⟧ ⟧( α0 ↦ ⟦ Δ ⤍ 05- ⟧ ) ⟧"+        (referring 1 "x.y" False "*'\"Δ\":\"04-\"'*")+        "⟦ Δ ⤍ FF- ⟧"++    -- What an application binds an attribute to is what the attribute is,+    -- whatever the formation under it still says about it+    it "takes the argument of an application over the void it fills" $+      servesAt+        "⟦ x ↦ ⟦ y ↦ ∅ ⟧( y ↦ ⟦ Δ ⤍ 03- ⟧ ) ⟧"+        (referring 1 "x.y" False "*'\"Δ\":\"03-\"'*")+        "⟦ Δ ⤍ FF- ⟧"+     -- 𝜑-calculus types nothing nominally, so the forma of a typed literal     -- lives in the name it is dispatched off Φ by and nowhere else: an answer     -- that is an application spells that name, the way a formation spells its

@@ -1844,32 +1844,8 @@         ["explain", "--morph"]         [ unlines             [ "\\begin{phinoMorphingInference}"-            , "  \\phinoName{mf}"-            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_0 ]] }{ e_0 }{ s }{ [[ B_0 ]] }{ s } }"-            , "\\end{phinoMorphingInference}"-            , "\\begin{phinoMorphingInference}"-            , "  \\phinoName{ml}"-            , "  \\phinoLabel{\\lambda}"-            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F_0, B_2 ]] }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"-            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau_0 }{ n_2 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F_0, B_2 ]] . \\tau_0 }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }"-            , "\\end{phinoMorphingInference}"-            , "\\begin{phinoMorphingInference}"-            , "  \\phinoName{mphi}"-            , "  \\phinoLabel{\\varphi}"-            , "  \\phinoCondition{ @ \\in B_0 \\;\\text{and}\\; \\tau_0 \\notin B_0 \\;\\text{and}\\; L \\notin B_0 }"-            , "  \\phinoPremise{ \\phinoNormalize{ [[ B_0 ]] . @ . \\tau_0 }{ n_1 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n_1 }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_0 ]] . \\tau_0 }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"-            , "\\end{phinoMorphingInference}"-            , "\\begin{phinoMorphingInference}"-            , "  \\phinoName{md}"-            , "  \\phinoCondition{ \\phinoNotFormation{ n_0 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n_0 }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"-            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau_0 }{ n_2 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ n_0 . \\tau_0 }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }"+            , "  \\phinoName{dead}"+            , "  \\phinoConclusion{ \\phinoMorph{ T }{ e_0 }{ s }{ T }{ s } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{ma}"@@ -1886,18 +1862,51 @@             , "  \\phinoConclusion{ \\phinoMorph{ n_0 ( \\phiTerminal{\\alpha_{i0}} -> k_1 ) }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"-            , "  \\phinoName{mad}"+            , "  \\phinoName{maad}"             , "  \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }"             , "  \\phinoPremise{ \\phinoMorph{ T }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> n_1 ) }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> n_1 ) }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"-            , "  \\phinoName{maad}"+            , "  \\phinoName{mad}"             , "  \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }"             , "  \\phinoPremise{ \\phinoMorph{ T }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> n_1 ) }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> n_1 ) }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"+            , "  \\phinoName{md}"+            , "  \\phinoCondition{ \\phinoNotFormation{ n_0 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_0 }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau_0 }{ n_2 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ n_0 . \\tau_0 }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }"+            , "\\end{phinoMorphingInference}"+            , "\\begin{phinoMorphingInference}"+            , "  \\phinoName{mf}"+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_0 ]] }{ e_0 }{ s }{ [[ B_0 ]] }{ s } }"+            , "\\end{phinoMorphingInference}"+            , "\\begin{phinoMorphingInference}"+            , "  \\phinoName{mg}"+            , "  \\phinoPremise{ \\phinoMorph{ T }{ Q }{ s_1 }{ n_1 }{ s_2 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n_1 }{ s_2 } }"+            , "\\end{phinoMorphingInference}"+            , "\\begin{phinoMorphingInference}"+            , "  \\phinoName{ml}"+            , "  \\phinoLabel{\\lambda}"+            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F_0, B_2 ]] }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau_0 }{ n_2 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F_0, B_2 ]] . \\tau_0 }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }"+            , "\\end{phinoMorphingInference}"+            , "\\begin{phinoMorphingInference}"+            , "  \\phinoName{mphi}"+            , "  \\phinoLabel{\\varphi}"+            , "  \\phinoCondition{ @ \\in B_0 \\;\\text{and}\\; \\tau_0 \\notin B_0 \\;\\text{and}\\; L \\notin B_0 }"+            , "  \\phinoPremise{ \\phinoNormalize{ [[ B_0 ]] . @ . \\tau_0 }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_1 }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_0 ]] . \\tau_0 }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"+            , "\\end{phinoMorphingInference}"+            , "\\begin{phinoMorphingInference}"             , "  \\phinoName{universe}"             , "  \\phinoLabel{\\Phi}"             , "  \\phinoCondition{ e_0 \\not= Q }"@@ -1906,19 +1915,10 @@             , "  \\phinoConclusion{ \\phinoMorph{ Q }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"-            , "  \\phinoName{dead}"-            , "  \\phinoConclusion{ \\phinoMorph{ T }{ e_0 }{ s }{ T }{ s } }"-            , "\\end{phinoMorphingInference}"-            , "\\begin{phinoMorphingInference}"             , "  \\phinoName{xi}"             , "  \\phinoPremise{ \\phinoMorph{ T }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"             , "  \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"             , "\\end{phinoMorphingInference}"-            , "\\begin{phinoMorphingInference}"-            , "  \\phinoName{mg}"-            , "  \\phinoPremise{ \\phinoMorph{ T }{ Q }{ s_1 }{ n_1 }{ s_2 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n_1 }{ s_2 } }"-            , "\\end{phinoMorphingInference}"             ]         ] @@ -1927,11 +1927,6 @@         ["explain", "--dataize"]         [ unlines             [ "\\begin{phinoDataizationInference}"-            , "  \\phinoName{delta}"-            , "  \\phinoLabel{\\Delta}"-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta_0, B_2 ]] }{ e_0 }{ s }{ \\delta_0 }{ s } }"-            , "\\end{phinoDataizationInference}"-            , "\\begin{phinoDataizationInference}"             , "  \\phinoName{box}"             , "  \\phinoCondition{ [ D \\char44{} L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset }"             , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ [[ B_1, @ -> e_1, B_2 ]] }{ e_2 } }"@@ -1940,6 +1935,11 @@             , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_1, B_2 ]] }{ e_0 }{ s_1 }{ \\delta_0 }{ s_2 } }"             , "\\end{phinoDataizationInference}"             , "\\begin{phinoDataizationInference}"+            , "  \\phinoName{delta}"+            , "  \\phinoLabel{\\Delta}"+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta_0, B_2 ]] }{ e_0 }{ s }{ \\delta_0 }{ s } }"+            , "\\end{phinoDataizationInference}"+            , "\\begin{phinoDataizationInference}"             , "  \\phinoName{fire}"             , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F_0, B_2 ]] }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"             , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e_0 }{ s_2 }{ \\delta_0 }{ s_3 } }"@@ -1966,37 +1966,37 @@         ["explain", "--contextualize"]         [ unlines             [ "\\begin{phinoContextualizationInference}"-            , "  \\phinoName{cg}"-            , "  \\phinoConclusion{ \\phinoContextualize{ Q }{ k_0 }{ Q } }"+            , "  \\phinoName{ca}"+            , "  \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ k_0 }{ n_2 } }"+            , "  \\phinoConclusion{ \\phinoContextualize{ n_0 ( \\tau_0 -> e_1 ) }{ k_0 }{ n_1 ( \\tau_0 -> n_2 ) } }"             , "\\end{phinoContextualizationInference}"             , "\\begin{phinoContextualizationInference}"-            , "  \\phinoName{cxi}"-            , "  \\phinoConclusion{ \\phinoContextualize{ \\phiTerminal{\\xi} }{ k_0 }{ k_0 } }"+            , "  \\phinoName{caa}"+            , "  \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ k_0 }{ n_2 } }"+            , "  \\phinoConclusion{ \\phinoContextualize{ n_0 ( \\phiTerminal{\\alpha_{i0}} -> e_1 ) }{ k_0 }{ n_1 ( \\phiTerminal{\\alpha_{i0}} -> n_2 ) } }"             , "\\end{phinoContextualizationInference}"             , "\\begin{phinoContextualizationInference}"-            , "  \\phinoName{ct}"-            , "  \\phinoConclusion{ \\phinoContextualize{ T }{ k_0 }{ T } }"+            , "  \\phinoName{cd}"+            , "  \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }"+            , "  \\phinoConclusion{ \\phinoContextualize{ n_0 . \\tau_0 }{ k_0 }{ n_1 . \\tau_0 } }"             , "\\end{phinoContextualizationInference}"             , "\\begin{phinoContextualizationInference}"             , "  \\phinoName{cf}"             , "  \\phinoConclusion{ \\phinoContextualize{ [[ B_0 ]] }{ k_0 }{ [[ B_0 ]] } }"             , "\\end{phinoContextualizationInference}"             , "\\begin{phinoContextualizationInference}"-            , "  \\phinoName{cd}"-            , "  \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }"-            , "  \\phinoConclusion{ \\phinoContextualize{ n_0 . \\tau_0 }{ k_0 }{ n_1 . \\tau_0 } }"+            , "  \\phinoName{cg}"+            , "  \\phinoConclusion{ \\phinoContextualize{ Q }{ k_0 }{ Q } }"             , "\\end{phinoContextualizationInference}"             , "\\begin{phinoContextualizationInference}"-            , "  \\phinoName{ca}"-            , "  \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }"-            , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ k_0 }{ n_2 } }"-            , "  \\phinoConclusion{ \\phinoContextualize{ n_0 ( \\tau_0 -> e_1 ) }{ k_0 }{ n_1 ( \\tau_0 -> n_2 ) } }"+            , "  \\phinoName{ct}"+            , "  \\phinoConclusion{ \\phinoContextualize{ T }{ k_0 }{ T } }"             , "\\end{phinoContextualizationInference}"             , "\\begin{phinoContextualizationInference}"-            , "  \\phinoName{caa}"-            , "  \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }"-            , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ k_0 }{ n_2 } }"-            , "  \\phinoConclusion{ \\phinoContextualize{ n_0 ( \\phiTerminal{\\alpha_{i0}} -> e_1 ) }{ k_0 }{ n_1 ( \\phiTerminal{\\alpha_{i0}} -> n_2 ) } }"+            , "  \\phinoName{cxi}"+            , "  \\phinoConclusion{ \\phinoContextualize{ \\phiTerminal{\\xi} }{ k_0 }{ k_0 } }"             , "\\end{phinoContextualizationInference}"             ]         ]

@@ -10,7 +10,7 @@ module DataizeSpec (spec) where  import AST-import Atoms (Registry, emptyRegistry, readRegistry)+import Atoms (Registry, emptyRegistry) import Control.Exception (SomeException) import Control.Monad import Data.Aeson (FromJSON)@@ -19,162 +19,63 @@ import Data.List.NonEmpty (NonEmpty (..)) import Data.Maybe (fromMaybe, isJust) import Data.Yaml qualified as Decode-import Dataize (DataizeContext (..), Outcome (..), Steps (..), dataize, dataize', emptyState, execBuildTerm, insideUniverse, morph, morph')-import Deps (Evaluation (..), Term (TeExpression), dontSaveEval, dontSaveStep)+import Dataize (Outcome (..), dataize, dataize', reduction)+import Deps (Evaluation (..), dontSaveEval, dontSaveStep) import Files (allPathsIn)-import Fixtures (fixtureRegistry, withNode, withServing, withShell)+import Fixtures (defaultReduceContext, fixtureRegistry, primitives, withAtoms, withNode) import Functions (buildTerm) import GHC.Generics (Generic) import Matcher (substEmpty)-import Parser (parseExpressionThrows)+import Morph (ReduceContext (..), Steps (..), emptyState, execBuildTerm)+import Parser (parseBytes, parseExpressionThrows) import Rewriter (Rewritten) import Rule (RuleContext (RuleContext), matchExpressionWithRule') import System.FilePath (makeRelative) import Test.Hspec-import Yaml (ExtraArgument (..)) import Yaml qualified --- Shuffle is enabled so the suite exercises the order-independence of the--- dataization rules (#909): a hidden overlap surfaces as a nondeterministic--- failure instead of staying silently green. The registry of λ functions is--- empty, since phino implements none of them: a case that needs an atom to--- answer brings the fixture registry in through 'withAtoms'.-defaultDataizeContext :: Expression -> DataizeContext-defaultDataizeContext loc = DataizeContext loc 25 25 (Steps 250 0) False True False False emptyRegistry buildTerm dontSaveStep dontSaveEval---- The same context with the fixture λ functions registered (see 'Fixtures').-withAtoms :: Registry -> DataizeContext -> DataizeContext-withAtoms registry ctx = ctx{_atoms = registry}--test :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> String -> DataizeContext -> IO ((a, [Rewritten]), String)) -> [(String, Expression, Expression, a)] -> Spec+test :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> String -> ReduceContext -> IO ((a, [Rewritten]), String)) -> [(String, Expression, Expression, a)] -> Spec test func useCases =   forM_ useCases $ \(desc, input, expr, output) ->     it desc $ do-      ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultDataizeContext ExRoot)-      res `shouldBe` output--test' :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> String -> DataizeContext -> IO ((a, NonEmpty Rewritten), String)) -> [(String, Expression, Expression, a)] -> Spec-test' func useCases =-  forM_ useCases $ \(desc, input, expr, output) ->-    it desc $ do-      ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultDataizeContext ExRoot)+      ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultReduceContext ExRoot)       res `shouldBe` output -testDataize :: [(String, String, String, Bytes)] -> Spec-testDataize useCases =-  forM_ useCases $ \(name, loc, src, res) ->-    it name $ do-      expr <- parseExpressionThrows src-      loc' <- parseExpressionThrows loc-      (value, _) <- dataize expr (defaultDataizeContext loc')-      value `shouldBe` Dataized res--testMorph :: [(String, String, String, String)] -> Spec-testMorph useCases =-  forM_ useCases $ \(name, loc, src, res) ->-    it name $ do-      expr <- parseExpressionThrows src-      loc' <- parseExpressionThrows loc-      expected <- parseExpressionThrows res-      (morphed, _) <- morph expr (defaultDataizeContext loc')-      morphed `shouldBe` expected---- One case of the deep walk, as a pack of 'test-resources/morph-deep-packs'--- spells it: the program under 'input', wrapped in the fixture object model--- where 'model' says so and run against the fixture λ functions where 'atoms'--- does, entered at 'location' and answering either the program under 'result'--- or the failure under 'fails'.-data DeepPack = DeepPack+-- One case of 𝔻, as a pack of 'test-resources/dataization-packs' spells it: the+-- program under 'input', wrapped in the fixture object model where 'model' says+-- so and run against the fixture λ functions where 'atoms' does, entered at+-- 'location' and answering either the bytes under 'result' or the failure under+-- 'fails'.+data DataizePack = DataizePack   { location :: Maybe String   , input :: String   , model :: Maybe Bool   , atoms :: Maybe Bool-  , partial :: Maybe Bool   , result :: Maybe String   , fails :: Maybe String   }   deriving (Generic, Show, FromJSON) --- Walk one such pack with '_deep' on and check what it answers. A pack that--- registers the fixture λ functions fires one under 'node', so it is pending--- where 'node' is not installed.-testDeep :: Registry -> FilePath -> Expectation-testDeep registry pth = do-  DeepPack{..} <- Decode.decodeFileThrow pth+-- Dataize one such pack and check what it answers. A pack that registers the+-- fixture λ functions runs an external script, so it is pending where 'node' is+-- not installed.+testDataize :: Registry -> FilePath -> Expectation+testDataize registry pth = do+  DataizePack{..} <- Decode.decodeFileThrow pth   expr <- parseExpressionThrows (if model == Just True then primitives input else input)   loc <- parseExpressionThrows (fromMaybe "Q" location)-  let ctx =-        (defaultDataizeContext loc)-          { _deep = True-          , _partial = partial == Just True-          , _atoms = if atoms == Just True then registry else emptyRegistry-          }+  let ctx = (defaultReduceContext loc){_atoms = if atoms == Just True then registry else emptyRegistry}       checked :: Expectation       checked = case (result, fails) of         (Just res, Nothing) -> do-          expected <- parseExpressionThrows res-          (morphed, _) <- morph expr ctx-          morphed `shouldBe` expected+          bts <- either (fail . ("cannot read the expected bytes: " ++)) pure (parseBytes res)+          (value, _) <- dataize expr ctx+          value `shouldBe` Dataized bts         (Nothing, Just message) ->-          morph expr ctx `shouldThrow` (\err -> message `isInfixOf` show (err :: SomeException))+          dataize expr ctx `shouldThrow` (\err -> message `isInfixOf` show (err :: SomeException))         _ -> expectationFailure "The pack holds neither a single 'result' nor a single 'fails'"   if atoms == Just True then withNode checked else checked --- The EO objects the fixture λ functions answer for, declared the way--- 'number.eo' and 'bytes.eo' declare them, so a case below only has to spell--- the expression under φ. 'number.eq' is the one operation with no atom of its--- own: EO spells it out of 'L_bytes_eq' (eq.eo), so the fixture composes it the--- same way. Alongside them stand the objects the atoms hand results to: 'string'--- carries what a byte-array complaint would say, while 'true' and 'false' fill--- in for the real bool objects, since the single byte an EO bool dataizes to is--- all these cases assert. Those bytes are EO's own: 'true.eo' asserts--- 'true.as-bytes.eq FF-' and 'bool.eo' branches 'if' over 'FF-' and '00-', so a--- universe copied from here starts with a bool an EO program recognizes.--- 'number.nope' is declared and left out of the registry on purpose: it is the--- λ function that cannot fire, the one '--partial' parks on.-primitives :: String -> String-primitives src =-  unlines-    [ "[["-    , "  bytes -> [["-    , "    φ -> ?,"-    , "    not -> [[ L> L_bytes_not ]],"-    , "    eq -> [[ b -> ?, L> L_bytes_eq ]]"-    , "  ]],"-    , "  number -> [["-    , "    φ -> ?,"-    , "    as-bytes -> $.φ,"-    , "    plus -> [[ x -> ?, L> L_number_plus ]],"-    , "    times -> [[ x -> ?, L> L_number_times ]],"-    , "    div -> [[ x -> ?, L> L_number_div ]],"-    , "    gt -> [[ x -> ?, L> L_number_gt ]],"-    , "    eq -> [[ x -> ?, @ -> $.^.as-bytes.eq( x.as-bytes ) ]],"-    , "    nope -> [[ L> L_number_nope ]]"-    , "  ]],"-    , "  string -> [[ φ -> ?, as-bytes -> $.φ ]],"-    , "  true -> [[ @ -> [[ D> FF- ]] ]],"-    , "  false -> [[ @ -> [[ D> 00- ]] ]],"-    , "  @ -> " ++ src-    , "]]"-    ]---- Wrap a hex literal into the bytes object that EO source spells as a bare '20-1F'-raw :: String -> String-raw bts = "Φ.bytes( φ ↦ ⟦ Δ ⤍ " ++ bts ++ " ⟧ )"---- Dataize an expression against the fixture universe, with the fixture λ--- functions registered. Every such case runs an external script, so it is--- pending where 'node' is not installed.-testAtom :: Registry -> [(String, String, Bytes)] -> Spec-testAtom registry useCases =-  forM_ useCases $ \(name, src, res) ->-    it name $-      withNode $ do-        expr <- parseExpressionThrows (primitives src)-        loc <- parseExpressionThrows "Q"-        (value, _) <- dataize expr (withAtoms registry (defaultDataizeContext loc))-        value `shouldBe` Dataized res- -- Dataize under '--partial', collecting every report 𝔼 makes on the way, in -- the order it makes them partially :: Registry -> String -> IO ((Outcome, [Rewritten]), [Evaluation])@@ -182,7 +83,7 @@   expr <- parseExpressionThrows (primitives src)   reports <- newIORef []   let ctx =-        (withAtoms registry (defaultDataizeContext ExRoot))+        (withAtoms registry (defaultReduceContext ExRoot))           { _partial = True           , _saveEval = \report -> modifyIORef' reports (report :)           }@@ -190,138 +91,12 @@   collected <- readIORef reports   pure (result, reverse collected) --- An atom with no answer yields ⊥, which stops the whole dataization-testStuckAtom :: Registry -> [(String, String)] -> Spec-testStuckAtom registry useCases =-  forM_ useCases $ \(name, src) ->-    it name $-      withNode $ do-        expr <- parseExpressionThrows (primitives src)-        loc <- parseExpressionThrows "Q"-        dataize expr (withAtoms registry (defaultDataizeContext loc))-          `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))- spec :: Spec spec = do   -- Every λ function a case may fire comes from the fixture registry, read   -- once here: phino carries none of its own (see 'Fixtures').   registry <- runIO fixtureRegistry -  -- The top-level 𝕄 entry point, the one the 'morph' command runs: it locates-  -- the subterm, threads the whole input expression as the universe and hands-  -- back the morphed expression together with the chain that led to it (#1114).-  describe "morph" $ do-    testMorph-      [ ("hands the top formation back untouched under the Q locator", "Q", "[[ D> 00- ]]", "[[ D> 00- ]]")-      , -- 𝕄 is total where 𝔻 is not: the 'xi' axiom morphs ξ to ⊥, so the run-        -- ends with an answer rather than with a failure-        ("answers ⊥ where no formation is reachable", "Q.x", "[[ x -> $ ]]", "T")-      ]--    -- The chain runs oldest step first and carries the rule that produced the-    -- step after it, exactly as 'dataize' reports its own, so '--sequence'-    -- prints both the same way-    it "reports the chain of steps oldest first" $ do-      expr <- parseExpressionThrows "[[ D> 00- ]]"-      (morphed, chain) <- morph expr (defaultDataizeContext ExRoot)-      morphed `shouldBe` expr-      map snd chain `shouldBe` [Just "mf", Nothing]-      map fst chain `shouldBe` [expr, expr]--    -- 𝕄 never fires a bare λ-formation, so only an atom sitting under a-    -- dispatch (the 'ml' rule) can get stuck-    describe "a stuck atom under 'ml'" $ do-      let stuck :: IO (Expression, Expression)-          stuck = (,) <$> parseExpressionThrows "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" <*> parseExpressionThrows "Q.x"-      it "fails the run without '_partial'" $ do-        (expr, loc) <- stuck-        morph expr (defaultDataizeContext loc)-          `shouldThrow` (\e -> "Atom 'Sym_arg_0' does not exist" `isInfixOf` show (e :: SomeException))--      it "is parked in the residue under '_partial'" $ do-        (expr, loc) <- stuck-        expected <- parseExpressionThrows "[[ L> Sym_arg_0 ]].foo"-        (residue, _) <- morph expr (defaultDataizeContext loc){_partial = True}-        residue `shouldBe` expected--  -- 𝕄 stops at the first formation 'mf' hands back and leaves its bindings as-  -- they were written, since firing a bare λ is 𝔻's business, so a program-  -- whose parts nothing demands is never reduced (#1124). The deep walk-  -- ('_deep') enters every binding and finishes what 'mf' left, while what no-  -- atom touched keeps the shape it was written in and the answer stays a-  -- program.-  describe "morph with '_deep'" $ do-    let resources = "test-resources/morph-deep-packs"-    packs <- runIO (allPathsIn resources)-    forM_ packs (\pth -> it (makeRelative resources pth) (testDeep registry pth))--    -- The walk enters a dispatch through its target and fires the box it finds-    -- there before 𝕄 is ever asked about the dispatch, while 'ml' demands that-    -- λ only where the dispatched attribute is none of the box's own (#1187)-    describe "a dispatch naming an attribute of the formation it stands on" $-      it "cannot fire the λ the dispatch does not demand" $-        withShell $-          withServing "printf '{\"id\": %s, \"𝑛\": \"⟦ Δ ⤍ FF- ⟧\"}\\n' \"$id\"" $ \path -> do-            box <- readRegistry path-            world <- parseExpressionThrows "[[ foo -> [[ f -> [[ a -> ?, @ -> $.a, L> L_answer ]] ]], x -> Q.foo.f( a -> [[ D> 01- ]] ).@ ]]"-            (morphed, _) <- morph world (withAtoms box (defaultDataizeContext ExRoot)){_deep = True}-            morphed `shouldBe` world--  describe "morph'" $-    test'-      morph'-      [ ("[[ D> 00- ]] => [[ D> 00- ]]", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")])-      , ("T => T", ExTermination, ExRoot, ExTermination)-      , ("$ => X", ExXi, ExRoot, ExTermination)-      , ("Q => X", ExRoot, ExRoot, ExTermination)-      ,-        ( "Q.x (Q -> [[ x -> [[]] ]]) => [[ ρ -> Q ]]"-        , ExDispatch ExRoot (AtLabel "x")-        , ExFormation [BiTau (AtLabel "x") (ExFormation [])]-        , ExFormation [BiTau AtRho (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho])]-        )-      , -- A void slot fed a non-absolute argument can never be filled, so 'copy'-        -- cannot fire and the application is a stuck normal form. Before #959,-        -- 'ma' re-morphed this identical term forever; now the 'mad' axiom-        -- morphs it straight to ⊥, keeping 𝕄 total.--        ( "[[ x -> ? ]](x -> $.foo) => T"-        , ExApplication (ExFormation [BiVoid (AtLabel "x")]) (ArTau (AtLabel "x") (ExDispatch ExXi (AtLabel "foo")))-        , ExRoot-        , ExTermination-        )-      , -- Same as above but through the alpha-argument sibling 'maad' instead of-        -- 'mad': a void slot fed a non-absolute alpha-indexed argument also-        -- morphs straight to ⊥.--        ( "[[ ^ -> ? ]](α0 -> $.foo) => T"-        , ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) (ExDispatch ExXi (AtLabel "foo")))-        , ExRoot-        , ExTermination-        )-      , -- 'universe' fires only when the universe 'e' differs from Φ itself-        -- ('not (eq(e, Φ))'); it then normalizes and re-morphs that universe.-        -- Here the universe is a plain formation, already a normal form, so-        -- re-morphing it lands straight on 'mf' and returns it unchanged.--        ( "Q => [[]] (a universe distinct from Φ) => [[]]"-        , ExRoot-        , ExFormation []-        , ExFormation []-        )-      ]--  -- 𝕄's first argument is always a normal form reachable through normalization,-  -- and every such normal form is covered by some morphing clause (an axiom-  -- like 'mf'/'dead'/'xi'/'universe'/'mg' or a recursive rule), so the "no rule-  -- matched" fallback never fires along any real derivation. It is still total-  -- code, reachable by calling 'morph'' directly (bypassing normalization) on a-  -- raw meta 𝑛, an AST node the matcher never binds to any concrete pattern.-  describe "morph' fails when no morphing rule matches the term" $-    it "throws instead of looping when handed a bare, unmatched meta" $-      morph' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)-        `shouldThrow` (\e -> "no morphing rule matched" `isInfixOf` show (e :: SomeException))-   -- Symmetric to the morphing fallback above: every normal form 𝔻 actually   -- receives is covered by 'delta'/'box'/'fire'/'none' (formations) or 'norm'   -- (everything else, disjoint from ⊥ and formations), so this fallback is@@ -330,153 +105,17 @@   -- proving the fallback itself is live code, not dead weight.   describe "dataize' fails when no dataization rule matches the term" $     it "throws instead of treating the unmatched meta as ⊥" $-      dataize' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)+      dataize' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)         `shouldThrow` (\e -> "no dataization rule matched" `isInfixOf` show (e :: SomeException)) -  -- 'execBuildTerm's "evaluate" and "morph" cases expose 𝔼 and 𝕄 to the-  -- matcher's condition path (guards in 'when'/'having'). No built-in rule's-  -- guard actually calls either function, so these error paths — reachable only-  -- by malformed arguments — are exercised here directly through the exported-  -- 'execBuildTerm', the same way the matcher would call it.-  describe "execBuildTerm 'evaluate'" $ do-    let univ = ExFormation []-        ctx = withAtoms registry (defaultDataizeContext ExRoot)-        runEvaluate args = execBuildTerm univ ctx "evaluate" args substEmpty-    forM_-      [-        ( "the first argument is not a formation"-        , [ArgExpression ExRoot, ArgExpression univ]-        , "Function evaluate() expects a formation"-        )-      ,-        ( "the formation has no λ binding at all"-        , [ArgExpression (ExFormation []), ArgExpression univ]-        , "expects a formation with a"-        )-      ,-        ( "a non-λ formation still has other bindings"-        , [ArgExpression (ExFormation [BiVoid AtRho]), ArgExpression univ]-        , "expects a formation with a"-        )-      ,-        ( "not given exactly two expression arguments"-        , [ArgExpression univ]-        , "requires exactly 2 expression arguments"-        )-      ]-      ( \(desc, args, message) ->-          it ("throws when " ++ desc) $-            runEvaluate args `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException))-      )-    it "evaluates a λ-bearing formation to the atom's normalized result" $-      withNode $ do-        let form = ExFormation [BiLambda (Function "L_bytes_not"), BiTau AtRho (ExFormation [BiDelta (BtOne "00")])]-        result <- runEvaluate [ArgExpression form, ArgExpression univ]-        case result of-          TeExpression expr -> expr `shouldBe` dataBytes (BtOne "FF")-          _ -> expectationFailure "expected TeExpression"--  describe "execBuildTerm 'morph'" $ do-    let univ = ExFormation []-        ctx = defaultDataizeContext ExRoot-    it "throws when not given exactly one expression argument" $-      execBuildTerm univ ctx "morph" [] substEmpty-        `shouldThrow` (\e -> "requires exactly 1 expression argument" `isInfixOf` show (e :: SomeException))-    it "morphs a single expression argument to its already-normal form" $ do-      result <- execBuildTerm univ ctx "morph" [ArgExpression (ExFormation [BiDelta (BtOne "00")])] substEmpty-      case result of-        TeExpression expr -> expr `shouldBe` ExFormation [BiDelta (BtOne "00")]-        _ -> expectationFailure "expected TeExpression"--  -- An expression that is not part of the program — the operand an atom script-  -- asks phino to reduce — is bound to a synthetic attribute of the universe and-  -- that attribute is what 𝔻 is aimed at. This is what the '--inside' option-  -- runs, and what phino did internally while the atoms still lived in the-  -- binary.-  describe "insideUniverse" $ do-    let universe = "[[ y -> [[ D> 02- ]] ]]"-        reduced src = do-          univ <- parseExpressionThrows universe-          target <- parseExpressionThrows src-          (extended, ctx) <- insideUniverse target univ (defaultDataizeContext ExRoot)-          fst <$> dataize extended ctx-    it "reduces an expression the program does not contain" $ do-      value <- reduced "Q.y"-      value `shouldBe` Dataized (BtOne "02")-    -- 𝔻 accepts normal forms only, and a dispatch off a formation is not one:-    -- 'dot' still applies to it. So the expression is normalized first, which-    -- is the whole reason an atom script cannot simply splice it into the-    -- universe itself.-    it "normalizes what it is handed before 𝔻 sees it" $ do-      value <- reduced "[[ x -> [[ D> 01- ]] ]].x"-      value `shouldBe` Dataized (BtOne "01")-    it "refuses a universe which is not a formation" $ do-      target <- parseExpressionThrows "Q.y"-      insideUniverse target ExRoot (defaultDataizeContext ExRoot)-        `shouldThrow` (\e -> "not a formation" `isInfixOf` show (e :: SomeException))--  -- 'defaultDataizeContext' runs with '_shuffle' on, so 'morph'' walks the-  -- morphing rules in a random order on every step. Every clause is-  -- order-independent (the known overlaps were removed in #856 and #860), so the-  -- outcome must never depend on that order: morphing each input many times under-  -- a shuffling context yields exactly the formation the fixed declaration order-  -- does, proving the rules may be applied in any order with the same result.-  -- Were a hidden overlap re-introduced, some of these random orders would-  -- disagree and 'nub' would collect more than the single expected form.-  describe "morphing is order-independent under --shuffle" $ do-    let cases =-          [ ("a byte formation", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")])-          , ("termination", ExTermination, ExRoot, ExTermination)-          , ("xi", ExXi, ExRoot, ExTermination)-          , ("the global object", ExRoot, ExRoot, ExTermination)-          ,-            ( "a dispatch over a formation"-            , ExDispatch ExRoot (AtLabel "x")-            , ExFormation [BiTau (AtLabel "x") (ExFormation [])]-            , ExFormation [BiTau AtRho (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho])]-            )-          ]-    forM_ cases $ \(desc, input, univ, expected) ->-      it ("morphs " ++ desc ++ " to the same form across 100 random rule orders") $ do-        results <- replicateM 100 (fst . fst <$> morph' (input, (univ, Nothing) :| []) univ emptyState (defaultDataizeContext ExRoot))-        nub results `shouldBe` [expected]--  -- 'md' fires only when its head is not a formation ('not (formation 𝑛)'),-  -- so a formation head — λ-bearing or not — is left to 'ml'/'mf'. The-  -- two clauses are mutually exclusive and their order in 'morphing.yaml'-  -- cannot change behavior.-  describe "morphing 'md' is disjoint from 'ml'" $ do-    let rctx = RuleContext (execBuildTerm ExRoot (defaultDataizeContext ExRoot))-        morphRule :: String -> Yaml.MorphRule-        morphRule nm = fromMaybe (error ("no morphing rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.morphingRules)-        asRule :: Yaml.MorphRule -> Yaml.Rule-        asRule r = Yaml.Rule r.name Nothing Nothing r.match ExRoot r.when Nothing Nothing-        lambdaFormation = ExFormation [BiLambda (Function "L_dummy"), BiVoid AtRho]-    it "does not fire on a λ-bearing formation dispatch" $ do-      substs <- matchExpressionWithRule' [substEmpty] (ExDispatch lambdaFormation (AtLabel "x")) (asRule (morphRule "md")) rctx-      substs `shouldBe` []-    it "still fires on a non-λ-formation dispatch" $ do-      substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (morphRule "md")) rctx-      null substs `shouldBe` False-    -- ⟦λ ⤍ F⟧.a.b.c : 'md' peels .c then .b (their heads are dispatches,-    -- not λ-formations, so 'λ ∉ 𝐵' holds), then 'ml' handles the base-    -- ⟦λ ⤍ F⟧.a and fires the atom. The chain therefore routes-    -- md → md → ml; firing the undefined atom 'F' is what-    -- raises the error, proving the base λ-formation reached 'ml'.-    it "drills a chained λ-formation dispatch down to the base 'ml'" $ do-      let base = ExFormation [BiLambda (Function "F")]-          chain = ExDispatch (ExDispatch (ExDispatch base (AtLabel "a")) (AtLabel "b")) (AtLabel "c")-      morph' (chain, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)-        `shouldThrow` (\e -> "Atom 'F' does not exist" `isInfixOf` show (e :: SomeException))-   -- 'norm' matches the bare meta 𝑛, which unifies with any expression, so it is   -- guarded to fire only when 𝑛 is neither a formation ('not (formation 𝑛)',   -- left to 'delta'/'box'/'fire'/'none') nor the termination ⊥ ('not (𝑛 = ⊥)').   -- 𝔻 is partial: ⊥ matches no clause and lands on the unmatched-term error   -- (#955). The dataization clauses are therefore disjoint and their order in-  -- 'dataization.yaml' cannot change behavior.+  -- 'resources/dataization' cannot change behavior.   describe "dataization 'norm' is disjoint from the specific clauses" $ do-    let rctx = RuleContext (execBuildTerm ExRoot (defaultDataizeContext ExRoot))+    let rctx = RuleContext (execBuildTerm ExRoot (defaultReduceContext ExRoot))         dataizeRule :: String -> Yaml.DataizeRule         dataizeRule nm = fromMaybe (error ("no dataization rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.dataizationRules)         asRule :: Yaml.DataizeRule -> Yaml.Rule@@ -491,7 +130,23 @@       substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (dataizeRule "norm")) rctx       null substs `shouldBe` False -  describe "dataize" $+  -- Most cases of 𝔻 are four plain values — the program, where the run enters+  -- it, which λ functions answer it and what it must dataize to — so they are+  -- packs of 'test-resources/dataization-packs' rather than Haskell (#1201).+  -- Which λ functions exist is no longer phino's business: the registry given+  -- with '--atoms' decides, and each one runs as an external script (see+  -- 'Atoms'). What a pack with 'atoms' on asserts is that the answer of such a+  -- script lands in the derivation exactly where a built-in atom's answer used+  -- to: 𝔼 normalizes it and 𝔻 carries on. The λ functions themselves are the+  -- fixture ones (see 'Fixtures'), and 'number.eq' is composed out of+  -- 'L_bytes_eq' the way 'eq.eo' composes it, so the EO-level composition is+  -- exercised too.+  describe "dataize" $ do+    let resources = "test-resources/dataization-packs"+    packs <- runIO (allPathsIn resources)+    forM_ packs (\pth -> it (makeRelative resources pth) (testDataize registry pth))++  describe "dataize'" $     test       dataize'       [ ("[[ D> 00- ]] => 00-", ExFormation [BiDelta (BtOne "00")], ExRoot, BtOne "00")@@ -536,7 +191,7 @@   describe "fails to dataize the terminator" $ do     let failsOn desc input =           it desc $-            dataize' (input, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)+            dataize' (input, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)               `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))     failsOn "throws on ⊥ instead of mapping it to empty bytes" ExTermination     failsOn "throws on a data-less formation, which dataizes ⊥" (ExFormation [])@@ -558,7 +213,7 @@     it "fails on the step limit instead of morphing forever" $       withNode $ do         expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧"-        dataize expr (DataizeContext ExRoot 25 25 (Steps 40 0) False True False False registry buildTerm dontSaveStep dontSaveEval)+        dataize expr (ReduceContext ExRoot 25 25 (Steps 40 0) False True False False registry buildTerm reduction dontSaveStep dontSaveEval)           `shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException))      -- A budget spent on a cycle is a stuck site just as an atom that cannot@@ -567,7 +222,7 @@     it "parks the step limit as a residual with --partial" $       withNode $ do         expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧"-        (outcome, _) <- dataize expr (DataizeContext ExRoot 25 25 (Steps 40 0) False True True False registry buildTerm dontSaveStep dontSaveEval)+        (outcome, _) <- dataize expr (ReduceContext ExRoot 25 25 (Steps 40 0) False True True False registry buildTerm reduction dontSaveStep dontSaveEval)         case outcome of           Residual _ -> pure ()           Dataized bts -> expectationFailure ("expected a residual, dataized to " ++ show bts)@@ -586,7 +241,7 @@     it "fails on it without the flag, naming the unknown atom" $       withNode $ do         expr <- parseExpressionThrows (primitives "2.times(3).nope")-        dataize expr (withAtoms registry (defaultDataizeContext ExRoot))+        dataize expr (withAtoms registry (defaultReduceContext ExRoot))           `shouldThrow` (\e -> "Atom 'L_number_nope' does not exist" `isInfixOf` show (e :: SomeException))     it "leaves the application of the unregistered atom in place" $       withNode $ do@@ -624,21 +279,21 @@         map (._function) reports `shouldBe` ["L_number_times"]     it "stops on the terminator ⊥ as before, since a wrong operand is not a stuck atom" $       withNode $ do-        expr <- parseExpressionThrows (primitives ("5.plus( " ++ raw "--" ++ " )"))-        dataize expr ((withAtoms registry (defaultDataizeContext ExRoot)){_partial = True})+        expr <- parseExpressionThrows (primitives "5.plus( Φ.bytes( φ ↦ ⟦ Δ ⤍ -- ⟧ ) )")+        dataize expr ((withAtoms registry (defaultReduceContext ExRoot)){_partial = True})           `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException)) -  describe "DataizeContext's --max-depth/--max-cycles reach into the normalization it splices in" $ do+  describe "ReduceContext's --max-depth/--max-cycles reach into the normalization it splices in" $ do     let boxed = "[[ @ -> [[ D> 00- ]] ]]"     forM_       [         ( "--max-cycles"-        , DataizeContext ExRoot 25 0 (Steps 250 0) True True False False emptyRegistry buildTerm dontSaveStep dontSaveEval+        , ReduceContext ExRoot 25 0 (Steps 250 0) True True False False emptyRegistry buildTerm reduction dontSaveStep dontSaveEval         , "--max-cycles=0"         )       ,         ( "--max-depth"-        , DataizeContext ExRoot 0 25 (Steps 250 0) True True False False emptyRegistry buildTerm dontSaveStep dontSaveEval+        , ReduceContext ExRoot 0 25 (Steps 250 0) True True False False emptyRegistry buildTerm reduction dontSaveStep dontSaveEval         , "--max-depth=0"         )       ]@@ -648,8 +303,8 @@             dataize expr ctx `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException))       )     forM_-      [ ("--max-cycles", DataizeContext ExRoot 25 0 (Steps 250 0) False True False False emptyRegistry buildTerm dontSaveStep dontSaveEval)-      , ("--max-depth", DataizeContext ExRoot 0 25 (Steps 250 0) False True False False emptyRegistry buildTerm dontSaveStep dontSaveEval)+      [ ("--max-cycles", ReduceContext ExRoot 25 0 (Steps 250 0) False True False False emptyRegistry buildTerm reduction dontSaveStep dontSaveEval)+      , ("--max-depth", ReduceContext ExRoot 0 25 (Steps 250 0) False True False False emptyRegistry buildTerm reduction dontSaveStep dontSaveEval)       ]       ( \(flag, ctx) ->           it ("does not throw without --depth-sensitive even once " ++ flag ++ " is exhausted") $ do@@ -675,7 +330,7 @@       withNode $ do         expr <- parseExpressionThrows (primitives "5.plus(6)")         loc <- parseExpressionThrows "Q"-        (_, chain) <- dataize expr (withAtoms registry (defaultDataizeContext loc))+        (_, chain) <- dataize expr (withAtoms registry (defaultReduceContext loc))         let orphans = nub [label | (_, Just label) <- chain, label `notElem` allowed]         unless           (null orphans)@@ -695,7 +350,7 @@     let labelsOf loc src = do           expr <- parseExpressionThrows src           loc' <- parseExpressionThrows loc-          (_, chain) <- dataize expr (withAtoms registry (defaultDataizeContext loc'))+          (_, chain) <- dataize expr (withAtoms registry (defaultReduceContext loc'))           pure [label | (_, Just label) <- chain]     it "dataizes 5.plus(6) through the expected rules" $       withNode $ do@@ -723,133 +378,3 @@     it "dataizes a located reference through the expected rules" $ do       labels <- labelsOf "Q.foo.bar" "[[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]"       labels `shouldBe` ["contextualize", "md", "dot", "copy", "mf", "delta"]-    -- The 'none' rule dataizes ⊥ (𝔻(⟦⟧) → 𝔻(⊥)), which matches no clause now-    -- that there is no 'end' rule, so an empty formation reduces through one-    -- labelled 'dataize' step and then fails: it has nothing to dataize (#955).-    it "fails to dataize an empty formation, which dataizes ⊥" $ do-      expr <- parseExpressionThrows "[[ ]]"-      loc <- parseExpressionThrows "Q"-      dataize expr (defaultDataizeContext loc)-        `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))--  -- Every case below reaches its bytes without firing an atom, so none of them-  -- needs the registry: what they exercise is the calculus itself.-  testDataize-    [-      ( "Located"-      , "Q.foo.bar"-      , unlines-          [ "[["-          , "  foo -> [["-          , "    bar -> [["-          , "      @ -> Q.x"-          , "    ]]"-          , "  ]],"-          , "  x -> [[ D> 42- ]]"-          , "]]"-          ]-      , BtOne "42"-      )-    ,-      ( "Five"-      , "Q.x"-      , unlines-          [ "[["-          , "  number ↦ ⟦ φ ↦ ∅ ⟧,"-          , "  bytes ↦ ⟦ φ ↦ ∅ ⟧,"-          , "  x -> 5"-          , "]]"-          ]-      , BtMany ["40", "14", "00", "00", "00", "00", "00", "00"]-      )-    , -- Dispatching an absent attribute on a φ-decorated formation now resolves-      -- the inherited attribute through morphing 'mphi' (#973): PHI used to be a-      -- normalization rule, but following the decoration is a semantic 𝕄 step,-      -- so it moved into 'morphing.yaml'. Here '.t' is missing from the outer-      -- formation, so 𝕄 walks the '@' decoration to the parent that defines 't'-      -- and dataizes its datum.--      ( "InheritedThroughPhi"-      , "Q"-      , "[[ @ -> [[ t -> [[ D> 2A- ]] ]] ]].t"-      , BtOne "2A"-      )-    ]--  -- Which λ functions exist is no longer phino's business: the registry given-  -- with '--atoms' decides, and each one runs as an external script (see-  -- 'Atoms'). What the cases below assert is that the answer of such a script-  -- lands in the derivation exactly where a built-in atom's answer used to: 𝔼-  -- normalizes it and 𝔻 carries on. The λ functions themselves are the fixture-  -- ones (see 'Fixtures'), and 'number.eq' is composed out of 'L_bytes_eq' the-  -- way 'eq.eo' composes it, so the EO-level composition is exercised too.-  describe "atoms come from the registry" $ do-    testAtom-      registry-      [ ("adds two numbers", "5.plus( 6 )", BtMany ["40", "26", "00", "00", "00", "00", "00", "00"])-      , ("multiplies two numbers", "5.times( 6 )", BtMany ["40", "3E", "00", "00", "00", "00", "00", "00"])-      , -- Two firings in a row: 'ml' reduces the head of the second dispatch,-        -- which fires the first atom, before the second one is handed its own-        -- formation to fire against-        ("fires twice down a chain of dispatches", "5.plus( 6 ).plus( 7 )", BtMany ["40", "32", "00", "00", "00", "00", "00", "00"])-      , ("divides a positive dividend", "256.div( 16 )", BtMany ["40", "30", "00", "00", "00", "00", "00", "00"])-      , ("divides by zero into infinity", "2.div( 0 )", BtMany ["7F", "F0", "00", "00", "00", "00", "00", "00"])-      , ("tells 1000 is greater than 200", "1000.gt( 200 )", BtOne "FF")-      , ("tells 42 is not greater than 42.5", "42.gt( 42.5 )", BtOne "00")-      , ("tells zero is greater than a negative", "0.gt( -5 )", BtOne "FF")-      , ("tells 5 equals 5", "5.eq( 5 )", BtOne "FF")-      , ("tells 5 is not equal to 6", "5.eq( 6 )", BtOne "00")-      , ("inverts bytes", raw "CA-FE-BE-BE" ++ ".not", BtMany ["35", "01", "41", "41"])-      , ("tells equal bytes are equal", raw "CA-FE" ++ ".eq( " ++ raw "CA-FE" ++ " )", BtOne "FF")-      , ("tells different bytes are not equal", raw "CA-FE" ++ ".eq( " ++ raw "CA-FF" ++ " )", BtOne "00")-      ]--    -- A whole program, not a single operation: every atom on the way is an-    -- external script and the run still lands on the bytes EO's own-    -- 'Fahrenheit' example lands on-    it "dataizes a program whose every operation is an external atom" $-      withNode $ do-        expr <--          parseExpressionThrows-            ( unlines-                [ "[["-                , "  bytes -> [["-                , "    φ -> ?"-                , "  ]],"-                , "  number -> [["-                , "    φ -> ?,"-                , "    as-bytes -> $.φ,"-                , "    plus -> [[ x -> ?, L> L_number_plus ]],"-                , "    times -> [[ x -> ?, L> L_number_times ]]"-                , "  ]],"-                , "  @ -> $.c.times(1.8).plus(32),"-                , "  c -> 25"-                , "]]"-                ]-            )-        loc <- parseExpressionThrows "Q"-        (value, _) <- dataize expr (withAtoms registry (defaultDataizeContext loc))-        value `shouldBe` Dataized (BtMany ["40", "53", "40", "00", "00", "00", "00", "00"])--    -- A name the registry does not carry has no λ function at all: 𝔼 gets-    -- stuck on it, which is the only behaviour phino itself is left with-    it "gets stuck on a λ function the registry does not carry" $ do-      expr <- parseExpressionThrows (primitives "5.nope")-      loc <- parseExpressionThrows "Q"-      dataize expr (withAtoms registry (defaultDataizeContext loc))-        `shouldThrow` (\e -> "Atom 'L_number_nope' does not exist" `isInfixOf` show (e :: SomeException))--    -- An operand carrying no number is what an EO number atom answers ⊥ to, and-    -- dataizing ⊥ fails through the terminator path. The judgment is the-    -- script's now, so what these cases prove is that a ⊥ coming back from a-    -- script stops 𝔻 exactly as a built-in ⊥ used to.-    testStuckAtom-      registry-      [ ("cannot add a non-numeric operand", "5.plus( " ++ raw "--" ++ " )")-      , ("cannot multiply by a non-numeric operand", "5.times( " ++ raw "--" ++ " )")-      , ("cannot divide by a non-numeric divisor", "5.div( " ++ raw "--" ++ " )")-      , ("cannot compare against a non-numeric threshold", "5.gt( " ++ raw "--" ++ " )")-      , -- A byte array whose length is not 8 carries no number either (#1072)-        ("cannot add a 5-byte operand", "5.plus( " ++ raw "68-65-6C-6C-6F" ++ " )")-      , ("cannot multiply by a 2-byte operand", "5.times( " ++ raw "20-1F" ++ " )")-      ]

@@ -13,10 +13,13 @@ -- written for the occasion, either run once per fire or kept resident for the -- run. module Fixtures-  ( fixtureAtoms+  ( defaultReduceContext+  , fixtureAtoms   , fixtureRegistry+  , primitives   , resident   , withAskingRegistry+  , withAtoms   , withExecutable   , withFixtureRegistry   , withLoopingAskRegistry@@ -29,7 +32,8 @@   ) where -import Atoms (Registry, readRegistry)+import AST (Expression)+import Atoms (Registry, emptyRegistry, readRegistry) import Control.Exception (bracket) import Data.Aeson (Value, encode, object, (.=)) import Data.Aeson.Key qualified as Key@@ -38,10 +42,65 @@ import Data.Maybe (isNothing) import Data.Text qualified as T import Data.Text.Encoding (decodeUtf8, encodeUtf8)+import Dataize (reduction)+import Deps (dontSaveEval, dontSaveStep)+import Functions (buildTerm)+import Morph (ReduceContext (..), Steps (..)) import System.Directory (findExecutable, getPermissions, getTemporaryDirectory, removePathForcibly, setOwnerExecutable, setPermissions) import System.IO (Handle, hClose, openBinaryTempFile) import System.Info (os) import Test.Hspec (Expectation, pendingWith)++-- The context every reduction of a spec starts from. Shuffle is enabled so the+-- suite exercises the order-independence of the morphing and dataization rules+-- (#909): a hidden overlap surfaces as a nondeterministic failure instead of+-- staying silently green. The registry of λ functions is empty, since phino+-- implements none of them: a case that needs an atom to answer brings the+-- fixture registry in through 'withAtoms'.+defaultReduceContext :: Expression -> ReduceContext+defaultReduceContext loc = ReduceContext loc 25 25 (Steps 250 0) False True False False emptyRegistry buildTerm reduction dontSaveStep dontSaveEval++-- The same context with the fixture λ functions registered+withAtoms :: Registry -> ReduceContext -> ReduceContext+withAtoms registry ctx = ctx{_atoms = registry}++-- The EO objects the fixture λ functions answer for, declared the way+-- 'number.eo' and 'bytes.eo' declare them, so a case only has to spell the+-- expression under φ. 'number.eq' is the one operation with no atom of its+-- own: EO spells it out of 'L_bytes_eq' (eq.eo), so the fixture composes it the+-- same way. Alongside them stand the objects the atoms hand results to: 'string'+-- carries what a byte-array complaint would say, while 'true' and 'false' fill+-- in for the real bool objects, since the single byte an EO bool dataizes to is+-- all these cases assert. Those bytes are EO's own: 'true.eo' asserts+-- 'true.as-bytes.eq FF-' and 'bool.eo' branches 'if' over 'FF-' and '00-', so a+-- universe copied from here starts with a bool an EO program recognizes.+-- 'number.nope' is declared and left out of the registry on purpose: it is the+-- λ function that cannot fire, the one '--partial' parks on.+primitives :: String -> String+primitives src =+  unlines+    [ "[["+    , "  bytes -> [["+    , "    φ -> ?,"+    , "    not -> [[ L> L_bytes_not ]],"+    , "    eq -> [[ b -> ?, L> L_bytes_eq ]]"+    , "  ]],"+    , "  number -> [["+    , "    φ -> ?,"+    , "    as-bytes -> $.φ,"+    , "    plus -> [[ x -> ?, L> L_number_plus ]],"+    , "    times -> [[ x -> ?, L> L_number_times ]],"+    , "    div -> [[ x -> ?, L> L_number_div ]],"+    , "    gt -> [[ x -> ?, L> L_number_gt ]],"+    , "    eq -> [[ x -> ?, @ -> $.^.as-bytes.eq( x.as-bytes ) ]],"+    , "    nope -> [[ L> L_number_nope ]]"+    , "  ]],"+    , "  string -> [[ φ -> ?, as-bytes -> $.φ ]],"+    , "  true -> [[ @ -> [[ D> FF- ]] ]],"+    , "  false -> [[ @ -> [[ D> 00- ]] ]],"+    , "  @ -> " ++ src+    , "]]"+    ]  -- Every λ function the fixture answers for. A name outside this list is -- unregistered, which is how a spec asks for an atom that cannot fire.

@@ -0,0 +1,321 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE OverloadedRecordDot #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-}++-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++module MorphSpec (spec) where++import AST+import Atoms (Registry, emptyRegistry, readRegistry)+import Control.Exception (SomeException)+import Control.Monad+import Data.Aeson (FromJSON)+import Data.List (find, isInfixOf, nub)+import Data.List.NonEmpty (NonEmpty (..))+import Data.Maybe (fromMaybe)+import Data.Yaml qualified as Decode+import Dataize (Outcome (..), dataize)+import Deps (Term (TeExpression))+import Files (allPathsIn)+import Fixtures (defaultReduceContext, fixtureRegistry, primitives, withAtoms, withNode, withServing, withShell)+import GHC.Generics (Generic)+import Matcher (substEmpty)+import Morph (ReduceContext (..), emptyState, execBuildTerm, insideUniverse, morph, morph')+import Parser (parseExpressionThrows)+import Rewriter (Rewritten)+import Rule (RuleContext (RuleContext), matchExpressionWithRule')+import System.FilePath (makeRelative)+import Test.Hspec+import Yaml (ExtraArgument (..))+import Yaml qualified++test' :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> String -> ReduceContext -> IO ((a, NonEmpty Rewritten), String)) -> [(String, Expression, Expression, a)] -> Spec+test' func useCases =+  forM_ useCases $ \(desc, input, expr, output) ->+    it desc $ do+      ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultReduceContext ExRoot)+      res `shouldBe` output++-- One case of 𝕄, as a pack of 'test-resources/morph-packs' — or, for the deep+-- walk, of 'test-resources/morph-deep-packs' — spells it: the program under+-- 'input', wrapped in the fixture object model where 'model' says so and run+-- against the fixture λ functions where 'atoms' does, entered at 'location' and+-- answering either the program under 'result' or the failure under 'fails'.+data MorphPack = MorphPack+  { location :: Maybe String+  , input :: String+  , model :: Maybe Bool+  , atoms :: Maybe Bool+  , partial :: Maybe Bool+  , result :: Maybe String+  , fails :: Maybe String+  }+  deriving (Generic, Show, FromJSON)++-- Morph one such pack and check what it answers, walking every binding where+-- 'deep' says so, since that is what tells the two pack directories apart. A+-- pack that registers the fixture λ functions fires one under 'node', so it is+-- pending where 'node' is not installed.+testMorph :: Registry -> Bool -> FilePath -> Expectation+testMorph registry deep pth = do+  MorphPack{..} <- Decode.decodeFileThrow pth+  expr <- parseExpressionThrows (if model == Just True then primitives input else input)+  loc <- parseExpressionThrows (fromMaybe "Q" location)+  let ctx =+        (defaultReduceContext loc)+          { _deep = deep+          , _partial = partial == Just True+          , _atoms = if atoms == Just True then registry else emptyRegistry+          }+      checked :: Expectation+      checked = case (result, fails) of+        (Just res, Nothing) -> do+          expected <- parseExpressionThrows res+          (morphed, _) <- morph expr ctx+          morphed `shouldBe` expected+        (Nothing, Just message) ->+          morph expr ctx `shouldThrow` (\err -> message `isInfixOf` show (err :: SomeException))+        _ -> expectationFailure "The pack holds neither a single 'result' nor a single 'fails'"+  if atoms == Just True then withNode checked else checked++spec :: Spec+spec = do+  -- Every λ function a case may fire comes from the fixture registry, read+  -- once here: phino carries none of its own (see 'Fixtures').+  registry <- runIO fixtureRegistry++  -- The top-level 𝕄 entry point, the one the 'morph' command runs: it locates+  -- the subterm, threads the whole input expression as the universe and hands+  -- back the morphed expression together with the chain that led to it (#1114).+  describe "morph" $ do+    let resources = "test-resources/morph-packs"+    packs <- runIO (allPathsIn resources)+    forM_ packs (\pth -> it (makeRelative resources pth) (testMorph registry False pth))++    -- The chain runs oldest step first and carries the rule that produced the+    -- step after it, exactly as 'dataize' reports its own, so '--sequence'+    -- prints both the same way+    it "reports the chain of steps oldest first" $ do+      expr <- parseExpressionThrows "[[ D> 00- ]]"+      (morphed, chain) <- morph expr (defaultReduceContext ExRoot)+      morphed `shouldBe` expr+      map snd chain `shouldBe` [Just "mf", Nothing]+      map fst chain `shouldBe` [expr, expr]++  -- 𝕄 stops at the first formation 'mf' hands back and leaves its bindings as+  -- they were written, since firing a bare λ is 𝔻's business, so a program+  -- whose parts nothing demands is never reduced (#1124). The deep walk+  -- ('_deep') enters every binding and finishes what 'mf' left, while what no+  -- atom touched keeps the shape it was written in and the answer stays a+  -- program.+  describe "morph with '_deep'" $ do+    let resources = "test-resources/morph-deep-packs"+    packs <- runIO (allPathsIn resources)+    forM_ packs (\pth -> it (makeRelative resources pth) (testMorph registry True pth))++    -- The walk enters a dispatch through its target and fires the box it finds+    -- there before 𝕄 is ever asked about the dispatch, while 'ml' demands that+    -- λ only where the dispatched attribute is none of the box's own (#1187)+    describe "a dispatch naming an attribute of the formation it stands on" $+      it "cannot fire the λ the dispatch does not demand" $+        withShell $+          withServing "printf '{\"id\": %s, \"𝑛\": \"⟦ Δ ⤍ FF- ⟧\"}\\n' \"$id\"" $ \path -> do+            box <- readRegistry path+            world <- parseExpressionThrows "[[ foo -> [[ f -> [[ a -> ?, @ -> $.a, L> L_answer ]] ]], x -> Q.foo.f( a -> [[ D> 01- ]] ).@ ]]"+            (morphed, _) <- morph world (withAtoms box (defaultReduceContext ExRoot)){_deep = True}+            morphed `shouldBe` world++  describe "morph'" $+    test'+      morph'+      [ ("[[ D> 00- ]] => [[ D> 00- ]]", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")])+      , ("T => T", ExTermination, ExRoot, ExTermination)+      , ("$ => X", ExXi, ExRoot, ExTermination)+      , ("Q => X", ExRoot, ExRoot, ExTermination)+      ,+        ( "Q.x (Q -> [[ x -> [[]] ]]) => [[ ρ -> Q ]]"+        , ExDispatch ExRoot (AtLabel "x")+        , ExFormation [BiTau (AtLabel "x") (ExFormation [])]+        , ExFormation [BiTau AtRho (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho])]+        )+      , -- A void slot fed a non-absolute argument can never be filled, so 'copy'+        -- cannot fire and the application is a stuck normal form. Before #959,+        -- 'ma' re-morphed this identical term forever; now the 'mad' axiom+        -- morphs it straight to ⊥, keeping 𝕄 total.++        ( "[[ x -> ? ]](x -> $.foo) => T"+        , ExApplication (ExFormation [BiVoid (AtLabel "x")]) (ArTau (AtLabel "x") (ExDispatch ExXi (AtLabel "foo")))+        , ExRoot+        , ExTermination+        )+      , -- Same as above but through the alpha-argument sibling 'maad' instead of+        -- 'mad': a void slot fed a non-absolute alpha-indexed argument also+        -- morphs straight to ⊥.++        ( "[[ ^ -> ? ]](α0 -> $.foo) => T"+        , ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) (ExDispatch ExXi (AtLabel "foo")))+        , ExRoot+        , ExTermination+        )+      , -- 'universe' fires only when the universe 'e' differs from Φ itself+        -- ('not (eq(e, Φ))'); it then normalizes and re-morphs that universe.+        -- Here the universe is a plain formation, already a normal form, so+        -- re-morphing it lands straight on 'mf' and returns it unchanged.++        ( "Q => [[]] (a universe distinct from Φ) => [[]]"+        , ExRoot+        , ExFormation []+        , ExFormation []+        )+      ]++  -- 𝕄's first argument is always a normal form reachable through normalization,+  -- and every such normal form is covered by some morphing clause (an axiom+  -- like 'mf'/'dead'/'xi'/'universe'/'mg' or a recursive rule), so the "no rule+  -- matched" fallback never fires along any real derivation. It is still total+  -- code, reachable by calling 'morph'' directly (bypassing normalization) on a+  -- raw meta 𝑛, an AST node the matcher never binds to any concrete pattern.+  describe "morph' fails when no morphing rule matches the term" $+    it "throws instead of looping when handed a bare, unmatched meta" $+      morph' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)+        `shouldThrow` (\e -> "no morphing rule matched" `isInfixOf` show (e :: SomeException))++  -- 'execBuildTerm's "evaluate" and "morph" cases expose 𝔼 and 𝕄 to the+  -- matcher's condition path (guards in 'when'/'having'). No built-in rule's+  -- guard actually calls either function, so these error paths — reachable only+  -- by malformed arguments — are exercised here directly through the exported+  -- 'execBuildTerm', the same way the matcher would call it.+  describe "execBuildTerm 'evaluate'" $ do+    let univ = ExFormation []+        ctx = withAtoms registry (defaultReduceContext ExRoot)+        runEvaluate args = execBuildTerm univ ctx "evaluate" args substEmpty+    forM_+      [+        ( "the first argument is not a formation"+        , [ArgExpression ExRoot, ArgExpression univ]+        , "Function evaluate() expects a formation"+        )+      ,+        ( "the formation has no λ binding at all"+        , [ArgExpression (ExFormation []), ArgExpression univ]+        , "expects a formation with a"+        )+      ,+        ( "a non-λ formation still has other bindings"+        , [ArgExpression (ExFormation [BiVoid AtRho]), ArgExpression univ]+        , "expects a formation with a"+        )+      ,+        ( "not given exactly two expression arguments"+        , [ArgExpression univ]+        , "requires exactly 2 expression arguments"+        )+      ]+      ( \(desc, args, message) ->+          it ("throws when " ++ desc) $+            runEvaluate args `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException))+      )+    it "evaluates a λ-bearing formation to the atom's normalized result" $+      withNode $ do+        let form = ExFormation [BiLambda (Function "L_bytes_not"), BiTau AtRho (ExFormation [BiDelta (BtOne "00")])]+        result <- runEvaluate [ArgExpression form, ArgExpression univ]+        case result of+          TeExpression expr -> expr `shouldBe` dataBytes (BtOne "FF")+          _ -> expectationFailure "expected TeExpression"++  describe "execBuildTerm 'morph'" $ do+    let univ = ExFormation []+        ctx = defaultReduceContext ExRoot+    it "throws when not given exactly one expression argument" $+      execBuildTerm univ ctx "morph" [] substEmpty+        `shouldThrow` (\e -> "requires exactly 1 expression argument" `isInfixOf` show (e :: SomeException))+    it "morphs a single expression argument to its already-normal form" $ do+      result <- execBuildTerm univ ctx "morph" [ArgExpression (ExFormation [BiDelta (BtOne "00")])] substEmpty+      case result of+        TeExpression expr -> expr `shouldBe` ExFormation [BiDelta (BtOne "00")]+        _ -> expectationFailure "expected TeExpression"++  -- An expression that is not part of the program — the operand an atom script+  -- asks phino to reduce — is bound to a synthetic attribute of the universe and+  -- that attribute is what 𝔻 is aimed at. This is what the '--inside' option+  -- runs, and what phino did internally while the atoms still lived in the+  -- binary.+  describe "insideUniverse" $ do+    let universe = "[[ y -> [[ D> 02- ]] ]]"+        reduced src = do+          univ <- parseExpressionThrows universe+          target <- parseExpressionThrows src+          (extended, ctx) <- insideUniverse target univ (defaultReduceContext ExRoot)+          fst <$> dataize extended ctx+    it "reduces an expression the program does not contain" $ do+      value <- reduced "Q.y"+      value `shouldBe` Dataized (BtOne "02")+    -- 𝔻 accepts normal forms only, and a dispatch off a formation is not one:+    -- 'dot' still applies to it. So the expression is normalized first, which+    -- is the whole reason an atom script cannot simply splice it into the+    -- universe itself.+    it "normalizes what it is handed before 𝔻 sees it" $ do+      value <- reduced "[[ x -> [[ D> 01- ]] ]].x"+      value `shouldBe` Dataized (BtOne "01")+    it "refuses a universe which is not a formation" $ do+      target <- parseExpressionThrows "Q.y"+      insideUniverse target ExRoot (defaultReduceContext ExRoot)+        `shouldThrow` (\e -> "not a formation" `isInfixOf` show (e :: SomeException))++  -- 'defaultReduceContext' runs with '_shuffle' on, so 'morph'' walks the+  -- morphing rules in a random order on every step. Every clause is+  -- order-independent (the known overlaps were removed in #856 and #860), so the+  -- outcome must never depend on that order: morphing each input many times under+  -- a shuffling context yields exactly the formation the fixed declaration order+  -- does, proving the rules may be applied in any order with the same result.+  -- Were a hidden overlap re-introduced, some of these random orders would+  -- disagree and 'nub' would collect more than the single expected form.+  describe "morphing is order-independent under --shuffle" $ do+    let cases =+          [ ("a byte formation", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")])+          , ("termination", ExTermination, ExRoot, ExTermination)+          , ("xi", ExXi, ExRoot, ExTermination)+          , ("the global object", ExRoot, ExRoot, ExTermination)+          ,+            ( "a dispatch over a formation"+            , ExDispatch ExRoot (AtLabel "x")+            , ExFormation [BiTau (AtLabel "x") (ExFormation [])]+            , ExFormation [BiTau AtRho (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho])]+            )+          ]+    forM_ cases $ \(desc, input, univ, expected) ->+      it ("morphs " ++ desc ++ " to the same form across 100 random rule orders") $ do+        results <- replicateM 100 (fst . fst <$> morph' (input, (univ, Nothing) :| []) univ emptyState (defaultReduceContext ExRoot))+        nub results `shouldBe` [expected]++  -- 'md' fires only when its head is not a formation ('not (formation 𝑛)'),+  -- so a formation head — λ-bearing or not — is left to 'ml'/'mf'. The+  -- two clauses are mutually exclusive and their order in 'resources/morphing'+  -- cannot change behavior.+  describe "morphing 'md' is disjoint from 'ml'" $ do+    let rctx = RuleContext (execBuildTerm ExRoot (defaultReduceContext ExRoot))+        morphRule :: String -> Yaml.MorphRule+        morphRule nm = fromMaybe (error ("no morphing rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.morphingRules)+        asRule :: Yaml.MorphRule -> Yaml.Rule+        asRule r = Yaml.Rule r.name Nothing Nothing r.match ExRoot r.when Nothing Nothing+        lambdaFormation = ExFormation [BiLambda (Function "L_dummy"), BiVoid AtRho]+    it "does not fire on a λ-bearing formation dispatch" $ do+      substs <- matchExpressionWithRule' [substEmpty] (ExDispatch lambdaFormation (AtLabel "x")) (asRule (morphRule "md")) rctx+      substs `shouldBe` []+    it "still fires on a non-λ-formation dispatch" $ do+      substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (morphRule "md")) rctx+      null substs `shouldBe` False+    -- ⟦λ ⤍ F⟧.a.b.c : 'md' peels .c then .b (their heads are dispatches,+    -- not λ-formations, so 'λ ∉ 𝐵' holds), then 'ml' handles the base+    -- ⟦λ ⤍ F⟧.a and fires the atom. The chain therefore routes+    -- md → md → ml; firing the undefined atom 'F' is what+    -- raises the error, proving the base λ-formation reached 'ml'.+    it "drills a chained λ-formation dispatch down to the base 'ml'" $ do+      let base = ExFormation [BiLambda (Function "F")]+          chain = ExDispatch (ExDispatch (ExDispatch base (AtLabel "a")) (AtLabel "b")) (AtLabel "c")+      morph' (chain, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)+        `shouldThrow` (\e -> "Atom 'F' does not exist" `isInfixOf` show (e :: SomeException))

@@ -10,7 +10,7 @@ import Control.Exception (Exception (displayException), SomeException) import Control.Monad import Data.Either (isLeft)-import Data.List (isInfixOf, nub, (\\))+import Data.List (isInfixOf, nub, sort, (\\)) import Data.Maybe (fromMaybe) import Data.Text qualified as T import Data.Text.Encoding (encodeUtf8)@@ -183,6 +183,24 @@               ++ map (\DataizeRule{name, label} -> fromMaybe name label) dataizationRules               ++ map (\ContextualizeRule{name, label} -> fromMaybe name label) contextualizationRules       (labels \\ nub labels) `shouldBe` []++  describe "keeps one rule per file in every rule directory" $ do+    -- Each judgment lives in its own directory, one YAML per rule, embedded+    -- wholesale by 'embedDir', which sorts by path. The clauses of a judgment+    -- are disjoint, so nothing orders them and a file is named after the rule+    -- it carries and nothing else. Compare the directory listing against the+    -- embedded rule set, position by position.+    let named :: FilePath -> IO [String]+        named dir = map takeBaseName . sort . filter ((== ".yaml") . takeExtension) <$> allPathsIn dir+    morphed <- runIO (named "resources/morphing")+    dataized <- runIO (named "resources/dataization")+    contextualized <- runIO (named "resources/contextualization")+    it "names one morphing file after every morphing rule" $+      morphed `shouldBe` map (\MorphRule{name} -> name) morphingRules+    it "names one dataization file after every dataization rule" $+      dataized `shouldBe` map (\DataizeRule{name} -> name) dataizationRules+    it "names one contextualization file after every contextualization rule" $+      contextualized `shouldBe` map (\ContextualizeRule{name} -> name) contextualizationRules    describe "reserves 𝑛-family metas for normal forms" $     -- 𝒞 ('contextualize') returns an expression that is not necessarily a normal