diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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. @@ -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 diff --git a/phino.cabal b/phino.cabal --- a/phino.cabal +++ b/phino.cabal @@ -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 diff --git a/resources/dataization.yaml b/resources/dataization.yaml --- a/resources/dataization.yaml +++ b/resources/dataization.yaml @@ -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: 𝑛 diff --git a/resources/morphing.yaml b/resources/morphing.yaml --- a/resources/morphing.yaml +++ b/resources/morphing.yaml @@ -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' diff --git a/src/AST.hs b/src/AST.hs --- a/src/AST.hs +++ b/src/AST.hs @@ -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 diff --git a/src/Builder.hs b/src/Builder.hs --- a/src/Builder.hs +++ b/src/Builder.hs @@ -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 diff --git a/src/CST.hs b/src/CST.hs --- a/src/CST.hs +++ b/src/CST.hs @@ -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) diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -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") diff --git a/src/Encoding.hs b/src/Encoding.hs --- a/src/Encoding.hs +++ b/src/Encoding.hs @@ -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 diff --git a/src/Functions.hs b/src/Functions.hs --- a/src/Functions.hs +++ b/src/Functions.hs @@ -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 diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -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 diff --git a/src/Lining.hs b/src/Lining.hs --- a/src/Lining.hs +++ b/src/Lining.hs @@ -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 diff --git a/src/Margin.hs b/src/Margin.hs --- a/src/Margin.hs +++ b/src/Margin.hs @@ -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), ..} = diff --git a/src/Matcher.hs b/src/Matcher.hs --- a/src/Matcher.hs +++ b/src/Matcher.hs @@ -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 = [] diff --git a/src/Parser.hs b/src/Parser.hs --- a/src/Parser.hs +++ b/src/Parser.hs @@ -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 diff --git a/src/Printer.hs b/src/Printer.hs --- a/src/Printer.hs +++ b/src/Printer.hs @@ -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 = diff --git a/src/Render.hs b/src/Render.hs --- a/src/Render.hs +++ b/src/Render.hs @@ -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) diff --git a/src/Rule.hs b/src/Rule.hs --- a/src/Rule.hs +++ b/src/Rule.hs @@ -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 _ = [] diff --git a/src/Sugar.hs b/src/Sugar.hs --- a/src/Sugar.hs +++ b/src/Sugar.hs @@ -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 diff --git a/src/Tau.hs b/src/Tau.hs --- a/src/Tau.hs +++ b/src/Tau.hs @@ -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 diff --git a/src/Yaml.hs b/src/Yaml.hs --- a/src/Yaml.hs +++ b/src/Yaml.hs @@ -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 diff --git a/test/ASTSpec.hs b/test/ASTSpec.hs --- a/test/ASTSpec.hs +++ b/test/ASTSpec.hs @@ -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) ] diff --git a/test/BuilderSpec.hs b/test/BuilderSpec.hs --- a/test/BuilderSpec.hs +++ b/test/BuilderSpec.hs @@ -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") , [] diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -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}" diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -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 [ diff --git a/test/MatcherSpec.hs b/test/MatcherSpec.hs --- a/test/MatcherSpec.hs +++ b/test/MatcherSpec.hs @@ -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 >> $)]" diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs --- a/test/ParserSpec.hs +++ b/test/ParserSpec.hs @@ -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" $ diff --git a/test/PrinterSpec.hs b/test/PrinterSpec.hs --- a/test/PrinterSpec.hs +++ b/test/PrinterSpec.hs @@ -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 -> $ ]]")