    {-|
    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 PolyKinds #-}
    {-# LANGUAGE ViewPatterns #-}
    module What4.Expr.BoolMap
      ( BoolMap
      , var
      , addVar
      , fromVars
      , combine
      , Polarity(..)
      , negatePolarity
      , contains
      , isInconsistent
      , isNull
      , BoolMapView(..)
      , viewBoolMap
      , traverseVars
      , reversePolarities
      , removeVar
      , Wrap(..)
      ) where

    import           Control.Lens (_1, over)
    import           Data.Hashable
    import           Data.List (foldl')
    import           Data.List.NonEmpty (NonEmpty(..))
    import           Data.Kind (Type)
    import           Data.Parameterized.Classes

    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

    -- | This data structure keeps track of a collection of expressions
    --   together with their polarities. Such a collection might represent
    --   either a conjunction or a disjunction of expressions.  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.

    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

    -- | 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 bool map
    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
    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)