Concrete syntax for programs and procedures

Surface syntax for the imperative probabilistic language (StmtWithHoles / ProcedureWithHoles from GaudisCrypt). Expression syntax (GaudiExpr[ ] and the $ sigil) is in ExpressionSyntax.lean; module syntax is in ModuleSyntax.lean. See syntax-ideas.md for design notes.

Statements / programs — GaudiProg[ … ]

A ;-terminated sequence of statements. The statement forms are:

• skip;
• x <- e; — assignment;
• a, b <- e; / (a, b) <- e; — tuple assignment (the parentheses are optional);
• x <$ e; — sample x from distribution e;
• x <- call p (e₁, …, eₙ); — call procedure p, storing the result in x;
• call p (e₁, …, eₙ); — call p, discarding the result;
• if (e) { … } else { … } — the else branch is optional;
• while (e) { … }
• { … } — a nested block.

The argument list ( … ) of a call is always required (write () for no arguments).

Example (a b c : Lens Nat State, inc : Procedure …):

GaudiProg[
  a <- $a + 1;
  b, c <- ($a, $a * 2);
  if ($a == 0) { a <- 1; } else { skip; }
  while ($b == 0) { b <- $b + 1; }
  a <- call inc ($a);
]

Procedures — proc (…) [uses (…)] [: R] { … }

A procedure term:

proc (x : T, y : U) uses (A : (Nat) → Bool, B : (Bool) → Nat) : R {
  var u : V, w : W;     -- zero or more `var …;` lines of local variables
  <statements>
  return e
}

• parameters (x : T, …) (possibly none);
• an optional uses (…) clause declaring holes (abstract sub-procedures), each written name : (T₁, …, Tₙ) → R. Inside the body a hole is invoked with the ordinary call A (…) syntax — A resolves to a hole when it is one of the declared names, and to a concrete procedure otherwise;
• an optional return type : R (inferred from return e when omitted);
• local variables via one or more var name : T, …; lines;
• a body of statements ending in return e.

Procedure types and signatures

• proctype (T, U, …) -> W — the type of a closed procedure;
• proctype (T, …) -> W uses ((T₁,…) → R, …) — the type of a procedure with holes;
• procsig (T, U, …) -> W — the bare ProcedureSignature.

-> is used (rather than :) so these nest inside type ascriptions without extra parentheses; they also pretty-print back into this form.

Printing

Statements, procedures and the two type forms all print in this syntax again, and do so round-trip faithfully: parsing what was printed gives the same term back. A variable read prints as §x, the printable spelling of $x. See the Printing section at the end of this file for the delaborators and for the two places where the printed form differs from what one would write by hand.

e.g. proctype (Nat, Bool) -> Nat, proctype (Nat) -> Nat uses ((Nat) → Bool, (Bool) → Nat), procsig (Nat, Bool) -> Nat. Note Procedure (procsig (Nat) -> Nat) = proctype (Nat) -> Nat.

The module type of a procedure, procmod (…) -> R, is in ModuleSyntax.lean.

Syntax for programs (StmtWithHoles)

Statement syntax over StmtWithHoles h l. Each expression position (assignment RHS, sampling distribution, if/while condition) is wrapped with GaudiExpr[ ] so the $x sigil works. An l-value (assignment/sample LHS) is a lens, lifted into the current full state State × l by liftLens — so a global Lens a State may be written bare and is lifted with .ofst.

Surface forms (gaudi_stmt):

skip;
x <- e;                       -- assignment
a, b <- e;   (a,b) <- e;      -- tuple l-value (parens optional), via `Lens.pair`
x <$ e;                       -- sampling (e : a distribution expression)
x <- call p (e₁, …, eₙ);      -- procedure call, result stored in `x`
call p (e₁, …, eₙ);           -- procedure call, result discarded (Lens.throwaway)
if (e) { … } else { … }       -- the `else` branch is optional
while (e) { … }
{ … }                         -- a block (sequence)

The call argument list ( … ) is always required (even ()); the arguments form a tuple matching the callee's ParamType. (hole is still deferred.)

class GaudisCrypt.LiftLens [ProgramSpec] (S M : Type) : Type (max 1 u_1)

Lift a program variable used as an l-value into a lens on the full current state State × S. Dispatch is on the lens's container M: a global lens (M = State) is lifted with .ofst, a full-state lens (M = State × S) is kept as-is. The content type A is deliberately not a class parameter — resolution then only needs M (always concrete from the argument), and the result's content unifies with the expected type as an ordinary, postponable constraint. (That is what lets a call result l-value resolve even before the callee's sig is known.)

• lift {A : Type} : Lens A M → Setter A (ProcedureState S)

@[implicit_reducible]

instance GaudisCrypt.instLiftLensState [ProgramSpec] {S : Type} : LiftLens S State

Equations

• GaudisCrypt.instLiftLensState = { lift := fun {A : Type} (x : GaudisCrypt.Lens A GaudisCrypt.State) => (GaudisCrypt.ProcedureState.globalL.chain x).toSetter }

@[implicit_reducible]

instance GaudisCrypt.instLiftLensProcedureState [ProgramSpec] {S : Type} : LiftLens S (ProcedureState S)

Equations

• GaudisCrypt.instLiftLensProcedureState = { lift := fun {A : Type} (x : GaudisCrypt.Lens A (GaudisCrypt.ProcedureState S)) => x.toSetter }

def GaudisCrypt.liftLens [ProgramSpec] {S A M : Type} [LiftLens S M] (x : Lens A M) : Setter A (ProcedureState S)

User-facing l-value lift; S, the container M, and the content A are inferred. The result is a Setter (l-values only ever set).

Equations

• GaudisCrypt.liftLens x = GaudisCrypt.LiftLens.lift x

def GaudisCrypt.«term[lvalRaw|_]» : Lean.ParserDescr

The raw (un-lifted) lens for an l-value: a tuple (x, y, …) becomes a nested Lens.pair; a single term is itself. Pairing needs the components to be disjoint lenses in the same container — the disjoint instance is resolved at the concrete lenses, so (a, b) requires disjoint a b.

Equations

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

def GaudisCrypt.«term[lvalRawList|_]» : Lean.ParserDescr

Raw nested Lens.pair of a comma-list of l-value components (each component may itself be a paren-tuple, handled by [lvalRaw|]).

Equations

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

def GaudisCrypt.«term[lval|_]» : Lean.ParserDescr

An l-value lifted into the current full state State × S. Accepts a single lens, a parenthesised tuple (a, b), or a bare comma-list a, b (top-level parens optional) — all interpreted via Lens.pair.

Equations

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

def GaudisCrypt.gaudi_stmt.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.gaudi_stmt : Category

Equations

• Lean.Parser.Category.gaudi_stmt = { }

def GaudisCrypt.«gaudi_stmt_Skip;» : Lean.ParserDescr

Equations

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

def GaudisCrypt.«gaudi_stmt__<-_;» : Lean.ParserDescr

Equations

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

def GaudisCrypt.«gaudi_stmt__<$_;» : Lean.ParserDescr

Equations

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

def GaudisCrypt.callStore : Lean.ParserDescr

Equations

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

def GaudisCrypt.callVoid : Lean.ParserDescr

Equations

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

def GaudisCrypt.holecallStore : Lean.ParserDescr

Equations

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

def GaudisCrypt.holecallVoid : Lean.ParserDescr

Equations

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

def GaudisCrypt.«gaudi_stmt_If(_){__}Else{__}» : Lean.ParserDescr

Equations

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

def GaudisCrypt.«gaudi_stmt_If(_){__}» : Lean.ParserDescr

Equations

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

def GaudisCrypt.«gaudi_stmt_While(_){__}» : Lean.ParserDescr

Equations

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

def GaudisCrypt.«gaudi_stmt_{__}» : Lean.ParserDescr

Equations

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

def GaudisCrypt.«term[gstmt|_]» : Lean.ParserDescr

Translate one statement to a StmtWithHoles term.

Equations

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

def GaudisCrypt.«term[gseq|_]» : Lean.ParserDescr

Translate a statement sequence (fold with seq; empty ↦ skip).

Equations

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

def GaudisCrypt.«termGaudiProg[__]» : Lean.ParserDescr

Top-level program bracket.

Equations

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

def GaudisCrypt.proc_binder.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.proc_binder : Category

Equations

• Lean.Parser.Category.proc_binder = { }

def GaudisCrypt.«proc_binder_:_» : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.hole_binder : Category

A hole declaration A : (T₁, …, Tₙ) → R (an abstract procedure with no locals).

Equations

• Lean.Parser.Category.hole_binder = { }

def GaudisCrypt.hole_binder.quot : Lean.ParserDescr

Equations

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

def GaudisCrypt.«hole_binder_:(_)→_» : Lean.ParserDescr

Equations

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

partial def GaudisCrypt.rewriteHoles (holeNames : List Lean.Name) (s : Lean.TSyntax `gaudi_stmt) : Lean.MacroM (Lean.TSyntax `gaudi_stmt)

Rewrite call A (…) → holecall A (…) for every callee A whose name is a hole (recursing into if/while/block bodies); everything else is left untouched.

def GaudisCrypt.«termProc(_)_Uses(_):_{_Var_;__Return_;_}» : Lean.ParserDescr

Equations

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

Procedure type syntax

proctype (T, U, V) -> W is the type Procedure { params := [T, U, V], ret := W }, and proctype (…) -> W uses ((A₁,…) → R₁, …) is the corresponding ProcedureWithHoles, whose hole context is built from the listed (nameless) procedure signatures. (Uses -> rather than : so it needs no extra parentheses inside a type ascription.)

def GaudisCrypt.hole_sig.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.hole_sig : Category

A nameless hole signature (T₁, …, Tₙ) → R inside a proctype … uses (…) clause.

Equations

• Lean.Parser.Category.hole_sig = { }

def GaudisCrypt.«hole_sig(_)→_» : Lean.ParserDescr

Equations

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

def GaudisCrypt.«termProctype(_)→->_Uses(_)» : Lean.ParserDescr

Equations

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

proctype unexpanders. A signature already prints as procsig (…) -> … (the ProcedureSignature.mk unexpander), so we just rewrite Procedure (procsig …) and ProcedureWithHoles … (procsig …) to proctype …. Parameter lists are read off the raw procsig node (a category quotation can't match the sepBy inside the parens).

def GaudisCrypt.procsigParts? (s : Lean.Syntax) : Option (Lean.Syntax.TSepArray `term "," × Lean.TSyntax `term)

If s is a procsig ( … ) -> … node, return its parameter list and return type. (Not private: ModuleSyntax.lean unexpands procmod with it.)

Equations

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

def GaudisCrypt.unexpandProcedure : Lean.PrettyPrinter.Unexpander

Equations

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

def GaudisCrypt.unexpandProcedureWithHoles : Lean.PrettyPrinter.Unexpander

Equations

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

Procedure signature syntax

procsig (T, U, V) -> W is the bare ProcedureSignature.mk [T, U, V] W (the same surface form as proctype, minus the holes — a signature has none). By construction Procedure (procsig …) = proctype …. The unexpander is on ProcedureSignature.mk, so any signature with a literal parameter list prints back as procsig (…) -> ….

def GaudisCrypt.«termProcsig(_)→->_» : Lean.ParserDescr

Equations

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

def GaudisCrypt.unexpandProcSig : Lean.PrettyPrinter.Unexpander

Equations

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

Printing

Delaborators that render elaborated terms back into the surface syntax above: a procedure built by proc prints as proc (…) uses (…) : R { … }, and a statement prints as GaudiProg[ … ] (with variable reads as the §x sigil, the printable spelling of $x).

Printing is round-trip faithful: parsing what was printed yields the same term back (ProgramSyntaxTest.lean checks this by printing, re-parsing and re-elaborating). Hence the two places where the printed form deviates from what one would write by hand:

• a seq in the left position of a seq is printed as a block { … }, since re-parsing a flat sequence would re-associate it;
• a hole call prints as call A (…) only inside the proc that declares A in its uses clause (which is where the macro turns call back into a hole call), and as the internal holecall n (…) anywhere else.

Whenever a term does not fit the surface syntax — a Getter that is not of the shape GaudiExpr[ ] builds, an l-value that is not a lifted lens, lets that proc would not have generated — the delaborators fail and Lean falls back to its default output. They also step aside under pp.explicit and set_option pp.notation false.