suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix handling of un-enumerable patterns to avoid

Browse Source 
signalling erros in redex-check (we just bail
out to the ad hoc random generator if we can't
enumerate)
This commit is contained in:
Robby Findler 2014-03-26 23:51:15 -05:00
parent c9aba4de94
commit 2cf652eccf
4 changed files with 116 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt
View File

@ -21,14 +21,14 @@
[lang-enumerators (-> (listof nt?) (promise/c (listof nt?)) lang-enum?)]
[pat-enumerator (-> lang-enum?
any/c ;; pattern
enum?)]
(or/c #f enum?))]
[enum-ith (-> enum? exact-nonnegative-integer? any/c)]
[enum-size (-> enum? (or/c +inf.0 exact-nonnegative-integer?))]
[lang-enum? (-> any/c boolean?)]
[enum? (-> any/c boolean?)]))
;; nt-enums : hash[sym -o> enum]
;; cc-enums : promise/c (hash[sym -o> enum])
;; nt-enums : hash[sym -o> (or/c #f enum)]
;; cc-enums : promise/c (hash[sym -o> (or/c #f enum)])
;; unused-var/e : enum
(struct lang-enum (nt-enums delayed-cc-enums unused-var/e))
(struct production (n term) #:transparent)
@ -49,14 +49,14 @@
(define (lang-enumerators lang cc-lang)
(define (make-lang-table! ht lang)
(define-values (fin-lang rec-lang cant-enumerate-table) (sep-lang lang))
(define (enumerate-lang! cur-lang enum-f)
(for ([nt (in-list cur-lang)])
(hash-set! ht
(nt-name nt)
(with-handlers ([exn:fail:redex? fail/e])
(enum-f (nt-rhs nt)
nt-enums)))))
(define-values (fin-lang rec-lang) (sep-lang lang))
(if (hash-ref cant-enumerate-table (nt-name nt))
#f
(enum-f (nt-rhs nt) nt-enums)))))
(enumerate-lang! fin-lang
(λ (rhs enums)
(enumerate-rhss rhs l-enum)))
@ -82,11 +82,14 @@
(struct-copy lang-enum l-enum [delayed-cc-enums filled-cc-enums]))
(define (pat-enumerator l-enum pat)
(cond
[(can-enumerate? pat (lang-enum-nt-enums l-enum) (lang-enum-delayed-cc-enums l-enum))
(map/e
to-term
(λ (_)
(redex-error 'pat-enum "Enumerator is not a bijection"))
(pat/e pat l-enum)))
(pat/e pat l-enum))]
[else #f]))
(define (enumerate-rhss rhss l-enum)
(define (with-index i e)
@ -284,10 +287,10 @@
(for/list ([f (in-list fs)])
(f x))))
;; lang-enum-get-nt-enum : lang-enum Symbol -> Enum
;; lang-enum-get-nt-enum : lang-enum Symbol -> (or/c Enum #f)
(define (lang-enum-get-nt-enum l-enum s)
(hash-ref (lang-enum-nt-enums l-enum) s))
;; lang-enum-get-cross-enum : lang-enum Symbol -> Enum
;; lang-enum-get-cross-enum : lang-enum Symbol -> (or/c Enum #f)
(define (lang-enum-get-cross-enum l-enum s)
(hash-ref (force (lang-enum-delayed-cc-enums l-enum)) s))

10
pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt
View File

@ -306,12 +306,7 @@
(define (default-generator lang pat)
(define ad-hoc-generator ((compile lang 'redex-check) pat))
(define enum (with-handlers ([exn:fail? (λ (x) #f)])
;; would be better if the pat-enumerator were to
;; return something to indicate failure instead of
;; raising an exception so that bugs in there wouldn't
;; turn into #f here
(pat-enumerator (compiled-lang-enum-table lang) pat)))
(define enum (pat-enumerator (compiled-lang-enum-table lang) pat))
(cond
[enum
(define in-bounds (if (= +inf.0 (enum-size enum))
@ -349,6 +344,7 @@
(define (ith-generator lang pat enum-bound enum-p-value)
(define enum-lang (compiled-lang-enum-table lang))
(define enum (pat-enumerator enum-lang pat))
(unless enum (error 'redex-check "cannot enumerate the pattern ~s" pat))
(define the-size (enum-size enum))
(cond
[enum-bound
@ -372,6 +368,7 @@
(define (in-order-generator lang pat)
(define enum-lang (compiled-lang-enum-table lang))
(define enum (pat-enumerator enum-lang pat))
(unless enum (error 'redex-check "cannot enumerate the pattern ~s" pat))
(define the-size (enum-size enum))
(λ (_size _attempt _retries)
(values (enum-ith enum (if (= +inf.0 the-size)
@ -698,6 +695,7 @@
(define (generate-ith/proc lang pat)
(define enum-lang (compiled-lang-enum-table lang))
(define enum (pat-enumerator enum-lang pat))
(unless enum (error 'generate-term "cannot enumerate ~s" pat))
(define the-size (enum-size enum))
(λ (i)
(unless (exact-nonnegative-integer? i)

86
pkgs/redex-pkgs/redex-lib/redex/private/preprocess-lang.rkt
View File

@ -7,6 +7,7 @@
racket/math
racket/match
racket/set
racket/promise
"build-nt-property.rkt"
"lang-struct.rkt"
"match-a-pattern.rkt")
@ -15,9 +16,14 @@
(contract-out
[sep-lang (-> (listof nt?)
(values (listof nt?)
(listof nt?)))]
(listof nt?)
(hash/c symbol? boolean?)))]
[used-vars (-> (listof nt?)
(listof symbol?))]))
(listof symbol?))]
[can-enumerate? (-> any/c
(hash/c symbol? any/c)
(promise/c (hash/c symbol? any/c))
boolean?)]))
;; sep-lang : lang -> lang lang
;; topologically sorts non-terminals by dependency
@ -42,8 +48,10 @@
(define sorted-right
(sort-productions cyclic
cyclic-nts))
(values sorted-left
sorted-right))
sorted-right
(build-cant-enumerate-table lang edges)))
;; find-edges : lang -> (hash[symbol] -o> (setof (listof symbol)))
(define (find-edges lang)
@ -324,3 +332,75 @@
(my-max current-max
(let () . defs+exprs))))]))
(define (build-cant-enumerate-table lang edges)
;; cant-enumerate-table : hash[sym[nt] -o> boolean]
(define cant-enumerate-table (make-hash))
;; fill in base cases
(for ([nt (in-list lang)])
(define name (nt-name nt))
(unless (for/and ([rhs (in-list (nt-rhs nt))])
(can-enumerate? (rhs-pattern rhs) #f #f))
(hash-set! cant-enumerate-table name #t)))
;; short-circuiting graph traversal
(define visited (make-hash))
(define (cant-enumerate-nt/fill-table nt-sym)
(hash-ref
cant-enumerate-table
nt-sym
(λ ()
(define ans
(cond
[(hash-ref visited nt-sym #f) #f]
[else
(hash-set! visited nt-sym #t)
;; the '() in the next line is supicious; take it out and see tests fail
;; that probably should be fixed not by putting it back....
(for/or ([next (in-set (hash-ref edges nt-sym '()))])
(cant-enumerate-nt/fill-table next))]))
(hash-set! cant-enumerate-table nt-sym ans)
ans)))
;; fill in the entire table
(for ([nt (in-list lang)])
(cant-enumerate-nt/fill-table (nt-name nt)))
cant-enumerate-table)
;; can-enumerate? : any/c hash[sym -o> any[boolean]] (promise hash[sym -o> any[boolean]])
(define (can-enumerate? pat can-enumerate-ht cross-can-enumerate-ht)
(let loop ([pat pat])
(match-a-pattern
pat
[`any #t]
[`number #t]
[`string #t]
[`natural #t]
[`integer #t]
[`real #t]
[`boolean #t]
[`variable #t]
[`(variable-except ,s ...) #t]
[`(variable-prefix ,s) #t]
[`variable-not-otherwise-mentioned #t]
[`hole #t]
[`(nt ,id)
(or (not can-enumerate-ht)
(and (hash-ref can-enumerate-ht id) #t))]
[`(name ,n ,pat) (loop pat)]
[`(mismatch-name ,n ,pat) (loop pat)]
[`(in-hole ,p1 ,p2) (and (loop p1) (loop p2))]
[`(hide-hole ,p) (loop p)]
[`(side-condition ,p ,g ,e) #f]
[`(cross ,id)
(or (not cross-can-enumerate-ht)
(and (hash-ref (force cross-can-enumerate-ht) id)
#t))]
[`(list ,sub-pats ...)
(for/and ([sub-pat (in-list sub-pats)])
(match sub-pat
[`(repeat ,pat ,_ ,_) (loop pat)]
[else (loop sub-pat)]))]
[(? (compose not pair?)) #t])))

12
pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt
View File

@ -922,6 +922,18 @@
checked)
'(4 3 2 1 0)))
(let ()
;; just make sure no errors
;(redex-check (side-condition any #t) cap-x #t #:attempts 10)
(define-language L
(cap-x := (side-condition
variable_1
(regexp-match #rx"^[A-Z]" (symbol->string (term variable_1))))))
;; just make sure no errors
(redex-check L cap-x #t #:attempts 10))
;; check-reduction-relation
(let ()
(define-language L