From 843edcc78d859e860c63755b83564397e5354bdc Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Wed, 15 May 2013 09:42:53 -0500
Subject: [PATCH] Redex enum maintains bijection internally

Also simplified other redex enumeration internals.
---
 collects/redex/private/enum.rkt    | 574 +++++++++++++++++------------
 collects/redex/tests/enum-test.rkt |  20 +-
 2 files changed, 349 insertions(+), 245 deletions(-)

diff --git a/collects/redex/private/enum.rkt b/collects/redex/private/enum.rkt
index 1b568ba79f..fda789d322 100644
--- a/collects/redex/private/enum.rkt
+++ b/collects/redex/private/enum.rkt
@@ -3,172 +3,270 @@
          racket/list
          racket/match
          racket/function
+         racket/set
          "lang-struct.rkt"
          "match-a-pattern.rkt"
          "enumerator.rkt")
 
 (provide 
  (contract-out
-  [lang-enumerators (-> (listof nt?) (hash/c symbol? enum?))]
-  [pat-enumerator (-> (hash/c symbol? enum?)
+  [lang-enumerators (-> (listof nt?) lang-enum?)]
+  [pat-enumerator (-> lang-enum?
                       any/c ;; pattern
                       enum?)]
   [enum-ith (-> enum? exact-nonnegative-integer? any/c)]
+  [lang-enum? (-> any/c boolean?)]
   [enum? (-> any/c boolean?)]))
 
-
-(define (lang-enumerators nts)
-  (let* ([l-enums (make-hash)]
-         [rec-nt-terms (find-recs nts)]
-         [sorted-nts (sort-nt-terms nts rec-nt-terms)])
-    (foldl
-     (λ (nt m)
-        (hash-set
-         m
-         (nt-name nt)
-         (with-handlers
-             ([exn:fail? fail/enum])
-           (rec-pat/enum `(nt ,(nt-name nt))
-                         sorted-nts
-                         rec-nt-terms))))
-     (hash)
-     sorted-nts)))
+(struct lang-enum (enums))
+(struct decomposition (ctx term))
+(struct hole ())
+(struct named (name val))
+(struct named-t (val term))
+(struct name (name) #:transparent)
+(struct unimplemented (msg))
 
 (define enum-ith decode)
-(struct decomposition (ctx term))
 
-(define (pat-enumerator lang-enums pat)
-  (enum-names pat
-              (sep-names pat)
-              lang-enums))
+(define (lang-enumerators lang)
+  (let ([l-enums (make-hash)])
+    (let-values ([(fin-lang rec-lang)
+                  (sep-lang lang)])
+      (for-each
+       (λ (nt)
+          (hash-set! l-enums
+                     (nt-name nt)
+                     (enumerate-rhss (nt-rhs nt)
+                                     l-enums)))
+       fin-lang)
+      (for-each
+       (λ (nt)
+          (hash-set! l-enums
+                     (nt-name nt)
+                     (thunk/enum +inf.f
+                                 (λ ()
+                                    (enumerate-rhss (nt-rhs nt)
+                                                    l-enums)))))
+       rec-lang))
+    (lang-enum l-enums)))
 
-(define (rec-pat/enum pat nts rec-nt-terms)
-  (enum-names pat
-              nts
-              (sep-names pat)
-              rec-nt-terms))
+(define (pat-enumerator l-enum pat)
+  (map/enum
+   to-term
+   (λ (_)
+      (error 'pat-enum "Enumerator is not a  bijection"))
+   (pat/enum pat
+             (lang-enum-enums l-enum))))
 
+(define (enumerate-rhss rhss l-enums)
+  (apply sum/enum
+         (map
+          (λ (rhs)
+             (pat/enum (rhs-pattern rhs)
+                       l-enums))
+          rhss)))
 
-;; find-recs : lang -> (hash symbol -o> (assoclist rhs bool))
-;; Identifies which non-terminals are recursive
-(define (find-recs nt-pats)
-  (define is-rec?
-    (case-lambda
-      [(n) (is-rec? n (hash))]
-      [(nt seen)
-       (or (seen? seen (nt-name nt))
-           (ormap
-            (λ (rhs)
-               (let rec ([pat (rhs-pattern rhs)])
-                 (match-a-pattern
-                  pat
-                  [`any #f]
-                  [`number #f]
-                  [`string #f]
-                  [`natural #f]
-                  [`integer #f]
-                  [`real #f]
-                  [`boolean #f]
-                  [`variable #f]
-                  [`(variable-except ,s ...) #f]
-                  [`(variable-prefix ,s) #f]
-                  [`variable-not-otherwise-mentioned #f]
-                  [`hole #f]
-                  [`(nt ,id)
-                   (is-rec? (make-nt
-                             id
-                             (lookup nt-pats id))
-                            (add-seen seen
-                                      (nt-name nt)))]
-                  [`(name ,name ,pat)
+;; find-edges : lang -> (hash symbol -o> (setof symbol))
+(define (find-edges lang)
+  (foldl
+   (λ (nt m)
+      (hash-set
+       m (nt-name nt)
+       (fold-map/set
+        (λ (rhs)
+           (let loop ([pat (rhs-pattern rhs)]
+                      [s (set)])
+             (match-a-pattern
+              pat
+              [`any s]
+              [`number s]
+              [`string s]
+              [`natural s]
+              [`integer s]
+              [`real s]
+              [`boolean s]
+              [`variable s]
+              [`(variable-except ,v ...) s]
+              [`(variable-prefix ,v) s]
+              [`variable-not-otherwise-mentioned s]
+              [`hole s]
+              [`(nt ,id)
+               (set-add s id)]
+              [`(name ,name ,pat)
+               (loop pat s)]
+              [`(mismatch-name ,name ,pat)
+               (loop pat s)]
+              [`(in-hole ,p1 ,p2)
+               (set-union (loop p1 s)
+                          (loop p2 s))]
+              [`(hide-hole ,p) (loop p s)]
+              [`(side-condition ,p ,g ,e) ;; error
+               (unsupported/enum pat)]
+              [`(cross ,s)
+               (unsupported/enum pat)] ;; error
+              [`(list ,sub-pats ...)
+               (fold-map/set
+                (λ (sub-pat)
+                   (match sub-pat
+                     [`(repeat ,pat ,name ,mismatch)
+                      (loop pat s)]
+                     [else (loop sub-pat s)]))
+                sub-pats)]
+              [(? (compose not pair?)) s])))
+        (nt-rhs nt))))
+   (hash)
+   lang))
+
+;; find-cycles : (hashsymbol -o> (setof symbol)) -> (setof symbol)
+(define (find-cycles edges)
+  (foldl
+   (λ (v s)
+      (if (let rec ([cur v]
+                    [seen (set)])
+            (cond [(set-member? seen cur) #t]
+                  [else
+                   (ormap
+                    (λ (next)
+                       (rec next
+                            (set-add seen cur)))
+                    (set->list (hash-ref edges
+                                         cur)))]))
+          (set-add s v)
+          s))
+   (set)
+   (hash-keys edges)))
+
+;; calls-rec? : pat (setof symbol) -> bool
+(define (calls-rec? pat recs)
+  (let rec ([pat pat])
+    (match-a-pattern
+     pat
+     [`any #f]
+     [`number #f]
+     [`string #f]
+     [`natural #f]
+     [`integer #f]
+     [`real #f]
+     [`boolean #f]
+     [`variable #f]
+     [`(variable-except ,s ...) #f]
+     [`(variable-prefix ,s) #f]
+     [`variable-not-otherwise-mentioned #f]
+     [`hole #f]
+     [`(nt ,id)
+      (set-member? recs id)]
+     [`(name ,name ,pat)
+      (rec pat)]
+     [`(mismatch-name ,name ,pat)
+      (rec pat)]
+     [`(in-hole ,p1 ,p2)
+      (or (rec p1)
+          (rec p2))]
+     [`(hide-hole ,p) (rec p)]
+     [`(side-condition ,p ,g ,e) ;; error
+      (unsupported/enum pat)]
+     [`(cross ,s)
+      (unsupported/enum pat)] ;; error
+     [`(list ,sub-pats ...)
+      (ormap (λ (sub-pat)
+                (match sub-pat
+                  [`(repeat ,pat ,name ,mismatch)
                    (rec pat)]
-                  [`(mismatch-name ,name ,pat)
-                   (rec pat)]
-                  [`(in-hole ,p1 ,p2)
-                   (or (rec p1)
-                       (rec p2))]
-                  [`(hide-hole ,p) (rec p)]
-                  [`(side-condition ,p ,g ,e) ;; error
-                   (unsupported/enum pat)]
-                  [`(cross ,s)
-                   (unsupported/enum pat)] ;; error
-                  [`(list ,sub-pats ...)
-                   (ormap (λ (sub-pat)
-                             (match sub-pat
-                               [`(repeat ,pat ,name ,mismatch)
-                                (rec pat)]
-                               [else (rec sub-pat)]))
-                          sub-pats)]
-                  [(? (compose not pair?)) #f])))
-            (nt-rhs nt)))]))
-  (define (calls-rec? rhs recs)
-    (let rec ([pat (rhs-pattern rhs)])
-      (match-a-pattern
-       pat
-       [`any #f]
-       [`number #f]
-       [`string #f]
-       [`natural #f]
-       [`integer #f]
-       [`real #f]
-       [`boolean #f]
-       [`variable #f]
-       [`(variable-except ,s ...) #f]
-       [`(variable-prefix ,s) #f]
-       [`variable-not-otherwise-mentioned #f]
-       [`hole #f]
-       [`(nt ,id)
-        (hash-ref recs id)]
-       [`(name ,name ,pat)
-        (rec pat)]
-       [`(mismatch-name ,name ,pat)
-        (rec pat)]
-       [`(in-hole ,p1 ,p2)
-        (or (rec p1)
-            (rec p2))]
-       [`(hide-hole ,p) (rec p)]
-       [`(side-condition ,p ,g ,e) ;; error
-        (rec p)]
-       [`(cross ,s)
-        (unsupported/enum pat)] ;; error
-       [`(list ,sub-pats ...)
-        (ormap (λ (sub-pat)
-                  (match sub-pat
-                    [`(repeat ,pat ,name ,mismatch)
-                     (rec pat)]
-                    [else (rec sub-pat)]))
-               sub-pats)]
-       [(? (compose not pair?)) #f])))
-  (define (seen? m s)
-    (hash-ref m s #f))
-  (define (add-seen m s)
-    (hash-set m s #t))
-  (let ([recs
-         (foldl
-          (λ (nt m)
-             (hash-set m (nt-name nt) (is-rec? nt)))
-          (hash) nt-pats)])
+                  [else (rec sub-pat)]))
+             sub-pats)]
+     [(? (compose not pair?)) #f])))
+
+;; fold-map : (a -> setof b) (listof a) -> (setof b)
+(define (fold-map/set f l)
+  (foldl
+   (λ (x s)
+      (set-union (f x) s))
+   (set)
+   l))
+
+;; sep-lang : lang -> lang lang
+;; topologically sorts non-terminals by dependency
+;; sorts rhs's so that recursive ones go last
+(define (sep-lang lang)
+  (define (filter-edges edges lang)
     (foldl
      (λ (nt m)
-        (let ([rhs (nt-rhs nt)])
-          (hash-set m (nt-name nt)
-                    (map (λ (rhs)
-                            (cons rhs (calls-rec? rhs recs)))
-                         rhs))))
+        (let ([name (nt-name nt)])
+          (hash-set m name
+                    (hash-ref edges name))))
      (hash)
-     nt-pats)))
+     lang))
+  (let* ([edges (find-edges lang)]
+         [cyclic-nts (find-cycles edges)])
+    (let-values ([(cyclic non-cyclic)
+                  (partition (λ (nt)
+                                (set-member? cyclic-nts (nt-name nt)))
+                             lang)])
+      (let ([sorted-left (topo-sort non-cyclic
+                                    (filter-edges edges non-cyclic))] ;; topological sort
+            [sorted-right (sort-nt-terms cyclic
+                                         cyclic-nts)] ;; rhs sort
+            )
+        (values sorted-left
+                sorted-right)))))
 
-;; sort-nt-terms : lang (hash symbol -o> (assoclist rhs bool)) -> lang
-(define (sort-nt-terms nt-pats recs)
-  (map
-   (λ (nt)
-      (let ([rec-nts (hash-ref recs (nt-name nt))])
-        (make-nt (nt-name nt)
-                 (sort (nt-rhs nt)
-                       (λ (r1 r2)
-                          (and (not (cdr (assoc r1 rec-nts)))
-                               (cdr (assoc r2 rec-nts))))))))
-   nt-pats))
+;; recursive-rhss : lang (hash symbol -o> (setof symbol)) -> (hash symbol -o> (assoclist rhs bool))
+(define (recursive-rhss lang recs)
+  (foldl
+   (λ (nt m)
+      (let ([rhs (nt-rhs nt)])
+        (hash-set m (nt-name nt)
+                  (map (λ (rhs)
+                          (cons rhs
+                                (calls-rec? (rhs-pattern rhs)
+                                            recs)))
+                       rhs))))
+   (hash)
+   lang))
+
+;; topo-sort : lang (hash symbol -o> (setof symbol)) -> lang
+(define (topo-sort lang edges)
+  (define (find-top rem edges)
+    (let find ([rem rem])
+      (let ([v (car rem)])
+        (let check ([vs (hash-keys edges)])
+          (cond [(empty? vs) v]
+                [(set-member? (hash-ref edges (car vs))
+                              v)
+                 (find (cdr rem))]
+                [else (check (cdr vs))])))))
+  (let loop ([rem (hash-keys edges)]
+             [edges edges]
+             [out-lang '()])
+    (cond [(empty? rem) out-lang]
+          [else
+           (let ([v (find-top rem edges)])
+             (loop (remove v rem)
+                   (hash-remove edges v)
+                   (cons
+                    (findf
+                     (λ (nt)
+                        (eq? v (nt-name nt)))
+                     lang)
+                    out-lang)))])))
+
+;; sort-nt-terms : lang (setof symbol) -> lang
+(define (sort-nt-terms lang nts)
+  (let ([recs (recursive-rhss lang nts)])
+    (map
+     (λ (nt)
+        (let ([rec-nts (hash-ref recs (nt-name nt))])
+          (make-nt (nt-name nt)
+                   (sort (nt-rhs nt)
+                         (λ (r1 r2)
+                            (and (not (cdr (assoc r1 rec-nts)))
+                                 (cdr (assoc r2 rec-nts))))))))
+     lang)))
+
+(define (pat/enum pat l-enums)
+  (enum-names pat
+              (sep-names pat)
+              l-enums))
 
 ;; sep-names : single-pattern lang -> (assoclist symbol pattern)
 (define (sep-names pat)
@@ -194,8 +292,7 @@
       (loop pat
             (add-if-new name pat named-pats))]
      [`(mismatch-name ,name ,pat)
-      (loop pat
-            (add-if-new name pat named-pats))]
+      (loop pat (cons (unimplemented "mismatch") named-pats))]
      [`(in-hole ,p1 ,p2)
       (loop p2
             (loop p1 named-pats))]
@@ -207,18 +304,12 @@
      [`(list ,sub-pats ...)
       (foldl (λ (sub-pat named-pats)
                 (match sub-pat
-                  ;; unnamed repeat
                   [`(repeat ,pat #f #f)
                    (loop pat named-pats)]
-                  ;; named repeat 
                   [`(repeat ,pat ,name #f)
-                   (loop pat
-                         (add-if-new name 'name-r named-pats))]
-                  ;; mismatch named repeat
+                   (loop pat (cons (unimplemented "named repeat") named-pats))]
                   [`(repeat ,pat #f ,mismatch)
-                   (loop pat
-                         (add-if-new mismatch 'mismatch-r named-pats))]
-                  ;; normal subpattern
+                   (loop pat (cons (unimplemented "mismatch repeat") named-pats))]
                   [else (loop sub-pat named-pats)]))
              named-pats
              sub-pats)]
@@ -226,82 +317,54 @@
       named-pats])))
 
 (define (add-if-new k v l)
-  (cond [(assoc k l) l]
-        [else (cons `(,k ,v) l)]))
+  (cond [(assoc-named k l) l]
+        [else (cons (named k v) l)]))
 
-(define enum-names
-  (case-lambda
-    [(pat named-pats nts)
-     (enum-names-with
-      (λ (pat named)
-         (pat/enum-with-names pat nts named))
-      pat named-pats)]
-    [(pat nts named-pats rec-nt-terms)
-     (enum-names-with
-      (λ (pat named)
-         (pat/enum-with-names pat nts named rec-nt-terms))
-      pat named-pats)]))
+(define (assoc-named n l)
+  (cond [(null? l) #f]
+        [else
+         (or (let ([cur (car l)])
+               (and (named? cur)
+                    (equal? (named-name cur)
+                            n)))
+             (assoc-named n (cdr l)))]))
 
-(define (enum-names-with f pat named-pats)
+(define (enum-names pat named-pats nt-enums)
   (let rec ([named-pats named-pats]
             [env (hash)])
-    (cond [(null? named-pats) (f pat env)]
+    (cond [(null? named-pats)
+           (pat/enum-with-names pat nt-enums env)]
           [else
-           (match
-             (car named-pats)
-             ;; named repeat
-             [`(,name name-r)
-              (error/enum 'unimplemented "named-repeat")]
-             ;; mismatch repeat
-             [`(,name mismatch-r)
-              (error/enum 'unimplemented "mismatch-repeat")]
-             [`(,name ,pat mismatch)
-              (error/enum 'unimplemented "mismatch")]
-             ;; named
-             [`(,name ,pat)
-              (map/enum ;; loses bijection
-               cdr
-               (λ (x) (cons name x))
-               (dep/enum
-                (f pat env)
-                (λ (term)
-                   (rec (cdr named-pats)
-                        (hash-set env
-                                  name
-                                  term)))))]
-             [else (error 'bad-assoc)])])))
+           (let ([cur (car named-pats)])
+             (cond ([named? cur]
+                    (let ([name (named-name cur)]
+                          [pat (named-val cur)])
+                      (map/enum
+                       (λ (ts)
+                          (named name
+                                 (named-t (car ts)
+                                          (cdr ts))))
+                       (λ (n)
+                          (if (equal? (named-name n)
+                                      name)
+                              (let ([val (named-val n)])
+                                (cons (named-t-val val)
+                                      (named-t-term val)))
+                              (error 'wrong-name
+                                     "expected ~a, got ~a"
+                                     name
+                                     (named-name n))))
+                       (dep/enum
+                        (pat/enum-with-names pat nt-enums env)
+                        (λ (term)
+                           (rec (cdr named-pats)
+                                (hash-set env
+                                          name
+                                          term)))))))
+                   [else (error/enum 'unimplemented
+                                     (unimplemented-msg cur))]))])))
 
-(define pat/enum-with-names
-  (case-lambda
-    [(pat nt-enums named-terms)
-     (pat/enum-with-names-with
-      pat
-      named-terms
-      (λ (nt)
-         (hash-ref nt-enums nt)))]
-    [(pat nts named-terms rec-nt-terms)
-     (pat/enum-with-names-with
-      pat
-      named-terms
-      (λ (nt)
-         (let ([rhss (lookup nts nt)])
-           (apply sum/enum
-                  (map
-                   (λ (rhs)
-                      (cond [(cdr (assoc rhs (hash-ref rec-nt-terms nt)))
-                             (thunk/enum
-                              +inf.f
-                              (λ ()
-                                 (rec-pat/enum (rhs-pattern rhs)
-                                               nts
-                                               rec-nt-terms)))]
-                            [else
-                             (rec-pat/enum (rhs-pattern rhs)
-                                           nts
-                                           rec-nt-terms)]))
-                   rhss)))))]))
-
-(define (pat/enum-with-names-with pat named-terms f)
+(define (pat/enum-with-names pat nt-enums named-terms)
   (let loop ([pat pat])
     (match-a-pattern
      pat
@@ -326,18 +389,19 @@
      [`hole
       (const/enum 'hole)]
      [`(nt ,id)
-      (f id)]
-     [`(name ,name ,pat)
-      (const/enum (hash-ref named-terms name))]
+      (hash-ref nt-enums id)]
+     [`(name ,n ,pat)
+      (const/enum (name n))]
      [`(mismatch-name ,name ,pat)
       (error/enum 'unimplemented "mismatch-name")]
      [`(in-hole ,p1 ,p2) ;; untested
       (map/enum
-       (λ (t1-t2) ;; loses bijection
-          (plug-hole (car t1-t2)
-                     (cdr t1-t2)))
-       (λ (plugged)
-          (cons 'hole plugged))
+       (λ (ts)
+          (decomposition (car ts)
+                         (cdr ts)))
+       (λ (decomp)
+          (cons (decomposition-ctx decomp)
+                (decomposition-term decomp)))
        (prod/enum
         (loop p1)
         (loop p2)))]
@@ -437,11 +501,43 @@
             bool/enum
             var/enum))
 
+(define (to-term aug)
+  (cond [(named? aug)
+         (rep-name aug)]
+        [else aug]))
+
+(define (rep-name s)
+  (to-term
+   (let* ([n (named-name s)]
+          [v (named-val s)]
+          [val (named-t-val v)]
+          [term (named-t-term v)])
+     (let loop ([term term])
+       (cond [(and (name? term)
+                   (equal? (name-name term) n))
+              val]
+             [(named? term)
+              (map-named loop
+                         term)]
+             [else term])))))
+
+(define (map-named f n)
+  (let ([v (named-val n)])
+   (named (named-name n)
+          (named-t
+           (named-t-val v)
+           (f (named-t-term v))))))
+
+#;
 (define (plug-hole ctx term)
-  (let loop ([ctx ctx])
-    (match
-      ctx
-      ['hole term]
-      [`(,ts ...)
-       (map loop ts)]
-      [x x])))
+  (to-term
+   (let loop ([ctx ctx])
+     (cond [(hole? ctx) term]
+           [(cons? ctx) (map loop ctx)]
+           [(named? )])
+     (match
+       ctx
+       ['hole term]
+       [`(,ts ...)
+        (map loop ts)]
+       [x x]))))
diff --git a/collects/redex/tests/enum-test.rkt b/collects/redex/tests/enum-test.rkt
index d227af70c7..92abc62b91 100644
--- a/collects/redex/tests/enum-test.rkt
+++ b/collects/redex/tests/enum-test.rkt
@@ -7,11 +7,14 @@
   (syntax-case stx ()
     [(_ N l p)
      (with-syntax ([line (syntax-line stx)])
-       #'(for ([i (in-range N)])
-           (unless (redex-match
-                    l p
-                    (generate-term l p #:i-th i))
-             (error 'bad-term "line ~a: i=~a" line i))))]))
+       #'(test-begin
+          (for ([i (in-range N)])
+            (check-not-exn
+             (λ ()
+                (unless (redex-match
+                         l p
+                         (generate-term l p #:i-th i))
+                  (error 'bad-term "line ~a: i=~a" line i)))))))]))
 
 ;; Repeat test
 (define-language Rep
@@ -38,6 +41,11 @@
 (try-it 100 Named n)
 
 (define-language not-SKI
+  (y x
+     s
+     k
+     i)
   (x (variable-except s k i)))
 
-(try-it 21 not-SKI x)
+(try-it 22 not-SKI x)
+(try-it 25 not-SKI y)