Module Synext

External Syntax Definition

ASTs constructed with the constructors in this module are not necessarily in normal form.

These types are suited for pretty-printing and elaboration to the internal syntax. Note that this is a named representation without ambiguities.

There are three kinds of variables to consider in Beluga:

• LF-bound variables, which are introduced by LF abstractions and contexts, and range over pure LF terms (not contextual LF terms).
• Contextual (or meta-level) variables, which are introduced by computation-level Pi types, dependent type abstractions and meta-object patterns, and range over meta-objects.
• Computation-level variables, which are introduced by computation-level patterns, and range over computation-level expressions.

Contextual variables are further classified in four variants:

• Meta-variables, which range over contextual LF terms.
• Context variables, which range over contextual LF contexts.
• Parameter variables, prefixed by #, which range over contextual LF terms. These are bound variables implicit to a context variable.
• Substitution variables, prefixed by $, which range over contextual LF substitutions.

External LF Syntax

The representation of LF kinds, types, and terms after parsing and data-dependent disambiguation.

These types are only intended to be used in the definition of LF type-level or term-level constants. This is a weak, representational function space without case analysis or recursion.

LF terms as defined below may contain free variables. During the abstraction phase of term reconstruction, implicit binders are introduced for those free variables.

In the following grammar, the metavariable:

• x ranges over variables
• c ranges over term-level constants
• a ranges over type-level constants

      \begin{aligned}
      &\text{LF kinds} &K &\Coloneqq
      \mathsf{type}
      \mid \Pi x {:} A. K
      \mid A \to K\\

      &\text{LF types} &A, B &\Coloneqq
      a
      \mid \Pi x {:} A. B
      \mid A \to B
      \mid A \; M_1 \; M_2 \; \dots \; M_n\\

      &\text{LF terms} &M, N &\Coloneqq
      c
      \mid x
      \mid \_
      \mid \lambda x {:} A. M
      \mid M \; N_1 \; N_2 \; \dots \; N_n
      \mid M : A
      \end{aligned}
    

External Contextual LF Syntax

The representation of contextual LF types, terms, and patterns after parsing and data-dependent disambiguation.

The distinction between contextual LF objects and plain LF objects is that contextual LF objects may have substitutions, and may appear in patterns. Plain LF objects are only used in the definition of type-level or term-level LF constants.

Contextual LF terms as defined below may contain free variables. During the abstraction phase of term reconstruction, implicit binders are introduced for those free variables.

Additionally, free contextual LF variables occurring in a computation-level pattern are considered as pattern variables. That is, free variables occurring in a type annotation to a computation-level pattern count as pattern variables, and are added to the case analysis branch's meta-context.

In the following grammar, the metavariable:

• x ranges over variables
• c ranges over term-level constants
• a ranges over type-level constants
• \$s ranges over substitutions
• g ranges over contexts
• \mathsf{id} ranges over identifiers
• n ranges over integers

      \begin{aligned}
      &\text{Contextual LF types} &A, B &\Coloneqq
      a
      \mid \Pi x {:} A. B
      \mid A \to B
      \mid A \; M_1 \; M_2 \; \dots \; M_n \\&&&
      \mid \mathsf{block} (x_1 : A_1, x_2 : A_2, \dots, x_n : A_n)\\

      &\text{Contextual LF terms} &M, N &\Coloneqq
      c
      \mid x
      \mid \#x
      \mid \_
      \mid \lambda x {:} A. M
      \mid M \; N_1 \; N_2 \; \dots \; N_n \\&&&
      \mid M : A
      \mid M[\sigma]
      \mid \;?
      \mid \;?\mathsf{id}
      \mid \langle M_1; M_2; \dots; M_n \rangle
      \mid M.n
      \mid M.\mathsf{id}\\

      &\text{Contextual LF substitutions} &\sigma &\Coloneqq
      \char`\^
      \mid \dots
      \mid \sigma, M
      \mid \$s[\sigma]\\

      &\text{Contextual LF contexts} &\Psi &\Coloneqq
      \char`\^
      \mid g
      \mid \Psi, x : A\\

      &\text{Contextual LF patterns} &M_p, N_p &\Coloneqq
      c
      \mid x
      \mid \#x
      \mid \_
      \mid \lambda x {:} A. M_p
      \mid M_p \; N_{p,1} \; N_{p,2} \; \dots \; N_{p_n} \\&&&
      \mid M_p : A
      \mid M_p[\sigma]
      \mid \langle M_{p,1}; M_{p,2}; \dots; M_{p,n} \rangle
      \mid M.n
      \mid M.\mathsf{id}\\

      &\text{Contextual LF substitution patterns} &\sigma_p &\Coloneqq
      \char`\^
      \mid \dots
      \mid \sigma_p, M_p
      \mid \$s[\sigma]\\

      &\text{Contextual LF context patterns} &\Psi_p &\Coloneqq
      \char`\^
      \mid g
      \mid \Psi_p, x : A
      \end{aligned}
    

External Meta-Syntax

The representation of meta-types, meta-objects, meta-object patterns, meta-substitutions and meta-contexts after parsing and data-dependent disambiguation.

In the following grammar, the metavariable:

• X ranges over meta-level variables
• \psi ranges over contexts
• g ranges over context schemas

      \begin{aligned}
      &\text{Meta-types} &U &\Coloneqq
      g
      \mid [\Psi \vdash A]
      \mid \#[\Psi \vdash A]
      \mid \$[\Psi ⊢ \Psi]
      \mid \$[\Psi \vdash\!\!\#\; \Psi]\\

      &\text{Meta-objects} &C &\Coloneqq
      [\Psi]
      \mid [\Psi \vdash M]
      \mid \$[\Psi \vdash \sigma]
      \mid \$[\Psi \vdash\!\!\#\; \sigma]\\

      &\text{Meta-substitutions} &\theta &\Coloneqq
      \char`\^
      \mid \theta, C / X\\

      &\text{Meta-contexts} &\Delta &\Coloneqq
      \char`\^
      \mid \psi
      \mid \Delta, X : U\\

      &\text{Schemas} &G &\Coloneqq
      g
      \mid G + G
      \mid \mathsf{some} [x_1 : A_1, x_2 : A_2, \dots, x_n : A_n] \;
      \mathsf{block} (y_1 : B_1, y_2 : B_2, \dots, y_m : B_m)\\

      &\text{Meta-object patterns} &C_p &\Coloneqq
      [\Psi_p]
      \mid [\Psi_p \vdash M_p]
      \mid \$[\Psi_p \vdash \sigma_p]
      \mid \$[\Psi_p \vdash\!\!\#\; \sigma_p]
      \end{aligned}
    

External Computation-Level Syntax

The representation of computation-level kinds, types, expressions and patterns after parsing and data-dependent disambiguation.

In the following grammar, the metavariable:

• x ranges over computation-level variables
• c ranges over computation-level constants
• X ranges over meta-level variables

      \begin{aligned}
      &\text{Computation-level kinds} &K &\Coloneqq
      \mathsf{ctype}
      \mid \Pi X {:} U. K
      \mid U \to K\\

      &\text{Computation-level types} &T, S &\Coloneqq
      \Pi X {:} U. S
      \mid T \to S
      \mid T_1 \times T_2 \times \dots \times T_n
      \mid U \\&&&
      \mid T \; C_1 \; C_2 \; \dots \; C_n\\

      &\text{Computation-level expressions} &E &\Coloneqq
      x
      \mid c
      \mid \mathsf{let} \; x = P \; \mathsf{in} \; E
      \mid \mathsf{impossible} \; E \\&&&
      \mid (E_1, E_2, \dots, E_n)
      \mid \;?
      \mid \;?\mathsf{id}
      \mid \_
      \mid E \; E_1 \; E_2 \; \dots \; E_n \\&&&
      \mid \mathsf{case} \; E \; \mathsf{of} \; P_1 \Rightarrow E_1 | P_2 \Rightarrow E_2 | \dots | P_n \Rightarrow E_n \\&&&
      \mid \mathsf{fn} \; x_1 \; x_2 \; \dots \; x_n \Rightarrow E
      \mid \mathsf{mlam} \; X_1 \; X_2 \; \dots \; X_n \Rightarrow E \\&&&
      \mid \mathsf{fun} \; P_1 \Rightarrow E_1 | P_2 \Rightarrow E_2 | \dots | P_n \Rightarrow E_n\\&&&
      \mid e .c\\

      &\text{Computation-level patterns} &P &\Coloneqq
      x
      \mid c
      \mid C_p
      \mid (P_1, P_2, \dots, P_n)
      \mid P \; P_1 \; P_2 \; \dots \; P_n\\

      &\text{Computation-level context} &\Gamma &\Coloneqq
      \char`\^
      \mid \Gamma, x : T
      \end{aligned}
    

Name resolution for computation-level patterns is intricate.

• All variables outside a pattern are not considered in scope.
• All free variables in patterns are considered pattern variables. This includes free meta-variables in contextual LF terms.
• Variables introduced by the meta-context occurring in a pattern are considered pattern variables. That is, the pattern meta-context applies to the branch expression.
• Bound variables in a pattern (bound by contextual LF abstractions or the meta-context) are not pattern variables.
• Patterns have to be linear, meaning that all pattern variables in a pattern-matching branch have to be unique.

External Harpoon Syntax

External Signature Syntax

Constants

Type Aliases

LF

Contextual LF

Meta-level

Computation-level

Harpoon

Signature

Common

Locations

LF

Contextual LF

Meta-Level

Computation-Level

Harpoon

Signature

Precedences

Explicit Arguments

Pretty-Printing