(** Token definition for lexing. *)

open Support

(** Tokens *)
type t =
  (* Symbols *)
  | LPAREN  (** [(] *)
  | HASH_LPAREN  (** [#(] *)
  | DOLLAR_LPAREN  (** [$(] *)
  | RPAREN  (** [)] *)
  | LBRACK  (** [\[] *)
  | HASH_LBRACK  (** [#\[] *)
  | DOLLAR_LBRACK  (** [$\[] *)
  | RBRACK  (** [\]] *)
  | LBRACE  (** [{] *)
  | RBRACE  (** [}] *)
  | LANGLE  (** [<] *)
  | RANGLE  (** [>] *)
  | COMMA  (** [,] *)
  | DOUBLE_COLON  (** [::] *)
  | COLON  (** [:] *)
  | SEMICOLON  (** [;] *)
  | PIPE  (** [|] *)
  | TURNSTILE  (** [|-] *)
  | TURNSTILE_HASH  (** [|-#] *)
  | DOTS  (** [..] *)
  | BACKARROW  (** [<-] *)
  | ARROW  (** [->] *)
  | THICK_ARROW  (** [=>] *)
  | HAT  (** [^] *)
  | DOT  (** [.] *)
  | LAMBDA  (** [\ ] *)
  | STAR  (** [*] *)
  | EQUALS  (** [=] *)
  | SLASH  (** [/] *)
  | UNDERSCORE  (** [_] *)
  | HASH  (** [#] *)
  | DOLLAR  (** [$] *)
  | PLUS  (** [+] *)
  (* Keywords *)
  | KW_AND  (** [and] *)
  | KW_BLOCK  (** [block] *)
  | KW_CASE  (** [case] *)
  | KW_IF  (** [if] *)
  | KW_THEN  (** [then]*)
  | KW_ELSE  (** [else] *)
  | KW_IMPOSSIBLE  (** [impossible] *)
  | KW_LET  (** [let] *)
  | KW_IN  (** [in] *)
  | KW_OF  (** [of] *)
  | KW_REC  (** [rec] *)
  | KW_SCHEMA  (** [schema] *)
  | KW_SOME  (** [some] *)
  | KW_FN  (** [fn] *)
  | KW_MLAM  (** [mlam] *)
  | KW_MODULE  (** [module] *)
  | KW_STRUCT  (** [struct] *)
  | KW_END  (** [end] *)
  | KW_TOTAL  (** [total] *)
  | KW_TRUST  (** [trust] *)
  | KW_TYPE  (** [type] *)
  | KW_CTYPE  (** [ctype] *)
  | KW_PROP  (** [prop] *)
  | KW_INDUCTIVE  (** [inductive] *)
  | KW_COINDUCTIVE  (** [coinductive] *)
  | KW_STRATIFIED  (** [stratified] *)
  | KW_LF  (** [LF] *)
  | KW_FUN  (** [fun] *)
  | KW_TYPEDEF  (** [typedef] *)
  | KW_PROOF  (** [proof] *)
  | KW_BY  (** [by] *)
  | KW_AS  (** [as] *)
  | KW_SUFFICES  (** [suffices] *)
  | KW_TOSHOW  (** [toshow] *)
  | STRING of string
      (** [STRING s] is a string literal ["\"" ^ String.escaped s ^ "\""]. *)
  | IDENT of string
      (** [IDENT x] is an identifier [x] that may represent an operator, a
          variable, etc.. *)
  | PRAGMA of string  (** [PRAGMA p] is [--p]. *)
  | DOT_IDENT of string  (** [DOT_IDENT x] is a dot followed by [x]. *)
  | DOT_INTLIT of int  (** [DOT_INTLIT n] is a dot followed by [n]. *)
  | HASH_IDENT of string
      (** [HASH_IDENT x] is [x] where [x] starts with [#]. *)
  | DOLLAR_IDENT of string
      (** [DOLLAR_IDENT x] is [x] where [x] starts with [$]. *)
  | HASH_BLANK  (** [#_] *)
  | DOLLAR_BLANK  (** [$_] *)
  | HOLE of string option  (** [HOLE x] is [?x]. *)
  | INTLIT of int  (** [INTLIT i] is the integer literal [i]. *)
  | BLOCK_COMMENT of string  (** A block comment of the form [%{{ ... }}%] *)

(** {1 Instances} *)

include Eq.EQ with type t := t

include Show.SHOW with type t := t
