Fixes a bug in the generation of `side-condition' patterns

The bindings supplied to `side-condition' predicates by the matcher
sometimes contain the-not-hole; the ones supplied by the generator
must be the same.
This commit is contained in:
Casey Klein 2010-12-30 09:53:36 -06:00
parent 699058d3a4
commit de8b1bc101
2 changed files with 90 additions and 87 deletions

View File

@ -162,19 +162,19 @@
(define-values/invoke-unit (generation-decisions)
(import) (export decisions^))
(define (gen-nt lang name cross? retries size attempt fillers)
(define (gen-nt lang name cross? retries size attempt filler)
(let*-values
([(productions)
(hash-ref ((if cross? rg-lang-cross rg-lang-non-cross) lang) name)]
[(terms _)
[(term _)
(let ([gen (pick-from-list
(if (zero? size)
(min-prods name productions
((if cross? base-cases-cross base-cases-non-cross)
(rg-lang-base-cases lang)))
((next-non-terminal-decision) productions)))])
(gen retries (max 0 (sub1 size)) attempt empty-env fillers))])
terms))
(gen retries (max 0 (sub1 size)) attempt empty-env filler))])
term))
(define (generate/pred name gen pred init-sz init-att retries)
(let ([pre-threshold-incr
@ -191,9 +191,9 @@
[attempt init-att])
(if (zero? remaining)
(raise-gen-fail what (format "pattern ~a" name) retries)
(let-values ([(terms env) (gen size attempt)])
(if (pred (unfilled-term terms) env)
(values terms env)
(let-values ([(term env) (gen size attempt)])
(if (pred term env)
(values term env)
(retry (sub1 remaining)
(if (incr-size? remaining) (add1 size) size)
(+ attempt
@ -205,9 +205,9 @@
(let* ([none (gensym)]
[prior (hash-ref env name none)])
(if (eq? prior none)
(let-values ([(terms env) (gen)])
(values terms (hash-set env name (unfilled-term terms))))
(values (unfilled prior) env))))
(let-values ([(term env) (gen)])
(values term (hash-set env name term)))
(values prior env))))
(define (generate-sequence gen env vars length)
(define (split-environment env)
@ -222,18 +222,18 @@
(hash-set env var (map (λ (seq-env) (hash-ref seq-env var)) seq-envs)))
env vars))
(let-values
([(seqs envs)
([(seq envs)
(let recur ([envs (split-environment env)])
(if (null? envs)
(values (unfilled null) null)
(values null null)
(let*-values
([(hds env) (gen (car envs))]
[(tls envs) (recur (cdr envs))])
(values (combine cons hds tls) (cons env envs)))))])
(values seqs (merge-environments envs))))
([(hd env) (gen (car envs))]
[(tl envs) (recur (cdr envs))])
(values (cons hd tl) (cons env envs)))))])
(values seq (merge-environments envs))))
(define ((unfilled-generator/attempts g) r s a e f)
(values (unfilled (g a)) e))
(define ((generator/attempts g) r s a e f)
(values (g a) e))
(define (mismatches-satisfied? env)
(let ([groups (make-hasheq)])
@ -258,17 +258,6 @@
(cons (make-bind (binder-name key) val) bindings)
bindings))))
(define (combine f ts us)
(match* (ts us)
[((list t) _)
(map (λ (u) (f t u)) us)]
[(_ (list u))
(map (λ (t) (f t u)) ts)]
[(_ _) (map f ts us)]))
(define unfilled-term first)
(define unfilled list)
(let*-values ([(langp lits lang-bases) (prepare-lang lang)]
[(sexpp _ sexp-bases) (prepare-lang sexp)]
[(lit-syms) (compiled-lang-literals lang)])
@ -278,26 +267,30 @@
(let* ([nt? (is-nt? (if any? sexpp langp))]
[mismatches? #f]
[generator
; retries size attempt env hole-fillers -> (values terms env)
; hole-fillers = (non-empty-listof term)
; terms = (non-empty-listof term)
; retries size attempt env filler -> (values terms env)
;
; Patterns like (in-hole C_1 p) require constructing both an unfilled context
; (exposed via the C_1 binding) and a filled context (exposed as the result).
; These terms can be constructed by first generating the unfilled context then
; constructing the filled one from it, via something like `plug', but care must
; be taken to avoid filling holes generated within `in-hole' patterns (and to
; avoid exposing the dreaded `the-not-hole' term). Instead, generators construct
; the filled and unfilled contexts simultaneously, taking multiple fillers as
; input (one of which can be `hole') and producing multiple terms as output.
; As an optimization, generators produce singleton lists when the constructed term
; contained no fillable position.
; A generator constructs both by constructing the context, using either
; `the-hole' or `the-not-hole' as appropriate, then filling it using `plug'.
; Before returning its result, a generator replaces occurrences of `the-not-hole'
; with `the-hole' to avoid exposing the distinction to the user, but
; `the-not-hole' remains in bindings supplied to side-condition predicates, to
; match the behavior of the matcher.
;
; Repeated traversals via `plug' are not asymptotically worse than simultaneously
; constructing the filled and unfilled pattern, due to languages like this one,
; which names contexts in a way that prevents any sharing.
; (define-language L
; (W hole
; ; extra parens to avoid matcher loop
; (in-hole (W_1) (+ natural hole))))
(let recur ([pat pat])
(match pat
[`number (unfilled-generator/attempts (λ (a) ((next-number-decision) a)))]
[`natural (unfilled-generator/attempts (λ (a) ((next-natural-decision) a)))]
[`integer (unfilled-generator/attempts (λ (a) ((next-integer-decision) a)))]
[`real (unfilled-generator/attempts (λ (a) ((next-real-decision) a)))]
[`number (generator/attempts (λ (a) ((next-number-decision) a)))]
[`natural (generator/attempts (λ (a) ((next-natural-decision) a)))]
[`integer (generator/attempts (λ (a) ((next-integer-decision) a)))]
[`real (generator/attempts (λ (a) ((next-real-decision) a)))]
[`(variable-except ,vars ...)
(let ([g (recur 'variable)])
(λ (r s a e f)
@ -305,7 +298,7 @@
(λ (s a) (g r s a e f))
(λ (var _) (not (memq var vars)))
s a r)))]
[`variable (unfilled-generator/attempts (λ (a) ((next-variable-decision) lits a)))]
[`variable (generator/attempts (λ (a) ((next-variable-decision) lits a)))]
[`variable-not-otherwise-mentioned
(let ([g (recur 'variable)])
(λ (r s a e f)
@ -318,9 +311,9 @@
(string->symbol (string-append (symbol->string prefix) (symbol->string suffix))))
(let ([g (recur 'variable)])
(λ (r s a e f)
(let-values ([(ts e) (g r s a e f)])
(values (unfilled (symbol-append prefix (unfilled-term ts))) e))))]
[`string (unfilled-generator/attempts (λ (a) ((next-string-decision) lits a)))]
(let-values ([(t e) (g r s a e f)])
(values (symbol-append prefix t) e))))]
[`string (generator/attempts (λ (a) ((next-string-decision) lits a)))]
[`(side-condition ,pat ,(? procedure? condition) ,guard-src-loc)
(let ([g (recur pat)])
(λ (r s a e f)
@ -331,20 +324,20 @@
[`(name ,(? symbol? id) ,p)
(let ([g (recur p)])
(λ (r s a e f)
(let-values ([(ts env) (g r s a e f)])
(values ts (hash-set env (make-binder id) (unfilled-term ts))))))]
(let-values ([(t env) (g r s a e f)])
(values t (hash-set env (make-binder id) t)))))]
[`hole (λ (r s a e f) (values f e))]
[`(in-hole ,context ,filler)
(let ([c-context (recur context)]
[c-filler (recur filler)])
(λ (r s a e f)
(let*-values ([(fillers env) (c-filler r s a e f)]
[(filled env) (c-context r s a env (cons the-hole fillers))])
(values (if (empty? (rest filled)) filled (rest filled)) env))))]
(let*-values ([(filler env) (c-filler r s a e f)]
[(context env) (c-context r s a env the-hole)])
(values (plug context filler) env))))]
[`(hide-hole ,pattern)
(let ([g (recur pattern)])
(λ (r s a e f)
(g r s a e (list the-hole))))]
(g r s a e the-not-hole)))]
[`any
(λ (r s a e f)
(let*-values ([(lang nt) ((next-any-decision) langc sexpc)]
@ -362,10 +355,10 @@
(let ([g (recur (mismatch-pattern pat))])
(set! mismatches? #t)
(λ (r s a e f)
(let-values ([(ts e) (g r s a e f)])
(values ts (hash-set e pat (unfilled-term ts))))))]
(let-values ([(t e) (g r s a e f)])
(values t (hash-set e pat t)))))]
[(or (? symbol?) (? number?) (? string?) (? boolean?) (? null?))
(λ (r s a e f) (values (unfilled pat) e))]
(λ (r s a e f) (values pat e))]
[(list-rest (struct ellipsis (name sub-pat class vars)) rest)
(let ([elemg (recur sub-pat)]
[tailg (recur rest)])
@ -377,20 +370,20 @@
(if prior
prior
(if (zero? s) 0 ((next-sequence-decision) a))))]
[(seqs env)
[(seq env)
(generate-sequence (λ (e) (elemg r s a e f)) e vars len)]
[(tails env)
[(tail env)
(let ([e (hash-set (hash-set env class len) name len)])
(tailg r s a e f))])
(values (combine append seqs tails) env))))]
(values (append seq tail) env))))]
[(list-rest hdp tlp)
(let ([hdg (recur hdp)]
[tlg (recur tlp)])
(λ (r s a e f)
(let*-values
([(hds env) (hdg r s a e f)]
[(tls env) (tlg r s a env f)])
(values (combine cons hds tls) env))))]
([(hd env) (hdg r s a e f)]
[(tl env) (tlg r s a env f)])
(values (cons hd tl) env))))]
[else
(error what "unknown pattern ~s\n" pat)]))])
(if mismatches?
@ -420,8 +413,12 @@
(λ (pat)
(let ([g (compile-pattern (reassign-classes (parse-pattern pat lang 'top-level)))])
(λ (size attempt retries)
(let-values ([(ts e) (g retries size attempt empty-env (list the-hole))])
(values (unfilled-term ts) (bindings e)))))))))
(let-values ([(t e) (g retries size attempt empty-env the-hole)])
(values (let replace-the-not-hole ([t t])
(cond [(eq? t the-not-hole) the-hole]
[(list? t) (map replace-the-not-hole t)]
[else t]))
(bindings e)))))))))
(define-struct base-cases (cross non-cross))

View File

@ -444,29 +444,20 @@
(C (c hole))
(D (d hole))
(E (e hole))
(F (f hole)))
(F (f hole))
(p (in-hole (hole hole) 4))
(q (in-hole (hole ... hole) 4)))
(test (generate-term L (in-hole 3 4) 5) 3)
(test (generate-term L (in-hole (hole hole) 4) 5) '(4 4))
(test (generate-term/decisions L (in-hole (hole ... hole) 4) 5 0 (decisions #:seq (list (λ (_) 1))))
'(4 4))
(let-syntax ([test-sequence-holes
(λ (stx)
(syntax-case stx ()
[(_ l)
#`(let ([length l]
[bindings #f])
(test (generate-term/decisions
L
(side-condition (in-hole ((name x (q C)) (... ...)) 4)
(set! bindings (term ((x C) (... ...)))))
5 0 (decisions #:seq (list (λ (_) length))))
#,(syntax/loc stx (build-list length (λ (_) '(q (c 4))))))
(test bindings
#,(syntax/loc stx (build-list length (λ (_) (term ((q (c hole)) (c hole))))))))]))])
(test-sequence-holes 3)
(test-sequence-holes 0))
(test (raised-exn-msg
exn:fail?
(test-match L p (generate-term L p 5)))
#rx"two holes")
(test (raised-exn-msg
exn:fail?
(test-match L q (generate-term/decisions L q 5 0 (decisions #:seq (list (λ (_) 1))))))
#rx"two holes")
(let ([bindings #f])
(test (generate-term
@ -476,7 +467,22 @@
0)
(term (c (d (e (f hole))))))
(test bindings (term ((c hole) (d hole) (e hole) (f hole)
(c (d hole)) (c (d (e hole))) (c (d (e (f hole)))))))))
(c (d hole)) (c (d (e hole))) (c (d (e (f hole))))))))
(test
(let/ec return
(generate-term
L
(side-condition (name C (hide-hole hole))
(return (term (in-hole C 1))))
0))
(term hole))
(test (generate-term
L
(in-hole ((hide-hole (in-hole hole hole)) hole) 1)
0)
(term (hole 1))))
(let ()
(define-language lc