suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

minor cleanup

Browse Source
This commit is contained in:
Stephen Chang 2017-02-08 13:05:59 -05:00
parent 7058b51cdb
commit fcd9a83d9c
4 changed files with 12 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
macrotypes/examples/tests/rackunit-kindchecking.rkt
View File

@ -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)]))

7
turnstile/examples/fomega-no-reuse-old.rkt
View File

@ -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)

20
turnstile/examples/fomega-no-reuse.rkt
View File

@ -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_τ ...) #'(τ ...))
--------

18
turnstile/examples/tests/rackunit-kindchecking.rkt
View File

@ -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)]))