diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -29,7 +29,7 @@ ```bash cabal update -cabal install --overwrite-policy=always phino-0.0.0.57 +cabal install --overwrite-policy=always phino-0.0.0.58 phino --version ``` diff --git a/phino.cabal b/phino.cabal --- a/phino.cabal +++ b/phino.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino -version: 0.0.0.58 +version: 0.0.0.59 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at @@ -155,7 +155,6 @@ containers ^>=0.6.7, directory ^>=1.3.8.5, filepath ^>=1.4.301.0, - hlint ^>=3.8, hspec ^>=2.11.16, hspec-core ^>=2.11.16, megaparsec ^>=9.7.0, diff --git a/src/AST.hs b/src/AST.hs --- a/src/AST.hs +++ b/src/AST.hs @@ -1,5 +1,4 @@ {-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE LambdaCase #-} -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT @@ -61,10 +60,15 @@ show (AtMeta meta) = '!' : meta countNodes :: Expression -> Int -countNodes ExGlobal = 1 -countNodes ExTermination = 1 -countNodes ExThis = 1 -countNodes (ExApplication expr' (BiTau _ bexpr')) = 2 + countNodes expr' + countNodes bexpr' +countNodes (ExFormation bds) = 1 + sum (map nodesInBinding bds) + length bds + where + nodesInBinding :: Binding -> Int + nodesInBinding (BiTau _ expr) = countNodes expr + 2 + nodesInBinding (BiMeta _) = 1 + nodesInBinding _ = 3 +countNodes (ExApplication expr (BiTau _ expr')) = 4 + countNodes expr + countNodes expr' countNodes (ExDispatch expr' _) = 2 + countNodes expr' -countNodes (ExFormation bds) = 1 + sum (map (\case BiTau _ expr' -> countNodes expr'; _ -> 1) bds) -countNodes _ = 0 +countNodes (ExMetaTail expr _) = 2 + countNodes expr +countNodes (ExPhiMeet _ _ expr) = countNodes expr +countNodes (ExPhiAgain _ _ expr) = countNodes expr +countNodes _ = 1 diff --git a/src/CLI.hs b/src/CLI.hs --- a/src/CLI.hs +++ b/src/CLI.hs @@ -3,7 +3,6 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-} -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT @@ -19,15 +18,16 @@ import Data.Foldable (for_) import Data.Functor ((<&>)) import Data.List (intercalate) -import Data.Maybe (fromJust, isJust, isNothing) +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), explainRules, programToLaTeX, rewrittensToLatex) +import LaTeX (LatexContext (LatexContext), explainRules, expressionToLaTeX, programToLaTeX, rewrittensToLatex) import Lining (LineFormat (MULTILINE, SINGLELINE)) +import Locator (locatedExpression) import Logger import Merge (merge) import Misc (ensuredFile) @@ -48,27 +48,33 @@ import qualified Yaml as Y data PrintProgramContext = PrintProgCtx - { sugar :: SugarType - , line :: LineFormat - , xmirCtx :: XmirContext - , nonumber :: Bool - , compress :: Bool - , expression :: Maybe String - , label :: Maybe String - , meetPrefix :: Maybe String - , outputFormat :: IOFormat + { _sugar :: SugarType + , _line :: LineFormat + , _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 @@ -86,94 +92,100 @@ 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 - , hide :: [String] - , show' :: [String] - , locator :: String - , expression :: Maybe String - , label :: Maybe String - , meetPrefix :: Maybe String - , stepsDir :: Maybe FilePath - , inputFile :: Maybe FilePath + { _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 + , _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 + { _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 - , rules :: [FilePath] - , hide :: [String] - , show' :: [String] - , locator :: String - , expression :: Maybe String - , label :: Maybe String - , meetPrefix :: Maybe String - , targetFile :: Maybe FilePath - , stepsDir :: Maybe FilePath - , inputFile :: Maybe FilePath + { _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 + , _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 - , targetFile :: Maybe FilePath - , inputs :: [FilePath] + { _logLevel :: LogLevel + , _logLines :: Int + , _inputFormat :: IOFormat + , _outputFormat :: IOFormat + , _sugarType :: SugarType + , _flat :: LineFormat + , _omitListing :: Bool + , _omitComments :: Bool + , _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 + { _logLevel :: LogLevel + , _logLines :: Int + , _sugarType :: SugarType + , _flat :: LineFormat + , _pattern :: Maybe String + , _when :: Maybe String + , _inputFile :: Maybe FilePath } validateIntOption :: (Int -> Bool) -> String -> Int -> ReadM Int @@ -243,6 +255,25 @@ (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) +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 "The minimum popularity of an expression in order to be suitable for \\phiMeet{}, in percentage (default: 50)") + ) + +optMeetLength :: Parser (Maybe Int) +optMeetLength = + optional + ( option + (auto >>= validateIntOption (> 0) "--meet-length must be positive") + (long "meet-length" <> metavar "NODES" <> help "The minimum length of an expression that fits into \\phiMeet{}, in AST nodes (default: 8)") + ) + 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)") @@ -282,6 +313,16 @@ 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") @@ -350,9 +391,12 @@ <*> optCompress <*> optMaxDepth <*> optMaxCycles + <*> optMeetPopularity + <*> optMeetLength <*> optHide <*> optShow <*> optLocator + <*> optFocus <*> optExpression <*> optLabel <*> optMeetPrefix @@ -390,10 +434,13 @@ <*> optCompress <*> optMaxDepth <*> optMaxCycles + <*> optMeetPopularity + <*> optMeetLength <*> optRule <*> optHide <*> optShow <*> optLocator + <*> optFocus <*> optExpression <*> optLabel <*> optMeetPrefix @@ -456,13 +503,13 @@ setLogger :: Command -> IO () setLogger cmd = - let (level, lines) = case cmd of - CmdRewrite OptsRewrite{logLevel, logLines} -> (logLevel, logLines) - CmdDataize OptsDataize{logLevel, logLines} -> (logLevel, logLines) - CmdExplain OptsExplain{logLevel, logLines} -> (logLevel, logLines) - CmdMerge OptsMerge{logLevel, logLines} -> (logLevel, logLines) - CmdMatch OptsMatch{logLevel, logLines} -> (logLevel, logLines) - in setLogConfig level lines + let (level, lns) = case cmd of + CmdRewrite OptsRewrite{_logLevel, _logLines} -> (_logLevel, _logLines) + CmdDataize OptsDataize{_logLevel, _logLines} -> (_logLevel, _logLines) + CmdExplain OptsExplain{_logLevel, _logLines} -> (_logLevel, _logLines) + CmdMerge OptsMerge{_logLevel, _logLines} -> (_logLevel, _logLines) + CmdMatch OptsMatch{_logLevel, _logLines} -> (_logLevel, _logLines) + in setLogConfig level lns invalidCLIArguments :: String -> IO a invalidCLIArguments msg = throwIO (InvalidCLIArguments msg) @@ -474,44 +521,44 @@ case cmd of CmdRewrite OptsRewrite{..} -> do validateOpts - excluded <- validatedDispatches "hide" hide - included <- validatedDispatches "show" show' - [loc] <- validatedDispatches "locator" [locator] - 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)) - xmirCtx = XmirContext omitListing omitComments listing - printCtx = PrintProgCtx sugarType flat xmirCtx nonumber compress expression label meetPrefix outputFormat - _canonize = if canonize then C.canonize else id - _hide = (`F.exclude` excluded) - _show = (`F.include` included) - rewrittens <- rewrite program rules' (context loc printCtx) <&> _canonize . _hide . _show - let rewrittens' = if sequence then rewrittens else [last rewrittens] - logDebug (printf "Printing rewritten 𝜑-program as %s" (show outputFormat)) + 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)) + 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 + output _targetFile progs where validateOpts :: IO () validateOpts = do when - (inPlace && isNothing inputFile) + (_inPlace && isNothing _inputFile) (invalidCLIArguments "The option --in-place requires an input file") when - (inPlace && isJust targetFile) + (_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") + 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")] - validateMust' must - validateXmirOptions - outputFormat - [(omitListing, "omit-listing"), (omitComments, "omit-comments")] + _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 + 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 @@ -529,98 +576,152 @@ context loc ctx = RewriteContext loc - maxDepth - maxCycles - depthSensitive + _maxDepth + _maxCycles + _depthSensitive buildTerm - must - (saveStepFunc stepsDir ctx) + _must + (saveStepFunc _stepsDir ctx) + printProgCtx :: XmirContext -> Expression -> PrintProgramContext + printProgCtx xmirCtx focus = + PrintProgCtx + _sugarType + _flat + 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] - input <- readInput inputFile - prog <- parseProgram input inputFormat - let printCtx = PrintProgCtx sugarType flat defaultXmirContext nonumber compress expression label meetPrefix outputFormat - _canonize = if canonize then C.canonize else id - _hide = (`F.exclude` excluded) - _show = (`F.include` included) - (maybeBytes, seq) <- dataize (context loc prog printCtx) - when sequence (printRewrittens printCtx (_canonize $ _hide $ _show seq) >>= putStrLn) - unless quiet (putStrLn (maybe (P.printExpression ExTermination) P.printBytes maybeBytes)) + 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")] - validateXmirOptions - outputFormat - [(omitListing, "omit-listing"), (omitComments, "omit-comments")] - when (length show' > 1) (invalidCLIArguments "The option --show can be used only once") + _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 + _maxDepth + _maxCycles + _depthSensitive buildTerm - (saveStepFunc stepsDir ctx) + (saveStepFunc _stepsDir ctx) + printProgCtx :: Expression -> PrintProgramContext + printProgCtx focus = + PrintProgCtx + _sugarType + _flat + defaultXmirContext + _nonumber + _compress + _sequence + (justMeetPopularity _meetPopularity) + (justMeetLength _meetLength) + focus + _expression + _label + _meetPrefix + _outputFormat CmdExplain OptsExplain{..} -> do validateOpts - rules' <- getRules normalize shuffle rules - output targetFile (explainRules rules') + rules <- getRules _normalize _shuffle _rules + printOut _targetFile (explainRules rules) where validateOpts :: IO () validateOpts = when - (null rules && not normalize) + (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' + inputs' <- traverse (readInput . Just) _inputs + progs <- traverse (`parseProgram` _inputFormat) inputs' prog <- merge progs - let listing = const (P.printProgram' prog (sugarType, UNICODE, flat)) - xmirCtx = XmirContext omitListing omitComments listing - printProgCtx = PrintProgCtx sugarType flat xmirCtx False False Nothing Nothing Nothing outputFormat - prog' <- printProgram printProgCtx prog - output targetFile prog' + let listing = const (P.printProgram' prog (_sugarType, UNICODE, _flat)) + xmirCtx = XmirContext _omitListing _omitComments listing + printCtx = printProgCtx xmirCtx + prog' <- printProgram printCtx prog + printOut _targetFile prog' where validateOpts :: IO () validateOpts = do when - (null inputs) + (null _inputs) (throwIO (InvalidCLIArguments "At least one input file must be specified for 'merge' command")) - validateXmirOptions outputFormat [(omitListing, "omit-listing"), (omitComments, "omit-comments")] + validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] "Q" + printProgCtx :: XmirContext -> PrintProgramContext + printProgCtx xmirCtx = + PrintProgCtx + _sugarType + _flat + xmirCtx + False + False + False + (justMeetPopularity Nothing) + (justMeetLength Nothing) + ExGlobal + Nothing + Nothing + Nothing + _outputFormat CmdMatch OptsMatch{..} -> do - input <- readInput inputFile + input <- readInput _inputFile prog <- parseProgram input PHI - if isNothing pattern + if isNothing _pattern then logDebug "The --pattern is not provided, no substitutions are built" else do - ptn <- parseExpressionThrows (fromJust pattern) - condition <- traverse parseConditionThrows when' + 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)) + else putStrLn (P.printSubsts' substs (_sugarType, UNICODE, _flat)) 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 50 + +justMeetLength :: Maybe Int -> Int +justMeetLength = fromMaybe 8 + -- 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 + | _outputFormat == LATEX = "tex" + | otherwise = show _outputFormat -- Validate given expressions as valid dispatches validatedDispatches :: String -> [String] -> IO [Expression] @@ -630,8 +731,8 @@ asDispatch expr = asDispatch' expr where asDispatch' :: Expression -> IO Expression - asDispatch' exp@ExGlobal = pure exp - asDispatch' exp@(ExDispatch ex _) = asDispatch' ex >> pure exp + asDispatch' ex@ExGlobal = pure ex + asDispatch' disp@(ExDispatch ex _) = asDispatch' ex >> pure disp asDispatch' _ = invalidCLIArguments ( printf @@ -641,24 +742,24 @@ ) -- Validate LaTeX options -validateLatexOptions :: IOFormat -> [(Bool, String)] -> [(Maybe String, String)] -> IO () -validateLatexOptions LATEX _ _ = pure () -validateLatexOptions _ bools maybes = do +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_ - maybes - (\(maybe', opt) -> when (isJust maybe') (invalidCLIArguments (printf msg opt))) + 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)] -> IO () -validateXmirOptions XMIR _ = pure () -validateXmirOptions _ bools = +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)) @@ -685,15 +786,23 @@ printRewrittens :: PrintProgramContext -> [Rewritten] -> IO String printRewrittens ctx@PrintProgCtx{..} rewrittens - | outputFormat == LATEX = pure (rewrittensToLatex rewrittens (LatexContext sugar line nonumber compress expression label meetPrefix)) - | otherwise = mapM (printProgram ctx . fst) rewrittens <&> intercalate "\n" + | _outputFormat == LATEX && _sequence = rewrittensToLatex rewrittens (LatexContext _sugar _line _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)) + XMIR -> throwIO CouldNotPrintExpressionInXMIR + LATEX -> pure (expressionToLaTeX ex (LatexContext _sugar _line _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)) - XMIR -> programToXMIR prog xmirCtx <&> printXMIR - LATEX -> pure (programToLaTeX prog (LatexContext sugar line nonumber compress expression label meetPrefix)) +printProgram PrintProgCtx{..} prog = case _outputFormat of + PHI -> pure (P.printProgram' prog (_sugar, UNICODE, _line)) + XMIR -> programToXMIR prog _xmirCtx <&> printXMIR + LATEX -> pure (programToLaTeX prog (LatexContext _sugar _line _nonumber _compress _meetPopularity _meetLength _focus _expression _label _meetPrefix)) -- Get rules for rewriting depending on provided flags getRules :: Bool -> Bool -> [FilePath] -> IO [Y.Rule] @@ -720,8 +829,8 @@ else pure ordered -- Output content -output :: Maybe FilePath -> String -> IO () -output target content = case target of +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 diff --git a/src/Encoding.hs b/src/Encoding.hs --- a/src/Encoding.hs +++ b/src/Encoding.hs @@ -3,7 +3,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Encoding (toASCII, withEncoding, Encoding (..)) where +module Encoding (toASCII, withEncoding, Encoding (..), ToASCII) where import CST diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -1,6 +1,7 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE RecordWildCards #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-} -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT @@ -9,6 +10,7 @@ ( explainRules , rewrittensToLatex , programToLaTeX + , expressionToLaTeX , defaultLatexContext , LatexContext (..) , meetInPrograms @@ -19,72 +21,68 @@ import CST import Data.List (intercalate, nub) import Data.Maybe (fromMaybe) -import Encoding (Encoding (ASCII), withEncoding) -import Lining (LineFormat (MULTILINE), withLineFormat) +import Encoding (Encoding (ASCII), ToASCII, withEncoding) +import Lining (LineFormat (MULTILINE), ToSingleLine, withLineFormat) +import Locator (locatedExpression) import Matcher import Misc import Render (Render (render)) import Replacer (replaceProgram) import Rewriter (Rewritten) -import Sugar (SugarType (SWEET), withSugarType) +import Sugar (SugarType (SWEET), ToSalty, withSugarType) import Text.Printf (printf) import qualified Yaml as Y data LatexContext = LatexContext - { sugar :: SugarType - , line :: LineFormat - , nonumber :: Bool - , compress :: Bool - , expression :: Maybe String - , label :: Maybe String - , meetPrefix :: Maybe String + { _sugar :: SugarType + , _line :: LineFormat + , _nonumber :: Bool + , _compress :: Bool + , _meetPopularity :: Int + , _meetLength :: Int + , _focus :: Expression + , _expression :: Maybe String + , _label :: Maybe String + , _meetPrefix :: Maybe String } defaultLatexContext :: LatexContext -defaultLatexContext = LatexContext SWEET MULTILINE False False Nothing Nothing Nothing +defaultLatexContext = LatexContext SWEET MULTILINE False False 50 8 ExGlobal Nothing Nothing Nothing -meetInProgram :: Program -> Program -> [Expression] -meetInProgram (Program expr) = meetInExpression expr +meetInProgram :: Program -> Int -> Program -> [Expression] +meetInProgram (Program expr) len = meetInExpression expr where meetInExpression :: Expression -> Program -> [Expression] - meetInExpression ExGlobal _ = [] - meetInExpression ExThis _ = [] - meetInExpression ExTermination _ = [] - meetInExpression (ExFormation [BiVoid AtRho]) _ = [] - meetInExpression (ExFormation [BiDelta _, BiVoid AtRho]) _ = [] - meetInExpression (ExFormation []) _ = [] - meetInExpression (ExDispatch ExGlobal _) _ = [] - meetInExpression (ExDispatch ExThis _) _ = [] - meetInExpression (ExDispatch ExTermination _) _ = [] meetInExpression (DataString _) _ = [] meetInExpression (DataNumber _) _ = [] meetInExpression (ExPhiMeet{}) _ = [] meetInExpression (ExPhiAgain{}) _ = [] - meetInExpression expr prog = - map (const expr) (matchProgram expr prog) ++ case expr of - ExDispatch exp _ -> meetInExpression exp prog - ExApplication exp (BiTau _ arg) -> meetInExpression exp prog ++ meetInExpression arg prog - ExFormation bds -> meetInBindings bds prog - _ -> [] + meetInExpression ex prog = + let matched = if countNodes ex >= len then map (const ex) (matchProgram ex prog) else [] + in matched ++ case ex of + ExDispatch ex' _ -> meetInExpression ex' prog + ExApplication ex' (BiTau _ arg) -> meetInExpression ex' prog ++ meetInExpression arg prog + ExFormation bds -> meetInBindings bds prog + _ -> [] meetInBindings :: [Binding] -> Program -> [Expression] meetInBindings [] _ = [] - meetInBindings (BiTau _ expr : bds) prog = meetInExpression expr prog ++ meetInBindings bds prog + meetInBindings (BiTau _ ex : bds) prog = meetInExpression ex prog ++ meetInBindings bds prog meetInBindings (_ : bds) prog = meetInBindings bds prog {- | Here we're trying to compress sequence of programs with \phiMeet{} and \phiAgain LaTeX functions. We process the sequence of programs and trying to find all expressions in first program which are present in following programs. Then we find ONE expression which is the most frequently encountered. -If it's encountered in more than 50% of following programs - we replace it with \phiAgain{} in following -programs and with \phiMeet{} in first program. +If it's encountered in more than specific percentage (_meetPopularity) of following programs - we replace +it with \phiAgain{} in following programs and with \phiMeet{} in first program. -} -meetInPrograms :: Maybe String -> [Program] -> [Program] -meetInPrograms prefix = meetInPrograms' 1 +meetInPrograms :: [Program] -> LatexContext -> [Program] +meetInPrograms prog LatexContext{..} = meetInPrograms' prog 1 where - meetInPrograms' :: Int -> [Program] -> [Program] - meetInPrograms' _ [] = [] - meetInPrograms' _ [prog] = [prog] - meetInPrograms' idx (first : rest) = - let met = map (meetInProgram first) rest + meetInPrograms' :: [Program] -> Int -> [Program] + meetInPrograms' [] _ = [] + meetInPrograms' [program] _ = [program] + meetInPrograms' (first : rest) idx = + let met = map (meetInProgram first _meetLength) rest unique = nub (concat met) (frequent, _) = foldl @@ -96,62 +94,95 @@ ) (Nothing, 0) unique - next = first : meetInPrograms' idx rest + next = first : meetInPrograms' rest idx in case frequent of Just expr -> case matchProgram expr first of (_ : substs) -> let met' = map (filter (== expr)) met - prog = replaceProgram (first, [expr], [ExPhiMeet prefix idx]) - prog' = replaceProgram (prog, map (const expr) substs, map (const (ExPhiAgain prefix idx)) substs) - rest' = zipWith (\prgm exprs -> replaceProgram (prgm, exprs, map (const (ExPhiAgain prefix idx)) exprs)) rest met' + program = replaceProgram (first, [expr], [ExPhiMeet _meetPrefix idx]) + program' = replaceProgram (program, map (const expr) substs, map (const (ExPhiAgain _meetPrefix idx)) substs) + rest' = zipWith (\prgm exprs -> replaceProgram (prgm, exprs, map (const (ExPhiAgain _meetPrefix idx)) exprs)) rest met' found = filter (not . null) met' - in if length met' > 1 && toDouble (length found) / toDouble (length met') >= 0.5 - then prog' : meetInPrograms' (idx + 1) rest' + in if length met' > 1 && toDouble (length found) / toDouble (length met') >= popularity + then program' : meetInPrograms' rest' (idx + 1) else next [] -> next _ -> next + popularity :: Double + popularity = toDouble _meetPopularity / 100.0 -renderToLatex :: Program -> LatexContext -> String -renderToLatex prog LatexContext{..} = render (toLaTeX $ withLineFormat line $ withEncoding ASCII $ withSugarType sugar $ programToCST prog) +renderToLatex :: (ToSalty a, ToASCII a, ToSingleLine a, ToLaTeX a, Render a) => a -> LatexContext -> String +renderToLatex renderable LatexContext{..} = render (toLaTeX $ withLineFormat _line $ withEncoding ASCII $ withSugarType _sugar renderable) phiquation :: LatexContext -> String -phiquation LatexContext{nonumber = True} = "phiquation*" -phiquation LatexContext{nonumber = False} = "phiquation" +phiquation LatexContext{_nonumber = True} = "phiquation*" +phiquation LatexContext{_nonumber = False} = "phiquation" -rewrittensToLatex :: [Rewritten] -> LatexContext -> String -rewrittensToLatex rewrittens ctx@LatexContext{..} = +preamble :: LatexContext -> String +preamble ctx@LatexContext{..} = let equation = phiquation ctx - (progs, rules) = unzip rewrittens - rewrittens' = if compress then zip (meetInPrograms meetPrefix progs) rules else rewrittens in concat [ printf "\\begin{%s}\n" equation - , maybe "" (printf "\\label{%s}\n") label - , maybe "" (printf "\\phiExpression{%s} ") expression - , intercalate - "\n \\leadsto " - ( map - ( \(program, maybeName) -> - let prog = renderToLatex program ctx - in maybe prog (printf "%s \\leadsto_{\\nameref{r:%s}}" prog) maybeName - ) - rewrittens' - ) - , printf "{.}\n\\end{%s}" equation + , maybe "" (printf "\\label{%s}\n") _label + , maybe "" (printf "\\phiExpression{%s} ") _expression ] +body :: [(a, Maybe String)] -> (a -> String) -> String +body printed toLatex = + intercalate + "\n \\leadsto " + ( map + ( \(item, maybeName) -> + let item' = toLatex item + in maybe item' (printf "%s \\leadsto_{\\nameref{r:%s}}" item') maybeName + ) + printed + ) + +ending :: LatexContext -> String +ending ctx = printf "{.}\n\\end{%s}" (phiquation ctx) + +metRewrittens :: [Rewritten] -> LatexContext -> [Rewritten] +metRewrittens 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} = + pure + ( concat + [ preamble ctx + , body (metRewrittens rewrittens ctx) (\prog -> renderToLatex (programToCST prog) ctx) + , ending ctx + ] + ) +rewrittensToLatex rewrittens ctx@LatexContext{..} = do + let (progs, rules) = unzip (metRewrittens rewrittens ctx) + exprs <- mapM (locatedExpression _focus) progs + pure + ( concat + [ preamble ctx + , body (zip exprs rules) (\expr -> renderToLatex (expressionToCST expr) ctx) + , ending ctx + ] + ) + programToLaTeX :: Program -> LatexContext -> String programToLaTeX prog ctx = - let equation = phiquation ctx - in concat - [ "\\begin{" - , equation - , "}\n" - , renderToLatex prog ctx - , "\n\\end{" - , equation - , "}" - ] + concat + [ preamble ctx + , renderToLatex (programToCST prog) ctx + , ending ctx + ] + +expressionToLaTeX :: Expression -> LatexContext -> String +expressionToLaTeX ex ctx = + concat + [ preamble ctx + , renderToLatex (expressionToCST ex) ctx + , ending ctx + ] piped :: String -> String piped str = "|" <> str <> "|" diff --git a/src/Lining.hs b/src/Lining.hs --- a/src/Lining.hs +++ b/src/Lining.hs @@ -4,7 +4,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Lining (toSingleLine, LineFormat (..), withLineFormat) where +module Lining (toSingleLine, LineFormat (..), withLineFormat, ToSingleLine) where import CST diff --git a/src/Rule.hs b/src/Rule.hs --- a/src/Rule.hs +++ b/src/Rule.hs @@ -31,9 +31,7 @@ import Yaml (normalizationRules) import qualified Yaml as Y -newtype RuleContext = RuleContext - { _buildTerm :: BuildTermFunc - } +newtype RuleContext = RuleContext {_buildTerm :: BuildTermFunc} -- Returns True if given expression matches with any of given normalization rules -- Here we use unsafePerformIO because we're sure that conditions which are used diff --git a/src/Sugar.hs b/src/Sugar.hs --- a/src/Sugar.hs +++ b/src/Sugar.hs @@ -7,7 +7,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Sugar (toSalty, withSugarType, SugarType (..)) where +module Sugar (toSalty, withSugarType, SugarType (..), ToSalty) where import AST import CST diff --git a/src/XMIR.hs b/src/XMIR.hs --- a/src/XMIR.hs +++ b/src/XMIR.hs @@ -41,9 +41,9 @@ import qualified Text.XML.Cursor as C data XmirContext = XmirContext - { omitListing :: Bool - , omitComments :: Bool - , listing :: Program -> String + { _omitListing :: Bool + , _omitComments :: Bool + , _listing :: Program -> String } defaultXmirContext :: XmirContext @@ -105,7 +105,7 @@ [object [] [NodeContent (T.pack (printBytes bytes))]] in pure ( "Φ.number" - , if omitComments + , if _omitComments then [bts] else [ NodeComment (T.pack (either show show (btsToNum bytes))) @@ -119,7 +119,7 @@ [object [] [NodeContent (T.pack (printBytes bytes))]] in pure ( "Φ.string" - , if omitComments + , if _omitComments then [bts] else [ NodeComment (T.pack ('"' : btsToStr bytes ++ "\"")) @@ -172,12 +172,12 @@ (pckg, expr') <- getPackage expr root <- rootExpression expr' ctx now <- getCurrentTime - let text = listing prog - listingContent = - if omitListing + let text = _listing prog + listing = + if _omitListing then show (length (lines text)) ++ " line(s)" else text - listing' = NodeElement (element "listing" [] [NodeContent (T.pack listingContent)]) + listing' = NodeElement (element "listing" [] [NodeContent (T.pack listing)]) metas = metasWithPackage (intercalate "." pckg) pure ( Document diff --git a/test/ASTSpec.hs b/test/ASTSpec.hs --- a/test/ASTSpec.hs +++ b/test/ASTSpec.hs @@ -220,18 +220,18 @@ , ("T", ExTermination, 1) , ("$", ExThis, 1) , ("dispatch on global", ExDispatch ExGlobal (AtLabel "x"), 3) - , ("application with globals", ExApplication ExGlobal (BiTau AtRho ExGlobal), 4) - , ("nested expressions", ExFormation [BiTau AtRho ExGlobal, BiTau AtPhi ExGlobal], 3) + , ("application with globals", ExApplication ExGlobal (BiTau AtRho ExGlobal), 6) + , ("nested expressions", ExFormation [BiTau AtRho ExGlobal, BiTau AtPhi ExGlobal], 9) , ("empty formation", ExFormation [], 1) - , ("void binding", ExFormation [BiVoid AtRho], 2) - , ("delta binding", ExFormation [BiDelta BtEmpty], 2) - , ("lambda binding", ExFormation [BiLambda "Func"], 2) - , ("meta binding", ExFormation [BiMeta "B"], 2) - , ("metalambda binding", ExFormation [BiMetaLambda "F"], 2) - , ("meta expression", ExMeta "e", 0) - , ("metatail expression", ExMetaTail ExGlobal "t", 0) + , ("void binding", ExFormation [BiVoid AtRho], 5) + , ("delta binding", ExFormation [BiDelta BtEmpty], 5) + , ("lambda binding", ExFormation [BiLambda "Func"], 5) + , ("meta binding", ExFormation [BiMeta "B"], 3) + , ("metalambda binding", ExFormation [BiMetaLambda "F"], 5) + , ("meta expression", ExMeta "e", 1) + , ("metatail expression", ExMetaTail ExGlobal "t", 3) , ("deeply nested dispatch", ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b"), 5) - , ("formation with dispatch inside", ExFormation [BiTau AtRho (ExDispatch ExGlobal (AtLabel "x"))], 4) + , ("formation with dispatch inside", ExFormation [BiTau AtRho (ExDispatch ExGlobal (AtLabel "x"))], 7) ] ( \(desc, expr, expected) -> it desc $ countNodes expr `shouldBe` expected diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -238,6 +238,42 @@ ["rewrite", "--show=Q.x(Q.y)"] ["[ERROR]:", "Only dispatch expression started with Φ (or Q) can be used in --show"] + it "with --meet-popularity < 0" $ + withStdin "{[[]]}" $ + testCLIFailed + ["rewrite", "--meet-popularity=-1"] + ["[ERROR]:", "--meet-popularity must be positive"] + + it "with --meet-popularity > 100" $ + withStdin "{[[]]}" $ + testCLIFailed + ["rewrite", "--meet-popularity=102"] + ["[ERROR]:", "--meet-popularity must be <= 100"] + + it "with --meet-popularity and output != latex" $ + withStdin "{[[]]}" $ + testCLIFailed + ["rewrite", "--meet-popularity=51", "--output=phi"] + ["[ERROR]:", "--meet-popularity option can stay together with --output=latex only"] + + it "with --meet-length and output != latex" $ + withStdin "{[[]]}" $ + testCLIFailed + ["rewrite", "--meet-length=4", "--output=phi"] + ["[ERROR]:", "--meet-length option can stay together with --output=latex only"] + + it "with non-dispatch --focus" $ + withStdin "{[[]]}" $ + testCLIFailed + ["rewrite", "--focus=Q.x(Q.y)"] + ["[ERROR]"] + + it "with --focus!=Q and --output=XMIR" $ + withStdin "{[[]]}" $ + testCLIFailed + ["rewrite", "--focus=Q.x", "--output=xmir"] + ["[ERROR]"] + it "prints help" $ testCLISucceeded ["rewrite", "--help"] @@ -318,44 +354,52 @@ withStdin "Q -> [[ x_o -> Q.z(y -> 5), q$ -> T, w -> $, ^ -> Q, @ -> 1, y -> \"H$@^M\", L> Fu_nc ]]" $ testCLISucceeded ["rewrite", "--output=latex", "--sweet"] - [ "\\begin{phiquation}" - , "\\Big\\{[[\n" - , " |x\\char95{}o| -> Q.|z|( |y| -> 5 ),\n" - , " |q\\char36{}| -> T,\n" - , " |w| -> $,\n" - , " ^ -> Q,\n" - , " @ -> 1,\n" - , " |y| -> \"H$@^M\",\n" - , " L> |Fu\\char95{}nc|\n" - , "]]\\Big\\}" - , "\\end{phiquation}" + [ unlines + [ "\\begin{phiquation}" + , "\\Big\\{[[" + , " |x\\char95{}o| -> Q.|z|( |y| -> 5 )," + , " |q\\char36{}| -> T," + , " |w| -> $," + , " ^ -> Q," + , " @ -> 1," + , " |y| -> \"H$@^M\"," + , " L> |Fu\\char95{}nc|" + , "]]\\Big\\}{.}" + , "\\end{phiquation}" + ] ] it "rewrites as LaTeX without numeration" $ withStdin "Q -> [[ x -> 5 ]]" $ testCLISucceeded ["rewrite", "--output=latex", "--sweet", "--nonumber", "--flat"] - [ "\\begin{phiquation*}" - , "\\Big\\{[[ |x| -> 5 ]]\\Big\\}" - , "\\end{phiquation*}" + [ unlines + [ "\\begin{phiquation*}" + , "\\Big\\{[[ |x| -> 5 ]]\\Big\\}{.}" + , "\\end{phiquation*}" + ] ] it "rewrite as LaTeX with expression name" $ withStdin "Q -> [[ x -> 5 ]]" $ testCLISucceeded ["rewrite", "--output=latex", "--sweet", "--flat", "--expression=foo"] - [ "\\begin{phiquation}" - , "\\phiExpression{foo} \\Big\\{[[ |x| -> 5 ]]\\Big\\}{.}\n" - , "\\end{phiquation}" + [ unlines + [ "\\begin{phiquation}" + , "\\phiExpression{foo} \\Big\\{[[ |x| -> 5 ]]\\Big\\}{.}" + , "\\end{phiquation}" + ] ] it "rewrite as LaTeX with label name" $ withStdin "Q -> [[ x -> 5 ]]" $ testCLISucceeded ["rewrite", "--output=latex", "--sweet", "--flat", "--label=foo"] - [ "\\begin{phiquation}\n\\label{foo}\n" - , "\\Big\\{[[ |x| -> 5 ]]\\Big\\}{.}\n" - , "\\end{phiquation}" + [ unlines + [ "\\begin{phiquation}\n\\label{foo}" + , "\\Big\\{[[ |x| -> 5 ]]\\Big\\}{.}" + , "\\end{phiquation}" + ] ] it "rewrites with XMIR as input" $ @@ -430,12 +474,12 @@ ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress", "--meet-prefix=foo"] [ unlines [ "\\begin{phiquation}" - , "\\Big\\{[[ |x| -> ?, |y| -> |x| ]]( |x| -> [[ D> 42- ]] ).|y|\\Big\\} \\leadsto_{\\nameref{r:copy}}" - , " \\leadsto \\Big\\{\\phiMeet{foo:1}{ [[ |x| -> [[ D> 42- ]], |y| -> |x| ]] }.|y|\\Big\\} \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\Big\\{\\phiAgain{foo:1}.|x|( ^ -> \\phiAgain{foo:1} )\\Big\\} \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\Big\\{[[ D> 42- ]]( ^ -> \\phiAgain{foo:1}, ^ -> \\phiAgain{foo:1} )\\Big\\} \\leadsto_{\\nameref{r:copy}}" - , " \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{foo:1} ]]( ^ -> \\phiAgain{foo:1} )\\Big\\} \\leadsto_{\\nameref{r:stay}}" - , " \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{foo:1} ]]\\Big\\}{.}" + , "\\Big\\{[[ |x| -> ?, |y| -> |x| ]]( |x| -> \\phiMeet{foo:1}{ [[ D> 42- ]] } ).|y|\\Big\\} \\leadsto_{\\nameref{r:copy}}" + , " \\leadsto \\Big\\{\\phiMeet{foo:2}{ [[ |x| -> \\phiAgain{foo:1}, |y| -> |x| ]] }.|y|\\Big\\} \\leadsto_{\\nameref{r:dot}}" + , " \\leadsto \\Big\\{\\phiAgain{foo:2}.|x|( ^ -> \\phiAgain{foo:2} )\\Big\\} \\leadsto_{\\nameref{r:dot}}" + , " \\leadsto \\Big\\{\\phiAgain{foo:1}( ^ -> \\phiAgain{foo:2}, ^ -> \\phiAgain{foo:2} )\\Big\\} \\leadsto_{\\nameref{r:copy}}" + , " \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{foo:2} ]]( ^ -> \\phiAgain{foo:2} )\\Big\\} \\leadsto_{\\nameref{r:stay}}" + , " \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{foo:2} ]]\\Big\\}{.}" , "\\end{phiquation}" ] ] @@ -446,12 +490,12 @@ ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress"] [ unlines [ "\\begin{phiquation}" - , "\\Big\\{[[ |x| -> ?, |y| -> |x| ]]( |x| -> [[ D> 42- ]] ).|y|\\Big\\} \\leadsto_{\\nameref{r:copy}}" - , " \\leadsto \\Big\\{\\phiMeet{1}{ [[ |x| -> [[ D> 42- ]], |y| -> |x| ]] }.|y|\\Big\\} \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\Big\\{\\phiAgain{1}.|x|( ^ -> \\phiAgain{1} )\\Big\\} \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\Big\\{[[ D> 42- ]]( ^ -> \\phiAgain{1}, ^ -> \\phiAgain{1} )\\Big\\} \\leadsto_{\\nameref{r:copy}}" - , " \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{1} ]]( ^ -> \\phiAgain{1} )\\Big\\} \\leadsto_{\\nameref{r:stay}}" - , " \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{1} ]]\\Big\\}{.}" + , "\\Big\\{[[ |x| -> ?, |y| -> |x| ]]( |x| -> \\phiMeet{1}{ [[ D> 42- ]] } ).|y|\\Big\\} \\leadsto_{\\nameref{r:copy}}" + , " \\leadsto \\Big\\{\\phiMeet{2}{ [[ |x| -> \\phiAgain{1}, |y| -> |x| ]] }.|y|\\Big\\} \\leadsto_{\\nameref{r:dot}}" + , " \\leadsto \\Big\\{\\phiAgain{2}.|x|( ^ -> \\phiAgain{2} )\\Big\\} \\leadsto_{\\nameref{r:dot}}" + , " \\leadsto \\Big\\{\\phiAgain{1}( ^ -> \\phiAgain{2}, ^ -> \\phiAgain{2} )\\Big\\} \\leadsto_{\\nameref{r:copy}}" + , " \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{2} ]]( ^ -> \\phiAgain{2} )\\Big\\} \\leadsto_{\\nameref{r:stay}}" + , " \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{2} ]]\\Big\\}{.}" , "\\end{phiquation}" ] ] @@ -469,6 +513,73 @@ ] ] + it "should not meet expression with high --meet-popularity" $ + withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]] ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $ + testCLISucceeded + ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet", "--meet-popularity=70"] + [ unlines + [ "\\begin{phiquation}" + , "\\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]]( |y| -> [[ |t| -> 42 ]] ) ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:copy}}" + , " \\leadsto \\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:stop}}" + , " \\leadsto \\Big\\{[[ |ex| -> T ]]\\Big\\}{.}" + , "\\end{phiquation}" + ] + ] + + it "meets with --meet-length=32" $ + withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]] ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $ + testCLISucceeded + ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet", "--meet-length=32"] + [ unlines + [ "\\begin{phiquation}" + , "\\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]]( |y| -> [[ |t| -> 42 ]] ) ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:copy}}" + , " \\leadsto \\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:stop}}" + , " \\leadsto \\Big\\{[[ |ex| -> T ]]\\Big\\}{.}" + , "\\end{phiquation}" + ] + ] + + it "focuses expression in latex with sequence" $ + withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]] ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $ + testCLISucceeded + ["rewrite", "--normalize", "--sequence", "--flat", "--output=latex", "--sweet", "--focus=Q.ex"] + [ unlines + [ "\\begin{phiquation}" + , "[[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]]( |y| -> [[ |t| -> 42 ]] ) ]].|i| \\leadsto_{\\nameref{r:copy}}" + , " \\leadsto [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]].|i| \\leadsto_{\\nameref{r:stop}}" + , " \\leadsto T{.}" + , "\\end{phiquation}" + ] + ] + + it "focuses expression in latex without sequence" $ + withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]] ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $ + testCLISucceeded + ["rewrite", "--normalize", "--flat", "--output=latex", "--sweet", "--focus=Q.ex"] + [ unlines + [ "\\begin{phiquation}" + , "T{.}" + , "\\end{phiquation}" + ] + ] + + it "focuses expression in phi without sequence" $ + withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]] ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $ + testCLISucceeded + ["rewrite", "--normalize", "--flat", "--output=phi", "--sweet", "--focus=Q.ex"] + ["⊥"] + + it "focuses expression in phi with sequence" $ + withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]] ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $ + testCLISucceeded + ["rewrite", "--normalize", "--sequence", "--flat", "--output=phi", "--sweet", "--focus=Q.ex"] + [ unlines + [ "⟦ x ↦ ⟦ y ↦ ∅, k ↦ ⟦ t ↦ 42 ⟧ ⟧( y ↦ ⟦ t ↦ 42 ⟧ ) ⟧.i" + , "⟦ x ↦ ⟦ y ↦ ⟦ t ↦ 42 ⟧, k ↦ ⟦ t ↦ 42 ⟧ ⟧ ⟧.i" + , "⊥" + ] + ] + it "prints input as listing in XMIR" $ withStdin "{[[ app -> [[]] ]]}" $ testCLISucceeded @@ -608,7 +719,7 @@ ["rewrite", "--log-level=debug", "--log-lines=4", "--normalize"] [ intercalate "\n" - [ "[DEBUG]: Applied 'COPY' (20 nodes -> 17 nodes)" + [ "[DEBUG]: Applied 'COPY' (44 nodes -> 39 nodes)" , "⟦" , " x ↦ ⟦" , " y ↦ 5" diff --git a/test/LaTeXSpec.hs b/test/LaTeXSpec.hs --- a/test/LaTeXSpec.hs +++ b/test/LaTeXSpec.hs @@ -14,7 +14,7 @@ spec :: Spec spec = describe "meet program in program" $ - Control.Monad.forM_ + forM_ [ ("Q.x.y", "{Q.x.y}", "{[[ x -> Q.x.y ]]}", ["Q.x.y"]) , ("Q.x.y twice", "{Q.x.y}", "{[[ x -> Q.x.y, y -> Q.x.y.z ]]}", ["Q.x.y", "Q.x.y"]) , ("Q.x.y.z.a and Q.x.y", "{Q.x.y.z.a}", "{[[ x -> Q.x.y, y -> Q.x.y.z ]]}", ["Q.x.y.z", "Q.x.y", "Q.x.y"]) @@ -26,5 +26,5 @@ ptn <- parseProgramThrows first tgt <- parseProgramThrows second res <- traverse parseExpressionThrows exprs - meetInProgram ptn tgt `shouldBe` res + meetInProgram ptn 4 tgt `shouldBe` res )