Module Beluga_parser.Make_parsing

Functor creating a Beluga parser using the given implementation of state.

Parameters

Signature

include PARSER_STATE with type token = Located_token.t and type location = Beluga_syntax.Location.t with type state = Parser_state.state
include Support.State.STATE with type state = Parser_state.state
type state = Parser_state.state

The type of states inside the monad.

val get : state -> state * state

Return the state from the internals of the monad.

val put : state -> state -> state * unit

Replace the state inside the monad.

val modify : (state -> state) -> state -> state * unit

Modify the state inside the monad.

val eval : (state -> state * 'a) -> state -> 'a

eval a init is run a init = (final, v), but outputs only v.

val exec : (state -> state * 'a) -> state -> state

exec a init is run a init = (final, v), but outputs only final.

Traversals

val traverse_tuple2 : ('a1 -> state -> state * 'b1) -> ('a2 -> state -> state * 'b2) -> ('a1 * 'a2) -> state -> state * ('b1 * 'b2)
val traverse_tuple3 : ('a1 -> state -> state * 'b1) -> ('a2 -> state -> state * 'b2) -> ('a3 -> state -> state * 'b3) -> ('a1 * 'a2 * 'a3) -> state -> state * ('b1 * 'b2 * 'b3)
val traverse_list : ('a -> state -> state * 'b) -> 'a Support.List.t -> state -> state * 'b Support.List.t
val traverse_list1 : ('a -> state -> state * 'b) -> 'a Support.List1.t -> state -> state * 'b Support.List1.t
val traverse_list2 : ('a -> state -> state * 'b) -> 'a Support.List2.t -> state -> state * 'b Support.List2.t
val traverse_list_void : ('a -> state -> state * _) -> 'a Support.List.t -> state -> state * Stdlib.Unit.t
val traverse_list1_void : ('a -> state -> state * _) -> 'a Support.List1.t -> state -> state * Stdlib.Unit.t
val traverse_list2_void : ('a -> state -> state * _) -> 'a Support.List2.t -> state -> state * Stdlib.Unit.t
val traverse_reverse_list : ('a -> state -> state * 'b) -> 'a Support.List.t -> state -> state * 'b Support.List.t
val traverse_reverse_list1 : ('a -> state -> state * 'b) -> 'a Support.List1.t -> state -> state * 'b Support.List1.t
val traverse_reverse_list2 : ('a -> state -> state * 'b) -> 'a Support.List2.t -> state -> state * 'b Support.List2.t
val traverse_reverse_list_void : ('a -> state -> state * _) -> 'a Support.List.t -> state -> state * Stdlib.Unit.t
val traverse_reverse_list1_void : ('a -> state -> state * _) -> 'a Support.List1.t -> state -> state * Stdlib.Unit.t
val traverse_reverse_list2_void : ('a -> state -> state * _) -> 'a Support.List2.t -> state -> state * Stdlib.Unit.t
val traverse_option : ('a -> state -> state * 'b) -> 'a Support.Option.t -> state -> state * 'b Support.Option.t
val traverse_option_void : ('a -> state -> state * _) -> 'a Support.Option.t -> state -> state * Stdlib.Unit.t
val seq_list : (state -> state * 'a) Support.List.t -> state -> state * 'a Support.List.t
val seq_list1 : (state -> state * 'a) Support.List1.t -> state -> state * 'a Support.List1.t
val seq_list_void : (state -> state * unit) list -> state -> state * unit

seq_list_void [x1; x2; ...; xn] performs x1, x2, ..., xn in order.

Instances

include Support.Monad.MONAD with type 'a t := state -> state * 'a
include Support.Functor.FUNCTOR with type 'a t := state -> state * 'a

Combinators

include Support.Apply.APPLY with type 'a t := state -> state * 'a

Combinators

Lexing

val peek : state -> state * Located_token.t option

peek state is (state', token_opt) where token_opt is the next unconsumed token in state. If token_opt = Option.None, then the end of the input stream was reached. Otherwise, token_opt = Option.Some token. The token is not consumed, meaning that state' is not advanced to the next token in the stream.

val observe : state -> state * Located_token.t option

observed state is like peek state, but the observed token is consumed.

val accept : state -> state * unit

accept state is (state', ()) where state' is derived from state by consuming the next token in the input stream. This effectively observes and discards the next token in state.

val insert : Located_token.t -> state -> state * unit

insert token state is (state', ()) where state' is derived from state by inserting token at the beginning of the input stream. That is, token is the next token in state'.

Locations

val next_location : state -> state * Beluga_syntax.Location.t option

next_location state is (state', next_location_opt) where next_location_opt is the location of the next token in state. This does not advance the input stream. next_location_opt = Option.None at the end of the input stream.

val previous_location : state -> state * Beluga_syntax.Location.t option

previous_location state is (state', previous_location_opt) where previous_location_opt is the location of the last token in state to have been consumed. previous_location_opt = Option.None at the beginning of the input stream.

Backtracking

val enable_backtracking : state -> state * unit

enable_backtracking state is (state', ()) where state' has backtracking enabled.

val disable_backtracking : state -> state * unit

enable_backtracking state is (state', ()) where state' has backtracking disabled.

val can_backtrack : state -> state * bool

can_backtrack state is (state', flag) where flag = true indicates that state and state' allow backtracking out of an erroneous result, and flag = false otherwise.

val allow_backtracking_on_error : (state -> state * ('a, 'e) Stdlib.result) -> state -> state * ('a, 'e) Stdlib.result

allow_backtracking_on_error m is m' such that m' state is (state', x) with backtracking enabled in state' if x = Result.Error cause. That is, this combinator enables backtracking if m' produces an error. Backtracking then needs to be manually disabled afterwards.

val with_checkpoint : (state -> state * ('a, 'e) Stdlib.result) -> state -> state * ('a, [> `Backtracked of 'e | `Did_not_backtrack of 'e ]) Stdlib.result

with_checkpoint m is m' such that m' state marks the current state, performs m, then either

  • discards the marked state if m state = (state', Result.Ok x),
  • backtracks to the marked state if m state = (state', Result.Error cause).

The output error from m is additionally annotated with whether backtracking occurred.

In the case of a parser m, backtracking can occur if backtracking is enabled with allow_backtracking_on_error, or if m did not consume any input.

include Parser_combinator.PARSER with type state := state and type location := Beluga_syntax.Location.t and type token := Located_token.t
exception Parser_error of exn
exception Labelled_exception of {
  1. label : string;
  2. cause : exn;
}
exception No_more_choices of exn list
exception Expected_end_of_input
include Support.Monad.MONAD with type 'a t := state -> state * ('a, exn) Stdlib.result
include Support.Functor.FUNCTOR with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

include Support.Apply.APPLY with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

include Common_parser.COMMON_PARSER with type state := state and type location := Beluga_syntax.Location.t and type token := Located_token.t
include Parser_combinator.PARSER with type state := state with type location := Beluga_syntax.Location.t with type token := Located_token.t
exception Parser_error of exn
exception Labelled_exception of {
  1. label : string;
  2. cause : exn;
}
exception No_more_choices of exn list
exception Expected_end_of_input
include Support.Monad.MONAD with type 'a t := state -> state * ('a, exn) Stdlib.result
include Support.Functor.FUNCTOR with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

include Support.Apply.APPLY with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

include Lf_parser.LF_PARSER with type state := state
include Common_parser.COMMON_PARSER with type state := state
include Parser_combinator.PARSER with type state := state
exception Parser_error of exn
exception Labelled_exception of {
  1. label : string;
  2. cause : exn;
}
exception No_more_choices of exn list
exception Expected_end_of_input
include Support.Monad.MONAD with type 'a t := state -> state * ('a, exn) Stdlib.result
include Support.Functor.FUNCTOR with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

include Support.Apply.APPLY with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

val lf_kind : state -> state * (Synprs.lf_object, exn) Stdlib.result
val lf_typ : state -> state * (Synprs.lf_object, exn) Stdlib.result
val lf_term : state -> state * (Synprs.lf_object, exn) Stdlib.result
include Clf_parser.CLF_PARSER with type state := state
include Common_parser.COMMON_PARSER with type state := state
include Parser_combinator.PARSER with type state := state
exception Parser_error of exn
exception Labelled_exception of {
  1. label : string;
  2. cause : exn;
}
exception No_more_choices of exn list
exception Expected_end_of_input
include Support.Monad.MONAD with type 'a t := state -> state * ('a, exn) Stdlib.result
include Support.Functor.FUNCTOR with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

include Support.Apply.APPLY with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

val clf_typ : state -> state * (Synprs.clf_object, exn) Stdlib.result
val clf_term : state -> state * (Synprs.clf_object, exn) Stdlib.result
val clf_term_pattern : state -> state * (Synprs.clf_object, exn) Stdlib.result
val clf_context : state -> state * (Synprs.clf_context_object, exn) Stdlib.result
val clf_substitution : state -> state * (Synprs.clf_context_object, exn) Stdlib.result
include Meta_parser.META_PARSER with type state := state
include Common_parser.COMMON_PARSER with type state := state
include Parser_combinator.PARSER with type state := state
exception Parser_error of exn
exception Labelled_exception of {
  1. label : string;
  2. cause : exn;
}
exception No_more_choices of exn list
exception Expected_end_of_input
include Support.Monad.MONAD with type 'a t := state -> state * ('a, exn) Stdlib.result
include Support.Functor.FUNCTOR with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

include Support.Apply.APPLY with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

val schema : state -> state * (Synprs.schema_object, exn) Stdlib.result
val meta_type : state -> state * (Synprs.meta_thing, exn) Stdlib.result
val meta_object : state -> state * (Synprs.meta_thing, exn) Stdlib.result
val meta_pattern : state -> state * (Synprs.meta_thing, exn) Stdlib.result
val meta_context : state -> state * (Synprs.meta_context_object, exn) Stdlib.result
include Comp_parser.COMP_PARSER with type state := state
include Common_parser.COMMON_PARSER with type state := state
include Parser_combinator.PARSER with type state := state
exception Parser_error of exn
exception Labelled_exception of {
  1. label : string;
  2. cause : exn;
}
exception No_more_choices of exn list
exception Expected_end_of_input
include Support.Monad.MONAD with type 'a t := state -> state * ('a, exn) Stdlib.result
include Support.Functor.FUNCTOR with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

include Support.Apply.APPLY with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

val comp_kind : state -> state * (Synprs.comp_sort_object, exn) Stdlib.result
val comp_typ : state -> state * (Synprs.comp_sort_object, exn) Stdlib.result
val comp_pattern : state -> state * (Synprs.comp_pattern_object, exn) Stdlib.result
val comp_copattern : state -> state * (Synprs.comp_copattern_object, exn) Stdlib.result
val comp_expression : state -> state * (Synprs.comp_expression_object, exn) Stdlib.result
val comp_context : state -> state * (Synprs.comp_context_object, exn) Stdlib.result
include Harpoon_parser.HARPOON_PARSER with type state := state
include Common_parser.COMMON_PARSER with type state := state
include Parser_combinator.PARSER with type state := state
exception Parser_error of exn
exception Labelled_exception of {
  1. label : string;
  2. cause : exn;
}
exception No_more_choices of exn list
exception Expected_end_of_input
include Support.Monad.MONAD with type 'a t := state -> state * ('a, exn) Stdlib.result
include Support.Functor.FUNCTOR with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

include Support.Apply.APPLY with type 'a t := state -> state * ('a, exn) Stdlib.result

Combinators

val harpoon_proof : state -> state * (Synprs.harpoon_proof, exn) Stdlib.result
val interactive_harpoon_command : state -> state * (Synprs.harpoon_repl_command, exn) Stdlib.result
include Signature_parser.SIGNATURE_PARSER with type state := state with type token = Parser_state.token with type location = Parser_state.location
include Common_parser.COMMON_PARSER with type state := state with type token = Parser_state.token with type location = Parser_state.location
include Parser_combinator.PARSER with type state := state with type token = Parser_state.token with type location = Parser_state.location
type token = Parser_state.token
type location = Parser_state.location
type 'a t = state -> state * ('a, exn) Stdlib.result
type 'a parser = 'a t
exception Parser_error of exn
exception Labelled_exception of {
  1. label : string;
  2. cause : exn;
}
exception No_more_choices of exn list
exception Expected_end_of_input
include Support.Monad.MONAD with type 'a t := 'a t
val return : 'a -> 'a t

return a injects a into the monadic type.

val bind : ('a -> 'b t) -> 'a t -> 'b t

bind f a is the sequential composition of two actions, passing any value produced by a as argument to f.

val (>>=) : 'a t -> ('a -> 'b t) -> 'b t

Operator alias of bind.

val compose : ('b -> 'c t) -> ('a -> 'b t) -> 'a -> 'c t

compose g f is the Kleisli composition of f and g, passing the input to f, then binding the output to g.

val (>=>) : ('a -> 'b t) -> ('b -> 'c t) -> 'a -> 'c t

Operator alias of compose.

val (let*) : 'a t -> ('a -> 'b t) -> 'b t

( let* ) ma f is bind f ma. This is a binding operator, and it is used as let* a = ma in f a.

val (and*) : 'a t -> 'b t -> ('a * 'b) t

( and* ) ma mb is let* a = ma in let* b = mb in return (a, b). This is a binding operator, and it is used as let* a = ma and* b = mb in ....

include Support.Functor.FUNCTOR with type 'a t := 'a t

Combinators

val map : ('a -> 'b) -> 'a t -> 'b t

map f is the function that maps values of t by f. The order of arguments is for use in function pipelines as fb = fa |> map (fun a -> (* ... *)).

val ($>) : 'a t -> ('a -> 'b) -> 'b t

( $> ) is an infix synonym for map.

val (let+) : 'a t -> ('a -> 'b) -> 'b t

( let+ ) ma f is map f a. This is a binding operator, and is used as let+ a = ma in f a

val (and+) : 'a t -> 'b t -> ('a * 'b) t

( and+ ) ma mb is let+ a = ma in let+ b = mb in return (a, b). This is a binding operator, and it is used as let+ a = ma and+ b = mb in ....

include Support.Apply.APPLY with type 'a t := 'a t
val ap : 'a t -> ('a -> 'b) t -> 'b t

ap fa fab applies argument fa to fab under the abstract datatype t.

val (<&>) : ('a -> 'b) t -> 'a t -> 'b t

( <&> ) is an infix synonym of ap.

Combinators

val ap_first : 'b t -> 'a t -> 'a t

ap_first second first combines actions first and second but keeps only first. That is, ap_first second first = first. The order of arguments is for use in function pipelines as first = first |> ap_first second.

val (<&) : 'a t -> 'b t -> 'a t

( <& ) is an infix synonym for ap_first.

val ap_second : 'b t -> 'a t -> 'b t

ap_second second first combines actions first and second but keeps only second. That is, ap_second second first = second. The order of arguments is for use in function pipelines as second = first |> ap_second second.

val (&>) : 'a t -> 'b t -> 'b t

( &> ) is an infix synonym for ap_second.

val seq2 : 'a1 t -> 'a2 t -> ('a1 * 'a2) t

seq2 fa1 fa2 sequentially executes actions fa1 and fa2, and keeps their outputs under the abstract datatype t.

val seq3 : 'a1 t -> 'a2 t -> 'a3 t -> ('a1 * 'a2 * 'a3) t

seq3 fa1 fa2 fa3 sequentially executes actions fa1, fa2 and fa3, and keeps their outputs under the abstract datatype t.

val seq4 : 'a1 t -> 'a2 t -> 'a3 t -> 'a4 t -> ('a1 * 'a2 * 'a3 * 'a4) t

seq4 fa1 fa2 fa3 fa4 sequentially executes actions fa1, fa2, fa3 and fa4, and keeps their outputs under the abstract datatype t.

val seq5 : 'a1 t -> 'a2 t -> 'a3 t -> 'a4 t -> 'a5 t -> ('a1 * 'a2 * 'a3 * 'a4 * 'a5) t

seq5 fa1 fa2 fa3 fa4 fa5 sequentially executes actions fa1, fa2, fa3, fa4 and fa5, and keeps their outputs under the abstract datatype t.

val lift2 : ('a1 -> 'a2 -> 'r) -> 'a1 t -> 'a2 t -> 'r t

lift2 f ma1 ma2 sequentially executes actions ma1, ma2 and passes their outputs to f.

val lift3 : ('a1 -> 'a2 -> 'a3 -> 'r) -> 'a1 t -> 'a2 t -> 'a3 t -> 'r t

lift3 f ma1 ma2 ma3 sequentially executes actions ma1, ma2, ma3 and passes their outputs to f.

val lift4 : ('a1 -> 'a2 -> 'a3 -> 'a4 -> 'r) -> 'a1 t -> 'a2 t -> 'a3 t -> 'a4 t -> 'r t

lift4 f ma1 ma2 ma3 ma4 sequentially executes actions ma1, ma2, ma3, ma4 and passes their outputs to f.

val lift5 : ('a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 -> 'r) -> 'a1 t -> 'a2 t -> 'a3 t -> 'a4 t -> 'a5 t -> 'r t

lift5 f ma1 ma2 ma3 ma4 ma5 sequentially executes actions ma1, ma2, ma3, ma4, ma5 and passes their outputs to f.

val replicate : int -> 'a t -> 'a list t

replicate n a sequentially runs n times a.

  • raises Invalid_argument

    If n < 0.

val run : 'a t -> state -> state * ('a, exn) Stdlib.result

run p state is (state', result) where result is the output of parsing p using state.

This is only meant to be used internally, or when defining new parser combinators, since it does not prune the parser exception when result = Result.Error exn.

The end user of a parser should use run_exn.

val run_exn : 'a t -> state -> state * 'a

run_exn p state is (state', parsed) where parsed is the object parsed from state using p. A pruned exception is raised if p fails.

val eval_exn : 'a t -> state -> 'a

eval_exn p state runs p on state like run_exn, and discards the output parser state. This is used whenever we do not resume parsing from the final parser state, particularly when using the only combinator since we expect the end of the input stream to be reached.

val catch : 'a t -> ((state * ('a, exn) Stdlib.result) -> state * ('b, exn) Stdlib.result) -> 'b t

catch p runs p and invokes the given handler to modify the outcome. Despite being called "catch", this parser is actually a kind of map, and is used to implement "low-level" parser transformations.

val fail : exn -> 'a t

fail exn is the parser that always fails with exn.

val fail_at_location : Beluga_syntax.Location.t -> exn -> 'a t

fail_at_location location exn is the parser that always fails with exn annotated with location.

val fail_at_next_location : exn -> 'a t

fail_at_next_location exn is the parser that always fails with exn annotated with the next location in the input stream.

val fail_at_previous_location : exn -> 'a t

fail_at_previous_location exn is the parser that always fails with exn annotated with the previous location in the input stream.

val labelled : string -> 'a t -> 'a t

labelled label p is p' such that when p fails, p' annotates the exception with a label for error-reporting.

val span : 'a t -> (location * 'a) t

span p is the parser p' that additionally returns the source file location that spans the tokens consumed by p.

val only : 'a t -> 'a t

only p is the parser p' that expects p to succeed, then the end of input to be reached immediately after.

val maybe : 'a t -> 'a option t

maybe p is the parser p' that may fail, in which case it returns Option.none.

val void : 'a t -> unit t

void p is the parser p' that discards the result of p.

val many : 'a t -> 'a list t

many p is the parser p' that parses tokens following the EBNF grammar p*, meaning that it parses 0 or more occurrences of p.

val some : 'a t -> 'a Support.List1.t t

some p is the parser p' that parses tokens following the EBNF grammar p+, meaning that it parses 1 or more occurrences of p.

val sep_by0 : sep:unit t -> 'a t -> 'a list t

sep_by0 ~sep p is the parser p' that parses tokens following the EBNF grammar [p (sep p)*], meaning that it parses 0 or more occurrences of p separated by sep.

val sep_by1 : sep:unit t -> 'a t -> 'a Support.List1.t t

sep_by1 ~sep p is the parser p' that parses tokens following the EBNF grammar p (sep p)+, meaning that it parses 1 or more occurrences of p separated by sep.

val trying : 'a t -> 'a t

trying p is the parser p' that enables backtracking in the parser state if p fails, which signals that the erroneous state can be backtracked out of irrespective of the number of consumed tokens.

val choice : 'a t Support.List.t -> 'a t

choice ps is the parser p that sequentially tries the parsers in p.

For instance, choice [p1; p2] first runs p1. If it fails, p2 is run if one of the following is true.

  • p1 failed without consuming any input.
  • p1 failed with backtracking enabled. Backtracking is enabled by the trying combinator.
val alt : 'a t -> 'a t -> 'a t

alt p1 p2 is choice [p1; p2].

val satisfy : (token option -> ('a, exn) Stdlib.result) -> 'a t

satisfy f is the basic parser p that performs an action based on whether the next token in the stream satisfies the predicate f. The parser is advanced only if the next token satisfies f. If the next token does not satisfy the predicate, then the error is annotated with the next token's location.

val eoi : unit t

eoi is the parser that expects the end of input to be reached. This is either the end of the input string, token stream, or file input channel.

val insert_token : token -> unit t

insert_token token is the parser that inserts token as the next token to be read from the input stream.

val keyword : string -> unit t

keyword s parses the string s either as a keyword token, or an identifier matching s.

val integer : int t

integer parses an integer.

val dot_integer : int t

dot_integer parses a dot followed by an integer.

val pragma : string -> unit t

pragma s parses --s.

val string_literal : string t

string_literal parses an escaped string literal between double quotes.

val dot : unit t

dot parses `.'.

val dots : unit t

dots parses `..'.

val comma : unit t

comma parses `,'.

val colon : unit t

colon parses `:'.

val semicolon : unit t

semicolon parses `;'.

val slash : unit t

slash pases `/'.

val equals : unit t

equals parses `='.

val lambda : unit t

lambda parses `\'.

val hat : unit t

hat parses `^'.

val underscore : unit t

underscore parses `_'.

val pipe : unit t

pipe parses `|'.

val forward_arrow : unit t

forward_arrow parses `->'.

val backward_arrow : unit t

backward_arrow parses `<-'.

val thick_forward_arrow : unit t

thick_forward_arrow parses `=>'.

val plus : unit t

plus parses `+'.

val star : unit t

star parses `*'.

val hash : unit t

hash parses `#'. For identifiers prefixed by a hash symbol, see hash_identifier and omittable_hash_identifier.

val double_colon : unit t

double_colon parses `::'.

val turnstile : unit t

turnstile parses `|-'.

val turnstile_hash : unit t

turnstile_hash parses `|-#'.

val left_parenthesis : unit t

left_parenthesis parses `('.

val right_parenthesis : unit t

right_parenthesis parses `)'.

val left_brace : unit t

left_brace parses `{'.

val right_brace : unit t

right_brace parses `}'.

val left_brack : unit t

left_brack parses `['.

val right_brack : unit t

right_brack parses `]'.

val left_angle : unit t

left_angle parses `<'.

val right_angle : unit t

right_angle parses `>'.

val parens : 'a t -> 'a t

parens p parses `(' p `)'.

val braces : 'a t -> 'a t

braces p parses `{' p `}'.

val bracks : 'a t -> 'a t

bracks p parses `[' p `]'.

val angles : 'a t -> 'a t

angles p parses `<' p `>'.

val opt_parens : 'a t -> 'a t

opt_parens p parses `(' p `)' | p.

val opt_braces : 'a t -> 'a t

opt_braces p parses `{' p `}' | p.

val opt_bracks : 'a t -> 'a t

opt_bracks p parses `[' p `]' | p.

val opt_angles : 'a t -> 'a t

opt_angles p parses `<' p `>' | p.

val hash_parens : 'a t -> 'a t

hash_parens p parses `#(' p `)'.

val dollar_parens : 'a t -> 'a t

dollar_parens p parses `$(' p `)'.

val hash_bracks : 'a t -> 'a t

hash_bracks p parses `#[' p `]'.

val dollar_bracks : 'a t -> 'a t

dollar_bracks p parses `$[' p `]'.

val identifier : Beluga_syntax.Identifier.t t

identifier parses a plain identifier.

val dot_identifier : Beluga_syntax.Identifier.t t

dot_identifier parses a dot followed by an identifier.

val hash_identifier : Beluga_syntax.Identifier.t t

hash_identifier parses an identifier starting with `#'. The prefix `#' is included in the identifier.

val dollar_identifier : Beluga_syntax.Identifier.t t

dollar_identifier parses an identifier starting with `$'. The prefix `$' is included in the identifier.

val omittable_identifier : Beluga_syntax.Identifier.t option t

omittable_identifier parses `_' | <identifier>.

val omittable_hash_identifier : Beluga_syntax.Identifier.t option t

omittable_hash_identifier parses `#_' | <hash-identifier>.

val omittable_dollar_identifier : Beluga_syntax.Identifier.t option t

omittable_dollar_identifier parses `$_' | <dollar-identifier>.

val qualified_identifier : Beluga_syntax.Qualified_identifier.t t

qualified_identifier parses <identifier> (<dot-identifier>)*.

val dot_qualified_identifier : Beluga_syntax.Qualified_identifier.t t

dot_qualified_identifier parses a dot followed by a qualified identifier.

val qualified_or_plain_identifier : [> `Plain of Beluga_syntax.Identifier.t | `Qualified of Beluga_syntax.Qualified_identifier.t ] t

qualified_or_plain_identifier parses a plain identifier or a qualified identifier, whichever is the longest parse. That is, if qualified_or_plain_identifier parses a qualified identifier, then it has at least one namespace.

val omittable_meta_object_identifier : (Beluga_syntax.Identifier.t option * [> `Dollar | `Hash | `Plain ]) t

omittable_meta_object_identifier parses `_' | `#_' | `$_' | <identifier> | <hash-identifier> | <dollar-identifier>.

val meta_object_identifier : (Beluga_syntax.Identifier.t * [> `Dollar | `Hash | `Plain ]) t

meta_object_identifier parses <identifier> | <hash-identifier> | <dollar-identifier>.

val hole : [> `Labelled of Beluga_syntax.Identifier.t | `Unlabelled ] parser

hole parses `?' | `?'<identifier>.

val block_comment : (Beluga_syntax.Location.t * string) t

block_comment parses %{{ c }}%.

val signature_file : Synprs.signature_file t
val signature_global_pragma : Synprs.signature_global_pragma t
val signature_entry : Synprs.signature_entry t
val signature_declaration : Synprs.signature_declaration t
val trust_totality_declaration : Synprs.signature_totality_declaration t
val named_totality_declaration : Synprs.signature_totality_declaration t
val numeric_totality_declaration : Synprs.signature_totality_declaration t
val totality_declaration : Synprs.signature_totality_declaration t