Skip to content

Commit 1b47350

Browse files
geo2ageo2a
committed
Move substitution-related stuff into a separate module
1 parent 2883e60 commit 1b47350

File tree

10 files changed

+31
-84
lines changed

10 files changed

+31
-84
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/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)

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

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -54,9 +54,10 @@ import Booster.Definition.Base as Def
5454
import Booster.Pattern.Base (Predicate (Predicate), Variable (..))
5555
import Booster.Pattern.Base qualified as Def
5656
import Booster.Pattern.Base qualified as Def.Symbol (Symbol (..))
57-
import Booster.Pattern.Bool (asEquations, foldAndBool, pattern TrueBool)
57+
import Booster.Pattern.Bool (foldAndBool, pattern TrueBool)
5858
import Booster.Pattern.Index as Idx
5959
import Booster.Pattern.Pretty
60+
import Booster.Pattern.Substitution qualified as Substitution
6061
import Booster.Pattern.Util qualified as Util
6162
import Booster.Prettyprinter hiding (attributes)
6263
import Booster.Syntax.Json.Internalise
@@ -788,7 +789,7 @@ internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref
788789
DefinitionPatternError ref (NotSupported (head unsupported))
789790
pure
790791
( Util.modifyVariablesInT f term
791-
, map (Util.modifyVariablesInP f) (preds <> asEquations substitution)
792+
, map (Util.modifyVariablesInP f) (preds <> Substitution.asEquations substitution)
792793
)
793794

794795
internaliseRewriteRuleNoAlias ::
@@ -970,7 +971,7 @@ internaliseCeil partialDef left right sortVars attrs = do
970971
internalisePredicates AllowAlias IgnoreSubsorts (Just sortVars) partialDef [p]
971972
let
972973
-- turn substitution-like predicates back into equations
973-
constraints = internalPs.boolPredicates <> asEquations internalPs.substitution
974+
constraints = internalPs.boolPredicates <> Substitution.asEquations internalPs.substitution
974975
unsupported = internalPs.unsupported
975976
unless (null unsupported) $
976977
throwE $
@@ -1017,7 +1018,7 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att
10171018
argPairs <- mapM internaliseArg args
10181019
let lhs =
10191020
Util.modifyVariablesInT (Util.modifyVarName ("Eq#" <>)) $
1020-
Util.substituteInTerm (Map.fromList argPairs) left
1021+
Substitution.substituteInTerm (Map.fromList argPairs) left
10211022
(rhs, ensures) <-
10221023
internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported
10231024
partialDef
@@ -1049,7 +1050,9 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att
10491050
{ lhs
10501051
, rhs
10511052
, requires =
1052-
map (Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>)) (preds <> asEquations substitution)
1053+
map
1054+
(Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>))
1055+
(preds <> Substitution.asEquations substitution)
10531056
, ensures
10541057
, attributes
10551058
, computedAttributes

0 commit comments

Comments
 (0)