diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index 7b657b29..f0097689 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -49,6 +49,16 @@ data NamingEnv = NamingEnv { neExprs :: !(Map.Map PName [Name]) -- ^ Expression-level fixity environment } 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 mempty = NamingEnv { neExprs = Map.empty diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index c8d74257..741552d5 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -238,7 +238,7 @@ vtop_decl :: { [TopDecl PName] } { [exportDecl $1 Public (mkProperty $3 $4 $6)] } | mbDoc 'property' name '=' expr { [exportDecl $1 Public (mkProperty $3 [] $5)] } - | mbDoc newtype { [exportNewtype Public $2] } + | mbDoc newtype { [exportNewtype Public $1 $2] } | prim_bind { $1 } | private_decls { $1 } diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index fd4cc9e2..c299e43f 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -265,10 +265,11 @@ exportDecl mbDoc e d = Decl TopLevel { tlExport = e , tlDoc = mbDoc , tlValue = d } -exportNewtype :: ExportType -> Newtype PName -> TopDecl PName -exportNewtype e n = TDNewtype TopLevel { tlExport = e - , tlDoc = Nothing - , tlValue = n } +exportNewtype :: ExportType -> Maybe (Located String) -> Newtype PName -> + TopDecl PName +exportNewtype e d n = TDNewtype TopLevel { tlExport = e + , tlDoc = d + , tlValue = n } changeExport :: ExportType -> [TopDecl PName] -> [TopDecl PName] changeExport e = map change diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 4e514c31..2457b8e9 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -803,43 +803,76 @@ helpCmd cmd case parseHelpName cmd of Just qname -> do (env,rnEnv,nameEnv) <- getFocusedEnv - name <- liftModuleCmd (M.renameVar rnEnv qname) - case Map.lookup name (M.ifDecls env) of - Just M.IfaceDecl { .. } -> - do rPutStrLn "" - - let property - | P.PragmaProperty `elem` ifDeclPragmas = text "property" - | otherwise = empty - rPrint $ runDoc nameEnv - $ nest 4 - $ property - <+> pp qname - <+> colon - <+> pp (ifDeclSig) - - let mbFix = ifDeclFixity `mplus` - (guard ifDeclInfix >> return P.defaultFixity) - case mbFix of - Just f -> - let msg = "Precedence " ++ show (P.fLevel f) ++ ", " ++ - (case P.fAssoc f of - P.LeftAssoc -> "associates to the left." - P.RightAssoc -> "associates to the right." - P.NonAssoc -> "does not associate.") - - in rPutStrLn ('\n' : msg) - Nothing -> return () - - case ifDeclDoc of - Just str -> rPutStrLn ('\n' : str) - Nothing -> return () - - Nothing -> rPutStrLn "// No documentation is available." + 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 + Just M.IfaceDecl { .. } -> + do rPutStrLn "" + + let property + | P.PragmaProperty `elem` ifDeclPragmas = text "property" + | otherwise = empty + rPrint $ runDoc nameEnv + $ nest 4 + $ property + <+> pp qname + <+> colon + <+> pp (ifDeclSig) + + let mbFix = ifDeclFixity `mplus` + (guard ifDeclInfix >> return P.defaultFixity) + case mbFix of + Just f -> + let msg = "Precedence " ++ show (P.fLevel f) ++ ", " ++ + (case P.fAssoc f of + P.LeftAssoc -> "associates to the left." + P.RightAssoc -> "associates to the right." + P.NonAssoc -> "does not associate.") + + in rPutStrLn ('\n' : msg) + Nothing -> return () + + case ifDeclDoc of + Just str -> rPutStrLn ('\n' : str) + Nothing -> return () + + _ -> case Map.lookup name (M.ifNewtypes env) of + Just _ -> return () + Nothing -> noInfo nameEnv name + + + + runShellCmd :: String -> REPL () runShellCmd cmd diff --git a/src/Cryptol/TypeCheck/Depends.hs b/src/Cryptol/TypeCheck/Depends.hs index 38c6d4c2..243a2f5e 100644 --- a/src/Cryptol/TypeCheck/Depends.hs +++ b/src/Cryptol/TypeCheck/Depends.hs @@ -26,7 +26,16 @@ import Data.Map (Map) import qualified Data.Map as Map 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. -- Returns the type-synonyms in dependency order. @@ -39,7 +48,7 @@ orderTyDecls ts = concat `fmap` mapM check ordered where - toMap vs ty@(NT (P.Newtype x as fs)) = + toMap vs ty@(NT (P.Newtype x as fs) _) = ( thing x , x { thing = (ty, Set.toList $ 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 , x { thing = (ty, Set.toList $ 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 , x { thing = (ty, Set.toList $ Set.difference (Set.unions (map (namesC vs) ps)) (Set.fromList (map P.tpName as))) } ) - getN (TS (P.TySyn x _ _)) = thing x - getN (PS (P.PropSyn x _ _)) = thing x - getN (NT x) = thing (P.nName x) + getN (TS (P.TySyn x _ _) _) = thing x + getN (PS (P.PropSyn x _ _) _) = thing x + getN (NT x _) = thing (P.nName 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 _ = Nothing - toTyDecl (P.TDNewtype d) = Just (NT (P.tlValue d)) - toTyDecl (P.Decl x) = toTyDecl (P.tlValue x) + toTyDecl (P.TDNewtype d) = Just (NT (P.tlValue d) (thing <$> P.tlDoc d)) + toTyDecl (P.Decl x) = setDocString (thing <$> P.tlDoc x) + <$> toTyDecl (P.tlValue x) toTyDecl _ = Nothing isTopDecl _ = True @@ -108,8 +118,8 @@ instance FromDecl (P.Decl Name) where toBind _ = Nothing toTyDecl (P.DLocated d _) = toTyDecl d - toTyDecl (P.DType x) = Just (TS x) - toTyDecl (P.DProp x) = Just (PS x) + toTyDecl (P.DType x) = Just (TS x Nothing) + toTyDecl (P.DProp x) = Just (PS x Nothing) toTyDecl _ = Nothing isTopDecl _ = False diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index b60ec932..2a3b9ce2 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -817,16 +817,16 @@ inferDs ds continue = checkTyDecls =<< orderTyDecls (mapMaybe toTyDecl ds) where isTopLevel = isTopDecl (head ds) - checkTyDecls (TS t : ts) = - do t1 <- checkTySyn t + checkTyDecls (TS t mbD : ts) = + do t1 <- checkTySyn t mbD withTySyn t1 (checkTyDecls ts) - checkTyDecls (PS t : ts) = - do t1 <- checkPropSyn t + checkTyDecls (PS t mbD : ts) = + do t1 <- checkPropSyn t mbD withTySyn t1 (checkTyDecls ts) - checkTyDecls (NT t : ts) = - do t1 <- checkNewtype t + checkTyDecls (NT t mbD : ts) = + do t1 <- checkNewtype t mbD withNewtype t1 (checkTyDecls ts) -- We checked all type synonyms, now continue with value-level definitions: diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs index 06d23fe2..86a4e356 100644 --- a/src/Cryptol/TypeCheck/Kind.hs +++ b/src/Cryptol/TypeCheck/Kind.hs @@ -54,8 +54,8 @@ checkSchema (P.Forall xs ps t mb) = Just r -> inRange r -- | Check a type-synonym declaration. -checkTySyn :: P.TySyn Name -> InferM TySyn -checkTySyn (P.TySyn x as t) = +checkTySyn :: P.TySyn Name -> Maybe String -> InferM TySyn +checkTySyn (P.TySyn x as t) mbD = do ((as1,t1),gs) <- collectGoals $ inRange (srcRange x) $ do r <- withTParams False as (doCheckType t Nothing) @@ -65,11 +65,12 @@ checkTySyn (P.TySyn x as t) = , tsParams = as1 , tsConstraints = map (tRebuild . goal) gs , tsDef = tRebuild t1 + , tsDoc = mbD } -- | Check a constraint-synonym declaration. -checkPropSyn :: P.PropSyn Name -> InferM TySyn -checkPropSyn (P.PropSyn x as ps) = +checkPropSyn :: P.PropSyn Name -> Maybe String -> InferM TySyn +checkPropSyn (P.PropSyn x as ps) mbD = do ((as1,t1),gs) <- collectGoals $ inRange (srcRange x) $ do r <- withTParams False as (traverse checkProp ps) @@ -79,12 +80,13 @@ checkPropSyn (P.PropSyn x as ps) = , tsParams = as1 , tsConstraints = map (tRebuild . goal) gs , tsDef = tRebuild (pAnd t1) + , tsDoc = mbD } -- | Check a newtype declaration. -- XXX: Do something with constraints. -checkNewtype :: P.Newtype Name -> InferM Newtype -checkNewtype (P.Newtype x as fs) = +checkNewtype :: P.Newtype Name -> Maybe String -> InferM Newtype +checkNewtype (P.Newtype x as fs) mbD = do ((as1,fs1),gs) <- collectGoals $ inRange (srcRange x) $ do r <- withTParams False as $ @@ -100,6 +102,7 @@ checkNewtype (P.Newtype x as fs) = , ntParams = as1 , ntConstraints = map goal gs , ntFields = fs1 + , ntDoc = mbD } @@ -191,7 +194,8 @@ tySyn :: Bool -- ^ Should we check for scoped type vars. tySyn scoped x ts k = do mb <- kLookupTSyn x 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) ts2 <- checkParams as ts1 let su = zip as ts2 diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index 634be6de..89fffd51 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -135,6 +135,7 @@ data TySyn = TySyn { tsName :: Name -- ^ Name , tsParams :: [TParam] -- ^ Parameters , tsConstraints :: [Prop] -- ^ Ensure body is OK , tsDef :: Type -- ^ Definition + , tsDoc :: !(Maybe String) -- ^ Documentation } deriving (Show, Generic, NFData) @@ -147,6 +148,7 @@ data Newtype = Newtype { ntName :: Name , ntParams :: [TParam] , ntConstraints :: [Prop] , ntFields :: [(Ident,Type)] + , ntDoc :: Maybe String } deriving (Show, Generic, NFData) @@ -224,7 +226,7 @@ instance HasKind Type where TRec {} -> KType 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 kindOf nt = foldr (:->) KType (map kindOf (ntParams nt)) @@ -702,10 +704,22 @@ instance PP TySyn where ppPrec = ppWithNamesPrec IntMap.empty instance PP (WithNames TySyn) where - ppPrec _ (WithNames (TySyn n ps _ ty) ns) = - text "type" <+> pp n <+> sep (map (ppWithNames ns1) ps) <+> char '=' - <+> ppWithNames ns1 ty - where ns1 = addTNames ps ns + ppPrec _ (WithNames ts ns) = + text "type" <+> ctr <+> pp (tsName ts) <+> + sep (map (ppWithNames ns1) (tsParams ts)) <+> char '=' + <+> 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