From e5cedb5c337b66cd773a70337b59ffdfb0ac0b67 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 23 Sep 2016 10:28:32 -0400 Subject: [PATCH] refactor guide and reference into separate files --- turnstile/scribblings/guide.scrbl | 7 +++ turnstile/scribblings/reference.scrbl | 67 +++++++++++++++++++++++++++ turnstile/scribblings/turnstile.scrbl | 65 +------------------------- 3 files changed, 76 insertions(+), 63 deletions(-) create mode 100644 turnstile/scribblings/guide.scrbl create mode 100644 turnstile/scribblings/reference.scrbl diff --git a/turnstile/scribblings/guide.scrbl b/turnstile/scribblings/guide.scrbl new file mode 100644 index 0000000..0549b2e --- /dev/null +++ b/turnstile/scribblings/guide.scrbl @@ -0,0 +1,7 @@ +#lang scribble/manual + +@(require (for-label racket/base + (except-in turnstile/turnstile ⊢) + )) + +@title{Guide} \ No newline at end of file diff --git a/turnstile/scribblings/reference.scrbl b/turnstile/scribblings/reference.scrbl new file mode 100644 index 0000000..c6fa94a --- /dev/null +++ b/turnstile/scribblings/reference.scrbl @@ -0,0 +1,67 @@ +#lang scribble/manual + +@(require (for-label racket/base + (except-in turnstile/turnstile ⊢) + )) + +@title{Reference} + +To type some of these unicode characters in DrRacket, type +the following and then hit Control-@litchar{\}. + +@itemlist[ + @item{@litchar{\vdash} → @litchar{⊢}} + @item{@litchar{\gg} → @litchar{≫}} + @item{@litchar{\Rightarrow} → @litchar{⇒}} + @item{@litchar{\Leftarrow} → @litchar{⇐}} + @item{@litchar{\succ} → @litchar{≻}} +] + +@defform[ + #:literals (≫ ⊢ ⇒ ⇐ ≻ : --------) + (define-typed-syntax name-id option ... rule) + #:grammar + ([option syntax-parse-option] + [rule [pattern ≫ + premise + ... + -------- + conclusion] + [pattern ⇐ : expected-type ≫ + premise + ... + -------- + ⇐-conclusion]] + [premise (code:line [⊢ inf ...] ooo ...) + (code:line [ctx ⊢ inf ...] ooo ...) + (code:line [ctx ctx ⊢ inf ...] ooo ...) + (code:line [type-template τ⊑ type-template #:for expr-template]) + (code:line [type-template τ⊑ type-template #:for expr-template] ooo)] + [ctx (ctx-elem ...)] + [ctx-elem [id ≫ id : type-template] + [id ≫ id : type-template] ooo] + [inf (code:line [expr-template ≫ pattern ⇒ type-pattern] ooo ...) + (code:line [expr-template ≫ pattern ⇐ type-pattern] ooo ...)] + [conclusion [⊢ [_ ≫ expr-template ⇒ type-template]] + [_ ≻ expr-template]] + [⇐-conclusion [⊢ [_ ≫ expr-template ⇐ _]]] + [ooo ...]) + ]{ +Defines a macro that can do typechecking. It's roughly an +extension of @racket[syntax-parse] that allows writing +type-judgement-like rules that interleave typechecking and +macro expansion. + +To typecheck an expression @racket[e], it needs to expand it +to get its type. To express that, write the clause +@racket[[⊢ [e ≫ pattern ⇒ type-pattern]]]. An example use of +this would be @racket[[⊢ [e ≫ e- ⇒ τ_e]]], which binds the +pattern variables @racket[e-] and @racket[τ_e] to the expanded +version of @racket[e] and the type of it, respectively. + +To check that an expression @racket[e] has a given type +@racket[τ_expected], it also needs to expand it. To express +that, write the clause +@racket[[⊢ [e ≫ pattern ⇐ τ_expected]]]. An example of this +would be @racket[[e ≫ e- ⇐ Int]]. +} diff --git a/turnstile/scribblings/turnstile.scrbl b/turnstile/scribblings/turnstile.scrbl index 0775329..b1a4a55 100644 --- a/turnstile/scribblings/turnstile.scrbl +++ b/turnstile/scribblings/turnstile.scrbl @@ -118,69 +118,8 @@ The @racket[define-typed-syntax] is roughly an extension of @item{and the premises may be interleaved with @racket[syntax-parse] @tech{pattern directives}, e.g., @racket[#:with] or @racket[#:when].}] - - -@section{Reference} - -To type some of these unicode characters in DrRacket, type -the following and then hit Control-@litchar{\}. - -@itemlist[ - @item{@litchar{\vdash} → @litchar{⊢}} - @item{@litchar{\gg} → @litchar{≫}} - @item{@litchar{\Rightarrow} → @litchar{⇒}} - @item{@litchar{\Leftarrow} → @litchar{⇐}} - @item{@litchar{\succ} → @litchar{≻}} -] - -@defform[ - #:literals (≫ ⊢ ⇒ ⇐ ≻ : --------) - (define-typed-syntax name-id option ... rule) - #:grammar - ([option syntax-parse-option] - [rule [pattern ≫ - premise - ... - -------- - conclusion] - [pattern ⇐ : expected-type ≫ - premise - ... - -------- - ⇐-conclusion]] - [premise (code:line [⊢ inf ...] ooo ...) - (code:line [ctx ⊢ inf ...] ooo ...) - (code:line [ctx ctx ⊢ inf ...] ooo ...) - (code:line [type-template τ⊑ type-template #:for expr-template]) - (code:line [type-template τ⊑ type-template #:for expr-template] ooo)] - [ctx (ctx-elem ...)] - [ctx-elem [id ≫ id : type-template] - [id ≫ id : type-template] ooo] - [inf (code:line [expr-template ≫ pattern ⇒ type-pattern] ooo ...) - (code:line [expr-template ≫ pattern ⇐ type-pattern] ooo ...)] - [conclusion [⊢ [_ ≫ expr-template ⇒ type-template]] - [_ ≻ expr-template]] - [⇐-conclusion [⊢ [_ ≫ expr-template ⇐ _]]] - [ooo ...]) - ]{ -Defines a macro that can do typechecking. It's roughly an -extension of @racket[syntax-parse] that allows writing -type-judgement-like rules that interleave typechecking and -macro expansion. - -To typecheck an expression @racket[e], it needs to expand it -to get its type. To express that, write the clause -@racket[[⊢ [e ≫ pattern ⇒ type-pattern]]]. An example use of -this would be @racket[[⊢ [e ≫ e- ⇒ τ_e]]], which binds the -pattern variables @racket[e-] and @racket[τ_e] to the expanded -version of @racket[e] and the type of it, respectively. - -To check that an expression @racket[e] has a given type -@racket[τ_expected], it also needs to expand it. To express -that, write the clause -@racket[[⊢ [e ≫ pattern ⇐ τ_expected]]]. An example of this -would be @racket[[e ≫ e- ⇐ Int]]. -} +@include-section{guide.scrbl} +@include-section{reference.scrbl} @(bibliography (bib-entry #:key "bidirectional"