@@ -20,15 +20,21 @@ import Debug.Trace
2020
2121-- | Check that a list of universe constraints can be satisfied.
2222ucheck :: [(UConstraint, FC)] -> TC ()
23−ucheck = void . solve
23+ucheck = void . solve . filter (not . ignore)
24+ where ignore (c,_) = any (== Var (-1)) (varsIn c)
25+ -- TODO: remove the ignore when Idris.Core.Binary:598
2426
2527newtype Var = Var Int
2628 deriving (Eq, Ord, Show)
2729
30+type Domain = (Int, Int)
31+
2832data SolverState =
2933 SolverState
3034 { queue :: [(UConstraint, FC)]
31− , domainStore :: M.Map Var (Int, Int)
35+ , domainStore :: M.Map Var ( Domain
36+ , [(UConstraint, FC)] -- constraints that effected this variable
37+ )
3238 }
3339
3440solve :: [(UConstraint, FC)] -> TC (M.Map Var Int)
@@ -40,7 +46,7 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
4046 initSolverState = SolverState
4147 { queue = inpConstraints
4248 , domainStore = M.fromList
43− [ (v, (0, 10))
49+ [ (v, ((0, 10), []))
4450 | v <- ordNub [ v
4551 | (c, _) <- inpConstraints
4652 , v <- varsIn c
@@ -55,31 +61,27 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
5561 , v <- varsIn c
5662 ]
5763
58− varsIn :: UConstraint -> [Var]
59− varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]
60− varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]
61−
6264 -- propagate :: MonadState SolverState m => m ()
6365 propagate = do
6466 mcons <- nextConstraint
6567 case mcons of
6668 Nothing -> return ()
67− Just (cons, _fc) -> do
69+ Just (cons, fc) -> do
6870 case cons of
6971 ULE a b -> do
7072 (lowerA, upperA) <- domainOf a
7173 (lowerB, upperB) <- domainOf b
72− updateDomainOf a (lowerA, min upperA upperB)
73− updateDomainOf b (max lowerB lowerA, upperB)
74+ updateDomainOf (cons, fc) a (lowerA, min upperA upperB)
75+ updateDomainOf (cons, fc) b (max lowerB lowerA, upperB)
7476 ULT a b -> do
7577 (lowerA, upperA) <- domainOf a
7678 (lowerB, upperB) <- domainOf b
77− updateDomainOf a (lowerA, min upperA (pred upperB))
78− updateDomainOf b (max lowerB (succ lowerA), upperB)
79+ updateDomainOf (cons, fc) a (lowerA, min upperA (pred upperB))
80+ updateDomainOf (cons, fc) b (max lowerB (succ lowerA), upperB)
7981 propagate
8082
8183 extractSolution :: (MonadState SolverState m, Functor m) => m (M.Map Var Int)
82− extractSolution = M.map fst <$> gets domainStore
84+ extractSolution = M.map (fst . fst) <$> gets domainStore
8385
8486 nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))
8587 nextConstraint = do
@@ -91,19 +93,34 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
9193 return (Just q)
9294
9395 domainOf :: MonadState SolverState m => UExp -> m (Int, Int)
94− domainOf (UVar var) = gets ((M.! Var var) . domainStore)
96+ domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)
9597 domainOf (UVal val) = return (val, val)
9698
97− -- updateDomainOf :: MonadState SolverState m => UExp -> (Int, Int) -> m ()
98− updateDomainOf (UVar var) dom = do
99+ -- updateDomainOf :: MonadState SolverState m => UConstraint -> UExp -> (Int, Int) -> m ()
100+ updateDomainOf suspect (UVar var) dom = do
99101 doms <- gets domainStore
100− let oldDom = doms M.! Var var
102+ let (oldDom, suspects) = doms M.! Var var
101103 let newDom = domainIntersect oldDom dom
102− when (wipeOut newDom) $ lift $ Error UniverseError
104+ varsDoms <- mapM (\ (Var v) -> do
105+ d <- domainOf (UVar v)
106+ return (UVar v, d)
107+ ) $ ordNub $ concatMap (varsIn . fst) (suspect : suspects)
108+ when (wipeOut newDom) $ lift $ Error $ Msg $ unlines
109+ $ "Universe inconsistency."
110+ : ("Working on: " ++ show (UVar var))
111+ : ("Old domain: " ++ show oldDom)
112+ : ("Inp domain: " ++ show dom)
113+ : ("New domain: " ++ show newDom)
114+ : "Involved constraints: "
115+ : map (("\t"++) . show) (suspect:suspects)
116+ ++ ["Involved variables: "]
117+ ++ map (\ (v,d) -> "\t"++ show v ++ " = " ++ show d) varsDoms
118+ -- ++ ["All constraints"]
119+ -- ++ map (show . fst) inpConstraints
103120 unless (oldDom == newDom) $ do
104− modify $ \ st -> st { domainStore = M.insert (Var var) newDom doms }
121+ modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, suspect:suspects) doms }
105122 addToQueue (Var var)
106− updateDomainOf UVal{} _ = return ()
123+ updateDomainOf _ UVal{} _ = return ()
107124
108125 -- addToQueue :: MonadState SolverState m => Var -> m ()
109126 addToQueue var = do
@@ -118,3 +135,7 @@ solve inpConstraints = evalStateT (propagate >> extractSolution) initSolverState
118135
119136ordNub :: Ord a => [a] -> [a]
120137ordNub = S.toList . S.fromList
138+
139+varsIn :: UConstraint -> [Var]
140+varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]
141+varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]