1111 vc-append hbl-append vl-append)
1212 redex))
1313
14- @(define redex-eval (make-base-eval '(require redex/reduction-semantics)))
14+ @(define redex-eval (make-base-eval '(require redex/reduction-semantics redex/pict)))
15+ @; this definition is copied from languages.scrbl
16+ @(redex-eval
17+ '(define-language lc-lang
18+ (e ::= (e e ... )
19+ x
20+ (λ (x ... ) e))
21+ (v ::= (λ (x ... ) e))
22+ (E ::= (v ... E e ... )
23+ hole)
24+ (x y ::= variable-not-otherwise-mentioned)))
1525
1626@title{Other Relations}
1727
@@ -99,8 +109,8 @@ clause to be taken.
99109The @racket[clause-name] is used only when typesetting. See
100110@racket[metafunction-cases].
101111
102- The @racket[or ] clause is used to define a form of conditional
103- right-hand side of a metafunction . In particular, if any of the
112+ The @racket[or ] clause is used to define piecewise conditional
113+ metafunctions . In particular, if any of the
104114@racket[where] or @racket[side-condition] clauses fail, then
105115evaluation continues after an @racket[or ] clause, treating the
106116term that follows as the result (subject to any subsequent
@@ -110,6 +120,29 @@ clause, once for each @racket[or] expression, but signals to
110120the typesetting library to use a large left curly brace to group
111121the conditions in the @racket[or ].
112122
123+ For example, here are two equivalent definitions of a @racket[biggest]
124+ metafunction that typeset differently:
125+
126+ @examples[#:eval redex-eval
127+ (define-metafunction lc-lang
128+ biggest : natural natural -> natural
129+ [(biggest natural_1 natural_2)
130+ natural_2
131+ (side-condition (< (term natural_1) (term natural_2)))]
132+ [(biggest natural_1 natural_2)
133+ natural_1])
134+ (render-metafunction biggest)
135+ (define-metafunction lc-lang
136+ biggest : natural natural -> natural
137+ [(biggest natural_1 natural_2)
138+ natural_2
139+ (side-condition (< (term natural_1) (term natural_2)))
140+
141+ or
142+
143+ natural_1])
144+ (render-metafunction biggest)]
145+
113146Note that metafunctions are assumed to always return the same results
114147for the same inputs, and their results are cached, unless
115148@racket[caching-enabled?] is set to @racket[#f ]. Accordingly, if a
0 commit comments