
   0 | module Idris.Pretty.Annotations
   1 | 
   2 | import Algebra
   3 | import Data.String
   4 | import Core.Name
   5 | import Libraries.Text.PrettyPrint.Prettyprinter
   6 | 
   7 | %default total
   8 | 
   9 | public export
  10 | data IdrisSyntax
  11 |   = Hole
  12 |   | TCon (Maybe Name) -- these may be primitive types
  13 |   | DCon (Maybe Name) -- these may be primitive constructors
  14 |   | Fun  Name
  15 |   | Bound
  16 |   | Keyword
  17 |   | Pragma
  18 | 
  19 | export
  20 | keyword : Doc IdrisSyntax -> Doc IdrisSyntax
  21 | keyword = annotate Keyword
  22 | 
  23 | export
  24 | hole : Doc IdrisSyntax -> Doc IdrisSyntax
  25 | hole = annotate Hole
  26 | 
  27 | export
  28 | let_ : Doc IdrisSyntax
  29 | let_ = keyword "let"
  30 | 
  31 | export
  32 | in_ : Doc IdrisSyntax
  33 | in_ = keyword "in"
  34 | 
  35 | export
  36 | case_ : Doc IdrisSyntax
  37 | case_ = keyword "case"
  38 | 
  39 | export
  40 | of_ : Doc IdrisSyntax
  41 | of_ = keyword "of"
  42 | 
  43 | export
  44 | lcurly : Doc IdrisSyntax
  45 | lcurly = keyword "{"
  46 | 
  47 | export
  48 | semi : Doc IdrisSyntax
  49 | semi = keyword ";"
  50 | 
  51 | export
  52 | equals : Doc IdrisSyntax
  53 | equals = keyword "="
  54 | 
  55 | export
  56 | arrow : Doc IdrisSyntax
  57 | arrow = keyword "->"
  58 | 
  59 | export
  60 | fatArrow : Doc IdrisSyntax
  61 | fatArrow = keyword "=>"
  62 | 
  63 | export
  64 | rcurly : Doc IdrisSyntax
  65 | rcurly = keyword "}"
  66 | 
  67 | export
  68 | do_ : Doc IdrisSyntax
  69 | do_ = keyword "do"
  70 | 
  71 | export
  72 | with_ : Doc IdrisSyntax
  73 | with_ = keyword "with"
  74 | 
  75 | export
  76 | record_ : Doc IdrisSyntax
  77 | record_ = keyword "record"
  78 | 
  79 | export
  80 | impossible_ : Doc IdrisSyntax
  81 | impossible_ = keyword "impossible"
  82 | 
  83 | export
  84 | forall_ : Doc IdrisSyntax
  85 | forall_ = keyword "forall"
  86 | 
  87 | export
  88 | auto_ : Doc IdrisSyntax
  89 | auto_ = keyword "auto"
  90 | 
  91 | export
  92 | default_ : Doc IdrisSyntax
  93 | default_ = keyword "default"
  94 | 
  95 | export
  96 | rewrite_ : Doc IdrisSyntax
  97 | rewrite_ = keyword "rewrite"
  98 | 
  99 | export
 100 | pragma : Doc IdrisSyntax -> Doc IdrisSyntax
 101 | pragma = annotate Pragma
 102 | 
 103 | export
 104 | prettyRig : RigCount -> Doc IdrisSyntax
 105 | prettyRig = elimSemi (keyword (pretty0 '0') <+> space)
 106 |                      (keyword (pretty0 '1') <+> space)
 107 |                      (const emptyDoc)
 108 |