From 5578437e2c1e00b4897b56c6544b291a30de9b1e Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 6 Jun 2022 14:46:54 -0700 Subject: [PATCH] Checkpoing: make signatures into a special kind of module. Still need to refactor interfaces to account for top-level signatures --- src/Cryptol/ModuleSystem/Base.hs | 45 +++++---- src/Cryptol/ModuleSystem/Binds.hs | 81 +++++++++------- src/Cryptol/ModuleSystem/Exports.hs | 2 - src/Cryptol/ModuleSystem/Interface.hs | 6 +- src/Cryptol/ModuleSystem/Monad.hs | 3 + src/Cryptol/ModuleSystem/NamingEnv.hs | 2 +- src/Cryptol/ModuleSystem/Renamer.hs | 86 +++++++++-------- src/Cryptol/ModuleSystem/Renamer/Error.hs | 36 ++++---- .../ModuleSystem/Renamer/ImplicitImports.hs | 8 +- src/Cryptol/ModuleSystem/Renamer/Imports.hs | 38 ++------ src/Cryptol/ModuleSystem/Renamer/Monad.hs | 92 +++++++++---------- src/Cryptol/Parser.y | 21 ++++- src/Cryptol/Parser/AST.hs | 63 +++++++------ src/Cryptol/Parser/NoInclude.hs | 2 +- src/Cryptol/Parser/NoPat.hs | 2 +- src/Cryptol/Parser/ParserUtils.hs | 35 ++++--- src/Cryptol/REPL/Help.hs | 6 +- src/Cryptol/TypeCheck/Error.hs | 1 - src/Cryptol/TypeCheck/Infer.hs | 34 +++---- src/Cryptol/TypeCheck/ModuleInstance.hs | 7 ++ src/Cryptol/TypeCheck/Monad.hs | 17 ++-- src/Cryptol/Utils/Ident.hs | 20 +++- src/Cryptol/Utils/PP.hs | 1 - tests/modsys/functors/T001.cry | 2 +- tests/modsys/functors/T002.cry | 2 +- 25 files changed, 328 insertions(+), 284 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 674e76e2..2a36f7ef 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -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 () diff --git a/src/Cryptol/ModuleSystem/Binds.hs b/src/Cryptol/ModuleSystem/Binds.hs index 05ce1947..7f6c163f 100644 --- a/src/Cryptol/ModuleSystem/Binds.hs +++ b/src/Cryptol/ModuleSystem/Binds.hs @@ -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 $ diff --git a/src/Cryptol/ModuleSystem/Exports.hs b/src/Cryptol/ModuleSystem/Exports.hs index ac6075d8..b5b1f12a 100644 --- a/src/Cryptol/ModuleSystem/Exports.hs +++ b/src/Cryptol/ModuleSystem/Exports.hs @@ -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)) ] diff --git a/src/Cryptol/ModuleSystem/Interface.hs b/src/Cryptol/ModuleSystem/Interface.hs index 0ce2dc1a..9a3a9d29 100644 --- a/src/Cryptol/ModuleSystem/Interface.hs +++ b/src/Cryptol/ModuleSystem/Interface.hs @@ -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 diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index 03469f75..0e11cf68 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -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 diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index badcf056..eed1cbf3 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -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 ] diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 412e9dad..e0c4d250 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -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 = diff --git a/src/Cryptol/ModuleSystem/Renamer/Error.hs b/src/Cryptol/ModuleSystem/Renamer/Error.hs index fef03e6a..a49d49f4 100644 --- a/src/Cryptol/ModuleSystem/Renamer/Error.hs +++ b/src/Cryptol/ModuleSystem/Renamer/Error.hs @@ -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 diff --git a/src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs b/src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs index 40d2228a..6b148acd 100644 --- a/src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs +++ b/src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs @@ -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], []) diff --git a/src/Cryptol/ModuleSystem/Renamer/Imports.hs b/src/Cryptol/ModuleSystem/Renamer/Imports.hs index f3c9802b..3f37a550 100644 --- a/src/Cryptol/ModuleSystem/Renamer/Imports.hs +++ b/src/Cryptol/ModuleSystem/Renamer/Imports.hs @@ -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 diff --git a/src/Cryptol/ModuleSystem/Renamer/Monad.hs b/src/Cryptol/ModuleSystem/Renamer/Monad.hs index 699ebd16..d4a92d3e 100644 --- a/src/Cryptol/ModuleSystem/Renamer/Monad.hs +++ b/src/Cryptol/ModuleSystem/Renamer/Monad.hs @@ -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) ] ) diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index b8264bd0..2f89cad6 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -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 diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 17eba818..75770cd5 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -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) diff --git a/src/Cryptol/Parser/NoInclude.hs b/src/Cryptol/Parser/NoInclude.hs index 3970e3c9..0e2cac58 100644 --- a/src/Cryptol/Parser/NoInclude.hs +++ b/src/Cryptol/Parser/NoInclude.hs @@ -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 diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs index 7fbed46b..8ba23cc2 100644 --- a/src/Cryptol/Parser/NoPat.hs +++ b/src/Cryptol/Parser/NoPat.hs @@ -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 [] diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index 78e14e9b..a8e27439 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -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 } ] - +-} diff --git a/src/Cryptol/REPL/Help.hs b/src/Cryptol/REPL/Help.hs index b6064141..0490e21b 100644 --- a/src/Cryptol/REPL/Help.hs +++ b/src/Cryptol/REPL/Help.hs @@ -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 diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index 1357b8cc..f4cceb3d 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -499,7 +499,6 @@ instance PP (WithNames Error) where NSValue -> "value" NSType -> "type" NSModule -> "module" - NSSignature -> "signature" TemporaryError doc -> doc where diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 64df0638..e7f786ff 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -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 diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs index 13945c7d..2c252cf0 100644 --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -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 diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index 53a1ecb4..ff405ea5 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -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 ())) diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs index d9f2d746..4a431032 100644 --- a/src/Cryptol/Utils/Ident.hs +++ b/src/Cryptol/Utils/Ident.hs @@ -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 diff --git a/src/Cryptol/Utils/PP.hs b/src/Cryptol/Utils/PP.hs index 1f2c8414..1ab9979e 100644 --- a/src/Cryptol/Utils/PP.hs +++ b/src/Cryptol/Utils/PP.hs @@ -420,4 +420,3 @@ instance PP Namespace where NSValue -> "/*value*/" NSType -> "/*type*/" NSModule -> "/*module*/" - NSSignature -> "/*signature*/" diff --git a/tests/modsys/functors/T001.cry b/tests/modsys/functors/T001.cry index 9cced4b5..9580500a 100644 --- a/tests/modsys/functors/T001.cry +++ b/tests/modsys/functors/T001.cry @@ -4,7 +4,7 @@ signature A where x : [n] submodule F where - import signature A + import signature submodule A y : [n] y = 1 + x diff --git a/tests/modsys/functors/T002.cry b/tests/modsys/functors/T002.cry index 9f872054..deea6fcb 100644 --- a/tests/modsys/functors/T002.cry +++ b/tests/modsys/functors/T002.cry @@ -4,7 +4,7 @@ signature A where x : [n] submodule F where - import signature A + import parameter A y : [n] y = 1 + x