Redex Miscellanea

7.7

top ← prev up next →

Redex Miscellanea

Cameron Moy

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

procedure
(genloc x) → symbol?
x : symbol?

Generates a fresh location, a variable prefixed with ℓ, based on the given variable name.

Example:

> (genloc 'x)
'ℓx3189

top ← prev up next →