git.iko.soy/Idris-dev
on 1b71663 help sign in
Idris-dev/src/Idris/Core/Constraints.hs
256 lines 11 kB history raw
1{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses #-}
2{-|
3Module : Idris.Core.Constraints
4Description : Check universe constraints.
6License : BSD3
7Maintainer : The Idris Community.
8-}
9module Idris.Core.Constraints ( ucheck ) where
11import Idris.Core.TT (ConstraintFC(..), Err'(..), TC(..), UConstraint(..),
12 UExp(..))
14import Control.Monad.State.Strict
15import Data.List (partition)
16import qualified Data.Map.Strict as M
17import qualified Data.Set as S
19-- | Check that a list of universe constraints can be satisfied.
20ucheck :: S.Set ConstraintFC -> TC ()
21ucheck = void . solve 10 . S.filter (not . ignore) . dropUnused
22 where
23 -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with
24 ignore (ConstraintFC c _) | any (== Var [] (-1)) (varsIn c) = True
25 ignore (ConstraintFC (ULE a b) _) = a == b
26 ignore _ = False
28dropUnused :: S.Set ConstraintFC -> S.Set ConstraintFC
29dropUnused xs = let cs = S.toList xs
30 onlhs = countLHS M.empty cs in
31 addIfUsed S.empty onlhs cs
32 where
33 -- Count the number of times a variable occurs on the LHS of a constraint
34 countLHS ms [] = ms
35 countLHS ms (c : cs) = let lhvar = getLHS (uconstraint c)
36 num = case M.lookup lhvar ms of
37 Nothing -> 1
38 Just v -> v + 1 in
39 countLHS (M.insert lhvar num ms) cs
41 -- Only keep a constraint if the variable on the RHS is used elsewhere
42 -- on the LHS of a constraint
43 addIfUsed cs' lhs [] = cs'
44 addIfUsed cs' lhs (c : cs)
45 = let rhvar = getRHS (uconstraint c) in
46 case M.lookup rhvar lhs of
47 Nothing -> addIfUsed cs' lhs cs
48 Just v -> addIfUsed (S.insert c cs') lhs cs
50 getLHS (ULT x _) = x
51 getLHS (ULE x _) = x
53 getRHS (ULT _ x) = x
54 getRHS (ULE _ x) = x
57data Var = Var String Int
58 deriving (Eq, Ord, Show)
60data Domain = Domain Int Int
61 deriving (Eq, Ord, Show)
63data SolverState =
64 SolverState
65 { queue :: Queue
66 , domainStore :: M.Map Var ( Domain
67 , S.Set ConstraintFC -- constraints that effected this variable
68 )
69 , cons_lhs :: M.Map Var (S.Set ConstraintFC)
70 , cons_rhs :: M.Map Var (S.Set ConstraintFC)
71 }
73data Queue = Queue [ConstraintFC] (S.Set UConstraint)
76solve :: Int -> S.Set ConstraintFC -> TC (M.Map Var Int)
77solve maxUniverseLevel ucs =
78 evalStateT (propagate >> extractSolution) initSolverState
80 where
81 inpConstraints = S.toAscList ucs
83 -- | initial solver state.
84 -- the queue contains all constraints, the domain store contains the initial domains.
85 initSolverState :: SolverState
86 initSolverState =
87 let
88 (initUnaryQueue, initQueue) = partition (\ c -> length (varsIn (uconstraint c)) == 1) inpConstraints
89 in
90 SolverState
91 { queue = Queue (initUnaryQueue ++ initQueue) (S.fromList (map uconstraint (initUnaryQueue ++ initQueue)))
92 , domainStore = M.fromList
93 [ (v, (Domain 0 maxUniverseLevel, S.empty))
94 | v <- ordNub [ v
95 | ConstraintFC c _ <- inpConstraints
96 , v <- varsIn c
97 ]
98 ]
99 , cons_lhs = constraintsLHS
100 , cons_rhs = constraintsRHS
101 }
103 lhs (ULT (UVar ns x) _) = Just (Var ns x)
104 lhs (ULE (UVar ns x) _) = Just (Var ns x)
105 lhs _ = Nothing
107 rhs (ULT _ (UVar ns x)) = Just (Var ns x)
108 rhs (ULE _ (UVar ns x)) = Just (Var ns x)
109 rhs _ = Nothing
111 -- | a map from variables to the list of constraints the variable occurs in. (in the LHS of a constraint)
112 constraintsLHS :: M.Map Var (S.Set ConstraintFC)
113 constraintsLHS = M.fromListWith S.union
114 [ (v, S.singleton (ConstraintFC c fc))
115 | (ConstraintFC c fc) <- inpConstraints
116 , let vars = varsIn c
117 , length vars > 1 -- do not register unary constraints
118 , v <- vars
119 , lhs c == Just v
120 ]
122 -- | a map from variables to the list of constraints the variable occurs in. (in the RHS of a constraint)
123 constraintsRHS :: M.Map Var (S.Set ConstraintFC)
124 constraintsRHS = M.fromListWith S.union
125 [ (v, S.singleton (ConstraintFC c fc))
126 | (ConstraintFC c fc) <- inpConstraints
127 , let vars = varsIn c
128 , length vars > 1 -- do not register unary constraints
129 , v <- vars
130 , rhs c == Just v
131 ]
133 -- | this is where the actual work is done.
134 -- dequeue the first constraint,
135 -- filter domains,
136 -- update domains (possibly resulting in a domain wipe out),
137 -- until the queue is empty.
138 propagate :: StateT SolverState TC ()
139 propagate = do
140 mcons <- nextConstraint
141 case mcons of
142 Nothing -> return ()
143 Just (ConstraintFC cons fc) -> do
144 case cons of
145 ULE a b -> do
146 Domain lowerA upperA <- domainOf a
147 Domain lowerB upperB <- domainOf b
148 when (upperB < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB
149 when (lowerA > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA
150 ULT a b -> do
151 Domain lowerA upperA <- domainOf a
152 Domain lowerB upperB <- domainOf b
153 let upperB_pred = pred upperB
154 let lowerA_succ = succ lowerA
155 when (upperB_pred < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB_pred
156 when (lowerA_succ > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA_succ
157 propagate
159 -- | extract a solution from the state.
160 extractSolution :: (MonadState SolverState m, Functor m) => m (M.Map Var Int)
161 extractSolution = M.map (extractValue . fst) <$> gets domainStore
163 extractValue :: Domain -> Int
164 extractValue (Domain x _) = x
166 -- | dequeue the first constraint.
167 nextConstraint :: MonadState SolverState m => m (Maybe ConstraintFC)
168 nextConstraint = do
169 Queue list set <- gets queue
170 case list of
171 [] -> return Nothing
172 (q:qs) -> do
173 modify $ \ st -> st { queue = Queue qs (S.delete (uconstraint q) set) }
174 return (Just q)
176 -- | look up the domain of a variable from the state.
177 -- for convenience, this function also accepts UVal's and returns a singleton domain for them.
178 domainOf :: MonadState SolverState m => UExp -> m Domain
179 domainOf (UVar ns var) = gets (fst . (M.! Var ns var) . domainStore)
180 domainOf (UVal val) = return (Domain val val)
182 asPair :: Domain -> (Int, Int)
183 asPair (Domain x y) = (x, y)
185 updateUpperBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
186 updateUpperBoundOf suspect (UVar ns var) upper = do
187 doms <- gets domainStore
188 let (oldDom@(Domain lower _), suspects) = doms M.! Var ns var
189 let newDom = Domain lower upper
190 when (wipeOut newDom) $
191 lift $ Error $
192 UniverseError (ufc suspect) (UVar ns var)
193 (asPair oldDom) (asPair newDom)
194 (suspect : S.toList suspects)
195 modify $ \ st -> st { domainStore = M.insert (Var ns var) (newDom, S.insert suspect suspects) doms }
196 addToQueueRHS (uconstraint suspect) (Var ns var)
197 updateUpperBoundOf _ UVal{} _ = return ()
199 updateLowerBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
200 updateLowerBoundOf suspect (UVar ns var) lower = do
201 doms <- gets domainStore
202 let (oldDom@(Domain _ upper), suspects) = doms M.! Var ns var
203 let newDom = Domain lower upper
204 when (wipeOut newDom) $
205 lift $ Error $
206 UniverseError (ufc suspect) (UVar ns var)
207 (asPair oldDom) (asPair newDom)
208 (suspect : S.toList suspects)
209 modify $ \ st -> st { domainStore = M.insert (Var ns var) (newDom, S.insert suspect suspects) doms }
210 addToQueueLHS (uconstraint suspect) (Var ns var)
211 updateLowerBoundOf _ UVal{} _ = return ()
213 -- | add all constraints (with the given var on the lhs) to the queue
214 addToQueueLHS :: MonadState SolverState m => UConstraint -> Var -> m ()
215 addToQueueLHS thisCons var = do
216 clhs <- gets cons_lhs
217 case M.lookup var clhs of
218 Nothing -> return ()
219 Just cs -> do
220 Queue list set <- gets queue
221 let set' = S.insert thisCons set
222 let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]
223 if null newCons
224 then return ()
225 else modify $ \ st -> st { queue = Queue (list ++ newCons)
226 (S.union set (S.fromList (map uconstraint newCons))) }
228 -- | add all constraints (with the given var on the rhs) to the queue
229 addToQueueRHS :: MonadState SolverState m => UConstraint -> Var -> m ()
230 addToQueueRHS thisCons var = do
231 crhs <- gets cons_rhs
232 case M.lookup var crhs of
233 Nothing -> return ()
234 Just cs -> do
235 Queue list set <- gets queue
236 let set' = S.insert thisCons set
237 let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]
238 if null newCons
239 then return ()
240 else modify $ \ st -> st { queue = Queue (list ++ newCons)
241 (insertAll (map uconstraint newCons) set) }
243 insertAll [] s = s
244 insertAll (x : xs) s = insertAll xs (S.insert x s)
246 -- | check if a domain is wiped out.
247 wipeOut :: Domain -> Bool
248 wipeOut (Domain l u) = l > u
250ordNub :: Ord a => [a] -> [a]
251ordNub = S.toList . S.fromList
253-- | variables in a constraint
254varsIn :: UConstraint -> [Var]
255varsIn (ULT a b) = [ Var ns v | UVar ns v <- [a,b] ]
256varsIn (ULE a b) = [ Var ns v | UVar ns v <- [a,b] ]