phino 0.0.112 → 0.0.113

raw patch · 10 files changed

+213/−48 lines, 10 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +55/−33
• phino.cabal +1/−1
• src/CLI/Helpers.hs +33/−3
• src/CLI/Parsers.hs +4/−0
• src/CLI/Runners.hs +6/−1
• src/CLI/Types.hs +1/−0
• src/Dataize.hs +20/−7
• src/Deps.hs +28/−0
• test/CLISpec.hs +62/−0
• test/DataizeSpec.hs +3/−3

@@ -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.  <!-- benchmark_end -->@@ -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

@@ -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 <https://github.com/objectionary/phino#readme>

@@ -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

@@ -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         ) 

@@ -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

@@ -106,6 +106,7 @@   , _label :: Maybe String   , _meetPrefix :: Maybe String   , _stepsDir :: Maybe FilePath+  , _evaluations :: Maybe FilePath   , _inputFile :: Maybe FilePath   } 

@@ -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")

@@ -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 ()

@@ -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" $

@@ -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