Commit Graph

13 Commits

Author SHA1 Message Date
Stephen Chang
115aae8e73 completely separate type and kind api, etc; generalize type environment
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
2017-02-08 13:07:24 -05:00
Stephen Chang
1c0fa751d6 split out a define-binding-type from define-type-constructor
- 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
2016-10-13 15:20:30 -04:00
Stephen Chang
a3433b9193 remove * version of pattern expanders 2016-10-12 14:10:03 -04:00
Stephen Chang
691ba9c51c Turnstile forms no longer automatically provide; add type-out
- 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
2016-10-12 10:46:05 -04:00
Stephen Chang
df4c26dd8d type=? handles binding types by default
- closes #32
2016-09-29 14:27:17 -04:00
Stephen Chang
df63a0bf57 predefine "type" stx-category and define-primop in typecheck.rkt (and turnstile) 2016-09-24 16:43:17 -04:00
Stephen Chang
d0c14c7e07 define-typed-syntax: support define-simple-macro-like single-clause syntax 2016-09-24 15:12:45 -04:00
Stephen Chang
bce55e8741 allow omitting "_ ≫" in conclusion 2016-09-24 15:12:45 -04:00
Stephen Chang
e1ea378f7d drop more parens 2016-09-24 15:12:45 -04:00
AlexKnauth
3d92dbdde3 add #lang turnstile/lang; change #lang turnstile's #%module-begin 2016-08-31 18:49:25 -04:00
AlexKnauth
e9230e0ba3 remove square brackets around syntax-parse kws 2016-08-17 17:49:37 -04:00
AlexKnauth
2ddf45f8de remove brackets around e ≫ e- 2016-07-26 11:44:17 -04:00
AlexKnauth
103086a62c rename typed-lang-builder -> turnstile 2016-06-28 13:35:51 -04:00