-- |
-- 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 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
  , DocFor(..)
  ) where

import Data.Maybe(catMaybes)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim)
import Cryptol.Parser.Position(Located, HasLoc(..), Range)
import Cryptol.ModuleSystem.Name
import Cryptol.ModuleSystem.NamingEnv.Types
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 qualified Data.IntMap as IntMap
import           Data.Map    (Map)
import qualified Data.Map    as Map
import           Data.Maybe  (mapMaybe, maybeToList, isJust)
import           Data.Set    (Set)
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 -> [Text]
mDoc              :: ![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 NominalType
mNominalTypes     :: Map Name NominalType
                     , forall mname. ModuleG mname -> [DeclGroup]
mDecls            :: [DeclGroup]
                     , forall mname. ModuleG mname -> Map Name Submodule
mSubmodules       :: Map Name Submodule
                     , forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures       :: !(Map Name ModParamNames)

                     , forall mname. ModuleG mname -> NamingEnv
mInScope          :: NamingEnv
                       -- ^ Things in scope at the top level.
                       --   Submodule in-scope information is in 'mSubmodules'.
                     } 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)

data Submodule = Submodule
  { Submodule -> IfaceNames Name
smIface :: IfaceNames Name
  , Submodule -> NamingEnv
smInScope :: NamingEnv
  } deriving (Int -> Submodule -> ShowS
[Submodule] -> ShowS
Submodule -> String
(Int -> Submodule -> ShowS)
-> (Submodule -> String)
-> ([Submodule] -> ShowS)
-> Show Submodule
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Submodule -> ShowS
showsPrec :: Int -> Submodule -> ShowS
$cshow :: Submodule -> String
show :: Submodule -> String
$cshowList :: [Submodule] -> ShowS
showList :: [Submodule] -> ShowS
Show, (forall x. Submodule -> Rep Submodule x)
-> (forall x. Rep Submodule x -> Submodule) -> Generic Submodule
forall x. Rep Submodule x -> Submodule
forall x. Submodule -> Rep Submodule x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Submodule -> Rep Submodule x
from :: forall x. Submodule -> Rep Submodule x
$cto :: forall x. Rep Submodule x -> Submodule
to :: forall x. Rep Submodule x -> Submodule
Generic, Submodule -> ()
(Submodule -> ()) -> NFData Submodule
forall a. (a -> ()) -> NFData a
$crnf :: Submodule -> ()
rnf :: Submodule -> ()
NFData)

emptyModule :: mname -> ModuleG mname
emptyModule :: forall mname. mname -> ModuleG mname
emptyModule mname
nm =
  Module
    { mName :: mname
mName             = mname
nm
    , mDoc :: [Text]
mDoc              = [Text]
forall a. Monoid a => a
mempty
    , 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
    , mNominalTypes :: Map Name NominalType
mNominalTypes     = Map Name NominalType
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 Submodule
mSubmodules       = Map Name Submodule
forall a. Monoid a => a
mempty
    , mSignatures :: Map Name ModParamNames
mSignatures       = Map Name ModParamNames
forall a. Monoid a => a
mempty

    , mInScope :: NamingEnv
mInScope          = NamingEnv
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 = (Decl -> Maybe (Name, FFIFunType))
-> [Decl] -> [(Name, FFIFunType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Decl -> Maybe (Name, FFIFunType)
getForeign ([Decl] -> [(Name, FFIFunType)])
-> (ModuleG mname -> [Decl])
-> ModuleG mname
-> [(Name, FFIFunType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DeclGroup -> [Decl]) -> [DeclGroup] -> [Decl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DeclGroup -> [Decl]
groupDecls ([DeclGroup] -> [Decl])
-> (ModuleG mname -> [DeclGroup]) -> ModuleG mname -> [Decl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleG mname -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls
  where getForeign :: Decl -> Maybe (Name, FFIFunType)
getForeign Decl
d =
          case Decl -> DeclDef
dDefinition Decl
d of
            DForeign FFIFunType
ffiType Maybe Expr
_ -> (Name, FFIFunType) -> Maybe (Name, FFIFunType)
forall a. a -> Maybe a
Just (Decl -> Name
dName Decl
d, FFIFunType
ffiType)
            DeclDef
_                  -> Maybe (Name, FFIFunType)
forall a. Maybe a
Nothing

-- | Find all the foreign declarations that are in functors, including in the
-- top-level module itself if it is a functor.
-- This is used to report an error
findForeignDeclsInFunctors :: ModuleG mname -> [Name]
findForeignDeclsInFunctors :: forall mname. ModuleG mname -> [Name]
findForeignDeclsInFunctors ModuleG mname
mo
  | ModuleG mname -> Bool
forall mname. ModuleG mname -> Bool
isParametrizedModule ModuleG mname
mo = ModuleG mname -> [Name]
forall mname. ModuleG mname -> [Name]
fromM ModuleG mname
mo
  | Bool
otherwise               = ModuleG mname -> [Name]
forall mname. ModuleG mname -> [Name]
findInSubs ModuleG mname
mo
  where
  findInSubs :: ModuleG mname -> [Name]
  findInSubs :: forall mname. ModuleG mname -> [Name]
findInSubs = (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
  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]
findInSubs 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
            | ECase Expr (Map Ident CaseAlt) (Maybe CaseAlt)
              -- ^ Case expression. The keys are the name of constructors
              -- `Nothing` for default case, the expresssions are what to
              -- do if the constructor matches.  If the constructor binds
              -- variables, then then the expr should be `EAbs`
            | 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]

            {- | Use 'ePropGuards' when constructing to get automatic
                 simplification of trivial constraints -}
            | 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)

-- | Used for case expressions.  Similar to a lambda, the variables
-- are bound by the value examined in the case.
data CaseAlt = CaseAlt [(Name,Type)] Expr
  deriving (Int -> CaseAlt -> ShowS
[CaseAlt] -> ShowS
CaseAlt -> String
(Int -> CaseAlt -> ShowS)
-> (CaseAlt -> String) -> ([CaseAlt] -> ShowS) -> Show CaseAlt
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CaseAlt -> ShowS
showsPrec :: Int -> CaseAlt -> ShowS
$cshow :: CaseAlt -> String
show :: CaseAlt -> String
$cshowList :: [CaseAlt] -> ShowS
showList :: [CaseAlt] -> ShowS
Show, (forall x. CaseAlt -> Rep CaseAlt x)
-> (forall x. Rep CaseAlt x -> CaseAlt) -> Generic CaseAlt
forall x. Rep CaseAlt x -> CaseAlt
forall x. CaseAlt -> Rep CaseAlt x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CaseAlt -> Rep CaseAlt x
from :: forall x. CaseAlt -> Rep CaseAlt x
$cto :: forall x. Rep CaseAlt x -> CaseAlt
to :: forall x. Rep CaseAlt x -> CaseAlt
Generic, CaseAlt -> ()
(CaseAlt -> ()) -> NFData CaseAlt
forall a. (a -> ()) -> NFData a
$crnf :: CaseAlt -> ()
rnf :: CaseAlt -> ()
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
                -- | Foreign functions can have an optional cryptol
                -- implementation
                | DForeign FFIFunType (Maybe Expr)
                | 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

-- | Construct a prop guard expression simplifying trivial cases.
ePropGuards :: [([Prop], Expr)] -> Type -> Expr
ePropGuards :: [([Prop], Expr)] -> Prop -> Expr
ePropGuards [([Prop], Expr)]
guards Prop
ty =
  case Bool -> [([Prop], Expr)] -> Either Expr [([Prop], Expr)]
forall {t :: * -> *} {b}.
Foldable t =>
Bool -> [(t Prop, b)] -> Either b [(t Prop, b)]
check Bool
True [([Prop], Expr)]
guards of
    Left Expr
body     -> Expr
body
    Right [([Prop], Expr)]
guards' -> [([Prop], Expr)] -> Prop -> Expr
EPropGuards [([Prop], Expr)]
guards' Prop
ty
  where
    check :: Bool -> [(t Prop, b)] -> Either b [(t Prop, b)]
check Bool
_ [] = [(t Prop, b)] -> Either b [(t Prop, b)]
forall a b. b -> Either a b
Right []
    check Bool
trivial ((t Prop
p, b
e):[(t Prop, b)]
xs)
      | Bool
trivial, (Prop -> Bool) -> t Prop -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([Prop] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Prop] -> Bool) -> (Prop -> [Prop]) -> Prop -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop -> [Prop]
pSplitAnd) t Prop
p = b -> Either b [(t Prop, b)]
forall a b. a -> Either a b
Left b
e
      | Bool
otherwise = ((t Prop
p,b
e)(t Prop, b) -> [(t Prop, b)] -> [(t Prop, b)]
forall a. a -> [a] -> [a]
:) ([(t Prop, b)] -> [(t Prop, b)])
-> Either b [(t Prop, b)] -> Either b [(t Prop, b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> [(t Prop, b)] -> Either b [(t Prop, b)]
check Bool
trivial' [(t Prop, b)]
xs
      where
        trivial' :: Bool
trivial' = Bool
trivial Bool -> Bool -> Bool
&& (Prop -> Bool) -> t Prop -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe Prop -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Prop -> Bool) -> (Prop -> Maybe Prop) -> Prop -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop -> Maybe Prop
tIsError) t Prop
p

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 ]
      ECase Expr
e Map Ident CaseAlt
arms Maybe CaseAlt
dflt ->
        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
vcat [ Doc
"case" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
e Doc -> Doc -> Doc
<+> Doc
"of"
             , Int -> Doc -> Doc
indent Int
2 ([Doc] -> Doc
vcat [Doc]
ppArms Doc -> Doc -> Doc
$$ Doc
ppDflt)
             ]
        where
        ppArms :: [Doc]
ppArms  = [ Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
i Doc -> Doc -> Doc
<+> CaseAlt -> Doc
forall a. PP a => a -> Doc
pp CaseAlt
c | (Ident
i,CaseAlt
c) <- [(Ident, CaseAlt)] -> [(Ident, CaseAlt)]
forall a. [a] -> [a]
reverse (Map Ident CaseAlt -> [(Ident, CaseAlt)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Ident CaseAlt
arms) ]
        ppDflt :: Doc
ppDflt  = Doc -> (CaseAlt -> Doc) -> Maybe CaseAlt -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Monoid a => a
mempty CaseAlt -> Doc
forall a. PP a => a -> Doc
pp Maybe CaseAlt
dflt

      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

instance PP CaseAlt where
  ppPrec :: Int -> CaseAlt -> Doc
ppPrec Int
_ (CaseAlt [(Name, Prop)]
xs Expr
e) = [Doc] -> Doc
hsep (((Name, Prop) -> Doc) -> [(Name, Prop)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Prop) -> Doc
forall {a} {a}. (PP a, PP a) => (a, a) -> Doc
ppV [(Name, Prop)]
xs) Doc -> Doc -> Doc
<+> Doc
"->" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
e
    where ppV :: (a, a) -> Doc
ppV (a
x,a
t) = Doc -> Doc
parens (a -> Doc
forall a. PP a => a -> Doc
pp a
x Doc -> Doc -> Doc
<.> Doc
":" Doc -> Doc -> Doc
<+> a -> Doc
forall a. PP a => a -> Doc
pp a
t)

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
dDefinition :: Decl -> DeclDef
dName :: Decl -> Name
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
_ Maybe Expr
me) NameMap
nm) =
    case Maybe Expr
me of
      Just Expr
e -> String -> Doc
text String
"(foreign)" Doc -> Doc -> Doc
<+> NameMap -> Expr -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm Expr
e
      Maybe Expr
Nothing -> 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
[Text]
[Located Prop]
[DeclGroup]
FunctorParams
Map Name NominalType
Map Name TySyn
Map Name ModVParam
Map Name ModTParam
Map Name ModParamNames
Map Name Submodule
Map Name (ModuleG Name)
Set Name
NamingEnv
ExportSpec Name
mName :: forall mname. ModuleG mname -> mname
mDoc :: forall mname. ModuleG mname -> [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
mNominalTypes :: forall mname. ModuleG mname -> Map Name NominalType
mDecls :: forall mname. ModuleG mname -> [DeclGroup]
mSubmodules :: forall mname. ModuleG mname -> Map Name Submodule
mSignatures :: forall mname. ModuleG mname -> Map Name ModParamNames
mInScope :: forall mname. ModuleG mname -> NamingEnv
mName :: n
mDoc :: [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
mNominalTypes :: Map Name NominalType
mDecls :: [DeclGroup]
mSubmodules :: Map Name Submodule
mSignatures :: Map Name ModParamNames
mInScope :: NamingEnv
.. } NameMap
nm) =
    [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    [Maybe Doc] -> [Doc]
forall a. [Maybe a] -> [a]
catMaybes
         [ Doc -> Maybe Doc
forall a. a -> Maybe a
Just (String -> Doc
text String
"module" Doc -> Doc -> Doc
<+> n -> Doc
forall a. PP a => a -> Doc
pp n
mName)
         , Doc -> Maybe Doc
forall a. a -> Maybe a
Just Doc
""
         -- XXX: Print exports?
         , [Doc] -> Maybe 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] -> Maybe 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] -> Maybe 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))

         , [Doc] -> Maybe Doc
vcat' (((Name, ModParamNames) -> Doc) -> [(Name, ModParamNames)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, ModParamNames) -> Doc
forall {a} {a}. (PP a, PP a) => (a, a) -> Doc
ppSig (Map Name ModParamNames -> [(Name, ModParamNames)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Name ModParamNames
mSignatures))
         ]
    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)
          ppSig :: (a, a) -> Doc
ppSig (a
x,a
y) = Doc
"interface module" Doc -> Doc -> Doc
<+> a -> Doc
forall a. PP a => a -> Doc
pp a
x Doc -> Doc -> Doc
<+> Doc
"where"
                        Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
indent Int
2 (a -> Doc
forall a. PP a => a -> Doc
pp a
y)
          vcat' :: [Doc] -> Maybe Doc
vcat' [Doc]
xs = if [Doc] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
xs then Maybe Doc
forall a. Maybe a
Nothing else Doc -> Maybe Doc
forall a. a -> Maybe a
Just ([Doc] -> Doc
vcat [Doc]
xs)

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)

data DocItem = DocItem
  { DocItem -> ImpName Name
docModContext :: ImpName Name -- ^ The module scope to run repl commands in
  , DocItem -> DocFor
docFor        :: DocFor -- ^ The name the documentation is attached to
  , DocItem -> [Text]
docText       :: [Text] -- ^ The text of the attached docstring, if any
  }

data DocFor
  = DocForMod (ImpName Name)
  | DocForDef Name -- definitions that aren't modules

instance PP DocFor where
  ppPrec :: Int -> DocFor -> Doc
ppPrec Int
p DocFor
x =
    case DocFor
x of
      DocForMod ImpName Name
m -> Int -> ImpName Name -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
p ImpName Name
m
      DocForDef Name
n -> Int -> Name -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
p Name
n 


gatherModuleDocstrings ::
  Map Name (ImpName Name) ->
  Module ->
  [DocItem]
gatherModuleDocstrings :: Map Name (ImpName Name) -> ModuleG ModName -> [DocItem]
gatherModuleDocstrings Map Name (ImpName Name)
nameToModule ModuleG ModName
m =
  [DocItem
    { docModContext :: ImpName Name
docModContext = ModName -> ImpName Name
forall name. ModName -> ImpName name
ImpTop (ModuleG ModName -> ModName
forall mname. ModuleG mname -> mname
mName ModuleG ModName
m)
    , docFor :: DocFor
docFor = ImpName Name -> DocFor
DocForMod (ModName -> ImpName Name
forall name. ModName -> ImpName name
ImpTop (ModuleG ModName -> ModName
forall mname. ModuleG mname -> mname
mName ModuleG ModName
m))
    , docText :: [Text]
docText = ModuleG ModName -> [Text]
forall mname. ModuleG mname -> [Text]
mDoc ModuleG ModName
m
    }
  ] [DocItem] -> [DocItem] -> [DocItem]
forall a. [a] -> [a] -> [a]
++
  -- mParams m
  -- mParamTypes m
  -- mParamFuns m
  [DocItem
    { docModContext :: ImpName Name
docModContext = Name -> ImpName Name
lookupModuleName Name
n
    , docFor :: DocFor
docFor = Name -> DocFor
DocForDef Name
n
    , docText :: [Text]
docText = Maybe Text -> [Text]
forall a. Maybe a -> [a]
maybeToList (TySyn -> Maybe Text
tsDoc TySyn
t)
    } | (Name
n, TySyn
t) <- Map Name TySyn -> [(Name, TySyn)]
forall k a. Map k a -> [(k, a)]
Map.assocs (ModuleG ModName -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ModName
m)] [DocItem] -> [DocItem] -> [DocItem]
forall a. [a] -> [a] -> [a]
++
  [DocItem
    { docModContext :: ImpName Name
docModContext = Name -> ImpName Name
lookupModuleName Name
n
    , docFor :: DocFor
docFor = Name -> DocFor
DocForDef Name
n
    , docText :: [Text]
docText = Maybe Text -> [Text]
forall a. Maybe a -> [a]
maybeToList (NominalType -> Maybe Text
ntDoc NominalType
t)
    } | (Name
n, NominalType
t) <- Map Name NominalType -> [(Name, NominalType)]
forall k a. Map k a -> [(k, a)]
Map.assocs (ModuleG ModName -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes ModuleG ModName
m)] [DocItem] -> [DocItem] -> [DocItem]
forall a. [a] -> [a] -> [a]
++
  [DocItem
    { docModContext :: ImpName Name
docModContext = Name -> ImpName Name
lookupModuleName (Decl -> Name
dName Decl
d)
    , docFor :: DocFor
docFor = Name -> DocFor
DocForDef (Decl -> Name
dName Decl
d)
    , docText :: [Text]
docText = Maybe Text -> [Text]
forall a. Maybe a -> [a]
maybeToList (Decl -> Maybe Text
dDoc Decl
d)
    } | DeclGroup
g <- ModuleG ModName -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ModName
m, Decl
d <- DeclGroup -> [Decl]
groupDecls DeclGroup
g] [DocItem] -> [DocItem] -> [DocItem]
forall a. [a] -> [a] -> [a]
++
  [DocItem
    { docModContext :: ImpName Name
docModContext = Name -> ImpName Name
forall name. name -> ImpName name
ImpNested Name
n
    , docFor :: DocFor
docFor = ImpName Name -> DocFor
DocForMod (Name -> ImpName Name
forall name. name -> ImpName name
ImpNested Name
n)
    , docText :: [Text]
docText = IfaceNames Name -> [Text]
forall name. IfaceNames name -> [Text]
ifsDoc (Submodule -> IfaceNames Name
smIface Submodule
s)
    } | (Name
n, Submodule
s) <- Map Name Submodule -> [(Name, Submodule)]
forall k a. Map k a -> [(k, a)]
Map.assocs (ModuleG ModName -> Map Name Submodule
forall mname. ModuleG mname -> Map Name Submodule
mSubmodules ModuleG ModName
m)] [DocItem] -> [DocItem] -> [DocItem]
forall a. [a] -> [a] -> [a]
++
  [DocItem
    { docModContext :: ImpName Name
docModContext = ModName -> ImpName Name
forall name. ModName -> ImpName name
ImpTop (ModuleG ModName -> ModName
forall mname. ModuleG mname -> mname
mName ModuleG ModName
m)
    , docFor :: DocFor
docFor = ImpName Name -> DocFor
DocForMod (Name -> ImpName Name
forall name. name -> ImpName name
ImpNested Name
n)
    , docText :: [Text]
docText = Maybe Text -> [Text]
forall a. Maybe a -> [a]
maybeToList (ModParamNames -> Maybe Text
mpnDoc ModParamNames
s)
    } | (Name
n, ModParamNames
s) <- Map Name ModParamNames -> [(Name, ModParamNames)]
forall k a. Map k a -> [(k, a)]
Map.assocs (ModuleG ModName -> Map Name ModParamNames
forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures ModuleG ModName
m)]
  where
    lookupModuleName :: Name -> ImpName Name
lookupModuleName Name
n =
      case Name -> Map Name (ImpName Name) -> Maybe (ImpName Name)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name (ImpName Name)
nameToModule of
        Just ImpName Name
x -> ImpName Name
x
        Maybe (ImpName Name)
Nothing -> String -> [String] -> ImpName Name
forall a. HasCallStack => String -> [String] -> a
panic String
"gatherModuleDocstrings" [String
"No owning module for name:", Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
forall a. PP a => a -> Doc
pp Name
n)]