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