Redex Miscellanea
1 Metafunctions
substitute-env
substitute*
lookup
ext
unique
rem
2 Macros
match-term
3 Functions
make-eval
current-max-steps
4 Typography
define-language/  style
define-extended-language/  style
render-language/  style
render-metafunction/  style
render-metafunctions/  style
render-judgment-form/  style
render-reduction-relation/  style
render-term/  style
nt-set
nt-set?
current-rule-label?
current-compact-threshold
current-arrow-hash
current-serif-font
current-sans-serif-font
current-mono-font
current-font-size
5 Rewriting
substitute-rw
substitute*-rw
lookup-rw
lookup*-rw
typing-rw
set-add-rw
sf-rw
sans-rw
mono-rw
unquote-rw
rw/  c
default-atomic-rewriters
default-compound-rewriters
default-unquote-rewriters
7.8

Redex Miscellanea

Cameron Moy

 (require redex-etc) package: redex-etc

This library is under development; compatibility will not be maintained.

This package implements miscellaneous metafunctions, macros, and functions for Redex. For the purposes of illustration, we will use the following language in our examples.

(define-language Λ
  [e ::= x v (e e ...)]
  [v ::= (λ (x ...) e)]
  [x ::= variable-not-otherwise-mentioned]
  [E ::= hole (v ... E e ...)]
 
  #:binding-forms
  (λ (x ...) e #:refers-to (shadow x ...)))
 
(default-language Λ)

1 Metafunctions

metafunction

(substitute-env target ([key value] ...))

Given an environment, a list of keys and values, replaces instances of key with value in the target term.

Example:
> (term (substitute-env x ([x 1] [y 2])))

1

metafunction

(substitute* target [key value] ...)

Shorthand for a call to substitute-env with the given key-value pairs as an environment.

Example:
> (term (substitute* x [x 1] [y 2]))

1

metafunction

(lookup ([key value] ...) needle)

Returns the first value whose key matches the needle. If none match, #f is returned.

Example:
> (term (lookup ([x 1] [y 2]) x))

1

metafunction

(ext ([key value] ...) [new-key new-value] ...)

Extends the given environment with the new key-value pairs, adding where the key isn’t already present, and overriding the value if the key is present.

Example:
> (term (ext ([x 1] [y 2]) [x 2] [z 3]))

'((z 3) (x 2) (y 2))

metafunction

(unique (any ...))

Returns whether the given elements are unique.

Examples:
> (term (unique (1 2 3)))

#t

> (term (unique (1 2 2)))

#f

metafunction

(rem ([key value] ...) old-key ...)

Removes the associations with the old-key if they are present in the environment. Does nothing otherwise.

Example:
> (term (rem ([x 1] [y 2]) x z))

'((y 2))

2 Macros

syntax

(match-term lang expression [pattern expression] ...)

Matches the given term against a series of patterns, choosing the expression corresponding to the first matching pattern.

Example:
> (match-term Λ (term (λ (x) (x x)))
    [(λ _ e) (term e)])

'(x«0» x«0»)

3 Functions

procedure

(make-eval rr    
  [#:inject inject    
  #:project project    
  #:program? program?    
  #:answer? answer?])  (-> any/c any)
  rr : reduction-relation?
  inject : (-> any/c any) = values
  project : (-> any/c any) = values
  program? : predicate/c = (const #t)
  answer? : predicate/c = (const #t)
Returns an evaluation function that applies the given reduction relation until reaching a normal form. The evaluation function will inject into an initial machine configuration and project out of the final configuration. Initial and final expressions will be checked against program? and answer? respectively. The evaluation function takes a maximum of current-max-steps steps before aborting. Additionally it will throw an error on a non-deterministic or non-terminating result.

Examples:
> (define v
    (reduction-relation Λ
      [--> (in-hole E ((λ (x ..._a) e) v ..._a))
           (in-hole E (substitute* e [x v] ...))
           βv]))
> (define  (make-eval v))
> ( (term ((λ (x) x) (λ (y) y))))

'(λ (y) y)

parameter

(current-max-steps)  natural?

(current-max-steps max-steps)  void?
  max-steps : natural?
 = 50
A parameter that determines the maximum number of steps the evaluation function created by make-eval will take before quitting.

Example:
> ( (term ((λ (x) ((x x) x)) (λ (y) ((y y) y)))))

make-eval: exceeded maximum number of steps

4 Typography

Redex has the ability to typeset your model for use directly in a paper. Sadly, the default typesetting options are out of place in acmart papers. What follows are a bunch of “stylish” rendering utilities that typeset the model with my preferences.

syntax

(define-language/style lang-name
  non-terminal-def ...
  maybe-binding-spec)
 
non-terminal-def = (nt ...+  nt-set ::= pattern ...+ maybe-rhs)
     
maybe-rhs = 
  | #:define
  | #:define rhs-expr
Defines a language like define-language, but also defines non-terminal set names.

Examples:
> (define-language/style L
    [e  Expr ::= x v]
    [v  Val ::= n]
    [n  Int ::= integer #:define]
    [x  Var ::= variable-not-otherwise-mentioned
                 #:define (nt-set "identifiers")])
> (render-language/style L)

image

syntax

(define-extended-language/style extended-lang base-lang
  non-terminal-def ...
  maybe-binding-spec)
Defines a language like define-extended-language, but can also define non-terminal set names.

procedure

(render-language/style lang [file #:nts nts])  pict?

  lang : compiled-lang?
  file : (or/c #f path-string?) = #f
  nts : (or/c #f (listof (or/c string? symbol?)))
   = (render-language-nts)
Renders like render-language, but stylish.

syntax

(render-metafunction/style metafunction-name maybe-contract)

(render-metafunction/style metafunction-name filename maybe-contract)

syntax

(render-metafunctions/style metafunction-name ...
  maybe-filename maybe-contract maybe-only-contract)
Renders like render-metafunction, but stylish.

syntax

(render-judgment-form/style judgment-form-name)

(render-judgment-form/style judgment-form-name filename)
Renders like render-judgment-form, but stylish.

procedure

(render-reduction-relation/style rel 
  [file 
  #:style style]) 
  (if file void? pict-convertible?)
  rel : reduction-relation?
  file : (or/c #f path-string?) = #f
  style : reduction-rule-style/c = (rule-pict-style)
Renders like render-reduction-relation, but stylish.

syntax

(render-term/style lang term)

(render-term/style lang term file)
Renders like render-term, but stylish.

procedure

(nt-set non-terminal-def)  nt-set?

  non-terminal-def : string?
Creates a right-hand-side expression for use in define-language/style and define-extended-language/style.

procedure

(nt-set? x)  boolean?

  x : any/c
Predicate that recognizes an nt-set.

parameter

(current-rule-label?)  boolean?

(current-rule-label? rule-label?)  void?
  rule-label? : boolean?
 = #t
Determines reduction relation rules names are rendered with render-reduction-relation/style.

parameter

(current-compact-threshold)  natural?

(current-compact-threshold compact-threshold)  void?
  compact-threshold : natural?
Determines the width to begin wrapping side conditions when rendering with render-reduction-relation/style.

parameter

(current-arrow-hash)  (hash/c symbol? string?)

(current-arrow-hash arrow-hash)  void?
  arrow-hash : (hash/c symbol? string?)
Maps symbols to strings for the arrows in a reduction relation.

parameter

(current-serif-font)  text-style/c

(current-serif-font serif-font)  void?
  serif-font : text-style/c
 = "Linux Libertine"

parameter

(current-sans-serif-font)  text-style/c

(current-sans-serif-font sans-serif-font)  void?
  sans-serif-font : text-style/c
 = "Linux Biolinum"

parameter

(current-mono-font)  text-style/c

(current-mono-font mono-font)  void?
  mono-font : text-style/c
 = "DejaVu Sans Mono"

parameter

(current-font-size)  natural?

(current-font-size font-size)  void?
  font-size : natural?
 = 22
Fonts and font preferences for stylish renderers.

5 Rewriting

procedure

(substitute-rw op [#:flip? flip?])  rw/c

  op : string?
  flip? : boolean? = #f

procedure

(substitute*-rw op [#:flip? flip?])  rw/c

  op : string?
  flip? : boolean? = #f
Rewriter for substitutions.

value

lookup-rw : rw/c

value

lookup*-rw : rw/c

Rewriter for lookups.

procedure

(typing-rw op)  rw/c

  op : string?
Rewriter for typing.

procedure

(set-add-rw op)  rw/c

  op : string?
Rewriter for adding an element to a set.

procedure

(sf-rw font-family)  rw/c

  font-family : text-style/c

procedure

(sans-rw font-family)  rw/c

  font-family : text-style/c

procedure

(mono-rw font-family)  rw/c

  font-family : text-style/c
Rewriters for font families.

procedure

(unquote-rw replacement)  (-> lw? lw?)

  replacement : 
(or/c string?
      symbol?
      pict-convertible?
      (listof (or/c (symbols 'spring) lw?)))
Unquoted rewriter.

value

rw/c : contract?

Recognizes a rewriter. Equivalent to (-> (listof lw?) (listof (or/c lw? string? pict-convertible?))).

parameter

(default-atomic-rewriters)

  
(plistof symbol?
         (listof (or/c lw?
                       string?
                       pict-convertible?)))
(default-atomic-rewriters atomic-rewriters)  void?
  atomic-rewriters : 
(plistof symbol?
         (listof (or/c lw?
                       string?
                       pict-convertible?)))

parameter

(default-compound-rewriters)  (plistof symbol? rw/c)

(default-compound-rewriters compound-rewriters)  void?
  compound-rewriters : (plistof symbol? rw/c)

parameter

(default-unquote-rewriters)  (plistof symbol? (-> lw? lw?))

(default-unquote-rewriters unquote-rewriters)  void?
  unquote-rewriters : (plistof symbol? (-> lw? lw?))
The rewriters to use when rendering stylish.