diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -260,11 +260,15 @@ {"id": 9, "𝑛": "⟦ Ξ” ‍ 40-08-00-00-00-00-00-00 ⟧", "Ξ”": "40-08-00-00-00-00-00-00"} ``` -Every segment but the last has to name a formation to go on into, and -`reduce` applies to the node the path ends at. A segment the formation does -not carry, or one that runs into a void attribute, fails the fire the same -way a missing `attr` does. `phino` holds the receiver whole, so there is no -depth a program has to re-parse an answer to reach. +Every segment but the last has to name a formation or an application to go on +into, and `reduce` applies to the node the path ends at. An argument binds an +attribute the way a Ο„ binding does, so `x.if.guard` reaches the `guard` of +`x ↦ Ξ¦.bool( if ↦ ⟦ guard ↦ … ⟧ )`, and it binds it from the outside, so an +argument wins over the void it fills. A positional argument names nothing and +the walk goes past it. A segment nothing carries, or one that runs into a void +attribute, fails the fire the same way a missing `attr` does. `phino` holds the +receiver whole, so there is no depth a program has to re-parse an answer to +reach. What the answered node is, `phino` says next to it, because the shape of an answer is `phino`'s knowledge and not the program's. A formation carrying a Ξ” diff --git a/phino.cabal b/phino.cabal --- a/phino.cabal +++ b/phino.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino -version: 0.0.131 +version: 0.0.132 license: MIT synopsis: Command-Line Manipulator of πœ‘-Calculus Expressions description: Please see the README on GitHub at @@ -12,7 +12,7 @@ copyright: 2025 Objectionary.com category: Language, Code Analysis build-type: Simple -extra-source-files: resources/*.yaml resources/normalize/*.yaml +extra-source-files: resources/normalize/*.yaml resources/morphing/*.yaml resources/dataization/*.yaml resources/contextualization/*.yaml extra-doc-files: README.md source-repository head @@ -61,6 +61,7 @@ Matcher Merge Misc + Morph Must Parser Printer @@ -152,6 +153,7 @@ MatcherSpec MergeSpec MiscSpec + MorphSpec MustSpec ParserSpec Paths_phino diff --git a/resources/contextualization.yaml b/resources/contextualization.yaml deleted file mode 100644 --- a/resources/contextualization.yaml +++ /dev/null @@ -1,81 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -# Contextualization π’ž β€” applied top-to-bottom, first matching clause wins. It is -# binary, π’ž(n, c): n is the term being contextualized and c is the context (the -# expression that every free ΞΎ inside n stands for). π’ž walks the term -# structurally, replacing each ΞΎ with the context c, descending through -# dispatches and applications and stopping at formations β€” which introduce their -# own scope and are returned untouched β€” and at the global Ξ¦ and termination βŠ₯. -# The context c is supplied by the caller: DOT dispatching 𝜏 on a formation -# passes that formation WITHOUT the dispatched binding (⟦𝐡1, 𝐡2⟧), so a -# self-referential ΞΎ resolves to an object that lacks 𝜏 and collapses to βŠ₯ -# rather than re-deriving the dispatch and diverging. -# -# Each rule is an inference rule: when 'match' matches the term and 'c-match' -# matches the context (binding the meta c), the rule yields the conclusion -# 'c-result' (a premise meta or a literal), provided the ordered 'premises' -# reduce as stated. A premise binds its 'n-result' to one π’ž ('contextualize') -# judgment. 'c-match' is the context-argument matcher of π’ž(n, c); it is always -# the π‘˜0 meta. Derived terms are named 𝑛1, 𝑛2, … in premise order; the term π’ž is -# handed is 𝑛0, leaving that numbering to the premises alone. A meta the rule -# never reads back is written bare: it matches whatever stands in its place, -# binds nothing and cannot be referenced. - -- name: cg - match: Ξ¦ - c-match: π‘˜0 - c-result: Ξ¦ - -- name: cxi - match: ΞΎ - c-match: π‘˜0 - c-result: π‘˜0 - -- name: ct - match: βŠ₯ - c-match: π‘˜0 - c-result: βŠ₯ - -- name: cf - match: ⟦𝐡0⟧ - c-match: π‘˜0 - c-result: ⟦𝐡0⟧ - -- name: cd - match: '𝑛0.𝜏0' - c-match: π‘˜0 - c-result: '𝑛1.𝜏0' - premises: - - n-result: 𝑛1 - contextualize: - - 𝑛0 - - π‘˜0 - -- name: ca - match: '𝑛0(𝜏0 ↦ 𝑒1)' - c-match: π‘˜0 - c-result: '𝑛1(𝜏0 ↦ 𝑛2)' - premises: - - n-result: 𝑛1 - contextualize: - - 𝑛0 - - π‘˜0 - - n-result: 𝑛2 - contextualize: - - 𝑒1 - - π‘˜0 - -- name: caa - match: '𝑛0(α𝑖0 ↦ 𝑒1)' - c-match: π‘˜0 - c-result: '𝑛1(α𝑖0 ↦ 𝑛2)' - premises: - - n-result: 𝑛1 - contextualize: - - 𝑛0 - - π‘˜0 - - n-result: 𝑛2 - contextualize: - - 𝑒1 - - π‘˜0 diff --git a/resources/contextualization/ca.yaml b/resources/contextualization/ca.yaml new file mode 100644 --- /dev/null +++ b/resources/contextualization/ca.yaml @@ -0,0 +1,16 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: ca +match: '𝑛0(𝜏0 ↦ 𝑒1)' +c-match: π‘˜0 +c-result: '𝑛1(𝜏0 ↦ 𝑛2)' +premises: + - n-result: 𝑛1 + contextualize: + - 𝑛0 + - π‘˜0 + - n-result: 𝑛2 + contextualize: + - 𝑒1 + - π‘˜0 diff --git a/resources/contextualization/caa.yaml b/resources/contextualization/caa.yaml new file mode 100644 --- /dev/null +++ b/resources/contextualization/caa.yaml @@ -0,0 +1,16 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: caa +match: '𝑛0(α𝑖0 ↦ 𝑒1)' +c-match: π‘˜0 +c-result: '𝑛1(α𝑖0 ↦ 𝑛2)' +premises: + - n-result: 𝑛1 + contextualize: + - 𝑛0 + - π‘˜0 + - n-result: 𝑛2 + contextualize: + - 𝑒1 + - π‘˜0 diff --git a/resources/contextualization/cd.yaml b/resources/contextualization/cd.yaml new file mode 100644 --- /dev/null +++ b/resources/contextualization/cd.yaml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: cd +match: '𝑛0.𝜏0' +c-match: π‘˜0 +c-result: '𝑛1.𝜏0' +premises: + - n-result: 𝑛1 + contextualize: + - 𝑛0 + - π‘˜0 diff --git a/resources/contextualization/cf.yaml b/resources/contextualization/cf.yaml new file mode 100644 --- /dev/null +++ b/resources/contextualization/cf.yaml @@ -0,0 +1,7 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: cf +match: ⟦𝐡0⟧ +c-match: π‘˜0 +c-result: ⟦𝐡0⟧ diff --git a/resources/contextualization/cg.yaml b/resources/contextualization/cg.yaml new file mode 100644 --- /dev/null +++ b/resources/contextualization/cg.yaml @@ -0,0 +1,7 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: cg +match: Ξ¦ +c-match: π‘˜0 +c-result: Ξ¦ diff --git a/resources/contextualization/ct.yaml b/resources/contextualization/ct.yaml new file mode 100644 --- /dev/null +++ b/resources/contextualization/ct.yaml @@ -0,0 +1,7 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: ct +match: βŠ₯ +c-match: π‘˜0 +c-result: βŠ₯ diff --git a/resources/contextualization/cxi.yaml b/resources/contextualization/cxi.yaml new file mode 100644 --- /dev/null +++ b/resources/contextualization/cxi.yaml @@ -0,0 +1,7 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: cxi +match: ΞΎ +c-match: π‘˜0 +c-result: π‘˜0 diff --git a/resources/dataization.yaml b/resources/dataization.yaml deleted file mode 100644 --- a/resources/dataization.yaml +++ /dev/null @@ -1,101 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -# Dataization 𝔻 β€” applied top-to-bottom, first matching clause wins. It is -# ternary, 𝔻(n, e, s): the second argument e is the global universe, the same -# expression that 𝕄 takes as its second argument (𝔻 forwards it to 𝕄), and the -# third argument s is the mutable state, threaded through and returned possibly -# changed. Only the 'fire' rule changes it, by firing an atom through 𝔼. The -# first argument is always a normal form: a non-NF expression matches no clause. -# -# Each rule is an inference rule: when 'match' matches the term and 'e-match' -# matches the universe (binding the meta e), the rule yields the conclusion -# 'd-result' (a premise bytes meta or a literal), provided 'when' holds and the -# ordered 'premises' reduce as stated. A premise binds its 'n-result'/'d-result' -# to one judgment β€” 𝔻 ('dataize'), 𝕄 ('morph'), 𝒩 ('normalize'), 𝔼 ('evaluate') -# or π’ž ('contextualize'). 'e-match' is the universe-argument matcher of -# 𝔻(n, e); it is always the 𝑒0 meta. The single bytes result is named Ξ΄0. A -# normal-form-valued result (𝕄 'morph', 𝒩 'normalize', 𝔼 'evaluate') is named -# 𝑛1, 𝑛2, … in premise order; the term 𝔻 is handed is 𝑛0, leaving that -# numbering to the premises alone. An expression-valued result (π’ž -# 'contextualize') is not a normal form β€” that is why a 'normalize' premise -# follows it β€” so it takes an 𝑒-family name (𝑒1, 𝑒2, …, the next index free of -# 'match', 𝑒0 itself being the universe) rather than an 𝑛 name reserved for -# normal forms. A meta the rule never reads back is written bare: it matches -# whatever stands in its place, binds nothing and cannot be referenced. -# -# The clauses are disjoint, so their relative order does not change behavior. -# 'norm' matches the lone meta 𝑛0, which unifies with any expression, so it is -# guarded to fire only when 𝑛0 is neither a formation ('not (formation 𝑛0)', -# carving out 'delta', 'box', 'fire' and 'none') nor the termination βŠ₯ -# ('not (𝑛0 = βŠ₯)'). 𝔻 is partial: βŠ₯ (the terminator T) signals an error and -# lies outside its domain, so it deliberately matches no clause and dataization -# stops there β€” there is no 'end' rule mapping βŠ₯ to empty bytes (see #955). -# Without the guard 'norm' would behave correctly only by being declared last; -# with it the clauses no longer rely on their order. - -- name: delta - label: \Delta - match: ⟦𝐡1, Ξ” ‍ Ξ΄0, 𝐡2⟧ - e-match: 𝑒0 - d-result: Ξ΄0 - -- name: box - match: ⟦𝐡1, Ο† ↦ 𝑒1, 𝐡2⟧ - e-match: 𝑒0 - d-result: Ξ΄0 - when: - disjoint: - - [Ξ”, Ξ»] - - [𝐡1, 𝐡2] - premises: - - n-result: 𝑒2 - contextualize: - - 𝑒1 - - ⟦𝐡1, Ο† ↦ 𝑒1, 𝐡2⟧ - - n-result: 𝑛1 - normalize: 𝑒2 - - d-result: Ξ΄0 - dataize: 𝑛1 - -- name: fire - match: ⟦𝐡1, Ξ» ‍ 𝑓0, 𝐡2⟧ - e-match: 𝑒0 - d-result: Ξ΄0 - premises: - - n-result: 𝑛1 - evaluate: - - ⟦𝐡1, Ξ» ‍ 𝑓0, 𝐡2⟧ - - 𝑒0 - - d-result: Ξ΄0 - dataize: 𝑛1 - -- name: none - match: ⟦𝐡0⟧ - e-match: 𝑒0 - d-result: Ξ΄0 - when: - disjoint: - - [Ξ”, Ξ», Ο†] - - [𝐡0] - premises: - - d-result: Ξ΄0 - dataize: βŠ₯ - -- name: norm - match: 𝑛0 - e-match: 𝑒0 - d-result: Ξ΄0 - when: - and: - - not: - formation: 𝑛0 - - not: - eq: - - 𝑛0 - - βŠ₯ - premises: - - n-result: 𝑛1 - morph: 𝑛0 - - d-result: Ξ΄0 - dataize: 𝑛1 diff --git a/resources/dataization/box.yaml b/resources/dataization/box.yaml new file mode 100644 --- /dev/null +++ b/resources/dataization/box.yaml @@ -0,0 +1,20 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: box +match: ⟦𝐡1, Ο† ↦ 𝑒1, 𝐡2⟧ +e-match: 𝑒0 +d-result: Ξ΄0 +when: + disjoint: + - [Ξ”, Ξ»] + - [𝐡1, 𝐡2] +premises: + - n-result: 𝑒2 + contextualize: + - 𝑒1 + - ⟦𝐡1, Ο† ↦ 𝑒1, 𝐡2⟧ + - n-result: 𝑛1 + normalize: 𝑒2 + - d-result: Ξ΄0 + dataize: 𝑛1 diff --git a/resources/dataization/delta.yaml b/resources/dataization/delta.yaml new file mode 100644 --- /dev/null +++ b/resources/dataization/delta.yaml @@ -0,0 +1,8 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: delta +label: \Delta +match: ⟦𝐡1, Ξ” ‍ Ξ΄0, 𝐡2⟧ +e-match: 𝑒0 +d-result: Ξ΄0 diff --git a/resources/dataization/fire.yaml b/resources/dataization/fire.yaml new file mode 100644 --- /dev/null +++ b/resources/dataization/fire.yaml @@ -0,0 +1,14 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: fire +match: ⟦𝐡1, Ξ» ‍ 𝑓0, 𝐡2⟧ +e-match: 𝑒0 +d-result: Ξ΄0 +premises: + - n-result: 𝑛1 + evaluate: + - ⟦𝐡1, Ξ» ‍ 𝑓0, 𝐡2⟧ + - 𝑒0 + - d-result: Ξ΄0 + dataize: 𝑛1 diff --git a/resources/dataization/none.yaml b/resources/dataization/none.yaml new file mode 100644 --- /dev/null +++ b/resources/dataization/none.yaml @@ -0,0 +1,14 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: none +match: ⟦𝐡0⟧ +e-match: 𝑒0 +d-result: Ξ΄0 +when: + disjoint: + - [Ξ”, Ξ», Ο†] + - [𝐡0] +premises: + - d-result: Ξ΄0 + dataize: βŠ₯ diff --git a/resources/dataization/norm.yaml b/resources/dataization/norm.yaml new file mode 100644 --- /dev/null +++ b/resources/dataization/norm.yaml @@ -0,0 +1,20 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: norm +match: 𝑛0 +e-match: 𝑒0 +d-result: Ξ΄0 +when: + and: + - not: + formation: 𝑛0 + - not: + eq: + - 𝑛0 + - βŠ₯ +premises: + - n-result: 𝑛1 + morph: 𝑛0 + - d-result: Ξ΄0 + dataize: 𝑛1 diff --git a/resources/morphing.yaml b/resources/morphing.yaml deleted file mode 100644 --- a/resources/morphing.yaml +++ /dev/null @@ -1,190 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -# Morphing 𝕄 β€” applied top-to-bottom, first matching clause wins. It is ternary, -# 𝕄(n, e, s): n is the morphed term, e is the fixed global universe and s is -# the mutable state. The universe is threaded unchanged through every recursive -# call and substituted for Ξ¦ by the 'universe' rule (Ξ¦, rendered Q, is just the -# locator of e); the state is threaded too and the new state returned. Only the -# 'ml' rule changes it, by firing an atom through 𝔼. The first argument is -# always a normal form: a non-NF expression matches no clause. 𝕄 navigates a -# normal form to a formation one operation at a time, resolving Ξ¦ against e and -# peeling dispatches and applications through normalization 𝒩. It never fires a -# bare atom: a saturated Ξ»-formation is returned untouched and fired later by 𝔼 -# (the 'fire' rule of 𝔻). -# -# Each rule is an inference rule: when 'match' matches the term and 'e-match' -# matches the universe (binding the meta e), the rule yields the conclusion -# 'n-result' (a premise meta or a literal), provided 'when' holds and the -# ordered 'premises' reduce as stated. A premise binds 'n-result' to the result -# of one judgment β€” 𝕄 ('morph'), 𝒩 ('normalize') or 𝔼 ('evaluate'). 'e-match' is -# the universe-argument matcher of 𝕄(n, e); usually the 𝑒0 meta, but a rule may -# pin it to a literal (e.g. 'mg' fires only on 𝕄(Ξ¦, Ξ¦)). Every judgment here is -# normal-form-valued (𝕄 'morph', 𝒩 'normalize', 𝔼 'evaluate' β€” 𝔼 normalizes its -# atom's result internally), so premise results are named 𝑛1, 𝑛2, … in premise -# order. The term a rule morphs is 𝑛0 and its universe 𝑒0, leaving that -# numbering to the premises alone; the 𝑒-family stays reserved for the universe. -# A meta the rule never reads back is written bare (see 'mad'): it matches -# whatever stands in its place, binds nothing and cannot be referenced. -# -# 'ml' and 'md' are kept mutually exclusive: 'md' fires only -# when its head 𝑛0 is not a formation ('not (formation 𝑛0)'), so every formation -# head β€” Ξ»-bearing or not β€” is left to 'ml' (and 'mf'). The two clauses -# are disjoint and their relative order does not change behavior. -# -# 'ma'/'maa' and 'mad'/'maad' partition application-headed normal forms on -# the argument's absoluteness (#959). Both pairs pin the argument to a -# normal-form meta, so the split is total over the normal forms 𝕄 actually -# sees: 'ma'/'maa' take a 'π‘˜1' argument β€” absolute (xi-free) and in normal -# form β€” and recurse by re-normalizing the application; 'mad'/'maad' take an -# '𝑛1' argument (a normal form) that is 'not (absolute 𝑛1)' and yield βŠ₯ -# through a single 'morph: βŠ₯' premise, which terminates at once via the -# 'dead' axiom (𝕄(βŠ₯, e, s) β†’ (βŠ₯, s)) β€” no recursion. A non-absolute argument -# can never fill a slot, so βŠ₯ is the correct outcome and morphing stays -# total: exactly one of the four fires, and these βŠ₯ premises add no regress. -# Without them, a void slot receiving a -# non-absolute argument β€” e.g. ⟦ x ↦ βˆ… ⟧( x ↦ ΞΎ.foo ) β€” had no terminating -# derivation: 'copy' cannot fire on a non-absolute argument, so 'ma' -# re-morphed the identical stuck term forever. - -- name: mf - match: ⟦𝐡0⟧ - e-match: 𝑒0 - n-result: ⟦𝐡0⟧ - -- name: ml - label: \lambda - match: '⟦𝐡1, Ξ» ‍ 𝑓0, 𝐡2⟧.𝜏0' - e-match: 𝑒0 - n-result: 𝑛3 - premises: - - n-result: 𝑛1 - evaluate: - - '⟦𝐡1, Ξ» ‍ 𝑓0, 𝐡2⟧' - - 𝑒0 - - n-result: 𝑛2 - normalize: '𝑛1.𝜏0' - - n-result: 𝑛3 - morph: 𝑛2 - -- name: mphi - label: \varphi - match: ⟦𝐡0⟧.𝜏0 - e-match: 𝑒0 - n-result: 𝑛2 - when: - and: - - in: - - Ο† - - 𝐡0 - - not: - in: - - 𝜏0 - - 𝐡0 - - not: - in: - - Ξ» - - 𝐡0 - premises: - - n-result: 𝑛1 - normalize: ⟦𝐡0⟧.Ο†.𝜏0 - - n-result: 𝑛2 - morph: 𝑛1 - -- name: md - match: '𝑛0.𝜏0' - e-match: 𝑒0 - n-result: 𝑛3 - when: - not: - formation: 𝑛0 - premises: - - n-result: 𝑛1 - morph: 𝑛0 - - n-result: 𝑛2 - normalize: '𝑛1.𝜏0' - - n-result: 𝑛3 - morph: 𝑛2 - -- name: ma - match: '𝑛0(𝜏0 ↦ π‘˜1)' - e-match: 𝑒0 - n-result: 𝑛3 - premises: - - n-result: 𝑛1 - morph: 𝑛0 - - n-result: 𝑛2 - normalize: '𝑛1(𝜏0 ↦ π‘˜1)' - - n-result: 𝑛3 - morph: 𝑛2 - -- name: maa - match: '𝑛0(α𝑖0 ↦ π‘˜1)' - e-match: 𝑒0 - n-result: 𝑛3 - premises: - - n-result: 𝑛1 - morph: 𝑛0 - - n-result: 𝑛2 - normalize: '𝑛1(α𝑖0 ↦ π‘˜1)' - - n-result: 𝑛3 - morph: 𝑛2 - -- name: mad - match: '𝑛(𝜏 ↦ 𝑛1)' - e-match: 𝑒0 - n-result: 𝑛2 - when: - not: - absolute: 𝑛1 - premises: - - n-result: 𝑛2 - morph: βŠ₯ - -- name: maad - match: '𝑛(α𝑖 ↦ 𝑛1)' - e-match: 𝑒0 - n-result: 𝑛2 - when: - not: - absolute: 𝑛1 - premises: - - n-result: 𝑛2 - morph: βŠ₯ - -- name: universe - label: \Phi - match: Ξ¦ - e-match: 𝑒0 - n-result: 𝑛2 - when: - not: - eq: - - 𝑒0 - - Ξ¦ - premises: - - n-result: 𝑛1 - normalize: 𝑒0 - - n-result: 𝑛2 - morph: 𝑛1 - -- name: dead - match: βŠ₯ - e-match: 𝑒0 - n-result: βŠ₯ - -- name: xi - match: ΞΎ - e-match: 𝑒0 - n-result: 𝑛1 - premises: - - n-result: 𝑛1 - morph: βŠ₯ - -- name: mg - match: Ξ¦ - e-match: Ξ¦ - n-result: 𝑛1 - premises: - - n-result: 𝑛1 - morph: βŠ₯ diff --git a/resources/morphing/dead.yaml b/resources/morphing/dead.yaml new file mode 100644 --- /dev/null +++ b/resources/morphing/dead.yaml @@ -0,0 +1,7 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: dead +match: βŠ₯ +e-match: 𝑒0 +n-result: βŠ₯ diff --git a/resources/morphing/ma.yaml b/resources/morphing/ma.yaml new file mode 100644 --- /dev/null +++ b/resources/morphing/ma.yaml @@ -0,0 +1,14 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: ma +match: '𝑛0(𝜏0 ↦ π‘˜1)' +e-match: 𝑒0 +n-result: 𝑛3 +premises: + - n-result: 𝑛1 + morph: 𝑛0 + - n-result: 𝑛2 + normalize: '𝑛1(𝜏0 ↦ π‘˜1)' + - n-result: 𝑛3 + morph: 𝑛2 diff --git a/resources/morphing/maa.yaml b/resources/morphing/maa.yaml new file mode 100644 --- /dev/null +++ b/resources/morphing/maa.yaml @@ -0,0 +1,14 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: maa +match: '𝑛0(α𝑖0 ↦ π‘˜1)' +e-match: 𝑒0 +n-result: 𝑛3 +premises: + - n-result: 𝑛1 + morph: 𝑛0 + - n-result: 𝑛2 + normalize: '𝑛1(α𝑖0 ↦ π‘˜1)' + - n-result: 𝑛3 + morph: 𝑛2 diff --git a/resources/morphing/maad.yaml b/resources/morphing/maad.yaml new file mode 100644 --- /dev/null +++ b/resources/morphing/maad.yaml @@ -0,0 +1,13 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: maad +match: '𝑛(α𝑖 ↦ 𝑛1)' +e-match: 𝑒0 +n-result: 𝑛2 +when: + not: + absolute: 𝑛1 +premises: + - n-result: 𝑛2 + morph: βŠ₯ diff --git a/resources/morphing/mad.yaml b/resources/morphing/mad.yaml new file mode 100644 --- /dev/null +++ b/resources/morphing/mad.yaml @@ -0,0 +1,13 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: mad +match: '𝑛(𝜏 ↦ 𝑛1)' +e-match: 𝑒0 +n-result: 𝑛2 +when: + not: + absolute: 𝑛1 +premises: + - n-result: 𝑛2 + morph: βŠ₯ diff --git a/resources/morphing/md.yaml b/resources/morphing/md.yaml new file mode 100644 --- /dev/null +++ b/resources/morphing/md.yaml @@ -0,0 +1,17 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: md +match: '𝑛0.𝜏0' +e-match: 𝑒0 +n-result: 𝑛3 +when: + not: + formation: 𝑛0 +premises: + - n-result: 𝑛1 + morph: 𝑛0 + - n-result: 𝑛2 + normalize: '𝑛1.𝜏0' + - n-result: 𝑛3 + morph: 𝑛2 diff --git a/resources/morphing/mf.yaml b/resources/morphing/mf.yaml new file mode 100644 --- /dev/null +++ b/resources/morphing/mf.yaml @@ -0,0 +1,7 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: mf +match: ⟦𝐡0⟧ +e-match: 𝑒0 +n-result: ⟦𝐡0⟧ diff --git a/resources/morphing/mg.yaml b/resources/morphing/mg.yaml new file mode 100644 --- /dev/null +++ b/resources/morphing/mg.yaml @@ -0,0 +1,10 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: mg +match: Ξ¦ +e-match: Ξ¦ +n-result: 𝑛1 +premises: + - n-result: 𝑛1 + morph: βŠ₯ diff --git a/resources/morphing/ml.yaml b/resources/morphing/ml.yaml new file mode 100644 --- /dev/null +++ b/resources/morphing/ml.yaml @@ -0,0 +1,17 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: ml +label: \lambda +match: '⟦𝐡1, Ξ» ‍ 𝑓0, 𝐡2⟧.𝜏0' +e-match: 𝑒0 +n-result: 𝑛3 +premises: + - n-result: 𝑛1 + evaluate: + - '⟦𝐡1, Ξ» ‍ 𝑓0, 𝐡2⟧' + - 𝑒0 + - n-result: 𝑛2 + normalize: '𝑛1.𝜏0' + - n-result: 𝑛3 + morph: 𝑛2 diff --git a/resources/morphing/mphi.yaml b/resources/morphing/mphi.yaml new file mode 100644 --- /dev/null +++ b/resources/morphing/mphi.yaml @@ -0,0 +1,26 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: mphi +label: \varphi +match: ⟦𝐡0⟧.𝜏0 +e-match: 𝑒0 +n-result: 𝑛2 +when: + and: + - in: + - Ο† + - 𝐡0 + - not: + in: + - 𝜏0 + - 𝐡0 + - not: + in: + - Ξ» + - 𝐡0 +premises: + - n-result: 𝑛1 + normalize: ⟦𝐡0⟧.Ο†.𝜏0 + - n-result: 𝑛2 + morph: 𝑛1 diff --git a/resources/morphing/universe.yaml b/resources/morphing/universe.yaml new file mode 100644 --- /dev/null +++ b/resources/morphing/universe.yaml @@ -0,0 +1,18 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: universe +label: \Phi +match: Ξ¦ +e-match: 𝑒0 +n-result: 𝑛2 +when: + not: + eq: + - 𝑒0 + - Ξ¦ +premises: + - n-result: 𝑛1 + normalize: 𝑒0 + - n-result: 𝑛2 + morph: 𝑛1 diff --git a/resources/morphing/xi.yaml b/resources/morphing/xi.yaml new file mode 100644 --- /dev/null +++ b/resources/morphing/xi.yaml @@ -0,0 +1,10 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: xi +match: ΞΎ +e-match: 𝑒0 +n-result: 𝑛1 +premises: + - n-result: 𝑛1 + morph: βŠ₯ diff --git a/src/Atoms.hs b/src/Atoms.hs --- a/src/Atoms.hs +++ b/src/Atoms.hs @@ -55,7 +55,9 @@ -- question from the formation it already holds for that request, so neither -- side ever re-prints a receiver the other side has in hand (#1165). The -- 'attr' may go deeper than one name: 'ρ.length' is a path down the receiver, --- read left to right, since phino holds the whole of it anyway (#1207). +-- read left to right, since phino holds the whole of it anyway (#1207). It +-- walks applications as well as formations, an argument being as much a +-- binding as a Ο„ inside a formation (#1212). -- -- Whichever way it was asked, an answer says what the node under '𝑛' carries, -- so that no program keeps a πœ‘ reader of its own to tell a datum from a stuck @@ -550,30 +552,39 @@ Nothing -> Left (printf "the receiver of request %d carries no attribute '%s'" req (T.unpack attrName)) Just held -> Right held -- Walk the dotted path of 'attr' down the receiver: every segment but - -- the last has to name a formation to go on into, and the last one is - -- what the question is about. An attribute bound to nothing at all - -- carries nothing to descend into, so a path through a void one names - -- no attribute (#1207). + -- the last has to name a formation or an application to go on into, + -- and the last one is what the question is about. An attribute bound + -- to nothing at all carries nothing to descend into, so a path through + -- a void one names no attribute (#1207). descended :: Expression -> Maybe Held descended form' = foldM deeper (Bound form') (T.splitOn "." attrName) deeper :: Held -> T.Text -> Maybe Held deeper (Bound expr) name = attributeValue name expr deeper Void _ = Nothing + -- An argument of an application binds an attribute the way a Ο„ + -- binding of a formation does, and it is the outer of the two, so it + -- is what the attribute is whatever the formation under it still says + -- about it. A positional argument names nothing, so the walk goes past + -- it into what the application applies to (#1212). attributeValue :: T.Text -> Expression -> Maybe Held attributeValue name (ExFormation bds) = go bds where go :: [Binding] -> Maybe Held go [] = Nothing go (BiTau attr value : rest) - | named attr = Just (Bound value) + | named name attr = Just (Bound value) | otherwise = go rest go (BiVoid attr : rest) - | named attr = Just Void + | named name attr = Just Void | otherwise = go rest go (_ : rest) = go rest - named :: Attribute -> Bool - named attr = T.pack (printAttribute attr) == name + attributeValue name (ExApplication applied (ArTau attr value)) + | named name attr = Just (Bound value) + | otherwise = attributeValue name applied + attributeValue name (ExApplication applied _) = attributeValue name applied attributeValue _ _ = Nothing + named :: T.Text -> Attribute -> Bool + named name attr = T.pack (printAttribute attr) == name -- Reduce the πœ‘-expression the program asks about and say it back under -- '𝑛', with the 'id' the question minted. A program started for the fire -- has nothing to be answered over, since phino closed its stdin behind the diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs --- a/src/CLI/Helpers.hs +++ b/src/CLI/Helpers.hs @@ -17,7 +17,6 @@ import Data.IORef import Data.List (intercalate, nub) import Data.Maybe -import Dataize (DataizeContext, insideUniverse) import Deps (SaveEvalFunc, SaveStepFunc, dontSaveEval, saveEval, saveStep) import Encoding import Files (ensuredFile) @@ -26,6 +25,7 @@ import Lining (LineFormat (SINGLELINE)) import Locator (locatedExpression) import Logger +import Morph (ReduceContext, insideUniverse) import Parser (parseExpressionThrows) import qualified Printer as P import qualified Random as R @@ -104,7 +104,7 @@ -- expression, which the run takes as the universe, and the locator becomes that -- attribute (see 'insideUniverse'). Without the option nothing moves and the -- context is handed back as it came. -aimed :: Maybe String -> Expression -> DataizeContext -> IO (Expression, DataizeContext) +aimed :: Maybe String -> Expression -> ReduceContext -> IO (Expression, ReduceContext) aimed Nothing expr ctx = pure (expr, ctx) aimed (Just src) expr@(ExFormation _) ctx = do target <- parseExpressionThrows src diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -28,6 +28,7 @@ import Logger import Margin (defaultMargin) import Merge (merge) +import Morph import Parser (parseExpressionThrows) import qualified Printer as P import qualified Random as R @@ -167,7 +168,7 @@ ( \record -> do -- The deep walk belongs to 𝕄 alone (the '--deep' of 'morph'), since 𝔻 -- reduces what dataization demands and ends in bytes, so it is off here. - let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial False atoms buildTerm save record + let ctx = ReduceContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial False atoms buildTerm reduction save record (universe, aiming) <- aimed _inside expr ctx dataize universe aiming ) @@ -252,7 +253,7 @@ _evaluations printCtx ( \record -> do - let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial _deep atoms buildTerm save record + let ctx = ReduceContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial _deep atoms buildTerm reduction save record (universe, aiming) <- aimed _inside expr ctx morph universe aiming ) diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -1,113 +1,41 @@ -{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} -{-# OPTIONS_GHC -Wno-unused-record-wildcards #-} -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Dataize (morph, morph', dataize, dataize', insideUniverse, DataizeContext (..), DataizeException (..), Outcome (..), Steps (..), State, emptyState, execBuildTerm) where +-- The Dataization function 𝔻 and what a program asking phino to reduce one of +-- its own terms gets back. Everything 𝔻 shares with the Morphing function 𝕄 β€” +-- the context, the budget, the signals, the premise plumbing β€” lives in +-- 'Morph', which this module imports. +module Dataize (dataize, dataize', reduction, Outcome (..)) where import AST -import Atoms (ReduceFunc, Registry, fireAtom, registeredAtom) -import Builder (buildBytesThrows, buildExpressionThrows, contextualize) -import Control.Exception (Exception, catch, throwIO, try) -import Control.Monad (foldM, when) -import Data.List (find, partition) +import Atoms (ReduceFunc) +import Builder (buildBytesThrows, buildExpressionThrows) +import Control.Exception (throwIO, try) +import Control.Monad (foldM) +import Data.List (find) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE -import Data.Maybe (fromMaybe) -import qualified Data.Text as T -import Deps (BuildTermFunc, BuildTermMethodS, Evaluation (..), SaveEvalFunc, SaveStepFunc, State, Term (..)) -import Locator (locatedExpression, withLocatedExpression) -import Matcher (MetaValue (..), Subst (..), combine, matchExpression', substEmpty, substSingle) -import Must (Must (..)) +import Deps (State) +import Locator (locatedExpression) +import Matcher (Subst, matchExpression') +import Morph (Morphed, ReduceContext (..), ReduceException (..), deeper, emptyState, excluding, execBuildTerm, insideUniverse, leadsTo, morph', normalized, parking, producer, sidePremise, verb) import Random (shuffle) -import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite) +import Rewriter (Rewritten) import Rule (RuleContext (RuleContext), matchExpressionWithRule') import Text.Printf (printf) -import Yaml (ExtraArgument (..), normalizationRules) import qualified Yaml as Y type Dataized = (Bytes, [Rewritten]) -type Dataizable = (Expression, NonEmpty Rewritten) - -type Morphed = Dataizable - --- The initial, empty state used when dataization starts. The 'State' type itself --- lives in 'Deps' next to 'BuildTermMethod'. -emptyState :: State -emptyState = "" - --- How many steps of the 𝕄/𝔻 recursion one branch of a derivation may take --- ('_limit', the '--max-steps' option) and how many the branch reaching this --- point has already taken ('_spent'). 𝕄 and 𝔻 recurse into each other, into the --- premises of their own rules and into the atoms they fire, so a budget local to --- one of those chains is reset by the next nested call and bounds nothing (see --- #1052). This one rides in the context that every such path β€” the spine, the --- side-premises, '_dataize' and '_morph' β€” already carries, so a nested call --- inherits the count of the call that made it. It bounds depth, not total work: --- a premise passes its count down but not back, so siblings each descend from --- the same '_spent'. Bounding every branch is enough to terminate, since a rule --- has finitely many premises. -data Steps = Steps - { _limit :: Int - , _spent :: Int - } - --- The evaluation context carries the configuration plus the step budget spent so --- far. Nothing global is fixed here: the universe (the second argument 'e' of --- 𝕄(n, e, s) and 𝔻(n, e, s)) is a plain expression threaded as an argument to --- 'dataize'', 'morph'' and on to the atoms, and the state 's' is threaded the same --- way (see 'State'). The working expression needed for normalization is taken --- from the head of the step chain, so no separate wrapper type is threaded --- around. -data DataizeContext = DataizeContext - { _locator :: Expression - , _maxDepth :: Int - , _maxCycles :: Int - , _steps :: Steps - , _depthSensitive :: Bool - , _shuffle :: Bool - , _partial :: Bool - , _deep :: Bool - , _atoms :: Registry - , _buildTerm :: BuildTermFunc - , _saveStep :: SaveStepFunc - , _saveEval :: SaveEvalFunc - } - -data DataizeException - = OutOfSteps Int - | -- An atom could not fire: the '--atoms' registry carries no Ξ» function of - -- that name, so there is nothing to run. The name is that of the atom 𝔼 - -- actually failed on, which for a chain of dispatches is the innermost one, - -- since 'ml' reduces a head before the atom above it fires. - Stuck T.Text - | -- A 'Stuck' caught by a frame of the 𝕄/𝔻 spine, together with the - -- derivation that frame had reached (see 'parking'). The head of the chain - -- is the working expression with the stuck application left intact and - -- everything reduced before it already in place: the residual program that - -- '_partial' turns into the 'Residual' outcome. - StuckAt T.Text (NonEmpty Rewritten) - | -- An 'OutOfSteps' caught by a spine frame, carrying that frame's derivation - -- just like 'StuckAt': a term that never reduces is a stuck site too, so - -- '_partial' parks it and hands back the residual instead of failing hard - -- (#1078) - OutOfStepsAt Int (NonEmpty Rewritten) - deriving anyclass (Exception) - -instance Show DataizeException where - show (OutOfSteps limit) = - printf "Dataization did not finish before reaching the limit of steps: --max-steps=%d" limit - show (OutOfStepsAt limit _) = show (OutOfSteps limit) - show (Stuck func) = printf "Atom '%s' does not exist" (T.unpack func) - show (StuckAt func _) = show (Stuck func) +-- What 𝔻 is handed: a term plus the derivation that reached it, the same pair +-- 𝕄 works on (see 'Morphed'). +type Dataizable = Morphed -- What a run of 𝔻 ends with: the bytes it reached or, under '_partial', the -- residual program: what the known inputs decided is computed, the stuck atom @@ -117,337 +45,6 @@ | Residual Expression deriving stock (Eq, Show) --- Charge one step of the 𝕄/𝔻 recursion to the budget, refusing to descend once --- it is gone. '--max-cycles' and '--max-depth' bound only the normalization run --- inside a single step, so before this the recursion itself was unbounded and a --- term that never reduces to bytes kept 𝕄 and 𝔻 calling each other forever --- (#1052). Rewriting hands back whatever it has reached when it runs out of --- cycles; 𝔻 has no partial answer to give, so an exhausted budget always throws, --- with or without '--depth-sensitive'. -deeper :: DataizeContext -> IO DataizeContext -deeper ctx@DataizeContext{_steps = Steps limit spent} - | spent >= limit = throwIO (OutOfSteps limit) - | otherwise = pure ctx{_steps = Steps limit (spent + 1)} - --- Split the Ξ» binding off a formation for the LAMBDA morphing rule: the name of --- the atom to fire and the formation it fires against, the Ξ» binding removed β€” --- the two things 𝔼 reports besides the result. A formation with no Ξ» binding, --- or with more than one, has nothing to fire. -lambda :: [Binding] -> Maybe (T.Text, Expression) -lambda bds = case partition isLambda bds of - ([BiLambda (Function func)], rest) -> Just (func, ExFormation rest) - _ -> Nothing - where - isLambda :: Binding -> Bool - isLambda (BiLambda _) = True - isLambda _ = False - --- The same as 'lambda', but only for a formation that is saturated: one with --- every binding of it filled (see 'filled'). A void is an argument the program --- has not given yet, so such a formation is a method waiting to be applied --- rather than an application waiting to be computed, and firing it would hand --- the atom a βˆ… where it expects a value. 𝔻 needs no such guard, since it --- fires only what dataization demands and nothing demands a method; the deep --- walk meets every one a program declares β€” the method table of the object --- model above all β€” so it asks first (see 'deepened'). -saturated :: [Binding] -> Maybe (T.Text, Expression) -saturated bds = case lambda bds of - Just (func, ExFormation rest) | all filled rest -> Just (func, ExFormation rest) - _ -> Nothing - --- Whether a binding hands the formation something to work with. A void does --- not: it names an argument the program has still to supply. Neither does βŠ₯: --- the deep walk reduces a body in the scope of the formation around it, and a --- formation standing unapplied still holds ρ ↦ βˆ…, so a ΞΎ.ρ in that body comes --- back as βŠ₯ rather than as the object the next dispatch supplies (#1196). -filled :: Binding -> Bool -filled (BiVoid _) = False -filled (BiTau _ ExTermination) = False -filled _ = True - --- Run one frame of the 𝕄/𝔻 spine, attaching its derivation to a stuck atom or --- an exhausted budget escaping it. 'Stuck' is raised deep inside an atom, which --- knows nothing about the chain, so the innermost spine frame it reaches is the --- one to record where the derivation stopped: the head of that frame's chain is --- the working expression with the stuck application intact and everything --- reduced before it already in place. The same holds for 'OutOfSteps': a term --- cycling through the universe is no more a failure of the chain than a missing --- atom is, and under '_partial' it deserves the same parked residual (#1078). --- Outer frames see the '…At' signals and let them pass, since their chains are --- prefixes of that one; a side-computation running on a chain of its own strips --- the chain off again (see 'unparked') before the signal reaches the spine. -parking :: NonEmpty Rewritten -> IO a -> IO a -parking seq action = action `catch` rethrow - where - rethrow :: DataizeException -> IO a - rethrow (Stuck func) = throwIO (StuckAt func seq) - rethrow (OutOfSteps limit) = throwIO (OutOfStepsAt limit seq) - rethrow failure = throwIO failure - --- Strip the derivation off a stuck atom escaping a side-computation that ran --- on a chain of its own β€” an atom dataizing its input through '_dataize', or a --- 'morph' premise through '_morph'. That chain is not the spine's, so it is --- dropped and the spine frame around the side-computation attaches its own --- (see 'parking'). -unparked :: IO a -> IO a -unparked action = action `catch` rethrow - where - rethrow :: DataizeException -> IO a - rethrow (StuckAt func _) = throwIO (Stuck func) - rethrow (OutOfStepsAt limit _) = throwIO (OutOfSteps limit) - rethrow failure = throwIO failure - --- The Morphing function 𝕄 maps normal forms to formations. It is ternary, --- 𝕄(n, e, s): besides the term 'n' it takes the universe 'e' ('univ') β€” a plain --- expression β€” and the mutable state 's', returning the morphed term together --- with the new state. The universe is matched against the rule's 'e-match' --- pattern (usually the '𝑒' meta, which binds 'e' so the 'universe' rule substitutes --- it, but a rule may pin it to a literal such as 'mg' matching Ξ¦). Its rules --- come from 'morphing.yaml': the first matching rule's premises are evaluated and --- its conclusion 'nresult' is built, always forwarding the same universe. The --- clauses are disjoint (see #856, #860), so their declaration order must not be --- load-bearing; when '_shuffle' is on (the '--shuffle' flag) the rules are --- shuffled before the 'firstMatch' walk to exercise that invariant β€” mirroring --- normalization's "apply until they stop matching". A genuinely order-independent --- step stays deterministic; a hidden overlap surfaces as a nondeterministic --- failure rather than staying silently green. --- The 'morph' premise that produces the conclusion is the spine: when --- its argument comes from a 'normalize' premise, the rewriter runs over that --- argument and its individual steps (alpha, copy, dot, …) are spliced into the --- chain before morphing continues. Every other premise is a side-computation --- evaluated in isolation by 'sidePremise', its own steps discarded. -morph' :: Morphed -> Expression -> State -> DataizeContext -> IO (Morphed, State) -morph' (expr, seq) univ state caller = do - ctx <- deeper caller - parking seq $ do - rules <- if ctx._shuffle then shuffle Y.morphingRules else pure Y.morphingRules - matched <- firstMatch ctx rules - case matched of - Just (rule, subst) -> reduce ctx rule subst - Nothing -> throwIO (userError "no morphing rule matched") - where - firstMatch :: DataizeContext -> [Y.MorphRule] -> IO (Maybe (Y.MorphRule, Subst)) - firstMatch _ [] = pure Nothing - firstMatch ctx (rule : rest) = do - substs <- matchExpressionWithRule' (matchExpression' rule.ematch univ) expr (asRule rule) (RuleContext (execBuildTerm univ ctx)) - case substs of - (subst : _) -> pure (Just (rule, subst)) - [] -> firstMatch ctx rest - -- Match the conclusion term and check the guard; premises are no longer the - -- matcher's business, so 'where'/'having' stay empty and the guard lives in - -- 'when'. Every morphing guard reads only meta-variables bound by 'match' - -- and 'e-match', so it holds before any premise runs. - asRule :: Y.MorphRule -> Y.Rule - asRule rule = Y.Rule rule.name Nothing Nothing rule.match ExRoot rule.when Nothing Nothing - -- Evaluate the rule's premises and build its conclusion. A literal - -- conclusion is terminal. Otherwise the conclusion meta is produced by a - -- trailing 'morph' premise (the spine); if that premise's argument is itself - -- bound by a 'normalize' premise, the normalization joins the spine and its - -- steps splice in before morphing continues. - reduce :: DataizeContext -> Y.MorphRule -> Subst -> IO (Morphed, State) - reduce ctx rule subst = case producer rule.nresult rule.premises of - Nothing -> do - (final, state') <- sides ctx rule.premises subst - built <- buildExpressionThrows rule.nresult final - seq' <- leadsTo seq rule.name built ctx - pure ((built, seq'), state') - Just concl@(Y.Premise _ (Y.OpMorph arg)) -> case producer arg rule.premises of - Just normal@(Y.Premise _ (Y.OpNormalize inner)) -> do - (final, state') <- sides ctx (rule.premises `excluding` [concl, normal]) subst - built <- buildExpressionThrows inner final - labelled <- leadsTo seq rule.name built ctx - (normal', seq') <- normalized built labelled ctx - morph' (normal', seq') univ state' ctx - _ -> do - (final, state') <- sides ctx (rule.premises `excluding` [concl]) subst - built <- buildExpressionThrows arg final - seq' <- leadsTo seq rule.name built ctx - morph' (built, seq') univ state' ctx - Just _ -> throwIO (userError (printf "morphing rule '%s' must conclude with a 'morph' premise" rule.name)) - sides :: DataizeContext -> [Y.Premise] -> Subst -> IO (Subst, State) - sides ctx premises subst = foldM (sidePremise univ ctx) (subst, state) premises - --- Morph the expression located at '_locator' β€” 𝕄 asked on its own, the way --- 'dataize' asks 𝔻. The whole input expression is itself the universe Ξ¦ (the 'e' --- argument) threaded through 𝕄, so it is passed both as the located target and --- as the universe; the default locator Q therefore morphs the top formation, --- which 'mf' hands back unchanged, and '_locator' is how one aims 𝕄 at a --- subterm. Unlike 𝔻, 𝕄 is total: it stops at the first formation it reaches --- ('mf') and never demands bytes, and where no formation is reachable it answers --- with the terminator βŠ₯ ('dead', 'xi', 'mg', 'mad', 'maad') rather than failing. --- Only the atoms 'ml' fires can still get stuck, and '_partial' parks them just --- as it does under 𝔻: the answer is then the residual subterm the spine had --- reached, taken from '_locator' of its working expression. Stopping at the --- first formation leaves everything that formation holds as it was written, --- which is what '_deep' walks into before the answer is handed back (see --- 'deepened'). -morph :: Expression -> DataizeContext -> IO (Expression, [Rewritten]) -morph universe ctx@DataizeContext{..} = do - expr <- locatedExpression _locator universe - result <- try (morph' (expr, (universe, Nothing) :| []) universe emptyState ctx) - case result of - Right ((morphed, seq), state) -> walked morphed seq state - Left (StuckAt _ seq) | _partial -> do - residue <- locatedExpression _locator (fst (NE.head seq)) - walked residue seq emptyState - Left (OutOfStepsAt _ seq) | _partial -> do - residue <- locatedExpression _locator (fst (NE.head seq)) - walked residue seq emptyState - Left failure -> throwIO (failure :: DataizeException) - where - -- The answer 𝕄 reached, walked by '_deep' before it is handed back (see - -- 'deepened'), and the chain that led to both. The walk joins the chain as - -- one step named 'deep', so '--sequence' ends on the term the command - -- prints. Morphing starts from the empty state and the state the walk ends - -- on goes the way 𝕄's own goes: no caller consumes it yet. - walked :: Expression -> NonEmpty Rewritten -> State -> IO (Expression, [Rewritten]) - walked morphed seq state - | not _deep = pure (morphed, reverse (NE.toList seq)) - | otherwise = do - (deep, _) <- deepened morphed universe state ctx - seq' <- leadsTo seq "deep" deep ctx - pure (deep, reverse (NE.toList seq')) - --- Walk what 𝕄 answered with, entering everything it left as it was written β€” --- the mechanism behind '--deep' ('_deep'). 𝕄 navigates a term to the first --- formation it reaches and 'mf' hands that formation back with its bindings --- untouched, since firing a bare Ξ» is 𝔻's business; 𝔻 in turn follows the one --- path dataization demands and ends in bytes. A part of a program that nothing --- demands β€” the argument of an atom that cannot fire, for one β€” is therefore --- reduced by neither, and the object structure is lost to the one that does --- reduce it (#1124). This walk demands nothing either. It asks 𝕄 about every --- sub-expression and, where 𝕄 lands on a formation whose Ξ» the registry --- serves, fires it and asks 𝕄 about the answer again (see 'fired'). A --- sub-expression on whose way an atom fired is replaced by the answer of the --- last firing; where none fired it stays as it was written and only its own --- parts are walked, so the calls the registry does not serve keep their names --- and what comes back is still the same program, reduced as far as the --- registry allows. Every entry is charged to the '--max-steps' budget, which --- is what bounds the walk. -deepened :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State) -deepened expr univ = go Nothing ExXi expr - where - -- A term as it was written, together with what its free ΞΎ stands for: the - -- formation the walk entered it from, without the binding it came from, - -- exactly the context the 'dot' rule hands a dispatched body. At the top - -- there is no such formation, so ΞΎ stands for itself and contextualization - -- leaves the term alone. - go :: Maybe Attribute -> Expression -> Expression -> State -> DataizeContext -> IO (Expression, State) - go dispatched context term state' caller = do - ctx' <- deeper caller - (walked, walkedState) <- parts context term state' caller - answer <- fired dispatched (contextualize walked context) univ walkedState ctx' - maybe (pure (walked, walkedState)) pure answer - -- The parts of a term nothing fired on, walked one by one and put back - -- where they were, so the term keeps the shape it was written in. - parts :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State) - parts _ (ExFormation bds) state' caller = do - (entered, state'') <- bindings bds bds state' caller - pure (ExFormation entered, state'') - parts context (ExDispatch target attr) state' caller = do - (entered, state'') <- go (Just attr) context target state' caller - pure (ExDispatch entered attr, state'') - parts context (ExApplication target arg) state' caller = do - (entered, state'') <- go Nothing context target state' caller - (applied, state''') <- argument context arg state'' caller - pure (ExApplication entered applied, state''') - parts _ term state' _ = pure (term, state') - -- Walk the bindings of a formation left to right, threading the state - -- through them. Only what the formation itself holds is entered: ρ names - -- the object around it rather than one inside it, and a void, Ξ” or Ξ» - -- binding carries no term to walk at all. - bindings :: [Binding] -> [Binding] -> State -> DataizeContext -> IO ([Binding], State) - bindings _ [] state' _ = pure ([], state') - bindings whole (BiTau attr body : rest) state' caller - | attr /= AtRho = do - (entered, state'') <- go Nothing (scope attr whole) body state' caller - (others, state''') <- bindings whole rest state'' caller - pure (BiTau attr entered : others, state''') - bindings whole (bd : rest) state' caller = do - (others, state'') <- bindings whole rest state' caller - pure (bd : others, state'') - -- The context a binding's body is entered in: the formation without that - -- binding, the very context 'dot' contextualizes a dispatched body in, so - -- a body reaching back at itself through ΞΎ collapses instead of looping. - scope :: Attribute -> [Binding] -> Expression - scope attr bds = ExFormation (filter (not . named) bds) - where - named :: Binding -> Bool - named (BiTau attr' _) = attr' == attr - named _ = False - -- Both sides of an application stand in the same context: the term it - -- applies is walked by the caller and the argument it binds is walked here. - argument :: Expression -> Argument -> State -> DataizeContext -> IO (Argument, State) - argument context (ArTau attr arg) state' caller = do - (entered, state'') <- go Nothing context arg state' caller - pure (ArTau attr entered, state'') - argument context (ArAlpha alpha arg) state' caller = do - (entered, state'') <- go Nothing context arg state' caller - pure (ArAlpha alpha entered, state'') - --- Ask 𝕄 about a term and fire the Ξ» of the formation it reaches, as long as --- the registry serves it, asking 𝕄 about every answer again: what comes back --- is the answer of the last firing, or nothing at all where no atom fired. This --- is the firing 'ml' makes without the dispatch that makes 'ml' make it β€” the --- one 𝕄 leaves to 𝔻 β€” except in what it hands back: the atom's raw answer, not --- the normal form 𝔼 makes of it, since the deep walk stands that answer back --- into the program, where a normal form would spell the whole object out in --- place of the name the program called it by. A Ξ» the registry does not carry --- is left alone rather than fired and got stuck on, so what phino cannot --- compute stays as it was written with or without '_partial'; an atom that --- cannot fire deeper on the spine still fails the run, exactly as it does --- under 𝕄 alone, and '_partial' parks it. A formation still waiting for its --- arguments is left alone too (see 'saturated'). A term standing as the target --- of a dispatch is where 'ml' has its say: the Ξ» is fired only where the --- dispatched attribute is none of the formation's own (see 'demanded'). -fired :: Maybe Attribute -> Expression -> Expression -> State -> DataizeContext -> IO (Maybe (Expression, State)) -fired dispatched term univ state caller = do - ctx <- deeper caller - morphed <- try (reduced ctx) - case morphed of - Right (ExFormation bds, state') - | demanded bds -> maybe (pure Nothing) (evaluated ctx state') (saturated bds) - Right _ -> pure Nothing - Left failure -> parked failure - where - -- Whether the dispatch the term stands under demands the Ξ» of the formation - -- 𝕄 reached. 'ml' fires that Ξ» only where the dispatched attribute is none - -- of the formation's own, since 'dot' resolves the dispatch before 'ml' is - -- ever reached, and a walk firing it first answers a formation the dispatch - -- no longer fits (#1187). A term standing anywhere else is demanded by - -- nothing and the walk fires what 'mf' left bare, as it always has. - demanded :: [Binding] -> Bool - demanded bds = not (any bound bds) - where - bound :: Binding -> Bool - bound (BiTau attr _) = Just attr == dispatched - bound _ = False - -- 𝕄 takes normal forms only and a term taken from the program as it was - -- written is not necessarily one, so it is normalized against the universe - -- first, exactly as '--inside' normalizes what it is handed. Both chains - -- are dropped: the walk is not the spine and reports one step of its own - -- (see 'morph'), so a stuck atom leaves without a derivation ('unparked'). - reduced :: DataizeContext -> IO (Expression, State) - reduced ctx = unparked $ do - (normal, _) <- normalized term ((univ, Nothing) :| []) ctx - ((morphed, _), state') <- morph' (normal, (univ, Nothing) :| []) univ state ctx - pure (morphed, state') - -- Fire the Ξ» of the formation 𝕄 reached and go on from its answer, keeping - -- the answer of the last firing. The firing is reported to '_saveEval' like - -- every other one, with the term the caller is given, so the protocol and - -- the program agree on what the atom answered. - evaluated :: DataizeContext -> State -> (T.Text, Expression) -> IO (Maybe (Expression, State)) - evaluated ctx state' (func, self) = case registeredAtom ctx._atoms func of - Nothing -> pure Nothing - Just registered -> do - answer <- fireAtom func registered self univ (reduction univ ctx) - ctx._saveEval (Evaluation func self (Just answer)) - again <- fired dispatched answer univ state' ctx - pure (Just (fromMaybe (answer, state') again)) - parked :: DataizeException -> IO (Maybe a) - parked (Stuck _) | caller._partial = pure Nothing - parked failure = throwIO failure - -- Dataize the expression located at '_locator'. The whole input expression is -- itself the universe Q (the 'e' argument) threaded through 𝔻 and 𝕄, so it is -- passed both as the located target and as the universe. An atom that cannot @@ -455,8 +52,8 @@ -- evaluation, and the run ends on the residual program the spine had reached -- (see 'StuckAt'), with the stuck application parked in it as a normal-form -- subterm, and the chain of steps that led there. -dataize :: Expression -> DataizeContext -> IO (Outcome, [Rewritten]) -dataize universe ctx@DataizeContext{..} = do +dataize :: Expression -> ReduceContext -> IO (Outcome, [Rewritten]) +dataize universe ctx@ReduceContext{..} = do expr <- locatedExpression _locator universe -- Dataization starts from the empty state; the final state is not yet -- consumed by any caller, so it is discarded here. @@ -465,12 +62,12 @@ Right ((bytes, seq), _state) -> pure (Dataized bytes, reverse seq) Left (StuckAt _ seq) | _partial -> pure (Residual (fst (NE.head seq)), reverse (NE.toList seq)) Left (OutOfStepsAt _ seq) | _partial -> pure (Residual (fst (NE.head seq)), reverse (NE.toList seq)) - Left failure -> throwIO (failure :: DataizeException) + Left failure -> throwIO (failure :: ReduceException) -- The Dataization function 𝔻 retrieves bytes from an expression. It is partial -- and ternary, 𝔻(n, e, s): besides the term 'n' it takes the universe 'e' ('univ'), -- which it forwards to 𝕄, and the mutable state 's', returning the bytes together --- with the new state. Its rules come from 'dataization.yaml': 'delta' yields the +-- with the new state. Its rules come from 'resources/dataization': 'delta' yields the -- asset bytes and 'none' (a formation with no Ξ”/Ξ»/Ο†) has nothing to dataize, so -- it dataizes βŠ₯. The terminator βŠ₯ signals an error and lies outside 𝔻's domain, -- so it matches no clause (there is no 'end' rule mapping it to empty bytes) and @@ -488,7 +85,7 @@ -- The conclusion bytes 'dresult' are produced by a trailing 'dataize' premise; -- when its argument is bound by a 'morph' or 'normalize' premise, that step -- joins the spine, otherwise the premise is an isolated side-computation. -dataize' :: Dataizable -> Expression -> State -> DataizeContext -> IO (Dataized, State) +dataize' :: Dataizable -> Expression -> State -> ReduceContext -> IO (Dataized, State) dataize' (expr, seq) univ state caller = do ctx <- deeper caller parking seq $ do @@ -505,7 +102,7 @@ unmatched :: Expression -> String unmatched ExTermination = "dataization reached the terminator βŠ₯, which signals an error and cannot be dataized" unmatched _ = "no dataization rule matched" - firstMatch :: DataizeContext -> [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst)) + firstMatch :: ReduceContext -> [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst)) firstMatch _ [] = pure Nothing firstMatch ctx (rule : rest) = do substs <- matchExpressionWithRule' (matchExpression' rule.ematch univ) expr (asRule rule) (RuleContext (execBuildTerm univ ctx)) @@ -514,7 +111,7 @@ [] -> firstMatch ctx rest asRule :: Y.DataizeRule -> Y.Rule asRule rule = Y.Rule rule.name Nothing Nothing rule.match ExRoot rule.when Nothing Nothing - reduce :: DataizeContext -> Y.DataizeRule -> Subst -> IO (Dataized, State) + reduce :: ReduceContext -> Y.DataizeRule -> Subst -> IO (Dataized, State) reduce ctx rule subst = case bytesProducer rule.dresult rule.premises of Nothing -> do (final, state') <- sides ctx rule.premises subst @@ -552,7 +149,7 @@ seq' <- leadsTo seq (labelOr (verb concl.operation) side) built ctx dataize' (built, seq') univ state' ctx Just _ -> throwIO (userError (printf "dataization rule '%s' must conclude with a 'dataize' premise" rule.name)) - sides :: DataizeContext -> [Y.Premise] -> Subst -> IO (Subst, State) + sides :: ReduceContext -> [Y.Premise] -> Subst -> IO (Subst, State) sides ctx premises subst = foldM (sidePremise univ ctx) (subst, state) premises -- A spliced dataization step is labelled by its first side-computation β€” -- 'box' by its 'contextualize', 'fire' by its 'evaluate'; with none it is blank. @@ -565,118 +162,12 @@ labelOr _ premises@(_ : _) = labelOf premises labelOr fallback [] = fallback --- The premise binding the given expression meta, if any. The conclusion of a --- morphing rule and the argument of a continuation premise are looked up here to --- find the premise that produces them. -producer :: Expression -> [Y.Premise] -> Maybe Y.Premise -producer (ExMeta name) = find (\premise -> premise.result == name) -producer _ = const Nothing - -- The premise binding the given bytes meta, if any β€” the dataization analogue of -- 'producer' for a rule's bytes conclusion. bytesProducer :: Bytes -> [Y.Premise] -> Maybe Y.Premise bytesProducer (BtMeta name) = find (\premise -> premise.result == name) bytesProducer _ = const Nothing --- The premises whose result meta is not bound by any of the given ones β€” the --- side-computations left once the spine premises are removed. -excluding :: [Y.Premise] -> [Y.Premise] -> [Y.Premise] -excluding premises removed = filter (\premise -> premise.result `notElem` map (.result) removed) premises - --- Evaluate one side-computation premise β€” a 'morph', 'evaluate' or 'contextualize' --- of an earlier term β€” in isolation, binding its result meta. These never splice --- steps into the trace: 'morph' and 'evaluate' reduce on a fresh chain and discard --- it, 'contextualize' is pure. The state is threaded through: 'evaluate' (the --- 𝔼 of the 'ml' and 'fire' rules) takes the incoming state 𝑠1 and yields a --- new one 𝑠2, 'morph' propagates whatever its sub-reduction produced, and every --- other operation leaves the state untouched. -sidePremise :: Expression -> DataizeContext -> (Subst, State) -> Y.Premise -> IO (Subst, State) -sidePremise univ ctx (subst, state) premise = do - (term, state') <- runOperation - case combine (substSingle premise.result (metaValue term)) subst of - Just subst' -> pure (subst', state') - Nothing -> throwIO (userError (printf "premise meta '%s' clashes with an existing binding" (T.unpack premise.result))) - where - -- The 𝔼 ('evaluate') and 𝕄 ('morph') operations can change the state, so they - -- go through their state-aware builders; every other operation is stateless - -- and the incoming state is returned unchanged. - runOperation :: IO (Term, State) - runOperation = case premise.operation of - Y.OpEvaluate expr universe -> _evaluate ctx state [ArgExpression expr, ArgExpression universe] subst - Y.OpMorph expr -> _morph univ ctx state [ArgExpression expr] subst - operation -> do - term <- execBuildTerm univ ctx (verb operation) (verbArgs operation) subst - pure (term, state) - metaValue :: Term -> MetaValue - metaValue (TeExpression value) = MvExpression value - metaValue (TeAttribute value) = MvAttribute value - metaValue (TeBytes value) = MvBytes value - metaValue (TeBindings value) = MvBindings value - --- The build-term function name backing a premise operation. -verb :: Y.Operation -> String -verb (Y.OpMorph _) = "morph" -verb (Y.OpNormalize _) = "normalize" -verb (Y.OpEvaluate _ _) = "evaluate" -verb (Y.OpContextualize _ _) = "contextualize" -verb (Y.OpDataize _) = "dataize" - --- The build-term arguments backing a premise operation. -verbArgs :: Y.Operation -> [ExtraArgument] -verbArgs (Y.OpMorph expr) = [ArgExpression expr] -verbArgs (Y.OpNormalize expr) = [ArgExpression expr] -verbArgs (Y.OpEvaluate expr universe) = [ArgExpression expr, ArgExpression universe] -verbArgs (Y.OpContextualize expr context) = [ArgExpression expr, ArgExpression context] -verbArgs (Y.OpDataize expr) = [ArgExpression expr] - -leadsTo :: NonEmpty Rewritten -> String -> Expression -> DataizeContext -> IO (NonEmpty Rewritten) -leadsTo ((current, _) :| rest) rule expr DataizeContext{..} = do - updated <- withLocatedExpression _locator expr current - pure ((updated, Nothing) :| (current, Just rule) : rest) - --- Reduce 'expr' to its normal form through the normalization rewriter, embedding --- it at '_locator' into the working expression taken from the head of the step --- chain so the rewriter sees the surrounding context. Splices the individual --- steps (alpha, copy, dot, …) into the chain and returns the normalized --- expression together with the extended sequence. -normalized :: Expression -> NonEmpty Rewritten -> DataizeContext -> IO (Expression, NonEmpty Rewritten) -normalized expr seq ctx@DataizeContext{..} = do - whole <- withLocatedExpression _locator expr (fst (NE.head seq)) - (rewrittens, _) <- rewrite whole normalizationRules (rewriteContext ctx) - let (rw :| rws) = NE.reverse rewrittens - seq' = rw :| rws <> NE.tail seq - expr' <- locatedExpression _locator (fst rw) - pure (expr', seq') - where - -- Switch the dataization context to a rewriting context for normalization, - -- disabling the must-checker and breakpoints. - rewriteContext :: DataizeContext -> RewriteContext - rewriteContext DataizeContext{..} = - RewriteContext _locator _maxDepth _maxCycles _depthSensitive _buildTerm MtDisabled Nothing _saveStep - --- Bind 'expr' to a synthetic attribute of the universe and reduce it to a --- normal form there, handing back the extended universe together with the --- locator that aims at the binding. This is the trick phino has always played --- to reduce a sub-expression that is not part of the program β€” an atom's --- operand, while the atoms still lived in the binary β€” and it is now the --- contract of the '--inside' option, so an atom script asking phino to reduce --- a part of the formation it was given does not have to splice it into the text --- of the universe by hand. 𝔻 and 𝕄 accept normal forms only and an expression --- handed in from outside is not necessarily one (a dispatch off a formation, --- '⟦ x ↦ 6, ρ ↦ 5 ⟧.x', is not), so it is normalized against the extended --- universe before either judgment sees it. The context comes back aimed at that --- binding, so the caller hands the extended universe and the context it got --- straight to 'dataize' or 'morph'. -insideUniverse :: Expression -> Expression -> DataizeContext -> IO (Expression, DataizeContext) -insideUniverse expr univ ctx@DataizeContext{_buildTerm = buildTerm} = case univ of - ExFormation bds -> do - (TeAttribute attr) <- buildTerm "random-tau" [] substEmpty - let aiming = ctx{_locator = ExDispatch ExRoot attr} - synthetic = ExFormation (BiTau attr expr : bds) - (normal, _) <- normalized expr ((synthetic, Nothing) :| []) aiming - pure (ExFormation (BiTau attr normal : bds), aiming) - _ -> throwIO (userError "Can't reduce an expression inside a universe which is not a formation") - -- What phino answers a program that asks it to reduce a πœ‘-expression (see -- 'ReduceFunc' in 'Atoms'): the expression is bound to a synthetic attribute -- of the universe and dataized there, exactly the way the '--inside' option @@ -692,7 +183,7 @@ -- no way to ask: it had to splice the operand into the text of the universe -- and run a phino of its own on it (see #1160). The context is the one the -- fire descended with, so the step budget of the run bounds the nesting. -reduction :: Expression -> DataizeContext -> ReduceFunc +reduction :: Expression -> ReduceContext -> ReduceFunc reduction univ ctx expr = do (universe, aiming) <- insideUniverse expr univ ctx (outcome, _) <- dataize universe aiming @@ -701,81 +192,3 @@ reduced :: Expression -> Outcome -> IO Expression reduced _ (Dataized bytes) = pure (ExFormation [BiDelta bytes]) reduced locator (Residual residue) = locatedExpression locator residue - --- phino implements no Ξ» function of its own. Which atoms exist is a property of --- the object model being dataized, not of the calculus, so they come from the --- '--atoms' registry and run as external scripts (see 'Atoms'). A name the --- registry does not carry has no Ξ» function to fire at all, and 𝔼 gets stuck on --- it β€” the one behaviour left here. The script is handed the formation 'self' --- (its Ξ» binding already removed, so it may dispatch on it) and the universe --- 'univ'; the state 𝑠 is not part of that contract yet, so it is threaded --- through untouched. -atom :: T.Text -> Expression -> Expression -> State -> DataizeContext -> IO (Expression, State) -atom func self univ state ctx = case registeredAtom ctx._atoms func of - Nothing -> throwIO (Stuck func) - Just registered -> do - raw <- fireAtom func registered self univ (reduction univ ctx) - pure (raw, state) - --- Augment the injected, context-free term builder with the dataization and --- morphing operations that need the universe: 'evaluate' applies an atom and --- 'morph' morphs a sub-expression. 𝔼 ('evaluate') takes the universe as an --- explicit second expression argument, while 𝕄 ('morph') is handed the threaded --- 'univ'. Every other function is delegated unchanged. This is the matcher's --- condition path (guards in 'when'/'having'), which has no state to thread, so 𝔼 --- and 𝕄 run here on a fresh, empty state whose result is discarded; the --- state-threading callers in 'sidePremise' use '_evaluate' and '_morph' directly. -execBuildTerm :: Expression -> DataizeContext -> BuildTermFunc -execBuildTerm _ ctx "evaluate" = \args subst -> fst <$> _evaluate ctx emptyState args subst -execBuildTerm univ ctx "morph" = \args subst -> fst <$> _morph univ ctx emptyState args subst -execBuildTerm _ ctx func = _buildTerm ctx func - --- The Evaluation function 𝔼(b, e, s): it fires the Ξ» atom of a formation 'b' --- against the global universe 'e', under the incoming state 𝑠, normalizes the --- atom's raw result 𝒩(e₁) = n, and returns that normal form together with the --- new state. Normalizing here makes 𝔼's codomain 𝓝 (as its type demands), so --- callers ('fire', 'ml') need no follow-up 'normalize' premise. The universe is --- passed explicitly as the second argument (rather than threaded behind the --- scenes), matching how the morphing 𝕄 and dataization 𝔻 functions carry it. --- Every firing is reported to '_saveEval', which the '--evaluations' option --- turns into one record per line. The reported result is the normal form 𝔼 --- returns, never the atom's raw answer, so the protocol and the caller see the --- same term. Firings are reported in the order they complete, so the atom of a --- head reduced by 'ml' is reported before the one dispatched on its result. A --- firing that gets stuck is reported too, with no result, when the run is a --- partial evaluation rather than a failure ('_partial'): the site is what the --- caller wants to learn then. The report is made before the signal goes on to --- the spine, where 'parking' attaches the derivation to it. -_evaluate :: DataizeContext -> State -> BuildTermMethodS -_evaluate ctx state [ArgExpression expr, ArgExpression universe] subst = do - form <- buildExpressionThrows expr subst - univ <- buildExpressionThrows universe subst - case form of - ExFormation bds -> case lambda bds of - Just (func, args) -> do - (raw, state') <- atom func args univ state ctx `catch` parked func args - (normal, _) <- normalized raw ((univ, Nothing) :| []) ctx - ctx._saveEval (Evaluation func args (Just normal)) - pure (TeExpression normal, state') - Nothing -> throwIO (userError "Function evaluate() expects a formation with a Ξ» binding") - _ -> throwIO (userError "Function evaluate() expects a formation") - where - parked :: T.Text -> Expression -> DataizeException -> IO a - parked func args failure@(Stuck _) = do - when ctx._partial (ctx._saveEval (Evaluation func args Nothing)) - throwIO failure - parked _ _ failure = throwIO failure -_evaluate _ _ _ _ = throwIO (userError "Function evaluate() requires exactly 2 expression arguments") - --- The Morphing function 𝕄 exposed as a build-term function so a rule can morph --- a sub-expression in its 'where' (the 'md' and 'ma' rules morph --- the head before re-attaching it). The step chain is discarded: the producing --- rule splices the surrounding normalization steps itself, and a stuck atom met --- on the way leaves without it (see 'unparked'). The state is threaded through --- and the new state returned alongside the morphed term. -_morph :: Expression -> DataizeContext -> State -> BuildTermMethodS -_morph univ ctx state [ArgExpression expr] subst = unparked $ do - built <- buildExpressionThrows expr subst - ((morphed, _), state') <- morph' (built, (univ, Nothing) :| []) univ state ctx - pure (TeExpression morphed, state') -_morph _ _ _ _ _ = throwIO (userError "Function morph() requires exactly 1 expression argument") diff --git a/src/Deps.hs b/src/Deps.hs --- a/src/Deps.hs +++ b/src/Deps.hs @@ -4,7 +4,7 @@ -- The main goal of this module is breaking cyclic dependency: -- Dataize -> Functions -> Rewriter -> Dataize -- Here we provide custom type BuildTermFunc and add it to --- RewriteContext and DataizeContext. Now Dataize and Rewrite depends +-- RewriteContext and ReduceContext. Now Dataize and Rewrite depends -- only on Term module. This allows us to use Rewriter and Dataize in -- Functions module because Rewriter does not depend on Functions anymore. module Deps where diff --git a/src/Morph.hs b/src/Morph.hs new file mode 100644 --- /dev/null +++ b/src/Morph.hs @@ -0,0 +1,638 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -Wno-name-shadowing #-} +{-# OPTIONS_GHC -Wno-unused-record-wildcards #-} + +-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +-- SPDX-License-Identifier: MIT + +-- The Morphing function 𝕄 and the machinery every reduction of the calculus is +-- threaded with: the context, the step budget, the signals a stuck run raises +-- and the plumbing that reads a rule's premises. 𝔻 lives in 'Dataize', which +-- imports this module; the one edge pointing back β€” an atom asking phino to +-- reduce an operand, which is a dataization β€” is injected as '_reduce' rather +-- than imported (see 'ReductionFunc'). +module Morph (ReduceContext (..), ReduceException (..), ReductionFunc, Morphed, Steps (..), deeper, emptyState, excluding, execBuildTerm, insideUniverse, leadsTo, morph, morph', normalized, parking, producer, sidePremise, verb) where + +import AST +import Atoms (ReduceFunc, Registry, fireAtom, registeredAtom) +import Builder (buildExpressionThrows, contextualize) +import Control.Exception (Exception, catch, throwIO, try) +import Control.Monad (foldM, when) +import Data.List (find, partition) +import Data.List.NonEmpty (NonEmpty (..)) +import qualified Data.List.NonEmpty as NE +import Data.Maybe (fromMaybe) +import qualified Data.Text as T +import Deps (BuildTermFunc, BuildTermMethodS, Evaluation (..), SaveEvalFunc, SaveStepFunc, State, Term (..)) +import Locator (locatedExpression, withLocatedExpression) +import Matcher (MetaValue (..), Subst (..), combine, matchExpression', substEmpty, substSingle) +import Must (Must (..)) +import Random (shuffle) +import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite) +import Rule (RuleContext (RuleContext), matchExpressionWithRule') +import Text.Printf (printf) +import Yaml (ExtraArgument (..), normalizationRules) +import qualified Yaml as Y + +-- A term together with the derivation that reached it: what one frame of a +-- judgment's spine is handed and hands on. +type Morphed = (Expression, NonEmpty Rewritten) + +-- How the morphing side reaches back to the dataization one. An atom may ask +-- phino to reduce an operand of its own (see 'ReduceFunc' in 'Atoms'), and the +-- answer is a whole run of 𝔻 β€” a judgment 𝕄 has no business knowing about, +-- since 'Dataize' imports 'Morph' and not the other way round. The reduction is +-- therefore injected into the context, the way 'Deps' injects '_buildTerm', and +-- 'Dataize' supplies its own 'reduction' for it. +type ReductionFunc = Expression -> ReduceContext -> ReduceFunc + +-- The initial, empty state a run of 𝕄 or 𝔻 starts from. The 'State' type itself +-- lives in 'Deps' next to 'BuildTermMethod'. +emptyState :: State +emptyState = "" + +-- How many steps of the 𝕄/𝔻 recursion one branch of a derivation may take +-- ('_limit', the '--max-steps' option) and how many the branch reaching this +-- point has already taken ('_spent'). 𝕄 and 𝔻 recurse into each other, into the +-- premises of their own rules and into the atoms they fire, so a budget local to +-- one of those chains is reset by the next nested call and bounds nothing (see +-- #1052). This one rides in the context that every such path β€” the spine, the +-- side-premises, '_dataize' and '_morph' β€” already carries, so a nested call +-- inherits the count of the call that made it. It bounds depth, not total work: +-- a premise passes its count down but not back, so siblings each descend from +-- the same '_spent'. Bounding every branch is enough to terminate, since a rule +-- has finitely many premises. +data Steps = Steps + { _limit :: Int + , _spent :: Int + } + +-- The context every reduction of the calculus is threaded with β€” 𝕄 here and 𝔻 in +-- 'Dataize' β€” carrying the configuration plus the step budget spent so far. Nothing global is fixed here: the universe (the second argument 'e' of +-- 𝕄(n, e, s) and 𝔻(n, e, s)) is a plain expression threaded as an argument to +-- 'dataize'', 'morph'' and on to the atoms, and the state 's' is threaded the same +-- way (see 'State'). The working expression needed for normalization is taken +-- from the head of the step chain, so no separate wrapper type is threaded +-- around. +data ReduceContext = ReduceContext + { _locator :: Expression + , _maxDepth :: Int + , _maxCycles :: Int + , _steps :: Steps + , _depthSensitive :: Bool + , _shuffle :: Bool + , _partial :: Bool + , _deep :: Bool + , _atoms :: Registry + , _buildTerm :: BuildTermFunc + , _reduce :: ReductionFunc + , _saveStep :: SaveStepFunc + , _saveEval :: SaveEvalFunc + } + +data ReduceException + = OutOfSteps Int + | -- An atom could not fire: the '--atoms' registry carries no Ξ» function of + -- that name, so there is nothing to run. The name is that of the atom 𝔼 + -- actually failed on, which for a chain of dispatches is the innermost one, + -- since 'ml' reduces a head before the atom above it fires. + Stuck T.Text + | -- A 'Stuck' caught by a frame of the 𝕄/𝔻 spine, together with the + -- derivation that frame had reached (see 'parking'). The head of the chain + -- is the working expression with the stuck application left intact and + -- everything reduced before it already in place: the residual program that + -- '_partial' turns into the 'Residual' outcome. + StuckAt T.Text (NonEmpty Rewritten) + | -- An 'OutOfSteps' caught by a spine frame, carrying that frame's derivation + -- just like 'StuckAt': a term that never reduces is a stuck site too, so + -- '_partial' parks it and hands back the residual instead of failing hard + -- (#1078) + OutOfStepsAt Int (NonEmpty Rewritten) + deriving anyclass (Exception) + +instance Show ReduceException where + show (OutOfSteps limit) = + printf "Dataization did not finish before reaching the limit of steps: --max-steps=%d" limit + show (OutOfStepsAt limit _) = show (OutOfSteps limit) + show (Stuck func) = printf "Atom '%s' does not exist" (T.unpack func) + show (StuckAt func _) = show (Stuck func) + +-- Charge one step of the 𝕄/𝔻 recursion to the budget, refusing to descend once +-- it is gone. '--max-cycles' and '--max-depth' bound only the normalization run +-- inside a single step, so before this the recursion itself was unbounded and a +-- term that never reduces to bytes kept 𝕄 and 𝔻 calling each other forever +-- (#1052). Rewriting hands back whatever it has reached when it runs out of +-- cycles; 𝔻 has no partial answer to give, so an exhausted budget always throws, +-- with or without '--depth-sensitive'. +deeper :: ReduceContext -> IO ReduceContext +deeper ctx@ReduceContext{_steps = Steps limit spent} + | spent >= limit = throwIO (OutOfSteps limit) + | otherwise = pure ctx{_steps = Steps limit (spent + 1)} + +-- Split the Ξ» binding off a formation for the LAMBDA morphing rule: the name of +-- the atom to fire and the formation it fires against, the Ξ» binding removed β€” +-- the two things 𝔼 reports besides the result. A formation with no Ξ» binding, +-- or with more than one, has nothing to fire. +lambda :: [Binding] -> Maybe (T.Text, Expression) +lambda bds = case partition isLambda bds of + ([BiLambda (Function func)], rest) -> Just (func, ExFormation rest) + _ -> Nothing + where + isLambda :: Binding -> Bool + isLambda (BiLambda _) = True + isLambda _ = False + +-- The same as 'lambda', but only for a formation that is saturated: one with +-- every binding of it filled (see 'filled'). A void is an argument the program +-- has not given yet, so such a formation is a method waiting to be applied +-- rather than an application waiting to be computed, and firing it would hand +-- the atom a βˆ… where it expects a value. 𝔻 needs no such guard, since it +-- fires only what dataization demands and nothing demands a method; the deep +-- walk meets every one a program declares β€” the method table of the object +-- model above all β€” so it asks first (see 'deepened'). +saturated :: [Binding] -> Maybe (T.Text, Expression) +saturated bds = case lambda bds of + Just (func, ExFormation rest) | all filled rest -> Just (func, ExFormation rest) + _ -> Nothing + +-- Whether a binding hands the formation something to work with. A void does +-- not: it names an argument the program has still to supply. Neither does βŠ₯: +-- the deep walk reduces a body in the scope of the formation around it, and a +-- formation standing unapplied still holds ρ ↦ βˆ…, so a ΞΎ.ρ in that body comes +-- back as βŠ₯ rather than as the object the next dispatch supplies (#1196). +filled :: Binding -> Bool +filled (BiVoid _) = False +filled (BiTau _ ExTermination) = False +filled _ = True + +-- Run one frame of the 𝕄/𝔻 spine, attaching its derivation to a stuck atom or +-- an exhausted budget escaping it. 'Stuck' is raised deep inside an atom, which +-- knows nothing about the chain, so the innermost spine frame it reaches is the +-- one to record where the derivation stopped: the head of that frame's chain is +-- the working expression with the stuck application intact and everything +-- reduced before it already in place. The same holds for 'OutOfSteps': a term +-- cycling through the universe is no more a failure of the chain than a missing +-- atom is, and under '_partial' it deserves the same parked residual (#1078). +-- Outer frames see the '…At' signals and let them pass, since their chains are +-- prefixes of that one; a side-computation running on a chain of its own strips +-- the chain off again (see 'unparked') before the signal reaches the spine. +parking :: NonEmpty Rewritten -> IO a -> IO a +parking seq action = action `catch` rethrow + where + rethrow :: ReduceException -> IO a + rethrow (Stuck func) = throwIO (StuckAt func seq) + rethrow (OutOfSteps limit) = throwIO (OutOfStepsAt limit seq) + rethrow failure = throwIO failure + +-- Strip the derivation off a stuck atom escaping a side-computation that ran +-- on a chain of its own β€” an atom dataizing its input through '_dataize', or a +-- 'morph' premise through '_morph'. That chain is not the spine's, so it is +-- dropped and the spine frame around the side-computation attaches its own +-- (see 'parking'). +unparked :: IO a -> IO a +unparked action = action `catch` rethrow + where + rethrow :: ReduceException -> IO a + rethrow (StuckAt func _) = throwIO (Stuck func) + rethrow (OutOfStepsAt limit _) = throwIO (OutOfSteps limit) + rethrow failure = throwIO failure + +-- The Morphing function 𝕄 maps normal forms to formations. It is ternary, +-- 𝕄(n, e, s): besides the term 'n' it takes the universe 'e' ('univ') β€” a plain +-- expression β€” and the mutable state 's', returning the morphed term together +-- with the new state. The universe is matched against the rule's 'e-match' +-- pattern (usually the '𝑒' meta, which binds 'e' so the 'universe' rule substitutes +-- it, but a rule may pin it to a literal such as 'mg' matching Ξ¦). Its rules +-- come from 'resources/morphing': the first matching rule's premises are evaluated and +-- its conclusion 'nresult' is built, always forwarding the same universe. The +-- clauses are disjoint (see #856, #860), so their declaration order must not be +-- load-bearing; when '_shuffle' is on (the '--shuffle' flag) the rules are +-- shuffled before the 'firstMatch' walk to exercise that invariant β€” mirroring +-- normalization's "apply until they stop matching". A genuinely order-independent +-- step stays deterministic; a hidden overlap surfaces as a nondeterministic +-- failure rather than staying silently green. +-- The 'morph' premise that produces the conclusion is the spine: when +-- its argument comes from a 'normalize' premise, the rewriter runs over that +-- argument and its individual steps (alpha, copy, dot, …) are spliced into the +-- chain before morphing continues. Every other premise is a side-computation +-- evaluated in isolation by 'sidePremise', its own steps discarded. +morph' :: Morphed -> Expression -> State -> ReduceContext -> IO (Morphed, State) +morph' (expr, seq) univ state caller = do + ctx <- deeper caller + parking seq $ do + rules <- if ctx._shuffle then shuffle Y.morphingRules else pure Y.morphingRules + matched <- firstMatch ctx rules + case matched of + Just (rule, subst) -> reduce ctx rule subst + Nothing -> throwIO (userError "no morphing rule matched") + where + firstMatch :: ReduceContext -> [Y.MorphRule] -> IO (Maybe (Y.MorphRule, Subst)) + firstMatch _ [] = pure Nothing + firstMatch ctx (rule : rest) = do + substs <- matchExpressionWithRule' (matchExpression' rule.ematch univ) expr (asRule rule) (RuleContext (execBuildTerm univ ctx)) + case substs of + (subst : _) -> pure (Just (rule, subst)) + [] -> firstMatch ctx rest + -- Match the conclusion term and check the guard; premises are no longer the + -- matcher's business, so 'where'/'having' stay empty and the guard lives in + -- 'when'. Every morphing guard reads only meta-variables bound by 'match' + -- and 'e-match', so it holds before any premise runs. + asRule :: Y.MorphRule -> Y.Rule + asRule rule = Y.Rule rule.name Nothing Nothing rule.match ExRoot rule.when Nothing Nothing + -- Evaluate the rule's premises and build its conclusion. A literal + -- conclusion is terminal. Otherwise the conclusion meta is produced by a + -- trailing 'morph' premise (the spine); if that premise's argument is itself + -- bound by a 'normalize' premise, the normalization joins the spine and its + -- steps splice in before morphing continues. + reduce :: ReduceContext -> Y.MorphRule -> Subst -> IO (Morphed, State) + reduce ctx rule subst = case producer rule.nresult rule.premises of + Nothing -> do + (final, state') <- sides ctx rule.premises subst + built <- buildExpressionThrows rule.nresult final + seq' <- leadsTo seq rule.name built ctx + pure ((built, seq'), state') + Just concl@(Y.Premise _ (Y.OpMorph arg)) -> case producer arg rule.premises of + Just normal@(Y.Premise _ (Y.OpNormalize inner)) -> do + (final, state') <- sides ctx (rule.premises `excluding` [concl, normal]) subst + built <- buildExpressionThrows inner final + labelled <- leadsTo seq rule.name built ctx + (normal', seq') <- normalized built labelled ctx + morph' (normal', seq') univ state' ctx + _ -> do + (final, state') <- sides ctx (rule.premises `excluding` [concl]) subst + built <- buildExpressionThrows arg final + seq' <- leadsTo seq rule.name built ctx + morph' (built, seq') univ state' ctx + Just _ -> throwIO (userError (printf "morphing rule '%s' must conclude with a 'morph' premise" rule.name)) + sides :: ReduceContext -> [Y.Premise] -> Subst -> IO (Subst, State) + sides ctx premises subst = foldM (sidePremise univ ctx) (subst, state) premises + +-- Morph the expression located at '_locator' β€” 𝕄 asked on its own, the way +-- 'dataize' asks 𝔻. The whole input expression is itself the universe Ξ¦ (the 'e' +-- argument) threaded through 𝕄, so it is passed both as the located target and +-- as the universe; the default locator Q therefore morphs the top formation, +-- which 'mf' hands back unchanged, and '_locator' is how one aims 𝕄 at a +-- subterm. Unlike 𝔻, 𝕄 is total: it stops at the first formation it reaches +-- ('mf') and never demands bytes, and where no formation is reachable it answers +-- with the terminator βŠ₯ ('dead', 'xi', 'mg', 'mad', 'maad') rather than failing. +-- Only the atoms 'ml' fires can still get stuck, and '_partial' parks them just +-- as it does under 𝔻: the answer is then the residual subterm the spine had +-- reached, taken from '_locator' of its working expression. Stopping at the +-- first formation leaves everything that formation holds as it was written, +-- which is what '_deep' walks into before the answer is handed back (see +-- 'deepened'). +morph :: Expression -> ReduceContext -> IO (Expression, [Rewritten]) +morph universe ctx@ReduceContext{..} = do + expr <- locatedExpression _locator universe + result <- try (morph' (expr, (universe, Nothing) :| []) universe emptyState ctx) + case result of + Right ((morphed, seq), state) -> walked morphed seq state + Left (StuckAt _ seq) | _partial -> do + residue <- locatedExpression _locator (fst (NE.head seq)) + walked residue seq emptyState + Left (OutOfStepsAt _ seq) | _partial -> do + residue <- locatedExpression _locator (fst (NE.head seq)) + walked residue seq emptyState + Left failure -> throwIO (failure :: ReduceException) + where + -- The answer 𝕄 reached, walked by '_deep' before it is handed back (see + -- 'deepened'), and the chain that led to both. The walk joins the chain as + -- one step named 'deep', so '--sequence' ends on the term the command + -- prints. Morphing starts from the empty state and the state the walk ends + -- on goes the way 𝕄's own goes: no caller consumes it yet. + walked :: Expression -> NonEmpty Rewritten -> State -> IO (Expression, [Rewritten]) + walked morphed seq state + | not _deep = pure (morphed, reverse (NE.toList seq)) + | otherwise = do + (deep, _) <- deepened morphed universe state ctx + seq' <- leadsTo seq "deep" deep ctx + pure (deep, reverse (NE.toList seq')) + +-- Walk what 𝕄 answered with, entering everything it left as it was written β€” +-- the mechanism behind '--deep' ('_deep'). 𝕄 navigates a term to the first +-- formation it reaches and 'mf' hands that formation back with its bindings +-- untouched, since firing a bare Ξ» is 𝔻's business; 𝔻 in turn follows the one +-- path dataization demands and ends in bytes. A part of a program that nothing +-- demands β€” the argument of an atom that cannot fire, for one β€” is therefore +-- reduced by neither, and the object structure is lost to the one that does +-- reduce it (#1124). This walk demands nothing either. It asks 𝕄 about every +-- sub-expression and, where 𝕄 lands on a formation whose Ξ» the registry +-- serves, fires it and asks 𝕄 about the answer again (see 'fired'). A +-- sub-expression on whose way an atom fired is replaced by the answer of the +-- last firing; where none fired it stays as it was written and only its own +-- parts are walked, so the calls the registry does not serve keep their names +-- and what comes back is still the same program, reduced as far as the +-- registry allows. Every entry is charged to the '--max-steps' budget, which +-- is what bounds the walk. +deepened :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) +deepened expr univ = go Nothing ExXi expr + where + -- A term as it was written, together with what its free ΞΎ stands for: the + -- formation the walk entered it from, without the binding it came from, + -- exactly the context the 'dot' rule hands a dispatched body. At the top + -- there is no such formation, so ΞΎ stands for itself and contextualization + -- leaves the term alone. + go :: Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) + go dispatched context term state' caller = do + ctx' <- deeper caller + (walked, walkedState) <- parts context term state' caller + answer <- fired dispatched (contextualize walked context) univ walkedState ctx' + maybe (pure (walked, walkedState)) pure answer + -- The parts of a term nothing fired on, walked one by one and put back + -- where they were, so the term keeps the shape it was written in. + parts :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) + parts _ (ExFormation bds) state' caller = do + (entered, state'') <- bindings bds bds state' caller + pure (ExFormation entered, state'') + parts context (ExDispatch target attr) state' caller = do + (entered, state'') <- go (Just attr) context target state' caller + pure (ExDispatch entered attr, state'') + parts context (ExApplication target arg) state' caller = do + (entered, state'') <- go Nothing context target state' caller + (applied, state''') <- argument context arg state'' caller + pure (ExApplication entered applied, state''') + parts _ term state' _ = pure (term, state') + -- Walk the bindings of a formation left to right, threading the state + -- through them. Only what the formation itself holds is entered: ρ names + -- the object around it rather than one inside it, and a void, Ξ” or Ξ» + -- binding carries no term to walk at all. + bindings :: [Binding] -> [Binding] -> State -> ReduceContext -> IO ([Binding], State) + bindings _ [] state' _ = pure ([], state') + bindings whole (BiTau attr body : rest) state' caller + | attr /= AtRho = do + (entered, state'') <- go Nothing (scope attr whole) body state' caller + (others, state''') <- bindings whole rest state'' caller + pure (BiTau attr entered : others, state''') + bindings whole (bd : rest) state' caller = do + (others, state'') <- bindings whole rest state' caller + pure (bd : others, state'') + -- The context a binding's body is entered in: the formation without that + -- binding, the very context 'dot' contextualizes a dispatched body in, so + -- a body reaching back at itself through ΞΎ collapses instead of looping. + scope :: Attribute -> [Binding] -> Expression + scope attr bds = ExFormation (filter (not . named) bds) + where + named :: Binding -> Bool + named (BiTau attr' _) = attr' == attr + named _ = False + -- Both sides of an application stand in the same context: the term it + -- applies is walked by the caller and the argument it binds is walked here. + argument :: Expression -> Argument -> State -> ReduceContext -> IO (Argument, State) + argument context (ArTau attr arg) state' caller = do + (entered, state'') <- go Nothing context arg state' caller + pure (ArTau attr entered, state'') + argument context (ArAlpha alpha arg) state' caller = do + (entered, state'') <- go Nothing context arg state' caller + pure (ArAlpha alpha entered, state'') + +-- Ask 𝕄 about a term and fire the Ξ» of the formation it reaches, as long as +-- the registry serves it, asking 𝕄 about every answer again: what comes back +-- is the answer of the last firing, or nothing at all where no atom fired. This +-- is the firing 'ml' makes without the dispatch that makes 'ml' make it β€” the +-- one 𝕄 leaves to 𝔻 β€” except in what it hands back: the atom's raw answer, not +-- the normal form 𝔼 makes of it, since the deep walk stands that answer back +-- into the program, where a normal form would spell the whole object out in +-- place of the name the program called it by. A Ξ» the registry does not carry +-- is left alone rather than fired and got stuck on, so what phino cannot +-- compute stays as it was written with or without '_partial'; an atom that +-- cannot fire deeper on the spine still fails the run, exactly as it does +-- under 𝕄 alone, and '_partial' parks it. A formation still waiting for its +-- arguments is left alone too (see 'saturated'). A term standing as the target +-- of a dispatch is where 'ml' has its say: the Ξ» is fired only where the +-- dispatched attribute is none of the formation's own (see 'demanded'). +fired :: Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Maybe (Expression, State)) +fired dispatched term univ state caller = do + ctx <- deeper caller + morphed <- try (reduced ctx) + case morphed of + Right (ExFormation bds, state') + | demanded bds -> maybe (pure Nothing) (evaluated ctx state') (saturated bds) + Right _ -> pure Nothing + Left failure -> parked failure + where + -- Whether the dispatch the term stands under demands the Ξ» of the formation + -- 𝕄 reached. 'ml' fires that Ξ» only where the dispatched attribute is none + -- of the formation's own, since 'dot' resolves the dispatch before 'ml' is + -- ever reached, and a walk firing it first answers a formation the dispatch + -- no longer fits (#1187). A term standing anywhere else is demanded by + -- nothing and the walk fires what 'mf' left bare, as it always has. + demanded :: [Binding] -> Bool + demanded bds = not (any bound bds) + where + bound :: Binding -> Bool + bound (BiTau attr _) = Just attr == dispatched + bound _ = False + -- 𝕄 takes normal forms only and a term taken from the program as it was + -- written is not necessarily one, so it is normalized against the universe + -- first, exactly as '--inside' normalizes what it is handed. Both chains + -- are dropped: the walk is not the spine and reports one step of its own + -- (see 'morph'), so a stuck atom leaves without a derivation ('unparked'). + reduced :: ReduceContext -> IO (Expression, State) + reduced ctx = unparked $ do + (normal, _) <- normalized term ((univ, Nothing) :| []) ctx + ((morphed, _), state') <- morph' (normal, (univ, Nothing) :| []) univ state ctx + pure (morphed, state') + -- Fire the Ξ» of the formation 𝕄 reached and go on from its answer, keeping + -- the answer of the last firing. The firing is reported to '_saveEval' like + -- every other one, with the term the caller is given, so the protocol and + -- the program agree on what the atom answered. + evaluated :: ReduceContext -> State -> (T.Text, Expression) -> IO (Maybe (Expression, State)) + evaluated ctx state' (func, self) = case registeredAtom ctx._atoms func of + Nothing -> pure Nothing + Just registered -> do + answer <- fireAtom func registered self univ (ctx._reduce univ ctx) + ctx._saveEval (Evaluation func self (Just answer)) + again <- fired dispatched answer univ state' ctx + pure (Just (fromMaybe (answer, state') again)) + parked :: ReduceException -> IO (Maybe a) + parked (Stuck _) | caller._partial = pure Nothing + parked failure = throwIO failure + +-- The premise binding the given expression meta, if any. The conclusion of a +-- morphing rule and the argument of a continuation premise are looked up here to +-- find the premise that produces them. +producer :: Expression -> [Y.Premise] -> Maybe Y.Premise +producer (ExMeta name) = find (\premise -> premise.result == name) +producer _ = const Nothing + +-- The premises whose result meta is not bound by any of the given ones β€” the +-- side-computations left once the spine premises are removed. +excluding :: [Y.Premise] -> [Y.Premise] -> [Y.Premise] +excluding premises removed = filter (\premise -> premise.result `notElem` map (.result) removed) premises + +-- Evaluate one side-computation premise β€” a 'morph', 'evaluate' or 'contextualize' +-- of an earlier term β€” in isolation, binding its result meta. These never splice +-- steps into the trace: 'morph' and 'evaluate' reduce on a fresh chain and discard +-- it, 'contextualize' is pure. The state is threaded through: 'evaluate' (the +-- 𝔼 of the 'ml' and 'fire' rules) takes the incoming state 𝑠1 and yields a +-- new one 𝑠2, 'morph' propagates whatever its sub-reduction produced, and every +-- other operation leaves the state untouched. +sidePremise :: Expression -> ReduceContext -> (Subst, State) -> Y.Premise -> IO (Subst, State) +sidePremise univ ctx (subst, state) premise = do + (term, state') <- runOperation + case combine (substSingle premise.result (metaValue term)) subst of + Just subst' -> pure (subst', state') + Nothing -> throwIO (userError (printf "premise meta '%s' clashes with an existing binding" (T.unpack premise.result))) + where + -- The 𝔼 ('evaluate') and 𝕄 ('morph') operations can change the state, so they + -- go through their state-aware builders; every other operation is stateless + -- and the incoming state is returned unchanged. + runOperation :: IO (Term, State) + runOperation = case premise.operation of + Y.OpEvaluate expr universe -> _evaluate ctx state [ArgExpression expr, ArgExpression universe] subst + Y.OpMorph expr -> _morph univ ctx state [ArgExpression expr] subst + operation -> do + term <- execBuildTerm univ ctx (verb operation) (verbArgs operation) subst + pure (term, state) + metaValue :: Term -> MetaValue + metaValue (TeExpression value) = MvExpression value + metaValue (TeAttribute value) = MvAttribute value + metaValue (TeBytes value) = MvBytes value + metaValue (TeBindings value) = MvBindings value + +-- The build-term function name backing a premise operation. +verb :: Y.Operation -> String +verb (Y.OpMorph _) = "morph" +verb (Y.OpNormalize _) = "normalize" +verb (Y.OpEvaluate _ _) = "evaluate" +verb (Y.OpContextualize _ _) = "contextualize" +verb (Y.OpDataize _) = "dataize" + +-- The build-term arguments backing a premise operation. +verbArgs :: Y.Operation -> [ExtraArgument] +verbArgs (Y.OpMorph expr) = [ArgExpression expr] +verbArgs (Y.OpNormalize expr) = [ArgExpression expr] +verbArgs (Y.OpEvaluate expr universe) = [ArgExpression expr, ArgExpression universe] +verbArgs (Y.OpContextualize expr context) = [ArgExpression expr, ArgExpression context] +verbArgs (Y.OpDataize expr) = [ArgExpression expr] + +leadsTo :: NonEmpty Rewritten -> String -> Expression -> ReduceContext -> IO (NonEmpty Rewritten) +leadsTo ((current, _) :| rest) rule expr ReduceContext{..} = do + updated <- withLocatedExpression _locator expr current + pure ((updated, Nothing) :| (current, Just rule) : rest) + +-- Reduce 'expr' to its normal form through the normalization rewriter, embedding +-- it at '_locator' into the working expression taken from the head of the step +-- chain so the rewriter sees the surrounding context. Splices the individual +-- steps (alpha, copy, dot, …) into the chain and returns the normalized +-- expression together with the extended sequence. +normalized :: Expression -> NonEmpty Rewritten -> ReduceContext -> IO (Expression, NonEmpty Rewritten) +normalized expr seq ctx@ReduceContext{..} = do + whole <- withLocatedExpression _locator expr (fst (NE.head seq)) + (rewrittens, _) <- rewrite whole normalizationRules (rewriteContext ctx) + let (rw :| rws) = NE.reverse rewrittens + seq' = rw :| rws <> NE.tail seq + expr' <- locatedExpression _locator (fst rw) + pure (expr', seq') + where + -- Switch the reduction context to a rewriting context for normalization, + -- disabling the must-checker and breakpoints. + rewriteContext :: ReduceContext -> RewriteContext + rewriteContext ReduceContext{..} = + RewriteContext _locator _maxDepth _maxCycles _depthSensitive _buildTerm MtDisabled Nothing _saveStep + +-- Bind 'expr' to a synthetic attribute of the universe and reduce it to a +-- normal form there, handing back the extended universe together with the +-- locator that aims at the binding. This is the trick phino has always played +-- to reduce a sub-expression that is not part of the program β€” an atom's +-- operand, while the atoms still lived in the binary β€” and it is now the +-- contract of the '--inside' option, so an atom script asking phino to reduce +-- a part of the formation it was given does not have to splice it into the text +-- of the universe by hand. 𝔻 and 𝕄 accept normal forms only and an expression +-- handed in from outside is not necessarily one (a dispatch off a formation, +-- '⟦ x ↦ 6, ρ ↦ 5 ⟧.x', is not), so it is normalized against the extended +-- universe before either judgment sees it. The context comes back aimed at that +-- binding, so the caller hands the extended universe and the context it got +-- straight to 'dataize' or 'morph'. +insideUniverse :: Expression -> Expression -> ReduceContext -> IO (Expression, ReduceContext) +insideUniverse expr univ ctx@ReduceContext{_buildTerm = buildTerm} = case univ of + ExFormation bds -> do + (TeAttribute attr) <- buildTerm "random-tau" [] substEmpty + let aiming = ctx{_locator = ExDispatch ExRoot attr} + synthetic = ExFormation (BiTau attr expr : bds) + (normal, _) <- normalized expr ((synthetic, Nothing) :| []) aiming + pure (ExFormation (BiTau attr normal : bds), aiming) + _ -> throwIO (userError "Can't reduce an expression inside a universe which is not a formation") + +-- phino implements no Ξ» function of its own. Which atoms exist is a property of +-- the object model being dataized, not of the calculus, so they come from the +-- '--atoms' registry and run as external scripts (see 'Atoms'). A name the +-- registry does not carry has no Ξ» function to fire at all, and 𝔼 gets stuck on +-- it β€” the one behaviour left here. The script is handed the formation 'self' +-- (its Ξ» binding already removed, so it may dispatch on it) and the universe +-- 'univ'; the state 𝑠 is not part of that contract yet, so it is threaded +-- through untouched. +atom :: T.Text -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) +atom func self univ state ctx = case registeredAtom ctx._atoms func of + Nothing -> throwIO (Stuck func) + Just registered -> do + raw <- fireAtom func registered self univ (ctx._reduce univ ctx) + pure (raw, state) + +-- Augment the injected, context-free term builder with the dataization and +-- morphing operations that need the universe: 'evaluate' applies an atom and +-- 'morph' morphs a sub-expression. 𝔼 ('evaluate') takes the universe as an +-- explicit second expression argument, while 𝕄 ('morph') is handed the threaded +-- 'univ'. Every other function is delegated unchanged. This is the matcher's +-- condition path (guards in 'when'/'having'), which has no state to thread, so 𝔼 +-- and 𝕄 run here on a fresh, empty state whose result is discarded; the +-- state-threading callers in 'sidePremise' use '_evaluate' and '_morph' directly. +execBuildTerm :: Expression -> ReduceContext -> BuildTermFunc +execBuildTerm _ ctx "evaluate" = \args subst -> fst <$> _evaluate ctx emptyState args subst +execBuildTerm univ ctx "morph" = \args subst -> fst <$> _morph univ ctx emptyState args subst +execBuildTerm _ ctx func = _buildTerm ctx func + +-- The Evaluation function 𝔼(b, e, s): it fires the Ξ» atom of a formation 'b' +-- against the global universe 'e', under the incoming state 𝑠, normalizes the +-- atom's raw result 𝒩(e₁) = n, and returns that normal form together with the +-- new state. Normalizing here makes 𝔼's codomain 𝓝 (as its type demands), so +-- callers ('fire', 'ml') need no follow-up 'normalize' premise. The universe is +-- passed explicitly as the second argument (rather than threaded behind the +-- scenes), matching how the morphing 𝕄 and dataization 𝔻 functions carry it. +-- Every firing is reported to '_saveEval', which the '--evaluations' option +-- turns into one record per line. The reported result is the normal form 𝔼 +-- returns, never the atom's raw answer, so the protocol and the caller see the +-- same term. Firings are reported in the order they complete, so the atom of a +-- head reduced by 'ml' is reported before the one dispatched on its result. A +-- firing that gets stuck is reported too, with no result, when the run is a +-- partial evaluation rather than a failure ('_partial'): the site is what the +-- caller wants to learn then. The report is made before the signal goes on to +-- the spine, where 'parking' attaches the derivation to it. +_evaluate :: ReduceContext -> State -> BuildTermMethodS +_evaluate ctx state [ArgExpression expr, ArgExpression universe] subst = do + form <- buildExpressionThrows expr subst + univ <- buildExpressionThrows universe subst + case form of + ExFormation bds -> case lambda bds of + Just (func, args) -> do + (raw, state') <- atom func args univ state ctx `catch` parked func args + (normal, _) <- normalized raw ((univ, Nothing) :| []) ctx + ctx._saveEval (Evaluation func args (Just normal)) + pure (TeExpression normal, state') + Nothing -> throwIO (userError "Function evaluate() expects a formation with a Ξ» binding") + _ -> throwIO (userError "Function evaluate() expects a formation") + where + parked :: T.Text -> Expression -> ReduceException -> IO a + parked func args failure@(Stuck _) = do + when ctx._partial (ctx._saveEval (Evaluation func args Nothing)) + throwIO failure + parked _ _ failure = throwIO failure +_evaluate _ _ _ _ = throwIO (userError "Function evaluate() requires exactly 2 expression arguments") + +-- The Morphing function 𝕄 exposed as a build-term function so a rule can morph +-- a sub-expression in its 'where' (the 'md' and 'ma' rules morph +-- the head before re-attaching it). The step chain is discarded: the producing +-- rule splices the surrounding normalization steps itself, and a stuck atom met +-- on the way leaves without it (see 'unparked'). The state is threaded through +-- and the new state returned alongside the morphed term. +_morph :: Expression -> ReduceContext -> State -> BuildTermMethodS +_morph univ ctx state [ArgExpression expr] subst = unparked $ do + built <- buildExpressionThrows expr subst + ((morphed, _), state') <- morph' (built, (univ, Nothing) :| []) univ state ctx + pure (TeExpression morphed, state') +_morph _ _ _ _ _ = throwIO (userError "Function morph() requires exactly 1 expression argument") diff --git a/src/Yaml.hs b/src/Yaml.hs --- a/src/Yaml.hs +++ b/src/Yaml.hs @@ -17,7 +17,7 @@ import qualified Data.Aeson.Key as Key import qualified Data.Aeson.KeyMap as KeyMap import qualified Data.ByteString as BS -import Data.FileEmbed (embedDir, embedFile) +import Data.FileEmbed (embedDir) import Data.Text (Text, unpack) import Data.Yaml (Parser) import qualified Data.Yaml as Yaml @@ -307,15 +307,17 @@ rule ) +-- Decode one rule out of the file that carries it, naming that file when its +-- YAML is broken. A rule set is a directory 'embedDir' embeds wholesale, one +-- rule per file, the file named after the rule it carries. +decodeRule :: (FromJSON a) => (FilePath, BS.ByteString) -> a +decodeRule (path, bs) = case Yaml.decodeEither' bs of + Right rule -> rule + Left err -> error $ "YAML parse error in " ++ path ++ ": " ++ show err + normalizationRules :: [Rule] {-# NOINLINE normalizationRules #-} normalizationRules = map decodeRule $(embedDir "resources/normalize") - where - decodeRule :: (FilePath, BS.ByteString) -> Rule - decodeRule (path, bs) = - case Yaml.decodeEither' bs of - Right rule -> rule - Left err -> error $ "YAML parse error in " ++ path ++ ": " ++ show err yamlRule :: FilePath -> IO Rule yamlRule = Yaml.decodeFileThrow @@ -494,19 +496,14 @@ pure rule ) -decodeRules :: (FromJSON a) => FilePath -> BS.ByteString -> [a] -decodeRules path bs = case Yaml.decodeEither' bs of - Right rs -> rs - Left err -> error $ "YAML parse error in " ++ path ++ ": " ++ show err - morphingRules :: [MorphRule] {-# NOINLINE morphingRules #-} -morphingRules = decodeRules "resources/morphing.yaml" $(embedFile "resources/morphing.yaml") +morphingRules = map decodeRule $(embedDir "resources/morphing") dataizationRules :: [DataizeRule] {-# NOINLINE dataizationRules #-} -dataizationRules = decodeRules "resources/dataization.yaml" $(embedFile "resources/dataization.yaml") +dataizationRules = map decodeRule $(embedDir "resources/dataization") contextualizationRules :: [ContextualizeRule] {-# NOINLINE contextualizationRules #-} -contextualizationRules = decodeRules "resources/contextualization.yaml" $(embedFile "resources/contextualization.yaml") +contextualizationRules = map decodeRule $(embedDir "resources/contextualization") diff --git a/test/AtomsSpec.hs b/test/AtomsSpec.hs --- a/test/AtomsSpec.hs +++ b/test/AtomsSpec.hs @@ -659,6 +659,36 @@ it "fails a question whose dotted path runs into a void attribute" $ refusesAt "⟦ v ↦ βˆ… ⟧" (referring 1 "v.length" False "*2A-*") ["L_answer", "carries no attribute 'v.length'"] + -- An argument of an application binds an attribute the way a Ο„ binding of + -- a formation does, so a path walks into one just the same: a marker a + -- program built itself and put in a void is read back as written, since + -- dataizing the object around it would fire the Ξ» inside it (#1212) + it "reaches an attribute an argument of an application binds" $ + servesAt + "⟦ x ↦ Ξ¦.bool( if ↦ ⟦ guard ↦ ⟦ Ξ» ‍ S1 ⟧ ⟧ ) ⟧" + (referring 1 "x.if.guard" False "*'\"Ξ»\":\"S1\"'*") + "⟦ Ξ” ‍ FF- ⟧" + + it "walks past the arguments of an application the path does not name" $ + servesAt + "⟦ x ↦ Ξ¦.tuple( length ↦ ⟦ Ξ” ‍ 01- ⟧, head ↦ ⟦ Ξ” ‍ 02- ⟧ ) ⟧" + (referring 1 "x.length" False "*'\"Ξ”\":\"01-\"'*") + "⟦ Ξ” ‍ FF- ⟧" + + it "walks past a positional argument of an application" $ + servesAt + "⟦ x ↦ ⟦ y ↦ ⟦ Ξ” ‍ 04- ⟧ ⟧( Ξ±0 ↦ ⟦ Ξ” ‍ 05- ⟧ ) ⟧" + (referring 1 "x.y" False "*'\"Ξ”\":\"04-\"'*") + "⟦ Ξ” ‍ FF- ⟧" + + -- What an application binds an attribute to is what the attribute is, + -- whatever the formation under it still says about it + it "takes the argument of an application over the void it fills" $ + servesAt + "⟦ x ↦ ⟦ y ↦ βˆ… ⟧( y ↦ ⟦ Ξ” ‍ 03- ⟧ ) ⟧" + (referring 1 "x.y" False "*'\"Ξ”\":\"03-\"'*") + "⟦ Ξ” ‍ FF- ⟧" + -- πœ‘-calculus types nothing nominally, so the forma of a typed literal -- lives in the name it is dispatched off Ξ¦ by and nowhere else: an answer -- that is an application spells that name, the way a formation spells its diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -1844,32 +1844,8 @@ ["explain", "--morph"] [ unlines [ "\\begin{phinoMorphingInference}" - , " \\phinoName{mf}" - , " \\phinoConclusion{ \\phinoMorph{ [[ B_0 ]] }{ e_0 }{ s }{ [[ B_0 ]] }{ s } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{ml}" - , " \\phinoLabel{\\lambda}" - , " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F_0, B_2 ]] }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }" - , " \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau_0 }{ n_2 } }" - , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }" - , " \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F_0, B_2 ]] . \\tau_0 }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{mphi}" - , " \\phinoLabel{\\varphi}" - , " \\phinoCondition{ @ \\in B_0 \\;\\text{and}\\; \\tau_0 \\notin B_0 \\;\\text{and}\\; L \\notin B_0 }" - , " \\phinoPremise{ \\phinoNormalize{ [[ B_0 ]] . @ . \\tau_0 }{ n_1 } }" - , " \\phinoPremise{ \\phinoMorph{ n_1 }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }" - , " \\phinoConclusion{ \\phinoMorph{ [[ B_0 ]] . \\tau_0 }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{md}" - , " \\phinoCondition{ \\phinoNotFormation{ n_0 } }" - , " \\phinoPremise{ \\phinoMorph{ n_0 }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }" - , " \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau_0 }{ n_2 } }" - , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }" - , " \\phinoConclusion{ \\phinoMorph{ n_0 . \\tau_0 }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }" + , " \\phinoName{dead}" + , " \\phinoConclusion{ \\phinoMorph{ T }{ e_0 }{ s }{ T }{ s } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{ma}" @@ -1886,18 +1862,51 @@ , " \\phinoConclusion{ \\phinoMorph{ n_0 ( \\phiTerminal{\\alpha_{i0}} -> k_1 ) }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" - , " \\phinoName{mad}" + , " \\phinoName{maad}" , " \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }" , " \\phinoPremise{ \\phinoMorph{ T }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }" - , " \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> n_1 ) }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }" + , " \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> n_1 ) }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" - , " \\phinoName{maad}" + , " \\phinoName{mad}" , " \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }" , " \\phinoPremise{ \\phinoMorph{ T }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }" - , " \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> n_1 ) }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }" + , " \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> n_1 ) }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" + , " \\phinoName{md}" + , " \\phinoCondition{ \\phinoNotFormation{ n_0 } }" + , " \\phinoPremise{ \\phinoMorph{ n_0 }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }" + , " \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau_0 }{ n_2 } }" + , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }" + , " \\phinoConclusion{ \\phinoMorph{ n_0 . \\tau_0 }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }" + , "\\end{phinoMorphingInference}" + , "\\begin{phinoMorphingInference}" + , " \\phinoName{mf}" + , " \\phinoConclusion{ \\phinoMorph{ [[ B_0 ]] }{ e_0 }{ s }{ [[ B_0 ]] }{ s } }" + , "\\end{phinoMorphingInference}" + , "\\begin{phinoMorphingInference}" + , " \\phinoName{mg}" + , " \\phinoPremise{ \\phinoMorph{ T }{ Q }{ s_1 }{ n_1 }{ s_2 } }" + , " \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n_1 }{ s_2 } }" + , "\\end{phinoMorphingInference}" + , "\\begin{phinoMorphingInference}" + , " \\phinoName{ml}" + , " \\phinoLabel{\\lambda}" + , " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F_0, B_2 ]] }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }" + , " \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau_0 }{ n_2 } }" + , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }" + , " \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F_0, B_2 ]] . \\tau_0 }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }" + , "\\end{phinoMorphingInference}" + , "\\begin{phinoMorphingInference}" + , " \\phinoName{mphi}" + , " \\phinoLabel{\\varphi}" + , " \\phinoCondition{ @ \\in B_0 \\;\\text{and}\\; \\tau_0 \\notin B_0 \\;\\text{and}\\; L \\notin B_0 }" + , " \\phinoPremise{ \\phinoNormalize{ [[ B_0 ]] . @ . \\tau_0 }{ n_1 } }" + , " \\phinoPremise{ \\phinoMorph{ n_1 }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }" + , " \\phinoConclusion{ \\phinoMorph{ [[ B_0 ]] . \\tau_0 }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }" + , "\\end{phinoMorphingInference}" + , "\\begin{phinoMorphingInference}" , " \\phinoName{universe}" , " \\phinoLabel{\\Phi}" , " \\phinoCondition{ e_0 \\not= Q }" @@ -1906,19 +1915,10 @@ , " \\phinoConclusion{ \\phinoMorph{ Q }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" - , " \\phinoName{dead}" - , " \\phinoConclusion{ \\phinoMorph{ T }{ e_0 }{ s }{ T }{ s } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" , " \\phinoName{xi}" , " \\phinoPremise{ \\phinoMorph{ T }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }" , " \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }" , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{mg}" - , " \\phinoPremise{ \\phinoMorph{ T }{ Q }{ s_1 }{ n_1 }{ s_2 } }" - , " \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n_1 }{ s_2 } }" - , "\\end{phinoMorphingInference}" ] ] @@ -1927,11 +1927,6 @@ ["explain", "--dataize"] [ unlines [ "\\begin{phinoDataizationInference}" - , " \\phinoName{delta}" - , " \\phinoLabel{\\Delta}" - , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta_0, B_2 ]] }{ e_0 }{ s }{ \\delta_0 }{ s } }" - , "\\end{phinoDataizationInference}" - , "\\begin{phinoDataizationInference}" , " \\phinoName{box}" , " \\phinoCondition{ [ D \\char44{} L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset }" , " \\phinoPremise{ \\phinoContextualize{ e_1 }{ [[ B_1, @ -> e_1, B_2 ]] }{ e_2 } }" @@ -1940,6 +1935,11 @@ , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_1, B_2 ]] }{ e_0 }{ s_1 }{ \\delta_0 }{ s_2 } }" , "\\end{phinoDataizationInference}" , "\\begin{phinoDataizationInference}" + , " \\phinoName{delta}" + , " \\phinoLabel{\\Delta}" + , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta_0, B_2 ]] }{ e_0 }{ s }{ \\delta_0 }{ s } }" + , "\\end{phinoDataizationInference}" + , "\\begin{phinoDataizationInference}" , " \\phinoName{fire}" , " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F_0, B_2 ]] }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }" , " \\phinoPremise{ \\phinoDataize{ n_1 }{ e_0 }{ s_2 }{ \\delta_0 }{ s_3 } }" @@ -1966,37 +1966,37 @@ ["explain", "--contextualize"] [ unlines [ "\\begin{phinoContextualizationInference}" - , " \\phinoName{cg}" - , " \\phinoConclusion{ \\phinoContextualize{ Q }{ k_0 }{ Q } }" + , " \\phinoName{ca}" + , " \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }" + , " \\phinoPremise{ \\phinoContextualize{ e_1 }{ k_0 }{ n_2 } }" + , " \\phinoConclusion{ \\phinoContextualize{ n_0 ( \\tau_0 -> e_1 ) }{ k_0 }{ n_1 ( \\tau_0 -> n_2 ) } }" , "\\end{phinoContextualizationInference}" , "\\begin{phinoContextualizationInference}" - , " \\phinoName{cxi}" - , " \\phinoConclusion{ \\phinoContextualize{ \\phiTerminal{\\xi} }{ k_0 }{ k_0 } }" + , " \\phinoName{caa}" + , " \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }" + , " \\phinoPremise{ \\phinoContextualize{ e_1 }{ k_0 }{ n_2 } }" + , " \\phinoConclusion{ \\phinoContextualize{ n_0 ( \\phiTerminal{\\alpha_{i0}} -> e_1 ) }{ k_0 }{ n_1 ( \\phiTerminal{\\alpha_{i0}} -> n_2 ) } }" , "\\end{phinoContextualizationInference}" , "\\begin{phinoContextualizationInference}" - , " \\phinoName{ct}" - , " \\phinoConclusion{ \\phinoContextualize{ T }{ k_0 }{ T } }" + , " \\phinoName{cd}" + , " \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }" + , " \\phinoConclusion{ \\phinoContextualize{ n_0 . \\tau_0 }{ k_0 }{ n_1 . \\tau_0 } }" , "\\end{phinoContextualizationInference}" , "\\begin{phinoContextualizationInference}" , " \\phinoName{cf}" , " \\phinoConclusion{ \\phinoContextualize{ [[ B_0 ]] }{ k_0 }{ [[ B_0 ]] } }" , "\\end{phinoContextualizationInference}" , "\\begin{phinoContextualizationInference}" - , " \\phinoName{cd}" - , " \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }" - , " \\phinoConclusion{ \\phinoContextualize{ n_0 . \\tau_0 }{ k_0 }{ n_1 . \\tau_0 } }" + , " \\phinoName{cg}" + , " \\phinoConclusion{ \\phinoContextualize{ Q }{ k_0 }{ Q } }" , "\\end{phinoContextualizationInference}" , "\\begin{phinoContextualizationInference}" - , " \\phinoName{ca}" - , " \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }" - , " \\phinoPremise{ \\phinoContextualize{ e_1 }{ k_0 }{ n_2 } }" - , " \\phinoConclusion{ \\phinoContextualize{ n_0 ( \\tau_0 -> e_1 ) }{ k_0 }{ n_1 ( \\tau_0 -> n_2 ) } }" + , " \\phinoName{ct}" + , " \\phinoConclusion{ \\phinoContextualize{ T }{ k_0 }{ T } }" , "\\end{phinoContextualizationInference}" , "\\begin{phinoContextualizationInference}" - , " \\phinoName{caa}" - , " \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }" - , " \\phinoPremise{ \\phinoContextualize{ e_1 }{ k_0 }{ n_2 } }" - , " \\phinoConclusion{ \\phinoContextualize{ n_0 ( \\phiTerminal{\\alpha_{i0}} -> e_1 ) }{ k_0 }{ n_1 ( \\phiTerminal{\\alpha_{i0}} -> n_2 ) } }" + , " \\phinoName{cxi}" + , " \\phinoConclusion{ \\phinoContextualize{ \\phiTerminal{\\xi} }{ k_0 }{ k_0 } }" , "\\end{phinoContextualizationInference}" ] ] diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -10,7 +10,7 @@ module DataizeSpec (spec) where import AST -import Atoms (Registry, emptyRegistry, readRegistry) +import Atoms (Registry, emptyRegistry) import Control.Exception (SomeException) import Control.Monad import Data.Aeson (FromJSON) @@ -19,162 +19,63 @@ import Data.List.NonEmpty (NonEmpty (..)) import Data.Maybe (fromMaybe, isJust) import Data.Yaml qualified as Decode -import Dataize (DataizeContext (..), Outcome (..), Steps (..), dataize, dataize', emptyState, execBuildTerm, insideUniverse, morph, morph') -import Deps (Evaluation (..), Term (TeExpression), dontSaveEval, dontSaveStep) +import Dataize (Outcome (..), dataize, dataize', reduction) +import Deps (Evaluation (..), dontSaveEval, dontSaveStep) import Files (allPathsIn) -import Fixtures (fixtureRegistry, withNode, withServing, withShell) +import Fixtures (defaultReduceContext, fixtureRegistry, primitives, withAtoms, withNode) import Functions (buildTerm) import GHC.Generics (Generic) import Matcher (substEmpty) -import Parser (parseExpressionThrows) +import Morph (ReduceContext (..), Steps (..), emptyState, execBuildTerm) +import Parser (parseBytes, parseExpressionThrows) import Rewriter (Rewritten) import Rule (RuleContext (RuleContext), matchExpressionWithRule') import System.FilePath (makeRelative) import Test.Hspec -import Yaml (ExtraArgument (..)) import Yaml qualified --- Shuffle is enabled so the suite exercises the order-independence of the --- dataization rules (#909): a hidden overlap surfaces as a nondeterministic --- failure instead of staying silently green. The registry of Ξ» functions is --- empty, since phino implements none of them: a case that needs an atom to --- answer brings the fixture registry in through 'withAtoms'. -defaultDataizeContext :: Expression -> DataizeContext -defaultDataizeContext loc = DataizeContext loc 25 25 (Steps 250 0) False True False False emptyRegistry buildTerm dontSaveStep dontSaveEval - --- The same context with the fixture Ξ» functions registered (see 'Fixtures'). -withAtoms :: Registry -> DataizeContext -> DataizeContext -withAtoms registry ctx = ctx{_atoms = registry} - -test :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> String -> DataizeContext -> IO ((a, [Rewritten]), String)) -> [(String, Expression, Expression, a)] -> Spec +test :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> String -> ReduceContext -> IO ((a, [Rewritten]), String)) -> [(String, Expression, Expression, a)] -> Spec test func useCases = forM_ useCases $ \(desc, input, expr, output) -> it desc $ do - ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultDataizeContext ExRoot) - res `shouldBe` output - -test' :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> String -> DataizeContext -> IO ((a, NonEmpty Rewritten), String)) -> [(String, Expression, Expression, a)] -> Spec -test' func useCases = - forM_ useCases $ \(desc, input, expr, output) -> - it desc $ do - ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultDataizeContext ExRoot) + ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultReduceContext ExRoot) res `shouldBe` output -testDataize :: [(String, String, String, Bytes)] -> Spec -testDataize useCases = - forM_ useCases $ \(name, loc, src, res) -> - it name $ do - expr <- parseExpressionThrows src - loc' <- parseExpressionThrows loc - (value, _) <- dataize expr (defaultDataizeContext loc') - value `shouldBe` Dataized res - -testMorph :: [(String, String, String, String)] -> Spec -testMorph useCases = - forM_ useCases $ \(name, loc, src, res) -> - it name $ do - expr <- parseExpressionThrows src - loc' <- parseExpressionThrows loc - expected <- parseExpressionThrows res - (morphed, _) <- morph expr (defaultDataizeContext loc') - morphed `shouldBe` expected - --- One case of the deep walk, as a pack of 'test-resources/morph-deep-packs' --- spells it: the program under 'input', wrapped in the fixture object model --- where 'model' says so and run against the fixture Ξ» functions where 'atoms' --- does, entered at 'location' and answering either the program under 'result' --- or the failure under 'fails'. -data DeepPack = DeepPack +-- One case of 𝔻, as a pack of 'test-resources/dataization-packs' spells it: the +-- program under 'input', wrapped in the fixture object model where 'model' says +-- so and run against the fixture Ξ» functions where 'atoms' does, entered at +-- 'location' and answering either the bytes under 'result' or the failure under +-- 'fails'. +data DataizePack = DataizePack { location :: Maybe String , input :: String , model :: Maybe Bool , atoms :: Maybe Bool - , partial :: Maybe Bool , result :: Maybe String , fails :: Maybe String } deriving (Generic, Show, FromJSON) --- Walk one such pack with '_deep' on and check what it answers. A pack that --- registers the fixture Ξ» functions fires one under 'node', so it is pending --- where 'node' is not installed. -testDeep :: Registry -> FilePath -> Expectation -testDeep registry pth = do - DeepPack{..} <- Decode.decodeFileThrow pth +-- Dataize one such pack and check what it answers. A pack that registers the +-- fixture Ξ» functions runs an external script, so it is pending where 'node' is +-- not installed. +testDataize :: Registry -> FilePath -> Expectation +testDataize registry pth = do + DataizePack{..} <- Decode.decodeFileThrow pth expr <- parseExpressionThrows (if model == Just True then primitives input else input) loc <- parseExpressionThrows (fromMaybe "Q" location) - let ctx = - (defaultDataizeContext loc) - { _deep = True - , _partial = partial == Just True - , _atoms = if atoms == Just True then registry else emptyRegistry - } + let ctx = (defaultReduceContext loc){_atoms = if atoms == Just True then registry else emptyRegistry} checked :: Expectation checked = case (result, fails) of (Just res, Nothing) -> do - expected <- parseExpressionThrows res - (morphed, _) <- morph expr ctx - morphed `shouldBe` expected + bts <- either (fail . ("cannot read the expected bytes: " ++)) pure (parseBytes res) + (value, _) <- dataize expr ctx + value `shouldBe` Dataized bts (Nothing, Just message) -> - morph expr ctx `shouldThrow` (\err -> message `isInfixOf` show (err :: SomeException)) + dataize expr ctx `shouldThrow` (\err -> message `isInfixOf` show (err :: SomeException)) _ -> expectationFailure "The pack holds neither a single 'result' nor a single 'fails'" if atoms == Just True then withNode checked else checked --- The EO objects the fixture Ξ» functions answer for, declared the way --- 'number.eo' and 'bytes.eo' declare them, so a case below only has to spell --- the expression under Ο†. 'number.eq' is the one operation with no atom of its --- own: EO spells it out of 'L_bytes_eq' (eq.eo), so the fixture composes it the --- same way. Alongside them stand the objects the atoms hand results to: 'string' --- carries what a byte-array complaint would say, while 'true' and 'false' fill --- in for the real bool objects, since the single byte an EO bool dataizes to is --- all these cases assert. Those bytes are EO's own: 'true.eo' asserts --- 'true.as-bytes.eq FF-' and 'bool.eo' branches 'if' over 'FF-' and '00-', so a --- universe copied from here starts with a bool an EO program recognizes. --- 'number.nope' is declared and left out of the registry on purpose: it is the --- Ξ» function that cannot fire, the one '--partial' parks on. -primitives :: String -> String -primitives src = - unlines - [ "[[" - , " bytes -> [[" - , " Ο† -> ?," - , " not -> [[ L> L_bytes_not ]]," - , " eq -> [[ b -> ?, L> L_bytes_eq ]]" - , " ]]," - , " number -> [[" - , " Ο† -> ?," - , " as-bytes -> $.Ο†," - , " plus -> [[ x -> ?, L> L_number_plus ]]," - , " times -> [[ x -> ?, L> L_number_times ]]," - , " div -> [[ x -> ?, L> L_number_div ]]," - , " gt -> [[ x -> ?, L> L_number_gt ]]," - , " eq -> [[ x -> ?, @ -> $.^.as-bytes.eq( x.as-bytes ) ]]," - , " nope -> [[ L> L_number_nope ]]" - , " ]]," - , " string -> [[ Ο† -> ?, as-bytes -> $.Ο† ]]," - , " true -> [[ @ -> [[ D> FF- ]] ]]," - , " false -> [[ @ -> [[ D> 00- ]] ]]," - , " @ -> " ++ src - , "]]" - ] - --- Wrap a hex literal into the bytes object that EO source spells as a bare '20-1F' -raw :: String -> String -raw bts = "Ξ¦.bytes( Ο† ↦ ⟦ Ξ” ‍ " ++ bts ++ " ⟧ )" - --- Dataize an expression against the fixture universe, with the fixture Ξ» --- functions registered. Every such case runs an external script, so it is --- pending where 'node' is not installed. -testAtom :: Registry -> [(String, String, Bytes)] -> Spec -testAtom registry useCases = - forM_ useCases $ \(name, src, res) -> - it name $ - withNode $ do - expr <- parseExpressionThrows (primitives src) - loc <- parseExpressionThrows "Q" - (value, _) <- dataize expr (withAtoms registry (defaultDataizeContext loc)) - value `shouldBe` Dataized res - -- Dataize under '--partial', collecting every report 𝔼 makes on the way, in -- the order it makes them partially :: Registry -> String -> IO ((Outcome, [Rewritten]), [Evaluation]) @@ -182,7 +83,7 @@ expr <- parseExpressionThrows (primitives src) reports <- newIORef [] let ctx = - (withAtoms registry (defaultDataizeContext ExRoot)) + (withAtoms registry (defaultReduceContext ExRoot)) { _partial = True , _saveEval = \report -> modifyIORef' reports (report :) } @@ -190,138 +91,12 @@ collected <- readIORef reports pure (result, reverse collected) --- An atom with no answer yields βŠ₯, which stops the whole dataization -testStuckAtom :: Registry -> [(String, String)] -> Spec -testStuckAtom registry useCases = - forM_ useCases $ \(name, src) -> - it name $ - withNode $ do - expr <- parseExpressionThrows (primitives src) - loc <- parseExpressionThrows "Q" - dataize expr (withAtoms registry (defaultDataizeContext loc)) - `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException)) - spec :: Spec spec = do -- Every Ξ» function a case may fire comes from the fixture registry, read -- once here: phino carries none of its own (see 'Fixtures'). registry <- runIO fixtureRegistry - -- The top-level 𝕄 entry point, the one the 'morph' command runs: it locates - -- the subterm, threads the whole input expression as the universe and hands - -- back the morphed expression together with the chain that led to it (#1114). - describe "morph" $ do - testMorph - [ ("hands the top formation back untouched under the Q locator", "Q", "[[ D> 00- ]]", "[[ D> 00- ]]") - , -- 𝕄 is total where 𝔻 is not: the 'xi' axiom morphs ΞΎ to βŠ₯, so the run - -- ends with an answer rather than with a failure - ("answers βŠ₯ where no formation is reachable", "Q.x", "[[ x -> $ ]]", "T") - ] - - -- The chain runs oldest step first and carries the rule that produced the - -- step after it, exactly as 'dataize' reports its own, so '--sequence' - -- prints both the same way - it "reports the chain of steps oldest first" $ do - expr <- parseExpressionThrows "[[ D> 00- ]]" - (morphed, chain) <- morph expr (defaultDataizeContext ExRoot) - morphed `shouldBe` expr - map snd chain `shouldBe` [Just "mf", Nothing] - map fst chain `shouldBe` [expr, expr] - - -- 𝕄 never fires a bare Ξ»-formation, so only an atom sitting under a - -- dispatch (the 'ml' rule) can get stuck - describe "a stuck atom under 'ml'" $ do - let stuck :: IO (Expression, Expression) - stuck = (,) <$> parseExpressionThrows "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" <*> parseExpressionThrows "Q.x" - it "fails the run without '_partial'" $ do - (expr, loc) <- stuck - morph expr (defaultDataizeContext loc) - `shouldThrow` (\e -> "Atom 'Sym_arg_0' does not exist" `isInfixOf` show (e :: SomeException)) - - it "is parked in the residue under '_partial'" $ do - (expr, loc) <- stuck - expected <- parseExpressionThrows "[[ L> Sym_arg_0 ]].foo" - (residue, _) <- morph expr (defaultDataizeContext loc){_partial = True} - residue `shouldBe` expected - - -- 𝕄 stops at the first formation 'mf' hands back and leaves its bindings as - -- they were written, since firing a bare Ξ» is 𝔻's business, so a program - -- whose parts nothing demands is never reduced (#1124). The deep walk - -- ('_deep') enters every binding and finishes what 'mf' left, while what no - -- atom touched keeps the shape it was written in and the answer stays a - -- program. - describe "morph with '_deep'" $ do - let resources = "test-resources/morph-deep-packs" - packs <- runIO (allPathsIn resources) - forM_ packs (\pth -> it (makeRelative resources pth) (testDeep registry pth)) - - -- The walk enters a dispatch through its target and fires the box it finds - -- there before 𝕄 is ever asked about the dispatch, while 'ml' demands that - -- Ξ» only where the dispatched attribute is none of the box's own (#1187) - describe "a dispatch naming an attribute of the formation it stands on" $ - it "cannot fire the Ξ» the dispatch does not demand" $ - withShell $ - withServing "printf '{\"id\": %s, \"𝑛\": \"⟦ Ξ” ‍ FF- ⟧\"}\\n' \"$id\"" $ \path -> do - box <- readRegistry path - world <- parseExpressionThrows "[[ foo -> [[ f -> [[ a -> ?, @ -> $.a, L> L_answer ]] ]], x -> Q.foo.f( a -> [[ D> 01- ]] ).@ ]]" - (morphed, _) <- morph world (withAtoms box (defaultDataizeContext ExRoot)){_deep = True} - morphed `shouldBe` world - - describe "morph'" $ - test' - morph' - [ ("[[ D> 00- ]] => [[ D> 00- ]]", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")]) - , ("T => T", ExTermination, ExRoot, ExTermination) - , ("$ => X", ExXi, ExRoot, ExTermination) - , ("Q => X", ExRoot, ExRoot, ExTermination) - , - ( "Q.x (Q -> [[ x -> [[]] ]]) => [[ ρ -> Q ]]" - , ExDispatch ExRoot (AtLabel "x") - , ExFormation [BiTau (AtLabel "x") (ExFormation [])] - , ExFormation [BiTau AtRho (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho])] - ) - , -- A void slot fed a non-absolute argument can never be filled, so 'copy' - -- cannot fire and the application is a stuck normal form. Before #959, - -- 'ma' re-morphed this identical term forever; now the 'mad' axiom - -- morphs it straight to βŠ₯, keeping 𝕄 total. - - ( "[[ x -> ? ]](x -> $.foo) => T" - , ExApplication (ExFormation [BiVoid (AtLabel "x")]) (ArTau (AtLabel "x") (ExDispatch ExXi (AtLabel "foo"))) - , ExRoot - , ExTermination - ) - , -- Same as above but through the alpha-argument sibling 'maad' instead of - -- 'mad': a void slot fed a non-absolute alpha-indexed argument also - -- morphs straight to βŠ₯. - - ( "[[ ^ -> ? ]](Ξ±0 -> $.foo) => T" - , ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) (ExDispatch ExXi (AtLabel "foo"))) - , ExRoot - , ExTermination - ) - , -- 'universe' fires only when the universe 'e' differs from Ξ¦ itself - -- ('not (eq(e, Ξ¦))'); it then normalizes and re-morphs that universe. - -- Here the universe is a plain formation, already a normal form, so - -- re-morphing it lands straight on 'mf' and returns it unchanged. - - ( "Q => [[]] (a universe distinct from Ξ¦) => [[]]" - , ExRoot - , ExFormation [] - , ExFormation [] - ) - ] - - -- 𝕄's first argument is always a normal form reachable through normalization, - -- and every such normal form is covered by some morphing clause (an axiom - -- like 'mf'/'dead'/'xi'/'universe'/'mg' or a recursive rule), so the "no rule - -- matched" fallback never fires along any real derivation. It is still total - -- code, reachable by calling 'morph'' directly (bypassing normalization) on a - -- raw meta 𝑛, an AST node the matcher never binds to any concrete pattern. - describe "morph' fails when no morphing rule matches the term" $ - it "throws instead of looping when handed a bare, unmatched meta" $ - morph' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot) - `shouldThrow` (\e -> "no morphing rule matched" `isInfixOf` show (e :: SomeException)) - -- Symmetric to the morphing fallback above: every normal form 𝔻 actually -- receives is covered by 'delta'/'box'/'fire'/'none' (formations) or 'norm' -- (everything else, disjoint from βŠ₯ and formations), so this fallback is @@ -330,153 +105,17 @@ -- proving the fallback itself is live code, not dead weight. describe "dataize' fails when no dataization rule matches the term" $ it "throws instead of treating the unmatched meta as βŠ₯" $ - dataize' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot) + dataize' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot) `shouldThrow` (\e -> "no dataization rule matched" `isInfixOf` show (e :: SomeException)) - -- 'execBuildTerm's "evaluate" and "morph" cases expose 𝔼 and 𝕄 to the - -- matcher's condition path (guards in 'when'/'having'). No built-in rule's - -- guard actually calls either function, so these error paths β€” reachable only - -- by malformed arguments β€” are exercised here directly through the exported - -- 'execBuildTerm', the same way the matcher would call it. - describe "execBuildTerm 'evaluate'" $ do - let univ = ExFormation [] - ctx = withAtoms registry (defaultDataizeContext ExRoot) - runEvaluate args = execBuildTerm univ ctx "evaluate" args substEmpty - forM_ - [ - ( "the first argument is not a formation" - , [ArgExpression ExRoot, ArgExpression univ] - , "Function evaluate() expects a formation" - ) - , - ( "the formation has no Ξ» binding at all" - , [ArgExpression (ExFormation []), ArgExpression univ] - , "expects a formation with a" - ) - , - ( "a non-Ξ» formation still has other bindings" - , [ArgExpression (ExFormation [BiVoid AtRho]), ArgExpression univ] - , "expects a formation with a" - ) - , - ( "not given exactly two expression arguments" - , [ArgExpression univ] - , "requires exactly 2 expression arguments" - ) - ] - ( \(desc, args, message) -> - it ("throws when " ++ desc) $ - runEvaluate args `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException)) - ) - it "evaluates a Ξ»-bearing formation to the atom's normalized result" $ - withNode $ do - let form = ExFormation [BiLambda (Function "L_bytes_not"), BiTau AtRho (ExFormation [BiDelta (BtOne "00")])] - result <- runEvaluate [ArgExpression form, ArgExpression univ] - case result of - TeExpression expr -> expr `shouldBe` dataBytes (BtOne "FF") - _ -> expectationFailure "expected TeExpression" - - describe "execBuildTerm 'morph'" $ do - let univ = ExFormation [] - ctx = defaultDataizeContext ExRoot - it "throws when not given exactly one expression argument" $ - execBuildTerm univ ctx "morph" [] substEmpty - `shouldThrow` (\e -> "requires exactly 1 expression argument" `isInfixOf` show (e :: SomeException)) - it "morphs a single expression argument to its already-normal form" $ do - result <- execBuildTerm univ ctx "morph" [ArgExpression (ExFormation [BiDelta (BtOne "00")])] substEmpty - case result of - TeExpression expr -> expr `shouldBe` ExFormation [BiDelta (BtOne "00")] - _ -> expectationFailure "expected TeExpression" - - -- An expression that is not part of the program β€” the operand an atom script - -- asks phino to reduce β€” is bound to a synthetic attribute of the universe and - -- that attribute is what 𝔻 is aimed at. This is what the '--inside' option - -- runs, and what phino did internally while the atoms still lived in the - -- binary. - describe "insideUniverse" $ do - let universe = "[[ y -> [[ D> 02- ]] ]]" - reduced src = do - univ <- parseExpressionThrows universe - target <- parseExpressionThrows src - (extended, ctx) <- insideUniverse target univ (defaultDataizeContext ExRoot) - fst <$> dataize extended ctx - it "reduces an expression the program does not contain" $ do - value <- reduced "Q.y" - value `shouldBe` Dataized (BtOne "02") - -- 𝔻 accepts normal forms only, and a dispatch off a formation is not one: - -- 'dot' still applies to it. So the expression is normalized first, which - -- is the whole reason an atom script cannot simply splice it into the - -- universe itself. - it "normalizes what it is handed before 𝔻 sees it" $ do - value <- reduced "[[ x -> [[ D> 01- ]] ]].x" - value `shouldBe` Dataized (BtOne "01") - it "refuses a universe which is not a formation" $ do - target <- parseExpressionThrows "Q.y" - insideUniverse target ExRoot (defaultDataizeContext ExRoot) - `shouldThrow` (\e -> "not a formation" `isInfixOf` show (e :: SomeException)) - - -- 'defaultDataizeContext' runs with '_shuffle' on, so 'morph'' walks the - -- morphing rules in a random order on every step. Every clause is - -- order-independent (the known overlaps were removed in #856 and #860), so the - -- outcome must never depend on that order: morphing each input many times under - -- a shuffling context yields exactly the formation the fixed declaration order - -- does, proving the rules may be applied in any order with the same result. - -- Were a hidden overlap re-introduced, some of these random orders would - -- disagree and 'nub' would collect more than the single expected form. - describe "morphing is order-independent under --shuffle" $ do - let cases = - [ ("a byte formation", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")]) - , ("termination", ExTermination, ExRoot, ExTermination) - , ("xi", ExXi, ExRoot, ExTermination) - , ("the global object", ExRoot, ExRoot, ExTermination) - , - ( "a dispatch over a formation" - , ExDispatch ExRoot (AtLabel "x") - , ExFormation [BiTau (AtLabel "x") (ExFormation [])] - , ExFormation [BiTau AtRho (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho])] - ) - ] - forM_ cases $ \(desc, input, univ, expected) -> - it ("morphs " ++ desc ++ " to the same form across 100 random rule orders") $ do - results <- replicateM 100 (fst . fst <$> morph' (input, (univ, Nothing) :| []) univ emptyState (defaultDataizeContext ExRoot)) - nub results `shouldBe` [expected] - - -- 'md' fires only when its head is not a formation ('not (formation 𝑛)'), - -- so a formation head β€” Ξ»-bearing or not β€” is left to 'ml'/'mf'. The - -- two clauses are mutually exclusive and their order in 'morphing.yaml' - -- cannot change behavior. - describe "morphing 'md' is disjoint from 'ml'" $ do - let rctx = RuleContext (execBuildTerm ExRoot (defaultDataizeContext ExRoot)) - morphRule :: String -> Yaml.MorphRule - morphRule nm = fromMaybe (error ("no morphing rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.morphingRules) - asRule :: Yaml.MorphRule -> Yaml.Rule - asRule r = Yaml.Rule r.name Nothing Nothing r.match ExRoot r.when Nothing Nothing - lambdaFormation = ExFormation [BiLambda (Function "L_dummy"), BiVoid AtRho] - it "does not fire on a Ξ»-bearing formation dispatch" $ do - substs <- matchExpressionWithRule' [substEmpty] (ExDispatch lambdaFormation (AtLabel "x")) (asRule (morphRule "md")) rctx - substs `shouldBe` [] - it "still fires on a non-Ξ»-formation dispatch" $ do - substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (morphRule "md")) rctx - null substs `shouldBe` False - -- ⟦λ ‍ F⟧.a.b.c : 'md' peels .c then .b (their heads are dispatches, - -- not Ξ»-formations, so 'Ξ» βˆ‰ 𝐡' holds), then 'ml' handles the base - -- ⟦λ ‍ F⟧.a and fires the atom. The chain therefore routes - -- md β†’ md β†’ ml; firing the undefined atom 'F' is what - -- raises the error, proving the base Ξ»-formation reached 'ml'. - it "drills a chained Ξ»-formation dispatch down to the base 'ml'" $ do - let base = ExFormation [BiLambda (Function "F")] - chain = ExDispatch (ExDispatch (ExDispatch base (AtLabel "a")) (AtLabel "b")) (AtLabel "c") - morph' (chain, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot) - `shouldThrow` (\e -> "Atom 'F' does not exist" `isInfixOf` show (e :: SomeException)) - -- 'norm' matches the bare meta 𝑛, which unifies with any expression, so it is -- guarded to fire only when 𝑛 is neither a formation ('not (formation 𝑛)', -- left to 'delta'/'box'/'fire'/'none') nor the termination βŠ₯ ('not (𝑛 = βŠ₯)'). -- 𝔻 is partial: βŠ₯ matches no clause and lands on the unmatched-term error -- (#955). The dataization clauses are therefore disjoint and their order in - -- 'dataization.yaml' cannot change behavior. + -- 'resources/dataization' cannot change behavior. describe "dataization 'norm' is disjoint from the specific clauses" $ do - let rctx = RuleContext (execBuildTerm ExRoot (defaultDataizeContext ExRoot)) + let rctx = RuleContext (execBuildTerm ExRoot (defaultReduceContext ExRoot)) dataizeRule :: String -> Yaml.DataizeRule dataizeRule nm = fromMaybe (error ("no dataization rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.dataizationRules) asRule :: Yaml.DataizeRule -> Yaml.Rule @@ -491,7 +130,23 @@ substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (dataizeRule "norm")) rctx null substs `shouldBe` False - describe "dataize" $ + -- Most cases of 𝔻 are four plain values β€” the program, where the run enters + -- it, which Ξ» functions answer it and what it must dataize to β€” so they are + -- packs of 'test-resources/dataization-packs' rather than Haskell (#1201). + -- Which Ξ» functions exist is no longer phino's business: the registry given + -- with '--atoms' decides, and each one runs as an external script (see + -- 'Atoms'). What a pack with 'atoms' on asserts is that the answer of such a + -- script lands in the derivation exactly where a built-in atom's answer used + -- to: 𝔼 normalizes it and 𝔻 carries on. The Ξ» functions themselves are the + -- fixture ones (see 'Fixtures'), and 'number.eq' is composed out of + -- 'L_bytes_eq' the way 'eq.eo' composes it, so the EO-level composition is + -- exercised too. + describe "dataize" $ do + let resources = "test-resources/dataization-packs" + packs <- runIO (allPathsIn resources) + forM_ packs (\pth -> it (makeRelative resources pth) (testDataize registry pth)) + + describe "dataize'" $ test dataize' [ ("[[ D> 00- ]] => 00-", ExFormation [BiDelta (BtOne "00")], ExRoot, BtOne "00") @@ -536,7 +191,7 @@ describe "fails to dataize the terminator" $ do let failsOn desc input = it desc $ - dataize' (input, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot) + dataize' (input, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot) `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException)) failsOn "throws on βŠ₯ instead of mapping it to empty bytes" ExTermination failsOn "throws on a data-less formation, which dataizes βŠ₯" (ExFormation []) @@ -558,7 +213,7 @@ it "fails on the step limit instead of morphing forever" $ withNode $ do expr <- parseExpressionThrows "⟦ @ ↦ ⟦ Ξ» ‍ L_number_div, ρ ↦ ⟦ Ξ” ‍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Ξ” ‍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧" - dataize expr (DataizeContext ExRoot 25 25 (Steps 40 0) False True False False registry buildTerm dontSaveStep dontSaveEval) + dataize expr (ReduceContext ExRoot 25 25 (Steps 40 0) False True False False registry buildTerm reduction dontSaveStep dontSaveEval) `shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException)) -- A budget spent on a cycle is a stuck site just as an atom that cannot @@ -567,7 +222,7 @@ it "parks the step limit as a residual with --partial" $ withNode $ do expr <- parseExpressionThrows "⟦ @ ↦ ⟦ Ξ» ‍ L_number_div, ρ ↦ ⟦ Ξ” ‍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Ξ” ‍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧" - (outcome, _) <- dataize expr (DataizeContext ExRoot 25 25 (Steps 40 0) False True True False registry buildTerm dontSaveStep dontSaveEval) + (outcome, _) <- dataize expr (ReduceContext ExRoot 25 25 (Steps 40 0) False True True False registry buildTerm reduction dontSaveStep dontSaveEval) case outcome of Residual _ -> pure () Dataized bts -> expectationFailure ("expected a residual, dataized to " ++ show bts) @@ -586,7 +241,7 @@ it "fails on it without the flag, naming the unknown atom" $ withNode $ do expr <- parseExpressionThrows (primitives "2.times(3).nope") - dataize expr (withAtoms registry (defaultDataizeContext ExRoot)) + dataize expr (withAtoms registry (defaultReduceContext ExRoot)) `shouldThrow` (\e -> "Atom 'L_number_nope' does not exist" `isInfixOf` show (e :: SomeException)) it "leaves the application of the unregistered atom in place" $ withNode $ do @@ -624,21 +279,21 @@ map (._function) reports `shouldBe` ["L_number_times"] it "stops on the terminator βŠ₯ as before, since a wrong operand is not a stuck atom" $ withNode $ do - expr <- parseExpressionThrows (primitives ("5.plus( " ++ raw "--" ++ " )")) - dataize expr ((withAtoms registry (defaultDataizeContext ExRoot)){_partial = True}) + expr <- parseExpressionThrows (primitives "5.plus( Ξ¦.bytes( Ο† ↦ ⟦ Ξ” ‍ -- ⟧ ) )") + dataize expr ((withAtoms registry (defaultReduceContext ExRoot)){_partial = True}) `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException)) - describe "DataizeContext's --max-depth/--max-cycles reach into the normalization it splices in" $ do + describe "ReduceContext's --max-depth/--max-cycles reach into the normalization it splices in" $ do let boxed = "[[ @ -> [[ D> 00- ]] ]]" forM_ [ ( "--max-cycles" - , DataizeContext ExRoot 25 0 (Steps 250 0) True True False False emptyRegistry buildTerm dontSaveStep dontSaveEval + , ReduceContext ExRoot 25 0 (Steps 250 0) True True False False emptyRegistry buildTerm reduction dontSaveStep dontSaveEval , "--max-cycles=0" ) , ( "--max-depth" - , DataizeContext ExRoot 0 25 (Steps 250 0) True True False False emptyRegistry buildTerm dontSaveStep dontSaveEval + , ReduceContext ExRoot 0 25 (Steps 250 0) True True False False emptyRegistry buildTerm reduction dontSaveStep dontSaveEval , "--max-depth=0" ) ] @@ -648,8 +303,8 @@ dataize expr ctx `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException)) ) forM_ - [ ("--max-cycles", DataizeContext ExRoot 25 0 (Steps 250 0) False True False False emptyRegistry buildTerm dontSaveStep dontSaveEval) - , ("--max-depth", DataizeContext ExRoot 0 25 (Steps 250 0) False True False False emptyRegistry buildTerm dontSaveStep dontSaveEval) + [ ("--max-cycles", ReduceContext ExRoot 25 0 (Steps 250 0) False True False False emptyRegistry buildTerm reduction dontSaveStep dontSaveEval) + , ("--max-depth", ReduceContext ExRoot 0 25 (Steps 250 0) False True False False emptyRegistry buildTerm reduction dontSaveStep dontSaveEval) ] ( \(flag, ctx) -> it ("does not throw without --depth-sensitive even once " ++ flag ++ " is exhausted") $ do @@ -675,7 +330,7 @@ withNode $ do expr <- parseExpressionThrows (primitives "5.plus(6)") loc <- parseExpressionThrows "Q" - (_, chain) <- dataize expr (withAtoms registry (defaultDataizeContext loc)) + (_, chain) <- dataize expr (withAtoms registry (defaultReduceContext loc)) let orphans = nub [label | (_, Just label) <- chain, label `notElem` allowed] unless (null orphans) @@ -695,7 +350,7 @@ let labelsOf loc src = do expr <- parseExpressionThrows src loc' <- parseExpressionThrows loc - (_, chain) <- dataize expr (withAtoms registry (defaultDataizeContext loc')) + (_, chain) <- dataize expr (withAtoms registry (defaultReduceContext loc')) pure [label | (_, Just label) <- chain] it "dataizes 5.plus(6) through the expected rules" $ withNode $ do @@ -723,133 +378,3 @@ it "dataizes a located reference through the expected rules" $ do labels <- labelsOf "Q.foo.bar" "[[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]" labels `shouldBe` ["contextualize", "md", "dot", "copy", "mf", "delta"] - -- The 'none' rule dataizes βŠ₯ (𝔻(⟦⟧) β†’ 𝔻(βŠ₯)), which matches no clause now - -- that there is no 'end' rule, so an empty formation reduces through one - -- labelled 'dataize' step and then fails: it has nothing to dataize (#955). - it "fails to dataize an empty formation, which dataizes βŠ₯" $ do - expr <- parseExpressionThrows "[[ ]]" - loc <- parseExpressionThrows "Q" - dataize expr (defaultDataizeContext loc) - `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException)) - - -- Every case below reaches its bytes without firing an atom, so none of them - -- needs the registry: what they exercise is the calculus itself. - testDataize - [ - ( "Located" - , "Q.foo.bar" - , unlines - [ "[[" - , " foo -> [[" - , " bar -> [[" - , " @ -> Q.x" - , " ]]" - , " ]]," - , " x -> [[ D> 42- ]]" - , "]]" - ] - , BtOne "42" - ) - , - ( "Five" - , "Q.x" - , unlines - [ "[[" - , " number ↦ ⟦ Ο† ↦ βˆ… ⟧," - , " bytes ↦ ⟦ Ο† ↦ βˆ… ⟧," - , " x -> 5" - , "]]" - ] - , BtMany ["40", "14", "00", "00", "00", "00", "00", "00"] - ) - , -- Dispatching an absent attribute on a Ο†-decorated formation now resolves - -- the inherited attribute through morphing 'mphi' (#973): PHI used to be a - -- normalization rule, but following the decoration is a semantic 𝕄 step, - -- so it moved into 'morphing.yaml'. Here '.t' is missing from the outer - -- formation, so 𝕄 walks the '@' decoration to the parent that defines 't' - -- and dataizes its datum. - - ( "InheritedThroughPhi" - , "Q" - , "[[ @ -> [[ t -> [[ D> 2A- ]] ]] ]].t" - , BtOne "2A" - ) - ] - - -- Which Ξ» functions exist is no longer phino's business: the registry given - -- with '--atoms' decides, and each one runs as an external script (see - -- 'Atoms'). What the cases below assert is that the answer of such a script - -- lands in the derivation exactly where a built-in atom's answer used to: 𝔼 - -- normalizes it and 𝔻 carries on. The Ξ» functions themselves are the fixture - -- ones (see 'Fixtures'), and 'number.eq' is composed out of 'L_bytes_eq' the - -- way 'eq.eo' composes it, so the EO-level composition is exercised too. - describe "atoms come from the registry" $ do - testAtom - registry - [ ("adds two numbers", "5.plus( 6 )", BtMany ["40", "26", "00", "00", "00", "00", "00", "00"]) - , ("multiplies two numbers", "5.times( 6 )", BtMany ["40", "3E", "00", "00", "00", "00", "00", "00"]) - , -- Two firings in a row: 'ml' reduces the head of the second dispatch, - -- which fires the first atom, before the second one is handed its own - -- formation to fire against - ("fires twice down a chain of dispatches", "5.plus( 6 ).plus( 7 )", BtMany ["40", "32", "00", "00", "00", "00", "00", "00"]) - , ("divides a positive dividend", "256.div( 16 )", BtMany ["40", "30", "00", "00", "00", "00", "00", "00"]) - , ("divides by zero into infinity", "2.div( 0 )", BtMany ["7F", "F0", "00", "00", "00", "00", "00", "00"]) - , ("tells 1000 is greater than 200", "1000.gt( 200 )", BtOne "FF") - , ("tells 42 is not greater than 42.5", "42.gt( 42.5 )", BtOne "00") - , ("tells zero is greater than a negative", "0.gt( -5 )", BtOne "FF") - , ("tells 5 equals 5", "5.eq( 5 )", BtOne "FF") - , ("tells 5 is not equal to 6", "5.eq( 6 )", BtOne "00") - , ("inverts bytes", raw "CA-FE-BE-BE" ++ ".not", BtMany ["35", "01", "41", "41"]) - , ("tells equal bytes are equal", raw "CA-FE" ++ ".eq( " ++ raw "CA-FE" ++ " )", BtOne "FF") - , ("tells different bytes are not equal", raw "CA-FE" ++ ".eq( " ++ raw "CA-FF" ++ " )", BtOne "00") - ] - - -- A whole program, not a single operation: every atom on the way is an - -- external script and the run still lands on the bytes EO's own - -- 'Fahrenheit' example lands on - it "dataizes a program whose every operation is an external atom" $ - withNode $ do - expr <- - parseExpressionThrows - ( unlines - [ "[[" - , " bytes -> [[" - , " Ο† -> ?" - , " ]]," - , " number -> [[" - , " Ο† -> ?," - , " as-bytes -> $.Ο†," - , " plus -> [[ x -> ?, L> L_number_plus ]]," - , " times -> [[ x -> ?, L> L_number_times ]]" - , " ]]," - , " @ -> $.c.times(1.8).plus(32)," - , " c -> 25" - , "]]" - ] - ) - loc <- parseExpressionThrows "Q" - (value, _) <- dataize expr (withAtoms registry (defaultDataizeContext loc)) - value `shouldBe` Dataized (BtMany ["40", "53", "40", "00", "00", "00", "00", "00"]) - - -- A name the registry does not carry has no Ξ» function at all: 𝔼 gets - -- stuck on it, which is the only behaviour phino itself is left with - it "gets stuck on a Ξ» function the registry does not carry" $ do - expr <- parseExpressionThrows (primitives "5.nope") - loc <- parseExpressionThrows "Q" - dataize expr (withAtoms registry (defaultDataizeContext loc)) - `shouldThrow` (\e -> "Atom 'L_number_nope' does not exist" `isInfixOf` show (e :: SomeException)) - - -- An operand carrying no number is what an EO number atom answers βŠ₯ to, and - -- dataizing βŠ₯ fails through the terminator path. The judgment is the - -- script's now, so what these cases prove is that a βŠ₯ coming back from a - -- script stops 𝔻 exactly as a built-in βŠ₯ used to. - testStuckAtom - registry - [ ("cannot add a non-numeric operand", "5.plus( " ++ raw "--" ++ " )") - , ("cannot multiply by a non-numeric operand", "5.times( " ++ raw "--" ++ " )") - , ("cannot divide by a non-numeric divisor", "5.div( " ++ raw "--" ++ " )") - , ("cannot compare against a non-numeric threshold", "5.gt( " ++ raw "--" ++ " )") - , -- A byte array whose length is not 8 carries no number either (#1072) - ("cannot add a 5-byte operand", "5.plus( " ++ raw "68-65-6C-6C-6F" ++ " )") - , ("cannot multiply by a 2-byte operand", "5.times( " ++ raw "20-1F" ++ " )") - ] diff --git a/test/Fixtures.hs b/test/Fixtures.hs --- a/test/Fixtures.hs +++ b/test/Fixtures.hs @@ -13,10 +13,13 @@ -- written for the occasion, either run once per fire or kept resident for the -- run. module Fixtures - ( fixtureAtoms + ( defaultReduceContext + , fixtureAtoms , fixtureRegistry + , primitives , resident , withAskingRegistry + , withAtoms , withExecutable , withFixtureRegistry , withLoopingAskRegistry @@ -29,7 +32,8 @@ ) where -import Atoms (Registry, readRegistry) +import AST (Expression) +import Atoms (Registry, emptyRegistry, readRegistry) import Control.Exception (bracket) import Data.Aeson (Value, encode, object, (.=)) import Data.Aeson.Key qualified as Key @@ -38,10 +42,65 @@ import Data.Maybe (isNothing) import Data.Text qualified as T import Data.Text.Encoding (decodeUtf8, encodeUtf8) +import Dataize (reduction) +import Deps (dontSaveEval, dontSaveStep) +import Functions (buildTerm) +import Morph (ReduceContext (..), Steps (..)) import System.Directory (findExecutable, getPermissions, getTemporaryDirectory, removePathForcibly, setOwnerExecutable, setPermissions) import System.IO (Handle, hClose, openBinaryTempFile) import System.Info (os) import Test.Hspec (Expectation, pendingWith) + +-- The context every reduction of a spec starts from. Shuffle is enabled so the +-- suite exercises the order-independence of the morphing and dataization rules +-- (#909): a hidden overlap surfaces as a nondeterministic failure instead of +-- staying silently green. The registry of Ξ» functions is empty, since phino +-- implements none of them: a case that needs an atom to answer brings the +-- fixture registry in through 'withAtoms'. +defaultReduceContext :: Expression -> ReduceContext +defaultReduceContext loc = ReduceContext loc 25 25 (Steps 250 0) False True False False emptyRegistry buildTerm reduction dontSaveStep dontSaveEval + +-- The same context with the fixture Ξ» functions registered +withAtoms :: Registry -> ReduceContext -> ReduceContext +withAtoms registry ctx = ctx{_atoms = registry} + +-- The EO objects the fixture Ξ» functions answer for, declared the way +-- 'number.eo' and 'bytes.eo' declare them, so a case only has to spell the +-- expression under Ο†. 'number.eq' is the one operation with no atom of its +-- own: EO spells it out of 'L_bytes_eq' (eq.eo), so the fixture composes it the +-- same way. Alongside them stand the objects the atoms hand results to: 'string' +-- carries what a byte-array complaint would say, while 'true' and 'false' fill +-- in for the real bool objects, since the single byte an EO bool dataizes to is +-- all these cases assert. Those bytes are EO's own: 'true.eo' asserts +-- 'true.as-bytes.eq FF-' and 'bool.eo' branches 'if' over 'FF-' and '00-', so a +-- universe copied from here starts with a bool an EO program recognizes. +-- 'number.nope' is declared and left out of the registry on purpose: it is the +-- Ξ» function that cannot fire, the one '--partial' parks on. +primitives :: String -> String +primitives src = + unlines + [ "[[" + , " bytes -> [[" + , " Ο† -> ?," + , " not -> [[ L> L_bytes_not ]]," + , " eq -> [[ b -> ?, L> L_bytes_eq ]]" + , " ]]," + , " number -> [[" + , " Ο† -> ?," + , " as-bytes -> $.Ο†," + , " plus -> [[ x -> ?, L> L_number_plus ]]," + , " times -> [[ x -> ?, L> L_number_times ]]," + , " div -> [[ x -> ?, L> L_number_div ]]," + , " gt -> [[ x -> ?, L> L_number_gt ]]," + , " eq -> [[ x -> ?, @ -> $.^.as-bytes.eq( x.as-bytes ) ]]," + , " nope -> [[ L> L_number_nope ]]" + , " ]]," + , " string -> [[ Ο† -> ?, as-bytes -> $.Ο† ]]," + , " true -> [[ @ -> [[ D> FF- ]] ]]," + , " false -> [[ @ -> [[ D> 00- ]] ]]," + , " @ -> " ++ src + , "]]" + ] -- Every Ξ» function the fixture answers for. A name outside this list is -- unregistered, which is how a spec asks for an atom that cannot fire. diff --git a/test/MorphSpec.hs b/test/MorphSpec.hs new file mode 100644 --- /dev/null +++ b/test/MorphSpec.hs @@ -0,0 +1,321 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} + +-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +-- SPDX-License-Identifier: MIT + +module MorphSpec (spec) where + +import AST +import Atoms (Registry, emptyRegistry, readRegistry) +import Control.Exception (SomeException) +import Control.Monad +import Data.Aeson (FromJSON) +import Data.List (find, isInfixOf, nub) +import Data.List.NonEmpty (NonEmpty (..)) +import Data.Maybe (fromMaybe) +import Data.Yaml qualified as Decode +import Dataize (Outcome (..), dataize) +import Deps (Term (TeExpression)) +import Files (allPathsIn) +import Fixtures (defaultReduceContext, fixtureRegistry, primitives, withAtoms, withNode, withServing, withShell) +import GHC.Generics (Generic) +import Matcher (substEmpty) +import Morph (ReduceContext (..), emptyState, execBuildTerm, insideUniverse, morph, morph') +import Parser (parseExpressionThrows) +import Rewriter (Rewritten) +import Rule (RuleContext (RuleContext), matchExpressionWithRule') +import System.FilePath (makeRelative) +import Test.Hspec +import Yaml (ExtraArgument (..)) +import Yaml qualified + +test' :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> String -> ReduceContext -> IO ((a, NonEmpty Rewritten), String)) -> [(String, Expression, Expression, a)] -> Spec +test' func useCases = + forM_ useCases $ \(desc, input, expr, output) -> + it desc $ do + ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultReduceContext ExRoot) + res `shouldBe` output + +-- One case of 𝕄, as a pack of 'test-resources/morph-packs' β€” or, for the deep +-- walk, of 'test-resources/morph-deep-packs' β€” spells it: the program under +-- 'input', wrapped in the fixture object model where 'model' says so and run +-- against the fixture Ξ» functions where 'atoms' does, entered at 'location' and +-- answering either the program under 'result' or the failure under 'fails'. +data MorphPack = MorphPack + { location :: Maybe String + , input :: String + , model :: Maybe Bool + , atoms :: Maybe Bool + , partial :: Maybe Bool + , result :: Maybe String + , fails :: Maybe String + } + deriving (Generic, Show, FromJSON) + +-- Morph one such pack and check what it answers, walking every binding where +-- 'deep' says so, since that is what tells the two pack directories apart. A +-- pack that registers the fixture Ξ» functions fires one under 'node', so it is +-- pending where 'node' is not installed. +testMorph :: Registry -> Bool -> FilePath -> Expectation +testMorph registry deep pth = do + MorphPack{..} <- Decode.decodeFileThrow pth + expr <- parseExpressionThrows (if model == Just True then primitives input else input) + loc <- parseExpressionThrows (fromMaybe "Q" location) + let ctx = + (defaultReduceContext loc) + { _deep = deep + , _partial = partial == Just True + , _atoms = if atoms == Just True then registry else emptyRegistry + } + checked :: Expectation + checked = case (result, fails) of + (Just res, Nothing) -> do + expected <- parseExpressionThrows res + (morphed, _) <- morph expr ctx + morphed `shouldBe` expected + (Nothing, Just message) -> + morph expr ctx `shouldThrow` (\err -> message `isInfixOf` show (err :: SomeException)) + _ -> expectationFailure "The pack holds neither a single 'result' nor a single 'fails'" + if atoms == Just True then withNode checked else checked + +spec :: Spec +spec = do + -- Every Ξ» function a case may fire comes from the fixture registry, read + -- once here: phino carries none of its own (see 'Fixtures'). + registry <- runIO fixtureRegistry + + -- The top-level 𝕄 entry point, the one the 'morph' command runs: it locates + -- the subterm, threads the whole input expression as the universe and hands + -- back the morphed expression together with the chain that led to it (#1114). + describe "morph" $ do + let resources = "test-resources/morph-packs" + packs <- runIO (allPathsIn resources) + forM_ packs (\pth -> it (makeRelative resources pth) (testMorph registry False pth)) + + -- The chain runs oldest step first and carries the rule that produced the + -- step after it, exactly as 'dataize' reports its own, so '--sequence' + -- prints both the same way + it "reports the chain of steps oldest first" $ do + expr <- parseExpressionThrows "[[ D> 00- ]]" + (morphed, chain) <- morph expr (defaultReduceContext ExRoot) + morphed `shouldBe` expr + map snd chain `shouldBe` [Just "mf", Nothing] + map fst chain `shouldBe` [expr, expr] + + -- 𝕄 stops at the first formation 'mf' hands back and leaves its bindings as + -- they were written, since firing a bare Ξ» is 𝔻's business, so a program + -- whose parts nothing demands is never reduced (#1124). The deep walk + -- ('_deep') enters every binding and finishes what 'mf' left, while what no + -- atom touched keeps the shape it was written in and the answer stays a + -- program. + describe "morph with '_deep'" $ do + let resources = "test-resources/morph-deep-packs" + packs <- runIO (allPathsIn resources) + forM_ packs (\pth -> it (makeRelative resources pth) (testMorph registry True pth)) + + -- The walk enters a dispatch through its target and fires the box it finds + -- there before 𝕄 is ever asked about the dispatch, while 'ml' demands that + -- Ξ» only where the dispatched attribute is none of the box's own (#1187) + describe "a dispatch naming an attribute of the formation it stands on" $ + it "cannot fire the Ξ» the dispatch does not demand" $ + withShell $ + withServing "printf '{\"id\": %s, \"𝑛\": \"⟦ Ξ” ‍ FF- ⟧\"}\\n' \"$id\"" $ \path -> do + box <- readRegistry path + world <- parseExpressionThrows "[[ foo -> [[ f -> [[ a -> ?, @ -> $.a, L> L_answer ]] ]], x -> Q.foo.f( a -> [[ D> 01- ]] ).@ ]]" + (morphed, _) <- morph world (withAtoms box (defaultReduceContext ExRoot)){_deep = True} + morphed `shouldBe` world + + describe "morph'" $ + test' + morph' + [ ("[[ D> 00- ]] => [[ D> 00- ]]", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")]) + , ("T => T", ExTermination, ExRoot, ExTermination) + , ("$ => X", ExXi, ExRoot, ExTermination) + , ("Q => X", ExRoot, ExRoot, ExTermination) + , + ( "Q.x (Q -> [[ x -> [[]] ]]) => [[ ρ -> Q ]]" + , ExDispatch ExRoot (AtLabel "x") + , ExFormation [BiTau (AtLabel "x") (ExFormation [])] + , ExFormation [BiTau AtRho (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho])] + ) + , -- A void slot fed a non-absolute argument can never be filled, so 'copy' + -- cannot fire and the application is a stuck normal form. Before #959, + -- 'ma' re-morphed this identical term forever; now the 'mad' axiom + -- morphs it straight to βŠ₯, keeping 𝕄 total. + + ( "[[ x -> ? ]](x -> $.foo) => T" + , ExApplication (ExFormation [BiVoid (AtLabel "x")]) (ArTau (AtLabel "x") (ExDispatch ExXi (AtLabel "foo"))) + , ExRoot + , ExTermination + ) + , -- Same as above but through the alpha-argument sibling 'maad' instead of + -- 'mad': a void slot fed a non-absolute alpha-indexed argument also + -- morphs straight to βŠ₯. + + ( "[[ ^ -> ? ]](Ξ±0 -> $.foo) => T" + , ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) (ExDispatch ExXi (AtLabel "foo"))) + , ExRoot + , ExTermination + ) + , -- 'universe' fires only when the universe 'e' differs from Ξ¦ itself + -- ('not (eq(e, Ξ¦))'); it then normalizes and re-morphs that universe. + -- Here the universe is a plain formation, already a normal form, so + -- re-morphing it lands straight on 'mf' and returns it unchanged. + + ( "Q => [[]] (a universe distinct from Ξ¦) => [[]]" + , ExRoot + , ExFormation [] + , ExFormation [] + ) + ] + + -- 𝕄's first argument is always a normal form reachable through normalization, + -- and every such normal form is covered by some morphing clause (an axiom + -- like 'mf'/'dead'/'xi'/'universe'/'mg' or a recursive rule), so the "no rule + -- matched" fallback never fires along any real derivation. It is still total + -- code, reachable by calling 'morph'' directly (bypassing normalization) on a + -- raw meta 𝑛, an AST node the matcher never binds to any concrete pattern. + describe "morph' fails when no morphing rule matches the term" $ + it "throws instead of looping when handed a bare, unmatched meta" $ + morph' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot) + `shouldThrow` (\e -> "no morphing rule matched" `isInfixOf` show (e :: SomeException)) + + -- 'execBuildTerm's "evaluate" and "morph" cases expose 𝔼 and 𝕄 to the + -- matcher's condition path (guards in 'when'/'having'). No built-in rule's + -- guard actually calls either function, so these error paths β€” reachable only + -- by malformed arguments β€” are exercised here directly through the exported + -- 'execBuildTerm', the same way the matcher would call it. + describe "execBuildTerm 'evaluate'" $ do + let univ = ExFormation [] + ctx = withAtoms registry (defaultReduceContext ExRoot) + runEvaluate args = execBuildTerm univ ctx "evaluate" args substEmpty + forM_ + [ + ( "the first argument is not a formation" + , [ArgExpression ExRoot, ArgExpression univ] + , "Function evaluate() expects a formation" + ) + , + ( "the formation has no Ξ» binding at all" + , [ArgExpression (ExFormation []), ArgExpression univ] + , "expects a formation with a" + ) + , + ( "a non-Ξ» formation still has other bindings" + , [ArgExpression (ExFormation [BiVoid AtRho]), ArgExpression univ] + , "expects a formation with a" + ) + , + ( "not given exactly two expression arguments" + , [ArgExpression univ] + , "requires exactly 2 expression arguments" + ) + ] + ( \(desc, args, message) -> + it ("throws when " ++ desc) $ + runEvaluate args `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException)) + ) + it "evaluates a Ξ»-bearing formation to the atom's normalized result" $ + withNode $ do + let form = ExFormation [BiLambda (Function "L_bytes_not"), BiTau AtRho (ExFormation [BiDelta (BtOne "00")])] + result <- runEvaluate [ArgExpression form, ArgExpression univ] + case result of + TeExpression expr -> expr `shouldBe` dataBytes (BtOne "FF") + _ -> expectationFailure "expected TeExpression" + + describe "execBuildTerm 'morph'" $ do + let univ = ExFormation [] + ctx = defaultReduceContext ExRoot + it "throws when not given exactly one expression argument" $ + execBuildTerm univ ctx "morph" [] substEmpty + `shouldThrow` (\e -> "requires exactly 1 expression argument" `isInfixOf` show (e :: SomeException)) + it "morphs a single expression argument to its already-normal form" $ do + result <- execBuildTerm univ ctx "morph" [ArgExpression (ExFormation [BiDelta (BtOne "00")])] substEmpty + case result of + TeExpression expr -> expr `shouldBe` ExFormation [BiDelta (BtOne "00")] + _ -> expectationFailure "expected TeExpression" + + -- An expression that is not part of the program β€” the operand an atom script + -- asks phino to reduce β€” is bound to a synthetic attribute of the universe and + -- that attribute is what 𝔻 is aimed at. This is what the '--inside' option + -- runs, and what phino did internally while the atoms still lived in the + -- binary. + describe "insideUniverse" $ do + let universe = "[[ y -> [[ D> 02- ]] ]]" + reduced src = do + univ <- parseExpressionThrows universe + target <- parseExpressionThrows src + (extended, ctx) <- insideUniverse target univ (defaultReduceContext ExRoot) + fst <$> dataize extended ctx + it "reduces an expression the program does not contain" $ do + value <- reduced "Q.y" + value `shouldBe` Dataized (BtOne "02") + -- 𝔻 accepts normal forms only, and a dispatch off a formation is not one: + -- 'dot' still applies to it. So the expression is normalized first, which + -- is the whole reason an atom script cannot simply splice it into the + -- universe itself. + it "normalizes what it is handed before 𝔻 sees it" $ do + value <- reduced "[[ x -> [[ D> 01- ]] ]].x" + value `shouldBe` Dataized (BtOne "01") + it "refuses a universe which is not a formation" $ do + target <- parseExpressionThrows "Q.y" + insideUniverse target ExRoot (defaultReduceContext ExRoot) + `shouldThrow` (\e -> "not a formation" `isInfixOf` show (e :: SomeException)) + + -- 'defaultReduceContext' runs with '_shuffle' on, so 'morph'' walks the + -- morphing rules in a random order on every step. Every clause is + -- order-independent (the known overlaps were removed in #856 and #860), so the + -- outcome must never depend on that order: morphing each input many times under + -- a shuffling context yields exactly the formation the fixed declaration order + -- does, proving the rules may be applied in any order with the same result. + -- Were a hidden overlap re-introduced, some of these random orders would + -- disagree and 'nub' would collect more than the single expected form. + describe "morphing is order-independent under --shuffle" $ do + let cases = + [ ("a byte formation", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")]) + , ("termination", ExTermination, ExRoot, ExTermination) + , ("xi", ExXi, ExRoot, ExTermination) + , ("the global object", ExRoot, ExRoot, ExTermination) + , + ( "a dispatch over a formation" + , ExDispatch ExRoot (AtLabel "x") + , ExFormation [BiTau (AtLabel "x") (ExFormation [])] + , ExFormation [BiTau AtRho (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho])] + ) + ] + forM_ cases $ \(desc, input, univ, expected) -> + it ("morphs " ++ desc ++ " to the same form across 100 random rule orders") $ do + results <- replicateM 100 (fst . fst <$> morph' (input, (univ, Nothing) :| []) univ emptyState (defaultReduceContext ExRoot)) + nub results `shouldBe` [expected] + + -- 'md' fires only when its head is not a formation ('not (formation 𝑛)'), + -- so a formation head β€” Ξ»-bearing or not β€” is left to 'ml'/'mf'. The + -- two clauses are mutually exclusive and their order in 'resources/morphing' + -- cannot change behavior. + describe "morphing 'md' is disjoint from 'ml'" $ do + let rctx = RuleContext (execBuildTerm ExRoot (defaultReduceContext ExRoot)) + morphRule :: String -> Yaml.MorphRule + morphRule nm = fromMaybe (error ("no morphing rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.morphingRules) + asRule :: Yaml.MorphRule -> Yaml.Rule + asRule r = Yaml.Rule r.name Nothing Nothing r.match ExRoot r.when Nothing Nothing + lambdaFormation = ExFormation [BiLambda (Function "L_dummy"), BiVoid AtRho] + it "does not fire on a Ξ»-bearing formation dispatch" $ do + substs <- matchExpressionWithRule' [substEmpty] (ExDispatch lambdaFormation (AtLabel "x")) (asRule (morphRule "md")) rctx + substs `shouldBe` [] + it "still fires on a non-Ξ»-formation dispatch" $ do + substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (morphRule "md")) rctx + null substs `shouldBe` False + -- ⟦λ ‍ F⟧.a.b.c : 'md' peels .c then .b (their heads are dispatches, + -- not Ξ»-formations, so 'Ξ» βˆ‰ 𝐡' holds), then 'ml' handles the base + -- ⟦λ ‍ F⟧.a and fires the atom. The chain therefore routes + -- md β†’ md β†’ ml; firing the undefined atom 'F' is what + -- raises the error, proving the base Ξ»-formation reached 'ml'. + it "drills a chained Ξ»-formation dispatch down to the base 'ml'" $ do + let base = ExFormation [BiLambda (Function "F")] + chain = ExDispatch (ExDispatch (ExDispatch base (AtLabel "a")) (AtLabel "b")) (AtLabel "c") + morph' (chain, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot) + `shouldThrow` (\e -> "Atom 'F' does not exist" `isInfixOf` show (e :: SomeException)) diff --git a/test/YamlSpec.hs b/test/YamlSpec.hs --- a/test/YamlSpec.hs +++ b/test/YamlSpec.hs @@ -10,7 +10,7 @@ import Control.Exception (Exception (displayException), SomeException) import Control.Monad import Data.Either (isLeft) -import Data.List (isInfixOf, nub, (\\)) +import Data.List (isInfixOf, nub, sort, (\\)) import Data.Maybe (fromMaybe) import Data.Text qualified as T import Data.Text.Encoding (encodeUtf8) @@ -183,6 +183,24 @@ ++ map (\DataizeRule{name, label} -> fromMaybe name label) dataizationRules ++ map (\ContextualizeRule{name, label} -> fromMaybe name label) contextualizationRules (labels \\ nub labels) `shouldBe` [] + + describe "keeps one rule per file in every rule directory" $ do + -- Each judgment lives in its own directory, one YAML per rule, embedded + -- wholesale by 'embedDir', which sorts by path. The clauses of a judgment + -- are disjoint, so nothing orders them and a file is named after the rule + -- it carries and nothing else. Compare the directory listing against the + -- embedded rule set, position by position. + let named :: FilePath -> IO [String] + named dir = map takeBaseName . sort . filter ((== ".yaml") . takeExtension) <$> allPathsIn dir + morphed <- runIO (named "resources/morphing") + dataized <- runIO (named "resources/dataization") + contextualized <- runIO (named "resources/contextualization") + it "names one morphing file after every morphing rule" $ + morphed `shouldBe` map (\MorphRule{name} -> name) morphingRules + it "names one dataization file after every dataization rule" $ + dataized `shouldBe` map (\DataizeRule{name} -> name) dataizationRules + it "names one contextualization file after every contextualization rule" $ + contextualized `shouldBe` map (\ContextualizeRule{name} -> name) contextualizationRules describe "reserves 𝑛-family metas for normal forms" $ -- π’ž ('contextualize') returns an expression that is not necessarily a normal