diff --git a/phino.cabal b/phino.cabal --- a/phino.cabal +++ b/phino.cabal @@ -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 @@ -32,7 +32,7 @@ Replacer, Rewriter, Yaml, - Condition, + Rule, Dataize, Functions, Term, @@ -97,7 +97,7 @@ ReplacerSpec, PrettySpec, RewriterSpec, - ConditionSpec, + RuleSpec, YamlSpec, MiscSpec, XMIRSpec, diff --git a/src/CLI.hs b/src/CLI.hs --- a/src/CLI.hs +++ b/src/CLI.hs @@ -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 diff --git a/src/Condition.hs b/src/Condition.hs deleted file mode 100644 --- a/src/Condition.hs +++ /dev/null @@ -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) diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -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 diff --git a/src/Rewriter.hs b/src/Rewriter.hs --- a/src/Rewriter.hs +++ b/src/Rewriter.hs @@ -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) diff --git a/src/Rule.hs b/src/Rule.hs new file mode 100644 --- /dev/null +++ b/src/Rule.hs @@ -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 diff --git a/src/Yaml.hs b/src/Yaml.hs --- a/src/Yaml.hs +++ b/src/Yaml.hs @@ -170,7 +170,8 @@ pattern :: Expression, result :: Expression, when :: Maybe Condition, - where_ :: Maybe [Extra] + where_ :: Maybe [Extra], + having :: Maybe Condition } deriving (Generic, Show) diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -178,6 +178,18 @@ ["rewrite", "--nothing", "--output=xmir", "--omit-listing"] ["", "4 lines of phi", " "] + 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- ]]" $ diff --git a/test/ConditionSpec.hs b/test/ConditionSpec.hs deleted file mode 100644 --- a/test/ConditionSpec.hs +++ /dev/null @@ -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 - ) - ) diff --git a/test/RewriterSpec.hs b/test/RewriterSpec.hs --- a/test/RewriterSpec.hs +++ b/test/RewriterSpec.hs @@ -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 diff --git a/test/RuleSpec.hs b/test/RuleSpec.hs new file mode 100644 --- /dev/null +++ b/test/RuleSpec.hs @@ -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 + ) + )