DISAMBIGUATION (beluga.Beluga_parser.DISAMBIGUATION)

include DISAMBIGUATION_STATE

include Support.Imperative_state.IMPERATIVE_STATE

type state

module Entry : Disambiguation_state.ENTRY

Recorded data on bindings in Beluga signatures.

Variables

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

add_lf_variable state ?location identifier adds identifier as a bound LF variable, with binding site location. If location = Option.None, then identifier's location is used instead.

This is mostly used for testing. For locally binding an LF variable, see with_bound_lf_variable.

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

add_meta_variable is like add_lf_variable, but the identifier is added as a bound meta-variable.

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

add_parameter_variable is like add_lf_variable, but the identifier is added as a bound parameter variable (those variables prefixed by '#' like "#p").

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

add_substitution_variable is like add_lf_variable, but the identifier is added as a bound substitution variable (those variables prefixed by '$' like "$S").

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

add_context_variable is like add_lf_variable, but the identifier is added as a bound context variable.

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

add_contextual_variable is like add_lf_variable, but the identifier is added as a bound contextual variable, meaning that it is ambiguously bound as either a meta, parameter, substitution or context variable.

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

add_computation_variable is like add_lf_variable, but the identifier is added as a bound computation-level variable.

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

add_free_lf_variable state ?location identifier is add_lf_variable state ?location identifier, with the additional behaviour of adding identifier as an inner pattern bound identifier and as a free variable during pattern disambiguation. This means that identifier can subsequently be looked up as a bound LF variable during pattern disambiguation. This effectively allows free LF variables to appear multiple times (non-linearly) in patterns.

See with_free_variables_as_pattern_variables for the handler for converting free variables in patterns to binders for use as bound variables in expressions.

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

add_free_meta_variable is like add_free_lf_variable, but the identifier is added as a free meta-variable.

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

add_free_meta_variable is like add_free_lf_variable, but the identifier is added as a free parameter variable.

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

add_free_meta_variable is like add_free_lf_variable, but the identifier is added as a free substitution variable.

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

add_free_meta_variable is like add_free_lf_variable, but the identifier is added as a free context variable.

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

add_free_computation_variable state ?location identifier adds identifier to state as a free variable during pattern disambiguation. This differs from add_free_lf_variable in that free computation-level variables in patterns do not have implicit binders (because they are not part of the meta-context), and hence must appear only once (linearly) in the overall pattern.

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

with_bound_lf_variable state ?location identifier m is the result of running m in the local state derived from state having identifier as a bound LF variable.

When disambiguating a pattern, identifier is also added as an inner pattern binding.

For example, the disambiguation of an LF term-level lambda-abstraction \x. m requires that the parameter x is locally added in scope when disambiguating the body m. This is achieved like this:

  with_bound_lf_variable state x (fun state ->
      disambiguate_lf_term state m)

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

with_bound_meta_variable state ?location identifier m is like with_bound_lf_variable, except that identifier is added to the state as a bound meta-variable.

When disambiguating a pattern, identifier is also added as an inner pattern binding.

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

with_bound_contextual_variable state ?location identifier m is like with_bound_lf_variable, except that identifier is added to the state as a bound contextual variable. This is different from with_bound_meta_variable, with_bound_parameter_variable, with_bound_substitution_variable and with_bound_context_variable in that it is unknown whether identifier should be a meta-variable, parameter variable, substitution variable or context variable. This is used in particular for mlam expressions.

When disambiguating a pattern, identifier is also added as an inner pattern binding.

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

with_bound_computation_variable state ?location identifier m is like with_bound_lf_variable, except that identifier is added to the state as a bound computation-level variable.

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

with_bound_pattern_meta_variable state ?location identifier m is like with_bound_meta_variable state ?location identifier m except that identifier is also treated as a free variable so that in with_free_variables_as_pattern_variables it can be treated as a pattern variable usable in the expression.

This is used for meta-variables introduced in the meta-context of a pattern during case analysis. Those variables are considered bound in both the pattern and expression.

For example, B as below is one such bound pattern meta-variable, and appears in scope for ?.

  case x of
  | { B : [g |- o] } [g |- impi \u. D] => ?

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

with_bound_pattern_parameter_variable is like with_bound_pattern_meta_variable, but for a parameter variable introduced in the meta-context of a pattern.

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

with_bound_pattern_substitution_variable is like with_bound_pattern_meta_variable, but for a substitution variable introduced in the meta-context of a pattern.

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

with_bound_pattern_context_variable is like with_bound_pattern_meta_variable, but for a context variable introduced in the meta-context of a pattern.

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

with_free_variables_as_pattern_variables state ~pattern ~expression state is the result of running expression with the free variables added in pattern as bound variables. This is used to disambiguate expression with bound variables arising from free variables in pattern.

pattern is run with respect to state while keeping track of free variables. Variables bound outside the pattern are ignored in lookups.
expression is run with respect to state with the addition of the tracked free variables from patterns as bound variables.

Lookups performed in pattern are more complex. The variables in state count as being unbound, but the variables with binders in the pattern count as bound. Binders in a pattern can be user-specified, or to be reconstructed during abstraction.

A variable is specifically inner bound if it is introduced explicitly by a lambda abstraction or the pattern meta-context, as an explicit or implicit parameter. Free meta-level variables are reconstructed inner bound. For instance, assuming s and ctx are constants:

In the pattern (x, x), both occurrences of x are pattern variables, and that pattern is not linear.
In the pattern {M : [ |- nat]} [ |- s M], M as introduced in the meta-context is a pattern variable, and M is an inner pattern-bound identifier in s M, so that pattern is linear.
In the pattern [ |- \x. s x], there are no pattern variables.
In the pattern ([g |- s M], [g |- s M]), g and M are pattern variables in the left projection of the tuple pattern, and inner pattern-bound in the right projection of the tuple pattern. This is because the pattern is reconstructed as {g : ctx} {M : [g |- nat]} ([g |- s M], [g |- s M]).

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

with_frame state m runs m in a nested bindings frame that is discarded afterwards.

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

with_parent_frame state m runs m while ignoring the topmost frame.

This is used for the disambiguation of Harpoon proof scripts because Harpoon hypotheticals are already serialized with all the identifiers in the meta-level and computation-level contexts of the proof.

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

with_bindings_checkpoint state m runs m with a checkpoint on the bindings' state to backtrack to in case m raises an exception.

This is used for backtracking when disambiguating old-style LF type-level and term-level declarations (i.e., x : X where X may be an LF kind or an LF type).

This is also used in REPLs to safely run parsing functions and recover the state in case of a raised exception during disambiguation.

This checkpoint mechanism does not perform a copy or snapshot of the referencing environment. You need to make sure that m does not pop too many frames.

Constants

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

add_lf_type_constant state ?location ?arity identifier adds identifier as a bound LF type-level constant.

In the disambiguation of a module's declaration, this also adds the constant as one of the module's declarations.

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

add_lf_term_constant is like add_lf_type_constant, but for LF term-level constants.

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

add_schema_constant is like add_lf_type_constant, but for schema constants.

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

add_inductive_computation_type_constant is like add_lf_type_constant, but for inductive computation-level type constants.

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

add_stratified_computation_type_constant is like add_lf_type_constant, but for stratified computation-level type constants.

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

add_coinductive_computation_type_constant is like add_lf_type_constant, but for coinductive computation-level type constants.

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

add_abbreviation_computation_type_constant is like add_lf_type_constant, but for computation-level abbreviation type constants.

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

add_computation_term_constructor is like add_lf_type_constant, but for computation-level term constructors.

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

add_computation_term_destructor is like add_lf_type_constant, but for computation-level term destructors.

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

add_program_constant is like add_lf_type_constant, but for computation-level program constants.

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

add_module state ?location identifier m is the result of running m in a module disambiguation state, whereby added constants are kept track of as declarations in the module having identifier.

Lookups

exception Unbound_identifier of Beluga_syntax.Syncom.Identifier.t

Unbound_identifier identifier is raised if identifier cannot be found in a disambiguation state when it is looked up.

This exception is caught whenever a variable lookup fails and identifier can be disambiguated as a free variable.

exception Unbound_qualified_identifier of Beluga_syntax.Syncom.Qualified_identifier.t

Unbound_qualified_identifier identifier is raised if identifier cannot be found in a disambiguation state when it is looked up.

This exception is unrecoverable, but is caught during disambiguation to provide better error messages.

exception Unbound_namespace of Beluga_syntax.Syncom.Qualified_identifier.t

Unbound_namespace namespace_identifier is raised if a qualified identifier could not be looked up in a disambiguation state because the namespace with identifier namespace_identifier is unbound.

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

lookup_toplevel state identifier is entry if identifier resolves to entry in state. If identifier is unbound in state, then Unbound_identifier identifier is raised.

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

lookup state identifier is entry if identifier resolves to entry in state. Otherwise:

Unbound_identifier ident) is raised if the first segment ident in identifier is unbound.
Unbound_namespace namespace_identifier is raised if a segment in identifier other than the first or last is unbound.
Unbound_qualified_identifier identifier is raised if the last segment in identifier is unbound.

type 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

maximum_lookup state segments is either:

Unbound { segments } if the first segment in segments is unbound in state.
Partially_bound { leading_segments; segment; entry; trailing_segments } if the qualified identifier with namespaces leading_segments and name segment is bound to entry in state.
Bound { identifier; entry } if segments form a qualified identifier bound to entry in state.

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

actual_binding_exn identifier entry is an exception reporting what sort of entry is bound at identifier. The exception is annotated with the entry's binding location.

Signature Operations

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

open_module state module_identifier adds the exported constants from the module bound to module_identifier as toplevel entries in state. If module_identifier is unbound in state, then an exception is raised.

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

get_default_associativity state is the associativity to use for infix operators defined by the user using a pragma, without specifying the infix operator's associativity.

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

set_default_associativity state default_associativity sets default_associativity as the associativity to return from get_default_associativity.

val get_default_precedence : state -> Support.Int.t

get_default_precedence state is the precedence to use for operators defined by the user using a pragma, without specifying the operator's precedence.

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

set_default_precedence state default_precedence sets default_precedence as the precedence to return from get_default_precedence.

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

add_prefix_notation state ?precedence identifier adds a prefix notation for identifier. If precedence = Option.None, then get_default_precedence is used instead.

An exception is raised if identifier is unbound in state, not bound to a constant, or bound to a constant of an unknown or invalid arity.

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

add_infix_notation state ?precedence ?associativity identifier adds an infix notation for identifier. If precedence = Option.None, then get_default_precedence is used instead. Likewise, if associativity = Option.None, then get_default_associativity is used instead.

An exception is raised if identifier is unbound in state, not bound to a constant, or bound to a constant of an unknown or invalid arity.

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

add_postfix_notation state ?precedence identifier adds a postfix notation for identifier. If precedence = Option.None, then get_default_precedence is used instead.

An exception is raised if identifier is unbound in state, not bound to a constant, or bound to a constant of an unknown or invalid arity.

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

add_postponed_prefix_notation state ?precedence identifier adds a postponed prefix notation for identifier. If precedence = Option.None, then get_default_precedence is used instead.

This notation is postponed, meaning that it only applies once apply_postponed_fixity_pragmas is called.

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

add_postponed_infix_notation state ?precedence ?associativity identifier adds a postponed infix notation for identifier. If precedence = Option.None, then get_default_precedence is used instead. Likewise, if associativity = Option.None, then get_default_associativity is used instead.

This notation is postponed, meaning that it only applies once apply_postponed_fixity_pragmas is called.

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

add_postponed_postfix_notation state ?precedence identifier adds a postponed postfix notation for identifier. If precedence = Option.None, then get_default_precedence is used instead.

This notation is postponed, meaning that it only applies once apply_postponed_fixity_pragmas is called.

val apply_postponed_fixity_pragmas : state -> unit

apply_postponed_fixity_pragmas state adds in scope the postponed prefix, infix and postfix fixity pragmas. This function should be called only when the targets of those postponed pragmas are in scope. That is, postponed fixity pragmas are applied after the subsequent declaration is added, or after a group of mutually recursive declarations are added.

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

lookup_operator state identifier is Option.Some operator if identifier is bound to an operator with descriptor operator in state, and Option.None otherwise.

This is used to resolve operators in the disambiguation of applications, which are parsed as lists of expressions.

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

add_module_abbreviation state ?location module_identifier abbreviation adds the synonym abbreviation for the module bound to identifier in state.

An exception is raised if module_identifier is unbound in state, or if module_identifier is not bound to a module in state.

include Lf_disambiguation.LF_DISAMBIGUATION with type state := state

include Support.Imperative_state.IMPERATIVE_STATE with type state := state

Disambiguation

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

disambiguate_lf_kind state object_ is kind', the LF kind disambiguated from kind in the disambiguation state state.

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

disambiguate_lf_typ state typ is typ', the LF type disambiguated from typ in the disambiguation state state.

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

disambiguate_lf_term state term is term', the LF term disambiguated from term in the disambiguation state state.

include Clf_disambiguation.CLF_DISAMBIGUATION with type state := state

include Support.Imperative_state.IMPERATIVE_STATE with type state := state

Disambiguation

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

include Meta_disambiguation.META_DISAMBIGUATION with type state := state

include Support.Imperative_state.IMPERATIVE_STATE with type state := state

Disambiguation

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

include Comp_disambiguation.COMP_DISAMBIGUATION with type state := state

include Support.Imperative_state.IMPERATIVE_STATE with type state := state

Disambiguation

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

include Harpoon_disambiguation.HARPOON_DISAMBIGUATION with type state := state

include Support.Imperative_state.IMPERATIVE_STATE with type state := state

Disambiguation

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

include Signature_disambiguation.SIGNATURE_DISAMBIGUATION
  with type state := state

include Support.Imperative_state.IMPERATIVE_STATE with type state := state

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

traverse_list state f [x1; x2; ...; xn] is [y1; y2; ...; yn] where yi = f state xi, and y1, y2, ..., yn are computed in order, meaning that y1 is computed first, then y2, etc.

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

iter_list state f [x1; x2; ...; xn] is f state x1; f state x2; ...; f state xn.

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

traverse_reverse_list state f [x1; x2; ...; xn] is [y1; y2; ...; yn] where yi = f state xi, and y1, y2, ..., yn are computed in reverse order, meaning that yn is computed first, then y(n-1), etc.

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

iter_rev_list state f [x1; x2; ...; xn] is f state xn; f state x(n-1); ...; f state x1.

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

Disambiguation

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