diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -234,9 +234,9 @@ {"𝑒": "⟦ bytes ↦ ⟦ … ⟧, number ↦ ⟦ … ⟧, φ ↦ … ⟧"} {"id": 1, "λ": "L_number_plus", "𝑏": "⟦ x ↦ Φ.number( … ).plus( … ) ⟧"} {"id": 7, "of": 1, "attr": "ρ", "reduce": true} -{"id": 7, "𝑛": "⟦ Δ ⤍ 40-14-00-00-00-00-00-00 ⟧"} +{"id": 7, "𝑛": "⟦ Δ ⤍ 40-14-00-00-00-00-00-00 ⟧", "Δ": "40-14-00-00-00-00-00-00"} {"id": 8, "of": 1, "attr": "x", "reduce": true} -{"id": 8, "𝑛": "⟦ Δ ⤍ 40-2A-00-00-00-00-00-00 ⟧"} +{"id": 8, "𝑛": "⟦ Δ ⤍ 40-2A-00-00-00-00-00-00 ⟧", "Δ": "40-2A-00-00-00-00-00-00"} {"id": 1, "𝑛": "Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-32-00-00-00-00-00-00 ⟧ ) )"} ``` @@ -247,8 +247,33 @@ answer is the node the attribute carries, as it was written; with `"reduce": true` it is the dataization of that node. A question about an `of` whose request is no longer in flight, or an `attr` the receiver does not carry, -fails the fire. +fails the fire. An `attr` bound to nothing at all does not: a void attribute +is a fact about the receiver, and the answer is `{"id": 7, "∅": true}`, with +no node in it, so a program may ask whether an operand is bound. +An `attr` may also go deeper than one name. It is a path down the receiver, +read left to right and split on the dot, which no attribute of 𝜑-calculus +carries in its own name: + +```text +{"id": 9, "of": 1, "attr": "ρ.length", "reduce": true} +{"id": 9, "𝑛": "⟦ Δ ⤍ 40-08-00-00-00-00-00-00 ⟧", "Δ": "40-08-00-00-00-00-00-00"} +``` + +Every segment but the last has to name a formation to go on into, and +`reduce` applies to the node the path ends at. A segment the formation does +not carry, or one that runs into a void attribute, fails the fire the same +way a missing `attr` does. `phino` holds the receiver whole, so there is no +depth a program has to re-parse an answer to reach. + +What the answered node is, `phino` says next to it, because the shape of an +answer is `phino`'s knowledge and not the program's. A formation carrying a Δ +binding carries its byte array under `Δ`, and one carrying a λ binding the name +of the function it is stuck on under `λ`, so a program tells a datum from a +stuck atom by reading the JSON and never has to parse 𝜑. Mind the `λ` there: a +line of `phino`'s is a request when it carries `𝑏` and an answer when it does +not. + The other way to ask quotes the 𝜑-expression itself, under `ask`; `phino` serves such a question by binding it to a fresh synthetic attribute of the universe, normalizing it there and dataizing it — the same trick `--inside` @@ -284,7 +309,7 @@ let minted = 0; const said = (message) => process.stdout.write(`${JSON.stringify(message)}\n`); const number = (answer) => Buffer - .from(/Δ ⤍ ([0-9A-F-]+)/.exec(answer)[1].replace(/-/g, ''), 'hex') + .from(answer['Δ'].replace(/-/g, ''), 'hex') .readDoubleBE(0); const hex = (value) => { const bytes = Buffer.alloc(8); @@ -310,12 +335,12 @@ }; readline.createInterface({ input: process.stdin }).on('line', (line) => { const message = JSON.parse(line); - if ('λ' in message) { + if ('𝑏' in message) { advance(plus(message.id), message.id, undefined); - } else if ('𝑛' in message) { + } else if (open.has(message.id)) { const waiting = open.get(message.id); open.delete(message.id); - advance(waiting.atom, waiting.id, message['𝑛']); + advance(waiting.atom, waiting.id, message); } }); ``` 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.129 +version: 0.0.130 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 @@ -53,8 +53,19 @@ -- the optional 'reduce' says whether to hand the node over as it is (false, -- by default) or to dataize it the way 'ask' does. phino serves such a -- question from the formation it already holds for that request, so neither --- side ever re-prints a receiver the other side has in hand (#1165). +-- side ever re-prints a receiver the other side has in hand (#1165). The +-- 'attr' may go deeper than one name: 'ρ.length' is a path down the receiver, +-- read left to right, since phino holds the whole of it anyway (#1207). -- +-- Whichever way it was asked, an answer says what the node under '𝑛' carries, +-- so that no program keeps a 𝜑 reader of its own to tell a datum from a stuck +-- atom: a formation with a Δ binding carries its byte array under 'Δ', one +-- with a λ binding the name of the function it is stuck on under 'λ'. An +-- attribute bound to nothing at all is a fact about the receiver and not a +-- failure of the question, so it is answered with '∅' and no node (#1206). +-- A line of phino's is a request when it carries '𝑏' and an answer when it +-- does not, since an answer may carry a 'λ' of its own. +-- -- The whole 𝜑-text on the channel is the currency of programs started for one -- fire: a kept one, able to ask for whatever the text left out, is served a -- lean one — '𝑏' and every answer carry no ρ chain, since that chain climbs @@ -90,7 +101,7 @@ import Data.Aeson.Decoding.ByteString (bsToTokens) import Data.Aeson.Decoding.Tokens (TkRecord (TkPair, TkRecordEnd, TkRecordErr), Tokens (TkErr, TkRecordOpen)) import qualified Data.Aeson.Key as Key -import Data.Aeson.Types (JSONPathElement (Key), parseEither, ()) +import Data.Aeson.Types (JSONPathElement (Key), Pair, parseEither, ()) import qualified Data.ByteString as BS import qualified Data.ByteString.Char8 as BC import qualified Data.ByteString.Lazy as BSL @@ -99,6 +110,7 @@ import Data.List (find, intercalate) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map +import Data.Maybe (mapMaybe) import qualified Data.Text as T import Data.Text.Encoding (decodeUtf8Lenient, encodeUtf8) import Encoding (Encoding (UNICODE)) @@ -106,7 +118,7 @@ import Logger (logDebug) import Margin (defaultMargin) import Parser (parseExpression) -import Printer (printAttribute, printExpression', printExpressionHidingRho') +import Printer (printAttribute, printBytes, printExpression', printExpressionHidingRho') import Sugar (SugarType (SALTY)) import System.Directory (doesFileExist, executable, getPermissions, getTemporaryDirectory, removePathForcibly) import System.Exit (ExitCode (ExitFailure, ExitSuccess)) @@ -187,6 +199,12 @@ -- stays open, so its questions can be answered. data Channel = Closed | Open +-- 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 + -- 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 -- the context to reduce under, so it hands the way down (see 'reduction' in @@ -504,38 +522,53 @@ -- formation it still holds for that request, without either side -- re-printing or re-parsing a receiver. 'reduce' says whether to dataize -- what the attribute carries, as 'ask' does, or to hand the node over as - -- it is (#1165). + -- it is (#1165). The attribute may be a dotted path, since depth is the + -- only thing such a question would otherwise be missing (#1207). referenced :: Int -> Int -> T.Text -> Bool -> IO () 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 + 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) + held <- describe + case held 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])) + Right Void -> said (lined (object ["id" .= minted, "∅" .= True])) + Right (Bound value) -> (if doReduce then reduce value else pure value) >>= said . answered minted where described :: String described = printf "{'of':%d,'attr':'%s'}" req (T.unpack attrName) - describe :: IO (Either String Expression) + describe :: IO (Either String Held) 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 attrName)) - Just form' -> case attributeValue attrName form' of + Just form' -> case descended 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 + Just held -> Right held + -- Walk the dotted path of 'attr' down the receiver: every segment but + -- the last has to name a formation to go on into, and the last one is + -- what the question is about. An attribute bound 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) + deeper :: Held -> T.Text -> Maybe Held + deeper (Bound expr) name = attributeValue name expr + deeper Void _ = Nothing + attributeValue :: T.Text -> Expression -> Maybe Held attributeValue name (ExFormation bds) = go bds where - go :: [Binding] -> Maybe Expression + go :: [Binding] -> Maybe Held go [] = Nothing go (BiTau attr value : rest) - | T.pack (printAttribute attr) == name = Just value + | named attr = Just (Bound value) | otherwise = go rest + go (BiVoid attr : rest) + | named attr = Just Void + | otherwise = go rest go (_ : rest) = go rest + named :: Attribute -> Bool + named attr = T.pack (printAttribute attr) == name 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 @@ -547,8 +580,22 @@ Open -> do logDebug (printf "Atom '%s' asks phino to reduce '%s' as question %d" (T.unpack func) (T.unpack raw) minted) target <- either (unreadable raw) pure (parseExpression (T.unpack raw)) - answer <- reduce target - said (lined (object ["id" .= minted, "𝑛" .= spelled answer])) + reduce target >>= said . answered minted + -- The answer to a question, as the line the program reads it off: the 'id' + -- the question minted, the node under '𝑛' and, next to it, what the node + -- carries — its byte array under 'Δ', the λ name it is stuck on under 'λ' + -- — so that telling a datum from a stuck atom takes no 𝜑 reader of the + -- program's own (#1206). + answered :: Int -> Expression -> BS.ByteString + answered minted answer = lined (object (["id" .= minted, "𝑛" .= spelled answer] ++ carried answer)) + where + carried :: Expression -> [Pair] + carried (ExFormation bds) = mapMaybe fact bds + carried _ = [] + fact :: Binding -> Maybe Pair + fact (BiDelta bytes) = Just ("Δ" .= printBytes bytes) + fact (BiLambda (Function name)) = Just ("λ" .= name) + fact _ = Nothing unreadable :: T.Text -> String -> IO a unreadable raw failure = throwIO (AtomMute func (T.unpack raw) (printf "it asks phino to reduce an expression that does not parse: %s" failure)) -- A program that has died leaves the write with nobody to drain it. The diff --git a/test/AtomsSpec.hs b/test/AtomsSpec.hs --- a/test/AtomsSpec.hs +++ b/test/AtomsSpec.hs @@ -81,8 +81,13 @@ -- The same, with phino reducing whatever the program asks about the given way firedFrom' :: Registry -> T.Text -> String -> ReduceFunc -> IO Expression -firedFrom' registry func universe reduce = do - form <- parseExpressionThrows "⟦ x ↦ ⟦ Δ ⤍ 01- ⟧ ⟧" +firedFrom' registry func = firedAt registry func "⟦ x ↦ ⟦ Δ ⤍ 01- ⟧ ⟧" + +-- The same, against the given receiver rather than the one every other case +-- fires at +firedAt :: Registry -> T.Text -> String -> String -> ReduceFunc -> IO Expression +firedAt registry func receiver universe reduce = do + form <- parseExpressionThrows receiver univ <- parseExpressionThrows universe maybe (fail (printf "'%s' is not registered" (T.unpack func))) (\atom -> fireAtom func atom form univ reduce) (registeredAtom registry func) @@ -147,9 +152,14 @@ -- The same, for an atom served by a resident program built of the given -- per-request snippet serves :: T.Text -> String -> Expectation -serves snippet expected = withShell $ +serves = servesAt "⟦ x ↦ ⟦ Δ ⤍ 01- ⟧ ⟧" + +-- The same, against the given receiver rather than the one every other case +-- fires at +servesAt :: String -> T.Text -> String -> Expectation +servesAt receiver snippet expected = withShell $ withServed ["L_answer"] snippet $ \registry -> do - answer <- firedFrom registry "L_answer" "⟦ y ↦ ⟦ Δ ⤍ 02- ⟧ ⟧" + answer <- firedAt registry "L_answer" receiver "⟦ y ↦ ⟦ Δ ⤍ 02- ⟧ ⟧" reducing wanted <- parseExpressionThrows expected answer `shouldBe` wanted @@ -163,9 +173,14 @@ -- The same, for a served atom refuses :: T.Text -> [String] -> Expectation -refuses snippet fragments = withShell $ +refuses = refusesAt "⟦ x ↦ ⟦ Δ ⤍ 01- ⟧ ⟧" + +-- The same, against the given receiver rather than the one every other case +-- fires at +refusesAt :: String -> T.Text -> [String] -> Expectation +refusesAt receiver snippet fragments = withShell $ withServed ["L_answer"] snippet $ \registry -> - firedFrom registry "L_answer" "⟦ y ↦ ⟦ Δ ⤍ 02- ⟧ ⟧" + firedAt registry "L_answer" receiver "⟦ y ↦ ⟦ Δ ⤍ 02- ⟧ ⟧" reducing `shouldThrow` (\failure -> all (`isInfixOf` show (failure :: SomeException)) fragments) -- The reply of a resident program answering the request with the given bytes @@ -598,6 +613,51 @@ it "fails a question about an attribute the receiver does not carry" $ refuses (referring 1 "z" False "*2A-*") ["L_answer", "carries no attribute 'z'"] + + -- The shape of an answer is phino's knowledge, not the program's, so what + -- the answered node carries is spelled next to it in the JSON and no + -- program has to keep a 𝜑 reader of its own (#1206) + it "says under 'Δ' what bytes the node of a by-reference answer carries" $ + serves (referring 1 "x" False "*'\"Δ\":\"01-\"'*") "⟦ Δ ⤍ FF- ⟧" + + it "says under 'Δ' what bytes the answer to a quoted question carries" $ + serves (asking "Q.x" "*'\"Δ\":\"2A-\"'*") "⟦ Δ ⤍ FF- ⟧" + + -- A node that is a stuck atom is told apart from a datum by the λ name it + -- is stuck on, which is the very thing a program used to read off the text + it "says under 'λ' which function the node of an answer is stuck on" $ + servesAt "⟦ x ↦ ⟦ λ ⤍ S4 ⟧ ⟧" (referring 1 "x" False "*'\"λ\":\"S4\"'*") "⟦ Δ ⤍ FF- ⟧" + + -- A void attribute is bound to nothing at all, which is a fact about the + -- receiver and not a failure of the question: a program may ask whether an + -- operand is bound and read the answer off '∅' + it "answers that the attribute a question names is void" $ + servesAt "⟦ x ↦ ⟦ Δ ⤍ 01- ⟧, v ↦ ∅ ⟧" (referring 1 "v" False "*'\"∅\":true'*") "⟦ Δ ⤍ FF- ⟧" + + -- phino holds the receiver, so depth is the only thing a question by + -- reference was missing: 'attr' is a dotted path and every segment but the + -- last has to name a formation to go on into (#1207) + it "reaches the attribute of the attribute a dotted path names" $ + servesAt "⟦ x ↦ ⟦ y ↦ ⟦ Δ ⤍ 07- ⟧ ⟧ ⟧" (referring 1 "x.y" False "*'\"Δ\":\"07-\"'*") "⟦ Δ ⤍ FF- ⟧" + + it "answers that the attribute a dotted path ends at is void" $ + servesAt "⟦ x ↦ ⟦ v ↦ ∅ ⟧ ⟧" (referring 1 "x.v" False "*'\"∅\":true'*") "⟦ Δ ⤍ FF- ⟧" + + -- What a question asks to reduce is the node its path ends at, not the one + -- the first segment names + it "reduces the node a dotted path ends at when the question asks to" $ + withShell $ + withServed ["L_answer"] (referring 1 "x.y" True "*2A-*") $ \registry -> do + seen <- newIORef Nothing + _ <- firedAt registry "L_answer" "⟦ x ↦ ⟦ y ↦ ⟦ Δ ⤍ 07- ⟧ ⟧ ⟧" "⟦ y ↦ ⟦ Δ ⤍ 02- ⟧ ⟧" (recording seen) + wanted <- parseExpressionThrows "⟦ Δ ⤍ 07- ⟧" + readIORef seen `shouldReturn` Just wanted + + it "fails a question whose dotted path names a segment the receiver lacks" $ + refusesAt "⟦ x ↦ ⟦ y ↦ ⟦ Δ ⤍ 07- ⟧ ⟧ ⟧" (referring 1 "x.z" False "*2A-*") ["L_answer", "carries no attribute 'x.z'"] + + it "fails a question whose dotted path runs into a void attribute" $ + refusesAt "⟦ v ↦ ∅ ⟧" (referring 1 "v.length" False "*2A-*") ["L_answer", "carries no attribute 'v.length'"] -- A program kept for the run is served a lean '𝑏', with no ρ chain: the -- chain climbs to the universe and compounds every question that quotes