[occurrence] type eval

tapl/stlc+occurrence.rkt

@@ -24,18 +24,31 @@
 ;; TODO disallow recursive ∪
 (begin-for-syntax
   (define τ-eval (current-type-eval))
-  (define (∪-eval τ)
-    (syntax-parse τ #:datum-literals (∪)
-     [(_ ∪ τ* ...)
-      ;; Assumes that each τ is non-∪
-      (define τ*+ (for/list ([τ (in-syntax #'(τ* ...))]) (τ-eval τ)))
-      ;; TODO just make a set
-      #`#,(cons '∪ 
-           (remove-duplicates 
-            (sort τ*+ symbol<? #:key syntax->datum)
-            (current-type=?)))]
+  (define (∪-eval τ-stx)
+    (syntax-parse τ-stx #:datum-literals (∪)
+     [(∪ τ-stx* ...)
+      ;; TODO Assumes that each τ is non-∪
+      ;; TODO just make a set?
+      ;;      will that work if we have ∪ inside the ∪ ?
+      ;(printf "Syntax prop type is ~a\n" (syntax-property (τ-eval τ) 'type))
+      (define τ*
+        (sort
+         (remove-duplicates (syntax->list #'(τ-stx* ...)) (current-type=?))
+         symbol<?
+         #:key syntax->datum))
+      (define τ
+        (cond
+         [(null? τ*)
+          (raise-user-error 'τ-eval "~a (~a:~a) empty union type ~a\n"
+                            (syntax-source τ-stx) (syntax-line τ-stx) (syntax-column τ-stx)
+                            (syntax->datum τ-stx))]
+         [(null? (cdr τ*))
+          #`#,(car τ*)]
+         [else
+          #`#,(cons #'∪ τ*)]))
+      (τ-eval τ)]
      [_
-      (τ-eval τ)]))
+      (τ-eval τ-stx)]))
   (current-type-eval ∪-eval))
 
 ;; - subtype U with simple, U with contained

tapl/tests/stlc+occurrence-tests.rkt

@@ -10,27 +10,25 @@
 (check-type 1 : Top)
 (check-type (λ ([x : (∪ Boolean Int)]) x)
             : (→ (∪ Boolean Int) (∪ Boolean Int)))
-(check-type (λ ([x : (∪ Int Int Int Int)]) x)
-            : (→ (∪ Int Int Int Int) (∪ Int Int Int Int)))
 
 (typecheck-fail
  (λ ([x : ∪]) x)
  #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments")
 (typecheck-fail
  (λ ([x : (∪)]) x)
- #:with-msg "Improper usage of type constructor ∪")
+ #:with-msg "empty union type")
 (typecheck-fail
  (λ ([x : (∪ ∪)]) x)
- #:with-msg "not a valid type")
+ #:with-msg "Improper usage of type constructor ∪")
 (typecheck-fail
  (λ ([x : (1 ∪)]) x)
- #:with-msg "not a valid type")
+ #:with-msg "")
 (typecheck-fail
  (λ ([x : (Int ∪)]) x)
- #:with-msg "not a valid type")
+ #:with-msg "expected identifier")
 (typecheck-fail
  (λ ([x : (→ ∪ ∪)]) x)
- #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments")
+ #:with-msg "Improper usage of type constructor ∪")
 (typecheck-fail
  (λ ([x : (→ Int ∪)]) x)
  #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments")
@@ -38,6 +36,18 @@
  (λ ([x : (∪ Int →)]) x)
  #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
 
+;; -----------------------------------------------------------------------------
+;; --- type evaluation
+
+(check-type (λ ([x : (∪ Int Int Int Int)]) x)
+            : (→ Int Int))
+(check-type (λ ([x : (∪ Int Boolean)]) 42)
+            : (→ (∪ Boolean Int) Int))
+(check-type (λ ([x : (∪ Int Boolean Boolean Int)]) x)
+            : (→ (∪ Boolean Int) (∪ Boolean Int)))
+
+;; -----------------------------------------------------------------------------
+;; --- basic subtyping
 ;; (check-type 1 : (∪ Int))
 ;; (check-type 1 : (∪ Int Boolean))
 ;; (check-type 1 : (∪ Boolean Int))