@@ -1,26 +1,18 @@
11-- | Check universe constraints.
2−module Idris.Core.Constraints(ucheck) where
2+module Idris.Core.Constraints ( ucheck ) where
33
4−import Idris.Core.TT hiding (I, Var)
5−import Idris.Core.Typecheck
4+import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..), Err'(..) )
65
76import Control.Applicative
8−import Control.Arrow
9−import Control.Monad.RWS
107import Control.Monad.State
11−import qualified Data.Set as S
128import Data.List
13−import Data.Maybe
14−import Data.Either
159import qualified Data.Map.Strict as M
10+import qualified Data.Set as S
1611
17−import Control.DeepSeq
18−
19−import Debug.Trace
2012
2113-- | Check that a list of universe constraints can be satisfied.
2214ucheck :: [(UConstraint, FC)] -> TC ()
23−ucheck = void . solve . filter (not . ignore)
15+ucheck = void . solve 10 . filter (not . ignore)
2416 where ignore (c,_) = any (== Var (-1)) (varsIn c)
2517 -- TODO: remove the ignore when Idris.Core.Binary:598
2618
@@ -37,16 +29,19 @@ data SolverState =
3729 )
3830 }
3931
40−solve :: [(UConstraint, FC)] -> TC (M.Map Var Int)
41−solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
32+solve :: Int -> [(UConstraint, FC)] -> TC (M.Map Var Int)
33+solve maxUniverseLevel inpConstraints =
34+ evalStateT (propagate >> extractSolution) initSolverState
4235
4336 where
4437
38+ -- | initial solver state.
39+ -- the queue contains all constraints, the domain store contains the initial domains.
4540 initSolverState :: SolverState
4641 initSolverState = SolverState
47− { queue = inpConstraints
42+ { queue = ordNub inpConstraints
4843 , domainStore = M.fromList
49− [ (v, ((0, 10), []))
44+ [ (v, ((0, maxUniverseLevel), []))
5045 | v <- ordNub [ v
5146 | (c, _) <- inpConstraints
5247 , v <- varsIn c
@@ -54,14 +49,20 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
5449 ]
5550 }
5651
52+ -- | a map from variables to the list of constraints the variable occurs in.
5753 constraints :: M.Map Var [(UConstraint, FC)]
58− constraints = M.fromListWith (++)
54+ constraints = M.map ordNub $ M.fromListWith (++)
5955 [ (v, [(c,fc)])
6056 | (c, fc) <- inpConstraints
6157 , v <- varsIn c
6258 ]
6359
64− -- propagate :: MonadState SolverState m => m ()
60+ -- | this is where the actual work is done.
61+ -- dequeue the first constraint,
62+ -- filter domains,
63+ -- update domains (possibly resulting in a domain wipe out),
64+ -- until the queue is empty.
65+ propagate :: StateT SolverState TC ()
6566 propagate = do
6667 mcons <- nextConstraint
6768 case mcons of
@@ -80,9 +81,11 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
8081 updateDomainOf (cons, fc) b (max lowerB (succ lowerA), upperB)
8182 propagate
8283
84+ -- | extract a solution from the state.
8385 extractSolution :: (MonadState SolverState m, Functor m) => m (M.Map Var Int)
8486 extractSolution = M.map (fst . fst) <$> gets domainStore
8587
88+ -- | dequeue the first constraint.
8689 nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))
8790 nextConstraint = do
8891 qu <- gets queue
@@ -92,11 +95,15 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
9295 modify $ \ st -> st { queue = qs \\ [q] }
9396 return (Just q)
9497
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.
95100 domainOf :: MonadState SolverState m => UExp -> m (Int, Int)
96101 domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)
97102 domainOf (UVal val) = return (val, val)
98103
99− -- updateDomainOf :: MonadState SolverState m => UConstraint -> UExp -> (Int, Int) -> m ()
104+ -- | updates the domain of a variable.
105+ -- this function is also where we fail, inc ase of a domain wipe-out.
106+ updateDomainOf :: (UConstraint, FC) -> UExp -> (Int, Int) -> StateT SolverState TC ()
100107 updateDomainOf suspect (UVar var) dom = do
101108 doms <- gets domainStore
102109 let (oldDom, suspects) = doms M.! Var var
@@ -122,20 +129,24 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
122129 addToQueue (Var var)
123130 updateDomainOf _ UVal{} _ = return ()
124131
125− -- addToQueue :: MonadState SolverState m => Var -> m ()
132+ -- | add all constraints related to a variable.
133+ addToQueue :: MonadState SolverState m => Var -> m ()
126134 addToQueue var = do
127135 let cs = constraints M.! var
128− modify $ \ st -> st { queue = queue st ++ ordNub cs }
136+ modify $ \ st -> st { queue = queue st ++ cs }
129137
138+ -- | intersecting two domains, the resulting domain can be wiped out.
130139 domainIntersect :: (Int, Int) -> (Int, Int) -> (Int, Int)
131140 domainIntersect (a,b) (c,d) = (max a c, min b d)
132141
142+ -- | check if a domain is wiped out.
133143 wipeOut :: (Int, Int) -> Bool
134144 wipeOut (l, u) = l > u
135145
136146ordNub :: Ord a => [a] -> [a]
137147ordNub = S.toList . S.fromList
138148
149+-- | variables in a constraint
139150varsIn :: UConstraint -> [Var]
140151varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]
141152varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]