adjust redex so that identifiers preserve their syntax-original ness
This commit is contained in:
parent
e4450e2705
commit
605e1b8c89
|
@ -497,10 +497,13 @@
|
||||||
[nts (definition-nts lang stx syn-err-name)]
|
[nts (definition-nts lang stx syn-err-name)]
|
||||||
[judgment (syntax-case stx () [(_ judgment _) #'judgment])])
|
[judgment (syntax-case stx () [(_ judgment _) #'judgment])])
|
||||||
(check-judgment-arity stx judgment)
|
(check-judgment-arity stx judgment)
|
||||||
#`(sort #,(bind-withs syn-err-name '() lang nts (list judgment)
|
(syntax-property
|
||||||
'flatten #`(list (term #,#'tmpl #:lang #,lang)) '() '() #f)
|
#`(sort #,(bind-withs syn-err-name '() lang nts (list judgment)
|
||||||
string<=?
|
'flatten #`(list (term #,#'tmpl #:lang #,lang)) '() '() #f)
|
||||||
#:key (λ (x) (format "~s" x))))]
|
string<=?
|
||||||
|
#:key (λ (x) (format "~s" x)))
|
||||||
|
'disappeared-use
|
||||||
|
(syntax-local-introduce #'form-name)))]
|
||||||
[(_ (not-form-name . _) . _)
|
[(_ (not-form-name . _) . _)
|
||||||
(not (judgment-form-id? #'form-name))
|
(not (judgment-form-id? #'form-name))
|
||||||
(raise-syntax-error #f "expected a judgment form name" stx #'not-form-name)]))
|
(raise-syntax-error #f "expected a judgment form name" stx #'not-form-name)]))
|
||||||
|
|
|
@ -1129,7 +1129,7 @@
|
||||||
'#,(judgment-form-rule-names jf)
|
'#,(judgment-form-rule-names jf)
|
||||||
#,(judgment-form-lang jf))
|
#,(judgment-form-lang jf))
|
||||||
'disappeared-use
|
'disappeared-use
|
||||||
form-name))
|
(syntax-local-introduce form-name)))
|
||||||
|
|
||||||
(define-syntax (render-judgment-form stx)
|
(define-syntax (render-judgment-form stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
|
|
|
@ -1650,7 +1650,7 @@
|
||||||
(syntax-property
|
(syntax-property
|
||||||
#`(make-metafunction #,(term-fn-get-id v))
|
#`(make-metafunction #,(term-fn-get-id v))
|
||||||
'disappeared-use
|
'disappeared-use
|
||||||
(list #'id))
|
(list (syntax-local-introduce #'id)))
|
||||||
(raise-syntax-error
|
(raise-syntax-error
|
||||||
#f
|
#f
|
||||||
"not bound as a metafunction"
|
"not bound as a metafunction"
|
||||||
|
|
|
@ -104,7 +104,8 @@
|
||||||
(defined-term-id? #'x)
|
(defined-term-id? #'x)
|
||||||
(let ([ref (syntax-property
|
(let ([ref (syntax-property
|
||||||
(defined-term-value (syntax-local-value #'x))
|
(defined-term-value (syntax-local-value #'x))
|
||||||
'disappeared-use #'x)])
|
'disappeared-use
|
||||||
|
(syntax-local-introduce #'x))])
|
||||||
(check-id (syntax->datum #'x) stx)
|
(check-id (syntax->datum #'x) stx)
|
||||||
(with-syntax ([v #`(begin
|
(with-syntax ([v #`(begin
|
||||||
#,(defined-check ref "term" #:external #'x)
|
#,(defined-check ref "term" #:external #'x)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user