turnstile.rkt (23282B)
1 #lang racket/base 2 3 (provide (except-out (all-from-out macrotypes/typecheck) 4 -define-typed-syntax -define-syntax-category) 5 define-typed-syntax 6 define-typed-variable-syntax 7 define-syntax-category 8 (rename-out [define-typed-syntax define-typerule] 9 [define-typed-syntax define-syntax/typecheck]) 10 (for-syntax syntax-parse/typecheck 11 ~typecheck ~⊢ 12 (rename-out 13 [syntax-parse/typecheck syntax-parse/typed-syntax]))) 14 15 (require (except-in (rename-in 16 macrotypes/typecheck 17 [define-typed-syntax -define-typed-syntax] 18 [define-syntax-category -define-syntax-category]) 19 #%module-begin)) 20 21 (module typecheck+ racket/base 22 (provide (all-defined-out)) 23 (require (for-meta -1 (except-in macrotypes/typecheck #%module-begin)) 24 (only-in lens/common lens-view lens-set) 25 (only-in lens/private/syntax/stx stx-flatten/depth-lens)) 26 ;; infer/depth returns a list of three values: 27 ;; tvxs- ; a stx-list of the expanded versions of type variables in the tvctx 28 ;; xs- ; a stx-list of the expanded versions of variables in the ctx 29 ;; es*- ; a nested list a depth given by the depth argument, with the same structure 30 ;; ; as es*, containing the expanded es*, with the types attached 31 (define (infer/depth #:ctx ctx #:tvctx tvctx depth es* origs* 32 #:tag [tag (current-tag)]) 33 (define flat (stx-flatten/depth-lens depth)) 34 (define es (lens-view flat es*)) 35 (define origs (lens-view flat origs*)) 36 (define/with-syntax [tvxs- xs- es- _] 37 (infer #:tvctx tvctx #:ctx ctx (stx-map pass-orig es origs) #:tag tag)) 38 (define es*- (lens-set flat es* #`es-)) 39 (list #'tvxs- #'xs- es*-)) 40 ;; infers/depths 41 (define (infers/depths clause-depth tc-depth tvctxs/ctxs/ess/origss* 42 #:tag [tag (current-tag)]) 43 (define flat (stx-flatten/depth-lens clause-depth)) 44 (define tvctxs/ctxs/ess/origss 45 (lens-view flat tvctxs/ctxs/ess/origss*)) 46 (define tcs 47 (for/list ([tvctx/ctx/es/origs (in-list (stx->list tvctxs/ctxs/ess/origss))]) 48 (match-define (list tvctx ctx es origs) 49 (stx->list tvctx/ctx/es/origs)) 50 (infer/depth #:tvctx tvctx #:ctx ctx tc-depth es origs #:tag tag))) 51 (define res 52 (lens-set flat tvctxs/ctxs/ess/origss* tcs)) 53 res) 54 (define (raise-⇐-expected-type-error ⇐-stx body expected-type existing-type) 55 (raise-syntax-error 56 '⇐ 57 (format (string-append "body already has a type other than the expected type\n" 58 " body: ~s\n" 59 " expected-type: ~a\n" 60 " existing-type: ~a\n") 61 (syntax->datum body) 62 (type->str expected-type) 63 (type->str existing-type)) 64 ⇐-stx 65 body))) 66 (module syntax-classes racket/base 67 (provide (all-defined-out)) 68 (require (for-meta 0 (submod ".." typecheck+)) 69 (for-meta -1 (submod ".." typecheck+) 70 (except-in macrotypes/typecheck #%module-begin mk-~ mk-?) 71 "mode.rkt") 72 (for-meta -2 (except-in macrotypes/typecheck #%module-begin))) 73 (define-syntax-class --- 74 [pattern dashes:id 75 #:do [(define str-dashes (symbol->string (syntax->datum #'dashes)))] 76 #:fail-unless (for/and ([d (in-string str-dashes)]) 77 (char=? #\- d)) 78 "expected a separator consisting of dashes" 79 #:fail-unless (>= (string-length str-dashes) 3) 80 "expected a separator of three or more dashes"]) 81 (define-syntax-class elipsis 82 [pattern (~literal ...)]) 83 84 ;; with-depth : Any (Stx-Listof Elipsis) -> Any 85 (define (with-depth stx elipses) 86 (cond [(stx-null? elipses) stx] 87 [else 88 (with-depth (list stx (stx-car elipses)) 89 (stx-cdr elipses))])) 90 91 ;; add-lists : Any Natural -> Any 92 (define (add-lists stx n) 93 (cond [(zero? n) stx] 94 [else (add-lists (list stx) (sub1 n))])) 95 96 (define-splicing-syntax-class props 97 [pattern (~and (~seq stuff ...) (~seq (~seq k:id v) ...))]) 98 (define-splicing-syntax-class ⇒-prop 99 #:datum-literals (⇒) 100 #:attributes (e-pat) 101 [pattern (~or (~seq ⇒ tag-pat ; implicit tag 102 (~parse tag #',(current-tag)) 103 (tag-prop:⇒-prop) ...) 104 (~seq ⇒ tag:id tag-pat (tag-prop:⇒-prop) ...)) ; explicit tag 105 #:with e-tmp (generate-temporary) 106 #:with e-pat 107 #'(~and e-tmp 108 (~parse 109 (~and tag-prop.e-pat ... tag-pat) 110 (detach #'e-tmp `tag)))]) 111 (define-splicing-syntax-class ⇒-prop/conclusion 112 #:datum-literals (⇒) 113 #:attributes (tag tag-expr) 114 [pattern (~or (~seq ⇒ tag-stx ; implicit tag 115 (~parse tag #',(current-tag)) 116 (~parse (tag-prop.tag ...) #'()) 117 (~parse (tag-prop.tag-expr ...) #'())) 118 (~seq ⇒ tag:id tag-stx (tag-prop:⇒-prop/conclusion) ...)) 119 #:with tag-expr 120 (for/fold ([tag-expr #'#`tag-stx]) 121 ([k (in-stx-list #'[tag-prop.tag ...])] 122 [v (in-stx-list #'[tag-prop.tag-expr ...])]) 123 (with-syntax ([tag-expr tag-expr] [k k] [v v]) 124 #'(attach tag-expr `k ((current-ev) v))))]) 125 (define-splicing-syntax-class ⇐-prop 126 #:datum-literals (⇐) 127 #:attributes (τ-stx e-pat) 128 [pattern (~or (~seq ⇐ τ-stx (~parse tag #',(current-tag))) 129 (~seq ⇐ tag:id τ-stx)) 130 #:with e-tmp (generate-temporary) 131 #:with τ-tmp (generate-temporary) 132 #:with τ-exp (generate-temporary) 133 #:with e-pat 134 #`(~and e-tmp 135 (~parse τ-exp (get-expected-type #'e-tmp)) 136 (~parse τ-tmp (detach #'e-tmp `tag)) 137 (~parse 138 (~post 139 (~fail #:when (and (not (check? #'τ-tmp #'τ-exp)) 140 (get-orig #'e-tmp)) 141 (typecheck-fail-msg/1 #'τ-exp #'τ-tmp #'e-tmp))) 142 (get-orig #'e-tmp)))]) 143 (define-splicing-syntax-class ⇒-props 144 #:attributes (e-pat) 145 [pattern (~seq :⇒-prop)] 146 [pattern (~seq (p:⇒-prop) ...) 147 #:with e-pat #'(~and p.e-pat ...)]) 148 (define-splicing-syntax-class ⇐-props 149 #:attributes (τ-stx e-pat) 150 [pattern (~seq :⇐-prop)] 151 [pattern (~seq (p:⇐-prop) (p2:⇒-prop) ...) 152 #:with τ-stx #'p.τ-stx 153 #:with e-pat #'(~and p.e-pat p2.e-pat ...)]) 154 (define-splicing-syntax-class ⇒-props/conclusion 155 #:attributes ([tag 1] [tag-expr 1]) 156 [pattern (~seq p:⇒-prop/conclusion) 157 #:with [tag ...] #'[p.tag] 158 #:with [tag-expr ...] #'[p.tag-expr]] 159 [pattern (~seq (:⇒-prop/conclusion) ...+)]) 160 (define-splicing-syntax-class id+props+≫ 161 #:datum-literals (≫) 162 #:attributes ([x- 1] [ctx 1]) 163 [pattern (~seq (~and X:id (~not _:elipsis))) 164 #:with [x- ...] #'[_] 165 #:with [ctx ...] #'[[X :: #%type]]] 166 [pattern (~seq X:id ooo:elipsis) 167 #:with [x- ...] #'[_ ooo] 168 #:with [ctx ...] #'[[X :: #%type] ooo]] 169 [pattern (~seq [x:id ≫ x--:id props:props]) 170 #:with [x- ...] #'[x--] 171 #:with [ctx ...] #'[[x props.stuff ...]]] 172 [pattern (~seq [x:id ≫ x--:id props:props] ooo:elipsis) 173 #:with [x- ...] #'[x-- ooo] 174 #:with [ctx ...] #'[[x props.stuff ...] ooo]]) 175 (define-splicing-syntax-class id-props+≫* 176 #:attributes ([x- 1] [ctx 1]) 177 [pattern (~seq ctx1:id+props+≫ ...) 178 #:with [x- ...] #'[ctx1.x- ... ...] 179 #:with [ctx ...] #'[ctx1.ctx ... ...]]) 180 (define-syntax-class tc-elem 181 #:datum-literals (⊢ ⇒ ⇐ ≫) 182 #:attributes (e-stx e-stx-orig e-pat) 183 [pattern [e-stx ≫ e-pat* props:⇒-props] 184 #:with e-stx-orig #'e-stx 185 #:with e-pat #'(~and props.e-pat e-pat*)] 186 [pattern [e-stx* ≫ e-pat* props:⇐-props] 187 #:with e-tmp (generate-temporary #'e-pat*) 188 #:with τ-tmp (generate-temporary 'τ) 189 #:with τ-exp-tmp (generate-temporary 'τ_expected) 190 #:with e-stx #'(add-expected e-stx* props.τ-stx) 191 #:with e-stx-orig #'e-stx* 192 #:with e-pat #'(~and props.e-pat e-pat*)]) 193 (define-splicing-syntax-class tc 194 #:attributes (depth es-stx es-stx-orig es-pat) 195 [pattern (~seq tc:tc-elem ooo:elipsis ...) 196 #:with depth (stx-length #'[ooo ...]) 197 #:with es-stx (with-depth #'tc.e-stx #'[ooo ...]) 198 #:with es-stx-orig (with-depth #'tc.e-stx-orig #'[ooo ...]) 199 #:with es-pat 200 #`(~post 201 #,(with-depth #'tc.e-pat #'[ooo ...]))]) 202 (define-syntax-class tc* 203 #:attributes (depth es-stx es-stx-orig es-pat wrap-computation) 204 [pattern tc:tc-elem 205 #:with depth 0 206 #:with es-stx #'tc.e-stx 207 #:with es-stx-orig #'tc.e-stx-orig 208 #:with es-pat #'tc.e-pat 209 #:attr wrap-computation (λ (stx) stx)] 210 [pattern (tc:tc ... opts:tc-post-options ...) 211 #:do [(define ds (stx-map syntax-e #'[tc.depth ...])) 212 (define max-d (apply max 0 ds))] 213 #:with depth (add1 max-d) 214 #:with [[es-stx* es-stx-orig* es-pat*] ...] 215 (for/list ([tc-es-stx (in-stx-list #'[tc.es-stx ...])] 216 [tc-es-stx-orig (in-stx-list #'[tc.es-stx-orig ...])] 217 [tc-es-pat (in-stx-list #'[tc.es-pat ...])] 218 [d (in-list ds)]) 219 (list 220 (add-lists tc-es-stx (- max-d d)) 221 (add-lists tc-es-stx-orig (- max-d d)) 222 (add-lists tc-es-pat (- max-d d)))) 223 #:with es-stx #'[es-stx* ...] 224 #:with es-stx-orig #'[es-stx-orig* ...] 225 #:with es-pat #'[es-pat* ...] 226 #:attr wrap-computation 227 (λ (stx) 228 (foldr (λ (fun stx) (fun stx)) 229 stx 230 (attribute opts.wrap)))]) 231 (define-splicing-syntax-class tc-post-options 232 #:attributes (wrap) 233 [pattern (~seq #:mode mode-expr) 234 #:attr wrap (λ (stx) #`(with-mode mode-expr #,stx))] 235 [pattern (~seq #:submode fn-expr) 236 #:attr wrap (λ (stx) #`(with-mode (fn-expr (current-mode)) #,stx))] 237 ) 238 (define-splicing-syntax-class tc-clause 239 #:attributes (pat) 240 #:datum-literals (⊢) 241 [pattern (~or (~seq [⊢ . tc:tc*] ooo:elipsis ... 242 (~parse ((ctx.x- ctx.ctx tvctx.x- tvctx.ctx) ...) #'())) 243 (~seq [ctx:id-props+≫* ⊢ . tc:tc*] ooo:elipsis ... 244 (~parse ((tvctx.x- tvctx.ctx) ...) #'())) 245 (~seq [(ctx:id-props+≫*) ⊢ . tc:tc*] ooo:elipsis ... 246 (~parse ((tvctx.x- tvctx.ctx) ...) #'())) 247 (~seq [(tvctx:id-props+≫*) (ctx:id-props+≫*) ⊢ . tc:tc*] ooo:elipsis ...)) 248 #:with clause-depth (stx-length #'[ooo ...]) 249 #:with tcs-pat 250 (with-depth 251 #'[(tvctx.x- ...) (ctx.x- ...) tc.es-pat] 252 #'[ooo ...]) 253 #:with tvctxs/ctxs/ess/origs 254 (with-depth 255 #`[(tvctx.ctx ...) (ctx.ctx ...) tc.es-stx tc.es-stx-orig] 256 #'[ooo ...]) 257 #:with inf #'(infers/depths 'clause-depth 258 'tc.depth 259 #`tvctxs/ctxs/ess/origs 260 #:tag (current-tag)) 261 #:with inf+ ((attribute tc.wrap-computation) #'inf) 262 #:with pat #`(~post (~post (~parse tcs-pat inf+)))] 263 ) 264 (define-splicing-syntax-class clause 265 #:attributes (pat) 266 #:datum-literals (τ⊑ τ=) ; TODO: drop the τ in τ⊑ and τ= 267 [pattern :tc-clause] 268 [pattern [a τ⊑ b] 269 #:with pat 270 #'(~post 271 (~fail #:unless (check? #'a #'b) 272 (typecheck-fail-msg/1/no-expr #'b #'a)))] 273 [pattern [a τ⊑ b #:for e] 274 #:with pat 275 #'(~post 276 (~fail #:unless (check? #'a #'b) 277 (typecheck-fail-msg/1 #'b #'a #'e)))] 278 [pattern (~seq [a τ⊑ b] ooo:elipsis) 279 #:with pat 280 #'(~post 281 (~fail #:unless (checks? #'[a ooo] #'[b ooo]) 282 (typecheck-fail-msg/multi/no-exprs #'[b ooo] #'[a ooo])))] 283 [pattern (~seq [a τ⊑ b #:for e] ooo:elipsis) 284 #:with pat 285 #'(~post 286 (~fail #:unless (checks? #'[a ooo] #'[b ooo]) 287 (typecheck-fail-msg/multi #'[b ooo] #'[a ooo] #'[e ooo])))] 288 [pattern [a τ= b] 289 #:with pat 290 #'(~post 291 (~fail #:unless ((current=?) #'a #'b) 292 (typecheck-fail-msg/1/no-expr #'b #'a)))] 293 [pattern [a τ= b #:for e] 294 #:with pat 295 #'(~post 296 (~fail #:unless ((current=?) #'a #'b) 297 (typecheck-fail-msg/1 #'b #'a #'e)))] 298 [pattern (~seq [a τ= b] ooo:elipsis) 299 #:with pat 300 #'(~post 301 (~fail #:unless (=s? #'[a ooo] #'[b ooo]) 302 (typecheck-fail-msg/multi/no-exprs #'[b ooo] #'[a ooo])))] 303 [pattern (~seq [a τ= b #:for e] ooo:elipsis) 304 #:with pat 305 #'(~post 306 (~fail #:unless (=s? #'[a ooo] #'[b ooo]) 307 (typecheck-fail-msg/multi #'[b ooo] #'[a ooo] #'[e ooo])))] 308 [pattern (~seq #:when condition:expr) 309 #:with pat 310 #'(~fail #:unless condition)] 311 [pattern (~seq #:with pat*:expr expr:expr) 312 #:with pat 313 #'(~post (~parse pat* expr))] 314 [pattern (~seq #:do [stuff ...]) 315 #:with pat 316 #'(~do stuff ...)] 317 [pattern (~seq #:fail-when condition:expr message:expr) 318 #:with pat 319 #'(~post (~fail #:when condition message))] 320 [pattern (~seq #:fail-unless condition:expr message:expr) 321 #:with pat 322 #'(~post (~fail #:unless condition message))] 323 [pattern (~seq #:mode mode-expr (sub-clause:clause ...)) 324 #:with (the-mode tmp) (generate-temporaries #'(the-mode tmp)) 325 #:with pat 326 #'(~and (~do (define the-mode mode-expr) 327 ((mode-setup-fn the-mode)) 328 (define tmp (current-mode)) 329 (current-mode the-mode)) 330 sub-clause.pat ... 331 (~do (current-mode tmp) 332 ((mode-teardown-fn the-mode))))] 333 [pattern (~seq #:submode fn-expr (sub-clause:clause ...)) 334 #:with (the-mode tmp) (generate-temporaries #'(the-mode tmp)) 335 #:with pat 336 #'(~and (~do (define the-mode (fn-expr (current-mode))) 337 ((mode-setup-fn the-mode)) 338 (define tmp (current-mode)) 339 (current-mode the-mode)) 340 sub-clause.pat ... 341 (~do (current-mode tmp) 342 ((mode-teardown-fn the-mode))))] 343 ) 344 (define-syntax-class last-clause 345 #:datum-literals (⊢ ≫ ≻ ⇒ ⇐) 346 #:attributes ([pat 0] [stuff 1] [body 0]) 347 ;; ⇒ conclusion 348 [pattern (~or [⊢ pat ≫ e-stx props:⇒-props/conclusion] 349 [⊢ [pat ≫ e-stx props:⇒-props/conclusion]]) 350 #:with [stuff ...] #'[] 351 #:with body:expr 352 (for/fold ([body #'(quasisyntax/loc this-syntax e-stx)]) 353 ([k (in-stx-list #'[props.tag ...])] 354 [v (in-stx-list #'[props.tag-expr ...])]) 355 (with-syntax ([body body] [k k] [v v]) 356 #`(attach body `k ((current-ev) v))))] 357 ;; ⇒ conclusion, implicit pat 358 [pattern (~or [⊢ e-stx props:⇒-props/conclusion] 359 [⊢ [e-stx props:⇒-props/conclusion]]) 360 #:with :last-clause #'[⊢ [_ ≫ e-stx . props]]] 361 ;; ⇐ conclusion 362 [pattern [⊢ (~and e-stx (~not [_ ≫ . rst]))] ;; TODO: this current tag isnt right? 363 #:with :last-clause #`[⊢ [_ ≫ e-stx ⇐ #,(datum->stx #'h (current-tag)) _]]] 364 [pattern (~or [⊢ pat* (~seq ≫ e-stx 365 ⇐ τ-pat ; implicit tag 366 (~parse tag #',(current-tag)))] 367 [⊢ pat* ≫ e-stx ⇐ tag:id τ-pat] ; explicit tag 368 [⊢ [pat* (~seq ≫ e-stx 369 ⇐ τ-pat ; implicit tag 370 (~parse tag #',(current-tag)))]] 371 [⊢ [pat* ≫ e-stx ⇐ tag:id τ-pat]]) ; explicit tag 372 #:with stx (generate-temporary 'stx) 373 #:with τ (generate-temporary #'τ-pat) 374 #:with pat 375 #'(~and stx 376 pat* 377 (~parse τ (get-expected-type #'stx)) 378 (~post (~post (~fail #:unless (syntax-e #'τ) 379 (no-expected-type-fail-msg)))) 380 (~parse τ-pat #'τ)) 381 #:with [stuff ...] #'[] 382 #:with body:expr 383 #'(attach (quasisyntax/loc this-syntax e-stx) `tag #`τ)] 384 ;; macro invocations 385 [pattern [≻ e-stx] 386 #:with :last-clause #'[_ ≻ e-stx]] 387 [pattern [pat ≻ e-stx] 388 #:with [stuff ...] #'[] 389 #:with body:expr 390 #'(quasisyntax/loc this-syntax e-stx)] 391 [pattern [#:error msg:expr] 392 #:with :last-clause #'[_ #:error msg]] 393 [pattern [pat #:error msg:expr] 394 #:with [stuff ...] 395 #'[#:fail-unless #f msg] 396 #:with body:expr 397 ;; should never get here 398 #'(error msg)]) 399 (define-splicing-syntax-class pat #:datum-literals (⇐) 400 [pattern (~seq pat) 401 #:attr transform-body identity] 402 [pattern (~or (~seq pat* left:⇐ τ-pat ; implicit tag 403 (~parse tag #',(current-tag))) 404 (~seq pat* left:⇐ tag:id τ-pat)) ; explicit tag 405 #:with stx (generate-temporary 'stx) 406 #:with τ (generate-temporary #'τ-pat) 407 #:with b (generate-temporary 'body) 408 #:with pat 409 #'(~and stx 410 pat* 411 (~parse τ (get-expected-type #'stx)) 412 (~post (~post (~fail #:unless (syntax-e #'τ) 413 (no-expected-type-fail-msg)))) 414 (~parse τ-pat #'τ)) 415 #:attr transform-body 416 (lambda (body) 417 #`(let* ([b #,body][ty-b (detach b `tag)]) 418 (when (and ty-b (not (check? ty-b #'τ))) 419 (raise-⇐-expected-type-error #'left b #'τ ty-b)) 420 (attach b `tag #'τ)))]) 421 (define-syntax-class rule #:datum-literals (≫) 422 [pattern [pat:pat ≫ 423 clause:clause ... 424 :--- 425 last-clause:last-clause] 426 #:with body:expr ((attribute pat.transform-body) #'last-clause.body) 427 #:with norm 428 #'[(~and pat.pat 429 last-clause.pat 430 clause.pat ...) 431 last-clause.stuff ... 432 body]]) 433 (define-splicing-syntax-class stxparse-kws 434 [pattern (~seq (~or (~seq :keyword _) 435 (~seq :keyword)) 436 ...)]) 437 ) 438 (require (for-meta 1 'syntax-classes) 439 (for-meta 2 'syntax-classes)) 440 441 (begin-for-syntax 442 (define-syntax ~typecheck 443 (pattern-expander 444 (syntax-parser 445 [(_ clause:clause ...) 446 #'(~and clause.pat ...)]))) 447 (define-syntax ~⊢ 448 (pattern-expander 449 (syntax-parser 450 [(_ . stuff) 451 #'(~typecheck [⊢ . stuff])]))) 452 453 (define-syntax syntax-parse/typecheck 454 (syntax-parser 455 [(_ stx-expr 456 (~and (~seq kw-stuff ...) :stxparse-kws) 457 rule:rule ...) 458 #'(syntax-parse stx-expr kw-stuff ... rule.norm ...)]))) 459 460 ;; macrotypes/typecheck.rkt already defines (-define-syntax-category type); 461 ;; - just add the "def-named-syntax" part of the def-stx-cat macro below 462 ;; TODO: eliminate code dup with def-named-stx in define-stx-cat below? 463 (define-syntax define-typed-syntax 464 (syntax-parser 465 ;; single-clause def 466 [(_ (rulename:id . pats) . rst) 467 ;; using #'rulename as patvar may cause problems, eg #%app, so use _ 468 #'(define-typed-syntax rulename [(_ . pats) . rst])] 469 ;; multi-clause def 470 ;; - let stx-parse/tychk match :rule (dont double-match) 471 [(_ rulename:id 472 (~and (~seq kw-stuff ...) :stxparse-kws) 473 rule ...+) 474 #'(define-syntax (rulename stx) 475 (parameterize ([current-check-relation (current-typecheck-relation)] 476 [current-ev (current-type-eval)] 477 [current-tag (type-key1)]) 478 (syntax-parse/typecheck stx kw-stuff ... rule ...)))])) 479 480 (define-syntax define-typed-variable-syntax 481 (syntax-parser 482 [(_ (~optional (~seq #:name name:id) #:defaults ([name (generate-temporary '#%var)])) 483 (~and (~seq kw-stuff ...) :stxparse-kws) 484 rule:rule ...+) 485 #'(begin 486 (define-typed-syntax name kw-stuff ... rule ...) 487 (begin-for-syntax 488 (current-var-assign (macro-var-assign #'name))))])) 489 490 (define-syntax define-syntax-category 491 (syntax-parser 492 [(_ name:id) ; default key1 = ': for types 493 #'(define-syntax-category : name)] 494 [(_ key:id name:id) ; default key2 = ':: for kinds 495 #`(define-syntax-category key name #,(mkx2 #'key))] 496 [(_ key1:id name:id key2:id) 497 #:with def-named-syntax (format-id #'name "define-~aed-syntax" #'name) 498 #:with new-check-rel (format-id #'name "current-~acheck-relation" #'name) 499 #:with new-eval (format-id #'name "current-~a-eval" #'name) 500 #'(begin 501 (-define-syntax-category key1 name key2) 502 (define-syntax def-named-syntax 503 (syntax-parser 504 ;; single-clause def 505 [(_ (rulename:id . pats) . rst) 506 ;; #'rulename as a pat var may cause problems, eg #%app, so use _ 507 #'(def-named-syntax rulename [(_ . pats) . rst])] 508 ;; multi-clause def 509 [(_ rulename:id 510 (~and (~seq kw-stuff (... ...)) :stxparse-kws) 511 rule (... ...+)) ; let stx-parse/tychk match :rule stxcls 512 #'(define-syntax (rulename stx) 513 (parameterize ([current-check-relation (new-check-rel)] 514 [current-ev (new-eval)] 515 [current-tag 'key1]) 516 (syntax-parse/typecheck stx kw-stuff (... ...) 517 rule (... ...))))])))]))