UnifyM.hs 17.8 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
{-# LANGUAGE Rank2Types #-}
-- | See <https://github.com/ezyang/ghc-proposals/blob/backpack/proposals/0000-backpack.rst>
module Distribution.Backpack.UnifyM (
    -- * Unification monad
    UnifyM,
    runUnifyM,
    unifyFail,
    withContext,
    liftST,

    UnifEnv(..),
    getUnifEnv,

    -- * Modules and unit IDs
    ModuleU,
    ModuleU'(..),
    convertModule,
    convertModuleU,

    UnitIdU,
    UnitIdU'(..),
    convertUnitId,
    convertUnitIdU,

    ModuleSubstU,
    convertModuleSubstU,
    convertModuleSubst,

    ModuleScopeU,
    emptyModuleScopeU,
    convertModuleScopeU,

    ModuleSourceU(..),

    convertInclude,
    convertModuleProvides,
    convertModuleProvidesU,

) where

import Prelude ()
import Distribution.Compat.Prelude hiding (mod)

import Distribution.Backpack.ModuleShape
import Distribution.Backpack.ModuleScope
import Distribution.Backpack.ModSubst
import Distribution.Backpack.FullUnitId
import Distribution.Backpack

import qualified Distribution.Utils.UnionFind as UnionFind
import Distribution.ModuleName
import Distribution.Package
import Distribution.PackageDescription
import Distribution.Text
import Distribution.Types.IncludeRenaming
56
import Distribution.Types.ComponentInclude
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184
import Distribution.Verbosity

import Data.STRef
import Control.Monad.ST
import Control.Monad
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.Traversable as T

-- TODO: more detailed trace output on high verbosity would probably
-- be appreciated by users debugging unification errors.  Collect
-- some good examples!

-- | The unification monad, this monad encapsulates imperative
-- unification.
newtype UnifyM s a = UnifyM { unUnifyM :: UnifEnv s -> ST s (Either String a) }

-- | Run a computation in the unification monad.
runUnifyM :: Verbosity -> FullDb -> (forall s. UnifyM s a) -> Either String a
runUnifyM verbosity db m
    = runST $ do i    <- newSTRef 0
                 hmap <- newSTRef Map.empty
                 unUnifyM m (UnifEnv i hmap verbosity Nothing db)
-- NB: GHC 7.6 throws a hissy fit if you pattern match on 'm'.

-- | The unification environment.
data UnifEnv s = UnifEnv {
        -- | A supply of unique integers to label 'UnitIdU'
        -- cells.  This is used to determine loops in unit
        -- identifiers (which can happen with mutual recursion.)
        unify_uniq :: UnifRef s UnitIdUnique,
        -- | The set of requirements in scope.  When
        -- a provision is brought into scope, we unify with
        -- the requirement at the same module name to fill it.
        -- This mapping grows monotonically.
        unify_reqs :: UnifRef s (Map ModuleName (ModuleU s)),
        -- | How verbose the error message should be
        unify_verbosity :: Verbosity,
        -- | The error reporting context
        unify_ctx :: Maybe (String, ModuleU s, ModuleU s),
        -- | The package index for expanding unit identifiers
        unify_db :: FullDb
    }

instance Functor (UnifyM s) where
    fmap f (UnifyM m) = UnifyM (fmap (fmap (fmap f)) m)

instance Applicative (UnifyM s) where
    pure = UnifyM . pure . pure . pure
    UnifyM f <*> UnifyM x = UnifyM $ \r -> do
        f' <- f r
        case f' of
          Left err -> return (Left err)
          Right f'' -> do
              x' <- x r
              case x' of
                  Left err -> return (Left err)
                  Right x'' -> return (Right (f'' x''))

instance Monad (UnifyM s) where
    return = pure
    UnifyM m >>= f = UnifyM $ \r -> do
        x <- m r
        case x of
            Left err -> return (Left err)
            Right x' -> unUnifyM (f x') r

-- | Lift a computation from 'ST' monad to 'UnifyM' monad.
-- Internal use only.
liftST :: ST s a -> UnifyM s a
liftST m = UnifyM $ \_ -> fmap Right m

unifyFail :: String -> UnifyM s a
unifyFail err = do
    env <- getUnifEnv
    msg <- case unify_ctx env of
        Nothing -> return ("Unspecified unification error: " ++ err)
        Just (ctx, mod1, mod2)
            | unify_verbosity env > normal
            -> do mod1' <- convertModuleU mod1
                  mod2' <- convertModuleU mod2
                  let extra = " (was unifying " ++ display mod1'
                                     ++ " and " ++ display mod2' ++ ")"
                  return (ctx ++ err ++ extra)
            | otherwise
            -> return (ctx ++ err ++ " (for more information, pass -v flag)")
    UnifyM $ \_ -> return (Left msg)

-- | A convenient alias for mutable references in the unification monad.
type UnifRef s a = STRef s a

-- | Imperatively read a 'UnifRef'.
readUnifRef :: UnifRef s a -> UnifyM s a
readUnifRef = liftST . readSTRef

-- | Imperatively write a 'UnifRef'.
writeUnifRef :: UnifRef s a -> a -> UnifyM s ()
writeUnifRef x = liftST . writeSTRef x

-- | Get the current unification environment.
getUnifEnv :: UnifyM s (UnifEnv s)
getUnifEnv = UnifyM $ \r -> return (Right r)

-- | Run a unification in some context
withContext :: String -> ModuleU s -> ModuleU s -> UnifyM s a -> UnifyM s a
withContext ctx mod1 mod2 m =
    UnifyM $ \r -> unUnifyM m r { unify_ctx = Just (ctx, mod1, mod2) }

-----------------------------------------------------------------------
-- The "unifiable" variants of the data types
--
-- In order to properly do unification over infinite trees, we
-- need to union find over 'Module's and 'UnitId's.  The pure
-- representation is ill-equipped to do this, so we convert
-- from the pure representation into one which is indirected
-- through union-find.  'ModuleU' handles hole variables;
-- 'UnitIdU' handles mu-binders.

-- | Contents of a mutable 'ModuleU' reference.
data ModuleU' s
    = ModuleU (UnitIdU s) ModuleName
    | ModuleVarU ModuleName

-- | Contents of a mutable 'UnitIdU' reference.
data UnitIdU' s
    = UnitIdU UnitIdUnique ComponentId (Map ModuleName (ModuleU s))
185
    | UnitIdThunkU DefUnitId
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236

-- | A mutable version of 'Module' which can be imperatively unified.
type ModuleU s = UnionFind.Point s (ModuleU' s)

-- | A mutable version of 'UnitId' which can be imperatively unified.
type UnitIdU s = UnionFind.Point s (UnitIdU' s)

-- | An integer for uniquely labeling 'UnitIdU' nodes.  We need
-- these labels in order to efficiently serialize 'UnitIdU's into
-- 'UnitId's (we use the label to check if any parent is the
-- node in question, and if so insert a deBruijn index instead.)
-- These labels must be unique across all 'UnitId's/'Module's which
-- participate in unification!
type UnitIdUnique = Int


-----------------------------------------------------------------------
-- Conversion to the unifiable data types

-- An environment for tracking the mu-bindings in scope.
-- The invariant for a state @(m, i)@ is that [0..i] are
-- keys of @m@; in fact, the @i-k@th entry is the @k@th
-- de Bruijn index (this saves us from having to shift as
-- we enter mu-binders.)
type MuEnv s = (IntMap (UnitIdU s), Int)

extendMuEnv :: MuEnv s -> UnitIdU s -> MuEnv s
extendMuEnv (m, i) x =
    (IntMap.insert (i + 1) x m, i + 1)

{-
lookupMuEnv :: MuEnv s -> Int {- de Bruijn index -} -> UnitIdU s
lookupMuEnv (m, i) k =
    case IntMap.lookup (i - k) m of
        -- Technically a user can trigger this by giving us a
        -- bad 'UnitId', so handle this better.
        Nothing -> error "lookupMuEnv: out of bounds (malformed de Bruijn index)"
        Just v -> v
-}

emptyMuEnv :: MuEnv s
emptyMuEnv = (IntMap.empty, -1)

-- The workhorse functions.  These share an environment:
--   * @UnifRef s UnitIdUnique@ - the unique label supply for 'UnitIdU' nodes
--   * @UnifRef s (Map ModuleName moduleU)@ - the (lazily initialized)
--     environment containing the implicitly universally quantified
--     @hole:A@ binders.
--   * @MuEnv@ - the environment for mu-binders.

convertUnitId' :: MuEnv s
237
               -> OpenUnitId
238 239 240
               -> UnifyM s (UnitIdU s)
-- TODO: this could be more lazy if we know there are no internal
-- references
241
convertUnitId' _ (DefiniteUnitId uid) =
242 243 244 245 246 247 248 249 250 251 252 253 254
    liftST $ UnionFind.fresh (UnitIdThunkU uid)
convertUnitId' stk (IndefFullUnitId cid insts) = do
    fs <- fmap unify_uniq getUnifEnv
    x <- liftST $ UnionFind.fresh (error "convertUnitId") -- tie the knot later
    insts_u <- T.forM insts $ convertModule' (extendMuEnv stk x)
    u <- readUnifRef fs
    writeUnifRef fs (u+1)
    y <- liftST $ UnionFind.fresh (UnitIdU u cid insts_u)
    liftST $ UnionFind.union x y
    return y
-- convertUnitId' stk (UnitIdVar i) = return (lookupMuEnv stk i)

convertModule' :: MuEnv s
255 256
               -> OpenModule -> UnifyM s (ModuleU s)
convertModule' _stk (OpenModuleVar mod_name) = do
257 258 259 260 261 262 263
    hmap <- fmap unify_reqs getUnifEnv
    hm <- readUnifRef hmap
    case Map.lookup mod_name hm of
        Nothing -> do mod <- liftST $ UnionFind.fresh (ModuleVarU mod_name)
                      writeUnifRef hmap (Map.insert mod_name mod hm)
                      return mod
        Just mod -> return mod
264
convertModule' stk (OpenModule uid mod_name) = do
265 266 267
    uid_u <- convertUnitId' stk uid
    liftST $ UnionFind.fresh (ModuleU uid_u mod_name)

268
convertUnitId :: OpenUnitId -> UnifyM s (UnitIdU s)
269 270
convertUnitId = convertUnitId' emptyMuEnv

271
convertModule :: OpenModule -> UnifyM s (ModuleU s)
272 273 274 275 276 277 278 279 280 281 282
convertModule = convertModule' emptyMuEnv



-----------------------------------------------------------------------
-- Substitutions

-- | The mutable counterpart of a 'ModuleSubst' (not defined here).
type ModuleSubstU s = Map ModuleName (ModuleU s)

-- | Conversion of 'ModuleSubst' to 'ModuleSubstU'
283
convertModuleSubst :: Map ModuleName OpenModule -> UnifyM s (Map ModuleName (ModuleU s))
284 285 286
convertModuleSubst = T.mapM convertModule

-- | Conversion of 'ModuleSubstU' to 'ModuleSubst'
287
convertModuleSubstU :: ModuleSubstU s -> UnifyM s OpenModuleSubst
288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313
convertModuleSubstU = T.mapM convertModuleU

-----------------------------------------------------------------------
-- Conversion from the unifiable data types

-- An environment for tracking candidates for adding a mu-binding.
-- The invariant for a state @(m, i)@, is that if we encounter a node
-- labeled @k@ such that @m[k -> v]@, then we can replace this
-- node with the de Bruijn index @i-v@ referring to an enclosing
-- mu-binder; furthermore, @range(m) = [0..i]@.
type MooEnv = (IntMap Int, Int)

emptyMooEnv :: MooEnv
emptyMooEnv = (IntMap.empty, -1)

extendMooEnv :: MooEnv -> UnitIdUnique -> MooEnv
extendMooEnv (m, i) k = (IntMap.insert k (i + 1) m, i + 1)

lookupMooEnv :: MooEnv -> UnitIdUnique -> Maybe Int
lookupMooEnv (m, i) k =
    case IntMap.lookup k m of
        Nothing -> Nothing
        Just v -> Just (i-v) -- de Bruijn indexize

-- The workhorse functions

314
convertUnitIdU' :: MooEnv -> UnitIdU s -> UnifyM s OpenUnitId
315 316 317
convertUnitIdU' stk uid_u = do
    x <- liftST $ UnionFind.find uid_u
    case x of
318
        UnitIdThunkU uid -> return (DefiniteUnitId uid)
319 320 321 322 323 324 325
        UnitIdU u cid insts_u ->
            case lookupMooEnv stk u of
                Just _i -> error "convertUnitIdU': mutual recursion" -- return (UnitIdVar i)
                Nothing -> do
                    insts <- T.forM insts_u $ convertModuleU' (extendMooEnv stk u)
                    return (IndefFullUnitId cid insts)

326
convertModuleU' :: MooEnv -> ModuleU s -> UnifyM s OpenModule
327 328 329
convertModuleU' stk mod_u = do
    mod <- liftST $ UnionFind.find mod_u
    case mod of
330
        ModuleVarU mod_name -> return (OpenModuleVar mod_name)
331 332
        ModuleU uid_u mod_name -> do
            uid <- convertUnitIdU' stk uid_u
333
            return (OpenModule uid mod_name)
334 335 336

-- Helper functions

337
convertUnitIdU :: UnitIdU s -> UnifyM s OpenUnitId
338 339
convertUnitIdU = convertUnitIdU' emptyMooEnv

340
convertModuleU :: ModuleU s -> UnifyM s OpenModule
341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364
convertModuleU = convertModuleU' emptyMooEnv

-- | An empty 'ModuleScopeU'.
emptyModuleScopeU :: ModuleScopeU s
emptyModuleScopeU = (Map.empty, Map.empty)


-- | The mutable counterpart of 'ModuleScope'.
type ModuleScopeU s = (ModuleProvidesU s, ModuleSubstU s)
-- | The mutable counterpart of 'ModuleProvides'
type ModuleProvidesU s = Map ModuleName [ModuleSourceU s]
data ModuleSourceU s =
    ModuleSourceU {
        -- We don't have line numbers, but if we did the
        -- package name and renaming could be associated
        -- with that as well
        usrc_pkgname :: PackageName,
        usrc_renaming :: IncludeRenaming,
        usrc_module :: ModuleU s
    }

-- | Convert a 'ModuleShape' into a 'ModuleScopeU', so we can do
-- unification on it.
convertInclude
365 366 367 368 369 370 371
    :: ComponentInclude (OpenUnitId, ModuleShape) IncludeRenaming
    -> UnifyM s (ModuleScopeU s, ComponentInclude (UnitIdU s) ModuleRenaming)
convertInclude (ComponentInclude {
                    ci_id = (uid, ModuleShape provs reqs),
                    ci_pkgid = pid,
                    ci_renaming = incl@(IncludeRenaming prov_rns req_rns)
               }) = do
372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407
    let pn = packageName pid

    -- Suppose our package has two requirements A and B, and
    -- we include it with @requires (A as X)@
    -- There are three closely related things we compute based
    -- off of @reqs@ and @reqs_rns@:
    --
    --      1. The requirement renaming (A -> X)
    --      2. The requirement substitution (A -> <X>, B -> <B>)

    -- Requirement renaming.  This is read straight off the syntax:
    --
    --      [nothing]          ==>  [empty]
    --      requires (B as Y)  ==>  B -> Y
    --
    -- Requirement renamings are NOT injective: if two requirements
    -- are mapped to the same name, the intent is to merge them
    -- together.  But they are *functions*, so @B as X, B as Y@ is
    -- illegal.
    let insertDistinct m (k,v) =
            if Map.member k m
                then error ("Duplicate requirement renaming " ++ display k)
                else return (Map.insert k v m)
    req_rename <- foldM insertDistinct Map.empty =<<
                      case req_rns of
                        DefaultRenaming -> return []
                        -- Not valid here, but whatever
                        HidingRenaming _ -> error "Cannot use hiding in requirement renaming"
                        ModuleRenaming rns -> return rns
    let req_rename_fn k = case Map.lookup k req_rename of
                            Nothing -> k
                            Just v  -> v

    -- Requirement substitution.
    --
    --      A -> X      ==>     A -> <X>
408
    let req_subst = fmap OpenModuleVar req_rename
409 410 411 412 413 414 415 416 417 418

    uid_u <- convertUnitId (modSubst req_subst uid)

    -- Requirement mapping.  This is just taking the range of the
    -- requirement substitution, and making a mapping so that it is
    -- convenient to merge things together.  It INCLUDES the implicit
    -- mappings.
    --
    --      A -> X      ==>     X -> <X>, B -> <B>
    reqs_u <- convertModuleSubst . Map.fromList $
419
                [ (k, OpenModuleVar k)
420 421 422
                | k <- map req_rename_fn (Set.toList reqs)
                ]

423 424 425 426 427 428 429
    -- Report errors if there were unused renamings
    let leftover = Map.keysSet req_rename `Set.difference` reqs
    unless (Set.null leftover) $
        error $ "Attempted to rename the following requirements, which " ++
                "were not actually requirements of " ++ display uid ++ ": " ++
                intercalate ", " (map display (Set.toList leftover))

430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457
    -- Provision computation is more complex.
    -- For example, if we have:
    --
    --      include p (A as X) requires (B as Y)
    --          where A -> q[B=<B>]:A
    --
    -- Then we need:
    --
    --      X -> [("p", q[B=<B>]:A)]
    --
    -- There are a bunch of clever ways to present the algorithm
    -- but here is the simple one:
    --
    --      1. If we have a default renaming, apply req_subst
    --      to provs and use that.
    --
    --      2. Otherwise, build a map by successively looking
    --      up the referenced modules in the renaming in provs.
    --
    -- Importantly, overlapping rename targets get accumulated
    -- together.  It's not an (immediate) error.
    (pre_prov_scope, prov_rns') <-
        case prov_rns of
            DefaultRenaming -> return (Map.toList provs, prov_rns)
            HidingRenaming hides ->
                let hides_set = Set.fromList hides
                in let r = [ (k,v)
                           | (k,v) <- Map.toList provs
458
                           , not (k `Set.member` hides_set) ]
459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474
                   -- GHC doesn't understand hiding, so expand it out!
                   in return (r, ModuleRenaming (map ((\x -> (x,x)).fst) r))
            ModuleRenaming rns -> do
              r <- sequence
                [ case Map.lookup from provs of
                    Just m -> return (to, m)
                    Nothing -> error ("Tried to rename non-existent module " ++ display from)
                | (from, to) <- rns ]
              return (r, prov_rns)
    let prov_scope = modSubst req_subst
                   $ Map.fromListWith (++)
                   [ (k, [ModuleSource pn incl v])
                   | (k, v) <- pre_prov_scope ]

    provs_u <- convertModuleProvides prov_scope

475
    return ((provs_u, reqs_u), ComponentInclude uid_u pid prov_rns')
476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498

-- | Convert a 'ModuleScopeU' to a 'ModuleScope'.
convertModuleScopeU :: ModuleScopeU s -> UnifyM s ModuleScope
convertModuleScopeU (provs_u, reqs_u) = do
    provs <- convertModuleProvidesU provs_u
    reqs  <- convertModuleSubstU reqs_u
    -- TODO: Test that the requirements are still free. If they
    -- are not, they got unified, and that's dodgy at best.
    return (ModuleScope provs (Map.keysSet reqs))

-- | Convert a 'ModuleProvides' to a 'ModuleProvidesU'
convertModuleProvides :: ModuleProvides -> UnifyM s (ModuleProvidesU s)
convertModuleProvides = T.mapM $ \ms ->
    mapM (\(ModuleSource pn incl m)
            -> do m' <- convertModule m
                  return (ModuleSourceU pn incl m')) ms

-- | Convert a 'ModuleProvidesU' to a 'ModuleProvides'
convertModuleProvidesU :: ModuleProvidesU s -> UnifyM s ModuleProvides
convertModuleProvidesU = T.mapM $ \ms ->
    mapM (\(ModuleSourceU pn incl m)
            -> do m' <- convertModuleU m
                  return (ModuleSource pn incl m')) ms