www

commit 5c2850123682dc033f2d025f7a5580f71df066be
parent 6cb15a06da533e6efc2d918df38c91b1b482e891
Author: Stephen Chang <stchang@ccs.neu.edu>
Date:   Wed, 13 Apr 2016 18:03:49 -0400

add some type validation in define-type

Diffstat:
M
tapl/mlish.rkt
 | 
42
+++++++++++++++++++++++++++++++++++++-----
M
tapl/tests/mlish/loop.mlish
 | 
30
+++++++++++++++++++++---------
M
tapl/tests/mlish/polyrecur.mlish
 | 
10
++++++----

3 files changed, 64 insertions(+), 18 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -109,10 +109,10 @@
                                     (syntax->datum #'e_fn)))))])]))
 
   ;; instantiate polymorphic types
-  (define (inst-type ty-solved Xs ty)
-    (substs ty-solved Xs ty))
-  (define (inst-types ty-solved Xs tys)
-    (stx-map (lambda (t) (inst-type ty-solved Xs t)) tys))
+  (define (inst-type tys-solved Xs ty)
+    (substs tys-solved Xs ty))
+  (define (inst-types tys-solved Xs tys)
+    (stx-map (lambda (t) (inst-type tys-solved Xs t)) tys))
   )
 
 ;; define --------------------------------------------------
@@ -170,7 +170,10 @@
         (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))])
 
 ;; define-type -----------------------------------------------
-;; TODO: should validate τ as part of define-type definition (before it's ever used)
+;; TODO: should validate τ as part of define-type definition (before it's used)
+;; - not completely possible, since some constructors may not be defined yet,
+;;   ie, mutually recursive datatypes
+;; for now, validate types but punt if encountering unbound ids
 (define-syntax (define-type stx)
   (syntax-parse stx
     [(_ Name:id . rst)
@@ -188,6 +191,35 @@
                    (Cons [fld (~datum :) τ] ...)
                    (~and (Cons τ ...)
                          (~parse (fld ...) (generate-temporaries #'(τ ...)))))) ...)
+     ;; validate tys
+     #:with (ty_flat ...) (stx-flatten #'((τ ...) ...))
+     #:with (_ _ (_ _ (_ _ (_ _ ty+ ...))))
+            (with-handlers 
+              ([exn:fail:syntax:unbound?
+                (λ (e) 
+                  (define X (stx-car (exn:fail:syntax-exprs e)))
+                  #`(lambda () (let-syntax () (let-syntax () (#%app void unbound)))))])
+              (expand/df 
+                #`(lambda (X ...)
+                    (let-syntax 
+                      ([Name 
+                        (syntax-parser 
+                         [(_ X ...) (mk-type #'void)]
+                         [stx 
+                          (type-error 
+                           #:src #'stx
+                           #:msg 
+                           (format "Improper use of constructor ~a; expected ~a args, got ~a"
+                                   (syntax->datum #'Name) (stx-length #'(X ...))
+                                   (stx-length (stx-cdr #'stx))))])]
+                       [X (make-rename-transformer (⊢ X #%type))] ...)
+                      (void ty_flat ...)))))
+     #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...)))
+                (stx-map 
+                  (lambda (t+ t) (unless (type? t+)
+                              (type-error #:src t
+                                          #:msg "~a is not a valid type" t)))
+                  #'(ty+ ...) #'(ty_flat ...)))
      #:with NameExpander (format-id #'Name "~~~a" #'Name)
      #:with NameExtraInfo (format-id #'Name "~a-extra-info" #'Name)
      #:with (StructName ...) (generate-temporaries #'(Cons ...))
diff --git a/tapl/tests/mlish/loop.mlish b/tapl/tests/mlish/loop.mlish
@@ -6,6 +6,21 @@
   (A X) 
   (B X X))
 
+(typecheck-fail
+    (define-type (Test2 X)
+      (AA (Test2 X X)))
+  #:with-msg "Improper use of constructor Test2; expected 1 args, got 2")
+
+(typecheck-fail
+    (define-type (Test3 X)
+      (AA (→)))
+  #:with-msg "Improper usage of type constructor →")
+
+(typecheck-fail
+    (define-type (Test4 X)
+      (AA (+ 1 2)))
+  #:with-msg "\\(\\+ 1 2\\) is not a valid type")
+
 (check-type (A 1) : (Test Int))
 (check-type (B 1 2) : (Test Int))
 
@@ -53,15 +68,12 @@
   NB
   (CB X (ListA X)))
 
-;; TODO: error should occur here
-(define-type (ListC X)
-  NC
-  (CC X (ListA X X))) ; misapplication of ListA type constructor
-
-(check-type NC : (ListC Int))
-(typecheck-fail (CC 1 NA)) ; and not here
-
-;; (define (g [x : (ListA Int Int)] -> Int) 0)
+(typecheck-fail
+    (define-type (ListC X)
+      NC
+      (CC X (ListA X X)))
+  #:with-msg 
+  "Improper usage of type constructor ListA: \\(ListA X X\\), expected = 1 arguments")
 
 (typecheck-fail (CA 1 NA))
 (check-type (CA 1 NB) : (ListA Int))
diff --git a/tapl/tests/mlish/polyrecur.mlish b/tapl/tests/mlish/polyrecur.mlish
@@ -94,15 +94,17 @@
 (define-type (BankersDeque A)
   [BD Int (List A) Int (List A)])
 
-(define-type (ImplicitCatDeque A)
-  [Shall (BankersDeque A)]
-  [Dp (BankersDeque A)
+(typecheck-fail
+    (define-type (ImplicitCatDeque A)
+      [Shall (BankersDeque A)]
+      [Dp (BankersDeque A)
         (ImplicitCatDeque (BankersDeque A) (CmpdElem (BankersDeque A)))
         (BankersDeque A)
         (ImplicitCatDeque (BankersDeque A) (CmpdElem (BankersDeque A)))
         (BankersDeque A)])
+  #:with-msg "Improper use of constructor ImplicitCatDeque; expected 1 args, got 2")
 
-(define-type (CmpdElem A)
+#;(define-type (CmpdElem A)
   [Simple (BankersDeque A)]
   [Cmpd (BankersDeque A) 
         (ImplicitCatDeque (BankersDeque (CmpdElem (BankersDeque A))))