Merge Match/Unify modules

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

@@ -18,6 +18,7 @@ module Booster.Definition.Attributes.Base (
     Constrained (..),
     ComputedAxiomAttributes (..),
     SymbolType (..),
+    FunctionType (..),
     SymbolAttributes (..),
     SMTType (..),
     SortAttributes (..),
@@ -155,11 +156,13 @@ data Concreteness
     deriving stock (Eq, Ord, Show, Generic)
     deriving anyclass (NFData)
 
+data FunctionType = Partial | Total
+    deriving stock (Eq, Ord, Show, Generic, Data, Lift)
+    deriving anyclass (NFData, Hashable)
+
 data SymbolType
-    = PartialFunction
-    | TotalFunction
+    = Function FunctionType
     | Constructor
-    | SortInjection
     deriving stock (Eq, Ord, Show, Generic, Data, Lift)
     deriving anyclass (NFData, Hashable)
 

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

@@ -152,9 +152,9 @@ instance HasAttributes ParsedSymbol where
                 isTotal <- attributes .! "total" <||> attributes .! "functional"
                 case (isConstr, isInjctn, isFunctn, isTotal) of
                     (True, _, _, _) -> pure Constructor
-                    (_, True, _, _) -> pure SortInjection
-                    (_, _, _, True) -> pure TotalFunction
-                    (_, _, True, _) -> pure PartialFunction
+                    (_, True, _, _) -> pure Constructor
+                    (_, _, _, True) -> pure $ Function Total
+                    (_, _, True, _) -> pure $ Function Partial
                     _other ->
                         throwE $ "Invalid symbol type '" <> name.getId <> "', attributes: " <> Text.pack (show attributes)
             isIdem = do

booster/library/Booster/Definition/Ceil.hs

@@ -143,7 +143,8 @@ computeCeilRule mllvm def [email protected]{lhs, requires, rhs, attribut
 
 computeCeil :: MonadLoggerIO io => Term -> EquationT io [Either Predicate Term]
 computeCeil term@(SymbolApplication symbol _ args)
-    | symbol.attributes.symbolType /= Booster.Definition.Attributes.Base.PartialFunction =
+    | symbol.attributes.symbolType
+        /= Booster.Definition.Attributes.Base.Function Booster.Definition.Attributes.Base.Partial =
         concatMapM computeCeil args
     | otherwise = do
         ceils <- (.definition.ceils) <$> getConfig

booster/library/Booster/Definition/Util.hs

@@ -70,7 +70,7 @@ mkSummary file def computeCeilsSummary =
                         concatMap Map.elems (Map.elems def.rewriteTheory)
         , partialSymbolsCount =
             length $
-                filter (\sym -> sym.attributes.symbolType == PartialFunction) $
+                filter (\sym -> sym.attributes.symbolType == Function Partial) $
                     Map.elems def.symbols
         , functionRuleCount =
             length $ concat $ concatMap Map.elems (Map.elems def.functionEquations)

booster/library/Booster/JsonRpc.hs

@@ -806,16 +806,21 @@ mkLogRewriteTrace
                                             { reason = "Uncertain about definedness of rule because of: " <> pack (show undefReasons)
                                             , _ruleId = fmap getUniqueId (uniqueId $ Definition.attributes r)
                                             }
-                                    UnificationIsNotMatch r _ _ ->
+                                    IsNotMatch r _ _ ->
                                         Failure
-                                            { reason = "Unification produced a non-match"
+                                            { reason = "Produced a non-match"
                                             , _ruleId = fmap getUniqueId (uniqueId $ Definition.attributes r)
                                             }
                                     RewriteSortError r _ _ ->
                                         Failure
                                             { reason = "Sort error while unifying"
                                             , _ruleId = fmap getUniqueId (uniqueId $ Definition.attributes r)
                                             }
+                                    InternalMatchError{} ->
+                                        Failure
+                                            { reason = "Internal match error"
+                                            , _ruleId = Nothing
+                                            }
                                 , origin = Booster
                                 }
             RewriteSimplified equationTraces Nothing

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -685,7 +685,7 @@ data ApplyEquationResult
     deriving stock (Eq, Show)
 
 data ApplyEquationFailure
-    = FailedMatch MatchFailReason
+    = FailedMatch FailReason
     | IndeterminateMatch
     | IndeterminateCondition [Predicate]
     | ConditionFalse Predicate
@@ -813,9 +813,9 @@ applyEquation term rule = fmap (either Failure Success) $ runExceptT $ do
         throwE (MatchConstraintViolated Concrete "* (term has variables)")
     -- match lhs
     koreDef <- (.definition) <$> lift getConfig
-    case matchTerm koreDef rule.lhs term of
+    case matchTerms Eval koreDef rule.lhs term of
         MatchFailed failReason -> throwE $ FailedMatch failReason
-        MatchIndeterminate _pat _subj -> throwE IndeterminateMatch
+        MatchIndeterminate{} -> throwE IndeterminateMatch
         MatchSuccess subst -> do
             -- cancel if condition
             -- forall (v, t) : subst. concrete(v) -> isConstructorLike(t) /\

booster/library/Booster/Pattern/Base.hs

@@ -13,6 +13,7 @@ module Booster.Pattern.Base (
 ) where
 
 import Booster.Definition.Attributes.Base (
+    FunctionType (..),
     KCollectionMetadata (..),
     KCollectionSymbolNames (..),
     KListDefinition (..),
@@ -182,7 +183,7 @@ unitSymbol def =
         , resultSort = SortApp collectionSort []
         , attributes =
             SymbolAttributes
-                { symbolType = TotalFunction
+                { symbolType = Function Total
                 , isIdem = IsNotIdem
                 , isAssoc = IsNotAssoc
                 , isMacroOrAlias = IsNotMacroOrAlias
@@ -219,9 +220,9 @@ concatSymbol def =
   where
     (symbolNames, collectionSort, symbolType) =
         case def of
-            KMapMeta mapDef -> (mapDef.symbolNames, mapDef.mapSortName, PartialFunction)
-            KListMeta listDef -> (listDef.symbolNames, listDef.listSortName, TotalFunction)
-            KSetMeta listDef -> (listDef.symbolNames, listDef.listSortName, PartialFunction)
+            KMapMeta mapDef -> (mapDef.symbolNames, mapDef.mapSortName, Function Partial)
+            KListMeta listDef -> (listDef.symbolNames, listDef.listSortName, Function Total)
+            KSetMeta listDef -> (listDef.symbolNames, listDef.listSortName, Function Partial)
 
 kmapElementSymbol :: KMapDefinition -> Symbol
 kmapElementSymbol def =
@@ -232,7 +233,7 @@ kmapElementSymbol def =
         , resultSort = SortApp def.mapSortName []
         , attributes =
             SymbolAttributes
-                { symbolType = TotalFunction
+                { symbolType = Function Total
                 , isIdem = IsNotIdem
                 , isAssoc = IsNotAssoc
                 , isMacroOrAlias = IsNotMacroOrAlias
@@ -252,7 +253,7 @@ klistElementSymbol def =
         , resultSort = SortApp def.listSortName []
         , attributes =
             SymbolAttributes
-                { symbolType = TotalFunction
+                { symbolType = Function Total
                 , isIdem = IsNotIdem
                 , isAssoc = IsNotAssoc
                 , isMacroOrAlias = IsNotMacroOrAlias
@@ -522,7 +523,7 @@ pattern SymbolApplication sym sorts args <- Term _ (SymbolApplicationF sym sorts
                         -- if there are arg.s
                         | otherwise = foldl1' (<>) $ map getAttributes args
                     symIsConstructor =
-                        sym.attributes.symbolType `elem` [Constructor, SortInjection]
+                        sym.attributes.symbolType == Constructor
                  in Term
                         argAttributes
                             { isEvaluated =
@@ -684,7 +685,7 @@ injectionSymbol =
         , resultSort = SortVar "To"
         , attributes =
             SymbolAttributes
-                { symbolType = SortInjection
+                { symbolType = Constructor
                 , isIdem = IsNotIdem
                 , isAssoc = IsNotAssoc
                 , isMacroOrAlias = IsNotMacroOrAlias
@@ -847,3 +848,17 @@ instance Pretty Pattern where
             ]
                 <> fmap (Pretty.indent 4 . pretty) (Set.toList patt.constraints)
                 <> fmap (Pretty.indent 4 . pretty) patt.ceilConditions
+
+pattern ConsApplication :: Symbol -> [Sort] -> [Term] -> Term
+pattern ConsApplication sym sorts args <-
+    Term
+        _
+        (SymbolApplicationF sym@(Symbol _ _ _ _ (SymbolAttributes{symbolType = Constructor})) sorts args)
+
+pattern FunctionApplication :: Symbol -> [Sort] -> [Term] -> Term
+pattern FunctionApplication sym sorts args <-
+    Term
+        _
+        (SymbolApplicationF sym@(Symbol _ _ _ _ (SymbolAttributes{symbolType = Function _})) sorts args)
+
+{-# COMPLETE AndTerm, ConsApplication, FunctionApplication, DomainValue, Var, Injection, KMap, KList, KSet #-}

booster/library/Booster/Pattern/Binary.hs

@@ -214,7 +214,7 @@ lookupKoreDefinitionSymbol name = DecodeM $ do
                     []
                     (SortApp "UNKNOWN" [])
                     ( SymbolAttributes
-                        PartialFunction
+                        (Function Booster.Definition.Attributes.Base.Partial)
                         IsNotIdem
                         IsNotAssoc
                         IsNotMacroOrAlias

booster/library/Booster/Pattern/Bool.hs

@@ -26,9 +26,10 @@ module Booster.Pattern.Bool (
 import Data.ByteString.Char8 (ByteString)
 
 import Booster.Definition.Attributes.Base (
+    FunctionType (..),
     SMTType (SMTHook),
     SymbolAttributes (SymbolAttributes),
-    SymbolType (TotalFunction),
+    SymbolType (Function),
     pattern CanBeEvaluated,
     pattern IsNotAssoc,
     pattern IsNotIdem,
@@ -54,7 +55,7 @@ import Booster.SMT.Base (SExpr (Atom), SMTId (..))
 pattern HookedTotalFunction :: ByteString -> SymbolAttributes
 pattern HookedTotalFunction hook =
     SymbolAttributes
-        TotalFunction
+        (Function Total)
         IsNotIdem
         IsNotAssoc
         IsNotMacroOrAlias
@@ -66,7 +67,7 @@ pattern HookedTotalFunction hook =
 pattern HookedTotalFunctionWithSMT :: ByteString -> ByteString -> SymbolAttributes
 pattern HookedTotalFunctionWithSMT hook smt =
     SymbolAttributes
-        TotalFunction
+        (Function Total)
         IsNotIdem
         IsNotAssoc
         IsNotMacroOrAlias