mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-13 10:58:23 +03:00
More information when browsing.
This implements the feature request in #689
This commit is contained in:
Iavor Diatchki
parent
ec36d1aa38
commit
fcc7a19998
@ -14,7 +14,7 @@
|
||||
|
||||
module Cryptol.ModuleSystem.Base where
|
||||
|
||||
import Cryptol.ModuleSystem.Env (DynamicEnv(..), deIfaceDecls)
|
||||
import Cryptol.ModuleSystem.Env (DynamicEnv(..))
|
||||
import Cryptol.ModuleSystem.Fingerprint
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
import Cryptol.ModuleSystem.Monad
|
||||
@ -22,6 +22,7 @@ import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap)
|
||||
import Cryptol.ModuleSystem.Env (lookupModule
|
||||
, LoadedModule(..)
|
||||
, meCoreLint, CoreLint(..)
|
||||
, ModContext(..)
|
||||
, ModulePath(..), modulePathLabel)
|
||||
import qualified Cryptol.Eval as E
|
||||
import qualified Cryptol.Eval.Value as E
|
||||
@ -313,21 +314,15 @@ loadDeps m =
|
||||
|
||||
-- Type Checking ---------------------------------------------------------------
|
||||
|
||||
-- | Load the local environment, which consists of the environment for the
|
||||
-- currently opened module, shadowed by the dynamic environment.
|
||||
getLocalEnv :: ModuleM (IfaceParams,IfaceDecls,R.NamingEnv)
|
||||
getLocalEnv =
|
||||
do (params,decls,fNames,_) <- getFocusedEnv
|
||||
denv <- getDynEnv
|
||||
let dynDecls = deIfaceDecls denv
|
||||
return (params,dynDecls `mappend` decls, deNames denv `R.shadowing` fNames)
|
||||
|
||||
-- | Typecheck a single expression, yielding a renamed parsed expression,
|
||||
-- typechecked core expression, and a type schema.
|
||||
checkExpr :: P.Expr PName -> ModuleM (P.Expr Name,T.Expr,T.Schema)
|
||||
checkExpr e = do
|
||||
|
||||
(params,decls,names) <- getLocalEnv
|
||||
fe <- getFocusedEnv
|
||||
let params = mctxParams fe
|
||||
decls = mctxDecls fe
|
||||
names = mctxNames fe
|
||||
|
||||
-- run NoPat
|
||||
npe <- noPat e
|
||||
@ -348,7 +343,10 @@ checkExpr e = do
|
||||
-- INVARIANT: This assumes that NoPat has already been run on the declarations.
|
||||
checkDecls :: [P.TopDecl PName] -> ModuleM (R.NamingEnv,[T.DeclGroup])
|
||||
checkDecls ds = do
|
||||
(params,decls,names) <- getLocalEnv
|
||||
fe <- getFocusedEnv
|
||||
let params = mctxParams fe
|
||||
decls = mctxDecls fe
|
||||
names = mctxNames fe
|
||||
|
||||
-- introduce names for the declarations before renaming them
|
||||
declsEnv <- liftSupply (R.namingEnv' (map (R.InModule interactiveName) ds))
|
||||
|
||||
@ -20,7 +20,7 @@ import Paths_cryptol (getDataDir)
|
||||
import Cryptol.Eval (EvalEnv)
|
||||
import Cryptol.ModuleSystem.Fingerprint
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
import Cryptol.ModuleSystem.Name (Supply,emptySupply)
|
||||
import Cryptol.ModuleSystem.Name (Name,Supply,emptySupply)
|
||||
import qualified Cryptol.ModuleSystem.NamingEnv as R
|
||||
import Cryptol.Parser.AST
|
||||
import qualified Cryptol.TypeCheck as T
|
||||
@ -31,8 +31,8 @@ import Data.ByteString(ByteString)
|
||||
import Control.Monad (guard,mplus)
|
||||
import qualified Control.Exception as X
|
||||
import Data.Function (on)
|
||||
import Data.Map (Map)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe(fromMaybe)
|
||||
import Data.Semigroup
|
||||
import System.Directory (getAppUserDataDirectory, getCurrentDirectory)
|
||||
import System.Environment(getExecutablePath)
|
||||
@ -45,6 +45,9 @@ import Control.DeepSeq
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.PP(pp)
|
||||
|
||||
-- Module Environment ----------------------------------------------------------
|
||||
|
||||
-- | This is the current state of the interpreter.
|
||||
@ -178,47 +181,95 @@ hasParamModules :: ModuleEnv -> Bool
|
||||
hasParamModules = not . null . lmLoadedParamModules . meLoadedModules
|
||||
|
||||
|
||||
-- | Produce an ifaceDecls that represents the focused environment of the module
|
||||
-- system, as well as a 'NameDisp' for pretty-printing names according to the
|
||||
-- imports.
|
||||
--
|
||||
-- XXX This could really do with some better error handling, just returning
|
||||
-- mempty when one of the imports fails isn't really desirable.
|
||||
--
|
||||
-- XXX: This is not quite right. For example, it does not take into
|
||||
-- account *how* things were imported in a module (e.g., qualified).
|
||||
-- It would be simpler to simply store the naming environment that was
|
||||
-- actually used when we renamed the module.
|
||||
focusedEnv :: ModuleEnv -> (IfaceParams,IfaceDecls,R.NamingEnv,NameDisp)
|
||||
|
||||
-- | Contains enough information to browse what's in scope,
|
||||
-- or type check new expressions.
|
||||
data ModContext = ModContext
|
||||
{ mctxParams :: IfaceParams
|
||||
, mctxDecls :: IfaceDecls
|
||||
, mctxNames :: R.NamingEnv
|
||||
, mctxNameDisp :: NameDisp
|
||||
, mctxTypeProvenace :: Map Name DeclProvenance
|
||||
, mctxValueProvenance :: Map Name DeclProvenance
|
||||
}
|
||||
|
||||
-- | Specifies how a declared name came to be in scope.
|
||||
data DeclProvenance =
|
||||
NameIsImportedFrom ModName
|
||||
| NameIsLocalPublic
|
||||
| NameIsLocalPrivate
|
||||
| NameIsParameter
|
||||
| NameIsDynamicDecl
|
||||
deriving (Eq,Ord)
|
||||
|
||||
|
||||
-- | 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@).
|
||||
focusedEnv :: ModuleEnv -> ModContext
|
||||
focusedEnv me =
|
||||
fromMaybe (noIfaceParams, mempty, mempty, mempty) $
|
||||
do fm <- meFocusedModule me
|
||||
lm <- lookupModule fm me
|
||||
deps <- mapM loadImport (T.mImports (lmModule lm))
|
||||
let (ifaces,names) = unzip deps
|
||||
Iface { .. } = lmInterface lm
|
||||
localDecls = ifPublic `mappend` ifPrivate
|
||||
localNames = R.unqualifiedEnv localDecls `mappend`
|
||||
R.modParamsNamingEnv ifParams
|
||||
namingEnv = localNames `R.shadowing` mconcat names
|
||||
ModContext
|
||||
{ mctxParams = parameters
|
||||
, mctxDecls = mconcat (dynDecls : localDecls : importedDecls)
|
||||
, mctxNames = namingEnv
|
||||
, mctxNameDisp = R.toNameDisp namingEnv
|
||||
, mctxTypeProvenace = fst provenance
|
||||
, mctxValueProvenance = snd provenance
|
||||
}
|
||||
|
||||
return ( ifParams
|
||||
, mconcat (localDecls:ifaces)
|
||||
, namingEnv
|
||||
, R.toNameDisp namingEnv)
|
||||
where
|
||||
(importedNames,importedDecls,importedProvs) = unzip3 (map loadImport imports)
|
||||
localDecls = publicDecls `mappend` privateDecls
|
||||
localNames = R.unqualifiedEnv localDecls `mappend`
|
||||
R.modParamsNamingEnv parameters
|
||||
dynDecls = deIfaceDecls (meDynEnv me)
|
||||
dynNames = deNames (meDynEnv me)
|
||||
|
||||
namingEnv = dynNames `R.shadowing`
|
||||
localNames `R.shadowing`
|
||||
mconcat importedNames
|
||||
|
||||
provenance = shadowProvs
|
||||
$ declsProv NameIsDynamicDecl dynDecls
|
||||
: declsProv NameIsLocalPublic publicDecls
|
||||
: declsProv NameIsLocalPrivate privateDecls
|
||||
: paramProv parameters
|
||||
: importedProvs
|
||||
|
||||
(imports, parameters, publicDecls, privateDecls) =
|
||||
case meFocusedModule me of
|
||||
Nothing -> (mempty, noIfaceParams, mempty, mempty)
|
||||
Just fm ->
|
||||
case lookupModule fm me of
|
||||
Just lm ->
|
||||
let Iface { .. } = lmInterface lm
|
||||
in (T.mImports (lmModule lm), ifParams, ifPublic, ifPrivate)
|
||||
Nothing -> panic "focusedEnv" ["Focused module is not loaded."]
|
||||
|
||||
loadImport imp =
|
||||
do lm <- lookupModule (iModule imp) me
|
||||
let decls = ifPublic (lmInterface lm)
|
||||
return (decls,R.interpImport imp decls)
|
||||
case lookupModule (iModule imp) me of
|
||||
Just lm ->
|
||||
let decls = ifPublic (lmInterface lm)
|
||||
in ( R.interpImport imp decls
|
||||
, decls
|
||||
, declsProv (NameIsImportedFrom (iModule imp)) decls
|
||||
)
|
||||
Nothing -> panic "focusedEnv"
|
||||
[ "Missing imported module: " ++ show (pp (iModule imp)) ]
|
||||
|
||||
-- | The unqualified declarations and name environment for the dynamic
|
||||
-- environment.
|
||||
dynamicEnv :: ModuleEnv -> (IfaceDecls,R.NamingEnv,NameDisp)
|
||||
dynamicEnv me = (decls,names,R.toNameDisp names)
|
||||
where
|
||||
decls = deIfaceDecls (meDynEnv me)
|
||||
names = R.unqualifiedEnv decls
|
||||
|
||||
-- earlier ones shadow
|
||||
shadowProvs ps = let (tss,vss) = unzip ps
|
||||
in (Map.unions tss, Map.unions vss)
|
||||
|
||||
paramProv IfaceParams { .. } = (doMap ifParamTypes, doMap ifParamFuns)
|
||||
where doMap mp = const NameIsParameter <$> mp
|
||||
|
||||
declsProv prov IfaceDecls { .. } =
|
||||
( Map.unions [ doMap ifTySyns, doMap ifNewtypes, doMap ifAbstractTypes ]
|
||||
, doMap ifDecls
|
||||
)
|
||||
where doMap mp = const prov <$> mp
|
||||
|
||||
|
||||
-- Loaded Modules --------------------------------------------------------------
|
||||
@ -281,14 +332,23 @@ instance Monoid LoadedModules where
|
||||
|
||||
data LoadedModule = LoadedModule
|
||||
{ lmName :: ModName
|
||||
-- ^ The name of this module. Should match what's in 'lmModule'
|
||||
|
||||
, lmFilePath :: ModulePath
|
||||
-- ^ The file path used to load this module (may not be canonical)
|
||||
|
||||
, lmModuleId :: String
|
||||
-- ^ An identifier used to identify the source of the bytes for the module.
|
||||
-- For files we just use the cononical path, for in memory things we
|
||||
-- use their label.
|
||||
|
||||
, lmInterface :: Iface
|
||||
-- ^ The module's interface. This is for convenient. At the moment
|
||||
-- we have the whole module in 'lmModule', so this could be computer.
|
||||
|
||||
, lmModule :: T.Module
|
||||
-- ^ The actual type-checked module
|
||||
|
||||
, lmFingerprint :: Fingerprint
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
@ -328,6 +388,8 @@ addLoadedModule path ident fp tm lm
|
||||
}
|
||||
|
||||
-- | Remove a previously loaded module.
|
||||
-- Note that this removes exactly the modules specified by the predicate.
|
||||
-- One should be carfule to preserve the invariant on 'LoadedModules'.
|
||||
removeLoadedModule :: (LoadedModule -> Bool) -> LoadedModules -> LoadedModules
|
||||
removeLoadedModule rm lm =
|
||||
LoadedModules
|
||||
@ -340,9 +402,8 @@ removeLoadedModule rm lm =
|
||||
|
||||
-- | Extra information we need to carry around to dynamically extend
|
||||
-- an environment outside the context of a single module. Particularly
|
||||
-- useful when dealing with interactive declarations as in @:let@ or
|
||||
-- useful when dealing with interactive declarations as in @let@ or
|
||||
-- @it@.
|
||||
|
||||
data DynamicEnv = DEnv
|
||||
{ deNames :: R.NamingEnv
|
||||
, deDecls :: [T.DeclGroup]
|
||||
|
||||
@ -19,8 +19,7 @@ import Cryptol.ModuleSystem.Env
|
||||
import Cryptol.ModuleSystem.Fingerprint
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
import Cryptol.ModuleSystem.Name (FreshM(..),Supply)
|
||||
import Cryptol.ModuleSystem.Renamer
|
||||
(RenamerError(),RenamerWarning(),NamingEnv)
|
||||
import Cryptol.ModuleSystem.Renamer (RenamerError(),RenamerWarning())
|
||||
import qualified Cryptol.Parser as Parser
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
import Cryptol.Parser.Position (Located)
|
||||
@ -508,8 +507,7 @@ withPrependedSearchPath fps m = ModuleT $ do
|
||||
set $! env { meSearchPath = fps0 }
|
||||
return x
|
||||
|
||||
-- XXX improve error handling here
|
||||
getFocusedEnv :: ModuleM (IfaceParams,IfaceDecls,NamingEnv,NameDisp)
|
||||
getFocusedEnv :: ModuleM ModContext
|
||||
getFocusedEnv = ModuleT (focusedEnv `fmap` get)
|
||||
|
||||
getDynEnv :: ModuleM DynamicEnv
|
||||
|
||||
@ -72,7 +72,7 @@ import qualified Cryptol.TypeCheck.Parseable as T
|
||||
import qualified Cryptol.TypeCheck.Subst as T
|
||||
import Cryptol.TypeCheck.Solve(defaultReplExpr)
|
||||
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
|
||||
import Cryptol.TypeCheck.PP (dump,ppWithNames,emptyNameMap,backticks)
|
||||
import Cryptol.TypeCheck.PP (dump,ppWithNames,emptyNameMap)
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
@ -89,7 +89,8 @@ import qualified Data.ByteString.Char8 as BS8
|
||||
import Data.Bits (shiftL, (.&.), (.|.))
|
||||
import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii)
|
||||
import Data.Function (on)
|
||||
import Data.List (intercalate, nub, sortBy, partition, isPrefixOf,intersperse)
|
||||
import Data.List (intercalate, nub, sortBy, groupBy,
|
||||
partition, isPrefixOf,intersperse)
|
||||
import Data.Maybe (fromMaybe,mapMaybe,isNothing)
|
||||
import System.Environment (lookupEnv)
|
||||
import System.Exit (ExitCode(ExitSuccess))
|
||||
@ -99,6 +100,7 @@ import System.FilePath((</>), isPathSeparator)
|
||||
import System.Directory(getHomeDirectory,setCurrentDirectory,doesDirectoryExist
|
||||
,getTemporaryDirectory,setPermissions,removeFile
|
||||
,emptyPermissions,setOwnerReadable)
|
||||
import Data.Map (Map)
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import System.IO(hFlush,stdout,openTempFile,hClose)
|
||||
@ -732,9 +734,9 @@ typeOfCmd str = do
|
||||
|
||||
-- XXX need more warnings from the module system
|
||||
whenDebug (rPutStrLn (dump def))
|
||||
(_,_,_,names) <- getFocusedEnv
|
||||
fDisp <- M.mctxNameDisp <$> getFocusedEnv
|
||||
-- type annotation ':' has precedence 2
|
||||
rPrint $ runDoc names $ ppPrec 2 expr <+> text ":" <+> pp sig
|
||||
rPrint $ runDoc fDisp $ ppPrec 2 expr <+> text ":" <+> pp sig
|
||||
|
||||
readFileCmd :: FilePath -> REPL ()
|
||||
readFileCmd fp = do
|
||||
@ -905,10 +907,6 @@ quitCmd = stop
|
||||
|
||||
browseCmd :: String -> REPL ()
|
||||
browseCmd input = do
|
||||
(params, iface, fNames, disp) <- getFocusedEnv
|
||||
denv <- getDynEnv
|
||||
let names = M.deNames denv `M.shadowing` fNames
|
||||
|
||||
let mnames = map (M.textToModName . T.pack) (words input)
|
||||
validModNames <- (:) M.interactiveName <$> getModNames
|
||||
let checkModName m =
|
||||
@ -916,6 +914,16 @@ browseCmd input = do
|
||||
rPutStrLn ("error: " ++ show m ++ " is not a loaded module.")
|
||||
mapM_ checkModName mnames
|
||||
|
||||
fe <- getFocusedEnv
|
||||
|
||||
let params = M.mctxParams fe
|
||||
iface = M.mctxDecls fe
|
||||
names = M.mctxNames fe
|
||||
disp = M.mctxNameDisp fe
|
||||
provV = M.mctxValueProvenance fe
|
||||
provT = M.mctxTypeProvenace fe
|
||||
|
||||
|
||||
let f &&& g = \x -> f x && g x
|
||||
isUser x = case M.nameInfo x of
|
||||
M.Declared _ M.SystemName -> False
|
||||
@ -929,16 +937,15 @@ browseCmd input = do
|
||||
visibleType = isUser &&& restricted &&& inSet visibleTypes
|
||||
visibleDecl = isUser &&& restricted &&& inSet visibleDecls
|
||||
|
||||
|
||||
browseMParams visibleType visibleDecl params disp
|
||||
browseTSyns visibleType iface disp
|
||||
browsePrimTys visibleType iface disp
|
||||
browseNewtypes visibleType iface disp
|
||||
browseVars visibleDecl iface disp
|
||||
browseTSyns visibleType provT iface disp
|
||||
browsePrimTys visibleType provT iface disp
|
||||
browseNewtypes visibleType provT iface disp
|
||||
browseVars visibleDecl provV iface disp
|
||||
|
||||
|
||||
browseMParams :: (M.Name -> Bool) -> (M.Name -> Bool) ->
|
||||
M.IfaceParams-> NameDisp -> REPL ()
|
||||
M.IfaceParams -> NameDisp -> REPL ()
|
||||
browseMParams visT visD M.IfaceParams { .. } names =
|
||||
do ppBlock names ppParamTy "Type Parameters"
|
||||
(sorted visT T.mtpName ifParamTypes)
|
||||
@ -953,53 +960,150 @@ browseMParams visT visD M.IfaceParams { .. } names =
|
||||
sorted vis nm mp = sortBy (M.cmpNameDisplay names `on` nm)
|
||||
$ filter (vis . nm) $ Map.elems mp
|
||||
|
||||
type Prov = Map M.Name M.DeclProvenance
|
||||
|
||||
browsePrimTys :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()
|
||||
browsePrimTys isVisible M.IfaceDecls { .. } names =
|
||||
do let pts = sortBy (M.cmpNameDisplay names `on` T.atName)
|
||||
[ ts | ts <- Map.elems ifAbstractTypes, isVisible (T.atName ts) ]
|
||||
ppBlock names ppA "Primitive Types" pts
|
||||
browsePrimTys :: (M.Name -> Bool) -> Prov -> M.IfaceDecls -> NameDisp -> REPL ()
|
||||
browsePrimTys isVisible prov M.IfaceDecls { .. } names =
|
||||
ppSection (Map.elems ifAbstractTypes)
|
||||
Section { secName = "Primitive Types"
|
||||
, secEntryName = T.atName
|
||||
, secProvenance = prov
|
||||
, secDisp = names
|
||||
, secPP = ppA
|
||||
, secVisible = isVisible
|
||||
}
|
||||
where
|
||||
ppA a = pp (T.atName a) <+> ":" <+> pp (T.atKind a)
|
||||
|
||||
browseTSyns :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()
|
||||
browseTSyns isVisible M.IfaceDecls { .. } names = do
|
||||
let tsyns = sortBy (M.cmpNameDisplay names `on` T.tsName)
|
||||
[ ts | ts <- Map.elems ifTySyns, isVisible (T.tsName ts) ]
|
||||
|
||||
(cts,tss) = partition isCtrait tsyns
|
||||
|
||||
ppBlock names pp "Type Synonyms" tss
|
||||
ppBlock names pp "Constraint Synonyms" cts
|
||||
|
||||
browseTSyns :: (M.Name -> Bool) -> Prov -> M.IfaceDecls -> NameDisp -> REPL ()
|
||||
browseTSyns isVisible prov M.IfaceDecls { .. } names =
|
||||
do ppSection tss
|
||||
Section { secName = "Type Synonyms"
|
||||
, secEntryName = T.tsName
|
||||
, secProvenance = prov
|
||||
, secDisp = names
|
||||
, secVisible = isVisible
|
||||
, secPP = pp
|
||||
}
|
||||
ppSection cts
|
||||
Section { secName = "Constraint Synonyms"
|
||||
, secEntryName = T.tsName
|
||||
, secProvenance = prov
|
||||
, secDisp = names
|
||||
, secVisible = isVisible
|
||||
, secPP = pp
|
||||
}
|
||||
where
|
||||
(cts,tss) = partition isCtrait (Map.elems ifTySyns)
|
||||
isCtrait t = T.kindResult (T.kindOf (T.tsDef t)) == T.KProp
|
||||
|
||||
browseNewtypes :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()
|
||||
browseNewtypes isVisible M.IfaceDecls { .. } names = do
|
||||
let nts = sortBy (M.cmpNameDisplay names `on` T.ntName)
|
||||
[ nt | nt <- Map.elems ifNewtypes, isVisible (T.ntName nt) ]
|
||||
unless (null nts) $ do
|
||||
rPutStrLn "Newtypes"
|
||||
rPutStrLn "========"
|
||||
rPrint (runDoc names (nest 4 (vcat (map T.ppNewtypeShort nts))))
|
||||
rPutStrLn ""
|
||||
browseNewtypes ::
|
||||
(M.Name -> Bool) -> Prov -> M.IfaceDecls -> NameDisp -> REPL ()
|
||||
browseNewtypes isVisible prov M.IfaceDecls { .. } names =
|
||||
ppSection (Map.elems ifNewtypes)
|
||||
Section { secName = "Newtypes"
|
||||
, secEntryName = T.ntName
|
||||
, secVisible = isVisible
|
||||
, secProvenance = prov
|
||||
, secDisp = names
|
||||
, secPP = T.ppNewtypeShort
|
||||
}
|
||||
|
||||
browseVars :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()
|
||||
browseVars isVisible M.IfaceDecls { .. } names = do
|
||||
let vars = sortBy (M.cmpNameDisplay names `on` M.ifDeclName)
|
||||
[ d | d <- Map.elems ifDecls, isVisible (M.ifDeclName d) ]
|
||||
browseVars :: (M.Name -> Bool) -> Prov -> M.IfaceDecls -> NameDisp -> REPL ()
|
||||
browseVars isVisible prov M.IfaceDecls { .. } names =
|
||||
do ppSection props Section { secName = "Properties"
|
||||
, secEntryName = M.ifDeclName
|
||||
, secVisible = isVisible
|
||||
, secProvenance = prov
|
||||
, secDisp = names
|
||||
, secPP = ppVar
|
||||
}
|
||||
ppSection syms Section { secName = "Symbols"
|
||||
, secEntryName = M.ifDeclName
|
||||
, secVisible = isVisible
|
||||
, secProvenance = prov
|
||||
, secDisp = names
|
||||
, secPP = ppVar
|
||||
}
|
||||
|
||||
where
|
||||
isProp p = T.PragmaProperty `elem` (M.ifDeclPragmas p)
|
||||
(props,syms) = partition isProp (Map.elems ifDecls)
|
||||
|
||||
ppVar M.IfaceDecl { .. } = hang (pp ifDeclName <+> char ':') 2 (pp ifDeclSig)
|
||||
|
||||
|
||||
let isProp p = T.PragmaProperty `elem` (M.ifDeclPragmas p)
|
||||
(props,syms) = partition isProp vars
|
||||
|
||||
data Section a = Section
|
||||
{ secName :: String
|
||||
, secEntryName :: a -> M.Name
|
||||
, secVisible :: M.Name -> Bool
|
||||
, secProvenance :: Map M.Name M.DeclProvenance
|
||||
, secDisp :: NameDisp
|
||||
, secPP :: a -> Doc
|
||||
}
|
||||
|
||||
let ppVar M.IfaceDecl { .. } = hang (pp ifDeclName <+> char ':')
|
||||
2 (pp ifDeclSig)
|
||||
ppSection :: [a] -> Section a -> REPL ()
|
||||
ppSection things s
|
||||
| null grouped = pure ()
|
||||
| otherwise =
|
||||
do let heading = secName s
|
||||
rPutStrLn heading
|
||||
rPutStrLn (map (const '=') heading)
|
||||
rPutStrLn ""
|
||||
mapM_ ppSub grouped
|
||||
|
||||
where
|
||||
ppSub (p,ts) =
|
||||
do let heading = provHeading p
|
||||
rPutStrLn (" " ++ heading)
|
||||
rPutStrLn (" " ++ map (const '-') heading)
|
||||
rPutStrLn ""
|
||||
rPutStrLn $ show $ runDoc (secDisp s) $ nest 4 $ vcat $ map (secPP s) ts
|
||||
rPutStrLn ""
|
||||
|
||||
grouped = map rearrange $
|
||||
groupBy sameProv $
|
||||
sortBy cmpThings
|
||||
[ (n,p,t) | t <- things,
|
||||
let n = secEntryName s t,
|
||||
secVisible s n,
|
||||
let p = case Map.lookup n (secProvenance s) of
|
||||
Just i -> i
|
||||
Nothing -> panic "ppSection"
|
||||
[ "Name with no provenance"
|
||||
, show n ]
|
||||
]
|
||||
|
||||
rearrange xs = (p, [ a | (_,_,a) <- xs ])
|
||||
where (_,p,_) : _ = xs
|
||||
|
||||
cmpThings (n1, p1, _) (n2, p2, _) =
|
||||
case cmpProv p1 p2 of
|
||||
EQ -> M.cmpNameDisplay (secDisp s) n1 n2
|
||||
r -> r
|
||||
|
||||
sameProv (_,p1,_) (_,p2,_) = provOrd p1 == provOrd p2
|
||||
|
||||
provOrd p =
|
||||
case p of
|
||||
M.NameIsParameter -> Left 1 :: Either Int P.ModName
|
||||
M.NameIsDynamicDecl -> Left 2
|
||||
M.NameIsLocalPublic -> Left 3
|
||||
M.NameIsLocalPrivate -> Left 4
|
||||
M.NameIsImportedFrom x -> Right x
|
||||
|
||||
cmpProv p1 p2 = compare (provOrd p1) (provOrd p2)
|
||||
|
||||
provHeading p =
|
||||
case p of
|
||||
M.NameIsParameter -> "Parameters"
|
||||
M.NameIsDynamicDecl -> "REPL"
|
||||
M.NameIsLocalPublic -> "Public"
|
||||
M.NameIsLocalPrivate -> "Private"
|
||||
M.NameIsImportedFrom m -> "From " ++ show (pp m)
|
||||
|
||||
ppBlock names ppVar "Properties" props
|
||||
ppBlock names ppVar "Symbols" syms
|
||||
|
||||
|
||||
ppBlock :: NameDisp -> (a -> Doc) -> String -> [a] -> REPL ()
|
||||
@ -1010,7 +1114,6 @@ ppBlock names ppFun name xs = unless (null xs) $
|
||||
rPutStrLn ""
|
||||
|
||||
|
||||
|
||||
setOptionCmd :: String -> REPL ()
|
||||
setOptionCmd str
|
||||
| Just value <- mbValue = setUser key value
|
||||
@ -1053,12 +1156,17 @@ helpCmd cmd
|
||||
| otherwise =
|
||||
case parseHelpName cmd of
|
||||
Just qname ->
|
||||
do (params,env,rnEnv,nameEnv) <- getFocusedEnv
|
||||
let vNames = M.lookupValNames qname rnEnv
|
||||
do fe <- getFocusedEnv
|
||||
let params = M.mctxParams fe
|
||||
env = M.mctxDecls fe
|
||||
rnEnv = M.mctxNames fe
|
||||
disp = M.mctxNameDisp fe
|
||||
|
||||
vNames = M.lookupValNames qname rnEnv
|
||||
tNames = M.lookupTypeNames qname rnEnv
|
||||
|
||||
let helps = map (showTypeHelp params env nameEnv) tNames ++
|
||||
map (showValHelp params env nameEnv qname) vNames
|
||||
let helps = map (showTypeHelp params env disp) tNames ++
|
||||
map (showValHelp params env disp qname) vNames
|
||||
|
||||
separ = rPutStrLn " ---------"
|
||||
sequence_ (intersperse separ helps)
|
||||
@ -1298,7 +1406,7 @@ moduleCmdResult (res,ws0) = do
|
||||
filterShadowing w = Just w
|
||||
|
||||
let ws = mapMaybe filterDefaults . mapMaybe filterShadowing $ ws0
|
||||
(_,_,_,names) <- getFocusedEnv
|
||||
names <- M.mctxNameDisp <$> getFocusedEnv
|
||||
mapM_ (rPrint . runDoc names . pp) ws
|
||||
case res of
|
||||
Right (a,me') -> setModuleEnv me' >> return a
|
||||
|
||||
@ -36,7 +36,6 @@ module Cryptol.REPL.Monad (
|
||||
, getModuleEnv, setModuleEnv
|
||||
, getDynEnv, setDynEnv
|
||||
, uniqify, freshName
|
||||
, getTSyns, getNewtypes, getVars
|
||||
, whenDebug
|
||||
, getExprNames
|
||||
, getTypeNames
|
||||
@ -474,75 +473,33 @@ rPutStrLn str = rPutStr $ str ++ "\n"
|
||||
rPrint :: Show a => a -> REPL ()
|
||||
rPrint x = rPutStrLn (show x)
|
||||
|
||||
getFocusedEnv :: REPL (M.IfaceParams,M.IfaceDecls,M.NamingEnv,NameDisp)
|
||||
getFocusedEnv = do
|
||||
me <- getModuleEnv
|
||||
-- dyNames is a NameEnv that removes the #Uniq prefix from interactively-bound
|
||||
-- variables.
|
||||
let (dyDecls,dyNames,dyDisp) = M.dynamicEnv me
|
||||
let (fParams,fDecls,fNames,fDisp) = M.focusedEnv me
|
||||
return ( fParams
|
||||
, dyDecls `mappend` fDecls
|
||||
, dyNames `M.shadowing` fNames
|
||||
, dyDisp `mappend` fDisp)
|
||||
|
||||
-- -- the subtle part here is removing the #Uniq prefix from
|
||||
-- -- interactively-bound variables, and also excluding any that are
|
||||
-- -- shadowed and thus can no longer be referenced
|
||||
-- let (fDecls,fNames,fDisp) = M.focusedEnv me
|
||||
-- edecls = M.ifDecls dyDecls
|
||||
-- -- is this QName something the user might actually type?
|
||||
-- isShadowed (qn@(P.QName (Just (P.unModName -> ['#':_])) name), _) =
|
||||
-- case Map.lookup localName neExprs of
|
||||
-- Nothing -> False
|
||||
-- Just uniqueNames -> isNamed uniqueNames
|
||||
-- where localName = P.QName Nothing name
|
||||
-- isNamed us = any (== qn) (map M.qname us)
|
||||
-- neExprs = M.neExprs (M.deNames (M.meDynEnv me))
|
||||
-- isShadowed _ = False
|
||||
-- unqual ((P.QName _ name), ifds) = (P.QName Nothing name, ifds)
|
||||
-- edecls' = Map.fromList
|
||||
-- . map unqual
|
||||
-- . filter isShadowed
|
||||
-- $ Map.toList edecls
|
||||
-- return (decls `mappend` mempty { M.ifDecls = edecls' }, names `mappend` dyNames)
|
||||
|
||||
getVars :: REPL (Map.Map M.Name M.IfaceDecl)
|
||||
getVars = do
|
||||
(_,decls,_,_) <- getFocusedEnv
|
||||
return (M.ifDecls decls)
|
||||
|
||||
getTSyns :: REPL (Map.Map M.Name T.TySyn)
|
||||
getTSyns = do
|
||||
(_,decls,_,_) <- getFocusedEnv
|
||||
return (M.ifTySyns decls)
|
||||
|
||||
getNewtypes :: REPL (Map.Map M.Name T.Newtype)
|
||||
getNewtypes = do
|
||||
(_,decls,_,_) <- getFocusedEnv
|
||||
return (M.ifNewtypes decls)
|
||||
getFocusedEnv :: REPL M.ModContext
|
||||
getFocusedEnv = M.focusedEnv <$> getModuleEnv
|
||||
|
||||
-- | Get visible variable names.
|
||||
-- This is used for command line completition.
|
||||
getExprNames :: REPL [String]
|
||||
getExprNames =
|
||||
do (_,_, fNames, _) <- getFocusedEnv
|
||||
do fNames <- M.mctxNames <$> getFocusedEnv
|
||||
return (map (show . pp) (Map.keys (M.neExprs fNames)))
|
||||
|
||||
-- | Get visible type signature names.
|
||||
-- This is used for command line completition.
|
||||
getTypeNames :: REPL [String]
|
||||
getTypeNames =
|
||||
do (_,_, fNames, _) <- getFocusedEnv
|
||||
do fNames <- M.mctxNames <$> getFocusedEnv
|
||||
return (map (show . pp) (Map.keys (M.neTypes fNames)))
|
||||
|
||||
-- | Return a list of property names, sorted by position in the file.
|
||||
getPropertyNames :: REPL ([M.Name],NameDisp)
|
||||
getPropertyNames =
|
||||
do (_,decls,_,names) <- getFocusedEnv
|
||||
let xs = M.ifDecls decls
|
||||
do fe <- getFocusedEnv
|
||||
let xs = M.ifDecls (M.mctxDecls fe)
|
||||
ps = sortBy (comparing (from . M.nameLoc))
|
||||
$ [ x | (x,d) <- Map.toList xs, T.PragmaProperty `elem` M.ifDeclPragmas d ]
|
||||
[ x | (x,d) <- Map.toList xs,
|
||||
T.PragmaProperty `elem` M.ifDeclPragmas d ]
|
||||
|
||||
return (ps, names)
|
||||
return (ps, M.mctxNameDisp fe)
|
||||
|
||||
getModNames :: REPL [I.ModName]
|
||||
getModNames =
|
||||
|
||||
@ -4,6 +4,10 @@ Loading module issue226r2
|
||||
Loading module issue226
|
||||
Type Synonyms
|
||||
=============
|
||||
|
||||
From Cryptol
|
||||
------------
|
||||
|
||||
type Bool = Bit
|
||||
type Char = [8]
|
||||
type lg2 n = width (max 1 n - 1)
|
||||
@ -12,12 +16,20 @@ Type Synonyms
|
||||
|
||||
Constraint Synonyms
|
||||
===================
|
||||
|
||||
From Cryptol
|
||||
------------
|
||||
|
||||
type constraint i < j = j >= 1 + i
|
||||
type constraint i <= j = j >= i
|
||||
type constraint i > j = i >= 1 + j
|
||||
|
||||
Primitive Types
|
||||
===============
|
||||
|
||||
From Cryptol
|
||||
------------
|
||||
|
||||
(!=) : # -> # -> Prop
|
||||
(==) : # -> # -> Prop
|
||||
(>=) : # -> # -> Prop
|
||||
@ -47,6 +59,15 @@ Primitive Types
|
||||
|
||||
Symbols
|
||||
=======
|
||||
|
||||
Public
|
||||
------
|
||||
|
||||
foo : {a} a -> a
|
||||
|
||||
From Cryptol
|
||||
------------
|
||||
|
||||
(==>) : Bit -> Bit -> Bit
|
||||
(\/) : Bit -> Bit -> Bit
|
||||
(/\) : Bit -> Bit -> Bit
|
||||
@ -98,7 +119,6 @@ Symbols
|
||||
False : Bit
|
||||
foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
|
||||
foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
|
||||
foo : {a} a -> a
|
||||
fromInteger : {a} (Arith a) => Integer -> a
|
||||
fromThenTo :
|
||||
{first, next, last, a, len} (fin first, fin next, fin last,
|
||||
|
||||
@ -2,5 +2,9 @@ Loading module Cryptol
|
||||
Loading module T10::Main
|
||||
Symbols
|
||||
=======
|
||||
|
||||
Public
|
||||
------
|
||||
|
||||
f : {T} {x : T} -> T
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user