phino 0.0.83 → 0.0.84

raw patch · 31 files changed

+432/−358 lines, 31 filesdep ~megaparsecPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: megaparsec

API changes (from Hackage documentation)

Files

• README.md +19/−16
• phino.cabal +3/−3
• resources/dataization.yaml +3/−3
• resources/morphing.yaml +16/−6
• src/CLI.hs +23/−25
• src/CLI/Parsers.hs +4/−4
• src/CST.hs +18/−13
• src/Condition.hs +1/−1
• src/Dataize.hs +9/−9
• src/Encoding.hs +6/−3
• src/LaTeX.hs +25/−23
• src/Lining.hs +1/−0
• src/Margin.hs +5/−0
• src/Matcher.hs +1/−1
• src/Parser.hs +13/−13
• src/Printer.hs +1/−1
• src/Random.hs +8/−3
• src/Render.hs +21/−10
• src/Sugar.hs +6/−5
• src/Yaml.hs +1/−1
• test/ASTSpec.hs +4/−4
• test/BuilderSpec.hs +19/−19
• test/CLISpec.hs +107/−92
• test/CSTSpec.hs +1/−1
• test/ConditionSpec.hs +7/−7
• test/MatcherSpec.hs +57/−57
• test/MiscSpec.hs +6/−6
• test/ParserSpec.hs +32/−28
• test/PrinterSpec.hs +5/−1
• test/RandomSpec.hs +7/−0
• test/ReplacerSpec.hs +3/−3

@@ -213,21 +213,21 @@ ```bash $ phino explain --normalize \begin{tabular}{rl}-\trrule{alpha}+\phinoNormalizationRule{alpha}   { [[ B_1, \tau -> ?, B_2 ]] ( \alpha_{i} -> e ) }   { [[ B_1, \tau -> ?, B_2 ]] ( \tau -> e ) }-  { if $ i = \vert \overline{ B_1 } \vert $ }+  { $ i = \vert \overline{ B_1 } \vert $ }   { }-\trrule{dc}+\phinoNormalizationRule{dc}   { T ( \tau -> e ) }   { T }   { }   { } ...-\trrule{stop}+\phinoNormalizationRule{stop}   { [[ B ]] . \tau }   { T }-  { if $ \tau \notin B \;\text{and}\; @ \notin B \;\text{and}\; L \notin B $ }+  { $ \tau \notin B \;\text{and}\; @ \notin B \;\text{and}\; L \notin B $ }   { } \end{tabular} ```@@ -237,30 +237,30 @@ ```bash $ phino explain --morph \begin{tabular}{rl}-\trrule{prim}+\phinoMorphingRule{prim}   { \mathbb{M}( [[ B ]] ) }   { [[ B ]] }   { }   { } ...-\trrule{root}+\phinoMorphingRule{root}   { \mathbb{M}( Q ) }-  { \mathbb{M}( \mathcal{N}( e ) ) }-  { if $ e \not= Q $ }-  { where $ e \coloneqq global(  ) $ }+  { \mathbb{M}( \phinoNormalize{ e } ) }+  { $ e \not= Q $ }+  { $ e \coloneqq \phinoGlobal{  } $ } \end{tabular} ```  ```bash $ phino explain --dataize \begin{tabular}{rl}-\trrule{delta}+\phinoDataizationRule{delta}   { \mathbb{D}( [[ B_1, D> δ, B_2 ]] ) }   { δ }   { }   { } ...-\trrule{norm}+\phinoDataizationRule{norm}   { \mathbb{D}( n ) }   { \mathbb{D}( \mathbb{M}( n ) ) }   { }@@ -330,7 +330,7 @@   = Bytes'               # !d   | Binding'             # !B   | Expression'          # !e-  | Attribute'           # !a+  | Attribute'           # !t ```  Here's list of functions that are supported for extensions:@@ -376,9 +376,9 @@  This is the list of supported meta variables: -* `!a` || `𝜏` - attribute+* `!t` || `𝜏` - attribute * `!i` || `𝑖` - the index of a positional (α) application argument,-                captured by writing `α𝑖`+                captured by writing `α𝑖` (or `a𝑖`) * `!e` || `𝑒` - any expression * `!n` || `𝑛` - any expression that is already in normal form (behaves like                 `!e`/`𝑒`, but only binds a sub-expression in NF, so no explicit@@ -389,9 +389,12 @@                 or `nf:` guard is needed * `!B` || `𝐵` - list of bindings * `!d` || `δ` - bytes in meta delta binding-* `!F` - function name in meta lambda binding+* `!F` || `𝐹` - function name in meta lambda binding  Every meta variable may also be used with an integer index, like `!B1` or `𝜏0`.++A positional (α) application argument is written as `α0`, `a0` (ASCII), or+`α𝑖`/`a!i` when its index is captured by an `!i`/`𝑖` meta variable.  Incorrect usage of meta variables in 𝜑-expression patterns leads to parsing errors.

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.83+version: 0.0.84 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>@@ -88,7 +88,7 @@     directory >=1.3.7 && <1.4,     file-embed >=0.0.15 && <0.0.17,     filepath >=1.4.200 && <1.6,-    megaparsec >=9.5 && <9.8,+    megaparsec >=9.5 && <9.9,     optparse-applicative >=0.18 && <0.20,     random >=1.2 && <1.4,     regex-pcre-builtin >=0.95.2 && <0.96,@@ -162,7 +162,7 @@     filepath >=1.4.200 && <1.6,     hspec >=2.11.0 && <2.12,     hspec-core >=2.11.0 && <2.12,-    megaparsec >=9.5 && <9.8,+    megaparsec >=9.5 && <9.9,     optparse-applicative >=0.18 && <0.20,     phino,     process >=1.6.17 && <1.7,

@@ -27,13 +27,13 @@       normalize: 𝑒1  - name: fire-  description: '𝔻(⟦𝐵1, λ ⤍ F, 𝐵2⟧) ⟿ 𝔻(𝒩(𝔼(⟦𝐵1, λ ⤍ F, 𝐵2⟧)))'-  match: ⟦𝐵1, λ ⤍ !F, 𝐵2⟧+  description: '𝔻(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧) ⟿ 𝔻(𝒩(𝔼(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧)))'+  match: ⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧   where:     - meta: 𝑒       function: lambda       args:-        - ⟦𝐵1, λ ⤍ !F, 𝐵2⟧+        - ⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧   then:     dataize:       normalize: 𝑒

@@ -14,13 +14,13 @@   then: ⟦𝐵⟧  - name: lambda-  description: '𝕄(⟦𝐵1, λ ⤍ F, 𝐵2⟧.τ) ⟿ 𝕄(𝒩(𝔼(⟦𝐵1, λ ⤍ F, 𝐵2⟧).τ))'-  match: '⟦𝐵1, λ ⤍ !F, 𝐵2⟧.𝜏'+  description: '𝕄(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧.τ) ⟿ 𝕄(𝒩(𝔼(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧).τ))'+  match: '⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧.𝜏'   where:     - meta: 𝑒       function: lambda       args:-        - '⟦𝐵1, λ ⤍ !F, 𝐵2⟧'+        - '⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧'   then:     morph:       normalize: '𝑒.𝜏'@@ -76,7 +76,17 @@     morph:       normalize: 𝑒 -- name: stuck-  description: '𝕄(n) ⟿ ⊥ otherwise'-  match: 𝑛+- name: dead+  description: '𝕄(⊥) ⟿ ⊥'+  match: ⊥+  then: ⊥++- name: xi+  description: '𝕄(ξ) ⟿ ⊥'+  match: ξ+  then: ⊥++- name: globe+  description: '𝕄(Φ) ⟿ ⊥ when the universe is Φ itself'+  match: Φ   then: ⊥

@@ -17,31 +17,6 @@ import Paths_phino (version) import System.Exit (ExitCode (..), exitFailure) -handler :: SomeException -> IO ()-handler e = case fromException e of-  Just ExitSuccess -> pure () -- prevent printing error on --version etc.-  _ -> do-    logError (displayException e)-    exitFailure--setLogger :: Command -> IO ()-setLogger cmd =-  let (level, lns) = case cmd of-        CmdRewrite OptsRewrite{_logLevel, _logLines} -> (_logLevel, _logLines)-        CmdDataize OptsDataize{_logLevel, _logLines} -> (_logLevel, _logLines)-        CmdExplain OptsExplain{_logLevel, _logLines} -> (_logLevel, _logLines)-        CmdMerge OptsMerge{_logLevel, _logLines} -> (_logLevel, _logLines)-        CmdMatch OptsMatch{_logLevel, _logLines} -> (_logLevel, _logLines)-   in setLogConfig level lns--checkPin :: Maybe String -> IO ()-checkPin Nothing = pure ()-checkPin (Just expected)-  | expected == actual = pure ()-  | otherwise = throwIO (VersionMismatch expected actual)-  where-    actual = showVersion version- runCLI :: [String] -> IO () runCLI args = handle handler $ do   CliArgs{_pin, _command} <- handleParseResult (execParserPure defaultPrefs parserInfo args)@@ -53,3 +28,26 @@     CmdExplain opts -> runExplain opts     CmdMerge opts -> runMerge opts     CmdMatch opts -> runMatch opts+  where+    handler :: SomeException -> IO ()+    handler e = case fromException e of+      Just ExitSuccess -> pure () -- prevent printing error on --version etc.+      _ -> do+        logError (displayException e)+        exitFailure+    setLogger :: Command -> IO ()+    setLogger cmd =+      let (level, lns) = case cmd of+            CmdRewrite OptsRewrite{_logLevel, _logLines} -> (_logLevel, _logLines)+            CmdDataize OptsDataize{_logLevel, _logLines} -> (_logLevel, _logLines)+            CmdExplain OptsExplain{_logLevel, _logLines} -> (_logLevel, _logLines)+            CmdMerge OptsMerge{_logLevel, _logLines} -> (_logLevel, _logLines)+            CmdMatch OptsMatch{_logLevel, _logLines} -> (_logLevel, _logLines)+       in setLogConfig level lns+    checkPin :: Maybe String -> IO ()+    checkPin Nothing = pure ()+    checkPin (Just expected)+      | expected == actual = pure ()+      | otherwise = throwIO (VersionMismatch expected actual)+      where+        actual = showVersion version

@@ -97,7 +97,7 @@         )         ( long "meet-popularity"             <> metavar "PERCENTAGE"-            <> help (printf "The minimum popularity of an expression in order to be suitable for \\phiMeet{}, in percentage (default: %d)" defaultMeetPopularity)+            <> help (printf "The minimum popularity of an expression in order to be suitable for \\phinoMeet{}, in percentage (default: %d)" defaultMeetPopularity)         )     ) @@ -108,7 +108,7 @@         (auto >>= validateIntOption (> 0) "--meet-length must be positive")         ( long "meet-length"             <> metavar "NODES"-            <> help (printf "The minimum length of an expression that fits into \\phiMeet{}, in AST nodes (default: %d)" defaultMeetLength)+            <> help (printf "The minimum length of an expression that fits into \\phinoMeet{}, in AST nodes (default: %d)" defaultMeetLength)         )     ) @@ -131,7 +131,7 @@ 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}"))+optMeetPrefix = optional (strOption (long "meet-prefix" <> metavar "PREFIX" <> help "Prefix to be inserted before index in \\phinoMeet{} and \\phinoAgain{} LaTeX functions, e.g. \\phinoMeet{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"))@@ -219,7 +219,7 @@ optOmitComments = switch (long "omit-comments" <> help "Omit comments in XMIR output")  optCompress :: Parser Bool-optCompress = switch (long "compress" <> help "Compress expressions in LaTeX output using \\phiMeet{} and \\phiAgain{} functions")+optCompress = switch (long "compress" <> help "Compress expressions in LaTeX output using \\phinoMeet{} and \\phinoAgain{} functions")  _intermediateOptions :: String _intermediateOptions = intercalate ", " ["--sequence", "--steps-dir"]

@@ -42,7 +42,7 @@ data PHI = PHI | AT   deriving (Eq, Show) -data RHO = RHO | CARET+data RHO = RHO | CARET | RHO'   deriving (Eq, Show)  data DELTA = DELTA | DELTA'@@ -83,7 +83,7 @@   | N' -- n   | K -- 𝑘   | K' -- k-  | A -- a+  | A -- t (ASCII attribute meta)   | TAU -- 𝜏   | TAU' -- \tau   | I -- 𝑖@@ -92,7 +92,8 @@   | B' -- B   | D -- δ   | D' -- \delta-  | F -- F+  | F -- 𝐹+  | F' -- F   deriving (Eq, Show)  data EXCLAMATION = EXCL | NO_EXCL@@ -107,9 +108,14 @@   | NO_TAB   deriving (Eq, Show) -data ALPHA = ALPHA | ALPHA'+data ALPHA' = ALPHA | ALPHA'   deriving (Eq, Show) +data ALPHA+  = AL_IDX {sym :: ALPHA', idx :: Int}+  | AL_META {sym :: ALPHA', meta :: META}+  deriving (Eq, Show)+ data PROGRAM   = PR_SWEET {lcb :: LCB, expr :: EXPRESSION, rcb :: RCB, space :: SPACE}   | PR_SALTY {global :: GLOBAL, arrow :: ARROW, expr :: EXPRESSION}@@ -117,6 +123,7 @@  data PAIR   = PA_TAU {attr :: ATTRIBUTE, arrow :: ARROW, expr :: EXPRESSION}+  | PA_ALPHA {alpha :: ALPHA, arrow :: ARROW, expr :: EXPRESSION}   | PA_FORMATION {attr :: ATTRIBUTE, voids :: [ATTRIBUTE], arrow :: ARROW, expr :: EXPRESSION}   | PA_VOID {attr :: ATTRIBUTE, arrow :: ARROW, void :: VOID}   | PA_LAMBDA {func :: T.Text}@@ -173,8 +180,6 @@  data ATTRIBUTE   = AT_LABEL {label :: T.Text}-  | AT_ALPHA {alpha :: ALPHA, idx :: Int}-  | AT_ALPHA_META {alpha :: ALPHA, meta :: META}   | AT_RHO {rho :: RHO}   | AT_PHI {phi :: PHI}   | AT_LAMBDA {lambda :: LAMBDA}@@ -338,7 +343,7 @@   -- Since we convert AST to CST in sweet notation, here we're trying to get rid of unnecessary rho bindings   -- in primitives (more details here: https://github.com/objectionary/phino/issues/451)   -- If we find something similar to:-  -- `Q.number(~0 -> Q.bytes(...), ^ -> ..., ^ -> ...)`+  -- `Q.number(a0 -> Q.bytes(...), ^ -> ..., ^ -> ...)`   -- We remove unnecessary rho bindings and save them to EX_STRING or EX_NUMBER so they can be successfully   -- converted to salty notation without losing information.   -- In the end we just get CST with data primitive which is printed correctly.@@ -404,7 +409,7 @@       -- 1. deepest start expression       -- 2. list of tau bindings which are applied to start expression       -- 3. list of expressions which are applied to start expression with default-      --    alpha attributes (~0 -> e1, ~1 -> e2, ...)+      --    alpha attributes (a0 -> e1, a1 -> e2, ...)       complexApplication :: Expression -> (Expression, [Argument], [Expression])       complexApplication expr =         let (expr', taus', exprs') = complexApplication' expr@@ -476,12 +481,12 @@   toCST (BiVoid attr) ctx = PA_VOID (toCST attr ctx) ARROW EMPTY   toCST (BiDelta bts) ctx = PA_DELTA (toCST bts ctx)   toCST (BiLambda (Function name)) _ = PA_LAMBDA name-  toCST (BiLambda (FnMeta mt)) _ = PA_META_LAMBDA (META EXCL F (metaTail mt))+  toCST (BiLambda (FnMeta mt)) _ = PA_META_LAMBDA (META NO_EXCL F (metaTail mt))   toCST (BiMeta mt) _ = error $ "BiMeta binding " ++ T.unpack mt ++ " cannot be converted to PAIR"  instance ToCST Argument PAIR where   toCST (ArTau attr exp) ctx = toCST (BiTau attr exp) ctx-  toCST (ArAlpha alpha exp) ctx = PA_TAU (toCST alpha ctx) ARROW (toCST exp ctx)+  toCST (ArAlpha alpha exp) ctx = PA_ALPHA (toCST alpha ctx) ARROW (toCST exp ctx)  instance ToCST [Argument] BINDING where   toCST [] (tabs, _) = BI_EMPTY (TAB tabs)@@ -509,9 +514,9 @@   toCST AtLambda _ = AT_LAMBDA LAMBDA   toCST (AtMeta mt) _ = AT_META (META NO_EXCL TAU (metaTail mt)) -instance ToCST Alpha ATTRIBUTE where-  toCST (Alpha idx) _ = AT_ALPHA ALPHA idx-  toCST (AlMeta mt) _ = AT_ALPHA_META ALPHA (META NO_EXCL I (metaTail mt))+instance ToCST Alpha ALPHA where+  toCST (Alpha idx) _ = AL_IDX ALPHA idx+  toCST (AlMeta mt) _ = AL_META ALPHA (META NO_EXCL I (metaTail mt))  instance ToCST Y.Condition CONDITION where   toCST (Y.Not (Y.In attr binding)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_BINDING (bindingsToCST [binding]))

@@ -58,7 +58,7 @@         bd <- _binding phiParser         _ <- rparen         return (Y.Domain bd)-    , Y.MetaIndex <$> _indexMeta phiParser+    , Y.MetaIndex <$> _index phiParser     , do         sign <- optional (choice [char '-', char '+'])         unsigned <- lexeme L.decimal

@@ -76,7 +76,7 @@   matched <- firstMatch Y.morphingRules   case matched of     Just (rule, subst) -> apply rule.then_ rule.name subst-    Nothing -> pure (expr, seq)+    Nothing -> throwIO (userError "no morphing rule matched")   where     firstMatch :: [Y.MorphRule] -> IO (Maybe (Y.MorphRule, Subst))     firstMatch [] = pure Nothing@@ -103,7 +103,7 @@     -- rewriter and splices its individual steps (alpha, copy, dot, …) into the     -- chain before morphing on the resulting normal form. Termination is the     -- rules' job: the 'root' rule's 'when' refuses to expand a universe that is-    -- Φ itself, so 'stuck' yields ⊥ instead of looping.+    -- Φ itself, so the 'globe' rule catches it and yields ⊥ instead of looping.     apply (Y.MoMorph (Y.MaNormalize arg)) name subst = do       built <- buildExpressionThrows arg subst       labelled <- leadsTo seq name built ctx@@ -127,7 +127,7 @@   matched <- firstMatch Y.dataizationRules   case matched of     Just (rule, subst) -> apply rule subst-    Nothing -> pure (Nothing, NE.toList seq)+    Nothing -> throwIO (userError "no dataization rule matched")   where     firstMatch :: [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst))     firstMatch [] = pure Nothing@@ -183,12 +183,12 @@       seq' = rw :| rws <> NE.tail seq   expr' <- locatedExpression _locator (fst rw)   pure (expr', seq')---- Switch the dataization context to a rewriting context for normalization,--- disabling the must-checker and breakpoints.-rewriteContext :: DataizeContext -> RewriteContext-rewriteContext DataizeContext{..} =-  RewriteContext _locator _maxDepth _maxCycles _depthSensitive _buildTerm MtDisabled Nothing _saveStep+  where+    -- Switch the dataization context to a rewriting context for normalization,+    -- disabling the must-checker and breakpoints.+    rewriteContext :: DataizeContext -> RewriteContext+    rewriteContext DataizeContext{..} =+      RewriteContext _locator _maxDepth _maxCycles _depthSensitive _buildTerm MtDisabled Nothing _saveStep  -- Synthetic dataize function for internal usage inside atoms -- Here we modify original program from context by adding new binding

@@ -60,17 +60,20 @@  instance ToASCII PAIR where   toASCII PA_TAU{..} = PA_TAU (toASCII attr) ARROW' (toASCII expr)+  toASCII PA_ALPHA{..} = PA_ALPHA (toASCII alpha) ARROW' (toASCII expr)   toASCII PA_FORMATION{..} = PA_FORMATION (toASCII attr) (map toASCII voids) ARROW' (toASCII expr)   toASCII PA_VOID{..} = PA_VOID (toASCII attr) ARROW' QUESTION   toASCII PA_LAMBDA{..} = PA_LAMBDA' func   toASCII PA_DELTA{..} = PA_DELTA' bytes-  toASCII PA_META_LAMBDA{..} = PA_META_LAMBDA' meta+  toASCII PA_META_LAMBDA{meta = META{..}} = PA_META_LAMBDA' (META EXCL F' rest)   toASCII PA_META_DELTA{..} = PA_META_DELTA' (META EXCL D' (rest meta))   toASCII pair = pair +instance ToASCII ALPHA where+  toASCII AL_IDX{..} = AL_IDX ALPHA' idx+  toASCII AL_META{..} = AL_META ALPHA' (META EXCL I' (rest meta))+ instance ToASCII ATTRIBUTE where-  toASCII AT_ALPHA{..} = AT_ALPHA ALPHA' idx-  toASCII AT_ALPHA_META{..} = AT_ALPHA_META ALPHA' (META EXCL I' (rest meta))   toASCII AT_PHI{} = AT_PHI AT   toASCII AT_RHO{} = AT_RHO CARET   toASCII AT_META{..} = AT_META (META EXCL A (rest meta))

@@ -88,11 +88,11 @@     argExpr (ArTau _ ex) = ex     argExpr (ArAlpha _ ex) = ex -{- | Here we're trying to compress sequence of programs with \phiMeet{} and \phiAgain LaTeX functions.+{- | Here we're trying to compress sequence of programs with \phinoMeet{} and \phinoAgain LaTeX functions. We process the sequence of programs and trying to find all expressions in first program which are present in following programs. Then we find ONE expression which is the most frequently encountered. If it's encountered in more than specific percentage (_meetPopularity) of following programs - we replace-it with \phiAgain{} in following programs and with \phiMeet{} in first program.+it with \phinoAgain{} in following programs and with \phinoMeet{} in first program. -} meetInPrograms :: [Program] -> LatexContext -> [Program] meetInPrograms prog LatexContext{..} = meetInPrograms' prog 1@@ -238,11 +238,11 @@  instance ToLaTeX ATTRIBUTE where   toLaTeX AT_LABEL{..} = AT_LABEL (piped label)-  toLaTeX AT_ALPHA_META{..} = AT_LABEL ("\\alpha_{" <> render (hd meta) <> rest meta <> "}")   toLaTeX AT_META{..} = AT_META (toLaTeX meta)   toLaTeX AT_LAMBDA{} = AT_LAMBDA LAMBDA'   toLaTeX AT_DELTA{} = AT_DELTA DELTA'   toLaTeX AT_REST{} = AT_REST DOTS'+  toLaTeX AT_RHO{} = AT_RHO RHO'   toLaTeX attr = attr  instance ToLaTeX APP_BINDING where@@ -265,6 +265,11 @@   toLaTeX PA_LAMBDA'{..} = PA_LAMBDA' (piped func)   toLaTeX PA_VOID{..} = PA_VOID (toLaTeX attr) arrow void   toLaTeX PA_TAU{..} = PA_TAU (toLaTeX attr) arrow (toLaTeX expr)+  toLaTeX PA_ALPHA{..} =+    let subscript = case alpha of+          AL_IDX _ n -> render n+          AL_META _ mt -> render (hd mt) <> rest mt+     in PA_TAU (AT_LABEL ("\\alpha_{" <> subscript <> "}")) arrow (toLaTeX expr)   toLaTeX PA_FORMATION{..} = PA_FORMATION (toLaTeX attr) (map toLaTeX voids) arrow (toLaTeX expr)   toLaTeX PA_META_DELTA{..} = toLaTeX (PA_META_DELTA' meta)   toLaTeX PA_META_DELTA'{..} = PA_META_DELTA' (toLaTeX meta)@@ -285,6 +290,7 @@   toLaTeX TAU = TAU'   toLaTeX B = B'   toLaTeX D = D'+  toLaTeX F = F'   toLaTeX mh = mh  instance ToLaTeX BYTES where@@ -346,6 +352,7 @@ explainRule :: Y.Rule -> String explainRule rule =   trrule+    "\\phinoNormalizationRule"     rule.name     (renderToLatex (expressionToCST rule.pattern) defaultLatexContext)     (renderToLatex (expressionToCST rule.result) defaultLatexContext)@@ -362,6 +369,7 @@ explainMorphRule :: Y.MorphRule -> String explainMorphRule rule =   trrule+    "\\phinoMorphingRule"     rule.name     (morph (renderToLatex (expressionToCST rule.match) defaultLatexContext))     (morphOutcome rule.then_)@@ -376,6 +384,7 @@ explainDataizeRule :: Y.DataizeRule -> String explainDataizeRule rule =   trrule+    "\\phinoDataizationRule"     rule.name     (dataize (renderToLatex (expressionToCST rule.match) defaultLatexContext))     (dataizeOutcome rule.then_)@@ -389,13 +398,15 @@     dataizeOutcome (Y.DoData bytes) = T.unpack (render (toLaTeX (toCST' bytes :: BYTES)))     dataizeOutcome Y.DoNothing = "\\varnothing" --- Render a single rule row through the shared \trrule macro: name, left-hand--- side, right-hand side, the optional 'if' condition and 'where' extras.-trrule :: String -> String -> String -> Maybe Y.Condition -> Maybe [Y.Extra] -> String-trrule name lhs rhs cond extras =+-- Render a single rule row through the given macro (one of+-- \phinoMorphingRule, \phinoNormalizationRule, \phinoDataizationRule): name,+-- left-hand side, right-hand side, the optional 'if' condition and 'where'+-- extras.+trrule :: String -> String -> String -> String -> Maybe Y.Condition -> Maybe [Y.Extra] -> String+trrule macro name lhs rhs cond extras =   intercalate     "\n  "-    [ "\\trrule{" ++ name ++ "}"+    [ macro ++ "{" ++ name ++ "}"     , braced lhs     , braced rhs     , conditionToLatex cond@@ -409,7 +420,7 @@ dataize inner = "\\mathbb{D}( " ++ inner ++ " )"  normalize :: String -> String-normalize inner = "\\mathcal{N}( " ++ inner ++ " )"+normalize inner = "\\phinoNormalize{ " ++ inner ++ " }"  braced :: String -> String braced = printf "{ %s }"@@ -418,28 +429,19 @@ conditionToLatex Nothing = "{ }" conditionToLatex (Just cond) = case conditionToCST cond of   CO_EMPTY -> "{ }"-  cond' -> braced ("if $ " <> renderToLatex cond' defaultLatexContext <> " $")+  cond' -> braced (renderToLatex cond' defaultLatexContext)  extraArgumentsToLatex :: Maybe [Y.Extra] -> String extraArgumentsToLatex Nothing = "{ }" extraArgumentsToLatex (Just extras) =   let extras' = map ((`renderToLatex` defaultLatexContext) . extraToCST) extras-   in braced ("where " <> intercalate " and " extras')+   in braced (intercalate " and " extras')  explainRules :: [Y.Rule] -> String-explainRules = explainTabular . map explainRule+explainRules = intercalate "\n" . map explainRule  explainMorphRules :: [Y.MorphRule] -> String-explainMorphRules = explainTabular . map explainMorphRule+explainMorphRules = intercalate "\n" . map explainMorphRule  explainDataizeRules :: [Y.DataizeRule] -> String-explainDataizeRules = explainTabular . map explainDataizeRule--explainTabular :: [String] -> String-explainTabular rows =-  intercalate-    "\n"-    [ "\\begin{tabular}{rl}"-    , intercalate "\n" rows-    , "\\end{tabular}"-    ]+explainDataizeRules = intercalate "\n" . map explainDataizeRule

@@ -48,6 +48,7 @@  instance ToSingleLine PAIR where   toSingleLine PA_TAU{..} = PA_TAU attr arrow (toSingleLine expr)+  toSingleLine PA_ALPHA{..} = PA_ALPHA alpha arrow (toSingleLine expr)   toSingleLine PA_FORMATION{..} = PA_FORMATION attr voids arrow (toSingleLine expr)   toSingleLine pair = pair 

@@ -104,6 +104,11 @@         extra' = extra + lengthOf attr + lengthOf arrow + 2 -- indent + attr + arrow + 2 spaces         pa' = PA_TAU attr arrow (withMargin' (extra', margin) expr)      in if lengthOf single + extra <= margin then single else pa'+  withMargin' (extra, margin) pa@PA_ALPHA{..} =+    let single = toSingleLine pa+        extra' = extra + lengthOf alpha + lengthOf arrow + 2 -- indent + alpha + arrow + 2 spaces+        pa' = PA_ALPHA alpha arrow (withMargin' (extra', margin) expr)+     in if lengthOf single + extra <= margin then single else pa'   withMargin' (extra, margin) pa@PA_FORMATION{..} =     let single = toSingleLine pa         extra' = extra + lengthOf attr + lengthOf voids + lengthOf arrow + 4 -- indent + 2 braces + 2 spaces + voids

@@ -14,7 +14,7 @@ -- Meta value -- The right part of substitution data MetaValue-  = MvAttribute Attribute -- !a+  = MvAttribute Attribute -- !t   | MvIndex Int -- α𝑖   | MvBytes Bytes -- !b   | MvBindings [Binding] -- !B

@@ -13,7 +13,7 @@   , parseAttribute   , parseAttributeThrows   , parseAlpha-  , parseIndexMeta+  , parseIndex   , parseNumber   , parseNumberThrows   , parseBinding@@ -50,14 +50,14 @@ data PhiParser = PhiParser   { _attribute :: Parser Attribute   , _alpha :: Parser Alpha-  , _indexMeta :: Parser T.Text+  , _index :: Parser T.Text   , _binding :: Parser Binding   , _expression :: Parser Expression   , _string :: Parser String   }  phiParser :: PhiParser-phiParser = PhiParser attribute alpha indexMeta binding expression quotedStr+phiParser = PhiParser attribute alpha index' binding expression quotedStr  instance Show ParserException where   show CouldNotParseProgram{..} = printf "Couldn't parse given phi program, cause: %s" message@@ -299,7 +299,7 @@         BiLambda . Function . T.pack <$> function     , do         _ <- lambda-        BiLambda . FnMeta <$> meta 'F'+        BiLambda . FnMeta <$> meta' 'F' "𝐹"     ]     <?> "binding" @@ -328,23 +328,23 @@ attribute =   choice     [ void'-    , AtMeta <$> meta' 'a' "𝜏"+    , AtMeta <$> meta' 't' "𝜏"     ]     <?> "attribute"  -- index meta: !i, 𝑖-indexMeta :: Parser T.Text-indexMeta = meta' 'i' "𝑖"+index' :: Parser T.Text+index' = meta' 'i' "𝑖"  -- alpha--- 1. index: ~0, α0--- 2. meta: α𝑖, ~!i+-- 1. index: a0, α0+-- 2. meta: α𝑖, a!i alpha :: Parser Alpha alpha = do-  _ <- choice [symbol "~", symbol "α"]+  _ <- choice [symbol "a", symbol "α"]   choice     [ Alpha <$> lexeme L.decimal-    , AlMeta <$> indexMeta+    , AlMeta <$> index'     ]     <?> "alpha" @@ -504,8 +504,8 @@ parseAlpha :: String -> Either String Alpha parseAlpha = parse' "alpha" alpha -parseIndexMeta :: String -> Either String T.Text-parseIndexMeta = parse' "index meta" indexMeta+parseIndex :: String -> Either String T.Text+parseIndex = parse' "index meta" index'  parseAttributeThrows :: String -> IO Attribute parseAttributeThrows attr = case parseAttribute attr of

@@ -64,7 +64,7 @@    in printAttribute' att encoding  printAlpha' :: Alpha -> Encoding -> String-printAlpha' index encoding = T.unpack $ render (withEncoding encoding (toCST index (0, NO_EOL) :: ATTRIBUTE))+printAlpha' index encoding = T.unpack $ render (withEncoding encoding (toCST index (0, NO_EOL) :: ALPHA))  printAlpha :: Alpha -> String printAlpha index =

@@ -40,6 +40,11 @@       pure next  randomString :: String -> IO String-randomString pat = do-  set <- readIORef strings-  regenerate pat set+randomString pat+  | randomized pat = readIORef strings >>= regenerate pat+  | otherwise = generate pat+  where+    randomized :: String -> Bool+    randomized [] = False+    randomized ('%' : ch : rest) = ch == 'd' || ch == 'x' || randomized rest+    randomized (_ : rest) = randomized rest

@@ -67,6 +67,7 @@ instance Render RHO where   render RHO = "ρ"   render CARET = "^"+  render RHO' = "\\rho"  instance Render DELTA where   render DELTA = "Δ"@@ -117,7 +118,7 @@   render N' = "n"   render K = "𝑘"   render K' = "k"-  render A = "a"+  render A = "t"   render TAU = "𝜏"   render TAU' = "\\tau"   render I = "𝑖"@@ -126,15 +127,20 @@   render B' = "B"   render D = "δ"   render D' = "\\delta"-  render F = "F"+  render F = "𝐹"+  render F' = "F"  instance Render META where   render META{..} = render excl <> render hd <> render rest -instance Render ALPHA where+instance Render ALPHA' where   render ALPHA = "α"-  render ALPHA' = "~"+  render ALPHA' = "a" +instance Render ALPHA where+  render AL_IDX{..} = render sym <> render idx+  render AL_META{..} = render sym <> render meta+ instance Render TAB where   render TAB{..} = T.replicate indent "  "   render TAB' = " "@@ -146,6 +152,7 @@  instance Render PAIR where   render PA_TAU{..} = render attr <> render SPACE <> render arrow <> render SPACE <> render expr+  render PA_ALPHA{..} = render alpha <> render SPACE <> render arrow <> render SPACE <> render expr   render PA_FORMATION{voids = [], attr, arrow, expr} = render (PA_TAU attr arrow expr)   render PA_FORMATION{..} = render attr <> "(" <> render voids <> ")" <> render SPACE <> render arrow <> render SPACE <> render expr   render PA_LAMBDA{..} = render LAMBDA <> render SPACE <> render DASHED_ARROW <> render SPACE <> render func@@ -197,16 +204,14 @@   render EX_STRING{..} = "\"" <> render str <> "\""   render EX_NUMBER{..} = either (T.pack . show) (T.pack . show) num   render EX_META{..} = render meta-  render EX_PHI_MEET{..} = "\\phiMeet{" <> maybe "" (\p -> T.pack p <> ":") prefix <> render idx <> "}{ " <> render expr <> " }"-  render EX_PHI_AGAIN{..} = "\\phiAgain{" <> maybe "" (\p -> T.pack p <> ":") prefix <> render idx <> "}"+  render EX_PHI_MEET{..} = "\\phinoMeet{" <> maybe "" (\p -> T.pack p <> ":") prefix <> render idx <> "}{ " <> render expr <> " }"+  render EX_PHI_AGAIN{..} = "\\phinoAgain{" <> maybe "" (\p -> T.pack p <> ":") prefix <> render idx <> "}"  instance Render [ATTRIBUTE] where   render attrs = T.intercalate ", " (map render attrs)  instance Render ATTRIBUTE where   render AT_LABEL{..} = render label-  render AT_ALPHA{..} = render alpha <> render idx-  render AT_ALPHA_META{..} = render alpha <> render meta   render AT_RHO{..} = render rho   render AT_PHI{..} = render phi   render AT_LAMBDA{..} = render lambda@@ -274,5 +279,11 @@   render ARG_BYTES{..} = render bytes  instance Render EXTRA where-  render EXTRA{func = "contextualize", args = arg : rest, ..} = "$ " <> render meta <> " \\coloneqq \\ctx{ " <> render arg <> " }{ " <> T.intercalate ", " (map render rest) <> " } $"-  render EXTRA{..} = "$ " <> render meta <> " \\coloneqq " <> T.pack func <> "( " <> T.intercalate ", " (map render args) <> " ) $"+  render EXTRA{func = "contextualize", args = arg : rest, ..} = render meta <> " \\coloneqq \\ctx{ " <> render arg <> " }{ " <> T.intercalate ", " (map render rest) <> " }"+  render EXTRA{..} = render meta <> " \\coloneqq " <> macro func <> "{ " <> T.intercalate ", " (map render args) <> " }"+    where+      macro :: String -> Text+      macro "lambda" = "\\phinoEvaluate"+      macro "morph" = "\\phinoMorph"+      macro "global" = "\\phinoGlobal"+      macro name = "\\" <> T.pack name

@@ -51,7 +51,7 @@ --  | a -> "Hey"                 | Q.number(Q.bytes([[ D> 48-65-79 ]]))                | --  | [[ B ]]                    | [[ B, ^ -> ? ]], if rho is absent in 'B'            | --  | a1(a2, a3, ...) -> [[ B ]] | a1 -> [[ a2 -> ?, a3 -> ?, ..., B ]]                |---  | e(e0, e1, ...)             | e(~0 -> e0, ~1 -> e1, ...)                          |+--  | e(e0, e1, ...)             | e(a0 -> e0, a1 -> e1, ...)                          | --  | e(a1 -> e1, a2 -> e2, ...) | e(a1 -> e1)(a2 -> e2)...                            | --  |----------------------------|-----------------------------------------------------| class ToSalty a where@@ -89,11 +89,11 @@       argToBinding :: APP_ARG -> TAB -> BINDING       argToBinding APP_ARG{..} =         BI_PAIR-          (PA_TAU (AT_ALPHA ALPHA 0) ARROW expr)+          (PA_ALPHA (AL_IDX ALPHA 0) ARROW expr)           (argsToBindings args 1 tab)       argsToBindings :: APP_ARGS -> Int -> TAB -> BINDINGS       argsToBindings AAS_EMPTY _ tab = BDS_EMPTY tab-      argsToBindings AAS_EXPR{..} idx tb = BDS_PAIR eol tb (PA_TAU (AT_ALPHA ALPHA idx) ARROW expr) (argsToBindings args (idx + 1) tb)+      argsToBindings AAS_EXPR{..} idx tb = BDS_PAIR eol tb (PA_ALPHA (AL_IDX ALPHA idx) ARROW expr) (argsToBindings args (idx + 1) tb)   toSalty EX_NUMBER{num, tab = tab@TAB{..}, rhos} =     saltifyPrimitive       (toCST (BaseObject "number") (indent + 1, EOL))@@ -122,8 +122,8 @@             EOL             next             ( BI_PAIR-                ( PA_TAU-                    (AT_ALPHA ALPHA 0)+                ( PA_ALPHA+                    (AL_IDX ALPHA 0)                     ARROW                     ( EX_APPLICATION_EXPRS                         bytes@@ -159,6 +159,7 @@  instance ToSalty PAIR where   toSalty PA_TAU{..} = PA_TAU attr arrow (toSalty expr)+  toSalty PA_ALPHA{..} = PA_ALPHA alpha arrow (toSalty expr)   toSalty PA_FORMATION{voids, attr, arrow, expr = EX_FORMATION{..}} =     PA_TAU attr arrow (toSalty (EX_FORMATION lsb eol tab (joinToBinding voids binding) eol' tab' rsb))     where

@@ -64,7 +64,7 @@         , Domain <$> o .: "domain"         ]     Number num -> pure (Literal (round num))-    String txt -> case parseIndexMeta (unpack txt) of+    String txt -> case parseIndex (unpack txt) of       Right mt -> pure (MetaIndex mt)       Left err -> fail err     _ ->

@@ -59,8 +59,8 @@    describe "Attribute Show instance renders AtMeta" $     forM_-      [ ("simple meta", AtMeta "a", "!a")-      , ("long meta", AtMeta "attribute", "!attribute")+      [ ("simple meta", AtMeta "t", "!t")+      , ("long meta", AtMeta "tttribute", "!tttribute")       , ("unicode meta", AtMeta "メタ", "!メタ")       ]       ( \(desc, attr, expected) ->@@ -71,8 +71,8 @@     forM_       [ ("labels equal", AtLabel "x", AtLabel "x", True)       , ("labels differ", AtLabel "x", AtLabel "y", False)-      , ("metas equal", AtMeta "a", AtMeta "a", True)-      , ("metas differ", AtMeta "a", AtMeta "b", False)+      , ("metas equal", AtMeta "t", AtMeta "t", True)+      , ("metas differ", AtMeta "t", AtMeta "b", False)       , ("rho equals rho", AtRho, AtRho, True)       , ("phi equals phi", AtPhi, AtPhi, True)       , ("delta equals delta", AtDelta, AtDelta, True)

@@ -25,21 +25,21 @@     test       buildExpression       [-        ( "Q.!a => (!a >> x) => Q.x"-        , ExDispatch ExRoot (AtMeta "a")-        , [("a", MvAttribute (AtLabel "x"))]+        ( "Q.!t => (!t >> x) => Q.x"+        , ExDispatch ExRoot (AtMeta "t")+        , [("t", MvAttribute (AtLabel "x"))]         , Right (ExDispatch ExRoot (AtLabel "x"))         )       ,-        ( "Q.c(!a -> !e) => (!a >> x, !e >> $.y.z) => Q.c(x -> $.y.z)"-        , ExApplication (ExDispatch ExRoot (AtLabel "c")) (ArTau (AtMeta "a") (ExMeta "e"))-        , [("a", MvAttribute (AtLabel "x")), ("e", MvExpression (ExDispatch (ExDispatch ExXi (AtLabel "y")) (AtLabel "z")))]+        ( "Q.c(!t -> !e) => (!t >> x, !e >> $.y.z) => Q.c(x -> $.y.z)"+        , ExApplication (ExDispatch ExRoot (AtLabel "c")) (ArTau (AtMeta "t") (ExMeta "e"))+        , [("t", MvAttribute (AtLabel "x")), ("e", MvExpression (ExDispatch (ExDispatch ExXi (AtLabel "y")) (AtLabel "z")))]         , Right (ExApplication (ExDispatch ExRoot (AtLabel "c")) (ArTau (AtLabel "x") (ExDispatch (ExDispatch ExXi (AtLabel "y")) (AtLabel "z"))))         )       ,-        ( "[[!a -> $.x, !B]] => (!a >> y, !B >> [[b -> ?, L> Func]]) => [[y -> $.x, b -> ?, L> Func]]"-        , ExFormation [BiTau (AtMeta "a") (ExDispatch ExXi (AtLabel "x")), BiMeta "B"]-        , [("a", MvAttribute (AtLabel "y")), ("B", MvBindings [BiVoid (AtLabel "b"), BiLambda (Function "Func")])]+        ( "[[!t -> $.x, !B]] => (!t >> y, !B >> [[b -> ?, L> Func]]) => [[y -> $.x, b -> ?, L> Func]]"+        , ExFormation [BiTau (AtMeta "t") (ExDispatch ExXi (AtLabel "x")), BiMeta "B"]+        , [("t", MvAttribute (AtLabel "y")), ("B", MvBindings [BiVoid (AtLabel "b"), BiLambda (Function "Func")])]         , Right             ( ExFormation                 [ BiTau (AtLabel "y") (ExDispatch ExXi (AtLabel "x"))@@ -49,28 +49,28 @@             )         )       ,-        ( "Q.!a => () => X"-        , ExDispatch ExRoot (AtMeta "a")+        ( "Q.!t => () => X"+        , ExDispatch ExRoot (AtMeta "t")         , []-        , Left "meta 'a' is either does not exist or refers to an inappropriate term"+        , Left "meta 't' is either does not exist or refers to an inappropriate term"         )       ,-        ( "!e0(!a1 -> !e1, !a2 => !e2) => (!e0 >> [[]], !a1 >> x, !e1 >> Q, !a2 >> y, !e2 >> $) => [[]](x -> Q, y -> $)"-        , ExApplication (ExApplication (ExMeta "e0") (ArTau (AtMeta "a1") (ExMeta "e1"))) (ArTau (AtMeta "a2") (ExMeta "e2"))+        ( "!e0(!t1 -> !e1, !t2 => !e2) => (!e0 >> [[]], !t1 >> x, !e1 >> Q, !t2 >> y, !e2 >> $) => [[]](x -> Q, y -> $)"+        , ExApplication (ExApplication (ExMeta "e0") (ArTau (AtMeta "t1") (ExMeta "e1"))) (ArTau (AtMeta "t2") (ExMeta "e2"))         ,           [ ("e0", MvExpression (ExFormation []))-          , ("a1", MvAttribute (AtLabel "x"))+          , ("t1", MvAttribute (AtLabel "x"))           , ("e1", MvExpression ExRoot)-          , ("a2", MvAttribute (AtLabel "y"))+          , ("t2", MvAttribute (AtLabel "y"))           , ("e2", MvExpression ExXi)           ]         , Right (ExApplication (ExApplication (ExFormation []) (ArTau (AtLabel "x") ExRoot)) (ArTau (AtLabel "y") ExXi))         )       ,-        ( "⟦!a ↦ ∅, !B⟧.!a => (!a >> t, !B >> ⟦ x ↦ ξ.t ⟧ ) => ⟦ t ↦ ∅, x ↦ ξ.t ⟧.t"-        , ExDispatch (ExFormation [BiVoid (AtMeta "a"), BiMeta "B"]) (AtMeta "a")+        ( "⟦!t ↦ ∅, !B⟧.!t => (!t >> t, !B >> ⟦ x ↦ ξ.t ⟧ ) => ⟦ t ↦ ∅, x ↦ ξ.t ⟧.t"+        , ExDispatch (ExFormation [BiVoid (AtMeta "t"), BiMeta "B"]) (AtMeta "t")         ,-          [ ("a", MvAttribute (AtLabel "t"))+          [ ("t", MvAttribute (AtLabel "t"))           , ("B", MvBindings [BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))])           ]         , Right

@@ -211,13 +211,16 @@             ["rewrite", rule "first.yaml", rule "second.yaml", "--max-depth=1", "--max-cycles=3"]             ["it seems rewriting is looping"] +      -- Only assert the stable parts of the parse error: phino's envelope and+      -- that megaparsec reports an 'unexpected' token. The exact line:column and+      -- offending token depend on megaparsec's internal try/longest-match error+      -- merging, which shifts between megaparsec releases (deps are unpinned), so+      -- pinning them here makes the test brittle without testing anything extra.       it "with wrong attribute and valid error message" $         testCLIFailed           ["rewrite", resource "with-$this-attribute.phi"]-          [ "[ERROR]: Couldn't parse given phi program, cause: program:10:13:"-          , "10 |             $this ↦ ⟦⟧"-          , "   |             ^^"-          , "unexpected \"$t\""+          [ "[ERROR]: Couldn't parse given phi program, cause:"+          , "unexpected"           ]        it "with --output != latex and --nonumber" $@@ -420,7 +423,7 @@               , "  |x\\char95{}o| -> Q . |z| ( |y| -> 5 ),"               , "  |q\\char36{}| -> T,"               , "  |w| -> $,"-              , "  ^ -> Q,"+              , "  \\rho -> Q,"               , "  @ -> 1,"               , "  |y| -> \"H$@^M\","               , "  L> |Fu\\char95{}nc|"@@ -440,6 +443,17 @@               ]           ] +    it "rewrites an alpha-index argument as \\alpha subscript in LaTeX" $+      withStdin "Q -> Q.foo(a1 -> Q.y)" $+        testCLISucceeded+          ["rewrite", "--output=latex", "--flat", "--nonumber"]+          [ unlines+              [ "\\begin{phiquation*}"+              , "Q -> Q . |foo| ( \\alpha_{1} -> Q . |y| ){.}"+              , "\\end{phiquation*}"+              ]+          ]+     it "rewrite as LaTeX with expression name" $       withStdin "Q -> [[ x -> 5 ]]" $         testCLISucceeded@@ -542,12 +556,12 @@           ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress", "--meet-prefix=foo"]           [ unlines               [ "\\begin{phiquation}"-              , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phiMeet{foo:1}{ [[ D> 42- ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto \\Big\\{ \\phiMeet{foo:2}{ [[ |x| -> \\phiAgain{foo:1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}"-              , "  \\leadsto \\Big\\{ \\phiAgain{foo:2} . |x| ( ^ -> \\phiAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}"-              , "  \\leadsto \\Big\\{ \\phiAgain{foo:1} ( ^ -> \\phiAgain{foo:2}, ^ -> \\phiAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto \\Big\\{ [[ D> 42-, ^ -> \\phiAgain{foo:2} ]] ( ^ -> \\phiAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"-              , "  \\leadsto \\Big\\{ [[ D> 42-, ^ -> \\phiAgain{foo:2} ]] \\Big\\}{.}"+              , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{foo:1}{ [[ D> 42- ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto \\Big\\{ \\phinoMeet{foo:2}{ [[ |x| -> \\phinoAgain{foo:1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}"+              , "  \\leadsto \\Big\\{ \\phinoAgain{foo:2} . |x| ( \\rho -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}"+              , "  \\leadsto \\Big\\{ \\phinoAgain{foo:1} ( \\rho -> \\phinoAgain{foo:2}, \\rho -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto \\Big\\{ [[ D> 42-, \\rho -> \\phinoAgain{foo:2} ]] ( \\rho -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"+              , "  \\leadsto \\Big\\{ [[ D> 42-, \\rho -> \\phinoAgain{foo:2} ]] \\Big\\}{.}"               , "\\end{phiquation}"               ]           ]@@ -558,24 +572,24 @@           ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress"]           [ unlines               [ "\\begin{phiquation}"-              , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phiMeet{1}{ [[ D> 42- ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto \\Big\\{ \\phiMeet{2}{ [[ |x| -> \\phiAgain{1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}"-              , "  \\leadsto \\Big\\{ \\phiAgain{2} . |x| ( ^ -> \\phiAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}"-              , "  \\leadsto \\Big\\{ \\phiAgain{1} ( ^ -> \\phiAgain{2}, ^ -> \\phiAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto \\Big\\{ [[ D> 42-, ^ -> \\phiAgain{2} ]] ( ^ -> \\phiAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"-              , "  \\leadsto \\Big\\{ [[ D> 42-, ^ -> \\phiAgain{2} ]] \\Big\\}{.}"+              , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{1}{ [[ D> 42- ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto \\Big\\{ \\phinoMeet{2}{ [[ |x| -> \\phinoAgain{1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}"+              , "  \\leadsto \\Big\\{ \\phinoAgain{2} . |x| ( \\rho -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}"+              , "  \\leadsto \\Big\\{ \\phinoAgain{1} ( \\rho -> \\phinoAgain{2}, \\rho -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto \\Big\\{ [[ D> 42-, \\rho -> \\phinoAgain{2} ]] ( \\rho -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"+              , "  \\leadsto \\Big\\{ [[ D> 42-, \\rho -> \\phinoAgain{2} ]] \\Big\\}{.}"               , "\\end{phiquation}"               ]           ] -    it "should not print \\phiMeet{} twice" $+    it "should not print \\phinoMeet{} twice" $       withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $         testCLISucceeded           ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet"]           [ unlines               [ "\\begin{phiquation}"-              , "\\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> \\phiMeet{1}{ [[ |t| -> 42 ]] } ]] ( |y| -> \\phiAgain{1} ) ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto \\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> \\phiAgain{1}, |k| -> \\phiAgain{1} ]] ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:stop}}"+              , "\\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> \\phinoMeet{1}{ [[ |t| -> 42 ]] } ]] ( |y| -> \\phinoAgain{1} ) ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto \\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> \\phinoAgain{1}, |k| -> \\phinoAgain{1} ]] ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:stop}}"               , "  \\leadsto \\Big\\{ [[ |ex| -> T ]] \\Big\\}{.}"               , "\\end{phiquation}"               ]@@ -638,7 +652,7 @@           [ unlines               [ "\\begin{phiquation}"               , "\\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}"-              , "  \\leadsto \\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |y| ( ^ -> [[ |x| -> |y|, |y| -> |x| ]] ) \\Big\\} \\leadsto"+              , "  \\leadsto \\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |y| ( \\rho -> [[ |x| -> |y|, |y| -> |x| ]] ) \\Big\\} \\leadsto"               , "  \\leadsto \\dots"               , "\\end{phiquation}"               ]@@ -867,8 +881,8 @@               , "\\Big\\{ [[ @ -> [[ |x| -> [[ D> 01-, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| ]] \\Big\\} \\leadsto_{\\nameref{r:contextualize}}"               , "  \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:copy}}"               , "  \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}"-              , "  \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]] ]] ( ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\}{.}"+              , "  \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]] ]] ( \\rho -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], \\rho -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\}{.}"               , "\\end{phiquation}"               , "01-"               ]@@ -878,7 +892,7 @@       withStdin "{[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]}" $         testCLISucceeded           ["dataize", "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--hide=Q.bytes", "--hide=Q.number", "--locator=Q.@", "--focus=Q.@", "--meet-length=5", "--meet-popularity=1"]-          ["\\phiMeet{dataization:1}{ [[ @ -> |c| . |plus| ( 32 ), |c| -> 25 ]] } \\leadsto_{\\nameref{r:contextualize}}"]+          ["\\phinoMeet{dataization:1}{ [[ @ -> |c| . |plus| ( 32 ), |c| -> 25 ]] } \\leadsto_{\\nameref{r:contextualize}}"]      it "dataizes with --locator" $       withStdin "{[[ ex -> [[ @ -> Q.x ]], x -> [[ D> 42- ]] ]]}" $@@ -930,87 +944,83 @@       testCLISucceeded         ["explain", "--rule=resources/normalize/copy.yaml"]         [ unlines-            [ "\\begin{tabular}{rl}"-            , "\\trrule{copy}"+            [ "\\phinoNormalizationRule{copy}"             , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"             , "  { [[ B_1, \\tau -> k, B_2 ]] }"             , "  { }"             , "  { }"-            , "\\end{tabular}"             ]         ]      it "explains multiple rules" $       testCLISucceeded         ["explain", "--rule=resources/normalize/copy.yaml", "--rule=resources/normalize/alpha.yaml"]-        ["\\begin{tabular}{rl}", "\\trrule{copy}", "\\trrule{alpha}"]+        ["\\phinoNormalizationRule{copy}", "\\phinoNormalizationRule{alpha}"]      it "explains normalization rules" $       testCLISucceeded         ["explain", "--normalize"]         [ unlines-            [ "\\begin{tabular}{rl}"-            , "\\trrule{alpha}"+            [ "\\phinoNormalizationRule{alpha}"             , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\alpha_{i} -> e ) }"             , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }"-            , "  { if $ i = \\vert \\overline{ B_1 } \\vert $ }"+            , "  { i = \\vert \\overline{ B_1 } \\vert }"             , "  { }"-            , "\\trrule{copy}"+            , "\\phinoNormalizationRule{copy}"             , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"             , "  { [[ B_1, \\tau -> k, B_2 ]] }"             , "  { }"             , "  { }"-            , "\\trrule{dc}"+            , "\\phinoNormalizationRule{dc}"             , "  { T ( \\tau -> e ) }"             , "  { T }"             , "  { }"             , "  { }"-            , "\\trrule{dca}"+            , "\\phinoNormalizationRule{dca}"             , "  { T ( \\alpha_{i} -> e ) }"             , "  { T }"             , "  { }"             , "  { }"-            , "\\trrule{dd}"+            , "\\phinoNormalizationRule{dd}"             , "  { T . \\tau }"             , "  { T }"             , "  { }"             , "  { }"-            , "\\trrule{dot}"+            , "\\phinoNormalizationRule{dot}"             , "  { [[ B_1, \\tau -> n, B_2 ]] . \\tau }"-            , "  { e ( ^ -> [[ B_1, \\tau -> n, B_2 ]] ) }"+            , "  { e ( \\rho -> [[ B_1, \\tau -> n, B_2 ]] ) }"             , "  { }"-            , "  { where $ e \\coloneqq \\ctx{ n }{ [[ B_1, \\tau -> n, B_2 ]] } $ }"-            , "\\trrule{miss}"+            , "  { e \\coloneqq \\ctx{ n }{ [[ B_1, \\tau -> n, B_2 ]] } }"+            , "\\phinoNormalizationRule{miss}"             , "  { [[ B ]] ( \\tau -> e ) }"             , "  { T }"-            , "  { if $ \\tau \\notin B $ }"+            , "  { \\tau \\notin B }"             , "  { }"-            , "\\trrule{null}"+            , "\\phinoNormalizationRule{null}"             , "  { [[ B_1, \\tau -> ?, B_2 ]] . \\tau }"             , "  { T }"             , "  { }"             , "  { }"-            , "\\trrule{over}"+            , "\\phinoNormalizationRule{over}"             , "  { [[ B_1, \\tau -> e_1, B_2 ]] ( \\tau -> e_2 ) }"             , "  { T }"-            , "  { if $ \\tau \\not= ^ $ }"+            , "  { \\tau \\not= \\rho }"             , "  { }"-            , "\\trrule{phi}"+            , "\\phinoNormalizationRule{phi}"             , "  { [[ B ]] . \\tau }"             , "  { [[ B ]] . @ . \\tau }"-            , "  { if $ @ \\in B \\;\\text{and}\\; \\tau \\notin B $ }"+            , "  { @ \\in B \\;\\text{and}\\; \\tau \\notin B }"             , "  { }"-            , "\\trrule{stay}"-            , "  { [[ B_1, ^ -> e_1, B_2 ]] ( ^ -> e_2 ) }"-            , "  { [[ B_1, ^ -> e_1, B_2 ]] }"+            , "\\phinoNormalizationRule{stay}"+            , "  { [[ B_1, \\rho -> e_1, B_2 ]] ( \\rho -> e_2 ) }"+            , "  { [[ B_1, \\rho -> e_1, B_2 ]] }"             , "  { }"             , "  { }"-            , "\\trrule{stop}"+            , "\\phinoNormalizationRule{stop}"             , "  { [[ B ]] . \\tau }"             , "  { T }"-            , "  { if $ \\tau \\notin B \\;\\text{and}\\; @ \\notin B \\;\\text{and}\\; L \\notin B $ }"+            , "  { \\tau \\notin B \\;\\text{and}\\; @ \\notin B \\;\\text{and}\\; L \\notin B }"             , "  { }"-            , "\\end{tabular}"             ]         ] @@ -1018,43 +1028,51 @@       testCLISucceeded         ["explain", "--morph"]         [ unlines-            [ "\\begin{tabular}{rl}"-            , "\\trrule{prim}"+            [ "\\phinoMorphingRule{prim}"             , "  { \\mathbb{M}( [[ B ]] ) }"             , "  { [[ B ]] }"             , "  { }"             , "  { }"-            , "\\trrule{lambda}"+            , "\\phinoMorphingRule{lambda}"             , "  { \\mathbb{M}( [[ B_1, L> F, B_2 ]] . \\tau ) }"-            , "  { \\mathbb{M}( \\mathcal{N}( e . \\tau ) ) }"+            , "  { \\mathbb{M}( \\phinoNormalize{ e . \\tau } ) }"             , "  { }"-            , "  { where $ e \\coloneqq lambda( [[ B_1, L> F, B_2 ]] ) $ }"-            , "\\trrule{dispatch}"+            , "  { e \\coloneqq \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] } }"+            , "\\phinoMorphingRule{dispatch}"             , "  { \\mathbb{M}( n . \\tau ) }"-            , "  { \\mathbb{M}( \\mathcal{N}( e . \\tau ) ) }"+            , "  { \\mathbb{M}( \\phinoNormalize{ e . \\tau } ) }"             , "  { }"-            , "  { where $ e \\coloneqq morph( n ) $ }"-            , "\\trrule{application}"+            , "  { e \\coloneqq \\phinoMorph{ n } }"+            , "\\phinoMorphingRule{application}"             , "  { \\mathbb{M}( n ( \\tau -> e ) ) }"-            , "  { \\mathbb{M}( \\mathcal{N}( e_1 ( \\tau -> e ) ) ) }"+            , "  { \\mathbb{M}( \\phinoNormalize{ e_1 ( \\tau -> e ) } ) }"             , "  { }"-            , "  { where $ e_1 \\coloneqq morph( n ) $ }"-            , "\\trrule{applicationa}"+            , "  { e_1 \\coloneqq \\phinoMorph{ n } }"+            , "\\phinoMorphingRule{applicationa}"             , "  { \\mathbb{M}( n ( \\alpha_{i} -> e ) ) }"-            , "  { \\mathbb{M}( \\mathcal{N}( e_1 ( \\alpha_{i} -> e ) ) ) }"+            , "  { \\mathbb{M}( \\phinoNormalize{ e_1 ( \\alpha_{i} -> e ) } ) }"             , "  { }"-            , "  { where $ e_1 \\coloneqq morph( n ) $ }"-            , "\\trrule{root}"+            , "  { e_1 \\coloneqq \\phinoMorph{ n } }"+            , "\\phinoMorphingRule{root}"             , "  { \\mathbb{M}( Q ) }"-            , "  { \\mathbb{M}( \\mathcal{N}( e ) ) }"-            , "  { if $ e \\not= Q $ }"-            , "  { where $ e \\coloneqq global(  ) $ }"-            , "\\trrule{stuck}"-            , "  { \\mathbb{M}( n ) }"+            , "  { \\mathbb{M}( \\phinoNormalize{ e } ) }"+            , "  { e \\not= Q }"+            , "  { e \\coloneqq \\phinoGlobal{  } }"+            , "\\phinoMorphingRule{dead}"+            , "  { \\mathbb{M}( T ) }"             , "  { T }"             , "  { }"             , "  { }"-            , "\\end{tabular}"+            , "\\phinoMorphingRule{xi}"+            , "  { \\mathbb{M}( $ ) }"+            , "  { T }"+            , "  { }"+            , "  { }"+            , "\\phinoMorphingRule{globe}"+            , "  { \\mathbb{M}( Q ) }"+            , "  { T }"+            , "  { }"+            , "  { }"             ]         ] @@ -1062,38 +1080,36 @@       testCLISucceeded         ["explain", "--dataize"]         [ unlines-            [ "\\begin{tabular}{rl}"-            , "\\trrule{delta}"+            [ "\\phinoDataizationRule{delta}"             , "  { \\mathbb{D}( [[ B_1, D> \\delta, B_2 ]] ) }"             , "  { \\delta }"             , "  { }"             , "  { }"-            , "\\trrule{box}"+            , "\\phinoDataizationRule{box}"             , "  { \\mathbb{D}( [[ B_1, @ -> e, B_2 ]] ) }"-            , "  { \\mathbb{D}( \\mathcal{N}( e_1 ) ) }"-            , "  { if $ [ \\Delta, L ] \\cap ( B_1 \\cup B_2 ) = \\emptyset $ }"-            , "  { where $ e_1 \\coloneqq \\ctx{ e }{ [[ B_1, @ -> e, B_2 ]] } $ }"-            , "\\trrule{fire}"+            , "  { \\mathbb{D}( \\phinoNormalize{ e_1 } ) }"+            , "  { [ \\Delta, L ] \\cap ( B_1 \\cup B_2 ) = \\emptyset }"+            , "  { e_1 \\coloneqq \\ctx{ e }{ [[ B_1, @ -> e, B_2 ]] } }"+            , "\\phinoDataizationRule{fire}"             , "  { \\mathbb{D}( [[ B_1, L> F, B_2 ]] ) }"-            , "  { \\mathbb{D}( \\mathcal{N}( e ) ) }"+            , "  { \\mathbb{D}( \\phinoNormalize{ e } ) }"             , "  { }"-            , "  { where $ e \\coloneqq lambda( [[ B_1, L> F, B_2 ]] ) $ }"-            , "\\trrule{none}"+            , "  { e \\coloneqq \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] } }"+            , "\\phinoDataizationRule{none}"             , "  { \\mathbb{D}( [[ B ]] ) }"             , "  { \\varnothing }"             , "  { }"             , "  { }"-            , "\\trrule{bott}"+            , "\\phinoDataizationRule{bott}"             , "  { \\mathbb{D}( T ) }"             , "  { \\varnothing }"             , "  { }"             , "  { }"-            , "\\trrule{norm}"+            , "\\phinoDataizationRule{norm}"             , "  { \\mathbb{D}( n ) }"             , "  { \\mathbb{D}( \\mathbb{M}( n ) ) }"             , "  { }"             , "  { }"-            , "\\end{tabular}"             ]         ] @@ -1121,8 +1137,7 @@             testCLISucceeded ["explain", "--normalize", printf "--target=%s" path] []             content <- readFile path             _ <- evaluate (length content)-            content `shouldContain` "\\begin{tabular}{rl}"-            content `shouldContain` "\\end{tabular}"+            content `shouldContain` "\\phinoNormalizationRule{alpha}"         )    describe "merge" $ do@@ -1178,17 +1193,17 @@      it "prints one substitution" $       withStdin "{[[ x -> Q.x ]]}" $-        testCLISucceeded ["match", "--pattern=Q.!a"] ["a >> x"]+        testCLISucceeded ["match", "--pattern=Q.!t"] ["t >> x"]      it "prints many substitutions" $       withStdin "{[[ x -> Q.x, y -> Q.y ]]}" $-        testCLISucceeded ["match", "--pattern=Q.!a"] ["a >> x\n------\na >> y"]+        testCLISucceeded ["match", "--pattern=Q.!t"] ["t >> x\n------\nt >> y"]      it "builds substitutions with conditions" $       withStdin "{[[ x -> Q.y ]].x}" $         testCLISucceeded-          ["match", "--pattern=[[ !a -> Q.y, !B ]].!a", "--when=eq(length(!B),1)"]-          ["B >> ⟦ ρ ↦ ∅ ⟧\na >> x"]+          ["match", "--pattern=[[ !t -> Q.y, !B ]].!t", "--when=eq(length(!B),1)"]+          ["B >> ⟦ ρ ↦ ∅ ⟧\nt >> x"]      it "builds with condition from file" $       testCLISucceeded@@ -1204,5 +1219,5 @@     it "fails on empty substitutions" $       withStdin "{Q.x.y}" $         testCLIFailed-          ["match", "--pattern=$.!a"]+          ["match", "--pattern=$.!t"]           ["[ERROR]"]

@@ -60,7 +60,7 @@           programToCST ast `shouldBe` cst       ) -  describe "build valid CST with wrapped phiAgain{} " $ do+  describe "build valid CST with wrapped phinoAgain{} " $ do     let number = BaseObject "number"         again = ExPhiAgain Nothing 1         bts = BaseObject "bytes"

@@ -16,10 +16,10 @@ spec = do   describe "just parses" $     forM_-      [ "in (!a, !B)"-      , " not   (in (!a1,   !B))   "+      [ "in (!t, !B)"+      , " not   (in (!t1,   !B))   "       , "eq(1, 1)"-      , "or(eq(!i,1),eq(length(!B),-2),eq(!e1,!e2),eq(!a1,x),eq(Q.org.eolang,[[ x -> 2 ]]))"+      , "or(eq(!i,1),eq(length(!B),-2),eq(!e1,!e2),eq(!t1,x),eq(Q.org.eolang,[[ x -> 2 ]]))"       , "nf([[ x -> !e ]].x)"       , "absolute(!e1)"       , "matches(\"hello(\\\"\\u0000)\", !e)"@@ -29,12 +29,12 @@    describe "parses correctly" $     forM_-      [ ("in(!a, !B)", Y.In (AtMeta "a") (BiMeta "B"))-      , ("not(in(!a,!B))", Y.Not (Y.In (AtMeta "a") (BiMeta "B")))+      [ ("in(!t, !B)", Y.In (AtMeta "t") (BiMeta "B"))+      , ("not(in(!t,!B))", Y.Not (Y.In (AtMeta "t") (BiMeta "B")))       , ("eq(1,-2)", Y.Eq (Y.CmpNum (Y.Literal 1)) (Y.CmpNum (Y.Literal (-2))))       , ("eq(!i,length(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i")) (Y.CmpNum (Y.Length (BiMeta "B1"))))       , ("eq(!i2,domain(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i2")) (Y.CmpNum (Y.Domain (BiMeta "B1"))))-      , ("eq(!a1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "a1")) (Y.CmpExpr (ExMeta "e2")))+      , ("eq(!t1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "t1")) (Y.CmpExpr (ExMeta "e2")))       , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (ExMeta "e1"), Y.NF (ExDispatch ExRoot (AtLabel "x"))])       , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")])       ]@@ -43,7 +43,7 @@   describe "does not parse" $     forM_       [ "some()"-      , "in(!a, !a)"+      , "in(!t, !t)"       , "or(or(), or())"       ]       (\expr -> it expr (parseCondition expr `shouldSatisfy` isLeft))

@@ -42,23 +42,23 @@         , substs [[], []]         )       ,-        ( "Q.!a => [[ @ -> Q.y, ^ -> [[ a -> Q.w ]], @ -> Q.y ]] => [(a >> y), (a >> w), (a >> y)]"-        , ExDispatch ExRoot (AtMeta "a")+        ( "Q.!t => [[ @ -> Q.y, ^ -> [[ a -> Q.w ]], @ -> Q.y ]] => [(t >> y), (t >> w), (t >> y)]"+        , ExDispatch ExRoot (AtMeta "t")         , ExFormation             [ BiTau AtPhi (ExDispatch ExRoot (AtLabel "y"))             , BiTau AtRho (ExFormation [BiTau (AtLabel "a") (ExDispatch ExRoot (AtLabel "w"))])             , BiTau AtPhi (ExDispatch ExRoot (AtLabel "y"))             ]-        , substs [[("a", MvAttribute (AtLabel "y"))], [("a", MvAttribute (AtLabel "w"))], [("a", MvAttribute (AtLabel "y"))]]+        , substs [[("t", MvAttribute (AtLabel "y"))], [("t", MvAttribute (AtLabel "w"))], [("t", MvAttribute (AtLabel "y"))]]         )       ,-        ( "[[!a -> Q.org.!a]] => [[f -> [[x -> Q.org.x]], t -> [[y -> Q.org.y]] => [(!a >> x), (!a >> y)]"-        , ExFormation [BiTau (AtMeta "a") (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtMeta "a"))]+        ( "[[!t -> Q.org.!t]] => [[f -> [[x -> Q.org.x]], t -> [[y -> Q.org.y]] => [(!t >> x), (!t >> y)]"+        , ExFormation [BiTau (AtMeta "t") (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtMeta "t"))]         , ExFormation             [ BiTau (AtLabel "f") (ExFormation [BiTau (AtLabel "x") (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "x"))])             , BiTau (AtLabel "t") (ExFormation [BiTau (AtLabel "y") (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "y"))])             ]-        , substs [[("a", MvAttribute (AtLabel "x"))], [("a", MvAttribute (AtLabel "y"))]]+        , substs [[("t", MvAttribute (AtLabel "x"))], [("t", MvAttribute (AtLabel "y"))]]         )       ,         ( "!e => [[x -> Q]] => [(!e >> [[x -> Q]] ), (!e >> Q)]"@@ -70,17 +70,17 @@             ]         )       ,-        ( "!e.!a => Q.org.eolang => [(!e >> Q.org, !a >> eolang), (!e >> Q, !a >> org)]"-        , ExDispatch (ExMeta "e") (AtMeta "a")+        ( "!e.!t => Q.org.eolang => [(!e >> Q.org, !t >> eolang), (!e >> Q, !t >> org)]"+        , ExDispatch (ExMeta "e") (AtMeta "t")         , ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang")         , substs-            [ [("e", MvExpression (ExDispatch ExRoot (AtLabel "org"))), ("a", MvAttribute (AtLabel "eolang"))]-            , [("e", MvExpression ExRoot), ("a", MvAttribute (AtLabel "org"))]+            [ [("e", MvExpression (ExDispatch ExRoot (AtLabel "org"))), ("t", MvAttribute (AtLabel "eolang"))]+            , [("e", MvExpression ExRoot), ("t", MvAttribute (AtLabel "org"))]             ]         )       ,-        ( "⟦!B1, !a ↦ ∅, !B2⟧.!a => ⟦ x ↦ ξ.t, t ↦ ∅ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧) => [(!B1 >> ⟦x ↦ ξ.t⟧, !a >> t, !B2 >> ⟦⟧ )]"-        , ExDispatch (ExFormation [BiMeta "B1", BiVoid (AtMeta "a"), BiMeta "B2"]) (AtMeta "a")+        ( "⟦!B1, !t ↦ ∅, !B2⟧.!t => ⟦ x ↦ ξ.t, t ↦ ∅ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧) => [(!B1 >> ⟦x ↦ ξ.t⟧, !t >> t, !B2 >> ⟦⟧ )]"+        , ExDispatch (ExFormation [BiMeta "B1", BiVoid (AtMeta "t"), BiMeta "B2"]) (AtMeta "t")         , ExApplication             ( ExDispatch                 ( ExFormation@@ -101,7 +101,7 @@         , substs             [               [ ("B1", MvBindings [BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))])-              , ("a", MvAttribute (AtLabel "t"))+              , ("t", MvAttribute (AtLabel "t"))               , ("B2", MvBindings [])               ]             ]@@ -152,8 +152,8 @@    describe "matchAttribute: attribute => attribute => substitution" $     forM_-      [ ("!a => ^ => [(!a >> ^)]", AtMeta "a", AtRho, substs [[("a", MvAttribute AtRho)]])-      , ("!a => @ => [(!a >> @)]", AtMeta "a", AtPhi, substs [[("a", MvAttribute AtPhi)]])+      [ ("!t => ^ => [(!t >> ^)]", AtMeta "t", AtRho, substs [[("t", MvAttribute AtRho)]])+      , ("!t => @ => [(!t >> @)]", AtMeta "t", AtPhi, substs [[("t", MvAttribute AtPhi)]])       ]       ( \(desc, ptn, tgt, expected) ->           it desc $ matchAttribute ptn tgt `shouldBe` expected@@ -190,10 +190,10 @@         , substs []         )       ,-        ( "[[y -> ?, !a -> ?]] => [[y -> ?, x -> ?]] => (!a >> x)"-        , [BiVoid (AtLabel "y"), BiVoid (AtMeta "a")]+        ( "[[y -> ?, !t -> ?]] => [[y -> ?, x -> ?]] => (!t >> x)"+        , [BiVoid (AtLabel "y"), BiVoid (AtMeta "t")]         , [BiVoid (AtLabel "y"), BiVoid (AtLabel "x")]-        , substs [[("a", MvAttribute (AtLabel "x"))]]+        , substs [[("t", MvAttribute (AtLabel "x"))]]         )       ,         ( "[[!B, x -> ?]] => [[x -> ?]] => (!B >> [[]])"@@ -244,36 +244,36 @@         , substs []         )       ,-        ( "[[!B, !a -> ?]] => [[x -> ?, y -> ?]] => (!a >> y, !B >> [[ x -> ? ]] )"-        , [BiMeta "B", BiVoid (AtMeta "a")]+        ( "[[!B, !t -> ?]] => [[x -> ?, y -> ?]] => (!t >> y, !B >> [[ x -> ? ]] )"+        , [BiMeta "B", BiVoid (AtMeta "t")]         , [BiVoid (AtLabel "x"), BiVoid (AtLabel "y")]-        , substs [[("a", MvAttribute (AtLabel "y")), ("B", MvBindings [BiVoid (AtLabel "x")])]]+        , substs [[("t", MvAttribute (AtLabel "y")), ("B", MvBindings [BiVoid (AtLabel "x")])]]         )       ,-        ( "[[!B1, !a -> ?, !B2]] => [[ x -> ?, y -> ?, z -> ? ]] => [(!B1 >> [[]], !a >> x, !B2 >> [[ y -> ?, z -> ? ]]), (...), (...)]"-        , [BiMeta "B1", BiVoid (AtMeta "a"), BiMeta "B2"]+        ( "[[!B1, !t -> ?, !B2]] => [[ x -> ?, y -> ?, z -> ? ]] => [(!B1 >> [[]], !t >> x, !B2 >> [[ y -> ?, z -> ? ]]), (...), (...)]"+        , [BiMeta "B1", BiVoid (AtMeta "t"), BiMeta "B2"]         , [BiVoid (AtLabel "x"), BiVoid (AtLabel "y"), BiVoid (AtLabel "z")]         , substs             [               [ ("B1", MvBindings [])-              , ("a", MvAttribute (AtLabel "x"))+              , ("t", MvAttribute (AtLabel "x"))               , ("B2", MvBindings [BiVoid (AtLabel "y"), BiVoid (AtLabel "z")])               ]             ,               [ ("B1", MvBindings [BiVoid (AtLabel "x")])-              , ("a", MvAttribute (AtLabel "y"))+              , ("t", MvAttribute (AtLabel "y"))               , ("B2", MvBindings [BiVoid (AtLabel "z")])               ]             ,               [ ("B1", MvBindings [BiVoid (AtLabel "x"), BiVoid (AtLabel "y")])-              , ("a", MvAttribute (AtLabel "z"))+              , ("t", MvAttribute (AtLabel "z"))               , ("B2", MvBindings [])               ]             ]         )       ,-        ( "[[!B1, !a1 -> ?, !B2, !a2 -> ?, !B3]] => [[ a -> ?, b -> ?, x -> ?, y -> ?, z -> ? ]] => [10 substs]"-        , [BiMeta "B1", BiVoid (AtMeta "a1"), BiMeta "B2", BiVoid (AtMeta "a2"), BiMeta "B3"]+        ( "[[!B1, !t1 -> ?, !B2, !t2 -> ?, !B3]] => [[ a -> ?, b -> ?, x -> ?, y -> ?, z -> ? ]] => [10 substs]"+        , [BiMeta "B1", BiVoid (AtMeta "t1"), BiMeta "B2", BiVoid (AtMeta "t2"), BiMeta "B3"]         ,           [ BiVoid (AtLabel "a")           , BiVoid (AtLabel "b")@@ -284,72 +284,72 @@         , substs             [               [ ("B1", MvBindings [])-              , ("a1", MvAttribute (AtLabel "a"))+              , ("t1", MvAttribute (AtLabel "a"))               , ("B2", MvBindings [])-              , ("a2", MvAttribute (AtLabel "b"))+              , ("t2", MvAttribute (AtLabel "b"))               , ("B3", MvBindings [BiVoid (AtLabel "x"), BiVoid (AtLabel "y"), BiVoid (AtLabel "z")])               ]             ,               [ ("B1", MvBindings [])-              , ("a1", MvAttribute (AtLabel "a"))+              , ("t1", MvAttribute (AtLabel "a"))               , ("B2", MvBindings [BiVoid (AtLabel "b")])-              , ("a2", MvAttribute (AtLabel "x"))+              , ("t2", MvAttribute (AtLabel "x"))               , ("B3", MvBindings [BiVoid (AtLabel "y"), BiVoid (AtLabel "z")])               ]             ,               [ ("B1", MvBindings [])-              , ("a1", MvAttribute (AtLabel "a"))+              , ("t1", MvAttribute (AtLabel "a"))               , ("B2", MvBindings [BiVoid (AtLabel "b"), BiVoid (AtLabel "x")])-              , ("a2", MvAttribute (AtLabel "y"))+              , ("t2", MvAttribute (AtLabel "y"))               , ("B3", MvBindings [BiVoid (AtLabel "z")])               ]             ,               [ ("B1", MvBindings [])-              , ("a1", MvAttribute (AtLabel "a"))+              , ("t1", MvAttribute (AtLabel "a"))               , ("B2", MvBindings [BiVoid (AtLabel "b"), BiVoid (AtLabel "x"), BiVoid (AtLabel "y")])-              , ("a2", MvAttribute (AtLabel "z"))+              , ("t2", MvAttribute (AtLabel "z"))               , ("B3", MvBindings [])               ]             ,               [ ("B1", MvBindings [BiVoid (AtLabel "a")])-              , ("a1", MvAttribute (AtLabel "b"))+              , ("t1", MvAttribute (AtLabel "b"))               , ("B2", MvBindings [])-              , ("a2", MvAttribute (AtLabel "x"))+              , ("t2", MvAttribute (AtLabel "x"))               , ("B3", MvBindings [BiVoid (AtLabel "y"), BiVoid (AtLabel "z")])               ]             ,               [ ("B1", MvBindings [BiVoid (AtLabel "a")])-              , ("a1", MvAttribute (AtLabel "b"))+              , ("t1", MvAttribute (AtLabel "b"))               , ("B2", MvBindings [BiVoid (AtLabel "x")])-              , ("a2", MvAttribute (AtLabel "y"))+              , ("t2", MvAttribute (AtLabel "y"))               , ("B3", MvBindings [BiVoid (AtLabel "z")])               ]             ,               [ ("B1", MvBindings [BiVoid (AtLabel "a")])-              , ("a1", MvAttribute (AtLabel "b"))+              , ("t1", MvAttribute (AtLabel "b"))               , ("B2", MvBindings [BiVoid (AtLabel "x"), BiVoid (AtLabel "y")])-              , ("a2", MvAttribute (AtLabel "z"))+              , ("t2", MvAttribute (AtLabel "z"))               , ("B3", MvBindings [])               ]             ,               [ ("B1", MvBindings [BiVoid (AtLabel "a"), BiVoid (AtLabel "b")])-              , ("a1", MvAttribute (AtLabel "x"))+              , ("t1", MvAttribute (AtLabel "x"))               , ("B2", MvBindings [])-              , ("a2", MvAttribute (AtLabel "y"))+              , ("t2", MvAttribute (AtLabel "y"))               , ("B3", MvBindings [BiVoid (AtLabel "z")])               ]             ,               [ ("B1", MvBindings [BiVoid (AtLabel "a"), BiVoid (AtLabel "b")])-              , ("a1", MvAttribute (AtLabel "x"))+              , ("t1", MvAttribute (AtLabel "x"))               , ("B2", MvBindings [BiVoid (AtLabel "y")])-              , ("a2", MvAttribute (AtLabel "z"))+              , ("t2", MvAttribute (AtLabel "z"))               , ("B3", MvBindings [])               ]             ,               [ ("B1", MvBindings [BiVoid (AtLabel "a"), BiVoid (AtLabel "b"), BiVoid (AtLabel "x")])-              , ("a1", MvAttribute (AtLabel "y"))+              , ("t1", MvAttribute (AtLabel "y"))               , ("B2", MvBindings [])-              , ("a2", MvAttribute (AtLabel "z"))+              , ("t2", MvAttribute (AtLabel "z"))               , ("B3", MvBindings [])               ]             ]@@ -380,14 +380,14 @@         , substs [[("e1", MvExpression (ExDispatch ExRoot (AtLabel "org")))]]         )       ,-        ( "!e.org.!a => $.org.x => [(!e >> $, !a >> x)]"-        , ExDispatch (ExDispatch (ExMeta "e") (AtLabel "org")) (AtMeta "a")+        ( "!e.org.!t => $.org.x => [(!e >> $, !t >> x)]"+        , ExDispatch (ExDispatch (ExMeta "e") (AtLabel "org")) (AtMeta "t")         , ExDispatch (ExDispatch ExXi (AtLabel "org")) (AtLabel "x")-        , substs [[("e", MvExpression ExXi), ("a", MvAttribute (AtLabel "x"))]]+        , substs [[("e", MvExpression ExXi), ("t", MvAttribute (AtLabel "x"))]]         )       ,-        ( "[[!a -> !e, !B]].!a => [[x -> Q, y -> $]].x => [(!a >> x, !e >> Q, !B >> [y -> $])]"-        , ExDispatch (ExFormation [BiTau (AtMeta "a") (ExMeta "e"), BiMeta "B"]) (AtMeta "a")+        ( "[[!t -> !e, !B]].!t => [[x -> Q, y -> $]].x => [(!t >> x, !e >> Q, !B >> [y -> $])]"+        , ExDispatch (ExFormation [BiTau (AtMeta "t") (ExMeta "e"), BiMeta "B"]) (AtMeta "t")         , ExDispatch             ( ExFormation                 [ BiTau (AtLabel "x") ExRoot@@ -397,15 +397,15 @@             (AtLabel "x")         , substs             [-              [ ("a", MvAttribute (AtLabel "x"))+              [ ("t", MvAttribute (AtLabel "x"))               , ("e", MvExpression ExRoot)               , ("B", MvBindings [BiTau (AtLabel "y") ExXi])               ]             ]         )       ,-        ( "[[!B1, !a ↦ !e1, !B2]](!a ↦ !e2) => ⟦ t ↦ ξ.k, x ↦ ξ.t, k ↦ ∅ ⟧(x ↦ ξ) => [(!B1 >> [[ t -> $.k ]], !a >> x, !B2 >> [[ k -> ? ]], !e1 >> $.t, !e2 >> $)]"-        , ExApplication (ExFormation [BiMeta "B1", BiTau (AtMeta "a") (ExMeta "e1"), BiMeta "B2"]) (ArTau (AtMeta "a") (ExMeta "e2"))+        ( "[[!B1, !t ↦ !e1, !B2]](!t ↦ !e2) => ⟦ t ↦ ξ.k, x ↦ ξ.t, k ↦ ∅ ⟧(x ↦ ξ) => [(!B1 >> [[ t -> $.k ]], !t >> x, !B2 >> [[ k -> ? ]], !e1 >> $.t, !e2 >> $)]"+        , ExApplication (ExFormation [BiMeta "B1", BiTau (AtMeta "t") (ExMeta "e1"), BiMeta "B2"]) (ArTau (AtMeta "t") (ExMeta "e2"))         , ExApplication             ( ExFormation                 [ BiTau (AtLabel "t") (ExDispatch ExXi (AtLabel "k"))@@ -417,7 +417,7 @@         , substs             [               [ ("B1", MvBindings [BiTau (AtLabel "t") (ExDispatch ExXi (AtLabel "k"))])-              , ("a", MvAttribute (AtLabel "x"))+              , ("t", MvAttribute (AtLabel "x"))               , ("B2", MvBindings [BiVoid (AtLabel "k")])               , ("e1", MvExpression (ExDispatch ExXi (AtLabel "t")))               , ("e2", MvExpression ExXi)

@@ -48,14 +48,14 @@         , [BiVoid AtRho, BiMeta "B", BiVoid (AtLabel "y")]         )       ,-        ( "[[!a -> ?, x -> $.y]] => [[!a -> Q.x, x -> $.y]]"-        , [BiVoid (AtMeta "a"), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]-        , [BiVoid (AtMeta "a"), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]+        ( "[[!t -> ?, x -> $.y]] => [[!t -> Q.x, x -> $.y]]"+        , [BiVoid (AtMeta "t"), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]+        , [BiVoid (AtMeta "t"), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]         )       ,-        ( "[[!a -> Q.x, x -> $.y]] => [[!a -> Q.x, x -> $.y]]"-        , [BiTau (AtMeta "a") (ExDispatch ExRoot (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]-        , [BiTau (AtMeta "a") (ExDispatch ExRoot (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]+        ( "[[!t -> Q.x, x -> $.y]] => [[!t -> Q.x, x -> $.y]]"+        , [BiTau (AtMeta "t") (ExDispatch ExRoot (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]+        , [BiTau (AtMeta "t") (ExDispatch ExRoot (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]         )       ] 

@@ -40,10 +40,10 @@   describe "parse expression" $     test       parseExpression-      [ ("Q.!a", Just (ExDispatch ExRoot (AtMeta "a")))-      , ("[[]](!a1 -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtMeta "a1") ExXi)))+      [ ("Q.!t", Just (ExDispatch ExRoot (AtMeta "t")))+      , ("[[]](!t1 -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtMeta "t1") ExXi)))       ,-        ( "[[]](~0 -> $)(~11 -> Q)"+        ( "[[]](a0 -> $)(a11 -> Q)"         , Just             ( ExApplication                 ( ExApplication@@ -55,12 +55,12 @@         )       , ("[[]](x -> $, y -> Q)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtLabel "x") ExXi)) (ArTau (AtLabel "y") ExRoot)))       , ("[[!B, !B1]]", Just (ExFormation [BiMeta "B", BiMeta "B1"]))-      , ("[[!B2, !a2 -> $]]", Just (ExFormation [BiMeta "B2", BiTau (AtMeta "a2") ExXi]))+      , ("[[!B2, !t2 -> $]]", Just (ExFormation [BiMeta "B2", BiTau (AtMeta "t2") ExXi]))       , ("!e0", Just (ExMeta "e0"))       , ("!k", Just (ExMeta "k"))       , ("[[x -> !k1]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "k1"), BiVoid AtRho]))       , ("[[x -> !e]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "e"), BiVoid AtRho]))-      , ("[[!a -> !e1]]", Just (ExFormation [BiTau (AtMeta "a") (ExMeta "e1")]))+      , ("[[!t -> !e1]]", Just (ExFormation [BiTau (AtMeta "t") (ExMeta "e1")]))       , ("[[D> --]]", Just (ExFormation [BiDelta BtEmpty, BiVoid AtRho]))       , ("[[D> 1F-]]", Just (ExFormation [BiDelta (BtOne "1F"), BiVoid AtRho]))       , ("[[\n  L> Func,\n  D> 00-\n]]", Just (ExFormation [BiLambda (Function "Func"), BiDelta (BtOne "00"), BiVoid AtRho]))@@ -103,7 +103,7 @@             )         )       ,-        ( "[[x -> y.z, w -> ^, u -> @, p -> !a, q -> !e]]"+        ( "[[x -> y.z, w -> ^, u -> @, p -> !t, q -> !e]]"         , Just             ( ExFormation                 [ BiTau@@ -117,7 +117,7 @@                     (ExDispatch ExXi AtPhi)                 , BiTau                     (AtLabel "p")-                    (ExDispatch ExXi (AtMeta "a"))+                    (ExDispatch ExXi (AtMeta "t"))                 , BiTau                     (AtLabel "q")                     (ExMeta "e")@@ -179,7 +179,7 @@         , Just             ( ExFormation                 [ BiMeta "B1"-                , BiTau (AtMeta "a0") ExXi+                , BiTau (AtMeta "t0") ExXi                 , BiTau (AtLabel "x") (ExMeta "e")                 ]             )@@ -192,10 +192,10 @@       , "[[x() -> [[]] ]]"       , "Q.x(y() -> [[]])"       , "Q.x(y(q) -> [[w -> !e]])"-      , "Q.x(~1(^,@) -> [[]])"-      , "Q.x.^.@.!a0"+      , "Q.x(a1(^,@) -> [[]])"+      , "Q.x.^.@.!t0"       , "[[x -> y.z]]"-      , "[[x -> ^, y -> @, z -> !a]]"+      , "[[x -> ^, y -> @, z -> !t]]"       , "Q.x(a.b.c, Q.a(b), [[]])"       , "Q.x(y, [[]].z, Q.y(^,@))"       , "[[x -> 5.plus(5), y -> \"hello\", z -> 42.5]]"@@ -206,7 +206,7 @@       , "[[ x -> \"\\u0001\\u0001\"]]"       , "[[ x -> \"\\uD835\\uDF11\"]]"       , "[[ x ↦ \"This plugin has \\x01\\x01\" ]]"-      , "[[ !afoo -> !e1Some, !a-BAR -> !e_123someW, !Bhi123 ]]"+      , "[[ !tfoo -> !e1Some, !t-BAR -> !e_123someW, !Bhi123 ]]"       , "[[ !B ]](α𝑖 -> !e)"       , "[[ 𝜏 -> !e, 𝐵 ]]"       ]@@ -225,17 +225,17 @@           , "Q.x(x -> ?)"           , "Q.x(L> Func)"           , "Q.x(D> --)"-          , "Q.x(~1 -> ?)"+          , "Q.x(a1 -> ?)"           , "Q.x(L> !F)"           , "Q.x(D> !b)"-          , "[[~0 -> Q.x]]"-          , "[[x(~1) -> [[]] ]]"+          , "[[α0 -> Q.x]]"+          , "[[x(α1) -> [[]] ]]"           , "[[y(!e) -> [[]] ]]"           , "[[z(w) -> Q.x]]"-          , "Q.x(y(~1) -> [[]])"+          , "Q.x(y(α1) -> [[]])"           , "Q.x(1, 2, !B)"-          , "Q.x.~0"-          , "Q.x(~1 -> Q.y, x -> 5, !B1)"+          , "Q.x.α0"+          , "Q.x(a1 -> Q.y, x -> 5, !B1)"           , "Q.x(𝐵1, 𝜏0 -> $, x -> 𝑒)"           , "[[ x -> \"\\uD800\"]]"           , "[[ x -> \"\\uDFFF\"]]"@@ -295,8 +295,8 @@       , ("@ -> $", Just (BiTau AtPhi ExXi))       , ("ρ -> Q", Just (BiTau AtRho ExRoot))       , ("φ -> T", Just (BiTau AtPhi ExTermination))-      , ("!a -> $", Just (BiTau (AtMeta "a") ExXi))-      , ("!a0 -> Q", Just (BiTau (AtMeta "a0") ExRoot))+      , ("!t -> $", Just (BiTau (AtMeta "t") ExXi))+      , ("!t0 -> Q", Just (BiTau (AtMeta "t0") ExRoot))       , ("D> --", Just (BiDelta BtEmpty))       , ("D> 42-", Just (BiDelta (BtOne "42")))       , ("D> 01-02-03", Just (BiDelta (BtMany ["01", "02", "03"])))@@ -309,6 +309,8 @@       , ("λ ⤍ Test", Just (BiLambda (Function "Test")))       , ("L> !F", Just (BiLambda (FnMeta "F")))       , ("L> !F0", Just (BiLambda (FnMeta "F0")))+      , ("λ ⤍ 𝐹", Just (BiLambda (FnMeta "F")))+      , ("L> 𝐹2", Just (BiLambda (FnMeta "F2")))       , ("!B", Just (BiMeta "B"))       , ("!B0", Just (BiMeta "B0"))       , ("!B_test", Just (BiMeta "B_test"))@@ -337,14 +339,14 @@       , ("ρ", Just AtRho)       , ("@", Just AtPhi)       , ("φ", Just AtPhi)-      , ("!a", Just (AtMeta "a"))-      , ("!a0", Just (AtMeta "a0"))-      , ("!a_test", Just (AtMeta "a_test"))-      , ("𝜏", Just (AtMeta "a"))-      , ("𝜏0", Just (AtMeta "a0"))-      , ("~0", Nothing)-      , ("~1", Nothing)-      , ("~123", Nothing)+      , ("!t", Just (AtMeta "t"))+      , ("!t0", Just (AtMeta "t0"))+      , ("!t_test", Just (AtMeta "t_test"))+      , ("𝜏", Just (AtMeta "t"))+      , ("𝜏0", Just (AtMeta "t0"))+      , ("a0", Just (AtLabel "a0"))+      , ("a1", Just (AtLabel "a1"))+      , ("a123", Just (AtLabel "a123"))       , ("α0", Nothing)       , ("α42", Nothing)       , ("X", Nothing)@@ -462,6 +464,8 @@       , ("[[]](Q, T)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) ExRoot)) (ArAlpha (Alpha 1) ExTermination)))       , ("Q.x(y -> $)", Just (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") ExXi)))       , ("[[x -> ?]].x(Q)", Just (ExApplication (ExDispatch (ExFormation [BiVoid (AtLabel "x"), BiVoid AtRho]) (AtLabel "x")) (ArAlpha (Alpha 0) ExRoot)))+      , ("[[]](a!i -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i") ExXi)))+      , ("[[]](α𝑖 -> Q)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i") ExRoot)))       ]    describe "parse meta expressions" $

@@ -56,11 +56,15 @@       , ("meta expr", ExMeta "e", "!e")       , ("meta binding", ExFormation [BiMeta "B"], "[[ !B ]]")       , ("meta lambda", ExFormation [BiLambda (FnMeta "F")], "[[ L> !F ]]")-      , ("meta attr tau", ExFormation [BiTau (AtMeta "a") ExXi], "[[ !a -> $ ]]")+      , ("meta attr tau", ExFormation [BiTau (AtMeta "t") ExXi], "[[ !t -> $ ]]")       ]       ( \(desc, expr, expected) ->           it desc (printExpression' expr (SWEET, ASCII, SINGLELINE, defaultMargin) `shouldBe` expected)       )++  describe "printExpression with SWEET UNICODE renders the pretty function meta" $+    it "meta lambda becomes 𝐹" $+      printExpression' (ExFormation [BiLambda (FnMeta "F")]) (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "⟦ λ ⤍ 𝐹 ⟧"    describe "printExpression keeps special double values in byte form so they re-parse" $     forM_

@@ -12,6 +12,7 @@ import Data.Char (isDigit, isHexDigit) import Data.Set qualified as Set import Random (randomString)+import System.Timeout (timeout) import Test.Hspec (Spec, describe, it, shouldBe, shouldSatisfy)  spec :: Spec@@ -25,6 +26,12 @@     it "returns literal unchanged" $ do       result <- randomString "hello"       result `shouldBe` "hello"++  describe "randomString called twice with the same literal pattern" $+    it "does not loop forever on the second call" $ do+      _ <- randomString "repeated"+      result <- timeout 1000000 (randomString "repeated")+      result `shouldBe` Just "repeated"    describe "randomString with literal pattern containing spaces" $     it "returns literal with spaces" $ do

@@ -183,21 +183,21 @@     test       (replaceProgramFast (ReplaceCtx 3))       [-        ( "Q -> [[^ -> ?, @ -> ?, D> -> ?]] => [[ !B1, !a -> ?, !B2 ]] => [[ !B1, !a -> $, !B2 ]] => Q -> [[ ^ -> $, @ -> $, D> -> $ ]]"+        ( "Q -> [[^ -> ?, @ -> ?, D> -> ?]] => [[ !B1, !t -> ?, !B2 ]] => [[ !B1, !t -> $, !B2 ]] => Q -> [[ ^ -> $, @ -> $, D> -> $ ]]"         , Program (ExFormation [BiVoid AtRho, BiVoid AtPhi, BiVoid AtDelta])         , [ExFormation [BiVoid AtRho], ExFormation [BiVoid AtPhi], ExFormation [BiVoid AtDelta]]         , [ExFormation [BiTau AtRho ExXi], ExFormation [BiTau AtPhi ExXi], ExFormation [BiTau AtDelta ExXi]]         , Program (ExFormation [BiTau AtRho ExXi, BiTau AtPhi ExXi, BiTau AtDelta ExXi])         )       ,-        ( "Q -> [[ ^ -> ? ]] => [[ !B1, !a -> ?, !B2 ]] => [[ !B1, !a -> [[ !a -> ? ]], !B2 ]] => Q -> [[ ^ -> [[ ^ -> [[ ^ -> [[ ^ -> ? ]] ]] ]] ]]"+        ( "Q -> [[ ^ -> ? ]] => [[ !B1, !t -> ?, !B2 ]] => [[ !B1, !t -> [[ !t -> ? ]], !B2 ]] => Q -> [[ ^ -> [[ ^ -> [[ ^ -> [[ ^ -> ? ]] ]] ]] ]]"         , Program (ExFormation [BiVoid AtRho])         , [ExFormation [BiVoid AtRho]]         , [ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])]]         , Program (ExFormation [BiTau AtRho (ExFormation [BiTau AtRho (ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])])])])         )       ,-        ( "Q -> [[ ^ -> T ]](^ -> [[ ^ -> $]]).@ => [[ !B1, !a -> ?, !B2 ]] => [[ !B1, !a -> $, !B2 ]] => Q -> [[ ^ -> $ ]].@"+        ( "Q -> [[ ^ -> T ]](^ -> [[ ^ -> $]]).@ => [[ !B1, !t -> ?, !B2 ]] => [[ !B1, !t -> $, !B2 ]] => Q -> [[ ^ -> $ ]].@"         , Program (ExDispatch (ExApplication (ExFormation [BiTau AtRho ExTermination]) (ArTau AtRho (ExFormation [BiTau AtRho ExXi]))) AtPhi)         , [ExFormation [BiTau AtRho ExTermination], ExFormation [BiTau AtRho ExXi]]         , [ExFormation [BiTau AtRho ExRoot], ExFormation [BiVoid AtPhi]]