The supported options are `-h`, `-V`, `-t`, `-T`, and `-c`.
Additional arguments are files to be loaded.
In the process, these additional changes have been made:
* `:check` has been replaced with `:printTypes`;
disabling typechecking is no longer possible.
* Ivo programs no longer allow top-level expressions;
a `main` definition must be used instead.
* Traces and type information are now printed to `STDERR`.
* The interpreter code underwent /some/ cleanup,
but more is still needed.
* Added line and block comments to the syntax
* Added `:trace`, `:clear`, `:load`, and `:check` commands to the REPL
* Added persistent declarations and a syntax for multi-expression programs
Future ideas:
* `:type` (print the type of an expression)
* `:dump` (dump all definitions to a file)
* auto-complete for commands and variable-names
* list files to load as arguments
* initial `:trace` and `:check` config as arguments
I also generalized substitution to *all* expressions (and types),
which itself involved a rewrite of the substitution function I already had.
(In hindsight, I wish I'd done that in a separate commit.)
The last four days have all been working up to this,
so I'm glad I've finally managed to integrate it into this project!
(I wrote the algorithm 4 days ago, but the infrastructure
just wasn't there to add it here.)
Trees that grow introduces a lot of boilerplate but is bound to be essentially necessary
when I add in the type checker and all sorts of builtin data types.
(I know this because I already *implemented* those things;
it's mostly a matter of trying to merge it all into this codebase).
Accomplishing this also involved restructuring the project
and rewriting a few algorithms in the process,
but those changes are fundamentally intwined with this one.
This is done by requiring applications to be at least 2 terms,
and making grouping a syntactic feature instead of a feature of applications.
I also made the code a bit more clear by handling whitespace a bit more cleanly;
now, each parser is responsible for its own trailing whitespace,
and whitespace handling is pushed down to the token level
to avoid cluttering high-level definitions with whitespace stuff.
This all also had the effect of improving error messages,
in part due to me labelling many of the parsers.
* The expression printer now knows how to use `let`, multi-argument lambdas and applications, and block arguments when appropriate.
* There is a separate type, AbstractSyntax, which separates parsing/printing logic from removing/reintroducing the more advanced syntax described above.
* Expression is now its own module because its 'show' depends on AbstractSyntax,
and I don't want the ast2expr/expr2ast stuff to be in the same module as the real lambda calculus stuff.
* Allows for multiple representations
* Evaluation strategies
* Type systems.
* No longer just the untyped lambda calculus.
* No longer "just an experiment".
James T. Martin