ast

Documentation

Index

• func Sprint(t Term) string
• type App
• type Fst
• type Global
• type Globals
• type Lam
• type Let
• type Level
• type Pair
• type Pi
• type RApp
• type RFst
• type RGlobal
• type RLam
• type RLet
• type RPair
• type RPi
• type RSigma
• type RSnd
• type RSort
• type RTerm
• type RVar
• type Sigma
• type Snd
• type Sort
  • func (s Sort) IsZeroLevel() bool
• type Term
  • func MkApps(t Term, us ...Term) Term
  • func Resolve(globals Globals, sc scope, r RTerm) (Term, error)
• type Var

Functions

func Sprint

func Sprint(t Term) string

Print a compact S-expression-like string for debugging.

Types

type App

type App struct {
	T Term
	U Term
}

App t u (application).

type Fst

type Fst struct{ P Term }

Fst and Snd projections.

type Global

type Global struct{ Name string }

Global refers to a globally named constant (post-elaboration).

type Globals

type Globals interface {
	// Has reports whether a global name exists.
	Has(name string) bool
}

type Lam

type Lam struct {
	Binder string
	Ann    Term // may be nil
	Body   Term
}

Lam (λ) abstraction with optional type annotation on the binder for printing.

type Let

type Let struct {
	Binder string
	Ann    Term // may be nil
	Val    Term
	Body   Term
}

Let x = v : A in body. (Convenience; kernel may desugar away later.)

type Level

type Level uint

Level represents a universe level (Type^u).

type Pair

type Pair struct {
	Fst Term
	Snd Term
}

Pair (a , b)

type Pi

type Pi struct {
	Binder string
	A      Term
	B      Term
}

Pi (Π) type with domain A and codomain B in a binder (x:A).B. We keep the binder name only for pretty-printing; kernel uses de Bruijn.

type RApp

type RApp struct{ T, U RTerm }

type RFst

type RFst struct{ P RTerm }

type RGlobal

type RGlobal struct{ Name string } // global symbol

type RLam

type RLam struct {
	Binder string
	Ann    RTerm
	Body   RTerm

} // Ann may be nil

type RLet

type RLet struct {
	Binder         string
	Ann, Val, Body RTerm

} // Ann may be nil

type RPair

type RPair struct{ Fst, Snd RTerm }

type RPi

type RPi struct {
	Binder string
	A, B   RTerm
}

type RSigma

type RSigma struct {
	Binder string
	A, B   RTerm
}

type RSnd

type RSnd struct{ P RTerm }

type RSort

type RSort struct{ U Level } // Type^U

type RTerm

type RTerm interface {
	// contains filtered or unexported methods
}

Raw terms carry user-chosen names before resolution.

type RVar

type RVar struct{ Name string } // free or bound

type Sigma

type Sigma struct {
	Binder string
	A      Term
	B      Term
}

Sigma (Σ) type.

type Snd

type Snd struct{ P Term }

type Sort

type Sort struct{ U Level }

Sort is a universe: Type^U.

func (Sort) IsZeroLevel

func (s Sort) IsZeroLevel() bool

IsZeroLevel returns true if this is Sort 0 (Type0).

type Term

type Term interface {
	// contains filtered or unexported methods
}

Term is the interface for all core terms.

func MkApps

func MkApps(t Term, us ...Term) Term

MkApps applies t to us left-associatively.

func Resolve

func Resolve(globals Globals, sc scope, r RTerm) (Term, error)

Resolve converts an RTerm to a core Term with respect to a scope and globals.

type Var

type Var struct{ Ix int }

Var is a de Bruijn variable: index (0 = innermost binder).