{-# 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.ModuleSystem.NamingEnv(NamingEnv,mapNamingEnv)
import Cryptol.IR.TraverseNames(TraverseNames,mapNames)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst(Subst,TVars,apSubst)


{- | `?tVarSu` substitutes 'Type's for 'TVar's which are module type parameters.
     `?nameSu` substitutes fresh 'Name's for the functor's 'Name's
       (in all namespaces). -}
type Su = (?tVarSu :: Subst, ?nameSu :: Map Name Name)

-- | Instantiate something that has 'Name's.
doNameInst :: (Su, TraverseNames a) => a -> a
doNameInst :: forall a. (Su, TraverseNames a) => a -> a
doNameInst = (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 ?nameSu::Map Name Name
Map Name Name
?nameSu)

-- | Instantiate something that has 'TVar's.
doTVarInst :: (Su, TVars a) => a -> a
doTVarInst :: forall a. (Su, TVars a) => a -> a
doTVarInst = Subst -> a -> a
forall t. TVars t => Subst -> t -> t
apSubst ?tVarSu::Subst
Subst
?tVarSu

-- | Instantiate something that has both 'TVar's and 'Name's.
-- Order is important here because '?tVarSu' might insert 'Name's.
doInst :: (Su, TVars a, TraverseNames a) => a -> a
doInst :: forall a. (Su, TVars a, TraverseNames a) => a -> a
doInst = a -> a
forall a. (Su, TraverseNames a) => a -> a
doNameInst (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. (Su, TVars a) => a -> a
doTVarInst

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
doNameInst

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

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 Submodule where
  moduleInstance :: Su => Submodule -> Submodule
moduleInstance Submodule
x = Submodule
    { smInScope :: NamingEnv
smInScope = NamingEnv -> NamingEnv
forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (Submodule -> NamingEnv
smInScope Submodule
x)
    , smIface :: IfaceNames Name
smIface = IfaceNames Name -> IfaceNames Name
forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (Submodule -> IfaceNames Name
smIface Submodule
x)
    }

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 :: [Text]
mDoc              = [Text]
forall a. Monoid a => a
mempty
           , mExports :: ExportSpec Name
mExports          = ExportSpec Name -> ExportSpec Name
forall a. (Su, TraverseNames a) => a -> a
doNameInst (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)
           , mNominalTypes :: Map Name NominalType
mNominalTypes     = Map Name NominalType -> Map Name NominalType
forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (ModuleG name -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes 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 Submodule
mSubmodules       = Map Name Submodule -> Map Name Submodule
forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (ModuleG name -> Map Name Submodule
forall mname. ModuleG mname -> Map Name Submodule
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)
           , mInScope :: NamingEnv
mInScope          = NamingEnv -> NamingEnv
forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (ModuleG name -> NamingEnv
forall mname. ModuleG mname -> NamingEnv
mInScope ModuleG name
m)
           }

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

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

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 NominalType where
  moduleInstance :: Su => NominalType -> NominalType
moduleInstance NominalType
nt =
    NominalType
            { ntName :: Name
ntName        = Name -> Name
forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (NominalType -> Name
ntName NominalType
nt)
            , ntParams :: [TParam]
ntParams      = NominalType -> [TParam]
ntParams NominalType
nt
            , ntKind :: Kind
ntKind        = NominalType -> Kind
ntKind NominalType
nt
            , ntConstraints :: [Prop]
ntConstraints = [Prop] -> [Prop]
forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (NominalType -> [Prop]
ntConstraints NominalType
nt)
            , ntDef :: NominalTypeDef
ntDef         = NominalTypeDef -> NominalTypeDef
forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (NominalType -> NominalTypeDef
ntDef NominalType
nt)
            , ntFixity :: Maybe Fixity
ntFixity      = NominalType -> Maybe Fixity
ntFixity NominalType
nt
            , ntDoc :: Maybe Text
ntDoc         = NominalType -> Maybe Text
ntDoc NominalType
nt
            }

instance ModuleInstance NominalTypeDef where
  moduleInstance :: Su => NominalTypeDef -> NominalTypeDef
moduleInstance NominalTypeDef
def =
    case NominalTypeDef
def of
      Struct StructCon
c -> StructCon -> NominalTypeDef
Struct (StructCon -> StructCon
forall t. (ModuleInstance t, Su) => t -> t
moduleInstance StructCon
c)
      Enum [EnumCon]
cs  -> [EnumCon] -> NominalTypeDef
Enum   ([EnumCon] -> [EnumCon]
forall t. (ModuleInstance t, Su) => t -> t
moduleInstance [EnumCon]
cs)
      NominalTypeDef
Abstract -> NominalTypeDef
Abstract

instance ModuleInstance StructCon where
  moduleInstance :: Su => StructCon -> StructCon
moduleInstance StructCon
c =
    StructCon
      { ntConName :: Name
ntConName     = Name -> Name
forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (StructCon -> Name
ntConName StructCon
c)
      , 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
<$> StructCon -> RecordMap Ident Prop
ntFields StructCon
c
      }

instance ModuleInstance EnumCon where
  moduleInstance :: Su => EnumCon -> EnumCon
moduleInstance EnumCon
c =
    EnumCon
      { ecName :: Name
ecName        = Name -> Name
forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (EnumCon -> Name
ecName EnumCon
c)
      , ecNumber :: Int
ecNumber      = EnumCon -> Int
ecNumber EnumCon
c
      , ecFields :: [Prop]
ecFields      = [Prop] -> [Prop]
forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (EnumCon -> [Prop]
ecFields EnumCon
c)
      , ecPublic :: Bool
ecPublic      = EnumCon -> Bool
ecPublic EnumCon
c
      , ecDoc :: Maybe Text
ecDoc         = EnumCon -> Maybe Text
ecDoc EnumCon
c
      }

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
doInst


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 :: [Text]
ifsDoc      = IfaceNames name -> [Text]
forall name. IfaceNames name -> [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
             }