fomega working with define-syntax-category
This commit is contained in:
Stephen Chang
parent
efaef8b60e
commit
d9e1c2febb
|
|
@ -22,10 +22,17 @@
|
|||
|
||||
(define-syntax-category kind)
|
||||
(begin-for-syntax
|
||||
(current-type? (λ (t) (or (type? t) (kind? (typeof t))))))
|
||||
(current-kind? (λ (k) (or (#%type? k) (kind? k))))
|
||||
;; Try to keep "type?" remain backward compatible with its uses so far,
|
||||
;; eg in the definition of λ or previous type constuctors.
|
||||
;; (However, this is not completely possible, eg define-type-alias)
|
||||
;; So now "type?" no longer validates types, rather it's a subset.
|
||||
;; But we no longer need type? to validate types, instead we can use (kind? (typeof t))
|
||||
(current-type? (λ (t) (or (type? t) (★? (typeof t)) (∀★? (typeof t)) #;(kind? (typeof t))))))
|
||||
|
||||
#;(provide define-type-alias)
|
||||
#;(define-syntax define-type-alias
|
||||
; must override
|
||||
(provide define-type-alias)
|
||||
(define-syntax define-type-alias
|
||||
(syntax-parser
|
||||
[(_ alias:id τ)
|
||||
#:with (τ- k_τ) (infer+erase #'τ)
|
||||
|
|
@ -33,18 +40,6 @@
|
|||
#'(define-syntax alias (syntax-parser [x:id #'τ-]))]))
|
||||
|
||||
(begin-for-syntax
|
||||
(define (type=? t1 t2)
|
||||
(printf "t1 = ~a\n" (syntax->datum t1))
|
||||
(printf "t2 = ~a\n" (syntax->datum t2))
|
||||
(and (syntax-parse (list t1 t2) #:datum-literals (:)
|
||||
[((~∀ ([tv1 : k1] ...) tbody1)
|
||||
(~∀ ([tv2 : k2] ...) tbody2))
|
||||
#:when (displayln "here")
|
||||
(types=? #'(k1 ...) #'(k2 ...))]
|
||||
[_ #t])
|
||||
(sysf:type=? t1 t2)))
|
||||
(current-type=? type=?)
|
||||
(current-typecheck-relation (current-type=?))
|
||||
;; extend type-eval to handle tyapp
|
||||
;; - requires manually handling all other forms
|
||||
(define (type-eval τ)
|
||||
|
|
@ -72,6 +67,7 @@
|
|||
|
||||
(define-base-kind ★)
|
||||
(define-kind-constructor ⇒ #:arity >= 1)
|
||||
(define-kind-constructor ∀★ #:arity >= 0)
|
||||
|
||||
;; for now, handle kind checking in the types themselves
|
||||
;; TODO: move kind checking to a common place (like #%app)?
|
||||
|
|
@ -102,28 +98,29 @@
|
|||
#:with (tvs- τ_body- k_body) (infer/ctx+erase #'(b ...) #'τ_body)
|
||||
#:when (★? #'k_body)
|
||||
(⊢ (λ tvs- b.tag ... τ_body-) : ★)]))
|
||||
|
||||
(define-syntax (∀ stx)
|
||||
(syntax-parse stx
|
||||
[(_ bvs:kind-ctx τ_body)
|
||||
; #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body)
|
||||
; #:when (★? #'k_body)
|
||||
#:when (displayln ((current-type-eval) #'(sysf:∀ (bvs.x ...) τ_body)))
|
||||
(⊢ #,((current-type-eval) #'(sysf:∀ (bvs.x ...) τ_body)) : (⇒ bvs.kind ...))]))
|
||||
;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type
|
||||
#:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
|
||||
; expand so kind gets overwritten
|
||||
(⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))]))
|
||||
; (⊢ (λ tvs- b.tag ... τ_body-) : ★)]))
|
||||
(begin-for-syntax
|
||||
(define-syntax ~∀
|
||||
(pattern-expander
|
||||
(syntax-parser #:datum-literals (:)
|
||||
[(_ ([tv:id : k] ...) τ)
|
||||
#:when (displayln "pat expand")
|
||||
#:with ∀τ (generate-temporary)
|
||||
#'(~and ∀τ
|
||||
(~parse (~sysf:∀ (tv ...) τ) #'∀τ)
|
||||
(~parse (~⇒ k ...) (typeof #'∀τ)))]
|
||||
(~parse (~∀★ k ...) (typeof #'∀τ)))]
|
||||
[(_ . args)
|
||||
#:with ∀τ (generate-temporary)
|
||||
#'(~and ∀τ
|
||||
(~parse (~sysf:∀ (tv (... ...)) τ) #'∀τ)
|
||||
(~parse (~⇒ k (... ...)) (typeof #'∀τ))
|
||||
(~parse (~∀★ k (... ...)) (typeof #'∀τ))
|
||||
(~parse args #'(([tv k] (... ...)) τ)))])))
|
||||
(define-syntax ~∀*
|
||||
(pattern-expander
|
||||
|
|
@ -134,7 +131,20 @@
|
|||
(~and any (~do
|
||||
(type-error
|
||||
#:src #'any
|
||||
#:msg "Expected ∀ type, got: ~a" #'any))))]))))
|
||||
#:msg "Expected ∀ type, got: ~a" #'any))))])))
|
||||
(define (type=? t1 t2)
|
||||
;(printf "t1 = ~a\n" (syntax->datum t1))
|
||||
;(printf "t2 = ~a\n" (syntax->datum t2))
|
||||
(or (and (★? t1) (#%type? t2))
|
||||
(and (#%type? t1) (★? t2))
|
||||
(and (syntax-parse (list t1 t2) #:datum-literals (:)
|
||||
[((~∀ ([tv1 : k1]) tbody1)
|
||||
(~∀ ([tv2 : k2]) tbody2))
|
||||
(type=? #'k1 #'k2)]
|
||||
[_ #t])
|
||||
(sysf:type=? t1 t2))))
|
||||
(current-type=? type=?)
|
||||
(current-typecheck-relation (current-type=?)))
|
||||
|
||||
#;(define-syntax (Λ stx)
|
||||
(syntax-parse stx
|
||||
|
|
@ -144,7 +154,7 @@
|
|||
(define-syntax (Λ stx)
|
||||
(syntax-parse stx
|
||||
[(_ bvs:kind-ctx e)
|
||||
#:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e)
|
||||
#:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
|
||||
(⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]))
|
||||
#;(define-syntax (inst stx)
|
||||
(syntax-parse stx
|
||||
|
|
@ -162,10 +172,13 @@
|
|||
(⊢ e- : #,(substs #'(τ ...) #'(tv ...) #'τ_body))]))
|
||||
(define-syntax (inst stx)
|
||||
(syntax-parse stx
|
||||
[(_ e τ:type ...)
|
||||
[(_ e τ ...)
|
||||
#:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
|
||||
#:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:expand (current-type-eval))
|
||||
#:when (typechecks? (stx-map typeof #'(k_τ ...)) #'(k ...))
|
||||
#:when (stx-andmap (λ (t k) (or ((current-kind?) k)
|
||||
(type-error #:src t #:msg "not a valid type: ~a" t)))
|
||||
#'(τ ...) #'(k_τ ...))
|
||||
#:when (typechecks? #'(k_τ ...) #'(k ...))
|
||||
(⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))]))
|
||||
|
||||
;; TODO: merge with regular λ and app?
|
||||
|
|
@ -173,6 +186,7 @@
|
|||
(syntax-parse stx
|
||||
[(_ bvs:kind-ctx τ_body)
|
||||
#:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
|
||||
#:when ((current-kind?) #'k_body)
|
||||
(⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))]))
|
||||
#;(define-syntax (tyλ stx)
|
||||
(syntax-parse stx
|
||||
|
|
|
|||
|
|
@ -1,204 +1,205 @@
|
|||
#lang s-exp "../fomega.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
;(check-type Int : ★)
|
||||
(check-type Int : #%type)
|
||||
;(check-type String : ★)
|
||||
(check-type String : #%type)
|
||||
(check-type Int : ★)
|
||||
(check-type String : ★)
|
||||
(typecheck-fail →)
|
||||
;(check-type (→ Int Int) : ★)
|
||||
(check-type (→ Int Int) : #%type)
|
||||
(check-type (→ Int Int) : ★)
|
||||
(typecheck-fail (→ →))
|
||||
(typecheck-fail (→ 1))
|
||||
(check-type 1 : Int)
|
||||
|
||||
;(check-type (∀ ([t : ★]) (→ t t)) : ★)
|
||||
(check-type (∀ ([t : ★]) (→ t t)) : (⇒ ★))
|
||||
;(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
|
||||
(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : #%type)
|
||||
(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
|
||||
(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
|
||||
|
||||
(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
|
||||
|
||||
(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
|
||||
: (∀ ([X : ★]) (→ X X)))
|
||||
((λ ([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 (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)
|
||||
; : (⇒ ★ ★))
|
||||
(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"))
|
||||
|
||||
;; 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 "not a valid type: 1")
|
||||
;
|
||||
;;; applied f too early
|
||||
;(typecheck-fail (inst
|
||||
; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
|
||||
; (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)))
|
||||
;(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, p451
|
||||
;(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
|
||||
;
|
||||
(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 "not a valid type: 1")
|
||||
|
||||
(typecheck-fail
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
|
||||
#:with-msg "Expected expression f to have → type")
|
||||
;; 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 expression f to have → type")
|
||||
(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, p451
|
||||
(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
|
||||
|
||||
;(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)))
|
||||
(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))
|
||||
(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)))
|
||||
(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))
|
||||
(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)
|
||||
(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)))
|
||||
;
|
||||
;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
|
||||
;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
|
||||
;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
|
||||
;
|
||||
;(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
|
||||
; : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
|
||||
;
|
||||
;(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
|
||||
; : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
|
||||
;
|
||||
;(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
|
||||
; : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
|
||||
;
|
||||
;(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
|
||||
;(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
|
||||
;; first inst should be discarded
|
||||
;(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
|
||||
;; second inst is discarded
|
||||
;(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
|
||||
;
|
||||
;;; polymorphic arguments
|
||||
;(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
|
||||
;(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
|
||||
;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
|
||||
;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
|
||||
;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
|
||||
;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
|
||||
;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
|
||||
;(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
|
||||
;(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
|
||||
;(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
|
||||
;(check-type
|
||||
; (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
|
||||
;(check-type
|
||||
; ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
|
||||
; : Int ⇒ 10)
|
||||
;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
|
||||
;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
|
||||
;(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
|
||||
; (Λ ([s : ★]) (λ ([y : s]) y)))
|
||||
; : Int ⇒ 10)
|
||||
;
|
||||
;
|
||||
;;; previous tests -------------------------------------------------------------
|
||||
;(check-type 1 : Int)
|
||||
;(check-not-type 1 : (→ Int Int))
|
||||
(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)))
|
||||
|
||||
(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
|
||||
(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
|
||||
(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
|
||||
|
||||
(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
|
||||
: (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
|
||||
|
||||
(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
|
||||
: (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
|
||||
|
||||
(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
|
||||
: (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
|
||||
|
||||
(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
|
||||
(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
|
||||
; first inst should be discarded
|
||||
(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
|
||||
; second inst is discarded
|
||||
(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
|
||||
|
||||
;; polymorphic arguments
|
||||
(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
|
||||
(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
|
||||
(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
|
||||
(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
|
||||
(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
|
||||
(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
|
||||
(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
|
||||
(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
|
||||
(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
|
||||
(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
|
||||
(check-type
|
||||
(inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
|
||||
(check-type
|
||||
((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
|
||||
: Int ⇒ 10)
|
||||
(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
|
||||
(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
|
||||
(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
|
||||
(Λ ([s : ★]) (λ ([y : s]) y)))
|
||||
: Int ⇒ 10)
|
||||
|
||||
|
||||
;; previous tests -------------------------------------------------------------
|
||||
(check-type 1 : Int)
|
||||
(check-not-type 1 : (→ Int Int))
|
||||
;(typecheck-fail #f) ; unsupported literal
|
||||
;(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
|
||||
;(check-not-type (λ ([x : Int]) x) : Int)
|
||||
;(check-type (λ ([x : Int]) x) : (→ Int Int))
|
||||
;(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
|
||||
;(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
|
||||
;(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
|
||||
;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
|
||||
;(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
|
||||
;(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
|
||||
; : (→ (→ Int Int Int) Int Int Int))
|
||||
;(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
|
||||
;(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
|
||||
;(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
|
||||
;(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
|
||||
;(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
|
||||
(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)
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@
|
|||
(for-syntax (all-defined-out)) (all-defined-out)
|
||||
(for-syntax
|
||||
(all-from-out racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt"))
|
||||
(for-meta 2 (all-from-out racket/base syntax/parse)))
|
||||
(for-meta 2 (all-from-out racket/base syntax/parse racket/syntax)))
|
||||
|
||||
;; type checking functions/forms
|
||||
|
||||
|
|
@ -122,12 +122,12 @@
|
|||
#'(τ_e (... ...)))
|
||||
#'res])]))
|
||||
;; infers the type and erases types in an expression
|
||||
(define (infer+erase e)
|
||||
(define e+ (expand/df e))
|
||||
(define (infer+erase e #:expand [expand-fn expand/df])
|
||||
(define e+ (expand-fn e))
|
||||
(list e+ (typeof e+)))
|
||||
;; infers the types and erases types in multiple expressions
|
||||
(define (infers+erase es)
|
||||
(stx-map infer+erase es))
|
||||
(define (infers+erase es #:expand [expand-fn expand/df])
|
||||
(stx-map (λ (e) (infer+erase e #:expand expand-fn)) es))
|
||||
|
||||
;; This is the main "infer" function. All others are defined in terms of this.
|
||||
;; It should be named infer+erase but leaving it for now for backward compat.
|
||||
|
|
@ -137,7 +137,7 @@
|
|||
;; the types before typechecking, which is acceptable
|
||||
(define (infer es #:ctx [ctx null] #:tvctx [tvctx null]
|
||||
#:octx [octx tvctx] #:tag [tag 'unused]
|
||||
#:expand [expand expand/df])
|
||||
#:expand [expand-fn expand/df])
|
||||
(syntax-parse ctx #:datum-literals (:)
|
||||
[([x : τ] ...) ; dont expand yet bc τ may have references to tvs
|
||||
#:with ([tv : k] ...) tvctx
|
||||
|
|
@ -158,16 +158,18 @@
|
|||
((~literal #%plain-lambda) xs+
|
||||
((~literal let-values) () ((~literal let-values) ()
|
||||
((~literal #%expression) e+) ... (~literal void))))))))
|
||||
(expand
|
||||
(expand-fn
|
||||
#`(λ (tv ...)
|
||||
(let-syntax ([tv (make-rename-transformer (assign-type (assign-type #'tv #'k) #'ok #:tag '#,tag))] ...)
|
||||
(λ (x ...)
|
||||
(let-syntax ([x (make-rename-transformer (assign-type #'x #'τ))] ...)
|
||||
(#%expression e) ... void)))))
|
||||
;#:when (stx-map displayln #'(e+ ...))
|
||||
; #:when (displayln (stx-map typeof #'(e+ ...)))
|
||||
; #:when (stx-map displayln #'(e+ ...))
|
||||
; #:when (displayln (stx-map typeof #'(e+ ...)))
|
||||
(list #'tvs+ #'xs+ #'(e+ ...)
|
||||
(stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
|
||||
(stx-map ; check is when trying to combine #%type and kinds
|
||||
(λ (t) (or (false? t) (syntax-local-introduce t)))
|
||||
(stx-map typeof #'(e+ ...))))]
|
||||
[([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)]))
|
||||
|
||||
;; fns derived from infer ---------------------------------------------------
|
||||
|
|
@ -176,11 +178,11 @@
|
|||
;; shorter names
|
||||
; ctx = type env for bound vars in term e, etc
|
||||
; can also use for bound tyvars in type e
|
||||
(define (infer/ctx+erase ctx e)
|
||||
(syntax-parse (infer (list e) #:ctx ctx)
|
||||
(define (infer/ctx+erase ctx e #:expand [expand-fn expand/df])
|
||||
(syntax-parse (infer (list e) #:ctx ctx #:expand expand-fn)
|
||||
[(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
|
||||
(define (infers/ctx+erase ctx es #:expand [expand expand/df])
|
||||
(stx-cdr (infer es #:ctx ctx #:expand expand)))
|
||||
(define (infers/ctx+erase ctx es #:expand [expand-fn expand/df])
|
||||
(stx-cdr (infer es #:ctx ctx #:expand expand-fn)))
|
||||
; tyctx = kind env for bound type vars in term e
|
||||
(define (infer/tyctx+erase ctx e)
|
||||
(syntax-parse (infer (list e) #:tvctx ctx)
|
||||
|
|
@ -313,54 +315,54 @@
|
|||
#;(define #%type void)
|
||||
#;(define-for-syntax (mk-type t) (assign-type t #'#%type))
|
||||
|
||||
#;(define-syntax (define-base-type stx)
|
||||
(syntax-parse stx
|
||||
[(_ τ:id)
|
||||
#:with τ? (format-id #'τ "~a?" #'τ)
|
||||
#:with τ-internal (generate-temporary #'τ)
|
||||
#:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
|
||||
#:with τ-cls (generate-temporary #'τ)
|
||||
#:with τ-expander (format-id #'τ "~~~a" #'τ)
|
||||
#'(begin
|
||||
(provide τ (for-syntax τ? inferτ+erase τ-expander))
|
||||
(define τ-internal
|
||||
(λ () (raise (exn:fail:type:runtime
|
||||
(format "~a: Cannot use type at run time" 'τ)
|
||||
(current-continuation-marks)))))
|
||||
(define-syntax (τ stx)
|
||||
(syntax-parse stx
|
||||
[x:id (add-orig #'(#%type (τ-internal)) #'τ)]))
|
||||
(begin-for-syntax
|
||||
; expanded form of τ
|
||||
(define-syntax-class τ-cls
|
||||
(pattern ((~literal #%plain-type) ((~literal #%plain-app) ty))))
|
||||
(define (τ? t)
|
||||
(syntax-parse ((current-type-eval) t)
|
||||
[expanded-type
|
||||
#:declare expanded-type τ-cls
|
||||
(typecheck? #'expanded-type.ty #'τ-internal)]))
|
||||
; base type pattern expanders should be identifier macros but
|
||||
; parsing them is ambiguous, so handle and pass through other args
|
||||
(define-syntax τ-expander
|
||||
(pattern-expander
|
||||
(syntax-parser
|
||||
[ty:id #'((~literal #%plain-type)
|
||||
((~literal #%plain-app)
|
||||
(~literal τ-internal)))]
|
||||
[(_ . rst)
|
||||
#'(((~literal #%plain-type)
|
||||
((~literal #%plain-app)
|
||||
(~literal τ-internal))) . rst)])))
|
||||
(define (inferτ+erase e)
|
||||
(syntax-parse (infer+erase e) #:context e
|
||||
[(e- expanded-type)
|
||||
#:declare expanded-type τ-cls
|
||||
#:fail-unless (typecheck? #'expanded-type.ty #'τ-internal)
|
||||
(format
|
||||
"~a (~a:~a): Expected type of expression ~v to be ~a, got: ~a"
|
||||
(syntax-source e) (syntax-line e) (syntax-column e)
|
||||
(syntax->datum e) (type->str #'τ) (type->str #'expanded-type))
|
||||
#'e-]))))]))
|
||||
;#;(define-syntax (define-base-type stx)
|
||||
; (syntax-parse stx
|
||||
; [(_ τ:id)
|
||||
; #:with τ? (format-id #'τ "~a?" #'τ)
|
||||
; #:with τ-internal (generate-temporary #'τ)
|
||||
; #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
|
||||
; #:with τ-cls (generate-temporary #'τ)
|
||||
; #:with τ-expander (format-id #'τ "~~~a" #'τ)
|
||||
; #'(begin
|
||||
; (provide τ (for-syntax τ? inferτ+erase τ-expander))
|
||||
; (define τ-internal
|
||||
; (λ () (raise (exn:fail:type:runtime
|
||||
; (format "~a: Cannot use type at run time" 'τ)
|
||||
; (current-continuation-marks)))))
|
||||
; (define-syntax (τ stx)
|
||||
; (syntax-parse stx
|
||||
; [x:id (add-orig #'(#%type (τ-internal)) #'τ)]))
|
||||
; (begin-for-syntax
|
||||
; ; expanded form of τ
|
||||
; (define-syntax-class τ-cls
|
||||
; (pattern ((~literal #%plain-type) ((~literal #%plain-app) ty))))
|
||||
; (define (τ? t)
|
||||
; (syntax-parse ((current-type-eval) t)
|
||||
; [expanded-type
|
||||
; #:declare expanded-type τ-cls
|
||||
; (typecheck? #'expanded-type.ty #'τ-internal)]))
|
||||
; ; base type pattern expanders should be identifier macros but
|
||||
; ; parsing them is ambiguous, so handle and pass through other args
|
||||
; (define-syntax τ-expander
|
||||
; (pattern-expander
|
||||
; (syntax-parser
|
||||
; [ty:id #'((~literal #%plain-type)
|
||||
; ((~literal #%plain-app)
|
||||
; (~literal τ-internal)))]
|
||||
; [(_ . rst)
|
||||
; #'(((~literal #%plain-type)
|
||||
; ((~literal #%plain-app)
|
||||
; (~literal τ-internal))) . rst)])))
|
||||
; (define (inferτ+erase e)
|
||||
; (syntax-parse (infer+erase e) #:context e
|
||||
; [(e- expanded-type)
|
||||
; #:declare expanded-type τ-cls
|
||||
; #:fail-unless (typecheck? #'expanded-type.ty #'τ-internal)
|
||||
; (format
|
||||
; "~a (~a:~a): Expected type of expression ~v to be ~a, got: ~a"
|
||||
; (syntax-source e) (syntax-line e) (syntax-column e)
|
||||
; (syntax->datum e) (type->str #'τ) (type->str #'expanded-type))
|
||||
; #'e-]))))]))
|
||||
|
||||
(define-syntax define-basic-checked-id-stx
|
||||
(syntax-parser #:datum-literals (:)
|
||||
|
|
@ -373,7 +375,7 @@
|
|||
#'(begin
|
||||
(provide τ (for-syntax τ? τ-expander))
|
||||
(begin-for-syntax
|
||||
(define (τ? t) (typecheck? t #'τ-internal))
|
||||
(define (τ? t) (and (identifier? t) (free-identifier=? t #'τ-internal)))
|
||||
(define (inferτ+erase e)
|
||||
(syntax-parse (infer+erase e) #:context e
|
||||
[(e- e_τ)
|
||||
|
|
@ -430,10 +432,9 @@
|
|||
#,(if (attribute has-bvs?)
|
||||
#'(~parse pat #'(bvs rst))
|
||||
#'(~parse pat #'rst)))]
|
||||
[(_ (~optional (~and (~fail #:unless #,(attribute has-bvs?))
|
||||
(bv (... ...)))
|
||||
#:defaults ([(bv 1) null])) . pat)
|
||||
#'((~literal #%plain-lambda) (bv (... ...))
|
||||
[(_ (~optional (~and (~fail #:unless #,(attribute has-bvs?)) bvs-pat)
|
||||
#:defaults ([bvs-pat #'()])) . pat)
|
||||
#'((~literal #%plain-lambda) bvs-pat
|
||||
((~literal #%plain-app) (~literal τ-internal) . pat))])))
|
||||
(define-syntax τ-expander*
|
||||
(pattern-expander
|
||||
|
|
@ -453,7 +454,8 @@
|
|||
(and (stx-pair? t)
|
||||
(syntax-parse t
|
||||
[((~literal #%plain-lambda) bvs ((~literal #%plain-app) tycon . _))
|
||||
(typecheck? #'tycon #'τ-internal)]))))
|
||||
(typecheck? #'tycon #'τ-internal)]
|
||||
[_ #f]))))
|
||||
; #;(define (τ-get t)
|
||||
; (syntax-parse t
|
||||
; [(τ-expander . pat) #'pat]))
|
||||
|
|
@ -918,7 +920,7 @@
|
|||
#%tag define-base-name define-name-cons)
|
||||
(define #%tag void)
|
||||
(begin-for-syntax
|
||||
(define (#%tag? t) (typecheck? t #'#%tag))
|
||||
(define (#%tag? t) (and (identifier? t) (free-identifier=? t #'#%tag)))
|
||||
(define (is-name? t) (#%tag? (typeof t)))
|
||||
(define current-is-name? (make-parameter is-name?))
|
||||
(define (mk-name t) (assign-type t #'#%tag))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user