From 2cf652eccf03c64e46d5a454c27a31f278e73dc7 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Wed, 26 Mar 2014 23:51:15 -0500 Subject: [PATCH] fix handling of un-enumerable patterns to avoid signalling erros in redex-check (we just bail out to the ad hoc random generator if we can't enumerate) --- .../redex-lib/redex/private/enum.rkt | 31 ++++--- .../redex-lib/redex/private/generate-term.rkt | 10 +-- .../redex/private/preprocess-lang.rkt | 86 ++++++++++++++++++- .../redex-test/redex/tests/rg-test.rkt | 12 +++ 4 files changed, 116 insertions(+), 23 deletions(-) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt index c58ee7abef..be8c91e9a8 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt @@ -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) - (map/e - to-term - (λ (_) - (redex-error 'pat-enum "Enumerator is not a bijection")) - (pat/e pat l-enum))) + (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))] + [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)) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt index 85baf6b52c..db255b1ca2 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt @@ -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) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-lang.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-lang.rkt index 6b098c2214..ff4f0b2531 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-lang.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-lang.rkt @@ -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]))) diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt index 82a47cc827..088e05410d 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt @@ -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