phino 0.0.0.37 → 0.0.0.38

raw patch · 10 files changed

+221/−53 lines, 10 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• phino.cabal +1/−1
• src/CLI.hs +13/−2
• src/Pretty.hs +7/−2
• src/Replacer.hs +111/−32
• src/Rewriter.hs +44/−5
• src/XMIR.hs +0/−2
• test/CLISpec.hs +15/−0
• test/MatcherSpec.hs +1/−1
• test/PrettySpec.hs +2/−1
• test/ReplacerSpec.hs +27/−7

@@ -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 <https://github.com/objectionary/phino#readme>

@@ -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

@@ -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 "⟧"

@@ -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

@@ -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)

@@ -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])

@@ -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" $

@@ -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,

@@ -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 

@@ -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))         )       ]