phino 0.0.115 → 0.0.116

raw patch · 26 files changed

+853/−137 lines, 26 filesdep +gitrevPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: gitrev

API changes (from Hackage documentation)

Files

• README.md +93/−33
• phino.cabal +2/−1
• src/Bytes.hs +26/−1
• src/CLI.hs +2/−0
• src/CLI/Helpers.hs +2/−2
• src/CLI/Parsers.hs +45/−3
• src/CLI/Runners.hs +82/−11
• src/CLI/Types.hs +44/−1
• src/CLI/Validators.hs +30/−0
• src/Dataize.hs +45/−20
• src/Filter.hs +17/−10
• src/Functions.hs +6/−2
• src/Random.hs +22/−7
• src/Sugar.hs +1/−1
• src/XMIR.hs +37/−11
• src/Yaml.hs +13/−3
• test/BytesSpec.hs +8/−0
• test/CLIHelpersSpec.hs +7/−2
• test/CLISpec.hs +206/−4
• test/DataizeSpec.hs +88/−22
• test/FilterSpec.hs +9/−1
• test/FunctionsSpec.hs +6/−0
• test/RandomSpec.hs +14/−1
• test/SugarSpec.hs +24/−0
• test/XMIRSpec.hs +8/−1
• test/YamlSpec.hs +16/−0

@@ -34,7 +34,7 @@  ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.114+cabal install --overwrite-policy=always phino-0.0.115 phino --version ``` @@ -166,6 +166,58 @@ that nothing asked for before the run got stuck is left as it is in the residual program, for the next iteration. +The nested morphing and dataization recursion is bounded by the+`--max-steps` option (default `1000`): when the budget is exhausted, the run+fails with `Dataization did not finish before reaching the limit of steps`.+This guards against non-terminating terms, which used to loop forever before+the bound was introduced:++```bash+$ phino dataize --max-steps=50 problem.phi+[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=50+```++## Morph++Dataization insists on bytes. Morphing 𝕄 asks a different question: evaluate+as far as the object model allows, without demanding data. It resolves Φ+against the universe, peels dispatches and applications through+normalization, fires whichever atoms sit under a dispatch, and stops at the+first formation it reaches, handing that formation back untouched. The+`morph` command runs 𝕄 on its own:++```bash+$ cat two.phi+⟦+  bytes(data) ↦ ⟦ φ ↦ data ⟧,+  number(as-bytes) ↦ ⟦ φ ↦ as-bytes, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧,+  φ ↦ 5.plus( 6 ).plus( 7 )+⟧+$ phino dataize --sweet --hide-rho two.phi+40-32-00-00-00-00-00-00+$ phino morph --locator=Q.φ --sweet --hide-rho two.phi+⟦ x ↦ 7, λ ⤍ L_number_plus ⟧+```++The inner `5.plus( 6 )` fires, because `.plus` is dispatched on its result,+and `11` lands in the `ρ` hidden by `--hide-rho`. The outer application is+saturated but bare, so 𝕄 returns it and is finished; firing it is+dataization's job and takes `dataize` on to `18`.++The default locator `Q` morphs the whole top formation, which 𝕄 returns+unchanged, so `--locator` is how one aims 𝕄 at a subterm, exactly as in+`dataize`. Unlike 𝔻, 𝕄 is total: where no formation is reachable the answer+is the terminator `⊥`, printed rather than reported as a failed run:++```bash+$ phino morph --locator=Q.x <<< '⟦ x ↦ ξ ⟧'+⊥+```++The whole `dataize` option surface applies unchanged — `--sequence`,+`--headers`, `--steps-dir`, `--evaluations`, `--partial`, `--max-steps`,+`--shuffle`/`--seed`, `--output`, `--focus` and the rest.+ ## Rewrite  You can rewrite this expression with the help of [rules](#rule-structure)@@ -409,6 +461,12 @@       Expression'        # (an abstraction ⟦…⟧); used by morphing 'md'                          # as 'not (formation 𝑛)', so a non-formation head is                          # morphed and a formation head is left to 'ml'+  | gt:                  # returns True if the first comparable object is+      - Comparable       # greater than the second one+      - Comparable+  | disjoint:            # returns True if none of the given attributes exists+      - [Attribute']     # in the given bindings+      - Binding'  Comparable:              # comparable object that may be used in 'eq' condition   = Attribute'@@ -419,6 +477,8 @@   = Integer              # just regular integer   | IndexMeta'           # 𝑖 (or !i), the index captured by an α𝑖 argument   | length: BiMeta'      # calculate length of bindings by given meta binding+  | domain: BiMeta'      # calculate number of unique attributes in given+                         # meta binding (excluding 'assets')  Extension:               # substitutions extension used to introduce new meta variables   meta: [ExtArgument]    # new introduced meta variable@@ -520,55 +580,55 @@ === parse/phi ===   warmup:     3 iterations   batches:    10 x 1-  total:      1543475.232 μs-  avg:        154347.523 μs-  min:        142171.737 μs-  max:        181971.002 μs-  std dev:    14975.901 μs+  total:      1781621.932 μs+  avg:        178162.193 μs+  min:        163679.993 μs+  max:        209804.570 μs+  std dev:    17409.000 μs === parse/xmir ===   warmup:     3 iterations   batches:    10 x 1-  total:      7819406.638 μs-  avg:        781940.664 μs-  min:        699138.670 μs-  max:        933188.047 μs-  std dev:    65608.137 μs+  total:      7611171.011 μs+  avg:        761117.101 μs+  min:        679176.096 μs+  max:        899930.605 μs+  std dev:    69464.089 μs === rewrite/normalize ===   warmup:     3 iterations   batches:    10 x 1-  total:      651966.123 μs-  avg:        65196.612 μs-  min:        61413.741 μs-  max:        76515.744 μs-  std dev:    4139.047 μs+  total:      811837.328 μs+  avg:        81183.733 μs+  min:        67331.161 μs+  max:        92232.373 μs+  std dev:    8117.233 μs === print/sweet/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      4663282.066 μs-  avg:        466328.207 μs-  min:        449248.604 μs-  max:        488747.559 μs-  std dev:    11022.030 μs+  total:      4199718.146 μs+  avg:        419971.815 μs+  min:        396063.240 μs+  max:        442595.822 μs+  std dev:    16504.492 μs === print/sweet/flat ===   warmup:     3 iterations   batches:    10 x 1-  total:      4595372.700 μs-  avg:        459537.270 μs-  min:        419405.034 μs-  max:        505827.470 μs-  std dev:    27196.223 μs+  total:      4060839.345 μs+  avg:        406083.934 μs+  min:        387257.807 μs+  max:        417907.724 μs+  std dev:    8861.891 μs === print/salty/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      14529614.517 μs-  avg:        1452961.452 μs-  min:        1402771.195 μs-  max:        1489996.347 μs-  std dev:    26769.638 μs+  total:      14257603.693 μs+  avg:        1425760.369 μs+  min:        1405945.748 μs+  max:        1449825.539 μs+  std dev:    11882.320 μs ```  The results were calculated in [this GHA job][benchmark-gha]-on 2026-09-03 at 07:49,+on 2026-09-07 at 19:51, on Linux with 4 CPUs.  <!-- benchmark_end -->@@ -617,4 +677,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/33729718905+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/34156988456

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.115+version: 0.0.116 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>@@ -91,6 +91,7 @@     directory >=1.3.7 && <1.4,     file-embed >=0.0.15 && <0.0.17,     filepath >=1.4.200 && <1.6,+    gitrev >=1.3.1 && <1.4,     megaparsec >=9.5 && <9.9,     optparse-applicative >=0.18 && <0.20,     random >=1.2 && <1.4,

@@ -256,7 +256,15 @@         escapeChar '\t' = "\\t"         escapeChar c           | isPrint c && c /= '\\' && c /= '"' = [c]-          | otherwise = printf "\\x%02x" (ord c)+          | ord c <= 0xFF = printf "\\x%02x" (ord c)+          | ord c <= 0xFFFF = printf "\\u%04x" (ord c)+          | otherwise = surrogates (ord c)+        surrogates :: Int -> String+        surrogates code =+          let rest = code - 0x10000+              high = 0xD800 + rest `div` 0x400+              low = 0xDC00 + rest `mod` 0x400+           in printf "\\u%04x\\u%04x" high low  -- The inverse of the escaping that 'btsToStr' applies, so that a sweet string -- literal can be turned back into the very bytes it was printed from. A@@ -279,11 +287,28 @@   where     go :: String -> String     go "" = ""+    go ('\\' : 'u' : digits) = goUnicode digits     go ('\\' : 'x' : high : low : rest)       | Just code <- hexPair high low = chr code : go rest     go ('\\' : escaped : rest)       | Just unescaped <- lookup escaped escapes = unescaped : go rest     go (char : rest) = char : go rest+    goUnicode :: String -> String+    goUnicode (h1 : h2 : h3 : h4 : rest)+      | Just code <- hexQuad h1 h2 h3 h4 =+          if code >= 0xD800 && code <= 0xDBFF+            then case rest of+              ('\\' : 'u' : l1 : l2 : l3 : l4 : rest')+                | Just low <- hexQuad l1 l2 l3 l4+                , low >= 0xDC00 && low <= 0xDFFF ->+                    chr (0x10000 + (code - 0xD800) * 0x400 + (low - 0xDC00)) : go rest'+              _ -> chr code : go rest+            else chr code : go rest+    goUnicode rest = go rest+    hexQuad :: Char -> Char -> Char -> Char -> Maybe Int+    hexQuad a b c d = case readHex [a, b, c, d] of+      [(code, "")] -> Just code+      _ -> Nothing     hexPair :: Char -> Char -> Maybe Int     hexPair high low = case readHex [high, low] of       [(code, "")] -> Just code

@@ -25,6 +25,7 @@   case _command of     CmdRewrite opts -> runRewrite opts     CmdDataize opts -> runDataize opts+    CmdMorph opts -> runMorph opts     CmdExplain opts -> runExplain opts     CmdMerge opts -> runMerge opts     CmdMatch opts -> runMatch opts@@ -40,6 +41,7 @@       let (level, lns) = case cmd of             CmdRewrite OptsRewrite{_logLevel, _logLines} -> (_logLevel, _logLines)             CmdDataize OptsDataize{_logLevel, _logLines} -> (_logLevel, _logLines)+            CmdMorph OptsMorph{_logLevel, _logLines} -> (_logLevel, _logLines)             CmdExplain OptsExplain{_logLevel, _logLines} -> (_logLevel, _logLines)             CmdMerge OptsMerge{_logLevel, _logLines} -> (_logLevel, _logLines)             CmdMatch OptsMatch{_logLevel, _logLines} -> (_logLevel, _logLines)

@@ -14,7 +14,7 @@ import Control.Monad ((>=>)) import Data.Functor ((<&>)) import Data.IORef-import Data.List (intercalate)+import Data.List (intercalate, nub) import Data.Maybe import Deps (SaveEvalFunc, SaveStepFunc, dontSaveEval, saveEval, saveStep) import Encoding@@ -176,7 +176,7 @@           pure []       | otherwise = do           logDebug (printf "Using rules from files: [%s]" (intercalate ", " rules))-          yamls <- mapM ensuredFile rules+          yamls <- mapM ensuredFile (nub rules)           mapM (Y.yamlRule >=> validateRewriteRule) yamls  -- Pass a user-supplied rewriting rule through unchanged, or fail fast if it

@@ -172,7 +172,7 @@     )  optLocator :: Parser String-optLocator = strOption (long "locator" <> metavar "FQN" <> help "Location of object to dataize. Must be a valid dispatch expression; e.g. Q.foo.bar" <> value "Q" <> showDefault)+optLocator = strOption (long "locator" <> metavar "FQN" <> help "Location of object to rewrite, dataize or morph. Must be a valid dispatch expression; e.g. Q.foo.bar" <> value "Q" <> showDefault)  optFocus :: Parser String optFocus =@@ -203,7 +203,7 @@ optStepsDir = optional (strOption (long "steps-dir" <> metavar "FILE" <> help "Directory to save intermediate steps during rewriting/dataizing"))  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 unknown, or an input of it reaches such an atom), leave it in place and print the residual 𝜑-program instead of bytes")+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 unknown, or an input of it reaches such an atom), leave it in place and print the residual 𝜑-program")  optEvaluations :: Parser (Maybe FilePath) optEvaluations = optional (strOption (long "evaluations" <> metavar "FILE" <> help "File to record every atom fired during dataizing, as one tab-separated line per firing: the λ function name, its argument formation and its result (requires --output=phi)"))@@ -272,6 +272,7 @@             <*> optDataize             <*> optContextualize             <*> optShuffle+            <*> optSeed             <*> optTarget         ) @@ -316,6 +317,47 @@             <*> argInputFile         ) +morphParser :: Parser Command+morphParser =+  CmdMorph+    <$> ( OptsMorph+            <$> optLogLevel+            <*> optLogLines+            <*> optInputFormat+            <*> optOutputFormat+            <*> optSugar+            <*> optHideRho+            <*> optLineFormat+            <*> optOmitListing+            <*> optOmitComments+            <*> optNonumber+            <*> optSequence+            <*> optHeaders+            <*> optCanonize+            <*> optDepthSensitive+            <*> optShuffle+            <*> optSeed+            <*> switch (long "quiet" <> help "Don't print the result of morphing")+            <*> optPartial+            <*> optCompress+            <*> optMaxDepth+            <*> optMaxCycles+            <*> optMaxSteps+            <*> optMargin+            <*> optMeetPopularity+            <*> optMeetLength+            <*> optHide+            <*> optShow+            <*> optLocator+            <*> optFocus+            <*> optExpression+            <*> optLabel+            <*> optMeetPrefix+            <*> optStepsDir+            <*> optEvaluations+            <*> argInputFile+        )+ rewriteParser :: Parser Command rewriteParser =   CmdRewrite@@ -385,7 +427,6 @@             <*> optLogLines             <*> optSugar             <*> optLineFormat-            <*> optSeed             <*> optional (strOption (long "pattern" <> metavar "EXPRESSION" <> help "Pattern expression to match against"))             <*> optional (strOption (long "when" <> metavar "CONDITION" <> help "Predicate for matched substitutions"))             <*> argInputFile@@ -396,6 +437,7 @@   hsubparser     ( command "rewrite" (info rewriteParser (progDesc "Rewrite the 𝜑-expression"))         <> command "dataize" (info dataizeParser (progDesc "Dataize the 𝜑-expression"))+        <> command "morph" (info morphParser (progDesc "Morph the 𝜑-expression"))         <> command "explain" (info explainParser (progDesc "Explain rules in LaTeX format"))         <> command "merge" (info mergeParser (progDesc "Merge 𝜑-expressions into single one by merging their top level formations"))         <> command "match" (info matchParser (progDesc "Match 𝜑-expression against provided pattern and build matched substitutions"))

@@ -27,6 +27,7 @@ import Merge (merge) import Parser (parseExpressionThrows) import qualified Printer as P+import qualified Random as R import Rewriter import Rule (RuleContext (..), matchExpressionWithRule) import System.Directory (doesFileExist, getModificationTime)@@ -45,17 +46,19 @@   included <- validatedDispatches "show" _show   [loc] <- validatedDispatches "locator" [_locator]   [foc] <- validatedDispatches "focus" [_focus]+  validateNoOverlap "show" included "hide" excluded   setStdGen (mkStdGen _seed)   rules <- getRules _normalize _shuffle _rules   validateBreakpoint _breakpoint rules   input <- readInput _inputFile   expr <- parseInput input _inputFormat+  validateXmirTopLevel _outputFormat expr   seedTaus expr   logDebug (printf "Amount of rewriting cycles across all the rules: %d, per rule: %d" _maxCycles _maxDepth)   let listing = case (rules, _inputFormat, _outputFormat) of         ([], XMIR, XMIR) -> (\_ -> escapeXML input)-        ([], _, _) -> const input-        (_, _, _) -> (\rewritten -> P.printExpression' rewritten (_sugarType, UNICODE, _flat, _margin))+        ([], _, _) -> (\_ -> escapeXMLText input)+        (_, _, _) -> (\rewritten -> escapeXMLText (P.printExpression' rewritten (_sugarType, UNICODE, _flat, _margin)))       xmirCtx = XmirContext _omitListing _omitComments listing       printCtx = toPrintCtx xmirCtx foc       exclude = (`F.exclude` excluded)@@ -71,6 +74,7 @@     validateOpts = do       when (_inPlace && isNothing _inputFile) (invalidCLIArguments "The option --in-place requires an input file")       when (_inPlace && isJust _targetFile) (invalidCLIArguments "The options --in-place and --target cannot be used together")+      when (_inPlace && _outputFormat /= PHI) (invalidCLIArguments "The option --in-place can only be used together with --output=phi")       when (_update && _inPlace) (invalidCLIArguments "The options --update and --in-place cannot be used together")       when (_update && isNothing _targetFile) (invalidCLIArguments "The option --update requires --target")       when (_update && isNothing _inputFile) (invalidCLIArguments "The option --update requires an input file")@@ -142,6 +146,7 @@   included <- validatedDispatches "show" _show   [loc] <- validatedDispatches "locator" [_locator]   [foc] <- validatedDispatches "focus" [_focus]+  validateNoOverlap "show" included "hide" excluded   input <- readInput _inputFile   expr <- parseInput input _inputFormat   setStdGen (mkStdGen _seed)@@ -197,22 +202,89 @@         _meetPrefix         _outputFormat +-- Run 𝕄 on its own, the way 'runDataize' runs 𝔻. The whole option surface of+-- 'dataize' applies unchanged, since the two commands differ only in the+-- judgment they run; what differs here is the answer printed: 𝕄 is total and+-- always hands back a 𝜑-expression — a formation, or the terminator ⊥ where no+-- formation is reachable — so there are no bytes to print and no failure to+-- report where 𝔻 would give up.+runMorph :: OptsMorph -> IO ()+runMorph OptsMorph{..} = do+  validateOpts+  excluded <- validatedDispatches "hide" _hide+  included <- validatedDispatches "show" _show+  [loc] <- validatedDispatches "locator" [_locator]+  [foc] <- validatedDispatches "focus" [_focus]+  validateNoOverlap "show" included "hide" excluded+  input <- readInput _inputFile+  expr <- parseInput input _inputFormat+  setStdGen (mkStdGen _seed)+  seedTaus expr+  let printCtx = toPrintCtx foc+      exclude = (`F.exclude` excluded)+      include = (`F.include` included)+  save <- saveStepFunc _stepsDir printCtx+  (morphed, chain) <-+    withEvalFunc _evaluations printCtx $+      morph expr . DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial buildTerm save+  when _sequence (printRewrittens printCtx (exclude $ include chain, False) >>= putStrLn)+  unless _quiet (printFocused printCtx morphed >>= putStrLn)+  where+    validateOpts :: IO ()+    validateOpts = do+      validateLatexOptions+        _outputFormat+        [(_nonumber, "nonumber"), (_compress, "compress")]+        [(_expression, "expression"), (_label, "label"), (_meetPrefix, "meet-prefix")]+        [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]+      validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus+      when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")+      when+        (isJust _evaluations && _outputFormat /= PHI)+        (invalidCLIArguments "The --evaluations option can stay together with --output=phi only, since one record must fit into one line")+    toPrintCtx :: Expression -> PrintContext+    toPrintCtx focus =+      PrintCtx+        _sugarType+        _hideRho+        _flat+        _margin+        defaultXmirContext+        _nonumber+        _compress+        _canonize+        _sequence+        _headers+        (justMeetPopularity _meetPopularity)+        (justMeetLength _meetLength)+        focus+        _expression+        _label+        _meetPrefix+        _outputFormat+ runExplain :: OptsExplain -> IO () runExplain OptsExplain{..} = do+  setStdGen (mkStdGen _seed)   validateOpts   explained >>= printOut _targetFile   where     explained :: IO String     explained-      | _morph = pure (explainMorphRules Y.morphingRules)-      | _dataize = pure (explainDataizeRules Y.dataizationRules)-      | _contextualize = pure (explainContextualizeRules Y.contextualizationRules)+      | _morph = explainMorphRules <$> shuffled Y.morphingRules+      | _dataize = explainDataizeRules <$> shuffled Y.dataizationRules+      | _contextualize = explainContextualizeRules <$> shuffled Y.contextualizationRules       | otherwise = explainRules <$> getRules _normalize _shuffle _rules+    shuffled :: [a] -> IO [a]+    shuffled xs+      | _shuffle = R.shuffle xs+      | otherwise = pure xs     validateOpts :: IO ()     validateOpts = do-      let selected = length (filter id [not (null _rules), _normalize, _morph, _dataize, _contextualize])-      when (selected == 0) (invalidCLIArguments "Either --rule, --normalize, --morph, --dataize or --contextualize must be specified")-      when (selected > 1) (invalidCLIArguments "Only one of --rule, --normalize, --morph, --dataize or --contextualize can be specified")+      let selected = length (filter id [_morph, _dataize, _contextualize])+      when (selected == 0 && null _rules && not _normalize) (invalidCLIArguments "Either --rule, --normalize, --morph, --dataize or --contextualize must be specified")+      when (selected > 1) (invalidCLIArguments "Only one of --morph, --dataize or --contextualize can be specified")+      when (selected == 1 && not (null _rules)) (invalidCLIArguments "The --rule option cannot be used together with --morph, --dataize or --contextualize")  runMerge :: OptsMerge -> IO () runMerge OptsMerge{..} = do@@ -220,7 +292,8 @@   inputs' <- traverse (readInput . Just) _inputs   exprs <- traverse (`parseInput` _inputFormat) inputs'   expr <- merge exprs-  let listing = const (P.printExpression' expr (_sugarType, UNICODE, _flat, _margin))+  validateXmirTopLevel _outputFormat expr+  let listing = const (escapeXMLText (P.printExpression' expr (_sugarType, UNICODE, _flat, _margin)))       xmirCtx = XmirContext _omitListing _omitComments listing       printCtx = toPrintCtx xmirCtx   expr' <- printInFormat printCtx expr@@ -255,8 +328,6 @@ runMatch OptsMatch{..} = do   input <- readInput _inputFile   expr <- parseInput input PHI-  setStdGen (mkStdGen _seed)-  seedTaus expr   if isNothing _pattern     then logDebug "The --pattern is not provided, no substitutions are built"     else do

@@ -56,6 +56,7 @@ data Command   = CmdRewrite OptsRewrite   | CmdDataize OptsDataize+  | CmdMorph OptsMorph   | CmdExplain OptsExplain   | CmdMerge OptsMerge   | CmdMatch OptsMatch@@ -111,6 +112,48 @@   , _inputFile :: Maybe FilePath   } +-- The option surface of 'morph' is that of 'dataize': the two commands read the+-- same input, aim the same '_locator' at the same subterm and print through the+-- same formatting flags, differing only in the judgment they run — 𝕄, which+-- stops at the first formation it reaches, against 𝔻, which insists on bytes.+data OptsMorph = OptsMorph+  { _logLevel :: LogLevel+  , _logLines :: Int+  , _inputFormat :: IOFormat+  , _outputFormat :: IOFormat+  , _sugarType :: SugarType+  , _hideRho :: Bool+  , _flat :: LineFormat+  , _omitListing :: Bool+  , _omitComments :: Bool+  , _nonumber :: Bool+  , _sequence :: Bool+  , _headers :: Bool+  , _canonize :: Bool+  , _depthSensitive :: Bool+  , _shuffle :: Bool+  , _seed :: Int+  , _quiet :: Bool+  , _partial :: Bool+  , _compress :: Bool+  , _maxDepth :: Int+  , _maxCycles :: Int+  , _maxSteps :: Int+  , _margin :: Int+  , _meetPopularity :: Maybe Int+  , _meetLength :: Maybe Int+  , _hide :: [String]+  , _show :: [String]+  , _locator :: String+  , _focus :: String+  , _expression :: Maybe String+  , _label :: Maybe String+  , _meetPrefix :: Maybe String+  , _stepsDir :: Maybe FilePath+  , _evaluations :: Maybe FilePath+  , _inputFile :: Maybe FilePath+  }+ data OptsExplain = OptsExplain   { _logLevel :: LogLevel   , _logLines :: Int@@ -120,6 +163,7 @@   , _dataize :: Bool   , _contextualize :: Bool   , _shuffle :: Bool+  , _seed :: Int   , _targetFile :: Maybe FilePath   } @@ -183,7 +227,6 @@   , _logLines :: Int   , _sugarType :: SugarType   , _flat :: LineFormat-  , _seed :: Int   , _pattern :: Maybe String   , _when :: Maybe String   , _inputFile :: Maybe FilePath

@@ -35,6 +35,22 @@                 (printExpression' expr logPrintConfig)             ) +-- Reject a --show locator that is also hidden via --hide: 'exclude' runs over+-- the result of 'include', so an overlap would silently wipe the very subtree+-- --show was meant to keep.+validateNoOverlap :: String -> [Expression] -> String -> [Expression] -> IO ()+validateNoOverlap showOpt shown hideOpt hidden =+  for_ shown $ \shown' ->+    for_ hidden $ \hidden' ->+      when (printExpression shown' == printExpression hidden') $+        invalidCLIArguments+          ( printf+              "The --%s locator '%s' is also listed in --%s, which would hide it from the result"+              showOpt+              (printExpression shown')+              hideOpt+          )+ -- Validate LaTeX options validateLatexOptions :: IOFormat -> [(Bool, String)] -> [(Maybe String, String)] -> [(Maybe Int, String)] -> IO () validateLatexOptions LATEX _ _ _ = pure ()@@ -57,6 +73,20 @@ validateXmirOptions _ bools _ =   let (bools', opts) = unzip bools    in validateBoolOpts (zip bools' (map (printf "The --%s can be used only with --output=xmir") opts))++-- Check that an expression is printable as XMIR: its top level must be a+-- single binding followed by ρ ↦ ∅ (the shape 'expressionToXMIR' accepts).+-- Called right after parsing, so a bad shape fails before any rewriting or+-- dataization work instead of at print time (issue #1082).+validateXmirTopLevel :: IOFormat -> Expression -> IO ()+validateXmirTopLevel XMIR (ExFormation [_, BiVoid AtRho]) = pure ()+validateXmirTopLevel XMIR expr =+  invalidCLIArguments+    ( printf+        "Expression cannot be printed with --output=xmir: its top level must be a single binding followed by ρ ↦ ∅, but got: %s"+        (printExpression expr)+    )+validateXmirTopLevel _ _ = pure ()  validateBoolOpts :: [(Bool, String)] -> IO () validateBoolOpts bools = forM_ bools (\(bool, msg) -> when bool (invalidCLIArguments msg))

@@ -10,7 +10,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Dataize (morph, dataize, dataize', DataizeContext (..), DataizeException (..), Outcome (..), Steps (..), State, emptyState, execBuildTerm) where+module Dataize (morph, morph', dataize, dataize', DataizeContext (..), DataizeException (..), Outcome (..), Steps (..), State, emptyState, execBuildTerm) where  import AST import Builder (buildBytesThrows, buildExpressionThrows)@@ -64,7 +64,7 @@ -- 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+-- '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.@@ -181,8 +181,8 @@ -- argument and its individual steps (alpha, copy, dot, …) are spliced into the -- chain before morphing continues. Every other premise is a side-computation -- evaluated in isolation by 'sidePremise', its own steps discarded.-morph :: Morphed -> Expression -> State -> DataizeContext -> IO (Morphed, State)-morph (expr, seq) univ state caller = do+morph' :: Morphed -> Expression -> State -> DataizeContext -> IO (Morphed, State)+morph' (expr, seq) univ state caller = do   ctx <- deeper caller   parking seq $ do     rules <- if ctx._shuffle then shuffle Y.morphingRules else pure Y.morphingRules@@ -222,16 +222,40 @@           built <- buildExpressionThrows inner final           labelled <- leadsTo seq rule.name built ctx           (normal', seq') <- normalized built labelled ctx-          morph (normal', seq') univ state' ctx+          morph' (normal', seq') univ state' ctx         _ -> do           (final, state') <- sides ctx (rule.premises `excluding` [concl]) subst           built <- buildExpressionThrows arg final           seq' <- leadsTo seq rule.name built ctx-          morph (built, seq') univ state' ctx+          morph' (built, seq') univ state' ctx       Just _ -> throwIO (userError (printf "morphing rule '%s' must conclude with a 'morph' premise" rule.name))     sides :: DataizeContext -> [Y.Premise] -> Subst -> IO (Subst, State)     sides ctx premises subst = foldM (sidePremise univ ctx) (subst, state) premises +-- Morph the expression located at '_locator' — 𝕄 asked on its own, the way+-- 'dataize' asks 𝔻. The whole input expression is itself the universe Φ (the 'e'+-- argument) threaded through 𝕄, so it is passed both as the located target and+-- as the universe; the default locator Q therefore morphs the top formation,+-- which 'mf' hands back unchanged, and '_locator' is how one aims 𝕄 at a+-- subterm. Unlike 𝔻, 𝕄 is total: it stops at the first formation it reaches+-- ('mf') and never demands bytes, and where no formation is reachable it answers+-- with the terminator ⊥ ('dead', 'xi', 'mg', 'mad', 'maad') rather than failing.+-- Only the atoms 'ml' fires can still get stuck, and '_partial' parks them just+-- as it does under 𝔻: the answer is then the residual subterm the spine had+-- reached, taken from '_locator' of its working expression.+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))+    Left (StuckAt _ seq) | _partial -> do+      residue <- locatedExpression _locator (fst (NE.head seq))+      pure (residue, reverse (NE.toList seq))+    Left failure -> throwIO (failure :: DataizeException)+ -- Dataize the expression located at '_locator'. The whole input expression is -- itself the universe Q (the 'e' argument) threaded through 𝔻 and 𝕄, so it is -- passed both as the located target and as the universe. An atom that cannot@@ -320,7 +344,7 @@         Just morphed@(Y.Premise _ (Y.OpMorph inner)) -> do           (final, state') <- sides ctx (rule.premises `excluding` [concl, morphed]) subst           built <- buildExpressionThrows inner final-          ((morphed', seq'), state'') <- morph (built, seq) univ state' ctx+          ((morphed', seq'), state'') <- morph' (built, seq) univ state' ctx           dataize' (morphed', seq') univ state'' ctx         -- The dataize argument is produced with no 'normalize'/'morph' spine to         -- splice: 'fire' by its 'evaluate' side-computation (𝔼 now yields a@@ -457,10 +481,12 @@  -- A number atom only operates on numeric data. Empty bytes — a genuine -- zero-length byte array ⟦Δ ⤍ --⟧ — carry no number, so the operand is rejected--- and the atom yields ⊥.+-- and the atom yields ⊥. So does any byte array whose length is not 8: 'btsToNum'+-- throws on such arrays, so the size is checked up front, exactly like 'asInt'. asNumber :: Bytes -> Maybe Double-asNumber BtEmpty = Nothing-asNumber bts = Just (either toDouble id (btsToNum bts))+asNumber bts+  | btsSize bts /= 8 = Nothing+  | otherwise = Just (either toDouble id (btsToNum bts))  -- An operand that EO reads as a Java 'int' — a shift distance or a slice bound. -- 'Expect.at(…).that(Integer)' turns down anything but a whole number inside the@@ -485,6 +511,14 @@   (rho, rstate) <- _dataize (ExDispatch self AtRho) univ bstate ctx   pure (maybe ExTermination dataBytes (op rho b), rstate) +-- The 12 primitive λ-atoms every EO data operation reduces to. phino mirrors+-- EO's set exactly: bytes {and, concat, eq, not, or, right, size, slice} and+-- number {div, gt, plus, times}. There is deliberately no 'L_number_eq': EO's+-- 'number.eq' (eo-runtime/src/main/eo/number/eq.eo) is pure EO — a formation+-- composing 'is-nan', 'or', 'and' and 'L_bytes_eq', with no λ of its own — so+-- nothing is left for a phino atom to implement. Names like 'L_bool_if' or+-- 'L_string_slice' must stay unimplemented too: the EO lowering declares them+-- precisely so that '--partial' parks on them and renders the call to Java. atom :: T.Text -> Expression -> Expression -> State -> DataizeContext -> IO (Expression, State) atom "L_number_plus" self univ state ctx = do   (left, lstate) <- _dataize (ExDispatch self (AtLabel "x")) univ state ctx@@ -498,15 +532,6 @@   case (asNumber left, asNumber right) of     (Just first, Just second) -> pure (DataNumber (numToBts (first * second)), rstate)     _ -> pure (ExTermination, rstate)-atom "L_number_eq" self univ state ctx = do-  (x, lstate) <- _dataize (ExDispatch self (AtLabel "x")) univ state ctx-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ lstate ctx-  case (asNumber x, asNumber rho) of-    (Just first, Just self') ->-      if self' == first-        then pure (DataNumber (numToBts first), rstate)-        else pure (ExDispatch self (AtLabel "y"), rstate)-    _ -> pure (ExTermination, rstate) atom "L_number_div" self univ state ctx = do   (x, xstate) <- _dataize (ExDispatch self (AtLabel "x")) univ state ctx   (rho, rstate) <- _dataize (ExDispatch self AtRho) univ xstate ctx@@ -622,6 +647,6 @@ _morph :: Expression -> DataizeContext -> State -> BuildTermMethodS _morph univ ctx state [ArgExpression expr] subst = unparked $ do   built <- buildExpressionThrows expr subst-  ((morphed, _), state') <- morph (built, (univ, Nothing) :| []) univ state ctx+  ((morphed, _), state') <- morph' (built, (univ, Nothing) :| []) univ state ctx   pure (TeExpression morphed, state') _morph _ _ _ _ _ = throwIO (userError "Function morph() requires exactly 1 expression argument")

@@ -4,6 +4,7 @@ module Filter (include, exclude) where  import AST+import Data.Maybe (mapMaybe) import Misc import Rewriter @@ -31,15 +32,22 @@ exclude rs [] = rs exclude ((expr, maybeRule) : rest) exprs = (exclude' expr exprs, maybeRule) : exclude rest exprs -include' :: Expression -> Expression -> Expression-include' ex@(ExFormation _) fqn =-  let def = ExFormation [BiVoid AtRho]-   in case fqnToAttrs fqn of-        Just fqn' -> case includedFormation ex fqn' of-          Just e -> e-          _ -> def-        _ -> def+include' :: Expression -> [Expression] -> Expression+include' expr fqns = case mapMaybe pick fqns of+  [] -> def+  forms -> mergeForms forms   where+    def :: Expression+    def = ExFormation [BiVoid AtRho]+    pick :: Expression -> Maybe Expression+    pick fqn = do+      attrs <- fqnToAttrs fqn+      includedFormation expr attrs+    mergeForms :: [Expression] -> Expression+    mergeForms forms =+      let bds = concat [bs | ExFormation bs <- forms]+          bds' = filter (\bd -> attributeFromBinding bd /= Just AtRho) bds+       in ExFormation (withVoidRho bds')     includedFormation :: Expression -> [Attribute] -> Maybe Expression     includedFormation (ExFormation bindings) [at] =       let bs = [bd | bd <- bindings, attributeFromBinding bd == Just at]@@ -52,9 +60,8 @@           | otherwise = includedBindings bs as         includedBindings _ _ = Nothing     includedFormation _ _ = Nothing-include' _ _ = ExFormation [BiVoid AtRho]  include :: [Rewritten] -> [Expression] -> [Rewritten] include [] _ = [] include rs [] = rs-include ((expr, maybeRule) : rest) (fqn : _) = (include' expr fqn, maybeRule) : include rest [fqn]+include ((expr, maybeRule) : rest) exprs = (include' expr exprs, maybeRule) : include rest exprs

@@ -7,7 +7,7 @@  import AST import Builder-import Bytes (btsToNum, btsToUnescapedStr, numToBts, strToBts)+import Bytes (btsSize, btsToNum, btsToUnescapedStr, numToBts, strToBts) import Control.Exception (throwIO) import Control.Monad (when) import qualified Data.ByteString.Char8 as B@@ -63,7 +63,11 @@ argToString arg subst = argToBytes arg subst <&> btsToUnescapedStr  argToNumber :: Y.ExtraArgument -> Subst -> IO Double-argToNumber arg subst = argToBytes arg subst <&> either toDouble id . btsToNum+argToNumber arg subst = do+  bts <- argToBytes arg subst+  case btsSize bts of+    8 -> pure (either toDouble id (btsToNum bts))+    _ -> throwIO (userError (printf "Expected 8 bytes for a number, got %d" (btsSize bts)))  _contextualize :: BuildTermMethod _contextualize [Y.ArgExpression expr, Y.ArgExpression context] subst = do

@@ -3,6 +3,7 @@  module Random (randomString, shuffle) where +import Control.Exception (throwIO) import Control.Monad (forM_, replicateM) import Data.Char (intToDigit) import Data.IORef (IORef, modifyIORef', newIORef, readIORef)@@ -34,14 +35,28 @@   rest' <- generate rest   pure (ch : rest') +-- The 'strings' set grows monotonically over a process, so a pattern with a+-- bounded space (e.g. '%d', which has exactly 10,000 values) eventually gets+-- exhausted. Trying again forever would hang, so the search gives up after a+-- bounded number of attempts and reports the collision space instead. The+-- limit is well above the largest realistic space (10,000) so that finding the+-- last free value of a nearly-full space still succeeds with overwhelming+-- probability: (9999/10000)^100000 ≈ 4.5e-5.+maxAttempts :: Int+maxAttempts = 100000+ regenerate :: String -> Set String -> IO String-regenerate pat set = do-  next <- generate pat-  if next `Set.member` set-    then regenerate pat set-    else do-      modifyIORef' strings (Set.insert next)-      pure next+regenerate pat set = go maxAttempts+  where+    go :: Int -> IO String+    go 0 = throwIO (userError (printf "randomString() cannot produce a unique value for pattern '%s': the value space is exhausted" pat))+    go attempts = do+      next <- generate pat+      if next `Set.member` set+        then go (attempts - 1)+        else do+          modifyIORef' strings (Set.insert next)+          pure next  randomString :: String -> IO String randomString pat

@@ -260,7 +260,7 @@       joinToBindings :: [ATTRIBUTE] -> BINDING -> BINDINGS       joinToBindings [] BI_EMPTY{..} = BDS_EMPTY tab       joinToBindings [] BI_PAIR{..} = BDS_PAIR eol tab pair bindings-      joinToBindings [] BI_META{} = error "BI_META unexpected in joinToBindings"+      joinToBindings [] BI_META{..} = BDS_META eol tab meta bindings       joinToBindings (attr : rest) bd = BDS_PAIR eol tab (PA_VOID attr arrow EMPTY) (joinToBindings rest bd)   toSalty pair = pair 

@@ -2,6 +2,7 @@ {-# LANGUAGE NumericUnderscores #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TemplateHaskell #-}  -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT@@ -15,6 +16,7 @@   , xmirToPhi   , defaultXmirContext   , escapeXML+  , escapeXMLText   , XmirContext (XmirContext)   ) where@@ -30,10 +32,11 @@ import qualified Data.Text as T import qualified Data.Text.Lazy as TL import qualified Data.Text.Lazy.Builder as TB-import Data.Time (UTCTime, getCurrentTime)+import Data.Time (UTCTime, diffUTCTime, getCurrentTime) import Data.Time.Clock.POSIX (utcTimeToPOSIXSeconds) import Data.Time.Format (defaultTimeLocale, formatTime) import Data.Version (showVersion)+import Development.GitRev (gitHash) import Misc import Paths_phino (version) import Printer@@ -48,6 +51,12 @@   , _listing :: Expression -> String   } +-- The 7-character Git SHA of the phino build that produced the document,+-- matching the XMIR schema pattern [0-9a-f]{7}. When built outside a git+-- checkout gitrev yields "UNKNOWN", which the schema allows us to omit.+gitRevision :: String+gitRevision = take 7 $(gitHash)+ defaultXmirContext :: XmirContext defaultXmirContext = XmirContext True True (const "") @@ -176,6 +185,7 @@   where     expressionToXMIR' :: IO Document     expressionToXMIR' = do+      started <- getCurrentTime       (pckg, expr') <- getPackage expr       root <- rootExpression expr' ctx       now <- getCurrentTime@@ -186,20 +196,25 @@               else text           listing' = NodeElement (element "listing" [] [NodeContent (T.pack listing)])           metas = metasWithPackage (intercalate "." pckg)+          ms :: Int+          ms = round (diffUTCTime now started * 1000)+          revisionAttr = [("revision", gitRevision) | gitRevision /= "UNKNOWN"]+          attrs =+            [ ("author", "phino")+            , ("dob", formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" now)+            , ("ms", show ms)+            , ("time", time now)+            , ("version", showVersion version)+            , ("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance")+            , ("xsi:noNamespaceSchemaLocation", "https://raw.githubusercontent.com/objectionary/eo/refs/heads/gh-pages/XMIR.xsd")+            ]+              <> revisionAttr       pure         ( Document             (Prologue [] Nothing [])             ( element                 "object"-                [ ("author", "phino")-                , ("dob", formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" now)-                , ("ms", "0")-                , ("revision", "1234567")-                , ("time", time now)-                , ("version", showVersion version)-                , ("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance")-                , ("xsi:noNamespaceSchemaLocation", "https://raw.githubusercontent.com/objectionary/eo/refs/heads/gh-pages/XMIR.xsd")-                ]+                attrs                 ( if null pckg                     then [listing', root]                     else [listing', metas, root]@@ -273,6 +288,17 @@     escapeChar '\'' = "&apos;"     escapeChar ch = [ch] +-- Escape just the characters that are mandatory in XML text content ('&' and+-- '<'); '>' and the quotes are optional there and staying literal keeps the+-- content readable, e.g. the '->' arrow inside a <listing>.+escapeXMLText :: String -> String+escapeXMLText = concatMap escapeChar+  where+    escapeChar :: Char -> String+    escapeChar '&' = "&amp;"+    escapeChar '<' = "&lt;"+    escapeChar ch = [ch]+ -- Add indentation (2 spaces per level). indent :: Int -> TB.Builder indent n = TB.fromText (T.replicate n (T.pack "  "))@@ -322,7 +348,7 @@   where     attrsText =       mconcat-        [ TB.fromString " " <> TB.fromText (nameLocalName k) <> TB.fromString "=\"" <> TB.fromText v <> TB.fromString "\""+        [ TB.fromString " " <> TB.fromText (nameLocalName k) <> TB.fromString "=\"" <> TB.fromText (T.pack (escapeXML (T.unpack v))) <> TB.fromString "\""         | (k, v) <- M.toList attrs         ] 

@@ -77,7 +77,9 @@         [ Length <$> o .: "length"         , Domain <$> o .: "domain"         ]-    Number num -> pure (Literal (round num))+    Number num+      | toRational (round num :: Integer) == toRational num -> pure (Literal (round num))+      | otherwise -> fail (printf "Expected an integer, got a fractional number %s" (show num))     String txt -> case parseIndex (unpack txt) of       Right mt -> pure (MetaIndex mt)       Left err -> fail err@@ -99,8 +101,16 @@       ( \v -> do           validateYamlObject v ["and", "or", "not", "nf", "absolute", "eq", "gt", "in", "matches", "part-of", "disjoint", "formation"]           asum-            [ And <$> v .: "and"-            , Or <$> v .: "or"+            [ do+                conds <- v .: "and"+                if null conds+                  then fail "The 'and' condition requires at least one element"+                  else pure (And conds)+            , do+                conds <- v .: "or"+                if null conds+                  then fail "The 'or' condition requires at least one element"+                  else pure (Or conds)             , Not <$> v .: "not"             , NF <$> v .: "nf"             , Absolute <$> v .: "absolute"

@@ -126,6 +126,8 @@       , ("escapes newline", BtOne "0A", "\\n")       , ("escapes tab", BtOne "09", "\\t")       , ("escapes non-printable", BtOne "01", "\\x01")+      , ("escapes a non-printable above U+00FF as \\u", BtMany ["61", "E2", "80", "A8", "7A"], "a\\u2028z")+      , ("keeps a printable emoji above U+FFFF as is", BtMany ["F0", "9F", "98", "80"], "\x1F600")       , ("mixed printable and quote", BtMany ["61", "22", "62"], "a\\\"b")       ]       ( \(desc, bts, str) ->@@ -146,6 +148,9 @@       , ("unknown escape is kept as it stands", "\\q", "\\q")       , ("trailing backslash is kept", "a\\", "a\\")       , ("truncated hex escape is kept", "\\x0", "\\x0")+      , ("unicode escape", "a\\u2028z", "a\x2028z")+      , ("uppercase unicode escape", "\\u2028", "\x2028")+      , ("surrogate pair", "\\uD83D\\uDE00", "\x1F600")       ]       ( \(desc, escaped, unescaped) ->           it desc $ unescapeStr escaped `shouldBe` unescaped@@ -161,6 +166,9 @@       , ("tab", BtOne "09")       , ("non-printable", BtMany ["01", "02"])       , ("text around a newline", BtMany ["65", "0A", "65"])+      , ("text around a line separator", BtMany ["61", "E2", "80", "A8", "7A"])+      , ("text around a paragraph separator", BtMany ["61", "E2", "80", "A9", "7A"])+      , ("emoji above U+FFFF", BtMany ["F0", "9F", "98", "80"])       ]       ( \(desc, bts) ->           it desc $ strToBts (unescapeStr (btsToStr bts)) `shouldBe` bts

@@ -12,13 +12,13 @@ module CLIHelpersSpec (spec) where  import AST (Expression (ExRoot))-import CLI.Helpers (parseInput, printExpression)+import CLI.Helpers (getRules, parseInput, printExpression) import CLI.Types (IOFormat (LATEX, PHI, XMIR), PrintContext (PrintCtx)) import Control.Exception (SomeException, try) import Control.Monad (forM_) import Lining (LineFormat (MULTILINE)) import Sugar (SugarType (SWEET))-import Test.Hspec (Spec, describe, it, shouldSatisfy)+import Test.Hspec (Spec, describe, it, shouldBe, shouldSatisfy) import XMIR (defaultXmirContext)  isLeft :: Either e a -> Bool@@ -50,3 +50,8 @@           result <- try (printExpression (testPrintContext format) ExRoot) :: IO (Either SomeException String)           result `shouldSatisfy` predicate       )++  describe "getRules" $+    it "deduplicates the same --rule file listed twice" $ do+      rules <- getRules False False ["test-resources/cli/simple.yaml", "test-resources/cli/simple.yaml"]+      length rules `shouldBe` 1

@@ -10,7 +10,8 @@ import CLI.Types (CmdException (..), IOFormat (..)) import Control.Exception import Control.Monad (forM_, unless)-import Data.List (intercalate, isInfixOf, sort)+import Data.Char (isDigit)+import Data.List (intercalate, isInfixOf, isPrefixOf, sort) import Data.Time.Clock (addUTCTime, getCurrentTime) import Data.Time.Clock.POSIX (getPOSIXTime) import Data.Version (showVersion)@@ -215,6 +216,12 @@           , ["it's expected rewriting cycles to be in range [1], but rewriting has already reached 2"]           )         , ("when --in-place is used without input file", "[[ ]]", ["rewrite", "--in-place"], ["--in-place requires an input file"])+        ,+          ( "with --output=xmir on a non-top-level expression"+          , "⟦ x ↦ 1, ρ ↦ 2 ⟧"+          , ["rewrite", "--output=xmir"]+          , ["[ERROR]:", "its top level must be a single binding followed by ρ ↦ ∅"]+          )         ]         (\(desc, input, args, expected) -> it desc (withStdin input (testCLIFailed args expected))) @@ -226,6 +233,14 @@             ["rewrite", "--in-place", "--target=output.phi", path]             ["--in-place and --target cannot be used together"] +      it "fails when --in-place is used with a non-phi output format" $+        withTempFile "inplaceXXXXXX.phi" $ \(path, h) -> do+          hPutStr h "[[ ]]"+          hClose h+          testCLIFailed+            ["rewrite", "--in-place", "--output=latex", path]+            ["--in-place can only be used together with --output=phi"]+       forM_         [ ("when --update is used without --target", "[[ ]]", ["rewrite", "--update"], ["--update requires --target"])         ,@@ -306,6 +321,7 @@           , ["rewrite", "--show=Q.x(Q.y)"]           , ["[ERROR]:", "Only dispatch expression started with Φ (or Q) can be used in --show"]           )+        , ("with --show overlapping --hide", ["rewrite", "--show=Q.x", "--hide=Q.x"], ["[ERROR]:", "The --show locator 'Φ.x' is also listed in --hide"])         , ("with --meet-popularity < 0", ["rewrite", "--meet-popularity=-1"], ["[ERROR]:", "--meet-popularity must be positive"])         , ("with --meet-popularity > 100", ["rewrite", "--meet-popularity=102"], ["[ERROR]:", "--meet-popularity must be <= 100"])         ,@@ -481,6 +497,25 @@           ["rewrite", "--output=xmir"]           ["<?xml version=\"1.0\" encoding=\"UTF-8\"?>", "<object", "  <o base=\"Φ.y\" name=\"x\"/>"] +    it "emits a real revision and ms in XMIR" $ do+      (output, _) <- withStdin "[[ x -> Q.y ]]" $ withStdout (runCLI ["rewrite", "--output=xmir"])+      let attrValue :: String -> String -> String+          attrValue name text =+            let needle = name ++ "=\""+                breakOn :: String -> Maybe String+                breakOn haystack+                  | needle `isPrefixOf` haystack = Just (drop (length needle) haystack)+                  | null haystack = Nothing+                  | otherwise = breakOn (drop 1 haystack)+             in case breakOn text of+                  Just afterNeedle -> takeWhile (/= '"') afterNeedle+                  Nothing -> ""+          revision = attrValue "revision" output+          ms = attrValue "ms" output+      revision `shouldSatisfy` (\sha -> length sha == 7 && all (`elem` "0123456789abcdef") sha)+      revision `shouldNotBe` "1234567"+      ms `shouldSatisfy` (all isDigit)+     it "rewrites as LaTeX" $       withStdin "[[ x_o -> Q.z(y -> 5), q$ -> T, w -> $, ^ -> Q, @ -> 1, y -> \"H$@^M\", L> Fu_nc ]]" $         testCLISucceeded@@ -1256,6 +1291,146 @@       withStdin "[[ D> 01- ]]" $         testCLISucceeded ["dataize", "--depth-sensitive"] ["01-"] +  -- 𝕄 was reachable only from inside 𝔻, through the 'norm' rule of the+  -- dataization relation, so there was no way to ask phino for 𝕄(n, Φ) on its+  -- own (#1114)+  describe "morph" $ do+    -- Two chained atom calls: the inner one fires under 'ml', because '.plus'+    -- is dispatched on its result, while the outer application is saturated but+    -- bare, so 'mf' hands it back and firing it is 𝔻's job+    let chained = "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]"+    it "prints help" $+      testCLISucceeded ["morph", "--help"] ["Morph the 𝜑-expression"]++    it "hands the top formation back untouched under the default locator" $+      withStdin "[[ D> 01- ]]" $+        testCLISucceeded ["morph", "--flat", "--hide-rho"] ["⟦ Δ ⤍ 01- ⟧"]++    it "stops at the bare saturated λ-formation" $+      withStdin chained $+        testCLISucceeded+          ["morph", "--locator=Q.@", "--sweet", "--hide-rho", "--flat"]+          ["⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"]++    -- The same term under 𝔻, which insists on bytes and fires what 𝕄 left bare+    it "leaves to dataize the firing that takes the same term to bytes" $+      withStdin chained $+        testCLISucceeded ["dataize"] ["40-32-00-00-00-00-00-00"]++    -- 'mf' hands a formation back as it is, so '--locator' is how one aims 𝕄 at+    -- a subterm worth navigating: here it resolves Φ against the universe and+    -- peels the dispatch through 𝒩+    it "morphs the subterm --locator aims at" $+      withStdin "[[ ex -> Q.x, x -> [[ D> 42- ]] ]]" $+        testCLISucceeded ["morph", "--locator=Q.ex", "--flat", "--hide-rho"] ["⟦ Δ ⤍ 42- ⟧"]++    -- 𝕄 is total and 𝔻 is not: where the derivation dies, 𝕄 answers ⊥ ('xi'+    -- here) and the run succeeds, while 𝔻 has no bytes to give and fails+    it "prints ⊥ instead of failing the run" $+      withStdin "[[ x -> $ ]]" $+        testCLISucceeded ["morph", "--locator=Q.x"] ["⊥"]++    it "fails to dataize what it morphs to ⊥" $+      withStdin "[[ x -> $ ]]" $+        testCLIFailed ["dataize", "--locator=Q.x"] ["terminator ⊥"]++    -- The chain carries the spine: the morphing rules that reduced the term+    -- ('maa', then the terminal 'mf') with the normalization steps they spliced+    -- in ('alpha', 'copy'). The 'ml' firing of the inner call is not there by+    -- design — it happens in a side premise, which reduces on a chain of its+    -- own and discards it+    it "prints the chain of morphing steps with --sequence" $+      withStdin chained $+        testCLISucceeded+          ["morph", "--locator=Q.@", "--sequence", "--headers", "--sweet", "--hide-rho", "--flat"]+          [ "Rule 'maa'"+          , "Rule 'alpha'"+          , "Rule 'copy'"+          , "Rule 'mf'"+          , "⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"+          ]++    it "does not print the result with --quiet" $+      withStdin "[[ D> 01- ]]" $+        testCLISucceeded ["morph", "--quiet"] []++    it "records the atoms it fires with --evaluations" $+      withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do+        hClose stream+        withStdin chained $+          testCLISucceeded ["morph", "--locator=Q.@", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []+        records <- readUtf8 path+        lines records `shouldBe` ["L_number_plus\t⟦ x ↦ 6 ⟧\t11"]++    it "saves morphing steps to dir with --steps-dir" $+      withTempDirectory "phino-steps-morph" $ \dir ->+        withStdin chained $ do+          testCLISucceeded+            ["morph", "--locator=Q.@", "--steps-dir=" ++ dir, "--sweet", "--hide-rho", "--flat"]+            ["⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"]+          steps <- sort <$> listDirectory dir+          steps `shouldBe` map (\n -> printf "%05d.phi" (n :: Int)) [1 .. length steps]+          length steps `shouldSatisfy` (> 0)++    it "accepts --seed, --shuffle and --depth-sensitive" $+      withStdin "[[ D> 01- ]]" $+        testCLISucceeded ["morph", "--seed=7", "--shuffle", "--depth-sensitive", "--flat", "--hide-rho"] ["⟦ Δ ⤍ 01- ⟧"]++    -- The division 𝔻 cannot finish, whatever '--max-steps' it is given (#1052),+    -- is no work at all for 𝕄: the term is already a formation, so 'mf' hands+    -- it back and the atom is never fired+    it "returns the λ-formation dataize cannot finish on" $+      withStdin "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧" $+        testCLISucceeded+          ["morph", "--locator=Q.@", "--max-steps=40", "--flat", "--hide-rho"]+          ["⟦ λ ⤍ L_number_div"]++    -- '--max-steps' bounds the 𝕄 recursion just as it bounds the 𝕄/𝔻 one+    it "fails once the --max-steps budget is spent" $+      withStdin chained $+        testCLIFailed+          ["morph", "--locator=Q.@", "--max-steps=3"]+          ["[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=3"]++    -- 𝕄 never fires a bare λ-formation, so only the atoms sitting under a+    -- dispatch ('ml') can get stuck; '--partial' parks them exactly as under 𝔻+    describe "--partial" $ do+      let stuck = "[[ @ -> [[ L> Sym_arg_0 ]].foo ]]"+      it "fails on an atom that cannot fire without the flag" $+        withStdin stuck $+          testCLIFailed ["morph", "--locator=Q.@"] ["Atom 'Sym_arg_0' does not exist"]++      it "prints the residue with the stuck application intact and exits successfully" $+        withStdin stuck $+          testCLISucceeded+            ["morph", "--locator=Q.@", "--partial", "--flat", "--hide-rho"]+            ["⟦ λ ⤍ Sym_arg_0 ⟧.foo"]++    describe "fails" $ do+      it "with --output != latex and --nonumber" $+        withStdin "" $+          testCLIFailed+            ["morph", "--nonumber", "--output=xmir"]+            ["The --nonumber option can stay together with --output=latex only"]++      it "with --evaluations and --output != phi" $+        withStdin "[[ D> 01- ]]" $+          testCLIFailed+            ["morph", "--evaluations=evaluations.txt", "--output=latex"]+            ["The --evaluations option can stay together with --output=phi only"]++      it "with --show used more than once" $+        withStdin "" $+          testCLIFailed+            ["morph", "--show=Q.a", "--show=Q.b"]+            ["The option --show can be used only once"]++      it "with wrong --locator option" $+        withStdin "" $+          testCLIFailed+            ["morph", "--locator=Q.x(Q.y)"]+            ["[ERROR]:", "Only dispatch expression started with Φ (or Q) can be used in --locator"]+   describe "explain" $ do     it "prints help" $       testCLISucceeded@@ -1291,6 +1466,23 @@         ["explain", "--rule=resources/normalize/copy.yaml", "--rule=resources/normalize/alpha.yaml"]         ["\\phinoNormalizationRule{copy}", "\\phinoNormalizationRule{alpha}"] +    it "reproduces the same shuffle order for the same --seed" $ do+      let args =+            [ "explain"+            , "--shuffle"+            , "--seed=42"+            , rule "swap-a.yaml"+            , rule "swap-b.yaml"+            ]+      (firstRun, _) <- withStdout (runCLI args)+      (secondRun, _) <- withStdout (runCLI args)+      firstRun `shouldBe` secondRun++    it "accepts --seed flag" $+      testCLISucceeded+        ["explain", "--seed=7", "--normalize"]+        ["\\phinoNormalizationRule{alpha}"]+     it "explains normalization rules" $       testCLISucceeded         ["explain", "--normalize"]@@ -1538,8 +1730,18 @@     it "fails when more than one rule set is specified" $       testCLIFailed         ["explain", "--morph", "--dataize"]-        ["Only one of --rule, --normalize, --morph, --dataize or --contextualize can be specified"]+        ["Only one of --morph, --dataize or --contextualize can be specified"] +    it "allows --normalize together with --rule" $+      testCLISucceeded+        ["explain", "--normalize", "--rule=resources/normalize/copy.yaml"]+        ["\\phinoNormalizationRule{copy}"]++    it "allows --shuffle together with --morph" $+      testCLISucceeded+        ["explain", "--morph", "--shuffle"]+        ["\\begin{phinoMorphingInference}"]+     it "writes to target file" $       bracket         ( do@@ -1625,9 +1827,9 @@       withStdin "[[ x -> Q.x ]]" $         testCLISucceeded ["match", "--pattern=Q.!t"] ["t >> x"] -    it "accepts --seed flag" $+    it "does not accept a --seed flag (matching has nothing random)" $       withStdin "[[ x -> Q.x ]]" $-        testCLISucceeded ["match", "--seed=3", "--pattern=Q.!t"] ["t >> x"]+        testCLIFailed ["match", "--seed=3", "--pattern=Q.!t"] ["Invalid option `--seed=3'"]      it "prints many substitutions" $       withStdin "[[ x -> Q.x, y -> Q.y ]]" $

@@ -13,7 +13,7 @@ import Data.List (find, isInfixOf, nub) import Data.List.NonEmpty (NonEmpty (..)) import Data.Maybe (fromMaybe, isJust)-import Dataize (DataizeContext (..), Outcome (..), Steps (..), dataize, dataize', emptyState, execBuildTerm, morph)+import Dataize (DataizeContext (..), Outcome (..), Steps (..), dataize, dataize', emptyState, execBuildTerm, morph, morph') import Deps (Evaluation (..), Term (TeExpression), dontSaveEval, dontSaveStep) import Functions (buildTerm) import Matcher (substEmpty)@@ -53,12 +53,28 @@       (value, _) <- dataize expr (defaultDataizeContext loc')       value `shouldBe` Dataized res +testMorph :: [(String, String, String, String)] -> Spec+testMorph useCases =+  forM_ useCases $ \(name, loc, src, res) ->+    it name $ do+      expr <- parseExpressionThrows src+      loc' <- parseExpressionThrows loc+      expected <- parseExpressionThrows res+      (morphed, _) <- morph expr (defaultDataizeContext loc')+      morphed `shouldBe` expected+ -- The 12 primitive λ-atoms every EO data operation reduces to, declared the way -- 'number.eo' and 'bytes.eo' declare them, so a case below only has to spell the--- expression under φ. Alongside them stand the objects the atoms hand results--- to: 'string' carries the 'cant-slice' complaint, while 'true' and 'false' fill--- in for the real bool objects, since the single byte an EO bool dataizes to is--- all these cases assert.+-- The 12 primitive λ-atoms every EO data operation reduces to, declared the way+-- 'number.eo' and 'bytes.eo' declare them, so a case below only has to spell the+-- expression under φ. 'number.eq' is the one operation with no atom of its own:+-- EO spells it out of 'L_bytes_eq' (eq.eo), so the fixture composes it the same+-- way. Alongside them stand the objects the atoms hand results to: 'string'+-- carries the 'cant-slice' complaint, while 'true' and 'false' fill in for the+-- real bool objects, since the single byte an EO bool dataizes to is all these+-- cases assert. Those bytes are EO's own: 'true.eo' asserts+-- 'true.as-bytes.eq FF-' and 'bool.eo' branches 'if' over 'FF-' and '00-', so a+-- universe copied from here starts with a bool an EO program recognizes. primitives :: String -> String primitives src =   unlines@@ -82,10 +98,10 @@     , "    times -> [[ x -> ?, L> L_number_times ]],"     , "    div -> [[ x -> ?, L> L_number_div ]],"     , "    gt -> [[ x -> ?, L> L_number_gt ]],"-    , "    eq -> [[ x -> ?, y -> ?, L> L_number_eq ]]"+    , "    eq -> [[ x -> ?, @ -> $.^.as-bytes.eq( x.as-bytes ) ]]"     , "  ]],"     , "  string -> [[ as-bytes -> ?, @ -> $.as-bytes ]],"-    , "  true -> [[ @ -> [[ D> 01- ]] ]],"+    , "  true -> [[ @ -> [[ D> FF- ]] ]],"     , "  false -> [[ @ -> [[ D> 00- ]] ]],"     , "  @ -> " ++ src     , "]]"@@ -127,9 +143,46 @@  spec :: Spec spec = do-  describe "morph" $+  -- The top-level 𝕄 entry point, the one the 'morph' command runs: it locates+  -- the subterm, threads the whole input expression as the universe and hands+  -- back the morphed expression together with the chain that led to it (#1114).+  describe "morph" $ do+    testMorph+      [ ("hands the top formation back untouched under the Q locator", "Q", "[[ D> 00- ]]", "[[ D> 00- ]]")+      , -- 𝕄 is total where 𝔻 is not: the 'xi' axiom morphs ξ to ⊥, so the run+        -- ends with an answer rather than with a failure+        ("answers ⊥ where no formation is reachable", "Q.x", "[[ x -> $ ]]", "T")+      ]++    -- The chain runs oldest step first and carries the rule that produced the+    -- step after it, exactly as 'dataize' reports its own, so '--sequence'+    -- prints both the same way+    it "reports the chain of steps oldest first" $ do+      expr <- parseExpressionThrows "[[ D> 00- ]]"+      (morphed, chain) <- morph expr (defaultDataizeContext ExRoot)+      morphed `shouldBe` expr+      map snd chain `shouldBe` [Just "mf", Nothing]+      map fst chain `shouldBe` [expr, expr]++    -- 𝕄 never fires a bare λ-formation, so only an atom sitting under a+    -- dispatch (the 'ml' rule) can get stuck+    describe "a stuck atom under 'ml'" $ do+      let stuck :: IO (Expression, Expression)+          stuck = (,) <$> parseExpressionThrows "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" <*> parseExpressionThrows "Q.x"+      it "fails the run without '_partial'" $ do+        (expr, loc) <- stuck+        morph expr (defaultDataizeContext loc)+          `shouldThrow` (\e -> "Atom 'Sym_arg_0' does not exist" `isInfixOf` show (e :: SomeException))++      it "is parked in the residue under '_partial'" $ do+        (expr, loc) <- stuck+        expected <- parseExpressionThrows "[[ L> Sym_arg_0 ]].foo"+        (residue, _) <- morph expr (defaultDataizeContext loc){_partial = True}+        residue `shouldBe` expected++  describe "morph'" $     test'-      morph+      morph'       [ ("[[ D> 00- ]] => [[ D> 00- ]]", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")])       , ("T => T", ExTermination, ExRoot, ExTermination)       , ("$ => X", ExXi, ExRoot, ExTermination)@@ -175,11 +228,11 @@   -- and every such normal form is covered by some morphing clause (an axiom   -- like 'mf'/'dead'/'xi'/'universe'/'mg' or a recursive rule), so the "no rule   -- matched" fallback never fires along any real derivation. It is still total-  -- code, reachable by calling 'morph' directly (bypassing normalization) on a+  -- code, reachable by calling 'morph'' directly (bypassing normalization) on a   -- raw meta 𝑛, an AST node the matcher never binds to any concrete pattern.-  describe "morph fails when no morphing rule matches the term" $+  describe "morph' fails when no morphing rule matches the term" $     it "throws instead of looping when handed a bare, unmatched meta" $-      morph (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)+      morph' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)         `shouldThrow` (\e -> "no morphing rule matched" `isInfixOf` show (e :: SomeException))    -- Symmetric to the morphing fallback above: every normal form 𝔻 actually@@ -260,7 +313,7 @@       dataize' (form, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)         `shouldThrow` (\e -> "non-formation universe" `isInfixOf` show (e :: SomeException)) -  -- 'defaultDataizeContext' runs with '_shuffle' on, so 'morph' walks the+  -- 'defaultDataizeContext' runs with '_shuffle' on, so 'morph'' walks the   -- morphing rules in a random order on every step. Every clause is   -- order-independent (the known overlaps were removed in #856 and #860), so the   -- outcome must never depend on that order: morphing each input many times under@@ -283,7 +336,7 @@           ]     forM_ cases $ \(desc, input, univ, expected) ->       it ("morphs " ++ desc ++ " to the same form across 100 random rule orders") $ do-        results <- replicateM 100 (fst . fst <$> morph (input, (univ, Nothing) :| []) univ emptyState (defaultDataizeContext ExRoot))+        results <- replicateM 100 (fst . fst <$> morph' (input, (univ, Nothing) :| []) univ emptyState (defaultDataizeContext ExRoot))         nub results `shouldBe` [expected]    -- 'md' fires only when its head is not a formation ('not (formation 𝑛)'),@@ -311,7 +364,7 @@     it "drills a chained λ-formation dispatch down to the base 'ml'" $ do       let base = ExFormation [BiLambda (Function "F")]           chain = ExDispatch (ExDispatch (ExDispatch base (AtLabel "a")) (AtLabel "b")) (AtLabel "c")-      morph (chain, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)+      morph' (chain, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)         `shouldThrow` (\e -> "Atom 'F' does not exist" `isInfixOf` show (e :: SomeException))    -- 'norm' matches the bare meta 𝑛, which unifies with any expression, so it is@@ -395,7 +448,7 @@    -- '--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'+  -- λ-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.@@ -619,6 +672,7 @@           [ "[["           , "  bytes -> [["           , "    data -> ?,"+          , "    eq -> [[ b -> ?, L> L_bytes_eq ]],"           , "    @ -> $.data"           , "  ]],"           , "  number -> [["@@ -626,11 +680,13 @@           , "    @ -> $.as-bytes,"           , "    times -> [[ x -> ?, L> L_number_times ]],"           , "    plus -> [[ x -> ?, L> L_number_plus ]],"-          , "    eq -> [[ x -> ?, y -> ?, L> L_number_eq ]]"+          , "    eq -> [[ x -> ?, @ -> $.^.as-bytes.eq( x.as-bytes ) ]]"           , "  ]],"+          , "  true -> [[ if -> [[ t -> ?, f -> ?, @ -> t ]] ]],"+          , "  false -> [[ if -> [[ t -> ?, f -> ?, @ -> f ]] ]],"           , "  fac -> [["           , "    x -> ?,"-          , "    @ -> $.x.eq("+          , "    @ -> $.x.eq( 1 ).if("           , "      1,"           , "      $.x.times($.^.fac($.x.plus(-1)))"           , "    )"@@ -685,9 +741,13 @@     testAtom       [ ("divides a positive dividend", "256.div( 16 )", BtMany ["40", "30", "00", "00", "00", "00", "00", "00"])       , ("divides by zero into infinity", "2.div( 0 )", BtMany ["7F", "F0", "00", "00", "00", "00", "00", "00"])-      , ("tells 1000 is greater than 200", "1000.gt( 200 )", BtOne "01")+      , ("tells 1000 is greater than 200", "1000.gt( 200 )", BtOne "FF")       , ("tells 42 is not greater than 42.5", "42.gt( 42.5 )", BtOne "00")-      , ("tells zero is greater than a negative", "0.gt( -5 )", BtOne "01")+      , ("tells zero is greater than a negative", "0.gt( -5 )", BtOne "FF")+      , ("tells 5 equals 5", "5.eq( 5 )", BtOne "FF")+      , ("tells 5 is not equal to 6", "5.eq( 6 )", BtOne "00")+      , ("adds two numbers", "5.plus( 6 )", BtMany ["40", "26", "00", "00", "00", "00", "00", "00"])+      , ("multiplies two numbers", "5.times( 6 )", BtMany ["40", "3E", "00", "00", "00", "00", "00", "00"])       ,         ( "conjoins two long bytes"         , raw "02-EF-D4-05-5E-78-3A" ++ ".and( " ++ raw "12-33-C1-B5-5E-71-55" ++ " )"@@ -710,7 +770,7 @@         , BtMany ["05", "5E", "78"]         )       , ("counts the size of bytes", raw "F1-20-5F-EC-B5-90-32" ++ ".size", BtMany ["40", "1C", "00", "00", "00", "00", "00", "00"])-      , ("tells equal bytes are equal", raw "CA-FE" ++ ".eq( " ++ raw "CA-FE" ++ " )", BtOne "01")+      , ("tells equal bytes are equal", raw "CA-FE" ++ ".eq( " ++ raw "CA-FE" ++ " )", BtOne "FF")       , ("tells different bytes are not equal", raw "CA-FE" ++ ".eq( " ++ raw "CA-FF" ++ " )", BtOne "00")       , ("takes a part of bytes", raw "20-1F-EE-B5-90" ++ ".slice( 1, 3 )", BtMany ["1F", "EE", "B5"])       ,@@ -751,7 +811,13 @@       , ("cannot multiply by a non-numeric operand", "5.times( " ++ raw "--" ++ " )")       , ("cannot divide by a non-numeric divisor", "5.div( " ++ raw "--" ++ " )")       , ("cannot compare against a non-numeric threshold", "5.gt( " ++ raw "--" ++ " )")-      , ("cannot test equality against a non-numeric operand", "5.eq( " ++ raw "--" ++ ", 6 )")+      , -- A number atom also rejects a non-empty operand whose byte array is not+        -- 8 bytes long (e.g. 2 or 5 bytes): such an array carries no number, and+        -- the atom must yield ⊥ instead of crashing on 'btsToNum' (issue #1072).+        ("cannot add a 5-byte operand", "5.plus( " ++ raw "68-65-6C-6C-6F" ++ " )")+      , ("cannot multiply by a 2-byte operand", "5.times( " ++ raw "20-1F" ++ " )")+      , ("cannot divide by a 3-byte divisor", "5.div( " ++ raw "CA-FE-BE" ++ " )")+      , ("cannot compare against a 4-byte threshold", "5.gt( " ++ raw "FF-FF-FF-FF" ++ " )")       , -- 'right' rejects a shift distance that is not a plain 8-byte integer;         -- empty bytes carry no such integer, so the shift atom is stuck too.         ("cannot shift right by a non-integer distance", raw "C0-43-00-00-00-00-00-00" ++ ".right( " ++ raw "--" ++ " )")

@@ -87,7 +87,7 @@             expr' `shouldBe` defaultHidden         ) -      it "recurses over a multi-element rewrite list, pinning every element to the first fqn" $ do+      it "recurses over a multi-element rewrite list, pinning every element to the fqns" $ do         first' <- parseExpressionThrows "[[ x -> ?, y -> ? ]]"         second' <- parseExpressionThrows "[[ x -> ?, y -> ? ]]"         fqn <- parseExpressionThrows "Q.x"@@ -95,3 +95,11 @@         let included = F.include [(first', Just "rule-a"), (second', Just "rule-b")] [fqn, ExRoot]         map fst included `shouldBe` [expected, expected]         map snd included `shouldBe` [Just "rule-a", Just "rule-b"]++      it "keeps every matching fqn, not only the first one" $ do+        expr <- parseExpressionThrows "[[ x -> ?, y -> ? ]]"+        firstFqn <- parseExpressionThrows "Q.x"+        secondFqn <- parseExpressionThrows "Q.y"+        expected <- parseExpressionThrows "[[ x -> ?, y -> ? ]]"+        let [(expr', _)] = F.include [(expr, Nothing)] [firstFqn, secondFqn]+        expr' `shouldBe` expected

@@ -206,6 +206,12 @@       , ("number fails on an expression that is not a string", "number", [ArgExpression (DataNumber (numToBts 1))], "expects expression to be 'Φ.string'")       , ("number fails on the wrong number of arguments", "number", [], "number() requires exactly 1 argument")       ,+        ( "sum fails on a byte array that is not 8 bytes long"+        , "sum"+        , [ArgExpression (DataNumber (BtMany ["68", "65", "6C", "6C", "6F"]))]+        , "Expected 8 bytes for a number, got 5"+        )+      ,         ( "an unsupported function name fails with a descriptive message"         , "no-such-function"         , []

@@ -9,12 +9,13 @@ -} module RandomSpec where +import Control.Exception (SomeException, try) import Control.Monad (forM_) import Data.Char (isDigit, isHexDigit) import Data.Set qualified as Set import Random (randomString) import System.Timeout (timeout)-import Test.Hspec (Spec, describe, it, shouldBe, shouldSatisfy)+import Test.Hspec (Spec, describe, expectationFailure, it, shouldBe, shouldSatisfy)  spec :: Spec spec = do@@ -122,6 +123,18 @@       results <- mapM (const (randomString "%d")) [1 :: Int .. 2000]       let unique = Set.fromList results       Set.size unique `shouldBe` 2000++  describe "randomString %d space exhaustion" $+    it "raises an error instead of looping forever once the 10000-value space is exhausted" $ do+      -- Fill the whole '%d' space; the next call has no unique value left, so+      -- 'regenerate' must give up (previously it recursed forever).+      -- All 10000 values are generated within the same 'try' because the very+      -- last fill may already fail to find a fresh value.+      result <- timeout 10000000 (try (mapM_ (const (randomString "%d")) [1 :: Int .. 10000]) :: IO (Either SomeException ()))+      case result of+        Just (Left _) -> pure ()+        Just (Right _) -> expectationFailure "expected an error once the %d space is exhausted"+        Nothing -> expectationFailure "randomString hung instead of raising an error"  wordsBy :: (Char -> Bool) -> String -> [String] wordsBy predicate str = case dropWhile predicate str of

@@ -364,6 +364,30 @@                 RSB             )         )+      ,+        ( "PA_FORMATION with void params and a meta tail carries the meta binding through"+        , PA_FORMATION+            (AT_LABEL "x")+            [AT_LABEL "a"]+            ARROW+            (EX_FORMATION LSB EOL (TAB 2) (BI_META (META NO_EXCL B "B") (BDS_EMPTY (TAB 2)) (TAB 2)) EOL (TAB 1) RSB)+        , PA_TAU+            (AT_LABEL "x")+            ARROW+            ( EX_FORMATION+                LSB+                EOL+                (TAB 2)+                ( BI_PAIR+                    (PA_VOID (AT_LABEL "a") ARROW EMPTY)+                    (BDS_META EOL (TAB 2) (META NO_EXCL B "B") (BDS_EMPTY (TAB 2)))+                    (TAB 2)+                )+                EOL+                (TAB 1)+                RSB+            )+        )       , ("default clause leaves a PA_VOID pair untouched", PA_VOID (AT_LABEL "x") ARROW QUESTION, PA_VOID (AT_LABEL "x") ARROW QUESTION)       ]       (\(desc, sweet, salty) -> it desc (toSalty sweet `shouldBe` salty))

@@ -21,7 +21,7 @@ import GHC.Generics (Generic) import Parser (parseExpressionThrows) import System.FilePath (makeRelative)-import Test.Hspec (Spec, anyException, describe, expectationFailure, it, runIO, shouldBe, shouldContain, shouldThrow)+import Test.Hspec (Spec, anyException, describe, expectationFailure, it, runIO, shouldBe, shouldContain, shouldReturn, shouldThrow) import Text.XML (Document (..), Element (..), Node (NodeElement), Prologue (..)) import Text.XML.Cursor qualified as C import XMIR (XmirContext (XmirContext), defaultXmirContext, escapeXML, expressionToXMIR, parseXMIRThrows, printXMIR, toName, xmirToPhi)@@ -388,6 +388,13 @@       case formationArg of         [argCur] -> C.attribute (toName "base") argCur `shouldBe` []         _ -> expectationFailure "expected exactly one α1 argument"++    it "escapes XML special characters in attribute values" $ do+      expr <- parseExpressionThrows "[[ a&b -> \"<quoted>\" ]]"+      xmir' <- expressionToXMIR expr defaultXmirContext+      let out = printXMIR xmir'+      out `shouldContain` "name=\"a&amp;b\""+      xmirToPhi xmir' `shouldReturn` expr    describe "XMIR malformed input containing a processing instruction" $     it "embeds a processing instruction verbatim when rendering the offending element" $ do

@@ -156,3 +156,19 @@   describe "rejects a numerable expression that is neither an object, a number nor an index meta" $     it "fails on a bare boolean" $       (decodeYaml' "true" :: Either Yaml.ParseException Number) `shouldSatisfy` isLeft++  describe "parses a literal number" $+    it "accepts a whole number" $+      (decodeYaml' "5" :: Either Yaml.ParseException Number) `shouldSatisfy` (not . isLeft)++  describe "rejects a fractional literal number" $+    it "fails on a fraction instead of silently rounding it" $+      (decodeYaml' "2.5" :: Either Yaml.ParseException Number) `shouldSatisfy` isLeft++  describe "rejects an empty 'and' condition" $+    it "fails on 'and: []'" $+      (decodeYaml' "and: []" :: Either Yaml.ParseException Condition) `shouldSatisfy` isLeft++  describe "rejects an empty 'or' condition" $+    it "fails on 'or: []'" $+      (decodeYaml' "or: []" :: Either Yaml.ParseException Condition) `shouldSatisfy` isLeft