www

commit 5497b347df8749fb1efea41da13fb11534c97508
parent 050c43b3a2eea7fc53f17219970b633799059b8d
Author: Ben Greenman <types@ccs.neu.edu>
Date:   Fri,  9 Oct 2015 02:24:09 -0400

[occurrence] simple type evaluator, assumes no recursive unions

Diffstat:
M
tapl/stlc+occurrence.rkt
 | 
18
++++++++++++++++--
M
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
@@ -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
@@ -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")