    -- |
    -- 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                   #-}
    {-# LANGUAGE NamedFieldPuns                      #-}
    {-# LANGUAGE ViewPatterns                        #-}
    module Cryptol.TypeCheck.AST
      ( module Cryptol.TypeCheck.AST
      , Name()
      , TFun(..)
      , Selector(..)
      , Import, ImportG(..), ImpName(..)
      , ImportSpec(..)
      , ExportType(..)
      , ExportSpec(..), isExportedBind, isExportedType, isExported
      , Pragma(..)
      , Fixity(..)
      , PrimMap(..)
      , module Cryptol.TypeCheck.Type
      ) where

    import Data.Maybe(mapMaybe)

    import Cryptol.Utils.Panic(panic)
    import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim)
    import Cryptol.Parser.Position(Located,Range,HasLoc(..))
    import Cryptol.ModuleSystem.Name
    import Cryptol.ModuleSystem.Interface
    import Cryptol.ModuleSystem.Exports(ExportSpec(..)
                                       , isExportedBind, isExportedType, isExported)
    import Cryptol.Parser.AST ( Selector(..),Pragma(..)
                              , Import
                              , ImportG(..), ImportSpec(..), ExportType(..)
                              , Fixity(..)
                              , ImpName(..)
                              )
    import Cryptol.Utils.RecordMap
    import Cryptol.TypeCheck.FFI.FFIType
    import Cryptol.TypeCheck.PP
    import Cryptol.TypeCheck.Type

    import GHC.Generics (Generic)
    import Control.DeepSeq

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

    data TCTopEntity =
        TCTopModule (ModuleG ModName)
      | TCTopSignature ModName ModParamNames
        deriving (Int -> TCTopEntity -> ShowS
    [TCTopEntity] -> ShowS
    TCTopEntity -> String
    (Int -> TCTopEntity -> ShowS)
    -> (TCTopEntity -> String)
    -> ([TCTopEntity] -> ShowS)
    -> Show TCTopEntity
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> TCTopEntity -> ShowS
    showsPrec :: Int -> TCTopEntity -> ShowS
    $cshow :: TCTopEntity -> String
    show :: TCTopEntity -> String
    $cshowList :: [TCTopEntity] -> ShowS
    showList :: [TCTopEntity] -> ShowS
    Show, (forall x. TCTopEntity -> Rep TCTopEntity x)
    -> (forall x. Rep TCTopEntity x -> TCTopEntity)
    -> Generic TCTopEntity
    forall x. Rep TCTopEntity x -> TCTopEntity
    forall x. TCTopEntity -> Rep TCTopEntity x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. TCTopEntity -> Rep TCTopEntity x
    from :: forall x. TCTopEntity -> Rep TCTopEntity x
    $cto :: forall x. Rep TCTopEntity x -> TCTopEntity
    to :: forall x. Rep TCTopEntity x -> TCTopEntity
    Generic, TCTopEntity -> ()
    (TCTopEntity -> ()) -> NFData TCTopEntity
    forall a. (a -> ()) -> NFData a
    $crnf :: TCTopEntity -> ()
    rnf :: TCTopEntity -> ()
    NFData)

    tcTopEntitytName :: TCTopEntity -> ModName
    tcTopEntitytName :: TCTopEntity -> ModName
    tcTopEntitytName TCTopEntity
    ent =
      case TCTopEntity
    ent of
        TCTopModule ModuleG ModName
    m -> ModuleG ModName -> ModName
    forall mname. ModuleG mname -> mname
    mName ModuleG ModName
    m
        TCTopSignature ModName
    m ModParamNames
    _ -> ModName
    m

    -- | Panics if the entity is not a module
    tcTopEntityToModule :: TCTopEntity -> Module
    tcTopEntityToModule :: TCTopEntity -> ModuleG ModName
    tcTopEntityToModule TCTopEntity
    ent =
      case TCTopEntity
    ent of
        TCTopModule ModuleG ModName
    m -> ModuleG ModName
    m
        TCTopSignature {} -> String -> [String] -> ModuleG ModName
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "tcTopEntityToModule" [ String
    "Not a module" ]

    -- | A Cryptol module.
    data ModuleG mname =
                  Module { forall mname. ModuleG mname -> mname
    mName             :: !mname
                         , forall mname. ModuleG mname -> Maybe Text
    mDoc              :: !(Maybe Text)
                         , forall mname. ModuleG mname -> ExportSpec Name
    mExports          :: ExportSpec Name

                         -- Functors:
                         , forall mname. ModuleG mname -> Map Name ModTParam
    mParamTypes       :: Map Name ModTParam
                         , forall mname. ModuleG mname -> Map Name ModVParam
    mParamFuns        :: Map Name ModVParam
                         , forall mname. ModuleG mname -> [Located Prop]
    mParamConstraints :: [Located Prop]

                         , forall mname. ModuleG mname -> FunctorParams
    mParams           :: FunctorParams
                           -- ^ Parameters grouped by "import".

                         , forall mname. ModuleG mname -> Map Name (ModuleG Name)
    mFunctors         :: Map Name (ModuleG Name)
                           -- ^ Functors directly nested in this module.
                           -- Things further nested are in the modules in the
                           -- elements of the map.

                         , forall mname. ModuleG mname -> Set Name
    mNested           :: !(Set Name)
                           -- ^ Submodules, functors, and interfaces nested directly
                           -- in this module

                          -- These have everything from this module and all submodules
                         , forall mname. ModuleG mname -> Map Name TySyn
    mTySyns           :: Map Name TySyn
                         , forall mname. ModuleG mname -> Map Name Newtype
    mNewtypes         :: Map Name Newtype
                         , forall mname. ModuleG mname -> Map Name AbstractType
    mPrimTypes        :: Map Name AbstractType
                         , forall mname. ModuleG mname -> [DeclGroup]
    mDecls            :: [DeclGroup]
                         , forall mname. ModuleG mname -> Map Name (IfaceNames Name)
    mSubmodules       :: Map Name (IfaceNames Name)
                         , forall mname. ModuleG mname -> Map Name ModParamNames
    mSignatures       :: !(Map Name ModParamNames)
                         } deriving (Int -> ModuleG mname -> ShowS
    [ModuleG mname] -> ShowS
    ModuleG mname -> String
    (Int -> ModuleG mname -> ShowS)
    -> (ModuleG mname -> String)
    -> ([ModuleG mname] -> ShowS)
    -> Show (ModuleG mname)
    forall mname. Show mname => Int -> ModuleG mname -> ShowS
    forall mname. Show mname => [ModuleG mname] -> ShowS
    forall mname. Show mname => ModuleG mname -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall mname. Show mname => Int -> ModuleG mname -> ShowS
    showsPrec :: Int -> ModuleG mname -> ShowS
    $cshow :: forall mname. Show mname => ModuleG mname -> String
    show :: ModuleG mname -> String
    $cshowList :: forall mname. Show mname => [ModuleG mname] -> ShowS
    showList :: [ModuleG mname] -> ShowS
    Show, (forall x. ModuleG mname -> Rep (ModuleG mname) x)
    -> (forall x. Rep (ModuleG mname) x -> ModuleG mname)
    -> Generic (ModuleG mname)
    forall x. Rep (ModuleG mname) x -> ModuleG mname
    forall x. ModuleG mname -> Rep (ModuleG mname) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall mname x. Rep (ModuleG mname) x -> ModuleG mname
    forall mname x. ModuleG mname -> Rep (ModuleG mname) x
    $cfrom :: forall mname x. ModuleG mname -> Rep (ModuleG mname) x
    from :: forall x. ModuleG mname -> Rep (ModuleG mname) x
    $cto :: forall mname x. Rep (ModuleG mname) x -> ModuleG mname
    to :: forall x. Rep (ModuleG mname) x -> ModuleG mname
    Generic, ModuleG mname -> ()
    (ModuleG mname -> ()) -> NFData (ModuleG mname)
    forall mname. NFData mname => ModuleG mname -> ()
    forall a. (a -> ()) -> NFData a
    $crnf :: forall mname. NFData mname => ModuleG mname -> ()
    rnf :: ModuleG mname -> ()
    NFData)

    emptyModule :: mname -> ModuleG mname
    emptyModule :: forall mname. mname -> ModuleG mname
    emptyModule mname
    nm =
      Module
        { mName :: mname
    mName             = mname
    nm
        , mDoc :: Maybe Text
    mDoc              = Maybe Text
    forall a. Maybe a
    Nothing
        , mExports :: ExportSpec Name
    mExports          = ExportSpec Name
    forall a. Monoid a => a
    mempty

        , mParams :: FunctorParams
    mParams           = FunctorParams
    forall a. Monoid a => a
    mempty
        , mParamTypes :: Map Name ModTParam
    mParamTypes       = Map Name ModTParam
    forall a. Monoid a => a
    mempty
        , mParamConstraints :: [Located Prop]
    mParamConstraints = [Located Prop]
    forall a. Monoid a => a
    mempty
        , mParamFuns :: Map Name ModVParam
    mParamFuns        = Map Name ModVParam
    forall a. Monoid a => a
    mempty

        , mNested :: Set Name
    mNested           = Set Name
    forall a. Monoid a => a
    mempty

        , mTySyns :: Map Name TySyn
    mTySyns           = Map Name TySyn
    forall a. Monoid a => a
    mempty
        , mNewtypes :: Map Name Newtype
    mNewtypes         = Map Name Newtype
    forall a. Monoid a => a
    mempty
        , mPrimTypes :: Map Name AbstractType
    mPrimTypes        = Map Name AbstractType
    forall a. Monoid a => a
    mempty
        , mDecls :: [DeclGroup]
    mDecls            = [DeclGroup]
    forall a. Monoid a => a
    mempty
        , mFunctors :: Map Name (ModuleG Name)
    mFunctors         = Map Name (ModuleG Name)
    forall a. Monoid a => a
    mempty
        , mSubmodules :: Map Name (IfaceNames Name)
    mSubmodules       = Map Name (IfaceNames Name)
    forall a. Monoid a => a
    mempty
        , mSignatures :: Map Name ModParamNames
    mSignatures       = Map Name ModParamNames
    forall a. Monoid a => a
    mempty
        }

    -- | Find all the foreign declarations in the module and return their names and FFIFunTypes.
    findForeignDecls :: ModuleG mname -> [(Name, FFIFunType)]
    findForeignDecls :: forall mname. ModuleG mname -> [(Name, FFIFunType)]
    findForeignDecls = (DeclGroup -> Maybe (Name, FFIFunType))
    -> [DeclGroup] -> [(Name, FFIFunType)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe DeclGroup -> Maybe (Name, FFIFunType)
    getForeign ([DeclGroup] -> [(Name, FFIFunType)])
    -> (ModuleG mname -> [DeclGroup])
    -> ModuleG mname
    -> [(Name, FFIFunType)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleG mname -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls
      where getForeign :: DeclGroup -> Maybe (Name, FFIFunType)
    getForeign (NonRecursive Decl { Name
    dName :: Name
    dName :: Decl -> Name
    dName, dDefinition :: Decl -> DeclDef
    dDefinition = DForeign FFIFunType
    ffiType })
              = (Name, FFIFunType) -> Maybe (Name, FFIFunType)
    forall a. a -> Maybe a
    Just (Name
    dName, FFIFunType
    ffiType)
            -- Recursive DeclGroups can't have foreign decls
            getForeign DeclGroup
    _ = Maybe (Name, FFIFunType)
    forall a. Maybe a
    Nothing

    -- | Find all the foreign declarations that are in functors.
    -- This is used to report an error
    findForeignDeclsInFunctors :: ModuleG mname -> [Name]
    findForeignDeclsInFunctors :: forall mname. ModuleG mname -> [Name]
    findForeignDeclsInFunctors = (ModuleG Name -> [Name]) -> [ModuleG Name] -> [Name]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ModuleG Name -> [Name]
    forall mname. ModuleG mname -> [Name]
    fromM ([ModuleG Name] -> [Name])
    -> (ModuleG mname -> [ModuleG Name]) -> ModuleG mname -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Name (ModuleG Name) -> [ModuleG Name]
    forall k a. Map k a -> [a]
    Map.elems (Map Name (ModuleG Name) -> [ModuleG Name])
    -> (ModuleG mname -> Map Name (ModuleG Name))
    -> ModuleG mname
    -> [ModuleG Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleG mname -> Map Name (ModuleG Name)
    forall mname. ModuleG mname -> Map Name (ModuleG Name)
    mFunctors
      where
      fromM :: ModuleG mname -> [Name]
    fromM ModuleG mname
    m = ((Name, FFIFunType) -> Name) -> [(Name, FFIFunType)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, FFIFunType) -> Name
    forall a b. (a, b) -> a
    fst (ModuleG mname -> [(Name, FFIFunType)]
    forall mname. ModuleG mname -> [(Name, FFIFunType)]
    findForeignDecls ModuleG mname
    m) [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    ++ ModuleG mname -> [Name]
    forall mname. ModuleG mname -> [Name]
    findForeignDeclsInFunctors ModuleG mname
    m

    type Module = ModuleG ModName

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

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

                | 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

                | ELocated Range Expr       -- ^ Source location information

                {- | 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]

                | EPropGuards [([Prop], Expr)] Type

                  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
    $cshowsPrec :: Int -> Expr -> ShowS
    showsPrec :: Int -> Expr -> ShowS
    $cshow :: Expr -> String
    show :: Expr -> String
    $cshowList :: [Expr] -> ShowS
    showList :: [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
    $cfrom :: forall x. Expr -> Rep Expr x
    from :: forall x. Expr -> Rep Expr x
    $cto :: forall x. Rep Expr x -> Expr
    to :: forall x. Rep Expr x -> Expr
    Generic, Expr -> ()
    (Expr -> ()) -> NFData Expr
    forall a. (a -> ()) -> NFData a
    $crnf :: Expr -> ()
    rnf :: 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
    $cshowsPrec :: Int -> Match -> ShowS
    showsPrec :: Int -> Match -> ShowS
    $cshow :: Match -> String
    show :: Match -> String
    $cshowList :: [Match] -> ShowS
    showList :: [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
    $cfrom :: forall x. Match -> Rep Match x
    from :: forall x. Match -> Rep Match x
    $cto :: forall x. Rep Match x -> Match
    to :: forall x. Rep Match x -> Match
    Generic, Match -> ()
    (Match -> ()) -> NFData Match
    forall a. (a -> ()) -> NFData a
    $crnf :: Match -> ()
    rnf :: 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
    $cshowsPrec :: Int -> DeclGroup -> ShowS
    showsPrec :: Int -> DeclGroup -> ShowS
    $cshow :: DeclGroup -> String
    show :: DeclGroup -> String
    $cshowList :: [DeclGroup] -> ShowS
    showList :: [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
    $cfrom :: forall x. DeclGroup -> Rep DeclGroup x
    from :: forall x. DeclGroup -> Rep DeclGroup x
    $cto :: forall x. Rep DeclGroup x -> DeclGroup
    to :: forall x. Rep DeclGroup x -> DeclGroup
    Generic, DeclGroup -> ()
    (DeclGroup -> ()) -> NFData DeclGroup
    forall a. (a -> ()) -> NFData a
    $crnf :: DeclGroup -> ()
    rnf :: DeclGroup -> ()
    NFData)

    groupDecls :: DeclGroup -> [Decl]
    groupDecls :: DeclGroup -> [Decl]
    groupDecls DeclGroup
    dg = case DeclGroup
    dg of
      Recursive [Decl]
    ds   -> [Decl]
    ds
      NonRecursive 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 Text
    dDoc         :: Maybe Text
                           } 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
    $cfrom :: forall x. Decl -> Rep Decl x
    from :: forall x. Decl -> Rep Decl x
    $cto :: forall x. Rep Decl x -> Decl
    to :: forall x. Rep Decl x -> Decl
    Generic, Decl -> ()
    (Decl -> ()) -> NFData Decl
    forall a. (a -> ()) -> NFData a
    $crnf :: Decl -> ()
    rnf :: 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
    $cshowsPrec :: Int -> Decl -> ShowS
    showsPrec :: Int -> Decl -> ShowS
    $cshow :: Decl -> String
    show :: Decl -> String
    $cshowList :: [Decl] -> ShowS
    showList :: [Decl] -> ShowS
    Show)

    data DeclDef    = DPrim
                    | DForeign FFIFunType
                    | 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
    $cshowsPrec :: Int -> DeclDef -> ShowS
    showsPrec :: Int -> DeclDef -> ShowS
    $cshow :: DeclDef -> String
    show :: DeclDef -> String
    $cshowList :: [DeclDef] -> ShowS
    showList :: [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
    $cfrom :: forall x. DeclDef -> Rep DeclDef x
    from :: forall x. DeclDef -> Rep DeclDef x
    $cto :: forall x. Rep DeclDef x -> DeclDef
    to :: forall x. Rep DeclDef x -> DeclDef
    Generic, DeclDef -> ()
    (DeclDef -> ()) -> NFData DeclDef
    forall a. (a -> ()) -> NFData a
    $crnf :: DeclDef -> ()
    rnf :: DeclDef -> ()
    NFData)

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

    -- | Construct a primitive, given a map to the unique primitive name.
    ePrim :: PrimMap -> PrimIdent -> Expr
    ePrim :: PrimMap -> PrimIdent -> Expr
    ePrim PrimMap
    pm PrimIdent
    n = Name -> Expr
    EVar (PrimIdent -> PrimMap -> Name
    lookupPrimDecl PrimIdent
    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 PrimMap
    prims Prop
    t String
    str =
      Expr -> Expr -> Expr
    EApp (Expr -> Prop -> Expr
    ETApp (Expr -> Prop -> Expr
    ETApp (PrimMap -> PrimIdent -> Expr
    ePrim PrimMap
    prims (Text -> PrimIdent
    prelPrim Text
    "error")) Prop
    t)
                  (Int -> Prop
    forall a. Integral a => a -> Prop
    tNum (String -> Int
    forall a. [a] -> 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 PrimMap
    prims 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 PrimMap
    prims Char
    c = Expr -> Prop -> Expr
    ETApp (Expr -> Prop -> Expr
    ETApp (PrimMap -> PrimIdent -> Expr
    ePrim PrimMap
    prims (Text -> PrimIdent
    prelPrim Text
    "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 = Int
    8 :: Int

    instance PP TCTopEntity where
      ppPrec :: Int -> TCTopEntity -> Doc
    ppPrec Int
    _ TCTopEntity
    te =
        case TCTopEntity
    te of
          TCTopModule ModuleG ModName
    m -> ModuleG ModName -> Doc
    forall a. PP a => a -> Doc
    pp ModuleG ModName
    m
          TCTopSignature ModName
    x ModParamNames
    p ->
            (Doc
    "interface" Doc -> Doc -> Doc
    <+> ModName -> Doc
    forall a. PP a => a -> Doc
    pp ModName
    x Doc -> Doc -> Doc
    <+> Doc
    "where") Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest Int
    2 (ModParamNames -> Doc
    forall a. PP a => a -> Doc
    pp ModParamNames
    p)

    instance PP (WithNames Expr) where
      ppPrec :: Int -> WithNames Expr -> Doc
    ppPrec Int
    prec (WithNames Expr
    expr NameMap
    nm) =
        case Expr
    expr of
          ELocated Range
    _ Expr
    t  -> Int -> Expr -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    ppWP Int
    prec Expr
    t

          EList [] Prop
    t    -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0)
                        (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    text String
    "[]" 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 [Expr]
    es Prop
    _    -> [Doc] -> Doc
    ppList ([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 [Expr]
    es     -> [Doc] -> Doc
    ppTuple ([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 RecordMap Ident Expr
    fs       -> [Doc] -> Doc
    ppRecord
                            [ Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    f Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "=" Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall {a}. PP (WithNames a) => a -> Doc
    ppW Expr
    e | (Ident
    f,Expr
    e) <- RecordMap Ident Expr -> [(Ident, Expr)]
    forall a b. (Show a, Ord a) => RecordMap a b -> [(a, b)]
    displayFields RecordMap Ident Expr
    fs ]

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

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

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

          EComp Prop
    _ Prop
    _ Expr
    e [[Match]]
    mss -> let arm :: [a] -> Doc
    arm [a]
    ms = String -> Doc
    text String
    "|" 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
    align ([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 Name
    x        -> Name -> Doc
    forall a. PPName a => a -> Doc
    ppPrefixName Name
    x

          EAbs {}       -> let ([(Name, Prop)]
    xs,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 ([Prop]
    ps,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
                               ([(Name, Prop)]
    xs,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 ([TParam]
    ts,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
                               ([Prop]
    ps,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
                               ([(Name, Prop)]
    xs,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 Name
    o) Expr
    a) Expr
    b
            | Ident -> Bool
    isInfixIdent (Name -> Ident
    nameIdent Name
    o) ->
              Int -> Expr -> Doc
    forall a. PP a => Int -> a -> Doc
    ppPrec Int
    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 Int
    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 Int
    3 Expr
    a Doc -> Doc -> Doc
    <+> Int -> Expr -> Doc
    forall a. PP a => Int -> a -> Doc
    ppPrec Int
    3 Expr
    b

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

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

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

          EWhere Expr
    e [DeclGroup]
    ds   -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> Doc
    align (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    vsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
                             [ Expr -> Doc
    forall {a}. PP (WithNames a) => a -> Doc
    ppW Expr
    e
                             , Doc -> Int -> Doc -> Doc
    hang Doc
    "where" Int
    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))
                             ]

          EPropGuards [([Prop], Expr)]
    guards Prop
    _ ->
            Doc -> Doc
    parens (String -> Doc
    text String
    "propguards" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    vsep (([Prop], Expr) -> Doc
    forall {a} {a}.
    (PP (WithNames a), PP (WithNames a)) =>
    ([a], a) -> Doc
    ppGuard (([Prop], Expr) -> Doc) -> [([Prop], Expr)] -> [Doc]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [([Prop], Expr)]
    guards))
            where ppGuard :: ([a], a) -> Doc
    ppGuard ([a]
    props, a
    e) = Int -> Doc -> Doc
    indent Int
    1
                                     (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    pipe Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    commaSep (a -> Doc
    forall {a}. PP (WithNames a) => a -> Doc
    ppW (a -> Doc) -> [a] -> [Doc]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [a]
    props)
                                   Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "=>" Doc -> Doc -> Doc
    <+> a -> Doc
    forall {a}. PP (WithNames a) => a -> Doc
    ppW a
    e

        where
        ppW :: a -> Doc
    ppW a
    x   = NameMap -> a -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm a
    x
        ppWP :: Int -> a -> Doc
    ppWP 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 NameMap
    nm Int
    prec [] [] [] Expr
    e = Int -> Doc -> Doc
    nest Int
    2 (NameMap -> Int -> Expr -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    nm Int
    prec Expr
    e)
    ppLam NameMap
    nm Int
    prec [TParam]
    ts [Prop]
    ps [(Name, Prop)]
    xs Expr
    e =
      Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
      Int -> Doc -> Doc
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    sep
        [ String -> Doc
    text String
    "\\" Doc -> Doc -> Doc
    <.> [Doc] -> Doc
    hsep ([Doc]
    tsD [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc]
    psD [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc]
    xsD [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [String -> Doc
    text String
    "->"])
        , 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 a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [TParam]
    ts then [] else [Doc -> Doc
    braces (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    commaSep ([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 a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Prop]
    ps then [] else [Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    commaSep ([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 a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Name, Prop)]
    xs then [] 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 (a
    x,a
    t) = Doc -> Doc
    parens (a -> Doc
    forall a. PP a => a -> Doc
    pp a
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    ":" 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 :: forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile a -> Maybe (b, a)
    f a
    e = case a -> Maybe (b, a)
    f a
    e of
                       Maybe (b, a)
    Nothing     -> ([], a
    e)
                       Just (b
    x,a
    e1) -> let ([b]
    xs,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)

    splitLoc :: Expr -> Maybe (Range, Expr)
    splitLoc :: Expr -> Maybe (Range, Expr)
    splitLoc Expr
    expr =
      case Expr
    expr of
        ELocated Range
    r Expr
    e -> (Range, Expr) -> Maybe (Range, Expr)
    forall a. a -> Maybe a
    Just (Range
    r,Expr
    e)
        Expr
    _            -> Maybe (Range, Expr)
    forall a. Maybe a
    Nothing

    -- | Remove outermost locations
    dropLocs :: Expr -> Expr
    dropLocs :: Expr -> Expr
    dropLocs = ([Range], Expr) -> Expr
    forall a b. (a, b) -> b
    snd (([Range], Expr) -> Expr)
    -> (Expr -> ([Range], Expr)) -> Expr -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> Maybe (Range, Expr)) -> Expr -> ([Range], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe (Range, Expr)
    splitLoc

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

    splitApp :: Expr -> Maybe (Expr,Expr)
    splitApp :: Expr -> Maybe (Expr, Expr)
    splitApp (Expr -> Expr
    dropLocs -> EApp Expr
    f Expr
    a) = (Expr, Expr) -> Maybe (Expr, Expr)
    forall a. a -> Maybe a
    Just (Expr
    a, Expr
    f)
    splitApp Expr
    _                      = Maybe (Expr, Expr)
    forall a. Maybe a
    Nothing

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

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

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

    splitProofApp :: Expr -> Maybe ((), Expr)
    splitProofApp :: Expr -> Maybe ((), Expr)
    splitProofApp (Expr -> Expr
    dropLocs -> EProofApp Expr
    e) = ((), Expr) -> Maybe ((), Expr)
    forall a. a -> Maybe a
    Just ((), Expr
    e)
    splitProofApp Expr
    _ = 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 Expr
    e = (Expr
    e2, [Prop] -> [Prop]
    forall a. [a] -> [a]
    reverse [Prop]
    ts, [()] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [()]
    ps)
      where
      ([()]
    ps,Expr
    e1) = (Expr -> Maybe ((), Expr)) -> Expr -> ([()], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe ((), Expr)
    splitProofApp Expr
    e
      ([Prop]
    ts,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 HasLoc Expr where
      getLoc :: Expr -> Maybe Range
    getLoc (ELocated Range
    r Expr
    _) = Range -> Maybe Range
    forall a. a -> Maybe a
    Just Range
    r
      getLoc Expr
    _ = Maybe Range
    forall a. Maybe a
    Nothing

    instance PP Expr where
      ppPrec :: Int -> Expr -> Doc
    ppPrec Int
    n 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 Int
    _ (WithNames Match
    mat NameMap
    nm) =
        case Match
    mat of
          From Name
    x Prop
    _ Prop
    _ Expr
    e -> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "<-" Doc -> Doc -> Doc
    <+> NameMap -> Expr -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm Expr
    e
          Let Decl
    d      -> String -> Doc
    text String
    "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 Int
    _ (WithNames DeclGroup
    dg NameMap
    nm) =
        case DeclGroup
    dg of
          Recursive [Decl]
    ds    -> String -> Doc
    text String
    "/* 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 String
    ""
          NonRecursive Decl
    d  -> String -> Doc
    text String
    "/* 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 String
    ""

    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 Int
    _ (WithNames Decl { Bool
    [Pragma]
    Maybe Text
    Maybe Fixity
    Name
    Schema
    DeclDef
    dName :: Decl -> Name
    dDefinition :: Decl -> DeclDef
    dSignature :: Decl -> Schema
    dPragmas :: Decl -> [Pragma]
    dInfix :: Decl -> Bool
    dFixity :: Decl -> Maybe Fixity
    dDoc :: Decl -> Maybe Text
    dName :: Name
    dSignature :: Schema
    dDefinition :: DeclDef
    dPragmas :: [Pragma]
    dInfix :: Bool
    dFixity :: Maybe Fixity
    dDoc :: Maybe Text
    .. } NameMap
    nm) =
        [Doc] -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          [ Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    dName Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    ":" Doc -> Doc -> Doc
    <+> NameMap -> Schema -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm Schema
    dSignature ]
          [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ (if [Pragma] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Pragma]
    dPragmas
                then []
                else [String -> Doc
    text String
    "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]
    forall a. [a] -> [a] -> [a]
    ++ [ Int -> Doc -> Doc
    nest Int
    2 ([Doc] -> Doc
    sep [Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    dName Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "=", 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 Int
    _ (WithNames DeclDef
    DPrim NameMap
    _)        = String -> Doc
    text String
    "<primitive>"
      ppPrec Int
    _ (WithNames (DForeign FFIFunType
    _) NameMap
    _) = String -> Doc
    text String
    "<foreign>"
      ppPrec Int
    _ (WithNames (DExpr Expr
    e) 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 n => PP (ModuleG n) where
      ppPrec :: Int -> ModuleG n -> Doc
    ppPrec = NameMap -> Int -> ModuleG n -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    forall a. IntMap a
    IntMap.empty

    instance PP n => PP (WithNames (ModuleG n)) where
      ppPrec :: Int -> WithNames (ModuleG n) -> Doc
    ppPrec Int
    _ (WithNames Module { n
    [Located Prop]
    [DeclGroup]
    Maybe Text
    Set Name
    FunctorParams
    Map Name AbstractType
    Map Name Newtype
    Map Name TySyn
    Map Name ModVParam
    Map Name ModTParam
    Map Name ModParamNames
    Map Name (IfaceNames Name)
    Map Name (ModuleG Name)
    ExportSpec Name
    mName :: forall mname. ModuleG mname -> mname
    mDoc :: forall mname. ModuleG mname -> Maybe Text
    mExports :: forall mname. ModuleG mname -> ExportSpec Name
    mParamTypes :: forall mname. ModuleG mname -> Map Name ModTParam
    mParamFuns :: forall mname. ModuleG mname -> Map Name ModVParam
    mParamConstraints :: forall mname. ModuleG mname -> [Located Prop]
    mParams :: forall mname. ModuleG mname -> FunctorParams
    mFunctors :: forall mname. ModuleG mname -> Map Name (ModuleG Name)
    mNested :: forall mname. ModuleG mname -> Set Name
    mTySyns :: forall mname. ModuleG mname -> Map Name TySyn
    mNewtypes :: forall mname. ModuleG mname -> Map Name Newtype
    mPrimTypes :: forall mname. ModuleG mname -> Map Name AbstractType
    mDecls :: forall mname. ModuleG mname -> [DeclGroup]
    mSubmodules :: forall mname. ModuleG mname -> Map Name (IfaceNames Name)
    mSignatures :: forall mname. ModuleG mname -> Map Name ModParamNames
    mName :: n
    mDoc :: Maybe Text
    mExports :: ExportSpec Name
    mParamTypes :: Map Name ModTParam
    mParamFuns :: Map Name ModVParam
    mParamConstraints :: [Located Prop]
    mParams :: FunctorParams
    mFunctors :: Map Name (ModuleG Name)
    mNested :: Set Name
    mTySyns :: Map Name TySyn
    mNewtypes :: Map Name Newtype
    mPrimTypes :: Map Name AbstractType
    mDecls :: [DeclGroup]
    mSubmodules :: Map Name (IfaceNames Name)
    mSignatures :: Map Name ModParamNames
    .. } NameMap
    nm) =
        [Doc] -> Doc
    vcat [ String -> Doc
    text String
    "module" Doc -> Doc -> Doc
    <+> n -> Doc
    forall a. PP a => a -> Doc
    pp n
    mName
             -- XXX: Print exports?
             , [Doc] -> Doc
    vcat ((TySyn -> Doc) -> [TySyn] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TySyn -> Doc
    forall {a}. PP (WithNames a) => a -> Doc
    pp' (Map Name TySyn -> [TySyn]
    forall k a. Map k a -> [a]
    Map.elems Map Name TySyn
    mTySyns))
             -- XXX: Print abstarct types/functions
             , [Doc] -> Doc
    vcat ((DeclGroup -> Doc) -> [DeclGroup] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map DeclGroup -> Doc
    forall {a}. PP (WithNames a) => a -> Doc
    pp' [DeclGroup]
    mDecls)

             , [Doc] -> Doc
    vcat ((ModuleG Name -> Doc) -> [ModuleG Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ModuleG Name -> Doc
    forall a. PP a => a -> Doc
    pp (Map Name (ModuleG Name) -> [ModuleG Name]
    forall k a. Map k a -> [a]
    Map.elems Map Name (ModuleG Name)
    mFunctors))
             ]
        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)
              pp' :: PP (WithNames a) => a -> Doc
              pp' :: forall {a}. PP (WithNames a) => a -> Doc
    pp' = NameMap -> a -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames ([TParam] -> NameMap -> NameMap
    addTNames [TParam]
    mps NameMap
    nm)

    instance PP (WithNames TCTopEntity) where
      ppPrec :: Int -> WithNames TCTopEntity -> Doc
    ppPrec Int
    _ (WithNames TCTopEntity
    ent NameMap
    nm) =
        case TCTopEntity
    ent of
         TCTopModule ModuleG ModName
    m -> NameMap -> ModuleG ModName -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm ModuleG ModName
    m
         TCTopSignature ModName
    n ModParamNames
    ps ->
            Doc -> Int -> Doc -> Doc
    hang (Doc
    "interface module" Doc -> Doc -> Doc
    <+> ModName -> Doc
    forall a. PP a => a -> Doc
    pp ModName
    n Doc -> Doc -> Doc
    <+> Doc
    "where") Int
    2 (ModParamNames -> Doc
    forall a. PP a => a -> Doc
    pp ModParamNames
    ps)