{-| Module : Idris.Docs Description : Data structures and utilities to work with Idris Documentation. Copyright : License : BSD3 Maintainer : The Idris Community. -} {-# LANGUAGE DeriveFunctor, MultiWayIf, PatternGuards #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Idris.Docs ( pprintDocs , getDocs, pprintConstDocs, pprintTypeDoc , FunDoc, FunDoc'(..), Docs, Docs'(..) ) where import Idris.AbsSyntax import Idris.AbsSyntaxTree import Idris.Core.Evaluate import Idris.Core.TT import Idris.Delaborate import Idris.Docstrings (DocTerm, Docstring, emptyDocstring, noDocs, nullDocstring, overview, renderDocTerm, renderDocstring) import Util.Pretty import Prelude hiding ((<$>)) import Control.Arrow (first) import Data.List import Data.Maybe import qualified Data.Text as T -- TODO: Only include names with public/export accessibility -- -- Issue #1573 on the Issue tracker. -- https://github.com/idris-lang/Idris-dev/issues/1573 data FunDoc' d = FD Name d [(Name, PTerm, Plicity, Maybe d)] -- args: name, ty, implicit, docs PTerm -- function type (Maybe Fixity) deriving Functor type FunDoc = FunDoc' (Docstring DocTerm) data Docs' d = FunDoc (FunDoc' d) | DataDoc (FunDoc' d) -- type constructor docs [FunDoc' d] -- data constructor docs | InterfaceDoc Name d -- interface docs [FunDoc' d] -- method docs [(Name, Maybe d)] -- parameters and their docstrings [PTerm] -- parameter constraints [(Maybe Name, PTerm, (d, [(Name, d)]))] -- implementations: name for named implementations, the constraint term, the docs [PTerm] -- sub interfaces [PTerm] -- super interfaces (Maybe (FunDoc' d)) -- explicit constructor | RecordDoc Name d -- record docs (FunDoc' d) -- data constructor docs [FunDoc' d] -- projection docs [(Name, PTerm, Maybe d)] -- parameters with type and doc | NamedImplementationDoc Name (FunDoc' d) -- name is interface | ModDoc [String] -- Module name d deriving Functor type Docs = Docs' (Docstring DocTerm) showDoc ist d | nullDocstring d = empty | otherwise = text " -- " <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d pprintFD :: IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation pprintFD ist totalityFlag nsFlag (FD n doc args ty f) = nest 4 (prettyName True nsFlag [] n <+> colon <+> pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args , not (T.isPrefixOf (T.pack "__") n') ] infixes ty -- show doc <$> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc -- show fixity <$> maybe empty (\f -> text (show f) <> line) f -- show arguments doc <> let argshow = showArgs args [] in (if not (null argshow) then nest 4 $ text "Arguments:" <$> vsep argshow else empty) -- show totality status <> let totality = getTotality in (if totalityFlag && not (null totality) then line <> (vsep . map (\t -> text "The function is" <+> t) $ totality) else empty)) where ppo = ppOptionIst ist infixes = idris_infixes ist -- Recurse over and show the Function's Documented arguments showArgs ((n, ty, Exp {}, Just d):args) bnd = -- Explicitly bound. bindingOf n False <+> colon <+> pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line : showArgs args ((n, False):bnd) showArgs ((n, ty, Constraint {}, Just d):args) bnd = -- Interface constraints. text "Interface constraint" <+> pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line : showArgs args ((n, True):bnd) showArgs ((n, ty, Imp {}, Just d):args) bnd = -- Implicit arguments. text "(implicit)" <+> bindingOf n True <+> colon <+> pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line : showArgs args ((n, True):bnd) showArgs ((n, ty, TacImp{}, Just d):args) bnd = -- Tacit implicits text "(auto implicit)" <+> bindingOf n True <+> colon <+> pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line : showArgs args ((n, True):bnd) showArgs ((n, _, _, _):args) bnd = -- Anything else showArgs args ((n, True):bnd) showArgs [] _ = [] -- end of arguments getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist) pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation pprintFDWithTotality ist = pprintFD ist True pprintFDWithoutTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation pprintFDWithoutTotality ist = pprintFD ist False pprintDocs :: IState -> Docs -> Doc OutputAnnotation pprintDocs ist (FunDoc d) = pprintFDWithTotality ist True d pprintDocs ist (DataDoc t args) = text "Data type" <+> pprintFDWithoutTotality ist True t <$> if null args then text "No constructors." else nest 4 (text "Constructors:" <> line <> vsep (map (pprintFDWithoutTotality ist False) args)) pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_interfaces super_interfaces ctor) = nest 4 (text "Interface" <+> prettyName True (ppopt_impl ppo) [] n <> if nullDocstring doc then empty else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc) <> line <$> nest 4 (text "Parameters:" <$> prettyParameters) <> (if null constraints then empty else line <$> nest 4 (text "Constraints:" <$> prettyConstraints)) <> line <$> nest 4 (text "Methods:" <$> vsep (map (pprintFDWithTotality ist False) meths)) <$> maybe empty ((<> line) . nest 4 . (text "Implementation constructor:" <$>) . pprintFDWithoutTotality ist False) ctor <> nest 4 (text "Implementations:" <$> vsep (if null implementations then [text ""] else map pprintImplementation normalImplementations)) <> (if null namedImplementations then empty else line <$> nest 4 (text "Named implementations:" <$> vsep (map pprintImplementation namedImplementations))) <> (if null sub_interfaces then empty else line <$> nest 4 (text "Child interfaces:" <$> vsep (map (dumpImplementation . prettifySubInterfaces) sub_interfaces))) <> (if null super_interfaces then empty else line <$> nest 4 (text "Default parent implementations:" <$> vsep (map dumpImplementation super_interfaces))) where params' = zip pNames (repeat False) (normalImplementations, namedImplementations) = partition (\(n, _, _) -> not $ isJust n) implementations pNames = map fst params ppo = ppOptionIst ist infixes = idris_infixes ist pprintImplementation (mname, term, (doc, argDocs)) = nest 4 (iname mname <> dumpImplementation term <> (if nullDocstring doc then empty else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc) <> if null argDocs then empty else line <> vsep (map (prettyImplementationParam (map fst argDocs)) argDocs)) iname Nothing = empty iname (Just n) = annName n <+> colon <> space prettyImplementationParam params (name, doc) = if nullDocstring doc then empty else prettyName True False (zip params (repeat False)) name <+> showDoc ist doc -- if any (isJust . snd) params -- then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params) -- else hsep (punctuate comma (map (prettyName True False params' . fst) params)) dumpImplementation :: PTerm -> Doc OutputAnnotation dumpImplementation = pprintPTerm ppo params' [] infixes prettifySubInterfaces (PPi (Constraint _ _) _ _ tm _) = prettifySubInterfaces tm prettifySubInterfaces (PPi plcity nm fc t1 t2) = PPi plcity (safeHead nm pNames) NoFC (prettifySubInterfaces t1) (prettifySubInterfaces t2) prettifySubInterfaces (PApp fc ref args) = PApp fc ref $ updateArgs pNames args prettifySubInterfaces tm = tm safeHead _ (y:_) = y safeHead x [] = x updateArgs (p:ps) ((PExp prty opts _ ref):as) = (PExp prty opts p (updateRef p ref)) : updateArgs ps as updateArgs ps (a:as) = a : updateArgs ps as updateArgs _ _ = [] updateRef nm (PRef fc _ _) = PRef fc [] nm updateRef _ pt = pt isSubInterface (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args' isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt isSubInterface _ = False prettyConstraints = cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints)) prettyParameters = if any (isJust . snd) params then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params) else hsep (punctuate comma (map (prettyName True False params' . fst) params)) pprintDocs ist (RecordDoc n doc ctor projs params) = nest 4 (text "Record" <+> prettyName True (ppopt_impl ppo) [] n <> if nullDocstring doc then empty else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc) -- Parameters <$> (if null params then empty else line <> nest 4 (text "Parameters:" <$> prettyParameters) <> line) -- Constructor <$> nest 4 (text "Constructor:" <$> pprintFDWithoutTotality ist False ctor) -- Projections <$> nest 4 (text "Projections:" <$> vsep (map (pprintFDWithoutTotality ist False) projs)) where ppo = ppOptionIst ist infixes = idris_infixes ist pNames = [n | (n,_,_) <- params] params' = zip pNames (repeat False) prettyParameters = if any isJust [d | (_,_,d) <- params] then vsep (map (\(n,pt,d) -> prettyParam (n,pt) <+> maybe empty (showDoc ist) d) params) else hsep (punctuate comma (map prettyParam [(n,pt) | (n,pt,_) <- params])) prettyParam (n,pt) = prettyName True False params' n <+> text ":" <+> pprintPTerm ppo params' [] infixes pt pprintDocs ist (NamedImplementationDoc _cls doc) = nest 4 (text "Named implementation:" <$> pprintFDWithoutTotality ist True doc) pprintDocs ist (ModDoc mod docs) = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs -- | Determine a truncation function depending how much docs the user -- wants to see howMuch FullDocs = id howMuch OverviewDocs = overview -- | Given a fully-qualified, disambiguated name, construct the -- documentation object for it getDocs :: Name -> HowMuchDocs -> Idris Docs getDocs n@(NS n' ns) w | n' == modDocName = do i <- getIState case lookupCtxtExact n (idris_moduledocs i) of Just doc -> return . ModDoc (reverse (map T.unpack ns)) $ howMuch w doc Nothing -> fail $ "Module docs for " ++ show (reverse (map T.unpack ns)) ++ " do not exist! This shouldn't have happened and is a bug." getDocs n w = do i <- getIState docs <- if | Just ci <- lookupCtxtExact n (idris_interfaces i) -> docInterface n ci | Just ri <- lookupCtxtExact n (idris_records i) -> docRecord n ri | Just ti <- lookupCtxtExact n (idris_datatypes i) -> docData n ti | Just interface_ <- interfaceNameForImpl i n -> do fd <- docFun n return $ NamedImplementationDoc interface_ fd | otherwise -> do fd <- docFun n return (FunDoc fd) return $ fmap (howMuch w) docs where interfaceNameForImpl :: IState -> Name -> Maybe Name interfaceNameForImpl ist n = listToMaybe [ cn | (cn, ci) <- toAlist (idris_interfaces ist) , n `elem` map fst (interface_implementations ci) ] docData :: Name -> TypeInfo -> Idris Docs docData n ti = do tdoc <- docFun n cdocs <- mapM docFun (con_names ti) return (DataDoc tdoc cdocs) docInterface :: Name -> InterfaceInfo -> Idris Docs docInterface n ci = do i <- getIState let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i docstr = maybe emptyDocstring fst docStrings params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (interface_params ci) docsForImplementation impl = fromMaybe (emptyDocstring, []) . flip lookupCtxtExact (idris_docstrings i) $ impl implementations = map (\impl -> (namedImpl impl, delabTy i impl, docsForImplementation impl)) (nub (map fst (interface_implementations ci))) (sub_interfaces, implementations') = partition (isSubInterface . (\(_,tm,_) -> tm)) implementations super_interfaces = catMaybes $ map getDImpl (interface_default_super_interfaces ci) mdocs <- mapM (docFun . fst) (interface_methods ci) let ctorN = implementationCtorName ci ctorDocs <- case basename ctorN of SN _ -> return Nothing _ -> fmap Just $ docFun ctorN return $ InterfaceDoc n docstr mdocs params (interface_constraints ci) implementations' (map (\(_,tm,_) -> tm) sub_interfaces) super_interfaces ctorDocs where namedImpl (NS n ns) = fmap (flip NS ns) (namedImpl n) namedImpl n@(UN _) = Just n namedImpl _ = Nothing getDImpl (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t getDImpl _ = Nothing isSubInterface (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args' isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt isSubInterface _ = False docRecord :: Name -> RecordInfo -> Idris Docs docRecord n ri = do i <- getIState let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i docstr = maybe emptyDocstring fst docStrings params = map (\(pn,pt) -> (pn, pt, docStrings >>= (lookup (nsroot pn) . snd))) (record_parameters ri) pdocs <- mapM docFun (record_projections ri) ctorDocs <- docFun $ record_constructor ri return $ RecordDoc n docstr ctorDocs pdocs params docFun :: Name -> Idris FunDoc docFun n = do i <- getIState let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of [d] -> d _ -> noDocs let ty = delabTy i n let args = getPArgNames ty argDocs let infixes = idris_infixes i let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes let f = case fixdecls of [] -> Nothing (Fix x _:_) -> Just x return (FD n docstr args ty f) where funName :: Name -> String funName (UN n) = str n funName (NS n _) = funName n funName n = show n getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))] getPArgNames (PPi plicity name _ ty body) ds = (name, ty, plicity, lookup name ds) : getPArgNames body ds getPArgNames _ _ = [] pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "type" else "value") <+> pprintPTerm (ppOptionIst ist) [] [] [] (PConstant NoFC c) <+> colon <+> pprintPTerm (ppOptionIst ist) [] [] [] (t c) <> nest 4 (line <> text str) where t (Fl _) = PConstant NoFC $ AType ATFloat t (BI _) = PConstant NoFC $ AType (ATInt ITBig) t (Str _) = PConstant NoFC StrType t (Ch c) = PConstant NoFC $ AType (ATInt ITChar) t _ = PType NoFC pprintTypeDoc :: IState -> Doc OutputAnnotation pprintTypeDoc ist = prettyIst ist (PType emptyFC) <+> colon <+> type1Doc <+> nest 4 (line <> text typeDescription)