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