7 GUI

(require redex/gui)

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

(traces   reductions             expr            [ #:multiple? multiple?             #:pred pred             #:pp pp             #:colors colors])   →   void?

reductions : reduction-relation?

expr : (or/c any/c (listof any/c))

multiple? : boolean? = #f

pred   :   (or/c (sexp -> any) (sexp term-node? any))       =   (lambda (x) #t)

pp   :   (or/c (any -> string)       (any output-port number (is-a?/c text%) -> void))       =   default-pretty-printer

colors : (listof (list string string)) = '()

This function opens a new window and inserts each expression in expr (if multiple? is #t – if multiple? is #f, then expr is treated as a single expression). Then, it reduces the terms until at least reduction-steps-cutoff (see below) different terms are found, or no more reductions can occur. It inserts each new term into the gui. Clicking the reduce button reduces until reduction-steps-cutoff more terms are found.

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.

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

You can save the contents of the window as a postscript file from the menus.

(stepper reductions t [pp]) → void?

reductions : reduction-relation?

t : any/c

pp   :   (or/c (any -> string)       (any output-port number (is-a?/c text%) -> void))       =   default-pretty-printer

This function opens a stepper window for exploring the behavior of its third argument in the reduction system described by its first two arguments.

The pp argument is the same as to the traces functions (above).

(stepper/seed reductions seed [pp]) → void?

reductions : reduction-relation?

seed : (cons/c any/c (listof any/c))

pp   :   (or/c (any -> string)       (any output-port number (is-a?/c text%) -> void))       =   default-pretty-printer

Like stepper, this function opens a stepper window, but it seeds it with the reduction-sequence supplied in seed.

(term-node-children tn) → (listof term-node?)

tn : term-node?

Returns a list of the children (ie, terms that this term reduces to) of the given node.

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

(term-node-parents tn) → (listof term-node?)

tn : term-node?

Returns a list of the parents (ie, terms that reduced to the current term) of the given node.

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

(term-node-labels tn) → (listof (or/c false/c string?))

tn : term-node

Returns a list of the names of the reductions that led to the given node, in the same order as the result of term-node-parents. If the list contains #f, that means that the corresponding step does not have a label.

(term-node-set-color! tn color) → void?

tn : term-node?

color : (or/c string? (is-a?/c color%) false/c)

Changes the highlighting of the node; if its second argument is #f, the coloring is removed, otherwise the color is set to the specified color% object or the color named by the string. The color-database<%> is used to convert the string to a color% object.

(term-node-set-red! tn red?) → void?

tn : term-node?

red? : boolean?

Changes the highlighting of the node; if its second argument is #t, the term is colored pink, if it is #f, the term is not colored specially.

(term-node-expr tn) → any

tn : term-node?

Returns the expression in this node.

(term-node? v) → boolean?

v : any/c

Recognizes term nodes.

(reduction-steps-cutoff) → number?

(reduction-steps-cutoff cutoff) → void?

cutoff : number?

A parameter that controls how many steps the traces function takes before stopping.

(initial-font-size) → number?

(initial-font-size size) → void?

size : number?

A parameter that controls the initial font size for the terms shown in the GUI window.

(initial-char-width) → number?

(initial-char-width width) → void?

width : number?

A parameter that determines the initial width of the boxes where terms are displayed (measured in characters) for both the stepper and traces.

(dark-pen-color) → (or/c string? (is-a?/c color<%>)) (dark-pen-color color) → void?   color : (or/c string? (is-a?/c color<%>))

(dark-brush-color) → (or/c string? (is-a?/c color<%>)) (dark-brush-color color) → void?   color : (or/c string? (is-a?/c color<%>))

(light-pen-color) → (or/c string? (is-a?/c color<%>)) (light-pen-color color) → void?   color : (or/c string? (is-a?/c color<%>))

(light-brush-color) → (or/c string? (is-a?/c color<%>)) (light-brush-color color) → void?   color : (or/c string? (is-a?/c color<%>))

These four parameters control the color of the edges in the graph.

(default-pretty-printer v port width text) → void?

v : any

port : output-port

width : number

text : (is-a?/c text%)

This is the default value of pp used by traces and stepper and it uses pretty-print.