2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
4 \section[UConSet]{UsageSP constraint solver}
6 This code is (based on) PhD work of Keith Wansbrough <kw217@cl.cam.ac.uk>,
7 February 1998 .. April 1999.
9 Keith Wansbrough 1998-02-16..1999-04-29
12 module UConSet ( UConSet,
22 #include "HsVersions.h"
25 import Type ( UsageAnn(..) )
27 import Monad ( foldM )
28 import Bag ( Bag, unitBag, emptyBag, unionBags, foldlBag, bagToList )
33 ======================================================================
38 First, individual constraints on particular variables. This is
39 private to the implementation.
42 data UCon = UCEq UVar UVar -- j = k (equivalence)
43 | UCBound [UVar] UVar [UVar] -- {..} <= j <= {..}
44 | UCUsOnce UVar -- j = 1
45 | UCUsMany UVar -- j = omega
48 Next, the public (but abstract) data type for a usage constraint set:
49 either a bag of mappings from @UVar@ to @UCon@, or an error message
50 for an inconsistent constraint set.
53 data UConSet = UConSet (Bag (VarEnv UCon))
57 The idea is that the @VarEnv@s (which will eventually be merged into a
58 single @VarEnv@) are union-find data structures: a variable is either
59 equal to another variable, or it is bounded or has a value. The
60 equalities form a forest pointing to a root node for each equality
61 class, on which is found the bound or value for that class.
63 The @Bag@ enables two-phase operation: we merely collect constraints
64 in the first phase, an donly union them at solution time. This gives
65 a much more efficient algorithm, as we make only a single pass over
68 Note that the absence of a variable from the @VarEnv@ is exactly
69 equivalent to it being mapped to @UCBound [] _ []@.
75 @emptyUConSet@ gives an empty constraint set.
76 @eqManyUConSet@ constrains an annotation to be Many.
77 @eqUConSet@ constrains two annotations to be equal.
78 @leqUConSet@ constrains one annotation to be less than or equal to
79 another (with Once < Many).
82 mkUCS = UConSet . unitBag -- helper function not exported
84 emptyUConSet :: UConSet
85 emptyUConSet = UConSet emptyBag
87 eqManyUConSet :: UsageAnn -> UConSet
89 eqManyUConSet UsOnce = UConFail (text "Once /= Many")
90 eqManyUConSet UsMany = emptyUConSet
91 eqManyUConSet (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsMany uv)
93 eqUConSet :: UsageAnn -> UsageAnn -> UConSet
95 eqUConSet UsOnce UsOnce = emptyUConSet
96 eqUConSet UsOnce (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsOnce uv)
97 eqUConSet UsMany UsMany = emptyUConSet
98 eqUConSet UsMany (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsMany uv)
99 eqUConSet (UsVar uv) UsOnce = mkUCS $ unitVarEnv uv (UCUsOnce uv)
100 eqUConSet (UsVar uv) UsMany = mkUCS $ unitVarEnv uv (UCUsMany uv)
101 eqUConSet (UsVar uv) (UsVar uv') = if uv==uv'
103 else mkUCS $ unitVarEnv uv (UCEq uv uv')
104 eqUConSet UsMany UsOnce = UConFail (text "Many /= Once")
105 eqUConSet UsOnce UsMany = UConFail (text "Once /= Many")
107 leqUConSet :: UsageAnn -> UsageAnn -> UConSet
109 leqUConSet UsOnce _ = emptyUConSet
110 leqUConSet _ UsMany = emptyUConSet
111 leqUConSet UsMany UsOnce = UConFail (text "Many /<= Once")
112 leqUConSet UsMany (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsMany uv)
113 leqUConSet (UsVar uv) UsOnce = mkUCS $ unitVarEnv uv (UCUsOnce uv)
114 leqUConSet (UsVar uv) (UsVar uv') = mkUCS $ mkVarEnv [(uv, UCBound [] uv [uv']),
115 (uv',UCBound [uv] uv' [] )]
118 @unionUCS@ forms the union of two @UConSet@s.
119 @unionUCSs@ forms the `big union' of a list of @UConSet@s.
122 unionUCS :: UConSet -> UConSet -> UConSet
124 unionUCS (UConSet b1) (UConSet b2) = UConSet (b1 `unionBags` b2)
125 unionUCS ucs@(UConFail _) _ = ucs -- favour first error
126 unionUCS (UConSet _) ucs@(UConFail _) = ucs
128 unionUCSs :: [UConSet] -> UConSet
130 unionUCSs ucss = foldl unionUCS emptyUConSet ucss
134 @solveUCS@ finds the minimal solution to the constraint set, returning
135 it as @Just@ a substitution function taking usage variables to usage
136 annotations (@UsOnce@ or @UsMany@). If this is not possible (for an
137 inconsistent constraint set), @solveUCS@ returns @Nothing@.
139 The minimal solution is found by simply reading off the known
140 variables, and for unknown ones substituting @UsOnce@.
143 solveUCS :: UConSet -> Maybe (UVar -> UsageAnn)
145 solveUCS (UConSet css)
146 = case foldlBag (\cs1 jcs2 -> foldVarEnv addUCS cs1 jcs2)
149 Left cs -> let cs' = mapVarEnv conToSub cs
150 sub uv = case lookupVarEnv cs' uv of
153 conToSub (UCEq _ uv') = case lookupVarEnv cs uv' of
155 Just con' -> conToSub con'
156 conToSub (UCUsOnce _ ) = UsOnce
157 conToSub (UCUsMany _ ) = UsMany
158 conToSub (UCBound _ _ _ ) = UsOnce
160 Right err -> solveUCS (UConFail err)
162 solveUCS (UConFail why) =
164 pprTrace "UConFail:" why $
169 ======================================================================
174 In the internals, we use the @VarEnv UCon@ explicitly, or occasionally
175 @Either (VarEnv UCon) SDoc@. In other words, the @Bag@ is no longer
178 @findUCon@ finds the root of an equivalence class.
179 @changeUConUVar@ copies a constraint, but changes the variable constrained.
182 findUCon :: VarEnv UCon -> UVar -> UVar
185 = case lookupVarEnv cs uv of
186 Just (UCEq _ uv') -> findUCon cs uv'
190 changeUConUVar :: UCon -> UVar -> UCon
192 changeUConUVar (UCEq _ v ) uv' = (UCEq uv' v )
193 changeUConUVar (UCBound us _ vs) uv' = (UCBound us uv' vs)
194 changeUConUVar (UCUsOnce _ ) uv' = (UCUsOnce uv' )
195 changeUConUVar (UCUsMany _ ) uv' = (UCUsMany uv' )
198 @mergeUVars@ tests to see if a set of @UVar@s can be constrained. If
199 they can, it returns the set of root @UVar@s represented (with no
200 duplicates); if they can't, it returns @Nothing@.
203 mergeUVars :: VarEnv UCon -- current constraint set
204 -> Bool -- True/False = try to constrain to Many/Once
205 -> [UVar] -- list of UVars to constrain
206 -> Maybe [UVar] -- Just [root uvars to force], or Nothing if conflict
208 mergeUVars cs isMany vs = foldl muv (Just []) vs
210 muv :: Maybe [UVar] -> UVar -> Maybe [UVar]
214 = let rv = findUCon cs v
219 case lookupVarEnv cs rv of -- never UCEq
220 Nothing -> Just (rv:vs)
221 Just (UCBound _ _ _) -> Just (rv:vs)
222 Just (UCUsOnce _) -> if isMany then Nothing else jvs
223 Just (UCUsMany _) -> if isMany then jvs else Nothing
226 @addUCS@ adds an individual @UCon@ on a @UVar@ to a @UConSet@. This
227 is the core of the algorithm. As such, it could probably use some
231 addUCS :: UCon -- constraint to add
232 -> Either (VarEnv UCon) SDoc -- old constraint set or error
233 -> Either (VarEnv UCon) SDoc -- new constraint set or error
235 addUCS _ jcs@(Right _) = jcs -- propagate errors
237 addUCS (UCEq uv1 uv2) jcs@(Left cs)
238 = let ruv1 = findUCon cs uv1
239 ruv2 = findUCon cs uv2
241 then jcs -- no change if already equal
242 else let cs' = Left $ extendVarEnv cs ruv1 (UCEq ruv1 ruv2) -- merge trees
243 in case lookupVarEnv cs ruv1 of
245 -> addUCS (changeUConUVar uc' ruv2) cs' -- merge old constraints
249 addUCS (UCBound us uv1 vs) jcs@(Left cs)
250 = let ruv1 = findUCon cs uv1
251 in case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of -- never UCEq
253 -> case (mergeUVars cs False (us'++us),
254 mergeUVars cs True (vs'++vs)) of
255 (Just us'',Just vs'') -- update
256 -> Left $ extendVarEnv cs ruv1 (UCBound us'' ruv1 vs'')
257 (Nothing, Just vs'') -- set
258 -> addUCS (UCUsMany ruv1)
259 (forceUVars UCUsMany vs'' jcs)
260 (Just us'',Nothing) -- set
261 -> addUCS (UCUsOnce ruv1)
262 (forceUVars UCUsOnce us'' jcs)
263 (Nothing, Nothing) -- fail
264 -> Right (text "union failed[B] at" <+> ppr uv1)
266 -> forceUVars UCUsOnce us jcs
268 -> forceUVars UCUsMany vs jcs
270 addUCS (UCUsOnce uv1) jcs@(Left cs)
271 = let ruv1 = findUCon cs uv1
272 in case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of -- never UCEq
274 -> forceUVars UCUsOnce us (Left $ extendVarEnv cs ruv1 (UCUsOnce ruv1))
278 -> Right (text "union failed[O] at" <+> ppr uv1)
280 addUCS (UCUsMany uv1) jcs@(Left cs)
281 = let ruv1 = findUCon cs uv1
282 in case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of -- never UCEq
284 -> forceUVars UCUsMany vs (Left $ extendVarEnv cs ruv1 (UCUsMany ruv1))
286 -> Right (text "union failed[M] at" <+> ppr uv1)
290 -- helper function forcing a set of UVars to either Once or Many:
291 forceUVars :: (UVar -> UCon)
293 -> Either (VarEnv UCon) SDoc
294 -> Either (VarEnv UCon) SDoc
295 forceUVars uc uvs cs0 = foldl (\cs uv -> addUCS (uc uv) cs) cs0 uvs
298 ======================================================================
304 -- Printing a usage constraint.
306 pprintUCon :: VarEnv UCon -> UCon -> SDoc
308 pprintUCon fm (UCEq uv1 uv2)
309 = ppr uv1 <+> text "=" <+> ppr uv2 <> text ":"
310 <+> let uv2' = findUCon fm uv2
311 in case lookupVarEnv fm uv2' of
312 Just uc -> pprintUCon fm uc
313 Nothing -> text "unconstrained"
315 pprintUCon fm (UCBound us uv vs)
316 = lbrace <> hcat (punctuate comma (map ppr us)) <> rbrace
317 <+> text "<=" <+> ppr uv <+> text "<="
318 <+> lbrace <> hcat (punctuate comma (map ppr vs)) <> rbrace
320 pprintUCon fm (UCUsOnce uv)
321 = ppr uv <+> text "=" <+> ppr UsOnce
323 pprintUCon fm (UCUsMany uv)
324 = ppr uv <+> text "=" <+> ppr UsMany
326 -- Printing a usage constraint set.
328 instance Outputable UConSet where
330 = text "UConSet:" <+> lbrace
331 $$ vcat (map (\fm -> nest 2 (vcat (map (pprintUCon fm) (rngVarEnv fm))))
336 = hang (text "UConSet inconsistent:")
340 ======================================================================