added a amb-based redex tutorial

collects/redex/private/tut-util.rkt

@@ -0,0 +1,66 @@
+#lang at-exp racket/base
+
+(require scribble/base 
+         scribble/core
+         scriblib/autobib)
+(provide exercise exref 
+         generate-bibliography ~cite citet
+         amb1 amb2 Hanford)
+
+(define i 0)
+(define (exercise [id #f])
+  (set! i (+ i 1))
+  (when id (hash-set! ex-ids id i))
+  (element (style 'bold '()) 
+           (format "Exercise ~a" i)))
+(define ex-ids (make-hash))
+(define (exref id) (format "~a" (hash-ref ex-ids id)))
+
+(define (book-chapter-location
+          #:title title
+          #:author [author #f]
+          #:edition [edition #f]
+          #:publisher [publisher #f])
+   (let* ([s @italic{@(string-titlecase title)}]
+          [s (if edition
+                 @elem{@|s| @(string-titlecase edition) edition}
+                 s)]
+          [s (if author
+                 @elem{@|s| by @|author|}
+                 s)]
+          [s (if publisher
+                 (if s
+                     @elem{@|s|. @|publisher|}
+                     publisher)
+                 s)])
+     (unless s
+       (error 'book-chapter-location "no arguments"))
+     @elem{In @|s|}))
+
+(define-cite ~cite citet generate-bibliography)
+(define amb1
+   (make-bib #:title "A Basis for a Mathematical Theory of Computation"
+             #:author "John McCarthy"
+             #:location
+             (book-chapter-location #:title "Computer Programming and Formal Systems"
+                                    #:author (editor (authors "P. Braffort" "D. Hirschberg")))
+             #:date 1963))
+(define amb2
+   (make-bib #:title "Non-deterministic Lisp with dependency-directed backtracking"
+             #:author (authors "Ramin Zabih"
+                               "David McAllester"
+                               "David Chapman")
+             #:location (proceedings-location "Proceedings of the Sixth National Conference on Artificial Intelligence"
+                                              #:pages '(59 64))
+             #:date 1987))
+
+(define ibm-sys "IBM Systems Journal")
+(define Hanford
+  (make-bib
+   #:author (authors "Kenneth V. Hanford")
+   #:title "Automatic generation of test cases"
+   #:location (journal-location ibm-sys
+                                #:volume 9
+                                #:number "4"
+                                #:pages '(244 257))
+   #:date "1970"))

collects/redex/tests/run-tests.rkt

@@ -29,7 +29,8 @@
      "stepper-test.rkt"
      "defined-checks-test.rkt"
      "check-syntax-test.rkt"
-     "test-docs-complete.rkt")
+     "test-docs-complete.rkt"
+     "tut-subst-test.rkt")
    (if test-bitmaps? '("bitmap-test.rkt") '())
    (if test-examples?
        '("../examples/cbn-letrec.rkt"

collects/redex/tests/tut-subst-test.rkt

@@ -0,0 +1,52 @@
+#lang racket/base
+(require redex/reduction-semantics 
+         "../tut-subst.rkt"
+         racket/set)
+
+(define (an-x? x) (memq x '(a b c x y z z2 z2 q)))
+
+(test-equal (fvs an-x? (term (+ x a b))) (set 'x 'a 'b))
+(test-equal (fvs an-x? (term (λ (x num) (+ x y)))) (set 'y))
+(test-equal (fvs an-x? (term (λ (x num) (y num) (+ x y)))) (set))
+
+(define-language L)
+(define-metafunction L
+  [(subst (any_x any_b) ... any_body)
+   ,(subst/proc an-x? (term (any_x ...)) (term (any_b ...)) (term any_body))])
+
+(test-equal (term (subst (x y) x)) (term y))
+(test-equal (term (subst (x y) z)) (term z))
+(test-equal (term (subst (x y) (x (y z)))) (term (y (y z))))
+(test-equal (term (subst (x y) ((λ (x num) x) ((λ (y1 num) y1) (λ (x num) z)))))
+            (term ((λ (x num) x) ((λ (y1 num) y1) (λ (x num) z)))))
+(test-equal (term (subst (x y) (if0 (+ 1 x) x x)))
+            (term (if0 (+ 1 y) y y)))
+(test-equal (term (subst (x (λ (z num) y)) (λ (y num) x)))
+            (term (λ (y1 num) (λ (z num) y))))
+(test-equal (term (subst (x 1) (λ (y num) x)))
+            (term (λ (y num) 1)))
+(test-equal (term (subst (x y) (λ (y num) x)))
+            (term (λ (y1 num) y)))
+(test-equal (term (subst (x (λ (y num) y)) (λ (z num) (z2 z))))
+            (term (λ (z num) (z2 z))))
+(test-equal (term (subst (x (λ (z num) z)) (λ (z num) (z1 z))))
+            (term (λ (z num) (z1 z))))
+(test-equal (term (subst (x z) (λ (z num) (z1 z))))
+            (term (λ (z2 num) (z1 z2))))
+(test-equal (term (subst (x3 5) (λ (x2 num) x2)))
+            (term (λ (x2 num) x2)))
+(test-equal (term (subst (z *) (λ (z num) (x num) 1)))
+            (term (λ (z num) (x num) 1)))
+(test-equal (term (subst (q (λ (x num) z)) (λ (z num) (x num) q)))
+            (term (λ (z1 num) (x num) (λ (x num) z))))
+(test-equal (term (subst (x 1) (λ (x num) (x num) x)))
+            (term (λ (x num) (x num) x)))
+(test-equal (term (subst (x (y z)) (λ (z num) (z (x y)))))
+            (term (λ (z1 num) (z1 ((y z) y)))))
+(test-equal (term (subst (x 1) (λ (a (→ num (→ num num)))
+                                 (λ (b (→ num (→ num num)))
+                                   x))))
+            (term (λ (a (→ num (→ num num)))
+                    (λ (b (→ num (→ num num)))
+                      1))))
+(test-results)

collects/redex/tut-subst.rkt

@@ -0,0 +1,96 @@
+#lang racket/base
+
+#|
+
+The substitution function in this file has been designed
+to work with any expression language so long as the only
+binding form is λ and the shape of λ terms is:
+  
+      (λ (x t) ... e)
+
+|#
+
+(require racket/set racket/match
+         redex/reduction-semantics
+         rackunit)
+(provide subst/proc fvs)
+
+(define (subst/proc x? vars replacements body)
+  (define replacements-ht
+    (for/fold ([m (hash)])
+              ([v (in-list vars)]
+               [rep (in-list replacements)])
+      (hash-set m v rep)))
+  (define replacements-free-vars (for/list ([x (in-set (fvs x? replacements))]) x))
+  (define replacements-fresh-vars (variables-not-in (cons vars body) 
+                                                    replacements-free-vars))
+  (define init-fv-map 
+    (for/fold ([m (hash)])
+              ([fresh (in-list replacements-fresh-vars)]
+               [free (in-list replacements-free-vars)])
+      (hash-set m free fresh)))
+  (let loop ([body body]
+             [fvs-inactive init-fv-map]
+             [fvs-active (hash)]
+             [replacements replacements-ht])
+    (match body
+      [`(λ (,xs ,ts) ... ,body)
+       (define-values (new-xs new-inactive new-active new-replacements)
+         (adjust-active-inactive xs fvs-inactive fvs-active replacements))
+       `(λ ,@(map (λ (x t) `(,x ,t)) new-xs ts)
+          ,(loop body new-inactive new-active new-replacements))]
+      [(? x? x)
+       (cond
+         [(hash-ref fvs-active x #f) => values]
+         [(hash-ref replacements x #f) => values]
+         [else x])]
+      [(? list?)
+       (map (λ (x) (loop x fvs-inactive fvs-active replacements))
+            body)]
+      [_ body])))
+
+(define (adjust-active-inactive xs fvs-inactive fvs-active replacements)
+  (let loop ([xs xs]
+             [new-xs '()]
+             [fvs-inactive fvs-inactive]
+             [fvs-active fvs-active]
+             [replacements replacements])
+    (cond
+      [(null? xs)
+       (values (reverse new-xs)
+               fvs-inactive 
+               fvs-active
+               replacements)]
+      [else
+       (define x (car xs))
+       (define inactive-var? (hash-has-key? fvs-inactive x))
+       (define active-var? (hash-has-key? fvs-active x))
+       (define new-x
+         (cond
+           [inactive-var? (hash-ref fvs-inactive x)]
+           [active-var? (hash-ref fvs-active x)]
+           [else x]))
+       (loop (cdr xs)
+             (cons new-x new-xs)
+             (if inactive-var?
+                 (hash-remove fvs-inactive x)
+                 fvs-inactive)
+             (if inactive-var?
+                 (hash-set fvs-active x (hash-ref fvs-inactive x))
+                 fvs-active)
+             (if (hash-has-key? replacements x)
+                 (hash-remove replacements x)
+                 replacements))])))
+
+(define (fvs x? body)
+  (let loop ([body body])
+    (match body
+      [`(λ (,xs ,ts) ... ,body)
+       (set-subtract (loop body) (apply set xs))]
+      [(? x?)
+       (set body)]
+      [(? list?)
+       (for/fold ([fvs (set)])
+                 ([e (in-list body)])
+         (set-union fvs (loop e)))]
+      [_ (set)])))