@@ -5,7 +5,6 @@ import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..), Err'(..) )
55
66import Control.Applicative
77import Control.Monad.State
8−import Data.List
98import qualified Data.Map.Strict as M
109import qualified Data.Set as S
1110
@@ -23,9 +22,9 @@ type Domain = (Int, Int)
2322
2423data SolverState =
2524 SolverState
26− { queue :: [(UConstraint, FC)]
25+ { queue :: S.Set (UConstraint, FC)
2726 , domainStore :: M.Map Var ( Domain
28− , [(UConstraint, FC)] -- constraints that effected this variable
27+ , S.Set (UConstraint, FC) -- constraints that effected this variable
2928 )
3029 }
3130
@@ -39,9 +38,9 @@ solve maxUniverseLevel inpConstraints =
3938 -- the queue contains all constraints, the domain store contains the initial domains.
4039 initSolverState :: SolverState
4140 initSolverState = SolverState
42− { queue = ordNub inpConstraints
41+ { queue = S.fromList inpConstraints
4342 , domainStore = M.fromList
44− [ (v, ((0, maxUniverseLevel), []))
43+ [ (v, ((0, maxUniverseLevel), S.empty))
4544 | v <- ordNub [ v
4645 | (c, _) <- inpConstraints
4746 , v <- varsIn c
@@ -50,8 +49,8 @@ solve maxUniverseLevel inpConstraints =
5049 }
5150
5251 -- | a map from variables to the list of constraints the variable occurs in.
53− constraints :: M.Map Var [(UConstraint, FC)]
54− constraints = M.map ordNub $ M.fromListWith (++)
52+ constraints :: M.Map Var (S.Set (UConstraint, FC))
53+ constraints = M.map S.fromList $ M.fromListWith (++)
5554 [ (v, [(c,fc)])
5655 | (c, fc) <- inpConstraints
5756 , v <- varsIn c
@@ -89,10 +88,10 @@ solve maxUniverseLevel inpConstraints =
8988 nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))
9089 nextConstraint = do
9190 qu <- gets queue
92− case qu of
93− [] -> return Nothing
94− (q:qs) -> do
95− modify $ \ st -> st { queue = qs \\ [q] }
91+ case S.minView qu of
92+ Nothing -> return Nothing
93+ Just (q,qs) -> do
94+ modify $ \ st -> st { queue = qs }
9695 return (Just q)
9796
9897 -- | look up the domain of a variable from the state.
@@ -111,7 +110,7 @@ solve maxUniverseLevel inpConstraints =
111110 varsDoms <- mapM (\ (Var v) -> do
112111 d <- domainOf (UVar v)
113112 return (UVar v, d)
114− ) $ ordNub $ concatMap (varsIn . fst) (suspect : suspects)
113+ ) $ ordNub $ concatMap (varsIn . fst) (suspect : S.toList suspects)
115114 when (wipeOut newDom) $ lift $ Error $ Msg $ unlines
116115 $ "Universe inconsistency."
117116 : ("Working on: " ++ show (UVar var))
@@ -119,13 +118,13 @@ solve maxUniverseLevel inpConstraints =
119118 : ("Inp domain: " ++ show dom)
120119 : ("New domain: " ++ show newDom)
121120 : "Involved constraints: "
122− : map (("\t"++) . show) (suspect:suspects)
121+ : map (("\t"++) . show) (suspect : S.toList suspects)
123122 ++ ["Involved variables: "]
124123 ++ map (\ (v,d) -> "\t"++ show v ++ " = " ++ show d) varsDoms
125124 -- ++ ["All constraints"]
126125 -- ++ map (show . fst) inpConstraints
127126 unless (oldDom == newDom) $ do
128− modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, suspect:suspects) doms }
127+ modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
129128 addToQueue (Var var)
130129 updateDomainOf _ UVal{} _ = return ()
131130
@@ -133,7 +132,7 @@ solve maxUniverseLevel inpConstraints =
133132 addToQueue :: MonadState SolverState m => Var -> m ()
134133 addToQueue var = do
135134 let cs = constraints M.! var
136− modify $ \ st -> st { queue = queue st ++ cs }
135+ modify $ \ st -> st { queue = S.union cs (queue st) }
137136
138137 -- | intersecting two domains, the resulting domain can be wiped out.
139138 domainIntersect :: (Int, Int) -> (Int, Int) -> (Int, Int)