From 3a337848b4a6c23dd0f3f02e0ddfd4bcde9639bd Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 26 May 2015 19:34:42 -0400
Subject: [PATCH] start stlc+sub

---
 tapl/README.md                                | 16 +++++----
 tapl/stlc+sub.rkt                             | 35 +++++++++++++++++++
 .../{stlc+box.rkt => stlc+box-tests.rkt}      |  0
 tapl/tests/stlc+sub-tests.rkt                 |  4 +++
 4 files changed, 48 insertions(+), 7 deletions(-)
 create mode 100644 tapl/stlc+sub.rkt
 rename tapl/tests/{stlc+box.rkt => stlc+box-tests.rkt} (100%)
 create mode 100644 tapl/tests/stlc+sub-tests.rkt

diff --git a/tapl/README.md b/tapl/README.md
index a6fd647..35bbf1a 100644
--- a/tapl/README.md
+++ b/tapl/README.md
@@ -1,10 +1,12 @@
 extension hierarchy
 
-A file2 that is immediately below a fileX.rkt extends that fileX.rkt.
+A file extends its immediate parent file.
 
-1) stlc.rkt
-2) stlc+lit.rkt
-3) ext-stlc.rkt
-4) stlc+tup.rkt
-5) stlc+var.rkt
-6) stlc+cons.rkt
\ No newline at end of file
+- stlc.rkt
+   - stlc+lit.rkt
+     - ext-stlc.rkt
+       - stlc+tup.rkt
+         - stlc+var.rkt
+           - stlc+cons.rkt
+             - stlc+box.rkt
+  - stlc+sub.rkt
\ No newline at end of file
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
new file mode 100644
index 0000000..4f319a6
--- /dev/null
+++ b/tapl/stlc+sub.rkt
@@ -0,0 +1,35 @@
+#lang racket/base
+(require
+  (for-syntax racket/base syntax/parse)
+  "typecheck.rkt")
+(require (prefix-in stlc: (only-in "stlc.rkt" #%app λ))
+         (except-in "stlc.rkt" #%app λ)
+         (prefix-in lit: (only-in "stlc+lit.rkt" Int))
+         (except-in "stlc+lit.rkt" Int))
+(provide (rename-out [stlc:#%app #%app]
+                     [stlc:λ λ]))
+(provide (all-from-out "stlc.rkt")
+         (all-from-out "stlc+lit.rkt"))
+(provide Int)
+
+;; can't write any terms with no base types
+
+;; Simply-Typed Lambda Calculus, plus subtyping
+;; Types:
+;; - types from stlc.rkt and stlc+lit.rkt
+;; Terms:
+;; - terms from stlc.rkt, stlc+lit.rkt
+
+(begin-for-syntax
+  (define (<: τ1 τ2)
+    (syntax-property τ1 'super τ2))
+  (define (sub? τ1 τ2)
+    (or (type=? τ1 τ2)
+        (syntax-parse (list τ1 τ2) #:literals (→)
+         [((→ s1 s2) (→ t1 t2))
+          (and (sub? #'t1 #'s1)
+               (sub? #'s1 #'t2))]))))
+
+(define-base-type Num)
+(define-syntax Int (make-rename-transformer (⊢ #'lit:Int #'Num)))
+
diff --git a/tapl/tests/stlc+box.rkt b/tapl/tests/stlc+box-tests.rkt
similarity index 100%
rename from tapl/tests/stlc+box.rkt
rename to tapl/tests/stlc+box-tests.rkt
diff --git a/tapl/tests/stlc+sub-tests.rkt b/tapl/tests/stlc+sub-tests.rkt
new file mode 100644
index 0000000..26d129c
--- /dev/null
+++ b/tapl/tests/stlc+sub-tests.rkt
@@ -0,0 +1,4 @@
+#lang s-exp "../stlc+sub.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; cannot have tests without base types
\ No newline at end of file