codegen

Documentation

Overview

Package codegen is the CODEGEN STRATUM: erased intermediate representation to target source, kept behind the Backend interface so a new deployment target is one plugin, not a fork. Dependent types are a build-time discipline; what deploys is the erasure — the shadow.

THE SHADOW RULE (CLAUDE.md): any optimization IR is built on erased, throwaway codegen output, NEVER on the immutable core/store. The core is the source of truth and identity; codegen mutates only its own shadow.

v1 ships one Backend (JavaScript); the interface exists so a later version adds targets without a rewrite.

Index

• type Backend
  • func Default() Backend
• type CtorSpec
• type DataSpec
• type DefSpec
• type IApp
• type IGlobal
• type ILam
• type ILet
• type IUnit
• type IVar
• type Ir
  • func Erase(t core.Tm, names map[core.Hash]string, typeRefs map[core.Hash]bool) Ir
• type JS
  • func (JS) Emit(p Program) (TargetSource, error)
  • func (JS) Target() string
• type NatSpec
• type Program
• type TargetSource

Types

type Backend

type Backend interface {
	// Target names the backend (e.g. "js").
	Target() string
	// Emit lowers an erased program to target source.
	Emit(p Program) (TargetSource, error)
}

Backend is the codegen stratum interface: it turns an erased Program into target source. One implementation ships per supported target.

func Default

func Default() Backend

Default returns the v1 backend.

type CtorSpec

type CtorSpec struct {
	Name  string
	Tag   int
	Arity int
}

CtorSpec is one constructor of an emitted datatype: its bound name, its 0-based tag, and the total number of curried parameters it takes (datatype parameters + its own arguments; parameters arrive erased).

type DataSpec

type DataSpec struct {
	ElimName  string
	NumParams int
	Ctors     []CtorSpec
	Rec       [][]bool
}

DataSpec is one datatype: its eliminator's bound name, the number of datatype parameters, and its constructors in declaration order. Rec mirrors core.CtorSig.Rec for building recursive calls in the eliminator.

type DefSpec

type DefSpec struct {
	Name string
	Body Ir
}

DefSpec is one emitted definition.

type IApp

type IApp struct {
	Fn  Ir
	Arg Ir
}

IApp is application.

type IGlobal

type IGlobal struct {
	Name string
}

IGlobal is a reference to a top-level definition, constructor, or eliminator, by the name the emitted program binds it to.

type ILam

type ILam struct {
	Name string
	Body Ir
}

ILam is a one-parameter function.

type ILet

type ILet struct {
	Name string
	Val  Ir
	Body Ir
}

ILet is a local binding.

type IUnit

type IUnit struct{}

IUnit is the erased token: every type, proof, and 0-quantity value.

type IVar

type IVar struct {
	Idx int
}

IVar is a bound variable (de Bruijn index, as in core).

type Ir

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

Ir is an erased term. Sealed like core.Tm.

func Erase

func Erase(t core.Tm, names map[core.Hash]string, typeRefs map[core.Hash]bool) Ir

Erase lowers elaborated, meta-free core to the erased IR. names maps a definition hash to its emitted global name; typeRefs holds the hashes that denote types at runtime (datatype formers), which erase to the unit token.

type JS

type JS struct{}

JS is the v1 backend: boring JavaScript. Everything is curried one-argument arrow functions; constructors build {tag, args} records; eliminators are switch-dispatch with recursive calls for the inductive hypotheses; the erased token is null. The output runs under node with no dependencies.

func (JS) Emit

func (JS) Emit(p Program) (TargetSource, error)

Emit lowers a program to a self-contained JavaScript source file.

func (JS) Target

func (JS) Target() string

type NatSpec

type NatSpec struct {
	Zero, Succ, ElimName string
}

NatSpec marks a datatype as the `builtin nat` binding (ergonomics rung 6): the backend may then compile it to native machine integers — zero/succ/the eliminator become arithmetic and a loop — instead of unary records. The core stays Peano and provable; only the shadow gets fast.

type Program

type Program struct {
	Datas []DataSpec
	Defs  []DefSpec
	// Nat, when non-nil, names the builtin-nat data group for fast-path
	// compilation.
	Nat *NatSpec
	// Main, when non-empty, names the definition whose value the emitted
	// program prints on run.
	Main string
}

Program is a whole erased program in definition order (acyclic, so the order is also the emission order).

type TargetSource

type TargetSource string

TargetSource is emitted source for some concrete backend target.