diff --git a/phino.cabal b/phino.cabal --- a/phino.cabal +++ b/phino.cabal @@ -1,7 +1,7 @@ cabal-version: 3.0 name: phino -version: 0.0.0.37 +version: 0.0.0.38 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at diff --git a/src/CLI.hs b/src/CLI.hs --- a/src/CLI.hs +++ b/src/CLI.hs @@ -76,6 +76,7 @@ omitComments :: Bool, must :: Integer, maxDepth :: Integer, + targetFile :: Maybe FilePath, inputFile :: Maybe FilePath } @@ -144,6 +145,7 @@ <|> option auto (long "must" <> metavar "N" <> help "Must-rewrite, stops execution if not exactly N rules applied (default 1 when specified without value, if 0 - flag is disabled)" <> value 0) ) <*> optMaxDepth + <*> optional (strOption (long "target" <> short 't' <> metavar "FILE" <> help "File to save output to")) <*> argInputFile ) @@ -188,8 +190,8 @@ program <- parseProgram input inputFormat rewritten <- rewrite' program rules' (RewriteContext program maxDepth buildTerm must) logDebug (printf "Printing rewritten 𝜑-program as %s" (show outputFormat)) - out <- printProgram rewritten outputFormat printMode - putStrLn out + prog <- printProgram rewritten outputFormat printMode + output prog where getRules :: IO [Y.Rule] getRules = do @@ -221,6 +223,15 @@ printProgram prog XMIR mode = do xmir <- programToXMIR prog (XmirContext omitListing omitComments printMode) pure (printXMIR xmir) + output :: String -> IO () + output prog = case targetFile of + Nothing -> do + logDebug "The option '--target' is not specified, printing to console..." + putStrLn prog + Just file -> do + logDebug (printf "The option '--target' is specified, printing to '%s'..." file) + writeFile file prog + logInfo (printf "The result program was saved in '%s'" file) CmdDataize OptsDataize {..} -> do validateMaxDepth maxDepth input <- readInput inputFile diff --git a/src/Pretty.hs b/src/Pretty.hs --- a/src/Pretty.hs +++ b/src/Pretty.hs @@ -20,12 +20,12 @@ where import Ast +import Data.List (intercalate) import qualified Data.Map.Strict as Map import Matcher +import Misc import Prettyprinter import Prettyprinter.Render.String (renderString) -import Misc -import Data.List (intercalate) import Yaml (ExtraArgument (..)) data PrintMode = SWEET | SALTY @@ -98,6 +98,8 @@ pretty (Formatted (_, BiVoid attr)) = pretty attr <+> prettyArrow <+> pretty "∅" pretty (Formatted (_, BiLambda func)) = pretty "λ" <+> prettyDashedArrow <+> pretty func +-- >>> render (Formatted (SWEET, [BiVoid AtRho])) +-- "" instance {-# OVERLAPPING #-} Pretty (Formatted [Binding]) where pretty (Formatted (SWEET, bds)) = vsep (punctuate comma (excludeVoidRho (\bd -> pretty (Formatted (SWEET, bd))) [] bds)) where @@ -124,11 +126,14 @@ complexApplication (ExApplication expr (BiTau (AtAlpha 0) expr')) = (expr, [BiTau (AtAlpha 0) expr'], [expr']) complexApplication (ExApplication expr tau) = (expr, [tau], []) +-- >>> render (Formatted (SWEET, ExFormation [BiVoid AtRho])) +-- "\10214\10215" instance Pretty (Formatted Expression) where pretty (Formatted (SWEET, ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang"))) = pretty "Φ̇" pretty (Formatted (SWEET, DataString bytes)) = pretty "\"" <> pretty (btsToStr bytes) <> pretty "\"" pretty (Formatted (SWEET, DataNumber bytes)) = either pretty pretty (btsToNum bytes) pretty (Formatted (SWEET, DataObject other bytes)) = pretty (Formatted (SALTY, DataObject other bytes)) + pretty (Formatted (SWEET, ExFormation [BiVoid AtRho])) = pretty "⟦⟧" pretty (Formatted (mode, ExFormation [binding])) = case binding of BiTau _ _ -> vsep [pretty "⟦", indent 2 (pretty (Formatted (mode, binding))), pretty "⟧"] _ -> pretty "⟦" <+> pretty (Formatted (mode, binding)) <+> pretty "⟧" diff --git a/src/Replacer.hs b/src/Replacer.hs --- a/src/Replacer.hs +++ b/src/Replacer.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE RecordWildCards #-} -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com @@ -6,14 +7,43 @@ -- The goal of the module is to traverse though the Program with replacing -- pattern sub expression with target expressions -module Replacer (replaceProgram, replaceProgramThrows) where +module Replacer + ( replaceProgram, + replaceProgramThrows, + replaceProgramFast, + replaceProgramFastThrows, + ReplaceProgramThrowsFunc, + ReplaceProgramFunc, + ReplaceProgramContext (..), + ) +where import Ast import Control.Exception (Exception, throwIO) import Matcher (Tail (TaApplication, TaDispatch)) import Pretty (prettyExpression, prettyProgram) import Text.Printf (printf) +import Data.List (isPrefixOf) +data ReplaceProgramContext = ReplaceProgramContext + { _program :: Program, + _maxDepth :: Integer + } + +data ReplaceExpressionContext = ReplaceExpressionContext + { _expression :: Expression, + _maxDepth :: Integer + } + +updateExpressionContext :: ReplaceExpressionContext -> Expression -> ReplaceExpressionContext +updateExpressionContext ReplaceExpressionContext {..} expr = ReplaceExpressionContext expr _maxDepth + +type ReplaceProgramThrowsFunc = [Expression] -> [Expression] -> ReplaceProgramContext -> IO Program + +type ReplaceProgramFunc = [Expression] -> [Expression] -> ReplaceProgramContext -> Maybe Program + +type ReplaceExpressionFunc = [Expression] -> [Expression] -> ReplaceExpressionContext -> (Expression, [Expression], [Expression]) + newtype ReplaceException = CouldNotReplace {prog :: Program} deriving (Exception) @@ -23,45 +53,94 @@ "Couldn't replace expression in program, lists of patterns and targets has different lengths\nProgram: %s" (prettyProgram prog) -replaceBindings :: [Binding] -> [Expression] -> [Expression] -> ([Binding], [Expression], [Expression]) -replaceBindings bds [] [] = (bds, [], []) -replaceBindings [] ptns repls = ([], ptns, repls) -replaceBindings (BiTau attr expr : bds) ptns repls = - let (expr', ptns', repls') = replaceExpression expr ptns repls - (bds', ptns'', repls'') = replaceBindings bds ptns' repls' +replaceBindings :: [Binding] -> [Expression] -> [Expression] -> ReplaceExpressionContext -> ReplaceExpressionFunc -> ([Binding], [Expression], [Expression]) +replaceBindings bds [] [] _ _ = (bds, [], []) +replaceBindings [] ptns repls _ _ = ([], ptns, repls) +replaceBindings (BiTau attr expr : bds) ptns repls ctx func = + let (expr', ptns', repls') = func ptns repls (updateExpressionContext ctx expr) + (bds', ptns'', repls'') = replaceBindings bds ptns' repls' ctx func in (BiTau attr expr' : bds', ptns'', repls'') -replaceBindings (bd : bds) ptns repls = - let (bds', ptns', repls') = replaceBindings bds ptns repls +replaceBindings (bd : bds) ptns repls ctx func = + let (bds', ptns', repls') = replaceBindings bds ptns repls ctx func in (bd : bds', ptns', repls') -replaceExpression :: Expression -> [Expression] -> [Expression] -> (Expression, [Expression], [Expression]) -replaceExpression expr [] [] = (expr, [], []) -replaceExpression expr ptns repls = - let (ptn : ptnsRest) = ptns - (repl : replsRest) = repls - in if expr == ptn - then replaceExpression repl ptnsRest replsRest - else case expr of - ExDispatch inner attr -> - let (expr', ptns', repls') = replaceExpression inner ptns repls - in (ExDispatch expr' attr, ptns', repls') - ExApplication inner tau -> - let (expr', ptns', repls') = replaceExpression inner ptns repls - ([tau'], ptns'', repls'') = replaceBindings [tau] ptns' repls' - in (ExApplication expr' tau', ptns'', repls'') +replaceExpression :: ReplaceExpressionFunc +replaceExpression [] [] ReplaceExpressionContext {..} = (_expression, [], []) +replaceExpression ptns@(ptn : ptnsRest) repls@(repl : replsRest) ctx@ReplaceExpressionContext {..} = + if _expression == ptn + then replaceExpression ptnsRest replsRest (updateExpressionContext ctx repl) + else case _expression of + ExDispatch inner attr -> + let (expr', ptns', repls') = replaceExpression ptns repls (updateExpressionContext ctx inner) + in (ExDispatch expr' attr, ptns', repls') + ExApplication inner tau -> + let (expr', ptns', repls') = replaceExpression ptns repls (updateExpressionContext ctx inner) + ([tau'], ptns'', repls'') = replaceBindings [tau] ptns' repls' ctx replaceExpression + in (ExApplication expr' tau', ptns'', repls'') + ExFormation bds -> + let (bds', ptns', repls') = replaceBindings bds ptns repls ctx replaceExpression + in (ExFormation bds', ptns', repls') + _ -> (_expression, ptns, repls) + +replaceBindingsFast :: [Binding] -> [Expression] -> [Expression] -> [Binding] +replaceBindingsFast bds [] [] = bds +replaceBindingsFast bds ((ExFormation pbds) : rptns) ((ExFormation rbds) : rrepls) = + let replaced = replaceBindingsFast' bds pbds rbds + in replaceBindingsFast replaced rptns rrepls + where + replaceBindingsFast' :: [Binding] -> [Binding] -> [Binding] -> [Binding] + replaceBindingsFast' bds pattern replacement + | null pattern = replacement + | otherwise = findAndReplace bds pattern replacement + findAndReplace :: [Binding] -> [Binding] -> [Binding] -> [Binding] + findAndReplace [] _ _ = [] + findAndReplace xs@(x : xs') pattern replacement + | pattern `isPrefixOf` xs = replacement ++ findAndReplace (drop (length pattern) xs) pattern replacement + | otherwise = x : findAndReplace xs' pattern replacement + +replaceExpressionFast :: ReplaceExpressionFunc +replaceExpressionFast = replaceExpressionFast' 0 + where + replaceExpressionFast' :: Integer -> ReplaceExpressionFunc + replaceExpressionFast' _ [] [] ReplaceExpressionContext {..} = (_expression, [], []) + replaceExpressionFast' depth ptns@((ExFormation pbds) : rptns) repls@((ExFormation rbds) : rrepls) ctx@ReplaceExpressionContext {..} = + if depth == _maxDepth + then (_expression, [], []) + else case _expression of ExFormation bds -> - let (bds', ptns', repls') = replaceBindings bds ptns repls + let replaced = replaceBindingsFast bds ptns repls + (bds', ptns', repls') = replaceBindings replaced ptns repls ctx (replaceExpressionFast' (depth + 1)) in (ExFormation bds', ptns', repls') - _ -> (expr, ptns, repls) + ExDispatch inner attr -> + let (expr', ptns', repls') = replaceExpressionFast ptns repls (updateExpressionContext ctx inner) + in (ExDispatch expr' attr, ptns', repls') + ExApplication inner (BiTau attr texpr) -> + let (expr', ptns', repls') = replaceExpressionFast ptns repls (updateExpressionContext ctx inner) + (expr'', ptns'', repls'') = replaceExpressionFast ptns' repls' (updateExpressionContext ctx texpr) + in (ExApplication expr' (BiTau attr expr''), ptns'', repls'') + _ -> (_expression, ptns, repls) + replaceExpressionFast' _ ptns repls ctx@ReplaceExpressionContext{..} = (_expression, ptns, repls) -replaceProgram :: Program -> [Expression] -> [Expression] -> Maybe Program -replaceProgram (Program expr) ptns repls +replaceProgram' :: ReplaceExpressionFunc -> ReplaceProgramFunc +replaceProgram' func ptns repls ReplaceProgramContext {_program = Program expr, ..} | length ptns == length repls = - let (expr', _, _) = replaceExpression expr ptns repls + let (expr', _, _) = func ptns repls (ReplaceExpressionContext expr _maxDepth) in Just (Program expr') | otherwise = Nothing -replaceProgramThrows :: Program -> [Expression] -> [Expression] -> IO Program -replaceProgramThrows prog ptns repls = case replaceProgram prog ptns repls of +replaceProgram :: ReplaceProgramFunc +replaceProgram = replaceProgram' replaceExpression + +replaceProgramThrows' :: ReplaceExpressionFunc -> ReplaceProgramThrowsFunc +replaceProgramThrows' func ptns repls ctx = case replaceProgram' func ptns repls ctx of Just prog' -> pure prog' - _ -> throwIO (CouldNotReplace prog) + _ -> throwIO (CouldNotReplace (_program ctx)) + +replaceProgramThrows :: ReplaceProgramThrowsFunc +replaceProgramThrows = replaceProgramThrows' replaceExpression + +replaceProgramFast :: ReplaceProgramFunc +replaceProgramFast = replaceProgram' replaceExpressionFast + +replaceProgramFastThrows :: ReplaceProgramThrowsFunc +replaceProgramFastThrows = replaceProgramThrows' replaceExpressionFast diff --git a/src/Rewriter.hs b/src/Rewriter.hs --- a/src/Rewriter.hs +++ b/src/Rewriter.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE RecordWildCards #-} -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com @@ -18,7 +19,7 @@ import Misc (ensuredFile) import Parser (parseProgram, parseProgramThrows) import Pretty (PrintMode (SWEET), prettyAttribute, prettyBytes, prettyExpression, prettyExpression', prettyProgram, prettyProgram', prettySubsts) -import Replacer (replaceProgram, replaceProgramThrows) +import Replacer (ReplaceProgramContext (ReplaceProgramContext), ReplaceProgramThrowsFunc, replaceProgramFastThrows, replaceProgramThrows) import Rule (RuleContext (RuleContext), matchProgramWithRule) import qualified Rule as R import Term @@ -52,14 +53,52 @@ must -- Build pattern and result expression and replace patterns to results in given program -buildAndReplace :: Program -> Expression -> Expression -> [Subst] -> IO Program -buildAndReplace program ptn res substs = do +buildAndReplace' :: Expression -> Expression -> [Subst] -> ReplaceProgramThrowsFunc -> ReplaceProgramContext -> IO Program +buildAndReplace' ptn res substs func ctx = do ptns <- buildExpressions ptn substs repls <- buildExpressions res substs let repls' = map fst repls ptns' = map fst ptns - replaceProgramThrows program ptns' repls' + func ptns' repls' ctx +-- If pattern and replacement are appropriate for fast replacing - does it. +-- Pattern and replacement expressions can be used in fast replacing only if +-- 1. they are both formations +-- 2. they start and end with the same meta bindings, e.g. [!B1, ..., !B2] +-- 3. the does not have meta bindings between first and last meta bindings +-- In such case we can just replace bindings one by one without building whole expression. +-- You can find more details in this ticket: https://github.com/objectionary/phino/issues/321 +-- If we don't meet the conditions above - just do a regular replacing +tryBuildAndReplaceFast :: Expression -> Expression -> [Subst] -> ReplaceProgramContext -> IO Program +tryBuildAndReplaceFast (ExFormation pbds) (ExFormation rbds) substs ctx = + let pbds' = init (tail pbds) + rbds' = init (tail rbds) + in if startsAndEndsWithMeta pbds + && startsAndEndsWithMeta rbds + && head pbds == head rbds + && last pbds == last rbds + && not (hasMetaBindings pbds') + && not (hasMetaBindings rbds') + then do + logDebug "Applying fast replacing since 'pattern' and 'result' are suitable for this..." + buildAndReplace' (ExFormation pbds') (ExFormation rbds') substs replaceProgramFastThrows ctx + else do + logDebug "Applying regular replacing..." + buildAndReplace' (ExFormation pbds) (ExFormation rbds) substs replaceProgramThrows ctx + where + startsAndEndsWithMeta :: [Binding] -> Bool + startsAndEndsWithMeta bds = + length bds > 1 + && isMetaBinding (head bds) + && isMetaBinding (last bds) + hasMetaBindings :: [Binding] -> Bool + isMetaBinding :: Binding -> Bool + isMetaBinding = \case + BiMeta _ -> True + _ -> False + hasMetaBindings = foldl (\acc bd -> acc || isMetaBinding bd) False +tryBuildAndReplaceFast ptn res substs ctx = buildAndReplace' ptn res substs replaceProgramThrows ctx + rewrite :: Program -> [Y.Rule] -> RewriteContext -> IO Program rewrite program [] _ = pure program rewrite program (rule : rest) ctx = do @@ -85,7 +124,7 @@ pure prog else do logDebug (printf "Rule '%s' has been matched, applying..." ruleName) - prog' <- buildAndReplace prog ptn res matched + prog' <- tryBuildAndReplaceFast ptn res matched (ReplaceProgramContext prog depth) if prog == prog' then do logDebug (printf "Applied '%s', no changes made" ruleName) diff --git a/src/XMIR.hs b/src/XMIR.hs --- a/src/XMIR.hs +++ b/src/XMIR.hs @@ -172,8 +172,6 @@ -- The function returns tuple (X, Y), where -- - X: list of package parts -- - Y: root object expression --- @todo #197:30min Make patterns with L> Package softer. Right now we expect L> Package only in the end --- of the formation bindings list. That's not really correct since this binding may be anywhere. Let's fix it getPackage :: Expression -> IO ([String], Expression) getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda "Package", BiVoid AtRho]), BiVoid AtRho]) = do (pckg, expr') <- getPackage (ExFormation [bd, BiLambda "Package", BiVoid AtRho]) diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -18,6 +18,7 @@ import System.IO import System.IO.Silently (capture_) import Test.Hspec +import Text.Printf (printf) withStdin :: String -> IO a -> IO a withStdin input action = @@ -191,6 +192,20 @@ it "fails with --normalize and --must" $ withStdin "Q -> [[ x -> [[ y -> 5 ]].y ]].x" $ testCLIFailed ["rewrite", "--max-depth=2", "--normalize", "--must"] "it's expected exactly 1 rewriting cycles happened, but rewriting is still going" + + it "prints to target file" $ + withStdin "Q -> [[ ]]" $ + bracket + (openTempFile "." "targetXXXXXX.tmp") + (\(path, _) -> removeFile path) + ( \(path, h) -> do + hClose h + testCLI + ["rewrite", "--nothing", "--sweet", printf "--target=%s" path] + [printf "The result program was saved in '%s'" path] + content <- readFile path + content `shouldBe` "{⟦⟧}" + ) describe "dataize" $ do it "dataizes simple program" $ diff --git a/test/MatcherSpec.hs b/test/MatcherSpec.hs --- a/test/MatcherSpec.hs +++ b/test/MatcherSpec.hs @@ -251,7 +251,7 @@ defaultScope, [[("a", MvAttribute (AtLabel "y")), ("B", MvBindings [BiVoid (AtLabel "x")])]] ), - ( "[[!B1, !a -> ?, !B2]] => [[ x -> ?, y -> ?, z -> ? ]] => [(), (), ()]", + ( "[[!B1, !a -> ?, !B2]] => [[ x -> ?, y -> ?, z -> ? ]] => [(!B1 >> [[]], !a >> x, !B2 >> [[ y -> ?, z -> ? ]]), (...), (...)]", [BiMeta "B1", BiVoid (AtMeta "a"), BiMeta "B2"], [BiVoid (AtLabel "x"), BiVoid (AtLabel "y"), BiVoid (AtLabel "z")], defaultScope, diff --git a/test/PrettySpec.hs b/test/PrettySpec.hs --- a/test/PrettySpec.hs +++ b/test/PrettySpec.hs @@ -54,7 +54,8 @@ ("Q -> Q.x(~0 -> 1)(~1 -> 2)(~2 -> 3)", "{Φ.x(\n 1,\n 2,\n 3\n)}"), ("Q -> Q.x(~0 -> 1)(~2 -> 2)(~1 -> 3)", "{Φ.x(\n α0 ↦ 1,\n α2 ↦ 2,\n α1 ↦ 3\n)}"), ("Q -> Φ.jeo.opcode.ldc(18, \"Reading \\\"\")", "{Φ.jeo.opcode.ldc(\n 18,\n \"Reading \\\"\"\n)}"), - ("Q -> [[ k -> [[]] ]]", "{⟦\n k ↦ ⟦⟧\n⟧}") + ("Q -> [[ k -> [[]] ]]", "{⟦\n k ↦ ⟦⟧\n⟧}"), + ("Q -> [[ ]]", "{⟦⟧}") ] test prettyProgram' useCases diff --git a/test/ReplacerSpec.hs b/test/ReplacerSpec.hs --- a/test/ReplacerSpec.hs +++ b/test/ReplacerSpec.hs @@ -8,17 +8,14 @@ import Replacer import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, describe, it, shouldBe) -test :: - (Program -> [Expression] -> [Expression] -> Maybe Program) -> - [(String, Program, [Expression], [Expression], Maybe Program)] -> - SpecWith (Arg Expectation) +test :: ReplaceProgramFunc -> [(String, Program, [Expression], [Expression], Maybe Program)] -> SpecWith (Arg Expectation) test function useCases = forM_ useCases $ \(desc, prog, ptns, repls, res) -> - it desc $ function prog ptns repls `shouldBe` res + it desc $ function ptns repls (ReplaceProgramContext prog 3) `shouldBe` res spec :: Spec -spec = - describe "replaceProgram: program => ([expression], [expression]) => program" $ +spec = do + describe "replace program: Program => ([Expression], [Expression]) => Program" $ test replaceProgram [ ( "Q -> Q.y.x => ([Q.y], [$]) => Q -> $.x", @@ -101,5 +98,28 @@ ) ) ) + ) + ] + + describe "replace program fast: Program => ([Expression], [Expression]) => Program" $ + test + replaceProgramFast + [ ( "Q -> [[^ -> ?, @ -> ?, D> -> ?]] => [[ !B1, !a -> ?, !B2 ]] => [[ !B1, !a -> $, !B2 ]] => Q -> [[ ^ -> $, @ -> $, D> -> $ ]]", + Program (ExFormation [BiVoid AtRho, BiVoid AtPhi, BiVoid AtDelta]), + [ExFormation [BiVoid AtRho], ExFormation [BiVoid AtPhi], ExFormation [BiVoid AtDelta]], + [ExFormation [BiTau AtRho ExThis], ExFormation [BiTau AtPhi ExThis], ExFormation [BiTau AtDelta ExThis]], + Just (Program (ExFormation [BiTau AtRho ExThis, BiTau AtPhi ExThis, BiTau AtDelta ExThis])) + ), + ( "Q -> [[ ^ -> ? ]] => [[ !B1, !a -> ?, !B2 ]] => [[ !B1, !a -> [[ !a -> ? ]], !B2 ]] => Q -> [[ ^ -> [[ ^ -> [[ ^ -> [[ ^ -> ? ]] ]] ]] ]]", + Program (ExFormation [BiVoid AtRho]), + [ExFormation [BiVoid AtRho]], + [ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])]], + Just (Program (ExFormation [BiTau AtRho (ExFormation [BiTau AtRho (ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])])])])) + ), + ( "Q -> [[ ^ -> T ]](^ -> [[ ^ -> $]]).@ => [[ !B1, !a -> ?, !B2 ]] => [[ !B1, !a -> $, !B2 ]] => Q -> [[ ^ -> $ ]].@", + Program (ExDispatch (ExApplication (ExFormation [BiTau AtRho ExTermination]) (BiTau AtRho (ExFormation [BiTau AtRho ExThis]))) AtPhi), + [ExFormation [BiTau AtRho ExTermination], ExFormation [BiTau AtRho ExThis]], + [ExFormation [BiTau AtRho ExGlobal], ExFormation [BiVoid AtPhi]], + Just (Program (ExDispatch (ExApplication (ExFormation [BiTau AtRho ExGlobal]) (BiTau AtRho (ExFormation [BiVoid AtPhi]))) AtPhi)) ) ]