diff --git a/library/Booster/Definition/Ceil.hs b/library/Booster/Definition/Ceil.hs index 4b27214f..da27ff6a 100644 --- a/library/Booster/Definition/Ceil.hs +++ b/library/Booster/Definition/Ceil.hs @@ -143,7 +143,7 @@ computeCeilRule mllvm def r@RewriteRule.RewriteRule{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 diff --git a/library/Booster/Pattern/ApplyEquations.hs b/library/Booster/Pattern/ApplyEquations.hs index dbc39705..4c29ecda 100644 --- a/library/Booster/Pattern/ApplyEquations.hs +++ b/library/Booster/Pattern/ApplyEquations.hs @@ -73,7 +73,7 @@ import Booster.LLVM qualified as LLVM import Booster.Pattern.Base import Booster.Pattern.Bool import Booster.Pattern.Index -import Booster.Pattern.Match +import Booster.Pattern.UnifiedMatcher import Booster.Pattern.Util import Booster.Prettyprinter (renderDefault, renderText) import Booster.SMT.Interface qualified as SMT @@ -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 Fun 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) /\ diff --git a/library/Booster/Pattern/Match.hs b/library/Booster/Pattern/Match.hs deleted file mode 100644 index 42a54cdb..00000000 --- a/library/Booster/Pattern/Match.hs +++ /dev/null @@ -1,475 +0,0 @@ -{- | -Copyright : (c) Runtime Verification, 2022 -License : BSD-3-Clause --} -module Booster.Pattern.Match ( - MatchResult (..), - MatchFailReason (..), - matchTerm, - matchPredicate, -) where - -import Control.Monad -import Control.Monad.Trans.Class -import Control.Monad.Trans.Except -import Control.Monad.Trans.State -import Data.Bifunctor (first) -import Data.Either.Extra -import Data.Map (Map) -import Data.Map qualified as Map -import Data.Maybe (fromMaybe) -import Data.Sequence (Seq (..), (><)) -import Data.Sequence qualified as Seq -import Data.Set (Set) -import Data.Set qualified as Set -import Prettyprinter - -import Booster.Definition.Base -import Booster.Pattern.Base -import Booster.Pattern.Unify (FailReason (..), SortError, checkSubsort) -import Booster.Pattern.Util ( - checkSymbolIsAc, - freeVariables, - isConcrete, - isConstructorSymbol, - isFunctionSymbol, - sortOfTerm, - substituteInTerm, - ) - --- | Result of matching a pattern to a subject (unification, failure, or indeterminate) -data MatchResult - = -- | found a matching substitution - MatchSuccess (Map Variable Term) - | -- | pattern and subject have differences (using same failure type as unification) - MatchFailed MatchFailReason - | -- | match cannot be determined - MatchIndeterminate Term Term - deriving stock (Eq, Show) - -data MatchFailReason - = -- | shared with unification - General FailReason - | -- | Shared variables between matching terms - SharedVariables (Set Variable) - | -- | Subsorting related errors - SubsortingError SortError - | -- | The two terms have differing argument lengths - ArgLengthsDiffer Term Term - deriving stock (Eq, Show) - -instance Pretty MatchFailReason where - pretty = \case - General reason -> pretty reason - SharedVariables vs -> "Shared variables:" <+> hsep (map pretty $ Set.toList vs) - SubsortingError err -> pretty $ show err - ArgLengthsDiffer t1 t2 -> vsep ["Argument length differ", pretty t1, pretty t2] - -{- | Attempts to find a matching substitution for the given - term1 to term2. - - Symbols (functions and constructors) are matched syntactically, - i.e., when present in the pattern (term1) they also need to be - present in the subject (term2). --} -matchTerm :: KoreDefinition -> Term -> Term -> MatchResult -matchTerm KoreDefinition{sorts} term1 term2 = - let runMatching :: MatchState -> MatchResult - runMatching = - fromEither - . runExcept - . fmap (MatchSuccess . mSubstitution) - . execStateT matching - freeVars1 = freeVariables term1 - freeVars2 = freeVariables term2 - sharedVars = freeVars1 `Set.intersection` freeVars2 - in if not $ Set.null sharedVars - then MatchFailed $ SharedVariables sharedVars - else - runMatching - State - { mSubstitution = Map.empty - , mQueue = Seq.singleton (term1, term2) - , mMapQueue = mempty - , mSubsorts = Map.map snd sorts - } - -data MatchState = State - { mSubstitution :: Map Variable Term - , mQueue :: Seq (Term, Term) -- work queue - , mMapQueue :: Seq (Term, Term) -- work queue for Map/Set matching (2nd priority) - , mSubsorts :: Map SortName (Set SortName) - } - -matching :: StateT MatchState (Except MatchResult) () -matching = do - st <- get - case st.mQueue of - (term1, term2) :<| rest -> do - modify $ \s -> s{mQueue = rest} - match1 term1 term2 - matching - Empty -> - case st.mMapQueue of - (term1, term2) :<| rest -> do - modify $ \s -> s{mMapQueue = rest} - match1 term1 term2 - matching - Empty -> pure () -- done - -match1 :: - Term -> - Term -> - StateT MatchState (Except MatchResult) () ------ Variables --- pattern term is a (target) variable: check sorts, introduce a new binding - --- Matching term2 with term1, when term2 is a variable is safe here, --- because functional equations are ordered. --- Consider a function f: --- --- rule f(foo(A)) => baz() [priority(40)] --- rule f(A) => A --- where foo() is a constructor and A is a variable. --- --- We can safely match f(foo(X)) and rewrite to baz(), because there --- are no preceding equations involving the constructor foo. --- --- If instead there was a higher-priority rule --- --- rule f(foo(bar())) => flob() [priority(30)] --- --- the preceding match would be indeterminate and the function --- application would be aborted before reaching the --- f(foo(A)) => baz() --- case. --- --- Finally, if the rules had the opposite priorities --- --- rule f(foo(A)) => baz() [priority(30)] --- rule f(foo(bar())) => flob() [priority(40)] --- rule f(A) => A --- --- Since function equations are ordered, the pattern --- f(foo(bar())) => flob() --- would be unreachable anyway, hence --- f(foo(A)) => baz() --- must always apply to f(foo(X)) - - -match1 t1@AndTerm{} t2@AndTerm{} = indeterminate t1 t2 -match1 t1@AndTerm{} t2@DomainValue{} = matchAndTerm t1 t2 -match1 t1@AndTerm{} t2@Injection{} = matchAndTerm t1 t2 -match1 t1@AndTerm{} t2@KMap{} = matchAndTerm t1 t2 -match1 t1@AndTerm{} t2@KList{} = matchAndTerm t1 t2 -match1 t1@AndTerm{} t2@KSet{} = matchAndTerm t1 t2 -match1 t1@AndTerm{} t2@ConsApplication{} = matchAndTerm t1 t2 -match1 t1@AndTerm{} t2@FunctionApplication{} = matchAndTerm t1 t2 -match1 t1@AndTerm{} t2@Var{} = indeterminate t1 t2 -match1 t1@DomainValue{} t2@AndTerm{} = indeterminate t1 t2 -match1 t1@DomainValue{} t2@DomainValue{} = matchDVDV t1 t2 -match1 t1@DomainValue{} t2@Injection{} = failWith $ DifferentValues t1 t2 -match1 t1@DomainValue{} t2@KMap{} = failWith $ DifferentValues t1 t2 -match1 t1@DomainValue{} t2@KList{} = failWith $ DifferentValues t1 t2 -match1 t1@DomainValue{} t2@KSet{} = failWith $ DifferentValues t1 t2 -match1 t1@DomainValue{} t2@ConsApplication{} = failWith $ DifferentValues t1 t2 -match1 t1@DomainValue{} t2@FunctionApplication{} = indeterminate t1 t2 -match1 t1@DomainValue{} t2@Var{} = indeterminate t1 t2 -match1 t1@Injection{} t2@AndTerm{} = indeterminate t1 t2 -match1 t1@Injection{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 t1@Injection{} t2@Injection{} = matchInjInj t1 t2 -match1 t1@Injection{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 t1@Injection{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -match1 t1@Injection{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 t1@Injection{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -match1 t1@Injection{} t2@FunctionApplication{} = indeterminate t1 t2 -match1 t1@Injection{} t2@Var{} = indeterminate t1 t2 -match1 t1@KMap{} t2@AndTerm{} = indeterminate t1 t2 -match1 t1@KMap{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 t1@KMap{} t2@Injection{} = indeterminate t1 t2 -match1 t1@KMap{} t2@KMap{} = matchKMap t1 t2 -match1 t1@KMap{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -match1 t1@KMap{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 t1@KMap{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -match1 t1@KMap{} t2@FunctionApplication{} = indeterminate t1 t2 -match1 t1@KMap{} t2@Var{} = indeterminate t1 t2 -match1 t1@KList{} t2@AndTerm{} = indeterminate t1 t2 -match1 t1@KList{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 t1@KList{} t2@Injection{} = indeterminate t1 t2 -match1 t1@KList{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 t1@KList{} t2@KList{} = indeterminate t1 t2 -match1 t1@KList{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 t1@KList{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -match1 t1@KList{} t2@FunctionApplication{} = indeterminate t1 t2 -match1 t1@KList{} t2@Var{} = indeterminate t1 t2 -match1 t1@KSet{} t2@AndTerm{} = indeterminate t1 t2 -match1 t1@KSet{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 t1@KSet{} t2@Injection{} = indeterminate t1 t2 -match1 t1@KSet{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 t1@KSet{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -match1 t1@KSet{} t2@KSet{} = indeterminate t1 t2 -match1 t1@KSet{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -match1 t1@KSet{} t2@FunctionApplication{} = indeterminate t1 t2 -match1 t1@KSet{} t2@Var{} = indeterminate t1 t2 -match1 t1@ConsApplication{} t2@AndTerm{} = indeterminate t1 t2 -match1 t1@ConsApplication{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 t1@ConsApplication{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -match1 t1@ConsApplication{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 t1@ConsApplication{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -match1 t1@ConsApplication{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 t1@ConsApplication{} t2@ConsApplication{} = matchSymbolApplicationSymbolApplication t1 t2 -match1 t1@ConsApplication{} t2@FunctionApplication{} = matchSymbolApplicationSymbolApplication t1 t2 -match1 t1@ConsApplication{} t2@Var{} = indeterminate t1 t2 -match1 t1@FunctionApplication{} t2@AndTerm{} = indeterminate t1 t2 -match1 t1@FunctionApplication{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 t1@FunctionApplication{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -match1 t1@FunctionApplication{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 t1@FunctionApplication{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -match1 t1@FunctionApplication{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 t1@FunctionApplication{} t2@ConsApplication{} = matchSymbolApplicationSymbolApplication t1 t2 -match1 t1@FunctionApplication{} t2@FunctionApplication{} = matchSymbolApplicationSymbolApplication t1 t2 -match1 t1@FunctionApplication{} t2@Var{} = indeterminate t1 t2 -match1 t1@Var{} t2@AndTerm{} = matchVar t1 t2 -match1 t1@Var{} t2@DomainValue{} = matchVar t1 t2 -match1 t1@Var{} t2@Injection{} = matchVar t1 t2 -match1 t1@Var{} t2@KMap{} = matchVar t1 t2 -match1 t1@Var{} t2@KList{} = matchVar t1 t2 -match1 t1@Var{} t2@KSet{} = matchVar t1 t2 -match1 t1@Var{} t2@ConsApplication{} = matchVar t1 t2 -match1 t1@Var{} t2@FunctionApplication{} = matchVar t1 t2 -match1 t1@Var{} t2@Var{} = matchVar t1 t2 - - - -matchVar - term1@(Var var@Variable{variableSort}) - term2 = - do - let termSort = sortOfTerm term2 - subsorts <- gets mSubsorts - isSubsort <- - lift . withExcept (MatchFailed . SubsortingError) $ - checkSubsort subsorts termSort variableSort - unless isSubsort $ - failWith $ - DifferentSorts term1 term2 - -- TODO are subsorts allowed? - bindVariable - var - ( if termSort == variableSort - then term2 - else Injection termSort variableSort term2 - ) - - ------ Domain values -matchDVDV - d1@(DomainValue s1 t1) - subj@(DomainValue s2 t2) = do - unless (t1 == t2) $ - failWith (DifferentValues d1 subj) - unless (s1 == s2) $ -- sorts must be exactly the same for DVs - failWith (DifferentSorts d1 subj) - ------ And Terms --- and-term in pattern: must unify with both arguments (typically used --- to bind variables while also matching) -matchAndTerm - (AndTerm t1a t1b) - term2 = - do - enqueueProblem t1a term2 - enqueueProblem t1b term2 ------ Injections - -matchInjInj - inj@(Injection source1 target1 trm1) - subj@(Injection source2 target2 trm2) - | target1 /= target2 = do - failWith (DifferentSorts inj subj) - | source1 == source2 = do - enqueueProblem trm1 trm2 - | Var v <- trm1 = do - -- variable in pattern, check source sorts and bind - subsorts <- gets mSubsorts - isSubsort <- - lift . withExcept (MatchFailed . SubsortingError) $ - checkSubsort subsorts source2 source1 - if isSubsort - then bindVariable v (Injection source2 source1 trm2) - else failWith (DifferentSorts trm1 trm2) - | otherwise = - failWith (DifferentSorts inj subj) - - - ------ Symbol Applications -matchSymbolApplicationSymbolApplication - app@(SymbolApplication symbol1 sorts1 args1) - subj@(SymbolApplication symbol2 sorts2 args2) - | symbol1.name /= symbol2.name = - if isConstructorSymbol symbol1 && isConstructorSymbol symbol2 - then failWith (DifferentSymbols app subj) - else indeterminate app subj - | length args1 /= length args2 = - lift $ throwE $ MatchFailed $ ArgLengthsDiffer app subj - | sorts1 /= sorts2 = - failWith (DifferentSorts app subj) - -- If the symbol is non-free (AC symbol), return indeterminate - | checkSymbolIsAc symbol1 = - indeterminate app subj - | otherwise = - enqueueProblems $ Seq.fromList $ zip args1 args2 - ------ KMap -matchKMap - t1@(KMap patDef patKeyVals patRest) - t2@(KMap subjDef subjKeyVals subjRest) = do - -- different map sorts do not match - unless (patDef == subjDef) $ - failWith (DifferentSorts t1 t2) - st <- get - if not (Seq.null st.mQueue) - then -- delay matching 'KMap's until there are no regular - -- problems left, to obtain a maximal prior substitution - -- before matching map keys. - enqueueMapProblem t1 t2 - else do - -- first apply current substitution to pattern key-value pairs - let patternKeyVals = map (first (substituteInTerm st.mSubstitution)) patKeyVals - - -- check for duplicate keys - checkDuplicateKeys (KMap patDef patternKeyVals patRest) - checkDuplicateKeys t2 - - let patMap = Map.fromList patternKeyVals - subjMap = Map.fromList subjKeyVals - -- handles syntactically identical keys in pattern and subject - commonMap = Map.intersectionWith (,) patMap subjMap - patExtra = patMap `Map.withoutKeys` Map.keysSet commonMap - subjExtra = subjMap `Map.withoutKeys` Map.keysSet commonMap - - -- Before enqueueing the common elements for matching, - -- check whether we can abort early - case (Map.null patExtra, Map.null subjExtra) of - (True, True) -> - -- all keys are common, handle opaque rest (if any) - case patRest of - Nothing -> - maybe (pure ()) (enqueueProblem emptyMap) subjRest - Just pRest -> - enqueueProblem pRest $ fromMaybe emptyMap subjRest - (True, False) -> - -- subject has extra assocs to match with pattern rest - let subj' = KMap subjDef (Map.assocs subjExtra) subjRest - in case patRest of - Nothing -> - failWith $ DifferentValues emptyMap subj' - Just pRest -> do - enqueueProblem pRest subj' - (False, True) -> - -- pattern has extra assocs - let pat' = KMap patDef (Map.assocs patExtra) patRest - in case subjRest of - Nothing -> - -- no opaque rest, match is definitely failing - failWith $ DifferentValues pat' emptyMap - Just sRest -> - -- indeterminate matching with an opaque rest - indeterminate pat' sRest - (False, False) - -- Special case: definitely fail if all (extra) pattern keys are concrete - -- and there is no opaque subject rest - | Nothing <- subjRest - , all isConcrete (Map.keys patExtra) -> - let pat' = KMap patDef (Map.assocs patExtra) patRest - subj' = KMap subjDef (Map.assocs subjExtra) subjRest - in failWith $ DifferentValues pat' subj' - -- Special case: attempt a match if pattern and subject assocs - -- are singleton and there is no opaque subject rest - | Nothing <- subjRest - , [(pKey, pVal)] <- Map.assocs patExtra - , [(sKey, sVal)] <- Map.assocs subjExtra -> do - let opaque = case patRest of - Nothing -> [] - Just rest -> [(rest, emptyMap)] - enqueueProblems . Seq.fromList $ (pKey, sKey) : (pVal, sVal) : opaque - | otherwise -> - indeterminate t1 t2 - - -- enqueue common elements for matching unless already failed - enqueueProblems $ Seq.fromList $ Map.elems commonMap - where - emptyMap = KMap patDef [] Nothing - - checkDuplicateKeys m@(KMap _ assocs _) = - let duplicates = - Map.filter (> (1 :: Int)) $ foldr (flip (Map.insertWith (+)) 1 . fst) mempty assocs - in case Map.assocs duplicates of - [] -> pure () - (k, _) : _ -> failWith $ DuplicateKeys k m - checkDuplicateKeys _ = pure () - - - -failWith :: FailReason -> StateT s (Except MatchResult) () -failWith = lift . throwE . MatchFailed . General - -indeterminate :: Term -> Term -> StateT s (Except MatchResult) () -indeterminate t1 t2 = lift . throwE $ MatchIndeterminate t1 t2 - -enqueueProblem :: Monad m => Term -> Term -> StateT MatchState m () -enqueueProblem term1 term2 = - modify $ \s@State{mQueue} -> s{mQueue = mQueue :|> (term1, term2)} - -enqueueMapProblem :: Monad m => Term -> Term -> StateT MatchState m () -enqueueMapProblem term1 term2 = - modify $ \s@State{mMapQueue} -> s{mMapQueue = mMapQueue :|> (term1, term2)} - -enqueueProblems :: Monad m => Seq (Term, Term) -> StateT MatchState m () -enqueueProblems ts = - modify $ \s@State{mQueue} -> s{mQueue = mQueue >< ts} - -{- | Binds a variable to a term to add to the resulting unifier. - - We apply the accumulated substitution whenever a new variable - binding to a term is added. This avoids repeated traversals while - guarding against substitution loops. --} -bindVariable :: Variable -> Term -> StateT MatchState (Except MatchResult) () -bindVariable var term = do - currentSubst <- gets mSubstitution - case Map.lookup var currentSubst of - Just oldTerm - | oldTerm == term -> pure () -- already bound - | otherwise -> - -- only consider full syntactic match, not equivalence - failWith $ VariableConflict var oldTerm term - Nothing -> do - let - -- apply existing substitutions to term - term' = substituteInTerm currentSubst term - when (var `Set.member` freeVariables term') $ - failWith (VariableRecursion var term) - let - -- substitute in existing substitution terms - currentSubst' = - Map.map (substituteInTerm $ Map.singleton var term') currentSubst - newSubst = Map.insert var term' currentSubst' - modify $ \s -> s{mSubstitution = newSubst} - ----------------------------------------- - -{- | Match a predicate pattern (containing boolean terms) to a predicate - subject, by matching the contained terms. - - This will probably not be used in the booster, as we only accept - predicates which are boolean terms compared to true or false. --} -matchPredicate :: - KoreDefinition -> - Predicate -> - Predicate -> - MatchResult -matchPredicate def (Predicate pat) (Predicate subj) = - matchTerm def pat subj diff --git a/library/Booster/Pattern/Rewrite.hs b/library/Booster/Pattern/Rewrite.hs index 2f135436..b048e420 100644 --- a/library/Booster/Pattern/Rewrite.hs +++ b/library/Booster/Pattern/Rewrite.hs @@ -52,7 +52,7 @@ import Booster.Pattern.ApplyEquations qualified as ApplyEquations import Booster.Pattern.Base import Booster.Pattern.Bool import Booster.Pattern.Index (TermIndex (..), kCellTermIndex) -import Booster.Pattern.Unify +import Booster.Pattern.UnifiedMatcher import Booster.Pattern.Util import Booster.Prettyprinter import Booster.SMT.Interface qualified as SMT @@ -257,15 +257,14 @@ applyRule :: applyRule pat@Pattern{ceilConditions} rule = runRewriteRuleAppT $ do def <- lift getDefinition -- unify terms - let unified = unifyTerms def rule.lhs pat.term - subst <- case unified of - UnificationFailed _reason -> - fail "Unification failed" - UnificationSortError sortError -> + subst <- case matchTerms Rule def rule.lhs pat.term of + MatchFailed (SubsortingError sortError) -> failRewrite $ RewriteSortError rule pat.term sortError - UnificationRemainder remainder -> + MatchFailed _reason -> + fail "Rule matching failed" + MatchIndeterminate remainder -> failRewrite $ RuleApplicationUnclear rule pat.term remainder - UnificationSuccess substitution -> + MatchSuccess substitution -> pure substitution -- check it is a "matching" substitution (substitutes variables diff --git a/library/Booster/Pattern/Unify.hs b/library/Booster/Pattern/UnifiedMatcher.hs similarity index 50% rename from library/Booster/Pattern/Unify.hs rename to library/Booster/Pattern/UnifiedMatcher.hs index 8ae3c326..d2148b1f 100644 --- a/library/Booster/Pattern/Unify.hs +++ b/library/Booster/Pattern/UnifiedMatcher.hs @@ -3,11 +3,12 @@ Copyright : (c) Runtime Verification, 2022 License : BSD-3-Clause -} {-# OPTIONS_GHC -Wno-incomplete-patterns #-} -module Booster.Pattern.Unify ( - UnificationResult (..), +module Booster.Pattern.UnifiedMatcher ( + MatchResult (..), + MatchType (..), FailReason (..), Substitution, - unifyTerms, + matchTerms, checkSubsort, SortError (..), ) where @@ -32,26 +33,25 @@ import Booster.Definition.Base import Booster.Pattern.Base import Booster.Pattern.Util ( freeVariables, - isFunctionSymbol, sortOfTerm, - substituteInTerm, + substituteInTerm, checkSymbolIsAc, isConstructorSymbol, ) import Data.List (partition) import Data.ByteString (ByteString) -import Booster.Definition.Attributes.Base (SymbolType(..), SymbolAttributes (..), KListDefinition) +import Booster.Definition.Attributes.Base (KListDefinition) --- | Result of a unification (a substitution or an indication of what went wrong) -data UnificationResult +-- | Result of matching a pattern to a subject (a substitution or an indication of what went wrong) +data MatchResult = -- | equal structure (constructors) after substitution (substitution goes both ways) - UnificationSuccess Substitution + MatchSuccess Substitution | -- | different constructors or domain values, or sort mismatch - UnificationFailed FailReason + MatchFailed FailReason | -- | (other) cases that are unresolved (offending case in head position). - UnificationRemainder (NonEmpty (Term, Term)) - | -- | sort error (using variables or unknown sorts) - UnificationSortError SortError + MatchIndeterminate (NonEmpty (Term, Term)) deriving stock (Eq, Show) +data MatchType = Rule | Fun deriving Eq + -- | Additional information to explain why a unification has failed data FailReason = -- | (Domain) values differ @@ -69,6 +69,12 @@ data FailReason KeyNotFound Term Term | -- | Key not found in map DuplicateKeys Term Term + | -- | Shared variables between matching terms + SharedVariables (Set Variable) + | -- | sort error (using variables or unknown sorts) + SubsortingError SortError + | -- | The two terms have differing argument lengths + ArgLengthsDiffer Term Term deriving stock (Eq, Show) instance Pretty FailReason where @@ -109,163 +115,185 @@ type Substitution = Map Variable Term arguments that should not be possible), assuming the caller will catch and handle those errors. -} -unifyTerms :: KoreDefinition -> Term -> Term -> UnificationResult -unifyTerms KoreDefinition{sorts} term1 term2 = - let runUnification :: UnificationState -> UnificationResult - runUnification = +matchTerms :: MatchType -> KoreDefinition -> Term -> Term -> MatchResult +matchTerms mType KoreDefinition{sorts} term1 term2 = + let runMatch :: MatchState -> MatchResult + runMatch = fromEither . runExcept - . fmap (UnificationSuccess . uSubstitution) - . execStateT unification + . fmap (MatchSuccess . mSubstitution) + . execStateT (match mType) freeVars1 = freeVariables term1 freeVars2 = freeVariables term2 sharedVars = freeVars1 `Set.intersection` freeVars2 in if not $ Set.null sharedVars then - UnificationRemainder $ + MatchIndeterminate $ NE.fromList [(Var v, Var v) | v <- Set.toList sharedVars] else - runUnification + runMatch State - { uSubstitution = Map.empty - , uTargetVars = freeVars1 - , uQueue = Seq.singleton (term1, term2) -- PriorityQueue.singleton (term1, term2) RegularTerm () - , uMapQueue = mempty - , uIndeterminate = [] - , uSubsorts = Map.map snd sorts + { mSubstitution = Map.empty + , mTargetVars = freeVars1 + , mQueue = Seq.singleton (term1, term2) -- PriorityQueue.singleton (term1, term2) RegularTerm () + , mMapQueue = mempty + , mIndeterminate = [] + , mSubsorts = Map.map snd sorts } -data UnificationState = State - { uSubstitution :: Substitution - , uTargetVars :: Set Variable - , uQueue :: Seq (Term, Term) -- PriorityQueue.HashPSQ (Term, Term) UnificationPriority () -- work queue with a priority - , uMapQueue :: Seq (Term, Term) - , uIndeterminate :: [(Term, Term)] -- list of postponed indeterminate terms (function results) - , uSubsorts :: SortTable +data MatchState = State + { mSubstitution :: Substitution + , mTargetVars :: Set Variable + , mQueue :: Seq (Term, Term) -- PriorityQueue.HashPSQ (Term, Term) UnificationPriority () -- work queue with a priority + , mMapQueue :: Seq (Term, Term) + , mIndeterminate :: [(Term, Term)] -- list of postponed indeterminate terms (function results) + , mSubsorts :: SortTable } type SortTable = Map SortName (Set SortName) -unification :: StateT UnificationState (Except UnificationResult) () -unification = do - queue <- gets uQueue - mapQueue <- gets uMapQueue +match :: MatchType -> StateT MatchState (Except MatchResult) () +match mType = do + queue <- gets mQueue + mapQueue <- gets mMapQueue case queue of Empty -> case mapQueue of Empty -> checkIndeterminate -- done (term1, term2) :<| rest -> do - modify $ \s -> s{uMapQueue = rest} - unify1 term1 term2 - unification + modify $ \s -> s{mMapQueue = rest} + match1 mType term1 term2 + match mType (term1, term2) :<| rest -> do -- case PriorityQueue.minView queue of -- Nothing -> checkIndeterminate -- done -- Just ((term1, term2), _, _, rest) -> do - modify $ \s -> s{uQueue = rest} - unify1 term1 term2 - unification + modify $ \s -> s{mQueue = rest} + match1 mType term1 term2 + match mType -checkIndeterminate :: StateT UnificationState (Except UnificationResult) () +checkIndeterminate :: StateT MatchState (Except MatchResult) () checkIndeterminate = do - indeterminate <- gets uIndeterminate + indeterminate <- gets mIndeterminate unless (null indeterminate) . lift $ - throwE (UnificationRemainder $ NE.fromList indeterminate) - -unify1 :: + throwE (MatchIndeterminate $ NE.fromList indeterminate) +match1 :: + MatchType -> Term -> Term -> - StateT UnificationState (Except UnificationResult) () ------ Domain values --- two domain values: have to fully agree - - -unify1 (AndTerm t1a t1b) t2@AndTerm{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -unify1 (AndTerm t1a t1b) t2@DomainValue{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -unify1 (AndTerm t1a t1b) t2@Injection{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -unify1 (AndTerm t1a t1b) t2@KMap{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -unify1 (AndTerm t1a t1b) t2@KList{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -unify1 (AndTerm t1a t1b) t2@KSet{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -unify1 (AndTerm t1a t1b) t2@ConsApplication{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -unify1 (AndTerm t1a t1b) t2@FunctionApplication{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -unify1 (AndTerm t1a t1b) t2@Var{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -unify1 t1@DomainValue{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -unify1 (DomainValue s1 t1) (DomainValue s2 t2) = unifyDV s1 t1 s2 t2 -unify1 t1@DomainValue{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@DomainValue{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@DomainValue{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@DomainValue{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@DomainValue{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@DomainValue{} t2@FunctionApplication{} = addIndeterminate t1 t2 -unify1 t1@DomainValue{} (Var var2) = unifyVar var2 t1 -unify1 t1@Injection{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -unify1 t1@Injection{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -unify1 (Injection source1 target1 trm1) (Injection source2 target2 trm2) = unifyInj source1 target1 trm1 source2 target2 trm2 -unify1 t1@Injection{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@Injection{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@Injection{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@Injection{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@Injection{} t2@FunctionApplication{} = addIndeterminate t1 t2 -unify1 t1@Injection{} t2@Var{} = addIndeterminate t1 t2 -unify1 t1@KMap{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -unify1 t1@KMap{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KMap{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KMap{} t2@KMap{} = unifyMap t1 t2 -unify1 t1@KMap{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KMap{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KMap{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KMap{} t2@FunctionApplication{} = addIndeterminate t1 t2 -unify1 t1@KMap{} (Var var2) = unifyVar var2 t1 -unify1 t1@KList{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -unify1 t1@KList{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KList{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KList{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -unify1 (KList def1 heads1 rest1) (KList def2 heads2 rest2) = unifyList def1 heads1 rest1 def2 heads2 rest2 -unify1 t1@KList{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KList{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KList{} t2@FunctionApplication{} = addIndeterminate t1 t2 -unify1 t1@KList{} (Var var2) = unifyVar var2 t1 -unify1 t1@KSet{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -unify1 t1@KSet{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KSet{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KSet{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KSet{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KSet{} t2@KSet{} = addIndeterminate t1 t2 -unify1 t1@KSet{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@KSet{} t2@FunctionApplication{} = addIndeterminate t1 t2 -unify1 t1@KSet{} (Var var2) = unifyVar var2 t1 -unify1 t1@ConsApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -unify1 t1@ConsApplication{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@ConsApplication{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@ConsApplication{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@ConsApplication{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -unify1 t1@ConsApplication{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -unify1 (ConsApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = unifyConss symbol1 sorts1 args1 symbol2 sorts2 args2 -unify1 t1@ConsApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2 -unify1 t1@ConsApplication{} (Var var2) = unifyVar var2 t1 -unify1 t1@FunctionApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -unify1 t1@FunctionApplication{} t2@DomainValue{} = addIndeterminate t1 t2 -unify1 t1@FunctionApplication{} t2@Injection{} = addIndeterminate t1 t2 -unify1 t1@FunctionApplication{} t2@KMap{} = addIndeterminate t1 t2 -unify1 t1@FunctionApplication{} t2@KList{} = addIndeterminate t1 t2 -unify1 t1@FunctionApplication{} t2@KSet{} = addIndeterminate t1 t2 -unify1 t1@FunctionApplication{} t2@ConsApplication{} = addIndeterminate t1 t2 -unify1 t1@FunctionApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2 -unify1 t1@FunctionApplication{} (Var var2) = unifyVar var2 t1 -unify1 t1@Var{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -unify1 (Var var1) t2@DomainValue{} = unifyVar var1 t2 -unify1 (Var var1) t2@Injection{} = unifyVar var1 t2 -unify1 (Var var1) t2@KMap{} = unifyVar var1 t2 -unify1 (Var var1) t2@KList{} = unifyVar var1 t2 -unify1 (Var var1) t2@KSet{} = unifyVar var1 t2 -unify1 (Var var1) t2@ConsApplication{} = unifyVar var1 t2 -unify1 (Var var1) t2@FunctionApplication{} = unifyVar var1 t2 -unify1 (Var var1) t2@Var{} = unifyVar var1 t2 - - - -unifyDV :: Sort -> ByteString -> Sort -> ByteString -> StateT s (Except UnificationResult) () -unifyDV + StateT MatchState (Except MatchResult) () +match1 Rule (AndTerm t1a t1b) t2@AndTerm{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 +match1 Fun t1@AndTerm{} t2@AndTerm{} = addIndeterminate t1 t2 +match1 _ (AndTerm t1a t1b) t2@DomainValue{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 +match1 _ (AndTerm t1a t1b) t2@Injection{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 +match1 _ (AndTerm t1a t1b) t2@KMap{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 +match1 _ (AndTerm t1a t1b) t2@KList{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 +match1 _ (AndTerm t1a t1b) t2@KSet{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 +match1 _ (AndTerm t1a t1b) t2@ConsApplication{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 +match1 _ (AndTerm t1a t1b) t2@FunctionApplication{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 +match1 _ (AndTerm t1a t1b) t2@Var{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 +match1 _ t1@DomainValue{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b +match1 _ (DomainValue s1 t1) (DomainValue s2 t2) = matchDV s1 t1 s2 t2 +match1 _ t1@DomainValue{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@DomainValue{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@DomainValue{} t2@KList{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@DomainValue{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@DomainValue{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@DomainValue{} t2@FunctionApplication{} = addIndeterminate t1 t2 +match1 Rule t1@DomainValue{} (Var var2) = matchVar Rule var2 t1 +match1 Fun t1@DomainValue{} t2@Var{} = addIndeterminate t1 t2 +match1 Rule t1@Injection{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b +match1 Fun t1@Injection{} t2@AndTerm{} = addIndeterminate t1 t2 +match1 _ t1@Injection{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 +match1 mTy (Injection source1 target1 trm1) (Injection source2 target2 trm2) = matchInj mTy source1 target1 trm1 source2 target2 trm2 +match1 _ t1@Injection{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@Injection{} t2@KList{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@Injection{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@Injection{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@Injection{} t2@FunctionApplication{} = addIndeterminate t1 t2 +match1 _ t1@Injection{} t2@Var{} = addIndeterminate t1 t2 +match1 Rule t1@KMap{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b +match1 Fun t1@KMap{} t2@AndTerm{} = addIndeterminate t1 t2 +match1 _ t1@KMap{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 +match1 Rule t1@KMap{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 +match1 Fun t1@KMap{} t2@Injection{} = addIndeterminate t1 t2 +match1 _ t1@KMap{} t2@KMap{} = matchMap t1 t2 +match1 _ t1@KMap{} t2@KList{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@KMap{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@KMap{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@KMap{} t2@FunctionApplication{} = addIndeterminate t1 t2 +match1 Rule t1@KMap{} (Var var2) = matchVar Rule var2 t1 +match1 Fun t1@KMap{} t2@Var{} = addIndeterminate t1 t2 +match1 Rule t1@KList{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b +match1 Fun t1@KList{} t2@AndTerm{} = addIndeterminate t1 t2 +match1 _ t1@KList{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 +match1 Rule t1@KList{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 +match1 Fun t1@KList{} t2@Injection{} = addIndeterminate t1 t2 +match1 _ t1@KList{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 +match1 Rule (KList def1 heads1 rest1) (KList def2 heads2 rest2) = unifyList def1 heads1 rest1 def2 heads2 rest2 +match1 Fun t1@KList{} t2@KList{} = addIndeterminate t1 t2 +match1 _ t1@KList{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@KList{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@KList{} t2@FunctionApplication{} = addIndeterminate t1 t2 +match1 Rule t1@KList{} (Var var2) = matchVar Rule var2 t1 +match1 Fun t1@KList{} t2@Var{} = addIndeterminate t1 t2 +match1 Rule t1@KSet{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b +match1 Fun t1@KSet{} t2@AndTerm{} = addIndeterminate t1 t2 +match1 _ t1@KSet{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 +match1 Rule t1@KSet{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 +match1 Fun t1@KSet{} t2@Injection{} = addIndeterminate t1 t2 +match1 _ t1@KSet{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@KSet{} t2@KList{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@KSet{} t2@KSet{} = addIndeterminate t1 t2 +match1 _ t1@KSet{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@KSet{} t2@FunctionApplication{} = addIndeterminate t1 t2 +match1 Rule t1@KSet{} (Var var2) = matchVar Rule var2 t1 +match1 Fun t1@KSet{} t2@Var{} = addIndeterminate t1 t2 +match1 Rule t1@ConsApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b +match1 Fun t1@ConsApplication{} t2@AndTerm{} = addIndeterminate t1 t2 +match1 _ t1@ConsApplication{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@ConsApplication{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@ConsApplication{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@ConsApplication{} t2@KList{} = failWith $ DifferentSymbols t1 t2 +match1 _ t1@ConsApplication{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 +match1 mTy (ConsApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = matchSymbolAplications mTy symbol1 sorts1 args1 symbol2 sorts2 args2 +match1 Rule t1@ConsApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2 +match1 Fun (ConsApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Fun symbol1 sorts1 args1 symbol2 sorts2 args2 +match1 Rule t1@ConsApplication{} (Var var2) = matchVar Rule var2 t1 +match1 Fun t1@ConsApplication{} t2@Var{} = addIndeterminate t1 t2 +match1 Rule t1@FunctionApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b +match1 Fun t1@FunctionApplication{} t2@AndTerm{} = addIndeterminate t1 t2 +match1 Rule t1@FunctionApplication{} t2@DomainValue{} = addIndeterminate t1 t2 +match1 Fun t1@FunctionApplication{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 +match1 Rule t1@FunctionApplication{} t2@Injection{} = addIndeterminate t1 t2 +match1 Fun t1@FunctionApplication{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 +match1 Rule t1@FunctionApplication{} t2@KMap{} = addIndeterminate t1 t2 +match1 Fun t1@FunctionApplication{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 +match1 Rule t1@FunctionApplication{} t2@KList{} = addIndeterminate t1 t2 +match1 Fun t1@FunctionApplication{} t2@KList{} = failWith $ DifferentSymbols t1 t2 +match1 Rule t1@FunctionApplication{} t2@KSet{} = addIndeterminate t1 t2 +match1 Fun t1@FunctionApplication{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 +match1 Rule t1@FunctionApplication{} t2@ConsApplication{} = addIndeterminate t1 t2 +match1 Fun (FunctionApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = matchSymbolAplications Fun symbol1 sorts1 args1 symbol2 sorts2 args2 +match1 Rule t1@FunctionApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2 +match1 Fun (FunctionApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Fun symbol1 sorts1 args1 symbol2 sorts2 args2 +match1 Rule t1@FunctionApplication{} (Var var2) = matchVar Rule var2 t1 +match1 Fun t1@FunctionApplication{} t2@Var{} = addIndeterminate t1 t2 +match1 Rule t1@Var{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b +match1 Fun (Var var1) t2@AndTerm{} = matchVar Fun var1 t2 +match1 mTy (Var var1) t2@DomainValue{} = matchVar mTy var1 t2 +match1 mTy (Var var1) t2@Injection{} = matchVar mTy var1 t2 +match1 mTy (Var var1) t2@KMap{} = matchVar mTy var1 t2 +match1 mTy (Var var1) t2@KList{} = matchVar mTy var1 t2 +match1 mTy (Var var1) t2@KSet{} = matchVar mTy var1 t2 +match1 mTy (Var var1) t2@ConsApplication{} = matchVar mTy var1 t2 +match1 mTy (Var var1) t2@FunctionApplication{} = matchVar mTy var1 t2 +match1 mTy (Var var1) t2@Var{} = matchVar mTy var1 t2 + + + +matchDV :: Sort -> ByteString -> Sort -> ByteString -> StateT s (Except MatchResult) () +matchDV s1 t1 s2 t2 = do unless (t1 == t2) $ @@ -273,13 +301,16 @@ unifyDV unless (s1 == s2) $ -- sorts must be exactly the same for DVs failWith (DifferentSorts (DomainValue s1 t1) (DomainValue s2 t2)) + + ----- Injections -- two injections. Try to unify the contained terms if the sorts -- agree. Target sorts must be the same, source sorts may differ if -- the contained pattern term is just a variable, otherwise they need -- to be identical. -unifyInj :: Sort -> Sort -> Term -> Sort -> Sort -> Term -> StateT UnificationState (Except UnificationResult) () -unifyInj +matchInj :: MatchType -> Sort -> Sort -> Term -> Sort -> Sort -> Term -> StateT MatchState (Except MatchResult) () +matchInj + mType source1 target1 trm1 source2 target2 trm2 | target1 /= target2 = do @@ -288,32 +319,54 @@ unifyInj enqueueRegularProblem trm1 trm2 | Var v <- trm1 = do -- variable in pattern, check source sorts and bind - subsorts <- gets uSubsorts + subsorts <- gets mSubsorts isSubsort <- - lift . withExcept UnificationSortError $ + lift . withExcept (MatchFailed . SubsortingError) $ checkSubsort subsorts source2 source1 if isSubsort - then bindVariable v (Injection source2 source1 trm2) + then bindVariable mType v (Injection source2 source1 trm2) else failWith (DifferentSorts trm1 trm2) | otherwise = failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2)) + ----- Symbol Applications -- two constructors: fail if names differ, recurse -unifyConss :: Symbol -> [Sort] -> [Term] -> Symbol -> [Sort] -> [Term] -> StateT UnificationState (Except UnificationResult) () -unifyConss + +----- Symbol Applications +matchSymbolAplications :: MatchType -> Symbol -> [Sort] -> [Term] -> Symbol -> [Sort] -> [Term] -> StateT MatchState (Except MatchResult) () +matchSymbolAplications + Rule symbol1 sorts1 args1 symbol2 sorts2 args2 | symbol1.name /= symbol2.name = failWith (DifferentSymbols (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2) ) | length args1 /= length args2 = - internalError $ - "Argument counts differ for same constructor" <> show (SymbolApplication symbol1 sorts1 args1, SymbolApplication symbol2 sorts2 args2) + failWith $ ArgLengthsDiffer (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2) | sorts1 /= sorts2 = failWith (DifferentSorts (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2) ) | otherwise = enqueueRegularProblems $ Seq.fromList $ zip args1 args2 +matchSymbolAplications + Fun + symbol1 sorts1 args1 + symbol2 sorts2 args2 + | symbol1.name /= symbol2.name = + if isConstructorSymbol symbol1 && isConstructorSymbol symbol2 + then failWith (DifferentSymbols (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2)) + else addIndeterminate (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2) + | length args1 /= length args2 = + failWith $ ArgLengthsDiffer (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2) + | sorts1 /= sorts2 = failWith (DifferentSorts (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2) ) + + -- If the symbol is non-free (AC symbol), return indeterminate + | checkSymbolIsAc symbol1 = + addIndeterminate (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2) + | otherwise = + enqueueRegularProblems $ Seq.fromList $ zip args1 args2 + ----- Variables -unifyVar :: Variable -> Term -> StateT UnificationState (Except UnificationResult) () -unifyVar +matchVar :: MatchType -> Variable -> Term -> StateT MatchState (Except MatchResult) () +matchVar + Rule -- twice the exact same variable: verify sorts are equal var1@(Variable varSort1 varName1) (Var var2@(Variable varSort2 varName2)) @@ -323,22 +376,23 @@ unifyVar | varName1 == varName2 && varSort1 /= varSort2 = -- sorts differ, names equal: error! failWith $ VariableConflict var1 (Var var1) (Var var2) -unifyVar +matchVar -- term1 variable (target): introduce a new binding + mType var@Variable{variableSort} term2 = do let termSort = sortOfTerm term2 - subsorts <- gets uSubsorts + subsorts <- gets mSubsorts isSubsort <- - lift . withExcept UnificationSortError $ + lift . withExcept (MatchFailed . SubsortingError) $ checkSubsort subsorts termSort variableSort if isSubsort - then bindVariable var term2 + then bindVariable mType var term2 else failWith $ DifferentSorts (Var var) term2 -- unification for lists. Only solves simple cases, returns indeterminate otherwise -unifyList :: KListDefinition -> [Term] -> Maybe (Term, [Term]) -> KListDefinition -> [Term] -> Maybe (Term, [Term]) -> StateT UnificationState (Except UnificationResult) () +unifyList :: KListDefinition -> [Term] -> Maybe (Term, [Term]) -> KListDefinition -> [Term] -> Maybe (Term, [Term]) -> StateT MatchState (Except MatchResult) () unifyList def1 heads1 rest1 def2 heads2 rest2 @@ -438,11 +492,12 @@ unifyList ------ Internalised Maps -unifyMap +matchMap :: Term -> Term -> StateT MatchState (Except MatchResult) () +matchMap t1@(KMap def1 _ _) t2@(KMap def2 _ _) | def1 == def2 = do - State{uSubstitution = currentSubst, uQueue = queue} <- get + State{mSubstitution = currentSubst, mQueue = queue} <- get case queue of Empty -> case (substituteInKeys currentSubst t1, substituteInKeys currentSubst t2) of @@ -513,34 +568,36 @@ unifyMap KMap attrs keyVals rest -> KMap attrs (first (substituteInTerm substitution) <$> keyVals) rest other -> other -failWith :: FailReason -> StateT s (Except UnificationResult) () -failWith = lift . throwE . UnificationFailed +matchMap _ _ = undefined + +failWith :: FailReason -> StateT s (Except MatchResult) () +failWith = lift . throwE . MatchFailed internalError :: String -> a internalError = error -enqueueRegularProblem, enqueueMapProblem :: Monad m => Term -> Term -> StateT UnificationState m () +enqueueRegularProblem, enqueueMapProblem :: Monad m => Term -> Term -> StateT MatchState m () enqueueRegularProblem term1 term2 = - modify $ \s@State{uQueue} -> + modify $ \s@State{mQueue} -> s - { uQueue = uQueue :|> (term1, term2) + { mQueue = mQueue :|> (term1, term2) } enqueueMapProblem term1 term2 = - modify $ \s@State{uMapQueue} -> + modify $ \s@State{mMapQueue} -> s - { uMapQueue = uMapQueue :|> (term1, term2) + { mMapQueue = mMapQueue :|> (term1, term2) } -enqueueRegularProblems :: Monad m => Seq (Term, Term) -> StateT UnificationState m () +enqueueRegularProblems :: Monad m => Seq (Term, Term) -> StateT MatchState m () enqueueRegularProblems ts = - modify $ \s@State{uQueue} -> s{uQueue = uQueue >< ts} + modify $ \s@State{mQueue} -> s{mQueue = mQueue >< ts} {- | pair up the argument lists and enqueue the pairs. If the lists are of equal length, return Nothing, else return the remaining terms in the longer list, tagged with their origin). -} enqueuePairs :: - Monad m => [Term] -> [Term] -> StateT UnificationState m (Maybe (Either [Term] [Term])) + Monad m => [Term] -> [Term] -> StateT MatchState m (Maybe (Either [Term] [Term])) enqueuePairs ts1 ts2 | l1 == l2 = enqueue ts1 ts2 >> pure Nothing @@ -556,7 +613,7 @@ enqueuePairs ts1 ts2 l2 = length ts2 enqueue xs ys = enqueueRegularProblems $ Seq.fromList $ zip xs ys --- modify $ \s@State{uQueue} -> s{uQueue = foldr (\(p, t) q -> PriorityQueue.insert t p () q) uQueue ts} +-- modify $ \s@State{mQueue} -> s{mQueue = foldr (\(p, t) q -> PriorityQueue.insert t p () q) mQueue ts} {- | Binds a variable to a term to add to the resulting unifier. @@ -564,26 +621,28 @@ enqueuePairs ts1 ts2 binding to a term is added. This avoids repeated traversals while guarding against substitution loops. -} -bindVariable :: Variable -> Term -> StateT UnificationState (Except UnificationResult) () -bindVariable var term = do - State{uSubstitution = currentSubst, uTargetVars = targets} <- get +bindVariable :: MatchType -> Variable -> Term -> StateT MatchState (Except MatchResult) () +bindVariable mType var term = do + State{mSubstitution = currentSubst, mTargetVars = targets} <- get case term of -- Check if term is a variable, prefer target variables. Should -- not happen given how we call it in the code above. Var var2 - | var2 `Set.member` targets + | mType == Rule && var2 `Set.member` targets && not (var `Set.member` targets) -> - bindVariable var2 (Var var) + bindVariable mType var2 (Var var) -- regular case _other -> do case Map.lookup var currentSubst of Just oldTerm | oldTerm == term -> pure () -- already bound - | DomainValue{} <- oldTerm, DomainValue{} <- term -> enqueueRegularProblem oldTerm term + | DomainValue{} <- oldTerm, DomainValue{} <- term, mType == Rule -> enqueueRegularProblem oldTerm term | otherwise -> -- the term in the binding could be _equivalent_ -- (not necessarily syntactically equal) to term' - addIndeterminate oldTerm term + case mType of + Rule -> addIndeterminate oldTerm term + Fun -> failWith $ VariableConflict var oldTerm term Nothing -> do let -- apply existing substitutions to term @@ -595,11 +654,11 @@ bindVariable var term = do currentSubst' = Map.map (substituteInTerm $ Map.singleton var term') currentSubst newSubst = Map.insert var term' currentSubst' - modify $ \s -> s{uSubstitution = newSubst} + modify $ \s -> s{mSubstitution = newSubst} -addIndeterminate :: Term -> Term -> StateT UnificationState (Except UnificationResult) () +addIndeterminate :: Term -> Term -> StateT MatchState (Except MatchResult) () addIndeterminate pat subj = - modify $ \s -> s{uIndeterminate = (pat, subj) : s.uIndeterminate} + modify $ \s -> s{mIndeterminate = (pat, subj) : s.mIndeterminate} {- | Matches a subject sort to a pattern sort, ensuring that the subject sort can be used in place of the pattern sort, i.e., is a subsort.