phino 0.0.81 → 0.0.82

raw patch · 28 files changed

+205/−329 lines, 28 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +43/−45
• phino.cabal +1/−1
• resources/dataization.yaml +23/−9
• resources/morphing.yaml +56/−13
• src/AST.hs +0/−13
• src/Builder.hs +0/−12
• src/CST.hs +2/−11
• src/Dataize.hs +25/−32
• src/Encoding.hs +0/−3
• src/Functions.hs +1/−1
• src/LaTeX.hs +0/−3
• src/Lining.hs +0/−2
• src/Margin.hs +0/−1
• src/Matcher.hs +2/−38
• src/Parser.hs +0/−10
• src/Printer.hs +0/−8
• src/Render.hs +0/−5
• src/Rule.hs +0/−10
• src/Sugar.hs +0/−2
• src/Tau.hs +0/−1
• src/Yaml.hs +2/−4
• test/ASTSpec.hs +1/−4
• test/BuilderSpec.hs +0/−6
• test/CLISpec.hs +38/−13
• test/DataizeSpec.hs +11/−16
• test/MatcherSpec.hs +0/−54
• test/ParserSpec.hs +0/−11
• test/PrinterSpec.hs +0/−1

@@ -34,7 +34,7 @@  ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.80+cabal install --overwrite-policy=always phino-0.0.81 phino --version ``` @@ -238,16 +238,16 @@ $ phino explain --morph \begin{tabular}{rl} \trrule{prim}-  { \mathbb{M}( e ) }-  { e }-  { if $ e \in \mathcal{P} $ }+  { \mathbb{M}( [[ B ]] ) }+  { [[ B ]] }   { }+  { } ... \trrule{root}-  { \mathbb{M}( Q . \tau * t ) }-  { \mathbb{M}( e * t ) }-  { }-  { where $ e \coloneqq global( \tau ) $ }+  { \mathbb{M}( Q ) }+  { \mathbb{M}( \mathcal{N}( e ) ) }+  { if $ e \not= Q $ }+  { where $ e \coloneqq global(  ) $ } \end{tabular} ``` @@ -260,9 +260,9 @@   { }   { } ...-\trrule{none}-  { \mathbb{D}( e ) }-  { \varnothing }+\trrule{norm}+  { \mathbb{D}( n ) }+  { \mathbb{D}( \mathbb{M}( n ) ) }   { }   { } \end{tabular}@@ -388,8 +388,6 @@                 or `nf:` guard is needed * `!B` || `𝐵` - list of bindings * `!d` || `δ` - bytes in meta delta binding-* `!t` - tail after expression, a possibly empty sequence of applications-         and/or dispatches * `!F` - function name in meta lambda binding  Every meta variable may also be used with an integer index, like `!B1` or `𝜏0`.@@ -419,55 +417,55 @@ === parse/phi ===   warmup:     3 iterations   batches:    10 x 1-  total:      1400685.745 μs-  avg:        140068.575 μs-  min:        128878.179 μs-  max:        170778.015 μs-  std dev:    15086.312 μs+  total:      1249146.083 μs+  avg:        124914.608 μs+  min:        114445.668 μs+  max:        153538.726 μs+  std dev:    14836.651 μs === parse/xmir ===   warmup:     3 iterations   batches:    10 x 1-  total:      7628269.229 μs-  avg:        762826.923 μs-  min:        700461.528 μs-  max:        895566.916 μs-  std dev:    53443.050 μs+  total:      7756845.678 μs+  avg:        775684.568 μs+  min:        717096.328 μs+  max:        814290.753 μs+  std dev:    28717.270 μs === rewrite/normalize ===   warmup:     3 iterations   batches:    10 x 1-  total:      389007.790 μs-  avg:        38900.779 μs-  min:        37763.081 μs-  max:        40258.745 μs-  std dev:    794.301 μs+  total:      438127.137 μs+  avg:        43812.714 μs+  min:        42655.269 μs+  max:        45113.109 μs+  std dev:    720.868 μs === print/sweet/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      3943382.302 μs-  avg:        394338.230 μs-  min:        375291.020 μs-  max:        416271.808 μs-  std dev:    12394.321 μs+  total:      4445373.874 μs+  avg:        444537.387 μs+  min:        426945.439 μs+  max:        466720.288 μs+  std dev:    13809.207 μs === print/sweet/flat ===   warmup:     3 iterations   batches:    10 x 1-  total:      3855869.876 μs-  avg:        385586.988 μs-  min:        365284.728 μs-  max:        405130.834 μs-  std dev:    11941.433 μs+  total:      4535005.765 μs+  avg:        453500.576 μs+  min:        426572.785 μs+  max:        478523.175 μs+  std dev:    14154.997 μs === print/salty/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      13541528.033 μs-  avg:        1354152.803 μs-  min:        1307453.767 μs-  max:        1399468.749 μs-  std dev:    27649.598 μs+  total:      13746516.677 μs+  avg:        1374651.668 μs+  min:        1338899.143 μs+  max:        1409557.147 μs+  std dev:    24026.755 μs ```  The results were calculated in [this GHA job][benchmark-gha]-on 2026-06-18 at 23:15,+on 2026-06-19 at 10:57, on Linux with 4 CPUs.  <!-- benchmark_end -->@@ -516,4 +514,4 @@ [jna]: https://github.com/java-native-access/jna [jna-native]: https://github.com/java-native-access/jna/blob/master/src/com/sun/jna/Native.java [jeo]: https://github.com/objectionary/jeo-maven-plugin-[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/27794897832+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/27821357485

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.81+version: 0.0.82 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>

@@ -26,17 +26,31 @@     dataize:       normalize: 𝑒1 -- name: norm-  description: '𝔻(n) ⟿ 𝔻(𝕄(n)) if n ∉ 𝒫'-  match: 𝑛-  when:-    not:-      primitive: 𝑛+- name: fire+  description: '𝔻(⟦𝐵1, λ ⤍ F, 𝐵2⟧) ⟿ 𝔻(𝒩(𝔼(⟦𝐵1, λ ⤍ F, 𝐵2⟧)))'+  match: ⟦𝐵1, λ ⤍ !F, 𝐵2⟧+  where:+    - meta: 𝑒+      function: lambda+      args:+        - ⟦𝐵1, λ ⤍ !F, 𝐵2⟧   then:     dataize:-      morph: 𝑛+      normalize: 𝑒  - name: none-  description: '𝔻(n) ⟿ nothing otherwise'-  match: 𝑛+  description: '𝔻(⟦𝐵⟧) ⟿ nothing'+  match: ⟦𝐵⟧   then: nothing++- name: bott+  description: '𝔻(⊥) ⟿ nothing'+  match: ⊥+  then: nothing++- name: norm+  description: '𝔻(n) ⟿ 𝔻(𝕄(n)) otherwise'+  match: 𝑛+  then:+    dataize:+      morph: 𝑛

@@ -1,17 +1,21 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----# Morphing 𝕄 — applied top-to-bottom, first matching clause wins. The input-# is always a normal form: a non-NF expression matches no clause.+# Morphing 𝕄 — applied top-to-bottom, first matching clause wins. The input is+# always a normal form: a non-NF expression matches no clause. 𝕄 navigates a+# normal form down to a formation one operation at a time,+# resolving the universe Φ and peeling dispatches and applications through+# normalization 𝒩. It never fires a bare atom: a saturated λ-formation is+# returned untouched and fired later by 𝔼 (the 'fire' rule of 𝔻).  - name: prim-  description: '𝕄(p) ⟿ p'-  match: 𝑝-  then: 𝑝+  description: '𝕄(⟦𝐵⟧) ⟿ ⟦𝐵⟧'+  match: ⟦𝐵⟧+  then: ⟦𝐵⟧  - name: lambda-  description: '𝕄(⟦𝐵1, λ ⤍ F, 𝐵2⟧ * t) ⟿ 𝕄(𝒩(F(⟦𝐵1, 𝐵2⟧) * t))'-  match: '⟦𝐵1, λ ⤍ !F, 𝐵2⟧ * !t'+  description: '𝕄(⟦𝐵1, λ ⤍ F, 𝐵2⟧.τ) ⟿ 𝕄(𝒩(𝔼(⟦𝐵1, λ ⤍ F, 𝐵2⟧).τ))'+  match: '⟦𝐵1, λ ⤍ !F, 𝐵2⟧.𝜏'   where:     - meta: 𝑒       function: lambda@@ -19,19 +23,58 @@         - '⟦𝐵1, λ ⤍ !F, 𝐵2⟧'   then:     morph:-      normalize: '𝑒 * !t'+      normalize: '𝑒.𝜏' +- name: dispatch+  description: '𝕄(n.τ) ⟿ 𝕄(𝒩(𝕄(n).τ))'+  match: '𝑛.𝜏'+  where:+    - meta: 𝑒+      function: morph+      args:+        - 𝑛+  then:+    morph:+      normalize: '𝑒.𝜏'++- name: application+  description: '𝕄(n(τ ↦ e)) ⟿ 𝕄(𝒩(𝕄(n)(τ ↦ e)))'+  match: '𝑛(𝜏 ↦ 𝑒)'+  where:+    - meta: 𝑒1+      function: morph+      args:+        - 𝑛+  then:+    morph:+      normalize: '𝑒1(𝜏 ↦ 𝑒)'++- name: applicationa+  description: '𝕄(n(η ↦ e)) ⟿ 𝕄(𝒩(𝕄(n)(η ↦ e)))'+  match: '𝑛(𝜂 ↦ 𝑒)'+  where:+    - meta: 𝑒1+      function: morph+      args:+        - 𝑛+  then:+    morph:+      normalize: '𝑒1(𝜂 ↦ 𝑒)'+ - name: root-  description: '𝕄(Φ.τ * t) ⟿ 𝕄(𝒩(e * t)) if Φ ↦ ⟦𝐵1, τ ↦ e, 𝐵2⟧'-  match: 'Φ.𝜏 * !t'+  description: '𝕄(Φ) ⟿ 𝕄(𝒩(e)) where e := global(), unless e is Φ'+  match: Φ   where:     - meta: 𝑒       function: global-      args:-        - 𝜏+  when:+    not:+      eq:+        - 𝑒+        - Φ   then:     morph:-      normalize: '𝑒 * !t'+      normalize: 𝑒  - name: stuck   description: '𝕄(n) ⟿ ⊥ otherwise'

@@ -24,7 +24,6 @@   | ExApplication Expression Argument   | ExDispatch Expression Attribute   | ExMeta Text-  | ExMetaTail Expression Text   | ExPhiMeet (Maybe String) Int Expression   | ExPhiAgain (Maybe String) Int Expression   deriving (Eq, Ord, Show, Generic)@@ -109,7 +108,6 @@       ExApplication ex arg -> goArgument (goExpr (step h 5) ex) arg       ExDispatch ex at -> goAttribute (goExpr (step h 6) ex) at       ExMeta t -> hashText (step h 7) t-      ExMetaTail ex t -> hashText (goExpr (step h 8) ex) t       ExPhiMeet ms i ex -> goExpr (hashMaybeString (step (step h 9) i) ms) ex       ExPhiAgain ms i ex -> goExpr (hashMaybeString (step (step h 10) i) ms) ex     goBinding :: Int -> Binding -> Int@@ -146,16 +144,6 @@       Function t -> hashText (step h 16) t       FnMeta t -> hashText (step h 29) t --- A primitive is the termination ⊥ or a formation without a λ binding.-primitive :: Expression -> Bool-primitive ExTermination = True-primitive (ExFormation bds) = not (any lambda bds)-  where-    lambda :: Binding -> Bool-    lambda (BiLambda _) = True-    lambda _ = False-primitive _ = False- countNodes :: Expression -> Int countNodes (ExFormation bds) = 1 + sum (map nodesInBinding bds) + length bds   where@@ -166,7 +154,6 @@ countNodes (ExApplication expr (ArTau _ expr')) = 4 + countNodes expr + countNodes expr' countNodes (ExApplication expr (ArAlpha _ expr')) = 4 + countNodes expr + countNodes expr' countNodes (ExDispatch expr' _) = 2 + countNodes expr'-countNodes (ExMetaTail expr _) = 2 + countNodes expr countNodes (ExPhiMeet _ _ expr) = countNodes expr countNodes (ExPhiAgain _ _ expr) = countNodes expr countNodes _ = 1

@@ -121,12 +121,6 @@   bds <- buildBindings rest subst   Right (first ++ bds) -buildExpressionWithTails :: Expression -> [Tail] -> Subst -> Expression-buildExpressionWithTails expr [] _ = expr-buildExpressionWithTails ex (tl : rest) subst = case tl of-  TaApplication arg -> buildExpressionWithTails (ExApplication ex arg) rest subst-  TaDispatch at -> buildExpressionWithTails (ExDispatch ex at) rest subst- -- Build meta expression with given substitution buildExpression :: Expression -> Subst -> Built Expression buildExpression (ExDispatch ex at) subst = do@@ -147,12 +141,6 @@           ExFormation bds -> uniqueBindings bds >> res           _ -> res   _ -> Left (metaMsg meta)-buildExpression (ExMetaTail expr meta) subst = do-  let (Subst mp) = subst-  expression <- buildExpression expr subst-  case Map.lookup meta mp of-    Just (MvTail tails) -> Right (buildExpressionWithTails expression tails subst)-    _ -> Left (metaMsg meta) buildExpression expr _ = Right expr  buildBytesThrows :: Bytes -> Subst -> IO Bytes

@@ -83,8 +83,6 @@   | N' -- n   | K -- 𝑘   | K' -- k-  | P -- 𝑝-  | P' -- p   | A -- a   | TAU -- 𝜏   | TAU' -- \tau@@ -95,7 +93,6 @@   | B' -- B   | D -- δ   | D' -- \delta-  | TAIL -- t   | F -- F   deriving (Eq, Show) @@ -171,7 +168,6 @@   | EX_STRING {str :: String, tab :: TAB, rhos :: [Argument]}   | EX_NUMBER {num :: Either Int Double, tab :: TAB, rhos :: [Argument]}   | EX_META {meta :: META}-  | EX_META_TAIL {expr :: EXPRESSION, meta :: META}   | EX_PHI_MEET {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION}   | EX_PHI_AGAIN {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION}   deriving (Eq, Show)@@ -230,7 +226,6 @@   | CO_COMPARE {left :: COMPARABLE, equal :: EQUAL, right :: COMPARABLE}   | CO_MATCHES {regex :: String, expr :: EXPRESSION}   | CO_PART_OF {expr :: EXPRESSION, binding :: BINDING}-  | CO_PRIMITIVE {expr :: EXPRESSION, belongs :: BELONGING}   | CO_DISJOINT {attrs :: [ATTRIBUTE], groups :: [BINDING]}   deriving (Eq, Show) @@ -293,13 +288,12 @@  -- The first character of an expression meta name encodes its kind: -- 'n'-prefixed names are normal-form-constrained '𝑛' metas, 'k'-prefixed--- names are absolute-constrained '𝑘' metas, 'p'-prefixed names are--- primitive-constrained '𝑝' metas, everything else is an ordinary '𝑒' meta.+-- names are absolute-constrained '𝑘' metas, everything else is an ordinary+-- '𝑒' meta. exMetaHead :: T.Text -> META_HEAD exMetaHead mt   | T.isPrefixOf "n" mt = N   | T.isPrefixOf "k" mt = K-  | T.isPrefixOf "p" mt = P   | otherwise = E  -- This class is used to convert AST to CST@@ -315,7 +309,6 @@   toCST ExRoot _ = EX_GLOBAL Φ   toCST ExXi _ = EX_XI XI   toCST (ExMeta mt) _ = EX_META (META NO_EXCL (exMetaHead mt) (metaTail mt))-  toCST (ExMetaTail expr mt) ctx = EX_META_TAIL (toCST expr ctx) (META EXCL TAIL (metaTail mt))   toCST ExTermination _ = EX_TERMINATION DEAD   toCST (ExPhiMeet prefix idx expr) ctx = EX_PHI_MEET prefix idx (toCST expr ctx)   toCST (ExPhiAgain prefix idx expr) ctx = EX_PHI_AGAIN prefix idx (toCST expr ctx)@@ -526,8 +519,6 @@ 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.Primitive expr)) _ = CO_PRIMITIVE (expressionToCST expr) NOT_IN-  toCST (Y.Primitive expr) _ = CO_PRIMITIVE (expressionToCST expr) IN   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)

@@ -12,7 +12,7 @@ module Dataize (morph, dataize, dataize', DataizeContext (..), execBuildTerm) where  import AST-import Builder (buildAttributeThrows, buildBytesThrows, buildExpressionThrows)+import Builder (buildBytesThrows, buildExpressionThrows) import Control.Exception (throwIO) import Data.List (partition) import Data.List.NonEmpty (NonEmpty (..))@@ -20,7 +20,7 @@ import qualified Data.Text as T import Deps (BuildTermFunc, BuildTermMethod, SaveStepFunc, Term (TeAttribute, TeExpression)) import Locator (locatedExpression, withLocatedExpression)-import Matcher (Subst, substEmpty)+import Matcher (Subst (..), substEmpty) import Misc import Must (Must (..)) import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite)@@ -65,25 +65,9 @@             [bd] -> (Just bd, rest)             _ -> (Nothing, bds) --- Resolve dispatch from global object (Q.tau) for ROOT Morphing rule.--- Here tau is the name of the attribute which is taken from Q--- and expr is expression which program refers to.--- If Q refers to formation which contains binding with attribute == tau ---- the expression from this binding is returned.-phiDispatch :: T.Text -> Expression -> Maybe Expression-phiDispatch tau expr = case expr of-  ExFormation bds -> boundExpr bds-  _ -> Nothing-  where-    boundExpr :: [Binding] -> Maybe Expression-    boundExpr [] = Nothing-    boundExpr (bd : bds) = case bd of-      BiTau (AtLabel attr) expr' -> if attr == tau then Just expr' else boundExpr bds-      _ -> boundExpr bds---- The Morphing function 𝕄 maps normal forms to primitives. It is driven by the+-- The Morphing function 𝕄 maps normal forms to formations. It is driven by the -- ordered rules from 'morphing.yaml': the first matching rule's 'then' outcome--- either stops with a primitive ('MoStop') or keeps morphing ('MoMorph'). When+-- either stops at a formation ('MoStop') or keeps morphing ('MoMorph'). When -- the morphed argument is a normalization ('MaNormalize', as in the 'lambda' and -- 'root' rules), the rewriter runs over the rule's product and its individual -- steps are spliced into the chain before morphing continues.@@ -117,7 +101,9 @@       morph (built, seq') ctx     -- 𝕄(𝒩(e)) records the producing step, then delegates to the normalization     -- rewriter and splices its individual steps (alpha, copy, dot, …) into the-    -- chain before morphing on the resulting normal form.+    -- 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.     apply (Y.MoMorph (Y.MaNormalize arg)) name subst = do       built <- buildExpressionThrows arg subst       labelled <- leadsTo seq name built ctx@@ -132,9 +118,10 @@  -- The Dataization function 𝔻 retrieves bytes from an expression. It is driven -- by the ordered rules from 'dataization.yaml': 'delta' yields the asset bytes,--- 'none' yields nothing, 'box' contextualizes the φ-body and keeps dataizing--- (its step is labelled by the operation, 'contextualize'), and 'norm' reduces--- through morphing, splicing the morphing steps into the chain.+-- 'none' (a formation) and 'bott' (⊥) yield nothing, 'box' contextualizes the+-- φ-body and keeps dataizing (its step is labelled by the operation,+-- 'contextualize'), and 'norm' reduces through morphing, splicing the morphing+-- steps into the chain. dataize' :: Dataizable -> DataizeContext -> IO Dataized dataize' (expr, seq) ctx = do   matched <- firstMatch Y.dataizationRules@@ -258,6 +245,7 @@ execBuildTerm :: DataizeContext -> BuildTermFunc execBuildTerm ctx "lambda" = _lambda ctx execBuildTerm ctx "global" = _global ctx+execBuildTerm ctx "morph" = _morph ctx execBuildTerm ctx func = _buildTerm ctx func  _lambda :: DataizeContext -> BuildTermMethod@@ -273,11 +261,16 @@ _lambda _ _ _ = throwIO (userError "Function lambda() requires exactly 1 expression argument")  _global :: DataizeContext -> BuildTermMethod-_global DataizeContext{_program = Program prog} [ArgAttribute attr] subst = do-  attr' <- buildAttributeThrows attr subst-  case attr' of-    AtLabel label -> case phiDispatch label prog of-      Just expr -> pure (TeExpression expr)-      Nothing -> throwIO (userError (printf "Universe Q has no attribute '%s'" (show attr')))-    _ -> throwIO (userError "Function global() expects a labelled attribute")-_global _ _ _ = throwIO (userError "Function global() requires exactly 1 attribute argument")+_global DataizeContext{_program = Program prog} [] _ = pure (TeExpression prog)+_global _ _ _ = throwIO (userError "Function global() requires no arguments")++-- The Morphing function 𝕄 exposed as a build-term function so a rule can morph+-- a sub-expression in its 'where' (the 'dispatch' and 'application' rules morph+-- the head before re-attaching it). The step chain is discarded: the producing+-- rule splices the surrounding normalization steps itself.+_morph :: DataizeContext -> BuildTermMethod+_morph ctx@DataizeContext{_program = prog} [ArgExpression expr] subst = do+  built <- buildExpressionThrows expr subst+  (morphed, _) <- morph (built, (prog, Nothing) :| []) ctx+  pure (TeExpression morphed)+_morph _ _ _ = throwIO (userError "Function morph() requires exactly 1 expression argument")

@@ -33,9 +33,7 @@   toASCII EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toASCII expr) space eol tab (toASCII args) eol' tab' indent   toASCII EX_META{meta = META{hd = N, ..}} = EX_META (META EXCL N' rest)   toASCII EX_META{meta = META{hd = K, ..}} = EX_META (META EXCL K' rest)-  toASCII EX_META{meta = META{hd = P, ..}} = EX_META (META EXCL P' rest)   toASCII EX_META{..} = EX_META (META EXCL E' (rest meta))-  toASCII EX_META_TAIL{..} = EX_META_TAIL (toASCII expr) meta   toASCII EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toASCII expr)   toASCII EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toASCII expr)   toASCII expr = expr@@ -102,7 +100,6 @@   toASCII CO_COMPARE{..} = CO_COMPARE (toASCII left) equal (toASCII right)   toASCII CO_MATCHES{..} = CO_MATCHES regex (toASCII expr)   toASCII CO_PART_OF{..} = CO_PART_OF (toASCII expr) (toASCII binding)-  toASCII CO_PRIMITIVE{..} = CO_PRIMITIVE (toASCII expr) belongs   toASCII CO_DISJOINT{..} = CO_DISJOINT (map toASCII attrs) (map toASCII groups)   toASCII CO_EMPTY = CO_EMPTY 

@@ -29,7 +29,7 @@ -- 'Dataize.execBuildTerm', not by 'buildTerm'. They are available while -- executing dataization and morphing rules, but not rewriting rules. execFunctions :: [String]-execFunctions = ["lambda", "global"]+execFunctions = ["lambda", "global", "morph"]  buildTerm :: BuildTermFunc buildTerm func args subst = do

@@ -223,7 +223,6 @@   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_META_TAIL{..} = EX_META_TAIL (toLaTeX expr) (toLaTeX meta)   toLaTeX expr = expr  instance ToLaTeX ATTRIBUTE where@@ -270,7 +269,6 @@   toLaTeX E = E'   toLaTeX N = N'   toLaTeX K = K'-  toLaTeX P = P'   toLaTeX A = TAU'   toLaTeX TAU = TAU'   toLaTeX ETA = ETA'@@ -323,7 +321,6 @@   toLaTeX CO_COMPARE{..} = CO_COMPARE (toLaTeX left) equal (toLaTeX right)   toLaTeX CO_MATCHES{..} = CO_MATCHES regex (toLaTeX expr)   toLaTeX CO_PART_OF{..} = CO_PART_OF (toLaTeX expr) (toLaTeX binding)-  toLaTeX CO_PRIMITIVE{..} = CO_PRIMITIVE (toLaTeX expr) belongs   toLaTeX CO_DISJOINT{..} = CO_DISJOINT (map toLaTeX attrs) (map toLaTeX groups)   toLaTeX CO_EMPTY = CO_EMPTY 

@@ -31,7 +31,6 @@   toSingleLine EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toSingleLine expr) space NO_EOL TAB' (toSingleLine args) NO_EOL TAB' indent   toSingleLine EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSingleLine expr)   toSingleLine EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toSingleLine expr)-  toSingleLine EX_META_TAIL{..} = EX_META_TAIL (toSingleLine expr) meta   toSingleLine expr = expr  instance ToSingleLine APP_BINDING where@@ -82,7 +81,6 @@   toSingleLine CO_COMPARE{..} = CO_COMPARE (toSingleLine left) equal (toSingleLine right)   toSingleLine CO_MATCHES{..} = CO_MATCHES regex (toSingleLine expr)   toSingleLine CO_PART_OF{..} = CO_PART_OF (toSingleLine expr) (toSingleLine binding)-  toSingleLine CO_PRIMITIVE{..} = CO_PRIMITIVE (toSingleLine expr) belongs   toSingleLine CO_DISJOINT{..} = CO_DISJOINT attrs (map toSingleLine groups)   toSingleLine CO_EMPTY = CO_EMPTY 

@@ -36,7 +36,6 @@   withMargin' _ num@EX_NUMBER{} = num   withMargin' _ str@EX_STRING{} = str   withMargin' cfg EX_DISPATCH{..} = EX_DISPATCH (withMargin' cfg expr) space attr-  withMargin' cfg EX_META_TAIL{..} = EX_META_TAIL (withMargin' cfg expr) meta   withMargin' cfg EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (withMargin' cfg expr)   withMargin' cfg EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (withMargin' cfg expr)   withMargin' cfg@(extra, margin) ex@EX_APPLICATION{tab = tab@(TAB indt), ..} =

@@ -1,5 +1,3 @@-{-# LANGUAGE OverloadedStrings #-}- -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT @@ -11,7 +9,7 @@ import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Maybe (catMaybes)-import Data.Text (Text, isPrefixOf)+import Data.Text (Text)  -- Meta value -- The right part of substitution@@ -22,16 +20,8 @@   | MvBindings [Binding] -- !B   | MvFunction Text -- !F   | MvExpression Expression -- !e-  | MvTail [Tail] -- !t   deriving (Eq, Show) --- Tail operation after expression--- Dispatch or application-data Tail-  = TaApplication Argument -- application argument-  | TaDispatch Attribute-  deriving (Eq, Show)- -- Substitution -- Shows the match of meta name to meta value newtype Subst = Subst (Map Text MetaValue)@@ -112,40 +102,14 @@ matchBindings (pb : pbs) (tb : tbs) = combineMany (matchBinding pb tb) (matchBindings pbs tbs) matchBindings _ _ = [] --- Recursively go through given target expression and try to find--- the head expression which matches to given pattern.--- If there's one - build the list of all the tail operations after head expression.--- The tail operations may be only dispatches or applications-tailExpressions :: Expression -> Expression -> ([Subst], [Tail])-tailExpressions ptn tgt = case tailExpressionsReversed ptn tgt of-  Just (substs, tails) -> (substs, reverse tails)-  _ -> ([], [])-  where-    tailExpressionsReversed :: Expression -> Expression -> Maybe ([Subst], [Tail])-    tailExpressionsReversed ptn' tgt' = case matchExpression' ptn' tgt' of-      [] -> case tgt' of-        ExDispatch expr attr -> do-          (substs, tails) <- tailExpressionsReversed ptn' expr-          Just (substs, TaDispatch attr : tails)-        ExApplication expr arg -> do-          (substs, tails) <- tailExpressionsReversed ptn' expr-          Just (substs, TaApplication arg : tails)-        _ -> Just ([], [])-      substs -> Just (substs, [])- matchExpression' :: MatchExpressionFunc-matchExpression' (ExMeta meta) tgt-  | "p" `isPrefixOf` meta = [substSingle meta (MvExpression tgt) | primitive tgt]-  | otherwise = [substSingle meta (MvExpression tgt)]+matchExpression' (ExMeta meta) tgt = [substSingle meta (MvExpression tgt)] matchExpression' ExXi ExXi = [substEmpty] matchExpression' ExRoot ExRoot = [substEmpty] matchExpression' ExTermination ExTermination = [substEmpty] matchExpression' (ExFormation pbs) (ExFormation tbs) = matchBindings pbs tbs matchExpression' (ExDispatch pexp pattr) (ExDispatch texp tattr) = combineMany (matchAttribute pattr tattr) (matchExpression' pexp texp) matchExpression' (ExApplication pexp parg) (ExApplication texp targ) = combineMany (matchExpression' pexp texp) (matchArgument parg targ)-matchExpression' (ExMetaTail expr meta) tgt = case tailExpressions expr tgt of-  ([], _) -> []-  (substs, tails) -> combineMany substs [substSingle meta (MvTail tails)] matchExpression' (ExPhiAgain prefix idx expr) (ExPhiAgain prefix' idx' expr')   | prefix == prefix' && idx == idx' = matchExpression' expr expr'   | otherwise = []

@@ -400,7 +400,6 @@     , try (ExMeta <$> meta' 'e' "𝑒")     , try (ExMeta <$> meta' 'n' "𝑛")     , try (ExMeta <$> meta' 'k' "𝑘")-    , try (ExMeta <$> meta' 'p' "𝑝")     , ExDispatch ExXi <$> attribute     ]     <?> "expression head"@@ -411,7 +410,6 @@ -- tail optional part of application -- 1. any head + dispatch -- 2. any head except $ and Q + application--- 3. any head except meta tail + meta tail exTail :: Expression -> Parser Expression exTail expr =   choice@@ -438,14 +436,6 @@                     ]                 _ <- symbol ")"                 return (application expr bds)-            , do-                guard-                  ( case expr of-                      ExMetaTail _ _ -> False-                      _ -> True-                  )-                _ <- symbol "*"-                ExMetaTail expr <$> meta 't'             ]             <?> "dispatch or application"         exTail next

@@ -77,9 +77,6 @@ printBinding :: Binding -> String printBinding bd = printBinding' bd defaultPrintConfig -printArgument' :: Argument -> PrintConfig -> String-printArgument' arg (_, encoding, _, _) = T.unpack $ render (withEncoding encoding (toCST arg (0, NO_EOL) :: PAIR))- printBytes :: Bytes -> String printBytes bts = T.unpack $ render (toCST bts (0, NO_EOL) :: BYTES) @@ -92,10 +89,6 @@ printExtraArg :: ExtraArgument -> String printExtraArg arg = printExtraArg' arg defaultPrintConfig -printTail :: Tail -> PrintConfig -> String-printTail (TaApplication arg) config = "(" <> printArgument' arg config <> ")"-printTail (TaDispatch att) (_, encoding, _, _) = "." <> printAttribute' att encoding- printMetaValue :: MetaValue -> PrintConfig -> String printMetaValue (MvAttribute att) (_, encoding, _, _) = printAttribute' att encoding printMetaValue (MvAlpha index) (_, encoding, _, _) = printAlpha' index encoding@@ -103,7 +96,6 @@ printMetaValue (MvBytes bts) _ = printBytes bts printMetaValue (MvBindings bds) config = printExpression' (ExFormation bds) config printMetaValue (MvFunction fun) _ = T.unpack fun-printMetaValue (MvTail tails) config = intercalate "," (map (`printTail` config) tails)  printSubst :: Subst -> PrintConfig -> String printSubst (Subst mp) config =

@@ -117,8 +117,6 @@   render N' = "n"   render K = "𝑘"   render K' = "k"-  render P = "𝑝"-  render P' = "p"   render A = "a"   render TAU = "𝜏"   render TAU' = "\\tau"@@ -129,7 +127,6 @@   render B' = "B"   render D = "δ"   render D' = "\\delta"-  render TAIL = "t"   render F = "F"  instance Render META where@@ -201,7 +198,6 @@   render EX_STRING{..} = "\"" <> render str <> "\""   render EX_NUMBER{..} = either (T.pack . show) (T.pack . show) num   render EX_META{..} = render meta-  render EX_META_TAIL{..} = render expr <> " * " <> 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 <> "}" @@ -260,7 +256,6 @@   render CO_COMPARE{..} = render left <> " " <> render equal <> " " <> render right   render CO_MATCHES{..} = "matches( " <> T.pack regex <> ", " <> render expr <> " )"   render CO_PART_OF{..} = "part-of( " <> render expr <> ", " <> render binding <> " )"-  render CO_PRIMITIVE{..} = render expr <> " " <> render belongs <> " \\mathcal{P}"   render CO_DISJOINT{..} =     "[ "       <> T.intercalate ", " (map render attrs)

@@ -207,14 +207,6 @@     partOf expr (BiTau _ expr' : rest) = expr == expr' || partOf expr rest     partOf expr (_ : rest) = partOf expr rest --- A primitive is the termination ⊥ or a formation without a λ binding;--- expression metas are resolved through the substitution first.-_primitive :: Expression -> Subst -> RuleContext -> IO [Subst]-_primitive (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of-  Just (MvExpression expr) -> _primitive expr (Subst mp) ctx-  _ -> pure []-_primitive expr subst _ = pure [subst | primitive expr]- -- Hold if none of the given attributes is present in the union of the -- bindings captured by the given binding metas. _disjoint :: [Attribute] -> [Binding] -> Subst -> RuleContext -> IO [Subst]@@ -244,7 +236,6 @@ meetCondition' (Y.Absolute expr) = _absolute expr meetCondition' (Y.Matches pat expr) = _matches pat expr meetCondition' (Y.PartOf expr bd) = _partOf expr bd-meetCondition' (Y.Primitive expr) = _primitive expr meetCondition' (Y.Disjoint attrs bds) = _disjoint attrs bds  -- For each substitution check if it meetCondition to given condition@@ -325,7 +316,6 @@     go (ExFormation bds) = concatMap goBinding bds     go (ExApplication e arg) = go e ++ goArgument arg     go (ExDispatch e _) = go e-    go (ExMetaTail e _) = go e     go (ExPhiMeet _ _ e) = go e     go (ExPhiAgain _ _ e) = go e     go _ = []

@@ -110,7 +110,6 @@       rhos   toSalty EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSalty expr)   toSalty EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toSalty expr)-  toSalty EX_META_TAIL{..} = EX_META_TAIL (toSalty expr) meta   toSalty expr = expr  saltifyPrimitive :: EXPRESSION -> EXPRESSION -> EXPRESSION -> TAB -> [Argument] -> EXPRESSION@@ -196,7 +195,6 @@   toSalty CO_COMPARE{..} = CO_COMPARE (toSalty left) equal (toSalty right)   toSalty CO_MATCHES{..} = CO_MATCHES regex (toSalty expr)   toSalty CO_PART_OF{..} = CO_PART_OF (toSalty expr) (toSalty binding)-  toSalty CO_PRIMITIVE{..} = CO_PRIMITIVE (toSalty expr) belongs   toSalty CO_DISJOINT{..} = CO_DISJOINT attrs (map toSalty groups)   toSalty CO_EMPTY = CO_EMPTY 

@@ -55,7 +55,6 @@ exprLabels (ExFormation bds) = Set.unions (map bindingLabels bds) exprLabels (ExApplication expr arg) = exprLabels expr <> argumentLabels arg exprLabels (ExDispatch expr attr) = exprLabels expr <> attrLabel attr-exprLabels (ExMetaTail expr _) = exprLabels expr exprLabels (ExPhiMeet _ _ expr) = exprLabels expr exprLabels (ExPhiAgain _ _ expr) = exprLabels expr exprLabels _ = Set.empty

@@ -81,14 +81,13 @@     withObject       "Condition"       ( \v -> do-          validateYamlObject v ["and", "or", "not", "nf", "absolute", "eq", "in", "matches", "part-of", "primitive", "disjoint"]+          validateYamlObject v ["and", "or", "not", "nf", "absolute", "eq", "in", "matches", "part-of", "disjoint"]           asum             [ And <$> v .: "and"             , Or <$> v .: "or"             , Not <$> v .: "not"             , NF <$> v .: "nf"             , Absolute <$> v .: "absolute"-            , Primitive <$> v .: "primitive"             , do                 vals <- v .: "disjoint"                 case vals of@@ -172,7 +171,6 @@   | Absolute Expression   | Matches String Expression   | PartOf Expression Binding-  | Primitive Expression   | Disjoint [Attribute] [Binding]   deriving (Eq, Generic, Show) @@ -216,7 +214,7 @@  -- The right-hand side of a morphing reduction 𝕄(match) ⟿ then. -- A mapping ('{ morph: arg }') keeps reducing under 𝕄; a bare expression--- (including ⊥) is the terminal primitive result.+-- (including ⊥) is the terminal result. data MorphOutcome   = MoMorph MorphArg   | MoStop Expression

@@ -180,8 +180,6 @@       , ("application equals", ExApplication ExRoot (ArTau AtRho ExXi), ExApplication ExRoot (ArTau AtRho ExXi), True)       , ("dispatch equals", ExDispatch ExRoot AtRho, ExDispatch ExRoot AtRho, True)       , ("dispatch differs", ExDispatch ExRoot AtRho, ExDispatch ExRoot AtPhi, False)-      , ("metatail equals", ExMetaTail ExRoot "t", ExMetaTail ExRoot "t", True)-      , ("metatail differs", ExMetaTail ExRoot "t", ExMetaTail ExRoot "s", False)       ]       ( \(desc, lhs, rhs, expected) ->           it desc $ (lhs == rhs) `shouldBe` expected@@ -199,7 +197,7 @@    describe "Expression Ord instance orders correctly" $     it "sorts expressions by constructor order" $-      let exprs = [ExMetaTail ExRoot "t", ExDispatch ExRoot AtRho, ExApplication ExRoot (ArTau AtRho ExRoot), ExMeta "e", ExTermination, ExRoot, ExXi, ExFormation []]+      let exprs = [ExDispatch ExRoot AtRho, ExApplication ExRoot (ArTau AtRho ExRoot), ExMeta "e", ExTermination, ExRoot, ExXi, ExFormation []]           first : _ = sort exprs        in first `shouldBe` ExFormation [] @@ -238,7 +236,6 @@       , ("meta binding", ExFormation [BiMeta "B"], 3)       , ("metalambda binding", ExFormation [BiLambda (FnMeta "F")], 5)       , ("meta expression", ExMeta "e", 1)-      , ("metatail expression", ExMetaTail ExRoot "t", 3)       , ("deeply nested dispatch", ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b"), 5)       , ("formation with dispatch inside", ExFormation [BiTau AtRho (ExDispatch ExRoot (AtLabel "x"))], 7)       ]

@@ -49,12 +49,6 @@             )         )       ,-        ( "Q * !t => (!t >> [.a, .b, (~1 -> $.x)]) => Q.a.b(~1 -> $.x)"-        , ExMetaTail ExRoot "t"-        , [("t", MvTail [TaDispatch (AtLabel "a"), TaDispatch (AtLabel "b"), TaApplication (ArAlpha (Alpha 1) (ExDispatch ExXi (AtLabel "x")))])]-        , Right (ExApplication (ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b")) (ArAlpha (Alpha 1) (ExDispatch ExXi (AtLabel "x"))))-        )-      ,         ( "Q.!a => () => X"         , ExDispatch ExRoot (AtMeta "a")         , []

@@ -1014,20 +1014,35 @@         [ unlines             [ "\\begin{tabular}{rl}"             , "\\trrule{prim}"-            , "  { \\mathbb{M}( p ) }"-            , "  { p }"+            , "  { \\mathbb{M}( [[ B ]] ) }"+            , "  { [[ B ]] }"             , "  { }"             , "  { }"             , "\\trrule{lambda}"-            , "  { \\mathbb{M}( [[ B_1, L> F, B_2 ]] * t ) }"-            , "  { \\mathbb{M}( \\mathcal{N}( e * t ) ) }"+            , "  { \\mathbb{M}( [[ B_1, L> F, B_2 ]] . \\tau ) }"+            , "  { \\mathbb{M}( \\mathcal{N}( e . \\tau ) ) }"             , "  { }"             , "  { where $ e \\coloneqq lambda( [[ B_1, L> F, B_2 ]] ) $ }"-            , "\\trrule{root}"-            , "  { \\mathbb{M}( Q . \\tau * t ) }"-            , "  { \\mathbb{M}( \\mathcal{N}( e * t ) ) }"+            , "\\trrule{dispatch}"+            , "  { \\mathbb{M}( n . \\tau ) }"+            , "  { \\mathbb{M}( \\mathcal{N}( e . \\tau ) ) }"             , "  { }"-            , "  { where $ e \\coloneqq global( \\tau ) $ }"+            , "  { where $ e \\coloneqq morph( n ) $ }"+            , "\\trrule{application}"+            , "  { \\mathbb{M}( n ( \\tau -> e ) ) }"+            , "  { \\mathbb{M}( \\mathcal{N}( e_1 ( \\tau -> e ) ) ) }"+            , "  { }"+            , "  { where $ e_1 \\coloneqq morph( n ) $ }"+            , "\\trrule{applicationa}"+            , "  { \\mathbb{M}( n ( \\eta -> e ) ) }"+            , "  { \\mathbb{M}( \\mathcal{N}( e_1 ( \\eta -> e ) ) ) }"+            , "  { }"+            , "  { where $ e_1 \\coloneqq morph( n ) $ }"+            , "\\trrule{root}"+            , "  { \\mathbb{M}( Q ) }"+            , "  { \\mathbb{M}( \\mathcal{N}( e ) ) }"+            , "  { if $ e \\not= Q $ }"+            , "  { where $ e \\coloneqq global(  ) $ }"             , "\\trrule{stuck}"             , "  { \\mathbb{M}( n ) }"             , "  { T }"@@ -1052,14 +1067,24 @@             , "  { \\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{norm}"-            , "  { \\mathbb{D}( n ) }"-            , "  { \\mathbb{D}( \\mathbb{M}( n ) ) }"-            , "  { if $ n \\notin \\mathcal{P} $ }"+            , "\\trrule{fire}"+            , "  { \\mathbb{D}( [[ B_1, L> F, B_2 ]] ) }"+            , "  { \\mathbb{D}( \\mathcal{N}( e ) ) }"             , "  { }"+            , "  { where $ e \\coloneqq lambda( [[ B_1, L> F, B_2 ]] ) $ }"             , "\\trrule{none}"-            , "  { \\mathbb{D}( n ) }"+            , "  { \\mathbb{D}( [[ B ]] ) }"             , "  { \\varnothing }"+            , "  { }"+            , "  { }"+            , "\\trrule{bott}"+            , "  { \\mathbb{D}( T ) }"+            , "  { \\varnothing }"+            , "  { }"+            , "  { }"+            , "\\trrule{norm}"+            , "  { \\mathbb{D}( n ) }"+            , "  { \\mathbb{D}( \\mathbb{M}( n ) ) }"             , "  { }"             , "  { }"             , "\\end{tabular}"

@@ -57,10 +57,10 @@       , ("$ => X", ExXi, ExRoot, ExTermination)       , ("Q => X", ExRoot, ExRoot, ExTermination)       ,-        ( "Q.x (Q -> [[ x -> [[]] ]]) => [[]]"+        ( "Q.x (Q -> [[ x -> [[]] ]]) => [[ ρ -> Q ]]"         , ExDispatch ExRoot (AtLabel "x")         , ExFormation [BiTau (AtLabel "x") (ExFormation [])]-        , ExFormation []+        , ExFormation [BiTau AtRho (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho])]         )       ] @@ -104,10 +104,10 @@       ]    describe "execBuildTerm" $-    it "resolves global dispatch from the universe Q" $ do+    it "returns the universe Q body for global()" $ do       prog <- parseProgramThrows "Q -> [[ x -> [[ D> 42- ]] ]]"-      expected <- parseExpressionThrows "[[ D> 42- ]]"-      term <- execBuildTerm (defaultDataizeContext ExRoot prog) "global" [Yaml.ArgAttribute (AtLabel "x")] substEmpty+      expected <- parseExpressionThrows "[[ x -> [[ D> 42- ]] ]]"+      term <- execBuildTerm (defaultDataizeContext ExRoot prog) "global" [] substEmpty       case term of         TeExpression actual -> actual `shouldBe` expected         _ -> expectationFailure "global() did not return an expression"@@ -160,24 +160,19 @@           "Q -> [[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"       labels         `shouldBe` [ "contextualize"-                   , "root"-                   , "alpha"-                   , "copy"-                   , "dot"-                   , "copy"+                   , "applicationa"                    , "alpha"                    , "copy"+                   , "prim"                    , "lambda"-                   , "root"+                   , "applicationa"                    , "alpha"                    , "copy"                    , "prim"                    , "contextualize"                    , "dot"-                   , "root"-                   , "alpha"-                   , "copy"-                   , "copy"+                   , "application"+                   , "stay"                    , "prim"                    , "contextualize"                    , "dot"@@ -185,7 +180,7 @@                    ]     it "dataizes a located reference through the expected rules" $ do       labels <- labelsOf "Q.foo.bar" "Q -> [[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]"-      labels `shouldBe` ["contextualize", "root", "prim"]+      labels `shouldBe` ["contextualize", "dispatch", "dot", "copy", "prim"]    testDataize     [

@@ -368,30 +368,6 @@         , substs [[("e", MvExpression ExRoot)]]         )       ,-        ( "!p => T => [(!p >> T)]"-        , ExMeta "p"-        , ExTermination-        , substs [[("p", MvExpression ExTermination)]]-        )-      ,-        ( "!p => [[ x -> Q ]] => [(!p >> [[ x -> Q ]])]"-        , ExMeta "p"-        , ExFormation [BiTau (AtLabel "x") ExRoot]-        , substs [[("p", MvExpression (ExFormation [BiTau (AtLabel "x") ExRoot]))]]-        )-      ,-        ( "!p => Q => []"-        , ExMeta "p"-        , ExRoot-        , substs []-        )-      ,-        ( "!p => [[ L> Func ]] => []"-        , ExMeta "p"-        , ExFormation [BiLambda (Function "Func")]-        , substs []-        )-      ,         ( "!e => Q.org(x -> $) => [(!e >> Q.org(x -> $))]"         , ExMeta "e"         , ExApplication (ExDispatch ExRoot (AtLabel "org")) (ArTau (AtLabel "x") ExXi)@@ -426,36 +402,6 @@               , ("B", MvBindings [BiTau (AtLabel "y") ExXi])               ]             ]-        )-      ,-        ( "Q * !t => Q.org => [(!t >> [.org])]"-        , ExMetaTail ExRoot "t"-        , ExDispatch ExRoot (AtLabel "x")-        , substs [[("t", MvTail [TaDispatch (AtLabel "x")])]]-        )-      ,-        ( "Q * !t => Q.org(x -> [[]]) => [(!t >> [.org, (x -> [[]])])]"-        , ExMetaTail ExRoot "t"-        , ExApplication (ExDispatch ExRoot (AtLabel "org")) (ArTau (AtLabel "x") (ExFormation [BiVoid AtRho]))-        , substs [[("t", MvTail [TaDispatch (AtLabel "org"), TaApplication (ArTau (AtLabel "x") (ExFormation [BiVoid AtRho]))])]]-        )-      ,-        ( "Q.x * !t => Q.x(y -> [[]]) => [(!t >> [(y -> [[]])])]"-        , ExMetaTail (ExDispatch ExRoot (AtLabel "x")) "t"-        , ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") (ExFormation [BiVoid AtRho]))-        , substs [[("t", MvTail [TaApplication (ArTau (AtLabel "y") (ExFormation [BiVoid AtRho]))])]]-        )-      ,-        ( "Q.!a * !t => Q.org.eolang(x -> [[]]) => [(!a >> org, !t >> [ .eolang, ( x -> [[ ]] ) ])]"-        , ExMetaTail (ExDispatch ExRoot (AtMeta "a")) "t"-        , ExApplication (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang")) (ArTau (AtLabel "x") (ExFormation [BiVoid AtRho]))-        , substs [[("a", MvAttribute (AtLabel "org")), ("t", MvTail [TaDispatch (AtLabel "eolang"), TaApplication (ArTau (AtLabel "x") (ExFormation [BiVoid AtRho]))])]]-        )-      ,-        ( "Q.x(y -> $ * !t1) * !t2 => Q.x(y -> $.q).p => [(!t1 >> [.q], !t2 >> [.p])]"-        , ExMetaTail (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") (ExMetaTail ExXi "t1"))) "t2"-        , ExDispatch (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") (ExDispatch ExXi (AtLabel "q")))) (AtLabel "p")-        , substs [[("t1", MvTail [TaDispatch (AtLabel "q")]), ("t2", MvTail [TaDispatch (AtLabel "p")])]]         )       ,         ( "[[!B1, !a ↦ !e1, !B2]](!a ↦ !e2) => ⟦ t ↦ ξ.k, x ↦ ξ.t, k ↦ ∅ ⟧(x ↦ ξ) => [(!B1 >> [[ t -> $.k ]], !a >> x, !B2 >> [[ k -> ? ]], !e1 >> $.t, !e2 >> $)]"

@@ -61,8 +61,6 @@       , ("[[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")]))-      , ("Q * !t", Just (ExMetaTail ExRoot "t"))-      , ("[[]](x -> $) * !t1", Just (ExMetaTail (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtLabel "x") ExXi)) "t1"))       , ("[[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]))@@ -479,15 +477,6 @@       , ("𝑛", Just (ExMeta "n"))       , ("𝑛1", Just (ExMeta "n1"))       , ("𝑛.x", Just (ExDispatch (ExMeta "n") (AtLabel "x")))-      ]--  describe "parse meta tails" $-    test-      parseExpression-      [ ("Q * !t", Just (ExMetaTail ExRoot "t"))-      , ("Q.x * !t", Just (ExMetaTail (ExDispatch ExRoot (AtLabel "x")) "t"))-      , ("[[]].y * !t0", Just (ExMetaTail (ExDispatch (ExFormation [BiVoid AtRho]) (AtLabel "y")) "t0"))-      , ("Q * !t * !t2", Nothing)       ]    describe "parse whitespace handling" $

@@ -54,7 +54,6 @@         , "[[]]( Q )"         )       , ("meta expr", ExMeta "e", "!e")-      , ("meta tail", ExMetaTail ExRoot "t", "Q * !t")       , ("meta binding", ExFormation [BiMeta "B"], "[[ !B ]]")       , ("meta lambda", ExFormation [BiLambda (FnMeta "F")], "[[ L> !F ]]")       , ("meta attr tau", ExFormation [BiTau (AtMeta "a") ExXi], "[[ !a -> $ ]]")