parser

Documentation

Overview

Package parser provides S-expression parsing for the HoTT kernel.

This package converts textual S-expression syntax into ast.Term values that can be type-checked and evaluated. It supports both core type theory constructs and cubical type theory extensions.

Parser Types

The main types are:

• SExprParser - stateful parser with position tracking
• ParseError - error type with position information

Key Functions

• ParseTerm - convenience function to parse a single term
• NewSExprParser - create parser for more control
• SExprParser.Parse - parse single term, ensure no trailing content
• ParseMultiple - parse a sequence of terms
• FormatTerm - serialize term back to S-expression

Syntax Overview

The parser accepts Lisp-style S-expressions:

; Comments start with semicolon
Type                       ; Universe Type₀
Type0, Type1, Type2        ; Universe shortcuts
(Sort 3)                   ; Universe Type₃
(Var 0)                    ; De Bruijn variable (0 = innermost)
0, 1, 2                    ; Variable shortcuts
name                       ; Global reference
(Pi x A B)                 ; Dependent function type
(Lam x body)               ; Lambda abstraction
(Lam x [A] body)           ; Lambda with type annotation
(App f x)                  ; Application
(Sigma x A B)              ; Dependent pair type
(Pair a b)                 ; Pair constructor
(Fst p), (Snd p)           ; Projections
(Let x A v body)           ; Let binding
(Id A x y)                 ; Identity type
(Refl A x)                 ; Reflexivity
(J A C d x y p)            ; J eliminator

Cubical Extensions

When cubical features are needed:

I, Interval                ; Interval type
i0, i1                     ; Interval endpoints
(IVar 0)                   ; Interval variable
(Path A x y)               ; Non-dependent path type
(PathP A x y)              ; Dependent path type
(PathLam i body)           ; Path abstraction
(PathApp p r)              ; Path application
(Transport A e)            ; Transport

Alternative Syntax

The parser accepts various alternative notations:

λ, \, fn        → Lam
Π, Pi, ->       → Pi
Σ, Sigma        → Sigma
×               → Sigma (non-dependent)

Error Handling

Parse errors include position information for diagnostics:

term, err := parser.ParseTerm(input)
if err != nil {
    if pe, ok := err.(*parser.ParseError); ok {
        fmt.Printf("Error at position %d: %s\n", pe.Pos, pe.Message)
    }
}

Round-Trip

Terms can be formatted back to S-expressions:

term, _ := parser.ParseTerm("(Pi x Type (Var 0))")
s := parser.FormatTerm(term)
// s == "(Pi x Type0 (Var 0))"

Note: Formatting may normalize some constructs (e.g., Type → Type0).

Package parser provides parsing utilities for the HoTT kernel.

This file documents the S-expression grammar for HoTT terms. The parser accepts a Lisp-like syntax where compound forms are parenthesized and atoms represent variables, constants, and special keywords.

Grammar (BNF Notation)

The following grammar specifies the complete syntax:

term         ::= simple | compound
simple       ::= number | keyword | global
compound     ::= '(' form-name term* ')'

number       ::= [0-9]+                    ; de Bruijn index
keyword      ::= 'Type' | 'Type0' | 'Type1' | 'Type2'
             |   'I' | 'Interval' | 'i0' | 'i1'
global       ::= identifier                ; any other atom
identifier   ::= [^()\s;]+                 ; non-whitespace, non-paren

form-name    ::= standard-form | cubical-form

Standard Type Theory Forms

standard-form ::= sort-form | var-form | global-form
              |   pi-form | lam-form | app-form
              |   sigma-form | pair-form | fst-form | snd-form
              |   let-form | id-form | refl-form | j-form

sort-form    ::= 'Sort' [number] | 'Type' [number]
var-form     ::= 'Var' number
global-form  ::= 'Global' identifier

pi-form      ::= ('Pi' | '->') binder term term
lam-form     ::= ('Lam' | 'λ' | '\\' | 'lambda') binder [term] term
app-form     ::= 'App' term term

sigma-form   ::= ('Sigma' | 'Σ') binder term term
pair-form    ::= 'Pair' term term
fst-form     ::= 'Fst' term
snd-form     ::= 'Snd' term

let-form     ::= 'Let' binder term term term
id-form      ::= 'Id' term term term
refl-form    ::= 'Refl' term term
j-form       ::= 'J' term term term term term term

binder       ::= identifier | '_'          ; optional, defaults to '_'

Cubical Type Theory Forms

cubical-form ::= ivar-form | path-form | pathp-form
             |   pathlam-form | pathapp-form | transport-form

ivar-form    ::= 'IVar' number
path-form    ::= 'Path' term term term
pathp-form   ::= 'PathP' term term term
pathlam-form ::= ('PathLam' | '<>') binder term
pathapp-form ::= ('PathApp' | '@') term term
transport-form ::= 'Transport' term term

Lexical Rules

Whitespace:

• Spaces, tabs, and newlines are ignored between tokens
• Whitespace separates atoms and is required between adjacent atoms

Comments:

• Line comments begin with ';' and extend to end of line
• Comments are treated as whitespace

Atoms:

• Any sequence of characters excluding '(', ')', whitespace, and ';'
• Numeric atoms parse as de Bruijn indices (Var)
• Keyword atoms parse as their corresponding term type
• All other atoms parse as Global references

De Bruijn Index Shorthand

Bare numeric atoms are parsed as de Bruijn indexed variables:

0        → Var{Ix: 0}    ; innermost bound variable
1        → Var{Ix: 1}    ; next outer binding
42       → Var{Ix: 42}   ; etc.

This provides concise notation for variable references.

Form Aliases

Several forms accept alternative keywords for convenience:

Pi:      'Pi', '->'
Lam:     'Lam', 'λ', '\', 'lambda'
Sigma:   'Sigma', 'Σ'
PathLam: 'PathLam', '<>'
PathApp: 'PathApp', '@'

Examples

Identity function on Type:

(Lam A (Lam x 0))
; or equivalently:
(λ A (λ x 0))

Dependent function type (A : Type) → A → A:

(Pi A Type (Pi _ 0 1))
; or equivalently:
(-> A Type (-> _ 0 1))

Pair of natural numbers:

(Pair zero (succ zero))

Path type Path Nat zero zero:

(Path Nat zero zero)

Path abstraction <i> x:

(PathLam i x)
; or equivalently:
(<> i x)

Transport along a type family:

(Transport (PathLam i A) e)

Identity type with reflexivity:

(Id Nat zero zero)
(Refl Nat zero)

J eliminator application:

(J A C d x y p)

Error Handling

Parse errors include position information:

type ParseError struct {
    Pos     int      // byte offset in input
    Message string   // description of error
}

Common error conditions:

• Unexpected EOF while parsing
• Missing closing parenthesis
• Unknown form name
• Invalid de Bruijn index (non-numeric where number expected)

Formatting

The FormatTerm function converts AST terms back to S-expression syntax, providing round-trip support. The output uses canonical form names (Sort, Pi, Lam, etc.) rather than aliases.

Package parser provides parsing utilities for the HoTT kernel.

Index

• func FormatTerm(t ast.Term) string
• func MustParse(input string) ast.Term
• func Normalize(input string) string
• func ParseMultiple(input string) ([]ast.Term, error)
• func ParseTerm(input string) (ast.Term, error)
• type ParseError
  • func (e *ParseError) Error() string
• type SExprParser
  • func NewSExprParser(input string) *SExprParser
  • func (p *SExprParser) Parse() (ast.Term, error)

Functions

func FormatTerm

func FormatTerm(t ast.Term) string

FormatTerm formats an AST term as an S-expression string.

func MustParse

func MustParse(input string) ast.Term

MustParse parses a term or panics.

func Normalize

func Normalize(input string) string

Normalize removes extra whitespace and standardizes formatting.

func ParseMultiple

func ParseMultiple(input string) ([]ast.Term, error)

ParseMultiple parses multiple terms separated by whitespace.

func ParseTerm

func ParseTerm(input string) (ast.Term, error)

ParseTerm parses the input string as an AST term.

Types

type ParseError

type ParseError struct {
	Pos     int
	Message string
}

ParseError represents a parsing error with position information.

func (*ParseError) Error

func (e *ParseError) Error() string

type SExprParser

type SExprParser struct {
	// contains filtered or unexported fields
}

SExprParser parses S-expressions into AST terms.

func NewSExprParser

func NewSExprParser(input string) *SExprParser

NewSExprParser creates a new S-expression parser.

func (*SExprParser) Parse

func (p *SExprParser) Parse() (ast.Term, error)

Parse parses the input and returns an AST term.