git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/Core/Constraints.hs
223 lines 10 kB history raw
1-- | Check universe constraints.
2module Idris.Core.Constraints ( ucheck ) where
4import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..),
5 ConstraintFC(..), Err'(..) )
7import Control.Applicative
8import Control.Monad.State.Strict
9import Data.List ( partition )
10import qualified Data.Map.Strict as M
11import qualified Data.Set as S
14-- | Check that a list of universe constraints can be satisfied.
15ucheck :: S.Set ConstraintFC -> TC ()
16ucheck = void . solve 10 . S.filter (not . ignore)
17 where
18 -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with
19 ignore (ConstraintFC c _) | any (== Var (-1)) (varsIn c) = True
20 ignore (ConstraintFC (ULE a b) _) = a == b
21 ignore _ = False
23newtype Var = Var Int
24 deriving (Eq, Ord, Show)
26data Domain = Domain Int Int
27 deriving (Eq, Ord, Show)
29data SolverState =
30 SolverState
31 { queue :: Queue
32 , domainStore :: M.Map Var ( Domain
33 , S.Set ConstraintFC -- constraints that effected this variable
34 )
35 , cons_lhs :: M.Map Var (S.Set ConstraintFC)
36 , cons_rhs :: M.Map Var (S.Set ConstraintFC)
37 }
39data Queue = Queue [ConstraintFC] (S.Set UConstraint)
42solve :: Int -> S.Set ConstraintFC -> TC (M.Map Var Int)
43solve maxUniverseLevel ucs =
44 evalStateT (propagate >> extractSolution) initSolverState
46 where
47 inpConstraints = S.toAscList ucs
49 -- | initial solver state.
50 -- the queue contains all constraints, the domain store contains the initial domains.
51 initSolverState :: SolverState
52 initSolverState =
53 let
54 (initUnaryQueue, initQueue) = partition (\ c -> length (varsIn (uconstraint c)) == 1) inpConstraints
55 in
56 SolverState
57 { queue = Queue (initUnaryQueue ++ initQueue) (S.fromList (map uconstraint (initUnaryQueue ++ initQueue)))
58 , domainStore = M.fromList
59 [ (v, (Domain 0 maxUniverseLevel, S.empty))
60 | v <- ordNub [ v
61 | ConstraintFC c _ <- inpConstraints
62 , v <- varsIn c
63 ]
64 ]
65 , cons_lhs = constraintsLHS
66 , cons_rhs = constraintsRHS
67 }
69 lhs (ULT (UVar x) _) = Just (Var x)
70 lhs (ULE (UVar x) _) = Just (Var x)
71 lhs _ = Nothing
73 rhs (ULT _ (UVar x)) = Just (Var x)
74 rhs (ULE _ (UVar x)) = Just (Var x)
75 rhs _ = Nothing
77 -- | a map from variables to the list of constraints the variable occurs in. (in the LHS of a constraint)
78 constraintsLHS :: M.Map Var (S.Set ConstraintFC)
79 constraintsLHS = M.fromListWith S.union
80 [ (v, S.singleton (ConstraintFC c fc))
81 | (ConstraintFC c fc) <- inpConstraints
82 , let vars = varsIn c
83 , length vars > 1 -- do not register unary constraints
84 , v <- vars
85 , lhs c == Just v
86 ]
88 -- | a map from variables to the list of constraints the variable occurs in. (in the RHS of a constraint)
89 constraintsRHS :: M.Map Var (S.Set ConstraintFC)
90 constraintsRHS = M.fromListWith S.union
91 [ (v, S.singleton (ConstraintFC c fc))
92 | (ConstraintFC c fc) <- inpConstraints
93 , let vars = varsIn c
94 , length vars > 1 -- do not register unary constraints
95 , v <- vars
96 , rhs c == Just v
97 ]
99 -- | this is where the actual work is done.
100 -- dequeue the first constraint,
101 -- filter domains,
102 -- update domains (possibly resulting in a domain wipe out),
103 -- until the queue is empty.
104 propagate :: StateT SolverState TC ()
105 propagate = do
106 mcons <- nextConstraint
107 case mcons of
108 Nothing -> return ()
109 Just (ConstraintFC cons fc) -> do
110 case cons of
111 ULE a b -> do
112 Domain lowerA upperA <- domainOf a
113 Domain lowerB upperB <- domainOf b
114 when (upperB < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB
115 when (lowerA > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA
116 ULT a b -> do
117 Domain lowerA upperA <- domainOf a
118 Domain lowerB upperB <- domainOf b
119 let upperB_pred = pred upperB
120 let lowerA_succ = succ lowerA
121 when (upperB_pred < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB_pred
122 when (lowerA_succ > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA_succ
123 propagate
125 -- | extract a solution from the state.
126 extractSolution :: (MonadState SolverState m, Functor m) => m (M.Map Var Int)
127 extractSolution = M.map (extractValue . fst) <$> gets domainStore
129 extractValue :: Domain -> Int
130 extractValue (Domain x _) = x
132 -- | dequeue the first constraint.
133 nextConstraint :: MonadState SolverState m => m (Maybe ConstraintFC)
134 nextConstraint = do
135 Queue list set <- gets queue
136 case list of
137 [] -> return Nothing
138 (q:qs) -> do
139 modify $ \ st -> st { queue = Queue qs (S.delete (uconstraint q) set) }
140 return (Just q)
142 -- | look up the domain of a variable from the state.
143 -- for convenience, this function also accepts UVal's and returns a singleton domain for them.
144 domainOf :: MonadState SolverState m => UExp -> m Domain
145 domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)
146 domainOf (UVal val) = return (Domain val val)
148 updateUpperBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
149 updateUpperBoundOf suspect (UVar var) upper = do
150 doms <- gets domainStore
151 let (oldDom@(Domain lower _), suspects) = doms M.! Var var
152 let newDom = Domain lower upper
153 when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines
154 $ "Universe inconsistency."
155 : ("Working on: " ++ show (UVar var))
156 : ("Old domain: " ++ show oldDom)
157 : ("New domain: " ++ show newDom)
158 : "Involved constraints: "
159 : map (("\t"++) . show) (suspect : S.toList suspects)
160 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
161 addToQueueRHS (uconstraint suspect) (Var var)
162 updateUpperBoundOf _ UVal{} _ = return ()
164 updateLowerBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
165 updateLowerBoundOf suspect (UVar var) lower = do
166 doms <- gets domainStore
167 let (oldDom@(Domain _ upper), suspects) = doms M.! Var var
168 let newDom = Domain lower upper
169 when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines
170 $ "Universe inconsistency."
171 : ("Working on: " ++ show (UVar var))
172 : ("Old domain: " ++ show oldDom)
173 : ("New domain: " ++ show newDom)
174 : "Involved constraints: "
175 : map (("\t"++) . show) (suspect : S.toList suspects)
176 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
177 addToQueueLHS (uconstraint suspect) (Var var)
178 updateLowerBoundOf _ UVal{} _ = return ()
180 -- | add all constraints (with the given var on the lhs) to the queue
181 addToQueueLHS :: MonadState SolverState m => UConstraint -> Var -> m ()
182 addToQueueLHS thisCons var = do
183 clhs <- gets cons_lhs
184 case M.lookup var clhs of
185 Nothing -> return ()
186 Just cs -> do
187 Queue list set <- gets queue
188 let set' = S.insert thisCons set
189 let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]
190 if null newCons
191 then return ()
192 else modify $ \ st -> st { queue = Queue (list ++ newCons)
193 (S.union set (S.fromList (map uconstraint newCons))) }
195 -- | add all constraints (with the given var on the rhs) to the queue
196 addToQueueRHS :: MonadState SolverState m => UConstraint -> Var -> m ()
197 addToQueueRHS thisCons var = do
198 crhs <- gets cons_rhs
199 case M.lookup var crhs of
200 Nothing -> return ()
201 Just cs -> do
202 Queue list set <- gets queue
203 let set' = S.insert thisCons set
204 let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]
205 if null newCons
206 then return ()
207 else modify $ \ st -> st { queue = Queue (list ++ newCons)
208 (insertAll (map uconstraint newCons) set) }
210 insertAll [] s = s
211 insertAll (x : xs) s = insertAll xs (S.insert x s)
213 -- | check if a domain is wiped out.
214 wipeOut :: Domain -> Bool
215 wipeOut (Domain l u) = l > u
217ordNub :: Ord a => [a] -> [a]
218ordNub = S.toList . S.fromList
220-- | variables in a constraint
221varsIn :: UConstraint -> [Var]
222varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]
223varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]