phino 0.0.116 → 0.0.117

raw patch · 44 files changed

+2130/−988 lines, 44 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +164/−28
• phino.cabal +6/−1
• resources/contextualization.yaml +28/−26
• resources/dataization.yaml +35/−33
• resources/morphing.yaml +54/−52
• resources/normalize/alpha.yaml +3/−3
• resources/normalize/amiss.yaml +3/−3
• resources/normalize/copy.yaml +2/−2
• resources/normalize/dot.yaml +12/−12
• resources/normalize/miss.yaml +3/−3
• resources/normalize/null.yaml +1/−1
• resources/normalize/over.yaml +2/−2
• resources/normalize/overa.yaml +3/−3
• resources/normalize/stop.yaml +5/−5
• src/AST.hs +25/−0
• src/Atoms.hs +261/−0
• src/Builder.hs +36/−10
• src/Bytes.hs +2/−0
• src/CLI/Helpers.hs +30/−0
• src/CLI/Parsers.hs +40/−1
• src/CLI/Runners.hs +20/−4
• src/CLI/Types.hs +7/−0
• src/CST.hs +14/−0
• src/Condition.hs +1/−1
• src/Dataize.hs +45/−134
• src/Matcher.hs +33/−11
• src/Misc.hs +4/−0
• src/Parser.hs +32/−31
• src/Printer.hs +9/−1
• src/Rewriter.hs +1/−0
• src/Rule.hs +39/−28
• src/Slots.hs +65/−0
• src/Yaml.hs +117/−28
• test/AtomsSpec.hs +154/−0
• test/BuilderSpec.hs +33/−1
• test/CLISpec.hs +289/−198
• test/ConditionSpec.hs +7/−7
• test/DataizeSpec.hs +245/−292
• test/Fixtures.hs +72/−0
• test/FunctionsSpec.hs +7/−7
• test/MatcherSpec.hs +50/−12
• test/ParserSpec.hs +57/−34
• test/PrinterSpec.hs +10/−10
• test/YamlSpec.hs +104/−4

@@ -100,6 +100,117 @@ 68-65-6C-6C-6F ``` +### Atoms++Which λ functions exist is a property of the object model being dataized, not+of the calculus, so `phino` implements none of them. They come from a JSON+registry given with `--atoms`, keyed by λ name:++```json+{+  "L_number_plus": {+    "rt": "node",+    "script": "const fs = require('fs'); ..."+  }+}+```++The `rt` field names the executable the `script` is run under. Only `node` is+supported for now; a registry naming any other runtime is refused when the file+is read, before dataization starts.++When 𝔼 reaches a λ function the registry carries, `phino` writes its `script`+to a temporary file and runs it as a POSIX process under that interpreter, with+the λ name as the first command-line argument:++```text+node /tmp/phino-atom-4f2a.js L_number_plus+```++The name matters: one script may be registered under several λ names and branch+on it, which is where `node` puts it — `process.argv[2]`. The script is then+fed one JSON object on `stdin`:++```json+{+  "b": "⟦ x ↦ Φ.number( as-bytes ↦ … ), ρ ↦ ⟦ … ⟧ ⟧",+  "s": "⟦ bytes ↦ ⟦ … ⟧, number ↦ ⟦ … ⟧, φ ↦ … ⟧"+}+```++Here `b` is the formation being evaluated, with its λ binding removed so that+the script may dispatch on it, and `s` is the universe Φ. Both are canonical+𝜑-calculus on a single line — no syntax sugar, whatever `--sweet` says about+the output of the run — so a script never has to know about `phino`'s sugar in+order to find a datum: every byte array is spelled out as a Δ binding.++The script writes one JSON object to `stdout`:++```json+{ "n": "11" }+```++The `n` field is the 𝜑-expression the atom answers with, in any syntax+`phino`'s parser reads — syntax sugar included, so the `11` above and the+`Φ.number( … )` it stands for are the same answer. `phino` parses it back+and hands it to 𝔼 as the atom's raw result, normalizing it exactly as it+normalizes anything else, so `--evaluations`, `--partial` and `--max-steps`+keep working unchanged. A non-zero exit, output that is not JSON, a missing+`n` or an `n` that does not parse fails the run, with the script's own+`stderr` in the message.++A λ name the registry does not carry has no λ function at all, so 𝔼 gets stuck+on it. Without `--atoms` the registry is empty and every atom gets stuck.++### Reducing the operands of an atom++A script gets at the parts of `b` by calling `phino` again, so no API has to be+exposed for it. The `--inside` option is how it asks: the expression it names+is bound to a fresh synthetic attribute of the input expression, which the run+takes as the universe, normalized there, and then dataized. This is the same+trick `phino` plays internally whenever it has to reduce a sub-expression the+program does not contain:++```bash+$ phino dataize --atoms=atoms.json --inside='5.plus( 6 )' universe.phi+40-26-00-00-00-00-00-00+```++Here `universe.phi` is the 𝜑-program the atom is being fired inside — the very+text the script was handed as `s`, which it feeds back on `stdin`.++So a `L_number_plus` that reduces its own operands reads like this:++```js+const fs = require('fs');+const { execFileSync } = require('child_process');+const atom = process.argv[2];+if (atom !== 'L_number_plus') {+  throw new Error(`unsupported atom ${atom}`);+}+const { b, s } = JSON.parse(fs.readFileSync(0, 'utf8'));+const dataized = (expr) => execFileSync(+  'phino',+  ['dataize', '--atoms=atoms.json', `--inside=${expr}`],+  { input: s, encoding: 'utf8' }+).trim();+const number = (expr) => Buffer.from(dataized(expr).replace(/-/g, ''), 'hex').readDoubleBE(0);+const sum = Buffer.alloc(8);+sum.writeDoubleBE(number(`${b}.ρ`) + number(`${b}.x`));+const hex = [...sum]+  .map((octet) => octet.toString(16).toUpperCase().padStart(2, '0'))+  .join('-');+process.stdout.write(JSON.stringify({+  n: `Φ.number( as-bytes ↦ Φ.bytes( data ↦ ⟦ Δ ⤍ ${hex} ⟧ ) )`+}));+```++The `--inside` option cannot be combined with `--locator`, since it aims the+run at the binding it mints itself. Both `dataize` and `morph` take `--atoms`+and `--inside`.++### Recording what fired+ Every atom fired on the way to the bytes may be recorded in a machine-readable protocol, with the `--evaluations` option. One firing is one line of three tab-separated fields: the name of the λ function, the formation it was applied@@ -112,7 +223,8 @@   number(as-bytes) ↦ ⟦ φ ↦ as-bytes, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧,   φ ↦ 5.plus( 6 ) ⟧-$ phino dataize --evaluations=atoms.tsv --quiet --sweet --hide-rho sum.phi+$ phino dataize --atoms=atoms.json --evaluations=atoms.tsv --quiet \+    --sweet --hide-rho sum.phi $ cat -T atoms.tsv L_number_plus^I⟦ x ↦ 6 ⟧^I11 ```@@ -122,14 +234,16 @@ beginning of every run, and `--output=phi` is the only output format it works with, since one record must fit into one line. -An atom that cannot fire fails the run: its λ function is unknown to phino,-or one of its inputs reaches such an atom. This is what happens when a-data input is replaced on purpose by a placeholder formation, such as-`⟦ λ ⤍ Sym_arg_0 ⟧`. With `--partial`, dataization becomes partial-evaluation instead: what the known inputs decide is computed, the rest-survives as the residual program, which is printed in place of the bytes,-and the run ends successfully:+### Partial evaluation +An atom that cannot fire fails the run: its λ function is not in the registry+given with `--atoms`. This is what happens when an operation is deliberately+left unimplemented — a data input replaced by a placeholder formation such as+`⟦ λ ⤍ Sym_arg_0 ⟧`, or an operation whose answer is not known yet. With+`--partial`, dataization becomes partial evaluation instead: what the known+inputs decide is computed, the rest survives as the residual program, which is+printed in place of the bytes, and the run ends successfully:+ ```bash $ cat partial.phi ⟦@@ -137,29 +251,29 @@   number(as-bytes) ↦ ⟦     φ ↦ as-bytes,     plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧,-    times(x) ↦ ⟦ λ ⤍ L_number_times ⟧+    times(x) ↦ ⟦ λ ⤍ L_number_times ⟧,+    as-bool ↦ ⟦ λ ⤍ L_number_as_bool ⟧   ⟧,-  φ ↦ 2.times(3).plus(⟦ λ ⤍ Sym_arg_0 ⟧)+  φ ↦ 2.times( 3 ).plus( 4 ).as-bool ⟧-$ phino dataize --partial --sweet --hide-rho partial.phi-⟦ x ↦ ⟦ λ ⤍ Sym_arg_0 ⟧, λ ⤍ L_number_plus ⟧+$ phino dataize --atoms=atoms.json --partial --sweet --hide-rho partial.phi+⟦ λ ⤍ L_number_as_bool ⟧ ``` -Here `2.times(3)` was decided by literals, so it was computed (its result,-`6`, sits in the hidden `ρ` of the residual program), while `plus` waits-for an `x` no atom can produce, so it stays in place as a normal-form-subterm. Each such stuck site also lands in the `--evaluations` file, as a-record with the first two fields only, since there is no result to report;-the inner stuck atom comes first, then the known atom whose input reached-it:+Here `2.times( 3 ).plus( 4 )` was decided by the atoms the registry carries, so+it was computed (its result, `10`, sits in the hidden `ρ` of the residual+program), while `as-bool` names a λ function no script answers for, so it stays+in place as a normal-form subterm. Each such stuck site also lands in the+`--evaluations` file, as a record with the first two fields only, since there is+no result to report:  ```bash-$ phino dataize --partial --evaluations=atoms.tsv --quiet \+$ phino dataize --atoms=atoms.json --partial --evaluations=atoms.tsv --quiet \     --sweet --hide-rho partial.phi $ cat -T atoms.tsv L_number_times^I⟦ x ↦ 3 ⟧^I6-Sym_arg_0^I⟦⟧-L_number_plus^I⟦ x ↦ ⟦ λ ⤍ Sym_arg_0 ⟧ ⟧+L_number_plus^I⟦ x ↦ 4 ⟧^I10+L_number_as_bool^I⟦⟧ ```  Evaluation stays demand-driven, as the calculus prescribes: an argument@@ -193,9 +307,9 @@   number(as-bytes) ↦ ⟦ φ ↦ as-bytes, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧,   φ ↦ 5.plus( 6 ).plus( 7 ) ⟧-$ phino dataize --sweet --hide-rho two.phi+$ phino dataize --atoms=atoms.json --sweet --hide-rho two.phi 40-32-00-00-00-00-00-00-$ phino morph --locator=Q.φ --sweet --hide-rho two.phi+$ phino morph --atoms=atoms.json --locator=Q.φ --sweet --hide-rho two.phi ⟦ x ↦ 7, λ ⤍ L_number_plus ⟧ ``` @@ -214,9 +328,9 @@ ⊥ ``` -The whole `dataize` option surface applies unchanged — `--sequence`,-`--headers`, `--steps-dir`, `--evaluations`, `--partial`, `--max-steps`,-`--shuffle`/`--seed`, `--output`, `--focus` and the rest.+The whole `dataize` option surface applies unchanged — `--atoms`, `--inside`,+`--sequence`, `--headers`, `--steps-dir`, `--evaluations`, `--partial`,+`--max-steps`, `--shuffle`/`--seed`, `--output`, `--focus` and the rest.  ## Rewrite @@ -550,7 +664,29 @@ * `!d` || `δ` - bytes in meta delta binding * `!F` || `𝑓` - function name in meta lambda binding -Every meta variable may also be used with an integer index, like `!B1` or `𝜏0`.+A meta variable carries a suffix, like `!B1` or `𝜏0`, to name what it+captured, so that the `result`, `when`, `where` and `having` of a rule can+read it back.++Written bare, with no suffix at all, a meta variable is anonymous: it matches+whatever term stands in its place, every occurrence on its own, and binds no+name. Two anonymous metas of one kind are therefore two different captures,+which is what lets a pattern ask for any two attributes without inventing+names for them:++```yaml+name: two-attributes+pattern: '⟦ 𝜏 ↦ 𝑒, 𝜏 ↦ 𝑒 ⟧'+result: '⟦ x ↦ ⟦ Δ ⤍ 2A- ⟧ ⟧'+```++Spelled with suffixes, that pattern would read `⟦ 𝜏1 ↦ 𝑒1, 𝜏2 ↦ 𝑒2 ⟧` and+name four captures the result never mentions, while `⟦ 𝜏1 ↦ 𝑒1, 𝜏1 ↦ 𝑒1 ⟧`+would be rejected as a duplicated attribute.++Nothing can refer to an anonymous meta, since it has no name to be referred to+by. Writing one outside a `pattern` (or the `match`, `e-match` and `c-match` of+an inference rule) is a mistake in the rule and is reported as the rule loads.  A positional (α) application argument is written as `α0`, `~0` (ASCII), or `α𝑖`/`~!i` when its index is captured by an `!i`/`𝑖` meta variable.

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.116+version: 0.0.117 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>@@ -35,6 +35,7 @@   import: warnings   exposed-modules:     AST+    Atoms     Builder     Bytes     Canonizer@@ -69,6 +70,7 @@     Replacer     Rewriter     Rule+    Slots     Sugar     Tau     XMIR@@ -94,6 +96,7 @@     gitrev >=1.3.1 && <1.4,     megaparsec >=9.5 && <9.9,     optparse-applicative >=0.18 && <0.20,+    process >=1.6.17 && <1.7,     random >=1.2 && <1.4,     regex-pcre-builtin >=0.95.2 && <0.96,     scientific >=0.3.7 && <0.4,@@ -125,6 +128,7 @@   hs-source-dirs: test   other-modules:     ASTSpec+    AtomsSpec     BuilderSpec     BytesSpec     CanonizerSpec@@ -138,6 +142,7 @@     EncodingSpec     FilesSpec     FilterSpec+    Fixtures     FunctionsSpec     LaTeXSpec     LiningSpec

@@ -17,63 +17,65 @@ # '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 c meta. Derived terms are named 𝑛, 𝑛1, … in premise order; the bare 𝑛 is-# skipped only when 'match' already binds it.+# 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: 𝑘+  c-match: 𝑘0   c-result: Φ  - name: cxi   match: ξ-  c-match: 𝑘-  c-result: 𝑘+  c-match: 𝑘0+  c-result: 𝑘0  - name: ct   match: ⊥-  c-match: 𝑘+  c-match: 𝑘0   c-result: ⊥  - name: cf-  match: ⟦𝐵⟧-  c-match: 𝑘-  c-result: ⟦𝐵⟧+  match: ⟦𝐵0⟧+  c-match: 𝑘0+  c-result: ⟦𝐵0⟧  - name: cd-  match: '𝑛.𝜏'-  c-match: 𝑘-  c-result: '𝑛1.𝜏'+  match: '𝑛0.𝜏0'+  c-match: 𝑘0+  c-result: '𝑛1.𝜏0'   premises:     - n-result: 𝑛1       contextualize:-        - 𝑛-        - 𝑘+        - 𝑛0+        - 𝑘0  - name: ca-  match: '𝑛(𝜏 ↦ 𝑒1)'-  c-match: 𝑘-  c-result: '𝑛1(𝜏 ↦ 𝑛2)'+  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: '𝑛(α𝑖 ↦ 𝑒1)'-  c-match: 𝑘-  c-result: '𝑛1(α𝑖 ↦ 𝑛2)'+  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

@@ -14,19 +14,21 @@ # 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 e meta. The single bytes result is named δ. A+# 𝔻(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, … in premise order, skipping the bare 𝑛 only when 'match' already binds-# it; 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', 𝑒 itself being the universe)-# rather than an 𝑛 name reserved for normal forms.+# 𝑛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 bare meta 𝑛, which unifies with any expression, so it is-# guarded to fire only when 𝑛 is neither a formation ('not (formation 𝑛)',+# '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 (𝑛 = ⊥)'). 𝔻 is partial: ⊥ (the terminator T) signals an error and+# ('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;@@ -34,14 +36,14 @@  - name: delta   label: \Delta-  match: ⟦𝐵1, Δ ⤍ δ, 𝐵2⟧-  e-match: 𝑒-  d-result: δ+  match: ⟦𝐵1, Δ ⤍ δ0, 𝐵2⟧+  e-match: 𝑒0+  d-result: δ0  - name: box   match: ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧-  e-match: 𝑒-  d-result: δ+  e-match: 𝑒0+  d-result: δ0   when:     disjoint:       - [Δ, λ]@@ -53,47 +55,47 @@         - ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧     - n-result: 𝑛1       normalize: 𝑒2-    - d-result: δ+    - d-result: δ0       dataize: 𝑛1  - name: fire-  match: ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧-  e-match: 𝑒-  d-result: δ+  match: ⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧+  e-match: 𝑒0+  d-result: δ0   premises:     - n-result: 𝑛1       evaluate:-        - ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧-        - 𝑒-    - d-result: δ+        - ⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧+        - 𝑒0+    - d-result: δ0       dataize: 𝑛1  - name: none-  match: ⟦𝐵⟧-  e-match: 𝑒-  d-result: δ+  match: ⟦𝐵0⟧+  e-match: 𝑒0+  d-result: δ0   when:     disjoint:       - [Δ, λ, φ]-      - [𝐵]+      - [𝐵0]   premises:-    - d-result: δ+    - d-result: δ0       dataize: ⊥  - name: norm-  match: 𝑛-  e-match: 𝑒-  d-result: δ+  match: 𝑛0+  e-match: 𝑒0+  d-result: δ0   when:     and:       - not:-          formation: 𝑛+          formation: 𝑛0       - not:           eq:-            - 𝑛+            - 𝑛0             - ⊥   premises:     - n-result: 𝑛1-      morph: 𝑛-    - d-result: δ+      morph: 𝑛0+    - d-result: δ0       dataize: 𝑛1

@@ -18,24 +18,26 @@ # '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 e meta, but a rule may+# 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 results are named 𝑛, 𝑛1, … in premise order, the-# bare 𝑛 skipped only when 'match' already binds it; the 𝑒-family stays reserved-# for the universe 𝑒 itself.+# 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 𝑛 is not a formation ('not (formation 𝑛)'), so every formation+# 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 '𝑘' argument — absolute (xi-free) and in normal+# 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-# '𝑛' argument (a normal form) that is 'not (absolute 𝑛1)' and yield ⊥+# '𝑛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@@ -46,91 +48,91 @@ # re-morphed the identical stuck term forever.  - name: mf-  match: ⟦𝐵⟧-  e-match: 𝑒-  n-result: ⟦𝐵⟧+  match: ⟦𝐵0⟧+  e-match: 𝑒0+  n-result: ⟦𝐵0⟧  - name: ml   label: \lambda-  match: '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧.𝜏'-  e-match: 𝑒+  match: '⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧.𝜏0'+  e-match: 𝑒0   n-result: 𝑛3   premises:     - n-result: 𝑛1       evaluate:-        - '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧'-        - 𝑒+        - '⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧'+        - 𝑒0     - n-result: 𝑛2-      normalize: '𝑛1.𝜏'+      normalize: '𝑛1.𝜏0'     - n-result: 𝑛3       morph: 𝑛2  - name: mphi   label: \varphi-  match: ⟦𝐵⟧.𝜏-  e-match: 𝑒-  n-result: 𝑛1+  match: ⟦𝐵0⟧.𝜏0+  e-match: 𝑒0+  n-result: 𝑛2   when:     and:       - in:           - φ-          - 𝐵+          - 𝐵0       - not:           in:-            - 𝜏-            - 𝐵+            - 𝜏0+            - 𝐵0       - not:           in:             - λ-            - 𝐵+            - 𝐵0   premises:-    - n-result: 𝑛-      normalize: ⟦𝐵⟧.φ.𝜏     - n-result: 𝑛1-      morph: 𝑛+      normalize: ⟦𝐵0⟧.φ.𝜏0+    - n-result: 𝑛2+      morph: 𝑛1  - name: md-  match: '𝑛.𝜏'-  e-match: 𝑒+  match: '𝑛0.𝜏0'+  e-match: 𝑒0   n-result: 𝑛3   when:     not:-      formation: 𝑛+      formation: 𝑛0   premises:     - n-result: 𝑛1-      morph: 𝑛+      morph: 𝑛0     - n-result: 𝑛2-      normalize: '𝑛1.𝜏'+      normalize: '𝑛1.𝜏0'     - n-result: 𝑛3       morph: 𝑛2  - name: ma-  match: '𝑛(𝜏 ↦ 𝑘1)'-  e-match: 𝑒+  match: '𝑛0(𝜏0 ↦ 𝑘1)'+  e-match: 𝑒0   n-result: 𝑛3   premises:     - n-result: 𝑛1-      morph: 𝑛+      morph: 𝑛0     - n-result: 𝑛2-      normalize: '𝑛1(𝜏 ↦ 𝑘1)'+      normalize: '𝑛1(𝜏0 ↦ 𝑘1)'     - n-result: 𝑛3       morph: 𝑛2  - name: maa-  match: '𝑛(α𝑖 ↦ 𝑘1)'-  e-match: 𝑒+  match: '𝑛0(α𝑖0 ↦ 𝑘1)'+  e-match: 𝑒0   n-result: 𝑛3   premises:     - n-result: 𝑛1-      morph: 𝑛+      morph: 𝑛0     - n-result: 𝑛2-      normalize: '𝑛1(α𝑖 ↦ 𝑘1)'+      normalize: '𝑛1(α𝑖0 ↦ 𝑘1)'     - n-result: 𝑛3       morph: 𝑛2  - name: mad   match: '𝑛(𝜏 ↦ 𝑛1)'-  e-match: 𝑒+  e-match: 𝑒0   n-result: 𝑛2   when:     not:@@ -141,7 +143,7 @@  - name: maad   match: '𝑛(α𝑖 ↦ 𝑛1)'-  e-match: 𝑒+  e-match: 𝑒0   n-result: 𝑛2   when:     not:@@ -153,36 +155,36 @@ - name: universe   label: \Phi   match: Φ-  e-match: 𝑒-  n-result: 𝑛1+  e-match: 𝑒0+  n-result: 𝑛2   when:     not:       eq:-        - 𝑒+        - 𝑒0         - Φ   premises:-    - n-result: 𝑛-      normalize: 𝑒     - n-result: 𝑛1-      morph: 𝑛+      normalize: 𝑒0+    - n-result: 𝑛2+      morph: 𝑛1  - name: dead   match: ⊥-  e-match: 𝑒+  e-match: 𝑒0   n-result: ⊥  - name: xi   match: ξ-  e-match: 𝑒-  n-result: 𝑛+  e-match: 𝑒0+  n-result: 𝑛1   premises:-    - n-result: 𝑛+    - n-result: 𝑛1       morph: ⊥  - name: mg   match: Φ   e-match: Φ-  n-result: 𝑛+  n-result: 𝑛1   premises:-    - n-result: 𝑛+    - n-result: 𝑛1       morph: ⊥

@@ -2,9 +2,9 @@ # SPDX-License-Identifier: MIT --- name: alpha-pattern: ⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧(α𝑖 ↦ 𝑒)-result: ⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧(𝜏 ↦ 𝑒)+pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(α𝑖1 ↦ 𝑒1)+result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒1) when:   eq:-    - 𝑖+    - 𝑖1     - domain: 𝐵1

@@ -2,10 +2,10 @@ # SPDX-License-Identifier: MIT --- name: amiss-pattern: ⟦𝐵⟧(α𝑖 ↦ 𝑒)+pattern: ⟦𝐵1⟧(α𝑖1 ↦ 𝑒) result: ⊥ when:   not:     gt:-      - domain: 𝐵-      - 𝑖+      - domain: 𝐵1+      - 𝑖1

@@ -2,5 +2,5 @@ # SPDX-License-Identifier: MIT --- name: copy-pattern: ⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑘)-result: ⟦ 𝐵1, 𝜏 ↦ 𝑘, 𝐵2 ⟧+pattern: ⟦ 𝐵1, 𝜏1 ↦ ∅, 𝐵2 ⟧(𝜏1 ↦ 𝑘1)+result: ⟦ 𝐵1, 𝜏1 ↦ 𝑘1, 𝐵2 ⟧

@@ -1,21 +1,21 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----# Dispatch 𝜏 on a formation: contextualize the dispatched body 𝑛 and decorate+# Dispatch 𝜏1 on a formation: contextualize the dispatched body 𝑛1 and decorate # it with the whole formation as ρ. The contextualization context is the-# formation WITHOUT the dispatched binding — ⟦𝐵1, 𝐵2⟧, not ⟦𝐵1, 𝜏 ↦ 𝑛, 𝐵2⟧ —-# so a self-referential ξ inside 𝑛 (as in ⟦ a ↦ ξ ⟧.a or ⟦ a ↦ ξ.a ⟧.a) no-# longer sees 𝜏. Such a self-reference then dispatches on a formation that-# lacks 𝜏 and collapses to ⊥ via stop/null/dd instead of rebuilding the same-# ⟦…, 𝜏 ↦ 𝑛, …⟧.𝜏 term and looping forever. ρ on line 'result' still binds the-# full formation, so sibling and φ-decoration references stay intact — only the-# self-ξ path narrows, keeping normalization (near-)total.+# formation WITHOUT the dispatched binding — ⟦𝐵1, 𝐵2⟧, not ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧ —+# so a self-referential ξ inside 𝑛1 (as in ⟦ a ↦ ξ ⟧.a or ⟦ a ↦ ξ.a ⟧.a) no+# longer sees 𝜏1. Such a self-reference then dispatches on a formation that+# lacks 𝜏1 and collapses to ⊥ via stop/null/dd instead of rebuilding the same+# ⟦…, 𝜏1 ↦ 𝑛1, …⟧.𝜏1 term and looping forever. ρ on line 'result' still binds+# the full formation, so sibling and φ-decoration references stay intact — only+# the self-ξ path narrows, keeping normalization (near-)total. name: dot-pattern: ⟦𝐵1, 𝜏 ↦ 𝑛, 𝐵2⟧.𝜏-result: 𝑒(ρ ↦ ⟦𝐵1, 𝜏 ↦ 𝑛, 𝐵2⟧)+pattern: ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧.𝜏1+result: 𝑒1(ρ ↦ ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧) where:-  - meta: 𝑒+  - meta: 𝑒1     function: contextualize     args:-      - 𝑛+      - 𝑛1       - ⟦𝐵1, 𝐵2⟧

@@ -2,10 +2,10 @@ # SPDX-License-Identifier: MIT --- name: miss-pattern: ⟦𝐵⟧(𝜏 ↦ 𝑒)+pattern: ⟦𝐵1⟧(𝜏1 ↦ 𝑒) result: ⊥ when:   not:     in:-      - 𝜏-      - 𝐵+      - 𝜏1+      - 𝐵1

@@ -2,5 +2,5 @@ # SPDX-License-Identifier: MIT --- name: 'null'-pattern: ⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧.𝜏+pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧.𝜏1 result: ⊥

@@ -2,10 +2,10 @@ # SPDX-License-Identifier: MIT --- name: over-pattern: ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧(𝜏 ↦ 𝑒2)+pattern: ⟦𝐵1, 𝜏1 ↦ 𝑒1, 𝐵2⟧(𝜏1 ↦ 𝑒2) result: ⊥ when:   not:     eq:-      - 𝜏+      - 𝜏1       - ρ

@@ -2,14 +2,14 @@ # SPDX-License-Identifier: MIT --- name: overa-pattern: ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧(α𝑖 ↦ 𝑒2)+pattern: ⟦𝐵1, 𝜏1 ↦ 𝑒1, 𝐵2⟧(α𝑖1 ↦ 𝑒2) result: ⊥ when:   and:     - eq:-        - 𝑖+        - 𝑖1         - domain: 𝐵1     - not:         eq:-          - 𝜏+          - 𝜏1           - ρ

@@ -2,19 +2,19 @@ # SPDX-License-Identifier: MIT --- name: stop-pattern: ⟦𝐵⟧.𝜏+pattern: ⟦𝐵1⟧.𝜏1 result: ⊥ when:   and:     - not:         in:-          - 𝜏-          - 𝐵+          - 𝜏1+          - 𝐵1     - not:         in:           - φ-          - 𝐵+          - 𝐵1     - not:         in:           - λ-          - 𝐵+          - 𝐵1

@@ -16,6 +16,14 @@ import qualified Data.Text as T import GHC.Generics (Generic) +-- An anonymous meta-variable, written bare — 𝜏, 𝐵, 𝑒, 𝑛, 𝑘, δ, 𝑓 or 𝑖 with+-- no index after it. It matches whatever term stands in its place and no rule+-- can name it afterwards, so it is known only by the kind it was written as+-- ('t', 'B', 'e', 'n', 'k', 'd', 'F', 'i') and by the offset it was written+-- at, which tells it apart from every other anonymous meta of the same term.+data Slot = Slot Text Int+  deriving (Eq, Ord, Show)+ data Expression   = ExFormation [Binding]   | ExXi@@ -24,6 +32,7 @@   | ExApplication Expression Argument   | ExDispatch Expression Attribute   | ExMeta Text+  | ExAny Slot   | ExPhiMeet (Maybe String) Int Expression   | ExPhiAgain (Maybe String) Int Expression   | {- | Bare data 𝛿 — the raw bytes extracted by the 'delta' dataization rule.@@ -43,6 +52,7 @@ data Alpha   = Alpha Int   | AlMeta Text+  | AlAny Slot   deriving (Eq, Ord, Generic)  data Binding@@ -51,6 +61,7 @@   | BiDelta Bytes   | BiLambda Function   | BiMeta Text+  | BiAny Slot   deriving (Eq, Ord, Show, Generic)  data Bytes@@ -58,6 +69,7 @@   | BtOne String   | BtMany [String]   | BtMeta Text+  | BtAny Slot   deriving (Eq, Ord, Show, Generic)  data Attribute@@ -67,11 +79,13 @@   | AtLambda   | AtDelta   | AtMeta Text+  | AtAny Slot   deriving (Eq, Generic, Ord)  data Function   = Function Text   | FnMeta Text+  | FnAny Slot   deriving (Eq, Generic, Show, Ord)  instance Show Attribute where@@ -81,10 +95,12 @@   show AtDelta = "Δ"   show AtLambda = "λ"   show (AtMeta meta) = '!' : T.unpack meta+  show (AtAny (Slot kind _)) = '!' : T.unpack kind  instance Show Alpha where   show (Alpha idx) = 'α' : show idx   show (AlMeta meta) = 'α' : '!' : T.unpack meta+  show (AlAny (Slot kind _)) = 'α' : '!' : T.unpack kind  -- A cheap, fixed-size digest of an expression, used for fast (dirty) equality -- checks during loop detection. Equal expressions always produce the same@@ -103,6 +119,8 @@     hashText = T.foldl' (\h c -> step h (fromEnum c))     hashString :: Int -> String -> Int     hashString = foldl' (\h c -> step h (fromEnum c))+    goSlot :: Int -> Slot -> Int+    goSlot h (Slot kind idx) = step (hashText h kind) idx     hashMaybeString :: Int -> Maybe String -> Int     hashMaybeString h Nothing = step h 0     hashMaybeString h (Just s) = hashString (step h 1) s@@ -115,6 +133,7 @@       ExApplication ex arg -> goArgument (goExpr (step h 5) ex) arg       ExDispatch ex at -> goAttribute (goExpr (step h 6) ex) at       ExMeta t -> hashText (step h 7) t+      ExAny slot -> goSlot (step h 32) slot       ExPhiMeet ms i ex -> goExpr (hashMaybeString (step (step h 9) i) ms) ex       ExPhiAgain ms i ex -> goExpr (hashMaybeString (step (step h 10) i) ms) ex       ExBytes bts -> goBytes (step h 8) bts@@ -125,12 +144,14 @@       BiVoid at -> goAttribute (step h 13) at       BiLambda fn -> goFunction (step h 14) fn       BiMeta t -> hashText (step h 15) t+      BiAny slot -> goSlot (step h 33) slot     goBytes :: Int -> Bytes -> Int     goBytes h = \case       BtEmpty -> step h 17       BtOne s -> hashString (step h 18) s       BtMany ss -> foldl' hashString (step h 19) ss       BtMeta t -> hashText (step h 20) t+      BtAny slot -> goSlot (step h 34) slot     goAttribute :: Int -> Attribute -> Int     goAttribute h = \case       AtLabel t -> hashText (step h 21) t@@ -139,6 +160,7 @@       AtLambda -> step h 25       AtDelta -> step h 26       AtMeta t -> hashText (step h 27) t+      AtAny slot -> goSlot (step h 35) slot     goArgument :: Int -> Argument -> Int     goArgument h = \case       ArTau at ex -> goExpr (goAttribute (step h 22) at) ex@@ -147,10 +169,12 @@     goAlpha h = \case       Alpha idx -> step (step h 31) idx       AlMeta t -> hashText (step h 28) t+      AlAny slot -> goSlot (step h 36) slot     goFunction :: Int -> Function -> Int     goFunction h = \case       Function t -> hashText (step h 16) t       FnMeta t -> hashText (step h 29) t+      FnAny slot -> goSlot (step h 37) slot  countNodes :: Expression -> Int countNodes (ExFormation bds) = 1 + sum (map nodesInBinding bds) + length bds@@ -158,6 +182,7 @@     nodesInBinding :: Binding -> Int     nodesInBinding (BiTau _ expr) = countNodes expr + 2     nodesInBinding (BiMeta _) = 1+    nodesInBinding (BiAny _) = 1     nodesInBinding _ = 3 countNodes (ExApplication expr (ArTau _ expr')) = 4 + countNodes expr + countNodes expr' countNodes (ExApplication expr (ArAlpha _ expr')) = 4 + countNodes expr + countNodes expr'

@@ -0,0 +1,261 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-}++-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++-- Which λ functions exist is a property of the object model being dataized,+-- not of the calculus. phino therefore implements none of them: it reads a+-- registry of them from a JSON file given with '--atoms' and fires each one as+-- a POSIX process. The registry maps a λ name to the runtime that runs it and+-- the script it runs:+--+-- > {+-- >   "L_bytes_eq": {+-- >     "rt": "node",+-- >     "script": "const fs = require('fs'); ..."+-- >   }+-- > }+--+-- A name absent from the registry has no λ function at all: 𝔼 gets stuck on+-- it, exactly as it does for a name no one ever declared (see 'Stuck' in+-- 'Dataize').+module Atoms+  ( Atom (..)+  , AtomException (..)+  , Registry+  , Runtime (..)+  , emptyRegistry+  , fireAtom+  , readRegistry+  , registeredAtom+  , runtimeNames+  )+where++import AST+import Control.Exception (Exception, bracket, catch, throwIO)+import Control.Monad (unless)+import Data.Aeson (FromJSON (parseJSON), eitherDecodeStrict', object, withObject, withText, (.:), (.=))+import qualified Data.Aeson as A+import qualified Data.ByteString as BS+import qualified Data.ByteString.Lazy as BSL+import Data.List (find, intercalate)+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import qualified Data.Text as T+import Data.Text.Encoding (decodeUtf8Lenient, encodeUtf8)+import Encoding (Encoding (UNICODE))+import Lining (LineFormat (SINGLELINE))+import Logger (logDebug)+import Margin (defaultMargin)+import Parser (parseExpression)+import Printer (printExpression')+import Sugar (SugarType (SALTY))+import System.Directory (getTemporaryDirectory, removePathForcibly)+import System.Exit (ExitCode (ExitFailure, ExitSuccess))+import System.IO (Handle, IOMode (WriteMode), hClose, hSetBinaryMode, openBinaryTempFile, withBinaryFile)+import System.Process (CreateProcess (std_err, std_in, std_out), ProcessHandle, StdStream (CreatePipe, UseHandle), createProcess, proc, waitForProcess)+import Text.Printf (printf)++-- The interpreter a script is run under, named after the executable itself:+-- only 'node' for now. A registry naming any other runtime is rejected when it+-- is read, before dataization starts, so a run never gets half-way through a+-- program to discover that one of its atoms cannot be run at all.+data Runtime = RtNode+  deriving stock (Eq, Show)++-- One entry of the registry: the runtime and the source of the script.+data Atom = Atom+  { _runtime :: Runtime+  , _script :: T.Text+  }+  deriving stock (Eq, Show)++-- Every λ function phino may fire, keyed by name.+type Registry = Map T.Text Atom++data AtomException+  = -- The '--atoms' file is not a JSON registry of λ functions.+    BrokenRegistry FilePath String+  | -- The interpreter of a runtime is not installed, so no script of it can run.+    NoRuntime T.Text String String+  | -- The script exited with a non-zero status; the message carries its stderr.+    AtomBroke T.Text Int String+  | -- The script exited successfully but said nothing phino can use: its stdout+    -- is not a JSON object, carries no 'n' field, or the 𝜑-expression under it+    -- does not parse.+    AtomMute T.Text String String+  deriving anyclass (Exception)++instance Show AtomException where+  show (BrokenRegistry file failure) = printf "The registry of atoms '%s' cannot be read: %s" file failure+  show (NoRuntime func runner failure) =+    printf "Atom '%s' cannot be fired, '%s' is not runnable: %s" (T.unpack func) runner failure+  show (AtomBroke func status complaint) =+    printf "Atom '%s' failed with exit code %d: %s" (T.unpack func) status complaint+  show (AtomMute func answer failure) =+    printf "Atom '%s' returned '%s', which phino cannot use: %s" (T.unpack func) answer failure++-- The name a registry spells a runtime with.+runtimeName :: Runtime -> String+runtimeName RtNode = "node"++-- The POSIX executable the scripts of a runtime are run under.+interpreter :: Runtime -> String+interpreter RtNode = "node"++-- The extension the script of a runtime is written to disk with, so the+-- interpreter recognizes the file for what it is. This is the language, not the+-- runtime: 'node' loads a file only if it is named '.js'.+extension :: Runtime -> String+extension RtNode = "js"++-- Every runtime phino can run, in the order the '--atoms' help lists them.+runtimes :: [Runtime]+runtimes = [RtNode]++runtimeNames :: [String]+runtimeNames = map runtimeName runtimes++instance FromJSON Runtime where+  parseJSON = withText "runtime" $ \name -> case find ((== T.unpack name) . runtimeName) runtimes of+    Just runtime -> pure runtime+    Nothing -> fail (printf "unknown runtime '%s', expected one of: %s" (T.unpack name) (intercalate ", " runtimeNames))++instance FromJSON Atom where+  parseJSON = withObject "atom" $ \entry -> Atom <$> entry .: "rt" <*> entry .: "script"++-- What the script writes to stdout: one JSON object whose 'n' field is the+-- 𝜑-expression the atom answers with.+newtype Answer = Answer T.Text++instance FromJSON Answer where+  parseJSON = withObject "answer" $ \answer -> Answer <$> answer .: "n"++-- No λ function at all: every atom gets stuck. This is what a run without+-- '--atoms' fires against.+emptyRegistry :: Registry+emptyRegistry = Map.empty++-- The λ function registered under this name, if any.+registeredAtom :: Registry -> T.Text -> Maybe Atom+registeredAtom registry func = Map.lookup func registry++-- Read the registry of λ functions from a JSON file. An unknown runtime, a+-- missing 'script' or malformed JSON fails here, before any dataization+-- starts.+readRegistry :: FilePath -> IO Registry+readRegistry path = do+  content <- BS.readFile path `catch` unreadable+  case eitherDecodeStrict' content of+    Left failure -> throwIO (BrokenRegistry path failure)+    Right registry -> do+      logDebug (printf "Loaded %d atom(s) from '%s'" (Map.size registry) path)+      pure registry+  where+    unreadable :: IOError -> IO BS.ByteString+    unreadable failure = throwIO (BrokenRegistry path (show failure))++-- Fire the λ function 'func' by running its script as a POSIX process under+-- the interpreter of its runtime, with the λ name as the first command-line+-- argument — one script may be registered under several names and branch on+-- it. The script is fed a JSON object on stdin (see 'payload') and answers+-- with one on stdout; the 𝜑-expression under 'n' becomes the atom's raw+-- result, which 𝔼 normalizes exactly as it normalized the answer of a built-in+-- one. A non-zero exit, unparsable output or a missing 'n' fails the run.+fireAtom :: T.Text -> Atom -> Expression -> Expression -> IO Expression+fireAtom func Atom{..} form univ =+  withTemp (printf "phino-atom-.%s" (extension _runtime)) (encodeUtf8 _script) $ \script ->+    withTemp "phino-atom-.err" "" $ \errors -> do+      logDebug (printf "Firing atom '%s' as '%s %s %s'" (T.unpack func) (interpreter _runtime) script (T.unpack func))+      (status, answer) <- executed script errors+      complaint <- readErrors errors+      unless (null complaint) (logDebug (printf "Atom '%s' wrote to stderr: %s" (T.unpack func) complaint))+      case status of+        ExitFailure code -> throwIO (AtomBroke func code complaint)+        ExitSuccess -> answered answer+  where+    -- Run the interpreter with its input and its output on pipes and its+    -- complaints in a file. The input is written and closed before the output is+    -- read, so the parent never has two streams to drain at once — which would+    -- need threads to be safe — and the script's own stderr, which may be+    -- anything at all, cannot fill a pipe nobody is reading. Every stream is+    -- bytes: a 𝜑 expression carries characters no single-byte locale can spell,+    -- so nothing is left to the locale.+    executed :: FilePath -> FilePath -> IO (ExitCode, BS.ByteString)+    executed script errors =+      withBinaryFile errors WriteMode $ \stderr' -> do+        (stdin', stdout', process) <- spawned script stderr'+        hSetBinaryMode stdin' True+        hSetBinaryMode stdout' True+        -- A script that dies before reading its input leaves this write with+        -- nobody to drain it. The failure worth reporting is the one the script+        -- made, so a broken pipe is swallowed here and the exit status decides.+        BS.hPut stdin' (payload form univ) `catch` unheard+        hClose stdin' `catch` unheard+        answer <- BS.hGetContents stdout'+        status <- waitForProcess process+        pure (status, answer)+    spawned :: FilePath -> Handle -> IO (Handle, Handle, ProcessHandle)+    spawned script stderr' = do+      spawn <- createProcess started `catch` missing+      case spawn of+        (Just stdin', Just stdout', _, process) -> pure (stdin', stdout', process)+        _ -> throwIO (AtomMute func "" "the interpreter gave phino no streams to talk over")+      where+        started :: CreateProcess+        started =+          (proc (interpreter _runtime) [script, T.unpack func])+            { std_in = CreatePipe+            , std_out = CreatePipe+            , std_err = UseHandle stderr'+            }+    missing :: IOError -> IO a+    missing failure = throwIO (NoRuntime func (interpreter _runtime) (show failure))+    unheard :: IOError -> IO ()+    unheard _ = pure ()+    -- Whatever the script complained about, decoded leniently: the stream is+    -- the script's, so it may hold anything at all.+    readErrors :: FilePath -> IO String+    readErrors errors = T.unpack . T.strip . decodeUtf8Lenient <$> BS.readFile errors+    -- Parse what the script said: a JSON object with the raw 𝜑-expression+    -- under 'n'.+    answered :: BS.ByteString -> IO Expression+    answered answer = case eitherDecodeStrict' answer of+      Left failure -> throwIO (AtomMute func spoken failure)+      Right (Answer raw) -> case parseExpression (T.unpack raw) of+        Left failure -> throwIO (AtomMute func (T.unpack raw) failure)+        Right expr -> pure expr+      where+        spoken :: String+        spoken = T.unpack (T.strip (decodeUtf8Lenient answer))++-- The JSON phino feeds a script on stdin: the formation being evaluated under+-- 'b', with its λ binding removed so the script may dispatch on it, and the+-- universe Φ under 's'. Both are rendered as canonical 𝜑-calculus on a single+-- line — no syntax sugar, whatever '--sweet' says about the output of the run —+-- so a script never has to know phino's sugar to find a datum: every byte array+-- it may need is spelled out as a Δ binding. The text is what phino's own parser+-- reads back, so a script may hand any part of it to another phino run (see the+-- '--inside' option).+payload :: Expression -> Expression -> BS.ByteString+payload form univ = BSL.toStrict (A.encode (object ["b" .= rendered form, "s" .= rendered univ]))+  where+    rendered :: Expression -> T.Text+    rendered expr = T.pack (printExpression' expr (SALTY, UNICODE, SINGLELINE, defaultMargin))++-- Write the content to a fresh temporary file, hand its path to the action and+-- delete the file afterwards, whatever the action does.+withTemp :: String -> BS.ByteString -> (FilePath -> IO a) -> IO a+withTemp template content action = do+  dir <- getTemporaryDirectory+  bracket (openBinaryTempFile dir template) discarded $ \(path, handle) -> do+    BS.hPut handle content+    hClose handle+    action path+  where+    discarded :: (FilePath, Handle) -> IO ()+    discarded (path, handle) = hClose handle >> removePathForcibly path

@@ -42,6 +42,11 @@ metaMsg :: Text -> String metaMsg = printf "meta '%s' is either does not exist or refers to an inappropriate term" . T.unpack +-- An anonymous meta is bound only within the very pattern that matched it, so+-- a lookup that misses means the term being built is not that pattern+slotMsg :: Slot -> String+slotMsg (Slot kind _) = printf "anonymous meta '!%s' cannot be referenced" (T.unpack kind)+ type Built a = Either String a  instance Show BuildException where@@ -64,21 +69,30 @@ contextualize ex _ = ex  buildAttribute :: Attribute -> Subst -> Built Attribute-buildAttribute (AtMeta meta) (Subst mp) = case Map.lookup meta mp of+buildAttribute (AtMeta meta) (Subst mp) = case Map.lookup (Named meta) mp of   Just (MvAttribute attr) -> Right attr   _ -> Left (metaMsg meta)+buildAttribute (AtAny slot) (Subst mp) = case Map.lookup (Anon slot) mp of+  Just (MvAttribute attr) -> Right attr+  _ -> Left (slotMsg slot) buildAttribute attr _ = Right attr  buildAlpha :: Alpha -> Subst -> Built Alpha-buildAlpha (AlMeta meta) (Subst mp) = case Map.lookup meta mp of+buildAlpha (AlMeta meta) (Subst mp) = case Map.lookup (Named meta) mp of   Just (MvIndex idx) -> Right (Alpha idx)   _ -> Left (metaMsg meta)+buildAlpha (AlAny slot) (Subst mp) = case Map.lookup (Anon slot) mp of+  Just (MvIndex idx) -> Right (Alpha idx)+  _ -> Left (slotMsg slot) buildAlpha a _ = Right a  buildBytes :: Bytes -> Subst -> Built Bytes-buildBytes (BtMeta meta) (Subst mp) = case Map.lookup meta mp of+buildBytes (BtMeta meta) (Subst mp) = case Map.lookup (Named meta) mp of   Just (MvBytes bytes) -> Right bytes   _ -> Left (metaMsg meta)+buildBytes (BtAny slot) (Subst mp) = case Map.lookup (Anon slot) mp of+  Just (MvBytes bytes) -> Right bytes+  _ -> Left (slotMsg slot) buildBytes bts _ = Right bts  -- Build binding@@ -92,15 +106,21 @@ buildBinding (BiVoid attr) subst = do   attribute <- buildAttribute attr subst   Right [BiVoid attribute]-buildBinding (BiMeta meta) (Subst mp) = case Map.lookup meta mp of+buildBinding (BiMeta meta) (Subst mp) = case Map.lookup (Named meta) mp of   Just (MvBindings bds) -> uniqueBindings bds   _ -> Left (metaMsg meta)+buildBinding (BiAny slot) (Subst mp) = case Map.lookup (Anon slot) mp of+  Just (MvBindings bds) -> uniqueBindings bds+  _ -> Left (slotMsg slot) buildBinding (BiDelta bytes) subst = do   bts <- buildBytes bytes subst   Right [BiDelta bts]-buildBinding (BiLambda (FnMeta meta)) (Subst mp) = case Map.lookup meta mp of+buildBinding (BiLambda (FnMeta meta)) (Subst mp) = case Map.lookup (Named meta) mp of   Just (MvFunction func) -> Right [BiLambda (Function func)]   _ -> Left (metaMsg meta)+buildBinding (BiLambda (FnAny slot)) (Subst mp) = case Map.lookup (Anon slot) mp of+  Just (MvFunction func) -> Right [BiLambda (Function func)]+  _ -> Left (slotMsg slot) buildBinding binding _ = Right [binding]  buildArgument :: Argument -> Subst -> Built Argument@@ -121,6 +141,12 @@   bds <- buildBindings rest subst   Right (first ++ bds) +-- The bindings of a formation a meta was bound to are checked once more here,+-- since a substitution may bring two of them together under one attribute.+unique :: Expression -> Built Expression+unique (ExFormation bds) = uniqueBindings bds >> Right (ExFormation bds)+unique expr = Right expr+ -- Build meta expression with given substitution buildExpression :: Expression -> Subst -> Built Expression buildExpression (ExDispatch ex at) subst = do@@ -134,12 +160,12 @@ buildExpression (ExFormation bds) subst = do   bds' <- buildBindings bds subst >>= uniqueBindings   Right (ExFormation bds')-buildExpression (ExMeta meta) (Subst mp) = case Map.lookup meta mp of-  Just (MvExpression expr) ->-    case expr of-      ExFormation bds -> uniqueBindings bds >> Right expr-      _ -> Right expr+buildExpression (ExMeta meta) (Subst mp) = case Map.lookup (Named meta) mp of+  Just (MvExpression expr) -> unique expr   _ -> Left (metaMsg meta)+buildExpression (ExAny slot) (Subst mp) = case Map.lookup (Anon slot) mp of+  Just (MvExpression expr) -> unique expr+  _ -> Left (slotMsg slot) buildExpression expr _ = Right expr  buildBytesThrows :: Bytes -> Subst -> IO Bytes

@@ -60,6 +60,7 @@ btsToWord8 (BtOne bt) = [hexByte bt] btsToWord8 (BtMany bts) = map hexByte bts btsToWord8 (BtMeta mt) = error $ "Cannot convert meta bytes to Word8; " ++ T.unpack mt+btsToWord8 (BtAny _) = error "Cannot convert anonymous meta bytes to Word8"  hexByte :: String -> Word8 hexByte [hi, lo] = (nibble hi `shiftL` 4) .|. nibble lo@@ -185,6 +186,7 @@ -- Nothing btsToNonFinite :: Bytes -> Maybe NonFinite btsToNonFinite (BtMeta _) = Nothing+btsToNonFinite (BtAny _) = Nothing btsToNonFinite bts = find (btsEqual bts . nonFiniteBts) nonFinites  -- The non-finite double the given name stands for, if it names one at all

@@ -7,6 +7,7 @@ module CLI.Helpers where  import AST+import Atoms (Registry, emptyRegistry, readRegistry) import CLI.Types import CLI.Validators (invalidCLIArguments) import Canonizer (canonize)@@ -16,6 +17,7 @@ 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)@@ -83,6 +85,34 @@       protocol <- openFile file WriteMode       hSetEncoding protocol utf8       pure protocol++-- The λ functions this run may fire. phino implements none of them, so without+-- '--atoms' the registry is empty and every atom a program names gets stuck —+-- which is exactly what '--partial' parks on. The file is read here, before+-- anything is parsed or dataized, so an unknown runtime or a malformed registry+-- fails the run up front rather than half-way through a derivation.+registryOf :: Maybe FilePath -> IO Registry+registryOf Nothing = do+  logDebug "The option '--atoms' is not specified, no λ function can be fired"+  pure emptyRegistry+registryOf (Just file) = do+  logDebug (printf "The option '--atoms' is specified, reading the λ functions from '%s'" file)+  ensuredFile file >>= readRegistry++-- Aim the run at the '--inside' expression instead of at '--locator': the+-- expression is bound to a synthetic attribute prepended to the input+-- 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 Nothing expr ctx = pure (expr, ctx)+aimed (Just src) expr@(ExFormation _) ctx = do+  target <- parseExpressionThrows src+  logDebug (printf "The option '--inside' is specified, reducing '%s' inside the given universe" (P.printExpression target))+  insideUniverse target expr ctx+aimed (Just _) expr _ =+  invalidCLIArguments+    (printf "The option --inside requires the input expression to be a formation, but given: %s" (P.printExpression expr))  -- Read input from file or stdin readInput :: Maybe FilePath -> IO String

@@ -3,6 +3,7 @@  module CLI.Parsers where +import Atoms (runtimeNames) import CLI.Types import Data.Char (toLower, toUpper) import Data.List (intercalate)@@ -203,8 +204,42 @@ optStepsDir = optional (strOption (long "steps-dir" <> metavar "FILE" <> help "Directory to save intermediate steps during rewriting/dataizing"))  optPartial :: Parser Bool-optPartial = switch (long "partial" <> help "Partial evaluation: compute what the known inputs decide and, instead of failing on an atom that cannot fire (its λ function is unknown, or an input of it reaches such an atom), leave it in place and print the residual 𝜑-program")+optPartial = switch (long "partial" <> help "Partial evaluation: compute what the known inputs decide and, instead of failing on an atom that cannot fire (its λ function is not in the --atoms registry), leave it in place and print the residual 𝜑-program") +-- Which λ functions this run may fire. phino implements none of them itself+-- (see 'Atoms'), so without this option every atom a program names gets stuck.+optAtoms :: Parser (Maybe FilePath)+optAtoms =+  optional+    ( strOption+        ( long "atoms"+            <> metavar "FILE"+            <> help+              ( printf+                  "Path to the JSON registry of λ functions this run may fire, mapping each name to the runtime that runs it (%s) and the script it runs"+                  (intercalate ", " runtimeNames)+              )+        )+    )++-- The external face of the trick phino plays internally to reduce a+-- sub-expression against a universe: prepend a synthetic binding holding it to+-- that universe and aim the locator at the binding. An atom script needs it to+-- reduce the parts of the formation it was given, so it does not have to splice+-- them into the text of the universe by hand.+optInside :: Parser (Maybe String)+optInside =+  optional+    ( strOption+        ( long "inside"+            <> metavar "EXPRESSION"+            <> help+              "The 𝜑-expression to dataize or morph inside the input expression, which is taken as the universe \+              \Φ: a synthetic binding holding it is prepended to the universe and the locator is aimed at that \+              \binding. Cannot be used together with --locator"+        )+    )+ optEvaluations :: Parser (Maybe FilePath) optEvaluations = optional (strOption (long "evaluations" <> metavar "FILE" <> help "File to record every atom fired during dataizing, as one tab-separated line per firing: the λ function name, its argument formation and its result (requires --output=phi)")) @@ -312,8 +347,10 @@             <*> optExpression             <*> optLabel             <*> optMeetPrefix+            <*> optInside             <*> optStepsDir             <*> optEvaluations+            <*> optAtoms             <*> argInputFile         ) @@ -353,8 +390,10 @@             <*> optExpression             <*> optLabel             <*> optMeetPrefix+            <*> optInside             <*> optStepsDir             <*> optEvaluations+            <*> optAtoms             <*> argInputFile         ) 

@@ -14,9 +14,11 @@ import Condition (parseConditionThrows) import Control.Exception import Control.Monad (unless, when)+import Data.Foldable (traverse_) import Data.List (intercalate) import qualified Data.List.NonEmpty as NE import Data.Maybe (fromJust, isJust, isNothing)+import qualified Data.Text as T import Dataize import Encoding import qualified Filter as F@@ -30,6 +32,7 @@ import qualified Random as R import Rewriter import Rule (RuleContext (..), matchExpressionWithRule)+import Slots (anonymous) import System.Directory (doesFileExist, getModificationTime) import System.Exit (exitSuccess) import System.Random (mkStdGen, setStdGen)@@ -142,6 +145,7 @@ runDataize :: OptsDataize -> IO () runDataize OptsDataize{..} = do   validateOpts+  atoms <- registryOf _atoms   excluded <- validatedDispatches "hide" _hide   included <- validatedDispatches "show" _show   [loc] <- validatedDispatches "locator" [_locator]@@ -156,8 +160,10 @@       include = (`F.include` included)   save <- saveStepFunc _stepsDir printCtx   (outcome, chain) <--    withEvalFunc _evaluations printCtx $-      dataize expr . DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial buildTerm save+    withEvalFunc _evaluations printCtx $ \record -> do+      let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial atoms buildTerm save record+      (universe, aiming) <- aimed _inside expr ctx+      dataize universe aiming   when _sequence (printRewrittens printCtx (exclude $ include chain, False) >>= putStrLn)   unless _quiet (printOutcome printCtx outcome >>= putStrLn)   where@@ -181,6 +187,9 @@       when         (isJust _evaluations && _outputFormat /= PHI)         (invalidCLIArguments "The --evaluations option can stay together with --output=phi only, since one record must fit into one line")+      when+        (isJust _inside && _locator /= "Q")+        (invalidCLIArguments "The options --inside and --locator cannot be used together, since --inside aims the run at the binding it mints")     toPrintCtx :: Expression -> PrintContext     toPrintCtx focus =       PrintCtx@@ -211,6 +220,7 @@ runMorph :: OptsMorph -> IO () runMorph OptsMorph{..} = do   validateOpts+  atoms <- registryOf _atoms   excluded <- validatedDispatches "hide" _hide   included <- validatedDispatches "show" _show   [loc] <- validatedDispatches "locator" [_locator]@@ -225,8 +235,10 @@       include = (`F.include` included)   save <- saveStepFunc _stepsDir printCtx   (morphed, chain) <--    withEvalFunc _evaluations printCtx $-      morph expr . DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial buildTerm save+    withEvalFunc _evaluations printCtx $ \record -> do+      let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial atoms buildTerm save record+      (universe, aiming) <- aimed _inside expr ctx+      morph universe aiming   when _sequence (printRewrittens printCtx (exclude $ include chain, False) >>= putStrLn)   unless _quiet (printFocused printCtx morphed >>= putStrLn)   where@@ -242,6 +254,9 @@       when         (isJust _evaluations && _outputFormat /= PHI)         (invalidCLIArguments "The --evaluations option can stay together with --output=phi only, since one record must fit into one line")+      when+        (isJust _inside && _locator /= "Q")+        (invalidCLIArguments "The options --inside and --locator cannot be used together, since --inside aims the run at the binding it mints")     toPrintCtx :: Expression -> PrintContext     toPrintCtx focus =       PrintCtx@@ -333,6 +348,7 @@     else do       ptn <- parseExpressionThrows (fromJust _pattern)       condition <- traverse parseConditionThrows _when+      traverse_ (throwIO . AnonymousMetaInCondition . T.unpack) (anonymous condition)       substs <- matchExpressionWithRule expr (rule ptn condition) (RuleContext buildTerm)       if null substs         then throwIO EmptySubstsOnMatch

@@ -41,6 +41,7 @@   | CouldNotDataize   | CouldNotPrintExpressionInXMIR   | EmptySubstsOnMatch+  | AnonymousMetaInCondition String   | VersionMismatch String String   deriving (Exception) @@ -50,6 +51,8 @@   show CouldNotDataize = "Could not dataize given expression"   show CouldNotPrintExpressionInXMIR = "Could not print expression with --output=xmir, only expression printing is allowed"   show EmptySubstsOnMatch = "Provided pattern was not matched, no substitutions are built"+  show (AnonymousMetaInCondition kind) =+    printf "Anonymous meta '!%s' cannot be referenced in --when, only a named one can" kind   show (VersionMismatch expected actual) =     printf "Version mismatch: --pin requires '%s', but this is phino %s" expected actual @@ -107,8 +110,10 @@   , _expression :: Maybe String   , _label :: Maybe String   , _meetPrefix :: Maybe String+  , _inside :: Maybe String   , _stepsDir :: Maybe FilePath   , _evaluations :: Maybe FilePath+  , _atoms :: Maybe FilePath   , _inputFile :: Maybe FilePath   } @@ -149,8 +154,10 @@   , _expression :: Maybe String   , _label :: Maybe String   , _meetPrefix :: Maybe String+  , _inside :: Maybe String   , _stepsDir :: Maybe FilePath   , _evaluations :: Maybe FilePath+  , _atoms :: Maybe FilePath   , _inputFile :: Maybe FilePath   } 

@@ -303,6 +303,11 @@ metaTail :: T.Text -> T.Text metaTail = T.drop 1 +-- An anonymous meta renders as the bare sigil it was written with: it carries+-- no suffix, and needs none, since nothing on the page refers back to it.+anyMeta :: META_HEAD -> META+anyMeta hd' = META NO_EXCL hd' T.empty+ -- The first character of an expression meta name encodes its kind: -- 'n'-prefixed names are normal-form-constrained '𝑛' metas, 'k'-prefixed -- names are absolute-constrained '𝑘' metas, everything else is an ordinary@@ -323,6 +328,7 @@   toCST ExRoot _ = EX_GLOBAL Φ   toCST ExXi _ = EX_XI XI   toCST (ExMeta mt) _ = EX_META (META NO_EXCL (exMetaHead mt) (metaTail mt))+  toCST (ExAny (Slot kind _)) _ = EX_META (anyMeta (exMetaHead kind))   toCST ExTermination _ = EX_TERMINATION DEAD   toCST (ExBytes bts) ctx = EX_BYTES (toCST bts ctx)   toCST (ExPhiMeet prefix idx expr) ctx = EX_PHI_MEET prefix idx (toCST expr ctx)@@ -467,11 +473,13 @@ instance ToCST [Binding] BINDING where   toCST [] (tabs, _) = BI_EMPTY (TAB tabs)   toCST (BiMeta mt : bds) ctx@(tabs, _) = BI_META (META NO_EXCL B (metaTail mt)) (toCST bds ctx) (TAB tabs)+  toCST (BiAny _ : bds) ctx@(tabs, _) = BI_META (anyMeta B) (toCST bds ctx) (TAB tabs)   toCST (bd : bds) ctx@(tabs, _) = BI_PAIR (toCST bd ctx) (toCST bds ctx) (TAB tabs)  instance ToCST [Binding] BINDINGS where   toCST [] (tabs, _) = BDS_EMPTY (TAB tabs)   toCST (BiMeta mt : bds) ctx@(tabs, eol) = BDS_META eol (TAB tabs) (META NO_EXCL B (metaTail mt)) (toCST bds ctx)+  toCST (BiAny _ : bds) ctx@(tabs, eol) = BDS_META eol (TAB tabs) (anyMeta B) (toCST bds ctx)   toCST (bd : bds) ctx@(tabs, eol) = BDS_PAIR eol (TAB tabs) (toCST bd ctx) (toCST bds ctx)  instance ToCST Binding PAIR where@@ -498,7 +506,9 @@   toCST (BiDelta bts) ctx = PA_DELTA (toCST bts ctx)   toCST (BiLambda (Function name)) _ = PA_LAMBDA name   toCST (BiLambda (FnMeta mt)) _ = PA_META_LAMBDA (META NO_EXCL F (metaTail mt))+  toCST (BiLambda (FnAny _)) _ = PA_META_LAMBDA (anyMeta F)   toCST (BiMeta mt) _ = error $ "BiMeta binding " ++ T.unpack mt ++ " cannot be converted to PAIR"+  toCST (BiAny _) _ = error "An anonymous meta binding cannot be converted to PAIR"  instance ToCST Argument PAIR where   toCST (ArTau attr exp) ctx = toCST (BiTau attr exp) ctx@@ -521,6 +531,7 @@   toCST (BtOne byte) _ = BT_ONE byte   toCST (BtMany bts) _ = BT_MANY bts   toCST (BtMeta mt) _ = BT_META (META NO_EXCL D (metaTail mt))+  toCST (BtAny _) _ = BT_META (anyMeta D)  instance ToCST Attribute ATTRIBUTE where   toCST (AtLabel label) _ = AT_LABEL label@@ -529,10 +540,12 @@   toCST AtDelta _ = AT_DELTA DELTA   toCST AtLambda _ = AT_LAMBDA LAMBDA   toCST (AtMeta mt) _ = AT_META (META NO_EXCL TAU (metaTail mt))+  toCST (AtAny _) _ = AT_META (anyMeta TAU)  instance ToCST Alpha ALPHA where   toCST (Alpha idx) _ = AL_IDX ALPHA idx   toCST (AlMeta mt) _ = AL_META ALPHA (META NO_EXCL I (metaTail mt))+  toCST (AlAny _) _ = AL_META ALPHA (anyMeta I)  instance ToCST Y.Condition CONDITION where   toCST (Y.Not (Y.In attr binding)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_BINDING (bindingsToCST [binding]))@@ -563,6 +576,7 @@  instance ToCST Y.Number NUMBER where   toCST (Y.MetaIndex mt) _ = IDX_META (META NO_EXCL I (metaTail mt))+  toCST (Y.AnyIndex _) _ = IDX_META (anyMeta I)   toCST (Y.Length binding) _ = LENGTH (bindingsToCST [binding])   toCST (Y.Domain binding) _ = DOMAIN (bindingsToCST [binding])   toCST (Y.Literal num) _ = LITERAL num

@@ -58,7 +58,7 @@         bd <- _binding phiParser         _ <- rparen         return (Y.Domain bd)-    , Y.MetaIndex <$> _index phiParser+    , either Y.AnyIndex Y.MetaIndex <$> _index phiParser     , do         sign <- optional (choice [char '-', char '+'])         unsigned <- lexeme L.decimal

@@ -10,14 +10,13 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Dataize (morph, morph', dataize, dataize', DataizeContext (..), DataizeException (..), Outcome (..), Steps (..), State, emptyState, execBuildTerm) where+module Dataize (morph, morph', dataize, dataize', insideUniverse, DataizeContext (..), DataizeException (..), Outcome (..), Steps (..), State, emptyState, execBuildTerm) where  import AST+import Atoms (Registry, fireAtom, registeredAtom) import Builder (buildBytesThrows, buildExpressionThrows)-import Bytes (btsAnd, btsConcat, btsEqual, btsNot, btsOr, btsShift, btsSize, btsSlice, btsToNum, numToBts, strToBts) import Control.Exception (Exception, catch, throwIO, try) import Control.Monad (foldM, when)-import Data.Int (Int32) import Data.List (find, partition) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE@@ -25,7 +24,6 @@ import Deps (BuildTermFunc, BuildTermMethodS, Evaluation (..), SaveEvalFunc, SaveStepFunc, State, Term (..)) import Locator (locatedExpression, withLocatedExpression) import Matcher (MetaValue (..), Subst (..), combine, matchExpression', substEmpty, substSingle)-import Misc import Must (Must (..)) import Random (shuffle) import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite)@@ -76,6 +74,7 @@   , _depthSensitive :: Bool   , _shuffle :: Bool   , _partial :: Bool+  , _atoms :: Registry   , _buildTerm :: BuildTermFunc   , _saveStep :: SaveStepFunc   , _saveEval :: SaveEvalFunc@@ -83,9 +82,10 @@  data DataizeException   = OutOfSteps Int-  | -- An atom could not fire: 'atom' does not know its λ function, or the-    -- dataization of one of its inputs met an atom it does not know. The name-    -- is that of the innermost unknown atom, the one 𝔼 actually failed on.+  | -- 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@@ -461,130 +461,43 @@     rewriteContext DataizeContext{..} =       RewriteContext _locator _maxDepth _maxCycles _depthSensitive _buildTerm MtDisabled Nothing _saveStep --- Synthetic dataize function for internal usage inside atoms. Here we modify the--- universe by adding a new binding which refers to the expression we want to--- dataize, building a local working expression to reduce within. As a caller of 𝔻,--- it first reduces the expression to a normal form, since 𝔻 only accepts normal--- forms. The universe 'univ' itself is forwarded unchanged, so morphing Φ under--- this context still resolves to the true universe rather than to this--- synthetic, binding-prepended formation. The chain is the synthetic one, so a--- stuck atom met on the way leaves without it (see 'unparked').-_dataize :: Expression -> Expression -> State -> DataizeContext -> IO (Bytes, State)-_dataize expr univ state ctx@DataizeContext{_buildTerm = buildTerm} = case univ of-  ExFormation bds -> unparked $ do+-- 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 synthetic = ExFormation (BiTau attr expr : bds)-    (normal, seq) <- normalized expr ((synthetic, Nothing) :| []) ctx-    ((bts, _), state') <- dataize' (normal, seq) univ state ctx-    pure (bts, state')-  _ -> throwIO (userError "Can't call _dataize from atoms with non-formation universe")---- A number atom only operates on numeric data. Empty bytes — a genuine--- zero-length byte array ⟦Δ ⤍ --⟧ — carry no number, so the operand is rejected--- and the atom yields ⊥. So does any byte array whose length is not 8: 'btsToNum'--- throws on such arrays, so the size is checked up front, exactly like 'asInt'.-asNumber :: Bytes -> Maybe Double-asNumber bts-  | btsSize bts /= 8 = Nothing-  | otherwise = Just (either toDouble id (btsToNum bts))---- An operand that EO reads as a Java 'int' — a shift distance or a slice bound.--- 'Expect.at(…).that(Integer)' turns down anything but a whole number inside the--- 32-bit range, and so does this, leaving the atom with ⊥-asInt :: Bytes -> Maybe Int-asInt bts-  | btsSize bts /= 8 = Nothing-  | otherwise = case btsToNum bts of-      Left num | num >= fromIntegral (minBound :: Int32) && num <= fromIntegral (maxBound :: Int32) -> Just num-      _ -> Nothing---- An atom whose EO signature ends in '/Q.bool' hands back one of the two bool--- objects of the universe, exactly what 'Data.ToPhi(boolean)' does in the runtime-boolean :: Bool -> Expression-boolean True = BaseObject "true"-boolean False = BaseObject "false"---- Both bitwise atoms take ρ and 'b' and reject operands of different lengths-bitwise :: (Bytes -> Bytes -> Maybe Bytes) -> Expression -> Expression -> State -> DataizeContext -> IO (Expression, State)-bitwise op self univ state ctx = do-  (b, bstate) <- _dataize (ExDispatch self (AtLabel "b")) univ state ctx-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ bstate ctx-  pure (maybe ExTermination dataBytes (op rho b), rstate)+    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") --- The 12 primitive λ-atoms every EO data operation reduces to. phino mirrors--- EO's set exactly: bytes {and, concat, eq, not, or, right, size, slice} and--- number {div, gt, plus, times}. There is deliberately no 'L_number_eq': EO's--- 'number.eq' (eo-runtime/src/main/eo/number/eq.eo) is pure EO — a formation--- composing 'is-nan', 'or', 'and' and 'L_bytes_eq', with no λ of its own — so--- nothing is left for a phino atom to implement. Names like 'L_bool_if' or--- 'L_string_slice' must stay unimplemented too: the EO lowering declares them--- precisely so that '--partial' parks on them and renders the call to Java.+-- 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 "L_number_plus" self univ state ctx = do-  (left, lstate) <- _dataize (ExDispatch self (AtLabel "x")) univ state ctx-  (right, rstate) <- _dataize (ExDispatch self AtRho) univ lstate ctx-  case (asNumber left, asNumber right) of-    (Just first, Just second) -> pure (DataNumber (numToBts (first + second)), rstate)-    _ -> pure (ExTermination, rstate)-atom "L_number_times" self univ state ctx = do-  (left, lstate) <- _dataize (ExDispatch self (AtLabel "x")) univ state ctx-  (right, rstate) <- _dataize (ExDispatch self AtRho) univ lstate ctx-  case (asNumber left, asNumber right) of-    (Just first, Just second) -> pure (DataNumber (numToBts (first * second)), rstate)-    _ -> pure (ExTermination, rstate)-atom "L_number_div" self univ state ctx = do-  (x, xstate) <- _dataize (ExDispatch self (AtLabel "x")) univ state ctx-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ xstate ctx-  case (asNumber x, asNumber rho) of-    (Just divisor, Just dividend) -> pure (DataNumber (numToBts (dividend / divisor)), rstate)-    _ -> pure (ExTermination, rstate)-atom "L_number_gt" self univ state ctx = do-  (x, xstate) <- _dataize (ExDispatch self (AtLabel "x")) univ state ctx-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ xstate ctx-  case (asNumber x, asNumber rho) of-    (Just threshold, Just value) -> pure (boolean (value > threshold), rstate)-    _ -> pure (ExTermination, rstate)-atom "L_bytes_and" self univ state ctx = bitwise btsAnd self univ state ctx-atom "L_bytes_or" self univ state ctx = bitwise btsOr self univ state ctx-atom "L_bytes_not" self univ state ctx = do-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ state ctx-  pure (dataBytes (btsNot rho), rstate)-atom "L_bytes_concat" self univ state ctx = do-  (b, bstate) <- _dataize (ExDispatch self (AtLabel "b")) univ state ctx-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ bstate ctx-  pure (dataBytes (btsConcat rho b), rstate)-atom "L_bytes_eq" self univ state ctx = do-  (b, bstate) <- _dataize (ExDispatch self (AtLabel "b")) univ state ctx-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ bstate ctx-  pure (boolean (btsEqual rho b), rstate)-atom "L_bytes_size" self univ state ctx = do-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ state ctx-  pure (DataNumber (numToBts (fromIntegral (btsSize rho))), rstate)-atom "L_bytes_right" self univ state ctx = do-  (x, xstate) <- _dataize (ExDispatch self (AtLabel "x")) univ state ctx-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ xstate ctx-  case asInt x of-    Just bits -> pure (dataBytes (btsShift bits rho), rstate)-    Nothing -> pure (ExTermination, rstate)-atom "L_bytes_slice" self univ state ctx = do-  (start, sstate) <- _dataize (ExDispatch self (AtLabel "start")) univ state ctx-  (len, lstate) <- _dataize (ExDispatch self (AtLabel "len")) univ sstate ctx-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ lstate ctx-  case (asInt start, asInt len) of-    (Just from, Just count)-      | from >= 0 && count >= 0 ->-          pure (maybe (cantSlice from count (btsSize rho)) dataBytes (btsSlice from count rho), rstate)-    _ -> pure (ExTermination, rstate)-  where-    -- A window past the end of the array does not stop EO: it copies the-    -- 'cant-slice' fallback, applies the complaint to it and lets the caller-    -- decide. A caller that left 'cant-slice' unbound gets ⊥ out of the dispatch-    cantSlice :: Int -> Int -> Int -> Expression-    cantSlice from count size =-      ExApplication-        (ExDispatch self (AtLabel "cant-slice"))-        (ArAlpha (Alpha 0) (DataString (strToBts (printf "cannot slice '%d' bytes from offset '%d' of bytes of size %d" count from size))))-atom func _ _ _ _ = throwIO (Stuck func)+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+    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@@ -609,14 +522,12 @@ -- 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. A nested firing — an atom that dataizes its own arguments —--- completes first, so it is reported before the firing that triggered it. A+-- 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, and the nested order holds, since the unknown--- atom is reported before the known one whose input reached it. The report is--- made before the signal goes on to the spine, where 'parking' attaches the--- derivation to it.+-- 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

@@ -22,9 +22,17 @@   | MvExpression Expression -- !e   deriving (Eq, Show) +-- The left-hand side of a substitution: a meta-variable the rule author named+-- and may reference from a result, or an anonymous slot that only the pattern+-- it was written in can address+data Meta+  = Named Text+  | Anon Slot+  deriving (Eq, Ord, Show)+ -- Substitution--- Shows the match of meta name to meta value-newtype Subst = Subst (Map Text MetaValue)+-- Shows the match of meta variable to meta value+newtype Subst = Subst (Map Meta MetaValue)   deriving (Eq, Show)  -- A way to match a pattern expression against a target expression, yielding@@ -37,14 +45,18 @@  -- Singleton substitution with one (key -> value) pair substSingle :: Text -> MetaValue -> Subst-substSingle key value = Subst (Map.singleton key value)+substSingle key value = Subst (Map.singleton (Named key) value) +-- Singleton substitution binding one anonymous slot+substSlot :: Slot -> MetaValue -> Subst+substSlot slot value = Subst (Map.singleton (Anon slot) value)+ -- Combine two substitutions into a single one -- Fails if values by the same keys are not equal combine :: Subst -> Subst -> Maybe Subst combine (Subst a) (Subst b) = go (Map.toList b) a   where-    go :: [(Text, MetaValue)] -> Map Text MetaValue -> Maybe Subst+    go :: [(Meta, MetaValue)] -> Map Meta MetaValue -> Maybe Subst     go [] acc = Just (Subst acc)     go ((key, value) : rest) acc = case Map.lookup key acc of       Just found@@ -57,18 +69,21 @@  matchAttribute :: Attribute -> Attribute -> [Subst] matchAttribute (AtMeta meta) tgt = [substSingle meta (MvAttribute tgt)]+matchAttribute (AtAny slot) tgt = [substSlot slot (MvAttribute tgt)] matchAttribute ptn tgt   | ptn == tgt = [substEmpty]   | otherwise = []  matchAlpha :: Alpha -> Alpha -> [Subst] matchAlpha (AlMeta meta) (Alpha idx) = [substSingle meta (MvIndex idx)]+matchAlpha (AlAny slot) (Alpha idx) = [substSlot slot (MvIndex idx)] matchAlpha ptn tgt   | ptn == tgt = [substEmpty]   | otherwise = []  matchFunction :: Function -> Function -> [Subst] matchFunction (FnMeta meta) (Function name) = [substSingle meta (MvFunction name)]+matchFunction (FnAny slot) (Function name) = [substSlot slot (MvFunction name)] matchFunction ptn tgt   | ptn == tgt = [substEmpty]   | otherwise = []@@ -76,6 +91,7 @@ matchBinding :: Binding -> Binding -> [Subst] matchBinding (BiVoid pattr) (BiVoid tattr) = matchAttribute pattr tattr matchBinding (BiDelta (BtMeta meta)) (BiDelta tdata) = [substSingle meta (MvBytes tdata)]+matchBinding (BiDelta (BtAny slot)) (BiDelta tdata) = [substSlot slot (MvBytes tdata)] matchBinding (BiDelta pdata) (BiDelta tdata)   | pdata == tdata = [substEmpty]   | otherwise = []@@ -92,18 +108,24 @@ matchBindings :: [Binding] -> [Binding] -> [Subst] matchBindings [] [] = [substEmpty] matchBindings [] _ = []-matchBindings ((BiMeta name) : pbs) tbs =-  let splits = [splitAt idx tbs | idx <- [0 .. length tbs]]-   in catMaybes-        [ combine (substSingle name (MvBindings before)) subst-        | (before, after) <- splits-        , subst <- matchBindings pbs after-        ]+matchBindings ((BiMeta name) : pbs) tbs = matchBindingsMeta (substSingle name) pbs tbs+matchBindings ((BiAny slot) : pbs) tbs = matchBindingsMeta (substSlot slot) pbs tbs matchBindings (pb : pbs) (tb : tbs) = combineMany (matchBinding pb tb) (matchBindings pbs tbs) matchBindings _ _ = [] +-- A meta binding stands for any leading run of the target bindings, so every+-- way of splitting the target into that run and the rest is tried.+matchBindingsMeta :: (MetaValue -> Subst) -> [Binding] -> [Binding] -> [Subst]+matchBindingsMeta bind pbs tbs =+  catMaybes+    [ combine (bind (MvBindings before)) subst+    | (before, after) <- [splitAt idx tbs | idx <- [0 .. length tbs]]+    , subst <- matchBindings pbs after+    ]+ matchExpression' :: MatchExpressionFunc matchExpression' (ExMeta meta) tgt = [substSingle meta (MvExpression tgt)]+matchExpression' (ExAny slot) tgt = [substSlot slot (MvExpression tgt)] matchExpression' ExXi ExXi = [substEmpty] matchExpression' ExRoot ExRoot = [substEmpty] matchExpression' ExTermination ExTermination = [substEmpty]

@@ -36,6 +36,7 @@ attributeFromBinding (BiDelta _) = Just AtDelta attributeFromBinding (BiLambda _) = Just AtLambda attributeFromBinding (BiMeta _) = Nothing+attributeFromBinding (BiAny _) = Nothing  -- Extract attributes from bindings attributesFromBindings :: [Binding] -> [Attribute]@@ -79,8 +80,11 @@     go (bd : rest) hasRho =       case bd of         BiMeta _ -> bd : rest+        BiAny _ -> bd : rest         BiVoid (AtMeta _) -> bd : rest+        BiVoid (AtAny _) -> bd : rest         BiTau (AtMeta _) _ -> bd : rest+        BiTau (AtAny _) _ -> bd : rest         BiVoid AtRho -> bd : go rest True         BiTau AtRho _ -> bd : go rest True         _ -> bd : go rest hasRho

@@ -48,14 +48,14 @@ data PhiParser = PhiParser   { _attribute :: Parser Attribute   , _alpha :: Parser Alpha-  , _index :: Parser T.Text+  , _index :: Parser (Either Slot T.Text)   , _binding :: Parser Binding   , _expression :: Parser Expression   , _string :: Parser String   }  phiParser :: PhiParser-phiParser = PhiParser attribute alpha index' binding expression quotedStr+phiParser = PhiParser attribute alpha indexVar binding expression quotedStr  instance Show ParserException where   show CouldNotParseExpression{..} = printf "Couldn't parse given phi expression, cause: %s" message@@ -122,23 +122,24 @@ metaSuffix :: Parser String metaSuffix = lexeme (many (oneOf ('_' : '-' : ['0' .. '9'] ++ ['a' .. 'z'] ++ ['A' .. 'Z']) <?> "meta suffix")) --- Meta variable names are packed to Text once here; all AST meta fields are Text-meta :: Char -> Parser T.Text-meta ch = do-  _ <- char '!'-  c <- char ch-  suf <- metaSuffix-  return (T.pack (c : suf))--meta' :: Char -> String -> Parser T.Text-meta' ch uni =-  choice-    [ meta ch-    , do-        _ <- string uni-        suf <- metaSuffix-        return (T.pack (ch : suf))-    ]+-- A meta-variable, written either in ASCII ('!t') or in Unicode ('𝜏'). The+-- suffix tells the two kinds apart: with one the variable is named and a rule+-- may reference it from its result, without one it is an anonymous slot+-- pinned to the offset it starts at, unique within the parsed term. Named+-- variables are packed to Text once here; all AST meta fields are Text.+metaVar :: Char -> String -> Parser (Either Slot T.Text)+metaVar ch uni = do+  offset <- getOffset+  suf <-+    choice+      [ char '!' >> char ch >> metaSuffix+      , string uni >> metaSuffix+      ]+  return+    ( if null suf+        then Left (Slot (T.singleton ch) offset)+        else Right (T.pack (ch : suf))+    )  byte :: Parser String byte = do@@ -160,7 +161,7 @@ bytes =   lexeme     ( choice-        [ BtMeta <$> meta' 'd' "δ"+        [ either BtAny BtMeta <$> metaVar 'd' "δ"         , symbol "--" >> return BtEmpty         , try $ do             first <- byte@@ -290,7 +291,7 @@     rb = symbol ")"  metaBinding :: Parser Binding-metaBinding = BiMeta <$> meta' 'B' "𝐵"+metaBinding = either BiAny BiMeta <$> metaVar 'B' "𝐵"  -- binding -- 1. delta@@ -313,7 +314,7 @@     , try metaBinding     , do         _ <- try lambda-        BiLambda <$> choice [Function . T.pack <$> function, FnMeta <$> meta' 'F' "𝑓"]+        BiLambda <$> choice [Function . T.pack <$> function, either FnAny FnMeta <$> metaVar 'F' "𝑓"]     , do         attr <- attribute         choice@@ -351,13 +352,13 @@ attribute =   choice     [ void'-    , AtMeta <$> meta' 't' "𝜏"+    , either AtAny AtMeta <$> metaVar 't' "𝜏"     ]     <?> "attribute"  -- index meta: !i, 𝑖-index' :: Parser T.Text-index' = meta' 'i' "𝑖"+indexVar :: Parser (Either Slot T.Text)+indexVar = metaVar 'i' "𝑖"  -- alpha -- 1. index: ~0, α0@@ -367,7 +368,7 @@   _ <- choice [symbol "~", symbol "α"]   choice     [ Alpha <$> lexeme L.decimal-    , AlMeta <$> index'+    , either AlAny AlMeta <$> indexVar     ]     <?> "alpha" @@ -423,9 +424,9 @@         return ExTermination     , number     , lexeme (DataString . strToBts <$> quotedStr)-    , try (ExMeta <$> meta' 'e' "𝑒")-    , try (ExMeta <$> meta' 'n' "𝑛")-    , try (ExMeta <$> meta' 'k' "𝑘")+    , try (either ExAny ExMeta <$> metaVar 'e' "𝑒")+    , try (either ExAny ExMeta <$> metaVar 'n' "𝑛")+    , try (either ExAny ExMeta <$> metaVar 'k' "𝑘")     , ExDispatch ExXi <$> attribute     ]     <?> "expression head"@@ -508,8 +509,8 @@ parseAlpha :: String -> Either String Alpha parseAlpha = parse' "alpha" alpha -parseIndex :: String -> Either String T.Text-parseIndex = parse' "index meta" index'+parseIndex :: String -> Either String (Either Slot T.Text)+parseIndex = parse' "index meta" indexVar  parseAttributeThrows :: String -> IO Attribute parseAttributeThrows attr = orThrow CouldNotParseAttribute (parseAttribute attr)

@@ -101,11 +101,19 @@ printMetaValue (MvBindings bds) config = printExpression' (ExFormation bds) config printMetaValue (MvFunction fun) _ = T.unpack fun +-- An anonymous slot is reported under the bare sigil it was written with,+-- just as a named meta is reported under its name. Two slots of one kind+-- therefore share a line label while keeping their own values, which is all+-- the report can say about a variable no rule may refer back to.+printMeta :: Meta -> String+printMeta (Named name) = T.unpack name+printMeta (Anon (Slot kind _)) = T.unpack kind+ printSubst :: Subst -> PrintConfig -> String printSubst (Subst mp) config =   intercalate     "\n"-    (map (\(key, value) -> T.unpack key <> " >> " <> printMetaValue value config) (Map.toList mp))+    (map (\(key, value) -> printMeta key <> " >> " <> printMetaValue value config) (Map.toList mp))  printSubsts' :: [Subst] -> PrintConfig -> String printSubsts' [] _ = "------"

@@ -163,6 +163,7 @@     isMetaBinding :: Binding -> Bool     isMetaBinding = \case       BiMeta _ -> True+      BiAny _ -> True       _ -> False     hasMetaBindings = foldl (\acc bd -> acc || isMetaBinding bd) False tryBuildAndReplaceFast state _ = buildAndReplace' state replaceExpression

@@ -113,13 +113,13 @@ -- Convert a 'Number' to an 'Int' under the given substitution, resolving -- index metas, binding lengths and formation domains. numToInt :: Y.Number -> Subst -> Maybe Int-numToInt (Y.MetaIndex meta) (Subst mp) = case M.lookup meta mp of+numToInt (Y.MetaIndex meta) (Subst mp) = case M.lookup (Named meta) mp of   Just (MvIndex idx) -> Just idx   _ -> Nothing-numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of+numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup (Named meta) mp of   Just (MvBindings bds) -> Just (length bds)   _ -> Nothing-numToInt (Y.Domain (BiMeta meta)) (Subst mp) = case M.lookup meta mp of+numToInt (Y.Domain (BiMeta meta)) (Subst mp) = case M.lookup (Named meta) mp of   Just (MvBindings bds) -> Just (length (filter notAsset bds))   _ -> Nothing   where@@ -136,26 +136,26 @@ _eq (Y.CmpAttr left) (Y.CmpAttr right) subst _ = pure [subst | compareAttrs left right subst]   where     compareAttrs :: Attribute -> Attribute -> Subst -> Bool-    compareAttrs (AtMeta left) (AtMeta right) (Subst mp) = case (M.lookup left mp, M.lookup right mp) of+    compareAttrs (AtMeta left) (AtMeta right) (Subst mp) = case (M.lookup (Named left) mp, M.lookup (Named right) mp) of       (Just (MvAttribute left'), Just (MvAttribute right')) -> compareAttrs left' right' (Subst mp)       _ -> False-    compareAttrs attr (AtMeta meta) (Subst mp) = case M.lookup meta mp of+    compareAttrs attr (AtMeta meta) (Subst mp) = case M.lookup (Named meta) mp of       Just (MvAttribute found) -> attr == found       _ -> False-    compareAttrs (AtMeta meta) attr (Subst mp) = case M.lookup meta mp of+    compareAttrs (AtMeta meta) attr (Subst mp) = case M.lookup (Named meta) mp of       Just (MvAttribute found) -> attr == found       _ -> False     compareAttrs left right _ = right == left _eq (Y.CmpExpr left) (Y.CmpExpr right) subst _ = pure [subst | compareExprs left right subst]   where     compareExprs :: Expression -> Expression -> Subst -> Bool-    compareExprs (ExMeta left) (ExMeta right) (Subst mp) = case (M.lookup left mp, M.lookup right mp) of+    compareExprs (ExMeta left) (ExMeta right) (Subst mp) = case (M.lookup (Named left) mp, M.lookup (Named right) mp) of       (Just (MvExpression left'), Just (MvExpression right')) -> compareExprs left' right' (Subst mp)       _ -> False-    compareExprs expr (ExMeta meta) (Subst mp) = case M.lookup meta mp of+    compareExprs expr (ExMeta meta) (Subst mp) = case M.lookup (Named meta) mp of       Just (MvExpression found) -> expr == found       _ -> False-    compareExprs (ExMeta meta) expr (Subst mp) = case M.lookup meta mp of+    compareExprs (ExMeta meta) expr (Subst mp) = case M.lookup (Named meta) mp of       Just (MvExpression found) -> expr == found       _ -> False     compareExprs left right _ = left == right@@ -170,9 +170,12 @@ _gt _ _ _ _ = pure []  _nf :: Expression -> Subst -> RuleContext -> IO [Subst]-_nf (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of+_nf (ExMeta meta) (Subst mp) ctx = case M.lookup (Named meta) mp of   Just (MvExpression expr) -> _nf expr (Subst mp) ctx   _ -> pure []+_nf (ExAny slot) (Subst mp) ctx = case M.lookup (Anon slot) mp of+  Just (MvExpression expr) -> _nf expr (Subst mp) ctx+  _ -> pure [] _nf expr subst ctx = pure [subst | isNF expr ctx]  -- An expression is xi-free when it contains no ξ outside of a formation: it is@@ -184,9 +187,12 @@ -- structural, rules out the ξ-recursion the normal-form check could loop on) -- and the normal-form check second. _absolute :: Expression -> Subst -> RuleContext -> IO [Subst]-_absolute (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of+_absolute (ExMeta meta) (Subst mp) ctx = case M.lookup (Named meta) mp of   Just (MvExpression expr) -> _absolute expr (Subst mp) ctx   _ -> pure []+_absolute (ExAny slot) (Subst mp) ctx = case M.lookup (Anon slot) mp of+  Just (MvExpression expr) -> _absolute expr (Subst mp) ctx+  _ -> pure [] _absolute expr subst _ = pure [subst | xiFree expr]   where     xiFree :: Expression -> Bool@@ -201,7 +207,7 @@ -- Hold when the given expression is a formation (an abstraction ⟦…⟧). A meta -- is resolved first, so 'binding 𝑛' inspects whatever 𝑛 is bound to. _isFormation :: Expression -> Subst -> RuleContext -> IO [Subst]-_isFormation (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of+_isFormation (ExMeta meta) (Subst mp) ctx = case M.lookup (Named meta) mp of   Just (MvExpression expr) -> _isFormation expr (Subst mp) ctx   _ -> pure [] _isFormation expr subst _ = pure [subst | isFormation expr]@@ -211,7 +217,7 @@     isFormation _ = False  _matches :: String -> Expression -> Subst -> RuleContext -> IO [Subst]-_matches pat (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of+_matches pat (ExMeta meta) (Subst mp) ctx = case M.lookup (Named meta) mp of   Just (MvExpression expr) -> _matches pat expr (Subst mp) ctx   _ -> pure [] _matches pat expr subst ctx = do@@ -328,27 +334,32 @@     logDebug "Extra substitutions have been built"     pure (catMaybes res) --- Collect the names of constrained expression meta-variables with the given+-- Collect the constrained expression meta-variables with the given -- one-character prefix used in a pattern. Each kind ('𝑛'/'!n' normal-form, -- '𝑘'/'!k' absolute) lives in its own 'n'-/'k'-prefixed key-space, so a--- pattern may freely mix them with plain '𝑒' captures.-metaNamesWithPrefix :: T.Text -> Expression -> [T.Text]-metaNamesWithPrefix prefix = nub . go+-- pattern may freely mix them with plain '𝑒' captures. An anonymous meta+-- carries the same prefix as the sigil it was written with, so a bare '𝑛' is+-- held to the normal form just as '𝑛1' is.+metasWithPrefix :: T.Text -> Expression -> [Expression]+metasWithPrefix prefix = nub . go   where-    go :: Expression -> [T.Text]-    go (ExMeta mt)-      | T.isPrefixOf prefix mt = [mt]+    go :: Expression -> [Expression]+    go expr@(ExMeta mt)+      | T.isPrefixOf prefix mt = [expr]       | otherwise = []+    go expr@(ExAny (Slot kind _))+      | T.isPrefixOf prefix kind = [expr]+      | otherwise = []     go (ExFormation bds) = concatMap goBinding bds     go (ExApplication e arg) = go e ++ goArgument arg     go (ExDispatch e _) = go e     go (ExPhiMeet _ _ e) = go e     go (ExPhiAgain _ _ e) = go e     go _ = []-    goBinding :: Binding -> [T.Text]+    goBinding :: Binding -> [Expression]     goBinding (BiTau _ e) = go e     goBinding _ = []-    goArgument :: Argument -> [T.Text]+    goArgument :: Argument -> [Expression]     goArgument (ArTau _ expr) = go expr     goArgument (ArAlpha _ expr) = go expr @@ -381,8 +392,8 @@           -- A '𝑘' meta-variable is absolute (𝒦 ⊆ 𝒩): check it is xi-free first           -- (cheap, structural), then fold its name into the same normal-form           -- check used for '𝑛' metas, so 'isNF' is applied in a single place.-          inXiFree <- foldlM (\substs nm -> meetCondition (Y.Absolute (ExMeta nm)) substs ctx) matched (kMetaNames ptn)-          inNf <- foldlM (\substs nm -> meetCondition (Y.NF (ExMeta nm)) substs ctx) inXiFree (nfMetaNames ptn ++ kMetaNames ptn)+          inXiFree <- foldlM (\substs mt -> meetCondition (Y.Absolute mt) substs ctx) matched (kMetas ptn)+          inNf <- foldlM (\substs mt -> meetCondition (Y.NF mt) substs ctx) inXiFree (nfMetas ptn ++ kMetas ptn)           if null inNf             then do               logDebug "A '𝑛'/'𝑘' meta-variable is not in normal form, or a '𝑘' meta-variable is not xi-free"@@ -405,8 +416,8 @@                       when (null met) (logDebug "The 'having' condition wasn't met")                       pure met   where-    nfMetaNames :: Expression -> [T.Text]-    nfMetaNames = metaNamesWithPrefix "n"+    nfMetas :: Expression -> [Expression]+    nfMetas = metasWithPrefix "n" -    kMetaNames :: Expression -> [T.Text]-    kMetaNames = metaNamesWithPrefix "k"+    kMetas :: Expression -> [Expression]+    kMetas = metasWithPrefix "k"

@@ -0,0 +1,65 @@+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++-- The goal of the module is to collect the anonymous meta-variable slots a+-- term was written with. A rule binds them where it matches and nowhere else,+-- so every other part of a rule is asked for its slots and rejected when it+-- has any.+module Slots (Slots (..), anonymous) where++import AST+import Data.Text (Text)++class Slots a where+  slots :: a -> [Slot]++-- The kind sigil of the first anonymous meta a term was written with, if any,+-- so a caller can word its own complaint about a term that must have none+anonymous :: (Slots a) => a -> Maybe Text+anonymous term = case slots term of+  [] -> Nothing+  Slot kind _ : _ -> Just kind++instance (Slots a) => Slots [a] where+  slots = concatMap slots++instance (Slots a) => Slots (Maybe a) where+  slots = maybe [] slots++instance Slots Expression where+  slots (ExAny slot) = [slot]+  slots (ExFormation bds) = slots bds+  slots (ExApplication expr arg) = slots expr ++ slots arg+  slots (ExDispatch expr attr) = slots expr ++ slots attr+  slots (ExPhiMeet _ _ expr) = slots expr+  slots (ExPhiAgain _ _ expr) = slots expr+  slots (ExBytes bts) = slots bts+  slots _ = []++instance Slots Argument where+  slots (ArTau attr expr) = slots attr ++ slots expr+  slots (ArAlpha alpha expr) = slots alpha ++ slots expr++instance Slots Binding where+  slots (BiAny slot) = [slot]+  slots (BiTau attr expr) = slots attr ++ slots expr+  slots (BiVoid attr) = slots attr+  slots (BiDelta bts) = slots bts+  slots (BiLambda func) = slots func+  slots (BiMeta _) = []++instance Slots Attribute where+  slots (AtAny slot) = [slot]+  slots _ = []++instance Slots Alpha where+  slots (AlAny slot) = [slot]+  slots _ = []++instance Slots Bytes where+  slots (BtAny slot) = [slot]+  slots _ = []++instance Slots Function where+  slots (FnAny slot) = [slot]+  slots _ = []

@@ -1,6 +1,7 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TemplateHaskell #-} {-# OPTIONS_GHC -Wno-orphans #-}@@ -22,6 +23,7 @@ import qualified Data.Yaml as Yaml import GHC.Generics (Generic) import Parser+import Slots import Text.Printf (printf)  -- Fail unless the object names exactly one of the expected keys@@ -81,7 +83,8 @@       | toRational (round num :: Integer) == toRational num -> pure (Literal (round num))       | otherwise -> fail (printf "Expected an integer, got a fractional number %s" (show num))     String txt -> case parseIndex (unpack txt) of-      Right mt -> pure (MetaIndex mt)+      Right (Right mt) -> pure (MetaIndex mt)+      Right (Left slot) -> pure (AnyIndex slot)       Left err -> fail err     _ ->       fail "Expected a numerable expression (object, number or index meta)"@@ -172,16 +175,24 @@       )  instance FromJSON Rule where-  parseJSON =-    genericParseJSON-      defaultOptions-        { fieldLabelModifier = \case-            "where_" -> "where"-            other -> other-        }+  parseJSON value = do+    rule <-+      genericParseJSON+        defaultOptions+          { fieldLabelModifier = \case+              "where_" -> "where"+              other -> other+          }+        value+    referenceless rule.name "result" rule.result+    referenceless rule.name "when" rule.when+    referenceless rule.name "where" rule.where_+    referenceless rule.name "having" rule.having+    pure rule  data Number   = MetaIndex Text+  | AnyIndex Slot   | Length Binding   | Domain Binding   | Literal Int@@ -234,6 +245,68 @@   }   deriving (Generic, Show) +instance Slots Condition where+  slots (And conds) = slots conds+  slots (Or conds) = slots conds+  slots (Not cond) = slots cond+  slots (In attr bd) = slots attr ++ slots bd+  slots (Eq left right) = slots left ++ slots right+  slots (Gt left right) = slots left ++ slots right+  slots (NF expr) = slots expr+  slots (Absolute expr) = slots expr+  slots (Matches _ expr) = slots expr+  slots (PartOf expr bd) = slots expr ++ slots bd+  slots (Disjoint attrs bds) = slots attrs ++ slots bds+  slots (IsFormation expr) = slots expr++instance Slots Comparable where+  slots (CmpAttr attr) = slots attr+  slots (CmpNum num) = slots num+  slots (CmpExpr expr) = slots expr++instance Slots Number where+  slots (AnyIndex slot) = [slot]+  slots (Length bd) = slots bd+  slots (Domain bd) = slots bd+  slots (MetaIndex _) = []+  slots (Literal _) = []++instance Slots ExtraArgument where+  slots (ArgAttribute attr) = slots attr+  slots (ArgExpression expr) = slots expr+  slots (ArgBinding bd) = slots bd+  slots (ArgBytes bts) = slots bts++instance Slots Extra where+  slots extra = slots extra.meta ++ slots extra.args++instance Slots Premise where+  slots premise = slots premise.operation++instance Slots Operation where+  slots (OpMorph expr) = slots expr+  slots (OpNormalize expr) = slots expr+  slots (OpEvaluate expr universe) = slots expr ++ slots universe+  slots (OpContextualize expr context) = slots expr ++ slots context+  slots (OpDataize expr) = slots expr++-- An anonymous meta-variable is bound by the pattern it stands in and is+-- forgotten as soon as that pattern matches, so it has no name for any other+-- part of a rule to read it back by. Writing one outside the pattern is+-- therefore a mistake in the rule, not a term to be resolved later, and the+-- rule is rejected as it loads.+referenceless :: (MonadFail m, Slots a) => String -> String -> a -> m ()+referenceless rule field term = case anonymous term of+  Nothing -> pure ()+  Just kind ->+    fail+      ( printf+          "anonymous meta '!%s' cannot be referenced in '%s' of rule '%s'"+          (unpack kind)+          field+          rule+      )+ normalizationRules :: [Rule] {-# NOINLINE normalizationRules #-} normalizationRules = map decodeRule $(embedDir "resources/normalize")@@ -323,11 +396,13 @@   expr <- o .:? "n-result"   case expr of     Just (ExMeta metaName) -> pure metaName+    Just (ExAny _) -> fail "an anonymous 'n-result' meta cannot be referenced"     Just _ -> fail "'n-result' must be an expression meta"     Nothing -> do       bytes <- o .:? "d-result"       case bytes of         Just (BtMeta metaName) -> pure metaName+        Just (BtAny _) -> fail "an anonymous 'd-result' meta cannot be referenced"         Just _ -> fail "'d-result' must be a bytes meta"         Nothing -> fail "a premise needs an 'n-result' or 'd-result' meta" @@ -367,13 +442,18 @@       "MorphRule"       ( \o -> do           ruleName <- o .: "name"-          MorphRule ruleName-            <$> parseLabel ruleName o-            <*> o .: "match"-            <*> o .: "e-match"-            <*> o .: "n-result"-            <*> o .:? "when"-            <*> o .:? "premises" .!= []+          rule <-+            MorphRule ruleName+              <$> parseLabel ruleName o+              <*> o .: "match"+              <*> o .: "e-match"+              <*> o .: "n-result"+              <*> o .:? "when"+              <*> o .:? "premises" .!= []+          referenceless ruleName "n-result" rule.nresult+          referenceless ruleName "when" rule.when+          referenceless ruleName "premises" rule.premises+          pure rule       )  instance FromJSON DataizeRule where@@ -382,13 +462,18 @@       "DataizeRule"       ( \o -> do           ruleName <- o .: "name"-          DataizeRule ruleName-            <$> parseLabel ruleName o-            <*> o .: "match"-            <*> o .: "e-match"-            <*> o .: "d-result"-            <*> o .:? "when"-            <*> o .:? "premises" .!= []+          rule <-+            DataizeRule ruleName+              <$> parseLabel ruleName o+              <*> o .: "match"+              <*> o .: "e-match"+              <*> o .: "d-result"+              <*> o .:? "when"+              <*> o .:? "premises" .!= []+          referenceless ruleName "d-result" rule.dresult+          referenceless ruleName "when" rule.when+          referenceless ruleName "premises" rule.premises+          pure rule       )  instance FromJSON ContextualizeRule where@@ -397,12 +482,16 @@       "ContextualizeRule"       ( \o -> do           ruleName <- o .: "name"-          ContextualizeRule ruleName-            <$> parseLabel ruleName o-            <*> o .: "match"-            <*> o .: "c-match"-            <*> o .: "c-result"-            <*> o .:? "premises" .!= []+          rule <-+            ContextualizeRule ruleName+              <$> parseLabel ruleName o+              <*> o .: "match"+              <*> o .: "c-match"+              <*> o .: "c-result"+              <*> o .:? "premises" .!= []+          referenceless ruleName "c-result" rule.cresult+          referenceless ruleName "premises" rule.premises+          pure rule       )  decodeRules :: (FromJSON a) => FilePath -> BS.ByteString -> [a]

@@ -0,0 +1,154 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}++-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++module AtomsSpec (spec) where++import AST+import Atoms (Atom (..), Runtime (RtNode), emptyRegistry, fireAtom, readRegistry, registeredAtom)+import Control.Exception (SomeException, bracket)+import Control.Monad (forM_)+import Data.ByteString qualified as BS+import Data.List (isInfixOf)+import Data.Text qualified as T+import Data.Text.Encoding (encodeUtf8)+import Fixtures (withNode)+import Parser (parseExpressionThrows)+import System.Directory (getTemporaryDirectory, removePathForcibly)+import System.IO (Handle, hClose, openBinaryTempFile)+import Test.Hspec++-- A registry file holding the given content, removed afterwards+withRegistry :: T.Text -> (FilePath -> IO a) -> IO a+withRegistry content action = do+  dir <- getTemporaryDirectory+  bracket (openBinaryTempFile dir "phino-registry-.json") discarded $ \(path, handle) -> do+    BS.hPut handle (encodeUtf8 content)+    hClose handle+    action path+  where+    discarded :: (FilePath, Handle) -> IO ()+    discarded (path, handle) = hClose handle >> removePathForcibly path++-- Fire the λ function 'L_answer' out of the given script, against a formation+-- binding 'x' inside a universe binding 'y'+fired :: T.Text -> IO Expression+fired script = do+  form <- parseExpressionThrows "⟦ x ↦ ⟦ Δ ⤍ 01- ⟧ ⟧"+  univ <- parseExpressionThrows "⟦ y ↦ ⟦ Δ ⤍ 02- ⟧ ⟧"+  fireAtom "L_answer" (Atom RtNode script) form univ++-- What the script wrote under 'n' has to come back parsed, so a case asserting+-- on it says which expression it expects in 𝜑 rather than in constructors+answers :: T.Text -> String -> Expectation+answers script expected = withNode $ do+  answer <- fired script+  wanted <- parseExpressionThrows expected+  answer `shouldBe` wanted++-- A firing that has to fail, with the reason naming the given fragments+fails :: T.Text -> [String] -> Expectation+fails script fragments =+  withNode $+    fired script+      `shouldThrow` (\failure -> all (`isInfixOf` show (failure :: SomeException)) fragments)++spec :: Spec+spec = do+  -- phino implements no λ function, so an empty registry is what a run without+  -- '--atoms' fires against: every name is unknown there+  describe "emptyRegistry" $+    it "registers no λ function at all" $+      registeredAtom emptyRegistry "L_bytes_eq" `shouldBe` Nothing++  describe "readRegistry" $ do+    it "reads a λ function together with its runtime and script" $+      withRegistry "{\"L_answer\": {\"rt\": \"node\", \"script\": \"say(1)\"}}" $ \path -> do+        registry <- readRegistry path+        registeredAtom registry "L_answer" `shouldBe` Just (Atom RtNode "say(1)")++    it "leaves a name the file does not carry unregistered" $+      withRegistry "{\"L_answer\": {\"rt\": \"node\", \"script\": \"say(1)\"}}" $ \path -> do+        registry <- readRegistry path+        registeredAtom registry "L_bytes_eq" `shouldBe` Nothing++    -- An unknown runtime is refused where the file is read, which is before any+    -- dataization starts, rather than at the moment an atom of it would fire+    forM_+      [+        ( "the runtime is not one phino can run"+        , "{\"L_answer\": {\"rt\": \"ruby\", \"script\": \"say(1)\"}}"+        , ["unknown runtime 'ruby'", "node"]+        )+      ,+        ( "an entry carries no script"+        , "{\"L_answer\": {\"rt\": \"node\"}}"+        , ["script"]+        )+      ,+        ( "an entry carries no runtime"+        , "{\"L_answer\": {\"script\": \"say(1)\"}}"+        , ["rt"]+        )+      ,+        ( "the file is not JSON at all"+        , "L_answer: js"+        , ["cannot be read"]+        )+      ]+      ( \(desc, content, fragments) ->+          it ("fails when " ++ desc) $+            withRegistry content $ \path ->+              readRegistry path+                `shouldThrow` (\failure -> all (`isInfixOf` show (failure :: SomeException)) fragments)+      )++    it "fails when the file is not there" $+      readRegistry "no-such-registry.json"+        `shouldThrow` (\failure -> "cannot be read" `isInfixOf` show (failure :: SomeException))++  describe "fireAtom" $ do+    it "hands back the 𝜑-expression the script wrote under 'n'" $+      answers "process.stdout.write(JSON.stringify({n: '⟦ Δ ⤍ 2A- ⟧'}))" "⟦ Δ ⤍ 2A- ⟧"++    -- One script may stand for several λ functions, so the name of the one+    -- being fired is its first command-line argument — where node puts it+    it "names the λ function being fired as the first command-line argument" $+      answers+        "process.stdout.write(JSON.stringify({n: process.argv[2] === 'L_answer' ? '⟦ Δ ⤍ FF- ⟧' : '⟦ Δ ⤍ 00- ⟧'}))"+        "⟦ Δ ⤍ FF- ⟧"++    -- The formation being evaluated arrives under 'b' and the universe Φ under+    -- 's', both as 𝜑 text on stdin+    it "feeds the formation and the universe to the script on stdin" $+      answers+        "const {b, s} = JSON.parse(require('fs').readFileSync(0, 'utf8'));\+        \process.stdout.write(JSON.stringify({n: b.includes('x ↦') && s.includes('y ↦') ? '⟦ Δ ⤍ FF- ⟧' : '⟦ Δ ⤍ 00- ⟧'}))"+        "⟦ Δ ⤍ FF- ⟧"++    -- Neither payload carries syntax sugar, whatever '--sweet' says about the+    -- output of the run, so a script finds every datum spelled as a Δ binding+    it "spells the payloads as canonical 𝜑-calculus" $+      answers+        "const {b} = JSON.parse(require('fs').readFileSync(0, 'utf8'));\+        \process.stdout.write(JSON.stringify({n: b.includes('Δ ⤍ 01-') ? '⟦ Δ ⤍ FF- ⟧' : '⟦ Δ ⤍ 00- ⟧'}))"+        "⟦ Δ ⤍ FF- ⟧"++    it "reads a script that says nothing to stdin without waiting for it" $+      answers "process.stdout.write(JSON.stringify({n: '⟦ Δ ⤍ 01- ⟧'}))" "⟦ Δ ⤍ 01- ⟧"++    it "fails with the script's own complaint when it exits non-zero" $+      fails+        "process.stderr.write('no idea what to do');process.exit(4)"+        ["L_answer", "exit code 4", "no idea what to do"]++    it "fails when the script writes something other than JSON" $+      fails "process.stdout.write('almost')" ["L_answer", "almost"]++    it "fails when the script writes JSON with no 'n' in it" $+      fails "process.stdout.write(JSON.stringify({m: '⟦ ⟧'}))" ["L_answer", "n"]++    it "fails when what the script put under 'n' is not a 𝜑-expression" $+      fails "process.stdout.write(JSON.stringify({n: '⟦ ⟧⟧'}))" ["L_answer"]

@@ -19,7 +19,7 @@ test :: (Show a, Eq a) => (a -> Subst -> Either String a) -> [(String, a, [(T.Text, MetaValue)], Either String a)] -> SpecWith (Arg Expectation) test function useCases =   forM_ useCases $ \(desc, expr, mp, res) ->-    it desc $ function expr (Subst (Map.fromList mp)) `shouldBe` res+    it desc $ function expr (Subst (Map.mapKeys Named (Map.fromList mp))) `shouldBe` res  spec :: Spec spec = do@@ -208,6 +208,38 @@         )       ]       (\(desc, action, message) -> it desc (action `shouldThrow` (\exc -> message `isInfixOf` show (exc :: SomeException))))++  describe "builds an anonymous meta only from the pattern that bound it" $ do+    -- An anonymous slot is a key of the very substitution its own pattern+    -- produced, which is how a fired pattern is rebuilt for replacement. Asked+    -- for it under any other substitution, the builder says plainly that the+    -- meta has no name to be referenced by, rather than inventing a term.+    forM_+      [+        ( "buildExpression rebuilds an anonymous expression from its own slot"+        , buildExpression (ExAny (Slot "e" 7)) (substSlot (Slot "e" 7) (MvExpression ExRoot))+        , Right ExRoot+        )+      ,+        ( "buildExpression refuses an anonymous expression bound by another pattern"+        , buildExpression (ExAny (Slot "e" 7)) (substSlot (Slot "e" 9) (MvExpression ExRoot))+        , Left "anonymous meta '!e' cannot be referenced"+        )+      ]+      (\(desc, built, expected) -> it desc (built `shouldBe` expected))+    forM_+      [+        ( "buildAttribute rebuilds an anonymous attribute from its own slot"+        , buildAttribute (AtAny (Slot "t" 2)) (substSlot (Slot "t" 2) (MvAttribute AtPhi))+        , Right AtPhi+        )+      ,+        ( "buildAttribute refuses an anonymous attribute bound by another pattern"+        , buildAttribute (AtAny (Slot "t" 2)) substEmpty+        , Left "anonymous meta '!t' cannot be referenced"+        )+      ]+      (\(desc, built, expected) -> it desc (built `shouldBe` expected))    describe "build with duplicate attributes in bindings" $ do     it "build binding with duplicates" $

@@ -15,6 +15,7 @@ import Data.Time.Clock (addUTCTime, getCurrentTime) import Data.Time.Clock.POSIX (getPOSIXTime) import Data.Version (showVersion)+import Fixtures (withFixtureRegistry, withNode) import GHC.IO.Handle import Paths_phino (version) import System.Directory (createDirectoryIfMissing, doesDirectoryExist, doesFileExist, getTemporaryDirectory, listDirectory, removeDirectoryRecursive, removeFile, removePathForcibly, setModificationTime)@@ -119,6 +120,13 @@ testCLISucceeded :: [String] -> [String] -> Expectation testCLISucceeded args outputs = testCLI' args outputs (Right ()) +-- phino implements no λ function of its own, so a case that needs an atom to+-- fire brings the fixture registry in and hands its path to the command as+-- '--atoms' (see 'Fixtures'). Every such atom runs under 'node', so the case is+-- pending where 'node' is not installed.+withAtoms :: (String -> Expectation) -> Expectation+withAtoms action = withNode (withFixtureRegistry (action . ("--atoms=" ++)))+ testCLIFailed :: [String] -> [String] -> Expectation testCLIFailed args outputs = testCLI' args outputs (Left (ExitFailure 1)) @@ -392,20 +400,21 @@           doesFileExist (dir ++ "/00003.phi") `shouldReturn` True      it "saves dataize steps to dir with --steps-dir" $-      withTempDirectory "phino-steps-dataize" $ \dir ->-        withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ do-          testCLISucceeded-            ["dataize", "--steps-dir=" ++ dir, "--sweet"]-            ["40-26"]-          doesDirectoryExist dir `shouldReturn` True-          files <- listDirectory dir-          let steps = sort files-          -- The fix is about numbering, not about a specific rule set: the file-          -- names must be distinct and contiguous from 00001, and there must be-          -- more of them than a single normalization pass produces (this input-          -- runs several normalizations, so a global counter yields more steps).-          steps `shouldBe` map (\n -> printf "%05d.phi" (n :: Int)) [1 .. length steps]-          length steps `shouldSatisfy` (> 18)+      withAtoms $ \atoms ->+        withTempDirectory "phino-steps-dataize" $ \dir ->+          withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $ do+            testCLISucceeded+              ["dataize", atoms, "--steps-dir=" ++ dir, "--sweet"]+              ["40-32"]+            doesDirectoryExist dir `shouldReturn` True+            files <- listDirectory dir+            let steps = sort files+            -- The fix is about numbering, not about a specific rule set: the file+            -- names must be distinct and contiguous from 00001, and there must be+            -- more of them than a single normalization pass produces (this input+            -- runs several normalizations, so a global counter yields more steps).+            steps `shouldBe` map (\n -> printf "%05d.phi" (n :: Int)) [1 .. length steps]+            length steps `shouldSatisfy` (> 18)      it "saves steps with a .tex extension when --output=latex is used with --steps-dir" $       withTempDirectory "phino-steps-latex" $ \dir ->@@ -1070,10 +1079,11 @@     -- The 𝕄/𝔻 recursion used to be unbounded, so this division kept morphing     -- forever and no option could stop it (#1052)     it "fails on --max-steps instead of morphing forever" $-      withStdin "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧" $-        testCLIFailed-          ["dataize", "--max-steps=40"]-          ["[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=40"]+      withAtoms $ \atoms ->+        withStdin "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧" $+          testCLIFailed+            ["dataize", atoms, "--max-steps=40"]+            ["[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=40"]      it "dataizes with --sequence" $       withStdin "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]" $@@ -1112,16 +1122,18 @@           ["⟦ Δ ⤍ 01- ⟧\n01-"]      it "focuses a compressed sequence whose meet replaces a step root" $-      withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $-        testCLISucceeded-          ["dataize", "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--hide=Q.bytes", "--hide=Q.number", "--locator=Q.@", "--focus=Q.@", "--meet-length=5", "--meet-popularity=1"]-          ["\\phinoMeet{dataization:1}{ [[ @ -> |c| . |plus| ( 32 ), |c| -> 25 ]] } \\leadsto_{\\nameref{r:contextualize}}"]+      withAtoms $ \atoms ->+        withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $+          testCLISucceeded+            ["dataize", atoms, "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--hide=Q.bytes", "--hide=Q.number", "--locator=Q.@", "--focus=Q.@", "--meet-length=5", "--meet-popularity=1"]+            ["\\phinoMeet{dataization:1}{ [[ @ -> |c| . |plus| ( 32 ), |c| -> 25 ]] } \\leadsto_{\\nameref{r:contextualize}}"]      it "compresses a canonized whole-expression sequence into a meet" $-      withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $-        testCLISucceeded-          ["dataize", "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--meet-length=5", "--meet-popularity=1"]-          ["\\phinoMeet{dataization:1}"]+      withAtoms $ \atoms ->+        withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $+          testCLISucceeded+            ["dataize", atoms, "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--meet-length=5", "--meet-popularity=1"]+            ["\\phinoMeet{dataization:1}"]      it "dataizes with --locator" $       withStdin "[[ ex -> [[ @ -> Q.x ]], x -> [[ D> 42- ]] ]]" $@@ -1133,38 +1145,42 @@      describe "--evaluations" $ do       it "writes one tab-separated record per fired atom" $-        withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do-          hClose stream-          withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $-            testCLISucceeded ["dataize", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []-          records <- readUtf8 path-          records `shouldBe` "L_number_plus\t⟦ x ↦ 6 ⟧\t11\n"+        withAtoms $ \atoms ->+          withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do+            hClose stream+            withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $+              testCLISucceeded ["dataize", atoms, "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []+            records <- readUtf8 path+            records `shouldBe` "L_number_plus\t⟦ x ↦ 6 ⟧\t11\n"        it "writes a record for every firing" $-        withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do-          hClose stream-          withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $-            testCLISucceeded ["dataize", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []-          records <- readUtf8 path-          lines records `shouldBe` ["L_number_plus\t⟦ x ↦ 6 ⟧\t11", "L_number_plus\t⟦ x ↦ 7 ⟧\t18"]+        withAtoms $ \atoms ->+          withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do+            hClose stream+            withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $+              testCLISucceeded ["dataize", atoms, "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []+            records <- readUtf8 path+            lines records `shouldBe` ["L_number_plus\t⟦ x ↦ 6 ⟧\t11", "L_number_plus\t⟦ x ↦ 7 ⟧\t18"]        it "writes records in canonical syntax without --sweet" $-        withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do-          hClose stream-          withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $-            testCLISucceeded ["dataize", "--evaluations=" ++ path, "--quiet", "--hide-rho"] []-          records <- readUtf8 path-          records `shouldEndWith` "\tΦ.number( as-bytes ↦ Φ.bytes( data ↦ ⟦ Δ ⤍ 40-26-00-00-00-00-00-00 ⟧ ) )\n"+        withAtoms $ \atoms ->+          withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do+            hClose stream+            withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $+              testCLISucceeded ["dataize", atoms, "--evaluations=" ++ path, "--quiet", "--hide-rho"] []+            records <- readUtf8 path+            records `shouldEndWith` "\tΦ.number( as-bytes ↦ Φ.bytes( data ↦ ⟦ Δ ⤍ 40-26-00-00-00-00-00-00 ⟧ ) )\n"        it "keeps the records of a run that fails" $-        withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do-          hClose stream-          withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]], nope -> [[ L> L_number_nope ]] ]], @ -> 5.plus(6).nope ]]" $-            testCLIFailed-              ["dataize", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"]-              ["Atom 'L_number_nope' does not exist"]-          records <- readUtf8 path-          records `shouldBe` "L_number_plus\t⟦ x ↦ 6 ⟧\t11\n"+        withAtoms $ \atoms ->+          withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do+            hClose stream+            withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]], nope -> [[ L> L_number_nope ]] ]], @ -> 5.plus(6).nope ]]" $+              testCLIFailed+                ["dataize", atoms, "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"]+                ["Atom 'L_number_nope' does not exist"]+            records <- readUtf8 path+            records `shouldBe` "L_number_plus\t⟦ x ↦ 6 ⟧\t11\n"        it "truncates the records left over from the previous run" $         withTempFileContent "evaluationsXXXXXX.txt" "L_number_gt\t[[ ]]\t01-\n" $ \path -> do@@ -1185,53 +1201,117 @@             ["dataize", "--evaluations=evaluations.txt", "--output=latex"]             ["The --evaluations option can stay together with --output=phi only"] -    -- A placeholder formation ⟦ λ ⤍ Sym_arg_0 ⟧ standing in for a data input-    -- names an atom phino cannot fire; the run used to die on it, discarding-    -- what it had already evaluated (#1060)+    -- A λ function the '--atoms' registry does not carry cannot fire — a+    -- placeholder such as ⟦ λ ⤍ Sym_arg_0 ⟧ standing in for a data input, or+    -- an operation the caller left out of its registry on purpose. The run used+    -- to die on it, discarding what it had already evaluated (#1060)     describe "--partial" $ do-      let stuck = "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]], times(x) -> [[ L> L_number_times ]] ]], @ -> 2.times(3).plus([[ L> Sym_arg_0 ]]) ]]"+      let stuck = "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, times(x) -> [[ L> L_number_times ]], nope -> [[ L> L_number_nope ]] ]], @ -> 2.times(3).nope ]]"       it "fails on an atom that cannot fire without the flag" $-        withStdin stuck $-          testCLIFailed ["dataize", "--sweet", "--hide-rho"] ["Atom 'Sym_arg_0' does not exist"]+        withAtoms $ \atoms ->+          withStdin stuck $+            testCLIFailed ["dataize", atoms, "--sweet", "--hide-rho"] ["Atom 'L_number_nope' does not exist"]        it "prints the residue with the stuck application intact and exits successfully" $-        withStdin stuck $-          testCLISucceeded-            ["dataize", "--partial", "--sweet", "--hide-rho"]-            ["⟦ x ↦ ⟦ λ ⤍ Sym_arg_0 ⟧, λ ⤍ L_number_plus ⟧"]+        withAtoms $ \atoms ->+          withStdin stuck $+            testCLISucceeded+              ["dataize", atoms, "--partial", "--sweet", "--hide-rho"]+              ["⟦ λ ⤍ L_number_nope ⟧"]        it "keeps what was evaluated before the stuck site in the residue" $-        withStdin stuck $-          testCLISucceeded-            ["dataize", "--partial", "--sweet"]-            ["as-bytes ↦ Φ.bytes( data ↦ ⟦ Δ ⤍ 40-18-00-00-00-00-00-00 ⟧ )"]+        withAtoms $ \atoms ->+          withStdin stuck $+            testCLISucceeded+              ["dataize", atoms, "--partial", "--sweet"]+              ["as-bytes ↦ Φ.bytes( data ↦ ⟦ Δ ⤍ 40-18-00-00-00-00-00-00 ⟧ )"]        it "records every stuck site in --evaluations with no result" $-        withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do-          hClose stream-          withStdin stuck $-            testCLISucceeded ["dataize", "--partial", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []-          records <- readUtf8 path-          lines records-            `shouldBe` [ "L_number_times\t⟦ x ↦ 3 ⟧\t6"-                       , "Sym_arg_0\t⟦⟧"-                       , "L_number_plus\t⟦ x ↦ ⟦ λ ⤍ Sym_arg_0 ⟧ ⟧"-                       ]+        withAtoms $ \atoms ->+          withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do+            hClose stream+            withStdin stuck $+              testCLISucceeded ["dataize", atoms, "--partial", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []+            records <- readUtf8 path+            lines records+              `shouldBe` [ "L_number_times\t⟦ x ↦ 3 ⟧\t6"+                         , "L_number_nope\t⟦⟧"+                         ]        it "still prints bytes when nothing gets stuck" $-        withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $-          testCLISucceeded ["dataize", "--partial"] ["40-26-00-00-00-00-00-00"]+        withAtoms $ \atoms ->+          withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $+            testCLISucceeded ["dataize", atoms, "--partial"] ["40-26-00-00-00-00-00-00"]        it "prints the chain of steps ending in the residue with --sequence" $-        withStdin stuck $-          testCLISucceeded-            ["dataize", "--partial", "--sequence", "--sweet", "--hide-rho", "--flat"]-            ["2.times( 3 ).plus( ⟦ λ ⤍ Sym_arg_0 ⟧ )", "⟦ x ↦ ⟦ λ ⤍ Sym_arg_0 ⟧, λ ⤍ L_number_plus ⟧"]+        withAtoms $ \atoms ->+          withStdin stuck $+            testCLISucceeded+              ["dataize", atoms, "--partial", "--sequence", "--sweet", "--hide-rho", "--flat"]+              ["2.times( 3 ).nope", "⟦ λ ⤍ L_number_nope ⟧"]        it "still stops on the terminator ⊥, since a wrong operand is not a stuck atom" $         withStdin "[[ ]]" $           testCLIFailed ["dataize", "--partial"] ["terminator ⊥"] +    -- Which λ functions exist is not phino's business any more: the registry+    -- given with '--atoms' decides, and phino carries none of its own+    describe "--atoms" $ do+      let sum' = "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"+      it "fires the λ function the registry carries" $+        withAtoms $ \atoms ->+          withStdin sum' $+            testCLISucceeded ["dataize", atoms] ["40-26-00-00-00-00-00-00"]++      it "gets stuck on every atom when it is not given" $+        withStdin sum' $+          testCLIFailed ["dataize"] ["Atom 'L_number_plus' does not exist"]++      it "fails when the registry file is not there" $+        withStdin sum' $+          testCLIFailed ["dataize", "--atoms=no-such-registry.json"] ["no-such-registry.json"]++      -- An unknown runtime is refused where the registry is read, which is+      -- before the input is even parsed, rather than when an atom of it fires+      it "fails on a runtime phino cannot run, before dataizing anything" $+        withTempFileContent "atomsXXXXXX.json" "{\"L_number_plus\": {\"rt\": \"ruby\", \"script\": \"puts 1\"}}" $ \path ->+          withStdin sum' $+            testCLIFailed ["dataize", "--atoms=" ++ path] ["unknown runtime 'ruby'"]++      it "fails on a registry that is not JSON" $+        withTempFileContent "atomsXXXXXX.json" "L_number_plus: js" $ \path ->+          withStdin sum' $+            testCLIFailed ["dataize", "--atoms=" ++ path] ["cannot be read"]++    -- An atom script cannot reduce the operands it was handed by itself, so it+    -- asks phino for them: '--inside' binds an expression to a synthetic+    -- attribute of the universe and aims the run at it+    describe "--inside" $ do+      let universe = "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> [[ D> 01- ]] ]]"+      it "dataizes an expression the input does not contain" $+        withAtoms $ \atoms ->+          withStdin universe $+            testCLISucceeded ["dataize", atoms, "--inside=5.plus( 6 )"] ["40-26-00-00-00-00-00-00"]++      -- The expression is normalized first, so a dispatch off a formation — the+      -- very shape a script asks about, '⟦ x ↦ 6, ρ ↦ 5 ⟧.x' — reduces too+      it "normalizes what it is handed before dataizing it" $+        withStdin universe $+          testCLISucceeded ["dataize", "--inside=[[ x -> [[ D> 2A- ]] ]].x"] ["2A-"]++      it "morphs inside the universe just as it dataizes inside it" $+        withAtoms $ \atoms ->+          withStdin universe $+            testCLISucceeded ["morph", atoms, "--inside=5.plus( 6 )", "--sweet", "--hide-rho", "--flat"] ["⟦ x ↦ 6, λ ⤍ L_number_plus ⟧"]++      it "cannot be used together with --locator" $+        withStdin universe $+          testCLIFailed ["dataize", "--inside=Q.@", "--locator=Q.@"] ["--inside and --locator cannot be used together"]++      it "fails when the input expression is not a formation" $+        withStdin "Q.x" $+          testCLIFailed ["dataize", "--inside=Q.x"] ["--inside requires the input expression to be a formation"]+     describe "fails" $ do       it "with --output != latex and --nonumber" $         withStdin "" $@@ -1307,15 +1387,17 @@         testCLISucceeded ["morph", "--flat", "--hide-rho"] ["⟦ Δ ⤍ 01- ⟧"]      it "stops at the bare saturated λ-formation" $-      withStdin chained $-        testCLISucceeded-          ["morph", "--locator=Q.@", "--sweet", "--hide-rho", "--flat"]-          ["⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"]+      withAtoms $ \atoms ->+        withStdin chained $+          testCLISucceeded+            ["morph", atoms, "--locator=Q.@", "--sweet", "--hide-rho", "--flat"]+            ["⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"]      -- The same term under 𝔻, which insists on bytes and fires what 𝕄 left bare     it "leaves to dataize the firing that takes the same term to bytes" $-      withStdin chained $-        testCLISucceeded ["dataize"] ["40-32-00-00-00-00-00-00"]+      withAtoms $ \atoms ->+        withStdin chained $+          testCLISucceeded ["dataize", atoms] ["40-32-00-00-00-00-00-00"]      -- 'mf' hands a formation back as it is, so '--locator' is how one aims 𝕄 at     -- a subterm worth navigating: here it resolves Φ against the universe and@@ -1340,37 +1422,40 @@     -- design — it happens in a side premise, which reduces on a chain of its     -- own and discards it     it "prints the chain of morphing steps with --sequence" $-      withStdin chained $-        testCLISucceeded-          ["morph", "--locator=Q.@", "--sequence", "--headers", "--sweet", "--hide-rho", "--flat"]-          [ "Rule 'maa'"-          , "Rule 'alpha'"-          , "Rule 'copy'"-          , "Rule 'mf'"-          , "⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"-          ]+      withAtoms $ \atoms ->+        withStdin chained $+          testCLISucceeded+            ["morph", atoms, "--locator=Q.@", "--sequence", "--headers", "--sweet", "--hide-rho", "--flat"]+            [ "Rule 'maa'"+            , "Rule 'alpha'"+            , "Rule 'copy'"+            , "Rule 'mf'"+            , "⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"+            ]      it "does not print the result with --quiet" $       withStdin "[[ D> 01- ]]" $         testCLISucceeded ["morph", "--quiet"] []      it "records the atoms it fires with --evaluations" $-      withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do-        hClose stream-        withStdin chained $-          testCLISucceeded ["morph", "--locator=Q.@", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []-        records <- readUtf8 path-        lines records `shouldBe` ["L_number_plus\t⟦ x ↦ 6 ⟧\t11"]+      withAtoms $ \atoms ->+        withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do+          hClose stream+          withStdin chained $+            testCLISucceeded ["morph", atoms, "--locator=Q.@", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []+          records <- readUtf8 path+          lines records `shouldBe` ["L_number_plus\t⟦ x ↦ 6 ⟧\t11"]      it "saves morphing steps to dir with --steps-dir" $-      withTempDirectory "phino-steps-morph" $ \dir ->-        withStdin chained $ do-          testCLISucceeded-            ["morph", "--locator=Q.@", "--steps-dir=" ++ dir, "--sweet", "--hide-rho", "--flat"]-            ["⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"]-          steps <- sort <$> listDirectory dir-          steps `shouldBe` map (\n -> printf "%05d.phi" (n :: Int)) [1 .. length steps]-          length steps `shouldSatisfy` (> 0)+      withAtoms $ \atoms ->+        withTempDirectory "phino-steps-morph" $ \dir ->+          withStdin chained $ do+            testCLISucceeded+              ["morph", atoms, "--locator=Q.@", "--steps-dir=" ++ dir, "--sweet", "--hide-rho", "--flat"]+              ["⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"]+            steps <- sort <$> listDirectory dir+            steps `shouldBe` map (\n -> printf "%05d.phi" (n :: Int)) [1 .. length steps]+            length steps `shouldSatisfy` (> 0)      it "accepts --seed, --shuffle and --depth-sensitive" $       withStdin "[[ D> 01- ]]" $@@ -1442,8 +1527,8 @@         ["explain", "--rule=resources/normalize/copy.yaml"]         [ unlines             [ "\\phinoNormalizationRule{copy}"-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"-            , "  { [[ B_1, \\tau -> k, B_2 ]] }"+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> k_1 ) }"+            , "  { [[ B_1, \\tau_1 -> k_1, B_2 ]] }"             , "  { }"             , "  { }"             ]@@ -1454,8 +1539,8 @@         ["explain", "--rule=test-resources/cli/labeled.yaml"]         [ unlines             [ "\\phinoNormalizationRule[\\lambda]{copy}"-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"-            , "  { [[ B_1, \\tau -> k, B_2 ]] }"+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> k_1 ) }"+            , "  { [[ B_1, \\tau_1 -> k_1, B_2 ]] }"             , "  { }"             , "  { }"             ]@@ -1488,18 +1573,18 @@         ["explain", "--normalize"]         [ unlines             [ "\\phinoNormalizationRule{alpha}"-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }"-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }"-            , "  { i = \\vert \\overline{ B_1 } \\vert }"+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\phiTerminal{\\alpha_{i1}} -> e_1 ) }"+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> e_1 ) }"+            , "  { i_1 = \\vert \\overline{ B_1 } \\vert }"             , "  { }"             , "\\phinoNormalizationRule{amiss}"-            , "  { [[ B ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }"+            , "  { [[ B_1 ]] ( \\phiTerminal{\\alpha_{i1}} -> e ) }"             , "  { T }"-            , "  { \\vert \\overline{ B } \\vert \\leq i }"+            , "  { \\vert \\overline{ B_1 } \\vert \\leq i_1 }"             , "  { }"             , "\\phinoNormalizationRule{copy}"-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"-            , "  { [[ B_1, \\tau -> k, B_2 ]] }"+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> k_1 ) }"+            , "  { [[ B_1, \\tau_1 -> k_1, B_2 ]] }"             , "  { }"             , "  { }"             , "\\phinoNormalizationRule{dc}"@@ -1523,29 +1608,29 @@             , "  { D \\in B_1 \\;\\text{or}\\; D \\in B_2 }"             , "  { }"             , "\\phinoNormalizationRule{dot}"-            , "  { [[ B_1, \\tau -> n, B_2 ]] . \\tau }"-            , "  { e ( \\phiTerminal{\\rho} -> [[ B_1, \\tau -> n, B_2 ]] ) }"+            , "  { [[ B_1, \\tau_1 -> n_1, B_2 ]] . \\tau_1 }"+            , "  { e_1 ( \\phiTerminal{\\rho} -> [[ B_1, \\tau_1 -> n_1, B_2 ]] ) }"             , "  { }"-            , "  { \\phinoContextualize{ n }{ [[ B_1, B_2 ]] }{ e } }"+            , "  { \\phinoContextualize{ n_1 }{ [[ B_1, B_2 ]] }{ e_1 } }"             , "\\phinoNormalizationRule{miss}"-            , "  { [[ B ]] ( \\tau -> e ) }"+            , "  { [[ B_1 ]] ( \\tau_1 -> e ) }"             , "  { T }"-            , "  { \\tau \\notin B }"+            , "  { \\tau_1 \\notin B_1 }"             , "  { }"             , "\\phinoNormalizationRule{null}"-            , "  { [[ B_1, \\tau -> ?, B_2 ]] . \\tau }"+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] . \\tau_1 }"             , "  { T }"             , "  { }"             , "  { }"             , "\\phinoNormalizationRule{over}"-            , "  { [[ B_1, \\tau -> e_1, B_2 ]] ( \\tau -> e_2 ) }"+            , "  { [[ B_1, \\tau_1 -> e_1, B_2 ]] ( \\tau_1 -> e_2 ) }"             , "  { T }"-            , "  { \\tau \\not= \\phiTerminal{\\rho} }"+            , "  { \\tau_1 \\not= \\phiTerminal{\\rho} }"             , "  { }"             , "\\phinoNormalizationRule{overa}"-            , "  { [[ B_1, \\tau -> e_1, B_2 ]] ( \\phiTerminal{\\alpha_{i}} -> e_2 ) }"+            , "  { [[ B_1, \\tau_1 -> e_1, B_2 ]] ( \\phiTerminal{\\alpha_{i1}} -> e_2 ) }"             , "  { T }"-            , "  { i = \\vert \\overline{ B_1 } \\vert \\;\\text{and}\\; \\tau \\not= \\phiTerminal{\\rho} }"+            , "  { i_1 = \\vert \\overline{ B_1 } \\vert \\;\\text{and}\\; \\tau_1 \\not= \\phiTerminal{\\rho} }"             , "  { }"             , "\\phinoNormalizationRule{stay}"             , "  { [[ B_1, \\phiTerminal{\\rho} -> e_1, B_2 ]] ( \\phiTerminal{\\rho} -> e_2 ) }"@@ -1553,9 +1638,9 @@             , "  { }"             , "  { }"             , "\\phinoNormalizationRule{stop}"-            , "  { [[ B ]] . \\tau }"+            , "  { [[ B_1 ]] . \\tau_1 }"             , "  { T }"-            , "  { \\tau \\notin B \\;\\text{and}\\; @ \\notin B \\;\\text{and}\\; L \\notin B }"+            , "  { \\tau_1 \\notin B_1 \\;\\text{and}\\; @ \\notin B_1 \\;\\text{and}\\; L \\notin B_1 }"             , "  { }"             ]         ]@@ -1566,79 +1651,79 @@         [ unlines             [ "\\begin{phinoMorphingInference}"             , "  \\phinoName{mf}"-            , "  \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ s }{ [[ B ]] }{ s } }"+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_0 ]] }{ e_0 }{ s }{ [[ B_0 ]] }{ s } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{ml}"             , "  \\phinoLabel{\\lambda}"-            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ n_1 }{ s_2 } }"-            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau }{ n_2 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ s_1 }{ n_3 }{ s_3 } }"+            , "  \\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 \\;\\text{and}\\; \\tau \\notin B \\;\\text{and}\\; L \\notin B }"-            , "  \\phinoPremise{ \\phinoNormalize{ [[ B ]] . @ . \\tau }{ n } }"-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ [[ B ]] . \\tau }{ e }{ s_1 }{ n_1 }{ s_2 } }"+            , "  \\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 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"-            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau }{ n_2 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ n . \\tau }{ e }{ s_1 }{ n_3 }{ s_3 } }"+            , "  \\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{ma}"-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"-            , "  \\phinoPremise{ \\phinoNormalize{ n_1 ( \\tau -> k_1 ) }{ n_2 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> k_1 ) }{ e }{ s_1 }{ n_3 }{ s_3 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_0 }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 ( \\tau_0 -> k_1 ) }{ n_2 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ n_0 ( \\tau_0 -> k_1 ) }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{maa}"-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"-            , "  \\phinoPremise{ \\phinoNormalize{ n_1 ( \\phiTerminal{\\alpha_{i}} -> k_1 ) }{ n_2 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> k_1 ) }{ e }{ s_1 }{ n_3 }{ s_3 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_0 }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 ( \\phiTerminal{\\alpha_{i0}} -> k_1 ) }{ n_2 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ n_0 ( \\phiTerminal{\\alpha_{i0}} -> k_1 ) }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{mad}"             , "  \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }"-            , "  \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n_2 }{ s_2 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> n_1 ) }{ e }{ s_1 }{ n_2 }{ s_2 } }"+            , "  \\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 } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{maad}"             , "  \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }"-            , "  \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n_2 }{ s_2 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> n_1 ) }{ e }{ s_1 }{ n_2 }{ s_2 } }"+            , "  \\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 } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{universe}"             , "  \\phinoLabel{\\Phi}"-            , "  \\phinoCondition{ e \\not= Q }"-            , "  \\phinoPremise{ \\phinoNormalize{ e }{ n } }"-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ e }{ s_1 }{ n_1 }{ s_2 } }"+            , "  \\phinoCondition{ e_0 \\not= Q }"+            , "  \\phinoPremise{ \\phinoNormalize{ e_0 }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_1 }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{dead}"-            , "  \\phinoConclusion{ \\phinoMorph{ T }{ e }{ s }{ T }{ s } }"+            , "  \\phinoConclusion{ \\phinoMorph{ T }{ e_0 }{ s }{ T }{ s } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{xi}"-            , "  \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n }{ s_2 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ s_1 }{ n }{ s_2 } }"+            , "  \\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 }{ s_2 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n }{ s_2 } }"+            , "  \\phinoPremise{ \\phinoMorph{ T }{ Q }{ s_1 }{ n_1 }{ s_2 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n_1 }{ s_2 } }"             , "\\end{phinoMorphingInference}"             ]         ]@@ -1650,34 +1735,34 @@             [ "\\begin{phinoDataizationInference}"             , "  \\phinoName{delta}"             , "  \\phinoLabel{\\Delta}"-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] }{ e }{ s }{ \\delta }{ s } }"+            , "  \\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 } }"             , "  \\phinoPremise{ \\phinoNormalize{ e_2 }{ n_1 } }"-            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_1 }{ \\delta }{ s_2 } }"-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_1, B_2 ]] }{ e }{ s_1 }{ \\delta }{ s_2 } }"+            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e_0 }{ s_1 }{ \\delta_0 }{ s_2 } }"+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_1, B_2 ]] }{ e_0 }{ s_1 }{ \\delta_0 }{ s_2 } }"             , "\\end{phinoDataizationInference}"             , "\\begin{phinoDataizationInference}"             , "  \\phinoName{fire}"-            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ n_1 }{ s_2 } }"-            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_2 }{ \\delta }{ s_3 } }"-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ \\delta }{ s_3 } }"+            , "  \\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 } }"+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F_0, B_2 ]] }{ e_0 }{ s_1 }{ \\delta_0 }{ s_3 } }"             , "\\end{phinoDataizationInference}"             , "\\begin{phinoDataizationInference}"             , "  \\phinoName{none}"-            , "  \\phinoCondition{ [ D \\char44{} L \\char44{} @ ] \\cap B = \\emptyset }"-            , "  \\phinoPremise{ \\phinoDataize{ T }{ e }{ s_1 }{ \\delta }{ s_2 } }"-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ s_1 }{ \\delta }{ s_2 } }"+            , "  \\phinoCondition{ [ D \\char44{} L \\char44{} @ ] \\cap B_0 = \\emptyset }"+            , "  \\phinoPremise{ \\phinoDataize{ T }{ e_0 }{ s_1 }{ \\delta_0 }{ s_2 } }"+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_0 ]] }{ e_0 }{ s_1 }{ \\delta_0 }{ s_2 } }"             , "\\end{phinoDataizationInference}"             , "\\begin{phinoDataizationInference}"             , "  \\phinoName{norm}"-            , "  \\phinoCondition{ \\phinoNotFormation{ n } \\;\\text{and}\\; n \\not= T }"-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"-            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_2 }{ \\delta }{ s_3 } }"-            , "  \\phinoConclusion{ \\phinoDataize{ n }{ e }{ s_1 }{ \\delta }{ s_3 } }"+            , "  \\phinoCondition{ \\phinoNotFormation{ n_0 } \\;\\text{and}\\; n_0 \\not= T }"+            , "  \\phinoPremise{ \\phinoMorph{ n_0 }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"+            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e_0 }{ s_2 }{ \\delta_0 }{ s_3 } }"+            , "  \\phinoConclusion{ \\phinoDataize{ n_0 }{ e_0 }{ s_1 }{ \\delta_0 }{ s_3 } }"             , "\\end{phinoDataizationInference}"             ]         ]@@ -1688,36 +1773,36 @@         [ unlines             [ "\\begin{phinoContextualizationInference}"             , "  \\phinoName{cg}"-            , "  \\phinoConclusion{ \\phinoContextualize{ Q }{ k }{ Q } }"+            , "  \\phinoConclusion{ \\phinoContextualize{ Q }{ k_0 }{ Q } }"             , "\\end{phinoContextualizationInference}"             , "\\begin{phinoContextualizationInference}"             , "  \\phinoName{cxi}"-            , "  \\phinoConclusion{ \\phinoContextualize{ \\phiTerminal{\\xi} }{ k }{ k } }"+            , "  \\phinoConclusion{ \\phinoContextualize{ \\phiTerminal{\\xi} }{ k_0 }{ k_0 } }"             , "\\end{phinoContextualizationInference}"             , "\\begin{phinoContextualizationInference}"             , "  \\phinoName{ct}"-            , "  \\phinoConclusion{ \\phinoContextualize{ T }{ k }{ T } }"+            , "  \\phinoConclusion{ \\phinoContextualize{ T }{ k_0 }{ T } }"             , "\\end{phinoContextualizationInference}"             , "\\begin{phinoContextualizationInference}"             , "  \\phinoName{cf}"-            , "  \\phinoConclusion{ \\phinoContextualize{ [[ B ]] }{ k }{ [[ B ]] } }"+            , "  \\phinoConclusion{ \\phinoContextualize{ [[ B_0 ]] }{ k_0 }{ [[ B_0 ]] } }"             , "\\end{phinoContextualizationInference}"             , "\\begin{phinoContextualizationInference}"             , "  \\phinoName{cd}"-            , "  \\phinoPremise{ \\phinoContextualize{ n }{ k }{ n_1 } }"-            , "  \\phinoConclusion{ \\phinoContextualize{ n . \\tau }{ k }{ n_1 . \\tau } }"+            , "  \\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{ca}"-            , "  \\phinoPremise{ \\phinoContextualize{ n }{ k }{ n_1 } }"-            , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ k }{ n_2 } }"-            , "  \\phinoConclusion{ \\phinoContextualize{ n ( \\tau -> e_1 ) }{ k }{ n_1 ( \\tau -> n_2 ) } }"+            , "  \\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{caa}"-            , "  \\phinoPremise{ \\phinoContextualize{ n }{ k }{ n_1 } }"-            , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ k }{ n_2 } }"-            , "  \\phinoConclusion{ \\phinoContextualize{ n ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ k }{ n_1 ( \\phiTerminal{\\alpha_{i}} -> n_2 ) } }"+            , "  \\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}"             ]         ]@@ -1838,13 +1923,19 @@     it "builds substitutions with conditions" $       withStdin "[[ x -> Q.y ]].x" $         testCLISucceeded-          ["match", "--pattern=[[ !t -> Q.y, !B ]].!t", "--when=eq(length(!B),1)"]-          ["B >> ⟦ ρ ↦ ∅ ⟧\nt >> x"]+          ["match", "--pattern=[[ !t1 -> Q.y, !B1 ]].!t1", "--when=eq(length(!B1),1)"]+          ["B1 >> ⟦ ρ ↦ ∅ ⟧\nt1 >> x"]      it "builds with condition from file" $       testCLISucceeded-        ["match", "--pattern=[[ !B ]]", "--when=eq(length(!B),2)", "test-resources/cli/foo.phi"]-        ["B >> ⟦ foo ↦ Φ.org.eolang.x, ρ ↦ ∅ ⟧"]+        ["match", "--pattern=[[ !B1 ]]", "--when=eq(length(!B1),2)", "test-resources/cli/foo.phi"]+        ["B1 >> ⟦ foo ↦ Φ.org.eolang.x, ρ ↦ ∅ ⟧"]++    it "rejects an anonymous meta in --when" $+      withStdin "[[ x -> Q.y ]]" $+        testCLIFailed+          ["match", "--pattern=[[ !B ]]", "--when=eq(length(!B),1)"]+          ["[ERROR]: Anonymous meta '!B' cannot be referenced in --when"]      it "fails on parsing --when condition" $       withStdin "[[]]" $

@@ -27,22 +27,22 @@       , "absolute(!e1)"       , "matches(\"hello(\\\"\\u0000)\", !e)"       , "part-of ( [[ x -> 1 ]] , !B ) "-      , "not(formation(!n))"+      , "not(formation(!n1))"       ]       (\expr -> it expr (parseCondition expr `shouldSatisfy` isRight))    describe "parses correctly" $     forM_-      [ ("in(!t, !B)", Y.In (AtMeta "t") (BiMeta "B"))-      , ("not(in(!t,!B))", Y.Not (Y.In (AtMeta "t") (BiMeta "B")))+      [ ("in(!t1, !B1)", Y.In (AtMeta "t1") (BiMeta "B1"))+      , ("not(in(!t1,!B1))", Y.Not (Y.In (AtMeta "t1") (BiMeta "B1")))       , ("eq(1,-2)", Y.Eq (Y.CmpNum (Y.Literal 1)) (Y.CmpNum (Y.Literal (-2))))-      , ("eq(!i,length(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i")) (Y.CmpNum (Y.Length (BiMeta "B1"))))+      , ("eq(!i1,length(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i1")) (Y.CmpNum (Y.Length (BiMeta "B1"))))       , ("eq(!i2,domain(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i2")) (Y.CmpNum (Y.Domain (BiMeta "B1"))))-      , ("gt(domain(!B1),!i)", Y.Gt (Y.CmpNum (Y.Domain (BiMeta "B1"))) (Y.CmpNum (Y.MetaIndex "i")))+      , ("gt(domain(!B1),!i1)", Y.Gt (Y.CmpNum (Y.Domain (BiMeta "B1"))) (Y.CmpNum (Y.MetaIndex "i1")))       , ("eq(!t1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "t1")) (Y.CmpExpr (ExMeta "e2")))       , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (ExMeta "e1"), Y.NF (ExDispatch ExRoot (AtLabel "x"))])-      , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")])-      , ("not(formation(!n))", Y.Not (Y.IsFormation (ExMeta "n")))+      , ("and(matches(\"hi\", !e1),part-of(!e1, !B1))", Y.And [Y.Matches "hi" (ExMeta "e1"), Y.PartOf (ExMeta "e1") (BiMeta "B1")])+      , ("not(formation(!n1))", Y.Not (Y.IsFormation (ExMeta "n1")))       ]       (\(expr, res) -> it expr (parseCondition expr `shouldBe` Right res)) 

@@ -7,14 +7,16 @@ module DataizeSpec (spec) where  import AST+import Atoms (Registry, emptyRegistry) import Control.Exception (SomeException) import Control.Monad import Data.IORef (modifyIORef', newIORef, readIORef) import Data.List (find, isInfixOf, nub) import Data.List.NonEmpty (NonEmpty (..)) import Data.Maybe (fromMaybe, isJust)-import Dataize (DataizeContext (..), Outcome (..), Steps (..), dataize, dataize', emptyState, execBuildTerm, morph, morph')+import Dataize (DataizeContext (..), Outcome (..), Steps (..), dataize, dataize', emptyState, execBuildTerm, insideUniverse, morph, morph') import Deps (Evaluation (..), Term (TeExpression), dontSaveEval, dontSaveStep)+import Fixtures (fixtureRegistry, withNode) import Functions (buildTerm) import Matcher (substEmpty) import Parser (parseExpressionThrows)@@ -26,10 +28,16 @@  -- 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.+-- 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 buildTerm dontSaveStep dontSaveEval+defaultDataizeContext loc = DataizeContext loc 25 25 (Steps 250 0) False True 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 func useCases =   forM_ useCases $ \(desc, input, expr, output) ->@@ -63,18 +71,18 @@       (morphed, _) <- morph expr (defaultDataizeContext loc')       morphed `shouldBe` expected --- The 12 primitive λ-atoms every EO data operation reduces to, declared the way--- 'number.eo' and 'bytes.eo' declare them, so a case below only has to spell the--- The 12 primitive λ-atoms every EO data operation reduces to, 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 the 'cant-slice' complaint, 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+-- 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@@ -82,14 +90,8 @@     , "  bytes -> [["     , "    data -> ?,"     , "    @ -> $.data,"-    , "    and -> [[ b -> ?, L> L_bytes_and ]],"-    , "    or -> [[ b -> ?, L> L_bytes_or ]],"     , "    not -> [[ L> L_bytes_not ]],"-    , "    concat -> [[ b -> ?, L> L_bytes_concat ]],"-    , "    eq -> [[ b -> ?, L> L_bytes_eq ]],"-    , "    size -> [[ L> L_bytes_size ]],"-    , "    right -> [[ x -> ?, L> L_bytes_right ]],"-    , "    slice -> [[ start -> ?, len -> ?, cant-slice -> ?, L> L_bytes_slice ]]"+    , "    eq -> [[ b -> ?, L> L_bytes_eq ]]"     , "  ]],"     , "  number -> [["     , "    as-bytes -> ?,"@@ -98,7 +100,8 @@     , "    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 ) ]]"+    , "    eq -> [[ x -> ?, @ -> $.^.as-bytes.eq( x.as-bytes ) ]],"+    , "    nope -> [[ L> L_number_nope ]]"     , "  ]],"     , "  string -> [[ as-bytes -> ?, @ -> $.as-bytes ]],"     , "  true -> [[ @ -> [[ D> FF- ]] ]],"@@ -111,38 +114,51 @@ raw :: String -> String raw bts = "Q.bytes( data -> [[ D> " ++ bts ++ " ]] )" -testAtom :: [(String, String, Bytes)] -> Spec-testAtom useCases =+-- 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 $ do-      expr <- parseExpressionThrows (primitives src)-      loc <- parseExpressionThrows "Q"-      (value, _) <- dataize expr (defaultDataizeContext loc)-      value `shouldBe` Dataized 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 :: String -> IO ((Outcome, [Rewritten]), [Evaluation])-partially src = do+partially :: Registry -> String -> IO ((Outcome, [Rewritten]), [Evaluation])+partially registry src = do   expr <- parseExpressionThrows (primitives src)   reports <- newIORef []-  let ctx = (defaultDataizeContext ExRoot){_partial = True, _saveEval = \report -> modifyIORef' reports (report :)}+  let ctx =+        (withAtoms registry (defaultDataizeContext ExRoot))+          { _partial = True+          , _saveEval = \report -> modifyIORef' reports (report :)+          }   result <- dataize expr ctx   collected <- readIORef reports   pure (result, reverse collected)  -- An atom with no answer yields ⊥, which stops the whole dataization-testStuckAtom :: [(String, String)] -> Spec-testStuckAtom useCases =+testStuckAtom :: Registry -> [(String, String)] -> Spec+testStuckAtom registry useCases =   forM_ useCases $ \(name, src) ->-    it name $ do-      expr <- parseExpressionThrows (primitives src)-      loc <- parseExpressionThrows "Q"-      dataize expr (defaultDataizeContext loc)-        `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))+    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).@@ -253,7 +269,7 @@   -- 'execBuildTerm', the same way the matcher would call it.   describe "execBuildTerm 'evaluate'" $ do     let univ = ExFormation []-        ctx = defaultDataizeContext ExRoot+        ctx = withAtoms registry (defaultDataizeContext ExRoot)         runEvaluate args = execBuildTerm univ ctx "evaluate" args substEmpty     forM_       [@@ -281,12 +297,13 @@           it ("throws when " ++ desc) $             runEvaluate args `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException))       )-    it "evaluates a λ-bearing formation to the atom's normalized result" $ 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"+    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 []@@ -300,18 +317,32 @@         TeExpression expr -> expr `shouldBe` ExFormation [BiDelta (BtOne "00")]         _ -> expectationFailure "expected TeExpression" -  -- Every atom's operand is fetched through the synthetic '_dataize', which-  -- rebuilds the universe as a formation to bind the operand into before-  -- reducing it. A universe that is not itself a formation can never arise-  -- from the public 'dataize' entry point (its own universe argument doubles-  -- as the located root of a real program, always a formation), but 'dataize''-  -- lets a test drive an atom-bearing term against one directly, proving the-  -- guard fires instead of the atom looping or crashing some other way.-  describe "atoms refuse to run under a non-formation universe" $-    it "fails fast instead of dispatching against a non-formation universe" $ do-      let form = ExFormation [BiLambda (Function "L_bytes_not"), BiVoid AtRho]-      dataize' (form, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)-        `shouldThrow` (\e -> "non-formation universe" `isInfixOf` show (e :: SomeException))+  -- 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@@ -453,76 +484,79 @@   -- stop it (#1052). '--max-steps' bounds that recursion and fails once the   -- budget is gone.   describe "stops a dataization that never reaches bytes" $-    it "fails on the step limit instead of morphing forever" $ 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 buildTerm dontSaveStep dontSaveEval)-        `shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException))+    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 registry buildTerm dontSaveStep dontSaveEval)+          `shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException)) -  -- An atom phino does not know — a placeholder such as ⟦ λ ⤍ Sym_arg_0 ⟧-  -- standing in for a data input (#1060) — fails the run, and so does a known-  -- atom whose input reaches one. Under '_partial' the run ends on the residue+  -- An atom phino does not know — a name the '--atoms' registry does not carry,+  -- such as the placeholder ⟦ λ ⤍ Sym_arg_0 ⟧ standing in for a data input+  -- (#1060) — fails the run. Under '_partial' the run ends on the residue   -- instead: the working expression the spine had reached, with the stuck   -- application intact and everything the calculus demanded before it already-  -- evaluated, while 𝔼 reports each parked site with no result.+  -- evaluated, while 𝔼 reports each parked site with no result. Since the atoms+  -- moved out of the binary, an operand that cannot be reduced is the script's+  -- own business, so what parks here is the unregistered λ function alone.   describe "partially evaluates around an atom that cannot fire (--partial)" $ do     -- the parser gives every formation its void ρ     let placeholder = ExFormation [BiLambda (Function "Sym_arg_0"), BiVoid AtRho]-    it "fails on it without the flag, naming the unknown atom" $ do-      expr <- parseExpressionThrows (primitives "2.times(3).plus([[ L> Sym_arg_0 ]])")-      dataize expr (defaultDataizeContext ExRoot)-        `shouldThrow` (\e -> "Atom 'Sym_arg_0' does not exist" `isInfixOf` show (e :: SomeException))-    it "leaves the saturated application of the known atom in place, the placeholder inside it" $ do-      ((outcome, _), _) <- partially "2.times(3).plus([[ L> Sym_arg_0 ]])"-      case outcome of-        Residual (ExFormation bds) -> do-          bds `shouldContain` [BiLambda (Function "L_number_plus")]-          bds `shouldContain` [BiTau (AtLabel "x") placeholder]-        other -> expectationFailure ("expected a residual formation, got " ++ show other)-    it "keeps what was evaluated before the stuck site in the residue" $ do-      ((outcome, _), _) <- partially "2.times(3).plus([[ L> Sym_arg_0 ]])"-      case outcome of-        Residual (ExFormation bds) -> do-          let rho = [value | BiTau AtRho value <- bds]-          length rho `shouldBe` 1-          -- 2 × 3 = 6.0, whose IEEE 754 bytes are 40-18-00-00-00-00-00-00-          show rho `shouldContain` show (BtMany ["40", "18", "00", "00", "00", "00", "00", "00"])-          -- the times application is gone: ρ is the number it produced, its 'as-bytes' bound-          [() | ExFormation inner <- rho, BiTau (AtLabel "as-bytes") _ <- inner] `shouldBe` [()]-        other -> expectationFailure ("expected a residual formation, got " ++ show other)-    it "reports the firing that succeeded with its result and every stuck site without one" $ do-      (_, reports) <- partially "2.times(3).plus([[ L> Sym_arg_0 ]])"-      map (._function) reports `shouldBe` ["L_number_times", "Sym_arg_0", "L_number_plus"]-      map (isJust . (._result)) reports `shouldBe` [True, False, False]-    it "leaves an unknown atom dataized directly as the whole residue" $ do-      ((outcome, chain), reports) <- partially "[[ L> Sym_arg_0 ]]"-      outcome `shouldBe` Residual placeholder-      map (._function) reports `shouldBe` ["Sym_arg_0"]-      map fst chain `shouldEndWith` [placeholder]-    it "still reaches bytes when nothing is stuck" $ do-      ((outcome, _), reports) <- partially "2.times(3)"-      outcome `shouldBe` Dataized (BtMany ["40", "18", "00", "00", "00", "00", "00", "00"])-      map (._function) reports `shouldBe` ["L_number_times"]-    it "stops on the terminator ⊥ as before, since a wrong operand is not a stuck atom" $ do-      expr <- parseExpressionThrows (primitives (raw "20-1F" ++ ".and( " ++ raw "CA-FE-BE" ++ " )"))-      dataize expr ((defaultDataizeContext ExRoot){_partial = True})-        `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))+    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))+          `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+        ((outcome, _), _) <- partially registry "2.times(3).nope"+        case outcome of+          Residual (ExFormation bds) -> bds `shouldContain` [BiLambda (Function "L_number_nope")]+          other -> expectationFailure ("expected a residual formation, got " ++ show other)+    it "keeps what was evaluated before the stuck site in the residue" $+      withNode $ do+        ((outcome, _), _) <- partially registry "2.times(3).nope"+        case outcome of+          Residual (ExFormation bds) -> do+            let rho = [value | BiTau AtRho value <- bds]+            length rho `shouldBe` 1+            -- 2 × 3 = 6.0, whose IEEE 754 bytes are 40-18-00-00-00-00-00-00+            show rho `shouldContain` show (BtMany ["40", "18", "00", "00", "00", "00", "00", "00"])+            -- the times application is gone: ρ is the number it produced, its 'as-bytes' bound+            [() | ExFormation inner <- rho, BiTau (AtLabel "as-bytes") _ <- inner] `shouldBe` [()]+          other -> expectationFailure ("expected a residual formation, got " ++ show other)+    it "reports the firing that succeeded with its result and the stuck site without one" $+      withNode $ do+        (_, reports) <- partially registry "2.times(3).nope"+        map (._function) reports `shouldBe` ["L_number_times", "L_number_nope"]+        map (isJust . (._result)) reports `shouldBe` [True, False]+    it "leaves an unknown atom dataized directly as the whole residue" $+      withNode $ do+        ((outcome, chain), reports) <- partially registry "[[ L> Sym_arg_0 ]]"+        outcome `shouldBe` Residual placeholder+        map (._function) reports `shouldBe` ["Sym_arg_0"]+        map fst chain `shouldEndWith` [placeholder]+    it "still reaches bytes when nothing is stuck" $+      withNode $ do+        ((outcome, _), reports) <- partially registry "2.times(3)"+        outcome `shouldBe` Dataized (BtMany ["40", "18", "00", "00", "00", "00", "00", "00"])+        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})+          `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException)) -  -- '_maxDepth'/'_maxCycles' bound the normalization rewriter that a 'box' or-  -- 'norm' dataization step splices in (see 'normalized'); with-  -- '_depthSensitive' on, exhausting either one propagates the very same-  -- exception the rewriter itself throws, and with it off the limit is-  -- absorbed silently, so dataization still reaches an answer.   describe "DataizeContext'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 buildTerm dontSaveStep dontSaveEval+        , DataizeContext ExRoot 25 0 (Steps 250 0) True True False emptyRegistry buildTerm dontSaveStep dontSaveEval         , "--max-cycles=0"         )       ,         ( "--max-depth"-        , DataizeContext ExRoot 0 25 (Steps 250 0) True True False buildTerm dontSaveStep dontSaveEval+        , DataizeContext ExRoot 0 25 (Steps 250 0) True True False emptyRegistry buildTerm dontSaveStep dontSaveEval         , "--max-depth=0"         )       ]@@ -532,8 +566,8 @@             dataize expr ctx `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException))       )     forM_-      [ ("--max-cycles", DataizeContext ExRoot 25 0 (Steps 250 0) False True False buildTerm dontSaveStep dontSaveEval)-      , ("--max-depth", DataizeContext ExRoot 0 25 (Steps 250 0) False True False buildTerm dontSaveStep dontSaveEval)+      [ ("--max-cycles", DataizeContext ExRoot 25 0 (Steps 250 0) False True False emptyRegistry buildTerm dontSaveStep dontSaveEval)+      , ("--max-depth", DataizeContext ExRoot 0 25 (Steps 250 0) False True False emptyRegistry buildTerm dontSaveStep dontSaveEval)       ]       ( \(flag, ctx) ->           it ("does not throw without --depth-sensitive even once " ++ flag ++ " is exhausted") $ do@@ -555,23 +589,15 @@             ++ map (.name) Yaml.normalizationRules             ++ concatMap (map (verb . (.operation)) . (.premises)) Yaml.morphingRules             ++ concatMap (map (verb . (.operation)) . (.premises)) Yaml.dataizationRules-    it "uses no step label without a defining rule or operation" $ do-      expr <--        parseExpressionThrows-          ( unlines-              [ "[["-              , "  bytes(data) -> [[ @ -> $.data ]],"-              , "  number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]],"-              , "  @ -> 5.plus(6)"-              , "]]"-              ]-          )-      loc <- parseExpressionThrows "Q"-      (_, chain) <- dataize expr (defaultDataizeContext loc)-      let orphans = nub [label | (_, Just label) <- chain, label `notElem` allowed]-      unless-        (null orphans)-        (expectationFailure ("Dataization emitted step labels with no defining rule or operation: " ++ show orphans))+    it "uses no step label without a defining rule or operation" $+      withNode $ do+        expr <- parseExpressionThrows (primitives "5.plus(6)")+        loc <- parseExpressionThrows "Q"+        (_, chain) <- dataize expr (withAtoms registry (defaultDataizeContext loc))+        let orphans = nub [label | (_, Just label) <- chain, label `notElem` allowed]+        unless+          (null orphans)+          (expectationFailure ("Dataization emitted step labels with no defining rule or operation: " ++ show orphans))    describe "names every rule uniquely across rule sets" $     it "shares no rule name between morphing, dataization, normalization and contextualization" $ do@@ -587,33 +613,34 @@     let labelsOf loc src = do           expr <- parseExpressionThrows src           loc' <- parseExpressionThrows loc-          (_, chain) <- dataize expr (defaultDataizeContext loc')+          (_, chain) <- dataize expr (withAtoms registry (defaultDataizeContext loc'))           pure [label | (_, Just label) <- chain]-    it "dataizes 5.plus(6) through the expected rules" $ do-      labels <--        labelsOf-          "Q"-          "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"-      labels-        `shouldBe` [ "contextualize"-                   , "maa"-                   , "alpha"-                   , "copy"-                   , "mf"-                   , "evaluate"-                   , "ma"-                   , "copy"-                   , "mf"-                   , "contextualize"-                   , "dot"-                   , "ma"-                   , "stay"-                   , "mf"-                   , "contextualize"-                   , "dot"-                   , "copy"-                   , "delta"-                   ]+    it "dataizes 5.plus(6) through the expected rules" $+      withNode $ do+        labels <-+          labelsOf+            "Q"+            "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"+        labels+          `shouldBe` [ "contextualize"+                     , "maa"+                     , "alpha"+                     , "copy"+                     , "mf"+                     , "evaluate"+                     , "ma"+                     , "copy"+                     , "mf"+                     , "contextualize"+                     , "dot"+                     , "ma"+                     , "stay"+                     , "mf"+                     , "contextualize"+                     , "dot"+                     , "copy"+                     , "delta"+                     ]     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"]@@ -626,77 +653,10 @@       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     [-      ( "5.plus(6)"-      , "Q"-      , unlines-          [ "[["-          , "  bytes(data) -> [["-          , "    @ -> $.data"-          , "  ]],"-          , "  number(as-bytes) -> [["-          , "    @ -> $.as-bytes,"-          , "    plus(x) -> [[ L> L_number_plus ]]"-          , "  ]],"-          , "  @ -> 5.plus(6)"-          , "]]"-          ]-      , BtMany ["40", "26", "00", "00", "00", "00", "00", "00"]-      )-    ,-      ( "Fahrenheit"-      , "Q"-      , unlines-          [ "[["-          , "  bytes -> [["-          , "    data -> ?,"-          , "    @ -> $.data"-          , "  ]],"-          , "  number -> [["-          , "    as-bytes -> ?,"-          , "    @ -> $.as-bytes,"-          , "    plus -> [[ x -> ?, L> L_number_plus ]],"-          , "    times -> [[ x -> ?, L> L_number_times ]]"-          , "  ]],"-          , "  @ -> $.c.times(1.8).plus(32),"-          , "  c -> 25"-          , "]]"-          ]-      , BtMany ["40", "53", "40", "00", "00", "00", "00", "00"]-      )-    ,-      ( "Factorial"-      , "Q"-      , unlines-          [ "[["-          , "  bytes -> [["-          , "    data -> ?,"-          , "    eq -> [[ b -> ?, L> L_bytes_eq ]],"-          , "    @ -> $.data"-          , "  ]],"-          , "  number -> [["-          , "    as-bytes -> ?,"-          , "    @ -> $.as-bytes,"-          , "    times -> [[ x -> ?, L> L_number_times ]],"-          , "    plus -> [[ x -> ?, L> L_number_plus ]],"-          , "    eq -> [[ x -> ?, @ -> $.^.as-bytes.eq( x.as-bytes ) ]]"-          , "  ]],"-          , "  true -> [[ if -> [[ t -> ?, f -> ?, @ -> t ]] ]],"-          , "  false -> [[ if -> [[ t -> ?, f -> ?, @ -> f ]] ]],"-          , "  fac -> [["-          , "    x -> ?,"-          , "    @ -> $.x.eq( 1 ).if("-          , "      1,"-          , "      $.x.times($.^.fac($.x.plus(-1)))"-          , "    )"-          , "  ]],"-          , "  @ -> $.fac(3)"-          , "]]"-          ]-      , BtMany ["40", "18", "00", "00", "00", "00", "00", "00"]-      )-    ,       ( "Located"       , "Q.foo.bar"       , unlines@@ -737,88 +697,81 @@       )     ] -  describe "atoms" $ do+  -- 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-      [ ("divides a positive dividend", "256.div( 16 )", BtMany ["40", "30", "00", "00", "00", "00", "00", "00"])+      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")-      , ("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"])-      ,-        ( "conjoins two long bytes"-        , raw "02-EF-D4-05-5E-78-3A" ++ ".and( " ++ raw "12-33-C1-B5-5E-71-55" ++ " )"-        , BtMany ["02", "23", "C0", "05", "5E", "70", "10"]-        )-      ,-        ( "disjoins negative bytes with one"-        , raw "FF-FF-FF-FF-00-00-00-00" ++ ".or( " ++ raw "00-00-00-00-00-00-00-01" ++ " )"-        , BtMany ["FF", "FF", "FF", "FF", "00", "00", "00", "01"]-        )       , ("inverts bytes", raw "CA-FE-BE-BE" ++ ".not", BtMany ["35", "01", "41", "41"])-      ,-        ( "concats two long bytes"-        , raw "02-EF-D4-05-5E-78-3A" ++ ".concat( " ++ raw "12-33-C1-B5-5E-71-55" ++ " )"-        , BtMany ["02", "EF", "D4", "05", "5E", "78", "3A", "12", "33", "C1", "B5", "5E", "71", "55"]-        )-      ,-        ( "concats bytes with empty ones"-        , raw "05-5E-78" ++ ".concat( " ++ raw "--" ++ " )"-        , BtMany ["05", "5E", "78"]-        )-      , ("counts the size of bytes", raw "F1-20-5F-EC-B5-90-32" ++ ".size", BtMany ["40", "1C", "00", "00", "00", "00", "00", "00"])       , ("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")-      , ("takes a part of bytes", raw "20-1F-EE-B5-90" ++ ".slice( 1, 3 )", BtMany ["1F", "EE", "B5"])-      ,-        ( "shifts right an even negative"-        , raw "C0-43-00-00-00-00-00-00" ++ ".right( 1 )"-        , BtMany ["60", "21", "80", "00", "00", "00", "00", "00"]-        )-      ,-        ( "shifts right minus one"-        , raw "BF-F0-00-00-00-00-00-00" ++ ".right( 4 )"-        , BtMany ["0B", "FF", "00", "00", "00", "00", "00", "00"]-        )-      ,-        ( "shifts right by the integer minimum"-        , raw "BF-F0-00-00-00-00-00-00" ++ ".right( -2147483648 )"-        , BtMany ["00", "00", "00", "00", "00", "00", "00", "00"]-        )-      ,-        ( "recovers from an out-of-bounds slice"-        , raw "20-1F-EE-B5-90" ++ ".slice( 3, 10, [[ message -> ?, @ -> \"recovered\" ]] )"-        , BtMany ["72", "65", "63", "6F", "76", "65", "72", "65", "64"]-        )-      ,-        ( "recovers from a slice whose start plus length overflows"-        , raw "20-1F-EE-B5-90" ++ ".slice( 2000000000, 2000000000, [[ message -> ?, @ -> \"recovered\" ]] )"-        , BtMany ["72", "65", "63", "6F", "76", "65", "72", "65", "64"]-        )       ]++    -- 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 -> [["+                , "    data -> ?,"+                , "    @ -> $.data"+                , "  ]],"+                , "  number -> [["+                , "    as-bytes -> ?,"+                , "    @ -> $.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-      [ ("cannot conjoin bytes of different lengths", raw "20-1F" ++ ".and( " ++ raw "CA-FE-BE" ++ " )")-      , ("cannot disjoin bytes of different lengths", raw "20-1F" ++ ".or( " ++ raw "CA-FE-BE" ++ " )")-      , ("cannot slice from an offset beyond the int range", raw "20-1F-EE-B5-90" ++ ".slice( 3000000000, 1 )")-      , ("cannot slice a negative length", raw "20-1F-EE-B5-90" ++ ".slice( 1, -1 )")-      , -- A number atom rejects an operand that carries no number (empty bytes),-        -- yielding ⊥ rather than a result; dataizing ⊥ then fails through the-        -- terminator path, exactly like the bytes-atom cases above.-        ("cannot add a non-numeric operand", "5.plus( " ++ raw "--" ++ " )")+      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 number atom also rejects a non-empty operand whose byte array is not-        -- 8 bytes long (e.g. 2 or 5 bytes): such an array carries no number, and-        -- the atom must yield ⊥ instead of crashing on 'btsToNum' (issue #1072).+      , -- 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" ++ " )")-      , ("cannot divide by a 3-byte divisor", "5.div( " ++ raw "CA-FE-BE" ++ " )")-      , ("cannot compare against a 4-byte threshold", "5.gt( " ++ raw "FF-FF-FF-FF" ++ " )")-      , -- 'right' rejects a shift distance that is not a plain 8-byte integer;-        -- empty bytes carry no such integer, so the shift atom is stuck too.-        ("cannot shift right by a non-integer distance", raw "C0-43-00-00-00-00-00-00" ++ ".right( " ++ raw "--" ++ " )")       ]

@@ -0,0 +1,72 @@+{-# LANGUAGE OverloadedStrings #-}++-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++-- The λ functions the specs fire. phino implements none of them, so a spec that+-- needs an atom to answer brings its own: one JavaScript fixture,+-- 'test-resources/atoms/primitives.js', registered under every name in+-- 'fixtureAtoms' and branching on the one it is handed as its first+-- command-line argument.+module Fixtures (fixtureAtoms, fixtureRegistry, withFixtureRegistry, withNode) where++import Atoms (Atom (..), Registry, Runtime (RtNode))+import Control.Exception (bracket)+import Data.Aeson (encode, object, (.=))+import Data.Aeson.Key qualified as Key+import Data.ByteString qualified as BS+import Data.ByteString.Lazy qualified as BSL+import Data.Map.Strict qualified as Map+import Data.Maybe (isNothing)+import Data.Text qualified as T+import Data.Text.Encoding (decodeUtf8)+import System.Directory (findExecutable, getTemporaryDirectory, removePathForcibly)+import System.IO (Handle, hClose, openBinaryTempFile)+import Test.Hspec (Expectation, pendingWith)++-- 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.+fixtureAtoms :: [T.Text]+fixtureAtoms =+  [ "L_number_plus"+  , "L_number_times"+  , "L_number_div"+  , "L_number_gt"+  , "L_bytes_eq"+  , "L_bytes_not"+  ]++-- The fixture script itself, read as UTF-8 rather than through the locale,+-- since it spells 𝜑 expressions.+fixtureScript :: IO T.Text+fixtureScript = decodeUtf8 <$> BS.readFile "test-resources/atoms/primitives.js"++-- The registry the specs that drive 'Dataize' directly run against.+fixtureRegistry :: IO Registry+fixtureRegistry = do+  script <- fixtureScript+  pure (Map.fromList [(name, Atom RtNode script) | name <- fixtureAtoms])++-- The same registry as the JSON file '--atoms' reads, in a temporary file+-- removed afterwards, for the specs that go through the command line.+withFixtureRegistry :: (FilePath -> IO a) -> IO a+withFixtureRegistry action = do+  script <- fixtureScript+  dir <- getTemporaryDirectory+  bracket (openBinaryTempFile dir "phino-atoms-.json") discarded $ \(path, handle) -> do+    BSL.hPut handle (encode (object [Key.fromText name .= entry script | name <- fixtureAtoms]))+    hClose handle+    action path+  where+    entry script = object ["rt" .= ("node" :: T.Text), "script" .= script]+    discarded :: (FilePath, Handle) -> IO ()+    discarded (path, handle) = hClose handle >> removePathForcibly path++-- Every atom the fixture provides runs under 'node', so a machine without it+-- cannot fire one at all: such an expectation is pending rather than red.+withNode :: Expectation -> Expectation+withNode expectation = do+  node <- findExecutable "node"+  if isNothing node+    then pendingWith "'node' is not installed, so no λ function can be fired"+    else expectation

@@ -14,7 +14,7 @@ import Deps (Term (TeAttribute, TeBindings, TeBytes, TeExpression)) import Functions (buildTerm) import Logger (logDebug)-import Matcher (MetaValue (MvBindings), Subst (Subst), substEmpty)+import Matcher (Meta (Named), MetaValue (MvBindings), Subst (Subst), substEmpty) import Misc (uniqueBindings') import Printer (printExpression) import Test.Hspec (Expectation, Spec, describe, it, shouldBe, shouldThrow)@@ -44,9 +44,9 @@ spec = describe "Functions" $ do   describe "join" $ do     it "contains only unique bindings after 'join'" $ do-      let first = ("B1", MvBindings [BiVoid AtRho, BiDelta BtEmpty, BiTau (AtLabel "x") ExRoot, BiVoid (AtLabel "a0")])-          second = ("B2", MvBindings [BiTau AtRho ExXi, BiLambda (Function "Func"), BiDelta (BtOne "00"), BiVoid (AtLabel "a1")])-          third = ("B3", MvBindings [BiLambda (Function "Some"), BiTau (AtLabel "y") ExXi, BiTau (AtLabel "x") ExXi, BiVoid (AtLabel "a0")])+      let first = (Named "B1", MvBindings [BiVoid AtRho, BiDelta BtEmpty, BiTau (AtLabel "x") ExRoot, BiVoid (AtLabel "a0")])+          second = (Named "B2", MvBindings [BiTau AtRho ExXi, BiLambda (Function "Func"), BiDelta (BtOne "00"), BiVoid (AtLabel "a1")])+          third = (Named "B3", MvBindings [BiLambda (Function "Some"), BiTau (AtLabel "y") ExXi, BiTau (AtLabel "x") ExXi, BiVoid (AtLabel "a0")])           subst = Subst (Map.fromList [first, second, third])       TeBindings bds <- buildTerm "join" [ArgBinding (BiMeta "B1"), ArgBinding (BiMeta "B2"), ArgBinding (BiMeta "B3")] subst       bds' <- uniqueBindings' bds@@ -54,8 +54,8 @@       length bds' `shouldBe` 9      it "renames a duplicate tau binding (not rho/delta/lambda) instead of dropping it" $ do-      let first = ("B1", MvBindings [BiTau (AtLabel "x") ExRoot])-          second = ("B2", MvBindings [BiTau (AtLabel "x") ExXi])+      let first = (Named "B1", MvBindings [BiTau (AtLabel "x") ExRoot])+          second = (Named "B2", MvBindings [BiTau (AtLabel "x") ExXi])           subst = Subst (Map.fromList [first, second])       TeBindings bds <- buildTerm "join" [ArgBinding (BiMeta "B1"), ArgBinding (BiMeta "B2")] subst       length bds `shouldBe` 2@@ -86,7 +86,7 @@    describe "size" $     it "counts the bindings bound to a meta" $ do-      let subst = Subst (Map.singleton "B" (MvBindings [BiVoid AtRho, BiVoid (AtLabel "x")]))+      let subst = Subst (Map.singleton (Named "B") (MvBindings [BiVoid AtRho, BiVoid (AtLabel "x")]))       term <- buildTerm "size" [ArgBinding (BiMeta "B")] subst       expectExpression term (DataNumber (numToBts 2)) 

@@ -13,7 +13,7 @@ import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, describe, it, shouldBe)  substs :: [[(T.Text, MetaValue)]] -> [Subst]-substs = map (Subst . Map.fromList)+substs = map (Subst . Map.mapKeys Named . Map.fromList)  test ::   (a -> a -> [Subst]) ->@@ -466,6 +466,44 @@         )       ] +  describe "matches an anonymous meta independently at every occurrence" $+    -- Two anonymous metas of one kind sit at different offsets, so they are+    -- different keys and bind different terms. That is what lets a pattern say+    -- "any two attributes" without inventing a name for either of them (#218).+    forM_+      [+        ( "[[ !t -> !e, !t -> !e ]] => [[ a -> Q, b -> $ ]] => both bindings bind their own slots"+        , ExFormation+            [ BiTau (AtAny (Slot "t" 1)) (ExAny (Slot "e" 2))+            , BiTau (AtAny (Slot "t" 3)) (ExAny (Slot "e" 4))+            ]+        , ExFormation+            [ BiTau (AtLabel "a") ExRoot+            , BiTau (AtLabel "b") ExXi+            ]+        ,+          [ Subst+              ( Map.fromList+                  [ (Anon (Slot "t" 1), MvAttribute (AtLabel "a"))+                  , (Anon (Slot "e" 2), MvExpression ExRoot)+                  , (Anon (Slot "t" 3), MvAttribute (AtLabel "b"))+                  , (Anon (Slot "e" 4), MvExpression ExXi)+                  ]+              )+          ]+        )+      ,+        ( "[[ !t -> Q, !t -> Q ]] => [[ a -> Q ]] => no match, since one binding cannot fill two slots"+        , ExFormation+            [ BiTau (AtAny (Slot "t" 1)) ExRoot+            , BiTau (AtAny (Slot "t" 3)) ExRoot+            ]+        , ExFormation [BiTau (AtLabel "a") ExRoot]+        , []+        )+      ]+      (\(desc, ptn, tgt, expected) -> it desc (matchExpression ptn tgt `shouldBe` expected))+   describe "combine" $     forM_       [ ("combines two empty substitutions", substEmpty, substEmpty, Just substEmpty)@@ -473,26 +511,26 @@       ,         ( "combines an empty subst with a single-entry one"         , substEmpty-        , Subst (Map.singleton "at" (MvAttribute AtPhi))-        , Just (Subst (Map.singleton "at" (MvAttribute AtPhi)))+        , Subst (Map.singleton (Named "at") (MvAttribute AtPhi))+        , Just (Subst (Map.singleton (Named "at") (MvAttribute AtPhi)))         )       ,         ( "combines two substs with disjoint keys"-        , Subst (Map.singleton "first" (MvAttribute AtPhi))-        , Subst (Map.singleton "second" (MvBytes (BtOne "00")))-        , Just (Subst (Map.fromList [("first", MvAttribute AtPhi), ("second", MvBytes (BtOne "00"))]))+        , Subst (Map.singleton (Named "first") (MvAttribute AtPhi))+        , Subst (Map.singleton (Named "second") (MvBytes (BtOne "00")))+        , Just (Subst (Map.fromList [(Named "first", MvAttribute AtPhi), (Named "second", MvBytes (BtOne "00"))]))         )       ,         ( "keeps a shared key when both substs agree on its value"-        , Subst (Map.fromList [("first", MvAttribute AtRho), ("second", MvAttribute AtPhi)])-        , Subst (Map.singleton "first" (MvAttribute AtRho))-        , Just (Subst (Map.fromList [("first", MvAttribute AtRho), ("second", MvAttribute AtPhi)]))+        , Subst (Map.fromList [(Named "first", MvAttribute AtRho), (Named "second", MvAttribute AtPhi)])+        , Subst (Map.singleton (Named "first") (MvAttribute AtRho))+        , Just (Subst (Map.fromList [(Named "first", MvAttribute AtRho), (Named "second", MvAttribute AtPhi)]))         )-      , ("returns Nothing when a shared key disagrees", Subst (Map.singleton "x" (MvAttribute AtPhi)), Subst (Map.singleton "x" (MvAttribute AtRho)), Nothing)+      , ("returns Nothing when a shared key disagrees", Subst (Map.singleton (Named "x") (MvAttribute AtPhi)), Subst (Map.singleton (Named "x") (MvAttribute AtRho)), Nothing)       ,         ( "returns Nothing for the whole merge when any key conflicts"-        , Subst (Map.fromList [("x", MvAttribute AtRho), ("y", MvBytes (BtOne "1F"))])-        , Subst (Map.singleton "x" (MvAttribute AtPhi))+        , Subst (Map.fromList [(Named "x", MvAttribute AtRho), (Named "y", MvBytes (BtOne "1F"))])+        , Subst (Map.singleton (Named "x") (MvAttribute AtPhi))         , Nothing         )       ]

@@ -57,7 +57,7 @@       , ("T(x -> Q)", Just (ExApplication ExTermination (ArTau (AtLabel "x") ExRoot)))       , ("Q.org.eolang", Just (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang")))       , ("[[x -> $, y -> ?]]", Just (ExFormation [BiTau (AtLabel "x") ExXi, BiVoid (AtLabel "y"), BiVoid AtRho]))-      , ("Q.!t", Just (ExDispatch ExRoot (AtMeta "t")))+      , ("Q.!t1", Just (ExDispatch ExRoot (AtMeta "t1")))       , ("[[]](!t1 -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtMeta "t1") ExXi)))       ,         ( "[[]](~0 -> $)(~11 -> Q)"@@ -71,13 +71,13 @@             )         )       , ("[[]](x -> $, y -> Q)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtLabel "x") ExXi)) (ArTau (AtLabel "y") ExRoot)))-      , ("[[!B, !B1]]", Just (ExFormation [BiMeta "B", BiMeta "B1"]))+      , ("[[!B0, !B1]]", Just (ExFormation [BiMeta "B0", BiMeta "B1"]))       , ("[[!B2, !t2 -> $]]", Just (ExFormation [BiMeta "B2", BiTau (AtMeta "t2") ExXi]))       , ("!e0", Just (ExMeta "e0"))-      , ("!k", Just (ExMeta "k"))+      , ("!k1", Just (ExMeta "k1"))       , ("[[x -> !k1]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "k1"), BiVoid AtRho]))-      , ("[[x -> !e]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "e"), BiVoid AtRho]))-      , ("[[!t -> !e1]]", Just (ExFormation [BiTau (AtMeta "t") (ExMeta "e1")]))+      , ("[[x -> !e1]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "e1"), BiVoid AtRho]))+      , ("[[!t1 -> !e1]]", Just (ExFormation [BiTau (AtMeta "t1") (ExMeta "e1")]))       , ("[[D> --]]", Just (ExFormation [BiDelta BtEmpty, BiVoid AtRho]))       , ("[[D> 1F-]]", Just (ExFormation [BiDelta (BtOne "1F"), BiVoid AtRho]))       , ("[[\n  L> Func,\n  D> 00-\n]]", Just (ExFormation [BiLambda (Function "Func"), BiDelta (BtOne "00"), BiVoid AtRho]))@@ -104,10 +104,10 @@             )         )       ,-        ( "!e(x(^,@) -> [[w -> !e1]])"+        ( "!e0(x(^,@) -> [[w -> !e1]])"         , Just             ( ExApplication-                (ExMeta "e")+                (ExMeta "e0")                 ( ArTau                     (AtLabel "x")                     ( ExFormation@@ -120,7 +120,7 @@             )         )       ,-        ( "[[x -> y.z, w -> ^, u -> @, p -> !t, q -> !e]]"+        ( "[[x -> y.z, w -> ^, u -> @, p -> !t1, q -> !e1]]"         , Just             ( ExFormation                 [ BiTau@@ -134,10 +134,10 @@                     (ExDispatch ExXi AtPhi)                 , BiTau                     (AtLabel "p")-                    (ExDispatch ExXi (AtMeta "t"))+                    (ExDispatch ExXi (AtMeta "t1"))                 , BiTau                     (AtLabel "q")-                    (ExMeta "e")+                    (ExMeta "e1")                 , BiVoid AtRho                 ]             )@@ -192,12 +192,12 @@             )         )       ,-        ( "[[𝐵1, 𝜏0 -> $, x -> 𝑒]]"+        ( "[[𝐵1, 𝜏0 -> $, x -> 𝑒1]]"         , Just             ( ExFormation                 [ BiMeta "B1"                 , BiTau (AtMeta "t0") ExXi-                , BiTau (AtLabel "x") (ExMeta "e")+                , BiTau (AtLabel "x") (ExMeta "e1")                 ]             )         )@@ -309,10 +309,10 @@       , ("AB-", Just (BtOne "AB"))       , ("1F-2A-00", Just (BtMany ["1F", "2A", "00"]))       , ("01-02-03-04-05", Just (BtMany ["01", "02", "03", "04", "05"]))-      , ("!d", Just (BtMeta "d"))+      , ("!d1", Just (BtMeta "d1"))       , ("!d0", Just (BtMeta "d0"))       , ("!d_test", Just (BtMeta "d_test"))-      , ("δ", Just (BtMeta "d"))+      , ("δ1", Just (BtMeta "d1"))       , ("δ0", Just (BtMeta "d0"))       , ("GG-", Nothing)       , ("0-", Nothing)@@ -331,27 +331,27 @@       , ("@ -> $", Just (BiTau AtPhi ExXi))       , ("ρ -> Q", Just (BiTau AtRho ExRoot))       , ("φ -> T", Just (BiTau AtPhi ExTermination))-      , ("!t -> $", Just (BiTau (AtMeta "t") ExXi))+      , ("!t1 -> $", Just (BiTau (AtMeta "t1") ExXi))       , ("!t0 -> Q", Just (BiTau (AtMeta "t0") ExRoot))       , ("D> --", Just (BiDelta BtEmpty))       , ("D> 42-", Just (BiDelta (BtOne "42")))       , ("D> 01-02-03", Just (BiDelta (BtMany ["01", "02", "03"])))-      , ("D> !d", Just (BiDelta (BtMeta "d")))+      , ("D> !d1", Just (BiDelta (BtMeta "d1")))       , ("Δ ⤍ FF-", Just (BiDelta (BtOne "FF")))       , ("Δ ⤍ --", Just (BiDelta BtEmpty))       , ("L> Func", Just (BiLambda (Function "Func")))       , ("L> Function_name", Just (BiLambda (Function "Function_name")))       , ("L> Aφ", Just (BiLambda (Function "Aφ")))       , ("λ ⤍ Test", Just (BiLambda (Function "Test")))-      , ("L> !F", Just (BiLambda (FnMeta "F")))+      , ("L> !F1", Just (BiLambda (FnMeta "F1")))       , ("L> !F0", Just (BiLambda (FnMeta "F0")))-      , ("λ ⤍ 𝑓", Just (BiLambda (FnMeta "F")))+      , ("λ ⤍ 𝑓1", Just (BiLambda (FnMeta "F1")))       , ("L> 𝑓2", Just (BiLambda (FnMeta "F2")))-      , ("!B", Just (BiMeta "B"))+      , ("!B1", Just (BiMeta "B1"))       , ("!B0", Just (BiMeta "B0"))       , ("!B_test", Just (BiMeta "B_test"))-      , ("𝐵", Just (BiMeta "B"))       , ("𝐵1", Just (BiMeta "B1"))+      , ("𝐵1", Just (BiMeta "B1"))       , ("x() -> [[]]", Just (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho])))       , ("y(^) -> [[]]", Just (BiTau (AtLabel "y") (ExFormation [BiVoid AtRho])))       , ("z(^, @) -> [[]]", Just (BiTau (AtLabel "z") (ExFormation [BiVoid AtRho, BiVoid AtPhi])))@@ -375,10 +375,10 @@       , ("ρ", Just AtRho)       , ("@", Just AtPhi)       , ("φ", Just AtPhi)-      , ("!t", Just (AtMeta "t"))+      , ("!t1", Just (AtMeta "t1"))       , ("!t0", Just (AtMeta "t0"))       , ("!t_test", Just (AtMeta "t_test"))-      , ("𝜏", Just (AtMeta "t"))+      , ("𝜏1", Just (AtMeta "t1"))       , ("𝜏0", Just (AtMeta "t0"))       , ("a0", Just (AtLabel "a0"))       , ("a1", Just (AtLabel "a1"))@@ -526,28 +526,51 @@       , ("[[]](Q, T)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) ExRoot)) (ArAlpha (Alpha 1) ExTermination)))       , ("Q.x(y -> $)", Just (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") ExXi)))       , ("[[x -> ?]].x(Q)", Just (ExApplication (ExDispatch (ExFormation [BiVoid (AtLabel "x"), BiVoid AtRho]) (AtLabel "x")) (ArAlpha (Alpha 0) ExRoot)))-      , ("[[]](~!i -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i") ExXi)))-      , ("[[]](α𝑖 -> Q)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i") ExRoot)))+      , ("[[]](~!i1 -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i1") ExXi)))+      , ("[[]](α𝑖1 -> Q)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i1") ExRoot)))       , ("Q.foo(a1 -> Q.y)", Just (ExApplication (ExDispatch ExRoot (AtLabel "foo")) (ArTau (AtLabel "a1") (ExDispatch ExRoot (AtLabel "y"))))) -- #875: "a"-prefixed label in argument position is a named binding, not a positional alpha       ]    describe "parse meta expressions" $     test       parseExpression-      [ ("!e", Just (ExMeta "e"))+      [ ("!e1", Just (ExMeta "e1"))       , ("!e0", Just (ExMeta "e0"))       , ("!e_test", Just (ExMeta "e_test"))-      , ("𝑒", Just (ExMeta "e"))+      , ("𝑒1", Just (ExMeta "e1"))       , ("𝑒0", Just (ExMeta "e0"))-      , ("!e.x", Just (ExDispatch (ExMeta "e") (AtLabel "x")))-      , ("!e(Q)", Just (ExApplication (ExMeta "e") (ArAlpha (Alpha 0) ExRoot)))-      , ("!n", Just (ExMeta "n"))+      , ("!e1.x", Just (ExDispatch (ExMeta "e1") (AtLabel "x")))+      , ("!e1(Q)", Just (ExApplication (ExMeta "e1") (ArAlpha (Alpha 0) ExRoot)))       , ("!n1", Just (ExMeta "n1"))-      , ("𝑛", Just (ExMeta "n"))+      , ("!n1", Just (ExMeta "n1"))       , ("𝑛1", Just (ExMeta "n1"))-      , ("𝑛.x", Just (ExDispatch (ExMeta "n") (AtLabel "x")))+      , ("𝑛1", Just (ExMeta "n1"))+      , ("𝑛1.x", Just (ExDispatch (ExMeta "n1") (AtLabel "x")))       ] +  describe "parse anonymous meta-variables" $+    -- A meta written without an index is anonymous: it stands for whatever term+    -- fills its place and no rule may name it afterwards. It is told apart from+    -- every other anonymous meta of the same term by the offset it starts at,+    -- which is why one formation may carry two of the same kind (#218).+    test+      parseExpression+      [ ("!e", Just (ExAny (Slot "e" 0)))+      , ("𝑒", Just (ExAny (Slot "e" 0)))+      , ("!n", Just (ExAny (Slot "n" 0)))+      , ("𝑘", Just (ExAny (Slot "k" 0)))+      , ("!e.x", Just (ExDispatch (ExAny (Slot "e" 0)) (AtLabel "x")))+      ,+        ( "⟦ 𝜏 ↦ 𝑒, 𝜏 ↦ 𝑒 ⟧"+        , Just+            ( ExFormation+                [ BiTau (AtAny (Slot "t" 2)) (ExAny (Slot "e" 6))+                , BiTau (AtAny (Slot "t" 9)) (ExAny (Slot "e" 13))+                ]+            )+        )+      ]+   describe "parse whitespace handling" $     forM_       [ "[[  x   ->   Q  ]]"@@ -561,9 +584,9 @@   describe "parse unicode meta-k expression" $     test       parseExpression-      [ ("𝑘", Just (ExMeta "k"))+      [ ("𝑘1", Just (ExMeta "k1"))       , ("𝑘1", Just (ExMeta "k1"))-      , ("𝑘.x", Just (ExDispatch (ExMeta "k") (AtLabel "x")))+      , ("𝑘1.x", Just (ExDispatch (ExMeta "k1") (AtLabel "x")))       ]    describe "ParserException Show instance" $@@ -597,7 +620,7 @@     forM_       [ ("exposes an _alpha field parsing an alpha directly", parseMaybe (_alpha phiParser) "~3" `shouldBe` Just (Alpha 3))       , ("exposes an _attribute field parsing an attribute directly", parseMaybe (_attribute phiParser) "foo" `shouldBe` Just (AtLabel "foo"))-      , ("exposes an _index field parsing an index meta directly", parseMaybe (_index phiParser) "!i0" `shouldBe` Just "i0")+      , ("exposes an _index field parsing an index meta directly", parseMaybe (_index phiParser) "!i0" `shouldBe` Just (Right "i0"))       , ("exposes a _binding field parsing a binding directly", parseMaybe (_binding phiParser) "x -> $" `shouldBe` Just (BiTau (AtLabel "x") ExXi))       , ("exposes an _expression field parsing an expression directly", parseMaybe (_expression phiParser) "Q.x" `shouldBe` Just (ExDispatch ExRoot (AtLabel "x")))       , ("exposes a _string field parsing a quoted string directly", parseMaybe (_string phiParser) "\"hi\"" `shouldBe` Just "hi")

@@ -15,7 +15,7 @@ import Encoding (Encoding (..)) import Lining (LineFormat (..)) import Margin (defaultMargin)-import Matcher (MetaValue (..), Subst (Subst))+import Matcher (Meta (Named), MetaValue (..), Subst (Subst)) import Parser (parseExpression) import Printer import Sugar (SugarType (..))@@ -258,28 +258,28 @@    describe "printSubsts and printSubsts' render substitutions" $     forM_-      [ ("MvAttribute", [Subst (Map.singleton "t" (MvAttribute (AtLabel "x")))], (SWEET, UNICODE, MULTILINE, defaultMargin), "t >> x")-      , ("MvIndex", [Subst (Map.singleton "i" (MvIndex 3))], (SWEET, UNICODE, MULTILINE, defaultMargin), "i >> 3")-      , ("MvExpression", [Subst (Map.singleton "e" (MvExpression ExRoot))], (SWEET, UNICODE, MULTILINE, defaultMargin), "e >> Φ")-      , ("MvBytes", [Subst (Map.singleton "b" (MvBytes (BtOne "1F")))], (SWEET, UNICODE, MULTILINE, defaultMargin), "b >> 1F-")-      , ("MvBindings", [Subst (Map.singleton "bnd" (MvBindings [BiVoid (AtLabel "y")]))], (SWEET, UNICODE, MULTILINE, defaultMargin), "bnd >> ⟦ y ↦ ∅ ⟧")-      , ("MvFunction", [Subst (Map.singleton "f" (MvFunction "func"))], (SWEET, UNICODE, MULTILINE, defaultMargin), "f >> func")+      [ ("MvAttribute", [Subst (Map.singleton (Named "t") (MvAttribute (AtLabel "x")))], (SWEET, UNICODE, MULTILINE, defaultMargin), "t >> x")+      , ("MvIndex", [Subst (Map.singleton (Named "i") (MvIndex 3))], (SWEET, UNICODE, MULTILINE, defaultMargin), "i >> 3")+      , ("MvExpression", [Subst (Map.singleton (Named "e") (MvExpression ExRoot))], (SWEET, UNICODE, MULTILINE, defaultMargin), "e >> Φ")+      , ("MvBytes", [Subst (Map.singleton (Named "b") (MvBytes (BtOne "1F")))], (SWEET, UNICODE, MULTILINE, defaultMargin), "b >> 1F-")+      , ("MvBindings", [Subst (Map.singleton (Named "bnd") (MvBindings [BiVoid (AtLabel "y")]))], (SWEET, UNICODE, MULTILINE, defaultMargin), "bnd >> ⟦ y ↦ ∅ ⟧")+      , ("MvFunction", [Subst (Map.singleton (Named "f") (MvFunction "func"))], (SWEET, UNICODE, MULTILINE, defaultMargin), "f >> func")       ,         ( "keys of a multi-entry substitution are sorted and each is on its own line"-        , [Subst (Map.fromList [("a", MvIndex 1), ("b", MvIndex 2)])]+        , [Subst (Map.fromList [(Named "a", MvIndex 1), (Named "b", MvIndex 2)])]         , (SWEET, UNICODE, MULTILINE, defaultMargin)         , "a >> 1\nb >> 2"         )       ,         ( "multiple substitutions are separated with a dashed line"-        , [Subst (Map.singleton "a" (MvIndex 1)), Subst (Map.singleton "b" (MvIndex 2))]+        , [Subst (Map.singleton (Named "a") (MvIndex 1)), Subst (Map.singleton (Named "b") (MvIndex 2))]         , (SWEET, UNICODE, MULTILINE, defaultMargin)         , "a >> 1\n------\nb >> 2"         )       , ("an empty substitution list renders the dashed placeholder", [], (SWEET, UNICODE, SINGLELINE, defaultMargin), "------")       ,         ( "picks the encoding from its PrintConfig for an attribute meta value (ASCII rho)"-        , [Subst (Map.singleton "t" (MvAttribute AtRho))]+        , [Subst (Map.singleton (Named "t") (MvAttribute AtRho))]         , (SWEET, ASCII, SINGLELINE, defaultMargin)         , "t >> ^"         )

@@ -18,16 +18,19 @@ import Files (allPathsIn) import System.FilePath import Test.Hspec (Spec, describe, expectationFailure, it, runIO, shouldBe, shouldSatisfy, shouldThrow)-import Yaml (Condition (..), ContextualizeRule (..), DataizeRule (..), MorphRule (..), Number, Operation (..), Premise (..), contextualizationRules, dataizationRules, morphingRules, yamlRule)+import Yaml (Condition (..), ContextualizeRule (..), DataizeRule (..), MorphRule (..), Number, Operation (..), Premise (..), Rule, contextualizationRules, dataizationRules, morphingRules, yamlRule)  decodeYaml' :: (Yaml.FromJSON a) => String -> Either Yaml.ParseException a decodeYaml' = Yaml.decodeEither' . encodeUtf8 . T.pack -failsAsRedundant :: Either Yaml.ParseException a -> Bool-failsAsRedundant decoded = case decoded of-  Left err -> "redundant" `isInfixOf` Yaml.prettyPrintParseException err+failsWith :: String -> Either Yaml.ParseException a -> Bool+failsWith fragment decoded = case decoded of+  Left err -> fragment `isInfixOf` Yaml.prettyPrintParseException err   Right _ -> False +failsAsRedundant :: Either Yaml.ParseException a -> Bool+failsAsRedundant = failsWith "redundant"+ spec :: Spec spec = do   describe "parses yaml rule" $ do@@ -70,6 +73,103 @@       ( \(desc, yaml, valid) ->           it ("rejects " ++ desc) (unless valid (expectationFailure ("expected rejection for: " ++ yaml)))       )++  describe "rejects an anonymous meta outside a pattern" $ do+    -- An anonymous meta is bound by the pattern it stands in and forgotten as+    -- soon as that pattern matches, so no other part of a rule has a name to+    -- read it back by. Writing one there is a mistake in the rule, caught as+    -- the rule loads rather than left to surface as a silent non-match.+    let rewriting :: String -> String+        rewriting field = "name: foo\npattern: '⟦ 𝜏1 ↦ 𝑒1 ⟧'\n" ++ field+        inferring :: String -> String+        inferring field = "name: foo\nmatch: '⟦ 𝜏1 ↦ 𝑒1 ⟧'\n" ++ field+    forM_+      [+        ( "in 'result' of a rewriting rule"+        , failsWith+            "anonymous meta '!e' cannot be referenced in 'result' of rule 'foo'"+            (decodeYaml' (rewriting "result: '𝑒'") :: Either Yaml.ParseException Rule)+        )+      ,+        ( "in 'when' of a rewriting rule"+        , failsWith+            "anonymous meta '!t' cannot be referenced in 'when' of rule 'foo'"+            (decodeYaml' (rewriting "result: '⟦ ⟧'\nwhen:\n  in: ['𝜏', '!B1']") :: Either Yaml.ParseException Rule)+        )+      ,+        ( "in 'where' of a rewriting rule"+        , failsWith+            "anonymous meta '!e' cannot be referenced in 'where' of rule 'foo'"+            (decodeYaml' (rewriting "result: '⟦ ⟧'\nwhere:\n  - meta: '!t1'\n    function: concat\n    args: ['𝑒']") :: Either Yaml.ParseException Rule)+        )+      ,+        ( "in 'having' of a rewriting rule"+        , failsWith+            "anonymous meta '!e' cannot be referenced in 'having' of rule 'foo'"+            (decodeYaml' (rewriting "result: '⟦ ⟧'\nhaving:\n  formation: '𝑒'") :: Either Yaml.ParseException Rule)+        )+      ,+        ( "as a bare index meta in 'when' of a rewriting rule"+        , failsWith+            "anonymous meta '!i' cannot be referenced in 'when' of rule 'foo'"+            (decodeYaml' (rewriting "result: '⟦ ⟧'\nwhen:\n  eq: ['𝑖', 1]") :: Either Yaml.ParseException Rule)+        )+      ,+        ( "inside an 'nf' condition of a rewriting rule"+        , failsWith+            "anonymous meta '!e' cannot be referenced in 'when' of rule 'foo'"+            (decodeYaml' (rewriting "result: '⟦ ⟧'\nwhen:\n  nf: '𝑒'") :: Either Yaml.ParseException Rule)+        )+      ,+        ( "in 'n-result' of a morphing rule"+        , failsWith+            "anonymous meta '!n' cannot be referenced in 'n-result' of rule 'foo'"+            (decodeYaml' (inferring "e-match: 𝑒0\nn-result: '𝑛'") :: Either Yaml.ParseException MorphRule)+        )+      ,+        ( "in a premise of a morphing rule"+        , failsWith+            "anonymous meta '!e' cannot be referenced in 'premises' of rule 'foo'"+            (decodeYaml' (inferring "e-match: 𝑒0\nn-result: 𝑛1\npremises:\n  - n-result: 𝑛1\n    normalize: '𝑒'") :: Either Yaml.ParseException MorphRule)+        )+      ,+        ( "in 'when' of a morphing rule"+        , failsWith+            "anonymous meta '!e' cannot be referenced in 'when' of rule 'foo'"+            (decodeYaml' (inferring "e-match: 𝑒0\nn-result: 𝑛1\nwhen:\n  formation: '𝑒'") :: Either Yaml.ParseException MorphRule)+        )+      ,+        ( "in 'd-result' of a dataization rule"+        , failsWith+            "anonymous meta '!d' cannot be referenced in 'd-result' of rule 'foo'"+            (decodeYaml' (inferring "e-match: 𝑒0\nd-result: 'δ'") :: Either Yaml.ParseException DataizeRule)+        )+      ,+        ( "in 'when' of a dataization rule"+        , failsWith+            "anonymous meta '!e' cannot be referenced in 'when' of rule 'foo'"+            (decodeYaml' (inferring "e-match: 𝑒0\nd-result: δ0\nwhen:\n  formation: '𝑒'") :: Either Yaml.ParseException DataizeRule)+        )+      ,+        ( "in a premise of a dataization rule"+        , failsWith+            "anonymous meta '!e' cannot be referenced in 'premises' of rule 'foo'"+            (decodeYaml' (inferring "e-match: 𝑒0\nd-result: δ0\npremises:\n  - d-result: δ0\n    dataize: '𝑒'") :: Either Yaml.ParseException DataizeRule)+        )+      ,+        ( "in a premise of a contextualization rule"+        , failsWith+            "anonymous meta '!e' cannot be referenced in 'premises' of rule 'foo'"+            (decodeYaml' (inferring "c-match: 𝑘0\nc-result: 𝑛1\npremises:\n  - n-result: 𝑛1\n    normalize: '𝑒'") :: Either Yaml.ParseException ContextualizeRule)+        )+      ,+        ( "in 'c-result' of a contextualization rule"+        , failsWith+            "anonymous meta '!k' cannot be referenced in 'c-result' of rule 'foo'"+            (decodeYaml' (inferring "c-match: 𝑘0\nc-result: '𝑘'") :: Either Yaml.ParseException ContextualizeRule)+        )+      ]+      (\(desc, rejected) -> it ("rejects an anonymous meta " ++ desc) (rejected `shouldBe` True))    describe "keeps effective labels unique across rule sets" $     -- The effective label of a rule is its 'label' when present, else its