From b148a1fde24f7d03a3ee9d3acd5cac9c0244b201 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Fri, 25 Oct 2024 14:51:24 +0200 Subject: [PATCH] Introduce RewriteBranchNextState Fix unit tests --- booster/library/Booster/JsonRpc.hs | 3 +- booster/library/Booster/Pattern/Rewrite.hs | 40 +++++++-- .../Test/Booster/Pattern/Rewrite.hs | 84 ++++++++++--------- 3 files changed, 80 insertions(+), 47 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index a6f1841aa4..f1dbab6537 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -49,6 +49,7 @@ import Booster.Pattern.Base qualified as Pattern import Booster.Pattern.Implies (runImplies) import Booster.Pattern.Pretty import Booster.Pattern.Rewrite ( + RewriteBranchNextState (..), RewriteConfig (..), RewriteFailed (..), RewriteResult (..), @@ -485,7 +486,7 @@ execResponse req (d, traces, rr) unsupported = case rr of , nextStates = Just $ map - ( \(_, muid, p', mrulePred, ruleSubst) -> toExecState p' unsupported (Just muid) mrulePred (Just ruleSubst) + ( \(RewriteBranchNextState{ruleUniqueId, rewrittenPat, mRulePredicate, ruleSubstitution}) -> toExecState rewrittenPat unsupported (Just ruleUniqueId) mRulePredicate (Just ruleSubstitution) ) $ toList nexts , rule = Nothing diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index b30da58ed5..ae439054dd 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -13,6 +13,7 @@ module Booster.Pattern.Rewrite ( RewriteConfig (..), RewriteFailed (..), RewriteResult (..), + RewriteBranchNextState (..), RewriteTrace (..), pattern CollectRewriteTraces, pattern NoCollectRewriteTraces, @@ -247,7 +248,14 @@ rewriteStep cutLabels terminalLabels pat = do RewriteBranch base $ NE.fromList $ map - ( \(rule, RewriteRuleAppliedData{rewritten, rulePredicate, ruleSubstitution}) -> (ruleLabelOrLocT rule, uniqueId rule, rewritten, rulePredicate, ruleSubstitution) + ( \(rule, RewriteRuleAppliedData{rewritten, rulePredicate, ruleSubstitution}) -> + RewriteBranchNextState + { ruleLabel = ruleLabelOrLocT rule + , ruleUniqueId = uniqueId rule + , rewrittenPat = rewritten + , mRulePredicate = rulePredicate + , ruleSubstitution + } ) leafs @@ -789,10 +797,20 @@ ruleLabelOrLoc rule = fromMaybe "unknown rule" $ fmap pretty rule.attributes.ruleLabel <|> fmap pretty rule.attributes.location +data RewriteBranchNextState pat = RewriteBranchNextState + { ruleLabel :: Text + , ruleUniqueId :: UniqueId + , rewrittenPat :: pat + , mRulePredicate :: Maybe Predicate + , ruleSubstitution :: Substitution + } + deriving stock (Eq, Show) + deriving (Functor, Foldable, Traversable) + -- | Different rewrite results (returned from RPC execute endpoint) data RewriteResult pat = -- | branch point - RewriteBranch pat (NonEmpty (Text, UniqueId, pat, Maybe Predicate, Substitution)) + RewriteBranch pat (NonEmpty (RewriteBranchNextState pat)) | -- | no rules could be applied, config is stuck RewriteStuck pat | -- | cut point rule, return current (lhs) and single next state @@ -1020,15 +1038,19 @@ performRewrite rewriteConfig pat = do simplifyP p >>= \case Nothing -> pure $ RewriteTrivial orig Just p' -> do - -- simplify the 3rd component, i.e. the pattern - let simplifyP3rd (a, b, c, e, f) = - fmap (a,b,,e,f) <$> simplifyP c - nexts' <- catMaybes <$> mapM simplifyP3rd (toList nexts) + -- simplify the next-state pattern inside a branch payload + let simplifyRewritten pattr@RewriteBranchNextState{rewrittenPat} = do + ( fmap @Maybe + ( \rewrittenSimplified -> (pattr{rewrittenPat = rewrittenSimplified}) + ) + ) + <$> simplifyP rewrittenPat + nexts' <- catMaybes <$> mapM simplifyRewritten (toList nexts) pure $ case nexts' of -- The `[]` case should be `Stuck` not `Trivial`, because `RewriteTrivial p'` -- means the pattern `p'` is bottom, but we know that is not the case here. [] -> RewriteStuck p' - [(lbl, uId, n, _rp, _rs)] -> RewriteFinished (Just lbl) (Just uId) n + [RewriteBranchNextState{ruleLabel, ruleUniqueId, rewrittenPat}] -> RewriteFinished (Just ruleLabel) (Just ruleUniqueId) rewrittenPat ns -> RewriteBranch p' $ NE.fromList ns r@RewriteStuck{} -> pure r r@RewriteTrivial{} -> pure r @@ -1098,7 +1120,9 @@ performRewrite rewriteConfig pat = do incrementCounter doSteps False single RewriteBranch pat'' branches -> withPatternContext pat' $ do - emitRewriteTrace $ RewriteBranchingStep pat'' $ fmap (\(lbl, uid, _, _, _) -> (lbl, uid)) branches + emitRewriteTrace $ + RewriteBranchingStep pat'' $ + fmap (\RewriteBranchNextState{ruleLabel, ruleUniqueId} -> (ruleLabel, ruleUniqueId)) branches pure simplified _other -> withPatternContext pat' $ error "simplifyResult: Unexpected return value" Right (cutPoint@(RewriteCutPoint lbl _ _ _), _) -> withPatternContext pat' $ do diff --git a/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs b/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs index 916222fa54..83d1a6c6b8 100644 --- a/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs +++ b/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs @@ -175,7 +175,13 @@ testConf = do ignoreRulePredicateAndSubst :: RewriteResult Pattern -> RewriteResult Pattern ignoreRulePredicateAndSubst = \case - RewriteBranch pre posts -> RewriteBranch pre (NE.map (\(lbl, uid, p, _, _) -> (lbl, uid, p, Nothing, mempty)) posts) + RewriteBranch pre posts -> + RewriteBranch + pre + ( NE.map + (\nextState -> nextState{mRulePredicate = Nothing, ruleSubstitution = mempty}) + posts + ) other -> other ---------------------------------------- @@ -268,7 +274,7 @@ t `branchesTo` ts = @?>>= Right ( RewriteBranch (Pattern_ t) $ NE.fromList $ - map (\(lbl, t') -> (lbl, mockUniqueId, Pattern_ t', Nothing, mempty)) ts + map (\(lbl, t') -> RewriteBranchNextState lbl mockUniqueId (Pattern_ t') Nothing mempty) ts ) failsWith :: Term -> RewriteFailed "Rewrite" -> IO () @@ -312,19 +318,19 @@ canRewrite = RewriteStuck , testCase "Rewrites con3 twice, branching on con1" $ do let branch1 = - ( "con1-f2" - , mockUniqueId - , [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( \dv{SomeSort{}}("somethingElse"), \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] - , Nothing - , mempty - ) + RewriteBranchNextState + "con1-f2" + mockUniqueId + [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( \dv{SomeSort{}}("somethingElse"), \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] + Nothing + mempty branch2 = - ( "con1-f1'" - , mockUniqueId - , [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] - , Nothing - , mempty - ) + RewriteBranchNextState + "con1-f1'" + mockUniqueId + [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] + Nothing + mempty rewrites (Steps 1) @@ -409,19 +415,20 @@ supportsDepthControl = (RewriteFinished Nothing Nothing) , testCase "prefers reporting branches to stopping at depth" $ do let branch1 = - ( "con1-f2" - , mockUniqueId - , [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( \dv{SomeSort{}}("somethingElse"), \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] - , Nothing - , mempty - ) + RewriteBranchNextState + "con1-f2" + mockUniqueId + [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( \dv{SomeSort{}}("somethingElse"), \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] + Nothing + mempty + branch2 = - ( "con1-f1'" - , mockUniqueId - , [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] - , Nothing - , mempty - ) + RewriteBranchNextState + "con1-f1'" + mockUniqueId + [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] + Nothing + mempty rewritesToDepth (MaxDepth 2) @@ -466,19 +473,20 @@ supportsCutPoints = RewriteStuck , testCase "prefers reporting branches to stopping at label in one branch" $ do let branch1 = - ( "con1-f2" - , mockUniqueId - , [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( \dv{SomeSort{}}("somethingElse"), \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] - , Nothing - , mempty - ) + RewriteBranchNextState + "con1-f2" + mockUniqueId + [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( \dv{SomeSort{}}("somethingElse"), \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] + Nothing + mempty + branch2 = - ( "con1-f1'" - , mockUniqueId - , [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] - , Nothing - , mempty - ) + RewriteBranchNextState + "con1-f1'" + mockUniqueId + [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] + Nothing + mempty rewritesToCutPoint "con1-f2"