Redex Abbrevs

8.12

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.

procedure
(step/deterministic --> trm) → any/c
--> : reduction-relation?
trm : any/c

Similar to apply-reduction-relation, but either returns one term or raises an exception.