content: 
  module DDC.Core.Discus.Convert.Type.Witness
          ( convertCapabilityB
          , convertCapabilityT)
  where
  import DDC.Core.Discus.Convert.Type.Region
  import DDC.Core.Discus.Convert.Type.Base
  import DDC.Core.Discus.Convert.Error
  import DDC.Core.Exp.Annot
  import DDC.Control.Check                        (throw)
  import qualified DDC.Core.Discus.Prim            as E
  import qualified DDC.Core.Salt.Name             as A
  import Control.Monad
  import DDC.Data.Pretty
  
  
  -- | Convert a witness binder.
  convertCapabilityB :: Context -> Bind E.Name -> ConvertM a (Bind A.Name)
  convertCapabilityB ctx bb
   = case bb of
          BNone t         -> liftM  BNone (convertCapabilityT ctx t)
          BAnon t         -> liftM  BAnon (convertCapabilityT ctx t)
          BName n t       -> liftM2 BName (convertBindNameM n) (convertCapabilityT ctx t)
  
  
  -- | Convert a capability / coeffect type to Salt.
  --   Works for Read#, Write#, Alloc#
  convertCapabilityT :: Context -> Type E.Name -> ConvertM a (Type A.Name)
  convertCapabilityT ctx tt
           | Just (TyConSpec tc, [tR])    <- takeTyConApps tt
           = do   tR'     <- convertRegionT ctx tR
                  case tc of
                   TcConRead       -> return $ tRead  tR'
                   TcConWrite      -> return $ tWrite tR'
                   TcConAlloc      -> return $ tAlloc tR'
                   _ -> throw $ ErrorMalformed
                              $ "Malformed capability type " ++ (renderIndent $ ppr tt)
  
          | otherwise
          = throw $ ErrorMalformed
                  $ "Malformed capability type " ++ (renderIndent $ ppr tt)
  
  