STUCK: infer must know about sep
This commit is contained in:
Stephen Chang
parent
f8cb9959cd
commit
e9cc782aeb
|
|
@ -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)])
|
||||
|
|
|
|||
|
|
@ -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)])
|
||||
|
|
|
|||
|
|
@ -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 ...)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 ...)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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])
|
||||
|
|
|
|||
|
|
@ -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 ...) ≫
|
||||
|
|
|
|||
|
|
@ -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 ...]
|
||||
|
|
|
|||
|
|
@ -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] ...)))
|
||||
|
|
|
|||
|
|
@ -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)))
|
||||
|
|
|
|||
|
|
@ -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- ...) τ)])
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user