on master help sign in
avoiding repeated checks
commitee4d1cb77cb0ec132b87a6fa8a27f2d9c40a5867 authorOzgur Akgun <ozgurakgun@gmail.com> dateThu 19 Mar 2015, 23:37 (12 years ago) parent22914ec
1 file changed+9−14
src/Idris/Core/Constraints.hs+9−14
src/Idris/Core/Constraints.hs+9−14
@@ -73,13 +73,15 @@ solve maxUniverseLevel inpConstraints =
7373 ULE a b -> do
7474 (lowerA, upperA) <- domainOf a
7575 (lowerB, upperB) <- domainOf b
76− updateDomainOf (cons, fc) a (lowerA, min upperA upperB)
77− updateDomainOf (cons, fc) b (max lowerB lowerA, upperB)
76+ when (upperB < upperA) $ updateDomainOf (cons, fc) a (lowerA, upperB)
77+ when (lowerA > lowerB) $ updateDomainOf (cons, fc) b (lowerA, upperB)
7878 ULT a b -> do
7979 (lowerA, upperA) <- domainOf a
8080 (lowerB, upperB) <- domainOf b
81− updateDomainOf (cons, fc) a (lowerA, min upperA (pred upperB))
82− updateDomainOf (cons, fc) b (max lowerB (succ lowerA), upperB)
81+ let upperB_pred = pred upperB
82+ let lowerA_succ = succ lowerA
83+ when (upperB_pred < upperA) $ updateDomainOf (cons, fc) a (lowerA, upperB_pred)
84+ when (lowerA_succ > lowerB) $ updateDomainOf (cons, fc) b (lowerA_succ, upperB)
8385 propagate
8486
8587 -- | extract a solution from the state.
@@ -105,21 +107,18 @@ solve maxUniverseLevel inpConstraints =
105107 -- | updates the domain of a variable.
106108 -- this function is also where we fail, inc ase of a domain wipe-out.
107109 updateDomainOf :: (UConstraint, FC) -> UExp -> (Int, Int) -> StateT SolverState TC ()
108− updateDomainOf suspect (UVar var) dom = do
110+ updateDomainOf suspect (UVar var) newDom = do
109111 doms <- gets domainStore
110112 let (oldDom, suspects) = doms M.! Var var
111− let newDom = domainIntersect oldDom dom
112113 when (wipeOut newDom) $ lift $ Error $ Msg $ unlines
113114 $ "Universe inconsistency."
114115 : ("Working on: " ++ show (UVar var))
115116 : ("Old domain: " ++ show oldDom)
116− : ("Inp domain: " ++ show dom)
117117 : ("New domain: " ++ show newDom)
118118 : "Involved constraints: "
119119 : map (("\t"++) . show) (suspect : S.toList suspects)
120− unless (oldDom == newDom) $ do
121− modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
122− addToQueue (Var var)
120+ modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
121+ addToQueue (Var var)
123122 updateDomainOf _ UVal{} _ = return ()
124123
125124 -- | add all constraints related to a variable.
@@ -129,10 +128,6 @@ solve maxUniverseLevel inpConstraints =
129128 Nothing -> return ()
130129 Just cs -> modify $ \ st -> st { queue = S.union cs (queue st) }
131130
132− -- | intersecting two domains, the resulting domain can be wiped out.
133− domainIntersect :: (Int, Int) -> (Int, Int) -> (Int, Int)
134− domainIntersect (a,b) (c,d) = (max a c, min b d)
135−
136131 -- | check if a domain is wiped out.
137132 wipeOut :: (Int, Int) -> Bool
138133 wipeOut (l, u) = l > u