{-# OPTIONS_HADDOCK ignore-exports #-}
{-# OPTIONS_GHC -Wno-orphans #-} -- the Foldable instance for GHC.UniqFM is an orphan
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}

{-|
    Atomic constraints and sets of atomic constraints, represented as antichains.  Saturation and restriction. 
-}
module Intensional.Constraints
  ( 
    CInfo(..),
    modInfo,
    spanInfo,
    Atomic,
    Constraint (..),
    ConstraintSet,
    insert,
    guardWith,
    toList,
    fromList,
    isTriviallyUnsat,
    unsats,
    saturate,
    cexs,
    size,
  )
where

import Binary
import Data.Foldable
import Control.Monad.State (State)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.IntMap (IntMap)
import Data.HashMap.Strict (HashMap)
import Data.IntSet (IntSet)
import qualified Control.Monad.State as State
import qualified Data.HashMap.Strict as HashMap
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import qualified Data.Maybe as Maybe
import qualified GhcPlugins as GHC
import qualified Control.Monad as Monad

import Intensional.Ubiq
import Intensional.Types
import Intensional.Constructors
import Intensional.Guard (Guard)
import qualified Intensional.Guard as Guard

import Debug.Trace


{-| 
    Type type of auxilliary information attached to 
    constraints @c@:

      * @prov c@ is the module in which the constraint was created
      * @span c@ is the originating location of the rhs of the constraint
    
    INV: CInfo does not determine equality of constraints.
-}
data CInfo =
  CInfo {
    CInfo -> Module
prov :: GHC.Module,
    CInfo -> SrcSpan
sspn :: GHC.SrcSpan
  }
  deriving (CInfo -> CInfo -> Bool
(CInfo -> CInfo -> Bool) -> (CInfo -> CInfo -> Bool) -> Eq CInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CInfo -> CInfo -> Bool
$c/= :: CInfo -> CInfo -> Bool
== :: CInfo -> CInfo -> Bool
$c== :: CInfo -> CInfo -> Bool
Eq, Eq CInfo
Eq CInfo =>
(CInfo -> CInfo -> Ordering)
-> (CInfo -> CInfo -> Bool)
-> (CInfo -> CInfo -> Bool)
-> (CInfo -> CInfo -> Bool)
-> (CInfo -> CInfo -> Bool)
-> (CInfo -> CInfo -> CInfo)
-> (CInfo -> CInfo -> CInfo)
-> Ord CInfo
CInfo -> CInfo -> Bool
CInfo -> CInfo -> Ordering
CInfo -> CInfo -> CInfo
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
min :: CInfo -> CInfo -> CInfo
$cmin :: CInfo -> CInfo -> CInfo
max :: CInfo -> CInfo -> CInfo
$cmax :: CInfo -> CInfo -> CInfo
>= :: CInfo -> CInfo -> Bool
$c>= :: CInfo -> CInfo -> Bool
> :: CInfo -> CInfo -> Bool
$c> :: CInfo -> CInfo -> Bool
<= :: CInfo -> CInfo -> Bool
$c<= :: CInfo -> CInfo -> Bool
< :: CInfo -> CInfo -> Bool
$c< :: CInfo -> CInfo -> Bool
compare :: CInfo -> CInfo -> Ordering
$ccompare :: CInfo -> CInfo -> Ordering
$cp1Ord :: Eq CInfo
Ord)

instance GHC.Outputable CInfo where
  ppr :: CInfo -> SDoc
ppr (CInfo _ sp :: SrcSpan
sp) = SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr SrcSpan
sp

instance Binary CInfo where
  put_ :: BinHandle -> CInfo -> IO ()
put_ bh :: BinHandle
bh (CInfo m :: Module
m sp :: SrcSpan
sp) = BinHandle -> Module -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh Module
m IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> SrcSpan -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh SrcSpan
sp 
  get :: BinHandle -> IO CInfo
get bh :: BinHandle
bh = (Module -> SrcSpan -> CInfo) -> IO Module -> IO SrcSpan -> IO CInfo
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
Monad.liftM2 Module -> SrcSpan -> CInfo
CInfo (BinHandle -> IO Module
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh) (BinHandle -> IO SrcSpan
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh)
    

{-|
    The type of constraints @c@ of shape @guard c@ ? @left c@ ⊆ @right c@ that originated from the 
    source at @srcSpan c@.
-}
type Atomic = Constraint 'L 'R

data Constraint l r
  = Constraint
      { Constraint l r -> K l
left :: K l,
        Constraint l r -> K r
right :: K r,
        Constraint l r -> Guard
guard :: Guard,
        Constraint l r -> CInfo
cinfo :: CInfo
      }

instance Eq (Constraint l r) where
  -- Disregard info in comparison
  Constraint l :: K l
l r :: K r
r g :: Guard
g _ == :: Constraint l r -> Constraint l r -> Bool
== Constraint l' :: K l
l' r' :: K r
r' g' :: Guard
g' _ = K l
l K l -> K l -> Bool
forall a. Eq a => a -> a -> Bool
== K l
l' Bool -> Bool -> Bool
&& K r
r K r -> K r -> Bool
forall a. Eq a => a -> a -> Bool
== K r
r' Bool -> Bool -> Bool
&& Guard
g Guard -> Guard -> Bool
forall a. Eq a => a -> a -> Bool
== Guard
g'

instance GHC.Outputable (Constraint l r) where
  ppr :: Constraint l r -> SDoc
ppr = (RVar -> SDoc) -> Constraint l r -> SDoc
forall t. Refined t => (RVar -> SDoc) -> t -> SDoc
prpr RVar -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr

instance (Binary (K l), Binary (K r)) => Binary (Constraint l r) where
  put_ :: BinHandle -> Constraint l r -> IO ()
put_ bh :: BinHandle
bh (Constraint l :: K l
l r :: K r
r g :: Guard
g ss :: CInfo
ss) = BinHandle -> K l -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh K l
l IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> K r -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh K r
r IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> Guard -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh Guard
g IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> CInfo -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh CInfo
ss
  get :: BinHandle -> IO (Constraint l r)
get bh :: BinHandle
bh = K l -> K r -> Guard -> CInfo -> Constraint l r
forall (l :: Side) (r :: Side).
K l -> K r -> Guard -> CInfo -> Constraint l r
Constraint (K l -> K r -> Guard -> CInfo -> Constraint l r)
-> IO (K l) -> IO (K r -> Guard -> CInfo -> Constraint l r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO (K l)
forall a. Binary a => BinHandle -> IO a
Binary.get BinHandle
bh IO (K r -> Guard -> CInfo -> Constraint l r)
-> IO (K r) -> IO (Guard -> CInfo -> Constraint l r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BinHandle -> IO (K r)
forall a. Binary a => BinHandle -> IO a
Binary.get BinHandle
bh IO (Guard -> CInfo -> Constraint l r)
-> IO Guard -> IO (CInfo -> Constraint l r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BinHandle -> IO Guard
forall a. Binary a => BinHandle -> IO a
Binary.get BinHandle
bh IO (CInfo -> Constraint l r) -> IO CInfo -> IO (Constraint l r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BinHandle -> IO CInfo
forall a. Binary a => BinHandle -> IO a
Binary.get BinHandle
bh

instance Refined (Constraint l r) where
  domain :: Constraint l r -> Domain
domain c :: Constraint l r
c = K l -> Domain
forall t. Refined t => t -> Domain
domain (Constraint l r -> K l
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Constraint l r
c) Domain -> Domain -> Domain
forall a. Semigroup a => a -> a -> a
<> K r -> Domain
forall t. Refined t => t -> Domain
domain (Constraint l r -> K r
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Constraint l r
c) Domain -> Domain -> Domain
forall a. Semigroup a => a -> a -> a
<> Guard -> Domain
forall t. Refined t => t -> Domain
domain (Constraint l r -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Constraint l r
c)
  rename :: RVar -> RVar -> Constraint l r -> Constraint l r
rename x :: RVar
x y :: RVar
y c :: Constraint l r
c =
    Constraint l r
c
      { left :: K l
left = RVar -> RVar -> K l -> K l
forall t. Refined t => RVar -> RVar -> t -> t
rename RVar
x RVar
y (Constraint l r -> K l
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Constraint l r
c),
        right :: K r
right = RVar -> RVar -> K r -> K r
forall t. Refined t => RVar -> RVar -> t -> t
rename RVar
x RVar
y (Constraint l r -> K r
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Constraint l r
c),
        guard :: Guard
guard = RVar -> RVar -> Guard -> Guard
forall t. Refined t => RVar -> RVar -> t -> t
rename RVar
x RVar
y (Constraint l r -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Constraint l r
c)
      }
  prpr :: (RVar -> SDoc) -> Constraint l r -> SDoc
prpr m :: RVar -> SDoc
m a :: Constraint l r
a = (RVar -> SDoc) -> Guard -> SDoc
forall t. Refined t => (RVar -> SDoc) -> t -> SDoc
prpr RVar -> SDoc
m (Constraint l r -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Constraint l r
a) SDoc -> SDoc -> SDoc
GHC.<+> Char -> SDoc
GHC.char '?' SDoc -> SDoc -> SDoc
GHC.<+> (RVar -> SDoc) -> K l -> SDoc
forall t. Refined t => (RVar -> SDoc) -> t -> SDoc
prpr RVar -> SDoc
m (Constraint l r -> K l
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Constraint l r
a) SDoc -> SDoc -> SDoc
GHC.<+> String -> SDoc
GHC.text "<=" SDoc -> SDoc -> SDoc
GHC.<+> (RVar -> SDoc) -> K r -> SDoc
forall t. Refined t => (RVar -> SDoc) -> t -> SDoc
prpr RVar -> SDoc
m (Constraint l r -> K r
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Constraint l r
a)

modInfo :: Atomic -> GHC.Module
modInfo :: Atomic -> Module
modInfo = CInfo -> Module
prov (CInfo -> Module) -> (Atomic -> CInfo) -> Atomic -> Module
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atomic -> CInfo
forall (l :: Side) (r :: Side). Constraint l r -> CInfo
cinfo

spanInfo :: Atomic -> GHC.SrcSpan
spanInfo :: Atomic -> SrcSpan
spanInfo = CInfo -> SrcSpan
sspn (CInfo -> SrcSpan) -> (Atomic -> CInfo) -> Atomic -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atomic -> CInfo
forall (l :: Side) (r :: Side). Constraint l r -> CInfo
cinfo

{-|
    Given an atomic constraint @a@, @isTriviallyUnsat a@ just if @a@ is of the form G ? k in {}.
-}
isTriviallyUnsat :: Atomic -> Bool
isTriviallyUnsat :: Atomic -> Bool
isTriviallyUnsat a :: Atomic
a =
    case (Guard -> Bool
Guard.isEmpty (Atomic -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Atomic
a), Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
a, Atomic -> K 'R
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Atomic
a) of
      (True, Con _ _, Set ks :: UniqSet Name
ks _) | UniqSet Name -> Bool
forall a. UniqSet a -> Bool
GHC.isEmptyUniqSet UniqSet Name
ks -> Bool
True
      (_,    _,       _       )                         -> Bool
False

headVar :: Atomic -> Maybe (Int, GHC.Name)
headVar :: Atomic -> Maybe (RVar, Name)
headVar a :: Atomic
a = 
  case Atomic -> K 'R
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Atomic
a of
    Dom (Inj x :: RVar
x d :: Name
d) -> (RVar, Name) -> Maybe (RVar, Name)
forall a. a -> Maybe a
Just (RVar
x, Name
d)
    Set _ _       -> Maybe (RVar, Name)
forall a. Maybe a
Nothing
    _             -> String -> Maybe (RVar, Name)
forall a. HasCallStack => String -> a
error "Not possible!"

bodyVars :: Atomic -> Set (Int, GHC.Name) 
bodyVars :: Atomic -> Set (RVar, Name)
bodyVars a :: Atomic
a = Set (RVar, Name)
gVars Set (RVar, Name) -> Set (RVar, Name) -> Set (RVar, Name)
forall a. Semigroup a => a -> a -> a
<> Set (RVar, Name)
lVars
  where
    gVars :: Set (RVar, Name)
gVars = Guard -> Set (RVar, Name)
Guard.typedVars (Atomic -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Atomic
a)
    lVars :: Set (RVar, Name)
lVars = 
      case Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
a of
        Dom (Inj x :: RVar
x d :: Name
d) -> (RVar, Name) -> Set (RVar, Name)
forall a. a -> Set a
Set.singleton (RVar
x, Name
d)
        Con _ _       -> Set (RVar, Name)
forall a. Set a
Set.empty
        _             -> String -> Set (RVar, Name)
forall a. HasCallStack => String -> a
error "Not possible!"

{-|
    Given two atomic constraints @a@ and @b@, @a `impliedBy` b@ just
    if @a@ and @b@ have the same body and the guard of @a@ is implied
    by the guard of @b@.
-}
impliedBy :: Atomic -> Atomic -> Bool
impliedBy :: Atomic -> Atomic -> Bool
impliedBy a :: Atomic
a a' :: Atomic
a' =
  Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
a K 'L -> K 'L -> Bool
forall a. Eq a => a -> a -> Bool
== Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
a' Bool -> Bool -> Bool
&& Atomic -> K 'R
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Atomic
a K 'R -> K 'R -> Bool
forall a. Eq a => a -> a -> Bool
== Atomic -> K 'R
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Atomic
a' Bool -> Bool -> Bool
&& Atomic -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Atomic
a Guard -> Guard -> Bool
`Guard.impliedBy` Atomic -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Atomic
a'

{-|
    Given an atomic constraint @a@, @tautology a@ just if @a@ is satisfied in 
    every assignment.
-}
tautology :: Atomic -> Bool
tautology :: Atomic -> Bool
tautology a :: Atomic
a =
  case Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
a of
    Dom d :: DataType Name
d ->
      case Atomic -> K 'R
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Atomic
a of
        Dom d' :: DataType Name
d' -> DataType Name
d DataType Name -> DataType Name -> Bool
forall a. Eq a => a -> a -> Bool
== DataType Name
d'
        _ -> Bool
False
    Con k :: Name
k _ ->
      case Atomic -> K 'R
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Atomic
a of
        Dom (Inj x :: RVar
x d :: Name
d) ->
          case RVar -> Name -> Guard -> Maybe (UniqSet Name)
Guard.lookup RVar
x Name
d (Atomic -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Atomic
a) of
            Just ks :: UniqSet Name
ks -> Name -> UniqSet Name -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
GHC.elementOfUniqSet Name
k UniqSet Name
ks
            Nothing -> Bool
False
        Set ks :: UniqSet Name
ks _ -> Name -> UniqSet Name -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
GHC.elementOfUniqSet Name
k UniqSet Name
ks
        _        -> String -> Bool
forall a. HasCallStack => String -> a
error "[ERROR] Unexpected right atom"


{-|
    When @m@ is the current module:
    Given atomic constraints @a@ and @b@, @resolve m a b@ is:

      * @Nothing@ if the resolvant of @a@ and @b@ is a tautology
      * @Just r@ otherwise, where @r@ is the resolvant as an atomic constraint
-}
resolve :: CInfo -> Atomic -> Atomic -> Maybe Atomic
resolve :: CInfo -> Atomic -> Atomic -> Maybe Atomic
resolve ci :: CInfo
ci l :: Atomic
l r :: Atomic
r =
    -- simplify the the new constraint if it's body contains two literals
    case (Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
newR, Atomic -> K 'R
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Atomic
newR) of
      (Con k :: Name
k _, Set ks :: UniqSet Name
ks _) | Name -> UniqSet Name -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
GHC.elementOfUniqSet Name
k UniqSet Name
ks -> Maybe Atomic
forall a. Maybe a
Nothing
      (Con _ _, Set _  s :: SrcSpan
s) | Bool
otherwise                 -> Atomic -> Maybe Atomic
forall a. a -> Maybe a
Just (Atomic
newR { right :: K 'R
right = UniqSet Name -> SrcSpan -> K 'R
Set UniqSet Name
forall a. Monoid a => a
mempty SrcSpan
s})
      (_,       _       )                             -> Atomic -> Maybe Atomic
forall a. a -> Maybe a
Just Atomic
newR
  where
    weaken :: RVar -> Name -> RVar -> Guard -> Maybe Guard
weaken x :: RVar
x d :: Name
d y :: RVar
y g :: Guard
g = 
      -- weaken x(d) in g to y(d)
      case RVar -> Name -> Guard -> Maybe (UniqSet Name)
Guard.lookup RVar
x Name
d Guard
g of
        Just ms :: UniqSet Name
ms | [Name]
ks <- UniqSet Name -> [Name]
forall elt. UniqSet elt -> [elt]
GHC.nonDetEltsUniqSet UniqSet Name
ms -> 
          Guard -> Maybe Guard
forall a. a -> Maybe a
Just ([Name] -> RVar -> Name -> Guard
Guard.singleton [Name]
ks RVar
y Name
d Guard -> Guard -> Guard
forall a. Semigroup a => a -> a -> a
<> [Name] -> RVar -> Name -> Guard -> Guard
Guard.deleteAll [Name]
ks RVar
x Name
d Guard
g)
        Nothing -> Maybe Guard
forall a. Maybe a
Nothing
    satisfy :: RVar -> Name -> Name -> Guard -> Maybe Guard
satisfy x :: RVar
x d :: Name
d k :: Name
k g :: Guard
g =
      -- satisfy x(d) in g by k
      case RVar -> Name -> Guard -> Maybe (UniqSet Name)
Guard.lookup RVar
x Name
d Guard
g of
        Just ks :: UniqSet Name
ks | Name
k Name -> UniqSet Name -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
`GHC.elementOfUniqSet` UniqSet Name
ks -> Guard -> Maybe Guard
forall a. a -> Maybe a
Just (Name -> RVar -> Name -> Guard -> Guard
Guard.delete Name
k RVar
x Name
d Guard
g)
        _                                     -> Maybe Guard
forall a. Maybe a
Nothing
    mbNewGuard :: Maybe Guard
mbNewGuard = 
      -- create a new guard by modifying the old one according to
      -- saturation and weakening (ignoring l's guard, for now)
      case (Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
l, Atomic -> K 'R
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Atomic
l) of 
        (Dom (Inj y :: RVar
y _), Dom (Inj x :: RVar
x d :: Name
d)) -> RVar -> Name -> RVar -> Guard -> Maybe Guard
weaken RVar
x Name
d RVar
y (Atomic -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Atomic
r)
        (Con k :: Name
k _,       Dom (Inj x :: RVar
x d :: Name
d)) -> RVar -> Name -> Name -> Guard -> Maybe Guard
satisfy RVar
x Name
d Name
k (Atomic -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Atomic
r)
        (_,             _            ) -> Maybe Guard
forall a. Maybe a
Nothing
    mbNewLeft :: Maybe (K 'L)
mbNewLeft = 
      -- apply transitivity, or not (ignoring l's guard, for now)
      case (Atomic -> K 'R
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Atomic
l, Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
r) of
        (Dom (Inj x :: RVar
x d :: Name
d), Dom (Inj z :: RVar
z d' :: Name
d')) | RVar
z RVar -> RVar -> Bool
forall a. Eq a => a -> a -> Bool
== RVar
x Bool -> Bool -> Bool
&& Name
d Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
d' -> K 'L -> Maybe (K 'L)
forall a. a -> Maybe a
Just (Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
l)
        (_,             _            )                      -> Maybe (K 'L)
forall a. Maybe a
Nothing
    newR :: Atomic
newR = 
      -- determine whether or not to attach a single copy of l's guards
      case (Maybe Guard
mbNewGuard, Maybe (K 'L)
mbNewLeft) of
      (Just grd :: Guard
grd, Just lft :: K 'L
lft) -> Atomic
r { left :: K 'L
left = K 'L
lft, guard :: Guard
guard = Atomic -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Atomic
l Guard -> Guard -> Guard
forall a. Semigroup a => a -> a -> a
<> Guard
grd, cinfo :: CInfo
cinfo = CInfo
ci }
      (Just grd :: Guard
grd, Nothing ) -> Atomic
r { guard :: Guard
guard = Atomic -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Atomic
l Guard -> Guard -> Guard
forall a. Semigroup a => a -> a -> a
<> Guard
grd, cinfo :: CInfo
cinfo = CInfo
ci }
      (Nothing,  Just lft :: K 'L
lft) -> Atomic
r { left :: K 'L
left = K 'L
lft, guard :: Guard
guard = Atomic -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Atomic
l Guard -> Guard -> Guard
forall a. Semigroup a => a -> a -> a
<> Atomic -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Atomic
r, cinfo :: CInfo
cinfo = CInfo
ci }
      (Nothing,  Nothing ) -> Atomic
r
      
-- We only use ConstraintSetF with Atomic so far, but it is worth making
-- this structure clear to derive Foldable etc
-- TODO: Remove these hashmaps in favour of IntMaps
data ConstraintSetF a
  = ConstraintSetF
      { 
        -- constraints of the form GS ? Y(d) <= Y(d)
        -- represented as X -> (d -> (Y -> GS)) 
        ConstraintSetF a -> IntMap (NameEnv (HashMap RVar [a]))
definiteVV :: IntMap (GHC.NameEnv (HashMap Int [a])),
        -- constraints of the form GS ? k in X(d)
        -- represented as X -> (d -> (k -> GS))
        ConstraintSetF a -> IntMap (NameEnv (HashMap Name [a]))
definiteKV :: IntMap (GHC.NameEnv (HashMap GHC.Name [a])),
        -- constraints of the form G ? S1 <= {k1,...,km}
        -- represented as a list
        ConstraintSetF a -> [a]
goal :: [a],
        -- a reverse lookup to find all those constraints
        -- that have a given sorted variable X(d) in front of
        -- the head (i.e. eligible for saturation on the right)
        ConstraintSetF a -> Map (RVar, Name) [Atomic]
revMap :: Map (Int, GHC.Name) [Atomic]
      }
  deriving (ConstraintSetF a -> ConstraintSetF a -> Bool
(ConstraintSetF a -> ConstraintSetF a -> Bool)
-> (ConstraintSetF a -> ConstraintSetF a -> Bool)
-> Eq (ConstraintSetF a)
forall a. Eq a => ConstraintSetF a -> ConstraintSetF a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConstraintSetF a -> ConstraintSetF a -> Bool
$c/= :: forall a. Eq a => ConstraintSetF a -> ConstraintSetF a -> Bool
== :: ConstraintSetF a -> ConstraintSetF a -> Bool
$c== :: forall a. Eq a => ConstraintSetF a -> ConstraintSetF a -> Bool
Eq, a -> ConstraintSetF b -> ConstraintSetF a
(a -> b) -> ConstraintSetF a -> ConstraintSetF b
(forall a b. (a -> b) -> ConstraintSetF a -> ConstraintSetF b)
-> (forall a b. a -> ConstraintSetF b -> ConstraintSetF a)
-> Functor ConstraintSetF
forall a b. a -> ConstraintSetF b -> ConstraintSetF a
forall a b. (a -> b) -> ConstraintSetF a -> ConstraintSetF b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> ConstraintSetF b -> ConstraintSetF a
$c<$ :: forall a b. a -> ConstraintSetF b -> ConstraintSetF a
fmap :: (a -> b) -> ConstraintSetF a -> ConstraintSetF b
$cfmap :: forall a b. (a -> b) -> ConstraintSetF a -> ConstraintSetF b
Functor, ConstraintSetF a -> Bool
(a -> m) -> ConstraintSetF a -> m
(a -> b -> b) -> b -> ConstraintSetF a -> b
(forall m. Monoid m => ConstraintSetF m -> m)
-> (forall m a. Monoid m => (a -> m) -> ConstraintSetF a -> m)
-> (forall m a. Monoid m => (a -> m) -> ConstraintSetF a -> m)
-> (forall a b. (a -> b -> b) -> b -> ConstraintSetF a -> b)
-> (forall a b. (a -> b -> b) -> b -> ConstraintSetF a -> b)
-> (forall b a. (b -> a -> b) -> b -> ConstraintSetF a -> b)
-> (forall b a. (b -> a -> b) -> b -> ConstraintSetF a -> b)
-> (forall a. (a -> a -> a) -> ConstraintSetF a -> a)
-> (forall a. (a -> a -> a) -> ConstraintSetF a -> a)
-> (forall a. ConstraintSetF a -> [a])
-> (forall a. ConstraintSetF a -> Bool)
-> (forall a. ConstraintSetF a -> RVar)
-> (forall a. Eq a => a -> ConstraintSetF a -> Bool)
-> (forall a. Ord a => ConstraintSetF a -> a)
-> (forall a. Ord a => ConstraintSetF a -> a)
-> (forall a. Num a => ConstraintSetF a -> a)
-> (forall a. Num a => ConstraintSetF a -> a)
-> Foldable ConstraintSetF
forall a. Eq a => a -> ConstraintSetF a -> Bool
forall a. Num a => ConstraintSetF a -> a
forall a. Ord a => ConstraintSetF a -> a
forall m. Monoid m => ConstraintSetF m -> m
forall a. ConstraintSetF a -> Bool
forall a. ConstraintSetF a -> RVar
forall a. ConstraintSetF a -> [a]
forall a. (a -> a -> a) -> ConstraintSetF a -> a
forall m a. Monoid m => (a -> m) -> ConstraintSetF a -> m
forall b a. (b -> a -> b) -> b -> ConstraintSetF a -> b
forall a b. (a -> b -> b) -> b -> ConstraintSetF a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> RVar)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: ConstraintSetF a -> a
$cproduct :: forall a. Num a => ConstraintSetF a -> a
sum :: ConstraintSetF a -> a
$csum :: forall a. Num a => ConstraintSetF a -> a
minimum :: ConstraintSetF a -> a
$cminimum :: forall a. Ord a => ConstraintSetF a -> a
maximum :: ConstraintSetF a -> a
$cmaximum :: forall a. Ord a => ConstraintSetF a -> a
elem :: a -> ConstraintSetF a -> Bool
$celem :: forall a. Eq a => a -> ConstraintSetF a -> Bool
length :: ConstraintSetF a -> RVar
$clength :: forall a. ConstraintSetF a -> RVar
null :: ConstraintSetF a -> Bool
$cnull :: forall a. ConstraintSetF a -> Bool
toList :: ConstraintSetF a -> [a]
$ctoList :: forall a. ConstraintSetF a -> [a]
foldl1 :: (a -> a -> a) -> ConstraintSetF a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> ConstraintSetF a -> a
foldr1 :: (a -> a -> a) -> ConstraintSetF a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> ConstraintSetF a -> a
foldl' :: (b -> a -> b) -> b -> ConstraintSetF a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> ConstraintSetF a -> b
foldl :: (b -> a -> b) -> b -> ConstraintSetF a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> ConstraintSetF a -> b
foldr' :: (a -> b -> b) -> b -> ConstraintSetF a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> ConstraintSetF a -> b
foldr :: (a -> b -> b) -> b -> ConstraintSetF a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> ConstraintSetF a -> b
foldMap' :: (a -> m) -> ConstraintSetF a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> ConstraintSetF a -> m
foldMap :: (a -> m) -> ConstraintSetF a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> ConstraintSetF a -> m
fold :: ConstraintSetF m -> m
$cfold :: forall m. Monoid m => ConstraintSetF m -> m
Foldable)

{-|
    The type of sets of constraints.  
    
    We say that a set of constraints @cs@ is /reduced/ just if, 
    for all X, d, Y, k:
        @definiteVV cs X d Y@, @definiteKV cs X d k@ and @goal cs@
    are non-increasing lists wrt @impliedBy@.

    We say that a set of constraints @cs@ is an /antichain/ just if
    each of these lists are also non-decreasing.

    Most sets of constraints we process are reduced, but we allow
    non-reduced constraint sets to occur as a consequence of renaming
    of variables.

    Many sets of constraints are also antichains, 
    for example, when filtering a reduced constraint set one can
    guarantee the new constraint set will be an antichain by using
    @insert@  and constructing the new constraint set in the 
    reverse order. Constraint sets returned from saturation will 
    always be antichains.
-}
type ConstraintSet = ConstraintSetF Atomic

instance Foldable GHC.UniqFM where
  foldr :: (a -> b -> b) -> b -> UniqFM a -> b
foldr = (a -> b -> b) -> b -> UniqFM a -> b
forall a b. (a -> b -> b) -> b -> UniqFM a -> b
GHC.foldUFM 

{-|
    Given a list of atomic constraints @cs@, @fromList cs@ is
    largest antichain contained in @cs@
-}
fromList :: [Atomic] -> ConstraintSet
fromList :: [Atomic] -> ConstraintSet
fromList = (Atomic -> ConstraintSet -> ConstraintSet)
-> ConstraintSet -> [Atomic] -> ConstraintSet
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Atomic -> ConstraintSet -> ConstraintSet
insert ConstraintSet
empty

instance Semigroup ConstraintSet where
  cs :: ConstraintSet
cs <> :: ConstraintSet -> ConstraintSet -> ConstraintSet
<> ds :: ConstraintSet
ds = (Atomic -> ConstraintSet -> ConstraintSet)
-> ConstraintSet -> ConstraintSet -> ConstraintSet
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Atomic -> ConstraintSet -> ConstraintSet
insert ConstraintSet
ds ConstraintSet
cs

instance Monoid ConstraintSet where
  mempty :: ConstraintSet
mempty = ConstraintSet
empty

instance GHC.Outputable ConstraintSet where
  ppr :: ConstraintSet -> SDoc
ppr = (RVar -> SDoc) -> ConstraintSet -> SDoc
forall t. Refined t => (RVar -> SDoc) -> t -> SDoc
prpr RVar -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr

instance Binary ConstraintSet where
  put_ :: BinHandle -> ConstraintSet -> IO ()
put_ bh :: BinHandle
bh = BinHandle -> [Atomic] -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh ([Atomic] -> IO ())
-> (ConstraintSet -> [Atomic]) -> ConstraintSet -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintSet -> [Atomic]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
  get :: BinHandle -> IO ConstraintSet
get bh :: BinHandle
bh = [Atomic] -> ConstraintSet
fromList ([Atomic] -> ConstraintSet) -> IO [Atomic] -> IO ConstraintSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO [Atomic]
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh

instance Refined ConstraintSet where
  domain :: ConstraintSet -> Domain
domain = (Atomic -> Domain) -> ConstraintSet -> Domain
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Atomic -> Domain
forall t. Refined t => t -> Domain
domain
  rename :: RVar -> RVar -> ConstraintSet -> ConstraintSet
rename x :: RVar
x y :: RVar
y = 
    -- this may create non-reduced constraint sets
    (ConstraintSet -> Atomic -> ConstraintSet)
-> ConstraintSet -> ConstraintSet -> ConstraintSet
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ds :: ConstraintSet
ds a :: Atomic
a -> Atomic -> ConstraintSet -> ConstraintSet
unsafeInsert (RVar -> RVar -> Atomic -> Atomic
forall t. Refined t => RVar -> RVar -> t -> t
rename RVar
x RVar
y Atomic
a) ConstraintSet
ds) ConstraintSet
empty
  prpr :: (RVar -> SDoc) -> ConstraintSet -> SDoc
prpr m :: RVar -> SDoc
m = (Atomic -> SDoc -> SDoc) -> SDoc -> ConstraintSet -> SDoc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SDoc -> SDoc -> SDoc
(GHC.$$) (SDoc -> SDoc -> SDoc)
-> (Atomic -> SDoc) -> Atomic -> SDoc -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RVar -> SDoc) -> Atomic -> SDoc
forall t. Refined t => (RVar -> SDoc) -> t -> SDoc
prpr RVar -> SDoc
m) SDoc
GHC.empty


{-|
    @empty@ is the empty constraint set
-}
empty :: ConstraintSet
empty :: ConstraintSet
empty =
  ConstraintSetF :: forall a.
IntMap (NameEnv (HashMap RVar [a]))
-> IntMap (NameEnv (HashMap Name [a]))
-> [a]
-> Map (RVar, Name) [Atomic]
-> ConstraintSetF a
ConstraintSetF
    { 
      definiteVV :: IntMap (NameEnv (HashMap RVar [Atomic]))
definiteVV = IntMap (NameEnv (HashMap RVar [Atomic]))
forall a. Monoid a => a
mempty,
      definiteKV :: IntMap (NameEnv (HashMap Name [Atomic]))
definiteKV = IntMap (NameEnv (HashMap Name [Atomic]))
forall a. Monoid a => a
mempty,
      goal :: [Atomic]
goal = [],
      revMap :: Map (RVar, Name) [Atomic]
revMap = Map (RVar, Name) [Atomic]
forall a. Monoid a => a
mempty
    }

{-|
    Given a constraint set @cs@, @unsats cs@ is the constraint set 
    consisting of just those trivially unsatisfiable constraints in @cs@.
-}
unsats :: ConstraintSet -> ConstraintSet
unsats :: ConstraintSet -> ConstraintSet
unsats cs :: ConstraintSet
cs = 
  ConstraintSet
forall a. Monoid a => a
mempty { goal :: [Atomic]
goal = (Atomic -> Bool) -> [Atomic] -> [Atomic]
forall a. (a -> Bool) -> [a] -> [a]
filter Atomic -> Bool
isTriviallyUnsat (ConstraintSet -> [Atomic]
forall a. ConstraintSetF a -> [a]
goal ConstraintSet
cs) }

{-| 
    When @cs@ is a constraint set, @size cs@ is its cardinality.
-}
size :: ConstraintSet -> Int
size :: ConstraintSet -> RVar
size = (RVar -> Atomic -> RVar) -> RVar -> ConstraintSet -> RVar
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\sz :: RVar
sz _ -> 1 RVar -> RVar -> RVar
forall a. Num a => a -> a -> a
+ RVar
sz) 0

{-| 
    When @a@ is an atomic constraint and @cs@ a constraint set,
    @unsafeInsert a cs@ is the constraint set obtained by inserting
    @a@ into @cs@.  
    
    Note: @unsafeInsert a cs@ may not be reduced even if @cs@ is.
-}
unsafeInsert :: Atomic -> ConstraintSet -> ConstraintSet
unsafeInsert :: Atomic -> ConstraintSet -> ConstraintSet
unsafeInsert a :: Atomic
a cs :: ConstraintSet
cs =
    ConstraintSet
fwd { revMap :: Map (RVar, Name) [Atomic]
revMap = (Map (RVar, Name) [Atomic]
 -> (RVar, Name) -> Map (RVar, Name) [Atomic])
-> Map (RVar, Name) [Atomic]
-> Set (RVar, Name)
-> Map (RVar, Name) [Atomic]
forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl' (\m :: Map (RVar, Name) [Atomic]
m (x :: RVar
x,d :: Name
d) -> ([Atomic] -> [Atomic] -> [Atomic])
-> (RVar, Name)
-> [Atomic]
-> Map (RVar, Name) [Atomic]
-> Map (RVar, Name) [Atomic]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [Atomic] -> [Atomic] -> [Atomic]
forall a. [a] -> [a] -> [a]
(++) (RVar
x,Name
d) [Atomic
a] Map (RVar, Name) [Atomic]
m) (ConstraintSet -> Map (RVar, Name) [Atomic]
forall a. ConstraintSetF a -> Map (RVar, Name) [Atomic]
revMap ConstraintSet
fwd) (Atomic -> Set (RVar, Name)
bodyVars Atomic
a) }
  where
    fwd :: ConstraintSet
fwd = 
      case (Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
a, Atomic -> K 'R
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Atomic
a) of
        (Dom (Inj x :: RVar
x _), Dom (Inj y :: RVar
y yd :: Name
yd)) ->
          let ne :: NameEnv (HashMap RVar [Atomic])
ne = NameEnv (HashMap RVar [Atomic])
-> RVar
-> IntMap (NameEnv (HashMap RVar [Atomic]))
-> NameEnv (HashMap RVar [Atomic])
forall a. a -> RVar -> IntMap a -> a
IntMap.findWithDefault NameEnv (HashMap RVar [Atomic])
forall a. Monoid a => a
mempty RVar
y (ConstraintSet -> IntMap (NameEnv (HashMap RVar [Atomic]))
forall a. ConstraintSetF a -> IntMap (NameEnv (HashMap RVar [a]))
definiteVV ConstraintSet
cs)
              hm :: HashMap RVar [Atomic]
hm = NameEnv (HashMap RVar [Atomic])
-> HashMap RVar [Atomic] -> Name -> HashMap RVar [Atomic]
forall key elt. Uniquable key => UniqFM elt -> elt -> key -> elt
GHC.lookupWithDefaultUFM NameEnv (HashMap RVar [Atomic])
ne HashMap RVar [Atomic]
forall a. Monoid a => a
mempty Name
yd
              as :: [Atomic]
as = [Atomic] -> RVar -> HashMap RVar [Atomic] -> [Atomic]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
HashMap.findWithDefault [] RVar
x HashMap RVar [Atomic]
hm
          in ConstraintSet
cs {definiteVV :: IntMap (NameEnv (HashMap RVar [Atomic]))
definiteVV = RVar
-> NameEnv (HashMap RVar [Atomic])
-> IntMap (NameEnv (HashMap RVar [Atomic]))
-> IntMap (NameEnv (HashMap RVar [Atomic]))
forall a. RVar -> a -> IntMap a -> IntMap a
IntMap.insert RVar
y (NameEnv (HashMap RVar [Atomic])
-> Name -> HashMap RVar [Atomic] -> NameEnv (HashMap RVar [Atomic])
forall key elt.
Uniquable key =>
UniqFM elt -> key -> elt -> UniqFM elt
GHC.addToUFM NameEnv (HashMap RVar [Atomic])
ne Name
yd (RVar -> [Atomic] -> HashMap RVar [Atomic] -> HashMap RVar [Atomic]
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HashMap.insert RVar
x (Atomic
a Atomic -> [Atomic] -> [Atomic]
forall a. a -> [a] -> [a]
: [Atomic]
as) HashMap RVar [Atomic]
hm)) (ConstraintSet -> IntMap (NameEnv (HashMap RVar [Atomic]))
forall a. ConstraintSetF a -> IntMap (NameEnv (HashMap RVar [a]))
definiteVV ConstraintSet
cs)}
        (Con k :: Name
k _, Dom (Inj y :: RVar
y yd :: Name
yd)) ->
          let ne :: NameEnv (HashMap Name [Atomic])
ne = NameEnv (HashMap Name [Atomic])
-> RVar
-> IntMap (NameEnv (HashMap Name [Atomic]))
-> NameEnv (HashMap Name [Atomic])
forall a. a -> RVar -> IntMap a -> a
IntMap.findWithDefault NameEnv (HashMap Name [Atomic])
forall a. Monoid a => a
mempty RVar
y (ConstraintSet -> IntMap (NameEnv (HashMap Name [Atomic]))
forall a. ConstraintSetF a -> IntMap (NameEnv (HashMap Name [a]))
definiteKV ConstraintSet
cs)
              hm :: HashMap Name [Atomic]
hm = NameEnv (HashMap Name [Atomic])
-> HashMap Name [Atomic] -> Name -> HashMap Name [Atomic]
forall key elt. Uniquable key => UniqFM elt -> elt -> key -> elt
GHC.lookupWithDefaultUFM NameEnv (HashMap Name [Atomic])
ne HashMap Name [Atomic]
forall a. Monoid a => a
mempty Name
yd
              as :: [Atomic]
as = [Atomic] -> Name -> HashMap Name [Atomic] -> [Atomic]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
HashMap.findWithDefault [] Name
k HashMap Name [Atomic]
hm
          in ConstraintSet
cs {definiteKV :: IntMap (NameEnv (HashMap Name [Atomic]))
definiteKV = RVar
-> NameEnv (HashMap Name [Atomic])
-> IntMap (NameEnv (HashMap Name [Atomic]))
-> IntMap (NameEnv (HashMap Name [Atomic]))
forall a. RVar -> a -> IntMap a -> IntMap a
IntMap.insert RVar
y (NameEnv (HashMap Name [Atomic])
-> Name -> HashMap Name [Atomic] -> NameEnv (HashMap Name [Atomic])
forall key elt.
Uniquable key =>
UniqFM elt -> key -> elt -> UniqFM elt
GHC.addToUFM NameEnv (HashMap Name [Atomic])
ne Name
yd (Name -> [Atomic] -> HashMap Name [Atomic] -> HashMap Name [Atomic]
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HashMap.insert Name
k (Atomic
a Atomic -> [Atomic] -> [Atomic]
forall a. a -> [a] -> [a]
: [Atomic]
as) HashMap Name [Atomic]
hm)) (ConstraintSet -> IntMap (NameEnv (HashMap Name [Atomic]))
forall a. ConstraintSetF a -> IntMap (NameEnv (HashMap Name [a]))
definiteKV ConstraintSet
cs)}
        (_, Set _ _) -> ConstraintSet
cs {goal :: [Atomic]
goal = Atomic
a Atomic -> [Atomic] -> [Atomic]
forall a. a -> [a] -> [a]
: ConstraintSet -> [Atomic]
forall a. ConstraintSetF a -> [a]
goal ConstraintSet
cs}
        (_, _) -> ConstraintSet
cs

{-| 
    When @a@ is an atomic constraint and @cs@ is a constraint antichain 
    @insert a cs@ is: 
    
      * @Nothing@ just if @a@ is already implied by some constraint in @cs@.
      * @Just ds@ otherwise, where @ds@ is the constraint antichain obtained 
        by inserting @a@ into @cs@. Note: @ds@ may be smaller than @cs@.
-}
insert' :: Atomic -> ConstraintSet -> Maybe ConstraintSet
insert' :: Atomic -> ConstraintSet -> Maybe ConstraintSet
insert' a :: Atomic
a cs :: ConstraintSet
cs | Bool -> Bool
not (Atomic -> Bool
tautology Atomic
a) =
    case Maybe ConstraintSet
mbFwd of
      Just fwd :: ConstraintSet
fwd -> ConstraintSet -> Maybe ConstraintSet
forall a. a -> Maybe a
Just (ConstraintSet -> Maybe ConstraintSet)
-> ConstraintSet -> Maybe ConstraintSet
forall a b. (a -> b) -> a -> b
$ ConstraintSet
fwd { revMap :: Map (RVar, Name) [Atomic]
revMap = (Map (RVar, Name) [Atomic]
 -> (RVar, Name) -> Map (RVar, Name) [Atomic])
-> Map (RVar, Name) [Atomic]
-> Set (RVar, Name)
-> Map (RVar, Name) [Atomic]
forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl' (\m :: Map (RVar, Name) [Atomic]
m (x :: RVar
x,d :: Name
d) -> ([Atomic] -> [Atomic] -> [Atomic])
-> (RVar, Name)
-> [Atomic]
-> Map (RVar, Name) [Atomic]
-> Map (RVar, Name) [Atomic]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [Atomic] -> [Atomic] -> [Atomic]
forall a. [a] -> [a] -> [a]
(++) (RVar
x,Name
d) [Atomic
a] Map (RVar, Name) [Atomic]
m) (ConstraintSet -> Map (RVar, Name) [Atomic]
forall a. ConstraintSetF a -> Map (RVar, Name) [Atomic]
revMap ConstraintSet
fwd) (Atomic -> Set (RVar, Name)
bodyVars Atomic
a) }
      Nothing -> Maybe ConstraintSet
forall a. Maybe a
Nothing
  where
    mbFwd :: Maybe ConstraintSet
mbFwd = 
      case (Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
a, Atomic -> K 'R
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Atomic
a) of
        (Dom (Inj x :: RVar
x _), Dom (Inj y :: RVar
y yd :: Name
yd)) ->
          let ne :: NameEnv (HashMap RVar [Atomic])
ne = NameEnv (HashMap RVar [Atomic])
-> RVar
-> IntMap (NameEnv (HashMap RVar [Atomic]))
-> NameEnv (HashMap RVar [Atomic])
forall a. a -> RVar -> IntMap a -> a
IntMap.findWithDefault NameEnv (HashMap RVar [Atomic])
forall a. Monoid a => a
mempty RVar
y (ConstraintSet -> IntMap (NameEnv (HashMap RVar [Atomic]))
forall a. ConstraintSetF a -> IntMap (NameEnv (HashMap RVar [a]))
definiteVV ConstraintSet
cs)
              hm :: HashMap RVar [Atomic]
hm = NameEnv (HashMap RVar [Atomic])
-> HashMap RVar [Atomic] -> Name -> HashMap RVar [Atomic]
forall key elt. Uniquable key => UniqFM elt -> elt -> key -> elt
GHC.lookupWithDefaultUFM NameEnv (HashMap RVar [Atomic])
ne HashMap RVar [Atomic]
forall a. Monoid a => a
mempty Name
yd
              as :: [Atomic]
as = [Atomic] -> RVar -> HashMap RVar [Atomic] -> [Atomic]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
HashMap.findWithDefault [] RVar
x HashMap RVar [Atomic]
hm
          in ([Atomic] -> ConstraintSet)
-> Maybe [Atomic] -> Maybe ConstraintSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\as' :: [Atomic]
as' -> ConstraintSet
cs {definiteVV :: IntMap (NameEnv (HashMap RVar [Atomic]))
definiteVV = RVar
-> NameEnv (HashMap RVar [Atomic])
-> IntMap (NameEnv (HashMap RVar [Atomic]))
-> IntMap (NameEnv (HashMap RVar [Atomic]))
forall a. RVar -> a -> IntMap a -> IntMap a
IntMap.insert RVar
y (NameEnv (HashMap RVar [Atomic])
-> Name -> HashMap RVar [Atomic] -> NameEnv (HashMap RVar [Atomic])
forall key elt.
Uniquable key =>
UniqFM elt -> key -> elt -> UniqFM elt
GHC.addToUFM NameEnv (HashMap RVar [Atomic])
ne Name
yd (RVar -> [Atomic] -> HashMap RVar [Atomic] -> HashMap RVar [Atomic]
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HashMap.insert RVar
x [Atomic]
as' HashMap RVar [Atomic]
hm)) (ConstraintSet -> IntMap (NameEnv (HashMap RVar [Atomic]))
forall a. ConstraintSetF a -> IntMap (NameEnv (HashMap RVar [a]))
definiteVV ConstraintSet
cs)}) ([Atomic] -> Maybe [Atomic]
maintain [Atomic]
as)
        (Con k :: Name
k _, Dom (Inj y :: RVar
y yd :: Name
yd)) ->
          let ne :: NameEnv (HashMap Name [Atomic])
ne = NameEnv (HashMap Name [Atomic])
-> RVar
-> IntMap (NameEnv (HashMap Name [Atomic]))
-> NameEnv (HashMap Name [Atomic])
forall a. a -> RVar -> IntMap a -> a
IntMap.findWithDefault NameEnv (HashMap Name [Atomic])
forall a. Monoid a => a
mempty RVar
y (ConstraintSet -> IntMap (NameEnv (HashMap Name [Atomic]))
forall a. ConstraintSetF a -> IntMap (NameEnv (HashMap Name [a]))
definiteKV ConstraintSet
cs)
              hm :: HashMap Name [Atomic]
hm = NameEnv (HashMap Name [Atomic])
-> HashMap Name [Atomic] -> Name -> HashMap Name [Atomic]
forall key elt. Uniquable key => UniqFM elt -> elt -> key -> elt
GHC.lookupWithDefaultUFM NameEnv (HashMap Name [Atomic])
ne HashMap Name [Atomic]
forall a. Monoid a => a
mempty Name
yd
              as :: [Atomic]
as = [Atomic] -> Name -> HashMap Name [Atomic] -> [Atomic]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
HashMap.findWithDefault [] Name
k HashMap Name [Atomic]
hm
          in ([Atomic] -> ConstraintSet)
-> Maybe [Atomic] -> Maybe ConstraintSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\as' :: [Atomic]
as' -> ConstraintSet
cs {definiteKV :: IntMap (NameEnv (HashMap Name [Atomic]))
definiteKV = RVar
-> NameEnv (HashMap Name [Atomic])
-> IntMap (NameEnv (HashMap Name [Atomic]))
-> IntMap (NameEnv (HashMap Name [Atomic]))
forall a. RVar -> a -> IntMap a -> IntMap a
IntMap.insert RVar
y (NameEnv (HashMap Name [Atomic])
-> Name -> HashMap Name [Atomic] -> NameEnv (HashMap Name [Atomic])
forall key elt.
Uniquable key =>
UniqFM elt -> key -> elt -> UniqFM elt
GHC.addToUFM NameEnv (HashMap Name [Atomic])
ne Name
yd (Name -> [Atomic] -> HashMap Name [Atomic] -> HashMap Name [Atomic]
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HashMap.insert Name
k [Atomic]
as' HashMap Name [Atomic]
hm)) (ConstraintSet -> IntMap (NameEnv (HashMap Name [Atomic]))
forall a. ConstraintSetF a -> IntMap (NameEnv (HashMap Name [a]))
definiteKV ConstraintSet
cs)}) ([Atomic] -> Maybe [Atomic]
maintain [Atomic]
as)
        (_, Set _ _) ->
          ([Atomic] -> ConstraintSet)
-> Maybe [Atomic] -> Maybe ConstraintSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\as' :: [Atomic]
as' -> ConstraintSet
cs {goal :: [Atomic]
goal = [Atomic]
as'}) ([Atomic] -> Maybe [Atomic]
maintain (ConstraintSet -> [Atomic]
forall a. ConstraintSetF a -> [a]
goal ConstraintSet
cs))
        (_, _) -> Maybe ConstraintSet
forall a. Maybe a
Nothing -- Ignore constraints concerning base types
    maintain :: [Atomic] -> Maybe [Atomic]
maintain ds :: [Atomic]
ds =
      if (Atomic -> Bool) -> [Atomic] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Atomic
a Atomic -> Atomic -> Bool
`impliedBy`) [Atomic]
ds then Maybe [Atomic]
forall a. Maybe a
Nothing else [Atomic] -> Maybe [Atomic]
forall a. a -> Maybe a
Just (Atomic
a Atomic -> [Atomic] -> [Atomic]
forall a. a -> [a] -> [a]
: [Atomic]
ds)
insert' _ _ = Maybe ConstraintSet
forall a. Maybe a
Nothing

{-| 
    When @a@ is an atomic constraint and @cs@ is a constraint set
    @insert a cs@ is the constraint set obtained by inserting @a@
    into @cs@.

    If @cs@ is reduced then so is @insert a cs@.  However, @insert a cs@ 
    may not be an antichain even when @cs@ is.
-}
insert :: Atomic -> ConstraintSet -> ConstraintSet
insert :: Atomic -> ConstraintSet -> ConstraintSet
insert a :: Atomic
a cs :: ConstraintSet
cs = ConstraintSet -> Maybe ConstraintSet -> ConstraintSet
forall a. a -> Maybe a -> a
Maybe.fromMaybe ConstraintSet
cs (Atomic -> ConstraintSet -> Maybe ConstraintSet
insert' Atomic
a ConstraintSet
cs)

{-|
    When @g@ is a guard and @cs@ a set of constraints, @guardWith g cs@ is 
    the set of constraints obtained from @cs@ by appending @g@ to every guard
    of every constraint.
-}
guardWith :: Guard -> ConstraintSet -> ConstraintSet
guardWith :: Guard -> ConstraintSet -> ConstraintSet
guardWith g :: Guard
g =
  (ConstraintSet -> Atomic -> ConstraintSet)
-> ConstraintSet -> ConstraintSet -> ConstraintSet
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ds :: ConstraintSet
ds a :: Atomic
a -> Atomic -> ConstraintSet -> ConstraintSet
insert (Atomic
a { guard :: Guard
guard = Guard
g Guard -> Guard -> Guard
forall a. Semigroup a => a -> a -> a
<> Atomic -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Atomic
a }) ConstraintSet
ds) ConstraintSet
forall a. Monoid a => a
mempty

{-|
    When @iface@ is a set of interface variables and @ci@ is the current ctx 
    and @cs@ is a constraint set, @saturate ci iface cs@ is the constraint set 
    obtained from @cs@ by saturation and restriction to @iface@.
-}
saturate :: CInfo -> IntSet -> ConstraintSet -> ConstraintSet
saturate :: CInfo -> Domain -> ConstraintSet -> ConstraintSet
saturate ci :: CInfo
ci iface :: Domain
iface cs :: ConstraintSet
cs  = 
    ConstraintSet
es
  where
    ls :: ConstraintSet
ls = (ConstraintSet -> Atomic -> ConstraintSet)
-> ConstraintSet -> ConstraintSet -> ConstraintSet
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ms :: ConstraintSet
ms c :: Atomic
c -> if Domain -> Atomic -> Bool
eligible Domain
iface Atomic
c then Atomic -> ConstraintSet -> ConstraintSet
unsafeInsert Atomic
c ConstraintSet
ms else ConstraintSet
ms) ConstraintSet
forall a. Monoid a => a
mempty ConstraintSet
cs
    ds :: ConstraintSet
ds = (ConstraintSet, ConstraintSet) -> ConstraintSet
forall a b. (a, b) -> b
snd ((ConstraintSet, ConstraintSet) -> ConstraintSet)
-> (ConstraintSet, ConstraintSet) -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ State (ConstraintSet, ConstraintSet) ()
-> (ConstraintSet, ConstraintSet) -> (ConstraintSet, ConstraintSet)
forall s a. State s a -> s -> s
State.execState (CInfo -> Domain -> State (ConstraintSet, ConstraintSet) ()
fix CInfo
ci Domain
iface) (ConstraintSet
ls, ConstraintSet
cs)
    -- doing foldl with insert here will guarantee the result is an antichain
    es :: ConstraintSet
es = (ConstraintSet -> Atomic -> ConstraintSet)
-> ConstraintSet -> ConstraintSet -> ConstraintSet
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\fs :: ConstraintSet
fs a :: Atomic
a -> if Atomic -> Domain
forall t. Refined t => t -> Domain
domain Atomic
a Domain -> Domain -> Bool
`IntSet.isSubsetOf` Domain
iface then Atomic -> ConstraintSet -> ConstraintSet
insert Atomic
a ConstraintSet
fs else ConstraintSet
fs) ConstraintSet
forall a. Monoid a => a
mempty ConstraintSet
ds


{-|
    Given a set of interface variables @exts@ and a constraint @c@,
    @eligible exts c@ just if there are no interface variables in the
    head of @c@ and only interface variables elsewhere in @c@.

    (This means it is eligible to be used as the left-constraint in a
    resolution step.)
-}
eligible :: IntSet -> Atomic -> Bool
eligible :: Domain -> Atomic -> Bool
eligible exts :: Domain
exts c :: Atomic
c = 
      Guard -> Domain
forall t. Refined t => t -> Domain
domain (Atomic -> Guard
forall (l :: Side) (r :: Side). Constraint l r -> Guard
guard Atomic
c) Domain -> Domain -> Bool
`IntSet.isSubsetOf` Domain
exts  
        Bool -> Bool -> Bool
&& K 'L -> Domain
forall t. Refined t => t -> Domain
domain (Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
c) Domain -> Domain -> Bool
`IntSet.isSubsetOf` Domain
exts
        Bool -> Bool -> Bool
&& Bool -> Bool
not (K 'R -> Domain
forall t. Refined t => t -> Domain
domain (Atomic -> K 'R
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Atomic
c) Domain -> Domain -> Bool
`IntSet.isSubsetOf` Domain
exts)

{-|
    Given some context @ci@ and constraints @cs@ attempt to build
    a model of @cs@.  @cexs ci cs@ is the set of 
    trivially unsatisfiable constrants obtained from the candidate model.
-}
cexs :: CInfo -> ConstraintSet -> ConstraintSet 
cexs :: CInfo -> ConstraintSet -> ConstraintSet
cexs ci :: CInfo
ci = CInfo -> Domain -> ConstraintSet -> ConstraintSet
saturate CInfo
ci Domain
forall a. Monoid a => a
mempty

{-| 
    When @exts@ is the set of interface variables and @ci@ is the current 
    ctx @fix ci exts@ is the stateful computation that transforms an 
    initial state @(ls, rs)@ where @ls@ are all unit constraints modulo 
    @exts@ and @ls@ is contained in @rs@, into a final state @(ls', rs')@ 
    in which @ls@ is empty and @rs'@ is the saturation of @rs@.
-}
fix :: CInfo -> IntSet -> State (ConstraintSet, ConstraintSet) ()
fix :: CInfo -> Domain -> State (ConstraintSet, ConstraintSet) ()
fix ci :: CInfo
ci exts :: Domain
exts =
  do  (ls :: ConstraintSet
ls, rs :: ConstraintSet
rs) <- StateT
  (ConstraintSet, ConstraintSet)
  Identity
  (ConstraintSet, ConstraintSet)
forall s (m :: * -> *). MonadState s m => m s
State.get
      Bool
-> State (ConstraintSet, ConstraintSet) ()
-> State (ConstraintSet, ConstraintSet) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
Monad.when Bool
debugging (State (ConstraintSet, ConstraintSet) ()
 -> State (ConstraintSet, ConstraintSet) ())
-> State (ConstraintSet, ConstraintSet) ()
-> State (ConstraintSet, ConstraintSet) ()
forall a b. (a -> b) -> a -> b
$ 
        String -> State (ConstraintSet, ConstraintSet) ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("#ls = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RVar -> String
forall a. Show a => a -> String
show (ConstraintSet -> RVar
size ConstraintSet
ls) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ", #rs = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RVar -> String
forall a. Show a => a -> String
show (ConstraintSet -> RVar
size ConstraintSet
rs))
      Bool
-> State (ConstraintSet, ConstraintSet) ()
-> State (ConstraintSet, ConstraintSet) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
Monad.unless (ConstraintSet -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ConstraintSet
ls) (State (ConstraintSet, ConstraintSet) ()
 -> State (ConstraintSet, ConstraintSet) ())
-> State (ConstraintSet, ConstraintSet) ()
-> State (ConstraintSet, ConstraintSet) ()
forall a b. (a -> b) -> a -> b
$ CInfo -> Domain -> State (ConstraintSet, ConstraintSet) ()
saturate1 CInfo
ci Domain
exts State (ConstraintSet, ConstraintSet) ()
-> State (ConstraintSet, ConstraintSet) ()
-> State (ConstraintSet, ConstraintSet) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CInfo -> Domain -> State (ConstraintSet, ConstraintSet) ()
fix CInfo
ci Domain
exts

{-| 
     When @exts@ is a set of interface variables and @ci@ is the current ctx
     @saturate1 ci exts@ is the stateful computation that takes an initial state 
     @(ls, rs)@ consisting of a pair of constraint sets with @ls@ being unit 
     clauses modulo `exts` and @ls@ being contained in @rs@ to a final state 
     @(ls', rs')@ in which:

       *  @ls'@ is those constraints in @rs'@ that are not in @rs@ and which 
          are unit modulo @exts@.
       *  @rs'@ contains all the constraints obtained from @rs@ by resolving 
          on the left with each clauses from @ls@ once.
-}
saturate1 :: CInfo -> IntSet -> State (ConstraintSet, ConstraintSet) ()
saturate1 :: CInfo -> Domain -> State (ConstraintSet, ConstraintSet) ()
saturate1 ci :: CInfo
ci exts :: Domain
exts =
    do  (ls :: ConstraintSet
ls, rs :: ConstraintSet
rs) <- StateT
  (ConstraintSet, ConstraintSet)
  Identity
  (ConstraintSet, ConstraintSet)
forall s (m :: * -> *). MonadState s m => m s
State.get
        (ConstraintSet, ConstraintSet)
-> State (ConstraintSet, ConstraintSet) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
State.put (ConstraintSet
forall a. Monoid a => a
mempty, ConstraintSet
rs)
        ConstraintSet
-> (Atomic -> State (ConstraintSet, ConstraintSet) ())
-> State (ConstraintSet, ConstraintSet) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
Monad.forM_ ConstraintSet
ls ((Atomic -> State (ConstraintSet, ConstraintSet) ())
 -> State (ConstraintSet, ConstraintSet) ())
-> (Atomic -> State (ConstraintSet, ConstraintSet) ())
-> State (ConstraintSet, ConstraintSet) ()
forall a b. (a -> b) -> a -> b
$ \l :: Atomic
l ->
          do  -- We immediately get the current state to allow
              -- for two left constraints to be applied to the
              -- same right constraint
              ConstraintSet
rs' <- ((ConstraintSet, ConstraintSet) -> ConstraintSet)
-> StateT (ConstraintSet, ConstraintSet) Identity ConstraintSet
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
State.gets (ConstraintSet, ConstraintSet) -> ConstraintSet
forall a b. (a, b) -> b
snd
              -- This is guaranteed by varsAllExts
              case Atomic -> Maybe (RVar, Name)
headVar Atomic
l of
                Nothing -> String -> State (ConstraintSet, ConstraintSet) ()
forall a. HasCallStack => String -> a
error "impossible"
                Just (x :: RVar
x,d :: Name
d) -> 
                  [Atomic]
-> (Atomic -> State (ConstraintSet, ConstraintSet) ())
-> State (ConstraintSet, ConstraintSet) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
Monad.forM_ ([Atomic] -> (RVar, Name) -> Map (RVar, Name) [Atomic] -> [Atomic]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] (RVar
x,Name
d) (Map (RVar, Name) [Atomic] -> [Atomic])
-> Map (RVar, Name) [Atomic] -> [Atomic]
forall a b. (a -> b) -> a -> b
$ ConstraintSet -> Map (RVar, Name) [Atomic]
forall a. ConstraintSetF a -> Map (RVar, Name) [Atomic]
revMap ConstraintSet
rs') ((Atomic -> State (ConstraintSet, ConstraintSet) ())
 -> State (ConstraintSet, ConstraintSet) ())
-> (Atomic -> State (ConstraintSet, ConstraintSet) ())
-> State (ConstraintSet, ConstraintSet) ()
forall a b. (a -> b) -> a -> b
$ \r :: Atomic
r -> 
                      Maybe Atomic -> State (ConstraintSet, ConstraintSet) ()
addResolvant (CInfo -> Atomic -> Atomic -> Maybe Atomic
resolve CInfo
ci Atomic
l Atomic
r)
  where
    addResolvant :: Maybe Atomic -> State (ConstraintSet, ConstraintSet) ()
addResolvant Nothing  = () -> State (ConstraintSet, ConstraintSet) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    addResolvant (Just r :: Atomic
r) =
      do  (ls :: ConstraintSet
ls, rs :: ConstraintSet
rs) <- StateT
  (ConstraintSet, ConstraintSet)
  Identity
  (ConstraintSet, ConstraintSet)
forall s (m :: * -> *). MonadState s m => m s
State.get
          case Atomic -> ConstraintSet -> Maybe ConstraintSet
insert' Atomic
r ConstraintSet
rs of
            Nothing -> () -> State (ConstraintSet, ConstraintSet) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just rs' :: ConstraintSet
rs' -> 
              -- Insert the new constraint into ls only if it is a 
              -- unit clause modulo externals.
              (ConstraintSet, ConstraintSet)
-> State (ConstraintSet, ConstraintSet) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
State.put (if Domain -> Atomic -> Bool
eligible Domain
exts Atomic
r then Atomic -> ConstraintSet -> ConstraintSet
insert Atomic
r ConstraintSet
ls else ConstraintSet
ls, ConstraintSet
rs')