Skip to content

Commit 4fbcfe2

Browse files
committed
work in the word piecewise (and add an example to explain why it is interesting)
closes #148
1 parent e1ed446 commit 4fbcfe2

File tree

2 files changed

+38
-4
lines changed

2 files changed

+38
-4
lines changed

redex-doc/redex/scribblings/ref/languages.scrbl

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,8 @@ side-condition @|pattern|s can restrict matches in complex ways.
4646
A @racket[non-terminal-def] comprises one or more non-terminal names
4747
(considered aliases) followed by one or more productions.
4848

49-
For example, the following defines @deftech{@racket[_lc-lang]} as the
49+
@; this language is copied to other-relations.scrbl to be used in examples there, too
50+
For example, the following defines @deftech{@racket[_lc-lang]} as the
5051
grammar of the λ-calculus:
5152
@examples[#:label #f #:eval redex-eval #:no-prompt #:no-result
5253
(define-language lc-lang

redex-doc/redex/scribblings/ref/other-relations.scrbl

Lines changed: 36 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,17 @@
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.
99109
The @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
105115
evaluation continues after an @racket[or] clause, treating the
106116
term that follows as the result (subject to any subsequent
@@ -110,6 +120,29 @@ clause, once for each @racket[or] expression, but signals to
110120
the typesetting library to use a large left curly brace to group
111121
the 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+
113146
Note that metafunctions are assumed to always return the same results
114147
for the same inputs, and their results are cached, unless
115148
@racket[caching-enabled?] is set to @racket[#f]. Accordingly, if a

0 commit comments

Comments
 (0)