Surface syntax #

Programs have so far been written as abstract syntax: .div (.mul (.mul pi pi) (.mul hbar hbar)) (.mul (.mul (lit 2) mass) (.mul 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. Making the user write it would be both tedious and unsafe. 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 #