-- |
-- Module      :  Cryptol.ModuleSystem.Interface
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE Safe #-}
module Cryptol.ModuleSystem.Interface (
    Iface
  , IfaceG(..)
  , IfaceDecls(..)
  , IfaceDecl(..)
  , IfaceNames(..)
  , ifModName

  , emptyIface
  , ifacePrimMap
  , ifaceForgetName
  , ifaceIsFunctor
  , filterIfaceDecls
  , ifaceDeclsNames
  , ifaceOrigNameMap
  ) where

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

import GHC.Generics (Generic)
import Control.DeepSeq

import Prelude ()
import Prelude.Compat

import Cryptol.ModuleSystem.Name
import Cryptol.Utils.Ident (ModName, OrigName(..))
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Fixity(Fixity)
import Cryptol.Parser.AST(Pragma)
import Cryptol.TypeCheck.Type

type Iface = IfaceG ModName

-- | The interface repersenting a typecheck top-level module.
data IfaceG name = Iface
  { forall name. IfaceG name -> IfaceNames name
ifNames     :: IfaceNames name    -- ^ Info about names in this module
  , forall name. IfaceG name -> FunctorParams
ifParams    :: FunctorParams      -- ^ Module parameters, if any
  , forall name. IfaceG name -> IfaceDecls
ifDefines   :: IfaceDecls         -- ^ All things defines in the module
                                      -- (includes nested definitions)
  } deriving (Int -> IfaceG name -> ShowS
[IfaceG name] -> ShowS
IfaceG name -> String
(Int -> IfaceG name -> ShowS)
-> (IfaceG name -> String)
-> ([IfaceG name] -> ShowS)
-> Show (IfaceG name)
forall name. Show name => Int -> IfaceG name -> ShowS
forall name. Show name => [IfaceG name] -> ShowS
forall name. Show name => IfaceG name -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall name. Show name => Int -> IfaceG name -> ShowS
showsPrec :: Int -> IfaceG name -> ShowS
$cshow :: forall name. Show name => IfaceG name -> String
show :: IfaceG name -> String
$cshowList :: forall name. Show name => [IfaceG name] -> ShowS
showList :: [IfaceG name] -> ShowS
Show, (forall x. IfaceG name -> Rep (IfaceG name) x)
-> (forall x. Rep (IfaceG name) x -> IfaceG name)
-> Generic (IfaceG name)
forall x. Rep (IfaceG name) x -> IfaceG name
forall x. IfaceG name -> Rep (IfaceG name) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall name x. Rep (IfaceG name) x -> IfaceG name
forall name x. IfaceG name -> Rep (IfaceG name) x
$cfrom :: forall name x. IfaceG name -> Rep (IfaceG name) x
from :: forall x. IfaceG name -> Rep (IfaceG name) x
$cto :: forall name x. Rep (IfaceG name) x -> IfaceG name
to :: forall x. Rep (IfaceG name) x -> IfaceG name
Generic, IfaceG name -> ()
(IfaceG name -> ()) -> NFData (IfaceG name)
forall name. NFData name => IfaceG name -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall name. NFData name => IfaceG name -> ()
rnf :: IfaceG name -> ()
NFData)

-- | Remove the name of a module.  This is useful for dealing with collections
-- of modules, as in `Map (ImpName Name) (IfaceG ())`.
ifaceForgetName :: IfaceG name -> IfaceG ()
ifaceForgetName :: forall name. IfaceG name -> IfaceG ()
ifaceForgetName IfaceG name
i = IfaceG name
i { ifNames = newNames }
  where newNames :: IfaceNames ()
newNames = (IfaceG name -> IfaceNames name
forall name. IfaceG name -> IfaceNames name
ifNames IfaceG name
i) { ifsName = () }

-- | Access the name of a module.
ifModName :: IfaceG name -> name
ifModName :: forall name. IfaceG name -> name
ifModName = IfaceNames name -> name
forall name. IfaceNames name -> name
ifsName (IfaceNames name -> name)
-> (IfaceG name -> IfaceNames name) -> IfaceG name -> name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IfaceG name -> IfaceNames name
forall name. IfaceG name -> IfaceNames name
ifNames

-- | Information about the names in a module.
data IfaceNames name = IfaceNames
  { forall name. IfaceNames name -> name
ifsName     :: name       -- ^ Name of this submodule
  , forall name. IfaceNames name -> Set Name
ifsNested   :: Set Name   -- ^ Things nested in this module
  , forall name. IfaceNames name -> Set Name
ifsDefines  :: Set Name   -- ^ Things defined in this module
  , forall name. IfaceNames name -> Set Name
ifsPublic   :: Set Name   -- ^ Subset of `ifsDefines` that is public
  , forall name. IfaceNames name -> Maybe Text
ifsDoc      :: !(Maybe Text) -- ^ Documentation
  } deriving (Int -> IfaceNames name -> ShowS
[IfaceNames name] -> ShowS
IfaceNames name -> String
(Int -> IfaceNames name -> ShowS)
-> (IfaceNames name -> String)
-> ([IfaceNames name] -> ShowS)
-> Show (IfaceNames name)
forall name. Show name => Int -> IfaceNames name -> ShowS
forall name. Show name => [IfaceNames name] -> ShowS
forall name. Show name => IfaceNames name -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall name. Show name => Int -> IfaceNames name -> ShowS
showsPrec :: Int -> IfaceNames name -> ShowS
$cshow :: forall name. Show name => IfaceNames name -> String
show :: IfaceNames name -> String
$cshowList :: forall name. Show name => [IfaceNames name] -> ShowS
showList :: [IfaceNames name] -> ShowS
Show, (forall x. IfaceNames name -> Rep (IfaceNames name) x)
-> (forall x. Rep (IfaceNames name) x -> IfaceNames name)
-> Generic (IfaceNames name)
forall x. Rep (IfaceNames name) x -> IfaceNames name
forall x. IfaceNames name -> Rep (IfaceNames name) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall name x. Rep (IfaceNames name) x -> IfaceNames name
forall name x. IfaceNames name -> Rep (IfaceNames name) x
$cfrom :: forall name x. IfaceNames name -> Rep (IfaceNames name) x
from :: forall x. IfaceNames name -> Rep (IfaceNames name) x
$cto :: forall name x. Rep (IfaceNames name) x -> IfaceNames name
to :: forall x. Rep (IfaceNames name) x -> IfaceNames name
Generic, IfaceNames name -> ()
(IfaceNames name -> ()) -> NFData (IfaceNames name)
forall name. NFData name => IfaceNames name -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall name. NFData name => IfaceNames name -> ()
rnf :: IfaceNames name -> ()
NFData)

-- | Is this interface for a functor.
ifaceIsFunctor :: IfaceG name -> Bool
ifaceIsFunctor :: forall name. IfaceG name -> Bool
ifaceIsFunctor = Bool -> Bool
not (Bool -> Bool) -> (IfaceG name -> Bool) -> IfaceG name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FunctorParams -> Bool
forall k a. Map k a -> Bool
Map.null (FunctorParams -> Bool)
-> (IfaceG name -> FunctorParams) -> IfaceG name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IfaceG name -> FunctorParams
forall name. IfaceG name -> FunctorParams
ifParams

emptyIface :: ModName -> Iface
emptyIface :: ModName -> Iface
emptyIface ModName
nm = Iface
  { ifNames :: IfaceNames ModName
ifNames   = IfaceNames { ifsName :: ModName
ifsName    = ModName
nm
                           , ifsDefines :: Set Name
ifsDefines = Set Name
forall a. Monoid a => a
mempty
                           , ifsPublic :: Set Name
ifsPublic  = Set Name
forall a. Monoid a => a
mempty
                           , ifsNested :: Set Name
ifsNested  = Set Name
forall a. Monoid a => a
mempty
                           , ifsDoc :: Maybe Text
ifsDoc     = Maybe Text
forall a. Maybe a
Nothing
                           }
  , ifParams :: FunctorParams
ifParams  = FunctorParams
forall a. Monoid a => a
mempty
  , ifDefines :: IfaceDecls
ifDefines = IfaceDecls
forall a. Monoid a => a
mempty
  }

-- | Declarations in a module.  Note that this includes things from nested
-- modules, but not things from nested functors, which are in `ifFunctors`.
data IfaceDecls = IfaceDecls
  { IfaceDecls -> Map Name TySyn
ifTySyns        :: Map.Map Name TySyn
  , IfaceDecls -> Map Name NominalType
ifNominalTypes  :: Map.Map Name NominalType
  , IfaceDecls -> Map Name IfaceDecl
ifDecls         :: Map.Map Name IfaceDecl
  , IfaceDecls -> Map Name (IfaceNames Name)
ifModules       :: !(Map.Map Name (IfaceNames Name))
  , IfaceDecls -> Map Name ModParamNames
ifSignatures    :: !(Map.Map Name ModParamNames)
  , IfaceDecls -> Map Name (IfaceG Name)
ifFunctors      :: !(Map.Map Name (IfaceG Name))
    {- ^ XXX: Maybe arg info?
    Also, with the current implementation we aim to complete remove functors
    by essentially inlining them.  To achieve this with just interfaces
    we'd have to store here the entire module, not just its interface.
    At the moment we work around this by passing all loaded modules to the
    type checker, so it looks up functors there, instead of in the interfaces,
    but we'd need to change this if we want better support for separate
    compilation. -}

  } deriving (Int -> IfaceDecls -> ShowS
[IfaceDecls] -> ShowS
IfaceDecls -> String
(Int -> IfaceDecls -> ShowS)
-> (IfaceDecls -> String)
-> ([IfaceDecls] -> ShowS)
-> Show IfaceDecls
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IfaceDecls -> ShowS
showsPrec :: Int -> IfaceDecls -> ShowS
$cshow :: IfaceDecls -> String
show :: IfaceDecls -> String
$cshowList :: [IfaceDecls] -> ShowS
showList :: [IfaceDecls] -> ShowS
Show, (forall x. IfaceDecls -> Rep IfaceDecls x)
-> (forall x. Rep IfaceDecls x -> IfaceDecls) -> Generic IfaceDecls
forall x. Rep IfaceDecls x -> IfaceDecls
forall x. IfaceDecls -> Rep IfaceDecls x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. IfaceDecls -> Rep IfaceDecls x
from :: forall x. IfaceDecls -> Rep IfaceDecls x
$cto :: forall x. Rep IfaceDecls x -> IfaceDecls
to :: forall x. Rep IfaceDecls x -> IfaceDecls
Generic, IfaceDecls -> ()
(IfaceDecls -> ()) -> NFData IfaceDecls
forall a. (a -> ()) -> NFData a
$crnf :: IfaceDecls -> ()
rnf :: IfaceDecls -> ()
NFData)

filterIfaceDecls :: (Name -> Bool) -> IfaceDecls -> IfaceDecls
filterIfaceDecls :: (Name -> Bool) -> IfaceDecls -> IfaceDecls
filterIfaceDecls Name -> Bool
p IfaceDecls
ifs = IfaceDecls
  { ifTySyns :: Map Name TySyn
ifTySyns        = Map Name TySyn -> Map Name TySyn
forall a. Map Name a -> Map Name a
filterMap (IfaceDecls -> Map Name TySyn
ifTySyns IfaceDecls
ifs)
  , ifNominalTypes :: Map Name NominalType
ifNominalTypes  = Map Name NominalType -> Map Name NominalType
forall a. Map Name a -> Map Name a
filterMap (IfaceDecls -> Map Name NominalType
ifNominalTypes IfaceDecls
ifs)
  , ifDecls :: Map Name IfaceDecl
ifDecls         = Map Name IfaceDecl -> Map Name IfaceDecl
forall a. Map Name a -> Map Name a
filterMap (IfaceDecls -> Map Name IfaceDecl
ifDecls IfaceDecls
ifs)
  , ifModules :: Map Name (IfaceNames Name)
ifModules       = Map Name (IfaceNames Name) -> Map Name (IfaceNames Name)
forall a. Map Name a -> Map Name a
filterMap (IfaceDecls -> Map Name (IfaceNames Name)
ifModules IfaceDecls
ifs)
  , ifFunctors :: Map Name (IfaceG Name)
ifFunctors      = Map Name (IfaceG Name) -> Map Name (IfaceG Name)
forall a. Map Name a -> Map Name a
filterMap (IfaceDecls -> Map Name (IfaceG Name)
ifFunctors IfaceDecls
ifs)
  , ifSignatures :: Map Name ModParamNames
ifSignatures    = Map Name ModParamNames -> Map Name ModParamNames
forall a. Map Name a -> Map Name a
filterMap (IfaceDecls -> Map Name ModParamNames
ifSignatures IfaceDecls
ifs)
  }
  where
  filterMap :: Map.Map Name a -> Map.Map Name a
  filterMap :: forall a. Map Name a -> Map Name a
filterMap = (Name -> a -> Bool) -> Map Name a -> Map Name a
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\Name
k a
_ -> Name -> Bool
p Name
k)

ifaceDeclsNames :: IfaceDecls -> Set Name
ifaceDeclsNames :: IfaceDecls -> Set Name
ifaceDeclsNames IfaceDecls
i = [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 (IfaceDecls -> Map Name TySyn
ifTySyns IfaceDecls
i)
                               , Map Name NominalType -> Set Name
forall k a. Map k a -> Set k
Map.keysSet (IfaceDecls -> Map Name NominalType
ifNominalTypes IfaceDecls
i)
                               , Map Name IfaceDecl -> Set Name
forall k a. Map k a -> Set k
Map.keysSet (IfaceDecls -> Map Name IfaceDecl
ifDecls IfaceDecls
i)
                               , Map Name (IfaceNames Name) -> Set Name
forall k a. Map k a -> Set k
Map.keysSet (IfaceDecls -> Map Name (IfaceNames Name)
ifModules IfaceDecls
i)
                               , Map Name (IfaceG Name) -> Set Name
forall k a. Map k a -> Set k
Map.keysSet (IfaceDecls -> Map Name (IfaceG Name)
ifFunctors IfaceDecls
i)
                               , Map Name ModParamNames -> Set Name
forall k a. Map k a -> Set k
Map.keysSet (IfaceDecls -> Map Name ModParamNames
ifSignatures IfaceDecls
i)
                               ]


instance Semigroup IfaceDecls where
  IfaceDecls
l <> :: IfaceDecls -> IfaceDecls -> IfaceDecls
<> IfaceDecls
r = IfaceDecls
    { ifTySyns :: Map Name TySyn
ifTySyns   = Map Name TySyn -> Map Name TySyn -> Map Name TySyn
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (IfaceDecls -> Map Name TySyn
ifTySyns IfaceDecls
l)   (IfaceDecls -> Map Name TySyn
ifTySyns IfaceDecls
r)
    , ifNominalTypes :: Map Name NominalType
ifNominalTypes = Map Name NominalType
-> Map Name NominalType -> Map Name NominalType
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (IfaceDecls -> Map Name NominalType
ifNominalTypes IfaceDecls
l) (IfaceDecls -> Map Name NominalType
ifNominalTypes IfaceDecls
r)
    , ifDecls :: Map Name IfaceDecl
ifDecls    = Map Name IfaceDecl -> Map Name IfaceDecl -> Map Name IfaceDecl
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (IfaceDecls -> Map Name IfaceDecl
ifDecls IfaceDecls
l)    (IfaceDecls -> Map Name IfaceDecl
ifDecls IfaceDecls
r)
    , ifModules :: Map Name (IfaceNames Name)
ifModules  = Map Name (IfaceNames Name)
-> Map Name (IfaceNames Name) -> Map Name (IfaceNames Name)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (IfaceDecls -> Map Name (IfaceNames Name)
ifModules IfaceDecls
l)  (IfaceDecls -> Map Name (IfaceNames Name)
ifModules IfaceDecls
r)
    , ifFunctors :: Map Name (IfaceG Name)
ifFunctors = Map Name (IfaceG Name)
-> Map Name (IfaceG Name) -> Map Name (IfaceG Name)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (IfaceDecls -> Map Name (IfaceG Name)
ifFunctors IfaceDecls
l) (IfaceDecls -> Map Name (IfaceG Name)
ifFunctors IfaceDecls
r)
    , ifSignatures :: Map Name ModParamNames
ifSignatures = IfaceDecls -> Map Name ModParamNames
ifSignatures IfaceDecls
l Map Name ModParamNames
-> Map Name ModParamNames -> Map Name ModParamNames
forall a. Semigroup a => a -> a -> a
<> IfaceDecls -> Map Name ModParamNames
ifSignatures IfaceDecls
r
    }

instance Monoid IfaceDecls where
  mempty :: IfaceDecls
mempty      = IfaceDecls
                  { ifTySyns :: Map Name TySyn
ifTySyns = Map Name TySyn
forall a. Monoid a => a
mempty
                  , ifNominalTypes :: Map Name NominalType
ifNominalTypes = Map Name NominalType
forall a. Monoid a => a
mempty
                  , ifDecls :: Map Name IfaceDecl
ifDecls = Map Name IfaceDecl
forall a. Monoid a => a
mempty
                  , ifModules :: Map Name (IfaceNames Name)
ifModules = Map Name (IfaceNames Name)
forall a. Monoid a => a
mempty
                  , ifFunctors :: Map Name (IfaceG Name)
ifFunctors = Map Name (IfaceG Name)
forall a. Monoid a => a
mempty
                  , ifSignatures :: Map Name ModParamNames
ifSignatures = Map Name ModParamNames
forall a. Monoid a => a
mempty
                  }
  mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls
mappend = IfaceDecls -> IfaceDecls -> IfaceDecls
forall a. Semigroup a => a -> a -> a
(<>)
  mconcat :: [IfaceDecls] -> IfaceDecls
mconcat [IfaceDecls]
ds  = IfaceDecls
    { ifTySyns :: Map Name TySyn
ifTySyns   = [Map Name TySyn] -> Map Name TySyn
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ((IfaceDecls -> Map Name TySyn) -> [IfaceDecls] -> [Map Name TySyn]
forall a b. (a -> b) -> [a] -> [b]
map IfaceDecls -> Map Name TySyn
ifTySyns   [IfaceDecls]
ds)
    , ifNominalTypes :: Map Name NominalType
ifNominalTypes = [Map Name NominalType] -> Map Name NominalType
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ((IfaceDecls -> Map Name NominalType)
-> [IfaceDecls] -> [Map Name NominalType]
forall a b. (a -> b) -> [a] -> [b]
map IfaceDecls -> Map Name NominalType
ifNominalTypes [IfaceDecls]
ds)
    , ifDecls :: Map Name IfaceDecl
ifDecls    = [Map Name IfaceDecl] -> Map Name IfaceDecl
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ((IfaceDecls -> Map Name IfaceDecl)
-> [IfaceDecls] -> [Map Name IfaceDecl]
forall a b. (a -> b) -> [a] -> [b]
map IfaceDecls -> Map Name IfaceDecl
ifDecls    [IfaceDecls]
ds)
    , ifModules :: Map Name (IfaceNames Name)
ifModules  = [Map Name (IfaceNames Name)] -> Map Name (IfaceNames Name)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ((IfaceDecls -> Map Name (IfaceNames Name))
-> [IfaceDecls] -> [Map Name (IfaceNames Name)]
forall a b. (a -> b) -> [a] -> [b]
map IfaceDecls -> Map Name (IfaceNames Name)
ifModules [IfaceDecls]
ds)
    , ifFunctors :: Map Name (IfaceG Name)
ifFunctors = [Map Name (IfaceG Name)] -> Map Name (IfaceG Name)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ((IfaceDecls -> Map Name (IfaceG Name))
-> [IfaceDecls] -> [Map Name (IfaceG Name)]
forall a b. (a -> b) -> [a] -> [b]
map IfaceDecls -> Map Name (IfaceG Name)
ifFunctors [IfaceDecls]
ds)
    , ifSignatures :: Map Name ModParamNames
ifSignatures = [Map Name ModParamNames] -> Map Name ModParamNames
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ((IfaceDecls -> Map Name ModParamNames)
-> [IfaceDecls] -> [Map Name ModParamNames]
forall a b. (a -> b) -> [a] -> [b]
map IfaceDecls -> Map Name ModParamNames
ifSignatures [IfaceDecls]
ds)
    }

data IfaceDecl = IfaceDecl
  { IfaceDecl -> Name
ifDeclName    :: !Name          -- ^ Name of thing
  , IfaceDecl -> Schema
ifDeclSig     :: Schema         -- ^ Type
  , IfaceDecl -> Bool
ifDeclIsPrim   :: !Bool
  , IfaceDecl -> [Pragma]
ifDeclPragmas :: [Pragma]       -- ^ Pragmas
  , IfaceDecl -> Bool
ifDeclInfix   :: Bool           -- ^ Is this an infix thing
  , IfaceDecl -> Maybe Fixity
ifDeclFixity  :: Maybe Fixity   -- ^ Fixity information
  , IfaceDecl -> Maybe Text
ifDeclDoc     :: Maybe Text     -- ^ Documentation
  } deriving (Int -> IfaceDecl -> ShowS
[IfaceDecl] -> ShowS
IfaceDecl -> String
(Int -> IfaceDecl -> ShowS)
-> (IfaceDecl -> String)
-> ([IfaceDecl] -> ShowS)
-> Show IfaceDecl
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IfaceDecl -> ShowS
showsPrec :: Int -> IfaceDecl -> ShowS
$cshow :: IfaceDecl -> String
show :: IfaceDecl -> String
$cshowList :: [IfaceDecl] -> ShowS
showList :: [IfaceDecl] -> ShowS
Show, (forall x. IfaceDecl -> Rep IfaceDecl x)
-> (forall x. Rep IfaceDecl x -> IfaceDecl) -> Generic IfaceDecl
forall x. Rep IfaceDecl x -> IfaceDecl
forall x. IfaceDecl -> Rep IfaceDecl x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. IfaceDecl -> Rep IfaceDecl x
from :: forall x. IfaceDecl -> Rep IfaceDecl x
$cto :: forall x. Rep IfaceDecl x -> IfaceDecl
to :: forall x. Rep IfaceDecl x -> IfaceDecl
Generic, IfaceDecl -> ()
(IfaceDecl -> ()) -> NFData IfaceDecl
forall a. (a -> ()) -> NFData a
$crnf :: IfaceDecl -> ()
rnf :: IfaceDecl -> ()
NFData)


-- | Produce a PrimMap from an interface.
--
-- NOTE: the map will expose /both/ public and private names.
-- NOTE: this is a bit misnamed, as it is used to resolve known names
-- that Cryptol introduces (e.g., during type checking).  These
-- names need not be primitives.   A better way to do this in the future
-- might be to use original names instead (see #1522).
ifacePrimMap :: Iface -> PrimMap
ifacePrimMap :: Iface -> PrimMap
ifacePrimMap = IfaceDecls -> PrimMap
ifaceDeclsPrimMap (IfaceDecls -> PrimMap)
-> (Iface -> IfaceDecls) -> Iface -> PrimMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Iface -> IfaceDecls
forall name. IfaceG name -> IfaceDecls
ifDefines

ifaceDeclsPrimMap :: IfaceDecls -> PrimMap
ifaceDeclsPrimMap :: IfaceDecls -> PrimMap
ifaceDeclsPrimMap IfaceDecls { Map Name NominalType
Map Name TySyn
Map Name ModParamNames
Map Name IfaceDecl
Map Name (IfaceNames Name)
Map Name (IfaceG Name)
ifFunctors :: IfaceDecls -> Map Name (IfaceG Name)
ifTySyns :: IfaceDecls -> Map Name TySyn
ifNominalTypes :: IfaceDecls -> Map Name NominalType
ifDecls :: IfaceDecls -> Map Name IfaceDecl
ifModules :: IfaceDecls -> Map Name (IfaceNames Name)
ifSignatures :: IfaceDecls -> Map Name ModParamNames
ifTySyns :: Map Name TySyn
ifNominalTypes :: Map Name NominalType
ifDecls :: Map Name IfaceDecl
ifModules :: Map Name (IfaceNames Name)
ifSignatures :: Map Name ModParamNames
ifFunctors :: Map Name (IfaceG Name)
.. } =
  PrimMap { primDecls :: Map PrimIdent Name
primDecls = [(PrimIdent, Name)] -> Map PrimIdent Name
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(PrimIdent, Name)]
nominalVs [(PrimIdent, Name)] -> [(PrimIdent, Name)] -> [(PrimIdent, Name)]
forall a. [a] -> [a] -> [a]
++ [(PrimIdent, Name)]
exprs)
          , primTypes :: Map PrimIdent Name
primTypes = [(PrimIdent, Name)] -> Map PrimIdent Name
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(PrimIdent, Name)]
nominalTs [(PrimIdent, Name)] -> [(PrimIdent, Name)] -> [(PrimIdent, Name)]
forall a. [a] -> [a] -> [a]
++ [(PrimIdent, Name)]
types)
          }
  where
  entry :: Name -> (PrimIdent, Name)
entry Name
n = case Name -> Maybe PrimIdent
asPrim Name
n of
              Just PrimIdent
pid -> (PrimIdent
pid,Name
n)
              Maybe PrimIdent
Nothing ->
                String -> [String] -> (PrimIdent, Name)
forall a. HasCallStack => String -> [String] -> a
panic String
"ifaceDeclsPrimMap"
                          [ String
"Top level name not declared in a module?"
                          , Name -> String
forall a. Show a => a -> String
show Name
n ]

  nominalTs :: [(PrimIdent, Name)]
nominalTs = (Name -> (PrimIdent, Name)) -> [Name] -> [(PrimIdent, Name)]
forall a b. (a -> b) -> [a] -> [b]
map Name -> (PrimIdent, Name)
entry (Map Name NominalType -> [Name]
forall k a. Map k a -> [k]
Map.keys Map Name NominalType
ifNominalTypes)
  nominalVs :: [(PrimIdent, Name)]
nominalVs = [ Name -> (PrimIdent, Name)
entry Name
n
              | NominalType
nt <- Map Name NominalType -> [NominalType]
forall k a. Map k a -> [a]
Map.elems Map Name NominalType
ifNominalTypes
              , (Name
n,Schema
_) <- NominalType -> [(Name, Schema)]
nominalTypeConTypes NominalType
nt
              ]
  exprs :: [(PrimIdent, Name)]
exprs     = (Name -> (PrimIdent, Name)) -> [Name] -> [(PrimIdent, Name)]
forall a b. (a -> b) -> [a] -> [b]
map Name -> (PrimIdent, Name)
entry (Map Name IfaceDecl -> [Name]
forall k a. Map k a -> [k]
Map.keys Map Name IfaceDecl
ifDecls)
  types :: [(PrimIdent, Name)]
types     = (Name -> (PrimIdent, Name)) -> [Name] -> [(PrimIdent, Name)]
forall a b. (a -> b) -> [a] -> [b]
map Name -> (PrimIdent, Name)
entry (Map Name TySyn -> [Name]
forall k a. Map k a -> [k]
Map.keys Map Name TySyn
ifTySyns)


-- | Given an interface computing a map from original names to actual names,
-- grouped by namespace.
ifaceOrigNameMap :: IfaceG name -> Map Namespace (Map OrigName Name)
ifaceOrigNameMap :: forall name. IfaceG name -> Map Namespace (Map OrigName Name)
ifaceOrigNameMap IfaceG name
ifa = (Map OrigName Name -> Map OrigName Name -> Map OrigName Name)
-> [Map Namespace (Map OrigName Name)]
-> Map Namespace (Map OrigName Name)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith Map OrigName Name -> Map OrigName Name -> Map OrigName Name
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Map Namespace (Map OrigName Name)
here Map Namespace (Map OrigName Name)
-> [Map Namespace (Map OrigName Name)]
-> [Map Namespace (Map OrigName Name)]
forall a. a -> [a] -> [a]
: [Map Namespace (Map OrigName Name)]
nested)
  where
  here :: Map Namespace (Map OrigName Name)
here        = [(Namespace, Map OrigName Name)]
-> Map Namespace (Map OrigName Name)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Namespace, Map OrigName Name)]
 -> Map Namespace (Map OrigName Name))
-> [(Namespace, Map OrigName Name)]
-> Map Namespace (Map OrigName Name)
forall a b. (a -> b) -> a -> b
$
                  [ (Namespace
NSValue, Set Name -> Map OrigName Name
toMap Set Name
vaNames) | Bool -> Bool
not (Set Name -> Bool
forall a. Set a -> Bool
Set.null Set Name
vaNames) ] [(Namespace, Map OrigName Name)]
-> [(Namespace, Map OrigName Name)]
-> [(Namespace, Map OrigName Name)]
forall a. [a] -> [a] -> [a]
++
                  [ (Namespace
NSType,  Set Name -> Map OrigName Name
toMap Set Name
tyNames) | Bool -> Bool
not (Set Name -> Bool
forall a. Set a -> Bool
Set.null Set Name
tyNames) ] [(Namespace, Map OrigName Name)]
-> [(Namespace, Map OrigName Name)]
-> [(Namespace, Map OrigName Name)]
forall a. [a] -> [a] -> [a]
++
                  [ (Namespace
NSValue, Set Name -> Map OrigName Name
toMap Set Name
moNames) | Bool -> Bool
not (Set Name -> Bool
forall a. Set a -> Bool
Set.null Set Name
moNames) ]

  nested :: [Map Namespace (Map OrigName Name)]
nested      = (IfaceG Name -> Map Namespace (Map OrigName Name))
-> [IfaceG Name] -> [Map Namespace (Map OrigName Name)]
forall a b. (a -> b) -> [a] -> [b]
map IfaceG Name -> Map Namespace (Map OrigName Name)
forall name. IfaceG name -> Map Namespace (Map OrigName Name)
ifaceOrigNameMap (Map Name (IfaceG Name) -> [IfaceG Name]
forall k a. Map k a -> [a]
Map.elems (IfaceDecls -> Map Name (IfaceG Name)
ifFunctors IfaceDecls
decls))

  toMap :: Set Name -> Map OrigName Name
toMap Set Name
names = [(OrigName, Name)] -> Map OrigName Name
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
                  [ (OrigName
og,Name
x) | Name
x <- Set Name -> [Name]
forall a. Set a -> [a]
Set.toList Set Name
names, Just OrigName
og <- [ Name -> Maybe OrigName
asOrigName Name
x ] ]

  decls :: IfaceDecls
decls       = IfaceG name -> IfaceDecls
forall name. IfaceG name -> IfaceDecls
ifDefines IfaceG name
ifa
  from :: (IfaceDecls -> Map k a) -> Set k
from IfaceDecls -> Map k a
f      = Map k a -> Set k
forall k a. Map k a -> Set k
Map.keysSet (IfaceDecls -> Map k a
f IfaceDecls
decls)
  tyNames :: Set Name
tyNames     = [Set Name] -> Set Name
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [ (IfaceDecls -> Map Name TySyn) -> Set Name
forall {k} {a}. (IfaceDecls -> Map k a) -> Set k
from IfaceDecls -> Map Name TySyn
ifTySyns, (IfaceDecls -> Map Name NominalType) -> Set Name
forall {k} {a}. (IfaceDecls -> Map k a) -> Set k
from IfaceDecls -> Map Name NominalType
ifNominalTypes ]
  moNames :: Set Name
moNames     = [Set Name] -> Set Name
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [ (IfaceDecls -> Map Name (IfaceNames Name)) -> Set Name
forall {k} {a}. (IfaceDecls -> Map k a) -> Set k
from IfaceDecls -> Map Name (IfaceNames Name)
ifModules, (IfaceDecls -> Map Name ModParamNames) -> Set Name
forall {k} {a}. (IfaceDecls -> Map k a) -> Set k
from IfaceDecls -> Map Name ModParamNames
ifSignatures, (IfaceDecls -> Map Name (IfaceG Name)) -> Set Name
forall {k} {a}. (IfaceDecls -> Map k a) -> Set k
from IfaceDecls -> Map Name (IfaceG Name)
ifFunctors ]
  vaNames :: Set Name
vaNames     = [Set Name] -> Set Name
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [ Set Name
newtypeCons, (IfaceDecls -> Map Name IfaceDecl) -> Set Name
forall {k} {a}. (IfaceDecls -> Map k a) -> Set k
from IfaceDecls -> Map Name IfaceDecl
ifDecls ]
  newtypeCons :: Set Name
newtypeCons = [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 NominalType -> [Name]
conNames (Map Name NominalType -> [NominalType]
forall k a. Map k a -> [a]
Map.elems (IfaceDecls -> Map Name NominalType
ifNominalTypes IfaceDecls
decls)))
    where conNames :: NominalType -> [Name]
conNames = ((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