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.110 +cabal install --overwrite-policy=always phino-0.0.112 phino --version ``` @@ -100,6 +100,28 @@ 68-65-6C-6C-6F ``` +Every atom fired on the way to the bytes may be recorded in a machine-readable +protocol, with the `--evaluations` option. One firing is one line of three +tab-separated fields: the name of the λ function, the formation it was applied +to, and the expression it returned: + +```bash +$ cat sum.phi +⟦ + bytes(data) ↦ ⟦ φ ↦ data ⟧, + number(as-bytes) ↦ ⟦ φ ↦ as-bytes, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, + φ ↦ 5.plus( 6 ) +⟧ +$ phino dataize --evaluations=atoms.tsv --quiet --sweet --hide-rho sum.phi +$ cat -T atoms.tsv +L_number_plus^I⟦ x ↦ 6 ⟧^I11 +``` + +Records follow the syntax of the other options, such as `--sweet` and +`--hide-rho`, but always stay on one line. The file is truncated at the +beginning of every run, and `--output=phi` is the only output format it +works with, since one record must fit into one line. + ## Rewrite You can rewrite this expression with the help of [rules](#rule-structure) @@ -454,55 +476,55 @@ === parse/phi === warmup: 3 iterations batches: 10 x 1 - total: 1823744.302 μs - avg: 182374.430 μs - min: 166020.495 μs - max: 235134.815 μs - std dev: 21915.839 μs + total: 1548340.503 μs + avg: 154834.050 μs + min: 143956.756 μs + max: 183563.065 μs + std dev: 16085.516 μs === parse/xmir === warmup: 3 iterations batches: 10 x 1 - total: 7518652.376 μs - avg: 751865.238 μs - min: 680879.331 μs - max: 834737.644 μs - std dev: 43702.346 μs + total: 7516206.769 μs + avg: 751620.677 μs + min: 682874.922 μs + max: 842579.811 μs + std dev: 46693.965 μs === rewrite/normalize === warmup: 3 iterations batches: 10 x 1 - total: 628087.263 μs - avg: 62808.726 μs - min: 54676.886 μs - max: 71063.411 μs - std dev: 5609.304 μs + total: 520198.824 μs + avg: 52019.882 μs + min: 51367.239 μs + max: 52636.252 μs + std dev: 404.175 μs === print/sweet/multiline === warmup: 3 iterations batches: 10 x 1 - total: 4237321.401 μs - avg: 423732.140 μs - min: 399469.667 μs - max: 442779.214 μs - std dev: 13346.416 μs + total: 4326076.818 μs + avg: 432607.682 μs + min: 410101.006 μs + max: 471442.572 μs + std dev: 17970.166 μs === print/sweet/flat === warmup: 3 iterations batches: 10 x 1 - total: 4107718.132 μs - avg: 410771.813 μs - min: 395024.009 μs - max: 430270.510 μs - std dev: 11672.453 μs + total: 4306991.829 μs + avg: 430699.183 μs + min: 407690.710 μs + max: 450521.293 μs + std dev: 14268.817 μs === print/salty/multiline === warmup: 3 iterations batches: 10 x 1 - total: 14208719.443 μs - avg: 1420871.944 μs - min: 1398296.594 μs - max: 1455751.449 μs - std dev: 17141.226 μs + total: 13770643.090 μs + avg: 1377064.309 μs + min: 1349459.112 μs + max: 1422182.256 μs + std dev: 22169.348 μs ``` The results were calculated in [this GHA job][benchmark-gha] -on 2026-08-31 at 15:18, +on 2026-09-01 at 07:48, on Linux with 4 CPUs. @@ -551,4 +573,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/33403281766 +[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/33483476688 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.112 +version: 0.0.113 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs --- a/src/CLI/Helpers.hs +++ b/src/CLI/Helpers.hs @@ -16,18 +16,21 @@ import Data.IORef import Data.List (intercalate) import Data.Maybe -import Deps (SaveStepFunc, saveStep) +import Deps (SaveEvalFunc, SaveStepFunc, dontSaveEval, saveEval, saveStep) import Encoding import Files (ensuredFile) import Functions (execFunctions) -import LaTeX (LatexContext (..), defaultMeetLength, defaultMeetPopularity, expressionToLaTeX, rewrittensToLatex) +import LaTeX (LatexContext (LatexContext), defaultMeetLength, defaultMeetPopularity, expressionToLaTeX, rewrittensToLatex) +import Lining (LineFormat (SINGLELINE)) import Locator (locatedExpression) import Logger import Parser (parseExpressionThrows) import qualified Printer as P import qualified Random as R import Rewriter (Rewritten, Rewrittens', stepHeaders) -import System.IO (getContents') +import System.Directory (createDirectoryIfMissing) +import System.FilePath (takeDirectory) +import System.IO (Handle, IOMode (WriteMode), getContents', hClose, hSetEncoding, openFile, utf8) import Text.Printf (printf) import XMIR (expressionToXMIR, parseXMIRThrows, printXMIR, xmirToPhi) import Yaml (normalizationRules) @@ -53,6 +56,33 @@ step <- atomicModifyIORef' counter (\value -> (value + 1, value + 1)) saveStep stepsDir ioToExt render step expr pure save + +-- Run the action with a function recording atom firings, holding the protocol +-- file open for the whole run. Opening it for writing truncates it, so that it +-- always holds the firings of exactly one run: a caller reading it back never +-- picks up records left over from the previous run, even when this run fires no +-- atom at all. The handle is closed on the way out, failure included, so the +-- last records reach the disk even when dataization gives up. Every record is +-- flattened into a single line, whatever '--flat' says about the main output, +-- since the file is a line-per-firing protocol. The encoding is pinned to UTF-8 +-- rather than taken from the locale, since the file is read back by other +-- programs. +withEvalFunc :: Maybe FilePath -> PrintContext -> (SaveEvalFunc -> IO a) -> IO a +withEvalFunc Nothing _ action = action dontSaveEval +withEvalFunc (Just file) ctx action = do + createDirectoryIfMissing True (takeDirectory file) + logDebug (printf "The option '--evaluations' is specified, atom firings will be recorded in '%s'" file) + bracket opened hClose $ \protocol -> + action (saveEval protocol (printExpression ctx{_line = SINGLELINE})) + where + -- 'withFile' would do the same, except that it annotates whatever the action + -- throws with the name of the file, and a dataization failure has to reach + -- the user as it is + opened :: IO Handle + opened = do + protocol <- openFile file WriteMode + hSetEncoding protocol utf8 + pure protocol -- Read input from file or stdin readInput :: Maybe FilePath -> IO String diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs --- a/src/CLI/Parsers.hs +++ b/src/CLI/Parsers.hs @@ -202,6 +202,9 @@ optStepsDir :: Parser (Maybe FilePath) optStepsDir = optional (strOption (long "steps-dir" <> metavar "FILE" <> help "Directory to save intermediate steps during rewriting/dataizing")) +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)")) + optShuffle :: Parser Bool optShuffle = switch (long "shuffle" <> help "Shuffle rules before applying") @@ -305,6 +308,7 @@ <*> optLabel <*> optMeetPrefix <*> optStepsDir + <*> optEvaluations <*> argInputFile ) diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -150,7 +150,9 @@ exclude = (`F.exclude` excluded) include = (`F.include` included) save <- saveStepFunc _stepsDir printCtx - (bytes, chain) <- dataize expr (DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle buildTerm save) + (bytes, chain) <- + withEvalFunc _evaluations printCtx $ + dataize expr . DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle buildTerm save when _sequence (printRewrittens printCtx (exclude $ include chain, False) >>= putStrLn) unless _quiet (putStrLn (P.printBytes bytes)) where @@ -163,6 +165,9 @@ [(_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 diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs --- a/src/CLI/Types.hs +++ b/src/CLI/Types.hs @@ -106,6 +106,7 @@ , _label :: Maybe String , _meetPrefix :: Maybe String , _stepsDir :: Maybe FilePath + , _evaluations :: Maybe FilePath , _inputFile :: Maybe FilePath } diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -23,7 +23,7 @@ import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE import qualified Data.Text as T -import Deps (BuildTermFunc, BuildTermMethodS, SaveStepFunc, State, Term (..)) +import Deps (BuildTermFunc, BuildTermMethodS, Evaluation (..), SaveEvalFunc, SaveStepFunc, State, Term (..)) import Locator (locatedExpression, withLocatedExpression) import Matcher (MetaValue (..), Subst (..), combine, matchExpression', substEmpty, substSingle) import Misc @@ -78,6 +78,7 @@ , _shuffle :: Bool , _buildTerm :: BuildTermFunc , _saveStep :: SaveStepFunc + , _saveEval :: SaveEvalFunc } newtype DataizeException = OutOfSteps Int @@ -100,13 +101,19 @@ | otherwise = pure ctx{_steps = Steps limit (spent + 1)} -- Resolve formation for LAMBDA Morphing rule. --- If formation contains λ binding, the called atom result is returned. The --- universe 'univ' is forwarded to the atom. -formation :: [Binding] -> Expression -> State -> DataizeContext -> IO (Maybe (Expression, State)) +-- If formation contains λ binding, the called atom result is returned, together +-- with the name of the fired function and the formation the atom fired against, +-- since 𝔼 has to report all three. This is not the report itself: its '_result' +-- is the atom's raw answer, while the one 𝔼 reports carries the normal form of +-- that answer, which is what 𝔼 hands back to its caller. +-- The universe 'univ' is forwarded to the atom. +formation :: [Binding] -> Expression -> State -> DataizeContext -> IO (Maybe (Evaluation, State)) formation bds univ state ctx = do let (lambda, bds') = maybeLambda bds case lambda of - Just (BiLambda (Function func)) -> Just <$> atom func (ExFormation bds') univ state ctx + Just (BiLambda (Function func)) -> do + (obj, state') <- atom func (ExFormation bds') univ state ctx + pure (Just (Evaluation func (ExFormation bds') obj, state')) _ -> pure Nothing where maybeLambda :: [Binding] -> (Maybe Binding, [Binding]) @@ -528,6 +535,11 @@ -- callers ('fire', 'ml') need no follow-up 'normalize' premise. The universe is -- passed explicitly as the second argument (rather than threaded behind the -- scenes), matching how the morphing 𝕄 and dataization 𝔻 functions carry it. +-- Every firing is reported to '_saveEval', which the '--evaluations' option +-- turns into one record per line. The reported result is the normal form 𝔼 +-- returns, never the atom's raw answer, so the protocol and the caller see the +-- same term. A nested firing — an atom that dataizes its own arguments — +-- completes first, so it is reported before the firing that triggered it. _evaluate :: DataizeContext -> State -> BuildTermMethodS _evaluate ctx state [ArgExpression expr, ArgExpression universe] subst = do form <- buildExpressionThrows expr subst @@ -536,8 +548,9 @@ ExFormation bds -> do resolved <- formation bds univ state ctx case resolved of - Just (obj, state') -> do - (normal, _) <- normalized obj ((univ, Nothing) :| []) ctx + Just (fired, state') -> do + (normal, _) <- normalized fired._result ((univ, Nothing) :| []) ctx + ctx._saveEval (Evaluation fired._function fired._arguments normal) pure (TeExpression normal, state') Nothing -> throwIO (userError "Function evaluate() expects a formation with a λ binding") _ -> throwIO (userError "Function evaluate() expects a formation") diff --git a/src/Deps.hs b/src/Deps.hs --- a/src/Deps.hs +++ b/src/Deps.hs @@ -10,10 +10,13 @@ module Deps where import AST +import Data.List (intercalate) +import qualified Data.Text as T import Logger (logDebug) import Matcher import System.Directory (createDirectoryIfMissing) import System.FilePath +import System.IO (Handle, hPutStrLn) import Text.Printf (printf) import Yaml @@ -54,3 +57,28 @@ dontSaveStep :: SaveStepFunc dontSaveStep = saveStep Nothing "" (\_ -> pure "") 0 + +-- One firing of an atom, the way the Evaluation function 𝔼 sees it: the name of +-- the λ function, the formation it fired against with the λ binding removed, and +-- the term it produced. +data Evaluation = Evaluation + { _function :: T.Text + , _arguments :: Expression + , _result :: Expression + } + +type SaveEvalFunc = Evaluation -> IO () + +-- Append one evaluation to the protocol as a single tab-separated line: the λ +-- function name, its argument formation and its result. Both expressions are +-- rendered by the caller, which flattens them, so a record never spills over +-- more than one line. The handle stays open for the whole run, since a run may +-- fire thousands of atoms and reopening the file for each of them buys nothing. +saveEval :: Handle -> (Expression -> IO String) -> SaveEvalFunc +saveEval handle render (Evaluation func bindings outcome) = do + rendered <- mapM render [bindings, outcome] + hPutStrLn handle (intercalate "\t" (T.unpack func : rendered)) + logDebug (printf "Saved the evaluation of '%s'" (T.unpack func)) + +dontSaveEval :: SaveEvalFunc +dontSaveEval _ = pure () diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -79,6 +79,14 @@ hClose h action path +readUtf8 :: FilePath -> IO String +readUtf8 path = + withFile path ReadMode $ \stream -> do + hSetEncoding stream utf8 + content <- hGetContents stream + _ <- evaluate (length content) + pure content + testCLI' :: [String] -> [String] -> Either ExitCode () -> Expectation testCLI' args outputs exit = do (out, result) <- withStdout (try (runCLI args) :: IO (Either ExitCode ())) @@ -1084,6 +1092,60 @@ it "does not print bytes with --quiet" $ withStdin "[[ D> 01- ]]" $ testCLISucceeded ["dataize", "--quiet"] [] + + describe "--evaluations" $ do + it "writes one tab-separated record per fired atom" $ + withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do + hClose stream + withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ + testCLISucceeded ["dataize", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + records <- readUtf8 path + records `shouldBe` "L_number_plus\t⟦ x ↦ 6 ⟧\t11\n" + + it "writes a record for every firing" $ + withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do + hClose stream + withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $ + testCLISucceeded ["dataize", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + records <- readUtf8 path + lines records `shouldBe` ["L_number_plus\t⟦ x ↦ 6 ⟧\t11", "L_number_plus\t⟦ x ↦ 7 ⟧\t18"] + + it "writes records in canonical syntax without --sweet" $ + withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do + hClose stream + withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ + testCLISucceeded ["dataize", "--evaluations=" ++ path, "--quiet", "--hide-rho"] [] + records <- readUtf8 path + records `shouldEndWith` "\tΦ.number( as-bytes ↦ Φ.bytes( data ↦ ⟦ Δ ⤍ 40-26-00-00-00-00-00-00 ⟧ ) )\n" + + it "keeps the records of a run that fails" $ + withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do + hClose stream + withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]], nope -> [[ L> L_number_nope ]] ]], @ -> 5.plus(6).nope ]]" $ + testCLIFailed + ["dataize", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] + ["Atom 'L_number_nope' does not exist"] + records <- readUtf8 path + records `shouldBe` "L_number_plus\t⟦ x ↦ 6 ⟧\t11\n" + + it "truncates the records left over from the previous run" $ + withTempFileContent "evaluationsXXXXXX.txt" "L_number_gt\t[[ ]]\t01-\n" $ \path -> do + withStdin "[[ D> 01- ]]" $ + testCLISucceeded ["dataize", "--evaluations=" ++ path, "--quiet"] [] + records <- readUtf8 path + records `shouldBe` "" + + it "fails with --output=xmir" $ + withStdin "[[ D> 01- ]]" $ + testCLIFailed + ["dataize", "--evaluations=evaluations.txt", "--output=xmir"] + ["The --evaluations option can stay together with --output=phi only"] + + it "fails with --output=latex" $ + withStdin "[[ D> 01- ]]" $ + testCLIFailed + ["dataize", "--evaluations=evaluations.txt", "--output=latex"] + ["The --evaluations option can stay together with --output=phi only"] describe "fails" $ do it "with --output != latex and --nonumber" $ 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.NonEmpty (NonEmpty (..)) import Data.Maybe (fromMaybe) import Dataize (DataizeContext (DataizeContext), Steps (Steps), dataize, dataize', emptyState, execBuildTerm, morph) -import Deps (dontSaveStep) +import Deps (dontSaveEval, dontSaveStep) import Functions (buildTerm) import Matcher (substEmpty) import Parser (parseExpressionThrows) @@ -26,7 +26,7 @@ -- dataization rules (#909): a hidden overlap surfaces as a nondeterministic -- failure instead of staying silently green. defaultDataizeContext :: Expression -> DataizeContext -defaultDataizeContext loc = DataizeContext loc 25 25 (Steps 250 0) False True buildTerm dontSaveStep +defaultDataizeContext loc = DataizeContext loc 25 25 (Steps 250 0) False True buildTerm dontSaveStep dontSaveEval test :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> String -> DataizeContext -> IO ((a, [Rewritten]), String)) -> [(String, Expression, Expression, a)] -> Spec test func useCases = @@ -280,7 +280,7 @@ describe "stops a dataization that never reaches bytes" $ it "fails on the step limit instead of morphing forever" $ do expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧" - dataize expr (DataizeContext ExRoot 25 25 (Steps 40 0) False True buildTerm dontSaveStep) + dataize expr (DataizeContext ExRoot 25 25 (Steps 40 0) False True buildTerm dontSaveStep dontSaveEval) `shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException)) describe "labels every step with a defined rule or operation" $ do