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 ( {- SEE BELOW: -- KSW 2000-10-13
23 #include "HsVersions.h"
26 import Bag ( Bag, unitBag, emptyBag, unionBags, foldlBag, bagToList )
30 {- ENTIRE FILE COMMENTED OUT FOR NOW -- KSW 2000-10-13
32 This monomorphic version of the analysis is outdated. I'm
33 currently ripping out the old one and inserting the new one. For
34 now, I'm simply commenting out this entire file.
38 ======================================================================
43 First, individual constraints on particular variables. This is
44 private to the implementation.
47 data UCon = UCEq UVar UVar -- j = k (equivalence)
48 | UCBound [UVar] UVar [UVar] -- {..} <= j <= {..}
49 | UCUsOnce UVar -- j = 1
50 | UCUsMany UVar -- j = omega
53 Next, the public (but abstract) data type for a usage constraint set:
54 either a bag of mappings from @UVar@ to @UCon@, or an error message
55 for an inconsistent constraint set.
58 data UConSet = UConSet (Bag (VarEnv UCon))
62 The idea is that the @VarEnv@s (which will eventually be merged into a
63 single @VarEnv@) are union-find data structures: a variable is either
64 equal to another variable, or it is bounded or has a value. The
65 equalities form a forest pointing to a root node for each equality
66 class, on which is found the bound or value for that class.
68 The @Bag@ enables two-phase operation: we merely collect constraints
69 in the first phase, an donly union them at solution time. This gives
70 a much more efficient algorithm, as we make only a single pass over
73 Note that the absence of a variable from the @VarEnv@ is exactly
74 equivalent to it being mapped to @UCBound [] _ []@.
80 @emptyUConSet@ gives an empty constraint set.
81 @eqManyUConSet@ constrains an annotation to be Many.
82 @eqUConSet@ constrains two annotations to be equal.
83 @leqUConSet@ constrains one annotation to be less than or equal to
84 another (with Once < Many).
87 mkUCS = UConSet . unitBag -- helper function not exported
89 emptyUConSet :: UConSet
90 emptyUConSet = UConSet emptyBag
92 eqManyUConSet :: UsageAnn -> UConSet
94 eqManyUConSet UsOnce = UConFail (text "Once /= Many")
95 eqManyUConSet UsMany = emptyUConSet
96 eqManyUConSet (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsMany uv)
98 eqUConSet :: UsageAnn -> UsageAnn -> UConSet
100 eqUConSet UsOnce UsOnce = emptyUConSet
101 eqUConSet UsOnce (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsOnce uv)
102 eqUConSet UsMany UsMany = emptyUConSet
103 eqUConSet UsMany (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsMany uv)
104 eqUConSet (UsVar uv) UsOnce = mkUCS $ unitVarEnv uv (UCUsOnce uv)
105 eqUConSet (UsVar uv) UsMany = mkUCS $ unitVarEnv uv (UCUsMany uv)
106 eqUConSet (UsVar uv) (UsVar uv') = if uv==uv'
108 else mkUCS $ unitVarEnv uv (UCEq uv uv')
109 eqUConSet UsMany UsOnce = UConFail (text "Many /= Once")
110 eqUConSet UsOnce UsMany = UConFail (text "Once /= Many")
112 leqUConSet :: UsageAnn -> UsageAnn -> UConSet
114 leqUConSet UsOnce _ = emptyUConSet
115 leqUConSet _ UsMany = emptyUConSet
116 leqUConSet UsMany UsOnce = UConFail (text "Many /<= Once")
117 leqUConSet UsMany (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsMany uv)
118 leqUConSet (UsVar uv) UsOnce = mkUCS $ unitVarEnv uv (UCUsOnce uv)
119 leqUConSet (UsVar uv) (UsVar uv') = mkUCS $ mkVarEnv [(uv, UCBound [] uv [uv']),
120 (uv',UCBound [uv] uv' [] )]
123 @unionUCS@ forms the union of two @UConSet@s.
124 @unionUCSs@ forms the `big union' of a list of @UConSet@s.
127 unionUCS :: UConSet -> UConSet -> UConSet
129 unionUCS (UConSet b1) (UConSet b2) = UConSet (b1 `unionBags` b2)
130 unionUCS ucs@(UConFail _) _ = ucs -- favour first error
131 unionUCS (UConSet _) ucs@(UConFail _) = ucs
133 unionUCSs :: [UConSet] -> UConSet
135 unionUCSs ucss = foldl unionUCS emptyUConSet ucss
139 @solveUCS@ finds the minimal solution to the constraint set, returning
140 it as @Just@ a substitution function taking usage variables to usage
141 annotations (@UsOnce@ or @UsMany@). If this is not possible (for an
142 inconsistent constraint set), @solveUCS@ returns @Nothing@.
144 The minimal solution is found by simply reading off the known
145 variables, and for unknown ones substituting @UsOnce@.
148 solveUCS :: UConSet -> Maybe (UVar -> UsageAnn)
150 solveUCS (UConSet css)
151 = case foldlBag (\cs1 jcs2 -> foldVarEnv addUCS cs1 jcs2)
154 Left cs -> let cs' = mapVarEnv conToSub cs
155 sub uv = case lookupVarEnv cs' uv of
158 conToSub (UCEq _ uv') = case lookupVarEnv cs uv' of
160 Just con' -> conToSub con'
161 conToSub (UCUsOnce _ ) = UsOnce
162 conToSub (UCUsMany _ ) = UsMany
163 conToSub (UCBound _ _ _ ) = UsOnce
165 Right err -> solveUCS (UConFail err)
167 solveUCS (UConFail why) =
169 pprTrace "UConFail:" why $
174 ======================================================================
179 In the internals, we use the @VarEnv UCon@ explicitly, or occasionally
180 @Either (VarEnv UCon) SDoc@. In other words, the @Bag@ is no longer
183 @findUCon@ finds the root of an equivalence class.
184 @changeUConUVar@ copies a constraint, but changes the variable constrained.
187 findUCon :: VarEnv UCon -> UVar -> UVar
190 = case lookupVarEnv cs uv of
191 Just (UCEq _ uv') -> findUCon cs uv'
195 changeUConUVar :: UCon -> UVar -> UCon
197 changeUConUVar (UCEq _ v ) uv' = (UCEq uv' v )
198 changeUConUVar (UCBound us _ vs) uv' = (UCBound us uv' vs)
199 changeUConUVar (UCUsOnce _ ) uv' = (UCUsOnce uv' )
200 changeUConUVar (UCUsMany _ ) uv' = (UCUsMany uv' )
203 @mergeUVars@ tests to see if a set of @UVar@s can be constrained. If
204 they can, it returns the set of root @UVar@s represented (with no
205 duplicates); if they can't, it returns @Nothing@.
208 mergeUVars :: VarEnv UCon -- current constraint set
209 -> Bool -- True/False = try to constrain to Many/Once
210 -> [UVar] -- list of UVars to constrain
211 -> Maybe [UVar] -- Just [root uvars to force], or Nothing if conflict
213 mergeUVars cs isMany vs = foldl muv (Just []) vs
215 muv :: Maybe [UVar] -> UVar -> Maybe [UVar]
219 = let rv = findUCon cs v
224 case lookupVarEnv cs rv of -- never UCEq
225 Nothing -> Just (rv:vs)
226 Just (UCBound _ _ _) -> Just (rv:vs)
227 Just (UCUsOnce _) -> if isMany then Nothing else jvs
228 Just (UCUsMany _) -> if isMany then jvs else Nothing
231 @addUCS@ adds an individual @UCon@ on a @UVar@ to a @UConSet@. This
232 is the core of the algorithm. As such, it could probably use some
236 addUCS :: UCon -- constraint to add
237 -> Either (VarEnv UCon) SDoc -- old constraint set or error
238 -> Either (VarEnv UCon) SDoc -- new constraint set or error
240 addUCS _ jcs@(Right _) = jcs -- propagate errors
242 addUCS (UCEq uv1 uv2) jcs@(Left cs)
243 = let ruv1 = findUCon cs uv1
244 ruv2 = findUCon cs uv2
246 then jcs -- no change if already equal
247 else let cs' = Left $ extendVarEnv cs ruv1 (UCEq ruv1 ruv2) -- merge trees
248 in case lookupVarEnv cs ruv1 of
250 -> addUCS (changeUConUVar uc' ruv2) cs' -- merge old constraints
254 addUCS (UCBound us uv1 vs) jcs@(Left cs)
255 = let ruv1 = findUCon cs uv1
256 in case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of -- never UCEq
258 -> case (mergeUVars cs False (us'++us),
259 mergeUVars cs True (vs'++vs)) of
260 (Just us'',Just vs'') -- update
261 -> Left $ extendVarEnv cs ruv1 (UCBound us'' ruv1 vs'')
262 (Nothing, Just vs'') -- set
263 -> addUCS (UCUsMany ruv1)
264 (forceUVars UCUsMany vs'' jcs)
265 (Just us'',Nothing) -- set
266 -> addUCS (UCUsOnce ruv1)
267 (forceUVars UCUsOnce us'' jcs)
268 (Nothing, Nothing) -- fail
269 -> Right (text "union failed[B] at" <+> ppr uv1)
271 -> forceUVars UCUsOnce us jcs
273 -> forceUVars UCUsMany vs jcs
275 addUCS (UCUsOnce uv1) jcs@(Left cs)
276 = let ruv1 = findUCon cs uv1
277 in case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of -- never UCEq
279 -> forceUVars UCUsOnce us (Left $ extendVarEnv cs ruv1 (UCUsOnce ruv1))
283 -> Right (text "union failed[O] at" <+> ppr uv1)
285 addUCS (UCUsMany uv1) jcs@(Left cs)
286 = let ruv1 = findUCon cs uv1
287 in case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of -- never UCEq
289 -> forceUVars UCUsMany vs (Left $ extendVarEnv cs ruv1 (UCUsMany ruv1))
291 -> Right (text "union failed[M] at" <+> ppr uv1)
295 -- helper function forcing a set of UVars to either Once or Many:
296 forceUVars :: (UVar -> UCon)
298 -> Either (VarEnv UCon) SDoc
299 -> Either (VarEnv UCon) SDoc
300 forceUVars uc uvs cs0 = foldl (\cs uv -> addUCS (uc uv) cs) cs0 uvs
303 ======================================================================
309 -- Printing a usage constraint.
311 pprintUCon :: VarEnv UCon -> UCon -> SDoc
313 pprintUCon fm (UCEq uv1 uv2)
314 = ppr uv1 <+> text "=" <+> ppr uv2 <> text ":"
315 <+> let uv2' = findUCon fm uv2
316 in case lookupVarEnv fm uv2' of
317 Just uc -> pprintUCon fm uc
318 Nothing -> text "unconstrained"
320 pprintUCon fm (UCBound us uv vs)
321 = lbrace <> hcat (punctuate comma (map ppr us)) <> rbrace
322 <+> text "<=" <+> ppr uv <+> text "<="
323 <+> lbrace <> hcat (punctuate comma (map ppr vs)) <> rbrace
325 pprintUCon fm (UCUsOnce uv)
326 = ppr uv <+> text "=" <+> ppr UsOnce
328 pprintUCon fm (UCUsMany uv)
329 = ppr uv <+> text "=" <+> ppr UsMany
331 -- Printing a usage constraint set.
333 instance Outputable UConSet where
335 = text "UConSet:" <+> lbrace
336 $$ vcat (map (\fm -> nest 2 (vcat (map (pprintUCon fm) (rngVarEnv fm))))
341 = hang (text "UConSet inconsistent:")
344 END OF ENTIRELY-COMMENTED-OUT FILE -- KSW 2000-10-13 -}
347 ======================================================================