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.36 +version: 0.0.0.37 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at @@ -101,7 +101,6 @@ YamlSpec, MiscSpec, XMIRSpec, - HLintSpec, DataizeSpec, Paths_phino autogen-modules: diff --git a/src/Builder.hs b/src/Builder.hs --- a/src/Builder.hs +++ b/src/Builder.hs @@ -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)] diff --git a/src/CLI.hs b/src/CLI.hs --- a/src/CLI.hs +++ b/src/CLI.hs @@ -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 () diff --git a/src/Functions.hs b/src/Functions.hs --- a/src/Functions.hs +++ b/src/Functions.hs @@ -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)) diff --git a/src/Rewriter.hs b/src/Rewriter.hs --- a/src/Rewriter.hs +++ b/src/Rewriter.hs @@ -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 diff --git a/src/Rule.hs b/src/Rule.hs --- a/src/Rule.hs +++ b/src/Rule.hs @@ -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 diff --git a/src/Term.hs b/src/Term.hs --- a/src/Term.hs +++ b/src/Term.hs @@ -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 diff --git a/test/BuilderSpec.hs b/test/BuilderSpec.hs --- a/test/BuilderSpec.hs +++ b/test/BuilderSpec.hs @@ -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"), diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -178,7 +178,7 @@ ["rewrite", "--nothing", "--output=xmir", "--omit-listing"] ["", "4 lines of phi", " "] - 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" $ diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -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 = diff --git a/test/HLintSpec.hs b/test/HLintSpec.hs deleted file mode 100644 --- a/test/HLintSpec.hs +++ /dev/null @@ -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/" diff --git a/test/RewriterSpec.hs b/test/RewriterSpec.hs --- a/test/RewriterSpec.hs +++ b/test/RewriterSpec.hs @@ -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 diff --git a/test/RuleSpec.hs b/test/RuleSpec.hs --- a/test/RuleSpec.hs +++ b/test/RuleSpec.hs @@ -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