{-# 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
             }