{-# Language FlexibleInstances, PatternGuards #-}
-- | Assumes that local names do not shadow top level names.
module Cryptol.ModuleSystem.InstantiateModule
  ( instantiateModule
  ) where

import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.Map (Map)
import qualified Data.Map as Map
import           MonadLib(ReaderT,runReaderT,ask)

import Cryptol.Parser.Position(Located(..))
import Cryptol.ModuleSystem.Name
import Cryptol.ModuleSystem.Exports(ExportSpec(..))
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst(listParamSubst, apSubst)
import Cryptol.Utils.Ident(ModName,modParamIdent)

{-
XXX: Should we simplify constraints in the instantiated modules?

If so, we also need to adjust the constraint parameters on terms appropriately,
especially when working with dictionaries.
-}


-- | Convert a module instantiation into a partial module.
-- The resulting module is incomplete because it is missing the definitions
-- from the instantiation.
instantiateModule :: FreshM m =>
                     Module           {- ^ Parametrized module -} ->
                     ModName          {- ^ Name of the new module -} ->
                     Map TParam Type  {- ^ Type params -} ->
                     Map Name Expr    {- ^ Value parameters -} ->
                     m ([Located Prop], Module)
                     -- ^ Instantiated constraints, fresh module, new supply
instantiateModule :: Module
-> ModName
-> Map TParam Type
-> Map Name Expr
-> m ([Located Type], Module)
instantiateModule func :: Module
func newName :: ModName
newName tpMap :: Map TParam Type
tpMap vpMap :: Map Name Expr
vpMap =
  ModName
-> ReaderT ModName m ([Located Type], Module)
-> m ([Located Type], Module)
forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
runReaderT ModName
newName (ReaderT ModName m ([Located Type], Module)
 -> m ([Located Type], Module))
-> ReaderT ModName m ([Located Type], Module)
-> m ([Located Type], Module)
forall a b. (a -> b) -> a -> b
$
    do let oldVpNames :: [Name]
oldVpNames = Map Name Expr -> [Name]
forall k a. Map k a -> [k]
Map.keys Map Name Expr
vpMap
       [Name]
newVpNames <- (Name -> ReaderT ModName m Name)
-> [Name] -> ReaderT ModName m [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> ReaderT ModName m Name
forall (m :: * -> *). FreshM m => Name -> InstM m Name
freshParamName (Map Name Expr -> [Name]
forall k a. Map k a -> [k]
Map.keys Map Name Expr
vpMap)
       let vpNames :: Map Name Name
vpNames = [(Name, Name)] -> Map Name Name
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([Name] -> [Name] -> [(Name, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
oldVpNames [Name]
newVpNames)

       Env
env <- Module -> Map TParam Type -> Map Name Name -> InstM m Env
forall (m :: * -> *).
FreshM m =>
Module -> Map TParam Type -> Map Name Name -> InstM m Env
computeEnv Module
func Map TParam Type
tpMap Map Name Name
vpNames

       let rnMp :: Inst a => (a -> Name) -> Map Name a -> Map Name a
           rnMp :: (a -> Name) -> Map Name a -> Map Name a
rnMp f :: a -> Name
f m :: Map Name a
m = [(Name, a)] -> Map Name a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (a -> Name
f a
x, a
x) | a
a <- Map Name a -> [a]
forall k a. Map k a -> [a]
Map.elems Map Name a
m
                                              , let x :: a
x = Env -> a -> a
forall t. Inst t => Env -> t -> t
inst Env
env a
a ]

           renamedExports :: ExportSpec Name
renamedExports  = Env -> ExportSpec Name -> ExportSpec Name
forall t. Inst t => Env -> t -> t
inst Env
env (Module -> ExportSpec Name
mExports Module
func)
           renamedTySyns :: Map Name TySyn
renamedTySyns   = (TySyn -> Name) -> Map Name TySyn -> Map Name TySyn
forall a. Inst a => (a -> Name) -> Map Name a -> Map Name a
rnMp TySyn -> Name
tsName (Module -> Map Name TySyn
mTySyns Module
func)
           renamedNewtypes :: Map Name Newtype
renamedNewtypes = (Newtype -> Name) -> Map Name Newtype -> Map Name Newtype
forall a. Inst a => (a -> Name) -> Map Name a -> Map Name a
rnMp Newtype -> Name
ntName (Module -> Map Name Newtype
mNewtypes Module
func)
           renamedPrimTys :: Map Name AbstractType
renamedPrimTys  = (AbstractType -> Name)
-> Map Name AbstractType -> Map Name AbstractType
forall a. Inst a => (a -> Name) -> Map Name a -> Map Name a
rnMp AbstractType -> Name
atName (Module -> Map Name AbstractType
mPrimTypes Module
func)

           su :: Subst
su = [(TParam, Type)] -> Subst
listParamSubst (Map TParam Type -> [(TParam, Type)]
forall k a. Map k a -> [(k, a)]
Map.toList (Env -> Map TParam Type
tyParamMap Env
env))

           goals :: [Located Type]
goals = (Located Type -> Located Type) -> [Located Type] -> [Located Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> Located Type -> Located Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su)) (Module -> [Located Type]
mParamConstraints Module
func)
           -- Constraints to discharge about the type instances

       let renamedDecls :: [DeclGroup]
renamedDecls = Env -> [DeclGroup] -> [DeclGroup]
forall t. Inst t => Env -> t -> t
inst Env
env (Module -> [DeclGroup]
mDecls Module
func)
           paramDecls :: [DeclGroup]
paramDecls = ((Name, Expr) -> DeclGroup) -> [(Name, Expr)] -> [DeclGroup]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Map Name Name -> (Name, Expr) -> DeclGroup
mkParamDecl Subst
su Map Name Name
vpNames) (Map Name Expr -> [(Name, Expr)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Name Expr
vpMap)

       ([Located Type], Module)
-> ReaderT ModName m ([Located Type], Module)
forall (m :: * -> *) a. Monad m => a -> m a
return ( [Located Type]
goals
              , $WModule :: ModName
-> ExportSpec Name
-> [Import]
-> Map Name TySyn
-> Map Name Newtype
-> Map Name AbstractType
-> Map Name ModTParam
-> [Located Type]
-> Map Name ModVParam
-> [DeclGroup]
-> Module
Module
                 { mName :: ModName
mName              = ModName
newName
                 , mExports :: ExportSpec Name
mExports           = ExportSpec Name
renamedExports
                 , mImports :: [Import]
mImports           = Module -> [Import]
mImports Module
func
                 , mTySyns :: Map Name TySyn
mTySyns            = Map Name TySyn
renamedTySyns
                 , mNewtypes :: Map Name Newtype
mNewtypes          = Map Name Newtype
renamedNewtypes
                 , mPrimTypes :: Map Name AbstractType
mPrimTypes         = Map Name AbstractType
renamedPrimTys
                 , mParamTypes :: Map Name ModTParam
mParamTypes        = Map Name ModTParam
forall k a. Map k a
Map.empty
                 , mParamConstraints :: [Located Type]
mParamConstraints  = []
                 , mParamFuns :: Map Name ModVParam
mParamFuns         = Map Name ModVParam
forall k a. Map k a
Map.empty
                 , mDecls :: [DeclGroup]
mDecls             = [DeclGroup]
paramDecls [DeclGroup] -> [DeclGroup] -> [DeclGroup]
forall a. [a] -> [a] -> [a]
++ [DeclGroup]
renamedDecls
                 } )

  where
  mkParamDecl :: Subst -> Map Name Name -> (Name, Expr) -> DeclGroup
mkParamDecl su :: Subst
su vpNames :: Map Name Name
vpNames (x :: Name
x,e :: Expr
e) =
      Decl -> DeclGroup
NonRecursive $WDecl :: Name
-> Schema
-> DeclDef
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe String
-> Decl
Decl
        { dName :: Name
dName        = Name -> Name -> Map Name Name -> Name
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Name
forall a. HasCallStack => String -> a
error "OOPS") Name
x Map Name Name
vpNames
        , dSignature :: Schema
dSignature   = Subst -> Schema -> Schema
forall t. TVars t => Subst -> t -> t
apSubst Subst
su
                       (Schema -> Schema) -> Schema -> Schema
forall a b. (a -> b) -> a -> b
$ ModVParam -> Schema
mvpType
                       (ModVParam -> Schema) -> ModVParam -> Schema
forall a b. (a -> b) -> a -> b
$ ModVParam -> Name -> Map Name ModVParam -> ModVParam
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> ModVParam
forall a. HasCallStack => String -> a
error "UUPS") Name
x (Module -> Map Name ModVParam
mParamFuns Module
func)
        , dDefinition :: DeclDef
dDefinition  = Expr -> DeclDef
DExpr Expr
e
        , dPragmas :: [Pragma]
dPragmas     = []      -- XXX: which if any pragmas?
        , dInfix :: Bool
dInfix       = Bool
False   -- XXX: get from parameter?
        , dFixity :: Maybe Fixity
dFixity      = Maybe Fixity
forall a. Maybe a
Nothing -- XXX: get from parameter
        , dDoc :: Maybe String
dDoc         = Maybe String
forall a. Maybe a
Nothing -- XXX: get from parametr(or instance?)
        }


--------------------------------------------------------------------------------
-- Things that need to be renamed

class Defines t where
  defines :: t -> Set Name

instance Defines t => Defines [t] where
  defines :: [t] -> Set Name
defines = [Set Name] -> Set Name
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Name] -> Set Name) -> ([t] -> [Set Name]) -> [t] -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> Set Name) -> [t] -> [Set Name]
forall a b. (a -> b) -> [a] -> [b]
map t -> Set Name
forall t. Defines t => t -> Set Name
defines

instance Defines Decl where
  defines :: Decl -> Set Name
defines = Name -> Set Name
forall a. a -> Set a
Set.singleton (Name -> Set Name) -> (Decl -> Name) -> Decl -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decl -> Name
dName

instance Defines DeclGroup where
  defines :: DeclGroup -> Set Name
defines d :: DeclGroup
d =
    case DeclGroup
d of
      NonRecursive x :: Decl
x -> Decl -> Set Name
forall t. Defines t => t -> Set Name
defines Decl
x
      Recursive x :: [Decl]
x    -> [Decl] -> Set Name
forall t. Defines t => t -> Set Name
defines [Decl]
x


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

type InstM = ReaderT ModName

-- | Generate a new instance of a declared name.
freshenName :: FreshM m => Name -> InstM m Name
freshenName :: Name -> InstM m Name
freshenName x :: Name
x =
  do ModName
m <- ReaderT ModName m ModName
forall (m :: * -> *) i. ReaderM m i => m i
ask
     let sys :: NameSource
sys = case Name -> NameInfo
nameInfo Name
x of
                 Declared _ s :: NameSource
s -> NameSource
s
                 _            -> NameSource
UserName
     (Supply -> (Name, Supply)) -> InstM m Name
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply (ModName
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
mkDeclared ModName
m NameSource
sys (Name -> Ident
nameIdent Name
x) (Name -> Maybe Fixity
nameFixity Name
x) (Name -> Range
nameLoc Name
x))

freshParamName :: FreshM m => Name -> InstM m Name
freshParamName :: Name -> InstM m Name
freshParamName x :: Name
x =
  do ModName
m <- ReaderT ModName m ModName
forall (m :: * -> *) i. ReaderM m i => m i
ask
     let newName :: Ident
newName = Ident -> Ident
modParamIdent (Name -> Ident
nameIdent Name
x)
     (Supply -> (Name, Supply)) -> InstM m Name
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply (ModName
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
mkDeclared ModName
m NameSource
UserName Ident
newName (Name -> Maybe Fixity
nameFixity Name
x) (Name -> Range
nameLoc Name
x))




-- | Compute renaming environment from a module instantiation.
-- computeEnv :: ModInst -> InstM Env
computeEnv :: FreshM m =>
              Module {- ^ Functor being instantiated -} ->
              Map TParam Type {- replace type params by type -} ->
              Map Name Name {- replace value parameters by other names -} ->
              InstM m Env
computeEnv :: Module -> Map TParam Type -> Map Name Name -> InstM m Env
computeEnv m :: Module
m tpMap :: Map TParam Type
tpMap vpMap :: Map Name Name
vpMap =
  do [(Name, Name)]
tss <- ((Name, TySyn) -> ReaderT ModName m (Name, Name))
-> [(Name, TySyn)] -> ReaderT ModName m [(Name, Name)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, TySyn) -> ReaderT ModName m (Name, Name)
forall (m :: * -> *) b.
FreshM m =>
(Name, b) -> ReaderT ModName m (Name, Name)
freshTy (Map Name TySyn -> [(Name, TySyn)]
forall k a. Map k a -> [(k, a)]
Map.toList (Module -> Map Name TySyn
mTySyns Module
m))
     [(Name, Name)]
nts <- ((Name, Newtype) -> ReaderT ModName m (Name, Name))
-> [(Name, Newtype)] -> ReaderT ModName m [(Name, Name)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, Newtype) -> ReaderT ModName m (Name, Name)
forall (m :: * -> *) b.
FreshM m =>
(Name, b) -> ReaderT ModName m (Name, Name)
freshTy (Map Name Newtype -> [(Name, Newtype)]
forall k a. Map k a -> [(k, a)]
Map.toList (Module -> Map Name Newtype
mNewtypes Module
m))
     let tnMap :: Map Name Name
tnMap = [(Name, Name)] -> Map Name Name
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, Name)]
tss [(Name, Name)] -> [(Name, Name)] -> [(Name, Name)]
forall a. [a] -> [a] -> [a]
++ [(Name, Name)]
nts)

     [(Name, Name)]
defHere <- (Name -> ReaderT ModName m (Name, Name))
-> [Name] -> ReaderT ModName m [(Name, Name)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> ReaderT ModName m (Name, Name)
forall (m :: * -> *).
FreshM m =>
Name -> ReaderT ModName m (Name, Name)
mkVParam (Set Name -> [Name]
forall a. Set a -> [a]
Set.toList ([DeclGroup] -> Set Name
forall t. Defines t => t -> Set Name
defines (Module -> [DeclGroup]
mDecls Module
m)))
     let fnMap :: Map Name Name
fnMap = Map Name Name -> Map Name Name -> Map Name Name
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Name Name
vpMap ([(Name, Name)] -> Map Name Name
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Name, Name)]
defHere)

     Env -> InstM m Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env :: Map Name Name -> Map Name Name -> Map TParam Type -> Env
Env { funNameMap :: Map Name Name
funNameMap  = Map Name Name
fnMap
                , tyNameMap :: Map Name Name
tyNameMap   = Map Name Name
tnMap
                , tyParamMap :: Map TParam Type
tyParamMap  = Map TParam Type
tpMap
                }
  where
  freshTy :: (Name, b) -> ReaderT ModName m (Name, Name)
freshTy (x :: Name
x,_) = do Name
y <- Name -> InstM m Name
forall (m :: * -> *). FreshM m => Name -> InstM m Name
freshenName Name
x
                     (Name, Name) -> ReaderT ModName m (Name, Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x,Name
y)

  mkVParam :: Name -> ReaderT ModName m (Name, Name)
mkVParam x :: Name
x = do Name
y <- Name -> InstM m Name
forall (m :: * -> *). FreshM m => Name -> InstM m Name
freshenName Name
x
                  (Name, Name) -> ReaderT ModName m (Name, Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x,Name
y)



--------------------------------------------------------------------------------
-- Do the renaming

data Env = Env
  { Env -> Map Name Name
funNameMap  :: Map Name Name
  , Env -> Map Name Name
tyNameMap   :: Map Name Name
  , Env -> Map TParam Type
tyParamMap  :: Map TParam Type
  } deriving Int -> Env -> ShowS
[Env] -> ShowS
Env -> String
(Int -> Env -> ShowS)
-> (Env -> String) -> ([Env] -> ShowS) -> Show Env
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Env] -> ShowS
$cshowList :: [Env] -> ShowS
show :: Env -> String
$cshow :: Env -> String
showsPrec :: Int -> Env -> ShowS
$cshowsPrec :: Int -> Env -> ShowS
Show


class Inst t where
  inst :: Env -> t -> t

instance Inst a => Inst [a] where
  inst :: Env -> [a] -> [a]
inst env :: Env
env = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> a -> a
forall t. Inst t => Env -> t -> t
inst Env
env)

instance Inst Expr where
  inst :: Env -> Expr -> Expr
inst env :: Env
env = Expr -> Expr
go
    where
    go :: Expr -> Expr
go expr :: Expr
expr =
      case Expr
expr of
        EVar x :: Name
x -> case Name -> Map Name Name -> Maybe Name
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (Env -> Map Name Name
funNameMap Env
env) of
                    Just y :: Name
y -> Name -> Expr
EVar Name
y
                    _      -> Expr
expr

        EList xs :: [Expr]
xs t :: Type
t                -> [Expr] -> Type -> Expr
EList (Env -> [Expr] -> [Expr]
forall t. Inst t => Env -> t -> t
inst Env
env [Expr]
xs) (Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env Type
t)
        ETuple es :: [Expr]
es                 -> [Expr] -> Expr
ETuple (Env -> [Expr] -> [Expr]
forall t. Inst t => Env -> t -> t
inst Env
env [Expr]
es)
        ERec xs :: [(Ident, Expr)]
xs                   -> [(Ident, Expr)] -> Expr
ERec [ (Ident
f,Expr -> Expr
go Expr
e) | (f :: Ident
f,e :: Expr
e) <- [(Ident, Expr)]
xs ]
        ESel e :: Expr
e s :: Selector
s                  -> Expr -> Selector -> Expr
ESel (Expr -> Expr
go Expr
e) Selector
s
        ESet e :: Expr
e x :: Selector
x v :: Expr
v                -> Expr -> Selector -> Expr -> Expr
ESet (Expr -> Expr
go Expr
e) Selector
x (Expr -> Expr
go Expr
v)
        EIf e1 :: Expr
e1 e2 :: Expr
e2 e3 :: Expr
e3              -> Expr -> Expr -> Expr -> Expr
EIf (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2) (Expr -> Expr
go Expr
e3)
        EComp t1 :: Type
t1 t2 :: Type
t2 e :: Expr
e mss :: [[Match]]
mss         -> Type -> Type -> Expr -> [[Match]] -> Expr
EComp (Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env Type
t1) (Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env Type
t2)
                                           (Expr -> Expr
go Expr
e)
                                           (Env -> [[Match]] -> [[Match]]
forall t. Inst t => Env -> t -> t
inst Env
env [[Match]]
mss)
        ETAbs t :: TParam
t e :: Expr
e                 -> TParam -> Expr -> Expr
ETAbs TParam
t (Expr -> Expr
go Expr
e)
        ETApp e :: Expr
e t :: Type
t                 -> Expr -> Type -> Expr
ETApp (Expr -> Expr
go Expr
e) (Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env Type
t)
        EApp e1 :: Expr
e1 e2 :: Expr
e2                -> Expr -> Expr -> Expr
EApp (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
        EAbs x :: Name
x t :: Type
t e :: Expr
e                -> Name -> Type -> Expr -> Expr
EAbs Name
x (Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env Type
t) (Expr -> Expr
go Expr
e)
        EProofAbs p :: Type
p e :: Expr
e             -> Type -> Expr -> Expr
EProofAbs (Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env Type
p) (Expr -> Expr
go Expr
e)
        EProofApp e :: Expr
e               -> Expr -> Expr
EProofApp (Expr -> Expr
go Expr
e)
        EWhere e :: Expr
e ds :: [DeclGroup]
ds               -> Expr -> [DeclGroup] -> Expr
EWhere (Expr -> Expr
go Expr
e) (Env -> [DeclGroup] -> [DeclGroup]
forall t. Inst t => Env -> t -> t
inst Env
env [DeclGroup]
ds)


instance Inst DeclGroup where
  inst :: Env -> DeclGroup -> DeclGroup
inst env :: Env
env dg :: DeclGroup
dg =
    case DeclGroup
dg of
      NonRecursive d :: Decl
d -> Decl -> DeclGroup
NonRecursive (Env -> Decl -> Decl
forall t. Inst t => Env -> t -> t
inst Env
env Decl
d)
      Recursive ds :: [Decl]
ds   -> [Decl] -> DeclGroup
Recursive (Env -> [Decl] -> [Decl]
forall t. Inst t => Env -> t -> t
inst Env
env [Decl]
ds)

instance Inst DeclDef where
  inst :: Env -> DeclDef -> DeclDef
inst env :: Env
env d :: DeclDef
d =
    case DeclDef
d of
      DPrim   -> DeclDef
DPrim
      DExpr e :: Expr
e -> Expr -> DeclDef
DExpr (Env -> Expr -> Expr
forall t. Inst t => Env -> t -> t
inst Env
env Expr
e)

instance Inst Decl where
  inst :: Env -> Decl -> Decl
inst env :: Env
env d :: Decl
d = Decl
d { dSignature :: Schema
dSignature = Env -> Schema -> Schema
forall t. Inst t => Env -> t -> t
inst Env
env (Decl -> Schema
dSignature Decl
d)
                 , dDefinition :: DeclDef
dDefinition = Env -> DeclDef -> DeclDef
forall t. Inst t => Env -> t -> t
inst Env
env (Decl -> DeclDef
dDefinition Decl
d)
                 , dName :: Name
dName = Name -> Name -> Map Name Name -> Name
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (Decl -> Name
dName Decl
d) (Decl -> Name
dName Decl
d)
                                                         (Env -> Map Name Name
funNameMap Env
env)
                 }

instance Inst Match where
  inst :: Env -> Match -> Match
inst env :: Env
env m :: Match
m =
    case Match
m of
      From x :: Name
x t1 :: Type
t1 t2 :: Type
t2 e :: Expr
e -> Name -> Type -> Type -> Expr -> Match
From Name
x (Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env Type
t1) (Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env Type
t2) (Env -> Expr -> Expr
forall t. Inst t => Env -> t -> t
inst Env
env Expr
e)
      Let d :: Decl
d          -> Decl -> Match
Let (Env -> Decl -> Decl
forall t. Inst t => Env -> t -> t
inst Env
env Decl
d)

instance Inst Schema where
  inst :: Env -> Schema -> Schema
inst env :: Env
env s :: Schema
s = Schema
s { sProps :: [Type]
sProps = Env -> [Type] -> [Type]
forall t. Inst t => Env -> t -> t
inst Env
env (Schema -> [Type]
sProps Schema
s)
                 , sType :: Type
sType  = Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env (Schema -> Type
sType Schema
s)
                 }

instance Inst Type where
  inst :: Env -> Type -> Type
inst env :: Env
env ty :: Type
ty =
    case Type
ty of
      TCon tc :: TCon
tc ts :: [Type]
ts    -> TCon -> [Type] -> Type
TCon (Env -> TCon -> TCon
forall t. Inst t => Env -> t -> t
inst Env
env TCon
tc) (Env -> [Type] -> [Type]
forall t. Inst t => Env -> t -> t
inst Env
env [Type]
ts)
      TVar tv :: TVar
tv       ->
        case TVar
tv of
          TVBound tp :: TParam
tp | Just t :: Type
t <- TParam -> Map TParam Type -> Maybe Type
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TParam
tp (Env -> Map TParam Type
tyParamMap Env
env) -> Type
t
          _ -> Type
ty
      TUser x :: Name
x ts :: [Type]
ts t :: Type
t  -> Name -> [Type] -> Type -> Type
TUser Name
y (Env -> [Type] -> [Type]
forall t. Inst t => Env -> t -> t
inst Env
env [Type]
ts) (Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env Type
t)
        where y :: Name
y = Name -> Name -> Map Name Name -> Name
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Name
x Name
x (Env -> Map Name Name
tyNameMap Env
env)
      TRec fs :: [(Ident, Type)]
fs       -> [(Ident, Type)] -> Type
TRec [ (Ident
f, Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env Type
t) | (f :: Ident
f,t :: Type
t) <- [(Ident, Type)]
fs ]

instance Inst TCon where
  inst :: Env -> TCon -> TCon
inst env :: Env
env tc :: TCon
tc =
    case TCon
tc of
      TC x :: TC
x -> TC -> TCon
TC (Env -> TC -> TC
forall t. Inst t => Env -> t -> t
inst Env
env TC
x)
      _    -> TCon
tc

instance Inst TC where
  inst :: Env -> TC -> TC
inst env :: Env
env tc :: TC
tc =
    case TC
tc of
      TCNewtype x :: UserTC
x  -> UserTC -> TC
TCNewtype (Env -> UserTC -> UserTC
forall t. Inst t => Env -> t -> t
inst Env
env UserTC
x)
      TCAbstract x :: UserTC
x -> UserTC -> TC
TCAbstract (Env -> UserTC -> UserTC
forall t. Inst t => Env -> t -> t
inst Env
env UserTC
x)
      _            -> TC
tc

instance Inst UserTC where
  inst :: Env -> UserTC -> UserTC
inst env :: Env
env (UserTC x :: Name
x t :: Kind
t) = Name -> Kind -> UserTC
UserTC Name
y Kind
t
    where y :: Name
y = Name -> Name -> Map Name Name -> Name
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Name
x Name
x (Env -> Map Name Name
tyNameMap Env
env)

instance Inst (ExportSpec Name) where
  inst :: Env -> ExportSpec Name -> ExportSpec Name
inst env :: Env
env es :: ExportSpec Name
es = ExportSpec :: forall name. Set name -> Set name -> ExportSpec name
ExportSpec { eTypes :: Set Name
eTypes = (Name -> Name) -> Set Name -> Set Name
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Name -> Name
instT (ExportSpec Name -> Set Name
forall name. ExportSpec name -> Set name
eTypes ExportSpec Name
es)
                           , eBinds :: Set Name
eBinds = (Name -> Name) -> Set Name -> Set Name
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Name -> Name
instV (ExportSpec Name -> Set Name
forall name. ExportSpec name -> Set name
eBinds ExportSpec Name
es)
                           }
    where instT :: Name -> Name
instT x :: Name
x = Name -> Name -> Map Name Name -> Name
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Name
x Name
x (Env -> Map Name Name
tyNameMap Env
env)
          instV :: Name -> Name
instV x :: Name
x = Name -> Name -> Map Name Name -> Name
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Name
x Name
x (Env -> Map Name Name
funNameMap Env
env)

instance Inst TySyn where
  inst :: Env -> TySyn -> TySyn
inst env :: Env
env ts :: TySyn
ts = $WTySyn :: Name -> [TParam] -> [Type] -> Type -> Maybe String -> TySyn
TySyn { tsName :: Name
tsName = Env -> Name -> Name
instTyName Env
env Name
x
                      , tsParams :: [TParam]
tsParams = TySyn -> [TParam]
tsParams TySyn
ts
                      , tsConstraints :: [Type]
tsConstraints = Env -> [Type] -> [Type]
forall t. Inst t => Env -> t -> t
inst Env
env (TySyn -> [Type]
tsConstraints TySyn
ts)
                      , tsDef :: Type
tsDef = Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env (TySyn -> Type
tsDef TySyn
ts)
                      , tsDoc :: Maybe String
tsDoc = TySyn -> Maybe String
tsDoc TySyn
ts
                      }
    where x :: Name
x = TySyn -> Name
tsName TySyn
ts

instance Inst Newtype where
  inst :: Env -> Newtype -> Newtype
inst env :: Env
env nt :: Newtype
nt = Newtype :: Name
-> [TParam] -> [Type] -> [(Ident, Type)] -> Maybe String -> Newtype
Newtype { ntName :: Name
ntName = Env -> Name -> Name
instTyName Env
env Name
x
                        , ntParams :: [TParam]
ntParams = Newtype -> [TParam]
ntParams Newtype
nt
                        , ntConstraints :: [Type]
ntConstraints = Env -> [Type] -> [Type]
forall t. Inst t => Env -> t -> t
inst Env
env (Newtype -> [Type]
ntConstraints Newtype
nt)
                        , ntFields :: [(Ident, Type)]
ntFields = [ (Ident
f,Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env Type
t) | (f :: Ident
f,t :: Type
t) <- Newtype -> [(Ident, Type)]
ntFields Newtype
nt ]
                        , ntDoc :: Maybe String
ntDoc = Newtype -> Maybe String
ntDoc Newtype
nt
                        }
    where x :: Name
x = Newtype -> Name
ntName Newtype
nt

instance Inst AbstractType where
  inst :: Env -> AbstractType -> AbstractType
inst env :: Env
env a :: AbstractType
a = AbstractType :: Name
-> Kind
-> ([TParam], [Type])
-> Maybe Fixity
-> Maybe String
-> AbstractType
AbstractType { atName :: Name
atName    = Env -> Name -> Name
instTyName Env
env (AbstractType -> Name
atName AbstractType
a)
                            , atKind :: Kind
atKind    = AbstractType -> Kind
atKind AbstractType
a
                            , atCtrs :: ([TParam], [Type])
atCtrs    = case AbstractType -> ([TParam], [Type])
atCtrs AbstractType
a of
                                            (xs :: [TParam]
xs,ps :: [Type]
ps) -> ([TParam]
xs, Env -> [Type] -> [Type]
forall t. Inst t => Env -> t -> t
inst Env
env [Type]
ps)
                            , atFixitiy :: Maybe Fixity
atFixitiy = AbstractType -> Maybe Fixity
atFixitiy AbstractType
a
                            , atDoc :: Maybe String
atDoc     = AbstractType -> Maybe String
atDoc AbstractType
a
                            }

instTyName :: Env -> Name -> Name
instTyName :: Env -> Name -> Name
instTyName env :: Env
env x :: Name
x = Name -> Name -> Map Name Name -> Name
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Name
x Name
x (Env -> Map Name Name
tyNameMap Env
env)