packages feed

phino 0.0.142 → 0.0.143

raw patch · 63 files changed

+1451/−523 lines, 63 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

- Replacer: ReplaceCtx :: Int -> ReplaceContext
- Replacer: [_maxDepth] :: ReplaceContext -> Int
- Replacer: newtype ReplaceContext
+ CLI.Helpers: printAnswer :: PrintContext -> Expression -> IO String
+ Deps: EvStall :: Int -> Text -> Evaluation
+ Deps: EvStarved :: Int -> Int -> Judgment -> Expression -> Evaluation
+ Deps: EvStuckOn :: Int -> Text -> Evaluation
+ Filter: exclude' :: Expression -> [Expression] -> Expression
+ Filter: include' :: Expression -> [Expression] -> IO Expression
+ Language: data Language
+ Language: language :: Text -> Either String Language
+ Language: shared :: Language -> Language -> Maybe Text
+ Locator: CanNotFindObjectByLocator :: Expression -> LocatorException
+ Locator: InvalidLocatorProvided :: Expression -> LocatorException
+ Locator: [fqn] :: LocatorException -> Expression
+ Locator: data LocatorException
+ Morph: Stalled :: Text -> Int -> Kept
+ Morph: Unmorphable :: Expression -> ReduceException
+ Morph: counted :: Maybe Memo -> IO Int
+ Morph: starved :: Maybe Memo -> IO Int
- Abridge: abridged :: EXPRESSION -> EXPRESSION
+ Abridge: abridged :: Int -> EXPRESSION -> EXPRESSION
- CLI.Parsers: optAbridged :: Parser Bool
+ CLI.Parsers: optAbridged :: Parser (Maybe Int)
- CLI.Types: OptsDataize :: LogLevel -> Int -> IOFormat -> IOFormat -> SugarType -> Bool -> LineFormat -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> Maybe Acyclic -> Bool -> Int -> Int -> Int -> Maybe Int -> Int -> Maybe Int -> Maybe Int -> [String] -> [String] -> String -> String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe FilePath -> Maybe FilePath -> Bool -> Maybe FilePath -> Maybe FilePath -> OptsDataize
+ CLI.Types: OptsDataize :: LogLevel -> Int -> IOFormat -> IOFormat -> SugarType -> Bool -> LineFormat -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> Maybe Acyclic -> Bool -> Int -> Int -> Int -> Maybe Int -> Int -> Maybe Int -> Maybe Int -> [String] -> [String] -> String -> String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe FilePath -> Maybe FilePath -> Maybe Int -> Maybe FilePath -> Maybe FilePath -> OptsDataize
- CLI.Types: OptsMorph :: LogLevel -> Int -> IOFormat -> IOFormat -> SugarType -> Bool -> LineFormat -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> Bool -> Maybe Acyclic -> Bool -> Int -> Int -> Int -> Maybe Int -> Int -> Maybe Int -> Maybe Int -> [String] -> [String] -> String -> String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe FilePath -> Maybe FilePath -> Bool -> Maybe FilePath -> Maybe FilePath -> OptsMorph
+ CLI.Types: OptsMorph :: LogLevel -> Int -> IOFormat -> IOFormat -> SugarType -> Bool -> LineFormat -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> Bool -> Maybe Acyclic -> Bool -> Int -> Int -> Int -> Maybe Int -> Int -> Maybe Int -> Maybe Int -> [String] -> [String] -> String -> String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe FilePath -> Maybe FilePath -> Maybe Int -> Maybe FilePath -> Maybe FilePath -> OptsMorph
- CLI.Types: PrintCtx :: SugarType -> Bool -> Bool -> LineFormat -> Int -> XmirContext -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Int -> Expression -> Maybe String -> Maybe String -> Maybe String -> IOFormat -> PrintContext
+ CLI.Types: PrintCtx :: SugarType -> Bool -> Maybe Int -> LineFormat -> Int -> XmirContext -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Int -> Expression -> Maybe String -> Maybe String -> Maybe String -> IOFormat -> PrintContext
- CLI.Types: [_abridged] :: OptsMorph -> Bool
+ CLI.Types: [_abridged] :: OptsMorph -> Maybe Int
- CST: BT_CUT :: [String] -> Int -> BYTES
+ CST: BT_CUT :: [String] -> Int -> [String] -> BYTES
- CST: EX_SINGLE :: PAIR -> EXPRESSION -> EXPRESSION
+ CST: EX_SINGLE :: PAIR -> SPACE -> EXPRESSION -> EXPRESSION
- Filter: include :: [Rewritten] -> [Expression] -> [Rewritten]
+ Filter: include :: [Rewritten] -> [Expression] -> IO [Rewritten]
- Morph: Memo :: IORef (Store Kept) -> IORef (Set (Expression, Attribute)) -> Memo
+ Morph: Memo :: IORef (Store (Int, Kept)) -> IORef Int -> IORef Int -> IORef (Set (Expression, Attribute)) -> Memo
- Morph: recalled :: Maybe Memo -> Expression -> IO (Maybe Kept)
+ Morph: recalled :: Maybe Memo -> Expression -> Int -> IO (Maybe Kept)
- Morph: retained :: Maybe Memo -> Expression -> Kept -> IO ()
+ Morph: retained :: Maybe Memo -> Expression -> Int -> Kept -> IO ()
- Replacer: replaceExpressionFast :: ReplaceContext -> ReplaceExpressionFunc
+ Replacer: replaceExpressionFast :: ReplaceExpressionFunc
- Yaml: OpDataize :: Expression -> Operation
+ Yaml: OpDataize :: Expression -> Expression -> Operation
- Yaml: OpMorph :: Expression -> Operation
+ Yaml: OpMorph :: Expression -> Expression -> Operation

Files

README.md view
@@ -314,8 +314,8 @@ answers, which is what makes the value the term carries unknown. Firing it is therefore the same question as firing a λ name the `--symbolic` file does not carry, and gets the same answer: 𝔼 stops there, the protocol records the site as-`?(𝜎1)`, and `--partial` leaves the term where it stands. Dispatching an-attribute off a symbol — `⟦ λ ⤍ 𝜎1 ⟧.plus( 5 )` — therefore taints its own+`unanswered(𝜎1)`, and `--partial` leaves the term where it stands. Dispatching+an attribute off a symbol — `⟦ λ ⤍ 𝜎1 ⟧.plus( 5 )` — therefore taints its own binding and nothing else; what stands beside it still computes. In an answer, a bare `𝜎` asks for a fresh one, minted as the firing happens and numbered by the run, so no two unknowns are ever spelled alike. Minting starts after the symbols@@ -484,8 +484,8 @@ reader never has to open the `--symbolic` file beside the protocol and match every line by λ name and meta number. -`?(…)` is a λ name no entry answers, standing where the block of its firing-would have stood. Nothing fired, so nothing opens under it. The line is+`unanswered(…)` is a λ name no entry answers, standing where the block of its+firing would have stood. Nothing fired, so nothing opens under it. The line is commented with the judgment that asked and the formation it was asking about, `𝕄(L_none:λ)`, the way an operand line is commented with the term it was reduced from: 𝔼 is fired by the `ml` rule of morphing and by the `fire` rule@@ -515,7 +515,7 @@       𝛿2.1 := 40-18-00-00-00-00-00-00  # 𝔻(ξ.x)       𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ )  # 𝑛       𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧  # 𝕄(𝑛.1.1)-    ?(L_number_nope)  # 𝔻(L_number_nope:λ)+    unanswered(L_number_nope)  # 𝔻(L_number_nope:λ) ```  <!-- markdownlint-enable MD013 -->@@ -524,6 +524,29 @@ residue instead of failing: what `phino` could not decide is a property of the program and not of the option that decides what to do about it. +Three more lines say why a firing gave no answer.+`stuck(L_outer)` is the last line of a firing that got stuck, naming the λ+function it got stuck on, which is seldom the one `unanswered(…)` names: that+one is written where it was asked for, and this one closes every firing the+failure passed on its way out.+`stall(L_outer)` stands under a firing that `--acyclic=plausible` answered+with the stall an earlier firing of the same formation kept, so a told stall+never reads as a fresh firing that wrote nothing.+`starved(4)  # 𝔻(Φ.a🌵1)` is where `--max-steps=4` ran out, commented with the+judgment and the site the reduction stood at, whether or not `--partial` goes+on to park it:++```text+𝕄(Φ.x)+  𝔼(L_outer)  # 𝕄(Φ.x)+    𝔼(L_outer)  # 𝔻(Φ.a🌵0)+      starved(4)  # 𝔻(Φ.a🌵1)+    stuck(L_outer)+```++The markup spells them `<unfinished λ="L_outer"/>`, `<stall λ="L_outer"/>`+and `<starved limit="4" by="dataize" at="Φ.a🌵1"/>`.+ Every term is 𝜑 on a single line, whatever `--output` and `--flat` say about the result of the run, so a program reading the protocol back never has to know what the run printed. The file is truncated at the beginning of every run, so@@ -695,9 +718,9 @@ 𝔻, `<morph>` for a 𝕄 — with `at` naming the term it was aimed at, which is what the text format opens with as `𝔻(Φ)`. `<evaluate>` is one firing of 𝔼, `λ` naming the entry that answered it, `by` naming the judgment that asked for the-firing — the same word the root is named after and a `<stuck>` carries — and-`at` naming the site it was fired at. The text format writes those two as the-comment of its line, `𝔻(Φ)`.+firing — the same word the root is named after and an `<unanswered>` carries —+and `at` naming the site it was fired at. The text format writes those two as+the comment of its line, `𝔻(Φ)`. `<formation at="Φ" term="⟦ … ⟧">` is a formation 𝔻 got into through `box`, which the text format writes as `formation(⟦ … ⟧)  # 𝔻(Φ)`: `at` names the site it was entered at and `term` holds the formation. Whatever the `φ` body@@ -757,9 +780,9 @@ since the symbol it answers with comes from a `join` line and stands in a `<joined>` of its own. -A λ name no entry answers is `<stuck λ="…">`, standing where its `<evaluate>`-would have stood with the formation 𝔼 was fired against as its text and the-judgment that asked in its `by` attribute, where the text format writes+A λ name no entry answers is `<unanswered λ="…">`, standing where its+`<evaluate>` would have stood with the formation 𝔼 was fired against as its text+and the judgment that asked in its `by` attribute, where the text format writes the letter of it. A firing that happened while an operand of another was being reduced is an `<evaluate>` inside the one that asked, which is what the deeper indentation means in the text. Elements are written as the run goes and@@ -791,7 +814,7 @@       <built meta="𝑛.1.1">Φ.number( φ ↦ 𝜎1:λ )</built>       <answer meta="𝑛.1.2">⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧</answer>     </evaluate>-    <stuck λ="L_number_nope" by="dataize">L_number_nope:λ</stuck>+    <unanswered λ="L_number_nope" by="dataize">L_number_nope:λ</unanswered>   </formation> </dataize> ```@@ -803,9 +826,11 @@ A formation carrying a whole object is written flat on one line, so a real run fills the protocol with lines tens of thousands of characters long. The `--abridged` option shortens every term the protocol writes, in the text and-the XML alike: a formation longer than sixty characters keeps its `φ`, `Δ` and-`λ` bindings and folds the rest into a count, and a byte string longer than-eight bytes keeps its first four bytes and its length. The result the run+the XML alike: a formation longer than sixty-four characters keeps its `φ`,+`Δ` and `λ` bindings and folds the rest into a count, and a byte string longer+than eight bytes keeps its first two bytes and its last two, with the count of+the bytes cut out between them. The width is a value of the option,+`--abridged=120`, for a run that can read longer lines. The result the run prints stays whole, and the option is refused without `--protocol`:  <!-- markdownlint-disable MD013 -->@@ -824,7 +849,7 @@     --sweet --hide-rho wide.phi $ cat wide.txt 𝔻(Φ.t)-  formation(⟦ φ ↦ 48-65-6C-6C-...(12b):Δ, +3 attrs ⟧)  # 𝔻(Φ.t)+  formation(⟦ φ ↦ 48-65-..(8b)..-6C-64:Δ, +3 ⟧)  # 𝔻(Φ.t) ```  <!-- markdownlint-enable MD013 -->@@ -883,7 +908,8 @@ it was reduced — the symbol it came to sits in the hidden `ρ` of the residual program — while `as-bool` names a λ function no entry answers, so it stays in place as a normal-form subterm. A stuck site opens no block in the-`--protocol` file, since nothing fired there, and stands in it as `?(…)`:+`--protocol` file, since nothing fired there, and stands in it as+`unanswered(…)`:  <!-- markdownlint-disable MD013 --> @@ -910,7 +936,7 @@       𝛿2.2 := 40-10-00-00-00-00-00-00  # 𝔻(ξ.x)       𝑛.2.1 := Φ.number( φ ↦ 𝜎2:λ )  # 𝑛       𝑛.2.2 := ⟦ φ ↦ 𝜎2:λ, plus(x) ↦ L_number_plus:λ, times(x) ↦ L_number_times:λ, as-bool ↦ L_number_as_bool:λ ⟧  # 𝕄(𝑛.2.1)-    ?(L_number_as_bool)  # 𝔻(L_number_as_bool:λ)+    unanswered(L_number_as_bool)  # 𝔻(L_number_as_bool:λ) ```  <!-- markdownlint-enable MD013 -->@@ -922,8 +948,8 @@ An operand of a firing that reaches the terminator `⊥`, or a term no dataization rule matches, such as a formation whose `φ` is a void nothing filled, never comes down to data either, and `--partial` parks that firing-the same way, writing the dead end into the protocol as `?(⊥)` with the term-that could not be dataized beside it. Dataization aimed at `⊥` itself still+the same way, writing the dead end into the protocol as `unanswered(⊥)` with the+term that could not be dataized beside it. Dataization aimed at `⊥` itself still fails, with or without `--partial`, since there is no firing to park.  The nested morphing and dataization recursion is bounded by the@@ -994,6 +1020,15 @@ ⊥ ``` +𝕄 maps normal forms to formations and `morph` does not normalize what it is+given, so a term that is not a normal form, such as a dispatch off a formation+with neither `φ` nor `λ`, is reported as a failed run rather than answered:++```bash+$ phino morph --locator=Q.t <<< '⟦ t ↦ ⟦ x ↦ ⟦⟧ ⟧.x ⟧'+[ERROR]: Morphing expects a normal form, but no morphing rule matches: ⟦⟧:x.x+```+ The whole `dataize` option surface applies unchanged — `--symbolic`, `--inside`, `--sequence`, `--headers`, `--steps-dir`, `--protocol`, `--partial`, `--max-steps`, `--shuffle`/`--seed`, `--output`, `--focus` and the@@ -1341,10 +1376,14 @@ two under `a` and no operand line, since nothing was reduced for them, and they are not charged to `--max-firings`, which counts the firings the run made. The formation is compared with everything it carries, `ρ` included, so-a firing on another object is another firing, and a firing that got stuck-keeps nothing, since nothing was answered. A firing cut by the mode on its+a firing on another object is another firing. A firing cut by the mode on its way to an answer keeps the cut, and the next firing of the same formation is-cut at its own site without reducing anything first.+cut at its own site without reducing anything first. A firing that got stuck+keeps the λ function it got stuck on, and the next firing of the same+formation gets stuck at its own site the same way, with nothing reduced+under it, as long as nothing new was answered in between. Once something+was, the formation is fired again, since an operand that could not be+brought down the first time may come down now.  The mode also walks a binding of the world once. Every dispatch on an object of the world copies it, and `--deep` walks every copy, so the tests of an
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.142+version: 0.0.143 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>@@ -55,6 +55,7 @@     Filter     Functions     Lambdas+    Language     LaTeX     Lining     Locator@@ -149,6 +150,7 @@     Fixtures     FunctionsSpec     LambdasSpec+    LanguageSpec     LaTeXSpec     LiningSpec     LocatorSpec@@ -193,6 +195,7 @@     megaparsec >=9.5 && <9.9,     optparse-applicative >=0.18 && <0.20,     phino,+    random >=1.2 && <1.4,     silently >=1.2.5 && <1.3,     text >=2.0.2 && <2.2,     time >=1.12 && <1.17,
resources/dataization/box.yaml view
@@ -17,4 +17,6 @@   - n-result: 𝑛1     normalize: 𝑒3   - d-result: 𝛿1-    dataize: 𝑛1+    dataize:+      - 𝑛1+      - 𝑒1
resources/dataization/fire.yaml view
@@ -11,4 +11,6 @@       - ⟦𝐵1, λ ⤍ 𝑓1, 𝐵2⟧       - 𝑒1   - d-result: 𝛿1-    dataize: 𝑛1+    dataize:+      - 𝑛1+      - 𝑒1
resources/dataization/none.yaml view
@@ -11,4 +11,6 @@     - [𝐵1] premises:   - d-result: 𝛿1-    dataize: ⊥+    dataize:+      - ⊥+      - 𝑒1
resources/dataization/norm.yaml view
@@ -15,6 +15,10 @@           - ⊥ premises:   - n-result: 𝑛2-    morph: 𝑛1+    morph:+      - 𝑛1+      - 𝑒1   - d-result: 𝛿1-    dataize: 𝑛2+    dataize:+      - 𝑛2+      - 𝑒1
resources/morphing/ma.yaml view
@@ -7,8 +7,12 @@ conclusion: 𝑛4 premises:   - n-result: 𝑛2-    morph: 𝑛1+    morph:+      - 𝑛1+      - 𝑒1   - n-result: 𝑛3     normalize: '𝑛2(𝜏1 ↦ 𝑘1)'   - n-result: 𝑛4-    morph: 𝑛3+    morph:+      - 𝑛3+      - 𝑒1
resources/morphing/maa.yaml view
@@ -7,8 +7,12 @@ conclusion: 𝑛4 premises:   - n-result: 𝑛2-    morph: 𝑛1+    morph:+      - 𝑛1+      - 𝑒1   - n-result: 𝑛3     normalize: '𝑛2(α𝑖1 ↦ 𝑘1)'   - n-result: 𝑛4-    morph: 𝑛3+    morph:+      - 𝑛3+      - 𝑒1
resources/morphing/maad.yaml view
@@ -10,4 +10,6 @@     absolute: 𝑛1 premises:   - n-result: 𝑛2-    morph: ⊥+    morph:+      - ⊥+      - 𝑒1
resources/morphing/mad.yaml view
@@ -10,4 +10,6 @@     absolute: 𝑛1 premises:   - n-result: 𝑛2-    morph: ⊥+    morph:+      - ⊥+      - 𝑒1
resources/morphing/md.yaml view
@@ -10,8 +10,12 @@     formation: 𝑛1 premises:   - n-result: 𝑛2-    morph: 𝑛1+    morph:+      - 𝑛1+      - 𝑒1   - n-result: 𝑛3     normalize: '𝑛2.𝜏1'   - n-result: 𝑛4-    morph: 𝑛3+    morph:+      - 𝑛3+      - 𝑒1
resources/morphing/mg.yaml view
@@ -7,4 +7,6 @@ conclusion: 𝑛1 premises:   - n-result: 𝑛1-    morph: ⊥+    morph:+      - ⊥+      - Φ
resources/morphing/ml.yaml view
@@ -14,4 +14,6 @@   - n-result: 𝑛2     normalize: '𝑛1.𝜏1'   - n-result: 𝑛3-    morph: 𝑛2+    morph:+      - 𝑛2+      - 𝑒1
resources/morphing/mphi.yaml view
@@ -18,4 +18,6 @@   - n-result: 𝑛1     normalize: ⟦𝐵1⟧.φ.𝜏1   - n-result: 𝑛2-    morph: 𝑛1+    morph:+      - 𝑛1+      - 𝑒1
resources/morphing/universe.yaml view
@@ -15,4 +15,6 @@   - n-result: 𝑛1     normalize: 𝑒1   - n-result: 𝑛2-    morph: 𝑛1+    morph:+      - 𝑛1+      - 𝑒1
resources/morphing/xi.yaml view
@@ -7,4 +7,6 @@ conclusion: 𝑛1 premises:   - n-result: 𝑛1-    morph: ⊥+    morph:+      - ⊥+      - 𝑒1
resources/normalize/dot.yaml view
@@ -2,14 +2,24 @@ # SPDX-License-Identifier: MIT --- # Dispatch 𝜏1 on a formation: contextualize the dispatched body 𝑛1 and decorate-# it with the whole formation as ρ. The contextualization context is the-# formation WITHOUT the dispatched binding — ⟦𝐵1, 𝐵2⟧, not ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧ —-# so a self-referential ξ inside 𝑛1 (as in ⟦ a ↦ ξ ⟧.a or ⟦ a ↦ ξ.a ⟧.a) no-# longer sees 𝜏1. Such a self-reference then dispatches on a formation that-# lacks 𝜏1 and collapses to ⊥ via stop/null/dd instead of rebuilding the same-# ⟦…, 𝜏1 ↦ 𝑛1, …⟧.𝜏1 term and looping forever. ρ on line 'result' still binds-# the full formation, so sibling and φ-decoration references stay intact — only-# the self-ξ path narrows, keeping normalization (near-)total.+# it with the whole formation as ρ. The context of the contextualization is+# the formation WITHOUT the dispatched binding, ⟦𝐵1, 𝐵2⟧, on purpose: a body+# must not reach itself, so normalization admits no recursion through ξ and+# stays total (#967). A ξ in 𝑛1 therefore stands for a formation one attribute+# short of the one it is written in, and that holds for every path through ξ,+# not only for a path back to 𝜏1:+#   - a body reading 𝜏1 finds no 𝜏1 and answers ⊥ by 'stop', directly as in+#     ⟦ a ↦ ξ.a ⟧.a, or through a sibling as in ⟦ a ↦ ξ.b, b ↦ ξ.a ⟧.a;+#   - a body that is ξ answers the short formation, an ordinary object rather+#     than ⊥: ⟦ a ↦ ξ ⟧.a steps to ⟦⟧(ρ ↦ ⟦ a ↦ ξ ⟧), and+#     ⟦ a ↦ ⟦⟧, b ↦ ξ ⟧.b normalizes to ⟦ a ↦ ⟦⟧ ⟧;+#   - a sibling reached through ξ is the sibling of the short formation, so a+#     sibling that itself holds ξ sees the short formation too:+#     ⟦ a ↦ ξ, b ↦ ξ.a ⟧.b normalizes to ⟦⟧, not to the whole formation+#     (#1438).+# A sibling holding no ξ reads as written: ⟦ a ↦ ⟦ z ↦ Φ ⟧, b ↦ ξ.a ⟧.b+# normalizes to ⟦ z ↦ Φ ⟧. Only the ρ of the answer holds the whole+# formation; the context the body is read in never does. # The rule does not dispatch on a formation holding both λ and Δ: 'dl' says # such a formation is ⊥, and carrying it out into ρ would leave a ρ ↦ ⊥ in a # normal form that 'dl' firing first reduces to ⊥ outright, so the answer would
src/AST.hs view
@@ -433,13 +433,33 @@ -- wrappers the other lacks, so a recursion whose argument gains one on every -- round enters a formation the previous round is within, while a call nested -- inside another is smaller and never holds it. Any symbol stands for any--- other, since each is an opaque unknown. A ρ binding is never looked below,--- since it holds the object a term was taken from and not a term it grew into.+-- other, since each is an opaque unknown, and below the top a symbol also+-- stands for a term that holds no symbol itself, since a round holding an+-- unknown where the previous one held a datum is more general than it (#1491).+-- A ρ binding is never looked below, since it holds the object a term was+-- taken from and not a term it grew into. within :: Expression -> Expression -> Bool within = coupled   where     embedded :: Expression -> Expression -> Bool-    embedded inner outer = coupled inner outer || any (embedded inner) (children outer)+    embedded inner outer = general inner outer || coupled inner outer || any (embedded inner) (children outer)+    general :: Expression -> Expression -> Bool+    general inner (ExFormation [BiLambda (FnSymbol _)]) = plain inner+    general _ _ = False+    plain :: Expression -> Bool+    plain (ExFormation bds) = all plainBinding bds+    plain (ExApplication expr (ArTau AtRho _)) = plain expr+    plain (ExApplication expr (ArTau _ arg)) = plain expr && plain arg+    plain (ExApplication expr (ArAlpha _ arg)) = plain expr && plain arg+    plain (ExDispatch expr _) = plain expr+    plain (ExPhiMeet _ _ expr) = plain expr+    plain (ExPhiAgain _ _ expr) = plain expr+    plain _ = True+    plainBinding :: Binding -> Bool+    plainBinding (BiTau AtRho _) = True+    plainBinding (BiTau _ expr) = plain expr+    plainBinding (BiLambda (FnSymbol _)) = False+    plainBinding _ = True     coupled :: Expression -> Expression -> Bool     coupled (ExFormation left) (ExFormation right) = length left == length right && and (zipWith goBinding left right)     coupled (ExApplication left arg) (ExApplication right arg') = embedded left right && goArgument arg arg'
src/Abridge.hs view
@@ -7,10 +7,11 @@ -- A formation carrying a whole standard object flattens into a line tens of -- thousands of characters long, and every short line of the protocol ends up -- between two walls of text. So a formation whose flat spelling runs past--- sixty characters keeps its salient bindings — φ, Δ and λ, the ones saying--- what the object decorates, holds and fires — and folds the rest into a--- count, '+34 attrs'; a shorter one says little enough to keep them all. A--- byte string past eight bytes keeps its first four and its length, however+-- the width the option names keeps its salient bindings — φ, Δ and λ, the+-- ones saying what the object decorates, holds and fires — and folds the rest+-- into a count, '+34'; a shorter one says little enough to keep them all. A+-- byte string past eight bytes keeps its first two and its last two, with the+-- count of the bytes cut out between them, '00-00-..(45b)..-FF-EE', however -- short the formation holding it, so a wide Δ never blows a line either. The -- metas of a rule are kept, since they stand for bindings and are none. The -- arguments of an application are never folded, since they are what the@@ -22,15 +23,15 @@ import Lining (toSingleLine) import Render (render) -abridged :: EXPRESSION -> EXPRESSION-abridged = goExpr+abridged :: Int -> EXPRESSION -> EXPRESSION+abridged width = goExpr   where     goExpr :: EXPRESSION -> EXPRESSION     goExpr expr@EX_FORMATION{..}       | short expr = EX_FORMATION lsb eol tab (goIntact binding) eol' tab' rsb       | otherwise = EX_FORMATION lsb eol tab (goBinding binding) eol' tab' rsb     goExpr expr@EX_SINGLE{..}-      | short expr || salient pair = EX_SINGLE (goPair pair) (goExpr formation)+      | short expr || salient pair = EX_SINGLE (goPair pair) space (goExpr formation)       | otherwise = goExpr formation     goExpr EX_DISPATCH{..} = EX_DISPATCH (goExpr expr) space attr     goExpr EX_APPLICATION{..} = EX_APPLICATION (goExpr expr) space eol tab (goArgument argument) eol' tab' indent@@ -85,11 +86,11 @@     goAppArgs AAS_EMPTY = AAS_EMPTY     goBytes :: BYTES -> BYTES     goBytes (BT_MANY bts)-      | length bts > 8 = BT_CUT (take 4 bts) (length bts)+      | length bts > 8 = BT_CUT (take 2 bts) (length bts - 4) (drop (length bts - 2) bts)     goBytes bts = bts-    -- Whether a formation spelled flat fits in sixty characters.+    -- Whether a formation spelled flat fits in the width.     short :: EXPRESSION -> Bool-    short expr = T.length (render (toSingleLine expr)) <= 60+    short expr = T.length (render (toSingleLine expr)) <= width     -- Whether a binding says what the object decorates, holds or fires.     salient :: PAIR -> Bool     salient PA_TAU{attr = AT_PHI{}} = True
src/CLI/Helpers.hs view
@@ -12,7 +12,7 @@ import CLI.Types import CLI.Validators (invalidCLIArguments) import CST (EXPRESSION)-import Canonizer (canonize)+import Canonizer (canonize, canonizeExpr) import Control.Exception import Control.Monad ((>=>)) import Data.Char (toLower)@@ -171,9 +171,7 @@   pure (P.printExpressionWith shaped expr (_sugar, UNICODE, SINGLELINE, _margin))   where     shaped :: SugarType -> EXPRESSION -> EXPRESSION-    shaped sugar-      | _abridged = abridged . hidden ctx sugar-      | otherwise = hidden ctx sugar+    shaped sugar = maybe id abridged _abridged . hidden ctx sugar  -- The same, in canonical 𝜑 rather than in the sugar the run prints with. The -- operand a protocol line names is the term an entry of the '--symbolic' file@@ -244,6 +242,12 @@       where         prefixed :: String -> String -> String         prefixed = printf "\n%s\n%s"++-- Render the one answer a run of 𝕄 or 𝔻 hands back the way 'printRewrittens'+-- renders a step: canonized under '--canonize', then narrowed to '--focus'+-- (#1441).+printAnswer :: PrintContext -> Expression -> IO String+printAnswer ctx@PrintCtx{..} expr = printFocused ctx (if _canonize then canonizeExpr expr else expr)  -- Render one expression in the output format, narrowed to the '--focus' -- sub-expression when one is given.
src/CLI/Parsers.hs view
@@ -284,14 +284,19 @@         )     ) -optAbridged :: Parser Bool+optAbridged :: Parser (Maybe Int) optAbridged =-  switch-    ( long "abridged"-        <> help-          "Shorten every 𝜑-expression written to the --protocol file: a formation longer than sixty characters \-          \keeps its φ, Δ and λ bindings and folds the rest into a count, as '+34 attrs', and a byte string \-          \longer than eight bytes keeps its first four bytes and its length, as '00-00-00-00-...(45b)'"+  optional+    ( flag'+        64+        ( long "abridged"+            <> help+              "Shorten every 𝜑-expression written to the --protocol file: a formation longer than the width \+              \keeps its φ, Δ and λ bindings and folds the rest into a count, as '+34', and a byte string \+              \longer than eight bytes keeps its first two bytes and its last two with the count of the bytes \+              \between them, as '00-00-..(45b)..-FF-EE'; the width is 64 characters unless given as --abridged=WIDTH"+        )+        <|> option auto (long "abridged" <> metavar "WIDTH" <> internal)     )  optShuffle :: Parser Bool
src/CLI/Runners.hs view
@@ -63,17 +63,16 @@   validateXmirTopLevel _outputFormat expr   seedTaus expr   logDebug (printf "Amount of rewriting cycles across all the rules: %d, per rule: %d" _maxCycles _maxDepth)-  let listing = case (rules, _inputFormat, _outputFormat) of-        ([], XMIR, XMIR) -> (\_ -> escapeXML input)-        ([], _, _) -> (\_ -> escapeXMLText input)-        (_, _, _) -> (\rewritten -> escapeXMLText (P.printExpression' rewritten (_sugarType, UNICODE, _flat, _margin)))+  let listing = case (rules, _inputFormat) of+        ([], PHI) -> (\_ -> escapeXMLText input)+        (_, _) -> (\rewritten -> escapeXMLText (P.printExpression' rewritten (_sugarType, UNICODE, _flat, _margin)))       xmirCtx = XmirContext _omitListing _omitComments _hideRho listing atoms       printCtx = toPrintCtx xmirCtx foc       exclude = (`F.exclude` excluded)       include = (`F.include` included)   save <- saveStepFunc _stepsDir printCtx   (rewrittens, exceeded) <- rewrite expr rules (RewriteContext loc _maxDepth _maxCycles _depthSensitive Nothing buildTerm _must _breakpoint save)-  let rewrittens' = exclude $ include (if _sequence then NE.toList rewrittens else [NE.last rewrittens])+  rewrittens' <- exclude <$> include (if _sequence then NE.toList rewrittens else [NE.last rewrittens])   logDebug (printf "Printing rewritten 𝜑-expression as %s" (show _outputFormat))   exprs <- printRewrittens printCtx (rewrittens', exceeded)   output _targetFile exprs@@ -131,7 +130,7 @@       PrintCtx         _sugarType         _hideRho-        False+        Nothing         _flat         _margin         xmirCtx@@ -181,17 +180,20 @@           heading record printCtx Dataization aiming._locator           dataize universe (started universe) aiming       )-  when _sequence (printRewrittens printCtx (exclude $ include chain, False) >>= putStrLn)-  unless _quiet (printOutcome printCtx outcome >>= putStrLn)+  when _sequence (include chain >>= \shown -> printRewrittens printCtx (exclude shown, False) >>= putStrLn)+  unless _quiet (printOutcome printCtx (\residue -> (`F.exclude'` excluded) <$> F.include' residue included) outcome >>= putStrLn)   where     -- The bytes the run reached or, when '--partial' let it end on a λ function     -- that could not fire, the residual program, rendered like a rewriting-    -- result: in the output format, narrowed to '--focus'.-    printOutcome :: PrintContext -> Outcome -> IO String-    printOutcome _ (Dataized bytes) = pure (P.printBytes bytes)-    printOutcome ctx (Residual residue) = do+    -- result: narrowed by '--show' and '--hide', canonized, in the output+    -- format, narrowed to '--focus'.+    printOutcome :: PrintContext -> (Expression -> IO Expression) -> Outcome -> IO String+    printOutcome _ _ (Dataized bytes) = pure (P.printBytes bytes)+    printOutcome ctx narrowed (Residual residue) = do       logDebug "Dataization got stuck on a λ function that cannot fire, printing the residual program (--partial)"-      printFocused ctx residue+      answer <- narrowed residue+      validateXmirTopLevel _outputFormat answer+      printAnswer ctx answer     validateOpts :: IO ()     validateOpts = do       validateLatexOptions@@ -201,7 +203,7 @@         [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]       validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus       when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")-      when (_abridged && isNothing _protocol) (invalidCLIArguments "The option --abridged requires --protocol, since only the protocol is abridged")+      when (isJust _abridged && isNothing _protocol) (invalidCLIArguments "The option --abridged requires --protocol, since only the protocol is abridged")       when         (isJust _inside && _locator /= "Q")         (invalidCLIArguments "The options --inside and --locator cannot be used together, since --inside aims the run at the binding it mints")@@ -267,8 +269,11 @@           heading record printCtx Morphing aiming._locator           morph universe (started universe) aiming       )-  when _sequence (printRewrittens printCtx (exclude $ include chain, False) >>= putStrLn)-  unless _quiet (printFocused printCtx morphed >>= putStrLn)+  when _sequence (include chain >>= \shown -> printRewrittens printCtx (exclude shown, False) >>= putStrLn)+  unless _quiet $ do+    answer <- (`F.exclude'` excluded) <$> F.include' morphed included+    validateXmirTopLevel _outputFormat answer+    printAnswer printCtx answer >>= putStrLn   where     validateOpts :: IO ()     validateOpts = do@@ -279,7 +284,7 @@         [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]       validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus       when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")-      when (_abridged && isNothing _protocol) (invalidCLIArguments "The option --abridged requires --protocol, since only the protocol is abridged")+      when (isJust _abridged && isNothing _protocol) (invalidCLIArguments "The option --abridged requires --protocol, since only the protocol is abridged")       when         (isJust _inside && _locator /= "Q")         (invalidCLIArguments "The options --inside and --locator cannot be used together, since --inside aims the run at the binding it mints")@@ -356,7 +361,7 @@       PrintCtx         _sugarType         False-        False+        Nothing         _flat         _margin         xmirCtx
src/CLI/Types.hs view
@@ -19,7 +19,7 @@ data PrintContext = PrintCtx   { _sugar :: SugarType   , _hideRho :: Bool-  , _abridged :: Bool+  , _abridged :: Maybe Int   , _line :: LineFormat   , _margin :: Int   , _xmirCtx :: XmirContext@@ -119,7 +119,7 @@   , _inside :: Maybe String   , _stepsDir :: Maybe FilePath   , _protocol :: Maybe FilePath-  , _abridged :: Bool+  , _abridged :: Maybe Int   , _symbolic :: Maybe FilePath   , _inputFile :: Maybe FilePath   }@@ -167,7 +167,7 @@   , _inside :: Maybe String   , _stepsDir :: Maybe FilePath   , _protocol :: Maybe FilePath-  , _abridged :: Bool+  , _abridged :: Maybe Int   , _symbolic :: Maybe FilePath   , _inputFile :: Maybe FilePath   }
src/CST.hs view
@@ -76,7 +76,7 @@   | BT_MANY [String]   | BT_META META   | BT_PIPED BYTES -- bytes wrapped in vertical pipes, as the eolang LaTeX package expects-  | BT_CUT [String] Int -- the first bytes of a long string and its length in bytes, as '--abridged' spells it (#1465)+  | BT_CUT [String] Int [String] -- the first bytes of a long string, the count of the bytes cut out of it and its last bytes, as '--abridged' spells it (#1465)   deriving (Eq, Show)  data META_HEAD@@ -137,7 +137,7 @@   | PA_DELTA' {bytes :: BYTES} -- ASCII version of PA_DELTA   | PA_META_DELTA {meta :: META}   | PA_META_DELTA' {meta :: META} -- ASCII version of PA_META_DELTA-  | PA_FOLDED {count :: Int} -- the bindings '--abridged' folded away, as '+34 attrs' (#1465)+  | PA_FOLDED {count :: Int} -- the bindings '--abridged' folded away, as '+34' (#1465)   deriving (Eq, Show)  newtype APP_BINDING = APP_BINDING {pair :: PAIR}@@ -187,7 +187,7 @@   | EX_PHI_MEET {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION}   | EX_PHI_AGAIN {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION}   | EX_BYTES {bytes :: BYTES} -- bare data 𝛿, a rendering-only terminal chain node (see #980)-  | EX_SINGLE {pair :: PAIR, formation :: EXPRESSION} -- one-binding formation as 'FF-:Δ' or 'ξ.a:φ', with its full form (see #1385)+  | EX_SINGLE {pair :: PAIR, space :: SPACE, formation :: EXPRESSION} -- one-binding formation as 'FF-:Δ' or 'ξ.a:φ', with its full form (see #1385)   deriving (Eq, Show)  data ATTRIBUTE@@ -356,9 +356,9 @@   -- A formation of a single binding is sugared into its asset, a colon and   -- the attribute, as `FF-:Δ`, `Plus:λ`, `∅:a` or `ξ.a:φ` (see #1385). The   -- full formation is kept next to it, for the notations that have no such-  -- sugar: the salty one, LaTeX and the one '--hide-rho' strips.+  -- sugar: the salty one and the one '--hide-rho' strips.   toCST (ExFormation bds) ctx@(tabs, eol) =-    maybe full (`EX_SINGLE` full) (single bds)+    maybe full (\sole -> EX_SINGLE sole NO_SPACE full) (single bds)     where       full :: EXPRESSION       full =
src/Dataize.hs view
@@ -161,7 +161,7 @@         -- whichever symbol the last datum was manufactured for is forgotten         -- here: only a run ending on a symbol leaves one behind.         pure ((bts, NE.toList seq'), state'{_manufactured = Nothing})-      Just concl@(Y.Premise _ (Y.OpDataize arg)) -> case producer arg rule.premises of+      Just concl@(Y.Premise _ (Y.OpDataize arg universe)) -> case producer arg rule.premises of         -- 𝔻(𝒩(e)) records the producing step (the 'box' contextualization),         -- then normalizes its result back to a normal form before dataizing on,         -- so 𝔻 only ever sees normal forms.@@ -169,16 +169,20 @@           let side = rule.premises `excluding` [concl, normal]           (final, state') <- sides ctx side subst           built <- buildExpressionThrows inner final+          world <- buildExpressionThrows universe final           labelled <- leadsTo seq (labelOf side) built ctx           (normal', seq') <- normalized built labelled ctx-          dataize' (normal', seq') univ state' ctx-        -- 𝔻(𝕄(e)) delegates to the morphing relation, splicing its steps into the-        -- chain before dataizing on.-        Just morphed@(Y.Premise _ (Y.OpMorph inner)) -> do+          dataize' (normal', seq') world state' ctx+        -- 𝔻(𝕄(e)) delegates to the morphing relation, in the universe the+        -- 'morph' premise names, splicing its steps into the chain before+        -- dataizing on in the one the conclusion names.+        Just morphed@(Y.Premise _ (Y.OpMorph inner scene)) -> do           (final, state') <- sides ctx (rule.premises `excluding` [concl, morphed]) subst           built <- buildExpressionThrows inner final-          ((morphed', seq'), state'') <- morph' (built, seq) univ state' ctx-          dataize' (morphed', seq') univ state'' ctx+          stage <- buildExpressionThrows scene final+          ((morphed', seq'), state'') <- morph' (built, seq) stage state' ctx+          world <- buildExpressionThrows universe final+          dataize' (morphed', seq') world state'' ctx         -- The dataize argument is produced with no 'normalize'/'morph' spine to         -- splice: 'fire' by its 'evaluate' side-computation (𝔼 now yields a         -- normal form itself, so no follow-up 'normalize' is needed) and 'none'@@ -189,8 +193,9 @@           let side = rule.premises `excluding` [concl]           (final, state') <- sides ctx side subst           built <- buildExpressionThrows arg final+          world <- buildExpressionThrows universe final           seq' <- leadsTo seq (labelOr (verb concl.operation) side) built ctx-          dataize' (built, seq') univ state' ctx+          dataize' (built, seq') world state' ctx       Just _ -> throwIO (userError (printf "dataization rule '%s' must conclude with a 'dataize' premise" rule.name))     sides :: ReduceContext -> [Y.Premise] -> Subst -> IO (Subst, State)     sides ctx premises subst = foldM (sidePremise univ ctx) (subst, state) premises
src/Deps.hs view
@@ -138,7 +138,7 @@ -- the term the entry wrote, then the normal form 𝕄 makes of it, so the -- morphing between them is a step a reader watches happen rather than a shape a -- term arrives in (#1298). A name no entry answers stands there as--- '?(L_number_nope)', where the block of its firing would have been. A+-- 'unanswered(L_number_nope)', where the block of its firing would have been. A -- formation 𝔻 gets into through its 'box' rule opens a block of its own, -- 'formation(⟦ … ⟧)  # 𝔻(Φ.x)', and what its φ body fires stands under it -- (#1420).@@ -199,6 +199,27 @@     -- rule of morphing and the 'fire' rule of dataization — and which of them     -- asked is what says where in the reduction the site stands (#1300).     EvStuck Int T.Text Judgment Expression+  | -- A firing the memo of '--acyclic=plausible' answered with the stall an+    -- earlier firing of the same formation kept, at the depth of the lines+    -- under the firing, together with the λ function that stall names. It+    -- stands under the firing line the way a 'looped' line stands under a+    -- told cut, so a told stall no longer reads as a fresh firing whose+    -- first operand wrote nothing (#1524).+    EvStall Int T.Text+  | -- The last line of a firing that ended stuck, at the depth of the lines+    -- under the firing, together with the λ function it got stuck on, which+    -- is seldom the one no entry answers: that one is an 'EvStuck', written+    -- where it was asked for, and this one closes every firing the signal+    -- passed on its way out (#1524).+    EvStuckOn Int T.Text+  | -- The step budget running out, at the depth of the frame that asked for+    -- one more step, together with the limit, the judgment of that frame and+    -- the locator of the site it stood at. It is written whether or not+    -- '--partial' goes on to park the term, since a firing the budget starved+    -- otherwise reads the same as one that went well (#1524). The site and not+    -- the term, since the walk of 𝕄 stands at the whole formation it morphs,+    -- which on a real world spells a universe on every line (#1531).+    EvStarved Int Int Judgment Expression   | -- A 'dataize' operand of the firing: the meta it bound, the term the entry     -- wrote under that meta, and the data it came down to, or the symbol that     -- data was manufactured for.@@ -410,7 +431,14 @@       pure (protocol, Just (indented depth (printf "looped(%s)  # %s(%s), %s" form (letter judgment) locator (certainty mode))))     written (EvStuck depth key judgment self) protocol = do       form <- render self-      pure (protocol, Just (indented depth (printf "?(%s)  # %s(%s)" (T.unpack key) (letter judgment) form)))+      pure (protocol, Just (indented depth (printf "unanswered(%s)  # %s(%s)" (T.unpack key) (letter judgment) form)))+    written (EvStall depth key) protocol =+      pure (protocol, Just (indented depth (printf "stall(%s)" (T.unpack key))))+    written (EvStuckOn depth key) protocol =+      pure (protocol, Just (indented depth (printf "stuck(%s)" (T.unpack key))))+    written (EvStarved depth limit judgment site) protocol = do+      locator <- render site+      pure (protocol, Just (indented depth (printf "starved(%d)  # %s(%s)" limit (letter judgment) locator)))     written (EvData depth spelling operand value) protocol = do       datum <- spelled value       line <- commented (printf "%s := %s" (labelled protocol depth spelling) datum) Dataization operand@@ -588,7 +616,17 @@     elements (EvStuck depth key judgment self) nesting = do       form <- render self       let (kept, closers) = closed depth nesting._closing-      pure (nesting{_closing = kept}, closers ++ [indented depth (printf "<stuck λ=\"%s\" by=\"%s\">%s</stuck>" (quoted key) (opened judgment) (escapeXMLText form))])+      pure (nesting{_closing = kept}, closers ++ [indented depth (printf "<unanswered λ=\"%s\" by=\"%s\">%s</unanswered>" (quoted key) (opened judgment) (escapeXMLText form))])+    elements (EvStall depth key) nesting = do+      let (kept, closers) = closed depth nesting._closing+      pure (nesting{_closing = kept}, closers ++ [indented depth (printf "<stall λ=\"%s\"/>" (quoted key))])+    elements (EvStuckOn depth key) nesting = do+      let (kept, closers) = closed depth nesting._closing+      pure (nesting{_closing = kept}, closers ++ [indented depth (printf "<unfinished λ=\"%s\"/>" (quoted key))])+    elements (EvStarved depth limit judgment site) nesting = do+      locator <- render site+      let (kept, closers) = closed depth nesting._closing+      pure (nesting{_closing = kept}, closers ++ [indented depth (printf "<starved limit=\"%d\" by=\"%s\" at=\"%s\"/>" limit (opened judgment) (escapeXML locator))])     elements (EvData depth spelling _ value) nesting = do       record <- stood value       pure (nesting{_closing = kept}, closers ++ [indented depth record])
src/Encoding.hs view
@@ -31,7 +31,7 @@   toASCII EX_META{..} = EX_META (META EXCL E' (rest meta))   toASCII EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toASCII expr)   toASCII EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toASCII expr)-  toASCII EX_SINGLE{..} = EX_SINGLE (toASCII pair) (toASCII formation)+  toASCII EX_SINGLE{..} = EX_SINGLE (toASCII pair) space (toASCII formation)   toASCII expr = expr  instance ToASCII APP_BINDING where
src/Evaluate.hs view
@@ -27,7 +27,7 @@ import Deps (BuildTermMethodS, Evaluation (..), State (..), Term (..)) import Lambdas (Lambda (..), Meta (..), joined, matched, minted, symbolized) import Matcher (MetaValue (..), Subst, combine, substEmpty, substSingle, substSlot)-import Morph (Answer, Kept (..), ReduceContext (..), ReduceException (..), charged, deeper, enter, isLambda, lambda, morph', morphing, normalized, recalled, retained, unparked)+import Morph (Answer, Kept (..), ReduceContext (..), ReduceException (..), Steps (..), charged, counted, deeper, enter, isLambda, lambda, morph', morphing, normalized, recalled, retained, starved, unparked) import Printer (printFunction) import Rule (RuleContext (RuleContext), matchExpressionWithRule') import Text.Printf (printf)@@ -120,9 +120,9 @@ -- so the protocol says what was asked for whether or not '_partial' goes on to -- park the run — once, and not once per attempt: a site '_partial' has parked -- is still standing in the residue the '_deep' walk goes over, so 𝔼 is fired on--- it again and again answers nothing, and a reader counting the '?(…)' lines--- counts the sites 𝔼 got stuck on rather than the passes the walk made over--- them (see '_parked', #1300). A firing an entry answers is charged to the+-- it again and again answers nothing, and a reader counting the 'unanswered(…)'+-- lines counts the sites 𝔼 got stuck on rather than the passes the walk made+-- over them (see '_parked', #1300). A firing an entry answers is charged to the -- '--max-firings' budget before it writes anything, so a run that spent the -- budget leaves no firing open in the protocol (see 'charged', #1472). --@@ -141,17 +141,28 @@     unless (func `elem` caller._parked) (caller._saveEval (EvStuck caller._nesting func caller._judgment form))     throwIO (Stuck func)   Just entry -> do-    known <- recalled caller._memo form+    known <- recalled caller._memo form caller._steps._spent     maybe (made entry) told known   where     -- Fire the entry: charge the firing, reduce every operand, build the     -- answer and keep it for the next firing of the same formation. A     -- recursion cut on the way leaves the firing with no answer, and it is     -- kept instead, as the formation the cut carried, since the next firing-    -- of the same formation would only walk down to it again (#1480).+    -- of the same formation would only walk down to it again (#1480). A+    -- firing that got stuck is kept the same way, as the λ function it got+    -- stuck on, and the memo tells it only until something new is answered+    -- after the firing began, since an operand that could not be brought down+    -- may come down then (#1493, #1495, #1507). A firing inside which the step+    -- budget ran out keeps its stall beside the steps it had spent, and the+    -- memo tells it only to a firing that has spent at least as many, since+    -- at a shallower site the operand may come down (#1514, #1521). A firing+    -- that got stuck ends its block with a 'stuck' line naming the λ function,+    -- whether it is kept or not (#1524).     made :: Lambda -> IO (Expression, State)     made entry = do       charged caller+      stamp <- counted caller._memo+      exhausted <- starved caller._memo       caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site)       let ctx = caller{_nesting = caller._nesting + 1}       outcome <- try $ do@@ -163,22 +174,40 @@         answered ctx entry (reverse conditions) bound''' forked       case outcome of         Right (answer, state') -> do-          retained caller._memo form (Answered answer)+          retained caller._memo form stamp (Answered answer)           pure (snd answer, state')         Left failure -> do-          mapM_ (retained caller._memo form . Looped) (cut failure)+          exhausted' <- starved caller._memo+          mapM_ (retained caller._memo form stamp) (kept (exhausted' /= exhausted) failure)+          mapM_ (caller._saveEval . EvStuckOn (caller._nesting + 1)) (stranded failure)           throwIO failure-    -- The formation a recursion was cut at, where that is what the signal-    -- escaping a firing says.-    cut :: ReduceException -> Maybe Expression-    cut (Looping term) = Just term-    cut (LoopingAt term _ _) = Just term-    cut _ = Nothing+    -- What the memo keeps of a firing that never answered: the formation a+    -- recursion was cut at, or the λ function the firing got stuck on, where+    -- that is what the signal escaping it says, beside the steps the firing+    -- had spent where the step budget ran out inside it and none elsewhere.+    kept :: Bool -> ReduceException -> Maybe Kept+    kept _ (Looping term) = Just (Looped term)+    kept _ (LoopingAt term _ _) = Just (Looped term)+    kept starving (Stuck name) = Just (Stalled name (least starving))+    kept starving (StuckAt name _ _) = Just (Stalled name (least starving))+    kept _ _ = Nothing+    least :: Bool -> Int+    least True = caller._steps._spent+    least False = 0+    -- The λ function a firing got stuck on, where the signal escaping it says+    -- it got stuck, which the protocol writes as the last line of the firing.+    stranded :: ReduceException -> Maybe T.Text+    stranded (Stuck name) = Just name+    stranded (StuckAt name _ _) = Just name+    stranded _ = Nothing     -- Answer the firing with what the first firing of the formation made,     -- written as that one was written: the firing at its site, the term the     -- entry wrote and the normal form it came to, and nothing between them.     -- Where the first firing was cut, the firing is cut again at its own site,     -- with the formation that cut carried and nothing reduced before it.+    -- Where the first firing got stuck, the firing gets stuck again at its own+    -- site, on the same λ function and with nothing reduced under it, and a+    -- 'stall' line under it says so (#1524).     told :: Kept -> IO (Expression, State)     told (Answered (built, normal)) = do       caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site)@@ -189,6 +218,10 @@       caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site)       mapM_ (\mode -> caller._saveEval (EvLooped (caller._nesting + 1) caller._judgment mode term caller._site)) caller._acyclic       throwIO (Looping term)+    told (Stalled name _) = do+      caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site)+      caller._saveEval (EvStall (caller._nesting + 1) name)+      throwIO (Stuck name)     -- Bring one 'dataize' operand down through 𝔻 and bind the bytes meta that     -- names it. An operand 𝔻 could not bring down to data — a site '_partial'     -- parked — leaves the firing with nothing to bind, so it gets stuck like a
src/Filter.hs view
@@ -1,10 +1,13 @@+{-# LANGUAGE TupleSections #-}+ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Filter (include, exclude) where+module Filter (include, include', exclude, exclude') where  import AST-import Data.Maybe (mapMaybe)+import Control.Exception (throwIO)+import Locator (LocatorException (CanNotFindObjectByLocator, InvalidLocatorProvided)) import Misc import Rewriter @@ -32,17 +35,16 @@ exclude rs [] = rs exclude ((expr, maybeRule) : rest) exprs = (exclude' expr exprs, maybeRule) : exclude rest exprs -include' :: Expression -> [Expression] -> Expression-include' expr fqns = case mapMaybe pick fqns of-  [] -> def-  forms -> mergeForms forms+include' :: Expression -> [Expression] -> IO Expression+include' expr [] = pure expr+include' expr fqns+  | ExRoot `elem` fqns = pure expr+  | otherwise = mergeForms <$> traverse pick fqns   where-    def :: Expression-    def = ExFormation []-    pick :: Expression -> Maybe Expression-    pick fqn = do-      attrs <- fqnToAttrs fqn-      includedFormation expr attrs+    pick :: Expression -> IO Expression+    pick fqn = case fqnToAttrs fqn of+      Just attrs -> maybe (throwIO (CanNotFindObjectByLocator fqn)) pure (includedFormation expr attrs)+      _ -> throwIO (InvalidLocatorProvided fqn)     mergeForms :: [Expression] -> Expression     mergeForms forms =       let bds = concat [bs | ExFormation bs <- forms]@@ -61,7 +63,5 @@         includedBindings _ _ = Nothing     includedFormation _ _ = Nothing -include :: [Rewritten] -> [Expression] -> [Rewritten]-include [] _ = []-include rs [] = rs-include ((expr, maybeRule) : rest) exprs = (include' expr exprs, maybeRule) : include rest exprs+include :: [Rewritten] -> [Expression] -> IO [Rewritten]+include rs exprs = traverse (\(expr, maybeRule) -> (,maybeRule) <$> include' expr exprs) rs
src/LaTeX.hs view
@@ -273,9 +273,12 @@   -- one here too, with its name piped the way any other label is (see #1065)   toLaTeX EX_NONFINITE{..} = EX_DISPATCH (EX_GLOBAL global) SPACE (toLaTeX (AT_LABEL (nonFiniteName nonfinite)))   toLaTeX EX_BYTES{..} = EX_BYTES (toLaTeX bytes)-  -- The eolang LaTeX package knows no one-binding sugar, so the full-  -- formation is written instead (see #1385)-  toLaTeX EX_SINGLE{..} = toLaTeX formation+  -- The one-binding sugar is kept, with spaces around its colon, the way+  -- a dispatch keeps them around its dot (see #1527)+  toLaTeX EX_SINGLE{..} = EX_SINGLE (toLaTeX pair) SPACE (toLaTeX formation)+  -- A string is escaped the way a label is, so a '%' in it cannot+  -- comment out the rest of the equation (see #1429)+  toLaTeX EX_STRING{..} = EX_STRING (T.unpack (toLaTeX (T.pack str))) tab rhos   toLaTeX expr = expr  instance ToLaTeX ATTRIBUTE where@@ -359,10 +362,17 @@ instance ToLaTeX T.Text where   toLaTeX = T.concatMap escape     where+      escape '#' = "\\char35{}"       escape '$' = "\\char36{}"+      escape '%' = "\\char37{}"+      escape '&' = "\\char38{}"       escape '@' = "\\char64{}"       escape '^' = "\\char94{}"+      escape '\\' = "\\char92{}"       escape '_' = "\\char95{}"+      escape '{' = "\\char123{}"+      escape '}' = "\\char125{}"+      escape '~' = "\\char126{}"       escape ch = T.singleton ch  instance ToLaTeX SET where@@ -434,7 +444,7 @@     premises     (phinoMorph (renderExpr rule.match) (renderExpr rule.ematch) (conclusionStateName final 1) (conclusionStateName final final) (renderExpr rule.nresult))   where-    (premises, final) = premisesToLatex (renderExpr rule.ematch) rule.premises+    (premises, final) = premisesToLatex rule.premises  -- Render a dataization rule as a LaTeX inference rule, with 𝔻(match, e, s_1) ⟿ -- ⟨conclusion, s_k⟩ as the conclusion below the line, s_k being the final threaded@@ -449,7 +459,7 @@     premises     (phinoDataize (renderExpr rule.match) (renderExpr rule.ematch) (conclusionStateName final 1) (conclusionStateName final final) (renderBytes rule.dresult))   where-    (premises, final) = premisesToLatex (renderExpr rule.ematch) rule.premises+    (premises, final) = premisesToLatex rule.premises  -- Render a contextualization rule as a LaTeX inference rule, with 𝒞(match, c) ⟿ -- c-result as the conclusion below the line. 𝒞 carries no state, so its premises@@ -461,7 +471,7 @@     rule.name     rule.label     Nothing-    (fst (premisesToLatex "e" rule.premises))+    (fst (premisesToLatex rule.premises))     (phinoContextualize (renderExpr rule.match) (renderExpr rule.cmatch) (renderExpr rule.cresult))  -- The state metavariable for index 'n', rendered as s_1, s_2, … to mirror the@@ -482,30 +492,27 @@ -- Render a rule's premises in order, threading the state through them. The rule -- starts in state s_1; each state-changing premise (𝕄, 𝔻, 𝔼) consumes the -- current state and yields the next (s_2, s_3, …), matching how the engine folds--- the state through the premises ('sidePremise' in 'Dataize.hs'). The 'universe'--- is the rule's own 'universe' key, threaded into 𝕄/𝔻 premises (bound by the conclusion)--- rather than a free 'e'. Returns the rendered judgments and the final state--- index, which the conclusion returns.-premisesToLatex :: String -> [Y.Premise] -> ([String], Int)-premisesToLatex universe = go 1+-- the state through the premises ('sidePremise' in 'Dataize.hs'). Returns the+-- rendered judgments and the final state index, which the conclusion returns.+premisesToLatex :: [Y.Premise] -> ([String], Int)+premisesToLatex = go 1   where     go :: Int -> [Y.Premise] -> ([String], Int)     go index [] = ([], index)     go index (premise : rest) = (rendered : more, final)       where-        (rendered, next) = premiseToLatex universe index premise+        (rendered, next) = premiseToLatex index premise         (more, final) = go next rest  -- One premise judgment in state s_index, rendered per its operation. The -- state-changing operations 𝕄 ('morph'), 𝔻 ('dataize') and 𝔼 ('evaluate') consume -- s_index and yield s_index+1 (so they return the bumped index); the rest are--- stateless and leave the index as is. 𝕄 and 𝔻 carry the rule's own 'universe'--- (its 'universe' key) so the premise stays bound by the conclusion instead of naming a--- free 'e'; 𝔼 carries the explicit universe from its own operation.-premiseToLatex :: String -> Int -> Y.Premise -> (String, Int)-premiseToLatex universe index premise = case premise.operation of-  Y.OpMorph arg -> (phinoMorph (renderExpr arg) universe (stateName index) (stateName (index + 1)) (renderExpr (ExMeta premise.result)), index + 1)-  Y.OpDataize arg -> (phinoDataize (renderExpr arg) universe (stateName index) (stateName (index + 1)) (renderBytes (BtMeta premise.result)), index + 1)+-- stateless and leave the index as is. 𝕄, 𝔻 and 𝔼 carry the universe their own+-- operation names, so a premise is typeset as the rule wrote it (#1512).+premiseToLatex :: Int -> Y.Premise -> (String, Int)+premiseToLatex index premise = case premise.operation of+  Y.OpMorph arg universe -> (phinoMorph (renderExpr arg) (renderExpr universe) (stateName index) (stateName (index + 1)) (renderExpr (ExMeta premise.result)), index + 1)+  Y.OpDataize arg universe -> (phinoDataize (renderExpr arg) (renderExpr universe) (stateName index) (stateName (index + 1)) (renderBytes (BtMeta premise.result)), index + 1)   Y.OpNormalize arg -> (phinoNormalize (renderExpr arg) (renderExpr (ExMeta premise.result)), index)   Y.OpEvaluate arg evalUniverse -> (phinoEvaluate (renderExpr arg) (renderExpr evalUniverse) (stateName index) (stateName (index + 1)) (renderExpr (ExMeta premise.result)), index + 1)   Y.OpContextualize arg context -> (phinoContextualize (renderExpr arg) (renderExpr context) (renderExpr (ExMeta premise.result)), index)
src/Lambdas.hs view
@@ -86,6 +86,7 @@ import qualified Data.Text as T import Data.Text.Encoding (encodeUtf8) import qualified Data.Yaml as Yaml+import Language (Language, language, shared) import Logger (logDebug) import Metas (Metas (metas)) import Parser (parseBytes, parseExpression)@@ -366,24 +367,31 @@     unreadable key (_, failure) =       throwIO (BrokenLambdas path (printf "the key '%s' is not a regular expression: %s" (T.unpack key) failure)) +    -- Two keys matching one λ name leave the entry that answers it to the+    -- order the file lists them in, so the file is wrong as soon as there is+    -- such a name, whether or not either key spells it (#1440).     overlaps :: FilePath -> [(Regex, Lambda)] -> IO ()-    overlaps file = check+    overlaps file registered = mapM (spoken . snd) registered >>= check       where-        check :: [(Regex, Lambda)] -> IO ()+        spoken :: Lambda -> IO (Lambda, Language)+        spoken entry =+          either+            (throwIO . BrokenLambdas file . printf "the key '%s' cannot be compared with the other keys: %s" (T.unpack entry._key))+            (pure . (,) entry)+            (language entry._key)+        check :: [(Lambda, Language)] -> IO ()         check [] = pure ()-        check ((first, left) : rest) = do-          mapM_ (pair first left) rest-          check rest-        pair :: Regex -> Lambda -> (Regex, Lambda) -> IO ()-        pair first left (second, right)-          | matchTest first (encodeUtf8 right._key)-              || matchTest second (encodeUtf8 left._key) =-              throwIO-                ( BrokenLambdas-                    file-                    (printf "the keys '%s' and '%s' match some of the same lambda names" (T.unpack left._key) (T.unpack right._key))-                )-          | otherwise = pure ()+        check (first : rest) = mapM_ (pair first) rest >> check rest+        pair :: (Lambda, Language) -> (Lambda, Language) -> IO ()+        pair (left, one) (right, other) =+          maybe+            (pure ())+            ( throwIO+                . BrokenLambdas file+                . printf "the keys '%s' and '%s' match some of the same lambda names, such as '%s'" (T.unpack left._key) (T.unpack right._key)+                . T.unpack+            )+            (shared one other)  -- The entry whose key matches the whole λ name, if any. There is at most one: -- the keys are unique, so a name either has a λ function or has none at all.
+ src/Language.hs view
@@ -0,0 +1,260 @@+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++-- The set of λ names the key of a '--symbolic' entry matches, as the automaton+-- recognizing it, so that two keys can be asked for a name they both match.+-- Testing one key against the text of the other misses a name neither key+-- spells, such as 'L_number_plus' of 'L_[a-z]+_plus' and 'L_number_[a-z]+',+-- and leaves the answer to the order the file lists them in (#1440).+--+-- A key is read as the regular expressions of PCRE that describe a regular+-- language: characters, escapes, classes, the dot, groups, alternation and+-- quantifiers, lazy ones too. What goes beyond that, such as a back reference,+-- a lookaround or an anchor, is refused, since two such keys cannot be told+-- apart for certain. The dot stands for every character but a new line, and+-- '\d', '\w' and '\s' for their ASCII sets, the way PCRE reads them.+module Language (Language, language, shared) where++import Data.Char (isAlphaNum, isDigit)+import qualified Data.Map.Strict as Map+import qualified Data.Set as Set+import Data.Text (Text)+import qualified Data.Text as T+import Text.Printf (printf)+import Text.Read (readMaybe)++-- A set of characters, as sorted and disjoint ranges.+newtype Span = Span [(Char, Char)]++-- A regular expression, as the key spells it.+data Pattern+  = Chars Span+  | Chain [Pattern]+  | Choice [Pattern]+  | Repeat Int (Maybe Int) Pattern++-- A move of the automaton: to a state for free, or on a character of a span.+data Edge+  = Free Int+  | Step Span Int++-- The automaton recognizing the names a key matches, as the edges leaving+-- every state, starting at the state 0 and accepting at the state 1.+newtype Language = Language (Map.Map Int [Edge])++-- The language of a key, or the reason it cannot be read as one.+language :: Text -> Either String Language+language key = do+  (pattern, rest) <- choice (T.unpack key)+  case rest of+    [] -> Right (automaton pattern)+    _ -> Left (printf "the character '%s' is not expected" (take 1 rest))+  where+    choice :: String -> Either String (Pattern, String)+    choice text = do+      (first, rest) <- chain text+      case rest of+        '|' : more -> do+          (other, left) <- choice more+          Right (Choice [first, other], left)+        _ -> Right (first, rest)+    chain :: String -> Either String (Pattern, String)+    chain = go []+      where+        go :: [Pattern] -> String -> Either String (Pattern, String)+        go done text@(char : _)+          | char `elem` ("|)" :: String) = Right (Chain (reverse done), text)+        go done [] = Right (Chain (reverse done), [])+        go done text = do+          (atom, rest) <- single text+          (quantified, left) <- quantifier atom rest+          go (quantified : done) left+    single :: String -> Either String (Pattern, String)+    single ('(' : '?' : ':' : rest) = group rest+    single ('(' : '?' : 'P' : '<' : rest) = group (drop 1 (dropWhile (/= '>') rest))+    single ('(' : '?' : '<' : rest@(char : _))+      | char `notElem` ("=!" :: String) = group (drop 1 (dropWhile (/= '>') rest))+    single ('(' : '?' : _) = Left "a group of that kind cannot be compared"+    single ('(' : rest) = group rest+    single ('[' : rest) = klass rest+    single ('.' : rest) = Right (Chars (complement (Span [('\n', '\n')])), rest)+    single ('\\' : rest) = escape rest >>= \(span', left) -> Right (Chars span', left)+    single (char : rest)+      | char `elem` ("^$" :: String) = Left "an anchor cannot be compared"+      | char `elem` ("*+?" :: String) = Left (printf "the quantifier '%s' quantifies nothing" [char])+      | otherwise = Right (Chars (Span [(char, char)]), rest)+    single [] = Left "the expression ends too early"+    group :: String -> Either String (Pattern, String)+    group text = do+      (inner, rest) <- choice text+      case rest of+        ')' : left -> Right (inner, left)+        _ -> Left "a group is not closed"+    quantifier :: Pattern -> String -> Either String (Pattern, String)+    quantifier atom ('*' : rest) = lazy (Repeat 0 Nothing atom) rest+    quantifier atom ('+' : rest) = lazy (Repeat 1 Nothing atom) rest+    quantifier atom ('?' : rest) = lazy (Repeat 0 (Just 1) atom) rest+    quantifier atom text@('{' : rest) =+      case bounded rest of+        Just (low, high, left) -> lazy (Repeat low high atom) left+        Nothing -> Right (atom, text)+    quantifier atom rest = Right (atom, rest)+    lazy :: Pattern -> String -> Either String (Pattern, String)+    lazy _ ('+' : _) = Left "a possessive quantifier cannot be compared"+    lazy pattern ('?' : rest) = Right (pattern, rest)+    lazy pattern rest = Right (pattern, rest)+    bounded :: String -> Maybe (Int, Maybe Int, String)+    bounded text = do+      let (low, rest) = span isDigit text+      from <- readMaybe low+      case rest of+        '}' : left -> Just (from, Just from, left)+        ',' : more -> do+          let (high, left) = span isDigit more+          case (high, left) of+            ([], '}' : after) -> Just (from, Nothing, after)+            (_, '}' : after) -> readMaybe high >>= \to -> if to < from then Nothing else Just (from, Just to, after)+            _ -> Nothing+        _ -> Nothing+    escape :: String -> Either String (Span, String)+    escape (char : rest)+      | Just span' <- lookup char sets = Right (span', rest)+      | Just literal <- lookup char controls = Right (Span [(literal, literal)], rest)+      | not (isAlphaNum char) = Right (Span [(char, char)], rest)+      | otherwise = Left (printf "the escape '\\%s' cannot be compared" [char])+    escape [] = Left "the expression ends with a backslash"+    sets :: [(Char, Span)]+    sets =+      [ ('d', digits)+      , ('D', complement digits)+      , ('w', word)+      , ('W', complement word)+      , ('s', spaces)+      , ('S', complement spaces)+      ]+    controls :: [(Char, Char)]+    controls = [('t', '\t'), ('n', '\n'), ('r', '\r'), ('f', '\f'), ('e', '\ESC')]+    digits :: Span+    digits = Span [('0', '9')]+    word :: Span+    word = union [Span [('0', '9')], Span [('A', 'Z')], Span [('_', '_')], Span [('a', 'z')]]+    spaces :: Span+    spaces = Span [('\t', '\r'), (' ', ' ')]+    klass :: String -> Either String (Pattern, String)+    klass ('^' : rest) = members rest >>= \(span', left) -> Right (Chars (complement span'), left)+    klass rest = members rest >>= \(span', left) -> Right (Chars span', left)+    members :: String -> Either String (Span, String)+    members (']' : rest) = collect [Span [(']', ']')]] rest+    members rest = collect [] rest+    collect :: [Span] -> String -> Either String (Span, String)+    collect done (']' : rest) = Right (union done, rest)+    collect _ ('[' : ':' : _) = Left "a POSIX class cannot be compared"+    collect done ('\\' : rest) = do+      (span', left) <- escape rest+      case (span', left) of+        (Span [(low, _)], '-' : high : after)+          | high /= ']' -> ranged done low (high : after)+        _ -> collect (span' : done) left+    collect done (low : '-' : high : rest)+      | high /= ']' = ranged done low (high : rest)+    collect done (char : rest) = collect (Span [(char, char)] : done) rest+    collect _ [] = Left "a class is not closed"+    ranged :: [Span] -> Char -> String -> Either String (Span, String)+    ranged done low ('\\' : rest) = do+      (span', left) <- escape rest+      case span' of+        Span [(high, high')] | high == high' -> bound done low high left+        _ -> Left "a range ends at a set of characters"+    ranged done low (high : rest) = bound done low high rest+    ranged _ _ [] = Left "a class is not closed"+    bound :: [Span] -> Char -> Char -> String -> Either String (Span, String)+    bound done low high rest+      | low <= high = collect (Span [(low, high)] : done) rest+      | otherwise = Left "a range runs backwards"++-- A name both languages hold, if there is one, found by walking the two+-- automata side by side until both accept at once.+shared :: Language -> Language -> Maybe Text+shared (Language left) (Language right) = go (Set.singleton (0, 0)) [((0, 0), [])]+  where+    go :: Set.Set (Int, Int) -> [((Int, Int), String)] -> Maybe Text+    go _ [] = Nothing+    go seen (((here, there), name) : rest)+      | here == 1 && there == 1 = Just (T.pack (reverse name))+      | otherwise =+          let fresh = filter ((`Set.notMember` seen) . fst) (moves here there name)+           in go (foldr (Set.insert . fst) seen fresh) (rest ++ fresh)+    moves :: Int -> Int -> String -> [((Int, Int), String)]+    moves here there name =+      [((state, there), name) | Free state <- edges left here]+        ++ [((here, state), name) | Free state <- edges right there]+        ++ [ ((this, that), char : name)+           | Step first this <- edges left here+           , Step second that <- edges right there+           , Just char <- [sample (meet first second)]+           ]+    edges :: Map.Map Int [Edge] -> Int -> [Edge]+    edges table state = Map.findWithDefault [] state table++-- The automaton of a pattern, from the state 0 to the state 1.+automaton :: Pattern -> Language+automaton pattern = Language (Map.fromListWith (flip (++)) [(from, [edge]) | (from, edge) <- snd (build pattern 0 1 2)])+  where+    build :: Pattern -> Int -> Int -> Int -> (Int, [(Int, Edge)])+    build (Chars span') from to next = (next, [(from, Step span' to)])+    build (Chain []) from to next = (next, [(from, Free to)])+    build (Chain [single]) from to next = build single from to next+    build (Chain (first : rest)) from to next =+      let (after, head') = build first from next (next + 1)+          (last', tail') = build (Chain rest) next to after+       in (last', head' ++ tail')+    build (Choice options) from to next =+      foldl+        (\(counter, done) option -> let (counter', made) = build option from to counter in (counter', done ++ made))+        (next, [])+        options+    build (Repeat 0 (Just 0) _) from to next = (next, [(from, Free to)])+    build (Repeat 0 Nothing inner) from to next =+      let (after, made) = build inner next next (next + 1)+       in (after, (from, Free next) : (next, Free to) : made)+    build (Repeat 0 (Just high) inner) from to next =+      build (Choice [Chain [], Chain [inner, Repeat 0 (Just (high - 1)) inner]]) from to next+    build (Repeat low high inner) from to next =+      build (Chain [inner, Repeat (low - 1) (subtract 1 <$> high) inner]) from to next++-- Every character in any of the spans.+union :: [Span] -> Span+union spans = Span (merge (Set.toAscList (Set.fromList (concat [ranges | Span ranges <- spans]))))+  where+    merge :: [(Char, Char)] -> [(Char, Char)]+    merge ((low, high) : (low', high') : rest)+      | low' <= succ' high = merge ((low, max high high') : rest)+    merge (range : rest) = range : merge rest+    merge [] = []+    succ' :: Char -> Char+    succ' char+      | char == maxBound = char+      | otherwise = succ char++-- Every character outside the span.+complement :: Span -> Span+complement (Span ranges) = Span (go minBound ranges)+  where+    go :: Char -> [(Char, Char)] -> [(Char, Char)]+    go from [] = [(from, maxBound)]+    go from ((low, high) : rest)+      | high == maxBound = [(from, pred low) | from < low]+      | otherwise = [(from, pred low) | from < low] ++ go (succ high) rest++-- Every character in both spans.+meet :: Span -> Span -> Span+meet (Span first) (Span second) =+  Span [(max low low', min high high') | (low, high) <- first, (low', high') <- second, max low low' <= min high high']++-- A character of the span, a small letter if it has one, so the name an error+-- quotes reads like a λ name, and nothing if the span is empty.+sample :: Span -> Maybe Char+sample (Span ranges) =+  case [max low 'a' | (low, high) <- ranges, max low 'a' <= min high 'z'] ++ [low | (low, _) <- ranges] of+    char : _ -> Just char+    [] -> Nothing
src/Lining.hs view
@@ -25,7 +25,7 @@   toSingleLine EX_APPLICATION{..} = EX_APPLICATION (toSingleLine expr) space NO_EOL TAB' (toSingleLine argument) NO_EOL TAB' indent   toSingleLine EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSingleLine expr)   toSingleLine EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toSingleLine expr)-  toSingleLine EX_SINGLE{..} = EX_SINGLE (toSingleLine pair) (toSingleLine formation)+  toSingleLine EX_SINGLE{..} = EX_SINGLE (toSingleLine pair) space (toSingleLine formation)   toSingleLine expr = expr  instance ToSingleLine APP_BINDING where
src/Locator.hs view
@@ -4,7 +4,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Locator (locatedExpression, withLocatedExpression) where+module Locator (LocatorException (..), locatedExpression, withLocatedExpression) where  import AST import Control.Exception (Exception, throwIO)
src/Margin.hs view
@@ -37,7 +37,7 @@   withMargin' cfg@(extra, margin) ex@EX_SINGLE{pair = PA_TAU{..}, ..} =     let single = toSingleLine ex         asset = withMargin' (extra, margin - lengthOf attr - 1) expr-     in if lengthOf single + extra <= margin then single else EX_SINGLE (PA_TAU attr arrow asset) (withMargin' cfg formation)+     in if lengthOf single + extra <= margin then single else EX_SINGLE (PA_TAU attr arrow asset) space (withMargin' cfg formation)   withMargin' cfg@(extra, margin) ex@EX_APPLICATION{tab = tab@(TAB indt), ..} =     let single = toSingleLine ex         main = withMargin' cfg expr
src/Morph.hs view
@@ -18,10 +18,11 @@ -- a λ function itself, which is an evaluation — are injected as '_reduce', -- '_evaluate' and '_fire' rather than imported (see 'ReductionFunc' and -- 'EvaluationFunc').-module Morph (Answer, Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, FiringFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), boxed, charged, deeper, emptyState, enter, entering, excluding, execBuildTerm, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, parking, producer, recalled, retained, sidePremise, tallied, universed, unparked, verb) where+module Morph (Answer, Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, FiringFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), boxed, charged, counted, deeper, emptyState, enter, entering, excluding, execBuildTerm, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, parking, producer, recalled, retained, sidePremise, starved, tallied, universed, unparked, verb) where  import AST import Builder (buildExpressionThrows, contextualize, pathOf)+import Control.Applicative ((<|>)) import Control.Exception (Exception, catch, throwIO, try) import Control.Monad (foldM, unless, when) import Data.IORef (IORef, modifyIORef', newIORef, readIORef, writeIORef)@@ -29,7 +30,7 @@ import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE import qualified Data.Map.Strict as Map-import Data.Maybe (fromMaybe, isJust)+import Data.Maybe (fromMaybe, isJust, listToMaybe) import qualified Data.Set as Set import qualified Data.Text as T import Deps (Acyclic (..), BuildTermFunc, BuildTermMethodS, Evaluation (..), Judgment (..), SaveEvalFunc, SaveStepFunc, State (..), Term (..), dontSaveStep)@@ -132,13 +133,28 @@ -- is charged nothing. It is written to the protocol all the same, as a firing -- at its own site with that answer, since the protocol records where 𝔼 was -- asked and what it said there, and with no operand line under it, since none--- was reduced. A firing that got stuck keeps nothing, since nothing was--- answered; a site parked or a recursion cut inside an answer is a part of+-- was reduced. A site parked or a recursion cut inside an answer is a part of -- it, since that is what the run made of the formation. A recursion cut -- inside a firing, so that the firing itself never answered, is kept too, as -- the formation the cut carried: the formation is fired as often as the -- program reads it, and without the cut in the store every one of those--- firings walked all the way down to the same cut again (#1480). The store is+-- firings walked all the way down to the same cut again (#1480). A firing+-- that got stuck is kept as well, as the λ function it got stuck on, since a+-- fork whose branches never join was fired afresh at every read of it (#1493).+-- A stall is a fact about the firing and not about the formation, though: a+-- branch often stays unjoined only because an operand inside it could not yet+-- be brought down, and the walk brings it down a few steps later. So a stall+-- is kept beside the number of answers the memo held when its firing began,+-- and it is told to a later firing only while the memo holds no more, since+-- an operand that could not be reduced can only be reduced once something new+-- was answered, the answers of the firing's own nested firings included+-- (#1495, #1507). A firing inside which the step budget ran out is no stall+-- of the formation at all, since the budget a firing has depends on how deep+-- its site stands, and the same formation fired at a shallower site brings+-- the operand down; so the memo counts every time the budget runs out, and a+-- stall is not kept where that count grew while its firing ran (#1514). An+-- answer the formation made is told before any stall of it, whichever came+-- first. The store is -- one cell every frame of the run shares, like the count of 'Tally', since -- what one frame answered is what its siblings are after. It belongs to -- 'Plausible' and to no switch of its own: a run asking for plausible cuts is@@ -152,18 +168,23 @@ -- the world copies it, and the walk entered the bindings of every copy as if -- they were new, so the tests of 'Φ.number' were reduced once per number the -- program held (#1480).-data Memo = Memo (IORef (Store Kept)) (IORef (Set.Set (Expression, Attribute)))+data Memo = Memo (IORef (Store (Int, Kept))) (IORef Int) (IORef Int) (IORef (Set.Set (Expression, Attribute)))  -- What one firing answered, kept for the firings of the same formation to -- come: the term the entry wrote, symbols and all, and the normal form 𝕄 made -- of it, which are the two lines the protocol writes an answer as. type Answer = (Expression, Expression) --- What the memo keeps of one formation: the answer its firing made, or the--- formation a recursion was cut at while it was being fired.+-- What the memo keeps of one formation: the answer its firing made, the+-- formation a recursion was cut at while it was being fired, or the λ function+-- the firing got stuck on, beside the fewest steps a firing must have spent to+-- be told that stall: none for a stall of the formation's own, and the steps+-- the stuck firing had spent for a stall the step budget made, since a firing+-- with more of the budget left may bring the operand down (#1514, #1521). data Kept   = Answered Answer   | Looped Expression+  | Stalled T.Text Int  -- What 'Memo' keeps: the answers, by the digest of the formation they answer, -- each beside the very formation, since two terms may share a digest.@@ -227,12 +248,13 @@     -- reads is the judgment of the frame it was fired from and never of one     -- above it (#1300).     _judgment :: Judgment-  , -- The λ functions this run has already got stuck on and written a '?(…)'-    -- to the protocol for. A parked site stays in the residue exactly as it was-    -- written, so the '_deep' walk over that residue reaches it again and 𝕄-    -- fires 𝔼 on it once more, only to find out what the spine already found-    -- out; the site is one and the protocol records it once, so the firings-    -- after the first write nothing (see 'symbol' in 'Evaluate', #1300).+  , -- The λ functions this run has already got stuck on and written an+    -- 'unanswered(…)' to the protocol for. A parked site stays in the residue+    -- exactly as it was written, so the '_deep' walk over that residue reaches+    -- it again and 𝕄 fires 𝔼 on it once more, only to find out what the spine+    -- already found out; the site is one and the protocol records it once, so+    -- the firings after the first write nothing (see 'symbol' in 'Evaluate',+    -- #1300).     _parked :: [T.Text]   , -- The formations the frames above this one have entered, which is what     -- '_acyclic' answers "have I been here before" with (see 'entering'). A@@ -252,14 +274,16 @@   , _saveEval :: SaveEvalFunc   } --- Which of the two budgets a run spent, with the limit it was given: the depth--- one branch may descend ('--max-steps', see 'Steps') or the firings the whole--- run may make ('--max-firings', see 'Tally'). Both are the same signal to--- '_partial', which parks either as a site that never finishes, and differ only+-- Which of the budgets a run spent, with the limit it was given: the depth+-- one branch may descend ('--max-steps', see 'Steps'), the firings the whole+-- run may make ('--max-firings', see 'Tally') or the cycles one normalization+-- may take ('--max-cycles', see 'normalized'). All are the same signal to+-- '_partial', which parks any as a site that never finishes, and differ only -- in what the message names. data Budget   = Depth Int   | Firings Int+  | Cycles Int  data ReduceException   = OutOfSteps Budget@@ -308,6 +332,12 @@     -- firing under '_partial' the way an unanswered λ function does, since the     -- dead end is a property of the program rather than of phino (#1401).     Undataizable Expression State+  | -- 𝕄 was handed a term no morphing rule matches. 𝕄 maps normal forms to+    -- formations and every normal form is covered by some rule, so the term+    -- is not a normal form: 'morph' does not normalize what it is given, such+    -- as a dispatch off a formation with neither φ nor λ, which normalization+    -- would reduce (#1442). It carries the term.+    Unmorphable Expression   deriving anyclass (Exception)  instance Show ReduceException where@@ -315,6 +345,8 @@     printf "Dataization did not finish before reaching the limit of steps: --max-steps=%d" limit   show (OutOfSteps (Firings limit)) =     printf "Evaluation did not finish before reaching the limit of firings: --max-firings=%d" limit+  show (OutOfSteps (Cycles limit)) =+    printf "Normalization did not finish before reaching the limit of cycles: --max-cycles=%d" limit   show (OutOfStepsAt budget _ _) = show (OutOfSteps budget)   show (Stuck func) = printf "No entry of --symbolic answers the λ function '%s'" (T.unpack func)   show (StuckAt func _ _) = show (Stuck func)@@ -322,6 +354,7 @@   show (LoopingAt term _ _) = show (Looping term)   show (Undataizable ExTermination _) = "dataization reached the terminator ⊥, which signals an error and cannot be dataized"   show (Undataizable _ _) = "no dataization rule matched"+  show (Unmorphable term) = printf "Morphing expects a normal form, but no morphing rule matches: %s" (printExpression term)  -- 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@@ -329,11 +362,23 @@ -- 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'.+-- with or without '--depth-sensitive'. The memo is told every time it throws,+-- so a stall the budget made is kept as a stall of that budget and not of the+-- formation (see 'Kept', #1514, #1521). The protocol is told too, with the+-- site the frame stood at, so a firing the budget starved no longer reads as+-- one that went well (#1524), and a frame of 𝕄 standing at a whole universe+-- does not spell it on every line (#1531). deeper :: ReduceContext -> IO ReduceContext deeper ctx@ReduceContext{_steps = Steps limit spent}-  | spent >= limit = throwIO (OutOfSteps (Depth limit))+  | spent >= limit = do+      starve ctx._memo+      ctx._saveEval (EvStarved ctx._nesting limit ctx._judgment ctx._site)+      throwIO (OutOfSteps (Depth limit))   | otherwise = pure ctx{_steps = Steps limit (spent + 1)}+  where+    starve :: Maybe Memo -> IO ()+    starve Nothing = pure ()+    starve (Just (Memo _ _ exhausted _)) = modifyIORef' exhausted (+ 1)  -- The tally a run starts from where '--max-firings' gives a ceiling: nothing -- fired yet.@@ -354,35 +399,64 @@ -- one under 'Plausible', the mode the memo belongs to (see 'Memo'), and none -- under any other, where nothing is ever recalled. memoized :: Maybe Acyclic -> IO (Maybe Memo)-memoized (Just Plausible) = Just <$> (Memo <$> newIORef Map.empty <*> newIORef Set.empty)+memoized (Just Plausible) = Just <$> (Memo <$> newIORef Map.empty <*> newIORef 0 <*> newIORef 0 <*> newIORef Set.empty) memoized _ = pure Nothing  -- What the memo keeps for the formation, if this run fired it already (see--- 'Memo'); nothing where the run keeps no memo at all.-recalled :: Maybe Memo -> Expression -> IO (Maybe Kept)-recalled Nothing _ = pure Nothing-recalled (Just (Memo store _)) form = do+-- 'Memo'): an answer before anything else, and a stall only while nothing was+-- answered after it and only to a firing that has spent at least the steps+-- kept beside it (see 'Kept'); nothing where the run keeps no memo at all.+recalled :: Maybe Memo -> Expression -> Int -> IO (Maybe Kept)+recalled Nothing _ _ = pure Nothing+recalled (Just (Memo store answers _ _)) form spent = do   kept <- readIORef store-  pure (Map.lookup (hashExpression form) kept >>= lookup form)+  count <- readIORef answers+  let live = [known | (term, (stamp, known)) <- Map.findWithDefault [] (hashExpression form) kept, term == form, current count stamp known]+  pure (find answered live <|> listToMaybe live)+  where+    current :: Int -> Int -> Kept -> Bool+    current count stamp (Stalled _ least) = stamp == count && spent >= least+    current _ _ _ = True+    answered :: Kept -> Bool+    answered (Answered _) = True+    answered _ = False --- Keep what firing the formation came to, for the next firing of it (see--- 'Memo').-retained :: Maybe Memo -> Expression -> Kept -> IO ()-retained Nothing _ _ = pure ()-retained (Just (Memo store _)) form kept = modifyIORef' store (Map.insertWith (++) (hashExpression form) [(form, kept)])+-- How many answers the memo holds (see 'Memo'); none where the run keeps no+-- memo at all.+counted :: Maybe Memo -> IO Int+counted Nothing = pure 0+counted (Just (Memo _ answers _ _)) = readIORef answers +-- How many times the step budget has run out in this run (see 'Memo'); never+-- where the run keeps no memo at all.+starved :: Maybe Memo -> IO Int+starved Nothing = pure 0+starved (Just (Memo _ _ exhausted _)) = readIORef exhausted++-- Keep what firing the formation came to, for the next firing of it, stamped+-- with the count of answers the memo held when that firing began, so that+-- what the firing answered inside itself counts as answered after it (see+-- 'Memo', #1507).+retained :: Maybe Memo -> Expression -> Int -> Kept -> IO ()+retained Nothing _ _ _ = pure ()+retained (Just (Memo store answers _ _)) form stamp kept = do+  modifyIORef' store (Map.insertWith (++) (hashExpression form) [(form, (stamp, kept))])+  case kept of+    Answered _ -> modifyIORef' answers (+ 1)+    _ -> pure ()+ -- Whether the '--deep' walk has entered the binding the object of the world -- declares under the attribute, in whichever copy of the object (see 'Memo'); -- never where the run keeps no memo at all. visited :: Maybe Memo -> Expression -> Attribute -> IO Bool visited Nothing _ _ = pure False-visited (Just (Memo _ walked)) object attr = Set.member (object, attr) <$> readIORef walked+visited (Just (Memo _ _ _ walked)) object attr = Set.member (object, attr) <$> readIORef walked  -- Remember that the '--deep' walk has entered the binding the object of the -- world declares under the attribute (see 'visited'). visit :: Maybe Memo -> Expression -> Attribute -> IO () visit Nothing _ _ = pure ()-visit (Just (Memo _ walked)) object attr = modifyIORef' walked (Set.insert (object, attr))+visit (Just (Memo _ _ _ walked)) object attr = modifyIORef' walked (Set.insert (object, attr))  -- Run one frame of the 𝕄/𝔻 spine, attaching its derivation and its state to a -- stuck λ function or an exhausted budget escaping it. 'Stuck' is raised deep@@ -533,7 +607,8 @@ -- 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+-- its conclusion 'nresult' is built, in the universe the concluding premise+-- names, which every rule spells as the one it was matched in (#1512). 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@@ -553,7 +628,7 @@     matched <- firstMatch ctx rules     case matched of       Just (rule, subst) -> reduce ctx rule subst-      Nothing -> throwIO (userError "no morphing rule matched")+      Nothing -> throwIO (Unmorphable expr)   where     firstMatch :: ReduceContext -> [Y.MorphRule] -> IO (Maybe (Y.MorphRule, Subst))     firstMatch _ [] = pure Nothing@@ -580,17 +655,19 @@         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 concl@(Y.Premise _ (Y.OpMorph arg universe)) -> 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+          world <- buildExpressionThrows universe final           (normal', seq') <- settle ctx rule inner built-          morph' (normal', seq') univ state' ctx+          morph' (normal', seq') world state' ctx         _ -> do           (final, state') <- sides ctx (rule.premises `excluding` [concl]) subst           built <- buildExpressionThrows arg final+          world <- buildExpressionThrows universe final           seq' <- leadsTo seq rule.name built ctx-          morph' (built, seq') univ state' ctx+          morph' (built, seq') world 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@@ -858,12 +935,15 @@     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.+    -- go through their state-aware builders, each in the universe its premise+    -- names; 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 -> ctx._evaluate ctx state [ArgExpression expr, ArgExpression universe] subst-      Y.OpMorph expr -> _morph univ ctx state [ArgExpression expr] subst+      Y.OpMorph expr universe -> do+        world <- buildExpressionThrows universe subst+        _morph world ctx state [ArgExpression expr] subst       operation -> do         term <- execBuildTerm univ ctx (verb operation) (verbArgs operation) subst         pure (term, state)@@ -875,19 +955,22 @@  -- The build-term function name backing a premise operation. verb :: Y.Operation -> String-verb (Y.OpMorph _) = "morph"+verb (Y.OpMorph _ _) = "morph" verb (Y.OpNormalize _) = "normalize" verb (Y.OpEvaluate _ _) = "evaluate" verb (Y.OpContextualize _ _) = "contextualize"-verb (Y.OpDataize _) = "dataize"+verb (Y.OpDataize _ _) = "dataize" --- The build-term arguments backing a premise operation.+-- The build-term arguments backing a premise operation. The universe a 'morph'+-- or a 'dataize' premise names is the second argument of the judgment, not of+-- the build-term function: 'sidePremise' hands it to 𝕄 itself, and the+-- 'dataize' function reads data off a term and needs no universe. verbArgs :: Y.Operation -> [ExtraArgument]-verbArgs (Y.OpMorph expr) = [ArgExpression expr]+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]+verbArgs (Y.OpDataize expr _) = [ArgExpression expr]  leadsTo :: NonEmpty Rewritten -> String -> Expression -> ReduceContext -> IO (NonEmpty Rewritten) leadsTo ((current, _) :| rest) rule expr ReduceContext{..} = do@@ -898,11 +981,15 @@ -- 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.+-- expression together with the extended sequence. A rewriter that ran out of+-- '--max-cycles' hands back a term that is not a normal form, which neither 𝕄+-- nor 𝔻 accepts, so the exhausted budget is signalled instead and '_partial'+-- parks the site the way it parks any other (#1496). 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)+  (rewrittens, exceeded) <- rewrite whole normalizationRules (rewriteContext ctx)+  when exceeded (throwIO (OutOfSteps (Cycles _maxCycles)))   let (rw :| rws) = NE.reverse rewrittens       seq' = rw :| rws <> NE.tail seq   expr' <- locatedExpression _locator (fst rw)
src/Render.hs view
@@ -109,7 +109,7 @@   render (BT_MANY bts) = T.intercalate "-" (map render bts)   render (BT_META mt) = render mt   render (BT_PIPED bts) = "|" <> render bts <> "|"-  render (BT_CUT bts size) = T.intercalate "-" (map render bts) <> "-...(" <> render size <> "b)"+  render (BT_CUT opening omitted closing) = T.intercalate "-" (map render opening) <> "-..(" <> render omitted <> "b)..-" <> T.intercalate "-" (map render closing)  instance Render EXCLAMATION where   render EXCL = "!"@@ -169,7 +169,7 @@   render PA_META_LAMBDA'{..} = "L> " <> render meta   render PA_META_DELTA{..} = render DELTA <> render SPACE <> render DASHED_ARROW <> render SPACE <> render meta   render PA_META_DELTA'{..} = "D> " <> render meta-  render PA_FOLDED{..} = "+" <> render count <> " attrs"+  render PA_FOLDED{..} = "+" <> render count  instance Render BINDINGS where   render = TL.toStrict . TLB.toLazyText . binds@@ -218,18 +218,21 @@   render EX_PHI_AGAIN{..} = "\\phinoAgain{" <> maybe "" (\p -> T.pack p <> ":") prefix <> render idx <> "}"   render EX_BYTES{..} = render bytes   render EX_SINGLE{..} = case pair of-    PA_TAU{..} -> render expr <> ":" <> render attr-    PA_FORMATION{voids = [], ..} -> render expr <> ":" <> render attr-    PA_VOID{..} -> render void <> ":" <> render attr-    PA_DELTA{..} -> render bytes <> ":" <> render DELTA-    PA_DELTA'{..} -> render bytes <> ":" <> render DELTA'-    PA_META_DELTA{..} -> render meta <> ":" <> render DELTA-    PA_META_DELTA'{..} -> render meta <> ":" <> render DELTA'-    PA_LAMBDA{..} -> render func <> ":" <> render LAMBDA-    PA_LAMBDA'{..} -> render func <> ":" <> render LAMBDA'-    PA_META_LAMBDA{..} -> render meta <> ":" <> render LAMBDA-    PA_META_LAMBDA'{..} -> render meta <> ":" <> render LAMBDA'+    PA_TAU{..} -> render expr <> colon <> render attr+    PA_FORMATION{voids = [], ..} -> render expr <> colon <> render attr+    PA_VOID{..} -> render void <> colon <> render attr+    PA_DELTA{..} -> render bytes <> colon <> render DELTA+    PA_DELTA'{..} -> render bytes <> colon <> render DELTA'+    PA_META_DELTA{..} -> render meta <> colon <> render DELTA+    PA_META_DELTA'{..} -> render meta <> colon <> render DELTA'+    PA_LAMBDA{..} -> render func <> colon <> render LAMBDA+    PA_LAMBDA'{..} -> render func <> colon <> render LAMBDA'+    PA_META_LAMBDA{..} -> render meta <> colon <> render LAMBDA+    PA_META_LAMBDA'{..} -> render meta <> colon <> render LAMBDA'     _ -> render formation+    where+      colon :: T.Text+      colon = render space <> ":" <> render space  instance Render [ATTRIBUTE] where   render attrs = T.intercalate ", " (map render attrs)
src/Replacer.hs view
@@ -1,6 +1,3 @@-{-# LANGUAGE DuplicateRecordFields #-}-{-# LANGUAGE RecordWildCards #-}- -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT @@ -9,40 +6,37 @@ module Replacer   ( replaceExpression   , replaceExpressionFast-  , ReplaceContext (..)   , ReplaceExpressionFunc   ) where  import AST-import Data.List (isPrefixOf)+import Data.List (isInfixOf, isPrefixOf)  type ReplaceState a = (a, [Expression], [Expression -> Expression]) -type ReplaceExpressionFunc' = ReplaceState Expression -> ReplaceContext -> ReplaceState Expression+type ReplaceExpressionFunc' = ReplaceState Expression -> ReplaceState Expression  type ReplaceExpressionFunc = ReplaceState Expression -> Expression -newtype ReplaceContext = ReplaceCtx {_maxDepth :: Int}--replaceBindings :: ReplaceState [Binding] -> ReplaceContext -> ReplaceExpressionFunc' -> ReplaceState [Binding]-replaceBindings state@(_, [], _) _ _ = state-replaceBindings state@(_, _, []) _ _ = state-replaceBindings state@([], _, _) _ _ = state-replaceBindings (BiTau attr expr : bds, ptns, repls) ctx func =-  let (expr', ptns', repls') = func (expr, ptns, repls) ctx-      (bds', ptns'', repls'') = replaceBindings (bds, ptns', repls') ctx func+replaceBindings :: ReplaceState [Binding] -> ReplaceExpressionFunc' -> ReplaceState [Binding]+replaceBindings state@(_, [], _) _ = state+replaceBindings state@(_, _, []) _ = state+replaceBindings state@([], _, _) _ = state+replaceBindings (BiTau attr expr : bds, ptns, repls) func =+  let (expr', ptns', repls') = func (expr, ptns, repls)+      (bds', ptns'', repls'') = replaceBindings (bds, ptns', repls') func    in (BiTau attr expr' : bds', ptns'', repls'')-replaceBindings (bd : bds, ptns, repls) ctx func =-  let (bds', ptns', repls') = replaceBindings (bds, ptns, repls) ctx func+replaceBindings (bd : bds, ptns, repls) func =+  let (bds', ptns', repls') = replaceBindings (bds, ptns, repls) func    in (bd : bds', ptns', repls') -replaceArgument :: ReplaceState Argument -> ReplaceContext -> ReplaceExpressionFunc' -> ReplaceState Argument-replaceArgument (ArTau attr expr, ptns, repls) ctx func =-  let (expr', ptns', repls') = func (expr, ptns, repls) ctx+replaceArgument :: ReplaceState Argument -> ReplaceExpressionFunc' -> ReplaceState Argument+replaceArgument (ArTau attr expr, ptns, repls) func =+  let (expr', ptns', repls') = func (expr, ptns, repls)    in (ArTau attr expr', ptns', repls')-replaceArgument (ArAlpha alpha expr, ptns, repls) ctx func =-  let (expr', ptns', repls') = func (expr, ptns, repls) ctx+replaceArgument (ArAlpha alpha expr, ptns, repls) func =+  let (expr', ptns', repls') = func (expr, ptns, repls)    in (ArAlpha alpha expr', ptns', repls')  -- A term equal to a pattern is inert only when the pattern is, and a term@@ -50,67 +44,68 @@ -- looked for inside an inert term, which is where the copies of big objects -- a normalization carries along are (#1453). replaceExpression' :: ReplaceExpressionFunc'-replaceExpression' state@(expr, ptns@(ptn : _ptns), repls@(repl : _repls)) ctx+replaceExpression' state@(expr, ptns@(ptn : _ptns), repls@(repl : _repls))   | inert expr && not (inert ptn) = state-  | expr == ptn = replaceExpression' (repl expr, _ptns, _repls) ctx+  | expr == ptn = replaceExpression' (repl expr, _ptns, _repls)   | otherwise = case expr of       ExDispatch inner attr ->-        let (expr', ptns', repls') = replaceExpression' (inner, ptns, repls) ctx+        let (expr', ptns', repls') = replaceExpression' (inner, ptns, repls)          in (ExDispatch expr' attr, ptns', repls')       ExApplication inner arg ->-        let (expr', ptns', repls') = replaceExpression' (inner, ptns, repls) ctx-            (arg', ptns'', repls'') = replaceArgument (arg, ptns', repls') ctx replaceExpression'+        let (expr', ptns', repls') = replaceExpression' (inner, ptns, repls)+            (arg', ptns'', repls'') = replaceArgument (arg, ptns', repls') replaceExpression'          in (ExApplication expr' arg', ptns'', repls'')       ExFormation bds ->-        let (bds', ptns', repls') = replaceBindings (bds, ptns, repls) ctx replaceExpression'+        let (bds', ptns', repls') = replaceBindings (bds, ptns, repls) replaceExpression'          in (ExFormation bds', ptns', repls')       _ -> state-replaceExpression' state _ = state+replaceExpression' state = state -replaceBindingsFast :: [Binding] -> [Expression] -> [Expression] -> [Binding]-replaceBindingsFast _ ((ExFormation []) : _ptns) ((ExFormation rbds) : _repls) =-  replaceBindingsFast rbds _ptns _repls-replaceBindingsFast bds ((ExFormation pbds) : _ptns) ((ExFormation rbds) : _repls) =-  let replaced = findAndReplace bds pbds rbds-   in replaceBindingsFast replaced _ptns _repls+-- Every pair of a pattern and a replacement stands for one match, so a pair+-- is spent once it replaces something in the bindings of a formation, and the+-- bindings a replacement brings in are searched only with the pairs still+-- left. That is what ends the walk, as it ends the regular one, rather than a+-- cap on how deep the walk goes, which dropped every match below it (#1391).+replaceBindingsFast :: Expression -> ReplaceState [Binding] -> ReplaceState [Binding]+replaceBindingsFast _ state@(_, [], _) = state+replaceBindingsFast _ state@(_, _, []) = state+replaceBindingsFast expr (bds, ptn : ptns, repl : repls) = case (ptn, repl expr) of+  (ExFormation [], ExFormation rbds) -> replaceBindingsFast expr (rbds, ptns, repls)+  (ExFormation pbds, ExFormation rbds)+    | pbds `isInfixOf` bds -> replaceBindingsFast expr (findAndReplace bds pbds rbds, ptns, repls)+  _ ->+    let (bds', ptns', repls') = replaceBindingsFast expr (bds, ptns, repls)+     in (bds', ptn : ptns', repl : repls')   where     findAndReplace :: [Binding] -> [Binding] -> [Binding] -> [Binding]     findAndReplace [] _ _ = []-    findAndReplace _ [] repl = repl-    findAndReplace xs@(x : xs') ptn repl-      | ptn `isPrefixOf` xs = repl ++ findAndReplace (drop (length ptn) xs) ptn repl-      | otherwise = x : findAndReplace xs' ptn repl-replaceBindingsFast bds _ _ = bds+    findAndReplace _ [] rbds = rbds+    findAndReplace xs@(x : xs') pbds rbds+      | pbds `isPrefixOf` xs = rbds ++ findAndReplace (drop (length pbds) xs) pbds rbds+      | otherwise = x : findAndReplace xs' pbds rbds  replaceExpressionFast' :: ReplaceExpressionFunc'-replaceExpressionFast' = _replaceExpressionFast 0-  where-    _replaceExpressionFast :: Int -> ReplaceExpressionFunc'-    _replaceExpressionFast _ state@(_, [], _) _ = state-    _replaceExpressionFast _ state@(_, _, []) _ = state-    _replaceExpressionFast depth state@(expr, ptns, repls) ctx@ReplaceCtx{..} =-      if depth == _maxDepth-        then (expr, [], [])-        else case expr of-          ExFormation bds ->-            let replaced = replaceBindingsFast bds ptns (map (\rep -> rep expr) repls)-                (bds', ptns', repls') = replaceBindings (replaced, ptns, repls) ctx (_replaceExpressionFast (depth + 1))-             in (ExFormation bds', ptns', repls')-          ExDispatch inner attr ->-            let (expr', ptns', repls') = replaceExpressionFast' (inner, ptns, repls) ctx-             in (ExDispatch expr' attr, ptns', repls')-          ExApplication inner arg ->-            let (expr', ptns', repls') = replaceExpressionFast' (inner, ptns, repls) ctx-                (arg', ptns'', repls'') = replaceArgument (arg, ptns', repls') ctx replaceExpressionFast'-             in (ExApplication expr' arg', ptns'', repls'')-          _ -> state+replaceExpressionFast' state@(_, [], _) = state+replaceExpressionFast' state@(_, _, []) = state+replaceExpressionFast' state@(expr, ptns, repls) = case expr of+  ExFormation bds ->+    let (bds', ptns', repls') = replaceBindings (replaceBindingsFast expr (bds, ptns, repls)) replaceExpressionFast'+     in (ExFormation bds', ptns', repls')+  ExDispatch inner attr ->+    let (expr', ptns', repls') = replaceExpressionFast' (inner, ptns, repls)+     in (ExDispatch expr' attr, ptns', repls')+  ExApplication inner arg ->+    let (expr', ptns', repls') = replaceExpressionFast' (inner, ptns, repls)+        (arg', ptns'', repls'') = replaceArgument (arg, ptns', repls') replaceExpressionFast'+     in (ExApplication expr' arg', ptns'', repls'')+  _ -> state  replaceExpression :: ReplaceExpressionFunc replaceExpression state =-  let (expr, _, _) = replaceExpression' state (ReplaceCtx 0)+  let (expr, _, _) = replaceExpression' state    in expr -replaceExpressionFast :: ReplaceContext -> ReplaceExpressionFunc-replaceExpressionFast ctx state =-  let (expr, _, _) = replaceExpressionFast' state ctx+replaceExpressionFast :: ReplaceExpressionFunc+replaceExpressionFast state =+  let (expr, _, _) = replaceExpressionFast' state    in expr
src/Rewriter.hs view
@@ -24,7 +24,7 @@ import Matcher (Subst) import Must (Must (..), exceedsUpperBound, inRange) import Printer (printExpression)-import Replacer (ReplaceContext (ReplaceCtx), ReplaceExpressionFunc, replaceExpression, replaceExpressionFast)+import Replacer (ReplaceExpressionFunc, replaceExpression, replaceExpressionFast) import Rule (RuleContext (RuleContext)) import qualified Rule as R import Text.Printf (printf)@@ -143,8 +143,8 @@ -- In such case we can just replace bindings one by one without building whole expression. -- You can find more details in this ticket: https://github.com/objectionary/phino/issues/321 -- If we don't meet the conditions above - just do a regular replacing-tryBuildAndReplaceFast :: ToReplace -> ReplaceContext -> IO Expression-tryBuildAndReplaceFast state@(expr, ExFormation _pbds@(pbd : pbds), ExFormation _rbds@(rbd : rbds), substs) ctx =+tryBuildAndReplaceFast :: ToReplace -> IO Expression+tryBuildAndReplaceFast state@(expr, ExFormation _pbds@(pbd : pbds), ExFormation _rbds@(rbd : rbds), substs) =   let pbds' = init pbds       rbds' = init rbds    in if startsAndEndsWithMeta _pbds@@ -155,7 +155,7 @@         && not (hasMetaBindings rbds')         then do           logDebug "Applying fast replacing since 'pattern' and 'result' are suitable for this..."-          buildAndReplace' (expr, ExFormation pbds', ExFormation rbds', substs) (replaceExpressionFast ctx)+          buildAndReplace' (expr, ExFormation pbds', ExFormation rbds', substs) replaceExpressionFast         else do           logDebug "Applying regular replacing..."           buildAndReplace' state replaceExpression@@ -173,7 +173,7 @@       BiAny _ -> True       _ -> False     hasMetaBindings = foldl (\acc bd -> acc || isMetaBinding bd) False-tryBuildAndReplaceFast state _ = buildAndReplace' state replaceExpression+tryBuildAndReplaceFast state = buildAndReplace' state replaceExpression  -- The function returns tuple (X, Y, Z) where -- - X is sequence of expressions;@@ -198,7 +198,11 @@             then do               logDebug (printf "Max amount of rewriting cycles (%d) for rule '%s' has been reached, rewriting is stopped" _maxDepth ruleName)               if _depthSensitive-                then throwIO (StoppedOnLimit "max-depth" _maxDepth)+                then do+                  exhausted <- applicable current [rule] ctx+                  if exhausted+                    then throwIO (StoppedOnLimit "max-depth" _maxDepth)+                    else pure (_rewrittens, _unique, False)                 else pure (_rewrittens, _unique, False)             else do               logDebug (printf "Starting rewriting cycle for rule '%s': %d out of %d" ruleName _count _maxDepth)@@ -213,7 +217,7 @@                     else pure (_rewrittens, _unique, False)                 matched -> do                   logDebug (printf "Rule '%s' has been matched, applying..." ruleName)-                  expr <- tryBuildAndReplaceFast (expression, ptn, res, matched) (ReplaceCtx _maxDepth)+                  expr <- tryBuildAndReplaceFast (expression, ptn, res, matched)                   if expression == expr                     then do                       logDebug (printf "Applied '%s', no changes made" ruleName)@@ -240,6 +244,21 @@           let (head', _) :| rest = _rewrittens            in (next, Nothing) :| (head', Just rule.name) : rest +-- Tells whether any of the rules still matches the located expression. A run+-- with nothing left to rewrite after its last allowed step has finished, not+-- run out of its limit, so --depth-sensitive lets it pass (#1439)+applicable :: Expression -> [Y.Rule] -> RewriteContext -> IO Bool+applicable current rules RewriteContext{..} = do+  expression <- locatedExpression _locator current+  go expression rules+  where+    go :: Expression -> [Y.Rule] -> IO Bool+    go _ [] = pure False+    go expression (rule : rest) =+      R.matchExpressionWithRule expression rule (RuleContext _buildTerm _universe) >>= \case+        [] -> go expression rest+        _ -> pure True+ -- Rewrite the expression by provided locator from RewriteContext rewrite :: Expression -> [Y.Rule] -> RewriteContext -> IO Rewrittens rewrite expr rules ctx@RewriteContext{..} = do@@ -249,10 +268,15 @@     _rewrite :: RewriteState -> Int -> IO Rewrittens     _rewrite state@(rewrittens@((current, _) :| _), _, _) count       | not (inRange _must count) && count > 0 && exceedsUpperBound _must count = throwIO (MustStopBefore _must count)+      | count == _maxCycles && not (inRange _must count) = throwIO (MustBeGoing _must count)       | count == _maxCycles = do           logDebug (printf "Max amount of rewriting cycles for all rules (%d) has been reached, rewriting is stopped" _maxCycles)           if _depthSensitive-            then throwIO (StoppedOnLimit "max-cycles" _maxCycles)+            then do+              exhausted <- applicable current rules ctx+              if exhausted+                then throwIO (StoppedOnLimit "max-cycles" _maxCycles)+                else pure (rewrittens, False)             else pure (rewrittens, True)       | otherwise = do           logDebug (printf "Starting rewriting cycle for all rules: %d out of %d" count _maxCycles)
src/Rule.hs view
@@ -71,16 +71,22 @@ isNF (ExFormation []) _ = True isNF (ExFormation bds) ctx = normalBindings bds || not (matchesAnyNormalizationRule (ExFormation bds) ctx)   where-    -- Returns True if all given bindings are 100% in normal form+    -- Returns True if all given bindings are 100% in normal form: each one is+    -- a Δ, a λ or a void, and no Δ stands beside a λ, since 'dl' turns such a+    -- formation into ⊥ (#1437)     normalBindings :: [Binding] -> Bool-    normalBindings [] = True-    normalBindings (bd : bds) =-      let next = normalBindings bds-       in case bd of-            BiDelta _ -> next-            BiVoid _ -> next-            BiLambda _ -> next-            _ -> False+    normalBindings bds = all inert bds && not (any delta bds && any lambda bds)+    inert :: Binding -> Bool+    inert (BiDelta _) = True+    inert (BiVoid _) = True+    inert (BiLambda _) = True+    inert _ = False+    delta :: Binding -> Bool+    delta (BiDelta _) = True+    delta _ = False+    lambda :: Binding -> Bool+    lambda (BiLambda _) = True+    lambda _ = False isNF expr ctx = not (matchesAnyNormalizationRule expr ctx)  _or :: [Y.Condition] -> Subst -> RuleContext -> IO [Subst]
src/Sugar.hs view
@@ -36,7 +36,7 @@     goExpr EX_FORMATION{..} = case goBinding binding of       empty@BI_EMPTY{} -> EX_FORMATION lsb NO_EOL NO_TAB empty NO_EOL NO_TAB rsb       binding'@BI_PAIR{pair = pair', bindings = BDS_EMPTY{}}-        | sugar == SWEET && sugared pair' -> EX_SINGLE pair' (EX_FORMATION lsb eol tab binding' eol' tab' rsb)+        | sugar == SWEET && sugared pair' -> EX_SINGLE pair' NO_SPACE (EX_FORMATION lsb eol tab binding' eol' tab' rsb)       binding' -> EX_FORMATION lsb eol tab binding' eol' tab' rsb     goExpr EX_DISPATCH{..} = EX_DISPATCH (goExpr expr) space attr     goExpr EX_APPLICATION{..} = case goArgument argument of@@ -46,7 +46,7 @@     goExpr EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (goExpr expr)     goExpr EX_SINGLE{..}       | isRho pair = goExpr formation-      | otherwise = EX_SINGLE (goPair pair) (goExpr formation)+      | otherwise = EX_SINGLE (goPair pair) space (goExpr formation)     goExpr expr = expr     -- Formation bindings: drop the ρ pairs, recurse into whatever remains.     goBinding :: BINDING -> BINDING
src/XMIR.hs view
@@ -30,7 +30,7 @@ import Data.Bifunctor (bimap) import Data.Char (isAsciiLower, isDigit) import Data.Foldable (foldlM)-import Data.List (intercalate)+import Data.List (groupBy, intercalate) import qualified Data.Map as M import Data.Maybe (catMaybes) import qualified Data.Text as T@@ -149,6 +149,7 @@               , bts               ]         )+expression app@(ExApplication _ (ArTau AtRho _)) _ = throwIO (UnsupportedExpression app) expression (ExApplication expr arg) ctx = do   (base, children) <- expression expr ctx   (base', children') <- expression texpr ctx@@ -573,15 +574,22 @@  -- A formation keeps its Δ data in the text content of its own element, the way -- the printer emits a Δ binding, while the rest of the bindings live in the--- nested <o> elements+-- nested <o> elements; the text stands among them where the binding stands in+-- the formation, so the children are read in document order and a run of text+-- between two <o> elements is the Δ binding at that position (#1430) xmirToFormation :: C.Cursor -> [String] -> IO Expression xmirToFormation cur fqn = do-  nested <- mapM (`xmirToFormationBinding` fqn) (cur C.$/ C.element (toName "o"))-  bds <- if hasText cur then (: nested) <$> delta else pure nested+  bds <- concat <$> mapM binding (groupBy (\left right -> not (nested left) && not (nested right)) (C.child cur))   ExFormation <$> uniqueBindings' bds   where-    delta :: IO Binding-    delta = BiDelta . bytesToBts . T.unpack . T.strip . T.pack <$> getText cur+    nested :: C.Cursor -> Bool+    nested node = not (null (C.element (toName "o") node))+    binding :: [C.Cursor] -> IO [Binding]+    binding [node] | nested node = pure <$> xmirToFormationBinding node fqn+    binding nodes = pure [BiDelta (bytesToBts (T.unpack text)) | not (T.null text)]+      where+        text :: T.Text+        text = T.strip (T.concat [content | NodeContent content <- map C.node nodes])  xmirToExpression :: C.Cursor -> [String] -> IO Expression xmirToExpression cur fqn
src/Yaml.hs view
@@ -287,11 +287,11 @@   slots premise = slots premise.operation  instance Slots Operation where-  slots (OpMorph expr) = slots expr+  slots (OpMorph expr universe) = slots expr ++ slots universe   slots (OpNormalize expr) = slots expr   slots (OpEvaluate expr universe) = slots expr ++ slots universe   slots (OpContextualize expr context) = slots expr ++ slots context-  slots (OpDataize expr) = slots expr+  slots (OpDataize expr universe) = slots expr ++ slots universe  instance Metas Condition where   metas (And conds) = metas conds@@ -357,16 +357,16 @@   bare names premise = premise{result = bare names premise.result, operation = bare names premise.operation}  instance Metas Operation where-  metas (OpMorph expr) = metas expr+  metas (OpMorph expr universe) = metas expr ++ metas universe   metas (OpNormalize expr) = metas expr   metas (OpEvaluate expr universe) = metas expr ++ metas universe   metas (OpContextualize expr context) = metas expr ++ metas context-  metas (OpDataize expr) = metas expr-  bare names (OpMorph expr) = OpMorph (bare names expr)+  metas (OpDataize expr universe) = metas expr ++ metas universe+  bare names (OpMorph expr universe) = OpMorph (bare names expr) (bare names universe)   bare names (OpNormalize expr) = OpNormalize (bare names expr)   bare names (OpEvaluate expr universe) = OpEvaluate (bare names expr) (bare names universe)   bare names (OpContextualize expr context) = OpContextualize (bare names expr) (bare names context)-  bare names (OpDataize expr) = OpDataize (bare names expr)+  bare names (OpDataize expr universe) = OpDataize (bare names expr) (bare names universe)  -- A rule is the scope an index counts in: the reader meets the metas of one -- inference within it and nowhere else, so a kind the rule names just once@@ -457,8 +457,10 @@  -- One premise above the inference line of a morphing or dataization rule: bind -- the meta named 'result' to the value of applying 'operation' to its argument.--- The universe e is the fixed second argument of 𝕄 and 𝔻, not a per-premise--- value, so it is not recorded here.+-- A 'morph' or 'dataize' premise names the universe it reduces in beside the+-- term, the second argument of 𝕄(n, e, s) and 𝔻(n, e, s), the way 'evaluate'+-- names the one 𝔼 fires in: the rule says where each of its premises runs, and+-- nothing is handed to a premise behind the rule's back (#1512). data Premise = Premise   { result :: Text   , operation :: Operation@@ -468,11 +470,11 @@ -- The reduction a premise performs, mirroring the build-term functions and the -- 𝒩 and 𝔻 reducers the engine already provides. data Operation-  = OpMorph Expression+  = OpMorph Expression Expression   | OpNormalize Expression   | OpEvaluate Expression Expression   | OpContextualize Expression Expression-  | OpDataize Expression+  | OpDataize Expression Expression   deriving (Eq, Generic, Show)  -- One morphing rule in inference-rule form: when 'match' matches the term and@@ -541,24 +543,25 @@         Just _ -> fail "'d-result' must be a bytes meta"         Nothing -> fail "a premise needs an 'n-result' or 'd-result' meta" --- The single verb of a premise.+-- The single verb of a premise. Every judgment but 𝒩 is binary here: 𝕄, 𝔼 and+-- 𝔻 take the term and the universe, 𝒞 the term and the context, each as a+-- list of two. premiseOperation :: Object -> Parser Operation premiseOperation o =   asum-    [ OpMorph <$> o .: "morph"+    [ binary "morph" OpMorph     , OpNormalize <$> o .: "normalize"-    , do-        vals <- o .: "evaluate"-        case vals of-          [expr, universe] -> OpEvaluate <$> parseJSON expr <*> parseJSON universe-          _ -> fail "'evaluate' expects exactly two arguments"-    , do-        vals <- o .: "contextualize"-        case vals of-          [expr, context] -> OpContextualize <$> parseJSON expr <*> parseJSON context-          _ -> fail "'contextualize' expects exactly two arguments"-    , OpDataize <$> o .: "dataize"+    , binary "evaluate" OpEvaluate+    , binary "contextualize" OpContextualize+    , binary "dataize" OpDataize     ]+  where+    binary :: Key -> (Expression -> Expression -> Operation) -> Parser Operation+    binary key verb = do+      vals <- o .: key+      case vals of+        [expr, second] -> verb <$> parseJSON expr <*> parseJSON second+        _ -> fail (printf "'%s' expects exactly two arguments" (Key.toString key))  -- Parse the optional 'label', rejecting one that merely repeats the rule's -- 'name'. A label equal to the name typesets the same token across two macros
test/ASTSpec.hs view
@@ -311,6 +311,14 @@       within (call 2 ExRoot) (ExFormation [BiTau (AtLabel "x") (call 2 ExRoot), BiLambda (Function "L_g")]) `shouldBe` False     it "does not find a formation under the ρ of the next one" $       within (call 6 ExRoot) (call 6 (ExFormation [BiTau AtRho (call 6 ExRoot)])) `shouldBe` False+    it "finds a round holding a datum inside one holding a symbol in its place" $+      within (call 7 (pair (ExFormation [BiDelta (BtOne "1F")]))) (call 7 (ExFormation [BiLambda (FnSymbol 9)])) `shouldBe` True+    it "finds a round inside one holding a symbol where the first holds one only under ρ" $+      within (call 3 (ExFormation [BiDelta (BtOne "5C"), BiTau AtRho (call 2 ExRoot)])) (call 3 (ExFormation [BiLambda (FnSymbol 4)])) `shouldBe` True+    it "does not find a round holding a symbol inside one holding a bare symbol in its place" $+      within (call 8 (pair (ExFormation [BiLambda (FnSymbol 2)]))) (call 8 (ExFormation [BiLambda (FnSymbol 6)])) `shouldBe` False+    it "does not find a term inside a bare symbol at the top" $+      within (ExFormation [BiDelta (BtOne "3E")]) (ExFormation [BiLambda (FnSymbol 5)]) `shouldBe` False    describe "hashSkeleton" $ do     it "does not tell apart two formations that bind other terms to the same attributes" $
test/AbridgeSpec.hs view
@@ -17,19 +17,32 @@ import Printer (printExpressionWith) import Sugar (SugarType (..)) import Test.Hspec (Spec, describe, it, shouldBe)+import Text.Printf (printf)  spec :: Spec spec =   describe "abridged" $ do-    it "leaves a formation no longer than sixty characters as it is" $+    it "leaves a formation no longer than the width as it is" $       printExpressionWith-        (const abridged)+        (const (abridged 64))         (ExFormation [BiTau (AtLabel "kübel") (ExDispatch ExXi (AtLabel "wand")), BiVoid (AtLabel "zaun")])         (SWEET, UNICODE, SINGLELINE, defaultMargin)         `shouldBe` "⟦ kübel ↦ wand, zaun ↦ ∅ ⟧"+    it "keeps a formation exactly as wide as the width" $+      printExpressionWith+        (const (abridged 68))+        (ExFormation (map (\idx -> BiTau (AtLabel (T.pack ("ort-" <> show idx))) ExRoot) [1 .. 6 :: Int]))+        (SWEET, UNICODE, SINGLELINE, defaultMargin)+        `shouldBe` "⟦ ort-1 ↦ Φ, ort-2 ↦ Φ, ort-3 ↦ Φ, ort-4 ↦ Φ, ort-5 ↦ Φ, ort-6 ↦ Φ ⟧"+    it "folds a formation one character wider than the width" $+      printExpressionWith+        (const (abridged 67))+        (ExFormation (map (\idx -> BiTau (AtLabel (T.pack ("ort-" <> show idx))) ExRoot) [1 .. 6 :: Int]))+        (SWEET, UNICODE, SINGLELINE, defaultMargin)+        `shouldBe` "⟦ +6 ⟧"     it "keeps the data and the λ of a long formation and folds the rest into a count" $       printExpressionWith-        (const abridged)+        (const (abridged 64))         ( ExFormation             ( BiDelta (BtMany ["00", "77", "66"])                 : BiLambda (Function "L_xxx")@@ -37,10 +50,10 @@             )         )         (SWEET, UNICODE, SINGLELINE, defaultMargin)-        `shouldBe` "⟦ Δ ⤍ 00-77-66, λ ⤍ L_xxx, +34 attrs ⟧"+        `shouldBe` "⟦ Δ ⤍ 00-77-66, λ ⤍ L_xxx, +34 ⟧"     it "keeps the φ of a long formation and folds the formation it holds" $       printExpressionWith-        (const abridged)+        (const (abridged 64))         ( ExFormation             [ BiTau (AtLabel "hund") ExRoot             , BiTau AtPhi (ExFormation (map (\idx -> BiTau (AtLabel (T.pack ("pfote-" <> show idx))) ExRoot) [1 .. 9 :: Int]))@@ -48,28 +61,28 @@             ]         )         (SWEET, UNICODE, SINGLELINE, defaultMargin)-        `shouldBe` "⟦ φ ↦ ⟦ +9 attrs ⟧, +2 attrs ⟧"-    it "cuts a long byte string to its first bytes and its length" $+        `shouldBe` "⟦ φ ↦ ⟦ +9 ⟧, +2 ⟧"+    it "cuts a long byte string to its first bytes, its last bytes and the count of the bytes between them" $       printExpressionWith-        (const abridged)-        (ExFormation [BiDelta (BtMany (replicate 45 "A7"))])+        (const (abridged 64))+        (ExFormation [BiDelta (BtMany (map (printf "%02X") [7 .. 51 :: Int]))])         (SWEET, UNICODE, SINGLELINE, defaultMargin)-        `shouldBe` "A7-A7-A7-A7-...(45b):Δ"+        `shouldBe` "07-08-..(41b)..-32-33:Δ"     it "cuts a long byte string inside a formation too short to fold" $       printExpressionWith-        (const abridged)+        (const (abridged 64))         (ExFormation [BiTau (AtLabel "k") (ExFormation [BiDelta (BtMany ["01", "02", "03", "04", "05", "06", "07", "08", "09", "0A"])])])         (SWEET, UNICODE, SINGLELINE, defaultMargin)-        `shouldBe` "01-02-03-04-...(10b):Δ:k"+        `shouldBe` "01-02-..(6b)..-09-0A:Δ:k"     it "keeps a byte string of eight bytes whole" $       printExpressionWith-        (const abridged)+        (const (abridged 64))         (ExFormation (BiDelta (BtMany ["40", "60", "E0", "00", "00", "00", "00", "01"]) : map (\idx -> BiVoid (AtLabel (T.pack ("ränder-" <> show idx)))) [1 .. 5 :: Int]))         (SWEET, UNICODE, SINGLELINE, defaultMargin)-        `shouldBe` "⟦ Δ ⤍ 40-60-E0-00-00-00-00-01, +5 attrs ⟧"+        `shouldBe` "⟦ Δ ⤍ 40-60-E0-00-00-00-00-01, +5 ⟧"     it "spells a folded formation the same way in ASCII" $       printExpressionWith-        (const abridged)+        (const (abridged 64))         (ExFormation (BiLambda (Function "F") : map (\idx -> BiVoid (AtLabel (T.pack ("sehr-langes-" <> show idx)))) [1 .. 5 :: Int]))         (SWEET, ASCII, SINGLELINE, defaultMargin)-        `shouldBe` "[[ L> F, +5 attrs ]]"+        `shouldBe` "[[ L> F, +5 ]]"
test/BuilderSpec.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-}  -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com@@ -14,7 +15,10 @@ import Data.Map.Strict qualified as Map import Data.Text qualified as T import Matcher+import System.Random (randomRIO) import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, anyException, describe, it, shouldBe, shouldSatisfy, shouldThrow)+import Text.Printf (printf)+import Yaml qualified as Y  test :: (Show a, Eq a) => (a -> Subst -> Either String a) -> [(String, a, [(T.Text, MetaValue)], Either String a)] -> SpecWith (Arg Expectation) test function useCases =@@ -149,6 +153,16 @@           ]           (\(desc, expr, context, expected) -> it desc (contextualize expr context `shouldBe` expected)) +  describe "contextualize against the contextualization rules" $ do+    it "contextualizes every random term as the one rule matching it concludes" $ do+      pairs <- replicateM 500 ((,) <$> term 3 <*> term 2)+      map (\(expr, context) -> conclusions expr context Y.contextualizationRules) pairs+        `shouldBe` map (\(expr, context) -> [contextualize expr context]) pairs+    it "leaves no contextualization rule unmatched by random terms" $ do+      pairs <- replicateM 500 ((,) <$> term 3 <*> term 2)+      [rule.name | rule <- Y.contextualizationRules, all (\(expr, context) -> null (conclusions expr context [rule])) pairs]+        `shouldBe` []+   describe "buildBinding: lambda and delta bindings from metas" $     forM_       [@@ -260,3 +274,42 @@         (ExFormation [BiTau (AtLabel "qwv") (ExFormation [BiVoid AtRho]), BiLambda (Function "Kzr")])         (ExFormation [BiTau (AtLabel "qwv") (ExFormation [BiVoid AtRho]), BiLambda (Function "Kzr")])         `shouldBe` ExRoot+  where+    -- A term of the calculus no deeper than the given depth, made of the six+    -- forms 𝒞 is defined over, so every contextualization rule meets some.+    term :: Int -> IO Expression+    term depth = do+      form <- randomRIO (0 :: Int, if depth > 0 then 6 else 2)+      case form of+        0 -> pure ExXi+        1 -> pure ExRoot+        2 -> pure ExTermination+        3 -> do+          attr <- attribute+          body <- term (depth - 1)+          pure (ExFormation [BiTau attr body, BiVoid AtRho])+        4 -> ExDispatch <$> term (depth - 1) <*> attribute+        5 -> ExApplication <$> term (depth - 1) <*> (ArTau <$> attribute <*> term (depth - 1))+        _ -> ExApplication <$> term (depth - 1) <*> (ArAlpha . Alpha <$> randomRIO (0, 9) <*> term (depth - 1))+    attribute :: IO Attribute+    attribute = do+      letters <- replicateM 3 (randomRIO ('a', 'z'))+      pick <- randomRIO (0 :: Int, 3)+      pure ([AtLabel (T.pack letters), AtPhi, AtLabel (T.pack (reverse letters)), AtLambda] !! pick)+    -- What the given rules conclude 𝒞(n, c) to be, one conclusion per match,+    -- reading every premise 𝒞 of a smaller term off 'contextualize' itself.+    conclusions :: Expression -> Expression -> [Y.ContextualizeRule] -> [Expression]+    conclusions expr context rules =+      [ built+      | rule <- rules+      , matched <- matchExpression' rule.match expr+      , around <- matchExpression' rule.cmatch context+      , Just subst <- [combine matched around]+      , Right built <- [foldM premised subst rule.premises >>= buildExpression rule.cresult]+      ]+    premised :: Subst -> Y.Premise -> Either String Subst+    premised subst (Y.Premise result (Y.OpContextualize expr context)) = do+      inner <- buildExpression expr subst+      outer <- buildExpression context subst+      maybe (Left (printf "premise meta '%s' clashes with a binding" (T.unpack result))) Right (combine (substSingle result (MvExpression (contextualize inner outer))) subst)+    premised _ premise = Left (printf "premise '%s' is not a contextualization" (T.unpack premise.result))
test/CLIHelpersSpec.hs view
@@ -28,7 +28,7 @@ {-# ANN testPrintContext ("HLint: ignore Eta reduce" :: String) #-} testPrintContext :: IOFormat -> PrintContext testPrintContext format =-  PrintCtx SWEET False False MULTILINE 2 defaultXmirContext False False False False False 1 1 ExRoot Nothing Nothing Nothing format+  PrintCtx SWEET False Nothing MULTILINE 2 defaultXmirContext False False False False False 1 1 ExRoot Nothing Nothing Nothing format  spec :: Spec spec = do
test/CLISpec.hs view
@@ -580,7 +580,7 @@               , "  |w| -> \\phiTerminal{\\xi},"               , "  \\phiTerminal{\\rho} -> Q,"               , "  @ -> 1,"-              , "  |y| -> \"H$@^M\","+              , "  |y| -> \"H\\char36{}\\char64{}\\char94{}M\","               , "  L> |Fu\\char95{}nc|"               , "]]{.}"               , "\\end{phiquation}"@@ -593,7 +593,7 @@           ["rewrite", "--output=latex", "--sweet", "--nonumber", "--flat"]           [ unlines               [ "\\begin{phiquation*}"-              , "[[ |x| -> 5 ]]{.}"+              , "5 : |x|{.}"               , "\\end{phiquation*}"               ]           ]@@ -615,7 +615,7 @@           ["rewrite", "--output=latex", "--sweet", "--flat", "--expression=foo"]           [ unlines               [ "\\begin{phiquation}"-              , "\\phiExpression{foo} [[ |x| -> 5 ]]{.}"+              , "\\phiExpression{foo} 5 : |x|{.}"               , "\\end{phiquation}"               ]           ]@@ -626,7 +626,7 @@           ["rewrite", "--output=latex", "--sweet", "--flat", "--label=foo"]           [ unlines               [ "\\begin{phiquation}\n\\label{foo}"-              , "[[ |x| -> 5 ]]{.}"+              , "5 : |x|{.}"               , "\\end{phiquation}"               ]           ]@@ -646,9 +646,9 @@             ]         )         ( testCLISucceeded-            ["rewrite", "--input=xmir", "--output=xmir", "--sweet"]+            ["rewrite", "--input=xmir", "--output=xmir", "--sweet", "--flat"]             [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"-            , "<listing>&lt;?xml version=&quot;1.0&quot; encoding=&quot;UTF-8&quot;?&gt;&lt;object&gt;&lt;o name=&quot;app&quot;&gt;&lt;o name=&quot;x&quot; base=&quot;Φ.number&quot;/&gt;&lt;/o&gt;&lt;/object&gt;</listing>"+            , "<listing>Φ.number:x:app</listing>"             ]         ) @@ -733,11 +733,11 @@           [ unlines               [ "\\begin{phiquation}"               , "% === Step #1"-              , "[[ |x| -> \"foo\" ]] \\leadsto_{\\nameref{r:first}}"+              , "\"foo\" : |x| \\leadsto_{\\nameref{r:first}}"               , "% === Step #2, Rule 'first', 23t -> 26t"               , "  \\leadsto Q . |x| ( |y| -> \"foo\" ) \\leadsto_{\\nameref{r:second}}"               , "% === Step #3, Rule 'second', 26t -> 23t"-              , "  \\leadsto [[ |x| -> \"foo\" ]]{.}"+              , "  \\leadsto \"foo\" : |x|{.}"               , "\\end{phiquation}"               ]           ]@@ -757,9 +757,9 @@           ]           [ unlines               [ "\\begin{phiquation}"-              , "[[ |x| -> \"foo\" ]] \\leadsto_{\\nameref{r:first}}"+              , "\"foo\" : |x| \\leadsto_{\\nameref{r:first}}"               , "  \\leadsto Q . |x| ( |y| -> \"foo\" ) \\leadsto_{\\nameref{r:second}}"-              , "  \\leadsto [[ |x| -> \"foo\" ]]{.}"+              , "  \\leadsto \"foo\" : |x|{.}"               , "\\end{phiquation}"               ]           ]@@ -770,12 +770,12 @@           ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress", "--meet-prefix=foo"]           [ unlines               [ "\\begin{phiquation}"-              , "[[ |x| -> ?, |y| -> |x| ]] ( |x| -> [[ D> |42-| ]] ) . |y| \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto \\phinoMeet{foo:1}{ [[ |x| -> [[ D> |42-| ]], |y| -> |x| ]] } . |y| \\leadsto_{\\nameref{r:dot}}"-              , "  \\leadsto [[ |x| -> [[ D> |42-| ]] ]] . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:1} ) \\leadsto_{\\nameref{r:dot}}"-              , "  \\leadsto [[ D> |42-| ]] ( \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |42-| ]] ]], \\phiTerminal{\\rho} -> \\phinoAgain{foo:1} ) \\leadsto_{\\nameref{r:skip}}"-              , "  \\leadsto [[ D> |42-| ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:1} ) \\leadsto_{\\nameref{r:skip}}"-              , "  \\leadsto [[ D> |42-| ]]{.}"+              , "[[ |x| -> ?, |y| -> |x| ]] ( |x| -> |42-| : D ) . |y| \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto \\phinoMeet{foo:1}{ [[ |x| -> |42-| : D, |y| -> |x| ]] } . |y| \\leadsto_{\\nameref{r:dot}}"+              , "  \\leadsto |42-| : D : |x| . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:1} ) \\leadsto_{\\nameref{r:dot}}"+              , "  \\leadsto |42-| : D ( \\phiTerminal{\\rho} -> |42-| : D : |x|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:1} ) \\leadsto_{\\nameref{r:skip}}"+              , "  \\leadsto |42-| : D ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:1} ) \\leadsto_{\\nameref{r:skip}}"+              , "  \\leadsto |42-| : D{.}"               , "\\end{phiquation}"               ]           ]@@ -786,12 +786,12 @@           ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress"]           [ unlines               [ "\\begin{phiquation}"-              , "[[ |x| -> ?, |y| -> |x| ]] ( |x| -> [[ D> |42-| ]] ) . |y| \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto \\phinoMeet{1}{ [[ |x| -> [[ D> |42-| ]], |y| -> |x| ]] } . |y| \\leadsto_{\\nameref{r:dot}}"-              , "  \\leadsto [[ |x| -> [[ D> |42-| ]] ]] . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{1} ) \\leadsto_{\\nameref{r:dot}}"-              , "  \\leadsto [[ D> |42-| ]] ( \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |42-| ]] ]], \\phiTerminal{\\rho} -> \\phinoAgain{1} ) \\leadsto_{\\nameref{r:skip}}"-              , "  \\leadsto [[ D> |42-| ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{1} ) \\leadsto_{\\nameref{r:skip}}"-              , "  \\leadsto [[ D> |42-| ]]{.}"+              , "[[ |x| -> ?, |y| -> |x| ]] ( |x| -> |42-| : D ) . |y| \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto \\phinoMeet{1}{ [[ |x| -> |42-| : D, |y| -> |x| ]] } . |y| \\leadsto_{\\nameref{r:dot}}"+              , "  \\leadsto |42-| : D : |x| . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{1} ) \\leadsto_{\\nameref{r:dot}}"+              , "  \\leadsto |42-| : D ( \\phiTerminal{\\rho} -> |42-| : D : |x|, \\phiTerminal{\\rho} -> \\phinoAgain{1} ) \\leadsto_{\\nameref{r:skip}}"+              , "  \\leadsto |42-| : D ( \\phiTerminal{\\rho} -> \\phinoAgain{1} ) \\leadsto_{\\nameref{r:skip}}"+              , "  \\leadsto |42-| : D{.}"               , "\\end{phiquation}"               ]           ]@@ -802,9 +802,9 @@           ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet"]           [ unlines               [ "\\begin{phiquation}"-              , "[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> \\phinoMeet{1}{ [[ |t| -> 42 ]] } ]] ( |y| -> \\phinoAgain{1} ) ]] . |i| ]] \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto [[ |ex| -> [[ |x| -> [[ |y| -> \\phinoAgain{1}, |k| -> \\phinoAgain{1} ]] ]] . |i| ]] \\leadsto_{\\nameref{r:stop}}"-              , "  \\leadsto [[ |ex| -> T ]]{.}"+              , "[[ |y| -> ?, |k| -> \\phinoMeet{1}{ 42 : |t| } ]] ( |y| -> \\phinoAgain{1} ) : |x| . |i| : |ex| \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto [[ |y| -> \\phinoAgain{1}, |k| -> \\phinoAgain{1} ]] : |x| . |i| : |ex| \\leadsto_{\\nameref{r:stop}}"+              , "  \\leadsto T : |ex|{.}"               , "\\end{phiquation}"               ]           ]@@ -815,9 +815,9 @@           ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet", "--meet-popularity=70"]           [ unlines               [ "\\begin{phiquation}"-              , "[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| ]] \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto [[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| ]] \\leadsto_{\\nameref{r:stop}}"-              , "  \\leadsto [[ |ex| -> T ]]{.}"+              , "[[ |y| -> ?, |k| -> 42 : |t| ]] ( |y| -> 42 : |t| ) : |x| . |i| : |ex| \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto [[ |y| -> 42 : |t|, |k| -> 42 : |t| ]] : |x| . |i| : |ex| \\leadsto_{\\nameref{r:stop}}"+              , "  \\leadsto T : |ex|{.}"               , "\\end{phiquation}"               ]           ]@@ -828,9 +828,9 @@           ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet", "--meet-length=32"]           [ unlines               [ "\\begin{phiquation}"-              , "[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| ]] \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto [[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| ]] \\leadsto_{\\nameref{r:stop}}"-              , "  \\leadsto [[ |ex| -> T ]]{.}"+              , "[[ |y| -> ?, |k| -> 42 : |t| ]] ( |y| -> 42 : |t| ) : |x| . |i| : |ex| \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto [[ |y| -> 42 : |t|, |k| -> 42 : |t| ]] : |x| . |i| : |ex| \\leadsto_{\\nameref{r:stop}}"+              , "  \\leadsto T : |ex|{.}"               , "\\end{phiquation}"               ]           ]@@ -841,8 +841,8 @@           ["rewrite", "--normalize", "--sequence", "--flat", "--output=latex", "--sweet", "--focus=Q.ex"]           [ unlines               [ "\\begin{phiquation}"-              , "[[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| \\leadsto_{\\nameref{r:stop}}"+              , "[[ |y| -> ?, |k| -> 42 : |t| ]] ( |y| -> 42 : |t| ) : |x| . |i| \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto [[ |y| -> 42 : |t|, |k| -> 42 : |t| ]] : |x| . |i| \\leadsto_{\\nameref{r:stop}}"               , "  \\leadsto T{.}"               , "\\end{phiquation}"               ]@@ -866,7 +866,7 @@           [ unlines               [ "\\begin{phiquation}"               , "[[ |x| -> |y|, |y| -> |x| ]] . |x| \\leadsto_{\\nameref{r:dot}}"-              , "  \\leadsto [[ |y| -> |x| ]] . |y| ( \\phiTerminal{\\rho} -> [[ |x| -> |y|, |y| -> |x| ]] ) \\leadsto"+              , "  \\leadsto |x| : |y| . |y| ( \\phiTerminal{\\rho} -> [[ |x| -> |y|, |y| -> |x| ]] ) \\leadsto"               , "  \\leadsto \\dots"               , "\\end{phiquation}"               ]@@ -1047,6 +1047,18 @@           ["rewrite", "--sweet", "--flat", "--show=Q.org", "--hide=Q.org.eolang"]           ["Φ.y:yegor256:org"] +    it "fails on a --show locator that matches nothing" $+      withStdin "[[ a -> [[ b -> Q, c -> Q ]], d -> Q ]]" $+        testCLIFailed+          ["rewrite", "--flat", "--show=Q.zzz"]+          ["[ERROR]:", "Can't find object by locator: 'Φ.zzz'"]++    it "shows the whole program with --show=Q" $+      withStdin "[[ a -> [[ b -> Q, c -> Q ]], d -> Q ]]" $+        testCLISucceeded+          ["rewrite", "--flat", "--show=Q"]+          ["⟦ a ↦ ⟦ b ↦ Φ, c ↦ Φ ⟧, d ↦ Φ ⟧"]+     it "prints in line with --flat" $       withStdin "[[ x -> 5, y -> \"hey\", z -> [[ w -> [[ ]] ]] ]]" $         testCLISucceeded@@ -1262,10 +1274,10 @@           [ intercalate               "\n"               [ "\\begin{phiquation}"-              , "[[ @ -> [[ |x| -> [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| ]] \\leadsto_{\\nameref{r:contextualize}}"-              , "  \\leadsto [[ |x| -> [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] . |x| \\leadsto_{\\nameref{r:dot}}"-              , "  \\leadsto [[ D> |01-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] ) \\leadsto_{\\nameref{r:skip}}"+              , "[[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) : |x| . |x| : @ \\leadsto_{\\nameref{r:contextualize}}"+              , "  \\leadsto [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) : |x| . |x| \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto [[ D> |01-|, |y| -> [[]] ]] : |x| . |x| \\leadsto_{\\nameref{r:dot}}"+              , "  \\leadsto [[ D> |01-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ D> |01-|, |y| -> [[]] ]] : |x| ) \\leadsto_{\\nameref{r:skip}}"               , "  \\leadsto [[ D> |01-|, |y| -> [[]] ]] \\leadsto_{\\nameref{r:delta}}"               , "  \\leadsto |01-|{.}"               , "\\end{phiquation}"@@ -1279,7 +1291,7 @@           ["dataize", "--sequence", "--quiet", "--output=latex", "--flat", "--sweet"]           [ intercalate               "\n"-              [ "[[ D> |01-| ]] \\leadsto_{\\nameref{r:delta}}"+              [ "|01-| : D \\leadsto_{\\nameref{r:delta}}"               , "  \\leadsto |01-|{.}"               , "\\end{phiquation}"               ]@@ -1303,6 +1315,10 @@           ["dataize", symbolic, "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--meet-length=5", "--meet-popularity=1"]           ["\\phinoMeet{dataization:1}"] +    it "canonizes the residue it prints with --partial" $+      withStdin "[[ @ -> [[ L> Foo ]] ]]" $+        testCLISucceeded ["dataize", "--partial", "--canonize", "--flat", "--sweet"] ["Fn1:λ"]+     it "dataizes with --locator" $       withStdin "[[ ex -> [[ @ -> Q.x ]], x -> [[ D> 42- ]] ]]" $         testCLISucceeded ["dataize", "--locator=Q.ex"] ["42-"]@@ -1313,7 +1329,8 @@      -- A formation spelled flat in the protocol can run for tens of thousands     -- of characters, so '--abridged' folds a long one down to what says what-    -- it holds and fires, and cuts a long byte string to its head (#1465)+    -- it holds and fires, and cuts a long byte string to its ends (#1465);+    -- the width past which it folds is the value of the option (#1530)     describe "--abridged" $ do       let wide = "⟦ t ↦ ⟦ φ ↦ ⟦ Δ ⤍ 01-02 ⟧, anfang ↦ ξ.schluss, mitte ↦ ξ.anfang, schluss ↦ ξ.mitte, rand ↦ ξ.schluss ⟧ ⟧"       it "folds a long formation in the text protocol" $@@ -1322,14 +1339,31 @@           withStdin wide $             testCLISucceeded ["dataize", "--locator=Q.t", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] []           records <- readUtf8 path-          lines records `shouldContain` ["  formation(⟦ φ ↦ 01-02:Δ, +4 attrs ⟧)  # 𝔻(Φ.t)"]+          lines records `shouldContain` ["  formation(⟦ φ ↦ 01-02:Δ, +4 ⟧)  # 𝔻(Φ.t)"]       it "folds a long formation in the XML protocol" $         withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do           hClose stream           withStdin wide $             testCLISucceeded ["dataize", "--locator=Q.t", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] []           records <- readUtf8 path-          lines records `shouldContain` ["  <formation at=\"Φ.t\" term=\"⟦ φ ↦ 01-02:Δ, +4 attrs ⟧\">"]+          lines records `shouldContain` ["  <formation at=\"Φ.t\" term=\"⟦ φ ↦ 01-02:Δ, +4 ⟧\">"]+      it "folds a long formation under the width given as the value" $+        withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do+          hClose stream+          withStdin wide $+            testCLISucceeded ["dataize", "--locator=Q.t", "--protocol=" ++ path, "--abridged=64", "--sweet", "--hide-rho", "--quiet"] []+          records <- readUtf8 path+          lines records `shouldContain` ["  formation(⟦ φ ↦ 01-02:Δ, +4 ⟧)  # 𝔻(Φ.t)"]+      it "keeps a formation whole under a width it fits in" $+        withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do+          hClose stream+          withStdin wide $+            testCLISucceeded ["dataize", "--locator=Q.t", "--protocol=" ++ path, "--abridged=200", "--sweet", "--hide-rho", "--quiet"] []+          records <- readUtf8 path+          lines records `shouldContain` ["  formation(⟦ φ ↦ 01-02:Δ, anfang ↦ schluss, mitte ↦ anfang, schluss ↦ mitte, rand ↦ schluss ⟧)  # 𝔻(Φ.t)"]+      it "refuses a width that is not a number" $+        withStdin wide $+          testCLIFailed ["dataize", "--locator=Q.t", "--protocol=breit.txt", "--abridged=breit"] ["cannot parse value `breit'"]       it "leaves the printed result whole" $         withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do           hClose stream@@ -1501,6 +1535,36 @@                        , "    𝑛.1.2 := 𝜎1:λ:z  # 𝕄(𝑛.1.1)"                        ] +      -- A firing the memo answers with a kept stall, a firing that ends stuck+      -- and a step budget running out each leave an element of their own in+      -- the markup, the way a cut leaves '<looped>' (#1524)+      it "writes a told stall to the XML protocol" $+        withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do+          hClose stream+          withLambdasOf (T.pack "- λ: L_outer\n  dataize:\n    𝛿1: ξ.arg\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n") $ \outer ->+            withStdin "⟦ x ↦ ⟦ arg ↦ ⟦ λ ⤍ L_none ⟧, λ ⤍ L_outer ⟧, y ↦ ⟦ arg ↦ ⟦ λ ⤍ L_none ⟧, λ ⤍ L_outer ⟧ ⟧" $+              testCLISucceeded ["morph", "--symbolic=" ++ outer, "--deep", "--partial", "--acyclic=plausible", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []+          records <- readUtf8 path+          lines records `shouldContain` ["    <stall λ=\"L_none\"/>"]++      it "writes a stuck firing to the XML protocol" $+        withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do+          hClose stream+          withLambdasOf (T.pack "- λ: L_outer\n  dataize:\n    𝛿1: ξ.arg\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n") $ \outer ->+            withStdin "⟦ x ↦ ⟦ arg ↦ ⟦ λ ⤍ L_absent ⟧, λ ⤍ L_outer ⟧ ⟧" $+              testCLISucceeded ["morph", "--symbolic=" ++ outer, "--deep", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []+          records <- readUtf8 path+          lines records `shouldContain` ["    <unfinished λ=\"L_absent\"/>"]++      it "writes a starved step budget to the XML protocol" $+        withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do+          hClose stream+          withLambdasOf (T.pack "- λ: L_outer\n  dataize:\n    𝛿1: ξ.arg\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n") $ \outer ->+            withStdin "⟦ x ↦ ⟦ arg ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ Δ ⤍ 07- ⟧ ⟧ ⟧, λ ⤍ L_outer ⟧ ⟧" $+              testCLISucceeded ["dataize", "--symbolic=" ++ outer, "--locator=Q.x", "--partial", "--max-steps=3", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho", "--flat"] []+          records <- readUtf8 path+          lines records `shouldContain` ["        <starved limit=\"3\" by=\"dataize\" at=\"Φ.a🌵0\"/>"]+       it "keeps the lines of a run that fails" $         withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do           hClose stream@@ -1521,7 +1585,7 @@                        , "      𝛿2.1 := 40-18-00-00-00-00-00-00  # 𝔻(ξ.x)"                        , "      𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ )  # 𝑛"                        , "      𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧  # 𝕄(𝑛.1.1)"-                       , "    ?(L_number_nope)  # 𝔻(L_number_nope:λ)"+                       , "    unanswered(L_number_nope)  # 𝔻(L_number_nope:λ)"                        ]        it "truncates the lines left over from the previous run" $@@ -1830,7 +1894,7 @@                          ]          -- Nothing fired, so the element stands alone and nothing opens under-        -- it, exactly as '?(…)' stands alone in the text format; the formation+        -- it, exactly as 'unanswered(…)' stands alone in the text format; the formation         -- 𝔼 was asked about stands as the text of it, the way the comment of         -- the text format carries it (#1300)         it "records a λ function no entry answers as a childless element" $@@ -1858,7 +1922,7 @@                          , "      <built meta=\"𝑛.1.1\">Φ.number( φ ↦ 𝜎1:λ )</built>"                          , "      <answer meta=\"𝑛.1.2\">⟦ φ ↦ 𝜎1:λ, times(x) ↦ L_number_times:λ, nope ↦ L_number_nope:λ ⟧</answer>"                          , "    </evaluate>"-                         , "    <stuck λ=\"L_number_nope\" by=\"dataize\">L_number_nope:λ</stuck>"+                         , "    <unanswered λ=\"L_number_nope\" by=\"dataize\">L_number_nope:λ</unanswered>"                          , "  </formation>"                          , "</dataize>"                          ]@@ -1876,7 +1940,7 @@             lines records               `shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"                          , "<morph at=\"Φ.x\">"-                         , "  <stuck λ=\"L_number_nope\" by=\"morph\">⟦ λ ⤍ L_number_nope ⟧</stuck>"+                         , "  <unanswered λ=\"L_number_nope\" by=\"morph\">⟦ λ ⤍ L_number_nope ⟧</unanswered>"                          , "</morph>"                          ] @@ -1909,7 +1973,7 @@                          , "      <built meta=\"𝑛.1.1\">Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )</built>"                          , "      <answer meta=\"𝑛.1.2\">⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, times ↦ ⟦ ρ ↦ ∅, x ↦ ∅, λ ⤍ L_number_times ⟧, nope ↦ ⟦ ρ ↦ ∅, λ ⤍ L_number_nope ⟧ ⟧</answer>"                          , "    </evaluate>"-                         , "    <stuck λ=\"L_number_nope\" by=\"dataize\">⟦ ρ ↦ Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ), λ ⤍ L_number_nope ⟧</stuck>"+                         , "    <unanswered λ=\"L_number_nope\" by=\"dataize\">⟦ ρ ↦ Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ), λ ⤍ L_number_nope ⟧</unanswered>"                          , "  </formation>"                          , "</dataize>"                          ]@@ -1936,7 +2000,7 @@                          , "    <built meta=\"𝑛.1.1\">⟦ λ ⤍ 𝜎1 ⟧</built>"                          , "    <answer meta=\"𝑛.1.2\">⟦ λ ⤍ 𝜎1 ⟧</answer>"                          , "  </evaluate>"-                         , "  <stuck λ=\"𝜎1\" by=\"morph\">⟦ λ ⤍ 𝜎1 ⟧</stuck>"+                         , "  <unanswered λ=\"𝜎1\" by=\"morph\">⟦ λ ⤍ 𝜎1 ⟧</unanswered>"                          , "</morph>"                          ] @@ -1957,6 +2021,7 @@     describe "--partial" $ do       let stuck = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ times(^, x) -> [[ L> L_number_times ]], nope -> [[ ^ -> ?, L> L_number_nope ]] ]], @ -> 2.times(3).nope ]]"           dispatched = "[[ foo -> [[ bar -> [[ ^ -> ?, L> L_number_nope ]] ]], @ -> Q.foo.bar ]]"+          wrapped = "[[ app -> [[ foo -> [[ bar -> [[ ^ -> ?, L> L_number_nope ]] ]], @ -> Q.app.foo.bar ]] ]]"       it "fails on a λ function that cannot fire without the flag" $         withStdin stuck $           testCLIFailed@@ -1995,34 +2060,32 @@                        , "      𝛿2.1 := 40-08-00-00-00-00-00-00  # 𝔻(ξ.x)"                        , "      𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ )  # 𝑛"                        , "      𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, times(x) ↦ L_number_times:λ, nope ↦ L_number_nope:λ ⟧  # 𝕄(𝑛.1.1)"-                       , "    ?(L_number_nope)  # 𝔻(L_number_nope:λ)"+                       , "    unanswered(L_number_nope)  # 𝔻(L_number_nope:λ)"                        ]        it "still prints bytes when nothing gets stuck" $         withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $           testCLISucceeded ["dataize", symbolic, "--partial"] ["40-45-00-00-00-00-00-00"] -      -- The residual is an arbitrary formation, and a multi-binding <object>-      -- is exactly what XMIR now carries: one <o> per binding (#1076)       it "prints the residual to XMIR, with its real listing by default" $-        withStdin dispatched $+        withStdin wrapped $           testCLISucceeded-            ["dataize", symbolic, "--partial", "--output=xmir"]-            ["<o name=\"λ\">L_number_nope</o>", "<o base=\"Φ.foo\" name=\"ρ\"/>", "<listing>⟦"]+            ["dataize", symbolic, "--partial", "--locator=Q.app", "--output=xmir"]+            ["<o name=\"λ\">L_number_nope</o>", "<o name=\"app\">", "<listing>⟦"]        it "honors --hide-rho and --omit-listing when printing the residual to XMIR" $-        withStdin dispatched $+        withStdin wrapped $           testCLISucceeded-            ["dataize", symbolic, "--partial", "--output=xmir", "--hide-rho", "--omit-listing"]+            ["dataize", symbolic, "--partial", "--locator=Q.app", "--output=xmir", "--hide-rho", "--omit-listing"]             ["<o name=\"λ\">L_number_nope</o>", "line(s)</listing>"] -      -- A symbol is a name of the calculus, and XMIR carries no notation for-      -- one, so a residue standing for an unknown cannot be printed as XMIR-      it "cannot print a residue carrying a symbol as XMIR" $-        withStdin stuck $+      -- XMIR carries a single binding at the top, the shape 'rewrite' insists+      -- on, so a residual of several is refused the same way (#1444)+      it "cannot print a residual of several top bindings as XMIR" $+        withStdin dispatched $           testCLIFailed             ["dataize", symbolic, "--partial", "--output=xmir"]-            ["XMIR does not support such bindings"]+            ["[ERROR]:", "its top level must be a single binding"]        it "prints the chain of steps ending in the residue with --sequence" $         withStdin stuck $@@ -2187,6 +2250,18 @@      -- 𝕄 is total and 𝔻 is not: where the derivation dies, 𝕄 answers ⊥ ('xi'     -- here) and the run succeeds, while 𝔻 has no bytes to give and fails+    it "canonizes the answer it prints" $+      withStdin "[[ x -> [[ L> Foo ]], y -> [[ L> Bar ]] ]]" $+        testCLISucceeded ["morph", "--canonize", "--flat", "--sweet"] ["⟦ x ↦ Fn1:λ, y ↦ Fn2:λ ⟧"]++    it "hides a binding of the answer it prints" $+      withStdin "[[ x -> [[ L> Foo ]], y -> [[ L> Bar ]] ]]" $+        testCLISucceeded ["morph", "--hide=Q.x", "--flat", "--sweet"] ["Bar:λ:y"]++    it "shows only one binding of the answer it prints" $+      withStdin "[[ x -> [[ L> Foo ]], y -> [[ L> Bar ]] ]]" $+        testCLISucceeded ["morph", "--show=Q.x", "--flat", "--sweet"] ["Foo:λ:x"]+     it "prints ⊥ instead of failing the run" $       withStdin "[[ x -> $ ]]" $         testCLISucceeded ["morph", "--locator=Q.x"] ["⊥"]@@ -2480,6 +2555,12 @@               ["⟦ x ↦ ⟦ λ ⤍ L_loop ⟧.foo, y ↦ ⟦ z ↦ ⟦⟧ ⟧ ⟧"]      describe "fails" $ do+      it "with --output=xmir on a top formation of several bindings" $+        withStdin "[[ x -> [[ D> 01- ]], y -> [[ D> 02- ]] ]]" $+          testCLIFailed+            ["morph", "--output=xmir"]+            ["[ERROR]:", "its top level must be a single binding"]+       it "with --output != latex and --nonumber" $         withStdin "" $           testCLIFailed
test/CSTSpec.hs view
@@ -46,6 +46,7 @@         ( "[[ x -> Q.y ]]"         , EX_SINGLE             (PA_TAU (AT_LABEL "x") ARROW (EX_DISPATCH (EX_GLOBAL Φ) NO_SPACE (AT_LABEL "y")))+            NO_SPACE             ( EX_FORMATION                 LSB                 EOL
test/DataizeSpec.hs view
@@ -266,12 +266,12 @@           , "      𝛿2.1 := 40-08-00-00-00-00-00-00  # 𝔻(ξ.x)"           , "      𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ )  # 𝑛"           , "      𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, as-bytes ↦ φ, plus(ρ, x) ↦ L_number_plus:λ, times(ρ, x) ↦ L_number_times:λ, div(ρ, x) ↦ L_number_div:λ, gt(ρ, x) ↦ L_number_gt:λ, eq(ρ, x) ↦ ρ.as-bytes.eq( x.as-bytes ):φ, nope(ρ) ↦ L_number_nope:λ ⟧  # 𝕄(𝑛.1.1)"-          , "    ?(L_number_nope)  # 𝔻(⟦ ρ ↦ Φ.number( φ ↦ 𝜎1:λ ), λ ⤍ L_number_nope ⟧)"+          , "    unanswered(L_number_nope)  # 𝔻(⟦ ρ ↦ Φ.number( φ ↦ 𝜎1:λ ), λ ⤍ L_number_nope ⟧)"           ]     it "leaves an unanswered λ function dataized directly as the whole residue" $ do       ((outcome, chain), protocol) <- partially known "[[ L> Sym_arg_0 ]]"       outcome `shouldBe` Residual placeholder-      protocol `shouldBe` "  formation(⟦ bytes(φ) ↦ ⟦ not(ρ) ↦ L_bytes_not:λ, eq(ρ, b) ↦ L_bytes_eq:λ ⟧, bool(φ) ↦ ⟦ if(ρ, then, else) ↦ L_fork:λ ⟧, number(φ) ↦ ⟦ as-bytes ↦ φ, plus(ρ, x) ↦ L_number_plus:λ, times(ρ, x) ↦ L_number_times:λ, div(ρ, x) ↦ L_number_div:λ, gt(ρ, x) ↦ L_number_gt:λ, eq(ρ, x) ↦ ρ.as-bytes.eq( x.as-bytes ):φ, nope(ρ) ↦ L_number_nope:λ ⟧, φ ↦ Sym_arg_0:λ ⟧)  # 𝔻(Φ)\n    ?(Sym_arg_0)  # 𝔻(Sym_arg_0:λ)\n"+      protocol `shouldBe` "  formation(⟦ bytes(φ) ↦ ⟦ not(ρ) ↦ L_bytes_not:λ, eq(ρ, b) ↦ L_bytes_eq:λ ⟧, bool(φ) ↦ ⟦ if(ρ, then, else) ↦ L_fork:λ ⟧, number(φ) ↦ ⟦ as-bytes ↦ φ, plus(ρ, x) ↦ L_number_plus:λ, times(ρ, x) ↦ L_number_times:λ, div(ρ, x) ↦ L_number_div:λ, gt(ρ, x) ↦ L_number_gt:λ, eq(ρ, x) ↦ ρ.as-bytes.eq( x.as-bytes ):φ, nope(ρ) ↦ L_number_nope:λ ⟧, φ ↦ Sym_arg_0:λ ⟧)  # 𝔻(Φ)\n    unanswered(Sym_arg_0)  # 𝔻(Sym_arg_0:λ)\n"       map fst chain `shouldEndWith` [placeholder]     it "still reaches the manufactured datum when nothing is stuck" $ do       ((outcome, _), _) <- partially known "2.times(3)"@@ -284,7 +284,7 @@       case outcome of         Residual (ExFormation bds) -> bds `shouldContain` [BiLambda (Function "L_number_plus")]         other -> expectationFailure ("expected a residual formation, got " ++ show other)-      protocol `shouldSatisfy` isInfixOf "?(⊥)  # 𝔻(⊥)"+      protocol `shouldSatisfy` isInfixOf "unanswered(⊥)  # 𝔻(⊥)"    describe "ReduceContext's --max-depth/--max-cycles reach into the normalization it splices in" $ do     let boxed = "[[ @ -> [[ D> 00- ]] ]]"@@ -302,27 +302,28 @@       ]       ( \(flag, ctx, message) ->           it ("throws once " ++ flag ++ " is exhausted with --depth-sensitive") $ do-            expr <- parseExpressionThrows boxed+            expr <- parseExpressionThrows "[[ @ -> [[ x -> [[ D> 00- ]] ]].x ]]"             dataize expr emptyState ctx `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException))       )-    forM_-      [ ("--max-cycles", ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing Nothing 1 False True False False Nothing Dataization [] Map.empty emptyLambdas buildTerm reduction evaluation fired dontSaveStep dontSaveEval)-      , ("--max-depth", ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing Nothing 1 False True False False Nothing Dataization [] Map.empty emptyLambdas buildTerm reduction evaluation fired dontSaveStep dontSaveEval)-      ]-      ( \(flag, ctx) ->-          it ("does not throw without --depth-sensitive even once " ++ flag ++ " is exhausted") $ do-            expr <- parseExpressionThrows boxed-            (value, _, _) <- dataize expr emptyState ctx-            value `shouldBe` Dataized (BtOne "00")-      )+    it "does not throw without --depth-sensitive even once --max-depth is exhausted" $ do+      expr <- parseExpressionThrows boxed+      (value, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing Nothing 1 False True False False Nothing Dataization [] Map.empty emptyLambdas buildTerm reduction evaluation fired dontSaveStep dontSaveEval)+      value `shouldBe` Dataized (BtOne "00")+    -- A normalization that ran out of cycles hands back a term that is not a+    -- normal form, so the run names the budget even without --depth-sensitive+    -- rather than going on with it (#1496)+    it "throws once --max-cycles is exhausted even without --depth-sensitive" $ do+      expr <- parseExpressionThrows boxed+      dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing Nothing 1 False True False False Nothing Dataization [] Map.empty emptyLambdas buildTerm reduction evaluation fired dontSaveStep dontSaveEval)+        `shouldThrow` (\e -> "--max-cycles=0" `isInfixOf` show (e :: SomeException))    describe "labels every step with a defined rule or operation" $ do     let verb op = case op of-          Yaml.OpMorph _ -> "morph"+          Yaml.OpMorph _ _ -> "morph"           Yaml.OpNormalize _ -> "normalize"           Yaml.OpEvaluate _ _ -> "evaluate"           Yaml.OpContextualize _ _ -> "contextualize"-          Yaml.OpDataize _ -> "dataize"+          Yaml.OpDataize _ _ -> "dataize"         allowed =           map (.name) Yaml.morphingRules             ++ map (.name) Yaml.dataizationRules
test/EvaluateSpec.hs view
@@ -173,7 +173,7 @@         let stuck = (withLambdas known (defaultReduceContext ExRoot)){_saveEval = record}             fire = execBuildTerm univ stuck "evaluate" [ArgExpression (ExFormation [BiLambda (FnSymbol 1)]), ArgExpression univ] substEmpty         fire `shouldThrow` (\e -> "No entry of --symbolic answers the λ function '𝜎1'" `isInfixOf` show (e :: SomeException))-      written `shouldBe` "  ?(𝜎1)  # 𝕄(𝜎1:λ)\n"+      written `shouldBe` "  unanswered(𝜎1)  # 𝕄(𝜎1:λ)\n"      -- Two λ bindings never reach 𝔼: the builder refuses to make a formation out     -- of them first. The case is here anyway, since what matters is that such a
test/FilterSpec.hs view
@@ -46,7 +46,7 @@           included <- traverse parseExpressionThrows shown           excluded <- traverse parseExpressionThrows hidden           res <- parseExpressionThrows result-          let [(expr', _)] = F.exclude (F.include [(expr, Nothing)] included) excluded+          [(expr', _)] <- (`F.exclude` excluded) <$> F.include [(expr, Nothing)] included           expr' `shouldBe` res       ) @@ -75,24 +75,34 @@      describe "include" $ do       forM_-        [ ("falls back to the default hidden formation when the fqn is not a Q-dispatch chain", "[[ x -> ? ]]", "$.x")-        , ("falls back to the default hidden formation when nothing matches the fqn", "[[ x -> ? ]]", "Q.absent")-        , ("falls back to the default hidden formation for a non-formation expression", "Q.x", "Q.y")+        [ ("fails when the fqn is not a Q-dispatch chain", "[[ x -> ? ]]", "$.x")+        , ("fails when nothing matches the fqn", "[[ x -> ? ]]", "Q.absent")+        , ("fails when a nested fqn stops short of its last attribute", "[[ a -> [[ b -> ? ]] ]]", "Q.a.zzz")+        , ("fails for a non-formation expression", "Q.x", "Q.y")         ]         ( \(desc, exprText, fqnText) -> it desc $ do             expr <- parseExpressionThrows exprText             fqn <- parseExpressionThrows fqnText-            defaultHidden <- parseExpressionThrows "[[ ]]"-            let [(expr', _)] = F.include [(expr, Nothing)] [fqn]-            expr' `shouldBe` defaultHidden+            F.include [(expr, Nothing)] [fqn] `shouldThrow` anyException         ) +      it "keeps the whole program when the fqn is Q" $ do+        expr <- parseExpressionThrows "[[ a -> [[ b -> ?, c -> ? ]], d -> ? ]]"+        [(expr', _)] <- F.include [(expr, Nothing)] [ExRoot]+        expr' `shouldBe` expr++      it "fails when one of several fqns matches nothing" $ do+        expr <- parseExpressionThrows "[[ x -> ?, y -> ? ]]"+        found <- parseExpressionThrows "Q.x"+        absent <- parseExpressionThrows "Q.zzz"+        F.include [(expr, Nothing)] [found, absent] `shouldThrow` anyException+       it "recurses over a multi-element rewrite list, pinning every element to the fqns" $ do         first' <- parseExpressionThrows "[[ x -> ?, y -> ? ]]"         second' <- parseExpressionThrows "[[ x -> ?, y -> ? ]]"         fqn <- parseExpressionThrows "Q.x"         expected <- parseExpressionThrows "[[ x -> ? ]]"-        let included = F.include [(first', Just "rule-a"), (second', Just "rule-b")] [fqn, ExRoot]+        included <- F.include [(first', Just "rule-a"), (second', Just "rule-b")] [fqn]         map fst included `shouldBe` [expected, expected]         map snd included `shouldBe` [Just "rule-a", Just "rule-b"] @@ -101,5 +111,5 @@         firstFqn <- parseExpressionThrows "Q.x"         secondFqn <- parseExpressionThrows "Q.y"         expected <- parseExpressionThrows "[[ x -> ?, y -> ? ]]"-        let [(expr', _)] = F.include [(expr, Nothing)] [firstFqn, secondFqn]+        [(expr', _)] <- F.include [(expr, Nothing)] [firstFqn, secondFqn]         expr' `shouldBe` expected
test/Fixtures.hs view
@@ -144,7 +144,7 @@       PrintCtx         SWEET         hidden-        False+        Nothing         MULTILINE         2         defaultXmirContext
test/LaTeXSpec.hs view
@@ -142,17 +142,17 @@       [         ( "renders '\\phiquation*' (unnumbered) when '_nonumber' is set"         , \ctx -> ctx{_nonumber = True}-        , "\\begin{phiquation*}\n[[ |x| -> Q . |y| ]]{.}\n\\end{phiquation*}"+        , "\\begin{phiquation*}\nQ . |y| : |x|{.}\n\\end{phiquation*}"         )       ,         ( "renders a '\\label{}' when '_label' is set"         , \ctx -> ctx{_label = Just "eq:one"}-        , "\\begin{phiquation}\n\\label{eq:one}\n[[ |x| -> Q . |y| ]]{.}\n\\end{phiquation}"+        , "\\begin{phiquation}\n\\label{eq:one}\nQ . |y| : |x|{.}\n\\end{phiquation}"         )       ,         ( "renders a '\\phiExpression{}' prefix when '_expression' is set"         , \ctx -> ctx{_expression = Just "e"}-        , "\\begin{phiquation}\n\\phiExpression{e} [[ |x| -> Q . |y| ]]{.}\n\\end{phiquation}"+        , "\\begin{phiquation}\n\\phiExpression{e} Q . |y| : |x|{.}\n\\end{phiquation}"         )       ]       ( \(desc, adjustContext, expected) -> it desc $ do@@ -163,17 +163,17 @@     it "renders a non-finite double as a piped dispatch off the root" $ do       nan <- parseExpressionThrows "[[ x -> Q.number(Q.bytes([[ D> 7F-F8-00-00-00-00-00-00 ]])) ]]"       expressionToLaTeX nan defaultLatexContext-        `shouldBe` "\\begin{phiquation}\n[[ |x| -> Q . |nan| ]]{.}\n\\end{phiquation}"+        `shouldBe` "\\begin{phiquation}\nQ . |nan| : |x|{.}\n\\end{phiquation}"      it "renders a bytes meta with the '\\delta' head" $ do       bts <- parseExpressionThrows "[[ D> !d7 ]]"       expressionToLaTeX bts defaultLatexContext-        `shouldBe` "\\begin{phiquation}\n[[ D> \\delta_7 ]]{.}\n\\end{phiquation}"+        `shouldBe` "\\begin{phiquation}\n\\delta_7 : D{.}\n\\end{phiquation}"      it "escapes '@' and '^' in an attribute label, same as '$' and '_'" $ do       let weird = ExFormation [BiTau (AtLabel "a@b^c") ExRoot]       expressionToLaTeX weird defaultLatexContext-        `shouldBe` "\\begin{phiquation}\n[[ |a\\char64{}b\\char94{}c| -> Q ]]{.}\n\\end{phiquation}"+        `shouldBe` "\\begin{phiquation}\nQ : |a\\char64{}b\\char94{}c|{.}\n\\end{phiquation}"      forM_       [@@ -196,7 +196,7 @@     it "renders the ellipsis ending when the chain exceeded its bound" $ do       step1 <- parseExpressionThrows "[[ x -> Q.y ]]"       latex <- rewrittensToLatex ([(step1, Nothing)], True) defaultLatexContext-      latex `shouldBe` "\\begin{phiquation}\n[[ |x| -> Q . |y| ]] \\leadsto\n  \\leadsto \\dots\n\\end{phiquation}"+      latex `shouldBe` "\\begin{phiquation}\nQ . |y| : |x| \\leadsto\n  \\leadsto \\dots\n\\end{phiquation}"      it "prefixes each step with a '% === Step' header when '_headers' is set" $ do       step1 <- parseExpressionThrows "[[ x -> Q.y ]]"@@ -207,9 +207,9 @@           "\n"           [ "\\begin{phiquation}"           , "% === Step #1"-          , "[[ |x| -> Q . |y| ]]"+          , "Q . |y| : |x|"           , "% === Step #2, Rule '?', 7t -> 7t"-          , "  \\leadsto [[ |x| -> Q . |z| ]] \\leadsto_{\\nameref{r:myrule}}{.}"+          , "  \\leadsto Q . |z| : |x| \\leadsto_{\\nameref{r:myrule}}{.}"           , "\\end{phiquation}"           ] @@ -239,9 +239,9 @@         `shouldBe` intercalate           "\n"           [ "\\begin{phiquation}"-          , "[[ |x| -> \\phinoMeet{1}{ Q . |a| . |b| . |c| . |d| } ]]"-          , "  \\leadsto [[ |y| -> \\phinoAgain{1} ]] \\leadsto_{\\nameref{r:r1}}"-          , "  \\leadsto [[ |z| -> \\phinoAgain{1} ]] \\leadsto_{\\nameref{r:r2}}{.}"+          , "\\phinoMeet{1}{ Q . |a| . |b| . |c| . |d| } : |x|"+          , "  \\leadsto \\phinoAgain{1} : |y| \\leadsto_{\\nameref{r:r1}}"+          , "  \\leadsto \\phinoAgain{1} : |z| \\leadsto_{\\nameref{r:r2}}{.}"           , "\\end{phiquation}"           ] @@ -258,7 +258,7 @@         `shouldBe` intercalate           "\n"           [ "\\begin{phiquation}"-          , "\\phinoMeet{1}{ [[ |w| -> Q . |a| . |b| . |c| . |d| ]] }"+          , "\\phinoMeet{1}{ Q . |a| . |b| . |c| . |d| : |w| }"           , "  \\leadsto \\phinoAgain{1} \\leadsto_{\\nameref{r:r1}}"           , "  \\leadsto \\phinoAgain{1} \\leadsto_{\\nameref{r:r2}}{.}"           , "\\end{phiquation}"@@ -327,7 +327,7 @@         ,           [ "\\phinoNormalizationRule{lambdas}"           , "{ [[ B_1, L> f, B_2 ]] }"-          , "{ [[ L> \\sigma_1 ]] }"+          , "{ \\sigma_1 : L }"           , "{ }"           , "{ }"           ]@@ -386,11 +386,11 @@               , nresult = ExMeta "n1"               , when = Just (Y.NF (ExMeta "n"))               , premises =-                  [ Y.Premise{result = "n1", operation = Y.OpMorph (ExMeta "n")}+                  [ Y.Premise{result = "n1", operation = Y.OpMorph (ExMeta "n") (ExMeta "e")}                   , Y.Premise{result = "n2", operation = Y.OpNormalize (ExMeta "n1")}                   , Y.Premise{result = "n3", operation = Y.OpEvaluate (ExMeta "n2") (ExMeta "e")}                   , Y.Premise{result = "n4", operation = Y.OpContextualize (ExMeta "n3") (ExMeta "e")}-                  , Y.Premise{result = "n5", operation = Y.OpDataize (ExMeta "n4")}+                  , Y.Premise{result = "n5", operation = Y.OpDataize (ExMeta "n4") (ExMeta "e")}                   ]               }       explainMorphRules [rule]@@ -431,7 +431,7 @@           ]    describe "explainContextualizeRules" $-    it "threads a morph premise through the rule's own 'e' universe" $ do+    it "renders a morph premise in the universe it names, not in a free 'e'" $ do       let rule =             Y.ContextualizeRule               { name = "ctx1"@@ -439,14 +439,14 @@               , match = ExMeta "n"               , cmatch = ExMeta "c"               , cresult = ExMeta "n1"-              , premises = [Y.Premise{result = "n1", operation = Y.OpMorph (ExMeta "n")}]+              , premises = [Y.Premise{result = "n1", operation = Y.OpMorph (ExMeta "n") ExRoot}]               }       explainContextualizeRules [rule]         `shouldBe` intercalate           "\n"           [ "\\begin{phinoContextualizationInference}"           , "  \\phinoName{ctx1}"-          , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"+          , "  \\phinoPremise{ \\phinoMorph{ n }{ Q }{ s_1 }{ n_1 }{ s_2 } }"           , "  \\phinoConclusion{ \\phinoContextualize{ n }{ e }{ n_1 } }"           , "\\end{phinoContextualizationInference}"           ]@@ -504,7 +504,7 @@               , ematch = ExMeta "e1"               , nresult = ExMeta "n1"               , when = Nothing-              , premises = [Y.Premise{result = "d1", operation = Y.OpDataize (ExMeta "n1")}]+              , premises = [Y.Premise{result = "d1", operation = Y.OpDataize (ExMeta "n1") (ExMeta "e1")}]               }       explainMorphRules [rule]         `shouldBe` intercalate
test/LambdasSpec.hs view
@@ -67,6 +67,11 @@       known <- lambdasOf (entry "L_box_[0-9]+_number")       answering known "L_box_42_number" `shouldBe` Just "L_box_[0-9]+_number" +    -- Two families no one λ name belongs to both of stand side by side+    it "reads two keys whose families share no λ name" $ do+      known <- lambdasOf (entry "L_[a-z]+_plus" <> entry "L_number_[0-9]+")+      answering known "L_number_42" `shouldBe` Just "L_number_[0-9]+"+     -- The expression matches the whole name and not a part of it, so a plain     -- name keeps meaning that one λ function     it "cannot read a λ function whose name merely starts with a key" $ do@@ -169,6 +174,12 @@         , entry "L_(foo|bar)" <> entry "L_foo"         , "match some of the same lambda names"         )+      ,+        ( "two keys overlapping on a name neither of them spells"+        , entry "L_[a-z]+_plus" <> entry "L_number_[a-z]+"+        , "such as 'L_number_plus'"+        )+      , ("a key with a back reference phino cannot compare", entry "L_(a)\\1", "cannot be compared")       , ("a key which is no regular expression", entry "L_[pair", "is not a regular expression")       , ("an operand of 'dataize' which is no bytes meta", "- λ: L_pair\n  dataize:\n    𝑛1: $.x\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n", "is not a bytes meta")       , ("an operand of 'morph' which is no expression meta", "- λ: L_pair\n  morph:\n    𝛿1: $.x\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n", "is not an expression meta")
+ test/LanguageSpec.hs view
@@ -0,0 +1,62 @@+{-# LANGUAGE OverloadedStrings #-}++-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++-- Tests for the languages of '--symbolic' keys, which tell whether two keys+-- match one λ name, whether or not either of them spells it.+module LanguageSpec where++import Control.Monad (forM_)+import Data.Either (fromLeft)+import Data.List (isInfixOf)+import Data.Text (Text)+import Language (language, shared)+import Test.Hspec (Spec, describe, it, shouldBe, shouldSatisfy)++-- The name two keys both match, or nothing, or the reason one cannot be read.+common :: Text -> Text -> Either String (Maybe Text)+common first second = shared <$> language first <*> language second++spec :: Spec+spec = do+  describe "shared" $+    forM_+      [ ("L_[a-z]+_plus", "L_number_[a-z]+", Just "L_number_plus")+      , ("L_(foo|bar)", "L_foo", Just "L_foo")+      , ("L_number_(plus|times)", "L_number_gt", Nothing)+      , ("L_[a-z]+_plus", "L_number_[0-9]+", Nothing)+      , ("L_x{2,3}", "L_x{4,}", Nothing)+      , ("L_x{2,3}", "L_x+?", Just "L_xx")+      , ("L_\\d\\w*", "L_[^0-8]", Just "L_9")+      , ("L_.", "L_\\n", Nothing)+      , ("L_(?:ab)*", "L_(?<pair>ab){2}", Just "L_abab")+      , ("L_[]a-]", "L_-", Just "L_-")+      , ("L_[\\]]", "L_\\]", Just "L_]")+      , ("L_a{,2}", "L_a\\{,2}", Just "L_a{,2}")+      , ("", "x?", Just "")+      , ("L_é+", "L_[^a-z]", Just "L_é")+      ]+      ( \(first, second, answer) ->+          it ("tells what '" <> show first <> "' and '" <> show second <> "' both match") $+            common first second `shouldBe` Right answer+      )++  describe "language" $+    forM_+      [ ("L_(a)\\1", "cannot be compared")+      , ("L_(?=a)a", "cannot be compared")+      , ("^L_a", "cannot be compared")+      , ("L_a++", "cannot be compared")+      , ("L_[[:alpha:]]", "cannot be compared")+      , ("L_\\bfoo", "cannot be compared")+      , ("L_[z-a]", "runs backwards")+      , ("L_(a", "not closed")+      , ("L_a)", "not expected")+      , ("L_[a", "not closed")+      , ("*a", "quantifies nothing")+      ]+      ( \(key, message) ->+          it ("cannot read the key '" <> show key <> "'") $+            fromLeft "" (language key) `shouldSatisfy` (message `isInfixOf`)+      )
test/MorphSpec.hs view
@@ -11,6 +11,7 @@ module MorphSpec (spec) where  import AST+import Builder (buildExpressionThrows) import Control.Exception (SomeException) import Control.Monad import Data.Aeson (FromJSON)@@ -25,8 +26,8 @@ import Fixtures (defaultReduceContext, fixtureLambdas, primitives, withLambdas, withLambdasOf) import GHC.Generics (Generic) import Lambdas (Lambdas, emptyLambdas, readLambdas)-import Matcher (substEmpty)-import Morph (ReduceContext (..), emptyState, execBuildTerm, insideUniverse, morph, morph')+import Matcher (MetaValue (MvExpression), substEmpty, substSingle)+import Morph (ReduceContext (..), emptyState, execBuildTerm, insideUniverse, morph, morph', sidePremise) import Parser (parseExpressionThrows) import Rewriter (Rewritten) import Rule (RuleContext (RuleContext), matchExpressionWithRule')@@ -189,16 +190,31 @@         )       ] -  -- 𝕄'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.+  -- A 'morph' premise names the universe 𝕄 runs in beside the term, as its+  -- rule's conclusion does, so it is reduced in that universe and not in the+  -- one the frame around it was handed: here the frame is in Φ, where Φ morphs+  -- to ⊥ through 'mg', while the premise names a world where Φ morphs to that+  -- world through 'universe' (#1512).+  describe "sidePremise" $+    it "morphs a premise in the universe it names, not in the one the frame is in" $ do+      world <- parseExpressionThrows "[[ x -> [[ ]] ]]"+      (subst, _) <-+        sidePremise+          ExRoot+          (defaultReduceContext ExRoot)+          (substSingle "e" (MvExpression world), emptyState)+          Yaml.Premise{result = "n1", operation = Yaml.OpMorph ExRoot (ExMeta "e")}+      buildExpressionThrows (ExMeta "n1") subst `shouldReturn` world++  -- Every 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 fires only on a term that is not a normal form: one the+  -- user handed 'morph' unnormalized (#1442), or a raw meta 𝑛, an AST node the+  -- matcher never binds to any concrete pattern, handed to 'morph'' directly.   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))+        `shouldThrow` (\e -> "Morphing expects a normal form" `isInfixOf` show (e :: SomeException))    -- 'execBuildTerm's "morph" case exposes 𝕄 to the matcher's condition path   -- (guards in 'when'/'having'), the way its "evaluate" case exposes 𝔼 (see
test/ReplacerSpec.hs view
@@ -201,7 +201,7 @@    describe "replace expression fast: ([Expression], [Expression]) => Expression" $     test-      (replaceExpressionFast (ReplaceCtx 3))+      replaceExpressionFast       [         ( "Q -> [[^ -> ?, @ -> ?, D> -> ?]] => [[ !B1, !t -> ?, !B2 ]] => [[ !B1, !t -> $, !B2 ]] => Q -> [[ ^ -> $, @ -> $, D> -> $ ]]"         , ExFormation [BiVoid AtRho, BiVoid AtPhi, BiVoid AtDelta]@@ -210,13 +210,27 @@         , ExFormation [BiTau AtRho ExXi, BiTau AtPhi ExXi, BiTau AtDelta ExXi]         )       ,-        ( "Q -> [[ ^ -> ? ]] => [[ !B1, !t -> ?, !B2 ]] => [[ !B1, !t -> [[ !t -> ? ]], !B2 ]] => Q -> [[ ^ -> [[ ^ -> [[ ^ -> [[ ^ -> ? ]] ]] ]] ]]"+        ( "Q -> [[ ^ -> ? ]] => [[ !B1, !t -> ?, !B2 ]] => [[ !B1, !t -> [[ !t -> ? ]], !B2 ]] => Q -> [[ ^ -> [[ ^ -> ? ]] ]] (a replacement is not searched again with the pair it came from)"         , ExFormation [BiVoid AtRho]         , [ExFormation [BiVoid AtRho]]         , [ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])]]-        , ExFormation [BiTau AtRho (ExFormation [BiTau AtRho (ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])])])]+        , ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])]         )       ,+        ( "Q -> [[a -> [[b -> [[c -> [[d -> ?]]]]]]]] => ([[d -> ?]], [[d -> Q]]) => Q -> [[a -> [[b -> [[c -> [[d -> Q]]]]]]]] (a match deep inside is replaced)"+        , ExFormation [BiTau (AtLabel "a") (ExFormation [BiTau (AtLabel "b") (ExFormation [BiTau (AtLabel "c") (ExFormation [BiVoid (AtLabel "d")])])])]+        , [ExFormation [BiVoid (AtLabel "d")]]+        , [ExFormation [BiTau (AtLabel "d") ExRoot]]+        , ExFormation [BiTau (AtLabel "a") (ExFormation [BiTau (AtLabel "b") (ExFormation [BiTau (AtLabel "c") (ExFormation [BiTau (AtLabel "d") ExRoot])])])]+        )+      ,+        ( "Q -> [[x -> [[a -> ?]], y -> [[a -> ?]]]] => ([[a -> ?]], [[a -> $]]) => Q -> [[x -> [[a -> $]], y -> [[a -> ?]]]] (one pair replaces in one formation)"+        , ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid (AtLabel "a")]), BiTau (AtLabel "y") (ExFormation [BiVoid (AtLabel "a")])]+        , [ExFormation [BiVoid (AtLabel "a")]]+        , [ExFormation [BiTau (AtLabel "a") ExXi]]+        , ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "a") ExXi]), BiTau (AtLabel "y") (ExFormation [BiVoid (AtLabel "a")])]+        )+      ,         ( "Q -> [[ ^ -> T ]](^ -> [[ ^ -> $]]).@ => [[ !B1, !t -> ?, !B2 ]] => [[ !B1, !t -> $, !B2 ]] => Q -> [[ ^ -> $ ]].@"         , ExDispatch (ExApplication (ExFormation [BiTau AtRho ExTermination]) (ArTau AtRho (ExFormation [BiTau AtRho ExXi]))) AtPhi         , [ExFormation [BiTau AtRho ExTermination], ExFormation [BiTau AtRho ExXi]]@@ -302,21 +316,9 @@         )       ] -  describe "replace expression fast with depth 0" $-    test-      (replaceExpressionFast (ReplaceCtx 0))-      [-        ( "Q -> [[a -> ?]] => ([[a -> ?]], [[a -> $]]) => Q -> [[a -> ?]]"-        , ExFormation [BiVoid (AtLabel "a")]-        , [ExFormation [BiVoid (AtLabel "a")]]-        , [ExFormation [BiTau (AtLabel "a") ExXi]]-        , ExFormation [BiVoid (AtLabel "a")]-        )-      ]--  describe "replace expression fast with depth 1" $+  describe "replace expression fast on edge cases" $     test-      (replaceExpressionFast (ReplaceCtx 1))+      replaceExpressionFast       [         ( "Q -> [[ ^ -> ? ]] => [[ ^ -> ? ]] => [[ ^ -> [[ ^ -> ? ]] ]] => Q -> [[ ^ -> [[ ^ -> ? ]] ]]"         , ExFormation [BiVoid AtRho]
test/RewriterSpec.hs view
@@ -1,6 +1,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -Wno-orphans #-}  -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com@@ -8,7 +9,7 @@  module RewriterSpec where -import AST (Expression (ExRoot))+import AST (Attribute (AtLabel), Binding (BiTau), Expression (ExDispatch, ExFormation, ExRoot, ExTermination)) import Control.Exception (SomeException) import Control.Monad (forM_, unless) import Data.Aeson@@ -68,31 +69,78 @@     forM_       [         ( "throws with --depth-sensitive once --max-cycles is reached"-        , []+        , "⟦ t ↦ ⊥.a ⟧"         , (5, 0, True)         , Left "--max-cycles=0"         )       ,         ( "stops silently without --depth-sensitive once --max-cycles is reached"-        , []+        , "⟦ t ↦ ⊥.a ⟧"         , (5, 0, False)         , Right snd         )       ,         ( "throws with --depth-sensitive once --max-depth is reached for a rule"-        , normalizationRules+        , "⟦ t ↦ ⊥.a ⟧"         , (0, 5, True)         , Left "--max-depth=0"         )       ,         ( "does not throw without --depth-sensitive once --max-depth is reached for a rule"-        , normalizationRules+        , "⟦ t ↦ ⊥.a ⟧"         , (0, 5, False)-        , Right (\(rewrittens, _) -> fst (NE.last rewrittens) == ExRoot)+        , Right (\(rewrittens, _) -> fst (NE.last rewrittens) == ExFormation [BiTau (AtLabel "t") (ExDispatch ExTermination (AtLabel "a"))])         )+      ,+        ( "throws with --depth-sensitive when a rule still applies after --max-depth steps"+        , "⟦ t ↦ ⊥.a.b ⟧"+        , (1, 5, True)+        , Left "--max-depth=1"+        )+      ,+        ( "does not throw with --depth-sensitive when a rule finishes in exactly --max-depth steps"+        , "⟦ t ↦ ⊥.a ⟧"+        , (1, 5, True)+        , Right (\(rewrittens, _) -> fst (NE.last rewrittens) == ExFormation [BiTau (AtLabel "t") ExTermination])+        )+      ,+        ( "does not throw with --depth-sensitive when rewriting finishes in exactly --max-cycles cycles"+        , "⟦ t ↦ ⊥.a ⟧"+        , (5, 1, True)+        , Right (\(rewrittens, _) -> fst (NE.last rewrittens) == ExFormation [BiTau (AtLabel "t") ExTermination])+        )       ]-      ( \(desc, rewriteRules, (maxDepth, maxCycles, depthSensitive), expected) -> it desc $ do-          let action = rewrite ExRoot rewriteRules (RewriteContext ExRoot maxDepth maxCycles depthSensitive Nothing buildTerm MtDisabled Nothing dontSaveStep)+      ( \(desc, input', (maxDepth, maxCycles, depthSensitive), expected) -> it desc $ do+          expr <- parseExpressionThrows input'+          let action = rewrite expr normalizationRules (RewriteContext ExRoot maxDepth maxCycles depthSensitive Nothing buildTerm MtDisabled Nothing dontSaveStep)+          case expected of+            Left fragment -> action `shouldThrow` (\exc -> fragment `isInfixOf` show (exc :: SomeException))+            Right predicate -> do+              result <- action+              result `shouldSatisfy` predicate+      )++  describe "--must once --max-cycles stops the run" $+    forM_+      [+        ( "throws when --must demands more cycles than --max-cycles allowed"+        , MtExact 3+        , Left "--must=3"+        )+      ,+        ( "throws when the lower bound of --must lies above --max-cycles"+        , MtRange (Just 2) Nothing+        , Left "--must=2.."+        )+      ,+        ( "does not throw when --max-cycles stops the run inside the range of --must"+        , MtRange (Just 1) (Just 4)+        , Right snd+        )+      ]+      ( \(desc, must', expected) -> it desc $ do+          expr <- parseExpressionThrows "⟦ t ↦ ⊥.a.b.c ⟧"+          let action = rewrite expr normalizationRules (RewriteContext ExRoot 1 1 False Nothing buildTerm must' Nothing dontSaveStep)           case expected of             Left fragment -> action `shouldThrow` (\exc -> fragment `isInfixOf` show (exc :: SomeException))             Right predicate -> do
test/RuleSpec.hs view
@@ -75,7 +75,8 @@       , ("returns true for formation with only delta binding", ExFormation [BiDelta (BtMany ["00", "01"])], True)       , ("returns true for formation with only void binding", ExFormation [BiVoid (AtLabel "x")], True)       , ("returns true for formation with only lambda binding", ExFormation [BiLambda (Function "Func")], True)-      , ("returns true for formation with delta void and lambda", ExFormation [BiDelta (BtOne "FF"), BiVoid (AtLabel "y"), BiLambda (Function "G")], True)+      , ("returns false for formation with delta void and lambda", ExFormation [BiDelta (BtOne "FF"), BiVoid (AtLabel "y"), BiLambda (Function "G")], False)+      , ("returns false for formation with delta and lambda, which dl reduces", ExFormation [BiDelta (BtMany ["01"]), BiLambda (Function "Fn")], False)       , ("returns true for a formation with a tau binding whose expression is already normal", ExFormation [BiTau (AtLabel "x") ExRoot], True)       , ("returns false for a formation with a tau binding matching a normalization rule", ExFormation [BiTau (AtLabel "x") (ExDispatch ExTermination (AtLabel "y"))], False)       ]
test/SugarSpec.hs view
@@ -323,6 +323,7 @@             ARROW             ( EX_SINGLE                 (PA_TAU (AT_LABEL "a") ARROW xiExpr)+                NO_SPACE                 (EX_FORMATION LSB EOL (TAB 2) (BI_PAIR (PA_TAU (AT_LABEL "a") ARROW xiExpr) (BDS_EMPTY (TAB 2)) (TAB 2)) EOL (TAB 1) RSB)             )         , PA_TAU@@ -628,7 +629,7 @@       [         ( "a formation left with one binding takes the one-binding sugar"         , EX_FORMATION LSB EOL (TAB 1) (BI_PAIR (PA_LAMBDA "Fn") (BDS_PAIR EOL (TAB 1) (PA_TAU (AT_RHO RHO) ARROW xiExpr) (BDS_EMPTY (TAB 1))) (TAB 1)) EOL (TAB 0) RSB-        , EX_SINGLE (PA_LAMBDA "Fn") (EX_FORMATION LSB EOL (TAB 1) (BI_PAIR (PA_LAMBDA "Fn") (BDS_EMPTY (TAB 1)) (TAB 1)) EOL (TAB 0) RSB)+        , EX_SINGLE (PA_LAMBDA "Fn") NO_SPACE (EX_FORMATION LSB EOL (TAB 1) (BI_PAIR (PA_LAMBDA "Fn") (BDS_EMPTY (TAB 1)) (TAB 1)) EOL (TAB 0) RSB)         )       ,         ( "a formation left with two bindings stays a formation"@@ -637,7 +638,7 @@         )       ,         ( "a one-binding sugar standing for a rho collapses to the empty formation"-        , EX_SINGLE (PA_TAU (AT_RHO RHO) ARROW xiExpr) (EX_FORMATION LSB EOL (TAB 1) (BI_PAIR (PA_TAU (AT_RHO RHO) ARROW xiExpr) (BDS_EMPTY (TAB 1)) (TAB 1)) EOL (TAB 0) RSB)+        , EX_SINGLE (PA_TAU (AT_RHO RHO) ARROW xiExpr) NO_SPACE (EX_FORMATION LSB EOL (TAB 1) (BI_PAIR (PA_TAU (AT_RHO RHO) ARROW xiExpr) (BDS_EMPTY (TAB 1)) (TAB 1)) EOL (TAB 0) RSB)         , EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB         )       ]
test/XMIRSpec.hs view
@@ -306,6 +306,8 @@       [ ("keeps λ function name and bound ρ", "[[ k -> [[ x -> ?, L> Lorg_eolang_number_plus, ^ -> [[ y -> ? ]] ]] ]]")       , ("keeps Δ data bound to a named attribute", "[[ k -> [[ a -> [[ D> 01-02 ]], ^ -> [[ D> 03-04 ]] ]] ]]")       , ("keeps Δ data in a dispatched formation", "[[ k -> [[ D> 01-02 ]].plus ]]")+      , ("keeps Δ data behind a sibling binding", "[[ top -> [[ a -> [[]], D> FF- ]] ]]")+      , ("keeps Δ data between sibling bindings", "[[ top -> [[ a -> [[]], D> 01-02, b -> [[]] ]] ]]")       , ("keeps a bare 'Q' bound to a named attribute", "[[ x -> Q ]]")       , ("keeps a formation bound to φ", "[[ k -> [[ @ -> [[ L> S8 ]] ]] ]]")       ]@@ -331,6 +333,13 @@             expr <- parseExpressionThrows "[[ x -> [[ y -> !e1 ]] ]]"             try (void (expressionToXMIR expr defaultXmirContext)) :: IO (Either SomeException ())         , ["XMIR does not support such expression"]+        )+      ,+        ( "refuses an application argument bound to ρ"+        , do+            expr <- parseExpressionThrows "[[ top -> Q.a(^ -> [[]]) ]]"+            try (void (expressionToXMIR expr defaultXmirContext)) :: IO (Either SomeException ())+        , ["XMIR does not support such expression", "ρ ↦"]         )       ,         ( "explains an unsupported binding"
test/YamlSpec.hs view
@@ -6,7 +6,7 @@  module YamlSpec where -import AST (Alpha, Attribute, Binding, Bytes, Expression (ExRoot))+import AST (Alpha, Attribute, Binding, Bytes, Expression (ExMeta, ExRoot)) import Control.Exception (Exception (displayException), SomeException) import Control.Monad import Data.Either (isLeft)@@ -157,7 +157,7 @@         ( "in a premise of a dataization rule"         , failsWith             "anonymous meta '!e' cannot be referenced in 'premises' of rule 'foo'"-            (decodeYaml' (inferring "universe: 𝑒2\nconclusion: 𝛿1\npremises:\n  - d-result: 𝛿1\n    dataize: '𝑒'") :: Either Yaml.ParseException DataizeRule)+            (decodeYaml' (inferring "universe: 𝑒2\nconclusion: 𝛿1\npremises:\n  - d-result: 𝛿1\n    dataize: ['𝑒', 𝑒2]") :: Either Yaml.ParseException DataizeRule)         )       ,         ( "in a premise of a contextualization rule"@@ -262,13 +262,24 @@    describe "rejects a malformed premise" $     forM_-      [ ("fails when neither 'n-result' nor 'd-result' is present", "morph: 𝑛")-      , ("fails when 'n-result' is not an expression meta", "n-result: Q\nmorph: 𝑛")-      , ("fails when 'd-result' is not a bytes meta", "d-result: '--'\ndataize: 𝑛")-      , ("fails when 'evaluate' does not take exactly two arguments", "n-result: 𝑛\nevaluate: [𝑛]")-      , ("fails when 'contextualize' does not take exactly two arguments", "n-result: 𝑛\ncontextualize: [𝑛]")+      [ ("fails when neither 'n-result' nor 'd-result' is present", "morph: [𝑛, 𝑒]")+      , ("fails when 'n-result' is not an expression meta", "n-result: Q\nmorph: [𝑛, 𝑒]")+      , ("fails when 'd-result' is not a bytes meta", "d-result: '--'\ndataize: [𝑛, 𝑒]")+      , ("fails when 'morph' does not take exactly two arguments", "n-result: 𝑛1\nmorph: [𝑛2]")+      , ("fails when 'evaluate' does not take exactly two arguments", "n-result: 𝑛1\nevaluate: [𝑛2]")+      , ("fails when 'contextualize' does not take exactly two arguments", "n-result: 𝑛1\ncontextualize: [𝑛2]")+      , ("fails when 'dataize' does not take exactly two arguments", "d-result: 𝛿1\ndataize: [𝑛1]")       ]       (\(desc, yaml) -> it desc ((decodeYaml' yaml :: Either Yaml.ParseException Premise) `shouldSatisfy` isLeft))++  -- 𝕄 and 𝔻 take the universe as their second argument, so a 'morph' or a+  -- 'dataize' premise names it beside the term, the way 'evaluate' does (#1512)+  describe "reads the universe a premise names" $+    forM_+      [ ("beside the term of 'morph'", "n-result: 𝑛1\nmorph: [𝑛2, 𝑒1]", Premise{result = T.pack "n1", operation = OpMorph (ExMeta (T.pack "n2")) (ExMeta (T.pack "e1"))})+      , ("beside the term of 'dataize'", "d-result: 𝛿1\ndataize: [𝑛1, 𝑒1]", Premise{result = T.pack "d1", operation = OpDataize (ExMeta (T.pack "n1")) (ExMeta (T.pack "e1"))})+      ]+      (\(desc, yaml, premise) -> it desc (either (const Nothing) Just (decodeYaml' yaml) `shouldBe` Just premise))    describe "rejects a numerable expression that is neither an object, a number nor an index meta" $     it "fails on a bare boolean" $