stlc+sub.rkt (3524B)
1 #lang s-exp macrotypes/typecheck 2 (extends "stlc+lit.rkt" #:except #%datum +) 3 (reuse Bool String add1 #:from "ext-stlc.rkt") 4 (require (prefix-in ext: (only-in "ext-stlc.rkt" #%datum)) 5 (only-in "ext-stlc.rkt" current-join)) 6 7 ;; Simply-Typed Lambda Calculus, plus subtyping 8 ;; Types: 9 ;; - types from and stlc+lit.rkt 10 ;; - Top, Num, Nat 11 ;; Type relations: 12 ;; - sub? 13 ;; - Any <: Top 14 ;; - Nat <: Int 15 ;; - Int <: Num 16 ;; - → 17 ;; Terms: 18 ;; - terms from stlc+lit.rkt, except redefined: datum and + 19 ;; - also * 20 ;; Other: sub? current-sub? 21 22 (provide (for-syntax subs? current-sub?) 23 (type-out Top Num Nat) 24 (typed-out [+ : (→ Num Num Num)] 25 [* : (→ Num Num Num)]) 26 #%datum) 27 28 (define-base-types Top Num Nat) 29 30 (define-typed-syntax #%datum 31 [(_ . n:nat) (⊢ (#%datum- . n) : Nat)] 32 [(_ . n:integer) (⊢ (#%datum- . n) : Int)] 33 [(_ . n:number) (⊢ (#%datum- . n) : Num)] 34 [(_ . x) #'(ext:#%datum . x)]) 35 36 (begin-for-syntax 37 (define (sub? t1 t2) 38 ; need this because recursive calls made with unexpanded types 39 (define τ1 ((current-type-eval) t1)) 40 (define τ2 ((current-type-eval) t2)) 41 ; (printf "t1 = ~a\n" (syntax->datum τ1)) 42 ; (printf "t2 = ~a\n" (syntax->datum τ2)) 43 (or ((current-type=?) τ1 τ2) 44 (Top? τ2))) 45 (define current-sub? (make-parameter sub?)) 46 (current-typecheck-relation sub?) 47 (define (subs? τs1 τs2) 48 (and (stx-length=? τs1 τs2) 49 (stx-andmap (current-sub?) τs1 τs2))) 50 51 (define-syntax (define-sub-relation stx) 52 (syntax-parse stx #:datum-literals (<: =>) 53 [(_ τ1:id <: τ2:id) 54 #:with τ1-expander (mk-~ #'τ1) 55 #:with τ2-expander (mk-~ #'τ2) 56 #:with fn (generate-temporary) 57 #:with old-sub? (generate-temporary) 58 #'(begin 59 (define old-sub? (current-sub?)) 60 (define (fn t1 t2) 61 (define τ1 ((current-type-eval) t1)) 62 (define τ2 ((current-type-eval) t2)) 63 (syntax-parse (list τ1 τ2) 64 [(τ1-expander τ) ((current-sub?) #'τ2 #'τ)] 65 [(τ τ2-expander) ((current-sub?) #'τ #'τ1)] 66 [_ #f])) 67 (current-sub? (λ (t1 t2) (or (old-sub? t1 t2) (fn t1 t2)))) 68 (current-typecheck-relation (current-sub?)))] 69 [(_ (~seq τ1:id <: τ2:id (~and (~literal ...) ddd)) 70 (~seq τ3:id <: τ4:id) 71 => 72 (tycon1 . rst1) <: (tycon2 . rst2)) 73 #:with tycon1-expander (format-id #'tycon1 "~~~a" #'tycon1) 74 #:with tycon2-expander (format-id #'tycon2 "~~~a" #'tycon2) 75 #:with fn (generate-temporary) 76 #:with old-sub? (generate-temporary) 77 #'(begin 78 (define old-sub? (current-sub?)) 79 (define (fn t1 t2) 80 (define τ1 ((current-type-eval) t1)) 81 (define τ2 ((current-type-eval) t2)) 82 (syntax-parse (list τ1 τ2) 83 [((tycon1-expander . rst1) (tycon2-expander . rst2)) 84 (and (subs? #'(τ1 ddd) #'(τ2 ddd)) 85 ((current-sub?) #'τ3 #'τ4))] 86 [_ #f])) 87 (current-sub? (λ (t1 t2) (or (old-sub? t1 t2) (fn t1 t2)))) 88 (current-typecheck-relation (current-sub?)))])) 89 90 (define-sub-relation Nat <: Int) 91 (define-sub-relation Int <: Num) 92 (define-sub-relation t1 <: s1 ... s2 <: t2 => (→ s1 ... s2) <: (→ t1 ... t2)) 93 94 (define (join t1 t2) 95 (cond 96 [((current-sub?) t1 t2) t2] 97 [((current-sub?) t2 t1) t1] 98 [else #'Top])) 99 (current-join join))