remove extra tut-subst.rkt and tmp.rkt files

collects/redex/examples/tut-subst.rkt

@@ -1,96 +0,0 @@
-#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)])))

collects/redex/private/tmp.rkt

@@ -1,22 +0,0 @@
-#lang racket
-
-(require redex/reduction-semantics
-         redex/private/gen-trace
-         redex/private/search)
-
-(define-language L
-  (v a
-     b
-     c))
-
-(define-metafunction L
-  [(is-a? a)
-   T]
-  [(is-a? v)
-   F])
-
-(enable-gen-trace!)
-(test-equal (generate-term L #:satisfying
-                           (is-a? b) any
-                           +inf.0)
-            '((is-a? b) = F))