stlc+union+case.rkt (3861B)
1 #lang turnstile/lang 2 (extends "stlc+union.rkt" #:except #%app add1 sub1) 3 4 ;; Simply-Typed Lambda Calculus, plus union types and case-> function types 5 ;; Types: 6 ;; - types from and stlc+union.rkt 7 ;; - case-> 8 ;; Type relations: 9 ;; - sub? 10 ;; Terms: 11 ;; - terms from stlc+union.rkt 12 ;; Other: updated current-sub? 13 14 (provide (type-out case->) case→ 15 (typed-out [add1 : (case→ (→ Nat Nat) 16 (→ Int Int))] 17 [sub1 : (case→ (→ Zero NegInt) 18 (→ PosInt Nat) 19 (→ NegInt NegInt) 20 (→ Nat Nat) 21 (→ Int Int))]) 22 #%app) 23 24 (define-type-constructor case-> #:arity > 0) 25 (define-syntax case→ (make-rename-transformer #'case->)) 26 27 (define-typed-syntax #%app 28 [(_ e_fn e_arg ...) ≫ 29 [⊢ [e_fn ≫ e_fn- ⇒ : (~→ ~! τ_in ... τ_out)]] 30 #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) 31 (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) 32 [⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...] 33 -------- 34 [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]] 35 [(_ e_fn e_arg ...) ≫ 36 [⊢ [e_fn ≫ e_fn- ⇒ : (~case-> ~! . (~and ty_fns ((~→ . _) ...)))]] 37 [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...] 38 #:with τ_out 39 (for/first ([ty_f (stx->list #'ty_fns)] 40 #:when (syntax-parse ty_f 41 [(~→ τ_in ... τ_out) 42 (and (stx-length=? #'(τ_in ...) #'(e_arg ...)) 43 (typechecks? #'(τ_arg ...) #'(τ_in ...)))])) 44 (syntax-parse ty_f [(~→ _ ... t_out) #'t_out])) 45 #:fail-unless (syntax-e #'τ_out) 46 ; use (failing) typechecks? to get err msg 47 (syntax-parse #'ty_fns 48 [((~→ τ_in ... _) ...) 49 (let* ([τs_expecteds #'((τ_in ...) ...)] 50 [τs_given #'(τ_arg ...)] 51 [expressions #'(e_arg ...)]) 52 (format (string-append "type mismatch\n" 53 " expected one of:\n" 54 " ~a\n" 55 " given: ~a\n" 56 " expressions: ~a") 57 (string-join 58 (stx-map 59 (lambda (τs_expected) 60 (string-join (stx-map type->str τs_expected) ", ")) 61 τs_expecteds) 62 "\n ") 63 (string-join (stx-map type->str τs_given) ", ") 64 (string-join (map ~s (stx-map syntax->datum expressions)) ", ")))]) 65 -------- 66 [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]]) 67 68 (begin-for-syntax 69 (define (sub? t1 t2) 70 ; need this because recursive calls made with unexpanded types 71 ;; (define τ1 ((current-type-eval) t1)) 72 ;; (define τ2 ((current-type-eval) t2)) 73 ;; (printf "t1 = ~a\n" (syntax->datum t1)) 74 ;; (printf "t2 = ~a\n" (syntax->datum t2)) 75 (or 76 ((current-type=?) t1 t2) 77 (syntax-parse (list t1 t2) 78 ; 2 U types, subtype = subset 79 [((~U* . tys1) _) 80 (for/and ([t (stx->list #'tys1)]) 81 ((current-sub?) t t2))] 82 ; 1 U type, 1 non-U type. subtype = member 83 [(ty (~U* . tys)) 84 (for/or ([t (stx->list #'tys)]) 85 ((current-sub?) #'ty t))] 86 ; 2 case-> types, subtype = subset 87 [(_ (~case-> . tys2)) 88 (for/and ([t (stx->list #'tys2)]) 89 ((current-sub?) t1 t))] 90 ; 1 case-> , 1 non-case-> 91 [((~case-> . tys) ty) 92 (for/or ([t (stx->list #'tys)]) 93 ((current-sub?) t #'ty))] 94 [((~→ s1 ... s2) (~→ t1 ... t2)) 95 (and (subs? #'(t1 ...) #'(s1 ...)) 96 ((current-sub?) #'s2 #'t2))] 97 [_ #f]))) 98 (current-sub? sub?) 99 (current-typecheck-relation sub?) 100 (define (subs? τs1 τs2) 101 (and (stx-length=? τs1 τs2) 102 (stx-andmap (current-sub?) τs1 τs2)))) 103