implement sub and reco+sub with typed-lang-builder

tapl/tests/stlc+reco+sub-tests.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../stlc+reco+sub.rkt"
+#lang s-exp "../typed-lang-builder/stlc+reco+sub.rkt"
 (require "rackunit-typechecking.rkt")
 
 ;; record subtyping tests

tapl/tests/stlc+sub-tests.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../stlc+sub.rkt"
+#lang s-exp "../typed-lang-builder/stlc+sub.rkt"
 (require "rackunit-typechecking.rkt")
 
 ;; subtyping tests

tapl/typed-lang-builder/stlc+reco+sub.rkt

@@ -0,0 +1,52 @@
+#lang macrotypes/tapl/typed-lang-builder
+(extends "stlc+sub.rkt" #:except #%app #%datum)
+(extends "stlc+reco+var.rkt" #:except #%datum +)
+;;use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt
+;; but extend sub? from stlc+sub.rkt
+
+;; Simply-Typed Lambda Calculus, plus subtyping, plus records
+;; Types:
+;; - types from stlc+sub.rkt
+;; Type relations:
+;; - sub? extended to records
+;; Terms:
+;; - terms from stlc+sub.rkt
+;; - records and variants from stlc+reco+var
+
+(define-typed-syntax #%datum
+  [(#%datum . n:number) ▶
+   --------
+   [_ ≻ (stlc+sub:#%datum . n)]]
+  [(#%datum . x) ▶
+   --------
+   [_ ≻ (stlc+reco+var:#%datum . x)]])
+
+(begin-for-syntax
+  (define old-sub? (current-sub?))
+  (define (sub? τ1 τ2)
+;    (printf "t1 = ~a\n" (syntax->datum τ1))
+;    (printf "t2 = ~a\n" (syntax->datum τ2))
+    (or
+     (old-sub? τ1 τ2)
+     (syntax-parse (list τ1 τ2)
+       [((~× [k : τk] ...) (~× [l : τl] ...))
+        #:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
+                        (stx-map syntax-e (syntax->list #'(k ...))))
+        (stx-andmap
+         (syntax-parser
+           [(label τlabel)
+            #:with (k_match τk_match) (stx-assoc #'label #'([k τk] ...))
+            ((current-sub?) #'τk_match #'τlabel)])
+         #'([l τl] ...))]
+       [((~∨ [k : τk] ...) (~∨ [l : τl] ...))
+        #:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
+                        (stx-map syntax-e (syntax->list #'(k ...))))
+        (stx-andmap
+         (syntax-parser
+           [(label τlabel)
+            #:with (k_match τk_match) (stx-assoc #'label #'([k τk] ...))
+            ((current-sub?) #'τk_match #'τlabel)])
+         #'([l τl] ...))]
+       [_ #f])))
+  (current-sub? sub?)
+  (current-typecheck-relation (current-sub?)))

tapl/typed-lang-builder/stlc+sub.rkt

@@ -0,0 +1,107 @@
+#lang macrotypes/tapl/typed-lang-builder
+(extends "stlc+lit.rkt" #:except #%datum +)
+(reuse Bool String add1 #:from "ext-stlc.rkt")
+(require (prefix-in ext: (only-in "ext-stlc.rkt" #%datum))
+         (only-in "ext-stlc.rkt" current-join))
+(provide (for-syntax subs? current-sub?))
+
+;; Simply-Typed Lambda Calculus, plus subtyping
+;; Types:
+;; - types from and stlc+lit.rkt
+;; - Top, Num, Nat
+;; Type relations:
+;; - sub?
+;;   - Any <: Top
+;;   - Nat <: Int
+;;   - Int <: Num
+;;   - →
+;; Terms:
+;; - terms from stlc+lit.rkt, except redefined: datum and +
+;; - also *
+;; Other: sub? current-sub?
+
+(define-base-type Top)
+(define-base-type Num)
+(define-base-type Nat)
+
+(define-primop + : (→ Num Num Num))
+(define-primop * : (→ Num Num Num))
+
+(define-typed-syntax #%datum
+  [(#%datum . n:nat) ▶
+   --------
+   [⊢ [[_ ≫ (#%datum- . n)] ⇒ (: Nat)]]]
+  [(#%datum . n:integer) ▶
+   --------
+   [⊢ [[_ ≫ (#%datum- . n)] ⇒ (: Int)]]]
+  [(#%datum . n:number) ▶
+   --------
+   [⊢ [[_ ≫ (#%datum- . n)] ⇒ (: Num)]]]
+  [(#%datum . x) ▶
+   --------
+   [_ ≻ (ext:#%datum . x)]])
+
+(begin-for-syntax
+  (define (sub? t1 t2)
+    ; need this because recursive calls made with unexpanded types
+    (define τ1 ((current-type-eval) t1))
+    (define τ2 ((current-type-eval) t2))
+;    (printf "t1 = ~a\n" (syntax->datum τ1))
+;    (printf "t2 = ~a\n" (syntax->datum τ2))
+    (or ((current-type=?) τ1 τ2)
+        (Top? τ2)))
+  (define current-sub? (make-parameter sub?))
+  (current-typecheck-relation sub?)
+  (define (subs? τs1 τs2)
+    (and (stx-length=? τs1 τs2)
+         (stx-andmap (current-sub?) τs1 τs2)))
+  
+  (define-syntax (define-sub-relation stx)
+    (syntax-parse stx #:datum-literals (<: =>)
+      [(_ τ1:id <: τ2:id)
+       #:with τ1-expander (format-id #'τ1 "~~~a" #'τ1)
+       #:with τ2-expander (format-id #'τ2 "~~~a" #'τ2)
+       #:with fn (generate-temporary)
+       #:with old-sub? (generate-temporary)
+       #'(begin
+           (define old-sub? (current-sub?))
+           (define (fn t1 t2)
+             (define τ1 ((current-type-eval) t1))
+             (define τ2 ((current-type-eval) t2))
+             (syntax-parse (list τ1 τ2)
+               [(τ1-expander τ) ((current-sub?) #'τ2 #'τ)]
+               [(τ τ2-expander) ((current-sub?) #'τ #'τ1)]
+               [_ #f]))
+           (current-sub? (λ (t1 t2) (or (old-sub? t1 t2) (fn t1 t2))))
+           (current-typecheck-relation (current-sub?)))]
+      [(_ (~seq τ1:id <: τ2:id (~and (~literal ...) ddd))
+          (~seq τ3:id <: τ4:id)
+           =>
+          (tycon1 . rst1) <: (tycon2 . rst2))
+       #:with tycon1-expander (format-id #'tycon1 "~~~a" #'tycon1)
+       #:with tycon2-expander (format-id #'tycon2 "~~~a" #'tycon2)
+       #:with fn (generate-temporary)
+       #:with old-sub? (generate-temporary)
+       #'(begin
+           (define old-sub? (current-sub?))
+           (define (fn t1 t2)
+             (define τ1 ((current-type-eval) t1))
+             (define τ2 ((current-type-eval) t2))
+             (syntax-parse (list τ1 τ2)
+               [((tycon1-expander . rst1) (tycon2-expander . rst2))
+                (and (subs? #'(τ1 ddd) #'(τ2 ddd))
+                     ((current-sub?) #'τ3 #'τ4))]
+               [_ #f]))
+           (current-sub? (λ (t1 t2) (or (old-sub? t1 t2) (fn t1 t2))))
+           (current-typecheck-relation (current-sub?)))]))
+
+  (define-sub-relation Nat <: Int)
+  (define-sub-relation Int <: Num)
+  (define-sub-relation t1 <: s1 ... s2 <: t2 => (→ s1 ... s2) <: (→ t1 ... t2))
+  
+  (define (join t1 t2)
+    (cond
+      [((current-sub?) t1 t2) t2]
+      [((current-sub?) t2 t1) t1]
+      [else #'Top]))
+  (current-join join))