From e9cc782aebefd9c029aaebb1ae92457dcb5f8199 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Mon, 30 Jan 2017 10:28:22 -0500 Subject: [PATCH] STUCK: infer must know about sep --- macrotypes/examples/exist.rkt | 2 +- macrotypes/examples/fomega.rkt | 21 +- macrotypes/examples/fsub.rkt | 2 +- macrotypes/examples/mlish+adhoc.rkt | 2 +- macrotypes/examples/stlc+overloading.rkt | 2 +- macrotypes/examples/sysf.rkt | 2 +- macrotypes/examples/tests/ext-stlc-tests.rkt | 4 +- macrotypes/examples/tests/fomega-tests.rkt | 364 +++++++------- macrotypes/examples/tests/infer-tests.rkt | 2 +- macrotypes/typecheck.rkt | 447 ++++++++++-------- turnstile/examples/exist.rkt | 2 +- turnstile/examples/fsub.rkt | 2 +- turnstile/examples/infer.rkt | 2 +- turnstile/examples/mlish+adhoc.rkt | 4 +- turnstile/examples/mlish.rkt | 8 +- turnstile/examples/sysf.rkt | 2 +- turnstile/examples/tests/ext-stlc-tests.rkt | 4 +- .../examples/tests/rackunit-typechecking.rkt | 10 +- turnstile/examples/trivial.rkt | 2 +- 19 files changed, 457 insertions(+), 427 deletions(-) diff --git a/macrotypes/examples/exist.rkt b/macrotypes/examples/exist.rkt index d33d4f9..8ca71f4 100644 --- a/macrotypes/examples/exist.rkt +++ b/macrotypes/examples/exist.rkt @@ -69,6 +69,6 @@ #:with τ_x (subst #'X #'Y #'τ_body) #:with [(X-) (x-) (e-) (τ_e)] (infer #'(e) - #:tvctx #'([X : #%type]) + #:tvctx #'([X :: #%type]) #:ctx #`([x : τ_x])) (⊢ (let- ([x- e_packed-]) e-) : τ_e)]) diff --git a/macrotypes/examples/fomega.rkt b/macrotypes/examples/fomega.rkt index 89a0dda..57d27fb 100644 --- a/macrotypes/examples/fomega.rkt +++ b/macrotypes/examples/fomega.rkt @@ -17,7 +17,7 @@ (type-out ★ ⇒ ∀★ ∀) Λ inst tyλ tyapp) -(define-syntax-category kind) +(define-syntax-category :: kind :::) ; want #%type to be equiv to★ ; => edit current-kind? so existing #%type annotations (with no #%kind tag) @@ -32,7 +32,7 @@ ;; But we no longer need type? to validate types, instead we can use ;; (kind? (typeof t)) (current-type? (λ (t) - (define k (typeof t)) + (define k (kindof t)) #;(or (type? t) (★? (typeof t)) (∀★? (typeof t))) (and ((current-kind?) k) (not (⇒? k)))))) @@ -83,9 +83,9 @@ (define old-type=? (current-type=?)) ; ty=? == syntax eq and syntax prop eq (define (type=? t1 t2) - (let ([k1 (typeof t1)][k2 (typeof t2)]) + (let ([k1 (kindof t1)][k2 (kindof t2)]) (and (or (and (not k1) (not k2)) - (and k1 k2 ((current-type=?) k1 k2))) + (and k1 k2 ((current-kind=?) k1 k2))) (old-type=? t1 t2)))) (current-type=? type=?) (current-typecheck-relation (current-type=?))) @@ -93,15 +93,15 @@ (define-typed-syntax Λ [(_ bvs:kind-ctx e) #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e) - (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]) + (⊢ e- : (∀ ([tv- :: bvs.kind] ...) τ_e))]) (define-typed-syntax inst [(_ e τ ...) #:with [e- τ_e] (infer+erase #'e) #:with (~∀ (tv ...) τ_body) #'τ_e - #:with (~∀★ k ...) (typeof #'τ_e) + #:with (~∀★ k ...) (kindof #'τ_e) #:with ([τ- k_τ] ...) (infers+erase #'(τ ...)) - #:fail-unless (typechecks? #'(k_τ ...) #'(k ...)) + #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...)) (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...)) #:with τ_inst (substs #'(τ- ...) #'(tv ...) #'τ_body) @@ -112,15 +112,16 @@ (define-typed-syntax tyλ [(_ bvs:kind-ctx τ_body) #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body) + #:do [(displayln (stx->datum #'k_body))] #:fail-unless ((current-kind?) #'k_body) (format "not a valid type: ~a\n" (type->str #'τ_body)) - (⊢ (λ- tvs- τ_body-) : (⇒ bvs.kind ... k_body))]) + (⊢ (λ- tvs- τ_body-) :: (⇒ bvs.kind ... k_body))]) (define-typed-syntax tyapp [(_ τ_fn τ_arg ...) #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒) #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...)) - #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...)) + #:fail-unless (kindchecks? #'(k_arg ...) #'(k_in ...)) (string-append (format "~a (~a:~a) Arguments to function ~a have wrong kinds(s), " @@ -135,4 +136,4 @@ (format "Expected: ~a arguments with type(s): " (stx-length #'(k_in ...))) (string-join (stx-map type->str #'(k_in ...)) ", ")) - (⊢ (#%app- τ_fn- τ_arg- ...) : k_out)]) + (⊢ (#%app- τ_fn- τ_arg- ...) :: k_out)]) diff --git a/macrotypes/examples/fsub.rkt b/macrotypes/examples/fsub.rkt index c7c79be..5be7722 100644 --- a/macrotypes/examples/fsub.rkt +++ b/macrotypes/examples/fsub.rkt @@ -81,7 +81,7 @@ ;; The "expose" function looks for this tag to enforce the bound, ;; as in TaPL (fig 28-1) #:with ((tv- ...) _ (e-) (τ_e)) - (infer #'(e) #:tvctx #'([tv : #%type <: τsub] ...)) + (infer #'(e) #:tvctx #'([tv :: #%type <: τsub] ...)) (⊢ e- : (∀ ([tv- <: τsub] ...) τ_e))]) (define-typed-syntax inst [(_ e τ:type ...) diff --git a/macrotypes/examples/mlish+adhoc.rkt b/macrotypes/examples/mlish+adhoc.rkt index bee734d..4c14a3d 100644 --- a/macrotypes/examples/mlish+adhoc.rkt +++ b/macrotypes/examples/mlish+adhoc.rkt @@ -1670,7 +1670,7 @@ (~=> TCsub ... (~TC [generic-op-expected ty-concrete-op-expected] ...))) _) - (infers/tyctx+erase #'([X : #%type] ...) #'(TC ... (Name ty ...))) + (infers/tyctx+erase #'([X :: #%type] ...) #'(TC ... (Name ty ...))) #:when (TCs-exist? #'(TCsub ...) #:ctx stx) ;; simulate as if the declared concrete-op* has TC ... predicates ;; TODO: fix this manual deconstruction and assembly diff --git a/macrotypes/examples/stlc+overloading.rkt b/macrotypes/examples/stlc+overloading.rkt index 3b6125e..146b0a6 100644 --- a/macrotypes/examples/stlc+overloading.rkt +++ b/macrotypes/examples/stlc+overloading.rkt @@ -106,7 +106,7 @@ (define-typed-syntax signature [(_ (name:id α:id) τ) - #:with ((α+) (~→ τ_α:id τ-cod) _) (infer/tyctx+erase #'([α : #%type]) #'τ) + #:with ((α+) (~→ τ_α:id τ-cod) _) (infer/tyctx+erase #'([α :: #%type]) #'τ) (define ℜ (ℜ-init #'name #'τ-cod)) (⊢ (define-syntax name (syntax-parser diff --git a/macrotypes/examples/sysf.rkt b/macrotypes/examples/sysf.rkt index 7c08593..dc757d9 100644 --- a/macrotypes/examples/sysf.rkt +++ b/macrotypes/examples/sysf.rkt @@ -15,7 +15,7 @@ (define-typed-syntax Λ [(_ (tv:id ...) e) - #:with [(tv- ...) e- τ] (infer/tyctx+erase #'([tv : #%type] ...) #'e) + #:with [(tv- ...) e- τ] (infer/tyctx+erase #'([tv :: #%type] ...) #'e) (⊢ e- : (∀ (tv- ...) τ))]) (define-typed-syntax inst [(_ e τ:type ...) diff --git a/macrotypes/examples/tests/ext-stlc-tests.rkt b/macrotypes/examples/tests/ext-stlc-tests.rkt index c8594a1..7915e12 100644 --- a/macrotypes/examples/tests/ext-stlc-tests.rkt +++ b/macrotypes/examples/tests/ext-stlc-tests.rkt @@ -52,8 +52,8 @@ (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 "ann: type mismatch: expected Int, given #%type\n *expression: Int") +(typecheck-fail (ann Bool : Int) + #:with-msg "ann: type mismatch: expected Int, given #f\n *expression: Bool") ; let (check-type (let () (+ 1 1)) : Int ⇒ 2) diff --git a/macrotypes/examples/tests/fomega-tests.rkt b/macrotypes/examples/tests/fomega-tests.rkt index 61eab8b..fe02edc 100644 --- a/macrotypes/examples/tests/fomega-tests.rkt +++ b/macrotypes/examples/tests/fomega-tests.rkt @@ -1,211 +1,213 @@ #lang s-exp "../fomega.rkt" (require "rackunit-typechecking.rkt") -(check-type Int : ★) -(check-type String : ★) +(check-type Int :: ★) +(check-type String :: ★) (typecheck-fail →) -(check-type (→ Int Int) : ★) +(check-type (→ Int Int) :: ★) (typecheck-fail (→ →)) (typecheck-fail (→ 1)) (check-type 1 : Int) -(typecheck-fail (tyλ ([x : ★]) 1) #:with-msg "not a valid type: 1") +(typecheck-fail (tyλ ([x :: ★]) 1) #:with-msg "not a valid type: 1") -(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X))) -(check-not-type (Λ ([X : ★]) (λ ([x : X]) x)) : - (∀ ([X : (∀★ ★)]) (→ X X))) +(check-type (Λ ([X :: ★]) (λ ([x : X]) x)) : (∀ ([X :: ★]) (→ X X))) +(check-not-type (Λ ([X :: ★]) (λ ([x : X]) x)) : + (∀ ([X :: (∀★ ★)]) (→ X X))) ;(check-type (∀ ([t : ★]) (→ t t)) : ★) -(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★)) -(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★) +(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))) -(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 ((λ ([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 (tyλ ([t : ★]) t) : (⇒ ★ ★)) -(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★)) -(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★))) -(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★))) -(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★))) -(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★)) +(check-type (tyλ ([t :: ★]) t) :: (⇒ ★ ★)) +;; (check-type (tyλ ([t :: ★] [s :: ★]) t) :: (⇒ ★ ★ ★)) +;; (check-type (tyλ ([t :: ★]) (tyλ ([s :: ★]) t)) :: (⇒ ★ (⇒ ★ ★))) +;; (check-type (tyλ ([t :: (⇒ ★ ★)]) t) :: (⇒ (⇒ ★ ★) (⇒ ★ ★))) +;; (check-type (tyλ ([t :: (⇒ ★ ★ ★)]) t) :: (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★))) +;; (check-type (tyλ ([arg :: ★] [res :: ★]) (→ arg res)) :: (⇒ ★ ★ ★)) -(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★) -(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int)) -(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1) -(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2) -(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2) -(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string")) +;; (check-type (tyapp (tyλ ([t :: ★]) t) Int) :: ★) +;; (check-type (λ ([x : (tyapp (tyλ ([t :: ★]) t) Int)]) x) : (→ Int Int)) +;; (check-type ((λ ([x : (tyapp (tyλ ([t :: ★]) t) Int)]) x) 1) : Int ⇒ 1) +;; (check-type ((λ ([x : (tyapp (tyλ ([t :: ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2) +;; (check-type ((λ ([x : (tyapp (tyλ ([t :: ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2) +;; (typecheck-fail ((λ ([x : (tyapp (tyλ ([t :: ★]) t) Int)]) (+ 1 x)) "a-string")) -;; partial-apply → -(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int) - : (⇒ ★ ★)) -;; f's type must have kind ★ -(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f)) -(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) : - (∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String)))) -(check-type (inst - (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) - (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)) - : (→ (→ Int String) (→ Int String))) -(typecheck-fail - (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1) - #:with-msg "inst: type mismatch\n *expected: +★\n *given: +Int\n *expressions: 1") +;; ;; partial-apply → +;; (check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int) +;; : (⇒ ★ ★)) +;; ;; f's type must have kind ★ +;; (typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f)) +;; (check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) : +;; (∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String)))) +;; (check-type (inst +;; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) +;; (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)) +;; : (→ (→ Int String) (→ Int String))) +;; (typecheck-fail +;; (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1) +;; #:with-msg "inst: type mismatch\n *expected: +★\n *given: +Int\n *expressions: 1") -(typecheck-fail - (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1))) - #:with-msg "Expected → type, got: \\(tyapp tyf String\\)") -;; applied f too early -(typecheck-fail - (inst - (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1))) - (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)) - #:with-msg "Expected → type, got: \\(tyapp tyf String\\)") -(check-type ((inst - (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) - (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)) - (λ ([x : Int]) "int")) : (→ Int String)) -(check-type (((inst - (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) - (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)) - (λ ([x : Int]) "int")) 1) : String ⇒ "int") +;; (typecheck-fail +;; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1))) +;; #:with-msg "Expected → type, got: \\(tyapp tyf String\\)") +;; ;; applied f too early +;; (typecheck-fail +;; (inst +;; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1))) +;; (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)) +;; #:with-msg "Expected → type, got: \\(tyapp tyf String\\)") +;; (check-type ((inst +;; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) +;; (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)) +;; (λ ([x : Int]) "int")) : (→ Int String)) +;; (check-type (((inst +;; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) +;; (tyapp (tyλ ([arg : ★]) (tyλ ([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 (tyλ ([X : ★]) X)) -(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int)) -(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int)) -(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int)) -(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int)) -(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int)) -(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int)) -(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int)) -(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int)) -(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int)) -(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int)) +;; ;; tapl examples, p441 +;; (typecheck-fail +;; (define-type-alias tmp 1) +;; #:with-msg "not a valid type: 1") +;; (define-type-alias Id (tyλ ([X : ★]) X)) +;; (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int)) +;; (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int)) +;; (check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int)) +;; (check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int)) +;; (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int)) +;; (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int)) +;; (check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int)) +;; (check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int)) +;; (check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int)) +;; (check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int)) -;; tapl examples, p451 -(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X)))) +;; ;; tapl examples, p451 +;; (define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X)))) -;(check-type Pair : (⇒ ★ ★ ★)) -(check-type Pair : (⇒ ★ ★ (∀★ ★))) +;; ;(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 (tyapp 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 (tyapp 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") - : (tyapp 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 : ★]) (→ (tyapp 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) - : (→ (tyapp 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 : ★]) (→ (tyapp 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) - : (→ (tyapp 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") +;; (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 (tyapp 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 (tyapp 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") +;; : (tyapp 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 : ★]) (→ (tyapp 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) +;; : (→ (tyapp 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 : ★]) (→ (tyapp 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) +;; : (→ (tyapp 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))) +;; ;; 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 (Λ ([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)))) +;; : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2))))) -(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) - : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4))))) +;; (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-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)) +;; (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) +;; ;; 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) +;; ;; 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/infer-tests.rkt b/macrotypes/examples/tests/infer-tests.rkt index 525bd27..a0bc3ba 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 Int : Int) #:with-msg "expected Int, given #%type\n *expression: Int") +(typecheck-fail (ann Bool : Int) #:with-msg "expected Int, given #f\n *expression: Bool") ; let (check-type (let () (+ 1 1)) : Int ⇒ 2) diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt index 813d264..6a4ce81 100644 --- a/macrotypes/typecheck.rkt +++ b/macrotypes/typecheck.rkt @@ -64,6 +64,7 @@ (define (mk-- id) (format-id id "~a-" id)) (define (mk-~ id) (format-id id "~~~a" id)) (define (mk-#% id) (format-id id "#%~a" id)) + (define (mkx2 id) (format-id id "~a~a" id id)) (define (mk-param id) (format-id id "current-~a" id)) (define-for-syntax (mk-? id) (format-id id "~a?" id)) (define-for-syntax (mk-~ id) (format-id id "~~~a" id)) @@ -184,16 +185,224 @@ (set-stx-prop/preserved e 'expected-type ((current-type-eval) ty)) e)) -;; type assignment +;; define-syntax-category ------------------------------------------------------ +;; A syntax category requires a name and two keys, +;; - one to use when attaching values of this category (eg ': for types) +;; - another for attaching types to these values (eg ':: for kinds on types) +;; If key1 is unspecified, the default is ': +;; If key2 is unspecified, the default is double key1 (ie '::) +;; +;; examples: +;; (define-syntax-category type) +;; (define-syntax-category : type) +;; (define-syntax-category : type ::) +;; (define-syntax-category :: kind :::) +(define-syntax (define-syntax-category stx) + (syntax-parse stx + [(_ name:id) ; default key1 = ': (eg, types) + #'(define-syntax-category : name)] + [(_ key:id name:id) ; default key2 = ':: (eg, kinds) + #`(define-syntax-category key name #,(mkx2 #'key))] + [(_ key1:id name:id key2:id) + #:with names (format-id #'name "~as" #'name) + #:with #%tag (mk-#% #'name) + #:with #%tag? (mk-? #'#%tag) + #:with is-name? (mk-? #'name) + #:with any-name (format-id #'name "any-~a" #'name) + #:with any-name? (mk-? #'any-name) + #:with name-ctx (format-id #'name "~a-ctx" #'name) + #:with name-bind (format-id #'name "~a-bind" #'name) + #:with current-is-name? (mk-param #'is-name?) + #:with current-any-name? (mk-param #'any-name?) + #:with current-namecheck-relation (format-id #'name "current-~acheck-relation" #'name) + #:with namecheck? (format-id #'name "~acheck?" #'name) + #:with namechecks? (format-id #'name "~achecks?" #'name) + #:with current-name-eval (format-id #'name "current-~a-eval" #'name) + #:with default-name-eval (format-id #'name "default-~a-eval" #'name) + #:with name-evals (format-id #'name "~a-evals" #'name) + #:with mk-name (format-id #'name "mk-~a" #'name) + #:with define-base-name (format-id #'name "define-base-~a" #'name) + #:with define-base-names (format-id #'name "define-base-~as" #'name) + #:with define-name-cons (format-id #'name "define-~a-constructor" #'name) + #:with define-binding-name (format-id #'name "define-binding-~a" #'name) + #:with define-internal-name-cons (format-id #'name "define-internal-~a-constructor" #'name) + #:with define-internal-binding-name (format-id #'name "define-internal-binding-~a" #'name) + #:with name-ann (format-id #'name "~a-ann" #'name) + #:with name=? (format-id #'name "~a=?" #'name) + #:with names=? (format-id #'names "~a=?" #'names) + #:with current-name=? (mk-param #'name=?) + #:with same-names? (format-id #'name "same-~as?" #'name) + #:with name-out (format-id #'name "~a-out" #'name) + #:with assign-name (format-id #'name "assign-~a" #'name) + #:with fast-assign-name (format-id #'name "fast-assign-~a" #'name) + #:with nameof (format-id #'name "~aof" #'name) + #'(begin + (define #%tag void) ; TODO: cache expanded #%tag? + (begin-for-syntax + (define (#%tag? t) (and (identifier? t) (free-identifier=? t #'#%tag))) + (define (nameof stx #:tag [tag 'key1]) + (get-stx-prop/car stx tag)) + ;; is-name?, eg type?, corresponds to "well-formed" types + (define (is-name? t) (#%tag? (nameof t #:tag 'key2))) + (define current-is-name? (make-parameter is-name?)) + ;; any-name? corresponds to any type and defaults to is-name? + (define (any-name? t) (is-name? t)) + (define current-any-name? (make-parameter any-name?)) + (define (fast-assign-name e τ #:tag [tag 'key1]) + (set-stx-prop/preserved e tag (syntax-local-introduce τ))) + (define (assign-name e τ #:tag [tag 'key1]) + (fast-assign-name e ((current-name-eval) τ) #:tag tag)) + (define (mk-name t) + (set-stx-prop/preserved t 'key2 #'#%tag)) + (define-syntax-class name ;; e.g., well-formed types + #:attributes (norm) + (pattern τ + #:with norm ((current-name-eval) #'τ) + #:with k (nameof #'norm #:tag 'key2) + #:fail-unless ((current-is-name?) #'norm) + (format "~a (~a:~a) not a well-formed ~a: ~a" + (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ) + 'name (type->str #'τ)))) + (define-syntax-class any-name ;; e.g., any valid type + #:attributes (norm) + (pattern τ + #:with norm ((current-name-eval) #'τ) + #:with k (nameof #'norm) + #:fail-unless ((current-any-name?) #'norm) + (format "~a (~a:~a) not a valid ~a: ~a" + (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ) + 'name (type->str #'τ)))) + (define-syntax-class name-bind #:datum-literals (key1) + #:attributes (x name) + (pattern [x:id key1 ~! (~var ty name)] + #:attr name #'ty.norm) + (pattern any + #:fail-when #t + (format + (string-append + "Improperly formatted ~a annotation: ~a; should have shape [x : τ], " + "where τ is a valid ~a.") + 'name (type->str #'any) 'name) + #:attr x #f #:attr name #f)) + (define-syntax-class name-ctx + #:attributes ((x 1) (name 1)) + (pattern ((~var || name-bind) (... ...)))) + (define-syntax-class name-ann ; type instantiation + #:attributes (norm) + (pattern (~and (_) + (~fail #:unless (brace? this-syntax)) + ((~var t name) ~!)) + #:attr norm (delay #'t.norm)) + (pattern any + #:fail-when #t + (format + (string-append + "Improperly formatted ~a annotation: ~a; should have shape {τ}, " + "where τ is a valid ~a.") + 'name (type->str #'any) 'name) + #:attr norm #f)) + (define (name=? t1 t2) + ;(printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum t1)) + ;(printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum t2)) + (or (and (identifier? t1) (identifier? t2) (free-identifier=? t1 t2)) + (and (stx-null? t1) (stx-null? t2)) + (syntax-parse (list t1 t2) + [(((~literal #%plain-lambda) (~and (_:id (... ...)) xs) . ts1) + ((~literal #%plain-lambda) (~and (_:id (... ...)) ys) . ts2)) + (and (stx-length=? #'xs #'ys) + (stx-length=? #'ts1 #'ts2) + (stx-andmap + (λ (ty1 ty2) + ((current-name=?) (substs #'ys #'xs ty1) ty2)) + #'ts1 #'ts2))] + [_ (and (stx-pair? t1) (stx-pair? t2) + (names=? t1 t2))]))) + (define current-name=? (make-parameter name=?)) + (define (names=? τs1 τs2) + (and (stx-length=? τs1 τs2) + (stx-andmap (current-name=?) τs1 τs2))) + ; extra indirection, enables easily overriding type=? with sub? + ; to add subtyping, without changing any other definitions + (define current-namecheck-relation (make-parameter name=?)) + ;; convenience fns for current-typecheck-relation + (define (namecheck? t1 t2) + ((current-namecheck-relation) t1 t2)) + (define (namechecks? τs1 τs2) + (and (= (stx-length τs1) (stx-length τs2)) + (stx-andmap namecheck? τs1 τs2))) + (define (same-names? τs) + (define τs-lst (syntax->list τs)) + (or (null? τs-lst) + (andmap (λ (τ) ((current-name=?) (car τs-lst) τ)) (cdr τs-lst)))) + ;; type eval + ;; - default-type-eval == full expansion == canonical type representation + ;; - must expand because: + ;; - checks for unbound identifiers (ie, undefined types) + ;; - checks for valid types, ow can't distinguish types and terms + ;; - could parse types but separate parser leads to duplicate code + ;; - later, expanding enables reuse of same mechanisms for kind checking + ;; and type application + (define (default-name-eval τ) + ; TODO: optimization: don't expand if expanded + ; currently, this causes problems when + ; combining unexpanded and expanded types to create new types + (add-orig (expand/df τ) τ)) + (define current-name-eval (make-parameter default-name-eval)) + (define (name-evals τs) #`#,(stx-map (current-name-eval) τs))) + ;; helps with providing defined types + (define-syntax name-out + (make-provide-transformer + (lambda (stx modes) + (syntax-parse stx + ;; cannot write ty:type bc provides might precede type def + [(_ . ts) + #:with t-expanders (stx-map mk-~ #'ts) + #:with t?s (stx-map mk-? #'ts) + (expand-export + (syntax/loc stx (combine-out + (combine-out . ts) + (for-syntax (combine-out . t-expanders) . t?s))) + modes)])))) + (define-syntax define-base-name + (syntax-parser + [(_ (~var x id) new-key new-tag) + #`(define-basic-checked-id-stx x new-key new-tag)] + [(_ (~var x id)) + #'(define-basic-checked-id-stx x key2 #%tag)])) + (define-syntax define-base-names + (syntax-parser + [(_ (~var x id) (... ...)) + #'(begin (define-base-name x) (... ...))])) + (define-syntax define-internal-name-cons + (syntax-parser + [(_ (~var x id) . rst) + #'(define-basic-checked-stx x key2 name #:no-attach-kind . rst)])) + (define-syntax define-internal-binding-name + (syntax-parser + [(_ (~var x id) . rst) + #'(define-binding-checked-stx x key2 name #:no-attach-kind . rst)])) + (define-syntax define-name-cons + (syntax-parser + [(_ (~var x id) . rst) + #'(define-basic-checked-stx x key2 name . rst)])) + (define-syntax define-binding-name + (syntax-parser + [(_ (~var x id) . rst) + #'(define-binding-checked-stx x key2 name . rst)])))])) + +;; pre-declare all type-related functions and forms +(define-syntax-category type) + +;; type assignment utilities -------------------------------------------------- (begin-for-syntax ;; Type assignment macro for nicer syntax (define-syntax (⊢ stx) - (syntax-parse stx #:datum-literals (:) - [(_ e : τ) #'(assign-type #`e #`τ)] + (syntax-parse stx + [(_ e tag τ) #'(assign-type #`e #`τ #:tag 'tag)] [(_ e τ) #'(⊢ e : τ)])) (define-syntax (⊢/no-teval stx) - (syntax-parse stx #:datum-literals (:) - [(_ e : τ) #'(fast-assign-type #`e #`τ)] + (syntax-parse stx + [(_ e tag τ) #'(fast-assign-type #`e #`τ #:tag 'tag)] [(_ e τ) #'(⊢/no-teval e : τ)])) ;; Actual type assignment function. @@ -202,9 +411,9 @@ ;; - eval here so all types are stored in canonical form ;; - syntax-local-introduce fixes marks on types ;; which didnt get marked bc they were syntax properties - (define (fast-assign-type e τ #:tag [tag ':]) + #;(define (fast-assign-type e τ #:tag [tag ':]) (set-stx-prop/preserved e tag (syntax-local-introduce τ))) - (define (assign-type e τ #:tag [tag ':]) + #;(define (assign-type e τ #:tag [tag ':]) (fast-assign-type e ((current-type-eval) τ) #:tag tag)) (define (add-expected-type e τ) @@ -218,7 +427,7 @@ ;; typeof : Syntax -> Type or #f ;; Retrieves type of given stx, or #f if input has not been assigned a type. - (define (typeof stx #:tag [tag ':]) + #;(define (typeof stx #:tag [tag ':]) (get-stx-prop/car stx tag)) ;; get-stx-prop/car : Syntax Any -> Any @@ -323,9 +532,9 @@ ;; ctx = vars and their types (or other props, denoted with "sep") ;; tvctx = tyvars and their kinds (define (infer es #:ctx [ctx null] #:tvctx [tvctx null]) - (syntax-parse ctx #:datum-literals (:) - [([x : τ] ...) ; dont expand yet bc τ may have references to tvs - #:with ([tv (~seq sep:id tvk) ...] ...) tvctx + (syntax-parse ctx + [([x sep τ] ...) ; dont expand yet bc τ may have references to tvs + #:with ([tv (~seq tvsep:id tvk) ...] ...) tvctx #:with (e ...) es #:with ; old expander pattern (leave commented out) @@ -347,15 +556,18 @@ (let-syntax ([tv (make-rename-transformer (set-stx-prop/preserved (for/fold ([tv-id #'tv]) - ([s (in-list (list 'sep ...))] + ([s (in-list (list 'tvsep ...))] [k (in-list (list #'tvk ...))]) (assign-type tv-id k #:tag s)) 'tyvar #t))] ...) (λ (x ...) (let-syntax - ([x (make-variable-like-transformer (assign-type #'x #'τ))] ...) + ([x (make-variable-like-transformer (assign-type #'x #'τ #:tag 'sep))] ...) (#%expression e) ... void))))) - (list #'tvs+ #'xs+ #'(e+ ...) (stx-map typeof #'(e+ ...)))] + (list #'tvs+ #'xs+ + #'(e+ ...) + (stx-map (λ (t s) (typeof t #:tag (stx->datum s))) + #'(e+ ...) #'(sep ...)))] [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)])) ;; fns derived from infer --------------------------------------------------- @@ -543,7 +755,7 @@ (define-syntax define-basic-checked-id-stx (syntax-parser #:datum-literals (:) - [(_ τ:id : kind) + [(_ τ:id key tag) #:with τ? (mk-? #'τ) #:with τ-expander (mk-~ #'τ) #:with τ-internal (generate-temporary #'τ) @@ -564,22 +776,22 @@ #'(((~literal #%plain-app) (~literal τ-internal)) . rst)])))) (define τ-internal (λ () (raise (exn:fail:type:runtime - (format "~a: Cannot use ~a at run time" 'τ 'kind) + (format "~a: Cannot use ~a at run time" 'τ 'tag) (current-continuation-marks))))) (define-syntax τ (syntax-parser [:id (add-orig - (assign-type + (set-stx-prop/preserved (syntax/loc this-syntax (τ-internal)) - #'kind) + 'key (expand/df #'tag)) #'τ)])))])) ;; The def uses pattern vars "τ" and "kind" but this form is not restricted to ;; only types and kinds, eg, τ can be #'★ and kind can be #'#%kind (★'s type) (define-syntax (define-basic-checked-stx stx) (syntax-parse stx #:datum-literals (:) - [(_ τ:id : kind + [(_ τ:id key kind (~or (~optional (~and #:no-attach-kind (~parse no-attach-kind? #'#t))) (~optional @@ -647,7 +859,7 @@ ;; ie, "invalid type" instead of "improper tycon usage" #:with (~! (~var _ kind) (... ...)) #'(arg- (... ...)) (add-orig - (assign-type #'(τ- arg- (... ...)) #'#%kind) + (set-stx-prop/preserved #'(τ- arg- (... ...)) 'key (expand/df #'#%kind)) stx)] [_ ;; else fail with err msg (type-error @@ -661,8 +873,8 @@ ;; The def uses pattern vars "τ" and "kind" but this form is not restricted to ;; only types and kinds, eg, τ can be #'★ and kind can be #'#%kind (★'s type) (define-syntax (define-binding-checked-stx stx) - (syntax-parse stx #:datum-literals (:) - [(_ τ:id : kind + (syntax-parse stx + [(_ τ:id key kind (~or (~optional (~and #:no-attach-kind (~parse no-attach-kind? #'#t))) (~optional @@ -774,7 +986,7 @@ . args) #:with bvs+ks (if #,(attribute has-annotations?) #'bvs+ann - #'([bv : #%kind] (... ...))) + #'([bv :: #%kind] (... ...))) #:fail-unless (bvs-op (stx-length #'bvs+ks) bvs-n) (format "wrong number of type vars, expected ~a ~a" 'bvs-op 'bvs-n) @@ -786,12 +998,12 @@ ;; to ensure enough stx-parse progress so we get a proper err msg, ;; ie, "invalid type" instead of "improper tycon usage" #:with (~! (~var _ kind) (... ...)) #'τs- - #:with ([tv (~datum :) k_arg] (... ...)) #'bvs+ks + #:with ([tv (~datum ::) k_arg] (... ...)) #'bvs+ks #:with k_result (if #,(attribute has-annotations?) #'(kindcon k_arg (... ...)) #'#%kind) (add-orig - (assign-type #'(τ- bvs- . τs-) #'k_result) + (set-stx-prop/preserved #'(τ- bvs- . τs-) 'key (expand/df #'k_result)) stx)] ;; else fail with err msg [_ @@ -800,191 +1012,6 @@ "Improper usage of type constructor ~a: ~a, expected ~a ~a arguments") #'τ stx #'op #'n)])))))])) -; examples: -; (define-syntax-category type) -; (define-syntax-category kind) -(define-syntax (define-syntax-category stx) - (syntax-parse stx - [(_ name:id) - #:with names (format-id #'name "~as" #'name) - #:with #%tag (mk-#% #'name) - #:with #%tag? (mk-? #'#%tag) - #:with is-name? (mk-? #'name) - #:with any-name (format-id #'name "any-~a" #'name) - #:with any-name? (mk-? #'any-name) - #:with name-ctx (format-id #'name "~a-ctx" #'name) - #:with name-bind (format-id #'name "~a-bind" #'name) - #:with current-is-name? (mk-param #'is-name?) - #:with current-any-name? (mk-param #'any-name?) - #:with current-namecheck-relation (format-id #'name "current-~acheck-relation" #'name) - #:with namecheck? (format-id #'name "~acheck?" #'name) - #:with namechecks? (format-id #'name "~achecks?" #'name) - #:with current-name-eval (format-id #'name "current-~a-eval" #'name) - #:with default-name-eval (format-id #'name "default-~a-eval" #'name) - #:with name-evals (format-id #'name "~a-evals" #'name) - #:with mk-name (format-id #'name "mk-~a" #'name) - #:with define-base-name (format-id #'name "define-base-~a" #'name) - #:with define-base-names (format-id #'name "define-base-~as" #'name) - #:with define-name-cons (format-id #'name "define-~a-constructor" #'name) - #:with define-binding-name (format-id #'name "define-binding-~a" #'name) - #:with define-internal-name-cons (format-id #'name "define-internal-~a-constructor" #'name) - #:with define-internal-binding-name (format-id #'name "define-internal-binding-~a" #'name) - #:with name-ann (format-id #'name "~a-ann" #'name) - #:with name=? (format-id #'name "~a=?" #'name) - #:with names=? (format-id #'names "~a=?" #'names) - #:with current-name=? (mk-param #'name=?) - #:with same-names? (format-id #'name "same-~as?" #'name) - #:with name-out (format-id #'name "~a-out" #'name) - #'(begin - (define #%tag void) - (begin-for-syntax - (define (#%tag? t) (and (identifier? t) (free-identifier=? t #'#%tag))) - ;; is-name?, eg type?, corresponds to "well-formed" types - (define (is-name? t) (#%tag? (typeof t))) - (define current-is-name? (make-parameter is-name?)) - ;; any-name? corresponds to any type and defaults to is-name? - (define (any-name? t) (is-name? t)) - (define current-any-name? (make-parameter any-name?)) - (define (mk-name t) (assign-type t #'#%tag)) - (define-syntax-class name - #:attributes (norm) - (pattern τ - #:with norm ((current-type-eval) #'τ) - #:with k (typeof #'norm) - #:fail-unless ((current-is-name?) #'norm) - (format "~a (~a:~a) not a well-formed ~a: ~a" - (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ) - 'name (type->str #'τ)))) - (define-syntax-class any-name - #:attributes (norm) - (pattern τ - #:with norm ((current-type-eval) #'τ) - #:with k (typeof #'norm) - #:fail-unless ((current-any-name?) #'norm) - (format "~a (~a:~a) not a valid ~a: ~a" - (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ) - 'name (type->str #'τ)))) - (define-syntax-class name-bind #:datum-literals (:) - #:attributes (x name) - (pattern [x:id : ~! (~var ty name)] - #:attr name #'ty.norm) - (pattern any - #:fail-when #t - (format - (string-append - "Improperly formatted ~a annotation: ~a; should have shape [x : τ], " - "where τ is a valid ~a.") - 'name (type->str #'any) 'name) - #:attr x #f #:attr name #f)) - (define-syntax-class name-ctx - #:attributes ((x 1) (name 1)) - (pattern ((~var || name-bind) (... ...)))) - (define-syntax-class name-ann ; type instantiation - #:attributes (norm) - (pattern (~and (_) - (~fail #:unless (brace? this-syntax)) - ((~var t name) ~!)) - #:attr norm (delay #'t.norm)) - (pattern any - #:fail-when #t - (format - (string-append - "Improperly formatted ~a annotation: ~a; should have shape {τ}, " - "where τ is a valid ~a.") - 'name (type->str #'any) 'name) - #:attr norm #f)) - (define (name=? t1 t2) - ;(printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum t1)) - ;(printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum t2)) - (or (and (identifier? t1) (identifier? t2) (free-identifier=? t1 t2)) - (and (stx-null? t1) (stx-null? t2)) - (syntax-parse (list t1 t2) - [(((~literal #%plain-lambda) (~and (_:id (... ...)) xs) . ts1) - ((~literal #%plain-lambda) (~and (_:id (... ...)) ys) . ts2)) - (and (stx-length=? #'xs #'ys) - (stx-length=? #'ts1 #'ts2) - (stx-andmap - (λ (ty1 ty2) - ((current-name=?) (substs #'ys #'xs ty1) ty2)) - #'ts1 #'ts2))] - [_ (and (stx-pair? t1) (stx-pair? t2) - (names=? t1 t2))]))) - (define current-name=? (make-parameter name=?)) - (define (names=? τs1 τs2) - (and (stx-length=? τs1 τs2) - (stx-andmap (current-name=?) τs1 τs2))) - ; extra indirection, enables easily overriding type=? with sub? - ; to add subtyping, without changing any other definitions - (define current-namecheck-relation (make-parameter name=?)) - ;; convenience fns for current-typecheck-relation - (define (namecheck? t1 t2) - ((current-namecheck-relation) t1 t2)) - (define (namechecks? τs1 τs2) - (and (= (stx-length τs1) (stx-length τs2)) - (stx-andmap namecheck? τs1 τs2))) - (define (same-names? τs) - (define τs-lst (syntax->list τs)) - (or (null? τs-lst) - (andmap (λ (τ) ((current-name=?) (car τs-lst) τ)) (cdr τs-lst)))) - ;; type eval - ;; - default-type-eval == full expansion == canonical type representation - ;; - must expand because: - ;; - checks for unbound identifiers (ie, undefined types) - ;; - checks for valid types, ow can't distinguish types and terms - ;; - could parse types but separate parser leads to duplicate code - ;; - later, expanding enables reuse of same mechanisms for kind checking - ;; and type application - (define (default-name-eval τ) - ; TODO: optimization: don't expand if expanded - ; currently, this causes problems when - ; combining unexpanded and expanded types to create new types - (add-orig (expand/df τ) τ)) - (define current-name-eval (make-parameter default-name-eval)) - (define (name-evals τs) #`#,(stx-map (current-name-eval) τs))) - ;; helps with providing defined types - (define-syntax name-out - (make-provide-transformer - (lambda (stx modes) - (syntax-parse stx - ;; cannot write ty:type bc provides might precede type def - [(_ . ts) - #:with t-expanders (stx-map mk-~ #'ts) - #:with t?s (stx-map mk-? #'ts) - (expand-export - (syntax/loc stx (combine-out - (combine-out . ts) - (for-syntax (combine-out . t-expanders) . t?s))) - modes)])))) - (define-syntax define-base-name - (syntax-parser - [(_ (~var x id) (~datum :) k) - #'(define-basic-checked-id-stx x : k)] - [(_ (~var x id)) - #'(define-basic-checked-id-stx x : #%tag)])) - (define-syntax define-base-names - (syntax-parser - [(_ (~var x id) (... ...)) - #'(begin (define-base-name x) (... ...))])) - (define-syntax define-internal-name-cons - (syntax-parser - [(_ (~var x id) . rst) - #'(define-basic-checked-stx x : name #:no-attach-kind . rst)])) - (define-syntax define-internal-binding-name - (syntax-parser - [(_ (~var x id) . rst) - #'(define-binding-checked-stx x : name #:no-attach-kind . rst)])) - (define-syntax define-name-cons - (syntax-parser - [(_ (~var x id) . rst) - #'(define-basic-checked-stx x : name . rst)])) - (define-syntax define-binding-name - (syntax-parser - [(_ (~var x id) . rst) - #'(define-binding-checked-stx x : name . rst)])))])) - -;; pre-declare all type-related functions and forms -(define-syntax-category type) - (define-syntax typed-out (make-provide-pre-transformer (lambda (stx modes) diff --git a/turnstile/examples/exist.rkt b/turnstile/examples/exist.rkt index 17e9d58..203b0e4 100644 --- a/turnstile/examples/exist.rkt +++ b/turnstile/examples/exist.rkt @@ -66,6 +66,6 @@ ;; [⊢ e_packed ≫ e_packed- ⇒ (~∃ (Y) τ_body)] #:with τ_x (subst #'X #'Y #'τ_body) - [([X ≫ X- : #%type]) ([x ≫ x- : τ_x]) ⊢ e ≫ e- ⇒ τ_e] + [([X ≫ X- :: #%type]) ([x ≫ x- : τ_x]) ⊢ e ≫ e- ⇒ τ_e] -------- [⊢ (let- ([x- e_packed-]) e-) ⇒ τ_e]) diff --git a/turnstile/examples/fsub.rkt b/turnstile/examples/fsub.rkt index fa55a35..5345700 100644 --- a/turnstile/examples/fsub.rkt +++ b/turnstile/examples/fsub.rkt @@ -79,7 +79,7 @@ ;; environment with a syntax property using another tag: '<: ;; The "expose" function looks for this tag to enforce the bound, ;; as in TaPL (fig 28-1) - [([tv ≫ tv- : #%type <: τsub] ...) () ⊢ e ≫ e- ⇒ τ_e] + [([tv ≫ tv- :: #%type <: τsub] ...) () ⊢ e ≫ e- ⇒ τ_e] -------- [⊢ e- ⇒ (∀ ([tv- <: τsub] ...) τ_e)]) (define-typed-syntax (inst e τ:type ...) ≫ diff --git a/turnstile/examples/infer.rkt b/turnstile/examples/infer.rkt index 3e3f444..8335540 100644 --- a/turnstile/examples/infer.rkt +++ b/turnstile/examples/infer.rkt @@ -159,7 +159,7 @@ #:with [X ...] (for/list ([X (in-list (generate-temporaries #'[x ...]))]) (add-orig X X)) - [([X ≫ X- : #%type] ...) ([x ≫ x- : X] ...) + [([X ≫ X- :: #%type] ...) ([x ≫ x- : X] ...) ⊢ [body ≫ body- ⇒ : τ_body*]] #:with (~?Some [V ...] τ_body (~Cs [id_2 τ_2] ...)) (syntax-local-introduce #'τ_body*) #:with τ_fn (some/inst/generalize #'[X- ... V ...] diff --git a/turnstile/examples/mlish+adhoc.rkt b/turnstile/examples/mlish+adhoc.rkt index bf3bd98..1057cb6 100644 --- a/turnstile/examples/mlish+adhoc.rkt +++ b/turnstile/examples/mlish+adhoc.rkt @@ -1711,9 +1711,9 @@ (~=> TCsub ... (~TC [generic-op-expected ty-concrete-op-expected] ...))) _) - (infers/tyctx+erase #'([X : #%type] ...) #'(TC ... (Name ty ...))) + (infers/tyctx+erase #'([X :: #%type] ...) #'(TC ... (Name ty ...))) ;; this produces #%app bad stx err, so manually call infer for now - ;; [([X ≫ X- : #%type] ...) () ⊢ (TC ... (Name ty ...)) ≫ + ;; [([X ≫ X- :: #%type] ...) () ⊢ (TC ... (Name ty ...)) ≫ ;; (TC+ ... ;; (~=> TCsub ... ;; (~TC [generic-op-expected ty-concrete-op-expected] ...))) diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt index 2575f13..7f6b3a3 100644 --- a/turnstile/examples/mlish.rkt +++ b/turnstile/examples/mlish.rkt @@ -851,22 +851,22 @@ #:fail-unless (stx-length=? #'[x ...] #'[τ_in ...]) (format "expected a function of ~a arguments, got one with ~a arguments" (stx-length #'[τ_in ...]) (stx-length #'[x ...])) - [([X ≫ X- : #%type] ...) ([x ≫ x- : τ_in] ...) ⊢ [body ≫ body- ⇐ τ_out]] + [([X ≫ X- :: #%type] ...) ([x ≫ x- : τ_in] ...) ⊢ [body ≫ body- ⇐ τ_out]] -------- [⊢ (λ- (x- ...) body-)]] [(λ ([x : τ_x] ...) body) ⇐ (~?∀ (V ...) (~ext-stlc:→ τ_in ... τ_out)) ≫ #:with [X ...] (compute-tyvars #'(τ_x ...)) - [([X ≫ X- : #%type] ...) () ⊢ [τ_x ≫ τ_x- ⇐ #%type] ...] + [([X ≫ X- :: #%type] ...) () ⊢ [τ_x ≫ τ_x- ⇐ #%type] ...] [τ_in τ⊑ τ_x- #:for x] ... ;; TODO is there a way to have λs that refer to ids defined after them? - [([V ≫ V- : #%type] ... [X- ≫ X-- : #%type] ...) ([x ≫ x- : τ_x-] ...) + [([V ≫ V- :: #%type] ... [X- ≫ X-- : #%type] ...) ([x ≫ x- : τ_x-] ...) ⊢ body ≫ body- ⇐ τ_out] -------- [⊢ (λ- (x- ...) body-)]] [(λ ([x : τ_x] ...) body) ≫ #:with [X ...] (compute-tyvars #'(τ_x ...)) ;; TODO is there a way to have λs that refer to ids defined after them? - [([X ≫ X- : #%type] ...) ([x ≫ x- : τ_x] ...) ⊢ body ≫ body- ⇒ τ_body] + [([X ≫ X- :: #%type] ...) ([x ≫ x- : τ_x] ...) ⊢ body ≫ body- ⇒ τ_body] #:with [τ_x* ...] (inst-types/cs #'[X ...] #'([X X-] ...) #'[τ_x ...]) #:with τ_fn (add-orig #'(?∀ (X- ...) (ext-stlc:→ τ_x* ... τ_body)) #`(→ #,@(stx-map get-orig #'[τ_x* ...]) #,(get-orig #'τ_body))) diff --git a/turnstile/examples/sysf.rkt b/turnstile/examples/sysf.rkt index 4f2ff00..dde2c79 100644 --- a/turnstile/examples/sysf.rkt +++ b/turnstile/examples/sysf.rkt @@ -14,7 +14,7 @@ (define-binding-type ∀) (define-typed-syntax (Λ (tv:id ...) e) ≫ - [([tv ≫ tv- : #%type] ...) () ⊢ e ≫ e- ⇒ τ] + [([tv ≫ tv- :: #%type] ...) () ⊢ e ≫ e- ⇒ τ] -------- [⊢ e- ⇒ (∀ (tv- ...) τ)]) diff --git a/turnstile/examples/tests/ext-stlc-tests.rkt b/turnstile/examples/tests/ext-stlc-tests.rkt index 881819e..8cdcd71 100644 --- a/turnstile/examples/tests/ext-stlc-tests.rkt +++ b/turnstile/examples/tests/ext-stlc-tests.rkt @@ -52,8 +52,8 @@ (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 "ann: type mismatch: expected Int, given #%type\n *expression: Int") +(typecheck-fail (ann Bool : Int) + #:with-msg "ann: type mismatch: expected Int, given #f\n *expression: Bool") ; let (check-type (let () (+ 1 1)) : Int ⇒ 2) diff --git a/turnstile/examples/tests/rackunit-typechecking.rkt b/turnstile/examples/tests/rackunit-typechecking.rkt index 7fc621a..388d27c 100644 --- a/turnstile/examples/tests/rackunit-typechecking.rkt +++ b/turnstile/examples/tests/rackunit-typechecking.rkt @@ -19,19 +19,19 @@ (string-join (map add-escs (string-split givens ", ")) ".*")))) (define-syntax (check-type stx) - (syntax-parse stx #:datum-literals (: ⇒ ->) + (syntax-parse stx #:datum-literals (⇒ ->) ;; duplicate code to avoid redundant expansions - [(_ e : τ-expected (~or ⇒ ->) v) + [(_ e tag:id τ-expected (~or ⇒ ->) v) #:with e+ (expand/df #'(add-expected e τ-expected)) - #:with τ (typeof #'e+) + #:with τ (typeof #'e+ #:tag (stx->datum #'tag)) #:fail-unless (typecheck? #'τ ((current-type-eval) #'τ-expected)) (format "Expression ~a [loc ~a:~a] has type ~a, expected ~a" (syntax->datum #'e) (syntax-line #'e) (syntax-column #'e) (type->str #'τ) (type->str #'τ-expected)) (syntax/loc stx (check-equal? e+ (add-expected v τ-expected)))] - [(_ e : τ-expected) - #:with τ (typeof (expand/df #'(add-expected e τ-expected))) + [(_ e tag:id τ-expected) + #:with τ (typeof (expand/df #'(add-expected e τ-expected)) #:tag (stx->datum #'tag)) #:fail-unless (typecheck? #'τ ((current-type-eval) #'τ-expected)) (format diff --git a/turnstile/examples/trivial.rkt b/turnstile/examples/trivial.rkt index bf49307..f8d86c8 100644 --- a/turnstile/examples/trivial.rkt +++ b/turnstile/examples/trivial.rkt @@ -282,7 +282,7 @@ [x:id : ty])) ...) . es) ≫ #:with (X ...) (generate-temporaries #'(x ...)) - [([X ≫ X- : #%type] ...) ([x ≫ x- : X] ...) + [([X ≫ X- :: #%type] ...) ([x ≫ x- : X] ...) ⊢ (begin . es) ≫ e- ⇒ τ_out] ;; TODO: investigate why this extra syntax-local-introduce is needed? #:with τ_out* (syntax-local-introduce #'τ_out)