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.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. @@ -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 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.106 +version: 0.0.107 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs --- a/src/CLI/Helpers.hs +++ b/src/CLI/Helpers.hs @@ -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] diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs --- a/src/CLI/Parsers.hs +++ b/src/CLI/Parsers.hs @@ -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 diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -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 diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs --- a/src/CLI/Types.hs +++ b/src/CLI/Types.hs @@ -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 diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -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 ] ) diff --git a/src/Parser.hs b/src/Parser.hs --- a/src/Parser.hs +++ b/src/Parser.hs @@ -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" diff --git a/src/Printer.hs b/src/Printer.hs --- a/src/Printer.hs +++ b/src/Printer.hs @@ -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 diff --git a/src/Rewriter.hs b/src/Rewriter.hs --- a/src/Rewriter.hs +++ b/src/Rewriter.hs @@ -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]) diff --git a/src/Sugar.hs b/src/Sugar.hs --- a/src/Sugar.hs +++ b/src/Sugar.hs @@ -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 diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -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}" ] ] diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs --- a/test/ParserSpec.hs +++ b/test/ParserSpec.hs @@ -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") diff --git a/test/PrinterSpec.hs b/test/PrinterSpec.hs --- a/test/PrinterSpec.hs +++ b/test/PrinterSpec.hs @@ -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")