From bfa50ae031d3bb244c4cd403c230b5e0c3ad55df Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Sat, 22 Oct 2005 03:14:58 +0000 Subject: [PATCH] fixed up doc.txt and added labels to the arithmetic.ss example svn: r1127 --- collects/reduction-semantics/doc.txt | 12 +++-- .../examples/arithmetic.ss | 45 ++++++++++--------- 2 files changed, 33 insertions(+), 24 deletions(-) diff --git a/collects/reduction-semantics/doc.txt b/collects/reduction-semantics/doc.txt index 9a4eb197e8..5a19a8f94c 100644 --- a/collects/reduction-semantics/doc.txt +++ b/collects/reduction-semantics/doc.txt @@ -228,7 +228,7 @@ for two `term-let'-bound identifiers bound to lists of different lengths to appear together inside an ellipsis. > (reduction language pattern bodies ...) SYNTAX -> (reduction/name language pattern bodies ...) SYNTAX + This form defines a reduction. The first position must evaluate to a language defined by the `language' form. The pattern determines which terms this reductions apply to and @@ -261,12 +261,14 @@ the result of evaluating the last argument to reduction. See `plug' below and lc-subst is defined by using the subst.ss library below. +> (reduction/name name language pattern bodies ...) SYNTAX + The reduction/name form is the same as reduction, but additionally evaluates the `name' expression and names the -reduction to be its result, which must be a string. +reduction to be its result, which must be a string. The +names are used by `traces'. > (reduction/context language context pattern bodies ...) SYNTAX -> (reduction/context/name name language context pattern bodies ...) SYNTAX reduction/context is a short-hand form of reduction. It automatically adds the `in-hole' pattern and the call to @@ -281,9 +283,13 @@ example is this: (term (v_i ...)) (term e_body)))) +> (reduction/context/name name language context pattern bodies ...) SYNTAX + reduction/context/name is the same as reduction/context, but additionally evaluates the `name' expression and names the reduction to be its result, which must be a string. +The names are used by `traces'. + > red? : (any? . -> . boolean?) diff --git a/collects/reduction-semantics/examples/arithmetic.ss b/collects/reduction-semantics/examples/arithmetic.ss index 9d617c9579..5515375934 100644 --- a/collects/reduction-semantics/examples/arithmetic.ss +++ b/collects/reduction-semantics/examples/arithmetic.ss @@ -12,33 +12,36 @@ * /) - (e-ctxt (binop e e-ctxt) + (e-ctxt (binop v e-ctxt) (binop e-ctxt e) (sqrt e-ctxt) hole) (v number))) + (define-syntax (--> stx) + (syntax-case stx () + [(_ op from to) + (syntax (reduction/name op + lang + (in-hole e-ctxt_1 from) + (term (in-hole e-ctxt_1 ,to))))])) + (define reductions (list - (reduction lang - (in-hole e-ctxt_1 - (+ number_1 number_2)) - (plug (term e-ctxt_1) (+ (term number_1) (term number_2)))) - (reduction/context lang - e-ctxt - (- number_1 number_2) - (- (term number_1) (term number_2))) - (reduction/context lang - e-ctxt - (* number_1 number_2) - (* (term number_1) (term number_2))) - (reduction/context lang - e-ctxt - (/ number_1 number_2) - (/ (term number_1) (term number_2))) - (reduction/context lang - e-ctxt - (sqrt number_1) - (sqrt (term number_1))))) + (--> "add" + (+ number_1 number_2) + (+ (term number_1) (term number_2))) + (--> "subtract" + (- number_1 number_2) + (- (term number_1) (term number_2))) + (--> "multiply" + (* number_1 number_2) + (* (term number_1) (term number_2))) + (--> "divide" + (/ number_1 number_2) + (/ (term number_1) (term number_2))) + (--> "sqrt" + (sqrt number_1) + (sqrt (term number_1))))) (traces lang reductions '(- (* (sqrt 36) (/ 1 2)) (+ 1 2)))) \ No newline at end of file