Add rule names to runtime judgment form, for stepper support

Add the list of rule names to the runtime judgment form struct, so the stepper
can support displaying rule names in the reduction name label, and "run" a
judgment until a specific rule.

Author: wilbowma

redex-gui-lib/redex/private/stepper.rkt

@@ -132,9 +132,8 @@ todo:
                              [editor zoom-out-pb]))
 
     (define choice-vp (new vertical-panel% [alignment '(center center)] [parent lower-hp] [stretchable-width #f]))
-    (define reduction-names (if (IO-judgment-form? red)
-                                '()
-                                (reduction-relation->rule-names red)))
+    (define reduction-names (reduction-relation/IO-jf->rule-names red))
+
     (define reds-choice 
       (and (not (null? reduction-names))
            (new choice%

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

@@ -44,7 +44,8 @@
                                            compiled-input-contract-pat
                                            compiled-output-contract-pat
                                            input-contract-pat
-                                           output-contract-pat)
+                                           output-contract-pat
+                                           rule-names)
   #:methods gen:custom-write
   [(define (write-proc rjf port _mode)
      (if (runtime-judgment-form-mode rjf)
@@ -66,7 +67,8 @@
                                      name proc mode lang
                                      original-contract-expression ;; (or/c #f (listof s-exp))
                                      input-contract-pat
-                                     output-contract-pat)
+                                     output-contract-pat
+                                     (rule-names '()))
   (define cache (cons (box (make-hash)) (box (make-hash))))
   (make-runtime-judgment-form
    name proc mode cache lang
@@ -98,7 +100,15 @@
             (runtime-judgment-form-input-contract-pat parent-judgment-form)))
    (or output-contract-pat
        (and parent-judgment-form
-            (runtime-judgment-form-output-contract-pat parent-judgment-form)))))
+            (runtime-judgment-form-output-contract-pat parent-judgment-form)))
+   (map (lambda (raw-name)
+          (cond
+            [raw-name => (lambda (x)
+                           (if (symbol? x)
+                               x
+                               (string->symbol x)))]
+            [else raw-name]))
+        rule-names)))
 
 (define-for-syntax (prune-syntax stx)
   (datum->syntax
@@ -939,7 +949,8 @@
                                          #,lang
                                          original-contract-expression
                                          judgment-form-input-contract
-                                         judgment-form-output-contract))
+                                         judgment-form-output-contract
+                                         '#,rule-names))
           (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-lib/redex/private/reduction-semantics.rkt

@@ -2871,7 +2871,7 @@
 (define (reduction-relation/IO-jf->rule-names x)
   (cond
     [(reduction-relation? x) (reduction-relation->rule-names x)]
-    [(IO-judgment-form? x) '(judgment-form->rule-names x)]))
+    [(IO-judgment-form? x) (runtime-judgment-form-rule-names x)]))
 
 
 ;                                                                               
@@ -3361,6 +3361,7 @@
 (provide (rename-out [-reduction-relation reduction-relation])
          ::=
          reduction-relation->rule-names
+         reduction-relation/IO-jf->rule-names
          reduction-relation/IO-jf-lang
          extend-reduction-relation
          reduction-relation?