Makes cross' work better with hide-hole'
Fixes PR 11579
This commit is contained in:
Casey Klein
parent
e8130a2fd1
commit
1ad2b1b938
|
|
@ -370,21 +370,23 @@ before the pattern compiler is invoked.
|
|||
;; The number result is the number of times that the nt appeared in the pattern.
|
||||
(define (build-compatible-context-maker clang-ht pattern prefix)
|
||||
(let ([count 0])
|
||||
(values
|
||||
(define maker
|
||||
(let loop ([pattern pattern])
|
||||
(define (untouched-pattern _)
|
||||
(values pattern #f))
|
||||
(match pattern
|
||||
[`any (lambda (l) 'any)]
|
||||
[`number (lambda (l) 'number)]
|
||||
[`string (lambda (l) 'string)]
|
||||
[`natural (lambda (l) 'natural)]
|
||||
[`integer (lambda (l) 'integer)]
|
||||
[`real (lambda (l) 'real)]
|
||||
[`variable (lambda (l) 'variable)]
|
||||
[`(variable-except ,vars ...) (lambda (l) pattern)]
|
||||
[`(variable-prefix ,var) (lambda (l) pattern)]
|
||||
[`variable-not-otherwise-mentioned (λ (l) pattern)]
|
||||
[`hole (lambda (l) 'hole)]
|
||||
[(? string?) (lambda (l) pattern)]
|
||||
[`any untouched-pattern]
|
||||
[`number untouched-pattern]
|
||||
[`string untouched-pattern]
|
||||
[`natural untouched-pattern]
|
||||
[`integer untouched-pattern]
|
||||
[`real untouched-pattern]
|
||||
[`variable untouched-pattern]
|
||||
[`(variable-except ,vars ...) untouched-pattern]
|
||||
[`(variable-prefix ,var) untouched-pattern]
|
||||
[`variable-not-otherwise-mentioned untouched-pattern]
|
||||
[`hole untouched-pattern]
|
||||
[(? string?) untouched-pattern]
|
||||
[(? symbol?)
|
||||
(cond
|
||||
[(hash-ref clang-ht pattern #f)
|
||||
|
|
@ -393,73 +395,70 @@ before the pattern compiler is invoked.
|
|||
(let ([fst (car (unbox l))])
|
||||
(set-box! l (cdr (unbox l)))
|
||||
(if fst
|
||||
`(cross ,(symbol-append prefix '- pattern))
|
||||
pattern)))]
|
||||
[else
|
||||
(lambda (l) pattern)])]
|
||||
(values `(cross ,(symbol-append prefix '- pattern)) #t)
|
||||
(values pattern #f))))]
|
||||
[else untouched-pattern])]
|
||||
[`(name ,name ,pat)
|
||||
(let ([patf (loop pat)])
|
||||
(lambda (l)
|
||||
`(name ,name ,(patf l))))]
|
||||
(let-values ([(p h?) (patf l)])
|
||||
(values `(name ,name ,p) h?))))]
|
||||
[`(in-hole ,context ,contractum)
|
||||
(let ([match-context (loop context)]
|
||||
[match-contractum (loop contractum)])
|
||||
(lambda (l)
|
||||
`(in-hole ,(match-context l)
|
||||
,(match-contractum l))))]
|
||||
(let-values ([(ctxt _) (match-context l)]
|
||||
[(ctct h?) (match-contractum l)])
|
||||
(values `(in-hole ,ctxt ,ctct) h?))))]
|
||||
[`(hide-hole ,p)
|
||||
(let ([m (loop p)])
|
||||
(lambda (l)
|
||||
`(hide-hole ,(m l))))]
|
||||
(let-values ([(p h?) (m l)])
|
||||
(if h?
|
||||
(values p #t)
|
||||
(values `(hide-hole ,p) #f)))))]
|
||||
[`(side-condition ,pat ,condition ,expr)
|
||||
(let ([patf (loop pat)])
|
||||
(lambda (l)
|
||||
`(side-condition ,(patf l) ,condition ,expr)))]
|
||||
(let-values ([(p h?) (patf l)])
|
||||
(values `(side-condition ,p ,condition ,expr) h?))))]
|
||||
[(? list?)
|
||||
(let ([f/pats
|
||||
(let l-loop ([pattern pattern])
|
||||
(cond
|
||||
[(null? pattern) null]
|
||||
[(null? (cdr pattern))
|
||||
(list (vector (loop (car pattern))
|
||||
#f
|
||||
#f))]
|
||||
[(eq? (cadr pattern) '...)
|
||||
(cons (vector (loop (car pattern))
|
||||
#t
|
||||
(car pattern))
|
||||
(l-loop (cddr pattern)))]
|
||||
[else
|
||||
(cons (vector (loop (car pattern))
|
||||
#f
|
||||
#f)
|
||||
(l-loop (cdr pattern)))]))])
|
||||
(lambda (l)
|
||||
(let loop ([f/pats f/pats])
|
||||
(cond
|
||||
[(null? f/pats) null]
|
||||
[else
|
||||
(let ([f/pat (car f/pats)])
|
||||
(cond
|
||||
[(vector-ref f/pat 1)
|
||||
(let ([new ((vector-ref f/pat 0) l)]
|
||||
[pat (vector-ref f/pat 2)])
|
||||
(if (equal? new pat)
|
||||
(list* pat
|
||||
'...
|
||||
(loop (cdr f/pats)))
|
||||
(list* (vector-ref f/pat 2)
|
||||
'...
|
||||
new
|
||||
(vector-ref f/pat 2)
|
||||
'...
|
||||
(loop (cdr f/pats)))))]
|
||||
[else
|
||||
(cons ((vector-ref f/pat 0) l)
|
||||
(loop (cdr f/pats)))]))]))))]
|
||||
[else
|
||||
(lambda (l) pattern)]))
|
||||
count)))
|
||||
(define pre-cross
|
||||
(let l-loop ([ps pattern])
|
||||
(match ps
|
||||
['() '()]
|
||||
[(list-rest p '... ps*)
|
||||
(cons (list (loop p) p) (l-loop ps*))]
|
||||
[(cons p ps*)
|
||||
(cons (list (loop p) #f) (l-loop ps*))])))
|
||||
(λ (l)
|
||||
(define any-cross? #f)
|
||||
(define post-cross
|
||||
(map (match-lambda
|
||||
[(list f r?)
|
||||
(let-values ([(p h?) (f l)])
|
||||
(set! any-cross? (or any-cross? h?))
|
||||
(list p h? r?))])
|
||||
pre-cross))
|
||||
(define (hide p)
|
||||
(if any-cross? `(hide-hole ,p) p))
|
||||
(values
|
||||
(foldr (λ (post tail)
|
||||
(match post
|
||||
[(list p* #t (and (not #f) p))
|
||||
`(,(hide p) ... ,p* ,(hide p) ... . ,tail)]
|
||||
[(list p #f (not #f))
|
||||
`(,(hide p) ... . ,tail)]
|
||||
[(list p* #t #f)
|
||||
`(,p* . ,tail)]
|
||||
[(list p #f #f)
|
||||
`(,(hide p) . ,tail)]))
|
||||
'()
|
||||
post-cross)
|
||||
any-cross?))]
|
||||
[else untouched-pattern])))
|
||||
(values (λ (l) (let-values ([(p _) (maker l)]) p))
|
||||
count)))
|
||||
|
||||
;; build-list-nt-label : lang -> hash[symbol -o> boolean]
|
||||
(define (build-list-nt-label lang)
|
||||
|
|
|
|||
|
|
@ -557,22 +557,22 @@
|
|||
(list
|
||||
(make-nt 'ctxt-ctxt
|
||||
(list (make-rhs 'hole)
|
||||
(make-rhs `(+ (cross ctxt-ctxt) exp))
|
||||
(make-rhs `(+ ctxt (cross ctxt-exp)))
|
||||
(make-rhs `(+ (cross ctxt-exp) ctxt))
|
||||
(make-rhs `(+ exp (cross ctxt-ctxt)))))
|
||||
(make-rhs `((hide-hole +) (cross ctxt-ctxt) (hide-hole exp)))
|
||||
(make-rhs `((hide-hole +) (hide-hole ctxt) (cross ctxt-exp)))
|
||||
(make-rhs `((hide-hole +) (cross ctxt-exp) (hide-hole ctxt)))
|
||||
(make-rhs `((hide-hole +) (hide-hole exp) (cross ctxt-ctxt)))))
|
||||
(make-nt 'ctxt-exp
|
||||
(list (make-rhs `(+ (cross ctxt-exp) exp))
|
||||
(make-rhs `(+ exp (cross ctxt-exp)))))
|
||||
(list (make-rhs `((hide-hole +) (cross ctxt-exp) (hide-hole exp)))
|
||||
(make-rhs `((hide-hole +) (hide-hole exp) (cross ctxt-exp)))))
|
||||
(make-nt 'exp-ctxt
|
||||
(list (make-rhs `(+ (cross exp-ctxt) exp))
|
||||
(make-rhs `(+ ctxt (cross exp-exp)))
|
||||
(make-rhs `(+ (cross exp-exp) ctxt))
|
||||
(make-rhs `(+ exp (cross exp-ctxt)))))
|
||||
(list (make-rhs `((hide-hole +) (cross exp-ctxt) (hide-hole exp)))
|
||||
(make-rhs `((hide-hole +) (hide-hole ctxt) (cross exp-exp)))
|
||||
(make-rhs `((hide-hole +) (cross exp-exp) (hide-hole ctxt)))
|
||||
(make-rhs `((hide-hole +) (hide-hole exp) (cross exp-ctxt)))))
|
||||
(make-nt 'exp-exp
|
||||
(list (make-rhs 'hole)
|
||||
(make-rhs `(+ (cross exp-exp) exp))
|
||||
(make-rhs `(+ exp (cross exp-exp)))))))
|
||||
(make-rhs `((hide-hole +) (cross exp-exp) (hide-hole exp)))
|
||||
(make-rhs `((hide-hole +) (hide-hole exp) (cross exp-exp)))))))
|
||||
|
||||
(run-test
|
||||
'compatible-context-language2
|
||||
|
|
@ -581,23 +581,23 @@
|
|||
(list (make-nt 'm (list (make-rhs '(m m)) (make-rhs '(+ m m)) (make-rhs 'v)))
|
||||
(make-nt 'v (list (make-rhs 'number) (make-rhs '(lambda (x) m))))))
|
||||
(list
|
||||
(make-nt 'v-v (list (make-rhs 'hole) (make-rhs (list 'lambda (list 'x) (list 'cross 'v-m)))))
|
||||
(make-nt 'v-v (list (make-rhs 'hole) (make-rhs '((hide-hole lambda) (hide-hole (x)) (cross v-m)))))
|
||||
(make-nt 'v-m
|
||||
(list
|
||||
(make-rhs (list (list 'cross 'v-m) 'm))
|
||||
(make-rhs (list 'm (list 'cross 'v-m)))
|
||||
(make-rhs (list '+ (list 'cross 'v-m) 'm))
|
||||
(make-rhs (list '+ 'm (list 'cross 'v-m)))
|
||||
(make-rhs (list 'cross 'v-v))))
|
||||
(make-nt 'm-v (list (make-rhs (list 'lambda (list 'x) (list 'cross 'm-m)))))
|
||||
(make-rhs '((cross v-m) (hide-hole m)))
|
||||
(make-rhs '((hide-hole m) (cross v-m)))
|
||||
(make-rhs '((hide-hole +) (cross v-m) (hide-hole m)))
|
||||
(make-rhs '((hide-hole +) (hide-hole m) (cross v-m)))
|
||||
(make-rhs '(cross v-v))))
|
||||
(make-nt 'm-v (list (make-rhs '((hide-hole lambda) (hide-hole (x)) (cross m-m)))))
|
||||
(make-nt 'm-m
|
||||
(list
|
||||
(make-rhs 'hole)
|
||||
(make-rhs (list (list 'cross 'm-m) 'm))
|
||||
(make-rhs (list 'm (list 'cross 'm-m)))
|
||||
(make-rhs (list '+ (list 'cross 'm-m) 'm))
|
||||
(make-rhs (list '+ 'm (list 'cross 'm-m)))
|
||||
(make-rhs (list 'cross 'm-v))))))
|
||||
(make-rhs '((cross m-m) (hide-hole m)))
|
||||
(make-rhs '((hide-hole m) (cross m-m)))
|
||||
(make-rhs '((hide-hole +) (cross m-m) (hide-hole m)))
|
||||
(make-rhs '((hide-hole +) (hide-hole m) (cross m-m)))
|
||||
(make-rhs '(cross m-v))))))
|
||||
|
||||
(run-test
|
||||
'compatible-context-language3
|
||||
|
|
@ -607,10 +607,14 @@
|
|||
(make-nt 'seven (list (make-rhs 7)))))
|
||||
`(,(make-nt
|
||||
'm-m
|
||||
`(,(make-rhs 'hole) ,(make-rhs `((cross m-m) seven m)) ,(make-rhs `(m seven (cross m-m)))))
|
||||
`(,(make-rhs 'hole)
|
||||
,(make-rhs `((cross m-m) (hide-hole seven) (hide-hole m)))
|
||||
,(make-rhs `((hide-hole m) (hide-hole seven) (cross m-m)))))
|
||||
,(make-nt
|
||||
'seven-m
|
||||
`(,(make-rhs `((cross seven-m) seven m)) ,(make-rhs `(m (cross seven-seven) m)) ,(make-rhs `(m seven (cross seven-m)))))
|
||||
`(,(make-rhs `((cross seven-m) (hide-hole seven) (hide-hole m)))
|
||||
,(make-rhs `((hide-hole m) (cross seven-seven) (hide-hole m)))
|
||||
,(make-rhs `((hide-hole m) (hide-hole seven) (cross seven-m)))))
|
||||
,(make-nt 'seven-seven `(,(make-rhs 'hole)))))
|
||||
|
||||
(run-test
|
||||
|
|
|
|||
|
|
@ -287,6 +287,63 @@
|
|||
;; not a syntax error since first e is not a binder
|
||||
(test (pair? (redex-match L ((cross e) e ...) (term ((hole 2) 1)))) #t))
|
||||
|
||||
(define-syntax (test-match stx)
|
||||
(syntax-case stx ()
|
||||
[(_ actual (((var val) ...) ...))
|
||||
#`(test (equal?
|
||||
(apply
|
||||
set
|
||||
(for/list ([match actual])
|
||||
(for/list ([bind (match-bindings match)])
|
||||
(list (bind-name bind) (bind-exp bind)))))
|
||||
(apply set (list (list (list 'var (term val)) ...) ...)))
|
||||
#,(syntax/loc stx #t))]))
|
||||
|
||||
;; cross
|
||||
(let ()
|
||||
(define-language L
|
||||
(e (e e)
|
||||
(cont (hide-hole E))
|
||||
number
|
||||
x)
|
||||
(E hole
|
||||
(e ... E e ...))
|
||||
(x variable-not-otherwise-mentioned))
|
||||
(test-match
|
||||
(redex-match
|
||||
L
|
||||
(in-hole (cross e) e)
|
||||
(term (cont (1 hole))))
|
||||
(((e (cont (1 hole))))
|
||||
((e 1)))))
|
||||
(let ()
|
||||
(define-language L
|
||||
(e (e e ...)
|
||||
x
|
||||
v)
|
||||
(v (λ (x ...) e)
|
||||
cont-val
|
||||
number)
|
||||
(cont-val (cont (hide-hole E)))
|
||||
(E hole
|
||||
(in-hole L E))
|
||||
(L (v ... hole e ...))
|
||||
(x variable-not-otherwise-mentioned))
|
||||
|
||||
;; no "found two holes" error
|
||||
(test (redex-match L (cross e) (term (cont ((λ (x) x) hole)))) #f)
|
||||
|
||||
(test-match
|
||||
(redex-match
|
||||
L
|
||||
(in-hole (cross e) e)
|
||||
(term ((cont ((λ (x) x) hole)) (λ (y) y))))
|
||||
(((e x))
|
||||
((e ((cont ((λ (x) x) hole)) (λ (y) y))))
|
||||
((e y))
|
||||
((e (λ (y) y)))
|
||||
((e (cont ((λ (x) x) hole)))))))
|
||||
|
||||
;; test caching
|
||||
(let ()
|
||||
(define match? #t)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user