suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

added keywords #:mode/#:submode + module turnstile/mode

Browse Source 
closes #18
This commit is contained in:
Milo Turner 2017-08-23 14:10:04 -04:00 committed by Stephen Chang
parent fe5adac3db
commit 3ea1f05c51
3 changed files with 190 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

70
turnstile/mode.rkt Normal file
View File

@ -0,0 +1,70 @@
#lang racket/base
(provide (struct-out mode)
make-mode
current-mode
with-mode
make-param-mode)
;; mode object. contains setup routine and teardown routine
;; as fields.
(struct mode (setup-fn teardown-fn))
(define (make-mode #:setup [setup-fn void]
#:teardown [teardown-fn void])
(mode setup-fn teardown-fn))
;; apply the given mode for the successive expressions.
;; e.g.
;; (with-mode (mode (λ () (display "before "))
;; (λ () (display "after\n")))
;; (display "middle "))
;; ->
;; before middle after
;;
;; (with-mode <mode> <body> ...)
(define-syntax-rule (with-mode mode-expr body ...)
(let* ([the-mode mode-expr])
((mode-setup-fn the-mode))
(begin0 (parameterize ([current-mode the-mode]) body ...)
((mode-teardown-fn the-mode)))))
;; the current set mode. useful for #:submode/mode
(define current-mode
(make-parameter (mode void void)))
;; returns a mode that sets the given
;; parameter to the given value, for its duration.
;; similar to (parameterize ([P value]) ...)
;;
;; make-param-mode : ∀T. (parameterof T) T -> mode?
(define (make-param-mode P value)
(let* ([swap! (λ ()
(let ([cur (P)])
(P value)
(set! value cur)))])
(mode swap! swap!)))
(module+ test
(require rackunit)
(define color (make-parameter 'red))
(define ->blue (make-param-mode color 'blue))
(define ->green (make-param-mode color 'green))
(with-mode ->blue
(check-equal? (color) 'blue))
(check-equal? (color) 'red)
(with-mode ->green
(check-equal? (color) 'green)
(with-mode ->blue
(check-equal? (color) 'blue))
(check-equal? (color) 'green))
)

101
turnstile/scribblings/reference.scrbl
View File

@ -2,6 +2,7 @@
@(require scribble/example racket/sandbox
(for-label racket/base
turnstile/mode
(except-in turnstile/turnstile ⊢ stx mk-~ mk-?))
"doc-utils.rkt" "common.rkt")
@ -59,15 +60,17 @@ and then press Control-@litchar{\}.
[expr-template (code:line @#,racket[quasisyntax] @#,tech:template)]
[type-template (code:line @#,racket[quasisyntax] @#,tech:template)]
[key identifier?]
[premise (code:line [⊢ tc ...] ooo ...)
(code:line [ctx ⊢ tc ...] ooo ...)
(code:line [ctx-elem ... ⊢ tc ...] ooo ...)
(code:line [ctx ctx ⊢ tc ...] ooo ...)
[premise (code:line [⊢ tc ... prem-options] ooo ...)
(code:line [ctx-elem ... ⊢ tc ... prem-options] ooo ...)
(code:line [ctx ⊢ tc ... prem-options] ooo ...)
(code:line [ctx ctx ⊢ tc ... prem-options] ooo ...)
(code:line [⊢ . tc-elem] ooo ...)
(code:line [ctx ⊢ . tc-elem] ooo ...)
(code:line [ctx-elem ... ⊢ . tc-elem] ooo ...)
(code:line [ctx ⊢ . tc-elem] ooo ...)
(code:line [ctx ctx ⊢ . tc-elem] ooo ...)
type-relation
(code:line #:mode mode-expr (premise ...))
(code:line #:submode fn-expr (premise ...))
(code:line @#,racket[syntax-parse] @#,tech:pat-directive)]
[ctx (ctx-elem ...)]
[ctx-elem (code:line [id ≫ id key template ... ...] ooo ...)
@ -83,6 +86,9 @@ and then press Control-@litchar{\}.
(code:line [type-template τ= type-template #:for expr-template] ooo ...)
(code:line [type-template τ⊑ type-template] ooo ...)
(code:line [type-template τ⊑ type-template #:for expr-template] ooo ...)]
[prem-options (code:line)
(code:line #:mode mode-expr)
(code:line #:submode fn-expr)]
[conclusion [⊢ expr-template ⇒ type-template]
[⊢ expr-template ⇒ key template]
[⊢ expr-template (⇒ key template) ooo ...]
@ -142,6 +148,26 @@ pattern @racket[x ... y ...] will not work as expected.
For convenience, lone identifiers written to the left of the turnstile are
automatically treated as type variables.
@italic{Modes}
The keyword @racket[#:mode], when appearing at end of a typechecking rule,
sets the parameter @racket[current-mode] to the @racket[mode] object supplied
by @racket[_mode-expr], for the extent of that rule. @racket[#:mode], when
appearing as its own premise, sets the @racket[current-mode] parameter for the
extent of all the grouped sub-premises.
The keyword @racket[#:submode] is similar to @racket[#:mode], but it calls
@racket[(_fn-expr (current-mode))] to obtain the new mode object. Thus,
@racket[#:mode (_fn-expr (current-mode))] is identical to @racket[#:submode
_fn-expr].
See @secref{Modes} for more details.
WARNING: @racket[#:mode] is unaware of the backtracking behavior of
@racket[syntax-parse]. If pattern backtracking escapes a @racket[#:mode] group, it may
leave @racket[current-mode] in an undesirable state.
@; ----------------------------------------------------------------------------
@bold{Conclusion}
@ -692,7 +718,70 @@ The possible variances are:
@defproc[(variance? [v any/c]) boolean/c]{
Predicate that recognizes the variance values.}
@section{Modes}
@defmodule[turnstile/mode #:use-sources (turnstile/mode)]
@(define mode-ev
(let ([ev (make-base-eval)])
(ev '(require turnstile/mode))
ev))
Modes are typically used by the @racket[#:mode] and @racket[#:submode]
keywords in @racket[define-typed-syntax] (and related forms). When judgements
are parameterized by a @racket[mode] value, the parameter
@racket[current-mode] is set to that value for the extend of the
sub-premises. Additionally, the function @racket[mode-setup-fn] is called
before setting @racket[current-mode], and the function
@racket[mode-teardown-fn] is called after @racket[current-mode] is restored to
its previous value.
@defstruct*[mode ([setup-fn (-> any)] [teardown-fn (-> any)])]{
Structure type for modes. Modes can be used to parameterize type judgements
or groups of type judgements, to give additional context and to help enable
flow-sensitive languages.
User defined modes should be defined as structs that inherit from @racket[mode].
}
@defproc[(make-mode [#:setup setup-fn (-> any) void]
[#:teardown teardown-fn (-> any) void]) mode?]{
Constructs a new @racket[mode] object with the given setup and teardown functions.
}
@defparam[current-mode mode mode? #:value (make-mode)]{
A parameter that holds the current mode. Typically parameterized using the keywords
@racket[#:mode] and @racket[#:submode] from @racket[define-typed-syntax] forms.
}
@defform[(with-mode mode-expr body ...+)
#:contracts ([mode-expr mode?])]{
The result of @racket[with-mode] is the result of the last @racket[_body].
The parameter @racket[current-mode] is assigned to the result of
@racket[_mode-expr] for the extent of the @racket[_body] expressions. The
function @racket[mode-setup-fn] is called on the result of
@racket[_mode-expr] before @racket[current-mode] is set, and the function
@racket[mode-teardown-fn] is called after @racket[current-mode] is restored
to its previous value.
@examples[#:eval mode-ev
(define-struct (my-mode mode) ())
(define M (make-my-mode (λ () (displayln "M setup"))
(λ () (displayln "M teardown"))))
(with-mode M
(displayln (current-mode)))]}
@defproc[(make-param-mode [param parameter?] [value any/c]) mode?]{
Creates a @racket[mode] that assigns the given parameter to the given
value for the extent of the mode.
@examples[#:eval mode-ev
(define current-scope (make-parameter 'outer))
(with-mode (make-param-mode current-scope 'inner)
(displayln (current-scope)))]}
@section{Miscellaneous Syntax Object Functions}
These are all phase 1 functions.

43
turnstile/turnstile.rkt
View File

@ -1,6 +1,6 @@
#lang racket/base
(provide (except-out (all-from-out macrotypes/typecheck)
(provide (except-out (all-from-out macrotypes/typecheck)
-define-typed-syntax -define-syntax-category)
define-typed-syntax
define-typed-variable-syntax
@ -66,8 +66,9 @@
(module syntax-classes racket/base
(provide (all-defined-out))
(require (for-meta 0 (submod ".." typecheck+))
(for-meta -1 (submod ".." typecheck+)
(except-in macrotypes/typecheck #%module-begin mk-~ mk-?))
(for-meta -1 (submod ".." typecheck+)
(except-in macrotypes/typecheck #%module-begin mk-~ mk-?)
"mode.rkt")
(for-meta -2 (except-in macrotypes/typecheck #%module-begin)))
(define-syntax-class ---
[pattern dashes:id
@ -91,7 +92,7 @@
(define (add-lists stx n)
(cond [(zero? n) stx]
[else (add-lists (list stx) (sub1 n))]))
(define-splicing-syntax-class props
[pattern (~and (~seq stuff ...) (~seq (~seq k:id v) ...))])
(define-splicing-syntax-class ⇒-prop
@ -229,10 +230,10 @@
(attribute opts.wrap)))])
(define-splicing-syntax-class tc-post-options
#:attributes (wrap)
[pattern (~seq #:mode x:id v:expr)
#:attr wrap (λ (stx) #`(parameterize ([x v]) #,stx))]
[pattern (~seq #:modes ([x:id v:expr] ...))
#:attr wrap (λ (stx) #`(parameterize ([x v] ...) #,stx))]
[pattern (~seq #:mode mode-expr)
#:attr wrap (λ (stx) #`(with-mode mode-expr #,stx))]
[pattern (~seq #:submode fn-expr)
#:attr wrap (λ (stx) #`(with-mode (fn-expr (current-mode)) #,stx))]
)
(define-splicing-syntax-class tc-clause
#:attributes (pat)
@ -319,20 +320,26 @@
[pattern (~seq #:fail-unless condition:expr message:expr)
#:with pat
#'(~post (~fail #:unless condition message))]
[pattern (~seq #:mode param:id value:expr (sub-clause:clause ...))
#:with tmp (generate-temporary #'param)
[pattern (~seq #:mode mode-expr (sub-clause:clause ...))
#:with (the-mode tmp) (generate-temporaries #'(the-mode tmp))
#:with pat
#'(~and (~do (define tmp [param])
[param value])
#'(~and (~do (define the-mode mode-expr)
((mode-setup-fn the-mode))
(define tmp (current-mode))
(current-mode the-mode))
sub-clause.pat ...
(~do [param tmp]))]
[pattern (~seq #:modes ([param:id value:expr] ...) (sub-clause:clause ...))
#:with (tmp ...) (generate-temporaries #'[param ...])
(~do (current-mode tmp)
((mode-teardown-fn the-mode))))]
[pattern (~seq #:submode fn-expr (sub-clause:clause ...))
#:with (the-mode tmp) (generate-temporaries #'(the-mode tmp))
#:with pat
#'(~and (~do (define tmp [param]) ...
[param value] ...)
#'(~and (~do (define the-mode (fn-expr (current-mode)))
((mode-setup-fn the-mode))
(define tmp (current-mode))
(current-mode the-mode))
sub-clause.pat ...
(~do [param tmp] ...))]
(~do (current-mode tmp)
((mode-teardown-fn the-mode))))]
)
(define-syntax-class last-clause
#:datum-literals (⊢ ≫ ≻ ⇒ ⇐)