Diane

The Playground
- Instructions
- Keyboard Shortcuts
Syntax
Semantics

Diane is a toy stack-oriented language with dynamic scoping. It's not pretty or all that interesting, but it's simple enough to present the syntax and semantics in a straightforward way (and to build a reasonable playground for it).

Diane was born out of a need to visualize evaluation. During the spring (2024), I co-taught a course on programming languages in which we often used stack-oriented languages to motivate and demonstrate operational semantics. I worked through step-by-step evaluations on the board often enough to want a process for doing it which is automatic and interactive, along the same lines as the Python Tutor for Composing Programs.

Disclaimer. This page is not a tutorial, just a description of the language and playground.

The Playground

The primary goal of this project was to build a playground (in Elm) for toying with Diane programs. The playground consists of an editor window for writing programs, a visualization window for seeing how the stack and environment change over the course of evaluation, and a console window for seeing intermediate print statements and error messages.

The playground can also be embedded:

We take advantage of this below to highlight features of the semantics.

Partly out of laziness, partly out of a general bent towards minimal interfaces, there are no instructions for using the playground within the playground itself, so I've included them here.

Instructions

The step button consumes a single command of the program in the editor window and updates the stack and environment accordingly.
The run button consumes as much of the program as possible until
- the entire program is consumed
- there is an error
- the evaluation times out
The undo button reverses a step taken by pressing either the step button or the run.
The reset button resets the program state to its initial state, clearing the undo history.
The save button sets the program in the editor window to be the program of the initial state. This also clears the undo history.¹
The clear button in the console window clears the messages printed there.²

Keyboard Shortcuts

\	step
ALT	run
`	undo

It's possible to step through a program while writing it using the above keyboard shortcuts. In most cases you can also hold down the key to rapidly step through a program, providing a make-shift animation mechanism.

Syntax

The following is a simple EBNF Grammar describing a Diane program. In short, a program is a sequence of whitespace-separated commands.

<program>  ::= { <command> }
<body>     ::= '{' <program> '}'
<command>  ::= <int> | 'drop' | 'swap' | 'dup' | 'rot'
             | '+' | '-' | '*' | '/' | '%' | '=' | '<'
             | 'def' <ident> <body> | '#' <ident>
             | '@' <ident> | '[' | ']'
             | '?' <body> 'else' <body> | 'while' <body> 'do' <body>
<int>      ::= ℤ
<ident>    ::= ALL_CAPS_SNAKE

Semantics

We take a value (𝕍) to be a integer (ℤ) or a program representing a subroutine (ℙ).³ A configuration, written ( S, E, P ), is made up of a stack of integers (S), an environment consisting of a list of collections identifier-value bindings (E), and a program as given by the above grammar (P). The operational semantics of Diane are given by the reduction rules below.

Notation for Environments

⟨⟩	empty collection of bindings
𝒢	global bindings
L · E	E with (shadowing) local bindings L
E[X ↦ A]	E with X bound to the value A (in topmost local bindings)
X ∈ E	X is bound in E
E[X]	the value to which X is bound in E (searched for top down)
E/X	E with any binding of X removed

Stack Manipulation

Several commands are dedicated to manipulating the stack. We can

push an integer onto the stack
drop the top element off the stack
swap the top two elements on the stack
dup-licate the top element on the stack
rot-ate the top three elements on the stack

In the case that there aren't enough integers on the stack to perform a given operation, a stack underflow error message is printed to the console.

There is also an unofficial command for print-ing the top element of the stack and removing it. See the example below.⁴


               𝑘 ∈ ℤ
────────────────────────────────── ( push )
( S, E, k P ) ⟶ ( 𝑘 :: S, E, P )


───────────────────────────────────── ( drop )
( 𝑛 :: S, E, drop P ) ⟶ ( S, E, P )


─────────────────────────────────── ( dropErr )
( ⊥, E, drop P ) ⟶ StackUnderflow


──────────────────────────────────────────────────── ( swap )
( 𝑚 :: 𝑛 :: S, E, swap P) ⟶ ( 𝑛 :: 𝑚 :: S, E, P )


──────────────────────────────────────── ( swapErr₁ )
( 𝑛 :: ⊥, E, swap P ) ⟶ StackUnderflow


─────────────────────────────────── ( swapErr₀ )
( ⊥, E, swap P ) ⟶ StackUnderflow


──────────────────────────────────────────────────── ( dup )
( 𝑛 :: S, E, dup P ) ⟶ ( 𝑛 :: 𝑛 :: S, E, P )


─────────────────────────────────── ( dupErr₀ )
( ⊥, E, dup P ) ⟶ StackUnderflow


──────────────────────────────────────────────────────────── ( rot )
( 𝑙 :: 𝑚 :: 𝑛 :: S, E, rot P ) ⟶ ( 𝑚 :: 𝑛 :: 𝑙 :: S, E, P )


──────────────────────────────────────────── ( rotErr₂ )
( 𝑚 :: 𝑛 :: S, E, rot P ) ⟶ StackUnderflow


─────────────────────────────────────── ( rotErr₁ )
( 𝑛 :: ⊥, E, rot P ) ⟶ StackUnderflow


─────────────────────────────────── ( rotErr₀ )
( ⊥, E, rot P ) ⟶ StackUnderflow

The following is a small example program using these commands. Press the step button to see how the stack changes as each command is consumed and evaluated. Note that the last command cannot be consumed because there are no integers on the stack to duplicate. Attempting to evaluate this command results in a stack underflow error message.

Arithmetic and Comparisons

The commands in this section are used to operate on the integers on the stack. We can

(+) add
(-) subtract
(*) multiply
(/) divide
(%) determine the modulus
(=) check for equality
(<) check for less-than

As above, if there aren't enough integers on the stack to perform an operation, a stack underflow error message is printed. An error may also occur when trying to divide by zero.


────────────────────────────────────────────────── ( add )
( 𝑚 :: 𝑛 :: S, E, + P ) ⟶ ( 𝑚 ＋ 𝑛 :: S, E, P )


───────────────────────────────────── ( addErr₁ )
( 𝑛 :: ⊥, E, + P ) ⟶ StackUnderflow


──────────────────────────────── ( addErr₀ )
( ⊥, E, - P ) ⟶ StackUnderflow


  ─────────────────────────────────────────────── ( sub )
( 𝑚 :: 𝑛 :: S, E, - P ) ⟶ ( 𝑚 ─ 𝑛 :: S, E, P )


───────────────────────────────────── ( subErr₁ )
( 𝑛 :: ⊥, E, - P ) ⟶ StackUnderflow


──────────────────────────────── ( subErr₀ )
( ⊥, E, - P ) ⟶ StackUnderflow


───────────────────────────────────────────────── ( mul )
( 𝑚 :: 𝑛 :: S, E, * P ) ⟶ ( 𝑚 × 𝑛 :: S, E, P )


───────────────────────────────────── ( mulErr₁ )
( 𝑛 :: ⊥, E, * P ) ⟶ StackUnderflow


──────────────────────────────── ( mulErr₀ )
( ⊥, E, * P ) ⟶ StackUnderflow


                       n ≠ 0
────────────────────────────────────────────────── ( div )
( 𝑚 :: 𝑛 :: S, E, / P ) ⟶ ( 𝑚 ／ 𝑛 :: S, E, P )


────────────────────────────────────── ( divErrByZero )
( 𝑚 :: 0 :: S, E, / P ) ⟶ DivByZero


───────────────────────────────────── ( divErr₁ )
( 𝑛 :: ⊥, E, / P ) ⟶ StackUnderflow


──────────────────────────────── ( divErr₀ )
( ⊥, E, / P ) ⟶ StackUnderflow


                       n ≠ 0
─────────────────────────────────────────────────── ( mod )
( 𝑚 :: 𝑛 :: S, E, % P ) ⟶ ( 𝑚 mod 𝑛 :: S, E, P )


────────────────────────────────────── ( modErrByZero )
( 𝑚 :: 0 :: S, E, % P ) ⟶ DivByZero


───────────────────────────────────── ( modErr₁ )
( 𝑛 :: ⊥, E, % P ) ⟶ StackUnderflow


──────────────────────────────── ( modErr₀ )
( ⊥, E, % P ) ⟶ StackUnderflow


                   𝑚 ＝ 𝑛
──────────────────────────────────────────── ( eq )
( 𝑚 :: 𝑛 :: S, E, = P ) ⟶ ( 1 :: S, E, P )


                   𝑚 ≠ 𝑛
──────────────────────────────────────────── ( neq )
( 𝑚 :: 𝑛 :: S, E, = P ) ⟶ ( 0 :: S, E, P )


───────────────────────────────────── ( eqErr₁ )
( 𝑛 :: ⊥, E, = P ) ⟶ StackUnderflow


──────────────────────────────── ( eqErr₀ )
( ⊥, E, = P ) ⟶ StackUnderflow

                   𝑚 < 𝑛
──────────────────────────────────────────── ( le )
( 𝑚 :: 𝑛 :: S, E, < P ) ⟶ ( 1 :: S, E, P )


                   𝑚 ≮ 𝑛
──────────────────────────────────────────── ( nle )
( 𝑚 :: 𝑛 :: S, E, = P ) ⟶ ( 0 :: S, E, P )


───────────────────────────────────── ( leErr₁ )
( 𝑛 :: ⊥, E, = P ) ⟶ StackUnderflow


──────────────────────────────── ( leErr₀ )
( ⊥, E, = P ) ⟶ StackUnderflow

Subroutines

A subroutine is just a named program. We can define subroutines and call them. Defining a subroutine adds a binding in the environment of its name to the program in the body of its definition. Calling a subroutine simply prepends its body to the program being evaluated.⁵


────────────────────────────────────────────── ( def )
( S, E, def F { Q } P ) ⟶ ( S, E[F ↦ Q], P )


  F ∈ E                  E[X] ∈ ℙ
─────────────────────────────────── ( call )
( S, E, #F P ) ⟶ ( S, E, E[F] P )


  F ∈ E             E[X] ∉ ℙ
────────────────────────────── ( callErr₁ )
( S, E, #F P ) ⟶ InvalidCall


                F ∉ E
────────────────────────────────── ( callErr₀ )
( S, E, #F P ) ⟶ UnknownVariable

Variables

A variable is just a named integer. We can

assign an integer to a variable, which adds a binding to the environment
lookup a variable binding in the environment (by typing the variable itself)

Variables bindings are available within blocks (or globally). Local blocks can be opened and closed using the delimiters '[' and ']', respectively.⁶ Bindings created within a local block are available only within the evaluation of that block. Bindings not created within a local block are available anywhere in the program after they've been created.


────────────────────────────────────────── ( assign )
( 𝑛 :: S, E, @X P ) ⟶ ( S, E[X ↦ 𝑛], P )


───────────────────────────────── ( assignErr₀ )
( ⊥, E, @X P ) ⟶ StackUnderflow


  X ∈ E                    E[X] ∈ ℤ
───────────────────────────────────── ( lookup )
( S, E, X P ) ⟶ ( E[X] :: S, E, P )


  X ∈ E              E[X] ∉ ℤ
─────────────────────────────── ( lookupErr₁ )
( S, E, X P ) ⟶ InvalidLookup


               X ∉ E
───────────────────────────────── ( lookupErr₂ )
( S, E, X P ) ⟶ UnknownVariable


────────────────────────────────── ( openLocal )
( S, E, [ P ) ⟶ ( S, ⟨⟩ · E, P )


───────────────────────────────── ( closeLocal )
( S, L · E, ] P ) ⟶ ( S, E, P )


───────────────────────────── ( closeLocalErr )
( S, 𝒢, ] P ) ⟶ GlobalClose

Conditionals

Finally, there are if-statements for conditional reasoning. We also include while-loops with the usual semantics (i.e., defined in terms of if-statements).


                         𝑛 ≠ 0
─────────────────────────────────────────────────────── ( ifTrue )
( 𝑛 :: S, E, ? { Q₁ } else { Q₂ } P ) ⟶ ( S, E, Q₂ P )


──────────────────────────────────────────────────────── ( ifFalse )
( 0 :: S, E, ? { Q₁ } else { Q₂ } P ) ⟶ ( S, E, Q₁ P )


─────────────────────────────────────────────────── ( ifErr₀ )
( ⊥, E, ? { Q₁ } else { Q₂ } P ) ⟶ StackUnderflow


─────────────────────────────────────────────────────── ( while )
( S, E, while { Q₁ } do { Q₂ } P ) ⟶
( S, E, Q₁ ? { Q₂ while { Q₁ } do { Q₂ } } else { } P )

Footnotes:

Note that this only saves the program, not the whole program state. When reseting, the stack and environment will be empty, but the inital program will be the most recently saved program.

This cannot be undone.

In other word, 𝕍 = ℤ ∪ ℙ.

⁴

It's unofficial because printed strings are not a part of the configuration. Semantically, print is identical to drop.

⁵

Its truly amazing to me how simple this is.

⁶

Note that they aren't actually delimiters. It's possible to write program which opens more blocks than it closes.