phino 0.0.129 → 0.0.130

raw patch · 4 files changed

+164/−32 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• README.md +32/−7
• phino.cabal +1/−1
• src/Atoms.hs +65/−18
• test/AtomsSpec.hs +66/−6

@@ -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);   } }); ```

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

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

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