    -- |
    -- Module      :  Cryptol.TypeCheck.AST
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE Safe                                #-}

    {-# LANGUAGE RecordWildCards                     #-}
    {-# LANGUAGE PatternGuards                       #-}
    {-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
    {-# LANGUAGE DeriveAnyClass, DeriveGeneric       #-}
    {-# LANGUAGE OverloadedStrings                   #-}
    module Cryptol.TypeCheck.AST
      ( module Cryptol.TypeCheck.AST
      , Name()
      , TFun(..)
      , Selector(..)
      , Import(..)
      , ImportSpec(..)
      , ExportType(..)
      , ExportSpec(..), isExportedBind, isExportedType
      , Pragma(..)
      , Fixity(..)
      , PrimMap(..)
      , TCErrorMessage(..)
      , module Cryptol.TypeCheck.Type
      ) where

    import Cryptol.Parser.Position(Located)
    import Cryptol.ModuleSystem.Name
    import Cryptol.ModuleSystem.Exports(ExportSpec(..)
                                       , isExportedBind, isExportedType)
    import Cryptol.Parser.AST ( Selector(..),Pragma(..)
                              , Import(..), ImportSpec(..), ExportType(..)
                              , Fixity(..))
    import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent)
    import Cryptol.TypeCheck.PP
    import Cryptol.TypeCheck.Type

    import GHC.Generics (Generic)
    import Control.DeepSeq

    import           Data.Map    (Map)
    import qualified Data.Map    as Map
    import qualified Data.IntMap as IntMap

    -- | A Cryptol module.
    data Module = Module { Module -> ModName
    mName        :: !ModName
                         , Module -> ExportSpec Name
    mExports     :: ExportSpec Name
                         , Module -> [Import]
    mImports     :: [Import]

                         , Module -> Map Name TySyn
    mTySyns      :: Map Name TySyn
                           -- ^ This is just the type-level type synonyms
                           -- of a module.

                         , Module -> Map Name Newtype
    mNewtypes         :: Map Name Newtype
                         , Module -> Map Name AbstractType
    mPrimTypes        :: Map Name AbstractType
                         , Module -> Map Name ModTParam
    mParamTypes       :: Map Name ModTParam
                         , Module -> [Located Prop]
    mParamConstraints :: [Located Prop]
                         , Module -> Map Name ModVParam
    mParamFuns        :: Map Name ModVParam
                         , Module -> [DeclGroup]
    mDecls            :: [DeclGroup]
                         } deriving (Int -> Module -> ShowS
    [Module] -> ShowS
    Module -> String
    (Int -> Module -> ShowS)
    -> (Module -> String) -> ([Module] -> ShowS) -> Show Module
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Module] -> ShowS
    $cshowList :: [Module] -> ShowS
    show :: Module -> String
    $cshow :: Module -> String
    showsPrec :: Int -> Module -> ShowS
    $cshowsPrec :: Int -> Module -> ShowS
    Show, (forall x. Module -> Rep Module x)
    -> (forall x. Rep Module x -> Module) -> Generic Module
    forall x. Rep Module x -> Module
    forall x. Module -> Rep Module x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Module x -> Module
    $cfrom :: forall x. Module -> Rep Module x
    Generic, Module -> ()
    (Module -> ()) -> NFData Module
    forall a. (a -> ()) -> NFData a
    rnf :: Module -> ()
    $crnf :: Module -> ()
    NFData)

    -- | Is this a parameterized module?
    isParametrizedModule :: Module -> Bool
    isParametrizedModule :: Module -> Bool
    isParametrizedModule m :: Module
    m = Bool -> Bool
    not (Map Name ModTParam -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (Module -> Map Name ModTParam
    mParamTypes Module
    m) Bool -> Bool -> Bool
    &&
                                  [Located Prop] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (Module -> [Located Prop]
    mParamConstraints Module
    m) Bool -> Bool -> Bool
    &&
                                  Map Name ModVParam -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (Module -> Map Name ModVParam
    mParamFuns Module
    m))

    -- | A type parameter of a module.
    data ModTParam = ModTParam
      { ModTParam -> Name
    mtpName   :: Name
      , ModTParam -> Kind
    mtpKind   :: Kind
      , ModTParam -> Int
    mtpNumber :: !Int -- ^ The number of the parameter in the module
                          -- This is used when we move parameters from the module
                          -- level to individual declarations
                          -- (type synonyms in particular)
      , ModTParam -> Maybe String
    mtpDoc    :: Maybe String
      } deriving (Int -> ModTParam -> ShowS
    [ModTParam] -> ShowS
    ModTParam -> String
    (Int -> ModTParam -> ShowS)
    -> (ModTParam -> String)
    -> ([ModTParam] -> ShowS)
    -> Show ModTParam
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [ModTParam] -> ShowS
    $cshowList :: [ModTParam] -> ShowS
    show :: ModTParam -> String
    $cshow :: ModTParam -> String
    showsPrec :: Int -> ModTParam -> ShowS
    $cshowsPrec :: Int -> ModTParam -> ShowS
    Show,(forall x. ModTParam -> Rep ModTParam x)
    -> (forall x. Rep ModTParam x -> ModTParam) -> Generic ModTParam
    forall x. Rep ModTParam x -> ModTParam
    forall x. ModTParam -> Rep ModTParam x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep ModTParam x -> ModTParam
    $cfrom :: forall x. ModTParam -> Rep ModTParam x
    Generic,ModTParam -> ()
    (ModTParam -> ()) -> NFData ModTParam
    forall a. (a -> ()) -> NFData a
    rnf :: ModTParam -> ()
    $crnf :: ModTParam -> ()
    NFData)

    mtpParam :: ModTParam -> TParam
    mtpParam :: ModTParam -> TParam
    mtpParam mtp :: ModTParam
    mtp = $WTParam :: Int -> Kind -> TPFlavor -> TVarInfo -> TParam
    TParam { tpUnique :: Int
    tpUnique = Name -> Int
    nameUnique (ModTParam -> Name
    mtpName ModTParam
    mtp)
                          , tpKind :: Kind
    tpKind   = ModTParam -> Kind
    mtpKind ModTParam
    mtp
                          , tpFlav :: TPFlavor
    tpFlav   = Name -> TPFlavor
    TPModParam (ModTParam -> Name
    mtpName ModTParam
    mtp)
                          , tpInfo :: TVarInfo
    tpInfo   = TVarInfo
    desc
                          }
      where desc :: TVarInfo
    desc = TVarInfo :: Range -> TVarSource -> TVarInfo
    TVarInfo { tvarDesc :: TVarSource
    tvarDesc   = Name -> TVarSource
    TVFromModParam (ModTParam -> Name
    mtpName ModTParam
    mtp)
                            , tvarSource :: Range
    tvarSource = Name -> Range
    nameLoc (ModTParam -> Name
    mtpName ModTParam
    mtp)
                            }

    -- | A value parameter of a module.
    data ModVParam = ModVParam
      { ModVParam -> Name
    mvpName   :: Name
      , ModVParam -> Schema
    mvpType   :: Schema
      , ModVParam -> Maybe String
    mvpDoc    :: Maybe String
      , ModVParam -> Maybe Fixity
    mvpFixity :: Maybe Fixity
      } deriving (Int -> ModVParam -> ShowS
    [ModVParam] -> ShowS
    ModVParam -> String
    (Int -> ModVParam -> ShowS)
    -> (ModVParam -> String)
    -> ([ModVParam] -> ShowS)
    -> Show ModVParam
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [ModVParam] -> ShowS
    $cshowList :: [ModVParam] -> ShowS
    show :: ModVParam -> String
    $cshow :: ModVParam -> String
    showsPrec :: Int -> ModVParam -> ShowS
    $cshowsPrec :: Int -> ModVParam -> ShowS
    Show,(forall x. ModVParam -> Rep ModVParam x)
    -> (forall x. Rep ModVParam x -> ModVParam) -> Generic ModVParam
    forall x. Rep ModVParam x -> ModVParam
    forall x. ModVParam -> Rep ModVParam x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep ModVParam x -> ModVParam
    $cfrom :: forall x. ModVParam -> Rep ModVParam x
    Generic,ModVParam -> ()
    (ModVParam -> ()) -> NFData ModVParam
    forall a. (a -> ()) -> NFData a
    rnf :: ModVParam -> ()
    $crnf :: ModVParam -> ()
    NFData)

    data Expr   = EList [Expr] Type         -- ^ List value (with type of elements)
                | ETuple [Expr]             -- ^ Tuple value
                | ERec [(Ident,Expr)]       -- ^ Record value
                | ESel Expr Selector        -- ^ Elimination for tuple/record/list
                | ESet Expr Selector Expr   -- ^ Change the value of a field.

                | EIf Expr Expr Expr        -- ^ If-then-else
                | EComp Type Type Expr [[Match]]
                                            -- ^ List comprehensions
                                            --   The types cache the length of the
                                            --   sequence and its element type.

                | EVar Name                 -- ^ Use of a bound variable

                | ETAbs TParam Expr         -- ^ Function Value
                | ETApp Expr Type           -- ^ Type application

                | EApp Expr Expr            -- ^ Function application
                | EAbs Name Type Expr       -- ^ Function value

                {- | Proof abstraction.  Because we don't keep proofs around
                     we don't need to name the assumption, but we still need to
                     record the assumption.  The assumption is the `Type` term,
                     which should be of kind `KProp`.
                 -}
                | EProofAbs {- x -} Prop Expr

                {- | If `e : p => t`, then `EProofApp e : t`,
                     as long as we can prove `p`.

                     We don't record the actual proofs, as they are not
                     used for anything.  It may be nice to keep them around
                     for sanity checking.
                 -}

                | EProofApp Expr {- proof -}

                | EWhere Expr [DeclGroup]

                  deriving (Int -> Expr -> ShowS
    [Expr] -> ShowS
    Expr -> String
    (Int -> Expr -> ShowS)
    -> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Expr] -> ShowS
    $cshowList :: [Expr] -> ShowS
    show :: Expr -> String
    $cshow :: Expr -> String
    showsPrec :: Int -> Expr -> ShowS
    $cshowsPrec :: Int -> Expr -> ShowS
    Show, (forall x. Expr -> Rep Expr x)
    -> (forall x. Rep Expr x -> Expr) -> Generic Expr
    forall x. Rep Expr x -> Expr
    forall x. Expr -> Rep Expr x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Expr x -> Expr
    $cfrom :: forall x. Expr -> Rep Expr x
    Generic, Expr -> ()
    (Expr -> ()) -> NFData Expr
    forall a. (a -> ()) -> NFData a
    rnf :: Expr -> ()
    $crnf :: Expr -> ()
    NFData)

    data Match  = From Name Type Type Expr
                                      -- ^ Type arguments are the length and element
                                      --   type of the sequence expression
                | Let Decl
                  deriving (Int -> Match -> ShowS
    [Match] -> ShowS
    Match -> String
    (Int -> Match -> ShowS)
    -> (Match -> String) -> ([Match] -> ShowS) -> Show Match
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Match] -> ShowS
    $cshowList :: [Match] -> ShowS
    show :: Match -> String
    $cshow :: Match -> String
    showsPrec :: Int -> Match -> ShowS
    $cshowsPrec :: Int -> Match -> ShowS
    Show, (forall x. Match -> Rep Match x)
    -> (forall x. Rep Match x -> Match) -> Generic Match
    forall x. Rep Match x -> Match
    forall x. Match -> Rep Match x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Match x -> Match
    $cfrom :: forall x. Match -> Rep Match x
    Generic, Match -> ()
    (Match -> ()) -> NFData Match
    forall a. (a -> ()) -> NFData a
    rnf :: Match -> ()
    $crnf :: Match -> ()
    NFData)

    data DeclGroup  = Recursive   [Decl]    -- ^ Mutually recursive declarations
                    | NonRecursive Decl     -- ^ Non-recursive declaration
                      deriving (Int -> DeclGroup -> ShowS
    [DeclGroup] -> ShowS
    DeclGroup -> String
    (Int -> DeclGroup -> ShowS)
    -> (DeclGroup -> String)
    -> ([DeclGroup] -> ShowS)
    -> Show DeclGroup
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [DeclGroup] -> ShowS
    $cshowList :: [DeclGroup] -> ShowS
    show :: DeclGroup -> String
    $cshow :: DeclGroup -> String
    showsPrec :: Int -> DeclGroup -> ShowS
    $cshowsPrec :: Int -> DeclGroup -> ShowS
    Show, (forall x. DeclGroup -> Rep DeclGroup x)
    -> (forall x. Rep DeclGroup x -> DeclGroup) -> Generic DeclGroup
    forall x. Rep DeclGroup x -> DeclGroup
    forall x. DeclGroup -> Rep DeclGroup x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep DeclGroup x -> DeclGroup
    $cfrom :: forall x. DeclGroup -> Rep DeclGroup x
    Generic, DeclGroup -> ()
    (DeclGroup -> ()) -> NFData DeclGroup
    forall a. (a -> ()) -> NFData a
    rnf :: DeclGroup -> ()
    $crnf :: DeclGroup -> ()
    NFData)

    groupDecls :: DeclGroup -> [Decl]
    groupDecls :: DeclGroup -> [Decl]
    groupDecls dg :: DeclGroup
    dg = case DeclGroup
    dg of
      Recursive ds :: [Decl]
    ds   -> [Decl]
    ds
      NonRecursive d :: Decl
    d -> [Decl
    d]

    data Decl       = Decl { Decl -> Name
    dName        :: !Name
                           , Decl -> Schema
    dSignature   :: Schema
                           , Decl -> DeclDef
    dDefinition  :: DeclDef
                           , Decl -> [Pragma]
    dPragmas     :: [Pragma]
                           , Decl -> Bool
    dInfix       :: !Bool
                           , Decl -> Maybe Fixity
    dFixity      :: Maybe Fixity
                           , Decl -> Maybe String
    dDoc         :: Maybe String
                           } deriving ((forall x. Decl -> Rep Decl x)
    -> (forall x. Rep Decl x -> Decl) -> Generic Decl
    forall x. Rep Decl x -> Decl
    forall x. Decl -> Rep Decl x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Decl x -> Decl
    $cfrom :: forall x. Decl -> Rep Decl x
    Generic, Decl -> ()
    (Decl -> ()) -> NFData Decl
    forall a. (a -> ()) -> NFData a
    rnf :: Decl -> ()
    $crnf :: Decl -> ()
    NFData, Int -> Decl -> ShowS
    [Decl] -> ShowS
    Decl -> String
    (Int -> Decl -> ShowS)
    -> (Decl -> String) -> ([Decl] -> ShowS) -> Show Decl
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Decl] -> ShowS
    $cshowList :: [Decl] -> ShowS
    show :: Decl -> String
    $cshow :: Decl -> String
    showsPrec :: Int -> Decl -> ShowS
    $cshowsPrec :: Int -> Decl -> ShowS
    Show)

    data DeclDef    = DPrim
                    | DExpr Expr
                      deriving (Int -> DeclDef -> ShowS
    [DeclDef] -> ShowS
    DeclDef -> String
    (Int -> DeclDef -> ShowS)
    -> (DeclDef -> String) -> ([DeclDef] -> ShowS) -> Show DeclDef
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [DeclDef] -> ShowS
    $cshowList :: [DeclDef] -> ShowS
    show :: DeclDef -> String
    $cshow :: DeclDef -> String
    showsPrec :: Int -> DeclDef -> ShowS
    $cshowsPrec :: Int -> DeclDef -> ShowS
    Show, (forall x. DeclDef -> Rep DeclDef x)
    -> (forall x. Rep DeclDef x -> DeclDef) -> Generic DeclDef
    forall x. Rep DeclDef x -> DeclDef
    forall x. DeclDef -> Rep DeclDef x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep DeclDef x -> DeclDef
    $cfrom :: forall x. DeclDef -> Rep DeclDef x
    Generic, DeclDef -> ()
    (DeclDef -> ()) -> NFData DeclDef
    forall a. (a -> ()) -> NFData a
    rnf :: DeclDef -> ()
    $crnf :: DeclDef -> ()
    NFData)

    --------------------------------------------------------------------------------

    -- | Construct a primitive, given a map to the unique names of the Cryptol
    -- module.
    ePrim :: PrimMap -> Ident -> Expr
    ePrim :: PrimMap -> Ident -> Expr
    ePrim pm :: PrimMap
    pm n :: Ident
    n = Name -> Expr
    EVar (Ident -> PrimMap -> Name
    lookupPrimDecl Ident
    n PrimMap
    pm)

    -- | Make an expression that is `error` pre-applied to a type and a message.
    eError :: PrimMap -> Type -> String -> Expr
    eError :: PrimMap -> Prop -> String -> Expr
    eError prims :: PrimMap
    prims t :: Prop
    t str :: String
    str =
      Expr -> Expr -> Expr
    EApp (Expr -> Prop -> Expr
    ETApp (Expr -> Prop -> Expr
    ETApp (PrimMap -> Ident -> Expr
    ePrim PrimMap
    prims (String -> Ident
    packIdent "error")) Prop
    t)
                  (Int -> Prop
    forall a. Integral a => a -> Prop
    tNum (String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    str))) (PrimMap -> String -> Expr
    eString PrimMap
    prims String
    str)

    eString :: PrimMap -> String -> Expr
    eString :: PrimMap -> String -> Expr
    eString prims :: PrimMap
    prims str :: String
    str = [Expr] -> Prop -> Expr
    EList ((Char -> Expr) -> String -> [Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map (PrimMap -> Char -> Expr
    eChar PrimMap
    prims) String
    str) Prop
    tChar

    eChar :: PrimMap -> Char -> Expr
    eChar :: PrimMap -> Char -> Expr
    eChar prims :: PrimMap
    prims c :: Char
    c = Expr -> Prop -> Expr
    ETApp (Expr -> Prop -> Expr
    ETApp (PrimMap -> Ident -> Expr
    ePrim PrimMap
    prims (String -> Ident
    packIdent "number")) (Int -> Prop
    forall a. Integral a => a -> Prop
    tNum Int
    v)) (Prop -> Prop
    tWord (Int -> Prop
    forall a. Integral a => a -> Prop
    tNum Int
    w))
      where v :: Int
    v = Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    c
            w :: Int
    w = 8 :: Int

    instance PP (WithNames Expr) where
      ppPrec :: Int -> WithNames Expr -> Doc
    ppPrec prec :: Int
    prec (WithNames expr :: Expr
    expr nm :: NameMap
    nm) =
        case Expr
    expr of
          EList [] t :: Prop
    t    -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 0)
                        (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    text "[]" Doc -> Doc -> Doc
    <+> Doc
    colon Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    ppWP Int
    prec Prop
    t

          EList es :: [Expr]
    es _    -> Doc -> Doc
    brackets (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    sep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (Expr -> Doc) -> [Expr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr -> Doc
    forall a. PP (WithNames a) => a -> Doc
    ppW [Expr]
    es

          ETuple es :: [Expr]
    es     -> Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    sep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (Expr -> Doc) -> [Expr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr -> Doc
    forall a. PP (WithNames a) => a -> Doc
    ppW [Expr]
    es

          ERec fs :: [(Ident, Expr)]
    fs       -> Doc -> Doc
    braces (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    sep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma
                            [ Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    f Doc -> Doc -> Doc
    <+> String -> Doc
    text "=" Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall a. PP (WithNames a) => a -> Doc
    ppW Expr
    e | (f :: Ident
    f,e :: Expr
    e) <- [(Ident, Expr)]
    fs ]

          ESel e :: Expr
    e sel :: Selector
    sel    -> Int -> Expr -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    ppWP 4 Expr
    e Doc -> Doc -> Doc
    <+> String -> Doc
    text "." Doc -> Doc -> Doc
    <.> Selector -> Doc
    forall a. PP a => a -> Doc
    pp Selector
    sel

          ESet e :: Expr
    e sel :: Selector
    sel v :: Expr
    v  -> Doc -> Doc
    braces (Expr -> Doc
    forall a. PP a => a -> Doc
    pp Expr
    e Doc -> Doc -> Doc
    <+> "|" Doc -> Doc -> Doc
    <+> Selector -> Doc
    forall a. PP a => a -> Doc
    pp Selector
    sel Doc -> Doc -> Doc
    <+> "=" Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall a. PP a => a -> Doc
    pp Expr
    v)

          EIf e1 :: Expr
    e1 e2 :: Expr
    e2 e3 :: Expr
    e3  -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 0)
                        (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    sep [ String -> Doc
    text "if"   Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall a. PP (WithNames a) => a -> Doc
    ppW Expr
    e1
                              , String -> Doc
    text "then" Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall a. PP (WithNames a) => a -> Doc
    ppW Expr
    e2
                              , String -> Doc
    text "else" Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall a. PP (WithNames a) => a -> Doc
    ppW Expr
    e3 ]

          EComp _ _ e :: Expr
    e mss :: [[Match]]
    mss -> let arm :: [a] -> Doc
    arm ms :: [a]
    ms = String -> Doc
    text "|" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    commaSep ((a -> Doc) -> [a] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Doc
    forall a. PP (WithNames a) => a -> Doc
    ppW [a]
    ms)
                              in Doc -> Doc
    brackets (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Expr -> Doc
    forall a. PP (WithNames a) => a -> Doc
    ppW Expr
    e Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    vcat (([Match] -> Doc) -> [[Match]] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map [Match] -> Doc
    forall a. PP (WithNames a) => [a] -> Doc
    arm [[Match]]
    mss)

          EVar x :: Name
    x        -> Name -> Doc
    forall a. PPName a => a -> Doc
    ppPrefixName Name
    x

          EAbs {}       -> let (xs :: [(Name, Prop)]
    xs,e :: Expr
    e) = (Expr -> Maybe ((Name, Prop), Expr))
    -> Expr -> ([(Name, Prop)], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe ((Name, Prop), Expr)
    splitAbs Expr
    expr
                           in NameMap
    -> Int -> [TParam] -> [Prop] -> [(Name, Prop)] -> Expr -> Doc
    ppLam NameMap
    nm Int
    prec [] [] [(Name, Prop)]
    xs Expr
    e

          EProofAbs {}  -> let (ps :: [Prop]
    ps,e1 :: Expr
    e1) = (Expr -> Maybe (Prop, Expr)) -> Expr -> ([Prop], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe (Prop, Expr)
    splitProofAbs Expr
    expr
                               (xs :: [(Name, Prop)]
    xs,e2 :: Expr
    e2) = (Expr -> Maybe ((Name, Prop), Expr))
    -> Expr -> ([(Name, Prop)], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe ((Name, Prop), Expr)
    splitAbs Expr
    e1
                           in NameMap
    -> Int -> [TParam] -> [Prop] -> [(Name, Prop)] -> Expr -> Doc
    ppLam NameMap
    nm Int
    prec [] [Prop]
    ps [(Name, Prop)]
    xs Expr
    e2

          ETAbs {}      -> let (ts :: [TParam]
    ts,e1 :: Expr
    e1) = (Expr -> Maybe (TParam, Expr)) -> Expr -> ([TParam], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe (TParam, Expr)
    splitTAbs     Expr
    expr
                               (ps :: [Prop]
    ps,e2 :: Expr
    e2) = (Expr -> Maybe (Prop, Expr)) -> Expr -> ([Prop], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe (Prop, Expr)
    splitProofAbs Expr
    e1
                               (xs :: [(Name, Prop)]
    xs,e3 :: Expr
    e3) = (Expr -> Maybe ((Name, Prop), Expr))
    -> Expr -> ([(Name, Prop)], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe ((Name, Prop), Expr)
    splitAbs      Expr
    e2
                           in NameMap
    -> Int -> [TParam] -> [Prop] -> [(Name, Prop)] -> Expr -> Doc
    ppLam NameMap
    nm Int
    prec [TParam]
    ts [Prop]
    ps [(Name, Prop)]
    xs Expr
    e3

          -- infix applications
          EApp (EApp (EVar o :: Name
    o) a :: Expr
    a) b :: Expr
    b
            | Ident -> Bool
    isInfixIdent (Name -> Ident
    nameIdent Name
    o) ->
              Int -> Expr -> Doc
    forall a. PP a => Int -> a -> Doc
    ppPrec 3 Expr
    a Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PPName a => a -> Doc
    ppInfixName Name
    o Doc -> Doc -> Doc
    <+> Int -> Expr -> Doc
    forall a. PP a => Int -> a -> Doc
    ppPrec 3 Expr
    b

            | Bool
    otherwise ->
              Name -> Doc
    forall a. PPName a => a -> Doc
    ppPrefixName Name
    o Doc -> Doc -> Doc
    <+> Int -> Expr -> Doc
    forall a. PP a => Int -> a -> Doc
    ppPrec 3 Expr
    a Doc -> Doc -> Doc
    <+> Int -> Expr -> Doc
    forall a. PP a => Int -> a -> Doc
    ppPrec 3 Expr
    b

          EApp e1 :: Expr
    e1 e2 :: Expr
    e2    -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 3)
                        (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $  Int -> Expr -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    ppWP 3 Expr
    e1 Doc -> Doc -> Doc
    <+> Int -> Expr -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    ppWP 4 Expr
    e2

          EProofApp e :: Expr
    e   -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 3)
                        (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> Expr -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    ppWP 3 Expr
    e Doc -> Doc -> Doc
    <+> String -> Doc
    text "<>"

          ETApp e :: Expr
    e t :: Prop
    t     -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 3)
                        (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> Expr -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    ppWP 3 Expr
    e Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    ppWP 4 Prop
    t

          EWhere e :: Expr
    e ds :: [DeclGroup]
    ds   -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 0)
                         ( Expr -> Doc
    forall a. PP (WithNames a) => a -> Doc
    ppW Expr
    e Doc -> Doc -> Doc
    $$ String -> Doc
    text "where"
                                         Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest 2 ([Doc] -> Doc
    vcat ((DeclGroup -> Doc) -> [DeclGroup] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map DeclGroup -> Doc
    forall a. PP (WithNames a) => a -> Doc
    ppW [DeclGroup]
    ds))
                                         Doc -> Doc -> Doc
    $$ String -> Doc
    text "" )

        where
        ppW :: a -> Doc
    ppW x :: a
    x   = NameMap -> a -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm a
    x
        ppWP :: Int -> a -> Doc
    ppWP x :: Int
    x  = NameMap -> Int -> a -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    nm Int
    x

    ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name,Type)] -> Expr -> Doc
    ppLam :: NameMap
    -> Int -> [TParam] -> [Prop] -> [(Name, Prop)] -> Expr -> Doc
    ppLam nm :: NameMap
    nm prec :: Int
    prec [] [] [] e :: Expr
    e = NameMap -> Int -> Expr -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    nm Int
    prec Expr
    e
    ppLam nm :: NameMap
    nm prec :: Int
    prec ts :: [TParam]
    ts ps :: [Prop]
    ps xs :: [(Name, Prop)]
    xs e :: Expr
    e =
      Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 0) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
      [Doc] -> Doc
    sep [ String -> Doc
    text "\\" Doc -> Doc -> Doc
    <.> Doc
    tsD Doc -> Doc -> Doc
    <+> Doc
    psD Doc -> Doc -> Doc
    <+> Doc
    xsD Doc -> Doc -> Doc
    <+> String -> Doc
    text "->"
          , NameMap -> Expr -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1 Expr
    e
          ]
      where
      ns1 :: NameMap
    ns1 = [TParam] -> NameMap -> NameMap
    addTNames [TParam]
    ts NameMap
    nm

      tsD :: Doc
    tsD = if [TParam] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [TParam]
    ts then Doc
    empty else Doc -> Doc
    braces (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    sep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (TParam -> Doc) -> [TParam] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> Doc
    ppT [TParam]
    ts
      psD :: Doc
    psD = if [Prop] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Prop]
    ps then Doc
    empty else Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    sep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Prop -> Doc
    ppP [Prop]
    ps
      xsD :: Doc
    xsD = if [(Name, Prop)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Name, Prop)]
    xs then Doc
    empty else [Doc] -> Doc
    sep    ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ ((Name, Prop) -> Doc) -> [(Name, Prop)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, Prop) -> Doc
    forall a a. (PP a, PP (WithNames a)) => (a, a) -> Doc
    ppArg [(Name, Prop)]
    xs

      ppT :: TParam -> Doc
    ppT = NameMap -> TParam -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1
      ppP :: Prop -> Doc
    ppP = NameMap -> Prop -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1
      ppArg :: (a, a) -> Doc
    ppArg (x :: a
    x,t :: a
    t) = Doc -> Doc
    parens (a -> Doc
    forall a. PP a => a -> Doc
    pp a
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text ":" Doc -> Doc -> Doc
    <+> NameMap -> a -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1 a
    t)

    splitWhile :: (a -> Maybe (b,a)) -> a -> ([b],a)
    splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile f :: a -> Maybe (b, a)
    f e :: a
    e = case a -> Maybe (b, a)
    f a
    e of
                       Nothing     -> ([], a
    e)
                       Just (x :: b
    x,e1 :: a
    e1) -> let (xs :: [b]
    xs,e2 :: a
    e2) = (a -> Maybe (b, a)) -> a -> ([b], a)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile a -> Maybe (b, a)
    f a
    e1
                                      in (b
    xb -> [b] -> [b]
    forall a. a -> [a] -> [a]
    :[b]
    xs,a
    e2)

    splitAbs :: Expr -> Maybe ((Name,Type), Expr)
    splitAbs :: Expr -> Maybe ((Name, Prop), Expr)
    splitAbs (EAbs x :: Name
    x t :: Prop
    t e :: Expr
    e)         = ((Name, Prop), Expr) -> Maybe ((Name, Prop), Expr)
    forall a. a -> Maybe a
    Just ((Name
    x,Prop
    t), Expr
    e)
    splitAbs _                    = Maybe ((Name, Prop), Expr)
    forall a. Maybe a
    Nothing

    splitTAbs :: Expr -> Maybe (TParam, Expr)
    splitTAbs :: Expr -> Maybe (TParam, Expr)
    splitTAbs (ETAbs t :: TParam
    t e :: Expr
    e)         = (TParam, Expr) -> Maybe (TParam, Expr)
    forall a. a -> Maybe a
    Just (TParam
    t, Expr
    e)
    splitTAbs _                   = Maybe (TParam, Expr)
    forall a. Maybe a
    Nothing

    splitProofAbs :: Expr -> Maybe (Prop, Expr)
    splitProofAbs :: Expr -> Maybe (Prop, Expr)
    splitProofAbs (EProofAbs p :: Prop
    p e :: Expr
    e) = (Prop, Expr) -> Maybe (Prop, Expr)
    forall a. a -> Maybe a
    Just (Prop
    p,Expr
    e)
    splitProofAbs _               = Maybe (Prop, Expr)
    forall a. Maybe a
    Nothing

    splitTApp :: Expr -> Maybe (Type,Expr)
    splitTApp :: Expr -> Maybe (Prop, Expr)
    splitTApp (ETApp e :: Expr
    e t :: Prop
    t) = (Prop, Expr) -> Maybe (Prop, Expr)
    forall a. a -> Maybe a
    Just (Prop
    t, Expr
    e)
    splitTApp _           = Maybe (Prop, Expr)
    forall a. Maybe a
    Nothing

    splitProofApp :: Expr -> Maybe ((), Expr)
    splitProofApp :: Expr -> Maybe ((), Expr)
    splitProofApp (EProofApp e :: Expr
    e) = ((), Expr) -> Maybe ((), Expr)
    forall a. a -> Maybe a
    Just ((), Expr
    e)
    splitProofApp _ = Maybe ((), Expr)
    forall a. Maybe a
    Nothing

    -- | Deconstruct an expression, typically polymorphic, into
    -- the types and proofs to which it is applied.
    -- Since we don't store the proofs, we just return
    -- the number of proof applications.
    -- The first type is the one closest to the expr.
    splitExprInst :: Expr -> (Expr, [Type], Int)
    splitExprInst :: Expr -> (Expr, [Prop], Int)
    splitExprInst e :: Expr
    e = (Expr
    e2, [Prop] -> [Prop]
    forall a. [a] -> [a]
    reverse [Prop]
    ts, [()] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [()]
    ps)
      where
      (ps :: [()]
    ps,e1 :: Expr
    e1) = (Expr -> Maybe ((), Expr)) -> Expr -> ([()], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe ((), Expr)
    splitProofApp Expr
    e
      (ts :: [Prop]
    ts,e2 :: Expr
    e2) = (Expr -> Maybe (Prop, Expr)) -> Expr -> ([Prop], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe (Prop, Expr)
    splitTApp Expr
    e1

    instance PP Expr where
      ppPrec :: Int -> Expr -> Doc
    ppPrec n :: Int
    n t :: Expr
    t = NameMap -> Int -> Expr -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    forall a. IntMap a
    IntMap.empty Int
    n Expr
    t

    instance PP (WithNames Match) where
      ppPrec :: Int -> WithNames Match -> Doc
    ppPrec _ (WithNames mat :: Match
    mat nm :: NameMap
    nm) =
        case Match
    mat of
          From x :: Name
    x _ _ e :: Expr
    e -> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text "<-" Doc -> Doc -> Doc
    <+> NameMap -> Expr -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm Expr
    e
          Let d :: Decl
    d      -> String -> Doc
    text "let" Doc -> Doc -> Doc
    <+> NameMap -> Decl -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm Decl
    d

    instance PP Match where
      ppPrec :: Int -> Match -> Doc
    ppPrec = NameMap -> Int -> Match -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    forall a. IntMap a
    IntMap.empty

    instance PP (WithNames DeclGroup) where
      ppPrec :: Int -> WithNames DeclGroup -> Doc
    ppPrec _ (WithNames dg :: DeclGroup
    dg nm :: NameMap
    nm) =
        case DeclGroup
    dg of
          Recursive ds :: [Decl]
    ds    -> String -> Doc
    text "/* Recursive */"
                          Doc -> Doc -> Doc
    $$ [Doc] -> Doc
    vcat ((Decl -> Doc) -> [Decl] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (NameMap -> Decl -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm) [Decl]
    ds)
                          Doc -> Doc -> Doc
    $$ String -> Doc
    text ""
          NonRecursive d :: Decl
    d  -> String -> Doc
    text "/* Not recursive */"
                          Doc -> Doc -> Doc
    $$ NameMap -> Decl -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm Decl
    d
                          Doc -> Doc -> Doc
    $$ String -> Doc
    text ""

    instance PP DeclGroup where
      ppPrec :: Int -> DeclGroup -> Doc
    ppPrec = NameMap -> Int -> DeclGroup -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    forall a. IntMap a
    IntMap.empty

    instance PP (WithNames Decl) where
      ppPrec :: Int -> WithNames Decl -> Doc
    ppPrec _ (WithNames Decl { .. } nm :: NameMap
    nm) =
        Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    dName Doc -> Doc -> Doc
    <+> String -> Doc
    text ":" Doc -> Doc -> Doc
    <+> NameMap -> Schema -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm Schema
    dSignature  Doc -> Doc -> Doc
    $$
        (if [Pragma] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Pragma]
    dPragmas
            then Doc
    empty
            else String -> Doc
    text "pragmas" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    dName Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    sep ((Pragma -> Doc) -> [Pragma] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Pragma -> Doc
    forall a. PP a => a -> Doc
    pp [Pragma]
    dPragmas)
        ) Doc -> Doc -> Doc
    $$
        Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    dName Doc -> Doc -> Doc
    <+> String -> Doc
    text "=" Doc -> Doc -> Doc
    <+> NameMap -> DeclDef -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm DeclDef
    dDefinition

    instance PP (WithNames DeclDef) where
      ppPrec :: Int -> WithNames DeclDef -> Doc
    ppPrec _ (WithNames DPrim _)      = String -> Doc
    text "<primitive>"
      ppPrec _ (WithNames (DExpr e :: Expr
    e) nm :: NameMap
    nm) = NameMap -> Expr -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm Expr
    e

    instance PP Decl where
      ppPrec :: Int -> Decl -> Doc
    ppPrec = NameMap -> Int -> Decl -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    forall a. IntMap a
    IntMap.empty

    instance PP Module where
      ppPrec :: Int -> Module -> Doc
    ppPrec = NameMap -> Int -> Module -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    forall a. IntMap a
    IntMap.empty

    instance PP (WithNames Module) where
      ppPrec :: Int -> WithNames Module -> Doc
    ppPrec _ (WithNames Module { .. } nm :: NameMap
    nm) =
        String -> Doc
    text "module" Doc -> Doc -> Doc
    <+> ModName -> Doc
    forall a. PP a => a -> Doc
    pp ModName
    mName Doc -> Doc -> Doc
    $$
        -- XXX: Print exports?
        [Doc] -> Doc
    vcat ((Import -> Doc) -> [Import] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Import -> Doc
    forall a. PP a => a -> Doc
    pp [Import]
    mImports) Doc -> Doc -> Doc
    $$
        -- XXX: Print tysyns
        -- XXX: Print abstarct types/functions
        [Doc] -> Doc
    vcat ((DeclGroup -> Doc) -> [DeclGroup] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (NameMap -> DeclGroup -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames ([TParam] -> NameMap -> NameMap
    addTNames [TParam]
    mps NameMap
    nm)) [DeclGroup]
    mDecls)
        where mps :: [TParam]
    mps = (ModTParam -> TParam) -> [ModTParam] -> [TParam]
    forall a b. (a -> b) -> [a] -> [b]
    map ModTParam -> TParam
    mtpParam (Map Name ModTParam -> [ModTParam]
    forall k a. Map k a -> [a]
    Map.elems Map Name ModTParam
    mParamTypes)