{-# 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 -> b) -> FunDoc' a -> FunDoc' b)
-> (forall a b. a -> FunDoc' b -> FunDoc' a) -> Functor FunDoc'
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
$cfmap :: forall a b. (a -> b) -> FunDoc' a -> FunDoc' b
fmap :: forall a b. (a -> b) -> FunDoc' a -> FunDoc' b
$c<$ :: forall a b. a -> FunDoc' b -> FunDoc' a
<$ :: forall a b. a -> FunDoc' b -> FunDoc' a
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 -> b) -> Docs' a -> Docs' b)
-> (forall a b. a -> Docs' b -> Docs' a) -> Functor Docs'
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
$cfmap :: forall a b. (a -> b) -> Docs' a -> Docs' b
fmap :: forall a b. (a -> b) -> Docs' a -> Docs' b
$c<$ :: forall a b. a -> Docs' b -> Docs' a
<$ :: forall a b. a -> Docs' b -> Docs' a
Functor
type Docs = Docs' (Docstring DocTerm)
showDoc :: IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist Docstring DocTerm
d
| Docstring DocTerm -> Bool
forall a. Docstring a -> Bool
nullDocstring Docstring DocTerm
d = Doc OutputAnnotation
forall a. Doc a
empty
| Bool
otherwise = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" -- " Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
(DocTerm -> String -> Doc OutputAnnotation)
-> Docstring DocTerm -> Doc OutputAnnotation
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) =
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
nsFlag [] Name
n
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
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
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> (DocTerm -> String -> Doc OutputAnnotation)
-> Docstring DocTerm -> Doc OutputAnnotation
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
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> Doc OutputAnnotation
-> (Fixity -> Doc OutputAnnotation)
-> Maybe Fixity
-> Doc OutputAnnotation
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc OutputAnnotation
forall a. Doc a
empty (\Fixity
f -> String -> Doc OutputAnnotation
forall a. String -> Doc a
text (Fixity -> String
forall a. Show a => a -> String
show Fixity
f) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line) Maybe Fixity
f
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
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 ([Doc OutputAnnotation] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc OutputAnnotation]
argshow)
then Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Arguments:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep [Doc OutputAnnotation]
argshow
else Doc OutputAnnotation
forall a. Doc a
empty)
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
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
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
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
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist Docstring DocTerm
d
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
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)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
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 =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Interface constraint"
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
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
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist Docstring DocTerm
d
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
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)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
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 =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"(implicit)"
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
True
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
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
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist Docstring DocTerm
d
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
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)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
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 =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"(auto implicit)"
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
True
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
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
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist Docstring DocTerm
d
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
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)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
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)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
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
[] -> Doc a
forall a. Doc a
empty
[(Totality, Accessibility)]
xs -> Doc a
forall a. Doc a
line Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<> [Doc a] -> Doc a
forall a. [Doc a] -> Doc a
vsep (((Totality, Accessibility) -> Doc a)
-> [(Totality, Accessibility)] -> [Doc a]
forall a b. (a -> b) -> [a] -> [b]
map ((Totality, Accessibility) -> Doc a
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 String -> Doc a
forall a. String -> Doc a
text String
"The function is:" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> ((String -> Doc a
forall a. String -> Doc a
text (String -> Doc a) -> (a -> String) -> a -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
forall a. Show a => a -> String
show) a
t) Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc a
forall a. String -> Doc a
text String
"&") Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> ((String -> Doc a
forall a. String -> Doc a
text (String -> Doc a) -> (a -> String) -> a -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
forall a. Show a => a -> String
show) a
v)
else String -> Doc a
forall a. String -> Doc a
text String
"The function is:" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> ((String -> Doc a
forall a. String -> Doc a
text (String -> Doc a) -> (a -> String) -> a -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
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)
= String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Data type" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithoutTotality IState
ist Bool
True FunDoc
t Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
if [FunDoc] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FunDoc]
args then String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"No constructors."
else Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Constructors:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
[Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((FunDoc -> Doc OutputAnnotation)
-> [FunDoc] -> [Doc OutputAnnotation]
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)
= Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Interface" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
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 Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
if Docstring DocTerm -> Bool
forall a. Docstring a -> Bool
nullDocstring Docstring DocTerm
doc
then Doc OutputAnnotation
forall a. Doc a
empty
else Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> (DocTerm -> String -> Doc OutputAnnotation)
-> Docstring DocTerm -> Doc OutputAnnotation
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)
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Parameters:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> Doc OutputAnnotation
prettyParameters)
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> (if [PTerm] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PTerm]
constraints
then Doc OutputAnnotation
forall a. Doc a
empty
else Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Constraints:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> Doc OutputAnnotation
prettyConstraints))
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Methods:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
[Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((FunDoc -> Doc OutputAnnotation)
-> [FunDoc] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithTotality IState
ist Bool
False) [FunDoc]
meths))
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
Doc OutputAnnotation
-> (FunDoc -> Doc OutputAnnotation)
-> Maybe FunDoc
-> Doc OutputAnnotation
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc OutputAnnotation
forall a. Doc a
empty
((Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (FunDoc -> Doc OutputAnnotation)
-> FunDoc
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (FunDoc -> Doc OutputAnnotation)
-> FunDoc
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Implementation constructor:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (FunDoc -> Doc OutputAnnotation)
-> FunDoc
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithoutTotality IState
ist Bool
False)
Maybe FunDoc
ctor
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Implementations:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
[Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep (if [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
implementations then [String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"<no implementations>"]
else ((Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> Doc OutputAnnotation)
-> [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> [Doc OutputAnnotation]
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))
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
(if [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
namedImplementations then Doc OutputAnnotation
forall a. Doc a
empty
else Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Named implementations:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
[Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep (((Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> Doc OutputAnnotation)
-> [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> [Doc OutputAnnotation]
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)))
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
(if [PTerm] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PTerm]
sub_interfaces then Doc OutputAnnotation
forall a. Doc a
empty
else Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Child interfaces:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
[Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((PTerm -> Doc OutputAnnotation)
-> [PTerm] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm -> Doc OutputAnnotation
dumpImplementation (PTerm -> Doc OutputAnnotation)
-> (PTerm -> PTerm) -> PTerm -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PTerm -> PTerm
prettifySubInterfaces) [PTerm]
sub_interfaces)))
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
(if [PTerm] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PTerm]
super_interfaces then Doc OutputAnnotation
forall a. Doc a
empty
else Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Default parent implementations:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
[Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((PTerm -> Doc OutputAnnotation)
-> [PTerm] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> Doc OutputAnnotation
dumpImplementation [PTerm]
super_interfaces)))
where
params' :: [(Name, Bool)]
params' = [Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
pNames (Bool -> [Bool]
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) = ((Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> Bool)
-> [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> ([(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))],
[(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(Maybe Name
n, PTerm
_, (Docstring DocTerm, [(Name, Docstring DocTerm)])
_) -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Maybe Name -> Bool
forall a. Maybe a -> Bool
isJust Maybe Name
n)
[(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
implementations
pNames :: [Name]
pNames = ((Name, Maybe (Docstring DocTerm)) -> Name)
-> [(Name, Maybe (Docstring DocTerm))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Maybe (Docstring DocTerm)) -> Name
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)) =
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (Maybe Name -> Doc OutputAnnotation
iname Maybe Name
mname Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> PTerm -> Doc OutputAnnotation
dumpImplementation PTerm
term Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
(if Docstring DocTerm -> Bool
forall a. Docstring a -> Bool
nullDocstring Docstring DocTerm
doc
then Doc OutputAnnotation
forall a. Doc a
empty
else Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
(DocTerm -> String -> Doc OutputAnnotation)
-> Docstring DocTerm -> Doc OutputAnnotation
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) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
if [(Name, Docstring DocTerm)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, Docstring DocTerm)]
argDocs
then Doc OutputAnnotation
forall a. Doc a
empty
else Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep (((Name, Docstring DocTerm) -> Doc OutputAnnotation)
-> [(Name, Docstring DocTerm)] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> (Name, Docstring DocTerm) -> Doc OutputAnnotation
prettyImplementationParam (((Name, Docstring DocTerm) -> Name)
-> [(Name, Docstring DocTerm)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Docstring DocTerm) -> Name
forall a b. (a, b) -> a
fst [(Name, Docstring DocTerm)]
argDocs)) [(Name, Docstring DocTerm)]
argDocs))
iname :: Maybe Name -> Doc OutputAnnotation
iname Maybe Name
Nothing = Doc OutputAnnotation
forall a. Doc a
empty
iname (Just Name
n) = Name -> Doc OutputAnnotation
annName Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
space
prettyImplementationParam :: [Name] -> (Name, Docstring DocTerm) -> Doc OutputAnnotation
prettyImplementationParam [Name]
params (Name
name, Docstring DocTerm
doc) =
if Docstring DocTerm -> Bool
forall a. Docstring a -> Bool
nullDocstring Docstring DocTerm
doc
then Doc OutputAnnotation
forall a. Doc a
empty
else Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
False ([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
params (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) Name
name Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
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 (Name -> [Name] -> Name
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 ([PArg] -> PTerm) -> [PArg] -> PTerm
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) = (Int -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp Int
prty [ArgOpt]
opts Name
p (Name -> PTerm -> PTerm
updateRef Name
p PTerm
ref)) PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [Name] -> [PArg] -> [PArg]
updateArgs [Name]
ps [PArg]
as
updateArgs [Name]
ps (PArg
a:[PArg]
as) = PArg
a PArg -> [PArg] -> [PArg]
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 =
[Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
cat (Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. Doc a -> [Doc a] -> [Doc a]
punctuate (Doc OutputAnnotation
forall a. Doc a
comma Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
space) ((PTerm -> Doc OutputAnnotation)
-> [PTerm] -> [Doc OutputAnnotation]
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 ((Name, Maybe (Docstring DocTerm)) -> Bool)
-> [(Name, Maybe (Docstring DocTerm))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe (Docstring DocTerm) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Docstring DocTerm) -> Bool)
-> ((Name, Maybe (Docstring DocTerm)) -> Maybe (Docstring DocTerm))
-> (Name, Maybe (Docstring DocTerm))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Maybe (Docstring DocTerm)) -> Maybe (Docstring DocTerm)
forall a b. (a, b) -> b
snd) [(Name, Maybe (Docstring DocTerm))]
params
then [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep (((Name, Maybe (Docstring DocTerm)) -> Doc OutputAnnotation)
-> [(Name, Maybe (Docstring DocTerm))] -> [Doc OutputAnnotation]
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 Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
-> (Docstring DocTerm -> Doc OutputAnnotation)
-> Maybe (Docstring DocTerm)
-> Doc OutputAnnotation
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc OutputAnnotation
forall a. Doc a
empty (IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist) Maybe (Docstring DocTerm)
md) [(Name, Maybe (Docstring DocTerm))]
params)
else [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
hsep (Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. Doc a -> [Doc a] -> [Doc a]
punctuate Doc OutputAnnotation
forall a. Doc a
comma (((Name, Maybe (Docstring DocTerm)) -> Doc OutputAnnotation)
-> [(Name, Maybe (Docstring DocTerm))] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
False [(Name, Bool)]
params' (Name -> Doc OutputAnnotation)
-> ((Name, Maybe (Docstring DocTerm)) -> Name)
-> (Name, Maybe (Docstring DocTerm))
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Maybe (Docstring DocTerm)) -> Name
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)
= Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Record" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
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 Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
if Docstring DocTerm -> Bool
forall a. Docstring a -> Bool
nullDocstring Docstring DocTerm
doc
then Doc OutputAnnotation
forall a. Doc a
empty
else Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
(DocTerm -> String -> Doc OutputAnnotation)
-> Docstring DocTerm -> Doc OutputAnnotation
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)
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> (if [(Name, PTerm, Maybe (Docstring DocTerm))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, PTerm, Maybe (Docstring DocTerm))]
params
then Doc OutputAnnotation
forall a. Doc a
empty
else Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Parameters:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> Doc OutputAnnotation
prettyParameters) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line)
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Constructor:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> IState -> Bool -> FunDoc -> Doc OutputAnnotation
pprintFDWithoutTotality IState
ist Bool
False FunDoc
ctor)
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Projections:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((FunDoc -> Doc OutputAnnotation)
-> [FunDoc] -> [Doc OutputAnnotation]
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' = [Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
pNames (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)
prettyParameters :: Doc OutputAnnotation
prettyParameters =
if (Maybe (Docstring DocTerm) -> Bool)
-> [Maybe (Docstring DocTerm)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe (Docstring DocTerm) -> Bool
forall a. Maybe a -> Bool
isJust [Maybe (Docstring DocTerm)
d | (Name
_,PTerm
_,Maybe (Docstring DocTerm)
d) <- [(Name, PTerm, Maybe (Docstring DocTerm))]
params]
then [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep (((Name, PTerm, Maybe (Docstring DocTerm)) -> Doc OutputAnnotation)
-> [(Name, PTerm, Maybe (Docstring DocTerm))]
-> [Doc OutputAnnotation]
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) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
-> (Docstring DocTerm -> Doc OutputAnnotation)
-> Maybe (Docstring DocTerm)
-> Doc OutputAnnotation
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc OutputAnnotation
forall a. Doc a
empty (IState -> Docstring DocTerm -> Doc OutputAnnotation
showDoc IState
ist) Maybe (Docstring DocTerm)
d) [(Name, PTerm, Maybe (Docstring DocTerm))]
params)
else [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
hsep (Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. Doc a -> [Doc a] -> [Doc a]
punctuate Doc OutputAnnotation
forall a. Doc a
comma (((Name, PTerm) -> Doc OutputAnnotation)
-> [(Name, PTerm)] -> [Doc OutputAnnotation]
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 Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
":" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
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)
= Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Named implementation:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
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)
= Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Module" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
"." [String]
mod)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
(DocTerm -> String -> Doc OutputAnnotation)
-> Docstring DocTerm -> Doc OutputAnnotation
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 = Docstring a -> Docstring a
forall a. a -> a
id
howMuch HowMuchDocs
OverviewDocs = Docstring a -> Docstring a
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' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
modDocName
= do IState
i <- Idris IState
getIState
case Name -> Ctxt (Docstring DocTerm) -> Maybe (Docstring DocTerm)
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt (Docstring DocTerm)
idris_moduledocs IState
i) of
Just Docstring DocTerm
doc -> Docs -> Idris Docs
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Docs -> Idris Docs)
-> (Docstring DocTerm -> Docs) -> Docstring DocTerm -> Idris Docs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> Docstring DocTerm -> Docs
forall d. [String] -> d -> Docs' d
ModDoc ([String] -> [String]
forall a. [a] -> [a]
reverse ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack [Text]
ns)) (Docstring DocTerm -> Idris Docs)
-> Docstring DocTerm -> Idris Docs
forall a b. (a -> b) -> a -> b
$ HowMuchDocs -> Docstring DocTerm -> Docstring DocTerm
forall {a}. HowMuchDocs -> Docstring a -> Docstring a
howMuch HowMuchDocs
w Docstring DocTerm
doc
Maybe (Docstring DocTerm)
Nothing -> String -> Idris Docs
forall a. String -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Idris Docs) -> String -> Idris Docs
forall a b. (a -> b) -> a -> b
$ String
"Module docs for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show ([String] -> [String]
forall a. [a] -> [a]
reverse ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack [Text]
ns)) String -> String -> String
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 <- Name -> Ctxt InterfaceInfo -> Maybe InterfaceInfo
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 <- Name -> Ctxt RecordInfo -> Maybe RecordInfo
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 <- Name -> Ctxt TypeInfo -> Maybe TypeInfo
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
Docs -> Idris Docs
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Docs -> Idris Docs) -> Docs -> Idris Docs
forall a b. (a -> b) -> a -> b
$ Name -> FunDoc -> Docs
forall d. Name -> FunDoc' d -> Docs' d
NamedImplementationDoc Name
interface_ FunDoc
fd
| Bool
otherwise
-> do FunDoc
fd <- Name -> Idris FunDoc
docFun Name
n
Docs -> Idris Docs
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FunDoc -> Docs
forall d. FunDoc' d -> Docs' d
FunDoc FunDoc
fd)
Docs -> Idris Docs
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Docs -> Idris Docs) -> Docs -> Idris Docs
forall a b. (a -> b) -> a -> b
$ (Docstring DocTerm -> Docstring DocTerm) -> Docs -> Docs
forall a b. (a -> b) -> Docs' a -> Docs' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (HowMuchDocs -> Docstring DocTerm -> Docstring DocTerm
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 =
[Name] -> Maybe Name
forall a. [a] -> Maybe a
listToMaybe [ Name
cn
| (Name
cn, InterfaceInfo
ci) <- Ctxt InterfaceInfo -> [(Name, InterfaceInfo)]
forall a. Ctxt a -> [(Name, a)]
toAlist (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist)
, Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Name, Bool) -> Name) -> [(Name, Bool)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Name
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 <- (Name -> Idris FunDoc)
-> [Name] -> StateT IState (ExceptT Err IO) [FunDoc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Name -> Idris FunDoc
docFun (TypeInfo -> [Name]
con_names TypeInfo
ti)
Docs -> Idris Docs
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FunDoc -> [FunDoc] -> Docs
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 = [(Docstring DocTerm, [(Name, Docstring DocTerm)])]
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall a. [a] -> Maybe a
listToMaybe ([(Docstring DocTerm, [(Name, Docstring DocTerm)])]
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> [(Docstring DocTerm, [(Name, Docstring DocTerm)])]
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall a b. (a -> b) -> a -> b
$ Name
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Docstring DocTerm, [(Name, Docstring DocTerm)])]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Docstring DocTerm, [(Name, Docstring DocTerm)])])
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Docstring DocTerm, [(Name, Docstring DocTerm)])]
forall a b. (a -> b) -> a -> b
$ IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
i
docstr :: Docstring DocTerm
docstr = Docstring DocTerm
-> ((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm)
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Docstring DocTerm
forall a. Docstring a
emptyDocstring (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm
forall a b. (a, b) -> a
fst Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
docStrings
params :: [(Name, Maybe (Docstring DocTerm))]
params = (Name -> (Name, Maybe (Docstring DocTerm)))
-> [Name] -> [(Name, Maybe (Docstring DocTerm))]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
pn -> (Name
pn, Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
docStrings Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> ((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm))
-> Maybe (Docstring DocTerm)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Name -> [(Name, Docstring DocTerm)] -> Maybe (Docstring DocTerm)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
pn ([(Name, Docstring DocTerm)] -> Maybe (Docstring DocTerm))
-> ((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Name, Docstring DocTerm)])
-> (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Name, Docstring DocTerm)]
forall a b. (a, b) -> b
snd)))
(InterfaceInfo -> [Name]
interface_params InterfaceInfo
ci)
docsForImplementation :: Name -> (Docstring DocTerm, [(Name, Docstring DocTerm)])
docsForImplementation Name
impl = (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall a. a -> Maybe a -> a
fromMaybe (Docstring DocTerm
forall a. Docstring a
emptyDocstring, []) (Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> (Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> (Name -> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> Name
-> (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(Name
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Name
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall a b c. (a -> b -> c) -> b -> a -> c
flip Name
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
i) (Name -> (Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> Name -> (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall a b. (a -> b) -> a -> b
$
Name
impl
implementations :: [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
implementations = (Name
-> (Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)])))
-> [Name]
-> [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
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))
([Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub (((Name, Bool) -> Name) -> [(Name, Bool)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Name
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') = ((Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> Bool)
-> [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> ([(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))],
[(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (PTerm -> Bool
isSubInterface (PTerm -> Bool)
-> ((Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> PTerm)
-> (Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> Bool
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 = [Maybe PTerm] -> [PTerm]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe PTerm] -> [PTerm]) -> [Maybe PTerm] -> [PTerm]
forall a b. (a -> b) -> a -> b
$ (PDecl' PTerm -> Maybe PTerm) -> [PDecl' PTerm] -> [Maybe PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PDecl' PTerm -> Maybe PTerm
forall {a}. PDecl' a -> Maybe a
getDImpl (InterfaceInfo -> [PDecl' PTerm]
interface_default_super_interfaces InterfaceInfo
ci)
[FunDoc]
mdocs <- ((Name, (Bool, FnOpts, PTerm)) -> Idris FunDoc)
-> [(Name, (Bool, FnOpts, PTerm))]
-> StateT IState (ExceptT Err IO) [FunDoc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Name -> Idris FunDoc
docFun (Name -> Idris FunDoc)
-> ((Name, (Bool, FnOpts, PTerm)) -> Name)
-> (Name, (Bool, FnOpts, PTerm))
-> Idris FunDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, (Bool, FnOpts, PTerm)) -> Name
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
_ -> Maybe FunDoc -> StateT IState (ExceptT Err IO) (Maybe FunDoc)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FunDoc
forall a. Maybe a
Nothing
Name
_ -> (FunDoc -> Maybe FunDoc)
-> Idris FunDoc -> StateT IState (ExceptT Err IO) (Maybe FunDoc)
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FunDoc -> Maybe FunDoc
forall a. a -> Maybe a
Just (Idris FunDoc -> StateT IState (ExceptT Err IO) (Maybe FunDoc))
-> Idris FunDoc -> StateT IState (ExceptT Err IO) (Maybe FunDoc)
forall a b. (a -> b) -> a -> b
$ Name -> Idris FunDoc
docFun Name
ctorN
Docs -> Idris Docs
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Docs -> Idris Docs) -> Docs -> Idris Docs
forall a b. (a -> b) -> a -> b
$ Name
-> Docstring DocTerm
-> [FunDoc]
-> [(Name, Maybe (Docstring DocTerm))]
-> [PTerm]
-> [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> [PTerm]
-> [PTerm]
-> Maybe FunDoc
-> Docs
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' (((Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> PTerm)
-> [(Maybe Name, PTerm,
(Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> [PTerm]
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) = (Name -> Name) -> Maybe Name -> Maybe Name
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name -> [Text] -> Name) -> [Text] -> Name -> Name
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
_) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
namedImpl Name
_ = Maybe 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]
_) = a -> Maybe a
forall a. a -> Maybe a
Just a
t
getDImpl PDecl' a
_ = Maybe 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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n Bool -> Bool -> Bool
&& (PArg -> PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> PTerm
forall t. PArg' t -> t
getTm [PArg]
args [PTerm] -> [PTerm] -> Bool
forall a. Eq a => a -> a -> Bool
== (PArg -> PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> PTerm
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 = [(Docstring DocTerm, [(Name, Docstring DocTerm)])]
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall a. [a] -> Maybe a
listToMaybe ([(Docstring DocTerm, [(Name, Docstring DocTerm)])]
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> [(Docstring DocTerm, [(Name, Docstring DocTerm)])]
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall a b. (a -> b) -> a -> b
$ Name
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Docstring DocTerm, [(Name, Docstring DocTerm)])]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Docstring DocTerm, [(Name, Docstring DocTerm)])])
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Docstring DocTerm, [(Name, Docstring DocTerm)])]
forall a b. (a -> b) -> a -> b
$ IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
i
docstr :: Docstring DocTerm
docstr = Docstring DocTerm
-> ((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm)
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Docstring DocTerm
forall a. Docstring a
emptyDocstring (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm
forall a b. (a, b) -> a
fst Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
docStrings
params :: [(Name, PTerm, Maybe (Docstring DocTerm))]
params = ((Name, PTerm) -> (Name, PTerm, Maybe (Docstring DocTerm)))
-> [(Name, PTerm)] -> [(Name, PTerm, Maybe (Docstring DocTerm))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
pn,PTerm
pt) -> (Name
pn, PTerm
pt, Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
docStrings Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> ((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm))
-> Maybe (Docstring DocTerm)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Name -> [(Name, Docstring DocTerm)] -> Maybe (Docstring DocTerm)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Name -> Name
nsroot Name
pn) ([(Name, Docstring DocTerm)] -> Maybe (Docstring DocTerm))
-> ((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Name, Docstring DocTerm)])
-> (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Name, Docstring DocTerm)]
forall a b. (a, b) -> b
snd)))
(RecordInfo -> [(Name, PTerm)]
record_parameters RecordInfo
ri)
[FunDoc]
pdocs <- (Name -> Idris FunDoc)
-> [Name] -> StateT IState (ExceptT Err IO) [FunDoc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Name -> Idris FunDoc
docFun (RecordInfo -> [Name]
record_projections RecordInfo
ri)
FunDoc
ctorDocs <- Name -> Idris FunDoc
docFun (Name -> Idris FunDoc) -> Name -> Idris FunDoc
forall a b. (a -> b) -> a -> b
$ RecordInfo -> Name
record_constructor RecordInfo
ri
Docs -> Idris Docs
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Docs -> Idris Docs) -> Docs -> Idris Docs
forall a b. (a -> b) -> a -> b
$ Name
-> Docstring DocTerm
-> FunDoc
-> [FunDoc]
-> [(Name, PTerm, Maybe (Docstring DocTerm))]
-> Docs
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 Name
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Docstring DocTerm, [(Name, Docstring DocTerm)])]
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)])]
_ -> (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 = (FixDecl -> Bool) -> [FixDecl] -> [FixDecl]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Fix Fixity
_ String
x) -> String
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> String
funName Name
n) [FixDecl]
infixes
let f :: Maybe Fixity
f = case [FixDecl]
fixdecls of
[] -> Maybe Fixity
forall a. Maybe a
Nothing
(Fix Fixity
x String
_:[FixDecl]
_) -> Fixity -> Maybe Fixity
forall a. a -> Maybe a
Just Fixity
x
FunDoc -> Idris FunDoc
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
-> Docstring DocTerm
-> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
-> PTerm
-> Maybe Fixity
-> FunDoc
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 = Name -> String
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, Name -> [(Name, Docstring DocTerm)] -> Maybe (Docstring DocTerm)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
name [(Name, Docstring DocTerm)]
ds) (Name, PTerm, Plicity, Maybe (Docstring DocTerm))
-> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
-> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
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 = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Primitive" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text (if Const -> Bool
constIsType Const
c then String
"type" else String
"value") Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
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) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
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) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
str)
where t :: Const -> PTerm
t (Fl Double
_) = FC -> Const -> PTerm
PConstant FC
NoFC (Const -> PTerm) -> Const -> PTerm
forall a b. (a -> b) -> a -> b
$ ArithTy -> Const
AType ArithTy
ATFloat
t (BI Integer
_) = FC -> Const -> PTerm
PConstant FC
NoFC (Const -> PTerm) -> Const -> PTerm
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 (Const -> PTerm) -> Const -> PTerm
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) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
type1Doc Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
4 (Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
typeDescription)