suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

where clauses in metafunctions now are in 'term'

Browse Source 
svn: r11300
This commit is contained in:
Robby Findler 2008-08-18 21:23:56 +00:00
parent f6a754c48a
commit 5895bf4c35
5 changed files with 54 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
collects/redex/HISTORY
View File

@ -6,6 +6,9 @@ v4.2
- added render-* functions that make it easier to experiment
with typesetting at the REPL.
- where clauses in metafunctions now are implicitly in
`term's (they were not documented at all before)
v4.1 (this is the first version that was included in the PLT
distribution. Before this, Redex was in PLaneT).

20
collects/redex/private/reduction-semantics.ss
View File

@ -781,6 +781,24 @@
((metafunc-proc-in-dom? mp)
exp)))
;
;
;
; ; ;;; ; ;;
; ;; ;;;; ;; ;;
; ;;;;;;; ;;;; ;;; ;;;;; ;;;;;;; ;;;;; ;;;; ;;;; ;;;; ;;; ;;;;; ;;;;; ;;;; ;;;; ;;;
; ;;;;;;;;;;;;; ;;;;; ;;;;;; ;;;;;;;; ;;;; ;;;; ;;;; ;;;;;;;;; ;;;;;; ;;;;;; ;;;; ;;;;;; ;;;;;;;;;
; ;;;; ;;; ;;;; ;;;; ;; ;;;; ;;;; ;;;;;; ;;;; ;;;; ;;;; ;;;; ;;;;;;; ;;;; ;;;; ;;;;;;;; ;;;; ;;;;
; ;;;; ;;; ;;;; ;;;;;;; ;;;; ;;;;;;; ;;;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;; ;;;; ;;;;
; ;;;; ;;; ;;;; ;;;;; ;;;;; ;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;;;;; ;;;;; ;;;; ;;;;;;;; ;;;; ;;;;
; ;;;; ;;; ;;;; ;;;;;; ;;;;; ;;;;;;;; ;;;; ;;;;;;;;; ;;;; ;;;; ;;;;;; ;;;;; ;;;; ;;;;;; ;;;; ;;;;
; ;;;; ;;; ;;;; ;;;; ;;;; ;; ;;;; ;;;; ;;; ;;;; ;;;; ;;;; ;;;;; ;;;; ;;;; ;;;; ;;;; ;;;;
;
;
;
(define-syntax-set (define-metafunction define-metafunction/extension)
(define (define-metafunction/proc stx)
@ -858,7 +876,7 @@
(syntax
(λ (name bindings)
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
(term-let ([tl-var tl-exp] ...)
(term-let ([tl-var (term tl-exp)] ...)
(term-let-fn ((name name))
(term rhs)))))))))
(syntax->list (syntax (lhs ...)))

13
collects/redex/private/size-snip.ss
View File

@ -2,7 +2,8 @@
(require (lib "mred.ss" "mred")
(lib "class.ss")
(lib "pretty.ss")
(lib "framework.ss" "framework"))
(lib "framework.ss" "framework")
"matcher.ss")
(provide reflowing-snip<%>
size-editor-snip%
@ -13,7 +14,15 @@
(define initial-char-width (make-parameter 30))
(define (default-pretty-printer v port w spec)
(parameterize ([pretty-print-columns w])
(parameterize ([pretty-print-columns w]
[pretty-print-size-hook
(λ (val display? op)
(cond
[(hole? val) 4]
[else #f]))]
[pretty-print-print-hook
(λ (val display? op)
(display "hole" op))])
(pretty-print v port)))
(define reflowing-snip<%>

10
collects/redex/private/tl-test.ss
View File

@ -397,9 +397,17 @@
(define-metafunction empty-language
[(f (number_1 number_2))
number_3
(where number_3 (+ (term number_1) (term number_2)))])
(where number_3 ,(+ (term number_1) (term number_2)))])
(test (term (f (11 17))) 28))
(let ()
(define-metafunction empty-language
[(f variable)
(x x)
(where x (variable variable))])
(test (term (f z))
(term ((z z) (z z)))))
(let ()
(define-language x-lang
(x variable))

18
collects/redex/redex.scrbl
View File

@ -607,12 +607,14 @@ all non-GUI portions of Redex) and also exported by
@defform/subs[#:literals (--> fresh side-condition where)
(reduction-relation language reduction-case ...)
((reduction-case (--> #, @|ttpattern| #, @|tttterm| extras ...))
(extras name
([reduction-case (--> #, @|ttpattern| #, @|tttterm| extras ...)]
[extras name
(fresh fresh-clause ...)
(side-condition scheme-expression ...)
(where tl-pat #, @|tttterm|))
(fresh-clause var ((var1 ...) (var2 ...))))]{
(where tl-pat #, @|tttterm|)]
[fresh-clause var ((var1 ...) (var2 ...))]
[tl-pat identifier (tl-pat-ele ...)]
[tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
Defines a reduction relation casewise, one case for each of the
clauses beginning with @scheme[-->]. Each of the @scheme[pattern]s
@ -811,10 +813,14 @@ all non-GUI portions of Redex) and also exported by
@defform/subs[#:literals (: ->)
(define-metafunction language-exp
contract
[(name #, @|ttpattern| ...) #, @|tttterm| (side-condition scheme-expression) ...]
[(name #, @|ttpattern| ...) #, @|tttterm| extras ...]
...)
([contract (code:line)
(code:line id : #, @|ttpattern| ... -> #, @|ttpattern|)])]{
(code:line id : #, @|ttpattern| ... -> #, @|ttpattern|)]
[extras (side-condition scheme-expression)
(where tl-pat #, @|tttterm|)]
[tl-pat identifier (tl-pat-ele ...)]
[tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
The @scheme[define-metafunction] form builds a function on
sexpressions according to the pattern and right-hand-side