From a788c4a7d5f82fe187e07e84a4efd3835b7b707e Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Tue, 31 Jan 2017 14:30:46 -0500 Subject: [PATCH] macrotypes/mlish and macrotypes/mlish+adhoc tests passing --- macrotypes/examples/fomega3.rkt | 32 --- macrotypes/examples/fsub.rkt | 2 +- macrotypes/examples/mlish+adhoc.rkt | 4 +- macrotypes/examples/mlish.rkt | 2 +- macrotypes/examples/tests/ext-stlc-tests.rkt | 2 +- macrotypes/examples/tests/fomega3-tests.rkt | 200 ------------------- macrotypes/examples/tests/general-tests.rkt | 6 +- macrotypes/examples/tests/infer-tests.rkt | 2 +- macrotypes/examples/tests/mlish-tests.rkt | 4 +- macrotypes/typecheck.rkt | 8 +- turnstile/examples/fsub.rkt | 2 +- turnstile/examples/tests/ext-stlc-tests.rkt | 2 +- 12 files changed, 20 insertions(+), 246 deletions(-) delete mode 100644 macrotypes/examples/fomega3.rkt delete mode 100644 macrotypes/examples/tests/fomega3-tests.rkt diff --git a/macrotypes/examples/fomega3.rkt b/macrotypes/examples/fomega3.rkt deleted file mode 100644 index 2287210..0000000 --- a/macrotypes/examples/fomega3.rkt +++ /dev/null @@ -1,32 +0,0 @@ -#lang s-exp macrotypes/typecheck -(extends "fomega.rkt" #:except tyapp tyλ) - -; same as fomega2.rkt --- λ and #%app works as both regular and type versions, -; → is both type and kind --- but reuses parts of fomega.rkt, -; ie removes the duplication in fomega2.rkt - -;; System F_omega -;; Type relation: -;; - redefine current-kind? and current-type so #%app and λ -;; work for both terms and types -;; Types: -;; - types from fomega.rkt -;; - String from stlc+reco+var -;; Terms: -;; - extend ∀ Λ inst from fomega.rkt -;; - #%datum from stlc+reco+var - -;; types and kinds are now mixed, due to #%app and λ -(begin-for-syntax - (define old-kind? (current-kind?)) - (current-kind? (λ (k) (or (#%type? k) (old-kind? k) (#%type? (typeof k))))) - ;; Try to keep "type?" backward compatible with its uses so far, - ;; eg in the definition of λ or previous type constuctors. - ;; (However, this is not completely possible, eg define-type-alias) - ;; So now "type?" no longer validates types, rather it's a subset. - ;; But we no longer need type? to validate types, instead we can use - ;; (kind? (typeof t)) - (current-type? (λ (t) (or (type? t) - (let ([k (typeof t)]) - (or (★? k) (∀★? k))) - ((current-kind?) t))))) diff --git a/macrotypes/examples/fsub.rkt b/macrotypes/examples/fsub.rkt index 5be7722..6a63767 100644 --- a/macrotypes/examples/fsub.rkt +++ b/macrotypes/examples/fsub.rkt @@ -26,7 +26,7 @@ (begin-for-syntax (define (expose t) (cond [(identifier? t) - (define sub (typeof t #:tag '<:)) + (define sub (detach t '<:)) (if sub (expose sub) t)] [else t])) (current-promote expose) diff --git a/macrotypes/examples/mlish+adhoc.rkt b/macrotypes/examples/mlish+adhoc.rkt index 4c14a3d..0108259 100644 --- a/macrotypes/examples/mlish+adhoc.rkt +++ b/macrotypes/examples/mlish+adhoc.rkt @@ -383,7 +383,7 @@ (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))] ...) + [X (make-rename-transformer (⊢ X :: #%type))] ...) (void ty_flat ...))))) #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...))) (stx-map @@ -854,7 +854,7 @@ (expand/df #'(lambda (X ...) (let-syntax - ([X (make-rename-transformer (assign-type #'X #'#%type))] ...) + ([X (make-rename-transformer (mk-type #'X))] ...) (let-syntax ;; must have this inner macro bc body of lambda may require ;; ops defined by TC to be bound diff --git a/macrotypes/examples/mlish.rkt b/macrotypes/examples/mlish.rkt index b3cc585..8e9232b 100644 --- a/macrotypes/examples/mlish.rkt +++ b/macrotypes/examples/mlish.rkt @@ -447,7 +447,7 @@ (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))] ...) + [X (make-rename-transformer (⊢ X :: #%type))] ...) (void ty_flat ...))))) #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...))) (stx-map diff --git a/macrotypes/examples/tests/ext-stlc-tests.rkt b/macrotypes/examples/tests/ext-stlc-tests.rkt index 7915e12..4abe10f 100644 --- a/macrotypes/examples/tests/ext-stlc-tests.rkt +++ b/macrotypes/examples/tests/ext-stlc-tests.rkt @@ -53,7 +53,7 @@ (typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type") (typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type") (typecheck-fail (ann Bool : Int) - #:with-msg "ann: type mismatch: expected Int, given #f\n *expression: Bool") + #:with-msg "ann: type mismatch: expected Int, given an invalid expression\n *expression: Bool") ; let (check-type (let () (+ 1 1)) : Int ⇒ 2) diff --git a/macrotypes/examples/tests/fomega3-tests.rkt b/macrotypes/examples/tests/fomega3-tests.rkt deleted file mode 100644 index 9a98ede..0000000 --- a/macrotypes/examples/tests/fomega3-tests.rkt +++ /dev/null @@ -1,200 +0,0 @@ -#lang s-exp "../fomega3.rkt" -(require "rackunit-typechecking.rkt") - -(check-type Int : ★) -(check-type String : ★) -(typecheck-fail →) -(check-type (→ Int Int) : ★) -(typecheck-fail (→ →)) -(typecheck-fail (→ 1)) -(check-type 1 : Int) - -;(check-type (∀ ([t : ★]) (→ t t)) : ★) -(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★)) -(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★) - -(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X))) - -(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x))) - : (∀ ([X : ★]) (→ X X))) -(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (→ ★ ★)]) (λ ([x : X]) x)))) - -(check-type (λ ([t : ★]) t) : (→ ★ ★)) -(check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★)) -(check-type (λ ([t : ★]) (λ ([s : ★]) t)) : (→ ★ (→ ★ ★))) -(check-type (λ ([t : (→ ★ ★)]) t) : (→ (→ ★ ★) (→ ★ ★))) -(check-type (λ ([t : (→ ★ ★ ★)]) t) : (→ (→ ★ ★ ★) (→ ★ ★ ★))) -(check-type (λ ([arg : ★] [res : ★]) (→ arg res)) : (→ ★ ★ ★)) - -(check-type ((λ ([t : ★]) t) Int) : ★) -(check-type (λ ([x : ((λ ([t : ★]) t) Int)]) x) : (→ Int Int)) -(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1) -(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2) -(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2) -(typecheck-fail ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) "a-string")) - -;; partial-apply → -(check-type ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int) - : (→ ★ ★)) -; f's type must have kind ★ -(typecheck-fail (λ ([f : ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)]) f)) -(check-type (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) : - (∀ ([tyf : (→ ★ ★)]) (→ (tyf String) (tyf String)))) -(check-type (inst - (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) - ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)) - : (→ (→ Int String) (→ Int String))) -(typecheck-fail - (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)) - ;#:with-msg "not a valid type: 1") - -;; applied f too early -(typecheck-fail (inst - (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1))) - ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))) -(check-type ((inst - (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) - ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)) - (λ ([x : Int]) "int")) : (→ Int String)) -(check-type (((inst - (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) - ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)) - (λ ([x : Int]) "int")) 1) : String ⇒ "int") - -;; tapl examples, p441 -(typecheck-fail - (define-type-alias tmp 1)) - ;#:with-msg "not a valid type: 1") -(define-type-alias Id (λ ([X : ★]) X)) -(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int)) -(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (Id String)) Int)) -(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int String) Int)) -(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int (Id String)) Int)) -(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) (Id String)) Int)) -(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) String) Int)) -(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (→ Int String) Int)) -(check-type (λ ([f : (→ Int String)]) 1) : (→ (Id (→ Int String)) Int)) -(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (→ Int String)) Int)) -(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (Id (→ Int String))) Int)) - -;; tapl examples, p451 -(define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X)))) - -;(check-type Pair : (→ ★ ★ ★)) -(check-type Pair : (→ ★ ★ (∀★ ★))) - -(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X))) -; parametric pair constructor -(check-type - (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) - : (∀ ([X : ★][Y : ★]) (→ X Y (Pair X Y)))) -; concrete Pair Int String constructor -(check-type - (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) - Int String) - : (→ Int String (Pair Int String))) -; Pair Int String value -(check-type - ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) - Int String) 1 "1") - : (Pair Int String)) -; fst: parametric -(check-type - (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x)))) - : (∀ ([X : ★][Y : ★]) (→ (Pair X Y) X))) -; fst: concrete Pair Int String accessor -(check-type - (inst - (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x)))) - Int String) - : (→ (Pair Int String) Int)) -; apply fst -(check-type - ((inst - (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x)))) - Int String) - ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) - Int String) 1 "1")) - : Int ⇒ 1) -; snd -(check-type - (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y)))) - : (∀ ([X : ★][Y : ★]) (→ (Pair X Y) Y))) -(check-type - (inst - (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y)))) - Int String) - : (→ (Pair Int String) String)) -(check-type - ((inst - (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y)))) - Int String) - ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) - Int String) 1 "1")) - : String ⇒ "1") - -;;; sysf tests wont work, unless augmented with kinds -(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X))) - -(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true -(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false -(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv - -(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) - : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2))))) - -(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) - : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4))))) - -(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) - : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4))))) - -(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int)) -(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int) -; first inst should be discarded -(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int)) -; second inst is discarded -(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int)) - -;; polymorphic arguments -(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t))) -(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s))) -(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t)))) -(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t)))) -(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s)))) -(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u)))) -(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u)))) -(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x))) -(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1)) -(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u))) -(check-type - (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int)) -(check-type - ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10) - : Int ⇒ 10) -(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int))) -(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int)) -(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) - (Λ ([s : ★]) (λ ([y : s]) y))) - : Int ⇒ 10) - - -;; previous tests ------------------------------------------------------------- -(check-type 1 : Int) -(check-not-type 1 : (→ Int Int)) -;(typecheck-fail #f) ; unsupported literal -(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) -(check-not-type (λ ([x : Int]) x) : Int) -(check-type (λ ([x : Int]) x) : (→ Int Int)) -(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) -(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) -(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type -(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type -(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type -(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) - : (→ (→ Int Int Int) Int Int Int)) -(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) -(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int -(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int -(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args -(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) diff --git a/macrotypes/examples/tests/general-tests.rkt b/macrotypes/examples/tests/general-tests.rkt index aed236c..5fa6e70 100644 --- a/macrotypes/examples/tests/general-tests.rkt +++ b/macrotypes/examples/tests/general-tests.rkt @@ -15,9 +15,9 @@ (define-type-constructor -> #:arity > 0) (define-binding-type mu #:arity = 1 #:bvs = 1) (define-binding-type forall #:bvs = 1 #:arity = 1) - (define-binding-type exist #:no-attach-kind #:bvs = 1 #:arity = 1) - (define-binding-type exist2 #:bvs = 1 #:arity = 1 #:no-attach-kind) - (define-binding-type exist3 #:bvs = 1 #:no-attach-kind #:arity = 1) + (define-binding-type exist #:extra-info void #:bvs = 1 #:arity = 1) + (define-binding-type exist2 #:bvs = 1 #:arity = 1 #:extra-info void) + (define-binding-type exist3 #:bvs = 1 #:extra-info void #:arity = 1) (check-stx-err (define-binding-type exist4 #:bvs = 1 #:no-attach- #:arity = 1) diff --git a/macrotypes/examples/tests/infer-tests.rkt b/macrotypes/examples/tests/infer-tests.rkt index a0bc3ba..7e80b3d 100644 --- a/macrotypes/examples/tests/infer-tests.rkt +++ b/macrotypes/examples/tests/infer-tests.rkt @@ -246,7 +246,7 @@ (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier") (typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type") (typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type") -(typecheck-fail (ann Bool : Int) #:with-msg "expected Int, given #f\n *expression: Bool") +(typecheck-fail (ann Bool : Int) #:with-msg "expected Int, given an invalid expression\n *expression: Bool") ; let (check-type (let () (+ 1 1)) : Int ⇒ 2) diff --git a/macrotypes/examples/tests/mlish-tests.rkt b/macrotypes/examples/tests/mlish-tests.rkt index c455d80..75abf81 100644 --- a/macrotypes/examples/tests/mlish-tests.rkt +++ b/macrotypes/examples/tests/mlish-tests.rkt @@ -64,6 +64,8 @@ (check-type (g2 Nil) : (List (List Int)) ⇒ Nil) (check-type (g2 Nil) : (List (→ Int Int)) ⇒ Nil) +(check-type (λ ([x : (List Int)]) x) : (→/test (List Int) (List Int))) + (check-type (g2 (Cons 1 Nil)) : (List Int) ⇒ (Cons 1 Nil)) (check-type (g2 (Cons "1" Nil)) : (List String) ⇒ (Cons "1" Nil)) @@ -675,7 +677,7 @@ (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier") (typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type") (typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type") -(typecheck-fail (ann Int : Int) #:with-msg "expected Int, given #%type\n *expression: Int") +(typecheck-fail (ann Int : Int) #:with-msg "expected Int, given an invalid expression\n *expression: Int") ; let (check-type (let () (+ 1 1)) : Int ⇒ 2) diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt index e545bb5..14cc917 100644 --- a/macrotypes/typecheck.rkt +++ b/macrotypes/typecheck.rkt @@ -194,7 +194,8 @@ ;; If Val is a non-empty list, return first element, otherwise return Val. (define (get-stx-prop/car stx tag) (define v (syntax-property stx tag)) - (if (cons? v) (car v) v)) + (let L ([v v]) + (if (cons? v) (L (car v)) v))) ;; A Tag is a Symbol serving as a stx prop key for some kind of metadata. ;; e.g., ': for types, ':: for kinds, etc. @@ -408,6 +409,7 @@ (combine-out . ts) (combine-out . t-s) (for-syntax (combine-out . t-expanders) . t?s))) modes)])))) + ;; base types -------------------------------------------------------- (define-syntax define-base-type (syntax-parser [(_ (~var τ id)) ; default to 'key2 and #%tag @@ -448,6 +450,7 @@ (syntax-parser [(_ (~var x id) (... ...)) #'(begin (define-base-type x) (... ...))])) + ;; type constructors ------------------------------------------------- (define-syntax define-internal-type-constructor (syntax-parser ; [(_ (~var x id) . rst) @@ -899,7 +902,8 @@ (define (typecheck-fail-msg/1 τ_expected τ_given expression) (format "type mismatch: expected ~a, given ~a\n expression: ~s" (type->str τ_expected) - (type->str τ_given) + (or (and (syntax-e τ_given) (type->str τ_given)) + "an invalid expression") (syntax->datum (get-orig expression)))) ;; typecheck-fail-msg/1/no-expr : Type Type Stx -> String diff --git a/turnstile/examples/fsub.rkt b/turnstile/examples/fsub.rkt index 5345700..2349d7d 100644 --- a/turnstile/examples/fsub.rkt +++ b/turnstile/examples/fsub.rkt @@ -26,7 +26,7 @@ (begin-for-syntax (define (expose t) (cond [(identifier? t) - (define sub (typeof t #:tag '<:)) + (define sub (detach t '<:)) (if sub (expose sub) t)] [else t])) (current-promote expose) diff --git a/turnstile/examples/tests/ext-stlc-tests.rkt b/turnstile/examples/tests/ext-stlc-tests.rkt index 8cdcd71..889bd4d 100644 --- a/turnstile/examples/tests/ext-stlc-tests.rkt +++ b/turnstile/examples/tests/ext-stlc-tests.rkt @@ -53,7 +53,7 @@ (typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type") (typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type") (typecheck-fail (ann Bool : Int) - #:with-msg "ann: type mismatch: expected Int, given #f\n *expression: Bool") + #:with-msg "ann: type mismatch: expected Int, given an invalid expression\n *expression: Bool") ; let (check-type (let () (+ 1 1)) : Int ⇒ 2)