A refactoring tool for the dependently typed programming language Pi-forall (Pi-forall re-factorer), which I have worked on during my PhD: pire
(Beware that this is a snapshot release: no effort is made to keep a history, and I may replace the contents of the repository at any time).
This work is unfinished (and the code stale), kept here nevertheless for now, some noteworthy bits therein:
- a white-space aware parser
- a zipper implementation of the syntax tree in terms of a list of functions
- and (relatively hidden - i.e. undocumented so far:) an algorithm for list-to-vector refactorings (based on the type-checking algorithm W, but inferring list/vector sizes, rather than types)
Some documentation can be found in the docs directory therein, provided as
.org files, together with the org/pandoc/shake toolchain (but not rendered as pdf/html). Rendered versions of these docs are thus provided here (they need updating, however): pire.pdf pire.html
Pire's API docs (its haddocks i.e.)
As of July 2021 Pire compiles fine again with ghc 8.8.4, with some tests already passing (utests, filetests), and some remaining issues yet to be sorted out (doctests). For more details cf. the
changes.org file in git.