suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

removed reduction-semantics collection

Browse Source 
svn: r1791
This commit is contained in:
Robby Findler 2006-01-09 18:09:28 +00:00
parent 74a5a3efd5
commit 179f9ce01d
32 changed files with 0 additions and 8851 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

930
collects/reduction-semantics/doc.txt
View File

@ -1,930 +0,0 @@
_Reduction Semantics_
_reduction-semantics_
This collection provides three files:
_reduction-semantics.ss_: the core reduction semantics
library
_gui.ss_: a _visualization tool for reduction sequences_.
_subst.ss_: a library for _capture avoiding substitution_.
In addition, the examples subcollection contains several
small languages to demonstrate various different uses of
this tool:
_arithmetic.ss_: an arithmetic language with every
possible order of evaluation
_church.ss_: church numerals with call by name
normal order evaluation
_combinators.ss_: fills in the gaps in a proof in
Berendrecht that i and j (defined in the file) are
a combinator basis
_future.ss_: an adaptation of Cormac Flanagan's future
semantics.
_ho-contracts.ss_: computes the mechanical portions of a
proof in the Contracts for Higher Order Functions paper
(ICFP 2002). Contains a sophisticated example use of an
alternative pretty printer.
_macro.ss_: models macro expansion as a reduction semantics.
_omega.ss_: the call by value lambda calculus with call/cc.
Includes omega and two call/cc-based infinite loops, one of
which has an ever-expanding term size and one of which has
a bounded term size.
_threads.ss_: shows how non-deterministic choice can be
modeled in a reduction semantics. Contains an example use
of a simple alternative pretty printer.
_semaphores.ss_: a simple threaded language with semaphores
iswim.ss : see further below.
======================================================================
The _reduction-semantics.ss_ library defines a pattern
language, used in various ways:
pattern = any
| number
| string
| variable
| (variable-except <symbol> ...)
| hole
| (hole <symbol>)
| <symbol>
| (name <symbol> <pattern>)
| (in-hole <pattern> <pattern>)
| (in-named-hole <symbol> <symbol> <pattern> <pattern>)
| (side-condition <pattern> <guard>)
| (cross <symbol>>)
| (pattern ...)
| <scheme-constant>
The patterns match sexpressions. The _any_ pattern matches
any sepxression. The _number_ pattern matches any
number. The _string_ pattern matches any string. Those three
patterns may also be suffixed with an underscore and another
identifier, in which case they bind the full name (as if it
were an implicit `name' pattern) and match the portion
before the underscore.
The _variable_ pattern matches any symbol. The
_variable-except_ pattern matches any variable except those
listed in its argument. This is useful for ensuring that
keywords in the language are not accidentally captured by
variables.
The _hole_ pattern matches anything when inside a matching
in-hole pattern. The (hole <symbol>) variation on that
pattern is used in conjunction with in-named-hole to support
languages that require multiple patterns in a hole.
The _<symbol>_ pattern stands for a literal symbol that must
match exactly, unless it is the name of a non-terminal in a
relevant language or contains an underscore.
If it is a non-terminal, it matches any of the right-hand
sides of that non-terminal.
If the symbol is a non-terminal followed by an underscore,
for example e_1, it is implicitly the same as a name pattern
that matches only the non-terminal, (name e_1 e) for the
example. If the symbol otherwise has an underscore, it is
an error.
_name_: The pattern:
(name <symbol> <pattern>)
matches <pattern> and binds using it to the name <symbol>.
_in-hole_: The (in-hole <pattern> <pattern>) matches the first
pattern. This match must include exactly one match against the `hole'
pattern. The `hole' pattern matches any sexpression. Then, the
sexpression that matched the hole pattern is used to match against the
second pattern.
_in-named-hole_: The pattern:
(in-named-hole <symbol> <pattern> <pattern>)
is similar in spirit to in-hole, except that it supports
languages with multiple holes in a context. The first
argument identifies which hole, using the (hole <symbol>)
pattern that this expression requires and the rest of the
arguments are just like in-hole. That is, if there are
multiple holes in a term, each matching a different (hole
<name>) pattern, this one selects only the holes that are
named by the first argument to in-named-hole.
_side-condition_: The (side-condition pattern guard) pattern matches
what the embedded pattern matches, and then the guard expression is
evaluated. If it returns #f, the pattern fails to match, and if it
returns anything else, the pattern matches. In addition, any
occurrences of `name' in the pattern are bound using `term-let'
(see below) in the guard.
_cross_: The (cross <symbol>) pattern is used for the compatible
closure functions. If the language contains a non-terminal with the
same name as <symbol>, the pattern (cross <symbol>) matches the
context that corresponds to the compatible closure of that
non-terminal.
The (pattern ...) pattern matches a sexpression list, where
each pattern matches an element of the list. In addition, if
a list pattern contains an ellipses that is not treated as a
literal, instead it matches any number of duplications of the
pattern that came before the ellipses (including 0). Furthermore,
each (name <symbol> <pattern>) in the duplicated pattern
binds a list of matches to <symbol>, instead of a single match.
(A nested duplicated pattern creates a list of list matches,
etc.) Ellipses may be placed anywhere inside the row of
patterns, except in the first position or immediately after
another ellipses. Multiple ellipses are allowed.
> (language (non-terminal pattern ...) ...) SYNTAX
This form defines a context-free language. As an example,
this is the lambda calculus:
(define lc-lang
(language (e (e e ...)
variable
v)
(c (v ... c e ...)
hole)
(v (lambda (variable ...) e))))
with non-terminals e for the expression language, c for the
evaluation contexts and v for values.
> compiled-lang? : (any? . -> . boolean?)
Returns #t if its argument was produced by `language', #f
otherwise.
> (term-let ([tl-pat expr] ...) body) SYNTAX
Matches each given id pattern to the value yielded by
evaluating the corresponding expr and binds each variable in
the id pattern to the appropriate value (described
below). These bindings are then accessible to the `term'
syntactic form.
Identifier-patterns are terms in the following grammar:
tl-pat ::= identifier
| (tl-pat-ele ...)
tl-pat-ele ::= tl-pat
| tl-pat ellipses
where ellipses is the literal symbol consisting of three
dots (and the ... indicates repetition as usual). If tl-pat
is an identifier, it matches any value and binds it to the
identifier, for use inside `term'. If it is a list, it
matches only if the value being matched is a list value and
only if every subpattern recursively matches the
corresponding list element. There may be a single ellipsis
in any list pattern; if one is present, the pattern before
the ellipses may match multiple adjacent elements in the
list value (possibly none).
> (term s-expr) SYNTAX
This form is used for construction of new s-expressions in
the right-hand sides of reductions. It behaves identically
to quasiquote except that names bound by `term-let' are
implicitly substituted with the values that those names were
bound to, expanding ellipses as in-place sublists (in the
same manner as syntax-case patterns).
For example,
(term-let ([body '(+ x 1)]
[(expr ...) '(+ - (values * /))]
[((id ...) ...) '((a) (b) (c d))])
(term (let-values ([(id ...) expr] ...) body)))
evaluates to
'(let-values ([(a) +]
[(b) -]
[(c d) (values * /)])
(+ x 1))
It is an error for a term variable to appear in an
expression with an ellipsis-depth different from the depth
with which it was bound by `term-let'. It is also an error
for two `term-let'-bound identifiers bound to lists of
different lengths to appear together inside an ellipsis.
> (reduction 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
the last bodies are expressions that must evaluate to a new
sexpression corresponding to the reduct for this term. The
bodies are implicitly wrapped in a begin.
As an example, the reduction for the lambda calculus above
would be written like this:
(reduction lc-lang
(in-hole (name c c)
((lambda (variable_i ...) e_body)
v_i ...))
(plug
(term c)
(foldl lc-subst (term e_body)
(term (v_i ...))
(term (variable_i ...)))))
The in-hole pattern matches a term against `c', and binds
what matches the hole to `hole'. Then, it matches what
matched the hole against ((lambda (variable) e) v).
Because of the name pattern and the subscripted variable names
we used, c, hole, variable_i, e_body, and v_i
are bound with `term-let' in the right hand side of the
reduction. Then, when the reduction matches, the result is
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. The
names are used by `traces'.
> (reduction/context 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
`plug'. The equivalent reduction/context to the above
example is this:
(reduction/context
lang
c
((lambda (variable_i ...) e_body) v_i ...)
(lc-subst (term (variable_i ...))
(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?)
Returns #t if its argument is a reduction (produced by `reduction',
`reduction/context', etc.), #f otherwise.
> compatible-closure : (red?
compiled-lang?
symbol?
. -> .
red?)
This function accepts a reduction, a language, the name of a
non-terminal in the language and returns the compatible
closure of the reduction for the specified non-terminal.
> context-closure : (red?
compiled-lang?
any
. -> .
red?)
This function accepts a reduction, a language, a pattern
representing a context (ie, that can be used as the first
argument to `in-hole'; often just a non-terminal) in the
language and returns the closure of the reduction
in that context.
> plug : (any? any? . -> . any)
The first argument to this function is an sexpression to
plug into. The second argument is the sexpression to replace
in the first argument. It returns the replaced term.
> reduce : ((listof red?) any? . -> . (listof any?))
Reduce accepts a list of reductions, a term, and returns a
list of terms that the term reduces to.
> language->predicate : (compiled-lang?
symbol?
. -> .
(any? . -> . boolean?))
Takes a language and a non-terminal name and produces
a predicate that matches instances of the non-terminal.
> match-pattern : (compiled-pattern
any/c
. -> .
(union false? (listof mtch?)))
This is mostly used to explore a particular pattern to
determine what is going wrong. It accepts a compiled pattern
and a and returns #f if the pattern doesn't match the term,
and returns a list of mtch structure if the terms do match.
> compile-pattern : (compiled-lang? any? . -> . compiled-pattern)
This is mostly used in conjunction with match-pattern to
explore particular patterns and terms when debugging. It
compiles a sexpression pattern to a pattern.
> mtch? : (any/c . -> . boolean?)
Determines if a value is a mtch structure.
> mtch-bindings : (mtch? -> bindings?)
This returns a bindings structure (see below) that
binds the pattern variables in this match.
> mtch-context : (mtch? . -> . any/c)
Returns the current context being built up for a
match. Usually, this is the same as the original term being
matched.
> mtch-hole : (mtch? . -> . (union none? any/c))
Returns the current contents of the hole for this match (if
there was a decomposition). Usually returns none.
> variable-not-in : (any? symbol? . -> . symbol?)
This helper function accepts an sexpression and a
variable. It returns a variable not in the sexpression with
a prefix the same as the second argument.
> make-bindings : ((listof rib?) . -> . bindings?)
> bindings? : (any? . -> . boolean?)
> bindings-table : (bindings? . -> . (listof rib?))
Constructor, predicate, and selector functions for the bindings values
returned by match-pattern. Each bindings value represents the bindings
established for a single parse of the term; multiple such parses may be
possible in some situations.
> make-rib : (symbol? any? . -> . rib?)
> rib? : (any? . -> . boolean?)
> rib-name : (rib? . -> . symbol?)
> rib-exp : (rib? . -> . any?)
Constructor, predicate, and selector functions for the rib values contained
within a bindings. Each rib associates a name with an s-expression from
the language, or a list of such s-expressions, if the (name ...) clause is
followed by an ellipsis. Nested ellipses produce nested lists.
======================================================================
The _gui.ss_ library provides three functions:
> (traces language reductions expr [pp] [colors])
This function calls traces/multiple with language, reductions
and (list expr), and its optional arguments if supplied.
> (traces/multiple lang reductions exprs [pp] [colors])
This function calls traces/pred with the predicate
(lambda (x) #t)
> (traces/pred lang reductions exprs pred [pp] [colors])
lang : language
reductions : (listof reduction)
exprs : (listof sexp)
pred : (sexp -> boolean)
pp : (any -> string)
| (any port number (is-a?/c text%) -> void)
colors : (listof (list string string))
This function opens a new window and inserts each
expr. Then, reduces the terms until either
reduction-steps-cutoff (see below) different terms are
found, or no more reductions can occur. It inserts each new
term into the gui. Clicking the `reduce' button reduces
until reduction-steps-cutoff more terms are found.
The pred function indicates if this term has a particular
property. If the function returns #t, the term is displayed
normally. If it returns #f, the term is displayed with a
red border.
If the pp function can take four arguments, it renders its
first argument into the port (its second argument) with
width at most given by the number (its third argument). The
final argument is the text where the port is connected --
characters written to the port go to the end of the editor.
If the pp function cannot take four arguments, it is
instead invoked with a single argument, the s-expression to
render, and it must return a string which the GUI will use
as a representation of the given expression for display.
The default pp, provided as default-pretty-printer, uses
MzLib's pretty-print function. See threads.ss in the
examples directory for an example use of the one-argument
form of this argument and ho-contracts.ss in the examples
directory for an example use of its four-argument form.
The colors argument, if provided, specifies a list of
reduction-name/color-string pairs. The traces gui will color
arrows drawn because of the given reduction name with the
given color instead of using the default color.
You can save the contents of the window as a postscript file
from the menus.
> (reduction-steps-cutoff)
> (reduction-steps-cutoff number)
A parameter that controls how many steps the `traces' function
takes before stopping.
> (initial-font-size)
> (initial-font-size number)
A parameter that controls the initial font size for the terms shown
in the GUI window.
> (initial-char-width)
> (initial-char-width number)
A parameter that determines the initial width of the boxes
where terms are displayed (measured in characters)
> (dark-pen-color color-or-string)
> (dark-pen-color) => color-or-string
> (dark-brush-color color-or-string)
> (dark-brush-color) => color-or-string
> (light-pen-color color-or-string)
> (light-pen-color) => color-or-string
> (light-brush-color color-or-string)
> (light-brush-color) => color-or-string
These four parameters control the color of the edges in the graph.
======================================================================
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.
Example S-expression forms of ISWIM expressions:
Book S-expr
---- ------
(lambda x . x) ("lam" x x)
(+ '1` '2`) ("+" 1 2)
((lambda y y) '7`) (("lam" y y) 7)
CK machine:
Book S-expr
---- ------
<(lambda x . x), mt> (("lam" x x) : "mt")
CEK machine:
Book S-expr
---- ------
<<(lambda x . x), ((("lam" x x)
{<X,<5,{}>>}>, : ((X (5 : ()))))
mt> : "mt")
The full grammar:
(language (M (M M)
(o1 M)
(o2 M M)
V)
(V X
("lam" variable M)
b)
(X variable)
(b number)
(o1 "add1" "sub1" "iszero")
(o2 "+" "-" "*" "^")
(on o1 o2)
;; Evaluation contexts:
(E hole
(E M)
(V E)
(o1 E)
(o2 E M)
(o2 V E))
;; Continuations (CK machine):
(k "mt"
("fun" V k)
("arg" M k)
("narg" (V ... on) (M ...) k))
;; Environments and closures (CEK):
(env ((X = vcl) ...))
(cl (M : env))
(vcl (V- : env))
;; Values that are not variables:
(V- ("lam" variable M)
b)
;; Continuations with closures (CEK);
(k- "mt"
("fun" vcl k-)
("arg" cl k-)
("narg" (vcl ... on) (cl ...) k-)))
The following are provided by "iswim.ss" (case-insensitively):
Grammar and substitution:
> iswim-grammar : compiled-lang?
> M? : (any? . -> . boolean?)
> V? : (any? . -> . boolean?)
> o1? : (any? . -> . boolean?)
> o2? : (any? . -> . boolean?)
> on? : (any? . -> . boolean?)
> k? : (any? . -> . boolean?)
> env? : (any? . -> . boolean?)
> cl? : (any? . -> . boolean?)
> vcl? : (any? . -> . boolean?)
> k-? : (any? . -> . boolean?)
> iswim-subst : (M? symbol? M? . -> . M?)
> empty-env : env?
> env-extend : (env? symbol? vcl? . -> . env?)
> env-lookup : (env? symbol? . -> . (union false? vcl?))
Reductions:
> beta_v : red?
> delta : (listof red?)
> ->v : (listof red?)
> :->v : (listof red?)
Abbreviations:
> if0 : (M? M? M? . -> . M?)
> true : M?
> false : M?
> mkpair : M?
> fst : M?
> snd : M?
> Y_v : M?
> sum : M?
Helpers:
> delta*1 : (o1? V? . -> . (union false? V?))
delta as a function for unary operations.
> delta*2 : (o2? V? V? . -> . (union false? V?))
delta as a function for binary operations.
> delta*n : (on? (listof V?) . -> . (union false? V?))
delta as a function for any operation.
======================================================================
The _helper.ss_ module provides additional helper functions and syntax.
------- Memoization -------
> (define-memoized (f arg ...) expr ...) SYNTAX
Like `define' for function definitions, except that the function is
"memoized": it automatically remembers each result, and when `eq?'
arguments are provided later, the same result is returned
immediately.
> (lambda-memoized (arg ...) expr) SYNTAX
Like `lambda' except that the resulting function is "memoized" (see
`define-memoized' above).
------- Matching -------
> (lang-match-lambda (variable) grammar-expr
[pattern bodies ...] ...) SYNTAX
Combines a pattern-matching dispatch with a `lambda', producing a
function that takes a single argument and pattern-matches. Each
`pattern' is as for `reduction', and the names that the pattern
binds are visible in the `bodies'.
> (lang-match-lambda* (variable ...) main-variable grammar-expr
[pattern bodies ...] ...) SYNTAX
Generalizes `lang-match-lambda' to create a multi-arity procedure.
The `main-variable' must be one of the `variables', and it is the
variable used for matching.
> lang-match-lambda-memoized SYNTAX
> lang-match-lambda-memoized* SYNTAX
Memoized versions of the above.
------- Backtracking -------
A function that supports backtracking must returns one of the
following:
* #f to indicate failure
* any other value to indicate simple success
* (many-results l) to indicates success with any of the
results in the list l
* (explore-results ...) or (explore-parallel-results ...),
which explores the results of recursive calls to generate
one or more result values lazily
Whenever the backtracking function calls itself (or another
backtracking function in a cooperative set), it should use
`explore-results' or `explore-parallel-results' instead of
inspecting the value directly. To get a single result from
the backtracking function, uses `first-result'.
> many-results : ((listof any) . -> . any)
Aggregates potential results for future exploration.
> (explore-results (id) backtrackable-expr SYNTAX
body-expr ...)
Evaluates `backtrackable-expr'. In the simple case, `id' is bound to
the result, the the result of the `explore-results' expression is
the result of evaluating `body-expr's.
If `backtrackable-expr' produces multiple alternatives (via
`many-results') or if it produces a backtrackable computation, the
result is a backtrackable computation. This backtrackable
computation proceeds bey generating each successful result from
`backtrackable-expr', and then feeding the result to the
`body-expr's to refine the results. Naturally, `body-expr' can
contain further uses of `explore-results' or `many-results' which are
folded into the backtracking exploration.
> (explore-parallel-results (results-id) backtrackable-list-expr
body-expr ...)
Generalizes `explore-results' where `backtrackable-list-expr'
produces a list of backtrackable results, and `body-expr' is called
with successful combinations aggregated into `results-id' as a list.
> first-result : (any . -> . any)
If the argument to `first-result' is a backtrackable computation, it
is explored to obtain the first success, and that success is
returned. If complete backtracking fails, the result is #f. If the
argument to `first-result' is any other value, it is returned
immediately.
------- Misc -------
> function-reduce* : ((listof red?)
any?
(any? . -> . boolean?)
number?
. -> . (listof any?))
A poor-man's `gui' for test interaction. The first argument
represents a set of reductions that define a function; the second
argument is the starting expression; the third argument is a
predicate to recognize ending expressions; the fourth argument
limits the number of steps taken. The function applies the
reductions repeatedly until an ending expression is found, or until
the reduction gets stuck. (If the reduction produces multiple
results, an exception is raised.) The result is the list of
expressions leading to the ending expression.
> unique-names? : ((listof symbol?) . -> . boolean?)
Checks a list of symbols, returning #t if each symbol appears
only once in the list, #f otherwise.
> generate-string : (-> string?)
Returns a string that is generated by incrementing a counter.
> all-of : (any? (any? . -> . any) . -> . (listof any?))
Takes an arbitrary S-expression as the first argument, and a
predicate as the second argument. all-of' then traverses the pairs
that make up the S-expression, calling the predicate on every pair
and every value within a pair. The result is the list of values for
which the predicate returned true. (If the predicate returns true
for a pair, the search does not enter the pair.)
> transitive-closure : ((listof pair?) . -> . (listof (listof any?))
Given the representation of a function as a list of pairs,
`transitive-closure' produces the transitive closure as a list of
lists. Each nested list begins with a domain item and continues
with a list of range items.
Example:
(transitive-closure '((a . b) (b . c))) = '((a b c) (b c))
The input function must be complete (i.e., all range elements
should be in the domain).
Element equality is determined by `eq?' (with the expectation that
elements are usually symbols).
======================================================================
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).

47
collects/reduction-semantics/examples/arithmetic.ss
View File

@ -1,47 +0,0 @@
(module arithmetic mzscheme
(require "../reduction-semantics.ss"
"../gui.ss")
(define lang
(language
(e (binop e e)
(sqrt e)
number)
(binop +
-
*
/)
(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
(--> "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))))

961
collects/reduction-semantics/examples/beginner.ss
View File

@ -1,961 +0,0 @@
#|
This is the semantics of Beginner Scheme, one of the
languages in DrScheme.
The first test case fails because the beginner spec
is broken for that program (ie, the model faithfully
reflects the (broken) spec).
|#
(module beginner mzscheme
(require "../reduction-semantics.ss"
"../subst.ss"
(lib "match.ss"))
(provide run-tests)
#|
`lang' below is actually more generous than beginner, but the
reductions assume that the programs are all syntactically
well-formed programs in beginner scheme (with the additional
constraints that all makers are properly applied and function-
defined variables are only applied and non-function-defined
variables are never applied -- except for the maker check,
these will be in a future version of beginner)
still missing: many primops and characters
are there any primops that take zero arguments?
(should that be syntacically disallowed?)
|#
(define lang
(language
(p (d/e ...))
(d/e (define (x x x ...) e)
(define x (lambda (x x ...) e))
(define x e)
(define-struct x (x ...))
e)
(e (x e e ...)
(prim-op e ...)
(cond (e e) (e e) ...)
(cond (e e) ... (else e))
(if e e e)
(and e e e ...)
(or e e e ...)
empty
x
'x
number
boolean
string)
(prim-op + / cons first rest empty? struct? symbol=?)
(p-ctxt (d/e-v ... d/e-ctxt d/e ...))
(d/e-ctxt (define x e-ctxt)
e-ctxt)
(e-ctxt hole
(x v ... e-ctxt e ...)
(prim-op v ... e-ctxt e ...)
(cond [false e] ... [e-ctxt e] [e e] ...)
(cond [false e] ... [e-ctxt e] [e e] ... [else e])
(and true ... e-ctxt e ...)
(or false ... e-ctxt e ...))
(d/e-v (define x (lambda (x x ...) e))
(define x v)
(define (x x x ...) e)
(define-struct x (x ...))
v)
(v (maker v ...)
non-struct-value)
(non-struct-value number
list-value
boolean
string
'x)
(list-value empty
(cons v list-value))
(boolean true
false)
(maker (side-condition variable_1 (maker? (term variable_1))))
(x (side-condition
(name
x
(variable-except define
define-struct
lambda
cond
else
if
and
or
empty
true
false
quote))
(not (prim-op? (term x)))))))
(define beg-e-subst
(subst
[(? number?)
(constant)]
[(? symbol?)
(variable)]
;; slight cheat here -- but since cond, if, and, or, etc
;; aren't allowed to be variables (syntactically), we're okay.
[`(,@(e ...))
(all-vars '())
(build (lambda (vars . e) e))
(subterms '() e)]))
(define (maker? v)
(and (symbol? v)
(regexp-match #rx"^make-" (symbol->string v))))
(define p? (language->predicate lang 'p))
(define prim-op? (language->predicate lang 'prim-op))
(define-syntax (--> stx)
(syntax-case stx ()
[(_ lhs rhs)
(syntax (reduction/context lang p-ctxt lhs rhs))]))
(define-syntax (e--> stx)
(syntax-case stx ()
[(_ lhs rhs)
(syntax (reduction lang (in-hole p-ctxt lhs) rhs))]))
(define reductions
(list
((and true ... false e ...) . --> . 'false)
((and true ...) . --> . 'true)
((side-condition (and true ... v_1 e ...)
(and (not (eq? (term v_1) 'true))
(not (eq? (term v_1) 'false))))
. e--> .
"and: question result is not true or false")
((or false ... true e ...) . --> . 'true)
((or false ...) . --> . 'false)
((side-condition (or false ... v_1 e ...)
(and (not (eq? (term v_1) 'true))
(not (eq? (term v_1) 'false))))
. e--> .
"or: question result is not true or false")
((if true e_1 e_2) . --> . (term e_1))
((if false e_1 e_2) . --> . (term e_2))
((side-condition (if v_1 e e)
(and (not (eq? (term v_1) 'false))
(not (eq? (term v_1) 'true))))
. e--> .
"if: question result is not true or false")
((cond (false e) ... (true e_1) (e e) ...) . --> . (term e_1))
((cond (false e) ... (true e_1) (e e) ... (else e)) . --> . (term e_1))
((cond (false e) ... (else e_1)) . --> . (term e_1))
((cond (false e) ...) . e--> . "cond: all question results were false")
((side-condition
(cond (false e) ... (v_1 e) (e e) ...)
(and (not (eq? (term v_1) 'false))
(not (eq? (term v_1) 'true))
(not (eq? (term v_1) 'else))))
. e--> .
"cond: question result is not true or false")
((side-condition
(cond (false e) ... (v_1 e) (e e) ... (else e))
(and (not (eq? (term v_1) 'false))
(not (eq? (term v_1) 'true))
(not (eq? (term v_1) 'else))))
. e--> .
"cond: question result is not true or false")
((empty? empty) . --> . 'true)
((side-condition (empty? v_1)
(not (eq? (term v_1) 'empty)))
. --> .
'false)
((empty?) . e--> . "empty?: expects one argument")
((empty? v v v ...) . e--> . "empty?: expects one argument")
((side-condition (cons v v_1)
(and (not (eq? (term v_1) 'empty))
(not (and (pair? (term v_1))
(eq? (car (term v_1)) 'cons)))))
. e--> .
"cons: second argument must be of type <list>")
((first (cons v_1 list-value)) . --> . (term v_1))
((first) . e--> . "first: expects one argument")
((first v v v ...) . e--> . "first: expects one argument")
((side-condition (first v_1)
(not (and (pair? (term v_1))
(eq? (car (term v_1)) 'cons))))
. e--> .
"first: expects argument of type <pair>")
((rest (cons v list-value_1)) . --> . (term list-value_1))
((rest v v v ...) . e--> . "rest: expects one argument")
((rest) . e--> . "rest: expects one argument")
((side-condition (rest v_1)
(not (and (pair? (term v_1))
(eq? (car (term v_1)) 'cons))))
. e--> .
"rest: expects argument of type <pair>")
((symbol=? 'x_1 'x_2) . --> . (if (eq? (term x_1) (term x_2)) 'true 'false))
((side-condition (symbol=? v_1 v_2)
(or (not (and (pair? (term v_1))
(eq? (car (term v_1)) 'quote)))
(not (and (pair? (term v_2))
(eq? (car (term v_2)) 'quote)))))
. e--> .
"symbol=?: expects argument of type <symbol>")
((symbol=?)
. e--> .
"procedure symbol=?: expects 2 arguments")
((symbol=? v v v v ...)
. e--> .
"procedure symbol=?: expects 2 arguments")
((+ number_1 ...) . --> . (apply + (term (number_1 ...))))
((side-condition (+ v_arg ...)
(ormap (lambda (v_arg) (not (number? v_arg))) (term (v_arg ...))))
. e--> .
"+: expects type <number>")
((side-condition (/ number_1 number_2 ...)
(andmap (lambda (number_2) (not (zero? number_2))) (term (number_2 ...))))
. --> .
(apply / (term (number_1 number_2 ...))))
((side-condition (/ number_1 number_2 ...)
(ormap (lambda (number_2) (zero? number_2)) (term (number_2 ...))))
. e--> .
"/: division by zero")
((side-condition (/ v_arg ...)
(ormap (lambda (v_arg) (not (number? v_arg))) (term (v_arg ...))))
. e--> .
"/: expects type <number>")
;; unbound id application
(reduction
lang
(side-condition
((name before d/e-v) ...
(in-hole d/e-ctxt (x_f v ...))
d/e ...)
(and (not (prim-op? (term x_f)))
(not (defined? (term x_f) (term (before ...))))))
(format "reference to undefined identifier: ~a" (term x_f)))
;; procedure application as lambda
(reduction
lang
((name before d/e-v) ...
(name defn (define x_f (lambda (x_var ...) e_body)))
(name middle d/e-v) ...
(in-hole d/e-ctxt_1 (x_f v_arg ...))
(name after d/e) ...)
(term
(before ...
defn
middle ...
(in-hole d/e-ctxt_1
,(multi-subst (term (x_var ...)) (term (v_arg ...)) (term e_body)))
after ...)))
;; define-style procedure application
(reduction
lang
((name before d/e-v) ...
(name defn (define (x_f x_var ...) e_body))
(name middle d/e-v) ...
(in-hole (name ctxt d/e-ctxt) ((name f x) (name arg v) ...))
(name after d/e) ...)
(term
(before ...
defn
middle ...
(in-hole ctxt
,(multi-subst (term (x_var ...))
(term (arg ...))
(term e_body)))
after ...)))
;; reference to non-procedure define:
(reduction
lang
((name before d/e-v) ...
(name defn (define (name a x) (name val v)))
(name middle d/e-v) ...
(in-hole (name ctxt d/e-ctxt) (name a x))
(name after d/e) ...)
(term
(before ...
defn
middle ...
(in-hole ctxt val)
after ...)))
;; unbound reference to top-level id in hole:
(reduction
lang
(side-condition
((name before d/e-v) ...
(in-hole d/e-ctxt (name a x))
d/e ...)
(and (not (prim-op? (term a)))
(not (defined? (term a) (term (before ...))))))
(format "reference to undefined identifier: ~a" (term a)))
;; reference to procedure-bound var in hole:
(reduction
lang
(d/e-v ...
(define ((name f x) (name var x) ...) (name body e))
d/e-v ...
(in-hole d/e-ctxt (name f x))
d/e ...)
(format "~a is a procedure, so it must be applied to arguments" (term f)))
;; reference to non-procedure-bound-var in application
(reduction
lang
(d/e-v ...
(define (name a x) (name val v))
d/e-v ...
(in-hole d/e-ctxt ((name a x) v ...))
d/e ...)
(format "procedure application: expected procedure, given: ~a" (term val)))
((struct? ((name maker maker) v ...)) . --> . 'true)
((struct? non-struct-value) . --> . 'false)
;; struct predicate passes
(reduction
lang
(side-condition
((name before d/e-v) ...
(define-struct (name struct x) ((name field x) ...))
(name middle d/e-v) ...
(in-hole (name ctxt d/e-ctxt) ((name predicate x) ((name maker maker) v ...)))
(name after d/e) ...)
(and (maker-name-match? (term struct) (term maker))
(predicate-name-match? (term struct) (term predicate))))
(term
(before ...
(define-struct struct (field ...))
middle ...
(in-hole ctxt true)
after ...)))
;; struct predicate fail to another struct
(reduction
lang
(side-condition
((name before d/e-v) ...
(define-struct (name struct x) ((name field x) ...))
(name middle d/e-v) ...
(in-hole (name ctxt d/e-ctxt) ((name predicate x) ((name maker maker) v ...)))
(name after d/e) ...)
(and (not (maker-name-match? (term struct) (term maker)))
(predicate-name-match? (term struct) (term predicate))))
(term
(before ...
(define-struct struct (field ...))
middle ...
(in-hole ctxt false)
after ...)))
;; struct predicate fail to another value
(reduction
lang
(side-condition
((name before d/e-v) ...
(define-struct (name struct x) ((name field x) ...))
(name middle d/e-v) ...
(in-hole (name ctxt d/e-ctxt) ((name predicate x) non-struct-value))
(name after d/e) ...)
(predicate-name-match? (term struct) (term predicate)))
(term
(before ...
(define-struct struct (field ...))
middle ...
(in-hole ctxt false)
after ...)))
;; misapplied selector 1
(reduction
lang
(side-condition
(d/e-v
...
(define-struct (name struct x) ((name field x) ...))
d/e-v ...
(in-hole d/e-ctxt ((name selector x) ((name maker maker) (name arg v) ...)))
d/e ...)
(and (not (maker-name-match? (term struct) (term maker)))
(selector-name-match? (term struct) (term (field ...)) (term selector))))
(format "~a: expects argument of matching struct" (term selector)))
;; misapplied selector 2
(reduction
lang
(side-condition
(d/e-v
...
(define-struct (name struct x) ((name field x) ...))
d/e-v ...
(in-hole d/e-ctxt ((name selector x) non-struct-value))
d/e ...)
(selector-name-match? (term struct) (term (field ...)) (term selector)))
(format "~a: expects argument of matching struct" (term selector)))
;; well-applied selector
(reduction
lang
(side-condition
((name before d/e-v) ...
(define-struct (name struct x) ((name field x) ...))
(name middle d/e-v) ...
(in-hole (name ctxt d/e-ctxt) ((name selector x) ((name maker maker) (name arg v) ...)))
(name after d/e) ...)
(and (maker-name-match? (term struct) (term maker))
(selector-name-match? (term struct) (term (field ...)) (term selector))))
(term
(before ...
(define-struct struct (field ...))
middle ...
(in-hole ctxt
,(list-ref (term (arg ...))
(struct-index (term struct)
(term (field ...))
(term selector))))
after ...)))))
(define (defined? f befores)
(ormap
(lambda (before)
(match before
[`(define (,a-name ,@(x ...)) ,b)
(eq? f a-name)]
[`(define ,a-name (lambda ,@(x ...)))
(eq? f a-name)]
[`(define-struct ,struct-name (,@(fields ...)))
(or (ormap (lambda (field)
(eq? f (string->symbol (format "~a-~a" struct-name field))))
fields)
(eq? f (string->symbol (format "make-~a" struct-name)))
(eq? f (string->symbol (format "~a?" struct-name))))]
[else #t]))
befores))
(define (multi-subst vars args body)
(let loop ([args args]
[vars vars]
[body body])
(cond
[(and (null? args) (null? vars))
body]
[(or (null? args) (null? vars))
(error 'multi-subst "malformed program")]
[else (loop (cdr args)
(cdr vars)
(beg-e-subst (car vars) (car args) body))])))
(define (selector-name-match? struct fields selector)
(ormap (lambda (field) (string=? (format "~a-~a" struct field)
(symbol->string selector)))
fields))
(define (struct-index struct init-fields selector)
(let loop ([i 0]
[fields init-fields])
(cond
[(null? fields) (error 'struct-index "~s ~s ~s" struct init-fields selector)]
[else (let ([field (car fields)])
(if (string=? (format "~a-~a" struct field)
(symbol->string selector))
i
(loop (+ i 1)
(cdr fields))))])))
(define (maker-name-match? name maker)
(let* ([names (symbol->string name)]
[makers (symbol->string maker)]
[namel (string-length names)]
[makerl (string-length makers)])
(and (makerl . > . namel)
(string=? (substring makers (- makerl namel) makerl)
names))))
(define (predicate-name-match? name predicate)
(eq? (string->symbol (format "~a?" name)) predicate))
(define failed-tests 0)
(define total-tests 0)
(define (test in out)
(set! total-tests (+ total-tests 1))
(let/ec k
(let* ([failed
(lambda (msg)
(set! failed-tests (+ failed-tests 1))
(fprintf (current-error-port) "FAILED: ~a\n" msg)
(k (void)))]
[got (normalize in failed)])
(unless (equal? got out)
(fprintf (current-error-port) "FAILED: ~s\ngot: ~s\nexpected: ~s\n" in got out)
(set! failed-tests (+ failed-tests 1))))))
(define (test-all step . steps)
(set! total-tests (+ total-tests 1))
(let loop ([this step]
[rest steps])
(let ([nexts (reduce reductions this)])
(cond
[(null? rest)
(unless (null? nexts)
(set! failed-tests (+ failed-tests 1))
(fprintf (current-error-port) "FAILED: ~s\n last step: ~s\n reduced to: ~s\n"
step
this
nexts))]
[else
(cond
[(and (pair? nexts)
(null? (cdr nexts)))
(let ([next (car nexts)])
(if (equal? next (car rest))
(loop (car rest)
(cdr rest))
(begin
(set! failed-tests (+ failed-tests 1))
(fprintf (current-error-port)
"FAILED: ~s\n step: ~s\n expected: ~s\n got: ~s\n"
step
this
(car rest)
next))))]
[else
(set! failed-tests (+ failed-tests 1))
(fprintf (current-error-port)
"FAILED: ~s\n step: ~s\n not single step: ~s\n"
step
this
nexts)])]))))
(define show-dots (make-parameter #f))
(define (normalize term failed)
(let loop ([term term]
[n 1000])
(unless (p? term)
(failed (format "not a p: ~s" term)))
(let ([nexts (reduce reductions term)])
(when (show-dots)
(display #\.)
(flush-output))
(cond
[(= n 0)
(when (show-dots)
(newline))
(error 'normalize "found too many reductions")]
[(null? nexts)
(when (show-dots)
(newline))
term]
[(string? (car nexts))
(when (show-dots)
(newline))
(car nexts)]
[(null? (cdr nexts)) (loop (car nexts) (- n 1))]
[else
(when (show-dots)
(newline))
(failed (format "found more than one reduction\n ~s\n ->\n~s" term nexts))]))))
(define (show-test-results)
(cond
[(= failed-tests 0)
(fprintf (current-error-port) "passed all ~a tests\n" total-tests)]
[else
(fprintf (current-error-port) "failed ~a out of ~a tests\n" failed-tests total-tests)]))
(define-syntax (tests stx)
(syntax-case stx ()
[(_ args ...)
(syntax
(begin
(set! failed-tests 0)
(set! total-tests 0)
args ...
(show-test-results)))]))
(define (run-tests)
(tests
(test
'((define-struct s ())
(s? (make-s)))
'((define-struct s ())
true))
(test
'((define-struct s (a b))
(s-a (make-s 1 3)))
'((define-struct s (a b))
1))
(test
'((define-struct s (a b))
(s-b (make-s 1 3)))
'((define-struct s (a b))
3))
(test
'((define-struct s (a b))
(define-struct t (x y))
(t-x (make-s 1 2)))
"t-x: expects argument of matching struct")
(test
'((define-struct t (x y))
(t-x 12))
"t-x: expects argument of matching struct")
(test
'((define-struct s (a b))
(define-struct t (x y))
(s? (make-s 1 2)))
'((define-struct s (a b))
(define-struct t (x y))
true))
(test
'((define-struct s (a b))
(define-struct t (x y))
(t? (make-s 1 2)))
'((define-struct s (a b))
(define-struct t (x y))
false))
(test
'((define-struct s (a b))
(struct? (make-s 1 2))
(struct? 1))
'((define-struct s (a b))
true
false))
(test
'((define (f x) x)
(f 1))
'((define (f x) x)
1))
(test
'((define (double l) (+ l l))
(double 2))
'((define (double l) (+ l l))
4))
(test
'((define f (lambda (x) x))
(f 1))
'((define f (lambda (x) x))
1))
(test
'((define double (lambda (l) (+ l l)))
(double 2))
'((define double (lambda (l) (+ l l)))
4))
(test
'((f 1))
"reference to undefined identifier: f")
(test
'((f 1)
(define (f x) x))
"reference to undefined identifier: f")
(test
'((make-s 1)
(define-struct s (a b)))
"reference to undefined identifier: make-s")
(test
'((+ 1 2 3))
'(6))
(test
'((+ 1 "2" 3))
"+: expects type <number>")
(test
'((/ 1 2 3))
'(1/6))
(test
'((/ 1 2 0 3))
"/: division by zero")
(test
'((/ 1 "2" 3))
"/: expects type <number>")
(test '((+ 1 (/ (+ 3 5) (+ 2 2)))) '(3))
(test '((symbol=? 'x 'x)) '(true))
(test '((symbol=? 'x 'y)) '(false))
(test '((symbol=? 1 'x))
"symbol=?: expects argument of type <symbol>")
(test '((symbol=? 'x 1))
"symbol=?: expects argument of type <symbol>")
(test '((cons 1 empty)) '((cons 1 empty)))
(test '((cons 1 2))
"cons: second argument must be of type <list>")
(test '((+ (first (cons 1 2)) 2))
"cons: second argument must be of type <list>")
(test '((+ (first (cons 1 empty)) 2))
'(3))
(test
'((first (cons 1 empty)))
'(1))
(test
'((first 1))
"first: expects argument of type <pair>")
(test
'((first 1 2))
"first: expects one argument")
(test
'((first))
"first: expects one argument")
(test
'((rest (cons 1 empty)))
'(empty))
(test
'((rest 1))
"rest: expects argument of type <pair>")
(test
'((rest 1 2))
"rest: expects one argument")
(test
'((rest))
"rest: expects one argument")
(test
'((empty? empty))
'(true))
(test
'((empty? 1))
'(false))
(test
'((empty?))
"empty?: expects one argument")
(test
'((empty? 1 2))
"empty?: expects one argument")
(test
'((cond [true 1]))
'(1))
(test
'((cond [else 1]))
'(1))
(test-all
'((cond [false 1] [else 2]))
'(2))
(test-all
'((cond [false 1] [false 2]))
"cond: all question results were false")
(test
'((cond [1 1]))
"cond: question result is not true or false")
(test
'((cond [(empty? empty) 'infinite] [else 3]))
'('infinite))
(test-all
'((cond [(if false false false) 'x] [(if true true true) 'y] [(if false false false) 'z]))
'((cond [false 'x] [(if true true true) 'y] [(if false false false) 'z]))
'((cond [false 'x] [true 'y] [(if false false false) 'z]))
'('y))
(test-all
'((cond [(if false false false) 'x] [(if true true true) 'y] [else 'z]))
'((cond [false 'x] [(if true true true) 'y] [else 'z]))
'((cond [false 'x] [true 'y] [else 'z]))
'('y))
(test-all
'((cond [(if false false false) 'x] [(if false false false) 'y] [else 'z]))
'((cond [false 'x] [(if false false false) 'y] [else 'z]))
'((cond [false 'x] [false 'y] [else 'z]))
'('z))
(test-all
'((and true true 3))
"and: question result is not true or false")
(test-all
'((and 1 true true))
"and: question result is not true or false")
(test-all
'((and true true true false))
'(false))
(test-all
'((and false true))
'(false))
(test-all
'((or false false 3))
"or: question result is not true or false")
(test-all
'((or 1 false false))
"or: question result is not true or false")
(test-all
'((or false false false true))
'(true))
(test-all
'((or true false))
'(true))
(test-all
'((or (if false false false) (if false false false) (if true true true) (if false false false)))
'((or false (if false false false) (if true true true) (if false false false)))
'((or false false (if true true true) (if false false false)))
'((or false false true (if false false false)))
'(true))
(test-all
'((and (if true true true) (if true true true) (if false false false) (if true true true)))
'((and true (if true true true) (if false false false) (if true true true)))
'((and true true (if false false false) (if true true true)))
'((and true true false (if true true true)))
'(false))
(test
'((if 1 2 3))
"if: question result is not true or false")
(test
'((if true 'x 'y))
'('x))
(test
'((if false 'x 'y))
'('y))
; test non-procedure-defs in context:
(test
`((+ 3 4) (define a 3) (+ 5 6))
`(7 (define a 3) 11))
; test reduction of non-procedure-defs:
(test
`((define a 13) (define b (+ a 9)) (+ 3 4))
`((define a 13) (define b 22) 7))
; test reduction of unbound ids in hole:
(test
`(x)
"reference to undefined identifier: x")
; test reduction of function-bound id in hole:
(test
`((define (a x) (+ x 1)) a)
"a is a procedure, so it must be applied to arguments")
; test reduction of non-procedure-def in application:
(test
`((define a 3) (a 9))
"procedure application: expected procedure, given: 3")))
(define (run-big-test)
(parameterize ([show-dots #t])
(tests
(test
'((define-struct pr (hd tl))
(define (avg l)
(cond
[(empty? l) 'infinite]
[else (/ (sum l) (howmany/acc l 0))]))
(define (sum l)
(cond
[(empty? (pr-tl l)) (pr-hd l)]
[else (+ (pr-hd l) (sum (pr-tl l)))]))
(define (howmany/acc l acc)
(cond
[(empty? l) acc]
[else (howmany/acc (pr-tl l) (+ acc 1))]))
(avg empty)
(avg (make-pr 3 (make-pr 4 (make-pr 5 empty)))))
'((define-struct pr (hd tl))
(define (avg l)
(cond
[(empty? l) 'infinite]
[else (/ (sum l) (howmany/acc l 0))]))
(define (sum l)
(cond
[(empty? (pr-tl l)) (pr-hd l)]
[else (+ (pr-hd l) (sum (pr-tl l)))]))
(define (howmany/acc l acc)
(cond
[(empty? l) acc]
[else (howmany/acc (pr-tl l) (+ acc 1))]))
'infinite
4))
(test
'((define (contains-sym? s l)
(cond
[(empty? l) false]
[true (or (symbol=? s (first l))
(contains-sym? s (rest l)))]))
(contains-sym? 'x (cons 'z (cons 'y (cons 'x empty))))
(contains-sym? 'a (cons 'p (cons 'q empty))))
'((define (contains-sym? s l)
(cond
[(empty? l) false]
[true (or (symbol=? s (first l))
(contains-sym? s (rest l)))]))
true
false))))))

63
collects/reduction-semantics/examples/church.ss
View File

@ -1,63 +0,0 @@
(module church mzscheme
(require "../reduction-semantics.ss"
"../gui.ss"
"../subst.ss")
(reduction-steps-cutoff 100)
(define lang
(language (e (lambda (x) e)
(let (x e) e)
(app e e)
(+ e e)
number
x)
(e-ctxt (lambda (x) e-ctxt)
a-ctxt)
(a-ctxt (let (x a-ctxt) e)
(app a-ctxt e)
(app x a-ctxt)
hole)
(v (lambda (x) e)
x)
(x variable)))
(define reductions
(list
(reduction/context lang
e-ctxt
(app (lambda (x_1) e_body) e_arg)
(ch-subst (term x_1) (term e_arg) (term e_body)))
(reduction/context lang
e-ctxt
(let (x_1 v_1) e_1)
(ch-subst (term x_1) (term v_1) (term e_1)))))
(define ch-subst
(subst
[`(let (,x ,v) ,b)
(all-vars (list x))
(build (lambda (vars v b) `(let (,(car vars) ,v) ,b)))
(subterm '() v)
(subterm (list x) b)]
[`(app ,f ,x)
(all-vars '())
(build (lambda (vars f x) `(app ,f ,x)))
(subterm '() f)
(subterm '() x)]
[`(lambda (,x) ,b)
(all-vars (list x))
(build (lambda (vars body) `(lambda (,(car vars)) ,body)))
(subterm (list x) b)]
[(? number?) (constant)]
[(? symbol?) (variable)]))
(traces lang reductions
'(let (plus (lambda (m)
(lambda (n)
(lambda (s)
(lambda (z)
(app (app m s) (app (app n s) z)))))))
(let (two (lambda (s) (lambda (z) (app s (app s z)))))
(app (app plus two) two)))))

83
collects/reduction-semantics/examples/combinators.ss
View File

@ -1,83 +0,0 @@
;"one point basis"
;"formal aspects of computing"
(module combinators mzscheme
(require "../reduction-semantics.ss"
"../gui.ss")
(initial-font-size 12)
(reduction-steps-cutoff 100)
(initial-char-width 80)
(define lang
(language
(e (e e)
comb
abs1
abs2
abs3)
(e-ctxt (e e-ctxt)
(e-ctxt e)
hole)
(comb i
j
b
c
c*
w)))
(define ij-reductions
(list
(reduction/context lang
e-ctxt
(i e_1)
(term e_1))
(reduction/context lang
e-ctxt
((((j e_a) e_b) e_c) e_d)
(term ((e_a e_b) ((e_a e_d) e_c))))))
(define reductions
(append
ij-reductions
(list
(reduction/context lang
e-ctxt
(((b e_m) e_n) e_l)
(term (e_m (e_n e_l))))
(reduction/context lang
e-ctxt
(((c e_m) e_n) e_l)
(term ((e_m e_l) e_n)))
(reduction/context lang
e-ctxt
((c* e_a) e_b)
(term (e_b e_a)))
(reduction/context lang
e-ctxt
((w e_a) e_b)
(term ((e_a e_b) e_b))))))
(define c* `((j i) i))
(define (make-c c*) `(((j ,c*) (j ,c*)) (j ,c*)))
(define (make-b c) `((,c ((j i) ,c)) (j i)))
(define (make-w b c c*) `(,c ((,c ((,b ,c) ((,c ((,b j) ,c*)) ,c*))) ,c*)))
(define (make-s b c w) `((,b ((,b (,b ,w)) ,c)) (,b ,b)))
(traces/multiple lang
reductions
(list
`((,c* abs1) abs2)
`(((,(make-c 'c*) abs1) abs2) abs3)
`(((,(make-b 'c) abs1) abs2) abs3)
`((,(make-w 'b 'c 'c*) abs1) abs2)
`(((,(make-s 'b 'c 'w) abs1) abs2) abs3)))
;; s in terms of i and j ( > 18,000 reductions and probably still long way to go)
'(traces lang ij-reductions
(make-s (make-b (make-c c*))
(make-c c*)
(make-w (make-b (make-c c*))
(make-c c*)
c*))))

81
collects/reduction-semantics/examples/control.ss
View File

@ -1,81 +0,0 @@
(module control mzscheme
(require "../reduction-semantics.ss"
"../gui.ss"
"../subst.ss")
(reduction-steps-cutoff 100)
(define lang
(language (e (e e)
(\# e)
(f e)
variable
(+ e e)
v)
(c (v c)
(c e)
(\# c)
(f c)
(+ v c)
(+ c e)
hole)
(c# (v c#)
(c# e)
(f c#)
(+ v c#)
(+ c# e)
hole)
(v (lambda (variable) e)
number)))
(define reductions
(list
(reduction lang
(in-hole c_1 (\# (in-hole c#_1 (f v_1))))
(term-let ([x (variable-not-in (term c#) 'x)])
(term
(in-hole c_1
(v_1 (lambda (x) (in-hole c#_1 x)))))))
(reduction lang
(in-hole c#_1 (f v_1))
(term-let ([x (variable-not-in (term c#_1) 'x)])
(term (v_1 (lambda (x) (in-hole c#_1 x))))))
(reduction/context lang
c
((lambda (variable_x) e_body) v_arg)
(lc-subst (term variable_x) (term v_arg) (term e_body)))
(reduction/context lang
c
(+ number_1 number_2)
(+ (term number_1) (term number_2)))))
(define lc-subst
(subst
[`(\# ,e)
(all-vars '())
(build (lambda (vars body) `(\# ,body)))
(subterm '() e)]
[`(f ,e)
(all-vars '())
(build (lambda (vars body) `(f ,body)))
(subterm '() e)]
[`(+ ,e1 ,e2)
(all-vars '())
(build (lambda (vars e1 e2) `(+ ,e1 ,e2)))
(subterm '() e1)
(subterm '() e2)]
[(? symbol?) (variable)]
[(? number?) (constant)]
[`(lambda (,x) ,b)
(all-vars (list x))
(build (lambda (vars body) `(lambda (,(car vars)) ,body)))
(subterm (list x) b)]
[`(,f ,x)
(all-vars '())
(build (lambda (vars f x) `(,f ,x)))
(subterm '() f)
(subterm '() x)]))
(traces/multiple lang reductions
(list '(+ 1 (+ 2 (f (lambda (d) (d (d 0))))))
'(+ 1 (\# (+ 2 (f (lambda (d) (d (d 0))))))))))

72
collects/reduction-semantics/examples/eta.ss
View File

@ -1,72 +0,0 @@
(module eta mzscheme
(require "../reduction-semantics.ss"
"../gui.ss"
"../subst.ss")
(reduction-steps-cutoff 100)
(define lang
(language (e (e e)
x
(+ e e)
v)
(c (v c)
(c e)
(+ v c)
(+ c e)
hole)
(v (lambda (x) e)
number)
(x (variable-except lambda +))))
(define reductions
(list
(reduction/context lang
c
((lambda (variable_x) e_body) v_arg)
(lc-subst (term variable_x) (term v_arg) (term e_body)))
(reduction/context lang
c
(+ number_1 number_2)
(+ (term number_1) (term number_2)))
(reduction/context lang
c
(side-condition (lambda (variable_x) (e_fun variable_x))
(equal? (term e_fun) (lc-subst (term variable_x) 1234 (term e_fun))))
(term e_fun))
(reduction lang
(in-hole c (number_n v_arg))
(format "procedure application: expected procedure, given: ~a; arguments were: ~a"
(term number_n)
(term v_arg)))
(reduction lang
(in-hole c (+ (name non-num (lambda (variable) e)) (name arg2 v)))
(format "+: expects type <number> as 1st argument, given: ~s; other arguments were: ~s"
(term non-num) (term arg2)))
(reduction lang
(in-hole c (+ (name arg1 v) (name non-num (lambda (variable) e))))
(format "+: expects type <number> as 2nd argument, given: ~s; other arguments were: ~s"
(term arg1) (term non-num)))))
(define lc-subst
(subst
[(? symbol?) (variable)]
[(? number?) (constant)]
[`(lambda (,x) ,b)
(all-vars (list x))
(build (lambda (vars body) `(lambda (,(car vars)) ,body)))
(subterm (list x) b)]
[`(+ ,n2 ,n1)
(all-vars '())
(build (lambda (vars n1 n2) `(+ ,n1 ,n1)))
(subterm '() n1)
(subterm '() n2)]
[`(,f ,x)
(all-vars '())
(build (lambda (vars f x) `(,f ,x)))
(subterm '() f)
(subterm '() x)]))
(traces lang reductions '(+ (lambda (x) ((+ 1 2) x)) 1)))

123
collects/reduction-semantics/examples/future.ss
View File

@ -1,123 +0,0 @@
#|
This is an adaptation of Cormac Flanagan's future semantics
to a scheme where each term only has a single hole, but
there are multiple decompositions for each term.
|#
(module future mzscheme
(require "../reduction-semantics.ss"
"../gui.ss"
"../subst.ss")
(define lang
(language
(state (flet (variable state) state)
m
error)
(m (let (variable (future m)) m)
(let (variable (car v)) m)
(let (variable (cdr v)) m)
(let (variable (if v m m)) m)
(let (variable (apply v v)) m)
(let (variable v) m)
v)
(v number
variable
(cons v v)
(lambda (variable) m))
(e-state (flet (variable e-state) state)
(flet (variable state) e-state)
e)
(e hole
(let (variable e) m)
(let (variable (future e)) m))))
(define reductions
(list
(reduction lang
(in-hole (name e e-state)
(let (variable_1 v_val)
m_exp))
(plug (term e)
(future-subst (term variable_1) (term v_val) (term m_exp))))
(reduction lang
(in-hole (name e e-state)
(let (variable_1 (car (cons v_val v)))
m_exp))
(plug (term e) (future-subst (term variable_1)
(term v_val)
(term m_exp))))
(reduction lang
(in-hole (name e e-state)
(let (variable_1 (cdr (cons v v_val)))
m_exp))
(plug (term e) (future-subst (term variable_1)
(term v_val)
(term m_exp))))
(reduction lang
(in-hole (name e e-state)
(let (variable_1 (if true m_then m))
m_exp))
(plug (term e) (term (let (variable_1 m_then) m_exp))))
(reduction lang
(in-hole (name e e-state)
(let (variable_1 (if false m m_else))
m_exp))
(plug (term e) (term (let (variable_1 m_else) m_exp))))
(reduction lang
(in-hole (name e e-state)
(let (variable_1
(apply (lambda (variable_formal) m_body)
v_actual))
m_exp))
(plug
(term e)
(term (let (variable_1 ,(future-subst (term variable_formal) (term v_actual) (term m_body)))
m_exp))))
(reduction lang
(in-hole (name e e-state)
(let (variable_x (future m_1)) m_2))
(let ([p (variable-not-in (list (term e) (term m_1) (term m_2)) 'p)])
(term (flet (,p m_1) (let (variable_x ,p) m_2)))))
(reduction lang
(flet (variable_p v_1) state_body)
(future-subst (term variable_p) (term v_1) (term state_body)))
(reduction lang
(flet (variable_2 (flet (variable_1 state_1) state_2))
state_3)
(term (flet (variable_1 state_1) (flet (variable_2 state_2) state_3))))))
(define future-subst
(subst
[`(let (,a-var ,rhs-exp) ,body-exp)
(all-vars (list a-var))
(build (lambda (vars rhs-exp body-exp) `(let (,(car vars) ,rhs-exp) ,body-exp)))
(subterm '() rhs-exp)
(subterm (list a-var) body-exp)]
[`(lambda (,a-var) ,exp)
(all-vars (list a-var))
(build (lambda (vars body) `(lambda (,(car vars)) ,body)))
(subterm (list a-var) exp)]
[(? number?) (constant)]
[(? symbol?) (variable)]
[`(cons ,hd ,tl)
(all-vars '())
(build (lambda (vars hd tl) `(cons ,hd ,tl)))
(subterm '() hd)
(subterm '() tl)]))
(define (copy-sexp x) (if (pair? x) (cons (copy-sexp (car x)) (copy-sexp (cdr x))) x))
'(traces lang reductions '(let (x (future (let (y (cons 1 2))
(let (z (car y))
z))))
(let (p (cons 3 4))
(let (q (car p))
(cons x q)))))
(traces lang reductions '(let (x (future (let (y 1)
y)))
x)))

567
collects/reduction-semantics/examples/ho-contracts.ss
View File

@ -1,567 +0,0 @@
(module ho-contracts mzscheme
(require "../reduction-semantics.ss"
"../gui.ss"
"../subst.ss"
(lib "mred.ss" "mred")
(lib "framework.ss" "framework")
(lib "class.ss")
(lib "match.ss")
(lib "list.ss"))
(initial-font-size 7) (reduction-steps-cutoff 10)
;(initial-font-size 36) (reduction-steps-cutoff 1)
(define lang
(language
(p ((d ...) e))
(d (valrec x : e = e))
(e (lambda (x) e)
(e e)
(let ((x e) ...) e)
x
(fix x e)
number
(aop e e)
(rop e e)
(cons e e)
empty
(hd e)
(tl e)
(mt e)
(if e e e)
true
false
string
(--> e e)
(contract e)
(flatp e)
(pred e)
(dom e)
(rng e)
(blame e))
(x (variable-except valrec lambda let fix aop rop cons empty hd tl mt if true false --> contract flatp pred dom rng blame))
(p-ctxt (((valrec x : v = v) ...
(valrec x : e-ctxt = e)
d ...)
e)
(((valrec x : v = v) ...
(valrec x : v = e-ctxt)
d ...)
e)
(((valrec x : v = v) ...)
e-ctxt))
(e-ctxt (e-ctxt e)
(v e-ctxt)
(let ((x v) ... (x e-ctxt) (x e) ...) e)
(aop e-ctxt e)
(aop v e-ctxt)
(rop e-ctxt e)
(rop v e-ctxt)
(cons e-ctxt e)
(cons v e-ctxt)
(hd e-ctxt)
(tl e-ctxt)
(mt e-ctxt)
(if e-ctxt e e)
(--> v e-ctxt)
(--> e-ctxt e)
(contract e-ctxt)
(flatp e-ctxt)
(pred e-ctxt)
(dom e-ctxt)
(rng e-ctxt)
(blame e-ctxt)
hole)
(v (cons v v)
(lambda (x) e)
string
number
true
false
(--> v v)
(contract v)
(ob v (--> v v) x x)
compile-v1
compile-v2)
(aop + - * /)
(rop = >=)))
(define ho-contracts-subst
(subst
[`(let ([,a-vars ,rhs-exps] ...) ,body)
(all-vars a-vars)
(build (lambda (vars body . rhss)
`(let (,@(map (lambda (var rhs) `[,var ,rhs]) vars rhss))
,body)))
(subterm a-vars body)
(subterms '() rhs-exps)]
[`(lambda (,var) ,body)
(all-vars (list var))
(build (lambda (vars body) `(lambda (,(car vars)) ,body)))
(subterm (list var) body)]
[`(fix ,variable ,e)
(all-vars (list variable))
(build (lambda (vars body) `(fix ,(car vars) ,body)))
(subterm (list variable) e)]
[(? number?) (constant)]
[`(,(and op (? (lambda (x) (memq x '(cons + - = > / -->))))) ,e1 ,e2)
(all-vars '())
(build (lambda (vars e1 e2) `(,op ,e1 ,e2)))
(subterm '() e1)
(subterm '() e2)]
[`empty (constant)]
[`(,(and op (? (lambda (x) (memq x '(hd tl mt contract flat pred dom rng blame))))) ,e1)
(all-vars '())
(build (lambda (vars e1) `(,op ,e1)))
(subterm '() e1)]
[`(if ,e1 ,e2 ,e3)
(all-vars '())
(build (lambda (vars e1 e2 e3) `(if ,e1 ,e2 ,e3)))
(subterm '() e1)
(subterm '() e2)
(subterm '() e3)]
[`(,e1 ,e2)
(all-vars '())
(build (lambda (vars e1 e2) `(,e1 ,e2)))
(subterm '() e1)
(subterm '() e2)]
[`true (constant)]
[`false (constant)]
[(? string?) (constant)]
[(? symbol?) (variable)]))
(define reductions
(list
(reduction lang
(in-hole (name p p-ctxt) (/ number_n number_m))
(if (= (term number_m) 0)
(term (error /))
(plug (term p) (/ (term number_n) (term number_m)))))
(reduction lang
(in-hole (name p p-ctxt) (* number_n number_m))
(plug (term p) (* (term number_n) (term number_m))))
(reduction lang
(in-hole (name p p-ctxt) (+ number_n number_m))
(plug (term p) (+ (term number_n) (term number_m))))
(reduction lang
(in-hole (name p p-ctxt) (- number_n number_m))
(plug (term p) (- (term number_n) (term number_m))))
(reduction lang
(in-hole (name p p-ctxt) (>= number_n number_m))
(plug (term p) (if (>= (term number_n) (term number_m)) 'true 'false)))
(reduction lang
(in-hole (name p p-ctxt) (= number_n number_m))
(plug (term p) (if (= (term number_n) (term number_m)) 'true 'false)))
(reduction lang
(in-hole (name p p-ctxt) ((lambda (variable_x) e_body) v_arg))
(plug (term p) (ho-contracts-subst (term variable_x)
(term v_arg)
(term e_body))))
(reduction lang
(in-hole (name p p-ctxt)
(let ((variable_i v_i) ...) e_body))
(plug (term p)
(foldl
ho-contracts-subst
(term e_body)
(term (variable_i ...))
(term (v_i ...)))))
(reduction lang
(in-hole (name p p-ctxt) (name tot (fix (name x variable) (name body e))))
(plug (term p) (ho-contracts-subst (term x) (term tot) (term body))))
(reduction lang
((name defns
((valrec (name bvar variable) : (name bctc value) = (name brhs value)) ...
(valrec (name var variable) : value = (name rhs value))
(valrec variable : value = value) ...))
(in-hole (name p e-ctxt) (name var variable)))
(term (defns ,(plug (term p) (term rhs)))))
(reduction lang
(in-hole (name p p-ctxt) (if true e_then e))
(plug (term p) (term e_then)))
(reduction lang
(in-hole (name p p-ctxt) (if false e e_else))
(plug (term p) (term e_else)))
(reduction lang
(in-hole (name p p-ctxt) (hd (cons v_fst v)))
(plug (term p) (term v_fst)))
(reduction lang
(in-hole (name p p-ctxt) (hd empty))
(term (error hd)))
(reduction lang
(in-hole (name p p-ctxt) (tl (cons v v_rst)))
(plug (term p) (term v_rst)))
(reduction lang
(in-hole (name p p-ctxt) (tl empty))
(term (error tl)))
(reduction lang
(in-hole (name p p-ctxt) (mt empty))
(plug (term p) 'true))
(reduction lang
(in-hole (name p p-ctxt) (mt (cons v v)))
(plug (term p) 'false))
(reduction lang
(in-hole (name p p-ctxt) (flatp (contract v)))
(plug (term p) 'true))
(reduction lang
(in-hole (name p p-ctxt) (flatp (--> v v)))
(plug (term p) 'false))
(reduction lang
(in-hole (name p p-ctxt) (pred (contract v_pred)))
(plug (term p) (term v_pred)))
(reduction lang
(in-hole (name p p-ctxt) (pred (--> v v)))
(term (error pred)))
(reduction lang
(in-hole (name p p-ctxt) (dom (--> v_dm v)))
(plug (term p) (term v_dm)))
(reduction lang
(in-hole (name p p-ctxt) (dom (contract v)))
(term (error dom)))
(reduction lang
(in-hole (name p p-ctxt) (rng (--> v v_rg)))
(plug (term p) (term v_rg)))
(reduction lang
(in-hole (name p p-ctxt) (rng (contract v)))
(term (error rng)))
(reduction lang
(in-hole (name p p-ctxt) (blame (name x variable)))
(term (error x)))))
(define (pp v port w spec)
(parameterize ([current-output-port port])
(pp-prog v spec)))
(define (pp-prog prog spec)
(for-each (lambda (x) (pp-defn x spec)) (car prog))
(pp-expr (cadr prog) 0 spec)
(display "\n"))
(define (pp-defn defn spec)
(let ([var (second defn)]
[ctc (fourth defn)]
[exp (sixth defn)])
(printf "val rec ")
(display var)
(display " : ")
(pp-expr ctc 0 spec)
(display " = ")
(pp-expr exp 0 spec)
(display "\n")))
(define (dp/ct x)
(let* ([str (format "~a" x)]
[ct (string-length str)])
(display str)
ct))
;; pp-expr : sexp number (snip -> void) -> (union #f number)
;; returns #f if it started a new line and a
;; number if it didn't. The number indicates
;; how many columns were printed
(define (pp-expr x nl-col text)
(cond
[(equal? x wrapbar)
(insert-wrapbar text)]
[else
(match x
[`(lambda (,v) ,e)
(insert-lambda text)
(insert-variable text v)
(dp/ct ". ")
(next-line (+ nl-col 2))
(pp-expr e (+ nl-col 2) text)
#f]
[`(let ((,vs ,rhss) ...) ,body)
(insert-bold text "let")
(dp/ct " ")
(insert-variable text (car vs))
(dp/ct " = ")
(pp-expr (car rhss) (+ nl-col (string-length (format "let "))) text)
(for-each (lambda (v rhs)
(next-line (+ nl-col (string-length (format "let "))))
(insert-variable text v)
(dp/ct " = ")
(pp-expr rhs (+ nl-col (string-length (format "let "))) text))
(cdr vs)
(cdr rhss))
(next-line (+ nl-col 2))
(pp-expr body (+ nl-col 2) text)
#f]
[`(fix ,v ,e)
(insert-bold text "fix")
(dp/ct " ")
(dp/ct v)
(dp/ct ". ")
(next-line (+ nl-col 2))
(pp-expr e (+ nl-col 2) text)
#f]
[`(if ,e1 ,e2 ,e3)
(insert-bold text "if")
(dp/ct " ")
(pp-expr e1 (+ nl-col 3) text)
(next-line (+ nl-col 2))
(insert-bold text "then")
(dp/ct " ")
(pp-expr e2 (+ nl-col 2 5) text)
(next-line (+ nl-col 2))
(insert-bold text "else")
(dp/ct " ")
(pp-expr e3 (+ nl-col 2 5) text)
#f]
[`(,e1 ,e2)
(let* ([fst-res
(cond
[(simple? e1)
(pp-expr e1 nl-col text)]
[else
(comb (dp/ct "(")
(pp-expr e1 (+ nl-col 1) text)
(dp/ct ")"))])]
[break-lines?
(or (not fst-res)
(>= fst-res 10))]
[_ (when break-lines?
(next-line nl-col))]
[snd-res
(cond
[(simple? e2)
(comb
(dp/ct " ")
(pp-expr e2
(if break-lines?
(+ nl-col 1)
(+ fst-res nl-col 1))
text))]
[else
(comb (dp/ct " (")
(pp-expr e2
(if break-lines?
(+ nl-col 2)
(+ nl-col fst-res 2))
text)
(dp/ct ")"))])])
(comb
fst-res
snd-res))]
[`(,biop ,e1 ,e2)
(let* ([fst-res
(cond
[(simple? e1)
(pp-expr e1 nl-col text)]
[else
(comb
(dp/ct "(")
(pp-expr e1 (+ nl-col 1) text)
(dp/ct ")"))])]
[spc1 (if fst-res
(dp/ct " ")
(begin (next-line nl-col)
#f))]
[middle
(case biop
[(cons) (dp/ct "::")]
[(-->)
(insert-symbol text (string (integer->char 174)))
1]
[else (dp/ct biop)])]
[spc2 (if fst-res
(dp/ct " ")
(begin (next-line nl-col)
#f))]
[snd-res
(cond
[(simple? e2)
(pp-expr e2
(if fst-res
(+ nl-col fst-res spc1 middle spc2)
nl-col)
text)]
[else
(comb
(dp/ct "(")
(pp-expr e2
(if fst-res
(+ nl-col fst-res spc1 middle spc2 1)
(+ nl-col 1))
text)
(dp/ct ")"))])])
(comb fst-res
spc1
middle
spc2
snd-res))]
[`compile-v1
(insert-compile text "V" "1")]
[`compile-v2
(insert-compile text "V" "2")]
[`compile-e
(insert-compile text "e" #f)]
[`empty
(dp/ct "[]")]
[(? (lambda (x)
(and (symbol? x)
(memq x keywords))))
(insert-bold text (symbol->string x))]
[(? symbol?)
(insert-variable text x)]
[else
(dp/ct (format "~s" x))])]))
(define keywords '(contract pred dom rng flatp error blame true false))
(define (insert-lambda text)
(insert-symbol text "l "))
(define (insert-compile text arg subscript)
(let ([sd (make-object style-delta% 'change-family 'script)]
[b-sd (make-object style-delta% 'change-family 'script)])
(send b-sd set-delta 'change-bold)
(+ (insert/style text "C" b-sd)
(insert/snip text (make-object sub-snip% "e"))
(insert/style text "(" sd)
(insert/style text arg #f)
(if subscript
(insert/snip text (make-object sub-snip% subscript))
0)
(insert/style text ")" sd))))
(define (insert-wrapbar text)
(send text insert (make-object wrap-bar%)
(send text last-position)
(send text last-position))
4)
(define (insert-symbol text str)
(insert/style text str (make-object style-delta% 'change-family 'symbol)))
(define (insert-bold text str)
(insert/style text str (make-object style-delta% 'change-bold))
(string-length str))
(define (insert-variable text sym)
(let ([d (make-object style-delta%)]
[str (symbol->string sym)])
(send d set-delta-foreground "forest green")
(insert/style text str d)
(string-length str)))
(define wrap-bar%
(class snip%
(inherit get-style)
(define/override (get-extent dc x y wb hb db ab lspace rspace)
(set-box/f lspace 0)
(set-box/f rspace 0)
(let-values ([(w h d a) (send dc get-text-extent "wrap"
(send (get-style) get-font))])
(set-box/f wb w)
(set-box/f hb h)
(set-box/f db d)
(set-box/f ab a)))
(define/override (draw dc x y left top right bottom dx dy draw-caret?)
(let-values ([(w h d a) (send dc get-text-extent "wrap")])
(send dc draw-text "wrap" x y)
(send dc draw-line x (+ y 1) (+ x w -1) (+ y 1))))
(super-instantiate ())))
(define sub-snip%
(class snip%
(init-field str)
(inherit get-style)
(define/override (get-extent dc x y wb hb db ab lspace rspace)
(set-box/f lspace 0)
(set-box/f rspace 0)
(let-values ([(w h d a) (send dc get-text-extent str
(send (get-style) get-font))])
(set-box/f wb w)
(set-box/f hb (+ h (floor (/ h 3))))
(set-box/f db (- (+ h (floor (/ h 3)))
(- h d)))
(set-box/f ab a)))
(define/override (draw dc x y left top right bottom dx dy draw-caret?)
(let-values ([(w h d a) (send dc get-text-extent str)])
(send dc draw-text str x (+ y (floor (/ h 3))))))
(super-instantiate ())))
(define (set-box/f b v) (when (box? b) (set-box! b v)))
;; insert/snip : text snip -> number
;; returns an approximation to the width of what was inserted
(define (insert/snip text snip)
(send text insert snip (send text last-position) (send text last-position))
1)
;; insert/style : text string style-delta% -> number
;; returns the number of characters in the string
;; (an approximation to the width of what was inserted)
(define (insert/style text str sd)
(let ([pos (send text last-position)])
(send text insert str pos pos)
(when sd
(send text change-style
sd
pos
(send text last-position)))
(string-length str)))
;; comb : (union #f number) *-> (union #f number)
;; sums up its arguments, unless it gets #f,
;; in which case it returns #f
(define (comb . x)
(if (memq #f x)
#f
(apply + x)))
;; simple : any -> bool
;; determines if an expression need parenthesis
(define (simple? exp)
(or (not (pair? exp))
(equal? exp wrapbar)))
;; next-line : number -> void
;; dp/cts a newline and indents to the proper place
(define (next-line n)
(dp/ct "\n")
(let loop ([n n])
(unless (zero? n)
(dp/ct " ")
(loop (- n 1)))))
(define wrapbar
`(fix
wrap
(lambda (ct)
(lambda (x)
(lambda (p)
(lambda (n)
(if (flatp ct)
(if ((pred ct) x)
x
(blame p))
(let ((d (dom ct))
(r (rng ct)))
(lambda (y)
((((wrap r)
(x ((((wrap d) y) n) p)))
p)
n))))))))))
(define flat-case
`(();; defns...
((((,wrapbar (contract compile-v2)) compile-v1) "p") "n")))
(define ho-case
`(();; defns...
((((,wrapbar (--> compile-v1 compile-v2)) (lambda (x) compile-e)) "p") "n")))
(traces lang reductions flat-case pp)
(traces lang reductions ho-case pp)
)

2
collects/reduction-semantics/examples/info.ss
View File

@ -1,2 +0,0 @@
(module info (lib "infotab.ss" "setup")
(define name "Reduction Semantics examples"))

255
collects/reduction-semantics/examples/iswim.ss
View File

@ -1,255 +0,0 @@
(module iswim mzscheme
(require (lib "reduction-semantics.ss" "reduction-semantics")
(lib "subst.ss" "reduction-semantics")
(lib "contract.ss"))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Expression grammar:
(define iswim-grammar
(language (M (M M)
(o1 M)
(o2 M M)
V
("letcc" X M)
("cc" M M))
(V X
("lam" variable M)
b
("[" M "]"))
(X variable)
(b number)
(o1 "add1" "sub1" "iszero")
(o2 "+" "-" "*" "^")
(on o1 o2)
;; Evaluation contexts:
(E hole
(E M)
(V E)
(o1 E)
(o2 E M)
(o2 V E)
("cc" E M)
("cc" V E))
;; Continuations (CK machine):
(k "mt"
("fun" V k)
("arg" M k)
("narg" (V ... on) (M ...) k))
;; Environments and closures (CEK):
(env ((X = vcl) ...))
(cl (M : env))
(vcl (V- : env))
;; Values that are not variables:
(V- ("lam" variable M)
b)
;; Continuations with closures (CEK):
(k- "mt"
("fun" vcl k-)
("arg" cl k-)
("narg" (vcl ... on) (cl ...) k-))))
(define M? (language->predicate iswim-grammar 'M))
(define V? (language->predicate iswim-grammar 'V))
(define o1? (language->predicate iswim-grammar 'o1))
(define o2? (language->predicate iswim-grammar 'o2))
(define on? (language->predicate iswim-grammar 'on))
(define k? (language->predicate iswim-grammar 'k))
(define env? (language->predicate iswim-grammar 'env))
(define cl? (language->predicate iswim-grammar 'cl))
(define vcl? (language->predicate iswim-grammar 'vcl))
(define k-? (language->predicate iswim-grammar 'k-))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Substitution:
;; The subst form makes implemention of capture-avoiding
;; easier. We just have to describe how variables bind
;; in our language's forms.
(define iswim-subst/backwards
(subst
[(? symbol?) (variable)]
[(? number?) (constant)]
[`("lam" ,X ,M)
(all-vars (list X))
(build (lambda (X-list M) `("lam" ,(car X-list) ,M)))
(subterm (list X) M)]
[`(,(and o (or "add1" "sub1" "iszero")) ,M1)
(all-vars '())
(build (lambda (vars M1) `(,o ,M1)))
(subterm '() M1)]
[`(,(and o (or "+" "-" "*" "^")) ,M1 ,M2)
(all-vars '())
(build (lambda (vars M1 M2) `(,o ,M1 ,M2)))
(subterm '() M1)
(subterm '() M2)]
[`(,M1 ,M2)
(all-vars '())
(build (lambda (empty-list M1 M2) `(,M1 ,M2)))
(subterm '() M1)
(subterm '() M2)]
[`("letcc" ,X ,M)
(all-vars (list X))
(build (lambda (X-list M) `("letcc" ,(car X-list) ,M)))
(subterm (list X) M)]
[`("cc" ,M1 ,M2)
(all-vars '())
(build (lambda (vars M1 M2) `("cc" ,M1 ,M2)))
(subterm '() M1)
(subterm '() M2)]
[`("[" ,E "]")
(all-vars '())
(build (lambda (vars) `("[" ,E "]")))]))
;; the argument order for the subst-generated function
;; doesn't match the order in the notes:
(define (iswim-subst M Xr Mr)
(iswim-subst/backwards Xr Mr M))
(define empty-env '())
;; Environment lookup
(define (env-lookup env X)
(let ([m (assq X env)])
(and m (caddr m))))
;; Environment extension
(define (env-extend env X vcl)
(cons (list X '= vcl) env))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Reductions:
;; beta_v reduction
(define beta_v
(reduction iswim-grammar
(("lam" X_1 M_1) V_1)
(iswim-subst (term M_1) (term X_1) (term V_1))))
(define delta
(list
(reduction iswim-grammar ("add1" b_1) (add1 (term b_1)))
(reduction iswim-grammar ("sub1" b_1) (sub1 (term b_1)))
(reduction iswim-grammar ("iszero" b_1)
(if (zero? (term b_1))
'("lam" x ("lam" y x))
'("lam" x ("lam" y y))))
(reduction iswim-grammar ("+" b_1 b_2) (+ (term b_1) (term b_2)))
(reduction iswim-grammar ("-" b_1 b_2) (- (term b_1) (term b_2)))
(reduction iswim-grammar ("*" b_1 b_2) (* (term b_1) (term b_2)))
(reduction iswim-grammar ("^" b_1 b_2) (expt (term b_1) (term b_2)))))
;; ->v
(define ->v (map (lambda (red)
(compatible-closure red iswim-grammar 'M))
(cons beta_v delta)))
;; :->v
(define :->v (map (lambda (red)
(context-closure red iswim-grammar 'E))
(cons beta_v delta)))
;; :->v+letcc
(define :->v+letcc (append
:->v
(list
;; letcc rule:
(reduction
iswim-grammar
(in-hole E_1 ("letcc" X_1 M_1))
(plug (term E_1)
(iswim-subst (term M_1) (term X_1) `("["
,(plug (term E_1) '||)
"]"))))
;; cc rule:
(reduction
iswim-grammar
(in-hole E ("cc" ("[" (in-hole E_2 ||) "]") V_1))
(plug (term E_2) (term V_1))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Helpers:
(define (delta*n on Vs)
(let ([l (reduce delta `(,on ,@Vs))])
(if (null? l)
#f
(car l))))
(define (delta*1 o1 V)
(delta*n o1 (list V)))
(define (delta*2 o2 V1 V2)
(delta*n o2 (list V1 V2)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Abbreviations:
(define (if0 test then else)
(let ([X (variable-not-in `(,then ,else) 'X)])
`(((("iszero" ,test) ("lam" ,X ,then)) ("lam" ,X ,else)) 77)))
(define true '("lam" x ("lam" y x)))
(define false '("lam" x ("lam" y y)))
(define boolean-not `("lam" x ((x ,false) ,true)))
(define mkpair '("lam" x ("lam" y ("lam" s ((s x) y)))))
(define fst '("lam" p (p ("lam" x ("lam" y x)))))
(define snd '("lam" p (p ("lam" x ("lam" y y)))))
(define Y_v '("lam" f ("lam" x
((("lam" g (f ("lam" x ((g g) x))))
("lam" g (f ("lam" x ((g g) x)))))
x))))
(define mksum `("lam" s
("lam" x
,(if0 'x 0 '("+" x (s ("sub1" x)))))))
(define sum `(,Y_v ,mksum))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Exports:
(provide/contract (iswim-grammar compiled-lang?)
(M? (any/c . -> . boolean?))
(V? (any/c . -> . boolean?))
(o1? (any/c . -> . boolean?))
(o2? (any/c . -> . boolean?))
(on? (any/c . -> . boolean?))
(k? (any/c . -> . boolean?))
(env? (any/c . -> . boolean?))
(cl? (any/c . -> . boolean?))
(vcl? (any/c . -> . boolean?))
(iswim-subst (M? symbol? M? . -> . M?))
(env-lookup (env? symbol? . -> . (union false/c vcl?)))
(env-extend (env? symbol? vcl? . -> . env?))
(empty-env env?)
(beta_v red?)
(delta (listof red?))
(delta*1 (o1? V? . -> . (union false/c V?)))
(delta*2 (o2? V? V? . -> . (union false/c V?)))
(delta*n (on? (listof V?) . -> . (union false/c V?)))
(->v (listof red?))
(:->v (listof red?))
(:->v+letcc (listof red?))
(if0 (M? M? M? . -> . M?))
(true M?)
(false M?)
(boolean-not M?)
(mkpair M?)
(fst M?)
(snd M?)
(Y_v M?)
(sum M?)))

47
collects/reduction-semantics/examples/macro.ss
View File

@ -1,47 +0,0 @@
(module macro mzscheme
(require "../reduction-semantics.ss"
"../gui.ss")
(define lang
(language
(e (lambda (variable) e)
(app e e)
number
variable)
(e-ctxt (lambda (variable) e-ctxt)
(app e-ctxt any)
(app e e-ctxt)
hole)))
(define macros '(or let if true false id))
(define-syntax (--> stx)
(syntax-case stx ()
[(_ frm to)
(syntax (reduction/context lang e-ctxt frm to))]))
(define reductions
(list
(--> (id (name e any))
(term e))
(--> (side-condition ((name e1 any) (name e2 any))
(not (memq (term e1) macros)))
(term (app e1 e2)))
(--> (or (name e1 any) (name e2 any))
(let ([var (variable-not-in (list (term e1) (term e2)) 'x)])
(term (let (,var e1) (if ,var ,var e2)))))
(--> (let ((name var variable) (name rhs any))
(name body any))
(term ((lambda (var) body) rhs)))
(--> (if (name test any)
(name thn any)
(name els any))
(term ((test thn) els)))
(--> (true)
(term (lambda (x) (lambda (y) x))))
(--> (false)
(term (lambda (x) (lambda (y) y))))))
(traces lang reductions '((id id) 5))
(traces lang reductions '(id 5))
(traces lang reductions '(or (false) (true))))

64
collects/reduction-semantics/examples/omega.ss
View File

@ -1,64 +0,0 @@
(module omega mzscheme
(require "../reduction-semantics.ss"
"../gui.ss"
"../subst.ss")
(reduction-steps-cutoff 10)
(define lang
(language (e (e e)
(abort e)
x
v)
(c (v c)
(c e)
hole)
(v call/cc
number
(lambda (x) e))
(x (variable-except lambda call/cc abort))
))
(define reductions
(list
(reduction lang
(in-hole c_1 (call/cc v_arg))
(term-let ([v (variable-not-in (term c_1) 'x)])
(term (in-hole c_1 (v_arg (lambda (v) (abort (in-hole c_1 v))))))))
(reduction lang
(in-hole c (abort e_1))
(term e_1))
(reduction/context lang
c
((lambda (variable_x) e_body) v_arg)
(lc-subst (term variable_x) (term v_arg) (term e_body)))))
(define lc-subst
(plt-subst
['abort (constant)]
['call/cc (constant)]
[(? symbol?) (variable)]
[(? number?) (constant)]
[`(lambda (,x) ,b)
(all-vars (list x))
(build (lambda (vars body) `(lambda (,(car vars)) ,body)))
(subterm (list x) b)]
[`(call/cc ,v)
(all-vars '())
(build (lambda (vars arg) `(call/cc ,arg)))
(subterm '() v)]
[`(,f ,x)
(all-vars '())
(build (lambda (vars f x) `(,f ,x)))
(subterm '() f)
(subterm '() x)]))
;(traces lang reductions '((lambda (x) (x x)) (lambda (x) (x x))))
;(traces lang reductions '((call/cc call/cc) (call/cc call/cc)))
(traces lang reductions '((lambda (x) ((call/cc call/cc) x)) (call/cc call/cc)))
)

190
collects/reduction-semantics/examples/semaphores.ss
View File

@ -1,190 +0,0 @@
#|
semaphores make things much more predictable...
|#
(module semaphores mzscheme
(require "../reduction-semantics.ss"
"../gui.ss")
(reduction-steps-cutoff 100)
(define lang
(language
(p ((store (variable v) ...)
(semas (variable sema-count) ...)
(threads e ...)))
(sema-count number
none)
(e (set! variable e)
(begin e ...)
(semaphore variable)
(semaphore-wait e)
(semaphore-post e)
(lambda (variable) e)
(e e)
variable
(list e ...)
(cons e e)
number
(void))
(p-ctxt ((store (variable v) ...)
(semas (variable sema-count) ...)
(threads e ... e-ctxt e ...)))
(e-ctxt (e-ctxt e)
(v e-ctxt)
(cons e-ctxt e)
(cons v e-ctxt)
(list v ... e-ctxt e ...)
(set! variable e-ctxt)
(begin e-ctxt e ...)
(semaphore-wait e-ctxt)
(semaphore-post e-ctxt)
hole)
(v (semaphore variable)
(lambda (variable) e)
(list v ...)
number
(void))))
(define reductions
(list
(reduction lang
(in-hole (name c p-ctxt) (begin v e_1 e_2 e_rest ...))
(plug
(term c)
(term (begin e_1 e_2 e_rest ...))))
(reduction lang
(in-hole (name c p-ctxt)
(cons v_1 (list v_2s ...)))
(plug
(term c)
(term (list v_1 v_2s ...))))
(reduction lang
(in-hole (name c p-ctxt) (begin v e_1))
(plug (term c) (term e_1)))
(reduction lang
(in-hole (name c p-ctxt) (begin v_1))
(plug (term c) (term v_1)))
(reduction lang
((store
(name befores (variable v)) ...
((name x variable) (name v v))
(name afters (variable v)) ...)
(name semas any)
(threads
(name e-before e) ...
(in-hole (name c e-ctxt) (name x variable))
(name e-after e) ...))
(term
((store
befores ...
(x v)
afters ...)
semas
(threads
e-before ...
(in-hole c v)
e-after ...))))
(reduction lang
((store
(name befores (variable v)) ...
(variable_i v)
(name afters (variable v)) ...)
(name semas any)
(threads
(name e-before e) ...
(in-hole (name c e-ctxt) (set! variable_i v_new))
(name e-after e) ...))
(term
((store
befores ...
(variable_i v_new)
afters ...)
semas
(threads
e-before ...
(in-hole c (void))
e-after ...))))
(reduction lang
((name store any)
(semas
(name befores (variable v)) ...
(variable_sema number_n)
(name afters (variable v)) ...)
(threads
(name e-before e) ...
(in-hole (name c e-ctxt) (semaphore-wait (semaphore variable_sema)))
(name e-after e) ...))
(term
(store
(semas
befores ...
(variable_sema ,(if (= (term number_n) 1)
(term none)
(- (term number_n) 1)))
afters ...)
(threads
e-before ...
(in-hole c (void))
e-after ...))))
(reduction lang
((name store any)
(semas
(name befores (variable v)) ...
(variable_sema number_n)
(name afters (variable v)) ...)
(threads
(name e-before e) ...
(in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema)))
(name e-after e) ...))
(term
(store
(semas
befores ...
(variable_sema ,(+ (term number_n) 1))
afters ...)
(threads
e-before ...
(in-hole c (void))
e-after ...))))
(reduction lang
((name store any)
(semas
(name befores (variable v)) ...
(variable_sema none)
(name afters (variable v)) ...)
(threads
(name e-before e) ...
(in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema)))
(name e-after e) ...))
(term
(store
(semas
befores ...
(variable_sema 1)
afters ...)
(threads
e-before ...
(in-hole c (void))
e-after ...))))))
(traces lang
reductions
`((store (y (list)))
(semas)
(threads (set! y (cons 1 y))
(set! y (cons 2 y)))))
(traces lang
reductions
`((store (y (list)))
(semas (x 1))
(threads (begin (semaphore-wait (semaphore x))
(set! y (cons 1 y))
(semaphore-post (semaphore x)))
(begin (semaphore-wait (semaphore x))
(set! y (cons 2 y))
(semaphore-post (semaphore x)))))))

96
collects/reduction-semantics/examples/subject-reduction.ss
View File

@ -1,96 +0,0 @@
(module subject-reduction mzscheme
(require "../reduction-semantics.ss"
"../gui.ss"
"../subst.ss"
(lib "plt-match.ss"))
(reduction-steps-cutoff 10)
(define lang
(language (e (e e)
(abort e)
x
v)
(x (variable-except lambda call/cc abort))
(c (v c)
(c e)
hole)
(v call/cc
number
(lambda (x t) e))
(t num
(t -> t))))
(define reductions
(list
(reduction lang
(in-hole c_1 (call/cc v_arg))
(let ([v (variable-not-in (term c_1) 'x)])
(plug
(term c_1)
(term (v_arg (lambda (,v)
(abort ,(plug (term c_1) v))))))))
(reduction lang
(in-hole c (abort e_1))
(term e_1))
(reduction/context lang
c
((lambda (x_format t_1) e_body) v_actual)
;(lc-subst x_format v_actual e_body)
(lc-subst (term x_format) (term e_body) (term v_actual))
)))
(define lc-subst
(plt-subst
[(? symbol?) (variable)]
[(? number?) (constant)]
[`(lambda (,x ,t) ,b)
(all-vars (list x))
(build (lambda (vars body) `(lambda (,(car vars) ,t) ,body)))
(subterm (list x) b)]
[`(call/cc ,v)
(all-vars '())
(build (lambda (vars arg) `(call/cc ,arg)))
(subterm '() v)]
[`(,f ,x)
(all-vars '())
(build (lambda (vars f x) `(,f ,x)))
(subterm '() f)
(subterm '() x)]))
(define (type-check term)
(let/ec k
(let loop ([term term]
[env '()])
(match term
[(? symbol?)
(let ([l (assoc term env)])
(if l
(cdr l)
(k #f)))]
[(? number?) 'num]
[`(lambda (,x ,t) ,b)
(let ([body (loop b (cons (cons x t) env))])
`(,t -> ,body))]
[`(,e1 ,e2)
(let ([t1 (loop e1 env)]
[t2 (loop e2 env)])
(match t1
[`(,td -> ,tr)
(if (equal? td t2)
tr
(k #f))]
[else (k #f)]))]))))
(define (pred term1)
(let ([t1 (type-check term1)])
(lambda (term2)
(and t1
(equal? (type-check term2) t1)))))
(define (show term)
(traces/pred lang reductions (list term) (pred term)))
;(show '((lambda (x num) x) 1))
(show '((lambda (x (num -> num)) 1) ((lambda (x (num -> num)) x) (lambda (x num) x))))
)

128
collects/reduction-semantics/examples/threads.ss
View File

@ -1,128 +0,0 @@
(module threads mzscheme
(require "../reduction-semantics.ss"
"../gui.ss"
"../subst.ss"
(lib "plt-match.ss"))
(reduction-steps-cutoff 100)
(define threads
(language
(p ((store (x v) ...) (threads e ...)))
(e (set! x e)
(let ((x e)) e)
(e e)
x
v
(+ e e))
(v (lambda (x) e)
number)
(x variable)
(pc ((store (x v) ...) tc))
(tc (threads e ... ec e ...))
(ec (ec e) (v ec) (set! variable ec) (let ((x ec)) e) (+ ec e) (+ v ec) hole)))
(define reductions
(list
; sum
(reduction threads
(in-hole pc_1 (+ number_1 number_2))
(plug (term pc_1)
(+ (term number_1) (term number_2))))
; deref
(reduction threads
((store
(name befores (x v)) ...
(x_i v_i)
(name afters (x v)) ...)
(in-hole tc_1 x_i))
(term
((store
befores ...
(x_i v_i)
afters ...)
,(plug (term tc_1) (term v_i)))))
; set!
(reduction threads
((store (name befores (variable v)) ...
(x_i v)
(name afters (variable v)) ...)
(in-hole tc_1 (set! x_i v_new)))
(term
((store
befores ...
(x_i v_new)
afters ...)
,(plug (term tc_1)
(term v_new)))))
; beta
(reduction threads
(in-hole pc_1 ((lambda (x_1) e_1) v_1))
(plug (term pc_1)
(substitute (term x_1) (term v_1) (term e_1))))
; let
(reduction threads
((store (name the-store any) ...)
(in-hole tc_1 (let ((x_1 v_1)) e_1)))
(let ((new-x (variable-not-in (term (the-store ...)) (term x_1))))
(term
((store the-store ... (,new-x v_1))
,(plug (term tc_1)
(substitute (term x_1) new-x (term e_1)))))))))
(define substitute
(plt-subst
[(? symbol?) (variable)]
[(? number?) (constant)]
[`(lambda (,x) ,b)
(all-vars (list x))
(build (lambda (vars body) `(lambda (,(car vars)) ,body)))
(subterm (list x) b)]
[`(set! ,x ,e)
(all-vars '())
(build (lambda (vars name body) `(set! ,name ,body)))
(subterm '() x)
(subterm '() e)]
[`(let ((,x ,e1)) ,e2)
(all-vars (list x))
(build (lambda (vars letval body) `(let ((,(car vars) ,letval)) ,body)))
(subterm '() e1)
(subterm (list x) e2)]
[`(+ ,e1 ,e2)
(all-vars '())
(build (lambda (vars e1 e2) `(+ ,e1 ,e2)))
(subterm '() e1)
(subterm '() e2)]
[`(,f ,x)
(all-vars '())
(build (lambda (vars f x) `(,f ,x)))
(subterm '() f)
(subterm '() x)]))
(define (run es) (traces threads reductions `((store) (threads ,@es))))
(provide run)
(define (count x)
(match x
[`(set! ,x ,e) (+ 1 (count e))]
[(? symbol?) 1]
[(? number?) 0]
[`(+ ,e1 ,e2) (+ 1 (count e1) (count e2))]))
(traces threads reductions
'((store (x 1))
(threads
(set! x (+ x -1))
(set! x (+ x 1))))
(lambda (exp)
(match exp
[`((store (x ,x)) (threads ,t1 ,t2))
(format "~a ~a ~a" x (count t1) (count t2))])))
(parameterize ([initial-char-width 12])
(traces threads reductions '((store) (threads (+ 1 1) (+ 1 1)))))
)

91
collects/reduction-semantics/examples/types.ss
View File

@ -1,91 +0,0 @@
(module types mzscheme
(require (lib "reduction-semantics.ss" "reduction-semantics")
(lib "gui.ss" "reduction-semantics")
(lib "subst.ss" "reduction-semantics"))
(reduction-steps-cutoff 10)
(define lang
(language (e (e e)
x
number
(lambda (x t) e)
(if e e e)
(= e e)
(-> e e)
num
bool)
(c (t c)
(c e)
(-> t c)
(-> c e)
(= t c)
(= c e)
(if c e e)
(if t c e)
(if t t c)
hole)
(x (variable-except lambda -> if =))
(t num bool (-> t t))))
(define-syntax (r--> stx)
(syntax-case stx ()
[(_ i r) (syntax (reduction/context lang c i r))]))
(define-syntax (e--> stx)
(syntax-case stx ()
[(_ i msg) (syntax (reduction lang (in-hole c i) msg))]))
(define reductions
(list
(r--> number
'num)
(r--> (lambda (x_1 t_1) e_body)
(term (-> t_1 ,(lc-subst (term x_1)
(term t_1)
(term e_body)))))
(r--> ((-> t_1 t_2) t_1)
(term t_2))
(e--> (side-condition ((-> t_1 t) t_2)
(not (equal? (term t_1) (term t_2))))
(format "app: domain error ~s and ~s" (term t_1) (term t_2)))
(e--> (num t_1)
(format "app: non function error ~s" (term t_1)))
(r--> (if bool t_1 t_1)
(term t_1))
(e--> (side-condition (if bool t_1 t_2)
(not (equal? (term t_1) (term t_2))))
(format "if: then and else clause mismatch ~s and ~s" (term t_1) (term t_2)))
(e--> (side-condition (if t_1 t t)
(not (equal? (term t_1) 'bool)))
(format "if: test not boolean ~s" (term t_1)))
(r--> (= num num) 'bool)
(e--> (side-condition (= t_1 t_2)
(or (not (equal? (term t_1) 'num))
(not (equal? (term t_2) 'num))))
(format "=: not comparing numbers ~s and ~s" (term t_1) (term t_2)))))
(define lc-subst
(subst
[(? symbol?) (variable)]
[(? number?) (constant)]
[`(lambda (,x ,t) ,b)
(all-vars (list x))
(build (lambda (vars body) `(lambda (,(car vars) ,t) ,body)))
(subterm (list x) b)]
[`(,f ,@(xs ...))
(all-vars '())
(build (lambda (vars f . xs) `(,f ,@xs)))
(subterm '() f)
(subterms '() xs)]))
; (define theterm '((lambda (x num) (lambda (y num) (if (= x y) 0 x))) 1))
(define theterm '((lambda (x num) (lambda (y num) (if (= x y) 0 (lambda (x num) x)))) 1))
(traces lang reductions theterm)
)

245
collects/reduction-semantics/generator.ss
View File

@ -1,245 +0,0 @@
(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)))))

1023
collects/reduction-semantics/graph.ss
View File

File diff suppressed because it is too large Load Diff

565
collects/reduction-semantics/gui.ss
View File

@ -1,565 +0,0 @@
;; should cache the count of new snips -- dont
;; use `count-snips'; use something associated with the
;; equal hash-table
(module gui mzscheme
(require (lib "etc.ss")
(lib "graph.ss" "reduction-semantics")
"reduction-semantics.ss"
(lib "mred.ss" "mred")
(lib "framework.ss" "framework")
(lib "pretty.ss")
(lib "class.ss")
(lib "contract.ss")
(lib "list.ss")
(lib "match.ss"))
(provide/contract
[traces (opt-> (compiled-lang?
(listof red?)
any/c)
(procedure? (listof any/c))
any)]
[traces/pred (opt-> (compiled-lang?
(listof red?)
(listof any/c)
(any/c . -> . boolean?))
(procedure? (listof any/c))
any)]
[traces/multiple (opt-> (compiled-lang?
(listof red?)
(listof any/c))
(procedure? (listof any/c))
any)])
(provide reduction-steps-cutoff initial-font-size initial-char-width
dark-pen-color light-pen-color dark-brush-color light-brush-color
dark-text-color light-text-color
(rename default-pp default-pretty-printer))
(preferences:set-default 'plt-reducer:show-bottom #t boolean?)
(define dark-pen-color (make-parameter "blue"))
(define light-pen-color (make-parameter "lightblue"))
(define dark-brush-color (make-parameter "lightblue"))
(define light-brush-color (make-parameter "white"))
(define dark-text-color (make-parameter "blue"))
(define light-text-color (make-parameter "lightblue"))
;; after (about) this many steps, stop automatic, initial reductions
(define reduction-steps-cutoff (make-parameter 20))
(define initial-font-size
(make-parameter
(send (send (send (editor:get-standard-style-list)
find-named-style
"Standard")
get-font)
get-point-size)))
(define initial-char-width (make-parameter 30))
;; the initial spacing between row and columns of the reduction terms
(define x-spacing 15)
(define y-spacing 15)
(define (default-pp v port w spec)
(parameterize ([pretty-print-columns w])
(pretty-print v port)))
(define traces
(opt-lambda (lang reductions expr [pp default-pp] [colors '()])
(traces/multiple lang reductions (list expr) pp colors)))
(define traces/multiple
(opt-lambda (lang reductions exprs [pp default-pp] [colors '()])
(traces/pred lang reductions exprs (lambda (x) #t) pp colors)))
(define traces/pred
(opt-lambda (lang reductions exprs pred [pp default-pp] [colors '()])
(define main-eventspace (current-eventspace))
(define graph-pb (make-object graph-pasteboard%))
(define f (instantiate red-sem-frame% ()
(label "Reduction Graph")
(graph-pb graph-pb)
(width 600)
(height 400)
(toggle-panel-callback
(lambda ()
(send remove-my-contents-panel
change-children
(lambda (l)
(preferences:set 'plt-reducer:show-bottom (null? l))
(if (null? l)
(list bottom-panel)
null)))))))
(define ec (make-object editor-canvas% (send f get-area-container) graph-pb))
(define remove-my-contents-panel (new vertical-panel%
(parent (send f get-area-container))
(stretchable-height #f)))
(define bottom-panel (new vertical-panel%
(parent remove-my-contents-panel)
(stretchable-height #f)))
(define font-size (instantiate slider% ()
(label "Font Size")
(min-value 1)
(init-value (initial-font-size))
(max-value 127)
(parent bottom-panel)
(callback (lambda (slider evt) (set-font-size (send slider get-value))))))
(define lower-panel (instantiate horizontal-panel% ()
(parent bottom-panel)
(stretchable-height #f)))
(define reduce-button (make-object button%
"Reducing..."
lower-panel
(lambda (x y)
(reduce-button-callback))))
(define status-message (instantiate message% ()
(label "")
(parent lower-panel)
(stretchable-width #t)))
(define snip-cache (make-hash-table 'equal))
;; call-on-eventspace-main-thread : (-> any) -> any
;; =reduction thread=
(define (call-on-eventspace-main-thread thnk)
(parameterize ([current-eventspace main-eventspace])
(let ([s (make-semaphore 0)]
[ans #f])
(queue-callback
(lambda ()
(set! ans (thnk))
(semaphore-post s)))
(semaphore-wait s)
ans)))
;; only changed on the reduction thread
;; frontier : (listof (is-a?/c graph-editor-snip%))
(define frontier (map (lambda (expr) (build-snip snip-cache #f expr pred pp
(dark-pen-color) (light-pen-color)
(dark-text-color) (light-text-color) #f))
exprs))
;; set-font-size : number -> void
;; =eventspace main thread=
(define (set-font-size size)
(let* ([scheme-standard (send (editor:get-standard-style-list) find-named-style
"Standard")]
[scheme-delta (make-object style-delta%)])
(send scheme-standard get-delta scheme-delta)
(send scheme-delta set-size-mult 0)
(send scheme-delta set-size-add size)
(send scheme-standard set-delta scheme-delta)))
;; color-spec-list->color-scheme : (list (union string? #f)^4) -> (list string?^4)
;; converts a list of user-specified colors (including false) into a list of color strings, filling in
;; falses with the default colors
(define (color-spec-list->color-scheme l)
(map (λ (c d) (or c d))
l
(list (dark-pen-color) (light-pen-color) (dark-text-color) (light-text-color))))
(define name->color-ht
(let ((ht (make-hash-table 'equal)))
(for-each
(λ (c)
(hash-table-put! ht (car c)
(color-spec-list->color-scheme
(match (cdr c)
[(color)
(list color color (dark-text-color) (light-text-color))]
[(dark-arrow-color light-arrow-color)
(list dark-arrow-color light-arrow-color (dark-text-color) (light-text-color))]
[(dark-arrow-color light-arrow-color text-color)
(list dark-arrow-color light-arrow-color text-color text-color)]
[(_ _ _ _)
(cdr c)]))))
colors)
ht))
;; red->colors : reduction -> (values string string string string)
(define (red->colors red)
(apply values (hash-table-get name->color-ht (reduction->name red)
(λ () (list (dark-pen-color) (light-pen-color) (dark-text-color) (light-text-color))))))
;; reduce-frontier : -> void
;; =reduction thread=
;; updates frontier with the new snip after a single reduction
(define (reduce-frontier)
(let ([col #f])
(let loop ([snips frontier]
[new-frontier null]
[y 0])
(cond
[(null? snips)
(set! frontier new-frontier)]
[else
(let* ([snip (car snips)]
[new-snips
(filter
(lambda (x) x)
(map (lambda (red+sexp)
(let-values ([(red sexp) (apply values red+sexp)])
(call-on-eventspace-main-thread
(λ ()
(let-values ([(dark-arrow-color light-arrow-color dark-label-color light-label-color) (red->colors red)])
(build-snip snip-cache snip sexp pred pp light-arrow-color dark-arrow-color dark-label-color light-label-color
(reduction->name red)))))))
(reduce/tag-with-reduction reductions (send snip get-expr))))]
[new-y
(call-on-eventspace-main-thread
(lambda () ; =eventspace main thread=
(send graph-pb begin-edit-sequence)
(unless col ;; only compute col here, incase user moves snips
(set! col (+ x-spacing (find-rightmost-x graph-pb))))
(begin0
(insert-into col y graph-pb new-snips)
(send graph-pb end-edit-sequence)
(send status-message set-label
(string-append (term-count (count-snips)) "...")))))])
(loop (cdr snips)
(append new-frontier new-snips)
new-y))]))))
;; count-snips : -> number
;; =eventspace main thread=
;; counts the snips in `pb'. If connections?
;; is #t, also counts the number of connections
;; and returns the sum of the connections and snips
(define (count-snips)
(let loop ([n 0]
[snip (send graph-pb find-first-snip)])
(cond
[snip (loop (+ n 1) (send snip next))]
[else n])))
;; reduce-button-callback : -> void
;; =eventspace main thread=
(define (reduce-button-callback)
(send reduce-button enable #f)
(send reduce-button set-label "Reducing...")
(thread
(lambda ()
(do-some-reductions)
(queue-callback
(lambda () ;; =eventspace main thread=
(scroll-to-rightmost-snip)
(send reduce-button set-label "Reduce")
(cond
[(null? frontier)
(send status-message set-label (term-count (count-snips)))]
[else
(send status-message set-label
(string-append (term-count (count-snips))
"(possibly more to find)"))
(send reduce-button enable #t)]))))))
(define (term-count n)
(format "found ~a term~a" n (if (equal? n 1) "" "s")))
;; do-some-reductions : -> void
;; =reduction thread=
;; reduces some number of times,
;; adding at least reduction-steps-cutoff steps
;; before stopping (unless there aren't that many left)
(define (do-some-reductions)
(let ([initial-size (call-on-eventspace-main-thread count-snips)])
(let loop ()
(cond
[(null? frontier) (void)]
[((call-on-eventspace-main-thread count-snips) . >= . (+ initial-size (reduction-steps-cutoff)))
(void)]
[else
(reduce-frontier)
(loop)]))))
;; scroll-to-rightmost-snip : -> void
;; =eventspace main thread=
(define (scroll-to-rightmost-snip)
(let ([rightmost-snip (send graph-pb find-first-snip)])
(let loop ([rightmost-snip rightmost-snip]
[rightmost-y (get-right-edge rightmost-snip)]
[snip (send rightmost-snip next)])
(cond
[(not snip) (make-snip-visible rightmost-snip)]
[else
(let ([snip-y (get-right-edge snip)])
(if (<= rightmost-y snip-y)
(loop snip snip-y (send snip next))
(loop rightmost-snip rightmost-y (send snip next))))]))))
;; make-snip-visisble : snip -> void
;; =eventspace-main-thread=
(define (make-snip-visible snip)
(let ([bl (box 0)]
[bt (box 0)]
[br (box 0)]
[bb (box 0)])
(send graph-pb get-snip-location snip bl bt #f)
(send graph-pb get-snip-location snip br bb #t)
(send graph-pb scroll-to
snip
0
0
(- (unbox br) (unbox bl))
(- (unbox bb) (unbox bt))
#t)))
;; get-right-edge : snip -> void
;; =eventspace-main-thread=
(define (get-right-edge snip)
(let ([br (box 0)])
(send graph-pb get-snip-location snip br #f #t)
(unbox br)))
(send remove-my-contents-panel
change-children
(lambda (l)
(if (preferences:get 'plt-reducer:show-bottom)
(list bottom-panel)
null)))
(insert-into init-rightmost-x 0 graph-pb frontier)
(set-font-size (initial-font-size))
(reduce-button-callback)
(send f show #t)))
(define red-sem-frame%
(class (frame:standard-menus-mixin (frame:basic-mixin frame%))
(init-field graph-pb toggle-panel-callback)
(define/override (file-menu:create-save?) #f)
(define/override (file-menu:between-save-as-and-print file-menu)
(make-object menu-item% "Print..."
file-menu
(lambda (item evt) (send graph-pb print)))
(make-object menu-item% "Export as Encapsulted PostScript..."
file-menu
(lambda (item evt) (send graph-pb print #t #f 'postscript this #f)))
(make-object menu-item% "Export as PostScript..."
file-menu
(lambda (item evt) (send graph-pb print #t #f 'postscript this)))
(make-object menu-item%
"Toggle bottom stuff"
file-menu
(lambda (item evt) (toggle-panel-callback))))
(super-instantiate ())))
(define (resizing-pasteboard-mixin pb%)
(class pb%
(define/augment (on-interactive-resize snip)
(when (is-a? snip reflowing-snip<%>)
(send snip reflow-program))
#;(super on-interactive-resize snip))
(define/augment (after-interactive-resize snip)
(when (is-a? snip reflowing-snip<%>)
(send snip reflow-program))
#;(super after-interactive-resize snip))
(define/override (interactive-adjust-resize snip w h)
(super interactive-adjust-resize snip w h)
(when (is-a? snip reflowing-snip<%>)
(send snip reflow-program)))
(super-instantiate ())))
(define reflowing-snip<%>
(interface ()
reflow-program))
(define graph-pasteboard%
(resizing-pasteboard-mixin
(graph-pasteboard-mixin pasteboard%)))
(define graph-editor-snip%
(class* (graph-snip-mixin editor-snip%) (reflowing-snip<%>)
(init-field expr pp char-width bad?)
(define/public (get-expr) expr)
(inherit get-editor)
(define/public (reflow-program)
(let ([ed (get-editor)])
(when ed
(let ([ed-ad (send ed get-admin)])
(when ed-ad
(let ([dc (send ed get-dc)]
[wb (box 0)]
[std-style (send (editor:get-standard-style-list) find-named-style "Standard")])
(send ed-ad get-view #f #f wb #f)
(let-values ([(tw _1 _2 _3) (send dc get-text-extent "w"
(and std-style
(send std-style get-font)))])
(let ([new-width (max 1 (inexact->exact (floor (/ (- (unbox wb) 2) tw))))])
(unless (equal? new-width char-width)
(set! char-width new-width)
(format-expr))))))))))
(inherit get-extent)
(define/override (draw dc x y left top right bottom dx dy draw-caret)
(when bad?
(let ([bw (box 0)]
[bh (box 0)]
[pen (send dc get-pen)]
[brush (send dc get-brush)])
(get-extent dc x y bw bh #f #f #f #f)
(send dc set-pen (send the-pen-list find-or-create-pen bad-color 1 'solid))
(send dc set-brush (send the-brush-list find-or-create-brush bad-color 'solid))
(send dc draw-rectangle x y (unbox bw) (unbox bh))
(send dc set-pen pen)
(send dc set-brush brush)))
(super draw dc x y left top right bottom dx dy draw-caret))
(define/public (format-expr)
(let* ([text (get-editor)]
[port (make-output-port
'graph-port
always-evt
(lambda (bytes start end buffering? enable-breaks?)
(send text insert (bytes->string/utf-8 (subbytes bytes start end))
(send text last-position)
(send text last-position))
(- end start))
void)])
(send text begin-edit-sequence)
(send text thaw-colorer)
(send text set-styles-sticky #f)
(send text erase)
(pp expr port char-width text)
(when (char=? #\newline (send text get-character (- (send text last-position) 1)))
(send text delete (- (send text last-position) 1) (send text last-position)))
(send text freeze-colorer)
(when bad?
(send text change-style bad-style-delta 0 (send text last-position)))
(send text end-edit-sequence)))
(super-instantiate ())))
(define program-text%
(class scheme:text%
(init-field bad?)
(define/override (on-paint before? dc left top right bottom dx dy draw-caret)
(when (and bad? before?)
(let ([pen (send dc get-pen)]
[brush (send dc get-brush)])
(send dc set-pen (send the-pen-list find-or-create-pen bad-color 1 'solid))
(send dc set-brush (send the-brush-list find-or-create-brush bad-color 'solid))
(send dc draw-rectangle (+ dx left) (+ dy top) (- right left) (- bottom top))
(send dc set-pen pen)
(send dc set-brush brush)))
(super on-paint before? dc left top right bottom dx dy draw-caret))
(super-new)))
(define lines-pen (send the-pen-list find-or-create-pen "black" 1 'solid))
(define bad-style-delta (make-object style-delta% 'change-italic))
(define bad-color "pink")
;; where the first snips are inserted
(define init-rightmost-x 25)
;; insert-into : number number pasteboard (listof snip%) -> number
;; inserts the snips into the pasteboard vertically
;; aligned, starting at (x,y). Returns
;; the y coordinate where another snip might be inserted.
(define (insert-into x y pb exprs)
(let loop ([exprs exprs]
[y y])
(cond
[(null? exprs) y]
[else
(let ([es (car exprs)])
(send pb insert es x y)
(loop (cdr exprs)
(+ y (find-snip-height pb es) y-spacing)))])))
;; build-snip : hash-table
;; (union #f (is-a?/c graph-snip<%>))
;; sexp
;; sexp -> boolean
;; (any port number -> void)
;; color
;; (union #f string)
;; -> (union #f (is-a?/c graph-editor-snip%))
;; returns #f if a snip corresponding to the expr has already been created.
;; also adds in the links to the parent snip
;; =eventspace main thread=
(define (build-snip cache parent-snip expr pred pp light-arrow-color dark-arrow-color dark-label-color light-label-color label)
(let-values ([(snip new?)
(let/ec k
(k
(hash-table-get
cache
expr
(lambda ()
(let ([new-snip (make-snip parent-snip expr pred pp)])
(hash-table-put! cache expr new-snip)
(k new-snip #t))))
#f))])
(when parent-snip
(add-links/text-colors parent-snip snip
(send the-pen-list find-or-create-pen dark-arrow-color 0 'solid)
(send the-pen-list find-or-create-pen light-arrow-color 0 'solid)
(send the-brush-list find-or-create-brush (dark-brush-color) 'solid)
(send the-brush-list find-or-create-brush (light-brush-color) 'solid)
(make-object color% dark-label-color)
(make-object color% light-label-color)
0 0
label))
(and new? snip)))
;; make-snip : (union #f (is-a?/c graph-snip<%>))
;; sexp
;; sexp -> boolean
;; (any port number -> void)
;; -> (is-a?/c graph-editor-snip%)
;; unconditionally creates a new graph-editor-snip
;; =eventspace main thread=
(define (make-snip parent-snip expr pred pp)
(let* ([bad? (not (pred expr))]
[text (new program-text% (bad? bad?))]
[es (instantiate graph-editor-snip% ()
(char-width (initial-char-width))
(editor text)
(pp
(if (procedure-arity-includes? pp 4)
pp
(lambda (v port w spec) (display (pp v) port))))
(expr expr)
(bad? bad?))])
(send text set-autowrap-bitmap #f)
(send text freeze-colorer)
(send es format-expr)
es))
;; find-rightmost-x : pasteboard -> number
(define (find-rightmost-x pb)
(let ([first-snip (send pb find-first-snip)])
(if first-snip
(let loop ([snip first-snip]
[max-x (find-snip-right-edge pb first-snip)])
(cond
[snip
(loop (send snip next)
(max max-x (find-snip-right-edge pb snip)))]
[else max-x]))
init-rightmost-x)))
;; find-snip-right-edge : editor snip -> number
(define (find-snip-right-edge ed snip)
(let ([br (box 0)])
(send ed get-snip-location snip br #f #t)
(unbox br)))
;; find-snip-height : editor snip -> number
(define (find-snip-height ed snip)
(let ([bt (box 0)]
[bb (box 0)])
(send ed get-snip-location snip #f bt #f)
(send ed get-snip-location snip #f bb #t)
(- (unbox bb)
(unbox bt)))))

206
collects/reduction-semantics/helper.ss
View File

@ -1,206 +0,0 @@
(module helper mzscheme
(require (lib "contract.ss")
"reduction-semantics.ss")
(define counter 0)
(define (generate-string)
(set! counter (add1 counter))
(format "s~a" counter))
(define (unique-names? l)
(let ([ht (make-hash-table)])
(andmap (lambda (n)
(if (hash-table-get ht n (lambda () #f))
#f
(begin
(hash-table-put! ht n #t)
#t)))
l)))
(define (all-of P ?)
;; Traverse P as an sexp, and look for class-name uses:
(let ([l (let loop ([sexp P])
(cond
[(? sexp) (list sexp)]
[(pair? sexp) (append (loop (car sexp)) (loop (cdr sexp)))]
[else null]))]
[ht (make-hash-table)])
;; Filter duplicates by hashing:
(for-each (lambda (i) (hash-table-put! ht i #t)) l)
(hash-table-map ht (lambda (k v) k))))
(define-syntaxes (lang-match-lambda*
lang-match-lambda-memoized*
lang-match-lambda
lang-match-lambda-memoized)
(let ([generic
(lambda (lam)
(lambda (stx)
(syntax-case stx ()
[(_ (id ...) main-id grammar [pattern result] ...)
(with-syntax ([red (generate-temporaries #'(pattern ...))]
[lam lam]
[ids #'(id ...)])
(syntax/loc
stx
(let ([lang grammar]
[escape (make-parameter void)])
(let ([reds (list (reduction grammar pattern ((escape) (lambda ids result)))
...)])
(lam (id ...)
((let/ec esc
(parameterize ([escape esc])
(reduce reds main-id)
(error 'lang-match-lambda "no pattern matched input: ~e" main-id)))
id ...))))))])))]
[single
(lambda (multi)
(lambda (stx)
(syntax-case stx ()
[(_ (id) grammar [pattern result] ...)
(with-syntax ([multi multi])
#'(multi (id) id grammar [pattern result] ...))])))])
(values
(generic #'lambda)
(generic #'lambda-memoized)
(single #'lang-match-lambda*)
(single #'lang-match-lambda-memoized*))))
(define (transitive-closure orig)
;; Copy initial mapping:
(let ([map (map (lambda (p) (list (car p) (cdr p))) orig)])
;; Extend the map list until nothing changes
(let loop ()
(let ([changed? #f])
(for-each (lambda (pair)
(let ([mapping (cdr pair)])
(for-each (lambda (item)
(let ([trans (ormap (lambda (transitive)
(and (not (memq transitive mapping))
transitive))
(cdr (assq item map)))])
(when trans
(append! pair (list trans))
(set! changed? #t))))
mapping)))
map)
(when changed? (loop))))
;; Done
map))
(define-syntax (lambda-memoized stx)
(syntax-case stx ()
[(_ () body1 body ...)
(syntax/loc stx (lambda () body1 body ...))]
[(_ (arg) body1 body ...)
(syntax/loc
stx
(let ([ht (make-hash-table 'weak)])
(lambda (arg)
(hash-table-get
ht
arg
(lambda ()
(let ([v (begin body1 body ...)])
(hash-table-put! ht arg v)
v))))))]
[(_ (arg1 arg ...) body1 body ...)
(syntax/loc
stx
(let ([memo (lambda-memoized (arg1) (lambda-memoized (arg ...) body1 body ...))])
(lambda (arg1 arg ...)
((memo arg1) arg ...))))]))
(define-syntax define-memoized
(syntax-rules ()
[(_ (f . args) body1 body ...)
(define f (lambda-memoized args body1 body ...))]))
;; function-reduce*
(define (function-reduce* reds expr done? max-steps)
(cons
expr
(if (or (zero? max-steps) (done? expr))
null
(let ([l (reduce reds expr)])
(cond
[(null? l) null]
[(= 1 (length l))
(function-reduce* reds (car l) done? (sub1 max-steps))]
[else
(error 'function-reduce*
"found ~a possible steps from ~e"
(length l)
expr)])))))
(define-struct multi-result (choices))
;; ----------------------------------------
;; Path exploration:
(define-syntax (explore-results stx)
(syntax-case stx ()
[(_ (id) result-expr body-expr bes ...)
#'(let ([try (lambda (id) body-expr bes ...)])
(let ([r result-expr])
(do-explore r try)))]))
(define-syntax (explore-parallel-results stx)
(syntax-case stx ()
[(_ (list-id) result-list-expr body-expr bes ...)
#'(let ([try (lambda (list-id) body-expr bes ...)])
(let loop ([rs result-list-expr][es null])
(if (null? rs)
(try (reverse es))
(do-explore
(car rs)
(lambda (e)
(loop (cdr rs) (cons e es)))))))]))
(define (do-explore r try)
(cond
[(multi-result? r)
(let loop ([l (multi-result-choices r)])
(if (null? l)
#f
(let ([a ((car l))])
(if (multi-result? a)
(loop (append (multi-result-choices a)
(cdr l)))
(let ([v (try a)])
(if (not v)
(loop (cdr l))
(make-multi-result
(append (if (multi-result? v)
(multi-result-choices v)
(list (lambda () v)))
(list (lambda () (loop (cdr l))))))))))))]
[else (try r)]))
(define (many-results l)
(make-multi-result (map (lambda (v) (lambda () v)) l)))
(define (first-result result)
(let/ec k
(explore-results (x) result
(k x))))
(provide
define-memoized
lambda-memoized
lang-match-lambda
lang-match-lambda-memoized
lang-match-lambda*
lang-match-lambda-memoized*
explore-results
explore-parallel-results)
(provide/contract
(function-reduce* ((listof red?) any/c (any/c . -> . boolean?) number?
. -> . (listof any/c)))
(unique-names? ((listof symbol?) . -> . boolean?))
(generate-string (-> string?))
(all-of (any/c (any/c . -> . any) . -> . (listof any/c)))
(transitive-closure ((listof pair?) . -> . (listof (listof any/c))))
(many-results ((listof (lambda (x) (not (multi-result? x)))) . -> . any))
(first-result (any/c . -> . any))))

4
collects/reduction-semantics/info.ss
View File

@ -1,4 +0,0 @@
(module info (lib "infotab.ss" "setup")
(define name "PLT Redex")
(define doc.txt "doc.txt"))

376
collects/reduction-semantics/mc.ss
View File

@ -1,376 +0,0 @@
(module mc mzscheme
(require (lib "reduction-semantics.ss" "reduction-semantics")
(lib "generator.ss" "reduction-semantics")
(prefix matcher: (lib "matcher.ss" "reduction-semantics" "private"))
(lib "list.ss")
(lib "class.ss")
(lib "mred.ss" "mred"))
(provide build-reductions
generation-depth
reduction-depth
generate-and-test
(struct reduction-graph (initial ht)))
;; reduction-graph = (make-graph sexp hash-table[sexp -o> (listof sexp)])
(define-struct reduction-graph (initial ht))
(define generation-depth (make-parameter 2))
(define reduction-depth (make-parameter 10))
(define max-queue-size 100)
;; computes all of the terms of size `n' or smaller for each non-terminal
;; in the language
;; [ sizes are limited by number of recusive constructions of each non terminal;
;; 4 is huge for even tiny languages ]
(define (generate-and-test lang nt reductions reductions-test)
(define frame (make-object frame% "Status"))
(define gc-on-bitmap (make-object bitmap% (build-path (collection-path "icons") "recycle.gif")))
(define gc-off-bitmap (make-object bitmap%
(send gc-on-bitmap get-width)
(send gc-on-bitmap get-height)
#t))
(define stupid-internal-define-syntax1
(let ([bdc (make-object bitmap-dc% gc-off-bitmap)])
(send bdc clear)
(send bdc set-bitmap #f)))
(define-values (reductions-queue-size-message
total-reductions-message
test-queue-size-message
total-tests-message
memory-allocated-message)
(let* ([outer-hp (make-object horizontal-panel% frame)]
[outer-vp (make-object vertical-panel% outer-hp)]
[hp1 (make-object horizontal-panel% outer-vp)]
[hp2 (make-object horizontal-panel% outer-vp)]
[hp3 (make-object horizontal-panel% outer-vp)]
[hp4 (make-object horizontal-panel% outer-vp)]
[hp5 (make-object horizontal-panel% outer-vp)]
[l1 (make-object message% "To Reduce: " hp1)]
[l2 (make-object message% "Total Expressions: " hp2)]
[l3 (make-object message% "To Test: " hp3)]
[l4 (make-object message% "Total Tests: " hp4)]
[l5 (make-object message% "Megabytes Allocated: " hp5)]
[gc-canvas (instantiate canvas% ()
(parent outer-hp)
(stretchable-width #f)
(stretchable-height #f)
(min-width (send gc-on-bitmap get-width))
(min-height (send gc-on-bitmap get-height)))]
[dms-button (instantiate button% ("DMS" outer-hp)
[callback (lambda (b e)
(dump-memory-stats '<struct>))])])
(register-collecting-blit gc-canvas
0
0
(send gc-on-bitmap get-width)
(send gc-on-bitmap get-height)
gc-on-bitmap
gc-off-bitmap)
(let ([w (max (send l1 get-width)
(send l2 get-width)
(send l3 get-width)
(send l4 get-width)
(send l5 get-width))])
(send l1 min-width w)
(send l2 min-width w)
(send l3 min-width w)
(send l4 min-width w)
(send l5 min-width w))
(values
(instantiate message% ()
(label "0000000")
;(stretchable-width #t)
(parent hp1))
(instantiate message% ()
(label "0000000")
;(stretchable-width #t)
(parent hp2))
(instantiate message% ()
(label "0000000")
;(stretchable-width #t)
(parent hp3))
(instantiate message% ()
(label "0000000")
;(stretchable-width #t)
(parent hp4))
(instantiate message% ()
(label "0000000")
;(stretchable-width #t)
(parent hp5)))))
(define go (make-semaphore 0))
(define no-more-terms (box 'no-more-terms))
(define generation-thread
(thread
(lambda ()
(semaphore-wait go)
(generate lang nt enqueue-for-reduction-thread)
(enqueue-for-reduction-thread no-more-terms))))
(define total-reductions 0)
(define reduction-queue (new-queue))
(define reduction-queue-sema (make-semaphore 1))
(define reduction-thread-sema (make-semaphore 0))
(define reduction-producer-sema (make-semaphore max-queue-size))
(define (enqueue-for-reduction-thread sexp)
(semaphore-wait reduction-producer-sema)
(semaphore-wait reduction-queue-sema)
(enqueue reduction-queue sexp)
(set! total-reductions (+ total-reductions 1))
(semaphore-post reduction-thread-sema)
(semaphore-post reduction-queue-sema))
(define reduction-thread
(thread
(lambda ()
(semaphore-wait go)
(let loop ()
(semaphore-wait reduction-thread-sema)
(semaphore-wait reduction-queue-sema)
(let ([sexp (dequeue reduction-queue)])
(semaphore-post reduction-queue-sema)
(semaphore-post reduction-producer-sema)
(cond
[(eq? sexp no-more-terms)
(enqueue-for-test-thread no-more-terms)]
[else
(enqueue-for-test-thread (build-reductions sexp reductions))
(loop)]))))))
(define total-tests 0)
(define test-queue (new-queue))
(define test-queue-sema (make-semaphore 1))
(define test-thread-sema (make-semaphore 0))
(define test-producer-sema (make-semaphore max-queue-size))
(define (enqueue-for-test-thread sexp)
(semaphore-wait test-producer-sema)
(semaphore-wait test-queue-sema)
(enqueue test-queue sexp)
(set! total-tests (+ total-tests 1))
(semaphore-post test-thread-sema)
(semaphore-post test-queue-sema))
(define test-thread
(thread
(lambda ()
(semaphore-wait go)
(let loop ()
(semaphore-wait test-thread-sema)
(semaphore-wait test-queue-sema)
(let ([reds (dequeue test-queue)])
(semaphore-post test-queue-sema)
(semaphore-post test-producer-sema)
(cond
[(eq? reds no-more-terms)
(semaphore-post done-semaphore)]
[else
(reductions-test reds)]))
(loop)))))
(define mem-divisor (* 1024 1024))
(define (update-status)
(send test-queue-size-message set-label (format "~a" (queue-size test-queue)))
(send total-tests-message set-label (format "~a" total-tests))
(send reductions-queue-size-message set-label (format "~a" (queue-size reduction-queue)))
(send total-reductions-message set-label (format "~a" total-reductions))
(send memory-allocated-message set-label (number->string (quotient (current-memory-use) mem-divisor))))
(define status-thread
(thread
(lambda ()
(semaphore-wait go)
(with-handlers ([exn:break? (lambda (x) (semaphore-post status-thread-done))])
(let loop ()
(update-status)
(sleep 2)
(loop))))))
(define done-semaphore (make-semaphore 0))
(define status-thread-done (make-semaphore 0))
(send frame show #t)
(semaphore-post go)
(semaphore-post go)
(semaphore-post go)
(semaphore-post go)
(yield done-semaphore)
(break-thread status-thread)
(semaphore-wait status-thread-done)
(update-status)
(make-object message% "Done." frame))
;
;
;
; ; ; ;
; ; ;
; ; ; ;
; ; ;; ;;; ;;; ; ; ; ;;;; ;;;; ; ;;;; ; ;;; ;;; ; ; ;; ;;; ; ;;; ; ;;;
; ;; ; ; ; ;; ; ; ; ; ; ; ; ;; ; ; ;; ;; ; ; ;; ; ;; ;
; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;
; ; ;;;;; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;;;; ; ; ; ;
; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;
; ; ; ; ;; ; ;; ; ; ; ; ; ; ; ; ;; ; ; ; ;; ; ; ;
; ; ;;;; ;;; ; ;;; ; ;;;; ;; ; ;;;; ; ; ;;; ; ; ;;;;; ; ;;; ; ;
; ; ;
; ; ; ;
; ;;;; ;
;; build-reductions : sexp (listof reductions) -> reduction-graph
;; builds the reduction graph for expression according to reductions
(define (build-reductions expression reductions)
(let* ([ht (make-hash-table 'equal)]
[reduce/add
(lambda (term)
(let ([reduced (reduce reductions term)])
(hash-table-put! ht term reduced)
(filter (lambda (term)
(not (hash-table-get ht term (lambda () #f))))
reduced)))])
(let loop ([frontier (list expression)]
[depth (reduction-depth)])
(unless (zero? depth)
(let* ([new-terms (apply append (map reduce/add frontier))])
(cond
[(null? new-terms) (void)]
[else
(loop new-terms (- depth 1))]))))
(make-reduction-graph expression ht)))
;
;
;
; ;
;
; ;
; ;;; ; ;;; ; ;;; ;;; ; ;; ;;; ;;;; ; ;;;; ; ;;;
; ; ;; ; ; ;; ; ; ; ;; ; ; ; ; ; ; ;; ;
; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;
; ; ; ;;;;; ; ; ;;;;; ; ;;;; ; ; ; ; ; ;
; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;
; ; ;; ; ; ; ; ; ; ; ; ; ; ; ; ;
; ;;; ; ;;;; ; ; ;;;; ; ;;;;; ;; ; ;;;; ; ;
; ;
; ; ;
; ;;;;
;; generate : lang sexp (sexp -> void) -> void
;; generates the terms up to (generation-depth) in size
;; passes each that comes from gdesired-nt to enqueue-for-reduction-thread
(define (generate lang desired-nt enqueue-for-reduction-thread)
(let ([gens (lang->generator-table lang
'(0 1)
'(x y)
'("a" "b")
null
0)])
(let loop ([n 0])
(unless (n . > . (generation-depth))
(for-each-generated/size (lambda (sexp size)
(enqueue-for-reduction-thread sexp))
gens
n n desired-nt)
(loop (add1 n))))))
;; find-interesting-nts : (listof nt) sym -> (listof sym)
(define (find-interesting-nts clang desired-nt)
(let* ([lang (matcher:compiled-lang-lang clang)]
[ht (make-hash-table)]
[nt-syms (map matcher:nt-name lang)])
(let loop ([nt-sym desired-nt])
(let ([nt-lst (filter (lambda (x) (eq? (matcher:nt-name x) nt-sym)) lang)])
(cond
[(null? nt-lst) (void)]
[(null? (cdr nt-lst))
(let ([referenced-nt-syms (get-referenced-nts nt-syms (car nt-lst) lang)])
(for-each
(lambda (referenced-nt-sym)
(unless (hash-table-get ht referenced-nt-sym (lambda () #f))
(hash-table-put! ht referenced-nt-sym #t)
(loop referenced-nt-sym)))
referenced-nt-syms))]
[else (error 'mc.ss "found more than one definition of ~s in grammar" nt-sym)])))
(hash-table-map ht (lambda (x y) x))))
(define (get-referenced-nts nt-syms nt lang)
(let loop ([rhss (matcher:nt-rhs nt)]
[refd-nts null])
(cond
[(null? rhss) refd-nts]
[else (loop (cdr rhss)
(get-referenced-nts/rhs nt-syms (car rhss) refd-nts))])))
(define (get-referenced-nts/rhs nt-syms rhs acc)
(let loop ([pat (matcher:rhs-pattern rhs)]
[acc acc])
(cond
[(null? pat) acc]
[(pair? pat) (loop (car pat) (loop (cdr pat) acc))]
[(symbol? pat)
(if (memq pat nt-syms)
(cons pat acc)
acc)])))
;
;
;
;
;
;
; ;;; ; ; ; ;;; ; ; ;;;
; ; ;; ; ; ; ; ; ; ; ;
; ; ; ; ; ; ; ; ; ; ;
; ; ; ; ; ;;;;; ; ; ;;;;;
; ; ; ; ; ; ; ; ;
; ; ;; ; ;; ; ; ;; ;
; ;;; ; ;;; ; ;;;; ;;; ; ;;;;
; ;
; ;
; ;
(define-struct queue (hd tl size))
(define (new-queue) (make-queue null null 0))
(define (enqueue queue thnk)
(set-queue-size! queue (+ (queue-size queue) 1))
(let ([new-tail (cons thnk null)])
(if (null? (queue-hd queue))
(begin
(set-queue-hd! queue new-tail)
(set-queue-tl! queue new-tail))
(begin
(set-cdr! (queue-tl queue) new-tail)
(set-queue-tl! queue new-tail)))))
(define (dequeue queue)
(when (null? (queue-hd queue))
(error 'dequeue))
(set-queue-size! queue (- (queue-size queue) 1))
(let* ([qh (queue-hd queue)]
[fst (car qh)])
(set-queue-hd! queue (cdr qh))
(set-cdr! qh #f)
(when (null? (queue-hd queue))
(set-queue-tl! queue null))
fst))
(define (queue-empty? queue) (null? (queue-hd queue))))

2
collects/reduction-semantics/private/info.ss
View File

@ -1,2 +0,0 @@
(module info (lib "infotab.ss" "setup")
(define name "Reduction Semantics private"))

37
collects/reduction-semantics/private/make-plt.ss
View File

@ -1,37 +0,0 @@
(module make-plt mzscheme
(require (lib "file.ss")
(lib "pack.ss" "setup")
(lib "plthome.ss" "setup"))
(current-directory plthome)
(define (display-res f)
(lambda (x)
(let ([ans (f x)])
(when ans
(printf "including ~s~n" x))
ans)))
(define bad-dirs '("CVS" ".svn"))
(define bad-files '(".DS_Store" "reduction-semantics.plt"))
(pack (build-path "collects" "reduction-semantics" "reduction-semantics.plt")
"Reduction Semantics"
(list (build-path "collects" "reduction-semantics"))
'(("reduction-semantics"))
(display-res
(lambda (filename)
(let ([exp (reverse (explode-path (normalize-path filename)))])
(cond
[(member (cadr exp) bad-dirs)
#f]
[(member (car exp) bad-dirs)
#f]
[(member (car exp) bad-files)
#f]
[(regexp-match #rx"~$" (path->string filename))
#f]
[else
(std-filter filename)]))))
#t
'file-replace))

634
collects/reduction-semantics/private/matcher-test.ss
View File

@ -1,634 +0,0 @@
(module matcher-test mzscheme
(require "matcher.ss"
(lib "list.ss"))
(define (make-test-mtch a b c) (make-mtch a (build-flat-context b) c))
(define (test)
(print-struct #t)
(test-empty 'any 1 (list (make-test-mtch (make-bindings null) 1 none)))
(test-empty 'any 'true (list (make-test-mtch (make-bindings null) 'true none)))
(test-empty 'any "a" (list (make-test-mtch (make-bindings null) "a" none)))
(test-empty 'any '(a b) (list (make-test-mtch (make-bindings null) '(a b) none)))
(test-empty 1 1 (list (make-test-mtch (make-bindings null) 1 none)))
(test-empty 1 '() #f)
(test-empty 99999999999999999999999999999999999999999999999
99999999999999999999999999999999999999999999999
(list (make-test-mtch (make-bindings null)
99999999999999999999999999999999999999999999999
none)))
(test-empty 99999999999999999999999999999999999999999999999
'()
#f)
(test-empty 'x 'x (list (make-test-mtch (make-bindings null) 'x none)))
(test-empty 'x '() #f)
(test-empty 1 2 #f)
(test-empty "a" "b" #f)
(test-empty "a" '(x) #f)
(test-empty "a" '() #f)
(test-empty "a" "a" (list (make-test-mtch (make-bindings null) "a" none)))
(test-empty 'number 1 (list (make-test-mtch (make-bindings null) 1 none)))
(test-empty 'number 'x #f)
(test-empty 'number '() #f)
(test-empty 'string "a" (list (make-test-mtch (make-bindings null) "a" none)))
(test-empty 'string 1 #f)
(test-empty 'string '() #f)
(test-empty 'variable 'x (list (make-test-mtch (make-bindings null) 'x none)))
(test-empty 'variable 1 #f)
(test-empty '(variable-except x) 1 #f)
(test-empty '(variable-except x) 'x #f)
(test-empty '(variable-except x) 'y (list (make-test-mtch (make-bindings null) 'y none)))
(test-empty 'hole 1 #f)
(test-empty '(hole hole-name) 1 #f)
(test-empty '(name x number) 1 (list (make-test-mtch (make-bindings (list (make-rib 'x 1))) 1 none)))
(test-empty 'number_x 1 (list (make-test-mtch (make-bindings (list (make-rib 'number_x 1))) 1 none)))
(test-empty 'string_y "b" (list (make-test-mtch (make-bindings (list (make-rib 'string_y "b"))) "b" none)))
(test-empty 'any_z '(a b) (list (make-test-mtch (make-bindings (list (make-rib 'any_z '(a b)))) '(a b) none)))
(test-ellipses '(a) '(a))
(test-ellipses '(a ...) `(,(make-repeat 'a '())))
(test-ellipses '((a ...) ...) `(,(make-repeat '(a ...) '())))
(test-ellipses '(a ... b c ...) `(,(make-repeat 'a '()) b ,(make-repeat 'c '())))
(test-ellipses '((name x a) ...) `(,(make-repeat '(name x a) (list (make-rib 'x '())))))
(test-ellipses '((name x (a ...)) ...)
`(,(make-repeat '(name x (a ...)) (list (make-rib 'x '())))))
(test-ellipses '(((name x a) ...) ...)
`(,(make-repeat '((name x a) ...) (list (make-rib 'x '())))))
(test-ellipses '((1 (name x a)) ...)
`(,(make-repeat '(1 (name x a)) (list (make-rib 'x '())))))
(test-ellipses '((any (name x a)) ...)
`(,(make-repeat '(any (name x a)) (list (make-rib 'x '())))))
(test-ellipses '((number (name x a)) ...)
`(,(make-repeat '(number (name x a)) (list (make-rib 'x '())))))
(test-ellipses '((variable (name x a)) ...)
`(,(make-repeat '(variable (name x a)) (list (make-rib 'x '())))))
(test-ellipses '(((name x a) (name y b)) ...)
`(,(make-repeat '((name x a) (name y b)) (list (make-rib 'y '()) (make-rib 'x '())))))
(test-ellipses '((name x (name y b)) ...)
`(,(make-repeat '(name x (name y b)) (list (make-rib 'y '()) (make-rib 'x '())))))
(test-ellipses '((in-hole (name x a) (name y b)) ...)
`(,(make-repeat '(in-hole (name x a) (name y b))
(list (make-rib 'x '()) (make-rib 'y '())))))
(test-empty '() '() (list (make-test-mtch (make-bindings null) '() none)))
(test-empty '(a) '(a) (list (make-test-mtch (make-bindings null) '(a) none)))
(test-empty '(a) '(b) #f)
(test-empty '(a b) '(a b) (list (make-test-mtch (make-bindings null) '(a b) none)))
(test-empty '(a b) '(a c) #f)
(test-empty '() 1 #f)
(test-empty '(#f x) '(#f x) (list (make-test-mtch (make-bindings null) '(#f x) none)))
(test-empty '(#f (name y any)) '(#f) #f)
(test-empty '(in-hole (z hole) a) '(z a) (list (make-test-mtch (make-bindings (list)) '(z a) none)))
(test-empty '(in-hole (z hole) (in-hole (x hole) a))
'(z (x a))
(list (make-test-mtch (make-bindings (list)) '(z (x a)) none)))
(test-empty '(in-named-hole h1 (z (hole h1)) a)
'(z a)
(list (make-test-mtch (make-bindings (list)) '(z a) none)))
(test-empty '(in-named-hole h1 (z (hole h1)) a) '(z a) (list (make-test-mtch (make-bindings (list)) '(z a) none)))
(test-empty '(in-named-hole c (any (hole c)) y)
'(x y)
(list (make-test-mtch (make-bindings (list)) '(x y) none)))
(test-empty '(in-named-hole a (in-named-hole b (x (hole b)) (hole a)) y)
'(x y)
(list (make-test-mtch (make-bindings (list)) '(x y) none)))
(test-empty '(in-hole (in-hole (x hole) hole) y)
'(x y)
(list (make-test-mtch (make-bindings (list)) '(x y) none)))
(test-empty '((name x number) (name x number)) '(1 1) (list (make-test-mtch (make-bindings (list (make-rib 'x 1))) '(1 1) none)))
(test-empty '((name x number) (name x number)) '(1 2) #f)
(test-empty '(a ...) '() (list (make-test-mtch (make-bindings empty) '() none)))
(test-empty '(a ...) '(a) (list (make-test-mtch (make-bindings empty) '(a) none)))
(test-empty '(a ...) '(a a) (list (make-test-mtch (make-bindings empty) '(a a) none)))
(test-empty '((name x a) ...) '() (list (make-test-mtch (make-bindings (list (make-rib 'x '()))) '() none)))
(test-empty '((name x a) ...) '(a) (list (make-test-mtch (make-bindings (list (make-rib 'x '(a)))) '(a) none)))
(test-empty '((name x a) ...) '(a a) (list (make-test-mtch (make-bindings (list (make-rib 'x '(a a)))) '(a a) none)))
(test-empty '(b ... a ...) '() (list (make-test-mtch (make-bindings empty) '() none)))
(test-empty '(b ... a ...) '(a) (list (make-test-mtch (make-bindings empty) '(a) none)))
(test-empty '(b ... a ...) '(b) (list (make-test-mtch (make-bindings empty) '(b) none)))
(test-empty '(b ... a ...) '(b a) (list (make-test-mtch (make-bindings empty) '(b a) none)))
(test-empty '(b ... a ...) '(b b a a) (list (make-test-mtch (make-bindings empty) '(b b a a) none)))
(test-empty '(b ... a ...) '(a a) (list (make-test-mtch (make-bindings empty) '(a a) none)))
(test-empty '(b ... a ...) '(b b) (list (make-test-mtch (make-bindings empty) '(b b) none)))
(test-empty '((name y b) ... (name x a) ...) '()
(list (make-test-mtch (make-bindings (list (make-rib 'x '())
(make-rib 'y '())))
'()
none)))
(test-empty '((name y b) ... (name x a) ...) '(a)
(list (make-test-mtch (make-bindings (list (make-rib 'x '(a))
(make-rib 'y '())))
'(a)
none)))
(test-empty '((name y b) ... (name x a) ...) '(b)
(list (make-test-mtch (make-bindings (list (make-rib 'x '())
(make-rib 'y '(b))))
'(b)
none)))
(test-empty '((name y b) ... (name x a) ...) '(b b a a)
(list (make-test-mtch (make-bindings (list (make-rib 'x '(a a))
(make-rib 'y '(b b))))
'(b b a a)
none)))
(test-empty '((name y a) ... (name x a) ...) '(a)
(list (make-test-mtch (make-bindings (list (make-rib 'x '())
(make-rib 'y '(a))))
'(a)
none)
(make-test-mtch (make-bindings (list (make-rib 'x '(a))
(make-rib 'y '())))
'(a)
none)))
(test-empty '((name y a) ... (name x a) ...) '(a a)
(list (make-test-mtch (make-bindings (list (make-rib 'x '())
(make-rib 'y '(a a))))
'(a a)
none)
(make-test-mtch (make-bindings (list (make-rib 'x '(a))
(make-rib 'y '(a))))
'(a a)
none)
(make-test-mtch (make-bindings (list (make-rib 'x '(a a))
(make-rib 'y '())))
'(a a)
none)))
(test-ab '(bb_y ... aa_x ...) '()
(list (make-test-mtch (make-bindings (list (make-rib 'aa_x '())
(make-rib 'bb_y '())))
'()
none)))
(test-ab '(bb_y ... aa_x ...) '(a)
(list (make-test-mtch (make-bindings (list (make-rib 'aa_x '(a))
(make-rib 'bb_y '())))
'(a)
none)))
(test-ab '(bb_y ... aa_x ...) '(b)
(list (make-test-mtch (make-bindings (list (make-rib 'aa_x '())
(make-rib 'bb_y '(b))))
'(b)
none)))
(test-ab '(bb_y ... aa_x ...) '(b b a a)
(list (make-test-mtch (make-bindings (list (make-rib 'aa_x '(a a))
(make-rib 'bb_y '(b b))))
'(b b a a)
none)))
(test-ab '(aa_y ... aa_x ...) '(a)
(list (make-test-mtch (make-bindings (list (make-rib 'aa_x '())
(make-rib 'aa_y '(a))))
'(a)
none)
(make-test-mtch (make-bindings (list (make-rib 'aa_x '(a))
(make-rib 'aa_y '())))
'(a)
none)))
(test-ab '(aa_y ... aa_x ...) '(a a)
(list (make-test-mtch (make-bindings (list (make-rib 'aa_x '())
(make-rib 'aa_y '(a a))))
'(a a)
none)
(make-test-mtch (make-bindings (list (make-rib 'aa_x '(a))
(make-rib 'aa_y '(a))))
'(a a)
none)
(make-test-mtch (make-bindings (list (make-rib 'aa_x '(a a))
(make-rib 'aa_y '())))
'(a a)
none)))
(test-empty '((name x number) ...) '(1 2) (list (make-test-mtch (make-bindings (list (make-rib 'x '(1 2)))) '(1 2) none)))
(test-empty '(a ...) '(b) #f)
(test-empty '(a ... b ...) '(c) #f)
(test-empty '(a ... b) '(b c) #f)
(test-empty '(a ... b) '(a b c) #f)
(test-xab 'lsts '() (list (make-test-mtch (make-bindings null) '() none)))
(test-xab 'lsts '(x) (list (make-test-mtch (make-bindings null) '(x) none)))
(test-xab 'lsts 'x (list (make-test-mtch (make-bindings null) 'x none)))
(test-xab 'lsts #f (list (make-test-mtch (make-bindings null) #f none)))
(test-xab 'split-out '1 (list (make-test-mtch (make-bindings null) '1 none)))
(test-xab 'exp 1 (list (make-test-mtch (make-bindings null) 1 none)))
(test-xab 'exp '(+ 1 2) (list (make-test-mtch (make-bindings null) '(+ 1 2) none)))
(test-xab '(in-hole ctxt any)
'1
(list (make-test-mtch (make-bindings (list)) 1 none)))
(test-xab '(in-hole ctxt (name x any))
'1
(list (make-test-mtch (make-bindings (list (make-rib 'x 1))) 1 none)))
(test-xab '(in-hole (name c ctxt) (name x any))
'(+ 1 2)
(list (make-test-mtch (make-bindings (list (make-rib 'c (build-context hole)) (make-rib 'x '(+ 1 2)))) '(+ 1 2) none)
(make-test-mtch (make-bindings (list (make-rib 'c (build-context `(+ ,hole 2)))
(make-rib 'x 1)))
'(+ 1 2) none)
(make-test-mtch (make-bindings (list (make-rib 'c (build-context `(+ 1 ,hole)))
(make-rib 'x 2))) '(+ 1 2) none)))
(test-xab '(in-hole (name c ctxt) (name i (+ number number)))
'(+ (+ 1 2) (+ 3 4))
(list (make-test-mtch
(make-bindings (list (make-rib 'i '(+ 1 2)) (make-rib 'c (build-context `(+ ,hole (+ 3 4))))))
'(+ (+ 1 2) (+ 3 4))
none)
(make-test-mtch (make-bindings (list (make-rib 'i '(+ 3 4)) (make-rib 'c `(+ (+ 1 2) ,hole))))
'(+ (+ 1 2) (+ 3 4))
none)))
(test-empty '(in-hole ((z hole)) (name x any))
'((z a))
(list (make-test-mtch (make-bindings (list (make-rib 'x 'a))) '((z a)) none)))
(test-empty '(in-hole (name c (z ... hole z ...)) any)
'(z z)
(list
(make-test-mtch (make-bindings (list (make-rib 'c `(z ,hole)))) '(z z) none)
(make-test-mtch (make-bindings (list (make-rib 'c `(,hole z)))) '(z z) none)))
(test-empty '(in-hole (name c (z ... hole z ...)) any)
'(z z z)
(list
(make-test-mtch (make-bindings (list (make-rib 'c `(z z ,hole)))) '(z z z) none)
(make-test-mtch (make-bindings (list (make-rib 'c `(z ,hole z)))) '(z z z) none)
(make-test-mtch (make-bindings (list (make-rib 'c `(,hole z z)))) '(z z z) none)))
(test-empty '(z (in-hole (name c (z hole)) a))
'(z (z a))
(list
(make-test-mtch (make-bindings (list (make-rib 'c `(z ,hole))))
'(z (z a))
none)))
(test-empty '(a (in-hole (name c1 (b (in-hole (name c2 (c hole)) d) hole)) e))
'(a (b (c d) e))
(list
(make-test-mtch (make-bindings (list (make-rib 'c2 `(c ,hole))
(make-rib 'c1 `(b (c d) ,hole))))
'(a (b (c d) e))
none)))
(test-empty '(in-hole (in-hole hole hole) a)
'a
(list (make-test-mtch (make-bindings (list)) 'a none)))
(test-empty '(a (b (in-hole (name c1 (in-hole (name c2 (c hole)) (d hole))) e)))
'(a (b (c (d e))))
(list
(make-test-mtch (make-bindings (list (make-rib 'c1 `(c (d ,hole)))
(make-rib 'c2 `(c ,hole))))
'(a (b (c (d e))))
none)))
(test-empty `(+ 1 (side-condition any ,(lambda (bindings) #t)))
'(+ 1 b)
(list (make-test-mtch (make-bindings '()) '(+ 1 b) none)))
(test-empty `(+ 1 (side-condition any ,(lambda (bindings) #f)))
'(+ 1 b)
#f)
(test-empty `(+ 1 (side-condition b ,(lambda (bindings) #t)))
'(+ 1 b)
(list (make-test-mtch (make-bindings '()) '(+ 1 b) none)))
(test-empty `(+ 1 (side-condition a ,(lambda (bindings) #t)))
'(+ 1 b)
#f)
(test-empty `(side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)))
'a
(list
(make-test-mtch (make-bindings (list (make-rib 'x 'a)))
'a
none)))
(test-empty `(+ 1 (side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a))))
'(+ 1 a)
(list
(make-test-mtch (make-bindings (list (make-rib 'x 'a)))
'(+ 1 a)
none)))
(test-empty `(side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)))
'b
#f)
(test-empty `(+ 1 (side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a))))
'(+ 1 b)
#f)
(test-xab 'exp_1
'(+ 1 2)
(list (make-test-mtch (make-bindings (list (make-rib 'exp_1 '(+ 1 2)))) '(+ 1 2) none)))
(test-xab '(exp_1 exp_2)
'((+ 1 2) (+ 3 4))
(list (make-test-mtch (make-bindings (list (make-rib 'exp_1 '(+ 1 2)) (make-rib 'exp_2 '(+ 3 4))))
'((+ 1 2) (+ 3 4))
none)))
(test-xab '(exp_1 exp_1)
'((+ 1 2) (+ 3 4))
#f)
(test-xab 'nesting-names
'b
(list (make-test-mtch (make-bindings (list)) 'b none)))
(test-xab 'nesting-names
'(a b)
(list (make-test-mtch (make-bindings (list)) '(a b) none)))
(test-xab 'nesting-names
'(a (a b))
(list (make-test-mtch (make-bindings (list)) '(a (a b)) none)))
(test-xab '((name x a) nesting-names)
'(a (a (a b)))
(list (make-test-mtch (make-bindings (list (make-rib 'x 'a))) '(a (a (a b))) none)))
(test-xab 'nesting-names
'(a (a (a (a b))))
(list (make-test-mtch (make-bindings (list)) '(a (a (a (a b)))) none)))
(test-xab 'same-in-nt
'(x x)
(list (make-test-mtch (make-bindings (list)) '(x x) none)))
(test-xab 'same-in-nt
'(x y)
#f)
#;
(test-xab '(in-hole ec-multi (+ number number))
'(+ 1 2)
(list (make-bindings (list (make-rib 'hole (make-hole-binding '(+ 1 2) '() #f))))))
#;
(test-xab '(in-hole ec-multi (+ number number))
'(+ 1 (+ 5 6))
(list (make-bindings (list (make-rib 'hole (make-hole-binding '(+ 5 6) '(cdr cdr car) #f))))))
#;
(test-xab '(in-hole ec-multi (+ number number))
'(+ (+ (+ 1 2) 3) 4)
(list (make-bindings (list (make-rib 'hole (make-hole-binding '(+ 1 2) '(cdr car cdr car) #f))))))
#;
(test-xab '(in-hole ec-multi (+ number number))
'(+ (+ 3 (+ 1 2)) 4)
(list (make-bindings (list (make-rib 'hole (make-hole-binding '(+ 1 2) '(cdr car cdr cdr car) #f))))))
#;
(test-xab '(in-hole ec-multi (+ number number))
'(+ (+ (+ 1 2) (+ 3 4)) (+ 5 6))
(list (make-bindings (list (make-rib 'hole (make-hole-binding '(+ 5 6) '(cdr cdr car) #f))))
(make-bindings (list (make-rib 'hole (make-hole-binding '(+ 1 2) '(cdr car cdr car) #f))))
(make-bindings (list (make-rib 'hole (make-hole-binding '(+ 3 4) '(cdr car cdr cdr car) #f))))))
(run-test
'compatible-context-language1
(build-compatible-context-language
(mk-hasheq '((exp . ()) (ctxt . ())))
(list (make-nt 'exp
(list (make-rhs '(+ exp exp))
(make-rhs 'number)))
(make-nt 'ctxt
(list (make-rhs '(+ ctxt exp))
(make-rhs '(+ exp ctxt))
(make-rhs 'hole)))))
(list
(make-nt 'exp-exp
(list (make-rhs 'hole)
(make-rhs `(+ (cross exp-exp) exp))
(make-rhs `(+ exp (cross exp-exp)))))
(make-nt 'exp-ctxt
(list (make-rhs `(+ (cross exp-ctxt) exp))
(make-rhs `(+ ctxt (cross exp-exp)))
(make-rhs `(+ (cross exp-exp) ctxt))
(make-rhs `(+ exp (cross exp-ctxt)))))
(make-nt 'ctxt-exp
(list (make-rhs `(+ (cross ctxt-exp) exp))
(make-rhs `(+ exp (cross ctxt-exp)))))
(make-nt 'ctxt-ctxt
(list (make-rhs 'hole)
(make-rhs `(+ (cross ctxt-ctxt) exp))
(make-rhs `(+ ctxt (cross ctxt-exp)))
(make-rhs `(+ (cross ctxt-exp) ctxt))
(make-rhs `(+ exp (cross ctxt-ctxt)))))))
(run-test
'compatible-context-language2
(build-compatible-context-language
(mk-hasheq '((m . ()) (v . ())))
(list (make-nt 'm (list (make-rhs '(m m)) (make-rhs '(+ m m)) (make-rhs 'v)))
(make-nt 'v (list (make-rhs 'number) (make-rhs '(lambda (x) m))))))
(list
(make-nt 'm-m
(list
(make-rhs 'hole)
(make-rhs (list (list 'cross 'm-m) 'm))
(make-rhs (list 'm (list 'cross 'm-m)))
(make-rhs (list '+ (list 'cross 'm-m) 'm))
(make-rhs (list '+ 'm (list 'cross 'm-m)))
(make-rhs (list 'cross 'm-v))))
(make-nt 'm-v (list (make-rhs (list 'lambda (list 'x) (list 'cross 'm-m)))))
(make-nt 'v-m
(list
(make-rhs (list (list 'cross 'v-m) 'm))
(make-rhs (list 'm (list 'cross 'v-m)))
(make-rhs (list '+ (list 'cross 'v-m) 'm))
(make-rhs (list '+ 'm (list 'cross 'v-m)))
(make-rhs (list 'cross 'v-v))))
(make-nt 'v-v (list (make-rhs 'hole) (make-rhs (list 'lambda (list 'x) (list 'cross 'v-m)))))))
(run-test
'compatible-context-language3
(build-compatible-context-language
(mk-hasheq '((m . ()) (seven . ())))
(list (make-nt 'm (list (make-rhs '(m seven m)) (make-rhs 'number)))
(make-nt 'seven (list (make-rhs 7)))))
`(,(make-nt
'm-m
`(,(make-rhs 'hole) ,(make-rhs `((cross m-m) seven m)) ,(make-rhs `(m (cross m-seven) m)) ,(make-rhs `(m seven (cross m-m)))))
,(make-nt 'm-seven `())
,(make-nt
'seven-m
`(,(make-rhs `((cross seven-m) seven m)) ,(make-rhs `(m (cross seven-seven) m)) ,(make-rhs `(m seven (cross seven-m)))))
,(make-nt 'seven-seven `(,(make-rhs 'hole)))))
#;
(test-xab '(in-hole (cross exp) (+ number number))
'(+ (+ 1 2) 3)
(list (make-bindings (list (make-rib 'hole (make-hole-binding (list '+ 1 2) (list 'cdr 'car) #f))))))
(unless failure?
(fprintf (current-error-port) "All ~a tests passed.\n" test-count)))
;; mk-hasheq : (listof (cons sym any)) -> hash-table
;; builds a hash table that has the bindings in assoc-list
(define (mk-hasheq assoc-list)
(let ([ht (make-hash-table)])
(for-each
(lambda (a)
(hash-table-put! ht (car a) (cdr a)))
assoc-list)
ht))
;; test-empty : sexp[pattern] sexp[term] answer -> void
;; returns #t if pat matching exp with the empty language produces ans.
(define (test-empty pat exp ans)
(run-match-test
`(match-pattern (compile-pattern (compile-language '()) ',pat) ',exp)
(match-pattern
(compile-pattern (compile-language '()) pat)
exp)
ans))
(define xab-lang #f)
;; test-xab : sexp[pattern] sexp[term] answer -> void
;; returns #t if pat matching exp with a simple language produces ans.
(define (test-xab pat exp ans)
(unless xab-lang
(set! xab-lang
(compile-language (list (make-nt 'exp
(list (make-rhs '(+ exp exp))
(make-rhs 'number)))
(make-nt 'ctxt
(list (make-rhs '(+ ctxt exp))
(make-rhs '(+ exp ctxt))
(make-rhs 'hole)))
(make-nt 'ec-multi
(list (make-rhs 'hole)
(make-rhs '(in-named-hole xx ec-one ec-multi))))
(make-nt 'ec-one
(list (make-rhs '(+ (hole xx) exp))
(make-rhs '(+ exp (hole xx)))))
(make-nt 'same-in-nt (list (make-rhs '((name x any) (name x any)))))
(make-nt 'lsts
(list (make-rhs '())
(make-rhs '(x))
(make-rhs 'x)
(make-rhs '#f)))
(make-nt 'split-out
(list (make-rhs 'split-out2)))
(make-nt 'split-out2
(list (make-rhs 'number)))
(make-nt 'nesting-names
(list (make-rhs '(a (name x nesting-names)))
(make-rhs 'b)))))))
(run-match-test
`(match-pattern (compile-pattern xab-lang ',pat) ',exp)
(match-pattern (compile-pattern xab-lang pat) exp)
ans))
(define ab-lang #f)
;; test-xab : sexp[pattern] sexp[term] answer -> void
;; returns #t if pat matching exp with a simple language produces ans.
(define (test-ab pat exp ans)
(unless ab-lang
(set! ab-lang
(compile-language (list (make-nt 'aa
(list (make-rhs 'a)))
(make-nt 'bb
(list (make-rhs 'b)))))))
(run-match-test
`(match-pattern (compile-pattern ab-lang ',pat) ',exp)
(match-pattern (compile-pattern ab-lang pat) exp)
ans))
;; test-ellipses : sexp sexp -> void
(define (test-ellipses pat expected)
(run-test
`(rewrite-ellipses ',pat (lambda (x) (values x #f)))
(let-values ([(compiled-pattern has-hole?) (rewrite-ellipses pat (lambda (x) (values x #f)))])
(cons compiled-pattern has-hole?))
(cons expected #f)))
;; run-test/cmp : sexp any any (any any -> boolean)
;; compares ans with expected. If failure,
;; prints info about the test and sets `failure?' to #t.
(define failure? #f)
(define test-count 0)
(define (run-test/cmp symbolic ans expected cmp?)
(set! test-count (+ test-count 1))
(cond
[(cmp? ans expected)
'(printf "passed: ~s\n" symbolic)]
[else
(set! failure? #t)
(fprintf (current-error-port)
" test: ~s\nexpected: ~e\n got: ~e\n"
symbolic expected ans)]))
(define (run-test symbolic ans expected) (run-test/cmp symbolic ans expected equal/bindings?))
;; run-match-test : sexp got expected
;; expects both ans and expected to be lists or both to be #f and
;; compares them using a set-like equality if they are lists
(define (run-match-test symbolic ans expected)
(run-test/cmp
symbolic ans expected
(λ (xs ys)
(cond
[(and (not xs) (not ys)) #t]
[(and (list? xs)
(list? ys))
(and (andmap (λ (x) (memf (λ (y) (equal/bindings? x y)) ys)) xs)
(andmap (λ (y) (memf (λ (x) (equal/bindings? x y)) xs)) ys))]
[else #f]))))
;; equal/bindings? : any any -> boolean
;; compares two sexps (with embedded bindings) for equality.
;; uses an order-insensitive comparison for the bindings
(define (equal/bindings? fst snd)
(let loop ([fst fst]
[snd snd])
(cond
[(pair? fst)
(and (pair? snd)
(loop (car fst) (car snd))
(loop (cdr fst) (cdr snd)))]
[(mtch? fst)
(and (mtch? snd)
(loop (mtch-bindings fst)
(mtch-bindings snd))
(let ([g1 (gensym 'run-match-test-sym)])
(equal? (plug (mtch-context fst) g1)
(plug (mtch-context snd) g1)))
(equal? (mtch-hole fst)
(mtch-hole snd)))]
[(bindings? fst)
(and (bindings? snd)
(let ([fst-table (bindings-table fst)]
[snd-table (bindings-table snd)])
(and (= (length fst-table)
(length snd-table))
(andmap
loop
(quicksort fst-table rib-lt)
(quicksort snd-table rib-lt)))))]
[(and (rib? fst)
(rib? snd)
(context? (rib-exp fst))
(context? (rib-exp snd)))
(and (equal? (rib-name fst) (rib-name snd))
(let ([g (gensym 'run-match-test-sym2)])
(equal? (plug (rib-exp fst) g)
(plug (rib-exp snd) g))))]
[else (equal? fst snd)])))
(define (build-context c)
(let loop ([c c])
(cond
[(eq? c hole) hole]
[(pair? c) (build-cons-context (loop (car c)) (loop (cdr c)))]
[(or (null? c)
(number? c)
(symbol? c))
(build-flat-context c)]
[else (error 'build-context "unknown ~s" c)])))
;; rib-lt : rib rib -> boolean
(define (rib-lt r1 r2) (string<=? (format "~s" (rib-name r1))
(format "~s" (rib-name r2))))
(test))

1145
collects/reduction-semantics/private/matcher.ss
View File

File diff suppressed because it is too large Load Diff

31
collects/reduction-semantics/private/red-sem-macro-helpers.ss
View File

@ -1,31 +0,0 @@
(module red-sem-macro-helpers mzscheme
(provide extract-names)
(require (lib "match.ss"))
(define (extract-names stx)
(let ([dup-names
(let loop ([sexp (syntax-object->datum stx)]
[names null])
(match sexp
[`(name ,(and sym (? symbol?)) ,pat)
(loop pat (cons sym names))]
[`(in-hole* ,(and sym (? symbol?)) ,pat1 ,pat2)
(loop pat1
(loop pat2
(cons sym names)))]
[`(in-hole ,pat1 ,pat2)
(loop pat1
(loop pat2
(cons 'hole names)))]
[(? list?)
(let i-loop ([sexp sexp]
[names names])
(cond
[(null? sexp) names]
[else (i-loop (cdr sexp) (loop (car sexp) names))]))]
[else names]))]
[ht (make-hash-table)])
(for-each (lambda (name) (hash-table-put! ht name #f)) dup-names)
(hash-table-map ht (lambda (x y) x)))))

120
collects/reduction-semantics/private/subst-test.ss
View File

@ -1,120 +0,0 @@
(module subst-test mzscheme
(require "../subst.ss"
(lib "match.ss"))
(define (lc-subst1 var val exp) (subst/proc var val exp lc-separate))
(define (lc-free-vars exp) (free-vars/memoize (make-hash-table) exp lc-separate))
(define (lc-rename old-name new-name exp) (alpha-rename old-name new-name exp lc-separate))
(define lc-subst2
(subst
[`(lambda ,vars ,body)
(all-vars vars)
(build (lambda (vars body) `(lambda ,vars ,body)))
(subterm vars body)]
[`(let (,l-var ,exp) ,body)
(all-vars (list l-var))
(build (lambda (l-vars exp body) `(let (,@l-vars ,exp) ,body)))
(subterm '() exp)
(subterm (list l-var) body)]
[(? symbol?) (variable)]
[(? number?) (constant)]
[`(,fun ,@(args ...))
(all-vars '())
(build (lambda (vars fun . args) `(,fun ,@args)))
(subterm '() fun)
(subterms '() args)]))
(define (lc-separate exp constant variable combine sub-piece)
(match exp
[`(lambda ,vars ,body)
(combine (lambda (vars body) `(lambda ,vars ,body))
vars
(sub-piece vars body))]
[`(let (,l-var ,exp) ,body)
(combine (lambda (l-vars exp body) `(let (,(car l-vars) ,exp) ,body))
(list l-var)
(sub-piece '() exp)
(sub-piece (list l-var) body))]
[(? symbol?) (variable (lambda (x) x) exp)]
[(? number?) (constant exp)]
[`(,fun ,@(args ...))
(apply
combine
(lambda (variables fun . args) `(,fun ,@args))
'()
(append
(list (sub-piece '() fun))
(map (lambda (x) (sub-piece '() x)) args)))]))
(define-syntax (test stx)
(syntax-case stx ()
[(_ test-exp expected)
(syntax (test test-exp expected equal?))]
[(_ test-exp expected same?)
(syntax
(let ([actual test-exp]
[expected-v expected])
;(printf "testing: ~s\n" (syntax-object->datum #'test-exp))
(unless (same? actual expected-v)
(printf " test: ~s\n expected: ~s\n got: ~s\n"
(syntax-object->datum #'test-exp)
expected-v
actual))))]))
(define (set-equal? xs ys)
(and (andmap (lambda (x) (memq x ys)) xs)
(andmap (lambda (y) (memq y xs)) ys)))
(define (lc-tests)
(tests lc-free-vars lc-subst1 lc-rename)
(tests #f lc-subst2 #f))
(define (tests free-vars subst rename)
(when free-vars
(test (free-vars 'x) '(x) set-equal?)
(test (free-vars '(lambda (x) x)) '() set-equal?)
(test (free-vars '(lambda (x) y)) '(y) set-equal?)
(test (free-vars '(let (x 1) x)) '() set-equal?)
(test (free-vars '(let (x 1) y)) '(y) set-equal?)
(test (free-vars '(let (x x) y)) '(y x) set-equal?)
(test (free-vars '(let (x 1) (y y))) '(y) set-equal?)
(test (free-vars '(lambda (y) (y y))) '() set-equal?))
(when rename
(test (rename 'x 'y 'x) 'x)
(test (rename 'x 'y '(lambda (x) x)) '(lambda (y) y)))
(test (subst 'x 1 'x) 1)
(test (subst 'x 1 'y) 'y)
(test (subst 'x 1 '(lambda (x) x)) '(lambda (x) x))
(test (subst 'x 1 '(lambda (y) x)) '(lambda (y) 1))
(test (subst 'x 'y '(lambda (y) x)) '(lambda (y@) y))
(test (subst 'x 'y '(lambda (y) (x y))) '(lambda (y@) (y y@)))
(test (subst 'x 'y '(let (x 1) 1)) '(let (x 1) 1))
(test (subst 'x 'y '(let (x 1) x)) '(let (x 1) x))
(test (subst 'x 'y '(let (x 1) y)) '(let (x 1) y))
(test (subst 'x 'y '(let (y 1) (x y))) '(let (y@ 1) (y y@)))
(test (subst 'q '(lambda (x) y) '(lambda (y) y)) '(lambda (y) y))
(test (subst 'q '(lambda (x) y) '(let ([y q]) y)) '(let ([y (lambda (x) y)]) y))
(test (subst 'p '1 '(let (t 2) ((p t) t)))
'(let (t 2) ((1 t) t)))
(test (subst 'p '(lambda (s) s)
'(let (t (lambda (s) s)) ((p t) t)))
'(let (t (lambda (s) s)) (((lambda (s) s) t) t)))
(test (subst 'p
'(lambda (s) (s s))
'(let (t (lambda (s) s))
p))
'(let (t (lambda (s) s))
(lambda (s) (s s))))
(test (subst 's
'(lambda (z) (s z))
'(lambda (s) (lambda (z) (s z))))
'(lambda (s) (lambda (z) (s z))))
(test (subst 's
'(lambda (s) (lambda (z) (s z)))
'(lambda (z) (s z)))
'(lambda (z) ((lambda (s) (lambda (z) (s z))) z)))))

54
collects/reduction-semantics/private/term.ss
View File

@ -1,54 +0,0 @@
(module term mzscheme
(require "matcher.ss")
(provide term term-let)
(define-syntax (term orig-stx)
(define (rewrite stx)
(let loop ([stx stx])
(syntax-case stx (unquote unquote-splicing in-hole)
[(unquote x)
(with-syntax ([x-rewrite (loop (syntax x))])
(syntax (unsyntax x-rewrite)))]
[(unquote . x)
(raise-syntax-error 'term "malformed unquote" orig-stx stx)]
[(unquote-splicing x)
(with-syntax ([x-rewrite (loop (syntax x))])
(syntax (unsyntax-splicing x-rewrite)))]
[(unquote-splicing . x)
(raise-syntax-error 'term "malformed unquote splicing" orig-stx stx)]
[(in-hole id body)
(and (identifier? (syntax id))
(identifier? (syntax hole)))
(syntax (unsyntax (plug (term id) (term body))))]
[(in-hole . x)
(raise-syntax-error 'term "malformed in-hole" orig-stx stx)]
[(x ...)
(with-syntax ([(x-rewrite ...) (map loop (syntax->list (syntax (x ...))))])
(syntax (x-rewrite ...)))]
[_ stx])))
(syntax-case orig-stx ()
[(_ arg)
(with-syntax ([rewritten (rewrite (syntax arg))])
(syntax (syntax-object->datum (quasisyntax rewritten))))]))
(define-syntax (term-let stx)
(syntax-case stx ()
[(_ ([x rhs] ...) body1 body2 ...)
(syntax
(with-syntax ([x rhs] ...)
(begin body1 body2 ...)))]
[(_ x)
(raise-syntax-error 'term-let "expected at least one body" stx)]))
#|
(define (test stx exp)
(unless (equal? (eval stx) exp)
(error 'test "~s" (syntax-object->datum stx))))
(test (quote-syntax (term 1)) 1)
(test (quote-syntax (term (1 2))) (list 1 2))
(test (quote-syntax (term (1 ,(+ 1 1)))) (list 1 2))
(test (quote-syntax (term-let ([x 1]) (term (x x)))) (list 1 1))
(test (quote-syntax (term-let ([(x ...) (list 1 2 3)]) (term ((y x) ...)))) '((y 1) (y 2) (y 3)))
|#
)

317
collects/reduction-semantics/reduction-semantics.ss
View File

@ -1,317 +0,0 @@
#|
incompatible changes to be done:
- make contexts be bound to just the context to avoid a separate `hole' thingy
|#
(module reduction-semantics mzscheme
(require "private/matcher.ss"
"private/term.ss"
(lib "contract.ss")
(lib "etc.ss"))
(require-for-syntax (lib "list.ss"))
;; type red = (make-red compiled-pat ((listof (cons sym tst) (union string #f)) -> any)
(define-struct red (contractum reduct name))
(provide reduction
reduction/name
reduction/context
reduction/context/name
language
plug
compiled-lang?
red?
term
term-let
none?
(rename red-name reduction->name))
(provide match-pattern
compile-pattern
make-bindings bindings-table bindings?
mtch? mtch-bindings mtch-context mtch-hole
make-rib rib? rib-name rib-exp)
(provide/contract
(language->predicate (compiled-lang? symbol? . -> . (any/c . -> . boolean?)))
(reduce ((listof (lambda (x) (red? x))) any/c . -> . (listof any/c)))
(reduce/tag-with-reduction ((listof (lambda (x) (red? x))) any/c . -> . (listof any/c)))
(give-name ((λ (x) (red? x)) string? . -> . red?))
(variable-not-in (any/c symbol? . -> . symbol?))
(compatible-closure ((lambda (x) (red? x))
compiled-lang?
symbol?
. -> .
(lambda (x) (red? x))))
(context-closure ((lambda (x) (red? x))
compiled-lang?
any/c
. -> .
(lambda (x) (red? x)))))
;; give-name : red (union string #f) -> red
;; gives the reduction the given name
(define (give-name red name) (make-red (red-contractum red) (red-reduct red) name))
;; build-red : language pattern ((listof (cons sym tst)) -> any) (union string #f) -> red
(define (build-red lang contractum reduct name)
(make-red (compile-pattern lang contractum) reduct name))
(define (compatible-closure red lang nt)
(context-closure red lang `(cross ,nt)))
(define (context-closure red lang pattern)
(let ([new-name (gensym 'context-closure)])
(make-red (compile-pattern
lang
`(in-hole (name ,new-name ,pattern)
,(red-contractum red)))
(lambda (bindings)
(let ([context (lookup-binding bindings new-name)]
[res ((red-reduct red) bindings)])
(plug context res)))
#f)))
(define-syntax-set (reduction/context reduction reduction/name reduction/context/name language)
;; (reduction/context lang ctxt pattern expression ...)
(define (reduction/context/proc stx)
(syntax-case stx ()
[(_ lang-exp ctxt pattern bodies ...)
(let-values ([(names names/ellipses) (extract-names (syntax pattern))])
(when (null? (syntax->list (syntax (bodies ...))))
(raise-syntax-error #f "missing result expression" stx))
(with-syntax ([(names ...) names]
[(names/ellipses ...) names/ellipses]
[side-condition-rewritten (rewrite-side-conditions (syntax pattern))])
(syntax
(build-red lang-exp
`(in-hole (name context ctxt) side-condition-rewritten)
(lambda (bindings)
(term-let ([context (lookup-binding bindings 'context)]
[names/ellipses (lookup-binding bindings 'names)] ...)
(plug
(term context)
(begin
(void)
bodies ...))))
#f))))]))
(define (reduction/context/name/proc stx)
(syntax-case stx ()
[(_ name-exp lang-exp ctxt pattern bodies ...)
#'(give-name (reduction/context lang-exp ctxt pattern bodies ...)
name-exp)]))
;; (reduction lang pattern expression ...)
(define (reduction/proc stx)
(syntax-case stx ()
[(_ lang-exp pattern bodies ...)
(let-values ([(names names/ellipses) (extract-names (syntax pattern))])
(when (null? (syntax->list (syntax (bodies ...))))
(raise-syntax-error #f "missing result expression" stx))
(with-syntax ([(name-ellipses ...) names/ellipses]
[(name ...) names]
[side-condition-rewritten (rewrite-side-conditions (syntax pattern))])
(syntax
(build-red lang-exp
`side-condition-rewritten
(lambda (bindings)
(term-let ([name-ellipses (lookup-binding bindings 'name)] ...)
bodies ...))
#f))))]))
(define (reduction/name/proc stx)
(syntax-case stx ()
[(_ name-exp lang-exp pattern bodies ...)
#`(give-name (reduction lang-exp pattern bodies ...) name-exp)]))
(define (language/proc stx)
(syntax-case stx ()
[(_ (name rhs ...) ...)
(andmap identifier? (syntax->list (syntax/loc stx (name ...))))
(with-syntax ([((r-rhs ...) ...) (map (lambda (rhss) (map rewrite-side-conditions (syntax->list rhss)))
(syntax->list (syntax ((rhs ...) ...))))])
(syntax/loc stx
(compile-language (list (make-nt 'name (list (make-rhs `r-rhs) ...)) ...))))]
[(_ (name rhs ...) ...)
(for-each
(lambda (name)
(unless (identifier? name)
(raise-syntax-error 'language "expected name" stx name)))
(syntax->list (syntax (name ...))))]
[(_ x ...)
(for-each
(lambda (x)
(syntax-case x ()
[(name rhs ...)
(void)]
[_
(raise-syntax-error 'language "malformed non-terminal" stx x)]))
(syntax->list (syntax (x ...))))]))
(define (rewrite-side-conditions orig-stx)
(let loop ([term orig-stx])
(syntax-case term (side-condition)
[(side-condition pat exp)
(let-values ([(names names/ellipses) (extract-names (syntax pat))])
(with-syntax ([(name ...) names]
[(name/ellipses ...) names/ellipses])
(syntax/loc term
(side-condition
pat
,(lambda (bindings)
(term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
exp))))))]
[(terms ...)
(map loop (syntax->list (syntax (terms ...))))]
[else term])))
(define-struct id/depth (id depth))
;; extract-names : syntax -> (values (listof syntax) (listof syntax[x | (x ...) | ((x ...) ...) | ...]))
(define (extract-names orig-stx)
(let* ([dups
(let loop ([stx orig-stx]
[names null]
[depth 0])
(syntax-case stx (name in-hole in-named-hole side-condition)
[(name sym pat)
(identifier? (syntax sym))
(loop (syntax pat)
(cons (make-id/depth (syntax sym) depth) names)
depth)]
[(in-named-hole hlnm sym pat1 pat2)
(identifier? (syntax sym))
(loop (syntax pat1)
(loop (syntax pat2) names depth)
depth)]
[(in-hole pat1 pat2)
(loop (syntax pat1)
(loop (syntax pat2) names depth)
depth)]
[(side-condition pat e)
(loop (syntax pat) names depth)]
[(pat ...)
(let i-loop ([pats (syntax->list (syntax (pat ...)))]
[names names])
(cond
[(null? pats) names]
[else
(if (or (null? (cdr pats))
(not (identifier? (cadr pats)))
(not (module-identifier=? (quote-syntax ...)
(cadr pats))))
(i-loop (cdr pats)
(loop (car pats) names depth))
(i-loop (cdr pats)
(loop (car pats) names (+ depth 1))))]))]
[x
(and (identifier? (syntax x))
(has-underscore? (syntax x)))
(cons (make-id/depth (syntax x) depth) names)]
[else names]))]
[no-dups (filter-duplicates dups)])
(values (map id/depth-id no-dups)
(map build-dots no-dups))))
;; build-dots : id/depth -> syntax[x | (x ...) | ((x ...) ...) | ...]
(define (build-dots id/depth)
(let loop ([depth (id/depth-depth id/depth)])
(cond
[(zero? depth) (id/depth-id id/depth)]
[else (with-syntax ([rest (loop (- depth 1))]
[dots (quote-syntax ...)])
(syntax (rest dots)))])))
(define (has-underscore? x)
(memq #\_ (string->list (symbol->string (syntax-e x)))))
(define (filter-duplicates dups)
(let loop ([dups dups])
(cond
[(null? dups) null]
[else
(cons
(car dups)
(filter (lambda (x)
(let ([same-id? (module-identifier=? (id/depth-id x)
(id/depth-id (car dups)))])
(when same-id?
(unless (equal? (id/depth-depth x)
(id/depth-depth (car dups)))
(error 'reduction "found the same binder, ~s, at different depths, ~a and ~a"
(syntax-object->datum (id/depth-id x))
(id/depth-depth x)
(id/depth-depth (car dups)))))
(not same-id?)))
(loop (cdr dups))))]))))
(define (language->predicate lang id)
(let ([p (compile-pattern lang id)])
(lambda (x)
(and (match-pattern p x) #t))))
;; reduce : (listof red) exp -> (listof exp)
(define (reduce reductions exp)
(reduce/internal reductions exp (λ (red) (λ (mtch) ((red-reduct red) (mtch-bindings mtch))))))
; reduce/tag-with-reductions : (listof red) exp -> (listof (list red exp))
(define (reduce/tag-with-reduction reductions exp)
(reduce/internal reductions exp (λ (red) (λ (mtch) (list red ((red-reduct red) (mtch-bindings mtch)))))))
; reduce/internal : (listof red) exp (red -> match -> X) -> listof X
(define (reduce/internal reductions exp f)
(let loop ([reductions reductions]
[acc null])
(cond
[(null? reductions) acc]
[else (let ([red (car reductions)])
(let ([mtchs (match-pattern (red-contractum red) exp)])
(if mtchs
(loop (cdr reductions)
(map/mt
(f red)
mtchs
acc))
(loop (cdr reductions) acc))))])))
;; map/mt : (a -> b) (listof a) (listof b) -> (listof b)
;; map/mt is like map, except it uses the last argument
;; instaed of the empty list
(define (map/mt f l mt-l)
(let loop ([l l])
(cond
[(null? l) mt-l]
[else (cons (f (car l)) (loop (cdr l)))])))
(define re:gen-d #rx".*[^0-9]([0-9]+)$")
(define (variable-not-in sexp var)
(let* ([var-str (symbol->string var)]
[nums (let loop ([sexp sexp]
[nums null])
(cond
[(pair? sexp) (loop (cdr sexp) (loop (car sexp) nums))]
[(symbol? sexp) (let* ([str (symbol->string sexp)]
[match (regexp-match re:gen-d str)])
(if (and match
(is-prefix? var-str str))
(cons (string->number (cadr match)) nums)
nums))]
[else nums]))])
(if (null? nums)
(string->symbol (format "~a1" var))
(string->symbol (format "~a~a" var (+ 1 (apply max nums)))))))
(define (is-prefix? str1 str2)
(and (<= (string-length str1) (string-length str2))
(equal? str1 (substring str2 0 (string-length str1))))))

292
collects/reduction-semantics/subst.ss
View File

@ -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)
"@"))))