diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs index 2fdc19d18..1aaf640d8 100644 --- a/library/Booster/JsonRpc.hs +++ b/library/Booster/JsonRpc.hs @@ -816,6 +816,11 @@ mkLogRewriteTrace { 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 diff --git a/library/Booster/Pattern/Rewrite.hs b/library/Booster/Pattern/Rewrite.hs index b048e4200..5f4e0e543 100644 --- a/library/Booster/Pattern/Rewrite.hs +++ b/library/Booster/Pattern/Rewrite.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} {- | Copyright : (c) Runtime Verification, 2022 @@ -260,6 +261,8 @@ applyRule pat@Pattern{ceilConditions} rule = runRewriteRuleAppT $ do subst <- case matchTerms Rule def rule.lhs pat.term of MatchFailed (SubsortingError sortError) -> failRewrite $ RewriteSortError rule pat.term sortError + MatchFailed err@ArgLengthsDiffer{} -> + failRewrite $ InternalMatchError $ renderText $ pretty err MatchFailed _reason -> fail "Rule matching failed" MatchIndeterminate remainder -> @@ -400,6 +403,8 @@ data RewriteFailed k UnificationIsNotMatch (RewriteRule k) Term Substitution | -- | A sort error was detected during unification RewriteSortError (RewriteRule k) Term SortError + | -- | A sort error was detected during unification + InternalMatchError Text | -- | Term has index 'None', no rule should apply TermIndexIsNone Term deriving stock (Eq, Show) @@ -450,6 +455,7 @@ instance Pretty (RewriteFailed k) where ] pretty (TermIndexIsNone term) = "Term index is None for term " <> pretty term + pretty (InternalMatchError err) = "An internal error occured" <> pretty err ruleLabelOrLoc :: RewriteRule k -> Doc a ruleLabelOrLoc rule = diff --git a/library/Booster/Pattern/UnifiedMatcher.hs b/library/Booster/Pattern/UnifiedMatcher.hs index fadab7cf3..b36136c32 100644 --- a/library/Booster/Pattern/UnifiedMatcher.hs +++ b/library/Booster/Pattern/UnifiedMatcher.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE PatternSynonyms #-} + {- | Copyright : (c) Runtime Verification, 2022 License : BSD-3-Clause @@ -21,16 +23,16 @@ import Data.Either.Extra import Data.List.NonEmpty as NE (NonEmpty, fromList) import Data.Map (Map) import Data.Map qualified as Map -import Data.Sequence (Seq (..), (><)) +import Data.Sequence (Seq, pattern (:<|), pattern (:|>), (><)) import Data.Sequence qualified as Seq import Data.Set (Set) import Data.Set qualified as Set import Prettyprinter -import Booster.Definition.Attributes.Base (KListDefinition) +import Booster.Definition.Attributes.Base (KListDefinition, KMapDefinition) import Booster.Definition.Base -import Booster.Pattern.Base +import Booster.Pattern.Base hiding (DotDotDot) import Booster.Pattern.Util ( checkSymbolIsAc, freeVariables, @@ -38,8 +40,11 @@ import Booster.Pattern.Util ( sortOfTerm, substituteInTerm, ) +import Booster.Prettyprinter (renderText) +import Control.Monad.Trans.Maybe (MaybeT (..)) import Data.ByteString (ByteString) import Data.List (partition) +import Data.Text (unpack) -- | Result of matching a pattern to a subject (a substitution or an indication of what went wrong) data MatchResult @@ -135,10 +140,12 @@ matchTerms mType KoreDefinition{sorts} term1 term2 = freeVars2 = freeVariables term2 sharedVars = freeVars1 `Set.intersection` freeVars2 in if not $ Set.null sharedVars - then - MatchIndeterminate $ - NE.fromList - [(Var v, Var v) | v <- Set.toList sharedVars] + then case mType of + Rule -> + MatchIndeterminate $ + NE.fromList + [(Var v, Var v) | v <- Set.toList sharedVars] + Fun -> MatchFailed $ SharedVariables sharedVars else runMatch State @@ -166,8 +173,8 @@ match mType = do queue <- gets mQueue mapQueue <- gets mMapQueue case queue of - Empty -> case mapQueue of - Empty -> checkIndeterminate -- done + Seq.Empty -> case mapQueue of + Seq.Empty -> checkIndeterminate -- done (term1, term2) :<| rest -> do modify $ \s -> s{mMapQueue = rest} match1 mType term1 term2 @@ -228,7 +235,7 @@ match1 Fun t1@KMap{} t2@AndTerm{} 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{} = matchMaps t1 t2 +match1 _ t1@(KMap def1 patKeyVals patRest) t2@(KMap def2 subjKeyVals subjRest) = if def1 == def2 then matchMaps def1 patKeyVals patRest subjKeyVals subjRest else failWith $ DifferentSorts 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 @@ -241,7 +248,7 @@ match1 _ t1@KList{} t2@DomainValue{} 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) = matchLists def1 heads1 rest1 def2 heads2 rest2 +match1 Rule t1@(KList def1 heads1 rest1) t2@(KList def2 heads2 rest2) = if def1 == def2 then matchLists def1 heads1 rest1 heads2 rest2 else failWith $ DifferentSorts t1 t2 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 @@ -435,7 +442,12 @@ matchVar lift . withExcept (MatchFailed . SubsortingError) $ checkSubsort subsorts termSort variableSort if isSubsort - then bindVariable mType var term2 + then bindVariable mType var $ case mType of + Rule -> term2 + Fun -> + if termSort == variableSort + then term2 + else Injection termSort variableSort term2 else failWith $ DifferentSorts (Var var) term2 -- unification for lists. Only solves simple cases, returns indeterminate otherwise @@ -443,30 +455,25 @@ matchLists :: KListDefinition -> [Term] -> Maybe (Term, [Term]) -> - KListDefinition -> [Term] -> Maybe (Term, [Term]) -> StateT MatchState (Except MatchResult) () matchLists - def1 + def heads1 rest1 - def2 heads2 rest2 - | -- incompatible lists - def1 /= def2 = - failWith $ DifferentSorts (KList def1 heads1 rest1) (KList def2 heads2 rest2) | -- two fully-concrete lists of the same length Nothing <- rest1 , Nothing <- rest2 = if length heads1 == length heads2 then void $ enqueuePairs heads1 heads2 - else failWith $ DifferentValues (KList def1 heads1 rest1) (KList def2 heads2 rest2) + else failWith $ DifferentValues (KList def heads1 rest1) (KList def heads2 rest2) | -- left list has a symbolic part, right one is fully concrete Just (symb1, tails1) <- rest1 , Nothing <- rest2 = do - let emptyList = KList def1 [] Nothing + let emptyList = KList def [] Nothing remainder <- enqueuePairs heads1 heads2 case remainder of Nothing -- equal head length, rest1 must become .List @@ -474,15 +481,15 @@ matchLists enqueueRegularProblem symb1 emptyList | otherwise -> do -- fully concrete list too short - let surplusLeft = KList def1 [] rest1 + let surplusLeft = KList def [] rest1 failWith $ DifferentValues surplusLeft emptyList Just (Left leftover1) -> do -- fully concrete list too short - let surplusLeft = KList def1 leftover1 rest1 + let surplusLeft = KList def leftover1 rest1 failWith $ DifferentValues surplusLeft emptyList Just (Right leftover2) | null tails1 -> do - let newRight = KList def2 leftover2 Nothing + let newRight = KList def leftover2 Nothing enqueueRegularProblem symb1 newRight | otherwise -> do tailRemainder <- -- reversed! @@ -493,15 +500,15 @@ matchLists enqueueRegularProblem symb1 emptyList Just (Left tail1) -> do -- fully concrete list too short - let surplusLeft = KList def1 [] $ Just (symb1, reverse tail1) + let surplusLeft = KList def [] $ Just (symb1, reverse tail1) failWith $ DifferentValues surplusLeft emptyList Just (Right tail2) -> do - let newRight = KList def2 (reverse tail2) Nothing + let newRight = KList def (reverse tail2) Nothing enqueueRegularProblem symb1 newRight | -- mirrored case above: left list fully concrete, right one isn't Nothing <- rest1 , Just _ <- rest2 = - matchLists def2 heads2 rest2 def1 heads1 rest1 -- won't loop, will fail later if unification succeeds + matchLists def heads2 rest2 heads1 rest1 -- won't loop, will fail later if unification succeeds | -- two lists with symbolic middle Just (symb1, tails1) <- rest1 , Just (symb2, tails2) <- rest2 = do @@ -516,10 +523,10 @@ matchLists Nothing -> enqueueRegularProblem symb1 symb2 Just (Left tails1') -> do - let newLeft = KList def1 [] (Just (symb1, tails1')) + let newLeft = KList def [] (Just (symb1, tails1')) enqueueRegularProblem newLeft symb2 Just (Right tails2') -> do - let newRight = KList def2 [] (Just (symb2, tails2')) + let newRight = KList def [] (Just (symb2, tails2')) enqueueRegularProblem symb1 newRight Just headRem -> do -- either left or right was longer, remove tails and proceed @@ -528,107 +535,180 @@ matchLists <$> enqueuePairs (reverse tails1) (reverse tails2) case (headRem, tailRem) of (Left heads1', Nothing) -> do - let newLeft = KList def1 heads1' (Just (symb1, [])) + let newLeft = KList def heads1' (Just (symb1, [])) enqueueRegularProblem newLeft symb2 (Left heads1', Just (Left tails1')) -> do - let newLeft = KList def1 heads1' (Just (symb1, tails1')) + let newLeft = KList def heads1' (Just (symb1, tails1')) enqueueRegularProblem newLeft symb2 (Left heads1', Just (Right tails2')) -> do - let surplusLeft = KList def1 heads1' (Just (symb1, [])) - surplusRight = KList def2 [] (Just (symb2, tails2')) + let surplusLeft = KList def heads1' (Just (symb1, [])) + surplusRight = KList def [] (Just (symb2, tails2')) addIndeterminate surplusLeft surplusRight (Right heads2', Nothing) -> do - let newRight = KList def2 heads2' (Just (symb2, [])) + let newRight = KList def heads2' (Just (symb2, [])) enqueueRegularProblem symb1 newRight (Right heads2', Just (Right tails2')) -> do - let newRight = KList def2 heads2' (Just (symb2, tails2')) + let newRight = KList def heads2' (Just (symb2, tails2')) enqueueRegularProblem symb1 newRight (Right heads2', Just (Left tails1')) -> do - let surplusLeft = KList def1 [] (Just (symb1, tails1')) - surplusRight = KList def2 heads2' (Just (symb2, [])) + let surplusLeft = KList def [] (Just (symb1, tails1')) + surplusRight = KList def heads2' (Just (symb2, [])) addIndeterminate surplusLeft surplusRight {-# INLINE matchLists #-} +data MapList + = ConstructorKey Term Term MapList + | Rest RestMapList + +pattern SingleConstructorKey :: Term -> Term -> MapList +pattern SingleConstructorKey k v = ConstructorKey k v (Rest Empty) + +pattern SingleOtherKey :: Term -> Term -> MapList +pattern SingleOtherKey k v = Rest (OtherKey k v Empty) + +instance Show MapList where + show = \case + ConstructorKey k v rest -> unpack (renderText $ pretty k) <> " -> " <> unpack (renderText $ pretty v) <> " " <> show rest + Rest s -> show s + +data RestMapList + = OtherKey Term Term RestMapList + | Empty + | Remainder Term + +instance Show RestMapList where + show = \case + OtherKey k v rest -> + "?" + <> unpack (renderText $ pretty k) + <> " -> " + <> unpack (renderText $ pretty v) + <> " " + <> show rest + Empty -> "" + Remainder t -> "..." <> unpack (renderText $ pretty t) + +toMapList :: [(Term, Term)] -> Maybe Term -> MapList +toMapList kvs rest = + let (conc, sym) = partitionConcreteKeys kvs + in foldr + (uncurry ConstructorKey) + (Rest $ foldr (uncurry OtherKey) (maybe Empty Remainder rest) sym) + conc + where + partitionConcreteKeys :: [(Term, Term)] -> ([(Term, Term)], [(Term, Term)]) + partitionConcreteKeys = partition (\(Term attrs _, _) -> attrs.isConstructorLike) + +fromMapList :: KMapDefinition -> MapList -> Term +fromMapList def ml = uncurry (KMap def) $ recurse ml + where + recurse (ConstructorKey k v rest) = first ((k, v) :) $ recurse rest + recurse (Rest s) = recurseS s + + recurseS (OtherKey k v rest) = first ((k, v) :) $ recurseS rest + recurseS Empty = ([], Nothing) + recurseS (Remainder t) = ([], Just t) + +hasNoRemainder :: RestMapList -> Bool +hasNoRemainder = \case + OtherKey _ _ r -> hasNoRemainder r + Empty -> True + Remainder{} -> False + ------ Internalised Maps -matchMaps :: Term -> Term -> StateT MatchState (Except MatchResult) () +matchMaps :: + KMapDefinition -> + [(Term, Term)] -> + Maybe Term -> + [(Term, Term)] -> + Maybe Term -> + StateT MatchState (Except MatchResult) () matchMaps - t1@(KMap def1 _ _) - t2@(KMap def2 _ _) - | def1 == def2 = do - State{mSubstitution = currentSubst, mQueue = queue} <- get - case queue of - Empty -> - case (substituteInKeys currentSubst t1, substituteInKeys currentSubst t2) of - (KMap _ kvs1 rest1, KMap _ kvs2 rest2) - | Just duplicate <- duplicateKeys kvs1 -> failWith $ DuplicateKeys duplicate $ KMap def1 kvs1 rest1 - | Just duplicate <- duplicateKeys kvs2 -> failWith $ DuplicateKeys duplicate $ KMap def1 kvs2 rest2 - | -- both sets of keys are syntactically the same (some keys could be functions) - Set.fromList [k | (k, _v) <- kvs1] == Set.fromList [k | (k, _v) <- kvs2] -> do - forM_ (Map.elems $ Map.intersectionWith (,) (Map.fromList kvs1) (Map.fromList kvs2)) $ - uncurry enqueueRegularProblem - case (rest1, rest2) of - (Just r1, Just r2) -> enqueueRegularProblem r1 r2 - (Just r1, Nothing) -> enqueueRegularProblem r1 (KMap def1 [] Nothing) - (Nothing, Just r2) -> enqueueRegularProblem (KMap def1 [] Nothing) r2 - (Nothing, Nothing) -> pure () - (KMap _ kvs1 Nothing, KMap _ kvs2 Nothing) - | -- the sets of keys do not match but all keys are concrete and fully evaluated - -- this means there is a mismatch - allKeysConstructorLike kvs1 && allKeysConstructorLike kvs2 -> - case kvs1 `findAllKeysIn` kvs2 of - Left notFoundKeys -> failWith $ KeyNotFound (head notFoundKeys) $ KMap def1 kvs2 Nothing - Right (_matched, []) -> error "unreachable case" - Right (_matched, rest) -> failWith $ KeyNotFound (fst $ head rest) $ KMap def1 kvs1 Nothing - (KMap _ kvs (Just restVar@Var{}), KMap _ m Nothing) - | (cKvs, []) <- partitionConcreteKeys kvs -> unifySimpleMapShape cKvs restVar m - (KMap _ m Nothing, KMap _ kvs (Just restVar@Var{})) - | (cKvs, []) <- partitionConcreteKeys kvs -> unifySimpleMapShape cKvs restVar m - (t1', t2') -> addIndeterminate t1' t2' - _ -> - -- defer unification until all regular terms have unified - enqueueMapProblem t1 t2 - | otherwise = failWith $ DifferentSorts t1 t2 + def + patKeyVals + patRest + subjKeyVals + subjRest + | def == def = do + 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 (KMap def patKeyVals patRest) (KMap def subjKeyVals subjRest) + else do + let patternKeyVals = map (first (substituteInTerm st.mSubstitution)) patKeyVals + -- check for duplicate keys + checkDuplicateKeys patternKeyVals patRest + checkDuplicateKeys subjKeyVals subjRest + + 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 + + runMaybeT + ( matchRemainderOfMapLists + (toMapList (Map.toList patExtra) patRest) + (toMapList (Map.toList subjExtra) subjRest) + ) + >>= \case + Just newProblems -> + enqueueRegularProblems $ (Seq.fromList $ Map.elems commonMap) >< newProblems + Nothing -> pure () + | otherwise = + failWith $ DifferentSorts (KMap def patKeyVals patRest) (KMap def subjKeyVals subjRest) where - partitionConcreteKeys :: [(Term, Term)] -> ([(Term, Term)], [(Term, Term)]) - partitionConcreteKeys = partition (\(Term attrs _, _) -> attrs.isConstructorLike) - - allKeysConstructorLike :: [(Term, Term)] -> Bool - allKeysConstructorLike = all (\(Term attrs _, _) -> attrs.isConstructorLike) - - findAllKeysIn :: [(Term, Term)] -> [(Term, Term)] -> Either [Term] ([(Term, Term)], [(Term, Term)]) - findAllKeysIn kvs m = - let searchMap = Map.fromList kvs - subjectMap = Map.fromList m - matchedMap = Map.intersectionWith (,) searchMap subjectMap - restMap = Map.difference subjectMap matchedMap - unmatched = Map.keys $ Map.difference searchMap subjectMap - in if null unmatched - then Right (Map.elems matchedMap, Map.toList restMap) - else Left unmatched - - duplicateKeys :: [(Term, Term)] -> Maybe Term - duplicateKeys kvs = - let duplicates = Map.filter (> (1 :: Int)) $ foldr (flip (Map.insertWith (+)) 1 . fst) mempty kvs - in case Map.toList duplicates of - [] -> Nothing - (k, _) : _ -> Just k - - unifySimpleMapShape cKvs restVar m = do - let (cM, sM) = partitionConcreteKeys m - case cKvs `findAllKeysIn` cM of - Left notFoundKeys -> failWith $ KeyNotFound (head notFoundKeys) $ KMap def1 m Nothing - Right (matched, rest) -> do - forM_ matched $ uncurry enqueueRegularProblem - enqueueRegularProblem restVar $ KMap def1 (rest ++ sM) Nothing - - substituteInKeys :: Map Variable Term -> Term -> Term - substituteInKeys substitution = \case - KMap attrs keyVals rest -> KMap attrs (first (substituteInTerm substitution) <$> keyVals) rest - other -> other -matchMaps _ _ = undefined + checkDuplicateKeys assocs rest = + 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 $ KMap def assocs rest + + matchRemainderOfMapLists :: + MapList -> MapList -> MaybeT (StateT MatchState (Except MatchResult)) (Seq (Term, Term)) + -- match {} with {} + -- succeeds + matchRemainderOfMapLists (Rest Empty) (Rest Empty) = pure mempty + -- match {} with {...rest} or {K -> V, ...} + -- fails as the size of the maps is different and there is no substitution `subst`, s.t. + -- subst({}) = {...rest} or {K -> V, ...} + matchRemainderOfMapLists (Rest Empty) subj = + lift $ failWith $ DifferentSymbols (fromMapList def (Rest Empty)) (fromMapList def subj) + -- match {...pat} with subj + -- succeeds as `pat` must be a variable of sort map or a function which evaluates to a map + matchRemainderOfMapLists (Rest (Remainder pat)) subj = pure $ Seq.singleton (pat, fromMapList def subj) + -- match {K -> V ...} with `subj` where K is concrete + -- fail here because we already matched all concrete keys, so we know `K` does not appear in `subj` + matchRemainderOfMapLists (ConstructorKey patKey _ _) subj = lift $ failWith $ KeyNotFound patKey (fromMapList def subj) + -- match {K -> V} with {K' -> V'} where K' is a constructor like and K is not (i.e. a variable or function) + -- we can proceed matching because the two key/value pairs must match + matchRemainderOfMapLists (SingleOtherKey patKey patVal) (SingleConstructorKey subjKey subjVal) = + pure $ Seq.fromList [(patKey, subjKey), (patVal, subjVal)] + -- match {K -> V} with {K' -> V'} where K and K' are both non-constructor like (i.e. a variable or function) + -- same as above + matchRemainderOfMapLists (SingleOtherKey patKey patVal) (SingleOtherKey subjKey subjVal) = + pure $ Seq.fromList [(patKey, subjKey), (patVal, subjVal)] + -- match {K -> V ...} with {} + -- fails + matchRemainderOfMapLists pat@(Rest OtherKey{}) subj@(Rest Empty) = + lift $ failWith $ DifferentSymbols (fromMapList def pat) (fromMapList def subj) + -- match {?K/f(..) -> V ...} with {...?REST} where ?REST is a variable + -- fail because there is no substitution `sub` such that sub({?K -> V ...}) = {...?REST} + matchRemainderOfMapLists (Rest pat@OtherKey{}) subj@(Rest (Remainder Var{})) + | hasNoRemainder pat = + lift $ failWith $ DifferentSymbols (fromMapList def (Rest pat)) (fromMapList def subj) + -- match {?K/f(..) -> V ...} with {C -> V' ...} or {C -> V'} or {...} + -- indeterminate + matchRemainderOfMapLists pat@(Rest OtherKey{}) subj = do + lift $ addIndeterminate (fromMapList def pat) (fromMapList def subj) + fail "all other cases are indeterminate" {-# INLINE matchMaps #-} -failWith :: FailReason -> StateT s (Except MatchResult) () +failWith :: FailReason -> StateT s (Except MatchResult) a failWith = lift . throwE . MatchFailed internalError :: String -> a diff --git a/test/llvm-integration/LLVM.hs b/test/llvm-integration/LLVM.hs index 8eb157434..ee0588557 100644 --- a/test/llvm-integration/LLVM.hs +++ b/test/llvm-integration/LLVM.hs @@ -633,7 +633,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -653,7 +653,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -673,7 +673,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Just $ KListMeta sortListKList - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -693,7 +693,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Just $ KMapMeta sortMapKmap - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -713,7 +713,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Just $ KSetMeta sortSetKSet - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -733,7 +733,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -753,7 +753,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -773,7 +773,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -793,7 +793,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Just $ KListMeta sortListKList - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -813,7 +813,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Just $ KMapMeta sortMapKmap - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -833,7 +833,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Just $ KSetMeta sortSetKSet - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsIdem , isAssoc = IsAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -853,7 +853,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -873,7 +873,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -893,7 +893,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -913,7 +913,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -933,7 +933,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -953,7 +953,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -973,7 +973,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -993,7 +993,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1013,7 +1013,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1033,7 +1033,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1053,7 +1053,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1073,7 +1073,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1093,7 +1093,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1113,7 +1113,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1133,7 +1133,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1153,7 +1153,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1173,7 +1173,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1193,7 +1193,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1213,7 +1213,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1233,7 +1233,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1253,7 +1253,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1273,7 +1273,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1293,7 +1293,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1313,7 +1313,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1333,7 +1333,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1353,7 +1353,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1373,7 +1373,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1393,7 +1393,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1413,7 +1413,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1433,7 +1433,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1453,7 +1453,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1473,7 +1473,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1493,7 +1493,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1513,7 +1513,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Just $ KMapMeta sortMapKmap - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1533,7 +1533,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1553,7 +1553,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1573,7 +1573,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1593,7 +1593,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1613,7 +1613,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1633,7 +1633,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1653,7 +1653,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1673,7 +1673,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1694,7 +1694,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1714,7 +1714,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1795,7 +1795,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1816,7 +1816,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1836,7 +1836,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1856,7 +1856,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1876,7 +1876,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Just $ KListMeta sortListKList - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1896,7 +1896,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1916,7 +1916,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1976,7 +1976,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -1996,7 +1996,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2016,7 +2016,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Just $ KSetMeta sortSetKSet - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2076,7 +2076,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2176,7 +2176,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2217,7 +2217,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2237,7 +2237,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2257,7 +2257,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2277,7 +2277,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2297,7 +2297,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2319,7 +2319,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2339,7 +2339,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2359,7 +2359,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2379,7 +2379,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2399,7 +2399,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2419,7 +2419,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2439,7 +2439,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2459,7 +2459,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2479,7 +2479,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2499,7 +2499,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2519,7 +2519,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2539,7 +2539,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2559,7 +2559,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2579,7 +2579,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2599,7 +2599,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2619,7 +2619,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2639,7 +2639,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2659,7 +2659,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2679,7 +2679,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2699,7 +2699,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2719,7 +2719,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2739,7 +2739,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2759,7 +2759,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2779,7 +2779,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2799,7 +2799,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2819,7 +2819,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2839,7 +2839,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2859,7 +2859,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2879,7 +2879,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2899,7 +2899,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2919,7 +2919,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2959,7 +2959,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2979,7 +2979,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -2999,7 +2999,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3019,7 +3019,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3079,7 +3079,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3100,7 +3100,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3121,7 +3121,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3141,7 +3141,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3161,7 +3161,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3181,7 +3181,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3201,7 +3201,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3221,7 +3221,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3241,7 +3241,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3261,7 +3261,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3281,7 +3281,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3301,7 +3301,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3321,7 +3321,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3341,7 +3341,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3361,7 +3361,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3381,7 +3381,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3401,7 +3401,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3421,7 +3421,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3441,7 +3441,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3461,7 +3461,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3481,7 +3481,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3501,7 +3501,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3521,7 +3521,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3541,7 +3541,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3561,7 +3561,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3581,7 +3581,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3602,7 +3602,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3622,7 +3622,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3643,7 +3643,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3683,7 +3683,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3703,7 +3703,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3723,7 +3723,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3743,7 +3743,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3764,7 +3764,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3804,7 +3804,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3824,7 +3824,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3844,7 +3844,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = PartialFunction + , symbolType = Function Partial , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3864,7 +3864,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -3904,7 +3904,7 @@ defSymbols = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = SortInjection + , symbolType = Constructor , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias diff --git a/unit-tests/Test/Booster/Fixture.hs b/unit-tests/Test/Booster/Fixture.hs index 79ee58463..2956b2254 100644 --- a/unit-tests/Test/Booster/Fixture.hs +++ b/unit-tests/Test/Booster/Fixture.hs @@ -53,6 +53,7 @@ testDefinition = , ("f1", f1) , ("f2", f2) , ("f3", f3) + , ("g", g) , ("Lbl'UndsEqlsEqls'K'Und'", eqK) , ("kseq", kseq) , ("dotk", dotk) @@ -89,7 +90,7 @@ app s = SymbolApplication s [] inj :: Sort -> Sort -> Term -> Term inj = Injection -con1, con2, con3, con4, f1, f2, f3, eqK, kseq, dotk :: Symbol +con1, con2, con3, con4, f1, f2, f3, g, eqK, kseq, dotk :: Symbol con1 = [symb| symbol con1{}(SomeSort{}) : SomeSort{} [constructor{}()] |] con2 = [symb| symbol con2{}(SomeSort{}) : SomeSort{} [constructor{}()] |] con3 = [symb| symbol con3{}(SomeSort{}, SomeSort{}) : SomeSort{} [constructor{}()] |] @@ -97,6 +98,7 @@ con4 = [symb| symbol con4{}(SomeSort{}, SomeSort{}) : AnotherSort{} [constructor f1 = [symb| symbol f1{}(SomeSort{}) : SomeSort{} [function{}(), total{}()] |] f2 = [symb| symbol f2{}(SomeSort{}) : SomeSort{} [function{}()] |] f3 = [symb| symbol f3{}(SomeSort{}) : SortTestKMap{} [function{}()] |] +g = [symb| symbol g{}() : SortTestKMapKey{} [function{}(), total{}()] |] eqK = Symbol { name = "Lbl'UndsEqlsEqls'K'Unds'" @@ -106,7 +108,7 @@ eqK = , attributes = SymbolAttributes { collectionMetadata = Nothing - , symbolType = TotalFunction + , symbolType = Function Total , isIdem = IsNotIdem , isAssoc = IsNotAssoc , isMacroOrAlias = IsNotMacroOrAlias @@ -222,7 +224,7 @@ functionKMapWithOneItemAndRest = KMap testKMapDefinition [ - ( [trm| f1{}() |] + ( [trm| g{}() |] , [trm| \dv{SortTestKMapItem{}}("value") |] ) ] @@ -231,7 +233,7 @@ functionKMapWithOneItem = KMap testKMapDefinition [ - ( [trm| f1{}() |] + ( [trm| g{}() |] , [trm| B:SortTestKMapItem{} |] ) ] diff --git a/unit-tests/Test/Booster/Pattern/Binary.hs b/unit-tests/Test/Booster/Pattern/Binary.hs index 35f32644b..931d80370 100644 --- a/unit-tests/Test/Booster/Pattern/Binary.hs +++ b/unit-tests/Test/Booster/Pattern/Binary.hs @@ -39,7 +39,7 @@ genSymbolUnknownSort = ( \name -> Symbol name [] [] (SortApp "UNKNOWN" []) $ SymbolAttributes - PartialFunction + (Function Partial) IsNotIdem IsNotAssoc IsNotMacroOrAlias diff --git a/unit-tests/Test/Booster/Pattern/Match.hs b/unit-tests/Test/Booster/Pattern/MatchFun.hs similarity index 85% rename from unit-tests/Test/Booster/Pattern/Match.hs rename to unit-tests/Test/Booster/Pattern/MatchFun.hs index 2a2a7bd1a..639bb5689 100644 --- a/unit-tests/Test/Booster/Pattern/Match.hs +++ b/unit-tests/Test/Booster/Pattern/MatchFun.hs @@ -1,22 +1,24 @@ +{-# LANGUAGE QuasiQuotes #-} {- | Copyright : (c) Runtime Verification, 2022 License : BSD-3-Clause -} -module Test.Booster.Pattern.Match ( - test_match, +module Test.Booster.Pattern.MatchFun ( + test_match_fun, ) where import Data.Map qualified as Map +import Data.List.NonEmpty qualified as NE import Test.Tasty import Test.Tasty.HUnit import Booster.Pattern.Base -import Booster.Pattern.Match -import Booster.Pattern.Unify (FailReason (..)) +import Booster.Pattern.UnifiedMatcher +import Booster.Syntax.Json.Internalise (trm) import Test.Booster.Fixture -test_match :: TestTree -test_match = +test_match_fun :: TestTree +test_match_fun = testGroup "(equation) matching" [ symbols @@ -48,11 +50,11 @@ symbols = , let pat = app con1 [var "X" someSort] subj = app f1 [var "Y" someSort] in test "constructor and function" pat subj $ - MatchIndeterminate pat subj + MatchIndeterminate $ NE.singleton (pat, subj) , let pat = app f1 [var "X" someSort] subj = app con1 [var "Y" someSort] in test "function and constructor" pat subj $ - MatchIndeterminate pat subj + MatchIndeterminate $ NE.singleton (pat, subj) , let x = var "X" someSort d = dv differentSort "something" pat = app con1 [x] @@ -141,15 +143,15 @@ varsAndValues = , let v = var "X" someSort d = dv someSort "" in test "dv matching a var (on RHS): indeterminate" d v $ - MatchIndeterminate d v + MatchIndeterminate $ NE.singleton (d, v) , let d = dv someSort "" f = app f1 [d] in test "dv matching a function call (on RHS): indeterminate" d f $ - MatchIndeterminate d f + MatchIndeterminate $ NE.singleton (d, f) , let d = dv someSort "" c = app con1 [d] in test "dv matching a constructor (on RHS): fail" d c $ - failed (DifferentValues d c) + failed (DifferentSymbols d c) ] andTerms :: TestTree @@ -181,7 +183,7 @@ andTerms = "And-term on the right, indeterminate" d (AndTerm fa fb) - (MatchIndeterminate d (AndTerm fa fb)) + (MatchIndeterminate $ NE.singleton (d ,AndTerm fa fb)) ] kmapTerms :: TestTree @@ -198,21 +200,16 @@ kmapTerms = concreteKMapWithOneItem concreteKMapWithOneItem (success []) - , test - "Empty KMap ~= non-empty concrete KMap: fails" - emptyKMap - concreteKMapWithOneItem - (failed $ DifferentValues emptyKMap concreteKMapWithOneItem) , test "Non-empty concrete KMap ~= empty KMap: fails" concreteKMapWithOneItem emptyKMap - (failed $ DifferentValues concreteKMapWithOneItem emptyKMap) + (failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key")|] emptyKMap) , test "Non-empty symbolic KMap ~= empty KMap: fails" symbolicKMapWithOneItem emptyKMap - (failed $ DifferentValues symbolicKMapWithOneItem emptyKMap) + (failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key")|] emptyKMap) , test "Non-empty symbolic KMap ~= non-empty concrete KMap, same key: matches contained value" symbolicKMapWithOneItem -- "key" -> A @@ -231,19 +228,11 @@ kmapTerms = in success [("REST", kmapSort, restMap)] ) , -- pattern has more assocs than subject - let patRest = kmap [(dv kmapKeySort "key2", dv kmapElementSort "value2")] Nothing - in test + test "Extra concrete key in pattern, no rest in subject: fail on rest" concreteKMapWithTwoItems concreteKMapWithOneItem - (failed $ DifferentValues patRest emptyKMap) - , let patRest = - kmap [(dv kmapKeySort "key2", dv kmapElementSort "value2")] Nothing - in test - "Extra concrete key in pattern, opaque rest in subject: indeterminate part" - concreteKMapWithTwoItems - concreteKMapWithOneItemAndRest - (MatchIndeterminate patRest (var "REST" kmapSort)) + (failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key2")|] emptyKMap) , -- cases with disjoint keys test "Variable key ~= concrete key (and common element) without rest: match key" @@ -252,24 +241,24 @@ kmapTerms = ( success [("A", kmapKeySort, dv kmapKeySort "key2")] ) , let patMap = - kmap [(var "K" kmapKeySort, var "V" kmapElementSort)] (Just "PATTERN") + kmap [([trm| K:SortTestKMapKey{} |], var "V" kmapElementSort)] (Just "PATTERN") in test "Variable key ~= concrete key with rest in subject and pattern: indeterminate" patMap functionKMapWithOneItemAndRest - (MatchIndeterminate patMap functionKMapWithOneItemAndRest) + (MatchIndeterminate $ NE.singleton (patMap, functionKMapWithOneItemAndRest)) , let patMap = kmap [(var "K" kmapKeySort, var "V" kmapElementSort)] (Just "PATTERN") in test "Variable key and opaque rest ~= two items: indeterminate" patMap concreteKMapWithTwoItems - (MatchIndeterminate patMap concreteKMapWithTwoItems) + (MatchIndeterminate $ NE.singleton (patMap, concreteKMapWithTwoItems)) , test "Keys disjoint and pattern keys are fully-concrete: fail" concreteKMapWithOneItemAndRest functionKMapWithOneItem - (failed $ DifferentValues concreteKMapWithOneItemAndRest functionKMapWithOneItem) + (failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key")|] functionKMapWithOneItem) , let patMap = kmap [ (var "A" kmapKeySort, dv kmapElementSort "a") @@ -286,7 +275,7 @@ kmapTerms = "Disjoint non-singleton maps, non-concrete keys in pattern: indeterminate" patMap subjMap - (MatchIndeterminate patMap subjMap) + (MatchIndeterminate $ NE.singleton (patMap, subjMap)) ] where kmap :: [(Term, Term)] -> Maybe VarName -> Term @@ -300,7 +289,7 @@ cornerCases = test :: String -> Term -> Term -> MatchResult -> TestTree test name pat subj expected = - testCase name $ matchTerm testDefinition pat subj @?= expected + testCase name $ matchTerms Fun testDefinition pat subj @?= expected success :: [(VarName, Sort, Term)] -> MatchResult success assocs = @@ -311,11 +300,11 @@ success assocs = ] failed :: FailReason -> MatchResult -failed = MatchFailed . General +failed = MatchFailed errors :: String -> Term -> Term -> TestTree errors name pat subj = testCase name $ - case matchTerm testDefinition pat subj of + case matchTerms Fun testDefinition pat subj of MatchFailed _ -> pure () other -> assertFailure $ "Expected MatchFailed, got " <> show other diff --git a/unit-tests/Test/Booster/Pattern/Unify.hs b/unit-tests/Test/Booster/Pattern/MatchRule.hs similarity index 87% rename from unit-tests/Test/Booster/Pattern/Unify.hs rename to unit-tests/Test/Booster/Pattern/MatchRule.hs index 444bb8fc3..6583b4538 100644 --- a/unit-tests/Test/Booster/Pattern/Unify.hs +++ b/unit-tests/Test/Booster/Pattern/MatchRule.hs @@ -6,8 +6,8 @@ Copyright : (c) Runtime Verification, 2022 License : BSD-3-Clause -} -module Test.Booster.Pattern.Unify ( - test_unification, +module Test.Booster.Pattern.MatchRule ( + test_match_rule, ) where import Data.List.NonEmpty qualified as NE @@ -16,15 +16,15 @@ import Test.Tasty import Test.Tasty.HUnit import Booster.Pattern.Base -import Booster.Pattern.Unify +import Booster.Pattern.UnifiedMatcher import Booster.Syntax.Json.Internalise (trm) import Test.Booster.Fixture import Test.Booster.Pattern.InternalCollections -test_unification :: TestTree -test_unification = +test_match_rule :: TestTree +test_match_rule = testGroup - "Unification" + "Rule matching" [ constructors , functions , varsAndValues @@ -132,9 +132,9 @@ constructors = functions :: TestTree functions = testGroup - "Functions (should not unify)" + "Functions (should not match)" $ [ let f = app f1 [dv someSort ""] - in test "exact same function (but not unifying)" f f $ remainder [(f, f)] + in test "exact same function (but not matching)" f f $ remainder [(f, f)] , let f1T = app f1 [dv someSort ""] f2T = app f2 [dv someSort ""] in test "different functions" f1T f2T $ remainder [(f1T, f2T)] @@ -256,34 +256,34 @@ internalLists = testGroup "Internal lists" [ test - "Can unify an empty list with itself" + "Can match an empty list with itself" emptyList emptyList (success []) , test - "Can unify a concrete list with itself" + "Can match a concrete list with itself" concreteList concreteList (success []) , test - "Empty and non-empty concrete list fail to unify" + "Empty and non-empty concrete list fail to match" emptyList concreteList (failed $ DifferentValues emptyList concreteList) , let two = klist (replicate 2 headElem) Nothing three = klist (replicate 3 headElem) Nothing in test - "Concrete lists of different length fail to unify" + "Concrete lists of different length fail to match" two three (failed $ DifferentValues two three) , test - "Empty and non-empty list fail to unify (symbolic tail)" + "Empty and non-empty list fail to match (symbolic tail)" headList emptyList (failed $ DifferentValues headList emptyList) , test - "Empty and non-empty list fail to unify (symbolic init)" + "Empty and non-empty list fail to match (symbolic init)" tailList emptyList (failed $ DifferentValues tailList emptyList) @@ -379,22 +379,22 @@ internalMaps = testGroup "Internal maps" [ test - "Can unify an empty map with itself" + "Can match an empty map with itself" emptyKMap emptyKMap (success []) , test - "Can unify a concrete 2 element map with itself" + "Can match a concrete 2 element map with itself" concreteKMapWithTwoItems concreteKMapWithTwoItems (success []) , test - "Can unify a concrete and symbolic map" + "Can match a concrete and symbolic map" concreteKMapWithOneItem symbolicKMapWithOneItem (success [("A", kmapElementSort, [trm| \dv{SortTestKMapItem{}}("value")|])]) , test - "Can unify a concrete and symbolic map with two elements" + "Can match a concrete and symbolic map with two elements" concreteKMapWithTwoItems symbolicKMapWithTwoItems ( success @@ -403,16 +403,16 @@ internalMaps = ] ) , test - "Can unify {\"key\" |-> \"value\", ...REST} with {A |-> \"value\"}" + "Can match {\"key\" |-> \"value\", ...REST} with {A |-> \"value\"}" concreteKMapWithOneItemAndRest symbolicKMapWithOneItem ( success [("REST", kmapSort, emptyKMap), ("A", kmapElementSort, [trm| \dv{SortTestKMapItem{}}("value")|])] ) , test - "Can unify {\"key\" |-> \"value\", A |-> \"value2\"} with {\"key\" |-> \"value\", ...REST}" - concreteAndSymbolicKMapWithTwoItems + "Can match {\"key\" |-> \"value\", ...REST} with {\"key\" |-> \"value\", A |-> \"value2\"}" concreteKMapWithOneItemAndRest + concreteAndSymbolicKMapWithTwoItems ( success [ ( "REST" @@ -429,9 +429,20 @@ internalMaps = ] ) , test - "Can unify {\"f()\" |-> B} with {\"f()\" |-> \"value\", ...REST}" - functionKMapWithOneItem + "Fails to match {\"key\" |-> \"value\", A |-> \"value2\"} with {\"key\" |-> \"value\", ...REST}" + concreteAndSymbolicKMapWithTwoItems + concreteKMapWithOneItemAndRest + (failed $ DifferentSymbols ( KMap + testKMapDefinition + [( [trm| A:SortTestKMapKey{}|] + , [trm| \dv{SortTestKMapItem{}}("value2") |] + ) + ] + Nothing) (KMap testKMapDefinition [] (Just [trm| REST:SortTestKMap{}|]))) + , test + "Can match {\"f()\" |-> \"value\", ...REST} with {\"f()\" |-> B}" functionKMapWithOneItemAndRest + functionKMapWithOneItem ( success [ ( "REST" @@ -449,41 +460,41 @@ internalMaps = ] ) , test - "Empty and non-empty concrete map fail to unify" + "Empty and non-empty concrete map fail to match" emptyKMap concreteKMapWithOneItem - (failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key")|] emptyKMap) + (failed $ DifferentSymbols emptyKMap concreteKMapWithOneItem) , test - "Concrete maps of different length fail to unify" - concreteKMapWithOneItem + "Concrete maps of different length fail to match" concreteKMapWithTwoItems - (failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key2")|] concreteKMapWithOneItem) + concreteKMapWithOneItem + (failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key2")|] emptyKMap) , test - "Empty and symbolic non-empty map fail to unify" - emptyKMap + "Symbolic non-empty map and empty map fail to match" symbolicKMapWithOneItem + emptyKMap (failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key")|] emptyKMap) ] ---------------------------------------- -success :: [(VarName, Sort, Term)] -> UnificationResult +success :: [(VarName, Sort, Term)] -> MatchResult success assocs = - UnificationSuccess $ + MatchSuccess $ Map.fromList [ (Variable{variableSort, variableName}, term) | (variableName, variableSort, term) <- assocs ] -failed :: FailReason -> UnificationResult -failed = UnificationFailed +failed :: FailReason -> MatchResult +failed = MatchFailed -remainder :: [(Term, Term)] -> UnificationResult -remainder = UnificationRemainder . NE.fromList +remainder :: [(Term, Term)] -> MatchResult +remainder = MatchIndeterminate . NE.fromList -sortErr :: SortError -> UnificationResult -sortErr = UnificationSortError +sortErr :: SortError -> MatchResult +sortErr = MatchFailed . SubsortingError -test :: String -> Term -> Term -> UnificationResult -> TestTree +test :: String -> Term -> Term -> MatchResult -> TestTree test name term1 term2 expected = - testCase name $ unifyTerms testDefinition term1 term2 @?= expected + testCase name $ matchTerms Rule testDefinition term1 term2 @?= expected diff --git a/unit-tests/Test/Booster/Pattern/Rewrite.hs b/unit-tests/Test/Booster/Pattern/Rewrite.hs index eac376bdc..ada3f9369 100644 --- a/unit-tests/Test/Booster/Pattern/Rewrite.hs +++ b/unit-tests/Test/Booster/Pattern/Rewrite.hs @@ -9,7 +9,6 @@ module Test.Booster.Pattern.Rewrite ( test_performRewrite, ) where -import Control.Exception (ErrorCall, catch) import Control.Monad.Logger.CallStack import Data.Bifunctor (second) import Data.List.NonEmpty qualified as NE @@ -347,12 +346,13 @@ callsError :: TestTree callsError = testGroup "Calls error when there are unexpected situations" - [ testCase "on wrong argument count in a symbol application" $ do - ( runRewrite + [ testCase "on wrong argument count in a symbol application" $ + runRewrite [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing"), \dv{SomeSort{}}("thing"), \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] - >> assertFailure "success" - ) - `catch` (\(_ :: ErrorCall) -> pure ()) + >>= \case + (_, RewriteAborted InternalMatchError{} _) -> pure () + _ -> assertFailure "success" + ] getsStuckOnFailures :: TestTree