From c9045abf4d7af6dbf664edbb8e18da7814f9f198 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Wed, 1 May 2013 09:37:28 -0500 Subject: [PATCH] add stub for enumeration support to Redex --- collects/redex/private/enum.rkt | 21 +++++++++++++++ collects/redex/private/generate-term.rkt | 25 ++++++++++++++++-- collects/redex/private/lang-struct.rkt | 11 ++++++++ collects/redex/private/matcher.rkt | 24 +++++++---------- collects/redex/private/pat-unify.rkt | 5 +++- .../redex/private/reduction-semantics.rkt | 1 + collects/redex/private/rg.rkt | 1 + collects/redex/scribblings/ref.scrbl | 26 ++++++++++++------- collects/redex/tests/gen-test.rkt | 9 ++++++- 9 files changed, 96 insertions(+), 27 deletions(-) create mode 100644 collects/redex/private/enum.rkt create mode 100644 collects/redex/private/lang-struct.rkt diff --git a/collects/redex/private/enum.rkt b/collects/redex/private/enum.rkt new file mode 100644 index 0000000000..709b15cdc6 --- /dev/null +++ b/collects/redex/private/enum.rkt @@ -0,0 +1,21 @@ +#lang racket/base +(require racket/contract + "lang-struct.rkt") + +(provide + (contract-out + [lang-enumerators (-> (listof nt?) (hash/c symbol? enum?))] + [pat-enumerator (-> (hash/c symbol? enum?) + any/c ;; pattern + enum?)] + [enum-ith (-> enum? exact-nonnegative-integer? any/c)] + [enum? (-> any/c boolean?)])) + +(struct enum ()) + +(define (lang-enumerators nts) (make-hash)) +(define (pat-enumerator li p) + (unless (equal? p '(name natural natural)) + (error 'enum.rkt "not yet implemented")) + (enum)) +(define (enum-ith e i) i) diff --git a/collects/redex/private/generate-term.rkt b/collects/redex/private/generate-term.rkt index 96fd940aad..f7959a3a36 100644 --- a/collects/redex/private/generate-term.rkt +++ b/collects/redex/private/generate-term.rkt @@ -2,6 +2,7 @@ (require "rg.rkt" "jdg-gen.rkt" "error.rkt" + "enum.rkt" "reduction-semantics.rkt" "struct.rkt" "term.rkt" @@ -326,9 +327,20 @@ (for ([x (in-list l)]) (define k (syntax-e x)) (when (keyword? k) - (unless (member k '(#:satisfying #:source #:attempt-num #:retries)) + (unless (member k '(#:satisfying #:source #:attempt-num #:retries #:i-th)) (raise-syntax-error 'generate-term "unknown keyword" stx x)))))) + (define form-name (syntax-e #'orig-name)) (syntax-case stx () + [(_ orig-name lang pat #:i-th . rest) + (with-syntax ([(pattern (vars ...) (vars/ellipses ...)) + (rewrite-side-conditions/check-errs + (language-id-nts #'lang form-name) + form-name #t #'pat)]) + (syntax-case #'rest () + [() + #'(generate-ith/proc lang `pattern)] + [(i-expr) + #'((generate-ith/proc lang `pattern) i-expr)]))] [(_ orig-name language #:satisfying (jf/mf-id . args) . rest) (cond [(metafunc #'jf/mf-id) @@ -379,7 +391,6 @@ #'jf/mf-id)])] [(_ orig-name actual-stx ...) (let () - (define form-name (syntax-e #'orig-name)) (define-values (raw-generators args) (syntax-case #'(actual-stx ...) () [(#:source src . rest) @@ -416,6 +427,16 @@ (quasisyntax/loc stx (#,generator-syntax size . kw-args))]))])) +(define (generate-ith/proc lang pat) + (define enum-lang (compiled-lang-enum-table lang)) + (define enum (pat-enumerator enum-lang pat)) + (λ (i) + (unless (exact-nonnegative-integer? i) + (raise-argument-error 'generate-term + "exact-nonnegative-integer?" + i)) + (enum-ith enum i))) + (define (check-cases name cases) (when (null? cases) (raise-gen-fail 'generate-term (format "from ~a metafunction (it has no clauses)" name) 1))) diff --git a/collects/redex/private/lang-struct.rkt b/collects/redex/private/lang-struct.rkt new file mode 100644 index 0000000000..c7d034495e --- /dev/null +++ b/collects/redex/private/lang-struct.rkt @@ -0,0 +1,11 @@ +#lang racket/base + +(provide (struct-out nt) + (struct-out rhs)) + +;; lang = (listof nt) +;; nt = (make-nt sym (listof rhs)) +;; rhs = (make-rhs single-pattern) +;; single-pattern = sexp +(define-struct nt (name rhs) #:transparent) +(define-struct rhs (pattern) #:transparent) diff --git a/collects/redex/private/matcher.rkt b/collects/redex/private/matcher.rkt index 808d23252a..7b57ceba89 100644 --- a/collects/redex/private/matcher.rkt +++ b/collects/redex/private/matcher.rkt @@ -47,19 +47,14 @@ See match-a-pattern.rkt for more details racket/performance-hint (for-syntax racket/base) "underscore-allowed.rkt" - "match-a-pattern.rkt") + "match-a-pattern.rkt" + "lang-struct.rkt" + "enum.rkt") (define-struct compiled-pattern (cp binds-names? skip-dup-check?) #:transparent) (define caching-enabled? (make-parameter #t)) -;; lang = (listof nt) -;; nt = (make-nt sym (listof rhs)) -;; rhs = (make-rhs single-pattern) -;; single-pattern = sexp -(define-struct nt (name rhs) #:transparent) -(define-struct rhs (pattern) #:transparent) - ;; var = (make-var sym sexp) ;; patterns are sexps with `var's embedded ;; in them. It means to match the @@ -117,12 +112,14 @@ See match-a-pattern.rkt for more details ;; hash[sexp[pattern] -o> (cons compiled-pattern boolean)] ;; pict-builder ;; (listof symbol) -;; (listof (listof symbol))) -- keeps track of `primary' non-terminals +;; (listof (listof symbol)) -- keeps track of `primary' non-terminals ;; hash[sym -o> pattern] +;; (hash/c symbol? enum?)) ;; see enum.rkt (define-struct compiled-lang (lang delayed-cclang ht list-ht raw-across-ht raw-across-list-ht has-hole-or-hide-hole-ht cache bind-names-cache pict-builder - literals nt-map collapsible-nts)) + literals nt-map collapsible-nts + enum-table)) (define (compiled-lang-cclang x) (force (compiled-lang-delayed-cclang x))) (define (compiled-lang-across-ht x) (compiled-lang-cclang x) ;; ensure this is computed @@ -164,7 +161,8 @@ See match-a-pattern.rkt for more details pict-info literals nt-map - collapsible-nts)] + collapsible-nts + (lang-enumerators lang))] [non-list-nt-table (build-non-list-nt-label lang)] [list-nt-table (build-list-nt-label lang)] [do-compilation @@ -2034,9 +2032,7 @@ See match-a-pattern.rkt for more details (struct-out mismatch-bind) (struct-out compiled-pattern)) -(provide (struct-out nt) - (struct-out rhs) - (struct-out compiled-lang) +(provide (struct-out compiled-lang) compiled-lang-cclang lookup-binding diff --git a/collects/redex/private/pat-unify.rkt b/collects/redex/private/pat-unify.rkt index 5452b4d16d..2f1c793a9d 100644 --- a/collects/redex/private/pat-unify.rkt +++ b/collects/redex/private/pat-unify.rkt @@ -6,7 +6,9 @@ racket/match "match-a-pattern.rkt" "matcher.rkt" + "lang-struct.rkt" "extract-conditions.rkt" + "enum.rkt" (for-syntax "rewrite-side-conditions.rkt" racket/base)) @@ -754,4 +756,5 @@ (define empty-lang (compiled-lang - #f #f #f #f #f #f #f #f #f #f '() #f (hash))) + #f #f #f #f #f #f #f #f #f #f '() #f (hash) + (lang-enumerators '()))) diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index a1cfe033d6..735975815a 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -9,6 +9,7 @@ "judgment-form.rkt" "term-fn.rkt" "search.rkt" + "lang-struct.rkt" (for-syntax "cycle-check.rkt" setup/path-to-relative) racket/trace diff --git a/collects/redex/private/rg.rkt b/collects/redex/private/rg.rkt index a08bee358c..3b68c58608 100644 --- a/collects/redex/private/rg.rkt +++ b/collects/redex/private/rg.rkt @@ -1,6 +1,7 @@ #lang racket/base (require "matcher.rkt" + "lang-struct.rkt" "reduction-semantics.rkt" "underscore-allowed.rkt" "error.rkt" diff --git a/collects/redex/scribblings/ref.scrbl b/collects/redex/scribblings/ref.scrbl index cc3bfe59a1..038a97fc16 100644 --- a/collects/redex/scribblings/ref.scrbl +++ b/collects/redex/scribblings/ref.scrbl @@ -1693,9 +1693,10 @@ metafunctions or unnamed reduction-relation cases) to application counts.} (values (covered-cases equals-coverage) (covered-cases plus-coverage))))] -@defform*/subs[[(generate-term term-spec size-expr kw-args ...) +@defform*/subs[[(generate-term term-spec size-or-index-expr kw-args ...) (generate-term term-spec)] ([term-spec (code:line language @#,ttpattern) + (code:line language @#,ttpattern #:i-th) (code:line language #:satisfying (judgment-form-id @#,ttpattern ...)) (code:line language #:satisfying (metafunction-id @#,ttpattern ...) = @#,ttpattern) (code:line #:source metafunction) @@ -1706,15 +1707,22 @@ metafunctions or unnamed reduction-relation cases) to application counts.} [attempt-num-expr natural-number/c] [retries-expr natural-number/c])]{ -In its first form, @racket[generate-term] produces a random term according +In its first form, @racket[generate-term] produces a term according to @racket[term-spec]: @itemlist[@item{In the first @racket[term-spec] case, the produced - term matches the given pattern (interpreted - according to the definition of the given language).} - @item{In the second case, - the expression produced is the quoted form of a use of the judgment-form or - @racket[#f], if Redex cannot find one.} - @item{The third cases generates a random term that satsifies + term is generated randomly and matches the given pattern (interpreted + according to the definition of the given language). The + @racket[size-or-index-expr] is treated as a size bound + on the generated term, as it is for all of the cases when + @racket[generate-term] generates a random term.} + @item{In the second case, the produced + term is selected from an enumeration of terms matching the given pattern + (also interpreted according to the definition of the given language), using + the value of @racket[size-or-index-expr] to choose which element of the + enumeration.} + @item{In the third case, the term generated is a random instance of the quoted + form of a use of the judgment-form or @racket[#f], if Redex cannot find one.} + @item{The fourth case generates a random term that satisfies the call to the metafunction with the given result or @racket[#f], if Redex cannot find one.} @item{In the last two cases, @@ -1723,7 +1731,7 @@ to @racket[term-spec]: In @racket[generate-term]'s second form, it produces a procedure for constructing terms according to @racket[term-spec]. -This procedure expects @racket[size-expr] (below) as its sole positional +This procedure expects @racket[size-or-index-expr] (below) as its sole positional argument and allows the same optional keyword arguments as the first form. The second form may be more efficient when generating many terms. diff --git a/collects/redex/tests/gen-test.rkt b/collects/redex/tests/gen-test.rkt index 9005df37d3..6dfb5e8ea8 100644 --- a/collects/redex/tests/gen-test.rkt +++ b/collects/redex/tests/gen-test.rkt @@ -771,4 +771,11 @@ L0 #:satisfying (not-mem b (a (b (c ())))) - +inf.0))) \ No newline at end of file + +inf.0))) + +(let () + (test (generate-term L0 natural #:i-th 0) 0) + (let ([gen-ith (generate-term L0 natural #:i-th)]) + (test (gen-ith 0) 0) + (test (gen-ith 1) 1))) +