Moves metafunction construction to later expansion step
This commit is contained in:
parent
2b4f604776
commit
ac7856a377
|
@ -1373,9 +1373,8 @@
|
||||||
(if prev-metafunction
|
(if prev-metafunction
|
||||||
'define-metafunction/extension
|
'define-metafunction/extension
|
||||||
'define-metafunction))])
|
'define-metafunction))])
|
||||||
(define lang-nts
|
|
||||||
;; keep this near the beginning, so it signals the first error (PR 10062)
|
;; keep this near the beginning, so it signals the first error (PR 10062)
|
||||||
(definition-nts #'lang orig-stx syn-error-name))
|
(definition-nts #'lang orig-stx syn-error-name)
|
||||||
(when (null? (syntax-e #'rest))
|
(when (null? (syntax-e #'rest))
|
||||||
(raise-syntax-error syn-error-name "no clauses" orig-stx))
|
(raise-syntax-error syn-error-name "no clauses" orig-stx))
|
||||||
(when prev-metafunction
|
(when prev-metafunction
|
||||||
|
@ -1386,15 +1385,49 @@
|
||||||
(let*-values ([(contract-name dom-ctcs codom-contracts pats)
|
(let*-values ([(contract-name dom-ctcs codom-contracts pats)
|
||||||
(split-out-contract orig-stx syn-error-name #'rest relation?)]
|
(split-out-contract orig-stx syn-error-name #'rest relation?)]
|
||||||
[(name _) (defined-name (list contract-name) pats orig-stx)])
|
[(name _) (defined-name (list contract-name) pats orig-stx)])
|
||||||
|
(when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction)))
|
||||||
|
(raise-syntax-error syn-error-name "the extended and extending metafunctions cannot share a name" orig-stx prev-metafunction))
|
||||||
|
(with-syntax ([(name2 name-predicate) (generate-temporaries (list name name))]
|
||||||
|
[name name])
|
||||||
|
(with-syntax ([defs #`(begin
|
||||||
|
(define-values (name2 name-predicate)
|
||||||
|
(generate-metafunction #,orig-stx
|
||||||
|
lang
|
||||||
|
#,prev-metafunction
|
||||||
|
name
|
||||||
|
name-predicate
|
||||||
|
#,dom-ctcs
|
||||||
|
#,codom-contracts
|
||||||
|
#,pats
|
||||||
|
#,relation?
|
||||||
|
#,syn-error-name))
|
||||||
|
(term-define-fn name name2))])
|
||||||
|
(if (eq? 'top-level (syntax-local-context))
|
||||||
|
; Introduce the names before using them, to allow
|
||||||
|
; metafunction definition at the top-level.
|
||||||
|
(syntax
|
||||||
|
(begin
|
||||||
|
(define-syntaxes (name2 name-predicate) (values))
|
||||||
|
defs))
|
||||||
|
(syntax defs))))))]))
|
||||||
|
|
||||||
|
(define-syntax (generate-metafunction stx)
|
||||||
|
(syntax-case stx ()
|
||||||
|
[(_ orig-stx lang prev-metafunction name name-predicate dom-ctcs codom-contracts pats relation? syn-error-name)
|
||||||
|
(let ([prev-metafunction (and (syntax-e #'prev-metafunction) #'prev-metafunction)]
|
||||||
|
[dom-ctcs (syntax-e #'dom-ctcs)]
|
||||||
|
[codom-contracts (syntax-e #'codom-contracts)]
|
||||||
|
[pats (syntax-e #'pats)]
|
||||||
|
[relation? (syntax-e #'relation?)]
|
||||||
|
[syn-error-name (syntax-e #'syn-err-name)])
|
||||||
|
(define lang-nts
|
||||||
|
(definition-nts #'lang #'orig-stx syn-error-name))
|
||||||
(with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
|
(with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
|
||||||
[(lhs-for-lw ...) (lhs-lws pats)])
|
[(lhs-for-lw ...) (lhs-lws pats)])
|
||||||
(with-syntax ([((rhs stuff ...) ...) (if relation?
|
(with-syntax ([((rhs stuff ...) ...) (if relation?
|
||||||
#'((,(and (term raw-rhses) ...)) ...)
|
#'((,(and (term raw-rhses) ...)) ...)
|
||||||
#'((raw-rhses ...) ...))])
|
#'((raw-rhses ...) ...))]
|
||||||
(with-syntax ([(lhs ...) #'((lhs-clauses ...) ...)]
|
[(lhs ...) #'((lhs-clauses ...) ...)])
|
||||||
[name name])
|
|
||||||
(when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction)))
|
|
||||||
(raise-syntax-error syn-error-name "the extended and extending metafunctions cannot share a name" orig-stx prev-metafunction))
|
|
||||||
(parse-extras #'((stuff ...) ...))
|
(parse-extras #'((stuff ...) ...))
|
||||||
(let-values ([(lhs-namess lhs-namess/ellipsess)
|
(let-values ([(lhs-namess lhs-namess/ellipsess)
|
||||||
(lhss-bound-names (syntax->list (syntax (lhs ...))) lang-nts syn-error-name)])
|
(lhss-bound-names (syntax->list (syntax (lhs ...))) lang-nts syn-error-name)])
|
||||||
|
@ -1467,11 +1500,10 @@
|
||||||
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
|
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
|
||||||
rhs/where))))))
|
rhs/where))))))
|
||||||
lhs-namess lhs-namess/ellipsess
|
lhs-namess lhs-namess/ellipsess
|
||||||
(syntax->list (syntax (rhs/wheres ...))))]
|
(syntax->list (syntax (rhs/wheres ...))))])
|
||||||
[(name2 name-predicate) (generate-temporaries (syntax (name name)))])
|
(syntax-property
|
||||||
(with-syntax ([defs #`(begin
|
(prune-syntax
|
||||||
(define-values (name2 name-predicate)
|
#`(let ([sc `(side-conditions-rewritten ...)]
|
||||||
(let ([sc `(side-conditions-rewritten ...)]
|
|
||||||
[dsc `dom-side-conditions-rewritten])
|
[dsc `dom-side-conditions-rewritten])
|
||||||
(let ([cases (map (λ (pat rhs-fn rg-lhs src)
|
(let ([cases (map (λ (pat rhs-fn rg-lhs src)
|
||||||
(make-metafunc-case
|
(make-metafunc-case
|
||||||
|
@ -1511,20 +1543,9 @@
|
||||||
`(codom-side-conditions-rewritten ...)
|
`(codom-side-conditions-rewritten ...)
|
||||||
'name
|
'name
|
||||||
#,relation?))))
|
#,relation?))))
|
||||||
(term-define-fn name name2))])
|
|
||||||
(syntax-property
|
|
||||||
(prune-syntax
|
|
||||||
(if (eq? 'top-level (syntax-local-context))
|
|
||||||
; Introduce the names before using them, to allow
|
|
||||||
; metafunction definition at the top-level.
|
|
||||||
(syntax
|
|
||||||
(begin
|
|
||||||
(define-syntaxes (name2 name-predicate) (values))
|
|
||||||
defs))
|
|
||||||
(syntax defs)))
|
|
||||||
'disappeared-use
|
'disappeared-use
|
||||||
(map syntax-local-introduce
|
(map syntax-local-introduce
|
||||||
(syntax->list #'(original-names ...)))))))))))))]))
|
(syntax->list #'(original-names ...))))))))))]))
|
||||||
|
|
||||||
(define-syntax (define-judgment-form stx)
|
(define-syntax (define-judgment-form stx)
|
||||||
(not-expression-context stx)
|
(not-expression-context stx)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user