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.121 +cabal install --overwrite-policy=always phino-0.0.127 phino --version ``` @@ -900,55 +900,55 @@ === parse/phi === warmup: 3 iterations batches: 10 x 1 - total: 1775922.415 μs - avg: 177592.242 μs - min: 161735.069 μs - max: 206519.406 μs - std dev: 15129.161 μs + total: 1796596.921 μs + avg: 179659.692 μs + min: 164919.877 μs + max: 207942.466 μs + std dev: 16799.590 μs === parse/xmir === warmup: 3 iterations batches: 10 x 1 - total: 7571386.164 μs - avg: 757138.616 μs - min: 691286.480 μs - max: 813614.260 μs - std dev: 32034.618 μs + total: 7612275.214 μs + avg: 761227.521 μs + min: 709200.274 μs + max: 813312.545 μs + std dev: 30787.560 μs === rewrite/normalize === warmup: 3 iterations batches: 10 x 1 - total: 579674.000 μs - avg: 57967.400 μs - min: 56388.139 μs - max: 61829.190 μs - std dev: 1703.063 μs + total: 641726.516 μs + avg: 64172.652 μs + min: 59940.799 μs + max: 76191.091 μs + std dev: 4666.243 μs === print/sweet/multiline === warmup: 3 iterations batches: 10 x 1 - total: 3876263.188 μs - avg: 387626.319 μs - min: 373639.628 μs - max: 405513.521 μs - std dev: 10018.938 μs + total: 4232626.830 μs + avg: 423262.683 μs + min: 402756.415 μs + max: 452617.626 μs + std dev: 15405.204 μs === print/sweet/flat === warmup: 3 iterations batches: 10 x 1 - total: 3789406.984 μs - avg: 378940.698 μs - min: 367216.617 μs - max: 395082.263 μs - std dev: 8761.575 μs + total: 4143560.984 μs + avg: 414356.098 μs + min: 398710.605 μs + max: 431760.505 μs + std dev: 10740.809 μs === print/salty/multiline === warmup: 3 iterations batches: 10 x 1 - total: 13982361.998 μs - avg: 1398236.200 μs - min: 1366361.442 μs - max: 1433666.397 μs - std dev: 17717.682 μs + total: 14017459.280 μs + avg: 1401745.928 μs + min: 1380342.970 μs + max: 1418756.423 μs + std dev: 14496.070 μs ``` The results were calculated in [this GHA job][benchmark-gha] -on 2026-09-09 at 15:41, +on 2026-09-11 at 08:17, on Linux with 4 CPUs. @@ -997,4 +997,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/34371511775 +[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/34577695934 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.127 +version: 0.0.128 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at diff --git a/src/Atoms.hs b/src/Atoms.hs --- a/src/Atoms.hs +++ b/src/Atoms.hs @@ -506,35 +506,37 @@ -- what the attribute carries, as 'ask' does, or to hand the node over as -- it is (#1165). referenced :: Int -> Int -> T.Text -> Bool -> IO () - referenced minted req name doReduce = do - spoken' <- describe - case spoken' of - Left failure -> throwIO (AtomMute func described failure) - Right value -> do - logDebug (printf "Atom '%s' asks phino for '%s' of request %d%s as question %d" (T.unpack func) (T.unpack name) req (if doReduce then ", reduced," else ", as it is," :: String) minted) - answer <- if doReduce then reduce value else pure value - said (lined (object ["id" .= minted, "𝑛" .= spelled answer])) + referenced minted req attrName doReduce = case channel of + Closed -> throwIO (AtomMute func described "it asks phino for an attribute of a previous request, while its stdin is closed, since its entry does not say 'serve'") + Open -> do + spoken' <- describe + case spoken' of + Left failure -> throwIO (AtomMute func described failure) + Right value -> do + logDebug (printf "Atom '%s' asks phino for '%s' of request %d%s as question %d" (T.unpack func) (T.unpack attrName) req (if doReduce then ", reduced," else ", as it is," :: String) minted) + answer <- if doReduce then reduce value else pure value + said (lined (object ["id" .= minted, "𝑛" .= spelled answer])) where described :: String - described = printf "{'of':%d,'attr':'%s'}" req (T.unpack name) + described = printf "{'of':%d,'attr':'%s'}" req (T.unpack attrName) describe :: IO (Either String Expression) describe = do forms <- readIORef _forms pure $ case IM.lookup req forms of - Nothing -> Left (printf "there is no in-flight request %d to take '%s' from" req (T.unpack name)) - Just form' -> case attributeValue name form' of - Nothing -> Left (printf "the receiver of request %d carries no attribute '%s'" req (T.unpack name)) + Nothing -> Left (printf "there is no in-flight request %d to take '%s' from" req (T.unpack attrName)) + Just form' -> case attributeValue attrName form' of + Nothing -> Left (printf "the receiver of request %d carries no attribute '%s'" req (T.unpack attrName)) Just value -> Right value - attributeValue :: T.Text -> Expression -> Maybe Expression - attributeValue name (ExFormation bds) = go bds - where - go :: [Binding] -> Maybe Expression - go [] = Nothing - go (BiTau attr value : rest) - | T.pack (printAttribute attr) == name = Just value - | otherwise = go rest - go (_ : rest) = go rest - attributeValue _ _ = Nothing + attributeValue :: T.Text -> Expression -> Maybe Expression + attributeValue name (ExFormation bds) = go bds + where + go :: [Binding] -> Maybe Expression + go [] = Nothing + go (BiTau attr value : rest) + | T.pack (printAttribute attr) == name = Just value + | otherwise = go rest + go (_ : rest) = go rest + attributeValue _ _ = Nothing -- Reduce the 𝜑-expression the program asks about and say it back under -- '𝑛', with the 'id' the question minted. A program started for the fire -- has nothing to be answered over, since phino closed its stdin behind the diff --git a/src/Bytes.hs b/src/Bytes.hs --- a/src/Bytes.hs +++ b/src/Bytes.hs @@ -419,9 +419,12 @@ -- BtMany ["00","00"] btsShift :: Int -> Bytes -> Bytes btsShift bits bts + | magnitude >= toInteger size * 8 = word8ToBytes (replicate size 0) | bits < 0 = word8ToBytes (map leftwards indices) | otherwise = word8ToBytes (map rightwards indices) where + magnitude :: Integer + magnitude = abs (toInteger bits) octets :: [Word8] octets = btsToWord8 bts size :: Int @@ -429,9 +432,9 @@ indices :: [Int] indices = [0 .. size - 1] modulo :: Int - modulo = abs bits `mod` 8 + modulo = fromInteger (magnitude `mod` 8) offset :: Int - offset = abs bits `div` 8 + offset = fromInteger (magnitude `div` 8) octet :: Int -> Word8 octet index = octets !! index rightwards :: Int -> Word8 diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs --- a/src/CLI/Parsers.hs +++ b/src/CLI/Parsers.hs @@ -464,6 +464,7 @@ <*> optMargin <*> optTarget <*> many (argument str (metavar "[FILE]" <> help "Paths to input files")) + <*> optSeed ) matchParser :: Parser Command @@ -477,6 +478,7 @@ <*> optional (strOption (long "pattern" <> metavar "EXPRESSION" <> help "Pattern expression to match against")) <*> optional (strOption (long "when" <> metavar "CONDITION" <> help "Predicate for matched substitutions")) <*> argInputFile + <*> optSeed ) commandParser :: Parser Command diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -328,6 +328,7 @@ runMerge OptsMerge{..} = do validateOpts inputs' <- traverse (readInput . Just) _inputs + setStdGen (mkStdGen _seed) exprs <- traverse (`parseInput` _inputFormat) inputs' expr <- merge exprs validateXmirTopLevel _outputFormat expr @@ -364,6 +365,7 @@ runMatch :: OptsMatch -> IO () runMatch OptsMatch{..} = do + setStdGen (mkStdGen _seed) input <- readInput _inputFile expr <- parseInput input PHI if isNothing _pattern diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs --- a/src/CLI/Types.hs +++ b/src/CLI/Types.hs @@ -228,6 +228,7 @@ , _margin :: Int , _targetFile :: Maybe FilePath , _inputs :: [FilePath] + , _seed :: Int } data OptsMatch = OptsMatch @@ -238,4 +239,5 @@ , _pattern :: Maybe String , _when :: Maybe String , _inputFile :: Maybe FilePath + , _seed :: Int } diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -319,18 +319,18 @@ -- registry allows. Every entry is charged to the '--max-steps' budget, which -- is what bounds the walk. deepened :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State) -deepened expr univ = go ExXi expr +deepened expr univ = go Nothing ExXi expr where -- A term as it was written, together with what its free ξ stands for: the -- formation the walk entered it from, without the binding it came from, -- exactly the context the 'dot' rule hands a dispatched body. At the top -- there is no such formation, so ξ stands for itself and contextualization -- leaves the term alone. - go :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State) - go context term state' caller = do + go :: Maybe Attribute -> Expression -> Expression -> State -> DataizeContext -> IO (Expression, State) + go dispatched context term state' caller = do ctx' <- deeper caller (walked, walkedState) <- parts context term state' caller - answer <- fired (contextualize walked context) univ walkedState ctx' + answer <- fired dispatched (contextualize walked context) univ walkedState ctx' maybe (pure (walked, walkedState)) pure answer -- The parts of a term nothing fired on, walked one by one and put back -- where they were, so the term keeps the shape it was written in. @@ -339,10 +339,10 @@ (entered, state'') <- bindings bds bds state' caller pure (ExFormation entered, state'') parts context (ExDispatch target attr) state' caller = do - (entered, state'') <- go context target state' caller + (entered, state'') <- go (Just attr) context target state' caller pure (ExDispatch entered attr, state'') parts context (ExApplication target arg) state' caller = do - (entered, state'') <- go context target state' caller + (entered, state'') <- go Nothing context target state' caller (applied, state''') <- argument context arg state'' caller pure (ExApplication entered applied, state''') parts _ term state' _ = pure (term, state') @@ -354,7 +354,7 @@ bindings _ [] state' _ = pure ([], state') bindings whole (BiTau attr body : rest) state' caller | attr /= AtRho = do - (entered, state'') <- go (scope attr whole) body state' caller + (entered, state'') <- go Nothing (scope attr whole) body state' caller (others, state''') <- bindings whole rest state'' caller pure (BiTau attr entered : others, state''') bindings whole (bd : rest) state' caller = do @@ -373,10 +373,10 @@ -- applies is walked by the caller and the argument it binds is walked here. argument :: Expression -> Argument -> State -> DataizeContext -> IO (Argument, State) argument context (ArTau attr arg) state' caller = do - (entered, state'') <- go context arg state' caller + (entered, state'') <- go Nothing context arg state' caller pure (ArTau attr entered, state'') argument context (ArAlpha alpha arg) state' caller = do - (entered, state'') <- go context arg state' caller + (entered, state'') <- go Nothing context arg state' caller pure (ArAlpha alpha entered, state'') -- Ask 𝕄 about a term and fire the λ of the formation it reaches, as long as @@ -391,16 +391,31 @@ -- compute stays as it was written with or without '_partial'; an atom that -- cannot fire deeper on the spine still fails the run, exactly as it does -- under 𝕄 alone, and '_partial' parks it. A formation still waiting for its --- arguments is left alone too (see 'saturated'). -fired :: Expression -> Expression -> State -> DataizeContext -> IO (Maybe (Expression, State)) -fired term univ state caller = do +-- arguments is left alone too (see 'saturated'). A term standing as the target +-- of a dispatch is where 'ml' has its say: the λ is fired only where the +-- dispatched attribute is none of the formation's own (see 'demanded'). +fired :: Maybe Attribute -> Expression -> Expression -> State -> DataizeContext -> IO (Maybe (Expression, State)) +fired dispatched term univ state caller = do ctx <- deeper caller morphed <- try (reduced ctx) case morphed of - Right (ExFormation bds, state') -> maybe (pure Nothing) (evaluated ctx state') (saturated bds) + Right (ExFormation bds, state') + | demanded bds -> maybe (pure Nothing) (evaluated ctx state') (saturated bds) Right _ -> pure Nothing Left failure -> parked failure where + -- Whether the dispatch the term stands under demands the λ of the formation + -- 𝕄 reached. 'ml' fires that λ only where the dispatched attribute is none + -- of the formation's own, since 'dot' resolves the dispatch before 'ml' is + -- ever reached, and a walk firing it first answers a formation the dispatch + -- no longer fits (#1187). A term standing anywhere else is demanded by + -- nothing and the walk fires what 'mf' left bare, as it always has. + demanded :: [Binding] -> Bool + demanded bds = not (any bound bds) + where + bound :: Binding -> Bool + bound (BiTau attr _) = Just attr == dispatched + bound _ = False -- 𝕄 takes normal forms only and a term taken from the program as it was -- written is not necessarily one, so it is normalized against the universe -- first, exactly as '--inside' normalizes what it is handed. Both chains @@ -421,7 +436,7 @@ Just registered -> do answer <- fireAtom func registered self univ (reduction univ ctx) ctx._saveEval (Evaluation func self (Just answer)) - again <- fired answer univ state' ctx + again <- fired dispatched answer univ state' ctx pure (Just (fromMaybe (answer, state') again)) parked :: DataizeException -> IO (Maybe a) parked (Stuck _) | caller._partial = pure Nothing diff --git a/src/XMIR.hs b/src/XMIR.hs --- a/src/XMIR.hs +++ b/src/XMIR.hs @@ -26,6 +26,7 @@ import Control.Exception (Exception (displayException), throwIO) import Control.Monad (unless) import Data.Bifunctor (bimap) +import Data.Char (isAsciiLower, isDigit) import Data.Foldable (foldlM) import Data.List (intercalate) import qualified Data.Map as M @@ -157,9 +158,7 @@ formationBinding :: Binding -> XmirContext -> IO (Maybe Node) formationBinding (BiTau (AtLabel label) expr) ctx = Just <$> namedBinding (T.unpack label) expr ctx formationBinding (BiTau AtRho expr) ctx = Just <$> namedBinding (show AtRho) expr ctx -formationBinding (BiTau AtPhi expr) ctx = do - (base, children) <- expression expr ctx - pure (Just (object [("name", show AtPhi), ("base", base)] children)) +formationBinding (BiTau AtPhi expr) ctx = Just <$> namedBinding (show AtPhi) expr ctx formationBinding (BiDelta bytes) _ = pure (Just (NodeContent (T.pack (printBytes bytes)))) formationBinding (BiLambda (Function name)) _ = pure (Just (object [("name", show AtLambda)] [NodeContent name])) formationBinding (BiVoid AtRho) _ = pure Nothing @@ -507,7 +506,12 @@ lambdaFunction :: IO T.Text lambdaFunction | hasText cur = T.strip . T.pack <$> getText cur - | otherwise = pure (T.pack (intercalate "_" ("L" : reverse fqn))) + | otherwise = pure (T.pack (intercalate "_" ("L" : map (map spell) (reverse fqn)))) + -- A binding label admits nearly any character, while 'function' admits a + -- digit, an ASCII lowercase letter, '_' and 'φ' only, so everything else + -- folds into '_' and the derived name stays readable back (#1188) + spell :: Char -> Char + spell ch = if isDigit ch || isAsciiLower ch || ch == '_' || ch == 'φ' then ch else '_' -- A formation keeps its Δ data in the text content of its own element, the way -- the printer emits a Δ binding, while the rest of the bindings live in the diff --git a/test/BytesSpec.hs b/test/BytesSpec.hs --- a/test/BytesSpec.hs +++ b/test/BytesSpec.hs @@ -299,5 +299,10 @@ , BtMany ["02", "03", "00"] ) , ("large negative shift empties out", btsShift (-2147483648) (BtMany ["BF", "F0"]), BtMany ["00", "00"]) + , + ( "minimum Int shift empties out" + , btsShift (minBound :: Int) (BtMany ["BF", "F0"]) + , BtMany ["00", "00"] + ) ] (\(desc, actual, expected) -> it desc (actual `shouldBe` expected)) diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -2085,6 +2085,18 @@ ["merge", resource "desugar.phi", "--output=xmir"] ["", "⟦ foo ↦ ξ.x, ρ ↦ ∅ ⟧", ""] + it "reproduces the same output for the same --seed" $ do + let args = + [ "merge" + , "--seed=42" + , "--sweet" + , resource "number.phi" + , resource "bytes.phi" + ] + (firstRun, _) <- withStdout (runCLI args) + (secondRun, _) <- withStdout (runCLI args) + firstRun `shouldBe` secondRun + describe "match" $ do it "prints help" $ testCLISucceeded @@ -2102,13 +2114,22 @@ withStdin "[[]]" $ testCLISucceeded ["match", "--log-level=debug"] ["[DEBUG]: The --pattern is not provided, no substitutions are built"] - it "prints one substitution" $ - withStdin "[[ x -> Q.x ]]" $ - testCLISucceeded ["match", "--pattern=Q.!t"] ["t >> x"] - - it "does not accept a --seed flag (matching has nothing random)" $ - withStdin "[[ x -> Q.x ]]" $ - testCLIFailed ["match", "--seed=3", "--pattern=Q.!t"] ["Invalid option `--seed=3'"] + it "reproduces the same output for the same --seed" $ do + dir <- getTemporaryDirectory + let file = dir ++ "/phino-match-seed-test.phi" + writeFile file "[[ x -> Q.x, y -> Q.y, z -> Q.z ]]" + let args = + [ "match" + , "--seed=42" + , "--sweet" + , "--flat" + , "--pattern=Q.!t" + , file + ] + (firstRun, _) <- withStdout (runCLI args) + (secondRun, _) <- withStdout (runCLI args) + firstRun `shouldBe` secondRun + removeFile file 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 @@ -7,7 +7,7 @@ module DataizeSpec (spec) where import AST -import Atoms (Registry, emptyRegistry) +import Atoms (Registry, emptyRegistry, readRegistry) import Control.Exception (SomeException) import Control.Monad import Data.IORef (modifyIORef', newIORef, readIORef) @@ -16,7 +16,7 @@ import Data.Maybe (fromMaybe, isJust) import Dataize (DataizeContext (..), Outcome (..), Steps (..), dataize, dataize', emptyState, execBuildTerm, insideUniverse, morph, morph') import Deps (Evaluation (..), Term (TeExpression), dontSaveEval, dontSaveStep) -import Fixtures (fixtureRegistry, withNode) +import Fixtures (fixtureRegistry, withNode, withServing, withShell) import Functions (buildTerm) import Matcher (substEmpty) import Parser (parseExpressionThrows) @@ -286,6 +286,18 @@ expr <- stuck (morphed, _) <- morph expr (defaultDataizeContext ExRoot){_deep = True, _partial = True} morphed `shouldBe` expr + + -- The walk enters a dispatch through its target and fires the box it finds + -- there before 𝕄 is ever asked about the dispatch, while 'ml' demands that + -- λ only where the dispatched attribute is none of the box's own (#1187) + describe "a dispatch naming an attribute of the formation it stands on" $ + it "cannot fire the λ the dispatch does not demand" $ + withShell $ + withServing "printf '{\"id\": %s, \"𝑛\": \"⟦ Δ ⤍ FF- ⟧\"}\\n' \"$id\"" $ \path -> do + box <- readRegistry path + world <- parseExpressionThrows "[[ foo -> [[ f -> [[ a -> ?, @ -> $.a, L> L_answer ]] ]], x -> Q.foo.f( a -> [[ D> 01- ]] ).@ ]]" + (morphed, _) <- morph world (withAtoms box (defaultDataizeContext ExRoot)){_deep = True} + morphed `shouldBe` world describe "morph'" $ test' diff --git a/test/XMIRSpec.hs b/test/XMIRSpec.hs --- a/test/XMIRSpec.hs +++ b/test/XMIRSpec.hs @@ -20,6 +20,7 @@ import Files (allPathsIn) import GHC.Generics (Generic) import Parser (parseExpressionThrows) +import Printer (printExpression) import System.FilePath (makeRelative) import Test.Hspec (Spec, anyException, describe, expectationFailure, it, runIO, shouldBe, shouldContain, shouldNotContain, shouldReturn, shouldThrow) import Text.XML (Document (..), Element (..), Node (NodeElement), Prologue (..)) @@ -224,6 +225,14 @@ back `shouldBe` expr ) + -- A λ marker with no text is named after the enclosing bindings, whose + -- labels admit characters the 'function' parser refuses (#1188) + describe "derived λ function name" $ + it "spells itself in the alphabet the parser accepts" $ do + doc <- parseXMIRThrows "" + expr <- xmirToPhi doc + parseExpressionThrows (printExpression expr) `shouldReturn` expr + describe "--hide-rho in XMIR" $ it "drops every bound ρ from the printed document" $ do expr <- parseExpressionThrows "[[ x -> 4, ^ -> [[ y -> 5 ]] ]]" @@ -272,6 +281,7 @@ , ("keeps Δ data bound to a named attribute", "[[ k -> [[ a -> [[ D> 01-02 ]], ^ -> [[ D> 03-04 ]] ]] ]]") , ("keeps Δ data in a dispatched formation", "[[ k -> [[ D> 01-02 ]].plus ]]") , ("keeps a bare 'Q' bound to a named attribute", "[[ x -> Q ]]") + , ("keeps a formation bound to φ", "[[ k -> [[ @ -> [[ L> S8 ]] ]] ]]") ] ( \(desc, source) -> it desc $ do expr <- parseExpressionThrows source @@ -388,6 +398,15 @@ (\cur -> C.attribute (toName "name") cur == ["φ"] && C.attribute (toName "base") cur == ["∅"]) nested length phiVoid `shouldBe` 1 + + it "renders a formation bound to φ without an empty @base (#1189)" $ do + expr <- parseExpressionThrows "[[ x -> [[ @ -> [[ L> S8 ]] ]] ]]" + xmir' <- expressionToXMIR expr defaultXmirContext + let phis = + filter + (\cur -> C.attribute (toName "name") cur == ["φ"] && null (C.attribute (toName "base") cur)) + (C.fromDocument xmir' C.$/ C.element (toName "o") C.&/ C.element (toName "o")) + length phis `shouldBe` 1 it "renders a bare global reference as the top-level value" $ do expr <- parseExpressionThrows "[[ x -> Q ]]"