phino 0.0.77 → 0.0.78
raw patch · 20 files changed
+174/−397 lines, 20 files
Files
- README.md +44/−55
- phino.cabal +1/−1
- resources/normalize/copy.yaml +2/−4
- src/CST.hs +29/−6
- src/Condition.hs +2/−2
- src/Encoding.hs +2/−1
- src/Functions.hs +1/−61
- src/LaTeX.hs +2/−1
- src/Lining.hs +1/−1
- src/Misc.hs +11/−3
- src/Parser.hs +1/−0
- src/Render.hs +3/−1
- src/Rule.hs +37/−21
- src/Sugar.hs +1/−1
- src/Yaml.hs +3/−3
- test/CLISpec.hs +6/−6
- test/ConditionSpec.hs +2/−2
- test/FunctionsSpec.hs +5/−228
- test/ParserSpec.hs +2/−0
- test/PrinterSpec.hs +19/−0
README.md view
@@ -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. <!-- benchmark_end -->@@ -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
phino.cabal view
@@ -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 <https://github.com/objectionary/phino#readme>
resources/normalize/copy.yaml view
@@ -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 ⟧
src/CST.hs view
@@ -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)
src/Condition.hs view
@@ -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
src/Encoding.hs view
@@ -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)
src/Functions.hs view
@@ -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))
src/LaTeX.hs view
@@ -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)
src/Lining.hs view
@@ -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)
src/Misc.hs view
@@ -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] =
src/Parser.hs view
@@ -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"
src/Render.hs view
@@ -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 <> " )"
src/Rule.hs view
@@ -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
src/Sugar.hs view
@@ -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)
src/Yaml.hs view
@@ -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
test/CLISpec.hs view
@@ -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 ) }"
test/ConditionSpec.hs view
@@ -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))
test/FunctionsSpec.hs view
@@ -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
test/ParserSpec.hs view
@@ -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"))
test/PrinterSpec.hs view
@@ -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" $