- File todo.md — part of check-in [1d67ca7cf0] at 2015-01-28 15:41:50 on branch trunk — Added note about Node's assertion module. (user: andy size: 1626)
% % Arend TODO List % Updated: Dec 29, 2014 %
Since I haven't worked on Arend in a couple months, it seems like a good place to start would be with a general code review.
Refactor TODO List
This seems like a good time to clean up a few things that turned out to not work so well.
require. There's no good reason to load all of Arend's core modules into a single object. Instead, every
require-d module should load into a separate object. In the closing part of the
functionthat wraps each module, the module should register itself in the
window.libobject that corresponds to its file name (not including path).
Similarly, I don't know if there's a good way to make web-based modules aware of their relative paths, so that we don't have to ignore paths and just use filenames for look ups. We've already run into name collisions between libs and src files.
Error handling. We need a better error handling setup than just throwing exceptions. A standard set of globally available functions
ERROR, etc. would be helpful. Similarly, having all the built-in exceptions be defined in
baseis not so useful. Better to have them defined in the modules that care about them, as actual object types.
Node.js already has an assertion module; we'd just need to make a web-compatible version.
Implementation TODO list
Resolution proof search
Proof term representation (incl. "holes" for unproved props?)