Bikeshedding.idr

module Text.Lexer.Bikeshedding

{-
Other choices include:

-:, $:
!=>, $=>
:>, :$>
#^, *! -- not really

the possibilities are endless
-}
infix 0 !:, $:


{-
I'm unsatisfied with this name, because this would also be useful for identifier tokens.
-}
||| A `Literal` represents a `Lexer` and a way to produce a value of
||| type `a` based on the text it recognises.
public export
Literal : (a : Type) -> Type
Literal a = (Lexer, String -> a)

||| Make a `TokenMap tok` entry for a `Lexer` that always results in the
||| same token value.
|||
||| ```idris example
||| data MyToken = MTComma | MTColon
||| 
||| myMap : TokenMap MyToken
||| myMap = [ is ',' !: MTComma
|||         , is ':' !: MTColon
|||         ]
||| ```
(!:) : Lexer -> tok -> (Lexer, String -> tok)
(!:) l t = (l, const t)

||| Create a `TokenMap tok` entry from a `Literal a` and a function
||| that can create a `tok` from an `a`.
|||
||| ```idris example
||| data MyToken = MTInt Int | MTBool Bool
||| 
||| bool : Literal Bool
||| bool = (exact "True" <|> exact "False", (== "True"))
||| 
||| myMap : TokenMap MyToken
||| myMap = [ (intLit, cast) $: MTInt
|||         , bool           $: MTBool
|||         ]
||| ```
($:) : Literal a -> (a -> tok) -> (Lexer, String -> tok)
($:) (l, mkVal) mkTok = (l, mkTok . mkVal)

Hm, maybe it wouldn't be all that useful for identifier tokens.

name : Lexer
name
  = let initial = is '_' <|> alpha
       subsequent = is '_' <|> is '\'' <|> alphaNum in
       initlal <+> many subsequent

data MyToken
  = MTIdent String
  | MTOperator String
  | MTComma
  | MTInteger Integer

myTokenMap : TokenMap MyToken
myTokenMap
  = [ is ',' !: MTComma
    , (intLit, cast) $: MTInteger
    , (name, MTIdent)
    , (symbols, MTOperator)
    ]

Or potentially:

-- allows a Lexer to be used with `$:`
implicit
idLiteral : Lexer -> Literal String
idLiteral l = (l, id)