Information for Developers

General Tips

• Use virtualenv to keep Cozy and its dependencies isolated from the rest of your system.
• PyCharm is a good choice for developing and debugging Cozy. It has many useful features:
  • Set breakpoint: conditional or not
  • Sometimes failed assertions / exception might not be caught, move the code a bit and place a manual breakpoint
  • Watcher is awesome
  • Stepping is more reliable
  • Find usage

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/synthesis folder contains the core synthesis algorithm and some useful additions.

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

---

Using pre-commit hooks

A pre-commit hook is a script that runs when you run git commit. The commit aborts if the script fails. This pre-commit hook runs a linter and all the unit tests:

$ cat .git/hooks/pre-commit

#!/bin/bash
./lint.sh && python3 -m unittest -fb tests/*.py

$ cat lint.sh 
#!/bin/bash
cd "$(dirname "$0")"

if [[ "$1" == "" ]]; then
    ARGS="$(find cozy tests -name '*.py' -not -name 'parsetab.py')"
else
    ARGS="$@"
fi

# http://flake8.pycqa.org/en/latest/user/error-codes.html
# https://pycodestyle.readthedocs.io/en/latest/intro.html#error-codes
echo "Running flake8..."
exec flake8 \
    $(fgrep -- '--select' .travis.yml) \
    $ARGS
echo "Done!"

---

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 the Cozy Python code, == 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 expressions with non-collection types, valid(EEq(e1, e2)) accomplishes the same thing.