stlc+reco+sub.rkt (1670B)
1 #lang s-exp macrotypes/typecheck 2 (extends "stlc+sub.rkt" #:except #%datum) 3 (extends "stlc+reco+var.rkt" #:except #%datum + *) 4 5 ;; Simply-Typed Lambda Calculus, plus subtyping, plus records 6 ;; Types: 7 ;; - types from stlc+sub.rkt 8 ;; Type relations: 9 ;; - sub? (from stlc+sub.rkt) extended to records 10 ;; Terms: 11 ;; - terms from stlc+sub.rkt 12 ;; - records and variants from stlc+reco+var 13 14 (provide #%datum) 15 16 (define-typed-syntax #%datum 17 [(_ . n:number) #'(stlc+sub:#%datum . n)] 18 [(_ . x) #'(stlc+reco+var:#%datum . x)]) 19 20 (begin-for-syntax 21 (define old-sub? (current-sub?)) 22 (define (sub? τ1 τ2) 23 ; (printf "t1 = ~a\n" (syntax->datum τ1)) 24 ; (printf "t2 = ~a\n" (syntax->datum τ2)) 25 (or 26 (old-sub? τ1 τ2) 27 (syntax-parse (list τ1 τ2) 28 [((~× [k : τk] ...) (~× [l : τl] ...)) 29 #:when (subset? (stx-map syntax-e (syntax->list #'(l ...))) 30 (stx-map syntax-e (syntax->list #'(k ...)))) 31 (stx-andmap 32 (syntax-parser 33 [(label τlabel) 34 #:with (k_match τk_match) (stx-assoc #'label #'([k τk] ...)) 35 ((current-sub?) #'τk_match #'τlabel)]) 36 #'([l τl] ...))] 37 [((~∨ [k : τk] ...) (~∨ [l : τl] ...)) 38 #:when (subset? (stx-map syntax-e (syntax->list #'(l ...))) 39 (stx-map syntax-e (syntax->list #'(k ...)))) 40 (stx-andmap 41 (syntax-parser 42 [(label τlabel) 43 #:with (k_match τk_match) (stx-assoc #'label #'([k τk] ...)) 44 ((current-sub?) #'τk_match #'τlabel)]) 45 #'([l τl] ...))] 46 [_ #f]))) 47 (current-sub? sub?) 48 (current-typecheck-relation (current-sub?)))