add stub for enumeration support to Redex

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)

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)))

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)

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)
+(provide (struct-out compiled-lang)
-         (struct-out rhs)
-         (struct-out compiled-lang)
          compiled-lang-cclang
          
          lookup-binding

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 '())))

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

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"

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 
+                term is generated randomly and matches the given pattern (interpreted 
-                according to the definition of the given language).}
+                according to the definition of the given language). The 
-           @item{In the second case,
+                @racket[size-or-index-expr] is treated as a size bound
-                 the expression produced is the quoted form of a use of the judgment-form or
+                on the generated term, as it is for all of the cases when
-                 @racket[#f], if Redex cannot find one.}
+                @racket[generate-term] generates a random term.}
-           @item{The third cases generates a random term that satsifies 
+           @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.
 

collects/redex/tests/gen-test.rkt

@@ -772,3 +772,10 @@
     #:satisfying
     (not-mem b (a (b (c ()))))
     +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)))
+