Skip to content

Commit

Permalink
Introduce RewriteBranchNextState
Browse files Browse the repository at this point in the history 
Fix unit tests
  • Loading branch information
@geo2a
geo2a committed Oct 25, 2024
1 parent 920ad62 commit b148a1f
Show file tree
Hide file tree
Showing 3 changed files with 80 additions and 47 deletions.
3 changes: 2 additions & 1 deletion booster/library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 (..),
Expand Down Expand Up @@ -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
Expand Down
40 changes: 32 additions & 8 deletions booster/library/Booster/Pattern/Rewrite.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ module Booster.Pattern.Rewrite (
RewriteConfig (..),
RewriteFailed (..),
RewriteResult (..),
RewriteBranchNextState (..),
RewriteTrace (..),
pattern CollectRewriteTraces,
pattern NoCollectRewriteTraces,
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
84 changes: 46 additions & 38 deletions booster/unit-tests/Test/Booster/Pattern/Rewrite.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

----------------------------------------
Expand Down Expand Up @@ -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 ()
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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"
Expand Down

0 comments on commit b148a1f

Please sign in to comment.