phino 0.0.118 → 0.0.119

raw patch · 16 files changed

+454/−58 lines, 16 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +87/−33
• phino.cabal +1/−1
• resources/normalize/alpha.yaml +8/−3
• src/CLI/Parsers.hs +7/−0
• src/CLI/Runners.hs +4/−2
• src/CLI/Types.hs +1/−0
• src/CST.hs +3/−1
• src/Dataize.hs +163/−6
• src/Functions.hs +4/−1
• src/Rule.hs +1/−0
• src/XMIR.hs +7/−2
• test/CLISpec.hs +59/−1
• test/CSTSpec.hs +2/−0
• test/DataizeSpec.hs +92/−6
• test/PrinterSpec.hs +14/−0
• test/XMIRSpec.hs +1/−2

@@ -34,7 +34,7 @@  ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.115+cabal install --overwrite-policy=always phino-0.0.118 phino --version ``` @@ -404,6 +404,60 @@ `--sequence`, `--headers`, `--steps-dir`, `--evaluations`, `--partial`, `--max-steps`, `--shuffle`/`--seed`, `--output`, `--focus` and the rest. +### Deep morphing++𝕄 stops at the first formation it reaches and hands its bindings back as they+were written, since firing a bare λ is dataization's job, and `dataize`+follows the one path dataization demands and ends in bytes. What a program+holds but nothing demands — the argument of an atom the registry does not+serve, for one — is therefore reduced by neither. The `--deep` flag enters it:++```bash+$ cat gap.phi+⟦+  bytes(data) ↦ ⟦ φ ↦ ξ.data ⟧,+  number(as-bytes) ↦ ⟦ φ ↦ ξ.as-bytes, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧,+  bar(x) ↦ ⟦ λ ⤍ L_bar ⟧,+  demo ↦ ⟦ foo ↦ ⟦ n ↦ 3, φ ↦ Φ.bar( ξ.n.times( 5 ).times( 7 ) ) ⟧ ⟧+⟧+$ phino morph --atoms=atoms.json --inside='Q.demo.foo' \+    --sweet --hide-rho gap.phi+⟦ n ↦ 3, φ ↦ Φ.bar( n.times( 5 ).times( 7 ) ) ⟧+$ phino morph --deep --atoms=atoms.json --inside='Q.demo.foo' \+    --sweet --hide-rho gap.phi+⟦ n ↦ 3, φ ↦ Φ.bar( 105 ) ⟧+```++Every binding of the formation is entered, recursively. 𝕄 is asked about the+term standing there and, where it lands on a saturated formation whose λ the+registry serves, that λ is fired and 𝕄 is asked about the answer again. A term+on whose way an atom fired is replaced by the answer of the last firing, which+is the 𝜑-program the atom wrote rather than the normal form of it, so `105`+stands where the arithmetic stood. A term no atom touched stays exactly as it+was written and only its own parts are walked, so `Φ.bar` keeps its name and+what comes back is still the same program, reduced as far as the registry+allows. The step joins the chain under the name `deep`, so `--sequence` shows+it, and `--max-steps` bounds the walk.++Two things are left alone. A λ the registry does not serve is not fired at+all, so `--deep` stays as total as 𝕄 itself and needs no `--partial`; an atom+that gets stuck deeper on a spine still fails the run, and `--partial` parks+it, leaving that term as it was written. A formation still holding a void+binding is not fired either: the void is an argument the program has not given+yet, so `times(x) ↦ ⟦ λ ⤍ L_number_times ⟧` is a method waiting to be applied,+not an application waiting to be computed. Walking the whole program therefore+folds what it can and leaves the object model as it was declared:++```bash+$ phino morph --deep --atoms=atoms.json --sweet --hide-rho gap.phi+⟦+  bytes(data) ↦ ⟦ φ ↦ data ⟧,+  number(as-bytes) ↦ ⟦ φ ↦ as-bytes, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧,+  bar(x) ↦ ⟦ λ ⤍ L_bar ⟧,+  demo ↦ ⟦ foo ↦ ⟦ n ↦ 3, φ ↦ Φ.bar( 105 ) ⟧ ⟧+⟧+```+ ## Rewrite  You can rewrite this expression with the help of [rules](#rule-structure)@@ -788,55 +842,55 @@ === parse/phi ===   warmup:     3 iterations   batches:    10 x 1-  total:      1781621.932 μs-  avg:        178162.193 μs-  min:        163679.993 μs-  max:        209804.570 μs-  std dev:    17409.000 μs+  total:      1598588.273 μs+  avg:        159858.827 μs+  min:        147759.554 μs+  max:        193999.679 μs+  std dev:    17143.300 μs === parse/xmir ===   warmup:     3 iterations   batches:    10 x 1-  total:      7611171.011 μs-  avg:        761117.101 μs-  min:        679176.096 μs-  max:        899930.605 μs-  std dev:    69464.089 μs+  total:      7813131.215 μs+  avg:        781313.122 μs+  min:        724999.135 μs+  max:        842487.724 μs+  std dev:    32948.399 μs === rewrite/normalize ===   warmup:     3 iterations   batches:    10 x 1-  total:      811837.328 μs-  avg:        81183.733 μs-  min:        67331.161 μs-  max:        92232.373 μs-  std dev:    8117.233 μs+  total:      1071335.155 μs+  avg:        107133.516 μs+  min:        82715.009 μs+  max:        127072.342 μs+  std dev:    15148.984 μs === print/sweet/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      4199718.146 μs-  avg:        419971.815 μs-  min:        396063.240 μs-  max:        442595.822 μs-  std dev:    16504.492 μs+  total:      4764374.575 μs+  avg:        476437.457 μs+  min:        443528.234 μs+  max:        508780.337 μs+  std dev:    21790.459 μs === print/sweet/flat ===   warmup:     3 iterations   batches:    10 x 1-  total:      4060839.345 μs-  avg:        406083.934 μs-  min:        387257.807 μs-  max:        417907.724 μs-  std dev:    8861.891 μs+  total:      4829704.670 μs+  avg:        482970.467 μs+  min:        444530.419 μs+  max:        514344.452 μs+  std dev:    23249.943 μs === print/salty/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      14257603.693 μs-  avg:        1425760.369 μs-  min:        1405945.748 μs-  max:        1449825.539 μs-  std dev:    11882.320 μs+  total:      14789056.654 μs+  avg:        1478905.665 μs+  min:        1426640.434 μs+  max:        1589233.894 μs+  std dev:    46147.565 μs ```  The results were calculated in [this GHA job][benchmark-gha]-on 2026-09-07 at 19:51,+on 2026-09-08 at 20:28, on Linux with 4 CPUs.  <!-- benchmark_end -->@@ -885,4 +939,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/34156988456+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/34274639466

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.118+version: 0.0.119 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>

@@ -5,6 +5,11 @@ pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(α𝑖1 ↦ 𝑒1) result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒1) when:-  eq:-    - 𝑖1-    - domain: 𝐵1+  and:+    - eq:+        - 𝑖1+        - domain: 𝐵1+    - not:+        eq:+          - 𝜏1+          - ρ

@@ -206,6 +206,12 @@ optPartial :: Parser Bool optPartial = switch (long "partial" <> help "Partial evaluation: compute what the known inputs decide and, instead of failing on an atom that cannot fire (its λ function is not in the --atoms registry), leave it in place and print the residual 𝜑-program") +-- 𝕄 stops at the first formation it reaches and hands its bindings back as+-- they were written, so what a program holds but nothing demands is never+-- reduced. This walks into them (see 'deepened').+optDeep :: Parser Bool+optDeep = switch (long "deep" <> help "Don't stop at the first formation: enter its bindings too, recursively, firing every λ function the --atoms registry serves and standing its answer in the place of what it computed, while everything else stays as it was written")+ -- Which λ functions this run may fire. phino implements none of them itself -- (see 'Atoms'), so without this option every atom a program names gets stuck. optAtoms :: Parser (Maybe FilePath)@@ -376,6 +382,7 @@             <*> optSeed             <*> switch (long "quiet" <> help "Don't print the result of morphing")             <*> optPartial+            <*> optDeep             <*> optCompress             <*> optMaxDepth             <*> optMaxCycles

@@ -165,7 +165,9 @@       _evaluations       printCtx       ( \record -> do-          let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial atoms buildTerm save record+          -- The deep walk belongs to 𝕄 alone (the '--deep' of 'morph'), since 𝔻+          -- reduces what dataization demands and ends in bytes, so it is off here.+          let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial False atoms buildTerm save record           (universe, aiming) <- aimed _inside expr ctx           dataize universe aiming       )@@ -245,7 +247,7 @@       _evaluations       printCtx       ( \record -> do-          let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial atoms buildTerm save record+          let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial _deep atoms buildTerm save record           (universe, aiming) <- aimed _inside expr ctx           morph universe aiming       )

@@ -140,6 +140,7 @@   , _seed :: Int   , _quiet :: Bool   , _partial :: Bool+  , _deep :: Bool   , _compress :: Bool   , _maxDepth :: Int   , _maxCycles :: Int

@@ -11,7 +11,7 @@ module CST where  import AST-import Bytes (NonFinite, btsToNonFinite, btsToNum, btsToStr)+import Bytes (NonFinite, btsSize, btsToNonFinite, btsToNum, btsToStr) import Data.Maybe (isJust) import qualified Data.Text as T import qualified Yaml as Y@@ -270,6 +270,8 @@ -- pattern, such as a NaN carrying a payload, is kept in its byte form so that -- no bit of it is lost. sweetNumber :: Bytes -> Bool+sweetNumber bts+  | btsSize bts /= 8 = False sweetNumber bts = case btsToNum bts of   Right dbl | isNaN dbl || isInfinite dbl -> isJust (btsToNonFinite bts)   _ -> True

@@ -14,12 +14,13 @@  import AST import Atoms (Registry, fireAtom, registeredAtom)-import Builder (buildBytesThrows, buildExpressionThrows)+import Builder (buildBytesThrows, buildExpressionThrows, contextualize) import Control.Exception (Exception, catch, throwIO, try) import Control.Monad (foldM, when) import Data.List (find, partition) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE+import Data.Maybe (fromMaybe) import qualified Data.Text as T import Deps (BuildTermFunc, BuildTermMethodS, Evaluation (..), SaveEvalFunc, SaveStepFunc, State, Term (..)) import Locator (locatedExpression, withLocatedExpression)@@ -74,6 +75,7 @@   , _depthSensitive :: Bool   , _shuffle :: Bool   , _partial :: Bool+  , _deep :: Bool   , _atoms :: Registry   , _buildTerm :: BuildTermFunc   , _saveStep :: SaveStepFunc@@ -134,6 +136,23 @@     isLambda (BiLambda _) = True     isLambda _ = False +-- The same as 'lambda', but only for a formation that is saturated: one with no+-- void binding left in it. A void is an argument the program has not given yet,+-- so such a formation is a method waiting to be applied rather than an+-- application waiting to be computed, and firing it would hand the atom a ∅+-- where it expects a value. 𝔻 needs no such guard, since it fires only what+-- dataization demands and nothing demands a method; the deep walk meets every+-- one a program declares — the method table of the object model above all — so+-- it asks first (see 'deepened').+saturated :: [Binding] -> Maybe (T.Text, Expression)+saturated bds = case lambda bds of+  Just (func, ExFormation rest) | all filled rest -> Just (func, ExFormation rest)+  _ -> Nothing+  where+    filled :: Binding -> Bool+    filled (BiVoid _) = False+    filled _ = True+ -- Run one frame of the 𝕄/𝔻 spine, attaching its derivation to a stuck atom -- escaping it. 'Stuck' is raised deep inside an atom, which knows nothing about -- the chain, so the innermost spine frame it reaches is the one to record where@@ -242,19 +261,157 @@ -- with the terminator ⊥ ('dead', 'xi', 'mg', 'mad', 'maad') rather than failing. -- Only the atoms 'ml' fires can still get stuck, and '_partial' parks them just -- as it does under 𝔻: the answer is then the residual subterm the spine had--- reached, taken from '_locator' of its working expression.+-- reached, taken from '_locator' of its working expression. Stopping at the+-- first formation leaves everything that formation holds as it was written,+-- which is what '_deep' walks into before the answer is handed back (see+-- 'deepened'). morph :: Expression -> DataizeContext -> IO (Expression, [Rewritten]) morph universe ctx@DataizeContext{..} = do   expr <- locatedExpression _locator universe-  -- Morphing starts from the empty state; the final state is not yet-  -- consumed by any caller, so it is discarded here.   result <- try (morph' (expr, (universe, Nothing) :| []) universe emptyState ctx)   case result of-    Right ((morphed, seq), _state) -> pure (morphed, reverse (NE.toList seq))+    Right ((morphed, seq), state) -> walked morphed seq state     Left (StuckAt _ seq) | _partial -> do       residue <- locatedExpression _locator (fst (NE.head seq))-      pure (residue, reverse (NE.toList seq))+      walked residue seq emptyState     Left failure -> throwIO (failure :: DataizeException)+  where+    -- The answer 𝕄 reached, walked by '_deep' before it is handed back (see+    -- 'deepened'), and the chain that led to both. The walk joins the chain as+    -- one step named 'deep', so '--sequence' ends on the term the command+    -- prints. Morphing starts from the empty state and the state the walk ends+    -- on goes the way 𝕄's own goes: no caller consumes it yet.+    walked :: Expression -> NonEmpty Rewritten -> State -> IO (Expression, [Rewritten])+    walked morphed seq state+      | not _deep = pure (morphed, reverse (NE.toList seq))+      | otherwise = do+          (deep, _) <- deepened morphed universe state ctx+          seq' <- leadsTo seq "deep" deep ctx+          pure (deep, reverse (NE.toList seq'))++-- Walk what 𝕄 answered with, entering everything it left as it was written —+-- the mechanism behind '--deep' ('_deep'). 𝕄 navigates a term to the first+-- formation it reaches and 'mf' hands that formation back with its bindings+-- untouched, since firing a bare λ is 𝔻's business; 𝔻 in turn follows the one+-- path dataization demands and ends in bytes. A part of a program that nothing+-- demands — the argument of an atom that cannot fire, for one — is therefore+-- reduced by neither, and the object structure is lost to the one that does+-- reduce it (#1124). This walk demands nothing either. It asks 𝕄 about every+-- sub-expression and, where 𝕄 lands on a formation whose λ the registry+-- serves, fires it and asks 𝕄 about the answer again (see 'fired'). A+-- sub-expression on whose way an atom fired is replaced by the answer of the+-- last firing; where none fired it stays as it was written and only its own+-- parts are walked, so the calls the registry does not serve keep their names+-- and what comes back is still the same program, reduced as far as the+-- registry allows. Every entry is charged to the '--max-steps' budget, which+-- is what bounds the walk.+deepened :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State)+deepened expr univ = go ExXi expr+  where+    -- A term as it was written, together with what its free ξ stands for: the+    -- formation the walk entered it from, without the binding it came from,+    -- exactly the context the 'dot' rule hands a dispatched body. At the top+    -- there is no such formation, so ξ stands for itself and contextualization+    -- leaves the term alone.+    go :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State)+    go context term state' caller = do+      ctx' <- deeper caller+      answer <- fired (contextualize term context) univ state' ctx'+      maybe (parts context term state' ctx') pure answer+    -- The parts of a term nothing fired on, walked one by one and put back+    -- where they were, so the term keeps the shape it was written in.+    parts :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State)+    parts _ (ExFormation bds) state' caller = do+      (entered, state'') <- bindings bds bds state' caller+      pure (ExFormation entered, state'')+    parts context (ExDispatch target attr) state' caller = do+      (entered, state'') <- go context target state' caller+      pure (ExDispatch entered attr, state'')+    parts context (ExApplication target arg) state' caller = do+      (entered, state'') <- go context target state' caller+      (applied, state''') <- argument context arg state'' caller+      pure (ExApplication entered applied, state''')+    parts _ term state' _ = pure (term, state')+    -- Walk the bindings of a formation left to right, threading the state+    -- through them. Only what the formation itself holds is entered: ρ names+    -- the object around it rather than one inside it, and a void, Δ or λ+    -- binding carries no term to walk at all.+    bindings :: [Binding] -> [Binding] -> State -> DataizeContext -> IO ([Binding], State)+    bindings _ [] state' _ = pure ([], state')+    bindings whole (BiTau attr body : rest) state' caller+      | attr /= AtRho = do+          (entered, state'') <- go (scope attr whole) body state' caller+          (others, state''') <- bindings whole rest state'' caller+          pure (BiTau attr entered : others, state''')+    bindings whole (bd : rest) state' caller = do+      (others, state'') <- bindings whole rest state' caller+      pure (bd : others, state'')+    -- The context a binding's body is entered in: the formation without that+    -- binding, the very context 'dot' contextualizes a dispatched body in, so+    -- a body reaching back at itself through ξ collapses instead of looping.+    scope :: Attribute -> [Binding] -> Expression+    scope attr bds = ExFormation (filter (not . named) bds)+      where+        named :: Binding -> Bool+        named (BiTau attr' _) = attr' == attr+        named _ = False+    -- Both sides of an application stand in the same context: the term it+    -- applies is walked by the caller and the argument it binds is walked here.+    argument :: Expression -> Argument -> State -> DataizeContext -> IO (Argument, State)+    argument context (ArTau attr arg) state' caller = do+      (entered, state'') <- go context arg state' caller+      pure (ArTau attr entered, state'')+    argument context (ArAlpha alpha arg) state' caller = do+      (entered, state'') <- go context arg state' caller+      pure (ArAlpha alpha entered, state'')++-- Ask 𝕄 about a term and fire the λ of the formation it reaches, as long as+-- the registry serves it, asking 𝕄 about every answer again: what comes back+-- is the answer of the last firing, or nothing at all where no atom fired. This+-- is the firing 'ml' makes without the dispatch that makes 'ml' make it — the+-- one 𝕄 leaves to 𝔻 — except in what it hands back: the atom's raw answer, not+-- the normal form 𝔼 makes of it, since the deep walk stands that answer back+-- into the program, where a normal form would spell the whole object out in+-- place of the name the program called it by. A λ the registry does not carry+-- is left alone rather than fired and got stuck on, so what phino cannot+-- compute stays as it was written with or without '_partial'; an atom that+-- cannot fire deeper on the spine still fails the run, exactly as it does+-- under 𝕄 alone, and '_partial' parks it. A formation still waiting for its+-- arguments is left alone too (see 'saturated').+fired :: Expression -> Expression -> State -> DataizeContext -> IO (Maybe (Expression, State))+fired term univ state caller = do+  ctx <- deeper caller+  morphed <- try (reduced ctx)+  case morphed of+    Right (ExFormation bds, state') -> maybe (pure Nothing) (evaluated ctx state') (saturated bds)+    Right _ -> pure Nothing+    Left failure -> parked failure+  where+    -- 𝕄 takes normal forms only and a term taken from the program as it was+    -- written is not necessarily one, so it is normalized against the universe+    -- first, exactly as '--inside' normalizes what it is handed. Both chains+    -- are dropped: the walk is not the spine and reports one step of its own+    -- (see 'morph'), so a stuck atom leaves without a derivation ('unparked').+    reduced :: DataizeContext -> IO (Expression, State)+    reduced ctx = unparked $ do+      (normal, _) <- normalized term ((univ, Nothing) :| []) ctx+      ((morphed, _), state') <- morph' (normal, (univ, Nothing) :| []) univ state ctx+      pure (morphed, state')+    -- Fire the λ of the formation 𝕄 reached and go on from its answer, keeping+    -- the answer of the last firing. The firing is reported to '_saveEval' like+    -- every other one, with the term the caller is given, so the protocol and+    -- the program agree on what the atom answered.+    evaluated :: DataizeContext -> State -> (T.Text, Expression) -> IO (Maybe (Expression, State))+    evaluated ctx state' (func, self) = case registeredAtom ctx._atoms func of+      Nothing -> pure Nothing+      Just registered -> do+        answer <- fireAtom func registered self univ+        ctx._saveEval (Evaluation func self (Just answer))+        again <- fired answer univ state' ctx+        pure (Just (fromMaybe (answer, state') again))+    parked :: DataizeException -> IO (Maybe a)+    parked (Stuck _) | caller._partial = pure Nothing+    parked failure = throwIO failure  -- Dataize the expression located at '_locator'. The whole input expression is -- itself the universe Q (the 'e' argument) threaded through 𝔻 and 𝕄, so it is

@@ -169,7 +169,10 @@ _string [Y.ArgExpression expr] subst = do   expr' <- buildExpressionThrows expr subst   str <- case expr' of-    DataNumber bts -> pure (DataString (strToBts (either show show (btsToNum bts))))+    DataNumber bts+      | btsSize bts /= 8 ->+          throwIO (userError (printf "Expected 8 bytes for a number, got %d" (btsSize bts)))+      | otherwise -> pure (DataString (strToBts (either show show (btsToNum bts))))     DataString bts -> pure (DataString bts)     ex ->       throwIO

@@ -125,6 +125,7 @@   where     notAsset (BiDelta _) = False     notAsset (BiLambda _) = False+    notAsset (BiVoid AtRho) = False     notAsset _ = True numToInt (Y.Literal num) _ = Just num numToInt _ _ = Nothing

@@ -22,7 +22,7 @@ where  import AST-import Bytes (btsToNum, btsToStr, bytesToBts)+import Bytes (btsSize, btsToNum, btsToStr, bytesToBts) import Control.Exception (Exception (displayException), throwIO) import Data.Bifunctor (bimap) import Data.Foldable (foldlM)@@ -97,6 +97,7 @@ expression :: Expression -> XmirContext -> IO (String, [Node]) expression ExXi _ = pure (printExpression ExXi, []) expression ExRoot _ = pure (printExpression ExRoot, [])+expression ExTermination _ = pure ("⊥", []) expression (ExFormation bds) ctx = do   nested <- nestedBindings bds ctx   pure ("", nested)@@ -116,7 +117,7 @@           [object [("as", "data")] [NodeContent (T.pack (printBytes bytes))]]    in pure         ( "Φ.number"-        , if _omitComments+        , if _omitComments || btsSize bytes /= 8             then [bts]             else               [ NodeComment (T.pack (either show show (btsToNum bytes)))@@ -484,6 +485,10 @@           if null (cur C.$/ C.element (toName "o"))             then pure ExRoot             else throwIO (InvalidXMIRFormat "Application of 'Φ' is illegal in XMIR" cur)+        "⊥" ->+          if null (cur C.$/ C.element (toName "o"))+            then pure ExTermination+            else throwIO (InvalidXMIRFormat "Application of '⊥' is illegal in XMIR" cur)         'Φ' : '.' : rest -> xmirToExpression' ExRoot "Φ" rest cur fqn         'ξ' : '.' : rest -> xmirToExpression' ExXi "ξ" rest cur fqn         _ -> throwIO (InvalidXMIRFormat "The @base attribute must be either ['∅'|'Φ'] or start with ['Φ.'|'ξ.'|'.']" cur)

@@ -1502,6 +1502,64 @@             ["morph", "--locator=Q.@", "--partial", "--flat", "--hide-rho"]             ["⟦ λ ⤍ Sym_arg_0 ⟧.foo"] +    -- 𝕄 stops at the first formation and hands its bindings back as they were+    -- written, so a program whose parts nothing demands is never reduced;+    -- '--deep' enters every binding and finishes what 'mf' left, while what no+    -- atom touched keeps its name and the answer stays a program (#1124)+    describe "--deep" $ do+      let program =+            "[[ bytes(data) -> [[ @ -> $.data ]], \+            \number(as-bytes) -> [[ @ -> $.as-bytes, times(x) -> [[ L> L_number_times ]] ]], \+            \bar(x) -> [[ L> L_bar ]], \+            \demo -> [[ foo -> [[ n -> 3, @ -> Q.bar( $.n.times( 5 ).times( 7 ) ) ]] ]] ]]"+      it "answers the formation as it was written without the flag" $+        withAtoms $ \atoms ->+          withStdin program $+            testCLISucceeded+              ["morph", atoms, "--inside=Q.demo.foo", "--sweet", "--hide-rho", "--flat"]+              ["⟦ n ↦ 3, φ ↦ Φ.bar( n.times( 5 ).times( 7 ) ) ⟧"]++      -- 'L_bar' is not in the registry, so the call to it stays as written and+      -- keeps its name, while the arithmetic in the argument nothing demands+      -- folds into the number it makes+      it "reduces every binding it can and leaves the rest in place" $+        withAtoms $ \atoms ->+          withStdin program $+            testCLISucceeded+              ["morph", atoms, "--deep", "--inside=Q.demo.foo", "--sweet", "--hide-rho", "--flat"]+              ["⟦ n ↦ 3, φ ↦ Φ.bar( 105 ) ⟧"]++      -- The same term the run above stops at as a bare λ-formation: 'mf' leaves+      -- it to 𝔻, and the walk fires it instead of demanding bytes+      it "fires the bare saturated λ-formation mf hands back" $+        withAtoms $ \atoms ->+          withStdin chained $+            testCLISucceeded+              ["morph", atoms, "--deep", "--locator=Q.@", "--sweet", "--hide-rho", "--flat"]+              ["18"]++      -- The default locator walks the whole program: the method table of the+      -- object model keeps every one of its λ-formations, since not one of them+      -- is saturated, while the one place that can be computed is+      it "keeps the object model intact while it folds the program" $+        withAtoms $ \atoms ->+          withStdin program $+            testCLISucceeded+              ["morph", atoms, "--deep", "--sweet", "--hide-rho", "--flat"]+              [ "number(as-bytes) ↦ ⟦ φ ↦ as-bytes, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧"+              , "demo ↦ ⟦ foo ↦ ⟦ n ↦ 3, φ ↦ Φ.bar( 105 ) ⟧ ⟧"+              ]++      it "keeps a binding whose spine got stuck with --partial" $+        withStdin "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" $+          testCLISucceeded+            ["morph", "--deep", "--partial", "--sweet", "--hide-rho", "--flat"]+            ["⟦ x ↦ ⟦ λ ⤍ Sym_arg_0 ⟧.foo ⟧"]++      it "fails on that same spine without --partial" $+        withStdin "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" $+          testCLIFailed ["morph", "--deep"] ["Atom 'Sym_arg_0' does not exist"]+     describe "fails" $ do       it "with --output != latex and --nonumber" $         withStdin "" $@@ -1586,7 +1644,7 @@             [ "\\phinoNormalizationRule{alpha}"             , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\phiTerminal{\\alpha_{i1}} -> e_1 ) }"             , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> e_1 ) }"-            , "  { i_1 = \\vert \\overline{ B_1 } \\vert }"+            , "  { i_1 = \\vert \\overline{ B_1 } \\vert \\;\\text{and}\\; \\tau_1 \\not= \\phiTerminal{\\rho} }"             , "  { }"             , "\\phinoNormalizationRule{amiss}"             , "  { [[ B_1 ]] ( \\phiTerminal{\\alpha_{i1}} -> e ) }"

@@ -150,6 +150,8 @@       , ("is true for negative infinity", BtMany ["FF", "F0", "00", "00", "00", "00", "00", "00"], True)       , ("is false for a NaN carrying a payload", BtMany ["7F", "F8", "00", "00", "00", "00", "00", "01"], False)       , ("is false for the negative quiet NaN", BtMany ["FF", "F8", "00", "00", "00", "00", "00", "00"], False)+      , ("is false for fewer than eight bytes", BtOne "21", False)+      , ("is false for empty bytes", BtEmpty, False)       ]       (\(desc, bts, expected) -> it desc (sweetNumber bts `shouldBe` expected)) 

@@ -32,7 +32,7 @@ -- empty, since phino implements none of them: a case that needs an atom to -- answer brings the fixture registry in through 'withAtoms'. defaultDataizeContext :: Expression -> DataizeContext-defaultDataizeContext loc = DataizeContext loc 25 25 (Steps 250 0) False True False emptyRegistry buildTerm dontSaveStep dontSaveEval+defaultDataizeContext loc = DataizeContext loc 25 25 (Steps 250 0) False True False False emptyRegistry buildTerm dontSaveStep dontSaveEval  -- The same context with the fixture λ functions registered (see 'Fixtures'). withAtoms :: Registry -> DataizeContext -> DataizeContext@@ -71,6 +71,20 @@       (morphed, _) <- morph expr (defaultDataizeContext loc')       morphed `shouldBe` expected +-- The same as 'testMorph', with the deep walk on ('_deep') and the fixture λ+-- functions registered, since a case that reduces anything has to fire one: it+-- is pending where 'node' is not installed.+testDeep :: Registry -> [(String, String, String, String)] -> Spec+testDeep registry useCases =+  forM_ useCases $ \(name, loc, src, res) ->+    it name $+      withNode $ do+        expr <- parseExpressionThrows src+        loc' <- parseExpressionThrows loc+        expected <- parseExpressionThrows res+        (morphed, _) <- morph expr (withAtoms registry (defaultDataizeContext loc')){_deep = True}+        morphed `shouldBe` expected+ -- The EO objects the fixture λ functions answer for, declared the way -- 'number.eo' and 'bytes.eo' declare them, so a case below only has to spell -- the expression under φ. 'number.eq' is the one operation with no atom of its@@ -196,6 +210,78 @@         (residue, _) <- morph expr (defaultDataizeContext loc){_partial = True}         residue `shouldBe` expected +  -- 𝕄 stops at the first formation 'mf' hands back and leaves its bindings as+  -- they were written, since firing a bare λ is 𝔻's business, so a program+  -- whose parts nothing demands is never reduced (#1124). The deep walk+  -- ('_deep') enters every binding and finishes what 'mf' left, while what no+  -- atom touched keeps the shape it was written in and the answer stays a+  -- program.+  describe "morph with '_deep'" $ do+    testDeep+      registry+      [+        ( "stands the answer of the λ that 'mf' left bare in its place"+        , "Q.@"+        , primitives "[[ x -> 5.plus( 6 ) ]]"+        , "[[ x -> Q.number( as-bytes -> Q.bytes( data -> [[ D> 40-26-00-00-00-00-00-00 ]] ) ) ]]"+        )+      ,+        ( "keeps the answer of the last atom fired along one chain of them"+        , "Q.@"+        , primitives "[[ x -> 5.plus( 6 ).plus( 7 ) ]]"+        , "[[ x -> Q.number( as-bytes -> Q.bytes( data -> [[ D> 40-32-00-00-00-00-00-00 ]] ) ) ]]"+        )+      ,+        ( "resolves the ξ of a binding against the formation that holds it"+        , "Q.@"+        , primitives "[[ n -> 5, x -> $.n.plus( 6 ) ]]"+        , "[[ n -> 5, x -> Q.number( as-bytes -> Q.bytes( data -> [[ D> 40-26-00-00-00-00-00-00 ]] ) ) ]]"+        )+      , -- The registry carries no 'L_number_nope', so there is nothing to fire+        -- and the binding keeps the name it was written under++        ( "leaves the λ the registry does not serve as it was written"+        , "Q.@"+        , primitives "[[ x -> 5.nope ]]"+        , "[[ x -> 5.nope ]]"+        )+      , -- A λ-formation whose bindings are still void is a method waiting to be+        -- applied, not an application waiting to be computed: nothing demands+        -- one, so 𝔻 never meets one, while the walk meets every one the object+        -- model declares. Both the void ρ of 'not' and the void 'b' of 'eq'+        -- keep their atoms unfired here.++        ( "leaves a λ-formation still waiting for its arguments alone"+        , "Q.bytes"+        , primitives "[[ ]]"+        , "[[ data -> ?, @ -> $.data, not -> [[ L> L_bytes_not ]], eq -> [[ b -> ?, L> L_bytes_eq ]] ]]"+        )+      , -- Nothing demands the argument of an atom that cannot fire, so 𝔻 never+        -- reaches it; the walk does, and the atom around it stays in place++        ( "walks into the argument of an atom it cannot fire"+        , "Q.@"+        , primitives "[[ x -> [[ y -> ?, L> L_bar ]]( y -> 6.plus( 7 ) ) ]]"+        , "[[ x -> [[ y -> ?, L> L_bar ]]( y -> Q.number( as-bytes -> Q.bytes( data -> [[ D> 40-2A-00-00-00-00-00-00 ]] ) ) ) ]]"+        )+      ]++    -- An atom deeper on a binding's spine gets stuck exactly as it does under+    -- 𝕄 alone: the run fails, unless '_partial' parks it, and then the binding+    -- stays as it was written and the walk goes on+    describe "a stuck atom on the spine of a binding" $ do+      let stuck :: IO Expression+          stuck = parseExpressionThrows "[[ x -> [[ L> Sym_arg_0 ]].foo ]]"+      it "fails the run without '_partial'" $ do+        expr <- stuck+        morph expr (defaultDataizeContext ExRoot){_deep = True}+          `shouldThrow` (\e -> "Atom 'Sym_arg_0' does not exist" `isInfixOf` show (e :: SomeException))++      it "leaves the binding as it was written under '_partial'" $ do+        expr <- stuck+        (morphed, _) <- morph expr (defaultDataizeContext ExRoot){_deep = True, _partial = True}+        morphed `shouldBe` expr+   describe "morph'" $     test'       morph'@@ -487,7 +573,7 @@     it "fails on the step limit instead of morphing forever" $       withNode $ do         expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧"-        dataize expr (DataizeContext ExRoot 25 25 (Steps 40 0) False True False registry buildTerm dontSaveStep dontSaveEval)+        dataize expr (DataizeContext ExRoot 25 25 (Steps 40 0) False True False False registry buildTerm dontSaveStep dontSaveEval)           `shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException))    -- An atom phino does not know — a name the '--atoms' registry does not carry,@@ -551,12 +637,12 @@     forM_       [         ( "--max-cycles"-        , DataizeContext ExRoot 25 0 (Steps 250 0) True True False emptyRegistry buildTerm dontSaveStep dontSaveEval+        , DataizeContext ExRoot 25 0 (Steps 250 0) True True False False emptyRegistry buildTerm dontSaveStep dontSaveEval         , "--max-cycles=0"         )       ,         ( "--max-depth"-        , DataizeContext ExRoot 0 25 (Steps 250 0) True True False emptyRegistry buildTerm dontSaveStep dontSaveEval+        , DataizeContext ExRoot 0 25 (Steps 250 0) True True False False emptyRegistry buildTerm dontSaveStep dontSaveEval         , "--max-depth=0"         )       ]@@ -566,8 +652,8 @@             dataize expr ctx `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException))       )     forM_-      [ ("--max-cycles", DataizeContext ExRoot 25 0 (Steps 250 0) False True False emptyRegistry buildTerm dontSaveStep dontSaveEval)-      , ("--max-depth", DataizeContext ExRoot 0 25 (Steps 250 0) False True False emptyRegistry buildTerm dontSaveStep dontSaveEval)+      [ ("--max-cycles", DataizeContext ExRoot 25 0 (Steps 250 0) False True False False emptyRegistry buildTerm dontSaveStep dontSaveEval)+      , ("--max-depth", DataizeContext ExRoot 0 25 (Steps 250 0) False True False False emptyRegistry buildTerm dontSaveStep dontSaveEval)       ]       ( \(flag, ctx) ->           it ("does not throw without --depth-sensitive even once " ++ flag ++ " is exhausted") $ do

@@ -102,6 +102,20 @@             parseExpression printed `shouldBe` Right expr       ) +  describe "printExpression keeps a number with fewer than eight bytes in byte form" $+    forM_+      [ ("one byte", BtOne "21")+      , ("three bytes", BtMany ["00", "01", "02"])+      ]+      ( \(desc, bts) ->+          it desc $ do+            let expr = DataNumber bts+                printed = printExpression' expr (SWEET, ASCII, SINGLELINE, defaultMargin)+            printed `shouldContain` "number"+            printed `shouldContain` "bytes"+            parseExpression printed `shouldBe` Right expr+      )+   describe "printExpression keeps a compressed meet atomic under a narrow margin" $     -- A \phinoMeet is a single \overbracket visual unit, so its body must stay     -- on one line even when the surrounding margin forces the outer formation to

@@ -219,7 +219,6 @@       , "Q"       , "$"       , "[[ x -> T ]]"-      , "[[ top -> [[ x -> T ]] ]]"       , "[[ x -> [[ !t1 -> 5 ]] ]]"       , "[[ org -> [[ z -> ?, L> Package ]] ]]"       ]@@ -271,7 +270,7 @@       ,         ( "explains an unsupported nested expression"         , do-            expr <- parseExpressionThrows "[[ x -> [[ y -> T ]] ]]"+            expr <- parseExpressionThrows "[[ x -> [[ y -> !e1 ]] ]]"             try (void (expressionToXMIR expr defaultXmirContext)) :: IO (Either SomeException ())         , ["XMIR does not support such expression"]         )