Compare commits
130 Commits
parse/leve
...
dev
Author | SHA1 | Date |
---|---|---|
Leni Aniva | 9075ded885 | |
Leni Aniva | 27e4e45418 | |
Leni Aniva | b645d79fda | |
Leni Aniva | e36954a589 | |
Leni Aniva | 414f1c70fd | |
Leni Aniva | 25bb964604 | |
Leni Aniva | 7c49fcff27 | |
Leni Aniva | f11c5ebaa3 | |
Leni Aniva | e4d53733d0 | |
Leni Aniva | 68dac4c951 | |
Leni Aniva | 4042ec707e | |
Leni Aniva | 8394e1b468 | |
Leni Aniva | 9b3eef35ec | |
Leni Aniva | a7b30af36b | |
Leni Aniva | e2ad6ce6b3 | |
Leni Aniva | 37473b3efb | |
Leni Aniva | 82d99ccf9b | |
Leni Aniva | 02556f3c79 | |
Leni Aniva | 9c40a83956 | |
Leni Aniva | f8df2599f9 | |
Leni Aniva | 8d2cd6dfc7 | |
Leni Aniva | 948b535b5d | |
Leni Aniva | edec0f5733 | |
Leni Aniva | 0c529c5cd9 | |
Leni Aniva | 76765c913c | |
Leni Aniva | 3733c10a4e | |
Leni Aniva | 5d43068ec3 | |
Leni Aniva | f87eed817f | |
Leni Aniva | 43e11f1ba3 | |
Leni Aniva | 0c469027c6 | |
Leni Aniva | e1b7eaab12 | |
Leni Aniva | d17b21e282 | |
Leni Aniva | 5b4f8a37eb | |
Leni Aniva | 1e7a186bb1 | |
Leni Aniva | 9b0456a5e0 | |
Leni Aniva | 7968072097 | |
Leni Aniva | e07f9d9b3f | |
Leni Aniva | 56100a30af | |
Leni Aniva | e943a4b065 | |
Leni Aniva | 0bc7bc5856 | |
Leni Aniva | caac70f0cf | |
Leni Aniva | 64269868d5 | |
Leni Aniva | c9ee31bbfd | |
Leni Aniva | 394fb73137 | |
Leni Aniva | c0e2a592ea | |
Leni Aniva | 2c08ef1e23 | |
Leni Aniva | 651afa75f4 | |
Leni Aniva | abef7a6f0d | |
Leni Aniva | caa463f410 | |
Leni Aniva | 3ca52517ab | |
Leni Aniva | 1c9a411d4d | |
Leni Aniva | 7b5567d784 | |
Leni Aniva | 29f437f859 | |
Leni Aniva | 4c81f226d1 | |
Leni Aniva | 9db5463499 | |
Leni Aniva | bf941cd686 | |
Leni Aniva | 2682ce5b7b | |
Leni Aniva | 3b415e8dc1 | |
Leni Aniva | 431ca4e481 | |
Leni Aniva | eb5ee8c57c | |
Leni Aniva | 94c7b021f7 | |
Leni Aniva | 193d94e798 | |
Leni Aniva | a7fe7cbd7c | |
Leni Aniva | df8b6602ee | |
Leni Aniva | 9b1dd0ffda | |
Leni Aniva | 4549ae1f65 | |
Leni Aniva | c404564a2b | |
Leni Aniva | 6ddde2963d | |
Leni Aniva | fc0d872343 | |
Leni Aniva | 2d2ff24017 | |
Leni Aniva | 7acf1ffdf1 | |
Leni Aniva | 58f9d72288 | |
Leni Aniva | c0124b347f | |
Leni Aniva | 8e78718447 | |
Leni Aniva | ffbea41f62 | |
Leni Aniva | e282d9f781 | |
Leni Aniva | 25a7025c25 | |
Leni Aniva | 472cd54868 | |
Leni Aniva | fbe6e8fcb3 | |
Leni Aniva | 361e2e8926 | |
Leni Aniva | aceee85b05 | |
Leni Aniva | 8707dbc9bb | |
Leni Aniva | f80d90ce87 | |
Leni Aniva | b3a60fcea8 | |
Leni Aniva | bd20bf76da | |
Leni Aniva | 2d2cf75183 | |
Leni Aniva | c0e6e3ec39 | |
Leni Aniva | 3a53493089 | |
Leni Aniva | 6dcff8b151 | |
Leni Aniva | 3c90c94645 | |
Leni Aniva | 67e7f22b0a | |
Leni Aniva | a2c5c7448c | |
Leni Aniva | 855e771609 | |
Leni Aniva | b9b16ba0e9 | |
Leni Aniva | 09628309a9 | |
Leni Aniva | bd42c396d7 | |
Leni Aniva | bbc00cbbb8 | |
Leni Aniva | 75df7268c5 | |
Leni Aniva | 92acf7782c | |
Leni Aniva | cf1c884c8c | |
Leni Aniva | cc74d41b15 | |
Leni Aniva | 2f951c8fef | |
Leni Aniva | 6ad24b72d4 | |
Leni Aniva | cf17428001 | |
Leni Aniva | 5c7bb288b2 | |
Leni Aniva | bc09f4a29d | |
Leni Aniva | f813d4a8dd | |
Leni Aniva | c04b363de7 | |
Leni Aniva | 03ecb6cf19 | |
Leni Aniva | 0b88f6708e | |
Leni Aniva | e58dbc66a9 | |
Leni Aniva | 66a5dfcf3c | |
Leni Aniva | 69ec70ffbe | |
Leni Aniva | aa106f7591 | |
Leni Aniva | 679871cbc6 | |
Leni Aniva | 2937675044 | |
Leni Aniva | cf1289f159 | |
Leni Aniva | 1e1995255a | |
Leni Aniva | 63417ef179 | |
Leni Aniva | 4cff6677d2 | |
Leni Aniva | 6ffb227cd6 | |
Leni Aniva | feff62a3c5 | |
Leni Aniva | 3812aa56ec | |
Leni Aniva | 4a92e655f6 | |
Leni Aniva | 398b1c39ed | |
Leni Aniva | fec13ddb51 | |
Leni Aniva | 7aa7e6d7e9 | |
Leni Aniva | dbd54f7679 | |
Leni Aniva | 75b4648ba9 | |
Leni Aniva | b954f12526 |
|
@ -0,0 +1,674 @@
|
|||
GNU GENERAL PUBLIC LICENSE
|
||||
Version 3, 29 June 2007
|
||||
|
||||
Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/>
|
||||
Everyone is permitted to copy and distribute verbatim copies
|
||||
of this license document, but changing it is not allowed.
|
||||
|
||||
Preamble
|
||||
|
||||
The GNU General Public License is a free, copyleft license for
|
||||
software and other kinds of works.
|
||||
|
||||
The licenses for most software and other practical works are designed
|
||||
to take away your freedom to share and change the works. By contrast,
|
||||
the GNU General Public License is intended to guarantee your freedom to
|
||||
share and change all versions of a program--to make sure it remains free
|
||||
software for all its users. We, the Free Software Foundation, use the
|
||||
GNU General Public License for most of our software; it applies also to
|
||||
any other work released this way by its authors. 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
|
||||
them 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 prevent others from denying you
|
||||
these rights or asking you to surrender the rights. Therefore, you have
|
||||
certain responsibilities if you distribute copies of the software, or if
|
||||
you modify it: responsibilities to respect the freedom of others.
|
||||
|
||||
For example, if you distribute copies of such a program, whether
|
||||
gratis or for a fee, you must pass on to the recipients the same
|
||||
freedoms that you received. 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.
|
||||
|
||||
Developers that use the GNU GPL protect your rights with two steps:
|
||||
(1) assert copyright on the software, and (2) offer you this License
|
||||
giving you legal permission to copy, distribute and/or modify it.
|
||||
|
||||
For the developers' and authors' protection, the GPL clearly explains
|
||||
that there is no warranty for this free software. For both users' and
|
||||
authors' sake, the GPL requires that modified versions be marked as
|
||||
changed, so that their problems will not be attributed erroneously to
|
||||
authors of previous versions.
|
||||
|
||||
Some devices are designed to deny users access to install or run
|
||||
modified versions of the software inside them, although the manufacturer
|
||||
can do so. This is fundamentally incompatible with the aim of
|
||||
protecting users' freedom to change the software. The systematic
|
||||
pattern of such abuse occurs in the area of products for individuals to
|
||||
use, which is precisely where it is most unacceptable. Therefore, we
|
||||
have designed this version of the GPL to prohibit the practice for those
|
||||
products. If such problems arise substantially in other domains, we
|
||||
stand ready to extend this provision to those domains in future versions
|
||||
of the GPL, as needed to protect the freedom of users.
|
||||
|
||||
Finally, every program is threatened constantly by software patents.
|
||||
States should not allow patents to restrict development and use of
|
||||
software on general-purpose computers, but in those that do, we wish to
|
||||
avoid the special danger that patents applied to a free program could
|
||||
make it effectively proprietary. To prevent this, the GPL assures that
|
||||
patents cannot be used to render the program non-free.
|
||||
|
||||
The precise terms and conditions for copying, distribution and
|
||||
modification follow.
|
||||
|
||||
TERMS AND CONDITIONS
|
||||
|
||||
0. Definitions.
|
||||
|
||||
"This License" refers to version 3 of the GNU General Public License.
|
||||
|
||||
"Copyright" also means copyright-like laws that apply to other kinds of
|
||||
works, such as semiconductor masks.
|
||||
|
||||
"The Program" refers to any copyrightable work licensed under this
|
||||
License. Each licensee is addressed as "you". "Licensees" and
|
||||
"recipients" may be individuals or organizations.
|
||||
|
||||
To "modify" a work means to copy from or adapt all or part of the work
|
||||
in a fashion requiring copyright permission, other than the making of an
|
||||
exact copy. The resulting work is called a "modified version" of the
|
||||
earlier work or a work "based on" the earlier work.
|
||||
|
||||
A "covered work" means either the unmodified Program or a work based
|
||||
on the Program.
|
||||
|
||||
To "propagate" a work means to do anything with it that, without
|
||||
permission, would make you directly or secondarily liable for
|
||||
infringement under applicable copyright law, except executing it on a
|
||||
computer or modifying a private copy. Propagation includes copying,
|
||||
distribution (with or without modification), making available to the
|
||||
public, and in some countries other activities as well.
|
||||
|
||||
To "convey" a work means any kind of propagation that enables other
|
||||
parties to make or receive copies. Mere interaction with a user through
|
||||
a computer network, with no transfer of a copy, is not conveying.
|
||||
|
||||
An interactive user interface displays "Appropriate Legal Notices"
|
||||
to the extent that it includes a convenient and prominently visible
|
||||
feature that (1) displays an appropriate copyright notice, and (2)
|
||||
tells the user that there is no warranty for the work (except to the
|
||||
extent that warranties are provided), that licensees may convey the
|
||||
work under this License, and how to view a copy of this License. If
|
||||
the interface presents a list of user commands or options, such as a
|
||||
menu, a prominent item in the list meets this criterion.
|
||||
|
||||
1. Source Code.
|
||||
|
||||
The "source code" for a work means the preferred form of the work
|
||||
for making modifications to it. "Object code" means any non-source
|
||||
form of a work.
|
||||
|
||||
A "Standard Interface" means an interface that either is an official
|
||||
standard defined by a recognized standards body, or, in the case of
|
||||
interfaces specified for a particular programming language, one that
|
||||
is widely used among developers working in that language.
|
||||
|
||||
The "System Libraries" of an executable work include anything, other
|
||||
than the work as a whole, that (a) is included in the normal form of
|
||||
packaging a Major Component, but which is not part of that Major
|
||||
Component, and (b) serves only to enable use of the work with that
|
||||
Major Component, or to implement a Standard Interface for which an
|
||||
implementation is available to the public in source code form. A
|
||||
"Major Component", in this context, means a major essential component
|
||||
(kernel, window system, and so on) of the specific operating system
|
||||
(if any) on which the executable work runs, or a compiler used to
|
||||
produce the work, or an object code interpreter used to run it.
|
||||
|
||||
The "Corresponding Source" for a work in object code form means all
|
||||
the source code needed to generate, install, and (for an executable
|
||||
work) run the object code and to modify the work, including scripts to
|
||||
control those activities. However, it does not include the work's
|
||||
System Libraries, or general-purpose tools or generally available free
|
||||
programs which are used unmodified in performing those activities but
|
||||
which are not part of the work. For example, Corresponding Source
|
||||
includes interface definition files associated with source files for
|
||||
the work, and the source code for shared libraries and dynamically
|
||||
linked subprograms that the work is specifically designed to require,
|
||||
such as by intimate data communication or control flow between those
|
||||
subprograms and other parts of the work.
|
||||
|
||||
The Corresponding Source need not include anything that users
|
||||
can regenerate automatically from other parts of the Corresponding
|
||||
Source.
|
||||
|
||||
The Corresponding Source for a work in source code form is that
|
||||
same work.
|
||||
|
||||
2. Basic Permissions.
|
||||
|
||||
All rights granted under this License are granted for the term of
|
||||
copyright on the Program, and are irrevocable provided the stated
|
||||
conditions are met. This License explicitly affirms your unlimited
|
||||
permission to run the unmodified Program. The output from running a
|
||||
covered work is covered by this License only if the output, given its
|
||||
content, constitutes a covered work. This License acknowledges your
|
||||
rights of fair use or other equivalent, as provided by copyright law.
|
||||
|
||||
You may make, run and propagate covered works that you do not
|
||||
convey, without conditions so long as your license otherwise remains
|
||||
in force. You may convey covered works to others for the sole purpose
|
||||
of having them make modifications exclusively for you, or provide you
|
||||
with facilities for running those works, provided that you comply with
|
||||
the terms of this License in conveying all material for which you do
|
||||
not control copyright. Those thus making or running the covered works
|
||||
for you must do so exclusively on your behalf, under your direction
|
||||
and control, on terms that prohibit them from making any copies of
|
||||
your copyrighted material outside their relationship with you.
|
||||
|
||||
Conveying under any other circumstances is permitted solely under
|
||||
the conditions stated below. Sublicensing is not allowed; section 10
|
||||
makes it unnecessary.
|
||||
|
||||
3. Protecting Users' Legal Rights From Anti-Circumvention Law.
|
||||
|
||||
No covered work shall be deemed part of an effective technological
|
||||
measure under any applicable law fulfilling obligations under article
|
||||
11 of the WIPO copyright treaty adopted on 20 December 1996, or
|
||||
similar laws prohibiting or restricting circumvention of such
|
||||
measures.
|
||||
|
||||
When you convey a covered work, you waive any legal power to forbid
|
||||
circumvention of technological measures to the extent such circumvention
|
||||
is effected by exercising rights under this License with respect to
|
||||
the covered work, and you disclaim any intention to limit operation or
|
||||
modification of the work as a means of enforcing, against the work's
|
||||
users, your or third parties' legal rights to forbid circumvention of
|
||||
technological measures.
|
||||
|
||||
4. Conveying Verbatim Copies.
|
||||
|
||||
You may convey 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;
|
||||
keep intact all notices stating that this License and any
|
||||
non-permissive terms added in accord with section 7 apply to the code;
|
||||
keep intact all notices of the absence of any warranty; and give all
|
||||
recipients a copy of this License along with the Program.
|
||||
|
||||
You may charge any price or no price for each copy that you convey,
|
||||
and you may offer support or warranty protection for a fee.
|
||||
|
||||
5. Conveying Modified Source Versions.
|
||||
|
||||
You may convey a work based on the Program, or the modifications to
|
||||
produce it from the Program, in the form of source code under the
|
||||
terms of section 4, provided that you also meet all of these conditions:
|
||||
|
||||
a) The work must carry prominent notices stating that you modified
|
||||
it, and giving a relevant date.
|
||||
|
||||
b) The work must carry prominent notices stating that it is
|
||||
released under this License and any conditions added under section
|
||||
7. This requirement modifies the requirement in section 4 to
|
||||
"keep intact all notices".
|
||||
|
||||
c) You must license the entire work, as a whole, under this
|
||||
License to anyone who comes into possession of a copy. This
|
||||
License will therefore apply, along with any applicable section 7
|
||||
additional terms, to the whole of the work, and all its parts,
|
||||
regardless of how they are packaged. This License gives no
|
||||
permission to license the work in any other way, but it does not
|
||||
invalidate such permission if you have separately received it.
|
||||
|
||||
d) If the work has interactive user interfaces, each must display
|
||||
Appropriate Legal Notices; however, if the Program has interactive
|
||||
interfaces that do not display Appropriate Legal Notices, your
|
||||
work need not make them do so.
|
||||
|
||||
A compilation of a covered work with other separate and independent
|
||||
works, which are not by their nature extensions of the covered work,
|
||||
and which are not combined with it such as to form a larger program,
|
||||
in or on a volume of a storage or distribution medium, is called an
|
||||
"aggregate" if the compilation and its resulting copyright are not
|
||||
used to limit the access or legal rights of the compilation's users
|
||||
beyond what the individual works permit. Inclusion of a covered work
|
||||
in an aggregate does not cause this License to apply to the other
|
||||
parts of the aggregate.
|
||||
|
||||
6. Conveying Non-Source Forms.
|
||||
|
||||
You may convey a covered work in object code form under the terms
|
||||
of sections 4 and 5, provided that you also convey the
|
||||
machine-readable Corresponding Source under the terms of this License,
|
||||
in one of these ways:
|
||||
|
||||
a) Convey the object code in, or embodied in, a physical product
|
||||
(including a physical distribution medium), accompanied by the
|
||||
Corresponding Source fixed on a durable physical medium
|
||||
customarily used for software interchange.
|
||||
|
||||
b) Convey the object code in, or embodied in, a physical product
|
||||
(including a physical distribution medium), accompanied by a
|
||||
written offer, valid for at least three years and valid for as
|
||||
long as you offer spare parts or customer support for that product
|
||||
model, to give anyone who possesses the object code either (1) a
|
||||
copy of the Corresponding Source for all the software in the
|
||||
product that is covered by this License, on a durable physical
|
||||
medium customarily used for software interchange, for a price no
|
||||
more than your reasonable cost of physically performing this
|
||||
conveying of source, or (2) access to copy the
|
||||
Corresponding Source from a network server at no charge.
|
||||
|
||||
c) Convey individual copies of the object code with a copy of the
|
||||
written offer to provide the Corresponding Source. This
|
||||
alternative is allowed only occasionally and noncommercially, and
|
||||
only if you received the object code with such an offer, in accord
|
||||
with subsection 6b.
|
||||
|
||||
d) Convey the object code by offering access from a designated
|
||||
place (gratis or for a charge), and offer equivalent access to the
|
||||
Corresponding Source in the same way through the same place at no
|
||||
further charge. You need not require recipients to copy the
|
||||
Corresponding Source along with the object code. If the place to
|
||||
copy the object code is a network server, the Corresponding Source
|
||||
may be on a different server (operated by you or a third party)
|
||||
that supports equivalent copying facilities, provided you maintain
|
||||
clear directions next to the object code saying where to find the
|
||||
Corresponding Source. Regardless of what server hosts the
|
||||
Corresponding Source, you remain obligated to ensure that it is
|
||||
available for as long as needed to satisfy these requirements.
|
||||
|
||||
e) Convey the object code using peer-to-peer transmission, provided
|
||||
you inform other peers where the object code and Corresponding
|
||||
Source of the work are being offered to the general public at no
|
||||
charge under subsection 6d.
|
||||
|
||||
A separable portion of the object code, whose source code is excluded
|
||||
from the Corresponding Source as a System Library, need not be
|
||||
included in conveying the object code work.
|
||||
|
||||
A "User Product" is either (1) a "consumer product", which means any
|
||||
tangible personal property which is normally used for personal, family,
|
||||
or household purposes, or (2) anything designed or sold for incorporation
|
||||
into a dwelling. In determining whether a product is a consumer product,
|
||||
doubtful cases shall be resolved in favor of coverage. For a particular
|
||||
product received by a particular user, "normally used" refers to a
|
||||
typical or common use of that class of product, regardless of the status
|
||||
of the particular user or of the way in which the particular user
|
||||
actually uses, or expects or is expected to use, the product. A product
|
||||
is a consumer product regardless of whether the product has substantial
|
||||
commercial, industrial or non-consumer uses, unless such uses represent
|
||||
the only significant mode of use of the product.
|
||||
|
||||
"Installation Information" for a User Product means any methods,
|
||||
procedures, authorization keys, or other information required to install
|
||||
and execute modified versions of a covered work in that User Product from
|
||||
a modified version of its Corresponding Source. The information must
|
||||
suffice to ensure that the continued functioning of the modified object
|
||||
code is in no case prevented or interfered with solely because
|
||||
modification has been made.
|
||||
|
||||
If you convey an object code work under this section in, or with, or
|
||||
specifically for use in, a User Product, and the conveying occurs as
|
||||
part of a transaction in which the right of possession and use of the
|
||||
User Product is transferred to the recipient in perpetuity or for a
|
||||
fixed term (regardless of how the transaction is characterized), the
|
||||
Corresponding Source conveyed under this section must be accompanied
|
||||
by the Installation Information. But this requirement does not apply
|
||||
if neither you nor any third party retains the ability to install
|
||||
modified object code on the User Product (for example, the work has
|
||||
been installed in ROM).
|
||||
|
||||
The requirement to provide Installation Information does not include a
|
||||
requirement to continue to provide support service, warranty, or updates
|
||||
for a work that has been modified or installed by the recipient, or for
|
||||
the User Product in which it has been modified or installed. Access to a
|
||||
network may be denied when the modification itself materially and
|
||||
adversely affects the operation of the network or violates the rules and
|
||||
protocols for communication across the network.
|
||||
|
||||
Corresponding Source conveyed, and Installation Information provided,
|
||||
in accord with this section must be in a format that is publicly
|
||||
documented (and with an implementation available to the public in
|
||||
source code form), and must require no special password or key for
|
||||
unpacking, reading or copying.
|
||||
|
||||
7. Additional Terms.
|
||||
|
||||
"Additional permissions" are terms that supplement the terms of this
|
||||
License by making exceptions from one or more of its conditions.
|
||||
Additional permissions that are applicable to the entire Program shall
|
||||
be treated as though they were included in this License, to the extent
|
||||
that they are valid under applicable law. If additional permissions
|
||||
apply only to part of the Program, that part may be used separately
|
||||
under those permissions, but the entire Program remains governed by
|
||||
this License without regard to the additional permissions.
|
||||
|
||||
When you convey a copy of a covered work, you may at your option
|
||||
remove any additional permissions from that copy, or from any part of
|
||||
it. (Additional permissions may be written to require their own
|
||||
removal in certain cases when you modify the work.) You may place
|
||||
additional permissions on material, added by you to a covered work,
|
||||
for which you have or can give appropriate copyright permission.
|
||||
|
||||
Notwithstanding any other provision of this License, for material you
|
||||
add to a covered work, you may (if authorized by the copyright holders of
|
||||
that material) supplement the terms of this License with terms:
|
||||
|
||||
a) Disclaiming warranty or limiting liability differently from the
|
||||
terms of sections 15 and 16 of this License; or
|
||||
|
||||
b) Requiring preservation of specified reasonable legal notices or
|
||||
author attributions in that material or in the Appropriate Legal
|
||||
Notices displayed by works containing it; or
|
||||
|
||||
c) Prohibiting misrepresentation of the origin of that material, or
|
||||
requiring that modified versions of such material be marked in
|
||||
reasonable ways as different from the original version; or
|
||||
|
||||
d) Limiting the use for publicity purposes of names of licensors or
|
||||
authors of the material; or
|
||||
|
||||
e) Declining to grant rights under trademark law for use of some
|
||||
trade names, trademarks, or service marks; or
|
||||
|
||||
f) Requiring indemnification of licensors and authors of that
|
||||
material by anyone who conveys the material (or modified versions of
|
||||
it) with contractual assumptions of liability to the recipient, for
|
||||
any liability that these contractual assumptions directly impose on
|
||||
those licensors and authors.
|
||||
|
||||
All other non-permissive additional terms are considered "further
|
||||
restrictions" within the meaning of section 10. If the Program as you
|
||||
received it, or any part of it, contains a notice stating that it is
|
||||
governed by this License along with a term that is a further
|
||||
restriction, you may remove that term. If a license document contains
|
||||
a further restriction but permits relicensing or conveying under this
|
||||
License, you may add to a covered work material governed by the terms
|
||||
of that license document, provided that the further restriction does
|
||||
not survive such relicensing or conveying.
|
||||
|
||||
If you add terms to a covered work in accord with this section, you
|
||||
must place, in the relevant source files, a statement of the
|
||||
additional terms that apply to those files, or a notice indicating
|
||||
where to find the applicable terms.
|
||||
|
||||
Additional terms, permissive or non-permissive, may be stated in the
|
||||
form of a separately written license, or stated as exceptions;
|
||||
the above requirements apply either way.
|
||||
|
||||
8. Termination.
|
||||
|
||||
You may not propagate or modify a covered work except as expressly
|
||||
provided under this License. Any attempt otherwise to propagate or
|
||||
modify it is void, and will automatically terminate your rights under
|
||||
this License (including any patent licenses granted under the third
|
||||
paragraph of section 11).
|
||||
|
||||
However, if you cease all violation of this License, then your
|
||||
license from a particular copyright holder is reinstated (a)
|
||||
provisionally, unless and until the copyright holder explicitly and
|
||||
finally terminates your license, and (b) permanently, if the copyright
|
||||
holder fails to notify you of the violation by some reasonable means
|
||||
prior to 60 days after the cessation.
|
||||
|
||||
Moreover, your license from a particular copyright holder is
|
||||
reinstated permanently if the copyright holder notifies you of the
|
||||
violation by some reasonable means, this is the first time you have
|
||||
received notice of violation of this License (for any work) from that
|
||||
copyright holder, and you cure the violation prior to 30 days after
|
||||
your receipt of the notice.
|
||||
|
||||
Termination of your rights under this section does not terminate the
|
||||
licenses of parties who have received copies or rights from you under
|
||||
this License. If your rights have been terminated and not permanently
|
||||
reinstated, you do not qualify to receive new licenses for the same
|
||||
material under section 10.
|
||||
|
||||
9. Acceptance Not Required for Having Copies.
|
||||
|
||||
You are not required to accept this License in order to receive or
|
||||
run a copy of the Program. Ancillary propagation of a covered work
|
||||
occurring solely as a consequence of using peer-to-peer transmission
|
||||
to receive a copy likewise does not require acceptance. However,
|
||||
nothing other than this License grants you permission to propagate or
|
||||
modify any covered work. These actions infringe copyright if you do
|
||||
not accept this License. Therefore, by modifying or propagating a
|
||||
covered work, you indicate your acceptance of this License to do so.
|
||||
|
||||
10. Automatic Licensing of Downstream Recipients.
|
||||
|
||||
Each time you convey a covered work, the recipient automatically
|
||||
receives a license from the original licensors, to run, modify and
|
||||
propagate that work, subject to this License. You are not responsible
|
||||
for enforcing compliance by third parties with this License.
|
||||
|
||||
An "entity transaction" is a transaction transferring control of an
|
||||
organization, or substantially all assets of one, or subdividing an
|
||||
organization, or merging organizations. If propagation of a covered
|
||||
work results from an entity transaction, each party to that
|
||||
transaction who receives a copy of the work also receives whatever
|
||||
licenses to the work the party's predecessor in interest had or could
|
||||
give under the previous paragraph, plus a right to possession of the
|
||||
Corresponding Source of the work from the predecessor in interest, if
|
||||
the predecessor has it or can get it with reasonable efforts.
|
||||
|
||||
You may not impose any further restrictions on the exercise of the
|
||||
rights granted or affirmed under this License. For example, you may
|
||||
not impose a license fee, royalty, or other charge for exercise of
|
||||
rights granted under this License, and you may not initiate litigation
|
||||
(including a cross-claim or counterclaim in a lawsuit) alleging that
|
||||
any patent claim is infringed by making, using, selling, offering for
|
||||
sale, or importing the Program or any portion of it.
|
||||
|
||||
11. Patents.
|
||||
|
||||
A "contributor" is a copyright holder who authorizes use under this
|
||||
License of the Program or a work on which the Program is based. The
|
||||
work thus licensed is called the contributor's "contributor version".
|
||||
|
||||
A contributor's "essential patent claims" are all patent claims
|
||||
owned or controlled by the contributor, whether already acquired or
|
||||
hereafter acquired, that would be infringed by some manner, permitted
|
||||
by this License, of making, using, or selling its contributor version,
|
||||
but do not include claims that would be infringed only as a
|
||||
consequence of further modification of the contributor version. For
|
||||
purposes of this definition, "control" includes the right to grant
|
||||
patent sublicenses in a manner consistent with the requirements of
|
||||
this License.
|
||||
|
||||
Each contributor grants you a non-exclusive, worldwide, royalty-free
|
||||
patent license under the contributor's essential patent claims, to
|
||||
make, use, sell, offer for sale, import and otherwise run, modify and
|
||||
propagate the contents of its contributor version.
|
||||
|
||||
In the following three paragraphs, a "patent license" is any express
|
||||
agreement or commitment, however denominated, not to enforce a patent
|
||||
(such as an express permission to practice a patent or covenant not to
|
||||
sue for patent infringement). To "grant" such a patent license to a
|
||||
party means to make such an agreement or commitment not to enforce a
|
||||
patent against the party.
|
||||
|
||||
If you convey a covered work, knowingly relying on a patent license,
|
||||
and the Corresponding Source of the work is not available for anyone
|
||||
to copy, free of charge and under the terms of this License, through a
|
||||
publicly available network server or other readily accessible means,
|
||||
then you must either (1) cause the Corresponding Source to be so
|
||||
available, or (2) arrange to deprive yourself of the benefit of the
|
||||
patent license for this particular work, or (3) arrange, in a manner
|
||||
consistent with the requirements of this License, to extend the patent
|
||||
license to downstream recipients. "Knowingly relying" means you have
|
||||
actual knowledge that, but for the patent license, your conveying the
|
||||
covered work in a country, or your recipient's use of the covered work
|
||||
in a country, would infringe one or more identifiable patents in that
|
||||
country that you have reason to believe are valid.
|
||||
|
||||
If, pursuant to or in connection with a single transaction or
|
||||
arrangement, you convey, or propagate by procuring conveyance of, a
|
||||
covered work, and grant a patent license to some of the parties
|
||||
receiving the covered work authorizing them to use, propagate, modify
|
||||
or convey a specific copy of the covered work, then the patent license
|
||||
you grant is automatically extended to all recipients of the covered
|
||||
work and works based on it.
|
||||
|
||||
A patent license is "discriminatory" if it does not include within
|
||||
the scope of its coverage, prohibits the exercise of, or is
|
||||
conditioned on the non-exercise of one or more of the rights that are
|
||||
specifically granted under this License. You may not convey a covered
|
||||
work if you are a party to an arrangement with a third party that is
|
||||
in the business of distributing software, under which you make payment
|
||||
to the third party based on the extent of your activity of conveying
|
||||
the work, and under which the third party grants, to any of the
|
||||
parties who would receive the covered work from you, a discriminatory
|
||||
patent license (a) in connection with copies of the covered work
|
||||
conveyed by you (or copies made from those copies), or (b) primarily
|
||||
for and in connection with specific products or compilations that
|
||||
contain the covered work, unless you entered into that arrangement,
|
||||
or that patent license was granted, prior to 28 March 2007.
|
||||
|
||||
Nothing in this License shall be construed as excluding or limiting
|
||||
any implied license or other defenses to infringement that may
|
||||
otherwise be available to you under applicable patent law.
|
||||
|
||||
12. No Surrender of Others' Freedom.
|
||||
|
||||
If 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 convey a
|
||||
covered work so as to satisfy simultaneously your obligations under this
|
||||
License and any other pertinent obligations, then as a consequence you may
|
||||
not convey it at all. For example, if you agree to terms that obligate you
|
||||
to collect a royalty for further conveying from those to whom you convey
|
||||
the Program, the only way you could satisfy both those terms and this
|
||||
License would be to refrain entirely from conveying the Program.
|
||||
|
||||
13. Use with the GNU Affero General Public License.
|
||||
|
||||
Notwithstanding any other provision of this License, you have
|
||||
permission to link or combine any covered work with a work licensed
|
||||
under version 3 of the GNU Affero General Public License into a single
|
||||
combined work, and to convey the resulting work. The terms of this
|
||||
License will continue to apply to the part which is the covered work,
|
||||
but the special requirements of the GNU Affero General Public License,
|
||||
section 13, concerning interaction through a network will apply to the
|
||||
combination as such.
|
||||
|
||||
14. Revised Versions of this License.
|
||||
|
||||
The Free Software Foundation may publish revised and/or new versions of
|
||||
the GNU 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 that a certain numbered version of the GNU General
|
||||
Public License "or any later version" applies to it, you have the
|
||||
option of following the terms and conditions either of that numbered
|
||||
version or of any later version published by the Free Software
|
||||
Foundation. If the Program does not specify a version number of the
|
||||
GNU General Public License, you may choose any version ever published
|
||||
by the Free Software Foundation.
|
||||
|
||||
If the Program specifies that a proxy can decide which future
|
||||
versions of the GNU General Public License can be used, that proxy's
|
||||
public statement of acceptance of a version permanently authorizes you
|
||||
to choose that version for the Program.
|
||||
|
||||
Later license versions may give you additional or different
|
||||
permissions. However, no additional obligations are imposed on any
|
||||
author or copyright holder as a result of your choosing to follow a
|
||||
later version.
|
||||
|
||||
15. Disclaimer of Warranty.
|
||||
|
||||
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.
|
||||
|
||||
16. Limitation of Liability.
|
||||
|
||||
IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
|
||||
WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS
|
||||
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.
|
||||
|
||||
17. Interpretation of Sections 15 and 16.
|
||||
|
||||
If the disclaimer of warranty and limitation of liability provided
|
||||
above cannot be given local legal effect according to their terms,
|
||||
reviewing courts shall apply local law that most closely approximates
|
||||
an absolute waiver of all civil liability in connection with the
|
||||
Program, unless a warranty or assumption of liability accompanies a
|
||||
copy of the Program in return for a fee.
|
||||
|
||||
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
|
||||
state 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 3 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, see <https://www.gnu.org/licenses/>.
|
||||
|
||||
Also add information on how to contact you by electronic and paper mail.
|
||||
|
||||
If the program does terminal interaction, make it output a short
|
||||
notice like this when it starts in an interactive mode:
|
||||
|
||||
<program> Copyright (C) <year> <name of author>
|
||||
This program 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, your program's commands
|
||||
might be different; for a GUI interface, you would use an "about box".
|
||||
|
||||
You should also get your employer (if you work as a programmer) or school,
|
||||
if any, to sign a "copyright disclaimer" for the program, if necessary.
|
||||
For more information on this, and how to apply and follow the GNU GPL, see
|
||||
<https://www.gnu.org/licenses/>.
|
||||
|
||||
The GNU 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 Lesser General
|
||||
Public License instead of this License. But first, please read
|
||||
<https://www.gnu.org/licenses/why-not-lgpl.html>.
|
|
@ -4,6 +4,7 @@ import Lean.Environment
|
|||
import Pantograph.Version
|
||||
import Pantograph.Library
|
||||
import Pantograph
|
||||
import Repl
|
||||
|
||||
-- Main IO functions
|
||||
open Pantograph
|
||||
|
|
20
Makefile
20
Makefile
|
@ -1,20 +0,0 @@
|
|||
LIB := ./.lake/build/lib/Pantograph.olean
|
||||
EXE := ./.lake/build/bin/pantograph
|
||||
SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain
|
||||
|
||||
TEST_EXE := ./.lake/build/bin/test
|
||||
TEST_SOURCE := $(wildcard Test/*.lean)
|
||||
|
||||
$(LIB) $(EXE): $(SOURCE)
|
||||
lake build pantograph
|
||||
|
||||
$(TEST_EXE): $(LIB) $(TEST_SOURCE)
|
||||
lake build test
|
||||
|
||||
test: $(TEST_EXE)
|
||||
$(TEST_EXE)
|
||||
|
||||
clean:
|
||||
lake clean
|
||||
|
||||
.PHONY: test clean
|
196
Pantograph.lean
196
Pantograph.lean
|
@ -1,194 +1,8 @@
|
|||
import Pantograph.Compile
|
||||
import Pantograph.Condensed
|
||||
import Pantograph.Environment
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Library
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Serial
|
||||
import Pantograph.Environment
|
||||
import Pantograph.Library
|
||||
import Lean.Data.HashMap
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
structure Context where
|
||||
imports: List String
|
||||
|
||||
/-- Stores state of the REPL -/
|
||||
structure State where
|
||||
options: Protocol.Options := {}
|
||||
nextId: Nat := 0
|
||||
goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
|
||||
|
||||
/-- Main state monad for executing commands -/
|
||||
abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
|
||||
-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
|
||||
-- certain monadic features in `MainM`
|
||||
abbrev CR α := Except Protocol.InteractionError α
|
||||
|
||||
def execute (command: Protocol.Command): MainM Lean.Json := do
|
||||
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
|
||||
match Lean.fromJson? command.payload with
|
||||
| .ok args => do
|
||||
match (← comm args) with
|
||||
| .ok result => return Lean.toJson result
|
||||
| .error ierror => return Lean.toJson ierror
|
||||
| .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
|
||||
match command.cmd with
|
||||
| "reset" => run reset
|
||||
| "stat" => run stat
|
||||
| "expr.echo" => run expr_echo
|
||||
| "env.catalog" => run env_catalog
|
||||
| "env.inspect" => run env_inspect
|
||||
| "env.add" => run env_add
|
||||
| "options.set" => run options_set
|
||||
| "options.print" => run options_print
|
||||
| "goal.start" => run goal_start
|
||||
| "goal.tactic" => run goal_tactic
|
||||
| "goal.continue" => run goal_continue
|
||||
| "goal.delete" => run goal_delete
|
||||
| "goal.print" => run goal_print
|
||||
| cmd =>
|
||||
let error: Protocol.InteractionError :=
|
||||
errorCommand s!"Unknown command {cmd}"
|
||||
return Lean.toJson error
|
||||
where
|
||||
errorCommand := errorI "command"
|
||||
errorIndex := errorI "index"
|
||||
-- Command Functions
|
||||
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
|
||||
let state ← get
|
||||
let nGoals := state.goalStates.size
|
||||
set { state with nextId := 0, goalStates := Lean.HashMap.empty }
|
||||
return .ok { nGoals }
|
||||
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
|
||||
let state ← get
|
||||
let nGoals := state.goalStates.size
|
||||
return .ok { nGoals }
|
||||
env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
|
||||
let result ← Environment.catalog args
|
||||
return .ok result
|
||||
env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
|
||||
let state ← get
|
||||
Environment.inspect args state.options
|
||||
env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
|
||||
Environment.addDecl args
|
||||
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
|
||||
let state ← get
|
||||
exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
|
||||
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
|
||||
let state ← get
|
||||
let options := state.options
|
||||
set { state with
|
||||
options := {
|
||||
-- FIXME: This should be replaced with something more elegant
|
||||
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
|
||||
printExprPretty := args.printExprPretty?.getD options.printExprPretty,
|
||||
printExprAST := args.printExprAST?.getD options.printExprAST,
|
||||
printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars,
|
||||
noRepeat := args.noRepeat?.getD options.noRepeat,
|
||||
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
|
||||
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
|
||||
}
|
||||
}
|
||||
return .ok { }
|
||||
options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.OptionsPrintResult) := do
|
||||
return .ok (← get).options
|
||||
goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
|
||||
let state ← get
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
|
||||
| .some expr, .none => goalStartExpr expr (args.levels.getD #[])
|
||||
| .none, .some copyFrom =>
|
||||
(match env.find? <| copyFrom.toName with
|
||||
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
|
||||
| .some cInfo => return .ok (← GoalState.create cInfo.type))
|
||||
| _, _ =>
|
||||
return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
|
||||
match expr? with
|
||||
| .error error => return .error error
|
||||
| .ok goalState =>
|
||||
let stateId := state.nextId
|
||||
set { state with
|
||||
goalStates := state.goalStates.insert stateId goalState,
|
||||
nextId := state.nextId + 1
|
||||
}
|
||||
return .ok { stateId, root := goalState.root.name.toString }
|
||||
goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
|
||||
let state ← get
|
||||
match state.goalStates.find? args.stateId with
|
||||
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
|
||||
| .some goalState => do
|
||||
let nextGoalState?: Except _ GoalState ←
|
||||
match args.tactic?, args.expr?, args.have?, args.calc?, args.conv? with
|
||||
| .some tactic, .none, .none, .none, .none => do
|
||||
pure ( Except.ok (← goalTactic goalState args.goalId tactic))
|
||||
| .none, .some expr, .none, .none, .none => do
|
||||
pure ( Except.ok (← goalAssign goalState args.goalId expr))
|
||||
| .none, .none, .some type, .none, .none => do
|
||||
let binderName := args.binderName?.getD ""
|
||||
pure ( Except.ok (← goalHave goalState args.goalId binderName type))
|
||||
| .none, .none, .none, .some pred, .none => do
|
||||
pure ( Except.ok (← goalCalc goalState args.goalId pred))
|
||||
| .none, .none, .none, .none, .some true => do
|
||||
pure ( Except.ok (← goalConv goalState args.goalId))
|
||||
| .none, .none, .none, .none, .some false => do
|
||||
pure ( Except.ok (← goalConvExit goalState))
|
||||
| _, _, _, _, _ => pure (Except.error <|
|
||||
errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied")
|
||||
match nextGoalState? with
|
||||
| .error error => return .error error
|
||||
| .ok (.success nextGoalState) =>
|
||||
let nextStateId := state.nextId
|
||||
set { state with
|
||||
goalStates := state.goalStates.insert state.nextId nextGoalState,
|
||||
nextId := state.nextId + 1,
|
||||
}
|
||||
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
|
||||
return .ok {
|
||||
nextStateId? := .some nextStateId,
|
||||
goals? := .some goals,
|
||||
}
|
||||
| .ok (.parseError message) =>
|
||||
return .ok { parseError? := .some message }
|
||||
| .ok (.indexError goalId) =>
|
||||
return .error $ errorIndex s!"Invalid goal id index {goalId}"
|
||||
| .ok (.invalidAction message) =>
|
||||
return .error $ errorI "invalid" message
|
||||
| .ok (.failure messages) =>
|
||||
return .ok { tacticErrors? := .some messages }
|
||||
goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
|
||||
let state ← get
|
||||
match state.goalStates.find? args.target with
|
||||
| .none => return .error $ errorIndex s!"Invalid state index {args.target}"
|
||||
| .some target => do
|
||||
let nextState? ← match args.branch?, args.goals? with
|
||||
| .some branchId, .none => do
|
||||
match state.goalStates.find? branchId with
|
||||
| .none => return .error $ errorIndex s!"Invalid state index {branchId}"
|
||||
| .some branch => pure $ goalContinue target branch
|
||||
| .none, .some goals =>
|
||||
pure $ goalResume target goals
|
||||
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
|
||||
match nextState? with
|
||||
| .error error => return .error <| errorI "structure" error
|
||||
| .ok nextGoalState =>
|
||||
let nextStateId := state.nextId
|
||||
set { state with
|
||||
goalStates := state.goalStates.insert nextStateId nextGoalState,
|
||||
nextId := state.nextId + 1
|
||||
}
|
||||
let goals ← goalSerialize nextGoalState (options := state.options)
|
||||
return .ok {
|
||||
nextStateId,
|
||||
goals,
|
||||
}
|
||||
goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
|
||||
let state ← get
|
||||
let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates
|
||||
set { state with goalStates }
|
||||
return .ok {}
|
||||
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
|
||||
let state ← get
|
||||
match state.goalStates.find? args.stateId with
|
||||
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
|
||||
| .some goalState => runMetaM <| do
|
||||
return .ok (← goalPrint goalState state.options)
|
||||
|
||||
end Pantograph
|
||||
import Pantograph.Version
|
||||
|
|
|
@ -0,0 +1,25 @@
|
|||
/- Adapted from lean-training-data by semorrison -/
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Compile.Frontend
|
||||
import Pantograph.Compile.Elab
|
||||
import Pantograph.Compile.Parse
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph.Compile
|
||||
|
||||
def collectTacticsFromCompilation (steps : List CompilationStep) : IO (List Protocol.InvokedTactic) := do
|
||||
let infoTrees := steps.bind (·.trees)
|
||||
let tacticInfoTrees := infoTrees.bind λ tree => tree.filter λ
|
||||
| info@(.ofTacticInfo _) => info.isOriginal
|
||||
| _ => false
|
||||
let tactics := tacticInfoTrees.bind collectTactics
|
||||
tactics.mapM λ invocation => do
|
||||
let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
|
||||
let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
|
||||
let tactic ← invocation.ctx.runMetaM {} do
|
||||
let t ← Lean.PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
|
||||
return t.pretty
|
||||
return { goalBefore, goalAfter, tactic }
|
||||
|
||||
end Pantograph.Compile
|
|
@ -0,0 +1,146 @@
|
|||
|
||||
import Lean.Elab.Import
|
||||
import Lean.Elab.Command
|
||||
import Lean.Elab.InfoTree
|
||||
|
||||
import Pantograph.Compile.Frontend
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Lean.Elab.Info
|
||||
/-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
|
||||
protected def stx? : Info → Option Syntax
|
||||
| .ofTacticInfo info => info.stx
|
||||
| .ofTermInfo info => info.stx
|
||||
| .ofCommandInfo info => info.stx
|
||||
| .ofMacroExpansionInfo info => info.stx
|
||||
| .ofOptionInfo info => info.stx
|
||||
| .ofFieldInfo info => info.stx
|
||||
| .ofCompletionInfo info => info.stx
|
||||
| .ofUserWidgetInfo info => info.stx
|
||||
| .ofCustomInfo info => info.stx
|
||||
| .ofFVarAliasInfo _ => none
|
||||
| .ofFieldRedeclInfo info => info.stx
|
||||
| .ofOmissionInfo info => info.stx
|
||||
/-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
|
||||
protected def isOriginal (i : Info) : Bool :=
|
||||
match i.stx? with
|
||||
| none => true -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative.
|
||||
| some stx => match stx.getHeadInfo with
|
||||
| .original .. => true
|
||||
| _ => false
|
||||
end Lean.Elab.Info
|
||||
|
||||
namespace Lean.Elab.TacticInfo
|
||||
|
||||
/-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
|
||||
def name? (t : TacticInfo) : Option Name :=
|
||||
match t.stx with
|
||||
| Syntax.node _ n _ => some n
|
||||
| _ => none
|
||||
/-- Decide whether a tactic is "substantive",
|
||||
or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
|
||||
def isSubstantive (t : TacticInfo) : Bool :=
|
||||
match t.name? with
|
||||
| none => false
|
||||
| some `null => false
|
||||
| some ``cdot => false
|
||||
| some ``cdotTk => false
|
||||
| some ``Lean.Parser.Term.byTactic => false
|
||||
| some ``Lean.Parser.Tactic.tacticSeq => false
|
||||
| some ``Lean.Parser.Tactic.tacticSeq1Indented => false
|
||||
| some ``Lean.Parser.Tactic.«tactic_<;>_» => false
|
||||
| some ``Lean.Parser.Tactic.paren => false
|
||||
| _ => true
|
||||
|
||||
end Lean.Elab.TacticInfo
|
||||
|
||||
namespace Lean.Elab.InfoTree
|
||||
|
||||
/--
|
||||
Keep `.node` nodes and `.hole` nodes satisfying predicates.
|
||||
|
||||
Returns a `List InfoTree`, although in most situations this will be a singleton.
|
||||
-/
|
||||
partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
|
||||
InfoTree → List InfoTree
|
||||
| .context ctx tree => tree.filter p m |>.map (.context ctx)
|
||||
| .node info children =>
|
||||
if p info then
|
||||
[.node info (children.toList.map (filter p m)).join.toPArray']
|
||||
else
|
||||
(children.toList.map (filter p m)).join
|
||||
| .hole mvar => if m mvar then [.hole mvar] else []
|
||||
|
||||
end Lean.Elab.InfoTree
|
||||
|
||||
|
||||
namespace Pantograph.Compile
|
||||
|
||||
-- Info tree filtering functions
|
||||
|
||||
structure TacticInvocation where
|
||||
info : Elab.TacticInfo
|
||||
ctx : Elab.ContextInfo
|
||||
children : PersistentArray Elab.InfoTree
|
||||
namespace TacticInvocation
|
||||
|
||||
/-- Return the range of the tactic, as a pair of file positions. -/
|
||||
protected def range (t : TacticInvocation) : Position × Position := t.ctx.fileMap.stxRange t.info.stx
|
||||
|
||||
/-- Pretty print a tactic. -/
|
||||
protected def pp (t : TacticInvocation) : IO Format :=
|
||||
t.ctx.runMetaM {} try
|
||||
Lean.PrettyPrinter.ppTactic ⟨t.info.stx⟩
|
||||
catch _ =>
|
||||
pure "<failed to pretty print>"
|
||||
|
||||
/-- Run a tactic on the goals stored in a `TacticInvocation`. -/
|
||||
protected def runMetaMGoalsBefore (t : TacticInvocation) (x : List MVarId → MetaM α) : IO α := do
|
||||
t.ctx.runMetaM {} <| Meta.withMCtx t.info.mctxBefore <| x t.info.goalsBefore
|
||||
|
||||
/-- Run a tactic on the after goals stored in a `TacticInvocation`. -/
|
||||
protected def runMetaMGoalsAfter (t : TacticInvocation) (x : List MVarId → MetaM α) : IO α := do
|
||||
t.ctx.runMetaM {} <| Meta.withMCtx t.info.mctxAfter <| x t.info.goalsAfter
|
||||
|
||||
/-- Run a tactic on the main goal stored in a `TacticInvocation`. -/
|
||||
protected def runMetaM (t : TacticInvocation) (x : MVarId → MetaM α) : IO α := do
|
||||
match t.info.goalsBefore.head? with
|
||||
| none => throw <| IO.userError s!"No goals at {← t.pp}"
|
||||
| some g => t.runMetaMGoalsBefore fun _ => do g.withContext <| x g
|
||||
|
||||
protected def goalState (t : TacticInvocation) : IO (List Format) := do
|
||||
t.runMetaMGoalsBefore (fun gs => gs.mapM fun g => do Meta.ppGoal g)
|
||||
|
||||
protected def goalStateAfter (t : TacticInvocation) : IO (List Format) := do
|
||||
t.runMetaMGoalsAfter (fun gs => gs.mapM fun g => do Meta.ppGoal g)
|
||||
|
||||
protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format :=
|
||||
t.runMetaM (fun _ => do Meta.ppExpr (← instantiateMVars e))
|
||||
|
||||
end TacticInvocation
|
||||
|
||||
/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
|
||||
partial def findAllInfo (t : Elab.InfoTree) (ctx : Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
|
||||
List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
|
||||
match t with
|
||||
| .context inner t => findAllInfo t (inner.mergeIntoOuter? ctx) pred
|
||||
| .node i children =>
|
||||
(if pred i then [(i, ctx, children)] else []) ++ children.toList.bind (fun t => findAllInfo t ctx pred)
|
||||
| _ => []
|
||||
|
||||
/-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
|
||||
each equipped with its relevant `ContextInfo`, and any children info trees. -/
|
||||
def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
|
||||
let infos := findAllInfo t none fun i => match i with
|
||||
| .ofTacticInfo _ => true
|
||||
| _ => false
|
||||
infos.filterMap fun p => match p with
|
||||
| (.ofTacticInfo i, some ctx, children) => .some ⟨i, ctx, children⟩
|
||||
| _ => none
|
||||
|
||||
def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
|
||||
collectTacticNodes t |>.filter fun i => i.info.isSubstantive
|
||||
|
||||
|
||||
end Pantograph.Compile
|
|
@ -0,0 +1,86 @@
|
|||
import Lean.Parser
|
||||
import Lean.Elab.Frontend
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Lean.FileMap
|
||||
|
||||
/-- Extract the range of a `Syntax` expressed as lines and columns. -/
|
||||
-- Extracted from the private declaration `Lean.Elab.formatStxRange`,
|
||||
-- in `Lean.Elab.InfoTree.Main`.
|
||||
protected def stxRange (fileMap : FileMap) (stx : Syntax) : Position × Position :=
|
||||
let pos := stx.getPos?.getD 0
|
||||
let endPos := stx.getTailPos?.getD pos
|
||||
(fileMap.toPosition pos, fileMap.toPosition endPos)
|
||||
|
||||
end Lean.FileMap
|
||||
namespace Lean.PersistentArray
|
||||
|
||||
/--
|
||||
Drop the first `n` elements of a `PersistentArray`, returning the results as a `List`.
|
||||
-/
|
||||
-- We can't remove the `[Inhabited α]` hypotheses here until
|
||||
-- `PersistentArray`'s `GetElem` instance also does.
|
||||
protected def drop [Inhabited α] (t : PersistentArray α) (n : Nat) : List α :=
|
||||
List.range (t.size - n) |>.map fun i => t.get! (n + i)
|
||||
|
||||
end Lean.PersistentArray
|
||||
|
||||
|
||||
namespace Pantograph.Compile
|
||||
|
||||
structure CompilationStep where
|
||||
fileName : String
|
||||
fileMap : FileMap
|
||||
src : Substring
|
||||
stx : Syntax
|
||||
before : Environment
|
||||
after : Environment
|
||||
msgs : List Message
|
||||
trees : List Elab.InfoTree
|
||||
|
||||
|
||||
/--
|
||||
Process one command, returning a `CompilationStep` and
|
||||
`done : Bool`, indicating whether this was the last command.
|
||||
-/
|
||||
def processOneCommand: Elab.Frontend.FrontendM (CompilationStep × Bool) := do
|
||||
let s := (← get).commandState
|
||||
let before := s.env
|
||||
let done ← Elab.Frontend.processCommand
|
||||
let stx := (← get).commands.back
|
||||
let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos
|
||||
let s' := (← get).commandState
|
||||
let after := s'.env
|
||||
let msgs := s'.messages.toList.drop s.messages.toList.length
|
||||
let trees := s'.infoState.trees.drop s.infoState.trees.size
|
||||
let ⟨_, fileName, fileMap⟩ := (← read).inputCtx
|
||||
return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)
|
||||
|
||||
partial def processFile : Elab.Frontend.FrontendM (List CompilationStep) := do
|
||||
let (cmd, done) ← processOneCommand
|
||||
if done then
|
||||
return [cmd]
|
||||
else
|
||||
return cmd :: (← processFile)
|
||||
|
||||
|
||||
def findSourcePath (module : Name) : IO System.FilePath := do
|
||||
return System.FilePath.mk ((← findOLean module).toString.replace ".lake/build/lib/" "") |>.withExtension "lean"
|
||||
|
||||
def processSource (module : Name) (opts : Options := {}) : IO (List CompilationStep) := unsafe do
|
||||
let file ← IO.FS.readFile (← findSourcePath module)
|
||||
let inputCtx := Parser.mkInputContext file module.toString
|
||||
|
||||
let (header, parserState, messages) ← Parser.parseHeader inputCtx
|
||||
let (env, messages) ← Elab.processHeader header opts messages inputCtx
|
||||
let commandState := Elab.Command.mkState env messages opts
|
||||
processFile.run { inputCtx }
|
||||
|>.run' {
|
||||
commandState := { commandState with infoState.enabled := true },
|
||||
parserState,
|
||||
cmdPos := parserState.pos
|
||||
}
|
||||
|
||||
|
||||
end Pantograph.Compile
|
|
@ -0,0 +1,14 @@
|
|||
import Lean
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph.Compile
|
||||
|
||||
def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
|
||||
return Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := "<stdin>")
|
||||
|
||||
end Pantograph.Compile
|
|
@ -0,0 +1,96 @@
|
|||
/- structures for FFI based interface -/
|
||||
import Lean
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Expr
|
||||
import Pantograph.Protocol
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph
|
||||
namespace Condensed
|
||||
|
||||
-- Mirrors Lean's LocalDecl
|
||||
structure LocalDecl where
|
||||
-- Default value is for testing
|
||||
fvarId: FVarId := { name := .anonymous }
|
||||
userName: Name
|
||||
|
||||
-- Normalized expression
|
||||
type : Expr
|
||||
value? : Option Expr := .none
|
||||
|
||||
structure Goal where
|
||||
mvarId: MVarId := { name := .anonymous }
|
||||
userName: Name := .anonymous
|
||||
context: Array LocalDecl
|
||||
target: Expr
|
||||
|
||||
@[export pantograph_goal_is_lhs]
|
||||
def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
|
||||
|
||||
-- Functions for creating contexts and states
|
||||
@[export pantograph_elab_context]
|
||||
def elabContext: Elab.Term.Context := {
|
||||
errToSorry := false
|
||||
}
|
||||
|
||||
end Condensed
|
||||
|
||||
-- Get the list of visible (by default) free variables from a goal
|
||||
@[export pantograph_visible_fvars_of_mvar]
|
||||
protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do
|
||||
let mvarDecl ← mctx.findDecl? mvarId
|
||||
let lctx := mvarDecl.lctx
|
||||
return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
|
||||
| some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
|
||||
| none => r
|
||||
|
||||
@[export pantograph_to_condensed_goal_m]
|
||||
def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
|
||||
let ppAuxDecls := Meta.pp.auxDecls.get (← getOptions)
|
||||
let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions)
|
||||
let mvarDecl ← mvarId.getDecl
|
||||
let lctx := mvarDecl.lctx
|
||||
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
|
||||
Meta.withLCtx lctx mvarDecl.localInstances do
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName type _ _ =>
|
||||
let type ← instantiate type
|
||||
return { fvarId, userName, type }
|
||||
| .ldecl _ fvarId userName type value _ _ => do
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiate type
|
||||
let value ← instantiate value
|
||||
return { fvarId, userName, type, value? := .some value }
|
||||
let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
|
||||
let skip := !ppAuxDecls && localDecl.isAuxDecl ||
|
||||
!ppImplDetailHyps && localDecl.isImplementationDetail
|
||||
if skip then
|
||||
return acc
|
||||
else
|
||||
let var ← ppVar localDecl
|
||||
return var::acc
|
||||
return {
|
||||
mvarId,
|
||||
userName := mvarDecl.userName,
|
||||
context := vars.reverse.toArray,
|
||||
target := ← instantiate mvarDecl.type
|
||||
}
|
||||
where
|
||||
instantiate := instantiateAll
|
||||
|
||||
@[export pantograph_goal_state_to_condensed_m]
|
||||
protected def GoalState.toCondensed (state: GoalState):
|
||||
CoreM (Array Condensed.Goal):= do
|
||||
let metaM := do
|
||||
let goals := state.goals.toArray
|
||||
goals.mapM fun goal => do
|
||||
match state.mctx.findDecl? goal with
|
||||
| .some _ =>
|
||||
let serializedGoal ← toCondensedGoal goal
|
||||
pure serializedGoal
|
||||
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
|
||||
metaM.run' (s := state.savedState.term.meta.meta)
|
||||
|
||||
end Pantograph
|
|
@ -7,15 +7,36 @@ open Pantograph
|
|||
|
||||
namespace Pantograph.Environment
|
||||
|
||||
def isNameInternal (n: Lean.Name): Bool :=
|
||||
@[export pantograph_is_name_internal]
|
||||
def isNameInternal (n: Name): Bool :=
|
||||
-- Returns true if the name is an implementation detail which should not be shown to the user.
|
||||
isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma ∨ n.hasMacroScopes
|
||||
where
|
||||
isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
|
||||
isLeanSymbol (name: Name): Bool := match name.getRoot with
|
||||
| .str _ name => name == "Lean"
|
||||
| _ => true
|
||||
|
||||
def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String :=
|
||||
/-- Catalog all the non-internal and safe names -/
|
||||
@[export pantograph_environment_catalog]
|
||||
def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name info =>
|
||||
match isNameInternal name || info.isUnsafe with
|
||||
| false => acc.push name
|
||||
| true => acc)
|
||||
|
||||
@[export pantograph_environment_module_of_name]
|
||||
def module_of_name (env: Environment) (name: Name): Option Name := do
|
||||
let moduleId ← env.getModuleIdxFor? name
|
||||
return env.allImportedModuleNames.get! moduleId.toNat
|
||||
|
||||
@[export pantograph_constant_info_is_unsafe_or_partial]
|
||||
def constantInfoIsUnsafeOrPartial (info: ConstantInfo): Bool := info.isUnsafe || info.isPartial
|
||||
|
||||
@[export pantograph_constant_info_type]
|
||||
def constantInfoType (info: ConstantInfo): CoreM Expr := unfoldAuxLemmas info.type
|
||||
@[export pantograph_constant_info_value]
|
||||
def constantInfoValue (info: ConstantInfo): CoreM (Option Expr) := info.value?.mapM unfoldAuxLemmas
|
||||
|
||||
def toCompactSymbolName (n: Name) (info: ConstantInfo): String :=
|
||||
let pref := match info with
|
||||
| .axiomInfo _ => "a"
|
||||
| .defnInfo _ => "d"
|
||||
|
@ -52,21 +73,22 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
|
|||
| .some false, _ => .none
|
||||
| .none, .defnInfo _ => info.value?
|
||||
| .none, _ => .none
|
||||
let type ← unfoldAuxLemmas info.type
|
||||
let value? ← value?.mapM (λ v => unfoldAuxLemmas v)
|
||||
-- Information common to all symbols
|
||||
let core := {
|
||||
type := ← (serializeExpression options info.type).run',
|
||||
type := ← (serializeExpression options type).run',
|
||||
isUnsafe := info.isUnsafe,
|
||||
value? := ← value?.mapM (λ v => serializeExpression options v |>.run'),
|
||||
publicName? := Lean.privateToUserName? name |>.map (·.toString),
|
||||
-- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
|
||||
typeDependency? := if args.dependency?.getD false
|
||||
then .some <| info.type.getUsedConstants.map (λ n => serializeName n)
|
||||
then .some <| type.getUsedConstants.map (λ n => serializeName n)
|
||||
else .none,
|
||||
valueDependency? := if args.dependency?.getD false
|
||||
then value?.map (λ e =>
|
||||
e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
|
||||
else .none,
|
||||
valueDependency? := ← if args.dependency?.getD false
|
||||
then info.value?.mapM (λ e => do
|
||||
let e ← unfoldAuxLemmas e
|
||||
pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
|
||||
else pure (.none),
|
||||
module? := module?
|
||||
}
|
||||
let result ← match info with
|
||||
|
@ -131,7 +153,7 @@ def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) :
|
|||
(hints := Lean.mkReducibilityHintsRegularEx 1)
|
||||
(safety := Lean.DefinitionSafety.safe)
|
||||
(all := [])
|
||||
let env' ← match env.addDecl constant with
|
||||
let env' ← match env.addDecl (← getOptions) constant with
|
||||
| .error e => do
|
||||
let options ← Lean.MonadOptions.getOptions
|
||||
let desc ← (e.toMessageData options).toString
|
||||
|
|
|
@ -0,0 +1,160 @@
|
|||
import Lean
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
structure ProjectionApplication where
|
||||
projector: Name
|
||||
numParams: Nat
|
||||
inner: Expr
|
||||
|
||||
@[export pantograph_expr_proj_to_app]
|
||||
def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
|
||||
let (typeName, idx, inner) := match e with
|
||||
| .proj typeName idx inner => (typeName, idx, inner)
|
||||
| _ => panic! "Argument must be proj"
|
||||
let ctor := getStructureCtor env typeName
|
||||
let fieldName := getStructureFields env typeName |>.get! idx
|
||||
let projector := getProjFnForField? env typeName fieldName |>.get!
|
||||
{
|
||||
projector,
|
||||
numParams := ctor.numParams,
|
||||
inner,
|
||||
}
|
||||
|
||||
def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
|
||||
|
||||
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
|
||||
@[export pantograph_unfold_aux_lemmas]
|
||||
def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
|
||||
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
|
||||
|
||||
/--
|
||||
Force the instantiation of delayed metavariables even if they cannot be fully
|
||||
instantiated. This is used during resumption to provide diagnostic data about
|
||||
the current goal.
|
||||
|
||||
Since Lean 4 does not have an `Expr` constructor corresponding to delayed
|
||||
metavariables, any delayed metavariables must be recursively handled by this
|
||||
function to ensure that nested delayed metavariables can be properly processed.
|
||||
The caveat is this recursive call will lead to infinite recursion if a loop
|
||||
between metavariable assignment exists.
|
||||
|
||||
This function ensures any metavariable in the result is either
|
||||
1. Delayed assigned with its pending mvar not assigned in any form
|
||||
2. Not assigned (delay or not)
|
||||
-/
|
||||
partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
|
||||
--let padding := String.join $ List.replicate level "│ "
|
||||
--IO.println s!"{padding}Starting {toString eOrig}"
|
||||
let mut result ← Meta.transform (← instantiateMVars eOrig)
|
||||
(pre := fun e => e.withApp fun f args => do
|
||||
let .mvar mvarId := f | return .continue
|
||||
--IO.println s!"{padding}├V {e}"
|
||||
let mvarDecl ← mvarId.getDecl
|
||||
|
||||
-- This is critical to maintaining the interdependency of metavariables.
|
||||
-- Without setting `.syntheticOpaque`, Lean's metavariable elimination
|
||||
-- system will not make the necessary delayed assigned mvars in case of
|
||||
-- nested mvars.
|
||||
mvarId.setKind .syntheticOpaque
|
||||
|
||||
let lctx ← MonadLCtx.getLCtx
|
||||
if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
|
||||
let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
|
||||
| .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
|
||||
| .none => acc) []
|
||||
panic! s!"Local context variable violation: {violations}"
|
||||
|
||||
if let .some assign ← getExprMVarAssignment? mvarId then
|
||||
--IO.println s!"{padding}├A ?{mvarId.name}"
|
||||
assert! !(← mvarId.isDelayedAssigned)
|
||||
return .visit (mkAppN assign args)
|
||||
else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
|
||||
--let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
|
||||
--IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
|
||||
|
||||
if args.size < fvars.size then
|
||||
throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
|
||||
--if !args.isEmpty then
|
||||
--IO.println s!"{padding}├── Arguments Begin"
|
||||
let args ← args.mapM self
|
||||
--if !args.isEmpty then
|
||||
--IO.println s!"{padding}├── Arguments End"
|
||||
if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
|
||||
--IO.println s!"{padding}├T1"
|
||||
let result := mkAppN f args
|
||||
return .done result
|
||||
|
||||
let pending ← mvarIdPending.withContext do
|
||||
let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
|
||||
--IO.println s!"{padding}├Pre: {inner}"
|
||||
pure <| (← inner.abstractM fvars).instantiateRev args
|
||||
|
||||
-- Tail arguments
|
||||
let result := mkAppRange pending fvars.size args.size args
|
||||
--IO.println s!"{padding}├MD {result}"
|
||||
return .done result
|
||||
else
|
||||
assert! !(← mvarId.isAssigned)
|
||||
assert! !(← mvarId.isDelayedAssigned)
|
||||
--if !args.isEmpty then
|
||||
-- IO.println s!"{padding}├── Arguments Begin"
|
||||
let args ← args.mapM self
|
||||
--if !args.isEmpty then
|
||||
-- IO.println s!"{padding}├── Arguments End"
|
||||
|
||||
--IO.println s!"{padding}├M ?{mvarId.name}"
|
||||
return .done (mkAppN f args))
|
||||
--IO.println s!"{padding}└Result {result}"
|
||||
return result
|
||||
where
|
||||
self e := instantiateDelayedMVars e --(level := level + 1)
|
||||
|
||||
/--
|
||||
Convert an expression to an equiavlent form with
|
||||
1. No nested delayed assigned mvars
|
||||
2. No aux lemmas
|
||||
3. No assigned mvars
|
||||
-/
|
||||
@[export pantograph_instantiate_all_m]
|
||||
def instantiateAll (e: Expr): MetaM Expr := do
|
||||
let e ← instantiateDelayedMVars e
|
||||
let e ← unfoldAuxLemmas e
|
||||
return e
|
||||
|
||||
structure DelayedMVarInvocation where
|
||||
mvarIdPending: MVarId
|
||||
args: Array (FVarId × (Option Expr))
|
||||
-- Extra arguments applied to the result of this substitution
|
||||
tail: Array Expr
|
||||
|
||||
-- The pending mvar of any delayed assigned mvar must not be assigned in any way.
|
||||
@[export pantograph_to_delayed_mvar_invocation_m]
|
||||
def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
|
||||
let .mvar mvarId := e.getAppFn | return .none
|
||||
let .some decl ← getDelayedMVarAssignment? mvarId | return .none
|
||||
let mvarIdPending := decl.mvarIdPending
|
||||
let mvarDecl ← mvarIdPending.getDecl
|
||||
-- Print the function application e. See Lean's `withOverApp`
|
||||
let args := e.getAppArgs
|
||||
|
||||
assert! args.size ≥ decl.fvars.size
|
||||
assert! !(← mvarIdPending.isAssigned)
|
||||
assert! !(← mvarIdPending.isDelayedAssigned)
|
||||
let fvarArgMap: HashMap FVarId Expr := HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
|
||||
let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
|
||||
let fvarId := localDecl.fvarId
|
||||
let a := fvarArgMap.find? fvarId
|
||||
return acc ++ [(fvarId, a)]
|
||||
|
||||
assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)
|
||||
|
||||
return .some {
|
||||
mvarIdPending,
|
||||
args := subst.toArray,
|
||||
tail := args.toList.drop decl.fvars.size |>.toArray,
|
||||
}
|
||||
|
||||
end Pantograph
|
|
@ -4,13 +4,10 @@ Functions for handling metavariables
|
|||
All the functions starting with `try` resume their inner monadic state.
|
||||
-/
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Tactic
|
||||
import Pantograph.Compile.Parse
|
||||
import Lean
|
||||
|
||||
def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
|
||||
{
|
||||
msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false
|
||||
}
|
||||
|
||||
|
||||
namespace Pantograph
|
||||
open Lean
|
||||
|
@ -25,78 +22,165 @@ structure GoalState where
|
|||
|
||||
-- The root hole which is the search target
|
||||
root: MVarId
|
||||
-- New metavariables acquired in this state
|
||||
newMVars: SSet MVarId
|
||||
|
||||
-- Parent state metavariable source
|
||||
parentMVar?: Option MVarId
|
||||
|
||||
-- Existence of this field shows that we are currently in `conv` mode.
|
||||
convMVar?: Option (MVarId × MVarId) := .none
|
||||
-- (convRhs, goal, dormant)
|
||||
convMVar?: Option (MVarId × MVarId × List MVarId) := .none
|
||||
-- Previous RHS for calc, so we don't have to repeat it every time
|
||||
-- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
|
||||
calcPrevRhs?: Option Expr := .none
|
||||
calcPrevRhs?: Option (MVarId × Expr) := .none
|
||||
|
||||
@[export pantograph_goal_state_create_m]
|
||||
protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
|
||||
-- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context.
|
||||
-- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
|
||||
|
||||
--Elab.Term.synthesizeSyntheticMVarsNoPostponing
|
||||
--let expr ← instantiateMVars expr
|
||||
let goal ← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous)
|
||||
let root ← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous)
|
||||
let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
|
||||
let root := goal.mvarId!
|
||||
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]}
|
||||
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root.mvarId!]}
|
||||
return {
|
||||
root,
|
||||
root := root.mvarId!,
|
||||
savedState,
|
||||
newMVars := SSet.insert .empty root,
|
||||
parentMVar? := .none,
|
||||
}
|
||||
@[export pantograph_goal_state_is_conv]
|
||||
protected def GoalState.isConv (state: GoalState): Bool :=
|
||||
state.convMVar?.isSome
|
||||
protected def GoalState.goals (state: GoalState): List MVarId :=
|
||||
state.savedState.tactic.goals
|
||||
@[export pantograph_goal_state_goals]
|
||||
protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray
|
||||
protected def GoalState.mctx (state: GoalState): MetavarContext :=
|
||||
state.savedState.term.meta.meta.mctx
|
||||
protected def GoalState.env (state: GoalState): Environment :=
|
||||
state.savedState.term.meta.core.env
|
||||
|
||||
@[export pantograph_goal_state_meta_context_of_goal]
|
||||
protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do
|
||||
let mvarDecl ← state.mctx.findDecl? mvarId
|
||||
return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
|
||||
protected def GoalState.metaState (state: GoalState): Meta.State :=
|
||||
state.savedState.term.meta.meta
|
||||
|
||||
protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
|
||||
mvarId.withContext m |>.run' (← read) state.metaState
|
||||
|
||||
protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
|
||||
Meta.mapMetaM <| state.withContext state.parentMVar?.get!
|
||||
protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
|
||||
Meta.mapMetaM <| state.withContext state.root
|
||||
|
||||
private def GoalState.mvars (state: GoalState): SSet MVarId :=
|
||||
state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
|
||||
protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
|
||||
state.savedState.term.meta.restore
|
||||
private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
|
||||
protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
|
||||
state.savedState.term.restore
|
||||
private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
|
||||
state.savedState.restore
|
||||
Elab.Tactic.setGoals [goal]
|
||||
|
||||
private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId :=
|
||||
mctxNew.decls.foldl (fun acc mvarId mvarDecl =>
|
||||
if let .some prevMVarDecl := mctxOld.decls.find? mvarId then
|
||||
assert! prevMVarDecl.type == mvarDecl.type
|
||||
acc
|
||||
else
|
||||
acc.insert mvarId
|
||||
) SSet.empty
|
||||
@[export pantograph_goal_state_focus]
|
||||
protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
|
||||
let goal ← state.savedState.tactic.goals.get? goalId
|
||||
return {
|
||||
state with
|
||||
savedState := {
|
||||
state.savedState with
|
||||
tactic := { goals := [goal] },
|
||||
},
|
||||
calcPrevRhs? := .none,
|
||||
}
|
||||
|
||||
/-- Inner function for executing tactic on goal state -/
|
||||
def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
|
||||
Elab.TermElabM (Except (Array String) Elab.Tactic.SavedState):= do
|
||||
let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := do
|
||||
state.restore
|
||||
Elab.Tactic.setGoals [goal]
|
||||
try
|
||||
Elab.Tactic.evalTactic stx
|
||||
if (← getThe Core.State).messages.hasErrors then
|
||||
let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
|
||||
let errors ← (messages.map (·.data)).mapM fun md => md.toString
|
||||
return .error errors
|
||||
else
|
||||
return .ok (← MonadBacktrack.saveState)
|
||||
catch exception =>
|
||||
return .error #[← exception.toMessageData.toString]
|
||||
tacticM tactic { elaborator := .anonymous } |>.run' state.tactic
|
||||
/-- Immediately bring all parent goals back into scope. Used in automatic mode -/
|
||||
@[export pantograph_goal_state_immediate_resume_parent]
|
||||
protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
|
||||
-- Prune parents solved goals
|
||||
let mctx := state.mctx
|
||||
let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
|
||||
{
|
||||
state with
|
||||
savedState := {
|
||||
state.savedState with
|
||||
tactic := { goals := state.goals ++ parentGoals },
|
||||
},
|
||||
}
|
||||
|
||||
/--
|
||||
Brings into scope a list of goals
|
||||
-/
|
||||
@[export pantograph_goal_state_resume]
|
||||
protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
|
||||
if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
|
||||
let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
|
||||
.error s!"Goals {invalid_goals} are not in scope"
|
||||
else
|
||||
-- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
|
||||
let unassigned := goals.filter (λ goal =>
|
||||
let mctx := state.mctx
|
||||
¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
|
||||
.ok {
|
||||
state with
|
||||
savedState := {
|
||||
term := state.savedState.term,
|
||||
tactic := { goals := unassigned },
|
||||
},
|
||||
}
|
||||
/--
|
||||
Brings into scope all goals from `branch`
|
||||
-/
|
||||
@[export pantograph_goal_state_continue]
|
||||
protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
|
||||
if !target.goals.isEmpty then
|
||||
.error s!"Target state has unresolved goals"
|
||||
else if target.root != branch.root then
|
||||
.error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}"
|
||||
else
|
||||
target.resume (goals := branch.goals)
|
||||
|
||||
@[export pantograph_goal_state_root_expr]
|
||||
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
|
||||
let expr ← goalState.mctx.eAssignment.find? goalState.root
|
||||
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
|
||||
if expr.hasExprMVar then
|
||||
-- Must not assert that the goal state is empty here. We could be in a branch goal.
|
||||
--assert! ¬goalState.goals.isEmpty
|
||||
.none
|
||||
else
|
||||
assert! goalState.goals.isEmpty
|
||||
return expr
|
||||
@[export pantograph_goal_state_parent_expr]
|
||||
protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
|
||||
let parent ← goalState.parentMVar?
|
||||
let expr := goalState.mctx.eAssignment.find! parent
|
||||
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
|
||||
return expr
|
||||
@[export pantograph_goal_state_get_mvar_e_assignment]
|
||||
protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarId): Option Expr := do
|
||||
let expr ← goalState.mctx.eAssignment.find? mvarId
|
||||
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
|
||||
return expr
|
||||
|
||||
--- Tactic execution functions ---
|
||||
|
||||
protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
|
||||
: Elab.TermElabM GoalState := do
|
||||
unless (← getMCtx).decls.contains goal do
|
||||
throwError s!"Goal is not in context: {goal.name}"
|
||||
goal.checkNotAssigned `GoalState.step
|
||||
let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
|
||||
let nextElabState ← MonadBacktrack.saveState
|
||||
return {
|
||||
state with
|
||||
savedState := { term := nextElabState, tactic := newGoals },
|
||||
parentMVar? := .some goal,
|
||||
calcPrevRhs? := .none,
|
||||
}
|
||||
|
||||
/-- Response for executing a tactic -/
|
||||
inductive TacticResult where
|
||||
|
@ -106,19 +190,22 @@ inductive TacticResult where
|
|||
| failure (messages: Array String)
|
||||
-- Could not parse tactic
|
||||
| parseError (message: String)
|
||||
-- The goal index is out of bounds
|
||||
| indexError (goalId: Nat)
|
||||
-- The given action cannot be executed in the state
|
||||
| invalidAction (message: String)
|
||||
|
||||
/-- Execute tactic on given state -/
|
||||
protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
|
||||
/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
|
||||
protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit):
|
||||
Elab.TermElabM TacticResult := do
|
||||
try
|
||||
let nextState ← state.step goal tacticM
|
||||
return .success nextState
|
||||
catch exception =>
|
||||
return .failure #[← exception.toMessageData.toString]
|
||||
|
||||
/-- Execute a string tactic on given state. Restores TermElabM -/
|
||||
protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let goal ← match state.savedState.tactic.goals.get? goalId with
|
||||
| .some goal => pure $ goal
|
||||
| .none => return .indexError goalId
|
||||
goal.checkNotAssigned `GoalState.tryTactic
|
||||
let tactic ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := if state.isConv then `conv else `tactic)
|
||||
|
@ -126,213 +213,68 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
|
|||
(fileName := filename) with
|
||||
| .ok stx => pure $ stx
|
||||
| .error error => return .parseError error
|
||||
match ← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic) with
|
||||
| .error errors =>
|
||||
return .failure errors
|
||||
| .ok nextSavedState =>
|
||||
-- Assert that the definition of metavariables are the same
|
||||
let nextMCtx := nextSavedState.term.meta.meta.mctx
|
||||
let prevMCtx := state.mctx
|
||||
-- Generate a list of mvarIds that exist in the parent state; Also test the
|
||||
-- assertion that the types have not changed on any mvars.
|
||||
return .success {
|
||||
state with
|
||||
savedState := nextSavedState
|
||||
newMVars := newMVarSet prevMCtx nextMCtx,
|
||||
parentMVar? := .some goal,
|
||||
calcPrevRhs? := .none,
|
||||
}
|
||||
state.tryTacticM goal $ Elab.Tactic.evalTactic tactic
|
||||
|
||||
/-- Assumes elabM has already been restored. Assumes expr has already typechecked -/
|
||||
protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
|
||||
Elab.TermElabM TacticResult := do
|
||||
let goalType ← goal.getType
|
||||
try
|
||||
-- For some reason this is needed. One of the unit tests will fail if this isn't here
|
||||
let error?: Option String ← goal.withContext do
|
||||
let exprType ← Meta.inferType expr
|
||||
if ← Meta.isDefEq goalType exprType then
|
||||
pure .none
|
||||
else do
|
||||
return .some s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} != {← Meta.ppExpr goalType}"
|
||||
if let .some error := error? then
|
||||
return .parseError error
|
||||
goal.checkNotAssigned `GoalState.assign
|
||||
goal.assign expr
|
||||
if (← getThe Core.State).messages.hasErrors then
|
||||
let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
|
||||
let errors ← (messages.map (·.data)).mapM fun md => md.toString
|
||||
return .failure errors
|
||||
let prevMCtx := state.savedState.term.meta.meta.mctx
|
||||
let nextMCtx ← getMCtx
|
||||
-- Generate a list of mvarIds that exist in the parent state; Also test the
|
||||
-- assertion that the types have not changed on any mvars.
|
||||
let newMVars := newMVarSet prevMCtx nextMCtx
|
||||
let nextGoals ← newMVars.toList.filterM (λ mvar => do pure !(← mvar.isAssigned))
|
||||
return .success {
|
||||
root := state.root,
|
||||
savedState := {
|
||||
term := ← MonadBacktrack.saveState,
|
||||
tactic := { goals := nextGoals }
|
||||
},
|
||||
newMVars,
|
||||
parentMVar? := .some goal,
|
||||
calcPrevRhs? := .none
|
||||
}
|
||||
catch exception =>
|
||||
return .failure #[← exception.toMessageData.toString]
|
||||
|
||||
protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String):
|
||||
protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let goal ← match state.savedState.tactic.goals.get? goalId with
|
||||
| .some goal => pure goal
|
||||
| .none => return .indexError goalId
|
||||
let expr ← match Parser.runParserCategory
|
||||
(env := state.env)
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := expr)
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
let goalType ← goal.getType
|
||||
try
|
||||
let expr ← goal.withContext $
|
||||
Elab.Term.elabTermAndSynthesize (stx := expr) (expectedType? := .some goalType)
|
||||
state.assign goal expr
|
||||
catch exception =>
|
||||
return .failure #[← exception.toMessageData.toString]
|
||||
state.tryTacticM goal $ Tactic.evalAssign expr
|
||||
|
||||
-- Specialized Tactics
|
||||
|
||||
protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
|
||||
protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let goal ← match state.savedState.tactic.goals.get? goalId with
|
||||
| .some goal => pure goal
|
||||
| .none => return .indexError goalId
|
||||
let type ← match Parser.runParserCategory
|
||||
(env := state.env)
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := type)
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
let binderName := binderName.toName
|
||||
try
|
||||
-- Implemented similarly to the intro tactic
|
||||
let nextGoals: List MVarId ← goal.withContext do
|
||||
let type ← Elab.Term.elabType (stx := type)
|
||||
let lctx ← MonadLCtx.getLCtx
|
||||
|
||||
-- The branch goal inherits the same context, but with a different type
|
||||
let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
|
||||
|
||||
-- Create the context for the `upstream` goal
|
||||
let fvarId ← mkFreshFVarId
|
||||
let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
|
||||
let fvar := mkFVar fvarId
|
||||
let mvarUpstream ←
|
||||
withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
|
||||
Meta.withNewLocalInstances #[fvar] 0 do
|
||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
||||
(← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
|
||||
let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
|
||||
goal.assign expr
|
||||
pure mvarUpstream
|
||||
|
||||
pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
|
||||
return .success {
|
||||
root := state.root,
|
||||
savedState := {
|
||||
term := ← MonadBacktrack.saveState,
|
||||
tactic := { goals := nextGoals }
|
||||
},
|
||||
newMVars := nextGoals.toSSet,
|
||||
parentMVar? := .some goal,
|
||||
calcPrevRhs? := .none
|
||||
}
|
||||
catch exception =>
|
||||
return .failure #[← exception.toMessageData.toString]
|
||||
protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let goal ← match state.savedState.tactic.goals.get? goalId with
|
||||
| .some goal => pure goal
|
||||
| .none => return .indexError goalId
|
||||
let type ← match Parser.runParserCategory
|
||||
(env := state.env)
|
||||
(catName := `term)
|
||||
(input := type)
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
let binderName := binderName.toName
|
||||
try
|
||||
-- Implemented similarly to the intro tactic
|
||||
let nextGoals: List MVarId ← goal.withContext do
|
||||
let type ← Elab.Term.elabType (stx := type)
|
||||
let lctx ← MonadLCtx.getLCtx
|
||||
|
||||
-- The branch goal inherits the same context, but with a different type
|
||||
let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
|
||||
|
||||
let upstreamType := .letE binderName type mvarBranch (← goal.getType) false
|
||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
||||
upstreamType (kind := MetavarKind.synthetic) (userName := (← goal.getTag))
|
||||
|
||||
goal.assign mvarUpstream
|
||||
|
||||
pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
|
||||
return .success {
|
||||
root := state.root,
|
||||
savedState := {
|
||||
term := ← MonadBacktrack.saveState,
|
||||
tactic := { goals := nextGoals }
|
||||
},
|
||||
newMVars := nextGoals.toSSet,
|
||||
parentMVar? := .some goal,
|
||||
calcPrevRhs? := .none
|
||||
}
|
||||
catch exception =>
|
||||
return .failure #[← exception.toMessageData.toString]
|
||||
state.tryTacticM goal $ Tactic.evalLet binderName.toName type
|
||||
|
||||
/-- Enter conv tactic mode -/
|
||||
protected def GoalState.conv (state: GoalState) (goalId: Nat):
|
||||
protected def GoalState.conv (state: GoalState) (goal: MVarId):
|
||||
Elab.TermElabM TacticResult := do
|
||||
if state.convMVar?.isSome then
|
||||
return .invalidAction "Already in conv state"
|
||||
let goal ← match state.savedState.tactic.goals.get? goalId with
|
||||
| .some goal => pure goal
|
||||
| .none => return .indexError goalId
|
||||
goal.checkNotAssigned `GoalState.conv
|
||||
let tacticM : Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
|
||||
state.restoreTacticM goal
|
||||
|
||||
-- See Lean.Elab.Tactic.Conv.convTarget
|
||||
let convMVar ← Elab.Tactic.withMainContext do
|
||||
let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
|
||||
Elab.Tactic.setGoals [newGoal.mvarId!]
|
||||
Elab.Tactic.replaceMainGoal [newGoal.mvarId!]
|
||||
pure rhs.mvarId!
|
||||
return (← MonadBacktrack.saveState, convMVar)
|
||||
try
|
||||
let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
|
||||
let prevMCtx := state.mctx
|
||||
let nextMCtx := nextSavedState.term.meta.meta.mctx
|
||||
-- Other goals are now dormant
|
||||
let otherGoals := state.goals.filter $ λ g => g != goal
|
||||
return .success {
|
||||
root := state.root,
|
||||
savedState := nextSavedState
|
||||
newMVars := newMVarSet prevMCtx nextMCtx,
|
||||
parentMVar? := .some goal,
|
||||
convMVar? := .some (convRhs, goal),
|
||||
convMVar? := .some (convRhs, goal, otherGoals),
|
||||
calcPrevRhs? := .none
|
||||
}
|
||||
catch exception =>
|
||||
return .failure #[← exception.toMessageData.toString]
|
||||
|
||||
/-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
|
||||
@[export pantograph_goal_state_conv_exit_m]
|
||||
protected def GoalState.convExit (state: GoalState):
|
||||
Elab.TermElabM TacticResult := do
|
||||
let (convRhs, convGoal) ← match state.convMVar? with
|
||||
let (convRhs, convGoal, _) ← match state.convMVar? with
|
||||
| .some mvar => pure mvar
|
||||
| .none => return .invalidAction "Not in conv state"
|
||||
let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
|
||||
|
@ -355,12 +297,9 @@ protected def GoalState.convExit (state: GoalState):
|
|||
MonadBacktrack.saveState
|
||||
try
|
||||
let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
|
||||
let nextMCtx := nextSavedState.term.meta.meta.mctx
|
||||
let prevMCtx := state.savedState.term.meta.meta.mctx
|
||||
return .success {
|
||||
root := state.root,
|
||||
savedState := nextSavedState
|
||||
newMVars := newMVarSet prevMCtx nextMCtx,
|
||||
parentMVar? := .some convGoal,
|
||||
convMVar? := .none
|
||||
calcPrevRhs? := .none
|
||||
|
@ -368,19 +307,18 @@ protected def GoalState.convExit (state: GoalState):
|
|||
catch exception =>
|
||||
return .failure #[← exception.toMessageData.toString]
|
||||
|
||||
protected def GoalState.calcPrevRhsOf? (state: GoalState) (goalId: Nat) :=
|
||||
if goalId == 1 then
|
||||
state.calcPrevRhs?
|
||||
protected def GoalState.calcPrevRhsOf? (state: GoalState) (goal: MVarId): Option Expr := do
|
||||
let (mvarId, rhs) ← state.calcPrevRhs?
|
||||
if mvarId == goal then
|
||||
.some rhs
|
||||
else
|
||||
.none
|
||||
protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
|
||||
@[export pantograph_goal_state_try_calc_m]
|
||||
protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
if state.convMVar?.isSome then
|
||||
return .invalidAction "Cannot initiate `calc` while in `conv` state"
|
||||
let goal ← match state.savedState.tactic.goals.get? goalId with
|
||||
| .some goal => pure goal
|
||||
| .none => return .indexError goalId
|
||||
let `(term|$pred) ← match Parser.runParserCategory
|
||||
(env := state.env)
|
||||
(catName := `term)
|
||||
|
@ -388,9 +326,11 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
|
|||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
let calcPrevRhs? := state.calcPrevRhsOf? goalId
|
||||
let target ← instantiateMVars (← goal.getDecl).type
|
||||
let tag := (← goal.getDecl).userName
|
||||
goal.checkNotAssigned `GoalState.tryCalc
|
||||
let calcPrevRhs? := state.calcPrevRhsOf? goal
|
||||
let decl ← goal.getDecl
|
||||
let target ← instantiateMVars decl.type
|
||||
let tag := decl.userName
|
||||
try
|
||||
goal.withContext do
|
||||
|
||||
|
@ -414,9 +354,8 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
|
|||
(userName := tag ++ `calc)
|
||||
let mvarBranch := proof.mvarId!
|
||||
|
||||
let calcPrevRhs? := Option.some rhs
|
||||
let mut proofType ← Meta.inferType proof
|
||||
let mut remainder := Option.none
|
||||
let mut remainder? := Option.none
|
||||
|
||||
-- The calc tactic either solves the main goal or leaves another relation.
|
||||
-- Replace the main goal, and save the new goal if necessary
|
||||
|
@ -429,17 +368,17 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
|
|||
let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag
|
||||
(proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep
|
||||
unless ← Meta.isDefEq proofType target do throwFailed
|
||||
remainder := .some lastStepGoal.mvarId!
|
||||
remainder? := .some lastStepGoal.mvarId!
|
||||
goal.assign proof
|
||||
|
||||
let goals := [ mvarBranch ] ++ remainder.toList
|
||||
let goals := [ mvarBranch ] ++ remainder?.toList
|
||||
let calcPrevRhs? := remainder?.map $ λ g => (g, rhs)
|
||||
return .success {
|
||||
root := state.root,
|
||||
savedState := {
|
||||
term := ← MonadBacktrack.saveState,
|
||||
tactic := { goals },
|
||||
},
|
||||
newMVars := goals.toSSet,
|
||||
parentMVar? := .some goal,
|
||||
calcPrevRhs?
|
||||
}
|
||||
|
@ -447,66 +386,19 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
|
|||
return .failure #[← exception.toMessageData.toString]
|
||||
|
||||
|
||||
protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
|
||||
let goal ← state.savedState.tactic.goals.get? goalId
|
||||
return {
|
||||
state with
|
||||
savedState := {
|
||||
state.savedState with
|
||||
tactic := { goals := [goal] },
|
||||
},
|
||||
calcPrevRhs? := .none,
|
||||
}
|
||||
|
||||
/--
|
||||
Brings into scope a list of goals
|
||||
-/
|
||||
protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
|
||||
if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
|
||||
.error s!"Goals not in scope"
|
||||
else
|
||||
-- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
|
||||
let unassigned := goals.filter (λ goal =>
|
||||
let mctx := state.mctx
|
||||
¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
|
||||
.ok {
|
||||
state with
|
||||
savedState := {
|
||||
term := state.savedState.term,
|
||||
tactic := { goals := unassigned },
|
||||
},
|
||||
calcPrevRhs? := .none,
|
||||
}
|
||||
/--
|
||||
Brings into scope all goals from `branch`
|
||||
-/
|
||||
protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
|
||||
if !target.goals.isEmpty then
|
||||
.error s!"Target state has unresolved goals"
|
||||
else if target.root != branch.root then
|
||||
.error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}"
|
||||
else
|
||||
target.resume (goals := branch.goals)
|
||||
|
||||
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
|
||||
let expr ← goalState.mctx.eAssignment.find? goalState.root
|
||||
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
|
||||
if expr.hasMVar then
|
||||
-- Must not assert that the goal state is empty here. We could be in a branch goal.
|
||||
--assert! ¬goalState.goals.isEmpty
|
||||
.none
|
||||
else
|
||||
assert! goalState.goals.isEmpty
|
||||
return expr
|
||||
protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
|
||||
let parent ← goalState.parentMVar?
|
||||
let expr := goalState.mctx.eAssignment.find! parent
|
||||
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
|
||||
return expr
|
||||
protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do
|
||||
let expr ← goalState.mctx.eAssignment.find? mvar
|
||||
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
|
||||
return expr
|
||||
|
||||
protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let recursor ← match (← Compile.parseTermM recursor) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor)
|
||||
protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let eq ← match (← Compile.parseTermM eq) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -1,3 +1,4 @@
|
|||
import Pantograph.Condensed
|
||||
import Pantograph.Environment
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Protocol
|
||||
|
@ -38,13 +39,10 @@ open Lean
|
|||
|
||||
namespace Pantograph
|
||||
|
||||
def defaultTermElabMContext: Elab.Term.Context := {
|
||||
errToSorry := false
|
||||
}
|
||||
def runMetaM { α } (metaM: MetaM α): CoreM α :=
|
||||
metaM.run'
|
||||
def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
|
||||
termElabM.run' (ctx := defaultTermElabMContext) |>.run'
|
||||
termElabM.run' (ctx := Condensed.elabContext) |>.run'
|
||||
|
||||
def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
|
||||
|
||||
|
@ -78,22 +76,12 @@ def createCoreState (imports: Array String): IO Core.State := do
|
|||
(trustLevel := 1)
|
||||
return { env := env }
|
||||
|
||||
@[export pantograph_env_catalog_m]
|
||||
def envCatalog: CoreM Protocol.EnvCatalogResult :=
|
||||
Environment.catalog ({}: Protocol.EnvCatalog)
|
||||
|
||||
@[export pantograph_env_inspect_m]
|
||||
def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
|
||||
CoreM (Protocol.CR Protocol.EnvInspectResult) :=
|
||||
Environment.inspect ({
|
||||
name, value? := .some value, dependency?:= .some dependency
|
||||
}: Protocol.EnvInspect) options
|
||||
|
||||
@[export pantograph_env_add_m]
|
||||
def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
|
||||
CoreM (Protocol.CR Protocol.EnvAddResult) :=
|
||||
Environment.addDecl { name, type, value, isTheorem }
|
||||
|
||||
@[export pantograph_parse_elab_type_m]
|
||||
def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
|
||||
let env ← MonadEnv.getEnv
|
||||
let syn ← match parseTerm env type with
|
||||
|
@ -104,6 +92,7 @@ def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
|
|||
| .ok expr => return .ok (← instantiateMVars expr)
|
||||
|
||||
/-- This must be a TermElabM since the parsed expr contains extra information -/
|
||||
@[export pantograph_parse_elab_expr_m]
|
||||
def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do
|
||||
let env ← MonadEnv.getEnv
|
||||
let expectedType? ← match ← expectedType?.mapM parseElabType with
|
||||
|
@ -141,45 +130,10 @@ def goalStartExpr (expr: String) (levels: Array String): CoreM (Protocol.CR Goal
|
|||
| .ok expr => pure $ expr
|
||||
return .ok $ ← GoalState.create expr
|
||||
|
||||
@[export pantograph_goal_tactic_m]
|
||||
def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryTactic goalId tactic
|
||||
|
||||
@[export pantograph_goal_assign_m]
|
||||
def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryAssign goalId expr
|
||||
|
||||
@[export pantograph_goal_have_m]
|
||||
def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryHave goalId binderName type
|
||||
@[export pantograph_goal_let_m]
|
||||
def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryLet goalId binderName type
|
||||
|
||||
@[export pantograph_goal_conv_m]
|
||||
def goalConv (state: GoalState) (goalId: Nat): CoreM TacticResult :=
|
||||
runTermElabM <| state.conv goalId
|
||||
|
||||
@[export pantograph_goal_conv_exit_m]
|
||||
def goalConvExit (state: GoalState): CoreM TacticResult :=
|
||||
runTermElabM <| state.convExit
|
||||
|
||||
@[export pantograph_goal_calc_m]
|
||||
def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryCalc goalId pred
|
||||
|
||||
@[export pantograph_goal_focus]
|
||||
def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
|
||||
state.focus goalId
|
||||
|
||||
@[export pantograph_goal_resume]
|
||||
def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
|
||||
target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
|
||||
|
||||
@[export pantograph_goal_continue]
|
||||
def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
|
||||
target.continue branch
|
||||
|
||||
@[export pantograph_goal_serialize_m]
|
||||
def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
|
||||
runMetaM <| state.serializeGoals (parent := .none) options
|
||||
|
@ -189,11 +143,47 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.G
|
|||
runMetaM do
|
||||
state.restoreMetaM
|
||||
return {
|
||||
root? := ← state.rootExpr?.mapM (λ expr => do
|
||||
serializeExpression options (← unfoldAuxLemmas expr)),
|
||||
parent? := ← state.parentExpr?.mapM (λ expr => do
|
||||
serializeExpression options (← unfoldAuxLemmas expr)),
|
||||
root? := ← state.rootExpr?.mapM (λ expr =>
|
||||
state.withRootContext do
|
||||
serializeExpression options (← instantiateAll expr)),
|
||||
parent? := ← state.parentExpr?.mapM (λ expr =>
|
||||
state.withParentContext do
|
||||
serializeExpression options (← instantiateAll expr)),
|
||||
}
|
||||
|
||||
@[export pantograph_goal_tactic_m]
|
||||
def goalTactic (state: GoalState) (goal: MVarId) (tactic: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryTactic goal tactic
|
||||
@[export pantograph_goal_assign_m]
|
||||
def goalAssign (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryAssign goal expr
|
||||
@[export pantograph_goal_have_m]
|
||||
protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := do
|
||||
let type ← match (← Compile.parseTermM type) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
runTermElabM do
|
||||
state.restoreElabM
|
||||
state.tryTacticM goal $ Tactic.evalHave binderName.toName type
|
||||
@[export pantograph_goal_try_define_m]
|
||||
protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): CoreM TacticResult := do
|
||||
let expr ← match (← Compile.parseTermM expr) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
runTermElabM do
|
||||
state.restoreElabM
|
||||
state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
|
||||
@[export pantograph_goal_let_m]
|
||||
def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryLet goal binderName type
|
||||
@[export pantograph_goal_conv_m]
|
||||
def goalConv (state: GoalState) (goal: MVarId): CoreM TacticResult :=
|
||||
runTermElabM <| state.conv goal
|
||||
@[export pantograph_goal_conv_exit_m]
|
||||
def goalConvExit (state: GoalState): CoreM TacticResult :=
|
||||
runTermElabM <| state.convExit
|
||||
@[export pantograph_goal_calc_m]
|
||||
def goalCalc (state: GoalState) (goal: MVarId) (pred: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryCalc goal pred
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -27,6 +27,8 @@ structure Options where
|
|||
printAuxDecls: Bool := false
|
||||
-- See `pp.implementationDetailHyps`
|
||||
printImplementationDetailHyps: Bool := false
|
||||
-- If this is set to `true`, goals will never go dormant, so you don't have to manage resumption
|
||||
automaticMode: Bool := true
|
||||
deriving Lean.ToJson
|
||||
|
||||
abbrev OptionsT := ReaderT Options
|
||||
|
@ -51,7 +53,7 @@ structure Variable where
|
|||
/-- The name displayed to the user -/
|
||||
userName: String
|
||||
/-- Does the name contain a dagger -/
|
||||
isInaccessible?: Option Bool := .none
|
||||
isInaccessible: Bool := false
|
||||
type?: Option Expression := .none
|
||||
value?: Option Expression := .none
|
||||
deriving Lean.ToJson
|
||||
|
@ -190,12 +192,12 @@ structure OptionsSet where
|
|||
noRepeat?: Option Bool
|
||||
printAuxDecls?: Option Bool
|
||||
printImplementationDetailHyps?: Option Bool
|
||||
automaticMode?: Option Bool
|
||||
deriving Lean.FromJson
|
||||
structure OptionsSetResult where
|
||||
deriving Lean.ToJson
|
||||
structure OptionsPrint where
|
||||
deriving Lean.FromJson
|
||||
abbrev OptionsPrintResult := Options
|
||||
|
||||
structure GoalStart where
|
||||
-- Only one of the fields below may be populated.
|
||||
|
@ -278,6 +280,26 @@ structure GoalDiag where
|
|||
-- Print all mvars
|
||||
printAll: Bool := false
|
||||
instantiate: Bool := true
|
||||
printSexp: Bool := false
|
||||
|
||||
|
||||
/-- Executes the Lean compiler on a single file -/
|
||||
structure CompileUnit where
|
||||
module: String
|
||||
-- If set to true, query the string boundaries of compilation units
|
||||
compilationUnits: Bool := false
|
||||
-- If set to true, collect tactic invocations
|
||||
invocations: Bool := false
|
||||
deriving Lean.FromJson
|
||||
structure InvokedTactic where
|
||||
goalBefore: String
|
||||
goalAfter: String
|
||||
tactic: String
|
||||
deriving Lean.ToJson
|
||||
structure CompileUnitResult where
|
||||
units?: Option $ List (Nat × Nat)
|
||||
invocations?: Option $ List InvokedTactic
|
||||
deriving Lean.ToJson
|
||||
|
||||
abbrev CR α := Except InteractionError α
|
||||
|
||||
|
|
|
@ -4,21 +4,17 @@ This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without
|
|||
using `Scope`s.
|
||||
-/
|
||||
import Lean
|
||||
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Condensed
|
||||
import Pantograph.Expr
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Protocol
|
||||
|
||||
open Lean
|
||||
|
||||
-- Symbol processing functions --
|
||||
|
||||
def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
|
||||
def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
|
||||
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
|
||||
|
||||
--- Input Functions ---
|
||||
|
||||
|
@ -86,6 +82,7 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
|
|||
| _, .zero => s!"{k}"
|
||||
| _, _ => s!"(+ {u_str} {k})"
|
||||
|
||||
|
||||
/--
|
||||
Completely serializes an expression tree. Json not used due to compactness
|
||||
|
||||
|
@ -94,7 +91,28 @@ A `_` symbol in the AST indicates automatic deductions not present in the origin
|
|||
partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
|
||||
self expr
|
||||
where
|
||||
self (e: Expr): MetaM String :=
|
||||
delayedMVarToSexp (e: Expr): MetaM (Option String) := do
|
||||
let .some invocation ← toDelayedMVarInvocation e | return .none
|
||||
let callee ← self $ .mvar invocation.mvarIdPending
|
||||
let sites ← invocation.args.mapM (λ (fvarId, arg) => do
|
||||
let arg := match arg with
|
||||
| .some arg => arg
|
||||
| .none => .fvar fvarId
|
||||
self arg
|
||||
)
|
||||
let tailArgs ← invocation.tail.mapM self
|
||||
|
||||
let sites := " ".intercalate sites.toList
|
||||
let result := if tailArgs.isEmpty then
|
||||
s!"(:subst {callee} {sites})"
|
||||
else
|
||||
let tailArgs := " ".intercalate tailArgs.toList
|
||||
s!"((:subst {callee} {sites}) {tailArgs})"
|
||||
return .some result
|
||||
|
||||
self (e: Expr): MetaM String := do
|
||||
if let .some result ← delayedMVarToSexp e then
|
||||
return result
|
||||
match e with
|
||||
| .bvar deBruijnIndex =>
|
||||
-- This is very common so the index alone is shown. Literals are handled below.
|
||||
|
@ -104,9 +122,10 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
|
|||
| .fvar fvarId =>
|
||||
let name := ofName fvarId.name
|
||||
pure s!"(:fv {name})"
|
||||
| .mvar mvarId =>
|
||||
let name := ofName mvarId.name
|
||||
pure s!"(:mv {name})"
|
||||
| .mvar mvarId => do
|
||||
let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
|
||||
let name := ofName mvarId.name
|
||||
pure s!"(:{pref} {name})"
|
||||
| .sort level =>
|
||||
let level := serializeSortLevel level sanitize
|
||||
pure s!"(:sort {level})"
|
||||
|
@ -149,15 +168,12 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
|
|||
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
|
||||
-- It may become necessary to incorporate the metadata.
|
||||
self inner
|
||||
| .proj typeName idx inner => do
|
||||
| .proj _ _ _ => do
|
||||
let env ← getEnv
|
||||
let ctor := getStructureCtor env typeName
|
||||
let fieldName := getStructureFields env typeName |>.get! idx
|
||||
let projectorName := getProjFnForField? env typeName fieldName |>.get!
|
||||
|
||||
let autos := String.intercalate " " (List.replicate ctor.numParams "_")
|
||||
let inner ← self inner
|
||||
pure s!"((:c {projectorName}) {autos} {inner})"
|
||||
let projApp := exprProjToApp env e
|
||||
let autos := String.intercalate " " (List.replicate projApp.numParams "_")
|
||||
let inner ← self projApp.inner
|
||||
pure s!"((:c {projApp.projector}) {autos} {inner})"
|
||||
-- Elides all unhygenic names
|
||||
binderInfoSexp : Lean.BinderInfo → String
|
||||
| .default => ""
|
||||
|
@ -182,8 +198,9 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
|
|||
dependentMVars?,
|
||||
}
|
||||
|
||||
|
||||
/-- Adapted from ppGoal -/
|
||||
def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
|
||||
def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
|
||||
: MetaM Protocol.Goal := do
|
||||
-- Options for printing; See Meta.ppGoal for details
|
||||
let showLetValues := true
|
||||
|
@ -195,39 +212,40 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
|
|||
let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName _ _ _ =>
|
||||
let userName := userName.simpMacroScopes
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName.simpMacroScopes,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
}
|
||||
| .ldecl _ fvarId userName _ _ _ _ => do
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName := toString userName.simpMacroScopes,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
}
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName type _ _ =>
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiateMVars type
|
||||
let type ← instantiate type
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName,
|
||||
isInaccessible? := .some userName.isInaccessibleUserName
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
type? := .some (← serializeExpression options type)
|
||||
}
|
||||
| .ldecl _ fvarId userName type val _ _ => do
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiateMVars type
|
||||
let type ← instantiate type
|
||||
let value? ← if showLetValues then
|
||||
let val ← instantiateMVars val
|
||||
let val ← instantiate val
|
||||
pure $ .some (← serializeExpression options val)
|
||||
else
|
||||
pure $ .none
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName,
|
||||
isInaccessible? := .some userName.isInaccessibleUserName
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
type? := .some (← serializeExpression options type)
|
||||
value? := value?
|
||||
}
|
||||
|
@ -247,10 +265,11 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
|
|||
name := ofName goal.name,
|
||||
userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
|
||||
isConversion := isLHSGoal? mvarDecl.type |>.isSome,
|
||||
target := (← serializeExpression options (← instantiateMVars mvarDecl.type)),
|
||||
target := (← serializeExpression options (← instantiate mvarDecl.type)),
|
||||
vars := vars.reverse.toArray
|
||||
}
|
||||
where
|
||||
instantiate := instantiateAll
|
||||
ofName (n: Name) := serializeName n (sanitize := false)
|
||||
|
||||
protected def GoalState.serializeGoals
|
||||
|
@ -269,53 +288,68 @@ protected def GoalState.serializeGoals
|
|||
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
|
||||
|
||||
/-- Print the metavariables in a readable format -/
|
||||
protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
|
||||
goalState.restoreMetaM
|
||||
let savedState := goalState.savedState
|
||||
let goals := savedState.tactic.goals
|
||||
let mctx ← getMCtx
|
||||
let root := goalState.root
|
||||
-- Print the root
|
||||
match mctx.decls.find? root with
|
||||
| .some decl => printMVar ">" root decl
|
||||
| .none => IO.println s!">{root.name}: ??"
|
||||
goals.forM (fun mvarId => do
|
||||
if mvarId != root then
|
||||
@[export pantograph_goal_state_diag_m]
|
||||
protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do
|
||||
let metaM: MetaM String := do
|
||||
goalState.restoreMetaM
|
||||
let savedState := goalState.savedState
|
||||
let goals := savedState.tactic.goals
|
||||
let mctx ← getMCtx
|
||||
let root := goalState.root
|
||||
-- Print the root
|
||||
let result: String ← match mctx.decls.find? root with
|
||||
| .some decl => printMVar ">" root decl
|
||||
| .none => pure s!">{root.name}: ??"
|
||||
let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
|
||||
match mctx.decls.find? mvarId with
|
||||
| .some decl => printMVar "⊢" mvarId decl
|
||||
| .none => IO.println s!"⊢{mvarId.name}: ??"
|
||||
)
|
||||
let goals := goals.toSSet
|
||||
mctx.decls.forM (fun mvarId decl => do
|
||||
if goals.contains mvarId || mvarId == root then
|
||||
pure ()
|
||||
-- Print the remainig ones that users don't see in Lean
|
||||
else if options.printAll then
|
||||
let pref := if goalState.newMVars.contains mvarId then "~" else " "
|
||||
printMVar pref mvarId decl
|
||||
else
|
||||
pure ()
|
||||
--IO.println s!" {mvarId.name}{userNameToString decl.userName}"
|
||||
)
|
||||
| .none => pure s!"⊢{mvarId.name}: ??"
|
||||
)
|
||||
let goals := goals.toSSet
|
||||
let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
|
||||
!(goals.contains mvarId || mvarId == root) && options.printAll)
|
||||
|>.mapM (fun (mvarId, decl) => do
|
||||
let pref := if parentHasMVar mvarId then " " else "~"
|
||||
printMVar pref mvarId decl
|
||||
)
|
||||
pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
|
||||
metaM.run' {}
|
||||
where
|
||||
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
|
||||
if options.printContext then
|
||||
decl.lctx.fvarIdToDecl.forM printFVar
|
||||
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
|
||||
let resultFVars: List String ←
|
||||
if options.printContext then
|
||||
decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) =>
|
||||
do pure $ (← printFVar fvarId decl) ++ "\n")
|
||||
else
|
||||
pure []
|
||||
let type ← if options.instantiate
|
||||
then instantiateMVars decl.type
|
||||
then instantiateAll decl.type
|
||||
else pure $ decl.type
|
||||
let type_sexp ← serializeExpressionSexp type (sanitize := false)
|
||||
IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
|
||||
if options.printValue then
|
||||
if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
|
||||
let value ← if options.instantiate
|
||||
then instantiateMVars value
|
||||
else pure $ value
|
||||
IO.println s!" := {← Meta.ppExpr value}"
|
||||
printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do
|
||||
IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
|
||||
let type_sexp ← if options.printSexp then
|
||||
let sexp ← serializeExpressionSexp type (sanitize := false)
|
||||
pure <| " " ++ sexp
|
||||
else
|
||||
pure ""
|
||||
let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}"
|
||||
let resultValue: String ←
|
||||
if options.printValue then
|
||||
if let .some value ← getExprMVarAssignment? mvarId then
|
||||
let value ← if options.instantiate
|
||||
then instantiateAll value
|
||||
else pure $ value
|
||||
pure s!"\n := {← Meta.ppExpr value}"
|
||||
else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
|
||||
pure s!"\n ::= {mvarIdPending.name}"
|
||||
else
|
||||
pure ""
|
||||
else
|
||||
pure ""
|
||||
pure $ (String.join resultFVars) ++ resultMain ++ resultValue
|
||||
printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM String := do
|
||||
pure s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
|
||||
userNameToString : Name → String
|
||||
| .anonymous => ""
|
||||
| other => s!"[{other}]"
|
||||
parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -0,0 +1,5 @@
|
|||
import Pantograph.Tactic.Assign
|
||||
import Pantograph.Tactic.Congruence
|
||||
import Pantograph.Tactic.MotivatedApply
|
||||
import Pantograph.Tactic.NoConfuse
|
||||
import Pantograph.Tactic.Prograde
|
|
@ -0,0 +1,31 @@
|
|||
import Lean
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph.Tactic
|
||||
|
||||
/-- WARNING: This should be used with a function like `elabTermWithHoles` that properly collects the mvar information from `expr`. -/
|
||||
def assign (goal: MVarId) (expr: Expr) (nextGoals: List MVarId): MetaM (List MVarId) := do
|
||||
goal.checkNotAssigned `Pantograph.Tactic.assign
|
||||
|
||||
-- This run of the unifier is critical in resolving mvars in passing
|
||||
let exprType ← Meta.inferType expr
|
||||
let goalType ← goal.getType
|
||||
unless ← Meta.isDefEq goalType exprType do
|
||||
throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}"
|
||||
goal.assign expr
|
||||
nextGoals.filterM (not <$> ·.isAssigned)
|
||||
|
||||
def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
|
||||
let target ← Elab.Tactic.getMainTarget
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
goal.checkNotAssigned `Pantograph.Tactic.evalAssign
|
||||
let (expr, nextGoals) ← Elab.Tactic.elabTermWithHoles stx
|
||||
(expectedType? := .some target)
|
||||
(tagSuffix := .anonymous )
|
||||
(allowNaturalHoles := true)
|
||||
goal.assign expr
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
|
||||
end Pantograph.Tactic
|
|
@ -0,0 +1,98 @@
|
|||
import Lean
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph.Tactic
|
||||
|
||||
def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.congruenceArg
|
||||
let target ← mvarId.getType
|
||||
let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
|
||||
let userName := (← mvarId.getDecl).userName
|
||||
|
||||
let u ← Meta.mkFreshLevelMVar
|
||||
let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
|
||||
.natural (userName := userName ++ `α)
|
||||
let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous α β .default)
|
||||
.synthetic (userName := userName ++ `f)
|
||||
let a₁ ← Meta.mkFreshExprMVar (.some α)
|
||||
.synthetic (userName := userName ++ `a₁)
|
||||
let a₂ ← Meta.mkFreshExprMVar (.some α)
|
||||
.synthetic (userName := userName ++ `a₂)
|
||||
let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂)
|
||||
.synthetic (userName := userName ++ `h)
|
||||
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) target
|
||||
let conduit ← Meta.mkFreshExprMVar conduitType
|
||||
.synthetic (userName := userName ++ `conduit)
|
||||
mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
|
||||
let result := [α, a₁, a₂, f, h, conduit]
|
||||
return result.map (·.mvarId!)
|
||||
|
||||
def evalCongruenceArg: Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let nextGoals ← congruenceArg goal
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun
|
||||
let target ← mvarId.getType
|
||||
let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
|
||||
let userName := (← mvarId.getDecl).userName
|
||||
let u ← Meta.mkFreshLevelMVar
|
||||
let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
|
||||
.natural (userName := userName ++ `α)
|
||||
let fType := .forallE .anonymous α β .default
|
||||
let f₁ ← Meta.mkFreshExprMVar (.some fType)
|
||||
.synthetic (userName := userName ++ `f₁)
|
||||
let f₂ ← Meta.mkFreshExprMVar (.some fType)
|
||||
.synthetic (userName := userName ++ `f₂)
|
||||
let a ← Meta.mkFreshExprMVar (.some α)
|
||||
.synthetic (userName := userName ++ `a)
|
||||
let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
|
||||
.synthetic (userName := userName ++ `h)
|
||||
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target
|
||||
let conduit ← Meta.mkFreshExprMVar conduitType
|
||||
.synthetic (userName := userName ++ `conduit)
|
||||
mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
|
||||
let result := [α, f₁, f₂, h, a, conduit]
|
||||
return result.map (·.mvarId!)
|
||||
|
||||
def evalCongruenceFun: Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let nextGoals ← congruenceFun goal
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.congruence
|
||||
let target ← mvarId.getType
|
||||
let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
|
||||
let userName := (← mvarId.getDecl).userName
|
||||
let u ← Meta.mkFreshLevelMVar
|
||||
let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
|
||||
.natural (userName := userName ++ `α)
|
||||
let fType := .forallE .anonymous α β .default
|
||||
let f₁ ← Meta.mkFreshExprMVar (.some fType)
|
||||
.synthetic (userName := userName ++ `f₁)
|
||||
let f₂ ← Meta.mkFreshExprMVar (.some fType)
|
||||
.synthetic (userName := userName ++ `f₂)
|
||||
let a₁ ← Meta.mkFreshExprMVar (.some α)
|
||||
.synthetic (userName := userName ++ `a₁)
|
||||
let a₂ ← Meta.mkFreshExprMVar (.some α)
|
||||
.synthetic (userName := userName ++ `a₂)
|
||||
let h₁ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
|
||||
.synthetic (userName := userName ++ `h₁)
|
||||
let h₂ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂)
|
||||
.synthetic (userName := userName ++ `h₂)
|
||||
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) target
|
||||
let conduit ← Meta.mkFreshExprMVar conduitType
|
||||
.synthetic (userName := userName ++ `conduit)
|
||||
mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
|
||||
let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
|
||||
return result.map (·.mvarId!)
|
||||
|
||||
def evalCongruence: Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let nextGoals ← congruence goal
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
end Pantograph.Tactic
|
|
@ -0,0 +1,105 @@
|
|||
import Lean
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph.Tactic
|
||||
|
||||
def getForallArgsBody: Expr → List Expr × Expr
|
||||
| .forallE _ d b _ =>
|
||||
let (innerArgs, innerBody) := getForallArgsBody b
|
||||
(d :: innerArgs, innerBody)
|
||||
| e => ([], e)
|
||||
|
||||
def replaceForallBody: Expr → Expr → Expr
|
||||
| .forallE param domain body binderInfo, target =>
|
||||
let body := replaceForallBody body target
|
||||
.forallE param domain body binderInfo
|
||||
| _, target => target
|
||||
|
||||
structure RecursorWithMotive where
|
||||
args: List Expr
|
||||
body: Expr
|
||||
|
||||
-- .bvar index for the motive and major from the body
|
||||
iMotive: Nat
|
||||
|
||||
namespace RecursorWithMotive
|
||||
|
||||
protected def nArgs (info: RecursorWithMotive): Nat := info.args.length
|
||||
|
||||
protected def getMotiveType (info: RecursorWithMotive): Expr :=
|
||||
let level := info.nArgs - info.iMotive - 1
|
||||
let a := info.args.get! level
|
||||
a
|
||||
|
||||
protected def surrogateMotiveType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
|
||||
let motiveType := Expr.instantiateRev info.getMotiveType mvars
|
||||
let resultantType ← Meta.inferType resultant
|
||||
return replaceForallBody motiveType resultantType
|
||||
|
||||
protected def conduitType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
|
||||
let motiveCall := Expr.instantiateRev info.body mvars
|
||||
Meta.mkEq motiveCall resultant
|
||||
|
||||
end RecursorWithMotive
|
||||
|
||||
def getRecursorInformation (recursorType: Expr): Option RecursorWithMotive := do
|
||||
let (args, body) := getForallArgsBody recursorType
|
||||
if ¬ body.isApp then
|
||||
.none
|
||||
let iMotive ← match body.getAppFn with
|
||||
| .bvar iMotive => pure iMotive
|
||||
| _ => .none
|
||||
return {
|
||||
args,
|
||||
body,
|
||||
iMotive,
|
||||
}
|
||||
|
||||
def collectMotiveArguments (forallBody: Expr): SSet Nat :=
|
||||
match forallBody with
|
||||
| .app (.bvar i) _ => SSet.empty.insert i
|
||||
| _ => SSet.empty
|
||||
|
||||
/-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/
|
||||
def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.InductionSubgoal) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply
|
||||
let recursorType ← Meta.inferType recursor
|
||||
let resultant ← mvarId.getType
|
||||
|
||||
let info ← match getRecursorInformation recursorType with
|
||||
| .some info => pure info
|
||||
| .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}"
|
||||
|
||||
let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do
|
||||
if i ≥ info.nArgs then
|
||||
return prev
|
||||
else
|
||||
let argType := info.args.get! i
|
||||
-- If `argType` has motive references, its goal needs to be placed in it
|
||||
let argType := argType.instantiateRev prev
|
||||
let bvarIndex := info.nArgs - i - 1
|
||||
let argGoal ← if bvarIndex = info.iMotive then
|
||||
let surrogateMotiveType ← info.surrogateMotiveType prev resultant
|
||||
Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive)
|
||||
else
|
||||
Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous)
|
||||
let prev := prev ++ [argGoal]
|
||||
go (i + 1) prev
|
||||
termination_by info.nArgs - i
|
||||
let mut newMVars ← go 0 #[]
|
||||
|
||||
-- Create the conduit type which proves the result of the motive is equal to the goal
|
||||
let conduitType ← info.conduitType newMVars resultant
|
||||
let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit)
|
||||
mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
|
||||
newMVars := newMVars ++ [goalConduit]
|
||||
|
||||
return newMVars.map (λ mvar => { mvarId := mvar.mvarId!})
|
||||
|
||||
def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
|
||||
let recursor ← Elab.Term.elabTerm (stx := stx) .none
|
||||
let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
|
||||
Elab.Tactic.replaceMainGoal $ nextGoals.toList.map (·.mvarId)
|
||||
|
||||
end Pantograph.Tactic
|
|
@ -0,0 +1,22 @@
|
|||
import Lean
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph.Tactic
|
||||
|
||||
def noConfuse (mvarId: MVarId) (h: Expr): MetaM Unit := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.noConfuse
|
||||
let target ← mvarId.getType
|
||||
let noConfusion ← Meta.mkNoConfusion (target := target) (h := h)
|
||||
|
||||
unless ← Meta.isDefEq (← Meta.inferType noConfusion) target do
|
||||
throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr target}"
|
||||
mvarId.assign noConfusion
|
||||
|
||||
def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none
|
||||
noConfuse goal h
|
||||
Elab.Tactic.replaceMainGoal []
|
||||
|
||||
end Pantograph.Tactic
|
|
@ -0,0 +1,88 @@
|
|||
/- Prograde (forward) reasoning tactics -/
|
||||
|
||||
import Lean
|
||||
open Lean
|
||||
|
||||
namespace Pantograph.Tactic
|
||||
|
||||
private def mkUpstreamMVar (goal: MVarId) : MetaM Expr := do
|
||||
Meta.mkFreshExprSyntheticOpaqueMVar (← goal.getType) (tag := ← goal.getTag)
|
||||
|
||||
|
||||
/-- Introduces a fvar to the current mvar -/
|
||||
def define (mvarId: MVarId) (binderName: Name) (expr: Expr): MetaM (FVarId × MVarId) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.define
|
||||
let type ← Meta.inferType expr
|
||||
|
||||
Meta.withLetDecl binderName type expr λ fvar => do
|
||||
let mvarUpstream ← mkUpstreamMVar mvarId
|
||||
mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
|
||||
pure (fvar.fvarId!, mvarUpstream.mvarId!)
|
||||
|
||||
def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let expr ← goal.withContext $ Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
|
||||
let (_, mvarId) ← define goal binderName expr
|
||||
Elab.Tactic.replaceMainGoal [mvarId]
|
||||
|
||||
structure BranchResult where
|
||||
fvarId?: Option FVarId := .none
|
||||
branch: MVarId
|
||||
main: MVarId
|
||||
|
||||
def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.have
|
||||
let lctx ← MonadLCtx.getLCtx
|
||||
-- The branch goal inherits the same context, but with a different type
|
||||
let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
|
||||
|
||||
-- Create the context for the `upstream` goal
|
||||
let fvarId ← mkFreshFVarId
|
||||
let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
|
||||
let mvarUpstream ←
|
||||
withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
|
||||
Meta.withNewLocalInstances #[.fvar fvarId] 0 do
|
||||
let mvarUpstream ← mkUpstreamMVar mvarId
|
||||
--let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
|
||||
mvarId.assign $ ← Meta.mkLambdaFVars #[.fvar fvarId] mvarUpstream
|
||||
pure mvarUpstream
|
||||
|
||||
return {
|
||||
fvarId? := .some fvarId,
|
||||
branch := mvarBranch.mvarId!,
|
||||
main := mvarUpstream.mvarId!,
|
||||
}
|
||||
|
||||
def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let nextGoals: List MVarId ← goal.withContext do
|
||||
let type ← Elab.Term.elabType (stx := type)
|
||||
let result ← «have» goal binderName type
|
||||
pure [result.branch, result.main]
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.let
|
||||
let lctx ← MonadLCtx.getLCtx
|
||||
|
||||
-- The branch goal inherits the same context, but with a different type
|
||||
let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type (userName := binderName)
|
||||
|
||||
assert! ¬ type.hasLooseBVars
|
||||
let mvarUpstream ← Meta.withLetDecl binderName type mvarBranch $ λ fvar => do
|
||||
let mvarUpstream ← mkUpstreamMVar mvarId
|
||||
mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
|
||||
pure mvarUpstream
|
||||
|
||||
return {
|
||||
branch := mvarBranch.mvarId!,
|
||||
main := mvarUpstream.mvarId!,
|
||||
}
|
||||
|
||||
def evalLet (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let type ← goal.withContext $ Elab.Term.elabType (stx := type)
|
||||
let result ← «let» goal binderName type
|
||||
Elab.Tactic.replaceMainGoal [result.branch, result.main]
|
||||
|
||||
end Pantograph.Tactic
|
|
@ -1,6 +1,6 @@
|
|||
namespace Pantograph
|
||||
|
||||
@[export pantograph_version]
|
||||
def version := "0.2.15"
|
||||
def version := "0.2.18"
|
||||
|
||||
end Pantograph
|
||||
|
|
19
README.md
19
README.md
|
@ -11,9 +11,9 @@ examine the symbol list of a Lean project for machine learning.
|
|||
|
||||
For Nix based workflow, see below.
|
||||
|
||||
Install `elan` and `lake`. Execute
|
||||
Install `elan` and `lake`, and run
|
||||
``` sh
|
||||
make
|
||||
lake build
|
||||
```
|
||||
This builds the executable in `.lake/build/bin/pantograph`.
|
||||
|
||||
|
@ -90,6 +90,11 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
|
|||
only the values of definitions are printed.
|
||||
* `options.set { key: value, ... }`: Set one or more options (not Lean options; those
|
||||
have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
|
||||
|
||||
One particular option for interest for machine learning researchers is the
|
||||
automatic mode (flag: `"automaticMode"`). By default it is turned on, with
|
||||
all goals automatically resuming. This makes Pantograph act like a gym,
|
||||
with no resumption necessary to manage your goals.
|
||||
* `options.print`: Display the current set of options
|
||||
* `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
|
||||
Start a new proof from a given expression or symbol
|
||||
|
@ -138,6 +143,9 @@ ulimit -s unlimited
|
|||
with `Pantograph` which mirrors the REPL commands above. It is recommended to
|
||||
call Pantograph via this FFI since it provides a tremendous speed up.
|
||||
|
||||
Note that there isn't a 1-1 correspondence between executable (REPL) commands
|
||||
and library functions.
|
||||
|
||||
## Developing
|
||||
|
||||
A Lean development shell is provided in the Nix flake.
|
||||
|
@ -146,7 +154,12 @@ A Lean development shell is provided in the Nix flake.
|
|||
|
||||
The tests are based on `LSpec`. To run tests,
|
||||
``` sh
|
||||
make test
|
||||
lake test
|
||||
```
|
||||
You can run an individual test by specifying a prefix
|
||||
|
||||
``` sh
|
||||
lake test -- "Tactic/No Confuse"
|
||||
```
|
||||
|
||||
## Nix based workflow
|
||||
|
|
|
@ -0,0 +1,220 @@
|
|||
import Lean.Data.HashMap
|
||||
import Pantograph
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
structure Context where
|
||||
imports: List String
|
||||
|
||||
/-- Stores state of the REPL -/
|
||||
structure State where
|
||||
options: Protocol.Options := {}
|
||||
nextId: Nat := 0
|
||||
goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
|
||||
|
||||
/-- Main state monad for executing commands -/
|
||||
abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
|
||||
|
||||
-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
|
||||
-- certain monadic features in `MainM`
|
||||
abbrev CR α := Except Protocol.InteractionError α
|
||||
|
||||
def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
|
||||
metaM.run'
|
||||
def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=
|
||||
termElabM.run' (ctx := Condensed.elabContext) |>.run'
|
||||
|
||||
def execute (command: Protocol.Command): MainM Lean.Json := do
|
||||
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
|
||||
match Lean.fromJson? command.payload with
|
||||
| .ok args => do
|
||||
match (← comm args) with
|
||||
| .ok result => return Lean.toJson result
|
||||
| .error ierror => return Lean.toJson ierror
|
||||
| .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
|
||||
match command.cmd with
|
||||
| "reset" => run reset
|
||||
| "stat" => run stat
|
||||
| "expr.echo" => run expr_echo
|
||||
| "env.catalog" => run env_catalog
|
||||
| "env.inspect" => run env_inspect
|
||||
| "env.add" => run env_add
|
||||
| "options.set" => run options_set
|
||||
| "options.print" => run options_print
|
||||
| "goal.start" => run goal_start
|
||||
| "goal.tactic" => run goal_tactic
|
||||
| "goal.continue" => run goal_continue
|
||||
| "goal.delete" => run goal_delete
|
||||
| "goal.print" => run goal_print
|
||||
| "compile.unit" => run compile_unit
|
||||
| cmd =>
|
||||
let error: Protocol.InteractionError :=
|
||||
errorCommand s!"Unknown command {cmd}"
|
||||
return Lean.toJson error
|
||||
where
|
||||
errorCommand := errorI "command"
|
||||
errorIndex := errorI "index"
|
||||
-- Command Functions
|
||||
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
|
||||
let state ← get
|
||||
let nGoals := state.goalStates.size
|
||||
set { state with nextId := 0, goalStates := Lean.HashMap.empty }
|
||||
return .ok { nGoals }
|
||||
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
|
||||
let state ← get
|
||||
let nGoals := state.goalStates.size
|
||||
return .ok { nGoals }
|
||||
env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
|
||||
let result ← Environment.catalog args
|
||||
return .ok result
|
||||
env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
|
||||
let state ← get
|
||||
Environment.inspect args state.options
|
||||
env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
|
||||
Environment.addDecl args
|
||||
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
|
||||
let state ← get
|
||||
exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
|
||||
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
|
||||
let state ← get
|
||||
let options := state.options
|
||||
set { state with
|
||||
options := {
|
||||
-- FIXME: This should be replaced with something more elegant
|
||||
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
|
||||
printExprPretty := args.printExprPretty?.getD options.printExprPretty,
|
||||
printExprAST := args.printExprAST?.getD options.printExprAST,
|
||||
printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars,
|
||||
noRepeat := args.noRepeat?.getD options.noRepeat,
|
||||
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
|
||||
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
|
||||
automaticMode := args.automaticMode?.getD options.automaticMode,
|
||||
}
|
||||
}
|
||||
return .ok { }
|
||||
options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
|
||||
return .ok (← get).options
|
||||
goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
|
||||
let state ← get
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
|
||||
| .some expr, .none => goalStartExpr expr (args.levels.getD #[])
|
||||
| .none, .some copyFrom =>
|
||||
(match env.find? <| copyFrom.toName with
|
||||
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
|
||||
| .some cInfo => return .ok (← GoalState.create cInfo.type))
|
||||
| _, _ =>
|
||||
return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
|
||||
match expr? with
|
||||
| .error error => return .error error
|
||||
| .ok goalState =>
|
||||
let stateId := state.nextId
|
||||
set { state with
|
||||
goalStates := state.goalStates.insert stateId goalState,
|
||||
nextId := state.nextId + 1
|
||||
}
|
||||
return .ok { stateId, root := goalState.root.name.toString }
|
||||
goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
|
||||
let state ← get
|
||||
let .some goalState := state.goalStates.find? args.stateId |
|
||||
return .error $ errorIndex s!"Invalid state index {args.stateId}"
|
||||
let .some goal := goalState.goals.get? args.goalId |
|
||||
return .error $ errorIndex s!"Invalid goal index {args.goalId}"
|
||||
let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do
|
||||
match args.tactic?, args.expr?, args.have?, args.calc?, args.conv? with
|
||||
| .some tactic, .none, .none, .none, .none => do
|
||||
pure <| Except.ok <| ← goalState.tryTactic goal tactic
|
||||
| .none, .some expr, .none, .none, .none => do
|
||||
pure <| Except.ok <| ← goalState.tryAssign goal expr
|
||||
| .none, .none, .some type, .none, .none => do
|
||||
let binderName := args.binderName?.getD ""
|
||||
pure <| Except.ok <| ← goalState.tryHave goal binderName type
|
||||
| .none, .none, .none, .some pred, .none => do
|
||||
pure <| Except.ok <| ← goalState.tryCalc goal pred
|
||||
| .none, .none, .none, .none, .some true => do
|
||||
pure <| Except.ok <| ← goalState.conv goal
|
||||
| .none, .none, .none, .none, .some false => do
|
||||
pure <| Except.ok <| ← goalState.convExit
|
||||
| _, _, _, _, _ =>
|
||||
let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied"
|
||||
pure $ Except.error $ error
|
||||
match nextGoalState? with
|
||||
| .error error => return .error error
|
||||
| .ok (.success nextGoalState) => do
|
||||
let nextGoalState ← match state.options.automaticMode, args.conv? with
|
||||
| true, .none => do
|
||||
let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) | throwError "Resuming known goals"
|
||||
pure result
|
||||
| true, .some true => pure nextGoalState
|
||||
| true, .some false => do
|
||||
let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail"
|
||||
let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) | throwError "Resuming known goals"
|
||||
pure result
|
||||
| false, _ => pure nextGoalState
|
||||
let nextStateId := state.nextId
|
||||
set { state with
|
||||
goalStates := state.goalStates.insert state.nextId nextGoalState,
|
||||
nextId := state.nextId + 1,
|
||||
}
|
||||
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
|
||||
return .ok {
|
||||
nextStateId? := .some nextStateId,
|
||||
goals? := .some goals,
|
||||
}
|
||||
| .ok (.parseError message) =>
|
||||
return .ok { parseError? := .some message }
|
||||
| .ok (.invalidAction message) =>
|
||||
return .error $ errorI "invalid" message
|
||||
| .ok (.failure messages) =>
|
||||
return .ok { tacticErrors? := .some messages }
|
||||
goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
|
||||
let state ← get
|
||||
let .some target := state.goalStates.find? args.target | return .error $ errorIndex s!"Invalid state index {args.target}"
|
||||
let nextState? ← match args.branch?, args.goals? with
|
||||
| .some branchId, .none => do
|
||||
match state.goalStates.find? branchId with
|
||||
| .none => return .error $ errorIndex s!"Invalid state index {branchId}"
|
||||
| .some branch => pure $ target.continue branch
|
||||
| .none, .some goals =>
|
||||
pure $ goalResume target goals
|
||||
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
|
||||
match nextState? with
|
||||
| .error error => return .error <| errorI "structure" error
|
||||
| .ok nextGoalState =>
|
||||
let nextStateId := state.nextId
|
||||
set { state with
|
||||
goalStates := state.goalStates.insert nextStateId nextGoalState,
|
||||
nextId := state.nextId + 1
|
||||
}
|
||||
let goals ← goalSerialize nextGoalState (options := state.options)
|
||||
return .ok {
|
||||
nextStateId,
|
||||
goals,
|
||||
}
|
||||
goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
|
||||
let state ← get
|
||||
let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates
|
||||
set { state with goalStates }
|
||||
return .ok {}
|
||||
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
|
||||
let state ← get
|
||||
let .some goalState := state.goalStates.find? args.stateId | return .error $ errorIndex s!"Invalid state index {args.stateId}"
|
||||
let result ← runMetaInMainM <| goalPrint goalState state.options
|
||||
return .ok result
|
||||
compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do
|
||||
let module := args.module.toName
|
||||
try
|
||||
let steps ← Compile.processSource module
|
||||
let units? := if args.compilationUnits then
|
||||
.some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
|
||||
else
|
||||
.none
|
||||
let invocations? ← if args.invocations then
|
||||
pure $ .some (← Compile.collectTacticsFromCompilation steps)
|
||||
else
|
||||
pure .none
|
||||
return .ok { units?, invocations? }
|
||||
catch e =>
|
||||
return .error $ errorI "compile" (← e.toMessageData.toString)
|
||||
|
||||
end Pantograph
|
102
Test/Common.lean
102
Test/Common.lean
|
@ -1,6 +1,7 @@
|
|||
import Pantograph.Goal
|
||||
import Pantograph.Library
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Condensed
|
||||
import Lean
|
||||
import LSpec
|
||||
|
||||
|
@ -8,20 +9,33 @@ open Lean
|
|||
|
||||
namespace Pantograph
|
||||
|
||||
deriving instance Repr for Expr
|
||||
-- Use strict equality check for expressions
|
||||
instance : BEq Expr := ⟨Expr.equal⟩
|
||||
|
||||
def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n
|
||||
|
||||
-- Auxiliary functions
|
||||
namespace Protocol
|
||||
/-- Set internal names to "" -/
|
||||
def Goal.devolatilize (goal: Goal): Goal :=
|
||||
def Goal.devolatilizeVars (goal: Goal): Goal :=
|
||||
{
|
||||
goal with
|
||||
name := "",
|
||||
vars := goal.vars.map removeInternalAux,
|
||||
|
||||
}
|
||||
where removeInternalAux (v: Variable): Variable :=
|
||||
{
|
||||
v with
|
||||
name := ""
|
||||
}
|
||||
/-- Set internal names to "" -/
|
||||
def Goal.devolatilize (goal: Goal): Goal :=
|
||||
{
|
||||
goal.devolatilizeVars with
|
||||
name := "",
|
||||
}
|
||||
|
||||
deriving instance DecidableEq, Repr for Name
|
||||
deriving instance DecidableEq, Repr for Expression
|
||||
deriving instance DecidableEq, Repr for Variable
|
||||
deriving instance DecidableEq, Repr for Goal
|
||||
|
@ -30,13 +44,33 @@ deriving instance DecidableEq, Repr for InteractionError
|
|||
deriving instance DecidableEq, Repr for Option
|
||||
end Protocol
|
||||
|
||||
namespace Condensed
|
||||
|
||||
deriving instance BEq, Repr for LocalDecl
|
||||
deriving instance BEq, Repr for Goal
|
||||
|
||||
protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl :=
|
||||
{
|
||||
decl with fvarId := { name := .anonymous }
|
||||
}
|
||||
protected def Goal.devolatilize (goal: Goal): Goal :=
|
||||
{
|
||||
goal with
|
||||
mvarId := { name := .anonymous },
|
||||
context := goal.context.map LocalDecl.devolatilize
|
||||
}
|
||||
|
||||
end Condensed
|
||||
|
||||
def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals.get! i
|
||||
def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.goals.get! goalId) tactic
|
||||
|
||||
def TacticResult.toString : TacticResult → String
|
||||
| .success state => s!".success ({state.goals.length} goals)"
|
||||
| .failure messages =>
|
||||
let messages := "\n".intercalate messages.toList
|
||||
s!".failure {messages}"
|
||||
| .parseError error => s!".parseError {error}"
|
||||
| .indexError index => s!".indexError {index}"
|
||||
| .invalidAction error => s!".invalidAction {error}"
|
||||
|
||||
namespace Test
|
||||
|
@ -56,7 +90,65 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
|
|||
def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
|
||||
runCoreMSeq env metaM.run'
|
||||
def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
|
||||
termElabM.run' (ctx := Pantograph.defaultTermElabMContext)
|
||||
termElabM.run' (ctx := Condensed.elabContext)
|
||||
def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
|
||||
runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
|
||||
|
||||
def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
|
||||
|
||||
def strToTermSyntax [Monad m] [MonadEnv m] (s: String): m Syntax := do
|
||||
let .ok stx := Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := filename) | panic! s!"Failed to parse {s}"
|
||||
return stx
|
||||
def parseSentence (s: String): Elab.TermElabM Expr := do
|
||||
let stx ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
Elab.Term.elabTerm (stx := stx) .none
|
||||
|
||||
def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
|
||||
let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
|
||||
return newGoals.goals
|
||||
def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do
|
||||
let name := (← mvarId.getDecl).userName
|
||||
let t ← exprToStr (← mvarId.getType)
|
||||
return (name, t)
|
||||
|
||||
|
||||
-- Monadic testing
|
||||
|
||||
abbrev TestT := StateT LSpec.TestSeq
|
||||
|
||||
def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do
|
||||
set $ (← get) ++ test
|
||||
|
||||
def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq :=
|
||||
Prod.snd <$> t.run LSpec.TestSeq.done
|
||||
|
||||
def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit):
|
||||
IO LSpec.TestSeq :=
|
||||
runTermElabMSeq env $ runTest t
|
||||
|
||||
def cdeclOf (userName: Name) (type: Expr): Condensed.LocalDecl :=
|
||||
{ userName, type }
|
||||
|
||||
def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
|
||||
Protocol.Goal :=
|
||||
{
|
||||
userName?,
|
||||
target := { pp? := .some target},
|
||||
vars := (nameType.map fun x => ({
|
||||
userName := x.fst,
|
||||
type? := .some { pp? := .some x.snd },
|
||||
})).toArray
|
||||
}
|
||||
|
||||
end Test
|
||||
|
||||
|
|
|
@ -2,39 +2,24 @@
|
|||
-/
|
||||
import LSpec
|
||||
import Pantograph
|
||||
import Repl
|
||||
import Test.Common
|
||||
|
||||
namespace Pantograph.Test.Integration
|
||||
open Pantograph
|
||||
|
||||
def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json))
|
||||
(expected: Lean.Json): MainM LSpec.TestSeq := do
|
||||
let result ← execute { cmd := cmd, payload := Lean.Json.mkObj payload }
|
||||
return LSpec.test name (toString result = toString expected)
|
||||
def subroutine_step (cmd: String) (payload: List (String × Lean.Json))
|
||||
(expected: Lean.Json): MainM LSpec.TestSeq := subroutine_named_step cmd cmd payload expected
|
||||
def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json))
|
||||
(expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do
|
||||
let payload := Lean.Json.mkObj payload
|
||||
let name := name?.getD s!"{cmd} {payload.compress}"
|
||||
let result ← execute { cmd, payload }
|
||||
return LSpec.test name (toString result = toString (Lean.toJson expected))
|
||||
|
||||
def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do
|
||||
-- Setup the environment for execution
|
||||
let env ← Lean.importModules
|
||||
(imports := #[{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }])
|
||||
(opts := {})
|
||||
(trustLevel := 1)
|
||||
let context: Context := {
|
||||
imports := ["Init"]
|
||||
}
|
||||
let coreContext: Lean.Core.Context ← createCoreContext #[]
|
||||
let commands: MainM LSpec.TestSeq :=
|
||||
steps.foldlM (λ suite step => do
|
||||
let result ← step
|
||||
return suite ++ result) LSpec.TestSeq.done
|
||||
try
|
||||
let coreM := commands.run context |>.run' {}
|
||||
return Prod.fst $ (← coreM.toIO coreContext { env := env })
|
||||
catch ex =>
|
||||
return LSpec.check s!"Uncaught IO exception: {ex.toString}" false
|
||||
abbrev Test := List (MainM LSpec.TestSeq)
|
||||
|
||||
def test_elab : IO LSpec.TestSeq :=
|
||||
subroutine_runner [
|
||||
subroutine_step "expr.echo"
|
||||
def test_elab : Test :=
|
||||
[
|
||||
step "expr.echo"
|
||||
[("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])]
|
||||
(Lean.toJson ({
|
||||
type := { pp? := .some "{α : Type u} → Type u" },
|
||||
|
@ -42,130 +27,163 @@ def test_elab : IO LSpec.TestSeq :=
|
|||
}: Protocol.ExprEchoResult)),
|
||||
]
|
||||
|
||||
def test_option_modify : IO LSpec.TestSeq :=
|
||||
def test_option_modify : Test :=
|
||||
let pp? := Option.some "∀ (n : Nat), n + 1 = n.succ"
|
||||
let sexp? := Option.some "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"
|
||||
let module? := Option.some "Init.Data.Nat.Basic"
|
||||
let options: Protocol.Options := {}
|
||||
subroutine_runner [
|
||||
subroutine_step "env.inspect"
|
||||
[("name", .str "Nat.add_one")]
|
||||
(Lean.toJson ({
|
||||
type := { pp? }, module? }:
|
||||
Protocol.EnvInspectResult)),
|
||||
subroutine_step "options.set"
|
||||
[("printExprAST", .bool true)]
|
||||
(Lean.toJson ({ }:
|
||||
Protocol.OptionsSetResult)),
|
||||
subroutine_step "env.inspect"
|
||||
[("name", .str "Nat.add_one")]
|
||||
(Lean.toJson ({
|
||||
type := { pp?, sexp? }, module? }:
|
||||
Protocol.EnvInspectResult)),
|
||||
subroutine_step "options.print"
|
||||
[]
|
||||
(Lean.toJson ({ options with printExprAST := true }:
|
||||
Protocol.OptionsPrintResult))
|
||||
[
|
||||
step "env.inspect" [("name", .str "Nat.add_one")]
|
||||
({ type := { pp? }, module? }: Protocol.EnvInspectResult),
|
||||
step "options.set" [("printExprAST", .bool true)]
|
||||
({ }: Protocol.OptionsSetResult),
|
||||
step "env.inspect" [("name", .str "Nat.add_one")]
|
||||
({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult),
|
||||
step "options.print" []
|
||||
({ options with printExprAST := true }: Protocol.Options),
|
||||
]
|
||||
def test_malformed_command : IO LSpec.TestSeq :=
|
||||
def test_malformed_command : Test :=
|
||||
let invalid := "invalid"
|
||||
subroutine_runner [
|
||||
subroutine_named_step "Invalid command" invalid
|
||||
[("name", .str "Nat.add_one")]
|
||||
(Lean.toJson ({
|
||||
error := "command", desc := s!"Unknown command {invalid}"}:
|
||||
Protocol.InteractionError)),
|
||||
subroutine_named_step "JSON Deserialization" "expr.echo"
|
||||
[(invalid, .str "Random garbage data")]
|
||||
(Lean.toJson ({
|
||||
error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}:
|
||||
Protocol.InteractionError))
|
||||
[
|
||||
step invalid [("name", .str "Nat.add_one")]
|
||||
({ error := "command", desc := s!"Unknown command {invalid}" }: Protocol.InteractionError)
|
||||
(name? := .some "Invalid Command"),
|
||||
step "expr.echo" [(invalid, .str "Random garbage data")]
|
||||
({ error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected" }:
|
||||
Protocol.InteractionError)
|
||||
(name? := .some "JSON Deserialization")
|
||||
]
|
||||
def test_tactic : IO LSpec.TestSeq :=
|
||||
def test_tactic : Test :=
|
||||
let goal1: Protocol.Goal := {
|
||||
name := "_uniq.11",
|
||||
target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
|
||||
vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
|
||||
vars := #[{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}],
|
||||
}
|
||||
let goal2: Protocol.Goal := {
|
||||
name := "_uniq.14",
|
||||
name := "_uniq.17",
|
||||
target := { pp? := .some "x ∨ y → y ∨ x" },
|
||||
vars := #[
|
||||
{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
|
||||
{ name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
|
||||
{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }},
|
||||
{ name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }}
|
||||
],
|
||||
}
|
||||
subroutine_runner [
|
||||
subroutine_step "goal.start"
|
||||
[("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
|
||||
(Lean.toJson ({stateId := 0, root := "_uniq.9"}:
|
||||
Protocol.GoalStartResult)),
|
||||
subroutine_step "goal.tactic"
|
||||
[("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
|
||||
(Lean.toJson ({
|
||||
nextStateId? := .some 1,
|
||||
goals? := #[goal1],
|
||||
}:
|
||||
Protocol.GoalTacticResult)),
|
||||
subroutine_step "goal.print"
|
||||
[("stateId", .num 1)]
|
||||
(Lean.toJson ({
|
||||
parent? := .some { pp? := .some "fun x => ?m.12 x" },
|
||||
}:
|
||||
Protocol.GoalPrintResult)),
|
||||
subroutine_step "goal.tactic"
|
||||
[("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
|
||||
(Lean.toJson ({
|
||||
nextStateId? := .some 2,
|
||||
goals? := #[goal2],
|
||||
}:
|
||||
Protocol.GoalTacticResult))
|
||||
[
|
||||
step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
|
||||
({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
|
||||
step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
|
||||
({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
|
||||
step "goal.print" [("stateId", .num 1)]
|
||||
({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult),
|
||||
step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
|
||||
({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
|
||||
]
|
||||
def test_automatic_mode (automatic: Bool): Test :=
|
||||
let varsPQ := #[
|
||||
{ name := "_uniq.10", userName := "p", type? := .some { pp? := .some "Prop" }},
|
||||
{ name := "_uniq.13", userName := "q", type? := .some { pp? := .some "Prop" }}
|
||||
]
|
||||
let goal1: Protocol.Goal := {
|
||||
name := "_uniq.17",
|
||||
target := { pp? := .some "q ∨ p" },
|
||||
vars := varsPQ ++ #[
|
||||
{ name := "_uniq.16", userName := "h", type? := .some { pp? := .some "p ∨ q" }}
|
||||
],
|
||||
}
|
||||
let goal2l: Protocol.Goal := {
|
||||
name := "_uniq.59",
|
||||
userName? := .some "inl",
|
||||
target := { pp? := .some "q ∨ p" },
|
||||
vars := varsPQ ++ #[
|
||||
{ name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
|
||||
],
|
||||
}
|
||||
let goal2r: Protocol.Goal := {
|
||||
name := "_uniq.72",
|
||||
userName? := .some "inr",
|
||||
target := { pp? := .some "q ∨ p" },
|
||||
vars := varsPQ ++ #[
|
||||
{ name := "_uniq.60", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
|
||||
],
|
||||
}
|
||||
let goal3l: Protocol.Goal := {
|
||||
name := "_uniq.78",
|
||||
userName? := .some "inl.h",
|
||||
target := { pp? := .some "p" },
|
||||
vars := varsPQ ++ #[
|
||||
{ name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
|
||||
],
|
||||
}
|
||||
[
|
||||
step "options.set" [("automaticMode", .bool automatic)]
|
||||
({}: Protocol.OptionsSetResult),
|
||||
step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
|
||||
({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
|
||||
step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro p q h")]
|
||||
({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
|
||||
step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "cases h")]
|
||||
({ nextStateId? := .some 2, goals? := #[goal2l, goal2r], }: Protocol.GoalTacticResult),
|
||||
let goals? := if automatic then #[goal3l, goal2r] else #[goal3l]
|
||||
step "goal.tactic" [("stateId", .num 2), ("goalId", .num 0), ("tactic", .str "apply Or.inr")]
|
||||
({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult),
|
||||
]
|
||||
|
||||
def test_env_add_inspect : IO LSpec.TestSeq :=
|
||||
def test_env_add_inspect : Test :=
|
||||
let name1 := "Pantograph.mystery"
|
||||
let name2 := "Pantograph.mystery2"
|
||||
subroutine_runner [
|
||||
subroutine_step "env.add"
|
||||
[
|
||||
step "env.add"
|
||||
[
|
||||
("name", .str name1),
|
||||
("type", .str "Prop → Prop → Prop"),
|
||||
("value", .str "λ (a b: Prop) => Or a b"),
|
||||
("isTheorem", .bool false)
|
||||
]
|
||||
(Lean.toJson ({}: Protocol.EnvAddResult)),
|
||||
subroutine_step "env.inspect"
|
||||
[("name", .str name1)]
|
||||
(Lean.toJson ({
|
||||
({}: Protocol.EnvAddResult),
|
||||
step "env.inspect" [("name", .str name1)]
|
||||
({
|
||||
value? := .some { pp? := .some "fun a b => a ∨ b" },
|
||||
type := { pp? := .some "Prop → Prop → Prop" },
|
||||
}:
|
||||
Protocol.EnvInspectResult)),
|
||||
subroutine_step "env.add"
|
||||
Protocol.EnvInspectResult),
|
||||
step "env.add"
|
||||
[
|
||||
("name", .str name2),
|
||||
("type", .str "Nat → Int"),
|
||||
("value", .str "λ (a: Nat) => a + 1"),
|
||||
("isTheorem", .bool false)
|
||||
]
|
||||
(Lean.toJson ({}: Protocol.EnvAddResult)),
|
||||
subroutine_step "env.inspect"
|
||||
[("name", .str name2)]
|
||||
(Lean.toJson ({
|
||||
({}: Protocol.EnvAddResult),
|
||||
step "env.inspect" [("name", .str name2)]
|
||||
({
|
||||
value? := .some { pp? := .some "fun a => ↑a + 1" },
|
||||
type := { pp? := .some "Nat → Int" },
|
||||
}:
|
||||
Protocol.EnvInspectResult))
|
||||
Protocol.EnvInspectResult)
|
||||
]
|
||||
|
||||
def suite: List (String × IO LSpec.TestSeq) :=
|
||||
[
|
||||
("Elab", test_elab),
|
||||
("Option modify", test_option_modify),
|
||||
def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
|
||||
-- Setup the environment for execution
|
||||
let context: Context := {
|
||||
imports := ["Init"]
|
||||
}
|
||||
let commands: MainM LSpec.TestSeq :=
|
||||
steps.foldlM (λ suite step => do
|
||||
let result ← step
|
||||
return suite ++ result) LSpec.TestSeq.done
|
||||
runCoreMSeq env <| commands.run context |>.run' {}
|
||||
|
||||
|
||||
def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
|
||||
let tests := [
|
||||
("expr.echo", test_elab),
|
||||
("options.set options.print", test_option_modify),
|
||||
("Malformed command", test_malformed_command),
|
||||
("Tactic", test_tactic),
|
||||
("Manual Mode", test_automatic_mode false),
|
||||
("Automatic Mode", test_automatic_mode true),
|
||||
("env.add env.inspect", test_env_add_inspect),
|
||||
]
|
||||
tests.map (fun (name, test) => (name, runTest env test))
|
||||
|
||||
|
||||
end Pantograph.Test.Integration
|
||||
|
|
|
@ -5,6 +5,7 @@ import Test.Library
|
|||
import Test.Metavar
|
||||
import Test.Proofs
|
||||
import Test.Serial
|
||||
import Test.Tactic
|
||||
|
||||
-- Test running infrastructure
|
||||
|
||||
|
@ -43,11 +44,15 @@ def main (args: List String) := do
|
|||
|
||||
let suites: List (String × List (String × IO LSpec.TestSeq)) := [
|
||||
("Environment", Environment.suite),
|
||||
("Integration", Integration.suite),
|
||||
("Integration", Integration.suite env_default),
|
||||
("Library", Library.suite env_default),
|
||||
("Metavar", Metavar.suite env_default),
|
||||
("Proofs", Proofs.suite env_default),
|
||||
("Serial", Serial.suite env_default),
|
||||
("Tactic/Congruence", Tactic.Congruence.suite env_default),
|
||||
("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
|
||||
("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
|
||||
("Tactic/Prograde", Tactic.Prograde.suite env_default),
|
||||
]
|
||||
let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
|
||||
LSpec.lspecIO (← runTestGroup name_filter tests)
|
||||
|
|
|
@ -60,14 +60,13 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
|
|||
vars := (nameType.map fun x => ({
|
||||
userName := x.fst,
|
||||
type? := .some { pp? := .some x.snd },
|
||||
isInaccessible? := .some false
|
||||
})).toArray
|
||||
}
|
||||
def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
|
||||
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
|
||||
|
||||
let coreContext: Lean.Core.Context ← createCoreContext #[]
|
||||
let metaM := termElabM.run' (ctx := defaultTermElabMContext)
|
||||
let metaM := termElabM.run' (ctx := Condensed.elabContext)
|
||||
let coreM := metaM.run'
|
||||
match ← (coreM.run' coreContext { env := env }).toBaseIO with
|
||||
| .error exception =>
|
||||
|
@ -84,7 +83,7 @@ def test_m_couple: TestM Unit := do
|
|||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -93,7 +92,7 @@ def test_m_couple: TestM Unit := do
|
|||
#[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
|
||||
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
|
||||
-- Set m to 3
|
||||
let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 3") with
|
||||
let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 3") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -116,7 +115,7 @@ def test_m_couple_simp: TestM Unit := do
|
|||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -127,7 +126,7 @@ def test_m_couple_simp: TestM Unit := do
|
|||
addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) =
|
||||
#[#["_uniq.38"], #["_uniq.38"], #[]])
|
||||
|
||||
let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 2") with
|
||||
let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -141,7 +140,7 @@ def test_m_couple_simp: TestM Unit := do
|
|||
addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
|
||||
#[.some "2 ≤ 2", .some "2 ≤ 5"])
|
||||
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
|
||||
let state3 ← match ← state1b.tryTactic (goalId := 0) (tactic := "simp") with
|
||||
let state3 ← match ← state1b.tacticOn (goalId := 0) (tactic := "simp") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -151,7 +150,7 @@ def test_m_couple_simp: TestM Unit := do
|
|||
addTest $ assertUnreachable $ msg
|
||||
return ()
|
||||
| .ok state => pure state
|
||||
let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := "simp") with
|
||||
let state5 ← match ← state4.tacticOn (goalId := 0) (tactic := "simp") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -178,7 +177,7 @@ def test_proposition_generation: TestM Unit := do
|
|||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply PSigma.mk") with
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply PSigma.mk") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -192,21 +191,22 @@ def test_proposition_generation: TestM Unit := do
|
|||
addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})")
|
||||
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
|
||||
|
||||
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with
|
||||
let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := "λ (x: Nat) => _") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
|
||||
#[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"])
|
||||
#[.some "?m.29 x"])
|
||||
addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
|
||||
|
||||
let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with
|
||||
let assign := "Eq.refl x"
|
||||
let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := assign) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
|
||||
addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
|
||||
#[])
|
||||
|
||||
addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
|
||||
|
@ -220,7 +220,7 @@ def test_partial_continuation: TestM Unit := do
|
|||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -228,7 +228,7 @@ def test_partial_continuation: TestM Unit := do
|
|||
addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
|
||||
#[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
|
||||
|
||||
let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "apply Nat.succ") with
|
||||
let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "apply Nat.succ") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -263,7 +263,7 @@ def test_partial_continuation: TestM Unit := do
|
|||
|
||||
-- Continuation should fail if the state does not exist:
|
||||
match state0.resume coupled_goals with
|
||||
| .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope")
|
||||
| .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope")
|
||||
| .ok _ => addTest $ assertUnreachable "(continuation failure)"
|
||||
-- Continuation should fail if some goals have not been solved
|
||||
match state2.continue state1 with
|
||||
|
|
403
Test/Proofs.lean
403
Test/Proofs.lean
|
@ -49,21 +49,32 @@ def startProof (start: Start): TestM (Option GoalState) := do
|
|||
let goal ← GoalState.create (expr := expr)
|
||||
return Option.some goal
|
||||
|
||||
def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal :=
|
||||
def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
|
||||
(userName?: Option String := .none): Protocol.Goal :=
|
||||
{
|
||||
name,
|
||||
userName?,
|
||||
target := { pp? := .some target},
|
||||
vars := (nameType.map fun x => ({
|
||||
userName := x.fst,
|
||||
type? := .some { pp? := .some x.snd },
|
||||
})).toArray
|
||||
}
|
||||
def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
|
||||
Protocol.Goal :=
|
||||
{
|
||||
userName?,
|
||||
target := { pp? := .some target},
|
||||
vars := (nameType.map fun x => ({
|
||||
userName := x.fst,
|
||||
type? := .some { pp? := .some x.snd },
|
||||
isInaccessible? := .some false
|
||||
})).toArray
|
||||
}
|
||||
def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
|
||||
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
|
||||
|
||||
let coreContext: Lean.Core.Context ← createCoreContext #[]
|
||||
let metaM := termElabM.run' (ctx := defaultTermElabMContext)
|
||||
let metaM := termElabM.run' (ctx := Condensed.elabContext)
|
||||
let coreM := metaM.run'
|
||||
match ← (coreM.run' coreContext { env := env }).toBaseIO with
|
||||
| .error exception =>
|
||||
|
@ -71,6 +82,27 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
|
|||
| .ok (_, a) =>
|
||||
return a
|
||||
|
||||
def test_identity: TestM Unit := do
|
||||
let state? ← startProof (.expr "∀ (p: Prop), p → p")
|
||||
let state0 ← match state? with
|
||||
| .some state => pure state
|
||||
| .none => do
|
||||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
|
||||
let tactic := "intro p h"
|
||||
let state1 ← match ← state0.tacticOn 0 tactic with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let inner := "_uniq.12"
|
||||
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
|
||||
#[inner])
|
||||
let state1parent ← state1.withParentContext do
|
||||
serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
|
||||
addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")
|
||||
|
||||
-- Individual test cases
|
||||
example: ∀ (a b: Nat), a + b = b + a := by
|
||||
intro n m
|
||||
|
@ -86,7 +118,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
|
|||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n m") with
|
||||
let state1 ← match ← state0.tacticOn 0 "intro n m" with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -94,13 +126,13 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
|
|||
addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"])
|
||||
|
||||
match ← state1.tryTactic (goalId := 0) (tactic := "assumption") with
|
||||
match ← state1.tacticOn 0 "assumption" with
|
||||
| .failure #[message] =>
|
||||
addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
||||
let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "rw [Nat.add_comm]") with
|
||||
let state2 ← match ← state1.tacticOn 0 "rw [Nat.add_comm]" with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -118,14 +150,14 @@ def test_delta_variable: TestM Unit := do
|
|||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n") with
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
|
||||
#[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
|
||||
let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "intro m") with
|
||||
let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "intro m") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -141,7 +173,6 @@ def test_delta_variable: TestM Unit := do
|
|||
vars := (nameType.map fun x => ({
|
||||
userName := x.fst,
|
||||
type? := x.snd.map (λ type => { pp? := type }),
|
||||
isInaccessible? := x.snd.map (λ _ => false)
|
||||
})).toArray
|
||||
}
|
||||
|
||||
|
@ -158,14 +189,14 @@ def test_arith: TestM Unit := do
|
|||
return ()
|
||||
|
||||
let tactic := "intros"
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic (state1.goals.length = 1)
|
||||
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
|
||||
let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
|
||||
let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -173,7 +204,7 @@ def test_arith: TestM Unit := do
|
|||
addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
|
||||
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
|
||||
let tactic := "assumption"
|
||||
let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -208,56 +239,81 @@ def test_or_comm: TestM Unit := do
|
|||
addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
|
||||
|
||||
let tactic := "intro p q h"
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"])
|
||||
let fvP := "_uniq.10"
|
||||
let fvQ := "_uniq.13"
|
||||
let fvH := "_uniq.16"
|
||||
let state1g0 := "_uniq.17"
|
||||
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
|
||||
#[{
|
||||
name := state1g0,
|
||||
target := { pp? := .some "q ∨ p" },
|
||||
vars := #[
|
||||
{ name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } },
|
||||
{ name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" } },
|
||||
{ name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
|
||||
]
|
||||
}])
|
||||
addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
|
||||
addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
|
||||
|
||||
let state1parent ← state1.withParentContext do
|
||||
serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
|
||||
addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
|
||||
let tactic := "cases h"
|
||||
let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[branchGoal "inl" "p", branchGoal "inr" "q"])
|
||||
addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
|
||||
let (caseL, caseR) := ("_uniq.64", "_uniq.77")
|
||||
addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
|
||||
#[caseL, caseR])
|
||||
addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
|
||||
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
|
||||
|
||||
let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false)
|
||||
-- This is due to delayed assignment
|
||||
let state2parent ← state2.withParentContext do
|
||||
serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false)
|
||||
let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
|
||||
let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
|
||||
let motive := s!"(:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
|
||||
let caseL := s!"(:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))"
|
||||
let caseR := s!"(:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))"
|
||||
let conduit := s!"((:c Eq.refl) {orPQ} (:fv {fvH}))"
|
||||
addTest $ LSpec.test "(2 parent)" (state2parent ==
|
||||
"((:mv _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
|
||||
s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")
|
||||
|
||||
let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
|
||||
let state3_1 ← match ← state2.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let state3_1parent ← serializeExpressionSexp state3_1.parentExpr?.get! (sanitize := false)
|
||||
addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))")
|
||||
let state3_1parent ← state3_1.withParentContext do
|
||||
serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false)
|
||||
addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))")
|
||||
addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
|
||||
let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with
|
||||
let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check " assumption" state4_1.goals.isEmpty
|
||||
let state4_1parent ← serializeExpressionSexp state4_1.parentExpr?.get! (sanitize := false)
|
||||
addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)")
|
||||
let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
|
||||
addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
|
||||
addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
|
||||
let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with
|
||||
let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1)
|
||||
let state4_2 ← match ← state3_2.tryTactic (goalId := 0) (tactic := "assumption") with
|
||||
let state4_2 ← match ← state3_2.tacticOn (goalId := 0) (tactic := "assumption") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -271,13 +327,13 @@ def test_or_comm: TestM Unit := do
|
|||
return ()
|
||||
| .ok state => pure state
|
||||
addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0])
|
||||
let state3_1 ← match ← state2b.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
|
||||
let state3_1 ← match ← state2b.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
|
||||
let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with
|
||||
let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -292,75 +348,12 @@ def test_or_comm: TestM Unit := do
|
|||
userName? := .some caseName,
|
||||
target := { pp? := .some "q ∨ p" },
|
||||
vars := #[
|
||||
{ userName := "p", type? := .some typeProp, isInaccessible? := .some false },
|
||||
{ userName := "q", type? := .some typeProp, isInaccessible? := .some false },
|
||||
{ userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true }
|
||||
{ userName := "p", type? := .some typeProp },
|
||||
{ userName := "q", type? := .some typeProp },
|
||||
{ userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible := true }
|
||||
]
|
||||
}
|
||||
|
||||
def test_have: TestM Unit := do
|
||||
let state? ← startProof (.expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))")
|
||||
let state0 ← match state? with
|
||||
| .some state => pure state
|
||||
| .none => do
|
||||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
let tactic := "intro p q h"
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
|
||||
|
||||
let expr := "Or.inl (Or.inl h)"
|
||||
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
let haveBind := "y"
|
||||
let haveType := "p ∨ q"
|
||||
let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[
|
||||
buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p ∨ q",
|
||||
buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p ∨ q")] "(p ∨ q) ∨ p ∨ q"
|
||||
])
|
||||
|
||||
let expr := "Or.inl h"
|
||||
let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
let state2b ← match state3.continue state2 with
|
||||
| .ok state => pure state
|
||||
| .error e => do
|
||||
addTest $ assertUnreachable e
|
||||
return ()
|
||||
let expr := "Or.inl y"
|
||||
let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome
|
||||
|
||||
example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
|
||||
intro a b c1 c2 h
|
||||
conv =>
|
||||
|
@ -379,7 +372,7 @@ def test_conv: TestM Unit := do
|
|||
return ()
|
||||
|
||||
let tactic := "intro a b c1 c2 h"
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -387,7 +380,7 @@ def test_conv: TestM Unit := do
|
|||
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[interiorGoal [] "a + b + c1 = b + a + c2"])
|
||||
|
||||
let state2 ← match ← state1.conv (goalId := 0) with
|
||||
let state2 ← match ← state1.conv (state1.get! 0) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -396,7 +389,7 @@ def test_conv: TestM Unit := do
|
|||
#[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
|
||||
|
||||
let convTactic := "rhs"
|
||||
let state3R ← match ← state2.tryTactic (goalId := 0) convTactic with
|
||||
let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -405,7 +398,7 @@ def test_conv: TestM Unit := do
|
|||
#[{ interiorGoal [] "b + a + c2" with isConversion := true }])
|
||||
|
||||
let convTactic := "lhs"
|
||||
let state3L ← match ← state2.tryTactic (goalId := 0) convTactic with
|
||||
let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -414,7 +407,7 @@ def test_conv: TestM Unit := do
|
|||
#[{ interiorGoal [] "a + b + c1" with isConversion := true }])
|
||||
|
||||
let convTactic := "congr"
|
||||
let state4 ← match ← state3L.tryTactic (goalId := 0) convTactic with
|
||||
let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -426,7 +419,7 @@ def test_conv: TestM Unit := do
|
|||
])
|
||||
|
||||
let convTactic := "rw [Nat.add_comm]"
|
||||
let state5_1 ← match ← state4.tryTactic (goalId := 0) convTactic with
|
||||
let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -435,7 +428,7 @@ def test_conv: TestM Unit := do
|
|||
#[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
|
||||
|
||||
let convTactic := "rfl"
|
||||
let state6_1 ← match ← state5_1.tryTactic (goalId := 0) convTactic with
|
||||
let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -450,7 +443,7 @@ def test_conv: TestM Unit := do
|
|||
return ()
|
||||
|
||||
let convTactic := "rfl"
|
||||
let state6 ← match ← state4_1.tryTactic (goalId := 0) convTactic with
|
||||
let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -465,7 +458,7 @@ def test_conv: TestM Unit := do
|
|||
return ()
|
||||
|
||||
let tactic := "exact h"
|
||||
let stateF ← match ← state1_1.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -492,7 +485,7 @@ def test_calc: TestM Unit := do
|
|||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
let tactic := "intro a b c d h1 h2"
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -500,7 +493,7 @@ def test_calc: TestM Unit := do
|
|||
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[interiorGoal [] "a + b = c + d"])
|
||||
let pred := "a + b = b + c"
|
||||
let state2 ← match ← state1.tryCalc (goalId := 0) (pred := pred) with
|
||||
let state2 ← match ← state1.tryCalc (state1.get! 0) (pred := pred) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -510,11 +503,11 @@ def test_calc: TestM Unit := do
|
|||
interiorGoal [] "a + b = b + c" (.some "calc"),
|
||||
interiorGoal [] "b + c = c + d"
|
||||
])
|
||||
addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? 0 |>.isNone)
|
||||
addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? 1 |>.isSome)
|
||||
addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
|
||||
addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)
|
||||
|
||||
let tactic := "apply h1"
|
||||
let state2m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -525,7 +518,7 @@ def test_calc: TestM Unit := do
|
|||
addTest $ expectationFailure "continue" e
|
||||
return ()
|
||||
let pred := "_ = c + d"
|
||||
let state4 ← match ← state3.tryCalc (goalId := 0) (pred := pred) with
|
||||
let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -534,9 +527,9 @@ def test_calc: TestM Unit := do
|
|||
#[
|
||||
interiorGoal [] "b + c = c + d" (.some "calc")
|
||||
])
|
||||
addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? 0 |>.isNone)
|
||||
addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
|
||||
let tactic := "apply h2"
|
||||
let state4m ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
@ -548,95 +541,181 @@ def test_calc: TestM Unit := do
|
|||
("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
|
||||
buildGoal free target userName?
|
||||
|
||||
def test_let (specialized: Bool): TestM Unit := do
|
||||
let state? ← startProof (.expr "∀ (a: Nat) (p: Prop), p → p ∨ ¬p")
|
||||
def test_nat_zero_add: TestM Unit := do
|
||||
let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n")
|
||||
let state0 ← match state? with
|
||||
| .some state => pure state
|
||||
| .none => do
|
||||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
let tactic := "intro a p h"
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
let tactic := "intro n"
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[interiorGoal [] "p ∨ ¬p"])
|
||||
|
||||
|
||||
let letType := "Nat"
|
||||
let expr := s!"let b: {letType} := _; _"
|
||||
let result2 ← match specialized with
|
||||
| true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType)
|
||||
| false => state1.tryAssign (goalId := 0) (expr := expr)
|
||||
let state2 ← match result2 with
|
||||
#[buildGoal [("n", "Nat")] "n + 0 = n"])
|
||||
let recursor := "@Nat.brecOn"
|
||||
let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let serializedState2 ← state2.serializeGoals (options := ← read)
|
||||
addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) =
|
||||
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
|
||||
#[
|
||||
interiorGoal [] letType,
|
||||
interiorGoal [] "let b := ?m.20;\np ∨ ¬p"
|
||||
buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
|
||||
buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
|
||||
buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
|
||||
buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
|
||||
])
|
||||
-- Check that the goal mvar ids match up
|
||||
addTest $ LSpec.check expr ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20")
|
||||
|
||||
let tactic := "exact a"
|
||||
let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
let tactic := "exact n"
|
||||
let state3b ← match ← state2.tacticOn (goalId := 1) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) = #[])
|
||||
|
||||
let state3r ← match state3.continue state2 with
|
||||
| .error msg => do
|
||||
addTest $ assertUnreachable $ msg
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state3b.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[])
|
||||
let state2b ← match state3b.continue state2 with
|
||||
| .ok state => pure state
|
||||
addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[interiorGoal [] "let b := a;\np ∨ ¬p"])
|
||||
|
||||
let tactic := "exact h"
|
||||
match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
| .failure #[message] =>
|
||||
addTest $ LSpec.check tactic (message = "type mismatch\n h\nhas type\n p : Prop\nbut is expected to have type\n let b := a;\n p ∨ ¬p : Prop")
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
||||
let tactic := "intro b"
|
||||
let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
| .error e => do
|
||||
addTest $ assertUnreachable e
|
||||
return ()
|
||||
let tactic := "exact (λ x => x + 0 = x)"
|
||||
let state3c ← match ← state2b.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let tactic := "exact Or.inl h"
|
||||
let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
addTest $ LSpec.check tactic ((← state3c.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[])
|
||||
let state2c ← match state3c.continue state2b with
|
||||
| .ok state => pure state
|
||||
| .error e => do
|
||||
addTest $ assertUnreachable e
|
||||
return ()
|
||||
let tactic := "intro t h"
|
||||
let state3 ← match ← state2c.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.test "(5 root)" state5.rootExpr?.isSome
|
||||
where
|
||||
interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
|
||||
let free := [("a", "Nat"), ("p", "Prop"), ("h", "p")] ++ free
|
||||
buildGoal free target userName?
|
||||
addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
|
||||
|
||||
let tactic := "simp"
|
||||
let state3d ← match ← state3.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let state2d ← match state3d.continue state2c with
|
||||
| .ok state => pure state
|
||||
| .error e => do
|
||||
addTest $ assertUnreachable e
|
||||
return ()
|
||||
let tactic := "rfl"
|
||||
let stateF ← match ← state2d.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)) =
|
||||
#[])
|
||||
|
||||
let expr := stateF.mctx.eAssignment.find! stateF.root
|
||||
let (expr, _) := instantiateMVarsCore (mctx := stateF.mctx) (e := expr)
|
||||
addTest $ LSpec.check "(F root)" stateF.rootExpr?.isSome
|
||||
|
||||
def test_nat_zero_add_alt: TestM Unit := do
|
||||
let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n")
|
||||
let state0 ← match state? with
|
||||
| .some state => pure state
|
||||
| .none => do
|
||||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
let tactic := "intro n"
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[buildGoal [("n", "Nat")] "n + 0 = n"])
|
||||
let recursor := "@Nat.brecOn"
|
||||
let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let major := "_uniq.68"
|
||||
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
|
||||
#[
|
||||
buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
|
||||
buildNamedGoal major [("n", "Nat")] "Nat",
|
||||
buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
|
||||
buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
|
||||
])
|
||||
|
||||
let tactic := "intro x"
|
||||
let state3m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state3m.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[buildGoal [("n", "Nat"), ("x", "Nat")] "Prop" (.some "motive")])
|
||||
let tactic := "apply Eq"
|
||||
let state3m2 ← match ← state3m.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
|
||||
addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
|
||||
let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
|
||||
let state2b ← match state3m2.resume [conduit] with
|
||||
| .ok state => pure state
|
||||
| .error e => do
|
||||
addTest $ assertUnreachable e
|
||||
return ()
|
||||
|
||||
let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
|
||||
let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
|
||||
let fvN := "_uniq.63"
|
||||
let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
|
||||
let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
|
||||
addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
|
||||
#[
|
||||
{
|
||||
name := "_uniq.70",
|
||||
userName? := .some "conduit",
|
||||
target := {
|
||||
pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)",
|
||||
sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
|
||||
},
|
||||
vars := #[{
|
||||
name := fvN,
|
||||
userName := "n",
|
||||
type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
|
||||
}],
|
||||
}
|
||||
])
|
||||
|
||||
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||
let tests := [
|
||||
("identity", test_identity),
|
||||
("Nat.add_comm", test_nat_add_comm false),
|
||||
("Nat.add_comm manual", test_nat_add_comm true),
|
||||
("Nat.add_comm delta", test_delta_variable),
|
||||
("arithmetic", test_arith),
|
||||
("Or.comm", test_or_comm),
|
||||
("have", test_have),
|
||||
("conv", test_conv),
|
||||
("calc", test_calc),
|
||||
("let via assign", test_let false),
|
||||
("let via tryLet", test_let true),
|
||||
("Nat.zero_add", test_nat_zero_add),
|
||||
("Nat.zero_add alt", test_nat_zero_add_alt),
|
||||
]
|
||||
tests.map (fun (name, test) => (name, proofRunner env test))
|
||||
|
||||
|
|
|
@ -50,9 +50,9 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
|
|||
let entries: List (String × (List Name) × String) := [
|
||||
("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
|
||||
("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
|
||||
-- This tests `autoBoundImplicit`
|
||||
("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
|
||||
("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"),
|
||||
("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"),
|
||||
]
|
||||
entries.foldlM (λ suites (source, levels, target) =>
|
||||
let termElabM := do
|
||||
|
@ -64,7 +64,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
|
|||
| .ok expr => pure expr
|
||||
| .error e => return elabFailure e
|
||||
return LSpec.check source ((← serializeExpressionSexp expr) = target)
|
||||
let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := defaultTermElabMContext)
|
||||
let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := Condensed.elabContext)
|
||||
return LSpec.TestSeq.append suites (← runMetaMSeq env metaM))
|
||||
LSpec.TestSeq.done
|
||||
|
||||
|
@ -85,7 +85,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
|
|||
let testCaseName := target.take 10
|
||||
let test := LSpec.check testCaseName ((← serializeExpressionSexp expr) = target)
|
||||
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
|
||||
runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext)
|
||||
runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
|
||||
|
||||
-- Instance parsing
|
||||
def test_instance (env: Environment): IO LSpec.TestSeq :=
|
||||
|
|
|
@ -0,0 +1,4 @@
|
|||
import Test.Tactic.Congruence
|
||||
import Test.Tactic.MotivatedApply
|
||||
import Test.Tactic.NoConfuse
|
||||
import Test.Tactic.Prograde
|
|
@ -0,0 +1,88 @@
|
|||
import LSpec
|
||||
import Lean
|
||||
import Test.Common
|
||||
|
||||
open Lean
|
||||
open Pantograph
|
||||
|
||||
namespace Pantograph.Test.Tactic.Congruence
|
||||
|
||||
def test_congr_arg_list : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse"
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
|
||||
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||||
[
|
||||
(`α, "Sort ?u.30"),
|
||||
(`a₁, "?α"),
|
||||
(`a₂, "?α"),
|
||||
(`f, "?α → List α"),
|
||||
(`h, "?a₁ = ?a₂"),
|
||||
(`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
|
||||
])
|
||||
let f := newGoals.get! 3
|
||||
let h := newGoals.get! 4
|
||||
let c := newGoals.get! 5
|
||||
let results ← f.apply (← parseSentence "List.reverse")
|
||||
addTest $ LSpec.check "apply" (results.length = 0)
|
||||
addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
|
||||
addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)")
|
||||
def test_congr_arg : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
|
||||
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||||
[
|
||||
(`α, "Sort ?u.70"),
|
||||
(`a₁, "?α"),
|
||||
(`a₂, "?α"),
|
||||
(`f, "?α → Nat"),
|
||||
(`h, "?a₁ = ?a₂"),
|
||||
(`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"),
|
||||
])
|
||||
def test_congr_fun : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2"
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
|
||||
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||||
[
|
||||
(`α, "Sort ?u.159"),
|
||||
(`f₁, "?α → Nat"),
|
||||
(`f₂, "?α → Nat"),
|
||||
(`h, "?f₁ = ?f₂"),
|
||||
(`a, "?α"),
|
||||
(`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"),
|
||||
])
|
||||
def test_congr : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (a b: Nat) => a = b"
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let newGoals ← runTacticOnMVar Tactic.evalCongruence target.mvarId!
|
||||
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||||
[
|
||||
(`α, "Sort ?u.10"),
|
||||
(`f₁, "?α → Nat"),
|
||||
(`f₂, "?α → Nat"),
|
||||
(`a₁, "?α"),
|
||||
(`a₂, "?α"),
|
||||
(`h₁, "?f₁ = ?f₂"),
|
||||
(`h₂, "?a₁ = ?a₂"),
|
||||
(`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"),
|
||||
])
|
||||
|
||||
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||
[
|
||||
("congrArg List.reverse", test_congr_arg_list),
|
||||
("congrArg", test_congr_arg),
|
||||
("congrFun", test_congr_fun),
|
||||
("congr", test_congr),
|
||||
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
|
||||
|
||||
end Pantograph.Test.Tactic.Congruence
|
|
@ -0,0 +1,113 @@
|
|||
import LSpec
|
||||
import Lean
|
||||
import Test.Common
|
||||
|
||||
open Lean
|
||||
open Pantograph
|
||||
|
||||
namespace Pantograph.Test.Tactic.MotivatedApply
|
||||
|
||||
def test_type_extract : TestT Elab.TermElabM Unit := do
|
||||
let recursor ← parseSentence "@Nat.brecOn"
|
||||
let recursorType ← Meta.inferType recursor
|
||||
addTest $ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" =
|
||||
(← exprToStr recursorType))
|
||||
let info ← match Tactic.getRecursorInformation recursorType with
|
||||
| .some info => pure info
|
||||
| .none => throwError "Failed to extract recursor info"
|
||||
addTest $ LSpec.check "iMotive" (info.iMotive = 2)
|
||||
let motiveType := info.getMotiveType
|
||||
addTest $ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
|
||||
(← exprToStr motiveType))
|
||||
|
||||
def test_nat_brec_on : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (n t: Nat) => n + 0 = n"
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let recursor ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := "@Nat.brecOn")
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
-- Apply the tactic
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let tactic := Tactic.evalMotivatedApply recursor
|
||||
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
||||
let test := LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
||||
[
|
||||
"Nat → Prop",
|
||||
"Nat",
|
||||
"∀ (t : Nat), Nat.below t → ?motive t",
|
||||
"?motive ?m.67 = (n + 0 = n)",
|
||||
])
|
||||
addTest test
|
||||
|
||||
def test_list_brec_on : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l"
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let recursor ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := "@List.brecOn")
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
-- Apply the tactic
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let tactic := Tactic.evalMotivatedApply recursor
|
||||
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
||||
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
||||
[
|
||||
"Type ?u.90",
|
||||
"List ?m.92 → Prop",
|
||||
"List ?m.92",
|
||||
"∀ (t : List ?m.92), List.below t → ?motive t",
|
||||
"?motive ?m.94 = (l ++ [] = [] ++ l)",
|
||||
])
|
||||
|
||||
def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (n t: Nat) => n + 0 = n"
|
||||
let recursor ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := "@Nat.brecOn")
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
-- Apply the tactic
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let tactic := Tactic.evalMotivatedApply recursor
|
||||
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
||||
let majorId := 67
|
||||
addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
||||
[
|
||||
"Nat → Prop",
|
||||
"Nat",
|
||||
"∀ (t : Nat), Nat.below t → ?motive t",
|
||||
s!"?motive ?m.{majorId} = (n + 0 = n)",
|
||||
]))
|
||||
let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number"
|
||||
addTest $ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}"))
|
||||
|
||||
-- Assign motive to `λ x => x + _`
|
||||
let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _"
|
||||
motive.assign motive_assign
|
||||
|
||||
addTest $ ← conduit.withContext do
|
||||
let t := toString (← Meta.ppExpr $ ← conduit.getType)
|
||||
return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")
|
||||
|
||||
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||
[
|
||||
("type_extract", test_type_extract),
|
||||
("Nat.brecOn", test_nat_brec_on),
|
||||
("List.brecOn", test_list_brec_on),
|
||||
("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation),
|
||||
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
|
||||
|
||||
end Pantograph.Test.Tactic.MotivatedApply
|
|
@ -0,0 +1,72 @@
|
|||
import LSpec
|
||||
import Lean
|
||||
import Test.Common
|
||||
|
||||
open Lean
|
||||
open Pantograph
|
||||
|
||||
namespace Pantograph.Test.Tactic.NoConfuse
|
||||
|
||||
def test_nat : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (n: Nat) (h: 0 = n + 1) => False"
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let recursor ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := "h")
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
-- Apply the tactic
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let tactic := Tactic.evalNoConfuse recursor
|
||||
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
||||
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
|
||||
|
||||
def test_nat_fail : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (n: Nat) (h: n = n) => False"
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let recursor ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := "h")
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
-- Apply the tactic
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
try
|
||||
let tactic := Tactic.evalNoConfuse recursor
|
||||
let _ ← runTacticOnMVar tactic target.mvarId!
|
||||
addTest $ assertUnreachable "Tactic should fail"
|
||||
catch _ =>
|
||||
addTest $ LSpec.check "Tactic should fail" true
|
||||
|
||||
def test_list : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False"
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let recursor ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := "h")
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
-- Apply the tactic
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let tactic := Tactic.evalNoConfuse recursor
|
||||
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
||||
addTest $ LSpec.check "goals"
|
||||
((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
|
||||
|
||||
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||
[
|
||||
("Nat", test_nat),
|
||||
("Nat fail", test_nat_fail),
|
||||
("List", test_list),
|
||||
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
|
||||
|
||||
end Pantograph.Test.Tactic.NoConfuse
|
|
@ -0,0 +1,300 @@
|
|||
import LSpec
|
||||
import Lean
|
||||
import Test.Common
|
||||
|
||||
open Lean
|
||||
open Pantograph
|
||||
|
||||
namespace Pantograph.Test.Tactic.Prograde
|
||||
|
||||
def test_define : TestT Elab.TermElabM Unit := do
|
||||
let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)"
|
||||
let expr ← parseSentence expr
|
||||
Meta.forallTelescope expr $ λ _ body => do
|
||||
let e ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := "Or.inl h")
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
-- Apply the tactic
|
||||
let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let target: Expr := mkAnd
|
||||
(mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
|
||||
(mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
|
||||
let h := .fvar ⟨uniq 8⟩
|
||||
addTest $ LSpec.test "goals before" ((← toCondensedGoal goal.mvarId!).devolatilize == {
|
||||
context := #[
|
||||
cdeclOf `p (.sort 0),
|
||||
cdeclOf `q (.sort 0),
|
||||
cdeclOf `h h
|
||||
],
|
||||
target,
|
||||
})
|
||||
let tactic := Tactic.evalDefine `h2 e
|
||||
let m := .mvar ⟨uniq 13⟩
|
||||
let [newGoal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number"
|
||||
addTest $ LSpec.test "goals after" ((← toCondensedGoal newGoal).devolatilize == {
|
||||
context := #[
|
||||
cdeclOf `p (.sort 0),
|
||||
cdeclOf `q (.sort 0),
|
||||
cdeclOf `h h,
|
||||
{
|
||||
userName := `h2,
|
||||
type := mkOr h m,
|
||||
value? := .some $ mkApp3 (mkConst `Or.inl) h m (.fvar ⟨uniq 10⟩)
|
||||
}
|
||||
],
|
||||
target,
|
||||
})
|
||||
let .some e ← getExprMVarAssignment? goal.mvarId! | panic! "Tactic must assign"
|
||||
addTest $ LSpec.test "assign" e.isLet
|
||||
|
||||
def test_define_proof : TestT Elab.TermElabM Unit := do
|
||||
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
|
||||
let state0 ← GoalState.create rootExpr
|
||||
let tactic := "intro p q h"
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
|
||||
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
|
||||
|
||||
let expr := "Or.inl (Or.inl h)"
|
||||
let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
let evalBind := "y"
|
||||
let evalExpr := "Or.inl h"
|
||||
let state2 ← match ← state1.tryDefine (state1.get! 0) (binderName := evalBind) (expr := evalExpr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!"eval {evalBind} := {evalExpr}" ((← state2.serializeGoals).map (·.devolatilize) =
|
||||
#[{
|
||||
target := { pp? := .some "(p ∨ q) ∨ p ∨ q"},
|
||||
vars := #[
|
||||
{ userName := "p", type? := .some { pp? := .some "Prop" } },
|
||||
{ userName := "q", type? := .some { pp? := .some "Prop" } },
|
||||
{ userName := "h", type? := .some { pp? := .some "p" } },
|
||||
{ userName := "y",
|
||||
type? := .some { pp? := .some "p ∨ ?m.25" },
|
||||
value? := .some { pp? := .some "Or.inl h" },
|
||||
}
|
||||
]
|
||||
}])
|
||||
|
||||
let expr := "Or.inl y"
|
||||
let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
|
||||
|
||||
def fun_define_root_expr: ∀ (p: Prop), PProd (Nat → p) Unit → p := by
|
||||
intro p x
|
||||
apply x.fst
|
||||
exact 5
|
||||
|
||||
def test_define_root_expr : TestT Elab.TermElabM Unit := do
|
||||
--let rootExpr ← parseSentence "Nat"
|
||||
--let state0 ← GoalState.create rootExpr
|
||||
--let .success state1 ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
|
||||
--let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr"
|
||||
--addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5")
|
||||
let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p"
|
||||
let state0 ← GoalState.create rootExpr
|
||||
let tactic := "intro p x"
|
||||
let .success state1 ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
|
||||
let binderName := `binder
|
||||
let value := "x.fst"
|
||||
let expr ← state1.goals[0]!.withContext $ strToTermSyntax value
|
||||
let tacticM := Tactic.evalDefine binderName expr
|
||||
let .success state2 ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
|
||||
let tactic := s!"apply {binderName}"
|
||||
let .success state3 ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
|
||||
let tactic := s!"exact 5"
|
||||
let .success state4 ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
|
||||
let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
|
||||
addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n let binder := x.fst;\n binder 5")
|
||||
|
||||
--set_option pp.all true
|
||||
--#check @PSigma (α := Prop) (β := λ (p: Prop) => p)
|
||||
--def test_define_root_expr : TestT Elab.TermElabM Unit := do
|
||||
|
||||
def test_have_proof : TestT Elab.TermElabM Unit := do
|
||||
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
|
||||
let state0 ← GoalState.create rootExpr
|
||||
let tactic := "intro p q h"
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
|
||||
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
|
||||
|
||||
let expr := "Or.inl (Or.inl h)"
|
||||
let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
let haveBind := "y"
|
||||
let haveType := "p ∨ q"
|
||||
let state2 ← match ← state1.tryHave (state1.get! 0) (binderName := haveBind) (type := haveType) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals).map (·.devolatilize) =
|
||||
#[
|
||||
buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p ∨ q",
|
||||
buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p ∨ q")] "(p ∨ q) ∨ p ∨ q"
|
||||
])
|
||||
|
||||
let expr := "Or.inl h"
|
||||
let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
let state2b ← match state3.continue state2 with
|
||||
| .ok state => pure state
|
||||
| .error e => do
|
||||
addTest $ assertUnreachable e
|
||||
return ()
|
||||
let expr := "Or.inl y"
|
||||
let state4 ← match ← state2b.tryAssign (state2b.get! 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
|
||||
addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p q h y => Or.inl y")
|
||||
|
||||
def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
|
||||
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
|
||||
let state0 ← GoalState.create rootExpr
|
||||
let tactic := "intro a p h"
|
||||
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
|
||||
#[{
|
||||
target := { pp? := .some mainTarget },
|
||||
vars := interiorVars,
|
||||
}])
|
||||
|
||||
let letType := "Nat"
|
||||
let expr := s!"let b: {letType} := _; _"
|
||||
let result2 ← match specialized with
|
||||
| true => state1.tryLet (state1.get! 0) (binderName := "b") (type := letType)
|
||||
| false => state1.tryAssign (state1.get! 0) (expr := expr)
|
||||
let state2 ← match result2 with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let serializedState2 ← state2.serializeGoals
|
||||
let letBindName := if specialized then "b" else "_1"
|
||||
addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) =
|
||||
#[{
|
||||
target := { pp? := .some letType },
|
||||
vars := interiorVars,
|
||||
userName? := .some letBindName
|
||||
},
|
||||
{
|
||||
target := { pp? := .some mainTarget },
|
||||
vars := interiorVars ++ #[{
|
||||
userName := "b",
|
||||
type? := .some { pp? := .some letType },
|
||||
value? := .some { pp? := .some s!"?{letBindName}" },
|
||||
}],
|
||||
userName? := if specialized then .none else .some "_2",
|
||||
}
|
||||
])
|
||||
|
||||
let tactic := "exact 1"
|
||||
let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state3.serializeGoals).map (·.devolatilize) = #[])
|
||||
|
||||
let state3r ← match state3.continue state2 with
|
||||
| .error msg => do
|
||||
addTest $ assertUnreachable $ msg
|
||||
return ()
|
||||
| .ok state => pure state
|
||||
addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals).map (·.devolatilize) =
|
||||
#[
|
||||
{
|
||||
target := { pp? := .some mainTarget },
|
||||
vars := interiorVars ++ #[{
|
||||
userName := "b",
|
||||
type? := .some { pp? := .some "Nat" },
|
||||
value? := .some { pp? := .some "1" },
|
||||
}],
|
||||
userName? := if specialized then .none else .some "_2",
|
||||
}
|
||||
])
|
||||
|
||||
let tactic := "exact h"
|
||||
match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .failure #[message] =>
|
||||
addTest $ LSpec.check tactic (message = s!"type mismatch\n h\nhas type\n a : Prop\nbut is expected to have type\n {mainTarget} : Prop")
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
||||
let tactic := "exact Or.inl (Or.inl h)"
|
||||
let state4 ← match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.test "(4 root)" state4.rootExpr?.isSome
|
||||
where
|
||||
mainTarget := "(a ∨ p) ∨ a ∨ p"
|
||||
interiorVars: Array Protocol.Variable := #[
|
||||
{ userName := "a", type? := .some { pp? := .some "Prop" }, },
|
||||
{ userName := "p", type? := .some { pp? := .some "Prop" }, },
|
||||
{ userName := "h", type? := .some { pp? := .some "a" }, }
|
||||
]
|
||||
|
||||
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||
[
|
||||
("define", test_define),
|
||||
("define proof", test_define_proof),
|
||||
("define root expr", test_define_root_expr),
|
||||
("have proof", test_have_proof),
|
||||
("let via assign", test_let false),
|
||||
("let via tryLet", test_let true),
|
||||
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
|
||||
|
||||
end Pantograph.Test.Tactic.Prograde
|
16
flake.lock
16
flake.lock
|
@ -42,16 +42,16 @@
|
|||
"nixpkgs-old": "nixpkgs-old"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1714704934,
|
||||
"narHash": "sha256-q0kLyIahUXolkSrBZSegPF+R99WAH1YC96JfKoFntDE=",
|
||||
"lastModified": 1719788866,
|
||||
"narHash": "sha256-kB2cp1XJKODXiuiKp7J5OK+PFP+sOSBE5gdVNOKWCPI=",
|
||||
"owner": "leanprover",
|
||||
"repo": "lean4",
|
||||
"rev": "dcccfb73cb247e9478220375ab7de03f7c67e505",
|
||||
"rev": "3b58e0649156610ce3aeed4f7b5c652340c668d4",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "leanprover",
|
||||
"ref": "v4.8.0-rc1",
|
||||
"ref": "v4.10.0-rc1",
|
||||
"repo": "lean4",
|
||||
"type": "github"
|
||||
}
|
||||
|
@ -91,16 +91,16 @@
|
|||
"lspec": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
"lastModified": 1701971219,
|
||||
"narHash": "sha256-HYDRzkT2UaLDrqKNWesh9C4LJNt0JpW0u68wYVj4Byw=",
|
||||
"lastModified": 1722857503,
|
||||
"narHash": "sha256-F9uaymiw1wTCLrJm4n1Bpk3J8jW6poedQzvnnQlZ6Kw=",
|
||||
"owner": "lurk-lab",
|
||||
"repo": "LSpec",
|
||||
"rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
|
||||
"rev": "8a51034d049c6a229d88dd62f490778a377eec06",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "lurk-lab",
|
||||
"ref": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
|
||||
"ref": "8a51034d049c6a229d88dd62f490778a377eec06",
|
||||
"repo": "LSpec",
|
||||
"type": "github"
|
||||
}
|
||||
|
|
37
flake.nix
37
flake.nix
|
@ -6,10 +6,10 @@
|
|||
flake-parts.url = "github:hercules-ci/flake-parts";
|
||||
lean = {
|
||||
# Do not follow input's nixpkgs since it could cause build failures
|
||||
url = "github:leanprover/lean4?ref=v4.8.0-rc1";
|
||||
url = "github:leanprover/lean4?ref=v4.10.0-rc1";
|
||||
};
|
||||
lspec = {
|
||||
url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
|
||||
url = "github:lurk-lab/LSpec?ref=8a51034d049c6a229d88dd62f490778a377eec06";
|
||||
flake = false;
|
||||
};
|
||||
};
|
||||
|
@ -37,14 +37,25 @@
|
|||
};
|
||||
project = leanPkgs.buildLeanPackage {
|
||||
name = "Pantograph";
|
||||
roots = [ "Main" "Pantograph" ];
|
||||
src = pkgs.lib.cleanSourceWith {
|
||||
roots = [ "Pantograph" ];
|
||||
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
|
||||
src = ./.;
|
||||
filter = path: type:
|
||||
!(pkgs.lib.hasInfix "/Test/" path) &&
|
||||
!(pkgs.lib.hasSuffix ".md" path) &&
|
||||
!(pkgs.lib.hasSuffix "Makefile" path);
|
||||
};
|
||||
!(pkgs.lib.hasSuffix "Repl.lean" path);
|
||||
});
|
||||
};
|
||||
repl = leanPkgs.buildLeanPackage {
|
||||
name = "Repl";
|
||||
roots = [ "Main" "Repl" ];
|
||||
deps = [ project ];
|
||||
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
|
||||
src = ./.;
|
||||
filter = path: type:
|
||||
!(pkgs.lib.hasInfix "/Test/" path) &&
|
||||
!(pkgs.lib.hasSuffix ".md" path);
|
||||
});
|
||||
};
|
||||
test = leanPkgs.buildLeanPackage {
|
||||
name = "Test";
|
||||
|
@ -52,18 +63,22 @@
|
|||
# root begins (e.g. `import Test.Environment` and not `import
|
||||
# Environment`) and thats where `lakefile.lean` resides.
|
||||
roots = [ "Test.Main" ];
|
||||
deps = [ lspecLib project ];
|
||||
src = pkgs.lib.cleanSourceWith {
|
||||
deps = [ lspecLib repl ];
|
||||
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
|
||||
src = ./.;
|
||||
filter = path: type:
|
||||
!(pkgs.lib.hasInfix "Pantograph" path);
|
||||
};
|
||||
});
|
||||
};
|
||||
in rec {
|
||||
packages = {
|
||||
inherit (leanPkgs) lean lean-all;
|
||||
inherit (project) sharedLib executable;
|
||||
default = project.executable;
|
||||
inherit (project) sharedLib;
|
||||
inherit (repl) executable;
|
||||
default = repl.executable;
|
||||
};
|
||||
legacyPackages = {
|
||||
inherit project leanPkgs;
|
||||
};
|
||||
checks = {
|
||||
test = pkgs.runCommand "test" {
|
||||
|
|
|
@ -4,13 +4,16 @@ open Lake DSL
|
|||
package pantograph
|
||||
|
||||
lean_lib Pantograph {
|
||||
roots := #[`Pantograph]
|
||||
defaultFacets := #[LeanLib.sharedFacet]
|
||||
}
|
||||
|
||||
lean_lib Repl {
|
||||
}
|
||||
@[default_target]
|
||||
lean_exe pantograph {
|
||||
lean_exe repl {
|
||||
root := `Main
|
||||
-- Somehow solves the native symbol not found problem
|
||||
-- Solves the native symbol not found problem
|
||||
supportInterpreter := true
|
||||
}
|
||||
|
||||
|
@ -18,8 +21,9 @@ require LSpec from git
|
|||
"https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
|
||||
lean_lib Test {
|
||||
}
|
||||
@[test_driver]
|
||||
lean_exe test {
|
||||
root := `Test.Main
|
||||
-- Somehow solves the native symbol not found problem
|
||||
-- Solves the native symbol not found problem
|
||||
supportInterpreter := true
|
||||
}
|
||||
|
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:v4.8.0-rc1
|
||||
leanprover/lean4:v4.10.0-rc1
|
||||
|
|
Loading…
Reference in New Issue