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;
let x := e; / have h : P := prf; / letI …; / haveI …; — an ordinary Lean binder (not a program statement), scoping over the statements that follow it in the same block.

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

The sequence may start with var x : T, …; lines, GaudiProg[ var i : Nat; i <- 0; … ], which declare local variables exactly as in a proc (below): each name stands for its slot in the locals of the ProgramState.

Example (a b c : Lens Nat VariableAssignment globals, 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). A binder may name several variables of one type, (x y : T, …), and stands for the same list as writing them out one by one — so may a local-variable binder, and a module parameter after using;
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 (var u w : V; declares two). A parameter or local x : T stands for the slot localVarLens "x" T of the locals; a fresh local starts at an unspecified value (VariableAssignment.init), so it should be written before it is read;
a body of statements ending in return e.

A let/have/letI/haveI statement in the body scopes over the rest of the body and over return e. Body and return value are two separate fields of ProcedureWithHoles, so the binders on the body's spine — those of the procedure's own block, each carrying the rest of it — are repeated around the return value. A binder nested inside an if/while/ block, on the other hand, ends with that block and does not reach 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.

An argument of any of these may be named — procsig (h : G, m : F) -> Bool — which a ProcedureSignature cannot record and which is therefore dropped, except by moduletype, which keeps the names in the @[gaudiProcParamNames] attribute. See the Signature argument lists section below.

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. 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 ProgramState by liftLens — so a global Lens a VariableAssignment may be written bare and is lifted with Lens.intoGlobal, and a local variable (a lens into ProgramState) is used as it is.

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)
let x := e;   have h : P := prf;   letI …;   haveI …;   -- a Lean binder

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

The four binder forms are not StmtWithHoles constructors: they are the ordinary Lean term binders. Each carries the statements it scopes over as a nested statement list, so let x := e; followed by more statements is a single gaudi_stmt holding them, and the binder is visible exactly there — in the statements that follow it in its own block, and nowhere else.

The `@[gaudiProcParamNames]` attribute #

A ProcedureSignature records parameter types only, so the names written in a moduletype field or a module procedure would be lost. They are kept in this attribute instead, on the declaration that names the procedure — a moduletype accessor MT.f, a module's procedure module X.f and its X.f.procedure — so that notation about a procedure can bind its parameters by name even when the procedure itself is abstract (a field of an arbitrary module of a declared module type has no body to read names off).

The attribute's syntax has to be declared under Lean.Parser.Attr — that is the namespace Lean strips to get an attribute's name from its syntax kind — and an initialize block cannot be used in the file that declares it, which is why both live here rather than next to the commands that write them (ModuleSyntax.lean).

Concrete syntax for programs and procedures #

Statements / programs — GaudiProg[ … ] #

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

Procedure types and signatures #

Printing #

Syntax for programs (StmtWithHoles) #

The @[gaudiProcParamNames] attribute #

Signature argument lists — proc_arg #

Procedure type syntax #

Procedure signature syntax #

Printing #

Program variables #

Statements / programs — `GaudiProg[ … ]` #

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

Syntax for programs (`StmtWithHoles`) #

The `@[gaudiProcParamNames]` attribute #

Signature argument lists — `proc_arg` #