dep.rkt (4034B)
1 #lang turnstile/lang 2 3 ; Π λ ≻ ⊢ ≫ ⇒ ∧ (bidir ⇒ ⇐) 4 5 (provide (rename-out [#%type *]) Π → ∀ λ #%app ann define define-type-alias) 6 7 #;(begin-for-syntax 8 (define old-ty= (current-type=?)) 9 (current-type=? 10 (λ (t1 t2) 11 (displayln (stx->datum t1)) 12 (displayln (stx->datum t2)) 13 (old-ty= t1 t2))) 14 (current-typecheck-relation (current-type=?))) 15 16 ;(define-syntax-category : kind) 17 (define-internal-type-constructor →) 18 (define-internal-binding-type ∀) 19 ;; TODO: how to do Type : Type 20 (define-typed-syntax (Π ([X:id : τ_in] ...) τ_out) ≫ 21 [[X ≫ X- : τ_in] ... ⊢ [τ_out ≫ τ_out- ⇒ _][τ_in ≫ τ_in- ⇒ _] ...] 22 ------- 23 [⊢ (∀- (X- ...) (→- τ_in- ... τ_out-)) ⇒ #,(expand/df #'#%type)]) 24 ;; abbrevs for Π 25 (define-simple-macro (→ τ_in ... τ_out) 26 #:with (X ...) (generate-temporaries #'(τ_in ...)) 27 (Π ([X : τ_in] ...) τ_out)) 28 (define-simple-macro (∀ (X ...) τ) 29 (Π ([X : #%type] ...) τ)) 30 ;; ~Π pattern expander 31 (begin-for-syntax 32 (define-syntax ~Π 33 (pattern-expander 34 (syntax-parser 35 [(_ ([x:id : τ_in] ... (~and (~literal ...) ooo)) τ_out) 36 #'(~∀ (x ... ooo) (~→ τ_in ... ooo τ_out))] 37 [(_ ([x:id : τ_in] ...) τ_out) 38 #'(~∀ (x ...) (~→ τ_in ... τ_out))])))) 39 40 ;; TODO: add case with expected type + annotations 41 ;; - check that annotations match expected types 42 (define-typed-syntax λ 43 [(_ ([x:id : τ_in] ...) e) ≫ 44 [[x ≫ x- : τ_in] ... ⊢ [e ≫ e- ⇒ τ_out][τ_in ≫ τ_in- ⇒ _] ...] 45 ------- 46 [⊢ (λ- (x- ...) e-) ⇒ (Π ([x- : τ_in-] ...) τ_out)]] 47 [(_ (y:id ...) e) ⇐ (~Π ([x:id : τ_in] ...) τ_out) ≫ 48 [[x ≫ x- : τ_in] ... ⊢ #,(substs #'(x ...) #'(y ...) #'e) ≫ e- ⇐ τ_out] 49 --------- 50 [⊢ (λ- (x- ...) e-)]]) 51 52 ;; TODO: do beta on terms? 53 (define-typed-syntax #%app 54 [(_ e_fn e_arg ...) ≫ ; apply lambda 55 [⊢ e_fn ≫ (_ (x ...) e ~!) ⇒ (~Π ([X : τ_in] ...) τ_out)] 56 #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) 57 (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) 58 [⊢ e_arg ≫ e_arg- ⇐ τ_in] ... 59 -------- 60 [⊢ #,(substs #'(e_arg- ...) #'(x ...) #'e) ⇒ 61 #,(substs #'(e_arg- ...) #'(X ...) #'τ_out)]] 62 [(_ e_fn e_arg ... ~!) ≫ ; apply var 63 [⊢ e_fn ≫ e_fn- ⇒ (~Π ([X : τ_in] ...) τ_out)] 64 #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) 65 (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) 66 [⊢ e_arg ≫ e_arg- ⇐ τ_in] ... 67 -------- 68 [⊢ (#%app- e_fn- e_arg- ...) ⇒ 69 #,(substs #'(e_arg- ...) #'(X ...) #'τ_out)]]) 70 71 (define-typed-syntax (ann e (~datum :) τ) ≫ 72 [⊢ e ≫ e- ⇐ τ] 73 -------- 74 [⊢ e- ⇒ τ]) 75 76 (define-syntax define-type-alias 77 (syntax-parser 78 [(_ alias:id τ);τ:any-type) 79 #'(define-syntax- alias 80 (make-variable-like-transformer #'τ))] 81 #;[(_ (f:id x:id ...) ty) 82 #'(define-syntax- (f stx) 83 (syntax-parse stx 84 [(_ x ...) 85 #:with τ:any-type #'ty 86 #'τ.norm]))])) 87 88 (define-typed-syntax define 89 #;[(_ x:id (~datum :) τ:type e:expr) ≫ 90 ;[⊢ e ≫ e- ⇐ τ.norm] 91 #:with y (generate-temporary #'x) 92 -------- 93 [≻ (begin- 94 (define-syntax x (make-rename-transformer (⊢ y : τ.norm))) 95 (define- y (ann e : τ.norm)))]] 96 [(_ x:id e) ≫ 97 ;This won't work with mutually recursive definitions 98 [⊢ e ≫ e- ⇒ _] 99 #:with y (generate-temporary #'x) 100 #:with y+props (transfer-props #'e- #'y #:except '(origin)) 101 -------- 102 [≻ (begin- 103 (define-syntax x (make-rename-transformer #'y+props)) 104 (define- y e-))]] 105 #;[(_ (f [x (~datum :) ty] ... (~or (~datum →) (~datum ->)) ty_out) e ...+) ≫ 106 #:with f- (add-orig (generate-temporary #'f) #'f) 107 -------- 108 [≻ (begin- 109 (define-syntax- f 110 (make-rename-transformer (⊢ f- : (→ ty ... ty_out)))) 111 (define- f- 112 (stlc+lit:λ ([x : ty] ...) 113 (stlc+lit:ann (begin e ...) : ty_out))))]])