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.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. @@ -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 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.0.73 +version: 0.0.0.74 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at diff --git a/resources/alpha.yaml b/resources/alpha.yaml --- a/resources/alpha.yaml +++ b/resources/alpha.yaml @@ -7,4 +7,4 @@ when: eq: - index: 𝜏2 - - length: 𝐵1 + - domain: 𝐵1 diff --git a/resources/copy.yaml b/resources/copy.yaml --- a/resources/copy.yaml +++ b/resources/copy.yaml @@ -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: 𝑒 diff --git a/src/Builder.hs b/src/Builder.hs --- a/src/Builder.hs +++ b/src/Builder.hs @@ -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) diff --git a/src/CST.hs b/src/CST.hs --- a/src/CST.hs +++ b/src/CST.hs @@ -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 diff --git a/src/Condition.hs b/src/Condition.hs --- a/src/Condition.hs +++ b/src/Condition.hs @@ -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 diff --git a/src/Encoding.hs b/src/Encoding.hs --- a/src/Encoding.hs +++ b/src/Encoding.hs @@ -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) diff --git a/src/Functions.hs b/src/Functions.hs --- a/src/Functions.hs +++ b/src/Functions.hs @@ -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 diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -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) diff --git a/src/Lining.hs b/src/Lining.hs --- a/src/Lining.hs +++ b/src/Lining.hs @@ -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) diff --git a/src/Matcher.hs b/src/Matcher.hs --- a/src/Matcher.hs +++ b/src/Matcher.hs @@ -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 diff --git a/src/Printer.hs b/src/Printer.hs --- a/src/Printer.hs +++ b/src/Printer.hs @@ -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 diff --git a/src/Render.hs b/src/Render.hs --- a/src/Render.hs +++ b/src/Render.hs @@ -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) <> " ) $" diff --git a/src/Rewriter.hs b/src/Rewriter.hs --- a/src/Rewriter.hs +++ b/src/Rewriter.hs @@ -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 diff --git a/src/Rule.hs b/src/Rule.hs --- a/src/Rule.hs +++ b/src/Rule.hs @@ -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) diff --git a/src/Sugar.hs b/src/Sugar.hs --- a/src/Sugar.hs +++ b/src/Sugar.hs @@ -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) diff --git a/src/Yaml.hs b/src/Yaml.hs --- a/src/Yaml.hs +++ b/src/Yaml.hs @@ -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) diff --git a/test/BuilderSpec.hs b/test/BuilderSpec.hs --- a/test/BuilderSpec.hs +++ b/test/BuilderSpec.hs @@ -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 diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -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 }" diff --git a/test/ConditionSpec.hs b/test/ConditionSpec.hs --- a/test/ConditionSpec.hs +++ b/test/ConditionSpec.hs @@ -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)) diff --git a/test/MatcherSpec.hs b/test/MatcherSpec.hs --- a/test/MatcherSpec.hs +++ b/test/MatcherSpec.hs @@ -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) ] ] ) diff --git a/test/PrinterSpec.hs b/test/PrinterSpec.hs --- a/test/PrinterSpec.hs +++ b/test/PrinterSpec.hs @@ -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")