DONE Grammar Specification

The grammar is composed of production rules with syntactic meaning and attached typing rules conveying semantic information about the language.

The core data structures are defined in src/logic/grammar/mod.rs.

Production Rules

Production rules define the syntactic structure of the language. Each rule maps a nonterminal to one or more alternative right-hand sides.

Nonterminal(rule_name) ::= symbol₁ symbol₂ ... | alternative₂ | ...

Bindings are resolved via grammar paths during type-checking. See src/logic/binding/grammar.rs for the path construction algorithm.

Epsilon Productions

An epsilon production represents an empty alternative, written as ε.

// Optional tail matching zero or more Terms
ProgramTail ::= Term ProgramTail | ε

Typing Rules

Typing rules attach semantic information to productions using an inference-rule format.

premise₁, premise₂, ...
------------------------ (rule_name)
conclusion

The rule name in parentheses must match a (rule_name) annotation on a production.

Premises

Premises express conditions for rule application.

Conclusions

Conclusions specify the rule’s result:

Checking mode (▷) is not implemented as a conclusion; use the check premise Γ ▷ e instead.

Meta-Variables

A meta-variable (written ?A, ?B, etc.) is a placeholder unified during type checking, allowing rules to express polymorphic constraints.

// ?A must unify with both the function's domain and the argument's type.
Γ ⊢ f : ?A → ?B, Γ ⊢ e : ?A
-------------------------------- (app)
?B

Context Operations

The typing context Γ maps variable names to types:

• Γ(x): Look up type of variable x.
• Γ[x:τ]: Extend context with binding x:τ.
• x ∈ Γ: Check if x is bound in context.

Type Syntax

Types in typing rules follow this syntax:

Example: Simply-Typed Lambda Calculus

A complete specification for STLC from examples/stlc.auf:

// Identifier (supports Unicode)
Identifier ::= /[A-Za-z_][A-Za-z0-9]*/

// Variables with var typing rule
Variable(var) ::= Identifier[x]

TypeName ::= /[A-Za-z0-9_τ₁₂₃₄₅₆₇₈₉₀]+/

// Base types (parentheses are literals, hence quoted)
BaseType ::= TypeName | '(' Type ')'

// Function types (right-associative)
AtomicType ::= BaseType | '(' Type ')'
FunctionType ::= AtomicType '->' Type
Type ::= AtomicType | FunctionType

// Lambda abstraction (dot is a literal)
Lambda(lambda) ::= 'λ' Identifier[a] ':' Type[τ] '.' Expression[e]

// Atomic expressions
AtomicExpression ::= Variable | '(' Expression ')' | Lambda

// Applications (left-associative)
Application(app) ::= Expression[l] AtomicExpression[r]

// Expressions (start symbol)
Expression ::= AtomicExpression |  Application

// Typing Rules
x ∈ Γ
----------- (var)
Γ(x)

Γ[a:τ] ⊢ e : ?B
--------------------------- (lambda)
τ → ?B

Γ ⊢ l : ?A → ?B, Γ ⊢ r : ?A
--------------------------------- (app)
?B

Source Files