@@ -5,7 +5,6 @@ import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..), Err'(..) )
6import Control.Applicative
6import Control.Applicative
7import Control.Monad.State
7import Control.Monad.State
9import qualified Data.Map.Strict as M
8import qualified Data.Map.Strict as M
10import qualified Data.Set as S
9import qualified Data.Set as S
@@ -23,9 +22,9 @@ type Domain = (Int, Int)
24data SolverState =
23data SolverState =
25 SolverState
24 SolverState
26− { queue :: [(UConstraint, FC)]
25+ { queue :: S.Set (UConstraint, FC)
27 , domainStore :: M.Map Var ( Domain
26 , domainStore :: M.Map Var ( Domain
28− , [(UConstraint, FC)] -- constraints that effected this variable
27+ , S.Set (UConstraint, FC) -- constraints that effected this variable
@@ -39,9 +38,9 @@ solve maxUniverseLevel inpConstraints =
39 -- the queue contains all constraints, the domain store contains the initial domains.
38 -- the queue contains all constraints, the domain store contains the initial domains.
40 initSolverState :: SolverState
39 initSolverState :: SolverState
41 initSolverState = SolverState
40 initSolverState = SolverState
42− { queue = ordNub inpConstraints
41+ { queue = S.fromList inpConstraints
43 , domainStore = M.fromList
42 , domainStore = M.fromList
44− [ (v, ((0, maxUniverseLevel), []))
43+ [ (v, ((0, maxUniverseLevel), S.empty))
45 | v <- ordNub [ v
44 | v <- ordNub [ v
46 | (c, _) <- inpConstraints
45 | (c, _) <- inpConstraints
47 , v <- varsIn c
46 , v <- varsIn c
@@ -50,8 +49,8 @@ solve maxUniverseLevel inpConstraints =
52 -- | a map from variables to the list of constraints the variable occurs in.
51 -- | a map from variables to the list of constraints the variable occurs in.
53− constraints :: M.Map Var [(UConstraint, FC)]
52+ constraints :: M.Map Var (S.Set (UConstraint, FC))
54− constraints = M.map ordNub $ M.fromListWith (++)
53+ constraints = M.map S.fromList $ M.fromListWith (++)
55 [ (v, [(c,fc)])
54 [ (v, [(c,fc)])
56 | (c, fc) <- inpConstraints
55 | (c, fc) <- inpConstraints
57 , v <- varsIn c
56 , v <- varsIn c
@@ -89,10 +88,10 @@ solve maxUniverseLevel inpConstraints =
89 nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))
88 nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))
90 nextConstraint = do
89 nextConstraint = do
91 qu <- gets queue
90 qu <- gets queue
92− case qu of
91+ case S.minView qu of
93− [] -> return Nothing
92+ Nothing -> return Nothing
94− (q:qs) -> do
93+ Just (q,qs) -> do
95− modify $ \ st -> st { queue = qs \\ [q] }
94+ modify $ \ st -> st { queue = qs }
96 return (Just q)
95 return (Just q)
98 -- | look up the domain of a variable from the state.
97 -- | look up the domain of a variable from the state.
@@ -111,7 +110,7 @@ solve maxUniverseLevel inpConstraints =
111 varsDoms <- mapM (\ (Var v) -> do
110 varsDoms <- mapM (\ (Var v) -> do
112 d <- domainOf (UVar v)
111 d <- domainOf (UVar v)
113 return (UVar v, d)
112 return (UVar v, d)
114− ) $ ordNub $ concatMap (varsIn . fst) (suspect : suspects)
113+ ) $ ordNub $ concatMap (varsIn . fst) (suspect : S.toList suspects)
115 when (wipeOut newDom) $ lift $ Error $ Msg $ unlines
114 when (wipeOut newDom) $ lift $ Error $ Msg $ unlines
116 $ "Universe inconsistency."
115 $ "Universe inconsistency."
117 : ("Working on: " ++ show (UVar var))
116 : ("Working on: " ++ show (UVar var))
@@ -119,13 +118,13 @@ solve maxUniverseLevel inpConstraints =
119 : ("Inp domain: " ++ show dom)
118 : ("Inp domain: " ++ show dom)
120 : ("New domain: " ++ show newDom)
119 : ("New domain: " ++ show newDom)
121 : "Involved constraints: "
120 : "Involved constraints: "
122− : map (("\t"++) . show) (suspect:suspects)
121+ : map (("\t"++) . show) (suspect : S.toList suspects)
123 ++ ["Involved variables: "]
122 ++ ["Involved variables: "]
124 ++ map (\ (v,d) -> "\t"++ show v ++ " = " ++ show d) varsDoms
123 ++ map (\ (v,d) -> "\t"++ show v ++ " = " ++ show d) varsDoms
125 -- ++ ["All constraints"]
124 -- ++ ["All constraints"]
126 -- ++ map (show . fst) inpConstraints
125 -- ++ map (show . fst) inpConstraints
127 unless (oldDom == newDom) $ do
126 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 }
129 addToQueue (Var var)
128 addToQueue (Var var)
130 updateDomainOf _ UVal{} _ = return ()
129 updateDomainOf _ UVal{} _ = return ()
@@ -133,7 +132,7 @@ solve maxUniverseLevel inpConstraints =
133 addToQueue :: MonadState SolverState m => Var -> m ()
132 addToQueue :: MonadState SolverState m => Var -> m ()
134 addToQueue var = do
133 addToQueue var = do
135 let cs = constraints M.! var
134 let cs = constraints M.! var
136− modify $ \ st -> st { queue = queue st ++ cs }
135+ modify $ \ st -> st { queue = S.union cs (queue st) }
138 -- | intersecting two domains, the resulting domain can be wiped out.
137 -- | intersecting two domains, the resulting domain can be wiped out.
139 domainIntersect :: (Int, Int) -> (Int, Int) -> (Int, Int)
138 domainIntersect :: (Int, Int) -> (Int, Int) -> (Int, Int)