phino 0.0.0.36 → 0.0.0.37

raw patch · 13 files changed

+273/−233 lines, 13 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• phino.cabal +1/−2
• src/Builder.hs +57/−51
• src/CLI.hs +3/−3
• src/Functions.hs +63/−27
• src/Rewriter.hs +38/−25
• src/Rule.hs +88/−58
• src/Term.hs +1/−1
• test/BuilderSpec.hs +8/−8
• test/CLISpec.hs +2/−2
• test/DataizeSpec.hs +2/−2
• test/HLintSpec.hs +0/−48
• test/RewriterSpec.hs +8/−4
• test/RuleSpec.hs +2/−2

@@ -1,7 +1,7 @@ cabal-version:      3.0  name:               phino-version:            0.0.0.36+version:            0.0.0.37 license:            MIT synopsis:           Command-Line Manipulator of 𝜑-Calculus Expressions description:        Please see the README on GitHub at <https://github.com/objectionary/phino#readme>@@ -101,7 +101,6 @@     YamlSpec,     MiscSpec,     XMIRSpec,-    HLintSpec,     DataizeSpec,     Paths_phino   autogen-modules:

@@ -31,33 +31,40 @@ import Yaml (ExtraArgument (..))  data BuildException-  = CouldNotBuildExpression {_expr :: Expression, _subst :: Subst}-  | CouldNotBuildAttribute {_attr :: Attribute, _subst :: Subst}-  | CouldNotBuildBinding {_bd :: Binding, _subst :: Subst}-  | CouldNotBuildBytes {_bts :: Bytes, _subst :: Subst}+  = CouldNotBuildExpression {_expr :: Expression, _meta :: String}+  | CouldNotBuildAttribute {_attr :: Attribute, _meta :: String}+  | CouldNotBuildBinding {_bd :: Binding, _meta :: String}+  | CouldNotBuildBytes {_bts :: Bytes, _meta :: String}   deriving (Exception) +metaMsg :: String -> String+metaMsg = printf "meta '%s' is either does not exist or refers to an inappropriate term"++-- @todo #277:30min Error messages are too verbose. Now, if we can't build expression or binding, we+--  throw an exception and just print whole expression or binding to console.+--  If this elements are big, it's just a mess and error message became unreadable. It would be nice to+--  print expression or binding in some reduce way, removing some parts or printing only first N lines instance Show BuildException where   show CouldNotBuildExpression {..} =     printf-      "Couldn't build given expression with provided substitutions\n--Expression: %s\n--Substitutions: %s"+      "Couldn't build expression, %s\n--Expression: %s"+      (metaMsg _meta)       (prettyExpression _expr)-      (prettySubst _subst)   show CouldNotBuildAttribute {..} =     printf-      "Couldn't build given attribute with provided substitutions\n--Attribute: %s\n--Substitutions: %s"+      "Couldn't build attribute '%s', %s"       (prettyAttribute _attr)-      (prettySubst _subst)+      (metaMsg _meta)   show CouldNotBuildBinding {..} =     printf-      "Couldn't build given binding with provided substitutions\n--Binding: %s\n--Substitutions: %s"+      "Couldn't build binding, %s\n--Binding: %s"+      (metaMsg _meta)       (prettyBinding _bd)-      (prettySubst _subst)   show CouldNotBuildBytes {..} =     printf-      "Couldn't build given bytes with provided substitutions\n--Bytes: %s\n--Substitutions: %s"+      "Couldn't build bytes '%s', %s"       (prettyBytes _bts)-      (prettySubst _subst)+      (metaMsg _meta)  contextualize :: Expression -> Expression -> Program -> Expression contextualize ExGlobal _ (Program expr) = expr@@ -70,47 +77,47 @@       bexpr' = contextualize bexpr context prog    in ExApplication expr' (BiTau attr bexpr') -buildAttribute :: Attribute -> Subst -> Maybe Attribute+buildAttribute :: Attribute -> Subst -> Either String Attribute buildAttribute (AtMeta meta) (Subst mp) = case Map.lookup meta mp of-  Just (MvAttribute attr) -> Just attr-  _ -> Nothing-buildAttribute attr _ = Just attr+  Just (MvAttribute attr) -> Right attr+  _ -> Left meta+buildAttribute attr _ = Right attr -buildBytes :: Bytes -> Subst -> Maybe Bytes+buildBytes :: Bytes -> Subst -> Either String Bytes buildBytes (BtMeta meta) (Subst mp) = case Map.lookup meta mp of-  Just (MvBytes bytes) -> Just bytes-  _ -> Nothing-buildBytes bts _ = Just bts+  Just (MvBytes bytes) -> Right bytes+  _ -> Left meta+buildBytes bts _ = Right bts  -- Build binding -- The function returns [Binding] because the BiMeta is always attached -- to the list of bindings-buildBinding :: Binding -> Subst -> Maybe [Binding]+buildBinding :: Binding -> Subst -> Either String [Binding] buildBinding (BiTau attr expr) subst = do   attribute <- buildAttribute attr subst   (expression, _) <- buildExpression expr subst-  Just [BiTau attribute expression]+  Right [BiTau attribute expression] buildBinding (BiVoid attr) subst = do   attribute <- buildAttribute attr subst-  Just [BiVoid attribute]+  Right [BiVoid attribute] buildBinding (BiMeta meta) (Subst mp) = case Map.lookup meta mp of-  Just (MvBindings bds) -> Just bds-  _ -> Nothing+  Just (MvBindings bds) -> Right bds+  _ -> Left meta buildBinding (BiDelta bytes) subst = do   bts <- buildBytes bytes subst-  Just [BiDelta bts]+  Right [BiDelta bts] buildBinding (BiMetaLambda meta) (Subst mp) = case Map.lookup meta mp of-  Just (MvFunction func) -> Just [BiLambda func]-  _ -> Nothing-buildBinding binding _ = Just [binding]+  Just (MvFunction func) -> Right [BiLambda func]+  _ -> Left meta+buildBinding binding _ = Right [binding]  -- Build bindings that may contain meta binding (BiMeta)-buildBindings :: [Binding] -> Subst -> Maybe [Binding]-buildBindings [] _ = Just []+buildBindings :: [Binding] -> Subst -> Either String [Binding]+buildBindings [] _ = Right [] buildBindings (bd : rest) subst = do   first <- buildBinding bd subst   bds <- buildBindings rest subst-  Just (first ++ bds)+  Right (first ++ bds)  buildExpressionWithTails :: Expression -> [Tail] -> Subst -> Expression buildExpressionWithTails expr [] _ = expr@@ -123,49 +130,48 @@ -- 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 -> Maybe (Expression, Expression)+buildExpression :: Expression -> Subst -> Either String (Expression, Expression) buildExpression (ExDispatch expr attr) subst = do   (dispatched, scope) <- buildExpression expr subst   attr <- buildAttribute attr subst-  return (ExDispatch dispatched attr, scope)+  Right (ExDispatch dispatched attr, scope) buildExpression (ExApplication expr (BiTau battr bexpr)) subst = do   (applied, scope) <- buildExpression expr subst-  [binding] <- buildBinding (BiTau battr bexpr) subst-  Just (ExApplication applied binding, scope)-buildExpression (ExApplication _ _) _ = Nothing+  bds <- buildBinding (BiTau battr bexpr) subst+  Right (ExApplication applied (head bds), scope) buildExpression (ExFormation bds) subst = do   bds' <- buildBindings bds subst-  Just (ExFormation bds', defaultScope)+  Right (ExFormation bds', defaultScope) buildExpression (ExMeta meta) (Subst mp) = case Map.lookup meta mp of-  Just (MvExpression expr scope) -> Just (expr, scope)-  _ -> Nothing+  Just (MvExpression expr scope) -> Right (expr, scope)+  _ -> Left meta buildExpression (ExMetaTail expr meta) subst = do   let (Subst mp) = subst   (expression, scope) <- buildExpression expr subst   case Map.lookup meta mp of-    Just (MvTail tails) -> Just (buildExpressionWithTails expression tails subst, scope)-    _ -> Nothing-buildExpression expr _ = Just (expr, defaultScope)+    Just (MvTail tails) -> Right (buildExpressionWithTails expression tails subst, scope)+    _ -> Left meta+buildExpression expr _ = Right (expr, defaultScope)  buildBytesThrows :: Bytes -> Subst -> IO Bytes buildBytesThrows bytes subst = case buildBytes bytes subst of-  Just bts -> pure bts-  _ -> throwIO (CouldNotBuildBytes bytes subst)+  Right bts -> pure bts+  Left meta -> throwIO (CouldNotBuildBytes bytes meta)  buildBindingThrows :: Binding -> Subst -> IO [Binding] buildBindingThrows bd subst = case buildBinding bd subst of-  Just bds -> pure bds-  _ -> throwIO (CouldNotBuildBinding bd subst)+  Right bds -> pure bds+  Left meta -> throwIO (CouldNotBuildBinding bd meta)  buildAttributeThrows :: Attribute -> Subst -> IO Attribute buildAttributeThrows attr subst = case buildAttribute attr subst of-  Just attr' -> pure attr'-  _ -> throwIO (CouldNotBuildAttribute attr subst)+  Right attr' -> pure attr'+  Left meta -> throwIO (CouldNotBuildAttribute attr meta)  buildExpressionThrows :: Expression -> Subst -> IO (Expression, Expression) buildExpressionThrows expr subst = case buildExpression expr subst of-  Just built -> pure built-  _ -> throwIO (CouldNotBuildExpression expr subst)+  Right built -> pure built+  Left meta -> throwIO (CouldNotBuildExpression expr meta)  -- Build a several expression from one expression and several substitutions buildExpressions :: Expression -> [Subst] -> IO [(Expression, Expression)]

@@ -17,7 +17,7 @@ import Data.List (intercalate) import Data.Version (showVersion) import Dataize (DataizeContext (DataizeContext), dataize)-import Functions (buildTermFromFunction)+import Functions (buildTerm) import qualified Functions import Logger import Misc (ensuredFile)@@ -186,7 +186,7 @@       input <- readInput inputFile       rules' <- getRules       program <- parseProgram input inputFormat-      rewritten <- rewrite' program rules' (RewriteContext program maxDepth buildTermFromFunction must)+      rewritten <- rewrite' program rules' (RewriteContext program maxDepth buildTerm must)       logDebug (printf "Printing rewritten 𝜑-program as %s" (show outputFormat))       out <- printProgram rewritten outputFormat printMode       putStrLn out@@ -225,7 +225,7 @@       validateMaxDepth maxDepth       input <- readInput inputFile       prog <- parseProgram input inputFormat-      dataized <- dataize prog (DataizeContext prog maxDepth buildTermFromFunction)+      dataized <- dataize prog (DataizeContext prog maxDepth buildTerm)       maybe (throwIO CouldNotDataize) (putStrLn . prettyBytes) dataized   where     validateMaxDepth :: Integer -> IO ()

@@ -3,7 +3,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Functions where+module Functions (buildTerm) where  import Ast import Builder@@ -26,26 +26,44 @@ import Text.Printf (printf) import qualified Yaml as Y +buildTerm :: String -> [Y.ExtraArgument] -> Subst -> Program -> IO Term+buildTerm "contextualize" = _contextualize+buildTerm "scope" = _scope+buildTerm "random-tau" = _randomTau+buildTerm "dataize" = _dataize+buildTerm "concat" = _concat+buildTerm "sed" = _sed+buildTerm "random-string" = _randomString+buildTerm "size" = _size+buildTerm "tau" = _tau+buildTerm "string" = _string+buildTerm "number" = _number+buildTerm func  = _unsupported func+ argToStrBytes :: Y.ExtraArgument -> Subst -> Program -> IO String argToStrBytes (Y.ArgBytes bytes) subst _ = do   bts <- buildBytesThrows bytes subst   pure (btsToUnescapedStr bts) argToStrBytes (Y.ArgExpression expr) subst prog = do-  (TeBytes bts) <- buildTermFromFunction "dataize" [Y.ArgExpression expr] subst prog+  (TeBytes bts) <- _dataize [Y.ArgExpression expr] subst prog   pure (btsToUnescapedStr bts) argToStrBytes arg _ _ = throwIO (userError (printf "Can't extract bytes from given argument: %s" (prettyExtraArg arg))) -buildTermFromFunction :: String -> [Y.ExtraArgument] -> Subst -> Program -> IO Term-buildTermFromFunction "contextualize" [Y.ArgExpression expr, Y.ArgExpression context] subst prog = do+_contextualize :: [Y.ExtraArgument] -> Subst -> Program -> IO Term+_contextualize [Y.ArgExpression expr, Y.ArgExpression context] subst prog = do   (expr', _) <- buildExpressionThrows expr subst   (context', _) <- buildExpressionThrows context subst   pure (TeExpression (contextualize expr' context' prog))-buildTermFromFunction "contextualize" _ _ _ = throwIO (userError "Function contextualize() requires exactly 2 arguments as expression")-buildTermFromFunction "scope" [Y.ArgExpression expr] subst _ = do-  (expr', scope) <- buildExpressionThrows expr subst+_contextualize _ _ _ = throwIO (userError "Function contextualize() requires exactly 2 arguments as expression")++_scope :: [Y.ExtraArgument] -> Subst -> Program -> IO Term+_scope [Y.ArgExpression expr] subst _ = do+  (_, scope) <- buildExpressionThrows expr subst   pure (TeExpression scope)-buildTermFromFunction "scope" _ _ _ = throwIO (userError "Function scope() requires exactly 1 argument as expression")-buildTermFromFunction "random-tau" args subst _ = do+_scope _ _ _ = throwIO (userError "Function scope() requires exactly 1 argument as expression")++_randomTau :: [Y.ExtraArgument] -> Subst -> Program -> IO Term+_randomTau args subst _ = do   attrs <- argsToAttrs args   tau <- randomTau attrs   pure (TeAttribute (AtLabel tau))@@ -76,19 +94,25 @@     randomTau attrs = do       tau <- randomString "a🌵%d"       if tau `elem` attrs then randomTau attrs else pure tau-buildTermFromFunction "dataize" [Y.ArgBytes bytes] subst _ = do++_dataize :: [Y.ExtraArgument] -> Subst -> Program -> IO Term+_dataize [Y.ArgBytes bytes] subst _ = do   bts <- buildBytesThrows bytes subst   pure (TeBytes bts)-buildTermFromFunction "dataize" [Y.ArgExpression expr] subst _ = do+_dataize [Y.ArgExpression expr] subst _ = do   (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")-buildTermFromFunction "dataize" _ _ _ = throwIO (userError "Function dataize() requires exactly 1 argument as expression")-buildTermFromFunction "concat" args subst prog = do+_dataize _ _ _ = throwIO (userError "Function dataize() requires exactly 1 argument as expression or bytes")++_concat :: [Y.ExtraArgument] -> Subst -> Program -> IO Term+_concat args subst prog = do   args' <- traverse (\arg -> argToStrBytes arg subst prog) args   pure (TeExpression (DataString (strToBts (concat args'))))-buildTermFromFunction "sed" args subst prog = do++_sed :: [Y.ExtraArgument] -> Subst -> Program -> IO Term+_sed args subst prog = do   when (length args < 2) (throwIO (userError "Function sed() requires at least two arguments"))   args' <-     traverse@@ -131,21 +155,29 @@             Nothing -> (if escape then acc else B.snoc acc '\\', B.empty)         | h == '/' -> (acc, rest)         | otherwise -> nextUntilSlash rest (B.snoc acc h) escape-buildTermFromFunction "random-string" [arg] subst prog = do++_randomString :: [Y.ExtraArgument] -> Subst -> Program -> IO Term+_randomString [arg] subst prog = do   pat <- argToStrBytes arg subst prog   str <- randomString pat   pure (TeExpression (DataString (strToBts str)))-buildTermFromFunction "random-string" _ _ _ = throwIO (userError "Function random-string() requires exactly 1 dataizable argument")-buildTermFromFunction "size" [Y.ArgBinding (BiMeta meta)] subst _ = do+_randomString _ _ _ = throwIO (userError "Function random-string() requires exactly 1 dataizable argument")++_size :: [Y.ExtraArgument] -> Subst -> Program -> IO Term+_size [Y.ArgBinding (BiMeta meta)] subst _ = do   bds <- buildBindingThrows (BiMeta meta) subst   pure (TeExpression (DataNumber (numToBts (fromIntegral (length bds)))))-buildTermFromFunction "size" _ _ _ = throwIO (userError "Function size() requires exactly 1 meta binding")-buildTermFromFunction "tau" [Y.ArgExpression expr] subst prog = do-  TeBytes bts <- buildTermFromFunction "dataize" [Y.ArgExpression expr] subst prog+_size _ _ _ = throwIO (userError "Function size() requires exactly 1 meta binding")++_tau :: [Y.ExtraArgument] -> Subst -> Program -> IO Term+_tau [Y.ArgExpression expr] subst prog = do+  TeBytes bts <- _dataize [Y.ArgExpression expr] subst prog   attr <- parseAttributeThrows (btsToUnescapedStr bts)   pure (TeAttribute attr)-buildTermFromFunction "tau" _ _ _ = throwIO (userError "Function tau() requires exactly 1 argument as expression")-buildTermFromFunction "string" [Y.ArgExpression expr] subst _ = do+_tau _ _ _ = throwIO (userError "Function tau() requires exactly 1 argument as expression")++_string :: [Y.ExtraArgument] -> Subst -> Program -> IO Term+_string [Y.ArgExpression expr] subst _ = do   (expr', _) <- buildExpressionThrows expr subst   str <- case expr' of     DataNumber bts -> pure (DataString (strToBts (either show show (btsToNum bts))))@@ -159,16 +191,20 @@             )         )   pure (TeExpression str)-buildTermFromFunction "string" [Y.ArgAttribute attr] subst _ = do+_string [Y.ArgAttribute attr] subst _ = do   attr' <- buildAttributeThrows attr subst   pure (TeExpression (DataString (strToBts (prettyAttribute attr'))))-buildTermFromFunction "string" _ _ _ = throwIO (userError "Function string() requires exactly 1 argument as attribute or data expression (Φ̇.number or Φ̇.string)")-buildTermFromFunction "number" [Y.ArgExpression expr] subst _ = do+_string _ _ _ = throwIO (userError "Function string() requires exactly 1 argument as attribute or data expression (Φ̇.number or Φ̇.string)")++_number :: [Y.ExtraArgument] -> Subst -> Program -> IO Term+_number [Y.ArgExpression expr] subst _ = do   (expr', _) <- buildExpressionThrows expr subst   case expr' of     DataString bts -> do       num <- parseNumberThrows (btsToUnescapedStr bts)       pure (TeExpression num)     _ -> throwIO (userError (printf "Function number() expects expression to be 'Φ̇.string', but got:\n%s" (prettyExpression' expr')))-buildTermFromFunction "number" _ _ _ = throwIO (userError "Function number() requires exactly 1 argument as 'Φ̇.string'")-buildTermFromFunction func _ _ _ = throwIO (userError (printf "Function %s() is not supported or does not exist" func))+_number _ _ _ = throwIO (userError "Function number() requires exactly 1 argument as 'Φ̇.string'")++_unsupported :: String -> [Y.ExtraArgument] -> Subst -> Program -> IO Term+_unsupported func _ _ _ = throwIO (userError (printf "Function %s() is not supported or does not exist" func))

@@ -19,7 +19,7 @@ import Parser (parseProgram, parseProgramThrows) import Pretty (PrintMode (SWEET), prettyAttribute, prettyBytes, prettyExpression, prettyExpression', prettyProgram, prettyProgram', prettySubsts) import Replacer (replaceProgram, replaceProgramThrows)-import Rule (RuleContext (RuleContext), meetMaybeCondition)+import Rule (RuleContext (RuleContext), matchProgramWithRule) import qualified Rule as R import Term import Text.Printf@@ -63,29 +63,42 @@ rewrite :: Program -> [Y.Rule] -> RewriteContext -> IO Program rewrite program [] _ = pure program rewrite program (rule : rest) ctx = do-  let ruleName = fromMaybe "unknown" (Y.name rule)-      ptn = Y.pattern rule-      res = Y.result rule-  matched <- R.matchProgramWithRule program rule (RuleContext (_program ctx) (_buildTerm ctx))-  prog <--    if null matched-      then pure program-      else do-        logDebug (printf "Rule '%s' has been matched, applying..." ruleName)-        prog' <- buildAndReplace program ptn res matched-        if program == prog'-          then logDebug (printf "Applied '%s', no changes made" ruleName)-          else-            logDebug-              ( printf-                  "Applied '%s' (%d nodes -> %d nodes):\n%s"-                  ruleName-                  (countNodes program)-                  (countNodes prog')-                  (prettyProgram' prog' SWEET)-              )-        pure prog'+  prog <- _rewrite program 1   rewrite prog rest ctx+  where+    _rewrite :: Program -> Integer -> IO Program+    _rewrite prog count =+      let ruleName = fromMaybe "unknown" (Y.name rule)+          ptn = Y.pattern rule+          res = Y.result rule+          depth = _maxDepth ctx+       in if count - 1 == depth+            then do+              logDebug (printf "Max amount of rewriting cycles (%d) for rule '%s' has been reached, rewriting is stopped" depth ruleName)+              pure prog+            else do+              logDebug (printf "Starting rewriting cycle for rule '%s': %d out of %d" ruleName count depth)+              matched <- R.matchProgramWithRule prog rule (RuleContext (_program ctx) (_buildTerm ctx))+              if null matched+                then do+                  logDebug (printf "Rule '%s' does not match, rewriting is stopped" ruleName)+                  pure prog+                else do+                  logDebug (printf "Rule '%s' has been matched, applying..." ruleName)+                  prog' <- buildAndReplace prog ptn res matched+                  if prog == prog'+                    then do+                      logDebug (printf "Applied '%s', no changes made" ruleName)+                      pure prog+                    else do+                      logDebug+                        ( printf+                            "Applied '%s' (%d nodes -> %d nodes)"+                            ruleName+                            (countNodes prog)+                            (countNodes prog')+                        )+                      _rewrite prog' (count + 1)  -- @todo #169:30min Memorize previous rewritten programs. Right now in order not to --  get an infinite recursion during rewriting we just count have many times we apply@@ -106,10 +119,10 @@         else           if count - 1 == depth             then do-              logDebug (printf "Max amount of rewriting cycles (%d) has been reached, rewriting is stopped" depth)+              logDebug (printf "Max amount of rewriting cycles for all rules (%d) has been reached, rewriting is stopped" depth)               pure prog             else do-              logDebug (printf "Starting rewriting cycle %d out of %d" count depth)+              logDebug (printf "Starting rewriting cycle for all rules: %d out of %d" count depth)               rewritten <- rewrite prog rules ctx               if rewritten == prog                 then do

@@ -4,7 +4,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Rule where+module Rule (RuleContext (..), isNF, matchProgramWithRule, meetCondition) where  import Ast import Builder (buildAttribute, buildBinding, buildBindingThrows, buildExpression, buildExpressionThrows)@@ -31,30 +31,6 @@     _buildTerm :: BuildTermFunc   } --- Check if given attribute is present in given binding-attrInBindings :: Attribute -> [Binding] -> Bool-attrInBindings attr (bd : bds) = attrInBinding attr bd || attrInBindings attr bds-  where-    attrInBinding :: Attribute -> Binding -> Bool-    attrInBinding attr (BiTau battr _) = attr == battr-    attrInBinding attr (BiVoid battr) = attr == battr-    attrInBinding AtLambda (BiLambda _) = True-    attrInBinding AtDelta (BiDelta _) = True-    attrInBinding _ _ = False-attrInBindings _ _ = False---- Convert Number to Integer-numToInt :: Y.Number -> Subst -> Maybe Integer-numToInt (Y.Ordinal (AtMeta meta)) (Subst mp) = case M.lookup meta mp of-  Just (MvAttribute (AtAlpha idx)) -> Just idx-  _ -> Nothing-numToInt (Y.Ordinal (AtAlpha idx)) subst = Just idx-numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of-  Just (MvBindings bds) -> Just (toInteger (length bds))-  _ -> Nothing-numToInt (Y.Literal num) subst = Just num-numToInt _ _ = Nothing- -- Returns True if given expression matches with any of given normalization rules -- Here we use unsafePerformIO because we're sure that conditions which are used -- in normalization rules doesn't throw an exception.@@ -91,36 +67,70 @@             _ -> False isNF expr ctx = not (matchesAnyNormalizationRule expr ctx) -meetCondition' :: Y.Condition -> Subst -> RuleContext -> IO [Subst]-meetCondition' (Y.Or []) _ _ = pure []-meetCondition' (Y.Or (cond : rest)) subst ctx = do+_or :: [Y.Condition] -> Subst -> RuleContext -> IO [Subst]+_or [] _ _ = pure []+_or (cond : rest) subst ctx = do   met <- meetCondition' cond subst ctx   if null met-    then meetCondition' (Y.Or rest) subst ctx+    then _or rest subst ctx     else pure met-meetCondition' (Y.And []) subst _ = pure [subst]-meetCondition' (Y.And (cond : rest)) subst ctx = do++_and :: [Y.Condition] -> Subst -> RuleContext -> IO [Subst]+_and [] subst _ = pure [subst]+_and (cond : rest) subst ctx = do   met <- meetCondition' cond subst ctx   if null met     then pure []-    else meetCondition' (Y.And rest) subst ctx-meetCondition' (Y.Not cond) subst ctx = do+    else _and rest subst ctx++_not :: Y.Condition -> Subst -> RuleContext -> IO [Subst]+_not cond subst ctx = do   met <- meetCondition' cond subst ctx   pure [subst | null met]-meetCondition' (Y.In attr binding) subst _ =++_in :: Attribute -> Binding -> Subst -> RuleContext -> IO [Subst]+_in attr binding subst _ =   case (buildAttribute attr subst, buildBinding binding subst) of-    (Just attr, Just bds) -> pure [subst | attrInBindings attr bds] -- if attrInBindings attr bd then [subst] else []+    (Right attr, Right bds) -> pure [subst | attrInBindings attr bds] -- if attrInBindings attr bd then [subst] else []     (_, _) -> pure []-meetCondition' (Y.Alpha (AtAlpha _)) subst _ = pure [subst]-meetCondition' (Y.Alpha (AtMeta name)) (Subst mp) _ = case M.lookup name mp of+  where+    -- Check if given attribute is present in given binding+    attrInBindings :: Attribute -> [Binding] -> Bool+    attrInBindings attr (bd : bds) = attrInBinding attr bd || attrInBindings attr bds+      where+        attrInBinding :: Attribute -> Binding -> Bool+        attrInBinding attr (BiTau battr _) = attr == battr+        attrInBinding attr (BiVoid battr) = attr == battr+        attrInBinding AtLambda (BiLambda _) = True+        attrInBinding AtDelta (BiDelta _) = True+        attrInBinding _ _ = False+    attrInBindings _ _ = False++_alpha :: Attribute -> Subst -> RuleContext -> IO [Subst]+_alpha (AtAlpha _) subst _ = pure [subst]+_alpha (AtMeta name) (Subst mp) _ = case M.lookup name mp of   Just (MvAttribute (AtAlpha _)) -> pure [Subst mp]   _ -> pure []-meetCondition' (Y.Alpha _) _ _ = pure []-meetCondition' (Y.Eq (Y.CmpNum left) (Y.CmpNum right)) subst _ = case (numToInt left subst, numToInt right subst) of+_alpha _ _ _ = pure []++_eq :: Y.Comparable -> Y.Comparable -> Subst -> RuleContext -> IO [Subst]+_eq (Y.CmpNum left) (Y.CmpNum right) subst _ = case (numToInt left subst, numToInt right subst) of   (Just left_, Just right_) -> pure [subst | left_ == right_]   (_, _) -> pure []-meetCondition' (Y.Eq (Y.CmpAttr left) (Y.CmpAttr right)) subst _ = pure [subst | compareAttrs left right subst]   where+      -- Convert Number to Integer+    numToInt :: Y.Number -> Subst -> Maybe Integer+    numToInt (Y.Ordinal (AtMeta meta)) (Subst mp) = case M.lookup meta mp of+      Just (MvAttribute (AtAlpha idx)) -> Just idx+      _ -> Nothing+    numToInt (Y.Ordinal (AtAlpha idx)) subst = Just idx+    numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of+      Just (MvBindings bds) -> Just (toInteger (length bds))+      _ -> Nothing+    numToInt (Y.Literal num) subst = Just num+    numToInt _ _ = Nothing+_eq (Y.CmpAttr left) (Y.CmpAttr right) subst _ = pure [subst | compareAttrs left right subst]+  where     compareAttrs :: Attribute -> Attribute -> Subst -> Bool     compareAttrs (AtMeta left) (AtMeta right) (Subst mp) = case (M.lookup left mp, M.lookup right mp) of       (Just (MvAttribute left'), Just (MvAttribute right')) -> compareAttrs left' right' (Subst mp)@@ -132,7 +142,7 @@       Just (MvAttribute found) -> attr == found       _ -> False     compareAttrs left right _ = right == left-meetCondition' (Y.Eq (Y.CmpExpr left) (Y.CmpExpr right)) subst _ = pure [subst | compareExprs left right subst]+_eq (Y.CmpExpr left) (Y.CmpExpr right) subst _ = pure [subst | compareExprs left right subst]   where     compareExprs :: Expression -> Expression -> Subst -> Bool     compareExprs (ExMeta left) (ExMeta right) (Subst mp) = case (M.lookup left mp, M.lookup right mp) of@@ -145,30 +155,38 @@       Just (MvExpression found _) -> expr == found       _ -> False     compareExprs left right _ = left == right-meetCondition' (Y.Eq _ _) _ _ = pure []-meetCondition' (Y.NF (ExMeta meta)) (Subst mp) ctx = case M.lookup meta mp of-  Just (MvExpression expr _) -> pure [Subst mp | isNF expr ctx]+_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   _ -> pure []-meetCondition' (Y.NF expr) (Subst mp) ctx = pure [Subst mp | isNF expr ctx]-meetCondition' (Y.XI (ExMeta meta)) (Subst mp) ctx = case M.lookup meta mp of-  Just (MvExpression expr _) -> meetCondition' (Y.XI expr) (Subst mp) ctx+_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   _ -> pure []-meetCondition' (Y.XI (ExFormation _)) subst _ = pure [subst]-meetCondition' (Y.XI ExThis) subst _ = pure []-meetCondition' (Y.XI ExGlobal) subst _ = pure [subst]-meetCondition' (Y.XI (ExApplication expr (BiTau attr texpr))) subst ctx = do-  onExpr <- meetCondition' (Y.XI expr) subst ctx-  onTau <- meetCondition' (Y.XI texpr) subst ctx+_xi (ExFormation _) subst _ = pure [subst]+_xi ExThis subst _ = pure []+_xi ExGlobal subst _ = pure [subst]+_xi (ExApplication expr (BiTau attr texpr)) subst ctx = do+  onExpr <- _xi expr subst ctx+  onTau <- _xi texpr subst ctx   pure [subst | not (null onExpr) && not (null onTau)]-meetCondition' (Y.XI (ExDispatch expr _)) subst ctx = meetCondition' (Y.XI expr) subst ctx-meetCondition' (Y.Matches pat (ExMeta meta)) (Subst mp) ctx = case M.lookup meta mp of-  Just (MvExpression expr _) -> meetCondition' (Y.Matches pat expr) (Subst mp) ctx+_xi (ExDispatch expr _) subst ctx = _xi expr subst ctx++_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   _ -> pure []-meetCondition' (Y.Matches pat expr) subst ctx = do+_matches pat expr subst ctx = do   (TeBytes tgt) <- _buildTerm ctx "dataize" [Y.ArgExpression expr] subst (Program expr)   matched <- match (B.pack pat) (B.pack (btsToUnescapedStr tgt))   pure [subst | matched]-meetCondition' (Y.PartOf exp bd) subst _ = do++_partOf :: Expression -> Binding -> Subst -> RuleContext -> IO [Subst]+_partOf exp bd subst _ = do   (exp', _) <- buildExpressionThrows exp subst   bds <- buildBindingThrows bd subst   pure [subst | partOf exp' bds]@@ -178,6 +196,18 @@     partOf expr (BiTau _ (ExFormation bds) : rest) = expr == ExFormation bds || partOf expr bds || partOf expr rest     partOf expr (BiTau _ expr' : rest) = expr == expr' || partOf expr rest     partOf expr (bd : rest) = partOf expr rest++meetCondition' :: Y.Condition -> Subst -> RuleContext -> IO [Subst]+meetCondition' (Y.Or conds) = _or conds+meetCondition' (Y.And conds) = _and conds+meetCondition' (Y.Not cond) = _not cond+meetCondition' (Y.In attr binding) = _in attr binding+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.Matches pat expr) = _matches pat expr+meetCondition' (Y.PartOf expr bd) = _partOf expr bd  -- For each substitution check if it meetCondition to given condition -- If substitution does not meet the condition - it's thrown out

@@ -1,7 +1,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT --- The main goal of this module is breking cyclic dependency:+-- The main goal of this module is breaking cyclic dependency: -- Dataize -> Functions -> Rewriter -> Dataize -- Here we provide custom type BuildTermFunc and add it to -- RewriteContext and DataizeContext. Now Dataize and Rewrite depends

@@ -10,7 +10,7 @@ import Matcher import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, anyException, describe, it, shouldBe, shouldThrow) -test :: (Show a, Eq a) => (a -> Subst -> Maybe (a, a)) -> [(String, a, [(String, MetaValue)], Maybe (a, a))] -> SpecWith (Arg Expectation)+test :: (Show a, Eq a) => (a -> Subst -> Either String (a, a)) -> [(String, a, [(String, MetaValue)], Either String (a, a))] -> SpecWith (Arg Expectation) test function useCases =   forM_ useCases $ \(desc, expr, mp, res) ->     it desc $ function expr (Subst (Map.fromList mp)) `shouldBe` res@@ -23,17 +23,17 @@       [ ( "Q.!a => (!a >> x) => Q.x",           ExDispatch ExGlobal (AtMeta "a"),           [("a", MvAttribute (AtLabel "x"))],-          Just (ExDispatch ExGlobal (AtLabel "x"), defaultScope)+          Right (ExDispatch ExGlobal (AtLabel "x"), defaultScope)         ),         ( "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)],-          Just (ExApplication (ExDispatch ExGlobal (AtLabel "c")) (BiTau (AtLabel "x") (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 -> $.x, !B]] => (!a >> y, !B >> [[b -> ?, L> Func]]) => [[y -> $.x, b -> ?, L> Func]]",           ExFormation [BiTau (AtMeta "a") (ExDispatch ExThis (AtLabel "x")), BiMeta "B"],           [("a", MvAttribute (AtLabel "y")), ("B", MvBindings [BiVoid (AtLabel "b"), BiLambda "Func"])],-          Just+          Right             ( ExFormation                 [ BiTau (AtLabel "y") (ExDispatch ExThis (AtLabel "x")),                   BiVoid (AtLabel "b"),@@ -45,12 +45,12 @@         ( "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")))])],-          Just (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"))), defaultScope)         ),         ( "Q.!a => () => X",           ExDispatch ExGlobal (AtMeta "a"),           [],-          Nothing+          Left "a"         ),         ( "!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")),@@ -60,14 +60,14 @@             ("a2", MvAttribute (AtLabel "y")),             ("e2", MvExpression ExThis defaultScope)           ],-          Just (ExApplication (ExApplication (ExFormation []) (BiTau (AtLabel "x") ExGlobal)) (BiTau (AtLabel "y") ExThis), defaultScope)+          Right (ExApplication (ExApplication (ExFormation []) (BiTau (AtLabel "x") ExGlobal)) (BiTau (AtLabel "y") ExThis), defaultScope)         ),         ( "⟦!a ↦ ∅, !B⟧.!a => (!a >> t, !B >> ⟦ x ↦ ξ.t ⟧ ) => ⟦ t ↦ ∅, x ↦ ξ.t ⟧.t",           ExDispatch (ExFormation [BiVoid (AtMeta "a"), BiMeta "B"]) (AtMeta "a"),           [ ("a", MvAttribute (AtLabel "t")),             ("B", MvBindings [BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))])           ],-          Just+          Right             ( ExDispatch                 ( ExFormation                     [ BiVoid (AtLabel "t"),

@@ -178,7 +178,7 @@           ["rewrite", "--nothing", "--output=xmir", "--omit-listing"]           ["<?xml version=\"1.0\" encoding=\"UTF-8\"?>", "<object", "<listing>4 lines of phi</listing>", "  <o base=\"Q.y\" name=\"x\"/>"] -    it "does not fail on exactly 1 rewrtingin" $+    it "does not fail on exactly 1 rewriting" $       withStdin "{⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧}" $         testCLI           ["rewrite", "--rule=test-resources/cli/simple.yaml", "--must=1", "--sweet"]@@ -190,7 +190,7 @@      it "fails with --normalize and --must" $       withStdin "Q -> [[ x -> [[ y -> 5 ]].y ]].x" $-        testCLIFailed ["rewrite", "--normalize", "--must"] "it's expected exactly 1 rewriting cycles happened, but rewriting is still going"+        testCLIFailed ["rewrite", "--max-depth=2", "--normalize", "--must"] "it's expected exactly 1 rewriting cycles happened, but rewriting is still going"    describe "dataize" $ do     it "dataizes simple program" $

@@ -8,10 +8,10 @@ import Dataize (dataize, dataize', morph, DataizeContext (DataizeContext)) import Parser (parseProgramThrows) import Test.Hspec-import Functions (buildTermFromFunction)+import Functions (buildTerm)  defaultDataizeContext :: Program -> DataizeContext-defaultDataizeContext prog = DataizeContext prog 25 buildTermFromFunction+defaultDataizeContext prog = DataizeContext prog 25 buildTerm  test :: (Eq a, Show a) => (Expression -> DataizeContext -> IO (Maybe a)) -> [(String, Expression, Expression, Maybe a)] -> Spec test func useCases =

@@ -1,48 +0,0 @@-{-# LANGUAGE ScopedTypeVariables #-}---- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com--- SPDX-License-Identifier: MIT--module HLintSpec (spec) where--import Control.Exception (try, IOException)-import System.Exit (ExitCode(..))-import System.Process (readProcessWithExitCode)-import Test.Hspec---- | Check if hlint is available on the system-isHLintAvailable :: IO Bool-isHLintAvailable = do-  result <- try (readProcessWithExitCode "hlint" ["--version"] "")-  case result of-    Left (_ :: IOException) -> return False-    Right (ExitSuccess, _, _) -> return True-    Right (ExitFailure _, _, _) -> return False---- | Run hlint on a directory and check for success-runHLintCheck :: String -> IO ()-runHLintCheck dir = do-  available <- isHLintAvailable-  if not available -    then pendingWith "hlint is not available on this system"-    else do-      (exitCode, stdout, stderr) <- readProcessWithExitCode "hlint" [dir] ""-      case exitCode of-        ExitSuccess -> return ()-        ExitFailure _ -> do-          putStrLn $ "HLint warnings/errors in " ++ dir ++ ":"-          putStrLn stdout-          putStrLn stderr-          exitCode `shouldBe` ExitSuccess--spec :: Spec-spec =-  describe "HLint" $ do-    it "should pass hlint check for src/" $-      runHLintCheck "src/"--    it "should pass hlint check for app/" $-      runHLintCheck "app/"-          -    it "should pass hlint check for test/" $-      runHLintCheck "test/"

@@ -12,16 +12,16 @@ import Data.Aeson import Data.Char (isSpace) import Data.Yaml qualified as Yaml+import Functions (buildTerm) import GHC.Generics import Misc (allPathsIn, ensuredFile) import Parser (parseProgramThrows)-import Pretty (prettyProgram', PrintMode (SWEET))+import Pretty (PrintMode (SWEET), prettyProgram')+import Rewriter (RewriteContext (RewriteContext), rewrite') import System.FilePath (makeRelative, replaceExtension, (</>)) import Test.Hspec (Spec, describe, expectationFailure, it, pending, runIO) import Yaml (normalizationRules) import Yaml qualified as Y-import Rewriter (rewrite', RewriteContext (RewriteContext))-import Functions (buildTermFromFunction)  data Rules = Rules   { basic :: Maybe [String],@@ -35,6 +35,7 @@     rules :: Maybe Rules,     skip :: Maybe Bool,     repeat_ :: Maybe Integer,+    must :: Maybe Integer,     normalize :: Maybe Bool   }   deriving (Generic, Show)@@ -72,6 +73,9 @@                   else case repeat_ pack of                     Just num -> num                     _ -> 1+              must' = case must pack of+                Just num -> num+                _ -> 0           case skip pack of             Just True -> pending             _ -> do@@ -92,7 +96,7 @@                   if normalize'                     then pure normalizationRules                     else pure []-              rewritten <- rewrite' program rules' (RewriteContext program repeat' buildTermFromFunction 0)+              rewritten <- rewrite' program rules' (RewriteContext program repeat' buildTerm must')               result' <- parseProgramThrows (output pack)               unless (rewritten == result') $                 expectationFailure

@@ -10,7 +10,7 @@ import Control.Monad import Data.Aeson import Data.Yaml qualified as Y-import Functions (buildTermFromFunction)+import Functions (buildTerm) import GHC.Generics import Matcher import Misc@@ -39,7 +39,7 @@         let prog = Program (expression pack)         let matched = matchProgram (pattern pack) prog         unless (matched /= []) (expectationFailure "List of matched substitutions is empty which is not expected")-        met <- meetCondition (condition pack) matched (RuleContext prog buildTermFromFunction)+        met <- meetCondition (condition pack) matched (RuleContext prog buildTerm)         case failure pack of           Just True ->             unless