From 5497b347df8749fb1efea41da13fb11534c97508 Mon Sep 17 00:00:00 2001
From: Ben Greenman <types@ccs.neu.edu>
Date: Fri, 9 Oct 2015 02:24:09 -0400
Subject: [PATCH] [occurrence] simple type evaluator, assumes no recursive
 unions

---
 tapl/stlc+occurrence.rkt             | 18 ++++++++++++++++--
 tapl/tests/stlc+occurrence-tests.rkt |  8 +++-----
 2 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt
index 4384c55..23655e8 100644
--- a/tapl/stlc+occurrence.rkt
+++ b/tapl/stlc+occurrence.rkt
@@ -21,9 +21,23 @@
   [(_ . x) #'(stlc+sub:#%datum . x)])
 
 (define-type-constructor ∪ #:arity >= 1)
+;; 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=?)))]
+     [_
+      (τ-eval τ)]))
+  (current-type-eval ∪-eval))
 
-;; - define normal form for U, sorted
-;; - TEST create U types
 ;; - subtype U with simple, U with contained
 ;; - TEST subtyping, with 'values' and with 'functions'
 ;; - add filters
diff --git a/tapl/tests/stlc+occurrence-tests.rkt b/tapl/tests/stlc+occurrence-tests.rkt
index 50ec6fb..9b22aa0 100644
--- a/tapl/tests/stlc+occurrence-tests.rkt
+++ b/tapl/tests/stlc+occurrence-tests.rkt
@@ -21,15 +21,13 @@
  #:with-msg "Improper usage of type constructor ∪")
 (typecheck-fail
  (λ ([x : (∪ ∪)]) x)
- #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments")
+ #:with-msg "not a valid type")
 (typecheck-fail
  (λ ([x : (1 ∪)]) x)
- ;; TODO Weird message for this one.
- #:with-msg "Expected expression 1 to have → type")
+ #:with-msg "not a valid type")
 (typecheck-fail
  (λ ([x : (Int ∪)]) x)
- ;; TODO a little weird of a message
- #:with-msg "expected identifier")
+ #:with-msg "not a valid type")
 (typecheck-fail
  (λ ([x : (→ ∪ ∪)]) x)
  #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments")