Disambiguation (beluga.Beluga_parser.Parser.Disambiguation)

type state = Disambiguation_state.state

module Entry : sig ... end

val add_lf_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_meta_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_parameter_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_substitution_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_context_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_contextual_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_computation_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_free_lf_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_free_meta_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_free_parameter_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_free_substitution_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_free_context_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_free_computation_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val with_bound_lf_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  (state -> 'a) ->
  'a

val with_bound_meta_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  (state -> 'a) ->
  'a

val with_bound_parameter_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  (state -> 'a) ->
  'a

val with_bound_substitution_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  (state -> 'a) ->
  'a

val with_bound_context_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  (state -> 'a) ->
  'a

val with_bound_contextual_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  (state -> 'a) ->
  'a

val with_bound_computation_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  (state -> 'a) ->
  'a

val with_bound_pattern_meta_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  (state -> 'a) ->
  'a

val with_bound_pattern_parameter_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  (state -> 'a) ->
  'a

val with_bound_pattern_substitution_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  (state -> 'a) ->
  'a

val with_bound_pattern_context_variable : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  (state -> 'a) ->
  'a

val with_free_variables_as_pattern_variables : 
  state ->
  pattern:(state -> 'a) ->
  expression:(state -> 'a -> 'b) ->
  'b

val with_frame : state -> (state -> 'a) -> 'a

val with_parent_frame : state -> (state -> 'a) -> 'a

val with_bindings_checkpoint : state -> (state -> 'a) -> 'a

val add_lf_type_constant : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  ?arity:Support.Int.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_lf_term_constant : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  ?arity:Support.Int.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_schema_constant : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_inductive_computation_type_constant : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  ?arity:Support.Int.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_stratified_computation_type_constant : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  ?arity:Support.Int.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_coinductive_computation_type_constant : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  ?arity:Support.Int.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_abbreviation_computation_type_constant : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  ?arity:Support.Int.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_computation_term_constructor : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  ?arity:Support.Int.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_computation_term_destructor : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_program_constant : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  ?arity:Support.Int.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val add_module : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  (state -> 'a) ->
  'a

exception Unbound_identifier of Beluga_syntax.Syncom.Identifier.t

exception Unbound_qualified_identifier of Beluga_syntax.Syncom.Qualified_identifier.t

exception Unbound_namespace of Beluga_syntax.Syncom.Qualified_identifier.t

val lookup_toplevel : state -> Beluga_syntax.Syncom.Identifier.t -> Entry.t

val lookup : state -> Beluga_syntax.Syncom.Qualified_identifier.t -> Entry.t

type maximum_lookup_result =
  Make_disambiguation(Disambiguation_state).maximum_lookup_result =

| Unbound of {
1. segments : Beluga_syntax.Syncom.Identifier.t Support.List1.t;
}
| Partially_bound of {
1. leading_segments : Beluga_syntax.Syncom.Identifier.t Support.List.t;
2. segment : Beluga_syntax.Syncom.Identifier.t;
3. entry : Entry.t;
4. trailing_segments : Beluga_syntax.Syncom.Identifier.t Support.List1.t;
}
| Bound of {
1. entry : Entry.t;
}

val maximum_lookup : 
  state ->
  Beluga_syntax.Syncom.Identifier.t Support.List1.t ->
  maximum_lookup_result

val actual_binding_exn : 
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Entry.t ->
  exn

val open_module : 
  state ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

val get_default_associativity : state -> Beluga_syntax.Syncom.Associativity.t

val set_default_associativity : 
  state ->
  Beluga_syntax.Syncom.Associativity.t ->
  Stdlib.Unit.t

val get_default_precedence : state -> Support.Int.t

val set_default_precedence : state -> Support.Int.t -> Stdlib.Unit.t

val add_prefix_notation : 
  state ->
  ?precedence:Support.Int.t ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

val add_infix_notation : 
  state ->
  ?precedence:Support.Int.t ->
  ?associativity:Beluga_syntax.Syncom.Associativity.t ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

val add_postfix_notation : 
  state ->
  ?precedence:Support.Int.t ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

val add_postponed_prefix_notation : 
  state ->
  ?precedence:Support.Int.t ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

val add_postponed_infix_notation : 
  state ->
  ?precedence:Support.Int.t ->
  ?associativity:Beluga_syntax.Syncom.Associativity.t ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

val add_postponed_postfix_notation : 
  state ->
  ?precedence:Support.Int.t ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

val apply_postponed_fixity_pragmas : state -> unit

val lookup_operator : 
  state ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Beluga_syntax.Syncom.Operator.t Support.Option.t

val add_module_abbreviation : 
  state ->
  ?location:Beluga_syntax.Syncom.Location.t ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

val disambiguate_lf_kind : state -> Synprs.lf_object -> Synext.lf_kind

val disambiguate_lf_typ : state -> Synprs.lf_object -> Synext.lf_typ

val disambiguate_lf_term : state -> Synprs.lf_object -> Synext.lf_term

val disambiguate_clf_typ : state -> Synprs.clf_object -> Synext.clf_typ

val disambiguate_clf_term : state -> Synprs.clf_object -> Synext.clf_term

val disambiguate_clf_substitution : 
  state ->
  Synprs.clf_context_object ->
  Synext.clf_substitution

val with_disambiguated_clf_context : 
  state ->
  Synprs.clf_context_object ->
  (state -> Synext.clf_context -> 'a) ->
  'a

val disambiguate_clf_term_pattern : 
  state ->
  Synprs.clf_object ->
  Synext.clf_term_pattern

val disambiguate_clf_substitution_pattern : 
  state ->
  Synprs.clf_context_object ->
  Synext.clf_substitution_pattern

val with_disambiguated_clf_context_pattern : 
  state ->
  Synprs.clf_context_object ->
  (state -> Synext.clf_context_pattern -> 'a) ->
  'a

val disambiguate_clf_context_pattern : 
  state ->
  Synprs.clf_context_object ->
  Synext.clf_context_pattern

val disambiguate_meta_typ : state -> Synprs.meta_thing -> Synext.meta_typ

val disambiguate_meta_object : state -> Synprs.meta_thing -> Synext.meta_object

val disambiguate_meta_pattern : 
  state ->
  Synprs.meta_thing ->
  Beluga_syntax.Synext.Meta.Pattern.t

val disambiguate_schema : state -> Synprs.schema_object -> Synext.schema

val with_disambiguated_meta_context : 
  state ->
  Synprs.meta_context_object ->
  (state -> Synext.meta_context -> 'a) ->
  'a

val with_disambiguated_meta_context_pattern : 
  state ->
  Synprs.meta_context_object ->
  (state -> Synext.meta_context -> 'a) ->
  'a

val disambiguate_comp_kind : 
  state ->
  Synprs.comp_sort_object ->
  Synext.comp_kind

val disambiguate_comp_typ : state -> Synprs.comp_sort_object -> Synext.comp_typ

val disambiguate_comp_expression : 
  state ->
  Synprs.comp_expression_object ->
  Synext.comp_expression

val disambiguate_comp_pattern : 
  state ->
  Synprs.comp_pattern_object ->
  Synext.comp_pattern

val disambiguate_comp_copattern : 
  state ->
  Synprs.comp_copattern_object Support.List1.t ->
  Synext.comp_copattern

val with_disambiguated_comp_context : 
  state ->
  Synprs.comp_context_object ->
  (state -> Synext.comp_context -> 'a) ->
  'a

val disambiguate_harpoon_proof : 
  state ->
  Synprs.harpoon_proof ->
  Synext.harpoon_proof

val with_disambiguated_harpoon_command : 
  state ->
  Synprs.harpoon_command ->
  (state -> Synext.harpoon_command -> 'a) ->
  'a

val disambiguate_harpoon_directive : 
  state ->
  Synprs.harpoon_directive ->
  Synext.harpoon_directive

val disambiguate_harpoon_split_branch : 
  state ->
  Synprs.harpoon_split_branch ->
  Synext.harpoon_split_branch

val disambiguate_harpoon_suffices_branch : 
  state ->
  Synprs.harpoon_suffices_branch ->
  Synext.harpoon_suffices_branch

val disambiguate_harpoon_hypothetical : 
  state ->
  Synprs.harpoon_hypothetical ->
  Synext.harpoon_hypothetical

val disambiguate_harpoon_repl_command : 
  state ->
  Synprs.harpoon_repl_command ->
  Synext.harpoon_repl_command

val traverse_tuple2 : 
  state ->
  (state -> 'a1 -> 'b1) ->
  (state -> 'a2 -> 'b2) ->
  ('a1 * 'a2) ->
  'b1 * 'b2

val traverse_tuple3 : 
  state ->
  (state -> 'a1 -> 'b1) ->
  (state -> 'a2 -> 'b2) ->
  (state -> 'a3 -> 'b3) ->
  ('a1 * 'a2 * 'a3) ->
  'b1 * 'b2 * 'b3

val traverse_list : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.List.t ->
  'b Support.List.t

val traverse_list1 : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.List1.t ->
  'b Support.List1.t

val traverse_list2 : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.List2.t ->
  'b Support.List2.t

val iter_list : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List.t ->
  Stdlib.Unit.t

val iter_list1 : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List1.t ->
  Stdlib.Unit.t

val iter_list2 : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List2.t ->
  Stdlib.Unit.t

val traverse_reverse_list : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.List.t ->
  'b Support.List.t

val traverse_reverse_list1 : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.List1.t ->
  'b Support.List1.t

val traverse_reverse_list2 : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.List2.t ->
  'b Support.List2.t

val iter_rev_list : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List.t ->
  Stdlib.Unit.t

val iter_rev_list1 : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List1.t ->
  Stdlib.Unit.t

val iter_rev_list2 : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List2.t ->
  Stdlib.Unit.t

val traverse_option : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.Option.t ->
  'b Support.Option.t

val iter_option : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.Option.t ->
  Stdlib.Unit.t

val seq_list : state -> (state -> 'a) Support.List.t -> 'a Support.List.t

val seq_list1 : state -> (state -> 'a) Support.List1.t -> 'a Support.List1.t

val iter_seq : 
  state ->
  (state -> Stdlib.Unit.t) Support.List.t ->
  Stdlib.Unit.t

val disambiguate_pragma : 
  state ->
  Synprs.signature_pragma ->
  Synext.signature_pragma

val disambiguate_global_pragma : 
  state ->
  Synprs.signature_global_pragma ->
  Synext.signature_global_pragma

val disambiguate_totality_declaration : 
  state ->
  Synprs.signature_totality_declaration ->
  Synext.signature_totality_declaration

val disambiguate_numeric_totality_order : 
  state ->
  Support.Int.t Synprs.signature_totality_order ->
  Support.Int.t Synext.signature_totality_order

val disambiguate_named_totality_order : 
  state ->
  Beluga_syntax.Synext.Identifier.t Synprs.signature_totality_order ->
  Beluga_syntax.Synext.Identifier.t Synext.signature_totality_order

val disambiguate_declaration : 
  state ->
  Synprs.signature_declaration ->
  Synext.signature_declaration

val disambiguate_signature_file : 
  state ->
  Synprs.signature_file ->
  Synext.signature_file

val disambiguate_signature : state -> Synprs.signature -> Synext.signature