mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Implementation of nested modules.
* Limitations: Does not work in combination parameterized modules, as I am about to redo how that works. * General refeactorings: * Namespaces: - We have an explicit type for namespaces, see `Cryptol.Util.Ident` - Display environments should now be aware of the namespace of the name being displayed. * Renamer: - Factor out the renamer monad and error type into separate modules - All name resultion is done through a single function `resolveName` - The renamer now computes the dependencies between declarations, orders things in dependency order, and checks for bad recursion. * Typechecker: Redo checking of declarations (both top-level and local). Previously we used a sort of CPS to add things in scope. Now we use a state monad and add things to the state. We assume that the renamer has been run, which means that declarations are ordered in dependency order, and things have unique name, so we don't need to worry about scoping too much. * Change specific to nested modules: - We have a new namespace for module names - The interface file of a module contains the interfaces for nested modules - Most of the changes related to nested modules in the renamer are in `ModuleSystem.NamingEnv` and `ModuleSystem.Rename` - There is some trickiness when resolving module names when importing submodules (seed `processOpen` and `openLoop`) - There are some changes to the representation of modules in the typechecked syntax, in particular: - During type-checking we "flatten" nested module declarations into a single big declaration. Hopefully, this means that passes after the type checker don't need to worry about nested modules - There is a new field containing the interfaces of the nested modules, this is needed so that when we import the module we know we have the nested structure - Declarations in functor/parameterzied modules do not appear in the flattened list of declarations. Instead thouse modules are collected in a separate field, and the plan is that they would be used from there when we implmenet functor instantiation.
This commit is contained in:
parent
8a0a0094ae
commit
34b1d87df3
@ -37,7 +37,8 @@ import Cryptol.Eval.Concrete (Value)
|
||||
import Cryptol.Eval.Type (TValue(..), tValTy)
|
||||
import Cryptol.Eval.Value (GenValue(..), asWordVal, enumerateSeqMap)
|
||||
import Cryptol.Parser
|
||||
import Cryptol.Parser.AST (Bind(..), BindDef(..), Decl(..), Expr(..), Named(Named), TypeInst(NamedInst), Type(..), PName(..), Literal(..), NumInfo(..), Type)
|
||||
import Cryptol.Parser.AST (Bind(..), BindDef(..), Decl(..), Expr(..), Named(Named), TypeInst(NamedInst), Type(..), PName(..), Literal(..), NumInfo(..), Type,
|
||||
ExportType(..))
|
||||
import Cryptol.Parser.Position (Located(..), emptyRange)
|
||||
import Cryptol.Parser.Selector
|
||||
import Cryptol.Utils.Ident
|
||||
@ -319,7 +320,17 @@ getCryptolExpr (Let binds body) =
|
||||
mkBind (LetBinding x rhs) =
|
||||
DBind .
|
||||
(\bindBody ->
|
||||
Bind (fakeLoc (UnQual (mkIdent x))) [] bindBody Nothing False Nothing [] True Nothing) .
|
||||
Bind { bName = fakeLoc (UnQual (mkIdent x))
|
||||
, bParams = []
|
||||
, bDef = bindBody
|
||||
, bSignature = Nothing
|
||||
, bInfix = False
|
||||
, bFixity = Nothing
|
||||
, bPragmas = []
|
||||
, bMono = True
|
||||
, bDoc = Nothing
|
||||
, bExport = Public
|
||||
}) .
|
||||
fakeLoc .
|
||||
DExpr <$>
|
||||
getCryptolExpr rhs
|
||||
|
@ -17,9 +17,11 @@ import Cryptol.Parser.Name (PName(..))
|
||||
import Cryptol.ModuleSystem.Env (ModContext(..), ModuleEnv(..), DynamicEnv(..), focusedEnv)
|
||||
import Cryptol.ModuleSystem.Interface (IfaceDecl(..), IfaceDecls(..))
|
||||
import Cryptol.ModuleSystem.Name (Name)
|
||||
import Cryptol.ModuleSystem.NamingEnv (NamingEnv(..), lookupValNames, shadowing)
|
||||
import Cryptol.ModuleSystem.NamingEnv
|
||||
(NamingEnv, namespaceMap, lookupValNames, shadowing)
|
||||
import Cryptol.TypeCheck.Type (Schema(..))
|
||||
import Cryptol.Utils.PP (pp)
|
||||
import Cryptol.Utils.Ident(Namespace(..))
|
||||
|
||||
import CryptolServer
|
||||
import CryptolServer.Data.Type
|
||||
@ -41,7 +43,7 @@ visibleNames _ =
|
||||
do me <- getModuleEnv
|
||||
let DEnv { deNames = dyNames } = meDynEnv me
|
||||
let ModContext { mctxDecls = fDecls, mctxNames = fNames} = focusedEnv me
|
||||
let inScope = Map.keys (neExprs $ dyNames `shadowing` fNames)
|
||||
let inScope = Map.keys (namespaceMap NSValue $ dyNames `shadowing` fNames)
|
||||
return $ concatMap (getInfo fNames (ifDecls fDecls)) inScope
|
||||
|
||||
getInfo :: NamingEnv -> Map Name IfaceDecl -> PName -> [NameInfo]
|
||||
|
@ -111,9 +111,11 @@ library
|
||||
Cryptol.ModuleSystem.Monad,
|
||||
Cryptol.ModuleSystem.Name,
|
||||
Cryptol.ModuleSystem.NamingEnv,
|
||||
Cryptol.ModuleSystem.Renamer,
|
||||
Cryptol.ModuleSystem.Exports,
|
||||
Cryptol.ModuleSystem.InstantiateModule,
|
||||
Cryptol.ModuleSystem.Renamer,
|
||||
Cryptol.ModuleSystem.Renamer.Monad,
|
||||
Cryptol.ModuleSystem.Renamer.Error,
|
||||
|
||||
Cryptol.TypeCheck,
|
||||
Cryptol.TypeCheck.Type,
|
||||
@ -126,12 +128,12 @@ library
|
||||
Cryptol.TypeCheck.Infer,
|
||||
Cryptol.TypeCheck.CheckModuleInstance,
|
||||
Cryptol.TypeCheck.InferTypes,
|
||||
Cryptol.TypeCheck.Interface,
|
||||
Cryptol.TypeCheck.Error,
|
||||
Cryptol.TypeCheck.Kind,
|
||||
Cryptol.TypeCheck.Subst,
|
||||
Cryptol.TypeCheck.Instantiate,
|
||||
Cryptol.TypeCheck.Unify,
|
||||
Cryptol.TypeCheck.Depends,
|
||||
Cryptol.TypeCheck.PP,
|
||||
Cryptol.TypeCheck.Solve,
|
||||
Cryptol.TypeCheck.Default,
|
||||
|
@ -29,7 +29,7 @@ module Cryptol.ModuleSystem (
|
||||
, renameType
|
||||
|
||||
-- * Interfaces
|
||||
, Iface(..), IfaceParams(..), IfaceDecls(..), genIface
|
||||
, Iface, IfaceG(..), IfaceParams(..), IfaceDecls(..), T.genIface
|
||||
, IfaceTySyn, IfaceDecl(..)
|
||||
) where
|
||||
|
||||
@ -44,6 +44,7 @@ import qualified Cryptol.Parser.AST as P
|
||||
import Cryptol.Parser.Name (PName)
|
||||
import Cryptol.Parser.NoPat (RemovePatterns)
|
||||
import qualified Cryptol.TypeCheck.AST as T
|
||||
import qualified Cryptol.TypeCheck.Interface as T
|
||||
import qualified Cryptol.Utils.Ident as M
|
||||
|
||||
-- Public Interface ------------------------------------------------------------
|
||||
@ -105,10 +106,14 @@ evalDecls dgs env = runModuleM env (interactive (Base.evalDecls dgs))
|
||||
noPat :: RemovePatterns a => a -> ModuleCmd a
|
||||
noPat a env = runModuleM env (interactive (Base.noPat a))
|
||||
|
||||
-- | Rename a *use* of a value name. The distinction between uses and
|
||||
-- binding is used to keep track of dependencies.
|
||||
renameVar :: R.NamingEnv -> PName -> ModuleCmd Name
|
||||
renameVar names n env = runModuleM env $ interactive $
|
||||
Base.rename M.interactiveName names (R.renameVar n)
|
||||
Base.rename M.interactiveName names (R.renameVar R.NameUse n)
|
||||
|
||||
-- | Rename a *use* of a type name. The distinction between uses and
|
||||
-- binding is used to keep track of dependencies.
|
||||
renameType :: R.NamingEnv -> PName -> ModuleCmd Name
|
||||
renameType names n env = runModuleM env $ interactive $
|
||||
Base.rename M.interactiveName names (R.renameType n)
|
||||
Base.rename M.interactiveName names (R.renameType R.NameUse n)
|
||||
|
@ -12,14 +12,37 @@
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE ImplicitParams #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
module Cryptol.ModuleSystem.Base where
|
||||
|
||||
import qualified Control.Exception as X
|
||||
import Control.Monad (unless,when)
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Monoid ((<>))
|
||||
import Data.Text.Encoding (decodeUtf8')
|
||||
import System.Directory (doesFileExist, canonicalizePath)
|
||||
import System.FilePath ( addExtension
|
||||
, isAbsolute
|
||||
, joinPath
|
||||
, (</>)
|
||||
, normalise
|
||||
, takeDirectory
|
||||
, takeFileName
|
||||
)
|
||||
import qualified System.IO.Error as IOE
|
||||
import qualified Data.Map as Map
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat hiding ( (<>) )
|
||||
|
||||
|
||||
|
||||
import Cryptol.ModuleSystem.Env (DynamicEnv(..))
|
||||
import Cryptol.ModuleSystem.Fingerprint
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
import Cryptol.ModuleSystem.Monad
|
||||
import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap)
|
||||
import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap,ModPath(..))
|
||||
import Cryptol.ModuleSystem.Env (lookupModule
|
||||
, LoadedModule(..)
|
||||
, meCoreLint, CoreLint(..)
|
||||
@ -53,33 +76,21 @@ import Cryptol.Prelude ( preludeContents, floatContents, arrayContents
|
||||
, suiteBContents, primeECContents, preludeReferenceContents )
|
||||
import Cryptol.Transform.MonoValues (rewModule)
|
||||
|
||||
import qualified Control.Exception as X
|
||||
import Control.Monad (unless,when)
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Monoid ((<>))
|
||||
import Data.Text.Encoding (decodeUtf8')
|
||||
import System.Directory (doesFileExist, canonicalizePath)
|
||||
import System.FilePath ( addExtension
|
||||
, isAbsolute
|
||||
, joinPath
|
||||
, (</>)
|
||||
, normalise
|
||||
, takeDirectory
|
||||
, takeFileName
|
||||
)
|
||||
import qualified System.IO.Error as IOE
|
||||
import qualified Data.Map as Map
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat hiding ( (<>) )
|
||||
|
||||
|
||||
-- Renaming --------------------------------------------------------------------
|
||||
|
||||
rename :: ModName -> R.NamingEnv -> R.RenameM a -> ModuleM a
|
||||
rename modName env m = do
|
||||
ifaces <- getIfaces
|
||||
(res,ws) <- liftSupply $ \ supply ->
|
||||
case R.runRenamer supply modName env m of
|
||||
let info = R.RenamerInfo
|
||||
{ renSupply = supply
|
||||
, renContext = TopModule modName
|
||||
, renEnv = env
|
||||
, renIfaces = ifaces
|
||||
}
|
||||
in
|
||||
case R.runRenamer info m of
|
||||
(Right (a,supply'),ws) -> ((Right a,ws),supply')
|
||||
(Left errs,ws) -> ((Left errs,ws),supply)
|
||||
|
||||
@ -89,12 +100,9 @@ rename modName env m = do
|
||||
Left errs -> renamerErrors errs
|
||||
|
||||
-- | Rename a module in the context of its imported modules.
|
||||
renameModule :: P.Module PName
|
||||
-> ModuleM (IfaceDecls,R.NamingEnv,P.Module Name)
|
||||
renameModule m = do
|
||||
(decls,menv) <- importIfaces (map thing (P.mImports m))
|
||||
(declsEnv,rm) <- rename (thing (mName m)) menv (R.renameModule m)
|
||||
return (decls,declsEnv,rm)
|
||||
renameModule ::
|
||||
P.Module PName -> ModuleM (IfaceDecls,R.NamingEnv,P.Module Name)
|
||||
renameModule m = rename (thing (mName m)) mempty (R.renameModule m)
|
||||
|
||||
|
||||
-- NoPat -----------------------------------------------------------------------
|
||||
@ -231,17 +239,6 @@ doLoadModule quiet isrc path fp pm0 =
|
||||
fullyQualified :: P.Import -> P.Import
|
||||
fullyQualified i = i { iAs = Just (iModule i) }
|
||||
|
||||
-- | Find the interface referenced by an import, and generate the naming
|
||||
-- environment that it describes.
|
||||
importIface :: P.Import -> ModuleM (IfaceDecls,R.NamingEnv)
|
||||
importIface imp =
|
||||
do Iface { .. } <- getIface (T.iModule imp)
|
||||
return (ifPublic, R.interpImport imp ifPublic)
|
||||
|
||||
-- | Load a series of interfaces, merging their public interfaces.
|
||||
importIfaces :: [P.Import] -> ModuleM (IfaceDecls,R.NamingEnv)
|
||||
importIfaces is = mconcat `fmap` mapM importIface is
|
||||
|
||||
moduleFile :: ModName -> String -> FilePath
|
||||
moduleFile n = addExtension (joinPath (modNameChunks n))
|
||||
|
||||
@ -299,13 +296,13 @@ addPrelude :: P.Module PName -> P.Module PName
|
||||
addPrelude m
|
||||
| preludeName == P.thing (P.mName m) = m
|
||||
| preludeName `elem` importedMods = m
|
||||
| otherwise = m { mImports = importPrelude : mImports m }
|
||||
| otherwise = m { mDecls = importPrelude : mDecls m }
|
||||
where
|
||||
importedMods = map (P.iModule . P.thing) (P.mImports m)
|
||||
importPrelude = P.Located
|
||||
importPrelude = P.DImport P.Located
|
||||
{ P.srcRange = emptyRange
|
||||
, P.thing = P.Import
|
||||
{ iModule = preludeName
|
||||
{ iModule = P.ImpTop preludeName
|
||||
, iAs = Nothing
|
||||
, iSpec = Nothing
|
||||
}
|
||||
@ -360,11 +357,8 @@ checkDecls ds = do
|
||||
decls = mctxDecls fe
|
||||
names = mctxNames fe
|
||||
|
||||
-- introduce names for the declarations before renaming them
|
||||
declsEnv <- liftSupply (R.namingEnv' (map (R.InModule interactiveName) ds))
|
||||
rds <- rename interactiveName (declsEnv `R.shadowing` names)
|
||||
(traverse R.rename ds)
|
||||
|
||||
(declsEnv,rds) <- rename interactiveName names
|
||||
$ R.renameTopDecls interactiveName ds
|
||||
prims <- getPrimMap
|
||||
let act = TCAction { tcAction = T.tcDecls, tcLinter = declsLinter
|
||||
, tcPrims = prims }
|
||||
|
@ -24,6 +24,7 @@ import Cryptol.ModuleSystem.Name (Name,Supply,emptySupply)
|
||||
import qualified Cryptol.ModuleSystem.NamingEnv as R
|
||||
import Cryptol.Parser.AST
|
||||
import qualified Cryptol.TypeCheck as T
|
||||
import qualified Cryptol.TypeCheck.Interface as T
|
||||
import qualified Cryptol.TypeCheck.AST as T
|
||||
import Cryptol.Utils.PP (PP(..),text,parens,NameDisp)
|
||||
|
||||
@ -197,6 +198,9 @@ data ModContext = ModContext
|
||||
, mctxDecls :: IfaceDecls
|
||||
, mctxNames :: R.NamingEnv
|
||||
, mctxNameDisp :: NameDisp
|
||||
|
||||
-- XXX: use namespace
|
||||
, mctxModProvenace :: Map Name DeclProvenance
|
||||
, mctxTypeProvenace :: Map Name DeclProvenance
|
||||
, mctxValueProvenance :: Map Name DeclProvenance
|
||||
}
|
||||
@ -214,6 +218,9 @@ data DeclProvenance =
|
||||
-- | Given the state of the environment, compute information about what's
|
||||
-- in scope on the REPL. This includes what's in the focused module, plus any
|
||||
-- additional definitions from the REPL (e.g., let bound names, and @it@).
|
||||
-- XXX: nested modules.
|
||||
-- XXX: it seems that this does a bunch of work that should be happening
|
||||
-- somewhere else too...
|
||||
focusedEnv :: ModuleEnv -> ModContext
|
||||
focusedEnv me =
|
||||
ModContext
|
||||
@ -221,11 +228,16 @@ focusedEnv me =
|
||||
, mctxDecls = mconcat (dynDecls : localDecls : importedDecls)
|
||||
, mctxNames = namingEnv
|
||||
, mctxNameDisp = R.toNameDisp namingEnv
|
||||
, mctxTypeProvenace = fst provenance
|
||||
, mctxValueProvenance = snd provenance
|
||||
, mctxModProvenace = fst3 provenance
|
||||
, mctxTypeProvenace = snd3 provenance
|
||||
, mctxValueProvenance = trd3 provenance
|
||||
}
|
||||
|
||||
where
|
||||
fst3 (x,_,_) = x
|
||||
snd3 (_,x,_) = x
|
||||
trd3 (_,_,x) = x
|
||||
|
||||
(importedNames,importedDecls,importedProvs) = unzip3 (map loadImport imports)
|
||||
localDecls = publicDecls `mappend` privateDecls
|
||||
localNames = R.unqualifiedEnv localDecls `mappend`
|
||||
@ -258,7 +270,7 @@ focusedEnv me =
|
||||
case lookupModule (iModule imp) me of
|
||||
Just lm ->
|
||||
let decls = ifPublic (lmInterface lm)
|
||||
in ( R.interpImport imp decls
|
||||
in ( R.interpImportIface imp decls
|
||||
, decls
|
||||
, declsProv (NameIsImportedFrom (iModule imp)) decls
|
||||
)
|
||||
@ -267,14 +279,15 @@ focusedEnv me =
|
||||
|
||||
|
||||
-- earlier ones shadow
|
||||
shadowProvs ps = let (tss,vss) = unzip ps
|
||||
in (Map.unions tss, Map.unions vss)
|
||||
shadowProvs ps = let (mss,tss,vss) = unzip3 ps
|
||||
in (Map.unions mss, Map.unions tss, Map.unions vss)
|
||||
|
||||
paramProv IfaceParams { .. } = (doMap ifParamTypes, doMap ifParamFuns)
|
||||
paramProv IfaceParams { .. } = (mempty, doMap ifParamTypes, doMap ifParamFuns)
|
||||
where doMap mp = const NameIsParameter <$> mp
|
||||
|
||||
declsProv prov IfaceDecls { .. } =
|
||||
( Map.unions [ doMap ifTySyns, doMap ifNewtypes, doMap ifAbstractTypes ]
|
||||
( doMap ifModules
|
||||
, Map.unions [ doMap ifTySyns, doMap ifNewtypes, doMap ifAbstractTypes ]
|
||||
, doMap ifDecls
|
||||
)
|
||||
where doMap mp = const prov <$> mp
|
||||
@ -390,7 +403,7 @@ addLoadedModule path ident fp tm lm
|
||||
{ lmName = T.mName tm
|
||||
, lmFilePath = path
|
||||
, lmModuleId = ident
|
||||
, lmInterface = genIface tm
|
||||
, lmInterface = T.genIface tm
|
||||
, lmModule = tm
|
||||
, lmFingerprint = fp
|
||||
}
|
||||
@ -444,7 +457,8 @@ deIfaceDecls DEnv { deDecls = dgs } =
|
||||
, ifNewtypes = Map.empty
|
||||
, ifAbstractTypes = Map.empty
|
||||
, ifDecls = Map.singleton (ifDeclName ifd) ifd
|
||||
, ifModules = Map.empty
|
||||
}
|
||||
| decl <- concatMap T.groupDecls dgs
|
||||
, let ifd = mkIfaceDecl decl
|
||||
, let ifd = T.mkIfaceDecl decl
|
||||
]
|
||||
|
@ -3,14 +3,17 @@ module Cryptol.ModuleSystem.Exports where
|
||||
|
||||
import Data.Set(Set)
|
||||
import qualified Data.Set as Set
|
||||
import Data.Map(Map)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Foldable(fold)
|
||||
import Control.DeepSeq(NFData)
|
||||
import GHC.Generics (Generic)
|
||||
|
||||
import Cryptol.Parser.AST
|
||||
import Cryptol.Parser.Names
|
||||
import Cryptol.Parser.Names(namesD,tnamesD,tnamesNT)
|
||||
import Cryptol.ModuleSystem.Name
|
||||
|
||||
modExports :: Ord name => Module name -> ExportSpec name
|
||||
modExports :: Ord name => ModuleG manme name -> ExportSpec name
|
||||
modExports m = fold (concat [ exportedNames d | d <- mDecls m ])
|
||||
where
|
||||
names by td = [ td { tlValue = thing n } | n <- fst (by (tlValue td)) ]
|
||||
@ -20,46 +23,61 @@ modExports m = fold (concat [ exportedNames d | d <- mDecls m ])
|
||||
exportedNames (DPrimType t) = [ exportType (thing . primTName <$> t) ]
|
||||
exportedNames (TDNewtype nt) = map exportType (names tnamesNT nt)
|
||||
exportedNames (Include {}) = []
|
||||
exportedNames (DImport {}) = []
|
||||
exportedNames (DParameterFun {}) = []
|
||||
exportedNames (DParameterType {}) = []
|
||||
exportedNames (DParameterConstraint {}) = []
|
||||
exportedNames (DModule nested) =
|
||||
case tlValue nested of
|
||||
NestedModule x ->
|
||||
[exportName NSModule nested { tlValue = thing (mName x) }]
|
||||
|
||||
|
||||
|
||||
data ExportSpec name = ExportSpec { eTypes :: Set name
|
||||
, eBinds :: Set name
|
||||
} deriving (Show, Generic)
|
||||
newtype ExportSpec name = ExportSpec (Map Namespace (Set name))
|
||||
deriving (Show, Generic)
|
||||
|
||||
instance NFData name => NFData (ExportSpec name)
|
||||
|
||||
instance Ord name => Semigroup (ExportSpec name) where
|
||||
l <> r = ExportSpec { eTypes = eTypes l <> eTypes r
|
||||
, eBinds = eBinds l <> eBinds r
|
||||
}
|
||||
ExportSpec l <> ExportSpec r = ExportSpec (Map.unionWith Set.union l r)
|
||||
|
||||
instance Ord name => Monoid (ExportSpec name) where
|
||||
mempty = ExportSpec { eTypes = mempty, eBinds = mempty }
|
||||
mappend = (<>)
|
||||
mempty = ExportSpec Map.empty
|
||||
|
||||
exportName :: Ord name => Namespace -> TopLevel name -> ExportSpec name
|
||||
exportName ns n
|
||||
| tlExport n == Public = ExportSpec
|
||||
$ Map.singleton ns
|
||||
$ Set.singleton (tlValue n)
|
||||
| otherwise = mempty
|
||||
|
||||
exported :: Namespace -> ExportSpec name -> Set name
|
||||
exported ns (ExportSpec mp) = Map.findWithDefault Set.empty ns mp
|
||||
|
||||
-- | Add a binding name to the export list, if it should be exported.
|
||||
exportBind :: Ord name => TopLevel name -> ExportSpec name
|
||||
exportBind n
|
||||
| tlExport n == Public = mempty { eBinds = Set.singleton (tlValue n) }
|
||||
| otherwise = mempty
|
||||
exportBind = exportName NSValue
|
||||
|
||||
-- | Add a type synonym name to the export list, if it should be exported.
|
||||
exportType :: Ord name => TopLevel name -> ExportSpec name
|
||||
exportType n
|
||||
| tlExport n == Public = mempty { eTypes = Set.singleton (tlValue n) }
|
||||
| otherwise = mempty
|
||||
exportType = exportName NSType
|
||||
|
||||
|
||||
|
||||
isExported :: Ord name => Namespace -> name -> ExportSpec name -> Bool
|
||||
isExported ns x (ExportSpec s) =
|
||||
case Map.lookup ns s of
|
||||
Nothing -> False
|
||||
Just mp -> Set.member x mp
|
||||
|
||||
-- | Check to see if a binding is exported.
|
||||
isExportedBind :: Ord name => name -> ExportSpec name -> Bool
|
||||
isExportedBind n = Set.member n . eBinds
|
||||
isExportedBind = isExported NSValue
|
||||
|
||||
-- | Check to see if a type synonym is exported.
|
||||
isExportedType :: Ord name => name -> ExportSpec name -> Bool
|
||||
isExportedType n = Set.member n . eTypes
|
||||
isExportedType = isExported NSType
|
||||
|
||||
|
||||
|
||||
|
@ -1,4 +1,5 @@
|
||||
{-# Language FlexibleInstances, PatternGuards #-}
|
||||
{-# Language BlockArguments #-}
|
||||
-- | Assumes that local names do not shadow top level names.
|
||||
module Cryptol.ModuleSystem.InstantiateModule
|
||||
( instantiateModule
|
||||
@ -10,12 +11,13 @@ import Data.Map (Map)
|
||||
import qualified Data.Map as Map
|
||||
import MonadLib(ReaderT,runReaderT,ask)
|
||||
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.Ident(ModName,modParamIdent)
|
||||
import Cryptol.Parser.Position(Located(..))
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Subst(listParamSubst, apSubst)
|
||||
import Cryptol.TypeCheck.SimpType(tRebuild)
|
||||
import Cryptol.Utils.Ident(ModName,modParamIdent)
|
||||
|
||||
{-
|
||||
XXX: Should we simplify constraints in the instantiated modules?
|
||||
@ -35,8 +37,12 @@ instantiateModule :: FreshM m =>
|
||||
Map Name Expr {- ^ Value parameters -} ->
|
||||
m ([Located Prop], Module)
|
||||
-- ^ Instantiated constraints, fresh module, new supply
|
||||
instantiateModule func newName tpMap vpMap =
|
||||
runReaderT newName $
|
||||
instantiateModule func newName tpMap vpMap
|
||||
| not (null (mSubModules func)) =
|
||||
panic "instantiateModule"
|
||||
[ "XXX: we don't support functors with nested moduels yet." ]
|
||||
| otherwise =
|
||||
runReaderT (TopModule newName) $
|
||||
do let oldVpNames = Map.keys vpMap
|
||||
newVpNames <- mapM freshParamName (Map.keys vpMap)
|
||||
let vpNames = Map.fromList (zip oldVpNames newVpNames)
|
||||
@ -72,6 +78,9 @@ instantiateModule func newName tpMap vpMap =
|
||||
, mParamConstraints = []
|
||||
, mParamFuns = Map.empty
|
||||
, mDecls = paramDecls ++ renamedDecls
|
||||
|
||||
, mSubModules = mempty
|
||||
, mFunctors = mempty
|
||||
} )
|
||||
|
||||
where
|
||||
@ -110,7 +119,7 @@ instance Defines DeclGroup where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
type InstM = ReaderT ModName
|
||||
type InstM = ReaderT ModPath
|
||||
|
||||
-- | Generate a new instance of a declared name.
|
||||
freshenName :: FreshM m => Name -> InstM m Name
|
||||
@ -119,13 +128,15 @@ freshenName x =
|
||||
let sys = case nameInfo x of
|
||||
Declared _ s -> s
|
||||
_ -> UserName
|
||||
liftSupply (mkDeclared m sys (nameIdent x) (nameFixity x) (nameLoc x))
|
||||
liftSupply (mkDeclared (nameNamespace x)
|
||||
m sys (nameIdent x) (nameFixity x) (nameLoc x))
|
||||
|
||||
freshParamName :: FreshM m => Name -> InstM m Name
|
||||
freshParamName x =
|
||||
do m <- ask
|
||||
let newName = modParamIdent (nameIdent x)
|
||||
liftSupply (mkDeclared m UserName newName (nameFixity x) (nameLoc x))
|
||||
liftSupply (mkDeclared (nameNamespace x)
|
||||
m UserName newName (nameFixity x) (nameLoc x))
|
||||
|
||||
|
||||
|
||||
@ -263,11 +274,14 @@ instance Inst UserTC where
|
||||
where y = Map.findWithDefault x x (tyNameMap env)
|
||||
|
||||
instance Inst (ExportSpec Name) where
|
||||
inst env es = ExportSpec { eTypes = Set.map instT (eTypes es)
|
||||
, eBinds = Set.map instV (eBinds es)
|
||||
}
|
||||
where instT x = Map.findWithDefault x x (tyNameMap env)
|
||||
instV x = Map.findWithDefault x x (funNameMap env)
|
||||
inst env (ExportSpec spec) = ExportSpec (Map.mapWithKey doNS spec)
|
||||
where
|
||||
doNS ns =
|
||||
case ns of
|
||||
NSType -> Set.map \x -> Map.findWithDefault x x (tyNameMap env)
|
||||
NSValue -> Set.map \x -> Map.findWithDefault x x (funNameMap env)
|
||||
NSModule -> id
|
||||
|
||||
|
||||
instance Inst TySyn where
|
||||
inst env ts = TySyn { tsName = instTyName env x
|
||||
|
@ -12,24 +12,19 @@
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
module Cryptol.ModuleSystem.Interface (
|
||||
Iface(..)
|
||||
Iface
|
||||
, IfaceG(..)
|
||||
, IfaceDecls(..)
|
||||
, IfaceTySyn, ifTySynName
|
||||
, IfaceNewtype
|
||||
, IfaceDecl(..), mkIfaceDecl
|
||||
, IfaceDecl(..)
|
||||
, IfaceParams(..)
|
||||
|
||||
, genIface
|
||||
, emptyIface
|
||||
, ifacePrimMap
|
||||
, noIfaceParams
|
||||
) where
|
||||
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.Utils.Ident (ModName)
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Parser.Position(Located)
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import Data.Semigroup
|
||||
import Data.Text (Text)
|
||||
@ -40,15 +35,33 @@ import Control.DeepSeq
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.Utils.Ident (ModName)
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.Fixity(Fixity)
|
||||
import Cryptol.Parser.AST(Pragma)
|
||||
import Cryptol.Parser.Position(Located)
|
||||
import Cryptol.TypeCheck.Type
|
||||
|
||||
|
||||
-- | The resulting interface generated by a module that has been typechecked.
|
||||
data Iface = Iface
|
||||
{ ifModName :: !ModName -- ^ Module name
|
||||
data IfaceG mname = Iface
|
||||
{ ifModName :: !mname -- ^ Module name
|
||||
, ifPublic :: IfaceDecls -- ^ Exported definitions
|
||||
, ifPrivate :: IfaceDecls -- ^ Private defintiions
|
||||
, ifParams :: IfaceParams -- ^ Uninterpreted constants (aka module params)
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
type Iface = IfaceG ModName
|
||||
|
||||
emptyIface :: mname -> IfaceG mname
|
||||
emptyIface nm = Iface
|
||||
{ ifModName = nm
|
||||
, ifPublic = mempty
|
||||
, ifPrivate = mempty
|
||||
, ifParams = noIfaceParams
|
||||
}
|
||||
|
||||
data IfaceParams = IfaceParams
|
||||
{ ifParamTypes :: Map.Map Name ModTParam
|
||||
, ifParamConstraints :: [Located Prop] -- ^ Constraints on param. types
|
||||
@ -67,6 +80,7 @@ data IfaceDecls = IfaceDecls
|
||||
, ifNewtypes :: Map.Map Name IfaceNewtype
|
||||
, ifAbstractTypes :: Map.Map Name IfaceAbstractType
|
||||
, ifDecls :: Map.Map Name IfaceDecl
|
||||
, ifModules :: !(Map.Map Name (IfaceG Name))
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
instance Semigroup IfaceDecls where
|
||||
@ -75,16 +89,18 @@ instance Semigroup IfaceDecls where
|
||||
, ifNewtypes = Map.union (ifNewtypes l) (ifNewtypes r)
|
||||
, ifAbstractTypes = Map.union (ifAbstractTypes l) (ifAbstractTypes r)
|
||||
, ifDecls = Map.union (ifDecls l) (ifDecls r)
|
||||
, ifModules = Map.union (ifModules l) (ifModules r)
|
||||
}
|
||||
|
||||
instance Monoid IfaceDecls where
|
||||
mempty = IfaceDecls Map.empty Map.empty Map.empty Map.empty
|
||||
mempty = IfaceDecls Map.empty Map.empty Map.empty Map.empty Map.empty
|
||||
mappend l r = l <> r
|
||||
mconcat ds = IfaceDecls
|
||||
{ ifTySyns = Map.unions (map ifTySyns ds)
|
||||
, ifNewtypes = Map.unions (map ifNewtypes ds)
|
||||
, ifAbstractTypes = Map.unions (map ifAbstractTypes ds)
|
||||
, ifDecls = Map.unions (map ifDecls ds)
|
||||
, ifModules = Map.unions (map ifModules ds)
|
||||
}
|
||||
|
||||
type IfaceTySyn = TySyn
|
||||
@ -104,61 +120,6 @@ data IfaceDecl = IfaceDecl
|
||||
, ifDeclDoc :: Maybe Text -- ^ Documentation
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
mkIfaceDecl :: Decl -> IfaceDecl
|
||||
mkIfaceDecl d = IfaceDecl
|
||||
{ ifDeclName = dName d
|
||||
, ifDeclSig = dSignature d
|
||||
, ifDeclPragmas = dPragmas d
|
||||
, ifDeclInfix = dInfix d
|
||||
, ifDeclFixity = dFixity d
|
||||
, ifDeclDoc = dDoc d
|
||||
}
|
||||
|
||||
-- | Generate an Iface from a typechecked module.
|
||||
genIface :: Module -> Iface
|
||||
genIface m = Iface
|
||||
{ ifModName = mName m
|
||||
|
||||
, ifPublic = IfaceDecls
|
||||
{ ifTySyns = tsPub
|
||||
, ifNewtypes = ntPub
|
||||
, ifAbstractTypes = atPub
|
||||
, ifDecls = dPub
|
||||
}
|
||||
|
||||
, ifPrivate = IfaceDecls
|
||||
{ ifTySyns = tsPriv
|
||||
, ifNewtypes = ntPriv
|
||||
, ifAbstractTypes = atPriv
|
||||
, ifDecls = dPriv
|
||||
}
|
||||
|
||||
, ifParams = IfaceParams
|
||||
{ ifParamTypes = mParamTypes m
|
||||
, ifParamConstraints = mParamConstraints m
|
||||
, ifParamFuns = mParamFuns m
|
||||
}
|
||||
}
|
||||
where
|
||||
|
||||
(tsPub,tsPriv) =
|
||||
Map.partitionWithKey (\ qn _ -> qn `isExportedType` mExports m )
|
||||
(mTySyns m)
|
||||
(ntPub,ntPriv) =
|
||||
Map.partitionWithKey (\ qn _ -> qn `isExportedType` mExports m )
|
||||
(mNewtypes m)
|
||||
|
||||
(atPub,atPriv) =
|
||||
Map.partitionWithKey (\qn _ -> qn `isExportedType` mExports m)
|
||||
(mPrimTypes m)
|
||||
|
||||
(dPub,dPriv) =
|
||||
Map.partitionWithKey (\ qn _ -> qn `isExportedBind` mExports m)
|
||||
$ Map.fromList [ (qn,mkIfaceDecl d) | dg <- mDecls m
|
||||
, d <- groupDecls dg
|
||||
, let qn = dName d
|
||||
]
|
||||
|
||||
|
||||
-- | Produce a PrimMap from an interface.
|
||||
--
|
||||
|
@ -463,11 +463,15 @@ getImportSource = ModuleT $ do
|
||||
_ -> return (FromModule noModuleName)
|
||||
|
||||
getIface :: P.ModName -> ModuleM Iface
|
||||
getIface mn =
|
||||
do env <- ModuleT get
|
||||
case lookupModule mn env of
|
||||
Just lm -> return (lmInterface lm)
|
||||
Nothing -> panic "ModuleSystem" ["Interface not available", show (pp mn)]
|
||||
getIface mn = ($ mn) <$> getIfaces
|
||||
|
||||
getIfaces :: ModuleM (P.ModName -> Iface)
|
||||
getIfaces = doLookup <$> ModuleT get
|
||||
where
|
||||
doLookup env mn =
|
||||
case lookupModule mn env of
|
||||
Just lm -> lmInterface lm
|
||||
Nothing -> panic "ModuleSystem" ["Interface not available", show (pp mn)]
|
||||
|
||||
getLoaded :: P.ModName -> ModuleM T.Module
|
||||
getLoaded mn = ModuleT $
|
||||
|
@ -14,6 +14,7 @@
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
-- for the instances of RunM and BaseM
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
@ -26,10 +27,13 @@ module Cryptol.ModuleSystem.Name (
|
||||
, nameInfo
|
||||
, nameLoc
|
||||
, nameFixity
|
||||
, nameNamespace
|
||||
, asPrim
|
||||
, cmpNameLexical
|
||||
, cmpNameDisplay
|
||||
, asOrigName
|
||||
, ppLocName
|
||||
, Namespace(..)
|
||||
, ModPath(..)
|
||||
, cmpNameDisplay
|
||||
|
||||
-- ** Creation
|
||||
, mkDeclared
|
||||
@ -49,6 +53,18 @@ module Cryptol.ModuleSystem.Name (
|
||||
, lookupPrimType
|
||||
) where
|
||||
|
||||
import Control.DeepSeq
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Monoid as M
|
||||
import GHC.Generics (Generic)
|
||||
import MonadLib
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
import qualified Data.Text as Text
|
||||
import Data.Char(isAlpha,toUpper)
|
||||
|
||||
|
||||
|
||||
import Cryptol.Parser.Position (Range,Located(..),emptyRange)
|
||||
import Cryptol.Utils.Fixity
|
||||
import Cryptol.Utils.Ident
|
||||
@ -56,26 +72,16 @@ import Cryptol.Utils.Panic
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
|
||||
import Control.DeepSeq
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Monoid as M
|
||||
import Data.Ord (comparing)
|
||||
import qualified Data.Text as Text
|
||||
import Data.Char(isAlpha,toUpper)
|
||||
import GHC.Generics (Generic)
|
||||
import MonadLib
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
|
||||
-- Names -----------------------------------------------------------------------
|
||||
-- | Information about the binding site of the name.
|
||||
data NameInfo = Declared !ModName !NameSource
|
||||
data NameInfo = Declared !ModPath !NameSource
|
||||
-- ^ This name refers to a declaration from this module
|
||||
| Parameter
|
||||
-- ^ This name is a parameter (function or type)
|
||||
deriving (Eq, Show, Generic, NFData)
|
||||
|
||||
|
||||
data Name = Name { nUnique :: {-# UNPACK #-} !Int
|
||||
-- ^ INVARIANT: this field uniquely identifies a name for one
|
||||
-- session with the Cryptol library. Names are unique to
|
||||
@ -84,6 +90,8 @@ data Name = Name { nUnique :: {-# UNPACK #-} !Int
|
||||
, nInfo :: !NameInfo
|
||||
-- ^ Information about the origin of this name.
|
||||
|
||||
, nNamespace :: !Namespace
|
||||
|
||||
, nIdent :: !Ident
|
||||
-- ^ The name of the identifier
|
||||
|
||||
@ -100,6 +108,7 @@ data Name = Name { nUnique :: {-# UNPACK #-} !Int
|
||||
data NameSource = SystemName | UserName
|
||||
deriving (Generic, NFData, Show, Eq)
|
||||
|
||||
|
||||
instance Eq Name where
|
||||
a == b = compare a b == EQ
|
||||
a /= b = compare a b /= EQ
|
||||
@ -107,54 +116,41 @@ instance Eq Name where
|
||||
instance Ord Name where
|
||||
compare a b = compare (nUnique a) (nUnique b)
|
||||
|
||||
-- | Compare two names lexically.
|
||||
cmpNameLexical :: Name -> Name -> Ordering
|
||||
cmpNameLexical l r =
|
||||
case (nameInfo l, nameInfo r) of
|
||||
|
||||
(Declared nsl _,Declared nsr _) ->
|
||||
case compare nsl nsr of
|
||||
EQ -> comparing nameIdent l r
|
||||
cmp -> cmp
|
||||
|
||||
(Parameter,Parameter) -> comparing nameIdent l r
|
||||
|
||||
(Declared nsl _,Parameter) -> compare (modNameToText nsl)
|
||||
(identText (nameIdent r))
|
||||
(Parameter,Declared nsr _) -> compare (identText (nameIdent l))
|
||||
(modNameToText nsr)
|
||||
|
||||
|
||||
-- | Compare two names by the way they would be displayed.
|
||||
-- This is used to order names nicely when showing what's in scope
|
||||
cmpNameDisplay :: NameDisp -> Name -> Name -> Ordering
|
||||
cmpNameDisplay disp l r =
|
||||
case (nameInfo l, nameInfo r) of
|
||||
case (asOrigName l, asOrigName r) of
|
||||
|
||||
(Declared nsl _, Declared nsr _) -> -- XXX: uses system name info?
|
||||
let pfxl = fmtModName nsl (getNameFormat nsl (nameIdent l) disp)
|
||||
pfxr = fmtModName nsr (getNameFormat nsr (nameIdent r) disp)
|
||||
in case cmpText pfxl pfxr of
|
||||
EQ -> cmpName l r
|
||||
cmp -> cmp
|
||||
(Just ogl, Just ogr) -> -- XXX: uses system name info?
|
||||
case cmpText (fmtPref ogl) (fmtPref ogr) of
|
||||
EQ -> cmpName l r
|
||||
cmp -> cmp
|
||||
|
||||
(Parameter,Parameter) -> cmpName l r
|
||||
(Nothing,Nothing) -> cmpName l r
|
||||
|
||||
(Declared nsl _,Parameter) ->
|
||||
let pfxl = fmtModName nsl (getNameFormat nsl (nameIdent l) disp)
|
||||
in case cmpText pfxl (identText (nameIdent r)) of
|
||||
EQ -> GT
|
||||
cmp -> cmp
|
||||
(Just ogl,Nothing) ->
|
||||
case cmpText (fmtPref ogl) (identText (nameIdent r)) of
|
||||
EQ -> GT
|
||||
cmp -> cmp
|
||||
|
||||
(Parameter,Declared nsr _) ->
|
||||
let pfxr = fmtModName nsr (getNameFormat nsr (nameIdent r) disp)
|
||||
in case cmpText (identText (nameIdent l)) pfxr of
|
||||
EQ -> LT
|
||||
cmp -> cmp
|
||||
(Nothing,Just ogr) ->
|
||||
case cmpText (identText (nameIdent l)) (fmtPref ogr) of
|
||||
EQ -> LT
|
||||
cmp -> cmp
|
||||
|
||||
where
|
||||
cmpName xs ys = cmpIdent (nameIdent xs) (nameIdent ys)
|
||||
cmpIdent xs ys = cmpText (identText xs) (identText ys)
|
||||
|
||||
--- let pfxl = fmtModName nsl (getNameFormat nsl (nameIdent l) disp)
|
||||
fmtPref og = case getNameFormat og disp of
|
||||
UnQualified -> ""
|
||||
Qualified q -> modNameToText q
|
||||
NotInScope -> Text.pack $ show $ pp (ogModule og)
|
||||
|
||||
-- Note that this assumes that `xs` is `l` and `ys` is `r`
|
||||
cmpText xs ys =
|
||||
case (Text.null xs, Text.null ys) of
|
||||
@ -169,22 +165,17 @@ cmpNameDisplay disp l r =
|
||||
| a == '_' = 1
|
||||
| otherwise = 0
|
||||
|
||||
|
||||
|
||||
-- | Figure out how the name should be displayed, by referencing the display
|
||||
-- function in the environment. NOTE: this function doesn't take into account
|
||||
-- the need for parentheses.
|
||||
ppName :: Name -> Doc
|
||||
ppName Name { .. } =
|
||||
case nInfo of
|
||||
ppName nm =
|
||||
case asOrigName nm of
|
||||
Just og -> pp og
|
||||
Nothing -> pp (nameIdent nm)
|
||||
|
||||
Declared m _ -> withNameDisp $ \disp ->
|
||||
case getNameFormat m nIdent disp of
|
||||
Qualified m' -> ppQual m' <.> pp nIdent
|
||||
UnQualified -> pp nIdent
|
||||
NotInScope -> ppQual m <.> pp nIdent -- XXX: only when not in scope?
|
||||
where
|
||||
ppQual mo = if mo == exprModName then empty else pp mo <.> text "::"
|
||||
|
||||
Parameter -> pp nIdent
|
||||
|
||||
instance PP Name where
|
||||
ppPrec _ = ppPrefixName
|
||||
@ -199,6 +190,7 @@ instance PPName Name where
|
||||
|
||||
ppPrefixName n @ Name { .. } = optParens (isInfixIdent nIdent) (ppName n)
|
||||
|
||||
|
||||
-- | Pretty-print a name with its source location information.
|
||||
ppLocName :: Name -> Doc
|
||||
ppLocName n = pp Located { srcRange = nameLoc n, thing = n }
|
||||
@ -209,6 +201,9 @@ nameUnique = nUnique
|
||||
nameIdent :: Name -> Ident
|
||||
nameIdent = nIdent
|
||||
|
||||
nameNamespace :: Name -> Namespace
|
||||
nameNamespace = nNamespace
|
||||
|
||||
nameInfo :: Name -> NameInfo
|
||||
nameInfo = nInfo
|
||||
|
||||
@ -218,22 +213,31 @@ nameLoc = nLoc
|
||||
nameFixity :: Name -> Maybe Fixity
|
||||
nameFixity = nFixity
|
||||
|
||||
|
||||
-- | Primtiives must be in a top level module, at least for now.
|
||||
asPrim :: Name -> Maybe PrimIdent
|
||||
asPrim Name { .. } =
|
||||
case nInfo of
|
||||
Declared p _ -> Just $ PrimIdent p $ identText nIdent
|
||||
_ -> Nothing
|
||||
Declared (TopModule m) _ -> Just $ PrimIdent m $ identText nIdent
|
||||
_ -> Nothing
|
||||
|
||||
toParamInstName :: Name -> Name
|
||||
toParamInstName n =
|
||||
case nInfo n of
|
||||
Declared m s -> n { nInfo = Declared (paramInstModName m) s }
|
||||
Declared m s -> n { nInfo = Declared (apPathRoot paramInstModName m) s }
|
||||
Parameter -> n
|
||||
|
||||
asParamName :: Name -> Name
|
||||
asParamName n = n { nInfo = Parameter }
|
||||
|
||||
asOrigName :: Name -> Maybe OrigName
|
||||
asOrigName nm =
|
||||
case nInfo nm of
|
||||
Declared p _ -> Just OrigName { ogModule = p
|
||||
, ogNamespace = nNamespace nm
|
||||
, ogName = nIdent nm
|
||||
}
|
||||
Parameter -> Nothing
|
||||
|
||||
|
||||
-- Name Supply -----------------------------------------------------------------
|
||||
|
||||
@ -321,15 +325,17 @@ nextUnique (Supply n) = s' `seq` (n,s')
|
||||
-- Name Construction -----------------------------------------------------------
|
||||
|
||||
-- | Make a new name for a declaration.
|
||||
mkDeclared :: ModName -> NameSource -> Ident -> Maybe Fixity -> Range -> Supply -> (Name,Supply)
|
||||
mkDeclared m sys nIdent nFixity nLoc s =
|
||||
mkDeclared ::
|
||||
Namespace -> ModPath -> NameSource -> Ident -> Maybe Fixity -> Range ->
|
||||
Supply -> (Name,Supply)
|
||||
mkDeclared nNamespace m sys nIdent nFixity nLoc s =
|
||||
let (nUnique,s') = nextUnique s
|
||||
nInfo = Declared m sys
|
||||
in (Name { .. }, s')
|
||||
|
||||
-- | Make a new parameter name.
|
||||
mkParameter :: Ident -> Range -> Supply -> (Name,Supply)
|
||||
mkParameter nIdent nLoc s =
|
||||
mkParameter :: Namespace -> Ident -> Range -> Supply -> (Name,Supply)
|
||||
mkParameter nNamespace nIdent nLoc s =
|
||||
let (nUnique,s') = nextUnique s
|
||||
nFixity = Nothing
|
||||
in (Name { nInfo = Parameter, .. }, s')
|
||||
@ -340,6 +346,7 @@ paramModRecParam = Name { nInfo = Parameter
|
||||
, nIdent = packIdent "$modParams"
|
||||
, nLoc = emptyRange
|
||||
, nUnique = 0x01
|
||||
, nNamespace = NSValue
|
||||
}
|
||||
|
||||
-- Prim Maps -------------------------------------------------------------------
|
||||
|
@ -15,23 +15,17 @@
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
module Cryptol.ModuleSystem.NamingEnv where
|
||||
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.Parser.AST
|
||||
import Cryptol.Parser.Name(isGeneratedName)
|
||||
import Cryptol.Parser.Position
|
||||
import qualified Cryptol.TypeCheck.AST as T
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
|
||||
import Data.List (nub)
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Maybe (fromMaybe,mapMaybe,maybeToList)
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Set (Set)
|
||||
import qualified Data.Set as Set
|
||||
import Data.Semigroup
|
||||
import MonadLib (runId,Id)
|
||||
import MonadLib (runId,Id,StateT,runStateT,lift,sets_,forM_)
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
@ -39,46 +33,61 @@ import Control.DeepSeq
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.Parser.AST
|
||||
import Cryptol.Parser.Name(isGeneratedName)
|
||||
import Cryptol.Parser.Position
|
||||
import qualified Cryptol.TypeCheck.AST as T
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
import Cryptol.ModuleSystem.Name
|
||||
|
||||
|
||||
-- Naming Environment ----------------------------------------------------------
|
||||
|
||||
-- | The 'NamingEnv' is used by the renamer to determine what
|
||||
-- identifiers refer to.
|
||||
data NamingEnv = NamingEnv { neExprs :: !(Map.Map PName [Name])
|
||||
-- ^ Expr renaming environment
|
||||
, neTypes :: !(Map.Map PName [Name])
|
||||
-- ^ Type renaming environment
|
||||
} deriving (Show, Generic, NFData)
|
||||
newtype NamingEnv = NamingEnv (Map Namespace (Map PName [Name]))
|
||||
deriving (Show,Generic,NFData)
|
||||
|
||||
-- | Get the names in a given namespace
|
||||
namespaceMap :: Namespace -> NamingEnv -> Map PName [Name]
|
||||
namespaceMap ns (NamingEnv env) = Map.findWithDefault Map.empty ns env
|
||||
|
||||
-- | Resolve a name in the given namespace.
|
||||
lookupNS :: Namespace -> PName -> NamingEnv -> [Name]
|
||||
lookupNS ns x = Map.findWithDefault [] x . namespaceMap ns
|
||||
|
||||
-- | Return a list of value-level names to which this parsed name may refer.
|
||||
lookupValNames :: PName -> NamingEnv -> [Name]
|
||||
lookupValNames qn ro = Map.findWithDefault [] qn (neExprs ro)
|
||||
lookupValNames = lookupNS NSValue
|
||||
|
||||
-- | Return a list of type-level names to which this parsed name may refer.
|
||||
lookupTypeNames :: PName -> NamingEnv -> [Name]
|
||||
lookupTypeNames qn ro = Map.findWithDefault [] qn (neTypes ro)
|
||||
lookupTypeNames = lookupNS NSType
|
||||
|
||||
-- | Singleton renaming environment for the given namespace.
|
||||
singletonNS :: Namespace -> PName -> Name -> NamingEnv
|
||||
singletonNS ns pn n = NamingEnv (Map.singleton ns (Map.singleton pn [n]))
|
||||
|
||||
-- | Singleton expression renaming environment.
|
||||
singletonE :: PName -> Name -> NamingEnv
|
||||
singletonE = singletonNS NSValue
|
||||
|
||||
-- | Singleton type renaming environment.
|
||||
singletonT :: PName -> Name -> NamingEnv
|
||||
singletonT = singletonNS NSType
|
||||
|
||||
|
||||
|
||||
|
||||
instance Semigroup NamingEnv where
|
||||
l <> r =
|
||||
NamingEnv { neExprs = Map.unionWith merge (neExprs l) (neExprs r)
|
||||
, neTypes = Map.unionWith merge (neTypes l) (neTypes r) }
|
||||
NamingEnv l <> NamingEnv r =
|
||||
NamingEnv (Map.unionWith (Map.unionWith merge) l r)
|
||||
|
||||
instance Monoid NamingEnv where
|
||||
mempty =
|
||||
NamingEnv { neExprs = Map.empty
|
||||
, neTypes = Map.empty }
|
||||
|
||||
mappend l r = l <> r
|
||||
|
||||
mconcat envs =
|
||||
NamingEnv { neExprs = Map.unionsWith merge (map neExprs envs)
|
||||
, neTypes = Map.unionsWith merge (map neTypes envs) }
|
||||
|
||||
mempty = NamingEnv Map.empty
|
||||
{-# INLINE mempty #-}
|
||||
{-# INLINE mappend #-}
|
||||
{-# INLINE mconcat #-}
|
||||
|
||||
|
||||
-- | Merge two name maps, collapsing cases where the entries are the same, and
|
||||
@ -90,59 +99,53 @@ merge xs ys | xs == ys = xs
|
||||
-- | Generate a mapping from 'PrimIdent' to 'Name' for a
|
||||
-- given naming environment.
|
||||
toPrimMap :: NamingEnv -> PrimMap
|
||||
toPrimMap NamingEnv { .. } = PrimMap { .. }
|
||||
toPrimMap env =
|
||||
PrimMap
|
||||
{ primDecls = fromNS NSValue
|
||||
, primTypes = fromNS NSType
|
||||
}
|
||||
where
|
||||
fromNS ns = Map.fromList
|
||||
[ entry x | xs <- Map.elems (namespaceMap ns env), x <- xs ]
|
||||
|
||||
entry n = case asPrim n of
|
||||
Just p -> (p,n)
|
||||
Nothing -> panic "toPrimMap" [ "Not a declared name?"
|
||||
, show n
|
||||
]
|
||||
|
||||
primDecls = Map.fromList [ entry n | ns <- Map.elems neExprs, n <- ns ]
|
||||
primTypes = Map.fromList [ entry n | ns <- Map.elems neTypes, n <- ns ]
|
||||
|
||||
-- | Generate a display format based on a naming environment.
|
||||
toNameDisp :: NamingEnv -> NameDisp
|
||||
toNameDisp NamingEnv { .. } = NameDisp display
|
||||
toNameDisp env = NameDisp (`Map.lookup` names)
|
||||
where
|
||||
display mn ident = Map.lookup (mn,ident) names
|
||||
|
||||
-- only format declared names, as parameters don't need any special
|
||||
-- formatting.
|
||||
names = Map.fromList
|
||||
$ [ mkEntry (mn, nameIdent n) pn | (pn,ns) <- Map.toList neExprs
|
||||
, n <- ns
|
||||
, Declared mn _ <- [nameInfo n] ]
|
||||
|
||||
++ [ mkEntry (mn, nameIdent n) pn | (pn,ns) <- Map.toList neTypes
|
||||
, n <- ns
|
||||
, Declared mn _ <- [nameInfo n] ]
|
||||
|
||||
mkEntry key pn = (key,fmt)
|
||||
where fmt = case getModName pn of
|
||||
Just ns -> Qualified ns
|
||||
Nothing -> UnQualified
|
||||
[ (og, qn)
|
||||
| ns <- [ NSValue, NSType, NSModule ]
|
||||
, (pn,xs) <- Map.toList (namespaceMap ns env)
|
||||
, x <- xs
|
||||
, og <- maybeToList (asOrigName x)
|
||||
, let qn = case getModName pn of
|
||||
Just q -> Qualified q
|
||||
Nothing -> UnQualified
|
||||
]
|
||||
|
||||
|
||||
-- | Produce sets of visible names for types and declarations.
|
||||
--
|
||||
-- NOTE: if entries in the NamingEnv would have produced a name clash, they will
|
||||
-- be omitted from the resulting sets.
|
||||
visibleNames :: NamingEnv -> ({- types -} Set.Set Name
|
||||
,{- decls -} Set.Set Name)
|
||||
|
||||
visibleNames NamingEnv { .. } = (types,decls)
|
||||
-- NOTE: if entries in the NamingEnv would have produced a name clash,
|
||||
-- they will be omitted from the resulting sets.
|
||||
visibleNames :: NamingEnv -> Map Namespace (Set Name)
|
||||
visibleNames (NamingEnv env) = Set.fromList . mapMaybe check . Map.elems <$> env
|
||||
where
|
||||
types = Set.fromList [ n | [n] <- Map.elems neTypes ]
|
||||
decls = Set.fromList [ n | [n] <- Map.elems neExprs ]
|
||||
check names =
|
||||
case names of
|
||||
[name] -> Just name
|
||||
_ -> Nothing
|
||||
|
||||
-- | Qualify all symbols in a 'NamingEnv' with the given prefix.
|
||||
qualify :: ModName -> NamingEnv -> NamingEnv
|
||||
qualify pfx NamingEnv { .. } =
|
||||
NamingEnv { neExprs = Map.mapKeys toQual neExprs
|
||||
, neTypes = Map.mapKeys toQual neTypes
|
||||
}
|
||||
|
||||
qualify pfx (NamingEnv env) = NamingEnv (Map.mapKeys toQual <$> env)
|
||||
where
|
||||
-- XXX we don't currently qualify fresh names
|
||||
toQual (Qual _ n) = Qual pfx n
|
||||
@ -150,53 +153,84 @@ qualify pfx NamingEnv { .. } =
|
||||
toQual n@NewName{} = n
|
||||
|
||||
filterNames :: (PName -> Bool) -> NamingEnv -> NamingEnv
|
||||
filterNames p NamingEnv { .. } =
|
||||
NamingEnv { neExprs = Map.filterWithKey check neExprs
|
||||
, neTypes = Map.filterWithKey check neTypes
|
||||
}
|
||||
where
|
||||
check :: PName -> a -> Bool
|
||||
check n _ = p n
|
||||
filterNames p (NamingEnv env) = NamingEnv (Map.filterWithKey check <$> env)
|
||||
where check n _ = p n
|
||||
|
||||
|
||||
-- | Singleton type renaming environment.
|
||||
singletonT :: PName -> Name -> NamingEnv
|
||||
singletonT qn tn = mempty { neTypes = Map.singleton qn [tn] }
|
||||
|
||||
-- | Singleton expression renaming environment.
|
||||
singletonE :: PName -> Name -> NamingEnv
|
||||
singletonE qn en = mempty { neExprs = Map.singleton qn [en] }
|
||||
|
||||
-- | Like mappend, but when merging, prefer values on the lhs.
|
||||
shadowing :: NamingEnv -> NamingEnv -> NamingEnv
|
||||
shadowing l r = NamingEnv
|
||||
{ neExprs = Map.union (neExprs l) (neExprs r)
|
||||
, neTypes = Map.union (neTypes l) (neTypes r) }
|
||||
shadowing (NamingEnv l) (NamingEnv r) = NamingEnv (Map.unionWith Map.union l r)
|
||||
|
||||
travNamingEnv :: Applicative f => (Name -> f Name) -> NamingEnv -> f NamingEnv
|
||||
travNamingEnv f ne = NamingEnv <$> neExprs' <*> neTypes'
|
||||
where
|
||||
neExprs' = traverse (traverse f) (neExprs ne)
|
||||
neTypes' = traverse (traverse f) (neTypes ne)
|
||||
travNamingEnv f (NamingEnv mp) =
|
||||
NamingEnv <$> traverse (traverse (traverse f)) mp
|
||||
|
||||
|
||||
data InModule a = InModule !ModName a
|
||||
{- | Do somethign in context. If `Nothing` than we are working with
|
||||
a local declaration. Otherwise we are at the top-level of the
|
||||
given module. -}
|
||||
data InModule a = InModule (Maybe ModPath) a
|
||||
deriving (Functor,Traversable,Foldable,Show)
|
||||
|
||||
|
||||
-- | Generate a 'NamingEnv' using an explicit supply.
|
||||
namingEnv' :: BindsNames a => a -> Supply -> (NamingEnv,Supply)
|
||||
namingEnv' a supply = runId (runSupplyT supply (runBuild (namingEnv a)))
|
||||
|
||||
newTop :: FreshM m => ModName -> PName -> Maybe Fixity -> Range -> m Name
|
||||
newTop ns thing fx rng = liftSupply (mkDeclared ns src (getIdent thing) fx rng)
|
||||
newTop ::
|
||||
FreshM m => Namespace -> ModPath -> PName -> Maybe Fixity -> Range -> m Name
|
||||
newTop ns m thing fx rng =
|
||||
liftSupply (mkDeclared ns m src (getIdent thing) fx rng)
|
||||
where src = if isGeneratedName thing then SystemName else UserName
|
||||
|
||||
newLocal :: FreshM m => PName -> Range -> m Name
|
||||
newLocal thing rng = liftSupply (mkParameter (getIdent thing) rng)
|
||||
newLocal :: FreshM m => Namespace -> PName -> Range -> m Name
|
||||
newLocal ns thing rng = liftSupply (mkParameter ns (getIdent thing) rng)
|
||||
|
||||
newtype BuildNamingEnv = BuildNamingEnv { runBuild :: SupplyT Id NamingEnv }
|
||||
|
||||
|
||||
buildNamingEnv :: BuildNamingEnv -> Supply -> (NamingEnv,Supply)
|
||||
buildNamingEnv b supply = runId $ runSupplyT supply $ runBuild b
|
||||
|
||||
-- | Generate a 'NamingEnv' using an explicit supply.
|
||||
defsOf :: BindsNames a => a -> Supply -> (NamingEnv,Supply)
|
||||
defsOf = buildNamingEnv . namingEnv
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Collect definitions of nested modules
|
||||
|
||||
type NestedMods = Map Name NamingEnv
|
||||
type CollectM = StateT NestedMods (SupplyT Id)
|
||||
|
||||
collectNestedModules ::
|
||||
NamingEnv -> Module PName -> Supply -> (NestedMods, Supply)
|
||||
collectNestedModules env m =
|
||||
collectNestedModulesDecls env (thing (mName m)) (mDecls m)
|
||||
|
||||
collectNestedModulesDecls ::
|
||||
NamingEnv -> ModName -> [TopDecl PName] -> Supply -> (NestedMods, Supply)
|
||||
collectNestedModulesDecls env m ds sup = (mp,newS)
|
||||
where
|
||||
s0 = Map.empty
|
||||
mpath = TopModule m
|
||||
((_,mp),newS) = runId $ runSupplyT sup $ runStateT s0 $
|
||||
collectNestedModulesDs mpath env ds
|
||||
|
||||
collectNestedModulesDs :: ModPath -> NamingEnv -> [TopDecl PName] -> CollectM ()
|
||||
collectNestedModulesDs mpath env ds =
|
||||
forM_ [ tlValue nm | DModule nm <- ds ] \(NestedModule nested) ->
|
||||
do let pname = thing (mName nested)
|
||||
name = case lookupNS NSModule pname env of
|
||||
[n] -> n
|
||||
_ -> panic "collectedNestedModulesDs"
|
||||
[ "Missing/ambi definition for " ++ show pname ]
|
||||
newEnv <- lift (runBuild (moduleDefs (Nested mpath (nameIdent name)) nested))
|
||||
sets_ (Map.insert name newEnv)
|
||||
let newMPath = Nested mpath (nameIdent name)
|
||||
collectNestedModulesDs newMPath newEnv (mDecls nested)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
|
||||
|
||||
|
||||
instance Semigroup BuildNamingEnv where
|
||||
BuildNamingEnv a <> BuildNamingEnv b = BuildNamingEnv $
|
||||
do x <- a
|
||||
@ -212,6 +246,10 @@ instance Monoid BuildNamingEnv where
|
||||
do ns <- sequence (map runBuild bs)
|
||||
return (mconcat ns)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
|
||||
|
||||
-- | Things that define exported names.
|
||||
class BindsNames a where
|
||||
namingEnv :: a -> BuildNamingEnv
|
||||
@ -235,12 +273,12 @@ instance BindsNames (Schema PName) where
|
||||
{-# INLINE namingEnv #-}
|
||||
|
||||
|
||||
-- | Interpret an import in the context of an interface, to produce a name
|
||||
-- environment for the renamer, and a 'NameDisp' for pretty-printing.
|
||||
interpImport :: Import {- ^ The import declarations -} ->
|
||||
IfaceDecls {- ^ Declarations of imported module -} ->
|
||||
|
||||
-- | Adapt the things exported by something to the specific import/open.
|
||||
interpImportEnv :: ImportG name {- ^ The import declarations -} ->
|
||||
NamingEnv {- ^ All public things coming in -} ->
|
||||
NamingEnv
|
||||
interpImport imp publicDecls = qualified
|
||||
interpImportEnv imp public = qualified
|
||||
where
|
||||
|
||||
-- optionally qualify names based on the import
|
||||
@ -257,16 +295,21 @@ interpImport imp publicDecls = qualified
|
||||
|
||||
| otherwise = public
|
||||
|
||||
-- generate the initial environment from the public interface, where no names
|
||||
-- are qualified
|
||||
public = unqualifiedEnv publicDecls
|
||||
|
||||
|
||||
-- | Interpret an import in the context of an interface, to produce a name
|
||||
-- environment for the renamer, and a 'NameDisp' for pretty-printing.
|
||||
interpImportIface :: Import {- ^ The import declarations -} ->
|
||||
IfaceDecls {- ^ Declarations of imported module -} ->
|
||||
NamingEnv
|
||||
interpImportIface imp = interpImportEnv imp . unqualifiedEnv
|
||||
|
||||
|
||||
-- | Generate a naming environment from a declaration interface, where none of
|
||||
-- the names are qualified.
|
||||
unqualifiedEnv :: IfaceDecls -> NamingEnv
|
||||
unqualifiedEnv IfaceDecls { .. } =
|
||||
mconcat [ exprs, tySyns, ntTypes, absTys, ntExprs ]
|
||||
mconcat [ exprs, tySyns, ntTypes, absTys, ntExprs, mods ]
|
||||
where
|
||||
toPName n = mkUnqual (nameIdent n)
|
||||
|
||||
@ -275,16 +318,17 @@ unqualifiedEnv IfaceDecls { .. } =
|
||||
ntTypes = mconcat [ singletonT (toPName n) n | n <- Map.keys ifNewtypes ]
|
||||
absTys = mconcat [ singletonT (toPName n) n | n <- Map.keys ifAbstractTypes ]
|
||||
ntExprs = mconcat [ singletonE (toPName n) n | n <- Map.keys ifNewtypes ]
|
||||
|
||||
mods = mconcat [ singletonNS NSModule (toPName n) n
|
||||
| n <- Map.keys ifModules ]
|
||||
|
||||
-- | Compute an unqualified naming environment, containing the various module
|
||||
-- parameters.
|
||||
modParamsNamingEnv :: IfaceParams -> NamingEnv
|
||||
modParamsNamingEnv IfaceParams { .. } =
|
||||
NamingEnv { neExprs = Map.fromList $ map fromFu $ Map.keys ifParamFuns
|
||||
, neTypes = Map.fromList $ map fromTy $ Map.elems ifParamTypes
|
||||
}
|
||||
|
||||
NamingEnv $ Map.fromList
|
||||
[ (NSValue, Map.fromList $ map fromFu $ Map.keys ifParamFuns)
|
||||
, (NSType, Map.fromList $ map fromTy $ Map.elems ifParamTypes)
|
||||
]
|
||||
where
|
||||
toPName n = mkUnqual (nameIdent n)
|
||||
|
||||
@ -301,14 +345,16 @@ data ImportIface = ImportIface Import Iface
|
||||
-- mapping only from unqualified names to qualified ones.
|
||||
instance BindsNames ImportIface where
|
||||
namingEnv (ImportIface imp Iface { .. }) = BuildNamingEnv $
|
||||
return (interpImport imp ifPublic)
|
||||
return (interpImportIface imp ifPublic)
|
||||
{-# INLINE namingEnv #-}
|
||||
|
||||
-- | Introduce the name
|
||||
instance BindsNames (InModule (Bind PName)) where
|
||||
namingEnv (InModule ns b) = BuildNamingEnv $
|
||||
namingEnv (InModule mb b) = BuildNamingEnv $
|
||||
do let Located { .. } = bName b
|
||||
n <- newTop ns thing (bFixity b) srcRange
|
||||
n <- case mb of
|
||||
Just m -> newTop NSValue m thing (bFixity b) srcRange
|
||||
Nothing -> newLocal NSValue thing srcRange -- local fixitiies?
|
||||
|
||||
return (singletonE thing n)
|
||||
|
||||
@ -316,15 +362,18 @@ instance BindsNames (InModule (Bind PName)) where
|
||||
instance BindsNames (TParam PName) where
|
||||
namingEnv TParam { .. } = BuildNamingEnv $
|
||||
do let range = fromMaybe emptyRange tpRange
|
||||
n <- newLocal tpName range
|
||||
n <- newLocal NSType tpName range
|
||||
return (singletonT tpName n)
|
||||
|
||||
-- | The naming environment for a single module. This is the mapping from
|
||||
-- unqualified names to fully qualified names with uniques.
|
||||
instance BindsNames (Module PName) where
|
||||
namingEnv Module { .. } = foldMap (namingEnv . InModule ns) mDecls
|
||||
where
|
||||
ns = thing mName
|
||||
namingEnv m = moduleDefs (TopModule (thing (mName m))) m
|
||||
|
||||
|
||||
moduleDefs :: ModPath -> ModuleG mname PName -> BuildNamingEnv
|
||||
moduleDefs m Module { .. } = foldMap (namingEnv . InModule (Just m)) mDecls
|
||||
|
||||
|
||||
instance BindsNames (InModule (TopDecl PName)) where
|
||||
namingEnv (InModule ns td) =
|
||||
@ -335,60 +384,70 @@ instance BindsNames (InModule (TopDecl PName)) where
|
||||
DParameterType d -> namingEnv (InModule ns d)
|
||||
DParameterConstraint {} -> mempty
|
||||
DParameterFun d -> namingEnv (InModule ns d)
|
||||
Include _ -> mempty
|
||||
Include _ -> mempty
|
||||
DImport {} -> mempty -- see 'openLoop' in the renamer
|
||||
DModule m -> namingEnv (InModule ns (tlValue m))
|
||||
|
||||
|
||||
instance BindsNames (InModule (NestedModule PName)) where
|
||||
namingEnv (InModule ~(Just m) (NestedModule mdef)) = BuildNamingEnv $
|
||||
do let pnmame = mName mdef
|
||||
nm <- newTop NSModule m (thing pnmame) Nothing (srcRange pnmame)
|
||||
pure (singletonNS NSModule (thing pnmame) nm)
|
||||
|
||||
instance BindsNames (InModule (PrimType PName)) where
|
||||
namingEnv (InModule ns PrimType { .. }) =
|
||||
namingEnv (InModule ~(Just m) PrimType { .. }) =
|
||||
BuildNamingEnv $
|
||||
do let Located { .. } = primTName
|
||||
nm <- newTop ns thing primTFixity srcRange
|
||||
nm <- newTop NSType m thing primTFixity srcRange
|
||||
pure (singletonT thing nm)
|
||||
|
||||
instance BindsNames (InModule (ParameterFun PName)) where
|
||||
namingEnv (InModule ns ParameterFun { .. }) = BuildNamingEnv $
|
||||
namingEnv (InModule ~(Just ns) ParameterFun { .. }) = BuildNamingEnv $
|
||||
do let Located { .. } = pfName
|
||||
ntName <- newTop ns thing pfFixity srcRange
|
||||
ntName <- newTop NSValue ns thing pfFixity srcRange
|
||||
return (singletonE thing ntName)
|
||||
|
||||
instance BindsNames (InModule (ParameterType PName)) where
|
||||
namingEnv (InModule ns ParameterType { .. }) = BuildNamingEnv $
|
||||
namingEnv (InModule ~(Just ns) ParameterType { .. }) = BuildNamingEnv $
|
||||
-- XXX: we don't seem to have a fixity environment at the type level
|
||||
do let Located { .. } = ptName
|
||||
ntName <- newTop ns thing Nothing srcRange
|
||||
ntName <- newTop NSType ns thing Nothing srcRange
|
||||
return (singletonT thing ntName)
|
||||
|
||||
-- NOTE: we use the same name at the type and expression level, as there's only
|
||||
-- ever one name introduced in the declaration. The names are only ever used in
|
||||
-- different namespaces, so there's no ambiguity.
|
||||
instance BindsNames (InModule (Newtype PName)) where
|
||||
namingEnv (InModule ns Newtype { .. }) = BuildNamingEnv $
|
||||
namingEnv (InModule ~(Just ns) Newtype { .. }) = BuildNamingEnv $
|
||||
do let Located { .. } = nName
|
||||
ntName <- newTop ns thing Nothing srcRange
|
||||
ntName <- newTop NSType ns thing Nothing srcRange
|
||||
-- XXX: the name reuse here is sketchy
|
||||
return (singletonT thing ntName `mappend` singletonE thing ntName)
|
||||
|
||||
-- | The naming environment for a single declaration.
|
||||
instance BindsNames (InModule (Decl PName)) where
|
||||
namingEnv (InModule pfx d) = case d of
|
||||
DBind b -> BuildNamingEnv $
|
||||
do n <- mkName (bName b) (bFixity b)
|
||||
return (singletonE (thing (bName b)) n)
|
||||
|
||||
DBind b -> namingEnv (InModule pfx b)
|
||||
DSignature ns _sig -> foldMap qualBind ns
|
||||
DPragma ns _p -> foldMap qualBind ns
|
||||
DType syn -> qualType (tsName syn) (tsFixity syn)
|
||||
DProp syn -> qualType (psName syn) (psFixity syn)
|
||||
DLocated d' _ -> namingEnv (InModule pfx d')
|
||||
DPatBind _pat _e -> panic "ModuleSystem" ["Unexpected pattern binding"]
|
||||
DFixity{} -> panic "ModuleSystem" ["Unexpected fixity declaration"]
|
||||
DRec {} -> panic "namingEnv" [ "DRec" ]
|
||||
DPatBind _pat _e -> panic "namingEnv" ["Unexpected pattern binding"]
|
||||
DFixity{} -> panic "namingEnv" ["Unexpected fixity declaration"]
|
||||
|
||||
where
|
||||
|
||||
mkName ln fx = newTop pfx (thing ln) fx (srcRange ln)
|
||||
mkName ns ln fx = case pfx of
|
||||
Just m -> newTop ns m (thing ln) fx (srcRange ln)
|
||||
Nothing -> newLocal ns (thing ln) (srcRange ln)
|
||||
|
||||
qualBind ln = BuildNamingEnv $
|
||||
do n <- mkName ln Nothing
|
||||
do n <- mkName NSValue ln Nothing
|
||||
return (singletonE (thing ln) n)
|
||||
|
||||
qualType ln f = BuildNamingEnv $
|
||||
do n <- mkName ln f
|
||||
do n <- mkName NSType ln f
|
||||
return (singletonT (thing ln) n)
|
||||
|
File diff suppressed because it is too large
Load Diff
197
src/Cryptol/ModuleSystem/Renamer/Error.hs
Normal file
197
src/Cryptol/ModuleSystem/Renamer/Error.hs
Normal file
@ -0,0 +1,197 @@
|
||||
-- |
|
||||
-- Module : Cryptol.ModuleSystem.Renamer
|
||||
-- Copyright : (c) 2013-2016 Galois, Inc.
|
||||
-- License : BSD3
|
||||
-- Maintainer : cryptol@galois.com
|
||||
-- Stability : provisional
|
||||
-- Portability : portable
|
||||
|
||||
{-# Language DeriveGeneric, DeriveAnyClass #-}
|
||||
{-# Language OverloadedStrings #-}
|
||||
module Cryptol.ModuleSystem.Renamer.Error where
|
||||
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.Parser.AST
|
||||
import Cryptol.Parser.Position
|
||||
import Cryptol.Parser.Selector(ppNestedSels)
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
-- Errors ----------------------------------------------------------------------
|
||||
|
||||
data RenamerError
|
||||
= MultipleSyms (Located PName) [Name]
|
||||
-- ^ Multiple imported symbols contain this name
|
||||
|
||||
| UnboundName Namespace (Located PName)
|
||||
-- ^ Some name not bound to any definition
|
||||
|
||||
| OverlappingSyms [Name]
|
||||
-- ^ An environment has produced multiple overlapping symbols
|
||||
|
||||
| WrongNamespace Namespace Namespace (Located PName)
|
||||
-- ^ expected, actual.
|
||||
-- When a name is missing from the expected namespace, but exists in another
|
||||
|
||||
| FixityError (Located Name) Fixity (Located Name) Fixity
|
||||
-- ^ When the fixity of two operators conflict
|
||||
|
||||
| InvalidConstraint (Type PName)
|
||||
-- ^ When it's not possible to produce a Prop from a Type.
|
||||
|
||||
| MalformedBuiltin (Type PName) PName
|
||||
-- ^ When a builtin type/type-function is used incorrectly.
|
||||
|
||||
| BoundReservedType PName (Maybe Range) Doc
|
||||
-- ^ When a builtin type is named in a binder.
|
||||
|
||||
| OverlappingRecordUpdate (Located [Selector]) (Located [Selector])
|
||||
-- ^ When record updates overlap (e.g., @{ r | x = e1, x.y = e2 }@)
|
||||
|
||||
| InvalidDependency [DepName]
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
|
||||
-- We use this because parameter constrstaints have no names
|
||||
data DepName = NamedThing Name
|
||||
| ConstratintAt Range -- ^ identifed by location in source
|
||||
deriving (Eq,Ord,Show,Generic,NFData)
|
||||
|
||||
|
||||
|
||||
instance PP RenamerError where
|
||||
ppPrec _ e = case e of
|
||||
|
||||
MultipleSyms lqn qns ->
|
||||
hang (text "[error] at" <+> pp (srcRange lqn))
|
||||
4 $ (text "Multiple definitions for symbol:" <+> pp (thing lqn))
|
||||
$$ vcat (map ppLocName qns)
|
||||
|
||||
UnboundName ns lqn ->
|
||||
hang (text "[error] at" <+> pp (srcRange lqn))
|
||||
4 (something <+> "not in scope:" <+> pp (thing lqn))
|
||||
where
|
||||
something = case ns of
|
||||
NSValue -> "Value"
|
||||
NSType -> "Type"
|
||||
NSModule -> "Module"
|
||||
|
||||
OverlappingSyms qns ->
|
||||
hang (text "[error]")
|
||||
4 $ text "Overlapping symbols defined:"
|
||||
$$ vcat (map ppLocName qns)
|
||||
|
||||
WrongNamespace expected actual lqn ->
|
||||
hang ("[error] at" <+> pp (srcRange lqn ))
|
||||
4 (fsep
|
||||
[ "Expected a", sayNS expected, "named", quotes (pp (thing lqn))
|
||||
, "but found a", sayNS actual, "instead"
|
||||
, suggestion
|
||||
])
|
||||
where
|
||||
sayNS ns = case ns of
|
||||
NSValue -> "value"
|
||||
NSType -> "type"
|
||||
NSModule -> "module"
|
||||
suggestion =
|
||||
case (expected,actual) of
|
||||
(NSValue,NSType) ->
|
||||
"Did you mean `(" <.> pp (thing lqn) <.> text")?"
|
||||
_ -> empty
|
||||
|
||||
FixityError o1 f1 o2 f2 ->
|
||||
hang (text "[error] at" <+> pp (srcRange o1) <+> text "and" <+> pp (srcRange o2))
|
||||
4 (fsep [ text "The fixities of"
|
||||
, nest 2 $ vcat
|
||||
[ "•" <+> pp (thing o1) <+> parens (pp f1)
|
||||
, "•" <+> pp (thing o2) <+> parens (pp f2) ]
|
||||
, text "are not compatible."
|
||||
, text "You may use explicit parentheses to disambiguate." ])
|
||||
|
||||
InvalidConstraint ty ->
|
||||
hang (text "[error]" <+> maybe empty (\r -> text "at" <+> pp r) (getLoc ty))
|
||||
4 (fsep [ pp ty, text "is not a valid constraint" ])
|
||||
|
||||
MalformedBuiltin ty pn ->
|
||||
hang (text "[error]" <+> maybe empty (\r -> text "at" <+> pp r) (getLoc ty))
|
||||
4 (fsep [ text "invalid use of built-in type", pp pn
|
||||
, text "in type", pp ty ])
|
||||
|
||||
BoundReservedType n loc src ->
|
||||
hang (text "[error]" <+> maybe empty (\r -> text "at" <+> pp r) loc)
|
||||
4 (fsep [ text "built-in type", quotes (pp n), text "shadowed in", src ])
|
||||
|
||||
OverlappingRecordUpdate xs ys ->
|
||||
hang "[error] Overlapping record updates:"
|
||||
4 (vcat [ ppLab xs, ppLab ys ])
|
||||
where
|
||||
ppLab as = ppNestedSels (thing as) <+> "at" <+> pp (srcRange as)
|
||||
|
||||
InvalidDependency ds ->
|
||||
"[error] Invalid recursive dependency:"
|
||||
$$ nest 4 (vcat [ "•" <+> pp x | x <- ds ])
|
||||
|
||||
instance PP DepName where
|
||||
ppPrec _ d =
|
||||
case d of
|
||||
ConstratintAt r -> "constraint at" <+> pp r
|
||||
NamedThing n ->
|
||||
case nameNamespace n of
|
||||
NSModule -> "submodule" <+> pp n
|
||||
NSType -> "type" <+> pp n
|
||||
NSValue -> pp n
|
||||
|
||||
|
||||
|
||||
-- Warnings --------------------------------------------------------------------
|
||||
|
||||
data RenamerWarning
|
||||
= SymbolShadowed PName Name [Name]
|
||||
| UnusedName Name
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
instance Eq RenamerWarning where
|
||||
x == y = compare x y == EQ
|
||||
|
||||
-- used to determine in what order ot show things
|
||||
instance Ord RenamerWarning where
|
||||
compare w1 w2 =
|
||||
case w1 of
|
||||
SymbolShadowed x y _ ->
|
||||
case w2 of
|
||||
SymbolShadowed x' y' _ -> compare (byStart y,x) (byStart y',x')
|
||||
_ -> LT
|
||||
UnusedName x ->
|
||||
case w2 of
|
||||
UnusedName y -> compare (byStart x) (byStart y)
|
||||
_ -> GT
|
||||
|
||||
where
|
||||
byStart = from . nameLoc
|
||||
|
||||
|
||||
instance PP RenamerWarning where
|
||||
ppPrec _ (SymbolShadowed k x os) =
|
||||
hang (text "[warning] at" <+> loc)
|
||||
4 $ fsep [ "This binding for" <+> backticks (pp k)
|
||||
, "shadows the existing binding" <.> plural
|
||||
, text "at" ]
|
||||
$$ vcat (map (pp . nameLoc) os)
|
||||
|
||||
where
|
||||
plural | length os > 1 = char 's'
|
||||
| otherwise = empty
|
||||
|
||||
loc = pp (nameLoc x)
|
||||
|
||||
ppPrec _ (UnusedName x) =
|
||||
hang (text "[warning] at" <+> pp (nameLoc x))
|
||||
4 (text "Unused name:" <+> pp x)
|
||||
|
||||
|
||||
|
329
src/Cryptol/ModuleSystem/Renamer/Monad.hs
Normal file
329
src/Cryptol/ModuleSystem/Renamer/Monad.hs
Normal file
@ -0,0 +1,329 @@
|
||||
-- |
|
||||
-- Module : Cryptol.ModuleSystem.Renamer
|
||||
-- Copyright : (c) 2013-2016 Galois, Inc.
|
||||
-- License : BSD3
|
||||
-- Maintainer : cryptol@galois.com
|
||||
-- Stability : provisional
|
||||
-- Portability : portable
|
||||
|
||||
{-# Language RecordWildCards #-}
|
||||
{-# Language FlexibleContexts #-}
|
||||
{-# Language BlockArguments #-}
|
||||
module Cryptol.ModuleSystem.Renamer.Monad where
|
||||
|
||||
import Data.List(sort)
|
||||
import Data.Set(Set)
|
||||
import qualified Data.Set as Set
|
||||
import qualified Data.Foldable as F
|
||||
import Data.Map.Strict ( Map )
|
||||
import qualified Data.Map.Strict as Map
|
||||
import qualified Data.Sequence as Seq
|
||||
import qualified Data.Semigroup as S
|
||||
import MonadLib hiding (mapM, mapM_)
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.ModuleSystem.NamingEnv
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
import Cryptol.Parser.AST
|
||||
import Cryptol.Parser.Position
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.Utils.Ident(containsModule)
|
||||
|
||||
import Cryptol.ModuleSystem.Renamer.Error
|
||||
|
||||
-- | Indicates if a name is in a binding poisition or a use site
|
||||
data NameType = NameBind | NameUse
|
||||
|
||||
-- | Information needed to do some renaming.
|
||||
data RenamerInfo = RenamerInfo
|
||||
{ renSupply :: Supply -- ^ Use to make new names
|
||||
, renContext :: ModPath -- ^ We are renaming things in here
|
||||
, renEnv :: NamingEnv -- ^ This is what's in scope
|
||||
, renIfaces :: ModName -> Iface
|
||||
}
|
||||
|
||||
newtype RenameM a = RenameM { unRenameM :: ReaderT RO (StateT RW Lift) a }
|
||||
|
||||
data RO = RO
|
||||
{ roLoc :: Range
|
||||
, roNames :: NamingEnv
|
||||
, roIfaces :: ModName -> Iface
|
||||
, roCurMod :: ModPath -- ^ Current module we are working on
|
||||
, roNestedMods :: Map ModPath Name
|
||||
}
|
||||
|
||||
data RW = RW
|
||||
{ rwWarnings :: ![RenamerWarning]
|
||||
, rwErrors :: !(Seq.Seq RenamerError)
|
||||
, rwSupply :: !Supply
|
||||
, rwNameUseCount :: !(Map Name Int)
|
||||
-- ^ How many times did we refer to each name.
|
||||
-- Used to generate warnings for unused definitions.
|
||||
|
||||
, rwCurrentDeps :: Set Name
|
||||
-- ^ keeps track of names *used* by something.
|
||||
-- see 'depsOf'
|
||||
|
||||
, rwDepGraph :: Map DepName (Set Name)
|
||||
-- ^ keeps track of the dependencies for things.
|
||||
-- see 'depsOf'
|
||||
|
||||
, rwExternalDeps :: !IfaceDecls
|
||||
}
|
||||
|
||||
|
||||
|
||||
instance S.Semigroup a => S.Semigroup (RenameM a) where
|
||||
{-# INLINE (<>) #-}
|
||||
a <> b =
|
||||
do x <- a
|
||||
y <- b
|
||||
return (x S.<> y)
|
||||
|
||||
instance (S.Semigroup a, Monoid a) => Monoid (RenameM a) where
|
||||
{-# INLINE mempty #-}
|
||||
mempty = return mempty
|
||||
|
||||
{-# INLINE mappend #-}
|
||||
mappend = (S.<>)
|
||||
|
||||
instance Functor RenameM where
|
||||
{-# INLINE fmap #-}
|
||||
fmap f m = RenameM (fmap f (unRenameM m))
|
||||
|
||||
instance Applicative RenameM where
|
||||
{-# INLINE pure #-}
|
||||
pure x = RenameM (pure x)
|
||||
|
||||
{-# INLINE (<*>) #-}
|
||||
l <*> r = RenameM (unRenameM l <*> unRenameM r)
|
||||
|
||||
instance Monad RenameM where
|
||||
{-# INLINE return #-}
|
||||
return x = RenameM (return x)
|
||||
|
||||
{-# INLINE (>>=) #-}
|
||||
m >>= k = RenameM (unRenameM m >>= unRenameM . k)
|
||||
|
||||
instance FreshM RenameM where
|
||||
liftSupply f = RenameM $ sets $ \ RW { .. } ->
|
||||
let (a,s') = f rwSupply
|
||||
rw' = RW { rwSupply = s', .. }
|
||||
in a `seq` rw' `seq` (a, rw')
|
||||
|
||||
|
||||
runRenamer :: RenamerInfo -> RenameM a
|
||||
-> ( Either [RenamerError] (a,Supply)
|
||||
, [RenamerWarning]
|
||||
)
|
||||
runRenamer info m = (res, warns)
|
||||
where
|
||||
warns = sort (rwWarnings rw ++ warnUnused (renContext info) (renEnv info) rw)
|
||||
|
||||
(a,rw) = runM (unRenameM m) ro
|
||||
RW { rwErrors = Seq.empty
|
||||
, rwWarnings = []
|
||||
, rwSupply = renSupply info
|
||||
, rwNameUseCount = Map.empty
|
||||
, rwExternalDeps = mempty
|
||||
, rwCurrentDeps = Set.empty
|
||||
, rwDepGraph = Map.empty
|
||||
}
|
||||
|
||||
ro = RO { roLoc = emptyRange
|
||||
, roNames = renEnv info
|
||||
, roIfaces = renIfaces info
|
||||
, roCurMod = renContext info
|
||||
, roNestedMods = Map.empty
|
||||
}
|
||||
|
||||
res | Seq.null (rwErrors rw) = Right (a,rwSupply rw)
|
||||
| otherwise = Left (F.toList (rwErrors rw))
|
||||
|
||||
|
||||
setCurMod :: ModPath -> RenameM a -> RenameM a
|
||||
setCurMod mpath (RenameM m) =
|
||||
RenameM $ mapReader (\ro -> ro { roCurMod = mpath }) m
|
||||
|
||||
getCurMod :: RenameM ModPath
|
||||
getCurMod = RenameM $ asks roCurMod
|
||||
|
||||
|
||||
setNestedModule :: Map ModPath Name -> RenameM a -> RenameM a
|
||||
setNestedModule mp (RenameM m) =
|
||||
RenameM $ mapReader (\ro -> ro { roNestedMods = mp }) m
|
||||
|
||||
nestedModuleOrig :: ModPath -> RenameM (Maybe Name)
|
||||
nestedModuleOrig x = RenameM (asks (Map.lookup x . roNestedMods))
|
||||
|
||||
|
||||
-- | Record an error. XXX: use a better name
|
||||
record :: RenamerError -> RenameM ()
|
||||
record f = RenameM $
|
||||
do RW { .. } <- get
|
||||
set RW { rwErrors = rwErrors Seq.|> f, .. }
|
||||
|
||||
collectIfaceDeps :: RenameM a -> RenameM (IfaceDecls,a)
|
||||
collectIfaceDeps (RenameM m) =
|
||||
RenameM
|
||||
do ds <- sets \s -> (rwExternalDeps s, s { rwExternalDeps = mempty })
|
||||
a <- m
|
||||
ds' <- sets \s -> (rwExternalDeps s, s { rwExternalDeps = ds })
|
||||
pure (ds',a)
|
||||
|
||||
-- | Rename something. All name uses in the sub-computation are assumed
|
||||
-- to be dependenices of the thing.
|
||||
depsOf :: DepName -> RenameM a -> RenameM a
|
||||
depsOf x (RenameM m) = RenameM
|
||||
do ds <- sets \rw -> (rwCurrentDeps rw, rw { rwCurrentDeps = Set.empty })
|
||||
a <- m
|
||||
sets_ \rw ->
|
||||
rw { rwCurrentDeps = Set.union (rwCurrentDeps rw) ds
|
||||
, rwDepGraph = Map.insert x (rwCurrentDeps rw) (rwDepGraph rw)
|
||||
}
|
||||
pure a
|
||||
|
||||
-- | This is used when renaming a group of things. The result contains
|
||||
-- dependencies between names defines and the group, and is intended to
|
||||
-- be used to order the group members in dependency order.
|
||||
depGroup :: RenameM a -> RenameM (a, Map DepName (Set Name))
|
||||
depGroup (RenameM m) = RenameM
|
||||
do ds <- sets \rw -> (rwDepGraph rw, rw { rwDepGraph = Map.empty })
|
||||
a <- m
|
||||
ds1 <- sets \rw -> (rwDepGraph rw, rw { rwDepGraph = ds })
|
||||
pure (a,ds1)
|
||||
|
||||
-- | Get the source range for wahtever we are currently renaming.
|
||||
curLoc :: RenameM Range
|
||||
curLoc = RenameM (roLoc `fmap` ask)
|
||||
|
||||
-- | Annotate something with the current range.
|
||||
located :: a -> RenameM (Located a)
|
||||
located thing =
|
||||
do srcRange <- curLoc
|
||||
return Located { .. }
|
||||
|
||||
-- | Do the given computation using the source code range from `loc` if any.
|
||||
withLoc :: HasLoc loc => loc -> RenameM a -> RenameM a
|
||||
withLoc loc m = RenameM $ case getLoc loc of
|
||||
|
||||
Just range -> do
|
||||
ro <- ask
|
||||
local ro { roLoc = range } (unRenameM m)
|
||||
|
||||
Nothing -> unRenameM m
|
||||
|
||||
|
||||
-- | Shadow the current naming environment with some more names.
|
||||
shadowNames :: BindsNames env => env -> RenameM a -> RenameM a
|
||||
shadowNames = shadowNames' CheckAll
|
||||
|
||||
data EnvCheck = CheckAll -- ^ Check for overlap and shadowing
|
||||
| CheckOverlap -- ^ Only check for overlap
|
||||
| CheckNone -- ^ Don't check the environment
|
||||
deriving (Eq,Show)
|
||||
|
||||
-- | Shadow the current naming environment with some more names.
|
||||
shadowNames' :: BindsNames env => EnvCheck -> env -> RenameM a -> RenameM a
|
||||
shadowNames' check names m = do
|
||||
do env <- liftSupply (defsOf names)
|
||||
RenameM $
|
||||
do ro <- ask
|
||||
env' <- sets (checkEnv check env (roNames ro))
|
||||
let ro' = ro { roNames = env' `shadowing` roNames ro }
|
||||
local ro' (unRenameM m)
|
||||
|
||||
-- | Generate warnings when the left environment shadows things defined in
|
||||
-- the right. Additionally, generate errors when two names overlap in the
|
||||
-- left environment.
|
||||
checkEnv :: EnvCheck -> NamingEnv -> NamingEnv -> RW -> (NamingEnv,RW)
|
||||
checkEnv check (NamingEnv lenv) r rw0
|
||||
| check == CheckNone = (newEnv,rw0)
|
||||
| otherwise = (newEnv,rwFin)
|
||||
|
||||
where
|
||||
newEnv = NamingEnv newMap
|
||||
(rwFin,newMap) = Map.mapAccumWithKey doNS rw0 lenv
|
||||
doNS rw ns = Map.mapAccumWithKey (step ns) rw
|
||||
|
||||
step ns acc k xs = (acc', [head xs])
|
||||
where
|
||||
acc' = acc
|
||||
{ rwWarnings =
|
||||
if check == CheckAll
|
||||
then case Map.lookup k (namespaceMap ns r) of
|
||||
Just os | [x] <- xs
|
||||
, let os' = filter (/=x) os
|
||||
, not (null os') ->
|
||||
SymbolShadowed k x os' : rwWarnings acc
|
||||
_ -> rwWarnings acc
|
||||
|
||||
else rwWarnings acc
|
||||
, rwErrors = rwErrors acc Seq.>< containsOverlap xs
|
||||
}
|
||||
|
||||
-- | Check the RHS of a single name rewrite for conflicting sources.
|
||||
containsOverlap :: [Name] -> Seq.Seq RenamerError
|
||||
containsOverlap [_] = Seq.empty
|
||||
containsOverlap [] = panic "Renamer" ["Invalid naming environment"]
|
||||
containsOverlap ns = Seq.singleton (OverlappingSyms ns)
|
||||
|
||||
|
||||
recordUse :: Name -> RenameM ()
|
||||
recordUse x = RenameM $ sets_ $ \rw ->
|
||||
rw { rwNameUseCount = Map.insertWith (+) x 1 (rwNameUseCount rw) }
|
||||
{- NOTE: we don't distinguish between bindings and uses here, because
|
||||
the situation is complicated by the pattern signatures where the first
|
||||
"use" site is actually the bindin site. Instead we just count them all, and
|
||||
something is considered unused if it is used only once (i.e, just the
|
||||
binding site) -}
|
||||
|
||||
-- | Mark something as a dependenicy. This is similar but different from
|
||||
-- `recordUse`, in particular:
|
||||
-- * We only recurd use sites, not bindings
|
||||
-- * We record all namespaces, not just types
|
||||
-- * We only keep track of actual uses mentioned in the code.
|
||||
-- Otoh, `recordUse` also considers exported entities to be used.
|
||||
-- * If we depend on a name in a nested submodule, we also add a
|
||||
-- dependency on the submodule
|
||||
addDep :: Name -> RenameM ()
|
||||
addDep x =
|
||||
do cur <- getCurMod
|
||||
deps <- case nameInfo x of
|
||||
Declared m _ | cur `containsModule` m ->
|
||||
do mb <- nestedModuleOrig m
|
||||
pure case mb of
|
||||
Just y -> Set.fromList [x,y]
|
||||
Nothing -> Set.singleton x
|
||||
_ -> pure (Set.singleton x)
|
||||
RenameM $
|
||||
sets_ \rw -> rw { rwCurrentDeps = Set.union deps (rwCurrentDeps rw) }
|
||||
|
||||
|
||||
warnUnused :: ModPath -> NamingEnv -> RW -> [RenamerWarning]
|
||||
warnUnused m0 env rw =
|
||||
map warn
|
||||
$ Map.keys
|
||||
$ Map.filterWithKey keep
|
||||
$ rwNameUseCount rw
|
||||
where
|
||||
warn x = UnusedName x
|
||||
keep nm count = count == 1 && isLocal nm
|
||||
oldNames = Map.findWithDefault Set.empty NSType (visibleNames env)
|
||||
isLocal nm = case nameInfo nm of
|
||||
Declared m sys -> sys == UserName &&
|
||||
m == m0 && nm `Set.notMember` oldNames
|
||||
Parameter -> True
|
||||
|
||||
-- | Get the exported declarations in a module
|
||||
lookupImport :: Import -> RenameM IfaceDecls
|
||||
lookupImport imp = RenameM $
|
||||
do getIf <- roIfaces <$> ask
|
||||
let ifs = ifPublic (getIf (iModule imp))
|
||||
sets_ \s -> s { rwExternalDeps = ifs <> rwExternalDeps s }
|
||||
pure ifs
|
||||
|
||||
|
@ -43,7 +43,7 @@ import Cryptol.Utils.RecordMap(RecordMap)
|
||||
import Paths_cryptol
|
||||
}
|
||||
|
||||
{- state 196 contains 1 shift/reduce conflicts.
|
||||
{- state 202 contains 1 shift/reduce conflicts.
|
||||
`_` identifier conflicts with `_` in record update.
|
||||
We have `_` as an identifier for the cases where we parse types as
|
||||
expressions, for example `[ 12 .. _ ]`.
|
||||
@ -77,6 +77,7 @@ import Paths_cryptol
|
||||
'type' { Located $$ (Token (KW KW_type ) _)}
|
||||
'newtype' { Located $$ (Token (KW KW_newtype) _)}
|
||||
'module' { Located $$ (Token (KW KW_module ) _)}
|
||||
'submodule' { Located $$ (Token (KW KW_submodule ) _)}
|
||||
'where' { Located $$ (Token (KW KW_where ) _)}
|
||||
'let' { Located $$ (Token (KW KW_let ) _)}
|
||||
'if' { Located $$ (Token (KW KW_if ) _)}
|
||||
@ -158,27 +159,27 @@ import Paths_cryptol
|
||||
%%
|
||||
|
||||
|
||||
vmodule :: { Module PName }
|
||||
: 'module' modName 'where' 'v{' vmod_body 'v}' { mkModule $2 $5 }
|
||||
| 'module' modName '=' modName 'where' 'v{' vmod_body 'v}'
|
||||
{ mkModuleInstance $2 $4 $7 }
|
||||
| 'v{' vmod_body 'v}' { mkAnonymousModule $2 }
|
||||
vmodule :: { Module PName }
|
||||
: 'module' module_def { $2 }
|
||||
| 'v{' vmod_body 'v}' { mkAnonymousModule $2 }
|
||||
|
||||
vmod_body :: { ([Located Import], [TopDecl PName]) }
|
||||
: vimports 'v;' vtop_decls { (reverse $1, reverse $3) }
|
||||
| vimports ';' vtop_decls { (reverse $1, reverse $3) }
|
||||
| vimports { (reverse $1, []) }
|
||||
| vtop_decls { ([], reverse $1) }
|
||||
| {- empty -} { ([], []) }
|
||||
|
||||
vimports :: { [Located Import] }
|
||||
: vimports 'v;' import { $3 : $1 }
|
||||
| vimports ';' import { $3 : $1 }
|
||||
| import { [$1] }
|
||||
module_def :: { Module PName }
|
||||
|
||||
: modName 'where'
|
||||
'v{' vmod_body 'v}' { mkModule $1 $4 }
|
||||
|
||||
| modName '=' modName 'where'
|
||||
'v{' vmod_body 'v}' { mkModuleInstance $1 $3 $6 }
|
||||
|
||||
vmod_body :: { [TopDecl PName] }
|
||||
: vtop_decls { reverse $1 }
|
||||
| {- empty -} { [] }
|
||||
|
||||
|
||||
-- XXX replace rComb with uses of at
|
||||
import :: { Located Import }
|
||||
: 'import' modName mbAs mbImportSpec
|
||||
import :: { Located (ImportG (ImpName PName)) }
|
||||
: 'import' impName mbAs mbImportSpec
|
||||
{ Located { srcRange = rComb $1
|
||||
$ fromMaybe (srcRange $2)
|
||||
$ msum [ fmap srcRange $4
|
||||
@ -191,6 +192,11 @@ import :: { Located Import }
|
||||
}
|
||||
} }
|
||||
|
||||
impName :: { Located (ImpName PName) }
|
||||
: 'submodule' qname { ImpNested `fmap` $2 }
|
||||
| modName { ImpTop `fmap` $1 }
|
||||
|
||||
|
||||
mbAs :: { Maybe (Located ModName) }
|
||||
: 'as' modName { Just $2 }
|
||||
| {- empty -} { Nothing }
|
||||
@ -242,6 +248,9 @@ vtop_decl :: { [TopDecl PName] }
|
||||
| prim_bind { $1 }
|
||||
| private_decls { $1 }
|
||||
| parameter_decls { $1 }
|
||||
| mbDoc 'submodule'
|
||||
module_def {% ((:[]) . exportModule $1) `fmap` mkNested $3 }
|
||||
| import { [DImport $1] }
|
||||
|
||||
top_decl :: { [TopDecl PName] }
|
||||
: decl { [Decl (TopLevel {tlExport = Public, tlValue = $1 })] }
|
||||
@ -303,6 +312,7 @@ decl :: { Decl PName }
|
||||
, bInfix = True
|
||||
, bFixity = Nothing
|
||||
, bDoc = Nothing
|
||||
, bExport = Public
|
||||
} }
|
||||
|
||||
| 'type' name '=' type {% at ($1,$4) `fmap` mkTySyn $2 [] $4 }
|
||||
|
@ -37,7 +37,10 @@ module Cryptol.Parser.AST
|
||||
, psFixity
|
||||
|
||||
-- * Declarations
|
||||
, Module(..)
|
||||
, Module
|
||||
, ModuleG(..)
|
||||
, mImports
|
||||
, mSubmoduleImports
|
||||
, Program(..)
|
||||
, TopDecl(..)
|
||||
, Decl(..)
|
||||
@ -50,11 +53,12 @@ module Cryptol.Parser.AST
|
||||
, Pragma(..)
|
||||
, ExportType(..)
|
||||
, TopLevel(..)
|
||||
, Import(..), ImportSpec(..)
|
||||
, Import, ImportG(..), ImportSpec(..), ImpName(..)
|
||||
, Newtype(..)
|
||||
, PrimType(..)
|
||||
, ParameterType(..)
|
||||
, ParameterFun(..)
|
||||
, NestedModule(..)
|
||||
|
||||
-- * Interactive
|
||||
, ReplInput(..)
|
||||
@ -119,14 +123,38 @@ newtype Program name = Program [TopDecl name]
|
||||
deriving (Show)
|
||||
|
||||
-- | A parsed module.
|
||||
data Module name = Module
|
||||
{ mName :: Located ModName -- ^ Name of the module
|
||||
data ModuleG mname name = Module
|
||||
{ mName :: Located mname -- ^ Name of the module
|
||||
, mInstance :: !(Maybe (Located ModName)) -- ^ Functor to instantiate
|
||||
-- (if this is a functor instnaces)
|
||||
, mImports :: [Located Import] -- ^ Imports for the module
|
||||
-- , mImports :: [Located Import] -- ^ Imports for the module
|
||||
, mDecls :: [TopDecl name] -- ^ Declartions for the module
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
mImports :: ModuleG mname name -> [ Located Import ]
|
||||
mImports m =
|
||||
[ li { thing = i { iModule = n } }
|
||||
| DImport li <- mDecls m
|
||||
, let i = thing li
|
||||
, ImpTop n <- [iModule i]
|
||||
]
|
||||
|
||||
mSubmoduleImports :: ModuleG mname name -> [ Located (ImportG name) ]
|
||||
mSubmoduleImports m =
|
||||
[ li { thing = i { iModule = n } }
|
||||
| DImport li <- mDecls m
|
||||
, let i = thing li
|
||||
, ImpNested n <- [iModule i]
|
||||
]
|
||||
|
||||
|
||||
|
||||
type Module = ModuleG ModName
|
||||
|
||||
|
||||
newtype NestedModule name = NestedModule (ModuleG name name)
|
||||
deriving (Show,Generic,NFData)
|
||||
|
||||
|
||||
modRange :: Module name -> Range
|
||||
modRange m = rCombs $ catMaybes
|
||||
@ -146,12 +174,21 @@ data TopDecl name =
|
||||
| DParameterConstraint [Located (Prop name)]
|
||||
-- ^ @parameter type constraint (fin T)@
|
||||
| DParameterFun (ParameterFun name) -- ^ @parameter someVal : [256]@
|
||||
| DModule (TopLevel (NestedModule name)) -- ^ Nested module
|
||||
| DImport (Located (ImportG (ImpName name))) -- ^ An import declaration
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
data ImpName name =
|
||||
ImpTop ModName
|
||||
| ImpNested name
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
data Decl name = DSignature [Located name] (Schema name)
|
||||
| DFixity !Fixity [Located name]
|
||||
| DPragma [Located name] Pragma
|
||||
| DBind (Bind name)
|
||||
| DRec [Bind name]
|
||||
-- ^ A group of recursive bindings, introduced by the renamer.
|
||||
| DPatBind (Pattern name) (Expr name)
|
||||
| DType (TySyn name)
|
||||
| DProp (PropSyn name)
|
||||
@ -178,16 +215,15 @@ data ParameterFun name = ParameterFun
|
||||
|
||||
|
||||
-- | An import declaration.
|
||||
data Import = Import { iModule :: !ModName
|
||||
, iAs :: Maybe ModName
|
||||
, iSpec :: Maybe ImportSpec
|
||||
} deriving (Eq, Show, Generic, NFData)
|
||||
data ImportG mname = Import
|
||||
{ iModule :: !mname
|
||||
, iAs :: Maybe ModName
|
||||
, iSpec :: Maybe ImportSpec
|
||||
} deriving (Eq, Show, Generic, NFData)
|
||||
|
||||
type Import = ImportG ModName
|
||||
|
||||
-- | The list of names following an import.
|
||||
--
|
||||
-- INVARIANT: All of the 'Name' entries in the list are expected to be
|
||||
-- unqualified names; the 'QName' or 'NewName' constructors should not be
|
||||
-- present.
|
||||
data ImportSpec = Hiding [Ident]
|
||||
| Only [Ident]
|
||||
deriving (Eq, Show, Generic, NFData)
|
||||
@ -234,6 +270,7 @@ data Bind name = Bind
|
||||
, bPragmas :: [Pragma] -- ^ Optional pragmas
|
||||
, bMono :: Bool -- ^ Is this a monomorphic binding
|
||||
, bDoc :: Maybe Text -- ^ Optional doc string
|
||||
, bExport :: !ExportType
|
||||
} deriving (Eq, Generic, NFData, Functor, Show)
|
||||
|
||||
type LBindDef = Located (BindDef PName)
|
||||
@ -482,14 +519,17 @@ instance HasLoc a => HasLoc (TopLevel a) where
|
||||
getLoc = getLoc . tlValue
|
||||
|
||||
instance HasLoc (TopDecl name) where
|
||||
getLoc td = case td of
|
||||
Decl tld -> getLoc tld
|
||||
DPrimType pt -> getLoc pt
|
||||
TDNewtype n -> getLoc n
|
||||
Include lfp -> getLoc lfp
|
||||
DParameterType d -> getLoc d
|
||||
DParameterFun d -> getLoc d
|
||||
DParameterConstraint d -> getLoc d
|
||||
getLoc td =
|
||||
case td of
|
||||
Decl tld -> getLoc tld
|
||||
DPrimType pt -> getLoc pt
|
||||
TDNewtype n -> getLoc n
|
||||
Include lfp -> getLoc lfp
|
||||
DParameterType d -> getLoc d
|
||||
DParameterFun d -> getLoc d
|
||||
DParameterConstraint d -> getLoc d
|
||||
DModule d -> getLoc d
|
||||
DImport d -> getLoc d
|
||||
|
||||
instance HasLoc (PrimType name) where
|
||||
getLoc pt = Just (rComb (srcRange (primTName pt)) (srcRange (primTKind pt)))
|
||||
@ -500,7 +540,7 @@ instance HasLoc (ParameterType name) where
|
||||
instance HasLoc (ParameterFun name) where
|
||||
getLoc a = getLoc (pfName a)
|
||||
|
||||
instance HasLoc (Module name) where
|
||||
instance HasLoc (ModuleG mname name) where
|
||||
getLoc m
|
||||
| null locs = Nothing
|
||||
| otherwise = Just (rCombs locs)
|
||||
@ -510,6 +550,9 @@ instance HasLoc (Module name) where
|
||||
, getLoc (mDecls m)
|
||||
]
|
||||
|
||||
instance HasLoc (NestedModule name) where
|
||||
getLoc (NestedModule m) = getLoc m
|
||||
|
||||
instance HasLoc (Newtype name) where
|
||||
getLoc n
|
||||
| null locs = Nothing
|
||||
@ -537,10 +580,24 @@ ppNamed s x = ppL (name x) <+> text s <+> pp (value x)
|
||||
ppNamed' :: PP a => String -> (Ident, (Range, a)) -> Doc
|
||||
ppNamed' s (i,(_,v)) = pp i <+> text s <+> pp v
|
||||
|
||||
instance (Show name, PPName name) => PP (Module name) where
|
||||
ppPrec _ m = text "module" <+> ppL (mName m) <+> text "where"
|
||||
$$ vcat (map ppL (mImports m))
|
||||
$$ vcat (map pp (mDecls m))
|
||||
|
||||
|
||||
instance (Show name, PPName mname, PPName name) => PP (ModuleG mname name) where
|
||||
ppPrec _ = ppModule 0
|
||||
|
||||
ppModule :: (Show name, PPName mname, PPName name) =>
|
||||
Int -> ModuleG mname name -> Doc
|
||||
ppModule n m =
|
||||
text "module" <+> ppL (mName m) <+> text "where" $$ nest n body
|
||||
where
|
||||
body = vcat (map ppL (mImports m))
|
||||
$$ vcat (map pp (mDecls m))
|
||||
|
||||
|
||||
|
||||
instance (Show name, PPName name) => PP (NestedModule name) where
|
||||
ppPrec _ (NestedModule m) = ppModule 2 m
|
||||
|
||||
|
||||
instance (Show name, PPName name) => PP (Program name) where
|
||||
ppPrec _ (Program ds) = vcat (map pp ds)
|
||||
@ -556,10 +613,12 @@ instance (Show name, PPName name) => PP (TopDecl name) where
|
||||
DParameterType d -> pp d
|
||||
DParameterConstraint d ->
|
||||
"parameter" <+> "type" <+> "constraint" <+> prop
|
||||
where prop = case map pp d of
|
||||
where prop = case map (pp . thing) d of
|
||||
[x] -> x
|
||||
[] -> "()"
|
||||
xs -> parens (hsep (punctuate comma xs))
|
||||
DModule d -> pp d
|
||||
DImport i -> pp (thing i)
|
||||
|
||||
instance (Show name, PPName name) => PP (PrimType name) where
|
||||
ppPrec _ pt =
|
||||
@ -580,6 +639,7 @@ instance (Show name, PPName name) => PP (Decl name) where
|
||||
DSignature xs s -> commaSep (map ppL xs) <+> text ":" <+> pp s
|
||||
DPatBind p e -> pp p <+> text "=" <+> pp e
|
||||
DBind b -> ppPrec n b
|
||||
DRec bs -> "recursive" $$ nest 2 (vcat (map (ppPrec n) bs))
|
||||
DFixity f ns -> ppFixity f ns
|
||||
DPragma xs p -> ppPragma xs p
|
||||
DType ts -> ppPrec n ts
|
||||
@ -596,13 +656,19 @@ instance PPName name => PP (Newtype name) where
|
||||
[ text "newtype", ppL (nName nt), hsep (map pp (nParams nt)), char '='
|
||||
, braces (commaSep (map (ppNamed' ":") (displayFields (nBody nt)))) ]
|
||||
|
||||
instance PP Import where
|
||||
instance PP mname => PP (ImportG mname) where
|
||||
ppPrec _ d = text "import" <+> sep [ pp (iModule d), mbAs, mbSpec ]
|
||||
where
|
||||
mbAs = maybe empty (\ name -> text "as" <+> pp name ) (iAs d)
|
||||
|
||||
mbSpec = maybe empty pp (iSpec d)
|
||||
|
||||
instance PP name => PP (ImpName name) where
|
||||
ppPrec _ nm =
|
||||
case nm of
|
||||
ImpTop x -> pp x
|
||||
ImpNested x -> "submodule" <+> pp x
|
||||
|
||||
instance PP ImportSpec where
|
||||
ppPrec _ s = case s of
|
||||
Hiding names -> text "hiding" <+> parens (commaSep (map pp names))
|
||||
@ -915,13 +981,15 @@ instance (NoPos a, NoPos b) => NoPos (a,b) where
|
||||
instance NoPos (Program name) where
|
||||
noPos (Program x) = Program (noPos x)
|
||||
|
||||
instance NoPos (Module name) where
|
||||
instance NoPos (ModuleG mname name) where
|
||||
noPos m = Module { mName = mName m
|
||||
, mInstance = mInstance m
|
||||
, mImports = noPos (mImports m)
|
||||
, mDecls = noPos (mDecls m)
|
||||
}
|
||||
|
||||
instance NoPos (NestedModule name) where
|
||||
noPos (NestedModule m) = NestedModule (noPos m)
|
||||
|
||||
instance NoPos (TopDecl name) where
|
||||
noPos decl =
|
||||
case decl of
|
||||
@ -932,6 +1000,9 @@ instance NoPos (TopDecl name) where
|
||||
DParameterFun d -> DParameterFun (noPos d)
|
||||
DParameterType d -> DParameterType (noPos d)
|
||||
DParameterConstraint d -> DParameterConstraint (noPos d)
|
||||
DModule d -> DModule (noPos d)
|
||||
DImport d -> DImport (noPos d)
|
||||
|
||||
|
||||
instance NoPos (PrimType name) where
|
||||
noPos x = x
|
||||
@ -953,6 +1024,7 @@ instance NoPos (Decl name) where
|
||||
DPatBind x y -> DPatBind (noPos x) (noPos y)
|
||||
DFixity f ns -> DFixity f (noPos ns)
|
||||
DBind x -> DBind (noPos x)
|
||||
DRec bs -> DRec (map noPos bs)
|
||||
DType x -> DType (noPos x)
|
||||
DProp x -> DProp (noPos x)
|
||||
DLocated x _ -> noPos x
|
||||
@ -973,6 +1045,7 @@ instance NoPos (Bind name) where
|
||||
, bPragmas = noPos (bPragmas x)
|
||||
, bMono = bMono x
|
||||
, bDoc = bDoc x
|
||||
, bExport = bExport x
|
||||
}
|
||||
|
||||
instance NoPos Pragma where
|
||||
|
@ -100,6 +100,7 @@ $white+ { emit $ White Space }
|
||||
"private" { emit $ KW KW_private }
|
||||
"include" { emit $ KW KW_include }
|
||||
"module" { emit $ KW KW_module }
|
||||
"submodule" { emit $ KW KW_submodule }
|
||||
"newtype" { emit $ KW KW_newtype }
|
||||
"pragma" { emit $ KW KW_pragma }
|
||||
"property" { emit $ KW KW_property }
|
||||
|
@ -487,6 +487,7 @@ data TokenKW = KW_else
|
||||
| KW_max
|
||||
| KW_min
|
||||
| KW_module
|
||||
| KW_submodule
|
||||
| KW_newtype
|
||||
| KW_pragma
|
||||
| KW_property
|
||||
|
@ -9,7 +9,19 @@
|
||||
-- This module defines the scoping rules for value- and type-level
|
||||
-- names in Cryptol.
|
||||
|
||||
module Cryptol.Parser.Names where
|
||||
module Cryptol.Parser.Names
|
||||
( tnamesNT
|
||||
, tnamesT
|
||||
, tnamesC
|
||||
|
||||
, namesD
|
||||
, tnamesD
|
||||
, namesB
|
||||
, namesP
|
||||
|
||||
, boundNames
|
||||
, boundNamesSet
|
||||
) where
|
||||
|
||||
import Cryptol.Parser.AST
|
||||
import Cryptol.Utils.RecordMap
|
||||
@ -17,7 +29,6 @@ import Cryptol.Utils.RecordMap
|
||||
import Data.Set (Set)
|
||||
import qualified Data.Set as Set
|
||||
|
||||
|
||||
-- | The names defined by a newtype.
|
||||
tnamesNT :: Newtype name -> ([Located name], ())
|
||||
tnamesNT x = ([ nName x ], ())
|
||||
@ -34,6 +45,8 @@ namesD :: Ord name => Decl name -> ([Located name], Set name)
|
||||
namesD decl =
|
||||
case decl of
|
||||
DBind b -> namesB b
|
||||
DRec bs -> let (xs,ys) = unzip (map namesB bs)
|
||||
in (concat xs, Set.unions ys) -- remove binders?
|
||||
DPatBind p e -> (namesP p, namesE e)
|
||||
DSignature {} -> ([],Set.empty)
|
||||
DFixity{} -> ([],Set.empty)
|
||||
@ -42,25 +55,10 @@ namesD decl =
|
||||
DProp {} -> ([],Set.empty)
|
||||
DLocated d _ -> namesD d
|
||||
|
||||
-- | The names defined and used by a single declarations in such a way
|
||||
-- that they cannot be duplicated in a file. For example, it is fine
|
||||
-- to use @x@ on the RHS of two bindings, but not on the LHS of two
|
||||
-- type signatures.
|
||||
allNamesD :: Ord name => Decl name -> [Located name]
|
||||
allNamesD decl =
|
||||
case decl of
|
||||
DBind b -> fst (namesB b)
|
||||
DPatBind p _ -> namesP p
|
||||
DSignature ns _ -> ns
|
||||
DFixity _ ns -> ns
|
||||
DPragma ns _ -> ns
|
||||
DType ts -> [tsName ts]
|
||||
DProp ps -> [psName ps]
|
||||
DLocated d _ -> allNamesD d
|
||||
|
||||
-- | The names defined and used by a single binding.
|
||||
namesB :: Ord name => Bind name -> ([Located name], Set name)
|
||||
namesB b = ([bName b], boundLNames (namesPs (bParams b)) (namesDef (thing (bDef b))))
|
||||
namesB b =
|
||||
([bName b], boundLNames (namesPs (bParams b)) (namesDef (thing (bDef b))))
|
||||
|
||||
|
||||
namesDef :: Ord name => BindDef name -> Set name
|
||||
@ -164,6 +162,7 @@ tnamesD decl =
|
||||
DFixity {} -> ([], Set.empty)
|
||||
DPragma {} -> ([], Set.empty)
|
||||
DBind b -> ([], tnamesB b)
|
||||
DRec bs -> ([], Set.unions (map tnamesB bs))
|
||||
DPatBind _ e -> ([], tnamesE e)
|
||||
DLocated d _ -> tnamesD d
|
||||
DType (TySyn n _ ps t)
|
||||
|
@ -160,7 +160,7 @@ collectErrors f ts = do
|
||||
return rs
|
||||
|
||||
-- | Remove includes from a module.
|
||||
noIncludeModule :: Module PName -> NoIncM (Module PName)
|
||||
noIncludeModule :: ModuleG mname PName -> NoIncM (ModuleG mname PName)
|
||||
noIncludeModule m = update `fmap` collectErrors noIncTopDecl (mDecls m)
|
||||
where
|
||||
update tds = m { mDecls = concat tds }
|
||||
@ -174,13 +174,19 @@ noIncludeProgram (Program tds) =
|
||||
-- reference.
|
||||
noIncTopDecl :: TopDecl PName -> NoIncM [TopDecl PName]
|
||||
noIncTopDecl td = case td of
|
||||
Decl _ -> return [td]
|
||||
Decl _ -> pure [td]
|
||||
DPrimType {} -> pure [td]
|
||||
TDNewtype _-> return [td]
|
||||
DParameterType {} -> return [td]
|
||||
DParameterConstraint {} -> return [td]
|
||||
DParameterFun {} -> return [td]
|
||||
TDNewtype _-> pure [td]
|
||||
DParameterType {} -> pure [td]
|
||||
DParameterConstraint {} -> pure [td]
|
||||
DParameterFun {} -> pure [td]
|
||||
Include lf -> resolveInclude lf
|
||||
DModule tl ->
|
||||
case tlValue tl of
|
||||
NestedModule m ->
|
||||
do m1 <- noIncludeModule m
|
||||
pure [ DModule tl { tlValue = NestedModule m1 } ]
|
||||
DImport {} -> pure [td]
|
||||
|
||||
-- | Resolve the file referenced by a include into a list of top-level
|
||||
-- declarations.
|
||||
|
@ -44,18 +44,23 @@ instance RemovePatterns (Program PName) where
|
||||
instance RemovePatterns (Expr PName) where
|
||||
removePatterns e = runNoPatM (noPatE e)
|
||||
|
||||
instance RemovePatterns (Module PName) where
|
||||
instance RemovePatterns (ModuleG mname PName) where
|
||||
removePatterns m = runNoPatM (noPatModule m)
|
||||
|
||||
instance RemovePatterns [Decl PName] where
|
||||
removePatterns ds = runNoPatM (noPatDs ds)
|
||||
|
||||
instance RemovePatterns (NestedModule PName) where
|
||||
removePatterns (NestedModule m) = (NestedModule m1,errs)
|
||||
where (m1,errs) = removePatterns m
|
||||
|
||||
simpleBind :: Located PName -> Expr PName -> Bind PName
|
||||
simpleBind x e = Bind { bName = x, bParams = []
|
||||
, bDef = at e (Located emptyRange (DExpr e))
|
||||
, bSignature = Nothing, bPragmas = []
|
||||
, bMono = True, bInfix = False, bFixity = Nothing
|
||||
, bDoc = Nothing
|
||||
, bExport = Public
|
||||
}
|
||||
|
||||
sel :: Pattern PName -> PName -> Selector -> Bind PName
|
||||
@ -226,6 +231,7 @@ noMatchD decl =
|
||||
|
||||
DBind b -> do b1 <- noMatchB b
|
||||
return [DBind b1]
|
||||
DRec {} -> panic "noMatchD" [ "DRec" ]
|
||||
|
||||
DPatBind p e -> do (p',bs) <- noPat p
|
||||
let (x,ts) = splitSimpleP p'
|
||||
@ -240,6 +246,7 @@ noMatchD decl =
|
||||
, bInfix = False
|
||||
, bFixity = Nothing
|
||||
, bDoc = Nothing
|
||||
, bExport = Public
|
||||
} : map DBind bs
|
||||
DType {} -> return [decl]
|
||||
DProp {} -> return [decl]
|
||||
@ -323,7 +330,7 @@ noPatTopDs tds =
|
||||
noPatProg :: Program PName -> NoPatM (Program PName)
|
||||
noPatProg (Program topDs) = Program <$> noPatTopDs topDs
|
||||
|
||||
noPatModule :: Module PName -> NoPatM (Module PName)
|
||||
noPatModule :: ModuleG mname PName -> NoPatM (ModuleG mname PName)
|
||||
noPatModule m =
|
||||
do ds1 <- noPatTopDs (mDecls m)
|
||||
return m { mDecls = ds1 }
|
||||
@ -385,6 +392,13 @@ annotTopDs tds =
|
||||
TDNewtype {} -> (d :) <$> annotTopDs ds
|
||||
Include {} -> (d :) <$> annotTopDs ds
|
||||
|
||||
DModule m ->
|
||||
case removePatterns (tlValue m) of
|
||||
(m1,errs) -> do lift (mapM_ recordError errs)
|
||||
(DModule m { tlValue = m1 } :) <$> annotTopDs ds
|
||||
|
||||
DImport {} -> (d :) <$> annotTopDs ds
|
||||
|
||||
[] -> return []
|
||||
|
||||
|
||||
@ -403,6 +417,7 @@ annotD :: Decl PName -> ExceptionT () (StateT AnnotMap NoPatM) (Decl PName)
|
||||
annotD decl =
|
||||
case decl of
|
||||
DBind b -> DBind <$> lift (annotB b)
|
||||
DRec {} -> panic "annotD" [ "DRec" ]
|
||||
DSignature {} -> raise ()
|
||||
DFixity{} -> raise ()
|
||||
DPragma {} -> raise ()
|
||||
@ -524,6 +539,7 @@ toDocs TopLevel { .. }
|
||||
DSignature ns _ -> [ (thing n, [txt]) | n <- ns ]
|
||||
DFixity _ ns -> [ (thing n, [txt]) | n <- ns ]
|
||||
DBind b -> [ (thing (bName b), [txt]) ]
|
||||
DRec {} -> panic "toDocs" [ "DRec" ]
|
||||
DLocated d _ -> go txt d
|
||||
DPatBind p _ -> [ (thing n, [txt]) | n <- namesP p ]
|
||||
|
||||
|
@ -38,7 +38,7 @@ import Cryptol.Parser.Lexer
|
||||
import Cryptol.Parser.LexerUtils(SelectorType(..))
|
||||
import Cryptol.Parser.Position
|
||||
import Cryptol.Parser.Utils (translateExprToNumT,widthIdent)
|
||||
import Cryptol.Utils.Ident(packModName)
|
||||
import Cryptol.Utils.Ident(packModName,packIdent,modNameChunks)
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Panic
|
||||
import Cryptol.Utils.RecordMap
|
||||
@ -433,6 +433,11 @@ exportNewtype e d n = TDNewtype TopLevel { tlExport = e
|
||||
, tlDoc = d
|
||||
, tlValue = n }
|
||||
|
||||
exportModule :: Maybe (Located Text) -> NestedModule PName -> TopDecl PName
|
||||
exportModule mbDoc m = DModule TopLevel { tlExport = Public
|
||||
, tlDoc = mbDoc
|
||||
, tlValue = m }
|
||||
|
||||
mkParFun :: Maybe (Located Text) ->
|
||||
Located PName ->
|
||||
Schema PName ->
|
||||
@ -464,7 +469,9 @@ changeExport e = map change
|
||||
change (Decl d) = Decl d { tlExport = e }
|
||||
change (DPrimType t) = DPrimType t { tlExport = e }
|
||||
change (TDNewtype n) = TDNewtype n { tlExport = e }
|
||||
change (DModule m) = DModule m { tlExport = e }
|
||||
change td@Include{} = td
|
||||
change td@DImport{} = td
|
||||
change (DParameterType {}) = panic "changeExport" ["private type parameter?"]
|
||||
change (DParameterFun {}) = panic "changeExport" ["private value parameter?"]
|
||||
change (DParameterConstraint {}) =
|
||||
@ -534,6 +541,7 @@ mkProperty f ps e = DBind Bind { bName = f
|
||||
, bInfix = False
|
||||
, bFixity = Nothing
|
||||
, bDoc = Nothing
|
||||
, bExport = Public
|
||||
}
|
||||
|
||||
-- NOTE: The lists of patterns are reversed!
|
||||
@ -549,6 +557,7 @@ mkIndexedDecl f (ps, ixs) e =
|
||||
, bInfix = False
|
||||
, bFixity = Nothing
|
||||
, bDoc = Nothing
|
||||
, bExport = Public
|
||||
}
|
||||
where
|
||||
rhs :: Expr PName
|
||||
@ -588,6 +597,7 @@ mkPrimDecl mbDoc ln sig =
|
||||
, bInfix = isInfixIdent (getIdent (thing ln))
|
||||
, bFixity = Nothing
|
||||
, bDoc = Nothing
|
||||
, bExport = Public
|
||||
}
|
||||
, exportDecl Nothing Public
|
||||
$ DSignature [ln] sig
|
||||
@ -737,18 +747,24 @@ mkProp ty =
|
||||
err = errorMessage r ["Invalid constraint"]
|
||||
|
||||
-- | Make an ordinary module
|
||||
mkModule :: Located ModName ->
|
||||
([Located Import], [TopDecl PName]) ->
|
||||
Module PName
|
||||
mkModule nm (is,ds) = Module { mName = nm
|
||||
, mInstance = Nothing
|
||||
, mImports = is
|
||||
, mDecls = ds
|
||||
}
|
||||
mkModule :: Located ModName -> [TopDecl PName] -> Module PName
|
||||
mkModule nm ds = Module { mName = nm
|
||||
, mInstance = Nothing
|
||||
, mDecls = ds
|
||||
}
|
||||
|
||||
mkNested :: Module PName -> ParseM (NestedModule PName)
|
||||
mkNested m =
|
||||
case modNameChunks (thing nm) of
|
||||
[c] -> pure (NestedModule m { mName = nm { thing = mkUnqual (packIdent c)}})
|
||||
_ -> errorMessage r
|
||||
["Nested modules names should be a simple identifier."]
|
||||
where
|
||||
nm = mName m
|
||||
r = srcRange nm
|
||||
|
||||
-- | Make an unnamed module---gets the name @Main@.
|
||||
mkAnonymousModule :: ([Located Import], [TopDecl PName]) ->
|
||||
Module PName
|
||||
mkAnonymousModule :: [TopDecl PName] -> Module PName
|
||||
mkAnonymousModule = mkModule Located { srcRange = emptyRange
|
||||
, thing = mkModName [T.pack "Main"]
|
||||
}
|
||||
@ -756,12 +772,11 @@ mkAnonymousModule = mkModule Located { srcRange = emptyRange
|
||||
-- | Make a module which defines a functor instance.
|
||||
mkModuleInstance :: Located ModName ->
|
||||
Located ModName ->
|
||||
([Located Import], [TopDecl PName]) ->
|
||||
[TopDecl PName] ->
|
||||
Module PName
|
||||
mkModuleInstance nm fun (is,ds) =
|
||||
mkModuleInstance nm fun ds =
|
||||
Module { mName = nm
|
||||
, mInstance = Just fun
|
||||
, mImports = is
|
||||
, mDecls = ds
|
||||
}
|
||||
|
||||
|
@ -10,6 +10,9 @@
|
||||
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
{-# LANGUAGE DeriveFoldable #-}
|
||||
{-# LANGUAGE DeriveTraversable #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
module Cryptol.Parser.Position where
|
||||
|
||||
@ -22,7 +25,8 @@ import Control.DeepSeq
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
data Located a = Located { srcRange :: !Range, thing :: !a }
|
||||
deriving (Eq, Ord, Show, Generic, NFData)
|
||||
deriving (Eq, Ord, Show, Generic, NFData
|
||||
, Functor, Foldable, Traversable )
|
||||
|
||||
|
||||
data Position = Position { line :: !Int, col :: !Int }
|
||||
@ -65,8 +69,6 @@ rCombMaybe (Just x) (Just y) = Just (rComb x y)
|
||||
rCombs :: [Range] -> Range
|
||||
rCombs = foldl1 rComb
|
||||
|
||||
instance Functor Located where
|
||||
fmap f l = l { thing = f (thing l) }
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
|
@ -1172,6 +1172,7 @@ browseCmd input = do
|
||||
disp = M.mctxNameDisp fe
|
||||
provV = M.mctxValueProvenance fe
|
||||
provT = M.mctxTypeProvenace fe
|
||||
provM = M.mctxModProvenace fe
|
||||
|
||||
|
||||
let f &&& g = \x -> f x && g x
|
||||
@ -1180,20 +1181,43 @@ browseCmd input = do
|
||||
_ -> True
|
||||
inSet s x = x `Set.member` s
|
||||
|
||||
let (visibleTypes,visibleDecls) = M.visibleNames names
|
||||
let visNames = M.visibleNames names
|
||||
visibleTypes = Map.findWithDefault Set.empty M.NSType visNames
|
||||
visibleDecls = Map.findWithDefault Set.empty M.NSValue visNames
|
||||
visibleMods = Map.findWithDefault Set.empty M.NSModule visNames
|
||||
|
||||
restricted = if null mnames then const True else hasAnyModName mnames
|
||||
|
||||
visibleType = isUser &&& restricted &&& inSet visibleTypes
|
||||
visibleDecl = isUser &&& restricted &&& inSet visibleDecls
|
||||
visibleMod = isUser &&& restricted &&& inSet visibleMods
|
||||
|
||||
browseMParams visibleType visibleDecl params disp
|
||||
browseMods visibleMod provM iface disp
|
||||
browseTSyns visibleType provT iface disp
|
||||
browsePrimTys visibleType provT iface disp
|
||||
browseNewtypes visibleType provT iface disp
|
||||
browseVars visibleDecl provV iface disp
|
||||
|
||||
|
||||
browseMods :: (T.Name -> Bool) -> Map T.Name M.DeclProvenance ->
|
||||
M.IfaceDecls -> NameDisp -> REPL ()
|
||||
browseMods isVisible prov M.IfaceDecls { .. } names =
|
||||
ppSection (Map.elems ifModules)
|
||||
Section { secName = "Modules"
|
||||
, secEntryName = M.ifModName
|
||||
, secProvenance = prov
|
||||
, secDisp = names
|
||||
, secPP = ppM
|
||||
, secVisible = isVisible
|
||||
}
|
||||
where
|
||||
ppM m = pp (M.ifModName m)
|
||||
-- XXX: can print a lot more information about the moduels, but
|
||||
-- might be better to do that with a separate command
|
||||
|
||||
|
||||
|
||||
browseMParams :: (M.Name -> Bool) -> (M.Name -> Bool) ->
|
||||
M.IfaceParams -> NameDisp -> REPL ()
|
||||
browseMParams visT visD M.IfaceParams { .. } names =
|
||||
@ -1596,10 +1620,12 @@ handleCtrlC a = do rPutStrLn "Ctrl-C"
|
||||
|
||||
-- Utilities -------------------------------------------------------------------
|
||||
|
||||
-- XXX: browsing nested modules?
|
||||
hasAnyModName :: [M.ModName] -> M.Name -> Bool
|
||||
hasAnyModName mnames n =
|
||||
case M.nameInfo n of
|
||||
M.Declared m _ -> m `elem` mnames
|
||||
M.Declared (M.TopModule m) _ -> m `elem` mnames
|
||||
M.Declared (M.Nested p _) _ -> M.topModuleFor p `elem` mnames
|
||||
M.Parameter -> False
|
||||
|
||||
|
||||
|
@ -492,7 +492,7 @@ validEvalContext a =
|
||||
|
||||
badName nm bs =
|
||||
case M.nameInfo nm of
|
||||
M.Declared m _
|
||||
M.Declared (M.TopModule m) _ -- XXX: can we focus nested modules?
|
||||
| M.isLoadedParamMod m (M.meLoadedModules me) -> Set.insert nm bs
|
||||
_ -> bs
|
||||
|
||||
@ -547,14 +547,14 @@ getFocusedEnv = M.focusedEnv <$> getModuleEnv
|
||||
getExprNames :: REPL [String]
|
||||
getExprNames =
|
||||
do fNames <- M.mctxNames <$> getFocusedEnv
|
||||
return (map (show . pp) (Map.keys (M.neExprs fNames)))
|
||||
return (map (show . pp) (Map.keys (M.namespaceMap M.NSValue fNames)))
|
||||
|
||||
-- | Get visible type signature names.
|
||||
-- This is used for command line completition.
|
||||
getTypeNames :: REPL [String]
|
||||
getTypeNames =
|
||||
do fNames <- M.mctxNames <$> getFocusedEnv
|
||||
return (map (show . pp) (Map.keys (M.neTypes fNames)))
|
||||
return (map (show . pp) (Map.keys (M.namespaceMap M.NSType fNames)))
|
||||
|
||||
-- | Return a list of property names, sorted by position in the file.
|
||||
getPropertyNames :: REPL ([(M.Name,M.IfaceDecl)],NameDisp)
|
||||
@ -595,7 +595,8 @@ uniqify :: M.Name -> REPL M.Name
|
||||
uniqify name =
|
||||
case M.nameInfo name of
|
||||
M.Declared ns s ->
|
||||
M.liftSupply (M.mkDeclared ns s (M.nameIdent name) (M.nameFixity name) (M.nameLoc name))
|
||||
M.liftSupply (M.mkDeclared (M.nameNamespace name)
|
||||
ns s (M.nameIdent name) (M.nameFixity name) (M.nameLoc name))
|
||||
|
||||
M.Parameter ->
|
||||
panic "[REPL] uniqify" ["tried to uniqify a parameter: " ++ pretty name]
|
||||
@ -615,7 +616,8 @@ uniqify name =
|
||||
-- the "<interactive>" namespace.
|
||||
freshName :: I.Ident -> M.NameSource -> REPL M.Name
|
||||
freshName i sys =
|
||||
M.liftSupply (M.mkDeclared I.interactiveName sys i Nothing emptyRange)
|
||||
M.liftSupply (M.mkDeclared I.NSValue mpath sys i Nothing emptyRange)
|
||||
where mpath = M.TopModule I.interactiveName
|
||||
|
||||
|
||||
-- User Environment Interaction ------------------------------------------------
|
||||
|
@ -79,11 +79,11 @@
|
||||
module Cryptol.Transform.MonoValues (rewModule) where
|
||||
|
||||
import Cryptol.ModuleSystem.Name
|
||||
(SupplyT,liftSupply,Supply,mkDeclared,NameSource(..))
|
||||
(SupplyT,liftSupply,Supply,mkDeclared,NameSource(..),ModPath(..))
|
||||
import Cryptol.Parser.Position (emptyRange)
|
||||
import Cryptol.TypeCheck.AST hiding (splitTApp) -- XXX: just use this one
|
||||
import Cryptol.TypeCheck.TypeMap
|
||||
import Cryptol.Utils.Ident (ModName)
|
||||
import Cryptol.Utils.Ident(Namespace(..))
|
||||
import Data.List(sortBy,groupBy)
|
||||
import Data.Either(partitionEithers)
|
||||
import Data.Map (Map)
|
||||
@ -132,7 +132,7 @@ instance TrieMap RewMap' (Name,[Type],Int) where
|
||||
-- | Note that this assumes that this pass will be run only once for each
|
||||
-- module, otherwise we will get name collisions.
|
||||
rewModule :: Supply -> Module -> (Module,Supply)
|
||||
rewModule s m = runM body (mName m) s
|
||||
rewModule s m = runM body (TopModule (mName m)) s
|
||||
where
|
||||
body = do ds <- mapM (rewDeclGroup emptyTM) (mDecls m)
|
||||
return m { mDecls = ds }
|
||||
@ -140,13 +140,13 @@ rewModule s m = runM body (mName m) s
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
type M = ReaderT RO (SupplyT Id)
|
||||
type RO = ModName
|
||||
type RO = ModPath
|
||||
|
||||
-- | Produce a fresh top-level name.
|
||||
newName :: M Name
|
||||
newName =
|
||||
do ns <- ask
|
||||
liftSupply (mkDeclared ns SystemName "$mono" Nothing emptyRange)
|
||||
liftSupply (mkDeclared NSValue ns SystemName "$mono" Nothing emptyRange)
|
||||
|
||||
newTopOrLocalName :: M Name
|
||||
newTopOrLocalName = newName
|
||||
|
@ -242,9 +242,10 @@ destETAbs = go []
|
||||
freshName :: Name -> [Type] -> SpecM Name
|
||||
freshName n _ =
|
||||
case nameInfo n of
|
||||
Declared ns s -> liftSupply (mkDeclared ns s ident fx loc)
|
||||
Parameter -> liftSupply (mkParameter ident loc)
|
||||
Declared m s -> liftSupply (mkDeclared ns m s ident fx loc)
|
||||
Parameter -> liftSupply (mkParameter ns ident loc)
|
||||
where
|
||||
ns = nameNamespace n
|
||||
fx = nameFixity n
|
||||
ident = nameIdent n
|
||||
loc = nameLoc n
|
||||
|
@ -28,11 +28,10 @@ module Cryptol.TypeCheck
|
||||
) where
|
||||
|
||||
import Cryptol.ModuleSystem.Name
|
||||
(liftSupply,mkDeclared,NameSource(..))
|
||||
(liftSupply,mkDeclared,NameSource(..),ModPath(..))
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
import Cryptol.Parser.Position(Range,emptyRange)
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Depends (FromDecl)
|
||||
import Cryptol.TypeCheck.Error
|
||||
import Cryptol.TypeCheck.Monad
|
||||
( runInferM
|
||||
@ -41,16 +40,19 @@ import Cryptol.TypeCheck.Monad
|
||||
, NameSeeds
|
||||
, nameSeeds
|
||||
, lookupVar
|
||||
, newLocalScope, endLocalScope
|
||||
, newModuleScope, addParamType, addParameterConstraints
|
||||
, endModuleInstance
|
||||
)
|
||||
import Cryptol.TypeCheck.Infer (inferModule, inferBinds, inferDs)
|
||||
import Cryptol.TypeCheck.InferTypes(VarType(..), SolverConfig(..))
|
||||
import Cryptol.TypeCheck.Solve(proveModuleTopLevel)
|
||||
import Cryptol.TypeCheck.CheckModuleInstance(checkModuleInstance)
|
||||
import Cryptol.TypeCheck.Monad(withParamType,withParameterConstraints)
|
||||
import Cryptol.TypeCheck.PP(WithNames(..),NameMap)
|
||||
import Cryptol.Utils.Ident (exprModName,packIdent)
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.TypeCheck.Infer (inferModule, inferBinds, checkTopDecls)
|
||||
import Cryptol.TypeCheck.InferTypes(VarType(..), SolverConfig(..))
|
||||
import Cryptol.TypeCheck.Solve(proveModuleTopLevel)
|
||||
import Cryptol.TypeCheck.CheckModuleInstance(checkModuleInstance)
|
||||
-- import Cryptol.TypeCheck.Monad(withParamType,withParameterConstraints)
|
||||
import Cryptol.TypeCheck.PP(WithNames(..),NameMap)
|
||||
import Cryptol.Utils.Ident (exprModName,packIdent,Namespace(..))
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
|
||||
|
||||
|
||||
@ -59,17 +61,20 @@ tcModule m inp = runInferM inp (inferModule m)
|
||||
|
||||
-- | Check a module instantiation, assuming that the functor has already
|
||||
-- been checked.
|
||||
-- XXX: This will change
|
||||
tcModuleInst :: Module {- ^ functor -} ->
|
||||
P.Module Name {- params -} ->
|
||||
P.Module Name {- ^ params -} ->
|
||||
InferInput {- ^ TC settings -} ->
|
||||
IO (InferOutput Module) {- ^ new version of instance -}
|
||||
tcModuleInst func m inp = runInferM inp
|
||||
$ do x <- inferModule m
|
||||
flip (foldr withParamType) (mParamTypes x) $
|
||||
withParameterConstraints (mParamConstraints x) $
|
||||
do y <- checkModuleInstance func x
|
||||
proveModuleTopLevel
|
||||
pure y
|
||||
tcModuleInst func m inp = runInferM inp $
|
||||
do x <- inferModule m
|
||||
newModuleScope (mName func) [] mempty
|
||||
mapM_ addParamType (mParamTypes x)
|
||||
addParameterConstraints (mParamConstraints x)
|
||||
y <- checkModuleInstance func x
|
||||
proveModuleTopLevel
|
||||
endModuleInstance
|
||||
pure y
|
||||
|
||||
tcExpr :: P.Expr Name -> InferInput -> IO (InferOutput (Expr,Schema))
|
||||
tcExpr e0 inp = runInferM inp
|
||||
@ -92,8 +97,9 @@ tcExpr e0 inp = runInferM inp
|
||||
, show e'
|
||||
, show t
|
||||
]
|
||||
_ -> do fresh <- liftSupply (mkDeclared exprModName SystemName
|
||||
(packIdent "(expression)") Nothing loc)
|
||||
_ -> do fresh <- liftSupply $
|
||||
mkDeclared NSValue (TopModule exprModName) SystemName
|
||||
(packIdent "(expression)") Nothing loc
|
||||
res <- inferBinds True False
|
||||
[ P.Bind
|
||||
{ P.bName = P.Located { P.srcRange = loc, P.thing = fresh }
|
||||
@ -105,6 +111,7 @@ tcExpr e0 inp = runInferM inp
|
||||
, P.bInfix = False
|
||||
, P.bFixity = Nothing
|
||||
, P.bDoc = Nothing
|
||||
, P.bExport = Public
|
||||
} ]
|
||||
|
||||
case res of
|
||||
@ -119,10 +126,12 @@ tcExpr e0 inp = runInferM inp
|
||||
: map show res
|
||||
)
|
||||
|
||||
tcDecls :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup])
|
||||
tcDecls ds inp = runInferM inp $ inferDs ds $ \dgs -> do
|
||||
proveModuleTopLevel
|
||||
return dgs
|
||||
tcDecls :: [P.TopDecl Name] -> InferInput -> IO (InferOutput [DeclGroup])
|
||||
tcDecls ds inp = runInferM inp $
|
||||
do newLocalScope
|
||||
checkTopDecls ds
|
||||
proveModuleTopLevel
|
||||
endLocalScope
|
||||
|
||||
ppWarning :: (Range,Warning) -> Doc
|
||||
ppWarning (r,w) = text "[warning] at" <+> pp r <.> colon $$ nest 2 (pp w)
|
||||
|
@ -18,10 +18,10 @@ module Cryptol.TypeCheck.AST
|
||||
, Name()
|
||||
, TFun(..)
|
||||
, Selector(..)
|
||||
, Import(..)
|
||||
, Import, ImportG(..)
|
||||
, ImportSpec(..)
|
||||
, ExportType(..)
|
||||
, ExportSpec(..), isExportedBind, isExportedType
|
||||
, ExportSpec(..), isExportedBind, isExportedType, isExported
|
||||
, Pragma(..)
|
||||
, Fixity(..)
|
||||
, PrimMap(..)
|
||||
@ -30,10 +30,12 @@ module Cryptol.TypeCheck.AST
|
||||
|
||||
import Cryptol.Parser.Position(Located,Range,HasLoc(..))
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
import Cryptol.ModuleSystem.Exports(ExportSpec(..)
|
||||
, isExportedBind, isExportedType)
|
||||
, isExportedBind, isExportedType, isExported)
|
||||
import Cryptol.Parser.AST ( Selector(..),Pragma(..)
|
||||
, Import(..), ImportSpec(..), ExportType(..)
|
||||
, Import
|
||||
, ImportG(..), ImportSpec(..), ExportType(..)
|
||||
, Fixity(..))
|
||||
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim)
|
||||
import Cryptol.Utils.RecordMap
|
||||
@ -50,57 +52,59 @@ import Data.Text (Text)
|
||||
|
||||
|
||||
-- | A Cryptol module.
|
||||
data Module = Module { mName :: !ModName
|
||||
, mExports :: ExportSpec Name
|
||||
, mImports :: [Import]
|
||||
data ModuleG mname =
|
||||
Module { mName :: !mname
|
||||
, mExports :: ExportSpec Name
|
||||
, mImports :: [Import]
|
||||
|
||||
, mTySyns :: Map Name TySyn
|
||||
-- ^ This is just the type-level type synonyms
|
||||
-- of a module.
|
||||
{-| Interfaces of submodules, including functors.
|
||||
This is only the directly nested modules.
|
||||
Info about more nested modules is in the
|
||||
corresponding interface. -}
|
||||
, mSubModules :: Map Name (IfaceG Name)
|
||||
|
||||
, mNewtypes :: Map Name Newtype
|
||||
, mPrimTypes :: Map Name AbstractType
|
||||
-- params, if functor
|
||||
, mParamTypes :: Map Name ModTParam
|
||||
, mParamConstraints :: [Located Prop]
|
||||
, mParamFuns :: Map Name ModVParam
|
||||
|
||||
|
||||
-- Declarations, including everything from non-functor
|
||||
-- submodules
|
||||
, mTySyns :: Map Name TySyn
|
||||
, mNewtypes :: Map Name Newtype
|
||||
, mPrimTypes :: Map Name AbstractType
|
||||
, mDecls :: [DeclGroup]
|
||||
, mFunctors :: Map Name (ModuleG Name)
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
emptyModule :: mname -> ModuleG mname
|
||||
emptyModule nm =
|
||||
Module
|
||||
{ mName = nm
|
||||
, mExports = mempty
|
||||
, mImports = []
|
||||
, mSubModules = mempty
|
||||
|
||||
, mParamTypes = mempty
|
||||
, mParamConstraints = mempty
|
||||
, mParamFuns = mempty
|
||||
|
||||
, mTySyns = mempty
|
||||
, mNewtypes = mempty
|
||||
, mPrimTypes = mempty
|
||||
, mDecls = mempty
|
||||
, mFunctors = mempty
|
||||
}
|
||||
|
||||
type Module = ModuleG ModName
|
||||
|
||||
-- | Is this a parameterized module?
|
||||
isParametrizedModule :: Module -> Bool
|
||||
isParametrizedModule :: ModuleG mname -> Bool
|
||||
isParametrizedModule m = not (null (mParamTypes m) &&
|
||||
null (mParamConstraints m) &&
|
||||
null (mParamFuns m))
|
||||
|
||||
-- | A type parameter of a module.
|
||||
data ModTParam = ModTParam
|
||||
{ mtpName :: Name
|
||||
, mtpKind :: Kind
|
||||
, mtpNumber :: !Int -- ^ The number of the parameter in the module
|
||||
-- This is used when we move parameters from the module
|
||||
-- level to individual declarations
|
||||
-- (type synonyms in particular)
|
||||
, mtpDoc :: Maybe Text
|
||||
} deriving (Show,Generic,NFData)
|
||||
|
||||
mtpParam :: ModTParam -> TParam
|
||||
mtpParam mtp = TParam { tpUnique = nameUnique (mtpName mtp)
|
||||
, tpKind = mtpKind mtp
|
||||
, tpFlav = TPModParam (mtpName mtp)
|
||||
, tpInfo = desc
|
||||
}
|
||||
where desc = TVarInfo { tvarDesc = TVFromModParam (mtpName mtp)
|
||||
, tvarSource = nameLoc (mtpName mtp)
|
||||
}
|
||||
|
||||
-- | A value parameter of a module.
|
||||
data ModVParam = ModVParam
|
||||
{ mvpName :: Name
|
||||
, mvpType :: Schema
|
||||
, mvpDoc :: Maybe Text
|
||||
, mvpFixity :: Maybe Fixity
|
||||
} deriving (Show,Generic,NFData)
|
||||
|
||||
|
||||
data Expr = EList [Expr] Type -- ^ List value (with type of elements)
|
||||
| ETuple [Expr] -- ^ Tuple value
|
||||
@ -369,10 +373,10 @@ instance PP (WithNames DeclDef) where
|
||||
instance PP Decl where
|
||||
ppPrec = ppWithNamesPrec IntMap.empty
|
||||
|
||||
instance PP Module where
|
||||
instance PP n => PP (ModuleG n) where
|
||||
ppPrec = ppWithNamesPrec IntMap.empty
|
||||
|
||||
instance PP (WithNames Module) where
|
||||
instance PP n => PP (WithNames (ModuleG n)) where
|
||||
ppPrec _ (WithNames Module { .. } nm) =
|
||||
text "module" <+> pp mName $$
|
||||
-- XXX: Print exports?
|
||||
|
@ -1,3 +1,4 @@
|
||||
{-# Language OverloadedStrings #-}
|
||||
module Cryptol.TypeCheck.CheckModuleInstance (checkModuleInstance) where
|
||||
|
||||
import Data.Map ( Map )
|
||||
@ -20,7 +21,12 @@ import Cryptol.Utils.Panic
|
||||
checkModuleInstance :: Module {- ^ type-checked functor -} ->
|
||||
Module {- ^ type-checked instance -} ->
|
||||
InferM Module -- ^ Instantiated module
|
||||
checkModuleInstance func inst =
|
||||
checkModuleInstance func inst
|
||||
| not (null (mSubModules func) && null (mSubModules inst)) =
|
||||
do recordError $ TemporaryError
|
||||
"Cannot combine nested modules with old-style parameterized modules"
|
||||
pure func -- doesn't matter?
|
||||
| otherwise =
|
||||
do tMap <- checkTyParams func inst
|
||||
vMap <- checkValParams func tMap inst
|
||||
(ctrs, m) <- instantiateModule func (mName inst) tMap vMap
|
||||
@ -43,6 +49,9 @@ checkModuleInstance func inst =
|
||||
, mParamConstraints = mParamConstraints inst
|
||||
, mParamFuns = mParamFuns inst
|
||||
, mDecls = mDecls inst ++ mDecls m
|
||||
|
||||
, mSubModules = mempty
|
||||
, mFunctors = mempty
|
||||
}
|
||||
|
||||
-- | Check that the type parameters of the functors all have appropriate
|
||||
@ -179,6 +188,7 @@ makeValParamDef x sDef pDef =
|
||||
, P.bPragmas = []
|
||||
, P.bMono = False
|
||||
, P.bDoc = Nothing
|
||||
, P.bExport = Public
|
||||
}
|
||||
loc a = P.Located { P.srcRange = nameLoc x, P.thing = a }
|
||||
|
||||
|
@ -1,214 +0,0 @@
|
||||
-- |
|
||||
-- Module : Cryptol.TypeCheck.Depends
|
||||
-- Copyright : (c) 2013-2016 Galois, Inc.
|
||||
-- License : BSD3
|
||||
-- Maintainer : cryptol@galois.com
|
||||
-- Stability : provisional
|
||||
-- Portability : portable
|
||||
|
||||
{-# LANGUAGE Safe #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
module Cryptol.TypeCheck.Depends where
|
||||
|
||||
import Cryptol.ModuleSystem.Name (Name)
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
import Cryptol.Parser.Position(Range, Located(..), thing)
|
||||
import Cryptol.Parser.Names (namesB, tnamesT, tnamesC,
|
||||
boundNamesSet, boundNames)
|
||||
import Cryptol.TypeCheck.Monad( InferM, getTVars )
|
||||
import Cryptol.TypeCheck.Error(Error(..))
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.RecordMap(recordElements)
|
||||
|
||||
import Data.List(sortBy, groupBy)
|
||||
import Data.Function(on)
|
||||
import Data.Maybe(mapMaybe)
|
||||
import Data.Graph.SCC(stronglyConnComp)
|
||||
import Data.Graph (SCC(..))
|
||||
import Data.Map (Map)
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import Data.Text (Text)
|
||||
import MonadLib (ExceptionT, runExceptionT, raise)
|
||||
|
||||
data TyDecl =
|
||||
TS (P.TySyn Name) (Maybe Text) -- ^ Type synonym
|
||||
| NT (P.Newtype Name) (Maybe Text) -- ^ Newtype
|
||||
| AT (P.ParameterType Name) (Maybe Text) -- ^ Parameter type
|
||||
| PS (P.PropSyn Name) (Maybe Text) -- ^ Property synonym
|
||||
| PT (P.PrimType Name) (Maybe Text) -- ^ A primitive/abstract typee
|
||||
deriving Show
|
||||
|
||||
setDocString :: Maybe Text -> TyDecl -> TyDecl
|
||||
setDocString x d =
|
||||
case d of
|
||||
TS a _ -> TS a x
|
||||
PS a _ -> PS a x
|
||||
NT a _ -> NT a x
|
||||
AT a _ -> AT a x
|
||||
PT a _ -> PT a x
|
||||
|
||||
-- | Check for duplicate and recursive type synonyms.
|
||||
-- Returns the type-synonyms in dependency order.
|
||||
orderTyDecls :: [TyDecl] -> InferM (Either Error [TyDecl])
|
||||
orderTyDecls ts =
|
||||
do vs <- getTVars
|
||||
ds <- combine $ map (toMap vs) ts
|
||||
let ordered = mkScc [ (t,[x],deps)
|
||||
| (x,(t,deps)) <- Map.toList (Map.map thing ds) ]
|
||||
runExceptionT (concat `fmap` mapM check ordered)
|
||||
|
||||
where
|
||||
toMap vs ty@(PT p _) =
|
||||
let x = P.primTName p
|
||||
(as,cs) = P.primTCts p
|
||||
in ( thing x
|
||||
, x { thing = (ty, Set.toList $
|
||||
boundNamesSet vs $
|
||||
boundNames (map P.tpName as) $
|
||||
Set.unions $
|
||||
map tnamesC cs
|
||||
)
|
||||
}
|
||||
)
|
||||
|
||||
|
||||
toMap _ ty@(AT a _) =
|
||||
let x = P.ptName a
|
||||
in ( thing x, x { thing = (ty, []) } )
|
||||
|
||||
toMap vs ty@(NT (P.Newtype x as fs) _) =
|
||||
( thing x
|
||||
, x { thing = (ty, Set.toList $
|
||||
boundNamesSet vs $
|
||||
boundNames (map P.tpName as) $
|
||||
Set.unions $
|
||||
map (tnamesT . snd) (recordElements fs)
|
||||
)
|
||||
}
|
||||
)
|
||||
|
||||
toMap vs ty@(TS (P.TySyn x _ as t) _) =
|
||||
(thing x
|
||||
, x { thing = (ty, Set.toList $
|
||||
boundNamesSet vs $
|
||||
boundNames (map P.tpName as) $
|
||||
tnamesT t
|
||||
)
|
||||
}
|
||||
)
|
||||
|
||||
toMap vs ty@(PS (P.PropSyn x _ as ps) _) =
|
||||
(thing x
|
||||
, x { thing = (ty, Set.toList $
|
||||
boundNamesSet vs $
|
||||
boundNames (map P.tpName as) $
|
||||
Set.unions $
|
||||
map tnamesC ps
|
||||
)
|
||||
}
|
||||
)
|
||||
getN (TS x _) = thing (P.tsName x)
|
||||
getN (PS x _) = thing (P.psName x)
|
||||
getN (NT x _) = thing (P.nName x)
|
||||
getN (AT x _) = thing (P.ptName x)
|
||||
getN (PT x _) = thing (P.primTName x)
|
||||
|
||||
check :: SCC TyDecl -> ExceptionT Error InferM [TyDecl]
|
||||
check (AcyclicSCC x) = return [x]
|
||||
|
||||
-- We don't support any recursion, for now.
|
||||
-- We could support recursion between newtypes, or newtypes and tysysn.
|
||||
check (CyclicSCC xs) = raise (RecursiveTypeDecls (map getN xs))
|
||||
|
||||
-- | Associate type signatures with bindings and order bindings by dependency.
|
||||
orderBinds :: [P.Bind Name] -> [SCC (P.Bind Name)]
|
||||
orderBinds bs = mkScc [ (b, map thing defs, Set.toList uses)
|
||||
| b <- bs
|
||||
, let (defs,uses) = namesB b
|
||||
]
|
||||
|
||||
class FromDecl d where
|
||||
toBind :: d -> Maybe (P.Bind Name)
|
||||
toParamFun :: d -> Maybe (P.ParameterFun Name)
|
||||
toParamConstraints :: d -> [P.Located (P.Prop Name)]
|
||||
toTyDecl :: d -> Maybe TyDecl
|
||||
isTopDecl :: d -> Bool
|
||||
|
||||
instance FromDecl (P.TopDecl Name) where
|
||||
toBind (P.Decl x) = toBind (P.tlValue x)
|
||||
toBind _ = Nothing
|
||||
|
||||
toParamFun (P.DParameterFun d) = Just d
|
||||
toParamFun _ = Nothing
|
||||
|
||||
toParamConstraints (P.DParameterConstraint xs) = xs
|
||||
toParamConstraints _ = []
|
||||
|
||||
toTyDecl (P.DPrimType p) = Just (PT (P.tlValue p) (thing <$> P.tlDoc p))
|
||||
toTyDecl (P.DParameterType d) = Just (AT d (P.ptDoc d))
|
||||
toTyDecl (P.TDNewtype d) = Just (NT (P.tlValue d) (thing <$> P.tlDoc d))
|
||||
toTyDecl (P.Decl x) = setDocString (thing <$> P.tlDoc x)
|
||||
<$> toTyDecl (P.tlValue x)
|
||||
toTyDecl _ = Nothing
|
||||
|
||||
isTopDecl _ = True
|
||||
|
||||
instance FromDecl (P.Decl Name) where
|
||||
toBind (P.DLocated d _) = toBind d
|
||||
toBind (P.DBind b) = return b
|
||||
toBind _ = Nothing
|
||||
|
||||
toParamFun _ = Nothing
|
||||
toParamConstraints _ = []
|
||||
|
||||
toTyDecl (P.DLocated d _) = toTyDecl d
|
||||
toTyDecl (P.DType x) = Just (TS x Nothing)
|
||||
toTyDecl (P.DProp x) = Just (PS x Nothing)
|
||||
toTyDecl _ = Nothing
|
||||
|
||||
isTopDecl _ = False
|
||||
|
||||
{- | Given a list of declarations, annoted with (i) the names that they
|
||||
define, and (ii) the names that they use, we compute a list of strongly
|
||||
connected components of the declarations. The SCCs are in dependency order. -}
|
||||
mkScc :: [(a,[Name],[Name])] -> [SCC a]
|
||||
mkScc ents = stronglyConnComp $ zipWith mkGr keys ents
|
||||
where
|
||||
keys = [ 0 :: Integer .. ]
|
||||
|
||||
mkGr i (x,_,uses) = (x,i,mapMaybe (`Map.lookup` nodeMap) uses)
|
||||
|
||||
-- Maps names to node ids.
|
||||
nodeMap = Map.fromList $ concat $ zipWith mkNode keys ents
|
||||
mkNode i (_,defs,_) = [ (d,i) | d <- defs ]
|
||||
|
||||
{- | Combine a bunch of definitions into a single map. Here we check
|
||||
that each name is defined only onces. -}
|
||||
combineMaps :: [Map Name (Located a)] -> InferM (Map Name (Located a))
|
||||
combineMaps ms = if null bad then return (Map.unions ms)
|
||||
else panic "combineMaps" $ "Multiple definitions"
|
||||
: map show bad
|
||||
where
|
||||
bad = do m <- ms
|
||||
duplicates [ a { thing = x } | (x,a) <- Map.toList m ]
|
||||
|
||||
{- | Combine a bunch of definitions into a single map. Here we check
|
||||
that each name is defined only onces. -}
|
||||
combine :: [(Name, Located a)] -> InferM (Map Name (Located a))
|
||||
combine m = if null bad then return (Map.fromList m)
|
||||
else panic "combine" $ "Multiple definitions"
|
||||
: map show bad
|
||||
where
|
||||
bad = duplicates [ a { thing = x } | (x,a) <- m ]
|
||||
|
||||
-- | Identify multiple occurances of something.
|
||||
duplicates :: Ord a => [Located a] -> [(a,[Range])]
|
||||
duplicates = mapMaybe multiple
|
||||
. groupBy ((==) `on` thing)
|
||||
. sortBy (compare `on` thing)
|
||||
where
|
||||
multiple xs@(x : _ : _) = Just (thing x, map srcRange xs)
|
||||
multiple _ = Nothing
|
||||
|
||||
|
@ -139,6 +139,12 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind
|
||||
| TypeShadowing String Name String
|
||||
| MissingModTParam (Located Ident)
|
||||
| MissingModVParam (Located Ident)
|
||||
|
||||
| TemporaryError Doc
|
||||
-- ^ This is for errors that don't fit other cateogories.
|
||||
-- We should not use it much, and is generally to be used
|
||||
-- for transient errors, which are due to incomplete
|
||||
-- implementation.
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
-- | When we have multiple errors on the same location, we show only the
|
||||
@ -147,6 +153,10 @@ errorImportance :: Error -> Int
|
||||
errorImportance err =
|
||||
case err of
|
||||
BareTypeApp -> 11 -- basically a parse error
|
||||
TemporaryError {} -> 11
|
||||
-- show these as usually means the user used something that doesn't work
|
||||
|
||||
|
||||
KindMismatch {} -> 10
|
||||
TyVarWithParams {} -> 9
|
||||
TypeMismatch {} -> 8
|
||||
@ -236,6 +246,8 @@ instance TVars Error where
|
||||
MissingModTParam {} -> err
|
||||
MissingModVParam {} -> err
|
||||
|
||||
TemporaryError {} -> err
|
||||
|
||||
|
||||
instance FVS Error where
|
||||
fvs err =
|
||||
@ -269,6 +281,8 @@ instance FVS Error where
|
||||
MissingModTParam {} -> Set.empty
|
||||
MissingModVParam {} -> Set.empty
|
||||
|
||||
TemporaryError {} -> Set.empty
|
||||
|
||||
instance PP Warning where
|
||||
ppPrec = ppWithNamesPrec IntMap.empty
|
||||
|
||||
@ -436,9 +450,7 @@ instance PP (WithNames Error) where
|
||||
MissingModVParam x ->
|
||||
"Missing definition for value parameter" <+> quotes (pp (thing x))
|
||||
|
||||
|
||||
|
||||
|
||||
TemporaryError doc -> doc
|
||||
where
|
||||
bullets xs = vcat [ "•" <+> d | d <- xs ]
|
||||
|
||||
|
@ -13,16 +13,18 @@
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
{-# LANGUAGE RecursiveDo #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
module Cryptol.TypeCheck.Infer
|
||||
( checkE
|
||||
, checkSigB
|
||||
, inferModule
|
||||
, inferBinds
|
||||
, inferDs
|
||||
, checkTopDecls
|
||||
)
|
||||
where
|
||||
|
||||
import Data.Text(Text)
|
||||
import qualified Data.Text as Text
|
||||
|
||||
|
||||
@ -41,7 +43,6 @@ import Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
|
||||
checkPrimType,
|
||||
checkParameterConstraints)
|
||||
import Cryptol.TypeCheck.Instantiate
|
||||
import Cryptol.TypeCheck.Depends
|
||||
import Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst)
|
||||
import Cryptol.Utils.Ident
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
@ -50,43 +51,24 @@ import Cryptol.Utils.RecordMap
|
||||
import qualified Data.Map as Map
|
||||
import Data.Map (Map)
|
||||
import qualified Data.Set as Set
|
||||
import Data.List(foldl',sortBy)
|
||||
import Data.List(foldl',sortBy,groupBy)
|
||||
import Data.Either(partitionEithers)
|
||||
import Data.Maybe(mapMaybe,isJust, fromMaybe)
|
||||
import Data.Maybe(isJust, fromMaybe, mapMaybe)
|
||||
import Data.List(partition)
|
||||
import Data.Graph(SCC(..))
|
||||
import Data.Ratio(numerator,denominator)
|
||||
import Data.Traversable(forM)
|
||||
import Control.Monad(zipWithM,unless,foldM)
|
||||
import Data.Function(on)
|
||||
import Control.Monad(zipWithM,unless,foldM,forM_)
|
||||
|
||||
|
||||
|
||||
inferModule :: P.Module Name -> InferM Module
|
||||
inferModule m =
|
||||
inferDs (P.mDecls m) $ \ds1 ->
|
||||
do proveModuleTopLevel
|
||||
ts <- getTSyns
|
||||
nts <- getNewtypes
|
||||
ats <- getAbstractTypes
|
||||
pTs <- getParamTypes
|
||||
pCs <- getParamConstraints
|
||||
pFuns <- getParamFuns
|
||||
return Module { mName = thing (P.mName m)
|
||||
, mExports = P.modExports m
|
||||
, mImports = map thing (P.mImports m)
|
||||
, mTySyns = Map.mapMaybe onlyLocal ts
|
||||
, mNewtypes = Map.mapMaybe onlyLocal nts
|
||||
, mPrimTypes = Map.mapMaybe onlyLocal ats
|
||||
, mParamTypes = pTs
|
||||
, mParamConstraints = pCs
|
||||
, mParamFuns = pFuns
|
||||
, mDecls = ds1
|
||||
}
|
||||
where
|
||||
onlyLocal (IsLocal, x) = Just x
|
||||
onlyLocal (IsExternal, _) = Nothing
|
||||
|
||||
|
||||
do newModuleScope (thing (P.mName m)) (map thing (P.mImports m))
|
||||
(P.modExports m)
|
||||
checkTopDecls (P.mDecls m)
|
||||
proveModuleTopLevel
|
||||
endModule
|
||||
|
||||
-- | Construct a Prelude primitive in the parsed AST.
|
||||
mkPrim :: String -> InferM (P.Expr Name)
|
||||
@ -164,9 +146,8 @@ appTys expr ts tGoal =
|
||||
-- Here is an example of why this might be useful:
|
||||
-- f ` { x = T } where type T = ...
|
||||
P.EWhere e ds ->
|
||||
inferDs ds $ \ds1 -> do e1 <- appTys e ts tGoal
|
||||
return (EWhere e1 ds1)
|
||||
-- XXX: Is there a scoping issue here? I think not, but check.
|
||||
do (e1,ds1) <- checkLocalDecls ds (appTys e ts tGoal)
|
||||
pure (EWhere e1 ds1)
|
||||
|
||||
P.ELocated e r ->
|
||||
do e' <- inRange r (appTys e ts tGoal)
|
||||
@ -349,6 +330,23 @@ checkE expr tGoal =
|
||||
ds <- combineMaps dss
|
||||
e' <- withMonoTypes ds (checkE e (WithSource a TypeOfSeqElement))
|
||||
return (EComp len a e' mss')
|
||||
where
|
||||
-- the renamer should have made these checks already?
|
||||
combineMaps ms = if null bad
|
||||
then return (Map.unions ms)
|
||||
else panic "combineMaps" $ "Multiple definitions"
|
||||
: map show bad
|
||||
where
|
||||
bad = do m <- ms
|
||||
duplicates [ a { thing = x } | (x,a) <- Map.toList m ]
|
||||
duplicates = mapMaybe multiple
|
||||
. groupBy ((==) `on` thing)
|
||||
. sortBy (compare `on` thing)
|
||||
where
|
||||
multiple xs@(x : _ : _) = Just (thing x, map srcRange xs)
|
||||
multiple _ = Nothing
|
||||
|
||||
|
||||
|
||||
P.EAppT e fs -> appTys e (map uncheckedTypeArg fs) tGoal
|
||||
|
||||
@ -366,8 +364,8 @@ checkE expr tGoal =
|
||||
return (EIf e1' e2' e3')
|
||||
|
||||
P.EWhere e ds ->
|
||||
inferDs ds $ \ds1 -> do e1 <- checkE e tGoal
|
||||
return (EWhere e1 ds1)
|
||||
do (e1,ds1) <- checkLocalDecls ds (checkE e tGoal)
|
||||
pure (EWhere e1 ds1)
|
||||
|
||||
P.ETyped e t ->
|
||||
do tSig <- checkTypeOfKind t KType
|
||||
@ -406,7 +404,7 @@ checkRecUpd mb fs tGoal =
|
||||
|
||||
-- { _ | fs } ~~> \r -> { r | fs }
|
||||
Nothing ->
|
||||
do r <- newParamName (packIdent "r")
|
||||
do r <- newParamName NSValue (packIdent "r")
|
||||
let p = P.PVar Located { srcRange = nameLoc r, thing = r }
|
||||
fe = P.EFun P.emptyFunDesc [p] (P.EUpd (Just (P.EVar r)) fs)
|
||||
checkE fe tGoal
|
||||
@ -432,7 +430,7 @@ checkRecUpd mb fs tGoal =
|
||||
v1 <- checkE v (WithSource (tFun ft ft) src)
|
||||
-- XXX: ^ may be used a different src?
|
||||
d <- newHasGoal s (twsType tGoal) ft
|
||||
tmp <- newParamName (packIdent "rf")
|
||||
tmp <- newParamName NSValue (packIdent "rf")
|
||||
let e' = EVar tmp
|
||||
pure $ hasDoSet d e' (EApp v1 (hasDoSelect d e'))
|
||||
`EWhere`
|
||||
@ -581,10 +579,11 @@ checkHasType inferredType tGoal =
|
||||
|
||||
|
||||
checkFun ::
|
||||
P.FunDesc Name -> [P.Pattern Name] -> P.Expr Name -> TypeWithSource -> InferM Expr
|
||||
P.FunDesc Name -> [P.Pattern Name] ->
|
||||
P.Expr Name -> TypeWithSource -> InferM Expr
|
||||
checkFun _ [] e tGoal = checkE e tGoal
|
||||
checkFun (P.FunDesc fun offset) ps e tGoal =
|
||||
inNewScope $
|
||||
inNewScope
|
||||
do let descs = [ TypeOfArg (ArgDescr fun (Just n)) | n <- [ 1 + offset .. ] ]
|
||||
|
||||
(tys,tRes) <- expectFun fun (length ps) tGoal
|
||||
@ -965,68 +964,104 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
|
||||
, dDoc = P.bDoc b
|
||||
}
|
||||
|
||||
inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a
|
||||
inferDs ds continue = either onErr checkTyDecls =<< orderTyDecls (mapMaybe toTyDecl ds)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
checkLocalDecls :: [P.Decl Name] -> InferM a -> InferM (a,[DeclGroup])
|
||||
checkLocalDecls ds0 k =
|
||||
do newLocalScope
|
||||
forM_ ds0 \d -> checkDecl False d Nothing
|
||||
a <- k
|
||||
ds <- endLocalScope
|
||||
pure (a,ds)
|
||||
|
||||
|
||||
|
||||
checkTopDecls :: [P.TopDecl Name] -> InferM ()
|
||||
checkTopDecls = mapM_ checkTopDecl
|
||||
where
|
||||
onErr err = recordError err >> continue []
|
||||
checkTopDecl decl =
|
||||
case decl of
|
||||
P.Decl tl -> checkDecl True (P.tlValue tl) (thing <$> P.tlDoc tl)
|
||||
|
||||
isTopLevel = isTopDecl (head ds)
|
||||
P.TDNewtype tl ->
|
||||
do t <- checkNewtype (P.tlValue tl) (thing <$> P.tlDoc tl)
|
||||
addNewtype t
|
||||
|
||||
checkTyDecls (AT t mbD : ts) =
|
||||
do t1 <- checkParameterType t mbD
|
||||
withParamType t1 (checkTyDecls ts)
|
||||
P.DPrimType tl ->
|
||||
do t <- checkPrimType (P.tlValue tl) (thing <$> P.tlDoc tl)
|
||||
addPrimType t
|
||||
|
||||
checkTyDecls (TS t mbD : ts) =
|
||||
do t1 <- checkTySyn t mbD
|
||||
withTySyn t1 (checkTyDecls ts)
|
||||
P.DParameterType ty ->
|
||||
do t <- checkParameterType ty (P.ptDoc ty)
|
||||
addParamType t
|
||||
|
||||
checkTyDecls (PS t mbD : ts) =
|
||||
do t1 <- checkPropSyn t mbD
|
||||
withTySyn t1 (checkTyDecls ts)
|
||||
P.DParameterConstraint cs ->
|
||||
do cs1 <- checkParameterConstraints cs
|
||||
addParameterConstraints cs1
|
||||
|
||||
checkTyDecls (NT t mbD : ts) =
|
||||
do t1 <- checkNewtype t mbD
|
||||
withNewtype t1 (checkTyDecls ts)
|
||||
P.DParameterFun pf ->
|
||||
do x <- checkParameterFun pf
|
||||
addParamFun x
|
||||
|
||||
checkTyDecls (PT p mbD : ts) =
|
||||
do p1 <- checkPrimType p mbD
|
||||
withPrimType p1 (checkTyDecls ts)
|
||||
P.DModule tl ->
|
||||
do let P.NestedModule m = P.tlValue tl
|
||||
newSubmoduleScope (thing (P.mName m)) (map thing (P.mImports m))
|
||||
(P.modExports m)
|
||||
checkTopDecls (P.mDecls m)
|
||||
endSubmodule
|
||||
|
||||
-- We checked all type synonyms, now continue with value-level definitions:
|
||||
checkTyDecls [] =
|
||||
do cs <- checkParameterConstraints (concatMap toParamConstraints ds)
|
||||
withParameterConstraints cs $
|
||||
do xs <- mapM checkParameterFun (mapMaybe toParamFun ds)
|
||||
withParamFuns xs $ checkBinds [] $ orderBinds $ mapMaybe toBind ds
|
||||
P.DImport {} -> pure ()
|
||||
P.Include {} -> panic "checkTopDecl" [ "Unexpected `inlude`" ]
|
||||
|
||||
|
||||
checkParameterFun x =
|
||||
do (s,gs) <- checkSchema NoWildCards (P.pfSchema x)
|
||||
su <- proveImplication (Just (thing (P.pfName x)))
|
||||
(sVars s) (sProps s) gs
|
||||
unless (isEmptySubst su) $
|
||||
panic "checkParameterFun" ["Subst not empty??"]
|
||||
let n = thing (P.pfName x)
|
||||
return ModVParam { mvpName = n
|
||||
, mvpType = s
|
||||
, mvpDoc = P.pfDoc x
|
||||
, mvpFixity = P.pfFixity x
|
||||
}
|
||||
checkDecl :: Bool -> P.Decl Name -> Maybe Text -> InferM ()
|
||||
checkDecl isTopLevel d mbDoc =
|
||||
case d of
|
||||
|
||||
checkBinds decls (CyclicSCC bs : more) =
|
||||
do bs1 <- inferBinds isTopLevel True bs
|
||||
foldr (\b m -> withVar (dName b) (dSignature b) m)
|
||||
(checkBinds (Recursive bs1 : decls) more)
|
||||
bs1
|
||||
P.DBind c ->
|
||||
do ~[b] <- inferBinds isTopLevel False [c]
|
||||
addDecls (NonRecursive b)
|
||||
|
||||
P.DRec bs ->
|
||||
do bs1 <- inferBinds isTopLevel True bs
|
||||
addDecls (Recursive bs1)
|
||||
|
||||
P.DType t ->
|
||||
do t1 <- checkTySyn t mbDoc
|
||||
addTySyn t1
|
||||
|
||||
P.DProp t ->
|
||||
do t1 <- checkPropSyn t mbDoc
|
||||
addTySyn t1
|
||||
|
||||
P.DLocated d' r -> inRange r (checkDecl isTopLevel d' mbDoc)
|
||||
|
||||
P.DSignature {} -> bad "DSignature"
|
||||
P.DFixity {} -> bad "DFixity"
|
||||
P.DPragma {} -> bad "DPragma"
|
||||
P.DPatBind {} -> bad "DPatBind"
|
||||
|
||||
where
|
||||
bad x = panic "checkDecl" [x]
|
||||
|
||||
|
||||
checkParameterFun :: P.ParameterFun Name -> InferM ModVParam
|
||||
checkParameterFun x =
|
||||
do (s,gs) <- checkSchema NoWildCards (P.pfSchema x)
|
||||
su <- proveImplication (Just (thing (P.pfName x)))
|
||||
(sVars s) (sProps s) gs
|
||||
unless (isEmptySubst su) $
|
||||
panic "checkParameterFun" ["Subst not empty??"]
|
||||
let n = thing (P.pfName x)
|
||||
return ModVParam { mvpName = n
|
||||
, mvpType = s
|
||||
, mvpDoc = P.pfDoc x
|
||||
, mvpFixity = P.pfFixity x
|
||||
}
|
||||
|
||||
checkBinds decls (AcyclicSCC c : more) =
|
||||
do ~[b] <- inferBinds isTopLevel False [c]
|
||||
withVar (dName b) (dSignature b) $
|
||||
checkBinds (NonRecursive b : decls) more
|
||||
|
||||
-- We are done with all value-level definitions.
|
||||
-- Now continue with anything that's in scope of the declarations.
|
||||
checkBinds decls [] = continue (reverse decls)
|
||||
|
||||
tcPanic :: String -> [String] -> a
|
||||
tcPanic l msg = panic ("[TypeCheck] " ++ l) msg
|
||||
|
73
src/Cryptol/TypeCheck/Interface.hs
Normal file
73
src/Cryptol/TypeCheck/Interface.hs
Normal file
@ -0,0 +1,73 @@
|
||||
module Cryptol.TypeCheck.Interface where
|
||||
|
||||
import qualified Data.Map as Map
|
||||
|
||||
import Cryptol.Utils.Ident(Namespace(..))
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
import Cryptol.TypeCheck.AST
|
||||
|
||||
|
||||
mkIfaceDecl :: Decl -> IfaceDecl
|
||||
mkIfaceDecl d = IfaceDecl
|
||||
{ ifDeclName = dName d
|
||||
, ifDeclSig = dSignature d
|
||||
, ifDeclPragmas = dPragmas d
|
||||
, ifDeclInfix = dInfix d
|
||||
, ifDeclFixity = dFixity d
|
||||
, ifDeclDoc = dDoc d
|
||||
}
|
||||
|
||||
-- | Generate an Iface from a typechecked module.
|
||||
genIface :: ModuleG mname -> IfaceG mname
|
||||
genIface m = Iface
|
||||
{ ifModName = mName m
|
||||
|
||||
, ifPublic = IfaceDecls
|
||||
{ ifTySyns = tsPub
|
||||
, ifNewtypes = ntPub
|
||||
, ifAbstractTypes = atPub
|
||||
, ifDecls = dPub
|
||||
, ifModules = mPub
|
||||
}
|
||||
|
||||
, ifPrivate = IfaceDecls
|
||||
{ ifTySyns = tsPriv
|
||||
, ifNewtypes = ntPriv
|
||||
, ifAbstractTypes = atPriv
|
||||
, ifDecls = dPriv
|
||||
, ifModules = mPriv
|
||||
}
|
||||
|
||||
, ifParams = IfaceParams
|
||||
{ ifParamTypes = mParamTypes m
|
||||
, ifParamConstraints = mParamConstraints m
|
||||
, ifParamFuns = mParamFuns m
|
||||
}
|
||||
}
|
||||
where
|
||||
|
||||
(tsPub,tsPriv) =
|
||||
Map.partitionWithKey (\ qn _ -> qn `isExportedType` mExports m )
|
||||
(mTySyns m)
|
||||
(ntPub,ntPriv) =
|
||||
Map.partitionWithKey (\ qn _ -> qn `isExportedType` mExports m )
|
||||
(mNewtypes m)
|
||||
|
||||
(atPub,atPriv) =
|
||||
Map.partitionWithKey (\qn _ -> qn `isExportedType` mExports m)
|
||||
(mPrimTypes m)
|
||||
|
||||
(dPub,dPriv) =
|
||||
Map.partitionWithKey (\ qn _ -> qn `isExportedBind` mExports m)
|
||||
$ Map.fromList [ (qn,mkIfaceDecl d) | dg <- mDecls m
|
||||
, d <- groupDecls dg
|
||||
, let qn = dName d
|
||||
]
|
||||
|
||||
(mPub,mPriv) =
|
||||
Map.partitionWithKey (\ qn _ -> isExported NSModule qn (mExports m))
|
||||
$ mSubModules m
|
||||
|
||||
|
||||
|
||||
|
@ -13,30 +13,12 @@
|
||||
{-# LANGUAGE RecursiveDo #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
module Cryptol.TypeCheck.Monad
|
||||
( module Cryptol.TypeCheck.Monad
|
||||
, module Cryptol.TypeCheck.InferTypes
|
||||
) where
|
||||
|
||||
import Cryptol.ModuleSystem.Name
|
||||
(FreshM(..),Supply,mkParameter
|
||||
, nameInfo, NameInfo(..),NameSource(..))
|
||||
import Cryptol.Parser.Position
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Subst
|
||||
import Cryptol.TypeCheck.Unify(mgu, runResult, UnificationError(..))
|
||||
import Cryptol.TypeCheck.InferTypes
|
||||
import Cryptol.TypeCheck.Error( Warning(..),Error(..)
|
||||
, cleanupErrors, computeFreeVarNames
|
||||
)
|
||||
import qualified Cryptol.TypeCheck.SimpleSolver as Simple
|
||||
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
|
||||
import Cryptol.TypeCheck.PP(NameMap)
|
||||
import Cryptol.Utils.PP(pp, (<+>), text,commaSep,brackets)
|
||||
import Cryptol.Utils.Ident(Ident)
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
|
||||
import qualified Control.Applicative as A
|
||||
import qualified Control.Monad.Fail as Fail
|
||||
import Control.Monad.Fix(MonadFix(..))
|
||||
@ -45,14 +27,35 @@ import qualified Data.Set as Set
|
||||
import Data.Map (Map)
|
||||
import Data.Set (Set)
|
||||
import Data.List(find, foldl')
|
||||
import Data.List.NonEmpty(NonEmpty((:|)))
|
||||
import Data.Semigroup(sconcat)
|
||||
import Data.Maybe(mapMaybe,fromMaybe)
|
||||
import MonadLib hiding (mapM)
|
||||
|
||||
import Data.IORef
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
import MonadLib hiding (mapM)
|
||||
|
||||
import Cryptol.ModuleSystem.Name
|
||||
(FreshM(..),Supply,mkParameter
|
||||
, nameInfo, NameInfo(..),NameSource(..))
|
||||
import Cryptol.Parser.Position
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Subst
|
||||
import Cryptol.TypeCheck.Interface(genIface)
|
||||
import Cryptol.TypeCheck.Unify(mgu, runResult, UnificationError(..))
|
||||
import Cryptol.TypeCheck.InferTypes
|
||||
import Cryptol.TypeCheck.Error( Warning(..),Error(..)
|
||||
, cleanupErrors, computeFreeVarNames
|
||||
)
|
||||
import qualified Cryptol.TypeCheck.SimpleSolver as Simple
|
||||
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
|
||||
import Cryptol.TypeCheck.PP(NameMap)
|
||||
import Cryptol.Utils.PP(pp, (<+>), text,commaSep,brackets)
|
||||
import Cryptol.Utils.Ident(Ident,Namespace(..))
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
|
||||
-- | Information needed for type inference.
|
||||
data InferInput = InferInput
|
||||
@ -119,16 +122,21 @@ bumpCounter = do RO { .. } <- IM ask
|
||||
runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
|
||||
runInferM info (IM m) =
|
||||
do counter <- newIORef 0
|
||||
rec ro <- return RO { iRange = inpRange info
|
||||
, iVars = Map.map ExtVar (inpVars info)
|
||||
, iTVars = []
|
||||
, iTSyns = fmap mkExternal (inpTSyns info)
|
||||
, iNewtypes = fmap mkExternal (inpNewtypes info)
|
||||
, iAbstractTypes = mkExternal <$> inpAbstractTypes info
|
||||
, iParamTypes = inpParamTypes info
|
||||
, iParamFuns = inpParamFuns info
|
||||
, iParamConstraints = inpParamConstraints info
|
||||
let env = Map.map ExtVar (inpVars info)
|
||||
<> Map.map (ExtVar . newtypeConType) (inpNewtypes info)
|
||||
|
||||
rec ro <- return RO { iRange = inpRange info
|
||||
, iVars = env
|
||||
, iExtScope = (emptyModule ExternalScope)
|
||||
{ mTySyns = inpTSyns info
|
||||
, mNewtypes = inpNewtypes info
|
||||
, mPrimTypes = inpAbstractTypes info
|
||||
, mParamTypes = inpParamTypes info
|
||||
, mParamFuns = inpParamFuns info
|
||||
, mParamConstraints = inpParamConstraints info
|
||||
}
|
||||
|
||||
, iTVars = []
|
||||
, iSolvedHasLazy = iSolvedHas finalRW -- RECURSION
|
||||
, iMonoBinds = inpMonoBinds info
|
||||
, iCallStacks = inpCallStacks info
|
||||
@ -168,7 +176,6 @@ runInferM info (IM m) =
|
||||
in pure (InferFailed (computeFreeVarNames ws es1) ws es1)
|
||||
|
||||
|
||||
mkExternal x = (IsExternal, x)
|
||||
rw = RW { iErrors = []
|
||||
, iWarnings = []
|
||||
, iSubst = emptySubst
|
||||
@ -181,6 +188,9 @@ runInferM info (IM m) =
|
||||
, iSolvedHas = Map.empty
|
||||
|
||||
, iSupply = inpSupply info
|
||||
|
||||
, iScope = []
|
||||
, iBindTypes = mempty
|
||||
}
|
||||
|
||||
|
||||
@ -191,38 +201,31 @@ runInferM info (IM m) =
|
||||
|
||||
newtype InferM a = IM { unIM :: ReaderT RO (StateT RW IO) a }
|
||||
|
||||
data DefLoc = IsLocal | IsExternal
|
||||
|
||||
data ScopeName = ExternalScope
|
||||
| LocalScope
|
||||
| SubModule Name
|
||||
| MTopModule P.ModName
|
||||
|
||||
-- | Read-only component of the monad.
|
||||
data RO = RO
|
||||
{ iRange :: Range -- ^ Source code being analysed
|
||||
, iVars :: Map Name VarType -- ^ Type of variable that are in scope
|
||||
{ iRange :: Range -- ^ Source code being analysed
|
||||
, iVars :: Map Name VarType
|
||||
-- ^ Type of variable that are in scope
|
||||
-- These are only parameters vars that are in recursive component we
|
||||
-- are checking at the moment. If a var is not there, keep looking in
|
||||
-- the 'iScope'
|
||||
|
||||
{- NOTE: We assume no shadowing between these two, so it does not matter
|
||||
where we look first. Similarly, we assume no shadowing with
|
||||
the existential type variable (in RW). See 'checkTShadowing'. -}
|
||||
|
||||
, iTVars :: [TParam] -- ^ Type variable that are in scope
|
||||
, iTSyns :: Map Name (DefLoc, TySyn) -- ^ Type synonyms that are in scope
|
||||
, iNewtypes :: Map Name (DefLoc, Newtype)
|
||||
-- ^ Newtype declarations in scope
|
||||
--
|
||||
-- NOTE: type synonyms take precedence over newtype. The reason is
|
||||
-- that we can define local type synonyms, but not local newtypes.
|
||||
-- So, either a type-synonym shadows a newtype, or it was declared
|
||||
-- at the top-level, but then there can't be a newtype with the
|
||||
-- same name (this should be caught by the renamer).
|
||||
, iAbstractTypes :: Map Name (DefLoc, AbstractType)
|
||||
, iTVars :: [TParam] -- ^ Type variable that are in scope
|
||||
|
||||
, iParamTypes :: Map Name ModTParam
|
||||
-- ^ Parameter types
|
||||
|
||||
, iParamConstraints :: [Located Prop]
|
||||
-- ^ Constraints on the type parameters
|
||||
|
||||
, iParamFuns :: Map Name ModVParam
|
||||
-- ^ Parameter functions
|
||||
, iExtScope :: ModuleG ScopeName
|
||||
-- ^ These are things we know about, but are not part of the
|
||||
-- modules we are currently constructing.
|
||||
-- XXX: this sould probably be an interface
|
||||
|
||||
-- ^ Information about top-level declarations in modules under
|
||||
-- construction, most nested first.
|
||||
|
||||
, iSolvedHasLazy :: Map Int HasGoalSln
|
||||
-- ^ NOTE: This field is lazy in an important way! It is the
|
||||
@ -278,9 +281,17 @@ data RW = RW
|
||||
{- ^ Tuple/record projection constraints. The 'Int' is the "name"
|
||||
of the constraint, used so that we can name its solution properly. -}
|
||||
|
||||
, iScope :: ![ModuleG ScopeName]
|
||||
-- ^ Nested scopes we are currently checking, most nested first.
|
||||
|
||||
, iBindTypes :: !(Map Name Schema)
|
||||
-- ^ Types of variables that we know about. We don't worry about scoping
|
||||
-- here because we assume the bindings all have different names.
|
||||
|
||||
, iSupply :: !Supply
|
||||
}
|
||||
|
||||
|
||||
instance Functor InferM where
|
||||
fmap f (IM m) = IM (fmap f m)
|
||||
|
||||
@ -452,10 +463,10 @@ solveHasGoal n e =
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- | Generate a fresh variable name to be used in a local binding.
|
||||
newParamName :: Ident -> InferM Name
|
||||
newParamName x =
|
||||
newParamName :: Namespace -> Ident -> InferM Name
|
||||
newParamName ns x =
|
||||
do r <- curRange
|
||||
liftSupply (mkParameter x r)
|
||||
liftSupply (mkParameter ns x r)
|
||||
|
||||
newName :: (NameSeeds -> (a , NameSeeds)) -> InferM a
|
||||
newName upd = IM $ sets $ \s -> let (x,seeds) = upd (iNameSeeds s)
|
||||
@ -634,17 +645,13 @@ lookupVar :: Name -> InferM VarType
|
||||
lookupVar x =
|
||||
do mb <- IM $ asks $ Map.lookup x . iVars
|
||||
case mb of
|
||||
Just t -> return t
|
||||
Just a -> pure a
|
||||
Nothing ->
|
||||
do mbNT <- lookupNewtype x
|
||||
case mbNT of
|
||||
Just nt -> return (ExtVar (newtypeConType nt))
|
||||
Nothing ->
|
||||
do mbParamFun <- lookupParamFun x
|
||||
case mbParamFun of
|
||||
Just pf -> return (ExtVar (mvpType pf))
|
||||
Nothing -> panic "lookupVar" [ "Undefined type variable"
|
||||
, show x]
|
||||
do mb1 <- Map.lookup x . iBindTypes <$> IM get
|
||||
case mb1 of
|
||||
Just a -> pure (ExtVar a)
|
||||
Nothing -> panic "lookupVar" [ "Undefined vairable"
|
||||
, show x ]
|
||||
|
||||
-- | Lookup a type variable. Return `Nothing` if there is no such variable
|
||||
-- in scope, in which case we must be dealing with a type constant.
|
||||
@ -654,14 +661,14 @@ lookupTParam x = IM $ asks $ find this . iTVars
|
||||
|
||||
-- | Lookup the definition of a type synonym.
|
||||
lookupTSyn :: Name -> InferM (Maybe TySyn)
|
||||
lookupTSyn x = fmap (fmap snd . Map.lookup x) getTSyns
|
||||
lookupTSyn x = Map.lookup x <$> getTSyns
|
||||
|
||||
-- | Lookup the definition of a newtype
|
||||
lookupNewtype :: Name -> InferM (Maybe Newtype)
|
||||
lookupNewtype x = fmap (fmap snd . Map.lookup x) getNewtypes
|
||||
lookupNewtype x = Map.lookup x <$> getNewtypes
|
||||
|
||||
lookupAbstractType :: Name -> InferM (Maybe AbstractType)
|
||||
lookupAbstractType x = fmap (fmap snd . Map.lookup x) getAbstractTypes
|
||||
lookupAbstractType x = Map.lookup x <$> getAbstractTypes
|
||||
|
||||
-- | Lookup the kind of a parameter type
|
||||
lookupParamType :: Name -> InferM (Maybe ModTParam)
|
||||
@ -693,28 +700,28 @@ existVar x k =
|
||||
|
||||
|
||||
-- | Returns the type synonyms that are currently in scope.
|
||||
getTSyns :: InferM (Map Name (DefLoc,TySyn))
|
||||
getTSyns = IM $ asks iTSyns
|
||||
getTSyns :: InferM (Map Name TySyn)
|
||||
getTSyns = getScope mTySyns
|
||||
|
||||
-- | Returns the newtype declarations that are in scope.
|
||||
getNewtypes :: InferM (Map Name (DefLoc,Newtype))
|
||||
getNewtypes = IM $ asks iNewtypes
|
||||
getNewtypes :: InferM (Map Name Newtype)
|
||||
getNewtypes = getScope mNewtypes
|
||||
|
||||
-- | Returns the abstract type declarations that are in scope.
|
||||
getAbstractTypes :: InferM (Map Name (DefLoc,AbstractType))
|
||||
getAbstractTypes = IM $ asks iAbstractTypes
|
||||
getAbstractTypes :: InferM (Map Name AbstractType)
|
||||
getAbstractTypes = getScope mPrimTypes
|
||||
|
||||
-- | Returns the parameter functions declarations
|
||||
getParamFuns :: InferM (Map Name ModVParam)
|
||||
getParamFuns = IM $ asks iParamFuns
|
||||
getParamFuns = getScope mParamFuns
|
||||
|
||||
-- | Returns the abstract function declarations
|
||||
getParamTypes :: InferM (Map Name ModTParam)
|
||||
getParamTypes = IM $ asks iParamTypes
|
||||
getParamTypes = getScope mParamTypes
|
||||
|
||||
-- | Constraints on the module's parameters.
|
||||
getParamConstraints :: InferM [Located Prop]
|
||||
getParamConstraints = IM $ asks iParamConstraints
|
||||
getParamConstraints = getScope mParamConstraints
|
||||
|
||||
-- | Get the set of bound type variables that are in scope.
|
||||
getTVars :: InferM (Set Name)
|
||||
@ -724,8 +731,8 @@ getTVars = IM $ asks $ Set.fromList . mapMaybe tpName . iTVars
|
||||
getBoundInScope :: InferM (Set TParam)
|
||||
getBoundInScope =
|
||||
do ro <- IM ask
|
||||
let params = Set.fromList (map mtpParam (Map.elems (iParamTypes ro)))
|
||||
bound = Set.fromList (iTVars ro)
|
||||
params <- Set.fromList . map mtpParam . Map.elems <$> getParamTypes
|
||||
let bound = Set.fromList (iTVars ro)
|
||||
return $! Set.union params bound
|
||||
|
||||
-- | Retrieve the value of the `mono-binds` option.
|
||||
@ -740,12 +747,14 @@ because it is confusing. As a bonus, in the implementation we don't
|
||||
need to worry about where we lookup things (i.e., in the variable or
|
||||
type synonym environment. -}
|
||||
|
||||
-- XXX: this should be done in renamer
|
||||
checkTShadowing :: String -> Name -> InferM ()
|
||||
checkTShadowing this new =
|
||||
do ro <- IM ask
|
||||
do tsyns <- getTSyns
|
||||
ro <- IM ask
|
||||
rw <- IM get
|
||||
let shadowed =
|
||||
do _ <- Map.lookup new (iTSyns ro)
|
||||
do _ <- Map.lookup new tsyns
|
||||
return "type synonym"
|
||||
`mplus`
|
||||
do guard (new `elem` mapMaybe tpName (iTVars ro))
|
||||
@ -760,7 +769,6 @@ checkTShadowing this new =
|
||||
recordError (TypeShadowing this new that)
|
||||
|
||||
|
||||
|
||||
-- | The sub-computation is performed with the given type parameter in scope.
|
||||
withTParam :: TParam -> InferM a -> InferM a
|
||||
withTParam p (IM m) =
|
||||
@ -772,31 +780,148 @@ withTParam p (IM m) =
|
||||
withTParams :: [TParam] -> InferM a -> InferM a
|
||||
withTParams ps m = foldr withTParam m ps
|
||||
|
||||
|
||||
-- | Execute the given computation in a new top scope.
|
||||
-- The sub-computation would typically be validating a module.
|
||||
newScope :: ScopeName -> InferM ()
|
||||
newScope nm = IM $ sets_ \rw -> rw { iScope = emptyModule nm : iScope rw }
|
||||
|
||||
newLocalScope :: InferM ()
|
||||
newLocalScope = newScope LocalScope
|
||||
|
||||
newSubmoduleScope :: Name -> [Import] -> ExportSpec Name -> InferM ()
|
||||
newSubmoduleScope x is e =
|
||||
do newScope (SubModule x)
|
||||
updScope \m -> m { mImports = is, mExports = e }
|
||||
|
||||
newModuleScope :: P.ModName -> [Import] -> ExportSpec Name -> InferM ()
|
||||
newModuleScope x is e =
|
||||
do newScope (MTopModule x)
|
||||
updScope \m -> m { mImports = is, mExports = e }
|
||||
|
||||
-- | Update the current scope (first in the list). Assumes there is one.
|
||||
updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
|
||||
updScope f = IM $ sets_ \rw -> rw { iScope = upd (iScope rw) }
|
||||
where
|
||||
upd r =
|
||||
case r of
|
||||
[] -> panic "updTopScope" [ "No top scope" ]
|
||||
s : more -> f s : more
|
||||
|
||||
endLocalScope :: InferM [DeclGroup]
|
||||
endLocalScope =
|
||||
IM $ sets \rw ->
|
||||
case iScope rw of
|
||||
x : xs | LocalScope <- mName x ->
|
||||
(reverse (mDecls x), rw { iScope = xs })
|
||||
-- ^ This ignores local type synonyms... Where should we put them?
|
||||
|
||||
_ -> panic "endLocalScope" ["Missing local scope"]
|
||||
|
||||
endSubmodule :: InferM ()
|
||||
endSubmodule =
|
||||
IM $ sets_ \rw ->
|
||||
case iScope rw of
|
||||
x@Module { mName = SubModule m } : y : more -> rw { iScope = z : more }
|
||||
where
|
||||
x1 = x { mName = m }
|
||||
iface = genIface x1
|
||||
me = if isParametrizedModule x1 then Map.singleton m x1 else mempty
|
||||
z = y { mImports = mImports x ++ mImports y -- just for deps
|
||||
, mSubModules = Map.insert m iface (mSubModules y)
|
||||
|
||||
, mTySyns = mTySyns x <> mTySyns y
|
||||
, mNewtypes = mNewtypes x <> mNewtypes y
|
||||
, mPrimTypes = mPrimTypes x <> mPrimTypes y
|
||||
, mDecls = mDecls x <> mDecls y
|
||||
, mFunctors = me <> mFunctors x <> mFunctors y
|
||||
}
|
||||
|
||||
_ -> panic "endSubmodule" [ "Not a submodule" ]
|
||||
|
||||
|
||||
endModule :: InferM Module
|
||||
endModule =
|
||||
IM $ sets \rw ->
|
||||
case iScope rw of
|
||||
[ x ] | MTopModule m <- mName x ->
|
||||
( x { mName = m, mDecls = reverse (mDecls x) }
|
||||
, rw { iScope = [] }
|
||||
)
|
||||
_ -> panic "endModule" [ "Not a single top module" ]
|
||||
|
||||
endModuleInstance :: InferM ()
|
||||
endModuleInstance =
|
||||
IM $ sets_ \rw ->
|
||||
case iScope rw of
|
||||
[ x ] | MTopModule _ <- mName x -> rw { iScope = [] }
|
||||
_ -> panic "endModuleInstance" [ "Not single top module" ]
|
||||
|
||||
|
||||
-- | Get an environment combining all nested scopes.
|
||||
getScope :: Semigroup a => (ModuleG ScopeName -> a) -> InferM a
|
||||
getScope f =
|
||||
do ro <- IM ask
|
||||
rw <- IM get
|
||||
pure (sconcat (f (iExtScope ro) :| map f (iScope rw)))
|
||||
|
||||
addDecls :: DeclGroup -> InferM ()
|
||||
addDecls ds =
|
||||
do updScope \r -> r { mDecls = ds : mDecls r }
|
||||
IM $ sets_ \rw -> rw { iBindTypes = new rw }
|
||||
where
|
||||
add d = Map.insert (dName d) (dSignature d)
|
||||
new rw = foldr add (iBindTypes rw) (groupDecls ds)
|
||||
|
||||
-- | The sub-computation is performed with the given type-synonym in scope.
|
||||
withTySyn :: TySyn -> InferM a -> InferM a
|
||||
withTySyn t (IM m) =
|
||||
addTySyn :: TySyn -> InferM ()
|
||||
addTySyn t =
|
||||
do let x = tsName t
|
||||
checkTShadowing "synonym" x
|
||||
IM $ mapReader (\r -> r { iTSyns = Map.insert x (IsLocal,t) (iTSyns r) }) m
|
||||
updScope \r -> r { mTySyns = Map.insert x t (mTySyns r) }
|
||||
|
||||
withNewtype :: Newtype -> InferM a -> InferM a
|
||||
withNewtype t (IM m) =
|
||||
IM $ mapReader
|
||||
(\r -> r { iNewtypes = Map.insert (ntName t) (IsLocal,t)
|
||||
(iNewtypes r) }) m
|
||||
addNewtype :: Newtype -> InferM ()
|
||||
addNewtype t =
|
||||
do updScope \r -> r { mNewtypes = Map.insert (ntName t) t (mNewtypes r) }
|
||||
IM $ sets_ \rw -> rw { iBindTypes = Map.insert (ntName t)
|
||||
(newtypeConType t)
|
||||
(iBindTypes rw) }
|
||||
|
||||
withPrimType :: AbstractType -> InferM a -> InferM a
|
||||
withPrimType t (IM m) =
|
||||
IM $ mapReader
|
||||
(\r -> r { iAbstractTypes = Map.insert (atName t) (IsLocal,t)
|
||||
(iAbstractTypes r) }) m
|
||||
addPrimType :: AbstractType -> InferM ()
|
||||
addPrimType t =
|
||||
updScope \r ->
|
||||
r { mPrimTypes = Map.insert (atName t) t (mPrimTypes r) }
|
||||
|
||||
addParamType :: ModTParam -> InferM ()
|
||||
addParamType a =
|
||||
updScope \r -> r { mParamTypes = Map.insert (mtpName a) a (mParamTypes r) }
|
||||
|
||||
-- | The sub-computation is performed with the given abstract function in scope.
|
||||
addParamFun :: ModVParam -> InferM ()
|
||||
addParamFun x =
|
||||
do updScope \r -> r { mParamFuns = Map.insert (mvpName x) x (mParamFuns r) }
|
||||
IM $ sets_ \rw -> rw { iBindTypes = Map.insert (mvpName x) (mvpType x)
|
||||
(iBindTypes rw) }
|
||||
|
||||
-- | Add some assumptions for an entire module
|
||||
addParameterConstraints :: [Located Prop] -> InferM ()
|
||||
addParameterConstraints ps =
|
||||
updScope \r -> r { mParamConstraints = ps ++ mParamConstraints r }
|
||||
|
||||
|
||||
withParamType :: ModTParam -> InferM a -> InferM a
|
||||
withParamType a (IM m) =
|
||||
IM $ mapReader
|
||||
(\r -> r { iParamTypes = Map.insert (mtpName a) a (iParamTypes r) })
|
||||
m
|
||||
|
||||
|
||||
-- | Perform the given computation in a new scope (i.e., the subcomputation
|
||||
-- may use existential type variables). This is a different kind of scope
|
||||
-- from the nested modules one.
|
||||
inNewScope :: InferM a -> InferM a
|
||||
inNewScope m =
|
||||
do curScopes <- iExistTVars <$> IM get
|
||||
IM $ sets_ $ \s -> s { iExistTVars = Map.empty : curScopes }
|
||||
a <- m
|
||||
IM $ sets_ $ \s -> s { iExistTVars = curScopes }
|
||||
return a
|
||||
|
||||
|
||||
-- | The sub-computation is performed with the given variable in scope.
|
||||
withVarType :: Name -> VarType -> InferM a -> InferM a
|
||||
@ -809,19 +934,6 @@ withVarTypes xs m = foldr (uncurry withVarType) m xs
|
||||
withVar :: Name -> Schema -> InferM a -> InferM a
|
||||
withVar x s = withVarType x (ExtVar s)
|
||||
|
||||
-- | The sub-computation is performed with the given abstract function in scope.
|
||||
withParamFuns :: [ModVParam] -> InferM a -> InferM a
|
||||
withParamFuns xs (IM m) =
|
||||
IM $ mapReader (\r -> r { iParamFuns = foldr add (iParamFuns r) xs }) m
|
||||
where
|
||||
add x = Map.insert (mvpName x) x
|
||||
|
||||
-- | Add some assumptions for an entire module
|
||||
withParameterConstraints :: [Located Prop] -> InferM a -> InferM a
|
||||
withParameterConstraints ps (IM m) =
|
||||
IM $ mapReader (\r -> r { iParamConstraints = ps ++ iParamConstraints r }) m
|
||||
|
||||
|
||||
-- | The sub-computation is performed with the given variables in scope.
|
||||
withMonoType :: (Name,Located Type) -> InferM a -> InferM a
|
||||
withMonoType (x,lt) = withVar x (Forall [] [] (thing lt))
|
||||
@ -830,25 +942,6 @@ withMonoType (x,lt) = withVar x (Forall [] [] (thing lt))
|
||||
withMonoTypes :: Map Name (Located Type) -> InferM a -> InferM a
|
||||
withMonoTypes xs m = foldr withMonoType m (Map.toList xs)
|
||||
|
||||
-- | The sub-computation is performed with the given type synonyms
|
||||
-- and variables in scope.
|
||||
withDecls :: ([TySyn], Map Name Schema) -> InferM a -> InferM a
|
||||
withDecls (ts,vs) m = foldr withTySyn (foldr add m (Map.toList vs)) ts
|
||||
where
|
||||
add (x,t) = withVar x t
|
||||
|
||||
-- | Perform the given computation in a new scope (i.e., the subcomputation
|
||||
-- may use existential type variables).
|
||||
inNewScope :: InferM a -> InferM a
|
||||
inNewScope m =
|
||||
do curScopes <- iExistTVars <$> IM get
|
||||
IM $ sets_ $ \s -> s { iExistTVars = Map.empty : curScopes }
|
||||
a <- m
|
||||
IM $ sets_ $ \s -> s { iExistTVars = curScopes }
|
||||
return a
|
||||
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Kind checking
|
||||
|
||||
|
@ -15,7 +15,7 @@ import Cryptol.TypeCheck.Monad( InferM, unify, newGoals
|
||||
, newParamName
|
||||
)
|
||||
import Cryptol.TypeCheck.Subst (listParamSubst, apSubst)
|
||||
import Cryptol.Utils.Ident (Ident, packIdent)
|
||||
import Cryptol.Utils.Ident (Ident, packIdent,Namespace(..))
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.RecordMap
|
||||
|
||||
@ -163,9 +163,9 @@ mkSelSln s outerT innerT =
|
||||
-- xs.s ~~> [ x.s | x <- xs ]
|
||||
-- { xs | s = ys } ~~> [ { x | s = y } | x <- xs | y <- ys ]
|
||||
liftSeq len el =
|
||||
do x1 <- newParamName (packIdent "x")
|
||||
x2 <- newParamName (packIdent "x")
|
||||
y2 <- newParamName (packIdent "y")
|
||||
do x1 <- newParamName NSValue (packIdent "x")
|
||||
x2 <- newParamName NSValue (packIdent "x")
|
||||
y2 <- newParamName NSValue (packIdent "y")
|
||||
case tNoUser innerT of
|
||||
TCon _ [_,eli] ->
|
||||
do d <- mkSelSln s el eli
|
||||
@ -187,8 +187,8 @@ mkSelSln s outerT innerT =
|
||||
-- f.s ~~> \x -> (f x).s
|
||||
-- { f | s = g } ~~> \x -> { f x | s = g x }
|
||||
liftFun t1 t2 =
|
||||
do x1 <- newParamName (packIdent "x")
|
||||
x2 <- newParamName (packIdent "x")
|
||||
do x1 <- newParamName NSValue (packIdent "x")
|
||||
x2 <- newParamName NSValue (packIdent "x")
|
||||
case tNoUser innerT of
|
||||
TCon _ [_,inT] ->
|
||||
do d <- mkSelSln s t2 inT
|
||||
|
@ -41,9 +41,9 @@ builtInType :: M.Name -> Maybe TCon
|
||||
builtInType nm =
|
||||
case M.nameInfo nm of
|
||||
M.Declared m _
|
||||
| m == preludeName -> Map.lookup (M.nameIdent nm) builtInTypes
|
||||
| m == floatName -> Map.lookup (M.nameIdent nm) builtInFloat
|
||||
| m == arrayName -> Map.lookup (M.nameIdent nm) builtInArray
|
||||
| m == M.TopModule preludeName -> Map.lookup (M.nameIdent nm) builtInTypes
|
||||
| m == M.TopModule floatName -> Map.lookup (M.nameIdent nm) builtInFloat
|
||||
| m == M.TopModule arrayName -> Map.lookup (M.nameIdent nm) builtInArray
|
||||
_ -> Nothing
|
||||
|
||||
where
|
||||
|
@ -2,6 +2,11 @@
|
||||
{-# Language FlexibleInstances, FlexibleContexts #-}
|
||||
{-# Language PatternGuards #-}
|
||||
{-# Language OverloadedStrings #-}
|
||||
{-| This module contains types related to typechecking and the output of the
|
||||
typechecker. In particular, it should contain the types needed by
|
||||
interface files (see 'Crytpol.ModuleSystem.Interface'), which are (kind of)
|
||||
the output of the typechker.
|
||||
-}
|
||||
module Cryptol.TypeCheck.Type
|
||||
( module Cryptol.TypeCheck.Type
|
||||
, module Cryptol.TypeCheck.TCon
|
||||
@ -32,6 +37,38 @@ import Prelude
|
||||
infix 4 =#=, >==
|
||||
infixr 5 `tFun`
|
||||
|
||||
-- | A type parameter of a module.
|
||||
data ModTParam = ModTParam
|
||||
{ mtpName :: Name
|
||||
, mtpKind :: Kind
|
||||
, mtpNumber :: !Int -- ^ The number of the parameter in the module
|
||||
-- This is used when we move parameters from the module
|
||||
-- level to individual declarations
|
||||
-- (type synonyms in particular)
|
||||
, mtpDoc :: Maybe Text
|
||||
} deriving (Show,Generic,NFData)
|
||||
|
||||
|
||||
mtpParam :: ModTParam -> TParam
|
||||
mtpParam mtp = TParam { tpUnique = nameUnique (mtpName mtp)
|
||||
, tpKind = mtpKind mtp
|
||||
, tpFlav = TPModParam (mtpName mtp)
|
||||
, tpInfo = desc
|
||||
}
|
||||
where desc = TVarInfo { tvarDesc = TVFromModParam (mtpName mtp)
|
||||
, tvarSource = nameLoc (mtpName mtp)
|
||||
}
|
||||
|
||||
-- | A value parameter of a module.
|
||||
data ModVParam = ModVParam
|
||||
{ mvpName :: Name
|
||||
, mvpType :: Schema
|
||||
, mvpDoc :: Maybe Text
|
||||
, mvpFixity :: Maybe Fixity
|
||||
} deriving (Show,Generic,NFData)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
-- | The types of polymorphic values.
|
||||
@ -957,9 +994,8 @@ instance PP (WithNames Type) where
|
||||
|
||||
TUser c ts t ->
|
||||
withNameDisp $ \disp ->
|
||||
case nameInfo c of
|
||||
Declared m _
|
||||
| NotInScope <- getNameFormat m (nameIdent c) disp ->
|
||||
case asOrigName c of
|
||||
Just og | NotInScope <- getNameFormat og disp ->
|
||||
go prec t -- unfold type synonym if not in scope
|
||||
_ ->
|
||||
case ts of
|
||||
@ -1076,7 +1112,7 @@ pickTVarName k src uni =
|
||||
TypeParamInstPos f n -> mk (sh f ++ "_" ++ show n)
|
||||
DefinitionOf x ->
|
||||
case nameInfo x of
|
||||
Declared m SystemName | m == exprModName -> mk "it"
|
||||
Declared m SystemName | m == TopModule exprModName -> mk "it"
|
||||
_ -> using x
|
||||
LenOfCompGen -> mk "n"
|
||||
GeneratorOfListComp -> "seq"
|
||||
|
@ -7,10 +7,16 @@
|
||||
-- Portability : portable
|
||||
|
||||
{-# LANGUAGE DeriveGeneric, OverloadedStrings #-}
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
|
||||
module Cryptol.Utils.Ident
|
||||
( -- * Module names
|
||||
ModName
|
||||
ModPath(..)
|
||||
, apPathRoot
|
||||
, containsModule
|
||||
, topModuleFor
|
||||
|
||||
, ModName
|
||||
, modNameToText
|
||||
, textToModName
|
||||
, modNameChunks
|
||||
@ -41,6 +47,13 @@ module Cryptol.Utils.Ident
|
||||
, identText
|
||||
, modParamIdent
|
||||
|
||||
-- * Namespaces
|
||||
, Namespace(..)
|
||||
, allNamespaces
|
||||
|
||||
-- * Original names
|
||||
, OrigName(..)
|
||||
|
||||
-- * Identifiers for primitives
|
||||
, PrimIdent(..)
|
||||
, prelPrim
|
||||
@ -52,13 +65,54 @@ module Cryptol.Utils.Ident
|
||||
|
||||
import Control.DeepSeq (NFData)
|
||||
import Data.Char (isSpace)
|
||||
import Data.List (unfoldr)
|
||||
import Data.List (unfoldr,isPrefixOf)
|
||||
import qualified Data.Text as T
|
||||
import Data.String (IsString(..))
|
||||
import GHC.Generics (Generic)
|
||||
|
||||
|
||||
-- | Module names are just text.
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- | Namespaces for names
|
||||
data Namespace = NSValue | NSType | NSModule
|
||||
deriving (Generic,Show,NFData,Eq,Ord,Enum,Bounded)
|
||||
|
||||
allNamespaces :: [Namespace]
|
||||
allNamespaces = [ minBound .. maxBound ]
|
||||
|
||||
-- | Idnetifies a possibly nested module
|
||||
data ModPath = TopModule ModName
|
||||
| Nested ModPath Ident
|
||||
deriving (Eq,Ord,Show,Generic,NFData)
|
||||
|
||||
apPathRoot :: (ModName -> ModName) -> ModPath -> ModPath
|
||||
apPathRoot f path =
|
||||
case path of
|
||||
TopModule m -> TopModule (f m)
|
||||
Nested p q -> Nested (apPathRoot f p) q
|
||||
|
||||
topModuleFor :: ModPath -> ModName
|
||||
topModuleFor m =
|
||||
case m of
|
||||
TopModule x -> x
|
||||
Nested p _ -> topModuleFor p
|
||||
|
||||
containsModule :: ModPath -> ModPath -> Bool
|
||||
p1 `containsModule` p2 = m1 == m2 && reverse xs `isPrefixOf` reverse ys
|
||||
where
|
||||
(m1,xs) = toList p1
|
||||
(m2,ys) = toList p2
|
||||
|
||||
toList p =
|
||||
case p of
|
||||
TopModule a -> (a, [])
|
||||
Nested b i -> (a, i:bs)
|
||||
where (a,bs) = toList b
|
||||
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- | Top-level Module names are just text.
|
||||
data ModName = ModName T.Text
|
||||
deriving (Eq,Ord,Show,Generic)
|
||||
|
||||
@ -137,6 +191,15 @@ exprModName :: ModName
|
||||
exprModName = packModName ["<expr>"]
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- | Identifies an entitiy
|
||||
data OrigName = OrigName
|
||||
{ ogNamespace :: Namespace
|
||||
, ogModule :: ModPath
|
||||
, ogName :: Ident
|
||||
} deriving (Eq,Ord,Show,Generic,NFData)
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- | Identifiers, along with a flag that indicates whether or not they're infix
|
||||
|
@ -66,14 +66,14 @@ Getting a value of 'Nothing' from the NameDisp function indicates
|
||||
that the display has no opinion on how this name should be displayed,
|
||||
and some other display should be tried out. -}
|
||||
data NameDisp = EmptyNameDisp
|
||||
| NameDisp (ModName -> Ident -> Maybe NameFormat)
|
||||
| NameDisp (OrigName -> Maybe NameFormat)
|
||||
deriving (Generic, NFData)
|
||||
|
||||
instance Show NameDisp where
|
||||
show _ = "<NameDisp>"
|
||||
|
||||
instance S.Semigroup NameDisp where
|
||||
NameDisp f <> NameDisp g = NameDisp (\m n -> f m n `mplus` g m n)
|
||||
NameDisp f <> NameDisp g = NameDisp (\n -> f n `mplus` g n)
|
||||
EmptyNameDisp <> EmptyNameDisp = EmptyNameDisp
|
||||
EmptyNameDisp <> x = x
|
||||
x <> _ = x
|
||||
@ -88,21 +88,13 @@ data NameFormat = UnQualified
|
||||
deriving (Show)
|
||||
|
||||
-- | Never qualify names from this module.
|
||||
neverQualifyMod :: ModName -> NameDisp
|
||||
neverQualifyMod mn = NameDisp $ \ mn' _ ->
|
||||
if mn == mn' then Just UnQualified
|
||||
else Nothing
|
||||
|
||||
alwaysQualify :: NameDisp
|
||||
alwaysQualify = NameDisp $ \ mn _ -> Just (Qualified mn)
|
||||
neverQualifyMod :: ModPath -> NameDisp
|
||||
neverQualifyMod mn = NameDisp $ \n ->
|
||||
if ogModule n == mn then Just UnQualified else Nothing
|
||||
|
||||
neverQualify :: NameDisp
|
||||
neverQualify = NameDisp $ \ _ _ -> Just UnQualified
|
||||
neverQualify = NameDisp $ \ _ -> Just UnQualified
|
||||
|
||||
fmtModName :: ModName -> NameFormat -> T.Text
|
||||
fmtModName _ UnQualified = T.empty
|
||||
fmtModName _ (Qualified mn) = modNameToText mn
|
||||
fmtModName mn NotInScope = modNameToText mn
|
||||
|
||||
-- | Compose two naming environments, preferring names from the left
|
||||
-- environment.
|
||||
@ -111,9 +103,9 @@ extend = mappend
|
||||
|
||||
-- | Get the format for a name. When 'Nothing' is returned, the name is not
|
||||
-- currently in scope.
|
||||
getNameFormat :: ModName -> Ident -> NameDisp -> NameFormat
|
||||
getNameFormat m i (NameDisp f) = fromMaybe NotInScope (f m i)
|
||||
getNameFormat _ _ EmptyNameDisp = NotInScope
|
||||
getNameFormat :: OrigName -> NameDisp -> NameFormat
|
||||
getNameFormat m (NameDisp f) = fromMaybe NotInScope (f m)
|
||||
getNameFormat _ EmptyNameDisp = NotInScope
|
||||
|
||||
-- | Produce a document in the context of the current 'NameDisp'.
|
||||
withNameDisp :: (NameDisp -> Doc) -> Doc
|
||||
@ -163,6 +155,11 @@ class PP a => PPName a where
|
||||
-- | Print a name as an infix operator: @a + b@
|
||||
ppInfixName :: a -> Doc
|
||||
|
||||
instance PPName ModName where
|
||||
ppNameFixity _ = Nothing
|
||||
ppPrefixName = pp
|
||||
ppInfixName = pp
|
||||
|
||||
pp :: PP a => a -> Doc
|
||||
pp = ppPrec 0
|
||||
|
||||
@ -325,6 +322,7 @@ instance PP Ident where
|
||||
instance PP ModName where
|
||||
ppPrec _ = text . T.unpack . modNameToText
|
||||
|
||||
|
||||
instance PP Assoc where
|
||||
ppPrec _ LeftAssoc = text "left-associative"
|
||||
ppPrec _ RightAssoc = text "right-associative"
|
||||
@ -333,3 +331,31 @@ instance PP Assoc where
|
||||
instance PP Fixity where
|
||||
ppPrec _ (Fixity assoc level) =
|
||||
text "precedence" <+> int level <.> comma <+> pp assoc
|
||||
|
||||
instance PP ModPath where
|
||||
ppPrec _ p =
|
||||
case p of
|
||||
TopModule m -> pp m
|
||||
Nested q t -> pp q <.> "::" <.> pp t
|
||||
|
||||
instance PP OrigName where
|
||||
ppPrec _ og =
|
||||
withNameDisp $ \disp ->
|
||||
case getNameFormat og disp of
|
||||
UnQualified -> pp (ogName og)
|
||||
Qualified m -> ppQual (TopModule m) (pp (ogName og))
|
||||
NotInScope -> ppQual (ogModule og) (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)
|
||||
|
||||
instance PP Namespace where
|
||||
ppPrec _ ns =
|
||||
case ns of
|
||||
NSValue -> "/*value*/"
|
||||
NSType -> "/*type*/"
|
||||
NSModule -> "/*module*/"
|
||||
|
@ -5,15 +5,15 @@ Loading module Cryptol
|
||||
Loading module AES
|
||||
Loading module Cryptol
|
||||
Loading module ChaCha20
|
||||
[warning] at ChaChaPolyCryptolIETF.md:340:32--340:33 Unused name: b
|
||||
[warning] at ChaChaPolyCryptolIETF.md:2117:20--2117:21
|
||||
Unused name: b
|
||||
[warning] at ChaChaPolyCryptolIETF.md:1984:5--1984:15
|
||||
This binding for `cypherText` shadows the existing binding at
|
||||
ChaChaPolyCryptolIETF.md:1982:24--1982:34
|
||||
[warning] at ChaChaPolyCryptolIETF.md:2062:20--2062:27
|
||||
This binding for `AeadAAD` shadows the existing binding at
|
||||
ChaChaPolyCryptolIETF.md:1149:1--1149:8
|
||||
[warning] at ChaChaPolyCryptolIETF.md:340:32--340:33 Unused name: b
|
||||
[warning] at ChaChaPolyCryptolIETF.md:2117:20--2117:21
|
||||
Unused name: b
|
||||
Loading module Cryptol
|
||||
Loading module Cipher
|
||||
Loading module Cryptol
|
||||
|
@ -2,6 +2,5 @@ Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module binarytree
|
||||
|
||||
[error] at issue1040.cry:1:1--6:36:
|
||||
Recursive type declarations:
|
||||
`binarytree::Tree`
|
||||
[error] Invalid recursive dependency:
|
||||
• type binarytree::Tree
|
||||
|
@ -11,12 +11,12 @@ Loading module Cryptol
|
||||
This binding for `x` shadows the existing binding at
|
||||
issue567.icry:3:6--3:7
|
||||
(\(x, y) x -> x) : {a, b, c} (a, b) -> c -> c
|
||||
[warning] at issue567.icry:4:16--4:17
|
||||
This binding for `y` shadows the existing binding at
|
||||
issue567.icry:4:9--4:10
|
||||
[warning] at issue567.icry:4:13--4:14
|
||||
This binding for `x` shadows the existing binding at
|
||||
issue567.icry:4:6--4:7
|
||||
[warning] at issue567.icry:4:16--4:17
|
||||
This binding for `y` shadows the existing binding at
|
||||
issue567.icry:4:9--4:10
|
||||
(\(x, y) (x, y) -> x) : {a, b, c, d} (a, b) -> (c, d) -> c
|
||||
[warning] at issue567.icry:5:8--5:9
|
||||
This binding for `x` shadows the existing binding at
|
||||
|
@ -4,7 +4,7 @@ Loading module Main
|
||||
|
||||
[error] at issue723.cry:7:5--7:19:
|
||||
Failed to validate user-specified signature.
|
||||
in the definition of 'Main::g', at issue723.cry:7:5--7:6,
|
||||
in the definition of 'g', at issue723.cry:7:5--7:6,
|
||||
we need to show that
|
||||
for any type k
|
||||
assuming
|
||||
|
6
tests/modsys/nested/T1.cry
Normal file
6
tests/modsys/nested/T1.cry
Normal file
@ -0,0 +1,6 @@
|
||||
module T1 where
|
||||
|
||||
submodule A where
|
||||
x = 0x02
|
||||
|
||||
y = x
|
1
tests/modsys/nested/T1.icry
Normal file
1
tests/modsys/nested/T1.icry
Normal file
@ -0,0 +1 @@
|
||||
:load T1.cry
|
5
tests/modsys/nested/T1.icry.stdout
Normal file
5
tests/modsys/nested/T1.icry.stdout
Normal file
@ -0,0 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T1
|
||||
|
||||
[error] at T1.cry:6:5--6:6 Value not in scope: x
|
8
tests/modsys/nested/T2.cry
Normal file
8
tests/modsys/nested/T2.cry
Normal file
@ -0,0 +1,8 @@
|
||||
module T1 where
|
||||
|
||||
submodule A where
|
||||
x = 0x02
|
||||
|
||||
import submodule A
|
||||
|
||||
y = x
|
5
tests/modsys/nested/T2.icry
Normal file
5
tests/modsys/nested/T2.icry
Normal file
@ -0,0 +1,5 @@
|
||||
:load T2.icry
|
||||
:t x
|
||||
:t y
|
||||
x
|
||||
y
|
13
tests/modsys/nested/T2.icry.stdout
Normal file
13
tests/modsys/nested/T2.icry.stdout
Normal file
@ -0,0 +1,13 @@
|
||||
Loading module Cryptol
|
||||
|
||||
Parse error at T2.icry:1:1,
|
||||
unexpected: :
|
||||
expected: a declaration
|
||||
|
||||
[error] at T2.icry:2:4--2:5 Value not in scope: x
|
||||
|
||||
[error] at T2.icry:3:4--3:5 Value not in scope: y
|
||||
|
||||
[error] at T2.icry:4:1--4:2 Value not in scope: x
|
||||
|
||||
[error] at T2.icry:5:1--5:2 Value not in scope: y
|
11
tests/modsys/nested/T3.cry
Normal file
11
tests/modsys/nested/T3.cry
Normal file
@ -0,0 +1,11 @@
|
||||
module T3 where
|
||||
|
||||
import submodule A
|
||||
x = y
|
||||
|
||||
submodule A where
|
||||
y = x
|
||||
|
||||
|
||||
|
||||
|
1
tests/modsys/nested/T3.icry
Normal file
1
tests/modsys/nested/T3.icry
Normal file
@ -0,0 +1 @@
|
||||
:load T3.cry
|
7
tests/modsys/nested/T3.icry.stdout
Normal file
7
tests/modsys/nested/T3.icry.stdout
Normal file
@ -0,0 +1,7 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T3
|
||||
|
||||
[error] Invalid recursive dependency:
|
||||
• T3::x
|
||||
• submodule T3::A
|
11
tests/modsys/nested/T4.cry
Normal file
11
tests/modsys/nested/T4.cry
Normal file
@ -0,0 +1,11 @@
|
||||
module T4 where
|
||||
|
||||
x = 0x02
|
||||
|
||||
submodule A where
|
||||
y = x
|
||||
|
||||
import submodule A
|
||||
|
||||
z = y
|
||||
|
4
tests/modsys/nested/T4.icry
Normal file
4
tests/modsys/nested/T4.icry
Normal file
@ -0,0 +1,4 @@
|
||||
:load T4.cry
|
||||
x
|
||||
y
|
||||
z
|
6
tests/modsys/nested/T4.icry.stdout
Normal file
6
tests/modsys/nested/T4.icry.stdout
Normal file
@ -0,0 +1,6 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T4
|
||||
0x02
|
||||
0x02
|
||||
0x02
|
7
tests/modsys/nested/T5.cry
Normal file
7
tests/modsys/nested/T5.cry
Normal file
@ -0,0 +1,7 @@
|
||||
module T5 where
|
||||
|
||||
import T4
|
||||
|
||||
import submodule A
|
||||
|
||||
a = x
|
4
tests/modsys/nested/T5.icry
Normal file
4
tests/modsys/nested/T5.icry
Normal file
@ -0,0 +1,4 @@
|
||||
:load T5.cry
|
||||
a
|
||||
:browse T4
|
||||
:browse T5
|
30
tests/modsys/nested/T5.icry.stdout
Normal file
30
tests/modsys/nested/T5.icry.stdout
Normal file
@ -0,0 +1,30 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T4
|
||||
Loading module T5
|
||||
0x02
|
||||
Modules
|
||||
=======
|
||||
|
||||
From T4
|
||||
-------
|
||||
|
||||
A
|
||||
|
||||
Symbols
|
||||
=======
|
||||
|
||||
From T4
|
||||
-------
|
||||
|
||||
x : [8]
|
||||
z : [8]
|
||||
|
||||
Symbols
|
||||
=======
|
||||
|
||||
Public
|
||||
------
|
||||
|
||||
a : [8]
|
||||
|
7
tests/modsys/nested/T6.cry
Normal file
7
tests/modsys/nested/T6.cry
Normal file
@ -0,0 +1,7 @@
|
||||
module T6 where
|
||||
|
||||
import T4 as X
|
||||
|
||||
import submodule X::A
|
||||
|
||||
|
3
tests/modsys/nested/T6.icry
Normal file
3
tests/modsys/nested/T6.icry
Normal file
@ -0,0 +1,3 @@
|
||||
:load T6.cry
|
||||
:browse T6
|
||||
:browse T4
|
21
tests/modsys/nested/T6.icry.stdout
Normal file
21
tests/modsys/nested/T6.icry.stdout
Normal file
@ -0,0 +1,21 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T4
|
||||
Loading module T6
|
||||
Modules
|
||||
=======
|
||||
|
||||
From T4
|
||||
-------
|
||||
|
||||
X::A
|
||||
|
||||
Symbols
|
||||
=======
|
||||
|
||||
From T4
|
||||
-------
|
||||
|
||||
X::x : [8]
|
||||
X::z : [8]
|
||||
|
@ -6,11 +6,11 @@ import Cryptol
|
||||
/* Not recursive */
|
||||
test01::a : {n, a} (fin n) => [n]a -> [2 * n]a
|
||||
test01::a = \{n, a} (fin n) (x : [n]a) ->
|
||||
test01::f n x
|
||||
f n x
|
||||
where
|
||||
/* Not recursive */
|
||||
test01::f : {m} [m]a -> [n + m]a
|
||||
test01::f = \{m} (y : [m]a) -> (Cryptol::#) n m a <> x y
|
||||
f : {m} [m]a -> [n + m]a
|
||||
f = \{m} (y : [m]a) -> (Cryptol::#) n m a <> x y
|
||||
|
||||
|
||||
|
||||
@ -21,11 +21,11 @@ import Cryptol
|
||||
/* Not recursive */
|
||||
test01::a : {n, a} (fin n) => [n]a -> [2 * n]a
|
||||
test01::a = \{n, a} (fin n) (x : [n]a) ->
|
||||
test01::f x
|
||||
f x
|
||||
where
|
||||
/* Not recursive */
|
||||
test01::f : [n]a -> [2 * n]a
|
||||
test01::f = \ (y : [n]a) -> (Cryptol::#) n n a <> x y
|
||||
f : [n]a -> [2 * n]a
|
||||
f = \ (y : [n]a) -> (Cryptol::#) n n a <> x y
|
||||
|
||||
|
||||
|
||||
|
@ -6,13 +6,13 @@ import Cryptol
|
||||
/* Not recursive */
|
||||
test02::test : {a, b} a -> b
|
||||
test02::test = \{a, b} (a : a) ->
|
||||
test02::f b a
|
||||
f b a
|
||||
where
|
||||
/* Recursive */
|
||||
test02::f : {c} a -> c
|
||||
test02::f = \{c} (x : a) -> test02::g c a
|
||||
test02::g : {c} a -> c
|
||||
test02::g = \{c} (x : a) -> test02::f c x
|
||||
f : {c} a -> c
|
||||
f = \{c} (x : a) -> g c a
|
||||
g : {c} a -> c
|
||||
g = \{c} (x : a) -> f c x
|
||||
|
||||
|
||||
|
||||
@ -23,13 +23,13 @@ import Cryptol
|
||||
/* Not recursive */
|
||||
test02::test : {a, b} b -> a
|
||||
test02::test = \{a, b} (a : b) ->
|
||||
test02::f a
|
||||
f a
|
||||
where
|
||||
/* Recursive */
|
||||
test02::f : b -> a
|
||||
test02::f = \ (x : b) -> test02::g a
|
||||
test02::g : b -> a
|
||||
test02::g = \ (x : b) -> test02::f x
|
||||
f : b -> a
|
||||
f = \ (x : b) -> g a
|
||||
g : b -> a
|
||||
g = \ (x : b) -> f x
|
||||
|
||||
|
||||
|
||||
|
@ -6,11 +6,11 @@ import Cryptol
|
||||
/* Not recursive */
|
||||
test03::test : {a} (fin a, a >= width a) => [a]
|
||||
test03::test = \{a} (fin a, a >= width a) ->
|
||||
test03::foo [a] <>
|
||||
foo [a] <>
|
||||
where
|
||||
/* Not recursive */
|
||||
test03::foo : {b} (Literal a b) => b
|
||||
test03::foo = \{b} (Literal a b) -> Cryptol::number a b <>
|
||||
foo : {b} (Literal a b) => b
|
||||
foo = \{b} (Literal a b) -> Cryptol::number a b <>
|
||||
|
||||
|
||||
|
||||
@ -21,11 +21,11 @@ import Cryptol
|
||||
/* Not recursive */
|
||||
test03::test : {a} (fin a, a >= width a) => [a]
|
||||
test03::test = \{a} (fin a, a >= width a) ->
|
||||
test03::foo
|
||||
foo
|
||||
where
|
||||
/* Not recursive */
|
||||
test03::foo : [a]
|
||||
test03::foo = Cryptol::number a [a] <>
|
||||
foo : [a]
|
||||
foo = Cryptol::number a [a] <>
|
||||
|
||||
|
||||
|
||||
|
@ -6,18 +6,18 @@ import Cryptol
|
||||
/* Not recursive */
|
||||
test04::test : {a, b} (Literal 10 b) => a -> ((a, ()), (a, b))
|
||||
test04::test = \{a, b} (Literal 10 b) (a : a) ->
|
||||
(test04::f () (), test04::f b (Cryptol::number 10 b <>))
|
||||
(f () (), f b (Cryptol::number 10 b <>))
|
||||
where
|
||||
/* Not recursive */
|
||||
test04::f : {c} c -> (a, c)
|
||||
test04::f = \{c} (x : c) -> (a, x)
|
||||
f : {c} c -> (a, c)
|
||||
f = \{c} (x : c) -> (a, x)
|
||||
|
||||
|
||||
|
||||
Loading module Cryptol
|
||||
Loading module test04
|
||||
|
||||
[error] at test04.cry:1:1--5:14:
|
||||
[error] at test04.cry:3:1--5:14:
|
||||
• `10` is not a valid literal of type `()`
|
||||
arising from
|
||||
use of literal or demoted expression
|
||||
|
@ -19,24 +19,24 @@ test05::test = \{n, a, b} (Zero b, Literal 10 a) (a : [n]b) ->
|
||||
Cryptol::number 10 a <>
|
||||
where
|
||||
/* Not recursive */
|
||||
test05::foo : [10]
|
||||
test05::foo = Cryptol::number 10 [10] <>
|
||||
foo : [10]
|
||||
foo = Cryptol::number 10 [10] <>
|
||||
|
||||
/* Not recursive */
|
||||
test05::f : {m} (fin m) => [n + m]b
|
||||
test05::f = \{m} (fin m) ->
|
||||
test05::bar m <>
|
||||
where
|
||||
/* Not recursive */
|
||||
test05::foo : [n]b
|
||||
test05::foo = a
|
||||
|
||||
/* Not recursive */
|
||||
test05::bar : {i} (fin i) => [i + n]b
|
||||
test05::bar = \{i} (fin i) ->
|
||||
(Cryptol::#) i n b <> (Cryptol::zero ([i]b) <>) test05::foo
|
||||
|
||||
|
||||
f : {m} (fin m) => [n + m]b
|
||||
f = \{m} (fin m) ->
|
||||
bar m <>
|
||||
where
|
||||
/* Not recursive */
|
||||
foo : [n]b
|
||||
foo = a
|
||||
|
||||
/* Not recursive */
|
||||
bar : {i} (fin i) => [i + n]b
|
||||
bar = \{i} (fin i) ->
|
||||
(Cryptol::#) i n b <> (Cryptol::zero ([i]b) <>) foo
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
@ -6,15 +6,15 @@ import Cryptol
|
||||
/* Not recursive */
|
||||
test06::test : {a} (Zero a) => a -> a
|
||||
test06::test = \{a} (Zero a) (a : a) ->
|
||||
test06::bar
|
||||
bar
|
||||
where
|
||||
/* Not recursive */
|
||||
test06::foo : a
|
||||
test06::foo = Cryptol::zero a <>
|
||||
foo : a
|
||||
foo = Cryptol::zero a <>
|
||||
|
||||
/* Not recursive */
|
||||
test06::bar : a
|
||||
test06::bar = test06::foo
|
||||
bar : a
|
||||
bar = foo
|
||||
|
||||
|
||||
|
||||
@ -25,15 +25,15 @@ import Cryptol
|
||||
/* Not recursive */
|
||||
test06::test : {a} (Zero a) => a -> a
|
||||
test06::test = \{a} (Zero a) (a : a) ->
|
||||
test06::bar
|
||||
bar
|
||||
where
|
||||
/* Not recursive */
|
||||
test06::foo : a
|
||||
test06::foo = Cryptol::zero a <>
|
||||
foo : a
|
||||
foo = Cryptol::zero a <>
|
||||
|
||||
/* Not recursive */
|
||||
test06::bar : a
|
||||
test06::bar = test06::foo
|
||||
bar : a
|
||||
bar = foo
|
||||
|
||||
|
||||
|
||||
|
@ -1,13 +1,13 @@
|
||||
Loading module Cryptol
|
||||
Showing a specific instance of polymorphic result:
|
||||
* Using 'Integer' for the type of '<interactive>::x'
|
||||
* Using 'Integer' for the type of 'x'
|
||||
1
|
||||
Showing a specific instance of polymorphic result:
|
||||
* Using 'Integer' for the type of '<interactive>::x'
|
||||
* Using 'Integer' for the type of 'x'
|
||||
[1, 2]
|
||||
Showing a specific instance of polymorphic result:
|
||||
* Using 'Integer' for the type of '<interactive>::x'
|
||||
* Using 'Integer' for the type of '<interactive>::y'
|
||||
* Using 'Integer' for the type of 'x'
|
||||
* Using 'Integer' for the type of 'y'
|
||||
{x = 1, y = 2}
|
||||
Showing a specific instance of polymorphic result:
|
||||
* Using 'Integer' for type of 0th tuple field
|
||||
|
@ -11,30 +11,30 @@ where
|
||||
/* Not recursive */
|
||||
specialize::f : (Bit, Bit) -> (Bit, Bit)
|
||||
specialize::f = \ (__p1 : (Bit, Bit)) ->
|
||||
(specialize::x, specialize::y)
|
||||
(x, y)
|
||||
where
|
||||
/* Not recursive */
|
||||
specialize::y : Bit
|
||||
specialize::y = __p1 .1 /* of 2 */
|
||||
y : Bit
|
||||
y = __p1 .1 /* of 2 */
|
||||
|
||||
/* Not recursive */
|
||||
specialize::x : Bit
|
||||
specialize::x = __p1 .0 /* of 2 */
|
||||
x : Bit
|
||||
x = __p1 .0 /* of 2 */
|
||||
|
||||
|
||||
|
||||
/* Not recursive */
|
||||
specialize::top : (Bit, Bit) -> (Bit, Bit)
|
||||
specialize::top = \ (__p0 : (Bit, Bit)) ->
|
||||
specialize::f (specialize::x, specialize::y)
|
||||
specialize::f (x, y)
|
||||
where
|
||||
/* Not recursive */
|
||||
specialize::y : Bit
|
||||
specialize::y = __p0 .1 /* of 2 */
|
||||
y : Bit
|
||||
y = __p0 .1 /* of 2 */
|
||||
|
||||
/* Not recursive */
|
||||
specialize::x : Bit
|
||||
specialize::x = __p0 .0 /* of 2 */
|
||||
x : Bit
|
||||
x = __p0 .0 /* of 2 */
|
||||
|
||||
|
||||
|
||||
|
@ -51,9 +51,8 @@ Loading module Main
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
|
||||
[error] at :1:1--1:11:
|
||||
Recursive type declarations:
|
||||
`Main::T`
|
||||
[error] Invalid recursive dependency:
|
||||
• type Main::T
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user