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

{-# LANGUAGE Safe                                #-}

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

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

import GHC.Generics (Generic)
import Control.DeepSeq

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


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

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

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

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

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

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

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


data Expr   = EList [Expr] Type         -- ^ List value (with type of elements)
            | ETuple [Expr]             -- ^ Tuple value
            | ERec (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


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

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

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

            | EProofApp Expr {- proof -}

            | EWhere Expr [DeclGroup]

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


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

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

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

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


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

-- | Construct a primitive, given a map to the unique 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 (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 (WithNames Expr) where
  ppPrec :: Int -> WithNames Expr -> Doc
ppPrec Int
prec (WithNames Expr
expr NameMap
nm) =
    case Expr
expr of
      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
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Expr -> Doc) -> [Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW [Expr]
es

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

      ERec RecordMap Ident Expr
fs       -> Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma
                        [ Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
f Doc -> Doc -> Doc
<+> String -> Doc
text 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
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)
                     ( Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e Doc -> Doc -> Doc
$$ String -> Doc
text String
"where"
                                     Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 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))
                                     Doc -> Doc -> Doc
$$ String -> Doc
text String
"" )

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

  ppT :: TParam -> Doc
ppT = NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1
  ppP :: Prop -> Doc
ppP = NameMap -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1
  ppArg :: (a, a) -> Doc
ppArg (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 :: (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)

splitAbs :: Expr -> Maybe ((Name,Type), Expr)
splitAbs :: Expr -> Maybe ((Name, Prop), Expr)
splitAbs (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

splitTAbs :: Expr -> Maybe (TParam, Expr)
splitTAbs :: Expr -> Maybe (TParam, Expr)
splitTAbs (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 (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 (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 (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 (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 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
dDoc :: Maybe Text
dFixity :: Maybe Fixity
dInfix :: Bool
dPragmas :: [Pragma]
dDefinition :: DeclDef
dSignature :: Schema
dName :: Name
dDoc :: Decl -> Maybe Text
dFixity :: Decl -> Maybe Fixity
dInfix :: Decl -> Bool
dPragmas :: Decl -> [Pragma]
dDefinition :: Decl -> DeclDef
dSignature :: Decl -> Schema
dName :: Decl -> Name
.. } NameMap
nm) =
    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
$$
    (if [Pragma] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pragma]
dPragmas
        then Doc
empty
        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
$$
    Name -> Doc
forall a. PP a => a -> Doc
pp Name
dName Doc -> Doc -> Doc
<+> String -> Doc
text String
"=" Doc -> Doc -> Doc
<+> NameMap -> DeclDef -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm DeclDef
dDefinition

instance PP (WithNames DeclDef) where
  ppPrec :: Int -> WithNames DeclDef -> Doc
ppPrec Int
_ (WithNames DeclDef
DPrim NameMap
_)      = String -> Doc
text String
"<primitive>"
  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 Module where
  ppPrec :: Int -> Module -> Doc
ppPrec = NameMap -> Int -> Module -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty

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