@@ -1,7 +1,7 @@
11-- | Check universe constraints.
22module Idris.Core.Constraints(ucheck) where
33
4−import Idris.Core.TT hiding (I)
4+import Idris.Core.TT hiding (I, Var)
55import Idris.Core.Typecheck
66
77import Control.Applicative
@@ -22,8 +22,8 @@ import Debug.Trace
2222ucheck :: [(UConstraint, FC)] -> TC ()
2323ucheck = void . solve
2424
25−-- TODO: change this to a newtype
26−type Var = Int
25+newtype Var = Var Int
26+ deriving (Eq, Ord, Show)
2727
2828data SolverState =
2929 SolverState
@@ -70,8 +70,8 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
7070 ]
7171
7272 varsIn :: UConstraint -> [Var]
73− varsIn (ULT a b) = [ v | UVar v <- [a,b] ]
74− varsIn (ULE a b) = [ v | UVar v <- [a,b] ]
73+ varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]
74+ varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]
7575
7676 -- propagate :: MonadState SolverState m => m ()
7777 propagate = do
@@ -110,18 +110,18 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
110110 return (Just q)
111111
112112 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)
114114 domainOf (UVal val) = return (I val, I val)
115115
116116 -- updateDomainOf :: MonadState SolverState m => UExp -> (InfInt, InfInt) -> m ()
117117 updateDomainOf (UVar var) dom = do
118118 doms <- gets domainStore
119− let oldDom = doms M.! var
119+ let oldDom = doms M.! Var var
120120 let newDom = domainIntersect oldDom dom
121121 when (wipeOut newDom) $ lift $ Error UniverseError
122122 unless (oldDom == newDom) $ do
123− modify $ \ st -> st { domainStore = M.insert var newDom doms }
124− addToQueue var
123+ modify $ \ st -> st { domainStore = M.insert (Var var) newDom doms }
124+ addToQueue (Var var)
125125 updateDomainOf UVal{} _ = return ()
126126
127127 -- addToQueue :: MonadState SolverState m => Var -> m ()