@@ -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
4+import Idris.Core.TT hiding (I)
5import Idris.Core.Typecheck
5import Idris.Core.Typecheck
7import Control.Applicative
7import Control.Applicative
@@ -11,61 +11,129 @@ import Control.Monad.State
11import qualified Data.Set as S
11import qualified Data.Set as S
12import Data.List
12import Data.List
13import Data.Maybe
13import Data.Maybe
14import qualified Data.Map.Strict as M
15import qualified Data.Map.Strict as M
17+import Control.DeepSeq
16import Debug.Trace
19import Debug.Trace
18-- | Check that a list of universe constraints can be satisfied.
21-- | Check that a list of universe constraints can be satisfied.
19ucheck :: [(UConstraint, FC)] -> TC ()
22ucheck :: [(UConstraint, FC)] -> TC ()
20−ucheck cs = acyclic rels (map fst (M.toList rels))
23+ucheck = void . solve
21− where lhs (ULT l _) = l
24+
22− lhs (ULE l _) = l
25+-- TODO: change this to a newtype
23− cs' = S.toList (S.fromList cs)
26+type Var = Int
24− rels = mkRels cs' M.empty
27+
26−type Relations = M.Map UExp [(UConstraint, FC)]
29+ SolverState
27−
30+ { queue :: [(UConstraint, FC)]
28−mkRels :: [(UConstraint, FC)] -> Relations -> Relations
31+ , domainStore :: M.Map Var (InfInt, InfInt)
29−mkRels [] acc = acc
32+ }
30−mkRels ((c, f) : cs) acc
33+
31− | not (ignore c)
34+data InfInt = NegInf | I Int | PosInf
32− = case M.lookup (lhs c) acc of
35+ deriving (Eq, Ord, Show)
33− Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)
36+
34− Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)
37+instance Enum InfInt where
35− | otherwise = mkRels cs acc
38+ succ (I x) = I (succ x)
36− where lhs (ULT l _) = l
39+ succ x = x
37− lhs (ULE l _) = l
40+ pred (I x) = I (pred x)
38− ignore (ULE l r) = l == r
41+ pred x = x
39− ignore _ = False
42+ toEnum = I
40−
43+ fromEnum (I x) = x
41−
44+ fromEnum NegInf = minBound
42−acyclic :: Relations -> [UExp] -> TC ()
45+ fromEnum PosInf = maxBound
43−acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs
46+
48+solve :: [(UConstraint, FC)] -> TC (M.Map Var Int)
49+solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
45− checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()
52+
46− checkCycle fc r path inc [] = return ()
53+ initSolverState :: SolverState
47− checkCycle fc r path inc (c : cs)
54+ initSolverState = SolverState
48− = do check fc r path inc c
55+ { queue = inpConstraints
49− -- Remove c from r since we know there's no cycles now
56+ , domainStore = M.fromList
50− let r' = M.insert c [] r
57+ [ (v, (I 0, I 10))
51− checkCycle fc r' path inc cs
58+ | v <- ordNub [ v
52−
59+ | (c, _) <- inpConstraints
53− check fc r path inc (UVar x) | x < 0 = return ()
60+ , v <- varsIn c
54− check fc r path inc cv
61+ ]
55− | inc > 0 && cv `elem` map fst path
62+ ]
65+ constraints :: M.Map Var [(UConstraint, FC)]
66+ constraints = M.fromListWith (++)
68+ | (c, fc) <- inpConstraints
72+ varsIn :: UConstraint -> [Var]
73+ varsIn (ULT a b) = [ v | UVar v <- [a,b] ]
74+ varsIn (ULE a b) = [ v | UVar v <- [a,b] ]
76+ -- propagate :: MonadState SolverState m => m ()
78+ mcons <- nextConstraint
81+ Just (cons, _fc) -> do
84+ (lowerA, upperA) <- domainOf a
85+ (lowerB, upperB) <- domainOf b
86+ updateDomainOf a (lowerA, min upperA upperB)
87+ updateDomainOf b (max lowerB lowerA, upperB)
89+ (lowerA, upperA) <- domainOf a
90+ (lowerB, upperB) <- domainOf b
91+ updateDomainOf a (lowerA, min upperA (pred upperB))
92+ updateDomainOf b (max lowerB (succ lowerA), upperB)
95+ extractSolution :: (MonadState SolverState m, Functor m) => m (M.Map Var Int)
96+ extractSolution = M.map extractVal <$> gets domainStore
98+ extractVal :: (InfInt, InfInt) -> Int
99+ extractVal (_, I x) = x
100+ extractVal (I x, _) = x
103+ nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))
107+ [] -> return Nothing
109+ modify $ \ st -> st { queue = qs \\ [q] }
112+ domainOf :: MonadState SolverState m => UExp -> m (InfInt, InfInt)
113+ domainOf (UVar var) = gets ((M.! var) . domainStore)
114+ domainOf (UVal val) = return (I val, I val)
116+ -- updateDomainOf :: MonadState SolverState m => UExp -> (InfInt, InfInt) -> m ()
117+ updateDomainOf (UVar var) dom = do
118+ doms <- gets domainStore
119+ let oldDom = doms M.! var
120+ let newDom = domainIntersect oldDom dom
56− = Error $ At fc UniverseError
121+ when (wipeOut newDom) $ lift $ Error UniverseError
57− -- FIXME: Make informative
122+ unless (oldDom == newDom) $ do
58− -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))
123+ modify $ \ st -> st { domainStore = M.insert var newDom doms }
59− -- Issue #1725 on the issue tracker.
124+ addToQueue var
60− -- https://github.com/idris-lang/Idris-dev/issues/1725
125+ updateDomainOf UVal{} _ = return ()
61− -- if we reach a cycle but we're at the same universe level, it's
126+
62− -- fine, because they must all be equal, so stop.
127+ -- addToQueue :: MonadState SolverState m => Var -> m ()
63− | inc == 0 && cv `elem` map fst path
128+ addToQueue var = do
64− = return ()
129+ let cs = constraints M.! var
65− | otherwise
130+ modify $ \ st -> st { queue = queue st ++ ordNub cs }
66− = case M.lookup cv r of
131+
67− Nothing -> return ()
132+ domainIntersect :: (InfInt, InfInt) -> (InfInt, InfInt) -> (InfInt, InfInt)
68− Just cs -> mapM_ (next r ((cv, fc):path) inc) cs
133+ domainIntersect (a,b) (c,d) = (max a c, min b d)
70− next r path inc (ULT l x, fc) = check fc r path (inc + 1) x
135+ wipeOut :: (InfInt, InfInt) -> Bool
71− next r path inc (ULE l x, fc) = check fc r path inc x
136+ wipeOut (l, u) = l > u
138+ordNub :: Ord a => [a] -> [a]
139+ordNub = S.toList . S.fromList