Implement conjunction and negation over glob terms (#3926)

This change allows us to write the following filter:

```
kore|booster>!(kore-term|detail).
``` 

i.e. log everything from kore and booster except for the innermost
`kore-term` or `detail` contexts, which contain the pretty printed terms
and extra details about e.g. rule locations which may be too noisy. This
was previously not possible because we couldn't apply `!` over a
bracketed expression. I've added conjunction `&` for good measure, so we
could also write the above filter as `kore|booster>!kore-term&!detail.`

Author: goodlyrottenapple

booster/library/Booster/Log/Context.hs

@@ -11,47 +11,96 @@ import Data.Generics (Data, extQ)
 import Data.List.Extra (replace)
 import Language.Haskell.TH (ExpQ, Lit (StringL), appE, litE, varE)
 import Language.Haskell.TH.Quote (QuasiQuoter (..), dataToExpQ)
+import Options.Applicative (Alternative)
 
 data ContextFilterSingle
     = Exact BS.ByteString
     | Prefix BS.ByteString
     | Suffix BS.ByteString
     | Infix BS.ByteString
-    | Negate ContextFilterSingle
+    deriving (Show, Data)
+
+data ContextFilterBoolean
+    = And ContextFilterBoolean ContextFilterBoolean
+    | Or ContextFilterBoolean ContextFilterBoolean
+    | Negate ContextFilterBoolean
+    | Single ContextFilterSingle
     deriving (Show, Data)
 
 data ContextFilter
-    = First [ContextFilterSingle]
-    | ThenDirectChild [ContextFilterSingle] ContextFilter
-    | ThenChild [ContextFilterSingle] ContextFilter
-    | Last [ContextFilterSingle]
+    = First ContextFilterBoolean
+    | ThenDirectChild ContextFilterBoolean ContextFilter
+    | ThenChild ContextFilterBoolean ContextFilter
+    | Last ContextFilterBoolean
     deriving (Show, Data)
 
 reserved :: String
-reserved = "|*!>,."
+reserved = "()&|*!>,."
 
 stringP :: A.Parser BS.ByteString
 stringP = A.takeWhile1 (not . (`elem` reserved))
 
 singleP :: A.Parser ContextFilterSingle
 singleP =
-    A.char '!' *> A.skipSpace *> (Negate <$> singleP)
-        <|> A.char '*' *> (Infix <$> stringP) <* A.char '*'
+    A.char '*' *> (Infix <$> stringP) <* A.char '*'
         -- we want to allow * being parsed as `Suffix ""` so we allow the empty string via `takeWhile`
         <|> A.char '*' *> (Suffix . BS.dropWhileEnd isSpace <$> A.takeWhile (not . (`elem` reserved)))
         <|> Prefix . BS.dropWhile isSpace <$> stringP <* A.char '*'
         <|> Exact . BS.strip <$> stringP
 
-orP :: A.Parser [ContextFilterSingle]
-orP = singleP `A.sepBy` (A.char '|')
+parens :: A.Parser a -> A.Parser a
+parens p = A.char '(' *> A.skipSpace *> p <* A.skipSpace <* A.char ')' <* A.skipSpace
+
+chainl1 :: (Alternative m, Monad m) => m b -> m (b -> b -> b) -> m b
+chainl1 p op = do x <- p; rest x
+  where
+    rest x =
+        do
+            f <- op
+            y <- p
+            rest (f x y)
+            <|> return x
+
+-- adapted from https://gist.github.com/pedrominicz/6867c298608a96e6db4dedd798f49e60
+expression :: A.Parser ContextFilterBoolean
+expression =
+    orExpr
+        <|> andExpr
+        <|> negExpr
+        <|> Single <$> singleP
+        <|> parens expression
+
+orExpr :: A.Parser ContextFilterBoolean
+orExpr = A.try $ expression' `chainl1` (Or <$ A.char '|' <* A.skipSpace)
+  where
+    expression' =
+        andExpr
+            <|> negExpr
+            <|> Single <$> singleP
+            <|> parens expression
+
+andExpr :: A.Parser ContextFilterBoolean
+andExpr = A.try $ expression' `chainl1` (And <$ A.char '&' <* A.skipSpace)
+  where
+    expression' =
+        negExpr
+            <|> Single <$> singleP
+            <|> parens expression
+
+negExpr :: A.Parser ContextFilterBoolean
+negExpr = A.try $ A.char '!' *> A.skipSpace *> (Negate <$> expression')
+  where
+    expression' =
+        Single <$> singleP
+            <|> parens expression
 
 contextFilterP :: A.Parser ContextFilter
 contextFilterP =
     A.skipSpace
-        *> ( ThenChild <$> (orP <* A.skipSpace <* A.char '>') <*> contextFilterP
-                <|> ThenDirectChild <$> (orP <* A.skipSpace <* A.char ',') <*> contextFilterP
-                <|> Last <$> (orP <* A.skipSpace <* A.char '.')
-                <|> First <$> orP
+        *> ( ThenChild <$> (expression <* A.skipSpace <* A.char '>') <*> contextFilterP
+                <|> ThenDirectChild <$> (expression <* A.skipSpace <* A.char ',') <*> contextFilterP
+                <|> Last <$> (expression <* A.skipSpace <* A.char '.')
+                <|> First <$> expression
            )
 
 readContextFilter :: String -> Either String ContextFilter
@@ -63,19 +112,24 @@ matchSingle (Exact c) s = c == s
 matchSingle (Prefix c) s = BS.isPrefixOf c s
 matchSingle (Suffix c) s = BS.isSuffixOf c s
 matchSingle (Infix c) s = BS.isInfixOf c s
-matchSingle (Negate c) s = not $ matchSingle c s
+
+matchBoolean :: ContextFilterBoolean -> BS.ByteString -> Bool
+matchBoolean (Single e) s = matchSingle e s
+matchBoolean (And e1 e2) s = matchBoolean e1 s && matchBoolean e2 s
+matchBoolean (Or e1 e2) s = matchBoolean e1 s || matchBoolean e2 s
+matchBoolean (Negate e) s = not $ matchBoolean e s
 
 mustMatch :: ContextFilter -> [BS.ByteString] -> Bool
-mustMatch (First cs) [] = any (flip matchSingle "") cs
-mustMatch (First cs) (x : _) = any (flip matchSingle x) cs
-mustMatch (Last cs) [x] = any (flip matchSingle x) cs
+mustMatch (First cs) [] = matchBoolean cs ""
+mustMatch (First cs) (x : _) = matchBoolean cs x
+mustMatch (Last cs) [x] = matchBoolean cs x
 mustMatch Last{} _ = False
 mustMatch (_ `ThenDirectChild` _) [] = False
 mustMatch (cs `ThenDirectChild` css) (x : xs) =
-    any (flip matchSingle x) cs && mustMatch css xs
+    matchBoolean cs x && mustMatch css xs
 mustMatch (_ `ThenChild` _) [] = False
 mustMatch (cs `ThenChild` css) (x : xs) =
-    any (flip matchSingle x) cs && mayMatch css xs
+    matchBoolean cs x && mayMatch css xs
 
 mayMatch :: ContextFilter -> [BS.ByteString] -> Bool
 mayMatch c [] = mustMatch c []

docs/logging.md

@@ -142,15 +142,21 @@ To turn on context logging, use the `--log-context` flag to select which of the
 * `*foo*` - match context with the infix `foo`
 * `!foo*` - don't match `foo`
 * `foo|bar` - match `foo` or `bar` context, e.g. `kore|booster`
+* `foo&bar` - match `foo` and `bar` context, most likely used with negation e.g. `!kore&!proxy`
 * `foo,bar` - match a context `foo` with an immediately nested context `bar`
 * `foo>bar` - match a context `foo` with a child context `bar`
 * `foo>bar.` - match a context `foo` with a child context `bar` which is the last context, e.g. the context `[foo][baz][bar]` would match but `[foo][bar][baz]` does not.
 
+Other allowed expressions:
+
+* `(foo|bar)&!baz`
+* `!(foo|bar)`
+
 
 Here are some common patterns we may want to use:
 
 * `kore|booster` - log everything from kore and booster
-* `kore|booster>!kore-term.` - log everything from kore and booster except for the innermost `kore-term` contexts, which contain the pretty printed terms
+* `kore|booster>!(kore-term|detail).` - log everything from kore and booster except for the innermost `kore-term` or `detail` contexts, which contain the pretty printed terms and extra details about e.g. rule locations which may be too noisy.
 * `kore|booster>simplification*` - log every simplification rule attempt from kore and booster
 * `kore|booster>simplification*|equation*` - log every simplification and function application attempt from kore and booster
 * `ceil>partial-symbols.` - log a minimal ceil analysis showing all the rules which contain partial symbols on the RHS and aren't marked as preserving definedness