This commit breaks previous API for eliminating inductive types.
The previous eliminator for inductive types was too complex. It performed
automagic currying, making it difficult to type check, and difficult and
expensive to reduce.
The new version must be fully applied, and magic should be implemented
in the surface language. A sketch of such magic is left in sugar.rkt,
but not yet implemented.
This new version gives a 40% speed up on the Cur test
suite. Unfortunately, Redex is still the major bottleneck, so no
algorithmic gains.
* Moved cur.rkt to main.rkt, which fixes some reader issues
* Added sweet-expression tests
* Added notes about sweet-expressions to README
* Added sweet-exp as dependency to tests
The names of reflection API functions were previously confusing.
They included weird patterns that only made sense inside the Cur
implementation.
As they are Racket functions, they ought to somehow indicate that these
functions are for Cur, which they did not.
Previously, the core language of Cur, i.e. the default object language,
was stupidly providing syntax sugar.
E.g., both λ and lambda as syntax for functions.
Now, the default object language is much closer to the Curnel, and this
syntax sugar is moved to the sugar library.
* Unified the surface syntax. There are no longer distinctions between
single-arity and multi-arity function/function types.
* Removed case and case*, in favor of match, a single advanced pattern
matching construct.
* Updated all libraries, tests and documentation to use these new syntax.
* Some work to provide improved error messages in surface syntax.
Created split packages: cur, cur-lib, cur-test, cur-doc, similar to
other Racket packages, e.g., redex.
* Moved tests out of core and into cur-test
* Moved docs into cur-doc
* Moved cur implementation and libraries into cur-lib
* Added cur meta-pacakge that installs all of the above
* Match now infers the result more by adding pattern variables to
local-env while inferring types.
* Replaced uses of case* and case with match when possible
Added match, a better pattern matching construct than case.
Automatically infers inductive arguments, and feature a "recur" syntax.
Converted several functions from stdlib/nat to use this.
In dependent type system, Σ is normally the symbol for strong sums, not
signatures/declarations.
While Δ is sometimes used as an alternative to Γ, using it for
inductive signatures.
