{-# LANGUAGE Safe #-}

module Cryptol.TypeCheck.Interface where

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

import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Exports(allExported)
import Cryptol.TypeCheck.AST


-- | Information about a declaration to be stored an in interface.
mkIfaceDecl :: Decl -> IfaceDecl
mkIfaceDecl :: Decl -> IfaceDecl
mkIfaceDecl Decl
d = IfaceDecl
  { ifDeclName :: Name
ifDeclName    = Decl -> Name
dName Decl
d
  , ifDeclSig :: Schema
ifDeclSig     = Decl -> Schema
dSignature Decl
d
  , ifDeclIsPrim :: Bool
ifDeclIsPrim  = case Decl -> DeclDef
dDefinition Decl
d of
                      DPrim {} -> Bool
True
                      DeclDef
_        -> Bool
False
  , ifDeclPragmas :: [Pragma]
ifDeclPragmas = Decl -> [Pragma]
dPragmas Decl
d
  , ifDeclInfix :: Bool
ifDeclInfix   = Decl -> Bool
dInfix Decl
d
  , ifDeclFixity :: Maybe Fixity
ifDeclFixity  = Decl -> Maybe Fixity
dFixity Decl
d
  , ifDeclDoc :: Maybe Text
ifDeclDoc     = Decl -> Maybe Text
dDoc Decl
d
  }

-- | Compute information about the names in a module.
genIfaceNames :: ModuleG name -> IfaceNames name
genIfaceNames :: forall name. ModuleG name -> IfaceNames name
genIfaceNames ModuleG name
m = IfaceNames
  { ifsName :: name
ifsName     = ModuleG name -> name
forall mname. ModuleG mname -> mname
mName ModuleG name
m
  , ifsNested :: Set Name
ifsNested   = ModuleG name -> Set Name
forall mname. ModuleG mname -> Set Name
mNested ModuleG name
m
  , ifsDefines :: Set Name
ifsDefines  = ModuleG name -> Set Name
forall mname. ModuleG mname -> Set Name
genModDefines ModuleG name
m
  , ifsPublic :: Set Name
ifsPublic   = ExportSpec Name -> Set Name
forall name. Ord name => ExportSpec name -> Set name
allExported (ModuleG name -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG name
m)
  , ifsDoc :: [Text]
ifsDoc      = ModuleG name -> [Text]
forall mname. ModuleG mname -> [Text]
mDoc ModuleG name
m
  }

-- | Things defines by a module
genModDefines :: ModuleG name -> Set Name
genModDefines :: forall mname. ModuleG mname -> Set Name
genModDefines ModuleG name
m =
  [Set Name] -> Set Name
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
    [ Map Name TySyn -> Set Name
forall k a. Map k a -> Set k
Map.keysSet  (ModuleG name -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG name
m)
    , Map Name NominalType -> Set Name
forall k a. Map k a -> Set k
Map.keysSet  (ModuleG name -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes ModuleG name
m)
    , [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList ((NominalType -> [Name]) -> [NominalType] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (((Name, Schema) -> Name) -> [(Name, Schema)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Schema) -> Name
forall a b. (a, b) -> a
fst ([(Name, Schema)] -> [Name])
-> (NominalType -> [(Name, Schema)]) -> NominalType -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NominalType -> [(Name, Schema)]
nominalTypeConTypes)
                              (Map Name NominalType -> [NominalType]
forall k a. Map k a -> [a]
Map.elems (ModuleG name -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes ModuleG name
m)))
    , [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList ((Decl -> Name) -> [Decl] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> Name
dName ((DeclGroup -> [Decl]) -> [DeclGroup] -> [Decl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DeclGroup -> [Decl]
groupDecls (ModuleG name -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG name
m)))
    , Map Name Submodule -> Set Name
forall k a. Map k a -> Set k
Map.keysSet  (ModuleG name -> Map Name Submodule
forall mname. ModuleG mname -> Map Name Submodule
mSubmodules ModuleG name
m)
    , Map Name (ModuleG Name) -> Set Name
forall k a. Map k a -> Set k
Map.keysSet  (ModuleG name -> Map Name (ModuleG Name)
forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG name
m)
    , Map Name ModParamNames -> Set Name
forall k a. Map k a -> Set k
Map.keysSet  (ModuleG name -> Map Name ModParamNames
forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures ModuleG name
m)
    ] Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set Name -> Set Name
nestedInSet (ModuleG name -> Set Name
forall mname. ModuleG mname -> Set Name
mNested ModuleG name
m)
  where
  nestedInSet :: Set Name -> Set Name
nestedInSet = [Set Name] -> Set Name
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Name] -> Set Name)
-> (Set Name -> [Set Name]) -> Set Name -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Set Name) -> [Name] -> [Set Name]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Set Name
inNested ([Name] -> [Set Name])
-> (Set Name -> [Name]) -> Set Name -> [Set Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Name -> [Name]
forall a. Set a -> [a]
Set.toList
  inNested :: Name -> Set Name
inNested Name
x  = case Name -> Map Name Submodule -> Maybe Submodule
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (ModuleG name -> Map Name Submodule
forall mname. ModuleG mname -> Map Name Submodule
mSubmodules ModuleG name
m) of
                  Just Submodule
y  -> IfaceNames Name -> Set Name
forall name. IfaceNames name -> Set Name
ifsDefines IfaceNames Name
iface Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Name -> Set Name
nestedInSet (IfaceNames Name -> Set Name
forall name. IfaceNames name -> Set Name
ifsNested IfaceNames Name
iface)
                    where iface :: IfaceNames Name
iface = Submodule -> IfaceNames Name
smIface Submodule
y
                  Maybe Submodule
Nothing -> Set Name
forall a. Set a
Set.empty -- must be signature or a functor

genIface :: ModuleG name -> IfaceG name
genIface :: forall name. ModuleG name -> IfaceG name
genIface ModuleG name
m = IfaceNames name -> ModuleG name -> IfaceG name
forall name ignored.
IfaceNames name -> ModuleG ignored -> IfaceG name
genIfaceWithNames (ModuleG name -> IfaceNames name
forall name. ModuleG name -> IfaceNames name
genIfaceNames ModuleG name
m) ModuleG name
m

-- | Generate an Iface from a typechecked module.
genIfaceWithNames :: IfaceNames name -> ModuleG ignored -> IfaceG name
genIfaceWithNames :: forall name ignored.
IfaceNames name -> ModuleG ignored -> IfaceG name
genIfaceWithNames IfaceNames name
names ModuleG ignored
m =
  Iface
  { ifNames :: IfaceNames name
ifNames       = IfaceNames name
names

  , ifDefines :: IfaceDecls
ifDefines = IfaceDecls
    { ifTySyns :: Map Name TySyn
ifTySyns          = ModuleG ignored -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ignored
m
    , ifNominalTypes :: Map Name NominalType
ifNominalTypes    = ModuleG ignored -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes ModuleG ignored
m
    , ifDecls :: Map Name IfaceDecl
ifDecls           = [(Name, IfaceDecl)] -> Map Name IfaceDecl
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name
qn,Decl -> IfaceDecl
mkIfaceDecl Decl
d)
                                       | DeclGroup
dg <- ModuleG ignored -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ignored
m
                                       , Decl
d  <- DeclGroup -> [Decl]
groupDecls DeclGroup
dg
                                       , let qn :: Name
qn = Decl -> Name
dName Decl
d
                                       ]
    , ifModules :: Map Name (IfaceNames Name)
ifModules         = Submodule -> IfaceNames Name
smIface (Submodule -> IfaceNames Name)
-> Map Name Submodule -> Map Name (IfaceNames Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleG ignored -> Map Name Submodule
forall mname. ModuleG mname -> Map Name Submodule
mSubmodules ModuleG ignored
m
    , ifSignatures :: Map Name ModParamNames
ifSignatures      = ModuleG ignored -> Map Name ModParamNames
forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures ModuleG ignored
m
    , ifFunctors :: Map Name (IfaceG Name)
ifFunctors        = ModuleG Name -> IfaceG Name
forall name. ModuleG name -> IfaceG name
genIface (ModuleG Name -> IfaceG Name)
-> Map Name (ModuleG Name) -> Map Name (IfaceG Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleG ignored -> Map Name (ModuleG Name)
forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG ignored
m
    }

  , ifParams :: FunctorParams
ifParams = ModuleG ignored -> FunctorParams
forall mname. ModuleG mname -> FunctorParams
mParams ModuleG ignored
m
  }