Module Beluga_parser.Token

Token definition for lexing.

type t =
  1. | LPAREN
    (*

    (

    *)
  2. | HASH_LPAREN
    (*

    #(

    *)
  3. | DOLLAR_LPAREN
    (*

    $(

    *)
  4. | RPAREN
    (*

    )

    *)
  5. | LBRACK
    (*

    [

    *)
  6. | HASH_LBRACK
    (*

    #[

    *)
  7. | DOLLAR_LBRACK
    (*

    $[

    *)
  8. | RBRACK
    (*

    ]

    *)
  9. | LBRACE
    (*

    {

    *)
  10. | RBRACE
    (*

    }

    *)
  11. | LANGLE
    (*

    <

    *)
  12. | RANGLE
    (*

    >

    *)
  13. | COMMA
    (*

    ,

    *)
  14. | DOUBLE_COLON
    (*

    ::

    *)
  15. | COLON
    (*

    :

    *)
  16. | SEMICOLON
    (*

    ;

    *)
  17. | PIPE
    (*

    |

    *)
  18. | TURNSTILE
    (*

    |-

    *)
  19. | TURNSTILE_HASH
    (*

    |-#

    *)
  20. | DOTS
    (*

    ..

    *)
  21. | BACKARROW
    (*

    <-

    *)
  22. | ARROW
    (*

    ->

    *)
  23. | THICK_ARROW
    (*

    =>

    *)
  24. | HAT
    (*

    ^

    *)
  25. | DOT
    (*

    .

    *)
  26. | LAMBDA
    (*

    \

    *)
  27. | STAR
    (*

    *

    *)
  28. | EQUALS
    (*

    =

    *)
  29. | SLASH
    (*

    /

    *)
  30. | UNDERSCORE
    (*

    _

    *)
  31. | HASH
    (*

    #

    *)
  32. | DOLLAR
    (*

    $

    *)
  33. | PLUS
    (*

    +

    *)
  34. | KW_AND
    (*

    and

    *)
  35. | KW_BLOCK
    (*

    block

    *)
  36. | KW_CASE
    (*

    case

    *)
  37. | KW_IF
    (*

    if

    *)
  38. | KW_THEN
    (*

    then

    *)
  39. | KW_ELSE
    (*

    else

    *)
  40. | KW_IMPOSSIBLE
    (*

    impossible

    *)
  41. | KW_LET
    (*

    let

    *)
  42. | KW_IN
    (*

    in

    *)
  43. | KW_OF
    (*

    of

    *)
  44. | KW_REC
    (*

    rec

    *)
  45. | KW_SCHEMA
    (*

    schema

    *)
  46. | KW_SOME
    (*

    some

    *)
  47. | KW_FN
    (*

    fn

    *)
  48. | KW_MLAM
    (*

    mlam

    *)
  49. | KW_MODULE
    (*

    module

    *)
  50. | KW_STRUCT
    (*

    struct

    *)
  51. | KW_END
    (*

    end

    *)
  52. | KW_TOTAL
    (*

    total

    *)
  53. | KW_TRUST
    (*

    trust

    *)
  54. | KW_TYPE
    (*

    type

    *)
  55. | KW_CTYPE
    (*

    ctype

    *)
  56. | KW_PROP
    (*

    prop

    *)
  57. | KW_INDUCTIVE
    (*

    inductive

    *)
  58. | KW_COINDUCTIVE
    (*

    coinductive

    *)
  59. | KW_STRATIFIED
    (*

    stratified

    *)
  60. | KW_LF
    (*

    LF

    *)
  61. | KW_FUN
    (*

    fun

    *)
  62. | KW_TYPEDEF
    (*

    typedef

    *)
  63. | KW_PROOF
    (*

    proof

    *)
  64. | KW_BY
    (*

    by

    *)
  65. | KW_AS
    (*

    as

    *)
  66. | KW_SUFFICES
    (*

    suffices

    *)
  67. | KW_TOSHOW
    (*

    toshow

    *)
  68. | STRING of string
    (*

    STRING s is a string literal "\"" ^ String.escaped s ^ "\"".

    *)
  69. | IDENT of string
    (*

    IDENT x is an identifier x that may represent an operator, a variable, etc..

    *)
  70. | PRAGMA of string
    (*

    PRAGMA p is --p.

    *)
  71. | DOT_IDENT of string
    (*

    DOT_IDENT x is a dot followed by x.

    *)
  72. | DOT_INTLIT of int
    (*

    DOT_INTLIT n is a dot followed by n.

    *)
  73. | HASH_IDENT of string
    (*

    HASH_IDENT x is x where x starts with #.

    *)
  74. | DOLLAR_IDENT of string
    (*

    DOLLAR_IDENT x is x where x starts with $.

    *)
  75. | HASH_BLANK
    (*

    #_

    *)
  76. | DOLLAR_BLANK
    (*

    $_

    *)
  77. | HOLE of string option
    (*

    HOLE x is ?x.

    *)
  78. | INTLIT of int
    (*

    INTLIT i is the integer literal i.

    *)
  79. | BLOCK_COMMENT of string
    (*

    A block comment of the form %{{ ... }}%

    *)

Tokens

Instances

include Support.Eq.EQ with type t := t
val equal : t -> t -> bool

equal a b is true if and only if a and b are equal. This should satisfy the following properties:

  • Reflexivity: equal a a = true
  • Symmetry: equal a b is equivalent to equal b a
  • Transitivity: if equal a b = true and equal b c = true, then equal a c = true
val (=) : t -> t -> bool

Operator alias of equal.

val (<>) : t -> t -> bool

Negation of operator (=).

include Support.Show.SHOW with type t := t
val pp : Support.Format.formatter -> t -> unit

pp ppf t emits t pretty-printed to ppf.

val show : t -> string

show t pretty-prints t to a string.