
   0 | module Parser.Lexer.Package
   1 | 
   2 | import public Parser.Lexer.Common
   3 | import public Libraries.Text.Lexer
   4 | import public Libraries.Text.Parser
   5 | import public Libraries.Text.Bounded
   6 | import Libraries.Text.PrettyPrint.Prettyprinter
   7 | 
   8 | import Data.String
   9 | import Libraries.Data.String.Extra
  10 | import Libraries.Utils.String
  11 | 
  12 | import Core.Name.Namespace
  13 | 
  14 | %default total
  15 | 
  16 | public export
  17 | data Token
  18 |   = Comment String
  19 |   | EndOfInput
  20 |   | Equals
  21 |   | DotSepIdent (Maybe Namespace) String
  22 |   | Separator
  23 |   | Dot
  24 |   | LTE
  25 |   | GTE
  26 |   | LT
  27 |   | GT
  28 |   | EqOp
  29 |   | AndOp
  30 |   | Space
  31 |   | StringLit String
  32 |   | IntegerLit Integer
  33 | 
  34 | public export
  35 | Show Token where
  36 |   show (Comment str) = "Comment: " ++ str
  37 |   show EndOfInput = "EndOfInput"
  38 |   show Equals = "Equals"
  39 |   show (DotSepIdent ns n) = "DotSepIdentifier: " ++ show ns ++ "." ++ show n
  40 |   show Separator = "Separator"
  41 |   show Dot = "Dot"
  42 |   show LTE = "LTE"
  43 |   show GTE = "GTE"
  44 |   show LT = "LT"
  45 |   show GT = "GT"
  46 |   show EqOp = "EqOp"
  47 |   show AndOp = "AndOp"
  48 |   show Space = "Space"
  49 |   show (StringLit s) = "StringLit: " ++ s
  50 |   show (IntegerLit i) = "IntegerLit: " ++ show i
  51 | 
  52 | public export
  53 | Pretty Void Token where
  54 |   pretty (Comment str) = "Comment:" <++> pretty str
  55 |   pretty EndOfInput = "EndOfInput"
  56 |   pretty Equals = "Equals"
  57 |   pretty (DotSepIdent ns n) = "DotSepIdentifier:" <++> prettyMaybe ns <+> dot <+> pretty n
  58 |   pretty Separator = "Separator"
  59 |   pretty Dot = "Dot"
  60 |   pretty LTE = "LTE"
  61 |   pretty GTE = "GTE"
  62 |   pretty LT = "LT"
  63 |   pretty GT = "GT"
  64 |   pretty EqOp = "EqOp"
  65 |   pretty AndOp = "AndOp"
  66 |   pretty Space = "Space"
  67 |   pretty (StringLit s) = "StringLit:" <++> pretty s
  68 |   pretty (IntegerLit i) = "IntegerLit:" <++> byShow i
  69 | 
  70 | equals : Lexer
  71 | equals = is '='
  72 | 
  73 | separator : Lexer
  74 | separator = is ','
  75 | 
  76 | dot : Lexer
  77 | dot = is '.'
  78 | 
  79 | lte : Lexer
  80 | lte = is '<' <+> is '='
  81 | 
  82 | gte : Lexer
  83 | gte = is '>' <+> is '='
  84 | 
  85 | lt : Lexer
  86 | lt = is '<'
  87 | 
  88 | gt : Lexer
  89 | gt = is '>'
  90 | 
  91 | eqop : Lexer
  92 | eqop = is '=' <+> is '='
  93 | 
  94 | andop : Lexer
  95 | andop = is '&' <+> is '&'
  96 | 
  97 | rawTokens : TokenMap Token
  98 | rawTokens =
  99 |   [ (comment, Comment . drop 2)
 100 |   , (blockComment, Comment . shrink 2)
 101 |   , (identAllowDashes <+> reject dot, DotSepIdent Nothing)
 102 |   , (namespacedIdent, uncurry DotSepIdent . mkNamespacedIdent)
 103 |   , (separator, const Separator)
 104 |   , (dot, const Dot)
 105 |   , (lte, const LTE)
 106 |   , (gte, const GTE)
 107 |   , (lt, const LT)
 108 |   , (gt, const GT)
 109 |   , (eqop, const EqOp)
 110 |   , (andop, const AndOp)
 111 |   , (equals, const Equals)
 112 |   , (spacesOrNewlines, const Space)
 113 |   , (stringLit, \s => StringLit (stripQuotes s))
 114 |   , (intLit, \i => IntegerLit (cast i))
 115 |   ]
 116 | 
 117 | export
 118 | lex : String -> Either (Int, Int, String) (List (WithBounds Token))
 119 | lex str =
 120 |   case lex rawTokens str of
 121 |        (tokenData, (l, c, "")) =>
 122 |          Right $ (filter (useful . val) tokenData)
 123 |           ++ [MkBounded EndOfInput False (MkBounds l c l c)]
 124 |        (_, fail) => Left fail
 125 |   where
 126 |     useful : Token -> Bool
 127 |     useful (Comment c) = False
 128 |     useful Space       = False
 129 |     useful _ = True
 130 |