adjust define-judgment-form's typesetting so that it

tracks the lines of the premises in the source when
deciding how to linebreak the premises of the typeest form

collects/redex/private/pict.rkt

@@ -1076,7 +1076,8 @@
   (inference-rules-pict (metafunc-proc-name (metafunction-proc mf))
                         (metafunc-proc-pict-info (metafunction-proc mf))
                         (map (λ (x) #f) (metafunc-proc-pict-info (metafunction-proc mf)))
-                        (metafunc-proc-lang (metafunction-proc mf))))
+                        (metafunc-proc-lang (metafunction-proc mf))
+                        #f))
 
 (define (render-pict make-pict filename)
   (cond
@@ -1086,7 +1087,7 @@
      (parameterize ([dc-for-text-size (make-object bitmap-dc% (make-object bitmap% 1 1))])
        (make-pict))]))
 
-(define (inference-rules-pict name all-eqns eqn-names lang)
+(define (inference-rules-pict name all-eqns eqn-names lang judgment-form?)
   (define all-nts (language-nts lang))
   (define (wrapper->pict lw) (lw->pict all-nts lw))
   (define all-conclusions 
@@ -1096,21 +1097,55 @@
          all-eqns))
   (define-values (selected-eqns conclusions selected-eqn-names)
     (select-jf-cases all-eqns all-conclusions eqn-names))
-  (define premisess (map (lambda (eqn)
+  
-                           (append (map wrapper->pict (list-ref eqn 2))
+  (define (wrapper->pict+lines lw)
-                                   (map (match-lambda
+    (list (wrapper->pict lw) (lw-line lw) (+ (lw-line lw) (lw-line-span lw))))
-                                          [(struct metafunc-extra-where (lhs rhs))
+  
-                                           (where-pict (wrapper->pict lhs) (wrapper->pict rhs))]
+  ;; premises : (listof (listof pict))
-                                          [(struct metafunc-extra-side-cond (expr))
+  ;; each inner list of premises goes on the same line; each element
-                                           (wrapper->pict expr)]
+  ;; of the outer list is a separate line
-                                          [wrapper (wrapper->pict wrapper)])
+  (define premisess 
-                                        (list-ref eqn 1))))
+    (for/list ([eqn (in-list selected-eqns)])
-                         selected-eqns))
+      ;; all-premises : (listof pict number[first-line] number [last-line])
+      (define all-premises
+        (append (map wrapper->pict+lines (list-ref eqn 2))
+                (map (match-lambda
+                       [(struct metafunc-extra-where (lhs rhs))
+                        (list (where-pict (wrapper->pict lhs) (wrapper->pict rhs))
+                              (lw-line lhs)
+                              (+ (lw-line rhs) (lw-line-span rhs)))]
+                       [(struct metafunc-extra-side-cond (expr))
+                        (wrapper->pict+lines expr)]
+                       [wrapper (wrapper->pict+lines wrapper)])
+                     (list-ref eqn 1))))
+      (define sorted-premises (sort all-premises < #:key (λ (x) (list-ref x 1))))
+       
+      ;; returns #t if the two premises share at least one line in common
+      (define (overlaps? premise1 premise2)
+        (<= (list-ref premise1 1)
+            (list-ref premise2 1)
+            (list-ref premise1 2)))
+      
+      (cond
+        [(not judgment-form?) (list (map car all-premises))]
+        [(null? sorted-premises) '()]
+        [else
+         (define line-grouped-premises (list (list (car sorted-premises))))
+         (for ([prev-premise (in-list sorted-premises)]
+               [premise (in-list (cdr sorted-premises))])
+           (cond
+             [(overlaps? prev-premise premise)
+              (set! line-grouped-premises (cons (cons premise (car line-grouped-premises))
+                                                (cdr line-grouped-premises)))]
+             [else
+              (set! line-grouped-premises (cons (list premise) line-grouped-premises))]))
+         (reverse (map (λ (x) (reverse (map car x))) line-grouped-premises))])))
+
   ((relation-clauses-combine)
    (for/list ([conclusion (in-list conclusions)]
               [premises (in-list premisess)]
               [name (in-list selected-eqn-names)])
-     (define top (apply hbl-append 20 premises))
+     (define top (apply vc-append 4 (map (λ (premises) (apply hbl-append 20 premises)) premises)))
      (define line-w (max (pict-width top) (pict-width conclusion)))
      (define line (dc (λ (dc dx dy) (send dc draw-line dx dy (+ dx line-w) dy))
                       line-w 1)) 
@@ -1138,7 +1173,8 @@
    #`(inference-rules-pict '#,(judgment-form-name jf)
                            #,(judgment-form-lws jf)
                            '#,(judgment-form-rule-names jf)
-                           #,(judgment-form-lang jf))
+                           #,(judgment-form-lang jf)
+                           #t)
    'disappeared-use
    (syntax-local-introduce form-name)))
 

collects/redex/tests/bitmap-test.rkt

@@ -318,8 +318,7 @@
   (define-judgment-form nats
     #:mode (uses-ellipses I)
     [(uses-ellipses (n ...))
-     (lt2 n) ...
+     (lt2 n) ... (sum z z z)])
-     (sum z z z)])
   
   (btest (vc-append 
           10
@@ -352,8 +351,7 @@
     #:mode (typeof I I O)
     #:contract (typeof Γ e τ)
     [(typeof Γ (e_1 e_2) τ)
-     (typeof Γ e_1 (τ_2 → τ))
+     (typeof Γ e_1 (τ_2 → τ)) (typeof Γ e_2 τ_2)]
-     (typeof Γ e_2 τ_2)]
     [(typeof Γ (λ (x : τ) e) (τ → σ))
      (typeof (extend Γ x τ) e σ)]
     [(typeof Γ x τ)