Redex: corrections for disequations in generator

- handle parameters correctly when simplifying disequations
- rework term generation/disequation checking for parameters
- fix define-extended-metafunction w/r/t the above

collects/redex/private/jdg-gen.rkt

@@ -1,16 +1,19 @@
 #lang racket/base
 
-(require
+(require racket/match
- (only-in "rg.rkt"
+         racket/set
-          [compile rg:compile])
+         (only-in "rg.rkt"
- (only-in "reduction-semantics.rkt"
+                  [compile rg:compile])
-          do-test-match)
+         (only-in "reduction-semantics.rkt"
- "pat-unify.rkt"
+                  do-test-match)
- (for-syntax racket/base)
+         "pat-unify.rkt"
- racket/match)
+         (for-syntax racket/base))
 
 (provide pat->term
-         check-dq)
+         check-dq
+         dq)
+
+
 
 ;; term generation
 
@@ -72,31 +75,31 @@
 (define (check-dqs dqs term-e lang eqs)
   (for/and ([dq dqs])
     (define te (hash-copy term-e))
-    (define rhs (list-ref dq 0))
+    (check-dq dq te lang eqs)))
-    (define lhs (list-ref dq 1))
-    (check-dq rhs lhs te lang eqs)))
-
-(define sym-index 0)
 
 (struct not-ground ())
 
-(define (check-dq rhs lhs term-e lang eqs)
+(define (check-dq the-dq term-e lang eqs)
-  (set! sym-index 0)
+  (match-define (dq ps `(,lhs ,rhs)) the-dq)
-  (define rhs-term (pat->term/term-e rhs term-e eqs lang))
+  (define rhs-term (pat->term/term-e ps rhs term-e eqs lang))
-  (define lhs-term (pat->term/term-e lhs term-e eqs lang))
+  (define lhs-term (pat->term/term-e ps lhs term-e eqs lang))
-  (not (equal? rhs-term lhs-term)))
+  (not (compare-partial-terms rhs-term lhs-term)))
   
-(define (pat->term/term-e t term-e actual-e lang)
+(define (pat->term/term-e ps t term-e actual-e lang)
   (call/ec
    (λ (fail)
      (let recur ([p t])
        (match p
          [`(name ,var ,(bound))
-          (if (hash-has-key? term-e (lvar var))
+          (cond
-              (recur (hash-ref term-e (lvar var)))
+            [(member var ps)
-              (let ([new-val (recur (hash-ref actual-e (lvar var)))])
+             `(name ,var ,(bound))]
-                (hash-set! term-e (lvar var) new-val)
+            [(hash-has-key? term-e (lvar var))
-                new-val))]
+             (recur (hash-ref term-e (lvar var)))]
+            [else
+             (let ([new-val (recur (hash-ref actual-e (lvar var)))])
+               (hash-set! term-e (lvar var) new-val)
+               new-val)])]
          [`(cstr  (,nts ...) ,pat)
           (recur pat)]
          [`(list ,ps ...)
@@ -108,6 +111,37 @@
          [else
           (let-values ([(p bs) (gen-term p lang 2)])
            p)])))))
+
+(define (compare-partial-terms l r)
+  (define param-vals (hash))
+  (define (update-param-vals p v)
+    (set! param-vals
+          (hash-set param-vals p
+              (set-add (hash-ref param-vals p (λ () (set))) v))))
+  (and
+   (let recur ([l l]
+               [r r])
+     (match* (l r)
+       [(`(name ,lv ,(bound)) `(name ,rv ,(bound)))
+        (update-param-vals lv r)
+        (update-param-vals rv l)
+        #t]
+       [(`(name ,lv ,(bound)) _)
+        (update-param-vals lv r)
+        #t]
+       [(_ `(name ,rv ,(bound)))
+        (update-param-vals rv l)
+        #t]
+       [(`(,l-ts ...) `(,r-ts ...))
+        (and (= (length l-ts) (length r-ts))
+             (for/and ([lt l-ts]
+                       [rt r-ts])
+               (recur lt rt)))]
+       [(_ _)
+        (equal? l r)]))
+   ;; TODO: handle case where param appears twice against different stuff
+   (for/and ([vs (in-list (hash-values param-vals))])
+     ((set-count vs) . < . 2))))
                    
 
 (define (gen-term pat lang size [num-atts 1] [retries 100])
@@ -128,3 +162,4 @@
      (lookup new-id env)]
     [else
      (values (lvar id) res)]))
+

collects/redex/private/judgment-form.rkt

@@ -1382,7 +1382,7 @@
          (if in-judgment-form?
              (let-values ([(term-rws mf-cs) (rewrite-terms (list #'rest) ns)])
                (values (append mf-cs ps-rw)
-                       (cons #`(dqn #f '#,(car term-rws)) eqs)
+                       (cons #`(dqn '() #f '#,(car term-rws)) eqs)
                        ns))
              (values ps-rw eqs ns))]
         [(prem-name . prem-body)

collects/redex/private/pat-unify.rkt

@@ -23,10 +23,10 @@
          pat*-clause-p?s
          bind-names
          remove-empty-dqs
-         unif-fail
+         (struct-out unif-fail)
          dq)
 
-;(require racket/trace)
+
 ;;
 ;; atom := `any | `number | `string | `integer | `boolean | `real | `variable | `variable-not-otherwise-mentioned
 ;; var  := symbol?
@@ -213,16 +213,49 @@
   (filter (λ (dq) (not (equal? base-dq dq)))
           dqs))
 
-(define (extend-dq eqs ineq0)
+(define (extend-dq new-eqs ineq0 eqs)
   (for/fold ([ineq ineq0])
-    ([(k v) (in-hash eqs)])
+    ([(k v) (in-hash new-eqs)])
     (match ineq
       [`((list ,vars ...) (list ,terms ...))
        (match* (k v)
          [((lvar id-l) (lvar id-r))
-          `((list ,@vars (name ,id-l ,(bound))) (list ,@terms (name ,id-r ,(bound))))]
+          `((list ,@vars (name ,id-l ,(bound))) 
+            (list ,@terms ,(resolve-no-nts/var v eqs)))]
          [((lvar id-l) pat*-r)
-          `((list ,@vars (name ,id-l ,(bound))) (list ,@terms ,pat*-r))])])))
+          `((list ,@vars (name ,id-l ,(bound))) 
+            (list ,@terms ,(resolve-no-nts/pat v eqs)))])])))
+
+(define (resolve-no-nts/var lv eqs)
+  (define-values (rep pat) (lookup (lvar-id lv) eqs))
+  (if (not (groundable? pat))
+      `(name ,(lvar-id rep) ,(bound))
+      (resolve-no-nts/pat pat eqs)))
+
+(define (resolve-no-nts/pat pat eqs)
+  (let recur ([p pat])
+        (match p
+          [`(name ,id ,(bound))
+           (resolve-no-nts/var (lvar id) eqs)]
+          [`(list ,ps ...)
+           `(list ,@(for/list ([p ps]) (recur p)))]
+          [`(cstr (,cs ...) p)
+           (recur p)]
+          [else
+           (unless (groundable? p)
+             (error 'resolve/termable-pat 
+                    "non-termable pat at internal pattern position: ~s" p))
+           p])))
+
+
+(define (groundable? p)
+  (match p
+    [`(nt ,_) #f]
+    [(? predef-pat? _) #f]
+    [`(cstr ,_ ,p)
+     (groundable? p)]
+    [else #t]))
+           
                 
 (define (hash/mut->imm h0)
   (for/fold ([h (hash)])
@@ -265,7 +298,7 @@
         [(empty? (hash-keys (new-eqs))) #f]
         [else
          (define-values (new-ps new-dq)
-           (param-elim params (extend-dq (new-eqs) base-dq)))
+           (param-elim params (extend-dq (new-eqs) base-dq eqs)))
          (match new-dq
            [`((list) (list))
             #f]
@@ -641,9 +674,3 @@
     [else
      (values (lvar id) res)]))
 
-
-;(trace disunify*)
-
-
-
-

collects/redex/private/reduction-semantics.rkt

@@ -1300,7 +1300,7 @@
                                      (syntax->list #'(lhs-names ...))
                                      (syntax->list #'(lhs-namess/ellipses ...))
                                      (syntax->list (syntax (rhs/wheres ...))))]
-                               [((gen-clause lhs-pat) ...)
+                               [((gen-clause lhs-pat lhs-ps/pat*) ...)
                                 (make-mf-clauses (syntax->list #'(lhs ...))
                                                  (syntax->list #'(rhs ...))
                                                  (syntax->list #'((stuff ...) ...))
@@ -1322,7 +1322,9 @@
                                 #,(if prev-metafunction
                                       #`(metafunc-proc-cases #,(term-fn-get-id (syntax-local-value prev-metafunction)))
                                       #'null)]
-                               [new-lhs-pats '(lhs-pat ...)])
+                               [new-lhs-pats '(lhs-pat ...)]
+                               [new-lhs-ps/pats '(lhs-ps/pat* ...)])
+                           
                            (build-metafunction 
                             lang
                             cases
@@ -1348,7 +1350,7 @@
                                     #`(extend-mf-clauses #,(term-fn-get-id (syntax-local-value prev-metafunction))
                                                          (λ ()
                                                            #,(check-pats #'(list gen-clause ...)))
-                                                         new-lhs-pats)]
+                                                         new-lhs-ps/pats)]
                                    [else
                                     #`(memoize0
                                        (λ ()
@@ -1367,14 +1369,16 @@
 (define (extend-lhs-pats old-m new-pats)
   (append new-pats (metafunc-proc-lhs-pats old-m)))
 
-(define (extend-mf-clauses old-mf new-clauses new-lhs-pats)
+(define (extend-mf-clauses old-mf new-clauses new-lhs-ps/pats)
   (memoize0
    (λ ()
      (define old-clauses
        (for/list ([old-clauses (in-list ((metafunc-proc-gen-clauses old-mf)))]
                   [old-lhs-pat (in-list (metafunc-proc-lhs-pats old-mf))])
-         (define new-dqs (for/list ([new-lhs-pat (in-list new-lhs-pats)])
+         (define new-dqs (for/list ([new-lhs-ps/pat (in-list new-lhs-ps/pats)])
-                           (dqn old-lhs-pat new-lhs-pat)))
+                           (dqn (first new-lhs-ps/pat)
+                                old-lhs-pat 
+                                (second new-lhs-ps/pat))))
          (struct-copy clause old-clauses
                       [eq/dqs
                        (append 
@@ -1393,30 +1397,30 @@
       ans)))
 
 (define-for-syntax (make-mf-clauses lhss rhss extrass nts err-name name lang)
-  (define-values (rev-clauses _)
+  (define-values (rev-clauses _1 _2)
-    (for/fold ([clauses '()]
+    (for/fold ([clauses '()] [prev-lhs-pats '()] [prev-lhs-pats* '()]) 
-               [prev-lhs-pats '()]) ([lhs (in-list lhss)]
+      ([lhs (in-list lhss)] [rhs (in-list rhss)] [extras (in-list extrass)])
-                                     [rhs (in-list rhss)]
+      (with-syntax* ([(lhs-pat (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs nts err-name #t lhs)]
-                                     [extras (in-list extrass)])
+                     [((lhs-pat-ps* ...) lhs-pat*) (fix-and-extract-dq-vars #'lhs-pat)])
-      (with-syntax ([(lhs-pat (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs nts err-name #t lhs)])
         (define-values (ps-rw extra-eqdqs p-names) 
           (rewrite-prems #f (syntax->list extras) nts (syntax->datum #'(names ...)) 'define-metafunction))
         (define-values (rhs-pats mf-clausess) (rewrite-terms (list rhs) p-names)) 
         (define clause-stx
           (with-syntax ([(prem-rw ...) ps-rw]
                         [(eqs ...) extra-eqdqs]
-                        [(((lhs-pat-ps ...) prev-lhs-pat) ...)
+                        [(((prev-lhs-pat-ps ...) prev-lhs-pat) ...) prev-lhs-pats*]
-                         (map fix-and-extract-dq-vars prev-lhs-pats)]
                         [(mf-clauses ...) mf-clausess]
                         [(rhs-pat) rhs-pats])
             #`((clause '(list lhs-pat rhs-pat)
-                       (list eqs ... (dqn '(lhs-pat-ps ...) 'prev-lhs-pat 'lhs-pat) ...)
+                       (list eqs ... (dqn '(prev-lhs-pat-ps ...) 'prev-lhs-pat 'lhs-pat) ...)
                        (list prem-rw ... mf-clauses ...)
                        #,lang
                        '#,name)
-               lhs-pat)))
+               lhs-pat
+               ((lhs-pat-ps* ...) lhs-pat*))))
         (values (cons clause-stx clauses)
-                (cons #'lhs-pat prev-lhs-pats)))))
+                (cons #'lhs-pat prev-lhs-pats)
+                (cons #'((lhs-pat-ps* ...) lhs-pat*) prev-lhs-pats*)))))
   (reverse rev-clauses))
 
 (define-for-syntax (fix-and-extract-dq-vars pat)
@@ -1426,12 +1430,11 @@
       [(name vname p)
        (with-syntax ([((vs ...) new-p) (recur #'p)]
                      [new-vn (datum->syntax #'vname
-                                            (let* ([vn (syntax-e #'vname)]
+                                            (let ([vn (syntax-e #'vname)])
-                                                   [vn-sym (format "~s_" vn)])
                                               (hash-ref new-ids vn
                                                         (λ ()
                                                           (define new 
-                                                            (syntax-e (generate-temporary vn-sym)))
+                                                            (syntax-e (generate-temporary (format "~s_" vn))))
                                                           (set! new-ids (hash-set new-ids vn new))
                                                           new)))
                                             #'vname)])

collects/redex/tests/gen-test.rkt

@@ -8,35 +8,44 @@
                   bound
                   lvar))
 
+
+(define-syntax-rule (is-not-false e)
+  (test-equal (not e) #f))
+
+(define-syntax-rule (is-false e)
+  (test-equal e #f))
+
 (let ()
   (define-language L0)
   
-  (test-equal (check-dq `a `a (make-hash) L0 (hash))
+  (test-equal (check-dq (dq '() (list `a `a)) (make-hash) L0 (hash))
               #f)
-  (test-equal (check-dq `a `b (make-hash) L0 (hash))
+  (test-equal (check-dq (dq '() (list `a `b)) (make-hash) L0 (hash))
               #t)
-  (test-equal (check-dq `(list a) `(list a) (make-hash) L0 (hash))
+  (test-equal (check-dq (dq '() (list `(list a) `(list a))) (make-hash) L0 (hash))
               #f)
-  (test-equal (check-dq `(list a) `(list b) (make-hash) L0 (hash))
+  (test-equal (check-dq (dq '() (list `(list a) `(list b))) (make-hash) L0 (hash))
               #t)
-  (test-equal (check-dq `(list number) `(list variable) (make-hash) L0 (hash))
+  (test-equal (check-dq (dq '() (list `(list number) `(list variable))) (make-hash) L0 (hash))
               #t)
-  (test-equal (check-dq `(list a) `(list number) (make-hash) L0 (hash))
+  (test-equal (check-dq (dq '() (list `(list a) `(list number))) (make-hash) L0 (hash))
               #t)
-  (test-equal (check-dq `(list 2) `(list variable-not-otherwise-mentioned) (make-hash) L0 (hash))
+  (test-equal (check-dq (dq '() (list `(list 2) `(list variable-not-otherwise-mentioned))) (make-hash) L0 (hash))
               #t)
-  (test-equal (check-dq `(list a b) `(list a number) (make-hash) L0 (hash))
+  (test-equal (check-dq (dq '() (list `(list a b) `(list a number))) (make-hash) L0 (hash))
               #t)
-  (test-equal (check-dq `(list a b) `(list a b) (make-hash) L0 (hash))
+  (test-equal (check-dq (dq '() (list `(list a b) `(list a b))) (make-hash) L0 (hash))
               #f)
-  (test-equal (check-dq `(list (name a ,(bound)))
+  (test-equal (check-dq (dq '()
-                        `(list (name a ,(bound)))
+                            (list `(list (name a ,(bound)))
+                                  `(list (name a ,(bound)))))
                         (make-hash)
                         L0
                         (hash (lvar 'a) 'number))
               #f)
-  (test-equal (check-dq `(name a ,(bound))
+  (test-equal (check-dq (dq '()
-                        `(name b ,(bound))
+                            (list `(name a ,(bound))
+                                  `(name b ,(bound))))
                         (make-hash (list (cons (lvar 'a) '(1 2 3))
                                          (cons (lvar 'b) '(1 2 3))))
                         L0
@@ -151,26 +160,6 @@
    #t)
   )
 
-(let ()
-  (define-language STLC
-    (τ int
-       (τ → τ))
-    (Γ ([x τ] Γ)
-       •)
-    (x variable-not-otherwise-mentioned))
-  
-  (define-metafunction STLC
-    [(lookup x ([x τ] Γ))
-     τ]
-    [(lookup x ([x_1 τ] Γ))
-     (lookup x Γ)])
-  
-  (test-equal (generate-term STLC
-                             #:satisfying
-                             (lookup x ([x int] ([x (int → int)] •))) = (int → int)
-                             6)
-              #f))
-
 (let ()
   
   (define-language simple
@@ -281,6 +270,12 @@
      (typ-if Γ e_2 τ)
      (typ-if Γ e_3 τ)])
   
+  (test-equal (generate-term STLC
+                             #:satisfying
+                             (lookup x ([x int] ([x (int → int)] •))) = (int → int)
+                             6)
+              #f)
+  
   (test-equal (judgment-holds (typeof ([x_1 int] ([x_1 (int → int)] •)) (x_1 5) int))
               #f)
   (test-equal (judgment-holds (typeof ([x_2 int] ([x_1 (int → int)] •)) (x_1 5) int))
@@ -404,6 +399,19 @@
   (test-equal (generate-term L #:satisfying (is-a/b? c) = any +inf.0)
               '((is-a/b? c) = F))
   
+  (test-equal (generate-term L #:satisfying (is-a? a) = F +inf.0)
+              #f)
+  (test-equal (generate-term L #:satisfying (is-a? b) = T +inf.0)
+              #f)
+  (test-equal (generate-term L #:satisfying (is-a? c) = T +inf.0)
+              #f)
+  (test-equal (generate-term L #:satisfying (is-a/b? a) = F +inf.0)
+              #f)
+  (test-equal (generate-term L #:satisfying (is-a/b? b) = F +inf.0)
+              #f)
+  (test-equal (generate-term L #:satisfying (is-a/b? c) = T +inf.0)
+              #f)
+  
   (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? a) = any +inf.0)
               '((is-a/b/c/d/e? a) = T))
   (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? b) = any +inf.0)
@@ -415,7 +423,20 @@
   (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? e) = any +inf.0)
               '((is-a/b/c/d/e? e) = T))
   (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? f) = any +inf.0)
-              '((is-a/b/c/d/e? f) = F)))
+              '((is-a/b/c/d/e? f) = F))
+  
+  (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? a) = F +inf.0)
+              #f)
+  (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? b) = F +inf.0)
+              #f)
+  (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? c) = F +inf.0)
+              #f)
+  (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? d) = F +inf.0)
+              #f)
+  (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? e) = F +inf.0)
+              #f)
+  (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? f) = T +inf.0)
+              #f))
 
 ;; errors for unsupprted pats
 (let ()
@@ -608,11 +629,6 @@
 
 (let ()
   
-  (define-syntax-rule (is-not-false e)
-    (test-equal (not e) #f))
-  
-  (define-syntax-rule (is-false e)
-    (test-equal e #f))
   
   (define-language L0)
   
@@ -658,4 +674,40 @@
   (is-not-false (generate-term L0 #:satisfying (J ((1) (2))) +inf.0))
   (is-false (generate-term L0 #:satisfying (J ((1) (#f))) 5))
   (is-false (generate-term L0 #:satisfying (J ((#f) (2))) 5))
-  (is-not-false (generate-term L0 #:satisfying (J ((#t) (2))) 5)))
+  (is-not-false (generate-term L0 #:satisfying (J ((#t) (2))) 5)))
+
+(let ()
+  (define-language L0)
+  
+  (define-metafunction L0
+    [(f (any_1 any_2))
+     2]
+    [(f any_1)
+     1])
+  
+  (define-judgment-form L0
+    #:mode (J I I)
+    [(J (any_1 any_2) 2)]
+    [(J any_1 1)])
+  
+  
+  (test-equal (generate-term L0
+                             #:satisfying
+                             (f (any_1 any_2)) = 1
+                             +inf.0)
+              #f)
+  
+  (test-equal (not
+               (generate-term L0
+                              #:satisfying
+                              (f (any_1 any_2)) = 2
+                              +inf.0))
+              #f)
+  (is-not-false
+   (for/and ([_ 50])
+     (match (generate-term L0
+                           #:satisfying
+                           (f any) = 1
+                           5)
+       [`((f (,a ,b)) = 1) #f]
+       [else #t]))))

collects/redex/tests/unify-tests.rkt

@@ -1091,6 +1091,19 @@
               (,(lvar 'd) . (nt Q))) 
             '() #f)
 
+;; resolve fully
+;; (necessary for parameter elimination to be correct)
+(check-not-false
+ (env-equal?
+  (disunify
+   '(a)
+   '(list (name a any) (name a any))
+   '(list (name b any) 2)
+   (env '#hash() '())
+   #f)
+  (env (hash (lvar 'a) 'any (lvar 'b) 'any)
+       (list (dq '() `((list (name b ,(bound))) (list 2)))))))
+
 
 
 (let ([untested