Refactor Redex so that it tells Check Syntax that non-terminal
references are binding/bound variables (beyond those appearing in the define-language itself) Specifically, - change define-language (and friends) so they record binding and source location information for non-terminals in the identifier that names the language (and to expand to disappeared bindings); - change rewrite-side-conditions/check-errs so that it accepts the language identifier (instead of a list of non-terminals) and returns one extra piece of syntax: that extra piece of syntax is just (void), but it has a bunch of disappeared uses on it that connect to the identifiers added to define-language; - similarly, adjust (term ...) so that it puts disappeared uses for non-terminal references.
This commit is contained in:
Robby Findler
parent
104f22c9f8
commit
48c719a3ee
|
|
@ -4,7 +4,7 @@
|
|||
"TL-syntax.rkt" "TL-semantics.rkt"
|
||||
"CMT.rkt"
|
||||
"common.rkt"
|
||||
redex)
|
||||
redex/reduction-semantics)
|
||||
(provide main same-result?)
|
||||
|
||||
(define (main . args)
|
||||
|
|
|
|||
|
|
@ -85,9 +85,9 @@
|
|||
(define-syntax (redex-check stx)
|
||||
(syntax-case stx ()
|
||||
[(form lang pat property . kw-args)
|
||||
(with-syntax ([(pattern (name ...) (name/ellipses ...))
|
||||
(with-syntax ([(syncheck-exp pattern (name ...) (name/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs
|
||||
(language-id-nts #'lang 'redex-check)
|
||||
#'lang
|
||||
'redex-check #t #'pat)]
|
||||
[show (show-message stx)])
|
||||
(let-values ([(attempts-stx source-stx retries-stx print?-stx size-stx fix-stx)
|
||||
|
|
@ -114,6 +114,7 @@
|
|||
[term-match (λ (generated)
|
||||
(cond [(test-match lang pat generated) => values]
|
||||
[else (redex-error 'redex-check "~s does not match ~s" generated 'pat)]))])
|
||||
syncheck-exp
|
||||
(parameterize ([attempt->size #,size-stx])
|
||||
#,(if source-stx
|
||||
#`(let-values ([(metafunc/red-rel num-cases)
|
||||
|
|
@ -329,19 +330,17 @@
|
|||
(when (keyword? k)
|
||||
(unless (member k '(#:satisfying #:source #:attempt-num #:retries #:i-th))
|
||||
(raise-syntax-error 'generate-term "unknown keyword" stx x))))))
|
||||
(define form-name (with-syntax ([(_ orig-name . args) stx])
|
||||
(syntax-e #'orig-name)))
|
||||
(syntax-case stx ()
|
||||
[(_ orig-name lang pat #:i-th . rest)
|
||||
(with-syntax ([(pattern (vars ...) (vars/ellipses ...))
|
||||
(with-syntax ([(syncheck-exp pattern (vars ...) (vars/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs
|
||||
(language-id-nts #'lang form-name)
|
||||
form-name #t #'pat)])
|
||||
#'lang
|
||||
(syntax-e #'orig-name) #t #'pat)])
|
||||
(syntax-case #'rest ()
|
||||
[()
|
||||
#'(generate-ith/proc lang `pattern)]
|
||||
#'(begin syncheck-exp (generate-ith/proc lang `pattern))]
|
||||
[(i-expr)
|
||||
#'((generate-ith/proc lang `pattern) i-expr)]))]
|
||||
#'(begin syncheck-exp ((generate-ith/proc lang `pattern) i-expr))]))]
|
||||
[(_ orig-name language #:satisfying (jf/mf-id . args) . rest)
|
||||
(cond
|
||||
[(metafunc #'jf/mf-id)
|
||||
|
|
@ -400,27 +399,27 @@
|
|||
=> (λ (f)
|
||||
#`(let* ([f #,f]
|
||||
[L (metafunc-proc-lang f)]
|
||||
[compile-pat (compile L '#,form-name)]
|
||||
[compile-pat (compile L 'orig-name)]
|
||||
[cases (metafunc-proc-cases f)])
|
||||
(check-cases 'src cases)
|
||||
(map (λ (c) (compile-pat ((metafunc-case-lhs+ c) L)))
|
||||
cases)))]
|
||||
[else
|
||||
#`(let* ([r #,(apply-contract #'reduction-relation? #'src "#:source argument" form-name)]
|
||||
#`(let* ([r #,(apply-contract #'reduction-relation? #'src "#:source argument" (syntax-e #'orig-name))]
|
||||
[L (reduction-relation-lang r)]
|
||||
[compile-pat (compile L '#,form-name)])
|
||||
[compile-pat (compile L 'orig-name)])
|
||||
(map (λ (p) (compile-pat ((rewrite-proc-lhs p) L)))
|
||||
(reduction-relation-make-procs r)))])
|
||||
#'rest)]
|
||||
[(lang pat . rest)
|
||||
(with-syntax ([(pattern (vars ...) (vars/ellipses ...))
|
||||
(with-syntax ([(syncheck-exp pattern (vars ...) (vars/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs
|
||||
(language-id-nts #'lang form-name)
|
||||
form-name #t #'pat)])
|
||||
(values #`(list #,(term-generator #'lang #'pattern form-name))
|
||||
#'lang
|
||||
(syntax-e #'orig-name) #t #'pat)])
|
||||
(values #`(begin syncheck-exp (list #,(term-generator #'lang #'pattern (syntax-e #'orig-name))))
|
||||
#'rest))]))
|
||||
(define generator-syntax
|
||||
#`(make-generator #,raw-generators '#,form-name))
|
||||
#`(make-generator #,raw-generators 'orig-name))
|
||||
(syntax-case args ()
|
||||
[()
|
||||
generator-syntax]
|
||||
|
|
@ -473,16 +472,18 @@
|
|||
[args-stx (if relation?
|
||||
(syntax/loc #'args (args))
|
||||
#'args)])
|
||||
(with-syntax ([(pat (names ...) (names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs nts 'redex-generator #t args-stx)])
|
||||
(if relation?
|
||||
#`(let ([gen-proc (make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size)])
|
||||
(λ ()
|
||||
(match (gen-proc)
|
||||
[`(,jf-name (,trms (... ...)))
|
||||
`(,jf-name ,@trms)]
|
||||
[#f #f])))
|
||||
#`(make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size))))]
|
||||
(with-syntax ([(syncheck-exp pat (names ...) (names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs #'lang-id 'redex-generator #t args-stx)])
|
||||
#`(begin
|
||||
syncheck-exp
|
||||
#,(if relation?
|
||||
#`(let ([gen-proc (make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size)])
|
||||
(λ ()
|
||||
(match (gen-proc)
|
||||
[`(,jf-name (,trms (... ...)))
|
||||
`(,jf-name ,@trms)]
|
||||
[#f #f])))
|
||||
#`(make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size)))))]
|
||||
[_
|
||||
(raise-syntax-error 'redex-generator
|
||||
"expected an integer depth bound"
|
||||
|
|
@ -496,12 +497,12 @@
|
|||
(let ()
|
||||
(define mf (syntax-local-value #'jf/mf-id (λ () #f)))
|
||||
(define nts (definition-nts #'lang-id stx 'redex-generator))
|
||||
(with-syntax ([(lhs-pat (lhs-names ...) (lhs-names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs nts (syntax-e #'g-m-p) #t #'args)]
|
||||
[(rhs-pat (rhs-names ...) (rhs-names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs nts (syntax-e #'g-m-p) #t #'res)]
|
||||
(with-syntax ([(lhs-syncheck-exp lhs-pat (lhs-names ...) (lhs-names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs #'lang-id (syntax-e #'g-m-p) #t #'args)]
|
||||
[(rhs-syncheck-exp rhs-pat (rhs-names ...) (rhs-names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs #'lang-id (syntax-e #'g-m-p) #t #'res)]
|
||||
[mf-id (term-fn-get-id mf)])
|
||||
#`(make-mf-gen/proc 'mf-id mf-id lang-id 'lhs-pat 'rhs-pat size)))]
|
||||
#`(begin lhs-syncheck-exp rhs-syncheck-exp (make-mf-gen/proc 'mf-id mf-id lang-id 'lhs-pat 'rhs-pat size))))]
|
||||
[_
|
||||
(raise-syntax-error 'redex-generator
|
||||
"expected \"=\" followed by a result pattern and an integer depth bound"
|
||||
|
|
|
|||
|
|
@ -64,13 +64,16 @@
|
|||
[(a . b)
|
||||
(datum->syntax (identifier-prune-lexical-context #'whatever '(#%app))
|
||||
(cons (loop #'a) (loop #'b))
|
||||
stx
|
||||
stx)]
|
||||
[x
|
||||
(identifier? #'x)
|
||||
(identifier-prune-lexical-context #'x (list (syntax-e #'x) '#%top))]
|
||||
[() (datum->syntax #f '() stx)]
|
||||
[_ (datum->syntax (identifier-prune-lexical-context #'whatever '(#%datum))
|
||||
(syntax->datum stx) stx)]))))
|
||||
(syntax->datum stx)
|
||||
stx
|
||||
stx)]))))
|
||||
|
||||
(define-syntax (--> stx) (raise-syntax-error '--> "used outside of reduction-relation"))
|
||||
(define-syntax (fresh stx) (raise-syntax-error 'fresh "used outside of reduction-relation"))
|
||||
|
|
@ -107,7 +110,12 @@
|
|||
(hash-set extended (syntax-e name) w/ellipses))))
|
||||
|
||||
;; the withs, freshs, and side-conditions come in backwards order
|
||||
(define-for-syntax (bind-withs orig-name main lang lang-nts stx where-mode body names w/ellipses side-condition-unquoted? jf-results-id)
|
||||
;; rt-lang is an identifier that will be bound to a (runtime) language,
|
||||
;; not necc bound via define-language.
|
||||
;; ct-lang is an identifier guaranteed to be bound by define-language
|
||||
;; that can be used to call rewrite-side-conditions/check-errs, but
|
||||
;; some extension of that language may end up being bound to rt-lang
|
||||
(define-for-syntax (bind-withs orig-name main rt-lang lang-nts ct-lang stx where-mode body names w/ellipses side-condition-unquoted? jf-results-id)
|
||||
(with-disappeared-uses
|
||||
(let loop ([stx stx]
|
||||
[to-not-be-in main]
|
||||
|
|
@ -119,13 +127,13 @@
|
|||
[((-where x e) y ...)
|
||||
(where-keyword? #'-where)
|
||||
(let ()
|
||||
(with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...))
|
||||
(with-syntax ([(syncheck-exp side-conditions-rewritten (names ...) (names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
ct-lang
|
||||
'reduction-relation
|
||||
#t
|
||||
#'x)]
|
||||
[lang-stx lang])
|
||||
[lang-stx rt-lang])
|
||||
(define-values (binding-constraints temporaries env+)
|
||||
(generate-binding-constraints (syntax->list #'(names ...))
|
||||
(syntax->list #'(names/ellipses ...))
|
||||
|
|
@ -134,18 +142,20 @@
|
|||
(with-syntax ([(binding-constraints ...) binding-constraints]
|
||||
[(x ...) temporaries])
|
||||
(define rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in) env+))
|
||||
#`(#,(case where-mode
|
||||
#`(begin
|
||||
syncheck-exp
|
||||
(#,(case where-mode
|
||||
[(flatten)
|
||||
#'combine-where-results/flatten]
|
||||
[(predicate)
|
||||
#'combine-where-results/predicate]
|
||||
[else (error 'unknown-where-mode "~s" where-mode)])
|
||||
(match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term/nts e #,lang-nts))
|
||||
(match-pattern (compile-pattern #,rt-lang `side-conditions-rewritten #t) (term e #:lang #,ct-lang))
|
||||
(λ (bindings)
|
||||
(let ([x (lookup-binding bindings 'names)] ...)
|
||||
(and binding-constraints ...
|
||||
(term-let ([names/ellipses x] ...)
|
||||
#,rest-body))))))))]
|
||||
#,rest-body)))))))))]
|
||||
[((-side-condition s ...) y ...)
|
||||
(side-condition-keyword? #'-side-condition)
|
||||
(if side-condition-unquoted?
|
||||
|
|
@ -194,17 +204,18 @@
|
|||
(let ([ellipsis (syntax/loc premise (... ...))])
|
||||
(values #`(#,in #,ellipsis) #`(#,out #,ellipsis)))
|
||||
(values in out)))]
|
||||
[(output-pattern output-names output-names/ellipses)
|
||||
(with-syntax ([(output names names/ellipses)
|
||||
(rewrite-side-conditions/check-errs lang-nts orig-name #t output-pre-pattern)])
|
||||
(values #'output
|
||||
[(syncheck-exp output-pattern output-names output-names/ellipses)
|
||||
(with-syntax ([(syncheck-exp output names names/ellipses)
|
||||
(rewrite-side-conditions/check-errs ct-lang orig-name #t output-pre-pattern)])
|
||||
(values #'syncheck-exp
|
||||
#'output
|
||||
(syntax->list #'names)
|
||||
(syntax->list #'names/ellipses)))]
|
||||
[(binding-constraints temporaries env+)
|
||||
(generate-binding-constraints output-names output-names/ellipses env orig-name)]
|
||||
[(rest-body) (loop rest-clauses #`(list judgment-output #,to-not-be-in) env+)]
|
||||
[(call)
|
||||
(let ([input (quasisyntax/loc premise (term/nts #,input-template #,lang-nts))])
|
||||
(let ([input (quasisyntax/loc premise (term #,input-template #:lang #,ct-lang))])
|
||||
(define (make-traced input)
|
||||
(quasisyntax/loc premise
|
||||
(call-judgment-form 'form-name #,judgment-proc '#,mode #,input #,(if jf-results-id #''() #f))))
|
||||
|
|
@ -217,9 +228,10 @@
|
|||
[(temp ...) temporaries]
|
||||
[(binding-constraint ...) binding-constraints])
|
||||
#`(begin
|
||||
#,syncheck-exp
|
||||
(void #,(defined-check judgment-proc "judgment form" #:external #'form-name))
|
||||
(judgment-form-bind-withs/proc
|
||||
#,lang
|
||||
#,rt-lang
|
||||
`#,output-pattern
|
||||
#,call
|
||||
#,under-ellipsis?
|
||||
|
|
@ -674,7 +686,7 @@
|
|||
(error 'syn-err-name "judgment forms with output mode positions cannot currently be used in term"))
|
||||
(with-syntax* ([(binding ...) (generate-temporaries (cdr (syntax->list #'mode)))]
|
||||
[(input) (generate-temporaries (list #'input))]
|
||||
[body-stx (bind-withs #'syn-err-name '() #'lang (syntax->datum #'nts)
|
||||
[body-stx (bind-withs #'syn-err-name '() #'lang (syntax->datum #'nts) #'lang
|
||||
(if (jf-is-relation? #'jdg-name)
|
||||
(list #'(jdg-name ((unquote-splicing input))))
|
||||
(list #'(jdg-name (unquote binding) ...)))
|
||||
|
|
@ -710,7 +722,8 @@
|
|||
(car (generate-temporaries '(jf-derivation-lst)))
|
||||
#f)]
|
||||
[main-stx
|
||||
(bind-withs syn-err-name '() lang nts (list judgment)
|
||||
(bind-withs syn-err-name '() lang nts lang
|
||||
(list judgment)
|
||||
'flatten
|
||||
(if derivation?
|
||||
id-or-not
|
||||
|
|
@ -749,7 +762,7 @@
|
|||
[(_ jf-expr)
|
||||
#'(#%expression (judgment-holds/derivation build-derivations #t jf-expr any))]))
|
||||
|
||||
(define-for-syntax (do-compile-judgment-form-proc name mode-stx clauses rule-names contracts nts orig stx syn-error-name)
|
||||
(define-for-syntax (do-compile-judgment-form-proc name mode-stx clauses rule-names contracts nts orig lang stx syn-error-name)
|
||||
(with-syntax ([(init-jf-derivation-id) (generate-temporaries '(init-jf-derivation-id))])
|
||||
(define mode (cdr (syntax->datum mode-stx)))
|
||||
(define-values (input-contracts output-contracts)
|
||||
|
|
@ -761,19 +774,19 @@
|
|||
(syntax-case clause ()
|
||||
[((_ . conc-pats) . prems)
|
||||
(let-values ([(input-pats output-pats) (split-by-mode (syntax->list #'conc-pats) mode)])
|
||||
(with-syntax ([(lhs (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs nts syn-error-name #t input-pats)]
|
||||
(with-syntax ([(lhs-syncheck-exp lhs (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs lang syn-error-name #t input-pats)]
|
||||
[(jf-derivation-id) (generate-temporaries '(jf-derivation-id))])
|
||||
(define (contracts-compilation ctcs)
|
||||
(and ctcs
|
||||
(with-syntax ([(ctc ...) ctcs])
|
||||
#`(list (compile-pattern lang `ctc #f) ...))))
|
||||
(with-syntax ([(ctc ...) ctcs])
|
||||
#`(list (compile-pattern lang `ctc #f) ...)))
|
||||
(define body
|
||||
(parameterize ([judgment-form-pending-expansion
|
||||
(cons name
|
||||
(struct-copy judgment-form (lookup-judgment-form-id name)
|
||||
[proc #'recur]))])
|
||||
(bind-withs syn-error-name '() #'lang nts (syntax->list #'prems)
|
||||
'flatten #`(list (derivation-with-output-only (term/nts (#,@output-pats) #,nts)
|
||||
(bind-withs syn-error-name '() lang nts lang
|
||||
(syntax->list #'prems)
|
||||
'flatten #`(list (derivation-with-output-only (term (#,@output-pats) #:lang #,lang)
|
||||
#,clause-name
|
||||
jf-derivation-id))
|
||||
(syntax->list #'(names ...))
|
||||
|
|
@ -786,16 +799,17 @@
|
|||
#`(
|
||||
;; pieces of a 'let' expression to be combined: first some bindings
|
||||
([compiled-lhs (compile-pattern lang `lhs #t)]
|
||||
#,@(if (contracts-compilation input-contracts)
|
||||
#,@(if input-contracts
|
||||
(list #`[compiled-input-ctcs #,(contracts-compilation input-contracts)])
|
||||
(list))
|
||||
#,@(if (contracts-compilation output-contracts)
|
||||
#,@(if output-contracts
|
||||
(list #`[compiled-output-ctcs #,(contracts-compilation output-contracts)])
|
||||
(list)))
|
||||
;; and then the body of the let, but expected to be behind a (λ (input) ...).
|
||||
(let ([jf-derivation-id init-jf-derivation-id])
|
||||
(begin
|
||||
#,@(if (contracts-compilation input-contracts)
|
||||
lhs-syncheck-exp
|
||||
#,@(if input-contracts
|
||||
(list #`(check-judgment-form-contract '#,name input compiled-input-ctcs 'I '#,mode))
|
||||
(list))
|
||||
(combine-judgment-rhses
|
||||
|
|
@ -804,7 +818,7 @@
|
|||
(λ (bnds)
|
||||
(term-let ([names/ellipses (lookup-binding bnds 'names)] ...)
|
||||
#,body))
|
||||
#,(if (contracts-compilation output-contracts)
|
||||
#,(if output-contracts
|
||||
#`(λ (output)
|
||||
(check-judgment-form-contract '#,name output compiled-output-ctcs 'O '#,mode))
|
||||
#`void))))))))]))
|
||||
|
|
@ -1086,14 +1100,22 @@
|
|||
[mode (cdr (syntax->datum #'mode-arg))])
|
||||
(unless (jf-is-relation? #'judgment-form-name)
|
||||
(mode-check (cdr (syntax->datum #'mode-arg)) clauses nts syn-err-name stx))
|
||||
(define contracts (syntax-case #'ctcs ()
|
||||
[#f #f]
|
||||
[(p ...)
|
||||
(map (λ (pat)
|
||||
(with-syntax ([(pat (names ...) (names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs nts #'syn-error-name #f pat)])
|
||||
#'pat))
|
||||
(syntax->list #'(p ...)))]))
|
||||
(define-values (syncheck-exprs contracts)
|
||||
(syntax-case #'ctcs ()
|
||||
[#f (values '() #f)]
|
||||
[(p ...)
|
||||
(let loop ([pats (syntax->list #'(p ...))]
|
||||
[ctcs '()]
|
||||
[syncheck-exps '()])
|
||||
(cond
|
||||
[(null? pats) (values syncheck-exps (reverse ctcs))]
|
||||
[else
|
||||
(define pat (car pats))
|
||||
(with-syntax ([(syncheck-exp pat (names ...) (names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs #'lang #'syn-error-name #f pat)])
|
||||
(loop (cdr pats)
|
||||
(cons #'pat ctcs)
|
||||
(cons #'syncheck-exp syncheck-exps)))]))]))
|
||||
(define proc-stx (do-compile-judgment-form-proc #'judgment-form-name
|
||||
#'mode-arg
|
||||
clauses
|
||||
|
|
@ -1101,10 +1123,11 @@
|
|||
contracts
|
||||
nts
|
||||
#'orig
|
||||
#'lang
|
||||
#'full-def
|
||||
syn-err-name))
|
||||
(define gen-stx (with-syntax* ([(comp-clauses ...)
|
||||
(map (λ (c) (compile-gen-clause c mode nts syn-err-name
|
||||
(map (λ (c) (compile-gen-clause c mode syn-err-name
|
||||
#'judgment-form-name #'lang))
|
||||
clauses)])
|
||||
(if (identifier? #'orig)
|
||||
|
|
@ -1120,7 +1143,7 @@
|
|||
(λ ()
|
||||
#,(check-pats
|
||||
#'(list comp-clauses ...)))))))
|
||||
#`(values #,proc-stx #,gen-stx))]))
|
||||
#`(begin #,@syncheck-exprs (values #,proc-stx #,gen-stx)))]))
|
||||
|
||||
(define-for-syntax (rewrite-relation-prems clauses)
|
||||
(map (λ (c)
|
||||
|
|
@ -1189,7 +1212,7 @@
|
|||
[syn-err-name (syntax-e #'syn-err-name)]
|
||||
[mode (cdr (syntax->datum #'mode-arg))])
|
||||
(with-syntax* ([(comp-clauses ...)
|
||||
(map (λ (c) (compile-gen-clause c mode nts syn-err-name
|
||||
(map (λ (c) (compile-gen-clause c mode syn-err-name
|
||||
#'judgment-form-name #'lang))
|
||||
clauses)])
|
||||
(if (identifier? #'orig)
|
||||
|
|
@ -1339,32 +1362,36 @@
|
|||
|
||||
|
||||
|
||||
(define-for-syntax (compile-gen-clause clause-stx mode nts syn-error-name jdg-name lang)
|
||||
(define-for-syntax (compile-gen-clause clause-stx mode syn-error-name jdg-name lang)
|
||||
(syntax-case clause-stx ()
|
||||
[((conc-name . conc-body-raw) prems ...)
|
||||
(let*-values ([(conc/+ conc/-) (split-by-mode (syntax->list #'conc-body-raw) mode)]
|
||||
[(conc/+rw names) (rewrite-pats conc/+ nts)]
|
||||
[(ps-rw eqs p-names) (rewrite-prems #t (syntax->list #'(prems ...)) nts names 'define-judgment-form)]
|
||||
[(syncheck-exps conc/+rw names) (rewrite-pats conc/+ lang)]
|
||||
[(ps-rw eqs p-names) (rewrite-prems #t (syntax->list #'(prems ...)) names lang 'define-judgment-form)]
|
||||
[(conc/-rw conc-mfs) (rewrite-terms conc/- p-names)]
|
||||
[(conc) (fuse-by-mode conc/+rw conc/-rw mode)])
|
||||
(with-syntax ([(c ...) conc]
|
||||
[(c-mf ...) conc-mfs]
|
||||
[(eq ...) eqs]
|
||||
[(prem-bod ...) (reverse ps-rw)])
|
||||
#`(clause '(list c ...) (list eq ...) (list c-mf ... prem-bod ...) effective-lang '#,jdg-name)))]))
|
||||
#`(begin #,@syncheck-exps
|
||||
(clause '(list c ...) (list eq ...) (list c-mf ... prem-bod ...) effective-lang '#,jdg-name))))]))
|
||||
|
||||
|
||||
(define-for-syntax (rewrite-prems in-judgment-form? prems nts names what)
|
||||
(define-for-syntax (rewrite-prems in-judgment-form? prems names lang what)
|
||||
(define (rewrite-jf prem-name prem-body ns ps-rw eqs)
|
||||
(define p-form (lookup-judgment-form-id prem-name))
|
||||
(define p-mode (judgment-form-mode p-form))
|
||||
(define p-clauses (judgment-form-gen-clauses p-form))
|
||||
(define-values (p/-s p/+s) (split-by-mode (syntax->list prem-body) p-mode))
|
||||
(define-values (p/-rws mf-apps) (rewrite-terms p/-s ns))
|
||||
(define-values (p/+rws new-names) (rewrite-pats p/+s nts))
|
||||
(define-values (syncheck-exps p/+rws new-names) (rewrite-pats p/+s lang))
|
||||
(define p-rw (fuse-by-mode p/-rws p/+rws p-mode))
|
||||
(with-syntax ([(p ...) p-rw])
|
||||
(values (cons #`(prem #,p-clauses '(list p ...)) (append mf-apps ps-rw))
|
||||
(values (cons #`(begin
|
||||
#,@syncheck-exps
|
||||
(prem #,p-clauses '(list p ...)))
|
||||
(append mf-apps ps-rw))
|
||||
eqs
|
||||
(append ns new-names))))
|
||||
(define-values (prems-rev new-eqs new-names)
|
||||
|
|
@ -1376,9 +1403,9 @@
|
|||
[(-where pat term)
|
||||
(where-keyword? #'-where)
|
||||
(let-values ([(term-rws mf-cs) (rewrite-terms (list #'term) ns)])
|
||||
(with-syntax ([(pat-rw new-names) (rewrite/pat #'pat nts)])
|
||||
(with-syntax ([(syncheck-exp pat-rw new-names) (rewrite/pat #'pat lang)])
|
||||
(values (append mf-cs ps-rw)
|
||||
(cons #`(eqn 'pat-rw '#,(car term-rws)) eqs)
|
||||
(cons #`(begin syncheck-exp (eqn 'pat-rw '#,(car term-rws))) eqs)
|
||||
(append (syntax->datum #'new-names) ns))))]
|
||||
[(side-cond rest)
|
||||
(side-condition-keyword? #'side-cond)
|
||||
|
|
@ -1401,18 +1428,19 @@
|
|||
[else (raise-syntax-error what "malformed premise" prem)])))
|
||||
(values prems-rev new-eqs new-names))
|
||||
|
||||
(define-for-syntax (rewrite-pats pats nts)
|
||||
(with-syntax ([((pat-rw (names ...)) ...)
|
||||
(map (λ (p) (rewrite/pat p nts))
|
||||
(define-for-syntax (rewrite-pats pats lang)
|
||||
(with-syntax ([((syncheck-exp pat-rw (names ...)) ...)
|
||||
(map (λ (p) (rewrite/pat p lang))
|
||||
pats)])
|
||||
(values (syntax->list #'(pat-rw ...))
|
||||
(values #'(syncheck-exp ...)
|
||||
(syntax->list #'(pat-rw ...))
|
||||
(remove-duplicates (syntax->datum #'(names ... ...))))))
|
||||
|
||||
|
||||
(define-for-syntax (rewrite/pat pat nts)
|
||||
(with-syntax ([(body (names ...) (names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs nts #'rewrite/pat #t pat)])
|
||||
#'(body (names ...))))
|
||||
(define-for-syntax (rewrite/pat pat lang)
|
||||
(with-syntax ([(syncheck-exp body (names ...) (names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs lang #'rewrite/pat #t pat)])
|
||||
#'(syncheck-exp body (names ...))))
|
||||
|
||||
(define-for-syntax (rewrite-terms terms names)
|
||||
(with-syntax* ([((term-pattern ((res-pat ((metafunc f) args-pat)) ...) body-pat) ...)
|
||||
|
|
|
|||
|
|
@ -42,13 +42,14 @@
|
|||
(begin
|
||||
(unless (identifier? #'lang)
|
||||
(raise-syntax-error (syntax-e #'form-name) "expected an identifier in the language position" orig-stx #'lang))
|
||||
(let ([lang-nts (language-id-nts #'lang (syntax-e #'form-name))])
|
||||
(with-syntax ([((side-conditions-rewritten (names ...) (names/ellipses ...)) ...)
|
||||
(map (λ (x) (rewrite-side-conditions/check-errs lang-nts (syntax-e #'form-name) #t x))
|
||||
(syntax->list (syntax (pattern ...))))]
|
||||
[(cp-x ...) (generate-temporaries #'(pattern ...))]
|
||||
[make-matcher make-matcher])
|
||||
#'(make-matcher
|
||||
(with-syntax ([((syncheck-expr side-conditions-rewritten (names ...) (names/ellipses ...)) ...)
|
||||
(map (λ (x) (rewrite-side-conditions/check-errs #'lang (syntax-e #'form-name) #t x))
|
||||
(syntax->list (syntax (pattern ...))))]
|
||||
[(cp-x ...) (generate-temporaries #'(pattern ...))]
|
||||
[make-matcher make-matcher])
|
||||
#'(begin
|
||||
syncheck-expr ...
|
||||
(make-matcher
|
||||
'form-name lang
|
||||
(list 'pattern ...)
|
||||
(list (compile-pattern lang `side-conditions-rewritten #t) ...)
|
||||
|
|
@ -144,29 +145,32 @@
|
|||
(syntax-case stx ()
|
||||
[(_ red lang nt)
|
||||
(identifier? (syntax nt))
|
||||
(with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs (language-id-nts #'lang 'compatible-closure)
|
||||
(with-syntax ([(syncheck-expr side-conditions-rewritten (names ...) (names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs #'lang
|
||||
'compatible-closure
|
||||
#t
|
||||
(syntax (cross nt)))])
|
||||
(syntax (do-context-closure red lang `side-conditions-rewritten 'compatible-closure)))]
|
||||
(syntax (begin syncheck-expr
|
||||
(do-context-closure red lang `side-conditions-rewritten 'compatible-closure))))]
|
||||
[(_ red lang nt)
|
||||
(raise-syntax-error 'compatible-closure "expected a non-terminal as last argument" stx (syntax nt))]))
|
||||
|
||||
(define-syntax (context-closure stx)
|
||||
(syntax-case stx ()
|
||||
[(_ red lang pattern)
|
||||
(with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs (language-id-nts #'lang 'context-closure)
|
||||
(with-syntax ([(syncheck-expr side-conditions-rewritten (names ...) (names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs #'lang
|
||||
'context-closure
|
||||
#t
|
||||
(syntax pattern))])
|
||||
(syntax
|
||||
(do-context-closure
|
||||
red
|
||||
lang
|
||||
`side-conditions-rewritten
|
||||
'context-closure)))]))
|
||||
(begin
|
||||
syncheck-expr
|
||||
(do-context-closure
|
||||
red
|
||||
lang
|
||||
`side-conditions-rewritten
|
||||
'context-closure))))]))
|
||||
|
||||
(define (do-context-closure red lang pat name)
|
||||
(unless (reduction-relation? red)
|
||||
|
|
@ -595,8 +599,7 @@
|
|||
(for-each loop nexts)))))
|
||||
all-top-levels)
|
||||
|
||||
(let ([name-table (make-hasheq)]
|
||||
[lang-nts (language-id-nts lang-id orig-name)])
|
||||
(let ([name-table (make-hasheq)])
|
||||
(hash-set! name-table #f 0)
|
||||
;; name table maps symbols for the rule names to their syntax objects and to a counter indicating what
|
||||
;; order the names were encountered in. The current value of the counter is stored in the table at key '#f'.
|
||||
|
|
@ -609,20 +612,21 @@
|
|||
(map car (sort (hash-map name-table (λ (k v) (list k (list-ref v 1)))) < #:key cadr)))]
|
||||
[lws lws]
|
||||
|
||||
[(domain-pattern-side-conditions-rewritten (names ...) (names/ellipses ...))
|
||||
[(domain-syncheck-expr domain-pattern-side-conditions-rewritten (names ...) (names/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
lang-id
|
||||
orig-name
|
||||
#f
|
||||
domain-pattern)])
|
||||
|
||||
#`(build-reduction-relation
|
||||
#,orig-red-expr
|
||||
lang-id
|
||||
(list top-level ...)
|
||||
'(rule-names ...)
|
||||
lws
|
||||
`domain-pattern-side-conditions-rewritten)))))
|
||||
#`(begin
|
||||
domain-syncheck-expr
|
||||
(build-reduction-relation
|
||||
#,orig-red-expr
|
||||
lang-id
|
||||
(list top-level ...)
|
||||
'(rule-names ...)
|
||||
lws
|
||||
`domain-pattern-side-conditions-rewritten))))))
|
||||
|
||||
#|
|
||||
;; relation-tree =
|
||||
|
|
@ -659,29 +663,32 @@
|
|||
(syntax->list (syntax (extras ...)))
|
||||
lang-id))]
|
||||
[((rhs-arrow rhs-from rhs-to) (lhs-arrow lhs-frm-id lhs-to-id))
|
||||
(let* ([lang-nts (language-id-nts lang-id orig-name)]
|
||||
[rewrite-side-conds
|
||||
(λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))])
|
||||
(with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...))
|
||||
(let ([lang-nts (language-id-nts lang-id 'reduction-relation)]
|
||||
[rewrite-side-conds
|
||||
(λ (pat) (rewrite-side-conditions/check-errs lang-id orig-name #t pat))])
|
||||
(with-syntax ([(lhs-syncheck-expr side-conditions-rewritten (names ...) (names/ellipses ...))
|
||||
(rewrite-side-conds
|
||||
(rewrite-node-pat (syntax-e (syntax lhs-frm-id))
|
||||
(syntax rhs-from)))]
|
||||
[(fresh-rhs-from (fresh-names ...) (fresh-names/ellipses ...))
|
||||
[(rhs-syncheck-expr fresh-rhs-from (fresh-names ...) (fresh-names/ellipses ...))
|
||||
(rewrite-side-conds
|
||||
(freshen-names #'rhs-from #'lhs-frm-id lang-nts orig-name))]
|
||||
[lang lang])
|
||||
(map
|
||||
(λ (child-proc)
|
||||
#`(do-node-match
|
||||
'lhs-frm-id
|
||||
'lhs-to-id
|
||||
`side-conditions-rewritten
|
||||
(λ (bindings rhs-binder)
|
||||
(term-let ([lhs-to-id rhs-binder]
|
||||
[names/ellipses (lookup-binding bindings 'names)] ...)
|
||||
(term rhs-to #:lang lang)))
|
||||
#,child-proc
|
||||
`fresh-rhs-from))
|
||||
#`(begin
|
||||
lhs-syncheck-expr
|
||||
rhs-syncheck-expr
|
||||
(do-node-match
|
||||
'lhs-frm-id
|
||||
'lhs-to-id
|
||||
`side-conditions-rewritten
|
||||
(λ (bindings rhs-binder)
|
||||
(term-let ([lhs-to-id rhs-binder]
|
||||
[names/ellipses (lookup-binding bindings 'names)] ...)
|
||||
(term rhs-to #:lang lang)))
|
||||
#,child-proc
|
||||
`fresh-rhs-from)))
|
||||
(get-choices stx orig-name bm #'lang
|
||||
(syntax lhs-arrow)
|
||||
name-table lang-id
|
||||
|
|
@ -726,54 +733,59 @@
|
|||
p)])))))
|
||||
|
||||
(define (do-leaf stx orig-name lang name-table from to extras lang-id)
|
||||
(let* ([lang-nts (language-id-nts lang-id orig-name)]
|
||||
[rw-sc (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))])
|
||||
(let-values ([(name computed-name sides/withs/freshs) (process-extras stx orig-name name-table extras)])
|
||||
(with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...)) (rw-sc from)])
|
||||
(define body-code
|
||||
(bind-withs orig-name
|
||||
#'main-exp
|
||||
lang
|
||||
lang-nts
|
||||
sides/withs/freshs
|
||||
'flatten
|
||||
#`(list (cons #,(or computed-name #'none)
|
||||
(term #,to #:lang #,lang)))
|
||||
(syntax->list #'(names ...))
|
||||
(syntax->list #'(names/ellipses ...))
|
||||
#t
|
||||
#f))
|
||||
(define test-case-body-code
|
||||
;; this contains some redundant code
|
||||
(bind-withs orig-name
|
||||
#'#t
|
||||
#'lang-id2
|
||||
lang-nts
|
||||
sides/withs/freshs
|
||||
'predicate
|
||||
#'#t
|
||||
(syntax->list #'(names ...))
|
||||
(syntax->list #'(names/ellipses ...))
|
||||
#t
|
||||
#f))
|
||||
(with-syntax ([(lhs-w/extras (w/extras-names ...) (w/extras-names/ellipses ...))
|
||||
(rw-sc #`(side-condition #,from #,test-case-body-code))]
|
||||
[lhs-source (format "~a:~a:~a"
|
||||
(and (path? (syntax-source from))
|
||||
(path->relative-string/library (syntax-source from)))
|
||||
(syntax-line from)
|
||||
(syntax-column from))]
|
||||
[name name]
|
||||
[lang lang]
|
||||
[body-code body-code])
|
||||
#`
|
||||
(define lang-nts (language-id-nts lang-id 'reduction-relation))
|
||||
(define (rw-sc pat) (rewrite-side-conditions/check-errs lang-id orig-name #t pat))
|
||||
(define-values (name computed-name sides/withs/freshs) (process-extras stx orig-name name-table extras))
|
||||
(with-syntax ([(from-syncheck-expr side-conditions-rewritten (names ...) (names/ellipses ...)) (rw-sc from)])
|
||||
(define body-code
|
||||
(bind-withs orig-name
|
||||
#'main-exp
|
||||
lang
|
||||
lang-nts
|
||||
lang-id
|
||||
sides/withs/freshs
|
||||
'flatten
|
||||
#`(begin
|
||||
from-syncheck-expr
|
||||
(list (cons #,(or computed-name #'none)
|
||||
(term #,to #:lang #,lang))))
|
||||
(syntax->list #'(names ...))
|
||||
(syntax->list #'(names/ellipses ...))
|
||||
#t
|
||||
#f))
|
||||
(define test-case-body-code
|
||||
;; this contains some redundant code
|
||||
(bind-withs orig-name
|
||||
#'#t
|
||||
#'lang-id2
|
||||
lang-nts
|
||||
lang-id
|
||||
sides/withs/freshs
|
||||
'predicate
|
||||
#'#t
|
||||
(syntax->list #'(names ...))
|
||||
(syntax->list #'(names/ellipses ...))
|
||||
#t
|
||||
#f))
|
||||
(with-syntax ([(lhs-syncheck-expr lhs-w/extras (w/extras-names ...) (w/extras-names/ellipses ...))
|
||||
(rw-sc #`(side-condition #,from #,test-case-body-code))]
|
||||
[lhs-source (format "~a:~a:~a"
|
||||
(and (path? (syntax-source from))
|
||||
(path->relative-string/library (syntax-source from)))
|
||||
(syntax-line from)
|
||||
(syntax-column from))]
|
||||
[name name]
|
||||
[lang lang]
|
||||
[body-code body-code])
|
||||
#`(begin
|
||||
lhs-syncheck-expr
|
||||
(build-rewrite-proc/leaf `side-conditions-rewritten
|
||||
(λ (main-exp bindings)
|
||||
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
|
||||
body-code))
|
||||
lhs-source
|
||||
name
|
||||
(λ (lang-id2) `lhs-w/extras)))))))
|
||||
(λ (lang-id2) `lhs-w/extras))))))
|
||||
|
||||
(define (process-extras stx orig-name name-table extras)
|
||||
(let* ([the-name #f]
|
||||
|
|
@ -1037,13 +1049,15 @@
|
|||
(syntax-case stx ()
|
||||
[(form-name lang-exp pattern)
|
||||
(identifier? #'lang-exp)
|
||||
(let*-values ([(what) (syntax-e #'form-name)]
|
||||
[(nts) (language-id-nts #'lang-exp what)])
|
||||
(with-syntax ([(side-condition-rewritten (vars ...) (ids/depths ...))
|
||||
(rewrite-side-conditions/check-errs nts what #t #'pattern)])
|
||||
(let ()
|
||||
(define what (syntax-e #'form-name))
|
||||
(with-syntax ([(syncheck-expr side-condition-rewritten (vars ...) (ids/depths ...))
|
||||
(rewrite-side-conditions/check-errs #'lang-exp what #t #'pattern)])
|
||||
(with-syntax ([binders (map syntax-e (syntax->list #'(vars ...)))]
|
||||
[name (syntax-local-infer-name stx)])
|
||||
#`(do-test-match lang-exp `side-condition-rewritten 'binders 'name #,boolean-only?))))]
|
||||
#`(begin
|
||||
syncheck-expr
|
||||
(do-test-match lang-exp `side-condition-rewritten 'binders 'name #,boolean-only?)))))]
|
||||
[(form-name lang-exp pattern expression)
|
||||
(identifier? #'lang-exp)
|
||||
(syntax
|
||||
|
|
@ -1222,9 +1236,9 @@
|
|||
[(lhs ...) #'((lhs-clauses ...) ...)])
|
||||
(with-syntax ([((clause-name stuff ...) ...) (extract-clause-names #'((stuff+names ...) ...))])
|
||||
(parse-extras #'((stuff ...) ...))
|
||||
(with-syntax ([((side-conditions-rewritten lhs-names lhs-namess/ellipses) ...)
|
||||
(with-syntax ([((syncheck-expr side-conditions-rewritten lhs-names lhs-namess/ellipses) ...)
|
||||
(map (λ (x) (rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
#'lang
|
||||
syn-error-name
|
||||
#t
|
||||
x))
|
||||
|
|
@ -1233,7 +1247,7 @@
|
|||
(map (λ (sc/b rhs names names/ellipses)
|
||||
(bind-withs
|
||||
syn-error-name '()
|
||||
#'effective-lang lang-nts
|
||||
#'effective-lang lang-nts #'lang
|
||||
sc/b 'flatten
|
||||
#`(list (term #,rhs #:lang lang))
|
||||
(syntax->list names)
|
||||
|
|
@ -1248,7 +1262,7 @@
|
|||
(map (λ (sc/b rhs names names/ellipses)
|
||||
(bind-withs
|
||||
syn-error-name '()
|
||||
#'effective-lang lang-nts
|
||||
#'effective-lang lang-nts #'lang
|
||||
sc/b 'predicate
|
||||
#`#t
|
||||
(syntax->list names)
|
||||
|
|
@ -1259,9 +1273,9 @@
|
|||
(syntax->list #'(rhs ...))
|
||||
(syntax->list #'(lhs-names ...))
|
||||
(syntax->list #'(lhs-namess/ellipses ...)))])
|
||||
(with-syntax ([((rg-side-conditions-rewritten rg-names rg-names/ellipses ...) ...)
|
||||
(with-syntax ([((rg-syncheck-expr rg-side-conditions-rewritten rg-names rg-names/ellipses ...) ...)
|
||||
(map (λ (x) (rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
#'lang
|
||||
syn-error-name
|
||||
#t
|
||||
x))
|
||||
|
|
@ -1274,18 +1288,18 @@
|
|||
(syntax-line lhs)
|
||||
(syntax-column lhs)))
|
||||
pats)]
|
||||
[(dom-side-conditions-rewritten dom-names dom-names/ellipses)
|
||||
[(dom-syncheck-expr dom-side-conditions-rewritten dom-names dom-names/ellipses)
|
||||
(if dom-ctcs
|
||||
(rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
#'lang
|
||||
syn-error-name
|
||||
#f
|
||||
dom-ctcs)
|
||||
#'(any () ()))]
|
||||
[((codom-side-conditions-rewritten codom-names codom-names/ellipses) ...)
|
||||
#'((void) any () ()))]
|
||||
[((codom-syncheck-expr codom-side-conditions-rewritten codom-names codom-names/ellipses) ...)
|
||||
(map (λ (codom-contract)
|
||||
(rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
#'lang
|
||||
syn-error-name
|
||||
#f
|
||||
codom-contract))
|
||||
|
|
@ -1312,6 +1326,7 @@
|
|||
(prune-syntax
|
||||
#`(let ([sc `(side-conditions-rewritten ...)]
|
||||
[dsc `dom-side-conditions-rewritten])
|
||||
syncheck-expr ... rg-syncheck-expr ... dom-syncheck-expr codom-syncheck-expr ...
|
||||
(let ([cases (map (λ (pat rhs-fn rg-lhs src)
|
||||
(make-metafunc-case
|
||||
(λ (effective-lang) (compile-pattern effective-lang pat #t))
|
||||
|
|
@ -1403,10 +1418,10 @@
|
|||
(define-values (rev-clauses _1 _2)
|
||||
(for/fold ([clauses '()] [prev-lhs-pats '()] [prev-lhs-pats* '()])
|
||||
([lhs (in-list lhss)] [rhs (in-list rhss)] [extras (in-list extrass)])
|
||||
(with-syntax* ([(lhs-pat (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs nts err-name #t lhs)]
|
||||
(with-syntax* ([(lhs-syncheck-expr lhs-pat (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs lang err-name #t lhs)]
|
||||
[((lhs-pat-ps* ...) lhs-pat*) (fix-and-extract-dq-vars #'lhs-pat)])
|
||||
(define-values (ps-rw extra-eqdqs p-names)
|
||||
(rewrite-prems #f (syntax->list extras) nts (syntax->datum #'(names ...)) 'define-metafunction))
|
||||
(rewrite-prems #f (syntax->list extras) (syntax->datum #'(names ...)) lang 'define-metafunction))
|
||||
(define-values (rhs-pats mf-clausess) (rewrite-terms (list rhs) p-names))
|
||||
(define clause-stx
|
||||
(with-syntax ([(prem-rw ...) ps-rw]
|
||||
|
|
@ -1414,11 +1429,13 @@
|
|||
[(((prev-lhs-pat-ps ...) prev-lhs-pat) ...) prev-lhs-pats*]
|
||||
[(mf-clauses ...) mf-clausess]
|
||||
[(rhs-pat) rhs-pats])
|
||||
#`((clause '(list lhs-pat rhs-pat)
|
||||
(list eqs ... (dqn '(prev-lhs-pat-ps ...) 'prev-lhs-pat 'lhs-pat) ...)
|
||||
(list prem-rw ... mf-clauses ...)
|
||||
#,lang
|
||||
'#,name)
|
||||
#`((begin
|
||||
lhs-syncheck-expr
|
||||
(clause '(list lhs-pat rhs-pat)
|
||||
(list eqs ... (dqn '(prev-lhs-pat-ps ...) 'prev-lhs-pat 'lhs-pat) ...)
|
||||
(list prem-rw ... mf-clauses ...)
|
||||
#,lang
|
||||
'#,name))
|
||||
lhs-pat
|
||||
((lhs-pat-ps* ...) lhs-pat*))))
|
||||
(values (cons clause-stx clauses)
|
||||
|
|
@ -1708,11 +1725,29 @@
|
|||
(unless (identifier? #'lang-name)
|
||||
(raise-syntax-error #f "expected an identifier" stx #'lang-name))
|
||||
(with-syntax ([(define-language-name) (generate-temporaries #'(lang-name))])
|
||||
(let ([non-terms (parse-non-terminals #'nt-defs stx)])
|
||||
(with-syntax ([((names prods ...) ...) non-terms]
|
||||
[(all-names ...) (apply append (map car non-terms))])
|
||||
(define non-terms (parse-non-terminals #'nt-defs stx))
|
||||
(with-syntax ([((names prods ...) ...) non-terms]
|
||||
[(all-names ...) (apply append (map car non-terms))]
|
||||
[(nt-ids ...)
|
||||
(for/list ([nt-def (in-list (syntax->list #'nt-defs))])
|
||||
(syntax-case nt-def ()
|
||||
[(x . whatever) #'x]))])
|
||||
(with-syntax ([bindings
|
||||
(let loop ([nt-ids (syntax->list #'(nt-ids ...))]
|
||||
[stx #'(void)])
|
||||
(cond
|
||||
[(null? nt-ids) stx]
|
||||
[else
|
||||
(define old (syntax-property stx 'disappeared-binding))
|
||||
(define new (syntax-local-introduce (car nt-ids)))
|
||||
(loop (cdr nt-ids)
|
||||
(syntax-property stx
|
||||
'disappeared-binding
|
||||
(if old (cons new old) new)))]))])
|
||||
|
||||
(quasisyntax/loc stx
|
||||
(begin
|
||||
bindings
|
||||
(define-syntax lang-name
|
||||
(make-set!-transformer
|
||||
(make-language-id
|
||||
|
|
@ -1724,10 +1759,15 @@
|
|||
[x
|
||||
(identifier? #'x)
|
||||
#'define-language-name]))
|
||||
'(all-names ...))))
|
||||
'(all-names ...)
|
||||
(to-table #'(nt-ids ...)))))
|
||||
(define define-language-name
|
||||
#,(syntax/loc stx (language form-name lang-name (all-names ...) (names prods ...) ...)))))))))]))
|
||||
|
||||
(define-for-syntax (to-table x)
|
||||
(for/hash ([id (in-list (syntax->list x))])
|
||||
(values (syntax-e id) id)))
|
||||
|
||||
(define-struct binds (source binds))
|
||||
|
||||
(define-syntax (language stx)
|
||||
|
|
@ -1736,11 +1776,12 @@
|
|||
(prune-syntax
|
||||
(let ()
|
||||
(let ([all-names (syntax->list #'(all-names ...))])
|
||||
(with-syntax ([(((r-rhs r-names r-names/ellipses) ...) ...)
|
||||
(with-syntax ([(((r-syncheck-expr r-rhs r-names r-names/ellipses) ...) ...)
|
||||
;; r-syncheck-expr has nothing interesting, I believe, so drop it
|
||||
(map (lambda (rhss)
|
||||
(map (lambda (rhs)
|
||||
(rewrite-side-conditions/check-errs
|
||||
(map syntax-e all-names)
|
||||
#'lang-id
|
||||
(syntax-e #'form-name)
|
||||
#f
|
||||
rhs))
|
||||
|
|
@ -1833,12 +1874,13 @@
|
|||
[x
|
||||
(identifier? #'x)
|
||||
#'define-language-name]))
|
||||
'(all-names ...))))))))]))
|
||||
'(all-names ...)
|
||||
(to-table #'()))))))))]))
|
||||
|
||||
(define-syntax (extend-language stx)
|
||||
(syntax-case stx ()
|
||||
[(_ lang (all-names ...) (name rhs ...) ...)
|
||||
(with-syntax ([(((r-rhs r-names r-names/ellipses) ...) ...)
|
||||
(with-syntax ([(((r-syncheck-expr r-rhs r-names r-names/ellipses) ...) ...)
|
||||
(map (lambda (rhss) (map (λ (x) (rewrite-side-conditions/check-errs
|
||||
(append (language-id-nts #'lang 'define-extended-language)
|
||||
(map syntax-e
|
||||
|
|
@ -1854,7 +1896,7 @@
|
|||
(map (λ (x) (if (identifier? x) (list x) x))
|
||||
(syntax->list (syntax (name ...))))])
|
||||
(syntax/loc stx
|
||||
(do-extend-language lang
|
||||
(do-extend-language (begin r-syncheck-expr ... ... lang)
|
||||
(list (make-nt '(uniform-names ...) (list (make-rhs `r-rhs) ...)) ...)
|
||||
(list (list '(uniform-names ...) rhs/lw ...) ...))))]))
|
||||
|
||||
|
|
@ -1992,7 +2034,8 @@
|
|||
[x
|
||||
(identifier? #'x)
|
||||
#'define-language-name]))
|
||||
'(all-names ...)))))))]))
|
||||
'(all-names ...)
|
||||
(to-table #'())))))))]))
|
||||
|
||||
(define (union-language old-langs/prefixes)
|
||||
|
||||
|
|
|
|||
|
|
@ -19,7 +19,19 @@
|
|||
|
||||
(provide (struct-out id/depth))
|
||||
|
||||
(define (rewrite-side-conditions/check-errs all-nts what bind-names? orig-stx)
|
||||
;; the result is a four-tuple (as a list) syntax object
|
||||
;; - the first is an ordinary expression that evaluates
|
||||
;; to (void), but tells check syntax about binding information
|
||||
;; - the second is an expression that, when prefixed with a
|
||||
;; quasiquote, evaluates to a pattern that can be used with
|
||||
;; match-a-pattern (at runtime).
|
||||
(define (rewrite-side-conditions/check-errs all-nts/lang-id what bind-names? orig-stx)
|
||||
(define all-nts (if (identifier? all-nts/lang-id)
|
||||
(language-id-nts all-nts/lang-id what)
|
||||
all-nts/lang-id))
|
||||
(define id-stx-table (if (identifier? all-nts/lang-id)
|
||||
(language-id-nt-identifiers all-nts/lang-id #f)
|
||||
(hash)))
|
||||
(define (expected-exact name n stx)
|
||||
(raise-syntax-error what (format "~a expected to have ~a arguments"
|
||||
name
|
||||
|
|
@ -39,6 +51,8 @@
|
|||
(let recur ([chd e] [par (hash-ref sets e #f)])
|
||||
(if (and par (not (eq? chd par))) (recur par (hash-ref sets par #f)) chd)))
|
||||
|
||||
(define void-stx #'(void))
|
||||
|
||||
(define last-contexts (make-hasheq))
|
||||
(define last-stx (make-hasheq)) ;; used for syntax error reporting
|
||||
(define assignments #hasheq())
|
||||
|
|
@ -67,6 +81,15 @@
|
|||
[else
|
||||
(hash-set! last-contexts pat-sym under)
|
||||
assignments])))))
|
||||
|
||||
(define (record-syncheck-use stx nt)
|
||||
(define the-use (build-disappeared-use id-stx-table nt stx))
|
||||
(when the-use
|
||||
(define old (syntax-property void-stx 'disappeared-use))
|
||||
(set! void-stx
|
||||
(syntax-property void-stx
|
||||
'disappeared-use
|
||||
(if old (cons the-use old) the-use)))))
|
||||
|
||||
(define ellipsis-number 0)
|
||||
|
||||
|
|
@ -188,6 +211,7 @@
|
|||
term)]
|
||||
[(memq prefix-sym all-nts)
|
||||
(record-binder term under)
|
||||
(record-syncheck-use term prefix-sym)
|
||||
(values (if mismatch?
|
||||
`(mismatch-name ,term (nt ,prefix-stx))
|
||||
`(name ,term (nt ,prefix-stx)))
|
||||
|
|
@ -212,6 +236,7 @@
|
|||
orig-stx
|
||||
term)]
|
||||
[(memq (syntax-e term) all-nts)
|
||||
(record-syncheck-use term (syntax-e term))
|
||||
(cond
|
||||
[bind-names?
|
||||
(record-binder term under)
|
||||
|
|
@ -357,8 +382,9 @@
|
|||
(let ([without-mismatch-names (filter (λ (x) (not (id/depth-mismatch? x))) names)])
|
||||
(with-syntax ([(name/ellipses ...) (map build-dots without-mismatch-names)]
|
||||
[(name ...) (map id/depth-id without-mismatch-names)]
|
||||
[term ellipsis-normalized/simplified])
|
||||
#'(term (name ...) (name/ellipses ...)))))
|
||||
[term ellipsis-normalized/simplified]
|
||||
[void-stx void-stx])
|
||||
#'(void-stx term (name ...) (name/ellipses ...)))))
|
||||
|
||||
(define-struct id/depth (id depth mismatch?))
|
||||
|
||||
|
|
|
|||
|
|
@ -28,7 +28,10 @@
|
|||
|
||||
make-language-id
|
||||
language-id-nts
|
||||
pattern-symbols)
|
||||
language-id-nt-identifiers
|
||||
pattern-symbols
|
||||
|
||||
build-disappeared-use)
|
||||
|
||||
(define-values (struct-type make-term-fn term-fn? term-fn-get term-fn-set!)
|
||||
(make-struct-type 'term-fn #f 1 0))
|
||||
|
|
@ -57,7 +60,8 @@
|
|||
(when (eq? (syntax-local-context) 'expression)
|
||||
(raise-syntax-error #f "not allowed in an expression context" stx)))
|
||||
|
||||
(define-values (language-id make-language-id language-id? language-id-get language-id-set) (make-struct-type 'language-id #f 2 0 #f '() #f 0))
|
||||
(define-values (language-id make-language-id language-id? language-id-get language-id-set)
|
||||
(make-struct-type 'language-id #f 3 0 #f '() #f 0))
|
||||
|
||||
(define (language-id-nts stx id) (language-id-getter stx id 1))
|
||||
(define (language-id-getter stx id n)
|
||||
|
|
@ -68,6 +72,7 @@
|
|||
(language-id? (set!-transformer-procedure val)))
|
||||
(raise-syntax-error id "expected an identifier defined by define-language" stx))
|
||||
(language-id-get (set!-transformer-procedure val) n)))
|
||||
(define (language-id-nt-identifiers stx id) (language-id-getter stx id 2))
|
||||
|
||||
(define pattern-symbols '(any number natural integer real string variable
|
||||
variable-not-otherwise-mentioned hole symbol))
|
||||
|
|
@ -84,3 +89,24 @@
|
|||
(define metafunc-proc-cases (make-struct-field-accessor metafunc-proc-ref 8))
|
||||
(define metafunc-proc-gen-clauses (make-struct-field-accessor metafunc-proc-ref 9))
|
||||
(define metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 10))
|
||||
|
||||
|
||||
(define (build-disappeared-use id-stx-table nt id-stx)
|
||||
(cond
|
||||
[id-stx-table
|
||||
(define table-entry (hash-ref id-stx-table nt #f))
|
||||
(cond
|
||||
[table-entry
|
||||
(define the-srcloc (vector
|
||||
(syntax-source id-stx)
|
||||
(syntax-line id-stx)
|
||||
(syntax-column id-stx)
|
||||
(syntax-position id-stx)
|
||||
;; shorten the span so it covers only up to the underscore
|
||||
(string-length (symbol->string nt))))
|
||||
(define the-id (datum->syntax table-entry nt the-srcloc id-stx))
|
||||
(syntax-property the-id 'syncheck-original #t)]
|
||||
[else
|
||||
#f])]
|
||||
[else
|
||||
#f]))
|
||||
|
|
|
|||
|
|
@ -15,7 +15,6 @@
|
|||
(provide term term-let define-term
|
||||
hole in-hole
|
||||
term-let/error-name term-let-fn term-define-fn
|
||||
term/nts
|
||||
(for-syntax term-rewrite
|
||||
term-temp->pat
|
||||
currently-expanding-term-fn
|
||||
|
|
@ -39,30 +38,39 @@
|
|||
(define-syntax (term stx)
|
||||
(syntax-case stx ()
|
||||
[(term t . kw-args)
|
||||
(with-syntax ([(lang-stx) (parse-kw-args (list lang-keyword)
|
||||
(syntax kw-args)
|
||||
stx
|
||||
(syntax-e #'form))])
|
||||
(if (syntax->datum #'lang-stx)
|
||||
(let ([lang-nts (let loop ([ls #'lang-stx])
|
||||
(define slv (syntax-local-value ls (λ () #'lang-stx)))
|
||||
(if (term-id? slv)
|
||||
(loop (term-id-prev-id slv))
|
||||
(language-id-nts ls 'term)))])
|
||||
#`(term/nts t #,lang-nts))
|
||||
#'(term/nts t #f)))]))
|
||||
(let ()
|
||||
(define lang-stx (car
|
||||
(parse-kw-args (list lang-keyword)
|
||||
(syntax kw-args)
|
||||
stx
|
||||
(syntax-e #'form))))
|
||||
(cond
|
||||
[lang-stx
|
||||
(define-values (lang-nts lang-nt-ids)
|
||||
(let loop ([ls lang-stx])
|
||||
(define slv (syntax-local-value ls (λ () lang-stx)))
|
||||
(if (term-id? slv)
|
||||
(loop (term-id-prev-id slv))
|
||||
(values (language-id-nts ls 'term)
|
||||
(language-id-nt-identifiers ls 'term)))))
|
||||
#`(term/nts t #,lang-nts #,lang-nt-ids)]
|
||||
[else
|
||||
#'(term/nts t #f #f)]))]))
|
||||
|
||||
(define-syntax (term/nts stx)
|
||||
(syntax-case stx ()
|
||||
[(_ arg nts)
|
||||
#'(#%expression (term/private arg nts))]))
|
||||
[(_ arg nts nt-ids)
|
||||
#'(#%expression (term/private arg nts nt-ids))]))
|
||||
|
||||
(define-for-syntax current-id-stx-table (make-parameter #f))
|
||||
|
||||
(define-syntax (term/private stx)
|
||||
(syntax-case stx ()
|
||||
[(_ arg-stx nts-stx)
|
||||
(with-disappeared-uses
|
||||
(let-values ([(t a-mfs) (term-rewrite/private #'arg-stx #'nts-stx #f)])
|
||||
(term-temp->unexpanded-term t a-mfs)))]))
|
||||
[(_ arg-stx nts-stx id-stx-table)
|
||||
(parameterize ([current-id-stx-table (syntax-e #'id-stx-table)])
|
||||
(with-disappeared-uses
|
||||
(let-values ([(t a-mfs) (term-rewrite/private #'arg-stx #'nts-stx #f)])
|
||||
(term-temp->unexpanded-term t a-mfs))))]))
|
||||
|
||||
(define-for-syntax (term-rewrite t names)
|
||||
(let*-values ([(t-t a-mfs) (term-rewrite/private t #`#f names)]
|
||||
|
|
@ -169,11 +177,25 @@
|
|||
(term-fn? (syntax-local-value (syntax f) (λ () #f))))
|
||||
(raise-syntax-error 'term "metafunction must be in an application" arg-stx stx)]
|
||||
[x
|
||||
(and (identifier? (syntax x))
|
||||
(term-id? (syntax-local-value (syntax x) (λ () #f))))
|
||||
(let ([id (syntax-local-value/record (syntax x) (λ (x) #t))])
|
||||
(and (identifier? #'x)
|
||||
(term-id? (syntax-local-value #'x (λ () #f))))
|
||||
(let ([id (syntax-local-value/record #'x (λ (x) #t))])
|
||||
(define stx-result (datum->syntax (term-id-id id) (syntax-e (term-id-id id)) #'x))
|
||||
|
||||
(define raw-sym (syntax-e #'x))
|
||||
(define raw-str (symbol->string raw-sym))
|
||||
(define m (regexp-match #rx"^([^_]*)_" raw-str))
|
||||
(define prefix-sym (if m
|
||||
(string->symbol (list-ref m 1))
|
||||
raw-sym))
|
||||
(check-id (syntax->datum (term-id-id id)) stx)
|
||||
(values (datum->syntax (term-id-id id) (syntax-e (term-id-id id)) (syntax x))
|
||||
|
||||
(define new-id
|
||||
(build-disappeared-use (current-id-stx-table)
|
||||
prefix-sym
|
||||
(syntax-local-introduce #'x)))
|
||||
(when new-id (record-disappeared-uses (list new-id)))
|
||||
(values stx-result
|
||||
(term-id-depth id)))]
|
||||
[x
|
||||
(defined-term-id? #'x)
|
||||
|
|
@ -223,7 +245,7 @@
|
|||
(i-loop (cdr xs))])
|
||||
(values (cons fst rst)
|
||||
(max fst-max-depth rst-max-depth))))]))])
|
||||
(values (datum->syntax stx x-rewrite stx) max-depth))]
|
||||
(values (datum->syntax stx x-rewrite stx stx) max-depth))]
|
||||
|
||||
[_ (values stx 0)]))
|
||||
|
||||
|
|
@ -341,7 +363,7 @@
|
|||
(define-syntax (term-define-fn stx)
|
||||
(syntax-case stx ()
|
||||
[(_ id exp)
|
||||
(with-syntax ([id2 (datum->syntax #'here (syntax-e #'id))])
|
||||
(with-syntax ([id2 (datum->syntax #'here (syntax-e #'id) #'id #'id)])
|
||||
(syntax
|
||||
(begin
|
||||
(define id2 exp)
|
||||
|
|
@ -363,7 +385,7 @@
|
|||
[x
|
||||
(and (identifier? #'x)
|
||||
(not (free-identifier=? (quote-syntax ...) #'x)))
|
||||
(let ([new-name (datum->syntax #'here (syntax-e #'x))])
|
||||
(let ([new-name (datum->syntax #'here (syntax-e #'x) #'x #'x)])
|
||||
(values (list #'x)
|
||||
(list new-name)
|
||||
(list depth)
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@
|
|||
(define-syntax (rsc stx)
|
||||
(syntax-case stx ()
|
||||
[(_ pat (nts ...) bind-names?)
|
||||
(with-syntax ([(pat (vars ...) (vars/ellipses ...))
|
||||
(with-syntax ([(ignore pat (vars ...) (vars/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs
|
||||
(syntax->datum #'(nts ...))
|
||||
'rsc
|
||||
|
|
|
|||
|
|
@ -728,10 +728,10 @@
|
|||
(λ (stx)
|
||||
(syntax-case stx ()
|
||||
[(f-name lang t-1 t-2 env)
|
||||
(with-syntax ([(pat-1 (names-1 ...) (names/ellipses-1 ...))
|
||||
(with-syntax ([(ignore-1 pat-1 (names-1 ...) (names/ellipses-1 ...))
|
||||
(rewrite-side-conditions/check-errs
|
||||
(language-id-nts #'lang 'f-name) 'f-name stx #'t-1)]
|
||||
[(pat-2 (names-2 ...) (names/ellipses-2 ...))
|
||||
[(ignore-2 pat-2 (names-2 ...) (names/ellipses-2 ...))
|
||||
(rewrite-side-conditions/check-errs
|
||||
(language-id-nts #'lang 'f-name) 'f-name stx #'t-2)])
|
||||
#'(unify/format 'pat-1 'pat-2 env lang))])))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user