Added check-metafunction and check-reduction-relation. Fixed bug in
generation of `any' pattern. svn: r12974
This commit is contained in:
Casey Klein
parent
b58664d1f8
commit
f402605fed
|
|
@ -11,8 +11,10 @@
|
|||
(require (for-syntax (lib "name.ss" "syntax")
|
||||
"rewrite-side-conditions.ss"
|
||||
"term-fn.ss"
|
||||
"underscore-allowed.ss"
|
||||
(lib "boundmap.ss" "syntax")
|
||||
scheme/base))
|
||||
scheme/base
|
||||
(prefix-in pattern- scheme/match)))
|
||||
|
||||
(define (language-nts lang)
|
||||
(hash-map (compiled-lang-ht lang) (λ (x y) x)))
|
||||
|
|
@ -440,16 +442,17 @@
|
|||
(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)])
|
||||
(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))])
|
||||
(let-values ([(names names/ellipses) (extract-names lang-nts orig-name #t (syntax rhs-from))])
|
||||
(with-syntax ([(names ...) names]
|
||||
[(names/ellipses ...) names/ellipses]
|
||||
[side-conditions-rewritten (rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
orig-name
|
||||
#t
|
||||
[side-conditions-rewritten (rewrite-side-conds
|
||||
(rewrite-node-pat (syntax-e (syntax lhs-frm-id))
|
||||
(syntax->datum (syntax rhs-from))))]
|
||||
(syntax rhs-from)))]
|
||||
[fresh-rhs-from (rewrite-side-conds
|
||||
(freshen-names #'rhs-from #'lhs-frm-id lang-nts orig-name))]
|
||||
[lang lang])
|
||||
(map
|
||||
(λ (child-proc)
|
||||
|
|
@ -460,19 +463,51 @@
|
|||
(λ (bindings rhs-binder)
|
||||
(term-let ([lhs-to-id rhs-binder]
|
||||
[names/ellipses (lookup-binding bindings 'names)] ...)
|
||||
(term rhs-to)))
|
||||
#,child-proc))
|
||||
(term rhs-to)))
|
||||
#,child-proc
|
||||
`fresh-rhs-from))
|
||||
(get-choices stx orig-name bm #'lang
|
||||
(syntax lhs-arrow)
|
||||
name-table lang-id
|
||||
allow-zero-rules?)))))]))
|
||||
allow-zero-rules?)))))]))
|
||||
(define (rewrite-node-pat id term)
|
||||
(let loop ([term term])
|
||||
(cond
|
||||
[(eq? id term) `(name ,id any)]
|
||||
[(pair? term) (cons (loop (car term))
|
||||
(loop (cdr term)))]
|
||||
[else term])))
|
||||
(let loop ([t term])
|
||||
(syntax-case t (side-condition)
|
||||
[(side-condition p c)
|
||||
#`(side-condition #,(loop #'p) c)]
|
||||
[(p ...)
|
||||
(map loop (syntax->list #'(p ...)))]
|
||||
[else
|
||||
(if (and (identifier? t) (eq? id (syntax-e t)))
|
||||
`(name ,id any)
|
||||
t)])))
|
||||
|
||||
(define (freshen-names pat hole-id nts what)
|
||||
(define (fresh x)
|
||||
(gensym
|
||||
(if (or (memq x nts) (memq x underscore-allowed))
|
||||
(string-append (symbol->string x) "_")
|
||||
x)))
|
||||
(let-values ([(bound _) (extract-names nts what #t pat #f)])
|
||||
(let ([renames (make-bound-identifier-mapping)])
|
||||
(for-each
|
||||
(λ (x)
|
||||
(unless (bound-identifier=? x hole-id)
|
||||
(bound-identifier-mapping-put! renames x (fresh (syntax-e x)))))
|
||||
bound)
|
||||
(let recur ([p pat])
|
||||
(syntax-case p (side-condition)
|
||||
[(side-condition p c)
|
||||
#`(side-condition
|
||||
#,(recur #'p)
|
||||
(term-let (#,@(bound-identifier-mapping-map renames (λ (x y) #`(#,x (term #,y)))))
|
||||
c))]
|
||||
[(p ...)
|
||||
#`(#,@(map recur (syntax->list #'(p ...))))]
|
||||
[else
|
||||
(if (identifier? p)
|
||||
(bound-identifier-mapping-get renames p (λ () p))
|
||||
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)])
|
||||
|
|
@ -484,7 +519,7 @@
|
|||
orig-name
|
||||
#t
|
||||
from)]
|
||||
[to to]
|
||||
[to to #;#`,(begin (printf "~s\n" #,name) (term #,to))]
|
||||
[name name]
|
||||
[lang lang]
|
||||
[(names ...) names]
|
||||
|
|
@ -639,6 +674,18 @@
|
|||
(cons (format " ~s" (syntax->datum (car stxs)))
|
||||
(loop (cdr stxs)))])))))
|
||||
|
||||
(define (substitute from to pat)
|
||||
(let recur ([p pat])
|
||||
(syntax-case p (side-condition)
|
||||
[(side-condition p c)
|
||||
#`(side-condition #,(recur #'p) c)]
|
||||
[(p ...)
|
||||
#`(#,@(map recur (syntax->list #'(p ...))))]
|
||||
[else
|
||||
(if (and (identifier? p) (bound-identifier=? p from))
|
||||
to
|
||||
p)])))
|
||||
|
||||
(define (verify-name-ok orig-name the-name)
|
||||
(unless (symbol? the-name)
|
||||
(error orig-name "expected a single name, got ~s" the-name)))
|
||||
|
|
@ -679,7 +726,12 @@
|
|||
(apply append (map reduction-relation-lws lst))
|
||||
`any)))
|
||||
|
||||
(define (do-node-match lhs-frm-id lhs-to-id pat rhs-proc child-make-proc)
|
||||
(define (do-node-match lhs-frm-id lhs-to-id pat rhs-proc child-make-proc rhs-from)
|
||||
(define (subst from to in)
|
||||
(let recur ([p in])
|
||||
(cond [(eq? from p) to]
|
||||
[(pair? p) (map recur p)]
|
||||
[else p])))
|
||||
;; need call to make-rewrite-proc
|
||||
;; also need a test case here to check duplication of names.
|
||||
(make-rewrite-proc
|
||||
|
|
@ -701,7 +753,8 @@
|
|||
(λ (x) (f (rhs-proc (mtch-bindings (car mtchs)) x)))
|
||||
acc)))]))
|
||||
other-matches)))))
|
||||
(rewrite-proc-name child-make-proc)))
|
||||
(rewrite-proc-name child-make-proc)
|
||||
(subst lhs-frm-id (rewrite-proc-lhs child-make-proc) rhs-from)))
|
||||
|
||||
(define (do-leaf-match name pat proc)
|
||||
(make-rewrite-proc
|
||||
|
|
@ -717,7 +770,8 @@
|
|||
mtchs
|
||||
other-matches)
|
||||
other-matches)))))
|
||||
name))
|
||||
name
|
||||
pat))
|
||||
|
||||
(define-syntax (test-match stx)
|
||||
(syntax-case stx ()
|
||||
|
|
@ -758,7 +812,7 @@
|
|||
(symbol->string (bind-name y))))))
|
||||
|
||||
(define-values (struct:metafunc-proc make-metafunc-proc metafunc-proc? metafunc-proc-ref metafunc-proc-set!)
|
||||
(make-struct-type 'metafunc-proc #f 9 0 #f null (current-inspector) 0))
|
||||
(make-struct-type 'metafunc-proc #f 10 0 #f null (current-inspector) 0))
|
||||
(define metafunc-proc-pict-info (make-struct-field-accessor metafunc-proc-ref 1))
|
||||
(define metafunc-proc-lang (make-struct-field-accessor metafunc-proc-ref 2))
|
||||
(define metafunc-proc-multi-arg? (make-struct-field-accessor metafunc-proc-ref 3))
|
||||
|
|
@ -767,6 +821,7 @@
|
|||
(define metafunc-proc-rhss (make-struct-field-accessor metafunc-proc-ref 6))
|
||||
(define metafunc-proc-in-dom? (make-struct-field-accessor metafunc-proc-ref 7))
|
||||
(define metafunc-proc-dom-pat (make-struct-field-accessor metafunc-proc-ref 8))
|
||||
(define metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 9))
|
||||
(define-struct metafunction (proc))
|
||||
|
||||
(define-syntax (in-domain? stx)
|
||||
|
|
@ -937,7 +992,8 @@
|
|||
cps
|
||||
rhss
|
||||
(let ([name (lambda (x) (name-predicate x))]) name)
|
||||
`dom-side-conditions-rewritten))
|
||||
`dom-side-conditions-rewritten
|
||||
`(side-conditions-rewritten ...)))
|
||||
`dom-side-conditions-rewritten
|
||||
`codom-side-conditions-rewritten
|
||||
'name))
|
||||
|
|
@ -1714,6 +1770,7 @@
|
|||
metafunc-proc-rhss
|
||||
metafunc-proc-in-dom?
|
||||
metafunc-proc-dom-pat
|
||||
metafunc-proc-lhs-pats
|
||||
|
||||
(struct-out binds))
|
||||
|
||||
|
|
|
|||
|
|
@ -1,9 +1,10 @@
|
|||
(module rewrite-side-conditions mzscheme
|
||||
(module rewrite-side-conditions scheme/base
|
||||
(require (lib "list.ss")
|
||||
"underscore-allowed.ss")
|
||||
(require-for-template mzscheme
|
||||
"term.ss"
|
||||
"matcher.ss")
|
||||
(require (for-template
|
||||
mzscheme
|
||||
"term.ss"
|
||||
"matcher.ss"))
|
||||
|
||||
(provide rewrite-side-conditions/check-errs
|
||||
extract-names
|
||||
|
|
@ -85,7 +86,7 @@
|
|||
(define-struct id/depth (id depth))
|
||||
|
||||
;; extract-names : syntax syntax -> (values (listof syntax) (listof syntax[x | (x ...) | ((x ...) ...) | ...]))
|
||||
(define (extract-names all-nts what bind-names? orig-stx)
|
||||
(define (extract-names all-nts what bind-names? orig-stx [rhs-only? #t])
|
||||
(let* ([dups
|
||||
(let loop ([stx orig-stx]
|
||||
[names null]
|
||||
|
|
@ -115,8 +116,8 @@
|
|||
[else
|
||||
(if (or (null? (cdr pats))
|
||||
(not (identifier? (cadr pats)))
|
||||
(not (or (module-identifier=? (quote-syntax ...)
|
||||
(cadr pats))
|
||||
(not (or (free-identifier=? (quote-syntax ...)
|
||||
(cadr pats))
|
||||
(let ([inside (syntax-e (cadr pats))])
|
||||
(regexp-match #rx"^\\.\\.\\._" (symbol->string inside))))))
|
||||
(i-loop (cdr pats)
|
||||
|
|
@ -125,7 +126,8 @@
|
|||
(loop (car pats) names (+ depth 1))))]))]
|
||||
[x
|
||||
(and (identifier? (syntax x))
|
||||
(binds-in-right-hand-side? all-nts bind-names? (syntax x)))
|
||||
((if rhs-only? binds-in-right-hand-side? binds?)
|
||||
all-nts bind-names? (syntax x)))
|
||||
(cons (make-id/depth (syntax x) depth) names)]
|
||||
[else names]))]
|
||||
[no-dups (filter-duplicates what orig-stx dups)])
|
||||
|
|
@ -141,14 +143,16 @@
|
|||
[dots (quote-syntax ...)])
|
||||
(syntax (rest dots)))])))
|
||||
|
||||
|
||||
(define (binds-in-right-hand-side? nts bind-names? x)
|
||||
(define (binds? nts bind-names? x)
|
||||
(or (and bind-names? (memq (syntax-e x) nts))
|
||||
(and bind-names? (memq (syntax-e x) underscore-allowed))
|
||||
(let ([str (symbol->string (syntax-e x))])
|
||||
(and (regexp-match #rx"_" str)
|
||||
(not (regexp-match #rx"^\\.\\.\\._" str))
|
||||
(not (regexp-match #rx"_!_" str))))))
|
||||
(regexp-match #rx"_" (symbol->string (syntax-e x)))))
|
||||
|
||||
(define (binds-in-right-hand-side? nts bind-names? x)
|
||||
(and (binds? nts bind-names? x)
|
||||
(let ([str (symbol->string (syntax-e x))])
|
||||
(and (not (regexp-match #rx"^\\.\\.\\._" str))
|
||||
(not (regexp-match #rx"_!_" str))))))
|
||||
|
||||
(define (filter-duplicates what orig-stx dups)
|
||||
(let loop ([dups dups])
|
||||
|
|
@ -158,8 +162,8 @@
|
|||
(cons
|
||||
(car dups)
|
||||
(filter (lambda (x)
|
||||
(let ([same-id? (module-identifier=? (id/depth-id x)
|
||||
(id/depth-id (car dups)))])
|
||||
(let ([same-id? (free-identifier=? (id/depth-id x)
|
||||
(id/depth-id (car dups)))])
|
||||
(when same-id?
|
||||
(unless (equal? (id/depth-depth x)
|
||||
(id/depth-depth (car dups)))
|
||||
|
|
@ -167,7 +171,7 @@
|
|||
(make-exn:fail:syntax
|
||||
(format "~a: found the same binder, ~s, at different depths, ~a and ~a"
|
||||
what
|
||||
(syntax-object->datum (id/depth-id x))
|
||||
(syntax->datum (id/depth-id x))
|
||||
(id/depth-depth x)
|
||||
(id/depth-depth (car dups)))
|
||||
(current-continuation-marks)
|
||||
|
|
|
|||
|
|
@ -90,6 +90,21 @@
|
|||
(test (pick-char 0 null (make-random 65)) #\a)
|
||||
(test (random-string null null 1 0 (make-random 65)) "a"))
|
||||
|
||||
(let ()
|
||||
(define-language L
|
||||
(a 5 (x a) #:binds x a)
|
||||
(b 4))
|
||||
(test ((pick-nt 'dontcare) 'a L '(x) 1)
|
||||
(nt-rhs (car (compiled-lang-lang L))))
|
||||
(test ((pick-nt 'dontcare (make-random 1)) 'a L '(x) preferred-production-threshold)
|
||||
(nt-rhs (car (compiled-lang-lang L))))
|
||||
(let ([pref (car (nt-rhs (car (compiled-lang-lang L))))])
|
||||
(test ((pick-nt (make-immutable-hash `((a ,pref))) (make-random 0))
|
||||
'a L '(x) preferred-production-threshold)
|
||||
(list pref)))
|
||||
(test ((pick-nt 'dontcare) 'sexp sexp null preferred-production-threshold)
|
||||
(nt-rhs (car (compiled-lang-lang sexp)))))
|
||||
|
||||
(define-syntax exn:fail-message
|
||||
(syntax-rules ()
|
||||
[(_ expr)
|
||||
|
|
@ -101,7 +116,9 @@
|
|||
(make-exn-not-raised))))]))
|
||||
|
||||
(define (patterns . selectors)
|
||||
(map (λ (selector) (λ (name prods vars size) (list (selector prods))))
|
||||
(map (λ (selector)
|
||||
(λ (name lang vars size)
|
||||
(list (selector (nt-rhs (nt-by-name lang name))))))
|
||||
selectors))
|
||||
|
||||
(define (iterator name items)
|
||||
|
|
@ -145,7 +162,7 @@
|
|||
|
||||
;; Generate (λ (x) x)
|
||||
(test
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lc e 1 0
|
||||
(decisions #:var (list (λ _ 'x) (λ _'x))
|
||||
#:nt (patterns third first first first)))
|
||||
|
|
@ -153,14 +170,14 @@
|
|||
|
||||
;; Generate pattern that's not a non-terminal
|
||||
(test
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lc (x x x_1 x_1) 1 0
|
||||
(decisions #:var (list (λ _ 'x) (λ _ 'y))))
|
||||
'(x x y y))
|
||||
|
||||
; After choosing (e e), size decremented forces each e to x.
|
||||
(test
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lc e 1 0
|
||||
(decisions #:nt (patterns first)
|
||||
#:var (list (λ _ 'x) (λ _ 'y))))
|
||||
|
|
@ -176,7 +193,7 @@
|
|||
(let* ([x null]
|
||||
[prepend! (λ (c l b a) (begin (set! x (cons (car b) x)) 'x))])
|
||||
(test (begin
|
||||
(generate/decisions lang a 5 0 (decisions #:var (list (λ _ 'x) prepend! prepend!)))
|
||||
(generate-term lang a 5 0 (decisions #:var (list (λ _ 'x) prepend! prepend!)))
|
||||
x)
|
||||
'(x x))))
|
||||
|
||||
|
|
@ -187,7 +204,7 @@
|
|||
(x (variable-except λ)))
|
||||
(test
|
||||
(exn:fail-message
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
postfix e 2 0
|
||||
(decisions #:var (list (λ _ 'x) (λ _ 'y))
|
||||
#:nt (patterns third second first first))))
|
||||
|
|
@ -198,7 +215,7 @@
|
|||
(define-language var
|
||||
(e (variable-except x y)))
|
||||
(test
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
var e 2 0
|
||||
(decisions #:var (list (λ _ 'x) (λ _ 'y) (λ _ 'x) (λ _ 'z))))
|
||||
'z))
|
||||
|
|
@ -215,25 +232,25 @@
|
|||
(n number)
|
||||
(z 4))
|
||||
(test
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lang a 2 0
|
||||
(decisions #:num (build-list 3 (λ (n) (λ (_) n)))
|
||||
#:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 1))))
|
||||
`(0 1 2 "foo" "foo" "foo" "bar" #t))
|
||||
(test (generate/decisions lang b 5 0 (decisions #:seq (list (λ (_) 0))))
|
||||
(test (generate-term lang b 5 0 (decisions #:seq (list (λ (_) 0))))
|
||||
null)
|
||||
(test (generate/decisions lang c 5 0 (decisions #:seq (list (λ (_) 0))))
|
||||
(test (generate-term lang c 5 0 (decisions #:seq (list (λ (_) 0))))
|
||||
null)
|
||||
(test (generate/decisions lang d 5 0 (decisions #:seq (list (λ (_) 2))))
|
||||
(test (generate-term lang d 5 0 (decisions #:seq (list (λ (_) 2))))
|
||||
'(4 4 4 4 (4 4) (4 4)))
|
||||
(test (exn:fail-message (generate lang e 5))
|
||||
(test (exn:fail-message (generate-term lang e 5))
|
||||
#rx"generate: unable to generate pattern e")
|
||||
(test (generate/decisions lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null)
|
||||
(test (generate/decisions lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
|
||||
(test (generate-term lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null)
|
||||
(test (generate-term lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
|
||||
(decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 2) (λ (_) 3) (λ (_) 4)
|
||||
(λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 1) (λ (_) 3))))
|
||||
'((0 0 0) (0 0 0 0) (1 1 1)))
|
||||
(test (generate/decisions lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
|
||||
(test (generate-term lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
|
||||
(decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 2) (λ (_) 3) (λ (_) 5))))
|
||||
'((0 0 0) (0 0 0 0) (1 1 1) (1 1 1 1 1))))
|
||||
|
||||
|
|
@ -247,7 +264,7 @@
|
|||
;; x and y bound in body
|
||||
(test
|
||||
(let/ec k
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lc e 10 0
|
||||
(decisions #:var (list (λ _ 'x) (λ _ 'y) (λ (c l b a) (k b)))
|
||||
#:nt (patterns first first first third first)
|
||||
|
|
@ -257,7 +274,7 @@
|
|||
(let ()
|
||||
(define-language lang (e (variable-prefix pf)))
|
||||
(test
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lang e 5 0
|
||||
(decisions #:var (list (λ _ 'x))))
|
||||
'pfx))
|
||||
|
|
@ -271,7 +288,7 @@
|
|||
(define-language lang
|
||||
(e number (e_1 e_2 e e_1 e_2)))
|
||||
(test
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lang e 5 0
|
||||
(decisions #:nt (patterns second first first first)
|
||||
#:num (list (λ _ 2) (λ _ 3) (λ _ 4))))
|
||||
|
|
@ -283,7 +300,7 @@
|
|||
(x variable))
|
||||
(test
|
||||
(let/ec k
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lang e 5 0
|
||||
(decisions #:var (list (λ _ 'x) (λ (c l b a) (k b))))))
|
||||
'(x)))
|
||||
|
|
@ -294,17 +311,17 @@
|
|||
(b (c_!_1 c_!_1 c_!_1))
|
||||
(c 1 2))
|
||||
(test
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lang a 5 0
|
||||
(decisions #:num (list (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 2))))
|
||||
'(1 1 2))
|
||||
(test
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lang (number_!_1 number_!_2 number_!_1) 5 0
|
||||
(decisions #:num (list (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 2))))
|
||||
'(1 1 2))
|
||||
(test
|
||||
(exn:fail-message (generate lang b 5000))
|
||||
(exn:fail-message (generate-term lang b 5000))
|
||||
#rx"unable"))
|
||||
|
||||
(let ()
|
||||
|
|
@ -313,7 +330,7 @@
|
|||
(f foo bar))
|
||||
(test
|
||||
(let/ec k
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lang e 5 0
|
||||
(decisions #:str (list (λ (c l a) (k (cons (sort c char<=?) (sort l string<=?))))))))
|
||||
(cons '(#\a #\b #\f #\o #\r)
|
||||
|
|
@ -327,28 +344,28 @@
|
|||
(d (side-condition (x_1 x_1 x) (not (eq? (term x_1) 'x))) #:binds x_1 x)
|
||||
(e (side-condition (x_1 x_!_2 x_!_2) (not (eq? (term x_1) 'x))))
|
||||
(x variable))
|
||||
(test (generate lang b 5) 43)
|
||||
(test (generate lang (side-condition a (odd? (term a))) 5) 43)
|
||||
(test (exn:fail-message (generate lang c 5))
|
||||
(test (generate-term lang b 5) 43)
|
||||
(test (generate-term lang (side-condition a (odd? (term a))) 5) 43)
|
||||
(test (exn:fail-message (generate-term lang c 5))
|
||||
#rx"unable to generate")
|
||||
(test ; binding works for with side-conditions failure/retry
|
||||
(let/ec k
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lang d 5 0
|
||||
(decisions #:var (list (λ _ 'x) (λ _ 'x) (λ _ 'y) (λ (c l b a) (k b))))))
|
||||
'(y))
|
||||
(test ; mismatch patterns work with side-condition failure/retry
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lang e 5 0
|
||||
(decisions #:var (list (λ _ 'x) (λ _ 'x) (λ _ 'y) (λ _ 'y) (λ _ 'x) (λ _ 'y))))
|
||||
'(y x y))
|
||||
(test ; generate compiles side-conditions in pattern
|
||||
(generate/decisions lang (side-condition x_1 (not (eq? (term x_1) 'x))) 5 0
|
||||
(generate-term lang (side-condition x_1 (not (eq? (term x_1) 'x))) 5 0
|
||||
(decisions #:var (list (λ _ 'x) (λ _ 'y))))
|
||||
'y)
|
||||
(test ; bindings within ellipses collected properly
|
||||
(let/ec k
|
||||
(generate/decisions lang (side-condition (((number_1 3) ...) ...) (k (term ((number_1 ...) ...)))) 5 0
|
||||
(generate-term lang (side-condition (((number_1 3) ...) ...) (k (term ((number_1 ...) ...)))) 5 0
|
||||
(decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4))
|
||||
#:num (build-list 7 (λ (n) (λ (_) n))))))
|
||||
'((0 1 2) (3 4 5 6))))
|
||||
|
|
@ -360,9 +377,9 @@
|
|||
(c (side-condition (name x d) (zero? (term x))))
|
||||
(d 2 1 0)
|
||||
(e ((side-condition (name d_1 d) (zero? (term d_1))) d_1)))
|
||||
(test (generate lang a 5) 4)
|
||||
(test (generate lang c 5) 0)
|
||||
(test (generate lang e 5) '(0 0)))
|
||||
(test (generate-term lang a 5) 4)
|
||||
(test (generate-term lang c 5) 0)
|
||||
(test (generate-term lang e 5) '(0 0)))
|
||||
|
||||
(let ()
|
||||
(define-language lang
|
||||
|
|
@ -380,28 +397,28 @@
|
|||
(y variable))
|
||||
|
||||
(test
|
||||
(generate/decisions
|
||||
(generate-term
|
||||
lang (in-hole A number ) 5 0
|
||||
(decisions
|
||||
#:nt (patterns second second first first third first second first first)
|
||||
#:num (build-list 5 (λ (x) (λ (_) x)))))
|
||||
'(+ (+ 1 2) (+ 0 (+ 3 4))))
|
||||
|
||||
(test (generate lang (in-hole (in-hole (1 hole) hole) 5) 5) '(1 5))
|
||||
(test (generate lang (hole 4) 5) (term (hole 4)))
|
||||
(test (generate/decisions lang (variable_1 (in-hole C variable_1)) 5 0
|
||||
(test (generate-term lang (in-hole (in-hole (1 hole) hole) 5) 5) '(1 5))
|
||||
(test (generate-term lang (hole 4) 5) (term (hole 4)))
|
||||
(test (generate-term lang (variable_1 (in-hole C variable_1)) 5 0
|
||||
(decisions #:var (list (λ _ 'x) (λ _ 'y) (λ _ 'x))))
|
||||
'(x x))
|
||||
(test (generate/decisions lang (variable_!_1 (in-hole C variable_!_1)) 5 0
|
||||
(test (generate-term lang (variable_!_1 (in-hole C variable_!_1)) 5 0
|
||||
(decisions #:var (list (λ _ 'x) (λ _ 'x) (λ _ 'x) (λ _ 'y))))
|
||||
'(x y))
|
||||
(test (let/ec k (generate/decisions lang d 5 0 (decisions #:var (list (λ _ 'x) (λ (c l b a) (k b))))))
|
||||
(test (let/ec k (generate-term lang d 5 0 (decisions #:var (list (λ _ 'x) (λ (c l b a) (k b))))))
|
||||
'(x))
|
||||
(test (generate/decisions lang e 5 0 (decisions #:num (list (λ _ 1) (λ _ 2))))
|
||||
(test (generate-term lang e 5 0 (decisions #:num (list (λ _ 1) (λ _ 2))))
|
||||
'((2 (1 1)) 1))
|
||||
(test (generate/decisions lang g 5 0 (decisions #:num (list (λ _ 1) (λ _ 2) (λ _ 1) (λ _ 0))))
|
||||
(test (generate-term lang g 5 0 (decisions #:num (list (λ _ 1) (λ _ 2) (λ _ 1) (λ _ 0))))
|
||||
'(1 0))
|
||||
(test (generate/decisions lang h 5 0 (decisions #:num (list (λ _ 1) (λ _ 2) (λ _ 3))))
|
||||
(test (generate-term lang h 5 0 (decisions #:num (list (λ _ 1) (λ _ 2) (λ _ 3))))
|
||||
'((2 ((3 (2 1)) 3)) 1)))
|
||||
|
||||
(let ()
|
||||
|
|
@ -409,7 +426,7 @@
|
|||
(e (e e) (+ e e) x v)
|
||||
(v (λ (x) e) number)
|
||||
(x variable-not-otherwise-mentioned))
|
||||
(test (generate/decisions lc x 5 0 (decisions #:var (list (λ _ 'λ) (λ _ '+) (λ _ 'x))))
|
||||
(test (generate-term lc x 5 0 (decisions #:var (list (λ _ 'λ) (λ _ '+) (λ _ 'x))))
|
||||
'x))
|
||||
|
||||
(let ()
|
||||
|
|
@ -423,14 +440,14 @@
|
|||
(list four 'f))
|
||||
(test (call-with-values (λ () (pick-any four (make-random 1))) list)
|
||||
(list sexp 'sexp))
|
||||
(test (generate/decisions four any 5 0 (decisions #:any (list (λ _ (values four 'e))))) 4)
|
||||
(test (generate/decisions four any 5 0
|
||||
(test (generate-term four any 5 0 (decisions #:any (list (λ _ (values four 'e))))) 4)
|
||||
(test (generate-term four any 5 0
|
||||
(decisions #:any (list (λ _ (values sexp 'sexp)))
|
||||
#:nt (patterns fifth second second second)
|
||||
#:seq (list (λ _ 3))
|
||||
#:str (list (λ _ "foo") (λ _ "bar") (λ _ "baz"))))
|
||||
'("foo" "bar" "baz"))
|
||||
(test (generate/decisions empty any 5 0 (decisions #:nt (patterns first)
|
||||
(test (generate-term empty any 5 0 (decisions #:nt (patterns first)
|
||||
#:var (list (λ _ 'x))))
|
||||
'x))
|
||||
|
||||
|
|
@ -438,7 +455,7 @@
|
|||
(let ()
|
||||
(define-language lang
|
||||
(e (hide-hole (in-hole ((hide-hole hole) hole) 1))))
|
||||
(test (generate lang e 5) (term (hole 1))))
|
||||
(test (generate-term lang e 5) (term (hole 1))))
|
||||
|
||||
(define (output-error-port thunk)
|
||||
(let ([port (open-output-string)])
|
||||
|
|
@ -452,14 +469,11 @@
|
|||
(e x (e e) v)
|
||||
(v (λ (x) e))
|
||||
(x variable-not-otherwise-mentioned))
|
||||
(test (generate/decisions lang (cross e) 3 0
|
||||
(test (generate-term lang (cross e) 3 0
|
||||
(decisions #:nt (patterns fourth first first second first first first)
|
||||
#:var (list (λ _ 'x) (λ _ 'y))))
|
||||
(term (λ (x) (hole y)))))
|
||||
|
||||
; preferred productions
|
||||
|
||||
|
||||
;; current-error-port-output : (-> (-> any) string)
|
||||
(define (current-error-port-output thunk)
|
||||
(let ([p (open-output-string)])
|
||||
|
|
@ -521,6 +535,52 @@
|
|||
;; OK -- generated from pattern (any ...)
|
||||
(test (check-metafunction-contract i) #t))
|
||||
|
||||
;; check-reduction-relation
|
||||
(let ()
|
||||
(define-language L
|
||||
(e (+ e ...) number)
|
||||
(E (+ number ... E* e ...))
|
||||
(E* hole E*))
|
||||
(define R
|
||||
(reduction-relation
|
||||
L
|
||||
(==> (+ number ...) whatever)
|
||||
(--> (side-condition number (even? (term number))) whatever)
|
||||
with
|
||||
[(--> (in-hole E a) whatever)
|
||||
(==> a b)]))
|
||||
(let ([generated null])
|
||||
(test (begin
|
||||
(check-reduction-relation
|
||||
R (λ (term) (set! generated (cons term generated)))
|
||||
#:decisions (decisions #:seq (list (λ _ 0) (λ _ 0) (λ _ 0))
|
||||
#:num (list (λ _ 1) (λ _ 1) (λ _ 0)))
|
||||
#:attempts 1)
|
||||
generated)
|
||||
(reverse '((+ (+)) 0))))
|
||||
(let ([S (reduction-relation L (--> 1 2 name) (--> 3 4))])
|
||||
(test (check-reduction-relation S (λ (x) #t) #:attempts 1) #t)
|
||||
(test (current-error-port-output
|
||||
(λ () (check-reduction-relation S (λ (x) #f))))
|
||||
"checking name failed after 1 attempts:\n1\n")
|
||||
(test (current-error-port-output
|
||||
(λ () (check-reduction-relation S (curry eq? 1))))
|
||||
"checking unnamed failed after 1 attempts:\n3\n")))
|
||||
|
||||
; check-metafunction
|
||||
(let ()
|
||||
(define-language empty)
|
||||
(define-metafunction empty
|
||||
[(m 1) whatever]
|
||||
[(m 2) whatever])
|
||||
(let ([generated null])
|
||||
(test (begin
|
||||
(check-metafunction m (λ (t) (set! generated (cons t generated))) 1)
|
||||
generated)
|
||||
(reverse '((1) (2)))))
|
||||
(test (current-error-port-output (λ () (check-metafunction m (curry eq? 1))))
|
||||
#rx"checking clause #1 failed after 1 attempt"))
|
||||
|
||||
;; parse/unparse-pattern
|
||||
(let-syntax ([test-match (syntax-rules () [(_ p x) (test (match x [p #t] [_ #f]) #t)])])
|
||||
(define-language lang (x variable))
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@ To do a better job of not generating programs with free variables,
|
|||
"underscore-allowed.ss"
|
||||
"term.ss"
|
||||
"error.ss"
|
||||
"struct.ss"
|
||||
(for-syntax "rewrite-side-conditions.ss")
|
||||
(for-syntax "term-fn.ss")
|
||||
(for-syntax "reduction-semantics.ss")
|
||||
|
|
@ -83,13 +84,16 @@ To do a better job of not generating programs with free variables,
|
|||
(define (pick-string lang-chars lang-lits attempt [random random])
|
||||
(random-string lang-chars lang-lits (random-natural 1/5 random) attempt random))
|
||||
|
||||
(define ((pick-nt pref-prods) nt prods bound-vars attempt)
|
||||
(let* ([binders (filter (λ (x) (not (null? (rhs-var-info x)))) prods)]
|
||||
(define ((pick-nt pref-prods [random random]) name lang bound-vars attempt)
|
||||
(let* ([prods (nt-rhs (nt-by-name lang name))]
|
||||
[binders (filter (λ (x) (not (null? (rhs-var-info x)))) prods)]
|
||||
[do-intro-binder? (and (null? bound-vars)
|
||||
(not (null? binders))
|
||||
(try-to-introduce-binder?))])
|
||||
(cond [do-intro-binder? binders]
|
||||
[(preferred-production? attempt) (list (hash-ref pref-prods nt))]
|
||||
[(and (not (eq? lang sexp))
|
||||
(preferred-production? attempt random))
|
||||
(hash-ref pref-prods name)]
|
||||
[else prods])))
|
||||
|
||||
(define (pick-from-list l [random random]) (list-ref l (random (length l))))
|
||||
|
|
@ -155,7 +159,7 @@ To do a better job of not generating programs with free variables,
|
|||
[zip (λ (l m) (map cons l m))])
|
||||
(map cdr (filter (λ (x) (equal? min-size (car x))) (zip sizes (nt-rhs nt))))))
|
||||
|
||||
(define (generate* lang pat decisions@)
|
||||
(define (generate lang decisions@)
|
||||
(define-values/invoke-unit decisions@
|
||||
(import) (export decisions^))
|
||||
|
||||
|
|
@ -164,19 +168,16 @@ To do a better job of not generating programs with free variables,
|
|||
(define base-table (find-base-cases lang))
|
||||
|
||||
(define (generate-nt name fvt-id bound-vars size attempt in-hole state)
|
||||
(let*-values
|
||||
([(nt) (findf (λ (nt) (eq? name (nt-name nt)))
|
||||
(append (compiled-lang-lang lang)
|
||||
(compiled-lang-cclang lang)))]
|
||||
[(bound-vars) (append (extract-bound-vars fvt-id state) bound-vars)]
|
||||
(let*-values
|
||||
([(bound-vars) (append (extract-bound-vars fvt-id state) bound-vars)]
|
||||
[(term _)
|
||||
(generate/pred
|
||||
name
|
||||
(λ ()
|
||||
(let ([rhs (pick-from-list
|
||||
(if (zero? size)
|
||||
(min-prods nt base-table)
|
||||
((next-non-terminal-decision) name (nt-rhs nt) bound-vars attempt)))])
|
||||
(min-prods (nt-by-name lang name) base-table)
|
||||
((next-non-terminal-decision) name lang bound-vars attempt)))])
|
||||
(((generate-pat bound-vars (max 0 (sub1 size)) attempt) (rhs-pattern rhs) in-hole)
|
||||
(make-state (map fvt-entry (rhs-var-info rhs)) #hash()))))
|
||||
(λ (_ env) (mismatches-satisfied? env)))])
|
||||
|
|
@ -289,7 +290,7 @@ To do a better job of not generating programs with free variables,
|
|||
[`(hide-hole ,pattern) ((recur pattern the-hole) state)]
|
||||
[`any
|
||||
(let*-values ([(lang nt) ((next-any-decision) lang)]
|
||||
[(term _) ((generate* lang nt decisions@) size attempt)])
|
||||
[(term _) (((generate lang decisions@) nt) size attempt)])
|
||||
(values term state))]
|
||||
[(? (is-nt? lang))
|
||||
(generate-nt pat pat bound-vars size attempt in-hole state)]
|
||||
|
|
@ -355,15 +356,17 @@ To do a better job of not generating programs with free variables,
|
|||
(state-fvt state))
|
||||
(state-env state)))
|
||||
|
||||
(λ (size attempt)
|
||||
(let-values ([(term state)
|
||||
(generate/pred
|
||||
(unparse-pattern pat)
|
||||
(λ ()
|
||||
(((generate-pat null size attempt) pat the-hole)
|
||||
(make-state null #hash())))
|
||||
(λ (_ env) (mismatches-satisfied? env)))])
|
||||
(values term (bindings (state-env state))))))
|
||||
(λ (pat)
|
||||
(let ([unparsed (unparse-pattern pat)])
|
||||
(λ (size attempt)
|
||||
(let-values ([(term state)
|
||||
(generate/pred
|
||||
unparsed
|
||||
(λ ()
|
||||
(((generate-pat null size attempt) pat the-hole)
|
||||
(make-state null #hash())))
|
||||
(λ (_ env) (mismatches-satisfied? env)))])
|
||||
(values term (bindings (state-env state))))))))
|
||||
|
||||
;; find-base-cases : compiled-language -> hash-table
|
||||
(define (find-base-cases lang)
|
||||
|
|
@ -446,6 +449,12 @@ To do a better job of not generating programs with free variables,
|
|||
(define (built-in? x)
|
||||
(and (memq x underscore-allowed) #t))
|
||||
|
||||
;; nt-by-name : lang symbol -> nt
|
||||
(define (nt-by-name lang name)
|
||||
(findf (λ (nt) (eq? name (nt-name nt)))
|
||||
(append (compiled-lang-lang lang)
|
||||
(compiled-lang-cclang lang))))
|
||||
|
||||
(define named-nt-rx #rx"^([^_]+)_[^_]*$")
|
||||
(define mismatch-nt-rx #rx"([^_]+)_!_[^_]*$")
|
||||
(define named-ellipsis-rx #rx"^\\.\\.\\._[^_]*$")
|
||||
|
|
@ -591,7 +600,7 @@ To do a better job of not generating programs with free variables,
|
|||
[(struct ellipsis (name sub-pat class vars))
|
||||
(make-ellipsis name (recur sub-pat) (rewrite class)
|
||||
(map (λ (v) (if (class? v) (rewrite v) v)) vars))]
|
||||
[(? list?) (map (λ (p) (recur p)) pat)]
|
||||
[(? list?) (map recur pat)]
|
||||
[_ pat]))))
|
||||
|
||||
;; used in generating the `any' pattern
|
||||
|
|
@ -610,15 +619,16 @@ To do a better job of not generating programs with free variables,
|
|||
(with-syntax ([(name ...) names]
|
||||
[(name/ellipses ...) names/ellipses])
|
||||
(syntax/loc stx
|
||||
(check-property
|
||||
(term-generator lang pat random-decisions)
|
||||
(λ (_ bindings)
|
||||
(with-handlers ([exn:fail? (λ (_) #f)])
|
||||
(term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
|
||||
property)))
|
||||
attempts))))]))
|
||||
(or (check-property
|
||||
(term-generator lang pat random-decisions)
|
||||
(λ (_ bindings)
|
||||
(with-handlers ([exn:fail? (λ (_) #f)])
|
||||
(term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
|
||||
property)))
|
||||
attempts)
|
||||
(void)))))]))
|
||||
|
||||
(define (check-property generate property attempts)
|
||||
(define (check-property generate property attempts [source #f])
|
||||
(let loop ([remaining attempts])
|
||||
(if (zero? remaining)
|
||||
#t
|
||||
|
|
@ -628,23 +638,21 @@ To do a better job of not generating programs with free variables,
|
|||
(if (property term bindings)
|
||||
(loop (sub1 remaining))
|
||||
(begin
|
||||
(fprintf (current-error-port)
|
||||
"failed after ~s attempts:\n"
|
||||
attempt)
|
||||
(pretty-print term (current-error-port)))))))))
|
||||
(when source
|
||||
(fprintf (current-error-port) "checking ~a " source))
|
||||
(fprintf (current-error-port) "failed after ~s attempts:\n" attempt)
|
||||
(pretty-print term (current-error-port))
|
||||
#f)))))))
|
||||
|
||||
(define-syntax generate
|
||||
(define-syntax generate-term
|
||||
(syntax-rules ()
|
||||
[(_ lang pat size attempt)
|
||||
(let-values ([(term _) ((term-generator lang pat random-decisions) size attempt)])
|
||||
[(_ lang pat size attempt decisions)
|
||||
(let-values ([(term _) ((term-generator lang pat decisions) size attempt)])
|
||||
term)]
|
||||
[(_ lang pat size) (generate lang pat size 0)]))
|
||||
|
||||
(define-syntax generate/decisions
|
||||
(syntax-rules ()
|
||||
[(_ lang pat size attempt decisions@)
|
||||
(let-values ([(term _) ((term-generator lang pat decisions@) size attempt)])
|
||||
term)]))
|
||||
[(_ lang pat size attempt)
|
||||
(generate-term lang pat size attempt random-decisions)]
|
||||
[(_ lang pat size)
|
||||
(generate-term lang pat size 1)]))
|
||||
|
||||
(define-syntax (term-generator stx)
|
||||
(syntax-case stx ()
|
||||
|
|
@ -655,10 +663,14 @@ To do a better job of not generating programs with free variables,
|
|||
'generate #t #'pat)])
|
||||
(syntax/loc stx
|
||||
(let ([lang (parse-language lang)])
|
||||
(generate*
|
||||
lang
|
||||
(reassign-classes (parse-pattern `pattern lang 'top-level))
|
||||
(decisions lang)))))]))
|
||||
((generate lang (decisions lang))
|
||||
(reassign-classes (parse-pattern `pattern lang 'top-level))))))]))
|
||||
|
||||
(define-for-syntax (metafunc name stx)
|
||||
(let ([tf (syntax-local-value name (λ () #f))])
|
||||
(if (term-fn? tf)
|
||||
(term-fn-get-id tf)
|
||||
(raise-syntax-error #f "not a metafunction" stx name))))
|
||||
|
||||
(define-syntax (check-metafunction-contract stx)
|
||||
(syntax-case stx ()
|
||||
|
|
@ -666,22 +678,64 @@ To do a better job of not generating programs with free variables,
|
|||
(syntax/loc stx (check-metafunction-contract name random-decisions))]
|
||||
[(_ name decisions)
|
||||
(identifier? #'name)
|
||||
(with-syntax ([m (let ([tf (syntax-local-value #'name (λ () #f))])
|
||||
(if (term-fn? tf)
|
||||
(term-fn-get-id tf)
|
||||
(raise-syntax-error #f "not a metafunction" stx #'name)))])
|
||||
(with-syntax ([m (metafunc #'name stx)])
|
||||
(syntax/loc stx
|
||||
(let ([lang (parse-language (metafunc-proc-lang m))]
|
||||
[dom (metafunc-proc-dom-pat m)])
|
||||
(check-property
|
||||
(generate* lang
|
||||
(reassign-classes (parse-pattern (if dom dom '(any (... ...))) lang 'top-level))
|
||||
(decisions lang))
|
||||
((generate lang (decisions lang))
|
||||
(reassign-classes (parse-pattern (if dom dom '(any (... ...))) lang 'top-level)))
|
||||
(λ (t _)
|
||||
(with-handlers ([exn:fail:redex? (λ (_) #f)])
|
||||
(begin (term (name ,@t)) #t)))
|
||||
default-check-attempts))))]))
|
||||
|
||||
(define (check-property-many lang patterns ids prop decisions attempts)
|
||||
(let* ([lang-gen (generate lang (decisions lang))]
|
||||
[pat-gens (map (λ (pat) (lang-gen (reassign-classes (parse-pattern pat lang 'top-level))))
|
||||
patterns)])
|
||||
(for/and ([pat patterns]
|
||||
[id ids])
|
||||
(check-property
|
||||
(let ([gen (lang-gen (reassign-classes (parse-pattern pat lang 'top-level)))])
|
||||
(λ (size attempt) (gen size attempt)))
|
||||
(λ (term _) (prop term))
|
||||
attempts
|
||||
id))))
|
||||
|
||||
(define-syntax (check-metafunction stx)
|
||||
(syntax-case stx ()
|
||||
[(_ name property)
|
||||
(syntax/loc stx (check-metafunction name property default-check-attempts))]
|
||||
[(_ name property attempts)
|
||||
(syntax/loc stx (check-metafunction name property random-decisions attempts))]
|
||||
[(_ name property decisions attempts)
|
||||
(with-syntax ([m (metafunc #'name stx)])
|
||||
(syntax/loc stx
|
||||
(or (check-property-many
|
||||
(parse-language (metafunc-proc-lang m))
|
||||
(metafunc-proc-lhs-pats m)
|
||||
(build-list (length (metafunc-proc-lhs-pats m))
|
||||
(compose (curry format "clause #~s") add1))
|
||||
property
|
||||
decisions
|
||||
attempts)
|
||||
(void))))]))
|
||||
|
||||
(define (check-reduction-relation
|
||||
relation property
|
||||
#:decisions [decisions random-decisions]
|
||||
#:attempts [attempts default-check-attempts])
|
||||
(or (check-property-many
|
||||
(parse-language (reduction-relation-lang relation))
|
||||
(map rewrite-proc-lhs (reduction-relation-make-procs relation))
|
||||
(map (λ (proc) (or (rewrite-proc-name proc) 'unnamed))
|
||||
(reduction-relation-make-procs relation))
|
||||
property
|
||||
decisions
|
||||
attempts)
|
||||
(void)))
|
||||
|
||||
(define-signature decisions^
|
||||
(next-variable-decision
|
||||
next-number-decision
|
||||
|
|
@ -693,7 +747,7 @@ To do a better job of not generating programs with free variables,
|
|||
(define (random-decisions lang)
|
||||
(define preferred-productions
|
||||
(make-immutable-hasheq
|
||||
(map (λ (nt) (cons (nt-name nt) (pick-from-list (nt-rhs nt))))
|
||||
(map (λ (nt) (cons (nt-name nt) (list (pick-from-list (nt-rhs nt)))))
|
||||
(append (compiled-lang-lang lang)
|
||||
(compiled-lang-cclang lang)))))
|
||||
(unit (import) (export decisions^)
|
||||
|
|
@ -705,12 +759,13 @@ To do a better job of not generating programs with free variables,
|
|||
(define (next-string-decision) pick-string)))
|
||||
|
||||
(provide pick-from-list pick-var min-prods decisions^ pick-sequence-length
|
||||
is-nt? pick-char random-string pick-string check
|
||||
pick-nt unique-chars pick-any sexp generate parse-pattern
|
||||
is-nt? pick-char random-string pick-string check nt-by-name
|
||||
pick-nt unique-chars pick-any sexp generate-term parse-pattern
|
||||
class-reassignments reassign-classes unparse-pattern
|
||||
(struct-out ellipsis) (struct-out mismatch) (struct-out class)
|
||||
(struct-out binder) generate/decisions check-metafunction-contract
|
||||
pick-number parse-language)
|
||||
(struct-out binder) check-metafunction-contract
|
||||
pick-number parse-language check-reduction-relation
|
||||
preferred-production-threshold check-metafunction)
|
||||
|
||||
(provide/contract
|
||||
[find-base-cases (-> compiled-lang? hash?)])
|
||||
|
|
@ -9,7 +9,7 @@
|
|||
build-reduction-relation
|
||||
reduction-relation?
|
||||
empty-reduction-relation
|
||||
make-rewrite-proc rewrite-proc? rewrite-proc-name
|
||||
make-rewrite-proc rewrite-proc? rewrite-proc-name rewrite-proc-lhs
|
||||
(struct-out rule-pict))
|
||||
|
||||
(define-struct rule-pict (arrow lhs rhs label side-conditions fresh-vars pattern-binds))
|
||||
|
|
@ -20,13 +20,14 @@
|
|||
;; we want to avoid doing it multiple times, so it is cached in a reduction-relation struct
|
||||
|
||||
|
||||
(define-values (make-rewrite-proc rewrite-proc? rewrite-proc-name)
|
||||
(define-values (make-rewrite-proc rewrite-proc? rewrite-proc-name rewrite-proc-lhs)
|
||||
(let ()
|
||||
(define-values (type constructor predicate accessor mutator)
|
||||
(make-struct-type 'rewrite-proc #f 2 0 #f '() #f 0))
|
||||
(make-struct-type 'rewrite-proc #f 3 0 #f '() #f 0))
|
||||
(values constructor
|
||||
predicate
|
||||
(make-struct-field-accessor accessor 1 'name))))
|
||||
(make-struct-field-accessor accessor 1 'name)
|
||||
(make-struct-field-accessor accessor 2 'lhs))))
|
||||
|
||||
;; lang : compiled-language
|
||||
;; make-procs = (listof (compiled-lang -> proc))
|
||||
|
|
|
|||
|
|
@ -1,6 +1,9 @@
|
|||
(module tl-test mzscheme
|
||||
(require "../reduction-semantics.ss"
|
||||
"test-util.ss")
|
||||
"test-util.ss"
|
||||
(only "matcher.ss" make-bindings make-bind)
|
||||
scheme/match
|
||||
"struct.ss")
|
||||
|
||||
(reset-count)
|
||||
|
||||
|
|
@ -537,6 +540,19 @@
|
|||
(list '((2 3) 20)
|
||||
'(6 (4 5))))
|
||||
|
||||
; shortcuts like this fail if compilation fails to preserve
|
||||
; lexical context for side-conditions expressions.
|
||||
(test (let ([x #t])
|
||||
(apply-reduction-relation
|
||||
(reduction-relation
|
||||
grammar
|
||||
(==> variable variable)
|
||||
with
|
||||
[(--> (a (side-condition number x)) b)
|
||||
(==> a b)])
|
||||
'(x 4)))
|
||||
'(x))
|
||||
|
||||
(test (apply-reduction-relation/tag-with-names
|
||||
(reduction-relation
|
||||
grammar
|
||||
|
|
@ -1099,4 +1115,48 @@
|
|||
'x)
|
||||
'(x1))
|
||||
|
||||
(let ([r (reduction-relation
|
||||
grammar
|
||||
(->1 1 2)
|
||||
(->2 3 4)
|
||||
(->4 5 6)
|
||||
with
|
||||
[(--> (side-condition (a number) (even? (term number))) b)
|
||||
(->1 a b)]
|
||||
[(--> (X
|
||||
(number number)
|
||||
(X_1 X_1)
|
||||
(M_!_1 M_!_1)
|
||||
(1 ..._1 1 ..._1)
|
||||
(1 ..._!_1 1 ..._!_1))
|
||||
b)
|
||||
(->2 X b)]
|
||||
[(--> (a 1) b)
|
||||
(->3 a b)]
|
||||
[(->3 (a 2) b)
|
||||
(->4 a b)])])
|
||||
|
||||
; test that names are properly bound for side-conditions in shortcuts
|
||||
(let* ([lhs (rewrite-proc-lhs (first (reduction-relation-make-procs r)))]
|
||||
[proc (third lhs)]
|
||||
[name (cadadr lhs)]
|
||||
[bind (λ (n) (make-bindings (list (make-bind name n))))])
|
||||
(test (and (proc (bind 4)) (not (proc (bind 3)))) #t))
|
||||
|
||||
; test binder renaming
|
||||
(let ([sym-mtch? (λ (rx) (λ (s) (and (symbol? s) (regexp-match? rx (symbol->string s)))))])
|
||||
(match (rewrite-proc-lhs (second (reduction-relation-make-procs r)))
|
||||
[`(3
|
||||
(,(and n1 (? (sym-mtch? #px"^number_\\d+$"))) ,n1)
|
||||
(,(and n2 (? (sym-mtch? #px"^X_1\\d+$"))) ,n2)
|
||||
(,(and m1 (? (sym-mtch? #px"^M_!_1\\d+$"))) ,m1)
|
||||
(1 ,(and ...1 (? (sym-mtch? #px"^\\.\\.\\._1\\d+$"))) 1 ,...1)
|
||||
(1 ,(and ...!1 (? (sym-mtch? #px"^\\.\\.\\._!_1\\d+$"))) 1 ,...!1))
|
||||
#t]
|
||||
[else #f]))
|
||||
|
||||
; test shortcut in terms of shortcut
|
||||
(test (rewrite-proc-lhs (third (reduction-relation-make-procs r)))
|
||||
'((5 2) 1)))
|
||||
|
||||
(print-tests-passed 'tl-test.ss))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user