@@ -1,71 +1,164 @@
11-- | Check universe constraints.
2−module Idris.Core.Constraints(ucheck) where
2+module Idris.Core.Constraints ( ucheck ) where
33
4−import Idris.Core.TT
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
10−import Control.Monad.State
11−import qualified Data.Set as S
12−import Data.List
13−import Data.Maybe
7+import Control.Monad.State.Strict
8+import Data.Function ( on )
9+import Data.List ( partition, nubBy )
1410import qualified Data.Map.Strict as M
11+import qualified Data.Set as S
1512
16−import Debug.Trace
1713
1814-- | Check that a list of universe constraints can be satisfied.
1915ucheck :: [(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
16+ucheck = void . solve 10 . nubBy ((==) `on` fst) . filter (not . ignore)
17+ where
18+ -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with
19+ ignore (c,_) | any (== Var (-1)) (varsIn c) = True
20+ ignore (ULE a b, _) = a == b
3921 ignore _ = False
4022
23+newtype Var = Var Int
24+ deriving (Eq, Ord, Show)
25+
26+data Domain = Domain {-# UNPACK #-} !Int
27+ {-# UNPACK #-} !Int
28+ deriving (Eq, Ord, Show)
29+
30+data SolverState =
31+ SolverState
32+ { queue :: Queue
33+ , domainStore :: M.Map Var ( Domain
34+ , S.Set (UConstraint, FC) -- constraints that effected this variable
35+ )
36+ }
37+
38+data Queue = Queue [(UConstraint, FC)] (S.Set UConstraint)
39+
40+
41+solve :: Int -> [(UConstraint, FC)] -> TC (M.Map Var Int)
42+solve maxUniverseLevel inpConstraints =
43+ evalStateT (propagate >> extractSolution) initSolverState
44+
45+ where
46+
47+ -- | initial solver state.
48+ -- the queue contains all constraints, the domain store contains the initial domains.
49+ initSolverState :: SolverState
50+ initSolverState =
51+ let
52+ (initUnaryQueue, initQueue) = partition (\ (c,_) -> length (varsIn c) == 1) inpConstraints
53+ in
54+ SolverState
55+ { queue = Queue (initUnaryQueue ++ initQueue) (S.fromList (map fst (initUnaryQueue ++ initQueue)))
56+ , domainStore = M.fromList
57+ [ (v, (Domain 0 maxUniverseLevel, S.empty))
58+ | v <- ordNub [ v
59+ | (c, _) <- inpConstraints
60+ , v <- varsIn c
61+ ]
62+ ]
63+ }
64+
65+ -- | a map from variables to the list of constraints the variable occurs in.
66+ constraints :: M.Map Var (S.Set (UConstraint, FC))
67+ constraints = M.fromListWith S.union
68+ [ (v, S.singleton (c,fc))
69+ | (c, fc) <- inpConstraints
70+ , let vars = varsIn c
71+ , length vars > 1 -- do not register unary constraints
72+ , v <- vars
73+ ]
74+
75+ -- | this is where the actual work is done.
76+ -- dequeue the first constraint,
77+ -- filter domains,
78+ -- update domains (possibly resulting in a domain wipe out),
79+ -- until the queue is empty.
80+ propagate :: StateT SolverState TC ()
81+ propagate = do
82+ mcons <- nextConstraint
83+ case mcons of
84+ Nothing -> return ()
85+ Just (cons, fc) -> do
86+ case cons of
87+ ULE a b -> do
88+ Domain lowerA upperA <- domainOf a
89+ Domain lowerB upperB <- domainOf b
90+ when (upperB < upperA) $ updateDomainOf (cons, fc) a (Domain lowerA upperB)
91+ when (lowerA > lowerB) $ updateDomainOf (cons, fc) b (Domain lowerA upperB)
92+ ULT a b -> do
93+ Domain lowerA upperA <- domainOf a
94+ Domain lowerB upperB <- domainOf b
95+ let upperB_pred = pred upperB
96+ let lowerA_succ = succ lowerA
97+ when (upperB_pred < upperA) $ updateDomainOf (cons, fc) a (Domain lowerA upperB_pred)
98+ when (lowerA_succ > lowerB) $ updateDomainOf (cons, fc) b (Domain lowerA_succ upperB)
99+ propagate
100+
101+ -- | extract a solution from the state.
102+ extractSolution :: (MonadState SolverState m, Functor m) => m (M.Map Var Int)
103+ extractSolution = M.map (extractValue . fst) <$> gets domainStore
104+
105+ extractValue :: Domain -> Int
106+ extractValue (Domain x _) = x
107+
108+ -- | dequeue the first constraint.
109+ nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))
110+ nextConstraint = do
111+ Queue list set <- gets queue
112+ case list of
113+ [] -> return Nothing
114+ (q:qs) -> do
115+ modify $ \ st -> st { queue = Queue qs (S.delete (fst q) set) }
116+ return (Just q)
117+
118+ -- | look up the domain of a variable from the state.
119+ -- for convenience, this function also accepts UVal's and returns a singleton domain for them.
120+ domainOf :: MonadState SolverState m => UExp -> m Domain
121+ domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)
122+ domainOf (UVal val) = return (Domain val val)
123+
124+ -- | updates the domain of a variable.
125+ -- this function is also where we fail, inc ase of a domain wipe-out.
126+ updateDomainOf :: (UConstraint, FC) -> UExp -> Domain -> StateT SolverState TC ()
127+ updateDomainOf suspect (UVar var) newDom = do
128+ doms <- gets domainStore
129+ let (oldDom, suspects) = doms M.! Var var
130+ when (wipeOut newDom) $ lift $ Error $ At (snd suspect) $ Msg $ unlines
131+ $ "Universe inconsistency."
132+ : ("Working on: " ++ show (UVar var))
133+ : ("Old domain: " ++ show oldDom)
134+ : ("New domain: " ++ show newDom)
135+ : "Involved constraints: "
136+ : map (("\t"++) . show) (suspect : S.toList suspects)
137+ modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
138+ addToQueue (Var var)
139+ updateDomainOf _ UVal{} _ = return ()
140+
141+ -- | add all constraints related to a variable.
142+ addToQueue :: MonadState SolverState m => Var -> m ()
143+ addToQueue var =
144+ case M.lookup var constraints of
145+ Nothing -> return ()
146+ Just cs -> do
147+ Queue list set <- gets queue
148+ let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set ]
149+ if null newCons
150+ then return ()
151+ else modify $ \ st -> st { queue = Queue (list ++ newCons)
152+ (S.union set (S.fromList (map fst newCons))) }
153+
154+ -- | check if a domain is wiped out.
155+ wipeOut :: Domain -> Bool
156+ wipeOut (Domain l u) = l > u
157+
158+ordNub :: Ord a => [a] -> [a]
159+ordNub = S.toList . S.fromList
41160
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
161+-- | variables in a constraint
162+varsIn :: UConstraint -> [Var]
163+varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]
164+varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]