@@ -1,26 +1,18 @@
1-- | Check universe constraints.
1-- | Check universe constraints.
2−module Idris.Core.Constraints(ucheck) where
2+module Idris.Core.Constraints ( ucheck ) where
4−import Idris.Core.TT hiding (I, Var)
4+import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..), Err'(..) )
5−import Idris.Core.Typecheck
7import Control.Applicative
6import Control.Applicative
9−import Control.Monad.RWS
10import Control.Monad.State
7import Control.Monad.State
11−import qualified Data.Set as S
12import Data.List
8import Data.List
15import qualified Data.Map.Strict as M
9import qualified Data.Map.Strict as M
10+import qualified Data.Set as S
17−import Control.DeepSeq
21-- | Check that a list of universe constraints can be satisfied.
13-- | Check that a list of universe constraints can be satisfied.
22ucheck :: [(UConstraint, FC)] -> TC ()
14ucheck :: [(UConstraint, FC)] -> TC ()
23−ucheck = void . solve . filter (not . ignore)
15+ucheck = void . solve 10 . filter (not . ignore)
24 where ignore (c,_) = any (== Var (-1)) (varsIn c)
16 where ignore (c,_) = any (== Var (-1)) (varsIn c)
25 -- TODO: remove the ignore when Idris.Core.Binary:598
17 -- TODO: remove the ignore when Idris.Core.Binary:598
@@ -37,16 +29,19 @@ data SolverState =
40−solve :: [(UConstraint, FC)] -> TC (M.Map Var Int)
32+solve :: Int -> [(UConstraint, FC)] -> TC (M.Map Var Int)
33+solve maxUniverseLevel inpConstraints =
41−solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
34+ evalStateT (propagate >> extractSolution) initSolverState
38+ -- | initial solver state.
39+ -- the queue contains all constraints, the domain store contains the initial domains.
45 initSolverState :: SolverState
40 initSolverState :: SolverState
46 initSolverState = SolverState
41 initSolverState = SolverState
47− { queue = inpConstraints
42+ { queue = ordNub inpConstraints
48 , domainStore = M.fromList
43 , domainStore = M.fromList
49− [ (v, ((0, 10), []))
44+ [ (v, ((0, maxUniverseLevel), []))
50 | v <- ordNub [ v
45 | v <- ordNub [ v
51 | (c, _) <- inpConstraints
46 | (c, _) <- inpConstraints
52 , v <- varsIn c
47 , v <- varsIn c
@@ -54,14 +49,20 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
52+ -- | a map from variables to the list of constraints the variable occurs in.
57 constraints :: M.Map Var [(UConstraint, FC)]
53 constraints :: M.Map Var [(UConstraint, FC)]
58− constraints = M.fromListWith (++)
54+ constraints = M.map ordNub $ M.fromListWith (++)
59 [ (v, [(c,fc)])
55 [ (v, [(c,fc)])
60 | (c, fc) <- inpConstraints
56 | (c, fc) <- inpConstraints
61 , v <- varsIn c
57 , v <- varsIn c
60+ -- | this is where the actual work is done.
61+ -- dequeue the first constraint,
63+ -- update domains (possibly resulting in a domain wipe out),
64+ -- until the queue is empty.
64− -- propagate :: MonadState SolverState m => m ()
65+ propagate :: StateT SolverState TC ()
65 propagate = do
66 propagate = do
66 mcons <- nextConstraint
67 mcons <- nextConstraint
67 case mcons of
68 case mcons of
@@ -80,9 +81,11 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
80 updateDomainOf (cons, fc) b (max lowerB (succ lowerA), upperB)
81 updateDomainOf (cons, fc) b (max lowerB (succ lowerA), upperB)
84+ -- | extract a solution from the state.
83 extractSolution :: (MonadState SolverState m, Functor m) => m (M.Map Var Int)
85 extractSolution :: (MonadState SolverState m, Functor m) => m (M.Map Var Int)
84 extractSolution = M.map (fst . fst) <$> gets domainStore
86 extractSolution = M.map (fst . fst) <$> gets domainStore
88+ -- | dequeue the first constraint.
86 nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))
89 nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))
87 nextConstraint = do
90 nextConstraint = do
88 qu <- gets queue
91 qu <- gets queue
@@ -92,11 +95,15 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
92 modify $ \ st -> st { queue = qs \\ [q] }
95 modify $ \ st -> st { queue = qs \\ [q] }
93 return (Just q)
96 return (Just q)
98+ -- | look up the domain of a variable from the state.
99+ -- for convenience, this function also accepts UVal's and returns a singleton domain for them.
95 domainOf :: MonadState SolverState m => UExp -> m (Int, Int)
100 domainOf :: MonadState SolverState m => UExp -> m (Int, Int)
96 domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)
101 domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)
97 domainOf (UVal val) = return (val, val)
102 domainOf (UVal val) = return (val, val)
104+ -- | updates the domain of a variable.
105+ -- this function is also where we fail, inc ase of a domain wipe-out.
99− -- updateDomainOf :: MonadState SolverState m => UConstraint -> UExp -> (Int, Int) -> m ()
106+ updateDomainOf :: (UConstraint, FC) -> UExp -> (Int, Int) -> StateT SolverState TC ()
100 updateDomainOf suspect (UVar var) dom = do
107 updateDomainOf suspect (UVar var) dom = do
101 doms <- gets domainStore
108 doms <- gets domainStore
102 let (oldDom, suspects) = doms M.! Var var
109 let (oldDom, suspects) = doms M.! Var var
@@ -122,20 +129,24 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
122 addToQueue (Var var)
129 addToQueue (Var var)
123 updateDomainOf _ UVal{} _ = return ()
130 updateDomainOf _ UVal{} _ = return ()
132+ -- | add all constraints related to a variable.
125− -- addToQueue :: MonadState SolverState m => Var -> m ()
133+ addToQueue :: MonadState SolverState m => Var -> m ()
126 addToQueue var = do
134 addToQueue var = do
127 let cs = constraints M.! var
135 let cs = constraints M.! var
128− modify $ \ st -> st { queue = queue st ++ ordNub cs }
136+ modify $ \ st -> st { queue = queue st ++ cs }
138+ -- | intersecting two domains, the resulting domain can be wiped out.
130 domainIntersect :: (Int, Int) -> (Int, Int) -> (Int, Int)
139 domainIntersect :: (Int, Int) -> (Int, Int) -> (Int, Int)
131 domainIntersect (a,b) (c,d) = (max a c, min b d)
140 domainIntersect (a,b) (c,d) = (max a c, min b d)
142+ -- | check if a domain is wiped out.
133 wipeOut :: (Int, Int) -> Bool
143 wipeOut :: (Int, Int) -> Bool
134 wipeOut (l, u) = l > u
144 wipeOut (l, u) = l > u
136ordNub :: Ord a => [a] -> [a]
146ordNub :: Ord a => [a] -> [a]
137ordNub = S.toList . S.fromList
147ordNub = S.toList . S.fromList
149+-- | variables in a constraint
139varsIn :: UConstraint -> [Var]
150varsIn :: UConstraint -> [Var]
140varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]
151varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]
141varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]
152varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]