commit 0aa2857e7442be0570520edccc73d68d3b44573e
parent 2278adcf959a1164129f99ca27da612c67c98aed
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 6 Oct 2015 14:28:08 -0400
define-syntax-category defines default type=?; other cleanup
- extended type=? in rec-iso only does 1 subst
- simplify current-type? in fomega by defining in terms of current-kind?
Diffstat:
4 files changed, 43 insertions(+), 10 deletions(-)
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
@@ -21,7 +21,10 @@
;; (However, this is not completely possible, eg define-type-alias)
;; 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) (or (type? t) (★? (typeof t)) (∀★? (typeof t)) #;(kind? (typeof t))))))
+ (current-type? (λ (t)
+ (define k (typeof t))
+ #;(or (type? t) (★? (typeof t)) (∀★? (typeof t)))
+ (and ((current-kind?) k) (not (⇒? k))))))
; must override, to handle kinds
(provide define-type-alias)
@@ -106,7 +109,7 @@
(define-typed-syntax Λ
[(_ bvs:kind-ctx e)
#:with ((tv- ...) e- τ_e)
- (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
+ (infer/ctx+erase #'bvs #'e); #:expand (current-type-eval))
(⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
(define-typed-syntax inst
diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt
@@ -29,8 +29,20 @@
#:when (types=? #'(k1 ...) #'(k2 ...))
#:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
#:with (z ...) (generate-temporaries #'(x ...))
- ((current-type=?) (substs #'(z ...) #'(x ...) #'t1)
- (substs #'(z ...) #'(y ...) #'t2))]
+ ;; alternative #1: install wrappers that checks for x and y and return true
+ #;(define old-type=? (current-type=?))
+ #;(define (new-type=? ty1 ty2)
+ (or (and (identifier? ty1) (identifier? ty2)
+ (stx-ormap (λ (x y)
+ (and (bound-identifier=? ty1 x) (bound-identifier=? ty2 y)))
+ #'(x ...) #'(y ...)))
+ (old-type=? ty1 ty2)))
+ #;(parameterize ([current-type=? new-type=?]) ((current-type=?) #'t1 #'t2))
+ ;; alternative #2: subst fresh identifier for both x and y
+ #;((current-type=?) (substs #'(z ...) #'(x ...) #'t1)
+ (substs #'(z ...) #'(y ...) #'t2))
+ ;; alternative #3: subst y for x in t1
+ ((current-type=?) (substs #'(y ...) #'(x ...) #'t1) #'t2)]
[_ (stlc:type=? τ1 τ2)]))
(current-type=? type=?)
(current-typecheck-relation type=?))
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -36,14 +36,17 @@
;; type=? : Type Type -> Boolean
;; Two types are equivalent when structurally free-identifier=?
;; - assumes canonical (ie expanded) representation
- (define (type=? t1 t2)
+ ;; (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)))))
+ #;(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))
@@ -52,11 +55,11 @@
[((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
[_ #f]))
- (define current-type=? (make-parameter type=?))
- (current-typecheck-relation type=?)
+ #;(define current-type=? (make-parameter type=?))
+ #;(current-typecheck-relation type=?)
;; convenience fns for current-type=?
- (define (types=? τs1 τs2)
+ #;(define (types=? τs1 τs2)
(and (stx-length=? τs1 τs2)
(stx-andmap (current-type=?) τs1 τs2))))
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -473,6 +473,9 @@
#:with define-base-name (format-id #'name "define-base-~a" #'name)
#:with define-name-cons (format-id #'name "define-~a-constructor" #'name)
#:with name-ann (format-id #'name "~a-ann" #'name)
+ #:with name=? (format-id #'name "~a=?" #'name)
+ #:with names=? (format-id #'names "~a=?" #'names)
+ #:with current-name=? (format-id #'name=? "current-~a" #'name=?)
#'(begin
(provide (for-syntax current-is-name? is-name? #%tag? mk-name name name-bind name-ann name-ctx)
#%tag define-base-name define-name-cons)
@@ -521,7 +524,19 @@
"Improperly formatted ~a annotation: ~a; should have shape {τ}, "
"where τ is a valid ~a.")
'name (type->str #'any) 'name))
- #:attr norm #f)))
+ #:attr norm #f))
+ (define (name=? 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)
+ (names=? t1 t2))))
+ (define current-name=? (make-parameter name=?))
+ (current-typecheck-relation name=?)
+ (define (names=? τs1 τs2)
+ (and (stx-length=? τs1 τs2)
+ (stx-andmap (current-name=?) τs1 τs2))))
(define-syntax define-base-name
(syntax-parser
[(_ (~var x id)) #'(define-basic-checked-id-stx x : #%tag)]))
