packages feed

phino 0.0.160 → 0.0.161

raw patch · 40 files changed

+1106/−428 lines, 40 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

+ Deps: EvUnripe :: Int -> (Expression, Expression) -> (Expression, Expression) -> Side -> Attribute -> Evaluation
+ Deps: [_copies] :: State -> [Expression]
+ Deps: lodged :: [Attribute] -> Expression -> Maybe Binding
+ Forks: Unripe :: Side -> Attribute -> Refusal
+ Lambdas: [_terminators] :: Lambda -> [Text]
+ Lambdas: thrown :: [Text] -> Expression -> Bool
+ Morph: argued :: Expression -> ReduceContext -> State -> Expression -> [Binding] -> Expression -> IO Expression
+ Morph: called :: Expression -> ReduceContext -> [Binding] -> Maybe Expression
+ Morph: carried :: State -> ReduceContext -> (State, ReduceContext)
+ Morph: coined :: ReduceContext -> IO Int
+ Morph: fired :: Expression -> ReduceContext -> Expression -> State -> Expression -> IO (Expression, State)
+ Morph: origin :: Expression -> ReduceContext -> [Binding] -> Maybe (Expression, [Binding])
+ Morph: severing :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, ReduceContext)
- Deps: EvJoined :: Int -> Either Text Expression -> Int -> (Int, Int) -> Maybe Int -> Evaluation
+ Deps: EvJoined :: Int -> Either Text Expression -> Int -> (Int, Int) -> Maybe Int -> Maybe Expression -> Evaluation
- Deps: EvLooped :: Int -> Judgment -> Acyclic -> Expression -> Expression -> Evaluation
+ Deps: EvLooped :: Int -> Judgment -> Acyclic -> Expression -> Expression -> Maybe (Int, Expression) -> Evaluation
- Deps: State :: Maybe Int -> Maybe Text -> State
+ Deps: State :: Maybe Int -> Maybe Text -> [Expression] -> State
- Lambdas: Lambda :: Text -> [(Meta, Expression)] -> [(Meta, Expression)] -> [(Meta, Expression)] -> [Line] -> Ending -> Lambda
+ Lambdas: Lambda :: Text -> [(Meta, Expression)] -> [(Meta, Expression)] -> [(Meta, Expression)] -> [Line] -> [Text] -> Ending -> Lambda

Files

README.md view
@@ -34,7 +34,7 @@  ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.158+cabal install --overwrite-policy=always phino-0.0.160 phino --version ``` @@ -59,7 +59,7 @@ for the runner and puts it on the `PATH`:  ```yaml-- uses: objectionary/phino@0.0.158+- uses: objectionary/phino@0.0.160   with:     version-file: phino-version.txt - run: phino --version@@ -158,9 +158,9 @@   rules under `rules` applied and nothing normalized afterwards.   The rules are written as in a [rule file](#rule-structure). * `cast` holds exactly two lines and binds their two metas as one pair.-  When one term is a bare symbol, `⟦ λ ⤍ 𝜎1 ⟧`, and the φ chain of the other-  ends in the only symbol it holds, the bare symbol becomes a copy of the other-  term with `𝜎1` at the end of that chain.+  When one term is a bare symbol, `⟦ λ ⤍ 𝜎1 ⟧`, and the other is a formation+  binding φ, the bare symbol becomes a copy of the other term with `𝜎1` in+  place of the term its φ chain ends in, whatever that term is. * `𝑛` is the term the entry answers with.   A bare `𝜎` in it stands for a fresh symbol, and no `𝛿` may appear in it. * `join` answers with one term made of two sides, in place of `𝑛`.@@ -170,6 +170,10 @@   meta.   It may hold `otherwise`, a λ name that joins two formations of different   shapes one attribute at a time, and the file must answer that name too.+* `terminators` lists λ names that only raise, as in `[L_throw]`.+  A term holding one of them, or an application of one, passes every line+  as it is, and `join` takes it for a side that raises, as it takes `⊥`.+  No entry of the file may answer such a name.  An entry holds either `𝑛` or `join`, never both. The lines of all blocks run in the order of the metas they read, not in the@@ -262,7 +266,9 @@ `--max-steps` runs out. The `--acyclic=<mode>` option makes the run notice a loop instead. When a reduction is about to enter a formation it is already inside, the run-stops there and leaves the term in place, as `--partial` does.+answers a copy of an object binding φ with a fresh symbol and goes on, and+stops at any other formation and leaves the term in place, as `--partial`+does. The mode says when two formations are the same:  * `proven` means equal up to a renaming of symbols;@@ -274,8 +280,8 @@ takes the answer of the first one. The `--max-loops=<n>` option lets a reduction enter such a formation `n` more times before it is cut.-`dataize` takes `--acyclic` too, and fails on a cut unless `--partial` is-given, since a cut term holds no data to print.+`dataize` takes `--acyclic` too, and fails on a term left in place unless+`--partial` is given, since such a term holds no data to print.  ## Protocol @@ -338,8 +344,8 @@ * `𝛿·1·1 := …` closes a `𝔻` block with the data it found, or with   `𝔻(𝜎1:λ)` where it came down to a symbol. * `morphed …` closes a `𝕄` block with the term it came to.-* `joined …`, `fabricated …` and `diverged …` are what a `join` made of its-  two sides, or why it could not join them.+* `joined …`, `fabricated …`, `diverged …` and `unripe …` are what a `join`+  made of its two sides, or why it could not join them. * `deferred …` and `symbolized …` are the symbols a `defer` or a `symbolize`   line minted. * `cast …` binds a meta to the copy a `cast` block made of a bare symbol, and@@ -347,7 +353,8 @@ * `unanswered …` is a λ name no entry answers. * `stuck …` closes a firing that got stuck, and `stall …` stands under one   that `--acyclic=plausible` answered with an earlier stall.-* `looped …` is where `--acyclic` cut a loop.+* `looped …` is where `--acyclic` cut a loop, and `looped 𝜎1 := …` names+  the call of the object it answered with that symbol. * `starved …`, `spent …` and `timeout …` are where `--max-steps`,   `--max-firings` and `--max-seconds` ran out. * `msec …`, `firings …` and `fps …` close the file, and the listing above@@ -682,119 +689,119 @@ === parse/phi ===   warmup:     3 iterations   batches:    10 x 1-  total:      1409532.338 μs-  avg:        140953.234 μs-  min:        123104.580 μs-  max:        169752.210 μs-  std dev:    19431.803 μs+  total:      2364731.566 μs+  avg:        236473.157 μs+  min:        211300.467 μs+  max:        292747.941 μs+  std dev:    27820.705 μs === parse/xmir ===   warmup:     3 iterations   batches:    10 x 1-  total:      6269190.661 μs-  avg:        626919.066 μs-  min:        570410.014 μs-  max:        708906.404 μs-  std dev:    53168.480 μs+  total:      9413355.678 μs+  avg:        941335.568 μs+  min:        877776.308 μs+  max:        1027338.259 μs+  std dev:    48859.029 μs === rewrite/normalize ===   warmup:     3 iterations   batches:    10 x 1-  total:      10.204 μs-  avg:        1.020 μs-  min:        0.842 μs-  max:        1.442 μs-  std dev:    0.179 μs+  total:      20.380 μs+  avg:        2.038 μs+  min:        1.683 μs+  max:        2.665 μs+  std dev:    0.306 μs === print/sweet/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      3999871.155 μs-  avg:        399987.116 μs-  min:        357813.221 μs-  max:        448393.174 μs-  std dev:    27725.936 μs+  total:      5757294.693 μs+  avg:        575729.469 μs+  min:        538059.300 μs+  max:        598828.490 μs+  std dev:    18128.062 μs === print/sweet/flat ===   warmup:     3 iterations   batches:    10 x 1-  total:      455172.450 μs-  avg:        45517.245 μs-  min:        40716.412 μs-  max:        55514.792 μs-  std dev:    6068.706 μs+  total:      677431.913 μs+  avg:        67743.191 μs+  min:        60183.418 μs+  max:        82804.920 μs+  std dev:    9547.482 μs === print/salty/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      11916902.966 μs-  avg:        1191690.297 μs-  min:        1124787.007 μs-  max:        1324046.797 μs-  std dev:    62960.748 μs+  total:      18322088.429 μs+  avg:        1832208.843 μs+  min:        1797579.128 μs+  max:        1855894.416 μs+  std dev:    17033.785 μs === morph/symbolic/demo/e1 ===   warmup:     3 iterations-  batches:    10 x 15-  total:      8063.096 μs-  avg:        53.754 μs-  min:        52.409 μs-  max:        56.184 μs-  std dev:    0.955 μs+  batches:    10 x 9+  total:      11891.278 μs+  avg:        132.125 μs+  min:        122.627 μs+  max:        167.660 μs+  std dev:    13.084 μs === morph/symbolic/demo/e2 ===   warmup:     3 iterations-  batches:    10 x 294-  total:      163954.216 μs-  avg:        55.767 μs-  min:        54.415 μs-  max:        56.517 μs-  std dev:    0.716 μs+  batches:    10 x 139+  total:      175033.685 μs+  avg:        125.924 μs+  min:        124.889 μs+  max:        126.740 μs+  std dev:    0.630 μs === morph/symbolic/demo/e3 ===   warmup:     3 iterations-  batches:    10 x 277-  total:      161047.794 μs-  avg:        58.140 μs-  min:        57.025 μs-  max:        58.757 μs-  std dev:    0.553 μs+  batches:    10 x 134+  total:      170791.687 μs+  avg:        127.456 μs+  min:        126.059 μs+  max:        128.848 μs+  std dev:    0.830 μs === morph/symbolic/demo/e4 ===   warmup:     3 iterations-  batches:    10 x 271-  total:      156357.626 μs-  avg:        57.697 μs-  min:        57.150 μs-  max:        58.248 μs-  std dev:    0.363 μs+  batches:    10 x 106+  total:      134964.020 μs+  avg:        127.325 μs+  min:        125.971 μs+  max:        128.683 μs+  std dev:    0.765 μs === morph/symbolic/demo/e5 ===   warmup:     3 iterations-  batches:    10 x 260-  total:      160590.902 μs-  avg:        61.766 μs-  min:        59.089 μs-  max:        79.533 μs-  std dev:    5.932 μs+  batches:    10 x 128+  total:      167197.696 μs+  avg:        130.623 μs+  min:        129.334 μs+  max:        132.171 μs+  std dev:    0.854 μs === morph/symbolic/native/e5 ===   warmup:     3 iterations   batches:    10 x 5-  total:      35947.906 μs-  avg:        718.958 μs-  min:        682.191 μs-  max:        764.860 μs-  std dev:    22.764 μs+  total:      65499.420 μs+  avg:        1309.988 μs+  min:        1146.675 μs+  max:        1920.625 μs+  std dev:    229.609 μs === morph/symbolic/accum/0 ===   warmup:     3 iterations-  batches:    10 x 142-  total:      68966.685 μs-  avg:        48.568 μs-  min:        47.428 μs-  max:        49.936 μs-  std dev:    0.778 μs+  batches:    10 x 94+  total:      100369.800 μs+  avg:        106.776 μs+  min:        105.512 μs+  max:        109.443 μs+  std dev:    1.070 μs === morph/symbolic/accum/400 ===   warmup:     3 iterations-  batches:    10 x 112-  total:      63083.756 μs-  avg:        56.325 μs-  min:        55.561 μs-  max:        57.281 μs-  std dev:    0.537 μs+  batches:    10 x 66+  total:      81652.018 μs+  avg:        123.715 μs+  min:        121.695 μs+  max:        126.110 μs+  std dev:    1.480 μs ```  The results were calculated in [this GHA job][benchmark-gha]-on 2026-10-26 at 12:05,+on 2026-11-03 at 13:03, on Linux with 4 CPUs.  <!-- benchmark_end -->@@ -837,4 +844,4 @@ [jna]: https://github.com/java-native-access/jna [jna-native]: https://github.com/java-native-access/jna/blob/master/src/com/sun/jna/Native.java [jeo]: https://github.com/objectionary/jeo-maven-plugin-[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/40319368788+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/41639970792
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.160+version: 0.0.161 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
src/CLI/Parsers.hs view
@@ -235,7 +235,7 @@ optPartial = switch (long "partial" <> help "Partial evaluation: compute what the known inputs decide and, instead of failing on a λ function that cannot fire (no entry of the --symbolic file answers it), leave it in place and print the residual 𝜑-program")  optAcyclic :: Parser (Maybe Acyclic)-optAcyclic = optional (option parseAcyclic (long "acyclic" <> metavar "MODE" <> help "Stop reducing as soon as the reduction enters a formation it is already inside (fires its λ function or dataizes its φ body again) instead of going round until --max-steps runs out, and leave the term in place the way --partial leaves a λ function that cannot fire; 'proven' takes it for the same one up to a renaming of symbols, 'plausible' also when it holds the earlier one under wrappers it gained, such as a growing accumulator"))+optAcyclic = optional (option parseAcyclic (long "acyclic" <> metavar "MODE" <> help "Stop reducing as soon as the reduction enters a formation it is already inside (fires its λ function or dataizes its φ body again) instead of going round until --max-steps runs out, answering a copy of an object binding φ with a fresh symbol and leaving any other term in place the way --partial leaves a λ function that cannot fire; 'proven' takes it for the same one up to a renaming of symbols, 'plausible' also when it holds the earlier one under wrappers it gained, such as a growing accumulator"))   where     parseAcyclic :: ReadM Acyclic     parseAcyclic = eitherReader $ \mode -> case filter ((== map toLower mode) . certainty) [minBound .. maxBound] of@@ -264,7 +264,8 @@               \\"defer\", the terms it keeps with every ρ applied to a dispatch dropped under \"stay\", the terms \               \it rewrites with rules spelled as in a rule file under \"rewrite\", the terms it keeps with \               \every datum they hold turned into a fresh symbol under \"symbolize\", the pair of terms whose \-              \bare symbol it casts into the shape of the other under \"cast\", and \+              \bare symbol it casts into the shape of the other under \"cast\", the λ functions that only \+              \raise, whose objects pass every line as they are and join as ⊥, under \"terminators\", and \               \answering with the term under \"𝑛\", or joining under \"join\" the two sides of a datum of \               \\"dataize\" into one term, with a fresh symbol where they differ"         )
src/CST.hs view
@@ -503,7 +503,7 @@   toCST (BiAny _) _ = error "An anonymous meta binding cannot be converted to PAIR"  instance ToCST Argument PAIR where-  toCST (ArTau attr exp) ctx = toCST (BiTau attr exp) ctx+  toCST (ArTau attr exp) ctx = PA_TAU (toCST attr ctx) ARROW (toCST exp ctx)   toCST (ArAlpha alpha exp) ctx = PA_ALPHA (toCST alpha ctx) ARROW (toCST exp ctx)  instance ToCST [Argument] BINDING where
src/Dataize.hs view
@@ -20,7 +20,7 @@ import Engine (Engine (..)) import qualified Inference as In import Locator (locatedExpression)-import Morph (Morphed, ReduceContext (..), ReduceException (..), ReductionFunc, deeper, entering, inferred, insideUniverse, leadsTo, onward, opening, parking, universed)+import Morph (Morphed, ReduceContext (..), ReduceException (..), ReductionFunc, carried, deeper, inferred, insideUniverse, leadsTo, onward, opening, parking, severing, universed) import Rewriter (Rewritten)  type Dataized = (Bytes, [Rewritten])@@ -54,10 +54,12 @@       pure (Residual residue, reverse (NE.toList seq), parked)  dataize' :: Dataizable -> Expression -> State -> ReduceContext -> IO (Dataized, State)-dataize' (expr, seq) univ state caller = do-  ctx <- opening Dataization =<< deeper =<< entering expr =<< parking seq state (universed univ caller{_judgment = Dataization})+dataize' (start, seq) univ held caller = do+  let (state, aware) = carried held caller+  (expr, entered) <- severing start univ state =<< parking seq state (universed univ aware{_judgment = Dataization})+  ctx <- opening Dataization =<< deeper entered   parking seq state $ case unknown expr of-    Just idx -> manufactured idx ctx+    Just idx -> manufactured idx state ctx     Nothing -> do       reached <- inferred expr univ state ctx ctx._engine._dataization       case reached of@@ -80,8 +82,8 @@     unknown :: Expression -> Maybe Int     unknown (ExFormation bds) = listToMaybe [idx | BiLambda (FnSymbol idx) <- bds]     unknown _ = Nothing-    manufactured :: Int -> ReduceContext -> IO (Dataized, State)-    manufactured idx ctx = do+    manufactured :: Int -> State -> ReduceContext -> IO (Dataized, State)+    manufactured idx state ctx = do       ctx._saveEval (EvManufactured ctx._nesting idx)       seq' <- leadsTo seq (Dataization, "symbol") (ExBytes datum) ctx       pure ((datum, NE.toList seq'), state{_manufactured = Just idx})
src/Deps.hs view
@@ -19,7 +19,7 @@ import Data.IORef (IORef, readIORef, writeIORef) import Data.List (intercalate, sortOn) import qualified Data.Map.Strict as Map-import Data.Maybe (fromMaybe, listToMaybe, mapMaybe)+import Data.Maybe (fromMaybe, listToMaybe, mapMaybe, maybeToList) import qualified Data.Text as T import Data.Time (ZonedTime, defaultTimeLocale, formatTime) import Files (overwrite)@@ -27,7 +27,7 @@ import GHC.Clock (getMonotonicTime) import Logger (logDebug, logInfo) import Matcher-import Printer (printAlpha, printAttribute, printFunction)+import Printer (printAlpha, printAttribute, printBinding, printFunction) import System.Directory (createDirectoryIfMissing) import System.FilePath import System.IO (Handle, hPutStrLn)@@ -46,6 +46,7 @@ data State = State   { _manufactured :: Maybe Int   , _stuck :: Maybe T.Text+  , _copies :: [Expression]   }  type BuildTermMethodS = [ExtraArgument] -> Subst -> IO (Term, State)@@ -106,7 +107,11 @@ refused refusal = case refusal of   Unnamed -> "the join names no otherwise"   Unformed side -> printf "the %s side is no formation" (handed side)+  Holding side AtLambda -> printf "the %s side is an atom" (handed side)+  Holding side AtDelta -> printf "the %s side is a datum" (handed side)   Holding side attr -> printf "the %s side has %s" (handed side) (printAttribute attr)+  Unripe Lefthand attr -> printf "%s is void on the left and attached on the right" (printAttribute attr)+  Unripe Righthand attr -> printf "%s is void on the right and attached on the left" (printAttribute attr)   where     handed :: Side -> String     handed Lefthand = "left"@@ -115,6 +120,11 @@ dotted :: [Attribute] -> String dotted = concatMap (('.' :) . printAttribute) +lodged :: [Attribute] -> Expression -> Maybe Binding+lodged [attr] (ExFormation bds) = listToMaybe [bd | bd <- bds, attributeFromBinding bd == Just attr]+lodged (attr : path) (ExFormation bds) = listToMaybe [inner | BiTau attr' inner <- bds, attr' == attr] >>= lodged path+lodged _ _ = Nothing+ data Evaluation   = EvRun Judgment T.Text   | EvFiring Int T.Text Judgment Expression@@ -123,7 +133,7 @@   | EvManufactured Int Int   | EvBoxed Int Expression   | EvUndressed Int Expression-  | EvLooped Int Judgment Acyclic Expression Expression+  | EvLooped Int Judgment Acyclic Expression Expression (Maybe (Int, Expression))   | EvStuck Int T.Text Judgment Expression   | EvStall Int T.Text   | EvStuckOn Int T.Text@@ -142,8 +152,9 @@   | EvBuilt Int Expression   | EvAnswer Int Expression   | EvMorphed Int Expression-  | EvJoined Int (Either T.Text Expression) Int (Int, Int) (Maybe Int)+  | EvJoined Int (Either T.Text Expression) Int (Int, Int) (Maybe Int) (Maybe Expression)   | EvDiverged Int (Expression, Expression) (Expression, Expression) [Attribute] Refusal+  | EvUnripe Int (Expression, Expression) (Expression, Expression) Side Attribute   | EvFabricated Int (Expression, Expression) (Expression, Expression) Expression   | EvTaken Int Expression   | EvWorld Expression@@ -161,7 +172,7 @@     record :: Evaluation -> Evaluation     record (EvFiring depth key judgment site) = EvFiring depth key judgment (moved site)     record (EvStarted depth judgment site) = EvStarted depth judgment (moved site)-    record (EvLooped depth judgment mode self site) = EvLooped depth judgment mode self (moved site)+    record (EvLooped depth judgment mode self site answered) = EvLooped depth judgment mode self (moved site) answered     record (EvStarved depth limit judgment site) = EvStarved depth limit judgment (moved site)     record (EvTimeout depth limit judgment site) = EvTimeout depth limit judgment (moved site)     record (EvSpent depth limit judgment site) = EvSpent depth limit judgment (moved site)@@ -186,7 +197,7 @@ tier (EvManufactured depth _) = depth tier (EvBoxed depth _) = depth tier (EvUndressed depth _) = depth-tier (EvLooped depth _ _ _ _) = depth+tier (EvLooped depth _ _ _ _ _) = depth tier (EvStuck depth _ _ _) = depth tier (EvStall depth _) = depth tier (EvStuckOn depth _) = depth@@ -205,8 +216,9 @@ tier (EvBuilt depth _) = depth tier (EvAnswer depth _) = depth tier (EvMorphed depth _) = depth-tier (EvJoined depth _ _ _ _) = depth+tier (EvJoined depth _ _ _ _ _) = depth tier (EvDiverged depth _ _ _ _) = depth+tier (EvUnripe depth _ _ _ _) = depth tier (EvFabricated depth _ _ _) = depth tier (EvTaken depth _) = depth tier EvWorld{} = maxBound@@ -371,10 +383,16 @@       pure (protocol', Just (indented at (printf "%s := %s" naming datum)))     written at (EvBoxed _ term) protocol = taking at "boxed" term protocol     written at (EvUndressed _ term) protocol = taking at "undressed" term protocol-    written at (EvLooped _ judgment mode self site) protocol = do+    written at (EvLooped _ judgment mode self site answered) protocol = do       form <- render self       remarks <- context protocol judgment site-      pure (protocol, Just (indented at (remarked (printf "looped %s" form) (remarks ++ [certainty mode]))))+      (line, notes) <- maybe (pure (printf "looped %s" form, [])) (severed form) answered+      pure (protocol, Just (indented at (remarked line (remarks ++ certainty mode : notes))))+      where+        severed :: String -> (Int, Expression) -> IO (String, [String])+        severed form (symbol, call) = do+          made <- printed (abbreviatedInside protocol._made call)+          pure (printf "looped %s := %s" (printFunction (FnSymbol symbol)) made, [printf "repeats %s" form])     written at (EvStuck _ key judgment self) protocol = do       form <- render self       pure (protocol, Just (indented at (printf "unanswered %s  # %s(%s)" (T.unpack key) (letter judgment) form)))@@ -454,14 +472,20 @@         (Nothing, Nothing) -> valued counted naming term         _ -> (,) counted <$> borrowed protocol term       pure (protocol'{_made = namedFormation term (alias (opener protocol) index) protocol'._made}, Just (indented at (printf "morphed %s := %s" naming value)))-    written at (EvJoined _ condition symbol (left, right) bottom) protocol = do+    written at (EvJoined _ condition symbol (left, right) bottom raised) protocol = do       on <- either (pure . labelled protocol) salted condition       termination <- render ExTermination-      pure (protocol, Just (indented at (remarked (printf "joined %s := %s ? %s : %s" (printFunction (FnSymbol symbol)) on (printFunction (FnSymbol left)) (printFunction (FnSymbol right))) [printf "where %s is %s" (printFunction (FnSymbol idx)) termination | Just idx <- [bottom], idx `elem` [left, right]])))+      raiser <- traverse salted raised+      pure (protocol, Just (indented at (remarked (printf "joined %s := %s ? %s : %s" (printFunction (FnSymbol symbol)) on (printFunction (FnSymbol left)) (printFunction (FnSymbol right))) [printf "where %s is %s%s" (printFunction (FnSymbol idx)) termination (maybe "" (printf " raised by %s") raiser :: String) | Just idx <- [bottom], idx `elem` [left, right]])))     written at (EvDiverged _ left right path refusal) protocol = do       one <- sided protocol left       two <- sided protocol right-      pure (protocol, Just (indented at (printf "diverged %s vs %s  # %s" one two (explained path refusal))))+      differed <- explained protocol path (snd left) (snd right)+      pure (protocol, Just (indented at (printf "diverged %s vs %s  # cannot join: %s; cannot fabricate: %s" one two differed (refused refusal))))+    written at (EvUnripe _ left right side attr) protocol = do+      one <- sided protocol left+      two <- sided protocol right+      pure (protocol, Just (indented at (printf "unripe %s vs %s  # %s" one two (refused (Unripe side attr)))))     written at (EvFabricated _ left right term) protocol = do       one <- sided protocol left       two <- sided protocol right@@ -503,9 +527,19 @@     borrowed protocol term = case namedLookup term protocol._named of       Nothing -> render term       Just naming -> pure (T.unpack naming)-    explained :: [Attribute] -> Refusal -> String-    explained [] refusal = refused refusal-    explained path refusal = printf "they differ at %s, and %s" (dotted path) (refused refusal)+    explained :: Protocol -> [Attribute] -> Expression -> Expression -> IO String+    explained protocol path one two = case reverse path of+      [] -> printf "the left side is %s and the right side is %s" <$> borrowed protocol one <*> borrowed protocol two+      attr : _ -> printf "at %s the left side %s and the right side %s" (dotted path) <$> had one <*> had two+        where+          had :: Expression -> IO String+          had side = maybe (pure (printf "has no %s" (printAttribute attr))) (fmap ("has " ++) . bound) (lodged path side)+          bound :: Binding -> IO String+          bound (BiTau attr' term) = printf "%s ↦ %s" (printAttribute attr') <$> borrowed protocol term+          bound (BiVoid attr') = pure (printf "%s ↦ ∅" (printAttribute attr'))+          bound (BiDelta bytes) = printf "Δ ⤍ %s" <$> render (ExBytes bytes)+          bound (BiLambda func) = pure (printf "λ ⤍ %s" (printFunction func))+          bound bd = pure (printBinding bd)     sided :: Protocol -> (Expression, Expression) -> IO String     sided _ (_, term@(ExFormation [BiLambda (FnSymbol _)])) = render term     sided protocol (side@(ExMeta _), _) = spoken protocol side@@ -635,11 +669,17 @@         pending :: [(Int, Judgment, Expression)]         pending = dropWhile (\(level, _, _) -> level > at) nesting._pending         (kept, closers) = closed at nesting._closing-    elements at (EvLooped depth judgment mode self site) nesting =+    elements at (EvLooped depth judgment mode self site Nothing) nesting =       placed at nesting $ do         locator <- located depth site         origin <- sole depth self         pure (enclosed "looped" (printf "<looped by=\"%s\" match=\"%s\" at=\"%s\"" (opened judgment) (certainty mode) (escapeXML locator)) origin)+    elements at (EvLooped depth judgment mode self site (Just (symbol, call))) nesting =+      placed at nesting $ do+        locator <- located depth site+        origin <- leaf depth self+        (object, given) <- called depth call+        pure (printf "<looped symbol=\"%s\" by=\"%s\" match=\"%s\" at=\"%s\" of=\"%s\" object=\"%s\">%s</looped>" (sigma symbol) (opened judgment) (certainty mode) (escapeXML locator) (escapeXML origin) (escapeXML object) given)     elements at (EvStuck depth key judgment self) nesting =       placed at nesting (printf "<unanswered λ=\"%s\" by=\"%s\">%s</unanswered>" (quoted key) (opened judgment) . escapeXMLText <$> leaf depth self)     elements at (EvStall _ key) nesting =@@ -713,15 +753,22 @@         pure (printf "<built meta=\"%s\">%s</built>" (escapeXML naming) (escapeXMLText body))     elements at (EvAnswer depth term) nesting = placed at nesting (concluded "answered" depth term)     elements at (EvMorphed depth term) nesting = placed at nesting (concluded "morphed" depth term)-    elements at (EvJoined _ condition symbol (left, right) bottom) nesting =+    elements at (EvJoined depth condition symbol (left, right) bottom raised) nesting =       placed at nesting $ do         on <- either (pure . labelled nesting) (lift . traced) condition-        pure (printf "<joined symbol=\"%s\" on=\"%s\" left=\"%s\" right=\"%s\"%s/>" (sigma symbol) (escapeXML on) (sigma left) (sigma right) (concat [printf " terminator=\"%s\"" (sigma idx) :: String | Just idx <- [bottom], idx `elem` [left, right]]))+        raiser <- traverse (leaf depth) [term | Just idx <- [bottom], idx `elem` [left, right], Just term <- [raised]]+        pure (printf "<joined symbol=\"%s\" on=\"%s\" left=\"%s\" right=\"%s\"%s%s/>" (sigma symbol) (escapeXML on) (sigma left) (sigma right) (concat [printf " terminator=\"%s\"" (sigma idx) :: String | Just idx <- [bottom], idx `elem` [left, right]]) (concat [printf " raised=\"%s\"" (escapeXML name) :: String | name <- raiser]))     elements at (EvDiverged depth left right path refusal) nesting =       placed at nesting $ do         one <- sided depth nesting left         two <- sided depth nesting right-        pure (printf "<diverged left=\"%s\" right=\"%s\"%s reason=\"%s\"/>" (escapeXML one) (escapeXML two) (if null path then "" else printf " at=\"%s\"" (escapeXML (dotted path)) :: String) (escapeXML (refused refusal)))+        places <- mapM (uncurry (lodging depth path)) [("left", snd left), ("right", snd right)]+        pure (printf "<diverged left=\"%s\" right=\"%s\"%s reason=\"%s\">%s</diverged>" (escapeXML one) (escapeXML two) (if null path then "" else printf " at=\"%s\"" (escapeXML (dotted path)) :: String) (escapeXML (refused refusal)) (concat places))+    elements at (EvUnripe depth left right _ attr) nesting =+      placed at nesting $ do+        one <- sided depth nesting left+        two <- sided depth nesting right+        pure (printf "<unripe left=\"%s\" right=\"%s\" at=\"%s\"/>" (escapeXML one) (escapeXML two) (escapeXML (printAttribute attr)))     elements at (EvFabricated depth left right term) nesting =       placed at nesting $ do         one <- sided depth nesting left@@ -844,9 +891,19 @@     anonymous :: Int -> [Binding] -> Naming (String -> String)     anonymous depth bds = do       parts <- mapM (part depth) bds-      let marks = concat (lefts parts)-          inner = concat (rights parts)-      pure (\naming -> if null inner then printf "<formed meta=\"%s\"%s/>" naming marks else printf "<formed meta=\"%s\"%s>%s</formed>" naming marks inner)+      pure (\naming -> gathered "formed" (printf "formed meta=\"%s\"" naming) parts)+    lodging :: Int -> [Attribute] -> String -> Expression -> Naming String+    lodging depth [] tag side = (\body -> printf "<%s>%s</%s>" tag (escapeXMLText body) tag) <$> leaf depth side+    lodging depth path tag side = gathered tag tag <$> mapM (part depth) (maybeToList (lodged path side))+    gathered :: String -> String -> [Either String String] -> String+    gathered tag opening parts+      | null inner = printf "<%s%s/>" opening marks+      | otherwise = printf "<%s%s>%s</%s>" opening marks inner tag+      where+        marks :: String+        marks = concat (lefts parts)+        inner :: String+        inner = concat (rights parts)     part :: Int -> Binding -> Naming (Either String String)     part depth (BiTau attr value) = Right <$> (titled depth value >>= lift . attributed (printAttribute attr))     part _ (BiVoid attr) = pure (Right (printf "<void attr=\"%s\"/>" (escapeXML (printAttribute attr))))
src/Evaluate.hs view
@@ -12,17 +12,17 @@ import Builder (buildExpressionThrows) import Control.Exception (throwIO, try) import Control.Monad (foldM, unless)-import Data.IORef (atomicModifyIORef', readIORef, writeIORef)+import Data.IORef (readIORef, writeIORef) import Data.List (partition) import Data.List.NonEmpty (NonEmpty (..)) import Data.Maybe (fromMaybe, listToMaybe) import qualified Data.Text as T import Deps (Evaluation (..), Judgment (Evaluation, Morphing), State (..), dontSaveEval, dontSaveStep, resited) import Engine (Engine (..))-import Forks (Refusal (Unnamed), forked, joined)-import Lambdas (Ending (..), Lambda (..), Line (..), Meta (..), cast, emptyLambdas, matched, minted, rewritten, stayed, symbolized)+import Forks (Refusal (Unnamed, Unripe), forked, joined)+import Lambdas (Ending (..), Lambda (..), Line (..), Meta (..), cast, emptyLambdas, matched, minted, rewritten, stayed, symbolized, thrown) import Matcher (MetaValue (..), Subst, combine, substEmpty, substSingle, substSlot)-import Morph (Answer (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), awaited, boxed, charged, counted, deeper, ended, enter, expired, isLambda, lambda, morphing, normalized, opening, recalled, remember, remembered, retained, settled, starved, unparked)+import Morph (Answer (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), argued, awaited, boxed, called, charged, coined, counted, deeper, ended, expired, fired, isLambda, lambda, morphing, normalized, opening, origin, recalled, remember, remembered, retained, settled, starved, unparked) import Printer (printFunction) import Rule (RuleContext (RuleContext)) import Text.Printf (printf)@@ -87,7 +87,7 @@           throwIO (escaped failure)     worked :: ReduceContext -> Lambda -> Firing -> Subst -> State -> IO (Answer, State)     worked ctx entry firing@(Firing _ operands _) bound state' = do-      (lined, state'') <- foldM (line ctx entry._ending) (bound, state') entry._lines+      (lined, state'') <- foldM (passing ctx entry) (bound, state') entry._lines       (answer, state''') <- concluded ctx entry operands lined state''       remember caller._memo firing answer       pure (answer, state''')@@ -97,6 +97,25 @@     keyed :: Expression -> IO Expression     keyed side@(ExMeta _) = pure side     keyed side = operand side+    passing :: ReduceContext -> Lambda -> (Subst, State) -> Line -> IO (Subst, State)+    passing ctx entry held@(bound, state') item = case sourced item of+      Just (meta, source) -> do+        term <- buildExpressionThrows (ExMeta source._name) bound+        if thrown entry._terminators term+          then do+            ctx._saveEval (EvBound ctx._nesting (ExMeta meta._name) term)+            (,state') <$> bind meta (MvExpression term) bound+          else line ctx entry._ending held item+      Nothing -> line ctx entry._ending held item+    sourced :: Line -> Maybe (Meta, Meta)+    sourced (Morphed meta source) = Just (meta, source)+    sourced (Undressed meta source) = Just (meta, source)+    sourced (Evaluated meta source) = Just (meta, source)+    sourced (Deferred meta source) = Just (meta, source)+    sourced (Stayed meta source) = Just (meta, source)+    sourced (Rewritten meta source _) = Just (meta, source)+    sourced (Symbolized meta source) = Just (meta, source)+    sourced _ = Nothing     line :: ReduceContext -> Ending -> (Subst, State) -> Line -> IO (Subst, State)     line ctx _ held (Dataized meta source) = lowered ctx held meta source     line ctx _ held (Morphed meta source) = reduced ctx held meta source@@ -135,7 +154,7 @@       pure (ended answer, state)     told (Looped term) = do       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+      mapM_ (\mode -> caller._saveEval (EvLooped (caller._nesting + 1) caller._judgment mode term caller._site Nothing)) caller._acyclic       throwIO (Looping term)     told (Stalled name _) = do       caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site)@@ -151,7 +170,8 @@       pure (bound', state'')     brought :: ReduceContext -> Subst -> State -> Meta -> Expression -> Expression -> IO (Either Int Bytes, Subst, State)     brought ctx bound state' meta origin term = do-      (value, state'') <- unparked (ctx._reduce univ ctx{_site = origin} term state'{_manufactured = Nothing, _stuck = Nothing})+      (value, came) <- unparked (ctx._reduce univ ctx{_site = origin} term state'{_manufactured = Nothing, _stuck = Nothing, _copies = []})+      let state'' = came{_copies = state'._copies}       case value of         Nothing -> throwIO (Stuck (fromMaybe func state''._stuck))         Just bytes -> do@@ -239,55 +259,23 @@       pure (bound', state'')     kindled :: ReduceContext -> Ending -> Expression -> State -> Expression -> IO (Expression, State)     kindled _ _ _ state' term@(ExFormation [BiLambda (FnSymbol _)]) = pure (term, state')+    kindled ctx _ _ state' term@(ExFormation bds)+      | owned ctx bds = pure (term, state')     kindled ctx _ site state' term@(ExFormation _) = fire ctx site state' term     kindled _ Joining{} _ state' term = pure (term, state')     kindled ctx _ site state' term = fire ctx site state' term+    owned :: ReduceContext -> [Binding] -> Bool+    owned ctx bds = maybe False (\(_, voids) -> any (`notElem` (AtRho : [attr | BiVoid attr <- voids])) [attr | BiTau attr _ <- bds, not (cactus attr)]) (origin univ ctx bds)+    cactus :: Attribute -> Bool+    cactus (AtLabel label) = "🌵" `T.isSuffixOf` label+    cactus _ = False     fire :: ReduceContext -> Expression -> State -> Expression -> IO (Expression, State)     fire _ _ state' ExTermination = pure (ExTermination, state')-    fire ctx site state' term@(ExFormation _) = do-      entered <- deeper =<< enter term ctx{_judgment = Evaluation, _site = site}-      evaluation entered state' term univ+    fire ctx site state' term@(ExFormation _) = fired univ ctx site state' term     fire _ _ _ _ = throwIO (Stuck func)-    figured :: ReduceContext -> State -> Expression -> Expression -> IO Expression-    figured ctx state' site placed = unparked $ do-      (normal, morphed) <- settled placed univ state' =<< opening Morphing ctx{_site = site}-      fst <$> fire ctx site morphed normal     named :: Attribute -> Binding -> Bool     named attr (BiTau attr' _) = attr == attr'     named _ _ = False-    called :: [Binding] -> Maybe Expression-    called known = uncurry (applied known) <$> origin known-    applied :: [Binding] -> Expression -> [Binding] -> Expression-    applied known path declared = foldl ExApplication path [ArTau attr value | BiTau attr value <- known, attr /= AtRho, BiVoid attr `elem` declared]-    origin :: [Binding] -> Maybe (Expression, [Binding])-    origin known = do-      parent <- case filter ((== Just AtRho) . attributeFromBinding) known of-        [] -> Just ExRoot-        [BiTau AtRho (ExFormation outer)] -> fst <$> origin outer-        [BiTau AtRho path] -> Just (erased path)-        _ -> Nothing-      ExFormation siblings <- located parent (fromMaybe univ caller._universe)-      chosen [(ExDispatch parent attr, declared) | BiTau attr (ExFormation declared) <- siblings, attr /= AtRho, fits declared]-      where-        fits :: [Binding] -> Bool-        fits declared = all (`elem` map attributeFromBinding declared) [attributeFromBinding bd | bd <- known, attributeFromBinding bd /= Just AtRho]-        chosen :: [(Expression, [Binding])] -> Maybe (Expression, [Binding])-        chosen [] = Nothing-        chosen candidates = case [candidate | candidate <- candidates, agreed candidate == maximum (map agreed candidates)] of-          [one] -> Just one-          _ -> Nothing-        agreed :: (Expression, [Binding]) -> (Int, Int)-        agreed (_, declared) = (length [attr | BiTau attr _ <- known, BiVoid attr `elem` declared], length (filter (`elem` declared) known))-    located :: Expression -> Expression -> Maybe Expression-    located ExRoot whole = Just whole-    located (ExDispatch path attr) whole = case located path whole of-      Just (ExFormation siblings) -> listToMaybe [body | BiTau attr' body <- siblings, attr' == attr]-      _ -> Nothing-    located _ _ = Nothing-    erased :: Expression -> Expression-    erased (ExApplication target _) = erased target-    erased (ExDispatch target attr) = ExDispatch (erased target) attr-    erased other = other     deferred :: ReduceContext -> State -> Meta -> Meta -> Subst -> IO Subst     deferred ctx state' meta source bound = do       term <- buildExpressionThrows (ExMeta source._name) bound@@ -332,30 +320,15 @@         reading = ctx{_symbolic = emptyLambdas, _memo = Nothing, _tally = Nothing, _acyclic = Nothing, _saveStep = dontSaveStep, _saveEval = dontSaveEval}         postponed :: [Binding] -> IO Expression         postponed known = do-          call <- argued ctx state' site known-          fresh <- coined+          call <- traverse (argued univ ctx state' site known) (called univ ctx known)+          fresh <- coined caller           ctx._saveEval (EvDeferred ctx._nesting fresh Morphing (ExFormation known) call (ExDispatch site AtPhi))           pure (ExFormation [BiLambda (FnSymbol fresh)])     postponing _ _ _ _ = pure Nothing-    argued :: ReduceContext -> State -> Expression -> [Binding] -> IO (Maybe Expression)-    argued ctx state' site bds = traverse go (called bds)-      where-        go :: Expression -> IO Expression-        go (ExApplication target (ArTau attr body)) = do-          target' <- go target-          ExApplication target' . ArTau attr <$> reckoned attr body-        go call = pure call-        reckoned :: Attribute -> Expression -> IO Expression-        reckoned _ body@(ExFormation [BiLambda (FnSymbol _)]) = pure body-        reckoned attr body = do-          placed <- ctx._engine._contextualize body (ExFormation (filter (not . named attr) bds))-          figured ctx state' (ExDispatch site attr) placed-    coined :: IO Int-    coined = atomicModifyIORef' caller._minted (\count -> (succ count, succ count))     concluded :: ReduceContext -> Lambda -> [Either Int Bytes] -> Subst -> State -> IO (Answer, State)     concluded ctx entry operands bound state' = case entry._ending of       Answering template -> answered ctx template operands bound state'-      Joining on left right fallback -> merged ctx bound (zip (map (_name . fst) entry._dataized) operands) on left right fallback state'+      Joining on left right fallback -> merged ctx entry._terminators bound (zip (map (_name . fst) entry._dataized) operands) on left right fallback state'     answered :: ReduceContext -> Expression -> [Either Int Bytes] -> Subst -> State -> IO (Answer, State)     answered ctx template operands bound state' = do       (fresh, spent) <- minted template <$> readIORef ctx._minted@@ -367,22 +340,32 @@       (normal, state'') <- settled built univ state' =<< opening Morphing ctx{_saveEval = ctx._saveEval . resited ctx._site built}       ctx._saveEval (EvAnswer ctx._nesting normal)       pure (Answer built normal, state'')-    merged :: ReduceContext -> Subst -> [(T.Text, Either Int Bytes)] -> Either Meta Expression -> Expression -> Expression -> Maybe Function -> State -> IO (Answer, State)-    merged ctx bound operands on left right fallback state' = do+    merged :: ReduceContext -> [T.Text] -> Subst -> [(T.Text, Either Int Bytes)] -> Either Meta Expression -> Expression -> Expression -> Maybe Function -> State -> IO (Answer, State)+    merged ctx terminators bound operands on left right fallback state' = do       condition <- weighed operands on       (one, state'') <- reached ctx bound left state'       (two, state''') <- reached ctx bound right state''       spent <- readIORef ctx._minted-      case joined one two spent of+      let raised = case filter (thrown terminators) [one, two] of+            [side] -> Just side+            _ -> Nothing+          stopped :: Expression -> Expression+          stopped side+            | Just side == raised = ExTermination+            | otherwise = side+      case joined (stopped one) (stopped two) spent of         Right (term, made, bottom, spent') -> do           writeIORef ctx._minted spent'-          mapM_ (\(fresh, pair) -> ctx._saveEval (EvJoined ctx._nesting (either (Left . _spelling) Right on) fresh pair bottom)) made+          mapM_ (\(fresh, pair) -> ctx._saveEval (EvJoined ctx._nesting (either (Left . _spelling) Right on) fresh pair bottom raised)) made           ctx._saveEval (EvTaken ctx._nesting term)           pure (Joined term, state''')         Left path -> case maybe (Left Unnamed) (\name -> forked name condition one two) fallback of           Right term -> do             ctx._saveEval (EvFabricated ctx._nesting (left, one) (right, two) term)             pure (Joined term, state''')+          Left (Unripe side attr) -> do+            ctx._saveEval (EvUnripe ctx._nesting (left, one) (right, two) side attr)+            throwIO (Diverged func)           Left refusal -> do             ctx._saveEval (EvDiverged ctx._nesting (left, one) (right, two) path refusal)             throwIO (Diverged func)
src/Forks.hs view
@@ -25,6 +25,7 @@   = Unnamed   | Unformed Side   | Holding Side Attribute+  | Unripe Side Attribute   deriving (Eq, Show)  joined :: Expression -> Expression -> Int -> Either [Attribute] (Expression, [(Int, (Int, Int))], Maybe Int, Int)@@ -98,7 +99,10 @@       Nothing -> (succ spent', (succ spent', bottom, Map.insert pair (succ spent') names, (succ spent', pair) : made))  forked :: Function -> Either Int Bytes -> Expression -> Expression -> Either Refusal Expression-forked func condition left right = fabricated <$> formed Lefthand left <*> formed Righthand right+forked func condition left right = do+  one <- formed Lefthand left+  two <- formed Righthand right+  maybe (Right (fabricated one two)) Left (listToMaybe (unripe Lefthand one two ++ unripe Righthand two one))   where     formed :: Side -> Expression -> Either Refusal [Binding]     formed side (ExFormation bds) = maybe (Right bds) (Left . Holding side) (listToMaybe [attr | Just attr <- map attributeFromBinding bds, attr == AtDelta || attr == AtLambda])@@ -109,11 +113,21 @@         voids :: [Attribute]         voids = nub (vacant one ++ vacant two)         branch :: Attribute -> Binding-        branch attr = BiTau attr (ExFormation ([BiVoid AtRho, BiLambda func] ++ map BiVoid (inner attr) ++ [BiTau (AtLabel "on🌵") (ExFormation [either (BiLambda . FnSymbol) BiDelta condition]), ask "left🌵" one attr, ask "right🌵" two attr]))+        branch attr = maybe (forking attr) (BiTau attr) (aliased attr)+        aliased :: Attribute -> Maybe Expression+        aliased attr = case (bound one attr, bound two attr) of+          (Just term@(ExDispatch ExXi name), Just other) | term == other && name `elem` attributes one ++ attributes two -> Just term+          _ -> Nothing+        bound :: [Binding] -> Attribute -> Maybe Expression+        bound bds attr = listToMaybe [term | BiTau label term <- bds, label == attr]+        forking :: Attribute -> Binding+        forking attr = BiTau attr (ExFormation ([BiVoid AtRho, BiLambda func] ++ map BiVoid (inner attr) ++ [BiTau (AtLabel "on🌵") (ExFormation [either (BiLambda . FnSymbol) BiDelta condition]), ask "left🌵" one attr, ask "right🌵" two attr]))         inner :: Attribute -> [Attribute]         inner attr = nub (concat (mapMaybe (`held` attr) [one, two]))         ask :: Text -> [Binding] -> Attribute -> Binding         ask name bds attr = BiTau (AtLabel name) (applied (ExDispatch (ExDispatch (ExDispatch ExXi AtRho) (AtLabel name)) attr) (fromMaybe (inner attr) (held bds attr)))+    unripe :: Side -> [Binding] -> [Binding] -> [Refusal]+    unripe side bds others = [Unripe side attr | attr <- vacant bds, attr `elem` [label | BiTau label _ <- others]]     vacant :: [Binding] -> [Attribute]     vacant bds = [attr | BiVoid attr <- bds, own attr]     attributes :: [Binding] -> [Attribute]
src/Lambdas.hs view
@@ -23,6 +23,7 @@   , stayed   , symbolized   , taken+  , thrown   ) where @@ -84,6 +85,7 @@   , _morphed :: [(Meta, Expression)]   , _undressed :: [(Meta, Expression)]   , _lines :: [Line]+  , _terminators :: [Text]   , _ending :: Ending   } @@ -108,6 +110,7 @@     lambda <-       Lambda key dataized morphed undressed         <$> (written (T.unpack key) entry >>= ordered (T.unpack key) (map (_name . fst) (morphed ++ undressed)) . ((weighing ++ reading ++ peeling) ++))+        <*> entry .:? "terminators" .!= []         <*> pure ending     once (T.unpack key) lambda     mapM_ (metaless (T.unpack key) "dataize" "a path from '$' or a meta alone") lambda._dataized@@ -122,7 +125,7 @@         name : _ -> fail (printf "The key '%s' of λ function '%s' is none of the keys an entry reads: %s" (T.unpack name) key (T.unpack (T.intercalate ", " known)))         where           known :: [Text]-          known = ["λ", "dataize", "morph", "undress", "evaluate", "defer", "stay", "rewrite", "symbolize", "cast", "join", "𝑛"]+          known = ["λ", "dataize", "morph", "undress", "evaluate", "defer", "stay", "rewrite", "symbolize", "cast", "join", "terminators", "𝑛"]       concluded :: String -> [(Meta, Expression)] -> Object -> Yaml.Parser Ending       concluded key dataized entry = do         answer <- entry .:? "𝑛"@@ -365,6 +368,7 @@   mapM_ (unique entries) entries   registered <- mapM keyed entries   overlaps path registered+  mapM_ (answering registered) entries   logDebug (printf "Loaded %d λ function(s) from '%s'" (length entries) path)   pure (Lambdas registered)   where@@ -381,6 +385,10 @@     unreadable :: Text -> (a, String) -> IO b     unreadable key (_, failure) =       throwIO (BrokenLambdas path (printf "the key '%s' is not a regular expression: %s" (T.unpack key) failure))+    answering :: [(Regex, Lambda)] -> Lambda -> IO ()+    answering registered entry = case [(name, other) | name <- entry._terminators, Just other <- [matched (Lambdas registered) name]] of+      [] -> pure ()+      (name, other) : _ -> throwIO (BrokenLambdas path (printf "the terminator '%s' of the key '%s' is answered by the key '%s'" (T.unpack name) (T.unpack entry._key) (T.unpack other._key)))     overlaps :: FilePath -> [(Regex, Lambda)] -> IO ()     overlaps _ [_] = pure ()     overlaps file registered = mapM (spoken . snd) registered >>= check@@ -414,6 +422,11 @@     fresh :: [Slot]     fresh = [slot | slot@(Slot kind _) <- slots answer, kind == "S"] +thrown :: [Text] -> Expression -> Bool+thrown names (ExApplication expr _) = thrown names expr+thrown names (ExFormation bds) = or [name `elem` names | BiLambda (Function name) <- bds]+thrown _ _ = False+ taken :: Expression -> Int taken program = maximum (0 : symbols program) @@ -442,17 +455,17 @@  cast :: Expression -> Expression -> Maybe Expression cast bare@(ExFormation [BiLambda (FnSymbol _)]) shape-  | length (symbols shape) == 1 = goExpr shape+  | decorating shape = Just (goExpr shape)   where-    goExpr :: Expression -> Maybe Expression-    goExpr (ExFormation bds) = case [body | BiTau AtPhi body <- bds] of-      [ExFormation [BiLambda (FnSymbol _)]] -> Just (ExFormation (map (placed bare) bds))-      [body] -> (\made -> ExFormation (map (placed made) bds)) <$> goExpr body-      _ -> Nothing-    goExpr _ = Nothing-    placed :: Expression -> Binding -> Binding-    placed made (BiTau AtPhi _) = BiTau AtPhi made-    placed _ bd = bd+    goExpr :: Expression -> Expression+    goExpr body@(ExFormation bds) | decorating body = ExFormation (map placed bds)+    goExpr _ = bare+    placed :: Binding -> Binding+    placed (BiTau AtPhi body) = BiTau AtPhi (goExpr body)+    placed bd = bd+    decorating :: Expression -> Bool+    decorating (ExFormation bds) = AtPhi `elem` [attr | BiTau attr _ <- bds]+    decorating _ = False cast _ _ = Nothing  rewritten :: RuleContext -> [Y.Rule] -> Expression -> IO Expression
src/Morph.hs view
@@ -4,25 +4,26 @@ {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TupleSections #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} {-# OPTIONS_GHC -Wno-unused-record-wildcards #-}  -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Morph (Answer (..), Deadline (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), admitting, awaited, boxed, charged, counted, deeper, emptyState, ended, enter, entering, execBuildTerm, expired, inferred, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, onward, opening, parking, recalled, refused, remember, remembered, retained, settled, starved, tallied, timed, universed, unparked) where+module Morph (Answer (..), Deadline (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), admitting, argued, awaited, boxed, called, carried, charged, coined, counted, deeper, emptyState, ended, enter, entering, execBuildTerm, expired, fired, inferred, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, onward, opening, origin, parking, recalled, refused, remember, remembered, retained, settled, severing, starved, tallied, timed, universed, unparked) where  import AST import Builder (buildExpressionThrows, nameIn) import Control.Applicative ((<|>)) import Control.Exception (Exception, catch, evaluate, throwIO, try) import Control.Monad (when)-import Data.IORef (IORef, modifyIORef', newIORef, readIORef, writeIORef)+import Data.IORef (IORef, atomicModifyIORef', modifyIORef', newIORef, readIORef, writeIORef) import Data.List (find, partition) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE import qualified Data.Map.Strict as Map-import Data.Maybe (isJust, listToMaybe)+import Data.Maybe (fromMaybe, isJust, listToMaybe) import qualified Data.Text as T import Deps (Acyclic (..), BuildTermFunc, BuildTermMethod, Evaluation (..), Judgment (..), SaveEvalFunc, SaveStepFunc, State (..), Term (..), dontSaveStep) import Engine (Engine (..))@@ -47,7 +48,7 @@ type EvaluationFunc = ReduceContext -> State -> Expression -> Expression -> IO (Expression, State)  emptyState :: State-emptyState = State Nothing Nothing+emptyState = State Nothing Nothing []  data Steps = Steps   { _limit :: Int@@ -274,23 +275,121 @@  refused :: Expression -> ReduceContext -> (Acyclic, Expression) -> IO a refused form ctx (mode, before) = do-  ctx._saveEval (EvLooped ctx._nesting ctx._judgment mode before ctx._site)+  ctx._saveEval (EvLooped ctx._nesting ctx._judgment mode before ctx._site Nothing)   throwIO (Looping form) +severing :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, ReduceContext)+severing term univ state ctx = case entrance ctx._judgment term of+  Just form -> either (,ctx) (term,) <$> sever form univ state ctx+  Nothing -> pure (term, ctx)++sever :: Expression -> Expression -> State -> ReduceContext -> IO (Either Expression ReduceContext)+sever form univ state ctx = admitted form ctx >>= either cut (pure . Right)+  where+    cut :: (Acyclic, Expression) -> IO (Either Expression ReduceContext)+    cut loop = case form of+      ExFormation bds+        | boxed bds || ctx._judgment == Dataization+        , Just call <- called univ ctx bds ->+            Left <$> severed univ ctx state form bds call loop+      _ -> refused form ctx loop++severed :: Expression -> ReduceContext -> State -> Expression -> [Binding] -> Expression -> (Acyclic, Expression) -> IO Expression+severed univ ctx state form bds call (mode, before) = do+  reckoned <- argued univ ctx state form bds call+  fresh <- coined ctx+  ctx._saveEval (EvLooped ctx._nesting ctx._judgment mode before ctx._site (Just (fresh, reckoned)))+  pure (ExFormation [BiLambda (FnSymbol fresh)])++coined :: ReduceContext -> IO Int+coined ctx = atomicModifyIORef' ctx._minted (\count -> (succ count, succ count))++fired :: Expression -> ReduceContext -> Expression -> State -> Expression -> IO (Expression, State)+fired univ ctx site state form = sever form univ state ctx{_judgment = Evaluation, _site = site} >>= either (pure . (,state)) kindled+  where+    kindled :: ReduceContext -> IO (Expression, State)+    kindled entered = do+      deep <- deeper entered+      deep._evaluate deep state form univ++called :: Expression -> ReduceContext -> [Binding] -> Maybe Expression+called univ ctx known = uncurry applied <$> origin univ ctx known+  where+    applied :: Expression -> [Binding] -> Expression+    applied path declared = foldl ExApplication path [ArTau attr value | BiTau attr value <- known, attr /= AtRho, BiVoid attr `elem` declared]++origin :: Expression -> ReduceContext -> [Binding] -> Maybe (Expression, [Binding])+origin univ ctx bds = do+  parent <- case filter ((== Just AtRho) . attributeFromBinding) bds of+    [] -> Just ExRoot+    [BiTau AtRho (ExFormation outer)] -> fst <$> origin univ ctx outer+    [BiTau AtRho path] -> Just (erased path)+    _ -> Nothing+  ExFormation siblings <- located parent (fromMaybe univ ctx._universe)+  chosen [(ExDispatch parent attr, declared) | BiTau attr (ExFormation declared) <- siblings, attr /= AtRho, fits declared]+  where+    fits :: [Binding] -> Bool+    fits declared = all (`elem` map attributeFromBinding declared) [attributeFromBinding bd | bd <- bds, attributeFromBinding bd /= Just AtRho]+    chosen :: [(Expression, [Binding])] -> Maybe (Expression, [Binding])+    chosen [] = Nothing+    chosen candidates = case [candidate | candidate <- candidates, agreed candidate == maximum (map agreed candidates)] of+      [one] -> Just one+      _ -> Nothing+    agreed :: (Expression, [Binding]) -> (Int, Int)+    agreed (_, declared) = (length [attr | BiTau attr _ <- bds, BiVoid attr `elem` declared], length (filter (`elem` declared) bds))+    located :: Expression -> Expression -> Maybe Expression+    located ExRoot whole = Just whole+    located (ExDispatch path attr) whole = case located path whole of+      Just (ExFormation siblings) -> listToMaybe [body | BiTau attr' body <- siblings, attr' == attr]+      _ -> Nothing+    located _ _ = Nothing+    erased :: Expression -> Expression+    erased (ExApplication target _) = erased target+    erased (ExDispatch target attr) = ExDispatch (erased target) attr+    erased other = other++argued :: Expression -> ReduceContext -> State -> Expression -> [Binding] -> Expression -> IO Expression+argued univ ctx state site bds = go+  where+    go :: Expression -> IO Expression+    go (ExApplication target (ArTau attr body)) = do+      target' <- go target+      ExApplication target' . ArTau attr <$> reckoned attr body+    go call = pure call+    reckoned :: Attribute -> Expression -> IO Expression+    reckoned _ body@(ExFormation [BiLambda (FnSymbol _)]) = pure body+    reckoned attr body = do+      placed <- ctx._engine._contextualize body (ExFormation (filter (not . named attr) bds))+      figured (ExDispatch site attr) placed+    named :: Attribute -> Binding -> Bool+    named attr (BiTau attr' _) = attr == attr'+    named _ _ = False+    figured :: Expression -> Expression -> IO Expression+    figured place placed = unparked $ do+      (normal, morphed) <- settled placed univ state =<< opening Morphing ctx{_site = place}+      case normal of+        ExFormation _ -> fst <$> fired univ ctx place morphed normal+        _ -> pure normal+ admitted :: Expression -> ReduceContext -> IO (Either (Acyclic, Expression) ReduceContext) admitted form ctx = maybe (pure (Right ctx)) remembered ctx._acyclic   where     remembered :: Acyclic -> IO (Either (Acyclic, Expression) ReduceContext)-    remembered mode =-      maybe (Right ctx{_entered = seenInsert (digest mode form) form ctx._entered}) (\before -> Left (mode, before))-        <$> awaited ctx (evaluate (listToMaybe (drop ctx._maxLoops (filter (repeated mode form) (Map.findWithDefault [] (digest mode form) ctx._entered)))))-    digest :: Acyclic -> Expression -> Int-    digest Proven = hashShape-    digest Plausible = hashSkeleton-    repeated :: Acyclic -> Expression -> Expression -> Bool-    repeated Proven form before = alike form before-    repeated Plausible form before = within before form+    remembered mode = maybe (Right ctx{_entered = seenInsert (digest mode form) form ctx._entered}) (\before -> Left (mode, before)) . listToMaybe . drop ctx._maxLoops <$> repeats mode form ctx +repeats :: Acyclic -> Expression -> ReduceContext -> IO [Expression]+repeats mode form ctx = awaited ctx (evaluate (length hits `seq` hits))+  where+    hits :: [Expression]+    hits = take (succ ctx._maxLoops) (filter (repeated mode) (Map.findWithDefault [] (digest mode form) ctx._entered))+    repeated :: Acyclic -> Expression -> Bool+    repeated Proven before = alike form before+    repeated Plausible before = within before form++digest :: Acyclic -> Expression -> Int+digest Proven = hashShape+digest Plausible = hashSkeleton+ entrance :: Judgment -> Expression -> Maybe Expression entrance Dataization term@(ExFormation bds)   | boxed bds || isJust (lambda bds) = Just term@@ -457,8 +556,25 @@   (universe, aiming) <- insideUniverse expr univ ctx   normal <- locatedExpression aiming._locator universe   unparked $ do-    ((morphed, _), state') <- morph' (normal, (universe, Nothing) :| []) universe state =<< opening Morphing =<< universed universe aiming-    pure (morphed, state')+    opened <- opening Morphing =<< universed universe aiming+    ((morphed, _), state') <- morph' (normal, (universe, Nothing) :| []) universe state{_copies = []} opened+    recurring morphed universe state'{_copies = state._copies ++ state'._copies} opened+  where+    recurring :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)+    recurring term@(ExFormation bds) world state' opened+      | Just mode <- opened._acyclic+      , boxed bds+      , Just call <- called world opened bds = do+          hits <- repeats mode term opened+          case drop opened._maxLoops hits of+            before : _ -> (,state') <$> severed world opened state' term bds call (mode, before)+            []+              | null hits -> pure (term, state')+              | otherwise -> pure (term, state'{_copies = state'._copies ++ [term]})+    recurring term _ state' _ = pure (term, state')++carried :: State -> ReduceContext -> (State, ReduceContext)+carried state ctx = (state{_copies = []}, maybe ctx (\mode -> ctx{_entered = foldr (\form -> seenInsert (digest mode form) form) ctx._entered state._copies}) ctx._acyclic)  execBuildTerm :: Expression -> ReduceContext -> BuildTermFunc execBuildTerm _ ctx "evaluate" = evaluated ctx
src/Parser.hs view
@@ -427,8 +427,8 @@ argument :: Parser Argument argument =   choice-    [ ArAlpha <$> try alpha <*> tauValue-    , ArTau <$> attribute <*> tauValue+    [ ArAlpha <$> try alpha <* arrow <*> expression+    , ArTau <$> attribute <* arrow <*> expression     ]     <?> "argument"
+ test-resources/evaluate-packs/answers-an-operand-that-dataizes-in-circles-with-a-symbol.yaml view
@@ -0,0 +1,47 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# A loop met while an operand is being brought down to data, with no frame of 𝕄+# ever handed the same term twice: the body of 'cyc' dispatches 'cyc' again, so+# every round 𝕄 stops at a formation of its own and only 𝔻 — 'box'+# contextualizing that body and 'norm' morphing what comes out — comes back to+# the term it started from. Before #1290 the guard of '--acyclic' was 𝕄's alone+# and this went round until the step budget ran out; now 𝔻 asks it too. The box+# step answers the copy of 'cyc' it would enter again with a fresh symbol+# (#2226), so the operand comes down to the datum of that symbol and the firing+# answers.+symbolic: |+  - λ: L_outer+    dataize:+      𝛿1: ξ.arg+    𝑛: ⟦ bar ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧+location: 'Q.x'+acyclic: proven+steps: 250+input: >+  ⟦ cyc ↦ ⟦ x ↦ ∅, φ ↦ Φ.cyc( ξ.x ) ⟧,+    x ↦ ⟦ arg ↦ Φ.cyc( ⟦⟧ ), λ ⤍ L_outer ⟧.bar ⟧+result: '𝜎2:λ'+protocol: |+  𝕄(Φ.x):+    𝔼(L_outer):+      𝔻(ξ.arg):+        𝕄(ξ.arg):+          𝑛·1·1 := Φ.cyc( x ↦ ⟦⟧ )+          𝑛·1·2 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧+          morphed 𝑛·1·3 := 𝑛·1·2+        boxed 𝑛·1·4 := 𝑛·1·3.φ+        𝕄(𝑛·1·4):+          𝑛·1·5 := Φ.cyc( x ↦ ⟦⟧ )+          𝑛·1·6 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧+          morphed 𝑛·1·7 := 𝑛·1·6+        𝕄(𝑛·1·7.x):+          morphed 𝑛·1·8 := ⟦⟧+        looped 𝜎1 := Φ.cyc( x ↦ 𝑛·1·8 )  # 𝔻(𝑛·1·4), proven, repeats 𝑛·1·7+        𝛿·1·1 := 𝔻(𝜎1:λ)+      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.arg)+      𝑛·1·9 := 𝜎2:λ:bar  # 𝑛+      𝕄(𝑛·1·9):+        morphed 𝑛·1·10 := 𝜎2:λ:bar+      𝑛·1·11 := 𝑛·1·10  # 𝕄(𝑛·1·9)+    morphed 𝑛·0·1 := 𝜎2:λ
+ test-resources/evaluate-packs/answers-the-same-dataization-loop-under-partial.yaml view
@@ -0,0 +1,44 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# The program of 'answers-an-operand-that-dataizes-in-circles-with-a-symbol',+# run with '--partial' as well. The box step of 𝔻 answers the copy it would+# enter again with a fresh symbol (#2226), so nothing is left to park and the+# answer is the same, which is what "--acyclic needs no --partial" means for a+# loop 𝔻 catches (#1290).+symbolic: |+  - λ: L_outer+    dataize:+      𝛿1: ξ.arg+    𝑛: ⟦ bar ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧+location: 'Q.x'+acyclic: proven+partial: true+steps: 250+input: >+  ⟦ cyc ↦ ⟦ x ↦ ∅, φ ↦ Φ.cyc( ξ.x ) ⟧,+    x ↦ ⟦ arg ↦ Φ.cyc( ⟦⟧ ), λ ⤍ L_outer ⟧.bar ⟧+result: '𝜎2:λ'+protocol: |+  𝕄(Φ.x):+    𝔼(L_outer):+      𝔻(ξ.arg):+        𝕄(ξ.arg):+          𝑛·1·1 := Φ.cyc( x ↦ ⟦⟧ )+          𝑛·1·2 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧+          morphed 𝑛·1·3 := 𝑛·1·2+        boxed 𝑛·1·4 := 𝑛·1·3.φ+        𝕄(𝑛·1·4):+          𝑛·1·5 := Φ.cyc( x ↦ ⟦⟧ )+          𝑛·1·6 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧+          morphed 𝑛·1·7 := 𝑛·1·6+        𝕄(𝑛·1·7.x):+          morphed 𝑛·1·8 := ⟦⟧+        looped 𝜎1 := Φ.cyc( x ↦ 𝑛·1·8 )  # 𝔻(𝑛·1·4), proven, repeats 𝑛·1·7+        𝛿·1·1 := 𝔻(𝜎1:λ)+      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.arg)+      𝑛·1·9 := 𝜎2:λ:bar  # 𝑛+      𝕄(𝑛·1·9):+        morphed 𝑛·1·10 := 𝜎2:λ:bar+      𝑛·1·11 := 𝑛·1·10  # 𝕄(𝑛·1·9)+    morphed 𝑛·0·1 := 𝜎2:λ
test-resources/evaluate-packs/cuts-a-recursion-running-through-evaluate-lines.yaml view
@@ -12,19 +12,19 @@ symbolic: |   - λ: L_loop     morph:-      𝑛1: $.next+      𝑛1: $.next🌵     evaluate:       𝑛2: 𝑛1     𝑛: 𝑛2 location: 'Q.app' acyclic: proven firings: 5-input: '⟦ loop ↦ ⟦ next ↦ Φ.loop, λ ⤍ L_loop ⟧, app ↦ Φ.loop.φ ⟧'-result: '⟦ next ↦ Φ.loop, λ ⤍ L_loop ⟧.φ'+input: '⟦ loop ↦ ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧, app ↦ Φ.loop.φ ⟧'+result: '⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧.φ' protocol: |   𝕄(Φ.app):     𝔼(L_loop):-      𝕄(ξ.next):-        morphed 𝑛·1·1 := ⟦ next ↦ Φ.loop, λ ⤍ L_loop ⟧-      𝑛1·1 := ⟦ next ↦ Φ.loop, λ ⤍ L_loop ⟧  # 𝕄(ξ.next)-      looped ⟦ next ↦ Φ.loop, λ ⤍ L_loop ⟧  # 𝔼(𝑛1), proven+      𝕄(ξ.next🌵):+        morphed 𝑛·1·1 := ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧+      𝑛1·1 := ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧  # 𝕄(ξ.next🌵)+      looped ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧  # 𝔼(𝑛1), proven
test-resources/evaluate-packs/diverges-on-a-side-holding-a-datum-though-it-may-fabricate.yaml view
@@ -28,4 +28,4 @@         morphed 𝑛·1·1 := 01-:Δ       𝕄(ξ.b):         morphed 𝑛·1·2 := Φ.zu:φ-      diverged 01-:Δ vs 𝑛·1·2  # they differ at .Δ, and the left side has Δ+      diverged 01-:Δ vs 𝑛·1·2  # cannot join: at .Δ the left side has Δ ⤍ 01- and the right side has no Δ; cannot fabricate: the left side is a datum
test-resources/evaluate-packs/diverges-on-a-side-holding-a-symbol-though-it-may-fabricate.yaml view
@@ -30,4 +30,4 @@         morphed 𝑛·1·1 := 𝜎2:λ       𝕄(ξ.b):         morphed 𝑛·1·2 := ⟦ φ ↦ Φ.zu, ke ↦ Φ.ty ⟧-      diverged 𝜎2:λ vs 𝑛·1·2  # they differ at .λ, and the left side has λ+      diverged 𝜎2:λ vs 𝑛·1·2  # cannot join: at .λ the left side has λ ⤍ 𝜎2 and the right side has no λ; cannot fabricate: the left side is an atom
test-resources/evaluate-packs/diverges-on-two-sides-of-metas-that-differ.yaml view
@@ -32,4 +32,4 @@       𝕄(ξ.b):         morphed 𝑛·1·2 := 02-:Δ:φ       𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)-      diverged 𝑛1·1 vs 𝑛2·1  # they differ at .φ.Δ, and the join names no otherwise+      diverged 𝑛1·1 vs 𝑛2·1  # cannot join: at .φ.Δ the left side has Δ ⤍ 01- and the right side has Δ ⤍ 02-; cannot fabricate: the join names no otherwise
test-resources/evaluate-packs/diverges-on-two-sides-that-do-not-join.yaml view
@@ -101,4 +101,4 @@         𝑛·2·12 := 𝑛·2·10.plus( x ↦ 4.0 )         𝑛·2·13 := ⟦ x ↦ 4.0, λ ⤍ L_number_plus ⟧         morphed 𝑛·2·14 := 𝑛·2·13-      diverged 𝑛·2·8 vs 𝑛·2·13  # they differ at .ρ, and the join names no otherwise+      diverged 𝑛·2·8 vs 𝑛·2·13  # cannot join: at .ρ the left side has ρ ↦ 𝑛·2·5 and the right side has ρ ↦ 𝑛·2·10; cannot fabricate: the join names no otherwise
+ test-resources/evaluate-packs/fires-a-formation-written-in-place-after-a-stay-line.yaml view
@@ -0,0 +1,47 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# The side is a formation written in place, not an object of the world, with+# its void 'v' filled by an argument. The 'stay' line drops the '( ρ ↦ Φ )'+# of that argument, and the 'evaluate' line still fires the formation, since+# what it does depends on the term it gets and the world alone, and not on+# what happened to the term before (#2269, #2270).+symbolic: |+  - λ: L_probe+    morph:+      𝑛1: $.side🌵+    stay:+      𝑛2: 𝑛1+    evaluate:+      𝑛3: 𝑛2+    𝑛: 𝑛3+  - λ: L_box+    𝑛: ⟦ λ ⤍ 𝜎 ⟧+location: 'Q.y'+partial: true+input: >+  ⟦ k ↦ 𝜎1:λ,+    x ↦ ⟦ λ ⤍ L_probe, side🌵 ↦ ⟦ f ↦ ⟦ v ↦ ∅, λ ⤍ L_box ⟧ ⟧.f( v ↦ Φ.k( ρ ↦ Φ ) ) ⟧,+    y ↦ Φ.x.φ ⟧+result: '𝜎2:λ.φ'+protocol: |+  𝕄(Φ.y):+    𝑛·0·1 := ⟦ v ↦ ∅, λ ⤍ L_box ⟧( v ↦ Φ.k )+    𝑛·0·2 := ⟦ v ↦ Φ.k, λ ⤍ L_box ⟧+    𝔼(L_probe):+      𝕄(ξ.side🌵):+        morphed 𝑛·1·1 := 𝑛·0·2+      𝑛1·1 := 𝑛·0·2  # 𝕄(ξ.side🌵)+      𝑛2·1 := ⟦ v ↦ Φ.k, λ ⤍ L_box ⟧  # stay(𝑛1)+      𝔼(L_box):  # 𝔼(𝑛2)+        𝑛·2·1 := 𝜎2:λ  # 𝑛+        𝕄(𝑛·2·1):+          morphed 𝑛·2·2 := 𝜎2:λ+        𝑛·2·3 := 𝑛·2·2  # 𝕄(𝑛·2·1)+      𝑛3·1 := 𝑛·2·3  # 𝔼(𝑛2)+      𝑛·1·2 := 𝑛3·1  # 𝑛+      𝕄(𝑛·1·2):+        morphed 𝑛·1·3 := 𝑛3·1+      𝑛·1·4 := 𝑛3·1  # 𝕄(𝑛·1·2)+    unanswered 𝜎2  # 𝕄(𝜎2:λ)
+ test-resources/evaluate-packs/fires-a-formation-written-in-place-with-its-voids-filled.yaml view
@@ -0,0 +1,55 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# The left side of the fork is a formation written in place, not an object of+# the world, with its void 'v' filled by an argument. The 'v' it binds after+# the copy is the void it showed before, not an attribute of its own, so the+# 'evaluate' line fires it as it fires a copy of an object of the world, and+# the join joins the two symbols (#2267).+symbolic: |+  - λ: L_fork+    dataize:+      𝛿1: $.on🌵+    morph:+      𝑛1: $.left🌵+      𝑛2: $.right🌵+    evaluate:+      𝑛3: 𝑛1+      𝑛4: 𝑛2+    join:+      'on': 𝛿1+      left: 𝑛3+      right: 𝑛4+      otherwise: L_fork+  - λ: L_box+    𝑛: ⟦ λ ⤍ 𝜎 ⟧+location: 'Q.y'+partial: true+input: >+  ⟦ x ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ⟦ v ↦ ∅, λ ⤍ L_box ⟧( v ↦ 𝜎2:λ ), right🌵 ↦ 𝜎3:λ ⟧,+    y ↦ Φ.x.φ ⟧+result: '𝜎5:λ.φ'+protocol: |+  𝕄(Φ.y):+    𝑛·0·1 := ⟦ v ↦ ∅, λ ⤍ L_box ⟧( v ↦ 𝜎2:λ )+    𝑛·0·2 := ⟦ v ↦ 𝜎2:λ, λ ⤍ L_box ⟧+    𝔼(L_fork):+      𝔻(ξ.on🌵):+        𝛿·1·1 := 𝔻(𝜎1:λ)+      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.on🌵)+      𝕄(ξ.left🌵):+        morphed 𝑛·1·1 := 𝑛·0·2+      𝑛1·1 := 𝑛·0·2  # 𝕄(ξ.left🌵)+      𝕄(ξ.right🌵):+        morphed 𝑛·1·2 := 𝜎3:λ+      𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.right🌵)+      𝔼(L_box):  # 𝔼(𝑛1)+        𝑛·2·1 := 𝜎4:λ  # 𝑛+        𝕄(𝑛·2·1):+          morphed 𝑛·2·2 := 𝜎4:λ+        𝑛·2·3 := 𝑛·2·2  # 𝕄(𝑛·2·1)+      𝑛3·1 := 𝑛·2·3  # 𝔼(𝑛1)+      joined 𝜎5 := 𝛿1·1 ? 𝜎4 : 𝜎3+      𝑛·1·3 := 𝜎5:λ+    unanswered 𝜎5  # 𝕄(𝜎5:λ)
test-resources/evaluate-packs/hands-a-side-of-a-fabricated-formation-only-the-voids-its-attribute-leaves.yaml view
@@ -9,7 +9,8 @@ # leaves alone (#2031), since 'miss' turns an application to an attribute a # formation lacks into ⊥. The program hands 'x' over, so the right side gets # 'w' bound to ⊥, the two sides differ in shape and are fabricated again, and-# the copy under 'k' finds 'x' on both of them.+# 'k' stays the alias of 'x' both sides bind it to (#2260), so the copy under+# 'x' finds it on both of them. symbolic: |   - λ: L_fork     dataize:@@ -52,7 +53,7 @@       𝑛·2·7 := ⟦ x ↦ 𝜎2:λ:φ, w ↦ ⊥, k ↦ x ⟧       𝕄(ξ.right🌵):         morphed 𝑛·2·8 := 𝑛·2·7-      fabricated 𝑛·2·9 := 𝑛·2·3 and 𝑛·2·8  # ⟦ left🌵 ↦ 𝑛·2·3, right🌵 ↦ 𝑛·2·8, x ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.x, right🌵 ↦ ρ.right🌵.x ⟧, k ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.k, right🌵 ↦ ρ.right🌵.k ⟧, w ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.w, right🌵 ↦ ρ.right🌵.w ⟧ ⟧+      fabricated 𝑛·2·9 := 𝑛·2·3 and 𝑛·2·8  # ⟦ left🌵 ↦ 𝑛·2·3, right🌵 ↦ 𝑛·2·8, x ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.x, right🌵 ↦ ρ.right🌵.x ⟧, k ↦ x, w ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.w, right🌵 ↦ ρ.right🌵.w ⟧ ⟧     𝔼(L_join):       𝕄(ξ.left🌵):         morphed 𝑛·3·1 := 𝜎2:λ:φ
+ test-resources/evaluate-packs/joins-a-bare-symbol-a-cast-brought-into-a-decorator-of-a-fork.yaml view
@@ -0,0 +1,76 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# The left side holds 'k' beside a φ that is another fork, and the right side+# is the bare symbol 𝜎3. The φ chain of the left side ends in no symbol, so+# the 'cast' block used to cast nothing, and the join diverged (#2223). Now+# the cast copies the left side down its φ chain to the first φ binding no φ+# of its own, the fork, and puts 𝜎3 in its place. The two sides then differ+# in what their φ holds, so the firing fabricates a formation. The program+# asks that formation for its φ, a copy of 'L_fork' with the inner fork on the+# left and 𝜎3 on the right. That copy fires the inner fork, which answers 𝜎7,+# the join of 𝜎5 and 𝜎6, casts 𝜎3 into the shape of that answer, and answers+# 𝜎8, the join of 𝜎7 and 𝜎3.+symbolic: |+  - λ: L_fork+    dataize:+      𝛿1: $.on🌵+    morph:+      𝑛1: $.left🌵+      𝑛2: $.right🌵+    evaluate:+      𝑛3: 𝑛1+      𝑛4: 𝑛2+    cast:+      𝑛5: 𝑛3+      𝑛6: 𝑛4+    join:+      on: 𝛿1+      left: 𝑛5+      right: 𝑛6+      otherwise: L_fork+location: 'Q.e1'+input: '⟦ e1 ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎1 ⟧, left🌵 ↦ ⟦ k ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎5 ⟧ ⟧, right🌵 ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎6 ⟧ ⟧ ⟧ ⟧, right🌵 ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧.φ.φ ⟧'+result: '𝜎8:λ'+protocol: |+  𝕄(Φ.e1):+    𝔼(L_fork):+      𝔻(ξ.on🌵):+        𝛿·1·1 := 𝔻(𝜎1:λ)+      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.on🌵)+      𝕄(ξ.left🌵):+        morphed 𝑛·1·1 := ⟦ k ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎4:λ, left🌵 ↦ 𝜎5:λ:φ, right🌵 ↦ 𝜎6:λ:φ ⟧ ⟧+      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.left🌵)+      𝕄(ξ.right🌵):+        morphed 𝑛·1·2 := 𝜎3:λ+      𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.right🌵)+      cast 𝑛6·1 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎3:λ ⟧  # 𝑛2·1 up to 𝑛·1·1+      fabricated 𝑛·1·3 := 𝑛·1·1 and 𝑛6·1  # ⟦ left🌵 ↦ 𝑛·1·1, right🌵 ↦ ⟦ k ↦ ⟦⟧, φ ↦ 𝜎3:λ ⟧, k ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.k, right🌵 ↦ ρ.right🌵.k ⟧, φ ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.φ, right🌵 ↦ ρ.right🌵.φ ⟧ ⟧+    𝔼(L_fork):+      𝔻(ξ.on🌵):+        𝛿·2·1 := 𝔻(𝜎1:λ)+      𝛿1·2 := 𝛿·2·1  # 𝔻(ξ.on🌵)+      𝕄(ξ.left🌵):+        morphed 𝑛·2·1 := ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎4:λ, left🌵 ↦ 𝜎5:λ:φ, right🌵 ↦ 𝜎6:λ:φ ⟧+      𝑛1·2 := ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎4:λ, left🌵 ↦ 𝜎5:λ:φ, right🌵 ↦ 𝜎6:λ:φ ⟧  # 𝕄(ξ.left🌵)+      𝕄(ξ.right🌵):+        morphed 𝑛·2·2 := 𝑛2·1+      𝑛2·2 := 𝑛2·1  # 𝕄(ξ.right🌵)+      𝔼(L_fork):  # 𝔼(𝑛1)+        𝔻(ξ.on🌵):+          𝛿·3·1 := 𝔻(𝜎4:λ)+        𝛿1·3 := 𝛿·3·1  # 𝔻(ξ.on🌵)+        𝕄(ξ.left🌵):+          morphed 𝑛·3·1 := 𝜎5:λ:φ+        𝑛1·3 := 𝑛·3·1  # 𝕄(ξ.left🌵)+        𝕄(ξ.right🌵):+          morphed 𝑛·3·2 := 𝜎6:λ:φ+        𝑛2·3 := 𝑛·3·2  # 𝕄(ξ.right🌵)+        joined 𝜎7 := 𝛿1·3 ? 𝜎5 : 𝜎6+        𝑛·3·3 := 𝜎7:λ:φ+      𝑛3·2 := 𝑛·3·3  # 𝔼(𝑛1)+      cast 𝑛6·2 := 𝜎3:λ:φ  # 𝑛2·2 up to 𝑛3·2+      joined 𝜎8 := 𝛿1·2 ? 𝜎7 : 𝜎3+      𝑛·2·3 := 𝜎8:λ:φ+    morphed 𝑛·0·1 := 𝜎8:λ
+ test-resources/evaluate-packs/joins-a-bare-symbol-a-cast-brought-into-a-side-holding-a-symbol-off-its-phi-chain.yaml view
@@ -0,0 +1,43 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# The right side ends its φ chain in a bare symbol, and it holds another one+# under 'ke', off that chain. What the right side holds does not matter to a+# 'cast' block, which used to cast nothing here (#2187): it casts the bare+# symbol on the left into a copy of the right side with 𝜎2 in place of 𝜎3,+# keeping 𝜎4 under 'ke' (#2223). The two sides then differ in their φ alone,+# and the join makes one term of them with 𝜎5 standing for that φ.+symbolic: |+  - λ: L_fork+    dataize:+      𝛿1: $.c+    morph:+      𝑛1: $.a+      𝑛2: $.b+    cast:+      𝑛3: 𝑛1+      𝑛4: 𝑛2+    join:+      on: 𝛿1+      left: 𝑛3+      right: 𝑛4+location: 'Q.y'+input: '⟦ y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧, ke ↦ ⟦ λ ⤍ 𝜎4 ⟧ ⟧, λ ⤍ L_fork ⟧.φ ⟧'+result: '𝜎5:λ'+protocol: |+  𝕄(Φ.y):+    𝔼(L_fork):+      𝔻(ξ.c):+        𝛿·1·1 := 𝔻(𝜎1:λ)+      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.c)+      𝕄(ξ.a):+        morphed 𝑛·1·1 := 𝜎2:λ+      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.a)+      𝕄(ξ.b):+        morphed 𝑛·1·2 := ⟦ φ ↦ 𝜎3:λ, ke ↦ 𝜎4:λ ⟧+      𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)+      cast 𝑛3·1 := ⟦ φ ↦ 𝜎2:λ, ke ↦ 𝜎4:λ ⟧  # 𝑛1·1 up to 𝑛2·1+      joined 𝜎5 := 𝛿1·1 ? 𝜎2 : 𝜎3+      𝑛·1·3 := ⟦ φ ↦ 𝜎5:λ, ke ↦ 𝜎4:λ ⟧+    morphed 𝑛·0·1 := 𝜎5:λ
+ test-resources/evaluate-packs/joins-a-side-that-raises-through-a-terminator.yaml view
@@ -0,0 +1,56 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# The right side is a copy of 'throw', whose λ function 'L_throw' the entry+# names under 'terminators', the way EO raises its 'T' with a message. The+# side goes through the 'evaluate', 'stay', 'symbolize' and 'defer' lines+# untouched, so 'L_throw' is never fired and its message is never turned+# into a symbol. The join takes it for a side that raises, the way it takes+# ⊥: it keeps the left side, mints 𝜎3 to stand for the raise and names the+# copy of 'throw' in the comment of the 'joined' line (#2263).+symbolic: |+  - λ: L_fork+    terminators: [L_throw]+    dataize:+      𝛿1: $.on🌵+    morph:+      𝑛1: $.left🌵+      𝑛2: $.right🌵+    evaluate:+      𝑛3: 𝑛1+      𝑛4: 𝑛2+    stay:+      𝑛5: 𝑛3+      𝑛6: 𝑛4+    symbolize:+      𝑛7: 𝑛5+      𝑛8: 𝑛6+    defer:+      𝑛9: 𝑛7+      𝑛10: 𝑛8+    join:+      on: 𝛿1+      left: 𝑛9+      right: 𝑛10+      otherwise: L_fork+location: 'Q.x'+input: '⟦ throw(message) ↦ ⟦ λ ⤍ L_throw ⟧, x ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎1 ⟧, left🌵 ↦ ⟦ k ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧, right🌵 ↦ Φ.throw( "bad" ) ⟧.φ ⟧'+result: '𝜎4:λ'+protocol: |+  𝕄(Φ.x):+    𝔼(L_fork):+      𝔻(ξ.on🌵):+        𝛿·1·1 := 𝔻(𝜎1:λ)+      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.on🌵)+      𝕄(ξ.left🌵):+        morphed 𝑛·1·1 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎2:λ ⟧+      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.left🌵)+      𝕄(ξ.right🌵):+        𝑛·1·2 := Φ.throw( message ↦ "bad" )+        𝑛·1·3 := ⟦ message ↦ "bad", λ ⤍ L_throw ⟧+        morphed 𝑛·1·4 := 𝑛·1·3+      𝑛2·1 := 𝑛·1·3  # 𝕄(ξ.right🌵)+      joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3  # where 𝜎3 is ⊥ raised by 𝑛·1·3+      𝑛·1·5 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎4:λ ⟧+    morphed 𝑛·0·1 := 𝜎4:λ
− test-resources/evaluate-packs/leaves-a-bare-symbol-uncast-against-a-side-holding-a-symbol-off-its-phi-chain.yaml 
@@ -1,39 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----# yamllint disable rule:line-length-# The right side ends its φ chain in a bare symbol, but it holds another one-# under 'ke', off that chain. A cast would copy that symbol into the left side-# too, as if the left branch knew it, so a 'cast' block casts nothing here and-# binds both metas to their terms as they are. The join then diverges as it-# would with no 'cast' block at all (#2187).-symbolic: |-  - λ: L_fork-    dataize:-      𝛿1: $.c-    morph:-      𝑛1: $.a-      𝑛2: $.b-    cast:-      𝑛3: 𝑛1-      𝑛4: 𝑛2-    join:-      on: 𝛿1-      left: 𝑛3-      right: 𝑛4-location: 'Q.y'-input: '⟦ y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧, ke ↦ ⟦ λ ⤍ 𝜎4 ⟧ ⟧, λ ⤍ L_fork ⟧.φ ⟧'-fails: "No entry of --symbolic answers the λ function 'L_fork'"-protocol: |-  𝕄(Φ.y):-    𝔼(L_fork):-      𝔻(ξ.c):-        𝛿·1·1 := 𝔻(𝜎1:λ)-      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.c)-      𝕄(ξ.a):-        morphed 𝑛·1·1 := 𝜎2:λ-      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.a)-      𝕄(ξ.b):-        morphed 𝑛·1·2 := ⟦ φ ↦ 𝜎3:λ, ke ↦ 𝜎4:λ ⟧-      𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)-      diverged 𝜎2:λ vs 𝑛2·1  # they differ at .λ, and the join names no otherwise
+ test-resources/evaluate-packs/leaves-a-formation-with-an-attribute-of-its-own-as-it-is.yaml view
@@ -0,0 +1,53 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# The λ of a formation stands for its φ alone, so a dispatch on any other+# attribute it binds must find that attribute in the formation. Each side of+# the fork is a copy of 'box', which binds 'tag' beside its λ, and 'tag' is+# no void 'box' declares. The 'evaluate' lines hand both copies back as they+# are, the join fabricates nothing, since the two copies differ only in their+# symbols, and 'y' comes to the joined 'tag' rather than to a dispatch on a+# symbol (#2265).+symbolic: |+  - λ: L_fork+    dataize:+      𝛿1: $.on🌵+    morph:+      𝑛1: $.left🌵+      𝑛2: $.right🌵+    evaluate:+      𝑛3: 𝑛1+      𝑛4: 𝑛2+    join:+      'on': 𝛿1+      left: 𝑛3+      right: 𝑛4+      otherwise: L_fork+  - λ: L_box+    𝑛: ⟦ λ ⤍ 𝜎 ⟧+location: 'Q.y'+input: >+  ⟦ box(v) ↦ ⟦ tag ↦ ξ.v, λ ⤍ L_box ⟧,+    x ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎1:λ, left🌵 ↦ Φ.box( 𝜎2:λ ), right🌵 ↦ Φ.box( 𝜎3:λ ) ⟧,+    y ↦ Φ.x.tag ⟧+result: '𝜎4:λ'+protocol: |+  𝕄(Φ.y):+    𝔼(L_fork):+      𝔻(ξ.on🌵):+        𝛿·1·1 := 𝔻(𝜎1:λ)+      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.on🌵)+      𝕄(ξ.left🌵):+        𝑛·1·1 := Φ.box( v ↦ 𝜎2:λ )+        𝑛·1·2 := ⟦ v ↦ 𝜎2:λ, tag ↦ v, λ ⤍ L_box ⟧+        morphed 𝑛·1·3 := 𝑛·1·2+      𝑛1·1 := 𝑛·1·2  # 𝕄(ξ.left🌵)+      𝕄(ξ.right🌵):+        𝑛·1·4 := Φ.box( v ↦ 𝜎3:λ )+        𝑛·1·5 := ⟦ v ↦ 𝜎3:λ, tag ↦ v, λ ⤍ L_box ⟧+        morphed 𝑛·1·6 := 𝑛·1·5+      𝑛2·1 := 𝑛·1·5  # 𝕄(ξ.right🌵)+      joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3+      𝑛·1·7 := ⟦ v ↦ 𝜎4:λ, tag ↦ v, λ ⤍ L_box ⟧+    morphed 𝑛·0·1 := 𝜎4:λ
test-resources/evaluate-packs/parks-a-firing-whose-morph-operand-diverged.yaml view
@@ -40,5 +40,5 @@           𝕄(ξ.b):             morphed 𝑛·2·2 := 02-:Δ           𝑛2·2 := 02-:Δ  # 𝕄(ξ.b)-          diverged 𝑛1·2 vs 𝑛2·2  # they differ at .Δ, and the join names no otherwise+          diverged 𝑛1·2 vs 𝑛2·2  # cannot join: at .Δ the left side has Δ ⤍ 01- and the right side has Δ ⤍ 02-; cannot fabricate: the join names no otherwise       stuck L_fork
− test-resources/evaluate-packs/parks-a-firing-whose-operand-dataizes-in-circles.yaml 
@@ -1,37 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----# A loop met while an operand is being brought down to data, with no frame of 𝕄-# ever handed the same term twice: the body of 'cyc' dispatches 'cyc' again, so-# every round 𝕄 stops at a formation of its own and only 𝔻 — 'box'-# contextualizing that body and 'norm' morphing what comes out — comes back to-# the term it started from. Before #1290 the guard of '--acyclic' was 𝕄's alone-# and this went round until the step budget ran out; now 𝔻 asks it too, and the-# spine around the firing parks with the term it had reached when the firing-# started, exactly as it does for a loop 𝕄 catches.-symbolic: |-  - λ: L_outer-    dataize:-      𝛿1: ξ.arg-    𝑛: ⟦ λ ⤍ 𝜎 ⟧-location: 'Q.x'-acyclic: proven-steps: 250-input: >-  ⟦ cyc ↦ ⟦ x ↦ ∅, φ ↦ Φ.cyc( ξ.x ) ⟧,-    x ↦ ⟦ arg ↦ Φ.cyc( ⟦⟧ ), λ ⤍ L_outer ⟧.bar ⟧-result: '⟦ arg ↦ Φ.cyc( ⟦⟧ ), λ ⤍ L_outer ⟧.bar'-protocol: |-  𝕄(Φ.x):-    𝔼(L_outer):-      𝔻(ξ.arg):-        𝕄(ξ.arg):-          𝑛·1·1 := Φ.cyc( x ↦ ⟦⟧ )-          𝑛·1·2 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧-          morphed 𝑛·1·3 := 𝑛·1·2-        boxed 𝑛·1·4 := 𝑛·1·3.φ-        𝕄(𝑛·1·4):-          𝑛·1·5 := Φ.cyc( x ↦ ⟦⟧ )-          𝑛·1·6 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧-          morphed 𝑛·1·7 := 𝑛·1·6-        looped 𝑛·1·7  # 𝔻(𝑛·1·4), proven
− test-resources/evaluate-packs/parks-the-same-dataization-loop-under-partial.yaml 
@@ -1,39 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----# The very program of 'parks-a-firing-whose-operand-dataizes-in-circles', run-# with '--partial' as well. The two flags reach the same place by different-# roads: on its own '--acyclic' lets the loop travel up to the 𝕄 spine around-# the firing, while under '--partial' the operand's own run of 𝔻 ends on the-# residue it had reached and the firing is left with nothing to bind, so it gets-# stuck the way one whose λ function cannot fire does. Either way the site is-# parked and the answer is the same, which is what "--acyclic needs no-# --partial" means for a loop 𝔻 catches (#1290).-symbolic: |-  - λ: L_outer-    dataize:-      𝛿1: ξ.arg-    𝑛: ⟦ λ ⤍ 𝜎 ⟧-location: 'Q.x'-acyclic: proven-partial: true-steps: 250-input: >-  ⟦ cyc ↦ ⟦ x ↦ ∅, φ ↦ Φ.cyc( ξ.x ) ⟧,-    x ↦ ⟦ arg ↦ Φ.cyc( ⟦⟧ ), λ ⤍ L_outer ⟧.bar ⟧-result: '⟦ arg ↦ Φ.cyc( ⟦⟧ ), λ ⤍ L_outer ⟧.bar'-protocol: |-  𝕄(Φ.x):-    𝔼(L_outer):-      𝔻(ξ.arg):-        𝕄(ξ.arg):-          𝑛·1·1 := Φ.cyc( x ↦ ⟦⟧ )-          𝑛·1·2 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧-          morphed 𝑛·1·3 := 𝑛·1·2-        boxed 𝑛·1·4 := 𝑛·1·3.φ-        𝕄(𝑛·1·4):-          𝑛·1·5 := Φ.cyc( x ↦ ⟦⟧ )-          𝑛·1·6 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧-          morphed 𝑛·1·7 := 𝑛·1·6-        looped 𝑛·1·7  # 𝔻(𝑛·1·4), proven-      stuck L_outer
test-resources/evaluate-packs/parks-two-sides-that-do-not-join.yaml view
@@ -29,4 +29,4 @@         morphed 𝑛·1·1 := 01-:Δ:φ       𝕄(ξ.b):         morphed 𝑛·1·2 := 02-:Δ:φ-      diverged 𝑛·1·1 vs 𝑛·1·2  # they differ at .φ.Δ, and the join names no otherwise+      diverged 𝑛·1·1 vs 𝑛·1·2  # cannot join: at .φ.Δ the left side has Δ ⤍ 01- and the right side has Δ ⤍ 02-; cannot fabricate: the join names no otherwise
test-resources/evaluate-packs/passes-a-side-that-is-no-formation-through-an-evaluate-line-to-the-join.yaml view
@@ -50,4 +50,4 @@       𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)       𝑛3·1 := Φ.k  # rewrite(𝑛1)       𝑛4·1 := Φ.j  # rewrite(𝑛2)-      diverged Φ.k vs Φ.j  # the join names no otherwise+      diverged Φ.k vs Φ.j  # cannot join: the left side is Φ.k and the right side is Φ.j; cannot fabricate: the join names no otherwise
+ test-resources/evaluate-packs/refuses-to-fabricate-of-sides-that-disagree-on-a-void.yaml view
@@ -0,0 +1,32 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# The block names 'L_join' under 'otherwise', but the left side leaves 'k'+# void and the right side binds it, so the right side is applied further than+# the left one. A formation leaving 'k' void would hand a void to whoever takes+# 'k' of the right side, so nothing is fabricated: the firing writes 'unripe',+# naming the attribute and the side leaving it void, and gets stuck (#2202).+symbolic: |+  - λ: L_fork+    dataize:+      𝛿1: $.c+    join:+      on: 𝛿1+      left: $.a+      right: $.b+      otherwise: L_join+location: 'Q.y'+input: '⟦ y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, k ↦ ∅ ⟧, b ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧, k ↦ ⟦ ⟧ ⟧, λ ⤍ L_fork ⟧.φ ⟧'+fails: "No entry of --symbolic answers the λ function 'L_fork'"+protocol: |+  𝕄(Φ.y):+    𝔼(L_fork):+      𝔻(ξ.c):+        𝛿·1·1 := 𝔻(𝜎1:λ)+      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.c)+      𝕄(ξ.a):+        morphed 𝑛·1·1 := ⟦ φ ↦ 𝜎2:λ, k ↦ ∅ ⟧+      𝕄(ξ.b):+        morphed 𝑛·1·2 := ⟦ φ ↦ 𝜎3:λ, k ↦ ⟦⟧ ⟧+      unripe 𝑛·1·1 vs 𝑛·1·2  # k is void on the left and attached on the right
test-resources/evaluate-packs/spends-a-step-on-every-firing-of-an-evaluate-line.yaml view
@@ -11,21 +11,21 @@ symbolic: |   - λ: L_loop     morph:-      𝑛1: $.next+      𝑛1: $.next🌵     evaluate:       𝑛2: 𝑛1     𝑛: 𝑛2 location: 'Q.app' steps: 6 firings: 20-input: '⟦ loop ↦ ⟦ next ↦ Φ.loop, λ ⤍ L_loop ⟧, app ↦ Φ.loop.φ ⟧'+input: '⟦ loop ↦ ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧, app ↦ Φ.loop.φ ⟧' fails: 'reaching the limit of steps' protocol: |   𝕄(Φ.app):     𝔼(L_loop):-      𝕄(ξ.next):-        morphed 𝑛·1·1 := ⟦ next ↦ Φ.loop, λ ⤍ L_loop ⟧-      𝑛1·1 := ⟦ next ↦ Φ.loop, λ ⤍ L_loop ⟧  # 𝕄(ξ.next)+      𝕄(ξ.next🌵):+        morphed 𝑛·1·1 := ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧+      𝑛1·1 := ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧  # 𝕄(ξ.next🌵)       𝔼(L_loop):  # 𝔼(𝑛1)-        𝕄(ξ.next):+        𝕄(ξ.next🌵):           starved 6
test-resources/evaluate-packs/tells-why-a-join-fabricated-nothing-of-a-side-that-is-no-formation.yaml view
@@ -39,4 +39,4 @@         morphed 𝑛·1·1 := Φ.k:φ       𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.a)       𝑛2·1 := Φ.k  # rewrite(𝑛1)-      diverged 𝑛1·1 vs 𝑛2·1  # the right side is no formation+      diverged 𝑛1·1 vs 𝑛2·1  # cannot join: the left side is 𝑛·1·1 and the right side is Φ.k; cannot fabricate: the right side is no formation
test/CLISpec.hs view
@@ -1480,17 +1480,17 @@             ["dataize", "--locator=Q.t", "--max-steps=40"]             ["[ERROR]: Morphing did not finish before reaching the limit of steps: --max-steps=40"] -      it "names the term it came back to with the flag" $+      it "answers the copy it came back to with a symbol with the flag" $         withStdin circling $-          testCLIFailed+          testCLISucceeded             ["dataize", "--locator=Q.t", "--acyclic=proven", "--max-steps=4000"]-            ["[ERROR]: Reduction entered a formation it is already inside:"]+            ["40-45-00-00-00-00-00-00"] -      it "prints the residue and exits successfully with --partial" $+      it "answers the same with --partial" $         withStdin circling $           testCLISucceeded             ["dataize", "--locator=Q.t", "--acyclic=proven", "--partial", "--max-steps=4000", "--flat", "--hide-rho"]-            ["Φ.cyc( α0 ↦ ⟦⟧ )"]+            ["40-45-00-00-00-00-00-00"]        it "writes the cut to the protocol where the formation would have opened" $         withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do@@ -1511,7 +1511,10 @@                        , "    𝑛·0·5 := Φ.cyc( x ↦ ⟦⟧ )"                        , "    𝑛·0·6 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧"                        , "    morphed 𝑛·0·7 := 𝑛·0·6"-                       , "  looped 𝑛·0·7  # 𝔻(𝑛·0·4), proven"+                       , "  𝕄(𝑛·0·7.x):"+                       , "    morphed 𝑛·0·8 := ⟦⟧"+                       , "  looped 𝜎1 := Φ.cyc( x ↦ 𝑛·0·8 )  # 𝔻(𝑛·0·4), proven, repeats 𝑛·0·7"+                       , "  𝛿·0·1 := 𝔻(𝜎1:λ)"                        ]        it "writes the cut to the XML protocol with the formation in an element of its own" $@@ -1537,7 +1540,11 @@                        , "    <formed meta=\"𝑛·0·6\" of=\"Φ.cyc\"><meta attr=\"x\">𝑒·0·1</meta></formed>"                        , "    <morphed meta=\"𝑛·0·7\">𝑛·0·6</morphed>"                        , "  </morph>"-                       , "  <looped by=\"dataize\" match=\"proven\" at=\"𝑛·0·4\" of=\"𝑛·0·7\"/>"+                       , "  <morph at=\"𝑛·0·7.x\">"+                       , "    <morphed meta=\"𝑛·0·8\">𝑒·0·1</morphed>"+                       , "  </morph>"+                       , "  <looped symbol=\"𝜎1\" by=\"dataize\" match=\"proven\" at=\"𝑛·0·4\" of=\"𝑛·0·7\" object=\"Φ.cyc\"><with><meta attr=\"x\">𝑛·0·8</meta></with></looped>"+                       , "  <manufactured meta=\"𝛿·0·1\">𝜎1</manufactured>"                        , "</dataize>"                        ] @@ -1549,7 +1556,7 @@               ["dataize", "--locator=Q.t", "--acyclic=plausible", "--partial", "--protocol=" ++ path, "--sweet", "--hide-rho", "--flat", "--quiet"]               []           records <- readProtocol path-          lines records `shouldContain` ["  looped 𝑛·0·7  # 𝔻(𝑛·0·4), plausible"]+          lines records `shouldContain` ["  looped 𝜎1 := Φ.cyc( x ↦ 𝑛·0·8 )  # 𝔻(𝑛·0·4), plausible, repeats 𝑛·0·7"]        it "refuses the flag without a mode" $         withStdin "⟦ t ↦ ⟦ Δ ⤍ 01-02 ⟧ ⟧" $@@ -1567,9 +1574,9 @@       let once = "⟦ f ↦ ⟦ x ↦ ∅, φ ↦ ξ.x.again ⟧, start ↦ ⟦ again ↦ Φ.f( x ↦ Φ.stop( v ↦ Φ.start ) ) ⟧, stop ↦ ⟦ v ↦ ∅, again ↦ ⟦ Δ ⤍ 01- ⟧ ⟧, t ↦ Φ.f( x ↦ Φ.start ) ⟧"       it "cuts a recursion that stops after one round without the flag" $         withStdin once $-          testCLIFailed+          testCLISucceeded             ["dataize", "--locator=Q.t", "--acyclic=plausible"]-            ["[ERROR]: Reduction entered a formation it is already inside:"]+            ["40-45-00-00-00-00-00-00"]        it "dataizes a recursion that stops after one round with --max-loops=1" $         withStdin once $@@ -1577,9 +1584,9 @@        it "cuts a recursion that never stops with --max-loops=1" $         withStdin "⟦ cyc ↦ ⟦ x ↦ ∅, φ ↦ Φ.cyc( ξ.x ) ⟧, t ↦ Φ.cyc( ⟦⟧ ) ⟧" $-          testCLIFailed+          testCLISucceeded             ["dataize", "--locator=Q.t", "--acyclic=proven", "--max-loops=1", "--max-steps=4000"]-            ["[ERROR]: Reduction entered a formation it is already inside:"]+            ["40-45-00-00-00-00-00-00"]        it "refuses a negative count" $         withStdin once $@@ -1589,6 +1596,78 @@         withStdin once $           testCLIFailed ["dataize", "--locator=Q.t", "--max-loops=1"] ["The option --max-loops requires --acyclic, since only --acyclic cuts a loop"] +    describe "--acyclic at a recursive call" $ do+      let recursive = "⟦ call(a) ↦ ⟦ λ ⤍ L_call ⟧, wrap(v) ↦ ⟦⟧, down(i) ↦ ⟦ φ ↦ Φ.call( a ↦ Φ.down( i ↦ Φ.wrap( v ↦ i ) ) ) ⟧, t ↦ Φ.down( i ↦ ⟦ Δ ⤍ 01- ⟧ ) ⟧"+          calling = T.pack "- λ: L_call\n  morph:\n    𝑛1: $.a\n  evaluate:\n    𝑛2: 𝑛1\n  𝑛: 𝑛2\n"+          recorded :: String -> IO [String]+          recorded name =+            withTempFile name $ \(path, stream) -> do+              hClose stream+              withLambdasOf calling $ \file ->+                withStdin recursive $+                  testCLISucceeded+                    ["dataize", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=plausible", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"]+                    []+              lines <$> readProtocol path+      it "answers the recursive call it cuts with a fresh symbol and goes on" $+        withLambdasOf calling $ \file ->+          withStdin recursive $+            testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=plausible"] ["40-45-00-00-00-00-00-00"]++      it "writes the recursive call it cuts to the protocol as a call of the object" $+        recorded "protocolXXXXXX.txt" >>= (`shouldContain` ["      looped 𝜎1 := Φ.down( i ↦ 𝑛·1·6 )  # plausible, repeats 𝑛·0·3"])++      it "writes the recursive call it cuts to the XML protocol with the object and the metas of its arguments" $+        recorded "protocolXXXXXX.xml" >>= (`shouldContain` ["      <looped symbol=\"𝜎1\" by=\"morph\" match=\"plausible\" at=\"ξ.a\" of=\"𝑛·0·3\" object=\"Φ.down\"><with><meta attr=\"i\">𝑛·1·6</meta></with></looped>"])++    describe "--acyclic at a recursive call through a fork" $ do+      let recursive = "⟦ if(c, a, b) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ξ.c, left🌵 ↦ ξ.a, right🌵 ↦ ξ.b ⟧, wrap(v) ↦ ⟦⟧, down(i) ↦ ⟦ φ ↦ Φ.if( c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ Φ.down( i ↦ Φ.wrap( v ↦ i ) ), b ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧ ) ⟧, t ↦ Φ.down( i ↦ ⟦ Δ ⤍ 01- ⟧ ) ⟧"+          forking = T.pack "- λ: L_fork\n  dataize:\n    𝛿1: $.on🌵\n  morph:\n    𝑛1: $.left🌵\n    𝑛2: $.right🌵\n  evaluate:\n    𝑛3: 𝑛1\n    𝑛4: 𝑛2\n  cast:\n    𝑛5: 𝑛3\n    𝑛6: 𝑛4\n  join:\n    on: 𝛿1\n    left: 𝑛5\n    right: 𝑛6\n    otherwise: L_fork\n"+          recorded :: String -> String -> IO [String]+          recorded loops name =+            withTempFile name $ \(path, stream) -> do+              hClose stream+              withLambdasOf forking $ \file ->+                withStdin recursive $+                  testCLISucceeded+                    ["dataize", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=plausible", "--max-loops=" ++ loops, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"]+                    []+              lines <$> readProtocol path+      it "answers the copy a side of a fork makes again with a fresh symbol and joins" $+        withLambdasOf forking $ \file ->+          withStdin recursive $+            testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=plausible", "--max-loops=1"] ["40-45-00-00-00-00-00-00"]++      it "writes the copy it cuts in a side of a fork to the protocol as a call of the object" $+        recorded "1" "protocolXXXXXX.txt" >>= (`shouldContain` ["        looped 𝜎3 := Φ.down( i ↦ 𝑛·3·6 )  # plausible, repeats 𝑛·0·3"])++      it "writes the copy it cuts in a side of a fork to the XML protocol with the object and the metas of its arguments" $+        recorded "1" "protocolXXXXXX.xml" >>= (`shouldContain` ["        <looped symbol=\"𝜎3\" by=\"morph\" match=\"plausible\" at=\"ξ.left🌵\" of=\"𝑛·0·3\" object=\"Φ.down\"><with><meta attr=\"i\">𝑛·3·6</meta></with></looped>"])++      it "counts the copies the sides of earlier rounds of a fork made under --max-loops=2" $+        recorded "2" "protocolXXXXXX.txt" >>= (`shouldContain` ["          looped 𝜎3 := Φ.down( i ↦ 𝑛·6·6 )  # plausible, repeats 𝑛·0·3"])++    describe "--acyclic at a copy holding a λ" $ do+      let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, down(i) ↦ ⟦ φ ↦ Φ.dataized( Φ.fork( Φ.dataized( Φ.down( ⟦ λ ⤍ 𝜎2 ⟧ ) ), ⟦ λ ⤍ 𝜎3 ⟧ ) ) ⟧, x ↦ Φ.down( ⟦ λ ⤍ 𝜎1 ⟧ ) ⟧"+          forking = T.pack "- λ: L_fork\n  dataize:\n    𝛿1: $.on🌵\n  morph:\n    𝑛1: $.left🌵\n    𝑛2: $.right🌵\n  evaluate:\n    𝑛3: 𝑛1\n    𝑛4: 𝑛2\n  join:\n    on: 𝛿1\n    left: 𝑛3\n    right: 𝑛4\n    otherwise: L_fork\n- λ: L_dataized\n  dataize:\n    𝛿1: $.target\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n"+          recorded :: String -> IO [String]+          recorded name =+            withTempFile name $ \(path, stream) -> do+              hClose stream+              withLambdasOf forking $ \file ->+                withStdin recursive $+                  testCLISucceeded+                    ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"]+                    []+              lines <$> readProtocol path+      it "answers the copy holding a λ it cuts with a fresh symbol and goes on" $+        withLambdasOf forking $ \file ->+          withStdin recursive $+            testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2"] ["40-45-00-00-00-00-00-00"]++      it "writes the copy holding a λ it cuts to the protocol as a call of the object" $+        recorded "protocolXXXXXX.txt" >>= (`shouldContain` ["                      looped 𝜎8 := Φ.dataized( target ↦ 𝜎7:λ )  # 𝔻(𝑛·6·4), plausible, repeats 𝑛·7·2"])+     it "dataizes with --sequence" $       withStdin "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]" $         testCLISucceeded@@ -2559,7 +2638,7 @@                          , "      <formed meta=\"𝑒·1·2\"><datum attr=\"φ\">02-</datum></formed>"                          , "      <morphed meta=\"𝑛·1·2\">𝑒·1·2</morphed>"                          , "    </morph>"-                         , "    <diverged left=\"𝑛·1·1\" right=\"𝑛·1·2\" at=\".φ.Δ\" reason=\"the join names no otherwise\"/>"+                         , "    <diverged left=\"𝑛·1·1\" right=\"𝑛·1·2\" at=\".φ.Δ\" reason=\"the join names no otherwise\"><left Δ=\"01-\"/><right Δ=\"02-\"/></diverged>"                          , "  </evaluate>"                          , "</morph>"                          ]@@ -3567,7 +3646,7 @@                      , "    </morph>"                      , "    <bound meta=\"𝑛2·1\">𝑛·1·4</bound>"                      , "    <deferred symbol=\"𝜎3\" by=\"morph\" at=\"𝑛2.φ\" of=\"Φ.step\"><with><symbol attr=\"tup\">𝜎1</symbol></with></deferred>"-                     , "    <diverged left=\"01-\" right=\"𝜎3\" at=\".Δ\" reason=\"the join names no otherwise\"/>"+                     , "    <diverged left=\"01-\" right=\"𝜎3\" at=\".Δ\" reason=\"the join names no otherwise\"><left Δ=\"01-\"/><right/></diverged>"                      , "  </evaluate>"                      , "</dataize>"                      ]
test/DepsSpec.hs view
@@ -12,7 +12,7 @@ import Data.List (isInfixOf, isPrefixOf) import Data.Time (LocalTime (LocalTime), TimeOfDay (TimeOfDay), ZonedTime (ZonedTime), fromGregorian, hoursToTimeZone) import Data.Time.Clock.POSIX (getPOSIXTime)-import Deps (Acyclic (Proven), Evaluation (EvAnswer, EvApplied, EvBound, EvBoxed, EvBuilt, EvCast, EvData, EvDeferred, EvDelta, EvDiverged, EvFabricated, EvFiring, EvHeader, EvJoined, EvLooped, EvManufactured, EvMorphed, EvReshaped, EvRun, EvStarted, EvStuck, EvStuckOn, EvSymbolized, EvTaken, EvTerm, EvUndressed, EvWorld), Header (Header), Judgment (Dataization, Evaluation, Morphing), Nesting (..), Protocol (..), World (World), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, resited, saveStep)+import Deps (Acyclic (Proven), Evaluation (EvAnswer, EvApplied, EvBound, EvBoxed, EvBuilt, EvCast, EvData, EvDeferred, EvDelta, EvDiverged, EvFabricated, EvFiring, EvHeader, EvJoined, EvLooped, EvManufactured, EvMorphed, EvReshaped, EvRun, EvStarted, EvStuck, EvStuckOn, EvSymbolized, EvTaken, EvTerm, EvUndressed, EvUnripe, EvWorld), Header (Header), Judgment (Dataization, Evaluation, Morphing), Nesting (..), Protocol (..), World (World), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, resited, saveStep) import Fixtures (readUtf8, recorded, recordedWhole, recordedXml) import Forks (Refusal (..), Side (..)) import GHC.Clock (getMonotonicTime)@@ -253,8 +253,11 @@       (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_клёст" Dataization ExRoot, EvTaken 2 (ExFormation [BiTau (AtLabel "жук") (ExFormation [BiLambda (FnSymbol 7)]), BiTau AtPhi (ExDispatch ExXi (AtLabel "жук"))]), EvBoxed 1 (ExDispatch (ExFormation [BiTau (AtLabel "жук") (ExFormation [BiLambda (FnSymbol 7)]), BiTau AtPhi (ExDispatch ExXi (AtLabel "жук"))]) AtPhi)])       last (lines written) `shouldBe` "  boxed 𝑛·0·1 := 𝑛·1·1.φ"     it "keeps the mode of a cut made at the site of its block" $ do-      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvLooped 1 Morphing Proven (ExFormation []) ExRoot])+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvLooped 1 Morphing Proven (ExFormation []) ExRoot Nothing])       last (lines written) `shouldBe` "  looped ⟦⟧  # proven"+    it "writes a cut that answered a copy as the call of the object it repeats" $ do+      (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvLooped 1 Dataization Proven (ExFormation []) ExRoot (Just (14, ExApplication (ExDispatch ExRoot (AtLabel "клён")) (ArTau (AtLabel "ось") (ExFormation [BiLambda (FnSymbol 3)]))))])+      last (lines written) `shouldBe` "  looped 𝜎14 := Φ.клён( ось ↦ 𝜎3:λ )  # proven, repeats ⟦⟧"     it "names the block over an answer by the line that built it" $ do       (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_ф" Dataization ExRoot, EvBuilt 2 (ExDispatch ExRoot (AtLabel "ю")), EvStarted 2 Morphing (ExDispatch ExRoot (AtLabel "ю")), EvApplied 3 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) (ExDispatch ExRoot (AtLabel "ю"))])       lines written `shouldContain` ["    𝕄(𝑛·1·1):"]@@ -299,31 +302,46 @@       last (lines written) `shouldBe` "    𝔼(L_ю):  # 𝔼(Φ.щ)"     it "names the term a meta that wrote no line holds where a join could not join the side that meta bound" $ do       (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvBound 2 (ExMeta "n1") (ExDispatch ExRoot (AtLabel "ёж")), EvDiverged 2 (ExMeta "n1", ExDispatch ExRoot (AtLabel "ёж")) (ExMeta "n2", ExDispatch ExRoot (AtLabel "щука")) [] (Unformed Lefthand)])-      last (lines written) `shouldBe` "    diverged Φ.ёж vs 𝑛2·1  # the left side is no formation"+      last (lines written) `shouldBe` "    diverged Φ.ёж vs 𝑛2·1  # cannot join: the left side is Φ.ёж and the right side is Φ.щука; cannot fabricate: the left side is no formation"     it "writes the symbol a join minted beside the meta its condition was bound to and the two it stands for" $ do-      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿3") 12 (5, 9) Nothing])+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿3") 12 (5, 9) Nothing Nothing])       last (lines written) `shouldBe` "    joined 𝜎12 := 𝛿3·1 ? 𝜎5 : 𝜎9"     it "writes the symbol a join minted beside the path its condition was read off" $ do-      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Right (ExDispatch ExXi (AtLabel "щит"))) 12 (5, 9) Nothing])+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Right (ExDispatch ExXi (AtLabel "щит"))) 12 (5, 9) Nothing Nothing])       last (lines written) `shouldBe` "    joined 𝜎12 := ξ.щит ? 𝜎5 : 𝜎9"     it "writes the symbol standing for ⊥ in a join with a comment saying it is ⊥" $ do-      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿1") 4 (2, 3) (Just 3)])+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿1") 4 (2, 3) (Just 3) Nothing])       last (lines written) `shouldBe` "    joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3  # where 𝜎3 is ⊥"+    it "writes the object a side raises with beside the symbol standing for ⊥ in a join" $ do+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "бросок")) (ArTau (AtLabel "весть") (ExFormation []))) (ExFormation [BiTau (AtLabel "весть") (ExFormation []), BiLambda (Function "L_бросок")]) ExRoot, EvJoined 2 (Left "𝛿1") 4 (2, 3) (Just 3) (Just (ExFormation [BiTau (AtLabel "весть") (ExFormation []), BiLambda (Function "L_бросок")]))])+      last (lines written) `shouldBe` "    joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3  # where 𝜎3 is ⊥ raised by 𝑛·1·2"     it "writes two sides a join could not join by the formations applications made" $ do       (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "жук")) (ArTau (AtLabel "w") (ExFormation []))) (ExFormation [BiTau (AtLabel "w") (ExFormation [])]) ExRoot, EvDiverged 2 (ExDispatch ExXi (AtLabel "then"), ExFormation [BiTau (AtLabel "q") (ExFormation [])]) (ExDispatch ExXi (AtLabel "else"), ExFormation [BiTau (AtLabel "w") (ExFormation [])]) [AtLabel "q"] Unnamed])-      last (lines written) `shouldBe` "    diverged 𝑛·1·2 vs 𝑛·1·4  # they differ at .q, and the join names no otherwise"+      last (lines written) `shouldBe` "    diverged 𝑛·1·2 vs 𝑛·1·4  # cannot join: at .q the left side has q ↦ ⟦⟧ and the right side has no q; cannot fabricate: the join names no otherwise"     it "writes two sides a join could not join by the metas of the lines that bound them" $ do       (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvTerm 2 "𝑛1" Morphing (ExDispatch ExXi (AtLabel "a")) (ExFormation [BiTau AtPhi (ExFormation [BiDelta (BtOne "1F")])]), EvTerm 2 "𝑛2" Morphing (ExDispatch ExXi (AtLabel "b")) (ExFormation [BiTau AtPhi (ExFormation [BiDelta (BtOne "2E")])]), EvDiverged 2 (ExMeta "n1", ExFormation [BiTau AtPhi (ExFormation [BiDelta (BtOne "1F")])]) (ExMeta "n2", ExFormation [BiTau AtPhi (ExFormation [BiDelta (BtOne "2E")])]) [AtPhi, AtDelta] Unnamed])-      last (lines written) `shouldBe` "    diverged 𝑛1·1 vs 𝑛2·1  # they differ at .φ.Δ, and the join names no otherwise"+      last (lines written) `shouldBe` "    diverged 𝑛1·1 vs 𝑛2·1  # cannot join: at .φ.Δ the left side has Δ ⤍ 1F- and the right side has Δ ⤍ 2E-; cannot fabricate: the join names no otherwise"     it "writes a side of a join no line named as the term it is" $ do       (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvDiverged 2 (ExDispatch ExXi (AtLabel "a"), ExDispatch ExRoot (AtLabel "ёж")) (ExDispatch ExXi (AtLabel "b"), ExDispatch ExRoot (AtLabel "щука")) [] (Unformed Lefthand)])-      last (lines written) `shouldBe` "    diverged Φ.ёж vs Φ.щука  # the left side is no formation"+      last (lines written) `shouldBe` "    diverged Φ.ёж vs Φ.щука  # cannot join: the left side is Φ.ёж and the right side is Φ.щука; cannot fabricate: the left side is no formation"     it "writes a side of a join a defer line bound to a symbol as that symbol" $ do       (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvDiverged 2 (ExMeta "n7", ExFormation [BiLambda (FnSymbol 4)]) (ExDispatch ExXi (AtLabel "b"), ExDispatch ExRoot (AtLabel "щука")) [] (Holding Lefthand AtLambda)])-      last (lines written) `shouldBe` "    diverged 𝜎4:λ vs Φ.щука  # the left side has λ"+      last (lines written) `shouldBe` "    diverged 𝜎4:λ vs Φ.щука  # cannot join: the left side is 𝜎4:λ and the right side is Φ.щука; cannot fabricate: the left side is an atom"     it "writes where the two sides of a join differ beside why no formation was fabricated of them" $ do       (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvDiverged 2 (ExMeta "n2", ExFormation [BiTau AtPhi (ExFormation [BiTau (AtLabel "ко") (ExDispatch ExRoot (AtLabel "уж"))])]) (ExMeta "n9", ExFormation [BiTau AtPhi (ExFormation [BiTau (AtLabel "ко") (ExDispatch ExRoot (AtLabel "ёрш"))]), BiDelta (BtOne "3C")]) [AtPhi, AtLabel "ко"] (Holding Righthand AtDelta)])-      last (lines written) `shouldBe` "    diverged 𝑛2·1 vs 𝑛9·1  # they differ at .φ.ко, and the right side has Δ"+      last (lines written) `shouldBe` "    diverged 𝑛2·1 vs 𝑛9·1  # cannot join: at .φ.ко the left side has ко ↦ Φ.уж and the right side has ко ↦ Φ.ёрш; cannot fabricate: the right side is a datum"+    it "writes that a side of a join binds nothing where the other one binds a λ" $ do+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvDiverged 2 (ExMeta "n5", ExFormation [BiLambda (FnSymbol 8)]) (ExMeta "n6", ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёрш"))]) [AtLambda] (Holding Lefthand AtLambda)])+      last (lines written) `shouldBe` "    diverged 𝜎8:λ vs 𝑛6·1  # cannot join: at .λ the left side has λ ⤍ 𝜎8 and the right side has no λ; cannot fabricate: the left side is an atom"+    it "writes the void a side of a join leaves where the two sides differ" $ do+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvDiverged 2 (ExMeta "n3", ExFormation [BiVoid (AtLabel "щи")]) (ExMeta "n4", ExFormation [BiTau (AtLabel "щи") (ExDispatch ExRoot (AtLabel "ёж"))]) [AtLabel "щи"] Unnamed])+      last (lines written) `shouldBe` "    diverged 𝑛3·1 vs 𝑛4·1  # cannot join: at .щи the left side has щи ↦ ∅ and the right side has щи ↦ Φ.ёж; cannot fabricate: the join names no otherwise"+    it "writes two sides a join could not join for an attribute the left one leaves void as unripe" $ do+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvUnripe 2 (ExMeta "n1", ExFormation [BiVoid (AtLabel "кот")]) (ExMeta "n2", ExFormation [BiTau (AtLabel "кот") (ExDispatch ExRoot (AtLabel "ёж"))]) Lefthand (AtLabel "кот")])+      last (lines written) `shouldBe` "    unripe 𝑛1·1 vs 𝑛2·1  # кот is void on the left and attached on the right"+    it "writes two sides a join could not join for an attribute the right one leaves void as unripe" $ do+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvUnripe 2 (ExDispatch ExXi (AtLabel "a"), ExDispatch ExRoot (AtLabel "уж")) (ExMeta "n5", ExFormation [BiVoid (AtLabel "лис")]) Righthand (AtLabel "лис")])+      last (lines written) `shouldBe` "    unripe Φ.уж vs 𝑛5·1  # лис is void on the right and attached on the left"     it "writes the formation a join fabricated beside the metas of the lines that bound its sides" $ do       (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvFabricated 2 (ExMeta "n1", ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) (ExMeta "n2", ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) (ExFormation [BiTau AtPhi (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) AtPhi), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) AtPhi)]), BiTau (AtLabel "к") (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) (AtLabel "к")), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) (AtLabel "к"))])])])       last (lines written) `shouldSatisfy` isPrefixOf "    fabricated 𝑛·1·1 := 𝑛1·1 and 𝑛2·1  # "@@ -501,7 +519,7 @@       lines written `shouldContain` ["    <cast meta=\"𝑛9·1\" of=\"Φ.ёрш\" up-to=\"𝑛4·1\">𝑒·1·2</cast>"]     it "names the term a meta that wrote no element holds where a join could not join the side that meta bound in the markup" $ do       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvBound 2 (ExMeta "n5") (ExDispatch ExRoot (AtLabel "ёж")), EvDiverged 2 (ExMeta "n5", ExDispatch ExRoot (AtLabel "ёж")) (ExMeta "n6", ExDispatch ExRoot (AtLabel "ёрш")) [] (Unformed Lefthand)])-      lines written `shouldContain` ["    <diverged left=\"Φ.ёж\" right=\"𝑛6·1\" reason=\"the left side is no formation\"/>"]+      lines written `shouldContain` ["    <diverged left=\"Φ.ёж\" right=\"𝑛6·1\" reason=\"the left side is no formation\"><left>Φ.ёж</left><right>Φ.ёрш</right></diverged>"]     it "names the term a meta that wrote no element holds at the site of a firing it was read for in the markup" $ do       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvBound 2 (ExMeta "n4") (ExDispatch ExRoot (AtLabel "щ")), EvFiring 2 "L_ю" Evaluation (ExMeta "n4")])       lines written `shouldContain` ["    <evaluate λ=\"L_ю\" by=\"evaluate\" at=\"Φ.щ\">"]@@ -590,8 +608,11 @@       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvDeferred 1 9 Morphing (ExFormation []) (Just (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "щ") (ExApplication (ExDispatch ExRoot (AtLabel "ю")) (ArTau (AtLabel "ж") (ExFormation [BiLambda (FnSymbol 2)])))))) ExRoot, EvDeferred 1 10 Morphing (ExFormation []) (Just (ExApplication (ExDispatch ExRoot (AtLabel "ёрш")) (ArTau (AtLabel "ц") (ExApplication (ExDispatch ExRoot (AtLabel "ю")) (ArTau (AtLabel "ж") (ExFormation [BiLambda (FnSymbol 2)])))))) ExRoot])       length (filter (isInfixOf ">𝑒1<") (lines written)) `shouldBe` 2     it "writes a cut that answered no copy as an element naming the formation it entered" $ do-      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvLooped 1 Morphing Proven (ExFormation [BiTau (AtLabel "ъ") ExRoot]) ExRoot])+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvLooped 1 Morphing Proven (ExFormation [BiTau (AtLabel "ъ") ExRoot]) ExRoot Nothing])       lines written `shouldContain` ["  <looped by=\"morph\" match=\"proven\" at=\"Φ\" of=\"𝑒·0·1\"/>"]+    it "writes a cut that answered a copy as an element naming the formation it repeats, the object and its arguments" $ do+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Dataization "Φ", EvLooped 1 Dataization Proven (ExFormation [BiTau (AtLabel "ъ") ExRoot]) ExRoot (Just (14, ExApplication (ExDispatch ExRoot (AtLabel "клён")) (ArTau (AtLabel "ось") (ExFormation [BiLambda (FnSymbol 3)]))))])+      lines written `shouldContain` ["  <looped symbol=\"𝜎14\" by=\"dataize\" match=\"proven\" at=\"Φ\" of=\"𝑒·0·1\" object=\"Φ.клён\"><with><symbol attr=\"ось\">𝜎3</symbol></with></looped>"]     it "names an argument of a deferred copy by the formation an application made" $ do       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "кулик")) (ArTau (AtLabel "ш") ExRoot)) (ExFormation [BiTau (AtLabel "ш") ExRoot]) ExRoot, EvDeferred 1 31 Morphing (ExFormation [BiTau (AtLabel "щ") (ExFormation [BiTau (AtLabel "ш") ExRoot]), BiTau AtPhi (ExDispatch ExXi (AtLabel "щ"))]) (Just (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "щ") (ExFormation [BiTau (AtLabel "ш") ExRoot])))) ExRoot])       lines written `shouldContain` ["  <deferred symbol=\"𝜎31\" by=\"morph\" at=\"Φ\" of=\"Φ.ёж\"><with><meta attr=\"щ\">𝑛·0·2</meta></with></deferred>"]@@ -599,29 +620,38 @@       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvTaken 2 (ExFormation [BiLambda (FnSymbol 3)])])       lines written `shouldContain` ["    <answered meta=\"𝑛·1·1\">𝜎3</answered>"]     it "writes the symbol a join minted as an element naming the meta its condition was bound to and the two it stands for" $ do-      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿3") 12 (5, 9) Nothing])+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿3") 12 (5, 9) Nothing Nothing])       lines written `shouldContain` ["    <joined symbol=\"𝜎12\" on=\"𝛿3·1\" left=\"𝜎5\" right=\"𝜎9\"/>"]     it "writes the symbol a join minted as an element naming the path its condition was read off" $ do-      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Right (ExDispatch ExXi (AtLabel "щит"))) 12 (5, 9) Nothing])+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Right (ExDispatch ExXi (AtLabel "щит"))) 12 (5, 9) Nothing Nothing])       lines written `shouldContain` ["    <joined symbol=\"𝜎12\" on=\"ξ.щит\" left=\"𝜎5\" right=\"𝜎9\"/>"]     it "writes the symbol standing for ⊥ in the markup and names it under terminator" $ do-      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿4") 17 (16, 6) (Just 16)])+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿4") 17 (16, 6) (Just 16) Nothing])       lines written `shouldContain` ["    <joined symbol=\"𝜎17\" on=\"𝛿4·1\" left=\"𝜎16\" right=\"𝜎6\" terminator=\"𝜎16\"/>"]+    it "names in the markup the object a side raises with beside the symbol standing for ⊥" $ do+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "бросок")) (ArTau (AtLabel "весть") (ExFormation []))) (ExFormation [BiTau (AtLabel "весть") (ExFormation []), BiLambda (Function "L_бросок")]) ExRoot, EvJoined 2 (Left "𝛿4") 17 (16, 6) (Just 16) (Just (ExFormation [BiTau (AtLabel "весть") (ExFormation []), BiLambda (Function "L_бросок")]))])+      lines written `shouldContain` ["    <joined symbol=\"𝜎17\" on=\"𝛿4·1\" left=\"𝜎16\" right=\"𝜎6\" terminator=\"𝜎16\" raised=\"𝑛·1·2\"/>"]     it "writes no terminator in the markup for a pair of a join that met ⊥ elsewhere" $ do-      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿2") 23 (8, 14) (Just 21)])+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿2") 23 (8, 14) (Just 21) Nothing])       lines written `shouldContain` ["    <joined symbol=\"𝜎23\" on=\"𝛿2·1\" left=\"𝜎8\" right=\"𝜎14\"/>"]     it "writes two sides a join could not join as an element naming both" $ do       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "ю")))) (ExFormation [BiTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "ю"))]) ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "жук")) (ArTau (AtLabel "w") (ExDispatch ExRoot (AtLabel "ю")))) (ExFormation [BiTau (AtLabel "w") (ExDispatch ExRoot (AtLabel "ю"))]) ExRoot, EvDiverged 2 (ExDispatch ExXi (AtLabel "then"), ExFormation [BiTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "ю"))]) (ExDispatch ExXi (AtLabel "else"), ExFormation [BiTau (AtLabel "w") (ExDispatch ExRoot (AtLabel "ю"))]) [AtLabel "q"] Unnamed])-      lines written `shouldContain` ["    <diverged left=\"𝑛·1·2\" right=\"𝑛·1·4\" at=\".q\" reason=\"the join names no otherwise\"/>"]+      lines written `shouldContain` ["    <diverged left=\"𝑛·1·2\" right=\"𝑛·1·4\" at=\".q\" reason=\"the join names no otherwise\"><left><ref attr=\"q\">Φ.ю</ref></left><right/></diverged>"]     it "writes a side of a join that is a path as that path in the markup" $ do       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvDiverged 2 (ExDispatch ExXi (AtLabel "a"), ExDispatch ExRoot (AtLabel "ёж")) (ExDispatch ExXi (AtLabel "b"), ExDispatch ExRoot (AtLabel "щука")) [] (Unformed Righthand)])-      lines written `shouldContain` ["    <diverged left=\"Φ.ёж\" right=\"Φ.щука\" reason=\"the right side is no formation\"/>"]+      lines written `shouldContain` ["    <diverged left=\"Φ.ёж\" right=\"Φ.щука\" reason=\"the right side is no formation\"><left>Φ.ёж</left><right>Φ.щука</right></diverged>"]     it "writes a side of a join read from a meta by the meta of its line in the markup" $ do       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvDiverged 2 (ExMeta "n3", ExFormation [BiTau AtPhi (ExFormation [BiDelta (BtOne "1F")])]) (ExMeta "n4", ExFormation [BiTau AtPhi (ExFormation [BiDelta (BtOne "2E")])]) [AtPhi, AtDelta] Unnamed])-      lines written `shouldContain` ["    <diverged left=\"𝑛3·1\" right=\"𝑛4·1\" at=\".φ.Δ\" reason=\"the join names no otherwise\"/>"]+      lines written `shouldContain` ["    <diverged left=\"𝑛3·1\" right=\"𝑛4·1\" at=\".φ.Δ\" reason=\"the join names no otherwise\"><left Δ=\"1F-\"/><right Δ=\"2E-\"/></diverged>"]     it "writes where the two sides of a join differ and why no formation was fabricated of them in the markup" $ do       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvDiverged 2 (ExMeta "n5", ExFormation [BiLambda (FnSymbol 8)]) (ExMeta "n6", ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёрш"))]) [AtLambda] (Holding Lefthand AtLambda)])-      lines written `shouldContain` ["    <diverged left=\"𝜎8\" right=\"𝑛6·1\" at=\".λ\" reason=\"the left side has λ\"/>"]+      lines written `shouldContain` ["    <diverged left=\"𝜎8\" right=\"𝑛6·1\" at=\".λ\" reason=\"the left side is an atom\"><left λ=\"𝜎8\"/><right/></diverged>"]+    it "writes the void a side of a join leaves where the two sides differ in the markup" $ do+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvDiverged 2 (ExMeta "n3", ExFormation [BiVoid (AtLabel "щи")]) (ExMeta "n4", ExFormation [BiTau (AtLabel "щи") (ExDispatch ExRoot (AtLabel "ёж"))]) [AtLabel "щи"] Unnamed])+      lines written `shouldContain` ["    <diverged left=\"𝑛3·1\" right=\"𝑛4·1\" at=\".щи\" reason=\"the join names no otherwise\"><left><void attr=\"щи\"/></left><right><ref attr=\"щи\">Φ.ёж</ref></right></diverged>"]+    it "writes two sides a join could not join for a void as an element naming both and the attribute in the markup" $ do+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvUnripe 2 (ExMeta "n3", ExFormation [BiTau (AtLabel "щи") (ExFormation [])]) (ExMeta "n4", ExFormation [BiVoid (AtLabel "щи")]) Righthand (AtLabel "щи")])+      lines written `shouldContain` ["    <unripe left=\"𝑛3·1\" right=\"𝑛4·1\" at=\"щи\"/>"]     it "writes the formation a join fabricated as an element naming both sides in the markup" $ do       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvFabricated 2 (ExMeta "n3", ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) (ExMeta "n4", ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) (ExFormation [BiTau AtPhi (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) AtPhi), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) AtPhi)]), BiTau (AtLabel "к") (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) (AtLabel "к")), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) (AtLabel "к"))])])])       lines written `shouldContain` ["    <fabricated meta=\"𝑛·1·1\" left=\"𝑛3·1\" right=\"𝑛4·1\">𝑒·1·5</fabricated>"]
test/ForksSpec.hs view
@@ -96,9 +96,15 @@     it "keeps one void for an attribute both sides leave void" $ do       expected <- parseExpressionThrows "⟦ dk ↦ ∅, left🌵 ↦ ⟦ dk ↦ ∅, φ ↦ Φ.ic ⟧( dk ↦ ξ.dk ), right🌵 ↦ ⟦ φ ↦ Φ.yo, dk ↦ ∅ ⟧( dk ↦ ξ.dk ), φ ↦ ⟦ ρ ↦ ∅, λ ⤍ L_vb, on🌵 ↦ ⟦ Δ ⤍ 3E- ⟧, left🌵 ↦ ξ.ρ.left🌵.φ, right🌵 ↦ ξ.ρ.right🌵.φ ⟧ ⟧"       fork "L_vb" (Right (BtOne "3E")) "⟦ dk ↦ ∅, φ ↦ Φ.ic ⟧" "⟦ φ ↦ Φ.yo, dk ↦ ∅ ⟧" >>= (`shouldBe` Right expected)-    it "takes as its own void an attribute one side leaves void and the other binds" $ do-      expected <- parseExpressionThrows "⟦ ws ↦ ∅, left🌵 ↦ ⟦ ws ↦ ∅ ⟧( ws ↦ ξ.ws ), right🌵 ↦ ⟦ ws ↦ Φ.ug ⟧ ⟧"-      fork "L_oh" (Right (BtOne "52")) "⟦ ws ↦ ∅ ⟧" "⟦ ws ↦ Φ.ug ⟧" >>= (`shouldBe` Right expected)+    it "tells that the left side leaves void an attribute the right side binds" $+      fork "L_oh" (Right (BtOne "52")) "⟦ ws ↦ ∅ ⟧" "⟦ ws ↦ Φ.ug ⟧" >>= (`shouldBe` Left (Unripe Lefthand (AtLabel "ws")))+    it "tells that the right side leaves void an attribute the left side binds" $+      fork "L_yk" (Left 17) "⟦ φ ↦ Φ.di, ob ↦ ⟦ ⟧ ⟧" "⟦ ob ↦ ∅, φ ↦ Φ.ru( ξ.ob ) ⟧" >>= (`shouldBe` Left (Unripe Righthand (AtLabel "ob")))+    it "tells about a void of the left side before a void of the right side" $+      fork "L_ze" (Right (BtOne "6A")) "⟦ ma ↦ Φ.pi, iv ↦ ∅ ⟧" "⟦ ma ↦ ∅, iv ↦ Φ.go ⟧" >>= (`shouldBe` Left (Unripe Lefthand (AtLabel "iv")))+    it "fabricates a formation of a side leaving its ρ void and a side binding it" $ do+      expected <- parseExpressionThrows "⟦ left🌵 ↦ ⟦ ρ ↦ ∅, φ ↦ Φ.ah ⟧, right🌵 ↦ ⟦ ρ ↦ Φ.nu, φ ↦ Φ.ek ⟧, φ ↦ ⟦ ρ ↦ ∅, λ ⤍ L_sa, on🌵 ↦ ⟦ Δ ⤍ 0D- ⟧, left🌵 ↦ ξ.ρ.left🌵.φ, right🌵 ↦ ξ.ρ.right🌵.φ ⟧ ⟧"+      fork "L_sa" (Right (BtOne "0D")) "⟦ ρ ↦ ∅, φ ↦ Φ.ah ⟧" "⟦ ρ ↦ Φ.nu, φ ↦ Φ.ek ⟧" >>= (`shouldBe` Right expected)     it "skips an attribute of a side whose name ends with the 🌵 mark" $ do       expected <- parseExpressionThrows "⟦ left🌵 ↦ ⟦ left🌵 ↦ Φ.ub, rq🌵 ↦ ∅, φ ↦ Φ.ar ⟧, right🌵 ↦ ⟦ φ ↦ Φ.se ⟧, φ ↦ ⟦ ρ ↦ ∅, λ ⤍ L_hn, on🌵 ↦ ⟦ Δ ⤍ 19- ⟧, left🌵 ↦ ξ.ρ.left🌵.φ, right🌵 ↦ ξ.ρ.right🌵.φ ⟧ ⟧"       fork "L_hn" (Right (BtOne "19")) "⟦ left🌵 ↦ Φ.ub, rq🌵 ↦ ∅, φ ↦ Φ.ar ⟧" "⟦ φ ↦ Φ.se ⟧" >>= (`shouldBe` Right expected)@@ -129,6 +135,15 @@     it "hands the voids of a copy of the function to a side that does not bind its attribute" $ do       expected <- parseExpressionThrows "⟦ left🌵 ↦ ⟦ ke ↦ ⟦ ev ↦ ∅, jo ↦ ∅ ⟧ ⟧, right🌵 ↦ ⟦ φ ↦ Φ.ty ⟧, ke ↦ ⟦ ρ ↦ ∅, λ ⤍ L_pu, ev ↦ ∅, jo ↦ ∅, on🌵 ↦ ⟦ Δ ⤍ 5C- ⟧, left🌵 ↦ ξ.ρ.left🌵.ke( ev ↦ ξ.ev, jo ↦ ξ.jo ), right🌵 ↦ ξ.ρ.right🌵.ke( ev ↦ ξ.ev, jo ↦ ξ.jo ) ⟧, φ ↦ ⟦ ρ ↦ ∅, λ ⤍ L_pu, on🌵 ↦ ⟦ Δ ⤍ 5C- ⟧, left🌵 ↦ ξ.ρ.left🌵.φ, right🌵 ↦ ξ.ρ.right🌵.φ ⟧ ⟧"       fork "L_pu" (Right (BtOne "5C")) "⟦ ke ↦ ⟦ ev ↦ ∅, jo ↦ ∅ ⟧ ⟧" "⟦ φ ↦ Φ.ty ⟧" >>= (`shouldBe` Right expected)+    it "keeps an attribute both sides bind to the same attribute of the fabricated formation" $ do+      expected <- parseExpressionThrows "⟦ left🌵 ↦ ⟦ wa ↦ ⟦ ov ↦ ∅, φ ↦ ξ.ov ⟧, ky ↦ ξ.wa ⟧, right🌵 ↦ ⟦ wa ↦ ⟦ ov ↦ ∅, ip ↦ ∅, φ ↦ ξ.ip ⟧, ky ↦ ξ.wa ⟧, wa ↦ ⟦ ρ ↦ ∅, λ ⤍ L_ko, ov ↦ ∅, ip ↦ ∅, on🌵 ↦ ⟦ λ ⤍ 𝜎14 ⟧, left🌵 ↦ ξ.ρ.left🌵.wa( ov ↦ ξ.ov ), right🌵 ↦ ξ.ρ.right🌵.wa( ov ↦ ξ.ov, ip ↦ ξ.ip ) ⟧, ky ↦ ξ.wa ⟧"+      fork "L_ko" (Left 14) "⟦ wa ↦ ⟦ ov ↦ ∅, φ ↦ ξ.ov ⟧, ky ↦ ξ.wa ⟧" "⟦ wa ↦ ⟦ ov ↦ ∅, ip ↦ ∅, φ ↦ ξ.ip ⟧, ky ↦ ξ.wa ⟧" >>= (`shouldBe` Right expected)+    it "asks the copies of both sides for an attribute both bind to an attribute the fabricated formation lacks" $ do+      expected <- parseExpressionThrows "⟦ left🌵 ↦ ⟦ ky ↦ ξ.ub ⟧, right🌵 ↦ ⟦ ky ↦ ξ.ub ⟧, ky ↦ ⟦ ρ ↦ ∅, λ ⤍ L_ex, on🌵 ↦ ⟦ Δ ⤍ 2A- ⟧, left🌵 ↦ ξ.ρ.left🌵.ky, right🌵 ↦ ξ.ρ.right🌵.ky ⟧ ⟧"+      fork "L_ex" (Right (BtOne "2A")) "⟦ ky ↦ ξ.ub ⟧" "⟦ ky ↦ ξ.ub ⟧" >>= (`shouldBe` Right expected)+    it "asks the copies of both sides for an attribute they bind to two other attributes" $ do+      expected <- parseExpressionThrows "⟦ left🌵 ↦ ⟦ ma ↦ Φ.ro, ni ↦ Φ.su, ky ↦ ξ.ma ⟧, right🌵 ↦ ⟦ ma ↦ Φ.ro, ni ↦ Φ.su, ky ↦ ξ.ni ⟧, ma ↦ ⟦ ρ ↦ ∅, λ ⤍ L_ud, on🌵 ↦ ⟦ Δ ⤍ 3B- ⟧, left🌵 ↦ ξ.ρ.left🌵.ma, right🌵 ↦ ξ.ρ.right🌵.ma ⟧, ni ↦ ⟦ ρ ↦ ∅, λ ⤍ L_ud, on🌵 ↦ ⟦ Δ ⤍ 3B- ⟧, left🌵 ↦ ξ.ρ.left🌵.ni, right🌵 ↦ ξ.ρ.right🌵.ni ⟧, ky ↦ ⟦ ρ ↦ ∅, λ ⤍ L_ud, on🌵 ↦ ⟦ Δ ⤍ 3B- ⟧, left🌵 ↦ ξ.ρ.left🌵.ky, right🌵 ↦ ξ.ρ.right🌵.ky ⟧ ⟧"+      fork "L_ud" (Right (BtOne "3B")) "⟦ ma ↦ Φ.ro, ni ↦ Φ.su, ky ↦ ξ.ma ⟧" "⟦ ma ↦ Φ.ro, ni ↦ Φ.su, ky ↦ ξ.ni ⟧" >>= (`shouldBe` Right expected)     it "tells that the left side has a datum" $       fork "L_ax" (Right (BtOne "11")) "⟦ Δ ⤍ 4F- ⟧" "⟦ φ ↦ Φ.bu ⟧" >>= (`shouldBe` Left (Holding Lefthand AtDelta))     it "tells that the left side has a λ function" $
test/LambdasSpec.hs view
@@ -13,7 +13,7 @@ import Data.Text qualified as T import Fixtures (withLambdasOf) import Functions (buildTerm)-import Lambdas (Ending (..), Lambda (..), Lambdas, Line (..), Meta (..), cast, emptyLambdas, matched, minted, readLambdas, rewritten, stayed, symbolized, taken)+import Lambdas (Ending (..), Lambda (..), Lambdas, Line (..), Meta (..), cast, emptyLambdas, matched, minted, readLambdas, rewritten, stayed, symbolized, taken, thrown) import Parser (parseExpressionThrows) import Rule (RuleContext (..), normal) import System.Mem.StableName (makeStableName)@@ -501,7 +501,9 @@       , ("an 'unfold' block, which is gone", "- λ: L_fork\n  morph:\n    𝑛1: $.a\n  unfold:\n    𝑛2: 𝑛1\n  𝑛: 𝑛2\n", "The key 'unfold' of λ function 'L_fork' is none of the keys an entry reads")       , ("an 'unbox' block, which is gone", "- λ: L_fork\n  morph:\n    𝑛1: $.a\n  unbox:\n    𝑛2: 𝑛1\n  𝑛: 𝑛2\n", "The key 'unbox' of λ function 'L_fork' is none of the keys an entry reads")       , ("an 'upcast' block, which is gone", "- λ: L_fork\n  morph:\n    𝑛1: $.a\n    𝑛2: $.b\n  upcast:\n    𝑛3: 𝑛1\n    𝑛4: 𝑛2\n  𝑛: 𝑛3\n", "The key 'upcast' of λ function 'L_fork' is none of the keys an entry reads")-      , ("a 'terminators' key, which is gone", "- λ: L_fork\n  morph:\n    𝑛1: $.a\n  terminators: [L_throw]\n  𝑛: 𝑛1\n", "The key 'terminators' of λ function 'L_fork' is none of the keys an entry reads")+      , ("a terminator another entry answers", "- λ: L_fork\n  morph:\n    𝑛1: $.a\n  terminators: [L_throw]\n  𝑛: 𝑛1\n- λ: L_th.*\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n", "the terminator 'L_throw' of the key 'L_fork' is answered by the key 'L_th.*'")+      , ("a terminator its own entry answers", "- λ: L_.*\n  morph:\n    𝑛1: $.a\n  terminators: [L_throw]\n  𝑛: 𝑛1\n", "the terminator 'L_throw' of the key 'L_.*' is answered by the key 'L_.*'")+      , ("a 'terminators' key holding no list", "- λ: L_fork\n  morph:\n    𝑛1: $.a\n  terminators: L_throw\n  𝑛: 𝑛1\n", "terminators")       , ("a 'lenient' key, which is gone", "- λ: L_fork\n  morph:\n    𝑛1: $.a\n  lenient: []\n  𝑛: 𝑛1\n", "The key 'lenient' of λ function 'L_fork' is none of the keys an entry reads")       , ("a misspelled 'dataize' block", "- λ: L_pair\n  datize:\n    𝛿1: $.ρ\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n", "The key 'datize' of λ function 'L_pair' is none of the keys an entry reads")       , ("a 'defer' key saying a flag instead of holding lines", "- λ: L_hold\n  morph:\n    𝑛1: $.a\n  defer: true\n  𝑛: 𝑛1\n", "defer: parsing")@@ -511,6 +513,23 @@             lambdasOf text `shouldThrow` (\err -> reason `isInfixOf` show (err :: SomeException))       ) +  describe "thrown" $ do+    it "tells a formation holding a terminator raises" $ do+      term <- parseExpressionThrows "⟦ notiz ↦ \"schlecht\", λ ⤍ L_wurf ⟧"+      thrown ["L_wurf"] term `shouldBe` True++    it "tells an application of a formation holding a terminator raises" $ do+      term <- parseExpressionThrows "⟦ notiz ↦ ∅, λ ⤍ L_wurf ⟧( notiz ↦ \"schlecht\" )"+      thrown ["L_wurf"] term `shouldBe` True++    it "tells a formation holding another λ function does not raise" $ do+      term <- parseExpressionThrows "⟦ notiz ↦ \"schlecht\", λ ⤍ L_fang ⟧"+      thrown ["L_wurf"] term `shouldBe` False++    it "tells a dispatch off a formation holding a terminator does not raise" $ do+      term <- parseExpressionThrows "⟦ λ ⤍ L_wurf ⟧.notiz"+      thrown ["L_wurf"] term `shouldBe` False+   describe "stayed" $ do     it "drops the ρ a dispatch is applied to" $ do       term <- parseExpressionThrows "Φ.bytes( ρ ↦ ⟦ x ↦ ∅ ⟧ )"@@ -572,14 +591,28 @@       cast bare shape `shouldBe` Just made      forM_+      [ ("a decorator whose φ is a fork" :: String, "⟦ kq ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎5 ⟧ ⟧, right🌵 ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎6 ⟧ ⟧ ⟧ ⟧", "⟦ kq ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧")+      , ("a decorator two steps down to a fork", "⟦ φ ↦ ⟦ φ ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧ ⟧, if ↦ ξ.ty ⟧, and ↦ ∅ ⟧", "⟦ φ ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧, if ↦ ξ.ty ⟧, and ↦ ∅ ⟧")+      , ("a decorator whose φ chain ends in no symbol", "⟦ φ ↦ Φ.kq ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧")+      , ("a decorator whose φ chain ends in a datum", "⟦ φ ↦ ⟦ Δ ⤍ 1F- ⟧ ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧")+      , ("a decorator whose φ chain ends in a symbol beside other bindings", "⟦ φ ↦ ⟦ λ ⤍ 𝜎6, zv ↦ ∅ ⟧ ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧")+      , ("a decorator holding a symbol off its φ chain", "⟦ φ ↦ ⟦ λ ⤍ 𝜎6 ⟧, zv ↦ ⟦ λ ⤍ 𝜎7 ⟧ ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧, zv ↦ ⟦ λ ⤍ 𝜎7 ⟧ ⟧")+      , ("a decorator holding the symbol of its φ chain once more off it", "⟦ φ ↦ ⟦ λ ⤍ 𝜎6 ⟧, zv ↦ ⟦ λ ⤍ 𝜎6 ⟧ ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧, zv ↦ ⟦ λ ⤍ 𝜎6 ⟧ ⟧")+      , ("a decorator whose φ chain runs through an application", "⟦ φ ↦ Φ.kq( φ ↦ ⟦ λ ⤍ 𝜎6 ⟧ ) ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧")+      ]+      ( \(desc, into, expected) ->+          it ("casts a bare symbol into a copy of " ++ desc) $ do+            bare <- parseExpressionThrows "⟦ λ ⤍ 𝜎3 ⟧"+            shape <- parseExpressionThrows into+            made <- parseExpressionThrows expected+            cast bare shape `shouldBe` Just made+      )++    forM_       [ ("another bare symbol" :: String, "⟦ λ ⤍ 𝜎3 ⟧", "⟦ λ ⤍ 𝜎4 ⟧")-      , ("a term whose φ chain ends in no symbol", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ Φ.kq ⟧")-      , ("a term whose φ chain ends in a datum", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ ⟦ Δ ⤍ 1F- ⟧ ⟧")+      , ("a formation binding no φ", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎5 ⟧ ⟧ ⟧")+      , ("a term that is no formation", "⟦ λ ⤍ 𝜎3 ⟧", "Φ.kq( φ ↦ ⟦ λ ⤍ 𝜎6 ⟧ )")       , ("a term whose φ is void", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ ∅, zv ↦ ⟦ λ ⤍ 𝜎6 ⟧ ⟧")-      , ("a term whose φ chain ends in a symbol beside other bindings", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎6, zv ↦ ∅ ⟧ ⟧")-      , ("a term holding a symbol off its φ chain", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎6 ⟧, zv ↦ ⟦ λ ⤍ 𝜎7 ⟧ ⟧")-      , ("a term holding the symbol of its φ chain once more off it", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎6 ⟧, zv ↦ ⟦ λ ⤍ 𝜎6 ⟧ ⟧")-      , ("a term whose φ chain runs through an application", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ Φ.kq( φ ↦ ⟦ λ ⤍ 𝜎6 ⟧ ) ⟧")       , ("a decorator from a term that is no bare symbol", "⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎6 ⟧ ⟧")       ]       ( \(desc, from, into) ->
test/ParserSpec.hs view
@@ -103,22 +103,6 @@             )         )       ,-        ( "!e1(x(^,@) -> [[w -> !e2]])"-        , Just-            ( ExApplication-                (ExMeta "e1")-                ( ArTau-                    (AtLabel "x")-                    ( ExFormation-                        [ BiVoid AtRho-                        , BiVoid AtPhi-                        , BiTau (AtLabel "w") (ExMeta "e2")-                        ]-                    )-                )-            )-        )-      ,         ( "[[x -> y.z, w -> ^, u -> @, p -> !t1, q -> !e1]]"         , Just             ( ExFormation@@ -205,9 +189,6 @@     forM_       [ "[[x -> $, y -> ?]]"       , "[[x() -> [[]] ]]"-      , "Q.x(y() -> [[]])"-      , "Q.x(y(q) -> [[w -> !e]])"-      , "Q.x(~1(^,@) -> [[]])"       , "Q.x.^.@.!t1"       , "[[x -> y.z]]"       , "[[x -> ^, y -> @, z -> !t]]"@@ -740,13 +721,11 @@       , ("⟦ x(y) ↦ 42:a:b ⟧", "⟦ x ↦ ⟦ y ↦ ∅, b ↦ ⟦ a ↦ 42 ⟧ ⟧ ⟧")       , ("⟦ x(y, z) ↦ ∅:a ⟧", "⟦ x ↦ ⟦ y ↦ ∅, z ↦ ∅, a ↦ ∅ ⟧ ⟧")       , ("[[ x(y) -> Plus:L ]]", "⟦ x ↦ ⟦ y ↦ ∅, λ ⤍ Plus ⟧ ⟧")-      , ("Q.x(y(z) ↦ FF-:Δ)", "Q.x(y ↦ ⟦ z ↦ ∅, Δ ⤍ FF- ⟧)")       , ("⟦ x(y) ↦ ⟦ z ↦ ξ ⟧:a ⟧", "⟦ x ↦ ⟦ y ↦ ∅, a ↦ ⟦ z ↦ ξ ⟧ ⟧ ⟧")       , ("⟦ x(y) ↦ ⟦ ⟧ : a ⟧", "⟦ x ↦ ⟦ y ↦ ∅, a ↦ ⟦ ⟧ ⟧ ⟧")       , ("⟦ x(y) ↦ ⟦ z ↦ ξ ⟧.z:a ⟧", "⟦ x ↦ ⟦ y ↦ ∅, a ↦ ⟦ z ↦ ξ ⟧.z ⟧ ⟧")       , ("⟦ x(y) ↦ ⟦ z ↦ ∅ ⟧(z ↦ Φ):a ⟧", "⟦ x ↦ ⟦ y ↦ ∅, a ↦ ⟦ z ↦ ∅ ⟧(z ↦ Φ) ⟧ ⟧")       , ("⟦ x(y) ↦ ⟦ z(w) ↦ ⟦ ⟧:b ⟧:a ⟧", "⟦ x ↦ ⟦ y ↦ ∅, a ↦ ⟦ z ↦ ⟦ w ↦ ∅, b ↦ ⟦ ⟧ ⟧ ⟧ ⟧ ⟧")-      , ("Q.x(y(z) ↦ ⟦ w ↦ ξ ⟧:a)", "Q.x(y ↦ ⟦ z ↦ ∅, a ↦ ⟦ w ↦ ξ ⟧ ⟧)")       ]       ( \(sweet, plain) ->           it sweet $ do@@ -767,7 +746,15 @@       parseExpression       ( map           (\ipt -> (ipt, Nothing :: Maybe Expression))-          ["⟦ x(y) ↦ 42 ⟧", "⟦ x(y) ↦ 42:a.b ⟧", "⟦ x(y) ↦ 42:a(z) ⟧", "⟦ x(y) ↦ ξ.a ⟧", "Q.x(y(z) ↦ FF-:Δ.b)", "⟦ x(y) ↦ ⟦ ⟧.a ⟧", "⟦ x(y) ↦ ⟦ ⟧(a ↦ ξ) ⟧", "⟦ x(y) ↦ ⟦ ⟧:y ⟧"]+          ["⟦ x(y) ↦ 42 ⟧", "⟦ x(y) ↦ 42:a.b ⟧", "⟦ x(y) ↦ 42:a(z) ⟧", "⟦ x(y) ↦ ξ.a ⟧", "⟦ x(y) ↦ ⟦ ⟧.a ⟧", "⟦ x(y) ↦ ⟦ ⟧(a ↦ ξ) ⟧", "⟦ x(y) ↦ ⟦ ⟧:y ⟧"]+      )++  describe "rejects inline voids in an argument of an application (#2258)" $+    test+      parseExpression+      ( map+          (\ipt -> (ipt, Nothing :: Maybe Expression))+          ["Φ.bool(v(x) ↦ ⟦ λ ⤍ L_fork ⟧)", "Q.x(y(z) ↦ FF-:Δ)", "Q.x(y(z) ↦ ⟦ w ↦ ξ ⟧:a)", "Q.x(α0(z) ↦ ⟦ ⟧)", "Q.x(a ↦ ξ, y(z, w) ↦ ⟦ ⟧)", "!e1(x(^,@) -> [[w -> !e2]])", "Q.x(y() -> [[]])", "Q.x(y(q) -> [[w -> !e]])", "Q.x(~1(^,@) -> [[]])"]       )    describe "rejects a mix of ASCII and Unicode symbols under monoform" $
test/PrinterSpec.hs view
@@ -454,6 +454,8 @@       , ("⟦ x ↦ ξ.a, y ↦ ∅ ⟧", SWEET, UNICODE, "⟦ x ↦ a, y ↦ ∅ ⟧")       , ("⟦ x ↦ ⟦ a ↦ ∅, 𝜏1 ↦ ∅ ⟧ ⟧", SWEET, UNICODE, "⟦ x(a) ↦ ∅:𝜏1 ⟧")       , ("⟦ x ↦ ⟦ 𝜏1 ↦ ∅, a ↦ ∅ ⟧ ⟧", SWEET, UNICODE, "⟦ 𝜏1 ↦ ∅, a ↦ ∅ ⟧:x")+      , ("Φ.bool(v ↦ ⟦ x ↦ ∅, λ ⤍ L_fork ⟧)", SWEET, UNICODE, "Φ.bool( v ↦ ⟦ x ↦ ∅, λ ⤍ L_fork ⟧ )")+      , ("Φ.bool(α0 ↦ ⟦ x ↦ ∅, y ↦ ξ ⟧)", SWEET, UNICODE, "Φ.bool( ⟦ x ↦ ∅, y ↦ ξ ⟧ )")       , ("⟦ x ↦ ξ.a ⟧", SALTY, UNICODE, "⟦ x ↦ ξ.a ⟧")       , ("⟦ Δ ⤍ FF-AA ⟧", SALTY, ASCII, "[[ D> FF-AA ]]")       ]