    {-# Language ImplicitParams, ConstraintKinds #-}
    module Cryptol.TypeCheck.ModuleInstance where

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

    import Cryptol.Parser.Position(Located)
    import Cryptol.ModuleSystem.Interface(IfaceNames(..))
    import Cryptol.IR.TraverseNames(TraverseNames,mapNames)
    import Cryptol.TypeCheck.AST
    import Cryptol.TypeCheck.Subst(Subst,TVars,apSubst)

    {- | `?tSu` should be applied to all types.
         `?vSu` shoudl be applied to all values. -}
    type Su = (?tSu :: Subst, ?vSu :: Map Name Name)

    -- | Has value names but no types.
    doVInst :: (Su, TraverseNames a) => a -> a
    doVInst :: forall a. (Su, TraverseNames a) => a -> a
    doVInst = (Name -> Name) -> a -> a
    forall t. TraverseNames t => (Name -> Name) -> t -> t
    mapNames (\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 ?vSu::Map Name Name
    Map Name Name
    ?vSu)

    -- | Has types but not values.
    doTInst :: (Su, TVars a) => a -> a
    doTInst :: forall a. (Su, TVars a) => a -> a
    doTInst = Subst -> a -> a
    forall t. TVars t => Subst -> t -> t
    apSubst ?tSu::Subst
    Subst
    ?tSu

    -- | Has both value names and types.
    doTVInst :: (Su, TVars a, TraverseNames a) => a -> a
    doTVInst :: forall a. (Su, TVars a, TraverseNames a) => a -> a
    doTVInst = Subst -> a -> a
    forall t. TVars t => Subst -> t -> t
    apSubst ?tSu::Subst
    Subst
    ?tSu (a -> a) -> (a -> a) -> a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> a
    forall a. (Su, TraverseNames a) => a -> a
    doVInst

    doMap :: (Su, ModuleInstance a) => Map Name a -> Map Name a
    doMap :: forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
    doMap Map Name a
    mp =
      [(Name, a)] -> Map Name a
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [ (Name -> Name
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance Name
    x, a -> a
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance a
    d) | (Name
    x,a
    d) <- Map Name a -> [(Name, a)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map Name a
    mp ]

    doSet :: Su => Set Name -> Set Name
    doSet :: Su => Set Name -> Set Name
    doSet = [Name] -> Set Name
    forall a. Ord a => [a] -> Set a
    Set.fromList ([Name] -> Set Name)
    -> (Set Name -> [Name]) -> Set Name -> Set Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name -> Name) -> [Name] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Name
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance ([Name] -> [Name]) -> (Set Name -> [Name]) -> Set Name -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set Name -> [Name]
    forall a. Set a -> [a]
    Set.toList

    class ModuleInstance t where
      moduleInstance :: Su => t -> t

    instance ModuleInstance a => ModuleInstance [a] where
      moduleInstance :: Su => [a] -> [a]
    moduleInstance = (a -> a) -> [a] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> a
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance

    instance ModuleInstance a => ModuleInstance (Located a) where
      moduleInstance :: Su => Located a -> Located a
    moduleInstance Located a
    l = a -> a
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (a -> a) -> Located a -> Located a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Located a
    l

    instance ModuleInstance Name where
      moduleInstance :: Su => Name -> Name
    moduleInstance = Name -> Name
    forall a. (Su, TraverseNames a) => a -> a
    doVInst

    instance ModuleInstance name => ModuleInstance (ImpName name) where
      moduleInstance :: Su => ImpName name -> ImpName name
    moduleInstance ImpName name
    x =
        case ImpName name
    x of
          ImpTop ModName
    t -> ModName -> ImpName name
    forall name. ModName -> ImpName name
    ImpTop ModName
    t
          ImpNested name
    n -> name -> ImpName name
    forall name. name -> ImpName name
    ImpNested (name -> name
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance name
    n)

    instance ModuleInstance (ModuleG name) where
      moduleInstance :: Su => ModuleG name -> ModuleG name
    moduleInstance ModuleG name
    m =
        Module { mName :: name
    mName             = ModuleG name -> name
    forall mname. ModuleG mname -> mname
    mName ModuleG name
    m
               , mDoc :: Maybe Text
    mDoc              = Maybe Text
    forall a. Maybe a
    Nothing
               , mExports :: ExportSpec Name
    mExports          = ExportSpec Name -> ExportSpec Name
    forall a. (Su, TraverseNames a) => a -> a
    doVInst (ModuleG name -> ExportSpec Name
    forall mname. ModuleG mname -> ExportSpec Name
    mExports ModuleG name
    m)
               , mParamTypes :: Map Name ModTParam
    mParamTypes       = Map Name ModTParam -> Map Name ModTParam
    forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
    doMap (ModuleG name -> Map Name ModTParam
    forall mname. ModuleG mname -> Map Name ModTParam
    mParamTypes ModuleG name
    m)
               , mParamFuns :: Map Name ModVParam
    mParamFuns        = Map Name ModVParam -> Map Name ModVParam
    forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
    doMap (ModuleG name -> Map Name ModVParam
    forall mname. ModuleG mname -> Map Name ModVParam
    mParamFuns ModuleG name
    m)
               , mParamConstraints :: [Located Prop]
    mParamConstraints = [Located Prop] -> [Located Prop]
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (ModuleG name -> [Located Prop]
    forall mname. ModuleG mname -> [Located Prop]
    mParamConstraints ModuleG name
    m)
               , mParams :: FunctorParams
    mParams           = ModParam -> ModParam
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (ModParam -> ModParam) -> FunctorParams -> FunctorParams
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleG name -> FunctorParams
    forall mname. ModuleG mname -> FunctorParams
    mParams ModuleG name
    m
               , mFunctors :: Map Name (ModuleG Name)
    mFunctors         = Map Name (ModuleG Name) -> Map Name (ModuleG Name)
    forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
    doMap (ModuleG name -> Map Name (ModuleG Name)
    forall mname. ModuleG mname -> Map Name (ModuleG Name)
    mFunctors ModuleG name
    m)
               , mNested :: Set Name
    mNested           = Su => Set Name -> Set Name
    Set Name -> Set Name
    doSet (ModuleG name -> Set Name
    forall mname. ModuleG mname -> Set Name
    mNested ModuleG name
    m)
               , mTySyns :: Map Name TySyn
    mTySyns           = Map Name TySyn -> Map Name TySyn
    forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
    doMap (ModuleG name -> Map Name TySyn
    forall mname. ModuleG mname -> Map Name TySyn
    mTySyns ModuleG name
    m)
               , mNewtypes :: Map Name Newtype
    mNewtypes         = Map Name Newtype -> Map Name Newtype
    forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
    doMap (ModuleG name -> Map Name Newtype
    forall mname. ModuleG mname -> Map Name Newtype
    mNewtypes ModuleG name
    m)
               , mPrimTypes :: Map Name AbstractType
    mPrimTypes        = Map Name AbstractType -> Map Name AbstractType
    forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
    doMap (ModuleG name -> Map Name AbstractType
    forall mname. ModuleG mname -> Map Name AbstractType
    mPrimTypes ModuleG name
    m)
               , mDecls :: [DeclGroup]
    mDecls            = [DeclGroup] -> [DeclGroup]
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (ModuleG name -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls ModuleG name
    m)
               , mSubmodules :: Map Name (IfaceNames Name)
    mSubmodules       = Map Name (IfaceNames Name) -> Map Name (IfaceNames Name)
    forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
    doMap (ModuleG name -> Map Name (IfaceNames Name)
    forall mname. ModuleG mname -> Map Name (IfaceNames Name)
    mSubmodules ModuleG name
    m)
               , mSignatures :: Map Name ModParamNames
    mSignatures       = Map Name ModParamNames -> Map Name ModParamNames
    forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
    doMap (ModuleG name -> Map Name ModParamNames
    forall mname. ModuleG mname -> Map Name ModParamNames
    mSignatures ModuleG name
    m)
               }

    instance ModuleInstance Type where
      moduleInstance :: Su => Prop -> Prop
    moduleInstance = Prop -> Prop
    forall a. (Su, TVars a) => a -> a
    doTInst

    instance ModuleInstance Schema where
      moduleInstance :: Su => Schema -> Schema
    moduleInstance = Schema -> Schema
    forall a. (Su, TVars a) => a -> a
    doTInst

    instance ModuleInstance TySyn where
      moduleInstance :: Su => TySyn -> TySyn
    moduleInstance TySyn
    ts =
        TySyn { tsName :: Name
    tsName        = Name -> Name
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (TySyn -> Name
    tsName TySyn
    ts)
              , tsParams :: [TParam]
    tsParams      = TySyn -> [TParam]
    tsParams TySyn
    ts
              , tsConstraints :: [Prop]
    tsConstraints = [Prop] -> [Prop]
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (TySyn -> [Prop]
    tsConstraints TySyn
    ts)
              , tsDef :: Prop
    tsDef         = Prop -> Prop
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (TySyn -> Prop
    tsDef TySyn
    ts)
              , tsDoc :: Maybe Text
    tsDoc         = TySyn -> Maybe Text
    tsDoc TySyn
    ts
              }

    instance ModuleInstance Newtype where
      moduleInstance :: Su => Newtype -> Newtype
    moduleInstance Newtype
    nt =
        Newtype { ntName :: Name
    ntName        = Name -> Name
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (Newtype -> Name
    ntName Newtype
    nt)
                , ntParams :: [TParam]
    ntParams      = Newtype -> [TParam]
    ntParams Newtype
    nt
                , ntConstraints :: [Prop]
    ntConstraints = [Prop] -> [Prop]
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (Newtype -> [Prop]
    ntConstraints Newtype
    nt)
                , ntConName :: Name
    ntConName     = Name -> Name
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (Newtype -> Name
    ntConName Newtype
    nt)
                , ntFields :: RecordMap Ident Prop
    ntFields      = Prop -> Prop
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (Prop -> Prop) -> RecordMap Ident Prop -> RecordMap Ident Prop
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Newtype -> RecordMap Ident Prop
    ntFields Newtype
    nt
                , ntDoc :: Maybe Text
    ntDoc         = Newtype -> Maybe Text
    ntDoc Newtype
    nt
                }

    instance ModuleInstance AbstractType where
      moduleInstance :: Su => AbstractType -> AbstractType
    moduleInstance AbstractType
    at =
        AbstractType { atName :: Name
    atName     = Name -> Name
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (AbstractType -> Name
    atName AbstractType
    at)
                     , atKind :: Kind
    atKind     = AbstractType -> Kind
    atKind AbstractType
    at
                     , atCtrs :: ([TParam], [Prop])
    atCtrs     = let ([TParam]
    ps,[Prop]
    cs) = AbstractType -> ([TParam], [Prop])
    atCtrs AbstractType
    at
                                    in ([TParam]
    ps, [Prop] -> [Prop]
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance [Prop]
    cs)
                     , atFixitiy :: Maybe Fixity
    atFixitiy  = AbstractType -> Maybe Fixity
    atFixitiy AbstractType
    at
                     , atDoc :: Maybe Text
    atDoc      = AbstractType -> Maybe Text
    atDoc AbstractType
    at
                     }

    instance ModuleInstance DeclGroup where
      moduleInstance :: Su => DeclGroup -> DeclGroup
    moduleInstance DeclGroup
    dg =
        case DeclGroup
    dg of
          Recursive [Decl]
    ds    -> [Decl] -> DeclGroup
    Recursive ([Decl] -> [Decl]
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance [Decl]
    ds)
          NonRecursive Decl
    d -> Decl -> DeclGroup
    NonRecursive (Decl -> Decl
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance Decl
    d)

    instance ModuleInstance Decl where
      moduleInstance :: Su => Decl -> Decl
    moduleInstance = Decl -> Decl
    forall a. (Su, TVars a, TraverseNames a) => a -> a
    doTVInst

    instance ModuleInstance name => ModuleInstance (IfaceNames name) where
      moduleInstance :: Su => IfaceNames name -> IfaceNames name
    moduleInstance IfaceNames name
    ns =
        IfaceNames { ifsName :: name
    ifsName     = name -> name
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (IfaceNames name -> name
    forall name. IfaceNames name -> name
    ifsName IfaceNames name
    ns)
                   , ifsNested :: Set Name
    ifsNested   = Su => Set Name -> Set Name
    Set Name -> Set Name
    doSet (IfaceNames name -> Set Name
    forall name. IfaceNames name -> Set Name
    ifsNested IfaceNames name
    ns)
                   , ifsDefines :: Set Name
    ifsDefines  = Su => Set Name -> Set Name
    Set Name -> Set Name
    doSet (IfaceNames name -> Set Name
    forall name. IfaceNames name -> Set Name
    ifsDefines IfaceNames name
    ns)
                   , ifsPublic :: Set Name
    ifsPublic   = Su => Set Name -> Set Name
    Set Name -> Set Name
    doSet (IfaceNames name -> Set Name
    forall name. IfaceNames name -> Set Name
    ifsPublic IfaceNames name
    ns)
                   , ifsDoc :: Maybe Text
    ifsDoc      = IfaceNames name -> Maybe Text
    forall name. IfaceNames name -> Maybe Text
    ifsDoc IfaceNames name
    ns
                   }

    instance ModuleInstance ModParamNames where
      moduleInstance :: Su => ModParamNames -> ModParamNames
    moduleInstance ModParamNames
    si =
        ModParamNames { mpnTypes :: Map Name ModTParam
    mpnTypes       = Map Name ModTParam -> Map Name ModTParam
    forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
    doMap (ModParamNames -> Map Name ModTParam
    mpnTypes ModParamNames
    si)
                      , mpnConstraints :: [Located Prop]
    mpnConstraints = [Located Prop] -> [Located Prop]
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (ModParamNames -> [Located Prop]
    mpnConstraints ModParamNames
    si)
                      , mpnFuns :: Map Name ModVParam
    mpnFuns        = Map Name ModVParam -> Map Name ModVParam
    forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
    doMap (ModParamNames -> Map Name ModVParam
    mpnFuns ModParamNames
    si)
                      , mpnTySyn :: Map Name TySyn
    mpnTySyn       = Map Name TySyn -> Map Name TySyn
    forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
    doMap (ModParamNames -> Map Name TySyn
    mpnTySyn ModParamNames
    si)
                      , mpnDoc :: Maybe Text
    mpnDoc         = ModParamNames -> Maybe Text
    mpnDoc ModParamNames
    si
                      }

    instance ModuleInstance ModTParam where
      moduleInstance :: Su => ModTParam -> ModTParam
    moduleInstance ModTParam
    mp =
        ModTParam { mtpName :: Name
    mtpName = Name -> Name
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (ModTParam -> Name
    mtpName ModTParam
    mp)
                  , mtpKind :: Kind
    mtpKind = ModTParam -> Kind
    mtpKind ModTParam
    mp
                  , mtpDoc :: Maybe Text
    mtpDoc  = ModTParam -> Maybe Text
    mtpDoc ModTParam
    mp
                  }

    instance ModuleInstance ModVParam where
      moduleInstance :: Su => ModVParam -> ModVParam
    moduleInstance ModVParam
    mp =
        ModVParam { mvpName :: Name
    mvpName   = Name -> Name
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (ModVParam -> Name
    mvpName ModVParam
    mp)
                  , mvpType :: Schema
    mvpType   = Schema -> Schema
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (ModVParam -> Schema
    mvpType ModVParam
    mp)
                  , mvpDoc :: Maybe Text
    mvpDoc    = ModVParam -> Maybe Text
    mvpDoc ModVParam
    mp
                  , mvpFixity :: Maybe Fixity
    mvpFixity = ModVParam -> Maybe Fixity
    mvpFixity ModVParam
    mp
                  }

    instance ModuleInstance ModParam where
      moduleInstance :: Su => ModParam -> ModParam
    moduleInstance ModParam
    p =
        ModParam { mpName :: Ident
    mpName        = ModParam -> Ident
    mpName ModParam
    p
                 , mpIface :: ImpName Name
    mpIface       = ImpName Name -> ImpName Name
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (ModParam -> ImpName Name
    mpIface ModParam
    p)
                 , mpParameters :: ModParamNames
    mpParameters  = ModParamNames -> ModParamNames
    forall t. (ModuleInstance t, Su) => t -> t
    moduleInstance (ModParam -> ModParamNames
    mpParameters ModParam
    p)
                 , mpQual :: Maybe ModName
    mpQual        = ModParam -> Maybe ModName
    mpQual ModParam
    p
                 }