From 9b3ab473195c9702a86a52550cfd3bb401e4cb64 Mon Sep 17 00:00:00 2001 From: Bretton Date: Fri, 28 Jul 2023 18:01:51 -0700 Subject: [PATCH 01/17] Add functor in-scope info to its instantiations --- cryptol.cabal | 1 + src/Cryptol/ModuleSystem/Base.hs | 6 ++- src/Cryptol/ModuleSystem/Interface.hs | 3 ++ src/Cryptol/ModuleSystem/NamingEnv.hs | 30 +++----------- src/Cryptol/ModuleSystem/NamingEnv/Types.hs | 34 ++++++++++++++++ src/Cryptol/ModuleSystem/Renamer.hs | 44 +++++++-------------- src/Cryptol/Parser/AST.hs | 8 ++++ src/Cryptol/Parser/ParserUtils.hs | 32 +++++++++------ src/Cryptol/TypeCheck/AST.hs | 7 ++++ src/Cryptol/TypeCheck/Infer.hs | 9 +++-- src/Cryptol/TypeCheck/Interface.hs | 1 + src/Cryptol/TypeCheck/Module.hs | 10 +++-- src/Cryptol/TypeCheck/ModuleInstance.hs | 6 +++ src/Cryptol/TypeCheck/Monad.hs | 16 +++++--- 14 files changed, 127 insertions(+), 80 deletions(-) create mode 100644 src/Cryptol/ModuleSystem/NamingEnv/Types.hs diff --git a/cryptol.cabal b/cryptol.cabal index a67de891b..bae401530 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -141,6 +141,7 @@ library Cryptol.ModuleSystem.Name, Cryptol.ModuleSystem.Names, Cryptol.ModuleSystem.NamingEnv, + Cryptol.ModuleSystem.NamingEnv.Types, Cryptol.ModuleSystem.Binds Cryptol.ModuleSystem.Exports, Cryptol.ModuleSystem.Renamer, diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 6f69b5152..be21d8a32 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -631,7 +631,11 @@ checkModule isrc m = do rewMod <- case tcm of T.TCTopModule mo -> T.TCTopModule <$> liftSupply (`rewModule` mo) T.TCTopSignature {} -> pure tcm - pure (R.rmInScope renMod,rewMod) + let nameEnv = case tcm of + T.TCTopModule mo -> T.mInScope mo + -- Name env for signatures does not change after typechecking + T.TCTopSignature {} -> mInScope (R.rmModule renMod) + pure (nameEnv,rewMod) data TCLinter o = TCLinter { lintCheck :: diff --git a/src/Cryptol/ModuleSystem/Interface.hs b/src/Cryptol/ModuleSystem/Interface.hs index 66c947d0d..7410bebca 100644 --- a/src/Cryptol/ModuleSystem/Interface.hs +++ b/src/Cryptol/ModuleSystem/Interface.hs @@ -42,6 +42,7 @@ import Prelude () import Prelude.Compat import Cryptol.ModuleSystem.Name +import Cryptol.ModuleSystem.NamingEnv.Types import Cryptol.Utils.Ident (ModName, OrigName(..)) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.Fixity(Fixity) @@ -74,6 +75,7 @@ data IfaceNames name = IfaceNames , ifsNested :: Set Name -- ^ Things nested in this module , ifsDefines :: Set Name -- ^ Things defined in this module , ifsPublic :: Set Name -- ^ Subset of `ifsDefines` that is public + , ifsInScope :: NamingEnv -- ^ Things in scope in this module , ifsDoc :: !(Maybe Text) -- ^ Documentation } deriving (Show, Generic, NFData) @@ -87,6 +89,7 @@ emptyIface nm = Iface , ifsDefines = mempty , ifsPublic = mempty , ifsNested = mempty + , ifsInScope = mempty , ifsDoc = Nothing } , ifParams = mempty diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index de4e7bb50..d7df7017e 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -6,14 +6,14 @@ -- Stability : provisional -- Portability : portable -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE BlockArguments #-} -{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} -module Cryptol.ModuleSystem.NamingEnv where +module Cryptol.ModuleSystem.NamingEnv + ( module Cryptol.ModuleSystem.NamingEnv.Types + , module Cryptol.ModuleSystem.NamingEnv + ) where import Data.Maybe (mapMaybe,maybeToList) import Data.Map.Strict (Map) @@ -22,9 +22,6 @@ import Data.Set (Set) import qualified Data.Set as Set import Data.Foldable(foldl') -import GHC.Generics (Generic) -import Control.DeepSeq(NFData) - import Cryptol.Utils.PP import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Ident(allNamespaces) @@ -34,24 +31,7 @@ import Cryptol.ModuleSystem.Name import Cryptol.ModuleSystem.Names import Cryptol.ModuleSystem.Interface - --- | The 'NamingEnv' is used by the renamer to determine what --- identifiers refer to. -newtype NamingEnv = NamingEnv (Map Namespace (Map PName Names)) - deriving (Show,Generic,NFData) - -instance Monoid NamingEnv where - mempty = NamingEnv Map.empty - {-# INLINE mempty #-} - -instance Semigroup NamingEnv where - NamingEnv l <> NamingEnv r = - NamingEnv (Map.unionWith (Map.unionWith (<>)) l r) - -instance PP NamingEnv where - ppPrec _ (NamingEnv mps) = vcat $ map ppNS $ Map.toList mps - where ppNS (ns,xs) = nest 2 (vcat (pp ns : map ppNm (Map.toList xs))) - ppNm (x,as) = pp x <+> "->" <+> commaSep (map pp (namesToList as)) +import Cryptol.ModuleSystem.NamingEnv.Types {- | This "joins" two naming environments by matching the text name. diff --git a/src/Cryptol/ModuleSystem/NamingEnv/Types.hs b/src/Cryptol/ModuleSystem/NamingEnv/Types.hs new file mode 100644 index 000000000..ae80535dd --- /dev/null +++ b/src/Cryptol/ModuleSystem/NamingEnv/Types.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE OverloadedStrings #-} + +module Cryptol.ModuleSystem.NamingEnv.Types where + +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map + +import Control.DeepSeq (NFData) +import GHC.Generics (Generic) + +import Cryptol.ModuleSystem.Names +import Cryptol.Parser.Name +import Cryptol.Utils.Ident +import Cryptol.Utils.PP + +-- | The 'NamingEnv' is used by the renamer to determine what +-- identifiers refer to. +newtype NamingEnv = NamingEnv (Map Namespace (Map PName Names)) + deriving (Show,Generic,NFData) + +instance Monoid NamingEnv where + mempty = NamingEnv Map.empty + {-# INLINE mempty #-} + +instance Semigroup NamingEnv where + NamingEnv l <> NamingEnv r = + NamingEnv (Map.unionWith (Map.unionWith (<>)) l r) + +instance PP NamingEnv where + ppPrec _ (NamingEnv mps) = vcat $ map ppNS $ Map.toList mps + where ppNS (ns,xs) = nest 2 (vcat (pp ns : map ppNm (Map.toList xs))) + ppNm (x,as) = pp x <+> "->" <+> commaSep (map pp (namesToList as)) diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index e9e4779c3..a5b08c9e9 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -118,7 +118,6 @@ The Renamer Algorithm data RenamedModule = RenamedModule { rmModule :: Module Name -- ^ The renamed module , rmDefines :: NamingEnv -- ^ What this module defines - , rmInScope :: NamingEnv -- ^ What's in scope in this module , rmImported :: IfaceDecls -- ^ Imported declarations. This provides the types for external -- names (used by the type-checker). @@ -152,12 +151,11 @@ renameModule m0 = setResolvedLocals resolvedMods $ setNestedModule pathToName - do (ifs,(inScope,m1)) <- collectIfaceDeps (renameModule' mname m) + do (ifs,m1) <- collectIfaceDeps (renameModule' mname m) env <- rmodDefines <$> lookupResolved mname pure RenamedModule { rmModule = m1 , rmDefines = env - , rmInScope = inScope , rmImported = ifs -- XXX: maybe we should keep the nested defines too? } @@ -220,7 +218,7 @@ class Rename f where renameModule' :: ImpName Name {- ^ Resolved name for this module -} -> ModuleG mname PName -> - RenameM (NamingEnv, ModuleG mname Name) + RenameM (ModuleG mname Name) renameModule' mname m = setCurMod case mname of @@ -247,7 +245,7 @@ renameModule' mname m = let exports = exportedDecls ds1 mapM_ recordUse (exported NSType exports) inScope <- getNamingEnv - pure (inScope, m { mDef = NormalModule ds1 }) + pure m { mDef = NormalModule ds1, mInScope = inScope } -- The things defined by this module are the *results* -- of the instantiation, so we should *not* add them @@ -260,30 +258,20 @@ renameModule' mname m = let l = Just (srcRange f') imap <- mkInstMap l mempty (thing f') mname - {- Now we need to compute what's "in scope" of the instantiated - module. This is used when the module is loaded at the command - line and users want to evalute things in the context of the - module -} - fuEnv <- if isFakeName (thing f') - then pure mempty - else lookupDefines (thing f') - let ren x = Map.findWithDefault x x imap - - -- XXX: This is not quite right as it only considers the things - -- defined in the module to be in scope. It misses things - -- that are *imported* by the functor, in particular the Cryptol - -- library - -- is missing. See #1455. - inScope <- shadowNames' CheckNone (mapNamingEnv ren fuEnv) - getNamingEnv - - pure (inScope, m { mDef = FunctorInstance f' as' imap }) + -- This inScope is incomplete; it only contains names from the + -- enclosing scope, but we also want the names in scope from the + -- functor, for ease of testing at the command line. We will fix + -- this up in doFunctorInst in the typechecker, because right now + -- we don't have access yet to the inScope of the functor. + inScope <- getNamingEnv + + pure m { mDef = FunctorInstance f' as' imap, mInScope = inScope } InterfaceModule s -> shadowNames' CheckNone (rmodDefines resolved) do d <- InterfaceModule <$> renameIfaceModule mname s inScope <- getNamingEnv - pure (inScope, m { mDef = d }) + pure m { mDef = d, mInScope = inScope } checkFunctorArgs :: ModuleInstanceArgs Name -> RenameM () @@ -820,10 +808,8 @@ instance Rename NestedModule where nm = thing lnm n <- resolveName NameBind NSModule nm depsOf (NamedThing n) - do -- XXX: we should store in scope somewhere if we want to browse - -- nested modules properly - let m' = m { mName = ImpNested <$> mName m } - (_inScope,m1) <- renameModule' (ImpNested n) m' + do let m' = m { mName = ImpNested <$> mName m } + m1 <- renameModule' (ImpNested n) m' pure (NestedModule m1 { mName = lnm { thing = n } }) @@ -1416,8 +1402,6 @@ instance PP RenamedModule where doc = vcat [ "// --- Defines -----------------------------" , pp (rmDefines rn) - , "// --- In scope ----------------------------" - , pp (rmInScope rn) , "// -- Module -------------------------------" , pp (rmModule rn) , "// -----------------------------------------" diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 096e8027a..9ac521a13 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -106,6 +106,7 @@ module Cryptol.Parser.AST , cppKind, ppSelector ) where +import Cryptol.ModuleSystem.NamingEnv.Types import Cryptol.Parser.Name import Cryptol.Parser.Position import Cryptol.Parser.Selector @@ -158,6 +159,11 @@ newtype Program name = Program [TopDecl name] data ModuleG mname name = Module { mName :: Located mname -- ^ Name of the module , mDef :: ModuleDefinition name + , mInScope :: NamingEnv + -- ^ Names in scope inside this module, filled in by the renamer. + -- Also, for the 'FunctorInstance' case this is not the final result of + -- the names in scope. The typechecker adds in the names in scope in the + -- functor, so this will just contain the names in the enclosing scope. } deriving (Show, Generic, NFData) @@ -839,6 +845,7 @@ 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) + $$ indent 2 (vcat ["/* In scope:", indent 2 (pp (mInScope m)), " */"]) where kw' = case mDef m of InterfaceModule {} -> "interface" <+> kw @@ -1352,6 +1359,7 @@ instance NoPos (Program name) where instance NoPos (ModuleG mname name) where noPos m = Module { mName = mName m , mDef = noPos (mDef m) + , mInScope = mInScope m } instance NoPos (ModuleDefinition name) where diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index 457f5c3aa..c0d0775e9 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -961,6 +961,7 @@ mkProp ty = mkModule :: Located ModName -> [TopDecl PName] -> Module PName mkModule nm ds = Module { mName = nm , mDef = NormalModule ds + , mInScope = mempty } mkNested :: Module PName -> ParseM (NestedModule PName) @@ -979,8 +980,9 @@ mkSigDecl doc (nm,sig) = TopLevel { tlExport = Public , tlDoc = doc , tlValue = NestedModule - Module { mName = nm - , mDef = InterfaceModule sig + Module { mName = nm + , mDef = InterfaceModule sig + , mInScope = mempty } } @@ -1055,8 +1057,9 @@ mkModuleInstanceAnon :: Located ModName -> [TopDecl PName] -> Module PName mkModuleInstanceAnon nm fun ds = - Module { mName = nm - , mDef = FunctorInstance fun (DefaultInstAnonArg ds) mempty + Module { mName = nm + , mDef = FunctorInstance fun (DefaultInstAnonArg ds) mempty + , mInScope = mempty } mkModuleInstance :: @@ -1065,8 +1068,9 @@ mkModuleInstance :: ModuleInstanceArgs PName -> Module PName mkModuleInstance m f as = - Module { mName = m - , mDef = FunctorInstance f as emptyModuleInstance + Module { mName = m + , mDef = FunctorInstance f as emptyModuleInstance + , mInScope = mempty } @@ -1188,8 +1192,9 @@ mkTopMods = desugarMod mkTopSig :: Located ModName -> Signature PName -> [Module PName] mkTopSig nm sig = - [ Module { mName = nm - , mDef = InterfaceModule sig + [ Module { mName = nm + , mDef = InterfaceModule sig + , mInScope = mempty } ] @@ -1233,7 +1238,8 @@ desugarMod mo = let i = mkAnon AnonArg (thing (mName mo)) nm = Located { srcRange = srcRange (mName mo), thing = i } as' = DefaultInstArg (ModuleArg . toImpName <$> nm) - pure [ Module { mName = nm, mDef = NormalModule lds' } + pure [ Module + { mName = nm, mDef = NormalModule lds', mInScope = mempty } , mo { mDef = FunctorInstance f as' mempty } ] @@ -1283,6 +1289,7 @@ desugarTopDs ownerName = go emptySig do let nm = mkAnon AnonIfaceMod <$> ownerName pure ( [ Module { mName = nm , mDef = InterfaceModule sig + , mInScope = mempty } ] , [ DModParam @@ -1326,9 +1333,10 @@ desugarInstImport :: ParseM [TopDecl PName] desugarInstImport i inst = do ms <- desugarMod - Module { mName = i { thing = iname } - , mDef = FunctorInstance - (iModule <$> i) inst emptyModuleInstance + Module { mName = i { thing = iname } + , mDef = FunctorInstance + (iModule <$> i) inst emptyModuleInstance + , mInScope = mempty } pure (DImport (newImp <$> i) : map modTop ms) diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index fafb5fb24..c0cdd122f 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -36,6 +36,7 @@ import Cryptol.Utils.Panic(panic) import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim) import Cryptol.Parser.Position(Located,Range,HasLoc(..)) import Cryptol.ModuleSystem.Name +import Cryptol.ModuleSystem.NamingEnv.Types import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Exports(ExportSpec(..) , isExportedBind, isExportedType, isExported) @@ -111,6 +112,10 @@ data ModuleG mname = , mDecls :: [DeclGroup] , mSubmodules :: Map Name (IfaceNames Name) , mSignatures :: !(Map Name ModParamNames) + + , mInScope :: NamingEnv + -- ^ Things in scope at the top level. + -- Submodule in-scope information is in 'mSubmodules'. } deriving (Show, Generic, NFData) emptyModule :: mname -> ModuleG mname @@ -134,6 +139,8 @@ emptyModule nm = , mFunctors = mempty , mSubmodules = mempty , mSignatures = mempty + + , mInScope = mempty } -- | Find all the foreign declarations in the module and return their names and FFIFunTypes. diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 17c6f56ea..99b808b0a 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -79,13 +79,14 @@ inferTopModule :: P.Module Name -> InferM TCTopEntity inferTopModule m = case P.mDef m of P.NormalModule ds -> - do newModuleScope (thing (P.mName m)) (P.exportedDecls ds) + do newModuleScope (thing (P.mName m)) (P.exportedDecls ds) (P.mInScope m) checkTopDecls ds proveModuleTopLevel endModule P.FunctorInstance f as inst -> - do mb <- doFunctorInst (P.ImpTop <$> P.mName m) f as inst Nothing + do mb <- doFunctorInst + (P.ImpTop <$> P.mName m) f as inst (P.mInScope m) Nothing case mb of Just mo -> pure mo Nothing -> panic "inferModule" ["Didnt' get a module"] @@ -1322,13 +1323,15 @@ checkTopDecls = mapM_ checkTopDecl do newSubmoduleScope (thing (P.mName m)) (thing <$> P.tlDoc tl) (P.exportedDecls ds) + (P.mInScope m) checkTopDecls ds proveModuleTopLevel endSubmodule P.FunctorInstance f as inst -> do let doc = thing <$> P.tlDoc tl - _ <- doFunctorInst (P.ImpNested <$> P.mName m) f as inst doc + _ <- doFunctorInst + (P.ImpNested <$> P.mName m) f as inst (P.mInScope m) doc pure () P.InterfaceModule sig -> diff --git a/src/Cryptol/TypeCheck/Interface.hs b/src/Cryptol/TypeCheck/Interface.hs index 3464635ce..c468a3669 100644 --- a/src/Cryptol/TypeCheck/Interface.hs +++ b/src/Cryptol/TypeCheck/Interface.hs @@ -32,6 +32,7 @@ genIfaceNames m = IfaceNames , ifsNested = mNested m , ifsDefines = genModDefines m , ifsPublic = allExported (mExports m) + , ifsInScope = mInScope m , ifsDoc = mDoc m } diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index e726e8632..59d724432 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -15,6 +15,7 @@ import Cryptol.Utils.Ident(Ident,Namespace(..),isInfixIdent) import Cryptol.Parser.Position (Range,Located(..), thing) import qualified Cryptol.Parser.AST as P import Cryptol.ModuleSystem.Name(nameIdent) +import Cryptol.ModuleSystem.NamingEnv (NamingEnv(..), shadowing) import Cryptol.ModuleSystem.Interface ( IfaceG(..), IfaceDecls(..), IfaceNames(..), IfaceDecl(..) , filterIfaceDecls @@ -36,9 +37,11 @@ doFunctorInst :: {- ^ Instantitation. These is the renaming for the functor that arises from generativity (i.e., it is something that will make the names "fresh"). -} -> + NamingEnv + {- ^ Names in the enclosing scope of the instantiated module -} -> Maybe Text {- ^ Documentation -} -> InferM (Maybe TCTopEntity) -doFunctorInst m f as inst doc = +doFunctorInst m f as inst enclosingInScope doc = inRange (srcRange m) do mf <- lookupFunctor (thing f) argIs <- checkArity (srcRange f) mf as @@ -73,9 +76,10 @@ doFunctorInst m f as inst doc = (Map.unions vps) m2 + let inScope = mInScope m2 `shadowing` enclosingInScope case thing m of - P.ImpTop mn -> newModuleScope mn (mExports m2) - P.ImpNested mn -> newSubmoduleScope mn doc (mExports m2) + P.ImpTop mn -> newModuleScope mn (mExports m2) inScope + P.ImpNested mn -> newSubmoduleScope mn doc (mExports m2) inScope mapM_ addTySyn (Map.elems (mTySyns m2)) mapM_ addNewtype (Map.elems (mNewtypes m2)) diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs index d041a3665..701f93114 100644 --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -8,6 +8,7 @@ import qualified Data.Set as Set import Cryptol.Parser.Position(Located) import Cryptol.ModuleSystem.Interface(IfaceNames(..)) +import Cryptol.ModuleSystem.NamingEnv(NamingEnv,mapNamingEnv) import Cryptol.IR.TraverseNames(TraverseNames,mapNames) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Subst(Subst,TVars,apSubst) @@ -51,6 +52,9 @@ instance ModuleInstance a => ModuleInstance (Located a) where instance ModuleInstance Name where moduleInstance = doVInst +instance ModuleInstance NamingEnv where + moduleInstance = mapNamingEnv doVInst + instance ModuleInstance name => ModuleInstance (ImpName name) where moduleInstance x = case x of @@ -74,6 +78,7 @@ instance ModuleInstance (ModuleG name) where , mDecls = moduleInstance (mDecls m) , mSubmodules = doMap (mSubmodules m) , mSignatures = doMap (mSignatures m) + , mInScope = moduleInstance (mInScope m) } instance ModuleInstance Type where @@ -127,6 +132,7 @@ instance ModuleInstance name => ModuleInstance (IfaceNames name) where , ifsNested = doSet (ifsNested ns) , ifsDefines = doSet (ifsDefines ns) , ifsPublic = doSet (ifsPublic ns) + , ifsInScope = moduleInstance (ifsInScope ns) , ifsDoc = ifsDoc ns } diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index 5dfb3ac80..054b4cb90 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -40,6 +40,7 @@ import MonadLib hiding (mapM) import Cryptol.ModuleSystem.Name (FreshM(..),Supply,mkLocal,asLocal , nameInfo, NameInfo(..),NameSource(..), nameTopModule) +import Cryptol.ModuleSystem.NamingEnv.Types import qualified Cryptol.ModuleSystem.Interface as If import Cryptol.Parser.Position import qualified Cryptol.Parser.AST as P @@ -1006,16 +1007,16 @@ newTopSignatureScope x = newScope (TopSignatureScope x) to initialize an empty module. As we type check declarations they are added to this module's scope. -} newSubmoduleScope :: - Name -> Maybe Text -> ExportSpec Name -> InferM () -newSubmoduleScope x docs e = + Name -> Maybe Text -> ExportSpec Name -> NamingEnv -> InferM () +newSubmoduleScope x docs e inScope = do updScope \o -> o { mNested = Set.insert x (mNested o) } newScope (SubModule x) - updScope \m -> m { mDoc = docs, mExports = e } + updScope \m -> m { mDoc = docs, mExports = e, mInScope = inScope } -newModuleScope :: P.ModName -> ExportSpec Name -> InferM () -newModuleScope x e = +newModuleScope :: P.ModName -> ExportSpec Name -> NamingEnv -> InferM () +newModuleScope x e inScope = do newScope (MTopModule x) - updScope \m -> m { mDoc = Nothing, mExports = e } + updScope \m -> m { mDoc = Nothing, mExports = e, mInScope = inScope } -- | Update the current scope (first in the list). Assumes there is one. updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM () @@ -1057,6 +1058,7 @@ endSubmodule = , mParamConstraints = mParamConstraints y , mParams = mParams y , mNested = mNested y + , mInScope = mInScope y , mTySyns = add mTySyns , mNewtypes = add mNewtypes @@ -1155,6 +1157,8 @@ getCurDecls = , mSubmodules = uni mSubmodules , mFunctors = uni mFunctors , mSignatures = uni mSignatures + + , mInScope = uni mInScope } where uni f = f m1 <> f m2 From 632adf480a617b7a34405264e704f63b44d03477 Mon Sep 17 00:00:00 2001 From: Bretton Date: Fri, 28 Jul 2023 18:46:26 -0700 Subject: [PATCH 02/17] Add comment in doFunctorInst explaining inScope --- src/Cryptol/TypeCheck/Module.hs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index 59d724432..40eea571c 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -76,7 +76,16 @@ doFunctorInst m f as inst enclosingInScope doc = (Map.unions vps) m2 + -- An instantiation doesn't really have anything "in scope" per se, but + -- here we compute what would be in scope as if you hand wrote the + -- instantiation by copy-pasting the functor then substituting the + -- parameters. That is, it would be whatever is in scope in the functor, + -- together with any names in the enclosing scope if this is a nested + -- module, with the functor's names taking precedence. This is used to + -- determine what is in scope at the REPL when the instantiation is loaded + -- and focused. let inScope = mInScope m2 `shadowing` enclosingInScope + case thing m of P.ImpTop mn -> newModuleScope mn (mExports m2) inScope P.ImpNested mn -> newSubmoduleScope mn doc (mExports m2) inScope From e9b3b5f6a63cb699687eaaf624807b56f7be09ea Mon Sep 17 00:00:00 2001 From: Bretton Date: Wed, 2 Aug 2023 15:20:08 -0700 Subject: [PATCH 03/17] Make fresh name for value params in instantiations --- src/Cryptol/ModuleSystem/Renamer.hs | 5 +- src/Cryptol/Parser/AST.hs | 7 ++- src/Cryptol/TypeCheck/Module.hs | 62 +++++++++++-------- .../TypeCheck/ModuleBacktickInstance.hs | 10 ++- 4 files changed, 47 insertions(+), 37 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index a5b08c9e9..6bd2cdb56 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -220,10 +220,7 @@ renameModule' :: ModuleG mname PName -> RenameM (ModuleG mname Name) renameModule' mname m = - setCurMod - case mname of - ImpTop r -> TopModule r - ImpNested r -> Nested (nameModPath r) (nameIdent r) + setCurMod (impNameModPath mname) do resolved <- lookupResolved mname shadowNames' CheckNone (rmodImports resolved) diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 9ac521a13..63c2ecec4 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -67,7 +67,7 @@ module Cryptol.Parser.AST , Pragma(..) , ExportType(..) , TopLevel(..) - , Import, ImportG(..), ImportSpec(..), ImpName(..) + , Import, ImportG(..), ImportSpec(..), ImpName(..), impNameModPath , Newtype(..) , PrimType(..) , ParameterType(..) @@ -106,6 +106,7 @@ module Cryptol.Parser.AST , cppKind, ppSelector ) where +import Cryptol.ModuleSystem.Name (Name, nameModPath, nameIdent) import Cryptol.ModuleSystem.NamingEnv.Types import Cryptol.Parser.Name import Cryptol.Parser.Position @@ -310,6 +311,10 @@ data ImpName name = | ImpNested name -- ^ The module in scope with the given name deriving (Show, Generic, NFData, Eq, Ord) +impNameModPath :: ImpName Name -> ModPath +impNameModPath (ImpTop mn) = TopModule mn +impNameModPath (ImpNested n) = Nested (nameModPath n) (nameIdent n) + -- | A simple declaration. Generally these are things that can appear -- both at the top-level of a module and in `where` clauses. data Decl name = DSignature [Located name] (Schema name) diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index 40eea571c..700600d17 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -7,14 +7,15 @@ import Data.Map(Map) import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set -import Control.Monad(unless,forM_) +import Control.Monad(unless,forM_,mapAndUnzipM) import Cryptol.Utils.Panic(panic) -import Cryptol.Utils.Ident(Ident,Namespace(..),isInfixIdent) +import Cryptol.Utils.Ident(Ident,Namespace(..),ModPath,isInfixIdent) import Cryptol.Parser.Position (Range,Located(..), thing) import qualified Cryptol.Parser.AST as P -import Cryptol.ModuleSystem.Name(nameIdent) +import Cryptol.ModuleSystem.Binds(newModParam) +import Cryptol.ModuleSystem.Name(nameIdent, nameLoc) import Cryptol.ModuleSystem.NamingEnv (NamingEnv(..), shadowing) import Cryptol.ModuleSystem.Interface ( IfaceG(..), IfaceDecls(..), IfaceNames(..), IfaceDecl(..) @@ -41,14 +42,16 @@ doFunctorInst :: {- ^ Names in the enclosing scope of the instantiated module -} -> Maybe Text {- ^ Documentation -} -> InferM (Maybe TCTopEntity) -doFunctorInst m f as inst enclosingInScope doc = +doFunctorInst m f as instMap enclosingInScope doc = inRange (srcRange m) do mf <- lookupFunctor (thing f) argIs <- checkArity (srcRange f) mf as - m2 <- do as2 <- mapM checkArg argIs - let (tySus,decls) = unzip [ (su,ds) | DefinedInst su ds <- as2 ] + m2 <- do let mpath = P.impNameModPath (thing m) + as2 <- mapM (checkArg mpath) argIs + let (tySus,decls,paramInstMaps) = + unzip3 [ (su,ds,im) | DefinedInst su ds im <- as2 ] let ?tSu = mergeDistinctSubst tySus - ?vSu = inst + ?vSu = instMap <> mconcat paramInstMaps let m1 = moduleInstance mf m2 = m1 { mName = m , mDoc = Nothing @@ -113,10 +116,7 @@ data ActualArg = {- | Validate a functor application, just checking the argument names. The result associates a module parameter with the concrete way it should -be instantiated, which could be: - - * `Left` instanciate using another parameter that is in scope - * `Right` instanciate using a module, with the given interface +be instantiated. -} checkArity :: Range {- ^ Location for reporting errors -} -> @@ -172,7 +172,10 @@ checkArity r mf args = checkArgs done ps more -data ArgInst = DefinedInst Subst [Decl] -- ^ Argument that defines the params +data ArgInst = DefinedInst Subst [Decl] (Map Name Name) + -- ^ Argument that defines the params + -- The map is for mapping the functor's names to the new names + -- created for the instantiation | ParamInst (Set (MBQual TParam)) [Prop] (Map (MBQual Name) Type) -- ^ Argument that add parameters -- The type parameters are in their module type parameter @@ -192,8 +195,8 @@ Returns: * XXX: Extra parameters for instantiation by adding params -} checkArg :: - (Range, ModParam, ActualArg) -> InferM ArgInst -checkArg (r,expect,actual') = + ModPath -> (Range, ModParam, ActualArg) -> InferM ArgInst +checkArg mpath (r,expect,actual') = case actual' of AddDeclParams -> paramInst UseParameter {} -> definedInst @@ -204,7 +207,7 @@ checkArg (r,expect,actual') = do let as = Set.fromList (map (qual . mtpParam) (Map.elems (mpnTypes params))) cs = map thing (mpnConstraints params) - check = checkSimpleParameterValue r (mpName expect) + check = checkSimpleParameterValue r paramName qual a = (mpQual expect, a) fs <- Map.mapMaybeWithKey (\_ v -> v) <$> mapM check (mpnFuns params) pure (ParamInst as cs (Map.mapKeys qual fs)) @@ -218,15 +221,16 @@ checkArg (r,expect,actual') = doFunctorInst -} - vDecls <- concat <$> - mapM (checkParamValue r vMap) - [ s { mvpType = apSubst renSu (mvpType s) } - | s <- Map.elems (mpnFuns params) ] + (vDeclss, vInstMaps) <- + mapAndUnzipM (checkParamValue mpath r paramName vMap) + [ s { mvpType = apSubst renSu (mvpType s) } + | s <- Map.elems (mpnFuns params) ] - pure (DefinedInst renSu vDecls) + pure (DefinedInst renSu (concat vDeclss) (mconcat vInstMaps)) params = mpParameters expect + paramName = mpName expect -- Things provided by the argument module tyMap :: Map Ident (Kind, Type) @@ -297,30 +301,36 @@ checkParamType r tyMap (name,mp) = -- | Check a value parameter to a module. checkParamValue :: + ModPath {- ^ The module we are instantiating -} -> Range {- ^ Location for error reporting -} -> + Ident {- ^ Name of the _module_ parameter (not value) -} -> Map Ident (Name,Schema) {- ^ Actual values -} -> ModVParam {- ^ The parameter we are checking -} -> - InferM [Decl] {- ^ Mapping from parameter name to definition -} -checkParamValue r vMap mp = + InferM ([Decl], Map Name Name) + {- ^ Decl mapping a new name to the actual value, + and a map from the value param name in the functor to the new name + (for instantiation) -} +checkParamValue mpath r paramName vMap mp = let name = mvpName mp i = nameIdent name expectT = mvpType mp in case Map.lookup i vMap of Nothing -> do recordErrorLoc (Just r) (FunctorInstanceMissingName NSValue i) - pure [] + pure ([], Map.empty) Just actual -> do e <- mkParamDef r (name,expectT) actual - let d = Decl { dName = name + name' <- newModParam mpath paramName (nameLoc (fst actual)) name + let d = Decl { dName = name' , dSignature = expectT , dDefinition = DExpr e , dPragmas = [] - , dInfix = isInfixIdent (nameIdent name) + , dInfix = isInfixIdent (nameIdent name') , dFixity = mvpFixity mp , dDoc = mvpDoc mp } - pure [d] + pure ([d], Map.singleton name name') diff --git a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs index 212cd10e3..772d563ce 100644 --- a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs @@ -18,15 +18,15 @@ import Data.List(group,sort) import Data.Maybe(mapMaybe) import qualified Data.Text as Text -import Cryptol.Utils.Ident(ModPath(..), modPathIsOrContains,Namespace(..) +import Cryptol.Utils.Ident(modPathIsOrContains,Namespace(..) , Ident, mkIdent, identText , ModName, modNameChunksText ) import Cryptol.Utils.PP(pp) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.RecordMap(RecordMap,recordFromFields,recordFromFieldsErr) +import Cryptol.Parser.AST(impNameModPath) import Cryptol.Parser.Position -import Cryptol.ModuleSystem.Name( - nameModPath, nameModPathMaybe, nameIdent, mapNameIdent) +import Cryptol.ModuleSystem.Name(nameModPathMaybe, nameIdent, mapNameIdent) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Error import qualified Cryptol.TypeCheck.Monad as TC @@ -80,9 +80,7 @@ doBacktickInstance as ps mp m mkBad sel a = [ (a,k) | k <- Map.keys (sel m) ] - ourPath = case thing (mName m) of - ImpTop mo -> TopModule mo - ImpNested mo -> Nested (nameModPath mo) (nameIdent mo) + ourPath = impNameModPath (thing (mName m)) doAddParams nt sel = mapReader (\ro -> ro { newNewtypes = nt }) (addParams (sel m)) From d6791fd1c52242f6c7375afdf5e57b6dc0444684 Mon Sep 17 00:00:00 2001 From: Bretton Date: Wed, 2 Aug 2023 15:46:13 -0700 Subject: [PATCH 04/17] Rename confusing arg in checkParamValue --- src/Cryptol/TypeCheck/Module.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index 700600d17..e22c15b5d 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -310,7 +310,7 @@ checkParamValue :: {- ^ Decl mapping a new name to the actual value, and a map from the value param name in the functor to the new name (for instantiation) -} -checkParamValue mpath r paramName vMap mp = +checkParamValue mpath r modParamName vMap mp = let name = mvpName mp i = nameIdent name expectT = mvpType mp @@ -320,7 +320,7 @@ checkParamValue mpath r paramName vMap mp = pure ([], Map.empty) Just actual -> do e <- mkParamDef r (name,expectT) actual - name' <- newModParam mpath paramName (nameLoc (fst actual)) name + name' <- newModParam mpath modParamName (nameLoc (fst actual)) name let d = Decl { dName = name' , dSignature = expectT , dDefinition = DExpr e From 6a0121cb04eba3c82f0a2ae9813c21d7303986b9 Mon Sep 17 00:00:00 2001 From: Bretton Date: Thu, 3 Aug 2023 17:03:35 -0700 Subject: [PATCH 05/17] Add type synonym for type params in instantiations --- src/Cryptol/TypeCheck/Module.hs | 75 +++++++++++++++++-------- src/Cryptol/TypeCheck/ModuleInstance.hs | 2 +- 2 files changed, 52 insertions(+), 25 deletions(-) diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index e22c15b5d..07d988835 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -1,7 +1,7 @@ {-# Language BlockArguments, ImplicitParams #-} module Cryptol.TypeCheck.Module (doFunctorInst) where -import Data.List(partition) +import Data.List(partition,unzip4) import Data.Text(Text) import Data.Map(Map) import qualified Data.Map as Map @@ -48,8 +48,8 @@ doFunctorInst m f as instMap enclosingInScope doc = argIs <- checkArity (srcRange f) mf as m2 <- do let mpath = P.impNameModPath (thing m) as2 <- mapM (checkArg mpath) argIs - let (tySus,decls,paramInstMaps) = - unzip3 [ (su,ds,im) | DefinedInst su ds im <- as2 ] + let (tySus,paramTySyns,decls,paramInstMaps) = + unzip4 [ (su,ts,ds,im) | DefinedInst su ts ds im <- as2 ] let ?tSu = mergeDistinctSubst tySus ?vSu = instMap <> mconcat paramInstMaps let m1 = moduleInstance mf @@ -59,6 +59,7 @@ doFunctorInst m f as instMap enclosingInScope doc = , mParamFuns = mempty , mParamConstraints = mempty , mParams = mempty + , mTySyns = mconcat paramTySyns <> mTySyns m1 , mDecls = map NonRecursive (concat decls) ++ mDecls m1 } @@ -172,10 +173,16 @@ checkArity r mf args = checkArgs done ps more -data ArgInst = DefinedInst Subst [Decl] (Map Name Name) - -- ^ Argument that defines the params - -- The map is for mapping the functor's names to the new names - -- created for the instantiation +data ArgInst = -- | Argument that defines the params + DefinedInst Subst + (Map Name TySyn) + -- ^ Type synonyms created from the functor's type parameters + [Decl] + -- ^ Bindings for value parameters + (Map Name Name) + -- ^ Map from the functor's parameter names to the new names + -- created for the instantiation + | ParamInst (Set (MBQual TParam)) [Prop] (Map (MBQual Name) Type) -- ^ Argument that add parameters -- The type parameters are in their module type parameter @@ -213,7 +220,8 @@ checkArg mpath (r,expect,actual') = pure (ParamInst as cs (Map.mapKeys qual fs)) definedInst = - do tRens <- mapM (checkParamType r tyMap) (Map.toList (mpnTypes params)) + do (tRens, tSyns, tInstMaps) <- unzip3 <$> mapM + (checkParamType mpath r paramName tyMap) (Map.toList (mpnTypes params)) let renSu = listParamSubst (concat tRens) {- Note: the constraints from the signature are already added to the @@ -221,19 +229,20 @@ checkArg mpath (r,expect,actual') = doFunctorInst -} - (vDeclss, vInstMaps) <- + (vDecls, vInstMaps) <- mapAndUnzipM (checkParamValue mpath r paramName vMap) [ s { mvpType = apSubst renSu (mvpType s) } | s <- Map.elems (mpnFuns params) ] - pure (DefinedInst renSu (concat vDeclss) (mconcat vInstMaps)) + pure $ DefinedInst renSu (mconcat tSyns) + (concat vDecls) (mconcat tInstMaps <> mconcat vInstMaps) params = mpParameters expect paramName = mpName expect -- Things provided by the argument module - tyMap :: Map Ident (Kind, Type) + tyMap :: Map Ident (Name, Kind, Type) vMap :: Map Ident (Name, Schema) (tyMap,vMap) = case actual' of @@ -243,7 +252,7 @@ checkArg mpath (r,expect,actual') = ) where ps = mpParameters mp - fromTP tp = (mtpKind tp, TVar (TVBound (mtpParam tp))) + fromTP tp = (mtpName tp, mtpKind tp, TVar (TVBound (mtpParam tp))) fromVP vp = (mvpName vp, mvpType vp) UseModule actual -> @@ -263,9 +272,9 @@ checkArg mpath (r,expect,actual') = decls = filterIfaceDecls isLocal (ifDefines actual) fromD d = (ifDeclName d, ifDeclSig d) - fromTS ts = (kindOf ts, tsDef ts) - fromNewtype nt = (kindOf nt, TNewtype nt []) - fromPrimT pt = (kindOf pt, TCon (abstractTypeTC pt) []) + fromTS ts = (tsName ts, kindOf ts, tsDef ts) + fromNewtype nt = (ntName nt, kindOf nt, TNewtype nt []) + fromPrimT pt = (atName pt, kindOf pt, TCon (abstractTypeTC pt) []) AddDeclParams -> panic "checkArg" ["AddDeclParams"] @@ -280,28 +289,46 @@ nameMapToIdentMap f m = -- | Check a type parameter to a module. checkParamType :: - Range {- ^ Location for error reporting -} -> - Map Ident (Kind,Type) {- ^ Actual types -} -> - (Name,ModTParam) {- ^ Type parameter -} -> - InferM [(TParam,Type)] {- ^ Mapping from parameter name to actual type -} -checkParamType r tyMap (name,mp) = + ModPath {- ^ The new module we are creating -} -> + Range {- ^ Location for error reporting -} -> + Ident {- ^ Name of the _module_ parameter + (not value) -} -> + Map Ident (Name,Kind,Type) {- ^ Actual types -} -> + (Name,ModTParam) {- ^ Type parameter -} -> + InferM ([(TParam,Type)], Map Name TySyn, Map Name Name) + {- ^ Mapping from parameter name to actual type (for type substitution), + type synonym map from a fresh type name to the actual type + (only so that the type can be referred to in the REPL; + type synonyms are fully inlined into types at this point), + and a map from the old type name to the fresh type name + (for instantiation) -} +checkParamType mpath r modParamName tyMap (name,mp) = let i = nameIdent name expectK = mtpKind mp in case Map.lookup i tyMap of Nothing -> do recordErrorLoc (Just r) (FunctorInstanceMissingName NSType i) - pure [] - Just (actualK,actualT) -> + pure ([], Map.empty, Map.empty) + Just (actualName,actualK,actualT) -> do unless (expectK == actualK) (recordErrorLoc (Just r) (KindMismatch (Just (TVFromModParam name)) expectK actualK)) - pure [(mtpParam mp, actualT)] + name' <- newModParam mpath modParamName (nameLoc actualName) name + let tySyn = TySyn { tsName = name' + , tsParams = [] + , tsConstraints = [] + , tsDef = actualT + , tsDoc = mtpDoc mp } + pure ( [(mtpParam mp, actualT)] + , Map.singleton name' tySyn + , Map.singleton name name' + ) -- | Check a value parameter to a module. checkParamValue :: - ModPath {- ^ The module we are instantiating -} -> + ModPath {- ^ The new module we are creating -} -> Range {- ^ Location for error reporting -} -> Ident {- ^ Name of the _module_ parameter (not value) -} -> Map Ident (Name,Schema) {- ^ Actual values -} -> diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs index 701f93114..c5dfd3b3e 100644 --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -28,7 +28,7 @@ doTInst = apSubst ?tSu -- | Has both value names and types. doTVInst :: (Su, TVars a, TraverseNames a) => a -> a -doTVInst = apSubst ?tSu . doVInst +doTVInst = doVInst . doTInst doMap :: (Su, ModuleInstance a) => Map Name a -> Map Name a doMap mp = From 44dd5908e44cd189256ffb7d634c5fbf7be3d3b2 Mon Sep 17 00:00:00 2001 From: Bretton Date: Fri, 4 Aug 2023 11:21:40 -0700 Subject: [PATCH 06/17] Remove mod params from inScope in _ instantiation --- src/Cryptol/ModuleSystem/Binds.hs | 2 +- src/Cryptol/ModuleSystem/NamingEnv.hs | 9 +++++++-- src/Cryptol/TypeCheck/Module.hs | 10 ++++++++-- 3 files changed, 16 insertions(+), 5 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Binds.hs b/src/Cryptol/ModuleSystem/Binds.hs index 1ff0dba24..8eb47ec2a 100644 --- a/src/Cryptol/ModuleSystem/Binds.hs +++ b/src/Cryptol/ModuleSystem/Binds.hs @@ -125,7 +125,7 @@ ifaceSigToMod ps = Mod , modState = () } where - env = modParamsNamingEnv ps + env = modParamNamesNamingEnv ps diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index d7df7017e..9f15471e0 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -211,8 +211,8 @@ isEmptyNamingEnv (NamingEnv mp) = Map.null mp -- | Compute an unqualified naming environment, containing the various module -- parameters. -modParamsNamingEnv :: T.ModParamNames -> NamingEnv -modParamsNamingEnv T.ModParamNames { .. } = +modParamNamesNamingEnv :: T.ModParamNames -> NamingEnv +modParamNamesNamingEnv T.ModParamNames { .. } = NamingEnv $ Map.fromList [ (NSValue, Map.fromList $ map fromFu $ Map.keys mpnFuns) , (NSType, Map.fromList $ map fromTS (Map.elems mpnTySyn) ++ @@ -228,6 +228,11 @@ modParamsNamingEnv T.ModParamNames { .. } = fromTS ts = (toPName (T.tsName ts), One (T.tsName ts)) +-- | Compute a naming environment from a module parameter, qualifying it +-- according to 'mpQual'. +modParamNamingEnv :: T.ModParam -> NamingEnv +modParamNamingEnv mp = maybe id qualify (T.mpQual mp) $ + modParamNamesNamingEnv (T.mpParameters mp) -- | Generate a naming environment from a declaration interface, where none of -- the names are qualified. diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index 07d988835..62d2b552a 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -16,7 +16,8 @@ import Cryptol.Parser.Position (Range,Located(..), thing) import qualified Cryptol.Parser.AST as P import Cryptol.ModuleSystem.Binds(newModParam) import Cryptol.ModuleSystem.Name(nameIdent, nameLoc) -import Cryptol.ModuleSystem.NamingEnv (NamingEnv(..), shadowing) +import Cryptol.ModuleSystem.NamingEnv + (NamingEnv(..), modParamNamingEnv, shadowing, without) import Cryptol.ModuleSystem.Interface ( IfaceG(..), IfaceDecls(..), IfaceNames(..), IfaceDecl(..) , filterIfaceDecls @@ -88,7 +89,12 @@ doFunctorInst m f as instMap enclosingInScope doc = -- module, with the functor's names taking precedence. This is used to -- determine what is in scope at the REPL when the instantiation is loaded -- and focused. - let inScope = mInScope m2 `shadowing` enclosingInScope + -- + -- The exception is when instantiating with _, in which case we must delete + -- the module parameters from the naming environment. + let inScope0 = mInScope m2 `without` + mconcat [ modParamNamingEnv mp | (_, mp, AddDeclParams) <- argIs ] + inScope = inScope0 `shadowing` enclosingInScope case thing m of P.ImpTop mn -> newModuleScope mn (mExports m2) inScope From 09fba48ac02964d544b6cabf48df1c5dce4a6332 Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 7 Aug 2023 15:26:56 -0700 Subject: [PATCH 07/17] Keep FromModParam sig name in namingEnvFromNames --- src/Cryptol/ModuleSystem/Name.hs | 12 +++++++++++- src/Cryptol/ModuleSystem/NamingEnv.hs | 8 +++++--- src/Cryptol/Parser/Name.hs | 11 +++++++++++ src/Cryptol/Utils/Ident.hs | 4 ++++ 4 files changed, 31 insertions(+), 4 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs index 9ca140c15..4047d381b 100644 --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -29,6 +29,7 @@ module Cryptol.ModuleSystem.Name ( , nameLoc , nameFixity , nameNamespace + , asPName , asPrim , asOrigName , nameModPath @@ -70,7 +71,8 @@ import qualified Data.Text as Text import Data.Char(isAlpha,toUpper) - +import Cryptol.Parser.Name (PName) +import qualified Cryptol.Parser.Name as PName import Cryptol.Parser.Position (Range,Located(..)) import Cryptol.Utils.Fixity import Cryptol.Utils.Ident @@ -227,6 +229,14 @@ nameLoc = nLoc nameFixity :: Name -> Maybe Fixity nameFixity = nFixity +-- | We only qualify the 'PName' with the interface name from 'FromModParam' in +-- 'ogSource', if any. We don't qualify with the 'ModPath'. +asPName :: Name -> PName +asPName n = + case nInfo n of + GlobalName _ og -> PName.fromOrigName og + LocalName _ txt -> PName.mkUnqual txt + -- | Primtiives must be in a top level module, at least for now. asPrim :: Name -> Maybe PrimIdent asPrim n = diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index 9f15471e0..ffa0258eb 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -71,14 +71,16 @@ namingEnvNames (NamingEnv xs) = Just (One x) -> Set.singleton x Just (Ambig as) -> as --- | Get a unqualified naming environment for the given names +-- | Get a naming environment for the given names +-- +-- We only qualify the PNames with the interface name from 'FromModParam' in +-- 'ogSource', if any. We don't qualify with the 'ModPath'. namingEnvFromNames :: Set Name -> NamingEnv namingEnvFromNames xs = NamingEnv (foldl' add mempty xs) where add mp x = let ns = nameNamespace x - txt = nameIdent x in Map.insertWith (Map.unionWith (<>)) - ns (Map.singleton (mkUnqual txt) (One x)) + ns (Map.singleton (asPName x) (One x)) mp diff --git a/src/Cryptol/Parser/Name.hs b/src/Cryptol/Parser/Name.hs index dc74f3a54..68826655d 100644 --- a/src/Cryptol/Parser/Name.hs +++ b/src/Cryptol/Parser/Name.hs @@ -46,6 +46,17 @@ mkUnqual = UnQual mkQual :: ModName -> Ident -> PName mkQual = Qual +-- | We only qualify the 'PName' with the interface name from 'FromModParam' in +-- 'ogSource', if any. We don't qualify with the 'ModPath'. +fromOrigName :: OrigName -> PName +fromOrigName og = toPName (ogName og) + where + toPName = + case ogSource og of + FromDefinition -> UnQual + FromFunctorInst -> UnQual + FromModParam sig -> Qual (identToModName sig) + getModName :: PName -> Maybe ModName getModName (Qual ns _) = Just ns getModName _ = Nothing diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs index ddc6e0595..712d870bb 100644 --- a/src/Cryptol/Utils/Ident.hs +++ b/src/Cryptol/Utils/Ident.hs @@ -26,6 +26,7 @@ module Cryptol.Utils.Ident , modNameChunks , modNameChunksText , packModName + , identToModName , preludeName , preludeReferenceName , undefinedModName @@ -214,6 +215,9 @@ packModName strs = textToModName (T.intercalate modSep (map trim strs)) -- trim space off of the start and end of the string trim str = T.dropWhile isSpace (T.dropWhileEnd isSpace str) +identToModName :: Ident -> ModName +identToModName (Ident _ anon txt) = ModName txt anon + modSep :: T.Text modSep = "::" From 5cd34d0afbe5958da74a86285d34c2c17547fbc1 Mon Sep 17 00:00:00 2001 From: Bretton Date: Tue, 8 Aug 2023 15:53:24 -0700 Subject: [PATCH 08/17] Qualify FromFunctorInst OrigNames by interface --- src/Cryptol/ModuleSystem/Binds.hs | 8 +++++ src/Cryptol/ModuleSystem/Name.hs | 16 +++++---- src/Cryptol/ModuleSystem/NamingEnv.hs | 4 +-- src/Cryptol/ModuleSystem/Renamer/Imports.hs | 9 ++--- src/Cryptol/Parser/Name.hs | 11 +++--- src/Cryptol/TypeCheck/Module.hs | 38 +++++++++------------ src/Cryptol/Utils/Ident.hs | 12 ++++--- src/Cryptol/Utils/PP.hs | 18 +++++----- 8 files changed, 62 insertions(+), 54 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Binds.hs b/src/Cryptol/ModuleSystem/Binds.hs index 8eb47ec2a..23dedf5d7 100644 --- a/src/Cryptol/ModuleSystem/Binds.hs +++ b/src/Cryptol/ModuleSystem/Binds.hs @@ -13,6 +13,7 @@ module Cryptol.ModuleSystem.Binds , topModuleDefs , topDeclsDefs , newModParam + , newFunctorInst , InModule(..) , ifaceToMod , ifaceSigToMod @@ -420,6 +421,13 @@ newLocal ns thing rng = liftSupply (mkLocal ns (getIdent thing) rng) newModParam :: FreshM m => ModPath -> Ident -> Range -> Name -> m Name newModParam m i rng n = liftSupply (mkModParam m i rng n) +-- | Given a name in a functor, make a fresh name for the corresponding thing in +-- the instantiation. +-- +-- The 'ModPath' should be the instantiation not the functor. +newFunctorInst :: FreshM m => ModPath -> Name -> m Name +newFunctorInst m n = liftSupply (freshNameFor m n) + {- | Do something in the context of a module. If `Nothing` than we are working with a local declaration. diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs index 4047d381b..8a6c57d2e 100644 --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -148,9 +148,9 @@ cmpNameDisplay disp l r = NotInScope -> let m = Text.pack (show (pp (ogModule og))) in - case ogSource og of - FromModParam q -> m <> "::" <> Text.pack (show (pp q)) - _ -> m + case ogFromParam og of + Just q -> m <> "::" <> Text.pack (show (pp q)) + Nothing -> m -- Note that this assumes that `xs` is `l` and `ys` is `r` cmpText xs ys = @@ -229,8 +229,8 @@ nameLoc = nLoc nameFixity :: Name -> Maybe Fixity nameFixity = nFixity --- | We only qualify the 'PName' with the interface name from 'FromModParam' in --- 'ogSource', if any. We don't qualify with the 'ModPath'. +-- | We only qualify the 'PName' with the interface name from 'ogFromParam'. We +-- don't qualify with the 'ogModule'. asPName :: Name -> PName asPName n = case nInfo n of @@ -242,7 +242,7 @@ asPrim :: Name -> Maybe PrimIdent asPrim n = case nInfo n of GlobalName _ og - | TopModule m <- ogModule og, not (ogFromModParam og) -> + | TopModule m <- ogModule og, not (ogIsModParam og) -> Just $ PrimIdent m $ identText $ ogName og _ -> Nothing @@ -381,6 +381,7 @@ mkDeclared ns m sys ident fixity loc s = (name, s') , ogModule = m , ogName = ident , ogSource = FromDefinition + , ogFromParam = Nothing } } @@ -420,7 +421,8 @@ mkModParam own pname rng n s = (name, s') { ogModule = own , ogName = nameIdent n , ogNamespace = nameNamespace n - , ogSource = FromModParam pname + , ogSource = FromModParam + , ogFromParam = Just pname } , nFixity = nFixity n , nLoc = rng diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index ffa0258eb..f8a08b123 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -73,8 +73,8 @@ namingEnvNames (NamingEnv xs) = -- | Get a naming environment for the given names -- --- We only qualify the PNames with the interface name from 'FromModParam' in --- 'ogSource', if any. We don't qualify with the 'ModPath'. +-- We only qualify the PNames with the interface name from 'ogFromParam'. We +-- don't qualify with the 'ogModule'. namingEnvFromNames :: Set Name -> NamingEnv namingEnvFromNames xs = NamingEnv (foldl' add mempty xs) where diff --git a/src/Cryptol/ModuleSystem/Renamer/Imports.hs b/src/Cryptol/ModuleSystem/Renamer/Imports.hs index 682fa4a4c..17e20880b 100644 --- a/src/Cryptol/ModuleSystem/Renamer/Imports.hs +++ b/src/Cryptol/ModuleSystem/Renamer/Imports.hs @@ -67,10 +67,11 @@ import Cryptol.Utils.Ident(ModName,ModPath(..),Namespace(..),OrigName(..)) import Cryptol.Parser.AST ( ImportG(..),PName, ModuleInstanceArgs(..), ImpName(..) ) -import Cryptol.ModuleSystem.Binds (Mod(..), TopDef(..), modNested, ModKind(..)) +import Cryptol.ModuleSystem.Binds + ( Mod(..), TopDef(..), modNested, ModKind(..), newFunctorInst ) import Cryptol.ModuleSystem.Name - ( Name, Supply, SupplyT, runSupplyT, liftSupply, freshNameFor - , asOrigName, nameIdent, nameTopModule ) + ( Name, Supply, SupplyT, runSupplyT, asOrigName, nameIdent + , nameTopModule ) import Cryptol.ModuleSystem.Names(Names(..)) import Cryptol.ModuleSystem.NamingEnv ( NamingEnv(..), lookupNS, shadowing, travNamingEnv @@ -511,7 +512,7 @@ doInstantiate keepArgs mpath def s = (newDef, Set.foldl' doSub newS nestedToDo) instName :: Name -> SupplyT (M.StateT (Set (Name,Name)) M.Id) Name instName x = - do y <- liftSupply (freshNameFor mpath x) + do y <- newFunctorInst mpath x when (x `Set.member` rmodNested def) (M.lift (M.sets_ (Set.insert (x,y)))) pure y diff --git a/src/Cryptol/Parser/Name.hs b/src/Cryptol/Parser/Name.hs index 68826655d..4647585f7 100644 --- a/src/Cryptol/Parser/Name.hs +++ b/src/Cryptol/Parser/Name.hs @@ -46,16 +46,15 @@ mkUnqual = UnQual mkQual :: ModName -> Ident -> PName mkQual = Qual --- | We only qualify the 'PName' with the interface name from 'FromModParam' in --- 'ogSource', if any. We don't qualify with the 'ModPath'. +-- | We only qualify the 'PName' with the interface name from 'ogFromParam'. We +-- don't qualify with the 'ogModule'. fromOrigName :: OrigName -> PName fromOrigName og = toPName (ogName og) where toPName = - case ogSource og of - FromDefinition -> UnQual - FromFunctorInst -> UnQual - FromModParam sig -> Qual (identToModName sig) + case ogFromParam og of + Nothing -> UnQual + Just sig -> Qual (identToModName sig) getModName :: PName -> Maybe ModName getModName (Qual ns _) = Just ns diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index 62d2b552a..c6e278727 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -14,8 +14,8 @@ import Cryptol.Utils.Panic(panic) import Cryptol.Utils.Ident(Ident,Namespace(..),ModPath,isInfixIdent) import Cryptol.Parser.Position (Range,Located(..), thing) import qualified Cryptol.Parser.AST as P -import Cryptol.ModuleSystem.Binds(newModParam) -import Cryptol.ModuleSystem.Name(nameIdent, nameLoc) +import Cryptol.ModuleSystem.Binds(newFunctorInst) +import Cryptol.ModuleSystem.Name(nameIdent) import Cryptol.ModuleSystem.NamingEnv (NamingEnv(..), modParamNamingEnv, shadowing, without) import Cryptol.ModuleSystem.Interface @@ -220,14 +220,14 @@ checkArg mpath (r,expect,actual') = do let as = Set.fromList (map (qual . mtpParam) (Map.elems (mpnTypes params))) cs = map thing (mpnConstraints params) - check = checkSimpleParameterValue r paramName + check = checkSimpleParameterValue r (mpName expect) qual a = (mpQual expect, a) fs <- Map.mapMaybeWithKey (\_ v -> v) <$> mapM check (mpnFuns params) pure (ParamInst as cs (Map.mapKeys qual fs)) definedInst = - do (tRens, tSyns, tInstMaps) <- unzip3 <$> mapM - (checkParamType mpath r paramName tyMap) (Map.toList (mpnTypes params)) + do (tRens, tSyns, tInstMaps) <- unzip3 <$> + mapM (checkParamType mpath r tyMap) (Map.toList (mpnTypes params)) let renSu = listParamSubst (concat tRens) {- Note: the constraints from the signature are already added to the @@ -236,7 +236,7 @@ checkArg mpath (r,expect,actual') = (vDecls, vInstMaps) <- - mapAndUnzipM (checkParamValue mpath r paramName vMap) + mapAndUnzipM (checkParamValue mpath r vMap) [ s { mvpType = apSubst renSu (mvpType s) } | s <- Map.elems (mpnFuns params) ] @@ -245,10 +245,9 @@ checkArg mpath (r,expect,actual') = params = mpParameters expect - paramName = mpName expect -- Things provided by the argument module - tyMap :: Map Ident (Name, Kind, Type) + tyMap :: Map Ident (Kind, Type) vMap :: Map Ident (Name, Schema) (tyMap,vMap) = case actual' of @@ -258,7 +257,7 @@ checkArg mpath (r,expect,actual') = ) where ps = mpParameters mp - fromTP tp = (mtpName tp, mtpKind tp, TVar (TVBound (mtpParam tp))) + fromTP tp = (mtpKind tp, TVar (TVBound (mtpParam tp))) fromVP vp = (mvpName vp, mvpType vp) UseModule actual -> @@ -278,9 +277,9 @@ checkArg mpath (r,expect,actual') = decls = filterIfaceDecls isLocal (ifDefines actual) fromD d = (ifDeclName d, ifDeclSig d) - fromTS ts = (tsName ts, kindOf ts, tsDef ts) - fromNewtype nt = (ntName nt, kindOf nt, TNewtype nt []) - fromPrimT pt = (atName pt, kindOf pt, TCon (abstractTypeTC pt) []) + fromTS ts = (kindOf ts, tsDef ts) + fromNewtype nt = (kindOf nt, TNewtype nt []) + fromPrimT pt = (kindOf pt, TCon (abstractTypeTC pt) []) AddDeclParams -> panic "checkArg" ["AddDeclParams"] @@ -297,9 +296,7 @@ nameMapToIdentMap f m = checkParamType :: ModPath {- ^ The new module we are creating -} -> Range {- ^ Location for error reporting -} -> - Ident {- ^ Name of the _module_ parameter - (not value) -} -> - Map Ident (Name,Kind,Type) {- ^ Actual types -} -> + Map Ident (Kind,Type) {- ^ Actual types -} -> (Name,ModTParam) {- ^ Type parameter -} -> InferM ([(TParam,Type)], Map Name TySyn, Map Name Name) {- ^ Mapping from parameter name to actual type (for type substitution), @@ -308,7 +305,7 @@ checkParamType :: type synonyms are fully inlined into types at this point), and a map from the old type name to the fresh type name (for instantiation) -} -checkParamType mpath r modParamName tyMap (name,mp) = +checkParamType mpath r tyMap (name,mp) = let i = nameIdent name expectK = mtpKind mp in @@ -316,12 +313,12 @@ checkParamType mpath r modParamName tyMap (name,mp) = Nothing -> do recordErrorLoc (Just r) (FunctorInstanceMissingName NSType i) pure ([], Map.empty, Map.empty) - Just (actualName,actualK,actualT) -> + Just (actualK,actualT) -> do unless (expectK == actualK) (recordErrorLoc (Just r) (KindMismatch (Just (TVFromModParam name)) expectK actualK)) - name' <- newModParam mpath modParamName (nameLoc actualName) name + name' <- newFunctorInst mpath name let tySyn = TySyn { tsName = name' , tsParams = [] , tsConstraints = [] @@ -336,14 +333,13 @@ checkParamType mpath r modParamName tyMap (name,mp) = checkParamValue :: ModPath {- ^ The new module we are creating -} -> Range {- ^ Location for error reporting -} -> - Ident {- ^ Name of the _module_ parameter (not value) -} -> Map Ident (Name,Schema) {- ^ Actual values -} -> ModVParam {- ^ The parameter we are checking -} -> InferM ([Decl], Map Name Name) {- ^ Decl mapping a new name to the actual value, and a map from the value param name in the functor to the new name (for instantiation) -} -checkParamValue mpath r modParamName vMap mp = +checkParamValue mpath r vMap mp = let name = mvpName mp i = nameIdent name expectT = mvpType mp @@ -353,7 +349,7 @@ checkParamValue mpath r modParamName vMap mp = pure ([], Map.empty) Just actual -> do e <- mkParamDef r (name,expectT) actual - name' <- newModParam mpath modParamName (nameLoc (fst actual)) name + name' <- newFunctorInst mpath name let d = Decl { dName = name' , dSignature = expectT , dDefinition = DExpr e diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs index 712d870bb..311361bba 100644 --- a/src/Cryptol/Utils/Ident.hs +++ b/src/Cryptol/Utils/Ident.hs @@ -64,7 +64,7 @@ module Cryptol.Utils.Ident -- * Original names , OrigName(..) , OrigSource(..) - , ogFromModParam + , ogIsModParam -- * Identifiers for primitives , PrimIdent(..) @@ -259,19 +259,21 @@ data OrigName = OrigName , ogModule :: ModPath , ogSource :: OrigSource , ogName :: Ident + , ogFromParam :: !(Maybe Ident) + -- ^ Does this name come from a module parameter } deriving (Eq,Ord,Show,Generic,NFData) -- | Describes where a top-level name came from data OrigSource = FromDefinition | FromFunctorInst - | FromModParam Ident + | FromModParam deriving (Eq,Ord,Show,Generic,NFData) -- | Returns true iff the 'ogSource' of the given 'OrigName' is 'FromModParam' -ogFromModParam :: OrigName -> Bool -ogFromModParam og = case ogSource og of - FromModParam _ -> True +ogIsModParam :: OrigName -> Bool +ogIsModParam og = case ogSource og of + FromModParam -> True _ -> False diff --git a/src/Cryptol/Utils/PP.hs b/src/Cryptol/Utils/PP.hs index 166ee6e0c..d151156a2 100644 --- a/src/Cryptol/Utils/PP.hs +++ b/src/Cryptol/Utils/PP.hs @@ -410,16 +410,16 @@ instance PP OrigName where UnQualified -> pp (ogName og) Qualified m -> ppQual (TopModule m) (pp (ogName og)) NotInScope -> ppQual (ogModule og) - case ogSource og of - FromModParam x -> pp x <.> "::" <.> pp (ogName og) - _ -> pp (ogName og) + case ogFromParam og of + Just x -> pp x <.> "::" <.> pp (ogName og) + Nothing -> pp (ogName og) where - ppQual mo x = - case mo of - TopModule m - | m == exprModName -> x - | otherwise -> pp m <.> "::" <.> x - Nested m y -> ppQual m (pp y <.> "::" <.> x) + ppQual mo x = + case mo of + TopModule m + | m == exprModName -> x + | otherwise -> pp m <.> "::" <.> x + Nested m y -> ppQual m (pp y <.> "::" <.> x) instance PP Namespace where ppPrec _ ns = From 999ba7b5b3c9e8b107cad92ece4771b987fd4de2 Mon Sep 17 00:00:00 2001 From: Bretton Date: Tue, 8 Aug 2023 17:07:46 -0700 Subject: [PATCH 09/17] Add tests for #1455 --- tests/issues/issue1455/F.cry | 6 + tests/issues/issue1455/G.cry | 7 + tests/issues/issue1455/I.cry | 8 + tests/issues/issue1455/Inst1.cry | 1 + tests/issues/issue1455/Inst2.cry | 1 + tests/issues/issue1455/Inst3.cry | 1 + tests/issues/issue1455/M.cry | 6 + tests/issues/issue1455_1.icry | 13 ++ tests/issues/issue1455_1.icry.stdout | 259 +++++++++++++++++++++++++ tests/issues/issue1455_2.icry | 9 + tests/issues/issue1455_2.icry.stdout | 257 +++++++++++++++++++++++++ tests/issues/issue1455_3.icry | 15 ++ tests/issues/issue1455_3.icry.stdout | 275 +++++++++++++++++++++++++++ 13 files changed, 858 insertions(+) create mode 100644 tests/issues/issue1455/F.cry create mode 100644 tests/issues/issue1455/G.cry create mode 100644 tests/issues/issue1455/I.cry create mode 100644 tests/issues/issue1455/Inst1.cry create mode 100644 tests/issues/issue1455/Inst2.cry create mode 100644 tests/issues/issue1455/Inst3.cry create mode 100644 tests/issues/issue1455/M.cry create mode 100644 tests/issues/issue1455_1.icry create mode 100644 tests/issues/issue1455_1.icry.stdout create mode 100644 tests/issues/issue1455_2.icry create mode 100644 tests/issues/issue1455_2.icry.stdout create mode 100644 tests/issues/issue1455_3.icry create mode 100644 tests/issues/issue1455_3.icry.stdout diff --git a/tests/issues/issue1455/F.cry b/tests/issues/issue1455/F.cry new file mode 100644 index 000000000..fdca6dd69 --- /dev/null +++ b/tests/issues/issue1455/F.cry @@ -0,0 +1,6 @@ +module F where + +import interface I + +a = x + 1 +b = y + 1 diff --git a/tests/issues/issue1455/G.cry b/tests/issues/issue1455/G.cry new file mode 100644 index 000000000..8810fb9eb --- /dev/null +++ b/tests/issues/issue1455/G.cry @@ -0,0 +1,7 @@ +module G where + +import interface I + +import F { interface I } + +c = y + b diff --git a/tests/issues/issue1455/I.cry b/tests/issues/issue1455/I.cry new file mode 100644 index 000000000..13797a12e --- /dev/null +++ b/tests/issues/issue1455/I.cry @@ -0,0 +1,8 @@ +interface module I where + +type n : # +type m = 2 * n +type constraint (fin n, n >= 1) + +x : [n] +y : [m] diff --git a/tests/issues/issue1455/Inst1.cry b/tests/issues/issue1455/Inst1.cry new file mode 100644 index 000000000..ac0e3fc03 --- /dev/null +++ b/tests/issues/issue1455/Inst1.cry @@ -0,0 +1 @@ +module Inst = F { M } diff --git a/tests/issues/issue1455/Inst2.cry b/tests/issues/issue1455/Inst2.cry new file mode 100644 index 000000000..ba18209bc --- /dev/null +++ b/tests/issues/issue1455/Inst2.cry @@ -0,0 +1 @@ +module Inst2 = F { _ } diff --git a/tests/issues/issue1455/Inst3.cry b/tests/issues/issue1455/Inst3.cry new file mode 100644 index 000000000..6581dbfbe --- /dev/null +++ b/tests/issues/issue1455/Inst3.cry @@ -0,0 +1 @@ +module Inst3 = G { M } diff --git a/tests/issues/issue1455/M.cry b/tests/issues/issue1455/M.cry new file mode 100644 index 000000000..87d07072b --- /dev/null +++ b/tests/issues/issue1455/M.cry @@ -0,0 +1,6 @@ +module M where + +type n = 4 + +x = 3 +y = 5 diff --git a/tests/issues/issue1455_1.icry b/tests/issues/issue1455_1.icry new file mode 100644 index 000000000..80b1453cd --- /dev/null +++ b/tests/issues/issue1455_1.icry @@ -0,0 +1,13 @@ +:l issue1455/Inst1.cry +`n : Integer +`m : Integer +x +y +:t x +:t y +a +b +:t a +:t b +a + 2 +:browse diff --git a/tests/issues/issue1455_1.icry.stdout b/tests/issues/issue1455_1.icry.stdout new file mode 100644 index 000000000..fc2f6e3c4 --- /dev/null +++ b/tests/issues/issue1455_1.icry.stdout @@ -0,0 +1,259 @@ +Loading module Cryptol +Loading module Cryptol +Loading interface module I +Loading module F +Loading module M +Loading module Inst1 +4 +8 +0x3 +0x05 +x : [4] +y : [8] +0x4 +0x06 +a : [4] +b : [m] +0x6 +Type Synonyms +============= + + From Cryptol + ------------ + + type Bool = Bit + type Char = [8] + type lg2 n = width (max 1 n - 1) + type String n = [n]Char + type Word n = [n] + + From Inst1 + ---------- + + type m = 8 + type n = 4 + +Constraint Synonyms +=================== + + From Cryptol + ------------ + + type constraint i < j = j >= 1 + i + type constraint i <= j = j >= i + type constraint i > j = i >= 1 + j + +Primitive Types +=============== + + From Cryptol + ------------ + + (!=) : # -> # -> Prop + (==) : # -> # -> Prop + (>=) : # -> # -> Prop + (+) : # -> # -> # + (-) : # -> # -> # + (%) : # -> # -> # + (%^) : # -> # -> # + (*) : # -> # -> # + (/) : # -> # -> # + (/^) : # -> # -> # + (^^) : # -> # -> # + Bit : * + Cmp : * -> Prop + Eq : * -> Prop + FLiteral : # -> # -> # -> * -> Prop + Field : * -> Prop + fin : # -> Prop + Integer : * + Integral : * -> Prop + inf : # + Literal : # -> * -> Prop + LiteralLessThan : # -> * -> Prop + Logic : * -> Prop + lengthFromThenTo : # -> # -> # -> # + max : # -> # -> # + min : # -> # -> # + prime : # -> Prop + Rational : * + Ring : * -> Prop + Round : * -> Prop + SignedCmp : * -> Prop + width : # -> # + Z : # -> * + Zero : * -> Prop + +Symbols +======= + + From + ------------------ + + it : [4] + + From Cryptol + ------------ + + (/.) : {a} (Field a) => a -> a -> a + (==>) : Bit -> Bit -> Bit + (\/) : Bit -> Bit -> Bit + (/\) : Bit -> Bit -> Bit + (!=) : {a} (Eq a) => a -> a -> Bit + (!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit + (==) : {a} (Eq a) => a -> a -> Bit + (===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit + (<) : {a} (Cmp a) => a -> a -> Bit + (<$) : {a} (SignedCmp a) => a -> a -> Bit + (<=) : {a} (Cmp a) => a -> a -> Bit + (<=$) : {a} (SignedCmp a) => a -> a -> Bit + (>) : {a} (Cmp a) => a -> a -> Bit + (>$) : {a} (SignedCmp a) => a -> a -> Bit + (>=) : {a} (Cmp a) => a -> a -> Bit + (>=$) : {a} (SignedCmp a) => a -> a -> Bit + (||) : {a} (Logic a) => a -> a -> a + (^) : {a} (Logic a) => a -> a -> a + (&&) : {a} (Logic a) => a -> a -> a + (#) : {front, back, a} (fin front) => [front]a -> [back]a -> [front + back]a + (<<) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (<<<) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a + (>>) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n] + (>>>) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a + (+) : {a} (Ring a) => a -> a -> a + (-) : {a} (Ring a) => a -> a -> a + (%) : {a} (Integral a) => a -> a -> a + (%$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + (*) : {a} (Ring a) => a -> a -> a + (/) : {a} (Integral a) => a -> a -> a + (/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + (^^) : {a, e} (Ring a, Integral e) => a -> e -> a + (!) : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a + (!!) : {n, k, ix, a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a + (@) : {n, a, ix} (Integral ix) => [n]a -> ix -> a + (@@) : {n, k, ix, a} (Integral ix) => [n]a -> [k]ix -> [k]a + abs : {a} (Cmp a, Ring a) => a -> a + all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit + and : {n} (fin n) => [n] -> Bit + any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit + assert : {a, n} (fin n) => Bit -> String n -> a -> a + carry : {n} (fin n) => [n] -> [n] -> Bit + ceiling : {a} (Round a) => a -> Integer + complement : {a} (Logic a) => a -> a + curry : {a, b, c} ((a, b) -> c) -> a -> b -> c + deepseq : {a, b} (Eq a) => a -> b -> b + demote : {val, rep} (Literal val rep) => rep + drop : {front, back, a} (fin front) => [front + back]a -> [back]a + elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit + error : {a, n} (fin n) => String n -> a + False : Bit + floor : {a} (Round a) => a -> Integer + foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a + foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a + foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b + foldr' : {n, a, b} (fin n, Eq b) => (a -> b -> b) -> b -> [n]a -> b + fraction : {m, n, r, a} (FLiteral m n r a) => a + fromInteger : {a} (Ring a) => Integer -> a + fromThenTo : + {first, next, last, a, len} + (fin first, fin next, fin last, Literal first a, Literal next a, + Literal last a, first != next, + lengthFromThenTo first next last == len) => + [len]a + fromTo : + {first, last, a} + (fin last, last >= first, Literal last a) => + [1 + (last - first)]a + fromToBy : + {first, last, stride, a} + (fin last, fin stride, stride >= 1, last >= first, Literal last a) => + [1 + (last - first) / stride]a + fromToByLessThan : + {first, bound, stride, a} + (fin first, fin stride, stride >= 1, bound >= first, + LiteralLessThan bound a) => + [(bound - first) /^ stride]a + fromToDownBy : + {first, last, stride, a} + (fin first, fin stride, stride >= 1, first >= last, Literal first a) => + [1 + (first - last) / stride]a + fromToDownByGreaterThan : + {first, bound, stride, a} + (fin first, fin stride, stride >= 1, first >= bound, Literal first a) => + [(first - bound) /^ stride]a + fromToLessThan : + {first, bound, a} + (fin first, bound >= first, LiteralLessThan bound a) => + [bound - first]a + fromZ : {n} (fin n, n >= 1) => Z n -> Integer + generate : + {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a + groupBy : {each, parts, a} (fin each) => [each * parts]a -> [parts][each]a + head : {n, a} [1 + n]a -> a + infFrom : {a} (Integral a) => a -> [inf]a + infFromThen : {a} (Integral a) => a -> a -> [inf]a + iterate : {a} (a -> a) -> a -> [inf]a + join : {parts, each, a} (fin each) => [parts][each]a -> [parts * each]a + last : {n, a} (fin n) => [1 + n]a -> a + length : {n, a, b} (fin n, Literal n b) => [n]a -> b + lg2 : {n} (fin n) => [n] -> [n] + map : {n, a, b} (a -> b) -> [n]a -> [n]b + max : {a} (Cmp a) => a -> a -> a + min : {a} (Cmp a) => a -> a -> a + negate : {a} (Ring a) => a -> a + number : {val, rep} (Literal val rep) => rep + or : {n} (fin n) => [n] -> Bit + parmap : {a, b, n} (Eq b, fin n) => (a -> b) -> [n]a -> [n]b + pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u] + pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v] + pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + (u + v)] + product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a + random : {a} [256] -> a + ratio : Integer -> Integer -> Rational + recip : {a} (Field a) => a -> a + repeat : {n, a} a -> [n]a + reverse : {n, a} (fin n) => [n]a -> [n]a + rnf : {a} (Eq a) => a -> a + roundAway : {a} (Round a) => a -> Integer + roundToEven : {a} (Round a) => a -> Integer + sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + scanl : {n, a, b} (a -> b -> a) -> a -> [n]b -> [1 + n]a + scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b + scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m] + sort : {a, n} (Cmp a, fin n) => [n]a -> [n]a + sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a + split : {parts, each, a} (fin each) => [parts * each]a -> [parts][each]a + splitAt : + {front, back, a} (fin front) => [front + back]a -> ([front]a, [back]a) + sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a + True : Bit + tail : {n, a} [1 + n]a -> [n]a + take : {front, back, a} [front + back]a -> [front]a + toInteger : {a} (Integral a) => a -> Integer + toSignedInteger : {n} (fin n, n >= 1) => [n] -> Integer + trace : {n, a, b} (fin n) => String n -> a -> b -> b + traceVal : {n, a} (fin n) => String n -> a -> a + transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a + trunc : {a} (Round a) => a -> Integer + uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c + undefined : {a} a + update : {n, a, ix} (Integral ix) => [n]a -> ix -> a -> [n]a + updateEnd : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a -> [n]a + updates : + {n, k, ix, a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + updatesEnd : + {n, k, ix, a} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + zero : {a} (Zero a) => a + zext : {m, n} (fin m, m >= n) => [n] -> [m] + zip : {n, a, b} [n]a -> [n]b -> [n](a, b) + zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c + + From Inst1 + ---------- + + a : [4] + b : [m] + x : [4] + y : [8] + diff --git a/tests/issues/issue1455_2.icry b/tests/issues/issue1455_2.icry new file mode 100644 index 000000000..ad16d4561 --- /dev/null +++ b/tests/issues/issue1455_2.icry @@ -0,0 +1,9 @@ +:l issue1455/Inst2.cry +`n +`(m 3) : Integer +x +y +:t a +:t b +1 + 1 : Integer +:browse diff --git a/tests/issues/issue1455_2.icry.stdout b/tests/issues/issue1455_2.icry.stdout new file mode 100644 index 000000000..ac4c2449c --- /dev/null +++ b/tests/issues/issue1455_2.icry.stdout @@ -0,0 +1,257 @@ +Loading module Cryptol +Loading module Cryptol +Loading interface module I +Loading module F +Loading module Inst2 + +[error] at issue1455_2.icry:2:2--2:3 + Type not in scope: n +6 + +[error] at issue1455_2.icry:4:1--4:2 + Value not in scope: x + +[error] at issue1455_2.icry:5:1--5:2 + Value not in scope: y +a : {n} (fin n, n >= 1, fin n, n >= 1) => {x : [n], y : [2 * n]} -> [n] +b : {n} (fin n, n >= 1, fin n, n >= 1) => {x : [n], y : [2 * n]} -> [m n] +2 +Type Synonyms +============= + + From Cryptol + ------------ + + type Bool = Bit + type Char = [8] + type lg2 n = width (max 1 n - 1) + type String n = [n]Char + type Word n = [n] + + From Inst2 + ---------- + + type m n = 2 * n + +Constraint Synonyms +=================== + + From Cryptol + ------------ + + type constraint i < j = j >= 1 + i + type constraint i <= j = j >= i + type constraint i > j = i >= 1 + j + +Primitive Types +=============== + + From Cryptol + ------------ + + (!=) : # -> # -> Prop + (==) : # -> # -> Prop + (>=) : # -> # -> Prop + (+) : # -> # -> # + (-) : # -> # -> # + (%) : # -> # -> # + (%^) : # -> # -> # + (*) : # -> # -> # + (/) : # -> # -> # + (/^) : # -> # -> # + (^^) : # -> # -> # + Bit : * + Cmp : * -> Prop + Eq : * -> Prop + FLiteral : # -> # -> # -> * -> Prop + Field : * -> Prop + fin : # -> Prop + Integer : * + Integral : * -> Prop + inf : # + Literal : # -> * -> Prop + LiteralLessThan : # -> * -> Prop + Logic : * -> Prop + lengthFromThenTo : # -> # -> # -> # + max : # -> # -> # + min : # -> # -> # + prime : # -> Prop + Rational : * + Ring : * -> Prop + Round : * -> Prop + SignedCmp : * -> Prop + width : # -> # + Z : # -> * + Zero : * -> Prop + +Symbols +======= + + From + ------------------ + + it : Integer + + From Cryptol + ------------ + + (/.) : {a} (Field a) => a -> a -> a + (==>) : Bit -> Bit -> Bit + (\/) : Bit -> Bit -> Bit + (/\) : Bit -> Bit -> Bit + (!=) : {a} (Eq a) => a -> a -> Bit + (!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit + (==) : {a} (Eq a) => a -> a -> Bit + (===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit + (<) : {a} (Cmp a) => a -> a -> Bit + (<$) : {a} (SignedCmp a) => a -> a -> Bit + (<=) : {a} (Cmp a) => a -> a -> Bit + (<=$) : {a} (SignedCmp a) => a -> a -> Bit + (>) : {a} (Cmp a) => a -> a -> Bit + (>$) : {a} (SignedCmp a) => a -> a -> Bit + (>=) : {a} (Cmp a) => a -> a -> Bit + (>=$) : {a} (SignedCmp a) => a -> a -> Bit + (||) : {a} (Logic a) => a -> a -> a + (^) : {a} (Logic a) => a -> a -> a + (&&) : {a} (Logic a) => a -> a -> a + (#) : {front, back, a} (fin front) => [front]a -> [back]a -> [front + back]a + (<<) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (<<<) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a + (>>) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n] + (>>>) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a + (+) : {a} (Ring a) => a -> a -> a + (-) : {a} (Ring a) => a -> a -> a + (%) : {a} (Integral a) => a -> a -> a + (%$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + (*) : {a} (Ring a) => a -> a -> a + (/) : {a} (Integral a) => a -> a -> a + (/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + (^^) : {a, e} (Ring a, Integral e) => a -> e -> a + (!) : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a + (!!) : {n, k, ix, a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a + (@) : {n, a, ix} (Integral ix) => [n]a -> ix -> a + (@@) : {n, k, ix, a} (Integral ix) => [n]a -> [k]ix -> [k]a + abs : {a} (Cmp a, Ring a) => a -> a + all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit + and : {n} (fin n) => [n] -> Bit + any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit + assert : {a, n} (fin n) => Bit -> String n -> a -> a + carry : {n} (fin n) => [n] -> [n] -> Bit + ceiling : {a} (Round a) => a -> Integer + complement : {a} (Logic a) => a -> a + curry : {a, b, c} ((a, b) -> c) -> a -> b -> c + deepseq : {a, b} (Eq a) => a -> b -> b + demote : {val, rep} (Literal val rep) => rep + drop : {front, back, a} (fin front) => [front + back]a -> [back]a + elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit + error : {a, n} (fin n) => String n -> a + False : Bit + floor : {a} (Round a) => a -> Integer + foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a + foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a + foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b + foldr' : {n, a, b} (fin n, Eq b) => (a -> b -> b) -> b -> [n]a -> b + fraction : {m, n, r, a} (FLiteral m n r a) => a + fromInteger : {a} (Ring a) => Integer -> a + fromThenTo : + {first, next, last, a, len} + (fin first, fin next, fin last, Literal first a, Literal next a, + Literal last a, first != next, + lengthFromThenTo first next last == len) => + [len]a + fromTo : + {first, last, a} + (fin last, last >= first, Literal last a) => + [1 + (last - first)]a + fromToBy : + {first, last, stride, a} + (fin last, fin stride, stride >= 1, last >= first, Literal last a) => + [1 + (last - first) / stride]a + fromToByLessThan : + {first, bound, stride, a} + (fin first, fin stride, stride >= 1, bound >= first, + LiteralLessThan bound a) => + [(bound - first) /^ stride]a + fromToDownBy : + {first, last, stride, a} + (fin first, fin stride, stride >= 1, first >= last, Literal first a) => + [1 + (first - last) / stride]a + fromToDownByGreaterThan : + {first, bound, stride, a} + (fin first, fin stride, stride >= 1, first >= bound, Literal first a) => + [(first - bound) /^ stride]a + fromToLessThan : + {first, bound, a} + (fin first, bound >= first, LiteralLessThan bound a) => + [bound - first]a + fromZ : {n} (fin n, n >= 1) => Z n -> Integer + generate : + {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a + groupBy : {each, parts, a} (fin each) => [each * parts]a -> [parts][each]a + head : {n, a} [1 + n]a -> a + infFrom : {a} (Integral a) => a -> [inf]a + infFromThen : {a} (Integral a) => a -> a -> [inf]a + iterate : {a} (a -> a) -> a -> [inf]a + join : {parts, each, a} (fin each) => [parts][each]a -> [parts * each]a + last : {n, a} (fin n) => [1 + n]a -> a + length : {n, a, b} (fin n, Literal n b) => [n]a -> b + lg2 : {n} (fin n) => [n] -> [n] + map : {n, a, b} (a -> b) -> [n]a -> [n]b + max : {a} (Cmp a) => a -> a -> a + min : {a} (Cmp a) => a -> a -> a + negate : {a} (Ring a) => a -> a + number : {val, rep} (Literal val rep) => rep + or : {n} (fin n) => [n] -> Bit + parmap : {a, b, n} (Eq b, fin n) => (a -> b) -> [n]a -> [n]b + pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u] + pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v] + pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + (u + v)] + product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a + random : {a} [256] -> a + ratio : Integer -> Integer -> Rational + recip : {a} (Field a) => a -> a + repeat : {n, a} a -> [n]a + reverse : {n, a} (fin n) => [n]a -> [n]a + rnf : {a} (Eq a) => a -> a + roundAway : {a} (Round a) => a -> Integer + roundToEven : {a} (Round a) => a -> Integer + sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + scanl : {n, a, b} (a -> b -> a) -> a -> [n]b -> [1 + n]a + scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b + scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m] + sort : {a, n} (Cmp a, fin n) => [n]a -> [n]a + sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a + split : {parts, each, a} (fin each) => [parts * each]a -> [parts][each]a + splitAt : + {front, back, a} (fin front) => [front + back]a -> ([front]a, [back]a) + sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a + True : Bit + tail : {n, a} [1 + n]a -> [n]a + take : {front, back, a} [front + back]a -> [front]a + toInteger : {a} (Integral a) => a -> Integer + toSignedInteger : {n} (fin n, n >= 1) => [n] -> Integer + trace : {n, a, b} (fin n) => String n -> a -> b -> b + traceVal : {n, a} (fin n) => String n -> a -> a + transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a + trunc : {a} (Round a) => a -> Integer + uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c + undefined : {a} a + update : {n, a, ix} (Integral ix) => [n]a -> ix -> a -> [n]a + updateEnd : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a -> [n]a + updates : + {n, k, ix, a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + updatesEnd : + {n, k, ix, a} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + zero : {a} (Zero a) => a + zext : {m, n} (fin m, m >= n) => [n] -> [m] + zip : {n, a, b} [n]a -> [n]b -> [n](a, b) + zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c + + From Inst2 + ---------- + + a : {n} (fin n, n >= 1, fin n, n >= 1) => {x : [n], y : [2 * n]} -> [n] + b : {n} (fin n, n >= 1, fin n, n >= 1) => {x : [n], y : [2 * n]} -> [m n] + diff --git a/tests/issues/issue1455_3.icry b/tests/issues/issue1455_3.icry new file mode 100644 index 000000000..ed32645f5 --- /dev/null +++ b/tests/issues/issue1455_3.icry @@ -0,0 +1,15 @@ +:l issue1455/Inst3.cry +`n : Integer +`m : Integer +x +y +:t x +:t y +a +b +c +:t a +:t b +:t c +c + 2 +:browse diff --git a/tests/issues/issue1455_3.icry.stdout b/tests/issues/issue1455_3.icry.stdout new file mode 100644 index 000000000..fca48b2de --- /dev/null +++ b/tests/issues/issue1455_3.icry.stdout @@ -0,0 +1,275 @@ +Loading module Cryptol +Loading module Cryptol +Loading interface module I +Loading module F +Loading module G +Loading module M +Loading module Inst3 +4 +8 +0x3 +0x05 +x : [4] +y : [8] +0x4 +0x06 +0x0b +a : [4] +b : [8] +c : [m] +0x0d +Submodules +========== + + From Inst3 + ---------- + + import of F at issue1455/G.cry:5:1--5:9 + +Type Synonyms +============= + + From Cryptol + ------------ + + type Bool = Bit + type Char = [8] + type lg2 n = width (max 1 n - 1) + type String n = [n]Char + type Word n = [n] + + From Inst3 + ---------- + + type m = 8 + type n = 4 + +Constraint Synonyms +=================== + + From Cryptol + ------------ + + type constraint i < j = j >= 1 + i + type constraint i <= j = j >= i + type constraint i > j = i >= 1 + j + +Primitive Types +=============== + + From Cryptol + ------------ + + (!=) : # -> # -> Prop + (==) : # -> # -> Prop + (>=) : # -> # -> Prop + (+) : # -> # -> # + (-) : # -> # -> # + (%) : # -> # -> # + (%^) : # -> # -> # + (*) : # -> # -> # + (/) : # -> # -> # + (/^) : # -> # -> # + (^^) : # -> # -> # + Bit : * + Cmp : * -> Prop + Eq : * -> Prop + FLiteral : # -> # -> # -> * -> Prop + Field : * -> Prop + fin : # -> Prop + Integer : * + Integral : * -> Prop + inf : # + Literal : # -> * -> Prop + LiteralLessThan : # -> * -> Prop + Logic : * -> Prop + lengthFromThenTo : # -> # -> # -> # + max : # -> # -> # + min : # -> # -> # + prime : # -> Prop + Rational : * + Ring : * -> Prop + Round : * -> Prop + SignedCmp : * -> Prop + width : # -> # + Z : # -> * + Zero : * -> Prop + +Symbols +======= + + From + ------------------ + + it : [8] + + From Cryptol + ------------ + + (/.) : {a} (Field a) => a -> a -> a + (==>) : Bit -> Bit -> Bit + (\/) : Bit -> Bit -> Bit + (/\) : Bit -> Bit -> Bit + (!=) : {a} (Eq a) => a -> a -> Bit + (!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit + (==) : {a} (Eq a) => a -> a -> Bit + (===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit + (<) : {a} (Cmp a) => a -> a -> Bit + (<$) : {a} (SignedCmp a) => a -> a -> Bit + (<=) : {a} (Cmp a) => a -> a -> Bit + (<=$) : {a} (SignedCmp a) => a -> a -> Bit + (>) : {a} (Cmp a) => a -> a -> Bit + (>$) : {a} (SignedCmp a) => a -> a -> Bit + (>=) : {a} (Cmp a) => a -> a -> Bit + (>=$) : {a} (SignedCmp a) => a -> a -> Bit + (||) : {a} (Logic a) => a -> a -> a + (^) : {a} (Logic a) => a -> a -> a + (&&) : {a} (Logic a) => a -> a -> a + (#) : {front, back, a} (fin front) => [front]a -> [back]a -> [front + back]a + (<<) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (<<<) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a + (>>) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n] + (>>>) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a + (+) : {a} (Ring a) => a -> a -> a + (-) : {a} (Ring a) => a -> a -> a + (%) : {a} (Integral a) => a -> a -> a + (%$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + (*) : {a} (Ring a) => a -> a -> a + (/) : {a} (Integral a) => a -> a -> a + (/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + (^^) : {a, e} (Ring a, Integral e) => a -> e -> a + (!) : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a + (!!) : {n, k, ix, a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a + (@) : {n, a, ix} (Integral ix) => [n]a -> ix -> a + (@@) : {n, k, ix, a} (Integral ix) => [n]a -> [k]ix -> [k]a + abs : {a} (Cmp a, Ring a) => a -> a + all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit + and : {n} (fin n) => [n] -> Bit + any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit + assert : {a, n} (fin n) => Bit -> String n -> a -> a + carry : {n} (fin n) => [n] -> [n] -> Bit + ceiling : {a} (Round a) => a -> Integer + complement : {a} (Logic a) => a -> a + curry : {a, b, c} ((a, b) -> c) -> a -> b -> c + deepseq : {a, b} (Eq a) => a -> b -> b + demote : {val, rep} (Literal val rep) => rep + drop : {front, back, a} (fin front) => [front + back]a -> [back]a + elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit + error : {a, n} (fin n) => String n -> a + False : Bit + floor : {a} (Round a) => a -> Integer + foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a + foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a + foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b + foldr' : {n, a, b} (fin n, Eq b) => (a -> b -> b) -> b -> [n]a -> b + fraction : {m, n, r, a} (FLiteral m n r a) => a + fromInteger : {a} (Ring a) => Integer -> a + fromThenTo : + {first, next, last, a, len} + (fin first, fin next, fin last, Literal first a, Literal next a, + Literal last a, first != next, + lengthFromThenTo first next last == len) => + [len]a + fromTo : + {first, last, a} + (fin last, last >= first, Literal last a) => + [1 + (last - first)]a + fromToBy : + {first, last, stride, a} + (fin last, fin stride, stride >= 1, last >= first, Literal last a) => + [1 + (last - first) / stride]a + fromToByLessThan : + {first, bound, stride, a} + (fin first, fin stride, stride >= 1, bound >= first, + LiteralLessThan bound a) => + [(bound - first) /^ stride]a + fromToDownBy : + {first, last, stride, a} + (fin first, fin stride, stride >= 1, first >= last, Literal first a) => + [1 + (first - last) / stride]a + fromToDownByGreaterThan : + {first, bound, stride, a} + (fin first, fin stride, stride >= 1, first >= bound, Literal first a) => + [(first - bound) /^ stride]a + fromToLessThan : + {first, bound, a} + (fin first, bound >= first, LiteralLessThan bound a) => + [bound - first]a + fromZ : {n} (fin n, n >= 1) => Z n -> Integer + generate : + {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a + groupBy : {each, parts, a} (fin each) => [each * parts]a -> [parts][each]a + head : {n, a} [1 + n]a -> a + infFrom : {a} (Integral a) => a -> [inf]a + infFromThen : {a} (Integral a) => a -> a -> [inf]a + iterate : {a} (a -> a) -> a -> [inf]a + join : {parts, each, a} (fin each) => [parts][each]a -> [parts * each]a + last : {n, a} (fin n) => [1 + n]a -> a + length : {n, a, b} (fin n, Literal n b) => [n]a -> b + lg2 : {n} (fin n) => [n] -> [n] + map : {n, a, b} (a -> b) -> [n]a -> [n]b + max : {a} (Cmp a) => a -> a -> a + min : {a} (Cmp a) => a -> a -> a + negate : {a} (Ring a) => a -> a + number : {val, rep} (Literal val rep) => rep + or : {n} (fin n) => [n] -> Bit + parmap : {a, b, n} (Eq b, fin n) => (a -> b) -> [n]a -> [n]b + pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u] + pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v] + pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + (u + v)] + product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a + random : {a} [256] -> a + ratio : Integer -> Integer -> Rational + recip : {a} (Field a) => a -> a + repeat : {n, a} a -> [n]a + reverse : {n, a} (fin n) => [n]a -> [n]a + rnf : {a} (Eq a) => a -> a + roundAway : {a} (Round a) => a -> Integer + roundToEven : {a} (Round a) => a -> Integer + sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + scanl : {n, a, b} (a -> b -> a) -> a -> [n]b -> [1 + n]a + scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b + scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m] + sort : {a, n} (Cmp a, fin n) => [n]a -> [n]a + sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a + split : {parts, each, a} (fin each) => [parts * each]a -> [parts][each]a + splitAt : + {front, back, a} (fin front) => [front + back]a -> ([front]a, [back]a) + sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a + True : Bit + tail : {n, a} [1 + n]a -> [n]a + take : {front, back, a} [front + back]a -> [front]a + toInteger : {a} (Integral a) => a -> Integer + toSignedInteger : {n} (fin n, n >= 1) => [n] -> Integer + trace : {n, a, b} (fin n) => String n -> a -> b -> b + traceVal : {n, a} (fin n) => String n -> a -> a + transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a + trunc : {a} (Round a) => a -> Integer + uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c + undefined : {a} a + update : {n, a, ix} (Integral ix) => [n]a -> ix -> a -> [n]a + updateEnd : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a -> [n]a + updates : + {n, k, ix, a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + updatesEnd : + {n, k, ix, a} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + zero : {a} (Zero a) => a + zext : {m, n} (fin m, m >= n) => [n] -> [m] + zip : {n, a, b} [n]a -> [n]b -> [n](a, b) + zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c + + From Inst3 + ---------- + + c : [m] + x : [4] + y : [8] + + From Inst3::import of F at issue1455/G.cry:5:1--5:9 + --------------------------------------------------- + + a : [4] + b : [8] + From bff4add0997f0a5885088b4fd356950f14a2bb21 Mon Sep 17 00:00:00 2001 From: Bretton Date: Tue, 8 Aug 2023 17:42:35 -0700 Subject: [PATCH 10/17] Fix tests/issues/issue1455/Inst1.cry --- tests/issues/issue1455/Inst1.cry | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/issues/issue1455/Inst1.cry b/tests/issues/issue1455/Inst1.cry index ac0e3fc03..e86afd8c4 100644 --- a/tests/issues/issue1455/Inst1.cry +++ b/tests/issues/issue1455/Inst1.cry @@ -1 +1 @@ -module Inst = F { M } +module Inst1 = F { M } From fbb2e37bdd4900cc911488c6fe4a68b636c0de8b Mon Sep 17 00:00:00 2001 From: Bretton Date: Tue, 8 Aug 2023 17:45:12 -0700 Subject: [PATCH 11/17] Add tests for #1561 --- tests/issues/issue1561/F.cry | 10 + tests/issues/issue1561/G.cry | 10 + tests/issues/issue1561/I.cry | 8 + tests/issues/issue1561/Inst1.cry | 1 + tests/issues/issue1561/Inst2.cry | 1 + tests/issues/issue1561/M.cry | 6 + tests/issues/issue1561/N.cry | 6 + tests/issues/issue1561_1.icry | 23 +++ tests/issues/issue1561_1.icry.stdout | 276 +++++++++++++++++++++++++ tests/issues/issue1561_2.icry | 27 +++ tests/issues/issue1561_2.icry.stdout | 288 +++++++++++++++++++++++++++ 11 files changed, 656 insertions(+) create mode 100644 tests/issues/issue1561/F.cry create mode 100644 tests/issues/issue1561/G.cry create mode 100644 tests/issues/issue1561/I.cry create mode 100644 tests/issues/issue1561/Inst1.cry create mode 100644 tests/issues/issue1561/Inst2.cry create mode 100644 tests/issues/issue1561/M.cry create mode 100644 tests/issues/issue1561/N.cry create mode 100644 tests/issues/issue1561_1.icry create mode 100644 tests/issues/issue1561_1.icry.stdout create mode 100644 tests/issues/issue1561_2.icry create mode 100644 tests/issues/issue1561_2.icry.stdout diff --git a/tests/issues/issue1561/F.cry b/tests/issues/issue1561/F.cry new file mode 100644 index 000000000..964a21666 --- /dev/null +++ b/tests/issues/issue1561/F.cry @@ -0,0 +1,10 @@ +module F where + +import interface I +import interface I as J + +a = x + 1 +b = y + 2 + +ja = J::x + 1 +jb = J::y + 2 diff --git a/tests/issues/issue1561/G.cry b/tests/issues/issue1561/G.cry new file mode 100644 index 000000000..97876a588 --- /dev/null +++ b/tests/issues/issue1561/G.cry @@ -0,0 +1,10 @@ +module G where + +import interface I as J +import interface I as K + +ja = J::x + 1 +jb = J::y + 2 + +ka = K::x + 1 +kb = K::y + 2 diff --git a/tests/issues/issue1561/I.cry b/tests/issues/issue1561/I.cry new file mode 100644 index 000000000..13797a12e --- /dev/null +++ b/tests/issues/issue1561/I.cry @@ -0,0 +1,8 @@ +interface module I where + +type n : # +type m = 2 * n +type constraint (fin n, n >= 1) + +x : [n] +y : [m] diff --git a/tests/issues/issue1561/Inst1.cry b/tests/issues/issue1561/Inst1.cry new file mode 100644 index 000000000..ba045c37b --- /dev/null +++ b/tests/issues/issue1561/Inst1.cry @@ -0,0 +1 @@ +module Inst1 = F { I = M, J = N } diff --git a/tests/issues/issue1561/Inst2.cry b/tests/issues/issue1561/Inst2.cry new file mode 100644 index 000000000..d030b6375 --- /dev/null +++ b/tests/issues/issue1561/Inst2.cry @@ -0,0 +1 @@ +module Inst2 = G { J = M, K = N } diff --git a/tests/issues/issue1561/M.cry b/tests/issues/issue1561/M.cry new file mode 100644 index 000000000..08f619a4e --- /dev/null +++ b/tests/issues/issue1561/M.cry @@ -0,0 +1,6 @@ +module M where + +type n = 2 + +x = 3 +y = 15 diff --git a/tests/issues/issue1561/N.cry b/tests/issues/issue1561/N.cry new file mode 100644 index 000000000..842947b4f --- /dev/null +++ b/tests/issues/issue1561/N.cry @@ -0,0 +1,6 @@ +module N where + +type n = 3 + +x = 5 +y = 20 diff --git a/tests/issues/issue1561_1.icry b/tests/issues/issue1561_1.icry new file mode 100644 index 000000000..3a6f5c52f --- /dev/null +++ b/tests/issues/issue1561_1.icry @@ -0,0 +1,23 @@ +:l issue1561/Inst1.cry +`n : Integer +`m : Integer +`J::n : Integer +`J::m : Integer +x +y +J::x +J::y +:t x +:t y +:t J::x +:t J::y +a +b +ja +jb +:t a +:t b +:t ja +:t jb +a + 2 +:browse diff --git a/tests/issues/issue1561_1.icry.stdout b/tests/issues/issue1561_1.icry.stdout new file mode 100644 index 000000000..93e2da94e --- /dev/null +++ b/tests/issues/issue1561_1.icry.stdout @@ -0,0 +1,276 @@ +Loading module Cryptol +Loading module Cryptol +Loading interface module I +Loading module F +Loading module N +Loading module M +Loading module Inst1 +2 +4 +3 +6 +0x3 +0xf +0x5 +0x14 +x : [2] +y : [4] +J::x : [3] +J::y : [6] +0x0 +0x1 +0x6 +0x16 +a : [2] +b : [m] +ja : [3] +jb : [J::m] +0x2 +Type Synonyms +============= + + From Cryptol + ------------ + + type Bool = Bit + type Char = [8] + type lg2 n = width (max 1 n - 1) + type String n = [n]Char + type Word n = [n] + + From Inst1 + ---------- + + type m = 4 + type n = 2 + type J::m = 6 + type J::n = 3 + +Constraint Synonyms +=================== + + From Cryptol + ------------ + + type constraint i < j = j >= 1 + i + type constraint i <= j = j >= i + type constraint i > j = i >= 1 + j + +Primitive Types +=============== + + From Cryptol + ------------ + + (!=) : # -> # -> Prop + (==) : # -> # -> Prop + (>=) : # -> # -> Prop + (+) : # -> # -> # + (-) : # -> # -> # + (%) : # -> # -> # + (%^) : # -> # -> # + (*) : # -> # -> # + (/) : # -> # -> # + (/^) : # -> # -> # + (^^) : # -> # -> # + Bit : * + Cmp : * -> Prop + Eq : * -> Prop + FLiteral : # -> # -> # -> * -> Prop + Field : * -> Prop + fin : # -> Prop + Integer : * + Integral : * -> Prop + inf : # + Literal : # -> * -> Prop + LiteralLessThan : # -> * -> Prop + Logic : * -> Prop + lengthFromThenTo : # -> # -> # -> # + max : # -> # -> # + min : # -> # -> # + prime : # -> Prop + Rational : * + Ring : * -> Prop + Round : * -> Prop + SignedCmp : * -> Prop + width : # -> # + Z : # -> * + Zero : * -> Prop + +Symbols +======= + + From + ------------------ + + it : [2] + + From Cryptol + ------------ + + (/.) : {a} (Field a) => a -> a -> a + (==>) : Bit -> Bit -> Bit + (\/) : Bit -> Bit -> Bit + (/\) : Bit -> Bit -> Bit + (!=) : {a} (Eq a) => a -> a -> Bit + (!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit + (==) : {a} (Eq a) => a -> a -> Bit + (===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit + (<) : {a} (Cmp a) => a -> a -> Bit + (<$) : {a} (SignedCmp a) => a -> a -> Bit + (<=) : {a} (Cmp a) => a -> a -> Bit + (<=$) : {a} (SignedCmp a) => a -> a -> Bit + (>) : {a} (Cmp a) => a -> a -> Bit + (>$) : {a} (SignedCmp a) => a -> a -> Bit + (>=) : {a} (Cmp a) => a -> a -> Bit + (>=$) : {a} (SignedCmp a) => a -> a -> Bit + (||) : {a} (Logic a) => a -> a -> a + (^) : {a} (Logic a) => a -> a -> a + (&&) : {a} (Logic a) => a -> a -> a + (#) : {front, back, a} (fin front) => [front]a -> [back]a -> [front + back]a + (<<) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (<<<) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a + (>>) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n] + (>>>) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a + (+) : {a} (Ring a) => a -> a -> a + (-) : {a} (Ring a) => a -> a -> a + (%) : {a} (Integral a) => a -> a -> a + (%$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + (*) : {a} (Ring a) => a -> a -> a + (/) : {a} (Integral a) => a -> a -> a + (/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + (^^) : {a, e} (Ring a, Integral e) => a -> e -> a + (!) : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a + (!!) : {n, k, ix, a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a + (@) : {n, a, ix} (Integral ix) => [n]a -> ix -> a + (@@) : {n, k, ix, a} (Integral ix) => [n]a -> [k]ix -> [k]a + abs : {a} (Cmp a, Ring a) => a -> a + all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit + and : {n} (fin n) => [n] -> Bit + any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit + assert : {a, n} (fin n) => Bit -> String n -> a -> a + carry : {n} (fin n) => [n] -> [n] -> Bit + ceiling : {a} (Round a) => a -> Integer + complement : {a} (Logic a) => a -> a + curry : {a, b, c} ((a, b) -> c) -> a -> b -> c + deepseq : {a, b} (Eq a) => a -> b -> b + demote : {val, rep} (Literal val rep) => rep + drop : {front, back, a} (fin front) => [front + back]a -> [back]a + elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit + error : {a, n} (fin n) => String n -> a + False : Bit + floor : {a} (Round a) => a -> Integer + foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a + foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a + foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b + foldr' : {n, a, b} (fin n, Eq b) => (a -> b -> b) -> b -> [n]a -> b + fraction : {m, n, r, a} (FLiteral m n r a) => a + fromInteger : {a} (Ring a) => Integer -> a + fromThenTo : + {first, next, last, a, len} + (fin first, fin next, fin last, Literal first a, Literal next a, + Literal last a, first != next, + lengthFromThenTo first next last == len) => + [len]a + fromTo : + {first, last, a} + (fin last, last >= first, Literal last a) => + [1 + (last - first)]a + fromToBy : + {first, last, stride, a} + (fin last, fin stride, stride >= 1, last >= first, Literal last a) => + [1 + (last - first) / stride]a + fromToByLessThan : + {first, bound, stride, a} + (fin first, fin stride, stride >= 1, bound >= first, + LiteralLessThan bound a) => + [(bound - first) /^ stride]a + fromToDownBy : + {first, last, stride, a} + (fin first, fin stride, stride >= 1, first >= last, Literal first a) => + [1 + (first - last) / stride]a + fromToDownByGreaterThan : + {first, bound, stride, a} + (fin first, fin stride, stride >= 1, first >= bound, Literal first a) => + [(first - bound) /^ stride]a + fromToLessThan : + {first, bound, a} + (fin first, bound >= first, LiteralLessThan bound a) => + [bound - first]a + fromZ : {n} (fin n, n >= 1) => Z n -> Integer + generate : + {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a + groupBy : {each, parts, a} (fin each) => [each * parts]a -> [parts][each]a + head : {n, a} [1 + n]a -> a + infFrom : {a} (Integral a) => a -> [inf]a + infFromThen : {a} (Integral a) => a -> a -> [inf]a + iterate : {a} (a -> a) -> a -> [inf]a + join : {parts, each, a} (fin each) => [parts][each]a -> [parts * each]a + last : {n, a} (fin n) => [1 + n]a -> a + length : {n, a, b} (fin n, Literal n b) => [n]a -> b + lg2 : {n} (fin n) => [n] -> [n] + map : {n, a, b} (a -> b) -> [n]a -> [n]b + max : {a} (Cmp a) => a -> a -> a + min : {a} (Cmp a) => a -> a -> a + negate : {a} (Ring a) => a -> a + number : {val, rep} (Literal val rep) => rep + or : {n} (fin n) => [n] -> Bit + parmap : {a, b, n} (Eq b, fin n) => (a -> b) -> [n]a -> [n]b + pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u] + pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v] + pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + (u + v)] + product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a + random : {a} [256] -> a + ratio : Integer -> Integer -> Rational + recip : {a} (Field a) => a -> a + repeat : {n, a} a -> [n]a + reverse : {n, a} (fin n) => [n]a -> [n]a + rnf : {a} (Eq a) => a -> a + roundAway : {a} (Round a) => a -> Integer + roundToEven : {a} (Round a) => a -> Integer + sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + scanl : {n, a, b} (a -> b -> a) -> a -> [n]b -> [1 + n]a + scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b + scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m] + sort : {a, n} (Cmp a, fin n) => [n]a -> [n]a + sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a + split : {parts, each, a} (fin each) => [parts * each]a -> [parts][each]a + splitAt : + {front, back, a} (fin front) => [front + back]a -> ([front]a, [back]a) + sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a + True : Bit + tail : {n, a} [1 + n]a -> [n]a + take : {front, back, a} [front + back]a -> [front]a + toInteger : {a} (Integral a) => a -> Integer + toSignedInteger : {n} (fin n, n >= 1) => [n] -> Integer + trace : {n, a, b} (fin n) => String n -> a -> b -> b + traceVal : {n, a} (fin n) => String n -> a -> a + transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a + trunc : {a} (Round a) => a -> Integer + uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c + undefined : {a} a + update : {n, a, ix} (Integral ix) => [n]a -> ix -> a -> [n]a + updateEnd : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a -> [n]a + updates : + {n, k, ix, a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + updatesEnd : + {n, k, ix, a} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + zero : {a} (Zero a) => a + zext : {m, n} (fin m, m >= n) => [n] -> [m] + zip : {n, a, b} [n]a -> [n]b -> [n](a, b) + zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c + + From Inst1 + ---------- + + a : [2] + b : [m] + ja : [3] + jb : [J::m] + x : [2] + y : [4] + J::x : [3] + J::y : [6] + diff --git a/tests/issues/issue1561_2.icry b/tests/issues/issue1561_2.icry new file mode 100644 index 000000000..8fdff0d3f --- /dev/null +++ b/tests/issues/issue1561_2.icry @@ -0,0 +1,27 @@ +:l issue1561/Inst2.cry +`J::n : Integer +`J::m : Integer +`K::n : Integer +`K::m : Integer +J::x +J::y +K::x +K::y +:t J::x +:t J::y +:t K::x +:t K::y +`n +`m +x +y +ja +jb +ka +kb +:t ja +:t jb +:t ka +:t kb +ja + 2 +:browse diff --git a/tests/issues/issue1561_2.icry.stdout b/tests/issues/issue1561_2.icry.stdout new file mode 100644 index 000000000..1c9131383 --- /dev/null +++ b/tests/issues/issue1561_2.icry.stdout @@ -0,0 +1,288 @@ +Loading module Cryptol +Loading module Cryptol +Loading interface module I +Loading module G +Loading module N +Loading module M +Loading module Inst2 +2 +4 +3 +6 +0x3 +0xf +0x5 +0x14 +J::x : [2] +J::y : [4] +K::x : [3] +K::y : [6] + +[error] at issue1561_2.icry:14:2--14:3 + Type not in scope: n + +[error] at issue1561_2.icry:15:2--15:3 + Type not in scope: m + +[error] at issue1561_2.icry:16:1--16:2 + Value not in scope: x + +[error] at issue1561_2.icry:17:1--17:2 + Value not in scope: y +0x0 +0x1 +0x6 +0x16 +ja : [2] +jb : [J::m] +ka : [3] +kb : [K::m] +0x2 +Type Synonyms +============= + + From Cryptol + ------------ + + type Bool = Bit + type Char = [8] + type lg2 n = width (max 1 n - 1) + type String n = [n]Char + type Word n = [n] + + From Inst2 + ---------- + + type J::m = 4 + type J::n = 2 + type K::m = 6 + type K::n = 3 + +Constraint Synonyms +=================== + + From Cryptol + ------------ + + type constraint i < j = j >= 1 + i + type constraint i <= j = j >= i + type constraint i > j = i >= 1 + j + +Primitive Types +=============== + + From Cryptol + ------------ + + (!=) : # -> # -> Prop + (==) : # -> # -> Prop + (>=) : # -> # -> Prop + (+) : # -> # -> # + (-) : # -> # -> # + (%) : # -> # -> # + (%^) : # -> # -> # + (*) : # -> # -> # + (/) : # -> # -> # + (/^) : # -> # -> # + (^^) : # -> # -> # + Bit : * + Cmp : * -> Prop + Eq : * -> Prop + FLiteral : # -> # -> # -> * -> Prop + Field : * -> Prop + fin : # -> Prop + Integer : * + Integral : * -> Prop + inf : # + Literal : # -> * -> Prop + LiteralLessThan : # -> * -> Prop + Logic : * -> Prop + lengthFromThenTo : # -> # -> # -> # + max : # -> # -> # + min : # -> # -> # + prime : # -> Prop + Rational : * + Ring : * -> Prop + Round : * -> Prop + SignedCmp : * -> Prop + width : # -> # + Z : # -> * + Zero : * -> Prop + +Symbols +======= + + From + ------------------ + + it : [2] + + From Cryptol + ------------ + + (/.) : {a} (Field a) => a -> a -> a + (==>) : Bit -> Bit -> Bit + (\/) : Bit -> Bit -> Bit + (/\) : Bit -> Bit -> Bit + (!=) : {a} (Eq a) => a -> a -> Bit + (!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit + (==) : {a} (Eq a) => a -> a -> Bit + (===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit + (<) : {a} (Cmp a) => a -> a -> Bit + (<$) : {a} (SignedCmp a) => a -> a -> Bit + (<=) : {a} (Cmp a) => a -> a -> Bit + (<=$) : {a} (SignedCmp a) => a -> a -> Bit + (>) : {a} (Cmp a) => a -> a -> Bit + (>$) : {a} (SignedCmp a) => a -> a -> Bit + (>=) : {a} (Cmp a) => a -> a -> Bit + (>=$) : {a} (SignedCmp a) => a -> a -> Bit + (||) : {a} (Logic a) => a -> a -> a + (^) : {a} (Logic a) => a -> a -> a + (&&) : {a} (Logic a) => a -> a -> a + (#) : {front, back, a} (fin front) => [front]a -> [back]a -> [front + back]a + (<<) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (<<<) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a + (>>) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n] + (>>>) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a + (+) : {a} (Ring a) => a -> a -> a + (-) : {a} (Ring a) => a -> a -> a + (%) : {a} (Integral a) => a -> a -> a + (%$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + (*) : {a} (Ring a) => a -> a -> a + (/) : {a} (Integral a) => a -> a -> a + (/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + (^^) : {a, e} (Ring a, Integral e) => a -> e -> a + (!) : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a + (!!) : {n, k, ix, a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a + (@) : {n, a, ix} (Integral ix) => [n]a -> ix -> a + (@@) : {n, k, ix, a} (Integral ix) => [n]a -> [k]ix -> [k]a + abs : {a} (Cmp a, Ring a) => a -> a + all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit + and : {n} (fin n) => [n] -> Bit + any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit + assert : {a, n} (fin n) => Bit -> String n -> a -> a + carry : {n} (fin n) => [n] -> [n] -> Bit + ceiling : {a} (Round a) => a -> Integer + complement : {a} (Logic a) => a -> a + curry : {a, b, c} ((a, b) -> c) -> a -> b -> c + deepseq : {a, b} (Eq a) => a -> b -> b + demote : {val, rep} (Literal val rep) => rep + drop : {front, back, a} (fin front) => [front + back]a -> [back]a + elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit + error : {a, n} (fin n) => String n -> a + False : Bit + floor : {a} (Round a) => a -> Integer + foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a + foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a + foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b + foldr' : {n, a, b} (fin n, Eq b) => (a -> b -> b) -> b -> [n]a -> b + fraction : {m, n, r, a} (FLiteral m n r a) => a + fromInteger : {a} (Ring a) => Integer -> a + fromThenTo : + {first, next, last, a, len} + (fin first, fin next, fin last, Literal first a, Literal next a, + Literal last a, first != next, + lengthFromThenTo first next last == len) => + [len]a + fromTo : + {first, last, a} + (fin last, last >= first, Literal last a) => + [1 + (last - first)]a + fromToBy : + {first, last, stride, a} + (fin last, fin stride, stride >= 1, last >= first, Literal last a) => + [1 + (last - first) / stride]a + fromToByLessThan : + {first, bound, stride, a} + (fin first, fin stride, stride >= 1, bound >= first, + LiteralLessThan bound a) => + [(bound - first) /^ stride]a + fromToDownBy : + {first, last, stride, a} + (fin first, fin stride, stride >= 1, first >= last, Literal first a) => + [1 + (first - last) / stride]a + fromToDownByGreaterThan : + {first, bound, stride, a} + (fin first, fin stride, stride >= 1, first >= bound, Literal first a) => + [(first - bound) /^ stride]a + fromToLessThan : + {first, bound, a} + (fin first, bound >= first, LiteralLessThan bound a) => + [bound - first]a + fromZ : {n} (fin n, n >= 1) => Z n -> Integer + generate : + {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a + groupBy : {each, parts, a} (fin each) => [each * parts]a -> [parts][each]a + head : {n, a} [1 + n]a -> a + infFrom : {a} (Integral a) => a -> [inf]a + infFromThen : {a} (Integral a) => a -> a -> [inf]a + iterate : {a} (a -> a) -> a -> [inf]a + join : {parts, each, a} (fin each) => [parts][each]a -> [parts * each]a + last : {n, a} (fin n) => [1 + n]a -> a + length : {n, a, b} (fin n, Literal n b) => [n]a -> b + lg2 : {n} (fin n) => [n] -> [n] + map : {n, a, b} (a -> b) -> [n]a -> [n]b + max : {a} (Cmp a) => a -> a -> a + min : {a} (Cmp a) => a -> a -> a + negate : {a} (Ring a) => a -> a + number : {val, rep} (Literal val rep) => rep + or : {n} (fin n) => [n] -> Bit + parmap : {a, b, n} (Eq b, fin n) => (a -> b) -> [n]a -> [n]b + pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u] + pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v] + pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + (u + v)] + product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a + random : {a} [256] -> a + ratio : Integer -> Integer -> Rational + recip : {a} (Field a) => a -> a + repeat : {n, a} a -> [n]a + reverse : {n, a} (fin n) => [n]a -> [n]a + rnf : {a} (Eq a) => a -> a + roundAway : {a} (Round a) => a -> Integer + roundToEven : {a} (Round a) => a -> Integer + sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + scanl : {n, a, b} (a -> b -> a) -> a -> [n]b -> [1 + n]a + scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b + scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m] + sort : {a, n} (Cmp a, fin n) => [n]a -> [n]a + sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a + split : {parts, each, a} (fin each) => [parts * each]a -> [parts][each]a + splitAt : + {front, back, a} (fin front) => [front + back]a -> ([front]a, [back]a) + sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a + True : Bit + tail : {n, a} [1 + n]a -> [n]a + take : {front, back, a} [front + back]a -> [front]a + toInteger : {a} (Integral a) => a -> Integer + toSignedInteger : {n} (fin n, n >= 1) => [n] -> Integer + trace : {n, a, b} (fin n) => String n -> a -> b -> b + traceVal : {n, a} (fin n) => String n -> a -> a + transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a + trunc : {a} (Round a) => a -> Integer + uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c + undefined : {a} a + update : {n, a, ix} (Integral ix) => [n]a -> ix -> a -> [n]a + updateEnd : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a -> [n]a + updates : + {n, k, ix, a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + updatesEnd : + {n, k, ix, a} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + zero : {a} (Zero a) => a + zext : {m, n} (fin m, m >= n) => [n] -> [m] + zip : {n, a, b} [n]a -> [n]b -> [n](a, b) + zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c + + From Inst2 + ---------- + + ja : [2] + jb : [J::m] + ka : [3] + kb : [K::m] + J::x : [2] + J::y : [4] + K::x : [3] + K::y : [6] + From edff7d30886618873493477cf5881b82a4d2c2a2 Mon Sep 17 00:00:00 2001 From: Bretton Date: Tue, 8 Aug 2023 18:34:13 -0700 Subject: [PATCH 12/17] Fix test output for issues/issue1455_3 on windows --- tests/issues/issue1455_3.icry.stdout.mingw32 | 275 +++++++++++++++++++ 1 file changed, 275 insertions(+) create mode 100644 tests/issues/issue1455_3.icry.stdout.mingw32 diff --git a/tests/issues/issue1455_3.icry.stdout.mingw32 b/tests/issues/issue1455_3.icry.stdout.mingw32 new file mode 100644 index 000000000..82bc68f29 --- /dev/null +++ b/tests/issues/issue1455_3.icry.stdout.mingw32 @@ -0,0 +1,275 @@ +Loading module Cryptol +Loading module Cryptol +Loading interface module I +Loading module F +Loading module G +Loading module M +Loading module Inst3 +4 +8 +0x3 +0x05 +x : [4] +y : [8] +0x4 +0x06 +0x0b +a : [4] +b : [8] +c : [m] +0x0d +Submodules +========== + + From Inst3 + ---------- + + import of F at issue1455\G.cry:5:1--5:9 + +Type Synonyms +============= + + From Cryptol + ------------ + + type Bool = Bit + type Char = [8] + type lg2 n = width (max 1 n - 1) + type String n = [n]Char + type Word n = [n] + + From Inst3 + ---------- + + type m = 8 + type n = 4 + +Constraint Synonyms +=================== + + From Cryptol + ------------ + + type constraint i < j = j >= 1 + i + type constraint i <= j = j >= i + type constraint i > j = i >= 1 + j + +Primitive Types +=============== + + From Cryptol + ------------ + + (!=) : # -> # -> Prop + (==) : # -> # -> Prop + (>=) : # -> # -> Prop + (+) : # -> # -> # + (-) : # -> # -> # + (%) : # -> # -> # + (%^) : # -> # -> # + (*) : # -> # -> # + (/) : # -> # -> # + (/^) : # -> # -> # + (^^) : # -> # -> # + Bit : * + Cmp : * -> Prop + Eq : * -> Prop + FLiteral : # -> # -> # -> * -> Prop + Field : * -> Prop + fin : # -> Prop + Integer : * + Integral : * -> Prop + inf : # + Literal : # -> * -> Prop + LiteralLessThan : # -> * -> Prop + Logic : * -> Prop + lengthFromThenTo : # -> # -> # -> # + max : # -> # -> # + min : # -> # -> # + prime : # -> Prop + Rational : * + Ring : * -> Prop + Round : * -> Prop + SignedCmp : * -> Prop + width : # -> # + Z : # -> * + Zero : * -> Prop + +Symbols +======= + + From + ------------------ + + it : [8] + + From Cryptol + ------------ + + (/.) : {a} (Field a) => a -> a -> a + (==>) : Bit -> Bit -> Bit + (\/) : Bit -> Bit -> Bit + (/\) : Bit -> Bit -> Bit + (!=) : {a} (Eq a) => a -> a -> Bit + (!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit + (==) : {a} (Eq a) => a -> a -> Bit + (===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit + (<) : {a} (Cmp a) => a -> a -> Bit + (<$) : {a} (SignedCmp a) => a -> a -> Bit + (<=) : {a} (Cmp a) => a -> a -> Bit + (<=$) : {a} (SignedCmp a) => a -> a -> Bit + (>) : {a} (Cmp a) => a -> a -> Bit + (>$) : {a} (SignedCmp a) => a -> a -> Bit + (>=) : {a} (Cmp a) => a -> a -> Bit + (>=$) : {a} (SignedCmp a) => a -> a -> Bit + (||) : {a} (Logic a) => a -> a -> a + (^) : {a} (Logic a) => a -> a -> a + (&&) : {a} (Logic a) => a -> a -> a + (#) : {front, back, a} (fin front) => [front]a -> [back]a -> [front + back]a + (<<) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (<<<) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a + (>>) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n] + (>>>) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a + (+) : {a} (Ring a) => a -> a -> a + (-) : {a} (Ring a) => a -> a -> a + (%) : {a} (Integral a) => a -> a -> a + (%$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + (*) : {a} (Ring a) => a -> a -> a + (/) : {a} (Integral a) => a -> a -> a + (/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + (^^) : {a, e} (Ring a, Integral e) => a -> e -> a + (!) : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a + (!!) : {n, k, ix, a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a + (@) : {n, a, ix} (Integral ix) => [n]a -> ix -> a + (@@) : {n, k, ix, a} (Integral ix) => [n]a -> [k]ix -> [k]a + abs : {a} (Cmp a, Ring a) => a -> a + all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit + and : {n} (fin n) => [n] -> Bit + any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit + assert : {a, n} (fin n) => Bit -> String n -> a -> a + carry : {n} (fin n) => [n] -> [n] -> Bit + ceiling : {a} (Round a) => a -> Integer + complement : {a} (Logic a) => a -> a + curry : {a, b, c} ((a, b) -> c) -> a -> b -> c + deepseq : {a, b} (Eq a) => a -> b -> b + demote : {val, rep} (Literal val rep) => rep + drop : {front, back, a} (fin front) => [front + back]a -> [back]a + elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit + error : {a, n} (fin n) => String n -> a + False : Bit + floor : {a} (Round a) => a -> Integer + foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a + foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a + foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b + foldr' : {n, a, b} (fin n, Eq b) => (a -> b -> b) -> b -> [n]a -> b + fraction : {m, n, r, a} (FLiteral m n r a) => a + fromInteger : {a} (Ring a) => Integer -> a + fromThenTo : + {first, next, last, a, len} + (fin first, fin next, fin last, Literal first a, Literal next a, + Literal last a, first != next, + lengthFromThenTo first next last == len) => + [len]a + fromTo : + {first, last, a} + (fin last, last >= first, Literal last a) => + [1 + (last - first)]a + fromToBy : + {first, last, stride, a} + (fin last, fin stride, stride >= 1, last >= first, Literal last a) => + [1 + (last - first) / stride]a + fromToByLessThan : + {first, bound, stride, a} + (fin first, fin stride, stride >= 1, bound >= first, + LiteralLessThan bound a) => + [(bound - first) /^ stride]a + fromToDownBy : + {first, last, stride, a} + (fin first, fin stride, stride >= 1, first >= last, Literal first a) => + [1 + (first - last) / stride]a + fromToDownByGreaterThan : + {first, bound, stride, a} + (fin first, fin stride, stride >= 1, first >= bound, Literal first a) => + [(first - bound) /^ stride]a + fromToLessThan : + {first, bound, a} + (fin first, bound >= first, LiteralLessThan bound a) => + [bound - first]a + fromZ : {n} (fin n, n >= 1) => Z n -> Integer + generate : + {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a + groupBy : {each, parts, a} (fin each) => [each * parts]a -> [parts][each]a + head : {n, a} [1 + n]a -> a + infFrom : {a} (Integral a) => a -> [inf]a + infFromThen : {a} (Integral a) => a -> a -> [inf]a + iterate : {a} (a -> a) -> a -> [inf]a + join : {parts, each, a} (fin each) => [parts][each]a -> [parts * each]a + last : {n, a} (fin n) => [1 + n]a -> a + length : {n, a, b} (fin n, Literal n b) => [n]a -> b + lg2 : {n} (fin n) => [n] -> [n] + map : {n, a, b} (a -> b) -> [n]a -> [n]b + max : {a} (Cmp a) => a -> a -> a + min : {a} (Cmp a) => a -> a -> a + negate : {a} (Ring a) => a -> a + number : {val, rep} (Literal val rep) => rep + or : {n} (fin n) => [n] -> Bit + parmap : {a, b, n} (Eq b, fin n) => (a -> b) -> [n]a -> [n]b + pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u] + pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v] + pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + (u + v)] + product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a + random : {a} [256] -> a + ratio : Integer -> Integer -> Rational + recip : {a} (Field a) => a -> a + repeat : {n, a} a -> [n]a + reverse : {n, a} (fin n) => [n]a -> [n]a + rnf : {a} (Eq a) => a -> a + roundAway : {a} (Round a) => a -> Integer + roundToEven : {a} (Round a) => a -> Integer + sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + scanl : {n, a, b} (a -> b -> a) -> a -> [n]b -> [1 + n]a + scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b + scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m] + sort : {a, n} (Cmp a, fin n) => [n]a -> [n]a + sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a + split : {parts, each, a} (fin each) => [parts * each]a -> [parts][each]a + splitAt : + {front, back, a} (fin front) => [front + back]a -> ([front]a, [back]a) + sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a + True : Bit + tail : {n, a} [1 + n]a -> [n]a + take : {front, back, a} [front + back]a -> [front]a + toInteger : {a} (Integral a) => a -> Integer + toSignedInteger : {n} (fin n, n >= 1) => [n] -> Integer + trace : {n, a, b} (fin n) => String n -> a -> b -> b + traceVal : {n, a} (fin n) => String n -> a -> a + transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a + trunc : {a} (Round a) => a -> Integer + uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c + undefined : {a} a + update : {n, a, ix} (Integral ix) => [n]a -> ix -> a -> [n]a + updateEnd : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a -> [n]a + updates : + {n, k, ix, a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + updatesEnd : + {n, k, ix, a} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + zero : {a} (Zero a) => a + zext : {m, n} (fin m, m >= n) => [n] -> [m] + zip : {n, a, b} [n]a -> [n]b -> [n](a, b) + zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c + + From Inst3 + ---------- + + c : [m] + x : [4] + y : [8] + + From Inst3::import of F at issue1455\G.cry:5:1--5:9 + --------------------------------------------------- + + a : [4] + b : [8] + From 064f391a045d4023f22bbb73e38e7027c4ff46b4 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 9 Aug 2023 16:30:11 -0700 Subject: [PATCH 13/17] Update CHANGES --- CHANGES.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 05d72c6fe..199f7801e 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,11 @@ +# UNRELEASED + +* Fixed #1556, #1237, and #1561. +* Fixed #1455, making anything in scope of the functor in scope at the REPL as + well when an instantiation of the functor is loaded and focused, + design choice (3) on the ticket. In particular, the prelude will be in scope. + + # 3.0.0 -- 2023-06-26 ## Language changes From 407d78c9e382fabf2afbc393cc15b147179cadd1 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 9 Aug 2023 16:30:32 -0700 Subject: [PATCH 14/17] Rename things, and add comments. --- src/Cryptol/ModuleSystem/Name.hs | 13 +++++++------ src/Cryptol/ModuleSystem/NamingEnv.hs | 10 +++++----- src/Cryptol/Parser/Name.hs | 9 +++++---- 3 files changed, 17 insertions(+), 15 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs index 8a6c57d2e..aff8e3468 100644 --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -29,7 +29,7 @@ module Cryptol.ModuleSystem.Name ( , nameLoc , nameFixity , nameNamespace - , asPName + , nameToDefPName , asPrim , asOrigName , nameModPath @@ -229,12 +229,13 @@ nameLoc = nLoc nameFixity :: Name -> Maybe Fixity nameFixity = nFixity --- | We only qualify the 'PName' with the interface name from 'ogFromParam'. We --- don't qualify with the 'ogModule'. -asPName :: Name -> PName -asPName n = +-- | Compute a `PName` for the definition site corresponding to the given +-- `Name`. Usually this is an unqualified name, but names that come +-- from module parameters are qualified with the corresponding parameter name. +nameToDefPName :: Name -> PName +nameToDefPName n = case nInfo n of - GlobalName _ og -> PName.fromOrigName og + GlobalName _ og -> PName.origNameToDefPName og LocalName _ txt -> PName.mkUnqual txt -- | Primtiives must be in a top level module, at least for now. diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index f8a08b123..fdd0dcce6 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -71,16 +71,16 @@ namingEnvNames (NamingEnv xs) = Just (One x) -> Set.singleton x Just (Ambig as) -> as --- | Get a naming environment for the given names --- --- We only qualify the PNames with the interface name from 'ogFromParam'. We --- don't qualify with the 'ogModule'. +-- | Get a naming environment for the given names. The `PName`s correspond +-- to the definition sites of the corresponding `Name`s, so typically they +-- will be unqualified. The exception is for names that comre from parameters, +-- which are qualified with the relevant parameter. namingEnvFromNames :: Set Name -> NamingEnv namingEnvFromNames xs = NamingEnv (foldl' add mempty xs) where add mp x = let ns = nameNamespace x in Map.insertWith (Map.unionWith (<>)) - ns (Map.singleton (asPName x) (One x)) + ns (Map.singleton (nameToDefPName x) (One x)) mp diff --git a/src/Cryptol/Parser/Name.hs b/src/Cryptol/Parser/Name.hs index 4647585f7..ddef23760 100644 --- a/src/Cryptol/Parser/Name.hs +++ b/src/Cryptol/Parser/Name.hs @@ -46,10 +46,11 @@ mkUnqual = UnQual mkQual :: ModName -> Ident -> PName mkQual = Qual --- | We only qualify the 'PName' with the interface name from 'ogFromParam'. We --- don't qualify with the 'ogModule'. -fromOrigName :: OrigName -> PName -fromOrigName og = toPName (ogName og) +-- | Compute a `PName` for the definition site corresponding to the given +-- `OrigName`. Usually this is an unqualified name, but names that come +-- from module parameters are qualified with the corresponding parameter name. +origNameToDefPName :: OrigName -> PName +origNameToDefPName og = toPName (ogName og) where toPName = case ogFromParam og of From f8ab523e4c6997715e9f6acb42852cc0b7109541 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 9 Aug 2023 16:42:36 -0700 Subject: [PATCH 15/17] Remove unused interface field. --- src/Cryptol/ModuleSystem/Interface.hs | 3 --- src/Cryptol/TypeCheck/Interface.hs | 1 - src/Cryptol/TypeCheck/ModuleInstance.hs | 1 - 3 files changed, 5 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Interface.hs b/src/Cryptol/ModuleSystem/Interface.hs index 7410bebca..66c947d0d 100644 --- a/src/Cryptol/ModuleSystem/Interface.hs +++ b/src/Cryptol/ModuleSystem/Interface.hs @@ -42,7 +42,6 @@ import Prelude () import Prelude.Compat import Cryptol.ModuleSystem.Name -import Cryptol.ModuleSystem.NamingEnv.Types import Cryptol.Utils.Ident (ModName, OrigName(..)) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.Fixity(Fixity) @@ -75,7 +74,6 @@ data IfaceNames name = IfaceNames , ifsNested :: Set Name -- ^ Things nested in this module , ifsDefines :: Set Name -- ^ Things defined in this module , ifsPublic :: Set Name -- ^ Subset of `ifsDefines` that is public - , ifsInScope :: NamingEnv -- ^ Things in scope in this module , ifsDoc :: !(Maybe Text) -- ^ Documentation } deriving (Show, Generic, NFData) @@ -89,7 +87,6 @@ emptyIface nm = Iface , ifsDefines = mempty , ifsPublic = mempty , ifsNested = mempty - , ifsInScope = mempty , ifsDoc = Nothing } , ifParams = mempty diff --git a/src/Cryptol/TypeCheck/Interface.hs b/src/Cryptol/TypeCheck/Interface.hs index c468a3669..3464635ce 100644 --- a/src/Cryptol/TypeCheck/Interface.hs +++ b/src/Cryptol/TypeCheck/Interface.hs @@ -32,7 +32,6 @@ genIfaceNames m = IfaceNames , ifsNested = mNested m , ifsDefines = genModDefines m , ifsPublic = allExported (mExports m) - , ifsInScope = mInScope m , ifsDoc = mDoc m } diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs index c5dfd3b3e..5839e916d 100644 --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -132,7 +132,6 @@ instance ModuleInstance name => ModuleInstance (IfaceNames name) where , ifsNested = doSet (ifsNested ns) , ifsDefines = doSet (ifsDefines ns) , ifsPublic = doSet (ifsPublic ns) - , ifsInScope = moduleInstance (ifsInScope ns) , ifsDoc = ifsDoc ns } From bcb60f2ef4e43218700205616af3466dacc08ba6 Mon Sep 17 00:00:00 2001 From: Bretton Date: Thu, 10 Aug 2023 15:29:12 -0700 Subject: [PATCH 16/17] Add missing interface type synonyms to instMap --- src/Cryptol/TypeCheck/Module.hs | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index c6e278727..4852591c6 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -5,6 +5,7 @@ import Data.List(partition,unzip4) import Data.Text(Text) import Data.Map(Map) import qualified Data.Map as Map +import qualified Data.Map.Merge.Strict as Map import Data.Set (Set) import qualified Data.Set as Set import Control.Monad(unless,forM_,mapAndUnzipM) @@ -43,7 +44,7 @@ doFunctorInst :: {- ^ Names in the enclosing scope of the instantiated module -} -> Maybe Text {- ^ Documentation -} -> InferM (Maybe TCTopEntity) -doFunctorInst m f as instMap enclosingInScope doc = +doFunctorInst m f as instMap0 enclosingInScope doc = inRange (srcRange m) do mf <- lookupFunctor (thing f) argIs <- checkArity (srcRange f) mf as @@ -51,6 +52,7 @@ doFunctorInst m f as instMap enclosingInScope doc = as2 <- mapM (checkArg mpath) argIs let (tySus,paramTySyns,decls,paramInstMaps) = unzip4 [ (su,ts,ds,im) | DefinedInst su ts ds im <- as2 ] + instMap <- addMissingTySyns mpath mf instMap0 let ?tSu = mergeDistinctSubst tySus ?vSu = instMap <> mconcat paramInstMaps let m1 = moduleInstance mf @@ -424,5 +426,21 @@ mkParamDef r (pname,wantedS) (arg,actualS) = applySubst res - - +-- | The instMap we get from the renamer will not contain the fresh names for +-- certain things in the functor generated in the typechecking stage, if we are +-- instantiating a functor that is in the same file, since renaming and +-- typechecking happens together with the instantiation. In particular, if the +-- functor's interface has type synonyms, they will only get copied over into +-- the functor in the typechecker, so the renamer will not see them. Here we +-- make the fresh names for those missing type synonyms and add them to the +-- instMap. +addMissingTySyns :: + ModPath {- ^ The new module we are creating -} -> + ModuleG () {- ^ The functor -} -> + Map Name Name {- ^ instMap we get from renamer -} -> + InferM (Map Name Name) {- ^ the complete instMap -} +addMissingTySyns mpath f = Map.mergeA + (Map.traverseMissing \name _ -> newFunctorInst mpath name) + Map.preserveMissing + (Map.zipWithMatched \_ _ name' -> name') + (mTySyns f) From fbfad1fd0c65c0fe873856eecb2bef2a9e3b18d1 Mon Sep 17 00:00:00 2001 From: Bretton Date: Thu, 10 Aug 2023 15:39:24 -0700 Subject: [PATCH 17/17] Add test for #1562 --- tests/issues/issue1562.cry | 13 +++++++++++++ tests/issues/issue1562.icry | 1 + tests/issues/issue1562.icry.stdout | 3 +++ 3 files changed, 17 insertions(+) create mode 100644 tests/issues/issue1562.cry create mode 100644 tests/issues/issue1562.icry create mode 100644 tests/issues/issue1562.icry.stdout diff --git a/tests/issues/issue1562.cry b/tests/issues/issue1562.cry new file mode 100644 index 000000000..7743cb74d --- /dev/null +++ b/tests/issues/issue1562.cry @@ -0,0 +1,13 @@ +interface submodule I where + type Zp = [8] + +submodule F where + import interface submodule I + +submodule M where + // this is unused, but just here because syntactically we cannot have an empty + // module + type Empty = Bit + +submodule F1 = submodule F { submodule M } +submodule F2 = submodule F { submodule M } diff --git a/tests/issues/issue1562.icry b/tests/issues/issue1562.icry new file mode 100644 index 000000000..4440eba98 --- /dev/null +++ b/tests/issues/issue1562.icry @@ -0,0 +1 @@ +:l issue1562.cry diff --git a/tests/issues/issue1562.icry.stdout b/tests/issues/issue1562.icry.stdout new file mode 100644 index 000000000..57a1d7a1c --- /dev/null +++ b/tests/issues/issue1562.icry.stdout @@ -0,0 +1,3 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main