added a main.ss and got rid of planet dependencies and the old crufty subst
svn: r10976
This commit is contained in:
Robby Findler
parent
ba2036681b
commit
35abfba5b4
|
|
@ -10,12 +10,6 @@ This collection provides these files:
|
|||
|
||||
_pict.ss_: a library for _generating picts and postscript from semantics_
|
||||
|
||||
_subst.ss_: a library for _capture avoiding substitution_.
|
||||
|
||||
_generator.ss_: automatically generates terms from a language
|
||||
|
||||
_schemeunit.ss_: a _plt-redex specific library of schemeunit checks_.
|
||||
|
||||
In addition, the examples subcollection contains several
|
||||
small languages to demonstrate various different uses of
|
||||
this tool:
|
||||
|
|
@ -1353,141 +1347,6 @@ when being used to typeset.
|
|||
|
||||
======================================================================
|
||||
|
||||
The _subst.ss_ library provides these names:
|
||||
|
||||
> (subst (match-pattern subst-rhs ...) ...) SYNTAX
|
||||
|
||||
The result of this form is a function that performs capture
|
||||
avoiding substitution for a particular (sexp-based)
|
||||
language. The function accepts three arguments, a variable,
|
||||
a term to substitute and a term to substitute into.
|
||||
|
||||
Each of the `match-pattern's specify the forms of
|
||||
the language and the `subst-rhs's specify what kind of form
|
||||
it is. Each of the match-patterns are in (lib "match.ss"
|
||||
"match")'s pattern language and any variable that they bind
|
||||
are available in the <scheme-expression>'s described below.
|
||||
|
||||
The language of the subst-rhs follows.
|
||||
|
||||
> (variable)
|
||||
|
||||
this means that the rhs for this form is a symbol that
|
||||
should be treated like a variable. Nothing may follow
|
||||
this.
|
||||
|
||||
> (constant)
|
||||
|
||||
this means that the rhs for this form is a constant that
|
||||
cannot be renamed. Nothing may follow this.
|
||||
|
||||
> (all-vars <scheme-expression>)
|
||||
|
||||
This form indicates that this pattern in the language binds
|
||||
the variables produced by the
|
||||
<scheme-expression>.
|
||||
|
||||
Immediately following this in a subst-rhs must be a (build
|
||||
...) form and some number of (subterm ...) or (subterms ...)
|
||||
forms.
|
||||
|
||||
> (build <scheme-expression>)
|
||||
|
||||
This form must come right after an (all-vars ...) form and
|
||||
before any (subterm ...) or (subterms ...) forms.
|
||||
|
||||
This form tells subst how to reconstruct this term. The
|
||||
<scheme-expression> must evaluate to a procedure that
|
||||
accepts the (possibly renamed) variables from the all-vars
|
||||
clause, and one argument for each of the subterms that
|
||||
follow this declaration (with subterms flattened into the
|
||||
argument list) in the same order that the subterm or
|
||||
subterms declarations are listed.
|
||||
|
||||
> (subterm <scheme-expression> <scheme-expression>)
|
||||
|
||||
The first <scheme-expression> must be a list of variables
|
||||
that is a sub-list of the variables in the all-vars
|
||||
expression. The second expression must be an sexp
|
||||
corresponding to one of the subexpressions of this
|
||||
expression (matched by the match-patten for this clause of
|
||||
subst).
|
||||
|
||||
> (subterms <scheme-expression> <scheme-expression>)
|
||||
|
||||
The first <scheme-expression> must be a list of variables
|
||||
that is a sub-list of the variables in the all-vars
|
||||
expression. The second expression must be an sexp
|
||||
corresponding to one of the subexpressions of this
|
||||
expression (matched by the match-patten for this clause of
|
||||
subst).
|
||||
|
||||
Consider this example of a substitution procedure for the
|
||||
lambda calculus:
|
||||
|
||||
(define lc-subst
|
||||
(subst
|
||||
[`(lambda ,vars ,body)
|
||||
(all-vars vars)
|
||||
(build (lambda (vars body) `(lambda ,vars ,body)))
|
||||
(subterm vars body)]
|
||||
[(? symbol?) (variable)]
|
||||
[(? number?) (constant)]
|
||||
[`(,fun ,@(args ...))
|
||||
(all-vars '())
|
||||
(build (lambda (vars fun . args) `(,fun ,@args)))
|
||||
(subterm '() fun)
|
||||
(subterms '() args)]))
|
||||
|
||||
The first clause matches lambda expressions with any number
|
||||
of arguments and says that there is one subterm, the body of
|
||||
the lambda, and that all of the variables are bound in it.
|
||||
|
||||
The second clause matches symbols and indicates that they
|
||||
are variables.
|
||||
|
||||
The third clause matches numbers and indicates that they are
|
||||
constants.
|
||||
|
||||
The final clause matches function applications. The
|
||||
`all-vars' shows that applications introduce no new
|
||||
names. The build procedure reconstructs a new application
|
||||
form. The subterm declaration says that the function
|
||||
position is a subterm with no variables bound in it. The
|
||||
subterms declaration says that all of the arguments are
|
||||
subterms and that they do not introduce any new terms.
|
||||
|
||||
In this program, lc-subst is bound to a function that does
|
||||
the substitution. The first argument is the variable to
|
||||
substitute for, the second is the term to substitute and the
|
||||
final argument is the term to substitute into. For example,
|
||||
this call:
|
||||
|
||||
(lc-subst 'q
|
||||
'(lambda (x) y)
|
||||
'((lambda (y) (y q)) (lambda (y) y)))
|
||||
|
||||
produces this output:
|
||||
|
||||
'((lambda (y@) (y@ (lambda (x) y))) (lambda (y) y))
|
||||
|
||||
This library also provides:
|
||||
|
||||
> (plt-subst (match-pattern subst-rhs ...) ...) SYNTAX
|
||||
|
||||
This is identical to subst, described above, except that
|
||||
the pattern language used is that from (lib "plt-match.ss"),
|
||||
instead of (lib "match.ss").
|
||||
|
||||
> subst/proc
|
||||
> alpha-rename
|
||||
> free-vars/memoize
|
||||
|
||||
Theses functions are the procedure-based interface to
|
||||
substitution that subst expands to and uses.
|
||||
|
||||
======================================================================
|
||||
|
||||
The _iswim.ss_ module in the "examples" sub-collection defines a
|
||||
grammar and reductions from "Programming Languages and Lambda Calculi"
|
||||
by Felleisen and Flatt.
|
||||
|
|
@ -1595,85 +1454,3 @@ by Felleisen and Flatt.
|
|||
> delta*n :: (on? (listof V?) . -> . (union false? V?))
|
||||
delta as a function for any operation.
|
||||
|
||||
======================================================================
|
||||
|
||||
The _generator.ss_ module provides a tool for generating instances of
|
||||
a grammar non-terminal.
|
||||
|
||||
> lang->generator-table :: (lang?
|
||||
(listof number?)
|
||||
(listof symbol?)
|
||||
(listof string?)
|
||||
(listof symbol?)
|
||||
number?
|
||||
. -> .
|
||||
generator-table?)
|
||||
|
||||
Prepares generator information for a particular language,
|
||||
given a set of numbers to use for the `number' keyword,
|
||||
a set of symbols for `variable' and `variable-except',
|
||||
and a set of string for `string'.
|
||||
|
||||
The fifth argument lists keywords that appear in the grammar but
|
||||
that should be skipped (to limit the generation space). The last
|
||||
argument should be 0, and it is currently ignored.
|
||||
|
||||
> for-each-generated :: (generator-table?
|
||||
(any? number? . -> . any)
|
||||
generator-table?
|
||||
symbol?
|
||||
. -> . any)
|
||||
|
||||
The first argument is a procedure to call with a series of generated
|
||||
grammar instances and each term's size. Instances are generated from
|
||||
smallest to largest; the size of an instance is roughly the size of
|
||||
the proof tree that demonstrates grammar membership.
|
||||
|
||||
The second argument is a generator table created with
|
||||
`lang->generator-table'.
|
||||
|
||||
The third argument is a symbol, the name of a non-terminal for which
|
||||
instances should be generated.
|
||||
|
||||
> for-each-generated/size :: (generator-table?
|
||||
(any? number? . -> . any)
|
||||
generator-table?
|
||||
symbol?
|
||||
. -> . any)
|
||||
|
||||
Like `for-each-generated', except minimum and maximum sizes are
|
||||
provided, and the order of generation is arbitrary (i.e., some
|
||||
larger instances may be generated before smaller instances).
|
||||
|
||||
======================================================================
|
||||
|
||||
_schemeunit.ss_: This library provides two 'test's and two
|
||||
'check's (in Schemeunit terminology):
|
||||
|
||||
> (test-reduces reduction-relation term term)
|
||||
|
||||
This check reduces its second argument according to the
|
||||
reductions in the first argument, and compares it to the
|
||||
final argument. It expects the reductions to only produce
|
||||
a single result.
|
||||
|
||||
It uses apply-reduction-rule* to do the reductions (as above).
|
||||
|
||||
|
||||
> (check-reduces reduction-relation term term)
|
||||
|
||||
The 'check' version of test-reduces.
|
||||
|
||||
> (test-reduces/multiple reduction-relation term (listof term))
|
||||
|
||||
This check reduces its second argument according to the
|
||||
reductions in the first argument, and compares the
|
||||
results to the final argument. The reductions may produce
|
||||
multiple results and those results are expected to be the
|
||||
same as the list in the last argument.
|
||||
|
||||
It uses apply-reduction-relation* to do the reductions (as above).
|
||||
|
||||
> (check-reduces/multiple reduction-relation term (listof term))
|
||||
|
||||
The 'check' version of test-reduces/multiple.
|
||||
|
|
|
|||
|
|
@ -1,252 +0,0 @@
|
|||
#|
|
||||
|
||||
An attempt to automatically test reduction systems;
|
||||
this generates terms from a language automatically.
|
||||
|
||||
|#
|
||||
|
||||
(module generator mzscheme
|
||||
(require "private/matcher.ss")
|
||||
|
||||
(provide lang->generator-table
|
||||
for-each-generated
|
||||
for-each-generated/size)
|
||||
|
||||
(define (lang->generator-table lang
|
||||
nums
|
||||
vars
|
||||
strs
|
||||
skip-kws
|
||||
cache-limit)
|
||||
|
||||
;; -------------------- Cache implementation --------------------
|
||||
;; Cache is currently disabled. It's not clear that it's useful.
|
||||
(define (cache-small gen) gen)
|
||||
|
||||
;; -------------------- Build table --------------------
|
||||
;; The `gens' table maps non-terminal symbols to
|
||||
;; generator functions. A generator function conumes:
|
||||
;; * the min acceptable size of a generated element
|
||||
;; * the max acceptable size of a generated element
|
||||
;; * a sucess continuation proc that accepts
|
||||
;; - the generated value
|
||||
;; - the value's size
|
||||
;; - a generator proc that produces the next value;
|
||||
;; this proc expects to be given the same min, max,
|
||||
;; and fail continuation proc as before
|
||||
;; * a failure continuation thunk
|
||||
;;
|
||||
(let ([nts (compiled-lang-lang lang)]
|
||||
[nt-map (make-hash-table)])
|
||||
;; nt-map tells us which symbols are non-terminals; it also
|
||||
;; provides conservative min-size and max-size thunks that are
|
||||
;; refined as table generation proceeds
|
||||
(for-each (lambda (nt) (hash-table-put! nt-map (nt-name nt)
|
||||
(cons (lambda () 1)
|
||||
(lambda () +inf.0))))
|
||||
nts)
|
||||
;; gens is the main hash table
|
||||
(let ([gens (make-hash-table)]
|
||||
[atomic-alts (lambda (l size)
|
||||
(values
|
||||
(lambda (min-size max-size result-k fail-k)
|
||||
(let loop ([l l][result-k result-k][max-size max-size][fail-k fail-k])
|
||||
(if (<= min-size size max-size)
|
||||
(if (null? l)
|
||||
(fail-k)
|
||||
(result-k (car l)
|
||||
size
|
||||
(lambda (s xs result-k fail-k)
|
||||
(loop (cdr l) result-k xs fail-k))))
|
||||
(fail-k))))
|
||||
(lambda () size)
|
||||
(lambda () size)))]
|
||||
[to-do nts])
|
||||
(letrec ([make-gen/get-size
|
||||
(lambda (p)
|
||||
(cond
|
||||
[(hash-table-get nt-map p (lambda () #f))
|
||||
=> (lambda (get-sizes)
|
||||
(values
|
||||
(lambda (min-size max-size result-k fail-k)
|
||||
((hash-table-get gens p) min-size max-size result-k fail-k))
|
||||
(car get-sizes)
|
||||
(cdr get-sizes)))]
|
||||
[(eq? 'number p) (atomic-alts nums 1)]
|
||||
[(eq? 'string p) (atomic-alts strs 1)]
|
||||
[(eq? 'any p) (atomic-alts (append nums strs vars) 1)]
|
||||
[(or (eq? 'variable p)
|
||||
(and (pair? p)
|
||||
(eq? (car p) 'variable-except)))
|
||||
(atomic-alts vars 1)]
|
||||
[(symbol? p) ; not a non-terminal, because we checked above
|
||||
(if (memq p skip-kws)
|
||||
(values
|
||||
(lambda (min-size max-size result-k fail-k)
|
||||
(fail-k))
|
||||
(lambda () +inf.0)
|
||||
(lambda () -1))
|
||||
(atomic-alts (list p) 0))]
|
||||
[(null? p) (atomic-alts (list null) 0)]
|
||||
[(and (pair? p)
|
||||
(or (not (pair? (cdr p)))
|
||||
(not (eq? '... (cadr p)))))
|
||||
(make-pair-gen/get-size p cons)]
|
||||
[(and (pair? p) (pair? (cdr p)) (eq? '... (cadr p)))
|
||||
(let-values ([(just-rest just-rest-min-size just-rest-max-size)
|
||||
(make-gen/get-size (cddr p))]
|
||||
[(both both-min-size both-max-size)
|
||||
(make-pair-gen/get-size (cons (kleene+ (car p)) (cddr p)) append)])
|
||||
(values
|
||||
(lambda (min-size max-size result-k fail-k)
|
||||
(let loop ([both both][result-k result-k][max-size max-size][fail-k fail-k])
|
||||
(both min-size max-size
|
||||
(lambda (v size next-both)
|
||||
(result-k v size
|
||||
(lambda (ns xs result-k fail-k)
|
||||
(loop next-both result-k xs fail-k))))
|
||||
(lambda ()
|
||||
(just-rest min-size max-size result-k fail-k)))))
|
||||
just-rest-min-size
|
||||
(lambda () +inf.0)))]
|
||||
[else
|
||||
(error 'make-gen "unrecognized pattern: ~e" p)]))]
|
||||
[make-pair-gen/get-size
|
||||
(lambda (p combiner)
|
||||
(let*-values ([(first first-min-size first-max-size)
|
||||
(make-gen/get-size (car p))]
|
||||
[(rest rest-min-size rest-max-size)
|
||||
(make-gen/get-size (cdr p))]
|
||||
[(this-min-size) (let ([v #f])
|
||||
(lambda ()
|
||||
(unless v
|
||||
(set! v (+ (first-min-size)
|
||||
(rest-min-size))))
|
||||
v))]
|
||||
[(this-max-size) (let ([v #f])
|
||||
(lambda ()
|
||||
(unless v
|
||||
(set! v (+ (first-max-size)
|
||||
(rest-max-size))))
|
||||
v))])
|
||||
(values
|
||||
(cache-small
|
||||
(lambda (min-size max-size result-k fail-k)
|
||||
(if (min-size . > . (this-max-size))
|
||||
(fail-k)
|
||||
(let rloop ([rest rest][result-k result-k][max-size max-size][fail-k fail-k][failed-size +inf.0])
|
||||
(if (max-size . < . (this-min-size))
|
||||
(fail-k)
|
||||
(rest
|
||||
(max 0 (- min-size (first-max-size)))
|
||||
(min (sub1 failed-size) (- max-size (first-min-size)))
|
||||
(lambda (rest rest-size next-rest)
|
||||
(if (rest-size . >= . failed-size)
|
||||
(rloop next-rest result-k max-size fail-k failed-size)
|
||||
(let floop ([first first]
|
||||
[result-k result-k]
|
||||
[max-size max-size]
|
||||
[fail-k fail-k]
|
||||
[first-fail-k (lambda ()
|
||||
(rloop next-rest result-k max-size fail-k rest-size))])
|
||||
(first (max 0 (- min-size rest-size))
|
||||
(- max-size rest-size)
|
||||
(lambda (first first-size next-first)
|
||||
(result-k
|
||||
(combiner first rest)
|
||||
(+ first-size rest-size)
|
||||
(lambda (ns xs result-k fail-k)
|
||||
(floop next-first result-k xs fail-k
|
||||
(lambda ()
|
||||
(rloop next-rest result-k xs fail-k failed-size))))))
|
||||
first-fail-k))))
|
||||
fail-k))))))
|
||||
this-min-size
|
||||
this-max-size)))]
|
||||
[kleene+ (lambda (p)
|
||||
(let ([n (gensym)])
|
||||
(hash-table-put! nt-map n (cons (lambda () 1)
|
||||
(lambda () +inf.0)))
|
||||
(set! to-do (cons (make-nt
|
||||
n
|
||||
(list (make-rhs (cons p '()))
|
||||
(make-rhs (cons p n))))
|
||||
to-do))
|
||||
n))])
|
||||
(let to-do-loop ([nts (reverse to-do)])
|
||||
(set! to-do null)
|
||||
(for-each (lambda (nt)
|
||||
(hash-table-put!
|
||||
gens
|
||||
(nt-name nt)
|
||||
(let* ([gens+sizes
|
||||
(map (lambda (rhs)
|
||||
(let-values ([(gen get-min-size get-max-size)
|
||||
(make-gen/get-size
|
||||
(rhs-pattern rhs))])
|
||||
(cons gen (cons get-min-size get-max-size))))
|
||||
(nt-rhs nt))]
|
||||
[get-min-size
|
||||
(let ([get-min-sizes (map cadr gens+sizes)])
|
||||
(let ([v #f])
|
||||
(lambda ()
|
||||
(unless v
|
||||
(set! v (add1
|
||||
(apply min (map (lambda (gs) (gs))
|
||||
get-min-sizes)))))
|
||||
v)))]
|
||||
[get-max-size
|
||||
(let ([get-max-sizes (map cddr gens+sizes)])
|
||||
(let ([v #f])
|
||||
(lambda ()
|
||||
(unless v
|
||||
(set! v (add1
|
||||
(apply max (map (lambda (gs) (gs))
|
||||
get-max-sizes)))))
|
||||
v)))])
|
||||
(hash-table-put! nt-map (nt-name nt)
|
||||
(cons get-min-size get-max-size))
|
||||
(cache-small
|
||||
(lambda (min-size max-size result-k fail-k)
|
||||
(if (min-size . > . (get-max-size))
|
||||
(fail-k)
|
||||
(let loop ([l (map car gens+sizes)][result-k result-k][max-size max-size][fail-k fail-k])
|
||||
(if (max-size . < . (get-min-size))
|
||||
(fail-k)
|
||||
(if (null? l)
|
||||
(fail-k)
|
||||
(let iloop ([alt-next (car l)]
|
||||
[result-k result-k]
|
||||
[max-size max-size]
|
||||
[fail-k fail-k])
|
||||
(alt-next
|
||||
(max 0 (sub1 min-size))
|
||||
(sub1 max-size)
|
||||
(lambda (alt a-size alt-next)
|
||||
(result-k
|
||||
alt
|
||||
(add1 a-size)
|
||||
(lambda (ns xs result-k fail-k)
|
||||
(iloop alt-next result-k xs fail-k))))
|
||||
(lambda ()
|
||||
(loop (cdr l) result-k max-size fail-k)))))))))))))
|
||||
nts)
|
||||
(unless (null? to-do)
|
||||
(to-do-loop to-do))))
|
||||
gens)))
|
||||
|
||||
(define (for-each-generated/size proc gens min-size max-size nonterm)
|
||||
(let ([gen (hash-table-get gens nonterm)])
|
||||
(let loop ([gen gen])
|
||||
(gen
|
||||
min-size
|
||||
max-size
|
||||
(lambda (val z1 gen-next)
|
||||
(proc val z1)
|
||||
(loop gen-next))
|
||||
void))))
|
||||
|
||||
(define (for-each-generated proc gens nonterm)
|
||||
(let loop ([i 0])
|
||||
(for-each-generated/size proc gens i i nonterm)
|
||||
(loop (add1 i)))))
|
||||
7
collects/redex/main.ss
Normal file
7
collects/redex/main.ss
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
#lang scheme/base
|
||||
(require "reduction-semantics.ss"
|
||||
"gui.ss"
|
||||
"pict.ss")
|
||||
(provide (all-from-out "reduction-semantics.ss"
|
||||
"gui.ss"
|
||||
"pict.ss"))
|
||||
|
|
@ -1,43 +0,0 @@
|
|||
#lang scheme
|
||||
|
||||
(require (planet "test.ss" ("schematics" "schemeunit.plt" 2))
|
||||
(except-in "reduction-semantics.ss" check))
|
||||
|
||||
(provide test-reduces
|
||||
check-reduces
|
||||
test-reduces/multiple
|
||||
check-reduces/multiple)
|
||||
|
||||
(define-shortcut (test-reduces reds from to) (check-reduces reds from to))
|
||||
|
||||
(define-check (check-reduces reds from to)
|
||||
(let ([all (apply-reduction-relation* reds from)])
|
||||
(cond
|
||||
[(null? (cdr all))
|
||||
(unless (equal? (car all) to)
|
||||
(with-check-info
|
||||
(('expected to)
|
||||
('actual (car all)))
|
||||
(fail-check)))]
|
||||
[else
|
||||
(with-check-info
|
||||
(('multiple-results all))
|
||||
(fail-check))])))
|
||||
|
||||
(define-shortcut (test-reduces/multiple reds from to) (check-reduces/multiple reds from to))
|
||||
|
||||
(define-check (check-reduces/multiple reds from to)
|
||||
(let ([all (apply-reduction-relation* reds from)])
|
||||
(unless (set-equal? all to)
|
||||
(with-check-info
|
||||
(('expecteds to)
|
||||
('actuals all))
|
||||
(fail-check)))))
|
||||
|
||||
(define (set-equal? s1 s2)
|
||||
(define (subset? a b)
|
||||
(let ([ht (make-hash)])
|
||||
(for-each (λ (x) (hash-set! ht x #t)) a)
|
||||
(andmap (λ (x) (hash-ref ht x #f)) b)))
|
||||
(and (subset? s1 s2)
|
||||
(subset? s2 s1)))
|
||||
|
|
@ -1,292 +0,0 @@
|
|||
(module subst mzscheme
|
||||
(require (lib "match.ss")
|
||||
(prefix plt: (lib "plt-match.ss"))
|
||||
(lib "list.ss"))
|
||||
|
||||
(provide plt-subst subst
|
||||
all-vars variable subterm subterms constant build
|
||||
subst/proc alpha-rename free-vars/memoize)
|
||||
|
||||
(define-syntax (all-vars stx) (raise-syntax-error 'subst "all-vars out of context" stx))
|
||||
(define-syntax (variable stx) (raise-syntax-error 'subst "variable out of context" stx))
|
||||
(define-syntax (subterm stx) (raise-syntax-error 'subst "subterm out of context" stx))
|
||||
(define-syntax (subterms stx) (raise-syntax-error 'subst "subterms out of context" stx))
|
||||
(define-syntax (constant stx) (raise-syntax-error 'subst "constant out of context" stx))
|
||||
(define-syntax (build stx) (raise-syntax-error 'subst "build out of context" stx))
|
||||
|
||||
(define-syntax (make-subst stx)
|
||||
(syntax-case stx ()
|
||||
[(_ subst match)
|
||||
(syntax
|
||||
(define-syntax (subst stx)
|
||||
(syntax-case stx ()
|
||||
[(_ (pat rhs (... ...)) (... ...))
|
||||
(with-syntax ([term/arg #'term/arg]
|
||||
[constant/arg #'constant/arg]
|
||||
[variable/arg #'variable/arg]
|
||||
[combine/arg #'combine/arg]
|
||||
[sub-piece/arg #'subpiece/arg])
|
||||
(define (handle-rhs rhs-stx)
|
||||
(syntax-case rhs-stx (all-vars build subterm subterms variable constant)
|
||||
[((all-vars all-vars-exp) (build build-exp) sub-pieces (... ...))
|
||||
(with-syntax ([(sub-pieces (... ...))
|
||||
(map (lambda (subterm-stx)
|
||||
(syntax-case subterm-stx (subterm subterms)
|
||||
[(subterm vars body) (syntax (list (sub-piece/arg vars body)))]
|
||||
[(subterms vars terms)
|
||||
(syntax
|
||||
(let ([terms-var terms])
|
||||
(unless (list? terms-var)
|
||||
(error 'subst
|
||||
"expected a list of terms for `subterms' subclause, got: ~e"
|
||||
terms-var))
|
||||
(map (lambda (x) (sub-piece/arg vars x))
|
||||
terms-var)))]
|
||||
[else (raise-syntax-error
|
||||
'subst
|
||||
"unknown all-vars subterm"
|
||||
stx
|
||||
subterm-stx)]))
|
||||
(syntax->list (syntax (sub-pieces (... ...)))))])
|
||||
(syntax
|
||||
(apply combine/arg
|
||||
build-exp
|
||||
all-vars-exp
|
||||
(append sub-pieces (... ...)))))]
|
||||
[((all-vars) sub-pieces (... ...))
|
||||
(raise-syntax-error 'subst "expected all-vars must have an argument" stx rhs-stx)]
|
||||
[((all-vars all-vars-exp) not-build-clause anything (... ...))
|
||||
(raise-syntax-error 'subst "expected build clause" (syntax not-build-clause))]
|
||||
[((all-vars all-vars-exp))
|
||||
(raise-syntax-error 'subst "missing build clause" (syntax (all-vars all-vars-exp)))]
|
||||
[((constant))
|
||||
(syntax (constant/arg term/arg))]
|
||||
[((variable))
|
||||
(syntax (variable/arg (lambda (x) x) term/arg))]
|
||||
[(unk unk-more (... ...))
|
||||
(raise-syntax-error 'subst "unknown clause" (syntax unk))]))
|
||||
(with-syntax ([(expanded-rhs (... ...))
|
||||
(map handle-rhs (syntax->list (syntax ((rhs (... ...)) (... ...)))))])
|
||||
(syntax
|
||||
(let ([separate
|
||||
(lambda (term/arg constant/arg variable/arg combine/arg sub-piece/arg)
|
||||
(match term/arg
|
||||
[pat expanded-rhs] (... ...)
|
||||
[else (error 'subst "no matching clauses for ~s\n" term/arg)]))])
|
||||
(lambda (var val exp)
|
||||
(subst/proc var val exp separate))))))])))]))
|
||||
|
||||
(make-subst subst match)
|
||||
(make-subst plt-subst plt:match)
|
||||
|
||||
(define (subst/proc var val exp separate)
|
||||
(let* ([free-vars-cache (make-hash-table 'equal)]
|
||||
[fv-val (free-vars/memoize free-vars-cache val separate)])
|
||||
(let loop ([exp exp])
|
||||
(let ([fv-exp (free-vars/memoize free-vars-cache exp separate)]
|
||||
[handle-constant
|
||||
(lambda (x) x)]
|
||||
[handle-variable
|
||||
(lambda (rebuild var-name)
|
||||
(if (equal? var-name var)
|
||||
val
|
||||
(rebuild var-name)))]
|
||||
[handle-complex
|
||||
(lambda (maker vars . subpieces)
|
||||
(cond
|
||||
[(ormap (lambda (var) (memq var fv-val)) vars)
|
||||
=>
|
||||
(lambda (to-be-renamed-l)
|
||||
(let ([to-be-renamed (car to-be-renamed-l)])
|
||||
(loop
|
||||
(alpha-rename
|
||||
to-be-renamed
|
||||
(pick-new-name to-be-renamed (cons to-be-renamed fv-val))
|
||||
exp
|
||||
separate))))]
|
||||
[else
|
||||
(apply maker
|
||||
vars
|
||||
(map (lambda (subpiece)
|
||||
(let ([sub-term-binders (subpiece-binders subpiece)]
|
||||
[sub-term (subpiece-term subpiece)])
|
||||
(if (memq var sub-term-binders)
|
||||
sub-term
|
||||
(loop sub-term))))
|
||||
subpieces))]))])
|
||||
(if (member var fv-exp)
|
||||
(separate
|
||||
exp
|
||||
handle-constant
|
||||
handle-variable
|
||||
handle-complex
|
||||
make-subpiece)
|
||||
exp)))))
|
||||
|
||||
(define-struct subpiece (binders term) (make-inspector))
|
||||
|
||||
;; alpha-rename : symbol symbol term separate -> term
|
||||
;; renames the occurrences of to-be-renamed that are
|
||||
;; bound in the "first level" of exp.
|
||||
(define (alpha-rename to-be-renamed new-name exp separate)
|
||||
(define (first exp)
|
||||
(separate exp
|
||||
first-handle-constant
|
||||
first-handle-variable
|
||||
first-handle-complex
|
||||
first-handle-complex-subpiece))
|
||||
(define (first-handle-constant x) x)
|
||||
(define (first-handle-variable rebuild var) (rebuild var))
|
||||
(define (first-handle-complex maker vars . subpieces)
|
||||
(let ([replaced-vars
|
||||
(map (lambda (x) (if (eq? x to-be-renamed) new-name x))
|
||||
vars)])
|
||||
(apply maker replaced-vars subpieces)))
|
||||
(define (first-handle-complex-subpiece binders subterm)
|
||||
(if (memq to-be-renamed binders)
|
||||
(beyond-first subterm)
|
||||
subterm))
|
||||
|
||||
(define (beyond-first exp)
|
||||
(define (handle-constant x) x)
|
||||
(define (handle-variable rebuild var)
|
||||
(if (eq? var to-be-renamed)
|
||||
(rebuild new-name)
|
||||
(rebuild var)))
|
||||
(define (handle-complex maker vars . subpieces)
|
||||
(apply maker vars subpieces))
|
||||
(define (handle-complex-subpiece binders subterm)
|
||||
(if (memq to-be-renamed binders)
|
||||
subterm
|
||||
(beyond-first subterm)))
|
||||
(separate
|
||||
exp
|
||||
handle-constant
|
||||
handle-variable
|
||||
handle-complex
|
||||
handle-complex-subpiece))
|
||||
|
||||
(first exp))
|
||||
|
||||
;; free-vars/memoize : hash-table[sexp -o> (listof symbols)] sexp separate -> (listof symbols)
|
||||
;; doesn't cache against separate -- if it changes, a new hash-table must be passed in,
|
||||
;; or the caching will be wrong
|
||||
(define (free-vars/memoize cache exp separate)
|
||||
(hash-table-get
|
||||
cache
|
||||
exp
|
||||
(lambda ()
|
||||
(let ([res (free-vars/compute cache exp separate)])
|
||||
(hash-table-put! cache exp res)
|
||||
res))))
|
||||
|
||||
;; free-vars/memoize : hash-table[sexp -o> (listof symbols)] sexp separate -> (listof symbols)
|
||||
(define (free-vars/compute cache exp separate)
|
||||
(let ([handle-constant (lambda (x) '())]
|
||||
[handle-variable (lambda (rebuild var) (list var))]
|
||||
[handle-complex
|
||||
(lambda (maker vars . subpieces)
|
||||
(apply append subpieces))]
|
||||
[handle-complex-subpiece
|
||||
(lambda (binders subterm)
|
||||
(foldl remove-all
|
||||
(free-vars/memoize cache subterm separate)
|
||||
binders))])
|
||||
(separate
|
||||
exp
|
||||
handle-constant
|
||||
handle-variable
|
||||
handle-complex
|
||||
handle-complex-subpiece)))
|
||||
|
||||
(define (remove-all var lst)
|
||||
(let loop ([lst lst]
|
||||
[ans '()])
|
||||
(cond
|
||||
[(null? lst) ans]
|
||||
[else (if (eq? (car lst) var)
|
||||
(loop (cdr lst) ans)
|
||||
(loop (cdr lst) (cons (car lst) ans)))])))
|
||||
|
||||
(define (lc-direct-subst var val exp)
|
||||
(let ([fv-exp (lc-direct-free-vars exp)])
|
||||
(if (memq var fv-exp)
|
||||
(match exp
|
||||
[`(lambda ,vars ,body)
|
||||
(if (memq var vars)
|
||||
exp
|
||||
(let* ([fv-val (lc-direct-free-vars val)]
|
||||
[vars1 (map (lambda (var) (pick-new-name var fv-val)) vars)])
|
||||
`(lambda ,vars1 ,(lc-direct-subst
|
||||
var
|
||||
val
|
||||
(lc-direct-subst/l vars
|
||||
vars1
|
||||
body)))))]
|
||||
[`(let (,l-var ,exp) ,body)
|
||||
(if (eq? l-var var)
|
||||
`(let (,l-var ,(lc-direct-subst var val exp)) ,body)
|
||||
(let* ([fv-val (lc-direct-free-vars val)]
|
||||
[l-var1 (pick-new-name l-var fv-val)])
|
||||
`(let (,l-var1 ,(lc-direct-subst var val exp))
|
||||
,(lc-direct-subst
|
||||
var
|
||||
val
|
||||
(lc-direct-subst
|
||||
l-var
|
||||
l-var1
|
||||
body)))))]
|
||||
[(? number?) exp]
|
||||
[(and var1 (? symbol?))
|
||||
(if (eq? var1 var)
|
||||
val
|
||||
var1)]
|
||||
[`(,@(args ...))
|
||||
`(,@(map (lambda (arg) (lc-direct-subst var val arg)) args))])
|
||||
exp)))
|
||||
|
||||
;; lc-direct-subst/l : (listof symbol) (listof symbol) (listof symbol) sexp -> exp
|
||||
;; substitutes each of vars with vals in exp
|
||||
;; [assume vals don't contain any vars]
|
||||
(define (lc-direct-subst/l vars vals exp)
|
||||
(foldr (lambda (var val exp) (lc-direct-subst var val exp))
|
||||
exp
|
||||
vars
|
||||
vals))
|
||||
|
||||
;; lc-direct-free-vars : sexp -> (listof symbol)
|
||||
;; returns the free variables in exp
|
||||
(define (lc-direct-free-vars exp)
|
||||
(let ([ht (make-hash-table)])
|
||||
(let loop ([exp exp]
|
||||
[binding-vars null])
|
||||
(match exp
|
||||
[(? symbol?)
|
||||
(unless (memq exp binding-vars)
|
||||
(hash-table-put! ht exp #t))]
|
||||
[(? number?)
|
||||
(void)]
|
||||
[`(lambda ,vars ,body)
|
||||
(loop body (append vars binding-vars))]
|
||||
[`(let (,var ,exp) ,body)
|
||||
(loop exp binding-vars)
|
||||
(loop body (cons var binding-vars))]
|
||||
[`(,@(args ...))
|
||||
(for-each (lambda (arg) (loop arg binding-vars)) args)]))
|
||||
(hash-table-map ht (lambda (x y) x))))
|
||||
|
||||
;; pick-new-name : symbol (listof symbol) -> symbol
|
||||
;; returns a primed version of `var' that does
|
||||
;; not occur in vars (possibly with no primes)
|
||||
(define (pick-new-name var vars)
|
||||
(if (member var vars)
|
||||
(pick-new-name (prime var) vars)
|
||||
var))
|
||||
|
||||
;; prime : symbol -> symbol
|
||||
;; adds an @ at the end of the symbol
|
||||
(define (prime var)
|
||||
(string->symbol
|
||||
(string-append
|
||||
(symbol->string var)
|
||||
"@"))))
|
||||
Loading…
Reference in New Issue
Block a user