mirror of
https://git.savannah.gnu.org/git/guile.git
synced 2025-04-30 03:40:34 +02:00
Import GC benchmarks from Larceny, by Hansen, Clinger, et al.
These GPLv2+-licensed GC benchmarks are available from http://www.ccs.neu.edu/home/will/GC/sourcecode.html .
This commit is contained in:
Ludovic Courtès
parent
b777f3b64c
commit
c1d1d8247c
21 changed files with 89532 additions and 0 deletions
340
gc-benchmarks/larceny/GPL
Normal file
340
gc-benchmarks/larceny/GPL
Normal file
|
|
@ -0,0 +1,340 @@
|
||||||
|
GNU GENERAL PUBLIC LICENSE
|
||||||
|
Version 2, June 1991
|
||||||
|
|
||||||
|
Copyright (C) 1989, 1991 Free Software Foundation, Inc.
|
||||||
|
59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
|
||||||
|
Everyone is permitted to copy and distribute verbatim copies
|
||||||
|
of this license document, but changing it is not allowed.
|
||||||
|
|
||||||
|
Preamble
|
||||||
|
|
||||||
|
The licenses for most software are designed to take away your
|
||||||
|
freedom to share and change it. By contrast, the GNU General Public
|
||||||
|
License is intended to guarantee your freedom to share and change free
|
||||||
|
software--to make sure the software is free for all its users. This
|
||||||
|
General Public License applies to most of the Free Software
|
||||||
|
Foundation's software and to any other program whose authors commit to
|
||||||
|
using it. (Some other Free Software Foundation software is covered by
|
||||||
|
the GNU Library General Public License instead.) You can apply it to
|
||||||
|
your programs, too.
|
||||||
|
|
||||||
|
When we speak of free software, we are referring to freedom, not
|
||||||
|
price. Our General Public Licenses are designed to make sure that you
|
||||||
|
have the freedom to distribute copies of free software (and charge for
|
||||||
|
this service if you wish), that you receive source code or can get it
|
||||||
|
if you want it, that you can change the software or use pieces of it
|
||||||
|
in new free programs; and that you know you can do these things.
|
||||||
|
|
||||||
|
To protect your rights, we need to make restrictions that forbid
|
||||||
|
anyone to deny you these rights or to ask you to surrender the rights.
|
||||||
|
These restrictions translate to certain responsibilities for you if you
|
||||||
|
distribute copies of the software, or if you modify it.
|
||||||
|
|
||||||
|
For example, if you distribute copies of such a program, whether
|
||||||
|
gratis or for a fee, you must give the recipients all the rights that
|
||||||
|
you have. You must make sure that they, too, receive or can get the
|
||||||
|
source code. And you must show them these terms so they know their
|
||||||
|
rights.
|
||||||
|
|
||||||
|
We protect your rights with two steps: (1) copyright the software, and
|
||||||
|
(2) offer you this license which gives you legal permission to copy,
|
||||||
|
distribute and/or modify the software.
|
||||||
|
|
||||||
|
Also, for each author's protection and ours, we want to make certain
|
||||||
|
that everyone understands that there is no warranty for this free
|
||||||
|
software. If the software is modified by someone else and passed on, we
|
||||||
|
want its recipients to know that what they have is not the original, so
|
||||||
|
that any problems introduced by others will not reflect on the original
|
||||||
|
authors' reputations.
|
||||||
|
|
||||||
|
Finally, any free program is threatened constantly by software
|
||||||
|
patents. We wish to avoid the danger that redistributors of a free
|
||||||
|
program will individually obtain patent licenses, in effect making the
|
||||||
|
program proprietary. To prevent this, we have made it clear that any
|
||||||
|
patent must be licensed for everyone's free use or not licensed at all.
|
||||||
|
|
||||||
|
The precise terms and conditions for copying, distribution and
|
||||||
|
modification follow.
|
||||||
|
|
||||||
|
GNU GENERAL PUBLIC LICENSE
|
||||||
|
TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
|
||||||
|
|
||||||
|
0. This License applies to any program or other work which contains
|
||||||
|
a notice placed by the copyright holder saying it may be distributed
|
||||||
|
under the terms of this General Public License. The "Program", below,
|
||||||
|
refers to any such program or work, and a "work based on the Program"
|
||||||
|
means either the Program or any derivative work under copyright law:
|
||||||
|
that is to say, a work containing the Program or a portion of it,
|
||||||
|
either verbatim or with modifications and/or translated into another
|
||||||
|
language. (Hereinafter, translation is included without limitation in
|
||||||
|
the term "modification".) Each licensee is addressed as "you".
|
||||||
|
|
||||||
|
Activities other than copying, distribution and modification are not
|
||||||
|
covered by this License; they are outside its scope. The act of
|
||||||
|
running the Program is not restricted, and the output from the Program
|
||||||
|
is covered only if its contents constitute a work based on the
|
||||||
|
Program (independent of having been made by running the Program).
|
||||||
|
Whether that is true depends on what the Program does.
|
||||||
|
|
||||||
|
1. You may copy and distribute verbatim copies of the Program's
|
||||||
|
source code as you receive it, in any medium, provided that you
|
||||||
|
conspicuously and appropriately publish on each copy an appropriate
|
||||||
|
copyright notice and disclaimer of warranty; keep intact all the
|
||||||
|
notices that refer to this License and to the absence of any warranty;
|
||||||
|
and give any other recipients of the Program a copy of this License
|
||||||
|
along with the Program.
|
||||||
|
|
||||||
|
You may charge a fee for the physical act of transferring a copy, and
|
||||||
|
you may at your option offer warranty protection in exchange for a fee.
|
||||||
|
|
||||||
|
2. You may modify your copy or copies of the Program or any portion
|
||||||
|
of it, thus forming a work based on the Program, and copy and
|
||||||
|
distribute such modifications or work under the terms of Section 1
|
||||||
|
above, provided that you also meet all of these conditions:
|
||||||
|
|
||||||
|
a) You must cause the modified files to carry prominent notices
|
||||||
|
stating that you changed the files and the date of any change.
|
||||||
|
|
||||||
|
b) You must cause any work that you distribute or publish, that in
|
||||||
|
whole or in part contains or is derived from the Program or any
|
||||||
|
part thereof, to be licensed as a whole at no charge to all third
|
||||||
|
parties under the terms of this License.
|
||||||
|
|
||||||
|
c) If the modified program normally reads commands interactively
|
||||||
|
when run, you must cause it, when started running for such
|
||||||
|
interactive use in the most ordinary way, to print or display an
|
||||||
|
announcement including an appropriate copyright notice and a
|
||||||
|
notice that there is no warranty (or else, saying that you provide
|
||||||
|
a warranty) and that users may redistribute the program under
|
||||||
|
these conditions, and telling the user how to view a copy of this
|
||||||
|
License. (Exception: if the Program itself is interactive but
|
||||||
|
does not normally print such an announcement, your work based on
|
||||||
|
the Program is not required to print an announcement.)
|
||||||
|
|
||||||
|
These requirements apply to the modified work as a whole. If
|
||||||
|
identifiable sections of that work are not derived from the Program,
|
||||||
|
and can be reasonably considered independent and separate works in
|
||||||
|
themselves, then this License, and its terms, do not apply to those
|
||||||
|
sections when you distribute them as separate works. But when you
|
||||||
|
distribute the same sections as part of a whole which is a work based
|
||||||
|
on the Program, the distribution of the whole must be on the terms of
|
||||||
|
this License, whose permissions for other licensees extend to the
|
||||||
|
entire whole, and thus to each and every part regardless of who wrote it.
|
||||||
|
|
||||||
|
Thus, it is not the intent of this section to claim rights or contest
|
||||||
|
your rights to work written entirely by you; rather, the intent is to
|
||||||
|
exercise the right to control the distribution of derivative or
|
||||||
|
collective works based on the Program.
|
||||||
|
|
||||||
|
In addition, mere aggregation of another work not based on the Program
|
||||||
|
with the Program (or with a work based on the Program) on a volume of
|
||||||
|
a storage or distribution medium does not bring the other work under
|
||||||
|
the scope of this License.
|
||||||
|
|
||||||
|
3. You may copy and distribute the Program (or a work based on it,
|
||||||
|
under Section 2) in object code or executable form under the terms of
|
||||||
|
Sections 1 and 2 above provided that you also do one of the following:
|
||||||
|
|
||||||
|
a) Accompany it with the complete corresponding machine-readable
|
||||||
|
source code, which must be distributed under the terms of Sections
|
||||||
|
1 and 2 above on a medium customarily used for software interchange; or,
|
||||||
|
|
||||||
|
b) Accompany it with a written offer, valid for at least three
|
||||||
|
years, to give any third party, for a charge no more than your
|
||||||
|
cost of physically performing source distribution, a complete
|
||||||
|
machine-readable copy of the corresponding source code, to be
|
||||||
|
distributed under the terms of Sections 1 and 2 above on a medium
|
||||||
|
customarily used for software interchange; or,
|
||||||
|
|
||||||
|
c) Accompany it with the information you received as to the offer
|
||||||
|
to distribute corresponding source code. (This alternative is
|
||||||
|
allowed only for noncommercial distribution and only if you
|
||||||
|
received the program in object code or executable form with such
|
||||||
|
an offer, in accord with Subsection b above.)
|
||||||
|
|
||||||
|
The source code for a work means the preferred form of the work for
|
||||||
|
making modifications to it. For an executable work, complete source
|
||||||
|
code means all the source code for all modules it contains, plus any
|
||||||
|
associated interface definition files, plus the scripts used to
|
||||||
|
control compilation and installation of the executable. However, as a
|
||||||
|
special exception, the source code distributed need not include
|
||||||
|
anything that is normally distributed (in either source or binary
|
||||||
|
form) with the major components (compiler, kernel, and so on) of the
|
||||||
|
operating system on which the executable runs, unless that component
|
||||||
|
itself accompanies the executable.
|
||||||
|
|
||||||
|
If distribution of executable or object code is made by offering
|
||||||
|
access to copy from a designated place, then offering equivalent
|
||||||
|
access to copy the source code from the same place counts as
|
||||||
|
distribution of the source code, even though third parties are not
|
||||||
|
compelled to copy the source along with the object code.
|
||||||
|
|
||||||
|
4. You may not copy, modify, sublicense, or distribute the Program
|
||||||
|
except as expressly provided under this License. Any attempt
|
||||||
|
otherwise to copy, modify, sublicense or distribute the Program is
|
||||||
|
void, and will automatically terminate your rights under this License.
|
||||||
|
However, parties who have received copies, or rights, from you under
|
||||||
|
this License will not have their licenses terminated so long as such
|
||||||
|
parties remain in full compliance.
|
||||||
|
|
||||||
|
5. You are not required to accept this License, since you have not
|
||||||
|
signed it. However, nothing else grants you permission to modify or
|
||||||
|
distribute the Program or its derivative works. These actions are
|
||||||
|
prohibited by law if you do not accept this License. Therefore, by
|
||||||
|
modifying or distributing the Program (or any work based on the
|
||||||
|
Program), you indicate your acceptance of this License to do so, and
|
||||||
|
all its terms and conditions for copying, distributing or modifying
|
||||||
|
the Program or works based on it.
|
||||||
|
|
||||||
|
6. Each time you redistribute the Program (or any work based on the
|
||||||
|
Program), the recipient automatically receives a license from the
|
||||||
|
original licensor to copy, distribute or modify the Program subject to
|
||||||
|
these terms and conditions. You may not impose any further
|
||||||
|
restrictions on the recipients' exercise of the rights granted herein.
|
||||||
|
You are not responsible for enforcing compliance by third parties to
|
||||||
|
this License.
|
||||||
|
|
||||||
|
7. If, as a consequence of a court judgment or allegation of patent
|
||||||
|
infringement or for any other reason (not limited to patent issues),
|
||||||
|
conditions are imposed on you (whether by court order, agreement or
|
||||||
|
otherwise) that contradict the conditions of this License, they do not
|
||||||
|
excuse you from the conditions of this License. If you cannot
|
||||||
|
distribute so as to satisfy simultaneously your obligations under this
|
||||||
|
License and any other pertinent obligations, then as a consequence you
|
||||||
|
may not distribute the Program at all. For example, if a patent
|
||||||
|
license would not permit royalty-free redistribution of the Program by
|
||||||
|
all those who receive copies directly or indirectly through you, then
|
||||||
|
the only way you could satisfy both it and this License would be to
|
||||||
|
refrain entirely from distribution of the Program.
|
||||||
|
|
||||||
|
If any portion of this section is held invalid or unenforceable under
|
||||||
|
any particular circumstance, the balance of the section is intended to
|
||||||
|
apply and the section as a whole is intended to apply in other
|
||||||
|
circumstances.
|
||||||
|
|
||||||
|
It is not the purpose of this section to induce you to infringe any
|
||||||
|
patents or other property right claims or to contest validity of any
|
||||||
|
such claims; this section has the sole purpose of protecting the
|
||||||
|
integrity of the free software distribution system, which is
|
||||||
|
implemented by public license practices. Many people have made
|
||||||
|
generous contributions to the wide range of software distributed
|
||||||
|
through that system in reliance on consistent application of that
|
||||||
|
system; it is up to the author/donor to decide if he or she is willing
|
||||||
|
to distribute software through any other system and a licensee cannot
|
||||||
|
impose that choice.
|
||||||
|
|
||||||
|
This section is intended to make thoroughly clear what is believed to
|
||||||
|
be a consequence of the rest of this License.
|
||||||
|
|
||||||
|
8. If the distribution and/or use of the Program is restricted in
|
||||||
|
certain countries either by patents or by copyrighted interfaces, the
|
||||||
|
original copyright holder who places the Program under this License
|
||||||
|
may add an explicit geographical distribution limitation excluding
|
||||||
|
those countries, so that distribution is permitted only in or among
|
||||||
|
countries not thus excluded. In such case, this License incorporates
|
||||||
|
the limitation as if written in the body of this License.
|
||||||
|
|
||||||
|
9. The Free Software Foundation may publish revised and/or new versions
|
||||||
|
of the General Public License from time to time. Such new versions will
|
||||||
|
be similar in spirit to the present version, but may differ in detail to
|
||||||
|
address new problems or concerns.
|
||||||
|
|
||||||
|
Each version is given a distinguishing version number. If the Program
|
||||||
|
specifies a version number of this License which applies to it and "any
|
||||||
|
later version", you have the option of following the terms and conditions
|
||||||
|
either of that version or of any later version published by the Free
|
||||||
|
Software Foundation. If the Program does not specify a version number of
|
||||||
|
this License, you may choose any version ever published by the Free Software
|
||||||
|
Foundation.
|
||||||
|
|
||||||
|
10. If you wish to incorporate parts of the Program into other free
|
||||||
|
programs whose distribution conditions are different, write to the author
|
||||||
|
to ask for permission. For software which is copyrighted by the Free
|
||||||
|
Software Foundation, write to the Free Software Foundation; we sometimes
|
||||||
|
make exceptions for this. Our decision will be guided by the two goals
|
||||||
|
of preserving the free status of all derivatives of our free software and
|
||||||
|
of promoting the sharing and reuse of software generally.
|
||||||
|
|
||||||
|
NO WARRANTY
|
||||||
|
|
||||||
|
11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY
|
||||||
|
FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN
|
||||||
|
OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES
|
||||||
|
PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED
|
||||||
|
OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
|
||||||
|
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS
|
||||||
|
TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE
|
||||||
|
PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,
|
||||||
|
REPAIR OR CORRECTION.
|
||||||
|
|
||||||
|
12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
|
||||||
|
WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR
|
||||||
|
REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,
|
||||||
|
INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING
|
||||||
|
OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED
|
||||||
|
TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY
|
||||||
|
YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER
|
||||||
|
PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE
|
||||||
|
POSSIBILITY OF SUCH DAMAGES.
|
||||||
|
|
||||||
|
END OF TERMS AND CONDITIONS
|
||||||
|
|
||||||
|
How to Apply These Terms to Your New Programs
|
||||||
|
|
||||||
|
If you develop a new program, and you want it to be of the greatest
|
||||||
|
possible use to the public, the best way to achieve this is to make it
|
||||||
|
free software which everyone can redistribute and change under these terms.
|
||||||
|
|
||||||
|
To do so, attach the following notices to the program. It is safest
|
||||||
|
to attach them to the start of each source file to most effectively
|
||||||
|
convey the exclusion of warranty; and each file should have at least
|
||||||
|
the "copyright" line and a pointer to where the full notice is found.
|
||||||
|
|
||||||
|
<one line to give the program's name and a brief idea of what it does.>
|
||||||
|
Copyright (C) <year> <name of author>
|
||||||
|
|
||||||
|
This program is free software; you can redistribute it and/or modify
|
||||||
|
it under the terms of the GNU General Public License as published by
|
||||||
|
the Free Software Foundation; either version 2 of the License, or
|
||||||
|
(at your option) any later version.
|
||||||
|
|
||||||
|
This program is distributed in the hope that it will be useful,
|
||||||
|
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||||
|
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||||
|
GNU General Public License for more details.
|
||||||
|
|
||||||
|
You should have received a copy of the GNU General Public License
|
||||||
|
along with this program; if not, write to the Free Software
|
||||||
|
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
|
||||||
|
|
||||||
|
|
||||||
|
Also add information on how to contact you by electronic and paper mail.
|
||||||
|
|
||||||
|
If the program is interactive, make it output a short notice like this
|
||||||
|
when it starts in an interactive mode:
|
||||||
|
|
||||||
|
Gnomovision version 69, Copyright (C) year name of author
|
||||||
|
Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
|
||||||
|
This is free software, and you are welcome to redistribute it
|
||||||
|
under certain conditions; type `show c' for details.
|
||||||
|
|
||||||
|
The hypothetical commands `show w' and `show c' should show the appropriate
|
||||||
|
parts of the General Public License. Of course, the commands you use may
|
||||||
|
be called something other than `show w' and `show c'; they could even be
|
||||||
|
mouse-clicks or menu items--whatever suits your program.
|
||||||
|
|
||||||
|
You should also get your employer (if you work as a programmer) or your
|
||||||
|
school, if any, to sign a "copyright disclaimer" for the program, if
|
||||||
|
necessary. Here is a sample; alter the names:
|
||||||
|
|
||||||
|
Yoyodyne, Inc., hereby disclaims all copyright interest in the program
|
||||||
|
`Gnomovision' (which makes passes at compilers) written by James Hacker.
|
||||||
|
|
||||||
|
<signature of Ty Coon>, 1 April 1989
|
||||||
|
Ty Coon, President of Vice
|
||||||
|
|
||||||
|
This General Public License does not permit incorporating your program into
|
||||||
|
proprietary programs. If your program is a subroutine library, you may
|
||||||
|
consider it more useful to permit linking proprietary applications with the
|
||||||
|
library. If this is what you want to do, use the GNU Library General
|
||||||
|
Public License instead of this License.
|
||||||
92
gc-benchmarks/larceny/README
Normal file
92
gc-benchmarks/larceny/README
Normal file
|
|
@ -0,0 +1,92 @@
|
||||||
|
Source Code for Selected GC Benchmarks
|
||||||
|
|
||||||
|
These benchmarks are derived from the benchmarks that Lars Hansen used for
|
||||||
|
his thesis on Older-first garbage collection in practice . That thesis
|
||||||
|
contains storage profiles and detailed discussion for most of these
|
||||||
|
benchmarks.
|
||||||
|
|
||||||
|
Portability
|
||||||
|
|
||||||
|
Apart from a run-benchmark procedure, most of these benchmarks are intended
|
||||||
|
to run in any R5RS-conforming implementation of Scheme. (The softscheme
|
||||||
|
benchmark is an exception.) Please report any portability problems that you
|
||||||
|
encounter.
|
||||||
|
|
||||||
|
To find the main entry point(s) of a benchmark, search for calls to
|
||||||
|
run-benchmark, which calculates and reports the run time and any other
|
||||||
|
relevant statistics. The run-benchmark procedure is
|
||||||
|
implementation-dependent; see run-benchmark.chez for an example of how to
|
||||||
|
write it.
|
||||||
|
|
||||||
|
GC Benchmarks
|
||||||
|
|
||||||
|
To obtain a gzip'ed tar file containing source code for all of the
|
||||||
|
benchmarks described below, click here .
|
||||||
|
|
||||||
|
dummy
|
||||||
|
Description: A null benchmark for testing the implementation-specific
|
||||||
|
run-benchmark procedure.
|
||||||
|
dynamic
|
||||||
|
Description: Fritz Henglein's algorithm for dynamic type inference.
|
||||||
|
Three inputs are available for this benchmark. In increasing order of
|
||||||
|
size, they are:
|
||||||
|
1. dynamic.sch, the code for the benchmark itself
|
||||||
|
2. dynamic-input-small.sch, which is macro-expanded code for the
|
||||||
|
Twobit compiler
|
||||||
|
3. dynamic-input-large.sch, which is macro-expanded code for the
|
||||||
|
Twobit compiler and SPARC assembler.
|
||||||
|
earley
|
||||||
|
Description: Earley's context-free parsing algorithm, as implemented by
|
||||||
|
Marc Feeley, given a simple ambiguous grammar, generating all the parse
|
||||||
|
trees for a short input.
|
||||||
|
gcbench
|
||||||
|
Description: A synthetic benchmark originally written in Java by John
|
||||||
|
Ellis, Pete Kovac, and Hans Boehm.
|
||||||
|
graphs
|
||||||
|
Description: Enumeration of directed graphs, possibly written by Jim
|
||||||
|
Miller. Makes heavy use of higher-order procedures.
|
||||||
|
lattice
|
||||||
|
Description: Enumeration of lattices of monotone maps between lattices,
|
||||||
|
obtained from Andrew Wright, possibly written by Wright or Jim Miller.
|
||||||
|
nboyer
|
||||||
|
Description: Bob Boyer's theorem proving benchmark, with a scaling
|
||||||
|
parameter suggested by Boyer, some bug fixes noted by Henry Baker and
|
||||||
|
ourselves, and rewritten to use a more reasonable representation for
|
||||||
|
the database (with constant-time lookups) instead of property lists
|
||||||
|
(which gave linear-time lookups for the most widely distributed form of
|
||||||
|
the boyer benchmark in Scheme).
|
||||||
|
nucleic2
|
||||||
|
Description: Marc Feeley et al's Pseudoknot benchmark, revised to use
|
||||||
|
R5RS macros instead of implementation-dependent macro systems.
|
||||||
|
perm
|
||||||
|
Description: Zaks's algorithm for generating a list of permutations.
|
||||||
|
This is a diabolical garbage collection benchmark with four parameters
|
||||||
|
M, N, K, and L. The MpermNKL benchmark allocates a queue of size K and
|
||||||
|
then performs M iterations of the following operation: Fill the queue
|
||||||
|
with individually computed copies of all permutations of a list of size
|
||||||
|
N, and then remove the oldest L copies from the queue. At the end of
|
||||||
|
each iteration, the oldest L/K of the live storage becomes garbage, and
|
||||||
|
object lifetimes are distributed uniformly between two volumes that
|
||||||
|
depend upon N, K, and L.
|
||||||
|
sboyer
|
||||||
|
Description: This is the nboyer benchmark with a small but effective
|
||||||
|
tweak: shared consing as implemented by Henry Baker.
|
||||||
|
softscheme
|
||||||
|
Description: Andrew's Wright's soft type inference for Scheme. This
|
||||||
|
software is covered by the GNU GENERAL PUBLIC LICENSE. This benchmark
|
||||||
|
is nonportable because it uses a low-level syntax definition to define
|
||||||
|
a non-hygienic defmacro construct. Requires an input file; the inputs
|
||||||
|
used with the dynamic and twobit benchmarks should be suitable.
|
||||||
|
twobit
|
||||||
|
Description: A portable version of the Twobit Scheme compiler and
|
||||||
|
Larceny's SPARC assembler, written by Will Clinger and Lars Hansen. Two
|
||||||
|
input files are provided:
|
||||||
|
1. twobit-input-short.sch, the nucleic2 benchmark stripped of
|
||||||
|
implementation-specific alternatives to its R4RS macros
|
||||||
|
2. twobit.sch, the twobit benchmark itself
|
||||||
|
twobit-smaller.sch
|
||||||
|
Description: The twobit benchmark without the SPARC assembler.
|
||||||
|
|
||||||
|
----------------------------------------------------------------------------
|
||||||
|
|
||||||
|
Last updated 4 April 2001.
|
||||||
21
gc-benchmarks/larceny/dumb.sch
Normal file
21
gc-benchmarks/larceny/dumb.sch
Normal file
|
|
@ -0,0 +1,21 @@
|
||||||
|
; Dumb benchmark to test the reporting of words marked during gc.
|
||||||
|
; Example: (foo 1000000)
|
||||||
|
|
||||||
|
(define (ballast bytes)
|
||||||
|
(do ((bytes bytes (- bytes 8))
|
||||||
|
(x '() (cons bytes x)))
|
||||||
|
((zero? bytes) x)))
|
||||||
|
|
||||||
|
(define (words-benchmark bytes0 bytes1)
|
||||||
|
(let ((x (ballast bytes0)))
|
||||||
|
(do ((bytes1 bytes1 (- bytes1 8)))
|
||||||
|
((not (positive? bytes1))
|
||||||
|
(car (last-pair x)))
|
||||||
|
(cons (car x) bytes1))))
|
||||||
|
|
||||||
|
(define (foo n)
|
||||||
|
(collect)
|
||||||
|
(display-memstats (memstats))
|
||||||
|
(run-benchmark "foo" (lambda () (words-benchmark 1000000 n)) 1)
|
||||||
|
(display-memstats (memstats)))
|
||||||
|
|
||||||
19
gc-benchmarks/larceny/dummy.sch
Normal file
19
gc-benchmarks/larceny/dummy.sch
Normal file
|
|
@ -0,0 +1,19 @@
|
||||||
|
; Dummy benchmark (for testing)
|
||||||
|
;
|
||||||
|
; $Id: dummy.sch,v 1.2 1999/07/12 18:03:37 lth Exp $
|
||||||
|
|
||||||
|
(define (dummy-benchmark . args)
|
||||||
|
(run-benchmark "dummy"
|
||||||
|
1
|
||||||
|
(lambda ()
|
||||||
|
(collect)
|
||||||
|
(display "This is the dummy benchmark!")
|
||||||
|
(newline)
|
||||||
|
(display "My arguments are: ")
|
||||||
|
(display args)
|
||||||
|
(newline)
|
||||||
|
args)
|
||||||
|
(lambda (result)
|
||||||
|
(equal? result args))))
|
||||||
|
|
||||||
|
; eof
|
||||||
2111
gc-benchmarks/larceny/dynamic-input-large.sch
Normal file
2111
gc-benchmarks/larceny/dynamic-input-large.sch
Normal file
File diff suppressed because one or more lines are too long
1201
gc-benchmarks/larceny/dynamic-input-small.sch
Normal file
1201
gc-benchmarks/larceny/dynamic-input-small.sch
Normal file
File diff suppressed because one or more lines are too long
2348
gc-benchmarks/larceny/dynamic.sch
Normal file
2348
gc-benchmarks/larceny/dynamic.sch
Normal file
File diff suppressed because it is too large
Load diff
658
gc-benchmarks/larceny/earley.sch
Normal file
658
gc-benchmarks/larceny/earley.sch
Normal file
|
|
@ -0,0 +1,658 @@
|
||||||
|
;;; EARLEY -- Earley's parser, written by Marc Feeley.
|
||||||
|
|
||||||
|
; $Id: earley.sch,v 1.2 1999/07/12 18:05:19 lth Exp $
|
||||||
|
; 990708 / lth -- changed 'main' to 'earley-benchmark'.
|
||||||
|
;
|
||||||
|
; (make-parser grammar lexer) is used to create a parser from the grammar
|
||||||
|
; description `grammar' and the lexer function `lexer'.
|
||||||
|
;
|
||||||
|
; A grammar is a list of definitions. Each definition defines a non-terminal
|
||||||
|
; by a set of rules. Thus a definition has the form: (nt rule1 rule2...).
|
||||||
|
; A given non-terminal can only be defined once. The first non-terminal
|
||||||
|
; defined is the grammar's goal. Each rule is a possibly empty list of
|
||||||
|
; non-terminals. Thus a rule has the form: (nt1 nt2...). A non-terminal
|
||||||
|
; can be any scheme value. Note that all grammar symbols are treated as
|
||||||
|
; non-terminals. This is fine though because the lexer will be outputing
|
||||||
|
; non-terminals.
|
||||||
|
;
|
||||||
|
; The lexer defines what a token is and the mapping between tokens and
|
||||||
|
; the grammar's non-terminals. It is a function of one argument, the input,
|
||||||
|
; that returns the list of tokens corresponding to the input. Each token is
|
||||||
|
; represented by a list. The first element is some `user-defined' information
|
||||||
|
; associated with the token and the rest represents the token's class(es) (as a
|
||||||
|
; list of non-terminals that this token corresponds to).
|
||||||
|
;
|
||||||
|
; The result of `make-parser' is a function that parses the single input it
|
||||||
|
; is given into the grammar's goal. The result is a `parse' which can be
|
||||||
|
; manipulated with the procedures: `parse->parsed?', `parse->trees'
|
||||||
|
; and `parse->nb-trees' (see below).
|
||||||
|
;
|
||||||
|
; Let's assume that we want a parser for the grammar
|
||||||
|
;
|
||||||
|
; S -> x = E
|
||||||
|
; E -> E + E | V
|
||||||
|
; V -> V y |
|
||||||
|
;
|
||||||
|
; and that the input to the parser is a string of characters. Also, assume we
|
||||||
|
; would like to map the characters `x', `y', `+' and `=' into the corresponding
|
||||||
|
; non-terminals in the grammar. Such a parser could be created with
|
||||||
|
;
|
||||||
|
; (make-parser
|
||||||
|
; '(
|
||||||
|
; (s (x = e))
|
||||||
|
; (e (e + e) (v))
|
||||||
|
; (v (v y) ())
|
||||||
|
; )
|
||||||
|
; (lambda (str)
|
||||||
|
; (map (lambda (char)
|
||||||
|
; (list char ; user-info = the character itself
|
||||||
|
; (case char
|
||||||
|
; ((#\x) 'x)
|
||||||
|
; ((#\y) 'y)
|
||||||
|
; ((#\+) '+)
|
||||||
|
; ((#\=) '=)
|
||||||
|
; (else (fatal-error "lexer error")))))
|
||||||
|
; (string->list str)))
|
||||||
|
; )
|
||||||
|
;
|
||||||
|
; An alternative definition (that does not check for lexical errors) is
|
||||||
|
;
|
||||||
|
; (make-parser
|
||||||
|
; '(
|
||||||
|
; (s (#\x #\= e))
|
||||||
|
; (e (e #\+ e) (v))
|
||||||
|
; (v (v #\y) ())
|
||||||
|
; )
|
||||||
|
; (lambda (str) (map (lambda (char) (list char char)) (string->list str)))
|
||||||
|
; )
|
||||||
|
;
|
||||||
|
; To help with the rest of the discussion, here are a few definitions:
|
||||||
|
;
|
||||||
|
; An input pointer (for an input of `n' tokens) is a value between 0 and `n'.
|
||||||
|
; It indicates a point between two input tokens (0 = beginning, `n' = end).
|
||||||
|
; For example, if `n' = 4, there are 5 input pointers:
|
||||||
|
;
|
||||||
|
; input token1 token2 token3 token4
|
||||||
|
; input pointers 0 1 2 3 4
|
||||||
|
;
|
||||||
|
; A configuration indicates the extent to which a given rule is parsed (this
|
||||||
|
; is the common `dot notation'). For simplicity, a configuration is
|
||||||
|
; represented as an integer, with successive configurations in the same
|
||||||
|
; rule associated with successive integers. It is assumed that the grammar
|
||||||
|
; has been extended with rules to aid scanning. These rules are of the
|
||||||
|
; form `nt ->', and there is one such rule for every non-terminal. Note
|
||||||
|
; that these rules are special because they only apply when the corresponding
|
||||||
|
; non-terminal is returned by the lexer.
|
||||||
|
;
|
||||||
|
; A configuration set is a configuration grouped with the set of input pointers
|
||||||
|
; representing where the head non-terminal of the configuration was predicted.
|
||||||
|
;
|
||||||
|
; Here are the rules and configurations for the grammar given above:
|
||||||
|
;
|
||||||
|
; S -> . \
|
||||||
|
; 0 |
|
||||||
|
; x -> . |
|
||||||
|
; 1 |
|
||||||
|
; = -> . |
|
||||||
|
; 2 |
|
||||||
|
; E -> . |
|
||||||
|
; 3 > special rules (for scanning)
|
||||||
|
; + -> . |
|
||||||
|
; 4 |
|
||||||
|
; V -> . |
|
||||||
|
; 5 |
|
||||||
|
; y -> . |
|
||||||
|
; 6 /
|
||||||
|
; S -> . x . = . E .
|
||||||
|
; 7 8 9 10
|
||||||
|
; E -> . E . + . E .
|
||||||
|
; 11 12 13 14
|
||||||
|
; E -> . V .
|
||||||
|
; 15 16
|
||||||
|
; V -> . V . y .
|
||||||
|
; 17 18 19
|
||||||
|
; V -> .
|
||||||
|
; 20
|
||||||
|
;
|
||||||
|
; Starters of the non-terminal `nt' are configurations that are leftmost
|
||||||
|
; in a non-special rule for `nt'. Enders of the non-terminal `nt' are
|
||||||
|
; configurations that are rightmost in any rule for `nt'. Predictors of the
|
||||||
|
; non-terminal `nt' are configurations that are directly to the left of `nt'
|
||||||
|
; in any rule.
|
||||||
|
;
|
||||||
|
; For the grammar given above,
|
||||||
|
;
|
||||||
|
; Starters of V = (17 20)
|
||||||
|
; Enders of V = (5 19 20)
|
||||||
|
; Predictors of V = (15 17)
|
||||||
|
|
||||||
|
(define (make-parser grammar lexer)
|
||||||
|
|
||||||
|
(define (non-terminals grammar) ; return vector of non-terminals in grammar
|
||||||
|
|
||||||
|
(define (add-nt nt nts)
|
||||||
|
(if (member nt nts) nts (cons nt nts))) ; use equal? for equality tests
|
||||||
|
|
||||||
|
(let def-loop ((defs grammar) (nts '()))
|
||||||
|
(if (pair? defs)
|
||||||
|
(let* ((def (car defs))
|
||||||
|
(head (car def)))
|
||||||
|
(let rule-loop ((rules (cdr def))
|
||||||
|
(nts (add-nt head nts)))
|
||||||
|
(if (pair? rules)
|
||||||
|
(let ((rule (car rules)))
|
||||||
|
(let loop ((l rule) (nts nts))
|
||||||
|
(if (pair? l)
|
||||||
|
(let ((nt (car l)))
|
||||||
|
(loop (cdr l) (add-nt nt nts)))
|
||||||
|
(rule-loop (cdr rules) nts))))
|
||||||
|
(def-loop (cdr defs) nts))))
|
||||||
|
(list->vector (reverse nts))))) ; goal non-terminal must be at index 0
|
||||||
|
|
||||||
|
(define (ind nt nts) ; return index of non-terminal `nt' in `nts'
|
||||||
|
(let loop ((i (- (vector-length nts) 1)))
|
||||||
|
(if (>= i 0)
|
||||||
|
(if (equal? (vector-ref nts i) nt) i (loop (- i 1)))
|
||||||
|
#f)))
|
||||||
|
|
||||||
|
(define (nb-configurations grammar) ; return nb of configurations in grammar
|
||||||
|
(let def-loop ((defs grammar) (nb-confs 0))
|
||||||
|
(if (pair? defs)
|
||||||
|
(let ((def (car defs)))
|
||||||
|
(let rule-loop ((rules (cdr def)) (nb-confs nb-confs))
|
||||||
|
(if (pair? rules)
|
||||||
|
(let ((rule (car rules)))
|
||||||
|
(let loop ((l rule) (nb-confs nb-confs))
|
||||||
|
(if (pair? l)
|
||||||
|
(loop (cdr l) (+ nb-confs 1))
|
||||||
|
(rule-loop (cdr rules) (+ nb-confs 1)))))
|
||||||
|
(def-loop (cdr defs) nb-confs))))
|
||||||
|
nb-confs)))
|
||||||
|
|
||||||
|
; First, associate a numeric identifier to every non-terminal in the
|
||||||
|
; grammar (with the goal non-terminal associated with 0).
|
||||||
|
;
|
||||||
|
; So, for the grammar given above we get:
|
||||||
|
;
|
||||||
|
; s -> 0 x -> 1 = -> 4 e ->3 + -> 4 v -> 5 y -> 6
|
||||||
|
|
||||||
|
(let* ((nts (non-terminals grammar)) ; id map = list of non-terms
|
||||||
|
(nb-nts (vector-length nts)) ; the number of non-terms
|
||||||
|
(nb-confs (+ (nb-configurations grammar) nb-nts)) ; the nb of confs
|
||||||
|
(starters (make-vector nb-nts '())) ; starters for every non-term
|
||||||
|
(enders (make-vector nb-nts '())) ; enders for every non-term
|
||||||
|
(predictors (make-vector nb-nts '())) ; predictors for every non-term
|
||||||
|
(steps (make-vector nb-confs #f)) ; what to do in a given conf
|
||||||
|
(names (make-vector nb-confs #f))) ; name of rules
|
||||||
|
|
||||||
|
(define (setup-tables grammar nts starters enders predictors steps names)
|
||||||
|
|
||||||
|
(define (add-conf conf nt nts class)
|
||||||
|
(let ((i (ind nt nts)))
|
||||||
|
(vector-set! class i (cons conf (vector-ref class i)))))
|
||||||
|
|
||||||
|
(let ((nb-nts (vector-length nts)))
|
||||||
|
|
||||||
|
(let nt-loop ((i (- nb-nts 1)))
|
||||||
|
(if (>= i 0)
|
||||||
|
(begin
|
||||||
|
(vector-set! steps i (- i nb-nts))
|
||||||
|
(vector-set! names i (list (vector-ref nts i) 0))
|
||||||
|
(vector-set! enders i (list i))
|
||||||
|
(nt-loop (- i 1)))))
|
||||||
|
|
||||||
|
(let def-loop ((defs grammar) (conf (vector-length nts)))
|
||||||
|
(if (pair? defs)
|
||||||
|
(let* ((def (car defs))
|
||||||
|
(head (car def)))
|
||||||
|
(let rule-loop ((rules (cdr def)) (conf conf) (rule-num 1))
|
||||||
|
(if (pair? rules)
|
||||||
|
(let ((rule (car rules)))
|
||||||
|
(vector-set! names conf (list head rule-num))
|
||||||
|
(add-conf conf head nts starters)
|
||||||
|
(let loop ((l rule) (conf conf))
|
||||||
|
(if (pair? l)
|
||||||
|
(let ((nt (car l)))
|
||||||
|
(vector-set! steps conf (ind nt nts))
|
||||||
|
(add-conf conf nt nts predictors)
|
||||||
|
(loop (cdr l) (+ conf 1)))
|
||||||
|
(begin
|
||||||
|
(vector-set! steps conf (- (ind head nts) nb-nts))
|
||||||
|
(add-conf conf head nts enders)
|
||||||
|
(rule-loop (cdr rules) (+ conf 1) (+ rule-num 1))))))
|
||||||
|
(def-loop (cdr defs) conf))))))))
|
||||||
|
|
||||||
|
; Now, for each non-terminal, compute the starters, enders and predictors and
|
||||||
|
; the names and steps tables.
|
||||||
|
|
||||||
|
(setup-tables grammar nts starters enders predictors steps names)
|
||||||
|
|
||||||
|
; Build the parser description
|
||||||
|
|
||||||
|
(let ((parser-descr (vector lexer
|
||||||
|
nts
|
||||||
|
starters
|
||||||
|
enders
|
||||||
|
predictors
|
||||||
|
steps
|
||||||
|
names)))
|
||||||
|
(lambda (input)
|
||||||
|
|
||||||
|
(define (ind nt nts) ; return index of non-terminal `nt' in `nts'
|
||||||
|
(let loop ((i (- (vector-length nts) 1)))
|
||||||
|
(if (>= i 0)
|
||||||
|
(if (equal? (vector-ref nts i) nt) i (loop (- i 1)))
|
||||||
|
#f)))
|
||||||
|
|
||||||
|
(define (comp-tok tok nts) ; transform token to parsing format
|
||||||
|
(let loop ((l1 (cdr tok)) (l2 '()))
|
||||||
|
(if (pair? l1)
|
||||||
|
(let ((i (ind (car l1) nts)))
|
||||||
|
(if i
|
||||||
|
(loop (cdr l1) (cons i l2))
|
||||||
|
(loop (cdr l1) l2)))
|
||||||
|
(cons (car tok) (reverse l2)))))
|
||||||
|
|
||||||
|
(define (input->tokens input lexer nts)
|
||||||
|
(list->vector (map (lambda (tok) (comp-tok tok nts)) (lexer input))))
|
||||||
|
|
||||||
|
(define (make-states nb-toks nb-confs)
|
||||||
|
(let ((states (make-vector (+ nb-toks 1) #f)))
|
||||||
|
(let loop ((i nb-toks))
|
||||||
|
(if (>= i 0)
|
||||||
|
(let ((v (make-vector (+ nb-confs 1) #f)))
|
||||||
|
(vector-set! v 0 -1)
|
||||||
|
(vector-set! states i v)
|
||||||
|
(loop (- i 1)))
|
||||||
|
states))))
|
||||||
|
|
||||||
|
(define (conf-set-get state conf)
|
||||||
|
(vector-ref state (+ conf 1)))
|
||||||
|
|
||||||
|
(define (conf-set-get* state state-num conf)
|
||||||
|
(let ((conf-set (conf-set-get state conf)))
|
||||||
|
(if conf-set
|
||||||
|
conf-set
|
||||||
|
(let ((conf-set (make-vector (+ state-num 6) #f)))
|
||||||
|
(vector-set! conf-set 1 -3) ; old elems tail (points to head)
|
||||||
|
(vector-set! conf-set 2 -1) ; old elems head
|
||||||
|
(vector-set! conf-set 3 -1) ; new elems tail (points to head)
|
||||||
|
(vector-set! conf-set 4 -1) ; new elems head
|
||||||
|
(vector-set! state (+ conf 1) conf-set)
|
||||||
|
conf-set))))
|
||||||
|
|
||||||
|
(define (conf-set-merge-new! conf-set)
|
||||||
|
(vector-set! conf-set
|
||||||
|
(+ (vector-ref conf-set 1) 5)
|
||||||
|
(vector-ref conf-set 4))
|
||||||
|
(vector-set! conf-set 1 (vector-ref conf-set 3))
|
||||||
|
(vector-set! conf-set 3 -1)
|
||||||
|
(vector-set! conf-set 4 -1))
|
||||||
|
|
||||||
|
(define (conf-set-head conf-set)
|
||||||
|
(vector-ref conf-set 2))
|
||||||
|
|
||||||
|
(define (conf-set-next conf-set i)
|
||||||
|
(vector-ref conf-set (+ i 5)))
|
||||||
|
|
||||||
|
(define (conf-set-member? state conf i)
|
||||||
|
(let ((conf-set (vector-ref state (+ conf 1))))
|
||||||
|
(if conf-set
|
||||||
|
(conf-set-next conf-set i)
|
||||||
|
#f)))
|
||||||
|
|
||||||
|
(define (conf-set-adjoin state conf-set conf i)
|
||||||
|
(let ((tail (vector-ref conf-set 3))) ; put new element at tail
|
||||||
|
(vector-set! conf-set (+ i 5) -1)
|
||||||
|
(vector-set! conf-set (+ tail 5) i)
|
||||||
|
(vector-set! conf-set 3 i)
|
||||||
|
(if (< tail 0)
|
||||||
|
(begin
|
||||||
|
(vector-set! conf-set 0 (vector-ref state 0))
|
||||||
|
(vector-set! state 0 conf)))))
|
||||||
|
|
||||||
|
(define (conf-set-adjoin* states state-num l i)
|
||||||
|
(let ((state (vector-ref states state-num)))
|
||||||
|
(let loop ((l1 l))
|
||||||
|
(if (pair? l1)
|
||||||
|
(let* ((conf (car l1))
|
||||||
|
(conf-set (conf-set-get* state state-num conf)))
|
||||||
|
(if (not (conf-set-next conf-set i))
|
||||||
|
(begin
|
||||||
|
(conf-set-adjoin state conf-set conf i)
|
||||||
|
(loop (cdr l1)))
|
||||||
|
(loop (cdr l1))))))))
|
||||||
|
|
||||||
|
(define (conf-set-adjoin** states states* state-num conf i)
|
||||||
|
(let ((state (vector-ref states state-num)))
|
||||||
|
(if (conf-set-member? state conf i)
|
||||||
|
(let* ((state* (vector-ref states* state-num))
|
||||||
|
(conf-set* (conf-set-get* state* state-num conf)))
|
||||||
|
(if (not (conf-set-next conf-set* i))
|
||||||
|
(conf-set-adjoin state* conf-set* conf i))
|
||||||
|
#t)
|
||||||
|
#f)))
|
||||||
|
|
||||||
|
(define (conf-set-union state conf-set conf other-set)
|
||||||
|
(let loop ((i (conf-set-head other-set)))
|
||||||
|
(if (>= i 0)
|
||||||
|
(if (not (conf-set-next conf-set i))
|
||||||
|
(begin
|
||||||
|
(conf-set-adjoin state conf-set conf i)
|
||||||
|
(loop (conf-set-next other-set i)))
|
||||||
|
(loop (conf-set-next other-set i))))))
|
||||||
|
|
||||||
|
(define (forw states state-num starters enders predictors steps nts)
|
||||||
|
|
||||||
|
(define (predict state state-num conf-set conf nt starters enders)
|
||||||
|
|
||||||
|
; add configurations which start the non-terminal `nt' to the
|
||||||
|
; right of the dot
|
||||||
|
|
||||||
|
(let loop1 ((l (vector-ref starters nt)))
|
||||||
|
(if (pair? l)
|
||||||
|
(let* ((starter (car l))
|
||||||
|
(starter-set (conf-set-get* state state-num starter)))
|
||||||
|
(if (not (conf-set-next starter-set state-num))
|
||||||
|
(begin
|
||||||
|
(conf-set-adjoin state starter-set starter state-num)
|
||||||
|
(loop1 (cdr l)))
|
||||||
|
(loop1 (cdr l))))))
|
||||||
|
|
||||||
|
; check for possible completion of the non-terminal `nt' to the
|
||||||
|
; right of the dot
|
||||||
|
|
||||||
|
(let loop2 ((l (vector-ref enders nt)))
|
||||||
|
(if (pair? l)
|
||||||
|
(let ((ender (car l)))
|
||||||
|
(if (conf-set-member? state ender state-num)
|
||||||
|
(let* ((next (+ conf 1))
|
||||||
|
(next-set (conf-set-get* state state-num next)))
|
||||||
|
(conf-set-union state next-set next conf-set)
|
||||||
|
(loop2 (cdr l)))
|
||||||
|
(loop2 (cdr l)))))))
|
||||||
|
|
||||||
|
(define (reduce states state state-num conf-set head preds)
|
||||||
|
|
||||||
|
; a non-terminal is now completed so check for reductions that
|
||||||
|
; are now possible at the configurations `preds'
|
||||||
|
|
||||||
|
(let loop1 ((l preds))
|
||||||
|
(if (pair? l)
|
||||||
|
(let ((pred (car l)))
|
||||||
|
(let loop2 ((i head))
|
||||||
|
(if (>= i 0)
|
||||||
|
(let ((pred-set (conf-set-get (vector-ref states i) pred)))
|
||||||
|
(if pred-set
|
||||||
|
(let* ((next (+ pred 1))
|
||||||
|
(next-set (conf-set-get* state state-num next)))
|
||||||
|
(conf-set-union state next-set next pred-set)))
|
||||||
|
(loop2 (conf-set-next conf-set i)))
|
||||||
|
(loop1 (cdr l))))))))
|
||||||
|
|
||||||
|
(let ((state (vector-ref states state-num))
|
||||||
|
(nb-nts (vector-length nts)))
|
||||||
|
(let loop ()
|
||||||
|
(let ((conf (vector-ref state 0)))
|
||||||
|
(if (>= conf 0)
|
||||||
|
(let* ((step (vector-ref steps conf))
|
||||||
|
(conf-set (vector-ref state (+ conf 1)))
|
||||||
|
(head (vector-ref conf-set 4)))
|
||||||
|
(vector-set! state 0 (vector-ref conf-set 0))
|
||||||
|
(conf-set-merge-new! conf-set)
|
||||||
|
(if (>= step 0)
|
||||||
|
(predict state state-num conf-set conf step starters enders)
|
||||||
|
(let ((preds (vector-ref predictors (+ step nb-nts))))
|
||||||
|
(reduce states state state-num conf-set head preds)))
|
||||||
|
(loop)))))))
|
||||||
|
|
||||||
|
(define (forward starters enders predictors steps nts toks)
|
||||||
|
(let* ((nb-toks (vector-length toks))
|
||||||
|
(nb-confs (vector-length steps))
|
||||||
|
(states (make-states nb-toks nb-confs))
|
||||||
|
(goal-starters (vector-ref starters 0)))
|
||||||
|
(conf-set-adjoin* states 0 goal-starters 0) ; predict goal
|
||||||
|
(forw states 0 starters enders predictors steps nts)
|
||||||
|
(let loop ((i 0))
|
||||||
|
(if (< i nb-toks)
|
||||||
|
(let ((tok-nts (cdr (vector-ref toks i))))
|
||||||
|
(conf-set-adjoin* states (+ i 1) tok-nts i) ; scan token
|
||||||
|
(forw states (+ i 1) starters enders predictors steps nts)
|
||||||
|
(loop (+ i 1)))))
|
||||||
|
states))
|
||||||
|
|
||||||
|
(define (produce conf i j enders steps toks states states* nb-nts)
|
||||||
|
(let ((prev (- conf 1)))
|
||||||
|
(if (and (>= conf nb-nts) (>= (vector-ref steps prev) 0))
|
||||||
|
(let loop1 ((l (vector-ref enders (vector-ref steps prev))))
|
||||||
|
(if (pair? l)
|
||||||
|
(let* ((ender (car l))
|
||||||
|
(ender-set (conf-set-get (vector-ref states j)
|
||||||
|
ender)))
|
||||||
|
(if ender-set
|
||||||
|
(let loop2 ((k (conf-set-head ender-set)))
|
||||||
|
(if (>= k 0)
|
||||||
|
(begin
|
||||||
|
(and (>= k i)
|
||||||
|
(conf-set-adjoin** states states* k prev i)
|
||||||
|
(conf-set-adjoin** states states* j ender k))
|
||||||
|
(loop2 (conf-set-next ender-set k)))
|
||||||
|
(loop1 (cdr l))))
|
||||||
|
(loop1 (cdr l)))))))))
|
||||||
|
|
||||||
|
(define (back states states* state-num enders steps nb-nts toks)
|
||||||
|
(let ((state* (vector-ref states* state-num)))
|
||||||
|
(let loop1 ()
|
||||||
|
(let ((conf (vector-ref state* 0)))
|
||||||
|
(if (>= conf 0)
|
||||||
|
(let* ((conf-set (vector-ref state* (+ conf 1)))
|
||||||
|
(head (vector-ref conf-set 4)))
|
||||||
|
(vector-set! state* 0 (vector-ref conf-set 0))
|
||||||
|
(conf-set-merge-new! conf-set)
|
||||||
|
(let loop2 ((i head))
|
||||||
|
(if (>= i 0)
|
||||||
|
(begin
|
||||||
|
(produce conf i state-num enders steps
|
||||||
|
toks states states* nb-nts)
|
||||||
|
(loop2 (conf-set-next conf-set i)))
|
||||||
|
(loop1)))))))))
|
||||||
|
|
||||||
|
(define (backward states enders steps nts toks)
|
||||||
|
(let* ((nb-toks (vector-length toks))
|
||||||
|
(nb-confs (vector-length steps))
|
||||||
|
(nb-nts (vector-length nts))
|
||||||
|
(states* (make-states nb-toks nb-confs))
|
||||||
|
(goal-enders (vector-ref enders 0)))
|
||||||
|
(let loop1 ((l goal-enders))
|
||||||
|
(if (pair? l)
|
||||||
|
(let ((conf (car l)))
|
||||||
|
(conf-set-adjoin** states states* nb-toks conf 0)
|
||||||
|
(loop1 (cdr l)))))
|
||||||
|
(let loop2 ((i nb-toks))
|
||||||
|
(if (>= i 0)
|
||||||
|
(begin
|
||||||
|
(back states states* i enders steps nb-nts toks)
|
||||||
|
(loop2 (- i 1)))))
|
||||||
|
states*))
|
||||||
|
|
||||||
|
(define (parsed? nt i j nts enders states)
|
||||||
|
(let ((nt* (ind nt nts)))
|
||||||
|
(if nt*
|
||||||
|
(let ((nb-nts (vector-length nts)))
|
||||||
|
(let loop ((l (vector-ref enders nt*)))
|
||||||
|
(if (pair? l)
|
||||||
|
(let ((conf (car l)))
|
||||||
|
(if (conf-set-member? (vector-ref states j) conf i)
|
||||||
|
#t
|
||||||
|
(loop (cdr l))))
|
||||||
|
#f)))
|
||||||
|
#f)))
|
||||||
|
|
||||||
|
(define (deriv-trees conf i j enders steps names toks states nb-nts)
|
||||||
|
(let ((name (vector-ref names conf)))
|
||||||
|
|
||||||
|
(if name ; `conf' is at the start of a rule (either special or not)
|
||||||
|
(if (< conf nb-nts)
|
||||||
|
(list (list name (car (vector-ref toks i))))
|
||||||
|
(list (list name)))
|
||||||
|
|
||||||
|
(let ((prev (- conf 1)))
|
||||||
|
(let loop1 ((l1 (vector-ref enders (vector-ref steps prev)))
|
||||||
|
(l2 '()))
|
||||||
|
(if (pair? l1)
|
||||||
|
(let* ((ender (car l1))
|
||||||
|
(ender-set (conf-set-get (vector-ref states j)
|
||||||
|
ender)))
|
||||||
|
(if ender-set
|
||||||
|
(let loop2 ((k (conf-set-head ender-set)) (l2 l2))
|
||||||
|
(if (>= k 0)
|
||||||
|
(if (and (>= k i)
|
||||||
|
(conf-set-member? (vector-ref states k)
|
||||||
|
prev i))
|
||||||
|
(let ((prev-trees
|
||||||
|
(deriv-trees prev i k enders steps names
|
||||||
|
toks states nb-nts))
|
||||||
|
(ender-trees
|
||||||
|
(deriv-trees ender k j enders steps names
|
||||||
|
toks states nb-nts)))
|
||||||
|
(let loop3 ((l3 ender-trees) (l2 l2))
|
||||||
|
(if (pair? l3)
|
||||||
|
(let ((ender-tree (list (car l3))))
|
||||||
|
(let loop4 ((l4 prev-trees) (l2 l2))
|
||||||
|
(if (pair? l4)
|
||||||
|
(loop4 (cdr l4)
|
||||||
|
(cons (append (car l4)
|
||||||
|
ender-tree)
|
||||||
|
l2))
|
||||||
|
(loop3 (cdr l3) l2))))
|
||||||
|
(loop2 (conf-set-next ender-set k) l2))))
|
||||||
|
(loop2 (conf-set-next ender-set k) l2))
|
||||||
|
(loop1 (cdr l1) l2)))
|
||||||
|
(loop1 (cdr l1) l2)))
|
||||||
|
l2))))))
|
||||||
|
|
||||||
|
(define (deriv-trees* nt i j nts enders steps names toks states)
|
||||||
|
(let ((nt* (ind nt nts)))
|
||||||
|
(if nt*
|
||||||
|
(let ((nb-nts (vector-length nts)))
|
||||||
|
(let loop ((l (vector-ref enders nt*)) (trees '()))
|
||||||
|
(if (pair? l)
|
||||||
|
(let ((conf (car l)))
|
||||||
|
(if (conf-set-member? (vector-ref states j) conf i)
|
||||||
|
(loop (cdr l)
|
||||||
|
(append (deriv-trees conf i j enders steps names
|
||||||
|
toks states nb-nts)
|
||||||
|
trees))
|
||||||
|
(loop (cdr l) trees)))
|
||||||
|
trees)))
|
||||||
|
#f)))
|
||||||
|
|
||||||
|
(define (nb-deriv-trees conf i j enders steps toks states nb-nts)
|
||||||
|
(let ((prev (- conf 1)))
|
||||||
|
(if (or (< conf nb-nts) (< (vector-ref steps prev) 0))
|
||||||
|
1
|
||||||
|
(let loop1 ((l (vector-ref enders (vector-ref steps prev)))
|
||||||
|
(n 0))
|
||||||
|
(if (pair? l)
|
||||||
|
(let* ((ender (car l))
|
||||||
|
(ender-set (conf-set-get (vector-ref states j)
|
||||||
|
ender)))
|
||||||
|
(if ender-set
|
||||||
|
(let loop2 ((k (conf-set-head ender-set)) (n n))
|
||||||
|
(if (>= k 0)
|
||||||
|
(if (and (>= k i)
|
||||||
|
(conf-set-member? (vector-ref states k)
|
||||||
|
prev i))
|
||||||
|
(let ((nb-prev-trees
|
||||||
|
(nb-deriv-trees prev i k enders steps
|
||||||
|
toks states nb-nts))
|
||||||
|
(nb-ender-trees
|
||||||
|
(nb-deriv-trees ender k j enders steps
|
||||||
|
toks states nb-nts)))
|
||||||
|
(loop2 (conf-set-next ender-set k)
|
||||||
|
(+ n (* nb-prev-trees nb-ender-trees))))
|
||||||
|
(loop2 (conf-set-next ender-set k) n))
|
||||||
|
(loop1 (cdr l) n)))
|
||||||
|
(loop1 (cdr l) n)))
|
||||||
|
n)))))
|
||||||
|
|
||||||
|
(define (nb-deriv-trees* nt i j nts enders steps toks states)
|
||||||
|
(let ((nt* (ind nt nts)))
|
||||||
|
(if nt*
|
||||||
|
(let ((nb-nts (vector-length nts)))
|
||||||
|
(let loop ((l (vector-ref enders nt*)) (nb-trees 0))
|
||||||
|
(if (pair? l)
|
||||||
|
(let ((conf (car l)))
|
||||||
|
(if (conf-set-member? (vector-ref states j) conf i)
|
||||||
|
(loop (cdr l)
|
||||||
|
(+ (nb-deriv-trees conf i j enders steps
|
||||||
|
toks states nb-nts)
|
||||||
|
nb-trees))
|
||||||
|
(loop (cdr l) nb-trees)))
|
||||||
|
nb-trees)))
|
||||||
|
#f)))
|
||||||
|
|
||||||
|
(let* ((lexer (vector-ref parser-descr 0))
|
||||||
|
(nts (vector-ref parser-descr 1))
|
||||||
|
(starters (vector-ref parser-descr 2))
|
||||||
|
(enders (vector-ref parser-descr 3))
|
||||||
|
(predictors (vector-ref parser-descr 4))
|
||||||
|
(steps (vector-ref parser-descr 5))
|
||||||
|
(names (vector-ref parser-descr 6))
|
||||||
|
(toks (input->tokens input lexer nts)))
|
||||||
|
|
||||||
|
(vector nts
|
||||||
|
starters
|
||||||
|
enders
|
||||||
|
predictors
|
||||||
|
steps
|
||||||
|
names
|
||||||
|
toks
|
||||||
|
(backward (forward starters enders predictors steps nts toks)
|
||||||
|
enders steps nts toks)
|
||||||
|
parsed?
|
||||||
|
deriv-trees*
|
||||||
|
nb-deriv-trees*))))))
|
||||||
|
|
||||||
|
(define (parse->parsed? parse nt i j)
|
||||||
|
(let* ((nts (vector-ref parse 0))
|
||||||
|
(enders (vector-ref parse 2))
|
||||||
|
(states (vector-ref parse 7))
|
||||||
|
(parsed? (vector-ref parse 8)))
|
||||||
|
(parsed? nt i j nts enders states)))
|
||||||
|
|
||||||
|
(define (parse->trees parse nt i j)
|
||||||
|
(let* ((nts (vector-ref parse 0))
|
||||||
|
(enders (vector-ref parse 2))
|
||||||
|
(steps (vector-ref parse 4))
|
||||||
|
(names (vector-ref parse 5))
|
||||||
|
(toks (vector-ref parse 6))
|
||||||
|
(states (vector-ref parse 7))
|
||||||
|
(deriv-trees* (vector-ref parse 9)))
|
||||||
|
(deriv-trees* nt i j nts enders steps names toks states)))
|
||||||
|
|
||||||
|
(define (parse->nb-trees parse nt i j)
|
||||||
|
(let* ((nts (vector-ref parse 0))
|
||||||
|
(enders (vector-ref parse 2))
|
||||||
|
(steps (vector-ref parse 4))
|
||||||
|
(toks (vector-ref parse 6))
|
||||||
|
(states (vector-ref parse 7))
|
||||||
|
(nb-deriv-trees* (vector-ref parse 10)))
|
||||||
|
(nb-deriv-trees* nt i j nts enders steps toks states)))
|
||||||
|
|
||||||
|
(define (test k)
|
||||||
|
(let ((p (make-parser '( (s (a) (s s)) )
|
||||||
|
(lambda (l) (map (lambda (x) (list x x)) l)))))
|
||||||
|
(let ((x (p (vector->list (make-vector k 'a)))))
|
||||||
|
(length (parse->trees x 's 0 k)))))
|
||||||
|
|
||||||
|
(define (earley-benchmark . args)
|
||||||
|
(let ((k (if (null? args) 9 (car args))))
|
||||||
|
(run-benchmark
|
||||||
|
"earley"
|
||||||
|
1
|
||||||
|
(lambda () (test k))
|
||||||
|
(lambda (result)
|
||||||
|
(display result)
|
||||||
|
(newline)
|
||||||
|
#t))))
|
||||||
233
gc-benchmarks/larceny/gcbench.sch
Normal file
233
gc-benchmarks/larceny/gcbench.sch
Normal file
|
|
@ -0,0 +1,233 @@
|
||||||
|
; This is adapted from a benchmark written by John Ellis and Pete Kovac
|
||||||
|
; of Post Communications.
|
||||||
|
; It was modified by Hans Boehm of Silicon Graphics.
|
||||||
|
; It was translated into Scheme by William D Clinger of Northeastern Univ;
|
||||||
|
; the Scheme version uses (RUN-BENCHMARK <string> <thunk>)
|
||||||
|
; It was later hacked by Lars T Hansen of Northeastern University;
|
||||||
|
; this version has a fixed tree height but accepts a number of
|
||||||
|
; iterations to run.
|
||||||
|
;
|
||||||
|
; Modified 2000-02-15 / lth: changed gc-benchmark to only stretch once,
|
||||||
|
; and to have a different interface (now accepts iteration numbers,
|
||||||
|
; not tree height)
|
||||||
|
; Last modified 2000-07-14 / lth -- fixed a buggy comment about storage
|
||||||
|
; use in Larceny.
|
||||||
|
;
|
||||||
|
; This is no substitute for real applications. No actual application
|
||||||
|
; is likely to behave in exactly this way. However, this benchmark was
|
||||||
|
; designed to be more representative of real applications than other
|
||||||
|
; Java GC benchmarks of which we are aware.
|
||||||
|
; It attempts to model those properties of allocation requests that
|
||||||
|
; are important to current GC techniques.
|
||||||
|
; It is designed to be used either to obtain a single overall performance
|
||||||
|
; number, or to give a more detailed estimate of how collector
|
||||||
|
; performance varies with object lifetimes. It prints the time
|
||||||
|
; required to allocate and collect balanced binary trees of various
|
||||||
|
; sizes. Smaller trees result in shorter object lifetimes. Each cycle
|
||||||
|
; allocates roughly the same amount of memory.
|
||||||
|
; Two data structures are kept around during the entire process, so
|
||||||
|
; that the measured performance is representative of applications
|
||||||
|
; that maintain some live in-memory data. One of these is a tree
|
||||||
|
; containing many pointers. The other is a large array containing
|
||||||
|
; double precision floating point numbers. Both should be of comparable
|
||||||
|
; size.
|
||||||
|
;
|
||||||
|
; The results are only really meaningful together with a specification
|
||||||
|
; of how much memory was used. It is possible to trade memory for
|
||||||
|
; better time performance. This benchmark should be run in a 32 MB
|
||||||
|
; heap, though we don't currently know how to enforce that uniformly.
|
||||||
|
|
||||||
|
; In the Java version, this routine prints the heap size and the amount
|
||||||
|
; of free memory. There is no portable way to do this in Scheme; each
|
||||||
|
; implementation needs its own version.
|
||||||
|
|
||||||
|
(define (PrintDiagnostics)
|
||||||
|
(display " Total memory available= ???????? bytes")
|
||||||
|
(display " Free memory= ???????? bytes")
|
||||||
|
(newline))
|
||||||
|
|
||||||
|
(define (yes answer) #t)
|
||||||
|
|
||||||
|
; Should we implement a Java class as procedures or hygienic macros?
|
||||||
|
; Take your pick.
|
||||||
|
|
||||||
|
(define-syntax let-class
|
||||||
|
(syntax-rules
|
||||||
|
()
|
||||||
|
; Put this rule first to implement a class using hygienic macros.
|
||||||
|
((let-class (((method . args) . method-body) ...) . body)
|
||||||
|
(letrec-syntax ((method (syntax-rules ()
|
||||||
|
((method . args) (begin . method-body))))
|
||||||
|
...)
|
||||||
|
. body))
|
||||||
|
; Put this rule first to implement a class using procedures.
|
||||||
|
((let-class (((method . args) . method-body) ...) . body)
|
||||||
|
(let () (define (method . args) . method-body) ... . body))
|
||||||
|
))
|
||||||
|
|
||||||
|
|
||||||
|
(define stretch #t) ; Controls whether stretching phase is run
|
||||||
|
|
||||||
|
(define (gcbench kStretchTreeDepth)
|
||||||
|
|
||||||
|
; Use for inner calls to reduce noise.
|
||||||
|
|
||||||
|
(define (run-benchmark name iters thunk test)
|
||||||
|
(do ((i 0 (+ i 1)))
|
||||||
|
((= i iters))
|
||||||
|
(thunk)))
|
||||||
|
|
||||||
|
; Nodes used by a tree of a given size
|
||||||
|
(define (TreeSize i)
|
||||||
|
(- (expt 2 (+ i 1)) 1))
|
||||||
|
|
||||||
|
; Number of iterations to use for a given tree depth
|
||||||
|
(define (NumIters i)
|
||||||
|
(quotient (* 2 (TreeSize kStretchTreeDepth))
|
||||||
|
(TreeSize i)))
|
||||||
|
|
||||||
|
; Parameters are determined by kStretchTreeDepth.
|
||||||
|
; In Boehm's version the parameters were fixed as follows:
|
||||||
|
; public static final int kStretchTreeDepth = 18; // about 16Mb
|
||||||
|
; public static final int kLongLivedTreeDepth = 16; // about 4Mb
|
||||||
|
; public static final int kArraySize = 500000; // about 4Mb
|
||||||
|
; public static final int kMinTreeDepth = 4;
|
||||||
|
; public static final int kMaxTreeDepth = 16;
|
||||||
|
; wdc: In Larceny the storage numbers above would be 12 Mby, 3 Mby, 6 Mby.
|
||||||
|
; lth: No they would not. A flonum requires 16 bytes, so the size
|
||||||
|
; of array + flonums would be 500,000*4 + 500,000*16=10 Mby.
|
||||||
|
|
||||||
|
(let* ((kLongLivedTreeDepth (- kStretchTreeDepth 2))
|
||||||
|
(kArraySize (* 4 (TreeSize kLongLivedTreeDepth)))
|
||||||
|
(kMinTreeDepth 4)
|
||||||
|
(kMaxTreeDepth kLongLivedTreeDepth))
|
||||||
|
|
||||||
|
; Elements 3 and 4 of the allocated vectors are useless.
|
||||||
|
|
||||||
|
(let-class (((make-node l r)
|
||||||
|
(let ((v (make-empty-node)))
|
||||||
|
(vector-set! v 0 l)
|
||||||
|
(vector-set! v 1 r)
|
||||||
|
v))
|
||||||
|
((make-empty-node) (make-vector 4 0))
|
||||||
|
((node.left node) (vector-ref node 0))
|
||||||
|
((node.right node) (vector-ref node 1))
|
||||||
|
((node.left-set! node x) (vector-set! node 0 x))
|
||||||
|
((node.right-set! node x) (vector-set! node 1 x)))
|
||||||
|
|
||||||
|
; Build tree top down, assigning to older objects.
|
||||||
|
(define (Populate iDepth thisNode)
|
||||||
|
(if (<= iDepth 0)
|
||||||
|
#f
|
||||||
|
(let ((iDepth (- iDepth 1)))
|
||||||
|
(node.left-set! thisNode (make-empty-node))
|
||||||
|
(node.right-set! thisNode (make-empty-node))
|
||||||
|
(Populate iDepth (node.left thisNode))
|
||||||
|
(Populate iDepth (node.right thisNode)))))
|
||||||
|
|
||||||
|
; Build tree bottom-up
|
||||||
|
(define (MakeTree iDepth)
|
||||||
|
(if (<= iDepth 0)
|
||||||
|
(make-empty-node)
|
||||||
|
(make-node (MakeTree (- iDepth 1))
|
||||||
|
(MakeTree (- iDepth 1)))))
|
||||||
|
|
||||||
|
(define (TimeConstruction depth)
|
||||||
|
(let ((iNumIters (NumIters depth)))
|
||||||
|
(display (string-append "Creating "
|
||||||
|
(number->string iNumIters)
|
||||||
|
" trees of depth "
|
||||||
|
(number->string depth)))
|
||||||
|
(newline)
|
||||||
|
(run-benchmark "GCBench: Top down construction"
|
||||||
|
1
|
||||||
|
(lambda ()
|
||||||
|
(do ((i 0 (+ i 1)))
|
||||||
|
((>= i iNumIters))
|
||||||
|
(Populate depth (make-empty-node))))
|
||||||
|
yes)
|
||||||
|
(run-benchmark "GCBench: Bottom up construction"
|
||||||
|
1
|
||||||
|
(lambda ()
|
||||||
|
(do ((i 0 (+ i 1)))
|
||||||
|
((>= i iNumIters))
|
||||||
|
(MakeTree depth)))
|
||||||
|
yes)))
|
||||||
|
|
||||||
|
(define (main)
|
||||||
|
(display "Garbage Collector Test")
|
||||||
|
(newline)
|
||||||
|
(if stretch
|
||||||
|
(begin
|
||||||
|
(display (string-append
|
||||||
|
" Stretching memory with a binary tree of depth "
|
||||||
|
(number->string kStretchTreeDepth)))
|
||||||
|
(newline)))
|
||||||
|
(PrintDiagnostics)
|
||||||
|
(run-benchmark "GCBench: Main"
|
||||||
|
1
|
||||||
|
(lambda ()
|
||||||
|
; Stretch the memory space quickly
|
||||||
|
(if stretch
|
||||||
|
(MakeTree kStretchTreeDepth))
|
||||||
|
|
||||||
|
; Create a long lived object
|
||||||
|
(display
|
||||||
|
(string-append
|
||||||
|
" Creating a long-lived binary tree of depth "
|
||||||
|
(number->string kLongLivedTreeDepth)))
|
||||||
|
(newline)
|
||||||
|
(let ((longLivedTree (make-empty-node)))
|
||||||
|
(Populate kLongLivedTreeDepth longLivedTree)
|
||||||
|
|
||||||
|
; Create long-lived array, filling half of it
|
||||||
|
(display (string-append
|
||||||
|
" Creating a long-lived array of "
|
||||||
|
(number->string kArraySize)
|
||||||
|
" inexact reals"))
|
||||||
|
(newline)
|
||||||
|
(let ((array (make-vector kArraySize 0.0)))
|
||||||
|
(do ((i 0 (+ i 1)))
|
||||||
|
((>= i (quotient kArraySize 2)))
|
||||||
|
(vector-set! array i
|
||||||
|
(/ 1.0 (exact->inexact i))))
|
||||||
|
(PrintDiagnostics)
|
||||||
|
|
||||||
|
(do ((d kMinTreeDepth (+ d 2)))
|
||||||
|
((> d kMaxTreeDepth))
|
||||||
|
(TimeConstruction d))
|
||||||
|
|
||||||
|
(if (or (eq? longLivedTree '())
|
||||||
|
(let ((n (min 1000
|
||||||
|
(- (quotient (vector-length array)
|
||||||
|
2)
|
||||||
|
1))))
|
||||||
|
(not (= (vector-ref array n)
|
||||||
|
(/ 1.0 (exact->inexact n))))))
|
||||||
|
(begin (display "Failed") (newline)))
|
||||||
|
; fake reference to LongLivedTree
|
||||||
|
; and array
|
||||||
|
; to keep them from being optimized away
|
||||||
|
)))
|
||||||
|
yes)
|
||||||
|
(PrintDiagnostics))
|
||||||
|
|
||||||
|
(main))))
|
||||||
|
|
||||||
|
(define (gc-benchmark . rest)
|
||||||
|
(let ((k 18)
|
||||||
|
(n (if (null? rest) 1 (car rest))))
|
||||||
|
(display "The garbage collector should touch about ")
|
||||||
|
(display (expt 2 (- k 13)))
|
||||||
|
(display " megabytes of heap storage.")
|
||||||
|
(newline)
|
||||||
|
(display "The use of more or less memory will skew the results.")
|
||||||
|
(newline)
|
||||||
|
(set! stretch #t)
|
||||||
|
(run-benchmark (string-append "GCBench" (number->string k))
|
||||||
|
n
|
||||||
|
(lambda ()
|
||||||
|
(gcbench k)
|
||||||
|
(set! stretch #f))
|
||||||
|
yes)
|
||||||
|
(set! stretch #t)))
|
||||||
644
gc-benchmarks/larceny/graphs.sch
Normal file
644
gc-benchmarks/larceny/graphs.sch
Normal file
|
|
@ -0,0 +1,644 @@
|
||||||
|
; Modified 2 March 1997 by Will Clinger to add graphs-benchmark
|
||||||
|
; and to expand the four macros below.
|
||||||
|
; Modified 11 June 1997 by Will Clinger to eliminate assertions
|
||||||
|
; and to replace a use of "recur" with a named let.
|
||||||
|
;
|
||||||
|
; Performance note: (graphs-benchmark 7) allocates
|
||||||
|
; 34509143 pairs
|
||||||
|
; 389625 vectors with 2551590 elements
|
||||||
|
; 56653504 closures (not counting top level and known procedures)
|
||||||
|
|
||||||
|
(define (graphs-benchmark . rest)
|
||||||
|
(let ((N (if (null? rest) 7 (car rest))))
|
||||||
|
(run-benchmark (string-append "graphs" (number->string N))
|
||||||
|
(lambda ()
|
||||||
|
(fold-over-rdg N
|
||||||
|
2
|
||||||
|
cons
|
||||||
|
'())))))
|
||||||
|
|
||||||
|
; End of new code.
|
||||||
|
|
||||||
|
;;; ==== std.ss ====
|
||||||
|
|
||||||
|
; (define-syntax assert
|
||||||
|
; (syntax-rules ()
|
||||||
|
; ((assert test info-rest ...)
|
||||||
|
; #F)))
|
||||||
|
;
|
||||||
|
; (define-syntax deny
|
||||||
|
; (syntax-rules ()
|
||||||
|
; ((deny test info-rest ...)
|
||||||
|
; #F)))
|
||||||
|
;
|
||||||
|
; (define-syntax when
|
||||||
|
; (syntax-rules ()
|
||||||
|
; ((when test e-first e-rest ...)
|
||||||
|
; (if test
|
||||||
|
; (begin e-first
|
||||||
|
; e-rest ...)))))
|
||||||
|
;
|
||||||
|
; (define-syntax unless
|
||||||
|
; (syntax-rules ()
|
||||||
|
; ((unless test e-first e-rest ...)
|
||||||
|
; (if (not test)
|
||||||
|
; (begin e-first
|
||||||
|
; e-rest ...)))))
|
||||||
|
|
||||||
|
(define assert
|
||||||
|
(lambda (test . info)
|
||||||
|
#f))
|
||||||
|
|
||||||
|
;;; ==== util.ss ====
|
||||||
|
|
||||||
|
|
||||||
|
; Fold over list elements, associating to the left.
|
||||||
|
(define fold
|
||||||
|
(lambda (lst folder state)
|
||||||
|
'(assert (list? lst)
|
||||||
|
lst)
|
||||||
|
'(assert (procedure? folder)
|
||||||
|
folder)
|
||||||
|
(do ((lst lst
|
||||||
|
(cdr lst))
|
||||||
|
(state state
|
||||||
|
(folder (car lst)
|
||||||
|
state)))
|
||||||
|
((null? lst)
|
||||||
|
state))))
|
||||||
|
|
||||||
|
; Given the size of a vector and a procedure which
|
||||||
|
; sends indicies to desired vector elements, create
|
||||||
|
; and return the vector.
|
||||||
|
(define proc->vector
|
||||||
|
(lambda (size f)
|
||||||
|
'(assert (and (integer? size)
|
||||||
|
(exact? size)
|
||||||
|
(>= size 0))
|
||||||
|
size)
|
||||||
|
'(assert (procedure? f)
|
||||||
|
f)
|
||||||
|
(if (zero? size)
|
||||||
|
(vector)
|
||||||
|
(let ((x (make-vector size (f 0))))
|
||||||
|
(let loop ((i 1))
|
||||||
|
(if (< i size) (begin ; [wdc - was when]
|
||||||
|
(vector-set! x i (f i))
|
||||||
|
(loop (+ i 1)))))
|
||||||
|
x))))
|
||||||
|
|
||||||
|
(define vector-fold
|
||||||
|
(lambda (vec folder state)
|
||||||
|
'(assert (vector? vec)
|
||||||
|
vec)
|
||||||
|
'(assert (procedure? folder)
|
||||||
|
folder)
|
||||||
|
(let ((len
|
||||||
|
(vector-length vec)))
|
||||||
|
(do ((i 0
|
||||||
|
(+ i 1))
|
||||||
|
(state state
|
||||||
|
(folder (vector-ref vec i)
|
||||||
|
state)))
|
||||||
|
((= i len)
|
||||||
|
state)))))
|
||||||
|
|
||||||
|
(define vector-map
|
||||||
|
(lambda (vec proc)
|
||||||
|
(proc->vector (vector-length vec)
|
||||||
|
(lambda (i)
|
||||||
|
(proc (vector-ref vec i))))))
|
||||||
|
|
||||||
|
; Given limit, return the list 0, 1, ..., limit-1.
|
||||||
|
(define giota
|
||||||
|
(lambda (limit)
|
||||||
|
'(assert (and (integer? limit)
|
||||||
|
(exact? limit)
|
||||||
|
(>= limit 0))
|
||||||
|
limit)
|
||||||
|
(let -*-
|
||||||
|
((limit
|
||||||
|
limit)
|
||||||
|
(res
|
||||||
|
'()))
|
||||||
|
(if (zero? limit)
|
||||||
|
res
|
||||||
|
(let ((limit
|
||||||
|
(- limit 1)))
|
||||||
|
(-*- limit
|
||||||
|
(cons limit res)))))))
|
||||||
|
|
||||||
|
; Fold over the integers [0, limit).
|
||||||
|
(define gnatural-fold
|
||||||
|
(lambda (limit folder state)
|
||||||
|
'(assert (and (integer? limit)
|
||||||
|
(exact? limit)
|
||||||
|
(>= limit 0))
|
||||||
|
limit)
|
||||||
|
'(assert (procedure? folder)
|
||||||
|
folder)
|
||||||
|
(do ((i 0
|
||||||
|
(+ i 1))
|
||||||
|
(state state
|
||||||
|
(folder i state)))
|
||||||
|
((= i limit)
|
||||||
|
state))))
|
||||||
|
|
||||||
|
; Iterate over the integers [0, limit).
|
||||||
|
(define gnatural-for-each
|
||||||
|
(lambda (limit proc!)
|
||||||
|
'(assert (and (integer? limit)
|
||||||
|
(exact? limit)
|
||||||
|
(>= limit 0))
|
||||||
|
limit)
|
||||||
|
'(assert (procedure? proc!)
|
||||||
|
proc!)
|
||||||
|
(do ((i 0
|
||||||
|
(+ i 1)))
|
||||||
|
((= i limit))
|
||||||
|
(proc! i))))
|
||||||
|
|
||||||
|
(define natural-for-all?
|
||||||
|
(lambda (limit ok?)
|
||||||
|
'(assert (and (integer? limit)
|
||||||
|
(exact? limit)
|
||||||
|
(>= limit 0))
|
||||||
|
limit)
|
||||||
|
'(assert (procedure? ok?)
|
||||||
|
ok?)
|
||||||
|
(let -*-
|
||||||
|
((i 0))
|
||||||
|
(or (= i limit)
|
||||||
|
(and (ok? i)
|
||||||
|
(-*- (+ i 1)))))))
|
||||||
|
|
||||||
|
(define natural-there-exists?
|
||||||
|
(lambda (limit ok?)
|
||||||
|
'(assert (and (integer? limit)
|
||||||
|
(exact? limit)
|
||||||
|
(>= limit 0))
|
||||||
|
limit)
|
||||||
|
'(assert (procedure? ok?)
|
||||||
|
ok?)
|
||||||
|
(let -*-
|
||||||
|
((i 0))
|
||||||
|
(and (not (= i limit))
|
||||||
|
(or (ok? i)
|
||||||
|
(-*- (+ i 1)))))))
|
||||||
|
|
||||||
|
(define there-exists?
|
||||||
|
(lambda (lst ok?)
|
||||||
|
'(assert (list? lst)
|
||||||
|
lst)
|
||||||
|
'(assert (procedure? ok?)
|
||||||
|
ok?)
|
||||||
|
(let -*-
|
||||||
|
((lst lst))
|
||||||
|
(and (not (null? lst))
|
||||||
|
(or (ok? (car lst))
|
||||||
|
(-*- (cdr lst)))))))
|
||||||
|
|
||||||
|
|
||||||
|
;;; ==== ptfold.ss ====
|
||||||
|
|
||||||
|
|
||||||
|
; Fold over the tree of permutations of a universe.
|
||||||
|
; Each branch (from the root) is a permutation of universe.
|
||||||
|
; Each node at depth d corresponds to all permutations which pick the
|
||||||
|
; elements spelled out on the branch from the root to that node as
|
||||||
|
; the first d elements.
|
||||||
|
; Their are two components to the state:
|
||||||
|
; The b-state is only a function of the branch from the root.
|
||||||
|
; The t-state is a function of all nodes seen so far.
|
||||||
|
; At each node, b-folder is called via
|
||||||
|
; (b-folder elem b-state t-state deeper accross)
|
||||||
|
; where elem is the next element of the universe picked.
|
||||||
|
; If b-folder can determine the result of the total tree fold at this stage,
|
||||||
|
; it should simply return the result.
|
||||||
|
; If b-folder can determine the result of folding over the sub-tree
|
||||||
|
; rooted at the resulting node, it should call accross via
|
||||||
|
; (accross new-t-state)
|
||||||
|
; where new-t-state is that result.
|
||||||
|
; Otherwise, b-folder should call deeper via
|
||||||
|
; (deeper new-b-state new-t-state)
|
||||||
|
; where new-b-state is the b-state for the new node and new-t-state is
|
||||||
|
; the new folded t-state.
|
||||||
|
; At the leaves of the tree, t-folder is called via
|
||||||
|
; (t-folder b-state t-state accross)
|
||||||
|
; If t-folder can determine the result of the total tree fold at this stage,
|
||||||
|
; it should simply return that result.
|
||||||
|
; If not, it should call accross via
|
||||||
|
; (accross new-t-state)
|
||||||
|
; Note, fold-over-perm-tree always calls b-folder in depth-first order.
|
||||||
|
; I.e., when b-folder is called at depth d, the branch leading to that
|
||||||
|
; node is the most recent calls to b-folder at all the depths less than d.
|
||||||
|
; This is a gross efficiency hack so that b-folder can use mutation to
|
||||||
|
; keep the current branch.
|
||||||
|
(define fold-over-perm-tree
|
||||||
|
(lambda (universe b-folder b-state t-folder t-state)
|
||||||
|
'(assert (list? universe)
|
||||||
|
universe)
|
||||||
|
'(assert (procedure? b-folder)
|
||||||
|
b-folder)
|
||||||
|
'(assert (procedure? t-folder)
|
||||||
|
t-folder)
|
||||||
|
(let -*-
|
||||||
|
((universe
|
||||||
|
universe)
|
||||||
|
(b-state
|
||||||
|
b-state)
|
||||||
|
(t-state
|
||||||
|
t-state)
|
||||||
|
(accross
|
||||||
|
(lambda (final-t-state)
|
||||||
|
final-t-state)))
|
||||||
|
(if (null? universe)
|
||||||
|
(t-folder b-state t-state accross)
|
||||||
|
(let -**-
|
||||||
|
((in
|
||||||
|
universe)
|
||||||
|
(out
|
||||||
|
'())
|
||||||
|
(t-state
|
||||||
|
t-state))
|
||||||
|
(let* ((first
|
||||||
|
(car in))
|
||||||
|
(rest
|
||||||
|
(cdr in))
|
||||||
|
(accross
|
||||||
|
(if (null? rest)
|
||||||
|
accross
|
||||||
|
(lambda (new-t-state)
|
||||||
|
(-**- rest
|
||||||
|
(cons first out)
|
||||||
|
new-t-state)))))
|
||||||
|
(b-folder first
|
||||||
|
b-state
|
||||||
|
t-state
|
||||||
|
(lambda (new-b-state new-t-state)
|
||||||
|
(-*- (fold out cons rest)
|
||||||
|
new-b-state
|
||||||
|
new-t-state
|
||||||
|
accross))
|
||||||
|
accross)))))))
|
||||||
|
|
||||||
|
|
||||||
|
;;; ==== minimal.ss ====
|
||||||
|
|
||||||
|
|
||||||
|
; A directed graph is stored as a connection matrix (vector-of-vectors)
|
||||||
|
; where the first index is the `from' vertex and the second is the `to'
|
||||||
|
; vertex. Each entry is a bool indicating if the edge exists.
|
||||||
|
; The diagonal of the matrix is never examined.
|
||||||
|
; Make-minimal? returns a procedure which tests if a labelling
|
||||||
|
; of the verticies is such that the matrix is minimal.
|
||||||
|
; If it is, then the procedure returns the result of folding over
|
||||||
|
; the elements of the automoriphism group. If not, it returns #F.
|
||||||
|
; The folding is done by calling folder via
|
||||||
|
; (folder perm state accross)
|
||||||
|
; If the folder wants to continue, it should call accross via
|
||||||
|
; (accross new-state)
|
||||||
|
; If it just wants the entire minimal? procedure to return something,
|
||||||
|
; it should return that.
|
||||||
|
; The ordering used is lexicographic (with #T > #F) and entries
|
||||||
|
; are examined in the following order:
|
||||||
|
; 1->0, 0->1
|
||||||
|
;
|
||||||
|
; 2->0, 0->2
|
||||||
|
; 2->1, 1->2
|
||||||
|
;
|
||||||
|
; 3->0, 0->3
|
||||||
|
; 3->1, 1->3
|
||||||
|
; 3->2, 2->3
|
||||||
|
; ...
|
||||||
|
(define make-minimal?
|
||||||
|
(lambda (max-size)
|
||||||
|
'(assert (and (integer? max-size)
|
||||||
|
(exact? max-size)
|
||||||
|
(>= max-size 0))
|
||||||
|
max-size)
|
||||||
|
(let ((iotas
|
||||||
|
(proc->vector (+ max-size 1)
|
||||||
|
giota))
|
||||||
|
(perm
|
||||||
|
(make-vector max-size 0)))
|
||||||
|
(lambda (size graph folder state)
|
||||||
|
'(assert (and (integer? size)
|
||||||
|
(exact? size)
|
||||||
|
(<= 0 size max-size))
|
||||||
|
size
|
||||||
|
max-size)
|
||||||
|
'(assert (vector? graph)
|
||||||
|
graph)
|
||||||
|
'(assert (procedure? folder)
|
||||||
|
folder)
|
||||||
|
(fold-over-perm-tree (vector-ref iotas size)
|
||||||
|
(lambda (perm-x x state deeper accross)
|
||||||
|
(case (cmp-next-vertex graph perm x perm-x)
|
||||||
|
((less)
|
||||||
|
#F)
|
||||||
|
((equal)
|
||||||
|
(vector-set! perm x perm-x)
|
||||||
|
(deeper (+ x 1)
|
||||||
|
state))
|
||||||
|
((more)
|
||||||
|
(accross state))
|
||||||
|
(else
|
||||||
|
(assert #F))))
|
||||||
|
0
|
||||||
|
(lambda (leaf-depth state accross)
|
||||||
|
'(assert (eqv? leaf-depth size)
|
||||||
|
leaf-depth
|
||||||
|
size)
|
||||||
|
(folder perm state accross))
|
||||||
|
state)))))
|
||||||
|
|
||||||
|
; Given a graph, a partial permutation vector, the next input and the next
|
||||||
|
; output, return 'less, 'equal or 'more depending on the lexicographic
|
||||||
|
; comparison between the permuted and un-permuted graph.
|
||||||
|
(define cmp-next-vertex
|
||||||
|
(lambda (graph perm x perm-x)
|
||||||
|
(let ((from-x
|
||||||
|
(vector-ref graph x))
|
||||||
|
(from-perm-x
|
||||||
|
(vector-ref graph perm-x)))
|
||||||
|
(let -*-
|
||||||
|
((y
|
||||||
|
0))
|
||||||
|
(if (= x y)
|
||||||
|
'equal
|
||||||
|
(let ((x->y?
|
||||||
|
(vector-ref from-x y))
|
||||||
|
(perm-y
|
||||||
|
(vector-ref perm y)))
|
||||||
|
(cond ((eq? x->y?
|
||||||
|
(vector-ref from-perm-x perm-y))
|
||||||
|
(let ((y->x?
|
||||||
|
(vector-ref (vector-ref graph y)
|
||||||
|
x)))
|
||||||
|
(cond ((eq? y->x?
|
||||||
|
(vector-ref (vector-ref graph perm-y)
|
||||||
|
perm-x))
|
||||||
|
(-*- (+ y 1)))
|
||||||
|
(y->x?
|
||||||
|
'less)
|
||||||
|
(else
|
||||||
|
'more))))
|
||||||
|
(x->y?
|
||||||
|
'less)
|
||||||
|
(else
|
||||||
|
'more))))))))
|
||||||
|
|
||||||
|
|
||||||
|
;;; ==== rdg.ss ====
|
||||||
|
|
||||||
|
|
||||||
|
; Fold over rooted directed graphs with bounded out-degree.
|
||||||
|
; Size is the number of verticies (including the root). Max-out is the
|
||||||
|
; maximum out-degree for any vertex. Folder is called via
|
||||||
|
; (folder edges state)
|
||||||
|
; where edges is a list of length size. The ith element of the list is
|
||||||
|
; a list of the verticies j for which there is an edge from i to j.
|
||||||
|
; The last vertex is the root.
|
||||||
|
(define fold-over-rdg
|
||||||
|
(lambda (size max-out folder state)
|
||||||
|
'(assert (and (exact? size)
|
||||||
|
(integer? size)
|
||||||
|
(> size 0))
|
||||||
|
size)
|
||||||
|
'(assert (and (exact? max-out)
|
||||||
|
(integer? max-out)
|
||||||
|
(>= max-out 0))
|
||||||
|
max-out)
|
||||||
|
'(assert (procedure? folder)
|
||||||
|
folder)
|
||||||
|
(let* ((root
|
||||||
|
(- size 1))
|
||||||
|
(edge?
|
||||||
|
(proc->vector size
|
||||||
|
(lambda (from)
|
||||||
|
(make-vector size #F))))
|
||||||
|
(edges
|
||||||
|
(make-vector size '()))
|
||||||
|
(out-degrees
|
||||||
|
(make-vector size 0))
|
||||||
|
(minimal-folder
|
||||||
|
(make-minimal? root))
|
||||||
|
(non-root-minimal?
|
||||||
|
(let ((cont
|
||||||
|
(lambda (perm state accross)
|
||||||
|
'(assert (eq? state #T)
|
||||||
|
state)
|
||||||
|
(accross #T))))
|
||||||
|
(lambda (size)
|
||||||
|
(minimal-folder size
|
||||||
|
edge?
|
||||||
|
cont
|
||||||
|
#T))))
|
||||||
|
(root-minimal?
|
||||||
|
(let ((cont
|
||||||
|
(lambda (perm state accross)
|
||||||
|
'(assert (eq? state #T)
|
||||||
|
state)
|
||||||
|
(case (cmp-next-vertex edge? perm root root)
|
||||||
|
((less)
|
||||||
|
#F)
|
||||||
|
((equal more)
|
||||||
|
(accross #T))
|
||||||
|
(else
|
||||||
|
(assert #F))))))
|
||||||
|
(lambda ()
|
||||||
|
(minimal-folder root
|
||||||
|
edge?
|
||||||
|
cont
|
||||||
|
#T)))))
|
||||||
|
(let -*-
|
||||||
|
((vertex
|
||||||
|
0)
|
||||||
|
(state
|
||||||
|
state))
|
||||||
|
(cond ((not (non-root-minimal? vertex))
|
||||||
|
state)
|
||||||
|
((= vertex root)
|
||||||
|
'(assert
|
||||||
|
(begin
|
||||||
|
(gnatural-for-each root
|
||||||
|
(lambda (v)
|
||||||
|
'(assert (= (vector-ref out-degrees v)
|
||||||
|
(length (vector-ref edges v)))
|
||||||
|
v
|
||||||
|
(vector-ref out-degrees v)
|
||||||
|
(vector-ref edges v))))
|
||||||
|
#T))
|
||||||
|
(let ((reach?
|
||||||
|
(make-reach? root edges))
|
||||||
|
(from-root
|
||||||
|
(vector-ref edge? root)))
|
||||||
|
(let -*-
|
||||||
|
((v
|
||||||
|
0)
|
||||||
|
(outs
|
||||||
|
0)
|
||||||
|
(efr
|
||||||
|
'())
|
||||||
|
(efrr
|
||||||
|
'())
|
||||||
|
(state
|
||||||
|
state))
|
||||||
|
(cond ((not (or (= v root)
|
||||||
|
(= outs max-out)))
|
||||||
|
(vector-set! from-root v #T)
|
||||||
|
(let ((state
|
||||||
|
(-*- (+ v 1)
|
||||||
|
(+ outs 1)
|
||||||
|
(cons v efr)
|
||||||
|
(cons (vector-ref reach? v)
|
||||||
|
efrr)
|
||||||
|
state)))
|
||||||
|
(vector-set! from-root v #F)
|
||||||
|
(-*- (+ v 1)
|
||||||
|
outs
|
||||||
|
efr
|
||||||
|
efrr
|
||||||
|
state)))
|
||||||
|
((and (natural-for-all? root
|
||||||
|
(lambda (v)
|
||||||
|
(there-exists? efrr
|
||||||
|
(lambda (r)
|
||||||
|
(vector-ref r v)))))
|
||||||
|
(root-minimal?))
|
||||||
|
(vector-set! edges root efr)
|
||||||
|
(folder
|
||||||
|
(proc->vector size
|
||||||
|
(lambda (i)
|
||||||
|
(vector-ref edges i)))
|
||||||
|
state))
|
||||||
|
(else
|
||||||
|
state)))))
|
||||||
|
(else
|
||||||
|
(let ((from-vertex
|
||||||
|
(vector-ref edge? vertex)))
|
||||||
|
(let -**-
|
||||||
|
((sv
|
||||||
|
0)
|
||||||
|
(outs
|
||||||
|
0)
|
||||||
|
(state
|
||||||
|
state))
|
||||||
|
(if (= sv vertex)
|
||||||
|
(begin
|
||||||
|
(vector-set! out-degrees vertex outs)
|
||||||
|
(-*- (+ vertex 1)
|
||||||
|
state))
|
||||||
|
(let* ((state
|
||||||
|
; no sv->vertex, no vertex->sv
|
||||||
|
(-**- (+ sv 1)
|
||||||
|
outs
|
||||||
|
state))
|
||||||
|
(from-sv
|
||||||
|
(vector-ref edge? sv))
|
||||||
|
(sv-out
|
||||||
|
(vector-ref out-degrees sv))
|
||||||
|
(state
|
||||||
|
(if (= sv-out max-out)
|
||||||
|
state
|
||||||
|
(begin
|
||||||
|
(vector-set! edges
|
||||||
|
sv
|
||||||
|
(cons vertex
|
||||||
|
(vector-ref edges sv)))
|
||||||
|
(vector-set! from-sv vertex #T)
|
||||||
|
(vector-set! out-degrees sv (+ sv-out 1))
|
||||||
|
(let* ((state
|
||||||
|
; sv->vertex, no vertex->sv
|
||||||
|
(-**- (+ sv 1)
|
||||||
|
outs
|
||||||
|
state))
|
||||||
|
(state
|
||||||
|
(if (= outs max-out)
|
||||||
|
state
|
||||||
|
(begin
|
||||||
|
(vector-set! from-vertex sv #T)
|
||||||
|
(vector-set! edges
|
||||||
|
vertex
|
||||||
|
(cons sv
|
||||||
|
(vector-ref edges vertex)))
|
||||||
|
(let ((state
|
||||||
|
; sv->vertex, vertex->sv
|
||||||
|
(-**- (+ sv 1)
|
||||||
|
(+ outs 1)
|
||||||
|
state)))
|
||||||
|
(vector-set! edges
|
||||||
|
vertex
|
||||||
|
(cdr (vector-ref edges vertex)))
|
||||||
|
(vector-set! from-vertex sv #F)
|
||||||
|
state)))))
|
||||||
|
(vector-set! out-degrees sv sv-out)
|
||||||
|
(vector-set! from-sv vertex #F)
|
||||||
|
(vector-set! edges
|
||||||
|
sv
|
||||||
|
(cdr (vector-ref edges sv)))
|
||||||
|
state)))))
|
||||||
|
(if (= outs max-out)
|
||||||
|
state
|
||||||
|
(begin
|
||||||
|
(vector-set! edges
|
||||||
|
vertex
|
||||||
|
(cons sv
|
||||||
|
(vector-ref edges vertex)))
|
||||||
|
(vector-set! from-vertex sv #T)
|
||||||
|
(let ((state
|
||||||
|
; no sv->vertex, vertex->sv
|
||||||
|
(-**- (+ sv 1)
|
||||||
|
(+ outs 1)
|
||||||
|
state)))
|
||||||
|
(vector-set! from-vertex sv #F)
|
||||||
|
(vector-set! edges
|
||||||
|
vertex
|
||||||
|
(cdr (vector-ref edges vertex)))
|
||||||
|
state)))))))))))))
|
||||||
|
|
||||||
|
; Given a vector which maps vertex to out-going-edge list,
|
||||||
|
; return a vector which gives reachability.
|
||||||
|
(define make-reach?
|
||||||
|
(lambda (size vertex->out)
|
||||||
|
(let ((res
|
||||||
|
(proc->vector size
|
||||||
|
(lambda (v)
|
||||||
|
(let ((from-v
|
||||||
|
(make-vector size #F)))
|
||||||
|
(vector-set! from-v v #T)
|
||||||
|
(for-each
|
||||||
|
(lambda (x)
|
||||||
|
(vector-set! from-v x #T))
|
||||||
|
(vector-ref vertex->out v))
|
||||||
|
from-v)))))
|
||||||
|
(gnatural-for-each size
|
||||||
|
(lambda (m)
|
||||||
|
(let ((from-m
|
||||||
|
(vector-ref res m)))
|
||||||
|
(gnatural-for-each size
|
||||||
|
(lambda (f)
|
||||||
|
(let ((from-f
|
||||||
|
(vector-ref res f)))
|
||||||
|
(if (vector-ref from-f m); [wdc - was when]
|
||||||
|
(begin
|
||||||
|
(gnatural-for-each size
|
||||||
|
(lambda (t)
|
||||||
|
(if (vector-ref from-m t)
|
||||||
|
(begin ; [wdc - was when]
|
||||||
|
(vector-set! from-f t #T)))))))))))))
|
||||||
|
res)))
|
||||||
|
|
||||||
|
|
||||||
|
;;; ==== test input ====
|
||||||
|
|
||||||
|
; Produces all directed graphs with N verticies, distinguished root,
|
||||||
|
; and out-degree bounded by 2, upto isomorphism (there are 44).
|
||||||
|
|
||||||
|
;(define go
|
||||||
|
; (let ((N 7))
|
||||||
|
; (fold-over-rdg N
|
||||||
|
; 2
|
||||||
|
; cons
|
||||||
|
; '())))
|
||||||
219
gc-benchmarks/larceny/lattice.sch
Normal file
219
gc-benchmarks/larceny/lattice.sch
Normal file
|
|
@ -0,0 +1,219 @@
|
||||||
|
; This benchmark was obtained from Andrew Wright.
|
||||||
|
; 970215 / wdc Added lattice-benchmark.
|
||||||
|
|
||||||
|
; Given a comparison routine that returns one of
|
||||||
|
; less
|
||||||
|
; more
|
||||||
|
; equal
|
||||||
|
; uncomparable
|
||||||
|
; return a new comparison routine that applies to sequences.
|
||||||
|
(define lexico
|
||||||
|
(lambda (base)
|
||||||
|
(define lex-fixed
|
||||||
|
(lambda (fixed lhs rhs)
|
||||||
|
(define check
|
||||||
|
(lambda (lhs rhs)
|
||||||
|
(if (null? lhs)
|
||||||
|
fixed
|
||||||
|
(let ((probe
|
||||||
|
(base (car lhs)
|
||||||
|
(car rhs))))
|
||||||
|
(if (or (eq? probe 'equal)
|
||||||
|
(eq? probe fixed))
|
||||||
|
(check (cdr lhs)
|
||||||
|
(cdr rhs))
|
||||||
|
'uncomparable)))))
|
||||||
|
(check lhs rhs)))
|
||||||
|
(define lex-first
|
||||||
|
(lambda (lhs rhs)
|
||||||
|
(if (null? lhs)
|
||||||
|
'equal
|
||||||
|
(let ((probe
|
||||||
|
(base (car lhs)
|
||||||
|
(car rhs))))
|
||||||
|
(case probe
|
||||||
|
((less more)
|
||||||
|
(lex-fixed probe
|
||||||
|
(cdr lhs)
|
||||||
|
(cdr rhs)))
|
||||||
|
((equal)
|
||||||
|
(lex-first (cdr lhs)
|
||||||
|
(cdr rhs)))
|
||||||
|
((uncomparable)
|
||||||
|
'uncomparable))))))
|
||||||
|
lex-first))
|
||||||
|
|
||||||
|
(define (make-lattice elem-list cmp-func)
|
||||||
|
(cons elem-list cmp-func))
|
||||||
|
|
||||||
|
(define lattice->elements car)
|
||||||
|
|
||||||
|
(define lattice->cmp cdr)
|
||||||
|
|
||||||
|
; Select elements of a list which pass some test.
|
||||||
|
(define zulu-select
|
||||||
|
(lambda (test lst)
|
||||||
|
(define select-a
|
||||||
|
(lambda (ac lst)
|
||||||
|
(if (null? lst)
|
||||||
|
(reverse! ac)
|
||||||
|
(select-a
|
||||||
|
(let ((head (car lst)))
|
||||||
|
(if (test head)
|
||||||
|
(cons head ac)
|
||||||
|
ac))
|
||||||
|
(cdr lst)))))
|
||||||
|
(select-a '() lst)))
|
||||||
|
|
||||||
|
(define reverse!
|
||||||
|
(letrec ((rotate
|
||||||
|
(lambda (fo fum)
|
||||||
|
(let ((next (cdr fo)))
|
||||||
|
(set-cdr! fo fum)
|
||||||
|
(if (null? next)
|
||||||
|
fo
|
||||||
|
(rotate next fo))))))
|
||||||
|
(lambda (lst)
|
||||||
|
(if (null? lst)
|
||||||
|
'()
|
||||||
|
(rotate lst '())))))
|
||||||
|
|
||||||
|
; Select elements of a list which pass some test and map a function
|
||||||
|
; over the result. Note, only efficiency prevents this from being the
|
||||||
|
; composition of select and map.
|
||||||
|
(define select-map
|
||||||
|
(lambda (test func lst)
|
||||||
|
(define select-a
|
||||||
|
(lambda (ac lst)
|
||||||
|
(if (null? lst)
|
||||||
|
(reverse! ac)
|
||||||
|
(select-a
|
||||||
|
(let ((head (car lst)))
|
||||||
|
(if (test head)
|
||||||
|
(cons (func head)
|
||||||
|
ac)
|
||||||
|
ac))
|
||||||
|
(cdr lst)))))
|
||||||
|
(select-a '() lst)))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
; This version of map-and tail-recurses on the last test.
|
||||||
|
(define map-and
|
||||||
|
(lambda (proc lst)
|
||||||
|
(if (null? lst)
|
||||||
|
#T
|
||||||
|
(letrec ((drudge
|
||||||
|
(lambda (lst)
|
||||||
|
(let ((rest (cdr lst)))
|
||||||
|
(if (null? rest)
|
||||||
|
(proc (car lst))
|
||||||
|
(and (proc (car lst))
|
||||||
|
(drudge rest)))))))
|
||||||
|
(drudge lst)))))
|
||||||
|
|
||||||
|
(define (maps-1 source target pas new)
|
||||||
|
(let ((scmp (lattice->cmp source))
|
||||||
|
(tcmp (lattice->cmp target)))
|
||||||
|
(let ((less
|
||||||
|
(select-map
|
||||||
|
(lambda (p)
|
||||||
|
(eq? 'less
|
||||||
|
(scmp (car p) new)))
|
||||||
|
cdr
|
||||||
|
pas))
|
||||||
|
(more
|
||||||
|
(select-map
|
||||||
|
(lambda (p)
|
||||||
|
(eq? 'more
|
||||||
|
(scmp (car p) new)))
|
||||||
|
cdr
|
||||||
|
pas)))
|
||||||
|
(zulu-select
|
||||||
|
(lambda (t)
|
||||||
|
(and
|
||||||
|
(map-and
|
||||||
|
(lambda (t2)
|
||||||
|
(memq (tcmp t2 t) '(less equal)))
|
||||||
|
less)
|
||||||
|
(map-and
|
||||||
|
(lambda (t2)
|
||||||
|
(memq (tcmp t2 t) '(more equal)))
|
||||||
|
more)))
|
||||||
|
(lattice->elements target)))))
|
||||||
|
|
||||||
|
(define (maps-rest source target pas rest to-1 to-collect)
|
||||||
|
(if (null? rest)
|
||||||
|
(to-1 pas)
|
||||||
|
(let ((next (car rest))
|
||||||
|
(rest (cdr rest)))
|
||||||
|
(to-collect
|
||||||
|
(map
|
||||||
|
(lambda (x)
|
||||||
|
(maps-rest source target
|
||||||
|
(cons
|
||||||
|
(cons next x)
|
||||||
|
pas)
|
||||||
|
rest
|
||||||
|
to-1
|
||||||
|
to-collect))
|
||||||
|
(maps-1 source target pas next))))))
|
||||||
|
|
||||||
|
(define (maps source target)
|
||||||
|
(make-lattice
|
||||||
|
(maps-rest source
|
||||||
|
target
|
||||||
|
'()
|
||||||
|
(lattice->elements source)
|
||||||
|
(lambda (x) (list (map cdr x)))
|
||||||
|
(lambda (x) (apply append x)))
|
||||||
|
(lexico (lattice->cmp target))))
|
||||||
|
|
||||||
|
(define print-frequency 10000)
|
||||||
|
|
||||||
|
(define (count-maps source target)
|
||||||
|
(let ((count 0))
|
||||||
|
(maps-rest source
|
||||||
|
target
|
||||||
|
'()
|
||||||
|
(lattice->elements source)
|
||||||
|
(lambda (x)
|
||||||
|
(set! count (+ count 1))
|
||||||
|
(if (= 0 (remainder count print-frequency))
|
||||||
|
(begin #f))
|
||||||
|
1)
|
||||||
|
(lambda (x) (apply + x)))))
|
||||||
|
|
||||||
|
(define (lattice-benchmark)
|
||||||
|
(run-benchmark "Lattice"
|
||||||
|
(lambda ()
|
||||||
|
(let* ((l2
|
||||||
|
(make-lattice '(low high)
|
||||||
|
(lambda (lhs rhs)
|
||||||
|
(case lhs
|
||||||
|
((low)
|
||||||
|
(case rhs
|
||||||
|
((low)
|
||||||
|
'equal)
|
||||||
|
((high)
|
||||||
|
'less)
|
||||||
|
(else
|
||||||
|
(error 'make-lattice "base" rhs))))
|
||||||
|
((high)
|
||||||
|
(case rhs
|
||||||
|
((low)
|
||||||
|
'more)
|
||||||
|
((high)
|
||||||
|
'equal)
|
||||||
|
(else
|
||||||
|
(error 'make-lattice "base" rhs))))
|
||||||
|
(else
|
||||||
|
(error 'make-lattice "base" lhs))))))
|
||||||
|
(l3 (maps l2 l2))
|
||||||
|
(l4 (maps l3 l3)))
|
||||||
|
(count-maps l2 l2)
|
||||||
|
(count-maps l3 l3)
|
||||||
|
(count-maps l2 l3)
|
||||||
|
(count-maps l3 l2)
|
||||||
|
(count-maps l4 l4)))))
|
||||||
|
|
||||||
770
gc-benchmarks/larceny/nboyer.sch
Normal file
770
gc-benchmarks/larceny/nboyer.sch
Normal file
|
|
@ -0,0 +1,770 @@
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
; File: nboyer.sch
|
||||||
|
; Description: The Boyer benchmark
|
||||||
|
; Author: Bob Boyer
|
||||||
|
; Created: 5-Apr-85
|
||||||
|
; Modified: 10-Apr-85 14:52:20 (Bob Shaw)
|
||||||
|
; 22-Jul-87 (Will Clinger)
|
||||||
|
; 2-Jul-88 (Will Clinger -- distinguished #f and the empty list)
|
||||||
|
; 13-Feb-97 (Will Clinger -- fixed bugs in unifier and rules,
|
||||||
|
; rewrote to eliminate property lists, and added
|
||||||
|
; a scaling parameter suggested by Bob Boyer)
|
||||||
|
; 19-Mar-99 (Will Clinger -- cleaned up comments)
|
||||||
|
; 4-Apr-01 (Will Clinger -- changed four 1- symbols to sub1)
|
||||||
|
; Language: Scheme
|
||||||
|
; Status: Public Domain
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
|
;;; NBOYER -- Logic programming benchmark, originally written by Bob Boyer.
|
||||||
|
;;; Fairly CONS intensive.
|
||||||
|
|
||||||
|
; Note: The version of this benchmark that appears in Dick Gabriel's book
|
||||||
|
; contained several bugs that are corrected here. These bugs are discussed
|
||||||
|
; by Henry Baker, "The Boyer Benchmark Meets Linear Logic", ACM SIGPLAN Lisp
|
||||||
|
; Pointers 6(4), October-December 1993, pages 3-10. The fixed bugs are:
|
||||||
|
;
|
||||||
|
; The benchmark now returns a boolean result.
|
||||||
|
; FALSEP and TRUEP use TERM-MEMBER? rather than MEMV (which is called MEMBER
|
||||||
|
; in Common Lisp)
|
||||||
|
; ONE-WAY-UNIFY1 now treats numbers correctly
|
||||||
|
; ONE-WAY-UNIFY1-LST now treats empty lists correctly
|
||||||
|
; Rule 19 has been corrected (this rule was not touched by the original
|
||||||
|
; benchmark, but is used by this version)
|
||||||
|
; Rules 84 and 101 have been corrected (but these rules are never touched
|
||||||
|
; by the benchmark)
|
||||||
|
;
|
||||||
|
; According to Baker, these bug fixes make the benchmark 10-25% slower.
|
||||||
|
; Please do not compare the timings from this benchmark against those of
|
||||||
|
; the original benchmark.
|
||||||
|
;
|
||||||
|
; This version of the benchmark also prints the number of rewrites as a sanity
|
||||||
|
; check, because it is too easy for a buggy version to return the correct
|
||||||
|
; boolean result. The correct number of rewrites is
|
||||||
|
;
|
||||||
|
; n rewrites peak live storage (approximate, in bytes)
|
||||||
|
; 0 95024 520,000
|
||||||
|
; 1 591777 2,085,000
|
||||||
|
; 2 1813975 5,175,000
|
||||||
|
; 3 5375678
|
||||||
|
; 4 16445406
|
||||||
|
; 5 51507739
|
||||||
|
|
||||||
|
; Nboyer is a 2-phase benchmark.
|
||||||
|
; The first phase attaches lemmas to symbols. This phase is not timed,
|
||||||
|
; but it accounts for very little of the runtime anyway.
|
||||||
|
; The second phase creates the test problem, and tests to see
|
||||||
|
; whether it is implied by the lemmas.
|
||||||
|
|
||||||
|
(define (nboyer-benchmark . args)
|
||||||
|
(let ((n (if (null? args) 0 (car args))))
|
||||||
|
(setup-boyer)
|
||||||
|
(run-benchmark (string-append "nboyer"
|
||||||
|
(number->string n))
|
||||||
|
1
|
||||||
|
(lambda () (test-boyer n))
|
||||||
|
(lambda (rewrites)
|
||||||
|
(and (number? rewrites)
|
||||||
|
(case n
|
||||||
|
((0) (= rewrites 95024))
|
||||||
|
((1) (= rewrites 591777))
|
||||||
|
((2) (= rewrites 1813975))
|
||||||
|
((3) (= rewrites 5375678))
|
||||||
|
((4) (= rewrites 16445406))
|
||||||
|
((5) (= rewrites 51507739))
|
||||||
|
; If it works for n <= 5, assume it works.
|
||||||
|
(else #t)))))))
|
||||||
|
|
||||||
|
(define (setup-boyer) #t) ; assigned below
|
||||||
|
(define (test-boyer) #t) ; assigned below
|
||||||
|
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
;
|
||||||
|
; The first phase.
|
||||||
|
;
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
|
; In the original benchmark, it stored a list of lemmas on the
|
||||||
|
; property lists of symbols.
|
||||||
|
; In the new benchmark, it maintains an association list of
|
||||||
|
; symbols and symbol-records, and stores the list of lemmas
|
||||||
|
; within the symbol-records.
|
||||||
|
|
||||||
|
(let ()
|
||||||
|
|
||||||
|
(define (setup)
|
||||||
|
(add-lemma-lst
|
||||||
|
(quote ((equal (compile form)
|
||||||
|
(reverse (codegen (optimize form)
|
||||||
|
(nil))))
|
||||||
|
(equal (eqp x y)
|
||||||
|
(equal (fix x)
|
||||||
|
(fix y)))
|
||||||
|
(equal (greaterp x y)
|
||||||
|
(lessp y x))
|
||||||
|
(equal (lesseqp x y)
|
||||||
|
(not (lessp y x)))
|
||||||
|
(equal (greatereqp x y)
|
||||||
|
(not (lessp x y)))
|
||||||
|
(equal (boolean x)
|
||||||
|
(or (equal x (t))
|
||||||
|
(equal x (f))))
|
||||||
|
(equal (iff x y)
|
||||||
|
(and (implies x y)
|
||||||
|
(implies y x)))
|
||||||
|
(equal (even1 x)
|
||||||
|
(if (zerop x)
|
||||||
|
(t)
|
||||||
|
(odd (sub1 x))))
|
||||||
|
(equal (countps- l pred)
|
||||||
|
(countps-loop l pred (zero)))
|
||||||
|
(equal (fact- i)
|
||||||
|
(fact-loop i 1))
|
||||||
|
(equal (reverse- x)
|
||||||
|
(reverse-loop x (nil)))
|
||||||
|
(equal (divides x y)
|
||||||
|
(zerop (remainder y x)))
|
||||||
|
(equal (assume-true var alist)
|
||||||
|
(cons (cons var (t))
|
||||||
|
alist))
|
||||||
|
(equal (assume-false var alist)
|
||||||
|
(cons (cons var (f))
|
||||||
|
alist))
|
||||||
|
(equal (tautology-checker x)
|
||||||
|
(tautologyp (normalize x)
|
||||||
|
(nil)))
|
||||||
|
(equal (falsify x)
|
||||||
|
(falsify1 (normalize x)
|
||||||
|
(nil)))
|
||||||
|
(equal (prime x)
|
||||||
|
(and (not (zerop x))
|
||||||
|
(not (equal x (add1 (zero))))
|
||||||
|
(prime1 x (sub1 x))))
|
||||||
|
(equal (and p q)
|
||||||
|
(if p (if q (t)
|
||||||
|
(f))
|
||||||
|
(f)))
|
||||||
|
(equal (or p q)
|
||||||
|
(if p (t)
|
||||||
|
(if q (t)
|
||||||
|
(f))))
|
||||||
|
(equal (not p)
|
||||||
|
(if p (f)
|
||||||
|
(t)))
|
||||||
|
(equal (implies p q)
|
||||||
|
(if p (if q (t)
|
||||||
|
(f))
|
||||||
|
(t)))
|
||||||
|
(equal (fix x)
|
||||||
|
(if (numberp x)
|
||||||
|
x
|
||||||
|
(zero)))
|
||||||
|
(equal (if (if a b c)
|
||||||
|
d e)
|
||||||
|
(if a (if b d e)
|
||||||
|
(if c d e)))
|
||||||
|
(equal (zerop x)
|
||||||
|
(or (equal x (zero))
|
||||||
|
(not (numberp x))))
|
||||||
|
(equal (plus (plus x y)
|
||||||
|
z)
|
||||||
|
(plus x (plus y z)))
|
||||||
|
(equal (equal (plus a b)
|
||||||
|
(zero))
|
||||||
|
(and (zerop a)
|
||||||
|
(zerop b)))
|
||||||
|
(equal (difference x x)
|
||||||
|
(zero))
|
||||||
|
(equal (equal (plus a b)
|
||||||
|
(plus a c))
|
||||||
|
(equal (fix b)
|
||||||
|
(fix c)))
|
||||||
|
(equal (equal (zero)
|
||||||
|
(difference x y))
|
||||||
|
(not (lessp y x)))
|
||||||
|
(equal (equal x (difference x y))
|
||||||
|
(and (numberp x)
|
||||||
|
(or (equal x (zero))
|
||||||
|
(zerop y))))
|
||||||
|
(equal (meaning (plus-tree (append x y))
|
||||||
|
a)
|
||||||
|
(plus (meaning (plus-tree x)
|
||||||
|
a)
|
||||||
|
(meaning (plus-tree y)
|
||||||
|
a)))
|
||||||
|
(equal (meaning (plus-tree (plus-fringe x))
|
||||||
|
a)
|
||||||
|
(fix (meaning x a)))
|
||||||
|
(equal (append (append x y)
|
||||||
|
z)
|
||||||
|
(append x (append y z)))
|
||||||
|
(equal (reverse (append a b))
|
||||||
|
(append (reverse b)
|
||||||
|
(reverse a)))
|
||||||
|
(equal (times x (plus y z))
|
||||||
|
(plus (times x y)
|
||||||
|
(times x z)))
|
||||||
|
(equal (times (times x y)
|
||||||
|
z)
|
||||||
|
(times x (times y z)))
|
||||||
|
(equal (equal (times x y)
|
||||||
|
(zero))
|
||||||
|
(or (zerop x)
|
||||||
|
(zerop y)))
|
||||||
|
(equal (exec (append x y)
|
||||||
|
pds envrn)
|
||||||
|
(exec y (exec x pds envrn)
|
||||||
|
envrn))
|
||||||
|
(equal (mc-flatten x y)
|
||||||
|
(append (flatten x)
|
||||||
|
y))
|
||||||
|
(equal (member x (append a b))
|
||||||
|
(or (member x a)
|
||||||
|
(member x b)))
|
||||||
|
(equal (member x (reverse y))
|
||||||
|
(member x y))
|
||||||
|
(equal (length (reverse x))
|
||||||
|
(length x))
|
||||||
|
(equal (member a (intersect b c))
|
||||||
|
(and (member a b)
|
||||||
|
(member a c)))
|
||||||
|
(equal (nth (zero)
|
||||||
|
i)
|
||||||
|
(zero))
|
||||||
|
(equal (exp i (plus j k))
|
||||||
|
(times (exp i j)
|
||||||
|
(exp i k)))
|
||||||
|
(equal (exp i (times j k))
|
||||||
|
(exp (exp i j)
|
||||||
|
k))
|
||||||
|
(equal (reverse-loop x y)
|
||||||
|
(append (reverse x)
|
||||||
|
y))
|
||||||
|
(equal (reverse-loop x (nil))
|
||||||
|
(reverse x))
|
||||||
|
(equal (count-list z (sort-lp x y))
|
||||||
|
(plus (count-list z x)
|
||||||
|
(count-list z y)))
|
||||||
|
(equal (equal (append a b)
|
||||||
|
(append a c))
|
||||||
|
(equal b c))
|
||||||
|
(equal (plus (remainder x y)
|
||||||
|
(times y (quotient x y)))
|
||||||
|
(fix x))
|
||||||
|
(equal (power-eval (big-plus1 l i base)
|
||||||
|
base)
|
||||||
|
(plus (power-eval l base)
|
||||||
|
i))
|
||||||
|
(equal (power-eval (big-plus x y i base)
|
||||||
|
base)
|
||||||
|
(plus i (plus (power-eval x base)
|
||||||
|
(power-eval y base))))
|
||||||
|
(equal (remainder y 1)
|
||||||
|
(zero))
|
||||||
|
(equal (lessp (remainder x y)
|
||||||
|
y)
|
||||||
|
(not (zerop y)))
|
||||||
|
(equal (remainder x x)
|
||||||
|
(zero))
|
||||||
|
(equal (lessp (quotient i j)
|
||||||
|
i)
|
||||||
|
(and (not (zerop i))
|
||||||
|
(or (zerop j)
|
||||||
|
(not (equal j 1)))))
|
||||||
|
(equal (lessp (remainder x y)
|
||||||
|
x)
|
||||||
|
(and (not (zerop y))
|
||||||
|
(not (zerop x))
|
||||||
|
(not (lessp x y))))
|
||||||
|
(equal (power-eval (power-rep i base)
|
||||||
|
base)
|
||||||
|
(fix i))
|
||||||
|
(equal (power-eval (big-plus (power-rep i base)
|
||||||
|
(power-rep j base)
|
||||||
|
(zero)
|
||||||
|
base)
|
||||||
|
base)
|
||||||
|
(plus i j))
|
||||||
|
(equal (gcd x y)
|
||||||
|
(gcd y x))
|
||||||
|
(equal (nth (append a b)
|
||||||
|
i)
|
||||||
|
(append (nth a i)
|
||||||
|
(nth b (difference i (length a)))))
|
||||||
|
(equal (difference (plus x y)
|
||||||
|
x)
|
||||||
|
(fix y))
|
||||||
|
(equal (difference (plus y x)
|
||||||
|
x)
|
||||||
|
(fix y))
|
||||||
|
(equal (difference (plus x y)
|
||||||
|
(plus x z))
|
||||||
|
(difference y z))
|
||||||
|
(equal (times x (difference c w))
|
||||||
|
(difference (times c x)
|
||||||
|
(times w x)))
|
||||||
|
(equal (remainder (times x z)
|
||||||
|
z)
|
||||||
|
(zero))
|
||||||
|
(equal (difference (plus b (plus a c))
|
||||||
|
a)
|
||||||
|
(plus b c))
|
||||||
|
(equal (difference (add1 (plus y z))
|
||||||
|
z)
|
||||||
|
(add1 y))
|
||||||
|
(equal (lessp (plus x y)
|
||||||
|
(plus x z))
|
||||||
|
(lessp y z))
|
||||||
|
(equal (lessp (times x z)
|
||||||
|
(times y z))
|
||||||
|
(and (not (zerop z))
|
||||||
|
(lessp x y)))
|
||||||
|
(equal (lessp y (plus x y))
|
||||||
|
(not (zerop x)))
|
||||||
|
(equal (gcd (times x z)
|
||||||
|
(times y z))
|
||||||
|
(times z (gcd x y)))
|
||||||
|
(equal (value (normalize x)
|
||||||
|
a)
|
||||||
|
(value x a))
|
||||||
|
(equal (equal (flatten x)
|
||||||
|
(cons y (nil)))
|
||||||
|
(and (nlistp x)
|
||||||
|
(equal x y)))
|
||||||
|
(equal (listp (gopher x))
|
||||||
|
(listp x))
|
||||||
|
(equal (samefringe x y)
|
||||||
|
(equal (flatten x)
|
||||||
|
(flatten y)))
|
||||||
|
(equal (equal (greatest-factor x y)
|
||||||
|
(zero))
|
||||||
|
(and (or (zerop y)
|
||||||
|
(equal y 1))
|
||||||
|
(equal x (zero))))
|
||||||
|
(equal (equal (greatest-factor x y)
|
||||||
|
1)
|
||||||
|
(equal x 1))
|
||||||
|
(equal (numberp (greatest-factor x y))
|
||||||
|
(not (and (or (zerop y)
|
||||||
|
(equal y 1))
|
||||||
|
(not (numberp x)))))
|
||||||
|
(equal (times-list (append x y))
|
||||||
|
(times (times-list x)
|
||||||
|
(times-list y)))
|
||||||
|
(equal (prime-list (append x y))
|
||||||
|
(and (prime-list x)
|
||||||
|
(prime-list y)))
|
||||||
|
(equal (equal z (times w z))
|
||||||
|
(and (numberp z)
|
||||||
|
(or (equal z (zero))
|
||||||
|
(equal w 1))))
|
||||||
|
(equal (greatereqp x y)
|
||||||
|
(not (lessp x y)))
|
||||||
|
(equal (equal x (times x y))
|
||||||
|
(or (equal x (zero))
|
||||||
|
(and (numberp x)
|
||||||
|
(equal y 1))))
|
||||||
|
(equal (remainder (times y x)
|
||||||
|
y)
|
||||||
|
(zero))
|
||||||
|
(equal (equal (times a b)
|
||||||
|
1)
|
||||||
|
(and (not (equal a (zero)))
|
||||||
|
(not (equal b (zero)))
|
||||||
|
(numberp a)
|
||||||
|
(numberp b)
|
||||||
|
(equal (sub1 a)
|
||||||
|
(zero))
|
||||||
|
(equal (sub1 b)
|
||||||
|
(zero))))
|
||||||
|
(equal (lessp (length (delete x l))
|
||||||
|
(length l))
|
||||||
|
(member x l))
|
||||||
|
(equal (sort2 (delete x l))
|
||||||
|
(delete x (sort2 l)))
|
||||||
|
(equal (dsort x)
|
||||||
|
(sort2 x))
|
||||||
|
(equal (length (cons x1
|
||||||
|
(cons x2
|
||||||
|
(cons x3 (cons x4
|
||||||
|
(cons x5
|
||||||
|
(cons x6 x7)))))))
|
||||||
|
(plus 6 (length x7)))
|
||||||
|
(equal (difference (add1 (add1 x))
|
||||||
|
2)
|
||||||
|
(fix x))
|
||||||
|
(equal (quotient (plus x (plus x y))
|
||||||
|
2)
|
||||||
|
(plus x (quotient y 2)))
|
||||||
|
(equal (sigma (zero)
|
||||||
|
i)
|
||||||
|
(quotient (times i (add1 i))
|
||||||
|
2))
|
||||||
|
(equal (plus x (add1 y))
|
||||||
|
(if (numberp y)
|
||||||
|
(add1 (plus x y))
|
||||||
|
(add1 x)))
|
||||||
|
(equal (equal (difference x y)
|
||||||
|
(difference z y))
|
||||||
|
(if (lessp x y)
|
||||||
|
(not (lessp y z))
|
||||||
|
(if (lessp z y)
|
||||||
|
(not (lessp y x))
|
||||||
|
(equal (fix x)
|
||||||
|
(fix z)))))
|
||||||
|
(equal (meaning (plus-tree (delete x y))
|
||||||
|
a)
|
||||||
|
(if (member x y)
|
||||||
|
(difference (meaning (plus-tree y)
|
||||||
|
a)
|
||||||
|
(meaning x a))
|
||||||
|
(meaning (plus-tree y)
|
||||||
|
a)))
|
||||||
|
(equal (times x (add1 y))
|
||||||
|
(if (numberp y)
|
||||||
|
(plus x (times x y))
|
||||||
|
(fix x)))
|
||||||
|
(equal (nth (nil)
|
||||||
|
i)
|
||||||
|
(if (zerop i)
|
||||||
|
(nil)
|
||||||
|
(zero)))
|
||||||
|
(equal (last (append a b))
|
||||||
|
(if (listp b)
|
||||||
|
(last b)
|
||||||
|
(if (listp a)
|
||||||
|
(cons (car (last a))
|
||||||
|
b)
|
||||||
|
b)))
|
||||||
|
(equal (equal (lessp x y)
|
||||||
|
z)
|
||||||
|
(if (lessp x y)
|
||||||
|
(equal (t) z)
|
||||||
|
(equal (f) z)))
|
||||||
|
(equal (assignment x (append a b))
|
||||||
|
(if (assignedp x a)
|
||||||
|
(assignment x a)
|
||||||
|
(assignment x b)))
|
||||||
|
(equal (car (gopher x))
|
||||||
|
(if (listp x)
|
||||||
|
(car (flatten x))
|
||||||
|
(zero)))
|
||||||
|
(equal (flatten (cdr (gopher x)))
|
||||||
|
(if (listp x)
|
||||||
|
(cdr (flatten x))
|
||||||
|
(cons (zero)
|
||||||
|
(nil))))
|
||||||
|
(equal (quotient (times y x)
|
||||||
|
y)
|
||||||
|
(if (zerop y)
|
||||||
|
(zero)
|
||||||
|
(fix x)))
|
||||||
|
(equal (get j (set i val mem))
|
||||||
|
(if (eqp j i)
|
||||||
|
val
|
||||||
|
(get j mem)))))))
|
||||||
|
|
||||||
|
(define (add-lemma-lst lst)
|
||||||
|
(cond ((null? lst)
|
||||||
|
#t)
|
||||||
|
(else (add-lemma (car lst))
|
||||||
|
(add-lemma-lst (cdr lst)))))
|
||||||
|
|
||||||
|
(define (add-lemma term)
|
||||||
|
(cond ((and (pair? term)
|
||||||
|
(eq? (car term)
|
||||||
|
(quote equal))
|
||||||
|
(pair? (cadr term)))
|
||||||
|
(put (car (cadr term))
|
||||||
|
(quote lemmas)
|
||||||
|
(cons
|
||||||
|
(translate-term term)
|
||||||
|
(get (car (cadr term)) (quote lemmas)))))
|
||||||
|
(else (error "ADD-LEMMA did not like term: " term))))
|
||||||
|
|
||||||
|
; Translates a term by replacing its constructor symbols by symbol-records.
|
||||||
|
|
||||||
|
(define (translate-term term)
|
||||||
|
(cond ((not (pair? term))
|
||||||
|
term)
|
||||||
|
(else (cons (symbol->symbol-record (car term))
|
||||||
|
(translate-args (cdr term))))))
|
||||||
|
|
||||||
|
(define (translate-args lst)
|
||||||
|
(cond ((null? lst)
|
||||||
|
'())
|
||||||
|
(else (cons (translate-term (car lst))
|
||||||
|
(translate-args (cdr lst))))))
|
||||||
|
|
||||||
|
; For debugging only, so the use of MAP does not change
|
||||||
|
; the first-order character of the benchmark.
|
||||||
|
|
||||||
|
(define (untranslate-term term)
|
||||||
|
(cond ((not (pair? term))
|
||||||
|
term)
|
||||||
|
(else (cons (get-name (car term))
|
||||||
|
(map untranslate-term (cdr term))))))
|
||||||
|
|
||||||
|
; A symbol-record is represented as a vector with two fields:
|
||||||
|
; the symbol (for debugging) and
|
||||||
|
; the list of lemmas associated with the symbol.
|
||||||
|
|
||||||
|
(define (put sym property value)
|
||||||
|
(put-lemmas! (symbol->symbol-record sym) value))
|
||||||
|
|
||||||
|
(define (get sym property)
|
||||||
|
(get-lemmas (symbol->symbol-record sym)))
|
||||||
|
|
||||||
|
(define (symbol->symbol-record sym)
|
||||||
|
(let ((x (assq sym *symbol-records-alist*)))
|
||||||
|
(if x
|
||||||
|
(cdr x)
|
||||||
|
(let ((r (make-symbol-record sym)))
|
||||||
|
(set! *symbol-records-alist*
|
||||||
|
(cons (cons sym r)
|
||||||
|
*symbol-records-alist*))
|
||||||
|
r))))
|
||||||
|
|
||||||
|
; Association list of symbols and symbol-records.
|
||||||
|
|
||||||
|
(define *symbol-records-alist* '())
|
||||||
|
|
||||||
|
; A symbol-record is represented as a vector with two fields:
|
||||||
|
; the symbol (for debugging) and
|
||||||
|
; the list of lemmas associated with the symbol.
|
||||||
|
|
||||||
|
(define (make-symbol-record sym)
|
||||||
|
(vector sym '()))
|
||||||
|
|
||||||
|
(define (put-lemmas! symbol-record lemmas)
|
||||||
|
(vector-set! symbol-record 1 lemmas))
|
||||||
|
|
||||||
|
(define (get-lemmas symbol-record)
|
||||||
|
(vector-ref symbol-record 1))
|
||||||
|
|
||||||
|
(define (get-name symbol-record)
|
||||||
|
(vector-ref symbol-record 0))
|
||||||
|
|
||||||
|
(define (symbol-record-equal? r1 r2)
|
||||||
|
(eq? r1 r2))
|
||||||
|
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
;
|
||||||
|
; The second phase.
|
||||||
|
;
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
|
(define (test n)
|
||||||
|
(let ((term
|
||||||
|
(apply-subst
|
||||||
|
(translate-alist
|
||||||
|
(quote ((x f (plus (plus a b)
|
||||||
|
(plus c (zero))))
|
||||||
|
(y f (times (times a b)
|
||||||
|
(plus c d)))
|
||||||
|
(z f (reverse (append (append a b)
|
||||||
|
(nil))))
|
||||||
|
(u equal (plus a b)
|
||||||
|
(difference x y))
|
||||||
|
(w lessp (remainder a b)
|
||||||
|
(member a (length b))))))
|
||||||
|
(translate-term
|
||||||
|
(do ((term
|
||||||
|
(quote (implies (and (implies x y)
|
||||||
|
(and (implies y z)
|
||||||
|
(and (implies z u)
|
||||||
|
(implies u w))))
|
||||||
|
(implies x w)))
|
||||||
|
(list 'or term '(f)))
|
||||||
|
(n n (- n 1)))
|
||||||
|
((zero? n) term))))))
|
||||||
|
(tautp term)))
|
||||||
|
|
||||||
|
(define (translate-alist alist)
|
||||||
|
(cond ((null? alist)
|
||||||
|
'())
|
||||||
|
(else (cons (cons (caar alist)
|
||||||
|
(translate-term (cdar alist)))
|
||||||
|
(translate-alist (cdr alist))))))
|
||||||
|
|
||||||
|
(define (apply-subst alist term)
|
||||||
|
(cond ((not (pair? term))
|
||||||
|
(let ((temp-temp (assq term alist)))
|
||||||
|
(if temp-temp
|
||||||
|
(cdr temp-temp)
|
||||||
|
term)))
|
||||||
|
(else (cons (car term)
|
||||||
|
(apply-subst-lst alist (cdr term))))))
|
||||||
|
|
||||||
|
(define (apply-subst-lst alist lst)
|
||||||
|
(cond ((null? lst)
|
||||||
|
'())
|
||||||
|
(else (cons (apply-subst alist (car lst))
|
||||||
|
(apply-subst-lst alist (cdr lst))))))
|
||||||
|
|
||||||
|
(define (tautp x)
|
||||||
|
(tautologyp (rewrite x)
|
||||||
|
'() '()))
|
||||||
|
|
||||||
|
(define (tautologyp x true-lst false-lst)
|
||||||
|
(cond ((truep x true-lst)
|
||||||
|
#t)
|
||||||
|
((falsep x false-lst)
|
||||||
|
#f)
|
||||||
|
((not (pair? x))
|
||||||
|
#f)
|
||||||
|
((eq? (car x) if-constructor)
|
||||||
|
(cond ((truep (cadr x)
|
||||||
|
true-lst)
|
||||||
|
(tautologyp (caddr x)
|
||||||
|
true-lst false-lst))
|
||||||
|
((falsep (cadr x)
|
||||||
|
false-lst)
|
||||||
|
(tautologyp (cadddr x)
|
||||||
|
true-lst false-lst))
|
||||||
|
(else (and (tautologyp (caddr x)
|
||||||
|
(cons (cadr x)
|
||||||
|
true-lst)
|
||||||
|
false-lst)
|
||||||
|
(tautologyp (cadddr x)
|
||||||
|
true-lst
|
||||||
|
(cons (cadr x)
|
||||||
|
false-lst))))))
|
||||||
|
(else #f)))
|
||||||
|
|
||||||
|
(define if-constructor '*) ; becomes (symbol->symbol-record 'if)
|
||||||
|
|
||||||
|
(define rewrite-count 0) ; sanity check
|
||||||
|
|
||||||
|
(define (rewrite term)
|
||||||
|
(set! rewrite-count (+ rewrite-count 1))
|
||||||
|
(cond ((not (pair? term))
|
||||||
|
term)
|
||||||
|
(else (rewrite-with-lemmas (cons (car term)
|
||||||
|
(rewrite-args (cdr term)))
|
||||||
|
(get-lemmas (car term))))))
|
||||||
|
|
||||||
|
(define (rewrite-args lst)
|
||||||
|
(cond ((null? lst)
|
||||||
|
'())
|
||||||
|
(else (cons (rewrite (car lst))
|
||||||
|
(rewrite-args (cdr lst))))))
|
||||||
|
|
||||||
|
(define (rewrite-with-lemmas term lst)
|
||||||
|
(cond ((null? lst)
|
||||||
|
term)
|
||||||
|
((one-way-unify term (cadr (car lst)))
|
||||||
|
(rewrite (apply-subst unify-subst (caddr (car lst)))))
|
||||||
|
(else (rewrite-with-lemmas term (cdr lst)))))
|
||||||
|
|
||||||
|
(define unify-subst '*)
|
||||||
|
|
||||||
|
(define (one-way-unify term1 term2)
|
||||||
|
(begin (set! unify-subst '())
|
||||||
|
(one-way-unify1 term1 term2)))
|
||||||
|
|
||||||
|
(define (one-way-unify1 term1 term2)
|
||||||
|
(cond ((not (pair? term2))
|
||||||
|
(let ((temp-temp (assq term2 unify-subst)))
|
||||||
|
(cond (temp-temp
|
||||||
|
(term-equal? term1 (cdr temp-temp)))
|
||||||
|
((number? term2) ; This bug fix makes
|
||||||
|
(equal? term1 term2)) ; nboyer 10-25% slower!
|
||||||
|
(else
|
||||||
|
(set! unify-subst (cons (cons term2 term1)
|
||||||
|
unify-subst))
|
||||||
|
#t))))
|
||||||
|
((not (pair? term1))
|
||||||
|
#f)
|
||||||
|
((eq? (car term1)
|
||||||
|
(car term2))
|
||||||
|
(one-way-unify1-lst (cdr term1)
|
||||||
|
(cdr term2)))
|
||||||
|
(else #f)))
|
||||||
|
|
||||||
|
(define (one-way-unify1-lst lst1 lst2)
|
||||||
|
(cond ((null? lst1)
|
||||||
|
(null? lst2))
|
||||||
|
((null? lst2)
|
||||||
|
#f)
|
||||||
|
((one-way-unify1 (car lst1)
|
||||||
|
(car lst2))
|
||||||
|
(one-way-unify1-lst (cdr lst1)
|
||||||
|
(cdr lst2)))
|
||||||
|
(else #f)))
|
||||||
|
|
||||||
|
(define (falsep x lst)
|
||||||
|
(or (term-equal? x false-term)
|
||||||
|
(term-member? x lst)))
|
||||||
|
|
||||||
|
(define (truep x lst)
|
||||||
|
(or (term-equal? x true-term)
|
||||||
|
(term-member? x lst)))
|
||||||
|
|
||||||
|
(define false-term '*) ; becomes (translate-term '(f))
|
||||||
|
(define true-term '*) ; becomes (translate-term '(t))
|
||||||
|
|
||||||
|
; The next two procedures were in the original benchmark
|
||||||
|
; but were never used.
|
||||||
|
|
||||||
|
(define (trans-of-implies n)
|
||||||
|
(translate-term
|
||||||
|
(list (quote implies)
|
||||||
|
(trans-of-implies1 n)
|
||||||
|
(list (quote implies)
|
||||||
|
0 n))))
|
||||||
|
|
||||||
|
(define (trans-of-implies1 n)
|
||||||
|
(cond ((equal? n 1)
|
||||||
|
(list (quote implies)
|
||||||
|
0 1))
|
||||||
|
(else (list (quote and)
|
||||||
|
(list (quote implies)
|
||||||
|
(- n 1)
|
||||||
|
n)
|
||||||
|
(trans-of-implies1 (- n 1))))))
|
||||||
|
|
||||||
|
; Translated terms can be circular structures, which can't be
|
||||||
|
; compared using Scheme's equal? and member procedures, so we
|
||||||
|
; use these instead.
|
||||||
|
|
||||||
|
(define (term-equal? x y)
|
||||||
|
(cond ((pair? x)
|
||||||
|
(and (pair? y)
|
||||||
|
(symbol-record-equal? (car x) (car y))
|
||||||
|
(term-args-equal? (cdr x) (cdr y))))
|
||||||
|
(else (equal? x y))))
|
||||||
|
|
||||||
|
(define (term-args-equal? lst1 lst2)
|
||||||
|
(cond ((null? lst1)
|
||||||
|
(null? lst2))
|
||||||
|
((null? lst2)
|
||||||
|
#f)
|
||||||
|
((term-equal? (car lst1) (car lst2))
|
||||||
|
(term-args-equal? (cdr lst1) (cdr lst2)))
|
||||||
|
(else #f)))
|
||||||
|
|
||||||
|
(define (term-member? x lst)
|
||||||
|
(cond ((null? lst)
|
||||||
|
#f)
|
||||||
|
((term-equal? x (car lst))
|
||||||
|
#t)
|
||||||
|
(else (term-member? x (cdr lst)))))
|
||||||
|
|
||||||
|
(set! setup-boyer
|
||||||
|
(lambda ()
|
||||||
|
(set! *symbol-records-alist* '())
|
||||||
|
(set! if-constructor (symbol->symbol-record 'if))
|
||||||
|
(set! false-term (translate-term '(f)))
|
||||||
|
(set! true-term (translate-term '(t)))
|
||||||
|
(setup)))
|
||||||
|
|
||||||
|
(set! test-boyer
|
||||||
|
(lambda (n)
|
||||||
|
(set! rewrite-count 0)
|
||||||
|
(let ((answer (test n)))
|
||||||
|
(write rewrite-count)
|
||||||
|
(display " rewrites")
|
||||||
|
(newline)
|
||||||
|
(if answer
|
||||||
|
rewrite-count
|
||||||
|
#f)))))
|
||||||
3772
gc-benchmarks/larceny/nucleic2.sch
Normal file
3772
gc-benchmarks/larceny/nucleic2.sch
Normal file
File diff suppressed because it is too large
Load diff
324
gc-benchmarks/larceny/perm.sch
Normal file
324
gc-benchmarks/larceny/perm.sch
Normal file
|
|
@ -0,0 +1,324 @@
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
; File: perm9.sch
|
||||||
|
; Description: memory system benchmark using Zaks's permutation generator
|
||||||
|
; Author: Lars Hansen, Will Clinger, and Gene Luks
|
||||||
|
; Created: 18-Mar-94
|
||||||
|
; Language: Scheme
|
||||||
|
; Status: Public Domain
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
|
; 940720 / lth Added some more benchmarks for the thesis paper.
|
||||||
|
; 970215 / wdc Increased problem size from 8 to 9; improved tenperm9-benchmark.
|
||||||
|
; 970531 / wdc Cleaned up for public release.
|
||||||
|
; 000820 / wdc Added the MpermNKL benchmark; revised for new run-benchmark.
|
||||||
|
|
||||||
|
; This benchmark is in four parts. Each tests a different aspect of
|
||||||
|
; the memory system.
|
||||||
|
;
|
||||||
|
; perm storage allocation
|
||||||
|
; 10perm storage allocation and garbage collection
|
||||||
|
; sumperms traversal of a large, linked, self-sharing structure
|
||||||
|
; mergesort! side effects and write barrier
|
||||||
|
;
|
||||||
|
; The perm9 benchmark generates a list of all 362880 permutations of
|
||||||
|
; the first 9 integers, allocating 1349288 pairs (typically 10,794,304
|
||||||
|
; bytes), all of which goes into the generated list. (That is, the
|
||||||
|
; perm9 benchmark generates absolutely no garbage.) This represents
|
||||||
|
; a savings of about 63% over the storage that would be required by
|
||||||
|
; an unshared list of permutations. The generated permutations are
|
||||||
|
; in order of a grey code that bears no obvious relationship to a
|
||||||
|
; lexicographic order.
|
||||||
|
;
|
||||||
|
; The 10perm9 benchmark repeats the perm9 benchmark 10 times, so it
|
||||||
|
; allocates and reclaims 13492880 pairs (typically 107,943,040 bytes).
|
||||||
|
; The live storage peaks at twice the storage that is allocated by the
|
||||||
|
; perm9 benchmark. At the end of each iteration, the oldest half of
|
||||||
|
; the live storage becomes garbage. Object lifetimes are distributed
|
||||||
|
; uniformly between 10.3 and 20.6 megabytes.
|
||||||
|
;
|
||||||
|
; The 10perm9 benchmark is the 10perm9:2:1 special case of the
|
||||||
|
; MpermNKL benchmark, which allocates a queue of size K and then
|
||||||
|
; performs M iterations of the following operation: Fill the queue
|
||||||
|
; with individually computed copies of all permutations of a list of
|
||||||
|
; size N, and then remove the oldest L copies from the queue. At the
|
||||||
|
; end of each iteration, the oldest L/K of the live storage becomes
|
||||||
|
; garbage, and object lifetimes are distributed uniformly between two
|
||||||
|
; volumes that depend upon N, K, and L.
|
||||||
|
;
|
||||||
|
; The sumperms benchmark computes the sum of the permuted integers
|
||||||
|
; over all permutations.
|
||||||
|
;
|
||||||
|
; The mergesort! benchmark destructively sorts the generated permutations
|
||||||
|
; into lexicographic order, allocating no storage whatsoever.
|
||||||
|
;
|
||||||
|
; The benchmarks are run by calling the following procedures:
|
||||||
|
;
|
||||||
|
; (perm-benchmark n)
|
||||||
|
; (tenperm-benchmark n)
|
||||||
|
; (sumperms-benchmark n)
|
||||||
|
; (mergesort-benchmark n)
|
||||||
|
;
|
||||||
|
; The argument n may be omitted, in which case it defaults to 9.
|
||||||
|
;
|
||||||
|
; These benchmarks assume that
|
||||||
|
;
|
||||||
|
; (RUN-BENCHMARK <string> <thunk> <count>)
|
||||||
|
; (RUN-BENCHMARK <string> <count> <thunk> <predicate>)
|
||||||
|
;
|
||||||
|
; reports the time required to call <thunk> the number of times
|
||||||
|
; specified by <count>, and uses <predicate> to test whether the
|
||||||
|
; result returned by <thunk> is correct.
|
||||||
|
|
||||||
|
; Date: Thu, 17 Mar 94 19:43:32 -0800
|
||||||
|
; From: luks@sisters.cs.uoregon.edu
|
||||||
|
; To: will
|
||||||
|
; Subject: Pancake flips
|
||||||
|
;
|
||||||
|
; Procedure P_n generates a grey code of all perms of n elements
|
||||||
|
; on top of stack ending with reversal of starting sequence
|
||||||
|
;
|
||||||
|
; F_n is flip of top n elements.
|
||||||
|
;
|
||||||
|
;
|
||||||
|
; procedure P_n
|
||||||
|
;
|
||||||
|
; if n>1 then
|
||||||
|
; begin
|
||||||
|
; repeat P_{n-1},F_n n-1 times;
|
||||||
|
; P_{n-1}
|
||||||
|
; end
|
||||||
|
;
|
||||||
|
|
||||||
|
(define (permutations x)
|
||||||
|
(let ((x x)
|
||||||
|
(perms (list x)))
|
||||||
|
(define (P n)
|
||||||
|
(if (> n 1)
|
||||||
|
(do ((j (- n 1) (- j 1)))
|
||||||
|
((zero? j)
|
||||||
|
(P (- n 1)))
|
||||||
|
(P (- n 1))
|
||||||
|
(F n))))
|
||||||
|
(define (F n)
|
||||||
|
(set! x (revloop x n (list-tail x n)))
|
||||||
|
(set! perms (cons x perms)))
|
||||||
|
(define (revloop x n y)
|
||||||
|
(if (zero? n)
|
||||||
|
y
|
||||||
|
(revloop (cdr x)
|
||||||
|
(- n 1)
|
||||||
|
(cons (car x) y))))
|
||||||
|
(define (list-tail x n)
|
||||||
|
(if (zero? n)
|
||||||
|
x
|
||||||
|
(list-tail (cdr x) (- n 1))))
|
||||||
|
(P (length x))
|
||||||
|
perms))
|
||||||
|
|
||||||
|
; Given a list of lists of numbers, returns the sum of the sums
|
||||||
|
; of those lists.
|
||||||
|
;
|
||||||
|
; for (; x != NULL; x = x->rest)
|
||||||
|
; for (y = x->first; y != NULL; y = y->rest)
|
||||||
|
; sum = sum + y->first;
|
||||||
|
|
||||||
|
(define (sumlists x)
|
||||||
|
(do ((x x (cdr x))
|
||||||
|
(sum 0 (do ((y (car x) (cdr y))
|
||||||
|
(sum sum (+ sum (car y))))
|
||||||
|
((null? y) sum))))
|
||||||
|
((null? x) sum)))
|
||||||
|
|
||||||
|
; Destructive merge of two sorted lists.
|
||||||
|
; From Hansen's MS thesis.
|
||||||
|
|
||||||
|
(define (merge!! a b less?)
|
||||||
|
|
||||||
|
(define (loop r a b)
|
||||||
|
(if (less? (car b) (car a))
|
||||||
|
(begin (set-cdr! r b)
|
||||||
|
(if (null? (cdr b))
|
||||||
|
(set-cdr! b a)
|
||||||
|
(loop b a (cdr b)) ))
|
||||||
|
;; (car a) <= (car b)
|
||||||
|
(begin (set-cdr! r a)
|
||||||
|
(if (null? (cdr a))
|
||||||
|
(set-cdr! a b)
|
||||||
|
(loop a (cdr a) b)) )) )
|
||||||
|
|
||||||
|
(cond ((null? a) b)
|
||||||
|
((null? b) a)
|
||||||
|
((less? (car b) (car a))
|
||||||
|
(if (null? (cdr b))
|
||||||
|
(set-cdr! b a)
|
||||||
|
(loop b a (cdr b)))
|
||||||
|
b)
|
||||||
|
(else ; (car a) <= (car b)
|
||||||
|
(if (null? (cdr a))
|
||||||
|
(set-cdr! a b)
|
||||||
|
(loop a (cdr a) b))
|
||||||
|
a)))
|
||||||
|
|
||||||
|
|
||||||
|
;; Stable sort procedure which copies the input list and then sorts
|
||||||
|
;; the new list imperatively. On the systems we have benchmarked,
|
||||||
|
;; this generic list sort has been at least as fast and usually much
|
||||||
|
;; faster than the library's sort routine.
|
||||||
|
;; Due to Richard O'Keefe; algorithm attributed to D.H.D. Warren.
|
||||||
|
|
||||||
|
(define (sort!! seq less?)
|
||||||
|
|
||||||
|
(define (step n)
|
||||||
|
(cond ((> n 2)
|
||||||
|
(let* ((j (quotient n 2))
|
||||||
|
(a (step j))
|
||||||
|
(k (- n j))
|
||||||
|
(b (step k)))
|
||||||
|
(merge!! a b less?)))
|
||||||
|
((= n 2)
|
||||||
|
(let ((x (car seq))
|
||||||
|
(y (cadr seq))
|
||||||
|
(p seq))
|
||||||
|
(set! seq (cddr seq))
|
||||||
|
(if (less? y x)
|
||||||
|
(begin
|
||||||
|
(set-car! p y)
|
||||||
|
(set-car! (cdr p) x)))
|
||||||
|
(set-cdr! (cdr p) '())
|
||||||
|
p))
|
||||||
|
((= n 1)
|
||||||
|
(let ((p seq))
|
||||||
|
(set! seq (cdr seq))
|
||||||
|
(set-cdr! p '())
|
||||||
|
p))
|
||||||
|
(else
|
||||||
|
'())))
|
||||||
|
|
||||||
|
(step (length seq)))
|
||||||
|
|
||||||
|
(define lexicographically-less?
|
||||||
|
(lambda (x y)
|
||||||
|
(define (lexicographically-less? x y)
|
||||||
|
(cond ((null? x) (not (null? y)))
|
||||||
|
((null? y) #f)
|
||||||
|
((< (car x) (car y)) #t)
|
||||||
|
((= (car x) (car y))
|
||||||
|
(lexicographically-less? (cdr x) (cdr y)))
|
||||||
|
(else #f)))
|
||||||
|
(lexicographically-less? x y)))
|
||||||
|
|
||||||
|
; This procedure isn't used by the benchmarks,
|
||||||
|
; but is provided as a public service.
|
||||||
|
|
||||||
|
(define (internally-imperative-mergesort list less?)
|
||||||
|
|
||||||
|
(define (list-copy l)
|
||||||
|
(define (loop l prev)
|
||||||
|
(if (null? l)
|
||||||
|
#t
|
||||||
|
(let ((q (cons (car l) '())))
|
||||||
|
(set-cdr! prev q)
|
||||||
|
(loop (cdr l) q))))
|
||||||
|
(if (null? l)
|
||||||
|
l
|
||||||
|
(let ((first (cons (car l) '())))
|
||||||
|
(loop (cdr l) first)
|
||||||
|
first)))
|
||||||
|
|
||||||
|
(sort!! (list-copy list) less?))
|
||||||
|
|
||||||
|
(define *perms* '())
|
||||||
|
|
||||||
|
(define (one..n n)
|
||||||
|
(do ((n n (- n 1))
|
||||||
|
(p '() (cons n p)))
|
||||||
|
((zero? n) p)))
|
||||||
|
|
||||||
|
(define (perm-benchmark . rest)
|
||||||
|
(let ((n (if (null? rest) 9 (car rest))))
|
||||||
|
(set! *perms* '())
|
||||||
|
(run-benchmark (string-append "Perm" (number->string n))
|
||||||
|
1
|
||||||
|
(lambda ()
|
||||||
|
(set! *perms* (permutations (one..n n)))
|
||||||
|
#t)
|
||||||
|
(lambda (x) #t))))
|
||||||
|
|
||||||
|
(define (tenperm-benchmark . rest)
|
||||||
|
(let ((n (if (null? rest) 9 (car rest))))
|
||||||
|
(set! *perms* '())
|
||||||
|
(MpermNKL-benchmark 10 n 2 1)))
|
||||||
|
|
||||||
|
(define (MpermNKL-benchmark m n k ell)
|
||||||
|
(if (and (<= 0 m)
|
||||||
|
(positive? n)
|
||||||
|
(positive? k)
|
||||||
|
(<= 0 ell k))
|
||||||
|
(let ((id (string-append (number->string m)
|
||||||
|
"perm"
|
||||||
|
(number->string n)
|
||||||
|
":"
|
||||||
|
(number->string k)
|
||||||
|
":"
|
||||||
|
(number->string ell)))
|
||||||
|
(queue (make-vector k '())))
|
||||||
|
|
||||||
|
; Fills queue positions [i, j).
|
||||||
|
|
||||||
|
(define (fill-queue i j)
|
||||||
|
(if (< i j)
|
||||||
|
(begin (vector-set! queue i (permutations (one..n n)))
|
||||||
|
(fill-queue (+ i 1) j))))
|
||||||
|
|
||||||
|
; Removes ell elements from queue.
|
||||||
|
|
||||||
|
(define (flush-queue)
|
||||||
|
(let loop ((i 0))
|
||||||
|
(if (< i k)
|
||||||
|
(begin (vector-set! queue
|
||||||
|
i
|
||||||
|
(let ((j (+ i ell)))
|
||||||
|
(if (< j k)
|
||||||
|
(vector-ref queue j)
|
||||||
|
'())))
|
||||||
|
(loop (+ i 1))))))
|
||||||
|
|
||||||
|
(fill-queue 0 (- k ell))
|
||||||
|
(run-benchmark id
|
||||||
|
m
|
||||||
|
(lambda ()
|
||||||
|
(fill-queue (- k ell) k)
|
||||||
|
(flush-queue)
|
||||||
|
queue)
|
||||||
|
(lambda (q)
|
||||||
|
(let ((q0 (vector-ref q 0))
|
||||||
|
(qi (vector-ref q (max 0 (- k ell 1)))))
|
||||||
|
(or (and (null? q0) (null? qi))
|
||||||
|
(and (pair? q0)
|
||||||
|
(pair? qi)
|
||||||
|
(equal? (car q0) (car qi))))))))
|
||||||
|
(begin (display "Incorrect arguments to MpermNKL-benchmark")
|
||||||
|
(newline))))
|
||||||
|
|
||||||
|
(define (sumperms-benchmark . rest)
|
||||||
|
(let ((n (if (null? rest) 9 (car rest))))
|
||||||
|
(if (or (null? *perms*)
|
||||||
|
(not (= n (length (car *perms*)))))
|
||||||
|
(set! *perms* (permutations (one..n n))))
|
||||||
|
(run-benchmark (string-append "Sumperms" (number->string n))
|
||||||
|
1
|
||||||
|
(lambda ()
|
||||||
|
(sumlists *perms*))
|
||||||
|
(lambda (x) #t))))
|
||||||
|
|
||||||
|
(define (mergesort-benchmark . rest)
|
||||||
|
(let ((n (if (null? rest) 9 (car rest))))
|
||||||
|
(if (or (null? *perms*)
|
||||||
|
(not (= n (length (car *perms*)))))
|
||||||
|
(set! *perms* (permutations (one..n n))))
|
||||||
|
(run-benchmark (string-append "Mergesort!" (number->string n))
|
||||||
|
1
|
||||||
|
(lambda ()
|
||||||
|
(sort!! *perms* lexicographically-less?)
|
||||||
|
#t)
|
||||||
|
(lambda (x) #t))))
|
||||||
50
gc-benchmarks/larceny/run-benchmark.chez
Normal file
50
gc-benchmarks/larceny/run-benchmark.chez
Normal file
|
|
@ -0,0 +1,50 @@
|
||||||
|
;;; Gambit-style run-benchmark.
|
||||||
|
;;;
|
||||||
|
;;; Invoke this procedure to run a benchmark.
|
||||||
|
;;; The first argument is a string identifying the benchmark.
|
||||||
|
;;; The second argument is the number of times to run the benchmark.
|
||||||
|
;;; The third argument is a thunk that runs the benchmark.
|
||||||
|
;;; The fourth argument is a unary predicate that warns if the result
|
||||||
|
;;; returned by the benchmark is incorrect.
|
||||||
|
;;;
|
||||||
|
;;; Example:
|
||||||
|
;;; (run-benchmark "make-vector"
|
||||||
|
;;; 1
|
||||||
|
;;; (lambda () (make-vector 1000000))
|
||||||
|
;;; (lambda (v) (and (vector? v) (= (vector-length v) #e1e6))))
|
||||||
|
|
||||||
|
;;; For backward compatibility, this procedure also works with the
|
||||||
|
;;; arguments that we once used to run benchmarks in Larceny.
|
||||||
|
|
||||||
|
(define (run-benchmark name arg2 . rest)
|
||||||
|
(let* ((old-style (procedure? arg2))
|
||||||
|
(thunk (if old-style arg2 (car rest)))
|
||||||
|
(n (if old-style
|
||||||
|
(if (null? rest) 1 (car rest))
|
||||||
|
arg2))
|
||||||
|
(ok? (if (or old-style (null? (cdr rest)))
|
||||||
|
(lambda (result) #t)
|
||||||
|
(cadr rest)))
|
||||||
|
(result '*))
|
||||||
|
(define (loop n)
|
||||||
|
(cond ((zero? n) #t)
|
||||||
|
((= n 1)
|
||||||
|
(set! result (thunk)))
|
||||||
|
(else
|
||||||
|
(thunk)
|
||||||
|
(loop (- n 1)))))
|
||||||
|
(if old-style
|
||||||
|
(begin (newline)
|
||||||
|
(display "Warning: Using old-style run-benchmark")
|
||||||
|
(newline)))
|
||||||
|
(newline)
|
||||||
|
(display "--------------------------------------------------------")
|
||||||
|
(newline)
|
||||||
|
(display name)
|
||||||
|
(newline)
|
||||||
|
; time is a macro supplied by Chez Scheme
|
||||||
|
(time (loop n))
|
||||||
|
(if (not (ok? result))
|
||||||
|
(begin (display "Error: Benchmark program returned wrong result: ")
|
||||||
|
(write result)
|
||||||
|
(newline)))))
|
||||||
784
gc-benchmarks/larceny/sboyer.sch
Normal file
784
gc-benchmarks/larceny/sboyer.sch
Normal file
|
|
@ -0,0 +1,784 @@
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
; File: sboyer.sch
|
||||||
|
; Description: The Boyer benchmark
|
||||||
|
; Author: Bob Boyer
|
||||||
|
; Created: 5-Apr-85
|
||||||
|
; Modified: 10-Apr-85 14:52:20 (Bob Shaw)
|
||||||
|
; 22-Jul-87 (Will Clinger)
|
||||||
|
; 2-Jul-88 (Will Clinger -- distinguished #f and the empty list)
|
||||||
|
; 13-Feb-97 (Will Clinger -- fixed bugs in unifier and rules,
|
||||||
|
; rewrote to eliminate property lists, and added
|
||||||
|
; a scaling parameter suggested by Bob Boyer)
|
||||||
|
; 19-Mar-99 (Will Clinger -- cleaned up comments)
|
||||||
|
; 4-Apr-01 (Will Clinger -- changed four 1- symbols to sub1)
|
||||||
|
; Language: Scheme
|
||||||
|
; Status: Public Domain
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
|
;;; SBOYER -- Logic programming benchmark, originally written by Bob Boyer.
|
||||||
|
;;; Much less CONS-intensive than NBOYER because it uses Henry Baker's
|
||||||
|
;;; "sharing cons".
|
||||||
|
|
||||||
|
; Note: The version of this benchmark that appears in Dick Gabriel's book
|
||||||
|
; contained several bugs that are corrected here. These bugs are discussed
|
||||||
|
; by Henry Baker, "The Boyer Benchmark Meets Linear Logic", ACM SIGPLAN Lisp
|
||||||
|
; Pointers 6(4), October-December 1993, pages 3-10. The fixed bugs are:
|
||||||
|
;
|
||||||
|
; The benchmark now returns a boolean result.
|
||||||
|
; FALSEP and TRUEP use TERM-MEMBER? rather than MEMV (which is called MEMBER
|
||||||
|
; in Common Lisp)
|
||||||
|
; ONE-WAY-UNIFY1 now treats numbers correctly
|
||||||
|
; ONE-WAY-UNIFY1-LST now treats empty lists correctly
|
||||||
|
; Rule 19 has been corrected (this rule was not touched by the original
|
||||||
|
; benchmark, but is used by this version)
|
||||||
|
; Rules 84 and 101 have been corrected (but these rules are never touched
|
||||||
|
; by the benchmark)
|
||||||
|
;
|
||||||
|
; According to Baker, these bug fixes make the benchmark 10-25% slower.
|
||||||
|
; Please do not compare the timings from this benchmark against those of
|
||||||
|
; the original benchmark.
|
||||||
|
;
|
||||||
|
; This version of the benchmark also prints the number of rewrites as a sanity
|
||||||
|
; check, because it is too easy for a buggy version to return the correct
|
||||||
|
; boolean result. The correct number of rewrites is
|
||||||
|
;
|
||||||
|
; n rewrites peak live storage (approximate, in bytes)
|
||||||
|
; 0 95024
|
||||||
|
; 1 591777
|
||||||
|
; 2 1813975
|
||||||
|
; 3 5375678
|
||||||
|
; 4 16445406
|
||||||
|
; 5 51507739
|
||||||
|
|
||||||
|
; Sboyer is a 2-phase benchmark.
|
||||||
|
; The first phase attaches lemmas to symbols. This phase is not timed,
|
||||||
|
; but it accounts for very little of the runtime anyway.
|
||||||
|
; The second phase creates the test problem, and tests to see
|
||||||
|
; whether it is implied by the lemmas.
|
||||||
|
|
||||||
|
(define (sboyer-benchmark . args)
|
||||||
|
(let ((n (if (null? args) 0 (car args))))
|
||||||
|
(setup-boyer)
|
||||||
|
(run-benchmark (string-append "sboyer"
|
||||||
|
(number->string n))
|
||||||
|
1
|
||||||
|
(lambda () (test-boyer n))
|
||||||
|
(lambda (rewrites)
|
||||||
|
(and (number? rewrites)
|
||||||
|
(case n
|
||||||
|
((0) (= rewrites 95024))
|
||||||
|
((1) (= rewrites 591777))
|
||||||
|
((2) (= rewrites 1813975))
|
||||||
|
((3) (= rewrites 5375678))
|
||||||
|
((4) (= rewrites 16445406))
|
||||||
|
((5) (= rewrites 51507739))
|
||||||
|
; If it works for n <= 5, assume it works.
|
||||||
|
(else #t)))))))
|
||||||
|
|
||||||
|
(define (setup-boyer) #t) ; assigned below
|
||||||
|
(define (test-boyer) #t) ; assigned below
|
||||||
|
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
;
|
||||||
|
; The first phase.
|
||||||
|
;
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
|
; In the original benchmark, it stored a list of lemmas on the
|
||||||
|
; property lists of symbols.
|
||||||
|
; In the new benchmark, it maintains an association list of
|
||||||
|
; symbols and symbol-records, and stores the list of lemmas
|
||||||
|
; within the symbol-records.
|
||||||
|
|
||||||
|
(let ()
|
||||||
|
|
||||||
|
(define (setup)
|
||||||
|
(add-lemma-lst
|
||||||
|
(quote ((equal (compile form)
|
||||||
|
(reverse (codegen (optimize form)
|
||||||
|
(nil))))
|
||||||
|
(equal (eqp x y)
|
||||||
|
(equal (fix x)
|
||||||
|
(fix y)))
|
||||||
|
(equal (greaterp x y)
|
||||||
|
(lessp y x))
|
||||||
|
(equal (lesseqp x y)
|
||||||
|
(not (lessp y x)))
|
||||||
|
(equal (greatereqp x y)
|
||||||
|
(not (lessp x y)))
|
||||||
|
(equal (boolean x)
|
||||||
|
(or (equal x (t))
|
||||||
|
(equal x (f))))
|
||||||
|
(equal (iff x y)
|
||||||
|
(and (implies x y)
|
||||||
|
(implies y x)))
|
||||||
|
(equal (even1 x)
|
||||||
|
(if (zerop x)
|
||||||
|
(t)
|
||||||
|
(odd (sub1 x))))
|
||||||
|
(equal (countps- l pred)
|
||||||
|
(countps-loop l pred (zero)))
|
||||||
|
(equal (fact- i)
|
||||||
|
(fact-loop i 1))
|
||||||
|
(equal (reverse- x)
|
||||||
|
(reverse-loop x (nil)))
|
||||||
|
(equal (divides x y)
|
||||||
|
(zerop (remainder y x)))
|
||||||
|
(equal (assume-true var alist)
|
||||||
|
(cons (cons var (t))
|
||||||
|
alist))
|
||||||
|
(equal (assume-false var alist)
|
||||||
|
(cons (cons var (f))
|
||||||
|
alist))
|
||||||
|
(equal (tautology-checker x)
|
||||||
|
(tautologyp (normalize x)
|
||||||
|
(nil)))
|
||||||
|
(equal (falsify x)
|
||||||
|
(falsify1 (normalize x)
|
||||||
|
(nil)))
|
||||||
|
(equal (prime x)
|
||||||
|
(and (not (zerop x))
|
||||||
|
(not (equal x (add1 (zero))))
|
||||||
|
(prime1 x (sub1 x))))
|
||||||
|
(equal (and p q)
|
||||||
|
(if p (if q (t)
|
||||||
|
(f))
|
||||||
|
(f)))
|
||||||
|
(equal (or p q)
|
||||||
|
(if p (t)
|
||||||
|
(if q (t)
|
||||||
|
(f))))
|
||||||
|
(equal (not p)
|
||||||
|
(if p (f)
|
||||||
|
(t)))
|
||||||
|
(equal (implies p q)
|
||||||
|
(if p (if q (t)
|
||||||
|
(f))
|
||||||
|
(t)))
|
||||||
|
(equal (fix x)
|
||||||
|
(if (numberp x)
|
||||||
|
x
|
||||||
|
(zero)))
|
||||||
|
(equal (if (if a b c)
|
||||||
|
d e)
|
||||||
|
(if a (if b d e)
|
||||||
|
(if c d e)))
|
||||||
|
(equal (zerop x)
|
||||||
|
(or (equal x (zero))
|
||||||
|
(not (numberp x))))
|
||||||
|
(equal (plus (plus x y)
|
||||||
|
z)
|
||||||
|
(plus x (plus y z)))
|
||||||
|
(equal (equal (plus a b)
|
||||||
|
(zero))
|
||||||
|
(and (zerop a)
|
||||||
|
(zerop b)))
|
||||||
|
(equal (difference x x)
|
||||||
|
(zero))
|
||||||
|
(equal (equal (plus a b)
|
||||||
|
(plus a c))
|
||||||
|
(equal (fix b)
|
||||||
|
(fix c)))
|
||||||
|
(equal (equal (zero)
|
||||||
|
(difference x y))
|
||||||
|
(not (lessp y x)))
|
||||||
|
(equal (equal x (difference x y))
|
||||||
|
(and (numberp x)
|
||||||
|
(or (equal x (zero))
|
||||||
|
(zerop y))))
|
||||||
|
(equal (meaning (plus-tree (append x y))
|
||||||
|
a)
|
||||||
|
(plus (meaning (plus-tree x)
|
||||||
|
a)
|
||||||
|
(meaning (plus-tree y)
|
||||||
|
a)))
|
||||||
|
(equal (meaning (plus-tree (plus-fringe x))
|
||||||
|
a)
|
||||||
|
(fix (meaning x a)))
|
||||||
|
(equal (append (append x y)
|
||||||
|
z)
|
||||||
|
(append x (append y z)))
|
||||||
|
(equal (reverse (append a b))
|
||||||
|
(append (reverse b)
|
||||||
|
(reverse a)))
|
||||||
|
(equal (times x (plus y z))
|
||||||
|
(plus (times x y)
|
||||||
|
(times x z)))
|
||||||
|
(equal (times (times x y)
|
||||||
|
z)
|
||||||
|
(times x (times y z)))
|
||||||
|
(equal (equal (times x y)
|
||||||
|
(zero))
|
||||||
|
(or (zerop x)
|
||||||
|
(zerop y)))
|
||||||
|
(equal (exec (append x y)
|
||||||
|
pds envrn)
|
||||||
|
(exec y (exec x pds envrn)
|
||||||
|
envrn))
|
||||||
|
(equal (mc-flatten x y)
|
||||||
|
(append (flatten x)
|
||||||
|
y))
|
||||||
|
(equal (member x (append a b))
|
||||||
|
(or (member x a)
|
||||||
|
(member x b)))
|
||||||
|
(equal (member x (reverse y))
|
||||||
|
(member x y))
|
||||||
|
(equal (length (reverse x))
|
||||||
|
(length x))
|
||||||
|
(equal (member a (intersect b c))
|
||||||
|
(and (member a b)
|
||||||
|
(member a c)))
|
||||||
|
(equal (nth (zero)
|
||||||
|
i)
|
||||||
|
(zero))
|
||||||
|
(equal (exp i (plus j k))
|
||||||
|
(times (exp i j)
|
||||||
|
(exp i k)))
|
||||||
|
(equal (exp i (times j k))
|
||||||
|
(exp (exp i j)
|
||||||
|
k))
|
||||||
|
(equal (reverse-loop x y)
|
||||||
|
(append (reverse x)
|
||||||
|
y))
|
||||||
|
(equal (reverse-loop x (nil))
|
||||||
|
(reverse x))
|
||||||
|
(equal (count-list z (sort-lp x y))
|
||||||
|
(plus (count-list z x)
|
||||||
|
(count-list z y)))
|
||||||
|
(equal (equal (append a b)
|
||||||
|
(append a c))
|
||||||
|
(equal b c))
|
||||||
|
(equal (plus (remainder x y)
|
||||||
|
(times y (quotient x y)))
|
||||||
|
(fix x))
|
||||||
|
(equal (power-eval (big-plus1 l i base)
|
||||||
|
base)
|
||||||
|
(plus (power-eval l base)
|
||||||
|
i))
|
||||||
|
(equal (power-eval (big-plus x y i base)
|
||||||
|
base)
|
||||||
|
(plus i (plus (power-eval x base)
|
||||||
|
(power-eval y base))))
|
||||||
|
(equal (remainder y 1)
|
||||||
|
(zero))
|
||||||
|
(equal (lessp (remainder x y)
|
||||||
|
y)
|
||||||
|
(not (zerop y)))
|
||||||
|
(equal (remainder x x)
|
||||||
|
(zero))
|
||||||
|
(equal (lessp (quotient i j)
|
||||||
|
i)
|
||||||
|
(and (not (zerop i))
|
||||||
|
(or (zerop j)
|
||||||
|
(not (equal j 1)))))
|
||||||
|
(equal (lessp (remainder x y)
|
||||||
|
x)
|
||||||
|
(and (not (zerop y))
|
||||||
|
(not (zerop x))
|
||||||
|
(not (lessp x y))))
|
||||||
|
(equal (power-eval (power-rep i base)
|
||||||
|
base)
|
||||||
|
(fix i))
|
||||||
|
(equal (power-eval (big-plus (power-rep i base)
|
||||||
|
(power-rep j base)
|
||||||
|
(zero)
|
||||||
|
base)
|
||||||
|
base)
|
||||||
|
(plus i j))
|
||||||
|
(equal (gcd x y)
|
||||||
|
(gcd y x))
|
||||||
|
(equal (nth (append a b)
|
||||||
|
i)
|
||||||
|
(append (nth a i)
|
||||||
|
(nth b (difference i (length a)))))
|
||||||
|
(equal (difference (plus x y)
|
||||||
|
x)
|
||||||
|
(fix y))
|
||||||
|
(equal (difference (plus y x)
|
||||||
|
x)
|
||||||
|
(fix y))
|
||||||
|
(equal (difference (plus x y)
|
||||||
|
(plus x z))
|
||||||
|
(difference y z))
|
||||||
|
(equal (times x (difference c w))
|
||||||
|
(difference (times c x)
|
||||||
|
(times w x)))
|
||||||
|
(equal (remainder (times x z)
|
||||||
|
z)
|
||||||
|
(zero))
|
||||||
|
(equal (difference (plus b (plus a c))
|
||||||
|
a)
|
||||||
|
(plus b c))
|
||||||
|
(equal (difference (add1 (plus y z))
|
||||||
|
z)
|
||||||
|
(add1 y))
|
||||||
|
(equal (lessp (plus x y)
|
||||||
|
(plus x z))
|
||||||
|
(lessp y z))
|
||||||
|
(equal (lessp (times x z)
|
||||||
|
(times y z))
|
||||||
|
(and (not (zerop z))
|
||||||
|
(lessp x y)))
|
||||||
|
(equal (lessp y (plus x y))
|
||||||
|
(not (zerop x)))
|
||||||
|
(equal (gcd (times x z)
|
||||||
|
(times y z))
|
||||||
|
(times z (gcd x y)))
|
||||||
|
(equal (value (normalize x)
|
||||||
|
a)
|
||||||
|
(value x a))
|
||||||
|
(equal (equal (flatten x)
|
||||||
|
(cons y (nil)))
|
||||||
|
(and (nlistp x)
|
||||||
|
(equal x y)))
|
||||||
|
(equal (listp (gopher x))
|
||||||
|
(listp x))
|
||||||
|
(equal (samefringe x y)
|
||||||
|
(equal (flatten x)
|
||||||
|
(flatten y)))
|
||||||
|
(equal (equal (greatest-factor x y)
|
||||||
|
(zero))
|
||||||
|
(and (or (zerop y)
|
||||||
|
(equal y 1))
|
||||||
|
(equal x (zero))))
|
||||||
|
(equal (equal (greatest-factor x y)
|
||||||
|
1)
|
||||||
|
(equal x 1))
|
||||||
|
(equal (numberp (greatest-factor x y))
|
||||||
|
(not (and (or (zerop y)
|
||||||
|
(equal y 1))
|
||||||
|
(not (numberp x)))))
|
||||||
|
(equal (times-list (append x y))
|
||||||
|
(times (times-list x)
|
||||||
|
(times-list y)))
|
||||||
|
(equal (prime-list (append x y))
|
||||||
|
(and (prime-list x)
|
||||||
|
(prime-list y)))
|
||||||
|
(equal (equal z (times w z))
|
||||||
|
(and (numberp z)
|
||||||
|
(or (equal z (zero))
|
||||||
|
(equal w 1))))
|
||||||
|
(equal (greatereqp x y)
|
||||||
|
(not (lessp x y)))
|
||||||
|
(equal (equal x (times x y))
|
||||||
|
(or (equal x (zero))
|
||||||
|
(and (numberp x)
|
||||||
|
(equal y 1))))
|
||||||
|
(equal (remainder (times y x)
|
||||||
|
y)
|
||||||
|
(zero))
|
||||||
|
(equal (equal (times a b)
|
||||||
|
1)
|
||||||
|
(and (not (equal a (zero)))
|
||||||
|
(not (equal b (zero)))
|
||||||
|
(numberp a)
|
||||||
|
(numberp b)
|
||||||
|
(equal (sub1 a)
|
||||||
|
(zero))
|
||||||
|
(equal (sub1 b)
|
||||||
|
(zero))))
|
||||||
|
(equal (lessp (length (delete x l))
|
||||||
|
(length l))
|
||||||
|
(member x l))
|
||||||
|
(equal (sort2 (delete x l))
|
||||||
|
(delete x (sort2 l)))
|
||||||
|
(equal (dsort x)
|
||||||
|
(sort2 x))
|
||||||
|
(equal (length (cons x1
|
||||||
|
(cons x2
|
||||||
|
(cons x3 (cons x4
|
||||||
|
(cons x5
|
||||||
|
(cons x6 x7)))))))
|
||||||
|
(plus 6 (length x7)))
|
||||||
|
(equal (difference (add1 (add1 x))
|
||||||
|
2)
|
||||||
|
(fix x))
|
||||||
|
(equal (quotient (plus x (plus x y))
|
||||||
|
2)
|
||||||
|
(plus x (quotient y 2)))
|
||||||
|
(equal (sigma (zero)
|
||||||
|
i)
|
||||||
|
(quotient (times i (add1 i))
|
||||||
|
2))
|
||||||
|
(equal (plus x (add1 y))
|
||||||
|
(if (numberp y)
|
||||||
|
(add1 (plus x y))
|
||||||
|
(add1 x)))
|
||||||
|
(equal (equal (difference x y)
|
||||||
|
(difference z y))
|
||||||
|
(if (lessp x y)
|
||||||
|
(not (lessp y z))
|
||||||
|
(if (lessp z y)
|
||||||
|
(not (lessp y x))
|
||||||
|
(equal (fix x)
|
||||||
|
(fix z)))))
|
||||||
|
(equal (meaning (plus-tree (delete x y))
|
||||||
|
a)
|
||||||
|
(if (member x y)
|
||||||
|
(difference (meaning (plus-tree y)
|
||||||
|
a)
|
||||||
|
(meaning x a))
|
||||||
|
(meaning (plus-tree y)
|
||||||
|
a)))
|
||||||
|
(equal (times x (add1 y))
|
||||||
|
(if (numberp y)
|
||||||
|
(plus x (times x y))
|
||||||
|
(fix x)))
|
||||||
|
(equal (nth (nil)
|
||||||
|
i)
|
||||||
|
(if (zerop i)
|
||||||
|
(nil)
|
||||||
|
(zero)))
|
||||||
|
(equal (last (append a b))
|
||||||
|
(if (listp b)
|
||||||
|
(last b)
|
||||||
|
(if (listp a)
|
||||||
|
(cons (car (last a))
|
||||||
|
b)
|
||||||
|
b)))
|
||||||
|
(equal (equal (lessp x y)
|
||||||
|
z)
|
||||||
|
(if (lessp x y)
|
||||||
|
(equal (t) z)
|
||||||
|
(equal (f) z)))
|
||||||
|
(equal (assignment x (append a b))
|
||||||
|
(if (assignedp x a)
|
||||||
|
(assignment x a)
|
||||||
|
(assignment x b)))
|
||||||
|
(equal (car (gopher x))
|
||||||
|
(if (listp x)
|
||||||
|
(car (flatten x))
|
||||||
|
(zero)))
|
||||||
|
(equal (flatten (cdr (gopher x)))
|
||||||
|
(if (listp x)
|
||||||
|
(cdr (flatten x))
|
||||||
|
(cons (zero)
|
||||||
|
(nil))))
|
||||||
|
(equal (quotient (times y x)
|
||||||
|
y)
|
||||||
|
(if (zerop y)
|
||||||
|
(zero)
|
||||||
|
(fix x)))
|
||||||
|
(equal (get j (set i val mem))
|
||||||
|
(if (eqp j i)
|
||||||
|
val
|
||||||
|
(get j mem)))))))
|
||||||
|
|
||||||
|
(define (add-lemma-lst lst)
|
||||||
|
(cond ((null? lst)
|
||||||
|
#t)
|
||||||
|
(else (add-lemma (car lst))
|
||||||
|
(add-lemma-lst (cdr lst)))))
|
||||||
|
|
||||||
|
(define (add-lemma term)
|
||||||
|
(cond ((and (pair? term)
|
||||||
|
(eq? (car term)
|
||||||
|
(quote equal))
|
||||||
|
(pair? (cadr term)))
|
||||||
|
(put (car (cadr term))
|
||||||
|
(quote lemmas)
|
||||||
|
(cons
|
||||||
|
(translate-term term)
|
||||||
|
(get (car (cadr term)) (quote lemmas)))))
|
||||||
|
(else (error "ADD-LEMMA did not like term: " term))))
|
||||||
|
|
||||||
|
; Translates a term by replacing its constructor symbols by symbol-records.
|
||||||
|
|
||||||
|
(define (translate-term term)
|
||||||
|
(cond ((not (pair? term))
|
||||||
|
term)
|
||||||
|
(else (cons (symbol->symbol-record (car term))
|
||||||
|
(translate-args (cdr term))))))
|
||||||
|
|
||||||
|
(define (translate-args lst)
|
||||||
|
(cond ((null? lst)
|
||||||
|
'())
|
||||||
|
(else (cons (translate-term (car lst))
|
||||||
|
(translate-args (cdr lst))))))
|
||||||
|
|
||||||
|
; For debugging only, so the use of MAP does not change
|
||||||
|
; the first-order character of the benchmark.
|
||||||
|
|
||||||
|
(define (untranslate-term term)
|
||||||
|
(cond ((not (pair? term))
|
||||||
|
term)
|
||||||
|
(else (cons (get-name (car term))
|
||||||
|
(map untranslate-term (cdr term))))))
|
||||||
|
|
||||||
|
; A symbol-record is represented as a vector with two fields:
|
||||||
|
; the symbol (for debugging) and
|
||||||
|
; the list of lemmas associated with the symbol.
|
||||||
|
|
||||||
|
(define (put sym property value)
|
||||||
|
(put-lemmas! (symbol->symbol-record sym) value))
|
||||||
|
|
||||||
|
(define (get sym property)
|
||||||
|
(get-lemmas (symbol->symbol-record sym)))
|
||||||
|
|
||||||
|
(define (symbol->symbol-record sym)
|
||||||
|
(let ((x (assq sym *symbol-records-alist*)))
|
||||||
|
(if x
|
||||||
|
(cdr x)
|
||||||
|
(let ((r (make-symbol-record sym)))
|
||||||
|
(set! *symbol-records-alist*
|
||||||
|
(cons (cons sym r)
|
||||||
|
*symbol-records-alist*))
|
||||||
|
r))))
|
||||||
|
|
||||||
|
; Association list of symbols and symbol-records.
|
||||||
|
|
||||||
|
(define *symbol-records-alist* '())
|
||||||
|
|
||||||
|
; A symbol-record is represented as a vector with two fields:
|
||||||
|
; the symbol (for debugging) and
|
||||||
|
; the list of lemmas associated with the symbol.
|
||||||
|
|
||||||
|
(define (make-symbol-record sym)
|
||||||
|
(vector sym '()))
|
||||||
|
|
||||||
|
(define (put-lemmas! symbol-record lemmas)
|
||||||
|
(vector-set! symbol-record 1 lemmas))
|
||||||
|
|
||||||
|
(define (get-lemmas symbol-record)
|
||||||
|
(vector-ref symbol-record 1))
|
||||||
|
|
||||||
|
(define (get-name symbol-record)
|
||||||
|
(vector-ref symbol-record 0))
|
||||||
|
|
||||||
|
(define (symbol-record-equal? r1 r2)
|
||||||
|
(eq? r1 r2))
|
||||||
|
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
;
|
||||||
|
; The second phase.
|
||||||
|
;
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
|
(define (test n)
|
||||||
|
(let ((term
|
||||||
|
(apply-subst
|
||||||
|
(translate-alist
|
||||||
|
(quote ((x f (plus (plus a b)
|
||||||
|
(plus c (zero))))
|
||||||
|
(y f (times (times a b)
|
||||||
|
(plus c d)))
|
||||||
|
(z f (reverse (append (append a b)
|
||||||
|
(nil))))
|
||||||
|
(u equal (plus a b)
|
||||||
|
(difference x y))
|
||||||
|
(w lessp (remainder a b)
|
||||||
|
(member a (length b))))))
|
||||||
|
(translate-term
|
||||||
|
(do ((term
|
||||||
|
(quote (implies (and (implies x y)
|
||||||
|
(and (implies y z)
|
||||||
|
(and (implies z u)
|
||||||
|
(implies u w))))
|
||||||
|
(implies x w)))
|
||||||
|
(list 'or term '(f)))
|
||||||
|
(n n (- n 1)))
|
||||||
|
((zero? n) term))))))
|
||||||
|
(tautp term)))
|
||||||
|
|
||||||
|
(define (translate-alist alist)
|
||||||
|
(cond ((null? alist)
|
||||||
|
'())
|
||||||
|
(else (cons (cons (caar alist)
|
||||||
|
(translate-term (cdar alist)))
|
||||||
|
(translate-alist (cdr alist))))))
|
||||||
|
|
||||||
|
(define (apply-subst alist term)
|
||||||
|
(cond ((not (pair? term))
|
||||||
|
(let ((temp-temp (assq term alist)))
|
||||||
|
(if temp-temp
|
||||||
|
(cdr temp-temp)
|
||||||
|
term)))
|
||||||
|
(else (cons (car term)
|
||||||
|
(apply-subst-lst alist (cdr term))))))
|
||||||
|
|
||||||
|
(define (apply-subst-lst alist lst)
|
||||||
|
(cond ((null? lst)
|
||||||
|
'())
|
||||||
|
(else (cons (apply-subst alist (car lst))
|
||||||
|
(apply-subst-lst alist (cdr lst))))))
|
||||||
|
|
||||||
|
(define (tautp x)
|
||||||
|
(tautologyp (rewrite x)
|
||||||
|
'() '()))
|
||||||
|
|
||||||
|
(define (tautologyp x true-lst false-lst)
|
||||||
|
(cond ((truep x true-lst)
|
||||||
|
#t)
|
||||||
|
((falsep x false-lst)
|
||||||
|
#f)
|
||||||
|
((not (pair? x))
|
||||||
|
#f)
|
||||||
|
((eq? (car x) if-constructor)
|
||||||
|
(cond ((truep (cadr x)
|
||||||
|
true-lst)
|
||||||
|
(tautologyp (caddr x)
|
||||||
|
true-lst false-lst))
|
||||||
|
((falsep (cadr x)
|
||||||
|
false-lst)
|
||||||
|
(tautologyp (cadddr x)
|
||||||
|
true-lst false-lst))
|
||||||
|
(else (and (tautologyp (caddr x)
|
||||||
|
(cons (cadr x)
|
||||||
|
true-lst)
|
||||||
|
false-lst)
|
||||||
|
(tautologyp (cadddr x)
|
||||||
|
true-lst
|
||||||
|
(cons (cadr x)
|
||||||
|
false-lst))))))
|
||||||
|
(else #f)))
|
||||||
|
|
||||||
|
(define if-constructor '*) ; becomes (symbol->symbol-record 'if)
|
||||||
|
|
||||||
|
(define rewrite-count 0) ; sanity check
|
||||||
|
|
||||||
|
; The next procedure is Henry Baker's sharing CONS, which avoids
|
||||||
|
; allocation if the result is already in hand.
|
||||||
|
; The REWRITE and REWRITE-ARGS procedures have been modified to
|
||||||
|
; use SCONS instead of CONS.
|
||||||
|
|
||||||
|
(define (scons x y original)
|
||||||
|
(if (and (eq? x (car original))
|
||||||
|
(eq? y (cdr original)))
|
||||||
|
original
|
||||||
|
(cons x y)))
|
||||||
|
|
||||||
|
(define (rewrite term)
|
||||||
|
(set! rewrite-count (+ rewrite-count 1))
|
||||||
|
(cond ((not (pair? term))
|
||||||
|
term)
|
||||||
|
(else (rewrite-with-lemmas (scons (car term)
|
||||||
|
(rewrite-args (cdr term))
|
||||||
|
term)
|
||||||
|
(get-lemmas (car term))))))
|
||||||
|
|
||||||
|
(define (rewrite-args lst)
|
||||||
|
(cond ((null? lst)
|
||||||
|
'())
|
||||||
|
(else (scons (rewrite (car lst))
|
||||||
|
(rewrite-args (cdr lst))
|
||||||
|
lst))))
|
||||||
|
|
||||||
|
(define (rewrite-with-lemmas term lst)
|
||||||
|
(cond ((null? lst)
|
||||||
|
term)
|
||||||
|
((one-way-unify term (cadr (car lst)))
|
||||||
|
(rewrite (apply-subst unify-subst (caddr (car lst)))))
|
||||||
|
(else (rewrite-with-lemmas term (cdr lst)))))
|
||||||
|
|
||||||
|
(define unify-subst '*)
|
||||||
|
|
||||||
|
(define (one-way-unify term1 term2)
|
||||||
|
(begin (set! unify-subst '())
|
||||||
|
(one-way-unify1 term1 term2)))
|
||||||
|
|
||||||
|
(define (one-way-unify1 term1 term2)
|
||||||
|
(cond ((not (pair? term2))
|
||||||
|
(let ((temp-temp (assq term2 unify-subst)))
|
||||||
|
(cond (temp-temp
|
||||||
|
(term-equal? term1 (cdr temp-temp)))
|
||||||
|
((number? term2) ; This bug fix makes
|
||||||
|
(equal? term1 term2)) ; nboyer 10-25% slower!
|
||||||
|
(else
|
||||||
|
(set! unify-subst (cons (cons term2 term1)
|
||||||
|
unify-subst))
|
||||||
|
#t))))
|
||||||
|
((not (pair? term1))
|
||||||
|
#f)
|
||||||
|
((eq? (car term1)
|
||||||
|
(car term2))
|
||||||
|
(one-way-unify1-lst (cdr term1)
|
||||||
|
(cdr term2)))
|
||||||
|
(else #f)))
|
||||||
|
|
||||||
|
(define (one-way-unify1-lst lst1 lst2)
|
||||||
|
(cond ((null? lst1)
|
||||||
|
(null? lst2))
|
||||||
|
((null? lst2)
|
||||||
|
#f)
|
||||||
|
((one-way-unify1 (car lst1)
|
||||||
|
(car lst2))
|
||||||
|
(one-way-unify1-lst (cdr lst1)
|
||||||
|
(cdr lst2)))
|
||||||
|
(else #f)))
|
||||||
|
|
||||||
|
(define (falsep x lst)
|
||||||
|
(or (term-equal? x false-term)
|
||||||
|
(term-member? x lst)))
|
||||||
|
|
||||||
|
(define (truep x lst)
|
||||||
|
(or (term-equal? x true-term)
|
||||||
|
(term-member? x lst)))
|
||||||
|
|
||||||
|
(define false-term '*) ; becomes (translate-term '(f))
|
||||||
|
(define true-term '*) ; becomes (translate-term '(t))
|
||||||
|
|
||||||
|
; The next two procedures were in the original benchmark
|
||||||
|
; but were never used.
|
||||||
|
|
||||||
|
(define (trans-of-implies n)
|
||||||
|
(translate-term
|
||||||
|
(list (quote implies)
|
||||||
|
(trans-of-implies1 n)
|
||||||
|
(list (quote implies)
|
||||||
|
0 n))))
|
||||||
|
|
||||||
|
(define (trans-of-implies1 n)
|
||||||
|
(cond ((equal? n 1)
|
||||||
|
(list (quote implies)
|
||||||
|
0 1))
|
||||||
|
(else (list (quote and)
|
||||||
|
(list (quote implies)
|
||||||
|
(- n 1)
|
||||||
|
n)
|
||||||
|
(trans-of-implies1 (- n 1))))))
|
||||||
|
|
||||||
|
; Translated terms can be circular structures, which can't be
|
||||||
|
; compared using Scheme's equal? and member procedures, so we
|
||||||
|
; use these instead.
|
||||||
|
|
||||||
|
(define (term-equal? x y)
|
||||||
|
(cond ((pair? x)
|
||||||
|
(and (pair? y)
|
||||||
|
(symbol-record-equal? (car x) (car y))
|
||||||
|
(term-args-equal? (cdr x) (cdr y))))
|
||||||
|
(else (equal? x y))))
|
||||||
|
|
||||||
|
(define (term-args-equal? lst1 lst2)
|
||||||
|
(cond ((null? lst1)
|
||||||
|
(null? lst2))
|
||||||
|
((null? lst2)
|
||||||
|
#f)
|
||||||
|
((term-equal? (car lst1) (car lst2))
|
||||||
|
(term-args-equal? (cdr lst1) (cdr lst2)))
|
||||||
|
(else #f)))
|
||||||
|
|
||||||
|
(define (term-member? x lst)
|
||||||
|
(cond ((null? lst)
|
||||||
|
#f)
|
||||||
|
((term-equal? x (car lst))
|
||||||
|
#t)
|
||||||
|
(else (term-member? x (cdr lst)))))
|
||||||
|
|
||||||
|
(set! setup-boyer
|
||||||
|
(lambda ()
|
||||||
|
(set! *symbol-records-alist* '())
|
||||||
|
(set! if-constructor (symbol->symbol-record 'if))
|
||||||
|
(set! false-term (translate-term '(f)))
|
||||||
|
(set! true-term (translate-term '(t)))
|
||||||
|
(setup)))
|
||||||
|
|
||||||
|
(set! test-boyer
|
||||||
|
(lambda (n)
|
||||||
|
(set! rewrite-count 0)
|
||||||
|
(let ((answer (test n)))
|
||||||
|
(write rewrite-count)
|
||||||
|
(display " rewrites")
|
||||||
|
(newline)
|
||||||
|
(if answer
|
||||||
|
rewrite-count
|
||||||
|
#f)))))
|
||||||
9319
gc-benchmarks/larceny/softscheme.sch
Normal file
9319
gc-benchmarks/larceny/softscheme.sch
Normal file
File diff suppressed because it is too large
Load diff
23798
gc-benchmarks/larceny/twobit-input-long.sch
Normal file
23798
gc-benchmarks/larceny/twobit-input-long.sch
Normal file
File diff suppressed because it is too large
Load diff
3623
gc-benchmarks/larceny/twobit-input-short.sch
Normal file
3623
gc-benchmarks/larceny/twobit-input-short.sch
Normal file
File diff suppressed because it is too large
Load diff
15408
gc-benchmarks/larceny/twobit-smaller.sch
Normal file
15408
gc-benchmarks/larceny/twobit-smaller.sch
Normal file
File diff suppressed because it is too large
Load diff
23798
gc-benchmarks/larceny/twobit.sch
Normal file
23798
gc-benchmarks/larceny/twobit.sch
Normal file
File diff suppressed because it is too large
Load diff
Loading…
Add table
Add a link
Reference in a new issue