% % (c) The GRASP/AQUA Project, Glasgow University, 1998 % \section[UConSet]{UsageSP constraint solver} This code is (based on) PhD work of Keith Wansbrough , February 1998 .. April 1999. Keith Wansbrough 1998-02-16..1999-04-29 \begin{code} module UConSet ( UConSet, emptyUConSet, eqManyUConSet, eqUConSet, leqUConSet, unionUCS, unionUCSs, solveUCS, ) where #include "HsVersions.h" import VarEnv import Type ( UsageAnn(..) ) import Var ( UVar ) import Monad ( foldM ) import Bag ( Bag, unitBag, emptyBag, unionBags, foldlBag, bagToList ) import Outputable import PprType \end{code} ====================================================================== The data type: ~~~~~~~~~~~~~~ First, individual constraints on particular variables. This is private to the implementation. \begin{code} data UCon = UCEq UVar UVar -- j = k (equivalence) | UCBound [UVar] UVar [UVar] -- {..} <= j <= {..} | UCUsOnce UVar -- j = 1 | UCUsMany UVar -- j = omega \end{code} Next, the public (but abstract) data type for a usage constraint set: either a bag of mappings from @UVar@ to @UCon@, or an error message for an inconsistent constraint set. \begin{code} data UConSet = UConSet (Bag (VarEnv UCon)) | UConFail SDoc \end{code} The idea is that the @VarEnv@s (which will eventually be merged into a single @VarEnv@) are union-find data structures: a variable is either equal to another variable, or it is bounded or has a value. The equalities form a forest pointing to a root node for each equality class, on which is found the bound or value for that class. The @Bag@ enables two-phase operation: we merely collect constraints in the first phase, an donly union them at solution time. This gives a much more efficient algorithm, as we make only a single pass over the constraints. Note that the absence of a variable from the @VarEnv@ is exactly equivalent to it being mapped to @UCBound [] _ []@. The interface: ~~~~~~~~~~~~~~ @emptyUConSet@ gives an empty constraint set. @eqManyUConSet@ constrains an annotation to be Many. @eqUConSet@ constrains two annotations to be equal. @leqUConSet@ constrains one annotation to be less than or equal to another (with Once < Many). \begin{code} mkUCS = UConSet . unitBag -- helper function not exported emptyUConSet :: UConSet emptyUConSet = UConSet emptyBag eqManyUConSet :: UsageAnn -> UConSet eqManyUConSet UsOnce = UConFail (text "Once /= Many") eqManyUConSet UsMany = emptyUConSet eqManyUConSet (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsMany uv) eqUConSet :: UsageAnn -> UsageAnn -> UConSet eqUConSet UsOnce UsOnce = emptyUConSet eqUConSet UsOnce (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsOnce uv) eqUConSet UsMany UsMany = emptyUConSet eqUConSet UsMany (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsMany uv) eqUConSet (UsVar uv) UsOnce = mkUCS $ unitVarEnv uv (UCUsOnce uv) eqUConSet (UsVar uv) UsMany = mkUCS $ unitVarEnv uv (UCUsMany uv) eqUConSet (UsVar uv) (UsVar uv') = if uv==uv' then emptyUConSet else mkUCS $ unitVarEnv uv (UCEq uv uv') eqUConSet UsMany UsOnce = UConFail (text "Many /= Once") eqUConSet UsOnce UsMany = UConFail (text "Once /= Many") leqUConSet :: UsageAnn -> UsageAnn -> UConSet leqUConSet UsOnce _ = emptyUConSet leqUConSet _ UsMany = emptyUConSet leqUConSet UsMany UsOnce = UConFail (text "Many /<= Once") leqUConSet UsMany (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsMany uv) leqUConSet (UsVar uv) UsOnce = mkUCS $ unitVarEnv uv (UCUsOnce uv) leqUConSet (UsVar uv) (UsVar uv') = mkUCS $ mkVarEnv [(uv, UCBound [] uv [uv']), (uv',UCBound [uv] uv' [] )] \end{code} @unionUCS@ forms the union of two @UConSet@s. @unionUCSs@ forms the `big union' of a list of @UConSet@s. \begin{code} unionUCS :: UConSet -> UConSet -> UConSet unionUCS (UConSet b1) (UConSet b2) = UConSet (b1 `unionBags` b2) unionUCS ucs@(UConFail _) _ = ucs -- favour first error unionUCS (UConSet _) ucs@(UConFail _) = ucs unionUCSs :: [UConSet] -> UConSet unionUCSs ucss = foldl unionUCS emptyUConSet ucss \end{code} @solveUCS@ finds the minimal solution to the constraint set, returning it as @Just@ a substitution function taking usage variables to usage annotations (@UsOnce@ or @UsMany@). If this is not possible (for an inconsistent constraint set), @solveUCS@ returns @Nothing@. The minimal solution is found by simply reading off the known variables, and for unknown ones substituting @UsOnce@. \begin{code} solveUCS :: UConSet -> Maybe (UVar -> UsageAnn) solveUCS (UConSet css) = case foldlBag (\cs1 jcs2 -> foldVarEnv addUCS cs1 jcs2) (Left emptyVarEnv) css of Left cs -> let cs' = mapVarEnv conToSub cs sub uv = case lookupVarEnv cs' uv of Just u -> u Nothing -> UsOnce conToSub (UCEq _ uv') = case lookupVarEnv cs uv' of Nothing -> UsOnce Just con' -> conToSub con' conToSub (UCUsOnce _ ) = UsOnce conToSub (UCUsMany _ ) = UsMany conToSub (UCBound _ _ _ ) = UsOnce in Just sub Right err -> solveUCS (UConFail err) solveUCS (UConFail why) = #ifdef DEBUG pprTrace "UConFail:" why $ #endif Nothing \end{code} ====================================================================== The internals: ~~~~~~~~~~~~~~ In the internals, we use the @VarEnv UCon@ explicitly, or occasionally @Either (VarEnv UCon) SDoc@. In other words, the @Bag@ is no longer used. @findUCon@ finds the root of an equivalence class. @changeUConUVar@ copies a constraint, but changes the variable constrained. \begin{code} findUCon :: VarEnv UCon -> UVar -> UVar findUCon cs uv = case lookupVarEnv cs uv of Just (UCEq _ uv') -> findUCon cs uv' Just _ -> uv Nothing -> uv changeUConUVar :: UCon -> UVar -> UCon changeUConUVar (UCEq _ v ) uv' = (UCEq uv' v ) changeUConUVar (UCBound us _ vs) uv' = (UCBound us uv' vs) changeUConUVar (UCUsOnce _ ) uv' = (UCUsOnce uv' ) changeUConUVar (UCUsMany _ ) uv' = (UCUsMany uv' ) \end{code} @mergeUVars@ tests to see if a set of @UVar@s can be constrained. If they can, it returns the set of root @UVar@s represented (with no duplicates); if they can't, it returns @Nothing@. \begin{code} mergeUVars :: VarEnv UCon -- current constraint set -> Bool -- True/False = try to constrain to Many/Once -> [UVar] -- list of UVars to constrain -> Maybe [UVar] -- Just [root uvars to force], or Nothing if conflict mergeUVars cs isMany vs = foldl muv (Just []) vs where muv :: Maybe [UVar] -> UVar -> Maybe [UVar] muv Nothing _ = Nothing muv jvs@(Just vs) v = let rv = findUCon cs v in if elem rv vs then jvs else case lookupVarEnv cs rv of -- never UCEq Nothing -> Just (rv:vs) Just (UCBound _ _ _) -> Just (rv:vs) Just (UCUsOnce _) -> if isMany then Nothing else jvs Just (UCUsMany _) -> if isMany then jvs else Nothing \end{code} @addUCS@ adds an individual @UCon@ on a @UVar@ to a @UConSet@. This is the core of the algorithm. As such, it could probably use some optimising. \begin{code} addUCS :: UCon -- constraint to add -> Either (VarEnv UCon) SDoc -- old constraint set or error -> Either (VarEnv UCon) SDoc -- new constraint set or error addUCS _ jcs@(Right _) = jcs -- propagate errors addUCS (UCEq uv1 uv2) jcs@(Left cs) = let ruv1 = findUCon cs uv1 ruv2 = findUCon cs uv2 in if ruv1==ruv2 then jcs -- no change if already equal else let cs' = Left $ extendVarEnv cs ruv1 (UCEq ruv1 ruv2) -- merge trees in case lookupVarEnv cs ruv1 of Just uc' -> addUCS (changeUConUVar uc' ruv2) cs' -- merge old constraints Nothing -> cs' addUCS (UCBound us uv1 vs) jcs@(Left cs) = let ruv1 = findUCon cs uv1 in case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of -- never UCEq UCBound us' _ vs' -> case (mergeUVars cs False (us'++us), mergeUVars cs True (vs'++vs)) of (Just us'',Just vs'') -- update -> Left $ extendVarEnv cs ruv1 (UCBound us'' ruv1 vs'') (Nothing, Just vs'') -- set -> addUCS (UCUsMany ruv1) (forceUVars UCUsMany vs'' jcs) (Just us'',Nothing) -- set -> addUCS (UCUsOnce ruv1) (forceUVars UCUsOnce us'' jcs) (Nothing, Nothing) -- fail -> Right (text "union failed[B] at" <+> ppr uv1) UCUsOnce _ -> forceUVars UCUsOnce us jcs UCUsMany _ -> forceUVars UCUsMany vs jcs addUCS (UCUsOnce uv1) jcs@(Left cs) = let ruv1 = findUCon cs uv1 in case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of -- never UCEq UCBound us _ vs -> forceUVars UCUsOnce us (Left $ extendVarEnv cs ruv1 (UCUsOnce ruv1)) UCUsOnce _ -> jcs UCUsMany _ -> Right (text "union failed[O] at" <+> ppr uv1) addUCS (UCUsMany uv1) jcs@(Left cs) = let ruv1 = findUCon cs uv1 in case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of -- never UCEq UCBound us _ vs -> forceUVars UCUsMany vs (Left $ extendVarEnv cs ruv1 (UCUsMany ruv1)) UCUsOnce _ -> Right (text "union failed[M] at" <+> ppr uv1) UCUsMany _ -> jcs -- helper function forcing a set of UVars to either Once or Many: forceUVars :: (UVar -> UCon) -> [UVar] -> Either (VarEnv UCon) SDoc -> Either (VarEnv UCon) SDoc forceUVars uc uvs cs0 = foldl (\cs uv -> addUCS (uc uv) cs) cs0 uvs \end{code} ====================================================================== Pretty-printing: ~~~~~~~~~~~~~~~~ \begin{code} -- Printing a usage constraint. pprintUCon :: VarEnv UCon -> UCon -> SDoc pprintUCon fm (UCEq uv1 uv2) = ppr uv1 <+> text "=" <+> ppr uv2 <> text ":" <+> let uv2' = findUCon fm uv2 in case lookupVarEnv fm uv2' of Just uc -> pprintUCon fm uc Nothing -> text "unconstrained" pprintUCon fm (UCBound us uv vs) = lbrace <> hcat (punctuate comma (map ppr us)) <> rbrace <+> text "<=" <+> ppr uv <+> text "<=" <+> lbrace <> hcat (punctuate comma (map ppr vs)) <> rbrace pprintUCon fm (UCUsOnce uv) = ppr uv <+> text "=" <+> ppr UsOnce pprintUCon fm (UCUsMany uv) = ppr uv <+> text "=" <+> ppr UsMany -- Printing a usage constraint set. instance Outputable UConSet where ppr (UConSet bfm) = text "UConSet:" <+> lbrace $$ vcat (map (\fm -> nest 2 (vcat (map (pprintUCon fm) (rngVarEnv fm)))) (bagToList bfm)) $$ rbrace ppr (UConFail d) = hang (text "UConSet inconsistent:") 4 d \end{code} ====================================================================== EOF