ghc/compiler/usageSP/UConSet.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
   3 %
   4 \section[UConSet]{UsageSP constraint solver}
   5
   6 This code is (based on) PhD work of Keith Wansbrough <kw217@cl.cam.ac.uk>,
   7 February 1998 .. April 1999.
   8
   9 Keith Wansbrough 1998-02-16..1999-04-29
  10
  11 \begin{code}
  12 module UConSet ( UConSet,
  13                  emptyUConSet,
  14                  eqManyUConSet,
  15                  eqUConSet,
  16                  leqUConSet,
  17                  unionUCS,
  18                  unionUCSs,
  19                  solveUCS,
  20                ) where
  21
  22 #include "HsVersions.h"
  23
  24 import VarEnv
  25 import Type             ( UsageAnn(..) )
  26 import Var              ( UVar )
  27 import Monad            ( foldM )
  28 import Bag              ( Bag, unitBag, emptyBag, unionBags, foldlBag, bagToList )
  29 import Outputable
  30 import PprType
  31 \end{code}
  32
  33 ======================================================================
  34
  35 The data type:
  36 ~~~~~~~~~~~~~~
  37
  38 First, individual constraints on particular variables.  This is
  39 private to the implementation.
  40
  41 \begin{code}
  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
  46 \end{code}
  47
  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.
  51
  52 \begin{code}
  53 data UConSet = UConSet (Bag (VarEnv UCon))
  54              | UConFail SDoc
  55 \end{code}
  56
  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.
  62
  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
  66 the constraints.
  67
  68 Note that the absence of a variable from the @VarEnv@ is exactly
  69 equivalent to it being mapped to @UCBound [] _ []@.
  70
  71
  72 The interface:
  73 ~~~~~~~~~~~~~~
  74
  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).
  80
  81 \begin{code}
  82 mkUCS = UConSet . unitBag  -- helper function not exported
  83
  84 emptyUConSet :: UConSet
  85 emptyUConSet  = UConSet emptyBag
  86
  87 eqManyUConSet :: UsageAnn -> UConSet
  88
  89 eqManyUConSet UsOnce     = UConFail (text "Once /= Many")
  90 eqManyUConSet UsMany     = emptyUConSet
  91 eqManyUConSet (UsVar uv) = mkUCS $ unitVarEnv uv (UCUsMany uv)
  92
  93 eqUConSet :: UsageAnn -> UsageAnn -> UConSet
  94
  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'
 102                                    then emptyUConSet
 103                                    else mkUCS $ unitVarEnv uv (UCEq uv uv')
 104 eqUConSet UsMany     UsOnce      = UConFail (text "Many /= Once")
 105 eqUConSet UsOnce     UsMany      = UConFail (text "Once /= Many")
 106
 107 leqUConSet :: UsageAnn -> UsageAnn -> UConSet
 108
 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' []   )]
 116 \end{code}
 117
 118 @unionUCS@ forms the union of two @UConSet@s.
 119 @unionUCSs@ forms the `big union' of a list of @UConSet@s.
 120
 121 \begin{code}
 122 unionUCS :: UConSet -> UConSet -> UConSet
 123
 124 unionUCS     (UConSet b1)      (UConSet b2) = UConSet (b1 `unionBags` b2)
 125 unionUCS ucs@(UConFail _)                _  = ucs  -- favour first error
 126 unionUCS     (UConSet  _)  ucs@(UConFail _) = ucs
 127
 128 unionUCSs :: [UConSet] -> UConSet
 129
 130 unionUCSs ucss = foldl unionUCS emptyUConSet ucss
 131 \end{code}
 132
 133
 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@.
 138
 139 The minimal solution is found by simply reading off the known
 140 variables, and for unknown ones substituting @UsOnce@.
 141
 142 \begin{code}
 143 solveUCS :: UConSet -> Maybe (UVar -> UsageAnn)
 144
 145 solveUCS (UConSet css)
 146   = case foldlBag (\cs1 jcs2 -> foldVarEnv addUCS cs1 jcs2)
 147                   (Left emptyVarEnv)
 148                   css of
 149       Left cs   -> let cs'    = mapVarEnv conToSub cs
 150                        sub uv = case lookupVarEnv cs' uv of
 151                                   Just u  -> u
 152                                   Nothing -> UsOnce
 153                        conToSub (UCEq       _ uv')    = case lookupVarEnv cs uv' of
 154                                                           Nothing   -> UsOnce
 155                                                           Just con' -> conToSub con'
 156                        conToSub (UCUsOnce   _    )    = UsOnce
 157                        conToSub (UCUsMany   _    )    = UsMany
 158                        conToSub (UCBound  _ _ _  )    = UsOnce
 159                    in  Just sub
 160       Right err -> solveUCS (UConFail err)
 161
 162 solveUCS (UConFail why) =
 163 #ifdef DEBUG
 164                           pprTrace "UConFail:" why $
 165 #endif
 166                           Nothing
 167 \end{code}
 168
 169 ======================================================================
 170
 171 The internals:
 172 ~~~~~~~~~~~~~~
 173
 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
 176 used.
 177
 178 @findUCon@ finds the root of an equivalence class.
 179 @changeUConUVar@ copies a constraint, but changes the variable constrained.
 180
 181 \begin{code}
 182 findUCon :: VarEnv UCon -> UVar -> UVar
 183
 184 findUCon cs uv
 185   = case lookupVarEnv cs uv of
 186       Just (UCEq _ uv') -> findUCon cs uv'
 187       Just _            -> uv
 188       Nothing           -> uv
 189
 190 changeUConUVar :: UCon -> UVar -> UCon
 191
 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'   )
 196 \end{code}
 197
 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@.
 201
 202 \begin{code}
 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
 207
 208 mergeUVars cs isMany vs = foldl muv (Just []) vs
 209   where
 210     muv :: Maybe [UVar] -> UVar -> Maybe [UVar]
 211     muv Nothing      _
 212       = Nothing
 213     muv jvs@(Just vs) v
 214       = let rv = findUCon cs v
 215         in  if elem rv vs
 216             then
 217               jvs
 218             else
 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
 224 \end{code}
 225
 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
 228 optimising.
 229
 230 \begin{code}
 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
 234
 235 addUCS _ jcs@(Right _) = jcs  -- propagate errors
 236
 237 addUCS (UCEq uv1 uv2) jcs@(Left cs)
 238   = let ruv1 = findUCon cs uv1
 239         ruv2 = findUCon cs uv2
 240     in  if ruv1==ruv2
 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
 244                    Just uc'
 245                      -> addUCS (changeUConUVar uc' ruv2) cs'  -- merge old constraints
 246                    Nothing
 247                      -> cs'
 248
 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
 252           UCBound us' _ vs'
 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)
 265           UCUsOnce _
 266             -> forceUVars UCUsOnce us jcs
 267           UCUsMany _
 268             -> forceUVars UCUsMany vs jcs
 269
 270 addUCS (UCUsOnce uv1) jcs@(Left cs)
 271   = let ruv1 = findUCon cs uv1
 272     in  case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of  -- never UCEq
 273           UCBound us _ vs
 274             -> forceUVars UCUsOnce us (Left $ extendVarEnv cs ruv1 (UCUsOnce ruv1))
 275           UCUsOnce _
 276             -> jcs
 277           UCUsMany _
 278             -> Right (text "union failed[O] at" <+> ppr uv1)
 279
 280 addUCS (UCUsMany uv1) jcs@(Left cs)
 281   = let ruv1 = findUCon cs uv1
 282     in  case lookupWithDefaultVarEnv cs (UCBound [] ruv1 []) ruv1 of  -- never UCEq
 283           UCBound us _ vs
 284             -> forceUVars UCUsMany vs (Left $ extendVarEnv cs ruv1 (UCUsMany ruv1))
 285           UCUsOnce _
 286             -> Right (text "union failed[M] at" <+> ppr uv1)
 287           UCUsMany _
 288             -> jcs
 289
 290 -- helper function forcing a set of UVars to either Once or Many:
 291 forceUVars :: (UVar -> UCon)
 292            -> [UVar]
 293            -> Either (VarEnv UCon) SDoc
 294            -> Either (VarEnv UCon) SDoc
 295 forceUVars uc uvs cs0 = foldl (\cs uv -> addUCS (uc uv) cs) cs0 uvs
 296 \end{code}
 297
 298 ======================================================================
 299
 300 Pretty-printing:
 301 ~~~~~~~~~~~~~~~~
 302
 303 \begin{code}
 304 -- Printing a usage constraint.
 305
 306 pprintUCon :: VarEnv UCon -> UCon -> SDoc
 307
 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"
 314
 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
 319
 320 pprintUCon fm (UCUsOnce uv)
 321   = ppr uv <+> text "=" <+> ppr UsOnce
 322
 323 pprintUCon fm (UCUsMany uv)
 324   = ppr uv <+> text "=" <+> ppr UsMany
 325
 326 -- Printing a usage constraint set.
 327
 328 instance Outputable UConSet where
 329   ppr (UConSet bfm)
 330     = text "UConSet:" <+> lbrace
 331       $$ vcat (map (\fm -> nest 2 (vcat (map (pprintUCon fm) (rngVarEnv fm))))
 332                    (bagToList bfm))
 333       $$ rbrace
 334
 335   ppr (UConFail d)
 336     = hang (text "UConSet inconsistent:")
 337         4 d
 338 \end{code}
 339
 340 ======================================================================
 341
 342 EOF