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. original commit: db51fdb8fdc943971122fea32a7b593b187bd685
This commit is contained in:
Asumu Takikawa
parent
1b78da2bf6
commit
c8595e7e45
|
|
@ -8,11 +8,16 @@
|
|||
|
||||
(require "../utils/utils.rkt"
|
||||
(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)
|
||||
(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
|
||||
(for-syntax parse-type) ; to allow resolution of Name types
|
||||
(except-out (all-from-out racket/base) #%module-begin)
|
||||
|
|
@ -20,33 +25,76 @@
|
|||
types rep private utils
|
||||
(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
|
||||
;; 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]"
|
||||
(pattern [id:identifier ty]
|
||||
#:with register #'(register-type (quote-syntax id) ty)))
|
||||
(syntax-parse stx #:literals (require provide begin)
|
||||
[(mb (~optional
|
||||
(~and extra (~or (begin . _)
|
||||
(require . args)
|
||||
(provide . args)))
|
||||
#:defaults ([extra #'(void)]))
|
||||
~! binding:clause ...)
|
||||
#'(#%plain-module-begin
|
||||
extra
|
||||
(require (for-syntax typed-racket/env/env-req))
|
||||
(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
|
||||
(rename-in racket/private/sort [sort raw-sort]))
|
||||
;; FIXME: add a switch to turn contracts on for testing
|
||||
binding.register ...)))
|
||||
(begin-for-syntax (add-mod! (variable-reference->module-path-index
|
||||
(#%variable-reference))))
|
||||
(provide binding.id ...))]
|
||||
[(mb . rest)
|
||||
#'(mb (begin) . rest)]))
|
||||
#:with form #'(register-type (quote-syntax id) ty)
|
||||
#:with outer-form #'(provide id)))
|
||||
|
||||
(define-syntax-class opaque-clause
|
||||
#:description "[#:opaque type pred]"
|
||||
(pattern [#:opaque type:id pred:id]
|
||||
#:with form
|
||||
#'(begin
|
||||
(register-type (quote-syntax id)
|
||||
(make-pred-ty (make-Opaque #'pred)))
|
||||
(register-type-name (quote-syntax type)
|
||||
(make-Opaque #'pred)))
|
||||
#:with outer-form #'(begin
|
||||
;; FIXME: same as the one used in prims
|
||||
;; lift out to utility module maybe
|
||||
(define-syntax (type stx)
|
||||
(raise-syntax-error 'type-check
|
||||
"type name used out of context"
|
||||
stx
|
||||
(and (stx-pair? stx) (stx-car stx))))
|
||||
(provide type pred))))
|
||||
|
||||
(define-syntax-class struct-clause
|
||||
#:description "[#:struct name ([field : type] ...)]"
|
||||
;; 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)
|
||||
|
||||
[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 (Un (-lst Univ) (-Syntax (-lst Univ))))]
|
||||
[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)]
|
||||
(begin-for-syntax
|
||||
(define (-stx-list type)
|
||||
(Un (-lst type) (-Syntax (-lst type)))))
|
||||
|
||||
(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