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.52 +cabal install --overwrite-policy=always phino-0.0.0.53 phino --version ``` @@ -217,7 +217,7 @@ ## Explain (under development) -You can _explain_ rewriting rule by printing them in [LaTeX][latex]format: +You can _explain_ rewriting rule by printing them in [LaTeX][latex] format: ```bash $ phino explain --rule=my-rule.yaml @@ -360,8 +360,7 @@ before sending us your pull request please make sure all your tests pass: ```bash -cabal build all -make +make all ``` To generate a local coverage report for development, run: 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.53 +version: 0.0.0.54 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at diff --git a/src/AST.hs b/src/AST.hs --- a/src/AST.hs +++ b/src/AST.hs @@ -22,8 +22,8 @@ | ExDispatch Expression Attribute -- expr.attr | ExMeta String -- !e | ExMetaTail Expression String -- expr * !t - | ExPhiMeet Int Expression - | ExPhiAgain Int Expression + | ExPhiMeet (Maybe String) Int Expression + | ExPhiAgain (Maybe String) Int Expression deriving (Eq, Ord, Show, Generic) data Binding diff --git a/src/CLI.hs b/src/CLI.hs --- a/src/CLI.hs +++ b/src/CLI.hs @@ -14,7 +14,7 @@ import Condition (parseConditionThrows) import Control.Exception (Exception (displayException), SomeException, handle, throw, throwIO) import Control.Exception.Base -import Control.Monad (unless, when, (>=>)) +import Control.Monad (forM_, unless, when, (>=>)) import Data.Char (toLower, toUpper) import Data.Foldable (for_) import qualified Data.Foldable @@ -57,6 +57,7 @@ , compress :: Bool , expression :: Maybe String , label :: Maybe String + , meetPrefix :: Maybe String , outputFormat :: IOFormat } @@ -106,6 +107,7 @@ , show' :: [String] , expression :: Maybe String , label :: Maybe String + , meetPrefix :: Maybe String , stepsDir :: Maybe FilePath , inputFile :: Maybe FilePath } @@ -144,6 +146,7 @@ , show' :: [String] , expression :: Maybe String , label :: Maybe String + , meetPrefix :: Maybe String , targetFile :: Maybe FilePath , stepsDir :: Maybe FilePath , inputFile :: Maybe FilePath @@ -254,6 +257,9 @@ 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")) @@ -340,6 +346,7 @@ <*> optShow <*> optExpression <*> optLabel + <*> optMeetPrefix <*> optStepsDir <*> argInputFile ) @@ -379,6 +386,7 @@ <*> optShow <*> optExpression <*> optLabel + <*> optMeetPrefix <*> optTarget <*> optStepsDir <*> argInputFile @@ -464,7 +472,7 @@ 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 outputFormat + 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) @@ -483,9 +491,14 @@ (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, compress, expression, label) + validateLatexOptions + outputFormat + [(nonumber, "nonumber"), (compress, "compress")] + [(expression, "expression"), (label, "label"), (meetPrefix, "meet-prefix")] validateMust' must - validateXmirOptions outputFormat omitListing omitComments + validateXmirOptions + outputFormat + [(omitListing, "omit-listing"), (omitComments, "omit-comments")] output :: Maybe FilePath -> String -> IO () output target prog = case (inPlace, target, inputFile) of (True, _, Just file) -> do @@ -514,7 +527,7 @@ included <- expressionsToFilter "show" show' input <- readInput inputFile prog <- parseProgram input inputFormat - let printCtx = PrintProgCtx sugarType flat defaultXmirContext nonumber compress expression label outputFormat + let printCtx = PrintProgCtx sugarType flat defaultXmirContext nonumber compress expression label meetPrefix outputFormat _hide = (`F.exclude` excluded) _show = (`F.include` included) (maybeBytes, seq) <- dataize prog (context prog printCtx) @@ -523,8 +536,13 @@ where validateOpts :: IO () validateOpts = do - validateLatexOptions (outputFormat, nonumber, compress, expression, label) - validateXmirOptions outputFormat omitListing omitComments + 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") context :: Program -> PrintProgramContext -> DataizeContext context program ctx = @@ -553,7 +571,7 @@ 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 outputFormat + printProgCtx = PrintProgCtx sugarType flat xmirCtx False False Nothing Nothing Nothing outputFormat prog' <- printProgram printProgCtx prog output targetFile prog' where @@ -562,7 +580,7 @@ when (null inputs) (throwIO (InvalidCLIArguments "At least one input file must be specified for 'merge' command")) - validateXmirOptions outputFormat omitListing omitComments + validateXmirOptions outputFormat [(omitListing, "omit-listing"), (omitComments, "omit-comments")] CmdMatch OptsMatch{..} -> do input <- readInput inputFile prog <- parseProgram input PHI @@ -607,36 +625,30 @@ ) -- Validate LaTeX options -validateLatexOptions :: (IOFormat, Bool, Bool, Maybe String, Maybe String) -> IO () -validateLatexOptions (LATEX, _, _, _, _) = pure () -validateLatexOptions (_, nonumber, compress, expression, label) = do - when - nonumber - (invalidCLIArguments "The --nonumber option can stay together with --output=latex only") - when - compress - (invalidCLIArguments "The --compress option can stay together with --output=latex only") - when - (isJust expression) - (invalidCLIArguments "The --expression option can stay together with --output=latex only") - when - (isJust label) - (invalidCLIArguments "The --label option can stay together with --output=latex only") +validateLatexOptions :: IOFormat -> [(Bool, String)] -> [(Maybe String, String)] -> IO () +validateLatexOptions LATEX _ _ = pure () +validateLatexOptions _ bools maybes = do + let (bools', opts) = unzip bools + msg = "The --%s option can stay together with --output=latex only" + validateBoolOpts (zip bools' (map (printf msg) opts)) + forM_ + maybes + (\(maybe', opt) -> when (isJust maybe') (invalidCLIArguments (printf msg opt))) -- Validate 'must' option validateMust' :: Must -> IO () validateMust' must = for_ (validateMust must) invalidCLIArguments -- Validate options for output to XMIR -validateXmirOptions :: IOFormat -> Bool -> Bool -> IO () -validateXmirOptions outputFormat omitListing omitComments = do - when - (outputFormat /= XMIR && omitListing) - (invalidCLIArguments "--omit-listing can be used only with --output=xmir") - when - (outputFormat /= XMIR && omitComments) - (invalidCLIArguments "--omit-comments can be used only with --output=xmir") +validateXmirOptions :: IOFormat -> [(Bool, String)] -> IO () +validateXmirOptions XMIR _ = pure () +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 @@ -656,7 +668,7 @@ printRewrittens :: PrintProgramContext -> [Rewritten] -> IO String printRewrittens ctx@PrintProgCtx{..} rewrittens - | outputFormat == LATEX = pure (rewrittensToLatex rewrittens (LatexContext sugar line nonumber compress expression label)) + | outputFormat == LATEX = pure (rewrittensToLatex rewrittens (LatexContext sugar line nonumber compress expression label meetPrefix)) | otherwise = mapM (printProgram ctx . fst) rewrittens <&> intercalate "\n" -- Convert program to corresponding String format @@ -664,7 +676,7 @@ 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)) + LATEX -> pure (programToLaTeX prog (LatexContext sugar line nonumber compress expression label meetPrefix)) -- Get rules for rewriting depending on provided flags getRules :: Bool -> Bool -> [FilePath] -> IO [Y.Rule] diff --git a/src/CST.hs b/src/CST.hs --- a/src/CST.hs +++ b/src/CST.hs @@ -155,8 +155,8 @@ | EX_NUMBER {num :: Either Int Double, tab :: TAB, rhos :: [Binding]} | EX_META {meta :: META} | EX_META_TAIL {expr :: EXPRESSION, meta :: META} - | EX_PHI_MEET {idx :: Int, expr :: EXPRESSION} - | EX_PHI_AGAIN {idx :: Int, expr :: EXPRESSION} + | EX_PHI_MEET {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION} + | EX_PHI_AGAIN {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION} deriving (Eq, Show) data ATTRIBUTE @@ -192,8 +192,8 @@ toCST ExTermination _ _ = EX_TERMINATION DEAD toCST (ExFormation [BiVoid AtRho]) _ eol = toCST (ExFormation []) 0 eol toCST (ExFormation []) _ _ = EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY NO_TAB) NO_EOL NO_TAB RSB - toCST (ExPhiMeet idx expr) tabs eol = EX_PHI_MEET idx (toCST expr tabs eol) - toCST (ExPhiAgain idx expr) tabs eol = EX_PHI_AGAIN idx (toCST expr tabs eol) + toCST (ExPhiMeet prefix idx expr) tabs eol = EX_PHI_MEET prefix idx (toCST expr tabs eol) + toCST (ExPhiAgain prefix idx expr) tabs eol = EX_PHI_AGAIN prefix idx (toCST expr tabs eol) toCST (ExFormation bds) tabs eol = let next = tabs + 1 bds' = toCST (withoutLastVoidRho bds) next eol :: BINDING diff --git a/src/Encoding.hs b/src/Encoding.hs --- a/src/Encoding.hs +++ b/src/Encoding.hs @@ -34,8 +34,8 @@ 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_PHI_MEET{..} = EX_PHI_MEET idx (toASCII expr) - toASCII EX_PHI_AGAIN{..} = EX_PHI_AGAIN idx (toASCII expr) + 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 instance ToASCII APP_BINDING where diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -37,10 +37,11 @@ , compress :: Bool , expression :: Maybe String , label :: Maybe String + , meetPrefix :: Maybe String } defaultLatexContext :: LatexContext -defaultLatexContext = LatexContext SWEET MULTILINE False False Nothing Nothing +defaultLatexContext = LatexContext SWEET MULTILINE False False Nothing Nothing Nothing meetInProgram :: Program -> Program -> [Expression] meetInProgram (Program expr) = meetInExpression expr @@ -57,8 +58,8 @@ meetInExpression (ExDispatch ExTermination _) _ = [] meetInExpression (DataString _) _ = [] meetInExpression (DataNumber _) _ = [] - meetInExpression (ExPhiMeet _ _) _ = [] - meetInExpression (ExPhiAgain _ _) _ = [] + meetInExpression (ExPhiMeet{}) _ = [] + meetInExpression (ExPhiAgain{}) _ = [] meetInExpression expr prog = map (const expr) (matchProgram expr prog) ++ case expr of ExDispatch exp _ -> meetInExpression exp prog @@ -76,8 +77,8 @@ 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. -} -meetInPrograms :: [Program] -> [Program] -meetInPrograms = meetInPrograms' 1 +meetInPrograms :: Maybe String -> [Program] -> [Program] +meetInPrograms prefix = meetInPrograms' 1 where meetInPrograms' :: Int -> [Program] -> [Program] meetInPrograms' _ [prog] = [prog] @@ -99,8 +100,8 @@ Just expr -> let met' = map (filter (== expr)) met substs = matchProgram expr first - prog = replaceProgram (first, map (const expr) substs, map (const (ExPhiMeet idx)) substs) - rest' = zipWith (\prgm exprs -> replaceProgram (prgm, exprs, map (const (ExPhiAgain idx)) exprs)) rest met' + prog = replaceProgram (first, map (const expr) substs, map (const (ExPhiMeet prefix idx)) substs) + rest' = zipWith (\prgm exprs -> replaceProgram (prgm, exprs, map (const (ExPhiAgain prefix 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' @@ -118,7 +119,7 @@ rewrittensToLatex rewrittens ctx@LatexContext{..} = let equation = phiquation ctx (progs, rules) = unzip rewrittens - rewrittens' = if compress then zip (meetInPrograms progs) rules else 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 @@ -165,8 +166,8 @@ toLaTeX EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toLaTeX expr) eol tab (toLaTeX taus) eol' tab' indent toLaTeX EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toLaTeX expr) eol tab (toLaTeX args) eol' tab' indent toLaTeX EX_DISPATCH{..} = EX_DISPATCH (toLaTeX expr) (toLaTeX attr) - toLaTeX EX_PHI_MEET{..} = EX_PHI_MEET idx (toLaTeX expr) - toLaTeX EX_PHI_AGAIN{..} = EX_PHI_AGAIN idx (toLaTeX expr) + toLaTeX EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toLaTeX expr) + toLaTeX EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toLaTeX expr) toLaTeX expr = expr instance ToLaTeX ATTRIBUTE where diff --git a/src/Lining.hs b/src/Lining.hs --- a/src/Lining.hs +++ b/src/Lining.hs @@ -29,8 +29,8 @@ toSingleLine EX_APPLICATION{..} = EX_APPLICATION (toSingleLine expr) NO_EOL TAB' (toSingleLine tau) NO_EOL TAB' indent toSingleLine EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toSingleLine expr) NO_EOL TAB' (toSingleLine taus) NO_EOL TAB' indent toSingleLine EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toSingleLine expr) NO_EOL TAB' (toSingleLine args) NO_EOL TAB' indent - toSingleLine EX_PHI_MEET{..} = EX_PHI_MEET idx (toSingleLine expr) - toSingleLine EX_PHI_AGAIN{..} = EX_PHI_AGAIN idx (toSingleLine expr) + toSingleLine EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSingleLine expr) + toSingleLine EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toSingleLine expr) toSingleLine expr = expr instance ToSingleLine APP_BINDING where diff --git a/src/Matcher.hs b/src/Matcher.hs --- a/src/Matcher.hs +++ b/src/Matcher.hs @@ -139,11 +139,11 @@ matchExpression (ExMetaTail exp meta) tgt scope = case tailExpressions exp tgt scope of ([], _) -> [] (substs, tails) -> combineMany substs [substSingle meta (MvTail tails)] -matchExpression (ExPhiAgain idx expr) (ExPhiAgain idx' expr') scope - | idx == idx' = matchExpression expr expr' scope +matchExpression (ExPhiAgain prefix idx expr) (ExPhiAgain prefix' idx' expr') scope + | prefix == prefix' && idx == idx' = matchExpression expr expr' scope | otherwise = [] -matchExpression (ExPhiMeet idx expr) (ExPhiMeet idx' expr') scope - | idx == idx' = matchExpression expr expr' scope +matchExpression (ExPhiMeet prefix idx expr) (ExPhiMeet prefix' idx' expr') scope + | prefix == prefix' && idx == idx' = matchExpression expr expr' scope | otherwise = [] matchExpression _ _ _ = [] diff --git a/src/Render.hs b/src/Render.hs --- a/src/Render.hs +++ b/src/Render.hs @@ -10,6 +10,7 @@ import AST import CST import Data.List +import Data.Maybe (fromMaybe) class Render a where render :: a -> String @@ -176,8 +177,8 @@ render EX_NUMBER{..} = either show show num render EX_META{..} = render meta render EX_META_TAIL{..} = render expr <> " * " <> render meta - render EX_PHI_MEET{..} = "\\phiMeet{" <> render idx <> "}{" <> render expr <> "}" - render EX_PHI_AGAIN{..} = "\\phiAgain{" <> render idx <> "}" + render EX_PHI_MEET{..} = "\\phiMeet{" <> maybe "" (++ ":") prefix <> render idx <> "}{" <> render expr <> "}" + render EX_PHI_AGAIN{..} = "\\phiAgain{" <> maybe "" (++ ":") prefix <> render idx <> "}" instance Render ATTRIBUTE where render AT_LABEL{..} = label diff --git a/src/Sugar.hs b/src/Sugar.hs --- a/src/Sugar.hs +++ b/src/Sugar.hs @@ -100,8 +100,8 @@ (toCST (ExFormation [BiDelta (strToBts str)]) (indent + 2) EOL) tab rhos - toSalty EX_PHI_MEET{..} = EX_PHI_MEET idx (toSalty expr) - toSalty EX_PHI_AGAIN{..} = EX_PHI_AGAIN idx (toSalty expr) + toSalty EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSalty expr) + toSalty EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toSalty expr) toSalty expr = expr saltifyPrimitive :: EXPRESSION -> EXPRESSION -> EXPRESSION -> TAB -> [Binding] -> EXPRESSION diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -214,6 +214,12 @@ ["rewrite", "--compress", "--output=phi"] ["--compress option can stay together with --output=latex only"] + it "with --meet-prefix and --output != latex" $ + withStdin "{[[]]}" $ + testCLIFailed + ["rewrite", "--meet-prefix=foo", "--output=phi"] + ["--meet-prefix option can stay together with --output=latex only"] + it "with wrong --hide option" $ withStdin "{[[]]}" $ testCLIFailed @@ -409,6 +415,22 @@ , "\\Big\\{[[ |x| -> \"foo\" ]]\\Big\\} \\leadsto_{\\nameref{r:first}}" , " \\leadsto \\Big\\{Q.|x|( |y| -> \"foo\" )\\Big\\} \\leadsto_{\\nameref{r:second}}" , " \\leadsto \\Big\\{[[ |x| -> \"foo\" ]]\\Big\\}." + , "\\end{phiquation}" + ] + ] + + it "prints meet prefix with --meet-prefix=foo in LaTeX" $ + withStdin "{[[ x -> ?, y -> $.x ]](x -> [[ D> 42- ]]).y}" $ + testCLISucceeded + ["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\\}." , "\\end{phiquation}" ] ]