0 | module Idris.Doc.String

  2 | import Core.Env

  3 | import Core.TT.Traversals

  5 | import Idris.Doc.Display

  6 | import Idris.Pretty

  7 | import Idris.REPL.Opts

  8 | import Idris.Resugar

  9 | import Idris.Syntax

 10 | import Idris.Syntax.Views

 12 | import TTImp.TTImp

 13 | import TTImp.TTImp.Functor

 14 | import TTImp.Elab.Prim

 16 | import Data.Maybe

 17 | import Data.SortedSet

 18 | import Data.SortedMap

 19 | import Data.String

 21 | import Libraries.Data.ANameMap

 22 | import Libraries.Data.NameMap

 23 | import Libraries.Data.NatSet

 24 | import Libraries.Data.WithDefault

 26 | import public Libraries.Text.PrettyPrint.Prettyprinter

 27 | import public Libraries.Text.PrettyPrint.Prettyprinter.Util

 29 | import public Idris.Doc.Annotations

 30 | import Idris.Doc.Keywords

 31 | import Idris.Doc.Brackets

 33 | %default covering

 37 | addDocString : {auto c : Ref Ctxt Defs} ->

 38 |                {auto s : Ref Syn SyntaxInfo} ->

 39 |                Name -> String ->

 40 |                Core ()

 41 | addDocString n_in doc

 42 |     = do n <- inCurrentNS n_in

 43 |          log "doc.record" 50 $

 44 |            "Adding doc for " ++ show n_in ++ " (aka " ++ show n ++ " in current NS)"

 45 |          update Syn { defDocstrings  $= addName n doc,

 46 |                       saveDocstrings $= insert n () }

 51 | addDocStringNS : {auto c : Ref Ctxt Defs} ->

 52 |                  {auto s : Ref Syn SyntaxInfo} ->

 53 |                  Namespace -> Name -> String ->

 54 |                  Core ()

 55 | addDocStringNS ns n_in doc

 56 |     = do n <- inCurrentNS n_in

 57 |          let n' = case n of

 58 |                        NS old root => NS (old <.> ns) root

 59 |                        root => NS ns root

 60 |          update Syn { defDocstrings  $= addName n' doc,

 61 |                       saveDocstrings $= insert n' () }

 63 | prettyName : Name -> Doc IdrisDocAnn

 64 | prettyName n =

 65 |   case userNameRoot n of

 66 |     -- shouldn't happen: we only show UN anyways...

 67 |     Nothing => pretty0 (nameRoot n)

 68 |     Just un => if isOpUserName un then parens (pretty0 un) else pretty0 un

 70 | prettyKindedName : Maybe String -> Doc IdrisDocAnn -> Doc IdrisDocAnn

 71 | prettyKindedName Nothing   nm = nm

 72 | prettyKindedName (Just kw) nm

 73 |   = annotate (Syntax Keyword) (pretty0 kw) <++> nm

 76 | prettyType : {auto c : Ref Ctxt Defs} ->

 77 |              {auto s : Ref Syn SyntaxInfo} ->

 78 |              (IdrisSyntax -> ann) -> ClosedTerm -> Core (Doc ann)

 79 | prettyType syn ty = do

 80 |   defs <- get Ctxt

 81 |   ty <- normaliseHoles defs Env.empty ty

 82 |   ty <- toFullNames ty

 83 |   ty <- resugar Env.empty ty

 84 |   pure (prettyBy syn ty)

 87 | getImplDocs : {auto c : Ref Ctxt Defs} ->

 88 |               {auto s : Ref Syn SyntaxInfo} ->

 89 |               (keep : ClosedTerm -> Core Bool) ->

 90 |               Core (List (Doc IdrisDocAnn))

 91 | getImplDocs keep

 92 |     = do defs <- get Ctxt

 93 |          docss <- for (concat $ values $ typeHints defs) $ \ (impl, _) =>

 94 |            do Just def <- lookupCtxtExact impl (gamma defs)

 95 |                 | _ => pure []

 96 |               -- Only keep things that look like implementations.

 97 |               -- i.e. get rid of data constructors

 98 |               let Just Func = defNameType (definition def)

 99 |                 | _ => pure []

100 |               -- Check that the type mentions the name of interest

101 |               ty <- toFullNames !(normaliseHoles defs Env.empty (type def))

102 |               True <- keep ty

103 |                 | False => pure []

104 |               ty <- resugar Env.empty ty

105 |               pure [annotate (Decl impl) $ prettyBy Syntax ty]

106 |          pure $ case concat docss of

107 |            [] => []

108 |            [doc] => [header "Hint" <++> annotate Declarations doc]

109 |            docs  => [vcat [header "Hints"

110 |                     , annotate Declarations $

111 |                         vcat $ map (indent 2) docs]]

114 | getHintsForType : {auto c : Ref Ctxt Defs} ->

115 |                   {auto s : Ref Syn SyntaxInfo} ->

116 |                   Name -> Core (List (Doc IdrisDocAnn))

117 | getHintsForType nty

118 |     = do log "doc.data" 10 $ "Looking at \{show nty}"

119 |          getImplDocs $ \ ty =>

120 |            do let nms = allGlobals ty

121 |               log "doc.data" 10 $ unlines

122 |                 [ "Candidate: " ++ show ty

123 |                 , "Containing names: " ++ show nms

124 |                 ]

125 |               pure $ isJust (lookup nty nms)

128 | getHintsForPrimitive : {auto c : Ref Ctxt Defs} ->

129 |                        {auto s : Ref Syn SyntaxInfo} ->

130 |                        Constant -> Core (List (Doc IdrisDocAnn))

131 | getHintsForPrimitive c

132 |     = do log "doc.data" 10 $ "Looking at \{show c}"

133 |          getImplDocs $ \ ty =>

134 |            do let nms = allConstants ty

135 |               log "doc.data" 10 $ unlines

136 |                 [ "Candidate: " ++ show ty

137 |                 , "Containing constants: " ++ show nms

138 |                 ]

139 |               pure $ contains c nms

142 | getDocsForPrimitive : {auto c : Ref Ctxt Defs} ->

143 |                       {auto s : Ref Syn SyntaxInfo} ->

144 |                       Constant -> Core (Doc IdrisDocAnn)

145 | getDocsForPrimitive constant = do

146 |     let (_, type) = checkPrim EmptyFC constant

147 |     let typeString = prettyBy Syntax constant

148 |                      <++> colon

149 |                      <++> prettyBy Syntax !(resugar Env.empty type)

150 |     hintsDoc <- getHintsForPrimitive constant

151 |     pure $ vcat $ typeString

152 |                :: indent 2 (primDoc constant)

153 |                :: hintsDoc

155 |   where

156 |   primTyDoc : PrimType -> Doc IdrisDocAnn

157 |   primTyDoc IntType = "Primitive type of bounded signed integers (backend dependent size)"

158 |   primTyDoc Int8Type = "Primitive type of 8 bits signed integers"

159 |   primTyDoc Int16Type = "Primitive type of 16 bits signed integers"

160 |   primTyDoc Int32Type = "Primitive type of 32 bits signed integers"

161 |   primTyDoc Int64Type = "Primitive type of 64 bits signed integers"

162 |   primTyDoc IntegerType = "Primitive type of unbounded signed integers"

163 |   primTyDoc Bits8Type = "Primitive type of 8 bits unsigned integers"

164 |   primTyDoc Bits16Type = "Primitive type of 16 bits unsigned integers"

165 |   primTyDoc Bits32Type = "Primitive type of 32 bits unsigned integers"

166 |   primTyDoc Bits64Type = "Primitive type of 64 bits unsigned integers"

167 |   primTyDoc StringType = "Primitive type of strings"

168 |   primTyDoc CharType = "Primitive type of characters"

169 |   primTyDoc DoubleType = "Primitive type of double-precision floating-points"

170 |   primTyDoc WorldType = "Primitive type of tokens for IO actions"

172 |   primDoc : Constant -> Doc IdrisDocAnn

173 |   primDoc (I i) = "Primitive signed int value (backend-dependent precision)"

174 |   primDoc (I8 i) = "Primitive signed 8 bits value"

175 |   primDoc (I16 i) = "Primitive signed 16 bits value"

176 |   primDoc (I32 i) = "Primitive signed 32 bits value"

177 |   primDoc (I64 i) = "Primitive signed 64 bits value"

178 |   primDoc (BI i) = "Primitive unsigned int value (backend-dependent precision)"

179 |   primDoc (B8 i) = "Primitive unsigned 8 bits value"

180 |   primDoc (B16 i) = "Primitive unsigned 16 bits value"

181 |   primDoc (B32 i) = "Primitive unsigned 32 bits value"

182 |   primDoc (B64 i) = "Primitive unsigned 64 bits value"

183 |   primDoc (Str s) = "Primitive string value"

184 |   primDoc (Ch c) = "Primitive character value"

185 |   primDoc (Db d) = "Primitive double value"

186 |   primDoc (PrT t) = primTyDoc t

187 |   primDoc WorldVal = "Primitive token for IO actions"

189 | public export

190 | data Config : Type where

191 |   ||| Configuration of the printer for a name

196 |   MkConfig : {default True  showType    : Bool} ->

197 |              {default True  longNames   : Bool} ->

198 |              {default False dropFirst   : Bool} ->

199 |              {default True  getTotality : Bool} ->

200 |              Config

210 | methodsConfig : Config

212 |   = MkConfig {showType = True}

213 |              {longNames = False}

214 |              {dropFirst = True}

215 |              {getTotality = False}

218 | shortNamesConfig : Config

220 |   = MkConfig {showType = True}

221 |              {longNames = False}

222 |              {dropFirst = False}

223 |              {getTotality = True}

226 | justUserDoc : Config

228 |   = MkConfig {showType = False}

229 |              {longNames = False}

230 |              {dropFirst = True}

231 |              {getTotality = False}

234 | getDocsForName : {auto o : Ref ROpts REPLOpts} ->

235 |                  {auto c : Ref Ctxt Defs} ->

236 |                  {auto s : Ref Syn SyntaxInfo} ->

237 |                  FC -> Name -> Config -> Core (Doc IdrisDocAnn)

238 | getDocsForName fc n config

239 |     = do syn <- get Syn

240 |          defs <- get Ctxt

241 |          let extra = case nameRoot n of

242 |                        "-" => [NS numNS (UN $ Basic "negate")]

243 |                        _ => []

244 |          resolved <- lookupCtxtName n (gamma defs)

245 |          let all@(_ :: _) = extra ++ map fst resolved

246 |              | _ => undefinedName fc n

247 |          let ns@(_ :: _) = concatMap (\n => lookupName n (defDocstrings syn)) all

248 |              | [] => pure emptyDoc

249 |          docs <- traverse (showDoc config) ns

250 |          pure $ vcat docs

251 |   where

253 |     showDoc : Config -> (Name, String) -> Core (Doc IdrisDocAnn)

255 |     reflowDoc : String -> List (Doc IdrisDocAnn)

256 |     reflowDoc str = map (indent 2 . pretty0) (lines str)

258 |     showTotal : Totality -> Maybe (Doc IdrisDocAnn)

259 |     showTotal tot

260 |         = case isTerminating tot of

261 |                Unchecked => Nothing

262 |                _ => pure (header "Totality" <++> annotate (Syntax Keyword) (pretty0 tot))

264 |     showVisible : Visibility -> Doc IdrisDocAnn

265 |     showVisible vis = header "Visibility" <++> annotate (Syntax Keyword) (pretty0 vis)

267 |     getDConDoc : {default True showType : Bool} -> Name -> Core (Doc IdrisDocAnn)

268 |     getDConDoc con

269 |         = do defs <- get Ctxt

270 |              Just def <- lookupCtxtExact con (gamma defs)

271 |                   -- should never happen, since we know that the DCon exists:

272 |                   | Nothing => pure Empty

273 |              syn <- get Syn

274 |              ty <- prettyType Syntax (type def)

275 |              let conWithTypeDoc

276 |                    = annotate (Decl con)

277 |                    $ ifThenElse showType

278 |                        (hsep [dCon con (prettyName con), colon, ty])

279 |                        (dCon con (prettyName con))

280 |              case lookupName con (defDocstrings syn) of

281 |                [(n, "")] => pure conWithTypeDoc

282 |                [(n, str)] => pure $ vcat

283 |                     [ conWithTypeDoc

284 |                     , annotate DocStringBody

285 |                     $ annotate UserDocString

286 |                     $ vcat $ reflowDoc str

287 |                     ]

288 |                _ => pure conWithTypeDoc

290 |     ||| The name corresponds to an implementation, typeset its type accordingly

291 |     getImplDoc : Name -> Core (List (Doc IdrisDocAnn))

292 |     getImplDoc n

293 |         = do defs <- get Ctxt

294 |              Just def <- lookupCtxtExact n (gamma defs)

295 |                   | Nothing => pure []

296 |              ty <- prettyType Syntax (type def)

297 |              pure [annotate (Decl n) ty]

299 |     getMethDoc : Method -> Core (List (Doc IdrisDocAnn))

300 |     getMethDoc meth

301 |         = do syn <- get Syn

302 |              let [nstr] = lookupName meth.name.val (defDocstrings syn)

303 |                   | _ => pure []

304 |              pure <$> showDoc methodsConfig nstr

306 |     getInfixDoc : Name -> Core (List (Doc IdrisDocAnn))

307 |     getInfixDoc n

308 |         = let names = lookupName (UN $ Basic $ nameRoot n) (infixes !(get Syn))

309 |           in pure $ map printName names

310 |         where

311 |           printName : (Name, FC, Fixity, Nat) -> (Doc IdrisDocAnn)

312 |           printName (name,  loc, fixity, assoc) =

313 |             -- todo,  change display as "infix operator (++)

314 |              hsep

315 |                   [ pretty0 (show fixity)

316 |                   , "operator,"

317 |                   , "level"

318 |                   , pretty0 (show assoc)

319 |                   ]

321 |     getPrefixDoc : Name -> Core (List (Doc IdrisDocAnn))

322 |     getPrefixDoc n

323 |         = let names = lookupName (UN $ Basic $ nameRoot n) (prefixes !(get Syn))

324 |           in pure $ map printPrefixName names

325 |           where

326 |             printPrefixName : (Name, FC, Nat) -> Doc IdrisDocAnn

327 |             printPrefixName (_, _, assoc) = "prefix operator, level" <++> pretty0 (show assoc)

329 |     getFixityDoc : Name -> Core (List (Doc IdrisDocAnn))

330 |     getFixityDoc n =

331 |       pure $ case toList !(getInfixDoc n) ++ toList !(getPrefixDoc n) of

332 |         []  => []

333 |         [f] => [header "Fixity Declaration" <++> f]

334 |         fs  => [header "Fixity Declarations" <+> Line <+>

335 |                  indent 2 (vcat fs)]

337 |     getIFaceDoc : (Name, IFaceInfo) -> Core (Doc IdrisDocAnn)

338 |     getIFaceDoc (n, iface)

339 |         = do let params =

340 |                 case params iface of

341 |                      [] => []

342 |                      ps => [hsep (header "Parameters" :: punctuate comma (map pretty0 ps))]

343 |              let constraints =

344 |                 case !(traverse (pterm . map defaultKindedName) (parents iface)) of

345 |                      [] => []

346 |                      ps => [hsep (header "Constraints" :: punctuate comma (map (prettyBy Syntax) ps))]

347 |              icon <- do cName <- toFullNames (iconstructor iface)

348 |                         case dropNS cName of

349 |                           UN{} => do doc <- getDConDoc {showType = False} cName

350 |                                      pure $ [header "Constructor" <++> annotate Declarations doc]

351 |                           _ => pure [] -- machine inserted

352 |              mdocs <- traverse getMethDoc (methods iface)

353 |              let meths = case concat mdocs of

354 |                            [] => []

355 |                            docs => [vcat [header "Methods", annotate Declarations $ vcat $ map (indent 2) docs]]

356 |              sd <- getSearchData fc False n

357 |              idocs <- case hintGroups sd of

358 |                            [] => pure (the (List (List (Doc IdrisDocAnn))) [])

359 |                            ((_, tophs) :: _) => traverse getImplDoc tophs

360 |              let insts = case concat idocs of

361 |                            [] => []

362 |                            [doc] => [header "Implementation" <++> annotate Declarations doc]

363 |                            docs => [vcat [header "Implementations"

364 |                                    , annotate Declarations $ vcat $ map (indent 2) docs]]

365 |              pure (vcat (params ++ constraints ++ icon ++ meths ++ insts))

367 |     getFieldDoc : Name -> Core (Doc IdrisDocAnn)

368 |     getFieldDoc nm

369 |       = do syn <- get Syn

370 |            defs <- get Ctxt

371 |            Just def <- lookupCtxtExact nm (gamma defs)

372 |                 -- should never happen, since we know that the DCon exists:

373 |                 | Nothing => pure Empty

374 |            ty <- prettyType Syntax (type def)

375 |            let projDecl = annotate (Decl nm) $

376 |                             reAnnotate Syntax (prettyRig def.multiplicity) <+> hsep

377 |                             [ fun nm (prettyName nm), colon, ty ]

378 |            case lookupName nm (defDocstrings syn) of

379 |                 [(_, "")] => pure projDecl

380 |                 [(_, str)] =>

381 |                   pure $ vcat [ projDecl

382 |                               , annotate DocStringBody

383 |                               $ annotate UserDocString

384 |                               $ vcat $ reflowDoc str

385 |                               ]

386 |                 _ => pure projDecl

388 |     getFieldsDoc : Name -> Core (Maybe (Doc IdrisDocAnn))

389 |     getFieldsDoc recName

390 |       = do let (Just ns, n) = displayName recName

391 |                | _ => pure Nothing

392 |            let recNS = ns <.> mkNamespace n

393 |            defs <- get Ctxt

394 |            let fields = getFieldNames (gamma defs) recNS

395 |            case fields of

396 |              [] => pure Nothing

397 |              [proj] => pure $ Just $ header "Projection" <++> annotate Declarations !(getFieldDoc proj)

398 |              projs => pure $ Just $ vcat

399 |                            [ header "Projections"

400 |                            , annotate Declarations $ vcat $

401 |                                map (indent 2) $ !(traverse getFieldDoc projs)

402 |                            ]

404 |     getExtra : Name -> GlobalDef -> Core (Maybe String, List (Doc IdrisDocAnn))

405 |     getExtra n d = do

406 |       do syn <- get Syn

407 |          let [] = lookupName n (ifaces syn)

408 |              | [ifacedata] => (Just "interface",) . pure <$> getIFaceDoc ifacedata

409 |              | _ => pure (Nothing, []) -- shouldn't happen, we've resolved ambiguity by now

410 |          case definition d of

411 |            PMDef {} => pure ( Nothing

412 |                                    , catMaybes [ showTotal (totality d)

413 |                                                , pure (showVisible (collapseDefault $ visibility d))])

414 |            TCon _ _ _ _ _ cons _ =>

415 |              do let tot = catMaybes [ showTotal (totality d)

416 |                                     , pure (showVisible (collapseDefault $ visibility d))]

417 |                 cdocs <- traverse (getDConDoc <=< toFullNames) (fromMaybe [] cons)

418 |                 cdoc <- case cdocs of

419 |                   [] => pure (Just "data", [])

420 |                   [doc] =>

421 |                     let cdoc = header "Constructor" <++> annotate Declarations doc in

422 |                     case !(getFieldsDoc n) of

423 |                       Nothing => pure (Just "data", [cdoc])

424 |                       Just fs => pure (Just "record", cdoc :: [fs])

425 |                   docs => pure (Just "data"

426 |                                , [vcat [header "Constructors"

427 |                                        , annotate Declarations $

428 |                                            vcat $ map (indent 2) docs]])

429 |                 idoc <- getHintsForType n

430 |                 pure (map (\ cons => tot ++ cons ++ idoc) cdoc)

431 |            _ => pure (Nothing, [])

433 |     showDoc (MkConfig {showType, longNames, dropFirst, getTotality}) (n, str)

434 |         = do defs <- get Ctxt

435 |              Just def <- lookupCtxtExact n (gamma defs)

436 |                   | Nothing => undefinedName fc n

437 |              -- First get the extra stuff because this also tells us whether a

438 |              -- definition is `data`, `record`, or `interface`.

439 |              (typ, extra) <- ifThenElse getTotality

440 |                                (getExtra n def)

441 |                                (pure (Nothing, []))

443 |              -- Then form the type declaration

444 |              ty <- resugar Env.empty =<< normaliseHoles defs Env.empty (type def)

445 |              -- when printing e.g. interface methods there is no point in

446 |              -- repeating the interface's name

447 |              let ty = ifThenElse (not dropFirst) ty $ case ty of

448 |                         PPi _ _ AutoImplicit _ _ sc => sc

449 |                         _ => ty

450 |              nm <- aliasName n

451 |              let prig = reAnnotate Syntax $ prettyRig def.multiplicity

452 |              let cat = showCategory Syntax def

453 |              let nm = prettyKindedName typ $ cat

454 |                     $ ifThenElse longNames (pretty0 (show nm)) (prettyName nm)

455 |              let deprecated = if Context.Deprecate `elem` def.flags

456 |                                  then annotate Deprecation "=DEPRECATED=" <+> line else emptyDoc

457 |              let docDecl = deprecated

458 |                      <+> annotate (Decl n) (hsep [prig <+> nm, colon, prettyBy Syntax ty])

460 |              -- Finally add the user-provided docstring

461 |              let docText = let docs = reflowDoc str in

462 |                            annotate UserDocString (vcat docs)

463 |                            <$ guard (not $ null docs)

464 |              fixes <- getFixityDoc n

465 |              let docBody =

466 |                   let docs = maybe id (::) docText

467 |                            $ map (indent 2) (extra ++ fixes)

468 |                   in annotate DocStringBody

469 |                      (concatWith (\l, r => l <+> hardline <+> r) docs)

470 |                      <$ guard (not (null docs))

471 |              let maybeDocDecl = [docDecl | showType]

472 |              pure . vcat . catMaybes $ maybeDocDecl :: (map Just $ docBody)

475 | getDocsForImplementation :

476 |   {auto s : Ref Syn SyntaxInfo} ->

477 |   {auto c : Ref Ctxt Defs} ->

478 |   PTerm -> Core (Maybe (Doc IdrisSyntax))

479 | getDocsForImplementation t = do

480 |   -- the term better be of the shape (I e1 e2 e3) where I is a name

481 |   let (PRef fc intf, args) = getFnArgs id t

482 |     | _ => pure Nothing

483 |   -- That name (I) better be the name of an interface

484 |   syn <- get Syn

485 |   -- Important: we shadow intf with the fully qualified version returned by lookupName

486 |   let [(intf, _)] = lookupName intf (ifaces syn)

487 |     | _ => pure Nothing

488 |   -- Now lookup the declared implementations for that interface

489 |   -- For now we only look at the top list

490 |   ((_, tophs) :: _) <- hintGroups <$> getSearchData fc False intf

491 |     | _ => pure Nothing

492 |   defs <- get Ctxt

493 |   impls <- map catMaybes $ for tophs $ \ hint => do

494 |     -- get the return type of all the candidate hints

495 |     Just (ix, def) <- lookupCtxtExactI hint (gamma defs)

496 |       | Nothing => pure Nothing

497 |     ty <- resugar Env.empty =<< normaliseHoles defs Env.empty (type def)

498 |     let (_, retTy) = underPis ty

499 |     -- try to see whether it approximates what we are looking for

500 |     -- we throw the head away because it'll be the interface name (I)

501 |     let (_, cargs) = getFnArgs defaultKindedName retTy

502 |     bs <- for (zip args cargs) $ \ (arg, carg) => do

503 |       -- For now we only compare the heads of the arguments because we expect

504 |       -- we are interested in implementations of the form

505 |       -- Eq (List a), Functor (Vect n), etc.

506 |       -- In the future we could be more discriminating and make sure we only

507 |       -- retain implementations whose type is fully compatible.

509 |       -- TODO: check the Args have the same shape before unArgging?

510 |       let ((PRef fc hd, _), (PRef _ chd, _)) = ( getFnArgs id (unArg arg), getFnArgs defaultKindedName (unArg carg))

511 |         | ((PPrimVal _ c, _), (PPrimVal _ c', _)) => pure (c == c')

512 |         | ((PType _, _), (PType _, _)) => pure True

513 |         | _ => pure False

514 |       -- if the names match on the nose we can readily say True

515 |       let False = dropNS hd == dropNS (fullName chd)

516 |         | True => pure True

517 |       -- otherwise we check hd is unknown in which case we're happy to

518 |       -- declare it to be a placeholder name and that it could possibly

519 |       -- unify e.g. a & b in (List a) vs. (List b)

520 |       existing <- lookupCtxtName hd (gamma defs)

521 |       log "doc.implementation" 50 $ unwords

522 |         [ "Mismatch between \{show hd} and \{show chd},"

523 |         , "checking whether \{show hd} exists:"

524 |         , "\{show $ length existing} candidates"

525 |         ]

526 |       let [] = existing

527 |         | _ => pure False

528 |       -- If the name starts with an uppercase letter it's probably a misspelt constructor name

529 |       whenJust ((isUN >=> (isBasic . snd) >=> strUncons >=> (guard . isUpper . fst)) hd) $ \ _ =>

530 |         undefinedName fc hd

531 |       pure True

532 |     -- all arguments better be valid approximations

533 |     let True = all id bs

534 |       | False => pure Nothing

535 |     pure (Just (hint, ix, def))

536 |   case impls of

537 |     [] => pure $ Just $ "Could not find an implementation for" <++> pretty0 (show t) --hack

538 |     _ => do ds <- traverse (displayImpl defs) impls

539 |             pure $ Just $ vcat ds

542 | getDocsForPTerm : {auto o : Ref ROpts REPLOpts} ->

543 |                   {auto c : Ref Ctxt Defs} ->

544 |                   {auto s : Ref Syn SyntaxInfo} ->

545 |                   PTerm -> Core (Doc IdrisDocAnn)

546 | getDocsForPTerm (PRef fc name) = getDocsForName fc name MkConfig

547 | getDocsForPTerm (PPrimVal _ c) = getDocsForPrimitive c

548 | getDocsForPTerm (PType _) = pure $ vcat

549 |   [ "Type : Type"

550 |   , indent 2 "The type of all types is Type. The type of Type is Type."

551 |   ]

552 | getDocsForPTerm (PString {}) = pure $ vcat

553 |   [ "String Literal"

554 |   , indent 2 "Desugars to a fromString call"

555 |   ]

556 | getDocsForPTerm (PList {}) = pure $ vcat

557 |   [ "List Literal"

558 |   , indent 2 "Desugars to (::) and Nil"

559 |   ]

560 | getDocsForPTerm (PSnocList {}) = pure $ vcat

561 |   [ "SnocList Literal"

562 |   , indent 2 "Desugars to (:<) and Lin"

563 |   ]

564 | getDocsForPTerm (PPair {}) = pure $ vcat

565 |   [ "Pair Literal"

566 |   , indent 2 "Desugars to MkPair or Pair"

567 |   ]

568 | getDocsForPTerm (PDPair {}) = pure $ vcat

569 |   [ "Dependant Pair Literal"

570 |   , indent 2 "Desugars to MkDPair or DPair"

571 |   ]

572 | getDocsForPTerm (PUnit _) = pure $ vcat

573 |   [ "Unit Literal"

574 |   , indent 2 "Desugars to MkUnit or Unit"

575 |   ]

576 | getDocsForPTerm (PUnquote {}) = pure $ vcat $

577 |   header "Unquotes" :: ""

578 |   :: map (indent 2) [

579 |   """

593 | getDocsForPTerm (PDelayed _ LLazy _) = pure $ vcat $

594 |   header "Laziness annotation" :: ""

595 |   :: map (indent 2) [

596 |   """

604 |   ]

605 | getDocsForPTerm (PDelayed _ LInf  _) = pure $ vcat $

606 |   header "Codata (infinite data type) annotation" :: ""

607 |   :: map (indent 2) [

608 |   """

618 |   ]

619 | getDocsForPTerm (PDelay {}) = pure $ vcat $

620 |   header "Laziness compiler primitive" :: ""

621 |   :: map (indent 2) [

622 |   """

630 |   ]

631 | getDocsForPTerm (PForce {}) = pure $ vcat $

632 |   header "Laziness compiler primitive" :: ""

633 |   :: map (indent 2) [

634 |   """

642 |   ]

643 | getDocsForPTerm pterm = pure $ "Docs not implemented for" <++> pretty0 (show pterm) <++> "yet"

646 | getDocs : {auto o : Ref ROpts REPLOpts} ->

647 |           {auto c : Ref Ctxt Defs} ->

648 |           {auto s : Ref Syn SyntaxInfo} ->

649 |           DocDirective -> Core (Doc IdrisDocAnn)

650 | getDocs (APTerm ptm) = getDocsForPTerm ptm

651 | getDocs (Symbol k) = pure $ getDocsForSymbol k

652 | getDocs (Bracket bracket) = pure $ getDocsForBracket bracket

653 | getDocs (Keyword k) = pure $ getDocsForKeyword k

654 | getDocs (AModule mod) = do

655 |   syn  <- get Syn

656 |   let Just modDoc = lookup mod (modDocstrings syn)

657 |     | _ => throw (ModuleNotFound replFC mod)

658 |   pure (pretty0 modDoc)

660 | summarise : {auto c : Ref Ctxt Defs} ->

661 |             {auto s : Ref Syn SyntaxInfo} ->

662 |             Name -> Core (Doc IdrisDocAnn)

663 | summarise n -- n is fully qualified

664 |     = do defs <- get Ctxt

665 |          Just def <- lookupCtxtExact n (gamma defs)

666 |              | _ => pure ""

667 |          ty <- prettyType Syntax (type def)

668 |          pure $ reAnnotate Syntax (prettyRig def.multiplicity)

669 |             <+> hsep [ showCategory Syntax def (prettyName n)

670 |                      , colon, hang 0 ty

671 |                      ]

675 | getContents : {auto o : Ref ROpts REPLOpts} ->

676 |               {auto c : Ref Ctxt Defs} ->

677 |               {auto s : Ref Syn SyntaxInfo} ->

678 |               Namespace -> Core (Doc IdrisDocAnn)

679 | getContents ns

680 |    = -- Get all the names, filter by any that match the given namespace

681 |      -- and are visible, then display with their type

682 |      do defs <- get Ctxt

683 |         ns <- allNames (gamma defs)

684 |         let allNs = filter inNS ns

685 |         allNs <- filterM (visible defs) allNs

686 |         vsep <$> traverse summarise (sort allNs)

687 |   where

688 |     visible : Defs -> Name -> Core Bool

689 |     visible defs n

690 |         = do Just def <- lookupCtxtExact n (gamma defs)

691 |                   | Nothing => pure False

692 |              pure (collapseDefault (visibility def) /= Private)

694 |     inNS : Name -> Bool

695 |     inNS (NS xns (UN _)) = ns `isParentOf` xns

696 |     inNS _ = False