finished docs port for redex and cleaned up some of the exampels
svn: r11092
This commit is contained in:
Robby Findler
parent
3f14a1325c
commit
ed6a9bad40
|
|
@ -1,41 +1,41 @@
|
|||
#lang scheme
|
||||
(require redex)
|
||||
|
||||
(define-language lang
|
||||
(e (binop e e)
|
||||
(sqrt e)
|
||||
number)
|
||||
(binop +
|
||||
-
|
||||
*
|
||||
/)
|
||||
|
||||
(define-language lang
|
||||
(e (binop e e)
|
||||
(sqrt e)
|
||||
number)
|
||||
(binop +
|
||||
-
|
||||
*
|
||||
/)
|
||||
|
||||
(e-ctxt (binop e e-ctxt)
|
||||
(binop e-ctxt e)
|
||||
(sqrt e-ctxt)
|
||||
hole)
|
||||
(v number))
|
||||
|
||||
(define reductions
|
||||
(reduction-relation
|
||||
lang
|
||||
(c--> (+ number_1 number_2)
|
||||
,(+ (term number_1) (term number_2))
|
||||
"add")
|
||||
(c--> (- number_1 number_2)
|
||||
,(- (term number_1) (term number_2))
|
||||
"subtract")
|
||||
(c--> (* number_1 number_2)
|
||||
,(* (term number_1) (term number_2))
|
||||
"multiply")
|
||||
(c--> (/ number_1 number_2)
|
||||
,(/ (term number_1) (term number_2))
|
||||
"divide")
|
||||
(c-->(sqrt number_1)
|
||||
,(sqrt (term number_1))
|
||||
"sqrt")
|
||||
with
|
||||
[(--> (in-hole e-ctxt_1 a) (in-hole e-ctxt_1 b))
|
||||
(c--> a b)]))
|
||||
|
||||
(traces reductions (term (- (* (sqrt 36) (/ 1 2)) (+ 1 2))))
|
||||
(e-ctxt (binop e e-ctxt)
|
||||
(binop e-ctxt e)
|
||||
(sqrt e-ctxt)
|
||||
hole)
|
||||
(v number))
|
||||
|
||||
(define reductions
|
||||
(reduction-relation
|
||||
lang
|
||||
(c--> (+ number_1 number_2)
|
||||
,(+ (term number_1) (term number_2))
|
||||
"add")
|
||||
(c--> (- number_1 number_2)
|
||||
,(- (term number_1) (term number_2))
|
||||
"subtract")
|
||||
(c--> (* number_1 number_2)
|
||||
,(* (term number_1) (term number_2))
|
||||
"multiply")
|
||||
(c--> (/ number_1 number_2)
|
||||
,(/ (term number_1) (term number_2))
|
||||
"divide")
|
||||
(c-->(sqrt number_1)
|
||||
,(sqrt (term number_1))
|
||||
"sqrt")
|
||||
with
|
||||
[(--> (in-hole e-ctxt_1 a) (in-hole e-ctxt_1 b))
|
||||
(c--> a b)]))
|
||||
|
||||
(traces reductions (term (- (* (sqrt 36) (/ 1 2)) (+ 1 2))))
|
||||
|
|
|
|||
|
|
@ -918,6 +918,6 @@ reflects the (broken) spec).
|
|||
false)))))
|
||||
|
||||
;; timing test
|
||||
;#;
|
||||
#;
|
||||
(time (run-tests)
|
||||
(run-big-test))
|
||||
|
|
@ -47,11 +47,11 @@
|
|||
(subst (x_1 e_1 e_3)))]
|
||||
[(subst (x_1 e_1 number_1)) number_1])
|
||||
|
||||
(traces lang reductions
|
||||
(traces reductions
|
||||
'(let (plus (lambda (m)
|
||||
(lambda (n)
|
||||
(lambda (s)
|
||||
(lambda (z)
|
||||
(app (app m s) (app (app n s) z)))))))
|
||||
(let (two (lambda (s) (lambda (z) (app s (app s z)))))
|
||||
(app (app plus two) two))))
|
||||
(app (app plus two) two))))
|
||||
|
|
|
|||
|
|
@ -54,38 +54,11 @@
|
|||
(define (make-w b c c*) `(,c ((,c ((,b ,c) ((,c ((,b j) ,c*)) ,c*))) ,c*)))
|
||||
(define (make-s b c w) `((,b ((,b (,b ,w)) ,c)) (,b ,b)))
|
||||
|
||||
(traces lang
|
||||
relation
|
||||
(traces relation
|
||||
(list
|
||||
`((,c* abs1) abs2)
|
||||
`(((,(make-c 'c*) abs1) abs2) abs3)
|
||||
`(((,(make-b 'c) abs1) abs2) abs3)
|
||||
`((,(make-w 'b 'c 'c*) abs1) abs2)
|
||||
`(((,(make-s 'b 'c 'w) abs1) abs2) abs3))
|
||||
#:multiple #t)
|
||||
|
||||
(require (lib "pretty.ss"))
|
||||
#;
|
||||
(let loop ([t (make-s (make-b (make-c c*))
|
||||
(make-c c*)
|
||||
(make-w (make-b (make-c c*))
|
||||
(make-c c*)
|
||||
c*))]
|
||||
[i 0])
|
||||
(when (zero? (modulo i 100))
|
||||
(display i)
|
||||
(display " ")
|
||||
(flush-output))
|
||||
(let ([next (apply-reduction-relation ij-relation t)])
|
||||
(if (null? next)
|
||||
(begin (newline)
|
||||
(pretty-print t))
|
||||
(loop (car next) (+ i 1)))))
|
||||
|
||||
#;
|
||||
(traces lang ij-relation
|
||||
(make-s (make-b (make-c c*))
|
||||
(make-c c*)
|
||||
(make-w (make-b (make-c c*))
|
||||
(make-c c*)
|
||||
c*)))
|
||||
#:multiple? #t)
|
||||
|
|
|
|||
|
|
@ -14,4 +14,4 @@
|
|||
|
||||
(define ->r (compatible-closure r grammar B))
|
||||
|
||||
(traces grammar ->r '((f * f) * (t * f)))
|
||||
(traces ->r '((f * f) * (t * f)))
|
||||
|
|
|
|||
|
|
@ -117,7 +117,7 @@ BUG: letrec & let are not handled properly by substitution
|
|||
with
|
||||
[(--> a ,(collect (term b))) (==> a b)]))
|
||||
|
||||
(define (run e) (traces lang reductions `((store) ,e)))
|
||||
(define (run e) (traces reductions `((store) ,e)))
|
||||
|
||||
(run '(letrec ((f (lambda (x)
|
||||
(letrec ((y (f 1)))
|
||||
|
|
|
|||
|
|
@ -31,6 +31,6 @@
|
|||
(in-hole c_1 (subst (variable_x v_arg e_body)))
|
||||
βv)))
|
||||
|
||||
(traces lang reductions '((lambda (x) (x x)) (lambda (x) (x x))))
|
||||
(traces lang reductions '((call/cc call/cc) (call/cc call/cc)))
|
||||
(traces lang reductions '((lambda (x) ((call/cc call/cc) x)) (call/cc call/cc)))
|
||||
(traces reductions '((lambda (x) (x x)) (lambda (x) (x x))))
|
||||
(traces reductions '((call/cc call/cc) (call/cc call/cc)))
|
||||
(traces reductions '((lambda (x) ((call/cc call/cc) x)) (call/cc call/cc)))
|
||||
|
|
|
|||
|
|
@ -149,15 +149,13 @@ semaphores make things much more predictable...
|
|||
(in-hole c (void))
|
||||
e_after ...)))))
|
||||
|
||||
(stepper lang
|
||||
reductions
|
||||
(stepper reductions
|
||||
`((store (y (list)))
|
||||
(semas)
|
||||
(threads (set! y (cons 1 y))
|
||||
(set! y (cons 2 y)))))
|
||||
|
||||
(stepper lang
|
||||
reductions
|
||||
(stepper reductions
|
||||
`((store (y (list)))
|
||||
(semas (x 1))
|
||||
(threads (begin (semaphore-wait (semaphore x))
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@
|
|||
|
||||
;; this rules calls subst with the wrong arguments, which is caught by the example below.
|
||||
(--> (in-hole c_1 ((lambda (x_format t_1) e_body) v_actual))
|
||||
(in-hole c_1 (subst x_format v_actual e_body))
|
||||
(in-hole c_1 (subst (x_format e_body v_actual)))
|
||||
βv)))
|
||||
|
||||
(define (type-check term)
|
||||
|
|
@ -65,6 +65,43 @@
|
|||
(and t1
|
||||
(equal? (type-check term2) t1)))))
|
||||
|
||||
(define-language subst-lang
|
||||
(x variable))
|
||||
|
||||
(define-metafunction subst-lang
|
||||
[(subst-n ((x_1 any_1) (x_2 any_2) ... any_3))
|
||||
(subst (x_1 any_1 (subst-n ((x_2 any_2) ... any_3))))]
|
||||
[(subst-n (any_3)) any_3])
|
||||
|
||||
(define-metafunction subst-lang
|
||||
;; 1. x_1 bound, so don't continue in λ body
|
||||
[(subst (x_1 any_1 (λ (x_1 t) any_2)))
|
||||
(λ (x_1 t) any_2)]
|
||||
;; 2. general purpose capture avoiding case
|
||||
[(subst (x_1 any_1 (λ (x_2 t) any_2)))
|
||||
,(term-let ([x_new
|
||||
(variable-not-in (term (x_1 any_1 any_2))
|
||||
(term x_2))])
|
||||
(term
|
||||
(λ (x_new t)
|
||||
(subst (x_1 any_1 (subst-vars ((x_2 x_new) any_2)))))))]
|
||||
;; 3. replace x_1 with e_1
|
||||
[(subst (x_1 any_1 x_1)) any_1]
|
||||
;; 4. x_1 and x_2 are different, so don't replace
|
||||
[(subst (x_1 any_1 x_2)) x_2]
|
||||
;; the last two cases cover all other expression forms
|
||||
[(subst (x_1 any_1 (any_2 ...)))
|
||||
((subst (x_1 any_1 any_2)) ...)]
|
||||
[(subst (x_1 any_1 any_2)) any_2])
|
||||
|
||||
(define-metafunction subst-lang
|
||||
[(subst-vars ((x_1 any_1) x_1)) any_1]
|
||||
[(subst-vars ((x_1 any_1) (any_2 ...))) ((subst-vars ((x_1 any_1) any_2)) ...)]
|
||||
[(subst-vars ((x_1 any_1) any_2)) any_2]
|
||||
[(subst-vars ((x_1 any_1) (x_2 any_2) ... any_3))
|
||||
(subst-vars ((x_1 any_1) (subst-vars ((x_2 any_2) ... any_3))))]
|
||||
[(subst-vars (any)) any])
|
||||
|
||||
(define (show term)
|
||||
(traces reductions term #:pred (pred term)))
|
||||
|
||||
|
|
|
|||
|
|
@ -74,13 +74,14 @@
|
|||
(set! x (+ x -1))
|
||||
(set! x (+ x 1))))
|
||||
|
||||
#:pp
|
||||
(lambda (exp)
|
||||
(match exp
|
||||
[`((store (x ,x)) (threads ,t1 ,t2))
|
||||
(format "~a ~a ~a" x (count t1) (count t2))])))
|
||||
|
||||
(parameterize ([initial-char-width 16])
|
||||
(stepper threads reductions '((store) (threads
|
||||
(+ 1 1)
|
||||
(+ 1 1)
|
||||
(+ 1 1)))))
|
||||
(stepper reductions '((store) (threads
|
||||
(+ 1 1)
|
||||
(+ 1 1)
|
||||
(+ 1 1)))))
|
||||
|
|
|
|||
|
|
@ -74,6 +74,9 @@
|
|||
lw-column
|
||||
lw-column-span)
|
||||
|
||||
(provide to-lw
|
||||
(struct-out lw))
|
||||
|
||||
(provide/contract
|
||||
[just-before (-> (or/c pict? string? symbol?) lw? lw?)]
|
||||
[just-after (-> (or/c pict? string? symbol?) lw? lw?)])
|
||||
|
|
|
|||
|
|
@ -83,9 +83,9 @@ semantics.
|
|||
|
||||
This is a reference manual for Redex. See
|
||||
@link["http://www.cs.uchicago.edu/~robby/plt-redex/"]{
|
||||
@tt{http://www.cs.uchicago.edu/~robby/plt-redex/}
|
||||
}
|
||||
for a gentler overview.
|
||||
@tt{http://www.cs.uchicago.edu/~robby/plt-redex/}} for a gentler
|
||||
overview. (See also the @tt{examples} subdirectory in the @tt{redex}
|
||||
collection.)
|
||||
|
||||
To load Redex use: @defmodule[redex] which provides all of
|
||||
the names documented in this library.
|
||||
|
|
@ -1415,8 +1415,6 @@ it. The thunk may be invoked multiple times when rendering a
|
|||
single reduction relation.
|
||||
}
|
||||
|
||||
@subsection{Pink & LW}
|
||||
|
||||
@deftech{Removing the pink background from PLT Redex rendered picts and ps files}
|
||||
|
||||
When reduction rules, a metafunction, or a grammar contains
|
||||
|
|
@ -1501,23 +1499,35 @@ explanation of logical-space):
|
|||
}
|
||||
|
||||
|
||||
A _lw_ is a struct:
|
||||
(build-lw element posnum posnum posnum posnum)
|
||||
with selectors:
|
||||
> lw-e :: lw -> element
|
||||
> lw-line :: lw -> posnum
|
||||
> lw-line-span :: lw -> posnum
|
||||
> lw-column :: lw -> posnum
|
||||
> lw-column-span :: lw -> posnum
|
||||
@subsection{LW}
|
||||
|
||||
An _element_ is either:
|
||||
string
|
||||
symbol
|
||||
pict
|
||||
(listof lw)
|
||||
@deftogether[[
|
||||
@defproc[(build-lw [e (or/c string? symbol? pict? (listof lw?))]
|
||||
[line exact-positive-integer?]
|
||||
[line-span exact-positive-integer?]
|
||||
[column exact-positive-integer?]
|
||||
[column-span exact-positive-integer?])
|
||||
lw?]{}
|
||||
@defproc[(lw-e (lw lw?)) (or/c string? symbol? pict? (listof lw?))]{}
|
||||
@defproc[(lw-line (lw lw?)) exact-positive-integer?]{}
|
||||
@defproc[(lw-line-span (lw lw?)) exact-positive-integer?]{}
|
||||
@defproc[(lw-column (lw lw?)) exact-positive-integer?]{}
|
||||
@defproc[(lw-column-span (lw lw?)) exact-positive-integer?]{}
|
||||
@defproc[(lw? (v any/c)) boolean?]{}
|
||||
@defidform[lw]{}]]{
|
||||
|
||||
The lw data structure corresponds represents a
|
||||
pattern or a Scheme expression that is to be typeset.
|
||||
The lw data structure corresponds represents a pattern or a Scheme
|
||||
expression that is to be typeset. The functions listed above
|
||||
construct @scheme[lw] structs, select fields out of them, and
|
||||
recognize them. The @scheme[lw] binding can be used with
|
||||
@scheme[copy-struct].
|
||||
}
|
||||
|
||||
@defform[(to-lw arg)]{
|
||||
|
||||
This form turns its argument into lw structs that
|
||||
contain all of the spacing information just as it would appear
|
||||
when being used to typeset.
|
||||
|
||||
Each sub-expression corresponds to its own lw, and
|
||||
the element indicates what kind of subexpression it is. If
|
||||
|
|
@ -1595,6 +1605,7 @@ will be lined up underneath each other, but the relative
|
|||
positions of "boys" and "fudge" will be determined by the
|
||||
natural size of the words as they rendered in the
|
||||
appropriate font.
|
||||
}
|
||||
|
||||
There are two helper functions that make building
|
||||
lws easier:
|
||||
|
|
@ -1614,12 +1625,6 @@ just before or just after that argument. The line-span and
|
|||
column-span of the new lw is always zero.
|
||||
}
|
||||
|
||||
@defform[(to-lw arg)]{
|
||||
|
||||
This form turns its argument into lw structs that
|
||||
contain all of the spacing information just as it would appear
|
||||
when being used to typeset.
|
||||
}
|
||||
|
||||
@index-section[]
|
||||
|
||||
|
|
|
|||
|
|
@ -4,8 +4,7 @@
|
|||
(require "private/reduction-semantics.ss"
|
||||
"private/matcher.ss"
|
||||
"private/term.ss"
|
||||
"private/rg.ss"
|
||||
"private/loc-wrapper.ss")
|
||||
"private/rg.ss")
|
||||
|
||||
#;(provide (all-from-out "private/rg.ss"))
|
||||
|
||||
|
|
@ -40,9 +39,6 @@
|
|||
test-predicate
|
||||
test-results)
|
||||
|
||||
(provide to-lw
|
||||
(struct-out lw))
|
||||
|
||||
(provide/contract
|
||||
[reduction-relation->rule-names (-> reduction-relation? (listof symbol?))]
|
||||
[language-nts (-> compiled-lang? (listof symbol?))]
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user