tapl: stlc code cleanup

This commit is contained in:
Stephen Chang 2015-05-19 19:00:43 -04:00
parent 338452aadd
commit bd8d1b32d1
2 changed files with 2 additions and 29 deletions

View File

@ -19,7 +19,7 @@
(define-syntax (datum/tc stx)
(syntax-parse stx
[(_ . n:integer) ( (syntax/loc stx (#%datum . n)) #'Int)]
[(_ . n:integer) ( #'(#%datum . n) #'Int)]
[(_ . x)
#:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
(syntax/loc stx (#%datum . x))]))
#'(#%datum . x)]))

View File

@ -11,45 +11,18 @@
;; - multi-arg lambda
;; - multi-arg app
;(define-syntax Int
; (syntax-id-rules ()
; [Int (error 'Int "Cannot use type at run time")]))
;(define-syntax →
; (syntax-id-rules ()
; [(→ τ ...) (error '→ "Cannot use type at run time")]
; [→ (error '→ "Cannot use type at run time")]))
(define-type-constructor )
(define-syntax (λ/tc stx)
(syntax-parse stx
[(_ (b:typed-binding ...) e)
; #:with τ_body (infer/type-ctxt #'([b.x b.τ] ...) #'e)
#:with τ_body (infer/type-ctxt #'([b.x b.τ] ...) #'e)
;; #:with (lam xs+ e+)
; #:with (lam xs+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 e+)))
; (with-extended-type-env
; #'([x τ] ...)
; (expand/df
; #'(λ (x ...)
; (let-syntax
; ([x (make-rename-transformer (⊢ #'x #'τ))] ...)
; e))))
;; #:with e++ (if (identifier? #'e+)
;; (with-extended-type-env #'([x τ] ...) (expand/df #'e+))
;; #'e+)
; #:with τ_body (typeof #'e+)
; #:with τ_body (typeof #'e++)
; (⊢ (syntax/loc stx (λ (b.x ...) e)) #'(b.τ ... → τ_body))]))
( #'(λ (b.x ...) e) #'(b.τ ... τ_body))]))
(define-syntax (app/tc stx)
(syntax-parse stx #:literals ()
[(_ e_fn e_arg ...)
; #:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
; #:with (τ ... → τ_res) (typeof #'e_fn+)
#:with (τ ... τ_res) (infer #'e_fn)
#:with (τ_arg ...) (infers #'(e_arg ...))
; #:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ ...))
#:when (types=? #'(τ ...) #'(τ_arg ...))
; (⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]))
( #'(#%app e_fn e_arg ...) #'τ_res)]))