{-|
Module      : What4.Expr.BoolMap
Description : Datastructure for representing a conjunction of predicates
Copyright   : (c) Galois Inc, 2019-2020
License     : BSD3
Maintainer  : rdockins@galois.com

Declares a datatype for representing n-way conjunctions or disjunctions
in a way that efficiently captures important algebraic
laws like commutativity, associativity and resolution.
-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module What4.Expr.BoolMap
  ( BoolMap
  , var
  , addVar
  , fromVars
  , combine
  , Polarity(..)
  , negatePolarity
  , contains
  , isInconsistent
  , isNull
  , BoolMapView(..)
  , viewBoolMap
  , foldMapVars
  , traverseVars
  , reversePolarities
  , removeVar
  , Wrap(..)
    -- * 'ConjMap'
  , ConjMap(..)
  , ConjMapView
  , pattern ConjTrue
  , pattern ConjFalse
  , pattern Conjuncts
  , viewConjMap
  , addConjunct
  , evalConj
  ) where

import           Control.Lens (_1, over)
import           Data.Coerce (coerce)
import           Data.Hashable
import qualified Data.List as List (foldl')
import           Data.List.NonEmpty (NonEmpty(..))
import           Data.Kind (Type)
import           Data.Parameterized.Classes
import           Data.Parameterized.TraversableF

import           What4.BaseTypes
import qualified What4.Utils.AnnotatedMap as AM
import           What4.Utils.IncrHash

-- | Describes the occurrence of a variable or expression, whether it is
--   negated or not.
data Polarity = Positive | Negative
 deriving (Polarity -> Polarity -> Bool
(Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool) -> Eq Polarity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Polarity -> Polarity -> Bool
== :: Polarity -> Polarity -> Bool
$c/= :: Polarity -> Polarity -> Bool
/= :: Polarity -> Polarity -> Bool
Eq,Eq Polarity
Eq Polarity =>
(Polarity -> Polarity -> Ordering)
-> (Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Polarity)
-> (Polarity -> Polarity -> Polarity)
-> Ord Polarity
Polarity -> Polarity -> Bool
Polarity -> Polarity -> Ordering
Polarity -> Polarity -> Polarity
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Polarity -> Polarity -> Ordering
compare :: Polarity -> Polarity -> Ordering
$c< :: Polarity -> Polarity -> Bool
< :: Polarity -> Polarity -> Bool
$c<= :: Polarity -> Polarity -> Bool
<= :: Polarity -> Polarity -> Bool
$c> :: Polarity -> Polarity -> Bool
> :: Polarity -> Polarity -> Bool
$c>= :: Polarity -> Polarity -> Bool
>= :: Polarity -> Polarity -> Bool
$cmax :: Polarity -> Polarity -> Polarity
max :: Polarity -> Polarity -> Polarity
$cmin :: Polarity -> Polarity -> Polarity
min :: Polarity -> Polarity -> Polarity
Ord,Int -> Polarity -> ShowS
[Polarity] -> ShowS
Polarity -> String
(Int -> Polarity -> ShowS)
-> (Polarity -> String) -> ([Polarity] -> ShowS) -> Show Polarity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Polarity -> ShowS
showsPrec :: Int -> Polarity -> ShowS
$cshow :: Polarity -> String
show :: Polarity -> String
$cshowList :: [Polarity] -> ShowS
showList :: [Polarity] -> ShowS
Show)

instance Hashable Polarity where
  hashWithSalt :: Int -> Polarity -> Int
hashWithSalt Int
s Polarity
Positive = Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
0::Int)
  hashWithSalt Int
s Polarity
Negative = Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
1::Int)

-- | Swap a polarity value
negatePolarity :: Polarity -> Polarity
negatePolarity :: Polarity -> Polarity
negatePolarity Polarity
Positive = Polarity
Negative
negatePolarity Polarity
Negative = Polarity
Positive

newtype Wrap (f :: k -> Type) (x :: k) = Wrap { forall k (f :: k -> Type) (x :: k). Wrap f x -> f x
unWrap:: f x }

instance TestEquality f => Eq (Wrap f x) where
  Wrap f x
a == :: Wrap f x -> Wrap f x -> Bool
== Wrap f x
b = Maybe (x :~: x) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (x :~: x) -> Bool) -> Maybe (x :~: x) -> Bool
forall a b. (a -> b) -> a -> b
$ f x -> f x -> Maybe (x :~: x)
forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f x
a f x
b
instance OrdF f => Ord (Wrap f x) where
  compare :: Wrap f x -> Wrap f x -> Ordering
compare (Wrap f x
a) (Wrap f x
b) = OrderingF x x -> Ordering
forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (OrderingF x x -> Ordering) -> OrderingF x x -> Ordering
forall a b. (a -> b) -> a -> b
$ f x -> f x -> OrderingF x x
forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF f x
a f x
b
instance (HashableF f, TestEquality f) => Hashable (Wrap f x) where
  hashWithSalt :: Int -> Wrap f x -> Int
hashWithSalt Int
s (Wrap f x
a) = Int -> f x -> Int
forall (tp :: k). Int -> f tp -> Int
forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF Int
s f x
a

-- | A representation of a conjunction or a disjunction.
--
--   This data structure keeps track of a collection of expressions together
--   with their polarities.  The implementation uses a map from expression
--   values to their polarities, and thus automatically implements the
--   associative, commutative and idempotency laws common to both conjunctions
--   and disjunctions.  Moreover, if the same expression occurs in the
--   collection with opposite polarities, the entire collection collapses
--   via a resolution step to an \"inconsistent\" map.  For conjunctions this
--   corresponds to a contradiction and represents false; for disjunction, this
--   corresponds to the law of the excluded middle and represents true.
--
--   The annotation on the 'AM.AnnotatedMap' is an incremental hash ('IncrHash')
--   of the map, used to support a fast 'Hashable' instance.

data BoolMap (f :: BaseType -> Type)
  = InconsistentMap
  | BoolMap !(AM.AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity)

instance OrdF f => Eq (BoolMap f) where
  BoolMap f
InconsistentMap == :: BoolMap f -> BoolMap f -> Bool
== BoolMap f
InconsistentMap = Bool
True
  BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m1 == BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m2 = (Polarity -> Polarity -> Bool)
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
-> Bool
forall k a v.
Eq k =>
(a -> a -> Bool)
-> AnnotatedMap k v a -> AnnotatedMap k v a -> Bool
AM.eqBy Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
(==) AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m1 AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m2
  BoolMap f
_ == BoolMap f
_ = Bool
False

instance OrdF f => Semigroup (BoolMap f) where
  <> :: BoolMap f -> BoolMap f -> BoolMap f
(<>) = BoolMap f -> BoolMap f -> BoolMap f
forall (f :: BaseType -> Type).
OrdF f =>
BoolMap f -> BoolMap f -> BoolMap f
combine

-- | Specialized version of 'foldMapVars'
instance FoldableF BoolMap where
  foldMapF :: forall m (e :: BaseType -> Type).
Monoid m =>
(forall (s :: BaseType). e s -> m) -> BoolMap e -> m
foldMapF forall (s :: BaseType). e s -> m
f = (e BaseBoolType -> m) -> BoolMap e -> m
forall m (f :: BaseType -> Type).
Monoid m =>
(f BaseBoolType -> m) -> BoolMap f -> m
foldMapVars e BaseBoolType -> m
forall (s :: BaseType). e s -> m
f

foldMapVars :: Monoid m => (f BaseBoolType -> m) -> BoolMap f -> m
foldMapVars :: forall m (f :: BaseType -> Type).
Monoid m =>
(f BaseBoolType -> m) -> BoolMap f -> m
foldMapVars f BaseBoolType -> m
_ BoolMap f
InconsistentMap = m
forall a. Monoid a => a
mempty
foldMapVars f BaseBoolType -> m
f (BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
am) = ((Wrap f BaseBoolType, Polarity) -> m)
-> [(Wrap f BaseBoolType, Polarity)] -> m
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (f BaseBoolType -> m
f (f BaseBoolType -> m)
-> ((Wrap f BaseBoolType, Polarity) -> f BaseBoolType)
-> (Wrap f BaseBoolType, Polarity)
-> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrap f BaseBoolType -> f BaseBoolType
forall k (f :: k -> Type) (x :: k). Wrap f x -> f x
unWrap (Wrap f BaseBoolType -> f BaseBoolType)
-> ((Wrap f BaseBoolType, Polarity) -> Wrap f BaseBoolType)
-> (Wrap f BaseBoolType, Polarity)
-> f BaseBoolType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Wrap f BaseBoolType, Polarity) -> Wrap f BaseBoolType
forall a b. (a, b) -> a
fst) (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
-> [(Wrap f BaseBoolType, Polarity)]
forall k v a. AnnotatedMap k v a -> [(k, a)]
AM.toList AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
am)

-- | Traverse the expressions in a bool map, and rebuild the map.
traverseVars :: (Applicative m, HashableF g, OrdF g) =>
  (f BaseBoolType -> m (g (BaseBoolType))) ->
  BoolMap f -> m (BoolMap g)
traverseVars :: forall (m :: Type -> Type) (g :: BaseType -> Type)
       (f :: BaseType -> Type).
(Applicative m, HashableF g, OrdF g) =>
(f BaseBoolType -> m (g BaseBoolType))
-> BoolMap f -> m (BoolMap g)
traverseVars f BaseBoolType -> m (g BaseBoolType)
_ BoolMap f
InconsistentMap = BoolMap g -> m (BoolMap g)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BoolMap g
forall (f :: BaseType -> Type). BoolMap f
InconsistentMap
traverseVars f BaseBoolType -> m (g BaseBoolType)
f (BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m) =
  [(g BaseBoolType, Polarity)] -> BoolMap g
forall (f :: BaseType -> Type).
(HashableF f, OrdF f) =>
[(f BaseBoolType, Polarity)] -> BoolMap f
fromVars ([(g BaseBoolType, Polarity)] -> BoolMap g)
-> m [(g BaseBoolType, Polarity)] -> m (BoolMap g)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Wrap f BaseBoolType, Polarity) -> m (g BaseBoolType, Polarity))
-> [(Wrap f BaseBoolType, Polarity)]
-> m [(g BaseBoolType, Polarity)]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((Wrap f BaseBoolType -> m (g BaseBoolType))
-> (Wrap f BaseBoolType, Polarity) -> m (g BaseBoolType, Polarity)
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (Wrap f BaseBoolType, Polarity)
  (g BaseBoolType, Polarity)
  (Wrap f BaseBoolType)
  (g BaseBoolType)
_1 (f BaseBoolType -> m (g BaseBoolType)
f (f BaseBoolType -> m (g BaseBoolType))
-> (Wrap f BaseBoolType -> f BaseBoolType)
-> Wrap f BaseBoolType
-> m (g BaseBoolType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrap f BaseBoolType -> f BaseBoolType
forall k (f :: k -> Type) (x :: k). Wrap f x -> f x
unWrap)) (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
-> [(Wrap f BaseBoolType, Polarity)]
forall k v a. AnnotatedMap k v a -> [(k, a)]
AM.toList AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m)

elementHash :: HashableF f => f BaseBoolType -> Polarity -> IncrHash
elementHash :: forall (f :: BaseType -> Type).
HashableF f =>
f BaseBoolType -> Polarity -> IncrHash
elementHash f BaseBoolType
x Polarity
p = Int -> IncrHash
mkIncrHash (Int -> f BaseBoolType -> Int
forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
forall (tp :: BaseType). Int -> f tp -> Int
hashWithSaltF (Polarity -> Int
forall a. Hashable a => a -> Int
hash Polarity
p) f BaseBoolType
x)

instance (OrdF f, HashableF f) => Hashable (BoolMap f) where
  hashWithSalt :: Int -> BoolMap f -> Int
hashWithSalt Int
s BoolMap f
InconsistentMap = Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
0::Int)
  hashWithSalt Int
s (BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m) =
    case AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
-> Maybe IncrHash
forall k v a. (Ord k, Semigroup v) => AnnotatedMap k v a -> Maybe v
AM.annotation AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m of
      Maybe IncrHash
Nothing -> Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
1::Int)
      Just IncrHash
h  -> Int -> IncrHash -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt (Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
1::Int)) IncrHash
h

-- | Represents the state of a 'BoolMap' (either a conjunction or disjunction).
--
-- If you know you are dealing with a 'BoolMap' that represents a conjunction,
-- consider using 'ConjMap' and 'viewConjMap' for the sake of clarity.
data BoolMapView f
  = BoolMapUnit
       -- ^ A bool map with no expressions, represents the unit of the corresponding operation
  | BoolMapDualUnit
       -- ^ An inconsistent bool map, represents the dual of the operation unit
  | BoolMapTerms (NonEmpty (f BaseBoolType, Polarity))
       -- ^ The terms appearing in the bool map, of which there is at least one

-- | Deconstruct the given bool map for later processing
viewBoolMap :: BoolMap f -> BoolMapView f
viewBoolMap :: forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
viewBoolMap BoolMap f
InconsistentMap = BoolMapView f
forall (f :: BaseType -> Type). BoolMapView f
BoolMapDualUnit
viewBoolMap (BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m) =
  case AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
-> [(Wrap f BaseBoolType, Polarity)]
forall k v a. AnnotatedMap k v a -> [(k, a)]
AM.toList AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m of
    []  -> BoolMapView f
forall (f :: BaseType -> Type). BoolMapView f
BoolMapUnit
    (Wrap f BaseBoolType
x,Polarity
p):[(Wrap f BaseBoolType, Polarity)]
xs -> NonEmpty (f BaseBoolType, Polarity) -> BoolMapView f
forall (f :: BaseType -> Type).
NonEmpty (f BaseBoolType, Polarity) -> BoolMapView f
BoolMapTerms ((f BaseBoolType
x,Polarity
p)(f BaseBoolType, Polarity)
-> [(f BaseBoolType, Polarity)]
-> NonEmpty (f BaseBoolType, Polarity)
forall a. a -> [a] -> NonEmpty a
:|(((Wrap f BaseBoolType, Polarity) -> (f BaseBoolType, Polarity))
-> [(Wrap f BaseBoolType, Polarity)]
-> [(f BaseBoolType, Polarity)]
forall a b. (a -> b) -> [a] -> [b]
map (ASetter
  (Wrap f BaseBoolType, Polarity)
  (f BaseBoolType, Polarity)
  (Wrap f BaseBoolType)
  (f BaseBoolType)
-> (Wrap f BaseBoolType -> f BaseBoolType)
-> (Wrap f BaseBoolType, Polarity)
-> (f BaseBoolType, Polarity)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (Wrap f BaseBoolType, Polarity)
  (f BaseBoolType, Polarity)
  (Wrap f BaseBoolType)
  (f BaseBoolType)
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (Wrap f BaseBoolType, Polarity)
  (f BaseBoolType, Polarity)
  (Wrap f BaseBoolType)
  (f BaseBoolType)
_1 Wrap f BaseBoolType -> f BaseBoolType
forall k (f :: k -> Type) (x :: k). Wrap f x -> f x
unWrap) [(Wrap f BaseBoolType, Polarity)]
xs))

-- | Returns true for an inconsistent bool map
isInconsistent :: BoolMap f -> Bool
isInconsistent :: forall (f :: BaseType -> Type). BoolMap f -> Bool
isInconsistent BoolMap f
InconsistentMap = Bool
True
isInconsistent BoolMap f
_ = Bool
False

-- | Returns true for a \"null\" bool map with no terms
isNull :: BoolMap f -> Bool
isNull :: forall (f :: BaseType -> Type). BoolMap f -> Bool
isNull BoolMap f
InconsistentMap = Bool
False
isNull (BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m) = AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> Bool
forall k v a. AnnotatedMap k v a -> Bool
AM.null AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m

-- | Produce a singleton bool map, consisting of just the given term
var :: (HashableF f, OrdF f) => f BaseBoolType -> Polarity -> BoolMap f
var :: forall (f :: BaseType -> Type).
(HashableF f, OrdF f) =>
f BaseBoolType -> Polarity -> BoolMap f
var f BaseBoolType
x Polarity
p = AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> BoolMap f
forall (f :: BaseType -> Type).
AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> BoolMap f
BoolMap (Wrap f BaseBoolType
-> IncrHash
-> Polarity
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
forall k v a.
(Ord k, Semigroup v) =>
k -> v -> a -> AnnotatedMap k v a
AM.singleton (f BaseBoolType -> Wrap f BaseBoolType
forall k (f :: k -> Type) (x :: k). f x -> Wrap f x
Wrap f BaseBoolType
x) (f BaseBoolType -> Polarity -> IncrHash
forall (f :: BaseType -> Type).
HashableF f =>
f BaseBoolType -> Polarity -> IncrHash
elementHash f BaseBoolType
x Polarity
p) Polarity
p)

-- | Add a variable to a bool map, performing a resolution step if possible
addVar :: (HashableF f, OrdF f) => f BaseBoolType -> Polarity -> BoolMap f -> BoolMap f
addVar :: forall (f :: BaseType -> Type).
(HashableF f, OrdF f) =>
f BaseBoolType -> Polarity -> BoolMap f -> BoolMap f
addVar f BaseBoolType
_ Polarity
_ BoolMap f
InconsistentMap = BoolMap f
forall (f :: BaseType -> Type). BoolMap f
InconsistentMap
addVar f BaseBoolType
x Polarity
p1 (BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
bm) = BoolMap f
-> (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
    -> BoolMap f)
-> Maybe (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity)
-> BoolMap f
forall b a. b -> (a -> b) -> Maybe a -> b
maybe BoolMap f
forall (f :: BaseType -> Type). BoolMap f
InconsistentMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> BoolMap f
forall (f :: BaseType -> Type).
AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> BoolMap f
BoolMap (Maybe (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity)
 -> BoolMap f)
-> Maybe (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity)
-> BoolMap f
forall a b. (a -> b) -> a -> b
$ (Maybe (IncrHash, Polarity) -> Maybe (Maybe (IncrHash, Polarity)))
-> Wrap f BaseBoolType
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
-> Maybe (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity)
forall (f :: Type -> Type) k v a.
(Functor f, Ord k, Semigroup v) =>
(Maybe (v, a) -> f (Maybe (v, a)))
-> k -> AnnotatedMap k v a -> f (AnnotatedMap k v a)
AM.alterF Maybe (IncrHash, Polarity) -> Maybe (Maybe (IncrHash, Polarity))
f (f BaseBoolType -> Wrap f BaseBoolType
forall k (f :: k -> Type) (x :: k). f x -> Wrap f x
Wrap f BaseBoolType
x) AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
bm
 where
 f :: Maybe (IncrHash, Polarity) -> Maybe (Maybe (IncrHash, Polarity))
f Maybe (IncrHash, Polarity)
Nothing = Maybe (IncrHash, Polarity) -> Maybe (Maybe (IncrHash, Polarity))
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((IncrHash, Polarity) -> Maybe (IncrHash, Polarity)
forall a. a -> Maybe a
Just (f BaseBoolType -> Polarity -> IncrHash
forall (f :: BaseType -> Type).
HashableF f =>
f BaseBoolType -> Polarity -> IncrHash
elementHash f BaseBoolType
x Polarity
p1, Polarity
p1))
 f el :: Maybe (IncrHash, Polarity)
el@(Just (IncrHash
_,Polarity
p2)) | Polarity
p1 Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
p2  = Maybe (IncrHash, Polarity) -> Maybe (Maybe (IncrHash, Polarity))
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (IncrHash, Polarity)
el
                    | Bool
otherwise = Maybe (Maybe (IncrHash, Polarity))
forall a. Maybe a
Nothing

-- | Generate a bool map from a list of terms and polarities by repeatedly
--   calling @addVar@.
fromVars :: (HashableF f, OrdF f) => [(f BaseBoolType, Polarity)] -> BoolMap f
fromVars :: forall (f :: BaseType -> Type).
(HashableF f, OrdF f) =>
[(f BaseBoolType, Polarity)] -> BoolMap f
fromVars = (BoolMap f -> (f BaseBoolType, Polarity) -> BoolMap f)
-> BoolMap f -> [(f BaseBoolType, Polarity)] -> BoolMap f
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\BoolMap f
m (f BaseBoolType
x,Polarity
p) -> f BaseBoolType -> Polarity -> BoolMap f -> BoolMap f
forall (f :: BaseType -> Type).
(HashableF f, OrdF f) =>
f BaseBoolType -> Polarity -> BoolMap f -> BoolMap f
addVar f BaseBoolType
x Polarity
p BoolMap f
m) (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> BoolMap f
forall (f :: BaseType -> Type).
AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> BoolMap f
BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
forall k v a. (Ord k, Semigroup v) => AnnotatedMap k v a
AM.empty)

-- | Merge two bool maps, performing resolution as necessary.
combine :: OrdF f => BoolMap f -> BoolMap f -> BoolMap f
combine :: forall (f :: BaseType -> Type).
OrdF f =>
BoolMap f -> BoolMap f -> BoolMap f
combine BoolMap f
InconsistentMap BoolMap f
_ = BoolMap f
forall (f :: BaseType -> Type). BoolMap f
InconsistentMap
combine BoolMap f
_ BoolMap f
InconsistentMap = BoolMap f
forall (f :: BaseType -> Type). BoolMap f
InconsistentMap
combine (BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m1) (BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m2) =
    BoolMap f
-> (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
    -> BoolMap f)
-> Maybe (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity)
-> BoolMap f
forall b a. b -> (a -> b) -> Maybe a -> b
maybe BoolMap f
forall (f :: BaseType -> Type). BoolMap f
InconsistentMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> BoolMap f
forall (f :: BaseType -> Type).
AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> BoolMap f
BoolMap (Maybe (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity)
 -> BoolMap f)
-> Maybe (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity)
-> BoolMap f
forall a b. (a -> b) -> a -> b
$ (Wrap f BaseBoolType
 -> (IncrHash, Polarity)
 -> (IncrHash, Polarity)
 -> Maybe (IncrHash, Polarity))
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
-> Maybe (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity)
forall k v (f :: Type -> Type) a.
(Ord k, Semigroup v, Applicative f) =>
(k -> (v, a) -> (v, a) -> f (v, a))
-> AnnotatedMap k v a
-> AnnotatedMap k v a
-> f (AnnotatedMap k v a)
AM.mergeA Wrap f BaseBoolType
-> (IncrHash, Polarity)
-> (IncrHash, Polarity)
-> Maybe (IncrHash, Polarity)
forall {b} {p} {a} {a}.
Eq b =>
p -> (a, b) -> (a, b) -> Maybe (a, b)
f AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m1 AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m2

  where f :: p -> (a, b) -> (a, b) -> Maybe (a, b)
f p
_k (a
v,b
p1) (a
_,b
p2)
          | b
p1 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
p2  = (a, b) -> Maybe (a, b)
forall a. a -> Maybe a
Just (a
v,b
p1)
          | Bool
otherwise = Maybe (a, b)
forall a. Maybe a
Nothing

-- | Test if the bool map contains the given term, and return the polarity
--   of that term if so.
contains :: OrdF f => BoolMap f -> f BaseBoolType -> Maybe Polarity
contains :: forall (f :: BaseType -> Type).
OrdF f =>
BoolMap f -> f BaseBoolType -> Maybe Polarity
contains BoolMap f
InconsistentMap f BaseBoolType
_ = Maybe Polarity
forall a. Maybe a
Nothing
contains (BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m) f BaseBoolType
x = (IncrHash, Polarity) -> Polarity
forall a b. (a, b) -> b
snd ((IncrHash, Polarity) -> Polarity)
-> Maybe (IncrHash, Polarity) -> Maybe Polarity
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Wrap f BaseBoolType
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
-> Maybe (IncrHash, Polarity)
forall k v a.
(Ord k, Semigroup v) =>
k -> AnnotatedMap k v a -> Maybe (v, a)
AM.lookup (f BaseBoolType -> Wrap f BaseBoolType
forall k (f :: k -> Type) (x :: k). f x -> Wrap f x
Wrap f BaseBoolType
x) AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m

-- | Swap the polarities of the terms in the given bool map.
reversePolarities :: OrdF f => BoolMap f -> BoolMap f
reversePolarities :: forall (f :: BaseType -> Type). OrdF f => BoolMap f -> BoolMap f
reversePolarities BoolMap f
InconsistentMap = BoolMap f
forall (f :: BaseType -> Type). BoolMap f
InconsistentMap
reversePolarities (BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m) = AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> BoolMap f
forall (f :: BaseType -> Type).
AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> BoolMap f
BoolMap (AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> BoolMap f)
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
-> BoolMap f
forall a b. (a -> b) -> a -> b
$! (Polarity -> Polarity)
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
forall a b.
(a -> b)
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash a
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Polarity -> Polarity
negatePolarity AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m

-- | Remove the given term from the bool map.  The map is unchanged
--   if inconsistent or if the term does not occur.
removeVar :: OrdF f => BoolMap f -> f BaseBoolType -> BoolMap f
removeVar :: forall (f :: BaseType -> Type).
OrdF f =>
BoolMap f -> f BaseBoolType -> BoolMap f
removeVar BoolMap f
InconsistentMap f BaseBoolType
_ = BoolMap f
forall (f :: BaseType -> Type). BoolMap f
InconsistentMap
removeVar (BoolMap AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m) f BaseBoolType
x = AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> BoolMap f
forall (f :: BaseType -> Type).
AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity -> BoolMap f
BoolMap (Wrap f BaseBoolType
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
-> AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
forall k v a.
(Ord k, Semigroup v) =>
k -> AnnotatedMap k v a -> AnnotatedMap k v a
AM.delete (f BaseBoolType -> Wrap f BaseBoolType
forall k (f :: k -> Type) (x :: k). f x -> Wrap f x
Wrap f BaseBoolType
x) AnnotatedMap (Wrap f BaseBoolType) IncrHash Polarity
m)

--------------------------------------------------------------------------------
-- ConjMap

-- | A 'BoolMap' representing a conjunction.
newtype ConjMap f = ConjMap { forall (f :: BaseType -> Type). ConjMap f -> BoolMap f
getConjMap :: BoolMap f }
  deriving (ConjMap f -> ConjMap f -> Bool
(ConjMap f -> ConjMap f -> Bool)
-> (ConjMap f -> ConjMap f -> Bool) -> Eq (ConjMap f)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (f :: BaseType -> Type).
OrdF f =>
ConjMap f -> ConjMap f -> Bool
$c== :: forall (f :: BaseType -> Type).
OrdF f =>
ConjMap f -> ConjMap f -> Bool
== :: ConjMap f -> ConjMap f -> Bool
$c/= :: forall (f :: BaseType -> Type).
OrdF f =>
ConjMap f -> ConjMap f -> Bool
/= :: ConjMap f -> ConjMap f -> Bool
Eq, (forall m (e :: BaseType -> Type).
 Monoid m =>
 (forall (s :: BaseType). e s -> m) -> ConjMap e -> m)
-> (forall (e :: BaseType -> Type) b.
    (forall (s :: BaseType). e s -> b -> b) -> b -> ConjMap e -> b)
-> (forall b (e :: BaseType -> Type).
    (forall (s :: BaseType). b -> e s -> b) -> b -> ConjMap e -> b)
-> (forall (e :: BaseType -> Type) b.
    (forall (s :: BaseType). e s -> b -> b) -> b -> ConjMap e -> b)
-> (forall b (e :: BaseType -> Type).
    (forall (s :: BaseType). b -> e s -> b) -> b -> ConjMap e -> b)
-> (forall (f :: BaseType -> Type) a.
    (forall (tp :: BaseType). f tp -> a) -> ConjMap f -> [a])
-> FoldableF ConjMap
forall m (e :: BaseType -> Type).
Monoid m =>
(forall (s :: BaseType). e s -> m) -> ConjMap e -> m
forall b (e :: BaseType -> Type).
(forall (s :: BaseType). b -> e s -> b) -> b -> ConjMap e -> b
forall k (t :: (k -> Type) -> Type).
(forall m (e :: k -> Type).
 Monoid m =>
 (forall (s :: k). e s -> m) -> t e -> m)
-> (forall (e :: k -> Type) b.
    (forall (s :: k). e s -> b -> b) -> b -> t e -> b)
-> (forall b (e :: k -> Type).
    (forall (s :: k). b -> e s -> b) -> b -> t e -> b)
-> (forall (e :: k -> Type) b.
    (forall (s :: k). e s -> b -> b) -> b -> t e -> b)
-> (forall b (e :: k -> Type).
    (forall (s :: k). b -> e s -> b) -> b -> t e -> b)
-> (forall (f :: k -> Type) a.
    (forall (tp :: k). f tp -> a) -> t f -> [a])
-> FoldableF t
forall (f :: BaseType -> Type) a.
(forall (tp :: BaseType). f tp -> a) -> ConjMap f -> [a]
forall (e :: BaseType -> Type) b.
(forall (s :: BaseType). e s -> b -> b) -> b -> ConjMap e -> b
$cfoldMapF :: forall m (e :: BaseType -> Type).
Monoid m =>
(forall (s :: BaseType). e s -> m) -> ConjMap e -> m
foldMapF :: forall m (e :: BaseType -> Type).
Monoid m =>
(forall (s :: BaseType). e s -> m) -> ConjMap e -> m
$cfoldrF :: forall (e :: BaseType -> Type) b.
(forall (s :: BaseType). e s -> b -> b) -> b -> ConjMap e -> b
foldrF :: forall (e :: BaseType -> Type) b.
(forall (s :: BaseType). e s -> b -> b) -> b -> ConjMap e -> b
$cfoldlF :: forall b (e :: BaseType -> Type).
(forall (s :: BaseType). b -> e s -> b) -> b -> ConjMap e -> b
foldlF :: forall b (e :: BaseType -> Type).
(forall (s :: BaseType). b -> e s -> b) -> b -> ConjMap e -> b
$cfoldrF' :: forall (e :: BaseType -> Type) b.
(forall (s :: BaseType). e s -> b -> b) -> b -> ConjMap e -> b
foldrF' :: forall (e :: BaseType -> Type) b.
(forall (s :: BaseType). e s -> b -> b) -> b -> ConjMap e -> b
$cfoldlF' :: forall b (e :: BaseType -> Type).
(forall (s :: BaseType). b -> e s -> b) -> b -> ConjMap e -> b
foldlF' :: forall b (e :: BaseType -> Type).
(forall (s :: BaseType). b -> e s -> b) -> b -> ConjMap e -> b
$ctoListF :: forall (f :: BaseType -> Type) a.
(forall (tp :: BaseType). f tp -> a) -> ConjMap f -> [a]
toListF :: forall (f :: BaseType -> Type) a.
(forall (tp :: BaseType). f tp -> a) -> ConjMap f -> [a]
FoldableF, Eq (ConjMap f)
Eq (ConjMap f) =>
(Int -> ConjMap f -> Int)
-> (ConjMap f -> Int) -> Hashable (ConjMap f)
Int -> ConjMap f -> Int
ConjMap f -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall (f :: BaseType -> Type).
(OrdF f, HashableF f) =>
Eq (ConjMap f)
forall (f :: BaseType -> Type).
(OrdF f, HashableF f) =>
Int -> ConjMap f -> Int
forall (f :: BaseType -> Type).
(OrdF f, HashableF f) =>
ConjMap f -> Int
$chashWithSalt :: forall (f :: BaseType -> Type).
(OrdF f, HashableF f) =>
Int -> ConjMap f -> Int
hashWithSalt :: Int -> ConjMap f -> Int
$chash :: forall (f :: BaseType -> Type).
(OrdF f, HashableF f) =>
ConjMap f -> Int
hash :: ConjMap f -> Int
Hashable, NonEmpty (ConjMap f) -> ConjMap f
ConjMap f -> ConjMap f -> ConjMap f
(ConjMap f -> ConjMap f -> ConjMap f)
-> (NonEmpty (ConjMap f) -> ConjMap f)
-> (forall b. Integral b => b -> ConjMap f -> ConjMap f)
-> Semigroup (ConjMap f)
forall b. Integral b => b -> ConjMap f -> ConjMap f
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall (f :: BaseType -> Type).
OrdF f =>
NonEmpty (ConjMap f) -> ConjMap f
forall (f :: BaseType -> Type).
OrdF f =>
ConjMap f -> ConjMap f -> ConjMap f
forall (f :: BaseType -> Type) b.
(OrdF f, Integral b) =>
b -> ConjMap f -> ConjMap f
$c<> :: forall (f :: BaseType -> Type).
OrdF f =>
ConjMap f -> ConjMap f -> ConjMap f
<> :: ConjMap f -> ConjMap f -> ConjMap f
$csconcat :: forall (f :: BaseType -> Type).
OrdF f =>
NonEmpty (ConjMap f) -> ConjMap f
sconcat :: NonEmpty (ConjMap f) -> ConjMap f
$cstimes :: forall (f :: BaseType -> Type) b.
(OrdF f, Integral b) =>
b -> ConjMap f -> ConjMap f
stimes :: forall b. Integral b => b -> ConjMap f -> ConjMap f
Semigroup)

-- | Represents the state of a 'ConjMap'. See 'viewConjMap'.
--
-- Like 'BoolMapView', but with more specific patterns for readability.
newtype ConjMapView f = ConjMapView (BoolMapView f)

pattern ConjTrue :: ConjMapView f
pattern $mConjTrue :: forall {r} {f :: BaseType -> Type}.
ConjMapView f -> ((# #) -> r) -> ((# #) -> r) -> r
$bConjTrue :: forall (f :: BaseType -> Type). ConjMapView f
ConjTrue = ConjMapView BoolMapUnit

pattern ConjFalse :: ConjMapView f
pattern $mConjFalse :: forall {r} {f :: BaseType -> Type}.
ConjMapView f -> ((# #) -> r) -> ((# #) -> r) -> r
$bConjFalse :: forall (f :: BaseType -> Type). ConjMapView f
ConjFalse = ConjMapView BoolMapDualUnit

pattern Conjuncts :: NonEmpty (f BaseBoolType, Polarity) -> ConjMapView f
pattern $mConjuncts :: forall {r} {f :: BaseType -> Type}.
ConjMapView f
-> (NonEmpty (f BaseBoolType, Polarity) -> r) -> ((# #) -> r) -> r
$bConjuncts :: forall (f :: BaseType -> Type).
NonEmpty (f BaseBoolType, Polarity) -> ConjMapView f
Conjuncts ts = ConjMapView (BoolMapTerms ts)

{-# COMPLETE ConjTrue, ConjFalse, Conjuncts #-}

-- | Deconstruct the given 'ConjMap' for later processing
viewConjMap :: forall f. ConjMap f -> ConjMapView f
viewConjMap :: forall (f :: BaseType -> Type). ConjMap f -> ConjMapView f
viewConjMap =
  -- The explicit type annotations on `coerce` are likely necessary because of
  -- https://gitlab.haskell.org/ghc/ghc/-/issues/21003
  forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @(BoolMap f -> BoolMapView f) @(ConjMap f -> ConjMapView f) BoolMap f -> BoolMapView f
forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
viewBoolMap
{-# INLINE viewConjMap #-}

-- | Add a conjunct to a 'ConjMap'.
--
-- Wrapper around 'addVar'.
addConjunct ::
  forall f.
  (HashableF f, OrdF f) =>
  f BaseBoolType ->
  Polarity ->
  ConjMap f ->
  ConjMap f
addConjunct :: forall (f :: BaseType -> Type).
(HashableF f, OrdF f) =>
f BaseBoolType -> Polarity -> ConjMap f -> ConjMap f
addConjunct =
  -- The explicit type annotations on `coerce` are likely necessary because of
  -- https://gitlab.haskell.org/ghc/ghc/-/issues/21003
  forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce
    @(f BaseBoolType -> Polarity -> BoolMap f -> BoolMap f)
    @(f BaseBoolType -> Polarity -> ConjMap f -> ConjMap f)
    f BaseBoolType -> Polarity -> BoolMap f -> BoolMap f
forall (f :: BaseType -> Type).
(HashableF f, OrdF f) =>
f BaseBoolType -> Polarity -> BoolMap f -> BoolMap f
addVar
{-# INLINE addConjunct #-}

-- | Given the means to evaluate the conjuncts of a 'ConjMap' to a concrete
-- 'Bool', evaluate the whole conjunction to a 'Bool'.
evalConj :: Applicative m => (f BaseBoolType -> m Bool) -> ConjMap f -> m Bool
evalConj :: forall (m :: Type -> Type) (f :: BaseType -> Type).
Applicative m =>
(f BaseBoolType -> m Bool) -> ConjMap f -> m Bool
evalConj f BaseBoolType -> m Bool
f ConjMap f
cm =
  let pol :: (f BaseBoolType, Polarity) -> m Bool
pol (f BaseBoolType
x, Polarity
Positive) = f BaseBoolType -> m Bool
f f BaseBoolType
x
      pol (f BaseBoolType
x, Polarity
Negative) = Bool -> Bool
not (Bool -> Bool) -> m Bool -> m Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f BaseBoolType -> m Bool
f f BaseBoolType
x
  in
  case ConjMap f -> ConjMapView f
forall (f :: BaseType -> Type). ConjMap f -> ConjMapView f
viewConjMap ConjMap f
cm of
    ConjMapView f
ConjTrue -> Bool -> m Bool
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True
    ConjMapView f
ConjFalse -> Bool -> m Bool
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
    Conjuncts ((f BaseBoolType, Polarity)
t:|[(f BaseBoolType, Polarity)]
ts) ->
      (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Bool -> Bool -> Bool
(&&) (Bool -> [Bool] -> Bool) -> m Bool -> m ([Bool] -> Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (f BaseBoolType, Polarity) -> m Bool
pol (f BaseBoolType, Polarity)
t m ([Bool] -> Bool) -> m [Bool] -> m Bool
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ((f BaseBoolType, Polarity) -> m Bool)
-> [(f BaseBoolType, Polarity)] -> m [Bool]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (f BaseBoolType, Polarity) -> m Bool
pol [(f BaseBoolType, Polarity)]
ts