GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-21 10:58:01 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #1559 from GaloisInc/T1455

Browse Source 
Make names in scope in functors accessible when their instantiations are loaded at the REPL
This commit is contained in:
Bretton 2023-08-10 17:06:09 -07:00 committed by GitHub
commit cd5d006277
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
48 changed files with 2123 additions and 155 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
CHANGES.md
View File

@ -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

1
cryptol.cabal
View File

@ -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,

6
src/Cryptol/ModuleSystem/Base.hs
View File

@ -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 ::

10
src/Cryptol/ModuleSystem/Binds.hs
View File

@ -13,6 +13,7 @@ module Cryptol.ModuleSystem.Binds
, topModuleDefs
, topDeclsDefs
, newModParam
, newFunctorInst
, InModule(..)
, ifaceToMod
, ifaceSigToMod
@ -125,7 +126,7 @@ ifaceSigToMod ps = Mod
, modState = ()
}
where
env = modParamsNamingEnv ps
env = modParamNamesNamingEnv ps
@ -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.

25
src/Cryptol/ModuleSystem/Name.hs
View File

@ -29,6 +29,7 @@ module Cryptol.ModuleSystem.Name (
, nameLoc
, nameFixity
, nameNamespace
, nameToDefPName
, 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
@ -146,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 =
@ -227,12 +229,21 @@ nameLoc = nLoc
nameFixity :: Name -> Maybe Fixity
nameFixity = nFixity
-- | 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.origNameToDefPName og
LocalName _ txt -> PName.mkUnqual txt
-- | Primtiives must be in a top level module, at least for now.
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
@ -371,6 +382,7 @@ mkDeclared ns m sys ident fixity loc s = (name, s')
, ogModule = m
, ogName = ident
, ogSource = FromDefinition
, ogFromParam = Nothing
}
}
@ -410,7 +422,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

47
src/Cryptol/ModuleSystem/NamingEnv.hs
View File

@ -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.
@ -91,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. 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
txt = nameIdent x
in Map.insertWith (Map.unionWith (<>))
ns (Map.singleton (mkUnqual txt) (One x))
ns (Map.singleton (nameToDefPName x) (One x))
mp
@ -231,8 +213,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) ++
@ -248,6 +230,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.

34
src/Cryptol/ModuleSystem/NamingEnv/Types.hs Normal file
View File

@ -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))

47
src/Cryptol/ModuleSystem/Renamer.hs
View File

@ -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,12 +218,9 @@ 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
ImpTop r -> TopModule r
ImpNested r -> Nested (nameModPath r) (nameIdent r)
setCurMod (impNameModPath mname)
do resolved <- lookupResolved mname
shadowNames' CheckNone (rmodImports resolved)
@ -247,7 +242,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 +255,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
-- 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
-- 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 })
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 +805,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 +1399,6 @@ instance PP RenamedModule where
doc =
vcat [ "// --- Defines -----------------------------"
, pp (rmDefines rn)
, "// --- In scope ----------------------------"
, pp (rmInScope rn)
, "// -- Module -------------------------------"
, pp (rmModule rn)
, "// -----------------------------------------"

9
src/Cryptol/ModuleSystem/Renamer/Imports.hs
View File

@ -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

15
src/Cryptol/Parser/AST.hs
View File

@ -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,8 @@ 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
import Cryptol.Parser.Selector
@ -158,6 +160,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)
@ -304,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)
@ -839,6 +850,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 +1364,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

11
src/Cryptol/Parser/Name.hs
View File

@ -46,6 +46,17 @@ mkUnqual = UnQual
mkQual :: ModName -> Ident -> PName
mkQual = Qual
-- | 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
Nothing -> UnQual
Just sig -> Qual (identToModName sig)
getModName :: PName -> Maybe ModName
getModName (Qual ns _) = Just ns
getModName _ = Nothing

32
src/Cryptol/Parser/ParserUtils.hs
View File

@ -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)

7
src/Cryptol/TypeCheck/AST.hs
View File

@ -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.

9
src/Cryptol/TypeCheck/Infer.hs
View File

@ -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 ->

144
src/Cryptol/TypeCheck/Module.hs
View File

@ -1,20 +1,24 @@
{-# 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
import qualified Data.Map.Merge.Strict 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.Binds(newFunctorInst)
import Cryptol.ModuleSystem.Name(nameIdent)
import Cryptol.ModuleSystem.NamingEnv
(NamingEnv(..), modParamNamingEnv, shadowing, without)
import Cryptol.ModuleSystem.Interface
( IfaceG(..), IfaceDecls(..), IfaceNames(..), IfaceDecl(..)
, filterIfaceDecls
@ -36,16 +40,21 @@ 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 instMap0 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,paramTySyns,decls,paramInstMaps) =
unzip4 [ (su,ts,ds,im) | DefinedInst su ts ds im <- as2 ]
instMap <- addMissingTySyns mpath mf instMap0
let ?tSu = mergeDistinctSubst tySus
?vSu = inst
?vSu = instMap <> mconcat paramInstMaps
let m1 = moduleInstance mf
m2 = m1 { mName = m
, mDoc = Nothing
@ -53,6 +62,7 @@ doFunctorInst m f as inst doc =
, mParamFuns = mempty
, mParamConstraints = mempty
, mParams = mempty
, mTySyns = mconcat paramTySyns <> mTySyns m1
, mDecls = map NonRecursive (concat decls) ++
mDecls m1
}
@ -73,9 +83,24 @@ doFunctorInst m f as inst 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.
--
-- 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)
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))
@ -100,10 +125,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 -} ->
@ -159,7 +181,16 @@ checkArity r mf args =
checkArgs done ps more
data ArgInst = DefinedInst Subst [Decl] -- ^ Argument that defines the params
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
@ -179,8 +210,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
@ -197,7 +228,8 @@ checkArg (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 tyMap) (Map.toList (mpnTypes params))
let renSu = listParamSubst (concat tRens)
{- Note: the constraints from the signature are already added to the
@ -205,12 +237,13 @@ checkArg (r,expect,actual') =
doFunctorInst -}
vDecls <- concat <$>
mapM (checkParamValue r vMap)
[ s { mvpType = apSubst renSu (mvpType s) }
| s <- Map.elems (mpnFuns params) ]
(vDecls, vInstMaps) <-
mapAndUnzipM (checkParamValue mpath r vMap)
[ s { mvpType = apSubst renSu (mvpType s) }
| s <- Map.elems (mpnFuns params) ]
pure (DefinedInst renSu vDecls)
pure $ DefinedInst renSu (mconcat tSyns)
(concat vDecls) (mconcat tInstMaps <> mconcat vInstMaps)
params = mpParameters expect
@ -263,51 +296,72 @@ 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 -} ->
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),
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 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 []
pure ([], Map.empty, Map.empty)
Just (actualK,actualT) ->
do unless (expectK == actualK)
(recordErrorLoc (Just r)
(KindMismatch (Just (TVFromModParam name))
expectK actualK))
pure [(mtpParam mp, actualT)]
name' <- newFunctorInst mpath 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 new module we are creating -} ->
Range {- ^ Location for error reporting -} ->
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 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' <- newFunctorInst mpath 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')
@ -372,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)

10
src/Cryptol/TypeCheck/ModuleBacktickInstance.hs
View File

@ -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))

7
src/Cryptol/TypeCheck/ModuleInstance.hs
View File

@ -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)
@ -27,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 =
@ -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

16
src/Cryptol/TypeCheck/Monad.hs
View File

@ -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

16
src/Cryptol/Utils/Ident.hs
View File

@ -26,6 +26,7 @@ module Cryptol.Utils.Ident
, modNameChunks
, modNameChunksText
, packModName
, identToModName
, preludeName
, preludeReferenceName
, undefinedModName
@ -63,7 +64,7 @@ module Cryptol.Utils.Ident
-- * Original names
, OrigName(..)
, OrigSource(..)
, ogFromModParam
, ogIsModParam
-- * Identifiers for primitives
, PrimIdent(..)
@ -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 = "::"
@ -255,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

18
src/Cryptol/Utils/PP.hs
View File

@ -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 =

6
tests/issues/issue1455/F.cry Normal file
View File

@ -0,0 +1,6 @@
module F where
import interface I
a = x + 1
b = y + 1

7
tests/issues/issue1455/G.cry Normal file
View File

@ -0,0 +1,7 @@
module G where
import interface I
import F { interface I }
c = y + b

8
tests/issues/issue1455/I.cry Normal file
View File

@ -0,0 +1,8 @@
interface module I where
type n : #
type m = 2 * n
type constraint (fin n, n >= 1)
x : [n]
y : [m]

1
tests/issues/issue1455/Inst1.cry Normal file
View File

@ -0,0 +1 @@
module Inst1 = F { M }

1
tests/issues/issue1455/Inst2.cry Normal file
View File

@ -0,0 +1 @@
module Inst2 = F { _ }

1
tests/issues/issue1455/Inst3.cry Normal file
View File

@ -0,0 +1 @@
module Inst3 = G { M }

6
tests/issues/issue1455/M.cry Normal file
View File

@ -0,0 +1,6 @@
module M where
type n = 4
x = 3
y = 5

13
tests/issues/issue1455_1.icry Normal file
View File

@ -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

259
tests/issues/issue1455_1.icry.stdout Normal file
View File

@ -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 <interactive>
------------------
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]

9
tests/issues/issue1455_2.icry Normal file
View File

@ -0,0 +1,9 @@
:l issue1455/Inst2.cry
`n
`(m 3) : Integer
x
y
:t a
:t b
1 + 1 : Integer
:browse

257
tests/issues/issue1455_2.icry.stdout Normal file
View File

@ -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 <interactive>
------------------
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]

15
tests/issues/issue1455_3.icry Normal file
View File

@ -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

275
tests/issues/issue1455_3.icry.stdout Normal file
View File

@ -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 <interactive>
------------------
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]

275
tests/issues/issue1455_3.icry.stdout.mingw32 Normal file
View File

@ -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 <interactive>
------------------
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]

10
tests/issues/issue1561/F.cry Normal file
View File

@ -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

10
tests/issues/issue1561/G.cry Normal file
View File

@ -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

8
tests/issues/issue1561/I.cry Normal file
View File

@ -0,0 +1,8 @@
interface module I where
type n : #
type m = 2 * n
type constraint (fin n, n >= 1)
x : [n]
y : [m]

1
tests/issues/issue1561/Inst1.cry Normal file
View File

@ -0,0 +1 @@
module Inst1 = F { I = M, J = N }

1
tests/issues/issue1561/Inst2.cry Normal file
View File

@ -0,0 +1 @@
module Inst2 = G { J = M, K = N }

6
tests/issues/issue1561/M.cry Normal file
View File

@ -0,0 +1,6 @@
module M where
type n = 2
x = 3
y = 15

6
tests/issues/issue1561/N.cry Normal file
View File

@ -0,0 +1,6 @@
module N where
type n = 3
x = 5
y = 20

23
tests/issues/issue1561_1.icry Normal file
View File

@ -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

276
tests/issues/issue1561_1.icry.stdout Normal file
View File

@ -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 <interactive>
------------------
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]

27
tests/issues/issue1561_2.icry Normal file
View File

@ -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

288
tests/issues/issue1561_2.icry.stdout Normal file
View File

@ -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 <interactive>
------------------
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]

13
tests/issues/issue1562.cry Normal file
View File

@ -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 }

1
tests/issues/issue1562.icry Normal file
View File

@ -0,0 +1 @@
:l issue1562.cry

3
tests/issues/issue1562.icry.stdout Normal file
View File

@ -0,0 +1,3 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main