Skip to content

Commit b0d4ee9

Browse files
goodlyrottenapplegithub-actions
goodlyrottenapple
and
github-actions
authored
Merge Match/Unify modules (#3810)
Fixes #3785 by merging the two versions of our matching algorithm, one used in matching rewrite rules and another matching function/simplification rules. This is a first pass which mostly just merges the two algorithms, prserving most of the divergent behaviour under the `Rewrite`/`Eval` `MatchType` flag. A followup refactor should clean up this code further. This PR is a port of runtimeverification/hs-backend-booster#573 where the development and testing happened. --------- Co-authored-by: github-actions <[email protected]>
1 parent a000386 commit b0d4ee9

File tree

29 files changed

+2147
-2337
lines changed

29 files changed

+2147
-2337
lines changed

‎booster/library/Booster/Definition/Attributes/Base.hs

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ module Booster.Definition.Attributes.Base (
1818
Constrained (..),
1919
ComputedAxiomAttributes (..),
2020
SymbolType (..),
21+
FunctionType (..),
2122
SymbolAttributes (..),
2223
SMTType (..),
2324
SortAttributes (..),
@@ -155,11 +156,13 @@ data Concreteness
155156
deriving stock (Eq, Ord, Show, Generic)
156157
deriving anyclass (NFData)
157158

159+
data FunctionType = Partial | Total
160+
deriving stock (Eq, Ord, Show, Generic, Data, Lift)
161+
deriving anyclass (NFData, Hashable)
162+
158163
data SymbolType
159-
= PartialFunction
160-
| TotalFunction
164+
= Function FunctionType
161165
| Constructor
162-
| SortInjection
163166
deriving stock (Eq, Ord, Show, Generic, Data, Lift)
164167
deriving anyclass (NFData, Hashable)
165168

‎booster/library/Booster/Definition/Attributes/Reader.hs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -152,9 +152,9 @@ instance HasAttributes ParsedSymbol where
152152
isTotal <- attributes .! "total" <||> attributes .! "functional"
153153
case (isConstr, isInjctn, isFunctn, isTotal) of
154154
(True, _, _, _) -> pure Constructor
155-
(_, True, _, _) -> pure SortInjection
156-
(_, _, _, True) -> pure TotalFunction
157-
(_, _, True, _) -> pure PartialFunction
155+
(_, True, _, _) -> pure Constructor
156+
(_, _, _, True) -> pure $ Function Total
157+
(_, _, True, _) -> pure $ Function Partial
158158
_other ->
159159
throwE $ "Invalid symbol type '" <> name.getId <> "', attributes: " <> Text.pack (show attributes)
160160
isIdem = do

‎booster/library/Booster/Definition/Ceil.hs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -143,7 +143,8 @@ computeCeilRule mllvm def [email protected]{lhs, requires, rhs, attribut
143143

144144
computeCeil :: MonadLoggerIO io => Term -> EquationT io [Either Predicate Term]
145145
computeCeil term@(SymbolApplication symbol _ args)
146-
| symbol.attributes.symbolType /= Booster.Definition.Attributes.Base.PartialFunction =
146+
| symbol.attributes.symbolType
147+
/= Booster.Definition.Attributes.Base.Function Booster.Definition.Attributes.Base.Partial =
147148
concatMapM computeCeil args
148149
| otherwise = do
149150
ceils <- (.definition.ceils) <$> getConfig

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ mkSummary file def computeCeilsSummary =
7070
concatMap Map.elems (Map.elems def.rewriteTheory)
7171
, partialSymbolsCount =
7272
length $
73-
filter (\sym -> sym.attributes.symbolType == PartialFunction) $
73+
filter (\sym -> sym.attributes.symbolType == Function Partial) $
7474
Map.elems def.symbols
7575
, functionRuleCount =
7676
length $ concat $ concatMap Map.elems (Map.elems def.functionEquations)

‎booster/library/Booster/JsonRpc.hs

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -806,16 +806,21 @@ mkLogRewriteTrace
806806
{ reason = "Uncertain about definedness of rule because of: " <> pack (show undefReasons)
807807
, _ruleId = fmap getUniqueId (uniqueId $ Definition.attributes r)
808808
}
809-
UnificationIsNotMatch r _ _ ->
809+
IsNotMatch r _ _ ->
810810
Failure
811-
{ reason = "Unification produced a non-match"
811+
{ reason = "Produced a non-match"
812812
, _ruleId = fmap getUniqueId (uniqueId $ Definition.attributes r)
813813
}
814814
RewriteSortError r _ _ ->
815815
Failure
816816
{ reason = "Sort error while unifying"
817817
, _ruleId = fmap getUniqueId (uniqueId $ Definition.attributes r)
818818
}
819+
InternalMatchError{} ->
820+
Failure
821+
{ reason = "Internal match error"
822+
, _ruleId = Nothing
823+
}
819824
, origin = Booster
820825
}
821826
RewriteSimplified equationTraces Nothing

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -685,7 +685,7 @@ data ApplyEquationResult
685685
deriving stock (Eq, Show)
686686

687687
data ApplyEquationFailure
688-
= FailedMatch MatchFailReason
688+
= FailedMatch FailReason
689689
| IndeterminateMatch
690690
| IndeterminateCondition [Predicate]
691691
| ConditionFalse Predicate
@@ -813,9 +813,9 @@ applyEquation term rule = fmap (either Failure Success) $ runExceptT $ do
813813
throwE (MatchConstraintViolated Concrete "* (term has variables)")
814814
-- match lhs
815815
koreDef <- (.definition) <$> lift getConfig
816-
case matchTerm koreDef rule.lhs term of
816+
case matchTerms Eval koreDef rule.lhs term of
817817
MatchFailed failReason -> throwE $ FailedMatch failReason
818-
MatchIndeterminate _pat _subj -> throwE IndeterminateMatch
818+
MatchIndeterminate{} -> throwE IndeterminateMatch
819819
MatchSuccess subst -> do
820820
-- cancel if condition
821821
-- forall (v, t) : subst. concrete(v) -> isConstructorLike(t) /\

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

Lines changed: 23 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ module Booster.Pattern.Base (
1313
) where
1414

1515
import Booster.Definition.Attributes.Base (
16+
FunctionType (..),
1617
KCollectionMetadata (..),
1718
KCollectionSymbolNames (..),
1819
KListDefinition (..),
@@ -182,7 +183,7 @@ unitSymbol def =
182183
, resultSort = SortApp collectionSort []
183184
, attributes =
184185
SymbolAttributes
185-
{ symbolType = TotalFunction
186+
{ symbolType = Function Total
186187
, isIdem = IsNotIdem
187188
, isAssoc = IsNotAssoc
188189
, isMacroOrAlias = IsNotMacroOrAlias
@@ -219,9 +220,9 @@ concatSymbol def =
219220
where
220221
(symbolNames, collectionSort, symbolType) =
221222
case def of
222-
KMapMeta mapDef -> (mapDef.symbolNames, mapDef.mapSortName, PartialFunction)
223-
KListMeta listDef -> (listDef.symbolNames, listDef.listSortName, TotalFunction)
224-
KSetMeta listDef -> (listDef.symbolNames, listDef.listSortName, PartialFunction)
223+
KMapMeta mapDef -> (mapDef.symbolNames, mapDef.mapSortName, Function Partial)
224+
KListMeta listDef -> (listDef.symbolNames, listDef.listSortName, Function Total)
225+
KSetMeta listDef -> (listDef.symbolNames, listDef.listSortName, Function Partial)
225226

226227
kmapElementSymbol :: KMapDefinition -> Symbol
227228
kmapElementSymbol def =
@@ -232,7 +233,7 @@ kmapElementSymbol def =
232233
, resultSort = SortApp def.mapSortName []
233234
, attributes =
234235
SymbolAttributes
235-
{ symbolType = TotalFunction
236+
{ symbolType = Function Total
236237
, isIdem = IsNotIdem
237238
, isAssoc = IsNotAssoc
238239
, isMacroOrAlias = IsNotMacroOrAlias
@@ -252,7 +253,7 @@ klistElementSymbol def =
252253
, resultSort = SortApp def.listSortName []
253254
, attributes =
254255
SymbolAttributes
255-
{ symbolType = TotalFunction
256+
{ symbolType = Function Total
256257
, isIdem = IsNotIdem
257258
, isAssoc = IsNotAssoc
258259
, isMacroOrAlias = IsNotMacroOrAlias
@@ -522,7 +523,7 @@ pattern SymbolApplication sym sorts args <- Term _ (SymbolApplicationF sym sorts
522523
-- if there are arg.s
523524
| otherwise = foldl1' (<>) $ map getAttributes args
524525
symIsConstructor =
525-
sym.attributes.symbolType `elem` [Constructor, SortInjection]
526+
sym.attributes.symbolType == Constructor
526527
in Term
527528
argAttributes
528529
{ isEvaluated =
@@ -684,7 +685,7 @@ injectionSymbol =
684685
, resultSort = SortVar "To"
685686
, attributes =
686687
SymbolAttributes
687-
{ symbolType = SortInjection
688+
{ symbolType = Constructor
688689
, isIdem = IsNotIdem
689690
, isAssoc = IsNotAssoc
690691
, isMacroOrAlias = IsNotMacroOrAlias
@@ -847,3 +848,17 @@ instance Pretty Pattern where
847848
]
848849
<> fmap (Pretty.indent 4 . pretty) (Set.toList patt.constraints)
849850
<> fmap (Pretty.indent 4 . pretty) patt.ceilConditions
851+
852+
pattern ConsApplication :: Symbol -> [Sort] -> [Term] -> Term
853+
pattern ConsApplication sym sorts args <-
854+
Term
855+
_
856+
(SymbolApplicationF sym@(Symbol _ _ _ _ (SymbolAttributes{symbolType = Constructor})) sorts args)
857+
858+
pattern FunctionApplication :: Symbol -> [Sort] -> [Term] -> Term
859+
pattern FunctionApplication sym sorts args <-
860+
Term
861+
_
862+
(SymbolApplicationF sym@(Symbol _ _ _ _ (SymbolAttributes{symbolType = Function _})) sorts args)
863+
864+
{-# COMPLETE AndTerm, ConsApplication, FunctionApplication, DomainValue, Var, Injection, KMap, KList, KSet #-}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -214,7 +214,7 @@ lookupKoreDefinitionSymbol name = DecodeM $ do
214214
[]
215215
(SortApp "UNKNOWN" [])
216216
( SymbolAttributes
217-
PartialFunction
217+
(Function Booster.Definition.Attributes.Base.Partial)
218218
IsNotIdem
219219
IsNotAssoc
220220
IsNotMacroOrAlias

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

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -26,9 +26,10 @@ module Booster.Pattern.Bool (
2626
import Data.ByteString.Char8 (ByteString)
2727

2828
import Booster.Definition.Attributes.Base (
29+
FunctionType (..),
2930
SMTType (SMTHook),
3031
SymbolAttributes (SymbolAttributes),
31-
SymbolType (TotalFunction),
32+
SymbolType (Function),
3233
pattern CanBeEvaluated,
3334
pattern IsNotAssoc,
3435
pattern IsNotIdem,
@@ -54,7 +55,7 @@ import Booster.SMT.Base (SExpr (Atom), SMTId (..))
5455
pattern HookedTotalFunction :: ByteString -> SymbolAttributes
5556
pattern HookedTotalFunction hook =
5657
SymbolAttributes
57-
TotalFunction
58+
(Function Total)
5859
IsNotIdem
5960
IsNotAssoc
6061
IsNotMacroOrAlias
@@ -66,7 +67,7 @@ pattern HookedTotalFunction hook =
6667
pattern HookedTotalFunctionWithSMT :: ByteString -> ByteString -> SymbolAttributes
6768
pattern HookedTotalFunctionWithSMT hook smt =
6869
SymbolAttributes
69-
TotalFunction
70+
(Function Total)
7071
IsNotIdem
7172
IsNotAssoc
7273
IsNotMacroOrAlias

0 commit comments

Comments
 (0)