phino 0.0.106 → 0.0.107

raw patch · 14 files changed

+405/−87 lines, 14 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +33/−33
• phino.cabal +1/−1
• src/CLI/Helpers.hs +26/−6
• src/CLI/Parsers.hs +14/−0
• src/CLI/Runners.hs +6/−0
• src/CLI/Types.hs +6/−0
• src/LaTeX.hs +27/−10
• src/Parser.hs +39/−34
• src/Printer.hs +13/−1
• src/Rewriter.hs +23/−1
• src/Sugar.hs +70/−1
• test/CLISpec.hs +78/−0
• test/ParserSpec.hs +29/−0
• test/PrinterSpec.hs +40/−0

@@ -34,7 +34,7 @@  ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.105+cabal install --overwrite-policy=always phino-0.0.106 phino --version ``` @@ -447,55 +447,55 @@ === parse/phi ===   warmup:     3 iterations   batches:    10 x 1-  total:      1289912.679 μs-  avg:        128991.268 μs-  min:        117209.849 μs-  max:        157967.879 μs-  std dev:    16178.452 μs+  total:      1279870.467 μs+  avg:        127987.047 μs+  min:        117457.988 μs+  max:        156105.148 μs+  std dev:    15737.223 μs === parse/xmir ===   warmup:     3 iterations   batches:    10 x 1-  total:      7732390.781 μs-  avg:        773239.078 μs-  min:        704582.049 μs-  max:        844495.931 μs-  std dev:    54136.286 μs+  total:      7617419.851 μs+  avg:        761741.985 μs+  min:        686228.460 μs+  max:        914941.984 μs+  std dev:    59800.299 μs === rewrite/normalize ===   warmup:     3 iterations   batches:    10 x 1-  total:      665998.989 μs-  avg:        66599.899 μs-  min:        63509.721 μs-  max:        72014.960 μs-  std dev:    2455.894 μs+  total:      603364.936 μs+  avg:        60336.494 μs+  min:        58688.247 μs+  max:        62431.021 μs+  std dev:    1196.183 μs === print/sweet/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      4722211.658 μs-  avg:        472221.166 μs-  min:        463189.991 μs-  max:        485006.422 μs-  std dev:    6780.561 μs+  total:      4208011.890 μs+  avg:        420801.189 μs+  min:        400713.926 μs+  max:        442532.655 μs+  std dev:    16080.251 μs === print/sweet/flat ===   warmup:     3 iterations   batches:    10 x 1-  total:      4645473.928 μs-  avg:        464547.393 μs-  min:        431061.415 μs-  max:        488222.918 μs-  std dev:    21693.313 μs+  total:      4195034.891 μs+  avg:        419503.489 μs+  min:        403618.144 μs+  max:        432523.908 μs+  std dev:    9981.104 μs === print/salty/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      14501593.398 μs-  avg:        1450159.340 μs-  min:        1407041.861 μs-  max:        1506159.801 μs-  std dev:    33325.764 μs+  total:      13849441.895 μs+  avg:        1384944.189 μs+  min:        1372281.323 μs+  max:        1410740.491 μs+  std dev:    10841.096 μs ```  The results were calculated in [this GHA job][benchmark-gha]-on 2026-07-07 at 18:32,+on 2026-07-24 at 23:39, on Linux with 4 CPUs.  <!-- benchmark_end -->@@ -544,4 +544,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/28889268073+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/30134184768

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.106+version: 0.0.107 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>

@@ -25,7 +25,7 @@ import Parser (parseExpressionThrows) import qualified Printer as P import qualified Random as R-import Rewriter (Rewritten, Rewrittens')+import Rewriter (Rewritten, Rewrittens', stepHeaders) import System.IO (getContents') import Text.Printf (printf) import XMIR (expressionToXMIR, parseXMIRThrows, printXMIR, xmirToPhi)@@ -69,28 +69,48 @@ printRewrittens :: PrintContext -> Rewrittens' -> IO String printRewrittens ctx@PrintCtx{..} rewrittens@(chain, _)   | _outputFormat == LATEX && _sequence = rewrittensToLatex rewrittens (printCtxToLatexCtx ctx)-  | _focus == ExRoot = mapM (printInFormat ctx . fst) (canonized chain) <&> intercalate "\n"-  | otherwise = mapM (\(expr, _) -> locatedExpression _focus expr >>= printExpression ctx) (canonized chain) <&> intercalate "\n"+  | otherwise = withHeaders <$> mapM render (canonized chain)   where+    render :: Rewritten -> IO String+    render (expr, _)+      | _focus == ExRoot = printInFormat ctx expr+      | otherwise = locatedExpression _focus expr >>= printExpression ctx     canonized :: [Rewritten] -> [Rewritten]     canonized = if _canonize then canonize else id+    -- Prefix every step with an empty line and its header (see 'stepHeaders')+    -- when '--headers' is on. Headers, like the other intermediate-output+    -- flags, are meaningful only together with '--sequence'. Node counts come+    -- from the original 'chain', not the canonized one, since canonization+    -- only renames functions and never changes the AST size.+    withHeaders :: [String] -> String+    withHeaders rendered+      | _headers && _sequence = intercalate "\n" (zipWith prefixed (stepHeaders chain) rendered)+      | otherwise = intercalate "\n" rendered+      where+        prefixed :: String -> String -> String+        prefixed = printf "\n%s\n%s"  printExpression :: PrintContext -> Expression -> IO String printExpression ctx@PrintCtx{..} ex = case _outputFormat of-  PHI -> pure (P.printExpression' ex (_sugar, UNICODE, _line, _margin))+  PHI -> pure (printPhi ctx ex)   XMIR -> throwIO CouldNotPrintExpressionInXMIR   LATEX -> pure (expressionToLaTeX ex (printCtxToLatexCtx ctx))  -- Convert an expression to its corresponding String format printInFormat :: PrintContext -> Expression -> IO String printInFormat ctx@PrintCtx{..} expr = case _outputFormat of-  PHI -> pure (P.printExpression' expr (_sugar, UNICODE, _line, _margin))+  PHI -> pure (printPhi ctx expr)   XMIR -> expressionToXMIR expr _xmirCtx <&> printXMIR   LATEX -> pure (expressionToLaTeX expr (printCtxToLatexCtx ctx)) +-- Render an expression as PHI, dropping every ρ binding when '--hide-rho' is set.+printPhi :: PrintContext -> Expression -> String+printPhi PrintCtx{..} expr =+  (if _hideRho then P.printExpressionHidingRho' else P.printExpression') expr (_sugar, UNICODE, _line, _margin)+ printCtxToLatexCtx :: PrintContext -> LatexContext printCtxToLatexCtx PrintCtx{..} =-  LatexContext _sugar _line _margin _nonumber _compress _canonize _meetPopularity _meetLength _focus _expression _label _meetPrefix+  LatexContext _sugar _line _margin _nonumber _compress _canonize _meetPopularity _meetLength _focus _expression _label _meetPrefix _headers  -- Get rules for rewriting depending on provided flags getRules :: Bool -> Bool -> [FilePath] -> IO [Y.Rule]

@@ -121,6 +121,13 @@ optSequence :: Parser Bool optSequence = switch (long "sequence" <> help "Result output contains all intermediate 𝜑-expressions concatenated with EOL") +optHeaders :: Parser Bool+optHeaders =+  switch+    ( long "headers"+        <> help "Prefix every intermediate step (see --sequence) with a header line: step number, the rule that produced it, and AST node count before and after that rule"+    )+ optCanonize :: Parser Bool optCanonize = switch (long "canonize" <> help "Rename all functions attached to λ binding with Fn1, Fn2, etc.") @@ -206,6 +213,9 @@ optSugar :: Parser SugarType optSugar = flag SALTY SWEET (long "sweet" <> help (printf "Print result and intermediate (see %s option(s)) 𝜑-expressions using syntax sugar" _intermediateOptions)) +optHideRho :: Parser Bool+optHideRho = switch (long "hide-rho" <> help "Remove every ρ binding from result and intermediate 𝜑-expressions for cleaner output")+ optSugar' :: Parser SugarType optSugar' = flag SALTY SWEET (long "sweet" <> help "Print result 𝜑-expression using syntax sugar") @@ -262,11 +272,13 @@             <*> optInputFormat             <*> optOutputFormat             <*> optSugar+            <*> optHideRho             <*> optLineFormat             <*> optOmitListing             <*> optOmitComments             <*> optNonumber             <*> optSequence+            <*> optHeaders             <*> optCanonize             <*> optDepthSensitive             <*> optShuffle@@ -298,6 +310,7 @@             <*> optInputFormat             <*> optOutputFormat             <*> optSugar+            <*> optHideRho             <*> optLineFormat             <*> optMust             <*> optNormalize@@ -310,6 +323,7 @@             <*> switch (long "in-place" <> help "Edit file in-place instead of printing to output")             <*> switch (long "update" <> help "Skip rewriting if --target file is newer than the input file")             <*> optSequence+            <*> optHeaders             <*> optCanonize             <*> optCompress             <*> optMaxDepth

@@ -119,6 +119,7 @@     toPrintCtx xmirCtx focus =       PrintCtx         _sugarType+        _hideRho         _flat         _margin         xmirCtx@@ -126,6 +127,7 @@         _compress         _canonize         _sequence+        _headers         (justMeetPopularity _meetPopularity)         (justMeetLength _meetLength)         focus@@ -167,6 +169,7 @@     toPrintCtx focus =       PrintCtx         _sugarType+        _hideRho         _flat         _margin         defaultXmirContext@@ -174,6 +177,7 @@         _compress         _canonize         _sequence+        _headers         (justMeetPopularity _meetPopularity)         (justMeetLength _meetLength)         focus@@ -219,9 +223,11 @@     toPrintCtx xmirCtx =       PrintCtx         _sugarType+        False         _flat         _margin         xmirCtx+        False         False         False         False

@@ -17,6 +17,7 @@  data PrintContext = PrintCtx   { _sugar :: SugarType+  , _hideRho :: Bool   , _line :: LineFormat   , _margin :: Int   , _xmirCtx :: XmirContext@@ -24,6 +25,7 @@   , _compress :: Bool   , _canonize :: Bool   , _sequence :: Bool+  , _headers :: Bool   , _meetPopularity :: Int   , _meetLength :: Int   , _focus :: Expression@@ -77,11 +79,13 @@   , _inputFormat :: IOFormat   , _outputFormat :: IOFormat   , _sugarType :: SugarType+  , _hideRho :: Bool   , _flat :: LineFormat   , _omitListing :: Bool   , _omitComments :: Bool   , _nonumber :: Bool   , _sequence :: Bool+  , _headers :: Bool   , _canonize :: Bool   , _depthSensitive :: Bool   , _shuffle :: Bool@@ -122,6 +126,7 @@   , _inputFormat :: IOFormat   , _outputFormat :: IOFormat   , _sugarType :: SugarType+  , _hideRho :: Bool   , _flat :: LineFormat   , _must :: Must   , _normalize :: Bool@@ -134,6 +139,7 @@   , _inPlace :: Bool   , _update :: Bool   , _sequence :: Bool+  , _headers :: Bool   , _canonize :: Bool   , _compress :: Bool   , _maxDepth :: Int

@@ -38,7 +38,7 @@ import Misc import Render (Render (render)) import Replacer (replaceExpression)-import Rewriter (Rewritten, Rewrittens')+import Rewriter (Rewritten, Rewrittens', stepHeaders) import Sugar (SugarType (SWEET), ToSalty, withSugarType) import Text.Printf (printf) import Text.Read (readMaybe)@@ -57,10 +57,11 @@   , _expression :: Maybe String   , _label :: Maybe String   , _meetPrefix :: Maybe String+  , _headers :: Bool   }  defaultLatexContext :: LatexContext-defaultLatexContext = LatexContext SWEET SINGLELINE defaultMargin False False False defaultMeetPopularity defaultMeetLength ExRoot Nothing Nothing Nothing+defaultLatexContext = LatexContext SWEET SINGLELINE defaultMargin False False False defaultMeetPopularity defaultMeetLength ExRoot Nothing Nothing Nothing False  defaultMeetPopularity :: Int defaultMeetPopularity = 50@@ -158,16 +159,21 @@ -- than 0 (via 'baseTab'); this keeps a wrapped multi-line step's members nested -- one level below its '\leadsto [[' line and its closing bracket aligned with -- that line. The first step has no '\leadsto' prefix and stays at base tab 0.-body :: [(a, Maybe String)] -> (Int -> a -> String) -> String-body printed toLatex =+-- Each step is prefixed with the matching entry from 'comments', which is+-- either empty or a '% ...'-commented header line ending in a newline (see+-- 'stepComments'), so headers stay on their own line above the equation.+body :: [String] -> [(a, Maybe String)] -> (Int -> a -> String) -> String+body comments printed toLatex =   intercalate-    "\n  \\leadsto "-    ( zipWith-        ( \idx (item, maybeName) ->+    "\n"+    ( zipWith3+        ( \idx comment (item, maybeName) ->             let item' = toLatex (baseTab idx) item-             in maybe item' (printf "%s \\leadsto_{\\nameref{r:%s}}" item') maybeName+                leadsto = if idx == 0 then item' else "  \\leadsto " ++ item'+             in comment ++ maybe leadsto (printf "%s \\leadsto_{\\nameref{r:%s}}" leadsto) maybeName         )         [0 ..]+        comments         printed     )   where@@ -175,6 +181,17 @@     baseTab 0 = 0     baseTab _ = 1 +-- LaTeX comment header lines for each step (see 'stepHeaders' in "Rewriter"),+-- or empty strings when '--headers' is off. A '%' starts a LaTeX comment, so+-- the header documents the '--sequence' chain without affecting the rendered+-- equation. Each comment ends in a newline so the following step starts on a+-- fresh line.+stepComments :: [Rewritten] -> LatexContext -> [String]+stepComments rewrittens LatexContext{_headers = enabled} =+  if enabled+    then map (printf "%% %s\n") (stepHeaders rewrittens)+    else map (const "") rewrittens+ ending :: Bool -> LatexContext -> String ending True ctx = printf " \\leadsto\n  \\leadsto \\dots\n\\end{%s}" (phiquation ctx) ending False ctx = printf "{.}\n\\end{%s}" (phiquation ctx)@@ -212,7 +229,7 @@   pure     ( concat         [ preamble ctx-        , body (canonizedRewrittens (compressedRewrittens rewrittens ctx) ctx) (\tabs expr -> renderToLatex (expressionToCSTFrom tabs expr) ctx)+        , body (stepComments rewrittens ctx) (canonizedRewrittens (compressedRewrittens rewrittens ctx) ctx) (\tabs expr -> renderToLatex (expressionToCSTFrom tabs expr) ctx)         , ending exceeded ctx         ]     )@@ -222,7 +239,7 @@   pure     ( concat         [ preamble ctx-        , body (zip (canonizedExpressions (compressedExpressions focused ctx) ctx) rules) (\tabs expr -> renderToLatex (expressionToCSTFrom tabs expr) ctx)+        , body (stepComments rewrittens ctx) (zip (canonizedExpressions (compressedExpressions focused ctx) ctx) rules) (\tabs expr -> renderToLatex (expressionToCSTFrom tabs expr) ctx)         , ending exceeded ctx         ]     )

@@ -82,15 +82,19 @@   return (T.pack (first : rest))  function :: Parser String-function = lexeme $ do-  first <- oneOf ['A' .. 'Z']-  rest <--    many-      ( satisfy-          (\ch -> isDigit ch || isAsciiLower ch || ch == '_' || ch == 'φ')-          <?> "allowed character in function name"-      )-  return (first : rest)+function =+  lexeme+    ( do+        first <- oneOf ['A' .. 'Z']+        rest <-+          many+            ( satisfy+                (\ch -> isDigit ch || isAsciiLower ch || ch == '_' || ch == 'φ')+                <?> "allowed character in function name"+            )+        return (first : rest)+    )+    <?> "function name"  delta :: Parser String delta =@@ -244,7 +248,7 @@ tauValue :: Parser Expression tauValue =   choice-    [ try $ do+    [ do         _ <- arrow         expression     , do@@ -265,41 +269,42 @@     rb :: Parser String     rb = symbol ")" -tauBinding :: Parser Attribute -> Parser Binding-tauBinding attr = BiTau <$> attr <*> tauValue- metaBinding :: Parser Binding metaBinding = BiMeta <$> meta' 'B' "𝐵"  -- binding--- 1. tau--- 2. void--- 3. delta--- 4. meta delta--- 5. meta--- 6. lambda--- 7. meta lambda+-- 1. delta+-- 2. meta delta+-- 3. meta+-- 4. lambda+-- 5. meta lambda+-- 6. void+-- 7. tau+--+-- Every alternative commits as soon as the token that tells it apart from its+-- siblings is consumed, so a failure deeper in the binding keeps its own+-- position instead of being rewound to the beginning of the binding. binding :: Parser Binding binding =   choice-    [ try (tauBinding attribute)-    , try $ do-        attr <- attribute-        _ <- arrow-        _ <- choice [symbol "?", symbol "∅"]-        return (BiVoid attr)-    , try $ do-        _ <- delta+    [ do+        _ <- try delta         BiDelta <$> bytes     , try metaBinding-    , try $ do-        _ <- lambda-        BiLambda . Function . T.pack <$> function     , do-        _ <- lambda-        BiLambda . FnMeta <$> meta' 'F' "𝑓"+        _ <- try lambda+        BiLambda <$> choice [Function . T.pack <$> function, FnMeta <$> meta' 'F' "𝑓"]+    , do+        attr <- attribute+        choice+          [ try blank >> return (BiVoid attr)+          , BiTau attr <$> tauValue+          ]     ]     <?> "binding"+  where+    blank :: Parser String+    blank = arrow >> choice [symbol "?", symbol "∅"]  -- inlined void attribute -- 1. label@@ -352,7 +357,7 @@ argument :: Parser Argument argument =   choice-    [ try (ArAlpha <$> alpha <*> tauValue)+    [ ArAlpha <$> try alpha <*> tauValue     , ArTau <$> attribute <*> tauValue     ]     <?> "argument"

@@ -7,6 +7,7 @@ module Printer   ( printExpression   , printExpression'+  , printExpressionHidingRho'   , printAttribute   , printAlpha   , printBinding@@ -42,7 +43,18 @@ logPrintConfig = (SWEET, UNICODE, SINGLELINE, defaultMargin)  printExpression' :: Expression -> PrintConfig -> String-printExpression' ex (sugar, encoding, line, margin) = T.unpack $ render (withLineFormat line $ withMargin margin $ withEncoding encoding $ withSugarType sugar $ expressionToCST ex)+printExpression' = printExpressionWith id++-- Like 'printExpression'', but drops every ρ binding from the rendered+-- expression (the '--hide-rho' switch). See 'withoutRho'.+printExpressionHidingRho' :: Expression -> PrintConfig -> String+printExpressionHidingRho' = printExpressionWith withoutRho++-- Shared rendering pipeline with a hook applied to the sugared CST, right+-- before encoding and margin wrapping.+printExpressionWith :: (EXPRESSION -> EXPRESSION) -> Expression -> PrintConfig -> String+printExpressionWith hide ex (sugar, encoding, line, margin) =+  T.unpack $ render (withLineFormat line $ withMargin margin $ withEncoding encoding $ hide $ withSugarType sugar $ expressionToCST ex)  printExpression :: Expression -> String printExpression ex = printExpression' ex defaultPrintConfig

@@ -9,7 +9,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Rewriter (rewrite, RewriteContext (..), Rewritten, Rewrittens, Rewrittens') where+module Rewriter (rewrite, RewriteContext (..), Rewritten, Rewrittens, Rewrittens', stepHeaders) where  import AST import Builder@@ -17,6 +17,7 @@ import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE import qualified Data.Map.Strict as Map+import Data.Maybe (fromMaybe) import Deps import Locator (locatedExpression, withLocatedExpression) import Logger (logDebug)@@ -53,6 +54,27 @@ type Rewrittens = (NonEmpty Rewritten, Bool)  type Rewrittens' = ([Rewritten], Bool)++-- Build a header line for every step of a rewriting chain. The chain is+-- '[(e0, Just r0), ..., (en, Nothing)]', where 'ri' is the rule applied to 'ei'+-- to produce 'e(i+1)' (see 'leadsTo'). A step's header names the rule that+-- produced its expression, together with the AST node counts before and after+-- that rule, e.g. "=== Step #4, Rule 'STOP', 32t -> 43t". The very first step is+-- the input, which no rule produced, so it carries only its number:+-- "=== Step #1". The 'N nodes -> M nodes' pair matches the debug log emitted+-- while rewriting.+stepHeaders :: [Rewritten] -> [String]+stepHeaders chain = zipWith3 header [1 ..] chain (Nothing : map Just chain)+  where+    header :: Int -> Rewritten -> Maybe Rewritten -> String+    header step _ Nothing = printf "=== Step #%d" step+    header step (current, _) (Just (before, rule)) =+      printf+        "=== Step #%d, Rule '%s', %dt -> %dt"+        step+        (fromMaybe "?" rule)+        (countNodes before)+        (countNodes current)  type ToReplace = (Expression, Expression, Expression, [Subst]) 

@@ -7,7 +7,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Sugar (toSalty, withSugarType, SugarType (..), ToSalty) where+module Sugar (toSalty, withSugarType, withoutRho, SugarType (..), ToSalty) where  import AST import Bytes (numToBts, strToBts)@@ -39,6 +39,75 @@  data SugarType = SWEET | SALTY   deriving (Eq, Show)++-- Drop every ρ binding (ρ ↦ ∅, ρ ↦ e and ρ(…) ↦ e) from a rendered CST, the+-- effect of the '--hide-rho' switch. It runs after 'withSugarType', so it also+-- removes the ρ ↦ ∅ that 'bdWithVoidRho' re-inserts into every formation on the+-- SALTY path. Only formation bindings are stripped: dispatches such as ξ.ρ and+-- application arguments are left untouched, and a formation left empty by the+-- strip collapses to the compact '⟦⟧' layout.+withoutRho :: EXPRESSION -> EXPRESSION+withoutRho = goExpr+  where+    goExpr :: EXPRESSION -> EXPRESSION+    goExpr EX_FORMATION{..} = case goBinding binding of+      empty@BI_EMPTY{} -> EX_FORMATION lsb NO_EOL NO_TAB empty NO_EOL NO_TAB rsb+      binding' -> EX_FORMATION lsb eol tab binding' eol' tab' rsb+    goExpr EX_DISPATCH{..} = EX_DISPATCH (goExpr expr) space attr+    goExpr EX_APPLICATION{..} = EX_APPLICATION (goExpr expr) space eol tab (goArgument argument) eol' tab' indent+    goExpr EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (goExpr expr)+    goExpr EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (goExpr expr)+    goExpr expr = expr+    -- Formation bindings: drop the ρ pairs, recurse into whatever remains.+    goBinding :: BINDING -> BINDING+    goBinding empty@BI_EMPTY{} = empty+    goBinding BI_META{..} = BI_META meta (goBindings bindings) tab+    goBinding BI_PAIR{..}+      | isRho pair = promote tab (goBindings bindings)+      | otherwise = BI_PAIR (goPair pair) (goBindings bindings) tab+    goBindings :: BINDINGS -> BINDINGS+    goBindings empty@BDS_EMPTY{} = empty+    goBindings BDS_META{..} = BDS_META eol tab meta (goBindings bindings)+    goBindings BDS_PAIR{..}+      | isRho pair = goBindings bindings+      | otherwise = BDS_PAIR eol tab (goPair pair) (goBindings bindings)+    -- Turn the tail chain back into a head binding once its leading pair was+    -- dropped; the promoted pair is already stripped and recursed by 'goBindings'.+    promote :: TAB -> BINDINGS -> BINDING+    promote tab (BDS_EMPTY _) = BI_EMPTY tab+    promote tab (BDS_PAIR _ _ pair bindings) = BI_PAIR pair bindings tab+    promote tab (BDS_META _ _ meta bindings) = BI_META meta bindings tab+    -- Application arguments keep their ρ (bdWithVoidRho never adds one there);+    -- only recurse into the expressions they carry.+    goArgument :: APP_ARGUMENT -> APP_ARGUMENT+    goArgument (AA_TAU binding) = AA_TAU (goAppBinding binding)+    goArgument (AA_TAUS binding) = AA_TAUS (goArgBinding binding)+    goArgument (AA_EXPRS args) = AA_EXPRS (goAppArg args)+    goAppBinding :: APP_BINDING -> APP_BINDING+    goAppBinding APP_BINDING{..} = APP_BINDING (goPair pair)+    goArgBinding :: BINDING -> BINDING+    goArgBinding empty@BI_EMPTY{} = empty+    goArgBinding BI_META{..} = BI_META meta (goArgBindings bindings) tab+    goArgBinding BI_PAIR{..} = BI_PAIR (goPair pair) (goArgBindings bindings) tab+    goArgBindings :: BINDINGS -> BINDINGS+    goArgBindings empty@BDS_EMPTY{} = empty+    goArgBindings BDS_META{..} = BDS_META eol tab meta (goArgBindings bindings)+    goArgBindings BDS_PAIR{..} = BDS_PAIR eol tab (goPair pair) (goArgBindings bindings)+    goAppArg :: APP_ARG -> APP_ARG+    goAppArg APP_ARG{..} = APP_ARG (goExpr expr) (goAppArgs args)+    goAppArgs :: APP_ARGS -> APP_ARGS+    goAppArgs AAS_EMPTY = AAS_EMPTY+    goAppArgs AAS_EXPR{..} = AAS_EXPR eol tab (goExpr expr) (goAppArgs args)+    goPair :: PAIR -> PAIR+    goPair PA_TAU{..} = PA_TAU attr arrow (goExpr expr)+    goPair PA_ALPHA{..} = PA_ALPHA alpha arrow (goExpr expr)+    goPair PA_FORMATION{..} = PA_FORMATION attr voids arrow (goExpr expr)+    goPair pair = pair+    isRho :: PAIR -> Bool+    isRho PA_VOID{attr = AT_RHO _} = True+    isRho PA_TAU{attr = AT_RHO _} = True+    isRho PA_FORMATION{attr = AT_RHO _} = True+    isRho _ = False  -- By default CST is generated with all possible syntax sugar -- The main purpose of this class is to get rid of syntax sugar

@@ -137,6 +137,25 @@           ["--pin=", "rewrite"]           ["Version mismatch: --pin requires ''"] +  describe "--hide-rho" $ do+    it "drops every rho binding from the default salty output" $+      withStdin "[[ foo -> [[ x -> [[ ]], ^ -> $.y ]], y -> [[ ]] ]]" $+        testCLISucceeded+          ["rewrite", "--flat", "--hide-rho"]+          ["⟦ foo ↦ ⟦ x ↦ ⟦⟧ ⟧, y ↦ ⟦⟧ ⟧"]++    it "also drops the rho that --sweet leaves behind" $+      withStdin "[[ foo -> [[ x -> [[ ]], ^ -> $.y ]], y -> [[ ]] ]]" $+        testCLISucceeded+          ["rewrite", "--flat", "--sweet", "--hide-rho"]+          ["⟦ foo ↦ ⟦ x ↦ ⟦⟧ ⟧, y ↦ ⟦⟧ ⟧"]++    it "keeps sweet numeric literals intact" $+      withStdin "[[ a -> 42 ]]" $+        testCLISucceeded+          ["rewrite", "--flat", "--sweet", "--hide-rho"]+          ["⟦ a ↦ 42 ⟧"]+   it "prints debug info with --log-level=DEBUG" $     withStdin "[[]]" $       testCLISucceeded ["rewrite", "--log-level=DEBUG"] ["[DEBUG]:"]@@ -542,6 +561,65 @@               [ "⟦ x ↦ \"foo\" ⟧"               , "Φ.x( y ↦ \"foo\" )"               , "⟦ x ↦ \"foo\" ⟧"+              ]+          ]++    it "prefixes every step with a header when --headers is on" $+      withStdin "[[ x -> \"foo\" ]]" $+        testCLISucceeded+          [ "rewrite"+          , rule "first.yaml"+          , rule "second.yaml"+          , "--max-depth=1"+          , "--max-cycles=2"+          , "--sequence"+          , "--headers"+          , "--sweet"+          , "--flat"+          ]+          [ intercalate+              "\n"+              [ ""+              , "=== Step #1"+              , "⟦ x ↦ \"foo\" ⟧"+              , ""+              , "=== Step #2, Rule 'first', 31t -> 30t"+              , "Φ.x( y ↦ \"foo\" )"+              , ""+              , "=== Step #3, Rule 'second', 30t -> 31t"+              , "⟦ x ↦ \"foo\" ⟧"+              ]+          ]++    it "ignores --headers without --sequence" $+      withStdin "[[ x -> \"foo\" ]]" $+        testCLISucceeded+          ["rewrite", rule "simple.yaml", "--headers", "--sweet", "--flat"]+          ["⟦ x ↦ \"bar\" ⟧"]++    it "emits step headers as LaTeX comments with --headers" $+      withStdin "[[ x -> \"foo\" ]]" $+        testCLISucceeded+          [ "rewrite"+          , rule "first.yaml"+          , rule "second.yaml"+          , "--max-depth=1"+          , "--max-cycles=2"+          , "--sequence"+          , "--headers"+          , "--sweet"+          , "--flat"+          , "--output=latex"+          ]+          [ unlines+              [ "\\begin{phiquation}"+              , "% === Step #1"+              , "[[ |x| -> \"foo\" ]] \\leadsto_{\\nameref{r:first}}"+              , "% === Step #2, Rule 'first', 31t -> 30t"+              , "  \\leadsto Q . |x| ( |y| -> \"foo\" ) \\leadsto_{\\nameref{r:second}}"+              , "% === Step #3, Rule 'second', 30t -> 31t"+              , "  \\leadsto [[ |x| -> \"foo\" ]]{.}"+              , "\\end{phiquation}"               ]           ] 

@@ -10,6 +10,7 @@ import AST import Control.Monad (forM_) import Data.Either (isLeft, isRight)+import Data.List (isInfixOf) import Files (allPathsIn) import Parser import System.FilePath (takeBaseName)@@ -26,6 +27,15 @@       Just right -> function ipt `shouldBe` Right right       _ -> function ipt `shouldSatisfy` isLeft +fails ::+  (Show a) =>+  (String -> Either String a) ->+  [(String, String)] ->+  SpecWith (Arg Expectation)+fails function useCases =+  forM_ useCases $ \(ipt, fragment) ->+    it ipt (function ipt `shouldSatisfy` either (isInfixOf fragment) (const False))+ spec :: Spec spec = do   describe "parse expression" $@@ -245,6 +255,25 @@           , "⟦ k ↦ ⟦ Δ ⤍ 42-, Δ ⤍ 55- ⟧ ⟧"           ]       )++  describe "points at the typo instead of the beginning of the binding" $+    fails+      parseExpression+      [ ("[[ D> x ]]", "expression:1:7:")+      , ("[[ L> 42 ]]", "expression:1:7:")+      , ("⟦ a ↦ Φ.foo() ⟧", "expression:1:13:")+      , ("[[ x -> ]]", "expression:1:9:")+      , ("[[ x -> Q.y(] ]]", "expression:1:13:")+      , ("[[ y -> 5, x -> Q.z(} ]]", "expression:1:21:")+      ]++  describe "tells what a binding prefix may be followed by" $+    fails+      parseExpression+      [ ("[[ D> x ]]", "expecting bytes")+      , ("[[ L> 42 ]]", "function name")+      , ("[[ x -> ]]", "expecting '?', '∅', or expression head")+      ]    describe "parse packs" $ do     packs <- runIO (allPathsIn "test-resources/parser-packs")

@@ -122,6 +122,46 @@           it desc (printExpression' expr (SALTY, UNICODE, SINGLELINE, defaultMargin) `shouldBe` expected)       ) +  describe "printExpressionHidingRho strips every rho binding for --hide-rho" $ do+    let issueExpr =+          ExFormation+            [ BiTau+                (AtLabel "foo")+                ( ExFormation+                    [ BiTau (AtLabel "x") (ExFormation [BiVoid AtRho])+                    , BiTau AtRho (ExDispatch ExXi (AtLabel "y"))+                    ]+                )+            , BiTau (AtLabel "y") (ExFormation [BiVoid AtRho])+            , BiVoid AtRho+            ]+    forM_+      [ ("salty clears both void and dispatch-valued rho", SALTY, issueExpr, "⟦ foo ↦ ⟦ x ↦ ⟦⟧ ⟧, y ↦ ⟦⟧ ⟧")+      , ("sweet also drops the rho that --sweet keeps", SWEET, issueExpr, "⟦ foo ↦ ⟦ x ↦ ⟦⟧ ⟧, y ↦ ⟦⟧ ⟧")+      ,+        ( "a rho bound to an expression is removed"+        , SWEET+        , ExFormation [BiTau (AtLabel "a") ExRoot, BiTau AtRho (ExDispatch ExXi (AtLabel "y"))]+        , "⟦ a ↦ Φ ⟧"+        )+      , ("a formation holding only rho collapses to empty", SALTY, ExFormation [BiVoid AtRho], "⟦⟧")+      ,+        ( "a ξ.ρ dispatch value is left untouched"+        , SALTY+        , ExFormation [BiTau (AtLabel "a") (ExDispatch ExXi AtRho)]+        , "⟦ a ↦ ξ.ρ ⟧"+        )+      ]+      ( \(desc, sugar, expr, expected) ->+          it desc (printExpressionHidingRho' expr (sugar, UNICODE, SINGLELINE, defaultMargin) `shouldBe` expected)+      )++  describe "printExpressionHidingRho keeps primitives that carry no visible rho" $+    it "renders a sweet numeric literal exactly as printExpression' does" $ do+      let number = DataNumber (BtMany ["40", "45", "00", "00", "00", "00", "00", "00"])+          config = (SWEET, UNICODE, SINGLELINE, defaultMargin)+      printExpressionHidingRho' number config `shouldBe` printExpression' number config+   describe "printAttribute with default encoding" $     forM_       [ ("label", AtLabel "attr", "attr")