@@ -1,7 +1,7 @@
1-- | Check universe constraints.
1-- | Check universe constraints.
2module Idris.Core.Constraints(ucheck) where
2module Idris.Core.Constraints(ucheck) where
4−import Idris.Core.TT hiding (I)
4+import Idris.Core.TT hiding (I, Var)
5import Idris.Core.Typecheck
5import Idris.Core.Typecheck
7import Control.Applicative
7import Control.Applicative
@@ -22,8 +22,8 @@ import Debug.Trace
22ucheck :: [(UConstraint, FC)] -> TC ()
22ucheck :: [(UConstraint, FC)] -> TC ()
23ucheck = void . solve
23ucheck = void . solve
25−-- TODO: change this to a newtype
26−type Var = Int
25+newtype Var = Var Int
26+ deriving (Eq, Ord, Show)
28data SolverState =
28data SolverState =
29 SolverState
29 SolverState
@@ -70,8 +70,8 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
72 varsIn :: UConstraint -> [Var]
72 varsIn :: UConstraint -> [Var]
73− varsIn (ULT a b) = [ v | UVar v <- [a,b] ]
73+ varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]
74− varsIn (ULE a b) = [ v | UVar v <- [a,b] ]
74+ varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]
76 -- propagate :: MonadState SolverState m => m ()
76 -- propagate :: MonadState SolverState m => m ()
77 propagate = do
77 propagate = do
@@ -110,18 +110,18 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
110 return (Just q)
110 return (Just q)
112 domainOf :: MonadState SolverState m => UExp -> m (InfInt, InfInt)
112 domainOf :: MonadState SolverState m => UExp -> m (InfInt, InfInt)
113− domainOf (UVar var) = gets ((M.! var) . domainStore)
113+ domainOf (UVar var) = gets ((M.! Var var) . domainStore)
114 domainOf (UVal val) = return (I val, I val)
114 domainOf (UVal val) = return (I val, I val)
116 -- updateDomainOf :: MonadState SolverState m => UExp -> (InfInt, InfInt) -> m ()
116 -- updateDomainOf :: MonadState SolverState m => UExp -> (InfInt, InfInt) -> m ()
117 updateDomainOf (UVar var) dom = do
117 updateDomainOf (UVar var) dom = do
118 doms <- gets domainStore
118 doms <- gets domainStore
119− let oldDom = doms M.! var
119+ let oldDom = doms M.! Var var
120 let newDom = domainIntersect oldDom dom
120 let newDom = domainIntersect oldDom dom
121 when (wipeOut newDom) $ lift $ Error UniverseError
121 when (wipeOut newDom) $ lift $ Error UniverseError
122 unless (oldDom == newDom) $ do
122 unless (oldDom == newDom) $ do
123− modify $ \ st -> st { domainStore = M.insert var newDom doms }
123+ modify $ \ st -> st { domainStore = M.insert (Var var) newDom doms }
124− addToQueue var
124+ addToQueue (Var var)
125 updateDomainOf UVal{} _ = return ()
125 updateDomainOf UVal{} _ = return ()
127 -- addToQueue :: MonadState SolverState m => Var -> m ()
127 -- addToQueue :: MonadState SolverState m => Var -> m ()