4.7 GUI🔗ℹ

This section describes the GUI tools that Redex provides for exploring reduction sequences.

The reduce function applies the reduction relation to the terms. By default, it is apply-reduction-relation/tag-with-names; it may be changed to only return a subset of the possible reductions, for example, but it must satisfy the same contract as apply-reduction-relation/tag-with-names.

If reductions is an IO-judgment-form?, then the judgment form is treated as a reduction relation. The initial input position is the given expr and the output position becomes the next input.

The pred function indicates if a term has a particular property. If it returns #f, the term is displayed with a pink background. If it returns a string or a color% object, the term is displayed with a background of that color (using the-color-database to map the string to a color). If it returns any other value, the term is displayed normally. If the pred function accepts two arguments, a term-node corresponding to the term is passed to the predicate. This lets the predicate function explore the (names of the) reductions that led to this term, using term-node-children, term-node-parents, and term-node-labels.

The pred function may be called more than once per node. In particular, it is called each time an edge is added to a node. The latest value returned determines the color.

The pp function is used to specially print expressions. It must either accept one or four arguments. If it accepts one argument, it will be passed each term and is expected to return a string to display the term.

If the pp function takes four arguments, it should render its first argument into the port (its second argument) with width at most given by the number (its third argument). The final argument is the text where the port is connected – characters written to the port go to the end of the editor. Use write-special to send snip% objects or 2htdp/image images (or other things that subscribe to file/convertible or pict/convert) directly to the editor.

The colors argument, if provided, specifies a list of reduction-name/color-list pairs. The traces gui will color arrows drawn because of the given reduction name with the given color instead of using the default color.

The cdr of each of the elements of colors is a list of colors, organized in pairs. The first two colors cover the colors of the line and the border around the arrow head, the first when the mouse is over a graph node that is connected to that arrow, and the second for when the mouse is not over that arrow. Similarly, the next colors are for the text drawn on the arrow and the last two are for the color that fills the arrow head. If fewer than six colors are specified, the specified colors are used and then defaults are filled in for the remaining colors.

The racket-colors? argument (along with scheme-colors?, retained for backward compatibility), controls the coloring of each window. When racket-colors? is #t (and scheme-colors? is #t too), traces colors the contents according to DrRacket’s Racket-mode color scheme; otherwise, traces uses a black color scheme.

The term-filter function is called each time a new node is about to be inserted into the graph. If the filter returns false, the node is not inserted into the graph.

The x-spacing and y-spacing arguments control the amount of space put between the snips in the default layout.

The layout argument is called (with all of the terms) when new terms are inserted into the window. In general, it is called after new terms are inserted in response to the user clicking on the reduce button, and after the initial set of terms is inserted. See also term-node-set-position!.

If edge-labels? is #t (the default), then edge labels are drawn; otherwise not.

The edge-label-font argument is used as the font on the edge labels. If #f is supplied, the dc<%> object’s default font is used.

The traces library uses an instance of the mrlib/graph library’s graph-pasteboard<%> interface to layout the graphs. Sometimes, overriding one of its methods can help give finer-grained control over the layout, so the graph-pasteboard-mixin is applied to the class before it is instantiated. Also note that all of the snips inserted into the editor by this library have a get-term-node method which returns the snip’s term-node?.

The Fix Layout button calls out to dot (a program that’s a part of graphviz) and uses its results to lay out the graph. While in the fixed-layout mode, the edges are now drawn. Click the button again to restore the edges.

All of the arguments behave like the arguments to traces, with the exception of the post-process argument. It is called just before the PostScript is created with the graph pasteboard.

The pp argument is the same as to the traces function but is here for backwards compatibility only and should not be changed for most uses, but instead adjusted with pretty-print-parameters. Specifically, the highlighting shown in the stepper window can be wrong if default-pretty-printer does not print sufficiently similarly to how pretty-print prints (when adjusted by pretty-print-parameters’s behavior, of course).

If show-font-size-control? is a true value, then a slider with a font size choice is shown in the window.

Changed in version 1.1 of package redex-gui-lib: Added the show-font-size-control? argument.

Changed in version 1.1 of package redex-gui-lib: Added the show-font-size-control? argument.

The pp and racket-colors? arguments are like those to traces.

The initial derivation shown in the window is chosen by init-derivation, used as an index into derivations.

Note that this function does not return all terms that this term reduces to – only those that are currently in the graph.

If its value is a number, then the number is used as the width for every term. If its value is a function, then the function is called with each term and the resulting number is used as the width.

The dark colors are used when the mouse is over one of the nodes that is connected to this edge. The light colors are used when it isn’t.

The pen colors control the color of the line. The brush colors control the color used to fill the arrowhead and the text colors control the color used to draw the label on the edge.

Specifically, whenever default-pretty-printer prints something it calls f with a thunk that does the actual printing. Thus, f can adjust pretty-print’s parameters to adjust how printing happens.

This function uses the value of pretty-print-parameters to adjust how it prints.

It sets the pretty-print-columns parameter to width, and it sets pretty-print-size-hook and pretty-print-print-hook to print holes and the symbol 'hole to match the way they are input in a term expression.