8.12
Redex Abbrevs
(require redex-abbrevs) | package: redex-abbrevs-lib |
Macros for working with PLT Redex.
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)))))
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:
procedure
--> : 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.