Concrete syntax for expressions

Surface syntax for the expressions of the imperative probabilistic language; see syntax-ideas.md for design notes.

Expressions — GaudiExpr[ e ]

Wraps a Lean expression e as a program expression. Inside, the $ sigil reads program variables:

• $x — the value of program variable / lens x;
• $(e) — the value of an arbitrary lens-valued term e.

e.g. GaudiExpr[ $a + $b * 2 ]. Every expression position in a statement is already an GaudiExpr, so $ may be used directly there (see ProgramSyntax.lean).

§x is a second spelling of $x, with the same meaning. It exists because it can be printed: $x parses as a Lean antiquotation node, and antiquotation nodes cannot be pretty-printed ($a + 1 fails to format), so §x is what the delaborators emit.

Ambient current state + variable evaluation

An expression of value type T is a Getter T ProgramState. Inside the body we make the current state available via the typeclass CurrentState, so a program variable x (a lens/getter) can be read as a plain value with eval x. eval accepts both global variables (into the globals, a VariableAssignment) and full-current-state variables (into ProgramState, e.g. locals lifted with Lens.intoLocal); dispatch is on the concrete type of the argument (see Evaluatable).

class GaudisCrypt.CurrentState : Type 1

The ambient current state.

• state : ProgramState

class GaudisCrypt.Evaluatable (X : Type u) (T : outParam Type) : Type (max 1 u)

Anything that can be read to a value T in the ambient CurrentState: program variables (lenses/getters into the globals VariableAssignment, or into the full ProgramState), and anything users later add instances for. Dispatch is on the concrete type X of the argument, so resolution is never stuck on a metavariable.

• eval : ProgramState → X → T

def GaudisCrypt.eval {X : Type u} {T : Type} [Evaluatable X T] [cs : CurrentState] (x : X) : T

User-facing variable read in the ambient CurrentState.

Equations

• §x = GaudisCrypt.Evaluatable.eval GaudisCrypt.CurrentState.state x

@[implicit_reducible]

instance GaudisCrypt.instEvaluatableGetterVariableAssignment {T : Type} : Evaluatable (Getter T VariableAssignment) T

The four container shapes, dispatched directly on the argument type. (No Lens → Getter forwarder: it would overlap these, so we spell out all four.)

Equations

• GaudisCrypt.instEvaluatableGetterVariableAssignment = { eval := fun (cs : GaudisCrypt.ProgramState) (x : GaudisCrypt.Getter T GaudisCrypt.VariableAssignment) => x.get cs.globals }

@[implicit_reducible]

instance GaudisCrypt.instEvaluatableGetterProgramState {T : Type} : Evaluatable (Getter T ProgramState) T

Equations

• GaudisCrypt.instEvaluatableGetterProgramState = { eval := fun (cs : GaudisCrypt.ProgramState) (x : GaudisCrypt.Getter T GaudisCrypt.ProgramState) => x.get cs }

@[implicit_reducible]

instance GaudisCrypt.instEvaluatableLensVariableAssignment {T : Type} : Evaluatable (Lens T VariableAssignment) T

Equations

• GaudisCrypt.instEvaluatableLensVariableAssignment = { eval := fun (cs : GaudisCrypt.ProgramState) (x : GaudisCrypt.Lens T GaudisCrypt.VariableAssignment) => x.get cs.globals }

@[implicit_reducible]

instance GaudisCrypt.instEvaluatableLensProgramState {T : Type} : Evaluatable (Lens T ProgramState) T

Equations

• GaudisCrypt.instEvaluatableLensProgramState = { eval := fun (cs : GaudisCrypt.ProgramState) (x : GaudisCrypt.Lens T GaudisCrypt.ProgramState) => x.get cs }

Reduction lemmas (so denotations compute)

simp reduces all four cases (global/full × getter/lens) to a plain .get read.

@[simp]

theorem GaudisCrypt.eval_getter_global {T : Type} [cs : CurrentState] (x : Getter T VariableAssignment) : §x = x.get CurrentState.state.globals

@[simp]

theorem GaudisCrypt.eval_getter_full {T : Type} [cs : CurrentState] (x : Getter T ProgramState) : §x = x.get CurrentState.state

@[simp]

theorem GaudisCrypt.eval_lens_global {T : Type} [cs : CurrentState] (x : Lens T VariableAssignment) : §x = x.get CurrentState.state.globals

@[simp]

theorem GaudisCrypt.eval_lens_full {T : Type} [cs : CurrentState] (x : Lens T ProgramState) : §x = x.get CurrentState.state

Sigil syntax for expressions

The $ sigil is parsed by Lean as a (pseudo) antiquotation node; we intercept those nodes inside the GaudiExpr[ ] macro and rewrite $e to eval e.

$x ↦ eval x (variable reference) $(e) ↦ eval e (arbitrary lens-valued term as a variable) GaudiExpr[ e ] wraps an expression body e into a Getter _ ProgramState, making the ambient CurrentState available inside e.

def GaudisCrypt.«termGaudiExpr[_]» : Lean.ParserDescr

Equations

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

The printable sigil §

$x is an antiquotation node, which Lean's formatter cannot print (it fails inside infix operators, so $a + 1 would be unprintable). §x means exactly the same — it expands to eval x just like $x does — but is an ordinary piece of syntax, so it both parses and prints. The eval unexpander turns every variable read back into it.

def GaudisCrypt.«term§__» : Lean.ParserDescr

§x — the value of program variable / lens x in the ambient CurrentState; the printable spelling of $x.

Equations

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

def GaudisCrypt.unexpandEval : Lean.PrettyPrinter.Unexpander

Equations

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