diff --git a/turnstile/mode.rkt b/turnstile/mode.rkt new file mode 100644 index 0000000..a60b077 --- /dev/null +++ b/turnstile/mode.rkt @@ -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 ...) +(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)) + ) diff --git a/turnstile/scribblings/reference.scrbl b/turnstile/scribblings/reference.scrbl index 1638831..81c153d 100644 --- a/turnstile/scribblings/reference.scrbl +++ b/turnstile/scribblings/reference.scrbl @@ -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. diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt index c6e1212..bd45c7d 100644 --- a/turnstile/turnstile.rkt +++ b/turnstile/turnstile.rkt @@ -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 (⊢ ≫ ≻ ⇒ ⇐)