phino 0.0.84 → 0.0.85

raw patch · 19 files changed

+180/−99 lines, 19 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +7/−7
• phino.cabal +1/−1
• resources/dataization.yaml +1/−0
• resources/morphing.yaml +1/−0
• resources/normalize/amiss.yaml +11/−0
• resources/normalize/phi.yaml +1/−0
• src/CLI/Runners.hs +1/−1
• src/CST.hs +7/−3
• src/Condition.hs +7/−0
• src/Dataize.hs +2/−2
• src/LaTeX.hs +17/−9
• src/Parser.hs +3/−3
• src/Render.hs +5/−2
• src/Rule.hs +28/−17
• src/Sugar.hs +1/−1
• src/Yaml.hs +12/−1
• test/CLISpec.hs +64/−47
• test/ConditionSpec.hs +2/−0
• test/ParserSpec.hs +9/−5

@@ -214,7 +214,7 @@ $ phino explain --normalize \begin{tabular}{rl} \phinoNormalizationRule{alpha}-  { [[ B_1, \tau -> ?, B_2 ]] ( \alpha_{i} -> e ) }+  { [[ B_1, \tau -> ?, B_2 ]] ( \phiTerminal{\alpha_{i}} -> e ) }   { [[ B_1, \tau -> ?, B_2 ]] ( \tau -> e ) }   { $ i = \vert \overline{ B_1 } \vert $ }   { }@@ -255,14 +255,14 @@ $ phino explain --dataize \begin{tabular}{rl} \phinoDataizationRule{delta}-  { \mathbb{D}( [[ B_1, D> δ, B_2 ]] ) }+  { \phinoDataize{ [[ B_1, D> δ, B_2 ]] } }   { δ }   { }   { } ... \phinoDataizationRule{norm}-  { \mathbb{D}( n ) }-  { \mathbb{D}( \mathbb{M}( n ) ) }+  { \phinoDataize{ n } }+  { \phinoDataize{ \mathbb{M}( n ) } }   { }   { } \end{tabular}@@ -378,7 +378,7 @@  * `!t` || `𝜏` - attribute * `!i` || `𝑖` - the index of a positional (α) application argument,-                captured by writing `α𝑖` (or `a𝑖`)+                captured by writing `α𝑖` (or `~!i`) * `!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@@ -393,8 +393,8 @@  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.+A positional (α) application argument is written as `α0`, `~0` (ASCII), or+`α𝑖`/`~!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.84+version: 0.0.85 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>

@@ -5,6 +5,7 @@ # is always a normal form: a non-NF expression matches no clause.  - name: delta+  label: \Delta   description: '𝔻(⟦𝐵1, Δ ⤍ δ, 𝐵2⟧) ⟿ δ'   match: ⟦𝐵1, Δ ⤍ δ, 𝐵2⟧   then: δ

@@ -14,6 +14,7 @@   then: ⟦𝐵⟧  - name: lambda+  label: \lambda   description: '𝕄(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧.τ) ⟿ 𝕄(𝒩(𝔼(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧).τ))'   match: '⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧.𝜏'   where:

@@ -0,0 +1,11 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: amiss+pattern: ⟦𝐵⟧(α𝑖 ↦ 𝑒)+result: ⊥+when:+  not:+    gt:+      - domain: 𝐵+      - 𝑖

@@ -2,6 +2,7 @@ # SPDX-License-Identifier: MIT --- name: phi+label: \phi pattern: ⟦𝐵⟧.𝜏 result: ⟦𝐵⟧.φ.𝜏 when:

@@ -246,4 +246,4 @@         else putStrLn (P.printSubsts' substs (_sugarType, UNICODE, _flat, defaultMargin))   where     rule :: Expression -> Maybe Y.Condition -> Y.Rule-    rule ptn cnd = Y.Rule "custom" Nothing ptn ExRoot cnd Nothing Nothing+    rule ptn cnd = Y.Rule "custom" Nothing Nothing ptn ExRoot cnd Nothing Nothing

@@ -48,7 +48,7 @@ data DELTA = DELTA | DELTA'   deriving (Eq, Show) -data XI = XI | DOLLAR+data XI = XI | DOLLAR | XI'   deriving (Eq, Show)  data LAMBDA = LAMBDA | LAMBDA'@@ -206,6 +206,8 @@ data EQUAL   = EQUAL   | NOT_EQUAL+  | GREATER+  | NOT_GREATER   deriving (Eq, Show)  data NUMBER@@ -343,7 +345,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(a0 -> Q.bytes(...), ^ -> ..., ^ -> ...)`+  -- `Q.number(~0 -> 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.@@ -409,7 +411,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 (a0 -> e1, a1 -> e2, ...)+      --    alpha attributes (~0 -> e1, ~1 -> e2, ...)       complexApplication :: Expression -> (Expression, [Argument], [Expression])       complexApplication expr =         let (expr', taus', exprs') = complexApplication' expr@@ -521,6 +523,7 @@ instance ToCST Y.Condition CONDITION where   toCST (Y.Not (Y.In attr binding)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_BINDING (bindingsToCST [binding]))   toCST (Y.Not (Y.Eq left right)) _ = CO_COMPARE (comparableToCST left) NOT_EQUAL (comparableToCST right)+  toCST (Y.Not (Y.Gt left right)) _ = CO_COMPARE (comparableToCST left) NOT_GREATER (comparableToCST right)   toCST (Y.Not (Y.Absolute expr)) _ = CO_ABSOLUTE (expressionToCST expr) NOT_IN   toCST (Y.Absolute expr) _ = CO_ABSOLUTE (expressionToCST expr) IN   toCST (Y.Disjoint attrs groups) _ = CO_DISJOINT (map attributeToCST attrs) (map (\bd -> bindingsToCST [bd]) groups)@@ -534,6 +537,7 @@   toCST (Y.NF expr) _ = CO_NF (expressionToCST expr)   toCST (Y.Not cond) _ = CO_NOT (conditionToCST cond)   toCST (Y.Eq left right) _ = CO_COMPARE (comparableToCST left) EQUAL (comparableToCST right)+  toCST (Y.Gt left right) _ = CO_COMPARE (comparableToCST left) GREATER (comparableToCST right)   toCST (Y.Matches regex expr) _ = CO_MATCHES regex (expressionToCST expr)   toCST (Y.PartOf expr binding) _ = CO_PART_OF (expressionToCST expr) (bindingsToCST [binding]) 

@@ -112,6 +112,13 @@         _ <- rparen         return (Y.Eq left right)     , do+        _ <- symbol "gt" >> lparen+        left <- comparable+        _ <- comma+        right <- comparable+        _ <- rparen+        return (Y.Gt left right)+    , do         _ <- symbol "nf" >> lparen         expr <- _expression phiParser         _ <- rparen

@@ -89,7 +89,7 @@     -- maps onto the 'having' slot (which runs after 'where'), not 'when' (which     -- 'matchExpressionWithRule'' runs before 'where').     asRule :: Y.MorphRule -> Y.Rule-    asRule rule = Y.Rule rule.name rule.description rule.match ExRoot Nothing rule.where_ rule.when+    asRule rule = Y.Rule rule.name Nothing rule.description rule.match ExRoot Nothing rule.where_ rule.when     apply :: Y.MorphOutcome -> String -> Subst -> IO Morphed     apply (Y.MoStop result) name subst = do       built <- buildExpressionThrows result subst@@ -137,7 +137,7 @@         (subst : _) -> pure (Just (rule, subst))         [] -> firstMatch rest     asRule :: Y.DataizeRule -> Y.Rule-    asRule rule = Y.Rule rule.name rule.description rule.match ExRoot Nothing rule.where_ rule.when+    asRule rule = Y.Rule rule.name Nothing rule.description rule.match ExRoot Nothing rule.where_ rule.when     apply :: Y.DataizeRule -> Subst -> IO Dataized     apply rule subst = case rule.then_ of       Y.DoData bytes -> do

@@ -234,6 +234,7 @@   toLaTeX EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toLaTeX expr)   toLaTeX EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toLaTeX expr)   toLaTeX EX_META{..} = EX_META (toLaTeX meta)+  toLaTeX EX_XI{} = EX_XI XI'   toLaTeX expr = expr  instance ToLaTeX ATTRIBUTE where@@ -269,7 +270,7 @@     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)+     in PA_TAU (AT_LABEL ("\\phiTerminal{\\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)@@ -353,6 +354,7 @@ explainRule rule =   trrule     "\\phinoNormalizationRule"+    rule.label     rule.name     (renderToLatex (expressionToCST rule.pattern) defaultLatexContext)     (renderToLatex (expressionToCST rule.result) defaultLatexContext)@@ -370,6 +372,7 @@ explainMorphRule rule =   trrule     "\\phinoMorphingRule"+    rule.label     rule.name     (morph (renderToLatex (expressionToCST rule.match) defaultLatexContext))     (morphOutcome rule.then_)@@ -385,6 +388,7 @@ explainDataizeRule rule =   trrule     "\\phinoDataizationRule"+    rule.label     rule.name     (dataize (renderToLatex (expressionToCST rule.match) defaultLatexContext))     (dataizeOutcome rule.then_)@@ -399,25 +403,29 @@     dataizeOutcome Y.DoNothing = "\\varnothing"  -- 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 =+-- \phinoMorphingRule, \phinoNormalizationRule, \phinoDataizationRule): an+-- optional typeset label, name, left-hand side, right-hand side, the optional+-- 'if' condition and 'where' extras. When the label is present it becomes the+-- macro's first optional argument ('\macro[label]{name}'); when absent the+-- optional argument is omitted entirely ('\macro{name}').+trrule :: String -> Maybe String -> String -> String -> String -> Maybe Y.Condition -> Maybe [Y.Extra] -> String+trrule macro label name lhs rhs cond extras =   intercalate     "\n  "-    [ macro ++ "{" ++ name ++ "}"+    [ macro ++ labelArg ++ "{" ++ name ++ "}"     , braced lhs     , braced rhs     , conditionToLatex cond     , extraArgumentsToLatex extras     ]+  where+    labelArg = maybe "" (\symbol -> "[" ++ symbol ++ "]") label  morph :: String -> String-morph inner = "\\mathbb{M}( " ++ inner ++ " )"+morph inner = "\\phinoMorph{ " ++ inner ++ " }"  dataize :: String -> String-dataize inner = "\\mathbb{D}( " ++ inner ++ " )"+dataize inner = "\\phinoDataize{ " ++ inner ++ " }"  normalize :: String -> String normalize inner = "\\phinoNormalize{ " ++ inner ++ " }"

@@ -337,11 +337,11 @@ index' = meta' 'i' "𝑖"  -- alpha--- 1. index: a0, α0--- 2. meta: α𝑖, a!i+-- 1. index: ~0, α0+-- 2. meta: α𝑖, ~!i alpha :: Parser Alpha alpha = do-  _ <- choice [symbol "a", symbol "α"]+  _ <- choice [symbol "~", symbol "α"]   choice     [ Alpha <$> lexeme L.decimal     , AlMeta <$> index'

@@ -67,7 +67,7 @@ instance Render RHO where   render RHO = "ρ"   render CARET = "^"-  render RHO' = "\\rho"+  render RHO' = "\\phiTerminal{\\rho}"  instance Render DELTA where   render DELTA = "Δ"@@ -76,6 +76,7 @@ instance Render XI where   render XI = "ξ"   render DOLLAR = "$"+  render XI' = "\\phiTerminal{\\xi}"  instance Render LAMBDA where   render LAMBDA = "λ"@@ -135,7 +136,7 @@  instance Render ALPHA' where   render ALPHA = "α"-  render ALPHA' = "a"+  render ALPHA' = "~"  instance Render ALPHA where   render AL_IDX{..} = render sym <> render idx@@ -245,6 +246,8 @@ instance Render EQUAL where   render EQUAL = "="   render NOT_EQUAL = "\\not="+  render GREATER = ">"+  render NOT_GREATER = "\\not>"  instance Render CONDITION where   render CO_BELONGS{..} = render attr <> " " <> render belongs <> " " <> render set

@@ -110,27 +110,29 @@         attrInBinding _ _ = False     attrInBindings _ _ = False -_eq :: Y.Comparable -> Y.Comparable -> Subst -> RuleContext -> IO [Subst]-_eq (Y.CmpNum left) (Y.CmpNum right) subst _ = case (numToInt left subst, numToInt right subst) of-  (Just left_, Just right_) -> pure [subst | left_ == right_]-  (_, _) -> pure []+-- Convert a 'Number' to an 'Int' under the given substitution, resolving+-- index metas, binding lengths and formation domains.+numToInt :: Y.Number -> Subst -> Maybe Int+numToInt (Y.MetaIndex meta) (Subst mp) = case M.lookup meta mp of+  Just (MvIndex idx) -> Just idx+  _ -> Nothing+numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of+  Just (MvBindings bds) -> Just (length bds)+  _ -> Nothing+numToInt (Y.Domain (BiMeta meta)) (Subst mp) = case M.lookup meta mp of+  Just (MvBindings bds) -> Just (length (filter notAsset bds))+  _ -> Nothing   where-    -- Convert Number to Int-    numToInt :: Y.Number -> Subst -> Maybe Int-    numToInt (Y.MetaIndex meta) (Subst mp) = case M.lookup meta mp of-      Just (MvIndex idx) -> Just idx-      _ -> Nothing-    numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of-      Just (MvBindings bds) -> Just (length bds)-      _ -> Nothing-    numToInt (Y.Domain (BiMeta meta)) (Subst mp) = case M.lookup meta mp of-      Just (MvBindings bds) -> Just (length (filter notAsset bds))-      _ -> Nothing-    numToInt (Y.Literal num) _ = Just num-    numToInt _ _ = Nothing     notAsset (BiDelta _) = False     notAsset (BiLambda _) = False     notAsset _ = True+numToInt (Y.Literal num) _ = Just num+numToInt _ _ = Nothing++_eq :: Y.Comparable -> Y.Comparable -> Subst -> RuleContext -> IO [Subst]+_eq (Y.CmpNum left) (Y.CmpNum right) subst _ = case (numToInt left subst, numToInt right subst) of+  (Just left_, Just right_) -> pure [subst | left_ == right_]+  (_, _) -> pure [] _eq (Y.CmpAttr left) (Y.CmpAttr right) subst _ = pure [subst | compareAttrs left right subst]   where     compareAttrs :: Attribute -> Attribute -> Subst -> Bool@@ -159,6 +161,14 @@     compareExprs left right _ = left == right _eq _ _ _ _ = pure [] +-- Hold if the left number is strictly greater than the right one. Only+-- numeric comparables are ordered; anything else fails to hold.+_gt :: Y.Comparable -> Y.Comparable -> Subst -> RuleContext -> IO [Subst]+_gt (Y.CmpNum left) (Y.CmpNum right) subst _ = case (numToInt left subst, numToInt right subst) of+  (Just left_, Just right_) -> pure [subst | left_ > right_]+  (_, _) -> pure []+_gt _ _ _ _ = pure []+ _nf :: Expression -> Subst -> RuleContext -> IO [Subst] _nf (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of   Just (MvExpression expr) -> _nf expr (Subst mp) ctx@@ -231,6 +241,7 @@ meetCondition' (Y.Not cond) = _not cond meetCondition' (Y.In attr binding) = _in attr binding meetCondition' (Y.Eq left right) = _eq left right+meetCondition' (Y.Gt left right) = _gt left right meetCondition' (Y.NF expr) = _nf expr meetCondition' (Y.Absolute expr) = _absolute expr meetCondition' (Y.Matches pat expr) = _matches pat expr

@@ -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(a0 -> e0, a1 -> e1, ...)                          |+--  | e(e0, e1, ...)             | e(~0 -> e0, ~1 -> e1, ...)                          | --  | e(a1 -> e1, a2 -> e2, ...) | e(a1 -> e1)(a2 -> e2)...                            | --  |----------------------------|-----------------------------------------------------| class ToSalty a where

@@ -83,7 +83,7 @@     withObject       "Condition"       ( \v -> do-          validateYamlObject v ["and", "or", "not", "nf", "absolute", "eq", "in", "matches", "part-of", "disjoint"]+          validateYamlObject v ["and", "or", "not", "nf", "absolute", "eq", "gt", "in", "matches", "part-of", "disjoint"]           asum             [ And <$> v .: "and"             , Or <$> v .: "or"@@ -101,6 +101,11 @@                   [left_, right_] -> Eq <$> parseJSON left_ <*> parseJSON right_                   _ -> fail "'eq' expects exactly two arguments"             , do+                vals <- v .: "gt"+                case vals of+                  [left_, right_] -> Gt <$> parseJSON left_ <*> parseJSON right_+                  _ -> fail "'gt' expects exactly two arguments"+            , do                 vals <- v .: "in"                 case vals of                   [attr_, binding_] -> do@@ -169,6 +174,7 @@   | In Attribute Binding   | Not Condition   | Eq Comparable Comparable+  | Gt Comparable Comparable   | NF Expression   | Absolute Expression   | Matches String Expression@@ -192,6 +198,7 @@  data Rule = Rule   { name :: String+  , label :: Maybe String   , description :: Maybe String   , pattern :: Expression   , result :: Expression@@ -251,6 +258,7 @@ -- 'where', filter by 'when', then reduce per 'then'. data MorphRule = MorphRule   { name :: String+  , label :: Maybe String   , description :: Maybe String   , match :: Expression   , where_ :: Maybe [Extra]@@ -263,6 +271,7 @@ -- under 𝔻 and able to terminate with bytes or 'nothing'. data DataizeRule = DataizeRule   { name :: String+  , label :: Maybe String   , description :: Maybe String   , match :: Expression   , where_ :: Maybe [Extra]@@ -306,6 +315,7 @@       ( \o ->           MorphRule             <$> o .: "name"+            <*> o .:? "label"             <*> o .:? "description"             <*> o .: "match"             <*> o .:? "where"@@ -320,6 +330,7 @@       ( \o ->           DataizeRule             <$> o .: "name"+            <*> o .:? "label"             <*> o .:? "description"             <*> o .: "match"             <*> o .:? "where"

@@ -422,8 +422,8 @@               , "\\Big\\{ [["               , "  |x\\char95{}o| -> Q . |z| ( |y| -> 5 ),"               , "  |q\\char36{}| -> T,"-              , "  |w| -> $,"-              , "  \\rho -> Q,"+              , "  |w| -> \\phiTerminal{\\xi},"+              , "  \\phiTerminal{\\rho} -> Q,"               , "  @ -> 1,"               , "  |y| -> \"H$@^M\","               , "  L> |Fu\\char95{}nc|"@@ -444,12 +444,12 @@           ]      it "rewrites an alpha-index argument as \\alpha subscript in LaTeX" $-      withStdin "Q -> Q.foo(a1 -> Q.y)" $+      withStdin "Q -> Q.foo(~1 -> Q.y)" $         testCLISucceeded           ["rewrite", "--output=latex", "--flat", "--nonumber"]           [ unlines               [ "\\begin{phiquation*}"-              , "Q -> Q . |foo| ( \\alpha_{1} -> Q . |y| ){.}"+              , "Q -> Q . |foo| ( \\phiTerminal{\\alpha_{1}} -> Q . |y| ){.}"               , "\\end{phiquation*}"               ]           ]@@ -558,10 +558,10 @@               [ "\\begin{phiquation}"               , "\\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\\}{.}"+              , "  \\leadsto \\Big\\{ \\phinoAgain{foo:2} . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}"+              , "  \\leadsto \\Big\\{ \\phinoAgain{foo:1} ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2}, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto \\Big\\{ [[ D> 42-, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"+              , "  \\leadsto \\Big\\{ [[ D> 42-, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]] \\Big\\}{.}"               , "\\end{phiquation}"               ]           ]@@ -574,10 +574,10 @@               [ "\\begin{phiquation}"               , "\\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\\}{.}"+              , "  \\leadsto \\Big\\{ \\phinoAgain{2} . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}"+              , "  \\leadsto \\Big\\{ \\phinoAgain{1} ( \\phiTerminal{\\rho} -> \\phinoAgain{2}, \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto \\Big\\{ [[ D> 42-, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"+              , "  \\leadsto \\Big\\{ [[ D> 42-, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]] \\Big\\}{.}"               , "\\end{phiquation}"               ]           ]@@ -652,7 +652,7 @@           [ unlines               [ "\\begin{phiquation}"               , "\\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}"-              , "  \\leadsto \\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |y| ( \\rho -> [[ |x| -> |y|, |y| -> |x| ]] ) \\Big\\} \\leadsto"+              , "  \\leadsto \\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |y| ( \\phiTerminal{\\rho} -> [[ |x| -> |y|, |y| -> |x| ]] ) \\Big\\} \\leadsto"               , "  \\leadsto \\dots"               , "\\end{phiquation}"               ]@@ -881,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| -> [[]] ]] ( \\rho -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], \\rho -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\}{.}"+              , "  \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"+              , "  \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], \\phiTerminal{\\rho} -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\}{.}"               , "\\end{phiquation}"               , "01-"               ]@@ -952,6 +952,18 @@             ]         ] +    it "explains single rule with a label" $+      testCLISucceeded+        ["explain", "--rule=test-resources/cli/labeled.yaml"]+        [ unlines+            [ "\\phinoNormalizationRule[\\lambda]{copy}"+            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"+            , "  { [[ B_1, \\tau -> k, B_2 ]] }"+            , "  { }"+            , "  { }"+            ]+        ]+     it "explains multiple rules" $       testCLISucceeded         ["explain", "--rule=resources/normalize/copy.yaml", "--rule=resources/normalize/alpha.yaml"]@@ -962,10 +974,15 @@         ["explain", "--normalize"]         [ unlines             [ "\\phinoNormalizationRule{alpha}"-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\alpha_{i} -> e ) }"+            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }"             , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }"             , "  { i = \\vert \\overline{ B_1 } \\vert }"             , "  { }"+            , "\\phinoNormalizationRule{amiss}"+            , "  { [[ B ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }"+            , "  { T }"+            , "  { \\vert \\overline{ B } \\vert \\not> i }"+            , "  { }"             , "\\phinoNormalizationRule{copy}"             , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"             , "  { [[ B_1, \\tau -> k, B_2 ]] }"@@ -977,7 +994,7 @@             , "  { }"             , "  { }"             , "\\phinoNormalizationRule{dca}"-            , "  { T ( \\alpha_{i} -> e ) }"+            , "  { T ( \\phiTerminal{\\alpha_{i}} -> e ) }"             , "  { T }"             , "  { }"             , "  { }"@@ -988,7 +1005,7 @@             , "  { }"             , "\\phinoNormalizationRule{dot}"             , "  { [[ B_1, \\tau -> n, B_2 ]] . \\tau }"-            , "  { e ( \\rho -> [[ B_1, \\tau -> n, B_2 ]] ) }"+            , "  { e ( \\phiTerminal{\\rho} -> [[ B_1, \\tau -> n, B_2 ]] ) }"             , "  { }"             , "  { e \\coloneqq \\ctx{ n }{ [[ B_1, \\tau -> n, B_2 ]] } }"             , "\\phinoNormalizationRule{miss}"@@ -1004,16 +1021,16 @@             , "\\phinoNormalizationRule{over}"             , "  { [[ B_1, \\tau -> e_1, B_2 ]] ( \\tau -> e_2 ) }"             , "  { T }"-            , "  { \\tau \\not= \\rho }"+            , "  { \\tau \\not= \\phiTerminal{\\rho} }"             , "  { }"-            , "\\phinoNormalizationRule{phi}"+            , "\\phinoNormalizationRule[\\phi]{phi}"             , "  { [[ B ]] . \\tau }"             , "  { [[ B ]] . @ . \\tau }"             , "  { @ \\in B \\;\\text{and}\\; \\tau \\notin B }"             , "  { }"             , "\\phinoNormalizationRule{stay}"-            , "  { [[ B_1, \\rho -> e_1, B_2 ]] ( \\rho -> e_2 ) }"-            , "  { [[ B_1, \\rho -> e_1, B_2 ]] }"+            , "  { [[ B_1, \\phiTerminal{\\rho} -> e_1, B_2 ]] ( \\phiTerminal{\\rho} -> e_2 ) }"+            , "  { [[ B_1, \\phiTerminal{\\rho} -> e_1, B_2 ]] }"             , "  { }"             , "  { }"             , "\\phinoNormalizationRule{stop}"@@ -1029,47 +1046,47 @@         ["explain", "--morph"]         [ unlines             [ "\\phinoMorphingRule{prim}"-            , "  { \\mathbb{M}( [[ B ]] ) }"+            , "  { \\phinoMorph{ [[ B ]] } }"             , "  { [[ B ]] }"             , "  { }"             , "  { }"-            , "\\phinoMorphingRule{lambda}"-            , "  { \\mathbb{M}( [[ B_1, L> F, B_2 ]] . \\tau ) }"-            , "  { \\mathbb{M}( \\phinoNormalize{ e . \\tau } ) }"+            , "\\phinoMorphingRule[\\lambda]{lambda}"+            , "  { \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau } }"+            , "  { \\phinoMorph{ \\phinoNormalize{ e . \\tau } } }"             , "  { }"             , "  { e \\coloneqq \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] } }"             , "\\phinoMorphingRule{dispatch}"-            , "  { \\mathbb{M}( n . \\tau ) }"-            , "  { \\mathbb{M}( \\phinoNormalize{ e . \\tau } ) }"+            , "  { \\phinoMorph{ n . \\tau } }"+            , "  { \\phinoMorph{ \\phinoNormalize{ e . \\tau } } }"             , "  { }"             , "  { e \\coloneqq \\phinoMorph{ n } }"             , "\\phinoMorphingRule{application}"-            , "  { \\mathbb{M}( n ( \\tau -> e ) ) }"-            , "  { \\mathbb{M}( \\phinoNormalize{ e_1 ( \\tau -> e ) } ) }"+            , "  { \\phinoMorph{ n ( \\tau -> e ) } }"+            , "  { \\phinoMorph{ \\phinoNormalize{ e_1 ( \\tau -> e ) } } }"             , "  { }"             , "  { e_1 \\coloneqq \\phinoMorph{ n } }"             , "\\phinoMorphingRule{applicationa}"-            , "  { \\mathbb{M}( n ( \\alpha_{i} -> e ) ) }"-            , "  { \\mathbb{M}( \\phinoNormalize{ e_1 ( \\alpha_{i} -> e ) } ) }"+            , "  { \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> e ) } }"+            , "  { \\phinoMorph{ \\phinoNormalize{ e_1 ( \\phiTerminal{\\alpha_{i}} -> e ) } } }"             , "  { }"             , "  { e_1 \\coloneqq \\phinoMorph{ n } }"             , "\\phinoMorphingRule{root}"-            , "  { \\mathbb{M}( Q ) }"-            , "  { \\mathbb{M}( \\phinoNormalize{ e } ) }"+            , "  { \\phinoMorph{ Q } }"+            , "  { \\phinoMorph{ \\phinoNormalize{ e } } }"             , "  { e \\not= Q }"             , "  { e \\coloneqq \\phinoGlobal{  } }"             , "\\phinoMorphingRule{dead}"-            , "  { \\mathbb{M}( T ) }"+            , "  { \\phinoMorph{ T } }"             , "  { T }"             , "  { }"             , "  { }"             , "\\phinoMorphingRule{xi}"-            , "  { \\mathbb{M}( $ ) }"+            , "  { \\phinoMorph{ \\phiTerminal{\\xi} } }"             , "  { T }"             , "  { }"             , "  { }"             , "\\phinoMorphingRule{globe}"-            , "  { \\mathbb{M}( Q ) }"+            , "  { \\phinoMorph{ Q } }"             , "  { T }"             , "  { }"             , "  { }"@@ -1080,34 +1097,34 @@       testCLISucceeded         ["explain", "--dataize"]         [ unlines-            [ "\\phinoDataizationRule{delta}"-            , "  { \\mathbb{D}( [[ B_1, D> \\delta, B_2 ]] ) }"+            [ "\\phinoDataizationRule[\\Delta]{delta}"+            , "  { \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] } }"             , "  { \\delta }"             , "  { }"             , "  { }"             , "\\phinoDataizationRule{box}"-            , "  { \\mathbb{D}( [[ B_1, @ -> e, B_2 ]] ) }"-            , "  { \\mathbb{D}( \\phinoNormalize{ e_1 } ) }"+            , "  { \\phinoDataize{ [[ B_1, @ -> e, B_2 ]] } }"+            , "  { \\phinoDataize{ \\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}( \\phinoNormalize{ e } ) }"+            , "  { \\phinoDataize{ [[ B_1, L> F, B_2 ]] } }"+            , "  { \\phinoDataize{ \\phinoNormalize{ e } } }"             , "  { }"             , "  { e \\coloneqq \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] } }"             , "\\phinoDataizationRule{none}"-            , "  { \\mathbb{D}( [[ B ]] ) }"+            , "  { \\phinoDataize{ [[ B ]] } }"             , "  { \\varnothing }"             , "  { }"             , "  { }"             , "\\phinoDataizationRule{bott}"-            , "  { \\mathbb{D}( T ) }"+            , "  { \\phinoDataize{ T } }"             , "  { \\varnothing }"             , "  { }"             , "  { }"             , "\\phinoDataizationRule{norm}"-            , "  { \\mathbb{D}( n ) }"-            , "  { \\mathbb{D}( \\mathbb{M}( n ) ) }"+            , "  { \\phinoDataize{ n } }"+            , "  { \\phinoDataize{ \\phinoMorph{ n } } }"             , "  { }"             , "  { }"             ]

@@ -19,6 +19,7 @@       [ "in (!t, !B)"       , " not   (in (!t1,   !B))   "       , "eq(1, 1)"+      , "gt(domain(!B), !i)"       , "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)"@@ -34,6 +35,7 @@       , ("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"))))+      , ("gt(domain(!B1),!i)", Y.Gt (Y.CmpNum (Y.Domain (BiMeta "B1"))) (Y.CmpNum (Y.MetaIndex "i")))       , ("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 @@       [ ("Q.!t", Just (ExDispatch ExRoot (AtMeta "t")))       , ("[[]](!t1 -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtMeta "t1") ExXi)))       ,-        ( "[[]](a0 -> $)(a11 -> Q)"+        ( "[[]](~0 -> $)(~11 -> Q)"         , Just             ( ExApplication                 ( ExApplication@@ -192,7 +192,7 @@       , "[[x() -> [[]] ]]"       , "Q.x(y() -> [[]])"       , "Q.x(y(q) -> [[w -> !e]])"-      , "Q.x(a1(^,@) -> [[]])"+      , "Q.x(~1(^,@) -> [[]])"       , "Q.x.^.@.!t0"       , "[[x -> y.z]]"       , "[[x -> ^, y -> @, z -> !t]]"@@ -225,7 +225,7 @@           , "Q.x(x -> ?)"           , "Q.x(L> Func)"           , "Q.x(D> --)"-          , "Q.x(a1 -> ?)"+          , "Q.x(~1 -> ?)"           , "Q.x(L> !F)"           , "Q.x(D> !b)"           , "[[α0 -> Q.x]]"@@ -235,7 +235,7 @@           , "Q.x(y(α1) -> [[]])"           , "Q.x(1, 2, !B)"           , "Q.x.α0"-          , "Q.x(a1 -> Q.y, x -> 5, !B1)"+          , "Q.x(~1 -> Q.y, x -> 5, !B1)"           , "Q.x(𝐵1, 𝜏0 -> $, x -> 𝑒)"           , "[[ x -> \"\\uD800\"]]"           , "[[ x -> \"\\uDFFF\"]]"@@ -349,6 +349,9 @@       , ("a123", Just (AtLabel "a123"))       , ("α0", Nothing)       , ("α42", Nothing)+      , ("~0", Nothing)+      , ("~1", Nothing)+      , ("~123", Nothing)       , ("X", Nothing)       , ("123", Nothing)       , ("", Nothing)@@ -464,8 +467,9 @@       , ("[[]](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)))+      , ("[[]](~!i -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i") ExXi)))       , ("[[]](α𝑖 -> Q)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i") ExRoot)))+      , ("Q.foo(a1 -> Q.y)", Just (ExApplication (ExDispatch ExRoot (AtLabel "foo")) (ArTau (AtLabel "a1") (ExDispatch ExRoot (AtLabel "y"))))) -- #875: "a"-prefixed label in argument position is a named binding, not a positional alpha       ]    describe "parse meta expressions" $