Improve TR's extra-env-lang
Instead of parsing the module's body like env-lang, export a `type-environment` form instead. That way the module may contain any auxiliary definitions or expressions that are needed. Additionally allow #:opaque and #:struct clauses for opaque and struct types in the base type environment. Update typed/syntax/stx for the new API.
This commit is contained in:
parent
d16572f003
commit
db51fdb8fd
|
@ -8,11 +8,16 @@
|
||||||
|
|
||||||
(require "../utils/utils.rkt"
|
(require "../utils/utils.rkt"
|
||||||
(for-syntax (private parse-type))
|
(for-syntax (private parse-type))
|
||||||
(for-syntax racket/base syntax/parse)
|
(for-syntax racket/base
|
||||||
|
racket/syntax
|
||||||
|
syntax/parse
|
||||||
|
syntax/struct
|
||||||
|
syntax/stx)
|
||||||
(types abbrev numeric-tower union filter-ops)
|
(types abbrev numeric-tower union filter-ops)
|
||||||
(for-syntax (types abbrev numeric-tower union filter-ops)))
|
(for-syntax (types abbrev numeric-tower union filter-ops)))
|
||||||
|
|
||||||
(provide (rename-out [-#%module-begin #%module-begin])
|
(provide type-environment
|
||||||
|
(rename-out [-#%module-begin #%module-begin])
|
||||||
require
|
require
|
||||||
(for-syntax parse-type) ; to allow resolution of Name types
|
(for-syntax parse-type) ; to allow resolution of Name types
|
||||||
(except-out (all-from-out racket/base) #%module-begin)
|
(except-out (all-from-out racket/base) #%module-begin)
|
||||||
|
@ -20,33 +25,76 @@
|
||||||
types rep private utils
|
types rep private utils
|
||||||
(for-syntax (types-out abbrev numeric-tower union filter-ops)))
|
(for-syntax (types-out abbrev numeric-tower union filter-ops)))
|
||||||
|
|
||||||
(define-syntax (-#%module-begin stx)
|
;; syntax classes for type clauses in the type-environment macro
|
||||||
|
(begin-for-syntax
|
||||||
(define-syntax-class clause
|
(define-syntax-class clause
|
||||||
|
;; form - syntax to put in the #%type-decl submodule
|
||||||
|
;; outer-form - other forms to put in outer module
|
||||||
|
#:attributes (form outer-form)
|
||||||
|
(pattern :simple-clause)
|
||||||
|
(pattern :opaque-clause)
|
||||||
|
(pattern :struct-clause))
|
||||||
|
|
||||||
|
(define-syntax-class simple-clause
|
||||||
#:description "[id type]"
|
#:description "[id type]"
|
||||||
(pattern [id:identifier ty]
|
(pattern [id:identifier ty]
|
||||||
#:with register #'(register-type (quote-syntax id) ty)))
|
#:with form #'(register-type (quote-syntax id) ty)
|
||||||
(syntax-parse stx #:literals (require provide begin)
|
#:with outer-form #'(provide id)))
|
||||||
[(mb (~optional
|
|
||||||
(~and extra (~or (begin . _)
|
(define-syntax-class opaque-clause
|
||||||
(require . args)
|
#:description "[#:opaque type pred]"
|
||||||
(provide . args)))
|
(pattern [#:opaque type:id pred:id]
|
||||||
#:defaults ([extra #'(void)]))
|
#:with form
|
||||||
~! binding:clause ...)
|
#'(begin
|
||||||
#'(#%plain-module-begin
|
(register-type (quote-syntax id)
|
||||||
extra
|
(make-pred-ty (make-Opaque #'pred)))
|
||||||
(require (for-syntax typed-racket/env/env-req))
|
(register-type-name (quote-syntax type)
|
||||||
(begin-for-syntax
|
(make-Opaque #'pred)))
|
||||||
(module* #%type-decl #f
|
#:with outer-form #'(begin
|
||||||
(#%plain-module-begin ;; avoid top-level printing and config
|
;; FIXME: same as the one used in prims
|
||||||
(require typed-racket/types/numeric-tower typed-racket/env/type-name-env
|
;; lift out to utility module maybe
|
||||||
typed-racket/env/global-env typed-racket/env/type-alias-env
|
(define-syntax (type stx)
|
||||||
typed-racket/types/struct-table typed-racket/types/abbrev
|
(raise-syntax-error 'type-check
|
||||||
(rename-in racket/private/sort [sort raw-sort]))
|
"type name used out of context"
|
||||||
;; FIXME: add a switch to turn contracts on for testing
|
stx
|
||||||
binding.register ...)))
|
(and (stx-pair? stx) (stx-car stx))))
|
||||||
(begin-for-syntax (add-mod! (variable-reference->module-path-index
|
(provide type pred))))
|
||||||
(#%variable-reference))))
|
|
||||||
(provide binding.id ...))]
|
(define-syntax-class struct-clause
|
||||||
[(mb . rest)
|
#:description "[#:struct name ([field : type] ...)]"
|
||||||
#'(mb (begin) . rest)]))
|
;; FIXME: support other struct options
|
||||||
|
(pattern [#:struct name:id ([field:id (~datum :) type:expr] ...)
|
||||||
|
(~optional (~seq #:extra-constructor-name extra:id)
|
||||||
|
#:defaults ([extra #f]))]
|
||||||
|
#:with form #'(d-s name ([field : type] ...))
|
||||||
|
#:with outer-form #'(provide (struct-out name)))))
|
||||||
|
|
||||||
|
(define-syntax (-#%module-begin stx)
|
||||||
|
(syntax-parse stx
|
||||||
|
[(mb e ...)
|
||||||
|
#'(#%plain-module-begin
|
||||||
|
(require (for-syntax typed-racket/env/env-req))
|
||||||
|
e ...
|
||||||
|
;; need to register this module
|
||||||
|
(begin-for-syntax (add-mod! (variable-reference->module-path-index
|
||||||
|
(#%variable-reference)))))]))
|
||||||
|
|
||||||
|
;; macro that actually sets up the #%type-decl, should be used
|
||||||
|
;; at most once per extra-env-lang module
|
||||||
|
(define-syntax (type-environment stx)
|
||||||
|
(syntax-parse stx
|
||||||
|
[(_ binding:clause ...)
|
||||||
|
#'(begin
|
||||||
|
(begin-for-syntax
|
||||||
|
(module* #%type-decl #f
|
||||||
|
(#%plain-module-begin ;; avoid top-level printing and config
|
||||||
|
(require typed-racket/types/numeric-tower typed-racket/env/type-name-env
|
||||||
|
typed-racket/env/global-env typed-racket/env/type-alias-env
|
||||||
|
typed-racket/types/struct-table typed-racket/types/abbrev
|
||||||
|
typed-racket/typecheck/tc-structs
|
||||||
|
(only-in typed-racket/rep/type-rep make-Name make-Opaque)
|
||||||
|
(rename-in racket/private/sort [sort raw-sort]))
|
||||||
|
;; FIXME: add a switch to turn contracts on for testing
|
||||||
|
binding.form ...)))
|
||||||
|
binding.outer-form ...)]))
|
||||||
|
|
||||||
|
|
|
@ -2,30 +2,38 @@
|
||||||
|
|
||||||
(require syntax/stx)
|
(require syntax/stx)
|
||||||
|
|
||||||
[stx-null? (make-pred-ty (Un (-val '()) (-Syntax (-val '()))))]
|
(begin-for-syntax
|
||||||
[stx-pair? (make-pred-ty (Un (-pair Univ Univ) (-Syntax (-pair Univ Univ))))]
|
(define (-stx-list type)
|
||||||
[stx-list? (make-pred-ty (Un (-lst Univ) (-Syntax (-lst Univ))))]
|
(Un (-lst type) (-Syntax (-lst type)))))
|
||||||
[stx-car (-poly (a b)
|
|
||||||
(cl->*
|
|
||||||
(-> (-pair a b) a)
|
|
||||||
(-> (-lst a) a)
|
|
||||||
(-> (-Syntax (-pair a b)) (-Syntax a))
|
|
||||||
(-> (-Syntax (-lst a)) (-Syntax a))))]
|
|
||||||
[stx-cdr (-poly (a b)
|
|
||||||
(cl->*
|
|
||||||
(-> (-pair a b) b)
|
|
||||||
(-> (-lst a) (-lst a))
|
|
||||||
(-> (-Syntax (-pair a (-lst b))) (-lst (-Syntax b)))
|
|
||||||
(-> (-Syntax (-pair a b)) (-Syntax b))
|
|
||||||
(-> (-Syntax (-lst a)) (-lst (-Syntax a)))))]
|
|
||||||
[stx-map (-polydots (c a b)
|
|
||||||
(cl->*
|
|
||||||
(-> (-> (-Syntax a) c) (-pair a (-lst a)) (-pair c (-lst c)))
|
|
||||||
(-> (-> (-Syntax a) c) (-Syntax (-pair a (-lst a))) (-pair c (-lst c)))
|
|
||||||
((list
|
|
||||||
((list (-Syntax a)) ((-Syntax b) b) . ->... . c)
|
|
||||||
(Un (-lst a) (-Syntax (-lst a))))
|
|
||||||
((Un (-lst b) (-Syntax (-lst b))) b) . ->... .(-lst c))))]
|
|
||||||
[module-or-top-identifier=?
|
|
||||||
(-> (-Syntax -Symbol) (-Syntax -Symbol) -Boolean)]
|
|
||||||
|
|
||||||
|
(type-environment
|
||||||
|
[stx-null? (make-pred-ty (Un (-val '()) (-Syntax (-val '()))))]
|
||||||
|
[stx-pair? (make-pred-ty (Un (-pair Univ Univ) (-Syntax (-pair Univ Univ))))]
|
||||||
|
[stx-list? (make-pred-ty (-stx-list Univ))]
|
||||||
|
[stx->list (-poly (a)
|
||||||
|
(cl->* (-> (-lst a) (-lst a))
|
||||||
|
(-> (-Syntax (-lst a)) (-lst (-Syntax a)))
|
||||||
|
(-> (-Syntax Univ) (-val #f))))]
|
||||||
|
[stx-car (-poly (a b)
|
||||||
|
(cl->*
|
||||||
|
(-> (-pair a b) a)
|
||||||
|
(-> (-lst a) a)
|
||||||
|
(-> (-Syntax (-pair a b)) (-Syntax a))
|
||||||
|
(-> (-Syntax (-lst a)) (-Syntax a))))]
|
||||||
|
[stx-cdr (-poly (a b)
|
||||||
|
(cl->*
|
||||||
|
(-> (-pair a b) b)
|
||||||
|
(-> (-lst a) (-lst a))
|
||||||
|
(-> (-Syntax (-pair a (-lst b))) (-lst (-Syntax b)))
|
||||||
|
(-> (-Syntax (-pair a b)) (-Syntax b))
|
||||||
|
(-> (-Syntax (-lst a)) (-lst (-Syntax a)))))]
|
||||||
|
[stx-map (-polydots (c a b)
|
||||||
|
(cl->*
|
||||||
|
(-> (-> (-Syntax a) c) (-pair a (-lst a)) (-pair c (-lst c)))
|
||||||
|
(-> (-> (-Syntax a) c) (-Syntax (-pair a (-lst a))) (-pair c (-lst c)))
|
||||||
|
((list
|
||||||
|
((list (-Syntax a)) ((-Syntax b) b) . ->... . c)
|
||||||
|
(Un (-lst a) (-Syntax (-lst a))))
|
||||||
|
((Un (-lst b) (-Syntax (-lst b))) b) . ->... .(-lst c))))]
|
||||||
|
[module-or-top-identifier=?
|
||||||
|
(-> (-Syntax -Symbol) (-Syntax -Symbol) -Boolean)])
|
||||||
|
|
|
@ -0,0 +1,28 @@
|
||||||
|
#lang typed/racket
|
||||||
|
|
||||||
|
;; Test that the typed/syntax/stx library can be used
|
||||||
|
|
||||||
|
(require typed/syntax/stx
|
||||||
|
typed/rackunit)
|
||||||
|
|
||||||
|
(check-true (stx-null? null))
|
||||||
|
(check-true (stx-null? #'()))
|
||||||
|
(check-false (stx-null? #'(a)))
|
||||||
|
|
||||||
|
(check-true (stx-pair? (cons #'a #'b)))
|
||||||
|
(check-true (stx-pair? #'(a . b)))
|
||||||
|
|
||||||
|
(check-true (stx-list? #'(a b c d)))
|
||||||
|
(check-false (stx-list? #'a))
|
||||||
|
|
||||||
|
(syntax-e (car (stx->list #'(a b c d))))
|
||||||
|
(add1 (car (stx->list '(1 2 3))))
|
||||||
|
|
||||||
|
(stx-car #'(a b))
|
||||||
|
(stx-cdr #'(a b))
|
||||||
|
|
||||||
|
(stx-map (λ: ([id : Identifier]) (free-identifier=? id #'a))
|
||||||
|
#'(a b c d))
|
||||||
|
|
||||||
|
(module-or-top-identifier=? #'a #'b)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user