0 | module Text.Lex.Tokenizer
  1 |
  2 | import Derive.Prelude
  3 | import Text.ParseError
  4 | import Text.Bounds
  5 | import Text.Lex.Manual
  6 |
  7 | %default total
  8 |
  9 | ||| Description of a language's tokenization rule.
 10 | public export
 11 | data Tokenizer : (errType, tokenType : Type) -> Type where
 12 |   ||| Use this for fast, direct lexing of constant tokens.
 13 |   ||| Note: It is assumed that the lexed characters do *NOT* contain
 14 |   ||| any line breaks.
 15 |   Direct : {0 e,tt : _} -> Tok True e tt -> Tokenizer e tt
 16 |
 17 |   Compose :
 18 |        {0 e, tt, tag : Type}
 19 |     -> (begin    : Tok True e (tt, tag))
 20 |     -> (middle   : Inf (tag -> Tokenizer e tt))
 21 |     -> (end      : tag -> Tok True e tt)
 22 |     -> Tokenizer e tt
 23 |
 24 |   (<|>) :
 25 |        {0 e,tt : _}
 26 |     -> Tokenizer e tt
 27 |     -> Lazy (Tokenizer e tt)
 28 |     -> Tokenizer e tt
 29 |
 30 | export
 31 | choiceMap :
 32 |      (a -> Tokenizer e tt)
 33 |   -> (as : List a)
 34 |   -> {auto 0 prf : NonEmpty as}
 35 |   -> Tokenizer e tt
 36 | choiceMap f (h :: t) = foldl (\v,e => v <|> f e) (f h) t
 37 |
 38 | export %inline
 39 | choice :
 40 |      (rs : List $ Tokenizer e tt)
 41 |   -> {auto 0 prf : NonEmpty rs}
 42 |   -> Tokenizer e tt
 43 | choice rs = choiceMap id rs
 44 |
 45 | ||| Result of running a `Tokenizer` repeatedly over a
 46 | ||| sequence of characters.
 47 | public export
 48 | record TokRes (strict : Bool) (cs : List Char) r a where
 49 |   constructor TR
 50 |   pos    : Position
 51 |   toks   : SnocList (Bounded a)
 52 |   reason : Maybe r 
 53 |   rem    : List Char
 54 |   0 suf  : Suffix strict rem cs
 55 |
 56 | wtrans : TokRes False cs r a -> (0 y : Suffix True cs xs) -> TokRes False xs r a
 57 | wtrans (TR x sx r rem z) y = TR x sx r rem (weaken $ trans z y)
 58 |
 59 | tokenise :
 60 |      {auto int : Interpolation a}
 61 |   -> (tokenizer : Tokenizer e a)
 62 |   -> Position
 63 |   -> (toks    : SnocList (Bounded a))
 64 |   -> (cs      : List Char)
 65 |   -> (0 acc   : SuffixAcc cs)
 66 |   -> TokRes False cs (Bounded $ InnerError e) a
 67 | tokenise x pos toks [] _ = TR pos toks Nothing [] Same
 68 | tokenise x pos toks cs acc@(SA r) = case next x cs acc of
 69 |   Right (TR pos2 toks2 Nothing cs2 su) =>
 70 |     tokenise x pos2 toks2 cs2 r `wtrans` su
 71 |   Left y  => TR pos toks (Just y) cs Same
 72 |   where
 73 |     next :
 74 |          Tokenizer e a
 75 |       -> (cs    : List Char)
 76 |       -> (0 acc : SuffixAcc cs)
 77 |       -> Either (Bounded $ InnerError e) (TokRes True cs Void a)
 78 |     next (Direct f) cs _ = case f cs of
 79 |       Succ val xs     @{p} =>
 80 |         let pos2 := endPos pos p
 81 |          in Right (TR pos2 (toks :< bounded val pos pos2) Nothing xs p)
 82 |       Fail start errEnd r =>
 83 |         Left $ boundedErr pos start errEnd r
 84 |     next (Compose beg midFn endFn) cs acc@(SA r) = case beg cs of
 85 |       Fail start errEnd r =>
 86 |         Left $ boundedErr pos start errEnd r
 87 |       Succ (st,tg) cs2 @{p2} =>
 88 |         let pos2   := endPos pos p2
 89 |             middle := midFn tg
 90 |             end    := endFn tg
 91 |             toks2  := toks :< bounded st pos pos2
 92 |             TR pos3 toks3 r cs3 p3 := tokenise middle pos2 toks2 cs2 r
 93 |          in case r of
 94 |               Just r@(B (Unclosed _) _) => Left r
 95 |               _                         => case end cs3 of
 96 |                 Succ val cs4 @{p4}   =>
 97 |                   let pos4   := endPos pos3 p4
 98 |                       toks4  := toks3 :< bounded val pos3 pos4
 99 |                    in Right (TR pos4 toks4 Nothing cs4 $ trans p4 (trans p3 p2))
100 |                 Fail start errEnd y => case y of
101 |                   EOI => Left $ boundedErr pos start errEnd (Unclosed "\{st}")
102 |                   r   => Left $ boundedErr pos start errEnd r
103 |     next (x <|> y) cs acc = case next x cs acc of
104 |       Right res                  => Right res
105 |       Left  r@(B (Unclosed _) _) => Left r
106 |       Left  _                    => next y cs acc
107 |
108 | ||| Given a tokenizer and an input string, return a list of recognised tokens,
109 | ||| and the line, column, and remainder of the input at the first point in the string
110 | ||| where there are no recognised tokens.
111 | export %inline
112 | lex :
113 |      {auto int : Interpolation a}
114 |   -> Tokenizer e a
115 |   -> (s : String)
116 |   -> TokRes False (unpack s) (Bounded $ InnerError e) a
117 | lex x s = tokenise x begin [<] (unpack s) suffixAcc
118 |