~ashton314/understanding-turnstile

64aed333b30c00e1f78ed3b976cb9b508928e4cf — Ashton Wiersdorf 1 year, 1 month ago 8202c63
Cleanup: remove ē → -e
1 files changed, 11 insertions(+), 11 deletions(-)

M stlc.rkt
M stlc.rkt => stlc.rkt +11 -11
@@ 27,9 27,9 @@
    (equal? t1 t2)))

(define-for-syntax (comp+erase-τ e)
  (let* ([ē (expand-stx e)]
         [τ (get-τ ē)])
    `[,ē ,τ]))
  (let* ([-e (expand-stx e)]
         [τ (get-τ -e)])
    `[,-e ,τ]))

(define-for-syntax (comp+erase-τ/ctx e ctx)
  (syntax-parse ctx


@@ 47,22 47,22 @@

(define-syntax (checked-λ stx)
  (syntax-parse stx
    [(_ ([x (~literal :) τ_in] ...) e)
    [(_ ([x (~datum :) τ_in] ...) e)
     #:with [-xs -e τ_out] (comp+erase-τ/ctx #'e #'([x τ_in] ...))
     #:when (printf "derived ~a :: ~a → ~a\n"
                    (syntax->datum stx)
                    (syntax->datum #'(τ_in ...))
                    (syntax->datum #'τ_out))
     #:do [(printf "derived ~a :: ~a → ~a\n"
                   (syntax->datum stx)
                   (syntax->datum #'(τ_in ...))
                   (syntax->datum #'τ_out))]
     (add-τ #'(λ -xs -e) #'(→ τ_in ... τ_out))]))

(define-syntax (checked-app stx)
  (syntax-parse stx
    [(_ e_fn e_arg ...)
     #:with [ē_fn (_ τ_in ... τ_out)] (comp+erase-τ #'e_fn)
     #:with ([ē_arg τ_arg] ...) (stx-map comp+erase-τ #'(e_arg ...))
     #:with [-e_fn (_ τ_in ... τ_out)] (comp+erase-τ #'e_fn)
     #:with ([-e_arg τ_arg] ...) (stx-map comp+erase-τ #'(e_arg ...))
     #:fail-unless (τ= #'(τ_arg ...) #'(τ_in ...))
     (format "~a: Function expected args with type ~a, got type ~a instead"
             (syntax-source stx)
             (syntax->datum #'(τ_in ...))
             (syntax->datum #'(τ_arg ...)))
     (add-τ #'(#%app ē_fn ē_arg ...) #'τ_out)]))
     (add-τ #'(#%app -e_fn -e_arg ...) #'τ_out)]))