phino 0.0.111 → 0.0.112

raw patch · 10 files changed

+173/−60 lines, 10 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• phino.cabal +1/−1
• src/CLI/Helpers.hs +14/−7
• src/CLI/Parsers.hs +7/−0
• src/CLI/Runners.hs +5/−7
• src/CLI/Types.hs +1/−0
• src/Dataize.hs +78/−37
• src/Deps.hs +4/−4
• src/Rewriter.hs +1/−1
• test/CLISpec.hs +48/−1
• test/DataizeSpec.hs +14/−2

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

@@ -13,6 +13,7 @@ import Control.Exception import Control.Monad ((>=>)) import Data.Functor ((<&>))+import Data.IORef import Data.List (intercalate) import Data.Maybe import Deps (SaveStepFunc, saveStep)@@ -39,13 +40,19 @@ justMeetLength = fromMaybe defaultMeetLength  -- Prepare saveStepFunc-saveStepFunc :: Maybe FilePath -> PrintContext -> SaveStepFunc-saveStepFunc stepsDir ctx@PrintCtx{..} = saveStep stepsDir ioToExt (printInFormat ctx)-  where-    ioToExt :: String-    ioToExt-      | _outputFormat == LATEX = "tex"-      | otherwise = show _outputFormat+saveStepFunc :: Maybe FilePath -> PrintContext -> IO SaveStepFunc+saveStepFunc stepsDir ctx@PrintCtx{..} = do+  counter <- newIORef (0 :: Int)+  let ioToExt :: String+      ioToExt+        | _outputFormat == LATEX = "tex"+        | otherwise = show _outputFormat+      render = printInFormat ctx+      save :: SaveStepFunc+      save expr = do+        step <- atomicModifyIORef' counter (\value -> (value + 1, value + 1))+        saveStep stepsDir ioToExt render step expr+  pure save  -- Read input from file or stdin readInput :: Maybe FilePath -> IO String

@@ -81,6 +81,12 @@     (auto >>= validateIntOption (> 0) "--max-cycles must be positive")     (long "max-cycles" <> metavar "CYCLES" <> help "Maximum number of rewriting cycles across all rules" <> value 25 <> showDefault) +optMaxSteps :: Parser Int+optMaxSteps =+  option+    (auto >>= validateIntOption (> 0) "--max-steps must be positive")+    (long "max-steps" <> metavar "STEPS" <> help "Maximum number of nested morphing and dataization steps" <> value 1000 <> showDefault)+ optMargin :: Parser Int optMargin =   option@@ -287,6 +293,7 @@             <*> optCompress             <*> optMaxDepth             <*> optMaxCycles+            <*> optMaxSteps             <*> optMargin             <*> optMeetPopularity             <*> optMeetLength

@@ -45,11 +45,11 @@   included <- validatedDispatches "show" _show   [loc] <- validatedDispatches "locator" [_locator]   [foc] <- validatedDispatches "focus" [_focus]+  setStdGen (mkStdGen _seed)   rules <- getRules _normalize _shuffle _rules   validateBreakpoint _breakpoint rules   input <- readInput _inputFile   expr <- parseInput input _inputFormat-  setStdGen (mkStdGen _seed)   seedTaus expr   logDebug (printf "Amount of rewriting cycles across all the rules: %d, per rule: %d" _maxCycles _maxDepth)   let listing = case (rules, _inputFormat, _outputFormat) of@@ -60,7 +60,8 @@       printCtx = toPrintCtx xmirCtx foc       exclude = (`F.exclude` excluded)       include = (`F.include` included)-  (rewrittens, exceeded) <- rewrite expr rules (context loc printCtx)+  save <- saveStepFunc _stepsDir printCtx+  (rewrittens, exceeded) <- rewrite expr rules (RewriteContext loc _maxDepth _maxCycles _depthSensitive buildTerm _must _breakpoint save)   let rewrittens' = exclude $ include (if _sequence then NE.toList rewrittens else [NE.last rewrittens])   logDebug (printf "Printing rewritten 𝜑-expression as %s" (show _outputFormat))   exprs <- printRewrittens printCtx (rewrittens', exceeded)@@ -113,8 +114,6 @@       (False, Nothing, _) -> do         logDebug "The option '--target' is not specified, printing to console..."         putStrLn expr-    context :: Expression -> PrintContext -> RewriteContext-    context loc ctx = RewriteContext loc _maxDepth _maxCycles _depthSensitive buildTerm _must _breakpoint (saveStepFunc _stepsDir ctx)     toPrintCtx :: XmirContext -> Expression -> PrintContext     toPrintCtx xmirCtx focus =       PrintCtx@@ -150,7 +149,8 @@   let printCtx = toPrintCtx foc       exclude = (`F.exclude` excluded)       include = (`F.include` included)-  (bytes, chain) <- dataize expr (context loc printCtx)+  save <- saveStepFunc _stepsDir printCtx+  (bytes, chain) <- dataize expr (DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle buildTerm save)   when _sequence (printRewrittens printCtx (exclude $ include chain, False) >>= putStrLn)   unless _quiet (putStrLn (P.printBytes bytes))   where@@ -163,8 +163,6 @@         [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]       validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus       when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")-    context :: Expression -> PrintContext -> DataizeContext-    context loc ctx = DataizeContext loc _maxDepth _maxCycles _depthSensitive _shuffle buildTerm (saveStepFunc _stepsDir ctx)     toPrintCtx :: Expression -> PrintContext     toPrintCtx focus =       PrintCtx

@@ -94,6 +94,7 @@   , _compress :: Bool   , _maxDepth :: Int   , _maxCycles :: Int+  , _maxSteps :: Int   , _margin :: Int   , _meetPopularity :: Maybe Int   , _meetLength :: Maybe Int

@@ -1,3 +1,5 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedRecordDot #-}@@ -9,12 +11,12 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Dataize (morph, dataize, dataize', DataizeContext (..), State, emptyState, execBuildTerm) where+module Dataize (morph, dataize, dataize', DataizeContext (..), Steps (..), State, emptyState, execBuildTerm) where  import AST import Builder (buildBytesThrows, buildExpressionThrows) import Bytes (btsAnd, btsConcat, btsEqual, btsNot, btsOr, btsShift, btsSize, btsSlice, btsToNum, numToBts, strToBts)-import Control.Exception (throwIO)+import Control.Exception (Exception, throwIO) import Control.Monad (foldM) import Data.Int (Int32) import Data.List (find, partition)@@ -44,22 +46,59 @@ emptyState :: State emptyState = "" --- The evaluation context carries only configuration. Nothing global is fixed--- here: the universe (the second argument 'e' of 𝕄(n, e, s) and 𝔻(n, e, s)) is a--- plain expression threaded as an argument to 'dataize'', 'morph' and on to the--- atoms, and the state 's' is threaded the same way (see 'State'). The working--- expression needed for normalization is taken from the head of the step chain,--- so no separate wrapper type is threaded around.+-- How many steps of the 𝕄/𝔻 recursion one branch of a derivation may take+-- ('_limit', the '--max-steps' option) and how many the branch reaching this+-- point has already taken ('_spent'). 𝕄 and 𝔻 recurse into each other, into the+-- premises of their own rules and into the atoms they fire, so a budget local to+-- one of those chains is reset by the next nested call and bounds nothing (see+-- #1052). This one rides in the context that every such path — the spine, the+-- side-premises, '_dataize' and '_morph' — already carries, so a nested call+-- inherits the count of the call that made it. It bounds depth, not total work:+-- a premise passes its count down but not back, so siblings each descend from+-- the same '_spent'. Bounding every branch is enough to terminate, since a rule+-- has finitely many premises.+data Steps = Steps+  { _limit :: Int+  , _spent :: Int+  }++-- The evaluation context carries the configuration plus the step budget spent so+-- far. Nothing global is fixed here: the universe (the second argument 'e' of+-- 𝕄(n, e, s) and 𝔻(n, e, s)) is a plain expression threaded as an argument to+-- 'dataize'', 'morph' and on to the atoms, and the state 's' is threaded the same+-- way (see 'State'). The working expression needed for normalization is taken+-- from the head of the step chain, so no separate wrapper type is threaded+-- around. data DataizeContext = DataizeContext   { _locator :: Expression   , _maxDepth :: Int   , _maxCycles :: Int+  , _steps :: Steps   , _depthSensitive :: Bool   , _shuffle :: Bool   , _buildTerm :: BuildTermFunc   , _saveStep :: SaveStepFunc   } +newtype DataizeException = OutOfSteps Int+  deriving anyclass (Exception)++instance Show DataizeException where+  show (OutOfSteps limit) =+    printf "Dataization did not finish before reaching the limit of steps: --max-steps=%d" limit++-- Charge one step of the 𝕄/𝔻 recursion to the budget, refusing to descend once+-- it is gone. '--max-cycles' and '--max-depth' bound only the normalization run+-- inside a single step, so before this the recursion itself was unbounded and a+-- term that never reduces to bytes kept 𝕄 and 𝔻 calling each other forever+-- (#1052). Rewriting hands back whatever it has reached when it runs out of+-- cycles; 𝔻 has no partial answer to give, so an exhausted budget always throws,+-- with or without '--depth-sensitive'.+deeper :: DataizeContext -> IO DataizeContext+deeper ctx@DataizeContext{_steps = Steps limit spent}+  | spent >= limit = throwIO (OutOfSteps limit)+  | otherwise = pure ctx{_steps = Steps limit (spent + 1)}+ -- Resolve formation for LAMBDA Morphing rule. -- If formation contains λ binding, the called atom result is returned. The -- universe 'univ' is forwarded to the atom.@@ -100,20 +139,21 @@ -- chain before morphing continues. Every other premise is a side-computation -- evaluated in isolation by 'sidePremise', its own steps discarded. morph :: Morphed -> Expression -> State -> DataizeContext -> IO (Morphed, State)-morph (expr, seq) univ state ctx = do+morph (expr, seq) univ state caller = do+  ctx <- deeper caller   rules <- if ctx._shuffle then shuffle Y.morphingRules else pure Y.morphingRules-  matched <- firstMatch rules+  matched <- firstMatch ctx rules   case matched of-    Just (rule, subst) -> reduce rule subst+    Just (rule, subst) -> reduce ctx rule subst     Nothing -> throwIO (userError "no morphing rule matched")   where-    firstMatch :: [Y.MorphRule] -> IO (Maybe (Y.MorphRule, Subst))-    firstMatch [] = pure Nothing-    firstMatch (rule : rest) = do+    firstMatch :: DataizeContext -> [Y.MorphRule] -> IO (Maybe (Y.MorphRule, Subst))+    firstMatch _ [] = pure Nothing+    firstMatch ctx (rule : rest) = do       substs <- matchExpressionWithRule' (matchExpression' rule.ematch univ) expr (asRule rule) (RuleContext (execBuildTerm univ ctx))       case substs of         (subst : _) -> pure (Just (rule, subst))-        [] -> firstMatch rest+        [] -> firstMatch ctx rest     -- Match the conclusion term and check the guard; premises are no longer the     -- matcher's business, so 'where'/'having' stay empty and the guard lives in     -- 'when'. Every morphing guard reads only meta-variables bound by 'match'@@ -125,28 +165,28 @@     -- trailing 'morph' premise (the spine); if that premise's argument is itself     -- bound by a 'normalize' premise, the normalization joins the spine and its     -- steps splice in before morphing continues.-    reduce :: Y.MorphRule -> Subst -> IO (Morphed, State)-    reduce rule subst = case producer rule.nresult rule.premises of+    reduce :: DataizeContext -> Y.MorphRule -> Subst -> IO (Morphed, State)+    reduce ctx rule subst = case producer rule.nresult rule.premises of       Nothing -> do-        (final, state') <- sides rule.premises subst+        (final, state') <- sides ctx rule.premises subst         built <- buildExpressionThrows rule.nresult final         seq' <- leadsTo seq rule.name built ctx         pure ((built, seq'), state')       Just concl@(Y.Premise _ (Y.OpMorph arg)) -> case producer arg rule.premises of         Just normal@(Y.Premise _ (Y.OpNormalize inner)) -> do-          (final, state') <- sides (rule.premises `excluding` [concl, normal]) subst+          (final, state') <- sides ctx (rule.premises `excluding` [concl, normal]) subst           built <- buildExpressionThrows inner final           labelled <- leadsTo seq rule.name built ctx           (normal', seq') <- normalized built labelled ctx           morph (normal', seq') univ state' ctx         _ -> do-          (final, state') <- sides (rule.premises `excluding` [concl]) subst+          (final, state') <- sides ctx (rule.premises `excluding` [concl]) subst           built <- buildExpressionThrows arg final           seq' <- leadsTo seq rule.name built ctx           morph (built, seq') univ state' ctx       Just _ -> throwIO (userError (printf "morphing rule '%s' must conclude with a 'morph' premise" rule.name))-    sides :: [Y.Premise] -> Subst -> IO (Subst, State)-    sides premises subst = foldM (sidePremise univ ctx) (subst, state) premises+    sides :: DataizeContext -> [Y.Premise] -> Subst -> IO (Subst, State)+    sides ctx premises subst = foldM (sidePremise univ ctx) (subst, state) premises  -- Dataize the expression located at '_locator'. The whole input expression is -- itself the universe Q (the 'e' argument) threaded through 𝔻 and 𝕄, so it is@@ -181,11 +221,12 @@ -- when its argument is bound by a 'morph' or 'normalize' premise, that step -- joins the spine, otherwise the premise is an isolated side-computation. dataize' :: Dataizable -> Expression -> State -> DataizeContext -> IO (Dataized, State)-dataize' (expr, seq) univ state ctx = do+dataize' (expr, seq) univ state caller = do+  ctx <- deeper caller   rules <- if ctx._shuffle then shuffle Y.dataizationRules else pure Y.dataizationRules-  matched <- firstMatch rules+  matched <- firstMatch ctx rules   case matched of-    Just (rule, subst) -> reduce rule subst+    Just (rule, subst) -> reduce ctx rule subst     Nothing -> throwIO (userError (unmatched expr))   where     -- 𝔻 is partial: the terminator ⊥ signals an error and lies outside its@@ -195,19 +236,19 @@     unmatched :: Expression -> String     unmatched ExTermination = "dataization reached the terminator ⊥, which signals an error and cannot be dataized"     unmatched _ = "no dataization rule matched"-    firstMatch :: [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst))-    firstMatch [] = pure Nothing-    firstMatch (rule : rest) = do+    firstMatch :: DataizeContext -> [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst))+    firstMatch _ [] = pure Nothing+    firstMatch ctx (rule : rest) = do       substs <- matchExpressionWithRule' (matchExpression' rule.ematch univ) expr (asRule rule) (RuleContext (execBuildTerm univ ctx))       case substs of         (subst : _) -> pure (Just (rule, subst))-        [] -> firstMatch rest+        [] -> firstMatch ctx rest     asRule :: Y.DataizeRule -> Y.Rule     asRule rule = Y.Rule rule.name Nothing Nothing rule.match ExRoot rule.when Nothing Nothing-    reduce :: Y.DataizeRule -> Subst -> IO (Dataized, State)-    reduce rule subst = case bytesProducer rule.dresult rule.premises of+    reduce :: DataizeContext -> Y.DataizeRule -> Subst -> IO (Dataized, State)+    reduce ctx rule subst = case bytesProducer rule.dresult rule.premises of       Nothing -> do-        (final, state') <- sides rule.premises subst+        (final, state') <- sides ctx rule.premises subst         bts <- buildBytesThrows rule.dresult final         seq' <- leadsTo seq rule.name (ExBytes bts) ctx         pure ((bts, NE.toList seq'), state')@@ -217,7 +258,7 @@         -- so 𝔻 only ever sees normal forms.         Just normal@(Y.Premise _ (Y.OpNormalize inner)) -> do           let side = rule.premises `excluding` [concl, normal]-          (final, state') <- sides side subst+          (final, state') <- sides ctx side subst           built <- buildExpressionThrows inner final           labelled <- leadsTo seq (labelOf side) built ctx           (normal', seq') <- normalized built labelled ctx@@ -225,7 +266,7 @@         -- 𝔻(𝕄(e)) delegates to the morphing relation, splicing its steps into the         -- chain before dataizing on.         Just morphed@(Y.Premise _ (Y.OpMorph inner)) -> do-          (final, state') <- sides (rule.premises `excluding` [concl, morphed]) subst+          (final, state') <- sides ctx (rule.premises `excluding` [concl, morphed]) subst           built <- buildExpressionThrows inner final           ((morphed', seq'), state'') <- morph (built, seq) univ state' ctx           dataize' (morphed', seq') univ state'' ctx@@ -237,13 +278,13 @@         -- conclusion's own verb ('dataize' for 𝔻(⊥)).         _ -> do           let side = rule.premises `excluding` [concl]-          (final, state') <- sides side subst+          (final, state') <- sides ctx side subst           built <- buildExpressionThrows arg final           seq' <- leadsTo seq (labelOr (verb concl.operation) side) built ctx           dataize' (built, seq') univ state' ctx       Just _ -> throwIO (userError (printf "dataization rule '%s' must conclude with a 'dataize' premise" rule.name))-    sides :: [Y.Premise] -> Subst -> IO (Subst, State)-    sides premises subst = foldM (sidePremise univ ctx) (subst, state) premises+    sides :: DataizeContext -> [Y.Premise] -> Subst -> IO (Subst, State)+    sides ctx premises subst = foldM (sidePremise univ ctx) (subst, state) premises     -- A spliced dataization step is labelled by its first side-computation —     -- 'box' by its 'contextualize', 'fire' by its 'evaluate'; with none it is blank.     labelOf :: [Y.Premise] -> String

@@ -41,11 +41,11 @@  type BuildTermFunc = String -> BuildTermMethod -type SaveStepFunc = Expression -> Int -> IO ()+type SaveStepFunc = Expression -> IO () -saveStep :: Maybe FilePath -> String -> (Expression -> IO String) -> SaveStepFunc+saveStep :: Maybe FilePath -> String -> (Expression -> IO String) -> Int -> SaveStepFunc saveStep Nothing _ _ _ _ = pure ()-saveStep (Just dir) ext render expr step = do+saveStep (Just dir) ext render step expr = do   createDirectoryIfMissing True dir   let path = dir </> printf "%05d.%s" step ext   content <- render expr@@ -53,4 +53,4 @@   logDebug (printf "Saved step '%d' to '%s'" step path)  dontSaveStep :: SaveStepFunc-dontSaveStep = saveStep Nothing "" (\_ -> pure "")+dontSaveStep = saveStep Nothing "" (\_ -> pure "") 0

@@ -224,7 +224,7 @@                                     (printExpression expr)                                 )                               updated <- withLocatedExpression _locator expr current-                              _saveStep updated (((iteration - 1) * _maxDepth) + _count)+                              _saveStep updated                               _rewrite (leadsTo updated, seenInsert digest expr _unique, False) (_count + 1)       where         leadsTo :: Expression -> NonEmpty Rewritten

@@ -9,7 +9,7 @@ import CLI (runCLI) import Control.Exception import Control.Monad (forM_, unless, when)-import Data.List (intercalate, isInfixOf)+import Data.List (intercalate, isInfixOf, sort) import Data.Time.Clock (addUTCTime, getCurrentTime) import Data.Time.Clock.POSIX (getPOSIXTime) import Data.Version (showVersion)@@ -366,6 +366,22 @@         ["rewrite", "--help"]         ["default: 0"] +    it "reproduces the same shuffle order for the same --seed" $ do+      let args =+            [ "rewrite"+            , "--shuffle"+            , "--seed=42"+            , "--sweet"+            , "--sequence"+            , "--max-depth=1"+            , "--max-cycles=1"+            , rule "swap-a.yaml"+            , rule "swap-b.yaml"+            ]+      (firstRun, _) <- withStdin "[[ x -> 5 ]]" $ withStdout (runCLI args)+      (secondRun, _) <- withStdin "[[ x -> 5 ]]" $ withStdout (runCLI args)+      firstRun `shouldBe` secondRun+     it "fails with a non-integer --seed" $       withStdin "[[ ]]" $         testCLIFailed@@ -387,6 +403,25 @@         (`shouldBe` True) <$> doesFileExist (dir ++ "/00003.phi")         removeDirectoryRecursive dir +    it "saves dataize steps to dir with --steps-dir" $ do+      let dir = "test-steps-temp-dataize"+      dirExists <- doesDirectoryExist dir+      when dirExists (removeDirectoryRecursive dir)+      withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ do+        testCLISucceeded+          ["dataize", "--steps-dir=" ++ dir, "--sweet"]+          ["40-26"]+        (`shouldBe` True) <$> doesDirectoryExist dir+        files <- listDirectory dir+        let steps = sort files+        -- The fix is about numbering, not about a specific rule set: the file+        -- names must be distinct and contiguous from 00001, and there must be+        -- more of them than a single normalization pass produces (this input+        -- runs several normalizations, so a global counter yields more steps).+        steps `shouldBe` map (\n -> printf "%05d.phi" (n :: Int)) [1 .. length steps]+        length steps `shouldSatisfy` (> 18)+        removeDirectoryRecursive dir+     it "desugares without any rules flag from file" $       testCLISucceeded         ["rewrite", resource "desugar.phi"]@@ -981,6 +1016,18 @@     it "fails to dataize an empty object, which dataizes the terminator ⊥" $       withStdin "[[ ]]" $         testCLIFailed ["dataize"] ["terminator ⊥"]++    it "fails with negative --max-steps" $+      withStdin "[[ D> 01- ]]" $+        testCLIFailed ["dataize", "--max-steps=-1"] ["--max-steps must be positive"]++    -- The 𝕄/𝔻 recursion used to be unbounded, so this division kept morphing+    -- forever and no option could stop it (#1052)+    it "fails on --max-steps instead of morphing forever" $+      withStdin "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧" $+        testCLIFailed+          ["dataize", "--max-steps=40"]+          ["[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=40"]      it "dataizes with --sequence" $       withStdin "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]" $

@@ -12,7 +12,7 @@ import Data.List (find, isInfixOf, nub) import Data.List.NonEmpty (NonEmpty (..)) import Data.Maybe (fromMaybe)-import Dataize (DataizeContext (DataizeContext), dataize, dataize', emptyState, execBuildTerm, morph)+import Dataize (DataizeContext (DataizeContext), Steps (Steps), dataize, dataize', emptyState, execBuildTerm, morph) import Deps (dontSaveStep) import Functions (buildTerm) import Matcher (substEmpty)@@ -26,7 +26,7 @@ -- dataization rules (#909): a hidden overlap surfaces as a nondeterministic -- failure instead of staying silently green. defaultDataizeContext :: Expression -> DataizeContext-defaultDataizeContext loc = DataizeContext loc 25 25 False True buildTerm dontSaveStep+defaultDataizeContext loc = DataizeContext loc 25 25 (Steps 250 0) False True buildTerm dontSaveStep  test :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> String -> DataizeContext -> IO ((a, [Rewritten]), String)) -> [(String, Expression, Expression, a)] -> Spec test func useCases =@@ -270,6 +270,18 @@     failsOn       "throws on a void slot fed a non-absolute argument instead of looping forever"       (ExApplication (ExFormation [BiVoid (AtLabel "x")]) (ArTau (AtLabel "x") (ExDispatch ExXi (AtLabel "foo"))))++  -- '--max-cycles' and '--max-depth' reach only the normalization run inside a+  -- single step, so the 𝕄/𝔻 recursion itself was unbounded: this division, whose+  -- λ-atom keeps re-firing on a term that never reduces to bytes, sent 'morph'+  -- through md → ma → universe → mf → mphi → ml forever and no CLI option could+  -- stop it (#1052). '--max-steps' bounds that recursion and fails once the+  -- budget is gone.+  describe "stops a dataization that never reaches bytes" $+    it "fails on the step limit instead of morphing forever" $ do+      expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧"+      dataize expr (DataizeContext ExRoot 25 25 (Steps 40 0) False True buildTerm dontSaveStep)+        `shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException))    describe "labels every step with a defined rule or operation" $ do     let verb op = case op of