{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses #-}
module Idris.Core.Constraints ( ucheck ) where
import Idris.Core.TT (ConstraintFC(..), Err'(..), TC(..), UConstraint(..),
UExp(..))
import Control.Monad.State.Strict
import Data.List (partition)
import qualified Data.Map.Strict as M
import qualified Data.Set as S
ucheck :: S.Set ConstraintFC -> TC ()
ucheck :: Set ConstraintFC -> TC ()
ucheck = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Set ConstraintFC -> TC (Map Var Int)
solve Int
10 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> Set a -> Set a
S.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintFC -> Bool
ignore) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set ConstraintFC -> Set ConstraintFC
dropUnused
where
ignore :: ConstraintFC -> Bool
ignore (ConstraintFC UConstraint
c FC
_) | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Eq a => a -> a -> Bool
== String -> Int -> Var
Var [] (-Int
1)) (UConstraint -> [Var]
varsIn UConstraint
c) = Bool
True
ignore (ConstraintFC (ULE UExp
a UExp
b) FC
_) = UExp
a forall a. Eq a => a -> a -> Bool
== UExp
b
ignore ConstraintFC
_ = Bool
False
dropUnused :: S.Set ConstraintFC -> S.Set ConstraintFC
dropUnused :: Set ConstraintFC -> Set ConstraintFC
dropUnused Set ConstraintFC
xs = let cs :: [ConstraintFC]
cs = forall a. Set a -> [a]
S.toList Set ConstraintFC
xs
onlhs :: Map UExp Integer
onlhs = forall {a}. Num a => Map UExp a -> [ConstraintFC] -> Map UExp a
countLHS forall k a. Map k a
M.empty [ConstraintFC]
cs in
forall {a}.
Set ConstraintFC
-> Map UExp a -> [ConstraintFC] -> Set ConstraintFC
addIfUsed forall a. Set a
S.empty Map UExp Integer
onlhs [ConstraintFC]
cs
where
countLHS :: Map UExp a -> [ConstraintFC] -> Map UExp a
countLHS Map UExp a
ms [] = Map UExp a
ms
countLHS Map UExp a
ms (ConstraintFC
c : [ConstraintFC]
cs) = let lhvar :: UExp
lhvar = UConstraint -> UExp
getLHS (ConstraintFC -> UConstraint
uconstraint ConstraintFC
c)
num :: a
num = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup UExp
lhvar Map UExp a
ms of
Maybe a
Nothing -> a
1
Just a
v -> a
v forall a. Num a => a -> a -> a
+ a
1 in
Map UExp a -> [ConstraintFC] -> Map UExp a
countLHS (forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert UExp
lhvar a
num Map UExp a
ms) [ConstraintFC]
cs
addIfUsed :: Set ConstraintFC
-> Map UExp a -> [ConstraintFC] -> Set ConstraintFC
addIfUsed Set ConstraintFC
cs' Map UExp a
lhs [] = Set ConstraintFC
cs'
addIfUsed Set ConstraintFC
cs' Map UExp a
lhs (ConstraintFC
c : [ConstraintFC]
cs)
= let rhvar :: UExp
rhvar = UConstraint -> UExp
getRHS (ConstraintFC -> UConstraint
uconstraint ConstraintFC
c) in
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup UExp
rhvar Map UExp a
lhs of
Maybe a
Nothing -> Set ConstraintFC
-> Map UExp a -> [ConstraintFC] -> Set ConstraintFC
addIfUsed Set ConstraintFC
cs' Map UExp a
lhs [ConstraintFC]
cs
Just a
v -> Set ConstraintFC
-> Map UExp a -> [ConstraintFC] -> Set ConstraintFC
addIfUsed (forall a. Ord a => a -> Set a -> Set a
S.insert ConstraintFC
c Set ConstraintFC
cs') Map UExp a
lhs [ConstraintFC]
cs
getLHS :: UConstraint -> UExp
getLHS (ULT UExp
x UExp
_) = UExp
x
getLHS (ULE UExp
x UExp
_) = UExp
x
getRHS :: UConstraint -> UExp
getRHS (ULT UExp
_ UExp
x) = UExp
x
getRHS (ULE UExp
_ UExp
x) = UExp
x
data Var = Var String Int
deriving (Var -> Var -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Eq Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
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 :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
Ord, Int -> Var -> ShowS
[Var] -> ShowS
Var -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> String
$cshow :: Var -> String
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> Var -> ShowS
Show)
data Domain = Domain Int Int
deriving (Domain -> Domain -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Domain -> Domain -> Bool
$c/= :: Domain -> Domain -> Bool
== :: Domain -> Domain -> Bool
$c== :: Domain -> Domain -> Bool
Eq, Eq Domain
Domain -> Domain -> Bool
Domain -> Domain -> Ordering
Domain -> Domain -> Domain
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 :: Domain -> Domain -> Domain
$cmin :: Domain -> Domain -> Domain
max :: Domain -> Domain -> Domain
$cmax :: Domain -> Domain -> Domain
>= :: Domain -> Domain -> Bool
$c>= :: Domain -> Domain -> Bool
> :: Domain -> Domain -> Bool
$c> :: Domain -> Domain -> Bool
<= :: Domain -> Domain -> Bool
$c<= :: Domain -> Domain -> Bool
< :: Domain -> Domain -> Bool
$c< :: Domain -> Domain -> Bool
compare :: Domain -> Domain -> Ordering
$ccompare :: Domain -> Domain -> Ordering
Ord, Int -> Domain -> ShowS
[Domain] -> ShowS
Domain -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Domain] -> ShowS
$cshowList :: [Domain] -> ShowS
show :: Domain -> String
$cshow :: Domain -> String
showsPrec :: Int -> Domain -> ShowS
$cshowsPrec :: Int -> Domain -> ShowS
Show)
data SolverState =
SolverState
{ SolverState -> Queue
queue :: Queue
, SolverState -> Map Var (Domain, Set ConstraintFC)
domainStore :: M.Map Var ( Domain
, S.Set ConstraintFC
)
, SolverState -> Map Var (Set ConstraintFC)
cons_lhs :: M.Map Var (S.Set ConstraintFC)
, SolverState -> Map Var (Set ConstraintFC)
cons_rhs :: M.Map Var (S.Set ConstraintFC)
}
data Queue = Queue [ConstraintFC] (S.Set UConstraint)
solve :: Int -> S.Set ConstraintFC -> TC (M.Map Var Int)
solve :: Int -> Set ConstraintFC -> TC (Map Var Int)
solve Int
maxUniverseLevel Set ConstraintFC
ucs =
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (StateT SolverState TC ()
propagate forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadState SolverState m, Functor m) =>
m (Map Var Int)
extractSolution) SolverState
initSolverState
where
inpConstraints :: [ConstraintFC]
inpConstraints = forall a. Set a -> [a]
S.toAscList Set ConstraintFC
ucs
initSolverState :: SolverState
initSolverState :: SolverState
initSolverState =
let
([ConstraintFC]
initUnaryQueue, [ConstraintFC]
initQueue) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\ ConstraintFC
c -> forall (t :: * -> *) a. Foldable t => t a -> Int
length (UConstraint -> [Var]
varsIn (ConstraintFC -> UConstraint
uconstraint ConstraintFC
c)) forall a. Eq a => a -> a -> Bool
== Int
1) [ConstraintFC]
inpConstraints
in
SolverState
{ queue :: Queue
queue = [ConstraintFC] -> Set UConstraint -> Queue
Queue ([ConstraintFC]
initUnaryQueue forall a. [a] -> [a] -> [a]
++ [ConstraintFC]
initQueue) (forall a. Ord a => [a] -> Set a
S.fromList (forall a b. (a -> b) -> [a] -> [b]
map ConstraintFC -> UConstraint
uconstraint ([ConstraintFC]
initUnaryQueue forall a. [a] -> [a] -> [a]
++ [ConstraintFC]
initQueue)))
, domainStore :: Map Var (Domain, Set ConstraintFC)
domainStore = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ (Var
v, (Int -> Int -> Domain
Domain Int
0 Int
maxUniverseLevel, forall a. Set a
S.empty))
| Var
v <- forall a. Ord a => [a] -> [a]
ordNub [ Var
v
| ConstraintFC UConstraint
c FC
_ <- [ConstraintFC]
inpConstraints
, Var
v <- UConstraint -> [Var]
varsIn UConstraint
c
]
]
, cons_lhs :: Map Var (Set ConstraintFC)
cons_lhs = Map Var (Set ConstraintFC)
constraintsLHS
, cons_rhs :: Map Var (Set ConstraintFC)
cons_rhs = Map Var (Set ConstraintFC)
constraintsRHS
}
lhs :: UConstraint -> Maybe Var
lhs (ULT (UVar String
ns Int
x) UExp
_) = forall a. a -> Maybe a
Just (String -> Int -> Var
Var String
ns Int
x)
lhs (ULE (UVar String
ns Int
x) UExp
_) = forall a. a -> Maybe a
Just (String -> Int -> Var
Var String
ns Int
x)
lhs UConstraint
_ = forall a. Maybe a
Nothing
rhs :: UConstraint -> Maybe Var
rhs (ULT UExp
_ (UVar String
ns Int
x)) = forall a. a -> Maybe a
Just (String -> Int -> Var
Var String
ns Int
x)
rhs (ULE UExp
_ (UVar String
ns Int
x)) = forall a. a -> Maybe a
Just (String -> Int -> Var
Var String
ns Int
x)
rhs UConstraint
_ = forall a. Maybe a
Nothing
constraintsLHS :: M.Map Var (S.Set ConstraintFC)
constraintsLHS :: Map Var (Set ConstraintFC)
constraintsLHS = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith forall a. Ord a => Set a -> Set a -> Set a
S.union
[ (Var
v, forall a. a -> Set a
S.singleton (UConstraint -> FC -> ConstraintFC
ConstraintFC UConstraint
c FC
fc))
| (ConstraintFC UConstraint
c FC
fc) <- [ConstraintFC]
inpConstraints
, let vars :: [Var]
vars = UConstraint -> [Var]
varsIn UConstraint
c
, forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
vars forall a. Ord a => a -> a -> Bool
> Int
1
, Var
v <- [Var]
vars
, UConstraint -> Maybe Var
lhs UConstraint
c forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Var
v
]
constraintsRHS :: M.Map Var (S.Set ConstraintFC)
constraintsRHS :: Map Var (Set ConstraintFC)
constraintsRHS = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith forall a. Ord a => Set a -> Set a -> Set a
S.union
[ (Var
v, forall a. a -> Set a
S.singleton (UConstraint -> FC -> ConstraintFC
ConstraintFC UConstraint
c FC
fc))
| (ConstraintFC UConstraint
c FC
fc) <- [ConstraintFC]
inpConstraints
, let vars :: [Var]
vars = UConstraint -> [Var]
varsIn UConstraint
c
, forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
vars forall a. Ord a => a -> a -> Bool
> Int
1
, Var
v <- [Var]
vars
, UConstraint -> Maybe Var
rhs UConstraint
c forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Var
v
]
propagate :: StateT SolverState TC ()
propagate :: StateT SolverState TC ()
propagate = do
Maybe ConstraintFC
mcons <- forall (m :: * -> *).
MonadState SolverState m =>
m (Maybe ConstraintFC)
nextConstraint
case Maybe ConstraintFC
mcons of
Maybe ConstraintFC
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just (ConstraintFC UConstraint
cons FC
fc) -> do
case UConstraint
cons of
ULE UExp
a UExp
b -> do
Domain Int
lowerA Int
upperA <- forall (m :: * -> *). MonadState SolverState m => UExp -> m Domain
domainOf UExp
a
Domain Int
lowerB Int
upperB <- forall (m :: * -> *). MonadState SolverState m => UExp -> m Domain
domainOf UExp
b
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
upperB forall a. Ord a => a -> a -> Bool
< Int
upperA) forall a b. (a -> b) -> a -> b
$ ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
updateUpperBoundOf (UConstraint -> FC -> ConstraintFC
ConstraintFC UConstraint
cons FC
fc) UExp
a Int
upperB
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
lowerA forall a. Ord a => a -> a -> Bool
> Int
lowerB) forall a b. (a -> b) -> a -> b
$ ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
updateLowerBoundOf (UConstraint -> FC -> ConstraintFC
ConstraintFC UConstraint
cons FC
fc) UExp
b Int
lowerA
ULT UExp
a UExp
b -> do
Domain Int
lowerA Int
upperA <- forall (m :: * -> *). MonadState SolverState m => UExp -> m Domain
domainOf UExp
a
Domain Int
lowerB Int
upperB <- forall (m :: * -> *). MonadState SolverState m => UExp -> m Domain
domainOf UExp
b
let upperB_pred :: Int
upperB_pred = forall a. Enum a => a -> a
pred Int
upperB
let lowerA_succ :: Int
lowerA_succ = forall a. Enum a => a -> a
succ Int
lowerA
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
upperB_pred forall a. Ord a => a -> a -> Bool
< Int
upperA) forall a b. (a -> b) -> a -> b
$ ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
updateUpperBoundOf (UConstraint -> FC -> ConstraintFC
ConstraintFC UConstraint
cons FC
fc) UExp
a Int
upperB_pred
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
lowerA_succ forall a. Ord a => a -> a -> Bool
> Int
lowerB) forall a b. (a -> b) -> a -> b
$ ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
updateLowerBoundOf (UConstraint -> FC -> ConstraintFC
ConstraintFC UConstraint
cons FC
fc) UExp
b Int
lowerA_succ
StateT SolverState TC ()
propagate
extractSolution :: (MonadState SolverState m, Functor m) => m (M.Map Var Int)
extractSolution :: forall (m :: * -> *).
(MonadState SolverState m, Functor m) =>
m (Map Var Int)
extractSolution = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Domain -> Int
extractValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SolverState -> Map Var (Domain, Set ConstraintFC)
domainStore
extractValue :: Domain -> Int
extractValue :: Domain -> Int
extractValue (Domain Int
x Int
_) = Int
x
nextConstraint :: MonadState SolverState m => m (Maybe ConstraintFC)
nextConstraint :: forall (m :: * -> *).
MonadState SolverState m =>
m (Maybe ConstraintFC)
nextConstraint = do
Queue [ConstraintFC]
list Set UConstraint
set <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SolverState -> Queue
queue
case [ConstraintFC]
list of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
(ConstraintFC
q:[ConstraintFC]
qs) -> do
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ SolverState
st -> SolverState
st { queue :: Queue
queue = [ConstraintFC] -> Set UConstraint -> Queue
Queue [ConstraintFC]
qs (forall a. Ord a => a -> Set a -> Set a
S.delete (ConstraintFC -> UConstraint
uconstraint ConstraintFC
q) Set UConstraint
set) }
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just ConstraintFC
q)
domainOf :: MonadState SolverState m => UExp -> m Domain
domainOf :: forall (m :: * -> *). MonadState SolverState m => UExp -> m Domain
domainOf (UVar String
ns Int
var) = forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall k a. Ord k => Map k a -> k -> a
M.! String -> Int -> Var
Var String
ns Int
var) forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverState -> Map Var (Domain, Set ConstraintFC)
domainStore)
domainOf (UVal Int
val) = forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Int -> Domain
Domain Int
val Int
val)
asPair :: Domain -> (Int, Int)
asPair :: Domain -> (Int, Int)
asPair (Domain Int
x Int
y) = (Int
x, Int
y)
updateUpperBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
updateUpperBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
updateUpperBoundOf ConstraintFC
suspect (UVar String
ns Int
var) Int
upper = do
Map Var (Domain, Set ConstraintFC)
doms <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SolverState -> Map Var (Domain, Set ConstraintFC)
domainStore
let (oldDom :: Domain
oldDom@(Domain Int
lower Int
_), Set ConstraintFC
suspects) = Map Var (Domain, Set ConstraintFC)
doms forall k a. Ord k => Map k a -> k -> a
M.! String -> Int -> Var
Var String
ns Int
var
let newDom :: Domain
newDom = Int -> Int -> Domain
Domain Int
lower Int
upper
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Domain -> Bool
wipeOut Domain
newDom) forall a b. (a -> b) -> a -> b
$
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
Error forall a b. (a -> b) -> a -> b
$
forall t.
FC -> UExp -> (Int, Int) -> (Int, Int) -> [ConstraintFC] -> Err' t
UniverseError (ConstraintFC -> FC
ufc ConstraintFC
suspect) (String -> Int -> UExp
UVar String
ns Int
var)
(Domain -> (Int, Int)
asPair Domain
oldDom) (Domain -> (Int, Int)
asPair Domain
newDom)
(ConstraintFC
suspect forall a. a -> [a] -> [a]
: forall a. Set a -> [a]
S.toList Set ConstraintFC
suspects)
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ SolverState
st -> SolverState
st { domainStore :: Map Var (Domain, Set ConstraintFC)
domainStore = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (String -> Int -> Var
Var String
ns Int
var) (Domain
newDom, forall a. Ord a => a -> Set a -> Set a
S.insert ConstraintFC
suspect Set ConstraintFC
suspects) Map Var (Domain, Set ConstraintFC)
doms }
forall (m :: * -> *).
MonadState SolverState m =>
UConstraint -> Var -> m ()
addToQueueRHS (ConstraintFC -> UConstraint
uconstraint ConstraintFC
suspect) (String -> Int -> Var
Var String
ns Int
var)
updateUpperBoundOf ConstraintFC
_ UVal{} Int
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
updateLowerBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
updateLowerBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
updateLowerBoundOf ConstraintFC
suspect (UVar String
ns Int
var) Int
lower = do
Map Var (Domain, Set ConstraintFC)
doms <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SolverState -> Map Var (Domain, Set ConstraintFC)
domainStore
let (oldDom :: Domain
oldDom@(Domain Int
_ Int
upper), Set ConstraintFC
suspects) = Map Var (Domain, Set ConstraintFC)
doms forall k a. Ord k => Map k a -> k -> a
M.! String -> Int -> Var
Var String
ns Int
var
let newDom :: Domain
newDom = Int -> Int -> Domain
Domain Int
lower Int
upper
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Domain -> Bool
wipeOut Domain
newDom) forall a b. (a -> b) -> a -> b
$
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
Error forall a b. (a -> b) -> a -> b
$
forall t.
FC -> UExp -> (Int, Int) -> (Int, Int) -> [ConstraintFC] -> Err' t
UniverseError (ConstraintFC -> FC
ufc ConstraintFC
suspect) (String -> Int -> UExp
UVar String
ns Int
var)
(Domain -> (Int, Int)
asPair Domain
oldDom) (Domain -> (Int, Int)
asPair Domain
newDom)
(ConstraintFC
suspect forall a. a -> [a] -> [a]
: forall a. Set a -> [a]
S.toList Set ConstraintFC
suspects)
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ SolverState
st -> SolverState
st { domainStore :: Map Var (Domain, Set ConstraintFC)
domainStore = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (String -> Int -> Var
Var String
ns Int
var) (Domain
newDom, forall a. Ord a => a -> Set a -> Set a
S.insert ConstraintFC
suspect Set ConstraintFC
suspects) Map Var (Domain, Set ConstraintFC)
doms }
forall (m :: * -> *).
MonadState SolverState m =>
UConstraint -> Var -> m ()
addToQueueLHS (ConstraintFC -> UConstraint
uconstraint ConstraintFC
suspect) (String -> Int -> Var
Var String
ns Int
var)
updateLowerBoundOf ConstraintFC
_ UVal{} Int
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
addToQueueLHS :: MonadState SolverState m => UConstraint -> Var -> m ()
addToQueueLHS :: forall (m :: * -> *).
MonadState SolverState m =>
UConstraint -> Var -> m ()
addToQueueLHS UConstraint
thisCons Var
var = do
Map Var (Set ConstraintFC)
clhs <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SolverState -> Map Var (Set ConstraintFC)
cons_lhs
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
var Map Var (Set ConstraintFC)
clhs of
Maybe (Set ConstraintFC)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just Set ConstraintFC
cs -> do
Queue [ConstraintFC]
list Set UConstraint
set <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SolverState -> Queue
queue
let set' :: Set UConstraint
set' = forall a. Ord a => a -> Set a -> Set a
S.insert UConstraint
thisCons Set UConstraint
set
let newCons :: [ConstraintFC]
newCons = [ ConstraintFC
c | ConstraintFC
c <- forall a. Set a -> [a]
S.toList Set ConstraintFC
cs, ConstraintFC -> UConstraint
uconstraint ConstraintFC
c forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set UConstraint
set' ]
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ConstraintFC]
newCons
then forall (m :: * -> *) a. Monad m => a -> m a
return ()
else forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ SolverState
st -> SolverState
st { queue :: Queue
queue = [ConstraintFC] -> Set UConstraint -> Queue
Queue ([ConstraintFC]
list forall a. [a] -> [a] -> [a]
++ [ConstraintFC]
newCons)
(forall a. Ord a => Set a -> Set a -> Set a
S.union Set UConstraint
set (forall a. Ord a => [a] -> Set a
S.fromList (forall a b. (a -> b) -> [a] -> [b]
map ConstraintFC -> UConstraint
uconstraint [ConstraintFC]
newCons))) }
addToQueueRHS :: MonadState SolverState m => UConstraint -> Var -> m ()
addToQueueRHS :: forall (m :: * -> *).
MonadState SolverState m =>
UConstraint -> Var -> m ()
addToQueueRHS UConstraint
thisCons Var
var = do
Map Var (Set ConstraintFC)
crhs <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SolverState -> Map Var (Set ConstraintFC)
cons_rhs
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
var Map Var (Set ConstraintFC)
crhs of
Maybe (Set ConstraintFC)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just Set ConstraintFC
cs -> do
Queue [ConstraintFC]
list Set UConstraint
set <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SolverState -> Queue
queue
let set' :: Set UConstraint
set' = forall a. Ord a => a -> Set a -> Set a
S.insert UConstraint
thisCons Set UConstraint
set
let newCons :: [ConstraintFC]
newCons = [ ConstraintFC
c | ConstraintFC
c <- forall a. Set a -> [a]
S.toList Set ConstraintFC
cs, ConstraintFC -> UConstraint
uconstraint ConstraintFC
c forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set UConstraint
set' ]
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ConstraintFC]
newCons
then forall (m :: * -> *) a. Monad m => a -> m a
return ()
else forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ SolverState
st -> SolverState
st { queue :: Queue
queue = [ConstraintFC] -> Set UConstraint -> Queue
Queue ([ConstraintFC]
list forall a. [a] -> [a] -> [a]
++ [ConstraintFC]
newCons)
(forall {a}. Ord a => [a] -> Set a -> Set a
insertAll (forall a b. (a -> b) -> [a] -> [b]
map ConstraintFC -> UConstraint
uconstraint [ConstraintFC]
newCons) Set UConstraint
set) }
insertAll :: [a] -> Set a -> Set a
insertAll [] Set a
s = Set a
s
insertAll (a
x : [a]
xs) Set a
s = [a] -> Set a -> Set a
insertAll [a]
xs (forall a. Ord a => a -> Set a -> Set a
S.insert a
x Set a
s)
wipeOut :: Domain -> Bool
wipeOut :: Domain -> Bool
wipeOut (Domain Int
l Int
u) = Int
l forall a. Ord a => a -> a -> Bool
> Int
u
ordNub :: Ord a => [a] -> [a]
ordNub :: forall a. Ord a => [a] -> [a]
ordNub = forall a. Set a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
S.fromList
varsIn :: UConstraint -> [Var]
varsIn :: UConstraint -> [Var]
varsIn (ULT UExp
a UExp
b) = [ String -> Int -> Var
Var String
ns Int
v | UVar String
ns Int
v <- [UExp
a,UExp
b] ]
varsIn (ULE UExp
a UExp
b) = [ String -> Int -> Var
Var String
ns Int
v | UVar String
ns Int
v <- [UExp
a,UExp
b] ]