{-# 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     = forall mname. ModuleG mname -> mname
mName ModuleG name
m
  , ifsNested :: Set Name
ifsNested   = forall mname. ModuleG mname -> Set Name
mNested ModuleG name
m
  , ifsDefines :: Set Name
ifsDefines  = forall mname. ModuleG mname -> Set Name
genModDefines ModuleG name
m
  , ifsPublic :: Set Name
ifsPublic   = forall name. Ord name => ExportSpec name -> Set name
allExported (forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG name
m)
  , ifsDoc :: Maybe Text
ifsDoc      = forall mname. ModuleG mname -> Maybe 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 =
  forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
    [ forall k a. Map k a -> Set k
Map.keysSet  (forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG name
m)
    , forall k a. Map k a -> Set k
Map.keysSet  (forall mname. ModuleG mname -> Map Name Newtype
mNewtypes ModuleG name
m)
    , forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map Newtype -> Name
ntConName (forall k a. Map k a -> [a]
Map.elems (forall mname. ModuleG mname -> Map Name Newtype
mNewtypes ModuleG name
m)))
    , forall k a. Map k a -> Set k
Map.keysSet  (forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes ModuleG name
m)
    , forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map Decl -> Name
dName (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DeclGroup -> [Decl]
groupDecls (forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG name
m)))
    , forall k a. Map k a -> Set k
Map.keysSet  (forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules ModuleG name
m)
    , forall k a. Map k a -> Set k
Map.keysSet  (forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG name
m)
    , forall k a. Map k a -> Set k
Map.keysSet  (forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures ModuleG name
m)
    ] forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set Name -> Set Name
nestedInSet (forall mname. ModuleG mname -> Set Name
mNested ModuleG name
m)
  where
  nestedInSet :: Set Name -> Set Name
nestedInSet = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Name -> Set Name
inNested forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList
  inNested :: Name -> Set Name
inNested Name
x  = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules ModuleG name
m) of
                  Just IfaceNames Name
y  -> forall name. IfaceNames name -> Set Name
ifsDefines IfaceNames Name
y forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Name -> Set Name
nestedInSet (forall name. IfaceNames name -> Set Name
ifsNested IfaceNames Name
y)
                  Maybe (IfaceNames Name)
Nothing -> 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 = forall name ignored.
IfaceNames name -> ModuleG ignored -> IfaceG name
genIfaceWithNames (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          = forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ignored
m
    , ifNewtypes :: Map Name Newtype
ifNewtypes        = forall mname. ModuleG mname -> Map Name Newtype
mNewtypes ModuleG ignored
m
    , ifAbstractTypes :: Map Name AbstractType
ifAbstractTypes   = forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes ModuleG ignored
m
    , ifDecls :: Map Name IfaceDecl
ifDecls           = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name
qn,Decl -> IfaceDecl
mkIfaceDecl Decl
d)
                                       | DeclGroup
dg <- 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         = forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules ModuleG ignored
m
    , ifSignatures :: Map Name ModParamNames
ifSignatures      = forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures ModuleG ignored
m
    , ifFunctors :: Map Name (IfaceG Name)
ifFunctors        = forall name. ModuleG name -> IfaceG name
genIface forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG ignored
m
    }

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