stlc+tup.rkt (896B)
1 #lang turnstile/lang 2 (extends "ext-stlc.rkt") 3 4 ;; Simply-Typed Lambda Calculus, plus tuples 5 ;; Types: 6 ;; - types from ext-stlc.rkt 7 ;; - × 8 ;; Terms: 9 ;; - terms from ext-stlc.rkt 10 ;; - tup and proj 11 12 (provide (type-out ×) tup proj) 13 14 (define-type-constructor × #:arity >= 0 15 #:arg-variances (λ (stx) 16 (make-list (stx-length (stx-cdr stx)) covariant))) 17 18 (define-typed-syntax tup 19 [(_ e ...) ⇐ (~× τ ...) ≫ 20 #:when (stx-length=? #'[e ...] #'[τ ...]) 21 [⊢ e ≫ e- ⇐ τ] ... 22 -------- 23 [⊢ (list- e- ...)]] 24 [(_ e ...) ≫ 25 [⊢ e ≫ e- ⇒ τ] ... 26 -------- 27 [⊢ (list- e- ...) ⇒ (× τ ...)]]) 28 29 (define-typed-syntax (proj e_tup n:nat) ≫ 30 [⊢ e_tup ≫ e_tup- ⇒ (~× τ ...)] 31 #:fail-unless (< (syntax-e #'n) (stx-length #'[τ ...])) "index too large" 32 -------- 33 [⊢ (list-ref- e_tup- n) ⇒ #,(stx-list-ref #'[τ ...] (syntax-e #'n))]) 34