Redex Abbrevs
check-mf-apply*
check-judgment-holds*
check-not-judgment-holds*
define-language+  +
make--->*
7.0

Redex Abbrevs

Macros for working with PLT Redex.

syntax

(check-mf-apply* #:is-equal? eq (actual expected) ...)

Expands to (begin (check eq (term actual) (term expected)) ...), where eq is equal? by default.

Examples:
> (define-language N
    (nat ::= Z (S nat)))
> (define-metafunction N
    add2 : nat -> nat
    [(add2 nat)
     (S (S nat))])
> (check-mf-apply*
   ((add2 Z)
    (S (S Z)))
   ((add2 (S Z))
    (S (S (S Z)))))

syntax

(check-judgment-holds* t ...)

Expands to (begin (check-true (judgment-holds t)) ...)

syntax

(check-not-judgment-holds* t ...)

Expands to (begin (check-false (judgment-holds t)) ...)

Examples:
> (define-language N
    (nat ::= Z (S nat)))
> (define-judgment-form N
    #:mode (is-zero I)
    [
     ---
     (is-zero Z)])
> (check-not-judgment-holds*
    (is-zero (S Z)))

syntax

(define-language++ lang-name #:alpha-equivalent? alpha-name non-terminal-def ... maybe-binding-spec)

Similar to define-language, but:
  • Defines a predicate for each non-terminal-def. The predicates have type (-> any/c boolean?) and return #true for terms that match the non-terminal.

  • Accepts an optional keyword argument alpha-name. If given, binds alpha-name to a function with type (-> any/c any/c boolean?) such that (alpha-name term0 term1) if and only if (alpha-equivalent? lang-name term0 term1).

Examples:
> (define-language++ N
    (nat ::= Z (S nat)))
> (nat? (term Z))

#t

procedure

(make--->* -->)  (-> any/c any/c)

  --> : reduction-relation?
The result of (make--->* -->) is a function on terms that acts like the reflexive-transitive closure of the reduction relation -->. If (apply-reduction-relation* --> t) returns a list with one term, then ((make--->* -->) t) will return the same term. Otherwise, ((make--->* -->) t) will raise an exception.