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

raco setup completes

Browse Source
This commit is contained in:
Stephen Chang 2017-01-30 15:11:57 -05:00
parent 25de3c5f20
commit f825eef92f
7 changed files with 41 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
macrotypes/examples/fomega.rkt
View File

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

2
macrotypes/examples/fomega2.rkt
View File

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

2
macrotypes/examples/infer.rkt
View File

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

55
macrotypes/typecheck.rkt
View File

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

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

@ -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- ⇒ (~★ . _)] ...
--------

4
turnstile/examples/tests/rackunit-typechecking.rkt
View File

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

6
turnstile/turnstile.rkt
View File

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