From fcd9a83d9c5ef95f1ce98bd6e60feb7c491e5313 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 8 Feb 2017 13:05:59 -0500 Subject: [PATCH] minor cleanup --- .../examples/tests/rackunit-kindchecking.rkt | 16 +++------------ turnstile/examples/fomega-no-reuse-old.rkt | 7 ++----- turnstile/examples/fomega-no-reuse.rkt | 20 ++----------------- .../examples/tests/rackunit-kindchecking.rkt | 18 +++++------------ 4 files changed, 12 insertions(+), 49 deletions(-) diff --git a/macrotypes/examples/tests/rackunit-kindchecking.rkt b/macrotypes/examples/tests/rackunit-kindchecking.rkt index 3c28455..4a886ae 100644 --- a/macrotypes/examples/tests/rackunit-kindchecking.rkt +++ b/macrotypes/examples/tests/rackunit-kindchecking.rkt @@ -5,22 +5,12 @@ (define-syntax (check-kind stx) (syntax-parse stx #:datum-literals (⇒ ->) - ;; duplicate code to avoid redundant expansions - #;[(_ τ tag:id k-expected (~or ⇒ ->) v) - #:with τ+ (expand/df #'(add-expected τ k-expected)) - #:with k (detach #'e+ (stx->datum #'tag)) + [(_ τ tag:id k-expected) + #:with k (detach (expand/df #'(add-expected τ k-expected)) + (stx->datum #'tag)) #:fail-unless (kindcheck? #'k ((current-kind-eval) #'k-expected)) (format "Type ~a [loc ~a:~a] has kind ~a, expected ~a" (syntax->datum #'τ) (syntax-line #'τ) (syntax-column #'τ) (type->str #'k) (type->str #'k-expected)) - (syntax/loc stx (check-equal? τ+ (add-expected v k-expected)))] - [(_ τ tag:id k-expected) - #:with k (detach (expand/df #'(add-expected τ k-expected)) (stx->datum #'tag)) - #:fail-unless - (kindcheck? #'k ((current-kind-eval) #'k-expected)) - (format - "Type ~a [loc ~a:~a] has kind ~a, expected ~a" - (syntax->datum #'τ) (syntax-line #'τ) (syntax-column #'τ) - (type->str #'k) (type->str #'k-expected)) #'(void)])) diff --git a/turnstile/examples/fomega-no-reuse-old.rkt b/turnstile/examples/fomega-no-reuse-old.rkt index 62bb896..e6be65c 100644 --- a/turnstile/examples/fomega-no-reuse-old.rkt +++ b/turnstile/examples/fomega-no-reuse-old.rkt @@ -163,13 +163,10 @@ -------- [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)]) -;; TODO: what to do when a def-typed-stx needs both -;; current-typecheck-relation and current-kindcheck-relation (define-typed-syntax (inst e τ ...) ≫ [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ (~★ k ...))] -; [⊢ τ ≫ τ- ⇐ k] ... - ;; want to use kindchecks? instead of typechecks? - [⊢ τ ≫ τ- ⇒ k_τ] ... +; [⊢ τ ≫ τ- ⇐ k] ... ; ⇐ would use typechecks? + [⊢ τ ≫ τ- ⇒ k_τ] ... ; so use ⇒ and kindchecks? #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...)) (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...)) #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body) diff --git a/turnstile/examples/fomega-no-reuse.rkt b/turnstile/examples/fomega-no-reuse.rkt index 12744b2..488d1ed 100644 --- a/turnstile/examples/fomega-no-reuse.rkt +++ b/turnstile/examples/fomega-no-reuse.rkt @@ -7,8 +7,6 @@ ;; example suggested by Alexis King -;; this version still uses ':: key for kinds - (provide define-type-alias ★ ⇒ Int Bool String Float Char → ∀ tyλ tyapp (typed-out [+ : (→ Int Int Int)]) @@ -51,17 +49,6 @@ (define old-eval (current-type-eval)) (current-type-eval (lambda (τ) (normalize (old-eval τ)))) - ;; (define old-type=? (current-type=?)) - ;; ; ty=? == syntax eq and syntax prop eq - ;; (define (type=? t1 t2) - ;; (let ([k1 (kindof t1)][k2 (kindof t2)]) - ;; ; the extra `and` and `or` clauses are bc type=? is a structural - ;; ; traversal on stx objs, so not all sub stx objs will have a "type"-stx - ;; (and (or (and (not k1) (not k2)) - ;; (and k1 k2 ((current-kind=?) k1 k2))) - ;; (old-type=? t1 t2)))) - ;; (current-type=? type=?) - ;; (current-typecheck-relation type=?)) (define old-typecheck? (current-typecheck-relation)) ; ty=? == syntax eq and syntax prop eq (define (new-typecheck? t1 t2) @@ -71,7 +58,6 @@ (and (or (and (not k1) (not k2)) (and k1 k2 (kindcheck? k1 k2))) (old-typecheck? t1 t2)))) -; (current-type=? type=?) (current-typecheck-relation new-typecheck?)) ;; kinds ---------------------------------------------------------------------- @@ -173,12 +159,10 @@ -------- [⊢ e- ⇒ (∀ ([tv- :: bvs.kind] ...) τ_e)]) -;; TODO: what to do when a def-typed-stx needs both -;; current-typecheck-relation and current-kindcheck-relation (define-typed-syntax (inst e τ:any-type ...) ≫ [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ :: (~★ k ...))] -; [⊢ τ ≫ τ- ⇐ :: k] ... ; doesnt work since def-typed-s ⇐ not using kindcheck? - #:with (k_τ ...) (stx-map kindof #'(τ.norm ...)) +; [⊢ τ ≫ τ- ⇐ k] ... ; ⇐ would use typechecks? + [⊢ τ ≫ τ- ⇒ :: k_τ] ... ; so use ⇒ and kindchecks? #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...)) (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...)) -------- diff --git a/turnstile/examples/tests/rackunit-kindchecking.rkt b/turnstile/examples/tests/rackunit-kindchecking.rkt index 3c28455..ac4b1ca 100644 --- a/turnstile/examples/tests/rackunit-kindchecking.rkt +++ b/turnstile/examples/tests/rackunit-kindchecking.rkt @@ -3,24 +3,16 @@ (only-in "../fomega2.rkt" current-kind-eval kindcheck?)) (provide check-kind) +;; Note: this file is separate from macrotypes/examples/test/rackunit-kindcheck +;; because each one uses different defs of current-kind-eval and kindcheck? (define-syntax (check-kind stx) (syntax-parse stx #:datum-literals (⇒ ->) - ;; duplicate code to avoid redundant expansions - #;[(_ τ tag:id k-expected (~or ⇒ ->) v) - #:with τ+ (expand/df #'(add-expected τ k-expected)) - #:with k (detach #'e+ (stx->datum #'tag)) + [(_ τ tag:id k-expected) + #:with k (detach (expand/df #'(add-expected τ k-expected)) + (stx->datum #'tag)) #:fail-unless (kindcheck? #'k ((current-kind-eval) #'k-expected)) (format "Type ~a [loc ~a:~a] has kind ~a, expected ~a" (syntax->datum #'τ) (syntax-line #'τ) (syntax-column #'τ) (type->str #'k) (type->str #'k-expected)) - (syntax/loc stx (check-equal? τ+ (add-expected v k-expected)))] - [(_ τ tag:id k-expected) - #:with k (detach (expand/df #'(add-expected τ k-expected)) (stx->datum #'tag)) - #:fail-unless - (kindcheck? #'k ((current-kind-eval) #'k-expected)) - (format - "Type ~a [loc ~a:~a] has kind ~a, expected ~a" - (syntax->datum #'τ) (syntax-line #'τ) (syntax-column #'τ) - (type->str #'k) (type->str #'k-expected)) #'(void)]))