phino 0.0.0.60 → 0.0.0.61

raw patch · 25 files changed

+1446/−1108 lines, 25 files

Files

• README.md +1/−1
• phino.cabal +6/−2
• resources/copy.yaml +3/−1
• src/CLI.hs +9/−825
• src/CLI/Helpers.hs +118/−0
• src/CLI/Parsers.hs +343/−0
• src/CLI/Runners.hs +208/−0
• src/CLI/Types.hs +161/−0
• src/CLI/Validators.hs +61/−0
• src/CST.hs +159/−21
• src/Condition.hs +1/−1
• src/Dataize.hs +1/−1
• src/Encoding.hs +39/−6
• src/LaTeX.hs +91/−30
• src/Lining.hs +32/−0
• src/Margin.hs +6/−0
• src/Render.hs +74/−10
• src/Rewriter.hs +10/−7
• src/Rule.hs +1/−1
• src/Sugar.hs +32/−0
• src/Yaml.hs +2/−2
• test/CLISpec.hs +86/−5
• test/ConditionSpec.hs +1/−1
• test/LiningSpec.hs +0/−193
• test/RewriterSpec.hs +1/−1

@@ -29,7 +29,7 @@  ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.0.59+cabal install --overwrite-policy=always phino-0.0.0.60 phino --version ``` 

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.0.60+version: 0.0.0.61 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>@@ -38,6 +38,11 @@     Builder     Canonizer     CLI+    CLI.Helpers+    CLI.Parsers+    CLI.Runners+    CLI.Types+    CLI.Validators     Condition     CST     Dataize@@ -125,7 +130,6 @@     FilterSpec     FunctionsSpec     LaTeXSpec-    LiningSpec     LocatorSpec     MatcherSpec     MergeSpec

@@ -5,7 +5,9 @@ pattern: ⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑒1) result: ⟦ 𝐵1, 𝜏 ↦ 𝑒3, 𝐵2 ⟧ when:-  xi: 𝑒1+  and:+    - xi: 𝑒1+    - nf: 𝑒1 where:   - meta: 𝑒2     function: scope

@@ -1,7 +1,5 @@-{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-}  -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com@@ -9,508 +7,14 @@  module CLI (runCLI) where -import AST-import qualified Canonizer as C-import Condition (parseConditionThrows)-import Control.Exception.Base (Exception (displayException), SomeException, catch, fromException, handle, throwIO)-import Control.Monad (forM_, unless, when, (>=>))-import Data.Char (toLower, toUpper)-import Data.Foldable (for_)-import Data.Functor ((<&>))-import Data.List (intercalate)-import Data.Maybe (fromJust, fromMaybe, isJust, isNothing)-import Data.Version (showVersion)-import Dataize (DataizeContext (DataizeContext), dataize)-import Deps (SaveStepFunc, saveStep)-import Encoding (Encoding (UNICODE))-import qualified Filter as F-import Functions (buildTerm)-import LaTeX (LatexContext (LatexContext), defaultMeetLength, defaultMeetPopularity, explainRules, expressionToLaTeX, programToLaTeX, rewrittensToLatex)-import Lining (LineFormat (MULTILINE, SINGLELINE))-import Locator (locatedExpression)+import CLI.Parsers+import CLI.Runners+import CLI.Types+import Control.Exception.Base (Exception (displayException), SomeException, fromException, handle) import Logger-import Margin (defaultMargin)-import Merge (merge)-import Misc (ensuredFile)-import qualified Misc-import Must (Must (..), validateMust) import Options.Applicative-import Parser (parseExpressionThrows, parseProgramThrows)-import Paths_phino (version)-import qualified Printer as P-import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite)-import Rule (RuleContext (RuleContext), matchProgramWithRule)-import Sugar import System.Exit (ExitCode (..), exitFailure)-import System.IO (getContents')-import Text.Printf (printf)-import XMIR (XmirContext (XmirContext), defaultXmirContext, parseXMIRThrows, printXMIR, programToXMIR, xmirToPhi)-import Yaml (normalizationRules)-import qualified Yaml as Y -data PrintProgramContext = PrintProgCtx-  { _sugar :: SugarType-  , _line :: LineFormat-  , _margin :: Int-  , _xmirCtx :: XmirContext-  , _nonumber :: Bool-  , _compress :: Bool-  , _sequence :: Bool-  , _meetPopularity :: Int-  , _meetLength :: Int-  , _focus :: Expression-  , _expression :: Maybe String-  , _label :: Maybe String-  , _meetPrefix :: Maybe String-  , _outputFormat :: IOFormat-  }--data CmdException-  = InvalidCLIArguments String-  | CouldNotReadFromStdin String-  | CouldNotDataize-  | CouldNotPrintExpressionInXMIR-  deriving (Exception)--instance Show CmdException where-  show (InvalidCLIArguments msg) = printf "Invalid set of arguments: %s" msg-  show (CouldNotReadFromStdin msg) = printf "Could not read input from stdin\nReason: %s" msg-  show CouldNotDataize = "Could not dataize given program"-  show CouldNotPrintExpressionInXMIR = "Could not print expression with --output=xmir, only program printing is allowed"--data Command-  = CmdRewrite OptsRewrite-  | CmdDataize OptsDataize-  | CmdExplain OptsExplain-  | CmdMerge OptsMerge-  | CmdMatch OptsMatch--data IOFormat = XMIR | PHI | LATEX-  deriving (Eq)--instance Show IOFormat where-  show XMIR = "xmir"-  show PHI = "phi"-  show LATEX = "latex"--data OptsDataize = OptsDataize-  { _logLevel :: LogLevel-  , _logLines :: Int-  , _inputFormat :: IOFormat-  , _outputFormat :: IOFormat-  , _sugarType :: SugarType-  , _flat :: LineFormat-  , _omitListing :: Bool-  , _omitComments :: Bool-  , _nonumber :: Bool-  , _sequence :: Bool-  , _canonize :: Bool-  , _depthSensitive :: Bool-  , _quiet :: Bool-  , _compress :: Bool-  , _maxDepth :: Int-  , _maxCycles :: Int-  , _margin :: Int-  , _meetPopularity :: Maybe Int-  , _meetLength :: Maybe Int-  , _hide :: [String]-  , _show :: [String]-  , _locator :: String-  , _focus :: String-  , _expression :: Maybe String-  , _label :: Maybe String-  , _meetPrefix :: Maybe String-  , _stepsDir :: Maybe FilePath-  , _inputFile :: Maybe FilePath-  }--data OptsExplain = OptsExplain-  { _logLevel :: LogLevel-  , _logLines :: Int-  , _rules :: [FilePath]-  , _normalize :: Bool-  , _shuffle :: Bool-  , _targetFile :: Maybe FilePath-  }--data OptsRewrite = OptsRewrite-  { _logLevel :: LogLevel-  , _logLines :: Int-  , _inputFormat :: IOFormat-  , _outputFormat :: IOFormat-  , _sugarType :: SugarType-  , _flat :: LineFormat-  , _must :: Must-  , _normalize :: Bool-  , _shuffle :: Bool-  , _omitListing :: Bool-  , _omitComments :: Bool-  , _depthSensitive :: Bool-  , _nonumber :: Bool-  , _inPlace :: Bool-  , _sequence :: Bool-  , _canonize :: Bool-  , _compress :: Bool-  , _maxDepth :: Int-  , _maxCycles :: Int-  , _margin :: Int-  , _meetPopularity :: Maybe Int-  , _meetLength :: Maybe Int-  , _rules :: [FilePath]-  , _hide :: [String]-  , _show :: [String]-  , _locator :: String-  , _focus :: String-  , _expression :: Maybe String-  , _label :: Maybe String-  , _meetPrefix :: Maybe String-  , _targetFile :: Maybe FilePath-  , _stepsDir :: Maybe FilePath-  , _inputFile :: Maybe FilePath-  }--data OptsMerge = OptsMerge-  { _logLevel :: LogLevel-  , _logLines :: Int-  , _inputFormat :: IOFormat-  , _outputFormat :: IOFormat-  , _sugarType :: SugarType-  , _flat :: LineFormat-  , _omitListing :: Bool-  , _omitComments :: Bool-  , _margin :: Int-  , _targetFile :: Maybe FilePath-  , _inputs :: [FilePath]-  }--data OptsMatch = OptsMatch-  { _logLevel :: LogLevel-  , _logLines :: Int-  , _sugarType :: SugarType-  , _flat :: LineFormat-  , _pattern :: Maybe String-  , _when :: Maybe String-  , _inputFile :: Maybe FilePath-  }--validateIntOption :: (Int -> Bool) -> String -> Int -> ReadM Int-validateIntOption cmp msg num-  | cmp num = return num-  | otherwise = readerError msg--optLogLevel :: Parser LogLevel-optLogLevel =-  option-    parseLogLevel-    ( long "log-level"-        <> metavar "LEVEL"-        <> help ("Log level (" <> intercalate ", " (map show [DEBUG, ERROR, NONE]) <> ")")-        <> value ERROR-        <> showDefault-    )-  where-    parseLogLevel :: ReadM LogLevel-    parseLogLevel = eitherReader $ \lvl -> case map toUpper lvl of-      "DEBUG" -> Right DEBUG-      "ERROR" -> Right ERROR-      "ERR" -> Right ERROR-      "NONE" -> Right NONE-      _ -> Left $ "unknown log-level: " <> lvl--optLogLines :: Parser Int-optLogLines =-  option-    (auto >>= validateIntOption (>= -1) "--log-lines must be >= -1")-    (long "log-lines" <> metavar "LINES" <> help "Amount of lines printed to console per each log operation (0 - print nothing, -1 - no limits)" <> value 25 <> showDefault)--optRule :: Parser [FilePath]-optRule = many (strOption (long "rule" <> metavar "[FILE]" <> help "Path to custom rule"))--optInputFormat :: Parser IOFormat-optInputFormat = option (parseIOFormat "input") (long "input" <> metavar "FORMAT" <> help "Program input format (phi, xmir)" <> value PHI <> showDefault)--parseIOFormat :: String -> ReadM IOFormat-parseIOFormat type' = eitherReader $ \format -> case (map toLower format, type') of-  ("xmir", _) -> Right XMIR-  ("phi", _) -> Right PHI-  ("latex", "output") -> Right LATEX-  _ -> Left (printf "The value '%s' can't be used for '--%s' option, use --help to check possible values" format type')--optOutputFormat :: Parser IOFormat-optOutputFormat =-  option-    (parseIOFormat "output")-    (long "output" <> metavar "FORMAT" <> help (printf "Result and intermediate (see %s option(s)) programs output format (phi, xmir, latex)" _intermediateOptions) <> value PHI <> showDefault)--argInputFile :: Parser (Maybe FilePath)-argInputFile = optional (argument str (metavar "FILE" <> help "Path to input file"))--optMaxDepth :: Parser Int-optMaxDepth =-  option-    (auto >>= validateIntOption (> 0) "--max-depth must be positive")-    (long "max-depth" <> metavar "DEPTH" <> help "Maximum number of rewriting iterations per rule" <> value 25 <> showDefault)--optMaxCycles :: Parser Int-optMaxCycles =-  option-    (auto >>= validateIntOption (> 0) "--max-cycles must be positive")-    (long "max-cycles" <> metavar "CYCLES" <> help "Maximum number of rewriting cycles across all rules" <> value 25 <> showDefault)--optMargin :: Parser Int-optMargin =-  option-    (auto >>= validateIntOption (> 0) "--margin must be positive")-    (long "margin" <> help "The maximum right margin for the printed 𝜑-programs or 𝜑-expressions" <> value defaultMargin <> showDefault)--optMeetPopularity :: Parser (Maybe Int)-optMeetPopularity =-  optional-    ( option-        ( auto-            >>= validateIntOption (> 0) "--meet-popularity must be positive"-            >>= validateIntOption (< 100) "--meet-popularity must be <= 100"-        )-        ( long "meet-popularity"-            <> metavar "PERCENTAGE"-            <> help (printf "The minimum popularity of an expression in order to be suitable for \\phiMeet{}, in percentage (default: %d)" defaultMeetPopularity)-        )-    )--optMeetLength :: Parser (Maybe Int)-optMeetLength =-  optional-    ( option-        (auto >>= validateIntOption (> 0) "--meet-length must be positive")-        ( long "meet-length"-            <> metavar "NODES"-            <> help (printf "The minimum length of an expression that fits into \\phiMeet{}, in AST nodes (default: %d)" defaultMeetLength)-        )-    )--optDepthSensitive :: Parser Bool-optDepthSensitive = switch (long "depth-sensitive" <> help "Fail if rewriting is not finished after reaching max attempts (see --max-cycles or --max-depth)")--optNonumber :: Parser Bool-optNonumber = switch (long "nonumber" <> help "Turn off equation auto numbering in LaTeX rendering (see --output option)")--optSequence :: Parser Bool-optSequence = switch (long "sequence" <> help "Result output contains all intermediate 𝜑-programs concatenated with EOL")--optCanonize :: Parser Bool-optCanonize = switch (long "canonize" <> help "Rename all functions attached to λ binding with F1, F2, etc.")--optExpression :: Parser (Maybe String)-optExpression = optional (strOption (long "expression" <> metavar "NAME" <> help "Name for 'phiExpression' element when rendering to LaTeX (see --output option)"))--optLabel :: Parser (Maybe String)-optLabel = optional (strOption (long "label" <> metavar "NAME" <> help "Name for 'label' element when rendering to LaTeX (see --output option)"))--optMeetPrefix :: Parser (Maybe String)-optMeetPrefix = optional (strOption (long "meet-prefix" <> metavar "PREFIX" <> help "Prefix to be inserted before index in \\phiMeet{} and \\phiAgain{} LaTeX functions, e.g. \\phiMeet{foo:1}"))--optHide :: Parser [String]-optHide = many (strOption (long "hide" <> metavar "FQN" <> help "Location of object to exclude from result and intermediate programs after rewriting. Must be a valid dispatch expression; e.g. Q.org.eolang"))--optShow :: Parser [String]-optShow =-  many-    ( strOption-        ( long "show"-            <> metavar "FQN"-            <> help-              "Location of object to include to result and intermediate programs after rewriting. \-              \Must be a valid dispatch expression; e.g. Q.org.eolang. Unlike --hide, can be used only once"-        )-    )--optLocator :: Parser String-optLocator = strOption (long "locator" <> metavar "FQN" <> help "Location of object to dataize. Must be a valid dispatch expression; e.g. Q.foo.bar" <> value "Q" <> showDefault)--optFocus :: Parser String-optFocus =-  strOption-    ( long "focus"-        <> metavar "FQN"-        <> help "Location of only object to be printed in entire program. Must be a valid dispatch expression; e.g. Q.foo.bar"-        <> value "Q"-        <> showDefault-    )--optNormalize :: Parser Bool-optNormalize = switch (long "normalize" <> help "Use built-in normalization rules")--optTarget :: Parser (Maybe FilePath)-optTarget = optional (strOption (long "target" <> short 't' <> metavar "FILE" <> help "File to save output to"))--optStepsDir :: Parser (Maybe FilePath)-optStepsDir = optional (strOption (long "steps-dir" <> metavar "FILE" <> help "Directory to save intermediate steps during rewriting/dataizing"))--optShuffle :: Parser Bool-optShuffle = switch (long "shuffle" <> help "Shuffle rules before applying")--optSugar :: Parser SugarType-optSugar = flag SALTY SWEET (long "sweet" <> help (printf "Print result and intermediate (see %s option(s)) 𝜑-programs using syntax sugar" _intermediateOptions))--optSugar' :: Parser SugarType-optSugar' = flag SALTY SWEET (long "sweet" <> help "Print result 𝜑-program using syntax sugar")--optLineFormat :: Parser LineFormat-optLineFormat = flag MULTILINE SINGLELINE (long "flat" <> help (printf "Print result and intermediate (see %s option(s)) 𝜑-programs in one line" _intermediateOptions))--optLineFormat' :: Parser LineFormat-optLineFormat' = flag MULTILINE SINGLELINE (long "flat" <> help "Print result 𝜑-program in one line")--optOmitListing :: Parser Bool-optOmitListing = switch (long "omit-listing" <> help "Omit full program listing in XMIR output")--optOmitComments :: Parser Bool-optOmitComments = switch (long "omit-comments" <> help "Omit comments in XMIR output")--optCompress :: Parser Bool-optCompress = switch (long "compress" <> help "Compress expressions in LaTeX output using \\phiMeet{} and \\phiAgain{} functions")--_intermediateOptions :: String-_intermediateOptions = intercalate ", " ["--sequence", "--steps-dir"]--explainParser :: Parser Command-explainParser =-  CmdExplain-    <$> ( OptsExplain-            <$> optLogLevel-            <*> optLogLines-            <*> optRule-            <*> optNormalize-            <*> optShuffle-            <*> optTarget-        )--dataizeParser :: Parser Command-dataizeParser =-  CmdDataize-    <$> ( OptsDataize-            <$> optLogLevel-            <*> optLogLines-            <*> optInputFormat-            <*> optOutputFormat-            <*> optSugar-            <*> optLineFormat-            <*> optOmitListing-            <*> optOmitComments-            <*> optNonumber-            <*> optSequence-            <*> optCanonize-            <*> optDepthSensitive-            <*> switch (long "quiet" <> help "Don't print the result of dataization")-            <*> optCompress-            <*> optMaxDepth-            <*> optMaxCycles-            <*> optMargin-            <*> optMeetPopularity-            <*> optMeetLength-            <*> optHide-            <*> optShow-            <*> optLocator-            <*> optFocus-            <*> optExpression-            <*> optLabel-            <*> optMeetPrefix-            <*> optStepsDir-            <*> argInputFile-        )--rewriteParser :: Parser Command-rewriteParser =-  CmdRewrite-    <$> ( OptsRewrite-            <$> optLogLevel-            <*> optLogLines-            <*> optInputFormat-            <*> optOutputFormat-            <*> optSugar-            <*> optLineFormat-            <*> option-              auto-              ( long "must"-                  <> metavar "RANGE"-                  <> help "Must-rewrite range (e.g., '3', '..5', '3..', '3..5'). Stops execution if number of rules applied is not in range. Use 0 to disable."-                  <> value MtDisabled-                  <> showDefaultWith show-              )-            <*> optNormalize-            <*> optShuffle-            <*> optOmitListing-            <*> optOmitComments-            <*> optDepthSensitive-            <*> optNonumber-            <*> switch (long "in-place" <> help "Edit file in-place instead of printing to output")-            <*> optSequence-            <*> optCanonize-            <*> optCompress-            <*> optMaxDepth-            <*> optMaxCycles-            <*> optMargin-            <*> optMeetPopularity-            <*> optMeetLength-            <*> optRule-            <*> optHide-            <*> optShow-            <*> optLocator-            <*> optFocus-            <*> optExpression-            <*> optLabel-            <*> optMeetPrefix-            <*> optTarget-            <*> optStepsDir-            <*> argInputFile-        )--mergeParser :: Parser Command-mergeParser =-  CmdMerge-    <$> ( OptsMerge-            <$> optLogLevel-            <*> optLogLines-            <*> optInputFormat-            <*> option (parseIOFormat "output") (long "output" <> metavar "FORMAT" <> help (printf "Result program output format (phi, xmir, latex)") <> value PHI <> showDefault)-            <*> optSugar'-            <*> optLineFormat'-            <*> optOmitListing-            <*> optOmitComments-            <*> optMargin-            <*> optTarget-            <*> many (argument str (metavar "[FILE]" <> help "Paths to input files"))-        )--matchParser :: Parser Command-matchParser =-  CmdMatch-    <$> ( OptsMatch-            <$> optLogLevel-            <*> optLogLines-            <*> optSugar-            <*> optLineFormat-            <*> optional (strOption (long "pattern" <> metavar "EXPRESSION" <> help "Pattern expression to match against"))-            <*> optional (strOption (long "when" <> metavar "CONDITION" <> help "Predicate for matched substitutions"))-            <*> argInputFile-        )--commandParser :: Parser Command-commandParser =-  hsubparser-    ( command "rewrite" (info rewriteParser (progDesc "Rewrite the 𝜑-program"))-        <> command "dataize" (info dataizeParser (progDesc "Dataize the 𝜑-program"))-        <> command "explain" (info explainParser (progDesc "Explain rules in LaTeX format"))-        <> command "merge" (info mergeParser (progDesc "Merge 𝜑-programs into single one by merging their top level formations"))-        <> command "match" (info matchParser (progDesc "Match 𝜑-program against provided pattern and build matched substitutions"))-    )--parserInfo :: ParserInfo Command-parserInfo =-  info-    (commandParser <**> helper <**> simpleVersioner (showVersion version))-    (fullDesc <> header "Phino - CLI Manipulator of 𝜑-Calculus Expressions")- handler :: SomeException -> IO () handler e = case fromException e of   Just ExitSuccess -> pure () -- prevent printing error on --version etc.@@ -528,333 +32,13 @@         CmdMatch OptsMatch{_logLevel, _logLines} -> (_logLevel, _logLines)    in setLogConfig level lns -invalidCLIArguments :: String -> IO a-invalidCLIArguments msg = throwIO (InvalidCLIArguments msg)- runCLI :: [String] -> IO () runCLI args = handle handler $ do   cmd <- handleParseResult (execParserPure defaultPrefs parserInfo args)   setLogger cmd   case cmd of-    CmdRewrite OptsRewrite{..} -> do-      validateOpts-      excluded <- validatedDispatches "hide" _hide-      included <- validatedDispatches "show" _show-      [loc] <- validatedDispatches "locator" [_locator]-      [foc] <- validatedDispatches "focus" [_focus]-      logDebug (printf "Amount of rewriting cycles across all the rules: %d, per rule: %d" _maxCycles _maxDepth)-      input <- readInput _inputFile-      rules <- getRules _normalize _shuffle _rules-      program <- parseProgram input _inputFormat-      let listing = if null rules then const input else (\prog -> P.printProgram' prog (_sugarType, UNICODE, _flat, _margin))-          xmirCtx = XmirContext _omitListing _omitComments listing-          printCtx = printProgCtx xmirCtx foc-          canonize = if _canonize then C.canonize else id-          exclude = (`F.exclude` excluded)-          include = (`F.include` included)-      rewrittens <- rewrite program rules (context loc printCtx) <&> canonize . exclude . include-      let rewrittens' = if _sequence then rewrittens else [last rewrittens]-      logDebug (printf "Printing rewritten 𝜑-program as %s" (show _outputFormat))-      progs <- printRewrittens printCtx rewrittens'-      output _targetFile progs-      where-        validateOpts :: IO ()-        validateOpts = do-          when-            (_inPlace && isNothing _inputFile)-            (invalidCLIArguments "The option --in-place requires an input file")-          when-            (_inPlace && isJust _targetFile)-            (invalidCLIArguments "The options --in-place and --target cannot be used together")-          when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")-          validateLatexOptions-            _outputFormat-            [(_nonumber, "nonumber"), (_compress, "compress")]-            [(_expression, "expression"), (_label, "label"), (_meetPrefix, "meet-prefix")]-            [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]-          validateMust' _must-          validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus-        output :: Maybe FilePath -> String -> IO ()-        output target prog = case (_inPlace, target, _inputFile) of-          (True, _, Just file) -> do-            logDebug (printf "The option '--in-place' is specified, writing back to '%s'..." file)-            writeFile file prog-            logDebug (printf "The file '%s' was modified in-place" file)-          (True, _, Nothing) ->-            error "The option --in-place requires an input file"-          (False, Just file, _) -> do-            logDebug (printf "The option '--target' is specified, printing to '%s'..." file)-            writeFile file prog-            logDebug (printf "The command result was saved in '%s'" file)-          (False, Nothing, _) -> do-            logDebug "The option '--target' is not specified, printing to console..."-            putStrLn prog-        context :: Expression -> PrintProgramContext -> RewriteContext-        context loc ctx =-          RewriteContext-            loc-            _maxDepth-            _maxCycles-            _depthSensitive-            buildTerm-            _must-            (saveStepFunc _stepsDir ctx)-        printProgCtx :: XmirContext -> Expression -> PrintProgramContext-        printProgCtx xmirCtx focus =-          PrintProgCtx-            _sugarType-            _flat-            _margin-            xmirCtx-            _nonumber-            _compress-            _sequence-            (justMeetPopularity _meetPopularity)-            (justMeetLength _meetLength)-            focus-            _expression-            _label-            _meetPrefix-            _outputFormat-    CmdDataize OptsDataize{..} -> do-      validateOpts-      excluded <- validatedDispatches "hide" _hide-      included <- validatedDispatches "show" _show-      [loc] <- validatedDispatches "locator" [_locator]-      [foc] <- validatedDispatches "focus" [_focus]-      input <- readInput _inputFile-      prog <- parseProgram input _inputFormat-      let printCtx = printProgCtx foc-          canonize = if _canonize then C.canonize else id-          exclude = (`F.exclude` excluded)-          include = (`F.include` included)-      (maybeBytes, chain) <- dataize (context loc prog printCtx)-      when _sequence (printRewrittens printCtx (canonize $ exclude $ include chain) >>= putStrLn)-      unless _quiet (putStrLn (maybe (P.printExpression ExTermination) P.printBytes maybeBytes))-      where-        validateOpts :: IO ()-        validateOpts = do-          validateLatexOptions-            _outputFormat-            [(_nonumber, "nonumber"), (_compress, "compress")]-            [(_expression, "expression"), (_label, "label"), (_meetPrefix, "meet-prefix")]-            [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]-          validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus-          when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")-        context :: Expression -> Program -> PrintProgramContext -> DataizeContext-        context loc prog ctx =-          DataizeContext-            loc-            prog-            _maxDepth-            _maxCycles-            _depthSensitive-            buildTerm-            (saveStepFunc _stepsDir ctx)-        printProgCtx :: Expression -> PrintProgramContext-        printProgCtx focus =-          PrintProgCtx-            _sugarType-            _flat-            _margin-            defaultXmirContext-            _nonumber-            _compress-            _sequence-            (justMeetPopularity _meetPopularity)-            (justMeetLength _meetLength)-            focus-            _expression-            _label-            _meetPrefix-            _outputFormat-    CmdExplain OptsExplain{..} -> do-      validateOpts-      rules <- getRules _normalize _shuffle _rules-      printOut _targetFile (explainRules rules)-      where-        validateOpts :: IO ()-        validateOpts =-          when-            (null _rules && not _normalize)-            (throwIO (InvalidCLIArguments "Either --rule or --normalize must be specified"))-    CmdMerge OptsMerge{..} -> do-      validateOpts-      inputs' <- traverse (readInput . Just) _inputs-      progs <- traverse (`parseProgram` _inputFormat) inputs'-      prog <- merge progs-      let listing = const (P.printProgram' prog (_sugarType, UNICODE, _flat, _margin))-          xmirCtx = XmirContext _omitListing _omitComments listing-          printCtx = printProgCtx xmirCtx-      prog' <- printProgram printCtx prog-      printOut _targetFile prog'-      where-        validateOpts :: IO ()-        validateOpts = do-          when-            (null _inputs)-            (throwIO (InvalidCLIArguments "At least one input file must be specified for 'merge' command"))-          validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] "Q"-        printProgCtx :: XmirContext -> PrintProgramContext-        printProgCtx xmirCtx =-          PrintProgCtx-            _sugarType-            _flat-            _margin-            xmirCtx-            False-            False-            False-            (justMeetPopularity Nothing)-            (justMeetLength Nothing)-            ExGlobal-            Nothing-            Nothing-            Nothing-            _outputFormat-    CmdMatch OptsMatch{..} -> do-      input <- readInput _inputFile-      prog <- parseProgram input PHI-      if isNothing _pattern-        then logDebug "The --pattern is not provided, no substitutions are built"-        else do-          ptn <- parseExpressionThrows (fromJust _pattern)-          condition <- traverse parseConditionThrows _when-          substs <- matchProgramWithRule prog (rule ptn condition) (RuleContext buildTerm)-          if null substs-            then logDebug "Provided pattern was not matched, no substitutions are built"-            else putStrLn (P.printSubsts' substs (_sugarType, UNICODE, _flat, defaultMargin))-      where-        rule :: Expression -> Maybe Y.Condition -> Y.Rule-        rule ptn cnd = Y.Rule Nothing Nothing ptn ExGlobal cnd Nothing Nothing--justMeetPopularity :: Maybe Int -> Int-justMeetPopularity = fromMaybe defaultMeetPopularity--justMeetLength :: Maybe Int -> Int-justMeetLength = fromMaybe defaultMeetLength---- Prepare saveStepFunc-saveStepFunc :: Maybe FilePath -> PrintProgramContext -> SaveStepFunc-saveStepFunc stepsDir ctx@PrintProgCtx{..} = saveStep stepsDir ioToExt (printProgram ctx)-  where-    ioToExt :: String-    ioToExt-      | _outputFormat == LATEX = "tex"-      | otherwise = show _outputFormat---- Validate given expressions as valid dispatches-validatedDispatches :: String -> [String] -> IO [Expression]-validatedDispatches opt = traverse (parseExpressionThrows >=> asDispatch)-  where-    asDispatch :: Expression -> IO Expression-    asDispatch expr = asDispatch' expr-      where-        asDispatch' :: Expression -> IO Expression-        asDispatch' ex@ExGlobal = pure ex-        asDispatch' disp@(ExDispatch ex _) = asDispatch' ex >> pure disp-        asDispatch' _ =-          invalidCLIArguments-            ( printf-                "Only dispatch expression started with Φ (or Q) can be used in --%s, but given: %s"-                opt-                (P.printExpression' expr P.logPrintConfig)-            )---- Validate LaTeX options-validateLatexOptions :: IOFormat -> [(Bool, String)] -> [(Maybe String, String)] -> [(Maybe Int, String)] -> IO ()-validateLatexOptions LATEX _ _ _ = pure ()-validateLatexOptions _ bools strings ints = do-  let (bools', opts) = unzip bools-      msg = "The --%s option can stay together with --output=latex only"-      callback (maybe', opt) = when (isJust maybe') (invalidCLIArguments (printf msg opt))-  validateBoolOpts (zip bools' (map (printf msg) opts))-  forM_ strings callback-  forM_ ints callback---- Validate 'must' option-validateMust' :: Must -> IO ()-validateMust' must = for_ (validateMust must) invalidCLIArguments---- Validate options for output to XMIR-validateXmirOptions :: IOFormat -> [(Bool, String)] -> String -> IO ()-validateXmirOptions XMIR _ focus = when (focus /= "Q") (invalidCLIArguments "Only --focus=Q is allowed to be used with --output=xmir")-validateXmirOptions _ bools _ =-  let (bools', opts) = unzip bools-   in validateBoolOpts (zip bools' (map (printf "The --%s can be used only with --output=xmir") opts))--validateBoolOpts :: [(Bool, String)] -> IO ()-validateBoolOpts bools = forM_ bools (\(bool, msg) -> when bool (invalidCLIArguments msg))---- Read input from file or stdin-readInput :: Maybe FilePath -> IO String-readInput inputFile' = case inputFile' of-  Just pth -> do-    logDebug (printf "Reading from file: '%s'" pth)-    readFile =<< ensuredFile pth-  Nothing -> do-    logDebug "Reading from stdin"-    getContents' `catch` (\(e :: SomeException) -> throwIO (CouldNotReadFromStdin (show e)))---- Parse program from String input depending on input IO format-parseProgram :: String -> IOFormat -> IO Program-parseProgram phi PHI = parseProgramThrows phi-parseProgram xmir XMIR = do-  doc <- parseXMIRThrows xmir-  xmirToPhi doc-parseProgram _ LATEX = invalidCLIArguments "LaTeX cannot be used as input format"--printRewrittens :: PrintProgramContext -> [Rewritten] -> IO String-printRewrittens ctx@PrintProgCtx{..} rewrittens-  | _outputFormat == LATEX && _sequence = rewrittensToLatex rewrittens (LatexContext _sugar _line _margin _nonumber _compress _meetPopularity _meetLength _focus _expression _label _meetPrefix)-  | _focus == ExGlobal = mapM (printProgram ctx . fst) rewrittens <&> intercalate "\n"-  | otherwise = mapM (\(prog, _) -> locatedExpression _focus prog >>= printExpression ctx) rewrittens <&> intercalate "\n"--printExpression :: PrintProgramContext -> Expression -> IO String-printExpression PrintProgCtx{..} ex = case _outputFormat of-  PHI -> pure (P.printExpression' ex (_sugar, UNICODE, _line, _margin))-  XMIR -> throwIO CouldNotPrintExpressionInXMIR-  LATEX -> pure (expressionToLaTeX ex (LatexContext _sugar _line _margin _nonumber _compress _meetPopularity _meetLength _focus _expression _label _meetPrefix))---- Convert--- Convert program to corresponding String format-printProgram :: PrintProgramContext -> Program -> IO String-printProgram PrintProgCtx{..} prog = case _outputFormat of-  PHI -> pure (P.printProgram' prog (_sugar, UNICODE, _line, _margin))-  XMIR -> programToXMIR prog _xmirCtx <&> printXMIR-  LATEX -> pure (programToLaTeX prog (LatexContext _sugar _line _margin _nonumber _compress _meetPopularity _meetLength _focus _expression _label _meetPrefix))---- Get rules for rewriting depending on provided flags-getRules :: Bool -> Bool -> [FilePath] -> IO [Y.Rule]-getRules normalize shuffle rules = do-  ordered <--    if normalize-      then do-        let rules' = normalizationRules-        logDebug (printf "The --normalize option is provided, %d built-it normalization rules are used" (length rules'))-        pure rules'-      else-        if null rules-          then do-            logDebug "No --rule and no --normalize options are provided, no rules are used"-            pure []-          else do-            logDebug (printf "Using rules from files: [%s]" (intercalate ", " rules))-            yamls <- mapM ensuredFile rules-            mapM Y.yamlRule yamls-  if shuffle-    then do-      logDebug "The --shuffle option is provided, rules are used in random order"-      Misc.shuffle ordered-    else pure ordered---- Output content-printOut :: Maybe FilePath -> String -> IO ()-printOut target content = case target of-  Nothing -> do-    logDebug "The option '--target' is not specified, printing to console..."-    putStrLn content-  Just file -> do-    logDebug (printf "The option '--target' is specified, printing to '%s'..." file)-    writeFile file content-    logDebug (printf "The command result was saved in '%s'" file)+    CmdRewrite opts -> runRewrite opts+    CmdDataize opts -> runDataize opts+    CmdExplain opts -> runExplain opts+    CmdMerge opts -> runMerge opts+    CmdMatch opts -> runMatch opts

@@ -0,0 +1,118 @@+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}++module CLI.Helpers where++import AST+import CLI.Types+import CLI.Validators (invalidCLIArguments)+import Control.Exception+import Data.Functor ((<&>))+import Data.List (intercalate)+import Data.Maybe+import Deps (SaveStepFunc, saveStep)+import Encoding+import LaTeX (LatexContext (..), defaultMeetLength, defaultMeetPopularity, expressionToLaTeX, programToLaTeX, rewrittensToLatex)+import Locator (locatedExpression)+import Logger+import qualified Misc as M+import Parser (parseProgramThrows)+import qualified Printer as P+import Rewriter (Rewrittens)+import System.IO (getContents')+import Text.Printf (printf)+import XMIR (parseXMIRThrows, printXMIR, programToXMIR, xmirToPhi)+import Yaml (normalizationRules)+import qualified Yaml as Y++justMeetPopularity :: Maybe Int -> Int+justMeetPopularity = fromMaybe defaultMeetPopularity++justMeetLength :: Maybe Int -> Int+justMeetLength = fromMaybe defaultMeetLength++-- Prepare saveStepFunc+saveStepFunc :: Maybe FilePath -> PrintProgramContext -> SaveStepFunc+saveStepFunc stepsDir ctx@PrintProgCtx{..} = saveStep stepsDir ioToExt (printProgram ctx)+  where+    ioToExt :: String+    ioToExt+      | _outputFormat == LATEX = "tex"+      | otherwise = show _outputFormat++-- Read input from file or stdin+readInput :: Maybe FilePath -> IO String+readInput inputFile' = case inputFile' of+  Just pth -> do+    logDebug (printf "Reading from file: '%s'" pth)+    readFile =<< M.ensuredFile pth+  Nothing -> do+    logDebug "Reading from stdin"+    getContents' `catch` (\(e :: SomeException) -> throwIO (CouldNotReadFromStdin (show e)))++-- Parse program from String input depending on input IO format+parseProgram :: String -> IOFormat -> IO Program+parseProgram phi PHI = parseProgramThrows phi+parseProgram xmir XMIR = parseXMIRThrows xmir >>= xmirToPhi+parseProgram _ LATEX = invalidCLIArguments "LaTeX cannot be used as input format"++printRewrittens :: PrintProgramContext -> Rewrittens -> IO String+printRewrittens ctx@PrintProgCtx{..} rewrittens@(chain, _)+  | _outputFormat == LATEX && _sequence = rewrittensToLatex rewrittens (printCtxToLatexCtx ctx)+  | _focus == ExGlobal = mapM (printProgram ctx . fst) chain <&> intercalate "\n"+  | otherwise = mapM (\(prog, _) -> locatedExpression _focus prog >>= printExpression ctx) chain <&> intercalate "\n"++printExpression :: PrintProgramContext -> Expression -> IO String+printExpression ctx@PrintProgCtx{..} ex = case _outputFormat of+  PHI -> pure (P.printExpression' ex (_sugar, UNICODE, _line, _margin))+  XMIR -> throwIO CouldNotPrintExpressionInXMIR+  LATEX -> pure (expressionToLaTeX ex (printCtxToLatexCtx ctx))++-- Convert+-- Convert program to corresponding String format+printProgram :: PrintProgramContext -> Program -> IO String+printProgram ctx@PrintProgCtx{..} prog = case _outputFormat of+  PHI -> pure (P.printProgram' prog (_sugar, UNICODE, _line, _margin))+  XMIR -> programToXMIR prog _xmirCtx <&> printXMIR+  LATEX -> pure (programToLaTeX prog (printCtxToLatexCtx ctx))++printCtxToLatexCtx :: PrintProgramContext -> LatexContext+printCtxToLatexCtx PrintProgCtx{..} =+  LatexContext _sugar _line _margin _nonumber _compress _meetPopularity _meetLength _focus _expression _label _meetPrefix++-- Get rules for rewriting depending on provided flags+getRules :: Bool -> Bool -> [FilePath] -> IO [Y.Rule]+getRules normalize shuffle rules = do+  ordered <-+    if normalize+      then do+        let rules' = normalizationRules+        logDebug (printf "The --normalize option is provided, %d built-it normalization rules are used" (length rules'))+        pure rules'+      else+        if null rules+          then do+            logDebug "No --rule and no --normalize options are provided, no rules are used"+            pure []+          else do+            logDebug (printf "Using rules from files: [%s]" (intercalate ", " rules))+            yamls <- mapM M.ensuredFile rules+            mapM Y.yamlRule yamls+  if shuffle+    then do+      logDebug "The --shuffle option is provided, rules are used in random order"+      M.shuffle ordered+    else pure ordered++-- Output content+printOut :: Maybe FilePath -> String -> IO ()+printOut target content = case target of+  Nothing -> do+    logDebug "The option '--target' is not specified, printing to console..."+    putStrLn content+  Just file -> do+    logDebug (printf "The option '--target' is specified, printing to '%s'..." file)+    writeFile file content+    logDebug (printf "The command result was saved in '%s'" file)

@@ -0,0 +1,343 @@+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++module CLI.Parsers where++import CLI.Types+import Data.Char (toLower, toUpper)+import Data.List (intercalate)+import Data.Version (showVersion)+import LaTeX (defaultMeetLength, defaultMeetPopularity)+import Lining (LineFormat (..))+import Logger+import Margin (defaultMargin)+import Must+import Options.Applicative+import Paths_phino (version)+import Sugar (SugarType (..))+import Text.Printf (printf)++validateIntOption :: (Int -> Bool) -> String -> Int -> ReadM Int+validateIntOption cmp msg num+  | cmp num = return num+  | otherwise = readerError msg++optLogLevel :: Parser LogLevel+optLogLevel =+  option+    parseLogLevel+    ( long "log-level"+        <> metavar "LEVEL"+        <> help ("Log level (" <> intercalate ", " (map show [DEBUG, ERROR, NONE]) <> ")")+        <> value ERROR+        <> showDefault+    )+  where+    parseLogLevel :: ReadM LogLevel+    parseLogLevel = eitherReader $ \lvl -> case map toUpper lvl of+      "DEBUG" -> Right DEBUG+      "ERROR" -> Right ERROR+      "ERR" -> Right ERROR+      "NONE" -> Right NONE+      _ -> Left $ "unknown log-level: " <> lvl++optLogLines :: Parser Int+optLogLines =+  option+    (auto >>= validateIntOption (>= -1) "--log-lines must be >= -1")+    (long "log-lines" <> metavar "LINES" <> help "Amount of lines printed to console per each log operation (0 - print nothing, -1 - no limits)" <> value 25 <> showDefault)++optRule :: Parser [FilePath]+optRule = many (strOption (long "rule" <> metavar "[FILE]" <> help "Path to custom rule"))++optInputFormat :: Parser IOFormat+optInputFormat = option (parseIOFormat "input") (long "input" <> metavar "FORMAT" <> help "Program input format (phi, xmir)" <> value PHI <> showDefault)++parseIOFormat :: String -> ReadM IOFormat+parseIOFormat type' = eitherReader $ \format -> case (map toLower format, type') of+  ("xmir", _) -> Right XMIR+  ("phi", _) -> Right PHI+  ("latex", "output") -> Right LATEX+  _ -> Left (printf "The value '%s' can't be used for '--%s' option, use --help to check possible values" format type')++optOutputFormat :: Parser IOFormat+optOutputFormat =+  option+    (parseIOFormat "output")+    (long "output" <> metavar "FORMAT" <> help (printf "Result and intermediate (see %s option(s)) programs output format (phi, xmir, latex)" _intermediateOptions) <> value PHI <> showDefault)++argInputFile :: Parser (Maybe FilePath)+argInputFile = optional (argument str (metavar "FILE" <> help "Path to input file"))++optMaxDepth :: Parser Int+optMaxDepth =+  option+    (auto >>= validateIntOption (> 0) "--max-depth must be positive")+    (long "max-depth" <> metavar "DEPTH" <> help "Maximum number of rewriting iterations per rule" <> value 25 <> showDefault)++optMaxCycles :: Parser Int+optMaxCycles =+  option+    (auto >>= validateIntOption (> 0) "--max-cycles must be positive")+    (long "max-cycles" <> metavar "CYCLES" <> help "Maximum number of rewriting cycles across all rules" <> value 25 <> showDefault)++optMargin :: Parser Int+optMargin =+  option+    (auto >>= validateIntOption (> 0) "--margin must be positive")+    (long "margin" <> help "The maximum right margin for the printed 𝜑-programs or 𝜑-expressions" <> value defaultMargin <> showDefault)++optMeetPopularity :: Parser (Maybe Int)+optMeetPopularity =+  optional+    ( option+        ( auto+            >>= validateIntOption (> 0) "--meet-popularity must be positive"+            >>= validateIntOption (<= 100) "--meet-popularity must be <= 100"+        )+        ( long "meet-popularity"+            <> metavar "PERCENTAGE"+            <> help (printf "The minimum popularity of an expression in order to be suitable for \\phiMeet{}, in percentage (default: %d)" defaultMeetPopularity)+        )+    )++optMeetLength :: Parser (Maybe Int)+optMeetLength =+  optional+    ( option+        (auto >>= validateIntOption (> 0) "--meet-length must be positive")+        ( long "meet-length"+            <> metavar "NODES"+            <> help (printf "The minimum length of an expression that fits into \\phiMeet{}, in AST nodes (default: %d)" defaultMeetLength)+        )+    )++optDepthSensitive :: Parser Bool+optDepthSensitive = switch (long "depth-sensitive" <> help "Fail if rewriting is not finished after reaching max attempts (see --max-cycles or --max-depth)")++optNonumber :: Parser Bool+optNonumber = switch (long "nonumber" <> help "Turn off equation auto numbering in LaTeX rendering (see --output option)")++optSequence :: Parser Bool+optSequence = switch (long "sequence" <> help "Result output contains all intermediate 𝜑-programs concatenated with EOL")++optCanonize :: Parser Bool+optCanonize = switch (long "canonize" <> help "Rename all functions attached to λ binding with F1, F2, etc.")++optExpression :: Parser (Maybe String)+optExpression = optional (strOption (long "expression" <> metavar "NAME" <> help "Name for 'phiExpression' element when rendering to LaTeX (see --output option)"))++optLabel :: Parser (Maybe String)+optLabel = optional (strOption (long "label" <> metavar "NAME" <> help "Name for 'label' element when rendering to LaTeX (see --output option)"))++optMeetPrefix :: Parser (Maybe String)+optMeetPrefix = optional (strOption (long "meet-prefix" <> metavar "PREFIX" <> help "Prefix to be inserted before index in \\phiMeet{} and \\phiAgain{} LaTeX functions, e.g. \\phiMeet{foo:1}"))++optHide :: Parser [String]+optHide =+  many+    ( strOption+        ( long "hide"+            <> metavar "FQN"+            <> help "Location of object to exclude from result and intermediate programs after rewriting. Must be a valid dispatch expression; e.g. Q.org.eolang"+        )+    )++optShow :: Parser [String]+optShow =+  many+    ( strOption+        ( long "show"+            <> metavar "FQN"+            <> help+              "Location of object to include to result and intermediate programs after rewriting. \+              \Must be a valid dispatch expression; e.g. Q.org.eolang. Unlike --hide, can be used only once"+        )+    )++optLocator :: Parser String+optLocator = strOption (long "locator" <> metavar "FQN" <> help "Location of object to dataize. Must be a valid dispatch expression; e.g. Q.foo.bar" <> value "Q" <> showDefault)++optFocus :: Parser String+optFocus =+  strOption+    ( long "focus"+        <> metavar "FQN"+        <> help "Location of only object to be printed in entire program. Must be a valid dispatch expression; e.g. Q.foo.bar"+        <> value "Q"+        <> showDefault+    )++optNormalize :: Parser Bool+optNormalize = switch (long "normalize" <> help "Use built-in normalization rules")++optTarget :: Parser (Maybe FilePath)+optTarget = optional (strOption (long "target" <> short 't' <> metavar "FILE" <> help "File to save output to"))++optStepsDir :: Parser (Maybe FilePath)+optStepsDir = optional (strOption (long "steps-dir" <> metavar "FILE" <> help "Directory to save intermediate steps during rewriting/dataizing"))++optShuffle :: Parser Bool+optShuffle = switch (long "shuffle" <> help "Shuffle rules before applying")++optSugar :: Parser SugarType+optSugar = flag SALTY SWEET (long "sweet" <> help (printf "Print result and intermediate (see %s option(s)) 𝜑-programs using syntax sugar" _intermediateOptions))++optSugar' :: Parser SugarType+optSugar' = flag SALTY SWEET (long "sweet" <> help "Print result 𝜑-program using syntax sugar")++optLineFormat :: Parser LineFormat+optLineFormat = flag MULTILINE SINGLELINE (long "flat" <> help (printf "Print result and intermediate (see %s option(s)) 𝜑-programs in one line" _intermediateOptions))++optLineFormat' :: Parser LineFormat+optLineFormat' = flag MULTILINE SINGLELINE (long "flat" <> help "Print result 𝜑-program in one line")++optOmitListing :: Parser Bool+optOmitListing = switch (long "omit-listing" <> help "Omit full program listing in XMIR output")++optOmitComments :: Parser Bool+optOmitComments = switch (long "omit-comments" <> help "Omit comments in XMIR output")++optCompress :: Parser Bool+optCompress = switch (long "compress" <> help "Compress expressions in LaTeX output using \\phiMeet{} and \\phiAgain{} functions")++_intermediateOptions :: String+_intermediateOptions = intercalate ", " ["--sequence", "--steps-dir"]++explainParser :: Parser Command+explainParser =+  CmdExplain+    <$> ( OptsExplain+            <$> optLogLevel+            <*> optLogLines+            <*> optRule+            <*> optNormalize+            <*> optShuffle+            <*> optTarget+        )++dataizeParser :: Parser Command+dataizeParser =+  CmdDataize+    <$> ( OptsDataize+            <$> optLogLevel+            <*> optLogLines+            <*> optInputFormat+            <*> optOutputFormat+            <*> optSugar+            <*> optLineFormat+            <*> optOmitListing+            <*> optOmitComments+            <*> optNonumber+            <*> optSequence+            <*> optCanonize+            <*> optDepthSensitive+            <*> switch (long "quiet" <> help "Don't print the result of dataization")+            <*> optCompress+            <*> optMaxDepth+            <*> optMaxCycles+            <*> optMargin+            <*> optMeetPopularity+            <*> optMeetLength+            <*> optHide+            <*> optShow+            <*> optLocator+            <*> optFocus+            <*> optExpression+            <*> optLabel+            <*> optMeetPrefix+            <*> optStepsDir+            <*> argInputFile+        )++rewriteParser :: Parser Command+rewriteParser =+  CmdRewrite+    <$> ( OptsRewrite+            <$> optLogLevel+            <*> optLogLines+            <*> optInputFormat+            <*> optOutputFormat+            <*> optSugar+            <*> optLineFormat+            <*> option+              auto+              ( long "must"+                  <> metavar "RANGE"+                  <> help "Must-rewrite range (e.g., '3', '..5', '3..', '3..5'). Stops execution if number of rules applied is not in range. Use 0 to disable."+                  <> value MtDisabled+                  <> showDefaultWith show+              )+            <*> optNormalize+            <*> optShuffle+            <*> optOmitListing+            <*> optOmitComments+            <*> optDepthSensitive+            <*> optNonumber+            <*> switch (long "in-place" <> help "Edit file in-place instead of printing to output")+            <*> optSequence+            <*> optCanonize+            <*> optCompress+            <*> optMaxDepth+            <*> optMaxCycles+            <*> optMargin+            <*> optMeetPopularity+            <*> optMeetLength+            <*> optRule+            <*> optHide+            <*> optShow+            <*> optLocator+            <*> optFocus+            <*> optExpression+            <*> optLabel+            <*> optMeetPrefix+            <*> optTarget+            <*> optStepsDir+            <*> argInputFile+        )++mergeParser :: Parser Command+mergeParser =+  CmdMerge+    <$> ( OptsMerge+            <$> optLogLevel+            <*> optLogLines+            <*> optInputFormat+            <*> option (parseIOFormat "output") (long "output" <> metavar "FORMAT" <> help (printf "Result program output format (phi, xmir, latex)") <> value PHI <> showDefault)+            <*> optSugar'+            <*> optLineFormat'+            <*> optOmitListing+            <*> optOmitComments+            <*> optMargin+            <*> optTarget+            <*> many (argument str (metavar "[FILE]" <> help "Paths to input files"))+        )++matchParser :: Parser Command+matchParser =+  CmdMatch+    <$> ( OptsMatch+            <$> optLogLevel+            <*> optLogLines+            <*> optSugar+            <*> optLineFormat+            <*> optional (strOption (long "pattern" <> metavar "EXPRESSION" <> help "Pattern expression to match against"))+            <*> optional (strOption (long "when" <> metavar "CONDITION" <> help "Predicate for matched substitutions"))+            <*> argInputFile+        )++commandParser :: Parser Command+commandParser =+  hsubparser+    ( command "rewrite" (info rewriteParser (progDesc "Rewrite the 𝜑-program"))+        <> command "dataize" (info dataizeParser (progDesc "Dataize the 𝜑-program"))+        <> command "explain" (info explainParser (progDesc "Explain rules in LaTeX format"))+        <> command "merge" (info mergeParser (progDesc "Merge 𝜑-programs into single one by merging their top level formations"))+        <> command "match" (info matchParser (progDesc "Match 𝜑-program against provided pattern and build matched substitutions"))+    )++parserInfo :: ParserInfo Command+parserInfo =+  info+    (commandParser <**> helper <**> simpleVersioner (showVersion version))+    (fullDesc <> header "Phino - CLI Manipulator of 𝜑-Calculus Expressions")

@@ -0,0 +1,208 @@+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}++-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++module CLI.Runners where++import AST+import CLI.Helpers+import CLI.Types+import CLI.Validators+import qualified Canonizer as C+import Condition (parseConditionThrows)+import Control.Exception+import Control.Monad (unless, when)+import Data.Maybe (fromJust, isJust, isNothing)+import Dataize+import Encoding+import qualified Filter as F+import Functions (buildTerm)+import LaTeX (explainRules)+import Logger+import Margin (defaultMargin)+import Merge (merge)+import Parser (parseExpressionThrows)+import qualified Printer as P+import Rewriter+import Rule (RuleContext (..), matchProgramWithRule)+import Text.Printf (printf)+import XMIR+import qualified Yaml as Y++runRewrite :: OptsRewrite -> IO ()+runRewrite OptsRewrite{..} = do+  validateOpts+  excluded <- validatedDispatches "hide" _hide+  included <- validatedDispatches "show" _show+  [loc] <- validatedDispatches "locator" [_locator]+  [foc] <- validatedDispatches "focus" [_focus]+  logDebug (printf "Amount of rewriting cycles across all the rules: %d, per rule: %d" _maxCycles _maxDepth)+  input <- readInput _inputFile+  rules <- getRules _normalize _shuffle _rules+  program <- parseProgram input _inputFormat+  let listing = if null rules then const input else (\prog -> P.printProgram' prog (_sugarType, UNICODE, _flat, _margin))+      xmirCtx = XmirContext _omitListing _omitComments listing+      printCtx = printProgCtx xmirCtx foc+      canonize = if _canonize then C.canonize else id+      exclude = (`F.exclude` excluded)+      include = (`F.include` included)+  (rewrittens, exceeded) <- rewrite program rules (context loc printCtx)+  let rewrittens' = canonize $ exclude $ include (if _sequence then rewrittens else [last rewrittens])+  logDebug (printf "Printing rewritten 𝜑-program as %s" (show _outputFormat))+  progs <- printRewrittens printCtx (rewrittens', exceeded)+  output _targetFile progs+  where+    validateOpts :: IO ()+    validateOpts = do+      when (_inPlace && isNothing _inputFile) (invalidCLIArguments "The option --in-place requires an input file")+      when (_inPlace && isJust _targetFile) (invalidCLIArguments "The options --in-place and --target cannot be used together")+      when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")+      validateLatexOptions+        _outputFormat+        [(_nonumber, "nonumber"), (_compress, "compress")]+        [(_expression, "expression"), (_label, "label"), (_meetPrefix, "meet-prefix")]+        [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]+      validateMust' _must+      validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus+    output :: Maybe FilePath -> String -> IO ()+    output target prog = case (_inPlace, target, _inputFile) of+      (True, _, Just file) -> do+        logDebug (printf "The option '--in-place' is specified, writing back to '%s'..." file)+        writeFile file prog+        logDebug (printf "The file '%s' was modified in-place" file)+      (True, _, Nothing) ->+        error "The option --in-place requires an input file"+      (False, Just file, _) -> do+        logDebug (printf "The option '--target' is specified, printing to '%s'..." file)+        writeFile file prog+        logDebug (printf "The command result was saved in '%s'" file)+      (False, Nothing, _) -> do+        logDebug "The option '--target' is not specified, printing to console..."+        putStrLn prog+    context :: Expression -> PrintProgramContext -> RewriteContext+    context loc ctx = RewriteContext loc _maxDepth _maxCycles _depthSensitive buildTerm _must (saveStepFunc _stepsDir ctx)+    printProgCtx :: XmirContext -> Expression -> PrintProgramContext+    printProgCtx xmirCtx focus =+      PrintProgCtx+        _sugarType+        _flat+        _margin+        xmirCtx+        _nonumber+        _compress+        _sequence+        (justMeetPopularity _meetPopularity)+        (justMeetLength _meetLength)+        focus+        _expression+        _label+        _meetPrefix+        _outputFormat++runDataize :: OptsDataize -> IO ()+runDataize OptsDataize{..} = do+  validateOpts+  excluded <- validatedDispatches "hide" _hide+  included <- validatedDispatches "show" _show+  [loc] <- validatedDispatches "locator" [_locator]+  [foc] <- validatedDispatches "focus" [_focus]+  input <- readInput _inputFile+  prog <- parseProgram input _inputFormat+  let printCtx = printProgCtx foc+      canonize = if _canonize then C.canonize else id+      exclude = (`F.exclude` excluded)+      include = (`F.include` included)+  (maybeBytes, chain) <- dataize (context loc prog printCtx)+  when _sequence (printRewrittens printCtx (canonize $ exclude $ include chain, False) >>= putStrLn)+  unless _quiet (putStrLn (maybe (P.printExpression ExTermination) P.printBytes maybeBytes))+  where+    validateOpts :: IO ()+    validateOpts = do+      validateLatexOptions+        _outputFormat+        [(_nonumber, "nonumber"), (_compress, "compress")]+        [(_expression, "expression"), (_label, "label"), (_meetPrefix, "meet-prefix")]+        [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]+      validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus+      when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")+    context :: Expression -> Program -> PrintProgramContext -> DataizeContext+    context loc prog ctx = DataizeContext loc prog _maxDepth _maxCycles _depthSensitive buildTerm (saveStepFunc _stepsDir ctx)+    printProgCtx :: Expression -> PrintProgramContext+    printProgCtx focus =+      PrintProgCtx+        _sugarType+        _flat+        _margin+        defaultXmirContext+        _nonumber+        _compress+        _sequence+        (justMeetPopularity _meetPopularity)+        (justMeetLength _meetLength)+        focus+        _expression+        _label+        _meetPrefix+        _outputFormat++runExplain :: OptsExplain -> IO ()+runExplain OptsExplain{..} = do+  validateOpts+  rules <- getRules _normalize _shuffle _rules+  printOut _targetFile (explainRules rules)+  where+    validateOpts :: IO ()+    validateOpts = when (null _rules && not _normalize) (invalidCLIArguments "Either --rule or --normalize must be specified")++runMerge :: OptsMerge -> IO ()+runMerge OptsMerge{..} = do+  validateOpts+  inputs' <- traverse (readInput . Just) _inputs+  progs <- traverse (`parseProgram` _inputFormat) inputs'+  prog <- merge progs+  let listing = const (P.printProgram' prog (_sugarType, UNICODE, _flat, _margin))+      xmirCtx = XmirContext _omitListing _omitComments listing+      printCtx = printProgCtx xmirCtx+  prog' <- printProgram printCtx prog+  printOut _targetFile prog'+  where+    validateOpts :: IO ()+    validateOpts = do+      when (null _inputs) (throwIO (InvalidCLIArguments "At least one input file must be specified for 'merge' command"))+      validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] "Q"+    printProgCtx :: XmirContext -> PrintProgramContext+    printProgCtx xmirCtx =+      PrintProgCtx+        _sugarType+        _flat+        _margin+        xmirCtx+        False+        False+        False+        (justMeetPopularity Nothing)+        (justMeetLength Nothing)+        ExGlobal+        Nothing+        Nothing+        Nothing+        _outputFormat++runMatch :: OptsMatch -> IO ()+runMatch OptsMatch{..} = do+  input <- readInput _inputFile+  prog <- parseProgram input PHI+  if isNothing _pattern+    then logDebug "The --pattern is not provided, no substitutions are built"+    else do+      ptn <- parseExpressionThrows (fromJust _pattern)+      condition <- traverse parseConditionThrows _when+      substs <- matchProgramWithRule prog (rule ptn condition) (RuleContext buildTerm)+      if null substs+        then logDebug "Provided pattern was not matched, no substitutions are built"+        else putStrLn (P.printSubsts' substs (_sugarType, UNICODE, _flat, defaultMargin))+  where+    rule :: Expression -> Maybe Y.Condition -> Y.Rule+    rule ptn cnd = Y.Rule Nothing Nothing ptn ExGlobal cnd Nothing Nothing

@@ -0,0 +1,161 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DuplicateRecordFields #-}++-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++module CLI.Types where++import AST+import Control.Exception (Exception)+import Lining (LineFormat)+import Logger (LogLevel)+import Must (Must)+import Sugar (SugarType)+import Text.Printf (printf)+import XMIR (XmirContext)++data PrintProgramContext = PrintProgCtx+  { _sugar :: SugarType+  , _line :: LineFormat+  , _margin :: Int+  , _xmirCtx :: XmirContext+  , _nonumber :: Bool+  , _compress :: Bool+  , _sequence :: Bool+  , _meetPopularity :: Int+  , _meetLength :: Int+  , _focus :: Expression+  , _expression :: Maybe String+  , _label :: Maybe String+  , _meetPrefix :: Maybe String+  , _outputFormat :: IOFormat+  }++data CmdException+  = InvalidCLIArguments String+  | CouldNotReadFromStdin String+  | CouldNotDataize+  | CouldNotPrintExpressionInXMIR+  deriving (Exception)++instance Show CmdException where+  show (InvalidCLIArguments msg) = printf "Invalid set of arguments: %s" msg+  show (CouldNotReadFromStdin msg) = printf "Could not read input from stdin\nReason: %s" msg+  show CouldNotDataize = "Could not dataize given program"+  show CouldNotPrintExpressionInXMIR = "Could not print expression with --output=xmir, only program printing is allowed"++data Command+  = CmdRewrite OptsRewrite+  | CmdDataize OptsDataize+  | CmdExplain OptsExplain+  | CmdMerge OptsMerge+  | CmdMatch OptsMatch++data IOFormat = XMIR | PHI | LATEX+  deriving (Eq)++instance Show IOFormat where+  show XMIR = "xmir"+  show PHI = "phi"+  show LATEX = "latex"++data OptsDataize = OptsDataize+  { _logLevel :: LogLevel+  , _logLines :: Int+  , _inputFormat :: IOFormat+  , _outputFormat :: IOFormat+  , _sugarType :: SugarType+  , _flat :: LineFormat+  , _omitListing :: Bool+  , _omitComments :: Bool+  , _nonumber :: Bool+  , _sequence :: Bool+  , _canonize :: Bool+  , _depthSensitive :: Bool+  , _quiet :: Bool+  , _compress :: Bool+  , _maxDepth :: Int+  , _maxCycles :: Int+  , _margin :: Int+  , _meetPopularity :: Maybe Int+  , _meetLength :: Maybe Int+  , _hide :: [String]+  , _show :: [String]+  , _locator :: String+  , _focus :: String+  , _expression :: Maybe String+  , _label :: Maybe String+  , _meetPrefix :: Maybe String+  , _stepsDir :: Maybe FilePath+  , _inputFile :: Maybe FilePath+  }++data OptsExplain = OptsExplain+  { _logLevel :: LogLevel+  , _logLines :: Int+  , _rules :: [FilePath]+  , _normalize :: Bool+  , _shuffle :: Bool+  , _targetFile :: Maybe FilePath+  }++data OptsRewrite = OptsRewrite+  { _logLevel :: LogLevel+  , _logLines :: Int+  , _inputFormat :: IOFormat+  , _outputFormat :: IOFormat+  , _sugarType :: SugarType+  , _flat :: LineFormat+  , _must :: Must+  , _normalize :: Bool+  , _shuffle :: Bool+  , _omitListing :: Bool+  , _omitComments :: Bool+  , _depthSensitive :: Bool+  , _nonumber :: Bool+  , _inPlace :: Bool+  , _sequence :: Bool+  , _canonize :: Bool+  , _compress :: Bool+  , _maxDepth :: Int+  , _maxCycles :: Int+  , _margin :: Int+  , _meetPopularity :: Maybe Int+  , _meetLength :: Maybe Int+  , _rules :: [FilePath]+  , _hide :: [String]+  , _show :: [String]+  , _locator :: String+  , _focus :: String+  , _expression :: Maybe String+  , _label :: Maybe String+  , _meetPrefix :: Maybe String+  , _targetFile :: Maybe FilePath+  , _stepsDir :: Maybe FilePath+  , _inputFile :: Maybe FilePath+  }++data OptsMerge = OptsMerge+  { _logLevel :: LogLevel+  , _logLines :: Int+  , _inputFormat :: IOFormat+  , _outputFormat :: IOFormat+  , _sugarType :: SugarType+  , _flat :: LineFormat+  , _omitListing :: Bool+  , _omitComments :: Bool+  , _margin :: Int+  , _targetFile :: Maybe FilePath+  , _inputs :: [FilePath]+  }++data OptsMatch = OptsMatch+  { _logLevel :: LogLevel+  , _logLines :: Int+  , _sugarType :: SugarType+  , _flat :: LineFormat+  , _pattern :: Maybe String+  , _when :: Maybe String+  , _inputFile :: Maybe FilePath+  }

@@ -0,0 +1,61 @@+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++module CLI.Validators where++import AST+import CLI.Types+import Control.Exception+import Control.Monad (forM_, when, (>=>))+import Data.Foldable (for_)+import Data.Maybe (isJust)+import Must+import Parser (parseExpressionThrows)+import Printer+import Text.Printf (printf)++invalidCLIArguments :: String -> IO a+invalidCLIArguments msg = throwIO (InvalidCLIArguments msg)++-- Validate given expressions as valid dispatches+validatedDispatches :: String -> [String] -> IO [Expression]+validatedDispatches opt = traverse (parseExpressionThrows >=> asDispatch)+  where+    asDispatch :: Expression -> IO Expression+    asDispatch expr = asDispatch' expr+      where+        asDispatch' :: Expression -> IO Expression+        asDispatch' ex@ExGlobal = pure ex+        asDispatch' disp@(ExDispatch ex _) = asDispatch' ex >> pure disp+        asDispatch' _ =+          invalidCLIArguments+            ( printf+                "Only dispatch expression started with Φ (or Q) can be used in --%s, but given: %s"+                opt+                (printExpression' expr logPrintConfig)+            )++-- Validate LaTeX options+validateLatexOptions :: IOFormat -> [(Bool, String)] -> [(Maybe String, String)] -> [(Maybe Int, String)] -> IO ()+validateLatexOptions LATEX _ _ _ = pure ()+validateLatexOptions _ bools strings ints = do+  let (bools', opts) = unzip bools+      msg = "The --%s option can stay together with --output=latex only"+      callback (maybe', opt) = when (isJust maybe') (invalidCLIArguments (printf msg opt))+  validateBoolOpts (zip bools' (map (printf msg) opts))+  forM_ strings callback+  forM_ ints callback++-- Validate 'must' option+validateMust' :: Must -> IO ()+validateMust' must = for_ (validateMust must) invalidCLIArguments++-- Validate options for output to XMIR+validateXmirOptions :: IOFormat -> [(Bool, String)] -> String -> IO ()+validateXmirOptions XMIR _ focus = when (focus /= "Q") (invalidCLIArguments "Only --focus=Q is allowed to be used with --output=xmir")+validateXmirOptions _ bools _ =+  let (bools', opts) = unzip bools+   in validateBoolOpts (zip bools' (map (printf "The --%s can be used only with --output=xmir") opts))++validateBoolOpts :: [(Bool, String)] -> IO ()+validateBoolOpts bools = forM_ bools (\(bool, msg) -> when bool (invalidCLIArguments msg))

@@ -1,6 +1,7 @@ {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-partial-fields -Wno-name-shadowing #-}  -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com@@ -11,6 +12,7 @@ import AST import Data.Maybe (isJust) import Misc+import qualified Yaml as Y  data LCB = LCB | BIG_LCB   deriving (Eq, Show)@@ -48,7 +50,7 @@ data XI = XI | DOLLAR   deriving (Eq, Show) -data LAMBDA = LAMBDA+data LAMBDA = LAMBDA | LAMBDA'   deriving (Eq, Show)  data GLOBAL = Φ | Q@@ -63,6 +65,9 @@ data EOL = EOL | NO_EOL   deriving (Eq, Show) +data DOTS = DOTS | DOTS'+  deriving (Eq, Show)+ data BYTES   = BT_EMPTY   | BT_ONE String@@ -70,19 +75,26 @@   | BT_META META   deriving (Eq, Show) -data META-  = MT_EXPRESSION {rest :: String}-  | MT_EXPRESSION' {rest :: String}-  | MT_ATTRIBUTE {rest :: String}-  | MT_ATTRIBUTE' {rest :: String}-  | MT_BINDING {rest :: String}-  | MT_BINDING' {rest :: String}-  | MT_BYTES {rest :: String}-  | MT_BYTES' {rest :: String}-  | MT_TAIL {rest :: String}-  | MT_FUNCTION {rest :: String}+data META_HEAD+  = E -- 𝑒+  | E' -- e+  | A -- a+  | TAU -- 𝜏+  | TAU' -- \tau+  | B -- 𝐵+  | B' -- B+  | D -- δ+  | D' -- d+  | TAIL -- t+  | F -- F   deriving (Eq, Show) +data EXCLAMATION = EXCL | NO_EXCL+  deriving (Eq, Show)++data META = META {excl :: EXCLAMATION, hd :: META_HEAD, rest :: String}+  deriving (Eq, Show)+ data TAB   = TAB {indent :: Int}   | TAB'@@ -162,14 +174,92 @@   | AT_LAMBDA {lambda :: LAMBDA}   | AT_DELTA {delta :: DELTA}   | AT_META {meta :: META}+  | AT_REST {dots :: DOTS}   deriving (Eq, Show) +data BELONGING+  = IN+  | NOT_IN+  deriving (Eq, Show)++data SET+  = ST_BINDING {binding :: BINDING}+  | ST_ATTRIBUTES {attrs :: [ATTRIBUTE]}+  deriving (Eq, Show)++data LOGIC_OPERATOR+  = AND+  | OR+  deriving (Eq, Show)++data EQUAL+  = EQUAL+  | NOT_EQUAL+  deriving (Eq, Show)++data NUMBER+  = ORDINAL {attr :: ATTRIBUTE}+  | LENGTH {binding :: BINDING}+  | LITERAL {num :: Int}+  deriving (Eq, Show)++data COMPARABLE+  = CMP_ATTR {attr :: ATTRIBUTE}+  | CMP_EXPR {expr :: EXPRESSION}+  | CMP_NUM {num :: NUMBER}+  deriving (Eq, Show)++data CONDITION+  = CO_EMPTY+  | CO_BELONGS {attr :: ATTRIBUTE, belongs :: BELONGING, set :: SET}+  | CO_LOGIC {conditions :: [CONDITION], operator :: LOGIC_OPERATOR}+  | CO_NF {expr :: EXPRESSION}+  | CO_NOT {condition :: CONDITION}+  | CO_COMPARE {left :: COMPARABLE, equal :: EQUAL, right :: COMPARABLE}+  | CO_MATCHES {regex :: String, expr :: EXPRESSION}+  | CO_PART_OF {expr :: EXPRESSION, binding :: BINDING}+  deriving (Eq, Show)++data EXTRA_ARG+  = ARG_EXPR {expr :: EXPRESSION}+  | ARG_ATTR {attr :: ATTRIBUTE}+  | ARG_BINDING {binding :: BINDING}+  | ARG_BYTES {bytes :: BYTES}+  deriving (Eq, Show)++data EXTRA = EXTRA {meta :: EXTRA_ARG, func :: String, args :: [EXTRA_ARG]}+  deriving (Eq, Show)+ programToCST :: Program -> PROGRAM-programToCST prog = toCST prog (0, EOL)+programToCST = toCST'  expressionToCST :: Expression -> EXPRESSION-expressionToCST ex = toCST ex (0, EOL)+expressionToCST = toCST' +attributeToCST :: Attribute -> ATTRIBUTE+attributeToCST = toCST'++bindingsToCST :: [Binding] -> BINDING+bindingsToCST = toCST'++conditionToCST :: Y.Condition -> CONDITION+conditionToCST = toCST'++comparableToCST :: Y.Comparable -> COMPARABLE+comparableToCST = toCST'++numberToCST :: Y.Number -> NUMBER+numberToCST = toCST'++extraToCST :: Y.Extra -> EXTRA+extraToCST = toCST'++toCST' :: ToCST a b => a -> b+toCST' = (`toCST` (0, EOL))++metaTail :: String -> String+metaTail = tail+ -- This class is used to convert AST to CST -- CST is created with sugar and unicode -- All further transformations must consider that@@ -182,8 +272,8 @@ instance ToCST Expression EXPRESSION where   toCST ExGlobal _ = EX_GLOBAL Φ   toCST ExThis _ = EX_XI XI-  toCST (ExMeta mt) _ = EX_META (MT_EXPRESSION (tail mt))-  toCST (ExMetaTail expr mt) ctx = EX_META_TAIL (toCST expr ctx) (MT_TAIL (tail mt))+  toCST (ExMeta mt) _ = EX_META (META NO_EXCL E (metaTail mt))+  toCST (ExMetaTail expr mt) ctx = EX_META_TAIL (toCST expr ctx) (META EXCL TAIL (metaTail mt))   toCST ExTermination _ = EX_TERMINATION DEAD   toCST (ExPhiMeet prefix idx expr) ctx = EX_PHI_MEET prefix idx (toCST expr ctx)   toCST (ExPhiAgain prefix idx expr) ctx = EX_PHI_AGAIN prefix idx (toCST expr ctx)@@ -304,12 +394,12 @@  instance ToCST [Binding] BINDING where   toCST [] (tabs, _) = BI_EMPTY (TAB tabs)-  toCST (BiMeta mt : bds) ctx@(tabs, _) = BI_META (MT_BINDING (tail mt)) (toCST bds ctx) (TAB tabs)+  toCST (BiMeta mt : bds) ctx@(tabs, _) = BI_META (META NO_EXCL B (metaTail mt)) (toCST bds ctx) (TAB tabs)   toCST (bd : bds) ctx@(tabs, _) = BI_PAIR (toCST bd ctx) (toCST bds ctx) (TAB tabs)  instance ToCST [Binding] BINDINGS where   toCST [] (tabs, _) = BDS_EMPTY (TAB tabs)-  toCST (BiMeta mt : bds) ctx@(tabs, eol) = BDS_META eol (TAB tabs) (MT_BINDING (tail mt)) (toCST bds ctx)+  toCST (BiMeta mt : bds) ctx@(tabs, eol) = BDS_META eol (TAB tabs) (META NO_EXCL B (metaTail mt)) (toCST bds ctx)   toCST (bd : bds) ctx@(tabs, eol) = BDS_PAIR eol (TAB tabs) (toCST bd ctx) (toCST bds ctx)  instance ToCST Binding PAIR where@@ -335,7 +425,7 @@   toCST (BiVoid attr) ctx = PA_VOID (toCST attr ctx) ARROW EMPTY   toCST (BiDelta bts) ctx = PA_DELTA (toCST bts ctx)   toCST (BiLambda func) _ = PA_LAMBDA func-  toCST (BiMetaLambda mt) _ = PA_META_LAMBDA (MT_FUNCTION (tail mt))+  toCST (BiMetaLambda mt) _ = PA_META_LAMBDA (META EXCL F (metaTail mt))   toCST (BiMeta mt) _ = error $ "BiMeta binding " ++ mt ++ " cannot be converted to PAIR"  instance ToCST Binding APP_BINDING where@@ -346,7 +436,7 @@   toCST BtEmpty _ = BT_EMPTY   toCST (BtOne byte) _ = BT_ONE byte   toCST (BtMany bts) _ = BT_MANY bts-  toCST (BtMeta mt) _ = BT_META (MT_BYTES (tail mt))+  toCST (BtMeta mt) _ = BT_META (META NO_EXCL D (metaTail mt))  instance ToCST Attribute ATTRIBUTE where   toCST (AtLabel label) _ = AT_LABEL label@@ -355,4 +445,52 @@   toCST AtRho _ = AT_RHO RHO   toCST AtDelta _ = AT_DELTA DELTA   toCST AtLambda _ = AT_LAMBDA LAMBDA-  toCST (AtMeta mt) _ = AT_META (MT_ATTRIBUTE (tail mt))+  toCST (AtMeta mt) _ = AT_META (META NO_EXCL TAU (metaTail mt))++withoutXi :: [Y.Condition] -> [Y.Condition]+withoutXi conds = [cond | cond <- conds, not (singleXi cond)]+  where+    singleXi :: Y.Condition -> Bool+    singleXi (Y.Xi _) = True+    singleXi (Y.Not (Y.Xi _)) = True+    singleXi (Y.And [cond]) = singleXi cond+    singleXi (Y.Or [cond]) = singleXi cond+    singleXi _ = False++instance ToCST Y.Condition CONDITION where+  toCST (Y.Not (Y.In attr binding)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_BINDING (bindingsToCST [binding]))+  toCST (Y.Not (Y.Eq left right)) _ = CO_COMPARE (comparableToCST left) NOT_EQUAL (comparableToCST right)+  toCST (Y.Not (Y.Alpha attr)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_ATTRIBUTES [attributeToCST (AtAlpha 0), attributeToCST (AtAlpha 1), AT_REST DOTS])+  toCST (Y.In attr binding) _ = CO_BELONGS (attributeToCST attr) IN (ST_BINDING (bindingsToCST [binding]))+  toCST (Y.And conds) _ = case withoutXi conds of+    [] -> CO_EMPTY+    conds' -> CO_LOGIC (map toCST' (withoutXi conds')) AND+  toCST (Y.Or conds) _ = case withoutXi conds of+    [] -> CO_EMPTY+    conds' -> CO_LOGIC (map toCST' (withoutXi conds')) OR+  toCST (Y.Alpha attr) _ = CO_BELONGS (attributeToCST attr) IN (ST_ATTRIBUTES [attributeToCST (AtAlpha 0), attributeToCST (AtAlpha 1), AT_REST DOTS])+  toCST (Y.NF expr) _ = CO_NF (expressionToCST expr)+  toCST (Y.Not cond) _ = CO_NOT (conditionToCST cond)+  toCST (Y.Eq left right) _ = CO_COMPARE (comparableToCST left) EQUAL (comparableToCST right)+  toCST (Y.Matches regex expr) _ = CO_MATCHES regex (expressionToCST expr)+  toCST (Y.PartOf expr binding) _ = CO_PART_OF (expressionToCST expr) (bindingsToCST [binding])+  toCST (Y.Xi _) _ = CO_EMPTY++instance ToCST Y.Comparable COMPARABLE where+  toCST (Y.CmpAttr attr) _ = CMP_ATTR (attributeToCST attr)+  toCST (Y.CmpExpr expr) _ = CMP_EXPR (expressionToCST expr)+  toCST (Y.CmpNum num) _ = CMP_NUM (numberToCST num)++instance ToCST Y.Number NUMBER where+  toCST (Y.Ordinal attr) _ = ORDINAL (attributeToCST attr)+  toCST (Y.Length binding) _ = LENGTH (bindingsToCST [binding])+  toCST (Y.Literal num) _ = LITERAL num++instance ToCST Y.ExtraArgument EXTRA_ARG where+  toCST (Y.ArgAttribute attr) _ = ARG_ATTR (attributeToCST attr)+  toCST (Y.ArgExpression expr) _ = ARG_EXPR (expressionToCST expr)+  toCST (Y.ArgBinding binding) _ = ARG_BINDING (bindingsToCST [binding])+  toCST (Y.ArgBytes bytes) _ = ARG_BYTES (toCST' bytes)++instance ToCST Y.Extra EXTRA where+  toCST Y.Extra{..} _ = EXTRA (toCST' meta) function (map toCST' args)

@@ -124,7 +124,7 @@         _ <- symbol "xi" >> lparen         expr <- _expression phiParser         _ <- rparen-        return (Y.XI expr)+        return (Y.Xi expr)     , do         _ <- symbol "matches" >> lparen         ptn <- _string phiParser

@@ -154,7 +154,7 @@         then morph (ExTermination, seq) ctx -- PRIM         else do           prog' <- withLocatedExpression _locator expr _program-          rewrittens' <- rewrite prog' normalizationRules (switchContext ctx) -- NMZ todo+          (rewrittens', _) <- rewrite prog' normalizationRules (switchContext ctx) -- NMZ todo           let seq' = reverse rewrittens' <> tail seq           expr' <- locatedExpression _locator (fst (head seq'))           morph (expr', seq') ctx

@@ -31,8 +31,8 @@   toASCII EX_APPLICATION{..} = EX_APPLICATION (toASCII expr) eol tab (toASCII tau) eol' tab' indent   toASCII EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toASCII expr) eol tab (toASCII taus) eol' tab' indent   toASCII EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toASCII expr) eol tab (toASCII args) eol' tab' indent-  toASCII EX_META{..} = EX_META (MT_EXPRESSION' (rest meta))-  toASCII EX_META_TAIL{..} = EX_META_TAIL (toASCII expr) (MT_TAIL (rest meta))+  toASCII EX_META{..} = EX_META (META EXCL E' (rest meta))+  toASCII EX_META_TAIL{..} = EX_META_TAIL (toASCII expr) meta   toASCII EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toASCII expr)   toASCII EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toASCII expr)   toASCII expr = expr@@ -42,12 +42,12 @@  instance ToASCII BINDING where   toASCII BI_PAIR{..} = BI_PAIR (toASCII pair) (toASCII bindings) tab-  toASCII BI_META{..} = BI_META (MT_BINDING' (rest meta)) (toASCII bindings) tab+  toASCII BI_META{meta = META{..}, ..} = BI_META (META EXCL B' rest) (toASCII bindings) tab   toASCII bd = bd  instance ToASCII BINDINGS where   toASCII BDS_PAIR{..} = BDS_PAIR eol tab (toASCII pair) (toASCII bindings)-  toASCII BDS_META{..} = BDS_META eol tab (MT_BINDING' (rest meta)) (toASCII bindings)+  toASCII BDS_META{..} = BDS_META eol tab (META EXCL B' (rest meta)) (toASCII bindings)   toASCII bds = bds  instance ToASCII APP_ARG where@@ -64,12 +64,45 @@   toASCII PA_LAMBDA{..} = PA_LAMBDA' func   toASCII PA_DELTA{..} = PA_DELTA' bytes   toASCII PA_META_LAMBDA{..} = PA_META_LAMBDA' meta-  toASCII PA_META_DELTA{..} = PA_META_DELTA' (MT_BYTES' (rest meta))+  toASCII PA_META_DELTA{..} = PA_META_DELTA' (META EXCL D' (rest meta))   toASCII pair = pair  instance ToASCII ATTRIBUTE where   toASCII AT_ALPHA{..} = AT_ALPHA ALPHA' idx   toASCII AT_PHI{} = AT_PHI AT   toASCII AT_RHO{} = AT_RHO CARET-  toASCII AT_META{..} = AT_META (MT_ATTRIBUTE' (rest meta))+  toASCII AT_META{..} = AT_META (META EXCL A (rest meta))   toASCII attr = attr++instance ToASCII SET where+  toASCII ST_BINDING{..} = ST_BINDING (toASCII binding)+  toASCII ST_ATTRIBUTES{..} = ST_ATTRIBUTES (map toASCII attrs)++instance ToASCII NUMBER where+  toASCII ORDINAL{..} = ORDINAL (toASCII attr)+  toASCII LENGTH{..} = LENGTH (toASCII binding)+  toASCII literal@LITERAL{} = literal++instance ToASCII COMPARABLE where+  toASCII CMP_ATTR{..} = CMP_ATTR (toASCII attr)+  toASCII CMP_EXPR{..} = CMP_EXPR (toASCII expr)+  toASCII CMP_NUM{..} = CMP_NUM (toASCII num)++instance ToASCII CONDITION where+  toASCII CO_BELONGS{..} = CO_BELONGS (toASCII attr) belongs (toASCII set)+  toASCII CO_LOGIC{..} = CO_LOGIC (map toASCII conditions) operator+  toASCII CO_NF{..} = CO_NF (toASCII expr)+  toASCII CO_NOT{..} = CO_NOT (toASCII condition)+  toASCII CO_COMPARE{..} = CO_COMPARE (toASCII left) equal (toASCII right)+  toASCII CO_MATCHES{..} = CO_MATCHES regex (toASCII expr)+  toASCII CO_PART_OF{..} = CO_PART_OF (toASCII expr) (toASCII binding)+  toASCII CO_EMPTY = CO_EMPTY++instance ToASCII EXTRA_ARG where+  toASCII ARG_ATTR{..} = ARG_ATTR (toASCII attr)+  toASCII ARG_EXPR{..} = ARG_EXPR (toASCII expr)+  toASCII ARG_BINDING{..} = ARG_BINDING (toASCII binding)+  toASCII bts@ARG_BYTES{} = bts++instance ToASCII EXTRA where+  toASCII EXTRA{..} = EXTRA (toASCII meta) func (map toASCII args)

@@ -23,15 +23,15 @@ import CST import Data.List (intercalate, nub) import Data.Maybe (fromMaybe)-import Encoding (Encoding (ASCII), ToASCII, withEncoding)-import Lining (LineFormat (MULTILINE), ToSingleLine, withLineFormat)+import Encoding+import Lining import Locator (locatedExpression) import Margin (WithMargin, defaultMargin, withMargin) import Matcher import Misc import Render (Render (render)) import Replacer (replaceProgram)-import Rewriter (Rewritten)+import Rewriter (Rewritten, Rewrittens) import Sugar (SugarType (SWEET), ToSalty, withSugarType) import Text.Printf (printf) import qualified Yaml as Y@@ -51,7 +51,7 @@   }  defaultLatexContext :: LatexContext-defaultLatexContext = LatexContext SWEET MULTILINE defaultMargin False False defaultMeetPopularity defaultMeetLength ExGlobal Nothing Nothing Nothing+defaultLatexContext = LatexContext SWEET SINGLELINE defaultMargin False False defaultMeetPopularity defaultMeetLength ExGlobal Nothing Nothing Nothing  defaultMeetPopularity :: Int defaultMeetPopularity = 50@@ -149,31 +149,32 @@         printed     ) -ending :: LatexContext -> String-ending ctx = printf "{.}\n\\end{%s}" (phiquation ctx)+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)  compressedRewrittens :: [Rewritten] -> LatexContext -> [Rewritten] compressedRewrittens rewrittens ctx@LatexContext{..} =   let (progs, rules) = unzip rewrittens    in if _compress then zip (meetInPrograms progs ctx) rules else rewrittens -rewrittensToLatex :: [Rewritten] -> LatexContext -> IO String-rewrittensToLatex rewrittens ctx@LatexContext{_focus = ExGlobal} =+rewrittensToLatex :: Rewrittens -> LatexContext -> IO String+rewrittensToLatex (rewrittens, exceeded) ctx@LatexContext{_focus = ExGlobal} =   pure     ( concat         [ preamble ctx         , body (compressedRewrittens rewrittens ctx) (\prog -> renderToLatex (programToCST prog) ctx)-        , ending ctx+        , ending exceeded ctx         ]     )-rewrittensToLatex rewrittens ctx@LatexContext{..} = do+rewrittensToLatex (rewrittens, exceeded) ctx@LatexContext{..} = do   let (progs, rules) = unzip (compressedRewrittens rewrittens ctx)   exprs <- mapM (locatedExpression _focus) progs   pure     ( concat         [ preamble ctx         , body (zip exprs rules) (\expr -> renderToLatex (expressionToCST expr) ctx)-        , ending ctx+        , ending exceeded ctx         ]     ) @@ -182,7 +183,7 @@   concat     [ preamble ctx     , renderToLatex (programToCST prog) ctx-    , ending ctx+    , ending False ctx     ]  expressionToLaTeX :: Expression -> LatexContext -> String@@ -190,7 +191,7 @@   concat     [ preamble ctx     , renderToLatex (expressionToCST ex) ctx-    , ending ctx+    , ending False ctx     ]  piped :: String -> String@@ -212,10 +213,14 @@   toLaTeX EX_DISPATCH{..} = EX_DISPATCH (toLaTeX expr) (toLaTeX attr)   toLaTeX EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toLaTeX expr)   toLaTeX EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toLaTeX expr)+  toLaTeX EX_META{..} = EX_META (META NO_EXCL E' (rest meta))   toLaTeX expr = expr  instance ToLaTeX ATTRIBUTE where   toLaTeX AT_LABEL{..} = AT_LABEL (piped (toLaTeX label))+  toLaTeX AT_META{..} = AT_META (META NO_EXCL TAU' (rest meta))+  toLaTeX AT_LAMBDA{} = AT_LAMBDA LAMBDA'+  toLaTeX AT_REST{} = AT_REST DOTS'   toLaTeX attr = attr  instance ToLaTeX APP_BINDING where@@ -223,10 +228,12 @@  instance ToLaTeX BINDING where   toLaTeX BI_PAIR{..} = BI_PAIR (toLaTeX pair) (toLaTeX bindings) tab+  toLaTeX BI_META{..} = BI_META (META NO_EXCL B' (rest meta)) (toLaTeX bindings) tab   toLaTeX bd = bd  instance ToLaTeX BINDINGS where   toLaTeX BDS_PAIR{..} = BDS_PAIR eol tab (toLaTeX pair) (toLaTeX bindings)+  toLaTeX BDS_META{..} = BDS_META eol tab (META NO_EXCL B' (rest meta)) (toLaTeX bindings)   toLaTeX bds = bds  instance ToLaTeX PAIR where@@ -236,6 +243,10 @@   toLaTeX PA_VOID{..} = PA_VOID (toLaTeX attr) arrow void   toLaTeX PA_TAU{..} = PA_TAU (toLaTeX attr) arrow (toLaTeX expr)   toLaTeX PA_FORMATION{..} = PA_FORMATION (toLaTeX attr) (map toLaTeX voids) arrow (toLaTeX expr)+  toLaTeX PA_META_DELTA{..} = toLaTeX (PA_META_DELTA' meta)+  toLaTeX PA_META_DELTA'{..} = PA_META_DELTA' (META NO_EXCL D' (rest meta))+  toLaTeX PA_META_LAMBDA{..} = toLaTeX (PA_META_LAMBDA' meta)+  toLaTeX PA_META_LAMBDA'{..} = PA_META_LAMBDA' (META NO_EXCL F (rest meta))   toLaTeX pair = pair  instance ToLaTeX APP_ARG where@@ -257,24 +268,74 @@         '_' -> "\\char95{}" <> escapeUnprintedChars rest         _ -> ch : escapeUnprintedChars rest --- @todo #114:30min Implement LaTeX conversion for rules.---  Convert Rule data structure to LaTeX inference rule format.---  Each rule should be formatted as a LaTeX inference rule with---  pattern, result, and optional conditions.---  Tests must be added for LaTeX conversion logic.+instance ToLaTeX SET where+  toLaTeX ST_BINDING{..} = ST_BINDING (toLaTeX binding)+  toLaTeX ST_ATTRIBUTES{..} = ST_ATTRIBUTES (map toLaTeX attrs)++instance ToLaTeX NUMBER where+  toLaTeX ORDINAL{..} = ORDINAL (toLaTeX attr)+  toLaTeX LENGTH{..} = LENGTH (toLaTeX binding)+  toLaTeX literal@LITERAL{} = literal++instance ToLaTeX COMPARABLE where+  toLaTeX CMP_EXPR{..} = CMP_EXPR (toLaTeX expr)+  toLaTeX CMP_ATTR{..} = CMP_ATTR (toLaTeX attr)+  toLaTeX CMP_NUM{..} = CMP_NUM (toLaTeX num)++instance ToLaTeX CONDITION where+  toLaTeX CO_BELONGS{..} = CO_BELONGS (toLaTeX attr) belongs (toLaTeX set)+  toLaTeX CO_LOGIC{..} = CO_LOGIC (map toLaTeX conditions) operator+  toLaTeX CO_NF{..} = CO_NF (toLaTeX expr)+  toLaTeX CO_NOT{..} = CO_NOT (toLaTeX condition)+  toLaTeX CO_COMPARE{..} = CO_COMPARE (toLaTeX left) equal (toLaTeX right)+  toLaTeX CO_MATCHES{..} = CO_MATCHES regex (toLaTeX expr)+  toLaTeX CO_PART_OF{..} = CO_PART_OF (toLaTeX expr) (toLaTeX binding)+  toLaTeX CO_EMPTY = CO_EMPTY++instance ToLaTeX EXTRA_ARG where+  toLaTeX ARG_ATTR{..} = ARG_ATTR (toLaTeX attr)+  toLaTeX ARG_EXPR{..} = ARG_EXPR (toLaTeX expr)+  toLaTeX ARG_BINDING{..} = ARG_BINDING (toLaTeX binding)+  toLaTeX bts@ARG_BYTES{} = bts++instance ToLaTeX EXTRA where+  toLaTeX EXTRA{..} = EXTRA (toLaTeX meta) func (map toLaTeX args)+ explainRule :: Y.Rule -> String-explainRule rule = "\\rule{" ++ fromMaybe "unnamed" (Y.name rule) ++ "}"+explainRule rule =+  intercalate+    "\n  "+    [ "\\trrule{" ++ fromMaybe "unknown" (Y.name rule) ++ "}"+    , braced (renderToLatex (expressionToCST (Y.pattern rule)) defaultLatexContext)+    , braced (renderToLatex (expressionToCST (Y.result rule)) defaultLatexContext)+    , conditionToLatex (joinedConditions (Y.when rule) (Y.having rule))+    , extraArgumentsToLatex (Y.where_ rule)+    ]+  where+    conditionToLatex :: Maybe Y.Condition -> String+    conditionToLatex Nothing = "{ }"+    conditionToLatex (Just cond) = case conditionToCST cond of+      CO_EMPTY -> "{ }"+      cond' -> braced ("if " <> renderToLatex cond' defaultLatexContext)+    extraArgumentsToLatex :: Maybe [Y.Extra] -> String+    extraArgumentsToLatex Nothing = "{ }"+    extraArgumentsToLatex (Just extras) =+      let extras' = map ((`renderToLatex` defaultLatexContext) . extraToCST) extras+       in braced ("where " <> intercalate "; " extras')+    braced :: String -> String+    braced = printf "{ %s }"+    -- Join two maybe conditions into single one using Y.And if at least one is just.+    joinedConditions :: Maybe Y.Condition -> Maybe Y.Condition -> Maybe Y.Condition+    joinedConditions Nothing Nothing = Nothing+    joinedConditions first@(Just _) Nothing = first+    joinedConditions Nothing second@(Just _) = second+    joinedConditions (Just first) (Just second) = Just (Y.And [first, second]) --- @todo #114:30min Create LaTeX document wrapper.---  Generate proper LaTeX document with tabular format for rules.---  Each rule should be   in its own tabular environment.---  Include tests for document structure generation. explainRules :: [Y.Rule] -> String-explainRules rules' =-  unlines-    [ "\\documentclass{article}"-    , "\\usepackage{amsmath}"-    , "\\begin{document}"+explainRules rules =+  intercalate+    "\n"+    [ "\\begin{tabular}{rl}"+    , intercalate "\n" (map explainRule rules)+    , "\\end{tabular}"     ]-    ++ unlines (map explainRule rules')-    ++ "\\end{document}"

@@ -57,3 +57,35 @@ instance ToSingleLine APP_ARGS where   toSingleLine AAS_EXPR{..} = AAS_EXPR NO_EOL TAB' (toSingleLine expr) (toSingleLine args)   toSingleLine args = args++instance ToSingleLine SET where+  toSingleLine ST_BINDING{..} = ST_BINDING (toSingleLine binding)+  toSingleLine st = st++instance ToSingleLine NUMBER where+  toSingleLine LENGTH{..} = LENGTH (toSingleLine binding)+  toSingleLine num = num++instance ToSingleLine COMPARABLE where+  toSingleLine comp@CMP_ATTR{} = comp+  toSingleLine CMP_EXPR{..} = CMP_EXPR (toSingleLine expr)+  toSingleLine CMP_NUM{..} = CMP_NUM (toSingleLine num)++instance ToSingleLine CONDITION where+  toSingleLine CO_BELONGS{..} = CO_BELONGS attr belongs (toSingleLine set)+  toSingleLine CO_LOGIC{..} = CO_LOGIC (map toSingleLine conditions) operator+  toSingleLine CO_NF{..} = CO_NF (toSingleLine expr)+  toSingleLine CO_NOT{..} = CO_NOT (toSingleLine condition)+  toSingleLine CO_COMPARE{..} = CO_COMPARE (toSingleLine left) equal (toSingleLine right)+  toSingleLine CO_MATCHES{..} = CO_MATCHES regex (toSingleLine expr)+  toSingleLine CO_PART_OF{..} = CO_PART_OF (toSingleLine expr) (toSingleLine binding)+  toSingleLine CO_EMPTY = CO_EMPTY++instance ToSingleLine EXTRA_ARG where+  toSingleLine ARG_EXPR{..} = ARG_EXPR (toSingleLine expr)+  toSingleLine ARG_BINDING{..} = ARG_BINDING (toSingleLine binding)+  toSingleLine at@ARG_ATTR{} = at+  toSingleLine bts@ARG_BYTES{} = bts++instance ToSingleLine EXTRA where+  toSingleLine EXTRA{..} = EXTRA (toSingleLine meta) func (map toSingleLine args)

@@ -111,5 +111,11 @@      in if lengthOf single + extra <= margin then single else pa'   withMargin' _ pa = pa +instance WithMargin CONDITION where+  withMargin' _ co = co++instance WithMargin EXTRA where+  withMargin' _ = id+ lengthOf :: Render a => a -> Int lengthOf renderable = length (render renderable)

@@ -9,6 +9,7 @@  import CST import Data.List (intercalate)+import Text.Printf (printf)  class Render a where   render :: a -> String@@ -76,6 +77,7 @@  instance Render LAMBDA where   render LAMBDA = "λ"+  render LAMBDA' = "\\lambda"  instance Render GLOBAL where   render Φ = "Φ"@@ -92,23 +94,35 @@   render EOL = "\n"   render NO_EOL = "" +instance Render DOTS where+  render DOTS = "..."+  render DOTS' = "\\dots"+ instance Render BYTES where   render BT_EMPTY = "--"   render (BT_ONE bte) = render bte <> "-"   render (BT_MANY bts) = intercalate "-" bts   render (BT_META mt) = render mt +instance Render EXCLAMATION where+  render EXCL = "!"+  render NO_EXCL = ""++instance Render META_HEAD where+  render E = "𝑒"+  render E' = "e"+  render A = "a"+  render TAU = "𝜏"+  render TAU' = "\\tau"+  render B = "𝐵"+  render B' = "B"+  render D = "δ"+  render D' = "d"+  render TAIL = "t"+  render F = "F"+ instance Render META where-  render MT_EXPRESSION{..} = '𝑒' : rest-  render MT_EXPRESSION'{..} = "!e" <> rest-  render MT_ATTRIBUTE{..} = '𝜏' : rest-  render MT_ATTRIBUTE'{..} = "!a" <> rest-  render MT_BINDING{..} = '𝐵' : rest-  render MT_BINDING'{..} = "!B" <> rest-  render MT_BYTES{..} = 'δ' : rest-  render MT_BYTES'{..} = "!d" <> rest-  render MT_TAIL{..} = "!t" <> rest-  render MT_FUNCTION{..} = "!F" <> rest+  render META{..} = render excl <> render hd <> render rest  instance Render ALPHA where   render ALPHA = "α"@@ -185,3 +199,53 @@   render AT_LAMBDA{..} = render lambda   render AT_DELTA{..} = render delta   render AT_META{..} = render meta+  render AT_REST{..} = render dots++instance Render BELONGING where+  render IN = "\\in"+  render NOT_IN = "\\notin"++instance Render SET where+  render ST_BINDING{..} = render binding+  render ST_ATTRIBUTES{..} = printf "[ %s ]" (intercalate ", " (map render attrs))++instance Render LOGIC_OPERATOR where+  render AND = "and"+  render OR = "or"++instance Render NUMBER where+  render ORDINAL{..} = renderFunc "ordinal" attr+  render LENGTH{..} = renderFunc "length" binding+  render LITERAL{..} = show num++instance Render COMPARABLE where+  render CMP_ATTR{..} = render attr+  render CMP_EXPR{..} = render expr+  render CMP_NUM{..} = render num++instance Render EQUAL where+  render EQUAL = "="+  render NOT_EQUAL = "\\not="++instance Render CONDITION where+  render CO_BELONGS{..} = render attr <> render SPACE <> render belongs <> render SPACE <> render set+  render CO_LOGIC{conditions = [cond]} = render cond+  render CO_LOGIC{..} = printf "\\( %s \\)" (intercalate (printf " \\) %s \\( " (render operator)) (map render conditions))+  render CO_NF{..} = renderFunc "NF" expr+  render CO_NOT{..} = renderFunc "not" condition+  render CO_COMPARE{..} = render left <> render SPACE <> render equal <> render SPACE <> render right+  render CO_MATCHES{..} = printf "matches( %s, %s )" regex (render expr)+  render CO_PART_OF{..} = printf "part-of( %s, %s )" (render expr) (render binding)+  render CO_EMPTY = ""++renderFunc :: Render a => String -> a -> String+renderFunc func renderable = printf "%s( %s )" func (render renderable)++instance Render EXTRA_ARG where+  render ARG_ATTR{..} = render attr+  render ARG_EXPR{..} = render expr+  render ARG_BINDING{..} = render binding+  render ARG_BYTES{..} = render bytes++instance Render EXTRA where+  render EXTRA{..} = render meta <> " <- " <> printf "%s( %s )" func (intercalate ", " (map render args))

@@ -8,13 +8,12 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Rewriter (rewrite, RewriteContext (..), Rewritten) where+module Rewriter (rewrite, RewriteContext (..), Rewritten, Rewrittens) where  import AST import Builder import Control.Exception (Exception, throwIO) import Data.Char (toLower)-import Data.Functor ((<&>)) import Data.Maybe (fromMaybe) import qualified Data.Set as Set import Deps@@ -33,6 +32,8 @@  type Rewritten = (Program, Maybe String) +type Rewrittens = ([Rewritten], Bool)+ type ToReplace = (Expression, Expression, Expression, [Subst])  data RewriteContext = RewriteContext@@ -183,17 +184,19 @@           [] -> [(_prog, Nothing)]  -- Rewrite program by provided locator from RewriteContext-rewrite :: Program -> [Y.Rule] -> RewriteContext -> IO [Rewritten]-rewrite prog rules ctx@RewriteContext{..} = _rewrite ([(prog, Nothing)], Set.empty) 0 <&> reverse+rewrite :: Program -> [Y.Rule] -> RewriteContext -> IO Rewrittens+rewrite prog rules ctx@RewriteContext{..} = do+  (rewrittens, exceeded) <- _rewrite ([(prog, Nothing)], Set.empty) 0+  pure (reverse rewrittens, exceeded)   where-    _rewrite :: RewriteState -> Int -> IO [Rewritten]+    _rewrite :: RewriteState -> Int -> IO Rewrittens     _rewrite state@(rewrittens, _) count       | not (inRange _must count) && count > 0 && exceedsUpperBound _must count = throwIO (MustStopBefore _must count)       | count == _maxCycles = do           logDebug (printf "Max amount of rewriting cycles for all rules (%d) has been reached, rewriting is stopped" _maxCycles)           if _depthSensitive             then throwIO (StoppedOnLimit "max-cycles" _maxCycles)-            else pure rewrittens+            else pure (rewrittens, True)       | otherwise = do           logDebug (printf "Starting rewriting cycle for all rules: %d out of %d" count _maxCycles)           state'@(rewrittens', _) <- rewrite' state rules count ctx@@ -204,5 +207,5 @@               logDebug "Rewriting is stopped since it has no effect"               if not (inRange _must count)                 then throwIO (MustBeGoing _must count)-                else pure rewrittens'+                else pure (rewrittens', False)             else _rewrite state' (count + 1)

@@ -208,7 +208,7 @@ meetCondition' (Y.Alpha attr) = _alpha attr meetCondition' (Y.Eq left right) = _eq left right meetCondition' (Y.NF expr) = _nf expr-meetCondition' (Y.XI expr) = _xi expr+meetCondition' (Y.Xi expr) = _xi expr meetCondition' (Y.Matches pat expr) = _matches pat expr meetCondition' (Y.PartOf expr bd) = _partOf expr bd 

@@ -166,3 +166,35 @@       joinToBindings [] BI_META{} = error "BI_META unexpected in joinToBindings"       joinToBindings (attr : rest) bd = BDS_PAIR eol tab (PA_VOID attr arrow EMPTY) (joinToBindings rest bd)   toSalty pair = pair++instance ToSalty SET where+  toSalty ST_BINDING{..} = ST_BINDING (toSalty binding)+  toSalty st = st++instance ToSalty NUMBER where+  toSalty LENGTH{..} = LENGTH (toSalty binding)+  toSalty num = num++instance ToSalty COMPARABLE where+  toSalty comp@CMP_ATTR{} = comp+  toSalty CMP_EXPR{..} = CMP_EXPR (toSalty expr)+  toSalty CMP_NUM{..} = CMP_NUM (toSalty num)++instance ToSalty CONDITION where+  toSalty CO_BELONGS{..} = CO_BELONGS attr belongs (toSalty set)+  toSalty CO_LOGIC{..} = CO_LOGIC (map toSalty conditions) operator+  toSalty CO_NF{..} = CO_NF (toSalty expr)+  toSalty CO_NOT{..} = CO_NOT (toSalty condition)+  toSalty CO_COMPARE{..} = CO_COMPARE (toSalty left) equal (toSalty right)+  toSalty CO_MATCHES{..} = CO_MATCHES regex (toSalty expr)+  toSalty CO_PART_OF{..} = CO_PART_OF (toSalty expr) (toSalty binding)+  toSalty CO_EMPTY = CO_EMPTY++instance ToSalty EXTRA_ARG where+  toSalty ARG_EXPR{..} = ARG_EXPR (toSalty expr)+  toSalty ARG_BINDING{..} = ARG_BINDING (toSalty binding)+  toSalty at@ARG_ATTR{} = at+  toSalty bts@ARG_BYTES{} = bts++instance ToSalty EXTRA where+  toSalty EXTRA{..} = EXTRA (toSalty meta) func (map toSalty args)

@@ -83,7 +83,7 @@             , Not <$> v .: "not"             , Alpha <$> v .: "alpha"             , NF <$> v .: "nf"-            , XI <$> v .: "xi"+            , Xi <$> v .: "xi"             , do                 vals <- v .: "eq"                 case vals of@@ -151,7 +151,7 @@   | Alpha Attribute   | Eq Comparable Comparable   | NF Expression-  | XI Expression+  | Xi Expression   | Matches String Expression   | PartOf Expression Binding   deriving (Eq, Generic, Show)

@@ -559,6 +559,19 @@               ]           ] +    it "shows exceeding of limits in latex" $+      withStdin "{[[ x -> $.y, y -> $.x ]].x}" $+        testCLISucceeded+          ["rewrite", "--normalize", "--flat", "--sequence", "--output=latex", "--sweet", "--max-depth=1", "--max-cycles=1"]+          [ unlines+              [ "\\begin{phiquation}"+              , "\\Big\\{[[ |x| -> |y|, |y| -> |x| ]].|x|\\Big\\} \\leadsto_{\\nameref{r:dot}}"+              , "  \\leadsto \\Big\\{[[ |x| -> |y|, |y| -> |x| ]].|y|( ^ -> [[ |x| -> |y|, |y| -> |x| ]] )\\Big\\} \\leadsto"+              , "  \\leadsto \\dots"+              , "\\end{phiquation}"+              ]+          ]+     it "focuses expression in phi without sequence" $       withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $         testCLISucceeded@@ -806,17 +819,85 @@     it "explains single rule" $       testCLISucceeded         ["explain", "--rule=resources/copy.yaml"]-        ["\\documentclass{article}", "\\usepackage{amsmath}", "\\begin{document}", "\\rule{COPY}", "\\end{document}"]+        [ unlines+            [ "\\begin{tabular}{rl}"+            , "\\trrule{COPY}"+            , "  { [[ B1, \\tau -> ?, B2 ]]( \\tau -> e1 ) }"+            , "  { [[ B1, \\tau -> e3, B2 ]] }"+            , "  { if NF( e1 ) }"+            , "  { where e2 <- scope( e1 ); e3 <- contextualize( e1, e2 ) }"+            , "\\end{tabular}"+            ]+        ]      it "explains multiple rules" $       testCLISucceeded         ["explain", "--rule=resources/copy.yaml", "--rule=resources/alpha.yaml"]-        ["\\documentclass{article}", "\\rule{COPY}", "\\rule{ALPHA}"]+        ["\\begin{tabular}{rl}", "\\trrule{COPY}", "\\trrule{ALPHA}"]      it "explains normalization rules" $       testCLISucceeded         ["explain", "--normalize"]-        ["\\documentclass{article}", "\\begin{document}", "\\end{document}"]+        [ unlines+            [ "\\begin{tabular}{rl}"+            , "\\trrule{ALPHA}"+            , "  { [[ B1, \\tau1 -> ?, B2 ]]( \\tau2 -> e ) }"+            , "  { [[ B1, \\tau1 -> ?, B2 ]]( \\tau1 -> e ) }"+            , "  { if ordinal( \\tau2 ) = length( B1 ) }"+            , "  { }"+            , "\\trrule{COPY}"+            , "  { [[ B1, \\tau -> ?, B2 ]]( \\tau -> e1 ) }"+            , "  { [[ B1, \\tau -> e3, B2 ]] }"+            , "  { if NF( e1 ) }"+            , "  { where e2 <- scope( e1 ); e3 <- contextualize( e1, e2 ) }"+            , "\\trrule{DC}"+            , "  { T( \\tau -> e ) }"+            , "  { T }"+            , "  { }"+            , "  { }"+            , "\\trrule{DD}"+            , "  { T.\\tau }"+            , "  { T }"+            , "  { }"+            , "  { }"+            , "\\trrule{DOT}"+            , "  { [[ B1, \\tau -> e1, B2 ]].\\tau }"+            , "  { e2( ^ -> [[ B1, \\tau -> e1, B2 ]] ) }"+            , "  { if NF( e1 ) }"+            , "  { where e2 <- contextualize( e1, [[ B1, \\tau -> e1, B2 ]] ) }"+            , "\\trrule{MISS}"+            , "  { [[ B ]]( \\tau -> e ) }"+            , "  { T }"+            , "  { if \\( \\tau \\notin B \\) and \\( \\tau \\notin [ ~0, ~1, \\dots ] \\) }"+            , "  { }"+            , "\\trrule{NULL}"+            , "  { [[ B1, \\tau -> ?, B2 ]].\\tau }"+            , "  { T }"+            , "  { }"+            , "  { }"+            , "\\trrule{OVER}"+            , "  { [[ B1, \\tau -> e1, B2 ]]( \\tau -> e2 ) }"+            , "  { T }"+            , "  { if \\tau \\not= ^ }"+            , "  { }"+            , "\\trrule{PHI}"+            , "  { [[ B ]].\\tau }"+            , "  { [[ B ]].@.\\tau }"+            , "  { if \\( @ \\in B \\) and \\( \\tau \\notin B \\) }"+            , "  { }"+            , "\\trrule{STAY}"+            , "  { [[ B1, ^ -> e1, B2 ]]( ^ -> e2 ) }"+            , "  { [[ B1, ^ -> e1, B2 ]] }"+            , "  { }"+            , "  { }"+            , "\\trrule{STOP}"+            , "  { [[ B ]].\\tau }"+            , "  { T }"+            , "  { if \\( \\tau \\notin B \\) and \\( @ \\notin B \\) and \\( \\lambda \\notin B \\) }"+            , "  { }"+            , "\\end{tabular}"+            ]+        ]      it "fails with no rules specified" $       testCLIFailed@@ -837,8 +918,8 @@             testCLISucceeded ["explain", "--normalize", printf "--target=%s" path] []             content <- readFile path             _ <- evaluate (length content)-            content `shouldContain` "\\documentclass{article}"-            content `shouldContain` "\\begin{document}"+            content `shouldContain` "\\begin{tabular}{rl}"+            content `shouldContain` "\\end{tabular}"         )    describe "merge" $ do

@@ -36,7 +36,7 @@       , ("eq(1,-2)", Y.Eq (Y.CmpNum (Y.Literal 1)) (Y.CmpNum (Y.Literal (-2))))       , ("eq(ordinal(z),length(!B1))", Y.Eq (Y.CmpNum (Y.Ordinal (AtLabel "z"))) (Y.CmpNum (Y.Length (BiMeta "B1"))))       , ("eq(!a1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "a1")) (Y.CmpExpr (ExMeta "e2")))-      , ("or(xi(!e1), nf(Q.x))", Y.Or [Y.XI (ExMeta "e1"), Y.NF (ExDispatch ExGlobal (AtLabel "x"))])+      , ("or(xi(!e1), nf(Q.x))", Y.Or [Y.Xi (ExMeta "e1"), Y.NF (ExDispatch ExGlobal (AtLabel "x"))])       , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")])       ]       (\(expr, res) -> it expr (parseCondition expr `shouldBe` Right res))

@@ -1,193 +0,0 @@--- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com--- SPDX-License-Identifier: MIT--{- | Tests for the Lining module that converts CST to single-line format.-The module provides functions to remove line breaks and indentation from-phi-calculus concrete syntax trees while preserving structural semantics.--}-module LiningSpec (spec) where--import CST-import Control.Monad (forM_)-import Lining (LineFormat (..), toSingleLine, withLineFormat)-import Test.Hspec (Spec, describe, it, shouldBe, shouldNotBe)--spec :: Spec-spec = do-  describe "withLineFormat preserves multiline programs" $-    it "returns program unchanged" $-      let prog = PR_SWEET LCB (EX_GLOBAL Φ) RCB-       in withLineFormat MULTILINE prog `shouldBe` prog--  describe "withLineFormat converts to singleline" $-    it "applies toSingleLine transformation" $-      let prog = PR_SWEET LCB (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB) RCB-          result = withLineFormat SINGLELINE prog-       in result `shouldBe` PR_SWEET LCB (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB) RCB--  describe "LineFormat Eq instance" $-    forM_-      [ ("SINGLELINE equals SINGLELINE", SINGLELINE, SINGLELINE, True)-      , ("MULTILINE equals MULTILINE", MULTILINE, MULTILINE, True)-      , ("SINGLELINE differs from MULTILINE", SINGLELINE, MULTILINE, False)-      ]-      ( \(desc, fmt1, fmt2, expected) ->-          it desc $-            if expected-              then fmt1 `shouldBe` fmt2-              else fmt1 `shouldNotBe` fmt2-      )--  describe "LineFormat Show instance" $-    forM_-      [ ("SINGLELINE shows correctly", SINGLELINE, "SINGLELINE")-      , ("MULTILINE shows correctly", MULTILINE, "MULTILINE")-      ]-      ( \(desc, fmt, expected) ->-          it desc (show fmt `shouldBe` expected)-      )--  describe "toSingleLine PROGRAM for PR_SWEET" $-    it "removes newlines from expression" $-      let prog = PR_SWEET LCB (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB) RCB-       in toSingleLine prog `shouldBe` PR_SWEET LCB (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB) RCB--  describe "toSingleLine PROGRAM for PR_SALTY" $-    it "converts salty program to singleline" $-      let prog = PR_SALTY Φ ARROW (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB)-       in toSingleLine prog `shouldBe` PR_SALTY Φ ARROW (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB)--  describe "toSingleLine EXPRESSION for EX_FORMATION with empty binding" $-    it "removes tabs and newlines" $-      let ex = EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB-       in toSingleLine ex `shouldBe` EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB--  describe "toSingleLine EXPRESSION for EX_FORMATION with bindings" $-    it "converts to singleline with TAB markers" $-      let bd = BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1)) (TAB 1)-          ex = EX_FORMATION LSB EOL (TAB 1) bd EOL (TAB 0) RSB-          result = toSingleLine ex-       in result `shouldBe` EX_FORMATION LSB NO_EOL TAB' (BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1)) TAB') NO_EOL TAB' RSB--  describe "toSingleLine EXPRESSION for EX_DISPATCH" $-    it "converts nested expression" $-      let ex = EX_DISPATCH (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB) (AT_LABEL "attr")-       in toSingleLine ex `shouldBe` EX_DISPATCH (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB) (AT_LABEL "attr")--  describe "toSingleLine EXPRESSION for EX_APPLICATION" $-    it "converts with proper spacing" $-      let t = APP_BINDING (PA_TAU (AT_LABEL "y") ARROW (EX_GLOBAL Φ))-          ex = EX_APPLICATION (EX_GLOBAL Φ) EOL (TAB 1) t EOL (TAB 0) 1-       in toSingleLine ex `shouldBe` EX_APPLICATION (EX_GLOBAL Φ) NO_EOL TAB' (APP_BINDING (PA_TAU (AT_LABEL "y") ARROW (EX_GLOBAL Φ))) NO_EOL TAB' 1--  describe "toSingleLine EXPRESSION for EX_APPLICATION_TAUS" $-    it "converts taus application" $-      let ts = BI_PAIR (PA_TAU (AT_LABEL "z") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1)) (TAB 1)-          ex = EX_APPLICATION_TAUS (EX_GLOBAL Φ) EOL (TAB 1) ts EOL (TAB 0) 1-       in toSingleLine ex `shouldBe` EX_APPLICATION_TAUS (EX_GLOBAL Φ) NO_EOL TAB' (BI_PAIR (PA_TAU (AT_LABEL "z") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1)) TAB') NO_EOL TAB' 1--  describe "toSingleLine EXPRESSION for EX_APPLICATION_EXPRS" $-    it "converts expressions application" $-      let as = APP_ARG (EX_GLOBAL Φ) AAS_EMPTY-          ex = EX_APPLICATION_EXPRS (EX_GLOBAL Φ) EOL (TAB 1) as EOL (TAB 0) 1-       in toSingleLine ex `shouldBe` EX_APPLICATION_EXPRS (EX_GLOBAL Φ) NO_EOL TAB' (APP_ARG (EX_GLOBAL Φ) AAS_EMPTY) NO_EOL TAB' 1--  describe "toSingleLine EXPRESSION for EX_PHI_MEET" $-    it "converts meet expression" $-      let ex = EX_PHI_MEET Nothing 0 (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB)-       in toSingleLine ex `shouldBe` EX_PHI_MEET Nothing 0 (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB)--  describe "toSingleLine EXPRESSION for EX_PHI_AGAIN" $-    it "converts again expression" $-      let ex = EX_PHI_AGAIN Nothing 1 (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB)-       in toSingleLine ex `shouldBe` EX_PHI_AGAIN Nothing 1 (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB)--  describe "toSingleLine EXPRESSION leaves primitives unchanged" $-    forM_-      [ ("EX_GLOBAL", EX_GLOBAL Φ)-      , ("EX_XI", EX_XI XI)-      , ("EX_ATTR", EX_ATTR (AT_LABEL "attr"))-      , ("EX_TERMINATION", EX_TERMINATION DEAD)-      , ("EX_STRING", EX_STRING "тест" (TAB 0) [])-      , ("EX_NUMBER", EX_NUMBER (Left 42) (TAB 0) [])-      , ("EX_META", EX_META (MT_EXPRESSION "e"))-      , ("EX_META_TAIL", EX_META_TAIL (EX_GLOBAL Φ) (MT_TAIL "t"))-      ]-      ( \(desc, ex) ->-          it desc (toSingleLine ex `shouldBe` ex)-      )--  describe "toSingleLine APP_BINDING" $-    it "converts nested pair expression" $-      let bd = APP_BINDING (PA_TAU (AT_LABEL "x") ARROW (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB))-       in toSingleLine bd `shouldBe` APP_BINDING (PA_TAU (AT_LABEL "x") ARROW (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB))--  describe "toSingleLine BINDING for BI_PAIR" $-    it "converts to singleline" $-      let bd = BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1)) (TAB 1)-       in toSingleLine bd `shouldBe` BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1)) TAB'--  describe "toSingleLine BINDING for BI_META" $-    it "converts meta binding" $-      let bd = BI_META (MT_BINDING "B") (BDS_EMPTY (TAB 1)) (TAB 1)-       in toSingleLine bd `shouldBe` BI_META (MT_BINDING "B") (BDS_EMPTY (TAB 1)) TAB'--  describe "toSingleLine BINDING for BI_EMPTY" $-    it "returns binding unchanged" $-      let bd = BI_EMPTY (TAB 1)-       in toSingleLine bd `shouldBe` bd--  describe "toSingleLine BINDINGS for BDS_PAIR" $-    it "converts to singleline" $-      let bds = BDS_PAIR EOL (TAB 1) (PA_TAU (AT_LABEL "y") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1))-       in toSingleLine bds `shouldBe` BDS_PAIR NO_EOL TAB' (PA_TAU (AT_LABEL "y") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1))--  describe "toSingleLine BINDINGS for BDS_META" $-    it "converts meta bindings" $-      let bds = BDS_META EOL (TAB 1) (MT_BINDING "B") (BDS_EMPTY (TAB 1))-       in toSingleLine bds `shouldBe` BDS_META NO_EOL TAB' (MT_BINDING "B") (BDS_EMPTY (TAB 1))--  describe "toSingleLine BINDINGS for BDS_EMPTY" $-    it "returns bindings unchanged" $-      let bds = BDS_EMPTY (TAB 1)-       in toSingleLine bds `shouldBe` bds--  describe "toSingleLine PAIR for PA_TAU" $-    it "converts expression" $-      let pr = PA_TAU (AT_LABEL "x") ARROW (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB)-       in toSingleLine pr `shouldBe` PA_TAU (AT_LABEL "x") ARROW (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB)--  describe "toSingleLine PAIR for PA_FORMATION" $-    it "converts formation pair" $-      let pr = PA_FORMATION (AT_LABEL "f") [AT_LABEL "v"] ARROW (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB)-       in toSingleLine pr `shouldBe` PA_FORMATION (AT_LABEL "f") [AT_LABEL "v"] ARROW (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB)--  describe "toSingleLine PAIR leaves non-expression pairs unchanged" $-    forM_-      [ ("PA_VOID", PA_VOID (AT_LABEL "v") ARROW EMPTY)-      , ("PA_LAMBDA", PA_LAMBDA "λфункция")-      , ("PA_LAMBDA'", PA_LAMBDA' "Function")-      , ("PA_META_LAMBDA", PA_META_LAMBDA (MT_FUNCTION "F"))-      , ("PA_META_LAMBDA'", PA_META_LAMBDA' (MT_FUNCTION "F"))-      , ("PA_DELTA", PA_DELTA (BT_ONE "FF"))-      , ("PA_DELTA'", PA_DELTA' (BT_MANY ["00", "01"]))-      , ("PA_META_DELTA", PA_META_DELTA (MT_BYTES "d"))-      , ("PA_META_DELTA'", PA_META_DELTA' (MT_BYTES "d"))-      ]-      ( \(desc, pr) ->-          it desc (toSingleLine pr `shouldBe` pr)-      )--  describe "toSingleLine APP_ARG" $-    it "converts expression and args" $-      let arg = APP_ARG (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB) AAS_EMPTY-       in toSingleLine arg `shouldBe` APP_ARG (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB) AAS_EMPTY--  describe "toSingleLine APP_ARGS for AAS_EXPR" $-    it "converts nested expression" $-      let as = AAS_EXPR EOL (TAB 1) (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB) AAS_EMPTY-       in toSingleLine as `shouldBe` AAS_EXPR NO_EOL TAB' (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB) AAS_EMPTY--  describe "toSingleLine APP_ARGS for AAS_EMPTY" $-    it "returns unchanged" $-      toSingleLine AAS_EMPTY `shouldBe` AAS_EMPTY

@@ -99,7 +99,7 @@                   if normalize'                     then pure normalizationRules                     else pure []-              rewrittens <-+              (rewrittens, _) <-                 rewrite                   prog                   rules'