split def-kinded-stx from def-typed-stx; split any-type? from type?
- the former prevents using current-typecheck-relation at type/kind level - the latter differentiates "well-formed" types (star) from valid types (any kind) - move define-*ed-syntax and *-eval into define-syntax-category - turnstile must wrap define-stx-category to define new define-*ed-syntax - add any-*? pred and any-* stx class in def-stx-category - fixes #44 - fixes #45
This commit is contained in:
Stephen Chang
parent
34b149e248
commit
28fa5dd033
|
|
@ -42,14 +42,14 @@
|
|||
;; τ.norm in 1st case causes "not valid type" error when file is compiled
|
||||
(define-syntax define-type-alias
|
||||
(syntax-parser
|
||||
[(_ alias:id τ:type)
|
||||
[(_ alias:id τ:any-type)
|
||||
#'(define-syntax- alias
|
||||
(make-variable-like-transformer #'τ))]
|
||||
[(_ (f:id x:id ...) ty)
|
||||
#'(define-syntax- (f stx)
|
||||
(syntax-parse stx
|
||||
[(_ x ...)
|
||||
#:with τ:type #'ty
|
||||
#:with τ:any-type #'ty
|
||||
#'τ.norm]))]))
|
||||
|
||||
(define-typed-syntax define
|
||||
|
|
|
|||
|
|
@ -50,8 +50,8 @@
|
|||
#:with-msg "ann: type mismatch: expected Bool, given Int\n *expression: 1")
|
||||
;ann errs
|
||||
(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
|
||||
(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
|
||||
(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
|
||||
(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")
|
||||
|
||||
|
|
|
|||
|
|
@ -244,8 +244,8 @@
|
|||
(typecheck-fail (ann 1 : Bool) #:with-msg "expected Bool, given Int\n *expression: 1")
|
||||
;ann errs
|
||||
(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
|
||||
(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
|
||||
(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
|
||||
(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")
|
||||
|
||||
; let
|
||||
|
|
|
|||
|
|
@ -673,8 +673,8 @@
|
|||
(typecheck-fail (ann 1 : Bool) #:with-msg "expected Bool, given Int\n *expression: 1")
|
||||
;ann errs
|
||||
(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
|
||||
(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
|
||||
(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
|
||||
(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")
|
||||
|
||||
; let
|
||||
|
|
|
|||
|
|
@ -55,7 +55,7 @@
|
|||
|
||||
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
|
||||
|
||||
(typecheck-fail (λ ([x : (→ 1 2)]) x) #:with-msg "not a valid type")
|
||||
(typecheck-fail (λ ([x : 1]) x) #:with-msg "not a valid type")
|
||||
(typecheck-fail (λ ([x : (+ 1 2)]) x) #:with-msg "not a valid type")
|
||||
(typecheck-fail (λ ([x : (λ ([y : Int]) y)]) x) #:with-msg "not a valid type")
|
||||
(typecheck-fail (λ ([x : (→ 1 2)]) x) #:with-msg "not a well-formed type")
|
||||
(typecheck-fail (λ ([x : 1]) x) #:with-msg "not a well-formed type")
|
||||
(typecheck-fail (λ ([x : (+ 1 2)]) x) #:with-msg "not a well-formed type")
|
||||
(typecheck-fail (λ ([x : (λ ([y : Int]) y)]) x) #:with-msg "not a well-formed type")
|
||||
|
|
|
|||
|
|
@ -237,16 +237,16 @@
|
|||
(typecheck-fail
|
||||
(λ ([x : (∪ Int Boolean)])
|
||||
(test (1 ? x) #t #f))
|
||||
#:with-msg "not a valid type")
|
||||
#:with-msg "not a well-formed type")
|
||||
(typecheck-fail
|
||||
(test (1 ? 1) #t #f)
|
||||
#:with-msg "not a valid type")
|
||||
#:with-msg "not a well-formed type")
|
||||
(typecheck-fail
|
||||
(test (1 ? 1) #t #f)
|
||||
#:with-msg "not a valid type")
|
||||
#:with-msg "not a well-formed type")
|
||||
(typecheck-fail
|
||||
(test (#f ? #t) #t #f)
|
||||
#:with-msg "not a valid type")
|
||||
#:with-msg "not a well-formed type")
|
||||
|
||||
;; -----------------------------------------------------------------------------
|
||||
;; --- Subtypes should not be collapsed
|
||||
|
|
|
|||
|
|
@ -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 (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))
|
||||
;; drop-file-ext : String -> String
|
||||
|
|
@ -401,21 +402,6 @@
|
|||
(syntax-parse (infer es #:tvctx ctx)
|
||||
[(tvs+ _ es+ tys) (list #'tvs+ #'es+ #'tys)]))
|
||||
|
||||
; extra indirection, enables easily overriding type=? with sub?
|
||||
; to add subtyping, without changing any other definitions
|
||||
; - must be here (instead of stlc) due to rackunit-typechecking
|
||||
(define current-typecheck-relation (make-parameter #f))
|
||||
|
||||
;; convenience fns for current-typecheck-relation
|
||||
(define (typecheck? t1 t2)
|
||||
((current-typecheck-relation) t1 t2))
|
||||
(define (typechecks? τs1 τs2)
|
||||
(and (= (stx-length τs1) (stx-length τs2))
|
||||
(stx-andmap typecheck? τs1 τs2)))
|
||||
|
||||
(define current-type-eval (make-parameter #f))
|
||||
(define (type-evals τs) #`#,(stx-map (current-type-eval) τs))
|
||||
|
||||
(define current-promote (make-parameter (λ (t) t)))
|
||||
|
||||
;; term expansion
|
||||
|
|
@ -429,22 +415,6 @@
|
|||
(define (expand/df e)
|
||||
(local-expand e 'expression null))
|
||||
|
||||
;; 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-type-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 τ) τ))
|
||||
|
||||
(current-type-eval default-type-eval)
|
||||
|
||||
;; typecheck-fail-msg/1 : Type Type Stx -> String
|
||||
(define (typecheck-fail-msg/1 τ_expected τ_given expression)
|
||||
(format "type mismatch: expected ~a, given ~a\n expression: ~s"
|
||||
|
|
@ -862,12 +832,21 @@
|
|||
(syntax-parse stx
|
||||
[(_ name:id)
|
||||
#:with names (format-id #'name "~as" #'name)
|
||||
#:with #%tag (format-id #'name "#%~a" #'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? (format-id #'is-name? "current-~a" #'is-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)
|
||||
|
|
@ -878,15 +857,19 @@
|
|||
#: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=? (format-id #'name=? "current-~a" #'name=?)
|
||||
#: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)
|
||||
|
|
@ -894,6 +877,15 @@
|
|||
#: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 #'τ))))
|
||||
|
|
@ -943,14 +935,37 @@
|
|||
[_ (and (stx-pair? t1) (stx-pair? t2)
|
||||
(names=? t1 t2))])))
|
||||
(define current-name=? (make-parameter name=?))
|
||||
(current-typecheck-relation 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)))))
|
||||
(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
|
||||
|
|
|
|||
|
|
@ -41,14 +41,14 @@
|
|||
;; τ.norm in 1st case causes "not valid type" error when file is compiled
|
||||
(define-syntax define-type-alias
|
||||
(syntax-parser
|
||||
[(_ alias:id τ:type)
|
||||
[(_ alias:id τ:any-type)
|
||||
#'(define-syntax- alias
|
||||
(make-variable-like-transformer #'τ))]
|
||||
[(_ (f:id x:id ...) ty)
|
||||
#'(define-syntax- (f stx)
|
||||
(syntax-parse stx
|
||||
[(_ x ...)
|
||||
#:with τ:type #'ty
|
||||
#:with τ:any-type #'ty
|
||||
#'τ.norm]))]))
|
||||
|
||||
(define-typed-syntax define
|
||||
|
|
|
|||
|
|
@ -15,12 +15,17 @@
|
|||
(define-syntax-category kind)
|
||||
|
||||
;; redefine:
|
||||
;; - current-type? - recognizes types with ★ kind only
|
||||
;; - current-type-eval - reduce tylams and tyapps
|
||||
;; - current-type=? - must check for any kind annotations
|
||||
;; - current-type?: well-formed types have kind ★
|
||||
;; - current-any-type?: valid types have any valid kind
|
||||
;; - current-type-eval: reduce tylams and tyapps
|
||||
;; - current-type=?: must compare kind annotations as well
|
||||
(begin-for-syntax
|
||||
;; need this for define-primop (which still uses type stx-class)
|
||||
|
||||
;; well-formed types have kind ★
|
||||
;; (need this for define-primop, which still uses type stx-class)
|
||||
(current-type? (λ (t) (★? (typeof t))))
|
||||
;; o.w., a valid type is one with any valid kind
|
||||
(current-any-type? (λ (t) ((current-kind?) (typeof t))))
|
||||
|
||||
;; TODO: I think this can be simplified
|
||||
(define (normalize τ)
|
||||
|
|
@ -47,11 +52,12 @@
|
|||
; ty=? == syntax eq and syntax prop eq
|
||||
(define (type=? t1 t2)
|
||||
(let ([k1 (typeof t1)][k2 (typeof t2)])
|
||||
(and (or (and (not k1) (not k2)) ; need this bc there's no current-kindcheck-rel
|
||||
; the extra `and` and `or` clauses are bc type=? is a structural
|
||||
; traversal on stx objs, so not all sub stx objs will have a "type"-stx
|
||||
(and (or (and (not k1) (not k2))
|
||||
(and k1 k2 ((current-kind=?) k1 k2)))
|
||||
(old-type=? t1 t2))))
|
||||
(current-type=? type=?)
|
||||
;; TODO: add current-kindcheck-rel
|
||||
(current-typecheck-relation (current-type=?)))
|
||||
|
||||
;; kinds ----------------------------------------------------------------------
|
||||
|
|
@ -64,13 +70,10 @@
|
|||
(define-kind-constructor ⇒ #:arity >= 1)
|
||||
|
||||
;; types ----------------------------------------------------------------------
|
||||
(define-typed-syntax (define-type-alias alias:id τ) ≫
|
||||
[⊢ τ ≫ τ- ⇒ k_τ]
|
||||
#:fail-unless ((current-kind?) #'k_τ)
|
||||
(format "not a valid type: ~a\n" (type->str #'τ))
|
||||
(define-kinded-syntax (define-type-alias alias:id τ:any-type) ≫
|
||||
------------------
|
||||
[≻ (define-syntax- alias
|
||||
(make-variable-like-transformer #'τ-))])
|
||||
(make-variable-like-transformer #'τ.norm))])
|
||||
|
||||
(define-base-type Int : ★)
|
||||
(define-base-type Bool : ★)
|
||||
|
|
@ -79,26 +82,26 @@
|
|||
(define-base-type Char : ★)
|
||||
|
||||
(define-internal-type-constructor →) ; defines →-
|
||||
(define-typed-syntax (→ ty ...+) ≫
|
||||
(define-kinded-syntax (→ ty ...+) ≫
|
||||
[⊢ ty ≫ ty- ⇒ (~★ . _)] ...
|
||||
--------
|
||||
[⊢ (→- ty- ...) ⇒ ★])
|
||||
|
||||
(define-internal-binding-type ∀) ; defines ∀-
|
||||
(define-typed-syntax ∀ #:datum-literals (:)
|
||||
(define-kinded-syntax ∀ #:datum-literals (:)
|
||||
[(_ ([tv:id : k_in:kind] ...) ty) ≫
|
||||
[[tv ≫ tv- : k_in.norm] ... ⊢ ty ≫ ty- ⇒ (~★ . _)]
|
||||
-------
|
||||
[⊢ (∀- (tv- ...) ty-) ⇒ (★ k_in.norm ...)]])
|
||||
|
||||
(define-typed-syntax (tyλ bvs:kind-ctx τ_body) ≫
|
||||
(define-kinded-syntax (tyλ bvs:kind-ctx τ_body) ≫
|
||||
[[bvs.x ≫ tv- : bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
|
||||
#:fail-unless ((current-kind?) #'k_body)
|
||||
(format "not a valid type: ~a\n" (type->str #'τ_body))
|
||||
--------
|
||||
[⊢ (λ- (tv- ...) τ_body-) ⇒ (⇒ bvs.kind ... k_body)])
|
||||
|
||||
(define-typed-syntax (tyapp τ_fn τ_arg ...) ≫
|
||||
(define-kinded-syntax (tyapp τ_fn τ_arg ...) ≫
|
||||
[⊢ τ_fn ≫ τ_fn- ⇒ (~⇒ k_in ... k_out)]
|
||||
#:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
|
||||
(num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
|
||||
|
|
@ -156,9 +159,15 @@
|
|||
--------
|
||||
[⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
|
||||
|
||||
;; TODO: what to do when a def-typed-stx needs both
|
||||
;; current-typecheck-relation and current-kindcheck-relation
|
||||
(define-typed-syntax (inst e τ ...) ≫
|
||||
[⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ (~★ k ...))]
|
||||
[⊢ τ ≫ τ- ⇐ k] ...
|
||||
; [⊢ τ ≫ τ- ⇐ k] ...
|
||||
;; want to use kindchecks? instead of typechecks?
|
||||
[⊢ τ ≫ τ- ⇒ k_τ] ...
|
||||
#:fail-unless (kindchecks? #'(k_τ ...) #'(k ...))
|
||||
(typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...))
|
||||
#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
|
||||
--------
|
||||
[⊢ e- ⇒ τ-inst])
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@
|
|||
|
||||
(define-syntax define-named-type-alias
|
||||
(syntax-parser
|
||||
[(define-named-type-alias Name:id τ:type)
|
||||
[(define-named-type-alias Name:id τ:any-type)
|
||||
#'(define-syntax Name
|
||||
(make-variable-like-transformer (add-orig #'τ #'Name)))]
|
||||
[(define-named-type-alias (f:id x:id ...) ty) ; dont expand yet
|
||||
|
|
|
|||
|
|
@ -50,8 +50,8 @@
|
|||
#:with-msg "ann: type mismatch: expected Bool, given Int\n *expression: 1")
|
||||
;ann errs
|
||||
(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
|
||||
(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
|
||||
(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
|
||||
(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")
|
||||
|
||||
|
|
|
|||
|
|
@ -54,7 +54,7 @@
|
|||
: (→ (→ Int String) (→ Int String)))
|
||||
(typecheck-fail
|
||||
(inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
|
||||
#:with-msg "inst: type mismatch: expected ★, given Int\n *expression: 1")
|
||||
#:with-msg "inst: type mismatch.*expected:.*★.*given:.*Int.*expressions: 1")
|
||||
|
||||
(typecheck-fail
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
|
||||
|
|
|
|||
|
|
@ -669,8 +669,8 @@
|
|||
(typecheck-fail (ann 1 : Bool) #:with-msg "expected Bool, given Int\n *expression: 1")
|
||||
;ann errs
|
||||
(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
|
||||
(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
|
||||
(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
|
||||
(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")
|
||||
|
||||
; let
|
||||
|
|
|
|||
|
|
@ -54,10 +54,10 @@
|
|||
|
||||
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
|
||||
|
||||
(typecheck-fail (λ ([x : (→ 1 2)]) x) #:with-msg "not a valid type")
|
||||
(typecheck-fail (λ ([x : 1]) x) #:with-msg "not a valid type")
|
||||
(typecheck-fail (λ ([x : (+ 1 2)]) x) #:with-msg "not a valid type")
|
||||
(typecheck-fail (λ ([x : (λ ([y : Int]) y)]) x) #:with-msg "not a valid type")
|
||||
(typecheck-fail (λ ([x : (→ 1 2)]) x) #:with-msg "not a well-formed type")
|
||||
(typecheck-fail (λ ([x : 1]) x) #:with-msg "not a well-formed type")
|
||||
(typecheck-fail (λ ([x : (+ 1 2)]) x) #:with-msg "not a well-formed type")
|
||||
(typecheck-fail (λ ([x : (λ ([y : Int]) y)]) x) #:with-msg "not a well-formed type")
|
||||
|
||||
(typecheck-fail
|
||||
(ann (ann 5 : Int) : (→ Int))
|
||||
|
|
|
|||
|
|
@ -112,8 +112,6 @@ Dually, one may write @racket[[⊢ e ≫ e- ⇐ τ]] to check that @racket[e] ha
|
|||
@racket[τ]. Here, both @racket[e] and @racket[τ] are inputs (templates) and only
|
||||
@racket[e-] is an output (pattern).}
|
||||
|
||||
@defform[(define-typerule ....)]{An alias for @racket[define-typed-syntax].}
|
||||
|
||||
@defform*[((define-primop typed-op-id τ)
|
||||
(define-primop typed-op-id : τ)
|
||||
(define-primop typed-op-id op-id τ)
|
||||
|
|
@ -135,11 +133,18 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn
|
|||
use any forms other than @racket[define-base-type] and
|
||||
@racket[define-type-constructor] in conjunction with @racket[define-typed-syntax]. The other forms are considered "low-level" and are automatically used by @racket[define-typed-syntax].
|
||||
@itemlist[
|
||||
@item{@defform[(define-base-type base-type-name-id)]{
|
||||
Defines a base type. A @racket[(define-base-type τ)] additionally defines:
|
||||
@item{@racket[define-typed-syntax], as described above.
|
||||
Uses @racket[current-typecheck-relation] for typechecking.}
|
||||
@item{@defform[(define-typerule ....)]{An alias for @racket[define-typed-syntax].}}
|
||||
@item{@defform*[((define-base-type base-type-name-id)
|
||||
(define-base-type base-type-name-id : kind))]{
|
||||
Defines a base type. @racket[(define-base-type τ)] in turn defines:
|
||||
@itemlist[@item{@racket[τ], an identifier macro representing type @racket[τ].}
|
||||
@item{@racket[τ?], a phase 1 predicate recognizing type @racket[τ].}
|
||||
@item{@racket[~τ], a phase 1 @tech:pat-expander recognizing type @racket[τ].}]}}
|
||||
@item{@racket[~τ], a phase 1 @tech:pat-expander recognizing type @racket[τ].}]}
|
||||
|
||||
The second form is useful when implementing your own kind system.
|
||||
@racket[#%type] is used as the @tt{kind} when it's not specified.}
|
||||
@item{@defform[(define-base-types base-type-name-id ...)]{Defines multiple base types.}}
|
||||
@item{
|
||||
@defform[(define-type-constructor name-id option ...)
|
||||
|
|
@ -235,6 +240,33 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn
|
|||
A @racket[provide]-spec that, given @racket[ty-id], provides @racket[ty-id],
|
||||
and provides @racket[for-syntax] a predicate @racket[ty-id?] and a @tech:pat-expander @racket[~ty-id].}}
|
||||
|
||||
@item{@defparam[current-type-eval type-eval type-eval]{
|
||||
A phase 1 parameter for controlling "type evaluation". A @racket[type-eval]
|
||||
function consumes and produces syntax. It is typically used to convert a type
|
||||
into a canonical representation. The @racket[(current-type-eval)] is called
|
||||
immediately before attacing a type to a syntax object, i.e., by
|
||||
@racket[assign-type].
|
||||
|
||||
It defaults to full expansion, i.e., @racket[(lambda (stx) (local-expand stx 'expression null))], and also stores extra surface syntax information used for error reporting.
|
||||
|
||||
One should extend @racket[current-type-eval] if canonicalization of types
|
||||
depends on combinations of different types, e.g., type lambdas and type application in F-omega. }}
|
||||
|
||||
@item{@defparam[current-typecheck-relation type-pred type-pred]{
|
||||
A phase 1 parameter for controlling type checking, used by @racket[define-type-syntax].
|
||||
A @racket[type-pred] function consumes
|
||||
two types and returns true if they "type check". It defaults to @racket[type=?] though it does not have to be a symmetric relation.
|
||||
Useful for reusing rules that differ only in the type check operation, e.g.,
|
||||
equality vs subtyping.}}
|
||||
|
||||
@item{@defproc[(typecheck? [τ1 type?] [τ2 type?]) boolean?]{A phase 1 function that calls
|
||||
@racket[current-typecheck-relation].}}
|
||||
|
||||
@item{@defproc[(typechecks? [τs1 (or/c (list/c type?) (stx-list/c type?))]
|
||||
[τs2 (or/c (list/c type?) (stx-list/c type?))]) boolean?]{
|
||||
Phase 1 function mapping @racket[typecheck?] over lists of types, pairwise. @racket[τs1] and @racket[τs2]
|
||||
must have the same length.}}
|
||||
|
||||
@item{@defproc[(type=? [τ1 type?] [τ2 type?]) boolean?]{A phase 1 equality
|
||||
predicate for types that computes structural, @racket[free-identifier=?]
|
||||
equality, but includes alpha-equivalence.
|
||||
|
|
@ -270,15 +302,28 @@ equality, but includes alpha-equivalence.
|
|||
A phase 1 parameter for computing type equality. Is initialized to @racket[type=?].}}
|
||||
@item{@defidform[#%type]{The default "kind" used to validate types.}}
|
||||
@item{@defproc[(#%type? [x Any]) boolean?]{Phase 1 predicate recognizing @racket[#%type].}}
|
||||
@item{@defproc[(type? [x Any]) boolean?]{A phase 1 predicate used to validate types.
|
||||
@item{@defproc[(type? [x Any]) boolean?]{A phase 1 predicate recognizing well-formed types.
|
||||
Checks that @racket[x] is a syntax object and has syntax propety @racket[#%type].}}
|
||||
@item{@defparam[current-type? type-pred type-pred]{A phase 1 parameter, initialized to @racket[type?],
|
||||
used to validate types. Useful when reusing type rules in different languages.}}
|
||||
used to recognize well-formed types.
|
||||
Useful when reusing type rules in different languages. For example,
|
||||
System F-omega may define this to recognize types with "star" kinds.}}
|
||||
@item{@defproc[(any-type? [x Any]) boolean?]{A phase 1 predicate recognizing valid types.
|
||||
Defaults to @racket[type?].}}
|
||||
@item{@defparam[current-any-type? type-pred type-pred]{A phase 1 parameter,
|
||||
initialized to @racket[any-type?],
|
||||
used to validate (not necessarily well-formed) types.
|
||||
Useful when reusing type rules in different languages. For example,
|
||||
System F-omega may define this to recognize types with a any valid kind,
|
||||
whereas @racket[current-type?] would recognize types with only the "star" kind.}}
|
||||
@item{@defproc[(mk-type [stx syntax?]) type?]{
|
||||
Phase 1 function that marks a syntax object as a type by attaching @racket[#%type].
|
||||
Useful for defining your own type with arbitrary syntax that does not fit with
|
||||
@racket[define-base-type] or @racket[define-type-constructor].}}
|
||||
@item{@defthing[type stx-class]{A syntax class that calls @racket[current-type?]
|
||||
to validate well-formed types.
|
||||
Binds a @racket[norm] attribute to the type's expanded representation.}}
|
||||
@item{@defthing[any-type stx-class]{A syntax class that calls @racket[current-any-type?]
|
||||
to validate types.
|
||||
Binds a @racket[norm] attribute to the type's expanded representation.}}
|
||||
@item{@defthing[type-bind stx-class]{A syntax class recognizing
|
||||
|
|
@ -335,32 +380,6 @@ necessary to call these directly, since @racket[define-typed-syntax] and other
|
|||
forms already do so, but some type systems may require extending some
|
||||
functionality.
|
||||
|
||||
@defparam[current-type-eval type-eval type-eval]{
|
||||
A phase 1 parameter for controlling "type evaluation". A @racket[type-eval]
|
||||
function consumes and produces syntax. It is typically used to convert a type
|
||||
into a canonical representation. The @racket[(current-type-eval)] is called
|
||||
immediately before attacing a type to a syntax object, i.e., by
|
||||
@racket[assign-type].
|
||||
|
||||
It defaults to full expansion, i.e., @racket[(lambda (stx) (local-expand stx 'expression null))], and also stores extra surface syntax information used for error reporting.
|
||||
|
||||
One should extend @racket[current-type-eval] if canonicalization of types
|
||||
depends on combinations of different types, e.g., type lambdas and type application in F-omega. }
|
||||
|
||||
@defparam[current-typecheck-relation type-pred type-pred]{
|
||||
A phase 1 parameter for controlling type checking. A @racket[type-pred] function consumes
|
||||
two types and returns true if they "type check". It defaults to @racket[type=?] though it does not have to be a symmetric relation.
|
||||
Useful for reusing rules that differ only in the type check operation, e.g.,
|
||||
equality vs subtyping.}
|
||||
|
||||
@defproc[(typecheck? [τ1 type?] [τ2 type?]) boolean?]{A phase 1 function that calls
|
||||
@racket[current-typecheck-relation].}
|
||||
|
||||
@defproc[(typechecks? [τs1 (or/c (list/c type?) (stx-list/c type?))]
|
||||
[τs2 (or/c (list/c type?) (stx-list/c type?))]) boolean?]{
|
||||
Phase 1 function mapping @racket[typecheck?] over lists of types, pairwise. @racket[τs1] and @racket[τs2]
|
||||
must have the same length.}
|
||||
|
||||
@defproc[(assign-type [e syntax?] [τ syntax?]) syntax?]{
|
||||
Phase 1 function that calls @racket[current-type-eval] on @racket[τ] and attaches it to @racket[e]}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,13 +1,15 @@
|
|||
#lang racket/base
|
||||
|
||||
(provide (except-out (all-from-out macrotypes/typecheck) -define-typed-syntax)
|
||||
define-typed-syntax
|
||||
(provide (except-out (all-from-out macrotypes/typecheck)
|
||||
-define-typed-syntax -define-syntax-category)
|
||||
define-typed-syntax define-syntax-category
|
||||
(rename-out [define-typed-syntax define-typerule])
|
||||
(for-syntax syntax-parse/typed-syntax))
|
||||
|
||||
(require (except-in (rename-in
|
||||
macrotypes/typecheck
|
||||
[define-typed-syntax -define-typed-syntax]
|
||||
[define-syntax-category -define-syntax-category]
|
||||
)
|
||||
#%module-begin))
|
||||
|
||||
|
|
@ -418,3 +420,28 @@
|
|||
rule.norm
|
||||
...)]))))
|
||||
|
||||
(define-syntax define-syntax-category
|
||||
(lambda (stx)
|
||||
(syntax-parse stx
|
||||
[(_ name:id)
|
||||
#:with def-named-syntax (format-id #'name "define-~aed-syntax" #'name)
|
||||
#:with check-relation (format-id #'name "current-~acheck-relation" #'name)
|
||||
#'(begin
|
||||
(-define-syntax-category name)
|
||||
(define-syntax (def-named-syntax stx)
|
||||
(syntax-parse stx
|
||||
;; single-clause def
|
||||
[(_ (rulename:id . pats) . rst)
|
||||
;; cannot bind name as pat var, eg #%app, so replace with _
|
||||
#:with r #'[(_ . pats) . rst]
|
||||
#'(define-syntax (rulename stxx)
|
||||
(parameterize ([current-typecheck-relation (check-relation)])
|
||||
(syntax-parse/typed-syntax stxx r)))]
|
||||
;; multi-clause def
|
||||
[(_ rulename:id
|
||||
(~and (~seq kw-stuff (... ...)) :stxparse-kws)
|
||||
rule:rule (... ...+))
|
||||
#'(define-syntax (rulename stxx)
|
||||
(parameterize ([current-typecheck-relation (check-relation)])
|
||||
(syntax-parse/typed-syntax stxx kw-stuff (... ...)
|
||||
rule (... ...))))])))])))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user