git.iko.soy/Idris-dev
on master help sign in
fancier queue implementation: the queue contains a set of constraints (without the FCs) so duplicate checking is a bit faster
d44a2dfOzgur Akgun
src/Idris/Core/Constraints.hs+35−20
compare with master
unifiedsplit
@@ -5,13 +5,15 @@ import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..), Err'(..) )
5
5
6import Control.Applicative
6import Control.Applicative
7import Control.Monad.State.Strict
7import Control.Monad.State.Strict
8+import Data.Function ( on )
9+import Data.List ( partition, nubBy )
8import qualified Data.Map.Strict as M
10import qualified Data.Map.Strict as M
9import qualified Data.Set as S
11import qualified Data.Set as S
10
12
11
13
12-- | Check that a list of universe constraints can be satisfied.
14-- | Check that a list of universe constraints can be satisfied.
13ucheck :: [(UConstraint, FC)] -> TC ()
15ucheck :: [(UConstraint, FC)] -> TC ()
14−ucheck = void . solve 10 . filter (not . ignore)
16+ucheck = void . solve 10 . nubBy ((==) `on` fst) . filter (not . ignore)
15 where
17 where
16 -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with
18 -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with
17 ignore (c,_) | any (== Var (-1)) (varsIn c) = True
19 ignore (c,_) | any (== Var (-1)) (varsIn c) = True
@@ -27,12 +29,15 @@ data Domain = Domain {-# UNPACK #-} !Int
27
29
28data SolverState =
30data SolverState =
29 SolverState
31 SolverState
30− { queue :: S.Set (UConstraint, FC)
32+ { queue :: Queue
31 , domainStore :: M.Map Var ( Domain
33 , domainStore :: M.Map Var ( Domain
32 , S.Set (UConstraint, FC) -- constraints that effected this variable
34 , S.Set (UConstraint, FC) -- constraints that effected this variable
33 )
35 )
34 }
36 }
35
37
38+data Queue = Queue [(UConstraint, FC)] (S.Set UConstraint)
39+
40+
36solve :: Int -> [(UConstraint, FC)] -> TC (M.Map Var Int)
41solve :: Int -> [(UConstraint, FC)] -> TC (M.Map Var Int)
37solve maxUniverseLevel inpConstraints =
42solve maxUniverseLevel inpConstraints =
38 evalStateT (propagate >> extractSolution) initSolverState
43 evalStateT (propagate >> extractSolution) initSolverState
@@ -42,21 +47,25 @@ solve maxUniverseLevel inpConstraints =
42 -- | initial solver state.
47 -- | initial solver state.
43 -- the queue contains all constraints, the domain store contains the initial domains.
48 -- the queue contains all constraints, the domain store contains the initial domains.
44 initSolverState :: SolverState
49 initSolverState :: SolverState
45− initSolverState = SolverState
50+ initSolverState =
46− { queue = S.fromList inpConstraints
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)))
47− , domainStore = M.fromList
56+ , domainStore = M.fromList
48− [ (v, (Domain 0 maxUniverseLevel, S.empty))
57+ [ (v, (Domain 0 maxUniverseLevel, S.empty))
49− | v <- ordNub [ v
58+ | v <- ordNub [ v
50− | (c, _) <- inpConstraints
59+ | (c, _) <- inpConstraints
51− , v <- varsIn c
60+ , v <- varsIn c
52− ]
61+ ]
53− ]
62+ ]
54− }
63+ }
55
64
56 -- | a map from variables to the list of constraints the variable occurs in.
65 -- | a map from variables to the list of constraints the variable occurs in.
57 constraints :: M.Map Var (S.Set (UConstraint, FC))
66 constraints :: M.Map Var (S.Set (UConstraint, FC))
58− constraints = M.map S.fromList $ M.fromListWith (++)
67+ constraints = M.fromListWith S.union
59− [ (v, [(c,fc)])
68+ [ (v, S.singleton (c,fc))
60 | (c, fc) <- inpConstraints
69 | (c, fc) <- inpConstraints
61 , let vars = varsIn c
70 , let vars = varsIn c
62 , length vars > 1 -- do not register unary constraints
71 , length vars > 1 -- do not register unary constraints
@@ -99,11 +108,11 @@ solve maxUniverseLevel inpConstraints =
99 -- | dequeue the first constraint.
108 -- | dequeue the first constraint.
100 nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))
109 nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))
101 nextConstraint = do
110 nextConstraint = do
102− qu <- gets queue
111+ Queue list set <- gets queue
103− case S.minView qu of
112+ case list of
104− Nothing -> return Nothing
113+ [] -> return Nothing
105− Just (q,qs) -> do
114+ (q:qs) -> do
106− modify $ \ st -> st { queue = qs }
115+ modify $ \ st -> st { queue = Queue qs (S.delete (fst q) set) }
107 return (Just q)
116 return (Just q)
108
117
109 -- | look up the domain of a variable from the state.
118 -- | look up the domain of a variable from the state.
@@ -134,7 +143,13 @@ solve maxUniverseLevel inpConstraints =
134 addToQueue var =
143 addToQueue var =
135 case M.lookup var constraints of
144 case M.lookup var constraints of
136 Nothing -> return ()
145 Nothing -> return ()
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 ()
137− Just cs -> modify $ \ st -> st { queue = S.union cs (queue st) }
151+ else modify $ \ st -> st { queue = Queue (list ++ newCons)
152+ (S.union set (S.fromList (map fst newCons))) }
138
153
139 -- | check if a domain is wiped out.
154 -- | check if a domain is wiped out.
140 wipeOut :: Domain -> Bool
155 wipeOut :: Domain -> Bool