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 multiple notions of "equality" between values and between expressions in Cozy. They are documented in value_types.py.

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.