Module Make_disambiguation.Entry

Recorded data on bindings in Beluga signatures.

type t

The type of entry.

val is_lf_variable : t -> Stdlib.Bool.t

is_lf_variable entry is true if and only if entry describes an LF variable.

val is_meta_variable : t -> Stdlib.Bool.t

is_meta_variable entry is true if entry describes a meta-variable or a contextual variable.

Contextual variables exist only because mlam-expressions ambiguously introduce either a meta-variable, a parameter variable, a substitution variable or a context variable.

val is_parameter_variable : t -> Stdlib.Bool.t

is_parameter_variable is like is_meta_variable, but for entries describing parameter variables.

val is_substitution_variable : t -> Stdlib.Bool.t

is_substitution_variable is like is_meta_variable, but for entries describing parameter variables.

val is_context_variable : t -> Stdlib.Bool.t

is_context_variable is like is_meta_variable, but for entries describing context variables.

val is_computation_variable : t -> Stdlib.Bool.t

is_computation_variable entry is true if and only if entry describes a computation-level variable.

val is_variable : t -> Stdlib.Bool.t

is_variable entry is true if and only if entry describes an LF variable, a meta-level variable, or a computation-level variable.

This is used to discern between the following two cases when disambiguating identifiers in patterns:

  • The case where an exception should be raised because the identifier is a bound variable of the wrong sort.
  • The case where the identifier should be a free variable shadowing a constant.
val is_lf_type_constant : t -> Stdlib.Bool.t

is_lf_type_constant entry is true if and only if entry describes an LF type-level constant.

val is_lf_term_constant : t -> Stdlib.Bool.t

is_lf_term_constant is like is_lf_type_constant, but for entries describing LF term-level constants.

val is_schema_constant : t -> Stdlib.Bool.t

is_schema_constant is like is_lf_type_constant, but for entries describing context schemas.

val is_computation_inductive_type_constant : t -> Stdlib.Bool.t

is_computation_inductive_type_constant is like is_lf_type_constant, but for entries describing inductive computation-level type constants.

val is_computation_stratified_type_constant : t -> Stdlib.Bool.t

is_computation_stratified_type_constant is like is_lf_type_constant, but for entries describing stratified computation-level type constants.

val is_computation_coinductive_type_constant : t -> Stdlib.Bool.t

is_computation_coinductive_type_constant is like is_lf_type_constant, but for entries describing coinductive computation-level type constants.

val is_computation_abbreviation_type_constant : t -> Stdlib.Bool.t

is_computation_abbreviation_type_constant is like is_lf_type_constant, but for entries describing computation-level type constant abbreviations (introduced by the Beluga keyword typedef).

val is_computation_term_constructor : t -> Stdlib.Bool.t

is_computation_term_constructor is like is_lf_type_constant, but for entries describing computation-level constructors.

val is_computation_term_destructor : t -> Stdlib.Bool.t

is_computation_term_destructor is like is_lf_type_constant, but for entries describing computation-level destructors.

val is_program_constant : t -> Stdlib.Bool.t

is_program_constant is like is_lf_type_constant, but for entries describing computation-level programs (introduced by the Beluga keyword rec or val).

val is_module : t -> Stdlib.Bool.t

is_module is like is_lf_type_constant, but for entries describing modules.