phino 0.0.0.23 → 0.0.0.24

raw patch · 11 files changed

+381/−322 lines, 11 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• phino.cabal +3/−3
• src/CLI.hs +12/−2
• src/Condition.hs +0/−191
• src/Dataize.hs +3/−3
• src/Rewriter.hs +64/−75
• src/Rule.hs +236/−0
• src/Yaml.hs +2/−1
• test/CLISpec.hs +12/−0
• test/ConditionSpec.hs +0/−46
• test/RewriterSpec.hs +1/−1
• test/RuleSpec.hs +48/−0

@@ -1,7 +1,7 @@ cabal-version:      3.0  name:               phino-version:            0.0.0.23+version:            0.0.0.24 license:            MIT synopsis:           Command-Line Manipulator of 𝜑-Calculus Expressions description:        Please see the README on GitHub at <https://github.com/objectionary/phino#readme>@@ -32,7 +32,7 @@     Replacer,     Rewriter,     Yaml,-    Condition,+    Rule,     Dataize,     Functions,     Term,@@ -97,7 +97,7 @@     ReplacerSpec,     PrettySpec,     RewriterSpec,-    ConditionSpec,+    RuleSpec,     YamlSpec,     MiscSpec,     XMIRSpec,

@@ -25,7 +25,7 @@ import Options.Applicative import Parser (parseProgramThrows) import Paths_phino (version)-import Pretty (PrintMode (SALTY, SWEET), prettyProgram', prettyBytes)+import Pretty (PrintMode (SALTY, SWEET), prettyBytes, prettyProgram') import Rewriter (RewriteContext (RewriteContext), rewrite') import System.Exit (ExitCode (..), exitFailure) import System.IO (getContents')@@ -74,6 +74,7 @@     shuffle :: Bool,     omitListing :: Bool,     omitComments :: Bool,+    must :: Integer,     maxDepth :: Integer,     inputFile :: Maybe FilePath   }@@ -139,6 +140,9 @@             <*> switch (long "shuffle" <> help "Shuffle rules before applying")             <*> switch (long "omit-listing" <> help "Omit full program listing in XMIR output")             <*> switch (long "omit-comments" <> help "Omit comments in XMIR output")+            <*> ( flag' 1 (long "must" <> help "Enable must-rewrite with default value 1")+                    <|> option auto (long "must" <> metavar "N" <> help "Must-rewrite, stops execution if not exactly N rules applied (default 1 when specified without value, if 0 - flag is disabled)" <> value 0)+                )             <*> optMaxDepth             <*> argInputFile         )@@ -177,11 +181,12 @@   case cmd of     CmdRewrite OptsRewrite {..} -> do       validateMaxDepth maxDepth+      validateMust must       logDebug (printf "Amount of rewriting cycles: %d" maxDepth)       input <- readInput inputFile       rules' <- getRules       program <- parseProgram input inputFormat-      rewritten <- rewrite' program rules' (RewriteContext program maxDepth buildTermFromFunction)+      rewritten <- rewrite' program rules' (RewriteContext program maxDepth buildTermFromFunction must)       logDebug (printf "Printing rewritten 𝜑-program as %s" (show outputFormat))       out <- printProgram rewritten outputFormat printMode       putStrLn out@@ -228,6 +233,11 @@       when         (depth <= 0)         (throwIO (InvalidRewriteArguments "--max-depth must be positive"))+    validateMust :: Integer -> IO ()+    validateMust must =+      when+        (must < 0)+        (throwIO (InvalidRewriteArguments "--must must be positive"))     readInput :: Maybe FilePath -> IO String     readInput inputFile' = case inputFile' of       Just pth -> do

@@ -1,191 +0,0 @@-{-# LANGUAGE OverloadedStrings #-}---- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com--- SPDX-License-Identifier: MIT--module Condition where--import Ast-import Builder (buildAttribute, buildBinding, buildExpression, buildExpressionThrows, buildBindingThrows)-import Control.Exception (SomeException (SomeException), evaluate)-import Control.Exception.Base (try)-import Data.Aeson (FromJSON)-import qualified Data.ByteString.Char8 as B-import qualified Data.Map.Strict as M-import Functions (buildTermFromFunction)-import GHC.IO (unsafePerformIO)-import Logger (logDebug)-import Matcher-import Misc (allPathsIn, btsToUnescapedStr)-import Pretty (prettyExpression, prettySubsts)-import Regexp (match)-import Term (Term (TeBytes))-import Yaml (normalizationRules)-import qualified Yaml as Y---- 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---- Apply 'eq' yaml condition to attributes-compareAttrs :: Attribute -> Attribute -> Subst -> Bool-compareAttrs (AtMeta left) (AtMeta right) _ = left == right-compareAttrs attr (AtMeta meta) (Subst mp) = case M.lookup meta mp of-  Just (MvAttribute found) -> attr == found-  _ -> False-compareAttrs (AtMeta meta) attr (Subst mp) = case M.lookup meta mp of-  Just (MvAttribute found) -> attr == found-  _ -> False-compareAttrs left right subst = right == left---- 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.-matchesAnyNormalizationRule :: Expression -> Bool-matchesAnyNormalizationRule expr = matchesAnyNormalizationRule' expr normalizationRules-  where-    matchesAnyNormalizationRule' :: Expression -> [Y.Rule] -> Bool-    matchesAnyNormalizationRule' _ [] = False-    matchesAnyNormalizationRule' expr (rule : rules) =-      case unsafePerformIO (matchProgramWithCondition (Y.pattern rule) (Y.when rule) (Program expr)) of-        Just matched -> not (null matched) || matchesAnyNormalizationRule' expr rules-        Nothing -> matchesAnyNormalizationRule' expr rules---- Returns True if given expression is in the normal form-isNF :: Expression -> Bool-isNF ExThis = True-isNF ExGlobal = True-isNF ExTermination = True-isNF (ExDispatch ExThis _) = True-isNF (ExDispatch ExGlobal _) = True-isNF (ExDispatch ExTermination _) = False -- dd rule-isNF (ExApplication ExTermination _) = False -- dc rule-isNF (ExFormation []) = True-isNF (ExFormation bds) = normalBindings bds || not (matchesAnyNormalizationRule (ExFormation bds))-  where-    -- Returns True if all given bindings are 100% in normal form-    normalBindings :: [Binding] -> Bool-    normalBindings [] = True-    normalBindings (bd : bds) =-      let next = normalBindings bds-       in case bd of-            BiDelta _ -> next-            BiVoid _ -> next-            BiLambda _ -> next-            _ -> False-isNF expr = not (matchesAnyNormalizationRule expr)--meetCondition' :: Y.Condition -> Subst -> IO [Subst]-meetCondition' (Y.Or []) subst = pure [subst]-meetCondition' (Y.Or (cond : rest)) subst = do-  met <- meetCondition' cond subst-  if null met-    then meetCondition' (Y.Or rest) subst-    else pure met-meetCondition' (Y.And []) subst = pure [subst]-meetCondition' (Y.And (cond : rest)) subst = do-  met <- meetCondition' cond subst-  if null met-    then pure []-    else meetCondition' (Y.And rest) subst-meetCondition' (Y.Not cond) subst = do-  met <- meetCondition' cond subst-  pure [subst | null met]-meetCondition' (Y.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 []-    (_, _) -> pure []-meetCondition' (Y.Alpha (AtAlpha _)) subst = pure [subst]-meetCondition' (Y.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-  (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]-meetCondition' (Y.Eq _ _) _ = pure []-meetCondition' (Y.NF (ExMeta meta)) (Subst mp) = case M.lookup meta mp of-  Just (MvExpression expr _) -> pure [Subst mp | isNF expr]-  _ -> pure []-meetCondition' (Y.NF expr) (Subst mp) = pure [Subst mp | isNF expr]-meetCondition' (Y.XI (ExMeta meta)) (Subst mp) = case M.lookup meta mp of-  Just (MvExpression expr _) -> meetCondition' (Y.XI expr) (Subst mp)-  _ -> 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 = do-  onExpr <- meetCondition' (Y.XI expr) subst-  onTau <- meetCondition' (Y.XI texpr) subst-  pure [subst | not (null onExpr) && not (null onTau)]-meetCondition' (Y.XI (ExDispatch expr _)) subst = meetCondition' (Y.XI expr) subst-meetCondition' (Y.Matches pat (ExMeta meta)) (Subst mp) = case M.lookup meta mp of-  Just (MvExpression expr _) -> meetCondition' (Y.Matches pat expr) (Subst mp)-  _ -> pure []-meetCondition' (Y.Matches pat expr) subst = do-  (TeBytes tgt) <- buildTermFromFunction "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-  (exp', _) <- buildExpressionThrows exp subst-  bds <- buildBindingThrows bd subst-  pure [subst | partOf exp' bds]-  where-    partOf :: Expression -> [Binding] -> Bool-    partOf expr [] = False-    partOf expr (BiTau _ expr' : rest) = expr == expr' || partOf expr rest-    partOf expr (bd : rest) = partOf expr rest---- For each substitution check if it meetCondition to given condition--- If substitution does not meet the condition - it's thrown out--- and is not used in replacement-meetCondition :: Y.Condition -> [Subst] -> IO [Subst]-meetCondition _ [] = pure []-meetCondition cond (subst : rest) = do-  met <- try (meetCondition' cond subst) :: IO (Either SomeException [Subst])-  case met of-    Right first -> do-      next <- meetCondition cond rest-      if null first-        then pure next-        else pure (head first : next)-    Left _ -> meetCondition cond rest---- Returns Just [...] if--- 1. program matches pattern and--- 2.1. condition is not present, or--- 2.2. condition is present and met--- Otherwise returns Nothing-matchProgramWithCondition :: Expression -> Maybe Y.Condition -> Program -> IO (Maybe [Subst])-matchProgramWithCondition ptn condition program =-  let matched = matchProgram ptn program-   in if null matched-        then pure Nothing-        else case condition of-          Nothing -> pure (Just matched)-          Just cond -> do-            met <- meetCondition cond matched-            if null met-              then pure Nothing-              else pure (Just met)

@@ -8,11 +8,11 @@  import Ast import Builder (contextualize)-import Condition (isNF) import Control.Exception (throwIO) import Data.List (partition) import Misc import Rewriter (RewriteContext (RewriteContext), rewrite')+import Rule (RuleContext (RuleContext), isNF) import Term (BuildTermFunc) import Text.Printf (printf) import XMIR (XmirContext (XmirContext))@@ -25,7 +25,7 @@   }  switchContext :: DataizeContext -> RewriteContext-switchContext DataizeContext {..} = RewriteContext _program _maxDepth _buildTerm+switchContext DataizeContext {..} = RewriteContext _program _maxDepth _buildTerm 0  maybeBinding :: (Binding -> Bool) -> [Binding] -> (Maybe Binding, [Binding]) maybeBinding _ [] = (Nothing, [])@@ -115,7 +115,7 @@   case resolved of     Just obj -> morph obj ctx     _ ->-      if isNF expr+      if isNF expr (RuleContext (_program ctx) (_buildTerm ctx))         then pure Nothing         else do           (Program expr') <- rewrite' (Program expr) normalizationRules (switchContext ctx) -- NMZ

@@ -1,3 +1,4 @@+{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE RecordWildCards #-} @@ -8,7 +9,7 @@  import Ast import Builder-import qualified Condition as C+import Control.Exception (Exception, throwIO) import Data.Foldable (foldlM) import qualified Data.Map.Strict as M import Data.Maybe (catMaybes, fromMaybe, isJust)@@ -17,8 +18,10 @@ import Matcher (MetaValue (MvAttribute, MvBindings, MvBytes, MvExpression), Subst (Subst), combine, combineMany, defaultScope, matchProgram, substEmpty, substSingle) import Misc (ensuredFile) import Parser (parseProgram, parseProgramThrows)-import Pretty+import Pretty (PrintMode (SWEET), prettyAttribute, prettyBytes, prettyExpression, prettyExpression', prettyProgram, prettyProgram', prettySubsts) import Replacer (replaceProgram, replaceProgramThrows)+import Rule (RuleContext (RuleContext), meetMaybeCondition)+import qualified Rule as R import Term import Text.Printf import Yaml (ExtraArgument (..))@@ -27,9 +30,28 @@ data RewriteContext = RewriteContext   { _program :: Program,     _maxDepth :: Integer,-    _buildTerm :: BuildTermFunc+    _buildTerm :: BuildTermFunc,+    _must :: Integer   } +data MustException+  = StoppedBefore {must :: Integer, count :: Integer}+  | ContinueAfter {must :: Integer}+  deriving (Exception)++instance Show MustException where+  show StoppedBefore {..} =+    printf+      "With option --must=%d it's expected exactly %d rewriting cycles happened, but rewriting stopped after %d"+      must+      must+      count+  show ContinueAfter {..} =+    printf+      "With option --must=%d it's expected exactly %d rewriting cycles happened, but rewriting is still going"+      must+      must+ -- Build pattern and result expression and replace patterns to results in given program buildAndReplace :: Program -> Expression -> Expression -> [Subst] -> IO Program buildAndReplace program ptn res substs = do@@ -39,70 +61,31 @@       ptns' = map fst ptns   replaceProgramThrows program ptns' repls' --- Extend list of given substitutions with extra substitutions from 'where' yaml rule section-extraSubstitutions :: Maybe [Y.Extra] -> [Subst] -> RewriteContext -> IO [Subst]-extraSubstitutions extras substs RewriteContext {..} = case extras of-  Nothing -> pure substs-  Just extras' -> do-    res <--      sequence-        [ foldlM-            ( \(Just subst') extra -> do-                let maybeName = case Y.meta extra of-                      ArgExpression (ExMeta name) -> Just name-                      ArgAttribute (AtMeta name) -> Just name-                      ArgBinding (BiMeta name) -> Just name-                      ArgBytes (BtMeta name) -> Just name-                      _ -> Nothing-                    func = Y.function extra-                    args = Y.args extra-                term <- _buildTerm func args subst' _program-                meta <- case term of-                  TeExpression expr -> do-                    logDebug (printf "Function %s() returned expression:\n%s" func (prettyExpression' expr))-                    pure (MvExpression expr defaultScope)-                  TeAttribute attr -> do-                    logDebug (printf "Function %s() returned attribute:\n%s" func (prettyAttribute attr))-                    pure (MvAttribute attr)-                  TeBytes bytes -> do-                    logDebug (printf "Function %s() returned bytes: %s" func (prettyBytes bytes))-                    pure (MvBytes bytes)-                case maybeName of-                  Just name -> pure (combine (substSingle name meta) subst')-                  _ -> pure Nothing-            )-            (Just subst)-            extras'-          | subst <- substs-        ]-    pure (catMaybes res)- rewrite :: Program -> [Y.Rule] -> RewriteContext -> IO Program rewrite program [] _ = pure program rewrite program (rule : rest) ctx = do-  let ptn = Y.pattern rule+  let ruleName = fromMaybe "unknown" (Y.name rule)+      ptn = Y.pattern rule       res = Y.result rule-      condition = Y.when rule-  maybeMatched <- C.matchProgramWithCondition ptn condition program-  prog <- case maybeMatched of-    Nothing -> pure program-    Just matched -> do-      let ruleName = fromMaybe "unknown" (Y.name rule)-      logDebug (printf "Rule '%s' has been matched, applying..." ruleName)-      substs <- extraSubstitutions (Y.where_ rule) matched ctx-      prog' <- buildAndReplace program ptn res substs-      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'+  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'   rewrite prog rest ctx  -- @todo #169:30min Memorize previous rewritten programs. Right now in order not to@@ -113,20 +96,26 @@ --  been memorized - we fail because we got into infinite recursion. Ofc we should keep counting --  rewriting cycles if program just only grows on each rewriting. rewrite' :: Program -> [Y.Rule] -> RewriteContext -> IO Program-rewrite' prog rules ctx = _rewrite prog 0+rewrite' prog rules ctx = _rewrite prog 1   where     _rewrite :: Program -> Integer -> IO Program     _rewrite prog count = do       let depth = _maxDepth ctx-      logDebug (printf "Starting rewriting cycle %d out of %d" count depth)-      if count == depth-        then do-          logDebug (printf "Max amount of rewriting cycles has been reached, rewriting is stopped")-          pure prog-        else do-          rewritten <- rewrite prog rules ctx-          if rewritten == prog+          must = _must ctx+      if must /= 0 && count > must+        then throwIO (ContinueAfter must)+        else+          if count - 1 == depth             then do-              logDebug "No rule matched, rewriting is stopped"-              pure rewritten-            else _rewrite rewritten (count + 1)+              logDebug (printf "Max amount of rewriting cycles (%d) has been reached, rewriting is stopped" depth)+              pure prog+            else do+              logDebug (printf "Starting rewriting cycle %d out of %d" count depth)+              rewritten <- rewrite prog rules ctx+              if rewritten == prog+                then do+                  logDebug "No rule matched, rewriting is stopped"+                  if must /= 0 && count /= must+                    then throwIO (StoppedBefore must count)+                    else pure rewritten+                else _rewrite rewritten (count + 1)

@@ -0,0 +1,236 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-}++-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++module Rule where++import Ast+import Builder (buildAttribute, buildBinding, buildBindingThrows, buildExpression, buildExpressionThrows)+import Control.Exception (SomeException (SomeException), evaluate)+import Control.Exception.Base (try)+import Data.Aeson (FromJSON)+import qualified Data.ByteString.Char8 as B+import Data.Foldable (foldlM)+import qualified Data.Map.Strict as M+import Data.Maybe (catMaybes, fromMaybe)+import GHC.IO (unsafePerformIO)+import Logger (logDebug)+import Matcher+import Misc (allPathsIn, btsToUnescapedStr)+import Pretty (prettyAttribute, prettyBytes, prettyExpression, prettyExpression', prettySubsts)+import Regexp (match)+import Term (BuildTermFunc, Term (..))+import Text.Printf (printf)+import Yaml (normalizationRules)+import qualified Yaml as Y++data RuleContext = RuleContext+  { _program :: Program,+    _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++-- Apply 'eq' yaml condition to attributes+compareAttrs :: Attribute -> Attribute -> Subst -> Bool+compareAttrs (AtMeta left) (AtMeta right) _ = left == right+compareAttrs attr (AtMeta meta) (Subst mp) = case M.lookup meta mp of+  Just (MvAttribute found) -> attr == found+  _ -> False+compareAttrs (AtMeta meta) attr (Subst mp) = case M.lookup meta mp of+  Just (MvAttribute found) -> attr == found+  _ -> False+compareAttrs left right subst = right == left++-- 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.+matchesAnyNormalizationRule :: Expression -> RuleContext -> Bool+matchesAnyNormalizationRule expr ctx = matchesAnyNormalizationRule' expr normalizationRules ctx+  where+    matchesAnyNormalizationRule' :: Expression -> [Y.Rule] -> RuleContext -> Bool+    matchesAnyNormalizationRule' _ [] _ = False+    matchesAnyNormalizationRule' expr (rule : rules) ctx =+      let matched = unsafePerformIO (matchProgramWithRule (Program expr) rule ctx)+       in not (null matched) || matchesAnyNormalizationRule' expr rules ctx++-- Returns True if given expression is in the normal form+isNF :: Expression -> RuleContext -> Bool+isNF ExThis _ = True+isNF ExGlobal _ = True+isNF ExTermination _ = True+isNF (ExDispatch ExThis _) _ = True+isNF (ExDispatch ExGlobal _) _ = True+isNF (ExDispatch ExTermination _) _ = False -- dd rule+isNF (ExApplication ExTermination _) _ = False -- dc rule+isNF (ExFormation []) _ = True+isNF (ExFormation bds) ctx = normalBindings bds || not (matchesAnyNormalizationRule (ExFormation bds) ctx)+  where+    -- Returns True if all given bindings are 100% in normal form+    normalBindings :: [Binding] -> Bool+    normalBindings [] = True+    normalBindings (bd : bds) =+      let next = normalBindings bds+       in case bd of+            BiDelta _ -> next+            BiVoid _ -> next+            BiLambda _ -> next+            _ -> False+isNF expr ctx = not (matchesAnyNormalizationRule expr ctx)++meetCondition' :: Y.Condition -> Subst -> RuleContext -> IO [Subst]+meetCondition' (Y.Or []) subst _ = pure [subst]+meetCondition' (Y.Or (cond : rest)) subst ctx = do+  met <- meetCondition' cond subst ctx+  if null met+    then meetCondition' (Y.Or rest) subst ctx+    else pure met+meetCondition' (Y.And []) subst _ = pure [subst]+meetCondition' (Y.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+  met <- meetCondition' cond subst ctx+  pure [subst | null met]+meetCondition' (Y.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 []+    (_, _) -> pure []+meetCondition' (Y.Alpha (AtAlpha _)) subst _ = pure [subst]+meetCondition' (Y.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+  (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]+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]+  _ -> 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+  _ -> 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+  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+  _ -> pure []+meetCondition' (Y.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+  (exp', _) <- buildExpressionThrows exp subst+  bds <- buildBindingThrows bd subst+  pure [subst | partOf exp' bds]+  where+    partOf :: Expression -> [Binding] -> Bool+    partOf expr [] = False+    partOf expr (BiTau _ expr' : rest) = expr == expr' || partOf expr rest+    partOf expr (bd : rest) = partOf expr rest++-- For each substitution check if it meetCondition to given condition+-- If substitution does not meet the condition - it's thrown out+-- and is not used in replacement+meetCondition :: Y.Condition -> [Subst] -> RuleContext -> IO [Subst]+meetCondition _ [] _ = pure []+meetCondition cond (subst : rest) ctx = do+  met <- try (meetCondition' cond subst ctx) :: IO (Either SomeException [Subst])+  case met of+    Right first -> do+      next <- meetCondition cond rest ctx+      if null first+        then pure next+        else pure (head first : next)+    Left _ -> meetCondition cond rest ctx++meetMaybeCondition :: Maybe Y.Condition -> [Subst] -> RuleContext -> IO [Subst]+meetMaybeCondition Nothing substs _ = pure substs+meetMaybeCondition (Just cond) substs ctx = meetCondition cond substs ctx++-- Extend list of given substitutions with extra substitutions from 'where' yaml rule section+extraSubstitutions :: [Subst] -> Maybe [Y.Extra] -> RuleContext -> IO [Subst]+extraSubstitutions substs extras RuleContext {..} = case extras of+  Nothing -> pure substs+  Just extras' -> do+    res <-+      sequence+        [ foldlM+            ( \(Just subst') extra -> do+                let maybeName = case Y.meta extra of+                      Y.ArgExpression (ExMeta name) -> Just name+                      Y.ArgAttribute (AtMeta name) -> Just name+                      Y.ArgBinding (BiMeta name) -> Just name+                      Y.ArgBytes (BtMeta name) -> Just name+                      _ -> Nothing+                    func = Y.function extra+                    args = Y.args extra+                term <- _buildTerm func args subst' _program+                meta <- case term of+                  TeExpression expr -> do+                    logDebug (printf "Function %s() returned expression:\n%s" func (prettyExpression' expr))+                    pure (MvExpression expr defaultScope)+                  TeAttribute attr -> do+                    logDebug (printf "Function %s() returned attribute:\n%s" func (prettyAttribute attr))+                    pure (MvAttribute attr)+                  TeBytes bytes -> do+                    logDebug (printf "Function %s() returned bytes: %s" func (prettyBytes bytes))+                    pure (MvBytes bytes)+                case maybeName of+                  Just name -> pure (combine (substSingle name meta) subst')+                  _ -> pure Nothing+            )+            (Just subst)+            extras'+          | subst <- substs+        ]+    pure (catMaybes res)++matchProgramWithRule :: Program -> Y.Rule -> RuleContext -> IO [Subst]+matchProgramWithRule program rule ctx =+  let ptn = Y.pattern rule+      matched = matchProgram ptn program+   in if null matched+        then pure []+        else do+          when <- meetMaybeCondition (Y.when rule) matched ctx+          if null when+            then pure []+            else do+              extended <- extraSubstitutions when (Y.where_ rule) ctx+              meetMaybeCondition (Y.having rule) extended ctx

@@ -170,7 +170,8 @@     pattern :: Expression,     result :: Expression,     when :: Maybe Condition,-    where_ :: Maybe [Extra]+    where_ :: Maybe [Extra],+    having :: Maybe Condition   }   deriving (Generic, Show) 

@@ -178,6 +178,18 @@           ["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 "fails with --nothing and --must=2" $+      withStdin "Q -> [[ ]]" $+        testCLIFailed ["rewrite", "--nothing", "--must=2"] "it's expected exactly 2 rewriting cycles happened, but rewriting stopped after 1"++    it "does not fail with --nothing and --must" $+      withStdin "Q -> [[ ]]" $+        testCLI ["rewrite", "--nothing", "--must"] ["Φ ↦ ⟦ ρ ↦ ∅ ⟧"]++    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"+   describe "dataize" $ do     it "dataizes simple program" $       withStdin "Q -> [[ D> 01- ]]" $

@@ -1,46 +0,0 @@-{-# LANGUAGE DeriveAnyClass #-}-{-# LANGUAGE DeriveGeneric #-}---- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com--- SPDX-License-Identifier: MIT--module ConditionSpec where--import Ast (Expression, Program (Program))-import Control.Monad-import Data.Aeson-import Data.Yaml qualified as Y-import GHC.Generics-import Misc-import System.FilePath-import Test.Hspec (Spec, describe, expectationFailure, it, runIO)-import Yaml qualified-import Matcher-import Condition-import Pretty--data ConditionPack = ConditionPack-  { expression :: Expression,-    pattern :: Expression,-    condition :: Yaml.Condition-  }-  deriving (Generic, FromJSON, Show)--spec :: Spec-spec = describe "check conditions" $ do-  let resources = "test-resources/condition-packs"-  packs <- runIO (allPathsIn resources)-  forM_-    packs-    ( \pth -> it (makeRelative resources pth) $ do-        pack <- Y.decodeFileThrow pth :: IO ConditionPack-        let matched = matchProgram (pattern pack) (Program (expression pack))-        unless (matched /= []) (expectationFailure "List of matched substitutions is empty which is not expected")-        met <- meetCondition (condition pack) matched-        when-          (null met)-          ( expectationFailure $-              "List of substitution after condition check must be not empty\nOriginal substitutions:\n"-                ++ prettySubsts matched-          )-    )

@@ -92,7 +92,7 @@                   if normalize'                     then pure normalizationRules                     else pure []-              rewritten <- rewrite' program rules' (RewriteContext program repeat' buildTermFromFunction)+              rewritten <- rewrite' program rules' (RewriteContext program repeat' buildTermFromFunction 0)               result' <- parseProgramThrows (output pack)               unless (rewritten == result') $                 expectationFailure

@@ -0,0 +1,48 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}++-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+-- SPDX-License-Identifier: MIT++module RuleSpec where++import Ast (Expression, Program (Program))+import Control.Monad+import Data.Aeson+import Data.Yaml qualified as Y+import Functions (buildTermFromFunction)+import GHC.Generics+import Matcher+import Misc+import Pretty+import Rule (RuleContext (RuleContext), meetCondition)+import System.FilePath+import Test.Hspec (Spec, describe, expectationFailure, it, runIO)+import Yaml qualified++data ConditionPack = ConditionPack+  { expression :: Expression,+    pattern :: Expression,+    condition :: Yaml.Condition+  }+  deriving (Generic, FromJSON, Show)++spec :: Spec+spec = describe "check conditions" $ do+  let resources = "test-resources/condition-packs"+  packs <- runIO (allPathsIn resources)+  forM_+    packs+    ( \pth -> it (makeRelative resources pth) $ do+        pack <- Y.decodeFileThrow pth :: IO ConditionPack+        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)+        when+          (null met)+          ( expectationFailure $+              "List of substitution after condition check must be not empty\nOriginal substitutions:\n"+                ++ prettySubsts matched+          )+    )