diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -214,7 +214,7 @@ $ phino explain --normalize \begin{tabular}{rl} \phinoNormalizationRule{alpha} - { [[ B_1, \tau -> ?, B_2 ]] ( \alpha_{i} -> e ) } + { [[ B_1, \tau -> ?, B_2 ]] ( \phiTerminal{\alpha_{i}} -> e ) } { [[ B_1, \tau -> ?, B_2 ]] ( \tau -> e ) } { $ i = \vert \overline{ B_1 } \vert $ } { } @@ -255,14 +255,14 @@ $ phino explain --dataize \begin{tabular}{rl} \phinoDataizationRule{delta} - { \mathbb{D}( [[ B_1, D> Ξ΄, B_2 ]] ) } + { \phinoDataize{ [[ B_1, D> Ξ΄, B_2 ]] } } { Ξ΄ } { } { } ... \phinoDataizationRule{norm} - { \mathbb{D}( n ) } - { \mathbb{D}( \mathbb{M}( n ) ) } + { \phinoDataize{ n } } + { \phinoDataize{ \mathbb{M}( n ) } } { } { } \end{tabular} @@ -378,7 +378,7 @@ * `!t` || `𝜏` - attribute * `!i` || `𝑖` - the index of a positional (Ξ±) application argument, - captured by writing `α𝑖` (or `a𝑖`) + captured by writing `α𝑖` (or `~!i`) * `!e` || `𝑒` - any expression * `!n` || `𝑛` - any expression that is already in normal form (behaves like `!e`/`𝑒`, but only binds a sub-expression in NF, so no explicit @@ -393,8 +393,8 @@ Every meta variable may also be used with an integer index, like `!B1` or `𝜏0`. -A positional (Ξ±) application argument is written as `Ξ±0`, `a0` (ASCII), or -`α𝑖`/`a!i` when its index is captured by an `!i`/`𝑖` meta variable. +A positional (Ξ±) application argument is written as `Ξ±0`, `~0` (ASCII), or +`α𝑖`/`~!i` when its index is captured by an `!i`/`𝑖` meta variable. Incorrect usage of meta variables in πœ‘-expression patterns leads to parsing errors. 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.84 +version: 0.0.85 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 @@ -5,6 +5,7 @@ # is always a normal form: a non-NF expression matches no clause. - name: delta + label: \Delta description: '𝔻(⟦𝐡1, Ξ” ‍ Ξ΄, 𝐡2⟧) ⟿ Ξ΄' match: ⟦𝐡1, Ξ” ‍ Ξ΄, 𝐡2⟧ then: Ξ΄ diff --git a/resources/morphing.yaml b/resources/morphing.yaml --- a/resources/morphing.yaml +++ b/resources/morphing.yaml @@ -14,6 +14,7 @@ then: ⟦𝐡⟧ - name: lambda + label: \lambda description: '𝕄(⟦𝐡1, Ξ» ‍ 𝐹, 𝐡2⟧.Ο„) ⟿ 𝕄(𝒩(𝔼(⟦𝐡1, Ξ» ‍ 𝐹, 𝐡2⟧).Ο„))' match: '⟦𝐡1, Ξ» ‍ 𝐹, 𝐡2⟧.𝜏' where: diff --git a/resources/normalize/amiss.yaml b/resources/normalize/amiss.yaml new file mode 100644 --- /dev/null +++ b/resources/normalize/amiss.yaml @@ -0,0 +1,11 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: amiss +pattern: ⟦𝐡⟧(α𝑖 ↦ 𝑒) +result: βŠ₯ +when: + not: + gt: + - domain: 𝐡 + - 𝑖 diff --git a/resources/normalize/phi.yaml b/resources/normalize/phi.yaml --- a/resources/normalize/phi.yaml +++ b/resources/normalize/phi.yaml @@ -2,6 +2,7 @@ # SPDX-License-Identifier: MIT --- name: phi +label: \phi pattern: ⟦𝐡⟧.𝜏 result: ⟦𝐡⟧.Ο†.𝜏 when: diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -246,4 +246,4 @@ else putStrLn (P.printSubsts' substs (_sugarType, UNICODE, _flat, defaultMargin)) where rule :: Expression -> Maybe Y.Condition -> Y.Rule - rule ptn cnd = Y.Rule "custom" Nothing ptn ExRoot cnd Nothing Nothing + rule ptn cnd = Y.Rule "custom" Nothing Nothing ptn ExRoot cnd Nothing Nothing diff --git a/src/CST.hs b/src/CST.hs --- a/src/CST.hs +++ b/src/CST.hs @@ -48,7 +48,7 @@ data DELTA = DELTA | DELTA' deriving (Eq, Show) -data XI = XI | DOLLAR +data XI = XI | DOLLAR | XI' deriving (Eq, Show) data LAMBDA = LAMBDA | LAMBDA' @@ -206,6 +206,8 @@ data EQUAL = EQUAL | NOT_EQUAL + | GREATER + | NOT_GREATER deriving (Eq, Show) data NUMBER @@ -343,7 +345,7 @@ -- Since we convert AST to CST in sweet notation, here we're trying to get rid of unnecessary rho bindings -- in primitives (more details here: https://github.com/objectionary/phino/issues/451) -- If we find something similar to: - -- `Q.number(a0 -> Q.bytes(...), ^ -> ..., ^ -> ...)` + -- `Q.number(~0 -> Q.bytes(...), ^ -> ..., ^ -> ...)` -- We remove unnecessary rho bindings and save them to EX_STRING or EX_NUMBER so they can be successfully -- converted to salty notation without losing information. -- In the end we just get CST with data primitive which is printed correctly. @@ -409,7 +411,7 @@ -- 1. deepest start expression -- 2. list of tau bindings which are applied to start expression -- 3. list of expressions which are applied to start expression with default - -- alpha attributes (a0 -> e1, a1 -> e2, ...) + -- alpha attributes (~0 -> e1, ~1 -> e2, ...) complexApplication :: Expression -> (Expression, [Argument], [Expression]) complexApplication expr = let (expr', taus', exprs') = complexApplication' expr @@ -521,6 +523,7 @@ instance ToCST Y.Condition CONDITION where toCST (Y.Not (Y.In attr binding)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_BINDING (bindingsToCST [binding])) toCST (Y.Not (Y.Eq left right)) _ = CO_COMPARE (comparableToCST left) NOT_EQUAL (comparableToCST right) + toCST (Y.Not (Y.Gt left right)) _ = CO_COMPARE (comparableToCST left) NOT_GREATER (comparableToCST right) toCST (Y.Not (Y.Absolute expr)) _ = CO_ABSOLUTE (expressionToCST expr) NOT_IN toCST (Y.Absolute expr) _ = CO_ABSOLUTE (expressionToCST expr) IN toCST (Y.Disjoint attrs groups) _ = CO_DISJOINT (map attributeToCST attrs) (map (\bd -> bindingsToCST [bd]) groups) @@ -534,6 +537,7 @@ toCST (Y.NF expr) _ = CO_NF (expressionToCST expr) toCST (Y.Not cond) _ = CO_NOT (conditionToCST cond) toCST (Y.Eq left right) _ = CO_COMPARE (comparableToCST left) EQUAL (comparableToCST right) + toCST (Y.Gt left right) _ = CO_COMPARE (comparableToCST left) GREATER (comparableToCST right) toCST (Y.Matches regex expr) _ = CO_MATCHES regex (expressionToCST expr) toCST (Y.PartOf expr binding) _ = CO_PART_OF (expressionToCST expr) (bindingsToCST [binding]) diff --git a/src/Condition.hs b/src/Condition.hs --- a/src/Condition.hs +++ b/src/Condition.hs @@ -112,6 +112,13 @@ _ <- rparen return (Y.Eq left right) , do + _ <- symbol "gt" >> lparen + left <- comparable + _ <- comma + right <- comparable + _ <- rparen + return (Y.Gt left right) + , do _ <- symbol "nf" >> lparen expr <- _expression phiParser _ <- rparen diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -89,7 +89,7 @@ -- maps onto the 'having' slot (which runs after 'where'), not 'when' (which -- 'matchExpressionWithRule'' runs before 'where'). asRule :: Y.MorphRule -> Y.Rule - asRule rule = Y.Rule rule.name rule.description rule.match ExRoot Nothing rule.where_ rule.when + asRule rule = Y.Rule rule.name Nothing rule.description rule.match ExRoot Nothing rule.where_ rule.when apply :: Y.MorphOutcome -> String -> Subst -> IO Morphed apply (Y.MoStop result) name subst = do built <- buildExpressionThrows result subst @@ -137,7 +137,7 @@ (subst : _) -> pure (Just (rule, subst)) [] -> firstMatch rest asRule :: Y.DataizeRule -> Y.Rule - asRule rule = Y.Rule rule.name rule.description rule.match ExRoot Nothing rule.where_ rule.when + asRule rule = Y.Rule rule.name Nothing rule.description rule.match ExRoot Nothing rule.where_ rule.when apply :: Y.DataizeRule -> Subst -> IO Dataized apply rule subst = case rule.then_ of Y.DoData bytes -> do diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -234,6 +234,7 @@ toLaTeX EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toLaTeX expr) toLaTeX EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toLaTeX expr) toLaTeX EX_META{..} = EX_META (toLaTeX meta) + toLaTeX EX_XI{} = EX_XI XI' toLaTeX expr = expr instance ToLaTeX ATTRIBUTE where @@ -269,7 +270,7 @@ let subscript = case alpha of AL_IDX _ n -> render n AL_META _ mt -> render (hd mt) <> rest mt - in PA_TAU (AT_LABEL ("\\alpha_{" <> subscript <> "}")) arrow (toLaTeX expr) + in PA_TAU (AT_LABEL ("\\phiTerminal{\\alpha_{" <> subscript <> "}}")) arrow (toLaTeX expr) toLaTeX PA_FORMATION{..} = PA_FORMATION (toLaTeX attr) (map toLaTeX voids) arrow (toLaTeX expr) toLaTeX PA_META_DELTA{..} = toLaTeX (PA_META_DELTA' meta) toLaTeX PA_META_DELTA'{..} = PA_META_DELTA' (toLaTeX meta) @@ -353,6 +354,7 @@ explainRule rule = trrule "\\phinoNormalizationRule" + rule.label rule.name (renderToLatex (expressionToCST rule.pattern) defaultLatexContext) (renderToLatex (expressionToCST rule.result) defaultLatexContext) @@ -370,6 +372,7 @@ explainMorphRule rule = trrule "\\phinoMorphingRule" + rule.label rule.name (morph (renderToLatex (expressionToCST rule.match) defaultLatexContext)) (morphOutcome rule.then_) @@ -385,6 +388,7 @@ explainDataizeRule rule = trrule "\\phinoDataizationRule" + rule.label rule.name (dataize (renderToLatex (expressionToCST rule.match) defaultLatexContext)) (dataizeOutcome rule.then_) @@ -399,25 +403,29 @@ dataizeOutcome Y.DoNothing = "\\varnothing" -- Render a single rule row through the given macro (one of --- \phinoMorphingRule, \phinoNormalizationRule, \phinoDataizationRule): name, --- left-hand side, right-hand side, the optional 'if' condition and 'where' --- extras. -trrule :: String -> String -> String -> String -> Maybe Y.Condition -> Maybe [Y.Extra] -> String -trrule macro name lhs rhs cond extras = +-- \phinoMorphingRule, \phinoNormalizationRule, \phinoDataizationRule): an +-- optional typeset label, name, left-hand side, right-hand side, the optional +-- 'if' condition and 'where' extras. When the label is present it becomes the +-- macro's first optional argument ('\macro[label]{name}'); when absent the +-- optional argument is omitted entirely ('\macro{name}'). +trrule :: String -> Maybe String -> String -> String -> String -> Maybe Y.Condition -> Maybe [Y.Extra] -> String +trrule macro label name lhs rhs cond extras = intercalate "\n " - [ macro ++ "{" ++ name ++ "}" + [ macro ++ labelArg ++ "{" ++ name ++ "}" , braced lhs , braced rhs , conditionToLatex cond , extraArgumentsToLatex extras ] + where + labelArg = maybe "" (\symbol -> "[" ++ symbol ++ "]") label morph :: String -> String -morph inner = "\\mathbb{M}( " ++ inner ++ " )" +morph inner = "\\phinoMorph{ " ++ inner ++ " }" dataize :: String -> String -dataize inner = "\\mathbb{D}( " ++ inner ++ " )" +dataize inner = "\\phinoDataize{ " ++ inner ++ " }" normalize :: String -> String normalize inner = "\\phinoNormalize{ " ++ inner ++ " }" diff --git a/src/Parser.hs b/src/Parser.hs --- a/src/Parser.hs +++ b/src/Parser.hs @@ -337,11 +337,11 @@ index' = meta' 'i' "𝑖" -- alpha --- 1. index: a0, Ξ±0 --- 2. meta: α𝑖, a!i +-- 1. index: ~0, Ξ±0 +-- 2. meta: α𝑖, ~!i alpha :: Parser Alpha alpha = do - _ <- choice [symbol "a", symbol "Ξ±"] + _ <- choice [symbol "~", symbol "Ξ±"] choice [ Alpha <$> lexeme L.decimal , AlMeta <$> index' diff --git a/src/Render.hs b/src/Render.hs --- a/src/Render.hs +++ b/src/Render.hs @@ -67,7 +67,7 @@ instance Render RHO where render RHO = "ρ" render CARET = "^" - render RHO' = "\\rho" + render RHO' = "\\phiTerminal{\\rho}" instance Render DELTA where render DELTA = "Ξ”" @@ -76,6 +76,7 @@ instance Render XI where render XI = "ΞΎ" render DOLLAR = "$" + render XI' = "\\phiTerminal{\\xi}" instance Render LAMBDA where render LAMBDA = "Ξ»" @@ -135,7 +136,7 @@ instance Render ALPHA' where render ALPHA = "Ξ±" - render ALPHA' = "a" + render ALPHA' = "~" instance Render ALPHA where render AL_IDX{..} = render sym <> render idx @@ -245,6 +246,8 @@ instance Render EQUAL where render EQUAL = "=" render NOT_EQUAL = "\\not=" + render GREATER = ">" + render NOT_GREATER = "\\not>" instance Render CONDITION where render CO_BELONGS{..} = render attr <> " " <> render belongs <> " " <> render set diff --git a/src/Rule.hs b/src/Rule.hs --- a/src/Rule.hs +++ b/src/Rule.hs @@ -110,27 +110,29 @@ attrInBinding _ _ = False attrInBindings _ _ = False -_eq :: Y.Comparable -> Y.Comparable -> Subst -> RuleContext -> IO [Subst] -_eq (Y.CmpNum left) (Y.CmpNum right) subst _ = case (numToInt left subst, numToInt right subst) of - (Just left_, Just right_) -> pure [subst | left_ == right_] - (_, _) -> pure [] +-- Convert a 'Number' to an 'Int' under the given substitution, resolving +-- index metas, binding lengths and formation domains. +numToInt :: Y.Number -> Subst -> Maybe Int +numToInt (Y.MetaIndex meta) (Subst mp) = case M.lookup meta mp of + Just (MvIndex idx) -> Just idx + _ -> Nothing +numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of + Just (MvBindings bds) -> Just (length bds) + _ -> Nothing +numToInt (Y.Domain (BiMeta meta)) (Subst mp) = case M.lookup meta mp of + Just (MvBindings bds) -> Just (length (filter notAsset bds)) + _ -> Nothing where - -- Convert Number to Int - numToInt :: Y.Number -> Subst -> Maybe Int - numToInt (Y.MetaIndex meta) (Subst mp) = case M.lookup meta mp of - Just (MvIndex idx) -> Just idx - _ -> Nothing - numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of - Just (MvBindings bds) -> Just (length bds) - _ -> Nothing - numToInt (Y.Domain (BiMeta meta)) (Subst mp) = case M.lookup meta mp of - Just (MvBindings bds) -> Just (length (filter notAsset bds)) - _ -> Nothing - numToInt (Y.Literal num) _ = Just num - numToInt _ _ = Nothing notAsset (BiDelta _) = False notAsset (BiLambda _) = False notAsset _ = True +numToInt (Y.Literal num) _ = Just num +numToInt _ _ = Nothing + +_eq :: Y.Comparable -> Y.Comparable -> Subst -> RuleContext -> IO [Subst] +_eq (Y.CmpNum left) (Y.CmpNum right) subst _ = case (numToInt left subst, numToInt right subst) of + (Just left_, Just right_) -> pure [subst | left_ == right_] + (_, _) -> pure [] _eq (Y.CmpAttr left) (Y.CmpAttr right) subst _ = pure [subst | compareAttrs left right subst] where compareAttrs :: Attribute -> Attribute -> Subst -> Bool @@ -159,6 +161,14 @@ compareExprs left right _ = left == right _eq _ _ _ _ = pure [] +-- Hold if the left number is strictly greater than the right one. Only +-- numeric comparables are ordered; anything else fails to hold. +_gt :: Y.Comparable -> Y.Comparable -> Subst -> RuleContext -> IO [Subst] +_gt (Y.CmpNum left) (Y.CmpNum right) subst _ = case (numToInt left subst, numToInt right subst) of + (Just left_, Just right_) -> pure [subst | left_ > right_] + (_, _) -> pure [] +_gt _ _ _ _ = pure [] + _nf :: Expression -> Subst -> RuleContext -> IO [Subst] _nf (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of Just (MvExpression expr) -> _nf expr (Subst mp) ctx @@ -231,6 +241,7 @@ meetCondition' (Y.Not cond) = _not cond meetCondition' (Y.In attr binding) = _in attr binding meetCondition' (Y.Eq left right) = _eq left right +meetCondition' (Y.Gt left right) = _gt left right meetCondition' (Y.NF expr) = _nf expr meetCondition' (Y.Absolute expr) = _absolute expr meetCondition' (Y.Matches pat expr) = _matches pat expr diff --git a/src/Sugar.hs b/src/Sugar.hs --- a/src/Sugar.hs +++ b/src/Sugar.hs @@ -51,7 +51,7 @@ -- | a -> "Hey" | Q.number(Q.bytes([[ D> 48-65-79 ]])) | -- | [[ B ]] | [[ B, ^ -> ? ]], if rho is absent in 'B' | -- | a1(a2, a3, ...) -> [[ B ]] | a1 -> [[ a2 -> ?, a3 -> ?, ..., B ]] | --- | e(e0, e1, ...) | e(a0 -> e0, a1 -> e1, ...) | +-- | e(e0, e1, ...) | e(~0 -> e0, ~1 -> e1, ...) | -- | e(a1 -> e1, a2 -> e2, ...) | e(a1 -> e1)(a2 -> e2)... | -- |----------------------------|-----------------------------------------------------| class ToSalty a where diff --git a/src/Yaml.hs b/src/Yaml.hs --- a/src/Yaml.hs +++ b/src/Yaml.hs @@ -83,7 +83,7 @@ withObject "Condition" ( \v -> do - validateYamlObject v ["and", "or", "not", "nf", "absolute", "eq", "in", "matches", "part-of", "disjoint"] + validateYamlObject v ["and", "or", "not", "nf", "absolute", "eq", "gt", "in", "matches", "part-of", "disjoint"] asum [ And <$> v .: "and" , Or <$> v .: "or" @@ -101,6 +101,11 @@ [left_, right_] -> Eq <$> parseJSON left_ <*> parseJSON right_ _ -> fail "'eq' expects exactly two arguments" , do + vals <- v .: "gt" + case vals of + [left_, right_] -> Gt <$> parseJSON left_ <*> parseJSON right_ + _ -> fail "'gt' expects exactly two arguments" + , do vals <- v .: "in" case vals of [attr_, binding_] -> do @@ -169,6 +174,7 @@ | In Attribute Binding | Not Condition | Eq Comparable Comparable + | Gt Comparable Comparable | NF Expression | Absolute Expression | Matches String Expression @@ -192,6 +198,7 @@ data Rule = Rule { name :: String + , label :: Maybe String , description :: Maybe String , pattern :: Expression , result :: Expression @@ -251,6 +258,7 @@ -- 'where', filter by 'when', then reduce per 'then'. data MorphRule = MorphRule { name :: String + , label :: Maybe String , description :: Maybe String , match :: Expression , where_ :: Maybe [Extra] @@ -263,6 +271,7 @@ -- under 𝔻 and able to terminate with bytes or 'nothing'. data DataizeRule = DataizeRule { name :: String + , label :: Maybe String , description :: Maybe String , match :: Expression , where_ :: Maybe [Extra] @@ -306,6 +315,7 @@ ( \o -> MorphRule <$> o .: "name" + <*> o .:? "label" <*> o .:? "description" <*> o .: "match" <*> o .:? "where" @@ -320,6 +330,7 @@ ( \o -> DataizeRule <$> o .: "name" + <*> o .:? "label" <*> o .:? "description" <*> o .: "match" <*> o .:? "where" diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -422,8 +422,8 @@ , "\\Big\\{ [[" , " |x\\char95{}o| -> Q . |z| ( |y| -> 5 )," , " |q\\char36{}| -> T," - , " |w| -> $," - , " \\rho -> Q," + , " |w| -> \\phiTerminal{\\xi}," + , " \\phiTerminal{\\rho} -> Q," , " @ -> 1," , " |y| -> \"H$@^M\"," , " L> |Fu\\char95{}nc|" @@ -444,12 +444,12 @@ ] it "rewrites an alpha-index argument as \\alpha subscript in LaTeX" $ - withStdin "Q -> Q.foo(a1 -> Q.y)" $ + withStdin "Q -> Q.foo(~1 -> Q.y)" $ testCLISucceeded ["rewrite", "--output=latex", "--flat", "--nonumber"] [ unlines [ "\\begin{phiquation*}" - , "Q -> Q . |foo| ( \\alpha_{1} -> Q . |y| ){.}" + , "Q -> Q . |foo| ( \\phiTerminal{\\alpha_{1}} -> Q . |y| ){.}" , "\\end{phiquation*}" ] ] @@ -558,10 +558,10 @@ [ "\\begin{phiquation}" , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{foo:1}{ [[ D> 42- ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}" , " \\leadsto \\Big\\{ \\phinoMeet{foo:2}{ [[ |x| -> \\phinoAgain{foo:1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\Big\\{ \\phinoAgain{foo:2} . |x| ( \\rho -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\Big\\{ \\phinoAgain{foo:1} ( \\rho -> \\phinoAgain{foo:2}, \\rho -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}" - , " \\leadsto \\Big\\{ [[ D> 42-, \\rho -> \\phinoAgain{foo:2} ]] ( \\rho -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}" - , " \\leadsto \\Big\\{ [[ D> 42-, \\rho -> \\phinoAgain{foo:2} ]] \\Big\\}{.}" + , " \\leadsto \\Big\\{ \\phinoAgain{foo:2} . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}" + , " \\leadsto \\Big\\{ \\phinoAgain{foo:1} ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2}, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}" + , " \\leadsto \\Big\\{ [[ D> 42-, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}" + , " \\leadsto \\Big\\{ [[ D> 42-, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]] \\Big\\}{.}" , "\\end{phiquation}" ] ] @@ -574,10 +574,10 @@ [ "\\begin{phiquation}" , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{1}{ [[ D> 42- ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}" , " \\leadsto \\Big\\{ \\phinoMeet{2}{ [[ |x| -> \\phinoAgain{1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\Big\\{ \\phinoAgain{2} . |x| ( \\rho -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\Big\\{ \\phinoAgain{1} ( \\rho -> \\phinoAgain{2}, \\rho -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}" - , " \\leadsto \\Big\\{ [[ D> 42-, \\rho -> \\phinoAgain{2} ]] ( \\rho -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}" - , " \\leadsto \\Big\\{ [[ D> 42-, \\rho -> \\phinoAgain{2} ]] \\Big\\}{.}" + , " \\leadsto \\Big\\{ \\phinoAgain{2} . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}" + , " \\leadsto \\Big\\{ \\phinoAgain{1} ( \\phiTerminal{\\rho} -> \\phinoAgain{2}, \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}" + , " \\leadsto \\Big\\{ [[ D> 42-, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}" + , " \\leadsto \\Big\\{ [[ D> 42-, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]] \\Big\\}{.}" , "\\end{phiquation}" ] ] @@ -652,7 +652,7 @@ [ unlines [ "\\begin{phiquation}" , "\\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |y| ( \\rho -> [[ |x| -> |y|, |y| -> |x| ]] ) \\Big\\} \\leadsto" + , " \\leadsto \\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |y| ( \\phiTerminal{\\rho} -> [[ |x| -> |y|, |y| -> |x| ]] ) \\Big\\} \\leadsto" , " \\leadsto \\dots" , "\\end{phiquation}" ] @@ -881,8 +881,8 @@ , "\\Big\\{ [[ @ -> [[ |x| -> [[ D> 01-, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| ]] \\Big\\} \\leadsto_{\\nameref{r:contextualize}}" , " \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:copy}}" , " \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]] ]] ( \\rho -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ) \\Big\\} \\leadsto_{\\nameref{r:copy}}" - , " \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], \\rho -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\}{.}" + , " \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ) \\Big\\} \\leadsto_{\\nameref{r:copy}}" + , " \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], \\phiTerminal{\\rho} -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\}{.}" , "\\end{phiquation}" , "01-" ] @@ -952,6 +952,18 @@ ] ] + it "explains single rule with a label" $ + testCLISucceeded + ["explain", "--rule=test-resources/cli/labeled.yaml"] + [ unlines + [ "\\phinoNormalizationRule[\\lambda]{copy}" + , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }" + , " { [[ B_1, \\tau -> k, B_2 ]] }" + , " { }" + , " { }" + ] + ] + it "explains multiple rules" $ testCLISucceeded ["explain", "--rule=resources/normalize/copy.yaml", "--rule=resources/normalize/alpha.yaml"] @@ -962,10 +974,15 @@ ["explain", "--normalize"] [ unlines [ "\\phinoNormalizationRule{alpha}" - , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\alpha_{i} -> e ) }" + , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }" , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }" , " { i = \\vert \\overline{ B_1 } \\vert }" , " { }" + , "\\phinoNormalizationRule{amiss}" + , " { [[ B ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }" + , " { T }" + , " { \\vert \\overline{ B } \\vert \\not> i }" + , " { }" , "\\phinoNormalizationRule{copy}" , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }" , " { [[ B_1, \\tau -> k, B_2 ]] }" @@ -977,7 +994,7 @@ , " { }" , " { }" , "\\phinoNormalizationRule{dca}" - , " { T ( \\alpha_{i} -> e ) }" + , " { T ( \\phiTerminal{\\alpha_{i}} -> e ) }" , " { T }" , " { }" , " { }" @@ -988,7 +1005,7 @@ , " { }" , "\\phinoNormalizationRule{dot}" , " { [[ B_1, \\tau -> n, B_2 ]] . \\tau }" - , " { e ( \\rho -> [[ B_1, \\tau -> n, B_2 ]] ) }" + , " { e ( \\phiTerminal{\\rho} -> [[ B_1, \\tau -> n, B_2 ]] ) }" , " { }" , " { e \\coloneqq \\ctx{ n }{ [[ B_1, \\tau -> n, B_2 ]] } }" , "\\phinoNormalizationRule{miss}" @@ -1004,16 +1021,16 @@ , "\\phinoNormalizationRule{over}" , " { [[ B_1, \\tau -> e_1, B_2 ]] ( \\tau -> e_2 ) }" , " { T }" - , " { \\tau \\not= \\rho }" + , " { \\tau \\not= \\phiTerminal{\\rho} }" , " { }" - , "\\phinoNormalizationRule{phi}" + , "\\phinoNormalizationRule[\\phi]{phi}" , " { [[ B ]] . \\tau }" , " { [[ B ]] . @ . \\tau }" , " { @ \\in B \\;\\text{and}\\; \\tau \\notin B }" , " { }" , "\\phinoNormalizationRule{stay}" - , " { [[ B_1, \\rho -> e_1, B_2 ]] ( \\rho -> e_2 ) }" - , " { [[ B_1, \\rho -> e_1, B_2 ]] }" + , " { [[ B_1, \\phiTerminal{\\rho} -> e_1, B_2 ]] ( \\phiTerminal{\\rho} -> e_2 ) }" + , " { [[ B_1, \\phiTerminal{\\rho} -> e_1, B_2 ]] }" , " { }" , " { }" , "\\phinoNormalizationRule{stop}" @@ -1029,47 +1046,47 @@ ["explain", "--morph"] [ unlines [ "\\phinoMorphingRule{prim}" - , " { \\mathbb{M}( [[ B ]] ) }" + , " { \\phinoMorph{ [[ B ]] } }" , " { [[ B ]] }" , " { }" , " { }" - , "\\phinoMorphingRule{lambda}" - , " { \\mathbb{M}( [[ B_1, L> F, B_2 ]] . \\tau ) }" - , " { \\mathbb{M}( \\phinoNormalize{ e . \\tau } ) }" + , "\\phinoMorphingRule[\\lambda]{lambda}" + , " { \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau } }" + , " { \\phinoMorph{ \\phinoNormalize{ e . \\tau } } }" , " { }" , " { e \\coloneqq \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] } }" , "\\phinoMorphingRule{dispatch}" - , " { \\mathbb{M}( n . \\tau ) }" - , " { \\mathbb{M}( \\phinoNormalize{ e . \\tau } ) }" + , " { \\phinoMorph{ n . \\tau } }" + , " { \\phinoMorph{ \\phinoNormalize{ e . \\tau } } }" , " { }" , " { e \\coloneqq \\phinoMorph{ n } }" , "\\phinoMorphingRule{application}" - , " { \\mathbb{M}( n ( \\tau -> e ) ) }" - , " { \\mathbb{M}( \\phinoNormalize{ e_1 ( \\tau -> e ) } ) }" + , " { \\phinoMorph{ n ( \\tau -> e ) } }" + , " { \\phinoMorph{ \\phinoNormalize{ e_1 ( \\tau -> e ) } } }" , " { }" , " { e_1 \\coloneqq \\phinoMorph{ n } }" , "\\phinoMorphingRule{applicationa}" - , " { \\mathbb{M}( n ( \\alpha_{i} -> e ) ) }" - , " { \\mathbb{M}( \\phinoNormalize{ e_1 ( \\alpha_{i} -> e ) } ) }" + , " { \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> e ) } }" + , " { \\phinoMorph{ \\phinoNormalize{ e_1 ( \\phiTerminal{\\alpha_{i}} -> e ) } } }" , " { }" , " { e_1 \\coloneqq \\phinoMorph{ n } }" , "\\phinoMorphingRule{root}" - , " { \\mathbb{M}( Q ) }" - , " { \\mathbb{M}( \\phinoNormalize{ e } ) }" + , " { \\phinoMorph{ Q } }" + , " { \\phinoMorph{ \\phinoNormalize{ e } } }" , " { e \\not= Q }" , " { e \\coloneqq \\phinoGlobal{ } }" , "\\phinoMorphingRule{dead}" - , " { \\mathbb{M}( T ) }" + , " { \\phinoMorph{ T } }" , " { T }" , " { }" , " { }" , "\\phinoMorphingRule{xi}" - , " { \\mathbb{M}( $ ) }" + , " { \\phinoMorph{ \\phiTerminal{\\xi} } }" , " { T }" , " { }" , " { }" , "\\phinoMorphingRule{globe}" - , " { \\mathbb{M}( Q ) }" + , " { \\phinoMorph{ Q } }" , " { T }" , " { }" , " { }" @@ -1080,34 +1097,34 @@ testCLISucceeded ["explain", "--dataize"] [ unlines - [ "\\phinoDataizationRule{delta}" - , " { \\mathbb{D}( [[ B_1, D> \\delta, B_2 ]] ) }" + [ "\\phinoDataizationRule[\\Delta]{delta}" + , " { \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] } }" , " { \\delta }" , " { }" , " { }" , "\\phinoDataizationRule{box}" - , " { \\mathbb{D}( [[ B_1, @ -> e, B_2 ]] ) }" - , " { \\mathbb{D}( \\phinoNormalize{ e_1 } ) }" + , " { \\phinoDataize{ [[ B_1, @ -> e, B_2 ]] } }" + , " { \\phinoDataize{ \\phinoNormalize{ e_1 } } }" , " { [ \\Delta, L ] \\cap ( B_1 \\cup B_2 ) = \\emptyset }" , " { e_1 \\coloneqq \\ctx{ e }{ [[ B_1, @ -> e, B_2 ]] } }" , "\\phinoDataizationRule{fire}" - , " { \\mathbb{D}( [[ B_1, L> F, B_2 ]] ) }" - , " { \\mathbb{D}( \\phinoNormalize{ e } ) }" + , " { \\phinoDataize{ [[ B_1, L> F, B_2 ]] } }" + , " { \\phinoDataize{ \\phinoNormalize{ e } } }" , " { }" , " { e \\coloneqq \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] } }" , "\\phinoDataizationRule{none}" - , " { \\mathbb{D}( [[ B ]] ) }" + , " { \\phinoDataize{ [[ B ]] } }" , " { \\varnothing }" , " { }" , " { }" , "\\phinoDataizationRule{bott}" - , " { \\mathbb{D}( T ) }" + , " { \\phinoDataize{ T } }" , " { \\varnothing }" , " { }" , " { }" , "\\phinoDataizationRule{norm}" - , " { \\mathbb{D}( n ) }" - , " { \\mathbb{D}( \\mathbb{M}( n ) ) }" + , " { \\phinoDataize{ n } }" + , " { \\phinoDataize{ \\phinoMorph{ n } } }" , " { }" , " { }" ] diff --git a/test/ConditionSpec.hs b/test/ConditionSpec.hs --- a/test/ConditionSpec.hs +++ b/test/ConditionSpec.hs @@ -19,6 +19,7 @@ [ "in (!t, !B)" , " not (in (!t1, !B)) " , "eq(1, 1)" + , "gt(domain(!B), !i)" , "or(eq(!i,1),eq(length(!B),-2),eq(!e1,!e2),eq(!t1,x),eq(Q.org.eolang,[[ x -> 2 ]]))" , "nf([[ x -> !e ]].x)" , "absolute(!e1)" @@ -34,6 +35,7 @@ , ("eq(1,-2)", Y.Eq (Y.CmpNum (Y.Literal 1)) (Y.CmpNum (Y.Literal (-2)))) , ("eq(!i,length(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i")) (Y.CmpNum (Y.Length (BiMeta "B1")))) , ("eq(!i2,domain(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i2")) (Y.CmpNum (Y.Domain (BiMeta "B1")))) + , ("gt(domain(!B1),!i)", Y.Gt (Y.CmpNum (Y.Domain (BiMeta "B1"))) (Y.CmpNum (Y.MetaIndex "i"))) , ("eq(!t1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "t1")) (Y.CmpExpr (ExMeta "e2"))) , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (ExMeta "e1"), Y.NF (ExDispatch ExRoot (AtLabel "x"))]) , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")]) diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs --- a/test/ParserSpec.hs +++ b/test/ParserSpec.hs @@ -43,7 +43,7 @@ [ ("Q.!t", Just (ExDispatch ExRoot (AtMeta "t"))) , ("[[]](!t1 -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtMeta "t1") ExXi))) , - ( "[[]](a0 -> $)(a11 -> Q)" + ( "[[]](~0 -> $)(~11 -> Q)" , Just ( ExApplication ( ExApplication @@ -192,7 +192,7 @@ , "[[x() -> [[]] ]]" , "Q.x(y() -> [[]])" , "Q.x(y(q) -> [[w -> !e]])" - , "Q.x(a1(^,@) -> [[]])" + , "Q.x(~1(^,@) -> [[]])" , "Q.x.^.@.!t0" , "[[x -> y.z]]" , "[[x -> ^, y -> @, z -> !t]]" @@ -225,7 +225,7 @@ , "Q.x(x -> ?)" , "Q.x(L> Func)" , "Q.x(D> --)" - , "Q.x(a1 -> ?)" + , "Q.x(~1 -> ?)" , "Q.x(L> !F)" , "Q.x(D> !b)" , "[[Ξ±0 -> Q.x]]" @@ -235,7 +235,7 @@ , "Q.x(y(Ξ±1) -> [[]])" , "Q.x(1, 2, !B)" , "Q.x.Ξ±0" - , "Q.x(a1 -> Q.y, x -> 5, !B1)" + , "Q.x(~1 -> Q.y, x -> 5, !B1)" , "Q.x(𝐡1, 𝜏0 -> $, x -> 𝑒)" , "[[ x -> \"\\uD800\"]]" , "[[ x -> \"\\uDFFF\"]]" @@ -349,6 +349,9 @@ , ("a123", Just (AtLabel "a123")) , ("Ξ±0", Nothing) , ("Ξ±42", Nothing) + , ("~0", Nothing) + , ("~1", Nothing) + , ("~123", Nothing) , ("X", Nothing) , ("123", Nothing) , ("", Nothing) @@ -464,8 +467,9 @@ , ("[[]](Q, T)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) ExRoot)) (ArAlpha (Alpha 1) ExTermination))) , ("Q.x(y -> $)", Just (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") ExXi))) , ("[[x -> ?]].x(Q)", Just (ExApplication (ExDispatch (ExFormation [BiVoid (AtLabel "x"), BiVoid AtRho]) (AtLabel "x")) (ArAlpha (Alpha 0) ExRoot))) - , ("[[]](a!i -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i") ExXi))) + , ("[[]](~!i -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i") ExXi))) , ("[[]](α𝑖 -> Q)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i") ExRoot))) + , ("Q.foo(a1 -> Q.y)", Just (ExApplication (ExDispatch ExRoot (AtLabel "foo")) (ArTau (AtLabel "a1") (ExDispatch ExRoot (AtLabel "y"))))) -- #875: "a"-prefixed label in argument position is a named binding, not a positional alpha ] describe "parse meta expressions" $