    {-# 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 :: Maybe Text
    ifsDoc      = ModuleG name -> Maybe Text
    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 =
      [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 Newtype -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet  (ModuleG name -> Map Name Newtype
    forall mname. ModuleG mname -> Map Name Newtype
    mNewtypes ModuleG name
    m)
        , [Name] -> Set Name
    forall a. Ord a => [a] -> Set a
    Set.fromList ((Newtype -> Name) -> [Newtype] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map Newtype -> Name
    ntConName (Map Name Newtype -> [Newtype]
    forall k a. Map k a -> [a]
    Map.elems (ModuleG name -> Map Name Newtype
    forall mname. ModuleG mname -> Map Name Newtype
    mNewtypes ModuleG name
    m)))
        , Map Name AbstractType -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet  (ModuleG name -> Map Name AbstractType
    forall mname. ModuleG mname -> Map Name AbstractType
    mPrimTypes 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 (IfaceNames Name) -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet  (ModuleG name -> Map Name (IfaceNames Name)
    forall mname. ModuleG mname -> Map Name (IfaceNames Name)
    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 (IfaceNames Name) -> Maybe (IfaceNames Name)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (ModuleG name -> Map Name (IfaceNames Name)
    forall mname. ModuleG mname -> Map Name (IfaceNames Name)
    mSubmodules ModuleG name
    m) of
                      Just IfaceNames Name
    y  -> IfaceNames Name -> Set Name
    forall name. IfaceNames name -> Set Name
    ifsDefines IfaceNames Name
    y 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
    y)
                      Maybe (IfaceNames Name)
    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
        , ifNewtypes :: Map Name Newtype
    ifNewtypes        = ModuleG ignored -> Map Name Newtype
    forall mname. ModuleG mname -> Map Name Newtype
    mNewtypes ModuleG ignored
    m
        , ifAbstractTypes :: Map Name AbstractType
    ifAbstractTypes   = ModuleG ignored -> Map Name AbstractType
    forall mname. ModuleG mname -> Map Name AbstractType
    mPrimTypes 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         = ModuleG ignored -> Map Name (IfaceNames Name)
    forall mname. ModuleG mname -> Map Name (IfaceNames Name)
    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
      }