mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-10-26 14:20:59 +03:00
Checkpoing: make signatures into a special kind of module.
Still need to refactor interfaces to account for top-level signatures
This commit is contained in:
parent
4ce271db02
commit
5578437e2c
@ -18,7 +18,7 @@
|
||||
module Cryptol.ModuleSystem.Base where
|
||||
|
||||
import qualified Control.Exception as X
|
||||
import Control.Monad (unless,when,forM)
|
||||
import Control.Monad (unless,forM)
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Monoid ((<>))
|
||||
import Data.Text.Encoding (decodeUtf8')
|
||||
@ -303,11 +303,12 @@ addPrelude m
|
||||
where
|
||||
newDef =
|
||||
case mDef m of
|
||||
NormalModule ds -> NormalModule (importPrelude : ds)
|
||||
NormalModule ds -> NormalModule (P.DImport prel : ds)
|
||||
FunctorInstance f as ins -> FunctorInstance f as ins
|
||||
SignatureModule s -> SignatureModule s { sigImports = prel : sigImports s }
|
||||
|
||||
importedMods = map (P.iModule . P.thing) (P.mImports m)
|
||||
importPrelude = P.DImport P.Located
|
||||
prel = P.Located
|
||||
{ P.srcRange = emptyRange
|
||||
, P.thing = P.Import
|
||||
{ iModule = P.ImpTop preludeName
|
||||
@ -320,34 +321,40 @@ addPrelude m
|
||||
loadDeps :: P.ModuleG mname name -> ModuleM ()
|
||||
loadDeps m =
|
||||
case mDef m of
|
||||
NormalModule ds -> mapM_ depsOfDecl ds
|
||||
NormalModule ds -> mapM_ depsOfDecl ds
|
||||
FunctorInstance f as _ ->
|
||||
do loadImpName f
|
||||
do loadImpName FromModuleInstance f
|
||||
case as of
|
||||
DefaultInstArg a -> loadImpName a
|
||||
DefaultInstArg a -> loadImpName FromModuleInstance a
|
||||
DefaultInstAnonArg ds -> mapM_ depsOfDecl ds
|
||||
NamedInstArgs args -> mapM_ loadInstArg args
|
||||
SignatureModule s -> mapM_ loadImpD (sigImports s)
|
||||
where
|
||||
loadI i = do (_,m1) <- loadModuleFrom False (FromImport i)
|
||||
when (T.isParametrizedModule m1) $ importParamModule $ T.mName m1
|
||||
loadF f = do _ <- loadModuleFrom False (FromModuleInstance f)
|
||||
return ()
|
||||
loadI i = do _ <- loadModuleFrom False i
|
||||
pure ()
|
||||
|
||||
loadImpName src l =
|
||||
case thing l of
|
||||
ImpTop f -> loadI (src l { thing = f })
|
||||
_ -> pure ()
|
||||
|
||||
loadImpD li = loadImpName (FromImport . new) (iModule <$> li)
|
||||
where new i = i { thing = (thing li) { iModule = thing i } }
|
||||
|
||||
loadInstArg (ModuleInstanceArg _ f) = loadImpName FromModuleInstance f
|
||||
|
||||
depsOfDecl d =
|
||||
case d of
|
||||
DImport li ->
|
||||
case iModule (thing li) of
|
||||
ImpTop f -> loadI li { thing = (thing li) { iModule = f } }
|
||||
_ -> pure ()
|
||||
DImport li -> loadImpD li
|
||||
|
||||
DModule TopLevel { tlValue = NestedModule nm } -> loadDeps nm
|
||||
|
||||
DModParam mo -> loadImpName FromSigImport s
|
||||
where s = mpSignature mo
|
||||
|
||||
_ -> pure ()
|
||||
|
||||
loadInstArg (ModuleInstanceArg _ f) = loadImpName f
|
||||
|
||||
loadImpName l =
|
||||
case thing l of
|
||||
ImpTop f -> loadF l { thing = f }
|
||||
_ -> pure ()
|
||||
|
||||
|
||||
|
||||
|
@ -7,6 +7,7 @@ module Cryptol.ModuleSystem.Binds
|
||||
( BindsNames
|
||||
, TopDef(..)
|
||||
, Mod(..)
|
||||
, ModKind(..)
|
||||
, modNested
|
||||
, modBuilder
|
||||
, topModuleDefs
|
||||
@ -42,14 +43,15 @@ import Cryptol.ModuleSystem.Interface
|
||||
|
||||
data TopDef = TopMod ModName (Mod ())
|
||||
| TopInst ModName (ImpName PName) (ModuleInstanceArgs PName)
|
||||
| TopSig ModName (Mod ())
|
||||
|
||||
-- | Things defined by a module
|
||||
data Mod a = Mod
|
||||
{ modImports :: [ ImportG (ImpName PName) ]
|
||||
, modParams :: Bool -- True = has params
|
||||
, modKind :: ModKind
|
||||
, modInstances :: Map Name (ImpName PName, ModuleInstanceArgs PName)
|
||||
, modMods :: Map Name (Mod a)
|
||||
, modSigs :: Map Name NamingEnv
|
||||
, modMods :: Map Name (Mod a) -- ^ this includes signatures
|
||||
|
||||
, modDefines :: NamingEnv
|
||||
{- ^ Things defined by this module. Note the for normal modules we
|
||||
really just need the public names, however for things within
|
||||
@ -68,7 +70,6 @@ data Mod a = Mod
|
||||
|
||||
modNested :: Mod a -> Set Name
|
||||
modNested m = Set.unions [ Map.keysSet (modInstances m)
|
||||
, Map.keysSet (modSigs m)
|
||||
, Map.keysSet (modMods m)
|
||||
]
|
||||
|
||||
@ -93,12 +94,13 @@ ifaceToMod iface = ifaceNamesToMod iface (ifaceIsFunctor iface) (ifNames iface)
|
||||
ifaceNamesToMod :: IfaceG topname -> Bool -> IfaceNames name -> Mod ()
|
||||
ifaceNamesToMod iface params names =
|
||||
Mod
|
||||
{ modParams = params
|
||||
{ modKind = if params then AFunctor else AModule
|
||||
, modMods = (ifaceNamesToMod iface False <$> ifModules decls)
|
||||
`Map.union`
|
||||
(ifaceToMod <$> ifFunctors decls)
|
||||
`Map.union`
|
||||
(ifaceSigToMod <$> ifSignatures decls)
|
||||
, modDefines = namingEnvFromNames defs
|
||||
, modSigs = modParamsNamingEnv <$> ifSignatures decls
|
||||
, modPublic = ifsPublic names
|
||||
|
||||
, modImports = []
|
||||
@ -111,6 +113,23 @@ ifaceNamesToMod iface params names =
|
||||
decls = filterIfaceDecls isLocal (ifPublic iface <> ifPrivate iface)
|
||||
|
||||
|
||||
ifaceSigToMod :: IfaceParams -> Mod ()
|
||||
ifaceSigToMod ps = Mod
|
||||
{ modImports = []
|
||||
, modKind = ASignature
|
||||
, modInstances = mempty
|
||||
, modMods = mempty
|
||||
, modDefines = env
|
||||
, modPublic = namingEnvNames env
|
||||
, modState = ()
|
||||
}
|
||||
where
|
||||
env = modParamsNamingEnv ps
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
type ModBuilder = SupplyT (M.StateT [RenamerError] M.Id)
|
||||
|
||||
@ -130,12 +149,26 @@ topModuleDefs m =
|
||||
case mDef m of
|
||||
NormalModule ds -> TopMod mname <$> declsToMod (Just (TopModule mname)) ds
|
||||
FunctorInstance f as _ -> pure (TopInst mname (thing f) as)
|
||||
SignatureModule s -> TopSig mname <$> sigToMod (TopModule mname) s
|
||||
where
|
||||
mname = thing (mName m)
|
||||
|
||||
topDeclsDefs :: [TopDecl PName] -> ModBuilder (Mod ())
|
||||
topDeclsDefs = declsToMod Nothing
|
||||
|
||||
sigToMod :: ModPath -> Signature PName -> ModBuilder (Mod ())
|
||||
sigToMod mp sig =
|
||||
do env <- defNames (signatureDefs mp sig)
|
||||
pure Mod { modImports = map thing (sigImports sig)
|
||||
, modKind = ASignature
|
||||
, modInstances = mempty
|
||||
, modMods = mempty
|
||||
, modDefines = env
|
||||
, modPublic = mempty -- unused
|
||||
, modState = ()
|
||||
}
|
||||
|
||||
|
||||
|
||||
declsToMod :: Maybe ModPath -> [TopDecl PName] -> ModBuilder (Mod ())
|
||||
declsToMod mbPath ds =
|
||||
@ -155,10 +188,10 @@ declsToMod mbPath ds =
|
||||
_ -> pure ()
|
||||
|
||||
let mo = Mod { modImports = [ thing i | DImport i <- ds ]
|
||||
, modParams = any isParamDecl ds
|
||||
, modKind = if any isParamDecl ds
|
||||
then AFunctor else AModule
|
||||
, modInstances = mempty
|
||||
, modMods = mempty
|
||||
, modSigs = mempty
|
||||
, modDefines = defs
|
||||
, modPublic = pub
|
||||
, modState = ()
|
||||
@ -181,29 +214,19 @@ declsToMod mbPath ds =
|
||||
pure mo
|
||||
Just path ->
|
||||
case mDef nmod of
|
||||
|
||||
NormalModule xs ->
|
||||
do m <- declsToMod (Just (Nested path (nameIdent name))) xs
|
||||
pure mo { modMods = Map.insert name m (modMods mo) }
|
||||
|
||||
FunctorInstance f args _ ->
|
||||
pure mo { modInstances = Map.insert name (thing f, args)
|
||||
(modInstances mo) }
|
||||
|
||||
DModSig tl ->
|
||||
do let sig = tlValue tl
|
||||
pname = thing (sigName sig)
|
||||
name = case lookupNS NSSignature pname defs of
|
||||
Just (One x) -> x
|
||||
_ -> panic "declsToMod" ["sig: Missed ambig/undefined"]
|
||||
case mbPath of
|
||||
{- No top level signatures at the moment, as nothing would
|
||||
be in scope in them (they don't have imports) -}
|
||||
Nothing ->
|
||||
do defErr (UnexpectedNest (srcRange (sigName sig)) pname)
|
||||
pure mo
|
||||
Just path ->
|
||||
do newEnv <-
|
||||
defNames (signatureDefs (Nested path (nameIdent name)) sig)
|
||||
pure mo { modSigs = Map.insert name newEnv (modSigs mo) }
|
||||
SignatureModule sig ->
|
||||
do m <- sigToMod (Nested path (nameIdent name)) sig
|
||||
pure mo { modMods = Map.insert name m (modMods mo) }
|
||||
|
||||
|
||||
_ -> pure mo
|
||||
|
||||
@ -304,8 +327,6 @@ instance BindsNames (InModule (TopDecl PName)) where
|
||||
Include _ -> mempty
|
||||
DImport {} -> mempty -- see 'openLoop' in the renamer
|
||||
DModule m -> namingEnv (InModule ns (tlValue m))
|
||||
|
||||
DModSig s -> namingEnv (InModule ns (tlValue s))
|
||||
DModParam {} -> mempty-- handled in the renamer as we need to resolve
|
||||
-- the signature name first (similar to import)
|
||||
|
||||
@ -315,14 +336,6 @@ instance BindsNames (InModule (NestedModule PName)) where
|
||||
nm <- newTop NSModule m (thing pnmame) Nothing (srcRange pnmame)
|
||||
pure (singletonNS NSModule (thing pnmame) nm)
|
||||
|
||||
instance BindsNames (InModule (Signature PName)) where
|
||||
namingEnv (InModule ~(Just m) sig) = BuildNamingEnv
|
||||
do let pname = sigName sig
|
||||
nm <- newTop NSSignature m (thing pname) Nothing (srcRange pname)
|
||||
pure (singletonNS NSSignature (thing pname) nm)
|
||||
|
||||
|
||||
|
||||
instance BindsNames (InModule (PrimType PName)) where
|
||||
namingEnv (InModule ~(Just m) PrimType { .. }) =
|
||||
BuildNamingEnv $
|
||||
|
@ -33,8 +33,6 @@ exportedNames decl =
|
||||
case tlValue nested of
|
||||
NestedModule x ->
|
||||
[exportName NSModule nested { tlValue = thing (mName x) }]
|
||||
DModSig s ->
|
||||
[ exportName NSSignature s { tlValue = thing (sigName (tlValue s)) } ]
|
||||
DModParam {} -> []
|
||||
where
|
||||
names by td = [ td { tlValue = thing n } | n <- fst (by (tlValue td)) ]
|
||||
|
@ -52,7 +52,7 @@ import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.Utils.Ident (ModName,Ident)
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.Fixity(Fixity)
|
||||
import Cryptol.Parser.AST(Pragma)
|
||||
import Cryptol.Parser.AST(Pragma,ImpName(..))
|
||||
import Cryptol.Parser.Position(Located)
|
||||
import Cryptol.TypeCheck.Type
|
||||
|
||||
@ -66,6 +66,8 @@ data IfaceG name = Iface
|
||||
, ifParams :: Maybe IfaceFunctorParams
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
-- XXX: signature
|
||||
|
||||
ifaceForgetName :: IfaceG name -> IfaceG ()
|
||||
ifaceForgetName i = i { ifNames = newNames }
|
||||
where newNames = (ifNames i) { ifsName = () }
|
||||
@ -103,7 +105,7 @@ data IfaceFunctorParams =
|
||||
|
||||
data IfaceModParam = IfaceModParam
|
||||
{ ifmpName :: Ident
|
||||
, ifmpSignature :: Name
|
||||
, ifmpSignature :: ImpName Name
|
||||
, ifmpParameters :: IfaceParams
|
||||
{- ^ These are the actual parameters, not the ones in the signature
|
||||
For example if the same signature is used for multiple parameters
|
||||
|
@ -61,6 +61,7 @@ import Prelude.Compat
|
||||
data ImportSource
|
||||
= FromModule P.ModName
|
||||
| FromImport (Located P.Import)
|
||||
| FromSigImport (Located P.ModName)
|
||||
| FromModuleInstance (Located P.ModName)
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
@ -71,6 +72,7 @@ instance PP ImportSource where
|
||||
ppPrec _ is = case is of
|
||||
FromModule n -> text "module name" <+> pp n
|
||||
FromImport li -> text "import of module" <+> pp (P.iModule (P.thing li))
|
||||
FromSigImport l -> text "import of signature" <+> pp (P.thing l)
|
||||
FromModuleInstance l ->
|
||||
text "instantiation of module" <+> pp (P.thing l)
|
||||
|
||||
@ -80,6 +82,7 @@ importedModule is =
|
||||
FromModule n -> n
|
||||
FromImport li -> P.iModule (P.thing li)
|
||||
FromModuleInstance l -> P.thing l
|
||||
FromSigImport l -> P.thing l
|
||||
|
||||
|
||||
data ModuleError
|
||||
|
@ -271,7 +271,7 @@ unqualifiedEnv IfaceDecls { .. } =
|
||||
mods = mconcat [ singletonNS NSModule (toPName n) n
|
||||
| n <- Map.keys ifModules ]
|
||||
|
||||
sigs = mconcat [ singletonNS NSSignature (toPName n) n
|
||||
sigs = mconcat [ singletonNS NSModule (toPName n) n
|
||||
| n <- Map.keys ifSignatures ]
|
||||
|
||||
|
||||
|
@ -132,6 +132,7 @@ renameModule m0 =
|
||||
NormalModule ds ->
|
||||
NormalModule (addImplicitNestedImports ds)
|
||||
FunctorInstance f as i -> FunctorInstance f as i
|
||||
SignatureModule s -> SignatureModule s
|
||||
}
|
||||
|
||||
-- Step 2: compute what's defined
|
||||
@ -139,7 +140,7 @@ renameModule m0 =
|
||||
mapM_ recordError errs
|
||||
|
||||
-- Step 3: resolve imports
|
||||
extern <- getLoadedMods
|
||||
extern <- getExternalMods
|
||||
resolvedMods <- liftSupply (resolveImports extern defs)
|
||||
|
||||
let pathToName = Map.fromList [ (Nested (nameModPath x) (nameIdent x), x)
|
||||
@ -182,7 +183,7 @@ renameTopDecls m ds0 =
|
||||
mapM_ recordError errs
|
||||
|
||||
-- Step 3: resolve imports
|
||||
extern <- getLoadedMods
|
||||
extern <- getExternalMods
|
||||
resolvedMods <- liftSupply (resolveImports extern (TopMod m defs))
|
||||
|
||||
let pathToName = Map.fromList [ (Nested (nameModPath x) (nameIdent x), x)
|
||||
@ -256,6 +257,9 @@ renameModule' mname m =
|
||||
imap <- mkInstMap l mempty (thing f') mname
|
||||
pure (FunctorInstance f' as' imap)
|
||||
|
||||
SignatureModule s ->
|
||||
SignatureModule <$> renameSig mname s
|
||||
|
||||
pure (inScope, newDef)
|
||||
return (inScope, m { mDef = newDef })
|
||||
|
||||
@ -264,10 +268,10 @@ checkFunctorArgs args =
|
||||
case args of
|
||||
DefaultInstAnonArg {} ->
|
||||
panic "checkFunctorArgs" ["Nested DefaultInstAnonArg"]
|
||||
DefaultInstArg l -> checkIsModule (srcRange l) (thing l)
|
||||
DefaultInstArg l -> checkIsModule (srcRange l) (thing l) AModule
|
||||
NamedInstArgs as -> mapM_ checkArg as
|
||||
where
|
||||
checkArg (ModuleInstanceArg _ l) = checkIsModule (srcRange l) (thing l)
|
||||
checkArg (ModuleInstanceArg _ l) = checkIsModule (srcRange l) (thing l) AModule
|
||||
|
||||
mkInstMap :: Maybe Range -> Map Name Name -> ImpName Name -> ImpName Name ->
|
||||
RenameM (Map Name Name)
|
||||
@ -465,7 +469,6 @@ renameTopDecls' ds =
|
||||
DModule tl -> any usesCtrs (mDecls m)
|
||||
where NestedModule m = tlValue tl
|
||||
DImport {} -> False
|
||||
DModSig {} -> False -- no definitions here
|
||||
DModParam {} -> False -- no definitions here
|
||||
Include {} -> bad "Include"
|
||||
DParameterType {} -> bad "DParameterType"
|
||||
@ -513,8 +516,6 @@ topDeclName topDecl =
|
||||
DModule d -> hasName (thing (mName m))
|
||||
where NestedModule m = tlValue d
|
||||
|
||||
DModSig d -> hasName (thing (sigName (tlValue d)))
|
||||
|
||||
DParameterConstraint ds ->
|
||||
case ds of
|
||||
[] -> noName
|
||||
@ -551,16 +552,23 @@ doModParam mp =
|
||||
do let sigName = mpSignature mp
|
||||
loc = srcRange sigName
|
||||
withLoc loc
|
||||
do nm <- resolveName NameUse NSSignature (thing sigName)
|
||||
do me <- getCurMod
|
||||
|
||||
me <- getCurMod
|
||||
case modPathCommon me (nameModPath nm) of
|
||||
Just (_,[],_) ->
|
||||
recordError (InvalidDependency [ModPath me, NamedThing nm])
|
||||
_ -> pure ()
|
||||
sigName' <-
|
||||
case thing sigName of
|
||||
ImpTop t -> pure (ImpTop t)
|
||||
ImpNested n ->
|
||||
do nm <- resolveName NameUse NSModule n
|
||||
case modPathCommon me (nameModPath nm) of
|
||||
Just (_,[],_) ->
|
||||
recordError
|
||||
(InvalidDependency [ModPath me, NamedThing nm])
|
||||
_ -> pure ()
|
||||
pure (ImpNested nm)
|
||||
|
||||
checkIsModule (srcRange sigName) sigName' ASignature
|
||||
sigEnv <- lookupDefines sigName'
|
||||
|
||||
sigEnv <- lookupSigDefines nm
|
||||
let newP x = do y <- lift (newModParam me (mpName mp) loc x)
|
||||
sets_ (Map.insert y x)
|
||||
pure y
|
||||
@ -573,7 +581,7 @@ doModParam mp =
|
||||
, RenModParam
|
||||
{ renModParamName = mpName mp
|
||||
, renModParamRange = loc
|
||||
, renModParamSig = nm
|
||||
, renModParamSig = sigName'
|
||||
, renModParamInstance = nameMap
|
||||
}
|
||||
)
|
||||
@ -630,17 +638,17 @@ instance Rename TopDecl where
|
||||
|
||||
DModule m -> DModule <$> traverse rename m
|
||||
DImport li -> DImport <$> traverse renI li
|
||||
where
|
||||
renI i = do m <- rename (iModule i)
|
||||
recordImport m
|
||||
pure i { iModule = m }
|
||||
|
||||
DModParam mp -> DModParam <$> rename mp
|
||||
DModSig sig -> DModSig <$> traverse rename sig
|
||||
|
||||
renI :: ImportG (ImpName PName) -> RenameM (ImportG (ImpName Name))
|
||||
renI i = do m <- rename (iModule i)
|
||||
recordImport m
|
||||
pure i { iModule = m }
|
||||
|
||||
|
||||
instance Rename ModParam where
|
||||
rename mp =
|
||||
do x <- rnLocated (resolveName NameUse NSSignature) (mpSignature mp)
|
||||
do x <- rnLocated rename (mpSignature mp)
|
||||
depsOf (ModParamName (srcRange (mpSignature mp)) (mpName mp))
|
||||
do ren <- renModParamInstance <$> getModParam (mpName mp)
|
||||
|
||||
@ -652,22 +660,24 @@ instance Rename ModParam where
|
||||
|
||||
pure mp { mpSignature = x, mpRenaming = ren }
|
||||
|
||||
instance Rename Signature where
|
||||
rename sig =
|
||||
do let pname = thing (sigName sig)
|
||||
nm <- resolveName NameBind NSSignature pname
|
||||
env <- rmodDefines <$> lookupResolved (ImpNested nm)
|
||||
shadowNames' CheckOverlap env $
|
||||
depsOf (NamedThing nm)
|
||||
do tps <- traverse rename (sigTypeParams sig)
|
||||
cts <- traverse (traverse rename) (sigConstraints sig)
|
||||
fun <- traverse rename (sigFunParams sig)
|
||||
pure Signature
|
||||
{ sigName = (sigName sig) { thing = nm }
|
||||
, sigTypeParams = tps
|
||||
, sigConstraints = cts
|
||||
, sigFunParams = fun
|
||||
}
|
||||
renameSig :: ImpName Name -> Signature PName -> RenameM (Signature Name)
|
||||
renameSig nm sig =
|
||||
do env <- rmodDefines <$> lookupResolved nm
|
||||
let depName = case nm of
|
||||
ImpNested n -> NamedThing n
|
||||
ImpTop t -> ModPath (TopModule t)
|
||||
shadowNames' CheckOverlap env $
|
||||
depsOf depName
|
||||
do imps <- traverse (traverse renI) (sigImports sig)
|
||||
tps <- traverse rename (sigTypeParams sig)
|
||||
cts <- traverse (traverse rename) (sigConstraints sig)
|
||||
fun <- traverse rename (sigFunParams sig)
|
||||
pure Signature
|
||||
{ sigImports = imps
|
||||
, sigTypeParams = tps
|
||||
, sigConstraints = cts
|
||||
, sigFunParams = fun
|
||||
}
|
||||
|
||||
instance Rename ImpName where
|
||||
rename i =
|
||||
|
@ -56,15 +56,12 @@ data RenamerError
|
||||
| InvalidFunctorImport (ImpName Name)
|
||||
-- ^ Can't import functors directly
|
||||
|
||||
| InvalidFunctorInInstance Range (ImpName Name)
|
||||
-- ^ The instantitated thing is not a functor
|
||||
|
||||
| InvalidInstanceModule Range (ImpName Name)
|
||||
-- ^ The argument to a functor instance is not a module
|
||||
|
||||
| UnexpectedNest Range PName
|
||||
-- ^ Nested modules were not supposed to appear here
|
||||
|
||||
| ModuleKindMismatch Range (ImpName Name) ModKind ModKind
|
||||
-- ^ Exepcted one kind (first one) but found the other (second one)
|
||||
|
||||
deriving (Show, Generic, NFData, Eq, Ord)
|
||||
|
||||
|
||||
@ -92,6 +89,18 @@ depNameLoc x =
|
||||
ModPath {} -> Nothing
|
||||
|
||||
|
||||
data ModKind = AFunctor | ASignature | AModule
|
||||
deriving (Show, Generic, NFData, Eq, Ord)
|
||||
|
||||
instance PP ModKind where
|
||||
ppPrec _ e =
|
||||
case e of
|
||||
AFunctor -> "a functor"
|
||||
ASignature -> "a signatre"
|
||||
AModule -> "a module"
|
||||
|
||||
|
||||
|
||||
instance PP RenamerError where
|
||||
ppPrec _ e = case e of
|
||||
|
||||
@ -108,7 +117,6 @@ instance PP RenamerError where
|
||||
NSValue -> "Value"
|
||||
NSType -> "Type"
|
||||
NSModule -> "Module"
|
||||
NSSignature -> "Signature"
|
||||
|
||||
OverlappingSyms qns ->
|
||||
hang (text "[error]")
|
||||
@ -126,7 +134,6 @@ instance PP RenamerError where
|
||||
NSValue -> "value"
|
||||
NSType -> "type"
|
||||
NSModule -> "module"
|
||||
NSSignature -> "signature"
|
||||
suggestion =
|
||||
case (expected,actual) of
|
||||
|
||||
@ -170,16 +177,10 @@ instance PP RenamerError where
|
||||
hang ("[error] at" <+> pp s)
|
||||
4 ("submodule" <+> backticks (pp x) <+> "may not be defined here.")
|
||||
|
||||
InvalidFunctorInInstance r x ->
|
||||
ModuleKindMismatch r x expected actual ->
|
||||
hang ("[error] at" <+> pp r)
|
||||
4 (vcat [ "• Invalid functor instantiation:"
|
||||
, " " <+> backticks (pp x) <+> "is not a functor."
|
||||
])
|
||||
|
||||
InvalidInstanceModule r x ->
|
||||
hang ("[error] at" <+> pp r)
|
||||
4 (vcat [ "• Invalid functor instantiation:"
|
||||
, " " <+> backticks (pp x) <+> "is not a module."
|
||||
4 (vcat [ "• Expected" <+> pp expected
|
||||
, "•" <+> backticks (pp x) <+> "is" <+> pp actual
|
||||
])
|
||||
|
||||
|
||||
@ -192,7 +193,6 @@ instance PP DepName where
|
||||
NSModule -> "submodule" <+> pp n
|
||||
NSType -> "type" <+> pp n
|
||||
NSValue -> pp n
|
||||
NSSignature -> "signature" <+> pp n
|
||||
ModParamName _r i -> "module parameter" <+> pp i
|
||||
ModPath mp ->
|
||||
case modPathSplit mp of
|
||||
|
@ -56,7 +56,7 @@ addImplicitNestedImports' decls =
|
||||
|
||||
|
||||
processModule :: TopDecl PName -> ([TopDecl PName], [[Ident]])
|
||||
processModule ~(DModule m) =
|
||||
processModule ~dcl@(DModule m) =
|
||||
let NestedModule m1 = tlValue m
|
||||
in
|
||||
case mDef m1 of
|
||||
@ -72,10 +72,8 @@ processModule ~(DModule m) =
|
||||
Private -> []
|
||||
)
|
||||
|
||||
FunctorInstance f as is -> ([new], [])
|
||||
where
|
||||
new = DModule m { tlValue = NestedModule m1 { mDef = newDef } }
|
||||
newDef = FunctorInstance f as is
|
||||
FunctorInstance {} -> ([dcl], [])
|
||||
SignatureModule {} -> ([dcl], [])
|
||||
|
||||
|
||||
|
||||
|
@ -67,14 +67,14 @@ import Cryptol.Utils.Ident(ModName,ModPath(..),Namespace(..),OrigName(..))
|
||||
|
||||
import Cryptol.Parser.AST
|
||||
( ImportG(..),PName, ModuleInstanceArgs(..), ImpName(..) )
|
||||
import Cryptol.ModuleSystem.Binds (Mod(..), TopDef(..), modNested)
|
||||
import Cryptol.ModuleSystem.Binds (Mod(..), TopDef(..), modNested, ModKind(..))
|
||||
import Cryptol.ModuleSystem.Name
|
||||
( Name, Supply, SupplyT, runSupplyT, liftSupply, freshNameFor
|
||||
, asOrigName, nameIdent, nameTopModule )
|
||||
import Cryptol.ModuleSystem.Names(Names(..))
|
||||
import Cryptol.ModuleSystem.NamingEnv
|
||||
( NamingEnv(..), lookupNS, shadowing, travNamingEnv
|
||||
, interpImportEnv, namingEnvNames, zipByTextName, filterUNames )
|
||||
, interpImportEnv, zipByTextName, filterUNames )
|
||||
|
||||
|
||||
{- | This represents a resolved module or signaure.
|
||||
@ -103,7 +103,6 @@ data ResolvedModule imps = ResolvedModule
|
||||
it is just part of the thing we compute for local modules. -}
|
||||
}
|
||||
|
||||
data ModKind = AFunctor | ASignature | AModule
|
||||
|
||||
-- | A resolved module that's defined in (or is) the current top-level module
|
||||
type ResolvedLocal = ResolvedModule NamingEnv
|
||||
@ -195,7 +194,6 @@ todoModule = fmap (const emptyModState)
|
||||
isDone :: Todo -> Bool
|
||||
isDone m = null (modImports m) &&
|
||||
Map.null (modInstances m) &&
|
||||
Map.null (modSigs m) &&
|
||||
Map.null (modMods m)
|
||||
|
||||
|
||||
@ -234,9 +232,8 @@ forceResolveMod todo =
|
||||
ResolvedModule
|
||||
{ rmodDefines = modDefines todo
|
||||
, rmodPublic = modPublic todo
|
||||
, rmodKind = if modParams todo then AFunctor else AModule
|
||||
, rmodNested = Map.keysSet (modSigs todo) `Set.union`
|
||||
Map.keysSet (modMods todo)
|
||||
, rmodKind = modKind todo
|
||||
, rmodNested = Map.keysSet (modMods todo)
|
||||
, rmodImports = modImported (modState todo)
|
||||
}
|
||||
|
||||
@ -263,7 +260,7 @@ externalMod :: Mod () -> ResolvedExt
|
||||
externalMod m = ResolvedModule
|
||||
{ rmodDefines = modDefines m
|
||||
, rmodPublic = modPublic m
|
||||
, rmodKind = if modParams m then AFunctor else AModule
|
||||
, rmodKind = modKind m
|
||||
, rmodNested = modNested m
|
||||
, rmodImports = ()
|
||||
}
|
||||
@ -527,36 +524,15 @@ doInstancesStep s = Map.foldlWithKey' tryInstance s0 (modInstances (curMod s))
|
||||
where
|
||||
s0 = updCur s \m' -> m' { modInstances = Map.empty }
|
||||
|
||||
|
||||
-- | Generate names for signatures. This always succeeds.
|
||||
doSignaturesStep :: CurState -> CurState
|
||||
doSignaturesStep s = updCur s1 \m -> m { modSigs = mempty }
|
||||
where
|
||||
s1 = s { doneModules = Map.union resolved (doneModules s)
|
||||
, changes = not (Map.null sigs)
|
||||
}
|
||||
|
||||
sigs = modSigs (curMod s)
|
||||
resolved = doSig <$> sigs
|
||||
doSig sig = ResolvedModule
|
||||
{ rmodDefines = sig
|
||||
, rmodPublic = namingEnvNames sig -- doesn't matter
|
||||
, rmodNested = mempty
|
||||
, rmodKind = ASignature
|
||||
, rmodImports = mempty
|
||||
-- no imports in signatures, at least for now.
|
||||
}
|
||||
|
||||
tryFinishCurMod :: Todo -> CurState -> Maybe ResolvedLocal
|
||||
tryFinishCurMod m newS
|
||||
| isDone newM =
|
||||
Just ResolvedModule
|
||||
{ rmodDefines = modDefines m
|
||||
, rmodPublic = modPublic m
|
||||
, rmodKind = if modParams m then AFunctor else AModule
|
||||
, rmodKind = modKind m
|
||||
, rmodNested = Set.unions
|
||||
[ Map.keysSet (modInstances m)
|
||||
, Map.keysSet (modSigs m)
|
||||
, Map.keysSet (modMods m)
|
||||
]
|
||||
, rmodImports = modImported (modState newM)
|
||||
@ -581,7 +557,6 @@ tryModule s nm m =
|
||||
newS = doModuleStep s1
|
||||
newM = curMod newS
|
||||
|
||||
|
||||
-- | Process all submodules of a module.
|
||||
doModulesStep :: CurState -> CurState
|
||||
doModulesStep s = Map.foldlWithKey' tryModule s0 (modMods m)
|
||||
@ -597,7 +572,6 @@ doModuleStep = doStep step
|
||||
where
|
||||
step = doStep doModulesStep
|
||||
. doStep doInstancesStep
|
||||
. doStep doSignaturesStep
|
||||
. doStep doImportStep
|
||||
|
||||
|
||||
|
@ -9,6 +9,7 @@
|
||||
{-# Language RecordWildCards #-}
|
||||
{-# Language FlexibleContexts #-}
|
||||
{-# Language BlockArguments #-}
|
||||
{-# Language OverloadedStrings #-}
|
||||
module Cryptol.ModuleSystem.Renamer.Monad where
|
||||
|
||||
import Data.List(sort,foldl')
|
||||
@ -33,7 +34,7 @@ import Cryptol.Utils.Ident(modPathCommon,OrigName(..))
|
||||
|
||||
import Cryptol.ModuleSystem.Renamer.Error
|
||||
import Cryptol.ModuleSystem.Renamer.Imports
|
||||
(ResolvedLocal,rmodKind,ModKind(..),rmodDefines,rmodNested)
|
||||
(ResolvedLocal,rmodKind,rmodDefines,rmodNested)
|
||||
|
||||
-- | Indicates if a name is in a binding poisition or a use site
|
||||
data NameType = NameBind | NameUse
|
||||
@ -97,7 +98,7 @@ data RW = RW
|
||||
data RenModParam = RenModParam
|
||||
{ renModParamName :: Ident
|
||||
, renModParamRange :: Range
|
||||
, renModParamSig :: Name
|
||||
, renModParamSig :: ImpName Name
|
||||
, renModParamInstance :: Map Name Name
|
||||
{- ^ Maps names that come into scope through this parameter
|
||||
to the names in *signature*. This is for functors, NOT functor
|
||||
@ -424,8 +425,10 @@ recordImport i =
|
||||
|
||||
-- XXX: Maybe we'd want to cache some of the conversion to Mod?
|
||||
-- | This gives the loaded *external* modules.
|
||||
getLoadedModsMaybe :: RenameM (ImpName Name -> Maybe (Mod ()))
|
||||
getLoadedModsMaybe =
|
||||
-- XXX: For now, this does *not* include top-level signatures, as we have no
|
||||
-- interface type for them yet.
|
||||
getExternalModsMaybe :: RenameM (ImpName Name -> Maybe (Mod ()))
|
||||
getExternalModsMaybe =
|
||||
do getIf <- RenameM (roIfaces <$> ask)
|
||||
pure \nm ->
|
||||
case nm of
|
||||
@ -435,54 +438,44 @@ getLoadedModsMaybe =
|
||||
let mp = modToMap (ImpTop top) (ifaceToMod (getIf top)) Map.empty
|
||||
Map.lookup nm mp
|
||||
|
||||
getLoadedMods :: RenameM (ImpName Name -> Mod ())
|
||||
getLoadedMods =
|
||||
do f <- getLoadedModsMaybe
|
||||
getExternalMods :: RenameM (ImpName Name -> Mod ())
|
||||
getExternalMods =
|
||||
do f <- getExternalModsMaybe
|
||||
pure \x -> case f x of
|
||||
Just a -> a
|
||||
Nothing -> panic "getLoadedMods"
|
||||
Nothing -> panic "getExternalMods"
|
||||
[ "Module not loaded", show x ]
|
||||
|
||||
lookupModuleThing :: ImpName Name -> RenameM (Either ResolvedLocal (Mod ()))
|
||||
lookupModuleThing nm =
|
||||
do ro <- RenameM ask
|
||||
traceM (unlines ("RESOLVED:" : [ show (pp k <+> pp (rmodKind v)) | (k,v) <- Map.toList (roResolvedModules ro) ]))
|
||||
case Map.lookup nm (roResolvedModules ro) of
|
||||
Just loc -> pure (Left loc)
|
||||
Nothing ->
|
||||
do loaded <- getExternalMods
|
||||
pure (Right (loaded nm))
|
||||
|
||||
lookupDefines :: ImpName Name -> RenameM NamingEnv
|
||||
lookupDefines nm =
|
||||
do thing <- lookupModuleThing nm
|
||||
pure case thing of
|
||||
Left loc -> rmodDefines (dump "resolved" rmodKind loc)
|
||||
Right e -> modDefines (dump "external" modKind e)
|
||||
where
|
||||
dump msg f d = trace (show ("lookup defines: " <+> msg <+> pp nm <+> pp (f d))) d
|
||||
|
||||
checkIsModule :: Range -> ImpName Name -> ModKind -> RenameM ()
|
||||
checkIsModule r nm expect =
|
||||
do ro <- RenameM ask
|
||||
case Map.lookup nm (roResolvedModules ro) of
|
||||
Just loc -> pure (rmodDefines loc)
|
||||
Nothing ->
|
||||
do loaded <- getLoadedMods
|
||||
pure (modDefines (loaded nm))
|
||||
actual <- case Map.lookup nm (roResolvedModules ro) of
|
||||
Just loc -> pure (rmodKind loc)
|
||||
Nothing ->
|
||||
do loaded <- getExternalMods
|
||||
pure (modKind (loaded nm))
|
||||
|
||||
lookupSigDefines :: Name -> RenameM NamingEnv
|
||||
lookupSigDefines nm =
|
||||
do ro <- RenameM ask
|
||||
case Map.lookup (ImpNested nm) (roResolvedModules ro) of
|
||||
Just loc -> pure (rmodDefines loc)
|
||||
Nothing ->
|
||||
do getIf <- RenameM (roIfaces <$> ask)
|
||||
let top = nameTopModule nm
|
||||
sigs = ifSignatures (ifPublic (getIf top))
|
||||
case Map.lookup nm sigs of
|
||||
Just s -> pure (modParamsNamingEnv s)
|
||||
Nothing ->
|
||||
panic "lookupSigDefines" [ "Missing signature "<> show nm]
|
||||
|
||||
|
||||
|
||||
|
||||
checkIsModule :: Range -> ImpName Name -> RenameM ()
|
||||
checkIsModule r nm =
|
||||
do ro <- RenameM ask
|
||||
case Map.lookup nm (roResolvedModules ro) of
|
||||
Just loc ->
|
||||
case rmodKind loc of
|
||||
AModule -> pure ()
|
||||
_ -> recordError (InvalidInstanceModule r nm)
|
||||
Nothing ->
|
||||
do mb <- ($ nm) <$> getLoadedModsMaybe
|
||||
case mb of
|
||||
Nothing -> pure ()
|
||||
Just m ->
|
||||
when (modParams m) (recordError (InvalidInstanceModule r nm))
|
||||
unless (actual == expect)
|
||||
(recordError (ModuleKindMismatch r nm expect actual))
|
||||
|
||||
lookupDefinesAndSubs ::
|
||||
Maybe Range -> ImpName Name -> RenameM (NamingEnv, Set Name)
|
||||
@ -495,24 +488,25 @@ lookupDefinesAndSubs checkFun nm =
|
||||
Just r ->
|
||||
case rmodKind loc of
|
||||
AFunctor -> pure ()
|
||||
_ -> recordError (InvalidFunctorInInstance r nm)
|
||||
k -> recordError (ModuleKindMismatch r nm AFunctor k)
|
||||
Nothing -> pure ()
|
||||
|
||||
pure (rmodDefines loc, rmodNested loc)
|
||||
|
||||
Nothing ->
|
||||
do mb <- ($ nm) <$> getLoadedModsMaybe
|
||||
do mb <- ($ nm) <$> getExternalModsMaybe
|
||||
case mb of
|
||||
Nothing -> pure ( mempty, Set.empty )
|
||||
Just m ->
|
||||
do case checkFun of
|
||||
Just r -> unless (modParams m)
|
||||
(recordError (InvalidFunctorInInstance r nm))
|
||||
Just r ->
|
||||
case modKind m of
|
||||
AFunctor -> pure ()
|
||||
k -> recordError (ModuleKindMismatch r nm AFunctor k)
|
||||
Nothing -> pure ()
|
||||
|
||||
pure ( modDefines m
|
||||
, Set.unions [ Map.keysSet (modMods m)
|
||||
, Map.keysSet (modSigs m)
|
||||
, Map.keysSet (modInstances m)
|
||||
]
|
||||
)
|
||||
|
@ -200,6 +200,13 @@ vmod_body :: { [TopDecl PName] }
|
||||
| {- empty -} { [] }
|
||||
|
||||
|
||||
|
||||
-- inverted
|
||||
imports1 :: { [ Located (ImportG (ImpName PName)) ] }
|
||||
: imports1 'v;' import { $3 : $1 }
|
||||
| imports1 ';' import { $3 : $1 }
|
||||
| import { [$1] }
|
||||
|
||||
-- XXX replace rComb with uses of at
|
||||
import :: { Located (ImportG (ImpName PName)) }
|
||||
: 'import' impName mbAs mbImportSpec
|
||||
@ -280,14 +287,20 @@ vtop_decl :: { [TopDecl PName] }
|
||||
-- we allow for documentation here to avoid conflicts with module paramaters
|
||||
-- currently that odcumentation is just discarded
|
||||
|
||||
sig_def :: { Signature PName }
|
||||
: 'signature' name 'where' 'v{' par_decls 'v}'
|
||||
{ mkSignature $2 $5 }
|
||||
sig_def :: { (Located PName, Signature PName) }
|
||||
: 'signature' name 'where' 'v{' sig_body 'v}'
|
||||
{ ($2, $5) }
|
||||
|
||||
sig_body :: { Signature PName }
|
||||
: par_decls { mkSignature [] $1 }
|
||||
| imports1 'v;' par_decls { mkSignature (reverse $1) $3 }
|
||||
| imports1 ';' par_decls { mkSignature (reverse $1) $3 }
|
||||
|
||||
|
||||
mod_param_decl :: { ModParam PName }
|
||||
: mbDoc
|
||||
'import' 'signature'
|
||||
name mbAs { ModParam { mpSignature = $4
|
||||
impName mbAs { ModParam { mpSignature = $4
|
||||
, mpAs = fmap thing $5
|
||||
, mpName = mkModParamName $4 $5
|
||||
, mpDoc = $1
|
||||
|
@ -111,7 +111,7 @@ import Data.Map(Map)
|
||||
import qualified Data.Map as Map
|
||||
import Data.List(intersperse)
|
||||
import Data.Bits(shiftR)
|
||||
import Data.Maybe (catMaybes)
|
||||
import Data.Maybe (catMaybes,mapMaybe)
|
||||
import Data.Ratio(numerator,denominator)
|
||||
import Data.Text (Text)
|
||||
import Numeric(showIntAtBase,showFloat,showHFloat)
|
||||
@ -152,6 +152,7 @@ data ModuleDefinition name =
|
||||
(ModuleInstanceArgs name)
|
||||
(ModuleInstance name)
|
||||
-- ^ The instance is filled in by the renamer
|
||||
| SignatureModule (Signature name)
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
{- | Maps names in the original functor with names in the instnace.
|
||||
@ -171,15 +172,22 @@ mDecls m =
|
||||
case mDef m of
|
||||
NormalModule ds -> ds
|
||||
FunctorInstance _ _ _ -> []
|
||||
SignatureModule {} -> []
|
||||
|
||||
-- | Imports of top-level (i.e. "file" based) modules.
|
||||
mImports :: ModuleG mname name -> [ Located Import ]
|
||||
mImports m =
|
||||
[ li { thing = i { iModule = n } }
|
||||
| DImport li <- mDecls m
|
||||
, let i = thing li
|
||||
, ImpTop n <- [iModule i]
|
||||
]
|
||||
case mDef m of
|
||||
NormalModule ds -> mapMaybe topImp [ li | DImport li <- ds ]
|
||||
FunctorInstance {} -> []
|
||||
SignatureModule sig -> mapMaybe topImp (sigImports sig)
|
||||
where
|
||||
topImp li = case iModule i of
|
||||
ImpTop n -> Just li { thing = i { iModule = n } }
|
||||
_ -> Nothing
|
||||
where i = thing li
|
||||
|
||||
|
||||
|
||||
-- | Imports of nested modules---these may require name resolution to
|
||||
-- detrmine what module we are talking about.
|
||||
@ -243,7 +251,6 @@ data TopDecl name =
|
||||
|
||||
| DModule (TopLevel (NestedModule name)) -- ^ @submodule M where ...@
|
||||
| DImport (Located (ImportG (ImpName name))) -- ^ @import X@
|
||||
| DModSig (TopLevel (Signature name)) -- ^ @signature X where ...@
|
||||
| DModParam (ModParam name) -- ^ @import signature X ...@
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
@ -314,7 +321,8 @@ other members of a signature. When a signature is "imported" as a functor
|
||||
parameter these names are instantiated to new names, because there could
|
||||
be multiple paramers using the same signature. -}
|
||||
data Signature name = Signature
|
||||
{ sigName :: Located name -- ^ Name of the signature
|
||||
{ sigImports :: ![Located (ImportG (ImpName name))]
|
||||
-- ^ Add things in scope
|
||||
, sigTypeParams :: [ParameterType name] -- ^ Type parameters
|
||||
, sigConstraints :: [Located (Prop name)] -- ^ Constraints on type params
|
||||
, sigFunParams :: [ParameterFun name] -- ^ Value parameters
|
||||
@ -332,7 +340,7 @@ If there is no `as` clause, then the type/value parameters are unqualified,
|
||||
and otherwise they are qualified.
|
||||
-}
|
||||
data ModParam name = ModParam
|
||||
{ mpSignature :: Located name -- ^ Signature for parameter
|
||||
{ mpSignature :: Located (ImpName name) -- ^ Signature for parameter
|
||||
, mpAs :: Maybe ModName -- ^ Qualified for actual params
|
||||
, mpName :: !Ident
|
||||
{- ^ Parameter name (for inst.)
|
||||
@ -668,15 +676,11 @@ instance HasLoc (TopDecl name) where
|
||||
DParameterConstraint d -> getLoc d
|
||||
DModule d -> getLoc d
|
||||
DImport d -> getLoc d
|
||||
DModSig d -> getLoc d
|
||||
DModParam d -> getLoc d
|
||||
|
||||
instance HasLoc (ModParam name) where
|
||||
getLoc mp = getLoc (mpSignature mp)
|
||||
|
||||
instance HasLoc (Signature name) where
|
||||
getLoc = getLoc . sigName
|
||||
|
||||
instance HasLoc (PrimType name) where
|
||||
getLoc pt = Just (rComb (srcRange (primTName pt)) (srcRange (primTKind pt)))
|
||||
|
||||
@ -736,7 +740,11 @@ instance (Show name, PPName name) => PP (NestedModule name) where
|
||||
|
||||
ppModule :: (Show name, PPName mname, PPName name) =>
|
||||
Doc -> ModuleG mname name -> Doc
|
||||
ppModule kw m = kw <+> ppL (mName m) <+> pp (mDef m)
|
||||
ppModule kw m = kw' <+> ppL (mName m) <+> pp (mDef m)
|
||||
where
|
||||
kw' = case mDef m of
|
||||
SignatureModule {} -> "parameter" <+> kw
|
||||
_ -> kw
|
||||
|
||||
|
||||
instance (Show name, PPName name) => PP (ModuleDefinition name) where
|
||||
@ -753,6 +761,7 @@ instance (Show name, PPName name) => PP (ModuleDefinition name) where
|
||||
]
|
||||
instLines = [ " *" <+> pp k <+> "->" <+> pp v
|
||||
| (k,v) <- Map.toList inst ]
|
||||
SignatureModule s -> pp s
|
||||
|
||||
|
||||
instance (Show name, PPName name) => PP (ModuleInstanceArgs name) where
|
||||
@ -785,22 +794,18 @@ instance (Show name, PPName name) => PP (TopDecl name) where
|
||||
xs -> nest 1 (parens (commaSepFill xs))
|
||||
DModule d -> pp d
|
||||
DImport i -> pp (thing i)
|
||||
DModSig s -> pp s
|
||||
DModParam s -> pp s
|
||||
|
||||
instance (Show name, PPName name) => PP (Signature name) where
|
||||
ppPrec _ = ppSignature "signature"
|
||||
|
||||
ppSignature :: (Show name, PPName name) => Doc -> Signature name -> Doc
|
||||
ppSignature kw sig = (kw <+> pp (thing (sigName sig)) <+> "where")
|
||||
$$ indent 2 (vcat ds)
|
||||
where
|
||||
ds = map pp (sigTypeParams sig)
|
||||
++ case map (pp . thing) (sigConstraints sig) of
|
||||
[x] -> ["type constraint" <+> x]
|
||||
[] -> []
|
||||
xs -> ["type constraint" <+> parens (commaSep xs)]
|
||||
++ map pp (sigFunParams sig)
|
||||
ppPrec _ sig = "where" $$ indent 2 (vcat (is ++ ds))
|
||||
where
|
||||
is = map pp (sigImports sig)
|
||||
ds = map pp (sigTypeParams sig)
|
||||
++ case map (pp . thing) (sigConstraints sig) of
|
||||
[x] -> ["type constraint" <+> x]
|
||||
[] -> []
|
||||
xs -> ["type constraint" <+> parens (commaSep xs)]
|
||||
++ map pp (sigFunParams sig)
|
||||
|
||||
|
||||
instance (Show name, PPName name) => PP (ModParam name) where
|
||||
@ -1207,6 +1212,7 @@ instance NoPos (ModuleDefinition name) where
|
||||
case m of
|
||||
NormalModule ds -> NormalModule (noPos ds)
|
||||
FunctorInstance f as ds -> FunctorInstance (noPos f) (noPos as) ds
|
||||
SignatureModule s -> SignatureModule (noPos s)
|
||||
|
||||
instance NoPos (ModuleInstanceArgs name) where
|
||||
noPos as =
|
||||
@ -1233,11 +1239,10 @@ instance NoPos (TopDecl name) where
|
||||
DParameterConstraint d -> DParameterConstraint (noPos d)
|
||||
DModule d -> DModule (noPos d)
|
||||
DImport d -> DImport (noPos d)
|
||||
DModSig d -> DModSig (noPos d)
|
||||
DModParam d -> DModParam (noPos d)
|
||||
|
||||
instance NoPos (Signature name) where
|
||||
noPos sig = Signature { sigName = noPos (sigName sig)
|
||||
noPos sig = Signature { sigImports = sigImports sig
|
||||
, sigTypeParams = map noPos (sigTypeParams sig)
|
||||
, sigConstraints = map noPos (sigConstraints sig)
|
||||
, sigFunParams = map noPos (sigFunParams sig)
|
||||
|
@ -166,6 +166,7 @@ noIncludeModule m =
|
||||
do newDef <- case mDef m of
|
||||
NormalModule ds -> NormalModule <$> doDecls ds
|
||||
FunctorInstance f as is -> pure (FunctorInstance f as is)
|
||||
SignatureModule s -> pure (SignatureModule s)
|
||||
pure m { mDef = newDef }
|
||||
where
|
||||
doDecls = fmap concat . collectErrors noIncTopDecl
|
||||
@ -192,7 +193,6 @@ noIncTopDecl td = case td of
|
||||
do m1 <- noIncludeModule m
|
||||
pure [ DModule tl { tlValue = NestedModule m1 } ]
|
||||
DImport {} -> pure [td]
|
||||
DModSig {} -> pure [td]
|
||||
DModParam {} -> pure [td]
|
||||
|
||||
-- | Resolve the file referenced by a include into a list of top-level
|
||||
|
@ -339,6 +339,7 @@ noPatModule m =
|
||||
case mDef m of
|
||||
NormalModule ds -> NormalModule <$> noPatTopDs ds
|
||||
FunctorInstance f as i -> pure (FunctorInstance f as i)
|
||||
SignatureModule s -> pure (SignatureModule s)
|
||||
pure m { mDef = def }
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
@ -392,7 +393,6 @@ annotTopDs tds =
|
||||
|
||||
DImport {} -> (d :) <$> annotTopDs ds
|
||||
|
||||
DModSig {} -> (d :) <$> annotTopDs ds
|
||||
DModParam {} -> (d :) <$> annotTopDs ds
|
||||
|
||||
[] -> return []
|
||||
|
@ -197,14 +197,17 @@ mkModName = packModName
|
||||
|
||||
-- | This is how we derive the name of a module parameter from the
|
||||
-- @import source@ declaration.
|
||||
mkModParamName :: Located PName -> Maybe (Located ModName) -> Ident
|
||||
mkModParamName :: Located (ImpName PName) -> Maybe (Located ModName) -> Ident
|
||||
mkModParamName lsig qual =
|
||||
case qual of
|
||||
Nothing ->
|
||||
case thing lsig of
|
||||
UnQual i -> i
|
||||
Qual _ i -> i
|
||||
NewName {} -> panic "mkModParamName" ["Unexpected NewName",show lsig]
|
||||
ImpTop t -> packIdent (last (modNameChunks t))
|
||||
ImpNested nm ->
|
||||
case nm of
|
||||
UnQual i -> i
|
||||
Qual _ i -> i
|
||||
NewName {} -> panic "mkModParamName" ["Unexpected NewName",show lsig]
|
||||
Just m -> packIdent (last (modNameChunks (thing m)))
|
||||
|
||||
-- Note that type variables are not resolved at this point: they are tcons.
|
||||
@ -531,7 +534,6 @@ changeExport e = map change
|
||||
DPrimType t -> DPrimType t { tlExport = e }
|
||||
TDNewtype n -> TDNewtype n { tlExport = e }
|
||||
DModule m -> DModule m { tlExport = e }
|
||||
DModSig s -> DModSig s { tlExport = e }
|
||||
DModParam {} -> decl
|
||||
Include{} -> decl
|
||||
DImport{} -> decl
|
||||
@ -825,18 +827,22 @@ mkNested m =
|
||||
nm = mName m
|
||||
r = srcRange nm
|
||||
|
||||
mkSigDecl :: Maybe (Located Text) -> Signature PName -> TopDecl PName
|
||||
mkSigDecl doc sig =
|
||||
DModSig
|
||||
mkSigDecl :: Maybe (Located Text) -> (Located PName,Signature PName) -> TopDecl PName
|
||||
mkSigDecl doc (nm,sig) =
|
||||
DModule
|
||||
TopLevel { tlExport = Public
|
||||
, tlDoc = doc
|
||||
, tlValue = sig
|
||||
, tlValue = NestedModule
|
||||
Module { mName = nm
|
||||
, mDef = SignatureModule sig
|
||||
}
|
||||
}
|
||||
|
||||
mkSignature :: LPName -> [TopDecl PName] -> Signature PName
|
||||
mkSignature nm =
|
||||
mkSignature :: [Located (ImportG (ImpName PName))] ->
|
||||
[TopDecl PName] -> Signature PName
|
||||
mkSignature is =
|
||||
foldl' add
|
||||
Signature { sigName = nm
|
||||
Signature { sigImports = is
|
||||
, sigTypeParams = []
|
||||
, sigConstraints = []
|
||||
, sigFunParams = []
|
||||
@ -990,12 +996,15 @@ mkModBody = collect 1 [] []
|
||||
|
||||
|
||||
anonSig l ts fs =
|
||||
panic "anonSig" ["XXX"]
|
||||
{-
|
||||
let nm = Located { srcRange = l, thing = mkUnqual anonymousSignatureIdent }
|
||||
in [ DModSig
|
||||
TopLevel
|
||||
{ tlExport = Private
|
||||
, tlDoc = Nothing
|
||||
, tlValue = Signature { sigName = nm
|
||||
, sigImports = [] -- XXX: what to do here
|
||||
, sigTypeParams = ts
|
||||
, sigConstraints = []
|
||||
, sigFunParams = fs
|
||||
@ -1011,7 +1020,7 @@ mkModBody = collect 1 [] []
|
||||
, mpRenaming = mempty
|
||||
}
|
||||
]
|
||||
|
||||
-}
|
||||
|
||||
|
||||
|
||||
|
@ -35,17 +35,15 @@ helpForNamed qname =
|
||||
vNames = M.lookupListNS M.NSValue qname rnEnv
|
||||
tNames = M.lookupListNS M.NSType qname rnEnv
|
||||
mNames = M.lookupListNS M.NSModule qname rnEnv
|
||||
sNames = M.lookupListNS M.NSSignature qname rnEnv
|
||||
|
||||
let helps = map (showTypeHelp params env disp) tNames ++
|
||||
map (showValHelp params env disp qname) vNames ++
|
||||
map (showModHelp env disp) mNames ++
|
||||
map (showSigHelp env disp) sNames
|
||||
map (showModHelp env disp) mNames
|
||||
|
||||
separ = rPutStrLn " ---------"
|
||||
sequence_ (intersperse separ helps)
|
||||
|
||||
when (null (vNames ++ tNames ++ mNames ++ sNames)) $
|
||||
when (null (vNames ++ tNames ++ mNames)) $
|
||||
rPrint $ "Undefined name:" <+> pp qname
|
||||
|
||||
|
||||
|
@ -499,7 +499,6 @@ instance PP (WithNames Error) where
|
||||
NSValue -> "value"
|
||||
NSType -> "type"
|
||||
NSModule -> "module"
|
||||
NSSignature -> "signature"
|
||||
|
||||
TemporaryError doc -> doc
|
||||
where
|
||||
|
@ -1088,25 +1088,25 @@ checkTopDecls = mapM_ checkTopDecl
|
||||
do _ <- doFunctorInst (P.ImpNested <$> P.mName m) f as inst
|
||||
pure ()
|
||||
|
||||
P.SignatureModule sig ->
|
||||
do let doc = P.thing <$> P.tlDoc tl
|
||||
inRange (srcRange (P.mName m))
|
||||
do newSignatureScope (thing (P.mName m)) doc
|
||||
|
||||
forM_ (P.sigTypeParams sig) \pt ->
|
||||
addParamType =<< checkParameterType pt
|
||||
|
||||
addParameterConstraints =<<
|
||||
checkParameterConstraints (P.sigConstraints sig)
|
||||
|
||||
forM_ (P.sigFunParams sig) \f ->
|
||||
addParamFun =<< checkParameterFun f
|
||||
|
||||
endSignature
|
||||
|
||||
|
||||
where P.NestedModule m = P.tlValue tl
|
||||
|
||||
P.DModSig tl ->
|
||||
do let sig = P.tlValue tl
|
||||
doc = P.thing <$> P.tlDoc tl
|
||||
inRange (srcRange (P.sigName sig))
|
||||
do newSignatureScope (thing (P.sigName sig)) doc
|
||||
|
||||
forM_ (P.sigTypeParams sig) \pt ->
|
||||
addParamType =<< checkParameterType pt
|
||||
|
||||
addParameterConstraints =<<
|
||||
checkParameterConstraints (P.sigConstraints sig)
|
||||
|
||||
forM_ (P.sigFunParams sig) \f ->
|
||||
addParamFun =<< checkParameterFun f
|
||||
|
||||
endSignature
|
||||
|
||||
P.DModParam p ->
|
||||
inRange (srcRange (P.mpSignature p))
|
||||
do let binds = P.mpRenaming p
|
||||
|
@ -10,6 +10,7 @@ import Cryptol.Parser.Position(Located)
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
(IfaceParams(..), IfaceNames(..), IfaceModParam(..))
|
||||
import Cryptol.IR.TraverseNames(TraverseNames,mapNames)
|
||||
import Cryptol.Parser.AST(ImpName(..))
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Subst(Subst,TVars,apSubst)
|
||||
|
||||
@ -52,6 +53,12 @@ instance ModuleInstance a => ModuleInstance (Located a) where
|
||||
instance ModuleInstance Name where
|
||||
moduleInstance = doVInst
|
||||
|
||||
instance ModuleInstance name => ModuleInstance (ImpName name) where
|
||||
moduleInstance x =
|
||||
case x of
|
||||
ImpTop t -> ImpTop t
|
||||
ImpNested n -> ImpNested (moduleInstance n)
|
||||
|
||||
instance ModuleInstance (ModuleG name) where
|
||||
moduleInstance m =
|
||||
Module { mName = mName m
|
||||
|
@ -699,13 +699,16 @@ lookupAbstractType x = Map.lookup x <$> getAbstractTypes
|
||||
lookupParamType :: Name -> InferM (Maybe ModTParam)
|
||||
lookupParamType x = Map.lookup x <$> getParamTypes
|
||||
|
||||
lookupSignature :: Name -> InferM If.IfaceParams
|
||||
lookupSignature x =
|
||||
do sigs <- getSignatures
|
||||
case Map.lookup x sigs of
|
||||
Just ips -> pure ips
|
||||
Nothing -> panic "lookupSignature"
|
||||
[ "Missing signature", show x ]
|
||||
lookupSignature :: P.ImpName Name -> InferM If.IfaceParams
|
||||
lookupSignature nx =
|
||||
case nx of
|
||||
-- XXX: top
|
||||
P.ImpNested x ->
|
||||
do sigs <- getSignatures
|
||||
case Map.lookup x sigs of
|
||||
Just ips -> pure ips
|
||||
Nothing -> panic "lookupSignature"
|
||||
[ "Missing signature", show x ]
|
||||
|
||||
-- | Lookup an external (i.e., previously loaded) top module.
|
||||
lookupTopModule :: ModName -> InferM (Maybe (ModuleG (), If.IfaceG ()))
|
||||
|
@ -32,6 +32,7 @@ module Cryptol.Utils.Ident
|
||||
, noModuleName
|
||||
, exprModName
|
||||
, modNameArg
|
||||
, modNameSig
|
||||
|
||||
, isParamInstModName
|
||||
, paramInstModName
|
||||
@ -81,7 +82,7 @@ import Cryptol.Utils.Panic(panic)
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- | Namespaces for names
|
||||
data Namespace = NSValue | NSType | NSModule | NSSignature
|
||||
data Namespace = NSValue | NSType | NSModule
|
||||
deriving (Generic,Show,NFData,Eq,Ord,Enum,Bounded)
|
||||
|
||||
allNamespaces :: [Namespace]
|
||||
@ -139,7 +140,7 @@ modPathSplit p0 = (top,reverse xs)
|
||||
data ModName = ModName T.Text ModNameFlavor
|
||||
deriving (Eq,Ord,Show,Generic)
|
||||
|
||||
data ModNameFlavor = NormalModName | AnonModArgName
|
||||
data ModNameFlavor = NormalModName | AnonModArgName | AnonSigName
|
||||
deriving (Eq,Ord,Show,Generic)
|
||||
|
||||
instance NFData ModName
|
||||
@ -148,14 +149,25 @@ instance NFData ModNameFlavor
|
||||
modNameArg :: ModName -> ModName
|
||||
modNameArg (ModName m fl) =
|
||||
case fl of
|
||||
NormalModName -> ModName m AnonModArgName
|
||||
AnonModArgName -> panic "modNameArg" ["Name is already an argument"]
|
||||
NormalModName -> ModName m AnonModArgName
|
||||
AnonModArgName -> panic "modNameArg" ["Name is not normal"]
|
||||
AnonSigName -> panic "modNameArg" ["Name is not normal"]
|
||||
|
||||
modNameSig :: ModName -> ModName
|
||||
modNameSig (ModName m fl) =
|
||||
case fl of
|
||||
NormalModName -> ModName m AnonSigName
|
||||
AnonModArgName -> panic "modNameSig" ["Name is not normal"]
|
||||
AnonSigName -> panic "modNameSig" ["Name is not normal"]
|
||||
|
||||
|
||||
|
||||
modNameToText :: ModName -> T.Text
|
||||
modNameToText (ModName x fl) =
|
||||
case fl of
|
||||
NormalModName -> x
|
||||
AnonModArgName -> x <> "$argument"
|
||||
AnonSigName -> x <> "$signature"
|
||||
|
||||
textToModName :: T.Text -> ModName
|
||||
textToModName txt = ModName txt NormalModName
|
||||
|
@ -420,4 +420,3 @@ instance PP Namespace where
|
||||
NSValue -> "/*value*/"
|
||||
NSType -> "/*type*/"
|
||||
NSModule -> "/*module*/"
|
||||
NSSignature -> "/*signature*/"
|
||||
|
@ -4,7 +4,7 @@ signature A where
|
||||
x : [n]
|
||||
|
||||
submodule F where
|
||||
import signature A
|
||||
import signature submodule A
|
||||
|
||||
y : [n]
|
||||
y = 1 + x
|
||||
|
@ -4,7 +4,7 @@ signature A where
|
||||
x : [n]
|
||||
|
||||
submodule F where
|
||||
import signature A
|
||||
import parameter A
|
||||
|
||||
y : [n]
|
||||
y = 1 + x
|
||||
|
Loading…
Reference in New Issue
Block a user