@@ -5,13 +5,15 @@ import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..), Err'(..) )
55
66import Control.Applicative
77import Control.Monad.State.Strict
8+import Data.Function ( on )
9+import Data.List ( partition, nubBy )
810import qualified Data.Map.Strict as M
911import qualified Data.Set as S
1012
1113
1214-- | Check that a list of universe constraints can be satisfied.
1315ucheck :: [(UConstraint, FC)] -> TC ()
14−ucheck = void . solve 10 . filter (not . ignore)
16+ucheck = void . solve 10 . nubBy ((==) `on` fst) . filter (not . ignore)
1517 where
1618 -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with
1719 ignore (c,_) | any (== Var (-1)) (varsIn c) = True
@@ -27,12 +29,15 @@ data Domain = Domain {-# UNPACK #-} !Int
2729
2830data SolverState =
2931 SolverState
30− { queue :: S.Set (UConstraint, FC)
32+ { queue :: Queue
3133 , domainStore :: M.Map Var ( Domain
3234 , S.Set (UConstraint, FC) -- constraints that effected this variable
3335 )
3436 }
3537
38+data Queue = Queue [(UConstraint, FC)] (S.Set UConstraint)
39+
40+
3641solve :: Int -> [(UConstraint, FC)] -> TC (M.Map Var Int)
3742solve maxUniverseLevel inpConstraints =
3843 evalStateT (propagate >> extractSolution) initSolverState
@@ -42,21 +47,25 @@ solve maxUniverseLevel inpConstraints =
4247 -- | initial solver state.
4348 -- the queue contains all constraints, the domain store contains the initial domains.
4449 initSolverState :: SolverState
45− initSolverState = SolverState
46− { queue = S.fromList inpConstraints
47− , domainStore = M.fromList
48− [ (v, (Domain 0 maxUniverseLevel, S.empty))
49− | v <- ordNub [ v
50− | (c, _) <- inpConstraints
51− , v <- varsIn c
52− ]
53− ]
54− }
50+ initSolverState =
51+ let
52+ (initUnaryQueue, initQueue) = partition (\ (c,_) -> length (varsIn c) == 1) inpConstraints
53+ in
54+ SolverState
55+ { queue = Queue (initUnaryQueue ++ initQueue) (S.fromList (map fst (initUnaryQueue ++ initQueue)))
56+ , domainStore = M.fromList
57+ [ (v, (Domain 0 maxUniverseLevel, S.empty))
58+ | v <- ordNub [ v
59+ | (c, _) <- inpConstraints
60+ , v <- varsIn c
61+ ]
62+ ]
63+ }
5564
5665 -- | a map from variables to the list of constraints the variable occurs in.
5766 constraints :: M.Map Var (S.Set (UConstraint, FC))
58− constraints = M.map S.fromList $ M.fromListWith (++)
59− [ (v, [(c,fc)])
67+ constraints = M.fromListWith S.union
68+ [ (v, S.singleton (c,fc))
6069 | (c, fc) <- inpConstraints
6170 , let vars = varsIn c
6271 , length vars > 1 -- do not register unary constraints
@@ -99,11 +108,11 @@ solve maxUniverseLevel inpConstraints =
99108 -- | dequeue the first constraint.
100109 nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))
101110 nextConstraint = do
102− qu <- gets queue
103− case S.minView qu of
104− Nothing -> return Nothing
105− Just (q,qs) -> do
106− modify $ \ st -> st { queue = qs }
111+ Queue list set <- gets queue
112+ case list of
113+ [] -> return Nothing
114+ (q:qs) -> do
115+ modify $ \ st -> st { queue = Queue qs (S.delete (fst q) set) }
107116 return (Just q)
108117
109118 -- | look up the domain of a variable from the state.
@@ -134,7 +143,13 @@ solve maxUniverseLevel inpConstraints =
134143 addToQueue var =
135144 case M.lookup var constraints of
136145 Nothing -> return ()
137− Just cs -> modify $ \ st -> st { queue = S.union cs (queue st) }
146+ Just cs -> do
147+ Queue list set <- gets queue
148+ let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set ]
149+ if null newCons
150+ then return ()
151+ else modify $ \ st -> st { queue = Queue (list ++ newCons)
152+ (S.union set (S.fromList (map fst newCons))) }
138153
139154 -- | check if a domain is wiped out.
140155 wipeOut :: Domain -> Bool