{-# LANGUAGE CPP, DeriveFunctor, MultiWayIf, PatternGuards #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
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 forall a b. a -> FunDoc' b -> FunDoc' a
forall a b. (a -> b) -> FunDoc' a -> FunDoc' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> FunDoc' b -> FunDoc' a
$c<$ :: forall a b. a -> FunDoc' b -> FunDoc' a
fmap :: forall a b. (a -> b) -> FunDoc' a -> FunDoc' b
$cfmap :: forall a b. (a -> b) -> FunDoc' a -> FunDoc' b
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 forall a b. a -> Docs' b -> Docs' a
forall a b. (a -> b) -> Docs' a -> Docs' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Docs' b -> Docs' a
$c<$ :: forall a b. a -> Docs' b -> Docs' a
fmap :: forall a b. (a -> b) -> Docs' a -> Docs' b
$cfmap :: forall a b. (a -> b) -> Docs' a -> Docs' b
Functor
type Docs = Docs' (Docstring DocTerm)
showDoc :: IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist Docstring DocTerm
d
| forall a. Docstring a -> Bool
nullDocstring Docstring DocTerm
d = forall a. Doc a
empty
| Bool
otherwise = forall a. String -> Doc a
text String
" -- " forall a. Doc a -> Doc a -> Doc a
<>
forall a.
(a -> String -> Doc OutputAnnotation)
-> Docstring a -> Doc OutputAnnotation
renderDocstring ((Term -> Doc OutputAnnotation)
-> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation
renderDocTerm (IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist) (Context -> Env -> Term -> Term
normaliseAll (IState -> Context
tt_ctxt IState
ist) [])) Docstring DocTerm
d
pprintFD :: IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFD :: IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFD IState
ist Bool
totalityFlag Bool
nsFlag (FD Name
n Docstring DocTerm
doc [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args PTerm
ty Maybe Fixity
f) =
forall a. Int -> Doc a -> Doc a
nest Int
4 (Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
nsFlag [] Name
n
forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon
forall a. Doc a -> Doc a -> Doc a
<+> PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppo [] [ Name
n | (n :: Name
n@(UN Text
n'),PTerm
_,Plicity
_,Maybe (Docstring DocTerm)
_) <- [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args
, Bool -> Bool
not (Text -> Text -> Bool
T.isPrefixOf (String -> Text
T.pack String
"__") Text
n') ] [FixDecl]
infixes PTerm
ty
forall a. Doc a -> Doc a -> Doc a
<$> forall a.
(a -> String -> Doc OutputAnnotation)
-> Docstring a -> Doc OutputAnnotation
renderDocstring ((Term -> Doc OutputAnnotation)
-> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation
renderDocTerm (IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist) (Context -> Env -> Term -> Term
normaliseAll (IState -> Context
tt_ctxt IState
ist) [])) Docstring DocTerm
doc
forall a. Doc a -> Doc a -> Doc a
<$> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Doc a
empty (\Fixity
f -> forall a. String -> Doc a
text (forall a. Show a => a -> String
show Fixity
f) forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
line) Maybe Fixity
f
forall a. Doc a -> Doc a -> Doc a
<> let argshow :: [Doc OutputAnnotation]
argshow = [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
-> [(Name, Bool)] -> [Doc OutputAnnotation]
showArgs [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args [] in
(if Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc OutputAnnotation]
argshow)
then forall a. Int -> Doc a -> Doc a
nest Int
4 forall a b. (a -> b) -> a -> b
$ forall a. String -> Doc a
text String
"Arguments:" forall a. Doc a -> Doc a -> Doc a
<$> forall a. [Doc a] -> Doc a
vsep [Doc OutputAnnotation]
argshow
else forall a. Doc a
empty)
forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
showTotalVisibility
)
where
ppo :: PPOption
ppo = IState -> PPOption
ppOptionIst IState
ist
infixes :: [FixDecl]
infixes = IState -> [FixDecl]
idris_infixes IState
ist
showArgs :: [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
-> [(Name, Bool)] -> [Doc OutputAnnotation]
showArgs ((Name
n, PTerm
ty, Exp {}, Just Docstring DocTerm
d):[(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args) [(Name, Bool)]
bnd =
Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
False
forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon
forall a. Doc a -> Doc a -> Doc a
<+> PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] [FixDecl]
infixes PTerm
ty
forall a. Doc a -> Doc a -> Doc a
<> IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist Docstring DocTerm
d
forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
line forall a. a -> [a] -> [a]
: [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
-> [(Name, Bool)] -> [Doc OutputAnnotation]
showArgs [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args ((Name
n, Bool
False)forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd)
showArgs ((Name
n, PTerm
ty, Constraint {}, Just Docstring DocTerm
d):[(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args) [(Name, Bool)]
bnd =
forall a. String -> Doc a
text String
"Interface constraint"
forall a. Doc a -> Doc a -> Doc a
<+> PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] [FixDecl]
infixes PTerm
ty
forall a. Doc a -> Doc a -> Doc a
<> IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist Docstring DocTerm
d
forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
line forall a. a -> [a] -> [a]
: [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
-> [(Name, Bool)] -> [Doc OutputAnnotation]
showArgs [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args ((Name
n, Bool
True)forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd)
showArgs ((Name
n, PTerm
ty, Imp {}, Just Docstring DocTerm
d):[(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args) [(Name, Bool)]
bnd =
forall a. String -> Doc a
text String
"(implicit)"
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
True
forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon
forall a. Doc a -> Doc a -> Doc a
<+> PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] [FixDecl]
infixes PTerm
ty
forall a. Doc a -> Doc a -> Doc a
<> IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist Docstring DocTerm
d
forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
line forall a. a -> [a] -> [a]
: [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
-> [(Name, Bool)] -> [Doc OutputAnnotation]
showArgs [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args ((Name
n, Bool
True)forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd)
showArgs ((Name
n, PTerm
ty, TacImp{}, Just Docstring DocTerm
d):[(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args) [(Name, Bool)]
bnd =
forall a. String -> Doc a
text String
"(auto implicit)"
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
True
forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon
forall a. Doc a -> Doc a -> Doc a
<+> PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] [FixDecl]
infixes PTerm
ty
forall a. Doc a -> Doc a -> Doc a
<> IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist Docstring DocTerm
d
forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
line forall a. a -> [a] -> [a]
: [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
-> [(Name, Bool)] -> [Doc OutputAnnotation]
showArgs [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args ((Name
n, Bool
True)forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd)
showArgs ((Name
n, PTerm
_, Plicity
_, Maybe (Docstring DocTerm)
_):[(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args) [(Name, Bool)]
bnd =
[(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
-> [(Name, Bool)] -> [Doc OutputAnnotation]
showArgs [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args ((Name
n, Bool
True)forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd)
showArgs [] [(Name, Bool)]
_ = []
showTotalVisibility :: Doc a
showTotalVisibility =
case Name -> Context -> [(Totality, Accessibility)]
lookupTotalAccessibility Name
n (IState -> Context
tt_ctxt IState
ist) of
[] -> forall a. Doc a
empty
[(Totality, Accessibility)]
xs -> forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<> forall a. [Doc a] -> Doc a
vsep (forall a b. (a -> b) -> [a] -> [b]
map (forall {a} {a} {a}. (Show a, Show a) => (a, a) -> Doc a
doShowTotalVisibility) [(Totality, Accessibility)]
xs)
doShowTotalVisibility :: (a, a) -> Doc a
doShowTotalVisibility (a
t,a
v) = if Bool
totalityFlag
then forall a. String -> Doc a
text String
"The function is:" forall a. Doc a -> Doc a -> Doc a
<+> ((forall a. String -> Doc a
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) a
t) forall a. Doc a -> Doc a -> Doc a
<+> (forall a. String -> Doc a
text String
"&") forall a. Doc a -> Doc a -> Doc a
<+> ((forall a. String -> Doc a
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) a
v)
else forall a. String -> Doc a
text String
"The function is:" forall a. Doc a -> Doc a -> Doc a
<+> ((forall a. String -> Doc a
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) a
v)
pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithTotality IState
ist = IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFD IState
ist Bool
True
pprintFDWithoutTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithoutTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithoutTotality IState
ist = IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFD IState
ist Bool
False
pprintDocs :: IState -> Docs -> Doc OutputAnnotation
pprintDocs :: IState -> Docs -> Doc OutputAnnotation
pprintDocs IState
ist (FunDoc FunDoc
d) = IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithTotality IState
ist Bool
True FunDoc
d
pprintDocs IState
ist (DataDoc FunDoc
t [FunDoc]
args)
= forall a. String -> Doc a
text String
"Data type" forall a. Doc a -> Doc a -> Doc a
<+> IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithoutTotality IState
ist Bool
True FunDoc
t forall a. Doc a -> Doc a -> Doc a
<$>
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FunDoc]
args then forall a. String -> Doc a
text String
"No constructors."
else forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Constructors:" forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<>
forall a. [Doc a] -> Doc a
vsep (forall a b. (a -> b) -> [a] -> [b]
map (IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithoutTotality IState
ist Bool
False) [FunDoc]
args))
pprintDocs IState
ist (InterfaceDoc Name
n Docstring DocTerm
doc [FunDoc]
meths [(Name, Maybe (Docstring DocTerm))]
params [PTerm]
constraints [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
implementations [PTerm]
sub_interfaces [PTerm]
super_interfaces Maybe FunDoc
ctor)
= forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Interface" forall a. Doc a -> Doc a -> Doc a
<+> Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True (PPOption -> Bool
ppopt_impl PPOption
ppo) [] Name
n forall a. Doc a -> Doc a -> Doc a
<>
if forall a. Docstring a -> Bool
nullDocstring Docstring DocTerm
doc
then forall a. Doc a
empty
else forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<> forall a.
(a -> String -> Doc OutputAnnotation)
-> Docstring a -> Doc OutputAnnotation
renderDocstring ((Term -> Doc OutputAnnotation)
-> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation
renderDocTerm (IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist) (Context -> Env -> Term -> Term
normaliseAll (IState -> Context
tt_ctxt IState
ist) [])) Docstring DocTerm
doc)
forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<$>
forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Parameters:" forall a. Doc a -> Doc a -> Doc a
<$> Doc OutputAnnotation
prettyParameters)
forall a. Doc a -> Doc a -> Doc a
<> (if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PTerm]
constraints
then forall a. Doc a
empty
else forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<$> forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Constraints:" forall a. Doc a -> Doc a -> Doc a
<$> Doc OutputAnnotation
prettyConstraints))
forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<$>
forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Methods:" forall a. Doc a -> Doc a -> Doc a
<$>
forall a. [Doc a] -> Doc a
vsep (forall a b. (a -> b) -> [a] -> [b]
map (IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithTotality IState
ist Bool
False) [FunDoc]
meths))
forall a. Doc a -> Doc a -> Doc a
<$>
forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Doc a
empty
((forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
line) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> Doc a -> Doc a
nest Int
4 forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(forall a. String -> Doc a
text String
"Implementation constructor:" forall a. Doc a -> Doc a -> Doc a
<$>) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithoutTotality IState
ist Bool
False)
Maybe FunDoc
ctor
forall a. Doc a -> Doc a -> Doc a
<>
forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Implementations:" forall a. Doc a -> Doc a -> Doc a
<$>
forall a. [Doc a] -> Doc a
vsep (if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
implementations then [forall a. String -> Doc a
text String
"<no implementations>"]
else forall a b. (a -> b) -> [a] -> [b]
map (Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> Doc OutputAnnotation
pprintImplementation [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
normalImplementations))
forall a. Doc a -> Doc a -> Doc a
<>
(if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
namedImplementations then forall a. Doc a
empty
else forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<$> forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Named implementations:" forall a. Doc a -> Doc a -> Doc a
<$>
forall a. [Doc a] -> Doc a
vsep (forall a b. (a -> b) -> [a] -> [b]
map (Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> Doc OutputAnnotation
pprintImplementation [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
namedImplementations)))
forall a. Doc a -> Doc a -> Doc a
<>
(if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PTerm]
sub_interfaces then forall a. Doc a
empty
else forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<$> forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Child interfaces:" forall a. Doc a -> Doc a -> Doc a
<$>
forall a. [Doc a] -> Doc a
vsep (forall a b. (a -> b) -> [a] -> [b]
map (PTerm -> Doc OutputAnnotation
dumpImplementation forall b c a. (b -> c) -> (a -> b) -> a -> c
. PTerm -> PTerm
prettifySubInterfaces) [PTerm]
sub_interfaces)))
forall a. Doc a -> Doc a -> Doc a
<>
(if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PTerm]
super_interfaces then forall a. Doc a
empty
else forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<$> forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Default parent implementations:" forall a. Doc a -> Doc a -> Doc a
<$>
forall a. [Doc a] -> Doc a
vsep (forall a b. (a -> b) -> [a] -> [b]
map PTerm -> Doc OutputAnnotation
dumpImplementation [PTerm]
super_interfaces)))
where
params' :: [(Name, Bool)]
params' = forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
pNames (forall a. a -> [a]
repeat Bool
False)
([(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
normalImplementations, [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
namedImplementations) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(Maybe Name
n, PTerm
_, (Docstring DocTerm, [(Name, Docstring DocTerm)])
_) -> Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> Bool
isJust Maybe Name
n)
[(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
implementations
pNames :: [Name]
pNames = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Maybe (Docstring DocTerm))]
params
ppo :: PPOption
ppo = IState -> PPOption
ppOptionIst IState
ist
infixes :: [FixDecl]
infixes = IState -> [FixDecl]
idris_infixes IState
ist
pprintImplementation :: (Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> Doc OutputAnnotation
pprintImplementation (Maybe Name
mname, PTerm
term, (Docstring DocTerm
doc, [(Name, Docstring DocTerm)]
argDocs)) =
forall a. Int -> Doc a -> Doc a
nest Int
4 (Maybe Name -> Doc OutputAnnotation
iname Maybe Name
mname forall a. Doc a -> Doc a -> Doc a
<> PTerm -> Doc OutputAnnotation
dumpImplementation PTerm
term forall a. Doc a -> Doc a -> Doc a
<>
(if forall a. Docstring a -> Bool
nullDocstring Docstring DocTerm
doc
then forall a. Doc a
empty
else forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<>
forall a.
(a -> String -> Doc OutputAnnotation)
-> Docstring a -> Doc OutputAnnotation
renderDocstring
((Term -> Doc OutputAnnotation)
-> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation
renderDocTerm
(IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist)
(Context -> Env -> Term -> Term
normaliseAll (IState -> Context
tt_ctxt IState
ist) []))
Docstring DocTerm
doc) forall a. Doc a -> Doc a -> Doc a
<>
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, Docstring DocTerm)]
argDocs
then forall a. Doc a
empty
else forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<> forall a. [Doc a] -> Doc a
vsep (forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> (Name, Docstring DocTerm) -> Doc OutputAnnotation
prettyImplementationParam (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Docstring DocTerm)]
argDocs)) [(Name, Docstring DocTerm)]
argDocs))
iname :: Maybe Name -> Doc OutputAnnotation
iname Maybe Name
Nothing = forall a. Doc a
empty
iname (Just Name
n) = Name -> Doc OutputAnnotation
annName Name
n forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
space
prettyImplementationParam :: [Name] -> (Name, Docstring DocTerm) -> Doc OutputAnnotation
prettyImplementationParam [Name]
params (Name
name, Docstring DocTerm
doc) =
if forall a. Docstring a -> Bool
nullDocstring Docstring DocTerm
doc
then forall a. Doc a
empty
else Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
False (forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
params (forall a. a -> [a]
repeat Bool
False)) Name
name forall a. Doc a -> Doc a -> Doc a
<+>
IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist Docstring DocTerm
doc
dumpImplementation :: PTerm -> Doc OutputAnnotation
dumpImplementation :: PTerm -> Doc OutputAnnotation
dumpImplementation = PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppo [(Name, Bool)]
params' [] [FixDecl]
infixes
prettifySubInterfaces :: PTerm -> PTerm
prettifySubInterfaces (PPi (Constraint [ArgOpt]
_ Static
_ RigCount
_) Name
_ FC
_ PTerm
tm PTerm
_) = PTerm -> PTerm
prettifySubInterfaces PTerm
tm
prettifySubInterfaces (PPi Plicity
plcity Name
nm FC
fc PTerm
t1 PTerm
t2) = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
plcity (forall {a}. a -> [a] -> a
safeHead Name
nm [Name]
pNames) FC
NoFC (PTerm -> PTerm
prettifySubInterfaces PTerm
t1) (PTerm -> PTerm
prettifySubInterfaces PTerm
t2)
prettifySubInterfaces (PApp FC
fc PTerm
ref [PArg]
args) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
ref forall a b. (a -> b) -> a -> b
$ [Name] -> [PArg] -> [PArg]
updateArgs [Name]
pNames [PArg]
args
prettifySubInterfaces PTerm
tm = PTerm
tm
safeHead :: a -> [a] -> a
safeHead a
_ (a
y:[a]
_) = a
y
safeHead a
x [] = a
x
updateArgs :: [Name] -> [PArg] -> [PArg]
updateArgs (Name
p:[Name]
ps) ((PExp Int
prty [ArgOpt]
opts Name
_ PTerm
ref):[PArg]
as) = (forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp Int
prty [ArgOpt]
opts Name
p (Name -> PTerm -> PTerm
updateRef Name
p PTerm
ref)) forall a. a -> [a] -> [a]
: [Name] -> [PArg] -> [PArg]
updateArgs [Name]
ps [PArg]
as
updateArgs [Name]
ps (PArg
a:[PArg]
as) = PArg
a forall a. a -> [a] -> [a]
: [Name] -> [PArg] -> [PArg]
updateArgs [Name]
ps [PArg]
as
updateArgs [Name]
_ [PArg]
_ = []
updateRef :: Name -> PTerm -> PTerm
updateRef Name
nm (PRef FC
fc [FC]
_ Name
_) = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
nm
updateRef Name
_ PTerm
pt = PTerm
pt
prettyConstraints :: Doc OutputAnnotation
prettyConstraints =
forall a. [Doc a] -> Doc a
cat (forall a. Doc a -> [Doc a] -> [Doc a]
punctuate (forall a. Doc a
comma forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
space) (forall a b. (a -> b) -> [a] -> [b]
map (PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppo [(Name, Bool)]
params' [] [FixDecl]
infixes) [PTerm]
constraints))
prettyParameters :: Doc OutputAnnotation
prettyParameters =
if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Name, Maybe (Docstring DocTerm))]
params
then forall a. [Doc a] -> Doc a
vsep (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
nm,Maybe (Docstring DocTerm)
md) -> Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
False [(Name, Bool)]
params' Name
nm forall a. Doc a -> Doc a -> Doc a
<+> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Doc a
empty (IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist) Maybe (Docstring DocTerm)
md) [(Name, Maybe (Docstring DocTerm))]
params)
else forall a. [Doc a] -> Doc a
hsep (forall a. Doc a -> [Doc a] -> [Doc a]
punctuate forall a. Doc a
comma (forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
False [(Name, Bool)]
params' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Name, Maybe (Docstring DocTerm))]
params))
pprintDocs IState
ist (RecordDoc Name
n Docstring DocTerm
doc FunDoc
ctor [FunDoc]
projs [(Name, PTerm, Maybe (Docstring DocTerm))]
params)
= forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Record" forall a. Doc a -> Doc a -> Doc a
<+> Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True (PPOption -> Bool
ppopt_impl PPOption
ppo) [] Name
n forall a. Doc a -> Doc a -> Doc a
<>
if forall a. Docstring a -> Bool
nullDocstring Docstring DocTerm
doc
then forall a. Doc a
empty
else forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<>
forall a.
(a -> String -> Doc OutputAnnotation)
-> Docstring a -> Doc OutputAnnotation
renderDocstring ((Term -> Doc OutputAnnotation)
-> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation
renderDocTerm (IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist) (Context -> Env -> Term -> Term
normaliseAll (IState -> Context
tt_ctxt IState
ist) [])) Docstring DocTerm
doc)
forall a. Doc a -> Doc a -> Doc a
<$> (if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, PTerm, Maybe (Docstring DocTerm))]
params
then forall a. Doc a
empty
else forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<> forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Parameters:" forall a. Doc a -> Doc a -> Doc a
<$> Doc OutputAnnotation
prettyParameters) forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
line)
forall a. Doc a -> Doc a -> Doc a
<$> forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Constructor:" forall a. Doc a -> Doc a -> Doc a
<$> IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithoutTotality IState
ist Bool
False FunDoc
ctor)
forall a. Doc a -> Doc a -> Doc a
<$> forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Projections:" forall a. Doc a -> Doc a -> Doc a
<$> forall a. [Doc a] -> Doc a
vsep (forall a b. (a -> b) -> [a] -> [b]
map (IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithoutTotality IState
ist Bool
False) [FunDoc]
projs))
where
ppo :: PPOption
ppo = IState -> PPOption
ppOptionIst IState
ist
infixes :: [FixDecl]
infixes = IState -> [FixDecl]
idris_infixes IState
ist
pNames :: [Name]
pNames = [Name
n | (Name
n,PTerm
_,Maybe (Docstring DocTerm)
_) <- [(Name, PTerm, Maybe (Docstring DocTerm))]
params]
params' :: [(Name, Bool)]
params' = forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
pNames (forall a. a -> [a]
repeat Bool
False)
prettyParameters :: Doc OutputAnnotation
prettyParameters =
if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Maybe a -> Bool
isJust [Maybe (Docstring DocTerm)
d | (Name
_,PTerm
_,Maybe (Docstring DocTerm)
d) <- [(Name, PTerm, Maybe (Docstring DocTerm))]
params]
then forall a. [Doc a] -> Doc a
vsep (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n,PTerm
pt,Maybe (Docstring DocTerm)
d) -> (Name, PTerm) -> Doc OutputAnnotation
prettyParam (Name
n,PTerm
pt) forall a. Doc a -> Doc a -> Doc a
<+> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Doc a
empty (IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist) Maybe (Docstring DocTerm)
d) [(Name, PTerm, Maybe (Docstring DocTerm))]
params)
else forall a. [Doc a] -> Doc a
hsep (forall a. Doc a -> [Doc a] -> [Doc a]
punctuate forall a. Doc a
comma (forall a b. (a -> b) -> [a] -> [b]
map (Name, PTerm) -> Doc OutputAnnotation
prettyParam [(Name
n,PTerm
pt) | (Name
n,PTerm
pt,Maybe (Docstring DocTerm)
_) <- [(Name, PTerm, Maybe (Docstring DocTerm))]
params]))
prettyParam :: (Name, PTerm) -> Doc OutputAnnotation
prettyParam (Name
n,PTerm
pt) = Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
False [(Name, Bool)]
params' Name
n forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text String
":" forall a. Doc a -> Doc a -> Doc a
<+> PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppo [(Name, Bool)]
params' [] [FixDecl]
infixes PTerm
pt
pprintDocs IState
ist (NamedImplementationDoc Name
_cls FunDoc
doc)
= forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. String -> Doc a
text String
"Named implementation:" forall a. Doc a -> Doc a -> Doc a
<$> IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithoutTotality IState
ist Bool
True FunDoc
doc)
pprintDocs IState
ist (ModDoc [String]
mod Docstring DocTerm
docs)
= forall a. Int -> Doc a -> Doc a
nest Int
4 forall a b. (a -> b) -> a -> b
$ forall a. String -> Doc a
text String
"Module" forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a. a -> [a] -> [a]
intersperse String
"." [String]
mod)) forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<$>
forall a.
(a -> String -> Doc OutputAnnotation)
-> Docstring a -> Doc OutputAnnotation
renderDocstring ((Term -> Doc OutputAnnotation)
-> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation
renderDocTerm (IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist) (Context -> Env -> Term -> Term
normaliseAll (IState -> Context
tt_ctxt IState
ist) [])) Docstring DocTerm
docs
howMuch :: HowMuchDocs -> Docstring a -> Docstring a
howMuch HowMuchDocs
FullDocs = forall a. a -> a
id
howMuch HowMuchDocs
OverviewDocs = forall a. Docstring a -> Docstring a
overview
getDocs :: Name -> HowMuchDocs -> Idris Docs
getDocs :: Name -> HowMuchDocs -> Idris Docs
getDocs n :: Name
n@(NS Name
n' [Text]
ns) HowMuchDocs
w | Name
n' forall a. Eq a => a -> a -> Bool
== Name
modDocName
= do IState
i <- Idris IState
getIState
case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt (Docstring DocTerm)
idris_moduledocs IState
i) of
Just Docstring DocTerm
doc -> forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall d. [String] -> d -> Docs' d
ModDoc (forall a. [a] -> [a]
reverse (forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack [Text]
ns)) forall a b. (a -> b) -> a -> b
$ forall {a}. HowMuchDocs -> Docstring a -> Docstring a
howMuch HowMuchDocs
w Docstring DocTerm
doc
Maybe (Docstring DocTerm)
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Module docs for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. [a] -> [a]
reverse (forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack [Text]
ns)) forall a. [a] -> [a] -> [a]
++
String
" do not exist! This shouldn't have happened and is a bug."
getDocs Name
n HowMuchDocs
w
= do IState
i <- Idris IState
getIState
Docs
docs <- if | Just InterfaceInfo
ci <- forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i)
-> Name -> InterfaceInfo -> Idris Docs
docInterface Name
n InterfaceInfo
ci
| Just RecordInfo
ri <- forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt RecordInfo
idris_records IState
i)
-> Name -> RecordInfo -> Idris Docs
docRecord Name
n RecordInfo
ri
| Just TypeInfo
ti <- forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
i)
-> Name -> TypeInfo -> Idris Docs
docData Name
n TypeInfo
ti
| Just Name
interface_ <- IState -> Name -> Maybe Name
interfaceNameForImpl IState
i Name
n
-> do FunDoc
fd <- Name -> Idris FunDoc
docFun Name
n
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall d. Name -> FunDoc' d -> Docs' d
NamedImplementationDoc Name
interface_ FunDoc
fd
| Bool
otherwise
-> do FunDoc
fd <- Name -> Idris FunDoc
docFun Name
n
forall (m :: * -> *) a. Monad m => a -> m a
return (forall d. FunDoc' d -> Docs' d
FunDoc FunDoc
fd)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall {a}. HowMuchDocs -> Docstring a -> Docstring a
howMuch HowMuchDocs
w) Docs
docs
where interfaceNameForImpl :: IState -> Name -> Maybe Name
interfaceNameForImpl :: IState -> Name -> Maybe Name
interfaceNameForImpl IState
ist Name
n =
forall a. [a] -> Maybe a
listToMaybe [ Name
cn
| (Name
cn, InterfaceInfo
ci) <- forall a. Ctxt a -> [(Name, a)]
toAlist (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist)
, Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (InterfaceInfo -> [(Name, Bool)]
interface_implementations InterfaceInfo
ci)
]
docData :: Name -> TypeInfo -> Idris Docs
docData :: Name -> TypeInfo -> Idris Docs
docData Name
n TypeInfo
ti
= do FunDoc
tdoc <- Name -> Idris FunDoc
docFun Name
n
[FunDoc]
cdocs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> Idris FunDoc
docFun (TypeInfo -> [Name]
con_names TypeInfo
ti)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall d. FunDoc' d -> [FunDoc' d] -> Docs' d
DataDoc FunDoc
tdoc [FunDoc]
cdocs)
docInterface :: Name -> InterfaceInfo -> Idris Docs
docInterface :: Name -> InterfaceInfo -> Idris Docs
docInterface Name
n InterfaceInfo
ci
= do IState
i <- Idris IState
getIState
let docStrings :: Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
docStrings = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n forall a b. (a -> b) -> a -> b
$ IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
i
docstr :: Docstring DocTerm
docstr = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Docstring a
emptyDocstring forall a b. (a, b) -> a
fst Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
docStrings
params :: [(Name, Maybe (Docstring DocTerm))]
params = forall a b. (a -> b) -> [a] -> [b]
map (\Name
pn -> (Name
pn, Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
docStrings forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
pn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)))
(InterfaceInfo -> [Name]
interface_params InterfaceInfo
ci)
docsForImplementation :: Name -> (Docstring DocTerm, [(Name, Docstring DocTerm)])
docsForImplementation Name
impl = forall a. a -> Maybe a -> a
fromMaybe (forall a. Docstring a
emptyDocstring, []) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
i) forall a b. (a -> b) -> a -> b
$
Name
impl
implementations :: [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
implementations = forall a b. (a -> b) -> [a] -> [b]
map (\Name
impl -> (Name -> Maybe Name
namedImpl Name
impl,
IState -> Name -> PTerm
delabTy IState
i Name
impl,
Name -> (Docstring DocTerm, [(Name, Docstring DocTerm)])
docsForImplementation Name
impl))
(forall a. Eq a => [a] -> [a]
nub (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (InterfaceInfo -> [(Name, Bool)]
interface_implementations InterfaceInfo
ci)))
([(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
sub_interfaces, [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
implementations') = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (PTerm -> Bool
isSubInterface forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Maybe Name
_,PTerm
tm,(Docstring DocTerm, [(Name, Docstring DocTerm)])
_) -> PTerm
tm)) [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
implementations
super_interfaces :: [PTerm]
super_interfaces = forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {a}. PDecl' a -> Maybe a
getDImpl (InterfaceInfo -> [PDecl]
interface_default_super_interfaces InterfaceInfo
ci)
[FunDoc]
mdocs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name -> Idris FunDoc
docFun forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci)
let ctorN :: Name
ctorN = InterfaceInfo -> Name
implementationCtorName InterfaceInfo
ci
Maybe FunDoc
ctorDocs <- case Name -> Name
basename Name
ctorN of
SN SpecialName
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Name
_ -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Name -> Idris FunDoc
docFun Name
ctorN
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall d.
Name
-> d
-> [FunDoc' d]
-> [(Name, Maybe d)]
-> [PTerm]
-> [(Maybe Name, PTerm, (d, [(Name, d)]))]
-> [PTerm]
-> [PTerm]
-> Maybe (FunDoc' d)
-> Docs' d
InterfaceDoc
Name
n Docstring DocTerm
docstr [FunDoc]
mdocs [(Name, Maybe (Docstring DocTerm))]
params (InterfaceInfo -> [PTerm]
interface_constraints InterfaceInfo
ci)
[(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
implementations' (forall a b. (a -> b) -> [a] -> [b]
map (\(Maybe Name
_,PTerm
tm,(Docstring DocTerm, [(Name, Docstring DocTerm)])
_) -> PTerm
tm) [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
sub_interfaces) [PTerm]
super_interfaces
Maybe FunDoc
ctorDocs
where
namedImpl :: Name -> Maybe Name
namedImpl (NS Name
n [Text]
ns) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> b -> a -> c
flip Name -> [Text] -> Name
NS [Text]
ns) (Name -> Maybe Name
namedImpl Name
n)
namedImpl n :: Name
n@(UN Text
_) = forall a. a -> Maybe a
Just Name
n
namedImpl Name
_ = forall a. Maybe a
Nothing
getDImpl :: PDecl' a -> Maybe a
getDImpl (PImplementation Docstring (Either Err a)
_ [(Name, Docstring (Either Err a))]
_ SyntaxInfo
_ FC
_ [(Name, a)]
_ [Name]
_ Accessibility
_ FnOpts
_ Name
_ FC
_ [a]
_ [(Name, a)]
_ a
t Maybe Name
_ [PDecl' a]
_) = forall a. a -> Maybe a
Just a
t
getDImpl PDecl' a
_ = forall a. Maybe a
Nothing
isSubInterface :: PTerm -> Bool
isSubInterface (PPi (Constraint [ArgOpt]
_ Static
_ RigCount
_) Name
_ FC
_ (PApp FC
_ PTerm
_ [PArg]
args) (PApp FC
_ (PRef FC
_ [FC]
_ Name
nm) [PArg]
args'))
= Name
nm forall a. Eq a => a -> a -> Bool
== Name
n Bool -> Bool -> Bool
&& forall a b. (a -> b) -> [a] -> [b]
map forall t. PArg' t -> t
getTm [PArg]
args forall a. Eq a => a -> a -> Bool
== forall a b. (a -> b) -> [a] -> [b]
map forall t. PArg' t -> t
getTm [PArg]
args'
isSubInterface (PPi Plicity
_ Name
_ FC
_ PTerm
_ PTerm
pt)
= PTerm -> Bool
isSubInterface PTerm
pt
isSubInterface PTerm
_
= Bool
False
docRecord :: Name -> RecordInfo -> Idris Docs
docRecord :: Name -> RecordInfo -> Idris Docs
docRecord Name
n RecordInfo
ri
= do IState
i <- Idris IState
getIState
let docStrings :: Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
docStrings = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n forall a b. (a -> b) -> a -> b
$ IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
i
docstr :: Docstring DocTerm
docstr = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Docstring a
emptyDocstring forall a b. (a, b) -> a
fst Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
docStrings
params :: [(Name, PTerm, Maybe (Docstring DocTerm))]
params = forall a b. (a -> b) -> [a] -> [b]
map (\(Name
pn,PTerm
pt) -> (Name
pn, PTerm
pt, Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
docStrings forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Name -> Name
nsroot Name
pn) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)))
(RecordInfo -> [(Name, PTerm)]
record_parameters RecordInfo
ri)
[FunDoc]
pdocs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> Idris FunDoc
docFun (RecordInfo -> [Name]
record_projections RecordInfo
ri)
FunDoc
ctorDocs <- Name -> Idris FunDoc
docFun forall a b. (a -> b) -> a -> b
$ RecordInfo -> Name
record_constructor RecordInfo
ri
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall d.
Name
-> d
-> FunDoc' d
-> [FunDoc' d]
-> [(Name, PTerm, Maybe d)]
-> Docs' d
RecordDoc Name
n Docstring DocTerm
docstr FunDoc
ctorDocs [FunDoc]
pdocs [(Name, PTerm, Maybe (Docstring DocTerm))]
params
docFun :: Name -> Idris FunDoc
docFun :: Name -> Idris FunDoc
docFun Name
n
= do IState
i <- Idris IState
getIState
let (Docstring DocTerm
docstr, [(Name, Docstring DocTerm)]
argDocs) = case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
i) of
[(Docstring DocTerm, [(Name, Docstring DocTerm)])
d] -> (Docstring DocTerm, [(Name, Docstring DocTerm)])
d
[(Docstring DocTerm, [(Name, Docstring DocTerm)])]
_ -> forall a. (Docstring a, [(Name, Docstring a)])
noDocs
let ty :: PTerm
ty = IState -> Name -> PTerm
delabTy IState
i Name
n
let args :: [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args = PTerm
-> [(Name, Docstring DocTerm)]
-> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
getPArgNames PTerm
ty [(Name, Docstring DocTerm)]
argDocs
let infixes :: [FixDecl]
infixes = IState -> [FixDecl]
idris_infixes IState
i
let fixdecls :: [FixDecl]
fixdecls = forall a. (a -> Bool) -> [a] -> [a]
filter (\(Fix Fixity
_ String
x) -> String
x forall a. Eq a => a -> a -> Bool
== Name -> String
funName Name
n) [FixDecl]
infixes
let f :: Maybe Fixity
f = case [FixDecl]
fixdecls of
[] -> forall a. Maybe a
Nothing
(Fix Fixity
x String
_:[FixDecl]
_) -> forall a. a -> Maybe a
Just Fixity
x
forall (m :: * -> *) a. Monad m => a -> m a
return (forall d.
Name
-> d
-> [(Name, PTerm, Plicity, Maybe d)]
-> PTerm
-> Maybe Fixity
-> FunDoc' d
FD Name
n Docstring DocTerm
docstr [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
args PTerm
ty Maybe Fixity
f)
where funName :: Name -> String
funName :: Name -> String
funName (UN Text
n) = Text -> String
str Text
n
funName (NS Name
n [Text]
_) = Name -> String
funName Name
n
funName Name
n = forall a. Show a => a -> String
show Name
n
getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
getPArgNames :: PTerm
-> [(Name, Docstring DocTerm)]
-> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
getPArgNames (PPi Plicity
plicity Name
name FC
_ PTerm
ty PTerm
body) [(Name, Docstring DocTerm)]
ds =
(Name
name, PTerm
ty, Plicity
plicity, forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
name [(Name, Docstring DocTerm)]
ds) forall a. a -> [a] -> [a]
: PTerm
-> [(Name, Docstring DocTerm)]
-> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
getPArgNames PTerm
body [(Name, Docstring DocTerm)]
ds
getPArgNames PTerm
_ [(Name, Docstring DocTerm)]
_ = []
pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation
pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation
pprintConstDocs IState
ist Const
c String
str = forall a. String -> Doc a
text String
"Primitive" forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text (if Const -> Bool
constIsType Const
c then String
"type" else String
"value") forall a. Doc a -> Doc a -> Doc a
<+>
PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
ist) [] [] [] (FC -> Const -> PTerm
PConstant FC
NoFC Const
c) forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+>
PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
ist) [] [] [] (Const -> PTerm
t Const
c) forall a. Doc a -> Doc a -> Doc a
<>
forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<> forall a. String -> Doc a
text String
str)
where t :: Const -> PTerm
t (Fl Double
_) = FC -> Const -> PTerm
PConstant FC
NoFC forall a b. (a -> b) -> a -> b
$ ArithTy -> Const
AType ArithTy
ATFloat
t (BI Integer
_) = FC -> Const -> PTerm
PConstant FC
NoFC forall a b. (a -> b) -> a -> b
$ ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITBig)
t (Str String
_) = FC -> Const -> PTerm
PConstant FC
NoFC Const
StrType
t (Ch Char
c) = FC -> Const -> PTerm
PConstant FC
NoFC forall a b. (a -> b) -> a -> b
$ ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITChar)
t Const
_ = FC -> PTerm
PType FC
NoFC
pprintTypeDoc :: IState -> Doc OutputAnnotation
pprintTypeDoc :: IState -> Doc OutputAnnotation
pprintTypeDoc IState
ist = IState -> PTerm -> Doc OutputAnnotation
prettyIst IState
ist (FC -> PTerm
PType FC
emptyFC) forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
type1Doc forall a. Doc a -> Doc a -> Doc a
<+>
forall a. Int -> Doc a -> Doc a
nest Int
4 (forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<> forall a. String -> Doc a
text String
typeDescription)