Data for "Toatie --- Functional Hardware Description with Dependent Types"

This repository contains all of the source files the "toatie" hardware description language and its compiler.
The dataset includes a reproducible build environment using nix, the compiler sources, standard libraries, example circuits, and test scripts.

This is an extension of Tiny Idris --- introduced by Edwin Brady at SPLV20. Our main additions to support hardware description include erasure/irrelevance of non-synthesisable terms, staging for circuit generators, deriving bit representations, and the synthesis itself.