From d2e93bb1c99c050b319c1f21b6f270669a4729cc Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Tue, 7 Feb 2017 17:18:07 -0500 Subject: [PATCH] generalize infer's ctx to use let* semantics and arbitrary sep+keys - allow lone ids that default to tyvars --- macrotypes/examples/exist.rkt | 5 +- macrotypes/examples/fomega2.rkt | 7 +- macrotypes/examples/fsub.rkt | 7 +- macrotypes/examples/sysf.rkt | 7 +- macrotypes/typecheck.rkt | 459 ++++++------------------- turnstile/examples/exist.rkt | 3 +- turnstile/examples/fomega-no-reuse.rkt | 2 +- turnstile/examples/fomega3.rkt | 2 + turnstile/examples/fsub.rkt | 2 +- turnstile/examples/mlish+adhoc.rkt | 2 +- turnstile/examples/mlish.rkt | 7 +- turnstile/examples/stlc+rec-iso.rkt | 3 +- turnstile/examples/sysf.rkt | 9 +- turnstile/scribblings/reference.scrbl | 36 +- turnstile/turnstile.rkt | 14 +- 15 files changed, 158 insertions(+), 407 deletions(-) diff --git a/macrotypes/examples/exist.rkt b/macrotypes/examples/exist.rkt index 8ca71f4..366f88b 100644 --- a/macrotypes/examples/exist.rkt +++ b/macrotypes/examples/exist.rkt @@ -67,8 +67,5 @@ ;; #:with [e_packed- (~∃ (Y) τ_body)] (infer+erase #'e_packed) #:with τ_x (subst #'X #'Y #'τ_body) - #:with [(X-) (x-) (e-) (τ_e)] - (infer #'(e) - #:tvctx #'([X :: #%type]) - #:ctx #`([x : τ_x])) + #:with [(_ x-) e- τ_e] (infer/ctx+erase #'(X [x : τ_x]) #'e) (⊢ (let- ([x- e_packed-]) e-) : τ_e)]) diff --git a/macrotypes/examples/fomega2.rkt b/macrotypes/examples/fomega2.rkt index 12f017c..0d33c74 100644 --- a/macrotypes/examples/fomega2.rkt +++ b/macrotypes/examples/fomega2.rkt @@ -73,11 +73,8 @@ (define old-typecheck? (current-typecheck-relation)) (define (new-typecheck? t1 t2) - (syntax-parse (list t1 t2) #:datum-literals (:) - [((~∀ ([tv1 : k1]) tbody1) - (~∀ ([tv2 : k2]) tbody2)) - (and (kindcheck? #'k1 #'k2) (typecheck? #'tbody1 #'tbody2))] - [_ (old-typecheck? t1 t2)])) + (and (kindcheck? (kindof t1) (kindof t2)) + (old-typecheck? t1 t2))) (current-typecheck-relation new-typecheck?) ;; must be kind= (and not kindcheck?) since old-kind=? recurs on curr-kind= diff --git a/macrotypes/examples/fsub.rkt b/macrotypes/examples/fsub.rkt index 6a63767..b7d6b00 100644 --- a/macrotypes/examples/fsub.rkt +++ b/macrotypes/examples/fsub.rkt @@ -75,14 +75,13 @@ #:msg "Expected ∀ type, got: ~a" #'any))))])))) (define-typed-syntax Λ #:datum-literals (<:) - [(_ ([tv:id <: τsub:type] ...) e) + [(_ ([X:id <: τsub:type] ...) e) ;; NOTE: store the subtyping relation of tv and τsub in another ;; "environment", ie, a syntax property with another tag: '<: ;; The "expose" function looks for this tag to enforce the bound, ;; as in TaPL (fig 28-1) - #:with ((tv- ...) _ (e-) (τ_e)) - (infer #'(e) #:tvctx #'([tv :: #%type <: τsub] ...)) - (⊢ e- : (∀ ([tv- <: τsub] ...) τ_e))]) + #:with ((X- ...) e- τ_e) (infer/ctx #'([X :: #%type <: τsub] ...) #'e) + (⊢ e- : (∀ ([X- <: τsub] ...) τ_e))]) (define-typed-syntax inst [(_ e τ:type ...) #:with (e- (([tv τ_sub] ...) τ_body)) (⇑ e as ∀) diff --git a/macrotypes/examples/sysf.rkt b/macrotypes/examples/sysf.rkt index dc757d9..3b5a99b 100644 --- a/macrotypes/examples/sysf.rkt +++ b/macrotypes/examples/sysf.rkt @@ -15,11 +15,10 @@ (define-typed-syntax Λ [(_ (tv:id ...) e) - #:with [(tv- ...) e- τ] (infer/tyctx+erase #'([tv :: #%type] ...) #'e) - (⊢ e- : (∀ (tv- ...) τ))]) + #:with [tvs- e- τ-] (infer/ctx #'(tv ...) #'e) + (⊢ e- : (∀ tvs- τ-))]) (define-typed-syntax inst [(_ e τ:type ...) #:with [e- (~∀ tvs τ_body)] (infer+erase #'e) - #:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body) - (⊢ e- : τ_inst)] + (⊢ e- : #,(substs #'(τ.norm ...) #'tvs #'τ_body))] [(_ e) #'e]) diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt index 1d22d43..59bd361 100644 --- a/macrotypes/typecheck.rkt +++ b/macrotypes/typecheck.rkt @@ -202,6 +202,9 @@ ;; e.g., Stx = expression, Tag = ':, Val = Type stx (define (attach stx tag v) (set-stx-prop/preserved stx tag v)) + (define (attachs stx tags vs #:ev [ev (λ (x) x)]) + (for/fold ([stx stx]) ([t (in-list tags)] [v (in-stx-list vs)]) + (attach stx t (ev v)))) ;; detach : Stx Tag -> Val ;; Retrieves Val at Tag stx prop on Stx. ;; If Val is a non-empty list, return first element, otherwise return Val. @@ -418,9 +421,8 @@ modes)])))) ;; base types -------------------------------------------------------- (define-syntax define-base-type - (syntax-parser - [(_ (~var τ id)) ; default to 'key2 and #%tag - #'(define-base-type τ key2 #%tag)] + (syntax-parser ; default = 'key2 + #%tag + [(_ (~var τ id)) #'(define-base-type τ key2 #%tag)] [(_ (~var τ id) new-key2 new-#%tag) #:with τ? (mk-? #'τ) #:with τ-expander (mk-~ #'τ) @@ -470,8 +472,6 @@ ;; - does not attach a kind to itself (define-syntax define-internal-type-constructor (syntax-parser -; [(_ (~var x id) . rst) -; #'(define-basic-checked-stx x key2 type #:no-attach-kind . rst)])) [(_ (~var τ id) (~or (~optional ; variances @@ -486,7 +486,6 @@ (~seq #:extra-info extra-info) #:name "#:extra-info keyword" #:defaults ([extra-info #'void]))) (... ...)) -; #:with #%kind (mk-#% #'kind) #:with τ? (mk-? #'τ) #:with τ- (mk-- #'τ) #:with τ-expander (mk-~ #'τ) @@ -517,7 +516,7 @@ ; τ- is an internal constructor: ; It does not validate inputs and does not attach a kind, ; ie, it won't be recognized as a valid type, the programmer - ; must implement their own kind system + ; must implement their own kind system on top (define-syntax (τ- stx) (syntax-parse stx [(_ . args) @@ -535,10 +534,8 @@ #:with τ- (mk-- #'τ) #'(begin (define-internal-type-constructor τ . other-options) -; #'(define-basic-checked-stx x key2 type . rst)])) (define-syntax (τ stx) (syntax-parse stx -; [(~var _ id) (add-orig (syntax/loc stx τ-) stx)] ; defer to τ- error [(_ . args) #:fail-unless (op (stx-length #'args) n) (format @@ -577,12 +574,14 @@ #:with τ-expander (mk-~ #'τ) #:with τ-internal (generate-temporary #'τ) #`(begin - (begin-for-syntax ; ------------------------------------------- + (begin-for-syntax (define (τ? t) (syntax-parse t [(~Any/bvs (~literal τ-internal) _ . _) #t] [_ #f])) + ;; cannot deal with annotations bc τ- has no knowledge of + ;; its kind (define-syntax τ-expander (pattern-expander (syntax-parser @@ -629,13 +628,12 @@ #'expanded-τ) bvs-pat . pat))]))) (define arg-vars arg-variances-stx)) - ; end define-internal-binding-type begin-for-stx ------------- (define τ-internal (λ _ (raise (exn:fail:type:runtime (format "~a: Cannot use ~a at run time" 'τ 'name) (current-continuation-marks))))) ; τ- is an internal constructor: - ; Tt does not validate inputs and does not attach a kind, + ; It does not validate inputs and does not attach a kind, ; ie, it won't be recognized as a valid type, the programmer ; must implement their own kind system (define-syntax (τ- stx) @@ -663,13 +661,11 @@ (... ...) . (~and other-options (~not ((~or #:arity #:bvs #:arr) . _)))) -; #'(define-binding-checked-stx x key2 type . rst)])))])) #:with τ- (mk-- #'τ) #`(begin (define-internal-binding-type τ . other-options) (define-syntax (τ stx) (syntax-parse stx -; [(~var _ id) (add-orig (syntax/loc stx τ-) stx)] ; defer to τ- error [(_ (~and bvs (~or (bv:id (... (... ...))) (~and (~fail #:unless #,(attribute has-annotations?)) @@ -713,6 +709,34 @@ ;; pre-declare all type-related functions and forms (define-syntax-category type) +;; TODO: move these into define-syntax-category? +(define-syntax typed-out + (make-provide-pre-transformer + (lambda (stx modes) + (syntax-parse stx #:datum-literals (:) + ;; cannot write ty:type bc provides might precede type def + [(_ (~and (~or (~and [out-x:id (~optional :) ty] (~parse x #'out-x)) + [[x:id (~optional :) ty] out-x:id])) ...) + #:with (x/tc ...) (generate-temporaries #'(x ...)) + #:when (stx-map + syntax-local-lift-module-end-declaration + ;; use define-primop to validate type + #'((define-primop x/tc x ty) ...)) + (pre-expand-export (syntax/loc stx (rename-out [x/tc out-x] ...)) + modes)])))) + +;; colon is optional to make it easier to use define-primop in macros +(define-syntax define-primop + (syntax-parser #:datum-literals (:) + [(define-primop op:id (~optional :) τ) + #:with op- (format-id #'op "~a-" #'op) + #'(define-primop op op- τ)] + [(define-primop op/tc:id (~optional #:as) op:id (~optional :) τ:type) + ; rename-transformer doesnt seem to expand at the right time + ; - op still has no type in #%app + #'(define-syntax op/tc + (make-variable-like-transformer (assign-type #'op #'τ)))])) + ;; generic, type-agnostic parameters ;; Use in code that is generic over types and kinds, e.g., in #lang Turnstile (begin-for-syntax @@ -726,12 +750,14 @@ (define (check? x1 x2) ((current-check-relation) x1 x2)) (define (checks? xs1 xs2) ; map current-check-relation pairwise of lists (and (stx-length=? xs1 xs2) (stx-andmap check? xs1 xs2))) - ;; (define current-attach (make-parameter assign-type)) - ;; (define current-detach (make-parameter typeof)) (define current-ev (make-parameter (current-type-eval))) (define current-tag (make-parameter (type-key1)))) ;; type assignment utilities -------------------------------------------------- +(define-syntax (let*-syntax stx) + (syntax-parse stx + [(_ () . body) #'(let-syntax () . body)] + [(_ (b . bs) . es) #'(let-syntax (b) (let*-syntax bs . es))])) (begin-for-syntax ;; Type assignment macro (ie assign-type) for nicer syntax (define-syntax (⊢ stx) @@ -743,41 +769,24 @@ [(_ e tag τ) #'(fast-assign-type #`e #`τ)] [(_ e τ) #'(⊢/no-teval e : τ)])) - ;; Actual type assignment function. - ;; assign-type Type -> Syntax - ;; Attaches type τ to (expanded) expression e. - ;; - eval here so all types are stored in canonical form - ;; - syntax-local-introduce fixes marks on types - ;; which didnt get marked bc they were syntax properties - #;(define (fast-assign-type e τ #:tag [tag ':]) - (set-stx-prop/preserved e tag (syntax-local-introduce τ))) - #;(define (assign-type e τ #:tag [tag ':]) - (fast-assign-type e ((current-type-eval) τ) #:tag tag)) - - (define (add-expected-type e τ) + ;; functions for manipulating "expected type" + (define (add-expected-type e τ) (if (and (syntax? τ) (syntax-e τ)) (set-stx-prop/preserved e 'expected-type τ) ; dont type-eval?, ie expand? e)) (define (get-expected-type e) (get-stx-prop/cd*r e 'expected-type)) + + ;; TODO: remove? only used by macrotypes/examples/infer.rkt (define (add-env e env) (set-stx-prop/preserved e 'env env)) (define (get-env e) (syntax-property e 'env)) - ;; typeof : Syntax -> Type or #f - ;; Retrieves type of given stx, or #f if input has not been assigned a type. - #;(define (typeof stx #:tag [tag ':]) - (get-stx-prop/car stx tag)) - - ;; get-stx-prop/car : Syntax Any -> Any - #;(define (get-stx-prop/car stx tag) - (define v (syntax-property stx tag)) - (if (cons? v) (car v) v)) - (define (mk-tyvar X) (attach X 'tyvar #t)) (define (tyvar? X) (syntax-property X 'tyvar)) (define type-pat "[A-Za-z]+") + ;; TODO: remove this? only benefit is single control point for current-promote ;; - infers type of e ;; - checks that type of e matches the specified type ;; - erases types in e @@ -849,19 +858,39 @@ #'(τ_e (... ...))) #'res])])) + ;; -------------------------------------------------------------------------- + ;; "infer" function for expanding/computing type of an expression + + ;; matches arbitrary number of nexted (expanded) let-stxs + (define-syntax ~let*-syntax + (pattern-expander + (syntax-parser + [(_ . pat) + #:with the-stx (generate-temporary) + #'(~and the-stx + (~parse pat (let L ([stxs #'(the-stx)]) + (syntax-parse stxs + [(((~literal let-values) () + ((~literal let-values) () + . rst))) + (L #'rst)] + [es #'es]))))]))) + ;; basic infer function with no context: ;; infers the type and erases types in an expression (define (infer+erase e #:tag [tag (current-tag)] #:expa [expa expand/df]) (define e+ (expa e)) (list e+ (detach e+ tag))) ;; infers the types and erases types in multiple expressions - (define (infers+erase es #:tag [tag (current-tag)]) - (stx-map (λ (e) (infer+erase e #:tag tag)) es)) + (define (infers+erase es #:tag [tag (current-tag)] #:expa [expa expand/df]) + (stx-map (λ (e) (infer+erase e #:tag tag #:expa expa)) es)) - ;; This is the main "infer" function. All others are defined in terms of this. + ;; This is the main "infer" function. Most others are defined in terms of this. ;; It should be named infer+erase but leaving it for now for backward compat. - ;; ctx = vars and their types (or other props, denoted with "sep") - ;; tvctx = tyvars and their kinds + ;; ctx = vars and their types (or or any props, denoted with any "sep") + ;; - each x in ctx is in scope for subsequent xs + ;; - ie, dont need separate ctx and tvctx + ;; - keep tvctx bc it's often useful to separate the returned Xs- ;; TODO: infer currently tries to be generic over types and kinds ;; but I'm not sure it properly generalizes ;; eg, what if I need separate type-eval and kind-eval fns? @@ -871,36 +900,32 @@ #:expa [expa expand/df] ; used to expand e #:tev [tev #'(current-type-eval)] ; type-eval (τ in ctx) #:key [kev #'(current-type-eval)]) ; kind-eval (tvk in tvctx) - (syntax-parse ctx - [([x sep τ] ...) ; dont expand yet bc τ may have references to tvs - #:with ([tv (~seq tvsep:id tvk) ...] ...) tvctx + (syntax-parse ctx + [((~or X:id [x:id (~seq sep:id τ) ...]) ...) ; dont expand; τ may reference to tv + #:with (~or (~and (tv:id ...) + (~parse ([(tvsep ...) (tvk ...)] ...) + (stx-map (λ _ #'[(::) (#%type)]) #'(tv ...)))) + ([tv (~seq tvsep:id tvk) ...] ...)) + tvctx #:with (e ...) es - #:with - ; old expander pattern (leave commented out) - #;((~literal #%plain-lambda) tvs+ - ((~literal #%expression) - ((~literal #%plain-lambda) xs+ - ((~literal letrec-syntaxes+values) stxs1 () - ((~literal letrec-syntaxes+values) stxs2 () - ((~literal #%expression) e+) ...))))) - ; new expander pattern - ((~literal #%plain-lambda) tvs+ - ((~literal let-values) () ((~literal let-values) () - ((~literal #%expression) - ((~literal #%plain-lambda) xs+ - ((~literal let-values) () ((~literal let-values) () - ((~literal #%expression) e+) ... (~literal void)))))))) - (expa + #:with ((~literal #%plain-lambda) tvs+ + (~let*-syntax + ((~literal #%expression) + ((~literal #%plain-lambda) xs+ + (~let*-syntax + ((~literal #%expression) e+) ... (~literal void)))))) + (expa #`(λ (tv ...) - (let-syntax ([tv (make-rename-transformer - (mk-tyvar - (for/fold ([tv-id #'tv]) - ([s (in-list '(tvsep ...))] - [k (in-stx-list #'(tvk ...))]) - (attach tv-id s (#,kev k)))))] ...) - (λ (x ...) - (let-syntax ([x (make-variable-like-transformer - (attach #'x 'sep (#,tev #'τ)))] ...) + (let*-syntax ([tv (make-rename-transformer + (mk-tyvar + (attachs #'tv '(tvsep ...) #'(tvk ...) + #:ev #,kev)))] ...) + (λ (X ... x ...) + (let*-syntax ([X (make-variable-like-transformer + (mk-tyvar (attach #'X ':: (#,kev #'#%type))))] ... + [x (make-variable-like-transformer + (attachs #'x '(sep ...) #'(τ ...) + #:ev #,tev))] ...) (#%expression e) ... void))))) (list #'tvs+ #'xs+ #'(e+ ...) @@ -925,6 +950,8 @@ (define (infers/tyctx+erase ctx es #:tag [tag (current-tag)]) (syntax-parse (infer es #:tvctx ctx #:tag tag) [(tvs+ _ es+ tys) (list #'tvs+ #'es+ #'tys)])) + (define infer/tyctx infer/tyctx+erase) + (define infer/ctx infer/ctx+erase) (define current-promote (make-parameter (λ (t) t))) @@ -939,6 +966,7 @@ (define (expand/df e) (local-expand e 'expression null)) + ;; TODO: move these into define-syntax-category? ;; typecheck-fail-msg/1 : Type Type Stx -> String (define (typecheck-fail-msg/1 τ_expected τ_given expression) (format "type mismatch: expected ~a, given ~a\n expression: ~s" @@ -988,6 +1016,7 @@ (struct exn:fail:type:check exn:fail:user ()) (struct exn:fail:type:infer exn:fail:user ()) + ;; TODO: deprecate this? can we rely on stx-parse instead? ;; type-error #:src Syntax #:msg String Syntax ... ;; usage: ;; type-error #:src src-stx @@ -1091,292 +1120,6 @@ (define (get-type-tags ts) (stx-map get-type-tag ts))) -#;(define-syntax define-basic-checked-id-stx - (syntax-parser #:datum-literals (:) - [(_ τ:id key tag) - #:with τ? (mk-? #'τ) - #:with τ-expander (mk-~ #'τ) - #:with τ-internal (generate-temporary #'τ) - #`(begin - (begin-for-syntax - (define (τ? t) - (syntax-parse t - [((~literal #%plain-app) (~literal τ-internal)) #t] - [_ #f])) - (define-syntax τ-expander - (pattern-expander - (syntax-parser - [:id #'((~literal #%plain-app) (~literal τ-internal))] - ; - this case used by ⇑, TODO: remove this case? - ; - but it's also needed when matching a list of types, - ; e.g., in stlc+sub (~Nat τ) - [(_ . rst) - #'(((~literal #%plain-app) (~literal τ-internal)) . rst)])))) - (define τ-internal - (λ () (raise (exn:fail:type:runtime - (format "~a: Cannot use ~a at run time" 'τ 'tag) - (current-continuation-marks))))) - (define-syntax τ - (syntax-parser - [:id - (add-orig - (set-stx-prop/preserved - (syntax/loc this-syntax (τ-internal)) - 'key (expand/df #'tag)) - #'τ)])))])) - -;; The def uses pattern vars "τ" and "kind" but this form is not restricted to -;; only types and kinds, eg, τ can be #'★ and kind can be #'#%kind (★'s type) -#;(define-syntax (define-basic-checked-stx stx) - (syntax-parse stx #:datum-literals (:) - [(_ τ:id key kind - (~or - (~optional (~and #:no-attach-kind (~parse no-attach-kind? #'#t))) - (~optional - (~seq #:arity op n:exact-nonnegative-integer) - #:defaults ([op #'=] [n #'1])) - (~optional (~seq #:arg-variances arg-variances-stx:expr) - #:defaults ([arg-variances-stx - #`(λ (stx-id) - (for/list ([arg (in-list (stx->list (stx-cdr stx-id)))]) - invariant))])) - (~optional (~seq #:extra-info extra-info) - #:defaults ([extra-info #'void]))) ...) - #:with #%kind (mk-#% #'kind) - #:with τ? (mk-? #'τ) - #:with τ- (mk-- #'τ) - #:with τ-expander (mk-~ #'τ) - #:with τ-internal (generate-temporary #'τ) - #`(begin - (begin-for-syntax - (define-syntax τ-expander - (pattern-expander - (syntax-parser - [(_ . pat) - #:with expanded-τ (generate-temporary) - #'(~and expanded-τ - (~Any - (~literal/else τ-internal - (format "Expected ~a type, got: ~a" - 'τ (type->str #'expanded-τ)) - #'expanded-τ) - . pat))]))) - (define arg-variances arg-variances-stx) - (define (τ? t) - (syntax-parse t - [(~Any (~literal τ-internal) . _) #t] - [_ #f]))) - (define τ-internal - (λ _ (raise (exn:fail:type:runtime - (format "~a: Cannot use ~a at run time" 'τ 'kind) - (current-continuation-marks))))) - ; τ- is an internal constructor: - ; - it does not validate inputs and does not attach a kind, - ; ie, it won't be recognized as a valid type unless a kind - ; system is implemented on top - ; - the τ constructor implements a default kind system but τ- - ; is available if the programmer wants to implement their own - (define-syntax (τ- stx) - (syntax-parse stx - [(_ . args) - #:with τ-internal* (add-arg-variances #'τ-internal (arg-variances #'(τ . args))) - (syntax/loc stx - (τ-internal* (λ () (#%expression extra-info) . args)))])) - ; this is the actual constructor - #,@(if (attribute no-attach-kind?) - #'() - #'((define-syntax (τ stx) - (syntax-parse stx - [(_ . args) - #:fail-unless (op (stx-length #'args) n) - (format "wrong number of arguments, expected ~a ~a" - 'op 'n) - #:with ([arg- _] (... ...)) (infers+erase #'args) - ;; the args are validated on the next line, rather than above - ;; to ensure enough stx-parse progress so we get a proper err msg, - ;; ie, "invalid type" instead of "improper tycon usage" - #:with (~! (~var _ kind) (... ...)) #'(arg- (... ...)) - (add-orig - (set-stx-prop/preserved #'(τ- arg- (... ...)) 'key (expand/df #'#%kind)) - stx)] - [_ ;; else fail with err msg - (type-error - #:src stx - #:msg - (string-append - "Improper usage of type constructor ~a: ~a, expected ~a ~a arguments") - #'τ stx #'op #'n)])))))])) - -;; Form for defining *binding* types, kinds, etc. -;; The def uses pattern vars "τ" and "kind" but this form is not restricted to -;; only types and kinds, eg, τ can be #'★ and kind can be #'#%kind (★'s type) -#;(define-syntax (define-binding-checked-stx stx) - (syntax-parse stx - [(_ τ:id key kind - (~or - (~optional (~and #:no-attach-kind (~parse no-attach-kind? #'#t))) - (~optional - (~seq #:arity op n:exact-nonnegative-integer) - #:defaults ([op #'=] [n #'1])) - (~optional - (~seq #:bvs bvs-op bvs-n:exact-nonnegative-integer) - #:defaults ([bvs-op #'>=][bvs-n #'0])) - (~optional - (~seq #:arr (~and kindcon (~parse has-annotations? #'#t))) - #:defaults ([kindcon #'void])) ; default kindcon should never be used - (~optional - (~seq #:arg-variances arg-variances-stx:expr) - #:defaults ([arg-variances-stx - #`(λ (stx-id) - (for/list ([arg (in-list (stx->list (stx-cdr stx-id)))]) - invariant))])) - (~optional - (~seq #:extra-info extra-info) - #:defaults ([extra-info #'void]))) ...) - #:with #%kind (mk-#% #'kind) - #:with τ? (mk-? #'τ) - #:with τ- (mk-- #'τ) - #:with τ-expander (mk-~ #'τ) - #:with τ-internal (generate-temporary #'τ) - #`(begin - (begin-for-syntax - (define-syntax τ-expander - (pattern-expander - (syntax-parser - ; this case used by ⇑, TODO: remove this case? - ;; if has-annotations? - ;; - type has surface shape - ;; (τ ([tv : k] ...) body ...) - ;; - this case parses to pattern - ;; [([tv k] ...) (body ...)] - ;; if not has-annotations? - ;; - type has surface shape - ;; (τ (tv ...) body ...) - ;; - this case parses to pattern - ;; [(tv ...) (body ...)] - [(_ . pat:id) - #:with expanded-τ (generate-temporary) - #:with kindcon-expander (mk-~ #'kindcon) - #'(~and expanded-τ - (~Any/bvs - (~literal/else τ-internal - (format "Expected ~a type, got: ~a" - 'τ (type->str #'expanded-τ)) - #'expanded-τ) - (~and bvs (tv (... (... ...)))) - . rst) - #,(if (attribute has-annotations?) - #'(~and - (~parse (kindcon-expander k (... (... ...))) - (tagoftype #'expanded-τ)) - (~parse pat - #'[([tv k] (... (... ...))) 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, - ;; parses to pattern[(tv ...) . (body ...)] - [(_ bvs-pat . pat) - #:with expanded-τ (generate-temporary) - #'(~and expanded-τ - (~Any/bvs - (~literal/else τ-internal - (format "Expected ~a type, got: ~a" - 'τ (type->str #'expanded-τ)) - #'expanded-τ) - bvs-pat - . pat))]))) - (define arg-variances arg-variances-stx) - (define (τ? t) - (syntax-parse t - [(~Any/bvs (~literal τ-internal) _ . _) - #t] - [_ #f]))) - (define τ-internal - (λ _ (raise (exn:fail:type:runtime - (format "~a: Cannot use ~a at run time" 'τ 'kind) - (current-continuation-marks))))) - ; τ- is an internal constructor: - ; - it does not validate inputs and does not attach a kind, - ; ie, it won't be recognized as a valid type unless a kind - ; system is implemented on top - ; - the τ constructor implements a default kind system but τ- - ; is available if the programmer wants to implement their own - (define-syntax (τ- stx) - (syntax-parse stx - [(_ bvs . args) - #:with τ-internal* (add-arg-variances - #'τ-internal - (arg-variances #'(τ- . args))) ; drop bvs - (syntax/loc stx - (τ-internal* (λ bvs (#%expression extra-info) . args)))])) - ; this is the actual constructor - #,@(if (attribute no-attach-kind?) - #'() - #`((define-syntax (τ stx) - (syntax-parse stx - [(_ (~or (bv:id (... ...)) - (~and (~fail #:unless #,(attribute has-annotations?)) - bvs+ann)) - . args) - #:with bvs+ks (if #,(attribute has-annotations?) - #'bvs+ann - #'([bv :: #%kind] (... ...))) - #:fail-unless (bvs-op (stx-length #'bvs+ks) bvs-n) - (format "wrong number of type vars, expected ~a ~a" - 'bvs-op 'bvs-n) - #:fail-unless (op (stx-length #'args) n) - (format "wrong number of arguments, expected ~a ~a" - 'op 'n) - #:with (bvs- τs- _) (infers/ctx+erase #'bvs+ks #'args) - ;; the args are validated on the next line, rather than above - ;; to ensure enough stx-parse progress so we get a proper err msg, - ;; ie, "invalid type" instead of "improper tycon usage" - #:with (~! (~var _ kind) (... ...)) #'τs- - #:with ([tv (~datum ::) k_arg] (... ...)) #'bvs+ks - #:with k_result (if #,(attribute has-annotations?) - #'(kindcon k_arg (... ...)) - #'#%kind) - (add-orig - (set-stx-prop/preserved #'(τ- bvs- . τs-) 'key (expand/df #'k_result)) - stx)] - ;; else fail with err msg - [_ - (type-error #:src stx - #:msg (string-append - "Improper usage of type constructor ~a: ~a, expected ~a ~a arguments") - #'τ stx #'op #'n)])))))])) - -(define-syntax typed-out - (make-provide-pre-transformer - (lambda (stx modes) - (syntax-parse stx #:datum-literals (:) - ;; cannot write ty:type bc provides might precede type def - [(_ (~and (~or (~and [out-x:id (~optional :) ty] (~parse x #'out-x)) - [[x:id (~optional :) ty] out-x:id])) ...) - #:with (x/tc ...) (generate-temporaries #'(x ...)) - #:when (stx-map - syntax-local-lift-module-end-declaration - ;; use define-primop to validate type - #'((define-primop x/tc x ty) ...)) - (pre-expand-export (syntax/loc stx (rename-out [x/tc out-x] ...)) - modes)])))) - -;; colon is optional to make it easier to use define-primop in macros -(define-syntax define-primop - (syntax-parser #:datum-literals (:) - [(define-primop op:id (~optional :) τ) - #:with op- (format-id #'op "~a-" #'op) - #'(define-primop op op- τ)] - [(define-primop op/tc:id (~optional #:as) op:id (~optional :) τ:type) - ; rename-transformer doesnt seem to expand at the right time - ; - op still has no type in #%app - #'(define-syntax op/tc - (make-variable-like-transformer (assign-type #'op #'τ)))])) - ; substitution (begin-for-syntax (define-syntax ~Any/bvs ; matches any tycon @@ -1404,7 +1147,7 @@ (free-identifier=? #'actual #'lit)) fail-msg) stx))]))) - (define (merge-type-tags stx) ;; TODO: merge other tags + (define (merge-type-tags stx) ;; TODO: merge other tags? (define t (syntax-property stx ':)) (or (and (pair? t) (identifier? (car t)) (identifier? (cdr t)) diff --git a/turnstile/examples/exist.rkt b/turnstile/examples/exist.rkt index 203b0e4..82bed5d 100644 --- a/turnstile/examples/exist.rkt +++ b/turnstile/examples/exist.rkt @@ -65,7 +65,6 @@ ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e ;; [⊢ e_packed ≫ e_packed- ⇒ (~∃ (Y) τ_body)] - #:with τ_x (subst #'X #'Y #'τ_body) - [([X ≫ X- :: #%type]) ([x ≫ x- : τ_x]) ⊢ e ≫ e- ⇒ τ_e] + [X [x ≫ x- : #,(subst #'X #'Y #'τ_body)] ⊢ e ≫ e- ⇒ τ_e] -------- [⊢ (let- ([x- e_packed-]) e-) ⇒ τ_e]) diff --git a/turnstile/examples/fomega-no-reuse.rkt b/turnstile/examples/fomega-no-reuse.rkt index 46cf2e1..12744b2 100644 --- a/turnstile/examples/fomega-no-reuse.rkt +++ b/turnstile/examples/fomega-no-reuse.rkt @@ -169,7 +169,7 @@ [_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]]) (define-typed-syntax (Λ bvs:kind-ctx e) ≫ - [([bvs.x ≫ tv- :: bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e] + [[bvs.x ≫ tv- :: bvs.kind] ... ⊢ e ≫ e- ⇒ τ_e] -------- [⊢ e- ⇒ (∀ ([tv- :: bvs.kind] ...) τ_e)]) diff --git a/turnstile/examples/fomega3.rkt b/turnstile/examples/fomega3.rkt index 08b5af8..c944915 100644 --- a/turnstile/examples/fomega3.rkt +++ b/turnstile/examples/fomega3.rkt @@ -1,6 +1,8 @@ #lang turnstile/lang (extends "fomega.rkt" #:except tyapp tyλ) +;; not current working 2017-02-03 + ; same as fomega2.rkt --- λ and #%app works as both regular and type versions, ; → is both type and kind --- but reuses parts of fomega.rkt, ; ie removes the duplication in fomega2.rkt diff --git a/turnstile/examples/fsub.rkt b/turnstile/examples/fsub.rkt index 393b76c..9f9557e 100644 --- a/turnstile/examples/fsub.rkt +++ b/turnstile/examples/fsub.rkt @@ -79,7 +79,7 @@ ;; environment with a syntax property using another tag: '<: ;; The "expose" function looks for this tag to enforce the bound, ;; as in TaPL (fig 28-1) - [([tv ≫ tv- :: #%type <: τsub] ...) () ⊢ e ≫ e- ⇒ τ_e] + [[tv ≫ tv- :: #%type <: τsub] ... ⊢ e ≫ e- ⇒ τ_e] -------- [⊢ e- ⇒ (∀ ([tv- <: τsub] ...) τ_e)]) (define-typed-syntax (inst e τ:type ...) ≫ diff --git a/turnstile/examples/mlish+adhoc.rkt b/turnstile/examples/mlish+adhoc.rkt index 03d172b..7665d48 100644 --- a/turnstile/examples/mlish+adhoc.rkt +++ b/turnstile/examples/mlish+adhoc.rkt @@ -1713,7 +1713,7 @@ (~=> TCsub ... (~TC [generic-op-expected ty-concrete-op-expected] ...))) _) - (infers/tyctx+erase #'([X :: #%type] ...) #'(TC ... (Name ty ...))) + (infers/tyctx+erase #'(X ...) #'(TC ... (Name ty ...))) ;; this produces #%app bad stx err, so manually call infer for now ;; [([X ≫ X- :: #%type] ...) () ⊢ (TC ... (Name ty ...)) ≫ ;; (TC+ ... diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt index bfb4464..b134612 100644 --- a/turnstile/examples/mlish.rkt +++ b/turnstile/examples/mlish.rkt @@ -850,16 +850,15 @@ #:fail-unless (stx-length=? #'[x ...] #'[τ_in ...]) (format "expected a function of ~a arguments, got one with ~a arguments" (stx-length #'[τ_in ...]) (stx-length #'[x ...])) - [([X ≫ X- :: #%type] ...) ([x ≫ x- : τ_in] ...) ⊢ [body ≫ body- ⇐ τ_out]] + [(X ...) ([x ≫ x- : τ_in] ...) ⊢ [body ≫ body- ⇐ τ_out]] -------- [⊢ (λ- (x- ...) body-)]] [(λ ([x : τ_x] ...) body) ⇐ (~?∀ (V ...) (~ext-stlc:→ τ_in ... τ_out)) ≫ #:with [X ...] (compute-tyvars #'(τ_x ...)) - [([X ≫ X- :: #%type] ...) () ⊢ [τ_x ≫ τ_x- ⇐ :: #%type] ...] + [[X ≫ X- :: #%type] ... ⊢ [τ_x ≫ τ_x- ⇐ :: #%type] ...] [τ_in τ⊑ τ_x- #:for x] ... ;; TODO is there a way to have λs that refer to ids defined after them? - [([V ≫ V- :: #%type] ... [X- ≫ X-- :: #%type] ...) ([x ≫ x- : τ_x-] ...) - ⊢ body ≫ body- ⇐ τ_out] + [(V ... X- ...) ([x ≫ x- : τ_x-] ...) ⊢ body ≫ body- ⇐ τ_out] -------- [⊢ (λ- (x- ...) body-)]] [(λ ([x : τ_x] ...) body) ≫ diff --git a/turnstile/examples/stlc+rec-iso.rkt b/turnstile/examples/stlc+rec-iso.rkt index 4900cd1..3fb33f0 100644 --- a/turnstile/examples/stlc+rec-iso.rkt +++ b/turnstile/examples/stlc+rec-iso.rkt @@ -23,7 +23,6 @@ [⊢ e- ⇒ #,(subst #'τ.norm #'tv #'τ_body)]) (define-typed-syntax (fld τ:type-ann e) ≫ #:with (~μ (tv) τ_body) #'τ.norm - #:with τ_e (subst #'τ.norm #'tv #'τ_body) - [⊢ e ≫ e- ⇐ τ_e] + [⊢ e ≫ e- ⇐ #,(subst #'τ.norm #'tv #'τ_body)] -------- [⊢ e- ⇒ τ.norm]) diff --git a/turnstile/examples/sysf.rkt b/turnstile/examples/sysf.rkt index dde2c79..0412f54 100644 --- a/turnstile/examples/sysf.rkt +++ b/turnstile/examples/sysf.rkt @@ -14,17 +14,14 @@ (define-binding-type ∀) (define-typed-syntax (Λ (tv:id ...) e) ≫ - [([tv ≫ tv- :: #%type] ...) () ⊢ e ≫ e- ⇒ τ] + [[tv ≫ tv- :: #%type] ... ⊢ e ≫ e- ⇒ τ] -------- [⊢ e- ⇒ (∀ (tv- ...) τ)]) (define-typed-syntax inst [(_ e τ:type ...) ≫ [⊢ e ≫ e- ⇒ (~∀ tvs τ_body)] - #:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body) -------- - [⊢ e- ⇒ τ_inst]] - [(_ e) ≫ - -------- - [≻ e]]) + [⊢ e- ⇒ #,(substs #'(τ.norm ...) #'tvs #'τ_body)]] + [(_ e) ≫ --- [≻ e]]) diff --git a/turnstile/scribblings/reference.scrbl b/turnstile/scribblings/reference.scrbl index 7998e86..4328a5f 100644 --- a/turnstile/scribblings/reference.scrbl +++ b/turnstile/scribblings/reference.scrbl @@ -34,7 +34,7 @@ and then press Control-@litchar{\}. @; define-typed-syntax--------------------------------------------------------- @defform*[ - #:literals (≫ ⊢ ⇒ ⇐ ≻ : --------) + #:literals (≫ ⊢ ⇒ ⇐ ≻ --------) ((define-typed-syntax (name-id . pattern) ≫ premise ... -------- @@ -50,7 +50,7 @@ and then press Control-@litchar{\}. premise ... -------- ⇐-conclusion] - [expr-pattern ⇐ key type-pattern ≫ + [expr-pattern ⇐ key pattern ≫ premise ... -------- ⇐-conclusion]] @@ -70,21 +70,22 @@ and then press Control-@litchar{\}. type-relation (code:line @#,racket[syntax-parse] @#,tech:pat-directive)] [ctx (ctx-elem ...)] - [ctx-elem (code:line [id ≫ id : type-template] ooo ...)] + [ctx-elem (code:line [id ≫ id key template ... ...] ooo ...) + (code:line id ooo ...)] [tc (code:line tc-elem ooo ...)] [tc-elem [expr-template ≫ expr-pattern ⇒ type-pattern] - [expr-template ≫ expr-pattern ⇒ key type-pattern] - [expr-template ≫ expr-pattern (⇒ key type-pattern) ooo ...] + [expr-template ≫ expr-pattern ⇒ key pattern] + [expr-template ≫ expr-pattern (⇒ key pattern) ooo ...] [expr-template ≫ expr-pattern ⇐ type-template] - [expr-template ≫ expr-pattern ⇐ key type-template] - [expr-template ≫ expr-pattern (⇐ key type-template) ooo ...]] + [expr-template ≫ expr-pattern ⇐ key template] + [expr-template ≫ expr-pattern (⇐ key template) ooo ...]] [type-relation (code:line [type-template τ= type-template] ooo ...) (code:line [type-template τ= type-template #:for expr-template] ooo ...) (code:line [type-template τ⊑ type-template] ooo ...) (code:line [type-template τ⊑ type-template #:for expr-template] ooo ...)] [conclusion [⊢ expr-template ⇒ type-template] - [⊢ expr-template ⇒ key type-template] - [⊢ expr-template (⇒ key type-template) ooo ...] + [⊢ expr-template ⇒ key template] + [⊢ expr-template (⇒ key template) ooo ...] [≻ expr-template] [#:error expr-template]] [⇐-conclusion [⊢ expr-template]] @@ -104,8 +105,8 @@ declares that expression @racket[e] expands to @racket[e-] and has type outputs. Syntactically, @racket[e] is a syntax template position and @racket[e-] @racket[τ] are syntax pattern positions. -A programmer may use the generalized form @racket[[⊢ e ≫ e- (⇒ key τ) ...]] to -specify propagation of arbitrary values, associated with any number of +A programmer may use the generalized form @racket[[⊢ e ≫ e- (⇒ key pat) ...]] +to specify propagation of arbitrary values, associated with any number of keys. For example, a type and effect system may wish to additionally propagate source locations of allocations and mutations. When no key is specified, @litchar{:}, i.e., the "type" key, is used. Dually, one may write @racket[[⊢ e @@ -113,6 +114,19 @@ source locations of allocations and mutations. When no key is specified, and @racket[τ] are inputs (templates) and only @racket[e-] is an output (pattern). +A context may be specified to the left of the turnstile. A context element has +shape @racket[[⊢ x ≫ x- key pat ... ...]] where @racket[x-] is the expansion of +@racket[x] and the @racket[(key pat) ...] are arbitrary key-value pairs, e.g. a +@litchar{:} key and type pattern. Elements in the context have @racket[let*] +semantics where each binding is in scope for subsequent parts of the +context. This means type and term variables may be in the same context (though +order matters). Nevertheless, Turnstile allows writing two separate contexts, +where bindings in first are in scope for the second. This is often convenient +for separating the context bindings and using their outputs in different forms. + +For convenience, lone identifiers written to the left of the turnstile are +automatically treated as type variables. + The @racket[≻] conclusion form is useful in many scenarios where the rule being implemented may not want to attach type information. E.g., diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt index 5502a10..3b85771 100644 --- a/turnstile/turnstile.rkt +++ b/turnstile/turnstile.rkt @@ -32,7 +32,7 @@ (define origs (lens-view flat origs*)) (define/with-syntax [tvxs- xs- es- _] (infer #:tvctx tvctx #:ctx ctx (stx-map pass-orig es origs) #:tag tag)) - (define es*- (lens-set flat es* #'es-)) + (define es*- (lens-set flat es* #`es-)) (list #'tvxs- #'xs- es*-)) ;; infers/depths (define (infers/depths clause-depth tc-depth tvctxs/ctxs/ess/origss* @@ -156,6 +156,12 @@ (define-splicing-syntax-class id+props+≫ #:datum-literals (≫) #:attributes ([x- 1] [ctx 1]) + [pattern (~seq (~and X:id (~not _:elipsis))) + #:with [x- ...] #'[_] + #:with [ctx ...] #'[[X :: #%type]]] + [pattern (~seq X:id ooo:elipsis) + #:with [x- ...] #'[_ ooo] + #:with [ctx ...] #'[[X :: #%type] ooo]] [pattern (~seq [x:id ≫ x--:id props:props]) #:with [x- ...] #'[x--] #:with [ctx ...] #'[[x props.stuff ...]]] @@ -229,19 +235,19 @@ #'[ooo ...]) #:with tvctxs/ctxs/ess/origs (with-depth - #'[(tvctx.ctx ...) (ctx.ctx ...) tc.es-stx tc.es-stx-orig] + #`[(tvctx.ctx ...) (ctx.ctx ...) tc.es-stx tc.es-stx-orig] #'[ooo ...]) #:with pat #`(~post (~post (~parse tcs-pat - (infers/depths 'clause-depth 'tc.depth #'tvctxs/ctxs/ess/origs + (infers/depths 'clause-depth 'tc.depth #`tvctxs/ctxs/ess/origs #:tag (current-tag)))))] ) (define-splicing-syntax-class clause #:attributes (pat) - #:datum-literals (τ⊑ τ=) ; TODO: drop the τ + #:datum-literals (τ⊑ τ=) ; TODO: drop the τ in τ⊑ and τ= [pattern :tc-clause] [pattern [a τ⊑ b] #:with pat