generalize types and kinds in turnstile; turnstile/fomega tests passing
This commit is contained in:
Stephen Chang
parent
a788c4a7d5
commit
e532907e47
|
|
@ -31,13 +31,11 @@
|
|||
;; 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)
|
||||
(define k (kindof t))
|
||||
(current-type? (λ (t) (define k (kindof t))
|
||||
#;(or (type? t) (★? (typeof t)) (∀★? (typeof t)))
|
||||
(and k ((current-kind?) k) (not (⇒? k)))))
|
||||
;; o.w., a valid type is one with any valid kind
|
||||
(current-any-type? (λ (t)
|
||||
(define k (kindof t))
|
||||
(current-any-type? (λ (t) (define k (kindof t))
|
||||
(and k ((current-kind?) k)))))
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@
|
|||
(define (stx-caddr stx) (stx-cadr (stx-cdr stx)))
|
||||
(define (stx-cddr stx) (stx-cdr (stx-cdr stx)))
|
||||
|
||||
(define datum->stx datum->syntax)
|
||||
(define (stx->datum stx)
|
||||
(if (syntax? stx)
|
||||
(syntax->datum stx)
|
||||
|
|
|
|||
|
|
@ -259,9 +259,12 @@
|
|||
#:with current-type? (mk-param #'type?)
|
||||
#:with current-any-type? (mk-param #'any-type?)
|
||||
;; assigning and retrieving types
|
||||
#:with type-key1 (format-id #'name "~a-key1" #'name)
|
||||
#:with type-key2 (format-id #'name "~a-key2" #'name)
|
||||
#:with assign-type (format-id #'name "assign-~a" #'name)
|
||||
#:with fast-assign-type (format-id #'name "fast-assign-~a" #'name)
|
||||
#:with typeof (format-id #'name "~aof" #'name)
|
||||
#:with tagoftype (format-id #'name "tagof~a" #'name)
|
||||
;; type checking
|
||||
#:with current-typecheck-relation (format-id #'name "current-~acheck-relation" #'name)
|
||||
#:with typecheck? (format-id #'name "~acheck?" #'name)
|
||||
|
|
@ -288,17 +291,20 @@
|
|||
(define (#%tag? t) (and (id? t) (free-id=? t #'#%tag)))
|
||||
(define (mk-type t) (attach t 'key2 #'#%tag))
|
||||
;; type? corresponds to "well-formed" types
|
||||
(define (type? t) (#%tag? (detach t 'key2)))
|
||||
(define (type? t) (#%tag? (tagoftype t)))
|
||||
(define current-type? (make-parameter type?))
|
||||
;; any-type? corresponds to any type, defaults to type?
|
||||
(define (any-type? t) (type? t))
|
||||
(define current-any-type? (make-parameter any-type?))
|
||||
;; assigning and retrieving types ----------------------------------
|
||||
(define (typeof stx) (detach stx 'key1))
|
||||
(define (type-key1) 'key1)
|
||||
(define (type-key2) 'key2)
|
||||
(define (typeof stx) (detach stx 'key1))
|
||||
(define (tagoftype stx) (detach stx 'key2)) ; = kindof if kind stx-cat defined
|
||||
(define (fast-assign-type e τ)
|
||||
(attach e 'key1 (syntax-local-introduce τ)))
|
||||
(define (assign-type e τ)
|
||||
(fast-assign-type e ((current-type-eval) τ)))
|
||||
(fast-assign-type e ((current-type-eval) τ)))
|
||||
;; helper stx classes ----------------------------------------------
|
||||
(define-syntax-class type ;; e.g., well-formed types
|
||||
#:attributes (norm)
|
||||
|
|
@ -444,7 +450,7 @@
|
|||
(add-orig
|
||||
(attach
|
||||
(syntax/loc this-syntax (τ-internal))
|
||||
'new-key2 (expand/df #'new-#%tag))
|
||||
'new-key2 ((current-type-eval) #'new-#%tag))
|
||||
#'τ)])))]))
|
||||
(define-syntax define-base-types
|
||||
(syntax-parser
|
||||
|
|
@ -681,7 +687,7 @@
|
|||
#'(kindcon k_arg (... (... ...)))
|
||||
#'#%tag)
|
||||
(add-orig
|
||||
(attach #'(τ- bvs- . τs-) 'key2 (expand/df #'k_result))
|
||||
(attach #'(τ- bvs- . τs-) 'key2 ((current-type-eval) #'k_result))
|
||||
stx)])))])))]))
|
||||
|
||||
;; end define-syntax-category -------------------------------------------------
|
||||
|
|
@ -690,16 +696,34 @@
|
|||
;; pre-declare all type-related functions and forms
|
||||
(define-syntax-category type)
|
||||
|
||||
;; generic, type-agnostic parameters
|
||||
;; Use these for code that is generic over types and kinds
|
||||
(begin-for-syntax
|
||||
(define current=? (make-parameter (current-type=?)))
|
||||
(define (=s? xs1 xs2) ; map current=? pairwise over lists
|
||||
(and (stx-length=? xs1 xs2) (stx-andmap (current=?) xs1 xs2)))
|
||||
(define (sames? stx) ; check list contains same types
|
||||
(define xs (stx->list stx))
|
||||
(or (null? xs) (andmap (λ (x) ((current=?) (car xs) x)) (cdr xs))))
|
||||
(define current-check-relation (make-parameter (current-typecheck-relation)))
|
||||
(define (check? x1 x2) ((current-check-relation) x1 x2))
|
||||
(define (checks? xs1 xs2) ; map current-check-relation pairwise of lists
|
||||
(and (stx-length=? xs1 xs2) (stx-andmap check? xs1 xs2)))
|
||||
;; (define current-attach (make-parameter assign-type))
|
||||
;; (define current-detach (make-parameter typeof))
|
||||
(define current-ev (make-parameter (current-type-eval)))
|
||||
(define current-tag (make-parameter (type-key1))))
|
||||
|
||||
;; type assignment utilities --------------------------------------------------
|
||||
(begin-for-syntax
|
||||
;; Type assignment macro for nicer syntax
|
||||
(define-syntax (⊢ stx)
|
||||
(syntax-parse stx
|
||||
[(_ e tag τ) #'(attach #`e 'tag ((current-type-eval) #`τ))]
|
||||
[(_ e tag τ) #'(attach #`e 'tag ((current-ev) #`τ))]
|
||||
[(_ e τ) #'(⊢ e : τ)]))
|
||||
(define-syntax (⊢/no-teval stx)
|
||||
(syntax-parse stx
|
||||
[(_ e tag τ) #'(attach #`e 'tag ((current-type-eval) #`τ))]
|
||||
[(_ e tag τ) #'(attach #`e 'tag ((current-ev) #`τ))]
|
||||
[(_ e τ) #'(⊢/no-teval e : τ)]))
|
||||
|
||||
;; Actual type assignment function.
|
||||
|
|
@ -817,18 +841,18 @@
|
|||
|
||||
;; basic infer function with no context:
|
||||
;; infers the type and erases types in an expression
|
||||
(define (infer+erase e #:tag [tag ':])
|
||||
(define (infer+erase e #:tag [tag (current-tag)])
|
||||
(define e+ (expand/df e))
|
||||
(list e+ (detach e+ tag)))
|
||||
;; infers the types and erases types in multiple expressions
|
||||
(define (infers+erase es #:tag [tag ':])
|
||||
(define (infers+erase es #:tag [tag (current-tag)])
|
||||
(stx-map (λ (e) (infer+erase e #:tag tag)) 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.
|
||||
;; 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] #:tag [tag ':])
|
||||
(define (infer es #:ctx [ctx null] #:tvctx [tvctx null] #:tag [tag (current-tag)])
|
||||
(syntax-parse ctx
|
||||
[([x sep τ] ...) ; dont expand yet bc τ may have references to tvs
|
||||
#:with ([tv (~seq tvsep:id tvk) ...] ...) tvctx
|
||||
|
|
@ -855,16 +879,16 @@
|
|||
(for/fold ([tv-id #'tv])
|
||||
([s (in-list (list 'tvsep ...))]
|
||||
[k (in-list (list #'tvk ...))])
|
||||
(attach tv-id s ((current-type-eval) k)))
|
||||
(attach tv-id s ((current-ev) k)))
|
||||
'tyvar #t))] ...)
|
||||
(λ (x ...)
|
||||
(let-syntax
|
||||
([x (make-variable-like-transformer (attach #'x 'sep ((current-type-eval) #'τ)))] ...)
|
||||
([x (make-variable-like-transformer (attach #'x 'sep ((current-ev) #'τ)))] ...)
|
||||
(#%expression e) ... void)))))
|
||||
(list #'tvs+ #'xs+
|
||||
#'(e+ ...)
|
||||
(stx-map (λ (e) (detach e tag)) #'(e+ ...)))]
|
||||
[([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx #:tag tag)]))
|
||||
[([x τ] ...) (infer es #:ctx #`([x #,tag τ] ...) #:tvctx tvctx #:tag tag)]))
|
||||
|
||||
;; fns derived from infer ---------------------------------------------------
|
||||
;; some are syntactic shortcuts, some are for backwards compat
|
||||
|
|
@ -872,16 +896,16 @@
|
|||
;; 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 #:tag [tag ':])
|
||||
(define (infer/ctx+erase ctx e #:tag [tag (current-tag)])
|
||||
(syntax-parse (infer (list e) #:ctx ctx #:tag tag)
|
||||
[(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
|
||||
(define (infers/ctx+erase ctx es #:tag [tag ':])
|
||||
(define (infers/ctx+erase ctx es #:tag [tag (current-tag)])
|
||||
(stx-cdr (infer es #:ctx ctx #:tag tag)))
|
||||
; tyctx = kind env for bound type vars in term e
|
||||
(define (infer/tyctx+erase ctx e #:tag [tag ':])
|
||||
(define (infer/tyctx+erase ctx e #:tag [tag (current-tag)])
|
||||
(syntax-parse (infer (list e) #:tvctx ctx #:tag tag)
|
||||
[(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
|
||||
(define (infers/tyctx+erase ctx es #:tag [tag ':])
|
||||
(define (infers/tyctx+erase ctx es #:tag [tag (current-tag)])
|
||||
(syntax-parse (infer es #:tvctx ctx #:tag tag)
|
||||
[(tvs+ _ es+ tys) (list #'tvs+ #'es+ #'tys)]))
|
||||
|
||||
|
|
@ -1227,7 +1251,7 @@
|
|||
#,(if (attribute has-annotations?)
|
||||
#'(~and
|
||||
(~parse (kindcon-expander k (... (... ...)))
|
||||
(detach #'expanded-τ))
|
||||
(tagoftype #'expanded-τ))
|
||||
(~parse pat
|
||||
#'[([tv k] (... (... ...))) rst]))
|
||||
#'(~parse
|
||||
|
|
@ -1363,7 +1387,7 @@
|
|||
(free-identifier=? #'actual #'lit))
|
||||
fail-msg)
|
||||
stx))])))
|
||||
(define (merge-type-tags stx)
|
||||
(define (merge-type-tags stx) ;; TODO: merge other tags
|
||||
(define t (syntax-property stx ':))
|
||||
(or (and (pair? t)
|
||||
(identifier? (car t)) (identifier? (cdr t))
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
@ -31,16 +31,19 @@
|
|||
;; 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)
|
||||
(define k (typeof t))
|
||||
(current-type? (λ (t) (define k (kindof t))
|
||||
#;(or (type? t) (★? (typeof t)) (∀★? (typeof t)))
|
||||
(and ((current-kind?) k) (not (⇒? k))))))
|
||||
(and k ((current-kind?) k) (not (⇒? k)))))
|
||||
;; o.w., a valid type is one with any valid kind
|
||||
(current-any-type? (λ (t) (define k (kindof t))
|
||||
(and k ((current-kind?) k)))))
|
||||
|
||||
|
||||
; must override, to handle kinds
|
||||
(define-syntax define-type-alias
|
||||
(syntax-parser
|
||||
[(define-type-alias alias:id τ)
|
||||
#:with (τ- k_τ) (infer+erase #'τ)
|
||||
#:with (τ- k_τ) (infer+erase #'τ #:tag '::)
|
||||
#:fail-unless ((current-kind?) #'k_τ)
|
||||
(format "not a valid type: ~a\n" (type->str #'τ))
|
||||
#'(define-syntax alias
|
||||
|
|
@ -79,39 +82,41 @@
|
|||
(define old-eval (current-type-eval))
|
||||
(define (type-eval τ) (normalize (old-eval τ)))
|
||||
(current-type-eval type-eval)
|
||||
(current-ev type-eval)
|
||||
|
||||
(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=?)))
|
||||
(current-typecheck-relation type=?)
|
||||
(current-check-relation type=?))
|
||||
|
||||
(define-typed-syntax (Λ bvs:kind-ctx e) ≫
|
||||
[([bvs.x ≫ tv- : bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e]
|
||||
[([bvs.x ≫ tv- :: bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e]
|
||||
--------
|
||||
[⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
|
||||
[⊢ e- ⇒ (∀ ([tv- :: bvs.kind] ...) τ_e)])
|
||||
|
||||
(define-typed-syntax (inst e τ ...) ≫
|
||||
[⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ (~∀★ k ...))]
|
||||
[⊢ τ ≫ τ- ⇐ k] ...
|
||||
(define-typed-syntax (inst e τ:any-type ...) ≫
|
||||
[⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ :: (~∀★ k ...))]
|
||||
[⊢ τ ≫ τ- ⇐ :: k] ...
|
||||
#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
|
||||
--------
|
||||
[⊢ e- ⇒ τ-inst])
|
||||
|
||||
;; TODO: merge with regular λ and app?
|
||||
;; - see fomega2.rkt
|
||||
(define-typed-syntax (tyλ bvs:kind-ctx τ_body) ≫
|
||||
[[bvs.x ≫ tv- : bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_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))
|
||||
(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 ...])
|
||||
|
|
|
|||
|
|
@ -1,82 +1,82 @@
|
|||
#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)) :: (∀★ ★))
|
||||
(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)
|
||||
: (⇒ ★ ★))
|
||||
(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))))
|
||||
(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))
|
||||
(Λ ([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: expected ★, given Int\n *expression: 1")
|
||||
(inst (Λ ([X :: ★]) (λ ([x : X]) x)) 1)
|
||||
#:with-msg "inst:.*not a valid type: 1")
|
||||
|
||||
(typecheck-fail
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
|
||||
(Λ ([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))
|
||||
(Λ ([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))
|
||||
(Λ ([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))
|
||||
(Λ ([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))
|
||||
(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))
|
||||
|
|
@ -89,104 +89,104 @@
|
|||
(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))))
|
||||
(define-type-alias Pair (tyλ ([A :: ★] [B :: ★]) (∀ ([X :: ★]) (→ (→ A B X) X))))
|
||||
|
||||
;(check-type Pair : (⇒ ★ ★ ★))
|
||||
(check-type Pair : (⇒ ★ ★ (∀★ ★)))
|
||||
(check-type Pair :: (⇒ ★ ★ (∀★ ★)))
|
||||
|
||||
(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
|
||||
(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))))
|
||||
(Λ ([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)))))
|
||||
(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)))))
|
||||
((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)))
|
||||
(Λ ([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))))
|
||||
(Λ ([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))))
|
||||
(Λ ([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)))))
|
||||
((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)))
|
||||
(Λ ([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))))
|
||||
(Λ ([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))))
|
||||
(Λ ([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)))))
|
||||
((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 :: ★]) (λ ([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)
|
||||
(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))
|
||||
(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 (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))))
|
||||
(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 ((λ ([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))
|
||||
(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)
|
||||
((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)))
|
||||
(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)
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -25,16 +25,18 @@
|
|||
;; xs- ; a stx-list of the expanded versions of variables in the ctx
|
||||
;; es*- ; a nested list a depth given by the depth argument, with the same structure
|
||||
;; ; as es*, containing the expanded es*, with the types attached
|
||||
(define (infer/depth #:ctx ctx #:tvctx tvctx depth es* origs*)
|
||||
(define (infer/depth #:ctx ctx #:tvctx tvctx depth es* origs*
|
||||
#:tag [tag (current-tag)])
|
||||
(define flat (stx-flatten/depth-lens depth))
|
||||
(define es (lens-view flat es*))
|
||||
(define origs (lens-view flat origs*))
|
||||
(define/with-syntax [tvxs- xs- es- _]
|
||||
(infer #:tvctx tvctx #:ctx ctx (stx-map pass-orig es origs)))
|
||||
(infer #:tvctx tvctx #:ctx ctx (stx-map pass-orig es origs) #:tag tag))
|
||||
(define es*- (lens-set flat es* #'es-))
|
||||
(list #'tvxs- #'xs- es*-))
|
||||
;; infers/depths
|
||||
(define (infers/depths clause-depth tc-depth tvctxs/ctxs/ess/origss*)
|
||||
(define (infers/depths clause-depth tc-depth tvctxs/ctxs/ess/origss*
|
||||
#:tag [tag (current-tag)])
|
||||
(define flat (stx-flatten/depth-lens clause-depth))
|
||||
(define tvctxs/ctxs/ess/origss
|
||||
(lens-view flat tvctxs/ctxs/ess/origss*))
|
||||
|
|
@ -42,7 +44,7 @@
|
|||
(for/list ([tvctx/ctx/es/origs (in-list (stx->list tvctxs/ctxs/ess/origss))])
|
||||
(match-define (list tvctx ctx es origs)
|
||||
(stx->list tvctx/ctx/es/origs))
|
||||
(infer/depth #:tvctx tvctx #:ctx ctx tc-depth es origs)))
|
||||
(infer/depth #:tvctx tvctx #:ctx ctx tc-depth es origs #:tag tag)))
|
||||
(define res
|
||||
(lens-set flat tvctxs/ctxs/ess/origss* tcs))
|
||||
res)
|
||||
|
|
@ -92,44 +94,45 @@
|
|||
(define-splicing-syntax-class ⇒-prop
|
||||
#:datum-literals (⇒)
|
||||
#:attributes (e-pat)
|
||||
[pattern (~or (~seq ⇒ tag-pat ; implicit : tag
|
||||
(~parse tag #':) (tag-prop:⇒-prop) ...)
|
||||
[pattern (~or (~seq ⇒ tag-pat ; implicit tag
|
||||
(~parse tag #',(current-tag))
|
||||
(tag-prop:⇒-prop) ...)
|
||||
(~seq ⇒ tag:id tag-pat (tag-prop:⇒-prop) ...)) ; explicit tag
|
||||
#:with e-tmp (generate-temporary)
|
||||
#:with e-pat
|
||||
#'(~and e-tmp
|
||||
(~parse
|
||||
(~and tag-prop.e-pat ... tag-pat)
|
||||
(detach #'e-tmp 'tag)))])
|
||||
(detach #'e-tmp `tag)))])
|
||||
(define-splicing-syntax-class ⇒-prop/conclusion
|
||||
#:datum-literals (⇒)
|
||||
#:attributes (tag tag-expr)
|
||||
[pattern (~or (~seq ⇒ tag-stx
|
||||
(~parse tag #':)
|
||||
(~parse (tag-prop.tag ...) #'())
|
||||
(~parse (tag-prop.tag-expr ...) #'()))
|
||||
[pattern (~or (~seq ⇒ tag-stx ; implicit tag
|
||||
(~parse tag #',(current-tag))
|
||||
(~parse (tag-prop.tag ...) #'())
|
||||
(~parse (tag-prop.tag-expr ...) #'()))
|
||||
(~seq ⇒ tag:id tag-stx (tag-prop:⇒-prop/conclusion) ...))
|
||||
#:with tag-expr
|
||||
(for/fold ([tag-expr #'#`tag-stx])
|
||||
([k (in-list (syntax->list #'[tag-prop.tag ...]))]
|
||||
[v (in-list (syntax->list #'[tag-prop.tag-expr ...]))])
|
||||
([k (in-stx-list #'[tag-prop.tag ...])]
|
||||
[v (in-stx-list #'[tag-prop.tag-expr ...])])
|
||||
(with-syntax ([tag-expr tag-expr] [k k] [v v])
|
||||
#'(attach tag-expr 'k ((current-type-eval) v))))])
|
||||
#'(attach tag-expr `k ((current-ev) v))))])
|
||||
(define-splicing-syntax-class ⇐-prop
|
||||
#:datum-literals (⇐ :)
|
||||
#:datum-literals (⇐)
|
||||
#:attributes (τ-stx e-pat)
|
||||
[pattern (~or (~seq ⇐ τ-stx)
|
||||
(~seq ⇐ : τ-stx))
|
||||
[pattern (~or (~seq ⇐ τ-stx (~parse tag #',(current-tag)))
|
||||
(~seq ⇐ tag:id τ-stx))
|
||||
#:with e-tmp (generate-temporary)
|
||||
#:with τ-tmp (generate-temporary)
|
||||
#:with τ-exp (generate-temporary)
|
||||
#:with e-pat
|
||||
#'(~and e-tmp
|
||||
#`(~and e-tmp
|
||||
(~parse τ-exp (get-expected-type #'e-tmp))
|
||||
(~parse τ-tmp (typeof #'e-tmp))
|
||||
(~parse τ-tmp (detach #'e-tmp `tag))
|
||||
(~parse
|
||||
(~post
|
||||
(~fail #:when (and (not (typecheck? #'τ-tmp #'τ-exp))
|
||||
(~fail #:when (and (not (check? #'τ-tmp #'τ-exp))
|
||||
(get-orig #'e-tmp))
|
||||
(typecheck-fail-msg/1 #'τ-exp #'τ-tmp #'e-tmp)))
|
||||
(get-orig #'e-tmp)))])
|
||||
|
|
@ -165,7 +168,7 @@
|
|||
#:with [x- ...] #'[ctx1.x- ... ...]
|
||||
#:with [ctx ...] #'[ctx1.ctx ... ...]])
|
||||
(define-syntax-class tc-elem
|
||||
#:datum-literals (⊢ ⇒ ⇐ ≫ :)
|
||||
#:datum-literals (⊢ ⇒ ⇐ ≫)
|
||||
#:attributes (e-stx e-stx-orig e-pat)
|
||||
[pattern [e-stx ≫ e-pat* props:⇒-props]
|
||||
#:with e-stx-orig #'e-stx
|
||||
|
|
@ -229,55 +232,56 @@
|
|||
#'[(tvctx.ctx ...) (ctx.ctx ...) tc.es-stx tc.es-stx-orig]
|
||||
#'[ooo ...])
|
||||
#:with pat
|
||||
#'(~post
|
||||
#`(~post
|
||||
(~post
|
||||
(~parse
|
||||
tcs-pat
|
||||
(infers/depths 'clause-depth 'tc.depth #'tvctxs/ctxs/ess/origs))))]
|
||||
(infers/depths 'clause-depth 'tc.depth #'tvctxs/ctxs/ess/origs
|
||||
#:tag (current-tag)))))]
|
||||
)
|
||||
(define-splicing-syntax-class clause
|
||||
#:attributes (pat)
|
||||
#:datum-literals (τ⊑ τ=)
|
||||
#:datum-literals (τ⊑ τ=) ; TODO: drop the τ
|
||||
[pattern :tc-clause]
|
||||
[pattern [a τ⊑ b]
|
||||
#:with pat
|
||||
#'(~post
|
||||
(~fail #:unless (typecheck? #'a #'b)
|
||||
(~fail #:unless (check? #'a #'b)
|
||||
(typecheck-fail-msg/1/no-expr #'b #'a)))]
|
||||
[pattern [a τ⊑ b #:for e]
|
||||
#:with pat
|
||||
#'(~post
|
||||
(~fail #:unless (typecheck? #'a #'b)
|
||||
(~fail #:unless (check? #'a #'b)
|
||||
(typecheck-fail-msg/1 #'b #'a #'e)))]
|
||||
[pattern (~seq [a τ⊑ b] ooo:elipsis)
|
||||
#:with pat
|
||||
#'(~post
|
||||
(~fail #:unless (typechecks? #'[a ooo] #'[b ooo])
|
||||
(~fail #:unless (checks? #'[a ooo] #'[b ooo])
|
||||
(typecheck-fail-msg/multi/no-exprs #'[b ooo] #'[a ooo])))]
|
||||
[pattern (~seq [a τ⊑ b #:for e] ooo:elipsis)
|
||||
#:with pat
|
||||
#'(~post
|
||||
(~fail #:unless (typechecks? #'[a ooo] #'[b ooo])
|
||||
(~fail #:unless (checks? #'[a ooo] #'[b ooo])
|
||||
(typecheck-fail-msg/multi #'[b ooo] #'[a ooo] #'[e ooo])))]
|
||||
[pattern [a τ= b]
|
||||
#:with pat
|
||||
#'(~post
|
||||
(~fail #:unless ((current-type=?) #'a #'b)
|
||||
(~fail #:unless ((current=?) #'a #'b)
|
||||
(typecheck-fail-msg/1/no-expr #'b #'a)))]
|
||||
[pattern [a τ= b #:for e]
|
||||
#:with pat
|
||||
#'(~post
|
||||
(~fail #:unless ((current-type=?) #'a #'b)
|
||||
(~fail #:unless ((current=?) #'a #'b)
|
||||
(typecheck-fail-msg/1 #'b #'a #'e)))]
|
||||
[pattern (~seq [a τ= b] ooo:elipsis)
|
||||
#:with pat
|
||||
#'(~post
|
||||
(~fail #:unless (types=? #'[a ooo] #'[b ooo])
|
||||
(~fail #:unless (=s? #'[a ooo] #'[b ooo])
|
||||
(typecheck-fail-msg/multi/no-exprs #'[b ooo] #'[a ooo])))]
|
||||
[pattern (~seq [a τ= b #:for e] ooo:elipsis)
|
||||
#:with pat
|
||||
#'(~post
|
||||
(~fail #:unless (types=? #'[a ooo] #'[b ooo])
|
||||
(~fail #:unless (=s? #'[a ooo] #'[b ooo])
|
||||
(typecheck-fail-msg/multi #'[b ooo] #'[a ooo] #'[e ooo])))]
|
||||
[pattern (~seq #:when condition:expr)
|
||||
#:with pat
|
||||
|
|
@ -296,7 +300,7 @@
|
|||
#'(~post (~fail #:unless condition message))]
|
||||
)
|
||||
(define-syntax-class last-clause
|
||||
#:datum-literals (⊢ ≫ ≻ ⇒ ⇐ :)
|
||||
#:datum-literals (⊢ ≫ ≻ ⇒ ⇐)
|
||||
#:attributes ([pat 0] [stuff 1] [body 0])
|
||||
;; ⇒ conclusion
|
||||
[pattern (~or [⊢ pat ≫ e-stx props:⇒-props/conclusion]
|
||||
|
|
@ -304,21 +308,25 @@
|
|||
#:with [stuff ...] #'[]
|
||||
#:with body:expr
|
||||
(for/fold ([body #'(quasisyntax/loc this-syntax e-stx)])
|
||||
([k (in-list (syntax->list #'[props.tag ...]))]
|
||||
[v (in-list (syntax->list #'[props.tag-expr ...]))])
|
||||
([k (in-stx-list #'[props.tag ...])]
|
||||
[v (in-stx-list #'[props.tag-expr ...])])
|
||||
(with-syntax ([body body] [k k] [v v])
|
||||
#'(attach body 'k ((current-type-eval) v))))]
|
||||
#'(attach body `k ((current-ev) v))))]
|
||||
;; ⇒ conclusion, implicit pat
|
||||
[pattern (~or [⊢ e-stx props:⇒-props/conclusion]
|
||||
[⊢ [e-stx props:⇒-props/conclusion]])
|
||||
#:with :last-clause #'[⊢ [_ ≫ e-stx . props]]]
|
||||
;; ⇐ conclusion
|
||||
[pattern [⊢ (~and e-stx (~not [_ ≫ . rst]))]
|
||||
#:with :last-clause #'[⊢ [_ ≫ e-stx ⇐ : _]]]
|
||||
[pattern (~or [⊢ pat* ≫ e-stx ⇐ τ-pat]
|
||||
[⊢ pat* ≫ e-stx ⇐ : τ-pat]
|
||||
[⊢ [pat* ≫ e-stx ⇐ τ-pat]]
|
||||
[⊢ [pat* ≫ e-stx ⇐ : τ-pat]])
|
||||
[pattern [⊢ (~and e-stx (~not [_ ≫ . rst]))] ;; TODO: this current tag isnt right?
|
||||
#:with :last-clause #`[⊢ [_ ≫ e-stx ⇐ #,(datum->stx #'h (current-tag)) _]]]
|
||||
[pattern (~or [⊢ pat* (~seq ≫ e-stx
|
||||
⇐ τ-pat ; implicit tag
|
||||
(~parse tag #',(current-tag)))]
|
||||
[⊢ pat* ≫ e-stx ⇐ tag:id τ-pat] ; explicit tag
|
||||
[⊢ [pat* (~seq ≫ e-stx
|
||||
⇐ τ-pat ; implicit tag
|
||||
(~parse tag #',(current-tag)))]]
|
||||
[⊢ [pat* ≫ e-stx ⇐ tag:id τ-pat]]) ; explicit tag
|
||||
#:with stx (generate-temporary 'stx)
|
||||
#:with τ (generate-temporary #'τ-pat)
|
||||
#:with pat
|
||||
|
|
@ -330,7 +338,7 @@
|
|||
(~parse τ-pat #'τ))
|
||||
#:with [stuff ...] #'[]
|
||||
#:with body:expr
|
||||
#'(assign-type (quasisyntax/loc this-syntax e-stx) #`τ)]
|
||||
#'(attach (quasisyntax/loc this-syntax e-stx) `tag #`τ)]
|
||||
;; macro invocations
|
||||
[pattern [≻ e-stx]
|
||||
#:with :last-clause #'[_ ≻ e-stx]]
|
||||
|
|
@ -346,11 +354,12 @@
|
|||
#:with body:expr
|
||||
;; should never get here
|
||||
#'(error msg)])
|
||||
(define-splicing-syntax-class pat #:datum-literals (⇐ :)
|
||||
(define-splicing-syntax-class pat #:datum-literals (⇐)
|
||||
[pattern (~seq pat)
|
||||
#:attr transform-body identity]
|
||||
[pattern (~or (~seq pat* left:⇐ τ-pat)
|
||||
(~seq pat* left:⇐ : τ-pat))
|
||||
[pattern (~or (~seq pat* left:⇐ τ-pat ; implicit tag
|
||||
(~parse tag #',current-tag))
|
||||
(~seq pat* left:⇐ tag:id τ-pat)) ; explicit tag
|
||||
#:with stx (generate-temporary 'stx)
|
||||
#:with τ (generate-temporary #'τ-pat)
|
||||
#:with b (generate-temporary 'body)
|
||||
|
|
@ -363,11 +372,10 @@
|
|||
(~parse τ-pat #'τ))
|
||||
#:attr transform-body
|
||||
(lambda (body)
|
||||
#`(let ([b #,body])
|
||||
(when (and (typeof b)
|
||||
(not (typecheck? (typeof b) #'τ)))
|
||||
(raise-⇐-expected-type-error #'left b #'τ (typeof b)))
|
||||
(assign-type b #'τ)))])
|
||||
#`(let* ([b #,body][ty-b (detach b `tag)])
|
||||
(when (and ty-b (not (check? ty-b #'τ)))
|
||||
(raise-⇐-expected-type-error #'left b #'τ ty-b))
|
||||
(attach b `tag #'τ)))])
|
||||
(define-syntax-class rule #:datum-literals (≫)
|
||||
[pattern [pat:pat ≫
|
||||
clause:clause ...
|
||||
|
|
@ -425,25 +433,43 @@
|
|||
(define-syntax define-syntax-category
|
||||
(lambda (stx)
|
||||
(syntax-parse stx
|
||||
[(_ name:id)
|
||||
[(_ name:id) ; default key1 = ': for types
|
||||
#'(define-syntax-category : name)]
|
||||
[(_ key:id name:id) ; default key2 = ':: for kinds
|
||||
#`(define-syntax-category key name #,(mkx2 #'key))]
|
||||
[(_ key1:id name:id key2:id)
|
||||
#:with def-named-syntax (format-id #'name "define-~aed-syntax" #'name)
|
||||
#:with check-relation (format-id #'name "current-~acheck-relation" #'name)
|
||||
#:with new-check-relation (format-id #'name "current-~acheck-relation" #'name)
|
||||
;; #:with new-attach (format-id #'name "assign-~a" #'name)
|
||||
;; #:with new-detach (format-id #'name "~aof" #'name)
|
||||
#:with new-eval (format-id #'name "current-~a-eval" #'name)
|
||||
#'(begin
|
||||
(-define-syntax-category name)
|
||||
(-define-syntax-category key1 name key2)
|
||||
(define-syntax (def-named-syntax stx)
|
||||
(syntax-parse stx
|
||||
;; single-clause def
|
||||
[(_ (rulename:id . pats) . rst)
|
||||
#;[(_ (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)])
|
||||
(parameterize ([current-check-relation (new-check-relation)]
|
||||
[current-attach new-attach]
|
||||
[current-detach new-detach]
|
||||
[current-tag 'key1])
|
||||
(syntax-parse/typed-syntax stxx r)))]
|
||||
[(_ (rulename:id . pats) . rst)
|
||||
;; cannot bind name as pat var, eg #%app, so replace with _
|
||||
#:with r #'[(_ . pats) . rst]
|
||||
#'(def-named-syntax rulename r)]
|
||||
;; multi-clause def
|
||||
[(_ rulename:id
|
||||
(~and (~seq kw-stuff (... ...)) :stxparse-kws)
|
||||
rule:rule (... ...+))
|
||||
#'(define-syntax (rulename stxx)
|
||||
(parameterize ([current-typecheck-relation (check-relation)])
|
||||
(parameterize ([current-check-relation (new-check-relation)]
|
||||
;; [current-attach new-attach]
|
||||
;; [current-detach new-detach]
|
||||
[current-ev (new-eval)]
|
||||
[current-tag 'key1])
|
||||
(syntax-parse/typed-syntax stxx kw-stuff (... ...)
|
||||
rule (... ...))))])))])))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user