{-# 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 = forall t. TraverseNames t => (Name -> Name) -> t -> t
mapNames (\Name
x -> forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Name
x Name
x ?vSu::Map Name Name
?vSu)

-- | Has types but not values.
doTInst :: (Su, TVars a) => a -> a
doTInst :: forall a. (Su, TVars a) => a -> a
doTInst = forall t. TVars t => Subst -> t -> t
apSubst ?tSu::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 = forall t. TVars t => Subst -> t -> t
apSubst ?tSu::Subst
?tSu forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 =
  forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (forall t. (ModuleInstance t, Su) => t -> t
moduleInstance Name
x, forall t. (ModuleInstance t, Su) => t -> t
moduleInstance a
d) | (Name
x,a
d) <- 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 = forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall t. (ModuleInstance t, Su) => t -> t
moduleInstance forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a b. (a -> b) -> [a] -> [b]
map 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 = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located a
l

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

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

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

instance ModuleInstance TySyn where
  moduleInstance :: Su => TySyn -> TySyn
moduleInstance TySyn
ts =
    TySyn { tsName :: Name
tsName        = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (TySyn -> Name
tsName TySyn
ts)
          , tsParams :: [TParam]
tsParams      = TySyn -> [TParam]
tsParams TySyn
ts
          , tsConstraints :: [Prop]
tsConstraints = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (TySyn -> [Prop]
tsConstraints TySyn
ts)
          , tsDef :: Prop
tsDef         = 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        = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (Newtype -> Name
ntName Newtype
nt)
            , ntParams :: [TParam]
ntParams      = Newtype -> [TParam]
ntParams Newtype
nt
            , ntConstraints :: [Prop]
ntConstraints = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (Newtype -> [Prop]
ntConstraints Newtype
nt)
            , ntConName :: Name
ntConName     = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (Newtype -> Name
ntConName Newtype
nt)
            , ntFields :: RecordMap Ident Prop
ntFields      = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance 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     = 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, 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 (forall t. (ModuleInstance t, Su) => t -> t
moduleInstance [Decl]
ds)
      NonRecursive Decl
d -> Decl -> DeclGroup
NonRecursive (forall t. (ModuleInstance t, Su) => t -> t
moduleInstance Decl
d)

instance ModuleInstance Decl where
  moduleInstance :: Su => Decl -> Decl
moduleInstance = 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     = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (forall name. IfaceNames name -> name
ifsName IfaceNames name
ns)
               , ifsNested :: Set Name
ifsNested   = Su => Set Name -> Set Name
doSet (forall name. IfaceNames name -> Set Name
ifsNested IfaceNames name
ns)
               , ifsDefines :: Set Name
ifsDefines  = Su => Set Name -> Set Name
doSet (forall name. IfaceNames name -> Set Name
ifsDefines IfaceNames name
ns)
               , ifsPublic :: Set Name
ifsPublic   = Su => Set Name -> Set Name
doSet (forall name. IfaceNames name -> Set Name
ifsPublic IfaceNames name
ns)
               , ifsDoc :: Maybe Text
ifsDoc      = 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       = forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
si)
                  , mpnConstraints :: [Located Prop]
mpnConstraints = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (ModParamNames -> [Located Prop]
mpnConstraints ModParamNames
si)
                  , mpnFuns :: Map Name ModVParam
mpnFuns        = forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
si)
                  , mpnTySyn :: Map Name TySyn
mpnTySyn       = 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 = 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   = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (ModVParam -> Name
mvpName ModVParam
mp)
              , mvpType :: Schema
mvpType   = 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       = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (ModParam -> ImpName Name
mpIface ModParam
p)
             , mpParameters :: ModParamNames
mpParameters  = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (ModParam -> ModParamNames
mpParameters ModParam
p)
             , mpQual :: Maybe ModName
mpQual        = ModParam -> Maybe ModName
mpQual ModParam
p
             }