0 | module Core.Context.Pretty
  1 |
  2 | import Core.Env
  3 |
  4 | import Data.String
  5 | import Idris.Doc.Annotations
  6 |
  7 | import Idris.Syntax
  8 | import Idris.Pretty
  9 |
 10 | import Core.Case.CaseTree.Pretty
 11 |
 12 | import Libraries.Data.NatSet
 13 |
 14 | %hide Env.(::)
 15 | %hide Env.Nil
 16 | %hide String.(::)
 17 | %hide String.Nil
 18 | %hide Doc.Nil
 19 | %hide Subst.(::)
 20 | %hide Subst.Nil
 21 | %hide CList.(::)
 22 | %hide CList.Nil
 23 | %hide Stream.(::)
 24 | %hide Symbols.equals
 25 | %hide String.indent
 26 | %hide List1.(++)
 27 | -- %hide SnocList.(++)
 28 | %hide String.(++)
 29 | %hide Pretty.Syntax
 30 | %hide List1.forget
 31 |
 32 | %default covering
 33 |
 34 | namespace Raw
 35 |   export
 36 |   prettyDef : Def -> Doc IdrisDocAnn
 37 |   prettyDef None = "undefined"
 38 |   prettyDef (PMDef _ args ct _ pats) =
 39 |        let ct = prettyTree ct in
 40 |        vcat
 41 |         [ "Arguments" <++> cast (prettyList $ toList args)
 42 |         , header "Compile time tree" <++> reAnnotate Syntax ct
 43 |         ]
 44 |   prettyDef (DCon tag arity nt) =
 45 |       vcat $ header "Data constructor" :: map (indent 2)
 46 |           ([ "tag:" <++> byShow tag
 47 |            , "arity:" <++> byShow arity
 48 |            ] ++ maybe [] (\ n => ["newtype by:" <++> byShow n]) nt)
 49 |   prettyDef (TCon arity ps ds u ms cons det) =
 50 |         let enum = hsep . punctuate "," in
 51 |         vcat $ header "Type constructor" :: map (indent 2)
 52 |           ([ "arity:" <++> byShow arity
 53 |            , "parameter positions:" <++> byShow ps
 54 |            , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> fromMaybe [] cons)
 55 |            ] ++ (("mutual with:" <++> enum (pretty0 <$> ms)) <$ guard (not $ null ms))
 56 |              ++ (maybe [] (\ pos => ["detaggable by:" <++> byShow pos]) det))
 57 |   prettyDef (ExternDef arity) =
 58 |       vcat $ header "External definition" :: map (indent 2)
 59 |            [ "arity:" <++> byShow arity ]
 60 |   prettyDef (ForeignDef arity calls) =
 61 |      vcat $ header "Foreign definition" :: map (indent 2)
 62 |           [ "arity:" <++> byShow arity
 63 |           , "bindings:" <++> byShow calls ]
 64 |   prettyDef (Builtin {arity} _) =
 65 |         vcat $ header "Builtin" :: map (indent 2)
 66 |           [ "arity:" <++> byShow arity ]
 67 |   prettyDef (Hole numlocs hf) =
 68 |         vcat $ header "Hole" :: map (indent 2)
 69 |           ("Implicitly bound name" <$ guard (implbind hf))
 70 |   prettyDef (BySearch rig depth def) =
 71 |         vcat $ header "Search" :: map (indent 2)
 72 |           [ "depth:" <++> byShow depth
 73 |           , "in:" <++> pretty0 def ]
 74 |   prettyDef (Guess tm _ cs) =
 75 |         vcat $ header "Guess" :: map (indent 2)
 76 |           [ "solution:" <++> byShow tm
 77 |           , "when:" <++> byShow cs ]
 78 |   prettyDef (UniverseLevel i) = "Universe level #" <+> byShow i
 79 |   prettyDef ImpBind = "Bound name"
 80 |   prettyDef Delayed = "Delayed"
 81 |
 82 | namespace Resugared
 83 |
 84 |   export
 85 |   prettyDef : {auto c : Ref Ctxt Defs} ->
 86 |               {auto s : Ref Syn SyntaxInfo} ->
 87 |               Def -> Core (Doc IdrisDocAnn)
 88 |   prettyDef None = pure "undefined"
 89 |   prettyDef (PMDef _ args ct _ pats) = do
 90 |       ct <- prettyTree (mkEnv emptyFC _) ct
 91 |       pure $ vcat
 92 |         [ "Arguments" <++> cast (prettyList $ toList args)
 93 |         , header "Compile time tree" <++> reAnnotate Syntax ct
 94 |         ]
 95 |   prettyDef (DCon tag arity nt) = pure $
 96 |       vcat $ header "Data constructor" :: map (indent 2)
 97 |           ([ "tag:" <++> byShow tag
 98 |            , "arity:" <++> byShow arity
 99 |            ] ++ maybe [] (\ n => ["newtype by:" <++> byShow n]) nt)
100 |   prettyDef (TCon arity ps ds u ms cons det) = pure $
101 |         let enum = hsep . punctuate "," in
102 |         vcat $ header "Type constructor" :: map (indent 2)
103 |           ([ "arity:" <++> byShow arity
104 |            , "parameter positions:" <++> byShow ps
105 |            , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> fromMaybe [] cons)
106 |            ] ++ (("mutual with:" <++> enum (pretty0 <$> ms)) <$ guard (not $ null ms))
107 |              ++ (maybe [] (\ pos => ["detaggable by:" <++> byShow pos]) det))
108 |   prettyDef (ExternDef arity) = pure $
109 |       vcat $ header "External definition" :: map (indent 2)
110 |            [ "arity:" <++> byShow arity ]
111 |   prettyDef (ForeignDef arity calls) = pure $
112 |      vcat $ header "Foreign definition" :: map (indent 2)
113 |           [ "arity:" <++> byShow arity
114 |           , "bindings:" <++> byShow calls ]
115 |   prettyDef (Builtin {arity} _) = pure $
116 |         vcat $ header "Builtin" :: map (indent 2)
117 |           [ "arity:" <++> byShow arity ]
118 |   prettyDef (Hole numlocs hf) = pure $
119 |         vcat $ header "Hole" :: map (indent 2)
120 |           ("Implicitly bound name" <$ guard (implbind hf))
121 |   prettyDef (BySearch rig depth def) = pure $
122 |         vcat $ header "Search" :: map (indent 2)
123 |           [ "depth:" <++> byShow depth
124 |           , "in:" <++> pretty0 def ]
125 |   prettyDef (Guess tm _ cs) = pure $
126 |         vcat $ header "Guess" :: map (indent 2)
127 |           [ "solution:" <++> byShow tm
128 |           , "when:" <++> byShow cs ]
129 |   prettyDef (UniverseLevel i) = pure $ "Universe level #" <+> byShow i
130 |   prettyDef ImpBind = pure "Bound name"
131 |   prettyDef Delayed = pure "Delayed"
132 |