CS**0 Fall2023 Project Part 3

December 2023

1 Overview

The stack-oriented programming language of part1 and part2 is fairly low level and difficult to write non-trivial programs

for. In this part of the project, your task is to implement a compiler that compiles a OCaml-like high-level programming

language into the stack language of part2. More specifically, you must implement a compile function with the following

signature.

compile : string -> string

Given a source string written in the high-level language, compile produces a string encoding a semantically equivalent

program written in the syntax of the stack language of part2. In other words, given an arbitrary high-level program

P, compiling P then interpreting its resulting stack program yields the same trace as interpreting P directly using the

operational semantics of the high-level language (Section 3).

The concrete syntax of the high-level language is substantially more complex than the stack language. We provide the

parser for the high-level language with the following AST and parser. The parse_prog function parses a string and produces

its corresponding high-level AST. Note that the context free grammar presented in Section 2 is not representative of

the strings accepted by parse_prog. The input to parse_prog is transformed by the parser (syntax desugaring + variable

scoping) to produce a valid expr value. It is these expr values that correspond to the grammar of Section 2.

type uopr =

| Neg | Not

type bopr =

| Add | Sub | Mul | Div | Mod

| And | Or

| Lt | Gt | Lte | Gte | Eq

type expr =

| Int of int | Bool of bool | Unit

| UOpr of uopr * expr

| BOpr of bopr * expr * expr

| Var of string

| Fun of string * string * expr

| App of expr * expr

| Let of string * expr * expr

| Seq of expr * expr

| Ifte of expr * expr * expr

| Trace of expr

let parse_prog (s : string) : expr = ...

1

2 Grammar

⟨digit⟩ ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9

⟨nat⟩ ::= ⟨digit⟩ | ⟨digit⟩⟨nat⟩

⟨int⟩ ::= ⟨nat⟩ | - ⟨nat⟩

⟨bool⟩ ::= true | false

⟨unit⟩ ::= ()

⟨unop⟩ ::= - | not

⟨binop⟩ ::= + | - | * | / | mod | && | || | < | > | <= | >= | =

⟨char ⟩ ::= a | b | .. | z

⟨var ⟩ ::= ⟨char ⟩ | ⟨var ⟩⟨char ⟩ | ⟨var ⟩⟨digit⟩

⟨expr ⟩ ::= ⟨int⟩ | ⟨bool⟩ | ⟨unit⟩

| ⟨unop⟩ ⟨expr ⟩

| ⟨expr ⟩ ⟨binop⟩ ⟨expr ⟩

| ⟨var ⟩

| fun ⟨var ⟩ ⟨var ⟩ -> ⟨expr ⟩

| ⟨expr ⟩ ⟨expr ⟩

| let ⟨var ⟩ = ⟨expr ⟩ in ⟨expr ⟩

| ⟨expr ⟩ ; ⟨expr ⟩

| if ⟨expr ⟩ then ⟨expr ⟩ else ⟨expr ⟩

| trace ⟨expr ⟩

The following table shows how symbols in the grammar correspond to constructors of the expr datatype.

Grammar OCaml Constructor Description

⟨int⟩ Int of int integer constant

⟨bool⟩ Bool of bool boolean constant

⟨unit⟩ Unit unit constant

⟨unop⟩ ⟨expr ⟩ UOpr of uopr * expr unary operation

⟨expr ⟩ ⟨binop⟩ ⟨expr ⟩ BOpr of bopr * expr * expr binary operation

⟨var ⟩ Var of string variable

fun ⟨var ⟩ ⟨var ⟩ -> ⟨expr ⟩ Fun of string * string * expr function

⟨expr ⟩ ⟨expr ⟩ App of expr * expr function application

let ⟨var ⟩ = ⟨expr ⟩ in ⟨expr ⟩ Let of string * expr * expr let-in expression

⟨expr ⟩; ⟨expr ⟩ Seq of expr * expr sequence expression

if ⟨expr ⟩ then ⟨expr ⟩ else ⟨expr ⟩ Ifte of expr * expr * expr if-then-else expression

trace ⟨expr ⟩ Trace of expr trace expression

2

3 Operational Semantics

3.1 Configuration of Programs

A program configuration is of the following form.

[ T ] s

• T: (Trace): List of strings logging the program trace.

• s: (State): Current state of the program. This can be an ⟨expr ⟩ or a special Error state.

Examples:

1. [ "True" :: ϵ ] let x = 1 in let y = 2 in trace (x + y)

2. [ "Unit" :: ϵ ] let foo = fun f x -> x in let y = 2 in trace (foo y)

3. [ "Panic" :: "1" :: ϵ ] Error

3.2 Single-Step Reduction

The operational semantics of the high-level language is similar to OCaml with a reduced feature set. The semantics are

given through the following primitive single-step relation.

[ T1 ] s1 ⇝ [ T2 ] s2

Here, s1 is the starting program state and T1 is its associated trace. The reduction relation transforms program s1 into

program s2 and transforms trace T1 into trace T2 in a single step. For the rules deriving the single-step relation, s1 will

always be an ⟨expr ⟩ while s2 may be an ⟨expr ⟩ or the special Error state. This means that if the Error state is ever

reached, reduction will not be able to continue further and the program terminates.

Note: Most of the operational semantics rules are simple but repetitive. Readers familiar with OCaml should already

have a good understanding of the high-level language.

3.3 Multi-Step Reduction

A separate multi-step reduction relation [ T1 ] s1 ⇝ [ T2 ] s2 is defined to compose together 0 or more single-step reductions.

The rules for deriving the multi-step relation are given as follows.

StarRefl

[ T ] s ⇝∗

[ T ] s

StarStep

[ T1 ] s1 ⇝∗

[ T2 ] s2 [ T2 ] s2 ⇝ [ T3 ] s3

[ T1 ] s1 ⇝∗

[ T3 ] s3

• StarRefl: A program configuration “reduces” to itself in 0 steps.

• StarStep: Multi-step can be extended with a single-step if their end state and starting state match.

3.4 Values

We refer to a special subset of expressions as values. In particular, values can be characterized by the following grammar.

We can see here that integer constants, boolean constants, unit constants and functions are considered values. Basically,

values are expressions which can not be reduced further.

⟨value⟩ ::= ⟨int⟩ | ⟨bool⟩ | ⟨unit⟩

| fun ⟨var ⟩ ⟨var ⟩ -> ⟨expr ⟩

Note: We use the v variable to range over values. In other words, all instances of v are required to be values.

3

3.5 Unary Operations

Integer Negation

Integer negation is a unary operation which negates the value of an integer argument.

NegInt

v is an integer value

[ T ] - v ⇝ [ T ] −v

NegExpr

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] - m1 ⇝ [ T2 ] - m2

NegError1

v is not an integer value

[ T ] - v ⇝ [ "Panic" :: T ] Error

NegError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] - m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• NegInt: Interpret syntactic - v as mathematical negation −v if applied to an integer value v.

• NegExpr: Structurally reduce the argument of negation if it is not a value.

• NegError1: Applying negation to a value of an incorrect type results in Error and panic trace.

• NegError2: A negation expression reduces to Error if its argument reduces to Error.

Boolean Not

Boolean not is a unary operation which negates the value of a boolean argument.

NotBool

v is a bool value

[ T ] not v ⇝ [ T ] ¬v

NotExpr

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] not m1 ⇝ [ T2 ] not m2

NotError1

v is not a boolean value

[ T ] not v ⇝ [ "Panic" :: T ] Error

NotError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] not m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• NotBool: Interpret syntactic not v as boolean negation ¬v if applied to a boolean value v.

• NotExpr: Structurally reduce the argument of not if it is not a value.

• NotError1: Applying not to a value of an incorrect type results in Error and panic trace.

• NotError2: A not expression reduces to Error if its argument reduces to Error.

4

3.6 Binary Operations

Integer Addition

Integer addition is a binary operation that sums the values of 2 integer arguments.

AddInt

v1 and v2 are integers

[ T ] v1 + v2 ⇝ [ T ] v1 + v2

AddExpr1

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1 + n ⇝ [ T2 ] m2 + n

AddExpr2

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] v + m1 ⇝ [ T2 ] v + m2

AddError1

v1 or v2 are not integers

[ T ] v1 + v2 ⇝ [ "Panic" :: T ] Error

AddError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m + n ⇝ [ T2 ] Error

AddError3

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] v + m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• AddInt: Interpret syntactic v1 + v2 as mathematical addition v1 + v2 if applied to integers v1 and v2.

• AddExpr1: Structurally reduce the left-hand side of addition if it is not a value.

• AddExpr2: Structurally reduce the right-hand side of addition if it is not a value. This rule additionally requires

the left-hand side to already be a value. Basically, the arguments of addition must be evaluated from left to right

in order for AddExpr2 to be applicable.

• AddError1: Applying addition to values of incorrect types results in Error and panic trace.

• AddError2: An addition expression reduces Error if its left-hand reduces to Error.

• AddError3: An addition expression reduces to Error if its right-hand side reduces to Error. Similarly to

AddExpr2, the AddError3 rule requires the left-hand side to already be a value.

Integer Subtraction

Integer subtraction is a binary operation that finds the difference of 2 integer arguments.

SubInt

v1 and v2 are integers

[ T ] v1 - v2 ⇝ [ T ] v1 − v2

SubExpr1

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1 - n ⇝ [ T2 ] m2 - n

SubExpr2

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] v - m1 ⇝ [ T2 ] v - m2

SubError1

v1 or v2 are not integers

[ T ] v1 - v2 ⇝ [ "Panic" :: T ] Error

SubError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m - n ⇝ [ T2 ] Error

SubError3

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] v - m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• SubInt: Interpret syntactic v1 - v2 as mathematical subtraction v1 − v2 if applied to integers v1 and v2.

• SubExpr1: Structurally reduce the left-hand side of subtraction if it is not a value.

• SubExpr2: Structurally reduce the right-hand side of subtraction if it is not a value. This rule additionally requires

the left-hand side to already be a value. Basically, the arguments of subtraction must be evaluated from left to right

in order for SubExpr2 to be applicable.

• SubError1: Applying subtraction to values of incorrect types results in Error and panic trace.

• SubError2: A subtraction expression reduces to Error if its left-hand side reduces to Error.

• SubError3: A subtraction expression reduces to Error if its right-hand side reduces to Error. Similarly to

SubExpr2, the SubError3 rule requires the left-hand side to already be a value.

5

Integer Multiplication

Integer multiplication is a binary operation that finds the product of 2 integer arguments.

MulInt

v1 and v2 are integers

[ T ] v1 * v2 ⇝ [ T ] v1 × v2

MulExpr1

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1 * n ⇝ [ T2 ] m2 * n

MulExpr2

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] v * m1 ⇝ [ T2 ] v * m2

MulError1

v1 or v2 are not integers

[ T ] v1 * v2 ⇝ [ "Panic" :: T ] Error

MulError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m * n ⇝ [ T2 ] Error

MulError3

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] v * m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• MulInt: Interpret syntactic v1 * v2 as mathematical multiply v1 × v2 if applied to integers v1 and v2.

• MulExpr1: Structurally reduce the left-hand side of multiplication if it is not a value.

• MulExpr2: Structurally reduce the right-hand side of multiplication if it is not a value. This rule additionally

requires the left-hand side to already be value. Basically, the arguments of multiplication must be evaluated from

left to right in order for MulExpr2 to be applicable.

• MulError1: Applying multiplication to values of incorrect types results in Error and panic trace.

• MulError2: A multiplication expression reduces to Error if its left-hand side reduces to Error.

• MulError3: A multiplication expression reduces to Error if its right-hand side reduces to Error. Similarly to

MulExpr2, the MulError3 rule requires the left-hand side to already be a value.

Integer Division

Integer division is a binary operation that finds the truncated quotient of 2 integer arguments. Truncated quotient (written

as ⌊

v1

v2

⌋) basically tells us how many times v2 cleanly divides v1.

DivInt

v1 and v2 are integers v2 ̸= 0

[ T ] v1 / v2 ⇝ [ T ] ⌊

v1

v2

⌋

DivExpr1

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1 / n ⇝ [ T2 ] m2 / n

DivExpr2

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] v / m1 ⇝ [ T2 ] v / m2

DivError0

v1 and v2 are integers v2 = 0

[ T ] v1 / v2 ⇝ [ "Panic" :: T ] Error

DivError1

v1 or v2 are not integers

[ T ] v1 / v2 ⇝ [ "Panic" :: T ] Error

DivError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m / n ⇝ [ T2 ] Error

DivError3

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] v / m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• DivInt: Interpret syntactic v1 / v2 as truncated quotient ⌊

v1

v2

⌋ if applied to integers v1 and v2 where v2 ̸= 0.

Note: The Div command from the stack language performs truncated quotient.

• DivExpr1: Structurally reduce the left-hand side of division if it is not a value.

• DivExpr2: Structurally reduce the right-hand side of division if it is not a value. This rule additionally requires

the left-hand side to already be a value. Basically, the arguments of division must be evaluated from left to right in

order for DivExpr2 to be applicable.

• DivError0: Applying division to integers v1 and v2 where v2 = 0 results in Error and panic trace

• DivError1: Applying division to values of incorrect types results in Error and panic trace.

• DivError2: A division expression reduces to Error if its left-hand side reduces to Error.

• DivError3: A division expression reduces to Error if its right-hand side reduces to Error. Similarly to DivExpr2,

the DivError3 rule requires the left-hand side to already be a value.

6

Integer Modulo

Integer modulo is a binary operation that finds the division remainder of 2 integer arguments. Due to the fact that there

is no modulo command in the stack language, your compiler must implement integer modulo as a series of primitive

commands supported by the stack language that produce the correct result and trace when evaluated.

ModInt

v1 and v2 are integers v2 ̸= 0

[ T ] v1 mod v2 ⇝ [ T ] v1 − v2⌊

v1

v2

⌋

ModExpr1

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1 mod n ⇝ [ T2 ] m2 mod n

ModExpr2

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] v mod m1 ⇝ [ T2 ] v mod m2

ModError0

v1 and v2 are integers v2 = 0

[ T ] v1 mod v2 ⇝ [ "Panic" :: T ] Error

ModError1

v1 or v2 are not integers

[ T ] v1 mod v2 ⇝ [ "Panic" :: T ] Error

ModError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m mod n ⇝ [ T2 ] Error

ModError3

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] v mod m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• ModInt: Interpret syntactic v1 mod v2 as integer modulo v1 − v2⌊

v1

v2

⌋ if applied to integers v1 and v2 where v2 ̸= 0.

Hint: Given a modulo expression m, transform it into an equivalent expression n comprised of only operators

supported by the stack language. Now compile expression n stead instead of m.

• ModExpr1: Structurally reduce the left-hand side of modulo if it is not a value.

• ModExpr2: Structurally reduce the right-hand side of modulo if it is not a value. This rule additionally requires

the left-hand side to already be a value. Basically, the arguments of modulo must be evaluated from left to right in

order for ModExpr2 to be applicable.

• ModError0: Applying modulo to integers v1 and v2 where v2 = 0 results in Error and panic trace

• ModError1: Applying modulo to values of incorrect types results in Error and panic trace.

• ModError2: A modulo expression reduces to Error if its left-hand side reduces to Error.

• ModError3: A modulo expression reduces to Error if its right-hand side reduces to Error. Similarly to ModExpr2, the ModError3 rule requires the left-hand side to already be a value.

Boolean And

Boolean and is a binary operation that finds the conjunction of 2 boolean arguments.

AndBool

v1 and v2 are bools

[ T ] v1 && v2 ⇝ [ T ] v1 ∧ v2

AndExpr1

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1 && n ⇝ [ T2 ] m2 && n

AndExpr2

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] v && m1 ⇝ [ T2 ] v && m2

AndError1

v1 or v2 are not bools

[ T ] v1 && v2 ⇝ [ "Panic" :: T ] Error

AndError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m && n ⇝ [ T2 ] Error

AndError3

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] v && m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• AndInt: Interpret syntactic v1 && v2 as conjunction v1 ∧ v2 if applied to booleans v1 and v2.

• AndExpr1: Structurally reduce the left-hand side of and if it is not a value.

• AndExpr2: Structurally reduce the right-hand side of and if it is not a value. This rule additionally requires the

left-hand side to already be a value. Basically, the arguments of and must be evaluated from left to right in order

for AndExpr2 to be applicable.

• AndError1: Applying and to values of incorrect types results in Error and panic trace.

• AndError2: An and expression reduces to Error if its left-hand side reduces to Error.

• AndError3: An and expression reduces to Error if its right-hand side reduces to Error. Similarly to AndExpr2,

the AndError3 rule requires the left-hand side to already be a value.

7

Boolean Or

Boolean or is a binary operation that finds the disjunction of 2 boolean arguments.

OrBool

v1 and v2 are bools

[ T ] v1 || v2 ⇝ [ T ] v1 ∨ v2

OrExpr1

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1 || n ⇝ [ T2 ] m2 || n

OrExpr2

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] v || m1 ⇝ [ T2 ] v || m2

OrError1

v1 or v2 are not bools

[ T ] v1 || v2 ⇝ [ "Panic" :: T ] Error

OrError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m || n ⇝ [ T2 ] Error

OrError3

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] v || m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• OrInt: Interpret syntactic v1 || v2 as disjunction v1 ∨ v2 if applied to booleans v1 and v2.

• OrExpr1: Structurally reduce the left-hand side of or if it is not a value.

• OrExpr2: Structurally reduce the right-hand side of or if it is not a value. This rule additionally requires the

left-hand side to already be a value. Basically, the arguments of or must be evaluated from left to right in order for

OrExpr2 to be applicable.

• OrError1: Applying or to values of incorrect types results in Error and panic trace.

• OrError2: An or expression reduces to Error if its left-hand side reduces to Error.

• OrError3: An or expression reduces to Error if its right-hand side reduces to Error. Similarly to OrExpr2,

the OrError3 rule requires the left-hand side to already be a value.

Integer Less-Than

Integer less-than is a binary operation that compares the values of 2 integer arguments.

LtInt

v1 and v2 are integers

[ T ] v1 < v2 ⇝ [ T ] v1 < v2

LtExpr1

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1 < n ⇝ [ T2 ] m2 < n

LtExpr2

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] v < m1 ⇝ [ T2 ] v < m2

LtError1

v1 or v2 are not integers

[ T ] v1 < v2 ⇝ [ "Panic" :: T ] Error

LtError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m < n ⇝ [ T2 ] Error

LtError3

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] v < m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• LtInt: Interpret syntactic v1 < v2 as the less-than comparison v1 < v2 if applied to integers v1 and v2.

• LtExpr1: Structurally reduce the left-hand side of less-than if it is not a value.

• LtExpr2: Structurally reduce the right-hand side of less-than if it is not a value. This rule additionally requires

the left-hand side to already be a value. Basically, the arguments of less-than must be evaluated from left to right

in order for LtExpr2 to be applicable.

• LtError1: Applying less-than to values of incorrect types results in Error and panic trace.

• LtError2: A less-than expression reduces to Error if its left-hand side reduces to Error.

• LtError3: A less-than expression reduces to Error if its right-hand side reduces to Error. Similarly to LtExpr2,

the LtError3 rule requires the left-hand side to already be a value.

8

Integer Greater-Than

Integer greater-than is a binary operation that compares the values of 2 integer arguments.

GtInt

v1 and v2 are integers

[ T ] v1 > v2 ⇝ [ T ] v1 > v2

GtExpr1

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1 > n ⇝ [ T2 ] m2 > n

GtExpr2

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] v > m1 ⇝ [ T2 ] v > m2

GtError1

v1 or v2 are not integers

[ T ] v1 > v2 ⇝ [ "Panic" :: T ] Error

GtError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m > n ⇝ [ T2 ] Error

GtError3

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] v > m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• GtInt: Interpret syntactic v1 > v2 as the greater-than comparison v1 > v2 if applied to integers v1 and v2.

• GtExpr1: Structurally reduce the left-hand side of greater-than if it is not a value.

• GtExpr2: Structurally reduce the right-hand side of greater-than if it is not a value. This rule additionally requires

the left-hand side to already be a value. Basically, the arguments of greater-than must be evaluated from left to

right in order for GtExpr2 to be applicable.

• GtError1: Applying greater-than to values of incorrect types results in Error and panic trace.

• GtError2: A greater-than expression reduces to Error if its left-hand side reduces to Error.

• GtError3: A greater-than expression reduces to Error if its right-hand side reduces to Error. Similarly to

GtExpr2, the GtError3 rule requires the left-hand side to already be a value.

Integer Less-Than-Equal

Integer less-than-equal is a binary operation that compares the values of 2 integer arguments. Due to the fact that there is

no less-than-equal command in the stack language, your compiler must implement less-than-equal as a series of primitive

commands supported by the stack language that produce the correct result and trace when evaluated.

LteInt

v1 and v2 are integers

[ T ] v1 <= v2 ⇝ [ T ] v1 ≤ v2

LteExpr1

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1 <= n ⇝ [ T2 ] m2 <= n

LteExpr2

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] v <= m1 ⇝ [ T2 ] v <= m2

LteError1

v1 or v2 are not integers

[ T ] v1 <= v2 ⇝ [ "Panic" :: T ] Error

LteError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m <= n ⇝ [ T2 ] Error

LteError3

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] v <= m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• LteInt: Interpret syntactic v1 <= v2 as the less-than-equal comparison v1 ≤ v2 if applied to integers v1 and v2.

• LteExpr1: Structurally reduce the left-hand side of less-than-equal if it is not a value.

• LteExpr2: Structurally reduce the right-hand side of less-than-equal if it is not a value. This rule additionally

requires the left-hand side to already be a value. Basically, the arguments of less-than-equal must be evaluated from

left to right in order for LteExpr2 to be applicable.

• LteError1: Applying less-than-equal to values of incorrect types results in Error and panic trace.

• LteError2: A less-than-equal expression reduces to Error if its left-hand side reduces to Error.

• LteError3: A less-than-equal expression reduces to Error if its right-hand side reduces to Error. Similarly to

LteExpr2, the LteError3 rule requires the left-hand side to already be a value.

9

Integer Greater-Than-Equal

Integer greater-than-equal is a binary operation that compares the values of 2 integer arguments. Due to the fact that

there is no greater-than-equal command in the stack language, your compiler must implement greater-than-equal as a

series of primitive commands supported by the stack language that produce the correct result and trace when evaluated.

GteInt

v1 and v2 are integers

[ T ] v1 >= v2 ⇝ [ T ] v1 ≥ v2

GteExpr1

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1 >= n ⇝ [ T2 ] m2 >= n

GteExpr2

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] v >= m1 ⇝ [ T2 ] v >= m2

GteError1

v1 or v2 are not integers

[ T ] v1 >= v2 ⇝ [ "Panic" :: T ] Error

GteError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m >= n ⇝ [ T2 ] Error

GteError3

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] v >= m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• GteInt: Interpret syntactic v1 >= v2 as the greater-than-equal comparison v1 ≥ v2 if applied to integers v1 and v2.

• GteExpr1: Structurally reduce the left-hand side of greater-than-equal if it is not a value.

• GteExpr2: Structurally reduce the right-hand side of greater-than-equal if it is not a value. This rule additionally

requires the left-hand side to already be a value. Basically, the arguments of greater-than-equal must be evaluated

from left to right in order for GteExpr2 to be applicable.

• GteError1: Applying greater-than-equal to values of incorrect types results in Error and panic trace.

• GteError2: A greater-than-equal expression reduces to Error if its left-hand side reduces to Error.

• GteError3: A greater-than-equal expression reduces to Error if its right-hand side reduces to Error. Similarly

to GteExpr2, the GteError3 rule requires the left-hand side to already be a value.

Integer Equality

Integer equality is a binary operation that compares the values of 2 integer arguments. Due to the fact that there is

no equality command in the stack language, your compiler must implement equality as a series of primitive commands

supported by the stack language. Hint: What relationship does equality have with Lt and Gt?

EqInt

v1 and v2 are integers v1 = v2

[ T ] v1 = v2 ⇝ [ T ] true

NeqInt

v1 and v2 are integers v1 ̸= v2

[ T ] v1 = v2 ⇝ [ T ] false

EqExpr1

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1 = n ⇝ [ T2 ] m2 = n

EqExpr2

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] v = m1 ⇝ [ T2 ] v = m2

EqError1

v1 or v2 are not integers

[ T ] v1 = v2 ⇝ [ "Panic" :: T ] Error

EqError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m = n ⇝ [ T2 ] Error

EqError3

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] v = m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• EqInt: Reduce syntactic v1 = v2 to true if they are mathematically equal v1 = v2.

• NeqInt: Reduce syntactic v1 = v2 to false if they are mathematically unequal v1 ̸= v2.

• EqExpr1: Structurally reduce the left-hand side of equality if it is not a value.

• EqExpr2: Structurally reduce the right-hand side of equality if it is not a value. This rule additionally requires

the left-hand side to already be a value. Basically, the arguments of equality must be evaluated from left to right in

order for EqExpr2 to be applicable.

• EqError1: Applying equality to values of incorrect types results in Error and panic trace.

• EqError2: An equality expression reduces to Error if its left-hand side reduces to Error.

• EqError3: An equality expression reduces to Error if its right-hand side reduces to Error. Similarly to EqExpr2,

the EqError3 rule requires the left-hand side to already be a value.

10

3.7 Expressions

Let-In Expression

Let-in expressions allow one to bind values to variables.

LetVal

[ T ] let x = v in m ⇝ [ T ] m[v/x]

LetExpr

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] let x = m1 in n ⇝ [ T2 ] let x = m2 in n

LetError

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] let x = m in n ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• LetVal: A let-in expression reduces by substituting value v for variable x in expression m. The notation m[v/x]

denotes an expression obtained from replacing all instances of variable x in expression m with value v. You may

assume that the let-in expressions produced by the parse_prog function each have uniquely named variable x.

Hint: In the stack language, we can use commands Bind and Lookup to achieve the same effect as substitution.

• LetExpr: Structurally reduce the bound expression m1 if it is not a value.

• LetError: A let-in expression reduces to Error if its bound expression m reduces to Error.

Function Application

Function application applies (possibly recursive) functions to value arguments.

AppFun

[ T ] (fun f x -> m) v ⇝ [ T ] m[(fun f x -> m)/f, v/x]

AppExpr1

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1 n ⇝ [ T2 ] m2 n

AppExpr2

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] v m1 ⇝ [ T2 ] v m2

AppError1

v1 is not of the form (fun f x -> m)

[ T ] v1 v2 ⇝ [ "Panic" :: T ] Error

AppError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m n ⇝ [ T2 ] Error

AppError3

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] v m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• AppFun: An applied function is reduced by substituting argument v for variable x in function body m. Furthermore,

the function itself is substituted for variable f in m. The notation m[(fun f x -> m)/f, v/x] denotes an expression

obtained from m by replacing all instances of variable x with value v and all instances of variable f with function

(fun f x -> m). The substitution of f for (fun f x -> m) facilitates recursion by allowing the function to refer to

itself through variable f.

Hint: Given an arbitrary closure ⟨f, Vf , C⟩ in the stack language, the Call command will evaluate its local commands

C using the extended local environment f &#**1; ⟨f, Vf , C⟩ :: Vf . Can the extension f &#**1; ⟨f, Vf , C⟩ to the local

environment be utilized to achieve the same effect of substituting f for (fun f x -> m)?

• AppExpr1: Structurally reduce the left-hand side of an application expression if it is not a value.

• AppExpr2: Structurally reduce the right-hand side of an application expression if it is not a value. This rule

additionally requires the left-hand side to already be a value. Basically, the sub-expressions of application expressions

must be evaluated from left to right in order for AppExpr2 to be applicable.

• AppError1: Applying a non-function value to a value argument results in Error and panic trace.

• AppError2: An application expression reduces to Error if its left-hand side reduces to Error.

• AppError3: An application expression reduces to Error if its right-hand side reduces to Error. Similarly to

AppExpr2, the AppError3 rule requires the left-hand side to already be a value.

11

Sequence Expression

The sequence expression allows one to compose 2 expressions together for sequential evaluation.

SeqVal

[ T ] v; m ⇝ [ T ] m

SeqExpr

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] m1; n ⇝ [ T2 ] m2; n

SeqError

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] m; n ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• SeqVal: Once the left-hand side of a sequence expression has been fully evaluated, evaluate the right-hand side.

Notice that the value of the overall sequence expression is determined by the right-hand side expression m because

v on the left-hand side is discarded.

• SeqExpr: Structurally evaluate the left-hand side of a sequence expression. While the left-hand side of a sequence

expression will not impact the value of the overall expression, traces made by the left-hand side will persist even

after the left-hand side is discarded by SeqVal.

• SeqError: A sequential expression reduces to Error if its left-hand side reduces to Error.

If-Then-Else Expression

If-then-else expression facilitates program branching on boolean conditions.

IfteTrue

[ T ] if true then n1 else n2 ⇝ [ T ] n1

IfteFalse

[ T ] if false then n1 else n2 ⇝ [ T ] n2

IfteExpr

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] if m1 then n1 else n2 ⇝ [ T2 ] if m2 then n1 else n2

IfteError1

v is not a bool

[ T ] if v then n1 else n2 ⇝ [ "Panic" :: T ] Error

IfteError2

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] if m then n1 else n2 ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• IfteTrue: An if-then-else expression reduces to its then-branch if its condition is true.

• IfteFalse: An if-then-else expression reduces to its else-branch if its condition is false.

• IfteExpr: Structurally evaluate the condition of an if-then-else expression.

• IfteError1: Attempting to branch on a non-boolean value results in Error and panic trace.

• IfteError2: An if-then-else expression reduces to Error if its condition reduces to Error.

12

Trace Expression

A trace expression logs the value of its argument to the program trace T.

TraceVal

[ T ] trace v ⇝ [ toString(v) :: T ] ()

TraceExpr

[ T1 ] m1 ⇝ [ T2 ] m2

[ T1 ] trace m1 ⇝ [ T2 ] trace m2

TraceError

[ T1 ] m ⇝ [ T2 ] Error

[ T1 ] trace m ⇝ [ T2 ] Error

The meaning behind these rules can be summarized as follows.

• TraceVal: If trace is applied to value v, prepend the string representation of v to T and reduce to unit value ().

• TraceExpr: Structurally evaluate the argument of trace.

• TraceError: A trace expression reduces to Error if its argument reduces to Error.

Given an arbitrary value v in the high-level language, the string obtained from toString(v) is the same string representation

of v’s corresponding stack language value. The following equations illustrate the strings expected for typical inputs.

toString(123) = "123" (1)

toString(true) = "True" (2)

toString(false) = "False" (3)

toString(()) = "Unit" (4)

toString(fun abc x -> m) = "Fun<abc>" (5)

Notice that these equations are missing the symbol case of the stack language. This is because variables in the high-level

language are always bound by let-expressions or function parameters and never appear in isolation. In fact, the parse_prog

function is raise an UnboundVariable exception and fail to parse if this criteria is not met. Consider the high-level program

let x = 1 in trace x where trace is applied to a let-bound variable. The expression reduces to trace 1 through the

LetVal rule which means that trace is no longer applied to a variable. The string "1" can now be successfully logged

by the TraceVal rule.

13

4 Compilation

In this section we demonstrate how to compile a simple high-level program into the stack language. Consider the program

(trace 1; 2) - (trace true; 3) in the high-level language. Informally, the following evaluation steps happen in order.

1. Begin evaluation of the left-hand side of subtraction expression (trace 1; 2) - (trace true; 3).

2. Begin evaluation of the left-hand side of sequence expression trace 1; 2.

3. Evaluation of trace 1 logs "1" to the trace and the sequence expression becomes (); 2.

4. Now that () is a value, (); 2 reduces to 2.

5. The left-hand side of 2 - (trace true; 3) is now an integer value, so evaluation of the right-hand side begins.

6. Begin evaluation of the left-hand side of sequence expression trace true; 3.

7. Evaluation of trace true logs "True" to the trace and the sequence expression becomes (); 3.

8. Now that () is a value, (); 3 reduces to 3.

9. Our subtraction expression is now 2 - 3 which can be reduced one last time to −1.

To capture the evaluation process of the high-level program, we maintain an compilation invariant: for a high-level

expression, the value expected of its direct evaluation is always on top of the stack after interpreting its compiled version.

We can see how this invariant comes into play during the compilation of the program given above. Compilation begins by

recursively compiling the left and right and sides of the subtraction expression. So we now have 3 subtasks: first compile

(trace 1; 2), next compile (trace true; 3), finally subtract their results.

To compile (trace 1; 2), it is easy to see that this corresponds to the stack commands Push 1; Trace; Pop; Push 2;.

Notice that trace 1 is compiled to Push 1; Trace; which logs "1" and puts Unit on the stack. Our compilation invariant

holds as the value expected of directly evaluating trace 1 is on top of the stack. Next, the sequence operator (_; _), which

is compiled to Pop, removes Unit from the stack. This implements the value discarding behavior of sequence expressions.

Finally the constant 2 is compiled to Push 2. The resulting stack after executing Push 1; Trace; Pop; Push 2 is exactly 2 so

our compilation invariant is maintained for the entire (trace 1; 2) expression.

Next, (trace true; 3) is compiled to Push True; Trace; Pop; Push 3;. Following the same reasoning as before, the

invariant is maintained as the expected value 3 is on top of the stack after interpreting these commands.

Now that we have recursively compiled the sub-expressions of our original subtraction expression, we are left with the

task of composing together the compiled commands and performing subtraction. Suppose we append the compiled commands together in the following way where the commands of (trace 1; 2) occur before the commands of (trace true; 3).

Push 1; Trace; Pop; Push 2; Push True; Trace; Pop; Push 3; (1)

Interpreting these stack commands results in stack [3 :: 2 :: ϵ] and trace ["True" :: "1" :: ϵ]. In order for our compilation

invariant to hold for all of (trace 1; 2) - (trace true; 3), the integer value −1 must be on top of the stack after evaluating

its compiled commands. If we haphazardly append Sub to the end of (1), the resulting command list (2) will produce

[1 :: ϵ] which violates the compilation invariant since -1 is not on top of the stack.

✗ Push 1; Trace; Pop; Push 2; Push True; Trace; Pop; Push 3; Sub; (2)

Suppose we append the compiled commands together in the following way where the commands of (trace true; 3)

occur before the commands of (trace 1; 2). Interpreting these stack commands results in stack [2 :: 3 :: ϵ] and trace

["1" :: "True" :: ϵ]. Although the stack is in the correct state for performing Sub, the order of strings in the trace is

incorrect as it logs "True" before logging "1".

✗ Push True; Trace; Pop; Push 3; Push 1; Trace; Pop; Push 2; (3)

The correct way to perform subtraction here is to insert a Swap command before the Sub command in (2). After the Swap

command, the stack is [2 :: 3 :: ϵ] and the trace is ["True" :: "1" :: ϵ]. At this point, performing Sub results in -1 on top of

the stack so our invariant is preserved. Furthermore, the order of strings in the trace is correct.

✓ Push 1; Trace; Pop; Push 2; Push True; Trace; Pop; Push 3; Swap; Sub; (4)

14

5 Example Programs

In this section, we present some programs written in the concrete syntax of the high-level language along with their

expected traces. Interpreting their compiled commands using the stack interpreter of part2 should yield the same trace.

Sequence of Traces

trace 1; trace 2

Expected Trace: ["2" :: "1" :: ϵ]

Factorial

let rec fact x =

if x <= 0 then 1

else x * fact (x - 1)

in trace (fact 10)

Expected Trace: ["3628800" :: ϵ]

Fibonacci

let fibo x =

let rec loop i a b =

trace a;

if i < x then

loop (i + 1) b (a + b)

else a

in loop 0 0 1

in trace (fibo 10)

Expected Trace: ["55" :: "55" :: "34" :: "21" :: "13" :: "8" :: "5" :: "3" :: "2" :: "1" :: "1" :: "0" :: ϵ]

Application of an Effectful Function

let eff x = trace x in

let foo x y z = () in

foo (eff 1) (eff 2) (eff 3)

Expected Trace: ["3" :: "2" :: "1" :: ϵ]

McCarthy’s 91 Function

let rec mccarthy n =

if n > 100 then n - 10

else mccarthy (mccarthy (n + 11))

in

trace (mccarthy 22)

Expected Trace: ["91" :: ϵ]

Iterated Power Function

let rec iter n f g =

if n <= 0 then g 0

else f (iter (n - 1) f g)

in

let rec pow x = trace x; x * x in

iter 4 pow (fun _ -> 2)

Expected Trace: ["256" :: "16" :: "4" :: "2" :: ϵ]

15

Greatest Common Denominator

let rec gcd a b =

if a = 0 then b

else gcd (b mod a) a

in

trace (gcd 77 11);

trace (gcd 77 121);

trace (gcd 39 91)

Expected Trace: ["13" :: "11" :: "11" :: ϵ]

Square Root via Binary Search

let rec bsearch n i j =

let k = (i + j) / 2 in

if i > j then k

else

let sq = k * k in

if sq = n then k

else

if n > sq

then bsearch n (k + 1) j

else bsearch n i (k - 1)

in

let rec sqrt n = bsearch n 0 n in

let x = 1234 * 1234 in

trace x;

trace (sqrt x)

Expected Trace: ["1234" :: "1522756" :: ϵ]

Digits of π

let rec pi n =

let q = 1 in

let r = 180 in

let t = 60 in

let j = 2 in

let rec loop n q r t j =

if n > 0 then

let u = 3 * (3 * j + 1) * (3 * j + 2) in

let y = (q * (27 * j - 12) + 5 * r) / (5 * t) in

trace y;

let q' = 10 * q * j * (2 * j - 1) in

let r' = 10 * u * (q * (5 * j - 2) + r - y * t) in

let t' = t * u in

let j' = j + 1 in

loop (n - 1) q' r' t' j'

else ()

in

loop n q r t j

in

pi 6

請加QQ：99515681 或郵箱：99515681@qq.com   WX：codehelp