From f825eef92fd1c251edb04ce0edd8d18a45861689 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Mon, 30 Jan 2017 15:11:57 -0500 Subject: [PATCH] raco setup completes --- macrotypes/examples/fomega.rkt | 2 +- macrotypes/examples/fomega2.rkt | 2 +- macrotypes/examples/infer.rkt | 2 +- macrotypes/typecheck.rkt | 55 ++++++++++--------- turnstile/examples/fomega-no-reuse.rkt | 8 +-- .../examples/tests/rackunit-typechecking.rkt | 4 +- turnstile/turnstile.rkt | 6 +- 7 files changed, 41 insertions(+), 38 deletions(-) diff --git a/macrotypes/examples/fomega.rkt b/macrotypes/examples/fomega.rkt index 57d27fb..338916b 100644 --- a/macrotypes/examples/fomega.rkt +++ b/macrotypes/examples/fomega.rkt @@ -53,7 +53,7 @@ (define-kind-constructor ⇒ #:arity >= 1) (define-kind-constructor ∀★ #:arity >= 0) -(define-binding-type ∀ #:bvs >= 0 #:arr ∀★) +(define-binding-type ∀ #:arr ∀★) ;; alternative: normalize before type=? ; but then also need to normalize in current-promote diff --git a/macrotypes/examples/fomega2.rkt b/macrotypes/examples/fomega2.rkt index e5bdce9..cceb550 100644 --- a/macrotypes/examples/fomega2.rkt +++ b/macrotypes/examples/fomega2.rkt @@ -44,7 +44,7 @@ (define-base-kind ★) (define-kind-constructor ∀★ #:arity >= 0) -(define-binding-type ∀ #:bvs >= 0 #:arr ∀★) +(define-binding-type ∀ #:arr ∀★) ;; alternative: normalize before type=? ; but then also need to normalize in current-promote diff --git a/macrotypes/examples/infer.rkt b/macrotypes/examples/infer.rkt index 9849f34..3c6a13b 100644 --- a/macrotypes/examples/infer.rkt +++ b/macrotypes/examples/infer.rkt @@ -51,7 +51,7 @@ (for/fold ([tv-id #'tv]) ([s (in-list (list 'sep ...))] [k (in-list (list #'tvk ...))]) - (assign-type tv-id k #:tag s)) + (attach tv-id s k)) 'tyvar #t))] ...) (λ- (x ...) (let-syntax diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt index f3c81f7..f04d41a 100644 --- a/macrotypes/typecheck.rkt +++ b/macrotypes/typecheck.rkt @@ -240,6 +240,12 @@ [(_ key:id name:id) ; default key2 = ':: for kinds #`(define-syntax-category key name #,(mkx2 #'key))] [(_ key1:id name:id key2:id) + ;; syntax classes + #:with type #'name ; dangerous, check `type` not used in binding pos below + #:with any-type (format-id #'name "any-~a" #'name) + #:with type-ctx (format-id #'name "~a-ctx" #'name) + #:with type-bind (format-id #'name "~a-bind" #'name) + #:with type-ann (format-id #'name "~a-ann" #'name) ;; type well-formedness #:with #%tag (mk-#% #'name) ; default "type" for this metadata, e.g. #%type #:with #%tag? (mk-? #'#%tag) @@ -252,12 +258,6 @@ #:with assign-type (format-id #'name "assign-~a" #'name) #:with fast-assign-type (format-id #'name "fast-assign-~a" #'name) #:with typeof (format-id #'name "~aof" #'name) - ;; syntax classes - #:with type #'name ; dangerous, check `type` not used in binding pos below - #:with any-type (format-id #'name "any-~a" #'name) - #:with type-ctx (format-id #'name "~a-ctx" #'name) - #:with type-bind (format-id #'name "~a-bind" #'name) - #:with type-ann (format-id #'name "~a-ann" #'name) ;; type checking #:with current-typecheck-relation (format-id #'name "current-~acheck-relation" #'name) #:with typecheck? (format-id #'name "~acheck?" #'name) @@ -272,10 +272,10 @@ ;; defining types #:with define-base-type (format-id #'name "define-base-~a" #'name) #:with define-base-types (format-id #'name "define-base-~as" #'name) - #:with define-type-constructor (format-id #'name "define-~a-constructor" #'name) - #:with define-binding-type (format-id #'name "define-binding-~a" #'name) #:with define-internal-type-constructor (format-id #'name "define-internal-~a-constructor" #'name) + #:with define-type-constructor (format-id #'name "define-~a-constructor" #'name) #:with define-internal-binding-type (format-id #'name "define-internal-binding-~a" #'name) + #:with define-binding-type (format-id #'name "define-binding-~a" #'name) #:with type-out (format-id #'name "~a-out" #'name) #'(begin (define #%tag void) ; TODO: cache expanded #%tag? @@ -406,8 +406,8 @@ modes)])))) (define-syntax define-base-type (syntax-parser - [(_ (~var x id)) ; default to 'key2 and #%tag - #'(define-base-type x key2 #%tag)] + [(_ (~var τ id)) ; default to 'key2 and #%tag + #'(define-base-type τ key2 #%tag)] [(_ (~var τ id) new-key2 new-#%tag) #:with τ? (mk-? #'τ) #:with τ-expander (mk-~ #'τ) @@ -462,7 +462,7 @@ invariant))])) (~optional ; extra-info (~seq #:extra-info extra-info) - #:defaults ([extra-info #'void]))) ...) + #:defaults ([extra-info #'void]))) (... ...)) ; #:with #%kind (mk-#% #'kind) #:with τ? (mk-? #'τ) #:with τ- (mk-- #'τ) @@ -517,18 +517,19 @@ (define-syntax define-type-constructor (syntax-parser [(_ (~var τ id) . options) + #:with τ- (mk-- #'τ) #'(begin (define-internal-type-constructor τ . options) ; #'(define-basic-checked-stx x key2 type . rst)])) (define-syntax (τ stx) (syntax-parse stx [(_ . args) - #:with ([arg- _] (... ...)) (infers+erase #'args #:tag 'key2) + #:with ([arg- _] (... (... ...))) (infers+erase #'args #:tag 'key2) ;; args are validated on the next line rather than above ;; to ensure enough stx-parse progress for proper err msg, ;; ie, "invalid type" instead of "improper tycon usage" - #:with (~! (~var _ type) (... ...)) #'(arg- (... ...)) - (add-orig (mk-type #'(τ- arg- (... ...))) stx)])))])) + #:with (~! (~var _ type) (... (... ...))) #'(arg- (... (... ...))) + (add-orig (mk-type #'(τ- arg- (... (... ...)))) stx)])))])) (define-syntax define-internal-binding-type (syntax-parser [(_ (~var τ id) @@ -548,7 +549,7 @@ invariant))])) (~optional ; extra-info (~seq #:extra-info extra-info) - #:defaults ([extra-info #'void]))) ...) + #:defaults ([extra-info #'void]))) (... ...)) #:with τ? (mk-? #'τ) #:with τ- (mk-- #'τ) #:with τ-expander (mk-~ #'τ) @@ -583,7 +584,7 @@ (format "Expected ~a type, got: ~a" 'τ (type->str #'expanded-τ)) #'expanded-τ) - (~and bvs (tv (... (... ...)))) + (~and bvs (tv (... (... (... ...))))) . rst) ;; #,(if (attribute has-annotations?) ;; #'(~and @@ -591,9 +592,9 @@ ;; (detach #'expanded-τ)) ;; (~parse pat ;; #'[([tv k] (... (... ...))) rst])) - #'(~parse - pat - #'[bvs rst]))] + (~parse + pat + #'[bvs rst]))] ;; TODO: fix this to handle has-annotations? ;; the difference with the first case is that here ;; the body is ungrouped, ie, @@ -621,7 +622,7 @@ (define-syntax (τ- stx) (syntax-parse stx [(_ bvs . args) - #:fail-unless (bvs-op (stx-length #'bvs+ks) bvs-n) + #:fail-unless (bvs-op (stx-length #'bvs) bvs-n) (format "wrong number of type vars, expected ~a ~a" 'bvs-op 'bvs-n) #:fail-unless (op (stx-length #'args) n) @@ -648,31 +649,33 @@ #:defaults ([kindcon #'void])) ; default kindcon should never be used . other-options) ; #'(define-binding-checked-stx x key2 type . rst)])))])) - #'(begin + #:with τ- (mk-- #'τ) + #`(begin (define-internal-binding-type τ . other-options) (define-syntax (τ stx) (syntax-parse stx - [(_ (~or (bv:id (... ...)) + [(_ (~or (bv:id (... (... ...))) (~and (~fail #:unless #,(attribute has-annotations?)) bvs+ann)) . args) #:with bvs+ks (if #,(attribute has-annotations?) #'bvs+ann - #'([bv key2 #%tag] (... ...))) + #'([bv key2 #%tag] (... (... ...)))) #:with (bvs- τs- _) (infers/ctx+erase #'bvs+ks #'args #:tag 'key2) ;; args are validated on the next line rather than above ;; to ensure enough stx-parse progress for proper err msg, ;; ie, "invalid type" instead of "improper tycon usage" - #:with (~! (~var _ type) (... ...)) #'τs- - #:with ([tv (~datum key2) k_arg] (... ...)) #'bvs+ks + #:with (~! (~var _ type) (... (... ...))) #'τs- + #:with ([tv (~datum key2) k_arg] (... (... ...))) #'bvs+ks #:with k_result (if #,(attribute has-annotations?) - #'(kindcon k_arg (... ...)) + #'(kindcon k_arg (... (... ...))) #'#%tag) (add-orig (attach #'(τ- bvs- . τs-) 'key2 (expand/df #'k_result)) stx)])))])))])) ;; end define-syntax-category ------------------------------------------------- +;; ---------------------------------------------------------------------------- ;; pre-declare all type-related functions and forms (define-syntax-category type) diff --git a/turnstile/examples/fomega-no-reuse.rkt b/turnstile/examples/fomega-no-reuse.rkt index 034ea1f..cfee4ea 100644 --- a/turnstile/examples/fomega-no-reuse.rkt +++ b/turnstile/examples/fomega-no-reuse.rkt @@ -23,9 +23,9 @@ ;; well-formed types have kind ★ ;; (need this for define-primop, which still uses type stx-class) - (current-type? (λ (t) (★? (typeof t)))) + (current-type? (λ (t) (★? (kindof t)))) ;; o.w., a valid type is one with any valid kind - (current-any-type? (λ (t) ((current-kind?) (typeof t)))) + (current-any-type? (λ (t) ((current-kind?) (kindof t)))) ;; TODO: I think this can be simplified (define (normalize τ) @@ -51,7 +51,7 @@ (define old-type=? (current-type=?)) ; ty=? == syntax eq and syntax prop eq (define (type=? t1 t2) - (let ([k1 (typeof t1)][k2 (typeof 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)) @@ -81,7 +81,7 @@ (define-base-type Float : ★) (define-base-type Char : ★) -(define-internal-type-constructor →) ; defines →- +(define-internal-type-constructor → #:arity >= 0) ; defines →- (define-kinded-syntax (→ ty ...+) ≫ [⊢ ty ≫ ty- ⇒ (~★ . _)] ... -------- diff --git a/turnstile/examples/tests/rackunit-typechecking.rkt b/turnstile/examples/tests/rackunit-typechecking.rkt index 388d27c..4c60084 100644 --- a/turnstile/examples/tests/rackunit-typechecking.rkt +++ b/turnstile/examples/tests/rackunit-typechecking.rkt @@ -23,7 +23,7 @@ ;; duplicate code to avoid redundant expansions [(_ e tag:id τ-expected (~or ⇒ ->) v) #:with e+ (expand/df #'(add-expected e τ-expected)) - #:with τ (typeof #'e+ #:tag (stx->datum #'tag)) + #:with τ (detach #'e+ (stx->datum #'tag)) #:fail-unless (typecheck? #'τ ((current-type-eval) #'τ-expected)) (format "Expression ~a [loc ~a:~a] has type ~a, expected ~a" @@ -31,7 +31,7 @@ (type->str #'τ) (type->str #'τ-expected)) (syntax/loc stx (check-equal? e+ (add-expected v τ-expected)))] [(_ e tag:id τ-expected) - #:with τ (typeof (expand/df #'(add-expected e τ-expected)) #:tag (stx->datum #'tag)) + #:with τ (detach (expand/df #'(add-expected e τ-expected)) (stx->datum #'tag)) #:fail-unless (typecheck? #'τ ((current-type-eval) #'τ-expected)) (format diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt index 27a5cce..a7ce5b6 100644 --- a/turnstile/turnstile.rkt +++ b/turnstile/turnstile.rkt @@ -100,7 +100,7 @@ #'(~and e-tmp (~parse (~and tag-prop.e-pat ... tag-pat) - (typeof #'e-tmp #:tag 'tag)))]) + (detach #'e-tmp 'tag)))]) (define-splicing-syntax-class ⇒-prop/conclusion #:datum-literals (⇒) #:attributes (tag tag-expr) @@ -114,7 +114,7 @@ ([k (in-list (syntax->list #'[tag-prop.tag ...]))] [v (in-list (syntax->list #'[tag-prop.tag-expr ...]))]) (with-syntax ([tag-expr tag-expr] [k k] [v v]) - #'(assign-type tag-expr #:tag 'k v)))]) + #'(attach tag-expr 'k ((current-type-eval) v))))]) (define-splicing-syntax-class ⇐-prop #:datum-literals (⇐ :) #:attributes (τ-stx e-pat) @@ -307,7 +307,7 @@ ([k (in-list (syntax->list #'[props.tag ...]))] [v (in-list (syntax->list #'[props.tag-expr ...]))]) (with-syntax ([body body] [k k] [v v]) - #'(assign-type body #:tag 'k v)))] + #'(attach body 'k ((current-type-eval) v))))] ;; ⇒ conclusion, implicit pat [pattern (~or [⊢ e-stx props:⇒-props/conclusion] [⊢ [e-stx props:⇒-props/conclusion]])