module Idris.Docs (
pprintDocs
, getDocs, pprintConstDocs, pprintTypeDoc
, FunDoc, FunDoc'(..), Docs, Docs'(..)
) where
import Idris.AbsSyntax (FixDecl(..), Fixity, IState(..), Idris,
InterfaceInfo(..), PArg'(..), PDecl'(..), PPOption(..),
PTerm(..), Plicity(..), RecordInfo(..), basename,
getIState, modDocName, ppOptionIst, pprintPTerm,
prettyIst, prettyName, type1Doc, typeDescription)
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate
import Idris.Docstrings (DocTerm, Docstring, emptyDocstring, noDocs,
nullDocstring, overview, renderDocTerm,
renderDocstring)
import Idris.Options (HowMuchDocs(..))
import Util.Pretty
#if (MIN_VERSION_base(4,11,0))
import Prelude hiding ((<$>), (<>))
#else
import Prelude hiding ((<$>))
#endif
import Data.List
import Data.Maybe
import qualified Data.Text as T
data FunDoc' d = FD Name d
[(Name, PTerm, Plicity, Maybe d)]
PTerm
(Maybe Fixity)
deriving Functor
type FunDoc = FunDoc' (Docstring DocTerm)
data Docs' d = FunDoc (FunDoc' d)
| DataDoc (FunDoc' d)
[FunDoc' d]
| InterfaceDoc Name d
[FunDoc' d]
[(Name, Maybe d)]
[PTerm]
[(Maybe Name, PTerm, (d, [(Name, d)]))]
[PTerm]
[PTerm]
(Maybe (FunDoc' d))
| RecordDoc Name d
(FunDoc' d)
[FunDoc' d]
[(Name, PTerm, Maybe d)]
| NamedImplementationDoc Name (FunDoc' d)
| ModDoc [String]
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
<$> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc
<$> maybe empty (\f -> text (show f) <> line) f
<> let argshow = showArgs args [] in
(if not (null argshow)
then nest 4 $ text "Arguments:" <$> vsep argshow
else empty)
<> 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
showArgs ((n, ty, Exp {}, Just d):args) bnd =
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 =
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 =
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 =
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 =
showArgs args ((n, True):bnd)
showArgs [] _ = []
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 "<no implementations>"]
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
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
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)
<$> (if null params
then empty
else line <> nest 4 (text "Parameters:" <$> prettyParameters) <> line)
<$> nest 4 (text "Constructor:" <$> pprintFDWithoutTotality ist False ctor)
<$> 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
howMuch FullDocs = id
howMuch OverviewDocs = overview
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)