mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-12 04:17:04 +03:00
Use abstract interface to module Cryptol.ModuleSystem.Name
This makes it possible to change the representation of the Name type without breaking lots of other code.
This commit is contained in:
Brian Huffman
parent
c9e4fab6a8
commit
4976a8db3e
@ -204,7 +204,7 @@ importIfaces :: [P.Import] -> ModuleM IfaceDecls
|
||||
importIfaces is = foldMap ifPublic `fmap` mapM importIface is
|
||||
|
||||
moduleFile :: ModName -> String -> FilePath
|
||||
moduleFile (ModName ns) = addExtension (joinPath ns)
|
||||
moduleFile n = addExtension (joinPath (P.unModName n))
|
||||
|
||||
-- | Discover a module.
|
||||
findModule :: ModName -> ModuleM FilePath
|
||||
@ -250,7 +250,7 @@ findFile path = do
|
||||
possibleFiles paths = map (</> path) paths
|
||||
|
||||
preludeName :: P.ModName
|
||||
preludeName = P.ModName ["Cryptol"]
|
||||
preludeName = P.mkModName ["Cryptol"]
|
||||
|
||||
-- | Add the prelude to the import list if it's not already mentioned.
|
||||
addPrelude :: P.Module -> P.Module
|
||||
|
||||
@ -292,7 +292,7 @@ loadingModule = loading . FromModule
|
||||
-- | Push an "interactive" context onto the loading stack. A bit of a hack, as
|
||||
-- it uses a faked module name
|
||||
interactive :: ModuleM a -> ModuleM a
|
||||
interactive = loadingModule (P.ModName ["<interactive>"])
|
||||
interactive = loadingModule (P.mkModName ["<interactive>"])
|
||||
|
||||
loading :: ImportSource -> ModuleM a -> ModuleM a
|
||||
loading src m = ModuleT $ do
|
||||
|
||||
@ -1,23 +1,44 @@
|
||||
module Cryptol.ModuleSystem.Name where
|
||||
|
||||
type Ident = String
|
||||
|
||||
pack :: String -> Ident
|
||||
pack = id
|
||||
|
||||
unpack :: Ident -> String
|
||||
unpack = id
|
||||
|
||||
-- | Module names are just namespaces.
|
||||
--
|
||||
-- INVARIANT: the list of strings should never be empty in a valid module name.
|
||||
newtype ModName = ModName [String]
|
||||
newtype ModName = ModName [Ident]
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
data Name = Name String
|
||||
data Name = Name Ident
|
||||
| NewName Pass Int
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
data QName = QName (Maybe ModName) Name
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
unModName :: ModName -> [String]
|
||||
unModName (ModName ns) = map unpack ns
|
||||
|
||||
mkModName :: [String] -> ModName
|
||||
mkModName ns = ModName (map pack ns)
|
||||
|
||||
mkName :: String -> Name
|
||||
mkName n = Name (pack n)
|
||||
|
||||
-- XXX It would be nice to also mark this as a name that doesn't need to be
|
||||
-- resolved, if it's going to be created before renaming.
|
||||
mkPrim :: String -> QName
|
||||
mkPrim n = mkQual (ModName ["Cryptol"]) (Name n)
|
||||
mkPrim n = mkQual (ModName [pack "Cryptol"]) (Name (pack n))
|
||||
|
||||
asPrim :: QName -> Maybe String
|
||||
asPrim (QName (Just (ModName [m])) (Name n))
|
||||
| m == pack "Cryptol" = Just (unpack n)
|
||||
asPrim _ = Nothing
|
||||
|
||||
mkQual :: ModName -> Name -> QName
|
||||
mkQual = QName . Just
|
||||
|
||||
@ -374,10 +374,10 @@ translateProp ty = go =<< rnType True ty
|
||||
|
||||
TLocated t' r -> (`CLocated` r) <$> go t'
|
||||
|
||||
TUser (QName Nothing (Name p)) [l,r]
|
||||
| p == "==" -> pure (CEqual l r)
|
||||
| p == ">=" -> pure (CGeq l r)
|
||||
| p == "<=" -> pure (CGeq r l)
|
||||
TUser (QName Nothing p) [l,r]
|
||||
| p == mkName "==" -> pure (CEqual l r)
|
||||
| p == mkName ">=" -> pure (CGeq l r)
|
||||
| p == mkName "<=" -> pure (CGeq r l)
|
||||
|
||||
_ ->
|
||||
do record (InvalidConstraint ty)
|
||||
@ -398,15 +398,15 @@ rnType isProp = go
|
||||
TChar _ -> return t
|
||||
TInf -> return t
|
||||
|
||||
TUser (QName Nothing (Name n)) ps
|
||||
| n == "inf", null ps -> return TInf
|
||||
| n == "Bit", null ps -> return TBit
|
||||
TUser (QName Nothing n) ps
|
||||
| n == mkName "inf", null ps -> return TInf
|
||||
| n == mkName "Bit", null ps -> return TBit
|
||||
|
||||
| n == "min" -> TApp TCMin <$> traverse go ps
|
||||
| n == "max" -> TApp TCMax <$> traverse go ps
|
||||
| n == "lengthFromThen" -> TApp TCLenFromThen <$> traverse go ps
|
||||
| n == "lengthFromThenTo" -> TApp TCLenFromThenTo <$> traverse go ps
|
||||
| n == "width" -> TApp TCWidth <$> traverse go ps
|
||||
| n == mkName "min" -> TApp TCMin <$> traverse go ps
|
||||
| n == mkName "max" -> TApp TCMax <$> traverse go ps
|
||||
| n == mkName "lengthFromThen" -> TApp TCLenFromThen <$> traverse go ps
|
||||
| n == mkName "lengthFromThenTo" -> TApp TCLenFromThenTo <$> traverse go ps
|
||||
| n == mkName "width" -> TApp TCWidth <$> traverse go ps
|
||||
|
||||
TUser qn ps -> TUser <$> renameType qn <*> traverse go ps
|
||||
TApp f xs -> TApp f <$> traverse go xs
|
||||
@ -463,7 +463,7 @@ mkTInfix t (op,_) z =
|
||||
renameTypeOp :: Bool -> Located QName -> RenameM (TOp,Fixity)
|
||||
renameTypeOp isProp op =
|
||||
do let sym = unqual (thing op)
|
||||
props = [ Name "==", Name ">=", Name "<=" ]
|
||||
props = [ mkName "==", mkName ">=", mkName "<=" ]
|
||||
lkp = do n <- Map.lookup (thing op) tfunNames
|
||||
(fAssoc,fLevel) <- Map.lookup n tBinOpPrec
|
||||
return (n,Fixity { .. })
|
||||
|
||||
@ -150,7 +150,7 @@ vmodule :: { Module }
|
||||
{ let { (is,ts) = $2
|
||||
-- XXX make a location from is and ts
|
||||
; modName = Located { srcRange = emptyRange
|
||||
, thing = ModName ["Main"]
|
||||
, thing = mkModName ["Main"]
|
||||
}
|
||||
} in Module modName is ts }
|
||||
|
||||
@ -377,25 +377,25 @@ iexpr :: { Expr }
|
||||
expr10 :: { Expr }
|
||||
: aexprs { mkEApp $1 }
|
||||
|
||||
| '-' expr10 %prec NEG { at ($1,$2) $ EApp (at $1 (EVar (mkUnqual (Name "negate")))) $2 }
|
||||
| '~' expr10 { at ($1,$2) $ EApp (at $1 (EVar (mkUnqual (Name "complement")))) $2 }
|
||||
| '-' expr10 %prec NEG { at ($1,$2) $ EApp (at $1 (EVar (mkUnqual (mkName "negate")))) $2 }
|
||||
| '~' expr10 { at ($1,$2) $ EApp (at $1 (EVar (mkUnqual (mkName "complement")))) $2 }
|
||||
|
||||
qop :: { LQName }
|
||||
: op { fmap mkUnqual $1 }
|
||||
| QOP { let Token (Op (Other ns i)) _ = thing $1
|
||||
in mkQual (ModName ns) (Name i) A.<$ $1 }
|
||||
in mkQual (mkModName ns) (mkName i) A.<$ $1 }
|
||||
|
||||
op :: { LName }
|
||||
: OP { let Token (Op (Other [] str)) _ = thing $1
|
||||
in Name str A.<$ $1 }
|
||||
in mkName str A.<$ $1 }
|
||||
|
||||
-- special cases for operators that are re-used elsewhere
|
||||
| '*' { Located $1 $ Name "*" }
|
||||
| '+' { Located $1 $ Name "+" }
|
||||
| '-' { Located $1 $ Name "-" }
|
||||
| '~' { Located $1 $ Name "~" }
|
||||
| '^^' { Located $1 $ Name "^^" }
|
||||
| '#' { Located $1 $ Name "#" }
|
||||
| '*' { Located $1 $ mkName "*" }
|
||||
| '+' { Located $1 $ mkName "+" }
|
||||
| '-' { Located $1 $ mkName "-" }
|
||||
| '~' { Located $1 $ mkName "~" }
|
||||
| '^^' { Located $1 $ mkName "^^" }
|
||||
| '#' { Located $1 $ mkName "#" }
|
||||
|
||||
ops :: { [LName] }
|
||||
: op { [$1] }
|
||||
@ -609,19 +609,19 @@ field_types :: { [Named Type] }
|
||||
|
||||
name :: { LName }
|
||||
: IDENT { $1 { thing = getName $1 } }
|
||||
| 'x' { Located { srcRange = $1, thing = Name "x" }}
|
||||
| 'private' { Located { srcRange = $1, thing = Name "private" } }
|
||||
| 'as' { Located { srcRange = $1, thing = Name "as" } }
|
||||
| 'hiding' { Located { srcRange = $1, thing = Name "hiding" } }
|
||||
| 'x' { Located { srcRange = $1, thing = mkName "x" }}
|
||||
| 'private' { Located { srcRange = $1, thing = mkName "private" } }
|
||||
| 'as' { Located { srcRange = $1, thing = mkName "as" } }
|
||||
| 'hiding' { Located { srcRange = $1, thing = mkName "hiding" } }
|
||||
|
||||
|
||||
modName :: { Located ModName }
|
||||
: qname { mkModName $1 }
|
||||
: qname { mkLModName $1 }
|
||||
|
||||
qname :: { Located QName }
|
||||
: name { fmap mkUnqual $1 }
|
||||
| QIDENT { let Token (Ident ns i) _ = thing $1
|
||||
in mkQual (ModName ns) (Name i) A.<$ $1 }
|
||||
in mkQual (mkModName ns) (mkName i) A.<$ $1 }
|
||||
|
||||
help_name :: { Located QName }
|
||||
: qname { $1 }
|
||||
|
||||
@ -15,7 +15,7 @@
|
||||
module Cryptol.Parser.AST
|
||||
( -- * Names
|
||||
ModName(..), {-splitNamespace, parseModName, nsChar,-} modRange
|
||||
, QName(..), mkPrim, mkQual, mkUnqual, unqual
|
||||
, QName(..), mkModName, unModName, mkName, mkPrim, asPrim, mkQual, mkUnqual, unqual
|
||||
, Name(..)
|
||||
, Named(..)
|
||||
, Pass(..)
|
||||
@ -634,8 +634,8 @@ wrap contextPrec myPrec doc = if myPrec < contextPrec then parens doc else doc
|
||||
|
||||
isPrefixOp :: Expr -> Maybe Doc
|
||||
isPrefixOp (ELocated e _) = isPrefixOp e
|
||||
isPrefixOp e@(EVar (QName Nothing (Name n))) | n == "-" = Just (pp e)
|
||||
| n == "~" = Just (pp e)
|
||||
isPrefixOp e@(EVar (QName Nothing n)) | n == mkName "-" = Just (pp e)
|
||||
| n == mkName "~" = Just (pp e)
|
||||
isPrefixOp _ = Nothing
|
||||
|
||||
isEApp :: Expr -> Maybe (Expr, Expr)
|
||||
|
||||
@ -121,7 +121,7 @@ noPat pat =
|
||||
r <- getRange
|
||||
let qx = mkUnqual x
|
||||
qtmp = mkUnqual tmp
|
||||
prim = EVar (mkUnqual (Name "splitAt"))
|
||||
prim = EVar (mkUnqual (mkName "splitAt"))
|
||||
bTmp = simpleBind (Located r qtmp) (EApp prim (EVar qx))
|
||||
b1 = sel a1 qtmp (TupleSel 0 (Just 2))
|
||||
b2 = sel a2 qtmp (TupleSel 1 (Just 2))
|
||||
|
||||
@ -108,8 +108,8 @@ errorMessage r x = P $ \_ _ _ -> Left (HappyErrorMsg r x)
|
||||
customError :: String -> Located Token -> ParseM a
|
||||
customError x t = P $ \_ _ _ -> Left (HappyErrorMsg (srcRange t) x)
|
||||
|
||||
mkModName :: LQName -> Located ModName
|
||||
mkModName = fmap $ \ (QName mb (Name n)) ->
|
||||
mkLModName :: LQName -> Located ModName
|
||||
mkLModName = fmap $ \ (QName mb (Name n)) ->
|
||||
case mb of
|
||||
Just (ModName ns) -> ModName (ns ++ [n])
|
||||
Nothing -> ModName [n]
|
||||
@ -129,7 +129,7 @@ mkSchema xs ps t = Forall xs ps t Nothing
|
||||
|
||||
getName :: Located Token -> Name
|
||||
getName l = case thing l of
|
||||
Token (Ident [] x) _ -> Name x
|
||||
Token (Ident [] x) _ -> mkName x
|
||||
_ -> panic "[Parser] getName" ["not an Ident:", show l]
|
||||
|
||||
getNum :: Located Token -> Integer
|
||||
@ -262,7 +262,7 @@ exprToNumT r expr =
|
||||
-- It is used to represent anonymous type applications.
|
||||
anonRecord :: Maybe Range -> [Type] -> Type
|
||||
anonRecord ~(Just r) ts = TRecord (map toField ts)
|
||||
where noName = Located { srcRange = r, thing = Name "" }
|
||||
where noName = Located { srcRange = r, thing = mkName "" }
|
||||
toField t = Named { name = noName, value = t }
|
||||
|
||||
exportDecl :: Maybe (Located String) -> ExportType -> Decl -> TopDecl
|
||||
@ -283,18 +283,18 @@ changeExport e = map change
|
||||
change td@Include{} = td
|
||||
|
||||
mkTypeInst :: Named Type -> TypeInst
|
||||
mkTypeInst x | thing (name x) == Name "" = PosInst (value x)
|
||||
| otherwise = NamedInst x
|
||||
mkTypeInst x | thing (name x) == mkName "" = PosInst (value x)
|
||||
| otherwise = NamedInst x
|
||||
|
||||
|
||||
mkTParam :: Located Name -> Maybe Kind -> ParseM TParam
|
||||
mkTParam Located { srcRange = rng, thing = n } k
|
||||
| Name "width" <- n = errorMessage rng "`width` is not a valid type parameter name."
|
||||
| n == mkName "width" = errorMessage rng "`width` is not a valid type parameter name."
|
||||
| otherwise = return (TParam n k (Just rng))
|
||||
|
||||
mkTySyn :: Located Name -> [TParam] -> Type -> ParseM Decl
|
||||
mkTySyn n ps b
|
||||
| Name "width" <- thing n = errorMessage (srcRange n) "`width` is not a valid type synonym name."
|
||||
| thing n == mkName "width" = errorMessage (srcRange n) "`width` is not a valid type synonym name."
|
||||
| otherwise = return $ DType $ TySyn (fmap mkUnqual n) ps b
|
||||
|
||||
polyTerm :: Range -> Integer -> Integer -> ParseM (Bool, Integer)
|
||||
@ -433,13 +433,13 @@ mkProp ty =
|
||||
-- these can be translated right away
|
||||
prefixProp r f xs =
|
||||
case f of
|
||||
QName Nothing (Name "Arith") | [x] <- xs ->
|
||||
QName Nothing n | n == mkName "Arith", [x] <- xs ->
|
||||
return [CLocated (CArith x) r]
|
||||
|
||||
QName Nothing (Name "fin") | [x] <- xs ->
|
||||
QName Nothing n | n == mkName "fin", [x] <- xs ->
|
||||
return [CLocated (CFin x) r]
|
||||
|
||||
QName Nothing (Name "Cmp") | [x] <- xs ->
|
||||
QName Nothing n | n == mkName "Cmp", [x] <- xs ->
|
||||
return [CLocated (CCmp x) r]
|
||||
|
||||
_ -> errorMessage r "Invalid constraint"
|
||||
|
||||
@ -21,7 +21,7 @@ translateExprToNumT :: Expr -> Maybe Type
|
||||
translateExprToNumT expr =
|
||||
case expr of
|
||||
ELocated e r -> (`TLocated` r) `fmap` translateExprToNumT e
|
||||
EVar (QName Nothing (Name "width")) -> mkFun TCWidth
|
||||
EVar (QName Nothing n) | n == mkName "width" -> mkFun TCWidth
|
||||
EVar x -> return (TUser x [])
|
||||
ELit x -> cvtLit x
|
||||
EApp e1 e2 -> do t1 <- translateExprToNumT e1
|
||||
|
||||
@ -26,6 +26,7 @@ import Cryptol.Eval.Type(evalTF)
|
||||
import Cryptol.Eval.Value
|
||||
import Cryptol.Testing.Random (randomValue)
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.ModuleSystem.Name (Ident, pack)
|
||||
|
||||
import Data.List (sortBy,transpose,genericTake,genericReplicate,genericSplitAt,genericIndex)
|
||||
import Data.Ord (comparing)
|
||||
@ -83,14 +84,14 @@ instance Bits Bool where
|
||||
-- Primitives ------------------------------------------------------------------
|
||||
|
||||
evalPrim :: Decl -> Value
|
||||
evalPrim Decl { dName = QName (Just (ModName ["Cryptol"])) (Name prim), .. }
|
||||
| Just val <- Map.lookup prim primTable = val
|
||||
evalPrim Decl { dName = QName (Just m) (Name prim), .. }
|
||||
| m == mkModName ["Cryptol"], Just val <- Map.lookup prim primTable = val
|
||||
|
||||
evalPrim Decl { .. } =
|
||||
panic "Eval" [ "Unimplemented primitive", show dName ]
|
||||
|
||||
primTable :: Map.Map String Value
|
||||
primTable = Map.fromList
|
||||
primTable :: Map.Map Ident Value
|
||||
primTable = Map.fromList $ map (\(n, v) -> (pack n, v))
|
||||
[ ("+" , binary (arithBinary (liftBinArith (+))))
|
||||
, ("-" , binary (arithBinary (liftBinArith (-))))
|
||||
, ("*" , binary (arithBinary (liftBinArith (*))))
|
||||
|
||||
@ -10,7 +10,7 @@ module Cryptol.Prims.Syntax
|
||||
( TFun(..), tBinOpPrec, tfunNames
|
||||
) where
|
||||
|
||||
import Cryptol.ModuleSystem.Name (QName,Name(Name),mkUnqual)
|
||||
import Cryptol.ModuleSystem.Name (QName,Name(Name),mkUnqual,pack)
|
||||
import Cryptol.Utils.PP
|
||||
import qualified Data.Map as Map
|
||||
|
||||
@ -65,7 +65,7 @@ tfunNames = Map.fromList
|
||||
, tprim "lengthFromThenTo" TCLenFromThenTo
|
||||
]
|
||||
where
|
||||
tprim n p = (mkUnqual (Name n), p)
|
||||
tprim n p = (mkUnqual (Name (pack n)), p)
|
||||
|
||||
instance PP TFun where
|
||||
ppPrec _ tcon =
|
||||
|
||||
@ -485,7 +485,7 @@ mkSolverResult :: String
|
||||
-> (T.Type, T.Expr)
|
||||
mkSolverResult thing result earg = (rty, re)
|
||||
where
|
||||
rName = T.Name "result"
|
||||
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
|
||||
@ -493,7 +493,7 @@ mkSolverResult thing result earg = (rty, re)
|
||||
where
|
||||
go [] fs _ = fs
|
||||
go ((t, e):tes') fs n = go tes' (((argName, t), (argName, e)):fs) (n+1)
|
||||
where argName = T.Name ("arg" ++ show n)
|
||||
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"))
|
||||
@ -839,7 +839,7 @@ replEvalExpr expr =
|
||||
-- it to the current dynamic environment
|
||||
bindItVariable :: T.Type -> T.Expr -> REPL ()
|
||||
bindItVariable ty expr = do
|
||||
let it = T.QName Nothing (P.Name "it")
|
||||
let it = T.QName Nothing (P.mkName "it")
|
||||
freshIt <- uniqify it
|
||||
let dg = T.NonRecursive decl
|
||||
schema = T.Forall { T.sVars = []
|
||||
|
||||
@ -10,6 +10,7 @@
|
||||
{-# LANGUAGE DeriveDataTypeable #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
|
||||
module Cryptol.REPL.Monad (
|
||||
-- * REPL Monad
|
||||
@ -351,7 +352,7 @@ getFocusedEnv = do
|
||||
let (decls,names) = M.focusedEnv me
|
||||
edecls = M.ifDecls dyDecls
|
||||
-- is this QName something the user might actually type?
|
||||
isShadowed (qn@(P.QName (Just (P.ModName ['#':_])) name), _) =
|
||||
isShadowed (qn@(P.QName (Just (P.unModName -> ['#':_])) name), _) =
|
||||
case Map.lookup localName neExprs of
|
||||
Nothing -> False
|
||||
Just uniqueNames -> isNamed uniqueNames
|
||||
@ -422,7 +423,7 @@ 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.ModName [ '#' : ("Uniq_" ++ show i) ]
|
||||
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]
|
||||
|
||||
@ -18,9 +18,10 @@ import Data.Ord (comparing)
|
||||
import Cryptol.Eval.Value (BitWord(..))
|
||||
import Cryptol.Prims.Eval (binary, unary, tlamN)
|
||||
import Cryptol.Symbolic.Value
|
||||
import Cryptol.TypeCheck.AST (ModName(..),QName(..),Name(..),Decl(..))
|
||||
import Cryptol.TypeCheck.AST (QName(..),Name(..),Decl(..),mkModName,mkName)
|
||||
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..), nMul)
|
||||
import Cryptol.Utils.Panic
|
||||
import Cryptol.ModuleSystem.Name (Ident, pack)
|
||||
|
||||
import qualified Data.SBV.Dynamic as SBV
|
||||
import qualified Data.Map as Map
|
||||
@ -35,15 +36,15 @@ traverseSnd f (x, y) = (,) x <$> f y
|
||||
-- Primitives ------------------------------------------------------------------
|
||||
|
||||
evalPrim :: Decl -> Value
|
||||
evalPrim Decl { dName = QName (Just (ModName ["Cryptol"])) (Name prim), .. }
|
||||
| Just val <- Map.lookup prim primTable = val
|
||||
evalPrim Decl { dName = QName (Just m) (Name prim), .. }
|
||||
| m == mkModName ["Cryptol"], Just val <- Map.lookup prim primTable = val
|
||||
|
||||
evalPrim Decl { .. } =
|
||||
panic "Eval" [ "Unimplemented primitive", show dName ]
|
||||
|
||||
-- See also Cryptol.Prims.Eval.primTable
|
||||
primTable :: Map.Map String Value
|
||||
primTable = Map.fromList
|
||||
primTable :: Map.Map Ident Value
|
||||
primTable = Map.fromList $ map (\(n, v) -> (pack n, v))
|
||||
[ ("True" , VBit SBV.svTrue)
|
||||
, ("False" , VBit SBV.svFalse)
|
||||
, ("demote" , ecDemoteV) -- Converts a numeric type into its corresponding value.
|
||||
|
||||
@ -15,6 +15,7 @@ import Cryptol.TypeCheck.Subst
|
||||
import qualified Cryptol.ModuleSystem as M
|
||||
import qualified Cryptol.ModuleSystem.Env as M
|
||||
import qualified Cryptol.ModuleSystem.Monad as M
|
||||
import Cryptol.ModuleSystem.Name (unpack)
|
||||
|
||||
import Data.List (intercalate)
|
||||
import Data.Map (Map)
|
||||
@ -241,12 +242,12 @@ freshName (QName m name) tys = do
|
||||
let go = if name' `elem` bNames
|
||||
then loop (1 :: Integer)
|
||||
else name'
|
||||
return $ QName m (Name go)
|
||||
return $ QName m (mkName go)
|
||||
|
||||
matchingBoundNames :: (Maybe ModName) -> SpecM [String]
|
||||
matchingBoundNames m = do
|
||||
qns <- allPublicQNames <$> liftSpecT M.getModuleEnv
|
||||
return [ n | QName m' (Name n) <- qns , m == m' ]
|
||||
return [ unpack n | QName m' (Name n) <- qns , m == m' ]
|
||||
|
||||
reifyName :: Name -> [Type] -> String
|
||||
reifyName name tys = intercalate "_" (showName name : concatMap showT tys)
|
||||
@ -287,9 +288,9 @@ reifyName name tys = intercalate "_" (showName name : concatMap showT tys)
|
||||
TupleSel _ sig -> "tup" : maybe [] ((:[]) . show) sig
|
||||
RecordSel x sig -> "rec" : showName x : map showName (maybe [] id sig)
|
||||
ListSel _ sig -> "list" : maybe [] ((:[]) . show) sig
|
||||
showName nm =
|
||||
showName nm =
|
||||
case nm of
|
||||
Name s -> s
|
||||
Name s -> unpack s
|
||||
NewName _ n -> "x" ++ show n
|
||||
showTF tf =
|
||||
case tf of
|
||||
|
||||
@ -68,7 +68,7 @@ tcExpr e0 inp = runInferM inp
|
||||
_ -> do res <- inferBinds True False
|
||||
[ P.Bind
|
||||
{ P.bName = P.Located (inpRange inp)
|
||||
$ mkUnqual (P.Name "(expression)")
|
||||
$ mkUnqual (P.mkName "(expression)")
|
||||
, P.bParams = []
|
||||
, P.bDef = P.Located (inpRange inp) (P.DExpr expr)
|
||||
, P.bPragmas = []
|
||||
|
||||
@ -13,7 +13,7 @@
|
||||
module Cryptol.TypeCheck.AST
|
||||
( module Cryptol.TypeCheck.AST
|
||||
, TFun(..)
|
||||
, Name(..), QName(..), mkUnqual, unqual
|
||||
, Name(..), QName(..), mkModName, mkName, mkUnqual, unqual
|
||||
, ModName(..)
|
||||
, Selector(..)
|
||||
, Import(..)
|
||||
@ -24,12 +24,13 @@ module Cryptol.TypeCheck.AST
|
||||
, Fixity(..)
|
||||
) where
|
||||
|
||||
import Cryptol.ModuleSystem.Name (mkQual)
|
||||
import Cryptol.ModuleSystem.Name (mkQual, mkName)
|
||||
import Cryptol.Prims.Syntax
|
||||
import Cryptol.Parser.AST ( Name(..), Selector(..),Pragma(..), ppSelector
|
||||
, Import(..), ImportSpec(..), ExportType(..)
|
||||
, ExportSpec(..), ModName(..), isExportedBind
|
||||
, isExportedType, QName(..), mkUnqual, unqual
|
||||
, mkModName
|
||||
, Fixity(..) )
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.TypeCheck.PP
|
||||
@ -402,7 +403,7 @@ tBit :: Type
|
||||
tBit = TCon (TC TCBit) []
|
||||
|
||||
ePrim :: String -> Expr
|
||||
ePrim n = EVar (mkQual (ModName ["Cryptol"]) (Name n))
|
||||
ePrim n = EVar (mkQual (mkModName ["Cryptol"]) (mkName n))
|
||||
|
||||
eTrue :: Expr
|
||||
eTrue = ePrim "True"
|
||||
|
||||
@ -68,7 +68,7 @@ desugarLiteral :: Bool -> P.Literal -> InferM P.Expr
|
||||
desugarLiteral fixDec lit =
|
||||
do l <- curRange
|
||||
let named (x,y) = P.NamedInst
|
||||
P.Named { name = Located l (Name x), value = P.TNum y }
|
||||
P.Named { name = Located l (mkName x), value = P.TNum y }
|
||||
demote fs = P.EAppT (P.EVar (P.mkPrim "demote")) (map named fs)
|
||||
|
||||
return $ case lit of
|
||||
@ -223,7 +223,7 @@ checkE expr tGoal =
|
||||
lstT = totLen .-. tNum (1::Int)
|
||||
|
||||
appTys (P.EVar (P.mkPrim "fromTo"))
|
||||
[ Located rng (Just (mkUnqual (Name x)), y)
|
||||
[ Located rng (Just (mkUnqual (mkName x)), y)
|
||||
| (x,y) <- [ ("first",fstT), ("last", lstT), ("bits", bit) ]
|
||||
] tGoal
|
||||
|
||||
@ -244,7 +244,7 @@ checkE expr tGoal =
|
||||
(P.EVar (P.mkPrim "fromThenTo"), [ ("next",t2), ("last",t3) ])
|
||||
|
||||
let e' = P.EAppT c
|
||||
[ P.NamedInst P.Named { name = Located l (Name x), value = y }
|
||||
[ P.NamedInst P.Named { name = Located l (mkName x), value = y }
|
||||
| (x,y) <- ("first",t1) : fs
|
||||
]
|
||||
|
||||
@ -305,7 +305,7 @@ checkE expr tGoal =
|
||||
do l <- curRange
|
||||
checkE (P.EAppT (P.EVar (P.mkPrim "demote"))
|
||||
[P.NamedInst
|
||||
P.Named { name = Located l (Name "val"), value = t }]) tGoal
|
||||
P.Named { name = Located l (mkName "val"), value = t }]) tGoal
|
||||
|
||||
P.EFun ps e -> checkFun (text "anonymous function") ps e tGoal
|
||||
|
||||
|
||||
@ -10,6 +10,7 @@
|
||||
|
||||
{-# LANGUAGE Safe #-}
|
||||
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
|
||||
module Cryptol.TypeCheck.InferTypes where
|
||||
|
||||
@ -505,7 +506,7 @@ instance PP ConstraintSource where
|
||||
ppUse :: Expr -> Doc
|
||||
ppUse expr =
|
||||
case expr of
|
||||
EVar (QName (Just (ModName ["Cryptol"])) (Name prim))
|
||||
EVar (P.asPrim -> Just prim)
|
||||
| prim == "demote" -> text "literal or demoted expression"
|
||||
| prim == "infFrom" -> text "infinite enumeration"
|
||||
| prim == "infFromThen" -> text "infinite enumeration (with step)"
|
||||
|
||||
@ -220,7 +220,7 @@ fixNameEnv :: NameEnv -> Doc -> Doc
|
||||
fixNameEnv env (Doc f) = Doc (\_ -> f env)
|
||||
|
||||
instance PP ModName where
|
||||
ppPrec _ (ModName ns) = hcat (punctuate (text "::") (map text ns))
|
||||
ppPrec _ (ModName ns) = hcat (punctuate (text "::") (map (text . unpack) ns))
|
||||
|
||||
instance PP QName where
|
||||
ppPrec _ qn = withNameEnv $ \ names ->
|
||||
@ -229,7 +229,7 @@ instance PP QName where
|
||||
in optParens isInfix (mbNs <> pp n)
|
||||
|
||||
instance PP Name where
|
||||
ppPrec _ (Name x) = text x
|
||||
ppPrec _ (Name x) = text (unpack x)
|
||||
-- XXX: This may clash with user-specified names.
|
||||
ppPrec _ (NewName p x) = text "__" <> passName p <> int x
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user