diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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. @@ -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 diff --git a/phino.cabal b/phino.cabal --- a/phino.cabal +++ b/phino.cabal @@ -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 @@ -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, diff --git a/src/Bytes.hs b/src/Bytes.hs --- a/src/Bytes.hs +++ b/src/Bytes.hs @@ -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 diff --git a/src/CLI.hs b/src/CLI.hs --- a/src/CLI.hs +++ b/src/CLI.hs @@ -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) diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs --- a/src/CLI/Helpers.hs +++ b/src/CLI/Helpers.hs @@ -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 diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs --- a/src/CLI/Parsers.hs +++ b/src/CLI/Parsers.hs @@ -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")) diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -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 diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs --- a/src/CLI/Types.hs +++ b/src/CLI/Types.hs @@ -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 diff --git a/src/CLI/Validators.hs b/src/CLI/Validators.hs --- a/src/CLI/Validators.hs +++ b/src/CLI/Validators.hs @@ -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)) diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -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") diff --git a/src/Filter.hs b/src/Filter.hs --- a/src/Filter.hs +++ b/src/Filter.hs @@ -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 diff --git a/src/Functions.hs b/src/Functions.hs --- a/src/Functions.hs +++ b/src/Functions.hs @@ -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 diff --git a/src/Random.hs b/src/Random.hs --- a/src/Random.hs +++ b/src/Random.hs @@ -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 diff --git a/src/Sugar.hs b/src/Sugar.hs --- a/src/Sugar.hs +++ b/src/Sugar.hs @@ -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 diff --git a/src/XMIR.hs b/src/XMIR.hs --- a/src/XMIR.hs +++ b/src/XMIR.hs @@ -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 '\'' = "'" 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 . +escapeXMLText :: String -> String +escapeXMLText = concatMap escapeChar + where + escapeChar :: Char -> String + escapeChar '&' = "&" + escapeChar '<' = "<" + 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 ] diff --git a/src/Yaml.hs b/src/Yaml.hs --- a/src/Yaml.hs +++ b/src/Yaml.hs @@ -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" diff --git a/test/BytesSpec.hs b/test/BytesSpec.hs --- a/test/BytesSpec.hs +++ b/test/BytesSpec.hs @@ -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 diff --git a/test/CLIHelpersSpec.hs b/test/CLIHelpersSpec.hs --- a/test/CLIHelpersSpec.hs +++ b/test/CLIHelpersSpec.hs @@ -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 diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -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"] ["", ""] + 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 ]]" $ diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -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 "--" ++ " )") diff --git a/test/FilterSpec.hs b/test/FilterSpec.hs --- a/test/FilterSpec.hs +++ b/test/FilterSpec.hs @@ -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 diff --git a/test/FunctionsSpec.hs b/test/FunctionsSpec.hs --- a/test/FunctionsSpec.hs +++ b/test/FunctionsSpec.hs @@ -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" , [] diff --git a/test/RandomSpec.hs b/test/RandomSpec.hs --- a/test/RandomSpec.hs +++ b/test/RandomSpec.hs @@ -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 diff --git a/test/SugarSpec.hs b/test/SugarSpec.hs --- a/test/SugarSpec.hs +++ b/test/SugarSpec.hs @@ -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)) diff --git a/test/XMIRSpec.hs b/test/XMIRSpec.hs --- a/test/XMIRSpec.hs +++ b/test/XMIRSpec.hs @@ -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 -> \"\" ]]" + xmir' <- expressionToXMIR expr defaultXmirContext + let out = printXMIR xmir' + out `shouldContain` "name=\"a&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 diff --git a/test/YamlSpec.hs b/test/YamlSpec.hs --- a/test/YamlSpec.hs +++ b/test/YamlSpec.hs @@ -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