module Cryptol.TypeCheck.Interface where

import qualified Data.Map as Map

import Cryptol.Utils.Ident(Namespace(..))
import Cryptol.ModuleSystem.Interface
import Cryptol.TypeCheck.AST


mkIfaceDecl :: Decl -> IfaceDecl
mkIfaceDecl :: Decl -> IfaceDecl
mkIfaceDecl Decl
d = IfaceDecl :: Name
-> Schema
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe Text
-> IfaceDecl
IfaceDecl
  { ifDeclName :: Name
ifDeclName    = Decl -> Name
dName Decl
d
  , ifDeclSig :: Schema
ifDeclSig     = Decl -> Schema
dSignature Decl
d
  , 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
  }

-- | Generate an Iface from a typechecked module.
genIface :: ModuleG mname -> IfaceG mname
genIface :: ModuleG mname -> IfaceG mname
genIface ModuleG mname
m = Iface :: forall mname.
mname -> IfaceDecls -> IfaceDecls -> IfaceParams -> IfaceG mname
Iface
  { ifModName :: mname
ifModName = ModuleG mname -> mname
forall mname. ModuleG mname -> mname
mName ModuleG mname
m

  , ifPublic :: IfaceDecls
ifPublic      = IfaceDecls :: Map Name IfaceTySyn
-> Map Name IfaceNewtype
-> Map Name IfaceAbstractType
-> Map Name IfaceDecl
-> Map Name (IfaceG Name)
-> IfaceDecls
IfaceDecls
    { ifTySyns :: Map Name IfaceTySyn
ifTySyns    = Map Name IfaceTySyn
tsPub
    , ifNewtypes :: Map Name IfaceNewtype
ifNewtypes  = Map Name IfaceNewtype
ntPub
    , ifAbstractTypes :: Map Name IfaceAbstractType
ifAbstractTypes = Map Name IfaceAbstractType
atPub
    , ifDecls :: Map Name IfaceDecl
ifDecls     = Map Name IfaceDecl
dPub
    , ifModules :: Map Name (IfaceG Name)
ifModules   = Map Name (IfaceG Name)
mPub
    }

  , ifPrivate :: IfaceDecls
ifPrivate = IfaceDecls :: Map Name IfaceTySyn
-> Map Name IfaceNewtype
-> Map Name IfaceAbstractType
-> Map Name IfaceDecl
-> Map Name (IfaceG Name)
-> IfaceDecls
IfaceDecls
    { ifTySyns :: Map Name IfaceTySyn
ifTySyns    = Map Name IfaceTySyn
tsPriv
    , ifNewtypes :: Map Name IfaceNewtype
ifNewtypes  = Map Name IfaceNewtype
ntPriv
    , ifAbstractTypes :: Map Name IfaceAbstractType
ifAbstractTypes = Map Name IfaceAbstractType
atPriv
    , ifDecls :: Map Name IfaceDecl
ifDecls     = Map Name IfaceDecl
dPriv
    , ifModules :: Map Name (IfaceG Name)
ifModules   = Map Name (IfaceG Name)
mPriv
    }

  , ifParams :: IfaceParams
ifParams = IfaceParams :: Map Name ModTParam
-> [Located Prop] -> Map Name ModVParam -> IfaceParams
IfaceParams
    { ifParamTypes :: Map Name ModTParam
ifParamTypes = ModuleG mname -> Map Name ModTParam
forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes ModuleG mname
m
    , ifParamConstraints :: [Located Prop]
ifParamConstraints = ModuleG mname -> [Located Prop]
forall mname. ModuleG mname -> [Located Prop]
mParamConstraints ModuleG mname
m
    , ifParamFuns :: Map Name ModVParam
ifParamFuns  = ModuleG mname -> Map Name ModVParam
forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns ModuleG mname
m
    }
  }
  where

  (Map Name IfaceTySyn
tsPub,Map Name IfaceTySyn
tsPriv) =
      (Name -> IfaceTySyn -> Bool)
-> Map Name IfaceTySyn
-> (Map Name IfaceTySyn, Map Name IfaceTySyn)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\ Name
qn IfaceTySyn
_ -> Name
qn Name -> ExportSpec Name -> Bool
forall name. Ord name => name -> ExportSpec name -> Bool
`isExportedType` ModuleG mname -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG mname
m )
                          (ModuleG mname -> Map Name IfaceTySyn
forall mname. ModuleG mname -> Map Name IfaceTySyn
mTySyns ModuleG mname
m)
  (Map Name IfaceNewtype
ntPub,Map Name IfaceNewtype
ntPriv) =
      (Name -> IfaceNewtype -> Bool)
-> Map Name IfaceNewtype
-> (Map Name IfaceNewtype, Map Name IfaceNewtype)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\ Name
qn IfaceNewtype
_ -> Name
qn Name -> ExportSpec Name -> Bool
forall name. Ord name => name -> ExportSpec name -> Bool
`isExportedType` ModuleG mname -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG mname
m )
                           (ModuleG mname -> Map Name IfaceNewtype
forall mname. ModuleG mname -> Map Name IfaceNewtype
mNewtypes ModuleG mname
m)

  (Map Name IfaceAbstractType
atPub,Map Name IfaceAbstractType
atPriv) =
    (Name -> IfaceAbstractType -> Bool)
-> Map Name IfaceAbstractType
-> (Map Name IfaceAbstractType, Map Name IfaceAbstractType)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\Name
qn IfaceAbstractType
_ -> Name
qn Name -> ExportSpec Name -> Bool
forall name. Ord name => name -> ExportSpec name -> Bool
`isExportedType` ModuleG mname -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG mname
m)
                         (ModuleG mname -> Map Name IfaceAbstractType
forall mname. ModuleG mname -> Map Name IfaceAbstractType
mPrimTypes ModuleG mname
m)

  (Map Name IfaceDecl
dPub,Map Name IfaceDecl
dPriv) =
      (Name -> IfaceDecl -> Bool)
-> Map Name IfaceDecl -> (Map Name IfaceDecl, Map Name IfaceDecl)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\ Name
qn IfaceDecl
_ -> Name
qn Name -> ExportSpec Name -> Bool
forall name. Ord name => name -> ExportSpec name -> Bool
`isExportedBind` ModuleG mname -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG mname
m)
      (Map Name IfaceDecl -> (Map Name IfaceDecl, Map Name IfaceDecl))
-> Map Name IfaceDecl -> (Map Name IfaceDecl, Map Name IfaceDecl)
forall a b. (a -> b) -> a -> b
$ [(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 mname -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG mname
m
                                          , Decl
d  <- DeclGroup -> [Decl]
groupDecls DeclGroup
dg
                                          , let qn :: Name
qn = Decl -> Name
dName Decl
d
                                          ]

  (Map Name (IfaceG Name)
mPub,Map Name (IfaceG Name)
mPriv) =
      (Name -> IfaceG Name -> Bool)
-> Map Name (IfaceG Name)
-> (Map Name (IfaceG Name), Map Name (IfaceG Name))
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\ Name
qn IfaceG Name
_ -> Namespace -> Name -> ExportSpec Name -> Bool
forall name.
Ord name =>
Namespace -> name -> ExportSpec name -> Bool
isExported Namespace
NSModule Name
qn (ModuleG mname -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG mname
m))
      (Map Name (IfaceG Name)
 -> (Map Name (IfaceG Name), Map Name (IfaceG Name)))
-> Map Name (IfaceG Name)
-> (Map Name (IfaceG Name), Map Name (IfaceG Name))
forall a b. (a -> b) -> a -> b
$ ModuleG mname -> Map Name (IfaceG Name)
forall mname. ModuleG mname -> Map Name (IfaceG Name)
mSubModules ModuleG mname
m