essentially code-complete on tosmt, modulo top-level let recs
merging ...
nits to Makefile