commit e308dad709a0ca2639a67fe7954a4b85823c52d9
parent df4c26dd8d38db87f00ac225c27fad8850c42803
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 29 Sep 2016 15:49:25 -0400
add more #:no-provide options; add eval'ed doc examples
- cant get scribble/example to automatically catch and print type errs
Diffstat:
2 files changed, 42 insertions(+), 11 deletions(-)
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
@@ -583,13 +583,16 @@
(define-syntax define-basic-checked-id-stx
(syntax-parser #:datum-literals (:)
- [(_ τ:id : kind)
+ [(_ τ:id : kind
+ (~optional (~and #:no-provide (~parse no-provide? #'#t))))
#:with #%tag (format-id #'kind "#%~a" #'kind)
#:with τ? (mk-? #'τ)
#:with τ-internal (generate-temporary #'τ)
#:with τ-expander (format-id #'τ "~~~a" #'τ)
- #'(begin
- (provide τ (for-syntax τ? τ-expander))
+ #`(begin
+ #,@(if (attribute no-provide?)
+ #'()
+ #'((provide τ (for-syntax τ? τ-expander))))
(begin-for-syntax
(define (τ? t) ;(and (identifier? t) (free-identifier=? t #'τ-internal)))
(syntax-parse t
@@ -648,9 +651,9 @@
#:with τ-expander (format-id #'τ "~~~a" #'τ)
#:with τ-expander* (format-id #'τ-expander "~a*" #'τ-expander)
#`(begin
- #,(if (attribute no-provide?)
- #'(provide)
- #'(provide τ (for-syntax τ-expander τ-expander* τ?)))
+ #,@(if (attribute no-provide?)
+ #'()
+ #'((provide τ (for-syntax τ-expander τ-expander* τ?))))
(begin-for-syntax
(define-syntax τ-expander
(pattern-expander
@@ -840,7 +843,7 @@
(andmap (λ (τ) ((current-name=?) (car τs-lst) τ)) (cdr τs-lst)))))
(define-syntax define-base-name
(syntax-parser
- [(_ (~var x id)) #'(define-basic-checked-id-stx x : name)]))
+ [(_ (~var x id) . rst) #'(define-basic-checked-id-stx x : name . rst)]))
(define-syntax define-base-names
(syntax-parser
[(_ (~var x id) (... ...)) #'(begin (define-base-name x) (... ...))]))
@@ -853,6 +856,9 @@
(define-syntax define-primop
(syntax-parser #:datum-literals (:)
+ [(define-primop op:id : τ #:no-provide)
+ #:with op/tc (generate-temporary #'op)
+ #'(define-primop op/tc op : τ)]
[(define-primop op:id : τ)
#:with op/tc (generate-temporary #'op)
#`(begin-
diff --git a/turnstile/scribblings/guide.scrbl b/turnstile/scribblings/guide.scrbl
@@ -1,6 +1,7 @@
#lang scribble/manual
-@(require (for-label racket/base
+@(require scribble/example racket/sandbox
+ (for-label racket/base
(except-in turnstile/turnstile ⊢))
"doc-utils.rkt" "common.rkt")
@@ -242,7 +243,7 @@ syntax object because the input type is automatically attached to that output.
We also define an annotation form @racket[ann], which invokes the @racket[⇐]
clause of a type rule.
-@section{Defining Primop}
+@section{Defining Primops}
The previous sections have defined type rules for @racket[#%app] and @racket[λ],
as well as a function type, but we cannot write any well-typed programs yet
@@ -322,6 +323,31 @@ language implementation:
[_ #:error (type-error #:src #'x
#:msg "Unsupported literal: ~v" #'x)]]))]
+@(define the-eval
+ (parameterize ([sandbox-output 'string]
+ [sandbox-error-output 'string]
+ [sandbox-eval-limits #f])
+ (make-base-eval #:lang "../examples/stlc+lit.rkt")))
+
+@(examples #:eval the-eval
+ (+ 1 2)
+ (((λ ([f : (→ Int Int Int)])
+ (λ ([x : Int][y : Int])
+ (f x y)))
+ +)
+ 1 2))
+
+@#reader scribble/comment-reader
+(racketblock
+ ;; eval:3.0: #%app: type mismatch: expected Int, given (→ Int Int)
+ ;; expression: (λ ((x : Int)) x)
+ ;; at: (λ ((x : Int)) x)
+ ;; in: (#%app + 1 (λ ((x : Int)) x))
+ (+ 1 (λ ([x : Int]) x))
+)
+
+
+
@section{Extending a Language}
Imagine our language from the previous section is named @tt{STLC}. Since it
@@ -408,4 +434,4 @@ 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:stx-template
-positions in Turnstile are @racket[quasisyntax]es.
-\ No newline at end of file
+positions in Turnstile are @racket[quasisyntax]es.
