{-# 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.TypeCheck.AST
import Cryptol.TypeCheck.Subst(listParamSubst, apSubst)
import Cryptol.TypeCheck.SimpType(tRebuild)
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 Module
func ModName
newName Map TParam Type
tpMap 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 a -> Name
f 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
              , Module :: 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 Subst
su Map Name Name
vpNames (Name
x,Expr
e) =
      Decl -> DeclGroup
NonRecursive Decl :: Name
-> Schema
-> DeclDef
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe Text
-> Decl
Decl
        { dName :: Name
dName        = Name -> Name -> Map Name Name -> Name
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Name
forall a. HasCallStack => [Char] -> a
error [Char]
"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 ([Char] -> ModVParam
forall a. HasCallStack => [Char] -> a
error [Char]
"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 Text
dDoc         = Maybe Text
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 DeclGroup
d =
    case DeclGroup
d of
      NonRecursive Decl
x -> Decl -> Set Name
forall t. Defines t => t -> Set Name
defines Decl
x
      Recursive [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 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 ModName
_ NameSource
s -> NameSource
s
                 NameInfo
_            -> 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 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 Module
m Map TParam Type
tpMap 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 (Name
x,b
_) = 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 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 -> [Char]
(Int -> Env -> ShowS)
-> (Env -> [Char]) -> ([Env] -> ShowS) -> Show Env
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Env] -> ShowS
$cshowList :: [Env] -> ShowS
show :: Env -> [Char]
$cshow :: Env -> [Char]
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 = (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 = Expr -> Expr
go
    where
    go :: Expr -> Expr
go Expr
expr =
      case Expr
expr of
        EVar 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 Name
y -> Name -> Expr
EVar Name
y
                    Maybe Name
_      -> Expr
expr

        ELocated Range
r Expr
e              -> Range -> Expr -> Expr
ELocated Range
r (Env -> Expr -> Expr
forall t. Inst t => Env -> t -> t
inst Env
env Expr
e)
        EList [Expr]
xs 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 [Expr]
es                 -> [Expr] -> Expr
ETuple (Env -> [Expr] -> [Expr]
forall t. Inst t => Env -> t -> t
inst Env
env [Expr]
es)
        ERec RecordMap Ident Expr
xs                   -> RecordMap Ident Expr -> Expr
ERec ((Expr -> Expr) -> RecordMap Ident Expr -> RecordMap Ident Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Expr
go RecordMap Ident Expr
xs)
        ESel Expr
e Selector
s                  -> Expr -> Selector -> Expr
ESel (Expr -> Expr
go Expr
e) Selector
s
        ESet Type
ty Expr
e Selector
x Expr
v             -> Type -> Expr -> Selector -> Expr -> Expr
ESet (Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env Type
ty) (Expr -> Expr
go Expr
e) Selector
x (Expr -> Expr
go Expr
v)
        EIf Expr
e1 Expr
e2 Expr
e3              -> Expr -> Expr -> Expr -> Expr
EIf (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2) (Expr -> Expr
go Expr
e3)
        EComp Type
t1 Type
t2 Expr
e [[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 TParam
t Expr
e                 -> TParam -> Expr -> Expr
ETAbs TParam
t (Expr -> Expr
go Expr
e)
        ETApp Expr
e 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 Expr
e1 Expr
e2                -> Expr -> Expr -> Expr
EApp (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
        EAbs Name
x Type
t 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 Type
p 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 Expr
e               -> Expr -> Expr
EProofApp (Expr -> Expr
go Expr
e)
        EWhere Expr
e [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 DeclGroup
dg =
    case DeclGroup
dg of
      NonRecursive Decl
d -> Decl -> DeclGroup
NonRecursive (Env -> Decl -> Decl
forall t. Inst t => Env -> t -> t
inst Env
env Decl
d)
      Recursive [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 DeclDef
d =
    case DeclDef
d of
      DeclDef
DPrim   -> DeclDef
DPrim
      DExpr 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 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 Match
m =
    case Match
m of
      From Name
x Type
t1 Type
t2 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 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 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 Type
ty =
    Type -> Type
tRebuild (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    case Type
ty of
      TCon TCon
tc [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 TVar
tv       ->
        case TVar
tv of
          TVBound TParam
tp | Just 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
          TVar
_ -> Type
ty
      TUser Name
x [Type]
ts 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 RecordMap Ident Type
fs       -> RecordMap Ident Type -> Type
TRec ((Type -> Type) -> RecordMap Ident Type -> RecordMap Ident Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env) RecordMap Ident Type
fs)
      TNewtype Newtype
nt [Type]
ts -> Newtype -> [Type] -> Type
TNewtype (Env -> Newtype -> Newtype
forall t. Inst t => Env -> t -> t
inst Env
env Newtype
nt) (Env -> [Type] -> [Type]
forall t. Inst t => Env -> t -> t
inst Env
env [Type]
ts)

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

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

instance Inst UserTC where
  inst :: Env -> UserTC -> UserTC
inst Env
env (UserTC Name
x 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 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 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 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 TySyn
ts = TySyn :: Name -> [TParam] -> [Type] -> Type -> Maybe Text -> 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 Text
tsDoc = TySyn -> Maybe Text
tsDoc TySyn
ts
                      }
    where x :: Name
x = TySyn -> Name
tsName TySyn
ts

instance Inst Newtype where
  inst :: Env -> Newtype -> Newtype
inst Env
env Newtype
nt = Newtype :: Name
-> [TParam]
-> [Type]
-> RecordMap Ident Type
-> Maybe Text
-> 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 :: RecordMap Ident Type
ntFields = (Type -> Type) -> RecordMap Ident Type -> RecordMap Ident Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> Type -> Type
forall t. Inst t => Env -> t -> t
inst Env
env) (Newtype -> RecordMap Ident Type
ntFields Newtype
nt)
                        , ntDoc :: Maybe Text
ntDoc = Newtype -> Maybe Text
ntDoc Newtype
nt
                        }
    where x :: Name
x = Newtype -> Name
ntName Newtype
nt

instance Inst AbstractType where
  inst :: Env -> AbstractType -> AbstractType
inst Env
env AbstractType
a = AbstractType :: Name
-> Kind
-> ([TParam], [Type])
-> Maybe Fixity
-> Maybe Text
-> 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
                                            ([TParam]
xs,[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 Text
atDoc     = AbstractType -> Maybe Text
atDoc AbstractType
a
                            }

instTyName :: Env -> Name -> Name
instTyName :: Env -> Name -> Name
instTyName Env
env 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)