{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses #-}
{-|
Module      : Idris.Core.Constraints
Description : Check universe constraints.

License     : BSD3
Maintainer  : The Idris Community.
-}
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

-- | Check that a list of universe constraints can be satisfied.
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
        -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with
        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
    -- Count the number of times a variable occurs on the LHS of a constraint
    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

    -- Only keep a constraint if the variable on the RHS is used elsewhere
    -- on the LHS of a constraint
    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        -- constraints that effected this variable
                                   )
        , 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

        -- | initial solver state.
        --   the queue contains all constraints, the domain store contains the initial domains.
        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

        -- | a map from variables to the list of constraints the variable occurs in. (in the LHS of a constraint)
        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               -- do not register unary constraints
            , 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
            ]

        -- | a map from variables to the list of constraints the variable occurs in. (in the RHS of a constraint)
        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               -- do not register unary constraints
            , 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
            ]

        -- | this is where the actual work is done.
        --   dequeue the first constraint,
        --   filter domains,
        --   update domains (possibly resulting in a domain wipe out),
        --   until the queue is empty.
        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

        -- | extract a solution from the state.
        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

        -- | dequeue the first constraint.
        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)

        -- | look up the domain of a variable from the state.
        --   for convenience, this function also accepts UVal's and returns a singleton domain for them.
        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 ()

        -- | add all constraints (with the given var on the lhs) to the queue
        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))) }

        -- | add all constraints (with the given var on the rhs) to the queue
        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)

        -- | check if a domain is wiped out.
        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

-- | variables in a constraint
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] ]