GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-28 09:23:04 +03:00
Code Issues Projects Releases Wiki Activity

Library is building again

Browse Source
This commit is contained in:
Trevor Elliott 2015-09-24 16:30:23 -05:00
parent e5ab23cfe8
commit 56171c60ca
8 changed files with 199 additions and 100 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
src/Cryptol/ModuleSystem.hs
View File

@ -6,6 +6,8 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE FlexibleContexts #-}
module Cryptol.ModuleSystem (
-- * Module System
ModuleEnv(..), initialModuleEnv
@ -21,6 +23,9 @@ module Cryptol.ModuleSystem (
, evalDecls
, noPat
, focusedEnv
, getPrimMap
, renameVar
, renameType
-- * Interfaces
, Iface(..), IfaceDecls(..), genIface
@ -31,8 +36,8 @@ import qualified Cryptol.Eval.Value as E
import Cryptol.ModuleSystem.Env
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Monad
import Cryptol.ModuleSystem.Name (Name)
import Cryptol.ModuleSystem.Renamer (Rename,BindsNames)
import Cryptol.ModuleSystem.Name (Name,PrimMap)
import qualified Cryptol.ModuleSystem.Renamer as R
import qualified Cryptol.ModuleSystem.Base as Base
import qualified Cryptol.Parser.AST as P
import Cryptol.Parser.Name (PName)
@ -40,6 +45,7 @@ import Cryptol.Parser.NoPat (RemovePatterns)
import Cryptol.Parser.Position (HasLoc)
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.Depends as T
import qualified Cryptol.Utils.Ident as M
-- Public Interface ------------------------------------------------------------
@ -48,6 +54,9 @@ type ModuleCmd a = ModuleEnv -> IO (ModuleRes a)
type ModuleRes a = (Either ModuleError (a,ModuleEnv), [ModuleWarning])
getPrimMap :: ModuleCmd PrimMap
getPrimMap me = runModuleM me Base.getPrimMap
-- | Find the file associated with a module name in the module search path.
findModule :: P.ModName -> ModuleCmd FilePath
findModule n env = runModuleM env (Base.findModule n)
@ -89,10 +98,12 @@ evalExpr :: T.Expr -> ModuleCmd E.Value
evalExpr e env = runModuleM env (interactive (Base.evalExpr e))
-- | Typecheck declarations.
checkDecls :: (HasLoc (d Name), Rename d, T.FromDecl (d Name)
,BindsNames (d PName))
checkDecls :: (HasLoc (d Name), R.Rename d, T.FromDecl (d Name)
,R.BindsNames (R.InModule (d PName)))
=> [d PName] -> ModuleCmd [T.DeclGroup]
checkDecls ds env = runModuleM env (interactive (Base.checkDecls ds))
checkDecls ds env = runModuleM env
$ interactive
$ Base.checkDecls ds
-- | Evaluate declarations and add them to the extended environment.
evalDecls :: [T.DeclGroup] -> ModuleCmd ()
@ -100,3 +111,11 @@ evalDecls dgs env = runModuleM env (interactive (Base.evalDecls dgs))
noPat :: RemovePatterns a => a -> ModuleCmd a
noPat a env = runModuleM env (interactive (Base.noPat a))
renameVar :: R.NamingEnv -> PName -> ModuleCmd Name
renameVar names n env = runModuleM env $ interactive $
Base.rename M.interactiveName names (R.renameVar n)
renameType :: R.NamingEnv -> PName -> ModuleCmd Name
renameType names n env = runModuleM env $ interactive $
Base.rename M.interactiveName names (R.renameType n)

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

@ -7,6 +7,7 @@
-- Portability : portable
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE FlexibleContexts #-}
module Cryptol.ModuleSystem.Base where
@ -319,15 +320,16 @@ checkExpr e = do
-- | Typecheck a group of declarations.
--
-- INVARIANT: This assumes that NoPat has already been run on the declarations.
checkDecls :: (R.BindsNames (d PName), R.Rename d, T.FromDecl (d Name)
checkDecls :: (R.BindsNames (R.InModule (d PName)), R.Rename d, T.FromDecl (d Name)
,HasLoc (d Name))
=> [d PName] -> ModuleM [T.DeclGroup]
checkDecls ds = do
(decls,names) <- getLocalEnv
-- introduce names for the declarations before renaming them
rds <- rename interactiveName names $ R.shadowNames ds
$ traverse R.rename ds
rds <- rename interactiveName names
$ R.shadowNames (map (R.InModule interactiveName) ds)
$ traverse R.rename ds
prims <- getPrimMap
let act = TCAction { tcAction = T.tcDecls, tcLinter = declsLinter

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

@ -17,12 +17,14 @@
module Cryptol.ModuleSystem.Renamer (
NamingEnv(), shadowing
, BindsNames(..), namingEnv'
, BindsNames(..), InModule(..), namingEnv'
, checkNamingEnv
, shadowNames
, Rename(..), runRenamer, RenameM()
, RenamerError(..)
, RenamerWarning(..)
, renameVar
, renameType
) where
import Cryptol.ModuleSystem.Name

119
src/Cryptol/REPL/Command.hs
View File

@ -48,9 +48,10 @@ import Cryptol.REPL.Monad
import Cryptol.REPL.Trie
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Name as M (preludeName)
import qualified Cryptol.ModuleSystem.Name as M
import qualified Cryptol.ModuleSystem.NamingEnv as M
import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowed))
import qualified Cryptol.Utils.Ident as M
import qualified Cryptol.Eval.Value as E
import qualified Cryptol.Testing.Eval as Test
@ -90,6 +91,7 @@ import qualified Data.IntMap as IntMap
import System.IO(hFlush,stdout)
import System.Random.TF(newTFGen)
import Numeric (showFFloat)
import qualified Data.Text as ST
import qualified Data.Text.Lazy as T
#if __GLASGOW_HASKELL__ < 710
@ -405,7 +407,7 @@ cmdProveSat isSat expr = do
Symbolic.ProverError msg -> rPutStrLn msg
Symbolic.ThmResult ts -> do
rPutStrLn (if isSat then "Unsatisfiable" else "Q.E.D.")
let (t, e) = mkSolverResult cexStr (not isSat) (Left ts)
(t, e) <- mkSolverResult cexStr (not isSat) (Left ts)
bindItVariable t e
Symbolic.AllSatResult tevss -> do
let tess = map (map $ \(t,e,_) -> (t,e)) tevss
@ -417,8 +419,8 @@ cmdProveSat isSat expr = do
doc = ppPrec 3 parseExpr
rPrint $ hsep (doc : docs) <+>
text (if isSat then "= True" else "= False")
resultRecs = map (mkSolverResult cexStr isSat . Right) tess
collectTes tes = (t, es)
resultRecs <- mapM (mkSolverResult cexStr isSat . Right) tess
let collectTes tes = (t, es)
where
(ts, es) = unzip tes
t = case nub ts of
@ -477,27 +479,38 @@ offlineProveSat isSat str mfile = do
}
liftModuleCmd $ Symbolic.satProveOffline cmd
rIdent :: M.Ident
rIdent = M.packIdent "result"
-- | Make a type/expression pair that is suitable for binding to @it@
-- after running @:sat@ or @:prove@
mkSolverResult :: String
-> Bool
-> Either [T.Type] [(T.Type, T.Expr)]
-> (T.Type, T.Expr)
mkSolverResult thing result earg = (rty, re)
-> REPL (T.Type, T.Expr)
mkSolverResult thing result earg =
do prims <- getPrimMap
let eError str = T.ePrim prims (M.packIdent "error")
addError t = (t, T.eError prims t ("no " ++ thing ++ " available"))
argF = case earg of
Left ts -> mkArgs (map addError ts)
Right tes -> mkArgs tes
eTrue = T.ePrim prims (M.packIdent "True")
eFalse = T.ePrim prims (M.packIdent "False")
resultE = if result then eTrue else eFalse
rty = T.TRec $ [(rIdent, T.tBit )] ++ map fst argF
re = T.ERec $ [(rIdent, resultE)] ++ map snd argF
return (rty, re)
where
rName = T.mkName "result"
rty = T.TRec $ [(rName, T.tBit )] ++ map fst argF
re = T.ERec $ [(rName, resultE)] ++ map snd argF
resultE = if result then T.eTrue else T.eFalse
mkArgs tes = reverse (go tes [] (1 :: Int))
where
go [] fs _ = fs
go ((t, e):tes') fs n = go tes' (((argName, t), (argName, e)):fs) (n+1)
where argName = T.mkName ("arg" ++ show n)
argF = case earg of
Left ts -> mkArgs $ (map addError) ts
where addError t = (t, T.eError t ("no " ++ thing ++ " available"))
Right tes -> mkArgs tes
mkArgs tes = zipWith mkArg [1 :: Int ..] tes
where
mkArg n (t,e) =
let argName = M.packIdent ("arg" ++ show n)
in ((argName,t),(argName,e))
specializeCmd :: String -> REPL ()
specializeCmd str = do
@ -520,7 +533,7 @@ typeOfCmd str = do
-- XXX need more warnings from the module system
--io (mapM_ printWarning ws)
whenDebug (rPutStrLn (dump def))
(_,names) <- getFocusedEnv
(_,_,names) <- getFocusedEnv
rPrint $ runDoc names $ pp re <+> text ":" <+> pp sig
reloadCmd :: REPL ()
@ -588,12 +601,13 @@ quitCmd = stop
browseCmd :: String -> REPL ()
browseCmd pfx = do
env <- getFocusedEnv
(iface,_,disp) <- getFocusedEnv
let env = (iface,disp)
browseTSyns env pfx
browseNewtypes env pfx
browseVars env pfx
browseTSyns :: (M.IfaceDecls,NameEnv) -> String -> REPL ()
browseTSyns :: (M.IfaceDecls,NameDisp) -> String -> REPL ()
browseTSyns (decls,names) pfx = do
let tsyns = keepOne "browseTSyns" `fmap` M.ifTySyns decls
tsyns' = Map.filterWithKey (\k _ -> pfx `isNamePrefix` k) tsyns
@ -604,7 +618,7 @@ browseTSyns (decls,names) pfx = do
rPrint (runDoc names (nest 4 (vcat (map ppSyn (Map.toList tsyns')))))
rPutStrLn ""
browseNewtypes :: (M.IfaceDecls,NameEnv) -> String -> REPL ()
browseNewtypes :: (M.IfaceDecls,NameDisp) -> String -> REPL ()
browseNewtypes (decls,names) pfx = do
let nts = keepOne "browseNewtypes" `fmap` M.ifNewtypes decls
nts' = Map.filterWithKey (\k _ -> pfx `isNamePrefix` k) nts
@ -615,7 +629,7 @@ browseNewtypes (decls,names) pfx = do
rPrint (runDoc names (nest 4 (vcat (map ppNT (Map.toList nts')))))
rPutStrLn ""
browseVars :: (M.IfaceDecls,NameEnv) -> String -> REPL ()
browseVars :: (M.IfaceDecls,NameDisp) -> String -> REPL ()
browseVars (decls,names) pfx = do
let vars = keepOne "browseVars" `fmap` M.ifDecls decls
allNames = vars
@ -669,14 +683,16 @@ setOptionCmd str
rPutStrLn ("Did you mean: `:set " ++ k1 ++ " =" ++ k2 ++ "`?")
-- XXX at the moment, this can only look at declarations.
helpCmd :: String -> REPL ()
helpCmd cmd
| null cmd = mapM_ rPutStrLn (genHelp commandList)
| otherwise =
case parseHelpName cmd of
Just qname ->
do (env,nameEnv) <- getFocusedEnv
case Map.lookup qname (M.ifDecls env) of
do (env,rnEnv,nameEnv) <- getFocusedEnv
name <- liftModuleCmd (M.renameVar rnEnv qname)
case Map.lookup name (M.ifDecls env) of
Just [M.IfaceDecl { .. }] ->
do rPutStrLn ""
@ -723,10 +739,13 @@ handleCtrlC = rPutStrLn "Ctrl-C"
-- Utilities -------------------------------------------------------------------
isNamePrefix :: String -> P.QName -> Bool
isNamePrefix pfx n = case n of
P.QName _ (P.Name _) -> pfx `isPrefixOf` pretty n
_ -> False
isNamePrefix :: String -> M.Name -> Bool
isNamePrefix pfx =
let pfx' = ST.pack pfx
in \n -> case M.nameInfo n of
M.Declared _ -> pfx' `ST.isPrefixOf` M.identText (M.nameIdent n)
M.Parameter -> False
{-
printWarning :: (Range,Warning) -> IO ()
@ -742,15 +761,18 @@ replParse parse str = case parse str of
Right a -> return a
Left e -> raise (ParseError e)
replParseInput :: String -> REPL P.ReplInput
replParseInput :: String -> REPL (P.ReplInput P.PName)
replParseInput = replParse (parseReplWith interactiveConfig . T.pack)
replParseExpr :: String -> REPL P.Expr
replParseExpr :: String -> REPL (P.Expr P.PName)
replParseExpr = replParse (parseExprWith interactiveConfig . T.pack)
interactiveConfig :: Config
interactiveConfig = defaultConfig { cfgSource = "<interactive>" }
getPrimMap :: REPL M.PrimMap
getPrimMap = liftModuleCmd M.getPrimMap
liftModuleCmd :: M.ModuleCmd a -> REPL a
liftModuleCmd cmd = moduleCmdResult =<< io . cmd =<< getModuleEnv
@ -779,23 +801,22 @@ moduleCmdResult (res,ws0) = do
filterShadowing w = Just w
let ws = mapMaybe filterDefaults . mapMaybe filterShadowing $ ws0
(_,names) <- getFocusedEnv
(_,_,names) <- getFocusedEnv
mapM_ (rPrint . runDoc names . pp) ws
case res of
Right (a,me') -> setModuleEnv me' >> return a
Left err -> raise (ModuleSystemError names err)
replCheckExpr :: P.Expr -> REPL (P.Expr,T.Expr,T.Schema)
replCheckExpr :: P.Expr P.PName -> REPL (P.Expr M.Name,T.Expr,T.Schema)
replCheckExpr e = liftModuleCmd $ M.checkExpr e
-- | Check declarations as though they were defined at the top-level.
replCheckDecls :: [P.Decl] -> REPL [T.DeclGroup]
replCheckDecls :: [P.Decl P.PName] -> REPL [T.DeclGroup]
replCheckDecls ds = do
npds <- liftModuleCmd $ M.noPat ds
denv <- getDynEnv
let dnames = M.namingEnv npds
ne' <- M.travNamingEnv uniqify dnames
let denv' = denv { M.deNames = ne' `M.shadowing` M.deNames denv }
dnames <- M.liftSupply (M.namingEnv' (map (M.InModule M.interactiveName) npds))
let denv' = denv { M.deNames = dnames `M.shadowing` M.deNames denv }
undo exn = do
-- if typechecking fails, we want to revert changes to the
-- dynamic environment and reraise
@ -803,12 +824,12 @@ replCheckDecls ds = do
raise exn
setDynEnv denv'
let topDecls = [ P.Decl (P.TopLevel P.Public Nothing d) | d <- npds ]
catch (liftModuleCmd $ M.checkDecls topDecls) undo
catch (liftModuleCmd (M.checkDecls topDecls)) undo
replSpecExpr :: T.Expr -> REPL T.Expr
replSpecExpr e = liftModuleCmd $ S.specialize e
replEvalExpr :: P.Expr -> REPL (E.Value, T.Type)
replEvalExpr :: P.Expr P.PName -> REPL (E.Value, T.Type)
replEvalExpr expr =
do (_,def,sig) <- replCheckExpr expr
@ -835,14 +856,16 @@ replEvalExpr expr =
warnDefault ns (x,t) =
rPrint $ text "Assuming" <+> ppWithNames ns x <+> text "=" <+> pp t
itIdent :: M.Ident
itIdent = M.packIdent "it"
-- | Creates a fresh binding of "it" to the expression given, and adds
-- it to the current dynamic environment
bindItVariable :: T.Type -> T.Expr -> REPL ()
bindItVariable ty expr = do
let it = T.QName Nothing (P.mkName "it")
freshIt <- uniqify it
let dg = T.NonRecursive decl
schema = T.Forall { T.sVars = []
freshIt <- freshName itIdent
let schema = T.Forall { T.sVars = []
, T.sProps = []
, T.sType = ty
}
@ -854,10 +877,10 @@ bindItVariable ty expr = do
, T.dFixity = Nothing
, T.dDoc = Nothing
}
liftModuleCmd (M.evalDecls [dg])
liftModuleCmd (M.evalDecls [T.NonRecursive decl])
denv <- getDynEnv
let en = M.EFromBind (P.Located emptyRange freshIt)
nenv' = M.singletonE it en `M.shadowing` M.deNames denv
let nenv' = M.singletonE (P.UnQual itIdent) freshIt
`M.shadowing` M.deNames denv
setDynEnv $ denv { M.deNames = nenv' }
-- | Creates a fresh binding of "it" to a finite sequence of
@ -870,7 +893,7 @@ bindItVariables ty exprs = bindItVariable seqTy seqExpr
seqTy = T.tSeq (T.tNum len) ty
seqExpr = T.EList exprs ty
replEvalDecl :: P.Decl -> REPL ()
replEvalDecl :: P.Decl P.PName -> REPL ()
replEvalDecl decl = do
dgs <- replCheckDecls [decl]
whenDebug (mapM_ (\dg -> (rPutStrLn (dump dg))) dgs)

114
src/Cryptol/REPL/Monad.hs
View File

@ -31,7 +31,7 @@ module Cryptol.REPL.Monad (
, getFocusedEnv, keepOne
, getModuleEnv, setModuleEnv
, getDynEnv, setDynEnv
, uniqify
, uniqify, freshName
, getTSyns, getNewtypes, getVars
, whenDebug
, getExprNames
@ -71,12 +71,15 @@ import Cryptol.REPL.Trie
import Cryptol.Eval (EvalError)
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Env as M
import qualified Cryptol.ModuleSystem.Name as M
import qualified Cryptol.ModuleSystem.NamingEnv as M
import Cryptol.Parser (ParseError,ppError)
import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError)
import Cryptol.Parser.NoPat (Error)
import Cryptol.Parser.Position (emptyRange)
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck as T
import qualified Cryptol.Utils.Ident as I
import Cryptol.Utils.PP
import Cryptol.Utils.Panic (panic)
import qualified Cryptol.Parser.AST as P
@ -86,7 +89,7 @@ import Control.Monad (ap,unless,when)
import Control.Monad.IO.Class
import Data.Char (isSpace)
import Data.IORef
(IORef,newIORef,readIORef,modifyIORef)
(IORef,newIORef,readIORef,modifyIORef,atomicModifyIORef)
import Data.List (intercalate, isPrefixOf, unfoldr)
import Data.Maybe (catMaybes)
import Data.Typeable (Typeable)
@ -115,7 +118,6 @@ data RW = RW
, eContinue :: Bool
, eIsBatch :: Bool
, eModuleEnv :: M.ModuleEnv
, eNameSupply :: Int
, eUserEnv :: UserEnv
, ePutStr :: String -> IO ()
, eLetEnabled :: Bool
@ -131,7 +133,6 @@ defaultRW isBatch = do
, eContinue = True
, eIsBatch = isBatch
, eModuleEnv = env
, eNameSupply = 0
, eUserEnv = mkUserEnv userOptions
, ePutStr = putStr
, eLetEnabled = True
@ -177,6 +178,12 @@ instance Monad REPL where
instance MonadIO REPL where
liftIO = io
instance M.FreshM REPL where
liftSupply f = modifyRW $ \ RW { .. } ->
let (a,s') = f (M.meSupply eModuleEnv)
in (RW { eModuleEnv = eModuleEnv { M.meSupply = s' }, .. },a)
-- Exceptions ------------------------------------------------------------------
-- | REPL exceptions.
@ -207,7 +214,7 @@ instance PP REPLException where
]
NoPatError es -> vcat (map pp es)
NoIncludeError es -> vcat (map ppIncludeError es)
ModuleSystemError ns me -> withNameDisp ns (pp me)
ModuleSystemError ns me -> fixNameDisp ns (pp me)
EvalError e -> pp e
EvalPolyError s -> text "Cannot evaluate polymorphic value."
$$ text "Type:" <+> pp s
@ -243,6 +250,9 @@ io m = REPL (\ _ -> m)
getRW :: REPL RW
getRW = REPL readIORef
modifyRW :: (RW -> (RW,a)) -> REPL a
modifyRW f = REPL (\ ref -> atomicModifyIORef ref f)
modifyRW_ :: (RW -> RW) -> REPL ()
modifyRW_ f = REPL (\ ref -> modifyIORef ref f)
@ -339,47 +349,51 @@ keepOne src as = case as of
[a] -> a
_ -> panic ("REPL: " ++ src) ["name clash in interface file"]
getFocusedEnv :: REPL (M.IfaceDecls,NameDisp)
getFocusedEnv :: REPL (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
-- 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)
return ( dyDecls `mappend` fDecls
, dyNames `M.shadowing` fNames
, dyDisp `mappend` fDisp)
getVars :: REPL (Map.Map P.QName M.IfaceDecl)
-- -- 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
(decls,_,_) <- getFocusedEnv
return (keepOne "getVars" `fmap` M.ifDecls decls)
getTSyns :: REPL (Map.Map P.QName T.TySyn)
getTSyns :: REPL (Map.Map M.Name T.TySyn)
getTSyns = do
(decls,_) <- getFocusedEnv
(decls,_,_) <- getFocusedEnv
return (keepOne "getTSyns" `fmap` M.ifTySyns decls)
getNewtypes :: REPL (Map.Map P.QName T.Newtype)
getNewtypes :: REPL (Map.Map M.Name T.Newtype)
getNewtypes = do
(decls,_) <- getFocusedEnv
(decls,_,_) <- getFocusedEnv
return (keepOne "getNewtypes" `fmap` M.ifNewtypes decls)
-- | Get visible variable names.
@ -399,7 +413,7 @@ getPropertyNames =
return [ getName x | (x,d) <- Map.toList xs,
T.PragmaProperty `elem` M.ifDeclPragmas d ]
getName :: P.QName -> String
getName :: M.Name -> String
getName = show . pp
getModuleEnv :: REPL M.ModuleEnv
@ -419,14 +433,32 @@ setDynEnv denv = do
-- | Given an existing qualified name, prefix it with a
-- relatively-unique string. We make it unique by prefixing with a
-- character @#@ that is not lexically valid in a module name.
uniqify :: P.QName -> REPL P.QName
uniqify (P.QName Nothing name) = do
i <- eNameSupply `fmap` getRW
modifyRW_ (\rw -> rw { eNameSupply = i+1 })
let modname' = P.mkModName [ '#' : ("Uniq_" ++ show i) ]
return (P.QName (Just modname') name)
uniqify qn =
panic "[REPL] uniqify" ["tried to uniqify a qualified name: " ++ pretty qn]
uniqify :: M.Name -> REPL M.Name
uniqify name =
case M.nameInfo name of
M.Declared ns ->
M.liftSupply (M.mkDeclared ns (M.nameIdent name) (M.nameLoc name))
M.Parameter ->
panic "[REPL] uniqify" ["tried to uniqify a parameter: " ++ pretty name]
-- uniqify (P.QName Nothing name) = do
-- i <- eNameSupply `fmap` getRW
-- modifyRW_ (\rw -> rw { eNameSupply = i+1 })
-- let modname' = P.mkModName [ '#' : ("Uniq_" ++ show i) ]
-- return (P.QName (Just modname') name)
-- uniqify qn =
-- panic "[REPL] uniqify" ["tried to uniqify a qualified name: " ++ pretty qn]
-- | Generate a fresh name using the given index. The name will reside within
-- the "<interactive>" namespace.
freshName :: I.Ident -> REPL M.Name
freshName i = M.liftSupply (M.mkDeclared I.interactiveName i emptyRange)
-- User Environment Interaction ------------------------------------------------

2
src/Cryptol/Symbolic.hs
View File

@ -21,7 +21,7 @@ import qualified Control.Exception as X
import qualified Data.SBV.Dynamic as SBV
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
import qualified Cryptol.ModuleSystem.Env as M
import qualified Cryptol.ModuleSystem.Base as M
import qualified Cryptol.ModuleSystem.Monad as M

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

@ -31,7 +31,7 @@ import Cryptol.Parser.AST ( Selector(..),Pragma(..), ppSelector
, Import(..), ImportSpec(..), ExportType(..)
, ExportSpec(..), isExportedBind
, isExportedType, Fixity(..) )
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName)
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent)
import Cryptol.Utils.Panic(panic)
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Solver.InfNat
@ -548,6 +548,20 @@ newtypeConType nt =
ePrim :: PrimMap -> Ident -> Expr
ePrim pm n = EVar (lookupPrimDecl n pm)
-- | Make an expression that is `error` pre-applied to a type and a message.
eError :: PrimMap -> Type -> String -> Expr
eError prims t str =
EApp (ETApp (ETApp (ePrim prims (packIdent "error")) t)
(tNum (length str))) (eString prims str)
eString :: PrimMap -> String -> Expr
eString prims str = EList (map (eChar prims) str) tChar
eChar :: PrimMap -> Char -> Expr
eChar prims c = ETApp (ETApp (ePrim prims (packIdent "demote")) (tNum v)) (tNum w)
where v = fromEnum c
w = 8 :: Int
--------------------------------------------------------------------------------

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

@ -32,6 +32,9 @@ import qualified Text.PrettyPrint as PJ
data NameDisp = EmptyNameDisp
| NameDisp (ModName -> Ident -> Maybe NameFormat)
instance Show NameDisp where
show _ = "<NameDisp>"
instance M.Monoid NameDisp where
mempty = EmptyNameDisp
@ -67,6 +70,10 @@ getNameFormat _ _ EmptyNameDisp = NotInScope
withNameDisp :: (NameDisp -> Doc) -> Doc
withNameDisp k = Doc (\disp -> runDoc disp (k disp))
-- | Fix the way that names are displayed inside of a doc.
fixNameDisp :: NameDisp -> Doc -> Doc
fixNameDisp disp (Doc f) = Doc (\ _ -> f disp)
-- Documents -------------------------------------------------------------------