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.76 +cabal install --overwrite-policy=always phino-0.0.77 phino --version ``` @@ -298,10 +298,13 @@ | nf: Expression' # returns True if given expression in normal form # which means that no more other normalization rules # can be applied - | 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. + | absolute: Expression' # returns True if given expression is xi-free, i.e. + # there is no ξ outside of a formation: it is Φ, a + # formation, a dispatch with a xi-free subject, or an + # application with a xi-free subject and argument. + # Combined with a normal-form check by the '𝑘'/'!k' + # meta variable, which ranges over the absolute + # expressions 𝒦 ⊆ 𝒩, used by the Rcopy rule. | matches: # returns True if given expression after dataization - String # matches to given regex - Expression @@ -366,24 +369,6 @@ * `join` - accepts list of bindings and returns list of joined bindings. Duplicated `ρ`, `Δ` and `λ` attributes are ignored, all other duplicated attributes are replaced with unique attributes using `random-tau` function. -* `splice` - accepts three arguments: input bindings `𝐵-in`, a sentinel expression, - and replacement bindings `𝐵-rep`. Returns a new binding group where `𝐵-rep` - is inserted in front of every binding in `𝐵-in` whose value is a formation - with `φ` equal to the sentinel. Every spliced copy of `𝐵-rep` has its - `τ`-labelled attributes renamed via `random-tau` so the resulting binding - group has no duplicates. `𝐵-rep` must contain only `τ`-labelled bindings - (`BiTau (AtLabel _) _` or `BiVoid (AtLabel _)`); any `ρ`, `Δ`, `λ`, `φ`, - `α`, or meta-attribute binding in `𝐵-rep` makes the function fail fast - because such bindings cannot be renamed and would produce duplicates - when spliced at more than one position. When no binding matches the - sentinel, the output equals the input unchanged. -* `graft` - same call shape as `splice` (`𝐵-in`, sentinel, `𝐵-rep`) and the - same renaming guarantees, but every matched sentinel binding is replaced by - the renamed copy of `𝐵-rep` instead of preserved in place. Use it when the - marker must not survive the substitution — for example, when fusing two - bodies that both produce the same effect and the original marker would fire - a second time. When no binding matches the sentinel, the output equals the - input unchanged. ## Meta variables @@ -397,6 +382,10 @@ * `!n` || `𝑛` - any expression that is already in normal form (behaves like `!e`/`𝑒`, but only binds a sub-expression in NF, so no explicit `nf:` guard is needed) +* `!k` || `𝑘` - any expression that is absolute, i.e. xi-free and in normal + form (ranges over `𝒦 ⊆ 𝒩`); behaves like `!e`/`𝑒` but only + binds an absolute sub-expression, so no explicit `absolute:` + 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 @@ -430,55 +419,55 @@ === parse/phi === warmup: 3 iterations batches: 10 x 1 - total: 1424805.977 μs - avg: 142480.598 μs - min: 127610.262 μs - max: 174684.935 μs - std dev: 17290.645 μs + total: 1453423.801 μs + avg: 145342.380 μs + min: 132303.541 μs + max: 180063.070 μs + std dev: 17728.265 μs === parse/xmir === warmup: 3 iterations batches: 10 x 1 - total: 7682830.477 μs - avg: 768283.048 μs - min: 705792.212 μs - max: 854675.506 μs - std dev: 39610.459 μs + total: 7722131.410 μs + avg: 772213.141 μs + min: 693107.857 μs + max: 828732.420 μs + std dev: 38785.881 μs === rewrite/normalize === warmup: 3 iterations batches: 10 x 1 - total: 385725.280 μs - avg: 38572.528 μs - min: 37709.086 μs - max: 40438.410 μs - std dev: 706.313 μs + total: 639905.274 μs + avg: 63990.527 μs + min: 45971.308 μs + max: 73170.128 μs + std dev: 7936.545 μs === print/sweet/multiline === warmup: 3 iterations batches: 10 x 1 - total: 4012945.140 μs - avg: 401294.514 μs - min: 394876.422 μs - max: 410082.600 μs - std dev: 5070.401 μs + total: 4161166.958 μs + avg: 416116.696 μs + min: 396490.037 μs + max: 440928.823 μs + std dev: 13277.332 μs === print/sweet/flat === warmup: 3 iterations batches: 10 x 1 - total: 3898651.004 μs - avg: 389865.100 μs - min: 364531.311 μs - max: 403024.894 μs - std dev: 13855.156 μs + total: 4101875.046 μs + avg: 410187.505 μs + min: 389712.342 μs + max: 421958.218 μs + std dev: 11340.723 μs === print/salty/multiline === warmup: 3 iterations batches: 10 x 1 - total: 13604785.574 μs - avg: 1360478.557 μs - min: 1335616.393 μs - max: 1382380.875 μs - std dev: 15958.883 μs + total: 14145704.886 μs + avg: 1414570.489 μs + min: 1375850.741 μs + max: 1454788.955 μs + std dev: 27864.927 μs ``` The results were calculated in [this GHA job][benchmark-gha] -on 2026-06-08 at 20:09, +on 2026-06-10 at 14:25, on Linux with 4 CPUs. @@ -514,4 +503,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/27163743003 +[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/27282978502 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.77 +version: 0.0.78 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at diff --git a/resources/normalize/copy.yaml b/resources/normalize/copy.yaml --- a/resources/normalize/copy.yaml +++ b/resources/normalize/copy.yaml @@ -2,7 +2,5 @@ # SPDX-License-Identifier: MIT --- name: copy -pattern: ⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑛) -result: ⟦ 𝐵1, 𝜏 ↦ 𝑛, 𝐵2 ⟧ -when: - xi-free: 𝑛 +pattern: ⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑘) +result: ⟦ 𝐵1, 𝜏 ↦ 𝑘, 𝐵2 ⟧ diff --git a/src/CST.hs b/src/CST.hs --- a/src/CST.hs +++ b/src/CST.hs @@ -82,6 +82,8 @@ | E' -- e | N -- 𝑛 | N' -- n + | K -- 𝑘 + | K' -- k | A -- a | TAU -- 𝜏 | TAU' -- \tau @@ -219,7 +221,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_ABSOLUTE {expr :: EXPRESSION, belongs :: BELONGING} | CO_NOT {condition :: CONDITION} | CO_COMPARE {left :: COMPARABLE, equal :: EQUAL, right :: COMPARABLE} | CO_MATCHES {regex :: String, expr :: EXPRESSION} @@ -244,6 +246,20 @@ expressionToCST :: Expression -> EXPRESSION expressionToCST = toCST' +-- A number can be rendered with the sweet numeric literal only when it is +-- finite. NaN and the infinities have no such literal — and the bare `show` +-- tokens (`NaN`, `Infinity`, `-Infinity`) would collide with object/function +-- names — so they are kept in their byte form instead. +sweetNumber :: Bytes -> Bool +sweetNumber bts = case btsToNum bts of + Right d -> not (isNaN d || isInfinite d) + Left _ -> True + +-- Whether a data object may be collapsed into its sweet literal form. +sweetCollapsible :: Expression -> Bool +sweetCollapsible (DataNumber bts) = sweetNumber bts +sweetCollapsible _ = True + attributeToCST :: Attribute -> ATTRIBUTE attributeToCST = toCST' @@ -269,11 +285,13 @@ metaTail = T.drop 1 -- The first character of an expression meta name encodes its kind: --- 'n'-prefixed names are normal-form-constrained '𝑛' metas, everything --- else is an ordinary '𝑒' meta. +-- 'n'-prefixed names are normal-form-constrained '𝑛' metas, 'k'-prefixed +-- 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 | otherwise = E -- This class is used to convert AST to CST @@ -312,7 +330,11 @@ withoutLastVoidRho [BiVoid AtRho] = [] withoutLastVoidRho (bd : bds') = bd : withoutLastVoidRho bds' toCST (DataString bts) (tabs, _) = EX_STRING (btsToStr bts) (TAB tabs) [] - toCST (DataNumber bts) (tabs, _) = EX_NUMBER (btsToNum bts) (TAB tabs) [] + -- NaN and the infinities have no sweet numeric literal (and printing the bare + -- `show` tokens would collide with object/function names), so they are left in + -- their byte form `Φ.number(Φ.bytes(⟦ Δ ⤍ … ⟧))` by falling through to the + -- generic application clause below. + toCST (DataNumber bts) (tabs, _) | sweetNumber bts = EX_NUMBER (btsToNum bts) (TAB tabs) [] toCST (ExDispatch ExThis attr) ctx = EX_ATTR (toCST attr ctx) toCST (ExDispatch expr attr) ctx = EX_DISPATCH (toCST expr ctx) NO_SPACE (toCST attr ctx) -- Since we convert AST to CST in sweet notation, here we're trying to get rid of unnecessary rho bindings @@ -331,7 +353,7 @@ next = tabs + 1 (ts', rs) = withoutRhosInPrimitives ex ts obj = ExApplication ex (head' ts') - in if length ts' == 1 && isJust (matchDataObject obj) + in if length ts' == 1 && isJust (matchDataObject obj) && sweetCollapsible obj then applicationToPrimitive obj tabs rs else if null exs @@ -480,6 +502,8 @@ 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.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) toCST (Y.In attr binding) _ = CO_BELONGS (attributeToCST attr) IN (ST_BINDING (bindingsToCST [binding])) toCST (Y.And conds) _ = case conds of @@ -494,7 +518,6 @@ 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.XiFree expr) _ = CO_XIFREE (expressionToCST expr) instance ToCST Y.Comparable COMPARABLE where toCST (Y.CmpAttr attr) _ = CMP_ATTR (attributeToCST attr) diff --git a/src/Condition.hs b/src/Condition.hs --- a/src/Condition.hs +++ b/src/Condition.hs @@ -126,10 +126,10 @@ _ <- rparen return (Y.NF expr) , do - _ <- symbol "xi-free" >> lparen + _ <- symbol "absolute" >> lparen expr <- _expression phiParser _ <- rparen - return (Y.XiFree expr) + return (Y.Absolute 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 @@ -32,6 +32,7 @@ toASCII EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toASCII expr) space eol tab (toASCII taus) eol' tab' indent 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{..} = 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) @@ -94,7 +95,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_ABSOLUTE{..} = CO_ABSOLUTE (toASCII expr) belongs 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 @@ -17,7 +17,7 @@ import Matcher import Misc import Parser (parseAttributeThrows, parseNumberThrows) -import Printer (printAttribute, printBinding, printExpression, printExtraArg) +import Printer (printAttribute, printExpression, printExtraArg) import Random (randomString) import Regexp import Tau (freshTau) @@ -49,8 +49,6 @@ buildTerm' "number" = _number buildTerm' "sum" = _sum buildTerm' "join" = _join -buildTerm' "splice" = _splice -buildTerm' "graft" = _graft buildTerm' func = _unsupported func argToBytes :: Y.ExtraArgument -> Subst -> IO Bytes @@ -233,64 +231,6 @@ case term of TeAttribute attr' -> pure attr' _ -> throwIO (userError "random-tau() did not return an attribute, internal invariant violated") - -_splice :: BuildTermMethod -_splice = _spliceLike "splice" True - -_graft :: BuildTermMethod -_graft = _spliceLike "graft" False - -_spliceLike :: String -> Bool -> BuildTermMethod -_spliceLike name keepMarker [Y.ArgBinding inArg, Y.ArgExpression sentExpr, Y.ArgBinding repArg] subst = do - inBds <- buildBindingThrows inArg subst - repBds <- buildBindingThrows repArg subst - mapM_ validateRep repBds - sentinel <- buildExpressionThrows sentExpr subst - result <- walk inBds sentinel repBds - pure (TeBindings result) - where - validateRep :: Binding -> IO () - validateRep (BiTau (AtLabel _) _) = pure () - validateRep (BiVoid (AtLabel _)) = pure () - validateRep bd = - throwIO - ( userError - ( printf - "Function %s() can only rename τ-labelled bindings in the replacement group, but got '%s' which would produce duplicates when applied at more than one position" - name - (printBinding bd) - ) - ) - walk :: [Binding] -> Expression -> [Binding] -> IO [Binding] - walk [] _ _ = pure [] - walk (bd : rest) sent rep - | matches sent bd = do - fresh <- traverse renamed rep - tail' <- walk rest sent rep - pure (fresh ++ (if keepMarker then bd : tail' else tail')) - | otherwise = do - tail' <- walk rest sent rep - pure (bd : tail') - matches :: Expression -> Binding -> Bool - matches sent (BiTau _ (ExFormation bds)) = any (isPhi sent) bds - matches _ _ = False - isPhi :: Expression -> Binding -> Bool - isPhi sent (BiTau AtPhi expr) = expr == sent - isPhi _ _ = False - renamed :: Binding -> IO Binding - renamed (BiTau (AtLabel _) expr) = do - term <- _randomTau [] subst - case term of - TeAttribute attr -> pure (BiTau attr expr) - _ -> throwIO (userError (printf "Failed to generate fresh tau attribute for %s" name)) - renamed (BiVoid (AtLabel _)) = do - term <- _randomTau [] subst - case term of - TeAttribute attr -> pure (BiVoid attr) - _ -> throwIO (userError (printf "Failed to generate fresh tau attribute for %s" name)) - renamed bd = pure bd -_spliceLike name _ _ _ = - throwIO (userError (printf "Function %s() requires exactly 3 arguments: input bindings, sentinel expression, replacement bindings" name)) _unsupported :: BuildTermFunc _unsupported func _ _ = throwIO (userError (printf "Function %s() is not supported or does not exist" func)) diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -266,6 +266,7 @@ instance ToLaTeX META_HEAD where toLaTeX E = E' toLaTeX N = N' + toLaTeX K = K' toLaTeX A = TAU' toLaTeX TAU = TAU' toLaTeX B = B' @@ -311,7 +312,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_ABSOLUTE{..} = CO_ABSOLUTE (toLaTeX expr) belongs 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 @@ -77,7 +77,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_ABSOLUTE{..} = CO_ABSOLUTE (toSingleLine expr) belongs 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/Misc.hs b/src/Misc.hs --- a/src/Misc.hs +++ b/src/Misc.hs @@ -304,6 +304,12 @@ -- Left 42 -- >>> btsToNum (BtMany ["40", "45"]) -- Expected 8 bytes for conversion, got 2 +-- >>> btsToNum (BtMany ["7F", "F8", "00", "00", "00", "00", "00", "00"]) +-- Right NaN +-- >>> btsToNum (BtMany ["7F", "F0", "00", "00", "00", "00", "00", "00"]) +-- Right Infinity +-- >>> btsToNum (BtMany ["FF", "F0", "00", "00", "00", "00", "00", "00"]) +-- Right (-Infinity) btsToNum :: Bytes -> Either Int Double btsToNum hx = let bytes = btsToWord8 hx @@ -312,9 +318,11 @@ else let word = toWord64BE bytes val = wordToDouble word - in case properFraction val of - (n, 0.0) -> Left n - _ -> Right val + in if isNaN val || isInfinite val + then Right val + else case properFraction val of + (n, 0.0) -> Left n + _ -> Right val where toWord64BE :: [Word8] -> Word64 toWord64BE [a, b, c, d, e, f, g, h] = diff --git a/src/Parser.hs b/src/Parser.hs --- a/src/Parser.hs +++ b/src/Parser.hs @@ -386,6 +386,7 @@ , lexeme (DataString . strToBts <$> quotedStr) , try (ExMeta <$> meta' 'e' "𝑒") , try (ExMeta <$> meta' 'n' "𝑛") + , try (ExMeta <$> meta' 'k' "𝑘") , ExDispatch ExThis <$> attribute ] "expression head" diff --git a/src/Render.hs b/src/Render.hs --- a/src/Render.hs +++ b/src/Render.hs @@ -115,6 +115,8 @@ render E' = "e" render N = "𝑛" render N' = "n" + render K = "𝑘" + render K' = "k" render A = "a" render TAU = "𝜏" render TAU' = "\\tau" @@ -248,7 +250,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_ABSOLUTE{..} = render expr <> " " <> render belongs <> " \\mathcal{K}" render CO_NOT{..} = renderFunc "not" condition render CO_COMPARE{..} = render left <> " " <> render equal <> " " <> render right render CO_MATCHES{..} = "matches( " <> T.pack regex <> ", " <> render expr <> " )" diff --git a/src/Rule.hs b/src/Rule.hs --- a/src/Rule.hs +++ b/src/Rule.hs @@ -175,19 +175,24 @@ _ -> pure [] _nf expr subst ctx = pure [subst | isNF expr 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 +-- An expression is xi-free when it contains no ξ outside of a formation: it is +-- Φ, a formation, a dispatch with a xi-free subject, or an application with a +-- xi-free subject and argument. Together with a normal-form check this is what +-- makes an expression absolute (𝒦 ⊆ 𝒩); the '𝑘' meta-variable applies this +-- xi-free check first (cheap, structural, rules out the ξ-recursion the +-- normal-form check could loop on) and the normal-form check second. +_absolute :: Expression -> Subst -> RuleContext -> IO [Subst] +_absolute (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of + Just (MvExpression expr) -> _absolute expr (Subst mp) ctx _ -> pure [] -_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)] -_xiFree (ExDispatch expr _) subst ctx = _xiFree expr subst ctx -_xiFree _ _ _ = pure [] +_absolute expr subst _ = pure [subst | xiFree expr] + where + xiFree :: Expression -> Bool + xiFree (ExFormation _) = True + xiFree ExGlobal = True + xiFree (ExApplication e (BiTau _ te)) = xiFree e && xiFree te + xiFree (ExDispatch e _) = xiFree e + xiFree _ = False _matches :: String -> Expression -> Subst -> RuleContext -> IO [Subst] _matches pat (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of @@ -255,7 +260,7 @@ meetCondition' (Y.Alpha attr) = _alpha attr meetCondition' (Y.Eq left right) = _eq left right meetCondition' (Y.NF expr) = _nf expr -meetCondition' (Y.XiFree expr) = _xiFree expr +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 @@ -325,15 +330,16 @@ logDebug "Extra substitutions have been built" pure (catMaybes res) --- Collect the names of NF-constrained expression meta-variables ('𝑛'/'!n') --- used in a pattern. Their names are 'n'-prefixed and live in their own --- key-space, so a pattern may freely mix plain '𝑒' captures with '𝑛' ones. -nfMetaNames :: Expression -> [T.Text] -nfMetaNames = nub . go +-- Collect the names of constrained expression meta-variables with the given +-- one-character prefix used in a pattern. Each kind ('𝑛'/'!n' normal-form, +-- '𝑘'/'!k' absolute) lives in its own 'n'-/'k'-prefixed key-space, so a +-- pattern may freely mix them with plain '𝑒' captures. +metaNamesWithPrefix :: T.Text -> Expression -> [T.Text] +metaNamesWithPrefix prefix = nub . go where go :: Expression -> [T.Text] go (ExMeta mt) - | T.isPrefixOf "n" mt = [mt] + | T.isPrefixOf prefix mt = [mt] | otherwise = [] go (ExFormation bds) = concatMap goBinding bds go (ExApplication e bd) = go e ++ goBinding bd @@ -346,6 +352,12 @@ goBinding (BiTau _ e) = go e goBinding _ = [] +nfMetaNames :: Expression -> [T.Text] +nfMetaNames = metaNamesWithPrefix "n" + +kMetaNames :: Expression -> [T.Text] +kMetaNames = metaNamesWithPrefix "k" + matchExpressionWithRule :: Expression -> Y.Rule -> RuleContext -> IO [Subst] matchExpressionWithRule = matchExpressionBy matchExpression @@ -366,10 +378,14 @@ logDebug (printf "Pattern from rule '%s' was not matched:\n%s" name (printExpression' ptn logPrintConfig)) pure [] else do - inNf <- foldlM (\substs nm -> meetCondition (Y.NF (ExMeta nm)) substs ctx) matched (nfMetaNames ptn) + -- A '𝑘' meta-variable is absolute (𝒦 ⊆ 𝒩): check it is xi-free first + -- (cheap, structural), then fold its name into the same normal-form + -- check used for '𝑛' metas, so 'isNF' is applied in a single place. + inXiFree <- foldlM (\substs nm -> meetCondition (Y.Absolute (ExMeta nm)) substs ctx) matched (kMetaNames ptn) + inNf <- foldlM (\substs nm -> meetCondition (Y.NF (ExMeta nm)) substs ctx) inXiFree (nfMetaNames ptn ++ kMetaNames ptn) if null inNf then do - logDebug "An NF-constrained '𝑛' meta-variable is not in normal form" + logDebug "A '𝑛'/'𝑘' meta-variable is not in normal form, or a '𝑘' meta-variable is not xi-free" pure [] else do when' <- meetMaybeCondition rule.when inNf ctx diff --git a/src/Sugar.hs b/src/Sugar.hs --- a/src/Sugar.hs +++ b/src/Sugar.hs @@ -191,7 +191,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_ABSOLUTE{..} = CO_ABSOLUTE (toSalty expr) belongs 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 @@ -78,14 +78,14 @@ withObject "Condition" ( \v -> do - validateYamlObject v ["and", "or", "not", "alpha", "nf", "xi-free", "eq", "in", "matches", "part-of", "primitive", "disjoint"] + validateYamlObject v ["and", "or", "not", "alpha", "nf", "absolute", "eq", "in", "matches", "part-of", "primitive", "disjoint"] asum [ And <$> v .: "and" , Or <$> v .: "or" , Not <$> v .: "not" , Alpha <$> v .: "alpha" , NF <$> v .: "nf" - , XiFree <$> v .: "xi-free" + , Absolute <$> v .: "absolute" , Primitive <$> v .: "primitive" , do vals <- v .: "disjoint" @@ -168,7 +168,7 @@ | Alpha Attribute | Eq Comparable Comparable | NF Expression - | XiFree Expression + | Absolute Expression | Matches String Expression | PartOf Expression Binding | Primitive Expression diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -927,10 +927,10 @@ [ unlines [ "\\begin{tabular}{rl}" , "\\trrule{copy}" - , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> n ) }" - , " { [[ B_1, \\tau -> n, B_2 ]] }" - , " { if $ \\xifree{ n } $ }" + , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }" + , " { [[ B_1, \\tau -> k, B_2 ]] }" , " { }" + , " { }" , "\\end{tabular}" ] ] @@ -951,9 +951,9 @@ , " { if $ \\indexof{ \\tau_2 } = \\vert \\overline{ B_1 } \\vert $ }" , " { }" , "\\trrule{copy}" - , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> n ) }" - , " { [[ B_1, \\tau -> n, B_2 ]] }" - , " { if $ \\xifree{ n } $ }" + , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }" + , " { [[ B_1, \\tau -> k, B_2 ]] }" + , " { }" , " { }" , "\\trrule{dc}" , " { T ( \\tau -> e ) }" 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-free(!e1)" + , "absolute(!e1)" , "matches(\"hello(\\\"\\u0000)\", !e)" , "part-of ( [[ x -> 1 ]] , !B ) " , "and(not(alpha(!a)),eq(!a,x))" @@ -39,7 +39,7 @@ , ("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-free(!e1), nf(Q.x))", Y.Or [Y.XiFree (ExMeta "e1"), Y.NF (ExDispatch ExGlobal (AtLabel "x"))]) + , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (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/FunctionsSpec.hs b/test/FunctionsSpec.hs --- a/test/FunctionsSpec.hs +++ b/test/FunctionsSpec.hs @@ -6,33 +6,20 @@ module FunctionsSpec where import AST -import Control.Exception (try) -import Control.Monad (void) import Data.Map.Strict qualified as Map -import Data.Text qualified as T import Deps (Term (TeBindings)) import Functions (buildTerm) import Logger (logDebug) import Matcher (MetaValue (MvBindings), Subst (Subst)) import Misc (uniqueBindings') import Printer (printExpression) -import Test.Hspec (Spec, describe, it, shouldBe, shouldSatisfy) +import Test.Hspec (Spec, describe, it, shouldBe) import Text.Printf (printf) -import Yaml (ExtraArgument (ArgBinding, ArgExpression)) - -emit :: Expression -emit = ExDispatch (ExDispatch ExGlobal (AtLabel "hone")) (AtLabel "emit") - -phiBinding :: T.Text -> Expression -> Binding -phiBinding name body = BiTau (AtLabel name) (ExFormation [BiTau AtPhi body]) - -bodyOf :: Binding -> Maybe Expression -bodyOf (BiTau _ (ExFormation [BiTau AtPhi expr])) = Just expr -bodyOf _ = Nothing +import Yaml (ExtraArgument (ArgBinding)) -spec :: Test.Hspec.Spec -spec = describe "Functions" $ do - Test.Hspec.it "contains only unique bindings after 'join'" $ do +spec :: Spec +spec = describe "Functions" $ + it "contains only unique bindings after 'join'" $ do let first = ("B1", MvBindings [BiVoid AtRho, BiDelta BtEmpty, BiTau (AtLabel "x") ExGlobal, BiVoid (AtAlpha 0)]) second = ("B2", MvBindings [BiTau AtRho ExThis, BiLambda "Func", BiDelta (BtOne "00"), BiVoid (AtAlpha 1)]) third = ("B3", MvBindings [BiLambda "Some", BiTau (AtLabel "y") ExThis, BiTau (AtLabel "x") ExThis, BiVoid (AtAlpha 0)]) @@ -41,213 +28,3 @@ bds' <- uniqueBindings' bds logDebug (printf "Joined bindings:\n%s" (printExpression (ExFormation bds'))) length bds' `shouldBe` 9 - Test.Hspec.it "splices replacement in the correct order before every sentinel match" $ do - let foo = ExDispatch ExGlobal (AtLabel "foo") - bar = ExDispatch ExGlobal (AtLabel "bar") - cpsBody = - [ phiBinding "x" foo - , phiBinding "emit1" emit - , phiBinding "y" bar - , phiBinding "emit2" emit - ] - autoBody = - [ phiBinding "add1" foo - , phiBinding "add2" bar - ] - subst = - Subst - ( Map.fromList - [ ("B-in", MvBindings cpsBody) - , ("B-rep", MvBindings autoBody) - ] - ) - TeBindings result <- - buildTerm - "splice" - [ ArgBinding (BiMeta "B-in") - , ArgExpression emit - , ArgBinding (BiMeta "B-rep") - ] - subst - bds <- uniqueBindings' result - logDebug (printf "Spliced bindings:\n%s" (printExpression (ExFormation bds))) - map bodyOf bds - `shouldBe` [ Just foo - , Just foo - , Just bar - , Just emit - , Just bar - , Just foo - , Just bar - , Just emit - ] - Test.Hspec.it "returns the input unchanged when no sentinel match is found" $ do - let foo = ExDispatch ExGlobal (AtLabel "foo") - body = [phiBinding "x" foo, phiBinding "y" foo] - subst = - Subst - ( Map.fromList - [ ("B-in", MvBindings body) - , ("B-rep", MvBindings [phiBinding "z" foo]) - ] - ) - TeBindings result <- - buildTerm - "splice" - [ ArgBinding (BiMeta "B-in") - , ArgExpression emit - , ArgBinding (BiMeta "B-rep") - ] - subst - result `shouldBe` body - Test.Hspec.it "produces only unique attributes for many splice positions" $ do - let foo = ExDispatch ExGlobal (AtLabel "foo") - body = [phiBinding (T.pack ('e' : show i)) emit | i <- [1 .. 5 :: Int]] - rep = [phiBinding "a" foo, phiBinding "b" foo] - subst = - Subst - ( Map.fromList - [ ("B-in", MvBindings body) - , ("B-rep", MvBindings rep) - ] - ) - TeBindings result <- - buildTerm - "splice" - [ ArgBinding (BiMeta "B-in") - , ArgExpression emit - , ArgBinding (BiMeta "B-rep") - ] - subst - bds <- uniqueBindings' result - bds `shouldSatisfy` ((== length body + 5 * length rep) . length) - Test.Hspec.it "fails fast when replacement contains a non-label binding" $ do - let body = [phiBinding "e1" emit, phiBinding "e2" emit] - rep = [phiBinding "a" emit, BiVoid AtRho] - subst = - Subst - ( Map.fromList - [ ("B-in", MvBindings body) - , ("B-rep", MvBindings rep) - ] - ) - outcome <- - try - ( void - ( buildTerm - "splice" - [ ArgBinding (BiMeta "B-in") - , ArgExpression emit - , ArgBinding (BiMeta "B-rep") - ] - subst - ) - ) :: - IO (Either IOError ()) - outcome `shouldSatisfy` isLeft - Test.Hspec.it "grafts replacement in place of every sentinel match" $ do - let foo = ExDispatch ExGlobal (AtLabel "foo") - bar = ExDispatch ExGlobal (AtLabel "bar") - cpsBody = - [ phiBinding "x" foo - , phiBinding "emit1" emit - , phiBinding "y" bar - , phiBinding "emit2" emit - ] - autoBody = - [ phiBinding "add1" foo - , phiBinding "add2" bar - ] - subst = - Subst - ( Map.fromList - [ ("B-in", MvBindings cpsBody) - , ("B-rep", MvBindings autoBody) - ] - ) - TeBindings result <- - buildTerm - "graft" - [ ArgBinding (BiMeta "B-in") - , ArgExpression emit - , ArgBinding (BiMeta "B-rep") - ] - subst - bds <- uniqueBindings' result - logDebug (printf "Grafted bindings:\n%s" (printExpression (ExFormation bds))) - map bodyOf bds - `shouldBe` [ Just foo - , Just foo - , Just bar - , Just bar - , Just foo - , Just bar - ] - Test.Hspec.it "returns the input unchanged when graft finds no sentinel" $ do - let foo = ExDispatch ExGlobal (AtLabel "foo") - body = [phiBinding "x" foo, phiBinding "y" foo] - subst = - Subst - ( Map.fromList - [ ("B-in", MvBindings body) - , ("B-rep", MvBindings [phiBinding "z" foo]) - ] - ) - TeBindings result <- - buildTerm - "graft" - [ ArgBinding (BiMeta "B-in") - , ArgExpression emit - , ArgBinding (BiMeta "B-rep") - ] - subst - result `shouldBe` body - Test.Hspec.it "produces only unique attributes for many graft positions" $ do - let foo = ExDispatch ExGlobal (AtLabel "foo") - body = [phiBinding (T.pack ('e' : show i)) emit | i <- [1 .. 5 :: Int]] - rep = [phiBinding "a" foo, phiBinding "b" foo] - subst = - Subst - ( Map.fromList - [ ("B-in", MvBindings body) - , ("B-rep", MvBindings rep) - ] - ) - TeBindings result <- - buildTerm - "graft" - [ ArgBinding (BiMeta "B-in") - , ArgExpression emit - , ArgBinding (BiMeta "B-rep") - ] - subst - bds <- uniqueBindings' result - bds `shouldSatisfy` ((== 5 * length rep) . length) - Test.Hspec.it "fails fast when graft replacement contains a non-label binding" $ do - let body = [phiBinding "e1" emit, phiBinding "e2" emit] - rep = [phiBinding "a" emit, BiVoid AtRho] - subst = - Subst - ( Map.fromList - [ ("B-in", MvBindings body) - , ("B-rep", MvBindings rep) - ] - ) - outcome <- - try - ( void - ( buildTerm - "graft" - [ ArgBinding (BiMeta "B-in") - , ArgExpression emit - , ArgBinding (BiMeta "B-rep") - ] - subst - ) - ) :: - IO (Either IOError ()) - outcome `shouldSatisfy` isLeft - where - isLeft :: Either a b -> Bool - isLeft (Left _) = True - isLeft _ = False diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs --- a/test/ParserSpec.hs +++ b/test/ParserSpec.hs @@ -57,6 +57,8 @@ , ("[[!B, !B1]]", Just (ExFormation [BiMeta "B", BiMeta "B1"])) , ("[[!B2, !a2 -> $]]", Just (ExFormation [BiMeta "B2", BiTau (AtMeta "a2") ExThis])) , ("!e0", Just (ExMeta "e0")) + , ("!k", Just (ExMeta "k")) + , ("[[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 ExGlobal "t")) diff --git a/test/PrinterSpec.hs b/test/PrinterSpec.hs --- a/test/PrinterSpec.hs +++ b/test/PrinterSpec.hs @@ -1,4 +1,5 @@ {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT @@ -14,6 +15,8 @@ import Encoding (Encoding (..)) import Lining (LineFormat (..)) import Margin (defaultMargin) +import Misc (pattern DataNumber) +import Parser (parseExpression) import Printer import Sugar (SugarType (..)) import Test.Hspec (Spec, describe, it, shouldBe, shouldContain) @@ -60,6 +63,22 @@ ] ( \(desc, expr, expected) -> it desc (printExpression' expr (SWEET, ASCII, SINGLELINE, defaultMargin) `shouldBe` expected) + ) + + describe "printExpression keeps special double values in byte form so they re-parse" $ + forM_ + [ ("NaN", BtMany ["7F", "F8", "00", "00", "00", "00", "00", "00"]) + , ("positive infinity", BtMany ["7F", "F0", "00", "00", "00", "00", "00", "00"]) + , ("negative infinity", BtMany ["FF", "F0", "00", "00", "00", "00", "00", "00"]) + ] + ( \(desc, bts) -> + it desc $ do + let expr = DataNumber bts + printed = printExpression' expr (SWEET, ASCII, SINGLELINE, defaultMargin) + -- rendered as Q.number( Q.bytes( [[ D> .. ]] ) ), not a bare literal + printed `shouldContain` "number" + printed `shouldContain` "bytes" + parseExpression printed `shouldBe` Right expr ) describe "printProgram with default config" $