stlc+tup.rkt (1079B)
1 #lang s-exp macrotypes/typecheck 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 #:with ty-expected (get-expected-type stx) 21 #:with (e_ann ...) 22 (if (syntax-e #'ty-expected) 23 (syntax-parse (local-expand #'ty-expected 'expression null) 24 [(~× ty_exp ...) #'((add-expected e ty_exp) ...)] 25 [_ #'(e ...)]) 26 #'(e ...)) 27 #:with ([e- τ] ...) (infers+erase #'(e_ann ...)) 28 (⊢ (list- e- ...) : (× τ ...))]) 29 (define-typed-syntax proj 30 [(_ e_tup n:nat) 31 #:with [e_tup- (~× . τs_tup)] (infer+erase #'e_tup) 32 #:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "index too large" 33 (⊢ (list-ref- e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))]) 34