Module type Disambiguation_state.ENTRY

Abstract definition of entries bound to identifiers.

Disambiguation performs a traversal of the parser syntax to convert it to the external syntax. During this traversal, the disambiguation state is updated to keep track of the referencing environment at each node. Specifically, we add identifiers introduced by function abstractions, patterns, lambdas a Pis.

A disambiguation state entry is the data associated with an identifier in scope. Entries are constructed when a binding is added to the disambiguation state. Notation pragmas edit entries as well.

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.