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