improve render-judgment-form and judgment-form->pict so they don't need to see the judgment form at compile time (ie, make them functions)

Author: rfindler

redex-doc/redex/scribblings/ref/typesetting.scrbl

@@ -369,8 +369,7 @@ This function sets @racket[dc-for-text-size]. See also
 @racket[relation->pict].
 }
 
-@defform*[[(render-judgment-form judgment-form-name)
-           (render-judgment-form judgment-form-name filename)]]{
+@defproc[(render-judgment-form [judgment-form judgment-form?] [filename (or/c path-string? #f)]) pict?]{
 Like @racket[render-metafunction] but for judgment forms. The
 @racket[judgment-form-cases] parameter can be used to control which clauses
 are rendered.
@@ -428,8 +427,8 @@ This function sets @racket[dc-for-text-size]. See also
   @racketmodname[pict]s.
 }
 
-@defform[(judgment-form->pict judgment-form-name)]{
-  This produces a pict, but without setting @racket[dc-for-text-size].
+@defproc[(judgment-form->pict [judgment-form judgment-form?]) pict?]{
+  Produces a pict like @racket[render-judgment-form], but without setting @racket[dc-for-text-size].
   It is suitable for use in Slideshow or other libraries that combine
   @racketmodname[pict]s.
 }

redex-lib/redex/HISTORY.txt

@@ -1,3 +1,9 @@
+v8.17
+
+  * render-judgment-form and judgment-form->pict are functions, making
+    them suitable to abstract over (before, they required their
+    arguments to be identifiers bound to judgment forms)
+
 v8.16
 
   * bug fixes

redex-lib/redex/private/judgment-form.rkt

@@ -45,7 +45,9 @@
                                            compiled-output-contract-pat
                                            input-contract-pat
                                            output-contract-pat
-                                           rule-names)
+                                           rule-names
+                                           lws
+                                           relation?)
   #:methods gen:custom-write
   [(define (write-proc rjf port _mode)
      (if (runtime-judgment-form-mode rjf)
@@ -68,7 +70,9 @@
                                      original-contract-expression ;; (or/c #f (listof s-exp))
                                      input-contract-pat
                                      output-contract-pat
-                                     (rule-names '()))
+                                     rule-names
+                                     lws
+                                     relation?)
   (define cache (cons (box (make-hash)) (box (make-hash))))
   (make-runtime-judgment-form
    name proc mode cache lang
@@ -108,7 +112,9 @@
                                x
                                (string->symbol x)))]
             [else raw-name]))
-        rule-names)))
+        rule-names)
+   lws
+   relation?))
 
 (define-for-syntax (prune-syntax stx)
   (datum->syntax
@@ -957,7 +963,9 @@
                                          original-contract-expression
                                          judgment-form-input-contract
                                          judgment-form-output-contract
-                                         '#,rule-names))
+                                         '#,rule-names
+                                         jf-lws
+                                         #,is-relation?))
           (define jf-cache (runtime-judgment-form-cache the-runtime-judgment-form))
           (define original-contract-expression-id
             (runtime-judgment-form-original-contract-expression the-runtime-judgment-form))

redex-pict-lib/redex/private/pict.rkt

@@ -1604,6 +1604,9 @@
        (make-pict))]))
 
 (define judgment-form-show-rule-names (make-parameter #t))
+
+;; inference-rules-pict : ?? ?? (listof (or/c #f string?)) ?? boolean? -> pict?
+;;   eqn-names is expected to be a list of all of the names in the jf/relation, in order
 (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))
@@ -1695,37 +1698,28 @@
 (define horizontal-bar-spacing (make-parameter 4))
 (define relation-clauses-combine (make-parameter (λ (l) (apply vc-append 20 l))))
 
-(define-for-syntax (inference-rules-pict/judgment-form form-name)
-  (define jf (syntax-local-value form-name))
-  (define-values (name lws rule-names lang relation?) 
-    (values (judgment-form-name jf) (judgment-form-lws jf) (judgment-form-rule-names jf)
-            (judgment-form-lang jf) (judgment-form-relation? jf)))
-  (syntax-property
-   #`(inference-rules-pict '#,name
-                           #,lws
-                           '#,rule-names
-                           #,lang
-                           #,(not relation?))
-   'disappeared-use
-   (syntax-local-introduce form-name)))
-
-(define-syntax (render-judgment-form stx)
-  (syntax-case stx ()
-    [(_ form-name . opt-arg)
-     (if (judgment-form-id? #'form-name)
-         (let ([save-as (syntax-case #'opt-arg ()
-                          [() #'#f]
-                          [(path) #'path])])
-           #`(render-pict (λ () #,(inference-rules-pict/judgment-form #'form-name))
-                          #,save-as))
-         (raise-syntax-error #f "expected a judgment form name" stx #'form-name))]))
-
-(define-syntax (judgment-form->pict stx)
-  (syntax-case stx ()
-    [(_ form-name)
-     (if (judgment-form-id? #'form-name)
-         (inference-rules-pict/judgment-form #'form-name)
-         (raise-syntax-error #f "expected a judgment form name" stx #'form-name))]))
+(define (inference-rules-pict/judgment-form who jf save-as)
+  (unless (runtime-judgment-form? jf)
+    (error who "expected a judgment-form\n  given: ~e" jf))
+  (render-pict
+   (λ ()
+     (inference-rules-pict (runtime-judgment-form-name jf)
+                           (runtime-judgment-form-lws jf)
+                           (for/list ([name (in-list (runtime-judgment-form-rule-names jf))])
+                             (if (symbol? name)
+                                 (symbol->string name)
+                                 #f))
+                           (runtime-judgment-form-lang jf)
+                           (not (runtime-judgment-form-relation? jf))))
+   save-as))
+
+(define (render-judgment-form jf [path #f])
+  (inference-rules-pict/judgment-form 'render-judgment-form
+                                      jf
+                                      path))
+
+(define (judgment-form->pict jf)
+  (inference-rules-pict/judgment-form 'judgment-form->pict jf #f))
 
 ;                              
 ;