phino 0.0.0.73 → 0.0.0.74

raw patch · 23 files changed

+237/−311 lines, 23 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +34/−38
• phino.cabal +1/−1
• resources/alpha.yaml +1/−1
• resources/copy.yaml +4/−14
• src/Builder.hs +14/−18
• src/CST.hs +8/−15
• src/Condition.hs +7/−2
• src/Encoding.hs +2/−0
• src/Functions.hs +6/−13
• src/LaTeX.hs +2/−0
• src/Lining.hs +2/−0
• src/Matcher.hs +43/−52
• src/Printer.hs +1/−1
• src/Render.hs +2/−1
• src/Rewriter.hs +2/−3
• src/Rule.hs +26/−19
• src/Sugar.hs +4/−0
• src/Yaml.hs +6/−4
• test/BuilderSpec.hs +14/−16
• test/CLISpec.hs +9/−9
• test/ConditionSpec.hs +3/−2
• test/MatcherSpec.hs +24/−102
• test/PrinterSpec.hs +22/−0

@@ -34,7 +34,7 @@  ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.0.72+cabal install --overwrite-policy=always phino-0.0.0.73 phino --version ``` @@ -259,7 +259,7 @@   | nf: Expression'      # returns True if given expression in normal form                          # which means that no more other normalization rules                          # can be applied-  | xi: Expression'      # special condition for Rcopy normalization rule to+  | xi-free: Expression' # special condition for Rcopy normalization rule to                          # avoid infinite recursion while the condition checking                          # returns True if there's no ξ outside of the formation                          # in given expression.@@ -297,10 +297,6 @@ * `contextualize` - function of two arguments, that rewrites given expression   depending on provided context according to the contextualization   [rules](assets/contextualize.jpg)-* `scope` - resolves the scope for given expression. Works only with meta-  expressions denotes as `𝑒` or `!e`. The scope is nearest outer formation,-  if it's present. In all other cases the default scope is used, which is-  anonymous formation `⟦ ρ ↦ ∅ ⟧`. * `random-tau` - creates attribute with random unique name. Accepts bindings,   and attributes. Ensures that created attribute is not present in list of   provided attributes and does not exist as attribute in provided bindings.@@ -392,55 +388,55 @@ === parse/phi ===   warmup:     3 iterations   batches:    10 x 1-  total:      1281818.631 μs-  avg:        128181.863 μs-  min:        115976.108 μs-  max:        157716.092 μs-  std dev:    17330.936 μs+  total:      1309885.482 μs+  avg:        130988.548 μs+  min:        119182.611 μs+  max:        164424.034 μs+  std dev:    17120.368 μs === parse/xmir ===   warmup:     3 iterations   batches:    10 x 1-  total:      7703218.666 μs-  avg:        770321.867 μs-  min:        708375.007 μs-  max:        835194.999 μs-  std dev:    41016.808 μs+  total:      8166516.875 μs+  avg:        816651.687 μs+  min:        746631.521 μs+  max:        905684.717 μs+  std dev:    58484.723 μs === rewrite/normalize ===   warmup:     3 iterations   batches:    10 x 1-  total:      546667.979 μs-  avg:        54666.798 μs-  min:        47131.404 μs-  max:        61636.208 μs-  std dev:    4936.214 μs+  total:      1020794.192 μs+  avg:        102079.419 μs+  min:        98049.050 μs+  max:        109067.886 μs+  std dev:    2847.343 μs === print/sweet/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      4661151.196 μs-  avg:        466115.120 μs-  min:        458816.744 μs-  max:        478741.573 μs-  std dev:    6479.319 μs+  total:      5308178.500 μs+  avg:        530817.850 μs+  min:        500095.243 μs+  max:        590475.507 μs+  std dev:    29328.246 μs === print/sweet/flat ===   warmup:     3 iterations   batches:    10 x 1-  total:      4649931.918 μs-  avg:        464993.192 μs-  min:        426197.450 μs-  max:        489664.247 μs-  std dev:    25327.503 μs+  total:      5104935.589 μs+  avg:        510493.559 μs+  min:        449111.602 μs+  max:        555034.745 μs+  std dev:    36795.722 μs === print/salty/multiline ===   warmup:     3 iterations   batches:    10 x 1-  total:      14136736.780 μs-  avg:        1413673.678 μs-  min:        1382452.302 μs-  max:        1433158.708 μs-  std dev:    16632.911 μs+  total:      15066270.227 μs+  avg:        1506627.023 μs+  min:        1427131.813 μs+  max:        1580723.339 μs+  std dev:    45705.458 μs ```  The results were calculated in [this GHA job][benchmark-gha]-on 2026-06-02 at 03:47,+on 2026-06-03 at 13:35, on Linux with 4 CPUs.  <!-- benchmark_end -->@@ -476,4 +472,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/26796987208+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/26888116250

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

@@ -7,4 +7,4 @@ when:   eq:     - index: 𝜏2-    - length: 𝐵1+    - domain: 𝐵1

@@ -2,19 +2,9 @@ # SPDX-License-Identifier: MIT --- name: copy-pattern: ⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑒1)-result: ⟦ 𝐵1, 𝜏 ↦ 𝑒3, 𝐵2 ⟧+pattern: ⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑒)+result: ⟦ 𝐵1, 𝜏 ↦ 𝑒, 𝐵2 ⟧ when:   and:-    - xi: 𝑒1-    - nf: 𝑒1-where:-  - meta: 𝑒2-    function: scope-    args:-      - 𝑒1-  - meta: 𝑒3-    function: contextualize-    args:-      - 𝑒1-      - 𝑒2+    - xi-free: 𝑒+    - nf: 𝑒

@@ -79,7 +79,7 @@ buildBinding :: Binding -> Subst -> Built [Binding] buildBinding (BiTau attr expr) subst = do   attribute <- buildAttribute attr subst-  (expression, _) <- buildExpression expr subst+  expression <- buildExpression expr subst   Right [BiTau attribute expression] buildBinding (BiVoid attr) subst = do   attribute <- buildAttribute attr subst@@ -110,40 +110,36 @@   TaDispatch at -> buildExpressionWithTails (ExDispatch ex at) rest subst  -- Build meta expression with given substitution--- It returns tuple (X, Y)--- where X is built expression and Y is context of X--- If meta expression is built from MvExpression, is has--- context from original Program. It have default context otherwise-buildExpression :: Expression -> Subst -> Built (Expression, Expression)+buildExpression :: Expression -> Subst -> Built Expression buildExpression (ExDispatch ex at) subst = do-  (dispatched, scope) <- buildExpression ex subst+  dispatched <- buildExpression ex subst   at' <- buildAttribute at subst-  Right (ExDispatch dispatched at', scope)+  Right (ExDispatch dispatched at') buildExpression (ExApplication expr (BiTau battr bexpr)) subst = do-  (applied, scope) <- buildExpression expr subst+  applied <- buildExpression expr subst   bd :| _ <- nonEmpty' =<< buildBinding (BiTau battr bexpr) subst-  Right (ExApplication applied bd, scope)+  Right (ExApplication applied bd)   where     nonEmpty' :: [a] -> Built (NonEmpty a)     nonEmpty' [] = Left ""     nonEmpty' (x : xs) = Right (x :| xs) buildExpression (ExFormation bds) subst = do   bds' <- buildBindings bds subst >>= uniqueBindings-  Right (ExFormation bds', defaultScope)+  Right (ExFormation bds') buildExpression (ExMeta meta) (Subst mp) = case Map.lookup meta mp of-  Just (MvExpression expr scope) ->-    let res = Right (expr, scope)+  Just (MvExpression expr) ->+    let res = Right expr      in case expr of           ExFormation bds -> uniqueBindings bds >> res           _ -> res   _ -> Left (metaMsg meta) buildExpression (ExMetaTail expr meta) subst = do   let (Subst mp) = subst-  (expression, scope) <- buildExpression expr subst+  expression <- buildExpression expr subst   case Map.lookup meta mp of-    Just (MvTail tails) -> Right (buildExpressionWithTails expression tails subst, scope)+    Just (MvTail tails) -> Right (buildExpressionWithTails expression tails subst)     _ -> Left (metaMsg meta)-buildExpression expr _ = Right (expr, defaultScope)+buildExpression expr _ = Right expr  buildBytesThrows :: Bytes -> Subst -> IO Bytes buildBytesThrows bytes subst = case buildBytes bytes subst of@@ -160,11 +156,11 @@   Right attr' -> pure attr'   Left msg -> throwIO (CouldNotBuildAttribute attr msg) -buildExpressionThrows :: Expression -> Subst -> IO (Expression, Expression)+buildExpressionThrows :: Expression -> Subst -> IO Expression buildExpressionThrows expr subst = case buildExpression expr subst of   Right built -> pure built   Left msg -> throwIO (CouldNotBuildExpression expr msg)  -- Build a several expression from one expression and several substitutions-buildExpressionsThrows :: Expression -> [Subst] -> IO [(Expression, Expression)]+buildExpressionsThrows :: Expression -> [Subst] -> IO [Expression] buildExpressionsThrows expr = traverse (buildExpressionThrows expr)

@@ -202,6 +202,7 @@ data NUMBER   = INDEX {attr :: ATTRIBUTE}   | LENGTH {binding :: BINDING}+  | DOMAIN {binding :: BINDING}   | LITERAL {num :: Int}   deriving (Eq, Show) @@ -216,6 +217,7 @@   | CO_BELONGS {attr :: ATTRIBUTE, belongs :: BELONGING, set :: SET}   | CO_LOGIC {conditions :: [CONDITION], operator :: LOGIC_OPERATOR}   | CO_NF {expr :: EXPRESSION}+  | CO_XIFREE {expr :: EXPRESSION}   | CO_NOT {condition :: CONDITION}   | CO_COMPARE {left :: COMPARABLE, equal :: EQUAL, right :: COMPARABLE}   | CO_MATCHES {regex :: String, expr :: EXPRESSION}@@ -460,34 +462,24 @@   toCST AtLambda _ = AT_LAMBDA LAMBDA   toCST (AtMeta mt) _ = AT_META (META NO_EXCL TAU (metaTail mt)) -withoutXi :: [Y.Condition] -> [Y.Condition]-withoutXi conds = [cond | cond <- conds, not (singleXi cond)]-  where-    singleXi :: Y.Condition -> Bool-    singleXi (Y.Xi _) = True-    singleXi (Y.Not (Y.Xi _)) = True-    singleXi (Y.And [cond]) = singleXi cond-    singleXi (Y.Or [cond]) = singleXi cond-    singleXi _ = False- 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.Alpha attr)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_ATTRIBUTES [attributeToCST (AtAlpha 0), attributeToCST (AtAlpha 1), AT_REST DOTS])   toCST (Y.In attr binding) _ = CO_BELONGS (attributeToCST attr) IN (ST_BINDING (bindingsToCST [binding]))-  toCST (Y.And conds) _ = case withoutXi conds of+  toCST (Y.And conds) _ = case conds of     [] -> CO_EMPTY-    conds' -> CO_LOGIC (map toCST' (withoutXi conds')) AND-  toCST (Y.Or conds) _ = case withoutXi conds of+    _ -> CO_LOGIC (map toCST' conds) AND+  toCST (Y.Or conds) _ = case conds of     [] -> CO_EMPTY-    conds' -> CO_LOGIC (map toCST' (withoutXi conds')) OR+    _ -> CO_LOGIC (map toCST' conds) OR   toCST (Y.Alpha attr) _ = CO_BELONGS (attributeToCST attr) IN (ST_ATTRIBUTES [attributeToCST (AtAlpha 0), attributeToCST (AtAlpha 1), AT_REST DOTS])   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.Matches regex expr) _ = CO_MATCHES regex (expressionToCST expr)   toCST (Y.PartOf expr binding) _ = CO_PART_OF (expressionToCST expr) (bindingsToCST [binding])-  toCST (Y.Xi _) _ = CO_EMPTY+  toCST (Y.XiFree expr) _ = CO_XIFREE (expressionToCST expr)  instance ToCST Y.Comparable COMPARABLE where   toCST (Y.CmpAttr attr) _ = CMP_ATTR (attributeToCST attr)@@ -497,6 +489,7 @@ instance ToCST Y.Number NUMBER where   toCST (Y.Index attr) _ = INDEX (attributeToCST attr)   toCST (Y.Length binding) _ = LENGTH (bindingsToCST [binding])+  toCST (Y.Domain binding) _ = DOMAIN (bindingsToCST [binding])   toCST (Y.Literal num) _ = LITERAL num  instance ToCST Y.ExtraArgument EXTRA_ARG where

@@ -59,6 +59,11 @@         _ <- rparen         return (Y.Length bd)     , do+        _ <- symbol "domain" >> lparen+        bd <- _binding phiParser+        _ <- rparen+        return (Y.Domain bd)+    , do         sign <- optional (choice [char '-', char '+'])         unsigned <- lexeme L.decimal         return@@ -121,10 +126,10 @@         _ <- rparen         return (Y.NF expr)     , do-        _ <- symbol "xi" >> lparen+        _ <- symbol "xi-free" >> lparen         expr <- _expression phiParser         _ <- rparen-        return (Y.Xi expr)+        return (Y.XiFree expr)     , do         _ <- symbol "matches" >> lparen         ptn <- _string phiParser

@@ -81,6 +81,7 @@ instance ToASCII NUMBER where   toASCII INDEX{..} = INDEX (toASCII attr)   toASCII LENGTH{..} = LENGTH (toASCII binding)+  toASCII DOMAIN{..} = DOMAIN (toASCII binding)   toASCII literal@LITERAL{} = literal  instance ToASCII COMPARABLE where@@ -92,6 +93,7 @@   toASCII CO_BELONGS{..} = CO_BELONGS (toASCII attr) belongs (toASCII set)   toASCII CO_LOGIC{..} = CO_LOGIC (map toASCII conditions) operator   toASCII CO_NF{..} = CO_NF (toASCII expr)+  toASCII CO_XIFREE{..} = CO_XIFREE (toASCII expr)   toASCII CO_NOT{..} = CO_NOT (toASCII condition)   toASCII CO_COMPARE{..} = CO_COMPARE (toASCII left) equal (toASCII right)   toASCII CO_MATCHES{..} = CO_MATCHES regex (toASCII expr)

@@ -31,7 +31,6 @@  buildTerm' :: BuildTermFunc buildTerm' "contextualize" = _contextualize-buildTerm' "scope" = _scope buildTerm' "random-tau" = _randomTau buildTerm' "dataize" = _dataize buildTerm' "concat" = _concat@@ -62,17 +61,11 @@  _contextualize :: BuildTermMethod _contextualize [Y.ArgExpression expr, Y.ArgExpression context] subst = do-  (expr', _) <- buildExpressionThrows expr subst-  (context', _) <- buildExpressionThrows context subst+  expr' <- buildExpressionThrows expr subst+  context' <- buildExpressionThrows context subst   pure (TeExpression (contextualize expr' context')) _contextualize _ _ = throwIO (userError "Function contextualize() requires exactly 2 arguments as expression") -_scope :: BuildTermMethod-_scope [Y.ArgExpression expr] subst = do-  (_, scope) <- buildExpressionThrows expr subst-  pure (TeExpression scope)-_scope _ _ = throwIO (userError "Function scope() requires exactly 1 argument as expression")- -- Uniqueness is the engine's job: 'freshTau' draws from the document-wide -- avoid-set seeded at the start of the run, so no collision list is needed. -- The function takes no arguments and rejects any extras so rule mistakes are@@ -86,7 +79,7 @@   bts <- buildBytesThrows bytes subst   pure (TeBytes bts) _dataize [Y.ArgExpression expr] subst = do-  (expr', _) <- buildExpressionThrows expr subst+  expr' <- buildExpressionThrows expr subst   case expr' of     DataObject _ bytes -> pure (TeBytes bytes)     _ -> throwIO (userError "Only data objects and bytes are supported by 'dataize' function now")@@ -164,7 +157,7 @@  _string :: BuildTermMethod _string [Y.ArgExpression expr] subst = do-  (expr', _) <- buildExpressionThrows expr subst+  expr' <- buildExpressionThrows expr subst   str <- case expr' of     DataNumber bts -> pure (DataString (strToBts (either show show (btsToNum bts))))     DataString bts -> pure (DataString bts)@@ -184,7 +177,7 @@  _number :: BuildTermMethod _number [Y.ArgExpression expr] subst = do-  (expr', _) <- buildExpressionThrows expr subst+  expr' <- buildExpressionThrows expr subst   case expr' of     DataString bts -> do       num <- parseNumberThrows (btsToUnescapedStr bts)@@ -245,7 +238,7 @@   inBds <- buildBindingThrows inArg subst   repBds <- buildBindingThrows repArg subst   mapM_ validateRep repBds-  (sentinel, _) <- buildExpressionThrows sentExpr subst+  sentinel <- buildExpressionThrows sentExpr subst   result <- walk inBds sentinel repBds   pure (TeBindings result)   where

@@ -289,6 +289,7 @@ instance ToLaTeX NUMBER where   toLaTeX INDEX{..} = INDEX (toLaTeX attr)   toLaTeX LENGTH{..} = LENGTH (toLaTeX binding)+  toLaTeX DOMAIN{..} = DOMAIN (toLaTeX binding)   toLaTeX literal@LITERAL{} = literal  instance ToLaTeX COMPARABLE where@@ -300,6 +301,7 @@   toLaTeX CO_BELONGS{..} = CO_BELONGS (toLaTeX attr) belongs (toLaTeX set)   toLaTeX CO_LOGIC{..} = CO_LOGIC (map toLaTeX conditions) operator   toLaTeX CO_NF{..} = CO_NF (toLaTeX expr)+  toLaTeX CO_XIFREE{..} = CO_XIFREE (toLaTeX expr)   toLaTeX CO_NOT{..} = CO_NOT (toLaTeX condition)   toLaTeX CO_COMPARE{..} = CO_COMPARE (toLaTeX left) equal (toLaTeX right)   toLaTeX CO_MATCHES{..} = CO_MATCHES regex (toLaTeX expr)

@@ -64,6 +64,7 @@  instance ToSingleLine NUMBER where   toSingleLine LENGTH{..} = LENGTH (toSingleLine binding)+  toSingleLine DOMAIN{..} = DOMAIN (toSingleLine binding)   toSingleLine num = num  instance ToSingleLine COMPARABLE where@@ -75,6 +76,7 @@   toSingleLine CO_BELONGS{..} = CO_BELONGS attr belongs (toSingleLine set)   toSingleLine CO_LOGIC{..} = CO_LOGIC (map toSingleLine conditions) operator   toSingleLine CO_NF{..} = CO_NF (toSingleLine expr)+  toSingleLine CO_XIFREE{..} = CO_XIFREE (toSingleLine expr)   toSingleLine CO_NOT{..} = CO_NOT (toSingleLine condition)   toSingleLine CO_COMPARE{..} = CO_COMPARE (toSingleLine left) equal (toSingleLine right)   toSingleLine CO_MATCHES{..} = CO_MATCHES regex (toSingleLine expr)

@@ -20,7 +20,7 @@   | MvBytes Bytes -- !b   | MvBindings [Binding] -- !B   | MvFunction Text -- !F-  | MvExpression Expression Expression -- !e, the second expression is scope, which is closest formation+  | MvExpression Expression -- !e   | MvTail [Tail] -- !t   deriving (Eq, Show) @@ -44,9 +44,6 @@ substSingle :: Text -> MetaValue -> Subst substSingle key value = Subst (Map.singleton key value) -defaultScope :: Expression-defaultScope = ExFormation [BiVoid AtRho]- -- Combine two substitutions into a single one -- Fails if values by the same keys are not equal combine :: Subst -> Subst -> Maybe Subst@@ -54,12 +51,6 @@   where     combine' :: [(Text, MetaValue)] -> Map Text MetaValue -> Maybe Subst     combine' [] acc = Just (Subst acc)-    combine' ((key, MvExpression tgt scope) : rest) acc = case Map.lookup key acc of-      Just (MvExpression expr' _)-        | expr' == tgt -> combine' rest acc-        | otherwise -> Nothing-      Just _ -> Nothing-      Nothing -> combine' rest (Map.insert key (MvExpression tgt scope) acc)     combine' ((key, value) : rest) acc = case Map.lookup key acc of       Just found         | found == value -> combine' rest acc@@ -75,44 +66,44 @@   | ptn == tgt = [substEmpty]   | otherwise = [] -matchBinding :: Binding -> Binding -> Expression -> [Subst]-matchBinding (BiVoid pattr) (BiVoid tattr) _ = matchAttribute pattr tattr-matchBinding (BiDelta (BtMeta meta)) (BiDelta tdata) _ = [substSingle meta (MvBytes tdata)]-matchBinding (BiDelta pdata) (BiDelta tdata) _+matchBinding :: Binding -> Binding -> [Subst]+matchBinding (BiVoid pattr) (BiVoid tattr) = matchAttribute pattr tattr+matchBinding (BiDelta (BtMeta meta)) (BiDelta tdata) = [substSingle meta (MvBytes tdata)]+matchBinding (BiDelta pdata) (BiDelta tdata)   | pdata == tdata = [substEmpty]   | otherwise = []-matchBinding (BiLambda pFunc) (BiLambda tFunc) _+matchBinding (BiLambda pFunc) (BiLambda tFunc)   | pFunc == tFunc = [substEmpty]   | otherwise = []-matchBinding (BiMetaLambda meta) (BiLambda tFunc) _ = [substSingle meta (MvFunction tFunc)]-matchBinding (BiTau pattr pexp) (BiTau tattr texp) scope = combineMany (matchAttribute pattr tattr) (matchExpression' pexp texp scope)-matchBinding _ _ _ = []+matchBinding (BiMetaLambda meta) (BiLambda tFunc) = [substSingle meta (MvFunction tFunc)]+matchBinding (BiTau pattr pexp) (BiTau tattr texp) = combineMany (matchAttribute pattr tattr) (matchExpression' pexp texp)+matchBinding _ _ = []  -- Match bindings with ordering-matchBindings :: [Binding] -> [Binding] -> Expression -> [Subst]-matchBindings [] [] _ = [substEmpty]-matchBindings [] _ _ = []-matchBindings ((BiMeta name) : pbs) tbs scope =+matchBindings :: [Binding] -> [Binding] -> [Subst]+matchBindings [] [] = [substEmpty]+matchBindings [] _ = []+matchBindings ((BiMeta name) : pbs) tbs =   let splits = [splitAt idx tbs | idx <- [0 .. length tbs]]    in catMaybes         [ combine (substSingle name (MvBindings before)) subst         | (before, after) <- splits-        , subst <- matchBindings pbs after scope+        , subst <- matchBindings pbs after         ]-matchBindings (pb : pbs) (tb : tbs) scope = combineMany (matchBinding pb tb scope) (matchBindings pbs tbs scope)-matchBindings _ _ _ = []+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 -> Expression -> ([Subst], [Tail])-tailExpressions ptn tgt scope = case tailExpressionsReversed ptn tgt of+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' scope of+    tailExpressionsReversed ptn' tgt' = case matchExpression' ptn' tgt' of       [] -> case tgt' of         ExDispatch expr attr -> do           (substs, tails) <- tailExpressionsReversed ptn' expr@@ -130,43 +121,43 @@         _ -> Just ([], [])       substs -> Just (substs, []) -matchExpression' :: Expression -> Expression -> Expression -> [Subst]-matchExpression' (ExMeta meta) tgt scope = [substSingle meta (MvExpression tgt scope)]-matchExpression' ExThis ExThis _ = [substEmpty]-matchExpression' ExGlobal ExGlobal _ = [substEmpty]-matchExpression' ExTermination ExTermination _ = [substEmpty]-matchExpression' (ExFormation pbs) (ExFormation tbs) _ = matchBindings pbs tbs (ExFormation tbs)-matchExpression' (ExDispatch pexp pattr) (ExDispatch texp tattr) scope = combineMany (matchAttribute pattr tattr) (matchExpression' pexp texp scope)-matchExpression' (ExApplication pexp pbd) (ExApplication texp tbd) scope = combineMany (matchExpression' pexp texp scope) (matchBinding pbd tbd scope)-matchExpression' (ExMetaTail expr meta) tgt scope = case tailExpressions expr tgt scope of+matchExpression' :: Expression -> Expression -> [Subst]+matchExpression' (ExMeta meta) tgt = [substSingle meta (MvExpression tgt)]+matchExpression' ExThis ExThis = [substEmpty]+matchExpression' ExGlobal ExGlobal = [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 pbd) (ExApplication texp tbd) = combineMany (matchExpression' pexp texp) (matchBinding pbd tbd)+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') scope-  | prefix == prefix' && idx == idx' = matchExpression' expr expr' scope+matchExpression' (ExPhiAgain prefix idx expr) (ExPhiAgain prefix' idx' expr')+  | prefix == prefix' && idx == idx' = matchExpression' expr expr'   | otherwise = []-matchExpression' (ExPhiMeet prefix idx expr) (ExPhiMeet prefix' idx' expr') scope-  | prefix == prefix' && idx == idx' = matchExpression' expr expr' scope+matchExpression' (ExPhiMeet prefix idx expr) (ExPhiMeet prefix' idx' expr')+  | prefix == prefix' && idx == idx' = matchExpression' expr expr'   | otherwise = []-matchExpression' _ _ _ = []+matchExpression' _ _ = []  -- Deep match pattern to expression inside binding-matchBindingExpression :: Binding -> Expression -> Expression -> [Subst]-matchBindingExpression (BiTau _ expr) ptn scope = matchExpressionDeep ptn expr scope-matchBindingExpression _ _ _ = []+matchBindingExpression :: Binding -> Expression -> [Subst]+matchBindingExpression (BiTau _ expr) ptn = matchExpressionDeep ptn expr+matchBindingExpression _ _ = []  -- Match expression with deep nested expression(s) matching-matchExpressionDeep :: Expression -> Expression -> Expression -> [Subst]-matchExpressionDeep ptn tgt scope =-  let matched = matchExpression' ptn tgt scope+matchExpressionDeep :: Expression -> Expression -> [Subst]+matchExpressionDeep ptn tgt =+  let matched = matchExpression' ptn tgt       deep = case tgt of-        ExFormation bds -> concatMap (\bd -> matchBindingExpression bd ptn tgt) bds-        ExDispatch expr _ -> matchExpressionDeep ptn expr scope-        ExApplication expr tau -> matchExpressionDeep ptn expr scope ++ matchBindingExpression tau ptn scope+        ExFormation bds -> concatMap (`matchBindingExpression` ptn) bds+        ExDispatch expr _ -> matchExpressionDeep ptn expr+        ExApplication expr tau -> matchExpressionDeep ptn expr ++ matchBindingExpression tau ptn         _ -> []    in matched ++ deep  matchExpression :: Expression -> Expression -> [Subst]-matchExpression ptn tgt = matchExpressionDeep ptn tgt defaultScope+matchExpression = matchExpressionDeep  matchProgram :: Expression -> Program -> [Subst] matchProgram ptn (Program expr) = matchExpression ptn expr

@@ -86,7 +86,7 @@  printMetaValue :: MetaValue -> PrintConfig -> String printMetaValue (MvAttribute att) (_, encoding, _, _) = printAttribute' att encoding-printMetaValue (MvExpression ex _) config = printExpression' ex config+printMetaValue (MvExpression ex) config = printExpression' ex config printMetaValue (MvBytes bts) _ = printBytes bts printMetaValue (MvBindings bds) config = printExpression' (ExFormation bds) config printMetaValue (MvFunction fun) _ = T.unpack fun

@@ -223,6 +223,7 @@ instance Render NUMBER where   render INDEX{..} = "\\indexof{ " <> render attr <> " }"   render LENGTH{..} = "\\vert " <> render binding <> " \\vert"+  render DOMAIN{..} = "\\vert \\overline{ " <> render binding <> " } \\vert"   render LITERAL{..} = T.pack (show num)  instance Render COMPARABLE where@@ -244,6 +245,7 @@       renderWrapped cond@CO_LOGIC{} = "( " <> render cond <> " )"       renderWrapped cond = render cond   render CO_NF{..} = "\\isnormal{ " <> render expr <> " }"+  render CO_XIFREE{..} = "\\xifree{ " <> render expr <> " }"   render CO_NOT{..} = renderFunc "not" condition   render CO_COMPARE{..} = render left <> " " <> render equal <> " " <> render right   render CO_MATCHES{..} = "matches( " <> T.pack regex <> ", " <> render expr <> " )"@@ -261,5 +263,4 @@  instance Render EXTRA where   render EXTRA{func = "contextualize", args = arg : rest, ..} = "$ " <> render meta <> " \\coloneqq \\ctx{ " <> render arg <> " }{ " <> T.intercalate ", " (map render rest) <> " } $"-  render EXTRA{func = "scope", args = arg : _, ..} = "$ " <> render meta <> " \\coloneqq \\scopeof{ " <> render arg <> " } $"   render EXTRA{..} = "$ " <> render meta <> " \\coloneqq " <> T.pack func <> "( " <> T.intercalate ", " (map render args) <> " ) $"

@@ -87,9 +87,8 @@ buildAndReplace' (expr, ptn, res, substs) func = do   ptns <- buildExpressionsThrows ptn substs   repls <- buildExpressionsThrows res substs-  let ptns' = map fst ptns-      repls' = map (\ex _ -> fst ex) repls-  pure (func (expr, ptns', repls'))+  let repls' = map const repls+  pure (func (expr, ptns, repls'))  -- If pattern and replacement are appropriate for fast replacing - does it. -- Pattern and replacement expressions can be used in fast replacing only if

@@ -129,8 +129,15 @@     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 (BiMetaLambda _) = False+    notAsset _ = True _eq (Y.CmpAttr left) (Y.CmpAttr right) subst _ = pure [subst | compareAttrs left right subst]   where     compareAttrs :: Attribute -> Attribute -> Subst -> Bool@@ -148,40 +155,40 @@   where     compareExprs :: Expression -> Expression -> Subst -> Bool     compareExprs (ExMeta left) (ExMeta right) (Subst mp) = case (M.lookup left mp, M.lookup right mp) of-      (Just (MvExpression left' _), Just (MvExpression right' _)) -> compareExprs left' right' (Subst mp)+      (Just (MvExpression left'), Just (MvExpression right')) -> compareExprs left' right' (Subst mp)       _ -> False     compareExprs expr (ExMeta meta) (Subst mp) = case M.lookup meta mp of-      Just (MvExpression found _) -> expr == found+      Just (MvExpression found) -> expr == found       _ -> False     compareExprs (ExMeta meta) expr (Subst mp) = case M.lookup meta mp of-      Just (MvExpression found _) -> expr == found+      Just (MvExpression found) -> expr == found       _ -> False     compareExprs left right _ = left == right _eq _ _ _ _ = 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+  Just (MvExpression expr) -> _nf expr (Subst mp) ctx   _ -> pure [] _nf expr subst ctx = pure [subst | isNF expr ctx] -_xi :: Expression -> Subst -> RuleContext -> IO [Subst]-_xi (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of-  Just (MvExpression expr _) -> _xi expr (Subst mp) ctx+_xiFree :: Expression -> Subst -> RuleContext -> IO [Subst]+_xiFree (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of+  Just (MvExpression expr) -> _xiFree expr (Subst mp) ctx   _ -> pure []-_xi (ExFormation _) subst _ = pure [subst]-_xi ExThis _ _ = pure []-_xi ExGlobal subst _ = pure [subst]-_xi (ExApplication expr (BiTau _ texpr)) subst ctx = do-  onExpr <- _xi expr subst ctx-  onTau <- _xi texpr subst ctx+_xiFree (ExFormation _) subst _ = pure [subst]+_xiFree ExThis _ _ = pure []+_xiFree ExGlobal subst _ = pure [subst]+_xiFree (ExApplication expr (BiTau _ texpr)) subst ctx = do+  onExpr <- _xiFree expr subst ctx+  onTau <- _xiFree texpr subst ctx   pure [subst | not (null onExpr) && not (null onTau)]-_xi (ExDispatch expr _) subst ctx = _xi expr subst ctx-_xi _ _ _ = pure []+_xiFree (ExDispatch expr _) subst ctx = _xiFree expr subst ctx+_xiFree _ _ _ = pure []  _matches :: String -> Expression -> Subst -> RuleContext -> IO [Subst] _matches pat (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of-  Just (MvExpression expr _) -> _matches pat expr (Subst mp) ctx+  Just (MvExpression expr) -> _matches pat expr (Subst mp) ctx   _ -> pure [] _matches pat expr subst ctx = do   (TeBytes tgt) <- _buildTerm ctx "dataize" [Y.ArgExpression expr] subst@@ -190,7 +197,7 @@  _partOf :: Expression -> Binding -> Subst -> RuleContext -> IO [Subst] _partOf exp bd subst _ = do-  (exp', _) <- buildExpressionThrows exp subst+  exp' <- buildExpressionThrows exp subst   bds <- buildBindingThrows bd subst   pure [subst | partOf exp' bds]   where@@ -208,7 +215,7 @@ meetCondition' (Y.Alpha attr) = _alpha attr meetCondition' (Y.Eq left right) = _eq left right meetCondition' (Y.NF expr) = _nf expr-meetCondition' (Y.Xi expr) = _xi expr+meetCondition' (Y.XiFree expr) = _xiFree expr meetCondition' (Y.Matches pat expr) = _matches pat expr meetCondition' (Y.PartOf expr bd) = _partOf expr bd @@ -255,7 +262,7 @@                   meta <- case term of                     TeExpression expr -> do                       logDebug (printf "Function %s() returned expression:\n%s" func (printExpression expr))-                      pure (MvExpression expr defaultScope)+                      pure (MvExpression expr)                     TeAttribute attr -> do                       logDebug (printf "Function %s() returned attribute: %s" func (printAttribute attr))                       pure (MvAttribute attr)

@@ -25,12 +25,14 @@ bdWithVoidRho BI_EMPTY{..} = BI_PAIR voidRho (BDS_EMPTY tab) tab bdWithVoidRho bd@BI_PAIR{pair = PA_VOID{attr = AT_RHO _}} = bd bdWithVoidRho bd@BI_PAIR{pair = PA_TAU{attr = AT_RHO _}} = bd+bdWithVoidRho bd@BI_PAIR{pair = PA_FORMATION{attr = AT_RHO _}} = bd bdWithVoidRho BI_PAIR{..} = BI_PAIR pair (bdsWithVoidRho bindings) tab   where     bdsWithVoidRho :: BINDINGS -> BINDINGS     bdsWithVoidRho BDS_EMPTY{..} = BDS_PAIR EOL tab voidRho (BDS_EMPTY tab)     bdsWithVoidRho bds@BDS_PAIR{pair = PA_VOID{attr = AT_RHO _}} = bds     bdsWithVoidRho bds@BDS_PAIR{pair = PA_TAU{attr = AT_RHO _}} = bds+    bdsWithVoidRho bds@BDS_PAIR{pair = PA_FORMATION{attr = AT_RHO _}} = bds     bdsWithVoidRho BDS_PAIR{..} = BDS_PAIR eol tab pair (bdsWithVoidRho bindings)     bdsWithVoidRho bds@BDS_META{} = bds bdWithVoidRho bd@BI_META{} = bd@@ -176,6 +178,7 @@  instance ToSalty NUMBER where   toSalty LENGTH{..} = LENGTH (toSalty binding)+  toSalty DOMAIN{..} = DOMAIN (toSalty binding)   toSalty num = num  instance ToSalty COMPARABLE where@@ -187,6 +190,7 @@   toSalty CO_BELONGS{..} = CO_BELONGS attr belongs (toSalty set)   toSalty CO_LOGIC{..} = CO_LOGIC (map toSalty conditions) operator   toSalty CO_NF{..} = CO_NF (toSalty expr)+  toSalty CO_XIFREE{..} = CO_XIFREE (toSalty expr)   toSalty CO_NOT{..} = CO_NOT (toSalty condition)   toSalty CO_COMPARE{..} = CO_COMPARE (toSalty left) equal (toSalty right)   toSalty CO_MATCHES{..} = CO_MATCHES regex (toSalty expr)

@@ -54,10 +54,11 @@ instance FromJSON Number where   parseJSON v = case v of     Object o -> do-      validateYamlObject o ["index", "length"]+      validateYamlObject o ["index", "length", "domain"]       asum         [ Index <$> o .: "index"         , Length <$> o .: "length"+        , Domain <$> o .: "domain"         ]     Number num -> pure (Literal (round num))     _ ->@@ -76,14 +77,14 @@     withObject       "Condition"       ( \v -> do-          validateYamlObject v ["and", "or", "not", "alpha", "nf", "xi", "eq", "in", "matches", "part-of"]+          validateYamlObject v ["and", "or", "not", "alpha", "nf", "xi-free", "eq", "in", "matches", "part-of"]           asum             [ And <$> v .: "and"             , Or <$> v .: "or"             , Not <$> v .: "not"             , Alpha <$> v .: "alpha"             , NF <$> v .: "nf"-            , Xi <$> v .: "xi"+            , XiFree <$> v .: "xi-free"             , do                 vals <- v .: "eq"                 case vals of@@ -142,6 +143,7 @@ data Number   = Index Attribute   | Length Binding+  | Domain Binding   | Literal Int   deriving (Eq, Generic, Show) @@ -159,7 +161,7 @@   | Alpha Attribute   | Eq Comparable Comparable   | NF Expression-  | Xi Expression+  | XiFree Expression   | Matches String Expression   | PartOf Expression Binding   deriving (Eq, Generic, Show)

@@ -14,7 +14,7 @@ import Matcher import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, anyException, describe, it, shouldBe, shouldSatisfy, shouldThrow) -test :: (Show a, Eq a) => (a -> Subst -> Either String (a, a)) -> [(String, a, [(T.Text, MetaValue)], Either String (a, a))] -> SpecWith (Arg Expectation)+test :: (Show a, Eq a) => (a -> Subst -> Either String a) -> [(String, a, [(T.Text, MetaValue)], Either String a)] -> SpecWith (Arg Expectation) test function useCases =   forM_ useCases $ \(desc, expr, mp, res) ->     it desc $ function expr (Subst (Map.fromList mp)) `shouldBe` res@@ -28,13 +28,13 @@         ( "Q.!a => (!a >> x) => Q.x"         , ExDispatch ExGlobal (AtMeta "a")         , [("a", MvAttribute (AtLabel "x"))]-        , Right (ExDispatch ExGlobal (AtLabel "x"), defaultScope)+        , Right (ExDispatch ExGlobal (AtLabel "x"))         )       ,         ( "Q.c(!a -> !e) => (!a >> x, !e >> $.y.z) => Q.c(x -> $.y.z)"         , ExApplication (ExDispatch ExGlobal (AtLabel "c")) (BiTau (AtMeta "a") (ExMeta "e"))-        , [("a", MvAttribute (AtLabel "x")), ("e", MvExpression (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z")) defaultScope)]-        , Right (ExApplication (ExDispatch ExGlobal (AtLabel "c")) (BiTau (AtLabel "x") (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z"))), defaultScope)+        , [("a", MvAttribute (AtLabel "x")), ("e", MvExpression (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z")))]+        , Right (ExApplication (ExDispatch ExGlobal (AtLabel "c")) (BiTau (AtLabel "x") (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z"))))         )       ,         ( "[[!a -> $.x, !B]] => (!a >> y, !B >> [[b -> ?, L> Func]]) => [[y -> $.x, b -> ?, L> Func]]"@@ -46,14 +46,13 @@                 , BiVoid (AtLabel "b")                 , BiLambda "Func"                 ]-            , defaultScope             )         )       ,         ( "Q * !t => (!t >> [.a, .b, (~1 -> $.x)]) => Q.a.b(~1 -> $.x)"         , ExMetaTail ExGlobal "t"         , [("t", MvTail [TaDispatch (AtLabel "a"), TaDispatch (AtLabel "b"), TaApplication (BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "x")))])]-        , Right (ExApplication (ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b")) (BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "x"))), defaultScope)+        , Right (ExApplication (ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b")) (BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "x"))))         )       ,         ( "Q.!a => () => X"@@ -65,13 +64,13 @@         ( "!e0(!a1 -> !e1, !a2 => !e2) => (!e0 >> [[]], !a1 >> x, !e1 >> Q, !a2 >> y, !e2 >> $) => [[]](x -> Q, y -> $)"         , ExApplication (ExApplication (ExMeta "e0") (BiTau (AtMeta "a1") (ExMeta "e1"))) (BiTau (AtMeta "a2") (ExMeta "e2"))         ,-          [ ("e0", MvExpression (ExFormation []) defaultScope)+          [ ("e0", MvExpression (ExFormation []))           , ("a1", MvAttribute (AtLabel "x"))-          , ("e1", MvExpression ExGlobal defaultScope)+          , ("e1", MvExpression ExGlobal)           , ("a2", MvAttribute (AtLabel "y"))-          , ("e2", MvExpression ExThis defaultScope)+          , ("e2", MvExpression ExThis)           ]-        , Right (ExApplication (ExApplication (ExFormation []) (BiTau (AtLabel "x") ExGlobal)) (BiTau (AtLabel "y") ExThis), defaultScope)+        , Right (ExApplication (ExApplication (ExFormation []) (BiTau (AtLabel "x") ExGlobal)) (BiTau (AtLabel "y") ExThis))         )       ,         ( "⟦!a ↦ ∅, !B⟧.!a => (!a >> t, !B >> ⟦ x ↦ ξ.t ⟧ ) => ⟦ t ↦ ∅, x ↦ ξ.t ⟧.t"@@ -88,7 +87,6 @@                     ]                 )                 (AtLabel "t")-            , defaultScope             )         )       ]@@ -98,18 +96,18 @@       built <-         buildExpressionsThrows           (ExMeta "e")-          [ substSingle "e" (MvExpression (ExDispatch ExGlobal (AtLabel "x")) defaultScope)-          , substSingle "e" (MvExpression (ExDispatch ExThis (AtLabel "y")) defaultScope)+          [ substSingle "e" (MvExpression (ExDispatch ExGlobal (AtLabel "x")))+          , substSingle "e" (MvExpression (ExDispatch ExThis (AtLabel "y")))           ]-      built `shouldBe` [(ExDispatch ExGlobal (AtLabel "x"), defaultScope), (ExDispatch ExThis (AtLabel "y"), defaultScope)]+      built `shouldBe` [ExDispatch ExGlobal (AtLabel "x"), ExDispatch ExThis (AtLabel "y")]     it "!e => [(!e1 >> Q.x)] => X" $       buildExpressionsThrows         (ExMeta "e")-        [substSingle "e1" (MvExpression (ExDispatch ExGlobal (AtLabel "x")) defaultScope)]+        [substSingle "e1" (MvExpression (ExDispatch ExGlobal (AtLabel "x")))]         `shouldThrow` anyException    describe "build with duplicate attributes in bindings" $ do     it "build binding with duplicates" $       buildBinding (BiMeta "B") (substSingle "B" (MvBindings [BiVoid AtRho, BiVoid AtRho])) `shouldSatisfy` isLeft     it "build formation with duplicates" $-      buildExpression (ExMeta "e") (substSingle "e" (MvExpression (ExFormation [BiVoid AtRho, BiVoid AtRho]) ExThis)) `shouldSatisfy` isLeft+      buildExpression (ExMeta "e") (substSingle "e" (MvExpression (ExFormation [BiVoid AtRho, BiVoid AtRho]))) `shouldSatisfy` isLeft

@@ -921,10 +921,10 @@         [ unlines             [ "\\begin{tabular}{rl}"             , "\\trrule{copy}"-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e_1 ) }"-            , "  { [[ B_1, \\tau -> e_3, B_2 ]] }"-            , "  { if $ \\isnormal{ e_1 } $ }"-            , "  { where $ e_2 \\coloneqq \\scopeof{ e_1 } $ and $ e_3 \\coloneqq \\ctx{ e_1 }{ e_2 } $ }"+            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }"+            , "  { [[ B_1, \\tau -> e, B_2 ]] }"+            , "  { if $ \\xifree{ e } \\;\\text{and}\\; \\isnormal{ e } $ }"+            , "  { }"             , "\\end{tabular}"             ]         ]@@ -942,13 +942,13 @@             , "\\trrule{alpha}"             , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_2 -> e ) }"             , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> e ) }"-            , "  { if $ \\indexof{ \\tau_2 } = \\vert B_1 \\vert $ }"+            , "  { if $ \\indexof{ \\tau_2 } = \\vert \\overline{ B_1 } \\vert $ }"             , "  { }"             , "\\trrule{copy}"-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e_1 ) }"-            , "  { [[ B_1, \\tau -> e_3, B_2 ]] }"-            , "  { if $ \\isnormal{ e_1 } $ }"-            , "  { where $ e_2 \\coloneqq \\scopeof{ e_1 } $ and $ e_3 \\coloneqq \\ctx{ e_1 }{ e_2 } $ }"+            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }"+            , "  { [[ B_1, \\tau -> e, B_2 ]] }"+            , "  { if $ \\xifree{ e } \\;\\text{and}\\; \\isnormal{ e } $ }"+            , "  { }"             , "\\trrule{dc}"             , "  { T ( \\tau -> e ) }"             , "  { T }"

@@ -23,7 +23,7 @@       , "or(eq(index(a),1),eq(length(!B),-2),eq(!e1,!e2),eq(!a1,x),eq(Q.org.eolang,[[ x -> 2 ]]))"       , "and(alpha(q),eq(-5,21))"       , "nf([[ x -> !e ]].x)"-      , "xi(!e1)"+      , "xi-free(!e1)"       , "matches(\"hello(\\\"\\u0000)\", !e)"       , "part-of ( [[ x -> 1 ]] , !B ) "       , "and(not(alpha(!a)),eq(!a,x))"@@ -37,8 +37,9 @@       , ("alpha(y)", Y.Alpha (AtLabel "y"))       , ("eq(1,-2)", Y.Eq (Y.CmpNum (Y.Literal 1)) (Y.CmpNum (Y.Literal (-2))))       , ("eq(index(z),length(!B1))", Y.Eq (Y.CmpNum (Y.Index (AtLabel "z"))) (Y.CmpNum (Y.Length (BiMeta "B1"))))+      , ("eq(index(z),domain(!B1))", Y.Eq (Y.CmpNum (Y.Index (AtLabel "z"))) (Y.CmpNum (Y.Domain (BiMeta "B1"))))       , ("eq(!a1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "a1")) (Y.CmpExpr (ExMeta "e2")))-      , ("or(xi(!e1), nf(Q.x))", Y.Or [Y.Xi (ExMeta "e1"), Y.NF (ExDispatch ExGlobal (AtLabel "x"))])+      , ("or(xi-free(!e1), nf(Q.x))", Y.Or [Y.XiFree (ExMeta "e1"), Y.NF (ExDispatch ExGlobal (AtLabel "x"))])       , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")])       ]       (\(expr, res) -> it expr (parseCondition expr `shouldBe` Right res))

@@ -23,12 +23,12 @@     (combine first second)  test ::-  (a -> a -> b -> [Subst]) ->-  [(String, a, a, b, [Subst])] ->+  (a -> a -> [Subst]) ->+  [(String, a, a, [Subst])] ->   SpecWith (Arg Expectation) test function useCases =-  forM_ useCases $ \(desc, ptn, tgt, scope, expected) ->-    it desc $ function ptn tgt scope `shouldBe` expected+  forM_ useCases $ \(desc, ptn, tgt, expected) ->+    it desc $ function ptn tgt `shouldBe` expected  spec :: Spec spec = do@@ -39,7 +39,6 @@         ( "Q => [[ @ -> Q, ^ -> Q ]] => [(), ()]"         , ExGlobal         , ExFormation [BiTau AtPhi ExGlobal, BiTau AtRho ExGlobal]-        , defaultScope         , substs [[], []]         )       ,@@ -50,7 +49,6 @@             , BiTau AtRho (ExFormation [BiTau (AtLabel "a") (ExDispatch ExGlobal (AtLabel "w"))])             , BiTau AtPhi (ExDispatch ExGlobal (AtLabel "y"))             ]-        , defaultScope         , substs [[("a", MvAttribute (AtLabel "y"))], [("a", MvAttribute (AtLabel "w"))], [("a", MvAttribute (AtLabel "y"))]]         )       ,@@ -60,27 +58,24 @@             [ BiTau (AtLabel "f") (ExFormation [BiTau (AtLabel "x") (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "x"))])             , BiTau (AtLabel "t") (ExFormation [BiTau (AtLabel "y") (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "y"))])             ]-        , defaultScope         , substs [[("a", MvAttribute (AtLabel "x"))], [("a", MvAttribute (AtLabel "y"))]]         )       ,         ( "!e => [[x -> Q]] => [(!e >> [[x -> Q]] ), (!e >> Q)]"         , ExMeta "e"         , ExFormation [BiTau (AtLabel "x") ExGlobal]-        , defaultScope         , substs-            [ [("e", MvExpression (ExFormation [BiTau (AtLabel "x") ExGlobal]) defaultScope)]-            , [("e", MvExpression ExGlobal (ExFormation [BiTau (AtLabel "x") ExGlobal]))]+            [ [("e", MvExpression (ExFormation [BiTau (AtLabel "x") ExGlobal]))]+            , [("e", MvExpression ExGlobal)]             ]         )       ,         ( "!e.!a => Q.org.eolang => [(!e >> Q.org, !a >> eolang), (!e >> Q, !a >> org)]"         , ExDispatch (ExMeta "e") (AtMeta "a")         , ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")-        , defaultScope         , substs-            [ [("e", MvExpression (ExDispatch ExGlobal (AtLabel "org")) defaultScope), ("a", MvAttribute (AtLabel "eolang"))]-            , [("e", MvExpression ExGlobal defaultScope), ("a", MvAttribute (AtLabel "org"))]+            [ [("e", MvExpression (ExDispatch ExGlobal (AtLabel "org"))), ("a", MvAttribute (AtLabel "eolang"))]+            , [("e", MvExpression ExGlobal), ("a", MvAttribute (AtLabel "org"))]             ]         )       ,@@ -103,7 +98,6 @@                     ]                 )             )-        , defaultScope         , substs             [               [ ("B1", MvBindings [BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))])@@ -146,39 +140,11 @@                     ]                 )             ]-        , defaultScope         , substs             [-              [-                ( "e0"-                , MvExpression-                    ExGlobal-                    ( ExFormation-                        [ BiTau (AtLabel "a") ExGlobal-                        , BiTau (AtLabel "b") ExThis-                        ]-                    )-                )-              ,-                ( "e-first"-                , MvExpression-                    ExThis-                    ( ExFormation-                        [ BiTau (AtLabel "a") ExGlobal-                        , BiTau (AtLabel "b") ExThis-                        ]-                    )-                )-              ,-                ( "e-second"-                , MvExpression-                    (ExFormation [BiVoid AtPhi])-                    ( ExFormation-                        [ BiTau (AtLabel "a") ExGlobal-                        , BiTau (AtLabel "b") (ExFormation [BiVoid AtPhi])-                        ]-                    )-                )+              [ ("e0", MvExpression ExGlobal)+              , ("e-first", MvExpression ExThis)+              , ("e-second", MvExpression (ExFormation [BiVoid AtPhi]))               ]             ]         )@@ -202,98 +168,84 @@         ( "[[]] => [[]] => ()"         , []         , []-        , defaultScope         , substs [[]]         )       ,         ( "[[!B]] => T:[[x -> ?, D> 01-, L> Func]] => (!B >> T)"         , [BiMeta "B"]         , [BiVoid (AtLabel "x"), BiDelta (BtOne "01"), BiLambda "Func"]-        , defaultScope         , substs [[("B", MvBindings [BiVoid (AtLabel "x"), BiDelta (BtOne "01"), BiLambda "Func"])]]         )       ,         ( "[[D> 00-]] => [[D> 00-, L> Func]] => []"         , [BiDelta (BtOne "00")]         , [BiDelta (BtOne "00"), BiLambda "Func"]-        , defaultScope         , substs []         )       ,         ( "[[y -> ?, !a -> ?]] => [[y -> ?, x -> ?]] => (!a >> x)"         , [BiVoid (AtLabel "y"), BiVoid (AtMeta "a")]         , [BiVoid (AtLabel "y"), BiVoid (AtLabel "x")]-        , defaultScope         , substs [[("a", MvAttribute (AtLabel "x"))]]         )       ,         ( "[[!B, x -> ?]] => [[x -> ?]] => (!B >> [[]])"         , [BiMeta "B", BiVoid (AtLabel "x")]         , [BiVoid (AtLabel "x")]-        , defaultScope         , substs [[("B", MvBindings [])]]         )       ,         ( "[[!B1, x -> ?, !B2]] => [[x -> ?, y -> ?]] => (!B1 >> [[]], !B2 >> [[y -> ?]])"         , [BiMeta "B1", BiVoid (AtLabel "x"), BiMeta "B2"]         , [BiVoid (AtLabel "x"), BiVoid (AtLabel "y")]-        , defaultScope         , substs [[("B1", MvBindings []), ("B2", MvBindings [BiVoid (AtLabel "y")])]]         )       ,         ( "[[!B1, !x -> ?, !B2]] => [[y -> ?, D> -> 00-, L> Func]] => (!x >> y, !B1 >> [[]], !B2 >> [[D> -> 00-, L> Func]])"         , [BiMeta "B1", BiVoid (AtMeta "x"), BiMeta "B2"]         , [BiVoid (AtLabel "y"), BiDelta (BtOne "00"), BiLambda "Func"]-        , defaultScope         , substs [[("B1", MvBindings []), ("B2", MvBindings [BiDelta (BtOne "00"), BiLambda "Func"]), ("x", MvAttribute (AtLabel "y"))]]         )       ,         ( "[[!x -> ?, !y -> ?]] => [[a -> ?, b -> ?]] => (!x >> a, !y >> b)"         , [BiVoid (AtMeta "x"), BiVoid (AtMeta "y")]         , [BiVoid (AtLabel "a"), BiVoid (AtLabel "b")]-        , defaultScope         , substs [[("x", MvAttribute (AtLabel "a")), ("y", MvAttribute (AtLabel "b"))]]         )       ,         ( "[[t -> ?, !B]] => [[t -> ?, x -> Q, y -> $]] => (!B >> [[x -> Q, y -> $]])"         , [BiVoid (AtLabel "t"), BiMeta "B"]         , [BiVoid (AtLabel "t"), BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis]-        , defaultScope         , substs [[("B", MvBindings [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis])]]         )       ,         ( "[[!B, z -> Q]] => [[x -> Q, y -> $, z -> Q]] => (!B >> [[x -> Q, y -> $]])"         , [BiMeta "B", BiTau (AtLabel "z") ExGlobal]         , [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis, BiTau (AtLabel "z") ExGlobal]-        , defaultScope         , substs [[("B", MvBindings [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis])]]         )       ,         ( "[[L> Func, D> 00-]] => [[D> 00-, L> Func]] => []"         , [BiLambda "Func", BiDelta (BtOne "00")]         , [BiDelta (BtOne "00"), BiLambda "Func"]-        , defaultScope         , substs []         )       ,         ( "[[t -> ?, !B]] => [[x -> ?, t -> ?]] => []"         , [BiVoid (AtLabel "t"), BiMeta "B"]         , [BiVoid (AtLabel "x"), BiVoid (AtLabel "t")]-        , defaultScope         , substs []         )       ,         ( "[[!B, !a -> ?]] => [[x -> ?, y -> ?]] => (!a >> y, !B >> [[ x -> ? ]] )"         , [BiMeta "B", BiVoid (AtMeta "a")]         , [BiVoid (AtLabel "x"), BiVoid (AtLabel "y")]-        , defaultScope         , substs [[("a", 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"]         , [BiVoid (AtLabel "x"), BiVoid (AtLabel "y"), BiVoid (AtLabel "z")]-        , defaultScope         , substs             [               [ ("B1", MvBindings [])@@ -322,7 +274,6 @@           , BiVoid (AtLabel "y")           , BiVoid (AtLabel "z")           ]-        , defaultScope         , substs             [               [ ("B1", MvBindings [])@@ -401,35 +352,31 @@   describe "matchExpression: expression => pattern => substitution" $     test       matchExpression'-      [ ("$ => $ => [()]", ExThis, ExThis, defaultScope, substs [[]])-      , ("Q => Q => [()]", ExGlobal, ExGlobal, defaultScope, substs [[]])+      [ ("$ => $ => [()]", ExThis, ExThis, substs [[]])+      , ("Q => Q => [()]", ExGlobal, ExGlobal, substs [[]])       ,         ( "!e => Q => [(!e >> Q)]"         , ExMeta "e"         , ExGlobal-        , defaultScope-        , substs [[("e", MvExpression ExGlobal defaultScope)]]+        , substs [[("e", MvExpression ExGlobal)]]         )       ,         ( "!e => Q.org(x -> $) => [(!e >> Q.org(x -> $))]"         , ExMeta "e"         , ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") ExThis)-        , defaultScope-        , substs [[("e", MvExpression (ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") ExThis)) defaultScope)]]+        , substs [[("e", MvExpression (ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") ExThis)))]]         )       ,         ( "!e1.x => Q.org.x => [(!e1 >> Q.org)]"         , ExDispatch (ExMeta "e1") (AtLabel "x")         , ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "x")-        , defaultScope-        , substs [[("e1", MvExpression (ExDispatch ExGlobal (AtLabel "org")) defaultScope)]]+        , substs [[("e1", MvExpression (ExDispatch ExGlobal (AtLabel "org")))]]         )       ,         ( "!e.org.!a => $.org.x => [(!e >> $, !a >> x)]"         , ExDispatch (ExDispatch (ExMeta "e") (AtLabel "org")) (AtMeta "a")         , ExDispatch (ExDispatch ExThis (AtLabel "org")) (AtLabel "x")-        , defaultScope-        , substs [[("e", MvExpression ExThis defaultScope), ("a", MvAttribute (AtLabel "x"))]]+        , substs [[("e", MvExpression ExThis), ("a", MvAttribute (AtLabel "x"))]]         )       ,         ( "[[!a -> !e, !B]].!a => [[x -> Q, y -> $]].x => [(!a >> x, !e >> Q, !B >> [y -> $])]"@@ -441,20 +388,10 @@                 ]             )             (AtLabel "x")-        , defaultScope         , substs             [               [ ("a", MvAttribute (AtLabel "x"))-              ,-                ( "e"-                , MvExpression-                    ExGlobal-                    ( ExFormation-                        [ BiTau (AtLabel "x") ExGlobal-                        , BiTau (AtLabel "y") ExThis-                        ]-                    )-                )+              , ("e", MvExpression ExGlobal)               , ("B", MvBindings [BiTau (AtLabel "y") ExThis])               ]             ]@@ -463,28 +400,24 @@         ( "Q * !t => Q.org => [(!t >> [.org])]"         , ExMetaTail ExGlobal "t"         , ExDispatch ExGlobal (AtLabel "x")-        , defaultScope         , substs [[("t", MvTail [TaDispatch (AtLabel "x")])]]         )       ,         ( "Q * !t => Q.org(x -> [[]]) => [(!t >> [.org, (x -> [[]])])]"         , ExMetaTail ExGlobal "t"-        , ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") defaultScope)-        , defaultScope-        , substs [[("t", MvTail [TaDispatch (AtLabel "org"), TaApplication (BiTau (AtLabel "x") defaultScope)])]]+        , ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))+        , substs [[("t", MvTail [TaDispatch (AtLabel "org"), TaApplication (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))])]]         )       ,         ( "Q.!a * !t => Q.org.eolang(x -> [[]]) => [(!a >> org, !t >> [ .eolang, ( x -> [[ ]] ) ])]"         , ExMetaTail (ExDispatch ExGlobal (AtMeta "a")) "t"-        , ExApplication (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (BiTau (AtLabel "x") defaultScope)-        , defaultScope-        , substs [[("a", MvAttribute (AtLabel "org")), ("t", MvTail [TaDispatch (AtLabel "eolang"), TaApplication (BiTau (AtLabel "x") defaultScope)])]]+        , ExApplication (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))+        , substs [[("a", MvAttribute (AtLabel "org")), ("t", MvTail [TaDispatch (AtLabel "eolang"), TaApplication (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))])]]         )       ,         ( "Q.x(y -> $ * !t1) * !t2 => Q.x(y -> $.q).p => [(!t1 >> [.q], !t2 >> [.p])]"         , ExMetaTail (ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") (ExMetaTail ExThis "t1"))) "t2"         , ExDispatch (ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") (ExDispatch ExThis (AtLabel "q")))) (AtLabel "p")-        , defaultScope         , substs [[("t1", MvTail [TaDispatch (AtLabel "q")]), ("t2", MvTail [TaDispatch (AtLabel "p")])]]         )       ,@@ -498,24 +431,13 @@                 ]             )             (BiTau (AtLabel "x") ExThis)-        , defaultScope         , substs             [               [ ("B1", MvBindings [BiTau (AtLabel "t") (ExDispatch ExThis (AtLabel "k"))])               , ("a", MvAttribute (AtLabel "x"))               , ("B2", MvBindings [BiVoid (AtLabel "k")])-              ,-                ( "e1"-                , MvExpression-                    (ExDispatch ExThis (AtLabel "t"))-                    ( ExFormation-                        [ BiTau (AtLabel "t") (ExDispatch ExThis (AtLabel "k"))-                        , BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))-                        , BiVoid (AtLabel "k")-                        ]-                    )-                )-              , ("e2", MvExpression ExThis defaultScope)+              , ("e1", MvExpression (ExDispatch ExThis (AtLabel "t")))+              , ("e2", MvExpression ExThis)               ]             ]         )

@@ -71,6 +71,28 @@           it desc (printProgram prog `shouldBe` expected)       ) +  describe "printProgram in salty does not inject a duplicate void rho when rho is already present" $+    forM_+      [+        ( "rho bound to an empty formation"+        , Program (ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])])+        , "Φ ↦ ⟦ ρ ↦ ⟦ ρ ↦ ∅ ⟧ ⟧"+        )+      ,+        ( "rho bound to a non empty formation"+        , Program (ExFormation [BiTau AtRho (ExFormation [BiVoid (AtLabel "名前"), BiVoid AtRho])])+        , "Φ ↦ ⟦ ρ ↦ ⟦ 名前 ↦ ∅, ρ ↦ ∅ ⟧ ⟧"+        )+      ,+        ( "rho binding placed after another binding"+        , Program (ExFormation [BiTau (AtLabel "café") ExGlobal, BiTau AtRho (ExFormation [BiVoid AtRho])])+        , "Φ ↦ ⟦ café ↦ Φ, ρ ↦ ⟦ ρ ↦ ∅ ⟧ ⟧"+        )+      ]+      ( \(desc, prog, expected) ->+          it desc (printProgram' prog (SALTY, UNICODE, SINGLELINE, defaultMargin) `shouldBe` expected)+      )+   describe "printAttribute with default encoding" $     forM_       [ ("label", AtLabel "attr", "attr")