on master help sign in
Cache constraint set in solver state

This way we don't need to recompute it all the time and it runs much faster.

commit9dc7105748fad1370a2d568e1408fa7d89a1ee5e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 22 Mar 2015, 21:25 (12 years ago) parent83ff2b6
1 file changed+10−4
src/Idris/Core/Constraints.hs+10−4
src/Idris/Core/Constraints.hs+10−4
@@ -32,6 +32,8 @@ data SolverState =
3232 , domainStore :: M.Map Var ( Domain
3333 , S.Set ConstraintFC -- constraints that effected this variable
3434 )
35+ , cons_lhs :: M.Map Var (S.Set ConstraintFC)
36+ , cons_rhs :: M.Map Var (S.Set ConstraintFC)
3537 }
3638
3739data Queue = Queue [ConstraintFC] (S.Set UConstraint)
@@ -60,6 +62,8 @@ solve maxUniverseLevel ucs =
6062 , v <- varsIn c
6163 ]
6264 ]
65+ , cons_lhs = constraintsLHS
66+ , cons_rhs = constraintsRHS
6367 }
6468
6569 lhs (ULT (UVar x) _) = Just (Var x)
@@ -175,8 +179,9 @@ solve maxUniverseLevel ucs =
175179
176180 -- | add all constraints (with the given var on the lhs) to the queue
177181 addToQueueLHS :: MonadState SolverState m => UConstraint -> Var -> m ()
178− addToQueueLHS thisCons var =
179− case M.lookup var constraintsLHS of
182+ addToQueueLHS thisCons var = do
183+ clhs <- gets cons_lhs
184+ case M.lookup var clhs of
180185 Nothing -> return ()
181186 Just cs -> do
182187 Queue list set <- gets queue
@@ -189,8 +194,9 @@ solve maxUniverseLevel ucs =
189194
190195 -- | add all constraints (with the given var on the rhs) to the queue
191196 addToQueueRHS :: MonadState SolverState m => UConstraint -> Var -> m ()
192− addToQueueRHS thisCons var =
193− case M.lookup var constraintsRHS of
197+ addToQueueRHS thisCons var = do
198+ crhs <- gets cons_rhs
199+ case M.lookup var crhs of
194200 Nothing -> return ()
195201 Just cs -> do
196202 Queue list set <- gets queue