* add ~typecheck and ~⊢ pattern expanders
So that in normal macros, syntax classes, and normal syntax-parse
expressions, you can use use the Turnstile syntax to do typechecking
* add documentation for ~typecheck and ~⊢
Previously, "type" functions were reused a lot to manipulate kinds, and other
metadata defined via `define-syntax-category`, but this meant it was impossible
to define separate behavior for some type and kind operations, e.g., type=? and
kind=?. This commit defines a separate api for each `define-syntax-category`
declaration.
Also, every `define-syntax-category` defines a new `define-NAMEd-syntax` form,
which implicitly uses the proper parameters, e.g., `define-kinded-syntax` uses
`kindcheck?`, `current-kind-eval`, and the ':: kind key by default (whereas
before, it was using typecheck?, type-eval, etc).
This commit breaks backwards compatibility. The most likely breakage results
from using a different default key for kinds. It used to be ':, the same as
types, but now the default is '::.
This commit also generalizes the contexts used with `define-NAMEd-syntax` and
`infer`.
- all contexts now accept arbitrary key-values associated with a variable
- all contexts use let* semantics, where a binding is in scope for subsequent
bindings; this means that one environment is sufficient in most scenarioes,
e.g., type and term vars can be mixed (if properly ordered)
- environments allow lone identifiers, which are treated as type variables by
default
- the former prevents using current-typecheck-relation at type/kind level
- the latter differentiates "well-formed" types (star)
from valid types (any kind)
- move define-*ed-syntax and *-eval into define-syntax-category
- turnstile must wrap define-stx-category to define new define-*ed-syntax
- add any-*? pred and any-* stx class in def-stx-category
- fixes#44
- fixes#45
- document #:arg-variances and variances; #:arr
- fixes#36
- start to split type constructor macro into (not working yet)
- ty-: expands to expanded type representation
- ty: performs kindchecking and expands to ty-
- this makes it easier for programmers to implement their own kind
system, but still get some turnstile conveniences like pat expanders
- not auto-providing more closely adheres to idiomatic Racket
- this commit changes:
- define-typed-syntax
- removed #:export-as option
- define-base-type
- removed #:no-provide option
- define-type-constructor
- removed #:no-provide option
- type-out helps with providing defined types
- in examples, move define and define-type-alias to ext-stlc
- fix bug in reuse where renamed id not provided
