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.65 +cabal install --overwrite-policy=always phino-0.0.0.66 phino --version ``` @@ -44,7 +44,8 @@ Download paths are: -* Ubuntu: +* Ubuntu 22.04: +* Ubuntu 24.04: * MacOS (ARM): * MacOS (Intel): * Windows: @@ -224,7 +225,7 @@ ```bnfc Rule: - name: String? + name: String pattern: String result: String when: Condition? # predicate, works with substitutions before extension 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.66 +version: 0.0.0.67 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at @@ -89,7 +89,7 @@ filepath >=1.4.200 && <1.6, megaparsec >=9.5 && <9.8, optparse-applicative >=0.18 && <0.20, - random >=1.2 && <1.3, + random >=1.2 && <1.4, regex-pcre-builtin >=0.95.2 && <0.96, scientific >=0.3.7 && <0.4, text >=2.0.2 && <2.2, diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs --- a/src/CLI/Parsers.hs +++ b/src/CLI/Parsers.hs @@ -133,6 +133,9 @@ 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}")) +optBreakpoint :: Parser (Maybe FilePath) +optBreakpoint = optional (strOption (long "breakpoint" <> metavar "FILE" <> help "The name of the first unmatched rule which leads to stopping entire rewriting process and returning original program")) + optHide :: Parser [String] optHide = many @@ -192,6 +195,17 @@ optLineFormat' :: Parser LineFormat optLineFormat' = flag MULTILINE SINGLELINE (long "flat" <> help "Print result 𝜑-program in one line") +optMust :: Parser Must +optMust = + 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 + ) + optOmitListing :: Parser Bool optOmitListing = switch (long "omit-listing" <> help "Omit full program listing in XMIR output") @@ -260,14 +274,7 @@ <*> 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 - ) + <*> optMust <*> optNormalize <*> optShuffle <*> optOmitListing @@ -291,6 +298,7 @@ <*> optExpression <*> optLabel <*> optMeetPrefix + <*> optBreakpoint <*> optTarget <*> optStepsDir <*> argInputFile diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -14,6 +14,7 @@ import Condition (parseConditionThrows) import Control.Exception import Control.Monad (unless, when) +import Data.List (intercalate) import qualified Data.List.NonEmpty as NE import Data.Maybe (fromJust, isJust, isNothing) import Dataize @@ -39,10 +40,11 @@ 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 + validateBreakpoint _breakpoint rules + input <- readInput _inputFile program <- parseProgram input _inputFormat + logDebug (printf "Amount of rewriting cycles across all the rules: %d, per rule: %d" _maxCycles _maxDepth) let listing = case (rules, _inputFormat, _outputFormat) of ([], XMIR, XMIR) -> (\_ -> escapeXML input) ([], _, _) -> const input @@ -70,6 +72,13 @@ [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")] validateMust' _must validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus + validateBreakpoint :: Maybe String -> [Y.Rule] -> IO () + validateBreakpoint Nothing _ = pure () + validateBreakpoint (Just rule) rules = + let names = map Y.name rules + in unless + (rule `elem` names) + (invalidCLIArguments (printf "The rule '%s' provided in '--breakpoint' option is absent across given rewriting rules: %s" rule (intercalate ", " names))) output :: Maybe FilePath -> String -> IO () output target prog = case (_inPlace, target, _inputFile) of (True, _, Just file) -> do @@ -86,7 +95,7 @@ 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) + context loc ctx = RewriteContext loc _maxDepth _maxCycles _depthSensitive buildTerm _must _breakpoint (saveStepFunc _stepsDir ctx) printProgCtx :: XmirContext -> Expression -> PrintProgramContext printProgCtx xmirCtx focus = PrintProgCtx @@ -205,8 +214,8 @@ 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" + then throwIO EmptySubstsOnMatch 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 + rule ptn cnd = Y.Rule "custom" Nothing ptn ExGlobal cnd Nothing Nothing diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs --- a/src/CLI/Types.hs +++ b/src/CLI/Types.hs @@ -37,6 +37,7 @@ | CouldNotReadFromStdin String | CouldNotDataize | CouldNotPrintExpressionInXMIR + | EmptySubstsOnMatch deriving (Exception) instance Show CmdException where @@ -44,6 +45,7 @@ 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" + show EmptySubstsOnMatch = "Provided pattern was not matched, no substitutions are built" data Command = CmdRewrite OptsRewrite @@ -131,6 +133,7 @@ , _expression :: Maybe String , _label :: Maybe String , _meetPrefix :: Maybe String + , _breakpoint :: Maybe String , _targetFile :: Maybe FilePath , _stepsDir :: Maybe FilePath , _inputFile :: Maybe FilePath diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -50,6 +50,7 @@ _depthSensitive _buildTerm MtDisabled + Nothing _saveStep maybeBinding :: (Binding -> Bool) -> [Binding] -> (Maybe Binding, [Binding]) diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -22,7 +22,7 @@ import AST import CST import Data.List (intercalate, nub) -import Data.Maybe (fromMaybe, isJust) +import Data.Maybe (isJust) import Encoding import Lining import Locator (locatedExpression) @@ -320,7 +320,7 @@ explainRule rule = intercalate "\n " - [ "\\trrule{" ++ fromMaybe "unknown" (Y.name rule) ++ "}" + [ "\\trrule{" ++ 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)) diff --git a/src/Rewriter.hs b/src/Rewriter.hs --- a/src/Rewriter.hs +++ b/src/Rewriter.hs @@ -15,7 +15,6 @@ import Control.Exception (Exception, throwIO) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE -import Data.Maybe (fromMaybe) import qualified Data.Set as Set import Deps import Locator (locatedExpression, withLocatedExpression) @@ -29,7 +28,7 @@ import Text.Printf (printf) import qualified Yaml as Y -type RewriteState = (NonEmpty Rewritten, Set.Set Expression) +type RewriteState = (NonEmpty Rewritten, Set.Set Expression, Bool) type Rewritten = (Program, Maybe String) @@ -46,6 +45,7 @@ , _depthSensitive :: Bool , _buildTerm :: BuildTermFunc , _must :: Must + , _breakpoint :: Maybe String , _saveStep :: SaveStepFunc } @@ -129,19 +129,23 @@ hasMetaBindings = foldl (\acc bd -> acc || isMetaBinding bd) False tryBuildAndReplaceFast state _ = buildAndReplace' state replaceExpression --- The function returns tuple (X, Y) where +-- The function returns tuple (X, Y, Z) where -- - X is sequence of programs; -- - Y is Set of unique programs after each rule application. It allows to stop the rewriting if we're getting -- into loop and get back to program which we've already got before +-- - Z is boolean flag which tells us if we reach breakpoint. If unmatched rule is equal to breakpoint rule - entire +-- rewriting must be stopped and original program must be returned rewrite' :: RewriteState -> [Y.Rule] -> Int -> RewriteContext -> IO RewriteState rewrite' state [] _ _ = pure state rewrite' state (rule : rest) iteration ctx@RewriteContext{..} = do state' <- _rewrite state 1 - rewrite' state' rest iteration ctx + case state' of + (_, _, True) -> pure state' + _ -> rewrite' state' rest iteration ctx where _rewrite :: RewriteState -> Int -> IO RewriteState - _rewrite (_rewrittens@((program, _) :| _), _unique) _count = - let ruleName = fromMaybe "unknown" (Y.name rule) + _rewrite (_rewrittens@((program, _) :| _), _unique, _) _count = + let ruleName = Y.name rule ptn = Y.pattern rule res = Y.result rule in if _count - 1 == _maxDepth @@ -149,22 +153,25 @@ logDebug (printf "Max amount of rewriting cycles (%d) for rule '%s' has been reached, rewriting is stopped" _maxDepth ruleName) if _depthSensitive then throwIO (StoppedOnLimit "max-depth" _maxDepth) - else pure (_rewrittens, _unique) + else pure (_rewrittens, _unique, False) else do logDebug (printf "Starting rewriting cycle for rule '%s': %d out of %d" ruleName _count _maxDepth) expression <- locatedExpression _locator program - matched <- R.matchExpressionWithRule expression rule (RuleContext _buildTerm) - if null matched - then do + R.matchExpressionWithRule expression rule (RuleContext _buildTerm) >>= \case + [] -> do logDebug (printf "Rule '%s' does not match, rewriting is stopped" ruleName) - pure (_rewrittens, _unique) - else do + if _breakpoint == Just ruleName + then do + logDebug (printf "Rule '%s' is a breakpoint, dropping down all the previous rewritings..." ruleName) + pure (_rewrittens, _unique, True) + else pure (_rewrittens, _unique, False) + matched -> do logDebug (printf "Rule '%s' has been matched, applying..." ruleName) expr <- tryBuildAndReplaceFast (expression, ptn, res, matched) (ReplaceCtx _maxDepth) if expression == expr then do logDebug (printf "Applied '%s', no changes made" ruleName) - pure (_rewrittens, _unique) + pure (_rewrittens, _unique, False) else if Set.member expr _unique then throwIO (LoopingRewriting (printExpression expr) ruleName _count) @@ -179,21 +186,21 @@ ) prog <- withLocatedExpression _locator expr program _saveStep prog (((iteration - 1) * _maxDepth) + _count) - _rewrite (leadsTo prog, Set.insert expr _unique) (_count + 1) + _rewrite (leadsTo prog, Set.insert expr _unique, False) (_count + 1) where leadsTo :: Program -> NonEmpty Rewritten leadsTo _prog = let (program, _) :| rest = _rewrittens - in (_prog, Nothing) :| (program, Just (fromMaybe "unknown" (Y.name rule))) : rest + in (_prog, Nothing) :| (program, Just (Y.name rule)) : rest -- Rewrite program by provided locator from RewriteContext rewrite :: Program -> [Y.Rule] -> RewriteContext -> IO Rewrittens rewrite prog rules ctx@RewriteContext{..} = do - (rewrittens, exceeded) <- _rewrite ((prog, Nothing) :| [], Set.empty) 0 + (rewrittens, exceeded) <- _rewrite ((prog, Nothing) :| [], Set.empty, False) 0 pure (NE.reverse rewrittens, exceeded) where _rewrite :: RewriteState -> Int -> IO Rewrittens - _rewrite state@(rewrittens@((program, _) :| _), _) count + _rewrite state@(rewrittens@((program, _) :| _), _, _) 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) @@ -202,11 +209,13 @@ else pure (rewrittens, True) | otherwise = do logDebug (printf "Starting rewriting cycle for all rules: %d out of %d" count _maxCycles) - state'@(rewrittens'@((program', _) :| _), _) <- rewrite' state rules count ctx - if program' == program - then do - logDebug "Rewriting is stopped since it has no effect" - if not (inRange _must count) - then throwIO (MustBeGoing _must count) - else pure (rewrittens', False) - else _rewrite state' (count + 1) + rewrite' state rules count ctx >>= \case + (_, _, True) -> pure ((prog, Nothing) :| [], False) -- breakpoint, return original program + state'@(rewrittens'@((program', _) :| _), _, False) -> + if program' == program + then do + logDebug "Rewriting is stopped since it has no effect" + if not (inRange _must count) + then throwIO (MustBeGoing _must count) + else pure (rewrittens', False) + else _rewrite state' (count + 1) diff --git a/src/Rule.hs b/src/Rule.hs --- a/src/Rule.hs +++ b/src/Rule.hs @@ -19,7 +19,7 @@ import qualified Data.ByteString.Char8 as B import Data.Foldable (foldlM) import qualified Data.Map.Strict as M -import Data.Maybe (catMaybes, fromMaybe) +import Data.Maybe (catMaybes) import Deps (BuildTermFunc, Term (..)) import GHC.IO (unsafePerformIO) import Logger (logDebug) @@ -280,7 +280,7 @@ matchExpressionWithRule expr rule ctx = let ptn = Y.pattern rule matched = matchExpression ptn expr - name = fromMaybe "unknown" (Y.name rule) + name = Y.name rule in if null matched then do logDebug (printf "Pattern from rule '%s' was not matched:\n%s" name (printExpression' ptn logPrintConfig)) diff --git a/src/Yaml.hs b/src/Yaml.hs --- a/src/Yaml.hs +++ b/src/Yaml.hs @@ -171,7 +171,7 @@ deriving (Generic, Show) data Rule = Rule - { name :: Maybe String + { name :: String , description :: Maybe String , pattern :: Expression , result :: Expression diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -277,6 +277,12 @@ ["rewrite", "--margin=-1"] ["[ERROR]"] + it "with --breakpoint which does not exist across the rules" $ + withStdin "" $ + testCLIFailed + ["rewrite", "--breakpoint=hello", "--normalize"] + ["[ERROR]"] + it "prints help" $ testCLISucceeded ["rewrite", "--help"] @@ -755,6 +761,15 @@ ["rewrite", "--sweet", "--flat", "--locator=Q.ex", "--normalize"] ["{⟦ ex ↦ ⟦ x ↦ 5 ⟧, abc ↦ ⟦ x ↦ ∅ ⟧( x ↦ 5 ) ⟧}"] + it "returns original program on --breakpoint" $ + withStdin "{[[ x -> ?, y -> $.x ]](x -> [[ D> 42- ]]).y}" $ + testCLISucceeded + ["rewrite", "--sweet", "--flat", "--normalize", "--breakpoint=stop", "--log-level=debug"] + [ "Applied 'copy' (30 nodes -> 25 nodes)" + , "Rule 'stop' is a breakpoint, dropping down all the previous rewritings..." + , "{⟦ x ↦ ∅, y ↦ x ⟧( x ↦ ⟦ Δ ⤍ 42- ⟧ ).y}" + ] + describe "dataize" $ do it "prints help" $ testCLISucceeded ["dataize", "--help"] ["Dataize the 𝜑-program"] @@ -1012,3 +1027,9 @@ testCLIFailed ["match", "--pattern=[[!B]]", "--when=hello"] ["[ERROR]: Couldn't parse given condition"] + + it "fails on empty substitutions" $ + withStdin "{Q.x.y}" $ + testCLIFailed + ["match", "--pattern=$.!a"] + ["[ERROR]"] diff --git a/test/RewriterSpec.hs b/test/RewriterSpec.hs --- a/test/RewriterSpec.hs +++ b/test/RewriterSpec.hs @@ -111,6 +111,7 @@ False buildTerm must' + Nothing dontSaveStep ) let (program, _) = NE.last rewrittens