CS320 Project Part 2 Solution

1 Overview
Stack-oriented programming languages utilize one or more stack data structures which the programmer manipulates to perform computations. The specification below lays out the syntax and semantics of such a language which you will need to implement an evaluator for, taking a program and evaluating it into an OCaml value. You must implement a function: interp : string -> string list option
Where the input string is some (possibly ill-formed) stack-language program and the result is a list of things “printed” by the program during its evaluation.
2 Grammar
For part 2, you will need to support the following grammar. The grammar specifies the form of a valid program. Any invalid program, one which is not derivable from the grammar, cannot be given meaning and evaluted. In the case of an invalid program, interp should return None. ⟨prog⟩ is the starting symbol.
2.1 Constants
⟨digit⟩ ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
⟨nat⟩ ::= ⟨digit⟩ | ⟨digit⟩⟨nat⟩
⟨int⟩ ::= ⟨nat⟩ | -⟨nat⟩
⟨bool⟩ ::= True | False
⟨char⟩ ::= a | b | ... | z
⟨sym⟩ ::= ⟨char⟩ | ⟨sym⟩⟨char⟩ | ⟨sym⟩⟨digit⟩
⟨const⟩ ::= ⟨int⟩ | ⟨bool⟩ | Unit | ⟨sym⟩
2.2 Programs
⟨prog⟩ ::= ⟨coms⟩
⟨com⟩ ::= Push ⟨const⟩ | Pop | Swap | Trace
| Add | Sub | Mul | Div
| And | Or | Not
| Lt | Gt
| If ⟨coms⟩ Else ⟨coms⟩ End | Bind | Lookup
| Fun ⟨coms⟩ End | Call | Return
⟨coms⟩ ::= ϵ | ⟨com⟩; ⟨coms⟩
Note: ϵ is the empty symbol. We use ϵ to refer to empty strings or empty lists depending on context.
3 Operational Semantics
For part 2, you will need to support the following operational semantics. The operational semantics specifies the meaning of a valid program. For the stack-language, a program is evaluated using a stack and it produces a trace. Once we have fully evaluated the program, we return the resulting trace from interp.
3.1 Constants and Values
Push places constants, as defined by the grammar, onto the stack during evaluation. However, as we use more commands, we create things on the stack which are not simple constants. We generically refer to things that can go on the stack as values.
Constants are values. We have as constants: numbers, e.g. -123; booleans, e.g. True; unit, e.g. Unit; and symbols, e.g. xyz123. Symbols are new to part 2 and are used for names when we create bindings in the variable environment.
3.2 Configuration of Programs
A program configuration is of the following form.
[S | T | V ] P
• S: (Stack) stack of intermediate values
• T: (Trace) list of strings logging the program trace
• V : (Variable Environment) mapping from symbols to values (we will use the notation x ↣ v to denote the map of the symbol x to the value v)
• P: (Program) program commands to be interpreted Examples:
[ϵ | ϵ | ϵ] PushTrue;Not;Push 1;Lt;ϵ (1)
[1 :: 2 :: ϵ | "True" :: "0" :: ϵ | ϵ] PushTrue;Push 9;Pop;ϵ (2)
[0 :: True :: ϵ | ϵ | x ↣ 9 :: ϵ] Push 10;Push x;Lookup;Add;Trace;ϵ (3)
[True :: False :: 321 :: ϵ | "123" :: "False" :: ϵ | ϵ] Pop;Pop;Trace;Gt;ϵ (4)
3.3 Closures
In part 2, the Stack language will have functions. Functions will not be given as constants, but as commands including other blocks of commands, as already seen above in the grammar. To store functions on our stack we will have function values (called closures). These values relate to OCaml closure values (aka fun ...).
We will write closures as ⟨f,V,C⟩.
• V is a variable environment containing the variable binds captured by the closure, meaning they are those variables bound when the closure is created e.g. let x = 3 in fun y -> x + y. In the function, the variable x is captured since it is bound when the function is created.
• C is the list of commands which make up the body of the function.
3.4 Program Reduction
The operational semantics of the language is defined in terms of the following single step relation.
[S1 | T1 | V1 ] P1 ⇝ [S2 | T2 | V2 ] P2
In one step, program configuration [S1 | T1 | V1 ] P1 evaluates to [S2 | T2 | V2 ] P2. For configurations where P = ϵ, we say that evaluation has terminated as there is no program left to interpret. In this case, return trace T as the final result of your interp function.
3.5 Push
Given any constant c, the command Push c pushes c onto the current stack S. Push never fails.
Push

[S | T | V ] Push c;P ⇝ [c :: S | T | V ] P
Examples:
• [1 :: True :: ϵ | "Unit" :: "False" :: ϵ | ϵ] Push 2;ϵ ⇝ [2 :: 1 :: True :: ϵ | "Unit" :: "False" :: ϵ | ϵ] ϵ • [1 :: True :: ϵ | "5" :: ϵ | ϵ] PushTrue;ϵ ⇝ [True :: 1 :: True :: ϵ | "5" :: ϵ | ϵ] ϵ
3.6 Pop
Given a stack of the form c :: S (constant c is on top of S), the Pop command removes c and leaves the rest of stack S unmodified.
The Pop command has 1 fail state.
1. PopError: The stack is empty (S = ϵ).
When Pop fails, the string "Panic" is prepended to the trace and the program terminates.
PopStack

[c :: S | T | V ] Pop;P ⇝ [S | T | V ] P PopError

[ϵ | T | V ] Pop;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [1 :: True :: ϵ | "Unit" :: "False" :: ϵ | ϵ] Pop;ϵ ⇝ [True :: ϵ | "Unit" :: "False" :: ϵ | ϵ] ϵ • [ϵ | "5" :: ϵ | ϵ] Pop;Push 12;ϵ ⇝ [ϵ | "Panic" :: "5" :: ϵ | ϵ] ϵ
3.7 Swap
Given a stack of the form c1 :: c2 :: S (constants c1 and c2 is on top of S), the Swap command changes the order of c1 and c2 and leaves the rest of stack S unmodified. The Swap command has 2 fail state.
1. SwapError1: The stack is empty (S = ϵ).
2. SwapError3: The stack has only 1 element (S = c :: ϵ).
When Swap fails, the string "Panic" is prepended to the trace and the program terminates.
SwapStack

[c1 :: c2 :: S | T | V ] Swap;P ⇝ [c2 :: c1 :: S | T | V ] P SwapError1

[ϵ | T | V ] Swap;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
SwapError2

[c :: ϵ | T | V ] Swap;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [1 :: True :: ϵ | "Unit" :: "False" :: ϵ | ϵ] Swap;ϵ ⇝ [True :: 1 :: ϵ | "Unit" :: "False" :: ϵ | ϵ] ϵ
• [ϵ | "5" :: ϵ | ϵ] Swap;Push 12;ϵ ⇝ [ϵ | "Panic" :: "5" :: ϵ | ϵ] ϵ

3.8 Trace
c S where c is any valid constant, the Trace command removes c from the stack
and puts a Unit constant onto the stack. The string representation of c as determined by the toString function to prepended to the trace.
The Trace command has 1 fail state.
1. TraceError: The stack is empty (S = ϵ).
When Trace fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
TraceStack

[c :: S | T | V ] Trace;P ⇝ [Unit :: S | toString(c) :: T | V ] P
TraceError

[ϵ | T | V ] Trace;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
The toString function is a special function which you must define to convert constant values into their string representations. The following equations illustrate the strings expected for typical inputs.
toString(123) = "123" (1)
toString(True) = "True" (2)
toString(False) = "False" (3)
toString(Unit) = "Unit" (4)
toString(abc) = "abc" (5)
toString(⟨abc,V,P⟩) = "Fun<abc>" (6)
Examples:
• [1 :: True :: ϵ | "Unit" :: "False" :: ϵ | ϵ] Trace;ϵ ⇝ [Unit :: True :: ϵ | "1" :: "Unit" :: "False" :: ϵ | ϵ] ϵ
• [ϵ | "5" :: ϵ | ϵ] Trace;Push 12;ϵ ⇝ [ϵ | "Panic" :: "5" :: ϵ | ϵ] ϵ
3.9 Add
Add from the stack and puts their sum (i + j) onto the stack. The Add command has 3 fail states.
1. AddError1: Either i or j is not an integer.
2. AddError2: The stack is empty (S = ϵ).
3. AddError3: The stack has only 1 element (S = c :: ϵ).
When Add fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
AddStack
i and j are both integers

[i :: j :: S | T | V ] Add;P ⇝ [(i + j) :: S | T | V ] P AddError1
i or j is not an integer

[i :: j :: S | T | V ] Add;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
AddError2

[ϵ | T | V ] Add;P ⇝ [ϵ | "Panic" :: T | V ] ϵ AddError3

[c :: ϵ | T | V ] Add;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [4 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Add;ϵ ⇝ [9 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] ϵ
• [4 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Add;Trace;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ • [4 :: ϵ | "False" :: ϵ | ϵ] Add;Trace;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ
3.10 Sub
Given a stack of the form i :: j :: S where both i and j are integer values, the Sub command removes i and j from the stack and puts their difference (i − j) onto the stack. The Sub command has 3 fail states.
1. SubError1: Either i or j is not an integer.
2. SubError2: The stack is empty (S = ϵ).
3. SubError3: The stack has only 1 element (S = c :: ϵ).
When Sub fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
SubStack
i and j are both integers

[i :: j :: S | T | V ] Sub;P ⇝ [(i − j) :: S | T | V ] P SubError1
i or j is not an integer

[i :: j :: S | T | V ] Sub;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
SubError2

[ϵ | T | V ] Sub;P ⇝ [ϵ | "Panic" :: T | V ] ϵ SubError3

[c :: ϵ | T | V ] Sub;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [4 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Sub;ϵ ⇝ [−1 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] ϵ
• [4 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Sub;Trace;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ
• [4 :: ϵ | "False" :: ϵ | ϵ] Sub;Trace;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ
3.11 Mul
Mul from the stack and puts their product (i × j) onto the stack. The Mul command has 3 fail states.
• MulError1: Either i or j is not an integer.
• MulError2: The stack is empty (S = ϵ).
• MulError3: The stack has only 1 element (S = c :: ϵ).
When Mul fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
MulStack
i and j are both integers

[i :: j :: S | T | V ] Mul;P ⇝ [(i × j) :: S | T | V ] P MulError1
i or j is not an integer

[i :: j :: S | T | V ] Mul;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
MulError2

[ϵ | T | V ] Mul;P ⇝ [ϵ | "Panic" :: T | V ] ϵ MulError3

[c :: ϵ | T | V ] Mul;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [4 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Mul;ϵ ⇝ [20 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] ϵ
• [4 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Mul;Trace;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ
• [4 :: ϵ | "False" :: ϵ | ϵ] Mul;Trace;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ
3.12 Div
Div from the stack and puts their quotient (i ÷ j) onto the stack. The Div command has 4 fail states.
1. DivError0: Both i and j are integers and j = 0.
2. DivError1: Either i or j is not an integer.
3. DivError2: The stack is empty (S = ϵ).
4. DivError3: The stack has only 1 element (S = c :: ϵ).
When Div fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
DivStack DivError0
i and j are both integers, j ̸= 0 i is an integer

[i :: j :: S | T | V ] Div;P ⇝ [(i ÷ j) :: S | T | V ] P [i :: 0 :: S | T | V ] Div;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
DivError1
i or j is not an integer DivError2

[i :: j :: S | T | V ] Div;P ⇝ [ϵ | "Panic" :: T | V ] ϵ [ϵ | T | V ] Div;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
DivError3

[c :: ϵ | T | V ] Div;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [16 :: 8 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Div;ϵ ⇝ [2 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] ϵ
• [16 :: 0 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Div;PushUnit;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ
• [16 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Div;Add;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ
• [4 :: ϵ | "False" :: ϵ | ϵ] Div;Trace;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ

3.13 And
a b a b are boolean values, the And a b
from the stack and puts their conjunction (a ∧ b) onto the stack. The And command has 3 fail states.
1. AndError1: Either a or b is not a boolean.
2. AndError2: The stack is empty (S = ϵ).
3. AndError3: The stack has only 1 element (S = c :: ϵ).
When And fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
AndStack
a and b are both booleans

[a :: b :: S | T | V ] And;P ⇝ [(a ∧ b) :: S | T | V ] P AndError1 a or b is not a boolean

[a :: b :: S | T | V ] And;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
AndError2

[ϵ | T | V ] And;P ⇝ [ϵ | "Panic" :: T | V ] ϵ AndError3

[c :: ϵ | T | V ] And;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [True :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] And;ϵ ⇝ [True :: Unit :: ϵ | "False" :: ϵ | ϵ] ϵ
• [False :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] And;Trace;ϵ ⇝ [False :: Unit :: ϵ | "False" :: ϵ | ϵ] Trace;ϵ • [True :: 4 :: Unit :: ϵ | "False" :: ϵ | ϵ] And;Pop;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ
3.14 Or
Given a stack of the form a :: b :: S where both a and b are boolean values, the Or command removes a and b from the stack and puts their disjunction (a ∨ b) onto the stack. The Or command has 3 fail states.
1. OrError1: Either a or b is not a boolean.
2. OrError2: The stack is empty (S = ϵ).
3. OrError3: The stack has only 1 element (S = c :: ϵ).
When Or fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
OrStack
a and b are both booleans

[a :: b :: S | T | V ] Or;P ⇝ [(a ∨ b) :: S | T | V ] P OrError1 a or b is not a boolean

[a :: b :: S | T | V ] Or;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
OrError2

[ϵ | T | V ] Or;P ⇝ [ϵ | "Panic" :: T | V ] ϵ OrError3

[c :: ϵ | T | V ] Or;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [True :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Or;ϵ ⇝ [True :: Unit :: ϵ | "False" :: ϵ | ϵ] ϵ
• [False :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Or;Trace;ϵ ⇝ [True :: Unit :: ϵ | "False" :: ϵ | ϵ] Trace;ϵ
• [True :: 4 :: Unit :: ϵ | "False" :: ϵ | ϵ] Or;Pop;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ
3.15 Not
a a is a boolean values, the Not command removes a from the stack and
puts its negation (¬a) onto the stack.
The Not command has 2 fail states. 1. NotError1: a is not a boolean.
2. NotError2: The stack is empty (S = ϵ).
When Not fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
NotStack NotError1
a is a boolean a is not a boolean

[a :: S | T | V ] Not;P ⇝ [(¬a) :: S | T | V ] P [a :: S | T | V ] Not;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
NotError2

[ϵ | T | V ] Not;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [True :: Unit :: ϵ | "False" :: ϵ | ϵ] Not;ϵ ⇝ [False :: Unit :: ϵ | "False" :: ϵ | ϵ] ϵ
• [4 :: Unit :: ϵ | "False" :: ϵ | ϵ] Not;Pop;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ
• [ϵ | "False" :: ϵ | ϵ] Not;Add;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ
3.16 Lt
Given a stack of the form i :: j :: S where both i and j are integer values, the Lt command removes i and j from the stack and puts the boolean result of their comparison (i < j) onto the stack. The Lt command has 3 fail states.
1. LtError1: Either i or j is not an integer.
2. LtError2: The stack is empty (S = ϵ).
3. LtError3: The stack has only 1 element (S = c :: ϵ).
When Lt fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
LtStack
i and j are both integers

[i :: j :: S | T | V ] Lt;P ⇝ [(i < j) :: S | T | V ] P LtError1
i or j is not an integer

[i :: j :: S | T | V ] Lt;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
LtError2

[ϵ | T | V ] Lt;P ⇝ [ϵ | "Panic" :: T | V ] ϵ LtError3

[c :: ϵ | T | V ] Lt;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [4 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Lt;ϵ ⇝ [True :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] ϵ
• [5 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Lt;ϵ ⇝ [False :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] ϵ
• [4 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Lt;Trace;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ
3.17 Gt
i j where both i and j are integer values, the Gt command removes i and j
from the stack and puts the boolean result of their comparison (i > j) onto the stack. The Gt command has 3 fail states.
1. GtError1: Either i or j is not an integer.
2. GtError2: The stack is empty (S = ϵ).
3. GtError3: The stack has only 1 element (S = c :: ϵ).
When Gt fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
GtStack
i and j are both integers

[i :: j :: S | T | V ] Gt;P ⇝ [(i > j) :: S | T | V ] P GtError1
i or j is not an integer

[i :: j :: S | T | V ] Gt;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
GtError2

[ϵ | T | V ] Gt;P ⇝ [ϵ | "Panic" :: T | V ] ϵ GtError3

[c :: ϵ | T | V ] Gt;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [4 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Gt;ϵ ⇝ [False :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] ϵ
• [10 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Gt;ϵ ⇝ [True :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] ϵ
• [5 :: 5 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Gt;ϵ ⇝ [False :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] ϵ
• [4 :: True :: Unit :: ϵ | "False" :: ϵ | ϵ] Gt;Trace;ϵ ⇝ [ϵ | "Panic" :: "False" :: ϵ | ϵ] ϵ
3.18 If Else
b b is a boolean values, the If C1 Else C2 End command removes b from
the stack and evaluates C1 if b is True and C2 if b is False before continuing with the program.
The If C1 Else C2 End command has 2 fail states.
1. IfElseError1: b is not a boolean.
2. IfElseError2: The stack is empty (S = ϵ).
When If C1 Else C2 End fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
ThenStack

[True :: S | T | V ] If C1 Else C2 End;P ⇝ [S | T | V ] C1 P
ElseStack

[False :: S | T | V ] If C1 Else C2 End;P ⇝ [S | T | V ] C2 P
IfElseError1
v is not a boolean

[v :: S | T | V ] If C1 Else C2 End;P ⇝ [ϵ | "Panic" :: T | V ] ϵ IfElseError2

[ϵ | T | V ] If C1 Else C2 End;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [True :: ϵ | "False" :: ϵ | ϵ] IfPush 8;Trace; ElseTrace; End;ϵ ⇝ [ϵ | "False" :: ϵ | ϵ] Push 8;Trace;ϵ
• [False :: ϵ | "False" :: ϵ | ϵ] IfPush 8;Trace; ElseTrace; End;ϵ ⇝ [ϵ | "False" :: ϵ | ϵ] Trace;ϵ
• [5 :: ϵ | ϵ | ϵ] IfPush 3; ElsePush 2; End;Add;ϵ ⇝ [ϵ | "Panic" :: ϵ | ϵ] ϵ
• [ϵ | "4" :: ϵ | ϵ] IfPush 3; ElsePush 2; End;Add;ϵ ⇝ [ϵ | "Panic" :: "4" :: ϵ | ϵ] ϵ
3.19 Bind
x v where x is a symbol value and v is any value, the Bind command removes
x and v from the stack and assigns x to v in the variable environment. The Bind command has 3 fail states.
1. BindError1: x is not a symbol.
2. BindError2: The stack is empty (S = ϵ).
3. BindError3: The stack has only 1 element (S = c :: ϵ).
When Bind fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates. As mentioned before, the notation x ↣ v in the rules below denotes the map of the symbol x to the value v.
BindStack
x is a symbol

[x :: v :: S | T | V ] Bind;P ⇝ [S | T | x ↣ v :: V ] P
BindError1
x is not a symbol BindError2

[x :: v :: S | T | V ] Bind;P ⇝ [ϵ | "Panic" :: T | V ] ϵ [ϵ | T | V ] Bind;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
BindError3

[c :: ϵ | T | V ] Bind;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [x :: True :: ϵ | ϵ | ϵ] Bind;ϵ ⇝ [ϵ | ϵ | x↣True :: ϵ] ϵ
• [True :: x :: ϵ | ϵ | ϵ] Bind;ϵ ⇝ [ϵ | "Panic" :: ϵ | ϵ] ϵ
• [x :: ϵ | ϵ | ϵ] Bind;ϵ ⇝ [ϵ | "Panic" :: ϵ | ϵ] ϵ
• [ϵ | "4" :: ϵ | ϵ] Bind;ϵ ⇝ [ϵ | "Panic" :: "4" :: ϵ | ϵ] ϵ
3.20 Lookup
x x is a symbol value, the Lookup command removes x from the stack,
finds the most recent value it is bound to, and puts this value on the stack. The Lookup command has 3 fail states.
1. LookupError1: x is not a symbol.
2. LookupError2: The stack is empty (S = ϵ).
3. LookupError3: x is not bound to a value.
When Lookup fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
LookupStack
x is a symbol x ↣ v ∈ V

[x :: S | T | V ] Lookup;P ⇝ [v :: S | T | V ] P LookupError1 x is not a symbol

[x :: S | T | V ] Lookup;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
LookupError2

[ϵ | T | V ] Lookup;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples: LookupError3
x ↣ v /∈ V

[x :: ϵ | T | V ] Lookup;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
• [x :: ϵ | ϵ | x↣True :: ϵ] Lookup;ϵ ⇝ [True :: ϵ | ϵ | x↣True :: ϵ] ϵ
• [x :: ϵ | ϵ | x↣True :: x↣False :: ϵ] Lookup;ϵ ⇝ [True :: ϵ | ϵ | x↣True :: x↣False :: ϵ] ϵ
• [Unit :: ϵ | ϵ | ϵ] Lookup;ϵ ⇝ [ϵ | "Panic" :: ϵ | ϵ] ϵ
• [ϵ | ϵ | ϵ] Lookup;ϵ ⇝ [ϵ | "Panic" :: ϵ | ϵ] ϵ
• [x :: ϵ | ϵ | y↣True :: y↣False :: ϵ] Lookup;ϵ ⇝ [ϵ | "Panic" :: ϵ | ϵ] ϵ

3.21 Fun
Fun C End is a command representing a function definition. Given a stack of the form x :: S where x is a symbol value, the Fun C End command creates a closure value (explained in Section 3.3) on the stack with name x, the current variable environment, and the commands C defining the function.
The Fun C End command has 2 fail states.
1. FunError1: x is not a symbol.
2. FunError2: The stack is empty (S = ϵ).
When Fun C End fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
FunStack
x is a symbol

[x :: S | T | V ] Fun C End;P ⇝ [⟨x,V,C⟩ :: S | T | V ] P
FunError1 x is not a symbol

[x :: S | T | V ] Fun C End;P ⇝ [ϵ | "Panic" :: T | V ] ϵ FunError2

[ϵ | T | V ] Fun C End;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [f :: ϵ | ϵ | x↣True :: ϵ] FunTrace; End;ϵ ⇝ [⟨f,x↣True :: ϵ,Trace;⟩ :: ϵ | ϵ | x↣True :: ϵ] ϵ
• [True :: 2 :: ϵ | ϵ | ϵ] FunPush 3; End;ϵ ⇝ [ϵ | "Panic" :: ϵ | ϵ] ϵ
• [ϵ | ϵ | ϵ] FunGt; End;ϵ ⇝ [ϵ | "Panic" :: ϵ | ϵ] ϵ
3.22 Call
Call is used to implement the call of a (potentially recursive) function. Given a stack of the form ⟨f,V,C⟩ :: a :: S where ⟨f,V,C⟩ is a closure value (explained in Section 3.3), the Call command consumes ⟨f,V,C⟩ and a , then executes the commands C from the closure with variable environment f ↣ ⟨f,V,C⟩ :: V (notice that this is the environment from the closure updated with a new map associating the symbol f with the closure itself - this is needed for recursive functions). The command also need to update the stack to have the current continuation and the value a. The current continuation is itself a closure ⟨cc,V ′,P′⟩ where cc is just a symbol standing for current continuation, V’ is the current environment and P′ is the list of remaining commands, put onto the stack.
The Call command has 2 fail states.
1. CallError1: v is not a closure value.
2. CallError2: The stack is empty (S = ϵ).
3. CallError3: The stack has only 1 element (S = c :: ϵ).
When Call fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
CallError1 CallStack c is not a closure value.

[⟨f,Vf,C⟩ :: a :: S | T | V ] Call;P [c :: S | T | V ] Call;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
⇝ [a :: ⟨cc,V,P⟩ :: S | T | f ↣ ⟨f,Vf,C⟩ :: Vf ] C
CallError2

[ϵ | T | V ] Call;P ⇝ [ϵ | "Panic" :: T | V ] ϵ CallError3

[c :: ϵ | T | V ] Call;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
•
[⟨f,x↣True,Trace;ϵ⟩ :: 2 :: ϵ | ϵ | x↣False :: ϵ] Call;ϵ
⇝
[2 :: ⟨cc,x↣False :: ϵ,ϵ⟩ :: ϵ | ϵ | f↣ ⟨f,x↣True,Trace;ϵ⟩ :: x↣True :: ϵ] Trace;ϵ
• [True :: 2 :: ϵ | ϵ | ϵ] Call;ϵ ⇝ [ϵ | "Panic" :: ϵ | ϵ] ϵ
• [⟨f,ϵ,ϵ⟩ :: ϵ | ϵ | ϵ] Call;ϵ ⇝ [ϵ | "Panic" :: ϵ | ϵ] ϵ
3.23 Return
Return is used to implement the return call from a function. The behavior of Return is similar to the one of Call, but no continuation is pushed and no name is bound.
Given a stack of the form v :: a :: S where v is a closure value, v = ⟨f,V,C⟩, the Return command consumes v, then executes the commands C with variable environment V . The Return command has 2 fail states.
1. ReturnError1: v is not a closure value.
2. ReturnError2: The stack is empty (S = ϵ).
3. ReturnError3: The stack has only 1 element (S = c :: ϵ).
When Return fails, the stack is cleared, the string "Panic" is prepended to the trace and the program terminates.
ReturnStack

[⟨f,Vf,C⟩ :: a :: S | T | V ] Return;P ⇝ [a :: S | T | Vf ] C
ReturnError1
c is not a closure value. ReturnError3

[c :: a :: S | T | V ] Return;P ⇝ [ϵ | "Panic" :: T | V ] ϵ [ϵ | T | V ] Return;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
ReturnError3

[c :: ϵ | T | V ] Return;P ⇝ [ϵ | "Panic" :: T | V ] ϵ
Examples:
• [⟨f,x↣True,Trace;ϵ⟩ :: 2 :: ϵ | ϵ | ϵ] Return;ϵ ⇝ [2 :: ϵ | ϵ | x↣True :: ϵ] Trace;ϵ
• [True :: 2 :: ϵ | ϵ | ϵ] Return;ϵ ⇝ [ϵ | "Panic" :: ϵ | ϵ] ϵ
• [⟨f,ϵ,ϵ⟩ :: ϵ | ϵ | ϵ] Return;ϵ ⇝ [ϵ | "Panic" :: ϵ | ϵ] ϵ

4 Function Example
Consider the OCaml program for computing factorial:
let rec factorial = fun n -> if 2 > n then
1 else
factorial(n - 1) * n let _ = print_int(factorial(4))
And the equivalent Stack language program:
Push factorial;
Fun
Push n;
Bind;
Push n; Lookup; Push 2;
Gt;
If
Push 1; Swap;
Return;
Else
Push n; Lookup;
Push -1; Add;
Push factorial;
Lookup;
Call;
Push n; Lookup;
Mul;
Swap;
Return;
End;
End;
Push factorial;
Bind;
Push 4;
Push factorial;
Lookup;
Call;
Trace;
Although the programs differ in visual complexity, they work in a similar way:
• Push factorial; Fun ...
As with let rec factorial = fun n -> ..., we are creating a recursive function with the name factorial and taking a single argument.
• ...
Fun
Push n;
Bind; ...
Implicit in the OCaml program, our argument in the Stack language is unnamed to start, so we assign it the name n.
• ...
Push n; Lookup; Push 2;
Gt; ...
Just 2 > n directly.
• ...
If
Push 1; Swap;
Return;
...
if 2 > n then 1. When factorial is called, it expects a continuation (a function) on its stack before its arguments. This continuation takes our result as an argument. Since arguments are put before a function on the stack, we must use Swap, and then we invoke the continuation with Return.
• ...
Else
Push n; Lookup;
Push -1;
Add;
Push factorial;
Lookup;
Call;
Push n; Lookup;
Mul;
Swap;
Return;
End;
...
• ....
Push factorial;
Bind; ...
As with our argument n in our function, this task is handled in OCaml during let rec factorial = fun n -> .... Using Fun ... End in Stack just makes a closure and places it on the stack. To have it be bound to a name to lookup, we must explicitly Bind.
• Push 4;
Push factorial;
Lookup;
Call;
5 Full Examples
• Compute the polynomial x2 − 4x + 7 at 3:
Push 3;
Push 3;
Mul;
Push -4;
Push 3;
Mul;
Add;
Push 7;
Add;
Trace;
Result: Some ["4"]
• De Morgan’s Law:
Push False;
Push False;
And;
Not;
Trace;
Push False;
Not;
Push False;
Not;
Or;
Trace;
Result: Some ["True"; "True"]
• x2 is monotonic:
Push 2;
Push 2;
Mul;
Push 3;
Push 3;
Mul;
Gt;
Trace;
Result: Some ["True"]
• Factorial from 4.
...
Result: Some ["24"]
• Define a function for polynomial x2 − 4x + 7 and evaluate at 3:
Push poly;
Fun
Push x;
Bind;
Push x;
Lookup;
Push x;
Lookup;
Mul;
Push -4;
Push x;
Lookup;
Mul;
Add;
Push 7;
Add;
Swap;
Return;
End;
Push 3;
Swap;
Call;
Trace;
Result: Some ["4"]