Skip to content

Commit 9e47e06

Browse files
geo2ageo2a
committed
Move substitution-related stuff into a separate module
Fix unit tests add test
1 parent 9f11343 commit 9e47e06

File tree

13 files changed

+199
-140
lines changed

13 files changed

+199
-140
lines changed

‎booster/library/Booster/JsonRpc.hs

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -55,12 +55,11 @@ import Booster.Pattern.Rewrite (
5555
RewriteTrace (..),
5656
performRewrite,
5757
)
58+
import Booster.Pattern.Substitution qualified as Substitution
5859
import Booster.Pattern.Util (
5960
freeVariables,
6061
sortOfPattern,
6162
sortOfTerm,
62-
substituteInPredicate,
63-
substituteInTerm,
6463
)
6564
import Booster.Prettyprinter (renderText)
6665
import Booster.SMT.Interface qualified as SMT
@@ -134,8 +133,8 @@ respond stateVar request =
134133
-- apply the given substitution before doing anything else
135134
let substPat =
136135
Pattern
137-
{ term = substituteInTerm substitution term
138-
, constraints = Set.fromList $ map (substituteInPredicate substitution) preds
136+
{ term = Substitution.substituteInTerm substitution term
137+
, constraints = Set.fromList $ map (Substitution.substituteInPredicate substitution) preds
139138
, ceilConditions = ceils
140139
, substitution
141140
}
@@ -252,8 +251,8 @@ respond stateVar request =
252251
-- apply the given substitution before doing anything else
253252
let substPat =
254253
Pattern
255-
{ term = substituteInTerm substitution pat.term
256-
, constraints = Set.map (substituteInPredicate substitution) pat.constraints
254+
{ term = Substitution.substituteInTerm substitution pat.term
255+
, constraints = Set.map (Substitution.substituteInPredicate substitution) pat.constraints
257256
, ceilConditions = pat.ceilConditions
258257
, substitution
259258
}
@@ -283,7 +282,7 @@ respond stateVar request =
283282
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do
284283
logMessage ("ignoring unsupported predicate parts" :: Text)
285284
-- apply the given substitution before doing anything else
286-
let predicates = map (substituteInPredicate ps.substitution) ps.boolPredicates
285+
let predicates = map (Substitution.substituteInPredicate ps.substitution) ps.boolPredicates
287286
withContext CtxConstraint $
288287
ApplyEquations.simplifyConstraints
289288
def

‎booster/library/Booster/Log.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,8 +68,8 @@ import Booster.Pattern.Base (
6868
TermAttributes (hash),
6969
pattern AndTerm,
7070
)
71-
import Booster.Pattern.Bool (asEquations)
7271
import Booster.Pattern.Pretty
72+
import Booster.Pattern.Substitution (asEquations)
7373
import Booster.Prettyprinter (renderOneLineText)
7474
import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern)
7575
import Booster.Syntax.Json.Externalise (externaliseTerm)

‎booster/library/Booster/Pattern/ApplyEquations.hs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,7 @@ import Booster.Pattern.Bool
6666
import Booster.Pattern.Index qualified as Idx
6767
import Booster.Pattern.Match
6868
import Booster.Pattern.Pretty
69+
import Booster.Pattern.Substitution
6970
import Booster.Pattern.Util
7071
import Booster.Prettyprinter (renderOneLineText)
7172
import Booster.SMT.Interface qualified as SMT

‎booster/library/Booster/Pattern/Bool.hs

Lines changed: 1 addition & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,6 @@ module Booster.Pattern.Bool (
1010
negateBool,
1111
splitBoolPredicates,
1212
splitAndBools,
13-
mkEq,
14-
destructEq,
15-
asEquations,
16-
partitionPredicates,
1713
-- patterns
1814
pattern TrueBool,
1915
pattern FalseBool,
@@ -28,10 +24,6 @@ module Booster.Pattern.Bool (
2824
) where
2925

3026
import Data.ByteString.Char8 (ByteString)
31-
import Data.List (partition)
32-
import Data.Map.Strict (Map)
33-
import Data.Map.Strict qualified as Map
34-
import Data.Maybe (isJust, mapMaybe)
3527

3628
import Booster.Definition.Attributes.Base (
3729
FunctionType (..),
@@ -48,18 +40,15 @@ import Booster.Pattern.Base (
4840
Predicate (..),
4941
Symbol (Symbol),
5042
Term,
51-
Variable,
5243
pattern DomainValue,
53-
pattern KSeq,
5444
pattern SortBool,
5545
pattern SortInt,
5646
pattern SortK,
5747
pattern SortKItem,
5848
pattern SortSet,
5949
pattern SymbolApplication,
60-
pattern Var,
6150
)
62-
import Booster.Pattern.Util (isConcrete, sortOfTerm)
51+
import Booster.Pattern.Util (isConcrete)
6352
import Booster.SMT.Base (SExpr (Atom), SMTId (..))
6453

6554
pattern HookedTotalFunction :: ByteString -> SymbolAttributes
@@ -216,28 +205,3 @@ splitAndBools :: Predicate -> [Predicate]
216205
splitAndBools p@(Predicate t)
217206
| AndBool l r <- t = concatMap (splitAndBools . Predicate) [l, r]
218207
| otherwise = [p]
219-
220-
mkEq :: Variable -> Term -> Predicate
221-
mkEq x t = Predicate $ case sortOfTerm t of
222-
SortInt -> EqualsInt (Var x) t
223-
SortBool -> EqualsBool (Var x) t
224-
otherSort -> EqualsK (KSeq otherSort (Var x)) (KSeq otherSort t)
225-
226-
-- | Pattern match on an equality predicate and try extracting a variable assignment
227-
destructEq :: Predicate -> Maybe (Variable, Term)
228-
destructEq = \case
229-
Predicate (EqualsInt (Var x) t) -> Just (x, t)
230-
Predicate (EqualsBool (Var x) t) -> Just (x, t)
231-
Predicate
232-
(EqualsK (KSeq _lhsSort (Var x)) (KSeq _rhsSort t)) -> Just (x, t)
233-
_ -> Nothing
234-
235-
-- | turns a substitution into a list of equations
236-
asEquations :: Map Variable Term -> [Predicate]
237-
asEquations = map (uncurry mkEq) . Map.assocs
238-
239-
-- | Extract substitution items from a list of generic predicates. Return empty substitution if none are found
240-
partitionPredicates :: [Predicate] -> (Map Variable Term, [Predicate])
241-
partitionPredicates ps =
242-
let (substItems, normalPreds) = partition (isJust . destructEq) ps
243-
in (Map.fromList . mapMaybe destructEq $ substItems, normalPreds)

‎booster/library/Booster/Pattern/Implies.hs

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,8 @@ import Booster.Pattern.Base (Pattern (..), Predicate (..))
2626
import Booster.Pattern.Bool (pattern TrueBool)
2727
import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (Implies), matchTerms)
2828
import Booster.Pattern.Pretty (FromModifiersT, ModifiersRep (..), pretty')
29-
import Booster.Pattern.Util (freeVariables, sortOfPattern, substituteInPredicate, substituteInTerm)
29+
import Booster.Pattern.Substitution qualified as Substitution
30+
import Booster.Pattern.Util (freeVariables, sortOfPattern)
3031
import Booster.Prettyprinter (renderDefault)
3132
import Booster.SMT.Interface qualified as SMT
3233
import Booster.Syntax.Json (addHeader, prettyPattern)
@@ -108,15 +109,15 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
108109
-- apply the given substitution before doing anything else
109110
substPatL =
110111
Pattern
111-
{ term = substituteInTerm substitutionL patL.term
112-
, constraints = Set.map (substituteInPredicate substitutionL) patL.constraints
112+
{ term = Substitution.substituteInTerm substitutionL patL.term
113+
, constraints = Set.map (Substitution.substituteInPredicate substitutionL) patL.constraints
113114
, ceilConditions = patL.ceilConditions
114115
, substitution = substitutionL
115116
}
116117
substPatR =
117118
Pattern
118-
{ term = substituteInTerm substitutionR patR.term
119-
, constraints = Set.map (substituteInPredicate substitutionR) patR.constraints
119+
{ term = Substitution.substituteInTerm substitutionR patR.term
120+
, constraints = Set.map (Substitution.substituteInPredicate substitutionR) patR.constraints
120121
, ceilConditions = patR.ceilConditions
121122
, substitution = substitutionR
122123
}
@@ -158,7 +159,8 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
158159
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err)
159160
MatchSuccess subst -> do
160161
let filteredConsequentPreds =
161-
Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints
162+
Set.map (Substitution.substituteInPredicate subst) substPatR.constraints
163+
`Set.difference` substPatL.constraints
162164

163165
if null filteredConsequentPreds
164166
then

‎booster/library/Booster/Pattern/Match.hs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -36,12 +36,12 @@ import Booster.Definition.Attributes.Base (KListDefinition, KMapDefinition, KSet
3636
import Booster.Definition.Base
3737
import Booster.Pattern.Base
3838
import Booster.Pattern.Pretty
39+
import Booster.Pattern.Substitution qualified as Substitution
3940
import Booster.Pattern.Util (
4041
checkSymbolIsAc,
4142
freeVariables,
4243
isConstructorSymbol,
4344
sortOfTerm,
44-
substituteInTerm,
4545
)
4646

4747
-- | Result of matching a pattern to a subject (a substitution or an indication of what went wrong)
@@ -665,7 +665,7 @@ matchMaps
665665
-- before matching map keys.
666666
enqueueMapProblem (KMap def patKeyVals patRest) (KMap def subjKeyVals subjRest)
667667
else do
668-
let patternKeyVals = map (first (substituteInTerm st.mSubstitution)) patKeyVals
668+
let patternKeyVals = map (first (Substitution.substituteInTerm st.mSubstitution)) patKeyVals
669669
-- check for duplicate keys
670670
checkDuplicateKeys patternKeyVals patRest
671671
checkDuplicateKeys subjKeyVals subjRest
@@ -782,13 +782,13 @@ bindVariable matchType var term@(Term termAttrs _) = do
782782
Nothing -> do
783783
let
784784
-- apply existing substitutions to term
785-
term' = substituteInTerm currentSubst term
785+
term' = Substitution.substituteInTerm currentSubst term
786786
when (var `Set.member` freeVariables term') $
787787
failWith (VariableRecursion var term)
788788
let
789789
-- substitute in existing substitution terms
790790
currentSubst' =
791-
Map.map (substituteInTerm $ Map.singleton var term') currentSubst
791+
Map.map (Substitution.substituteInTerm $ Map.singleton var term') currentSubst
792792
newSubst = Map.insert var term' currentSubst'
793793
modify $ \s -> s{mSubstitution = newSubst}
794794

‎booster/library/Booster/Pattern/Rewrite.hs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,7 @@ import Booster.Pattern.Match (
6666
matchTerms,
6767
)
6868
import Booster.Pattern.Pretty
69+
import Booster.Pattern.Substitution
6970
import Booster.Pattern.Util
7071
import Booster.Prettyprinter
7172
import Booster.SMT.Interface qualified as SMT

‎booster/library/Booster/Pattern/Substitution.hs

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
{- |
2+
Copyright : (c) Runtime Verification, 2024
3+
License : BSD-3-Clause
4+
5+
Function to manipulate @'Substitution'@s and convert to/from @'Predicate'@s
6+
7+
This module is intended to be imported qualified.
8+
-}
9+
module Booster.Pattern.Substitution (
10+
mkEq,
11+
destructEq,
12+
asEquations,
13+
partitionPredicates,
14+
compose,
15+
substituteInPredicate,
16+
substituteInTerm,
17+
) where
18+
19+
import Data.Bifunctor (bimap)
20+
import Data.Coerce (coerce)
21+
import Data.List (partition)
22+
import Data.Map.Strict (Map)
23+
import Data.Map.Strict qualified as Map
24+
import Data.Maybe (fromMaybe, isJust, mapMaybe)
25+
import Data.Set qualified as Set
26+
27+
import Booster.Pattern.Base
28+
import Booster.Pattern.Bool
29+
import Booster.Pattern.Util (sortOfTerm)
30+
31+
compose :: Substitution -> Substitution -> Substitution
32+
compose newSubst oldSubst =
33+
let substitutedOldSubst = Map.map (substituteInTerm newSubst) oldSubst
34+
in (newSubst `Map.union` substitutedOldSubst) -- new bindings take priority
35+
36+
-- | Build an equality predicate form a variable assignment
37+
mkEq :: Variable -> Term -> Predicate
38+
mkEq x t = Predicate $ case sortOfTerm t of
39+
SortInt -> EqualsInt (Var x) t
40+
SortBool -> EqualsBool (Var x) t
41+
otherSort -> EqualsK (KSeq otherSort (Var x)) (KSeq otherSort t)
42+
43+
{- | Pattern match on an equality predicate and try extracting a variable assignment.
44+
This is a partial inverse of @'mkEq'@
45+
-}
46+
destructEq :: Predicate -> Maybe (Variable, Term)
47+
destructEq = \case
48+
Predicate (EqualsInt (Var x) t) -> Just (x, t)
49+
Predicate (EqualsBool (Var x) t) -> Just (x, t)
50+
Predicate
51+
(EqualsK (KSeq _lhsSort (Var x)) (KSeq _rhsSort t)) -> Just (x, t)
52+
_ -> Nothing
53+
54+
-- | turns a substitution into a list of equations
55+
asEquations :: Map Variable Term -> [Predicate]
56+
asEquations = map (uncurry mkEq) . Map.assocs
57+
58+
-- | Extract substitution items from a list of generic predicates. Return empty substitution if none are found
59+
partitionPredicates :: [Predicate] -> (Map Variable Term, [Predicate])
60+
partitionPredicates ps =
61+
let (substItems, normalPreds) = partition (isJust . destructEq) ps
62+
in (Map.fromList . mapMaybe destructEq $ substItems, normalPreds)
63+
64+
substituteInTerm :: Substitution -> Term -> Term
65+
substituteInTerm substitution = goSubst
66+
where
67+
targetSet = Map.keysSet substitution
68+
goSubst t
69+
| Set.null (targetSet `Set.intersection` (getAttributes t).variables) = t
70+
| otherwise = case t of
71+
Var v -> fromMaybe t (Map.lookup v substitution)
72+
DomainValue{} -> t
73+
SymbolApplication sym sorts args ->
74+
SymbolApplication sym sorts $ map goSubst args
75+
AndTerm t1 t2 -> AndTerm (goSubst t1) (goSubst t2)
76+
Injection ss s sub -> Injection ss s (goSubst sub)
77+
KMap attrs keyVals rest -> KMap attrs (bimap goSubst goSubst <$> keyVals) (goSubst <$> rest)
78+
KList def heads rest ->
79+
KList def (map goSubst heads) (bimap goSubst (map goSubst) <$> rest)
80+
KSet def elements rest ->
81+
KSet def (map goSubst elements) (goSubst <$> rest)
82+
83+
substituteInPredicate :: Substitution -> Predicate -> Predicate
84+
substituteInPredicate substitution = coerce . substituteInTerm substitution . coerce

‎booster/library/Booster/Pattern/Util.hs

Lines changed: 0 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,6 @@ module Booster.Pattern.Util (
66
substituteInSort,
77
sortOfTerm,
88
sortOfPattern,
9-
substituteInTerm,
10-
substituteInPredicate,
119
modifyVariables,
1210
modifyVariablesInT,
1311
modifyVariablesInP,
@@ -82,28 +80,6 @@ substituteInSort subst (SortApp n args) =
8280
sortOfPattern :: Pattern -> Sort
8381
sortOfPattern pat = sortOfTerm pat.term
8482

85-
substituteInTerm :: Map Variable Term -> Term -> Term
86-
substituteInTerm substitution = goSubst
87-
where
88-
targetSet = Map.keysSet substitution
89-
goSubst t
90-
| Set.null (targetSet `Set.intersection` (getAttributes t).variables) = t
91-
| otherwise = case t of
92-
Var v -> fromMaybe t (Map.lookup v substitution)
93-
DomainValue{} -> t
94-
SymbolApplication sym sorts args ->
95-
SymbolApplication sym sorts $ map goSubst args
96-
AndTerm t1 t2 -> AndTerm (goSubst t1) (goSubst t2)
97-
Injection ss s sub -> Injection ss s (goSubst sub)
98-
KMap attrs keyVals rest -> KMap attrs (bimap goSubst goSubst <$> keyVals) (goSubst <$> rest)
99-
KList def heads rest ->
100-
KList def (map goSubst heads) (bimap goSubst (map goSubst) <$> rest)
101-
KSet def elements rest ->
102-
KSet def (map goSubst elements) (goSubst <$> rest)
103-
104-
substituteInPredicate :: Map Variable Term -> Predicate -> Predicate
105-
substituteInPredicate substitution = coerce . substituteInTerm substitution . coerce
106-
10783
modifyVariables :: (Variable -> Variable) -> Pattern -> Pattern
10884
modifyVariables f p =
10985
Pattern

‎booster/library/Booster/Syntax/Json/Internalise.hs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,7 @@ import Booster.Log (LoggerMIO, logMessage, withKorePatternContext)
7171
import Booster.Pattern.Base qualified as Internal
7272
import Booster.Pattern.Bool qualified as Internal
7373
import Booster.Pattern.Pretty
74+
import Booster.Pattern.Substitution qualified as Internal
7475
import Booster.Pattern.Util (freeVariables, sortOfTerm, substituteInSort)
7576
import Booster.Prettyprinter (renderDefault)
7677
import Booster.Syntax.Json (addHeader)

0 commit comments

Comments
 (0)