diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -269,7 +269,7 @@ const sum = hex(number(`${b}.ρ`) + number(`${b}.x`)); process.stdout.write(`${JSON.stringify({ id: message.id, - '𝑛': `Φ.number( as-bytes ↦ Φ.bytes( data ↦ ⟦ Δ ⤍ ${sum} ⟧ ) )`, + '𝑛': `Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ ${sum} ⟧ ) )`, })}\n`); }); ``` @@ -291,8 +291,8 @@ ```bash $ cat sum.phi ⟦ - bytes(data) ↦ ⟦ φ ↦ data ⟧, - number(as-bytes) ↦ ⟦ φ ↦ as-bytes, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, + bytes ↦ ⟦ φ ↦ ∅ ⟧, + number ↦ ⟦ φ ↦ ∅, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, φ ↦ 5.plus( 6 ) ⟧ $ phino dataize --atoms=atoms.json --evaluations=atoms.tsv --quiet \ @@ -319,9 +319,9 @@ ```bash $ cat partial.phi ⟦ - bytes(data) ↦ ⟦ φ ↦ data ⟧, - number(as-bytes) ↦ ⟦ - φ ↦ as-bytes, + bytes ↦ ⟦ φ ↦ ∅ ⟧, + number ↦ ⟦ + φ ↦ ∅, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧, as-bool ↦ ⟦ λ ⤍ L_number_as_bool ⟧ @@ -375,8 +375,8 @@ ```bash $ cat two.phi ⟦ - bytes(data) ↦ ⟦ φ ↦ data ⟧, - number(as-bytes) ↦ ⟦ φ ↦ as-bytes, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, + bytes ↦ ⟦ φ ↦ ∅ ⟧, + number ↦ ⟦ φ ↦ ∅, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, φ ↦ 5.plus( 6 ).plus( 7 ) ⟧ $ phino dataize --atoms=atoms.json --sweet --hide-rho two.phi @@ -415,8 +415,8 @@ ```bash $ cat gap.phi ⟦ - bytes(data) ↦ ⟦ φ ↦ ξ.data ⟧, - number(as-bytes) ↦ ⟦ φ ↦ ξ.as-bytes, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧, + bytes ↦ ⟦ φ ↦ ∅ ⟧, + number ↦ ⟦ φ ↦ ∅, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧, bar(x) ↦ ⟦ λ ⤍ L_bar ⟧, demo ↦ ⟦ foo ↦ ⟦ n ↦ 3, φ ↦ Φ.bar( ξ.n.times( 5 ).times( 7 ) ) ⟧ ⟧ ⟧ @@ -451,8 +451,8 @@ ```bash $ phino morph --deep --atoms=atoms.json --sweet --hide-rho gap.phi ⟦ - bytes(data) ↦ ⟦ φ ↦ data ⟧, - number(as-bytes) ↦ ⟦ φ ↦ as-bytes, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧, + bytes(φ) ↦ ⟦⟧, + number(φ) ↦ ⟦ times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧, bar(x) ↦ ⟦ λ ⤍ L_bar ⟧, demo ↦ ⟦ foo ↦ ⟦ n ↦ 3, φ ↦ Φ.bar( 105 ) ⟧ ⟧ ⟧ @@ -528,12 +528,9 @@ $ echo '[[ @ -> Q.io.stdout("hello") ]]' | phino rewrite ⟦ φ ↦ Φ.io.stdout( - α0 ↦ Φ.string( - α0 ↦ Φ.bytes( - α0 ↦ ⟦ Δ ⤍ 68-65-6C-6C-6F ⟧ - ) - ) - ) + α0 ↦ Φ.string( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 68-65-6C-6C-6F, ρ ↦ ∅ ⟧ ) ) + ), + ρ ↦ ∅ ⟧ ``` @@ -544,11 +541,11 @@ ```bash $ cat bytes.phi -⟦ bytes(data) ↦ ⟦ φ ↦ data ⟧ ⟧ +⟦ bytes ↦ ⟦ φ ↦ ∅ ⟧ ⟧ $ cat number.phi ⟦ - number(as-bytes) ↦ ⟦ - φ ↦ as-bytes, + number ↦ ⟦ + φ ↦ ∅, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ ⟧ @@ -556,9 +553,8 @@ ⟦ number ↦ ⟦ minus(x) ↦ ⟦ λ ⤍ L_number_minus ⟧ ⟧ ⟧ $ phino merge bytes.phi number.phi minus.phi --sweet ⟦ - bytes(data) ↦ ⟦ φ ↦ data ⟧, - number(as-bytes) ↦ ⟦ - φ ↦ as-bytes, + bytes(φ) ↦ ⟦⟧, + number(φ) ↦ ⟦ plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, minus(x) ↦ ⟦ λ ⤍ L_number_minus ⟧ ⟧ 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.122 +version: 0.0.123 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at diff --git a/src/AST.hs b/src/AST.hs --- a/src/AST.hs +++ b/src/AST.hs @@ -202,10 +202,10 @@ -- Minimal matcher function (required for view pattern) -- --- The primitive→bytes binding is named 'as-bytes' and the bytes→payload --- binding is named 'data' (jeo-maven-plugin 0.15.3+, following phi-calculus --- dropping positional attributes). The legacy positional α0 form is still --- recognized so XMIR produced by older jeo versions keeps sugaring back. +-- Both bindings of a literal are named φ, the only void that the real +-- 'number', 'string' and 'bytes' declare ([@] > number, see #1155). The +-- legacy 'as-bytes', 'data' and positional α0 forms are still recognized +-- so XMIR produced by older jeo versions keeps sugaring back. matchDataObject :: Expression -> Maybe (T.Text, Bytes) matchDataObject (ExApplication outer arg) | Just inner <- asBytesArg arg = case (matchOuter outer, matchInner inner) of @@ -213,6 +213,7 @@ _ -> Nothing where asBytesArg :: Argument -> Maybe Expression + asBytesArg (ArTau AtPhi inner) = Just inner asBytesArg (ArTau (AtLabel "as-bytes") inner) = Just inner asBytesArg (ArAlpha (Alpha 0) inner) = Just inner asBytesArg _ = Nothing @@ -254,10 +255,10 @@ pattern DataObject label bts <- (matchDataObject -> Just (label, bts)) where DataObject label bts = - ExApplication (BaseObject label) (ArTau (AtLabel "as-bytes") (dataBytes bts)) + ExApplication (BaseObject label) (ArTau AtPhi (dataBytes bts)) -- The bytes object Φ.bytes(φ ↦ ⟦ Δ ⤍ …, ρ ↦ ∅ ⟧) — what a 'bytes' atom --- yields and what a 'DataObject' carries under its 'as-bytes' argument. +-- yields and what a 'DataObject' carries under its φ argument. -- The payload is bound to 'φ', the void that the real 'bytes' object -- declares ([@] > bytes), so that every dispatch on the literal can bind -- (see #1142) diff --git a/src/Sugar.hs b/src/Sugar.hs --- a/src/Sugar.hs +++ b/src/Sugar.hs @@ -207,7 +207,7 @@ ( AA_TAUS ( BI_PAIR ( PA_TAU - (AT_LABEL "as-bytes") + (AT_PHI PHI) ARROW ( EX_APPLICATION bytes diff --git a/src/XMIR.hs b/src/XMIR.hs --- a/src/XMIR.hs +++ b/src/XMIR.hs @@ -113,7 +113,7 @@ expression (DataNumber bytes) XmirContext{..} = let bts = object - [("as", "as-bytes"), ("base", "Φ.bytes")] + [("as", "φ"), ("base", "Φ.bytes")] [object [("as", "φ")] [NodeContent (T.pack (printBytes bytes))]] in pure ( "Φ.number" @@ -127,7 +127,7 @@ expression (DataString bytes) XmirContext{..} = let bts = object - [("as", "as-bytes"), ("base", "Φ.bytes")] + [("as", "φ"), ("base", "Φ.bytes")] [object [("as", "φ")] [NodeContent (T.pack (printBytes bytes))]] in pure ( "Φ.string" diff --git a/test/ASTSpec.hs b/test/ASTSpec.hs --- a/test/ASTSpec.hs +++ b/test/ASTSpec.hs @@ -299,15 +299,20 @@ (ArTau AtPhi (ExFormation [BiDelta (BtOne "48"), BiVoid AtRho])) describe "DataObject/DataString/DataNumber pattern" $ do - it "constructs the named, unwrapped as-bytes form" $ + it "constructs the phi-named, unwrapped form" $ DataString (BtOne "48") `shouldBe` ExApplication (ExDispatch ExRoot (AtLabel "string")) - (ArTau (AtLabel "as-bytes") (dataBytes (BtOne "48"))) + (ArTau AtPhi (dataBytes (BtOne "48"))) forM_ [ - ( "matches the named, unwrapped form" + ( "matches the phi-named, unwrapped form" + , ExApplication (ExDispatch ExRoot (AtLabel "string")) (ArTau AtPhi (dataBytes (BtOne "48"))) + , Just (BtOne "48") + ) + , + ( "matches the legacy as-bytes name on the outer binding" , ExApplication (ExDispatch ExRoot (AtLabel "string")) (ArTau (AtLabel "as-bytes") (dataBytes (BtOne "48"))) , Just (BtOne "48") ) diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -425,7 +425,7 @@ it "saves dataize steps to dir with --steps-dir" $ withAtoms $ \atoms -> withTempDirectory "phino-steps-dataize" $ \dir -> - withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $ do + withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $ do testCLISucceeded ["dataize", atoms, "--steps-dir=" ++ dir, "--sweet"] ["40-32"] @@ -1146,14 +1146,14 @@ it "focuses a compressed sequence whose meet replaces a step root" $ withAtoms $ \atoms -> - withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $ + withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $ testCLISucceeded ["dataize", atoms, "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--hide=Q.bytes", "--hide=Q.number", "--locator=Q.@", "--focus=Q.@", "--meet-length=5", "--meet-popularity=1"] ["\\phinoMeet{dataization:1}{ [[ @ -> |c| . |plus| ( 32 ), |c| -> 25 ]] } \\leadsto_{\\nameref{r:contextualize}}"] it "compresses a canonized whole-expression sequence into a meet" $ withAtoms $ \atoms -> - withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $ + withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $ testCLISucceeded ["dataize", atoms, "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--meet-length=5", "--meet-popularity=1"] ["\\phinoMeet{dataization:1}"] @@ -1171,7 +1171,7 @@ withAtoms $ \atoms -> withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do hClose stream - withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ + withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ testCLISucceeded ["dataize", atoms, "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readUtf8 path records `shouldBe` "L_number_plus\t⟦ x ↦ 6 ⟧\t11\n" @@ -1180,7 +1180,7 @@ withAtoms $ \atoms -> withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do hClose stream - withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $ + withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $ testCLISucceeded ["dataize", atoms, "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readUtf8 path lines records `shouldBe` ["L_number_plus\t⟦ x ↦ 6 ⟧\t11", "L_number_plus\t⟦ x ↦ 7 ⟧\t18"] @@ -1189,16 +1189,16 @@ withAtoms $ \atoms -> withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do hClose stream - withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ + withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ testCLISucceeded ["dataize", atoms, "--evaluations=" ++ path, "--quiet", "--hide-rho"] [] records <- readUtf8 path - records `shouldEndWith` "\tΦ.number( as-bytes ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-26-00-00-00-00-00-00 ⟧ ) )\n" + records `shouldEndWith` "\tΦ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-26-00-00-00-00-00-00 ⟧ ) )\n" it "keeps the records of a run that fails" $ withAtoms $ \atoms -> withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do hClose stream - withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]], nope -> [[ L> L_number_nope ]] ]], @ -> 5.plus(6).nope ]]" $ + withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(x) -> [[ L> L_number_plus ]], nope -> [[ L> L_number_nope ]] ]], @ -> 5.plus(6).nope ]]" $ testCLIFailed ["dataize", atoms, "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] ["Atom 'L_number_nope' does not exist"] @@ -1229,7 +1229,7 @@ -- an operation the caller left out of its registry on purpose. The run used -- to die on it, discarding what it had already evaluated (#1060) describe "--partial" $ do - let stuck = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, times(x) -> [[ L> L_number_times ]], nope -> [[ L> L_number_nope ]] ]], @ -> 2.times(3).nope ]]" + let stuck = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ times(x) -> [[ L> L_number_times ]], nope -> [[ L> L_number_nope ]] ]], @ -> 2.times(3).nope ]]" it "fails on an atom that cannot fire without the flag" $ withAtoms $ \atoms -> withStdin stuck $ @@ -1247,7 +1247,7 @@ withStdin stuck $ testCLISucceeded ["dataize", atoms, "--partial", "--sweet"] - ["as-bytes ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-18-00-00-00-00-00-00 ⟧ )"] + ["φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-18-00-00-00-00-00-00 ⟧ )"] it "records every stuck site in --evaluations with no result" $ withAtoms $ \atoms -> @@ -1263,7 +1263,7 @@ it "still prints bytes when nothing gets stuck" $ withAtoms $ \atoms -> - withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ + withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ testCLISucceeded ["dataize", atoms, "--partial"] ["40-26-00-00-00-00-00-00"] it "prints the chain of steps ending in the residue with --sequence" $ @@ -1280,7 +1280,7 @@ -- Which λ functions exist is not phino's business any more: the registry -- given with '--atoms' decides, and phino carries none of its own describe "--atoms" $ do - let sum' = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" + let sum' = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" it "fires the λ function the registry carries" $ withAtoms $ \atoms -> withStdin sum' $ @@ -1310,7 +1310,7 @@ -- asks phino for them: '--inside' binds an expression to a synthetic -- attribute of the universe and aims the run at it describe "--inside" $ do - let universe = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> [[ D> 01- ]] ]]" + let universe = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(x) -> [[ L> L_number_plus ]] ]], @ -> [[ D> 01- ]] ]]" it "dataizes an expression the input does not contain" $ withAtoms $ \atoms -> withStdin universe $ @@ -1401,7 +1401,7 @@ -- Two chained atom calls: the inner one fires under 'ml', because '.plus' -- is dispatched on its result, while the outer application is saturated but -- bare, so 'mf' hands it back and firing it is 𝔻's job - let chained = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" + let chained = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" it "prints help" $ testCLISucceeded ["morph", "--help"] ["Morph the 𝜑-expression"] @@ -1521,7 +1521,7 @@ describe "--deep" $ do let program = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, \ - \number(as-bytes) -> [[ @ -> $.as-bytes, times(x) -> [[ L> L_number_times ]] ]], \ + \number(φ) -> [[ times(x) -> [[ L> L_number_times ]] ]], \ \bar(x) -> [[ L> L_bar ]], \ \demo -> [[ foo -> [[ n -> 3, @ -> Q.bar( $.n.times( 5 ).times( 7 ) ) ]] ]] ]]" it "answers the formation as it was written without the flag" $ @@ -1558,7 +1558,7 @@ withStdin program $ testCLISucceeded ["morph", atoms, "--deep", "--sweet", "--hide-rho", "--flat"] - [ "number(as-bytes) ↦ ⟦ φ ↦ as-bytes, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧" + [ "number(φ) ↦ ⟦ times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧" , "demo ↦ ⟦ foo ↦ ⟦ n ↦ 3, φ ↦ Φ.bar( 105 ) ⟧ ⟧" ] diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -107,8 +107,8 @@ , " eq -> [[ b -> ?, L> L_bytes_eq ]]" , " ]]," , " number -> [[" - , " as-bytes -> ?," - , " @ -> $.as-bytes," + , " φ -> ?," + , " as-bytes -> $.φ," , " plus -> [[ x -> ?, L> L_number_plus ]]," , " times -> [[ x -> ?, L> L_number_times ]]," , " div -> [[ x -> ?, L> L_number_div ]]," @@ -116,7 +116,7 @@ , " eq -> [[ x -> ?, @ -> $.^.as-bytes.eq( x.as-bytes ) ]]," , " nope -> [[ L> L_number_nope ]]" , " ]]," - , " string -> [[ as-bytes -> ?, @ -> $.as-bytes ]]," + , " string -> [[ φ -> ?, as-bytes -> $.φ ]]," , " true -> [[ @ -> [[ D> FF- ]] ]]," , " false -> [[ @ -> [[ D> 00- ]] ]]," , " @ -> " ++ src @@ -222,25 +222,25 @@ ( "stands the answer of the λ that 'mf' left bare in its place" , "Q.@" , primitives "[[ x -> 5.plus( 6 ) ]]" - , "[[ x -> Q.number( as-bytes -> Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-26-00-00-00-00-00-00 ⟧ ) ) ]]" + , "[[ x -> Q.number( φ -> Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-26-00-00-00-00-00-00 ⟧ ) ) ]]" ) , ( "fires the atom nested in the argument of the atom it fires" , "Q.@" , primitives "[[ x -> 5.plus( 6.plus( 7 ) ) ]]" - , "[[ x -> Q.number( as-bytes -> Q.bytes( data -> [[ D> 40-32-00-00-00-00-00-00 ]] ) ) ]]" + , "[[ x -> Q.number( φ -> Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-32-00-00-00-00-00-00 ⟧ ) ) ]]" ) , ( "keeps the answer of the last atom fired along one chain of them" , "Q.@" , primitives "[[ x -> 5.plus( 6 ).plus( 7 ) ]]" - , "[[ x -> Q.number( as-bytes -> Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-32-00-00-00-00-00-00 ⟧ ) ) ]]" + , "[[ x -> Q.number( φ -> Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-32-00-00-00-00-00-00 ⟧ ) ) ]]" ) , ( "resolves the ξ of a binding against the formation that holds it" , "Q.@" , primitives "[[ n -> 5, x -> $.n.plus( 6 ) ]]" - , "[[ n -> 5, x -> Q.number( as-bytes -> Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-26-00-00-00-00-00-00 ⟧ ) ) ]]" + , "[[ n -> 5, x -> Q.number( φ -> Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-26-00-00-00-00-00-00 ⟧ ) ) ]]" ) , -- The registry carries no 'L_number_nope', so there is nothing to fire -- and the binding keeps the name it was written under @@ -267,7 +267,7 @@ ( "walks into the argument of an atom it cannot fire" , "Q.@" , primitives "[[ x -> [[ y -> ?, L> L_bar ]]( y -> 6.plus( 7 ) ) ]]" - , "[[ x -> [[ y -> ?, L> L_bar ]]( y -> Q.number( as-bytes -> Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-2A-00-00-00-00-00-00 ⟧ ) ) ) ]]" + , "[[ x -> [[ y -> ?, L> L_bar ]]( y -> Q.number( φ -> Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-2A-00-00-00-00-00-00 ⟧ ) ) ) ]]" ) ] @@ -711,7 +711,7 @@ labels <- labelsOf "Q" - "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" + "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" labels `shouldBe` [ "contextualize" , "maa" @@ -723,9 +723,8 @@ , "copy" , "mf" , "contextualize" - , "dot" , "ma" - , "stay" + , "copy" , "mf" , "contextualize" , "delta" @@ -765,7 +764,7 @@ , "Q.x" , unlines [ "[[" - , " number(as-bytes) -> [[ @ -> as-bytes ]]," + , " number ↦ ⟦ φ ↦ ∅ ⟧," , " bytes ↦ ⟦ φ ↦ ∅ ⟧," , " x -> 5" , "]]" @@ -827,8 +826,8 @@ , " φ -> ?" , " ]]," , " number -> [[" - , " as-bytes -> ?," - , " @ -> $.as-bytes," + , " φ -> ?," + , " as-bytes -> $.φ," , " plus -> [[ x -> ?, L> L_number_plus ]]," , " times -> [[ x -> ?, L> L_number_times ]]" , " ]]," diff --git a/test/PrinterSpec.hs b/test/PrinterSpec.hs --- a/test/PrinterSpec.hs +++ b/test/PrinterSpec.hs @@ -146,6 +146,19 @@ str `shouldContain` "φ ↦" str `shouldNotContain` "data ↦" + describe "printExpression binds a datum to the φ of number and string (#1155)" $ + it "names the outer literal argument φ (their only void), not as-bytes" $ do + let number = + printExpression' + (DataNumber (BtMany ["40", "45", "00", "00", "00", "00", "00", "00"])) + (SALTY, UNICODE, SINGLELINE, defaultMargin) + str = + printExpression' + (DataString (BtMany ["68", "69"])) + (SALTY, UNICODE, SINGLELINE, defaultMargin) + number `shouldNotContain` "as-bytes" + str `shouldNotContain` "as-bytes" + describe "printExpression keeps a compressed meet atomic under a narrow margin" $ -- A \phinoMeet is a single \overbracket visual unit, so its body must stay -- on one line even when the surrounding margin forces the outer formation to diff --git a/test/SugarSpec.hs b/test/SugarSpec.hs --- a/test/SugarSpec.hs +++ b/test/SugarSpec.hs @@ -211,47 +211,47 @@ , ( "EX_NUMBER with no extra rho expands into the Q.number(Q.bytes(...)) form" , EX_NUMBER (Left 42) (TAB 1) [] - , "Φ.number(\n as-bytes ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 40-45-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.number(\n φ ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 40-45-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )" ) , ( "EX_NUMBER preserves an extra rho argument carried alongside the primitive" , EX_NUMBER (Left 42) (TAB 1) [ArTau AtRho (ExDispatch ExXi (AtLabel "y"))] - , "Φ.number(\n as-bytes ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 40-45-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )(\n ρ ↦ ξ.y\n )" + , "Φ.number(\n φ ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 40-45-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )(\n ρ ↦ ξ.y\n )" ) , ( "EX_NONFINITE nan expands into the Q.number(Q.bytes(...)) form" , EX_NONFINITE Φ NfNan (TAB 1) [] - , "Φ.number(\n as-bytes ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 7F-F8-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.number(\n φ ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 7F-F8-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )" ) , ( "EX_NONFINITE pinf expands into the Q.number(Q.bytes(...)) form" , EX_NONFINITE Φ NfPinf (TAB 1) [] - , "Φ.number(\n as-bytes ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 7F-F0-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.number(\n φ ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 7F-F0-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )" ) , ( "EX_NONFINITE ninf keeps an extra rho argument carried alongside the primitive" , EX_NONFINITE Φ NfNinf (TAB 1) [ArTau AtRho (ExDispatch ExXi (AtLabel "y"))] - , "Φ.number(\n as-bytes ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ FF-F0-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )(\n ρ ↦ ξ.y\n )" + , "Φ.number(\n φ ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ FF-F0-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )(\n ρ ↦ ξ.y\n )" ) , ( "EX_STRING expands into the Q.string(Q.bytes(...)) form" , EX_STRING "hi" (TAB 1) [] - , "Φ.string(\n as-bytes ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 68-69,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.string(\n φ ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 68-69,\n ρ ↦ ∅\n ⟧\n )\n )" ) , ( "EX_STRING unescapes a newline instead of taking its escape literally" , EX_STRING "e\\ne" (TAB 1) [] - , "Φ.string(\n as-bytes ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 65-0A-65,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.string(\n φ ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 65-0A-65,\n ρ ↦ ∅\n ⟧\n )\n )" ) , ( "EX_STRING unescapes a quote and a backslash into single bytes" , EX_STRING "\\\"\\\\" (TAB 1) [] - , "Φ.string(\n as-bytes ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 22-5C,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.string(\n φ ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 22-5C,\n ρ ↦ ∅\n ⟧\n )\n )" ) , ( "EX_STRING unescapes a hex escape back into its byte" , EX_STRING "\\x01" (TAB 1) [] - , "Φ.string(\n as-bytes ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 01-,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.string(\n φ ↦ Φ.bytes(\n φ ↦ ⟦\n Δ ⤍ 01-,\n ρ ↦ ∅\n ⟧\n )\n )" ) ] (\(desc, sweetExpr, expected) -> it desc (render (toSalty sweetExpr) `shouldBe` expected)) @@ -628,13 +628,13 @@ $ do let number = DataNumber (BtMany ["40", "45", "00", "00", "00", "00", "00", "00"]) printExpression' number (config SWEET) `shouldBe` "42" - printExpression' number (config SALTY) `shouldBe` "Φ.number( as-bytes ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00, ρ ↦ ∅ ⟧ ) )" + printExpression' number (config SALTY) `shouldBe` "Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00, ρ ↦ ∅ ⟧ ) )" it "a sweet string literal expands into Q.string(Q.bytes(...)) when salted" $ do let string = DataString (BtMany ["68", "69"]) printExpression' string (config SWEET) `shouldBe` "\"hi\"" - printExpression' string (config SALTY) `shouldBe` "Φ.string( as-bytes ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 68-69, ρ ↦ ∅ ⟧ ) )" + printExpression' string (config SALTY) `shouldBe` "Φ.string( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 68-69, ρ ↦ ∅ ⟧ ) )" it "an application with multiple positional arguments sugars/salts between e(e0, e1) and e(α0 ↦ e0)(α1 ↦ e1)" $ do