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.128 +cabal install --overwrite-policy=always phino-0.0.132 phino --version ``` @@ -946,55 +946,55 @@ === parse/phi === warmup: 3 iterations batches: 10 x 1 - total: 1234878.258 μs - avg: 123487.826 μs - min: 114898.378 μs - max: 147448.578 μs - std dev: 12608.859 μs + total: 1333129.634 μs + avg: 133312.963 μs + min: 123350.827 μs + max: 154501.079 μs + std dev: 11819.397 μs === parse/xmir === warmup: 3 iterations batches: 10 x 1 - total: 6115346.630 μs - avg: 611534.663 μs - min: 553273.770 μs - max: 658997.433 μs - std dev: 26432.183 μs + total: 6095344.927 μs + avg: 609534.493 μs + min: 552583.460 μs + max: 644040.036 μs + std dev: 25360.610 μs === rewrite/normalize === warmup: 3 iterations batches: 10 x 1 - total: 521385.086 μs - avg: 52138.509 μs - min: 46636.826 μs - max: 63889.183 μs - std dev: 5808.082 μs + total: 562461.372 μs + avg: 56246.137 μs + min: 54840.174 μs + max: 57549.116 μs + std dev: 778.435 μs === print/sweet/multiline === warmup: 3 iterations batches: 10 x 1 - total: 3741073.589 μs - avg: 374107.359 μs - min: 344671.911 μs - max: 406026.195 μs - std dev: 18304.000 μs + total: 2804710.586 μs + avg: 280471.059 μs + min: 263431.677 μs + max: 306476.931 μs + std dev: 12002.611 μs === print/sweet/flat === warmup: 3 iterations batches: 10 x 1 - total: 3807236.850 μs - avg: 380723.685 μs - min: 366420.230 μs - max: 395219.831 μs - std dev: 9900.160 μs + total: 2784962.131 μs + avg: 278496.213 μs + min: 264622.121 μs + max: 291750.726 μs + std dev: 10124.274 μs === print/salty/multiline === warmup: 3 iterations batches: 10 x 1 - total: 11573351.855 μs - avg: 1157335.186 μs - min: 1122778.266 μs - max: 1213750.752 μs - std dev: 26107.625 μs + total: 9124364.174 μs + avg: 912436.417 μs + min: 892913.298 μs + max: 935173.006 μs + std dev: 15007.336 μs ``` The results were calculated in [this GHA job][benchmark-gha] -on 2026-09-11 at 18:19, +on 2026-09-14 at 19:01, on Linux with 4 CPUs. @@ -1043,4 +1043,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/34632126707 +[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/34883926782 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.132 +version: 0.0.133 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 @@ -98,6 +98,7 @@ where import AST +import Builder (contextualize) import Control.Concurrent.MVar (MVar, modifyMVar, modifyMVar_, newMVar) import Control.Exception (Exception, catch, onException, throwIO) import Control.Monad (foldM, unless) @@ -208,8 +209,11 @@ -- What the receiver of a request holds under an attribute a question names: -- the node bound to it, or nothing at all, since the attribute is void. A void -- one is a fact about the receiver and not a failure of the question, so a --- program may ask whether an operand is bound and be told (#1206). -data Held = Bound Expression | Void +-- program may ask whether an operand is bound and be told (#1206). A bound one +-- is held twice over: as it is written, which is what a question that does not +-- reduce is answered with, and with its ξ standing for the formation it is +-- bound in, which is the only shape of it that reduces anywhere else (#1220). +data Held = Bound Expression Expression | Void -- How phino reduces a 𝜑-expression a program asks about. Only the caller of -- 'fireAtom' can do it, since it alone holds the universe to reduce inside and @@ -539,7 +543,7 @@ case held of Left failure -> throwIO (AtomMute func described failure) Right Void -> said (lined (object ["id" .= minted, "∅" .= True])) - Right (Bound value) -> (if doReduce then reduce value else pure value) >>= said . answered minted + Right (Bound written scoped) -> (if doReduce then reduce scoped else pure written) >>= said . answered minted where described :: String described = printf "{'of':%d,'attr':'%s'}" req (T.unpack attrName) @@ -557,29 +561,34 @@ -- to nothing at all carries nothing to descend into, so a path through -- a void one names no attribute (#1207). descended :: Expression -> Maybe Held - descended form' = foldM deeper (Bound form') (T.splitOn "." attrName) + descended form' = foldM deeper (Bound form' form') (T.splitOn "." attrName) deeper :: Held -> T.Text -> Maybe Held - deeper (Bound expr) name = attributeValue name expr + deeper (Bound _ scoped) name = attributeValue name scoped deeper Void _ = Nothing -- An argument of an application binds an attribute the way a τ -- binding of a formation does, and it is the outer of the two, so it -- is what the attribute is whatever the formation under it still says -- about it. A positional argument names nothing, so the walk goes past - -- it into what the application applies to (#1212). + -- it into what the application applies to (#1212). The ξ of a node + -- bound in a formation stands for that formation, so a node taken out + -- of one carries it along, the way the 'dot' rule does when it + -- dispatches the same attribute; an argument, written in the scope + -- around the application and contextualized long before a request + -- reaches this far, stands for itself (#1220). attributeValue :: T.Text -> Expression -> Maybe Held - attributeValue name (ExFormation bds) = go bds + attributeValue name form'@(ExFormation bds) = go bds where go :: [Binding] -> Maybe Held go [] = Nothing go (BiTau attr value : rest) - | named name attr = Just (Bound value) + | named name attr = Just (Bound value (contextualize value form')) | otherwise = go rest go (BiVoid attr : rest) | named name attr = Just Void | otherwise = go rest go (_ : rest) = go rest attributeValue name (ExApplication applied (ArTau attr value)) - | named name attr = Just (Bound value) + | named name attr = Just (Bound value value) | otherwise = attributeValue name applied attributeValue name (ExApplication applied _) = attributeValue name applied attributeValue _ _ = Nothing diff --git a/test/AtomsSpec.hs b/test/AtomsSpec.hs --- a/test/AtomsSpec.hs +++ b/test/AtomsSpec.hs @@ -606,6 +606,24 @@ wanted <- parseExpressionThrows "⟦ Δ ⤍ 01- ⟧" readIORef seen `shouldReturn` Just wanted + -- The ξ of a node bound in a formation stands for that formation, so a + -- node leaving one to be reduced elsewhere takes it along, the way the + -- 'dot' rule does. Without it the body of the very formation being fired + -- is the one node no question can reduce, since its ξ finds nothing where + -- the reduction binds it (#1220) + it "binds the ξ of the node it reduces to the formation the node came from" $ + withShell $ + withServed ["L_answer"] (referring 1 "φ" True "*2A-*") $ \registry -> do + seen <- newIORef Nothing + _ <- firedAt registry "L_answer" "⟦ a ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ξ.a ⟧" "⟦ y ↦ ⟦ Δ ⤍ 02- ⟧ ⟧" (recording seen) + wanted <- parseExpressionThrows "⟦ a ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ξ.a ⟧.a" + readIORef seen `shouldReturn` Just wanted + + -- A question that does not reduce is answered with the node as it is + -- written, ξ and all, since binding that ξ is what reducing does + it "leaves the ξ of a node alone when the question does not reduce it" $ + servesAt "⟦ a ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ξ.a ⟧" (referring 1 "φ" False "*'ξ.a'*") "⟦ Δ ⤍ FF- ⟧" + -- A receiver is of no use to the channel once its request has been -- answered, and a question may not dig out of it after that it "fails a question about a request that is no longer in flight" $ diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -450,6 +450,26 @@ withStdin "⟦ @ ↦ ⟦ λ ⤍ L_answer ⟧ ⟧" $ testCLISucceeded ["dataize", "--atoms=" ++ registry] ["2A-"] + -- The body of the formation being fired is what a program asks phino to + -- reduce for it, and the ξ of that body stands for the very formation the + -- program was handed, so the whole of it goes through the command line + -- here: the question names 'φ', the answer brings what ξ.a reached (#1220) + it "dataizes with an atom whose question reduces a body written with ξ" + $ withShell + $ withServing + ( T.unlines + [ T.pack "printf '{\"id\": 7, \"of\": %s, \"attr\": \"φ\", \"reduce\": true}\\n' \"$id\"" + , T.pack "IFS= read -r reply" + , T.pack "case \"$reply\" in" + , T.pack " *01-02*) printf '{\"id\": %s, \"𝑛\": \"⟦ Δ ⤍ 2A- ⟧\"}\\n' \"$id\";;" + , T.pack " *) printf '{\"id\": %s, \"𝑛\": \"⟦ Δ ⤍ 00- ⟧\"}\\n' \"$id\";;" + , T.pack "esac" + ] + ) + $ \registry -> + withStdin "⟦ @ ↦ ⟦ a ↦ ⟦ Δ ⤍ 01-02 ⟧, φ ↦ ξ.a, λ ⤍ L_answer ⟧ ⟧" $ + testCLISucceeded ["dataize", "--atoms=" ++ registry] ["2A-"] + it "saves dataize steps to dir with --steps-dir" $ withAtoms $ \atoms -> withTempDirectory "phino-steps-dataize" $ \dir ->