`where' clauses now properly bind in metafunctions
svn: r14712
This commit is contained in:
Casey Klein
parent
83cd3964f4
commit
039d24fc17
|
|
@ -199,6 +199,42 @@
|
|||
[(_ orig-reduction-relation lang args ...)
|
||||
#'(do-reduction-relation extend-reduction-relation orig-reduction-relation #t lang args ...)]))
|
||||
|
||||
;; the withs, freshs, and side-conditions come in backwards order
|
||||
(define-for-syntax (bind-withs orig-name main stx body)
|
||||
(let loop ([stx stx]
|
||||
[body body])
|
||||
(syntax-case stx (side-condition where fresh)
|
||||
[() body]
|
||||
[((where x e) y ...)
|
||||
(loop #'(y ...) #`(term-let ([x (term e)]) #,body))]
|
||||
[((side-condition s ...) y ...)
|
||||
(loop #'(y ...) #`(and s ... #,body))]
|
||||
[((fresh x) y ...)
|
||||
(identifier? #'x)
|
||||
(loop #'(y ...) #`(term-let ([x (variable-not-in #,main 'x)]) #,body))]
|
||||
[((fresh x name) y ...)
|
||||
(identifier? #'x)
|
||||
(loop #'(y ...)
|
||||
#`(term-let ([x (let ([the-name (term name)])
|
||||
(verify-name-ok '#,orig-name the-name)
|
||||
(variable-not-in #,main the-name))])
|
||||
#,body))]
|
||||
[((fresh (y) (x ...)) z ...)
|
||||
(loop #'(z ...)
|
||||
#`(term-let ([(y #,'...)
|
||||
(variables-not-in #,main
|
||||
(map (λ (_ignore_) 'y)
|
||||
(term (x ...))))])
|
||||
#,body))]
|
||||
[((fresh (y) (x ...) names) z ...)
|
||||
(loop #'(z ...)
|
||||
#`(term-let ([(y #,'...)
|
||||
(let ([the-names (term names)]
|
||||
[len-counter (term (x ...))])
|
||||
(verify-names-ok '#,orig-name the-names len-counter)
|
||||
(variables-not-in #,main the-names))])
|
||||
#,body))])))
|
||||
|
||||
(define-struct successful (result))
|
||||
|
||||
(define-syntax-set (do-reduction-relation)
|
||||
|
|
@ -608,42 +644,6 @@
|
|||
#,(bind-withs orig-name #'main sides/withs/freshs
|
||||
#'(make-successful (term to)))))))))))
|
||||
|
||||
;; the withs, freshs, and side-conditions come in backwards order
|
||||
(define (bind-withs orig-name main stx body)
|
||||
(let loop ([stx stx]
|
||||
[body body])
|
||||
(syntax-case stx (side-condition where fresh)
|
||||
[() body]
|
||||
[((where x e) y ...)
|
||||
(loop #'(y ...) #`(term-let ([x (term e)]) #,body))]
|
||||
[((side-condition s ...) y ...)
|
||||
(loop #'(y ...) #`(and s ... #,body))]
|
||||
[((fresh x) y ...)
|
||||
(identifier? #'x)
|
||||
(loop #'(y ...) #`(term-let ([x (variable-not-in #,main 'x)]) #,body))]
|
||||
[((fresh x name) y ...)
|
||||
(identifier? #'x)
|
||||
(loop #'(y ...)
|
||||
#`(term-let ([x (let ([the-name (term name)])
|
||||
(verify-name-ok '#,orig-name the-name)
|
||||
(variable-not-in #,main the-name))])
|
||||
#,body))]
|
||||
[((fresh (y) (x ...)) z ...)
|
||||
(loop #'(z ...)
|
||||
#`(term-let ([(y #,'...)
|
||||
(variables-not-in #,main
|
||||
(map (λ (_ignore_) 'y)
|
||||
(term (x ...))))])
|
||||
#,body))]
|
||||
[((fresh (y) (x ...) names) z ...)
|
||||
(loop #'(z ...)
|
||||
#`(term-let ([(y #,'...)
|
||||
(let ([the-names (term names)]
|
||||
[len-counter (term (x ...))])
|
||||
(verify-names-ok '#,orig-name the-names len-counter)
|
||||
(variables-not-in #,main the-names))])
|
||||
#,body))])))
|
||||
|
||||
(define (process-extras stx orig-name name-table extras)
|
||||
(let ([the-name #f]
|
||||
[the-name-stx #f]
|
||||
|
|
@ -1012,16 +1012,19 @@
|
|||
(loop name (cdr names))]))])
|
||||
|
||||
(with-syntax ([(((tl-side-conds ...) ...)
|
||||
(tl-bindings ...))
|
||||
(extract-side-conditions (syntax-e #'name) stx #'((stuff ...) ...))])
|
||||
(tl-bindings ...)
|
||||
(tl-side-cond/binds ...))
|
||||
(parse-extras #'((stuff ...) ...))])
|
||||
(let ([lang-nts (language-id-nts #'lang 'define-metafunction)])
|
||||
(with-syntax ([(tl-withs ...) (map (λ (sc/b) (bind-withs syn-error-name '() sc/b #t))
|
||||
(syntax->list #'(tl-side-cond/binds ...)))])
|
||||
(with-syntax ([(side-conditions-rewritten ...)
|
||||
(map (λ (x) (rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
'define-metafunction
|
||||
#t
|
||||
x))
|
||||
(syntax->list (syntax ((side-condition lhs (and tl-side-conds ...)) ...))))]
|
||||
(syntax->list (syntax ((side-condition lhs tl-withs) ...))))]
|
||||
[dom-side-conditions-rewritten
|
||||
(and dom-ctcs
|
||||
(rewrite-side-conditions/check-errs
|
||||
|
|
@ -1119,7 +1122,7 @@
|
|||
'name)))
|
||||
(term-define-fn name name2))
|
||||
'disappeared-use
|
||||
(map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))]
|
||||
(map syntax-local-introduce (syntax->list #'(original-names ...))))))))))))]
|
||||
[(_ prev-metafunction name lang clauses ...)
|
||||
(begin
|
||||
(unless (identifier? #'name)
|
||||
|
|
@ -1199,31 +1202,38 @@
|
|||
(syntax->list #'(x ...)))
|
||||
(raise-syntax-error syn-error-name "error checking failed.2" stx))]))
|
||||
|
||||
(define (extract-side-conditions name stx stuffs)
|
||||
(let loop ([stuffs (syntax->list stuffs)]
|
||||
(define (parse-extras extras)
|
||||
(let loop ([stuffs (syntax->list extras)]
|
||||
[side-conditionss '()]
|
||||
[bindingss '()])
|
||||
[bindingss '()]
|
||||
[bothss '()])
|
||||
(cond
|
||||
[(null? stuffs) (list (reverse side-conditionss)
|
||||
(reverse bindingss))]
|
||||
(reverse bindingss)
|
||||
(reverse bothss))]
|
||||
[else
|
||||
(let s-loop ([stuff (syntax->list (car stuffs))]
|
||||
[side-conditions '()]
|
||||
[bindings '()])
|
||||
[bindings '()]
|
||||
[boths '()])
|
||||
(cond
|
||||
[(null? stuff) (loop (cdr stuffs)
|
||||
(cons (reverse side-conditions) side-conditionss)
|
||||
(cons (reverse bindings) bindingss))]
|
||||
(cons (reverse bindings) bindingss)
|
||||
; Want these in reverse order.
|
||||
(cons boths bothss))]
|
||||
[else
|
||||
(syntax-case (car stuff) (where side-condition)
|
||||
[(side-condition tl-side-conds ...)
|
||||
(s-loop (cdr stuff)
|
||||
(append (syntax->list #'(tl-side-conds ...)) side-conditions)
|
||||
bindings)]
|
||||
bindings
|
||||
(cons (car stuff) boths))]
|
||||
[(where x e)
|
||||
(s-loop (cdr stuff)
|
||||
side-conditions
|
||||
(cons #'(x e) bindings))]
|
||||
(cons #'(x e) bindings)
|
||||
(cons (car stuff) boths))]
|
||||
[_
|
||||
(raise-syntax-error 'define-metafunction
|
||||
"expected a side-condition or where clause"
|
||||
|
|
|
|||
|
|
@ -820,11 +820,13 @@
|
|||
; check-metafunction
|
||||
(let ()
|
||||
(define-language empty)
|
||||
|
||||
(define-metafunction empty
|
||||
[(m 1) whatever]
|
||||
[(m 2) whatever])
|
||||
(define-metafunction empty
|
||||
[(n (side-condition any #f)) any])
|
||||
|
||||
(let ([generated null])
|
||||
(test (begin
|
||||
(output
|
||||
|
|
@ -832,6 +834,20 @@
|
|||
(check-metafunction m (λ (t) (set! generated (cons t generated))) #:attempts 1)))
|
||||
generated)
|
||||
(reverse '((1) (2)))))
|
||||
|
||||
(test
|
||||
(let/ec k
|
||||
(define-language L (n 2))
|
||||
(define-metafunction L
|
||||
[(f n)
|
||||
n
|
||||
(where number_2 ,(add1 (term n)))
|
||||
(where number_3 ,(add1 (term number_2)))
|
||||
(side-condition (k (term number_3)))]
|
||||
[(f any) 0])
|
||||
(check-metafunction f (λ (_) #t)))
|
||||
4)
|
||||
|
||||
(test (output (λ () (check-metafunction m (λ (_) #t)))) #rx"no counterexamples")
|
||||
(test (output (λ () (check-metafunction m (curry eq? 1))))
|
||||
#rx"check-metafunction:.*counterexample found after 1 attempt with clause #1")
|
||||
|
|
|
|||
|
|
@ -482,6 +482,17 @@
|
|||
(test (term (f z))
|
||||
(term ((z z) (z z)))))
|
||||
|
||||
(let ()
|
||||
(define-metafunction empty-language
|
||||
[(f number_1)
|
||||
number_1
|
||||
(where number_2 ,(add1 (term number_1)))
|
||||
(where number_3 ,(add1 (term number_2)))
|
||||
(side-condition (and (number? (term number_3))
|
||||
(= (term number_3) 4)))]
|
||||
[(f any) 0])
|
||||
(test (term (f 2)) 2))
|
||||
|
||||
(let ()
|
||||
(define-language x-lang
|
||||
(x variable))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user