Surface syntax #

Programs have so far been written as abstract syntax: .div (.mul (.mul (.mul pi pi) hbar) hbar) (.mul (.mul (.mul (lit 2) mass) width) width). That is a faithful way to describe a calculus and a terrible way to write physics.

This file adds a bracket ⟪ … ⟫ with the usual arithmetic notation inside, so the same term reads

⟪ (pi * pi * hbar * hbar) / (2 * mass * width * width) ⟫

Identifiers inside the bracket are ordinary Lean names bound to terms, so the notation composes with definitions rather than replacing them. It is a convenience layer over Tm and nothing more: no separate parser, no separate AST, and every guard elsewhere still checks the same core terms.

Elaboration, and where `convert` gets its annotation #

Tm.convert carries the unit it converts from, because the evaluator must recover the factor from the term and the unit environment alone. Writing it by hand would be tedious, though a wrong one is rejected: HasTy.convert demands the subject at exactly Q u. elabConvert supplies it by running the verified checker: it checks the subject, reads the unit off the type it derived, and builds the annotated term.

This is what makes conversion-as-a-core-constructor tenable. elabConvert returns the elaborated term together with its derivation, so a surface in cannot produce a core term the checker would reject: the annotation is not merely machine-generated but machine-justified.

The bracket #

source

def LambdaS.lamS.quot :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lean.Parser.Category.lamS :

Elaborating a conversion #

source

def LambdaS.elabConvert {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {j k : ℕ} (Δ : DCtx D j k) (Γ : Ctx B D j k) (e : Tm B D j k) (v : UExp B k) :

Option ((e' : Tm B D j k) × HasTy Δ Γ e' (Ty.Q v))

Insert a conversion's source annotation by type inference.

The paper abbreviates a conversion to e in v; the core needs convert e u v with u the unit of e. This runs the verified checker to find it, so the annotation is derived rather than trusted, and convert's own typing rule still checks it.

Equations

LambdaS.elabConvert Δ Γ e v = match LambdaS.check Δ Γ e with | some ⟨LambdaS.Ty.Q u, d⟩ => if h : LambdaS.SameDim Δ u v then some ⟨e.convert u v, d.convert h⟩ else none | x => none

Instances For

source

theorem LambdaS.elabConvert_isSome {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {v : UExp B k} :

(elabConvert Δ Γ e v).isSome = true ↔ ∃ (u : UExp B k), infer Δ Γ e = some (Ty.Q u) ∧ SameDim Δ u v

Elaboration succeeds exactly when the surface syntax is meaningful: the subject is a scalar, and its unit shares the target's dimension.

That is the whole specification, in both directions. There is no companion theorem saying the elaborated term typechecks, because elabConvert returns the derivation: a surface in cannot produce a core term the checker would reject.

Documentation

LambdaS.Notation

Surface syntax #

Elaboration, and where `convert` gets its annotation #

The bracket #

Elaborating a conversion #

Surface syntax #

Elaboration, and where convert gets its annotation #

The bracket #

Elaborating a conversion #

Elaboration, and where `convert` gets its annotation #