Module Make.Parsing

type state = Parser_state.state
val get : state -> state * state
val put : state -> state -> state * unit
val modify : (state -> state) -> state -> state * unit
val eval : (state -> state * 'a) -> state -> 'a
val exec : (state -> state * 'a) -> state -> state
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 * 'b) -> 'a Support.List.t -> state -> state * Stdlib.Unit.t
val traverse_list1_void : ('a -> state -> state * 'b) -> 'a Support.List1.t -> state -> state * Stdlib.Unit.t
val traverse_list2_void : ('a -> state -> state * 'b) -> '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 * 'b) -> 'a Support.List.t -> state -> state * Stdlib.Unit.t
val traverse_reverse_list1_void : ('a -> state -> state * 'b) -> 'a Support.List1.t -> state -> state * Stdlib.Unit.t
val traverse_reverse_list2_void : ('a -> state -> state * 'b) -> '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 * 'b) -> '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
val peek : state -> state * Located_token.t option
val observe : state -> state * Located_token.t option
val accept : state -> state * unit
val insert : Located_token.t -> state -> state * unit
val next_location : state -> state * Beluga_syntax.Location.t option
val previous_location : state -> state * Beluga_syntax.Location.t option
val enable_backtracking : state -> state * unit
val disable_backtracking : state -> state * unit
val can_backtrack : state -> state * bool
val allow_backtracking_on_error : (state -> state * ('a, 'e) Stdlib.result) -> state -> state * ('a, 'e) Stdlib.result
val with_checkpoint : (state -> state * ('a, 'e) Stdlib.result) -> state -> state * ('a, [> `Backtracked of 'e | `Did_not_backtrack of 'e ]) Stdlib.result
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
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
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
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
val harpoon_proof : state -> state * (Synprs.harpoon_proof, exn) Stdlib.result
val interactive_harpoon_command : state -> state * (Synprs.harpoon_repl_command, exn) Stdlib.result
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
val return : 'a -> 'a t
val bind : ('a -> 'b t) -> 'a t -> 'b t
val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
val compose : ('b -> 'c t) -> ('a -> 'b t) -> 'a -> 'c t
val (>=>) : ('a -> 'b t) -> ('b -> 'c t) -> 'a -> 'c t
val (let*) : 'a t -> ('a -> 'b t) -> 'b t
val (and*) : 'a t -> 'b t -> ('a * 'b) t
val map : ('a -> 'b) -> 'a t -> 'b t
val ($>) : 'a t -> ('a -> 'b) -> 'b t
val (let+) : 'a t -> ('a -> 'b) -> 'b t
val (and+) : 'a t -> 'b t -> ('a * 'b) t
val ap : 'a t -> ('a -> 'b) t -> 'b t
val (<&>) : ('a -> 'b) t -> 'a t -> 'b t
val ap_first : 'b t -> 'a t -> 'a t
val (<&) : 'a t -> 'b t -> 'a t
val ap_second : 'b t -> 'a t -> 'b t
val (&>) : 'a t -> 'b t -> 'b t
val seq2 : 'a1 t -> 'a2 t -> ('a1 * 'a2) t
val seq3 : 'a1 t -> 'a2 t -> 'a3 t -> ('a1 * 'a2 * 'a3) t
val seq4 : 'a1 t -> 'a2 t -> 'a3 t -> 'a4 t -> ('a1 * 'a2 * 'a3 * 'a4) t
val seq5 : 'a1 t -> 'a2 t -> 'a3 t -> 'a4 t -> 'a5 t -> ('a1 * 'a2 * 'a3 * 'a4 * 'a5) t
val lift2 : ('a1 -> 'a2 -> 'r) -> 'a1 t -> 'a2 t -> 'r t
val lift3 : ('a1 -> 'a2 -> 'a3 -> 'r) -> 'a1 t -> 'a2 t -> 'a3 t -> 'r t
val lift4 : ('a1 -> 'a2 -> 'a3 -> 'a4 -> 'r) -> 'a1 t -> 'a2 t -> 'a3 t -> 'a4 t -> 'r t
val lift5 : ('a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 -> 'r) -> 'a1 t -> 'a2 t -> 'a3 t -> 'a4 t -> 'a5 t -> 'r t
val replicate : int -> 'a t -> 'a list t
val run : 'a t -> state -> state * ('a, exn) Stdlib.result
val run_exn : 'a t -> state -> state * 'a
val eval_exn : 'a t -> state -> 'a
val catch : 'a t -> ((state * ('a, exn) Stdlib.result) -> state * ('b, exn) Stdlib.result) -> 'b t
val fail : exn -> 'a t
val fail_at_location : Beluga_syntax.Location.t -> exn -> 'a t
val fail_at_next_location : exn -> 'a t
val fail_at_previous_location : exn -> 'a t
val labelled : string -> 'a t -> 'a t
val span : 'a t -> (location * 'a) t
val only : 'a t -> 'a t
val maybe : 'a t -> 'a option t
val void : 'a t -> unit t
val many : 'a t -> 'a list t
val some : 'a t -> 'a Support.List1.t t
val sep_by0 : sep:unit t -> 'a t -> 'a list t
val sep_by1 : sep:unit t -> 'a t -> 'a Support.List1.t t
val trying : 'a t -> 'a t
val choice : 'a t Support.List.t -> 'a t
val alt : 'a t -> 'a t -> 'a t
val satisfy : (token option -> ('a, exn) Stdlib.result) -> 'a t
val eoi : unit t
val insert_token : token -> unit t
val keyword : string -> unit t
val integer : int t
val dot_integer : int t
val pragma : string -> unit t
val string_literal : string t
val dot : unit t
val dots : unit t
val comma : unit t
val colon : unit t
val semicolon : unit t
val slash : unit t
val equals : unit t
val lambda : unit t
val hat : unit t
val underscore : unit t
val pipe : unit t
val forward_arrow : unit t
val backward_arrow : unit t
val thick_forward_arrow : unit t
val plus : unit t
val star : unit t
val hash : unit t
val double_colon : unit t
val turnstile : unit t
val turnstile_hash : unit t
val left_parenthesis : unit t
val right_parenthesis : unit t
val left_brace : unit t
val right_brace : unit t
val left_brack : unit t
val right_brack : unit t
val left_angle : unit t
val right_angle : unit t
val parens : 'a t -> 'a t
val braces : 'a t -> 'a t
val bracks : 'a t -> 'a t
val angles : 'a t -> 'a t
val opt_parens : 'a t -> 'a t
val opt_braces : 'a t -> 'a t
val opt_bracks : 'a t -> 'a t
val opt_angles : 'a t -> 'a t
val hash_parens : 'a t -> 'a t
val dollar_parens : 'a t -> 'a t
val hash_bracks : 'a t -> 'a t
val dollar_bracks : 'a t -> 'a t
val identifier : Beluga_syntax.Identifier.t t
val dot_identifier : Beluga_syntax.Identifier.t t
val hash_identifier : Beluga_syntax.Identifier.t t
val dollar_identifier : Beluga_syntax.Identifier.t t
val omittable_identifier : Beluga_syntax.Identifier.t option t
val omittable_hash_identifier : Beluga_syntax.Identifier.t option t
val omittable_dollar_identifier : Beluga_syntax.Identifier.t option t
val qualified_identifier : Beluga_syntax.Qualified_identifier.t t
val dot_qualified_identifier : Beluga_syntax.Qualified_identifier.t t
val qualified_or_plain_identifier : [> `Plain of Beluga_syntax.Identifier.t | `Qualified of Beluga_syntax.Qualified_identifier.t ] t
val omittable_meta_object_identifier : (Beluga_syntax.Identifier.t option * [> `Dollar | `Hash | `Plain ]) t
val meta_object_identifier : (Beluga_syntax.Identifier.t * [> `Dollar | `Hash | `Plain ]) t
val hole : [> `Labelled of Beluga_syntax.Identifier.t | `Unlabelled ] parser
val block_comment : (Beluga_syntax.Location.t * string) t
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