module Idris.Docs (
pprintDocs
, getDocs, pprintConstDocs, pprintTypeDoc
, FunDoc, FunDoc'(..), Docs, Docs'(..)
) where
import Idris.AbsSyntax
import Idris.AbsSyntaxTree
import Idris.Delaborate
import Idris.Core.TT
import Idris.Core.Evaluate
import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring, DocTerm, renderDocTerm, overview)
import Util.Pretty
import Prelude hiding ((<$>))
import Control.Arrow (first)
import Data.Maybe
import Data.List
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)]
[(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 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)
<> 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
isSubInterface (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args'
isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt
isSubInterface _ = False
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
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)