
   0 | module Text.WebIDL.Lexer
   1 | 
   2 | import Text.Bounds
   3 | import Text.Lex.Manual
   4 | import Text.WebIDL.Types
   5 | 
   6 | %default total
   7 | 
   8 | --------------------------------------------------------------------------------
   9 | --          Noise
  10 | --------------------------------------------------------------------------------
  11 | 
  12 | keep : IdlToken -> Bool
  13 | keep Comment = False
  14 | keep Space   = False
  15 | keep _       = True
  16 | 
  17 | spaces : AutoTok e IdlToken
  18 | spaces ('\n' :: xs) = spaces xs
  19 | spaces ('\r' :: xs) = spaces xs
  20 | spaces ('\t' :: xs) = spaces xs
  21 | spaces (' ' :: xs)  = spaces xs
  22 | spaces xs           = Succ Space xs
  23 | 
  24 | comment : AutoTok e IdlToken
  25 | comment ('\n' :: xs) = Succ Comment ('\n' :: xs)
  26 | comment (x :: xs)    = comment xs
  27 | comment []           = Succ Comment []
  28 | 
  29 | mlComment : AutoTok e IdlToken
  30 | mlComment ('*' :: '/' :: xs) = Succ Comment xs
  31 | mlComment (x :: xs)          = mlComment xs
  32 | mlComment []                 = eoiAt p
  33 | 
  34 | string : SnocList Char -> AutoTok e IdlToken
  35 | string sc ('"' :: xs) = Succ (SLit $ MkStrLit $ cast sc) xs
  36 | string sc (x :: xs)   = string (sc :< x)  xs
  37 | string _  []          = eoiAt p
  38 | 
  39 | -- Takes a valid identifier and converts it either
  40 | -- to a FloatLit, a Keyword, or an Identifier
  41 | toIdent : String -> IdlToken
  42 | toIdent "Infinity"  = FLit Infinity
  43 | toIdent "-Infinity" = FLit NegativeInfinity
  44 | toIdent "NaN"       = FLit NaN
  45 | toIdent s           = maybe (Ident $ MkIdent s) Key (refineKeyword s)
  46 | 
  47 | ident : SnocList Char -> AutoTok e IdlToken
  48 | ident sc ('-' :: xs) = ident (sc :< '-') xs
  49 | ident sc ('_' :: xs) = ident (sc :< '_') xs
  50 | ident sc (x   :: xs) =
  51 |   if isAlphaNum x then ident (sc :< x) xs else Succ (toIdent $ cast sc) (x::xs)
  52 | ident sc  []         = Succ (toIdent $ cast sc) []
  53 | 
  54 | --------------------------------------------------------------------------------
  55 | --          Numbers
  56 | --------------------------------------------------------------------------------
  57 | 
  58 | toInt : Signum -> Nat -> Integer
  59 | toInt Plus  n = cast n
  60 | toInt Minus n = negate $ cast n
  61 | 
  62 | toNum : Integer -> Maybe Nat -> Maybe Integer -> IdlToken
  63 | toNum i Nothing Nothing   = ILit $ I i
  64 | toNum i mn      (Just ex) = FLit $ Exp i mn ex
  65 | toNum i (Just ad) Nothing = FLit $ NoExp i ad
  66 | 
  67 | exp : Integer -> Maybe Nat -> AutoTok e IdlToken
  68 | exp i mn (x :: xs) =
  69 |   if toLower x == 'e' then toNum i mn . Just <$> autoTok intPlus xs
  70 |   else Succ (toNum i mn Nothing) (x::xs)
  71 | exp i mn []        = Succ (toNum i mn Nothing) []
  72 | 
  73 | dot : Integer -> Nat -> AutoTok e IdlToken
  74 | dot i n (x :: xs) =
  75 |   if isDigit x then dot i (10*n + digit x) xs else exp i (Just n) (x::xs)
  76 | dot i n []        = Succ (toNum i (Just n) Nothing) []
  77 | 
  78 | rest : Integer -> AutoTok e IdlToken
  79 | rest i ('.'::x::xs) = if isDigit x then dot i (digit x) xs else unknownRange p xs
  80 | rest i ('.'::[])    = unknown p
  81 | rest i xs           = exp i Nothing xs
  82 | 
  83 | num : Signum -> Nat -> AutoTok e IdlToken
  84 | num s n (x :: xs) =
  85 |   if isDigit x then num s (n*10 + digit x) xs else rest (toInt s n) (x::xs)
  86 | num s n []        = Succ (ILit $ I $ toInt s n) []
  87 | 
  88 | --------------------------------------------------------------------------------
  89 | --          Numbers
  90 | --------------------------------------------------------------------------------
  91 | 
  92 | isFloat : List Char -> Bool
  93 | isFloat ('.' :: _) = True
  94 | isFloat ('e' :: _) = True
  95 | isFloat ('E' :: _) = True
  96 | isFloat _          = False
  97 | 
  98 | term : Tok True e IdlToken
  99 | term ('"':: xs) = string [<] xs
 100 | term ('/'::'/':: xs) = comment xs
 101 | term ('/'::'*':: xs) = mlComment xs
 102 | term ('0'::'x':: xs) = ILit . Hex <$> hex xs
 103 | term ('0'::'X':: xs) = ILit . Hex <$> hex xs
 104 | term ('0'::xs)       =
 105 |   if isFloat xs then rest 0 xs else ILit . Oct <$> oct ('0'::xs)
 106 | term ('.'::'.'::'.'::xs) = Succ (Other Ellipsis) xs
 107 | term ('_':: x::xs)   =
 108 |   if isAlpha x then ident [<'_',x] xs
 109 |   else Succ (Other $ Symb '_') (x::xs)
 110 | term ('-':: x::xs)   =
 111 |   if isAlpha x then ident [<'-',x] xs
 112 |   else if isDigit x then num Minus (digit x) xs
 113 |   else Succ (Other $ Symb '-') (x::xs)
 114 | term (x::xs)         =
 115 |   if      isAlpha x then ident [<x] xs
 116 |   else if isDigit x then num Plus (digit x) xs
 117 |   else if isSpace x then spaces xs
 118 |   else Succ (Other $ Symb x) xs
 119 | term [] = eoiAt Same
 120 | 
 121 | public export
 122 | 0 ParseErr : Type
 123 | ParseErr = InnerError IdlError
 124 | 
 125 | go :
 126 |      SnocList (Bounded IdlToken)
 127 |  -> (pos   : Position)
 128 |  -> (cs    : List Char)
 129 |  -> (0 acc : SuffixAcc cs)
 130 |  -> Either (Bounded ParseErr) (List (Bounded IdlToken))
 131 | go sx _ []    _     = Right (sx <>> [])
 132 | go sx pos xs (SA r) = case term xs of
 133 |   Succ t xs' @{prf} =>
 134 |     let pos2 := endPos pos prf
 135 |         sx'  := if keep t then (sx :< bounded t pos pos2) else sx
 136 |      in go sx' pos2 xs' r
 137 |   Fail start errEnd r => Left $ boundedErr pos start errEnd r
 138 | 
 139 | ||| Generates a list of IdlTokens
 140 | ||| from an input string, removing unnecessary tokens by
 141 | ||| means of `isNoise`.
 142 | export %inline
 143 | lexIdl : String -> Either (Bounded ParseErr) (List $ Bounded IdlToken)
 144 | lexIdl s = go [<] begin (unpack s) suffixAcc
 145 |