Information for Developers

Tests

The tests folder contains tests written with Python's unittest library. Run them with

$ python3 -m unittest -b tests/*.py

(The -b flag "buffers" output so that Python only shows output from failing tests.)

Code Organization

The cozy/codegen folder implements source code generation for C++ and Java.

---

Equality in Cozy

There are many different notions of "equality" between values and between expressions in Cozy. Developers need to know the differences.

Most values like ints have only one kind of equality. In Cozy syntax it is written with ==, and in Python the values are also compared with ==. However, bags and sets have two kinds of equality: == and === in Cozy syntax. Double-equals equality means "contain the same elements" while triple-equals ("deep") equality means "all observable properties of these bags are the same". Expressions for == are constructed with EEq while expressions for === are constructed with EDeepEq. (Note that === is not part of Cozy's concrete syntax.) There are operators like the whose behavior depends on the order of elements in a bag or set; the A and the B might give different output even if A == B. However they will give the same output if A === B. In Python, the == operator implements Cozy triple-equals on values, while values_equal implements Cozy double-equals.

Expressions have three different kinds of equality: syntactic equality, alpha equivalence, and semantic equality.

• syntactic equality means they are the same expression, right down to the names of variables
• alpha equivalence means they are the same expression, but variables can be renamed if it doesn't affect the meaning of the expression
• semantic equivalence means the expressions produce the same output on all inputs

e1	e2	syntactically equal?	alpha equivalent?	semantically equal?
x	x	yes	yes	yes
argmin {x -> -x} list	argmin {y -> -y} list	no	yes	yes
argmin {x -> -x} list	max list	no	no	yes
x	y	no	no	no

In Python, == on Exp objects implements syntactic equality (but ignores type information). alpha_equivalent tests for alpha equivalence (but also ignores type information). valid can be used as a partial decision procedure for semantic equality (the task is undecidable, unfortunately). Usually this is written valid(EDeepEq(e1, e2)). For non-collection types, valid(EEq(e1, e2)) accomplishes the same thing.