Fixed PR 8765
svn: r16564
This commit is contained in:
Casey Klein
parent
c993533814
commit
a021b75a67
|
|
@ -9,4 +9,4 @@
|
|||
(make-struct-type 'term-fn #f 1 0))
|
||||
(define term-fn-get-id (make-struct-field-accessor term-fn-get 0))
|
||||
|
||||
(define-struct term-id (id))
|
||||
(define-struct term-id (id depth))
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
(module term-test mzscheme
|
||||
(module term-test scheme
|
||||
(require "term.ss"
|
||||
"matcher.ss"
|
||||
"test-util.ss")
|
||||
|
|
@ -67,10 +67,7 @@
|
|||
(term ((in-hole E x) ...)))
|
||||
(term (1 2 3)))
|
||||
|
||||
(fprintf (current-error-port) "term-test.ss commented out test that fails; matches PR 8765\n")
|
||||
|
||||
#;
|
||||
(test (term-let-fn ((metafun (λ (x) x)))
|
||||
(test (term-let-fn ((metafun car))
|
||||
(term-let ((x 'whatever)
|
||||
((y ...) '(4 5 6)))
|
||||
(term (((metafun x) y) ...))))
|
||||
|
|
@ -81,4 +78,26 @@
|
|||
(term ((y (metafun 1)) ...))))
|
||||
'((4 1) (5 1) (6 1)))
|
||||
|
||||
(test (term-let-fn ((f (compose add1 car)))
|
||||
(term-let (((x ...) '(1 2 3))
|
||||
((y ...) '(a b c)))
|
||||
(term (((f x) y) ...))))
|
||||
'((2 a) (3 b) (4 c)))
|
||||
|
||||
(test (term-let-fn ((f (curry foldl + 0)))
|
||||
(term-let (((x ...) '(1 2 3)))
|
||||
(term (f x ...))))
|
||||
6)
|
||||
|
||||
(test (term-let-fn ((f (compose add1 car)))
|
||||
(term-let (((x ...) '(1 2 3))
|
||||
(((y ...) ...) '((a b c) (d e f) (g h i))))
|
||||
(term ((((f x) y) ...) ...))))
|
||||
'(((2 a) (3 b) (4 c)) ((2 d) (3 e) (4 f)) ((2 g) (3 h) (4 i))))
|
||||
|
||||
(test (term-let-fn ((f (curry foldl + 0)))
|
||||
(term-let ((((x ...) ...) '((1 2) (3 4 5) (6))))
|
||||
(term ((f x ...) ...))))
|
||||
'(3 12 6))
|
||||
|
||||
(print-tests-passed 'term-test.ss))
|
||||
|
|
|
|||
|
|
@ -5,7 +5,10 @@
|
|||
syntax/private/util/misc)
|
||||
"matcher.ss")
|
||||
|
||||
(provide term term-let term-let/error-name term-let-fn term-define-fn)
|
||||
(provide term term-let term-let/error-name term-let-fn term-define-fn hole in-hole)
|
||||
|
||||
(define-syntax (hole stx) (raise-syntax-error 'hole "used outside of term"))
|
||||
(define-syntax (in-hole stx) (raise-syntax-error 'in-hole "used outside of term"))
|
||||
|
||||
(define (with-syntax* stx)
|
||||
(syntax-case stx ()
|
||||
|
|
@ -15,62 +18,45 @@
|
|||
(define-syntax (term stx)
|
||||
(syntax-case stx ()
|
||||
[(_ arg)
|
||||
#`(term-let-fn ((#,(datum->syntax stx 'in-hole)
|
||||
(λ (x)
|
||||
(unless (and (list? x)
|
||||
(= 2 (length x)))
|
||||
(error 'in-hole "expected two arguments, got ~s" x))
|
||||
(apply plug x))))
|
||||
(term/private arg))]))
|
||||
#`(term/private arg)]))
|
||||
|
||||
(define-syntax (term/private orig-stx)
|
||||
(define outer-bindings '())
|
||||
|
||||
(define (rewrite stx)
|
||||
(let-values ([(rewritten has-term-let-bound-id?)
|
||||
(rewrite/has-term-let-bound-id? stx)])
|
||||
(let-values ([(rewritten _) (rewrite/max-depth stx 0)])
|
||||
rewritten))
|
||||
|
||||
(define (rewrite/has-term-let-bound-id? stx)
|
||||
(let loop ([stx stx]
|
||||
[depth 0])
|
||||
(define (rewrite-application fn args depth)
|
||||
(let-values ([(rewritten max-depth) (rewrite/max-depth args depth)])
|
||||
(let ([result-id (car (generate-temporaries '(f-results)))])
|
||||
(with-syntax ([fn fn])
|
||||
(let loop ([func (syntax (λ (x) (fn (syntax->datum x))))]
|
||||
[args rewritten]
|
||||
[res result-id]
|
||||
[args-depth (min depth max-depth)])
|
||||
(with-syntax ([func func]
|
||||
[args args]
|
||||
[res res])
|
||||
(if (zero? args-depth)
|
||||
(begin
|
||||
(set! outer-bindings
|
||||
(cons (syntax [res (func (quasisyntax args))])
|
||||
outer-bindings))
|
||||
(values result-id (min depth max-depth)))
|
||||
(loop (syntax (λ (l) (map func (syntax->list l))))
|
||||
(syntax (args (... ...)))
|
||||
(syntax (res (... ...)))
|
||||
(sub1 args-depth)))))))))
|
||||
|
||||
(define (rewrite/max-depth stx depth)
|
||||
(syntax-case stx (unquote unquote-splicing in-hole hole)
|
||||
[(metafunc-name arg ...)
|
||||
(and (identifier? (syntax metafunc-name))
|
||||
(term-fn? (syntax-local-value (syntax metafunc-name) (λ () #f))))
|
||||
(let-values ([(rewritten has-term-let-bound-id?) (loop (syntax (arg ...)) depth)])
|
||||
(let ([term-fn (syntax-local-value/catch (syntax metafunc-name) (λ (x) #t))])
|
||||
(with-syntax ([f (term-fn-get-id term-fn)])
|
||||
(cond
|
||||
[has-term-let-bound-id?
|
||||
(with-syntax ([(f-results) (generate-temporaries '(f-results))])
|
||||
(let d-loop ([arg-dots rewritten]
|
||||
[fres (syntax f-results)]
|
||||
[func (syntax (lambda (x) (f (syntax->datum x))))]
|
||||
[depth depth])
|
||||
(cond
|
||||
[(zero? depth)
|
||||
(let ([res
|
||||
(with-syntax ([fres fres]
|
||||
[func func]
|
||||
[arg-dots arg-dots])
|
||||
(set! outer-bindings (cons (syntax [fres (func (quasisyntax arg-dots))])
|
||||
outer-bindings))
|
||||
(syntax f-results))])
|
||||
(values res #t))]
|
||||
[else
|
||||
(with-syntax ([dots (quote-syntax ...)]
|
||||
[arg-dots arg-dots]
|
||||
[fres fres])
|
||||
(d-loop (syntax (arg-dots dots))
|
||||
(syntax (fres dots))
|
||||
(with-syntax ([f func])
|
||||
(syntax (lambda (l) (map f (syntax->list l)))))
|
||||
(- depth 1)))])))]
|
||||
[else
|
||||
(with-syntax ([rewritten rewritten])
|
||||
(values (syntax/loc stx (unsyntax (f (syntax->datum (quasisyntax rewritten)))))
|
||||
#f))]))))]
|
||||
(rewrite-application (term-fn-get-id (syntax-local-value/catch (syntax metafunc-name) (λ (x) #t)))
|
||||
(syntax (arg ...))
|
||||
depth)]
|
||||
[f
|
||||
(and (identifier? (syntax f))
|
||||
(term-fn? (syntax-local-value (syntax f) (λ () #f))))
|
||||
|
|
@ -78,29 +64,30 @@
|
|||
[x
|
||||
(and (identifier? (syntax x))
|
||||
(term-id? (syntax-local-value (syntax x) (λ () #f))))
|
||||
(values (term-id-id (syntax-local-value/catch (syntax x) (λ (x) #t))) #t)]
|
||||
(let ([id (syntax-local-value/catch (syntax x) (λ (x) #t))])
|
||||
(values (term-id-id id) (term-id-depth id)))]
|
||||
[(unquote x)
|
||||
(values (syntax (unsyntax x)) #f)]
|
||||
(values (syntax (unsyntax x)) 0)]
|
||||
[(unquote . x)
|
||||
(raise-syntax-error 'term "malformed unquote" orig-stx stx)]
|
||||
[(unquote-splicing x)
|
||||
(values (syntax (unsyntax-splicing x)) #f)]
|
||||
(values (syntax (unsyntax-splicing x)) 0)]
|
||||
[(unquote-splicing . x)
|
||||
(raise-syntax-error 'term "malformed unquote splicing" orig-stx stx)]
|
||||
[(in-hole id body)
|
||||
(values (syntax (unsyntax (plug (term id) (term body)))) #f)]
|
||||
(rewrite-application (syntax (λ (x) (apply plug x))) (syntax (id body)) depth)]
|
||||
[(in-hole . x)
|
||||
(raise-syntax-error 'term "malformed in-hole" orig-stx stx)]
|
||||
[hole (values (syntax (unsyntax the-hole)) #f)]
|
||||
[hole (values (syntax (unsyntax the-hole)) 0)]
|
||||
|
||||
|
||||
[() (values stx #f)]
|
||||
[() (values stx 0)]
|
||||
[(x ... . y)
|
||||
(not (null? (syntax->list #'(x ...))))
|
||||
(let-values ([(x-rewrite has-term-let-bound-id?)
|
||||
(let-values ([(x-rewrite max-depth)
|
||||
(let i-loop ([xs (syntax->list (syntax (x ...)))])
|
||||
(cond
|
||||
[(null? xs) (loop #'y depth)]
|
||||
[(null? xs) (rewrite/max-depth #'y depth)]
|
||||
[else
|
||||
(let ([new-depth (if (and (not (null? (cdr xs)))
|
||||
(identifier? (cadr xs))
|
||||
|
|
@ -108,19 +95,18 @@
|
|||
(cadr xs)))
|
||||
(+ depth 1)
|
||||
depth)])
|
||||
(let-values ([(fst fst-has-term-let-bound-id?)
|
||||
(loop (car xs) new-depth)]
|
||||
[(rst rst-has-term-let-bound-id?)
|
||||
(let-values ([(fst fst-max-depth)
|
||||
(rewrite/max-depth (car xs) new-depth)]
|
||||
[(rst rst-max-depth)
|
||||
(i-loop (cdr xs))])
|
||||
(values (cons fst rst)
|
||||
(or fst-has-term-let-bound-id?
|
||||
rst-has-term-let-bound-id?))))]))])
|
||||
(max fst-max-depth rst-max-depth))))]))])
|
||||
|
||||
(with-syntax ([x-rewrite x-rewrite])
|
||||
(values (syntax/loc stx x-rewrite)
|
||||
has-term-let-bound-id?)))]
|
||||
max-depth)))]
|
||||
|
||||
[_ (values stx #f)])))
|
||||
[_ (values stx 0)]))
|
||||
|
||||
(syntax-case orig-stx ()
|
||||
[(_ arg)
|
||||
|
|
@ -157,38 +143,48 @@
|
|||
(define-syntax (term-let/error-name stx)
|
||||
(syntax-case stx ()
|
||||
[(_ error-name ([x1 rhs1] [x rhs] ...) body1 body2 ...)
|
||||
(let-values ([(orig-names new-names new-x1)
|
||||
(let loop ([stx #'x1])
|
||||
(syntax-case stx ()
|
||||
(let-values ([(orig-names new-names depths new-x1)
|
||||
(let loop ([stx #'x1] [depth 0])
|
||||
(define ((combine orig-names new-names depths new-pat)
|
||||
orig-names* new-names* depths* new-pat*)
|
||||
(values (append orig-names orig-names*)
|
||||
(append new-names new-names*)
|
||||
(append depths depths*)
|
||||
(cons new-pat new-pat*)))
|
||||
(syntax-case stx (...)
|
||||
[x
|
||||
(and (identifier? #'x)
|
||||
(not (free-identifier=? (quote-syntax ...) #'x)))
|
||||
(let ([new-name (car (generate-temporaries (list #'x)))])
|
||||
(values (list #'x)
|
||||
(list new-name)
|
||||
(list depth)
|
||||
new-name))]
|
||||
[(x ...)
|
||||
(let l-loop ([lst (syntax->list #'(x ...))])
|
||||
(cond
|
||||
[(null? lst)
|
||||
(values '() '() '())]
|
||||
[else
|
||||
(let-values ([(hd-orig-names hd-new-names hd-new-pattern)
|
||||
(loop (car lst))]
|
||||
[(tl-orig-names tl-new-names tl-new-pattern)
|
||||
(l-loop (cdr lst))])
|
||||
(values (append hd-orig-names tl-orig-names)
|
||||
(append hd-new-names tl-new-names)
|
||||
(cons hd-new-pattern tl-new-pattern)))]))]
|
||||
[(x (... ...) . xs)
|
||||
(let-values ([(orig-names new-names depths new-pat)
|
||||
(call-with-values
|
||||
(λ () (loop #'xs depth))
|
||||
(call-with-values
|
||||
(λ () (loop #'x (add1 depth)))
|
||||
combine))])
|
||||
(values orig-names new-names depths
|
||||
(list* (car new-pat) #'(... ...) (cdr new-pat))))]
|
||||
[(x . xs)
|
||||
(call-with-values
|
||||
(λ () (loop #'xs depth))
|
||||
(call-with-values
|
||||
(λ () (loop #'x depth))
|
||||
combine))]
|
||||
[_
|
||||
(values '() '() stx)]))])
|
||||
(values '() '() '() stx)]))])
|
||||
(with-syntax ([(orig-names ...) orig-names]
|
||||
[(new-names ...) new-names]
|
||||
[(depths ...) depths]
|
||||
[new-x1 new-x1])
|
||||
(syntax
|
||||
(syntax-case rhs1 ()
|
||||
[new-x1
|
||||
(let-syntax ([orig-names (make-term-id #'new-names)] ...)
|
||||
(let-syntax ([orig-names (make-term-id #'new-names (syntax-e #'depths))] ...)
|
||||
(term-let/error-name error-name ((x rhs) ...) body1 body2 ...))]
|
||||
[_ (error 'error-name "term ~s does not match pattern ~s" rhs1 'x1)]))))]
|
||||
[(_ error-name () body1 body2 ...)
|
||||
|
|
|
|||
|
|
@ -485,6 +485,14 @@ for two @scheme[term-let]-bound identifiers bound to lists of
|
|||
different lengths to appear together inside an ellipsis.
|
||||
}
|
||||
|
||||
@defidform[hole]{ Recognized specially within
|
||||
@scheme[term]. A @scheme[hole] form is an
|
||||
error elsewhere. }
|
||||
|
||||
@defidform[in-hole]{ Recognized specially within
|
||||
@scheme[reduction-relation]. An @scheme[in-hole] form is an
|
||||
error elsewhere. }
|
||||
|
||||
@defform/subs[(term-let ([tl-pat expr] ...) body)
|
||||
([tl-pat identifier (tl-pat-ele ...)]
|
||||
[tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@
|
|||
|
||||
(provide reduction-relation
|
||||
--> fresh with ;; keywords for reduction-relation
|
||||
hole in-hole ;; keywords for term
|
||||
extend-reduction-relation
|
||||
reduction-relation?
|
||||
|
||||
|
|
|
|||
|
|
@ -1,11 +1,12 @@
|
|||
v4.2.3
|
||||
|
||||
* added support for collecting metafunction coverage, using the
|
||||
'relation-coverage' parameter. This includes a backwards
|
||||
incompatible change: the parameter's value is now a list of
|
||||
coverage structures, to allow coverage collection for multiple
|
||||
metafunctions and reduction relations at once.
|
||||
|
||||
* redex/reduction-semantics exports the names `hole' and `in-hole'
|
||||
(and `term' no longer captures those names).
|
||||
|
||||
* minor bug fixes
|
||||
|
||||
v4.2.2
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user