packages feed

phino 0.0.0.53 → 0.0.0.54

raw patch · 12 files changed

+102/−67 lines, 12 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

+ CST: [prefix] :: EXPRESSION -> Maybe String
+ LaTeX: [meetPrefix] :: LatexContext -> Maybe String
- AST: ExPhiAgain :: Int -> Expression -> Expression
+ AST: ExPhiAgain :: Maybe String -> Int -> Expression -> Expression
- AST: ExPhiMeet :: Int -> Expression -> Expression
+ AST: ExPhiMeet :: Maybe String -> Int -> Expression -> Expression
- CST: EX_PHI_AGAIN :: Int -> EXPRESSION -> EXPRESSION
+ CST: EX_PHI_AGAIN :: Maybe String -> Int -> EXPRESSION -> EXPRESSION
- CST: EX_PHI_MEET :: Int -> EXPRESSION -> EXPRESSION
+ CST: EX_PHI_MEET :: Maybe String -> Int -> EXPRESSION -> EXPRESSION
- LaTeX: LatexContext :: SugarType -> LineFormat -> Bool -> Bool -> Maybe String -> Maybe String -> LatexContext
+ LaTeX: LatexContext :: SugarType -> LineFormat -> Bool -> Bool -> Maybe String -> Maybe String -> Maybe String -> LatexContext
- LaTeX: meetInPrograms :: [Program] -> [Program]
+ LaTeX: meetInPrograms :: Maybe String -> [Program] -> [Program]

Files

README.md view
@@ -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:
phino.cabal view
@@ -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 <https://github.com/objectionary/phino#readme>
src/AST.hs view
@@ -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
src/CLI.hs view
@@ -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]
src/CST.hs view
@@ -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
src/Encoding.hs view
@@ -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
src/LaTeX.hs view
@@ -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
src/Lining.hs view
@@ -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
src/Matcher.hs view
@@ -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 _ _ _ = [] 
src/Render.hs view
@@ -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
src/Sugar.hs view
@@ -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
test/CLISpec.hs view
@@ -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}"               ]           ]