stlc+reco+sub.rkt (1694B)
1 #lang turnstile/lang 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) ≫ 18 -------- 19 [≻ (stlc+sub:#%datum . n)]] 20 [(_ . x) ≫ 21 -------- 22 [≻ (stlc+reco+var:#%datum . x)]]) 23 24 (begin-for-syntax 25 (define old-sub? (current-sub?)) 26 (define (sub? τ1 τ2) 27 ; (printf "t1 = ~a\n" (syntax->datum τ1)) 28 ; (printf "t2 = ~a\n" (syntax->datum τ2)) 29 (or 30 (old-sub? τ1 τ2) 31 (syntax-parse (list τ1 τ2) 32 [((~× [k : τk] ...) (~× [l : τl] ...)) 33 #:when (subset? (stx-map syntax-e (syntax->list #'(l ...))) 34 (stx-map syntax-e (syntax->list #'(k ...)))) 35 (stx-andmap 36 (syntax-parser 37 [(label τlabel) 38 #:with (k_match τk_match) (stx-assoc #'label #'([k τk] ...)) 39 ((current-sub?) #'τk_match #'τlabel)]) 40 #'([l τl] ...))] 41 [((~∨ [k : τk] ...) (~∨ [l : τl] ...)) 42 #:when (subset? (stx-map syntax-e (syntax->list #'(l ...))) 43 (stx-map syntax-e (syntax->list #'(k ...)))) 44 (stx-andmap 45 (syntax-parser 46 [(label τlabel) 47 #:with (k_match τk_match) (stx-assoc #'label #'([k τk] ...)) 48 ((current-sub?) #'τk_match #'τlabel)]) 49 #'([l τl] ...))] 50 [_ #f]))) 51 (current-sub? sub?) 52 (current-typecheck-relation sub?))