From 484636d92ed95096cafb5ee79c2b68f562cc4c0f Mon Sep 17 00:00:00 2001 From: Burke Fetscher Date: Wed, 17 Oct 2012 23:24:44 -0500 Subject: [PATCH] remove extra tut-subst.rkt and tmp.rkt files --- collects/redex/examples/tut-subst.rkt | 96 --------------------------- collects/redex/private/tmp.rkt | 22 ------ 2 files changed, 118 deletions(-) delete mode 100644 collects/redex/examples/tut-subst.rkt delete mode 100644 collects/redex/private/tmp.rkt diff --git a/collects/redex/examples/tut-subst.rkt b/collects/redex/examples/tut-subst.rkt deleted file mode 100644 index a61717da49..0000000000 --- a/collects/redex/examples/tut-subst.rkt +++ /dev/null @@ -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)]))) diff --git a/collects/redex/private/tmp.rkt b/collects/redex/private/tmp.rkt deleted file mode 100644 index 5b9674b9cd..0000000000 --- a/collects/redex/private/tmp.rkt +++ /dev/null @@ -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))