diff --git a/turnstile/scribblings/common.rkt b/turnstile/scribblings/common.rkt new file mode 100644 index 0000000..be4af2f --- /dev/null +++ b/turnstile/scribblings/common.rkt @@ -0,0 +1,28 @@ +#lang racket/base +(provide (all-defined-out)) +(require scribble/manual) + +(define tech:stx-pats + (tech #:doc '(lib "syntax/scribblings/syntax.scrbl") "syntax patterns")) +(define tech:stx-pat + (tech #:doc '(lib "syntax/scribblings/syntax.scrbl") "syntax pattern")) +(define tech:stx-templates + (list "syntax " (tech #:doc '(lib "scribblings/guide/guide.scrbl") "templates"))) +(define tech:stx-template + (list "syntax " (tech #:doc '(lib "scribblings/guide/guide.scrbl") "template"))) +(define tech:templates + (tech #:doc '(lib "scribblings/guide/guide.scrbl") "templates")) +(define tech:template + (tech #:doc '(lib "scribblings/guide/guide.scrbl") "template")) +(define tech:pat-expanders + (tech #:doc '(lib "syntax/scribblings/syntax.scrbl") "pattern expanders")) +(define tech:pat-expander + (tech #:doc '(lib "syntax/scribblings/syntax.scrbl") "pattern expander")) +(define tech:stx-classes + (tech #:doc '(lib "syntax/scribblings/syntax.scrbl") "syntax classes")) +(define tech:stx-class + (tech #:doc '(lib "syntax/scribblings/syntax.scrbl") "syntax class")) +(define tech:pat-directives + (tech #:doc '(lib "syntax/scribblings/syntax.scrbl") "pattern directives")) +(define tech:pat-directive + (tech #:doc '(lib "syntax/scribblings/syntax.scrbl") "pattern directive")) \ No newline at end of file diff --git a/turnstile/scribblings/guide.scrbl b/turnstile/scribblings/guide.scrbl index 30ea61f..8868272 100644 --- a/turnstile/scribblings/guide.scrbl +++ b/turnstile/scribblings/guide.scrbl @@ -2,7 +2,7 @@ @(require (for-label racket/base (except-in turnstile/turnstile ⊢)) - "doc-utils.rkt") + "doc-utils.rkt" "common.rkt") @title{Guide} @@ -27,8 +27,7 @@ expansion) and type checking. These type judgements rely on two core an input in the second relation. These input and output positions conveniently correspond to - @tech{syntax patterns} and - @tech{syntax templates}, respectively, as explained below.}] + @tech:stx-pats and @tech:stx-templates, respectively, as explained below.}] For example, here are some rules that check and rewrite simply-typed lambda-calculus terms to the untyped lambda-calculus. @@ -73,9 +72,9 @@ Implementing the above judgements with Turnstile might look like The above code assumes some existing bindings: @itemlist[ @item{A @racket[→] type constructor;} - @item{a @racket[~→] @tech{pattern expander} associated with the type + @item{a @racket[~→] @tech:pat-expander associated with the type constructor;} - @item{a @racket[type] @tech{syntax class} recognizing valid types;} + @item{a @racket[type] @tech:stx-class recognizing valid types;} @item{and core Racket forms, suffixed with @litchar{-}.} ] A language defined with Turnstile must define or import the first two items @@ -86,7 +85,7 @@ A @racket[define-typed-syntax] form resembles a conventional Racket macro-definition form: the above definitions begin with an input pattern, where the leftmost identifier is the name of the macro, followed by a @racket[≫] literal, a series of premises, and finally a conclusion (the conclusion includes -the output @tech{syntax template}. +the output @tech:stx-template). The @racket[define-typed-syntax] is roughly an extension of @racket[define-syntax-parser] in that: @@ -94,9 +93,9 @@ The @racket[define-typed-syntax] is roughly an extension of @item{A programmer may specify @racket[syntax-parse] options, e.g., @racket[#:datum-literals];} @item{a pattern position may use any @racket[syntax-parse] combinators, e.g. - @racket[~and], @racket[~seq], or custom-defined @tech{pattern expanders};} + @racket[~and], @racket[~seq], or custom-defined @tech:pat-expanders;} @item{and the premises may be interleaved with @racket[syntax-parse] - @tech{pattern directives}, e.g., @racket[#:with] or @racket[#:when].}] + @tech:pat-directives, e.g., @racket[#:with] or @racket[#:when].}] @subsection{Judgements vs @racket[define-typed-syntax]} @@ -155,7 +154,7 @@ used to avoid double-expansions of the types.) @subsection{@racket[syntax-parse] directives} A @racket[define-typed-syntax] definition may also use @racket[syntax-parse] -options and @tech{pattern directives}. Here is an @racket[#%app] that reports a +options and @|tech:pat-directives|. Here is an @racket[#%app] that reports a more precise error for an arity mismatch: @label-code["Function application with a better error message" @@ -181,8 +180,8 @@ We next extend our language with a type definition: The @racket[define-type-constructor] declaration defines the @racket[→] function typ as a macro that takes at least one argument, along with the -aforementioned @racket[~→] @tech{pattern expander} for that type, which makes it -easier to match on the type in @tech{syntax patterns}. +aforementioned @racket[~→] @tech:pat-expander for that type, which makes it +easier to match on the type in @|tech:stx-pats|. @section{Defining @racket[⇐] rules} @@ -408,5 +407,5 @@ Since the new language uses subtyping, it also defines a @racket[join] function, which is needed by conditional forms like @racket[if]. The @racket[if] definition uses the @racket[current-join] parameter, to make it reusable by other languages. Observe that the output type in the -@racket[if] definition uses @racket[unquote]. In general, all @tech{syntax - template} positions in Turnstile as @racket[quasiquote]s. \ No newline at end of file +@racket[if] definition uses @racket[unquote]. In general, all @tech:stx-template +positions in Turnstile as @racket[quasiquote]s. \ No newline at end of file diff --git a/turnstile/scribblings/reference.scrbl b/turnstile/scribblings/reference.scrbl index 7c50d3e..08eb35d 100644 --- a/turnstile/scribblings/reference.scrbl +++ b/turnstile/scribblings/reference.scrbl @@ -1,8 +1,8 @@ #lang scribble/manual @(require (for-label racket/base - (except-in turnstile/turnstile ⊢) - )) + (except-in turnstile/turnstile ⊢)) + "doc-utils.rkt" "common.rkt") @title{Reference} @@ -45,10 +45,10 @@ relevant characters. Type the following and then press Control-@litchar{\}. premise ... -------- ⇐-conclusion]] - [expr-pattern (code:line @#,racket[syntax-parse] @#,tech{syntax pattern})] - [type-pattern (code:line @#,racket[syntax-parse] @#,tech{syntax pattern})] - [expr-template (code:line @#,racket[quasisyntax] @#,tech{syntax template})] - [type-template (code:line @#,racket[quasisyntax] @#,tech{syntax template})] + [expr-pattern (code:line @#,racket[syntax-parse] @#,tech:stx-pat)] + [type-pattern (code:line @#,racket[syntax-parse] @#,tech:stx-pat)] + [expr-template (code:line @#,racket[quasisyntax] @#,tech:template)] + [type-template (code:line @#,racket[quasisyntax] @#,tech:template)] [premise (code:line [⊢ inf ...] ooo ...) (code:line [ctx ⊢ inf ...] ooo ...) (code:line [ctx-elem ... ⊢ inf ...] ooo ...) @@ -58,7 +58,7 @@ relevant characters. Type the following and then press Control-@litchar{\}. (code:line [ctx-elem ... ⊢ . inf-elem] ooo ...) (code:line [ctx ctx ⊢ . inf-elem] ooo ...) type-relation - (code:line @#,racket[syntax-parse] @#,tech{pattern directive})] + (code:line @#,racket[syntax-parse] @#,tech:pat-directive)] [ctx (ctx-elem ...)] [ctx-elem (code:line [id ≫ id : type-template] ooo ...)] [inf (code:line inf-elem ooo ...)] @@ -76,7 +76,7 @@ relevant characters. Type the following and then press Control-@litchar{\}. ]{ Defines a macro that additionally performs typechecking. It uses -@racket[syntax-parse] @tech{syntax patterns} and @tech{pattern directives} and +@racket[syntax-parse] @tech:stx-pats and @tech:pat-directives and additionally allows writing type-judgement-like clauses that interleave typechecking and macro expansion. @@ -114,7 +114,7 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn Defines a base type. A @racket[(define-base-type τ)] additionally defines: @itemlist[@item{@racket[τ]: An identifier macro representing type @racket[τ].} @item{@racket[τ?]: A predicate recognizing type @racket[τ].} - @item{@racket[~τ]: A @tech{pattern expander} recognizing type @racket[τ].}]}} + @item{@racket[~τ]: A @tech:pat-expander recognizing type @racket[τ].}]}} @item{@defform[(define-base-types base-type-name-id ...)]{Defines multiple base types.}} @item{ @defform[(define-type-constructor name-id option ...) @@ -128,7 +128,7 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn @itemlist[@item{@racket[τ]: An macro for constructing an instance of type @racket[τ], with the specified arity. The default arity is @racket[= 1].} @item{@racket[τ?]: A predicate recognizing type @racket[τ].} - @item{@racket[~τ]: A @tech{pattern expander} recognizing type @racket[τ].}] + @item{@racket[~τ]: A @tech:pat-expander recognizing type @racket[τ].}] The @racket[#:arity] argument specifies valid shapes for the type. For example @racket[(define-type-constructor → #:arity >= 1)] defines an arrow type and @racket[(define-type-constructor Pair #:arity = 2)] defines a pair type. diff --git a/turnstile/scribblings/turnstile.scrbl b/turnstile/scribblings/turnstile.scrbl index a33b11e..5acaa68 100644 --- a/turnstile/scribblings/turnstile.scrbl +++ b/turnstile/scribblings/turnstile.scrbl @@ -1,8 +1,6 @@ #lang scribble/manual -@(require (for-label racket/base - (except-in turnstile/turnstile ⊢) - )) +@(require (for-label racket/base)) @title{The @racketmodname[turnstile] language}