diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -274,6 +274,23 @@ line of `phino`'s is a request when it carries `𝑏` and an answer when it does not. +An answer that is an application rather than a formation says under `Φ.` the +chain it is dispatched off Φ by: + +```text +{"id": 9, "of": 1, "attr": "x"} +{"id": 9, "𝑛": "Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-08-… ⟧ ) )", "Φ.": "number"} +``` + +That name is the only place the forma of a typed literal lives, since +𝜑-calculus types nothing nominally: `Φ.true` says `true`, +`Φ.tuple( length ↦ …, head ↦ …, tail ↦ … )` says `tuple`, and a chain spelled +in full says `org.eolang.number`. Dataize the same operand instead and the +forma is gone, because `Δ` is all that is left of a number taken apart. A +chain with an application inside it, such as `Φ.number( … ).plus( … )`, +dispatches off a term `phino` would have to dataize to name, so it names no +forma and nothing is said. + 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` 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.130 +version: 0.0.131 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 @@ -63,6 +63,10 @@ -- 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). +-- An answer that is not a formation but an application says under 'Φ.' the +-- chain it is dispatched off Φ by — 'number' for 'Φ.number( φ ↦ … )' — since +-- 𝜑-calculus types nothing nominally and that name is the only place the +-- forma of a typed literal lives (#1210). -- 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. -- @@ -583,19 +587,36 @@ 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). + -- carries — its byte array under 'Δ', the λ name it is stuck on under 'λ', + -- the chain it is dispatched off Φ by under 'Φ.' — so that telling a datum + -- from a stuck atom, or a typed literal from either, takes no 𝜑 reader of + -- the program's own (#1206, #1210). 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 _ = [] + carried expr = maybe [] (\forma -> ["Φ." .= forma]) (dispatched expr) fact :: Binding -> Maybe Pair fact (BiDelta bytes) = Just ("Δ" .= printBytes bytes) fact (BiLambda (Function name)) = Just ("λ" .= name) fact _ = Nothing + -- The chain the answer is dispatched off Φ by, once the arguments + -- applied to it are stripped: 'number' for 'Φ.number( φ ↦ … )', 'true' + -- for 'Φ.true', 'org.eolang.tuple' for a chain that deep. 𝜑-calculus + -- types nothing nominally, so that name is the only place the forma of + -- a typed literal lives. A chain with an application inside it, such as + -- 'Φ.number( … ).plus( … )', dispatches off a term phino would have to + -- dataize to name, so it names no forma and nothing is said (#1210). + dispatched :: Expression -> Maybe T.Text + dispatched (ExApplication applied _) = dispatched applied + dispatched expr = case chain expr of + Just names@(_ : _) -> Just (T.intercalate "." names) + _ -> Nothing + chain :: Expression -> Maybe [T.Text] + chain ExRoot = Just [] + chain (ExDispatch applied attr) = (++ [T.pack (printAttribute attr)]) <$> chain applied + chain _ = 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 @@ -659,6 +659,39 @@ 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'"] + -- 𝜑-calculus types nothing nominally, so the forma of a typed literal + -- lives in the name it is dispatched off Φ by and nowhere else: an answer + -- that is an application spells that name, the way a formation spells its + -- Δ and its λ (#1210) + it "says under 'Φ.' the forma a typed literal is dispatched by" $ + servesAt + "⟦ x ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-08-00-00-00-00-00-00 ⟧ ) ) ⟧" + (referring 1 "x" False "*'\"Φ.\":\"number\"'*") + "⟦ Δ ⤍ FF- ⟧" + + it "says under 'Φ.' the forma of an object taking no argument at all" $ + servesAt "⟦ x ↦ Φ.true ⟧" (referring 1 "x" False "*'\"Φ.\":\"true\"'*") "⟦ Δ ⤍ FF- ⟧" + + it "says under 'Φ.' the forma of an object taking several arguments" $ + servesAt + "⟦ x ↦ Φ.tuple( length ↦ ⟦ Δ ⤍ 01- ⟧, head ↦ ⟦ Δ ⤍ 02- ⟧, tail ↦ ⟦ Δ ⤍ 03- ⟧ ) ⟧" + (referring 1 "x" False "*'\"Φ.\":\"tuple\"'*") + "⟦ Δ ⤍ FF- ⟧" + + it "says under 'Φ.' the whole chain a forma is spelled by" $ + servesAt + "⟦ x ↦ Φ.org.eolang.number( φ ↦ ⟦ Δ ⤍ 01- ⟧ ) ⟧" + (referring 1 "x" False "*'\"Φ.\":\"org.eolang.number\"'*") + "⟦ Δ ⤍ FF- ⟧" + + -- A chain with an application inside it names no forma, since what it + -- dispatches off is a term phino would have to dataize to know + it "stays silent about an answer whose chain has an application inside it" $ + servesAt + "⟦ x ↦ Φ.number( φ ↦ ⟦ Δ ⤍ 01- ⟧ ).plus( y ↦ ⟦ Δ ⤍ 02- ⟧ ) ⟧" + (referring 1 "x" False "*'\"Φ.\":'*") + "⟦ Δ ⤍ 00- ⟧" + -- 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 -- its receiver, and whatever the lean text leaves out this program can