0 | module Idris.Doc.Display
 1 |
 2 | import Core.Env
 3 |
 4 | import Idris.IDEMode.Holes
 5 |
 6 | import Idris.Pretty
 7 | import Idris.Resugar
 8 | import Idris.Syntax
 9 | import Idris.Syntax.Views
10 |
11 | %hide Symbols.equals
12 |
13 | %default covering
14 |
15 | export
16 | displayType : {auto c : Ref Ctxt Defs} ->
17 |               {auto s : Ref Syn SyntaxInfo} ->
18 |               (shortName : Bool) -> Defs -> (Name, Int, GlobalDef) ->
19 |               Core (Doc IdrisSyntax)
20 | displayType shortName defs (n, i, gdef)
21 |   = maybe (do tm <- resugar Env.empty !(normaliseHoles defs Env.empty (type gdef))
22 |               nm <- aliasName (fullname gdef)
23 |               let nm = ifThenElse shortName (dropNS nm) nm
24 |               let prig = prettyRig gdef.multiplicity
25 |               let ann = showCategory id gdef
26 |               pure (prig <+> ann (cast $ prettyOp True nm) <++> colon <++> pretty tm))
27 |           (\num => prettyHole defs Env.empty n num (type gdef))
28 |           (isHole gdef)
29 | export
30 | displayTerm : {auto c : Ref Ctxt Defs} ->
31 |               {auto s : Ref Syn SyntaxInfo} ->
32 |               Defs -> ClosedTerm ->
33 |               Core (Doc IdrisSyntax)
34 | displayTerm defs tm
35 |   = do ptm <- resugar Env.empty !(normaliseHoles defs Env.empty tm)
36 |        pure (pretty ptm)
37 |
38 | export
39 | displayClause : {auto c : Ref Ctxt Defs} ->
40 |                 {auto s : Ref Syn SyntaxInfo} ->
41 |                 Defs -> (vs ** (Env Term vs, Term vs, Term vs)) ->
42 |                 Core (Doc IdrisSyntax)
43 | displayClause defs (vs ** (env, lhs, rhs))
44 |   = do lhstm <- resugar env !(normaliseHoles defs env lhs)
45 |        rhstm <- resugar env !(normaliseHoles defs env rhs)
46 |        pure (prettyLHS lhstm <++> equals <++> pretty rhstm)
47 |
48 |   where
49 |     prettyLHS : IPTerm -> Doc IdrisSyntax
50 |     prettyLHS (PRef _ op) = cast $ prettyOp True op.rawName
51 |     prettyLHS t = pretty t
52 |
53 | export
54 | displayPats : {auto c : Ref Ctxt Defs} ->
55 |               {auto s : Ref Syn SyntaxInfo} ->
56 |               (shortName : Bool) -> Defs -> (Name, Int, GlobalDef) ->
57 |               Core (Doc IdrisSyntax)
58 | displayPats shortName defs (n, idx, gdef)
59 |   = case definition gdef of
60 |       PMDef _ _ _ _ pats =>
61 |         do ty <- displayType shortName defs (n, idx, gdef)
62 |            ps <- traverse (displayClause defs) pats
63 |            pure (vsep (ty :: ps))
64 |       _ => pure (pretty0 n <++> reflow "is not a pattern matching definition")
65 |
66 | export
67 | displayImpl : {auto c : Ref Ctxt Defs} ->
68 |               {auto s : Ref Syn SyntaxInfo} ->
69 |               Defs -> (Name, Int, GlobalDef) ->
70 |               Core (Doc IdrisSyntax)
71 | displayImpl defs (n, idx, gdef)
72 |   = case definition gdef of
73 |       PMDef _ _ ct _ [(vars ** (env,  _, rhs))] =>
74 |         do rhstm <- resugar env !(normaliseHoles defs env rhs)
75 |            let (_, args) = getFnArgs defaultKindedName rhstm
76 |            defs <- get Ctxt
77 |            pds <- map catMaybes $ for args $ \ arg => do
78 |              let (_, expr) = underLams (unArg arg)
79 |              let (PRef _ kn, _) = getFnArgs defaultKindedName expr
80 |                | _ => pure Nothing
81 |              log "doc.implementation" 20 $ "Got name \{show @{Raw} kn}"
82 |              let (ns, DN dn nm) = splitNS (kn.fullName)
83 |                | _ => do log "doc.implementation" 10 $ "Invalid name \{show @{Raw} kn}"
84 |                          pure Nothing
85 |              let nm = NS ns nm
86 |              Just (idx, gdef) <- lookupCtxtExactI kn.fullName (gamma defs)
87 |                | _ => do log "doc.implementation" 10 $ "Couldn't find \{show @{Raw} nm}"
88 |                          pure Nothing
89 |              pdef <- displayPats True defs (nm, idx, gdef)
90 |              pure (Just pdef)
91 |            pure (vcat $ intersperse "" pds)
92 |       _ => pure (pretty0 n <++> reflow "is not an implementation definition")
93 |