commit ccdb667fac361150f49b13f24caa1c8505013b6b
parent a075b9b4f846e07ec863f6d83b02329a1eb96f94
Author: AlexKnauth <alexander@knauth.org>
Date: Sat, 17 Sep 2016 09:15:41 -0400
move default-type-eval into typecheck.rkt
Diffstat:
3 files changed, 17 insertions(+), 68 deletions(-)
diff --git a/macrotypes/examples/stlc.rkt b/macrotypes/examples/stlc.rkt
@@ -1,6 +1,6 @@
#lang s-exp macrotypes/typecheck
(provide (for-syntax current-type=? types=?))
-
+
(require (for-syntax racket/list))
;; Simply-Typed Lambda Calculus
@@ -14,57 +14,7 @@
;; - "type" syntax category; defines:
;; - define-base-type
;; - define-type-constructor
-;; Typechecking forms:
-;; - current-type-eval
-;; - current-type=?
-
-(begin-for-syntax
- ;; type eval
- ;; - 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 (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 type-eval)
-
- ;; type=? : Type Type -> Boolean
- ;; Two types are equivalent when structurally free-identifier=?
- ;; - assumes canonical (ie expanded) representation
- ;; (new: without syntax-parse)
- ;; 2015-10-04: moved to define-syntax-category
- #;(define (type=? t1 t2)
- ;(printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum t1))
- ;(printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum t2))
- (or (and (identifier? t1) (identifier? t2) (free-identifier=? t1 t2))
- (and (stx-null? t1) (stx-null? t2))
- (and (stx-pair? t1) (stx-pair? t2)
- (with-syntax ([(ta ...) t1][(tb ...) t2])
- #;(types=? #'(ta ...) #'(tb ...)) (types=? t1 t2)))))
- ;; (old: uses syntax-parse)
- #;(define (type=? τ1 τ2)
-; (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
-; (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
- (syntax-parse (list τ1 τ2)
- [(x:id y:id) (free-identifier=? τ1 τ2)]
- [((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
- [_ #f]))
-
- #;(define current-type=? (make-parameter type=?))
- #;(current-typecheck-relation type=?)
- ;; convenience fns for current-type=?
- #;(define (types=? τs1 τs2)
- (and (stx-length=? τs1 τs2)
- (stx-andmap (current-type=?) τs1 τs2))))
-
(define-syntax-category type)
(define-type-constructor → #:arity >= 1
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
@@ -420,6 +420,22 @@
(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"
diff --git a/turnstile/examples/stlc.rkt b/turnstile/examples/stlc.rkt
@@ -1,23 +1,6 @@
#lang turnstile/lang
(provide only-in (for-syntax current-type=? types=?))
-(begin-for-syntax
- ;; type eval
- ;; - 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 (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 type-eval))
-
(define-syntax-category type)
(define-type-constructor → #:arity >= 1
#:arg-variances (λ (stx)
