www

commit 1fc2b3f538953f66ba045e2e70ebd1d6b194e867
parent 9b9c1dda9610daa4af1ad247e04a09a49a5004b3
Author: Stephen Chang <stchang@ccs.neu.edu>
Date:   Wed, 20 Apr 2016 15:42:52 -0400

change current-join to throw error on fail

- returns join type on success

Diffstat:
M
tapl/ext-stlc.rkt
 | 
14
+++++++++-----
M
tapl/stlc+reco+sub.rkt
 | 
10
+---------
M
tapl/stlc+sub.rkt
 | 
13
++++++++++---

3 files changed, 20 insertions(+), 17 deletions(-)
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
@@ -51,7 +51,15 @@
    (⊢ (or e- ...) : Bool)])
 
 (begin-for-syntax 
-  (define current-join (make-parameter (λ (x y) x))))
+  (define current-join 
+    (make-parameter 
+      (λ (x y) 
+        (unless (typecheck? x y)
+          (type-error
+            #:src x
+            #:msg  "branches have incompatible types: ~a and ~a" x y))
+        x))))
+
 (define-typed-syntax if
   [(~and ifstx (_ e_tst e1 e2))
    #:with τ-expected (get-expected-type #'ifstx)
@@ -62,10 +70,6 @@
    #:with (e1- τ1) (infer+erase #'e1_ann)
    #:with (e2- τ2) (infer+erase #'e2_ann)
    #:with τ-out ((current-join) #'τ1 #'τ2)
-   #:fail-unless (and (typecheck? #'τ1 #'τ-out)
-                      (typecheck? #'τ2 #'τ-out))
-                  (format "branches have incompatible types: ~a and ~a"
-                          (type->str #'τ1) (type->str #'τ2))
    (⊢ (if e_tst- e1- e2-) : τ-out)])
 
 (define-base-type Unit)
diff --git a/tapl/stlc+reco+sub.rkt b/tapl/stlc+reco+sub.rkt
@@ -45,11 +45,4 @@
          #'([l τl] ...))]
        [_ #f])))
   (current-sub? sub?)
-  (current-typecheck-relation (current-sub?))
-
-  (define (join t1 t2)
-    (cond
-      [((current-sub?) t1 t2) t2]
-      [((current-sub?) t2 t1) t1]
-      [else #'Top]))
-  (current-join join))
-\ No newline at end of file
+  (current-typecheck-relation (current-sub?)))
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
@@ -1,7 +1,8 @@
 #lang s-exp "typecheck.rkt"
 (extends "stlc+lit.rkt" #:except #%datum +)
 (reuse Bool String add1 #:from "ext-stlc.rkt")
-(require (prefix-in ext: (only-in "ext-stlc.rkt" #%datum)))
+(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
@@ -88,5 +89,11 @@
 
   (define-sub-relation Nat <: Int)
   (define-sub-relation Int <: Num)
-  (define-sub-relation t1 <: s1 ... s2 <: t2 => (→ s1 ... s2) <: (→ t1 ... t2)))
-           
+  (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))