stlc+sub.rkt (3635B)
1 #lang turnstile/lang 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) ≫ 32 -------- 33 [⊢ (#%datum- . n) ⇒ Nat]] 34 [(_ . n:integer) ≫ 35 -------- 36 [⊢ (#%datum- . n) ⇒ Int]] 37 [(_ . n:number) ≫ 38 -------- 39 [⊢ (#%datum- . n) ⇒ Num]] 40 [(_ . x) ≫ 41 -------- 42 [≻ (ext:#%datum . x)]]) 43 44 (begin-for-syntax 45 (define (sub? t1 t2) 46 ; need this because recursive calls made with unexpanded types 47 (define τ1 ((current-type-eval) t1)) 48 (define τ2 ((current-type-eval) t2)) 49 ; (printf "t1 = ~a\n" (syntax->datum τ1)) 50 ; (printf "t2 = ~a\n" (syntax->datum τ2)) 51 (or ((current-type=?) τ1 τ2) 52 (Top? τ2))) 53 (define current-sub? (make-parameter sub?)) 54 (current-typecheck-relation sub?) 55 56 (define (subs? τs1 τs2) 57 (and (stx-length=? τs1 τs2) 58 (stx-andmap (current-sub?) τs1 τs2))) 59 60 (define-syntax (define-sub-relation stx) 61 (syntax-parse stx #:datum-literals (<: =>) 62 [(_ τ1:id <: τ2:id) 63 #:with τ1-expander (format-id #'τ1 "~~~a" #'τ1) 64 #:with τ2-expander (format-id #'τ2 "~~~a" #'τ2) 65 #:with fn (generate-temporary) 66 #:with old-sub? (generate-temporary) 67 #'(begin 68 (define old-sub? (current-sub?)) 69 (define (fn t1 t2) 70 (define τ1 ((current-type-eval) t1)) 71 (define τ2 ((current-type-eval) t2)) 72 (syntax-parse (list τ1 τ2) 73 [(τ1-expander τ) ((current-sub?) #'τ2 #'τ)] 74 [(τ τ2-expander) ((current-sub?) #'τ #'τ1)] 75 [_ #f])) 76 (current-sub? (λ (t1 t2) (or (old-sub? t1 t2) (fn t1 t2)))) 77 (current-typecheck-relation (current-sub?)))] 78 [(_ (~seq τ1:id <: τ2:id (~and (~literal ...) ddd)) 79 (~seq τ3:id <: τ4:id) 80 => 81 (tycon1 . rst1) <: (tycon2 . rst2)) 82 #:with tycon1-expander (format-id #'tycon1 "~~~a" #'tycon1) 83 #:with tycon2-expander (format-id #'tycon2 "~~~a" #'tycon2) 84 #:with fn (generate-temporary) 85 #:with old-sub? (generate-temporary) 86 #'(begin 87 (define old-sub? (current-sub?)) 88 (define (fn t1 t2) 89 (define τ1 ((current-type-eval) t1)) 90 (define τ2 ((current-type-eval) t2)) 91 (syntax-parse (list τ1 τ2) 92 [((tycon1-expander . rst1) (tycon2-expander . rst2)) 93 (and (subs? #'(τ1 ddd) #'(τ2 ddd)) 94 ((current-sub?) #'τ3 #'τ4))] 95 [_ #f])) 96 (current-sub? (λ (t1 t2) (or (old-sub? t1 t2) (fn t1 t2)))) 97 (current-typecheck-relation (current-sub?)))])) 98 99 (define-sub-relation Nat <: Int) 100 (define-sub-relation Int <: Num) 101 (define-sub-relation t1 <: s1 ... s2 <: t2 => (→ s1 ... s2) <: (→ t1 ... t2)) 102 103 (define (join t1 t2) 104 (cond 105 [((current-sub?) t1 t2) t2] 106 [((current-sub?) t2 t1) t1] 107 [else #'Top])) 108 (current-join join))