mirror of
https://github.com/GaloisInc/cryptol.git
synced 2025-01-07 08:19:12 +03:00
parent
208119fbbf
commit
aa44dd7860
@ -49,6 +49,16 @@ data NamingEnv = NamingEnv { neExprs :: !(Map.Map PName [Name])
|
|||||||
-- ^ Expression-level fixity environment
|
-- ^ Expression-level fixity environment
|
||||||
} deriving (Show, Generic, NFData)
|
} deriving (Show, Generic, NFData)
|
||||||
|
|
||||||
|
-- | 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)
|
||||||
|
|
||||||
|
-- | 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)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
instance Monoid NamingEnv where
|
instance Monoid NamingEnv where
|
||||||
mempty =
|
mempty =
|
||||||
NamingEnv { neExprs = Map.empty
|
NamingEnv { neExprs = Map.empty
|
||||||
|
@ -238,7 +238,7 @@ vtop_decl :: { [TopDecl PName] }
|
|||||||
{ [exportDecl $1 Public (mkProperty $3 $4 $6)] }
|
{ [exportDecl $1 Public (mkProperty $3 $4 $6)] }
|
||||||
| mbDoc 'property' name '=' expr
|
| mbDoc 'property' name '=' expr
|
||||||
{ [exportDecl $1 Public (mkProperty $3 [] $5)] }
|
{ [exportDecl $1 Public (mkProperty $3 [] $5)] }
|
||||||
| mbDoc newtype { [exportNewtype Public $2] }
|
| mbDoc newtype { [exportNewtype Public $1 $2] }
|
||||||
| prim_bind { $1 }
|
| prim_bind { $1 }
|
||||||
| private_decls { $1 }
|
| private_decls { $1 }
|
||||||
|
|
||||||
|
@ -265,9 +265,10 @@ exportDecl mbDoc e d = Decl TopLevel { tlExport = e
|
|||||||
, tlDoc = mbDoc
|
, tlDoc = mbDoc
|
||||||
, tlValue = d }
|
, tlValue = d }
|
||||||
|
|
||||||
exportNewtype :: ExportType -> Newtype PName -> TopDecl PName
|
exportNewtype :: ExportType -> Maybe (Located String) -> Newtype PName ->
|
||||||
exportNewtype e n = TDNewtype TopLevel { tlExport = e
|
TopDecl PName
|
||||||
, tlDoc = Nothing
|
exportNewtype e d n = TDNewtype TopLevel { tlExport = e
|
||||||
|
, tlDoc = d
|
||||||
, tlValue = n }
|
, tlValue = n }
|
||||||
|
|
||||||
changeExport :: ExportType -> [TopDecl PName] -> [TopDecl PName]
|
changeExport :: ExportType -> [TopDecl PName] -> [TopDecl PName]
|
||||||
|
@ -803,7 +803,38 @@ helpCmd cmd
|
|||||||
case parseHelpName cmd of
|
case parseHelpName cmd of
|
||||||
Just qname ->
|
Just qname ->
|
||||||
do (env,rnEnv,nameEnv) <- getFocusedEnv
|
do (env,rnEnv,nameEnv) <- getFocusedEnv
|
||||||
name <- liftModuleCmd (M.renameVar rnEnv qname)
|
let vNames = M.lookupValNames qname rnEnv
|
||||||
|
tNames = M.lookupTypeNames qname rnEnv
|
||||||
|
|
||||||
|
mapM_ (showTypeHelp env nameEnv) tNames
|
||||||
|
mapM_ (showValHelp env nameEnv qname) vNames
|
||||||
|
Nothing ->
|
||||||
|
rPutStrLn ("Unable to parse name: " ++ cmd)
|
||||||
|
|
||||||
|
where
|
||||||
|
noInfo nameEnv name =
|
||||||
|
case M.nameInfo name of
|
||||||
|
M.Declared m -> rPrint $runDoc nameEnv ("Name defined in module" <+> pp m)
|
||||||
|
M.Parameter -> rPutStrLn "// No documentation is available."
|
||||||
|
|
||||||
|
showTypeHelp env nameEnv name =
|
||||||
|
case Map.lookup name (M.ifTySyns env) of
|
||||||
|
Nothing ->
|
||||||
|
case Map.lookup name (M.ifNewtypes env) of
|
||||||
|
Nothing -> noInfo nameEnv name
|
||||||
|
Just nt -> doShowTyHelp nameEnv decl (T.ntDoc nt)
|
||||||
|
where
|
||||||
|
decl = pp nt $$ (pp name <+> text ":" <+> pp (T.newtypeConType nt))
|
||||||
|
Just ts -> doShowTyHelp nameEnv (pp ts) (T.tsDoc ts)
|
||||||
|
|
||||||
|
doShowTyHelp nameEnv decl doc =
|
||||||
|
do rPutStrLn ""
|
||||||
|
rPrint (runDoc nameEnv (nest 4 decl))
|
||||||
|
case doc of
|
||||||
|
Nothing -> return ()
|
||||||
|
Just d -> rPutStrLn "" >> rPutStrLn d
|
||||||
|
|
||||||
|
showValHelp env nameEnv qname name =
|
||||||
case Map.lookup name (M.ifDecls env) of
|
case Map.lookup name (M.ifDecls env) of
|
||||||
Just M.IfaceDecl { .. } ->
|
Just M.IfaceDecl { .. } ->
|
||||||
do rPutStrLn ""
|
do rPutStrLn ""
|
||||||
@ -835,10 +866,12 @@ helpCmd cmd
|
|||||||
Just str -> rPutStrLn ('\n' : str)
|
Just str -> rPutStrLn ('\n' : str)
|
||||||
Nothing -> return ()
|
Nothing -> return ()
|
||||||
|
|
||||||
Nothing -> rPutStrLn "// No documentation is available."
|
_ -> case Map.lookup name (M.ifNewtypes env) of
|
||||||
|
Just _ -> return ()
|
||||||
|
Nothing -> noInfo nameEnv name
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Nothing ->
|
|
||||||
rPutStrLn ("Unable to parse name: " ++ cmd)
|
|
||||||
|
|
||||||
|
|
||||||
runShellCmd :: String -> REPL ()
|
runShellCmd :: String -> REPL ()
|
||||||
|
@ -26,7 +26,16 @@ import Data.Map (Map)
|
|||||||
import qualified Data.Map as Map
|
import qualified Data.Map as Map
|
||||||
import qualified Data.Set as Set
|
import qualified Data.Set as Set
|
||||||
|
|
||||||
data TyDecl = TS (P.TySyn Name) | PS (P.PropSyn Name) | NT (P.Newtype Name)
|
data TyDecl = TS (P.TySyn Name) (Maybe String)
|
||||||
|
| PS (P.PropSyn Name) (Maybe String)
|
||||||
|
| NT (P.Newtype Name) (Maybe String)
|
||||||
|
|
||||||
|
setDocString :: Maybe String -> TyDecl -> TyDecl
|
||||||
|
setDocString x d =
|
||||||
|
case d of
|
||||||
|
TS a _ -> TS a x
|
||||||
|
PS a _ -> PS a x
|
||||||
|
NT a _ -> NT a x
|
||||||
|
|
||||||
-- | Check for duplicate and recursive type synonyms.
|
-- | Check for duplicate and recursive type synonyms.
|
||||||
-- Returns the type-synonyms in dependency order.
|
-- Returns the type-synonyms in dependency order.
|
||||||
@ -39,7 +48,7 @@ orderTyDecls ts =
|
|||||||
concat `fmap` mapM check ordered
|
concat `fmap` mapM check ordered
|
||||||
|
|
||||||
where
|
where
|
||||||
toMap vs ty@(NT (P.Newtype x as fs)) =
|
toMap vs ty@(NT (P.Newtype x as fs) _) =
|
||||||
( thing x
|
( thing x
|
||||||
, x { thing = (ty, Set.toList $
|
, x { thing = (ty, Set.toList $
|
||||||
Set.difference
|
Set.difference
|
||||||
@ -49,7 +58,7 @@ orderTyDecls ts =
|
|||||||
}
|
}
|
||||||
)
|
)
|
||||||
|
|
||||||
toMap vs ty@(TS (P.TySyn x as t)) =
|
toMap vs ty@(TS (P.TySyn x as t) _) =
|
||||||
(thing x
|
(thing x
|
||||||
, x { thing = (ty, Set.toList $
|
, x { thing = (ty, Set.toList $
|
||||||
Set.difference (namesT vs t)
|
Set.difference (namesT vs t)
|
||||||
@ -57,16 +66,16 @@ orderTyDecls ts =
|
|||||||
}
|
}
|
||||||
)
|
)
|
||||||
|
|
||||||
toMap vs ty@(PS (P.PropSyn x as ps)) =
|
toMap vs ty@(PS (P.PropSyn x as ps) _) =
|
||||||
(thing x
|
(thing x
|
||||||
, x { thing = (ty, Set.toList $
|
, x { thing = (ty, Set.toList $
|
||||||
Set.difference (Set.unions (map (namesC vs) ps))
|
Set.difference (Set.unions (map (namesC vs) ps))
|
||||||
(Set.fromList (map P.tpName as)))
|
(Set.fromList (map P.tpName as)))
|
||||||
}
|
}
|
||||||
)
|
)
|
||||||
getN (TS (P.TySyn x _ _)) = thing x
|
getN (TS (P.TySyn x _ _) _) = thing x
|
||||||
getN (PS (P.PropSyn x _ _)) = thing x
|
getN (PS (P.PropSyn x _ _) _) = thing x
|
||||||
getN (NT x) = thing (P.nName x)
|
getN (NT x _) = thing (P.nName x)
|
||||||
|
|
||||||
check (AcyclicSCC x) = return [x]
|
check (AcyclicSCC x) = return [x]
|
||||||
|
|
||||||
@ -96,8 +105,9 @@ instance FromDecl (P.TopDecl Name) where
|
|||||||
toBind (P.Decl x) = toBind (P.tlValue x)
|
toBind (P.Decl x) = toBind (P.tlValue x)
|
||||||
toBind _ = Nothing
|
toBind _ = Nothing
|
||||||
|
|
||||||
toTyDecl (P.TDNewtype d) = Just (NT (P.tlValue d))
|
toTyDecl (P.TDNewtype d) = Just (NT (P.tlValue d) (thing <$> P.tlDoc d))
|
||||||
toTyDecl (P.Decl x) = toTyDecl (P.tlValue x)
|
toTyDecl (P.Decl x) = setDocString (thing <$> P.tlDoc x)
|
||||||
|
<$> toTyDecl (P.tlValue x)
|
||||||
toTyDecl _ = Nothing
|
toTyDecl _ = Nothing
|
||||||
|
|
||||||
isTopDecl _ = True
|
isTopDecl _ = True
|
||||||
@ -108,8 +118,8 @@ instance FromDecl (P.Decl Name) where
|
|||||||
toBind _ = Nothing
|
toBind _ = Nothing
|
||||||
|
|
||||||
toTyDecl (P.DLocated d _) = toTyDecl d
|
toTyDecl (P.DLocated d _) = toTyDecl d
|
||||||
toTyDecl (P.DType x) = Just (TS x)
|
toTyDecl (P.DType x) = Just (TS x Nothing)
|
||||||
toTyDecl (P.DProp x) = Just (PS x)
|
toTyDecl (P.DProp x) = Just (PS x Nothing)
|
||||||
toTyDecl _ = Nothing
|
toTyDecl _ = Nothing
|
||||||
|
|
||||||
isTopDecl _ = False
|
isTopDecl _ = False
|
||||||
|
@ -817,16 +817,16 @@ inferDs ds continue = checkTyDecls =<< orderTyDecls (mapMaybe toTyDecl ds)
|
|||||||
where
|
where
|
||||||
isTopLevel = isTopDecl (head ds)
|
isTopLevel = isTopDecl (head ds)
|
||||||
|
|
||||||
checkTyDecls (TS t : ts) =
|
checkTyDecls (TS t mbD : ts) =
|
||||||
do t1 <- checkTySyn t
|
do t1 <- checkTySyn t mbD
|
||||||
withTySyn t1 (checkTyDecls ts)
|
withTySyn t1 (checkTyDecls ts)
|
||||||
|
|
||||||
checkTyDecls (PS t : ts) =
|
checkTyDecls (PS t mbD : ts) =
|
||||||
do t1 <- checkPropSyn t
|
do t1 <- checkPropSyn t mbD
|
||||||
withTySyn t1 (checkTyDecls ts)
|
withTySyn t1 (checkTyDecls ts)
|
||||||
|
|
||||||
checkTyDecls (NT t : ts) =
|
checkTyDecls (NT t mbD : ts) =
|
||||||
do t1 <- checkNewtype t
|
do t1 <- checkNewtype t mbD
|
||||||
withNewtype t1 (checkTyDecls ts)
|
withNewtype t1 (checkTyDecls ts)
|
||||||
|
|
||||||
-- We checked all type synonyms, now continue with value-level definitions:
|
-- We checked all type synonyms, now continue with value-level definitions:
|
||||||
|
@ -54,8 +54,8 @@ checkSchema (P.Forall xs ps t mb) =
|
|||||||
Just r -> inRange r
|
Just r -> inRange r
|
||||||
|
|
||||||
-- | Check a type-synonym declaration.
|
-- | Check a type-synonym declaration.
|
||||||
checkTySyn :: P.TySyn Name -> InferM TySyn
|
checkTySyn :: P.TySyn Name -> Maybe String -> InferM TySyn
|
||||||
checkTySyn (P.TySyn x as t) =
|
checkTySyn (P.TySyn x as t) mbD =
|
||||||
do ((as1,t1),gs) <- collectGoals
|
do ((as1,t1),gs) <- collectGoals
|
||||||
$ inRange (srcRange x)
|
$ inRange (srcRange x)
|
||||||
$ do r <- withTParams False as (doCheckType t Nothing)
|
$ do r <- withTParams False as (doCheckType t Nothing)
|
||||||
@ -65,11 +65,12 @@ checkTySyn (P.TySyn x as t) =
|
|||||||
, tsParams = as1
|
, tsParams = as1
|
||||||
, tsConstraints = map (tRebuild . goal) gs
|
, tsConstraints = map (tRebuild . goal) gs
|
||||||
, tsDef = tRebuild t1
|
, tsDef = tRebuild t1
|
||||||
|
, tsDoc = mbD
|
||||||
}
|
}
|
||||||
|
|
||||||
-- | Check a constraint-synonym declaration.
|
-- | Check a constraint-synonym declaration.
|
||||||
checkPropSyn :: P.PropSyn Name -> InferM TySyn
|
checkPropSyn :: P.PropSyn Name -> Maybe String -> InferM TySyn
|
||||||
checkPropSyn (P.PropSyn x as ps) =
|
checkPropSyn (P.PropSyn x as ps) mbD =
|
||||||
do ((as1,t1),gs) <- collectGoals
|
do ((as1,t1),gs) <- collectGoals
|
||||||
$ inRange (srcRange x)
|
$ inRange (srcRange x)
|
||||||
$ do r <- withTParams False as (traverse checkProp ps)
|
$ do r <- withTParams False as (traverse checkProp ps)
|
||||||
@ -79,12 +80,13 @@ checkPropSyn (P.PropSyn x as ps) =
|
|||||||
, tsParams = as1
|
, tsParams = as1
|
||||||
, tsConstraints = map (tRebuild . goal) gs
|
, tsConstraints = map (tRebuild . goal) gs
|
||||||
, tsDef = tRebuild (pAnd t1)
|
, tsDef = tRebuild (pAnd t1)
|
||||||
|
, tsDoc = mbD
|
||||||
}
|
}
|
||||||
|
|
||||||
-- | Check a newtype declaration.
|
-- | Check a newtype declaration.
|
||||||
-- XXX: Do something with constraints.
|
-- XXX: Do something with constraints.
|
||||||
checkNewtype :: P.Newtype Name -> InferM Newtype
|
checkNewtype :: P.Newtype Name -> Maybe String -> InferM Newtype
|
||||||
checkNewtype (P.Newtype x as fs) =
|
checkNewtype (P.Newtype x as fs) mbD =
|
||||||
do ((as1,fs1),gs) <- collectGoals $
|
do ((as1,fs1),gs) <- collectGoals $
|
||||||
inRange (srcRange x) $
|
inRange (srcRange x) $
|
||||||
do r <- withTParams False as $
|
do r <- withTParams False as $
|
||||||
@ -100,6 +102,7 @@ checkNewtype (P.Newtype x as fs) =
|
|||||||
, ntParams = as1
|
, ntParams = as1
|
||||||
, ntConstraints = map goal gs
|
, ntConstraints = map goal gs
|
||||||
, ntFields = fs1
|
, ntFields = fs1
|
||||||
|
, ntDoc = mbD
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
@ -191,7 +194,8 @@ tySyn :: Bool -- ^ Should we check for scoped type vars.
|
|||||||
tySyn scoped x ts k =
|
tySyn scoped x ts k =
|
||||||
do mb <- kLookupTSyn x
|
do mb <- kLookupTSyn x
|
||||||
case mb of
|
case mb of
|
||||||
Just (tysyn@(TySyn f as ps def)) ->
|
Just (tysyn@(TySyn { tsName = f, tsParams = as
|
||||||
|
, tsConstraints = ps, tsDef = def })) ->
|
||||||
do (ts1,k1) <- appTy ts (kindOf tysyn)
|
do (ts1,k1) <- appTy ts (kindOf tysyn)
|
||||||
ts2 <- checkParams as ts1
|
ts2 <- checkParams as ts1
|
||||||
let su = zip as ts2
|
let su = zip as ts2
|
||||||
|
@ -135,6 +135,7 @@ data TySyn = TySyn { tsName :: Name -- ^ Name
|
|||||||
, tsParams :: [TParam] -- ^ Parameters
|
, tsParams :: [TParam] -- ^ Parameters
|
||||||
, tsConstraints :: [Prop] -- ^ Ensure body is OK
|
, tsConstraints :: [Prop] -- ^ Ensure body is OK
|
||||||
, tsDef :: Type -- ^ Definition
|
, tsDef :: Type -- ^ Definition
|
||||||
|
, tsDoc :: !(Maybe String) -- ^ Documentation
|
||||||
}
|
}
|
||||||
deriving (Show, Generic, NFData)
|
deriving (Show, Generic, NFData)
|
||||||
|
|
||||||
@ -147,6 +148,7 @@ data Newtype = Newtype { ntName :: Name
|
|||||||
, ntParams :: [TParam]
|
, ntParams :: [TParam]
|
||||||
, ntConstraints :: [Prop]
|
, ntConstraints :: [Prop]
|
||||||
, ntFields :: [(Ident,Type)]
|
, ntFields :: [(Ident,Type)]
|
||||||
|
, ntDoc :: Maybe String
|
||||||
} deriving (Show, Generic, NFData)
|
} deriving (Show, Generic, NFData)
|
||||||
|
|
||||||
|
|
||||||
@ -224,7 +226,7 @@ instance HasKind Type where
|
|||||||
TRec {} -> KType
|
TRec {} -> KType
|
||||||
|
|
||||||
instance HasKind TySyn where
|
instance HasKind TySyn where
|
||||||
kindOf (TySyn _ as _ t) = foldr (:->) (kindOf t) (map kindOf as)
|
kindOf ts = foldr (:->) (kindOf (tsDef ts)) (map kindOf (tsParams ts))
|
||||||
|
|
||||||
instance HasKind Newtype where
|
instance HasKind Newtype where
|
||||||
kindOf nt = foldr (:->) KType (map kindOf (ntParams nt))
|
kindOf nt = foldr (:->) KType (map kindOf (ntParams nt))
|
||||||
@ -702,10 +704,22 @@ instance PP TySyn where
|
|||||||
ppPrec = ppWithNamesPrec IntMap.empty
|
ppPrec = ppWithNamesPrec IntMap.empty
|
||||||
|
|
||||||
instance PP (WithNames TySyn) where
|
instance PP (WithNames TySyn) where
|
||||||
ppPrec _ (WithNames (TySyn n ps _ ty) ns) =
|
ppPrec _ (WithNames ts ns) =
|
||||||
text "type" <+> pp n <+> sep (map (ppWithNames ns1) ps) <+> char '='
|
text "type" <+> ctr <+> pp (tsName ts) <+>
|
||||||
<+> ppWithNames ns1 ty
|
sep (map (ppWithNames ns1) (tsParams ts)) <+> char '='
|
||||||
where ns1 = addTNames ps ns
|
<+> ppWithNames ns1 (tsDef ts)
|
||||||
|
where ns1 = addTNames (tsParams ts) ns
|
||||||
|
ctr = case kindResult (kindOf ts) of
|
||||||
|
KProp -> text "constraint"
|
||||||
|
_ -> empty
|
||||||
|
|
||||||
|
instance PP Newtype where
|
||||||
|
ppPrec = ppWithNamesPrec IntMap.empty
|
||||||
|
|
||||||
|
instance PP (WithNames Newtype) where
|
||||||
|
ppPrec _ (WithNames nt _) = ppNewtypeShort nt -- XXX: do the full thing?
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
instance PP (WithNames Type) where
|
instance PP (WithNames Type) where
|
||||||
|
Loading…
Reference in New Issue
Block a user