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.118 +cabal install --overwrite-policy=always phino-0.0.121 phino --version ``` @@ -842,55 +842,55 @@ === parse/phi === warmup: 3 iterations batches: 10 x 1 - total: 1598588.273 μs - avg: 159858.827 μs - min: 147759.554 μs - max: 193999.679 μs - std dev: 17143.300 μs + total: 1775922.415 μs + avg: 177592.242 μs + min: 161735.069 μs + max: 206519.406 μs + std dev: 15129.161 μs === parse/xmir === warmup: 3 iterations batches: 10 x 1 - total: 7813131.215 μs - avg: 781313.122 μs - min: 724999.135 μs - max: 842487.724 μs - std dev: 32948.399 μs + total: 7571386.164 μs + avg: 757138.616 μs + min: 691286.480 μs + max: 813614.260 μs + std dev: 32034.618 μs === rewrite/normalize === warmup: 3 iterations batches: 10 x 1 - total: 1071335.155 μs - avg: 107133.516 μs - min: 82715.009 μs - max: 127072.342 μs - std dev: 15148.984 μs + total: 579674.000 μs + avg: 57967.400 μs + min: 56388.139 μs + max: 61829.190 μs + std dev: 1703.063 μs === print/sweet/multiline === warmup: 3 iterations batches: 10 x 1 - total: 4764374.575 μs - avg: 476437.457 μs - min: 443528.234 μs - max: 508780.337 μs - std dev: 21790.459 μs + total: 3876263.188 μs + avg: 387626.319 μs + min: 373639.628 μs + max: 405513.521 μs + std dev: 10018.938 μs === print/sweet/flat === warmup: 3 iterations batches: 10 x 1 - total: 4829704.670 μs - avg: 482970.467 μs - min: 444530.419 μs - max: 514344.452 μs - std dev: 23249.943 μs + total: 3789406.984 μs + avg: 378940.698 μs + min: 367216.617 μs + max: 395082.263 μs + std dev: 8761.575 μs === print/salty/multiline === warmup: 3 iterations batches: 10 x 1 - total: 14789056.654 μs - avg: 1478905.665 μs - min: 1426640.434 μs - max: 1589233.894 μs - std dev: 46147.565 μs + total: 13982361.998 μs + avg: 1398236.200 μs + min: 1366361.442 μs + max: 1433666.397 μs + std dev: 17717.682 μs ``` The results were calculated in [this GHA job][benchmark-gha] -on 2026-09-08 at 20:28, +on 2026-09-09 at 15:41, on Linux with 4 CPUs. @@ -939,4 +939,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/34274639466 +[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/34371511775 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.121 +version: 0.0.122 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 @@ -217,6 +217,7 @@ asBytesArg (ArAlpha (Alpha 0) inner) = Just inner asBytesArg _ = Nothing dataArg :: Argument -> Maybe Expression + dataArg (ArTau AtPhi formation) = Just formation dataArg (ArTau (AtLabel "data") formation) = Just formation dataArg (ArAlpha (Alpha 0) formation) = Just formation dataArg _ = Nothing @@ -255,10 +256,13 @@ DataObject label bts = ExApplication (BaseObject label) (ArTau (AtLabel "as-bytes") (dataBytes bts)) --- The bytes object Φ.bytes(data ↦ ⟦ Δ ⤍ …, ρ ↦ ∅ ⟧) — what a 'bytes' atom --- yields and what a 'DataObject' carries under its 'as-bytes' argument +-- The bytes object Φ.bytes(φ ↦ ⟦ Δ ⤍ …, ρ ↦ ∅ ⟧) — what a 'bytes' atom +-- yields and what a 'DataObject' carries under its 'as-bytes' 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) dataBytes :: Bytes -> Expression dataBytes bts = ExApplication (BaseObject "bytes") - (ArTau (AtLabel "data") (ExFormation [BiDelta bts, BiVoid AtRho])) + (ArTau AtPhi (ExFormation [BiDelta bts, BiVoid AtRho])) diff --git a/src/CLI.hs b/src/CLI.hs --- a/src/CLI.hs +++ b/src/CLI.hs @@ -10,16 +10,32 @@ import CLI.Parsers import CLI.Runners import CLI.Types -import Control.Exception.Base (Exception (displayException), SomeException, fromException, handle, throwIO) +import Control.Exception.Base (SomeException, fromException, handle, throwIO) import Data.Version (showVersion) import Logger import Options.Applicative import Paths_phino (version) -import System.Exit (ExitCode (..), exitFailure) +import System.Exit (ExitCode (..), exitFailure, exitWith) +import System.IO (hPutStrLn, stderr) runCLI :: [String] -> IO () runCLI args = handle handler $ do - CliArgs{_pin, _command} <- handleParseResult (execParserPure defaultPrefs parserInfo args) + let parsed = execParserPure defaultPrefs parserInfo args + CliArgs{_pin, _command} <- case parsed of + Success opts -> pure opts + Failure failure -> do + let (msg, code) = renderFailure failure "phino" + case code of + ExitSuccess -> do + putStrLn msg -- --version/--help output as-is + exitWith code + _ -> do + -- Keep the full optparse message (including the Usage/synopsis + -- block that follows a parse error), but without the GHC + -- HasCallStack backtrace; prefix just the first line with [ERROR]:. + hPutStrLn stderr (prefixFirstLine "[ERROR]: " msg) + exitWith code + CompletionInvoked _ -> handleParseResult parsed checkPin _pin setLogger _command case _command of @@ -30,11 +46,15 @@ CmdMerge opts -> runMerge opts CmdMatch opts -> runMatch opts where + prefixFirstLine :: String -> String -> String + prefixFirstLine _ "" = "Failure" + prefixFirstLine prefix msg = prefix ++ msg handler :: SomeException -> IO () handler e = case fromException e of Just ExitSuccess -> pure () -- prevent printing error on --version etc. + Just (ExitFailure _) -> exitFailure -- already logged by the Failure branch above _ -> do - logError (displayException e) + logError (show e) exitFailure setLogger :: Command -> IO () setLogger cmd = diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -316,8 +316,9 @@ go :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State) go context term state' caller = do ctx' <- deeper caller - answer <- fired (contextualize term context) univ state' ctx' - maybe (parts context term state' ctx') pure answer + (walked, walkedState) <- parts context term state' caller + answer <- fired (contextualize walked context) univ walkedState ctx' + maybe (pure (walked, walkedState)) pure answer -- The parts of a term nothing fired on, walked one by one and put back -- where they were, so the term keeps the shape it was written in. parts :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State) diff --git a/src/Sugar.hs b/src/Sugar.hs --- a/src/Sugar.hs +++ b/src/Sugar.hs @@ -216,7 +216,7 @@ (TAB (indent + 2)) ( AA_TAUS ( BI_PAIR - (PA_TAU (AT_LABEL "data") ARROW data') + (PA_TAU (AT_PHI PHI) ARROW data') (BDS_EMPTY (TAB (indent + 2))) (TAB (indent + 2)) ) diff --git a/src/XMIR.hs b/src/XMIR.hs --- a/src/XMIR.hs +++ b/src/XMIR.hs @@ -114,7 +114,7 @@ let bts = object [("as", "as-bytes"), ("base", "Φ.bytes")] - [object [("as", "data")] [NodeContent (T.pack (printBytes bytes))]] + [object [("as", "φ")] [NodeContent (T.pack (printBytes bytes))]] in pure ( "Φ.number" , if _omitComments || btsSize bytes /= 8 @@ -128,7 +128,7 @@ let bts = object [("as", "as-bytes"), ("base", "Φ.bytes")] - [object [("as", "data")] [NodeContent (T.pack (printBytes bytes))]] + [object [("as", "φ")] [NodeContent (T.pack (printBytes bytes))]] in pure ( "Φ.string" , if _omitComments || not (btsIsUtf8 bytes) diff --git a/test/ASTSpec.hs b/test/ASTSpec.hs --- a/test/ASTSpec.hs +++ b/test/ASTSpec.hs @@ -296,7 +296,7 @@ dataBytes (BtOne "48") `shouldBe` ExApplication (ExDispatch ExRoot (AtLabel "bytes")) - (ArTau (AtLabel "data") (ExFormation [BiDelta (BtOne "48"), BiVoid AtRho])) + (ArTau AtPhi (ExFormation [BiDelta (BtOne "48"), BiVoid AtRho])) describe "DataObject/DataString/DataNumber pattern" $ do it "constructs the named, unwrapped as-bytes form" $ @@ -371,7 +371,7 @@ (AtLabel "as-bytes") ( ExApplication (ExDispatch ExRoot (AtLabel "other")) - (ArTau (AtLabel "data") (ExFormation [BiDelta (BtOne "48"), BiVoid AtRho])) + (ArTau AtPhi (ExFormation [BiDelta (BtOne "48"), BiVoid AtRho])) ) ) ) diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -250,6 +250,18 @@ ["rewrite", "--in-place", "--output=latex", path] ["--in-place can only be used together with --output=phi"] + it "does not leak a HasCallStack backtrace into errors" $ do + (out, _) <- withStdout (try (runCLI ["rewrite", "--in-place"]) :: IO (Either ExitCode ())) + out `shouldNotContain` "HasCallStack backtrace" + out `shouldNotContain` "ExitFailure 1" + out `shouldContain` "[ERROR]:" + + it "prints optparse errors once, without a backtrace" $ do + (out, _) <- withStdout (try (runCLI ["rewrite", "--badopt"]) :: IO (Either ExitCode ())) + out `shouldNotContain` "HasCallStack backtrace" + out `shouldNotContain` "ExitFailure 1" + out `shouldContain` "[ERROR]:" + forM_ [ ("when --update is used without --target", "[[ ]]", ["rewrite", "--update"], ["--update requires --target"]) , @@ -413,7 +425,7 @@ it "saves dataize steps to dir with --steps-dir" $ withAtoms $ \atoms -> withTempDirectory "phino-steps-dataize" $ \dir -> - withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $ do + withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $ do testCLISucceeded ["dataize", atoms, "--steps-dir=" ++ dir, "--sweet"] ["40-32"] @@ -1134,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(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $ + withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, 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(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $ + withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, 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}"] @@ -1159,7 +1171,7 @@ withAtoms $ \atoms -> withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do hClose stream - withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ + withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, 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" @@ -1168,7 +1180,7 @@ withAtoms $ \atoms -> withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do hClose stream - withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $ + withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, 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"] @@ -1177,16 +1189,16 @@ withAtoms $ \atoms -> withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do hClose stream - withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ + withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, 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( data ↦ ⟦ Δ ⤍ 40-26-00-00-00-00-00-00 ⟧ ) )\n" + records `shouldEndWith` "\tΦ.number( as-bytes ↦ Φ.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(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]], nope -> [[ L> L_number_nope ]] ]], @ -> 5.plus(6).nope ]]" $ + withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, 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"] @@ -1217,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(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, times(x) -> [[ L> L_number_times ]], nope -> [[ L> L_number_nope ]] ]], @ -> 2.times(3).nope ]]" + let stuck = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, 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 $ @@ -1235,7 +1247,7 @@ withStdin stuck $ testCLISucceeded ["dataize", atoms, "--partial", "--sweet"] - ["as-bytes ↦ Φ.bytes( data ↦ ⟦ Δ ⤍ 40-18-00-00-00-00-00-00 ⟧ )"] + ["as-bytes ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-18-00-00-00-00-00-00 ⟧ )"] it "records every stuck site in --evaluations with no result" $ withAtoms $ \atoms -> @@ -1251,7 +1263,7 @@ it "still prints bytes when nothing gets stuck" $ withAtoms $ \atoms -> - withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ + withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, 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" $ @@ -1268,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(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" + let sum' = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" it "fires the λ function the registry carries" $ withAtoms $ \atoms -> withStdin sum' $ @@ -1298,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(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> [[ D> 01- ]] ]]" + let universe = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> [[ D> 01- ]] ]]" it "dataizes an expression the input does not contain" $ withAtoms $ \atoms -> withStdin universe $ @@ -1389,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(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" + let chained = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" it "prints help" $ testCLISucceeded ["morph", "--help"] ["Morph the 𝜑-expression"] @@ -1508,7 +1520,7 @@ -- atom touched keeps its name and the answer stays a program (#1124) describe "--deep" $ do let program = - "[[ bytes(data) -> [[ @ -> $.data ]], \ + "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, \ \number(as-bytes) -> [[ @ -> $.as-bytes, times(x) -> [[ L> L_number_times ]] ]], \ \bar(x) -> [[ L> L_bar ]], \ \demo -> [[ foo -> [[ n -> 3, @ -> Q.bar( $.n.times( 5 ).times( 7 ) ) ]] ]] ]]" diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -102,8 +102,7 @@ unlines [ "[[" , " bytes -> [[" - , " data -> ?," - , " @ -> $.data," + , " φ -> ?," , " not -> [[ L> L_bytes_not ]]," , " eq -> [[ b -> ?, L> L_bytes_eq ]]" , " ]]," @@ -126,7 +125,7 @@ -- Wrap a hex literal into the bytes object that EO source spells as a bare '20-1F' raw :: String -> String -raw bts = "Q.bytes( data -> [[ D> " ++ bts ++ " ]] )" +raw bts = "Φ.bytes( φ ↦ ⟦ Δ ⤍ " ++ bts ++ " ⟧ )" -- Dataize an expression against the fixture universe, with the fixture λ -- functions registered. Every such case runs an external script, so it is @@ -223,19 +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 -> Q.bytes( data -> [[ D> 40-26-00-00-00-00-00-00 ]] ) ) ]]" + , "[[ x -> Q.number( as-bytes -> Φ.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 ]] ) ) ]]" + ) + , ( "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 -> Q.bytes( data -> [[ D> 40-32-00-00-00-00-00-00 ]] ) ) ]]" + , "[[ x -> Q.number( as-bytes -> Φ.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 -> Q.bytes( data -> [[ D> 40-26-00-00-00-00-00-00 ]] ) ) ]]" + , "[[ n -> 5, x -> Q.number( as-bytes -> Φ.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 @@ -254,7 +259,7 @@ ( "leaves a λ-formation still waiting for its arguments alone" , "Q.bytes" , primitives "[[ ]]" - , "[[ data -> ?, @ -> $.data, not -> [[ L> L_bytes_not ]], eq -> [[ b -> ?, L> L_bytes_eq ]] ]]" + , "[[ φ -> ?, not -> [[ L> L_bytes_not ]], eq -> [[ b -> ?, L> L_bytes_eq ]] ]]" ) , -- Nothing demands the argument of an atom that cannot fire, so 𝔻 never -- reaches it; the walk does, and the atom around it stays in place @@ -262,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 -> Q.bytes( data -> [[ D> 40-2A-00-00-00-00-00-00 ]] ) ) ) ]]" + , "[[ x -> [[ y -> ?, L> L_bar ]]( y -> Q.number( as-bytes -> Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-2A-00-00-00-00-00-00 ⟧ ) ) ) ]]" ) ] @@ -706,7 +711,7 @@ labels <- labelsOf "Q" - "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" + "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" labels `shouldBe` [ "contextualize" , "maa" @@ -723,8 +728,6 @@ , "stay" , "mf" , "contextualize" - , "dot" - , "copy" , "delta" ] it "dataizes a located reference through the expected rules" $ do @@ -763,7 +766,7 @@ , unlines [ "[[" , " number(as-bytes) -> [[ @ -> as-bytes ]]," - , " bytes(data) -> [[ @ -> data ]]," + , " bytes ↦ ⟦ φ ↦ ∅ ⟧," , " x -> 5" , "]]" ] @@ -821,8 +824,7 @@ ( unlines [ "[[" , " bytes -> [[" - , " data -> ?," - , " @ -> $.data" + , " φ -> ?" , " ]]," , " number -> [[" , " as-bytes -> ?," diff --git a/test/PrinterSpec.hs b/test/PrinterSpec.hs --- a/test/PrinterSpec.hs +++ b/test/PrinterSpec.hs @@ -19,7 +19,7 @@ import Parser (parseExpression) import Printer import Sugar (SugarType (..)) -import Test.Hspec (Spec, describe, it, shouldBe, shouldContain) +import Test.Hspec (Spec, describe, it, shouldBe, shouldContain, shouldNotContain) import Yaml (ExtraArgument (..)) spec :: Spec @@ -130,6 +130,21 @@ printed `shouldContain` "bytes" parseExpression printed `shouldBe` Right expr ) + + describe "printExpression binds a datum payload to φ in salty notation (#1142)" $ + it "names the bytes payload φ (the void the real bytes declares), not data" $ 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 `shouldContain` "φ ↦" + number `shouldNotContain` "data ↦" + str `shouldContain` "φ ↦" + str `shouldNotContain` "data ↦" describe "printExpression keeps a compressed meet atomic under a narrow margin" $ -- A \phinoMeet is a single \overbracket visual unit, so its body must stay 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 data ↦ ⟦\n Δ ⤍ 40-45-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.number(\n as-bytes ↦ Φ.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 data ↦ ⟦\n Δ ⤍ 40-45-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )(\n ρ ↦ ξ.y\n )" + , "Φ.number(\n as-bytes ↦ Φ.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 data ↦ ⟦\n Δ ⤍ 7F-F8-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.number(\n as-bytes ↦ Φ.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 data ↦ ⟦\n Δ ⤍ 7F-F0-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.number(\n as-bytes ↦ Φ.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 data ↦ ⟦\n Δ ⤍ FF-F0-00-00-00-00-00-00,\n ρ ↦ ∅\n ⟧\n )\n )(\n ρ ↦ ξ.y\n )" + , "Φ.number(\n as-bytes ↦ Φ.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 data ↦ ⟦\n Δ ⤍ 68-69,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.string(\n as-bytes ↦ Φ.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 data ↦ ⟦\n Δ ⤍ 65-0A-65,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.string(\n as-bytes ↦ Φ.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 data ↦ ⟦\n Δ ⤍ 22-5C,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.string(\n as-bytes ↦ Φ.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 data ↦ ⟦\n Δ ⤍ 01-,\n ρ ↦ ∅\n ⟧\n )\n )" + , "Φ.string(\n as-bytes ↦ Φ.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( data ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00, ρ ↦ ∅ ⟧ ) )" + printExpression' number (config SALTY) `shouldBe` "Φ.number( as-bytes ↦ Φ.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( data ↦ ⟦ Δ ⤍ 68-69, ρ ↦ ∅ ⟧ ) )" + printExpression' string (config SALTY) `shouldBe` "Φ.string( as-bytes ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 68-69, ρ ↦ ∅ ⟧ ) )" it "an application with multiple positional arguments sugars/salts between e(e0, e1) and e(α0 ↦ e0)(α1 ↦ e1)" $ do