mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Merge public and private in interfaces. One may consult IfaceNames to determine what's public
This commit is contained in:
parent
2a8391d02e
commit
1cfe50850b
@ -111,7 +111,7 @@ ifaceNamesToMod iface params names =
|
||||
where
|
||||
defs = ifsDefines names
|
||||
isLocal x = x `Set.member` defs
|
||||
decls = filterIfaceDecls isLocal (ifPublic iface <> ifPrivate iface)
|
||||
decls = filterIfaceDecls isLocal (ifDefines iface)
|
||||
|
||||
|
||||
ifaceSigToMod :: ModParamNames -> Mod ()
|
||||
|
@ -175,7 +175,7 @@ loadedNonParamModules = map lmModule . lmLoadedModules . meLoadedModules
|
||||
|
||||
loadedNewtypes :: ModuleEnv -> Map Name T.Newtype
|
||||
loadedNewtypes menv = Map.unions
|
||||
[ ifNewtypes (ifPublic i) <> ifNewtypes (ifPrivate i)
|
||||
[ ifNewtypes (ifDefines i) <> ifNewtypes (ifDefines i)
|
||||
| i <- map lmInterface (getLoadedModules (meLoadedModules menv))
|
||||
]
|
||||
|
||||
@ -226,12 +226,14 @@ modContextOf mname me =
|
||||
do lm <- lookupModule mname me
|
||||
let localIface = lmInterface lm
|
||||
localNames = lmNamingEnv lm
|
||||
loadedDecls = map (ifPublic . lmInterface)
|
||||
|
||||
-- XXX: do we want only public ones here?
|
||||
loadedDecls = map (ifDefines . lmInterface)
|
||||
$ getLoadedModules (meLoadedModules me)
|
||||
pure ModContext
|
||||
{ mctxParams = ifParams localIface
|
||||
, mctxExported = ifaceDeclsNames (ifPublic localIface)
|
||||
, mctxDecls = mconcat (ifPrivate localIface : loadedDecls)
|
||||
, mctxExported = ifsPublic (ifNames localIface)
|
||||
, mctxDecls = mconcat (ifDefines localIface : loadedDecls)
|
||||
, mctxNames = localNames
|
||||
, mctxNameDisp = R.toNameDisp localNames
|
||||
}
|
||||
|
@ -48,13 +48,12 @@ import Cryptol.TypeCheck.Type
|
||||
|
||||
type Iface = IfaceG ModName
|
||||
|
||||
-- | The resulting interface generated by a module that has been typechecked.
|
||||
-- | The interface repersenting a typecheck top-level module.
|
||||
data IfaceG name = Iface
|
||||
{ ifNames :: IfaceNames name -- ^ Info about names in this module
|
||||
, ifParams :: FunctorParams -- ^ Module parameters, if any
|
||||
, ifPublic :: IfaceDecls -- ^ Exported definitions
|
||||
, ifPrivate :: IfaceDecls
|
||||
-- ^ Private definitions. We keep those so that we can browse them.
|
||||
, ifParams :: FunctorParams -- ^ Module parameters, if any
|
||||
, ifDefines :: IfaceDecls -- ^ All things defines in the module
|
||||
-- (includes nested definitions)
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
ifaceForgetName :: IfaceG name -> IfaceG ()
|
||||
@ -83,9 +82,8 @@ emptyIface nm = Iface
|
||||
, ifsPublic = mempty
|
||||
, ifsNested = mempty
|
||||
}
|
||||
, ifPublic = mempty
|
||||
, ifPrivate = mempty
|
||||
, ifParams = mempty
|
||||
, ifDefines = mempty
|
||||
}
|
||||
|
||||
-- | Declarations in a module. Note that this includes things from nested
|
||||
@ -180,14 +178,7 @@ data IfaceDecl = IfaceDecl
|
||||
--
|
||||
-- NOTE: the map will expose /both/ public and private names.
|
||||
ifacePrimMap :: Iface -> PrimMap
|
||||
ifacePrimMap Iface { .. } =
|
||||
PrimMap { primDecls = merge primDecls
|
||||
, primTypes = merge primTypes }
|
||||
where
|
||||
merge f = Map.union (f public) (f private)
|
||||
|
||||
public = ifaceDeclsPrimMap ifPublic
|
||||
private = ifaceDeclsPrimMap ifPrivate
|
||||
ifacePrimMap = ifaceDeclsPrimMap . ifDefines
|
||||
|
||||
ifaceDeclsPrimMap :: IfaceDecls -> PrimMap
|
||||
ifaceDeclsPrimMap IfaceDecls { .. } =
|
||||
|
@ -455,7 +455,7 @@ recordImport r i =
|
||||
| ifaceIsFunctor iface ->
|
||||
recordError (ModuleKindMismatch r i AModule AFunctor)
|
||||
| otherwise ->
|
||||
RenameM $ sets_ \s -> s { rwExternalDeps = ifPublic iface <>
|
||||
RenameM $ sets_ \s -> s { rwExternalDeps = ifDefines iface <>
|
||||
rwExternalDeps s }
|
||||
|
||||
|
||||
|
@ -302,7 +302,7 @@ prepareQuery evo ProverCommand{..} =
|
||||
let m = tcTopEntityToModule ent
|
||||
|
||||
let decls = mDecls m
|
||||
let nms = fst <$> Map.toList (M.ifDecls (M.ifPublic (M.genIface m)))
|
||||
let nms = fst <$> Map.toList (M.ifDecls (M.ifDefines (M.genIface m)))
|
||||
let ds = Map.fromList [ (prelPrim (identText (M.nameIdent nm)), EWhere (EVar nm) decls) | nm <- nms ]
|
||||
pure ds
|
||||
|
||||
|
@ -336,7 +336,7 @@ prepareQuery sym ProverCommand { .. } = do
|
||||
ds <- do (_mp, ent) <- M.loadModuleFrom True (M.FromModule preludeReferenceName)
|
||||
let m = tcTopEntityToModule ent
|
||||
let decls = mDecls m
|
||||
let nms = fst <$> Map.toList (M.ifDecls (M.ifPublic (M.genIface m)))
|
||||
let nms = fst <$> Map.toList (M.ifDecls (M.ifDefines (M.genIface m)))
|
||||
let ds = Map.fromList [ (prelPrim (identText (M.nameIdent nm)), EWhere (EVar nm) decls) | nm <- nms ]
|
||||
pure ds
|
||||
|
||||
|
@ -54,49 +54,23 @@ genIface m = genIfaceWithNames (genIfaceNames m) m
|
||||
genIfaceWithNames :: IfaceNames name -> ModuleG ignored -> IfaceG name
|
||||
genIfaceWithNames names m =
|
||||
Iface
|
||||
{ ifNames = names
|
||||
{ ifNames = names
|
||||
|
||||
, ifPublic = IfaceDecls
|
||||
{ ifTySyns = tsPub
|
||||
, ifNewtypes = ntPub
|
||||
, ifAbstractTypes = atPub
|
||||
, ifDecls = dPub
|
||||
, ifModules = mPub
|
||||
, ifSignatures = sPub
|
||||
, ifFunctors = fPub
|
||||
}
|
||||
|
||||
, ifPrivate = IfaceDecls
|
||||
{ ifTySyns = tsPriv
|
||||
, ifNewtypes = ntPriv
|
||||
, ifAbstractTypes = atPriv
|
||||
, ifDecls = dPriv
|
||||
, ifModules = mPriv
|
||||
, ifSignatures = sPriv
|
||||
, ifFunctors = fPriv
|
||||
, ifDefines = IfaceDecls
|
||||
{ ifTySyns = mTySyns m
|
||||
, ifNewtypes = mNewtypes m
|
||||
, ifAbstractTypes = mPrimTypes m
|
||||
, ifDecls = Map.fromList [ (qn,mkIfaceDecl d)
|
||||
| dg <- mDecls m
|
||||
, d <- groupDecls dg
|
||||
, let qn = dName d
|
||||
]
|
||||
, ifModules = mSubmodules m
|
||||
, ifSignatures = mSignatures m
|
||||
, ifFunctors = genIface <$> mFunctors m
|
||||
}
|
||||
|
||||
, ifParams = mParams m
|
||||
}
|
||||
where
|
||||
pub = ifsPublic names
|
||||
|
||||
isPub qn _ = qn `Set.member` pub
|
||||
|
||||
|
||||
(tsPub,tsPriv) = Map.partitionWithKey isPub (mTySyns m)
|
||||
(ntPub,ntPriv) = Map.partitionWithKey isPub (mNewtypes m)
|
||||
(atPub,atPriv) = Map.partitionWithKey isPub (mPrimTypes m)
|
||||
|
||||
(dPub,dPriv) =
|
||||
Map.partitionWithKey isPub
|
||||
$ Map.fromList [ (qn,mkIfaceDecl d) | dg <- mDecls m
|
||||
, d <- groupDecls dg
|
||||
, let qn = dName d
|
||||
]
|
||||
|
||||
(mPub,mPriv) = Map.partitionWithKey isPub (mSubmodules m)
|
||||
(sPub,sPriv) = Map.partitionWithKey isPub (mSignatures m)
|
||||
(fPub,fPriv) = Map.partitionWithKey isPub (genIface <$> mFunctors m)
|
||||
|
||||
|
||||
|
@ -144,7 +144,8 @@ checkArg (r,expect,actual) =
|
||||
|
||||
localNames = ifsDefines (ifNames actual)
|
||||
isLocal x = x `Set.member` localNames
|
||||
decls = filterIfaceDecls isLocal (ifPublic actual)
|
||||
decls = filterIfaceDecls isLocal (ifDefines actual)
|
||||
-- XXX: check that the name is public
|
||||
|
||||
-- Available type names
|
||||
tyMap = Map.unions [ nameMapToIdentMap fromTS (ifTySyns decls)
|
||||
|
@ -681,8 +681,12 @@ lookupVar x =
|
||||
do mb1 <- Map.lookup x . iBindTypes <$> IM get
|
||||
case mb1 of
|
||||
Just a -> pure (ExtVar a)
|
||||
Nothing -> panic "lookupVar" [ "Undefined vairable"
|
||||
, show x ]
|
||||
Nothing ->
|
||||
do mp <- IM $ asks iVars
|
||||
panic "lookupVar" $ [ "Undefined vairable"
|
||||
, show x
|
||||
, "IVARS"
|
||||
] ++ map (show . pp) (Map.keys mp)
|
||||
|
||||
-- | Lookup a type variable. Return `Nothing` if there is no such variable
|
||||
-- in scope, in which case we must be dealing with a type constant.
|
||||
@ -770,7 +774,7 @@ lookupModule iname =
|
||||
pure (fromMb
|
||||
do iface <- snd <$> mb
|
||||
names <- Map.lookup m
|
||||
(If.ifModules (If.ifPublic iface))
|
||||
(If.ifModules (If.ifDefines iface))
|
||||
pure iface
|
||||
{ If.ifNames = names { If.ifsName = () } })
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user