improve handling of ellipses in premises when checking modeless judgment forms

Author: rfindler

redex-lib/redex/private/matcher.rkt

@@ -621,19 +621,35 @@ See match-a-pattern.rkt for more details
              (loop (cdr matches) (cons merged acc))
              (loop (cdr matches) acc)))])))
 
-(define (combine-bindings-lists bindings1 bindings2 lang-α-equal?)
+(define (combine-bindings-lists bindings1 bindings1-to-dup
+                                bindings2 bindings2-to-dup
+                                lang-α-equal?)
   (define all-combinations/f
     (for*/list ([binding1 (in-list bindings1)]
                 [binding2 (in-list bindings2)])
+      (define table1 (bindings-table binding1))
+      (define table2 (bindings-table binding2))
       (merge-multiples/remove/bindings
-       (make-bindings (append (bindings-table binding1)
-                              (bindings-table binding2)))
+       (make-bindings (append (fill-out-duplicates table1 bindings1-to-dup binding2)
+                              (fill-out-duplicates table2 bindings2-to-dup binding1)))
        lang-α-equal?)))
   (define all-combinations (filter values all-combinations/f))
   (cond
     [(null? all-combinations) #f]
     [else all-combinations]))
 
+(define (fill-out-duplicates table to-duplicate table-with-lengths)
+  (for/list ([a-bind (in-list table)])
+    (define n (bind-name a-bind))
+    (cond
+      [(member n to-duplicate)
+       (define exp (bind-exp a-bind))
+       (define how-many-times (length (lookup-binding table-with-lengths n)))
+       (bind n
+             (for/list ([i (in-range how-many-times)])
+               exp))]
+      [else a-bind])))
+
 ;; merge-multiples/remove : bindings (exp exp -> boolean) -> (union #f bindings)
 ;; returns #f if all duplicate bindings don't bind the same thing
 ;; returns a new bindings 
@@ -2110,7 +2126,9 @@ See match-a-pattern.rkt for more details
                        compiled-lang?))
  [combine-bindings-lists
   (-> (listof bindings?)
+      (listof symbol?)
       (listof bindings?)
+      (listof symbol?)
       (procedure-arity-includes/c 2)
       (or/c #f (non-empty-listof bindings?)))])
 (provide compiled-pattern? 

redex-lib/redex/private/modeless-jf.rkt

@@ -169,14 +169,38 @@
                        (lookup-binding bnds 'modeless-prem-names) ...)
                     body)))))
 
+       (define (get-id-depths ids)
+         (define ht (make-hash))
+         (for ([id (in-list (syntax->list ids))])
+           (define-values (sym depth) (get-id-depth id))
+           (hash-set! ht sym depth))
+         ht)
+       (define (get-id-depth stx)
+         (let loop ([stx stx]
+                    [n 0])
+           (syntax-case stx ()
+             [(more ell)
+              (is-ellipsis? #'ell)
+              (loop #'more (+ n 1))]
+             [_ (values (syntax-e stx) n)])))
+       (define premise-id-depths (get-id-depths #'(modeless-prem-names/ellipses ...)))
+       (define conc-id-depths (get-id-depths #'(conc-names/ellipses ...)))
+       (define (get-ids-to-dup our-id-depths others-id-depths)
+         (for/list ([(id depth) (in-hash our-id-depths)]
+                    #:when (< depth
+                              (hash-ref others-id-depths id -inf.0)))
+           id))
+
        #`(begin
            conc-syncheck-exp
            modeless-jf-name-only-prems-syncheck-exp
            modeless-prems-syncheck-exp
            (build-modeless-jf-clause
             lang
             `conc
+            '(#,@(get-ids-to-dup conc-id-depths premise-id-depths))
             `modeless-prem
+            '(#,@(get-ids-to-dup premise-id-depths conc-id-depths))
             `modeless-jf-name-only-prem
             '(#,@premise-repeat-names)
             #,other-conditions
@@ -205,10 +229,14 @@
                               (list)
                               (list #`(cons #f (list #,@noname-clauses))))))))
 
-(define (build-modeless-jf-clause lang conc modeless-prem modeless-jf-name-only-prem
+(define (build-modeless-jf-clause lang conc conc-ids-to-duplicate
+                                  modeless-prem modeless-prem-ids-to-duplicate
+                                  modeless-jf-name-only-prem
                                   premise-repeat-names other-conditions funcs)
   (modeless-jf-clause (compile-pattern lang conc #f)
+                      conc-ids-to-duplicate
                       (compile-pattern lang modeless-prem #f)
+                      modeless-prem-ids-to-duplicate
                       (compile-pattern lang modeless-jf-name-only-prem #f)
                       premise-repeat-names other-conditions funcs))
 
@@ -276,7 +304,9 @@
   (match candidates
     [`() (fail)]
     [(cons (modeless-jf-clause conclusion-compiled-pattern
+                               conclusion-ids-to-duplicate
                                premises-compiled-pattern
+                               premise-ids-to-duplicate
                                premises-jf-name-only-compiled-pattern
                                premises-repeat-names
                                other-conditions
@@ -297,10 +327,15 @@
             (cons (symbol->string (car t)) (cdr t))))
         (define sub-derivations-mtch (match-pattern premises-compiled-pattern
                                                     sub-derivations-arguments-term-list))
+        (define sub-derivation-bindings (and sub-derivations-mtch
+                                             (map mtch-bindings sub-derivations-mtch)))
+        (define conc-bindings (map mtch-bindings conc-mtch))
         (define conc+sub-bindings
           (and sub-derivations-mtch
-               (combine-bindings-lists (map mtch-bindings conc-mtch)
-                                       (map mtch-bindings sub-derivations-mtch)
+               (combine-bindings-lists sub-derivation-bindings
+                                       premise-ids-to-duplicate
+                                       conc-bindings
+                                       conclusion-ids-to-duplicate
                                        (λ (a b) (alpha-equivalent? lang a b)))))
         (cond
           [conc+sub-bindings
@@ -332,6 +367,7 @@
            (fail-to-next-candidate)])]
        [else (fail-to-next-candidate)])]))
 
+
 (define (modeless-jf-process-other-conditions lang
                                               sub-derivations
                                               conc+sub-bindings
@@ -398,13 +434,15 @@
               [_ #f])]))])))
 
 (struct modeless-jf-clause (conclusion-compiled-pattern
+                            conclusion-ids-to-duplicate
 
                             ;; pattern with all of the premises
                             ;; strung together in a list, but where
                             ;; the names of the judgment forms are
                             ;; strings instead of symbols (so that they
                             ;; don't accidentally run into non-terminals, etc)
                             premises-compiled-pattern
+                            premises-ids-to-duplicate
 
                             ;; pattern with all of the premises jf-names strung
                             ;; together, but with `any` for all of the arguments

redex-test/redex/tests/tl-judgment-form.rkt

@@ -1627,4 +1627,37 @@
                      (list)))
         #f))
 
+(let ()
+  (define-language L)
+
+  (define-judgment-form L
+
+    [-------------- "nat"
+     (⊢ natural N)]
+
+    [-------------- "bool"
+     (⊢ boolean B)]
+
+    [(⊢ any_many any_dup) ...
+     ---------------------------- "all-same"
+     (⊢ (any_many ...) any_dup)])
+
+  (test (judgment-holds
+         ⊢
+         (derivation
+          '(⊢ (0) N)
+          "all-same"
+          (list (derivation '(⊢ 0 N) "nat" (list)))))
+        #t)
+
+  (test (judgment-holds
+         ⊢
+         (derivation
+          '(⊢ (0 1 2) N)
+          "all-same"
+          (list (derivation '(⊢ 0 N) "nat" (list))
+                (derivation '(⊢ 1 N) "nat" (list))
+                (derivation '(⊢ 2 N) "nat" (list)))))
+        #t))
+
 (print-tests-passed 'tl-judgment-form.rkt)