git.iko.soy/Idris-dev
on master help sign in
Change Solver to use ConstraintFC, not a pair
6c673c2Edwin Brady
src/Idris/Core/Constraints.hs+19−19
compare with master
unifiedsplit
@@ -71,10 +71,10 @@ solve maxUniverseLevel ucs =
71 rhs _ = Nothing
71 rhs _ = Nothing
72
72
73 -- | a map from variables to the list of constraints the variable occurs in. (in the LHS of a constraint)
73 -- | a map from variables to the list of constraints the variable occurs in. (in the LHS of a constraint)
74− constraintsLHS :: M.Map Var (S.Set (UConstraint, FC))
74+ constraintsLHS :: M.Map Var (S.Set ConstraintFC)
75 constraintsLHS = M.fromListWith S.union
75 constraintsLHS = M.fromListWith S.union
76− [ (v, S.singleton (c,fc))
76+ [ (v, S.singleton (ConstraintFC c fc))
77− | (c, fc) <- inpConstraints
77+ | (ConstraintFC c fc) <- inpConstraints
78 , let vars = varsIn c
78 , let vars = varsIn c
79 , length vars > 1 -- do not register unary constraints
79 , length vars > 1 -- do not register unary constraints
80 , v <- vars
80 , v <- vars
@@ -82,10 +82,10 @@ solve maxUniverseLevel ucs =
82 ]
82 ]
83
83
84 -- | a map from variables to the list of constraints the variable occurs in. (in the RHS of a constraint)
84 -- | a map from variables to the list of constraints the variable occurs in. (in the RHS of a constraint)
85− constraintsRHS :: M.Map Var (S.Set (UConstraint, FC))
85+ constraintsRHS :: M.Map Var (S.Set ConstraintFC)
86 constraintsRHS = M.fromListWith S.union
86 constraintsRHS = M.fromListWith S.union
87− [ (v, S.singleton (c,fc))
87+ [ (v, S.singleton (ConstraintFC c fc))
88− | (c, fc) <- inpConstraints
88+ | (ConstraintFC c fc) <- inpConstraints
89 , let vars = varsIn c
89 , let vars = varsIn c
90 , length vars > 1 -- do not register unary constraints
90 , length vars > 1 -- do not register unary constraints
91 , v <- vars
91 , v <- vars
@@ -107,15 +107,15 @@ solve maxUniverseLevel ucs =
107 ULE a b -> do
107 ULE a b -> do
108 Domain lowerA upperA <- domainOf a
108 Domain lowerA upperA <- domainOf a
109 Domain lowerB upperB <- domainOf b
109 Domain lowerB upperB <- domainOf b
110− when (upperB < upperA) $ updateUpperBoundOf (cons, fc) a upperB
110+ when (upperB < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB
111− when (lowerA > lowerB) $ updateLowerBoundOf (cons, fc) b lowerA
111+ when (lowerA > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA
112 ULT a b -> do
112 ULT a b -> do
113 Domain lowerA upperA <- domainOf a
113 Domain lowerA upperA <- domainOf a
114 Domain lowerB upperB <- domainOf b
114 Domain lowerB upperB <- domainOf b
115 let upperB_pred = pred upperB
115 let upperB_pred = pred upperB
116 let lowerA_succ = succ lowerA
116 let lowerA_succ = succ lowerA
117− when (upperB_pred < upperA) $ updateUpperBoundOf (cons, fc) a upperB_pred
117+ when (upperB_pred < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB_pred
118− when (lowerA_succ > lowerB) $ updateLowerBoundOf (cons, fc) b lowerA_succ
118+ when (lowerA_succ > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA_succ
119 propagate
119 propagate
120
120
121 -- | extract a solution from the state.
121 -- | extract a solution from the state.
@@ -141,12 +141,12 @@ solve maxUniverseLevel ucs =
141 domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)
141 domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)
142 domainOf (UVal val) = return (Domain val val)
142 domainOf (UVal val) = return (Domain val val)
143
143
144− updateUpperBoundOf :: (UConstraint, FC) -> UExp -> Int -> StateT SolverState TC ()
144+ updateUpperBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
145 updateUpperBoundOf suspect (UVar var) upper = do
145 updateUpperBoundOf suspect (UVar var) upper = do
146 doms <- gets domainStore
146 doms <- gets domainStore
147 let (oldDom@(Domain lower _), suspects) = doms M.! Var var
147 let (oldDom@(Domain lower _), suspects) = doms M.! Var var
148 let newDom = Domain lower upper
148 let newDom = Domain lower upper
149− when (wipeOut newDom) $ lift $ Error $ At (snd suspect) $ Msg $ unlines
149+ when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines
150 $ "Universe inconsistency."
150 $ "Universe inconsistency."
151 : ("Working on: " ++ show (UVar var))
151 : ("Working on: " ++ show (UVar var))
152 : ("Old domain: " ++ show oldDom)
152 : ("Old domain: " ++ show oldDom)
@@ -154,15 +154,15 @@ solve maxUniverseLevel ucs =
154 : "Involved constraints: "
154 : "Involved constraints: "
155 : map (("\t"++) . show) (suspect : S.toList suspects)
155 : map (("\t"++) . show) (suspect : S.toList suspects)
156 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
156 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
157− addToQueueRHS (fst suspect) (Var var)
157+ addToQueueRHS (uconstraint suspect) (Var var)
158 updateUpperBoundOf _ UVal{} _ = return ()
158 updateUpperBoundOf _ UVal{} _ = return ()
159
159
160− updateLowerBoundOf :: (UConstraint, FC) -> UExp -> Int -> StateT SolverState TC ()
160+ updateLowerBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
161 updateLowerBoundOf suspect (UVar var) lower = do
161 updateLowerBoundOf suspect (UVar var) lower = do
162 doms <- gets domainStore
162 doms <- gets domainStore
163 let (oldDom@(Domain _ upper), suspects) = doms M.! Var var
163 let (oldDom@(Domain _ upper), suspects) = doms M.! Var var
164 let newDom = Domain lower upper
164 let newDom = Domain lower upper
165− when (wipeOut newDom) $ lift $ Error $ At (snd suspect) $ Msg $ unlines
165+ when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines
166 $ "Universe inconsistency."
166 $ "Universe inconsistency."
167 : ("Working on: " ++ show (UVar var))
167 : ("Working on: " ++ show (UVar var))
168 : ("Old domain: " ++ show oldDom)
168 : ("Old domain: " ++ show oldDom)
@@ -170,7 +170,7 @@ solve maxUniverseLevel ucs =
170 : "Involved constraints: "
170 : "Involved constraints: "
171 : map (("\t"++) . show) (suspect : S.toList suspects)
171 : map (("\t"++) . show) (suspect : S.toList suspects)
172 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
172 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
173− addToQueueLHS (fst suspect) (Var var)
173+ addToQueueLHS (uconstraint suspect) (Var var)
174 updateLowerBoundOf _ UVal{} _ = return ()
174 updateLowerBoundOf _ UVal{} _ = return ()
175
175
176 -- | add all constraints (with the given var on the lhs) to the queue
176 -- | add all constraints (with the given var on the lhs) to the queue
@@ -181,11 +181,11 @@ solve maxUniverseLevel ucs =
181 Just cs -> do
181 Just cs -> do
182 Queue list set <- gets queue
182 Queue list set <- gets queue
183 let set' = S.insert thisCons set
183 let set' = S.insert thisCons set
184− let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set' ]
184+ let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]
185 if null newCons
185 if null newCons
186 then return ()
186 then return ()
187 else modify $ \ st -> st { queue = Queue (list ++ newCons)
187 else modify $ \ st -> st { queue = Queue (list ++ newCons)
188− (S.union set (S.fromList (map fst newCons))) }
188+ (S.union set (S.fromList (map uconstraint newCons))) }
189
189
190 -- | add all constraints (with the given var on the rhs) to the queue
190 -- | add all constraints (with the given var on the rhs) to the queue
191 addToQueueRHS :: MonadState SolverState m => UConstraint -> Var -> m ()
191 addToQueueRHS :: MonadState SolverState m => UConstraint -> Var -> m ()
@@ -195,7 +195,7 @@ solve maxUniverseLevel ucs =
195 Just cs -> do
195 Just cs -> do
196 Queue list set <- gets queue
196 Queue list set <- gets queue
197 let set' = S.insert thisCons set
197 let set' = S.insert thisCons set
198− let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set' ]
198+ let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]
199 if null newCons
199 if null newCons
200 then return ()
200 then return ()
201 else modify $ \ st -> st { queue = Queue (list ++ newCons)
201 else modify $ \ st -> st { queue = Queue (list ++ newCons)
test/error001/expected+7−7
@@ -1,9 +1,9 @@
1−test002.idr:5:6:Universe inconsistency.
1+test002.idr:1:6:Universe inconsistency.
2−Working on: e2
2+Working on: t
3−Old domain: Domain 4 4
3+Old domain: Domain 6 6
4−New domain: Domain 4 3
4+New domain: Domain 6 5
5Involved constraints:
5Involved constraints:
6− (e2 < f2,test002.idr:5:6)
6+ ConstraintFC {uconstraint = t <= u, ufc = test002.idr:1:6}
7− (e2 < f2,test002.idr:5:6)
7+ ConstraintFC {uconstraint = s < t, ufc = test002.idr:1:6}
8− (i1 <= e2,test002.idr:5:6)
8+ ConstraintFC {uconstraint = t <= u, ufc = test002.idr:1:6}
9
9