Typing of eliminators is now entirely in metafunctions. It is easier to
understand, and should lead to more efficient typing. Some of these
functions should be exposed via reflection.
* Reorganized, reimplemented, and renamed many functions related to
contexts (telescopes Ξ and apply context Θ)
* Moved some test suite stuff to the top
* Various style fixes in comments, indentation and such
* Reorganizing sections of code to be easier to read. Grouping by
similar requirements in meta-functions, and trying to reduce
dependencies between meta-functions.
* Removed explicit reductions from various meta-functions. That should
be handled by equivalence rules in type-checking.
* This commit breaks something, not sure why
* Changed all uses of (where .... ,(variable-not-in )) to use (fresh-x)
instead.
* Defined check-equiv for testing modulo α-equivalence
* Changed many check-equal? to check-equiv?. Remaining require
splitting into separate tests, e.g., checking that judgment-form
returns exactly 1 argument that is check-equiv? ...
* Made the primitive form of elim (elim t_0 t_1), allowing this form to be
considered a value when t_0 and t_1 are values.
* Moved definition of values to reduction language, and fixed it. This
fixed issues with unique decomposition, and thus fixed reduction of
eliminators.
* Enabled caching in apply-reduction-relation* to speed up results of
recursive calls.
Fixed eliminator reduction for eliminators of inductive types whose
constructors do not have the same parameters as their type. The
canonical example is ==, which has 3 parameters, but whose constructor
refl only has two.
* Added single step meta-function to core
* Expose step/syn in redex-lang
* Added macro to sugar for convenience use
* Updated relevant docs (also fixed bug in reflection docs)
Previously, reflection procedures did not properly reify/reflect syntax
after evaluating in Redex. This limited compositionality of reflection
features.
No longer. Now all reflection procedures should reify their results back
into Cur syntax, and only top-level evaluation should result in Redex
datums (or explicit calls to cur->datum).
elim was not checking that the arguments to be used for the parameters
of the inductive matched the actual parameters expected, resulting in
incorrect and non-deterministic unification, and thus incorrect
reduction when the parameters were unified incorrectly.
Yesterday's changes to sugar broke some things:
* case isn't smart enough to infer the right things in all cases yet, so
added previously existing case* for when it is necessary.
* reexport define-theorem and qed from sugar, since still used in prop.
* run is user-definable through the existing reflection features; moved
to sugar.
* define need not have special function support in curnel; moved to
sugar.
* fixed relevant documentation
