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

allow omitting "_ ≫" in conclusion

Browse Source
This commit is contained in:
Stephen Chang 2016-09-22 15:25:19 -04:00
parent e1ea378f7d
commit bce55e8741
17 changed files with 180 additions and 177 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
turnstile/examples/exist.rkt
View File

@ -15,16 +15,15 @@
(define-type-constructor ∃ #:bvs = 1)
(define-typed-syntax pack
[(pack (τ:type e) as ∃τ:type) ≫
[(_ (τ:type e) as ∃τ:type) ≫
#:with (~∃* (τ_abstract) τ_body) #'∃τ.norm
#:with τ_e (subst #'τ.norm #'τ_abstract #'τ_body)
[⊢ e ≫ e- ⇐ τ_e]
--------
[⊢ _ ≫ e- ⇒ ∃τ.norm]])
[⊢ e- ⇒ ∃τ.norm]])
(define-typed-syntax open #:datum-literals (<= with)
[(open [x:id <= e_packed with X:id] e)
≫
[(_ [x:id <= e_packed with X:id] e) ≫
;; The subst below appears to be a hack, but it's not really.
;; It's the (TaPL) type rule itself that is fast and loose.
;; Leveraging the macro system's management of binding reveals this.
@ -72,4 +71,4 @@
#:with τ_x (subst #'X #'Y #'τ_body)
[([X ≫ X- : #%type]) ([x ≫ x- : τ_x]) ⊢ e ≫ e- ⇒ τ_e]
--------
[⊢ _ ≫ (let- ([x- e_packed-]) e-) ⇒ τ_e]])
[⊢ (let- ([x- e_packed-]) e-) ⇒ τ_e]])

81
turnstile/examples/ext-stlc.rkt
View File

@ -23,22 +23,22 @@
(define-base-type Char)
(define-typed-syntax #%datum
[(#%datum . b:boolean) ≫
[(_ . b:boolean) ≫
--------
[⊢ _ ≫ (#%datum- . b) ⇒ Bool]]
[(#%datum . s:str) ≫
[⊢ (#%datum- . b) ⇒ Bool]]
[(_ . s:str) ≫
--------
[⊢ _ ≫ (#%datum- . s) ⇒ String]]
[(#%datum . f) ≫
[⊢ (#%datum- . s) ⇒ String]]
[(_ . f) ≫
#:when (flonum? (syntax-e #'f))
--------
[⊢ _ ≫ (#%datum- . f) ⇒ Float]]
[(#%datum . c:char) ≫
[⊢ (#%datum- . f) ⇒ Float]]
[(_ . c:char) ≫
--------
[⊢ _ ≫ (#%datum- . c) ⇒ Char]]
[(#%datum . x) ≫
[⊢ (#%datum- . c) ⇒ Char]]
[(_ . x) ≫
--------
[_ ≻ (stlc+lit:#%datum . x)]])
[≻ (stlc+lit:#%datum . x)]])
(define-primop zero? : (→ Int Bool))
(define-primop = : (→ Int Int Bool))
@ -49,17 +49,16 @@
(define-primop not : (→ Bool Bool))
(define-typed-syntax and
[(and e1 e2) ≫
[⊢ e1 ≫ e1- ⇐ Bool]
[⊢ e2 ≫ e2- ⇐ Bool]
[(_ e ...) ≫
[⊢ e ≫ e- ⇐ Bool] ...
--------
[⊢ _ ≫ (and- e1- e2-) ⇒ Bool]])
[⊢ (and- e- ...) ⇒ Bool]])
(define-typed-syntax or
[(or e ...) ≫
[⊢ [e ≫ e- ⇐ Bool] ...]
[(_ e ...) ≫
[⊢ e ≫ e- ⇐ Bool] ...
--------
[⊢ _ ≫ (or- e- ...) ⇒ Bool]])
[⊢ (or- e- ...) ⇒ Bool]])
(begin-for-syntax
(define current-join
@ -79,68 +78,68 @@
((current-join) τ τ2))]))
(define-typed-syntax if
[(if e_tst e1 e2) ⇐ τ-expected ≫
[(_ e_tst e1 e2) ⇐ τ-expected ≫
[⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy.
[⊢ e1 ≫ e1- ⇐ τ-expected]
[⊢ e2 ≫ e2- ⇐ τ-expected]
--------
[⊢ _ ≫ (if- e_tst- e1- e2-) ⇐ _]]
[(if e_tst e1 e2) ≫
[⊢ (if- e_tst- e1- e2-)]]
[(_ e_tst e1 e2) ≫
[⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy.
[⊢ e1 ≫ e1- ⇒ τ1]
[⊢ e2 ≫ e2- ⇒ τ2]
--------
[⊢ _ ≫ (if- e_tst- e1- e2-) ⇒ (⊔ τ1 τ2)]])
[⊢ (if- e_tst- e1- e2-) ⇒ (⊔ τ1 τ2)]])
(define-base-type Unit)
(define-primop void : (→ Unit))
(define-typed-syntax begin
[(begin e_unit ... e) ⇐ τ_expected ≫
[⊢ [e_unit ≫ e_unit- ⇒ _] ...]
[(_ e_unit ... e) ⇐ τ_expected ≫
[⊢ e_unit ≫ e_unit- ⇒ _] ...
[⊢ e ≫ e- ⇐ τ_expected]
--------
[⊢ _ ≫ (begin- e_unit- ... e-) ⇐ _]]
[(begin e_unit ... e) ≫
[⊢ [e_unit ≫ e_unit- ⇒ _] ...]
[⊢ (begin- e_unit- ... e-)]]
[(_ e_unit ... e) ≫
[⊢ e_unit ≫ e_unit- ⇒ _] ...
[⊢ e ≫ e- ⇒ τ_e]
--------
[⊢ _ ≫ (begin- e_unit- ... e-) ⇒ τ_e]])
[⊢ (begin- e_unit- ... e-) ⇒ τ_e]])
(define-typed-syntax let
[(let ([x e] ...) e_body) ⇐ τ_expected ≫
[⊢ [e ≫ e- ⇒ : τ_x] ...]
[(_ ([x e] ...) e_body) ⇐ τ_expected ≫
[⊢ e ≫ e- ⇒ : τ_x] ...
[[x ≫ x- : τ_x] ... ⊢ e_body ≫ e_body- ⇐ τ_expected]
--------
[⊢ _ ≫ (let- ([x- e-] ...) e_body-) ⇐ _]]
[(let ([x e] ...) e_body) ≫
[⊢ [e ≫ e- ⇒ : τ_x] ...]
[⊢ (let- ([x- e-] ...) e_body-)]]
[(_ ([x e] ...) e_body) ≫
[⊢ e ≫ e- ⇒ : τ_x] ...
[[x ≫ x- : τ_x] ... ⊢ e_body ≫ e_body- ⇒ τ_body]
--------
[⊢ _ ≫ (let- ([x- e-] ...) e_body-) ⇒ τ_body]])
[⊢ (let- ([x- e-] ...) e_body-) ⇒ τ_body]])
; dont need to manually transfer expected type
; result template automatically propagates properties
; - only need to transfer expected type when local expanding an expression
; - see let/tc
(define-typed-syntax let*
[(let* () e_body) ≫
[(_ () e_body) ≫
--------
[_ ≻ e_body]]
[(let* ([x e] [x_rst e_rst] ...) e_body) ≫
[≻ e_body]]
[(_ ([x e] [x_rst e_rst] ...) e_body) ≫
--------
[_ ≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body))]])
[≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body))]])
(define-typed-syntax letrec
[(letrec ([b:type-bind e] ...) e_body) ⇐ τ_expected ≫
[(_ ([b:type-bind e] ...) e_body) ⇐ τ_expected ≫
[[b.x ≫ x- : b.type] ...
⊢ [e ≫ e- ⇐ b.type] ... [e_body ≫ e_body- ⇐ τ_expected]]
--------
[⊢ _ ≫ (letrec- ([x- e-] ...) e_body-) ⇐ _]]
[(letrec ([b:type-bind e] ...) e_body) ≫
[⊢ (letrec- ([x- e-] ...) e_body-)]]
[(_ ([b:type-bind e] ...) e_body) ≫
[[b.x ≫ x- : b.type] ...
⊢ [e ≫ e- ⇐ b.type] ... [e_body ≫ e_body- ⇒ τ_body]]
--------
[⊢ _ ≫ (letrec- ([x- e-] ...) e_body-) ⇒ τ_body]])
[⊢ (letrec- ([x- e-] ...) e_body-) ⇒ τ_body]])

28
turnstile/examples/fomega.rkt
View File

@ -83,34 +83,34 @@
(current-typecheck-relation (current-type=?)))
(define-typed-syntax Λ
[(Λ bvs:kind-ctx e) ≫
[([bvs.x ≫ tv- : bvs.kind] ...) () ⊢ [e ≫ e- ⇒ : τ_e]]
[(_ bvs:kind-ctx e) ≫
[([bvs.x ≫ tv- : bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e]
--------
[⊢ [_ ≫ e- ⇒ : (∀ ([tv- : bvs.kind] ...) τ_e)]]])
[⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)]])
(define-typed-syntax inst
[(inst e τ ...) ≫
[⊢ [e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]]
[⊢ [τ ≫ τ- ⇐ : k] ...]
[(_ e τ ...) ≫
[⊢ e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]
[⊢ τ ≫ τ- ⇐ k] ...
#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
--------
[⊢ [_ ≫ e- ⇒ : τ-inst]]])
[⊢ e- ⇒ τ-inst]])
;; TODO: merge with regular λ and app?
;; - see fomega2.rkt
(define-typed-syntax tyλ
[(tyλ bvs:kind-ctx τ_body) ≫
[() ([bvs.x ≫ tv- : bvs.kind] ...) ⊢ [τ_body ≫ τ_body- ⇒ : k_body]]
[(_ bvs:kind-ctx τ_body) ≫
[[bvs.x ≫ tv- : bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
#:fail-unless ((current-kind?) #'k_body)
(format "not a valid type: ~a\n" (type->str #'τ_body))
--------
[⊢ [_ ≫ (λ- (tv- ...) τ_body-) ⇒ : (⇒ bvs.kind ... k_body)]]])
[⊢ (λ- (tv- ...) τ_body-) ⇒ (⇒ bvs.kind ... k_body)]])
(define-typed-syntax tyapp
[(tyapp τ_fn τ_arg ...) ≫
[⊢ [τ_fn ≫ τ_fn- ⇒ : (~⇒ k_in ... k_out)]]
[(_ τ_fn τ_arg ...) ≫
[⊢ τ_fn ≫ τ_fn- ⇒ (~⇒ k_in ... k_out)]
#:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
(num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
[⊢ [τ_arg ≫ τ_arg- ⇐ : k_in] ...]
[⊢ τ_arg ≫ τ_arg- ⇐ k_in] ...
--------
[⊢ [_ ≫ (#%app- τ_fn- τ_arg- ...) ⇒ : k_out]]])
[⊢ (#%app- τ_fn- τ_arg- ...) ⇒ k_out]])

14
turnstile/examples/fomega2.rkt
View File

@ -79,16 +79,16 @@
(current-typecheck-relation (current-type=?)))
(define-typed-syntax Λ
[(Λ bvs:kind-ctx e) ≫
[() ([bvs.x ≫ tv- : bvs.kind] ...) ⊢ [e ≫ e- ⇒ : τ_e]]
[(_ bvs:kind-ctx e) ≫
[[bvs.x ≫ tv- : bvs.kind] ... ⊢ e ≫ e- ⇒ τ_e]
--------
[⊢ [_ ≫ e- ⇒ : (∀ ([tv- : bvs.kind] ...) τ_e)]]])
[⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)]])
(define-typed-syntax inst
[(inst e τ ...) ≫
[⊢ [e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]]
[⊢ [τ ≫ τ- ⇐ : k] ...]
[(_ e τ ...) ≫
[⊢ e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]
[⊢ τ ≫ τ- ⇐ k] ...
#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
--------
[⊢ [_ ≫ e- ⇒ : τ-inst]]])
[⊢ e- ⇒ τ-inst]])

12
turnstile/examples/fsub.rkt
View File

@ -45,10 +45,10 @@
;; Problem: need type annotations, even in expanded form
;; Solution: store type annotations in a (quasi) kind <:
(define-typed-syntax ∀ #:datum-literals (<:)
[(∀ ([tv:id <: τ:type] ...) τ_body) ≫
[(_ ([tv:id <: τ:type] ...) τ_body) ≫
--------
; eval first to overwrite the old #%type
[⊢ _ ≫ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) ⇒ (<: τ.norm ...)]])
[⊢ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) ⇒ (<: τ.norm ...)]])
(begin-for-syntax
(define-syntax ~∀
(pattern-expander
@ -74,19 +74,19 @@
#:msg "Expected ∀ type, got: ~a" #'any))))]))))
(define-typed-syntax Λ #:datum-literals (<:)
[(Λ ([tv:id <: τsub:type] ...) e) ≫
[(_ ([tv:id <: τsub:type] ...) e) ≫
;; NOTE: store the subtyping relation of tv and τsub in the
;; environment with a syntax property using another tag: '<:
;; The "expose" function looks for this tag to enforce the bound,
;; as in TaPL (fig 28-1)
[([tv ≫ tv- : #%type <: τsub] ...) () ⊢ e ≫ e- ⇒ τ_e]
--------
[⊢ _ ≫ e- ⇒ (∀ ([tv- <: τsub] ...) τ_e)]])
[⊢ e- ⇒ (∀ ([tv- <: τsub] ...) τ_e)]])
(define-typed-syntax inst
[(inst e τ:type ...) ≫
[(_ e τ:type ...) ≫
[⊢ e ≫ e- ⇒ (~∀ ([tv <: τ_sub] ...) τ_body)]
[τ.norm τ⊑ τ_sub #:for τ] ...
#:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)
--------
[⊢ _ ≫ e- ⇒ τ_inst]])
[⊢ e- ⇒ τ_inst]])

12
turnstile/examples/stlc+box.rkt
View File

@ -12,21 +12,21 @@
(define-type-constructor Ref)
(define-typed-syntax ref
[(ref e) ≫
[(_ e) ≫
[⊢ e ≫ e- ⇒ τ]
--------
[⊢ _ ≫ (box- e-) ⇒ (Ref τ)]])
[⊢ (box- e-) ⇒ (Ref τ)]])
(define-typed-syntax deref
[(deref e) ≫
[(_ e) ≫
[⊢ e ≫ e- ⇒ (~Ref τ)]
--------
[⊢ _ ≫ (unbox- e-) ⇒ τ]])
[⊢ (unbox- e-) ⇒ τ]])
(define-typed-syntax := #:literals (:=)
[(:= e_ref e) ≫
[(_ e_ref e) ≫
[⊢ e_ref ≫ e_ref- ⇒ (~Ref τ)]
[⊢ e ≫ e- ⇐ τ]
--------
[⊢ _ ≫ (set-box!- e_ref- e-) ⇒ Unit]])
[⊢ (set-box!- e_ref- e-) ⇒ Unit]])

48
turnstile/examples/stlc+cons.rkt
View File

@ -13,13 +13,13 @@
(define-type-constructor List)
(define-typed-syntax nil
[(nil ~! τi:type-ann) ≫
[(_ ~! τi:type-ann) ≫
--------
[⊢ _ ≫ null- ⇒ (List τi.norm)]]
[⊢ null- ⇒ (List τi.norm)]]
; minimal type inference
[nil:id ⇐ (~List τ) ≫
[:id ⇐ (~List τ) ≫
--------
[⊢ _ ≫ null- ⇐ _]])
[⊢ null-]])
(define-typed-syntax cons
[(cons e1 e2) ≫
[⊢ e1 ≫ e1- ⇒ τ1]
@ -27,55 +27,55 @@
--------
[⊢ _ ≫ (cons- e1- e2-) ⇒ (List τ1)]])
(define-typed-syntax isnil
[(isnil e) ≫
[(_ e) ≫
[⊢ e ≫ e- ⇒ (~List _)]
--------
[⊢ _ ≫ (null?- e-) ⇒ Bool]])
[⊢ (null?- e-) ⇒ Bool]])
(define-typed-syntax head
[(head e) ≫
[(_ e) ≫
[⊢ e ≫ e- ⇒ (~List τ)]
--------
[⊢ _ ≫ (car- e-) ⇒ τ]])
[⊢ (car- e-) ⇒ τ]])
(define-typed-syntax tail
[(tail e) ≫
[(_ e) ≫
[⊢ e ≫ e- ⇒ τ-lst]
#:fail-unless (List? #'τ-lst)
(format "Expected a list type, got: ~a" (type->str #'τ-lst))
--------
[⊢ _ ≫ (cdr- e-) ⇒ τ-lst]])
[⊢ (cdr- e-) ⇒ τ-lst]])
(define-typed-syntax list
[(list) ≫
[(_) ≫
--------
[_ ≻ nil]]
[(list x . rst) ⇐ (~List τ) ≫ ; has expected type
[≻ nil]]
[(_ x . rst) ⇐ (~List τ) ≫ ; has expected type
--------
[⊢ _ ≫ (cons (add-expected x τ) (list . rst)) ⇐ _]]
[(list x . rst) ≫ ; no expected type
[⊢ (cons (add-expected x τ) (list . rst))]]
[(_ x . rst) ≫ ; no expected type
--------
[_ ≻ (cons x (list . rst))]])
[≻ (cons x (list . rst))]])
(define-typed-syntax reverse
[(reverse e) ≫
[(_ e) ≫
[⊢ e ≫ e- ⇒ τ-lst]
#:fail-unless (List? #'τ-lst)
(format "Expected a list type, got: ~a" (type->str #'τ-lst))
--------
[⊢ _ ≫ (reverse- e-) ⇒ τ-lst]])
[⊢ (reverse- e-) ⇒ τ-lst]])
(define-typed-syntax length
[(length e) ≫
[(_ e) ≫
[⊢ e ≫ e- ⇒ τ-lst]
#:fail-unless (List? #'τ-lst)
(format "Expected a list type, got: ~a" (type->str #'τ-lst))
--------
[⊢ _ ≫ (length- e-) ⇒ Int]])
[⊢ (length- e-) ⇒ Int]])
(define-typed-syntax list-ref
[(list-ref e n) ≫
[(_ e n) ≫
[⊢ e ≫ e- ⇒ (~List τ)]
[⊢ n ≫ n- ⇐ Int]
--------
[⊢ _ ≫ (list-ref- e- n-) ⇒ τ]])
[⊢ (list-ref- e- n-) ⇒ τ]])
(define-typed-syntax member
[(member v e) ≫
[(_ v e) ≫
[⊢ e ≫ e- ⇒ (~List τ)]
[⊢ v ≫ v- ⇐ τ]
--------
[⊢ _ ≫ (member- v- e-) ⇒ Bool]])
[⊢ (member- v- e-) ⇒ Bool]])

18
turnstile/examples/stlc+effect.rkt
View File

@ -47,14 +47,14 @@
(⇒ ! (~locs ds ...))]
...]
--------
[⊢ _ ≫ (#%app- e_fn- e_arg- ...)
[⊢ (#%app- e_fn- e_arg- ...)
(⇒ : τ_out)
(⇒ ν (locs fns ... tyns ... ns ... ...))
(⇒ := (locs fas ... tyas ... as ... ...))
(⇒ ! (locs fds ... tyds ... ds ... ...))]])
(define-typed-syntax λ
[(λ bvs:type-ctx e) ≫
[(_ bvs:type-ctx e) ≫
[[bvs.x ≫ x- : bvs.type] ... ⊢
e ≫ e-
(⇒ : τ_res)
@ -62,7 +62,7 @@
(⇒ := (~locs as ...))
(⇒ ! (~locs ds ...))]
--------
[⊢ _ ≫ (λ- (x- ...) e-)
[⊢ (λ- (x- ...) e-)
(⇒ : (→ bvs.type ... τ_res)
(⇒ ν (locs ns ...))
(⇒ := (locs as ...))
@ -71,33 +71,33 @@
(define-type-constructor Ref)
(define-typed-syntax ref
[(ref e) ≫
[(_ e) ≫
[⊢ e ≫ e-
(⇒ : τ)
(⇒ ν (~locs ns ...))
(⇒ := (~locs as ...))
(⇒ ! (~locs ds ...))]
--------
[⊢ _ ≫ (box- e-)
[⊢ (box- e-)
(⇒ : (Ref τ))
(⇒ ν (locs #,(syntax-position stx) ns ...))
(⇒ := (locs as ...))
(⇒ ! (locs ds ...))]])
(define-typed-syntax deref
[(deref e) ≫
[(_ e) ≫
[⊢ e ≫ e-
(⇒ : (~Ref ty))
(⇒ ν (~locs ns ...))
(⇒ := (~locs as ...))
(⇒ ! (~locs ds ...))]
--------
[⊢ _ ≫ (unbox- e-)
[⊢ (unbox- e-)
(⇒ : ty)
(⇒ ν (locs ns ...))
(⇒ := (locs as ...))
(⇒ ! (locs #,(syntax-position stx) ds ...))]])
(define-typed-syntax := #:literals (:=)
[(:= e_ref e) ≫
[(_ e_ref e) ≫
[⊢ e_ref ≫ e_ref-
(⇒ : (~Ref ty))
(⇒ ν (~locs ns1 ...))
@ -109,7 +109,7 @@
(⇒ := (~locs as2 ...))
(⇒ ! (~locs ds2 ...))]
--------
[⊢ _ ≫ (set-box!- e_ref- e-)
[⊢ (set-box!- e_ref- e-)
(⇒ : Unit)
(⇒ ν (locs ns1 ... ns2 ...))
(⇒ := (locs #,(syntax-position stx) as1 ... as2 ...))

4
turnstile/examples/stlc+lit.rkt
View File

@ -33,9 +33,9 @@
(define-primop + : (→ Int Int Int))
(define-typed-syntax #%datum
[(#%datum . n:integer) ≫
[(_ . n:integer) ≫
--------
[⊢ _ ≫ (#%datum- . n) ⇒ Int]]
[⊢ (#%datum- . n) ⇒ Int]]
[(_ . x) ≫
--------
[_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])

8
turnstile/examples/stlc+rec-iso.rkt
View File

@ -37,15 +37,15 @@
(current-typecheck-relation type=?))
(define-typed-syntax unfld
[(unfld τ:type-ann e) ≫
[(_ τ:type-ann e) ≫
#:with (~μ* (tv) τ_body) #'τ.norm
[⊢ e ≫ e- ⇐ τ.norm]
--------
[⊢ _ ≫ e- ⇒ #,(subst #'τ.norm #'tv #'τ_body)]])
[⊢ e- ⇒ #,(subst #'τ.norm #'tv #'τ_body)]])
(define-typed-syntax fld
[(fld τ:type-ann e) ≫
[(_ τ:type-ann e) ≫
#:with (~μ* (tv) τ_body) #'τ.norm
#:with τ_e (subst #'τ.norm #'tv #'τ_body)
[⊢ e ≫ e- ⇐ τ_e]
--------
[⊢ _ ≫ e- ⇒ τ.norm]])
[⊢ e- ⇒ τ.norm]])

8
turnstile/examples/stlc+reco+sub.rkt
View File

@ -14,12 +14,12 @@
;; - records and variants from stlc+reco+var
(define-typed-syntax #%datum
[(#%datum . n:number) ≫
[(_ . n:number) ≫
--------
[_ ≻ (stlc+sub:#%datum . n)]]
[(#%datum . x) ≫
[≻ (stlc+sub:#%datum . n)]]
[(_ . x) ≫
--------
[_ ≻ (stlc+reco+var:#%datum . x)]])
[≻ (stlc+reco+var:#%datum . x)]])
(begin-for-syntax
(define old-sub? (current-sub?))

46
turnstile/examples/stlc+reco+var.rkt
View File

@ -29,21 +29,21 @@
[(_ x ...) #'ty]))]))
(define-typed-syntax define
[(define x:id : τ:type e:expr) ≫
[(_ x:id : τ:type e:expr) ≫
;This wouldn't work with mutually recursive definitions
;[⊢ [e ≫ e- ⇐ τ.norm]]
;So expand to an ann form instead.
--------
[_ ≻ (begin-
(define-syntax x (make-rename-transformer (⊢ y : τ.norm)))
(define- y (ann e : τ.norm)))]]
[(define x:id e) ≫
[≻ (begin-
(define-syntax x (make-rename-transformer (⊢ y : τ.norm)))
(define- y (ann e : τ.norm)))]]
[(_ x:id e) ≫
[⊢ e ≫ e- ⇒ τ]
#:with y (generate-temporary #'x)
--------
[_ ≻ (begin-
(define-syntax x (make-rename-transformer (⊢ y : τ)))
(define- y e-))]])
[≻ (begin-
(define-syntax x (make-rename-transformer (⊢ y : τ)))
(define- y e-))]])
; re-define tuples as records
@ -88,19 +88,19 @@
;; records
(define-typed-syntax tup #:datum-literals (=)
[(tup [l:id = e] ...) ≫
[⊢ [e ≫ e- ⇒ τ] ...]
[(_ [l:id = e] ...) ≫
[⊢ e ≫ e- ⇒ τ] ...
--------
[⊢ _ ≫ (list- (list- 'l e-) ...) ⇒ (× [l : τ] ...)]])
[⊢ (list- (list- 'l e-) ...) ⇒ (× [l : τ] ...)]])
(define-typed-syntax proj #:literals (quote)
[(proj e_rec l:id) ≫
[(_ e_rec l:id) ≫
[⊢ e_rec ≫ e_rec- ⇒ τ_e]
#:fail-unless (×? #'τ_e)
(format "Expected expression ~s to have × type, got: ~a"
(syntax->datum #'e_rec) (type->str #'τ_e))
#:with τ_l (×-ref #'τ_e #'l)
--------
[⊢ _ ≫ (cadr- (assoc- 'l e_rec-)) ⇒ τ_l]])
[⊢ (cadr- (assoc- 'l e_rec-)) ⇒ τ_l]])
(define-type-constructor ∨/internal #:arity >= 0)
@ -146,10 +146,10 @@
(add-orig res (get-orig res))])))
(define-typed-syntax var #:datum-literals (as =)
[(var l:id = e as τ:type) ≫
[(_ l:id = e as τ:type) ≫
--------
[_ ≻ (ann (var l = e) : τ.norm)]]
[(var l:id = e) ⇐ τ ≫
[≻ (ann (var l = e) : τ.norm)]]
[(_ l:id = e) ⇐ τ ≫
#:fail-unless (∨? #'τ)
(format "Expected the expected type to be a ∨ type, got: ~a" (type->str #'τ))
#:with τ_e
@ -159,18 +159,16 @@
stx)))
[⊢ e ≫ e- ⇐ τ_e]
--------
[⊢ _ ≫ (list- 'l e) ⇐ _]])
[⊢ (list- 'l e)]])
(define-typed-syntax case
#:datum-literals (of =>)
[(case e [l:id x:id => e_l] ...) ≫
(define-typed-syntax case #:datum-literals (of =>)
[(_ e [l:id x:id => e_l] ...) ≫
#:fail-unless (not (null? (syntax->list #'(l ...)))) "no clauses"
[⊢ e ≫ e- ⇒ (~∨* [l_x : τ_x] ...)]
#:fail-unless (stx-length=? #'(l ...) #'(l_x ...)) "wrong number of case clauses"
#:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
[[x ≫ x- : τ_x] ⊢ e_l ≫ e_l- ⇒ τ_el] ...
--------
[⊢ _ ≫
(let- ([l_e (car- e-)])
(cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...))
⇒ (⊔ τ_el ...)]])
[⊢ (let- ([l_e (car- e-)])
(cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...))
⇒ (⊔ τ_el ...)]])

16
turnstile/examples/stlc+sub.rkt
View File

@ -28,18 +28,18 @@
(define-primop * : (→ Num Num Num))
(define-typed-syntax #%datum
[(#%datum . n:nat) ≫
[(_ . n:nat) ≫
--------
[⊢ _ ≫ (#%datum- . n) ⇒ Nat]]
[(#%datum . n:integer) ≫
[⊢ (#%datum- . n) ⇒ Nat]]
[(_ . n:integer) ≫
--------
[⊢ _ ≫ (#%datum- . n) ⇒ Int]]
[(#%datum . n:number) ≫
[⊢ (#%datum- . n) ⇒ Int]]
[(_ . n:number) ≫
--------
[⊢ _ ≫ (#%datum- . n) ⇒ Num]]
[(#%datum . x) ≫
[⊢ (#%datum- . n) ⇒ Num]]
[(_ . x) ≫
--------
[_ ≻ (ext:#%datum . x)]])
[≻ (ext:#%datum . x)]])
(begin-for-syntax
(define (sub? t1 t2)

16
turnstile/examples/stlc+tup.rkt
View File

@ -16,20 +16,20 @@
(make-list (stx-length (stx-cdr stx)) covariant)))
(define-typed-syntax tup
[(tup e ...) ⇐ (~× τ ...) ≫
[(_ e ...) ⇐ (~× τ ...) ≫
#:when (stx-length=? #'[e ...] #'[τ ...])
[⊢ [e ≫ e- ⇐ τ] ...]
[⊢ e ≫ e- ⇐ τ] ...
--------
[⊢ _ ≫ (list- e- ...) ⇐ _]]
[(tup e ...) ≫
[⊢ [e ≫ e- ⇒ τ] ...]
[⊢ (list- e- ...)]]
[(_ e ...) ≫
[⊢ e ≫ e- ⇒ τ] ...
--------
[⊢ _ ≫ (list- e- ...) ⇒ (× τ ...)]])
[⊢ (list- e- ...) ⇒ (× τ ...)]])
(define-typed-syntax proj
[(proj e_tup n:nat) ≫
[(_ e_tup n:nat) ≫
[⊢ e_tup ≫ e_tup- ⇒ (~× τ ...)]
#:fail-unless (< (syntax-e #'n) (stx-length #'[τ ...])) "index too large"
--------
[⊢ _ ≫ (list-ref- e_tup- n) ⇒ #,(stx-list-ref #'[τ ...] (syntax-e #'n))]])
[⊢ (list-ref- e_tup- n) ⇒ #,(stx-list-ref #'[τ ...] (syntax-e #'n))]])

16
turnstile/examples/stlc.rkt
View File

@ -11,26 +11,26 @@
(list covariant))])))
(define-typed-syntax λ #:datum-literals (:)
[(λ ([x:id : τ_in:type] ...) e) ≫
[(_ ([x:id : τ_in:type] ...) e) ≫
[[x ≫ x- : τ_in.norm] ... ⊢ e ≫ e- ⇒ τ_out]
-------
[⊢ _ ≫ (λ- (x- ...) e-) ⇒ (→ τ_in.norm ... τ_out)]]
[(λ (x:id ...) e) ⇐ (~→ τ_in ... τ_out) ≫
[⊢ (λ- (x- ...) e-) ⇒ (→ τ_in.norm ... τ_out)]]
[(_ (x:id ...) e) ⇐ (~→ τ_in ... τ_out) ≫
[[x ≫ x- : τ_in] ... ⊢ e ≫ e- ⇐ τ_out]
---------
[⊢ _ ≫ (λ- (x- ...) e-) ⇐ _]])
[⊢ (λ- (x- ...) e-)]])
(define-typed-syntax #%app
[(_ e_fn e_arg ...) ≫
[⊢ e_fn ≫ e_fn- ⇒ (~→ τ_in ... τ_out)]
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
(num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
[⊢ [e_arg ≫ e_arg- ⇐ τ_in] ...]
[⊢ e_arg ≫ e_arg- ⇐ τ_in] ...
--------
[⊢ _ ≫ (#%app- e_fn- e_arg- ...) ⇒ τ_out]])
[⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out]])
(define-typed-syntax ann #:datum-literals (:)
[(ann e : τ:type) ≫
[(_ e : τ:type) ≫
[⊢ e ≫ e- ⇐ τ.norm]
--------
[⊢ _ ≫ e- ⇒ τ.norm]])
[⊢ e- ⇒ τ.norm]])

12
turnstile/examples/sysf.rkt
View File

@ -15,18 +15,18 @@
(define-type-constructor ∀ #:bvs >= 0)
(define-typed-syntax Λ
[(Λ (tv:id ...) e) ≫
[(_ (tv:id ...) e) ≫
[([tv ≫ tv- : #%type] ...) () ⊢ e ≫ e- ⇒ τ]
--------
[⊢ _ ≫ e- ⇒ (∀ (tv- ...) τ)]])
[⊢ e- ⇒ (∀ (tv- ...) τ)]])
(define-typed-syntax inst
[(inst e τ:type ...) ≫
[(_ e τ:type ...) ≫
[⊢ e ≫ e- ⇒ (~∀ tvs τ_body)]
#:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body)
--------
[⊢ _ ≫ e- ⇒ τ_inst]]
[(inst e) ≫
[⊢ e- ⇒ τ_inst]]
[(_ e) ≫
--------
[_ ≻ e]])
[≻ e]])

9
turnstile/turnstile.rkt
View File

@ -143,7 +143,7 @@
[pattern (~seq p:⇒-prop/conclusion)
#:with [tag ...] #'[p.tag]
#:with [tag-expr ...] #'[p.tag-expr]]
[pattern (~seq (:⇒-prop/conclusion) ...)])
[pattern (~seq (:⇒-prop/conclusion) ...+)])
(define-splicing-syntax-class id+props+≫
#:datum-literals (≫)
#:attributes ([x- 1] [ctx 1])
@ -274,6 +274,7 @@
(define-syntax-class last-clause
#:datum-literals (⊢ ≫ ≻ ⇒ ⇐ :)
#:attributes ([pat 0] [stuff 1] [body 0])
;; ⇒ conclusion
[pattern (~or [⊢ pat ≫ e-stx props:⇒-props/conclusion]
[⊢ [pat ≫ e-stx props:⇒-props/conclusion]])
#:with [stuff ...] #'[]
@ -283,6 +284,11 @@
[v (in-list (syntax->list #'[props.tag-expr ...]))])
(with-syntax ([body body] [k k] [v v])
#'(assign-type body #:tag 'k v)))]
;; ⇒ conclusion, implicit pat
[pattern (~or [⊢ e-stx props:⇒-props/conclusion]
[⊢ [e-stx props:⇒-props/conclusion]])
#:with :last-clause #'[⊢ [_ ≫ e-stx . props]]]
;; ⇐ conclusion
[pattern (~or [⊢ [e-stx]] [⊢ (~and e-stx (~not [_ ≫ . rst]))])
#:with :last-clause #'[⊢ [_ ≫ e-stx ⇐ : _]]]
[pattern (~or [⊢ pat* ≫ e-stx ⇐ τ-pat]
@ -301,6 +307,7 @@
#:with [stuff ...] #'[]
#:with body:expr
#'(assign-type (quasisyntax/loc this-syntax e-stx) #`τ)]
;; macro invocations
[pattern [≻ e-stx]
#:with :last-clause #'[_ ≻ e-stx]]
[pattern [pat ≻ e-stx]