{-# OPTIONS_HADDOCK ignore-exports #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
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
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)
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
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
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!"
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'
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"
resolve :: CInfo -> Atomic -> Atomic -> Maybe Atomic
resolve :: CInfo -> Atomic -> Atomic -> Maybe Atomic
resolve ci :: CInfo
ci l :: Atomic
l r :: Atomic
r =
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 =
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 =
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 =
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 =
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 =
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
data ConstraintSetF a
= ConstraintSetF
{
ConstraintSetF a -> IntMap (NameEnv (HashMap RVar [a]))
definiteVV :: IntMap (GHC.NameEnv (HashMap Int [a])),
ConstraintSetF a -> IntMap (NameEnv (HashMap Name [a]))
definiteKV :: IntMap (GHC.NameEnv (HashMap GHC.Name [a])),
ConstraintSetF a -> [a]
goal :: [a],
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)
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
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 =
(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 :: 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
}
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) }
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
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
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
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
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)
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
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)
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
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)
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
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
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
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
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' ->
(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')