doc: Reason why not to follow nixpkgs

Reviewed-on: #47

LICENSE

@@ -1,674 +0,0 @@
-                    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>.

Main.lean

@@ -4,7 +4,6 @@ import Lean.Environment
 import Pantograph.Version
 import Pantograph.Library
 import Pantograph
-import Repl
 
 -- Main IO functions
 open Pantograph

Makefile

@@ -0,0 +1,20 @@
+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

Pantograph.lean

@@ -1,8 +1,184 @@
-import Pantograph.Compile
-import Pantograph.Condensed
-import Pantograph.Environment
 import Pantograph.Goal
-import Pantograph.Library
 import Pantograph.Protocol
 import Pantograph.Serial
-import Pantograph.Version
+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 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,
+        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 => do
+        let expr ← match ← exprParse expr with
+          | .error e => return .error e
+          | .ok expr => pure $ expr
+        return .ok $ ← GoalState.create expr
+      | .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? with
+        | .some tactic, .none => do
+          pure ( Except.ok (← goalTactic goalState args.goalId tactic))
+        | .none, .some expr => do
+          pure ( Except.ok (← goalTryAssign goalState args.goalId expr))
+        | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} 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 (.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 $ 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
+    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

Pantograph/Compile.lean

@@ -1,25 +0,0 @@
-/- 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

Pantograph/Compile/Elab.lean

@@ -1,146 +0,0 @@
-
-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

Pantograph/Compile/Frontend.lean

@@ -1,86 +0,0 @@
-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

Pantograph/Compile/Parse.lean

@@ -1,14 +0,0 @@
-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

Pantograph/Condensed.lean

@@ -1,96 +0,0 @@
-/- 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

Pantograph/Environment.lean

@@ -7,36 +7,15 @@ open Pantograph
 
 namespace Pantograph.Environment
 
-@[export pantograph_is_name_internal]
-def isNameInternal (n: Name): Bool :=
+def isNameInternal (n: Lean.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: Name): Bool := match name.getRoot with
+  isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
     | .str _ name => name == "Lean"
     | _ => true
 
-/-- 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 :=
+def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String :=
   let pref := match info with
   | .axiomInfo  _ => "a"
   | .defnInfo   _ => "d"
@@ -73,26 +52,25 @@ 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 type).run',
+    type := ← (serialize_expression options info.type).run',
     isUnsafe := info.isUnsafe,
-    value? := ← value?.mapM (λ v => serializeExpression options v |>.run'),
+    value? := ← value?.mapM (λ v => serialize_expression 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 <| 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) )
+      then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n)
       else .none,
+    valueDependency? := ← if args.dependency?.getD false
+      then info.value?.mapM (λ e => do
+        let e ← (unfoldAuxLemmas e).run'
+        pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => name_to_ast n) )
+      else pure (.none),
     module? := module?
   }
-  let result ← match info with
-    | .inductInfo induct => pure { core with inductInfo? := .some {
+  let result := match info with
+    | .inductInfo induct => { core with inductInfo? := .some {
           numParams := induct.numParams,
           numIndices := induct.numIndices,
           all := induct.all.toArray.map (·.toString),
@@ -101,38 +79,32 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
           isReflexive := induct.isReflexive,
           isNested := induct.isNested,
       } }
-    | .ctorInfo ctor => pure { core with constructorInfo? := .some {
+    | .ctorInfo ctor => { core with constructorInfo? := .some {
           induct := ctor.induct.toString,
           cidx := ctor.cidx,
           numParams := ctor.numParams,
           numFields := ctor.numFields,
       } }
-    | .recInfo r => pure { core with recursorInfo? := .some {
+    | .recInfo r => { core with recursorInfo? := .some {
           all := r.all.toArray.map (·.toString),
           numParams := r.numParams,
           numIndices := r.numIndices,
           numMotives := r.numMotives,
           numMinors := r.numMinors,
-          rules := ← r.rules.toArray.mapM (λ rule => do
-              pure {
-                ctor := rule.ctor.toString,
-                nFields := rule.nfields,
-                rhs := ← (serializeExpression options rule.rhs).run',
-              })
           k := r.k,
       } }
-    | _ => pure core
+    | _ => core
   return .ok result
 def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
   let env ← Lean.MonadEnv.getEnv
   let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
-    let type ← match parseTerm env args.type with
+    let type ← match syntax_from_str env args.type with
       | .ok syn => do
-        match ← elabTerm syn with
+        match ← syntax_to_expr syn with
         | .error e => return .error e
         | .ok expr => pure expr
       | .error e => return .error e
-    let value ← match parseTerm env args.value with
+    let value ← match syntax_from_str env args.value with
       | .ok syn => do
         try
           let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
@@ -153,7 +125,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 (← getOptions) constant with
+  let env' ← match env.addDecl constant with
     | .error e => do
       let options ← Lean.MonadOptions.getOptions
       let desc ← (e.toMessageData options).toString

Pantograph/Expr.lean

@@ -1,160 +0,0 @@
-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

Pantograph/Goal.lean

@@ -1,124 +1,191 @@
-/-
-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
 
-def filename: String := "<pantograph>"
-
-/--
-Represents an interconnected set of metavariables, or a state in proof search
- -/
 structure GoalState where
   savedState : Elab.Tactic.SavedState
 
   -- The root hole which is the search target
   root: MVarId
+  -- New metavariables acquired in this state
+  newMVars: SSet MVarId
+
+  -- The id of the goal in the parent
+  parentGoalId: Nat := 0
 
   -- Parent state metavariable source
-  parentMVar?: Option MVarId
+  parentMVar: Option MVarId
 
-  -- Existence of this field shows that we are currently in `conv` mode.
-  -- (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 (MVarId × Expr) := .none
+abbrev M := Elab.TermElabM
 
-@[export pantograph_goal_state_create_m]
-protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
+protected def GoalState.create (expr: Expr): M 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 root ← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous)
+  let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous))
   let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
-  let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root.mvarId!]}
+  let root := goal.mvarId!
+  let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]}
   return {
-    root := root.mvarId!,
     savedState,
-    parentMVar? := .none,
+    root,
+    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.goals (state: GoalState): List MVarId := state.savedState.tactic.goals
+
+protected def GoalState.runM {α: Type} (state: GoalState) (m: Elab.TermElabM α) : M α := do
+  state.savedState.term.restore
+  m
+
 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
-protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
+private 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]
+def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
+  state.savedState.term.meta.restore
 
-@[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) :
+    M (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 Message.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 },
-    },
-  }
+/-- Response for executing a tactic -/
+inductive TacticResult where
+  -- Goes to next state
+  | success (state: GoalState)
+  -- Tactic failed with messages
+  | failure (messages: Array String)
+  -- Could not parse tactic
+  | parseError (message: String)
+  -- The goal index is out of bounds
+  | indexError (goalId: Nat)
+
+/-- Execute tactic on given state -/
+protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String):
+    M TacticResult := do
+  state.restoreElabM
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure $ goal
+    | .none => return .indexError goalId
+  let tactic ← match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `tactic)
+    (input := tactic)
+    (fileName := "<stdin>") 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.savedState.term.meta.meta.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.
+    let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
+      if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
+        assert! prevMVarDecl.type == mvarDecl.type
+        return acc
+      else
+        return acc.insert mvarId
+      ) SSet.empty
+    return .success {
+      root := state.root,
+      savedState := nextSavedState
+      newMVars,
+      parentGoalId := goalId,
+      parentMVar := .some goal,
+    }
+
+protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M 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)
+    (catName := `term)
+    (input := expr)
+    (fileName := "<stdin>") with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  let tacticM:  Elab.Tactic.TacticM TacticResult := do
+    state.savedState.restore
+    Elab.Tactic.setGoals [goal]
+    try
+      let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
+      -- Attempt to unify the expression
+      let goalType ← goal.getType
+      let exprType ← Meta.inferType expr
+      if !(← Meta.isDefEq goalType exprType) then
+        return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)]
+      goal.checkNotAssigned `GoalState.tryAssign
+      goal.assign expr
+      if (← getThe Core.State).messages.hasErrors then
+        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
+        let errors ← (messages.map Message.data).mapM fun md => md.toString
+        return .failure errors
+      else
+        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 ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
+          if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
+            assert! prevMVarDecl.type == mvarDecl.type
+            return acc
+          else
+            return mvarId :: acc
+          ) []
+        -- The new goals are the newMVars that lack an assignment
+        Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)))
+        let nextSavedState ← MonadBacktrack.saveState
+        return .success {
+          root := state.root,
+          savedState := nextSavedState,
+          newMVars := newMVars.toSSet,
+          parentGoalId := goalId,
+          parentMVar := .some goal,
+        }
+    catch exception =>
+      return .failure #[← exception.toMessageData.toString]
+  tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
 
 /--
 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"
+    .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 =>
@@ -131,10 +198,10 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
         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"
@@ -143,262 +210,25 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
   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
+  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
-@[export pantograph_goal_state_parent_expr]
 protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
-  let parent ← goalState.parentMVar?
+  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
+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
 
---- 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
-  -- Goes to next state
-  | success (state: GoalState)
-  -- Tactic failed with messages
-  | failure (messages: Array String)
-  -- Could not parse tactic
-  | parseError (message: String)
-  -- The given action cannot be executed in the state
-  | invalidAction (message: 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 tactic ← match Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
-    (catName := if state.isConv then `conv else `tactic)
-    (input := tactic)
-    (fileName := filename) with
-    | .ok stx => pure $ stx
-    | .error error => return .parseError error
-  state.tryTacticM goal $ Elab.Tactic.evalTactic tactic
-
-protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
-      Elab.TermElabM TacticResult := do
-  state.restoreElabM
-  let expr ← match Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
-    (catName := `term)
-    (input := expr)
-    (fileName := filename) with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  state.tryTacticM goal $ Tactic.evalAssign expr
-
--- Specialized Tactics
-
-protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String):
-      Elab.TermElabM TacticResult := do
-  state.restoreElabM
-  let type ← match Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
-    (catName := `term)
-    (input := type)
-    (fileName := filename) with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  state.tryTacticM goal $ Tactic.evalLet binderName.toName type
-
-/-- Enter conv tactic mode -/
-protected def GoalState.conv (state: GoalState) (goal: MVarId):
-      Elab.TermElabM TacticResult := do
-  if state.convMVar?.isSome then
-    return .invalidAction "Already in conv state"
-  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.replaceMainGoal [newGoal.mvarId!]
-      pure rhs.mvarId!
-    return (← MonadBacktrack.saveState, convMVar)
-  try
-    let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-    -- Other goals are now dormant
-    let otherGoals := state.goals.filter $ λ g => g != goal
-    return .success {
-      root := state.root,
-      savedState := nextSavedState
-      parentMVar? := .some 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
-    | .some mvar => pure mvar
-    | .none => return .invalidAction "Not in conv state"
-  let tacticM :  Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
-    -- Vide `Lean.Elab.Tactic.Conv.convert`
-    state.savedState.restore
-
-    -- Close all existing goals with `refl`
-    for mvarId in (← Elab.Tactic.getGoals) do
-      liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
-    Elab.Tactic.pruneSolvedGoals
-    unless (← Elab.Tactic.getGoals).isEmpty do
-      throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (← Elab.Tactic.getGoals)}"
-
-    Elab.Tactic.setGoals [convGoal]
-
-    let targetNew ← instantiateMVars (.mvar convRhs)
-    let proof ← instantiateMVars (.mvar convGoal)
-
-    Elab.Tactic.liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof
-    MonadBacktrack.saveState
-  try
-    let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-    return .success {
-      root := state.root,
-      savedState := nextSavedState
-      parentMVar? := .some convGoal,
-      convMVar? := .none
-      calcPrevRhs? := .none
-    }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
-
-protected def GoalState.calcPrevRhsOf? (state: GoalState) (goal: MVarId): Option Expr := do
-  let (mvarId, rhs) ← state.calcPrevRhs?
-  if mvarId == goal then
-    .some rhs
-  else
-    .none
-@[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 `(term|$pred) ← match Parser.runParserCategory
-    (env := state.env)
-    (catName := `term)
-    (input := pred)
-    (fileName := filename) with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  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
-
-    let mut step ← Elab.Term.elabType <| ← do
-      if let some prevRhs := calcPrevRhs? then
-        Elab.Term.annotateFirstHoleWithType pred (← Meta.inferType prevRhs)
-      else
-        pure pred
-
-    let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step |
-      throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}"
-    if let some prevRhs := calcPrevRhs? then
-      unless ← Meta.isDefEqGuarded lhs prevRhs do
-        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- "
-
-    -- Creates a mvar to represent the proof that the calc tactic solves the
-    -- current branch
-    -- In the Lean `calc` tactic this is gobbled up by
-    -- `withCollectingNewGoalsFrom`
-    let mut proof ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) step
-      (userName := tag ++ `calc)
-    let mvarBranch := proof.mvarId!
-
-    let mut proofType ← Meta.inferType proof
-    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
-    unless ← Meta.isDefEq proofType target do
-      let rec throwFailed :=
-        throwError "'calc' tactic failed, has type{indentExpr proofType}\nbut it is expected to have type{indentExpr target}"
-      let some (_, _, rhs) ← Elab.Term.getCalcRelation? proofType | throwFailed
-      let some (r, _, rhs') ← Elab.Term.getCalcRelation? target | throwFailed
-      let lastStep := mkApp2 r rhs rhs'
-      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!
-    goal.assign proof
-
-    let goals := [ mvarBranch ] ++ remainder?.toList
-    let calcPrevRhs? := remainder?.map $ λ g => (g, rhs)
-    return .success {
-      root := state.root,
-      savedState := {
-        term := ← MonadBacktrack.saveState,
-        tactic := { goals },
-      },
-      parentMVar? := .some goal,
-      calcPrevRhs?
-    }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
-
-
-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

Pantograph/Library.lean

@@ -1,4 +1,3 @@
-import Pantograph.Condensed
 import Pantograph.Environment
 import Pantograph.Goal
 import Pantograph.Protocol
@@ -35,14 +34,15 @@ def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO O
 
 end Lean
 
-open Lean
-
 namespace Pantograph
 
-def runMetaM { α } (metaM: MetaM α): CoreM α :=
+def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
   metaM.run'
-def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
-  termElabM.run' (ctx := Condensed.elabContext) |>.run'
+def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
+  termElabM.run' (ctx := {
+    declName? := .none,
+    errToSorry := false,
+  }) |>.run'
 
 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
 
@@ -54,13 +54,13 @@ unsafe def initSearch (sp: String): IO Unit := do
 
 /-- Creates a Core.Context object needed to run all monads -/
 @[export pantograph_create_core_context]
-def createCoreContext (options: Array String): IO Core.Context := do
-  let options? ← options.foldlM setOptionFromString' Options.empty |>.run
+def createCoreContext (options: Array String): IO Lean.Core.Context := do
+  let options? ← options.foldlM Lean.setOptionFromString' Lean.Options.empty |>.run
   let options ← match options? with
     | .ok options => pure options
     | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
   return {
-    currNamespace := Name.str .anonymous "Aniva"
+    currNamespace := Lean.Name.str .anonymous "Aniva"
     openDecls := [],     -- No 'open' directives needed
     fileName := "<Pantograph>",
     fileMap := { source := "", positions := #[0] },
@@ -69,121 +69,113 @@ def createCoreContext (options: Array String): IO Core.Context := do
 
 /-- Creates a Core.State object needed to run all monads -/
 @[export pantograph_create_core_state]
-def createCoreState (imports: Array String): IO Core.State := do
+def createCoreState (imports: Array String): IO Lean.Core.State := do
   let env ← Lean.importModules
     (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
     (opts := {})
     (trustLevel := 1)
   return { env := env }
 
+@[export pantograph_env_catalog_m]
+def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
+  Environment.catalog ({}: Protocol.EnvCatalog)
+
+@[export pantograph_mk_options]
+def mkOptions
+  (printJsonPretty: Bool)
+  (printExprPretty: Bool)
+  (printExprAST: Bool)
+  (noRepeat: Bool)
+  (printAuxDecls: Bool)
+  (printImplementationDetailHyps: Bool)
+  : Protocol.Options := {
+    printJsonPretty,
+    printExprPretty,
+    printExprAST,
+    noRepeat,
+    printAuxDecls,
+    printImplementationDetailHyps,
+  }
+
+@[export pantograph_env_inspect_m]
+def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
+    Lean.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) :=
+    Lean.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
-    | .error str => return .error $ errorI "parsing" str
-    | .ok syn => pure syn
-  match ← elabType syn with
-  | .error str => return .error $ errorI "elab" str
-  | .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
-    | .none => pure $ .none
-    | .some (.ok t) => pure $ .some t
-    | .some (.error e) => return .error e
-  let syn ← match parseTerm env expr with
+def exprParse (s: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
+  let env ← Lean.MonadEnv.getEnv
+  let syn ← match syntax_from_str env s with
     | .error str => return .error $ errorI "parsing" str
     | .ok syn => pure syn
-  match ← elabTerm syn expectedType? with
+  match ← syntax_to_expr syn with
   | .error str => return .error $ errorI "elab" str
-  | .ok expr => return .ok (← instantiateMVars expr)
+  | .ok expr => return .ok expr
 
 @[export pantograph_expr_echo_m]
-def exprEcho (expr: String) (expectedType?: Option String := .none) (levels: Array String := #[])  (options: @&Protocol.Options := {}):
-    CoreM (Protocol.CR Protocol.ExprEchoResult) :=
-  runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
-    let expr ← match ← parseElabExpr expr expectedType? with
+def exprEcho (expr: String) (options: @&Protocol.Options):
+    Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
+  let termElabM: Lean.Elab.TermElabM _ := do
+    let expr ← match ← exprParse expr with
       | .error e => return .error e
       | .ok expr => pure expr
     try
-      let type ← unfoldAuxLemmas (← Meta.inferType expr)
+      let type ← Lean.Meta.inferType expr
       return .ok {
-          type := (← serializeExpression options type),
-          expr := (← serializeExpression options expr)
+          type := (← serialize_expression options type),
+          expr := (← serialize_expression options expr)
       }
     catch exception =>
       return .error $ errorI "typing" (← exception.toMessageData.toString)
+  runTermElabM termElabM
 
 @[export pantograph_goal_start_expr_m]
-def goalStartExpr (expr: String) (levels: Array String): CoreM (Protocol.CR GoalState) :=
-  runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
-    let expr ← match ← parseElabType expr with
+def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
+  let termElabM: Lean.Elab.TermElabM _ := do
+    let expr ← match ← exprParse expr with
       | .error e => return .error e
       | .ok expr => pure $ expr
     return .ok $ ← GoalState.create expr
+  runTermElabM termElabM
+
+@[export pantograph_goal_tactic_m]
+def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult :=
+  runTermElabM <| GoalState.execute state goalId tactic
+
+@[export pantograph_goal_try_assign_m]
+def goalTryAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult :=
+  runTermElabM <| GoalState.tryAssign state goalId expr
+
+@[export pantograph_goal_continue]
+def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
+  target.continue branch
 
 @[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_serialize_m]
-def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
+def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
   runMetaM <| state.serializeGoals (parent := .none) options
 
 @[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
-  runMetaM do
+def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do
+  let metaM := do
     state.restoreMetaM
     return {
-      root? := ← state.rootExpr?.mapM (λ expr =>
-        state.withRootContext do
-          serializeExpression options (← instantiateAll expr)),
-      parent? := ← state.parentExpr?.mapM (λ expr =>
-        state.withParentContext do
-          serializeExpression options (← instantiateAll expr)),
+      root? := ← state.rootExpr?.mapM (λ expr => do
+        serialize_expression options (← unfoldAuxLemmas expr)),
+      parent? := ← state.parentExpr?.mapM (λ expr => do
+        serialize_expression options (← unfoldAuxLemmas expr)),
     }
+  runMetaM metaM
 
-@[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

Pantograph/Protocol.lean

@@ -18,7 +18,6 @@ structure Options where
   printExprPretty: Bool    := true
   -- When enabled, print the raw AST of expressions
   printExprAST: Bool       := false
-  printDependentMVars: Bool := false
   -- When enabled, the types and values of persistent variables in a goal
   -- are not shown unless they are new to the proof step. Reduces overhead.
   -- NOTE: that this assumes the type and assignment of variables can never change.
@@ -27,8 +26,6 @@ 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
@@ -44,7 +41,6 @@ structure Expression where
   pp?: Option String             := .none
   -- AST structure
   sexp?: Option String           := .none
-  dependentMVars?: Option (Array String) := .none
   deriving Lean.ToJson
 
 structure Variable where
@@ -53,7 +49,7 @@ structure Variable where
   /-- The name displayed to the user -/
   userName: String
   /-- Does the name contain a dagger -/
-  isInaccessible: Bool := false
+  isInaccessible?: Option Bool := .none
   type?: Option Expression  := .none
   value?: Option Expression := .none
   deriving Lean.ToJson
@@ -102,9 +98,6 @@ structure StatResult where
 -- Return the type of an expression
 structure ExprEcho where
   expr: String
-  type?: Option String
-  -- universe levels
-  levels: Option (Array String) := .none
   deriving Lean.FromJson
 structure ExprEchoResult where
   expr: Expression
@@ -144,20 +137,12 @@ structure ConstructorInfo where
   numParams: Nat
   numFields: Nat
   deriving Lean.ToJson
-
-/-- See `Lean/Declaration.lean` -/
-structure RecursorRule where
-  ctor: String
-  nFields: Nat
-  rhs: Expression
-  deriving Lean.ToJson
 structure RecursorInfo where
   all: Array String
   numParams: Nat
   numIndices: Nat
   numMotives: Nat
   numMinors: Nat
-  rules: Array RecursorRule
   k: Bool
   deriving Lean.ToJson
 structure EnvInspectResult where
@@ -188,22 +173,19 @@ structure OptionsSet where
   printJsonPretty?: Option Bool
   printExprPretty?: Option Bool
   printExprAST?: Option Bool
-  printDependentMVars?: Option Bool
   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.
   expr: Option String     -- Directly parse in an expression
-  -- universe levels
-  levels: Option (Array String) := .none
   copyFrom: Option String -- Copy the type from a theorem in the environment
   deriving Lean.FromJson
 structure GoalStartResult where
@@ -218,14 +200,6 @@ structure GoalTactic where
   -- One of the fields here must be filled
   tactic?: Option String := .none
   expr?: Option String := .none
-  have?: Option String := .none
-  calc?: Option String := .none
-  -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
-  conv?: Option Bool := .none
-
-  -- In case of the `have` tactic, the new free variable name is provided here
-  binderName?: Option String := .none
-
   deriving Lean.FromJson
 structure GoalTacticResult where
   -- The next goal state id. Existence of this field shows success
@@ -280,26 +254,6 @@ 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 α
 

Pantograph/Serial.lean

@@ -1,118 +1,97 @@
 /-
-All serialisation functions;
-This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without
-using `Scope`s.
+All serialisation functions
 -/
 import Lean
-import Pantograph.Condensed
-import Pantograph.Expr
-import Pantograph.Goal
+
 import Pantograph.Protocol
+import Pantograph.Goal
 
 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 : Lean.Expr) : Lean.MetaM Lean.Expr := do
+  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 
 --- Input Functions ---
 
 /-- Read syntax object from string -/
-def parseTerm (env: Environment) (s: String): Except String Syntax :=
+def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
   Parser.runParserCategory
     (env := env)
     (catName := `term)
     (input := s)
     (fileName := "<stdin>")
 
+
 /-- Parse a syntax object. May generate additional metavariables! -/
-def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
+def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
   try
     let expr ← Elab.Term.elabType syn
     return .ok expr
   catch ex => return .error (← ex.toMessageData.toString)
-def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
+def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
   try
-    let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
+    let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none)
     return .ok expr
   catch ex => return .error (← ex.toMessageData.toString)
 
 
 --- Output Functions ---
 
-def typeExprToBound (expr: Expr): MetaM Protocol.BoundExpression := do
+def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := do
   Meta.forallTelescope expr fun arr body => do
     let binders ← arr.mapM fun fvar => do
       return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
     return { binders, target := toString (← Meta.ppExpr body) }
 
-def serializeName (name: Name) (sanitize: Bool := true): String :=
+def name_to_ast (name: Name) (sanitize: Bool := true): String :=
   let internal := name.isInaccessibleUserName || name.hasMacroScopes
   if sanitize && internal then "_"
-  else toString name |> addQuotes
+  else toString name |> enclose_if_escaped
   where
-  addQuotes (n: String) :=
+  enclose_if_escaped (n: String) :=
     let quote := "\""
     if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
 
 /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
-partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
+partial def serialize_sort_level_ast (level: Level) (sanitize: Bool): String :=
   let k := level.getOffset
   let u := level.getLevelOffset
   let u_str := match u with
     | .zero => "0"
     | .succ _ => panic! "getLevelOffset should not return .succ"
     | .max v w =>
-      let v := serializeSortLevel v sanitize
-      let w := serializeSortLevel w sanitize
+      let v := serialize_sort_level_ast v sanitize
+      let w := serialize_sort_level_ast w sanitize
       s!"(:max {v} {w})"
     | .imax v w =>
-      let v := serializeSortLevel v sanitize
-      let w := serializeSortLevel w sanitize
+      let v := serialize_sort_level_ast v sanitize
+      let w := serialize_sort_level_ast w sanitize
       s!"(:imax {v} {w})"
     | .param name =>
-      let name := serializeName name sanitize
+      let name := name_to_ast name sanitize
       s!"{name}"
     | .mvar id =>
-      let name := serializeName id.name sanitize
+      let name := name_to_ast id.name sanitize
       s!"(:mv {name})"
   match k, u with
   | 0, _ => u_str
   | _, .zero => s!"{k}"
   | _, _ => s!"(+ {u_str} {k})"
 
-
 /--
  Completely serializes an expression tree. Json not used due to compactness
-
-A `_` symbol in the AST indicates automatic deductions not present in the original expression.
 -/
-partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
+partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do
   self expr
   where
-  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
+  self (e: Expr): MetaM String :=
     match e with
     | .bvar deBruijnIndex =>
       -- This is very common so the index alone is shown. Literals are handled below.
@@ -120,14 +99,13 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
       -- Lean these are handled using a `#` prefix.
       pure s!"{deBruijnIndex}"
     | .fvar fvarId =>
-      let name := ofName fvarId.name
+      let name := of_name fvarId.name
       pure s!"(:fv {name})"
-    | .mvar mvarId => do
-        let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
-        let name := ofName mvarId.name
-        pure s!"(:{pref} {name})"
+    | .mvar mvarId =>
+      let name := of_name mvarId.name
+      pure s!"(:mv {name})"
     | .sort level =>
-      let level := serializeSortLevel level sanitize
+      let level := serialize_sort_level_ast level sanitize
       pure s!"(:sort {level})"
     | .const declName _ =>
       -- The universe level of the const expression is elided since it should be
@@ -139,20 +117,20 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
       let args := " ".intercalate args
       pure s!"({fn'} {args})"
     | .lam binderName binderType body binderInfo => do
-      let binderName' := ofName binderName
+      let binderName' := of_name binderName
       let binderType' ← self binderType
       let body' ← self body
-      let binderInfo' := binderInfoSexp binderInfo
+      let binderInfo' := binder_info_to_ast binderInfo
       pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
     | .forallE binderName binderType body binderInfo => do
-      let binderName' := ofName binderName
+      let binderName' := of_name binderName
       let binderType' ← self binderType
       let body' ← self body
-      let binderInfo' := binderInfoSexp binderInfo
+      let binderInfo' := binder_info_to_ast binderInfo
       pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
     | .letE name type value body _ => do
       -- Dependent boolean flag diacarded
-      let name' := serializeName name
+      let name' := name_to_ast name
       let type' ← self type
       let value' ← self value
       let body' ← self body
@@ -168,39 +146,36 @@ 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 _ _ _ => do
+    | .proj typeName idx inner => do
       let env ← getEnv
-      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})"
+      let fieldName := getStructureFields env typeName |>.get! idx
+      let projectorName := getProjFnForField? env typeName fieldName |>.get!
+      let e := Expr.app (.const  projectorName []) inner
+      self e
   -- Elides all unhygenic names
-  binderInfoSexp : Lean.BinderInfo → String
+  binder_info_to_ast : Lean.BinderInfo → String
     | .default => ""
     | .implicit => " :implicit"
     | .strictImplicit => " :strictImplicit"
     | .instImplicit => " :instImplicit"
-  ofName (name: Name) := serializeName name sanitize
+  of_name (name: Name) := name_to_ast name sanitize
 
-def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
-  let pp?: Option String ← match options.printExprPretty with
-    | true => pure $ .some $ toString $ ← Meta.ppExpr e
-    | false => pure $ .none
-  let sexp?: Option String ← match options.printExprAST with
-    | true => pure $ .some $ ← serializeExpressionSexp e
-    | false => pure $ .none
-  let dependentMVars? ← match options.printDependentMVars with
-    | true => pure $ .some $ (← Meta.getMVars e).map (λ mvarId => mvarId.name.toString)
-    | false => pure $ .none
+def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
+  let pp := toString (← Meta.ppExpr e)
+  let pp?: Option String := match options.printExprPretty with
+    | true => .some pp
+    | false => .none
+  let sexp: String ← serialize_expression_ast e
+  let sexp?: Option String := match options.printExprAST with
+    | true => .some sexp
+    | false => .none
   return {
     pp?,
     sexp?
-    dependentMVars?,
   }
 
-
 /-- Adapted from ppGoal -/
-def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
+def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
       : MetaM Protocol.Goal := do
   -- Options for printing; See Meta.ppGoal for details
   let showLetValues  := true
@@ -212,41 +187,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
+          name := of_name fvarId.name,
+          userName:= of_name userName.simpMacroScopes,
         }
       | .ldecl _ fvarId userName _ _ _ _ => do
         return {
-          name := ofName fvarId.name,
+          name := of_name 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 ← instantiate type
+        let type ← instantiateMVars type
         return {
-          name := ofName fvarId.name,
-          userName:= ofName userName,
-          isInaccessible := userName.isInaccessibleUserName
-          type? := .some (← serializeExpression options type)
+          name := of_name fvarId.name,
+          userName:= of_name userName,
+          isInaccessible? := .some userName.isInaccessibleUserName
+          type? := .some (← serialize_expression options type)
         }
       | .ldecl _ fvarId userName type val _ _ => do
         let userName := userName.simpMacroScopes
-        let type ← instantiate type
+        let type ← instantiateMVars type
         let value? ← if showLetValues then
-          let val ← instantiate val
-          pure $ .some (← serializeExpression options val)
+          let val ← instantiateMVars val
+          pure $ .some (← serialize_expression options val)
         else
           pure $ .none
         return {
-          name := ofName fvarId.name,
-          userName:= ofName userName,
-          isInaccessible := userName.isInaccessibleUserName
-          type? := .some (← serializeExpression options type)
+          name := of_name fvarId.name,
+          userName:= of_name userName,
+          isInaccessible? := .some userName.isInaccessibleUserName
+          type? := .some (← serialize_expression options type)
           value? := value?
         }
     let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
@@ -262,15 +236,14 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
           | false => ppVar localDecl
         return var::acc
     return {
-      name := ofName goal.name,
-      userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
+      name := of_name goal.name,
+      userName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName),
       isConversion := isLHSGoal? mvarDecl.type |>.isSome,
-      target := (← serializeExpression options (← instantiate mvarDecl.type)),
+      target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
       vars := vars.reverse.toArray
     }
   where
-  instantiate := instantiateAll
-  ofName (n: Name) := serializeName n (sanitize := false)
+  of_name (n: Name) := name_to_ast n (sanitize := false)
 
 protected def GoalState.serializeGoals
       (state: GoalState)
@@ -279,77 +252,64 @@ protected def GoalState.serializeGoals
     MetaM (Array Protocol.Goal):= do
   state.restoreMetaM
   let goals := state.goals.toArray
-  let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
+  let parentDecl? := parent.bind (λ parentState =>
+    let parentGoal := parentState.goals.get! state.parentGoalId
+    parentState.mctx.findDecl? parentGoal)
   goals.mapM fun goal => do
     match state.mctx.findDecl? goal with
     | .some mvarDecl =>
-      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
+      let serializedGoal ← serialize_goal options goal mvarDecl (parentDecl? := parentDecl?)
       pure serializedGoal
     | .none => throwError s!"Metavariable does not exist in context {goal.name}"
 
 /-- Print the metavariables in a readable format -/
-@[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 =>
+protected def GoalState.print (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
       match mctx.decls.find? mvarId with
       | .some decl => printMVar "⊢" mvarId decl
-      | .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' {}
+      | .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}"
+  )
   where
-    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 []
+    printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
+      if options.printContext then
+        decl.lctx.fvarIdToDecl.forM printFVar
       let type ← if options.instantiate
-        then instantiateAll decl.type
+        then instantiateMVars decl.type
         else pure $ 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}"
+      let type_sexp ← serialize_expression_ast 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}"
     userNameToString : Name → String
       | .anonymous => ""
       | other => s!"[{other}]"
-    parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
 
 end Pantograph

Pantograph/Tactic.lean

@@ -1,5 +0,0 @@
-import Pantograph.Tactic.Assign
-import Pantograph.Tactic.Congruence
-import Pantograph.Tactic.MotivatedApply
-import Pantograph.Tactic.NoConfuse
-import Pantograph.Tactic.Prograde

Pantograph/Tactic/Assign.lean

@@ -1,31 +0,0 @@
-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

Pantograph/Tactic/Congruence.lean

@@ -1,98 +0,0 @@
-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

Pantograph/Tactic/MotivatedApply.lean

@@ -1,105 +0,0 @@
-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

Pantograph/Tactic/NoConfuse.lean

@@ -1,22 +0,0 @@
-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

Pantograph/Tactic/Prograde.lean

@@ -1,88 +0,0 @@
-/- 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

Pantograph/Version.lean

@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.2.18"
+def version := "0.2.14"
 
 end Pantograph

README.md

@@ -11,17 +11,11 @@ examine the symbol list of a Lean project for machine learning.
 
 For Nix based workflow, see below.
 
-Install `elan` and `lake`, and run
+Install `elan` and `lake`. Execute
 ``` sh
-lake build
+make build/bin/pantograph
 ```
-This builds the executable in `.lake/build/bin/pantograph`.
-
-To use Pantograph in a project environment, setup the `LEAN_PATH` environment
-variable so it contains the library path of lean libraries. The libraries must
-be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
-the environment might be setup like this:
-
+setup the `LEAN_PATH` environment variable so it contains the library path of lean libraries. The libraries must be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
 ``` sh
 LIB="../lib"
 LIB_MATHLIB="$LIB/mathlib4/lake-packages"
@@ -29,10 +23,7 @@ export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATH
 
 LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
 ```
-The `$LEAN_PATH` executable of any project can be extracted by
-``` sh
-lake env printenv LEAN_PATH
-```
+The provided `flake.nix` has a develop environment with Lean already setup.
 
 ## Executable Usage
 
@@ -80,47 +71,28 @@ where the application of `assumption` should lead to a failure.
 ### Commands
 
 See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
-* `reset`: Delete all cached expressions and proof trees
-* `stat`: Display resource usage
-* `expr.echo {"expr": <expr>, "type": <optional expected type>, ["levels": [<levels>]]}`: Determine the
-  type of an expression and format it.
-* `env.catalog`: Display a list of all safe Lean symbols in the current environment
-* `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
+- `reset`: Delete all cached expressions and proof trees
+- `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
+- `env.catalog`: Display a list of all safe Lean symbols in the current environment
+- `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
   given symbol; If value flag is set, the value is printed or hidden. By default
   only the values of definitions are printed.
-* `options.set { key: value, ... }`: Set one or more options (not Lean options; those
+- `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
-* `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a
-  given goal. The tactic is supplied as additional key-value pairs in one of the following formats:
-  - `{ "tactic": <tactic> }`: Execute an ordinary tactic
-  - `{ "expr": <expr> }`: Assign the given proof term to the current goal
-  - `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
-  - `{ "calc": <expr> }`: Execute one step of a `calc` tactic. Each step must
-    be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set
-    to the previous `rhs`.
-  - `{ "conv": <bool> }`: Enter or exit conversion tactic mode. In the case of
-    exit, the goal id is ignored.
-* `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`:
-  Execute continuation/resumption
-  - `{ "branch": <id> }`: Continue on branch state. The current state must have no goals.
-  - `{ "goals": <names> }`: Resume the given goals
-* `goal.remove {"stateIds": [<id>]}"`: Drop the goal states specified in the list
-* `goal.print {"stateId": <id>}"`: Print a goal state
+- `options.print`: Display the current set of options
+- `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
+- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr": <expr>]}`: Execute a tactic string on a given goal
+- `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`: Continue from a proof state
+- `goal.remove {"stateIds": [<id>]}"`: Remove a bunch of stored goals.
+- `goal.print {"stateId": <id>}"`: Print a goal state
+- `stat`: Display resource usage
 
 ### Errors
 
 When an error pertaining to the execution of a command happens, the returning JSON structure is
 
 ``` json
-{ "error": "type", "desc": "description" }
+{ error: "type", desc: "description" }
 ```
 Common error forms:
 * `command`: Indicates malformed command structure which results from either
@@ -143,23 +115,13 @@ 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.
-
 ### Testing
 
 The tests are based on `LSpec`. To run tests,
 ``` sh
-lake test
-```
-You can run an individual test by specifying a prefix
-
-``` sh
-lake test -- "Tactic/No Confuse"
+make test
 ```
 
 ## Nix based workflow
@@ -170,5 +132,8 @@ requires the presence of `lean-all`.
 
 To run tests:
 ``` sh
-nix flake check
+nix build .#checks.${system}.test
 ```
+
+For example, `${system}` could be `x86_64-linux`. Using `nix develop` drops the
+current session into a development shell with fixed Lean version.

Repl.lean

@@ -1,220 +0,0 @@
-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

Test/Common.lean

@@ -1,7 +1,6 @@
 import Pantograph.Goal
 import Pantograph.Library
 import Pantograph.Protocol
-import Pantograph.Condensed
 import Lean
 import LSpec
 
@@ -9,80 +8,38 @@ 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
-def Goal.devolatilizeVars (goal: Goal): Goal :=
+/-- Set internal names to "" -/
+def Goal.devolatilize (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
-deriving instance DecidableEq, Repr for ExprEchoResult
-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}"
-  | .invalidAction error => s!".invalidAction {error}"
+  | .indexError index => s!".indexError {index}"
 
-namespace Test
-
-def expectationFailure (desc: String) (error: String): LSpec.TestSeq := LSpec.test desc (LSpec.ExpectationFailure "ok _" error)
 def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
 
-def parseFailure (error: String) := expectationFailure "parse" error
-def elabFailure (error: String) := expectationFailure "elab" error
+open Lean
 
-def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array String := #[]): IO LSpec.TestSeq := do
-  let coreContext: Core.Context ← createCoreContext options
+def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq): IO LSpec.TestSeq := do
+  let coreContext: Core.Context ← createCoreContext #[]
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
     return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
@@ -90,66 +47,14 @@ 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 := Condensed.elabContext)
-def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
-  runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
+  termElabM.run' (ctx := {
+    declName? := .none,
+    errToSorry := false,
+  })
 
-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
+def defaultTermElabMContext: Lean.Elab.Term.Context := {
+    declName? := some "_pantograph".toName,
+    errToSorry := false
   }
 
-end Test
-
 end Pantograph

Test/Environment.lean

@@ -11,7 +11,6 @@ open Pantograph
 
 deriving instance DecidableEq, Repr for Protocol.InductInfo
 deriving instance DecidableEq, Repr for Protocol.ConstructorInfo
-deriving instance DecidableEq, Repr for Protocol.RecursorRule
 deriving instance DecidableEq, Repr for Protocol.RecursorInfo
 deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
 
@@ -70,7 +69,6 @@ def test_inspect: IO LSpec.TestSeq := do
       numIndices := 1,
       numMotives := 1,
       numMinors := 1,
-      rules := #[{ ctor := "Eq.refl", nFields := 0, rhs := { pp? := .some "fun {α} a motive refl => refl" } }]
       k := true,
     }),
     ("ForM.rec", ConstantCat.recursor {
@@ -79,7 +77,6 @@ def test_inspect: IO LSpec.TestSeq := do
       numIndices := 0,
       numMotives := 1,
       numMinors := 1,
-      rules := #[{ ctor := "ForM.mk", nFields := 1, rhs := { pp? := .some "fun m γ α motive mk forM => mk forM" } }]
       k := false,
     })
   ]
@@ -97,11 +94,10 @@ def test_inspect: IO LSpec.TestSeq := do
     ) LSpec.TestSeq.done
   runCoreMSeq env inner
 
-def suite: List (String × IO LSpec.TestSeq) :=
-  [
-    ("Catalog", test_catalog),
-    ("Symbol Visibility", test_symbol_visibility),
-    ("Inspect", test_inspect),
-  ]
+def suite: IO LSpec.TestSeq := do
+  return LSpec.group "Environment" $
+    (LSpec.group "Catalog" (← test_catalog)) ++
+    (LSpec.group "Symbol visibility" (← test_symbol_visibility)) ++
+    (LSpec.group "Inspect" (← test_inspect))
 
 end Pantograph.Test.Environment

Test/Integration.lean

@@ -2,188 +2,159 @@
  -/
 import LSpec
 import Pantograph
-import Repl
-import Test.Common
-
 namespace Pantograph.Test.Integration
 open Pantograph
 
-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_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
 
-abbrev Test := List (MainM LSpec.TestSeq)
+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
 
-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" },
-       expr := { pp? := .some "fun {α} => List α" }
-     }: Protocol.ExprEchoResult)),
-  ]
-
-def test_option_modify : Test :=
+def test_option_modify : IO LSpec.TestSeq :=
   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 := {}
-  [
-    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),
+  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))
   ]
-def test_malformed_command : Test :=
+def test_malformed_command : IO LSpec.TestSeq :=
   let invalid := "invalid"
-  [
-    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")
+  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))
   ]
-def test_tactic : Test :=
+def test_tactic : IO LSpec.TestSeq :=
   let goal1: Protocol.Goal := {
-    name := "_uniq.11",
+    name := "_uniq.10",
     target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
-    vars := #[{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}],
+    vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
   }
   let goal2: Protocol.Goal := {
-    name := "_uniq.17",
+    name := "_uniq.13",
     target := { pp? := .some "x ∨ y → y ∨ x" },
     vars := #[
-      { name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }},
-      { name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }}
+      { name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
+      { name := "_uniq.12", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
     ],
   }
-  [
-    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),
+  subroutine_runner [
+    subroutine_step "goal.start"
+      [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
+     (Lean.toJson ({stateId := 0, root := "_uniq.8"}:
+      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.11 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))
   ]
 
-def test_env_add_inspect : Test :=
+def test_env : IO LSpec.TestSeq :=
   let name1 := "Pantograph.mystery"
   let name2 := "Pantograph.mystery2"
-  [
-    step "env.add"
+  subroutine_runner [
+    subroutine_step "env.add"
       [
         ("name", .str name1),
         ("type", .str "Prop → Prop → Prop"),
         ("value", .str "λ (a b: Prop) => Or a b"),
         ("isTheorem", .bool false)
       ]
-     ({}: Protocol.EnvAddResult),
-    step "env.inspect" [("name", .str name1)]
-     ({
+     (Lean.toJson ({}: Protocol.EnvAddResult)),
+    subroutine_step "env.inspect"
+      [("name", .str name1)]
+     (Lean.toJson ({
        value? := .some { pp? := .some "fun a b => a ∨ b" },
        type := { pp? := .some "Prop → Prop → Prop" },
      }:
-      Protocol.EnvInspectResult),
-    step "env.add"
+      Protocol.EnvInspectResult)),
+    subroutine_step "env.add"
       [
         ("name", .str name2),
         ("type", .str "Nat → Int"),
         ("value", .str "λ (a: Nat) => a + 1"),
         ("isTheorem", .bool false)
       ]
-     ({}: Protocol.EnvAddResult),
-    step "env.inspect" [("name", .str name2)]
-     ({
+     (Lean.toJson ({}: Protocol.EnvAddResult)),
+    subroutine_step "env.inspect"
+      [("name", .str name2)]
+     (Lean.toJson ({
        value? := .some { pp? := .some "fun a => ↑a + 1" },
        type := { pp? := .some "Nat → Int" },
      }:
-      Protocol.EnvInspectResult)
+      Protocol.EnvInspectResult))
   ]
 
-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: IO LSpec.TestSeq := do
 
-
-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))
+  return LSpec.group "Integration" $
+    (LSpec.group "Option modify" (← test_option_modify)) ++
+    (LSpec.group "Malformed command" (← test_malformed_command)) ++
+    (LSpec.group "Tactic" (← test_tactic)) ++
+    (LSpec.group "Env" (← test_env))
 
 
 end Pantograph.Test.Integration

Test/Library.lean

@@ -1,38 +0,0 @@
-import LSpec
-import Lean
-import Pantograph.Library
-import Test.Common
-
-open Lean
-open Pantograph
-
-namespace Pantograph.Test.Library
-
-def test_expr_echo (env: Environment): IO LSpec.TestSeq := do
-  let inner: CoreM LSpec.TestSeq := do
-    let prop_and_proof := "⟨∀ (x: Prop), x → x, λ (x: Prop) (h: x) => h⟩"
-    let tests := LSpec.TestSeq.done
-    let echoResult ← exprEcho prop_and_proof (options := {})
-    let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
-      type := { pp? := "?m.2" }, expr := { pp? := "?m.3" }
-    }))
-    let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
-    let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
-      type := {
-        pp? := "(p : Prop) ×' p",
-        sexp? := "((:c PSigma) (:sort 0) (:lambda p (:sort 0) 0))",
-      },
-      expr := {
-        pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩",
-        sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall _ 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))",
-      }
-    }))
-    return tests
-  runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner
-
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
-  [
-    ("expr_echo", test_expr_echo env),
-  ]
-
-end Pantograph.Test.Library

Test/Main.lean

@@ -1,58 +1,21 @@
 import LSpec
 import Test.Environment
-import Test.Integration
-import Test.Library
 import Test.Metavar
+import Test.Integration
 import Test.Proofs
 import Test.Serial
-import Test.Tactic
-
--- Test running infrastructure
-
-namespace Pantograph.Test
-
-def addPrefix (pref: String) (tests: List (String × α)): List (String  × α) :=
-  tests.map (λ (name, x) => (pref ++ "/" ++ name, x))
-
-/-- Runs test in parallel. Filters test name if given -/
-def runTestGroup (filter: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
-  let tests: List (String × IO LSpec.TestSeq) := match filter with
-    | .some filter => tests.filter (λ (name, _) => filter.isPrefixOf name)
-    | .none => tests
-  let tasks: List (String × Task _) ← tests.mapM (λ (name, task) => do
-    return (name, ← EIO.asTask task))
-  let all := tasks.foldl (λ acc (name, task) =>
-    let v: Except IO.Error LSpec.TestSeq := Task.get task
-    match v with
-    | .ok case => acc ++ (LSpec.group name case)
-    | .error e => acc ++ (expectationFailure name e.toString)
-    ) LSpec.TestSeq.done
-  return all
-
-end Pantograph.Test
 
 open Pantograph.Test
 
-/-- Main entry of tests; Provide an argument to filter tests by prefix -/
-def main (args: List String) := do
-  let name_filter := args.head?
+def main := do
   Lean.initSearchPath (← Lean.findSysroot)
-  let env_default: Lean.Environment ← Lean.importModules
-    (imports := #[`Init])
-    (opts := {})
-    (trustLevel := 1)
 
-  let suites: List (String × List (String × IO LSpec.TestSeq)) := [
-    ("Environment", Environment.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 suites := [
+    Metavar.suite,
+    Integration.suite,
+    Proofs.suite,
+    Serial.suite,
+    Environment.suite
   ]
-  let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
-  LSpec.lspecIO (← runTestGroup name_filter tests)
+  let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
+  LSpec.lspecIO $ all

Test/Metavar.lean

@@ -8,42 +8,21 @@ namespace Pantograph.Test.Metavar
 open Pantograph
 open Lean
 
-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
 
 def addTest (test: LSpec.TestSeq): TestM Unit := do
   set $ (← get) ++ test
 
--- Tests that all delay assigned mvars are instantiated
-def test_instantiate_mvar: TestM Unit := do
-  let env ← Lean.MonadEnv.getEnv
-  let value := "@Nat.le_trans 2 2 5 (@of_eq_true (@LE.le Nat instLENat 2 2) (@eq_true (@LE.le Nat instLENat 2 2) (@Nat.le_refl 2))) (@of_eq_true (@LE.le Nat instLENat 2 5) (@eq_true_of_decide (@LE.le Nat instLENat 2 5) (@Nat.decLe 2 5) (@Eq.refl Bool Bool.true)))"
-  let syn ← match parseTerm env value with
-    | .ok s => pure $ s
-    | .error e => do
-      addTest $ assertUnreachable e
-      return ()
-  let expr ← match ← elabTerm syn with
-    | .ok expr => pure $ expr
-    | .error e => do
-      addTest $ assertUnreachable e
-      return ()
-  let t ← Lean.Meta.inferType expr
-  addTest $ LSpec.check "typing" ((toString (← serializeExpressionSexp t)) =
-    "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))")
-  return ()
-
-
-
 def startProof (expr: String): TestM (Option GoalState) := do
   let env ← Lean.MonadEnv.getEnv
-  let syn? := parseTerm env expr
+  let syn? := syntax_from_str env expr
   addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
   match syn? with
   | .error error =>
     IO.println error
     return Option.none
   | .ok syn =>
-    let expr? ← elabType syn
+    let expr? ← syntax_to_expr_type syn
     addTest $ LSpec.check s!"Elaborating" expr?.isOk
     match expr? with
     | .error error =>
@@ -60,13 +39,14 @@ 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 := Condensed.elabContext)
+  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
   let coreM := metaM.run'
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
@@ -83,7 +63,7 @@ def test_m_couple: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -92,7 +72,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.tacticOn (goalId := 2) (tactic := "exact 3") with
+  let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -115,18 +95,14 @@ def test_m_couple_simp: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let serializedState1 ← state1.serializeGoals (options := { ← read with printDependentMVars := true })
-  addTest $ LSpec.check "apply Nat.le_trans" (serializedState1.map (·.target.pp?) =
+  addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
-  addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) =
-    #[#["_uniq.38"], #["_uniq.38"], #[]])
-
-  let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
+  let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 2") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -140,7 +116,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.tacticOn (goalId := 0) (tactic := "simp") with
+  let state3 ← match ← state1b.execute (goalId := 0) (tactic := "simp") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -150,7 +126,7 @@ def test_m_couple_simp: TestM Unit := do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  let state5 ← match ← state4.tacticOn (goalId := 0) (tactic := "simp") with
+  let state5 ← match ← state4.execute (goalId := 0) (tactic := "simp") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -164,9 +140,8 @@ def test_m_couple_simp: TestM Unit := do
       return ()
   let rootStr: String := toString (← Lean.Meta.ppExpr root)
   addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
-  let unfoldedRoot ←  unfoldAuxLemmas root
-  addTest $ LSpec.check "(5 root)" ((toString (← Lean.Meta.ppExpr unfoldedRoot)) =
-    "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
+  let rootStr: String := toString (← Lean.Meta.ppExpr (← unfoldAuxLemmas root))
+  addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
   return ()
 
 def test_proposition_generation: TestM Unit := do
@@ -177,7 +152,7 @@ def test_proposition_generation: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply PSigma.mk") with
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply PSigma.mk") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -191,22 +166,21 @@ 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 (state1.get! 0) (expr := "λ (x: Nat) => _") with
+  let state2 ← match ← state1.tryAssign (goalId := 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 "?m.29 x"])
+    #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"])
   addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
 
-  let assign := "Eq.refl x"
-  let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := assign) with
+  let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
+  addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[])
 
   addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
@@ -220,7 +194,7 @@ def test_partial_continuation: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -228,7 +202,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.tacticOn (goalId := 2) (tactic := "apply Nat.succ") with
+  let state2 ← match ← state1.execute (goalId := 2) (tactic := "apply Nat.succ") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -249,8 +223,8 @@ def test_partial_continuation: TestM Unit := do
 
   -- Roundtrip
   --let coupled_goals := coupled_goals.map (λ g =>
-  --  { name := str_to_name $ serializeName g.name (sanitize := false)})
-  let coupled_goals := coupled_goals.map (λ g => serializeName g.name (sanitize := false))
+  --  { name := str_to_name $ name_to_ast g.name (sanitize := false)})
+  let coupled_goals := coupled_goals.map (λ g => name_to_ast g.name (sanitize := false))
   let coupled_goals := coupled_goals.map (λ g => { name := g.toName })
   let state1b ← match state2.resume (goals := coupled_goals) with
     | .error msg => do
@@ -263,7 +237,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 [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope")
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope")
   | .ok _ => addTest $ assertUnreachable "(continuation failure)"
   -- Continuation should fail if some goals have not been solved
   match state2.continue state1 with
@@ -272,14 +246,22 @@ def test_partial_continuation: TestM Unit := do
   return ()
 
 
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+def suite: IO LSpec.TestSeq := do
+  let env: Lean.Environment ← Lean.importModules
+    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
   let tests := [
-    ("Instantiate", test_instantiate_mvar),
     ("2 < 5", test_m_couple),
     ("2 < 5", test_m_couple_simp),
     ("Proposition Generation", test_proposition_generation),
     ("Partial Continuation", test_partial_continuation)
   ]
-  tests.map (fun (name, test) => (name, proofRunner env test))
+  let tests ← tests.foldlM (fun acc tests => do
+    let (name, tests) := tests
+    let tests ← proofRunner env tests
+    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
+
+  return LSpec.group "Metavar" tests
 
 end Pantograph.Test.Metavar

Test/Proofs.lean

@@ -14,7 +14,7 @@ inductive Start where
   | copy (name: String) -- Start from some name in the environment
   | expr (expr: String) -- Start from some expression
 
-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
 
 def addTest (test: LSpec.TestSeq): TestM Unit := do
   set $ (← get) ++ test
@@ -32,14 +32,14 @@ def startProof (start: Start): TestM (Option GoalState) := do
     | .none =>
       return Option.none
   | .expr expr =>
-    let syn? := parseTerm env expr
+    let syn? := syntax_from_str env expr
     addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
     match syn? with
     | .error error =>
       IO.println error
       return Option.none
     | .ok syn =>
-      let expr? ← elabType syn
+      let expr? ← syntax_to_expr_type syn
       addTest $ LSpec.check s!"Elaborating" expr?.isOk
       match expr? with
       | .error error =>
@@ -49,32 +49,21 @@ def startProof (start: Start): TestM (Option GoalState) := do
         let goal ← GoalState.create (expr := expr)
         return Option.some 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 :=
+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 := Condensed.elabContext)
+  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
   let coreM := metaM.run'
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
@@ -82,32 +71,11 @@ 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
   rw [Nat.add_comm]
-def test_nat_add_comm (manual: Bool): TestM Unit := do
+def proof_nat_add_comm (manual: Bool): TestM Unit := do
   let state? ← startProof <| match manual with
     | false => .copy "Nat.add_comm"
     | true => .expr "∀ (a b: Nat), a + b = b + a"
@@ -118,7 +86,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.tacticOn 0 "intro n m" with
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n m") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -126,13 +94,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.tacticOn 0 "assumption" with
+  match ← state1.execute (goalId := 0) (tactic := "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.tacticOn 0 "rw [Nat.add_comm]" with
+  let state2 ← match ← state1.execute (goalId := 0) (tactic := "rw [Nat.add_comm]") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -140,7 +108,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
   addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty
 
   return ()
-def test_delta_variable: TestM Unit := do
+def proof_delta_variable: TestM Unit := do
   let options: Protocol.Options := { noRepeat := true }
   let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a"
   addTest $ LSpec.check "Start goal" state?.isSome
@@ -150,14 +118,14 @@ def test_delta_variable: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with
+  let state1 ← match ← state0.execute (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.tacticOn (goalId := 0) (tactic := "intro m") with
+  let state2 ← match ← state1.execute (goalId := 0) (tactic := "intro m") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -173,6 +141,7 @@ 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
     }
 
@@ -180,7 +149,7 @@ example (w x y z : Nat) (p : Nat → Prop)
         (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
   simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
   assumption
-def test_arith: TestM Unit := do
+def proof_arith: TestM Unit := do
   let state? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
   let state0 ← match state? with
     | .some state => pure state
@@ -188,28 +157,26 @@ def test_arith: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let tactic := "intros"
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intros") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check tactic (state1.goals.length = 1)
+  addTest $ LSpec.check "intros" (state1.goals.length = 1)
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
-  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
+  let state2 ← match ← state1.execute (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
       return ()
   addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
-  let tactic := "assumption"
-  let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
+  let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.test tactic state3.goals.isEmpty
+  addTest $ LSpec.test "assumption" state3.goals.isEmpty
   addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
   return ()
 
@@ -228,7 +195,7 @@ example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
     assumption
   . apply Or.inl
     assumption
-def test_or_comm: TestM Unit := do
+def proof_or_comm: TestM Unit := do
   let state? ← startProof (.expr "∀ (p q: Prop), p ∨ q → q ∨ p")
   let state0 ← match state? with
     | .some state => pure state
@@ -238,82 +205,54 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
   addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
 
-  let tactic := "intro p q h"
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  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 "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"])
   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.tacticOn (goalId := 0) (tactic := tactic) with
+  let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+  addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[branchGoal "inl" "p", branchGoal "inr" "q"])
-  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 parent)" state2.parentExpr?.isSome
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
 
-  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}))"
+  let state2parent ← serialize_expression_ast state2.parentExpr?.get! (sanitize := false)
+  -- This is due to delayed assignment
   addTest $ LSpec.test "(2 parent)" (state2parent ==
-    s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")
+    "((:mv _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
 
-  let state3_1 ← match ← state2.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
+  let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  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))")
+  let state3_1parent ← serialize_expression_ast 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))")
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
-  let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
+  let state4_1 ← match ← state3_1.execute (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 ← instantiateAll state4_1.parentExpr?.get!
-  addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
+  let state4_1parent ← serialize_expression_ast state4_1.parentExpr?.get! (sanitize := false)
+  addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)")
   addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
-  let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
+  let state3_2 ← match ← state2.execute (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.tacticOn (goalId := 0) (tactic := "assumption") with
+  let state4_2 ← match ← state3_2.execute (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -327,13 +266,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.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
+  let state3_1 ← match ← state2b.execute (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.tacticOn (goalId := 0) (tactic := "assumption") with
+  let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -348,377 +287,30 @@ def test_or_comm: TestM Unit := do
       userName? := .some caseName,
       target := { pp? := .some "q ∨ p" },
       vars := #[
-        { userName := "p", type? := .some typeProp },
-        { userName := "q", type? := .some typeProp },
-        { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible := true }
+        { 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 }
       ]
     }
 
-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 =>
-    lhs
-    congr
-    . rw [Nat.add_comm]
-    . rfl
-  exact h
 
-def test_conv: TestM Unit := do
-  let state? ← startProof (.expr "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-
-  let tactic := "intro a b c1 c2 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 (options := ← read)).map (·.devolatilize) =
-    #[interiorGoal [] "a + b + c1 = b + a + c2"])
-
-  let state2 ← match ← state1.conv (state1.get! 0) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
-
-  let convTactic := "rhs"
-  let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  {convTactic} (discard)" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "b + a + c2" with isConversion := true }])
-
-  let convTactic := "lhs"
-  let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  {convTactic}" ((← state3L.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "a + b + c1" with isConversion := true }])
-
-  let convTactic := "congr"
-  let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  {convTactic}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      { interiorGoal [] "a + b" with isConversion := true, userName? := .some "a" },
-      { interiorGoal [] "c1" with isConversion := true, userName? := .some "a" }
-    ])
-
-  let convTactic := "rw [Nat.add_comm]"
-  let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  · {convTactic}" ((← state5_1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
-
-  let convTactic := "rfl"
-  let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"    {convTactic}" ((← state6_1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  let state4_1 ← match state6_1.continue state4 with
-    | .ok state => pure state
-    | .error e => do
-      addTest $ expectationFailure "continue" e
-      return ()
-
-  let convTactic := "rfl"
-  let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  · {convTactic}" ((← state6.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  let state1_1 ← match ← state6.convExit with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-
-  let tactic := "exact h"
-  let stateF ← match ← state1_1.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)).map (·.devolatilize) =
-    #[])
-
-  where
-    h := "b + a + c1 = b + a + c2"
-    interiorGoal (free: List (String × String)) (target: String) :=
-      let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free
-      buildGoal free target
-
-example : ∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d := by
-  intro a b c d h1 h2
-  calc a + b = b + c := by apply h1
-    _ = c + d := by apply h2
-
-def test_calc: TestM Unit := do
-  let state? ← startProof (.expr "∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-  let tactic := "intro a b c d h1 h2"
-  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 [] "a + b = c + d"])
-  let pred := "a + b = b + c"
-  let state2 ← match ← state1.tryCalc (state1.get! 0) (pred := pred) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      interiorGoal [] "a + b = b + c" (.some "calc"),
-      interiorGoal [] "b + c = c + d"
-    ])
-  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.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  let state3 ← match state2m.continue state2 with
-    | .ok state => pure state
-    | .error e => do
-      addTest $ expectationFailure "continue" e
-      return ()
-  let pred := "_ = c + d"
-  let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"calc {pred} := _" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      interiorGoal [] "b + c = c + d" (.some "calc")
-    ])
-  addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
-  let tactic := "apply h2"
-  let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
-  where
-    interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
-      let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
-        ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
-      buildGoal free target userName?
-
-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 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 ()
-  addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
-    #[
-      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")
-    ])
-
-  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 ((← state3b.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-  let state2b ← match state3b.continue state2 with
-    | .ok state => pure state
-    | .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 ()
-  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.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) :=
+def suite: IO LSpec.TestSeq := do
+  let env: Lean.Environment ← Lean.importModules
+    (imports := #[{ module := "Init".toName, runtimeOnly := false}])
+    (opts := {})
+    (trustLevel := 1)
   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),
-    ("conv", test_conv),
-    ("calc", test_calc),
-    ("Nat.zero_add", test_nat_zero_add),
-    ("Nat.zero_add alt", test_nat_zero_add_alt),
+    ("Nat.add_comm", proof_nat_add_comm false),
+    ("Nat.add_comm manual", proof_nat_add_comm true),
+    ("Nat.add_comm delta", proof_delta_variable),
+    ("arithmetic", proof_arith),
+    ("Or.comm", proof_or_comm)
   ]
-  tests.map (fun (name, test) => (name, proofRunner env test))
-
+  let tests ← tests.foldlM (fun acc tests => do
+    let (name, tests) := tests
+    let tests ← proofRunner env tests
+    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
 
+  return LSpec.group "Proofs" tests
 
 end Pantograph.Test.Proofs

Test/Serial.lean

@@ -10,24 +10,25 @@ open Pantograph
 
 deriving instance Repr, DecidableEq for Protocol.BoundExpression
 
-def test_serializeName: LSpec.TestSeq :=
+def test_name_to_ast: LSpec.TestSeq :=
   let quote := "\""
   let escape := "\\"
-  LSpec.test "a.b.1" (serializeName (Name.num (.str (.str .anonymous "a") "b") 1) = "a.b.1") ++
-  LSpec.test "seg.«a.b»" (serializeName (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}") ++
+  LSpec.test "a.b.1" (name_to_ast (Name.num (.str (.str .anonymous "a") "b") 1) = "a.b.1") ++
+  LSpec.test "seg.«a.b»" (name_to_ast (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}") ++
   -- Pathological test case
-  LSpec.test s!"«̈{escape}{quote}»" (serializeName (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«{escape}{quote}»{quote}")
+  LSpec.test s!"«̈{escape}{quote}»" (name_to_ast (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«{escape}{quote}»{quote}")
 
 def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
   let entries: List (Name × Protocol.BoundExpression) := [
     ("Nat.add_comm".toName, { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }),
     ("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "n.succ ≤ m")], target := "n ≤ m" })
   ]
-  runCoreMSeq env $ entries.foldlM (λ suites (symbol, target) => do
+  let coreM: CoreM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
     let env ← MonadEnv.getEnv
     let expr := env.find? symbol |>.get! |>.type
-    let test := LSpec.check symbol.toString ((← typeExprToBound expr) = target)
+    let test := LSpec.check symbol.toString ((← type_expr_to_bound expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
+  runCoreMSeq env coreM
 
 def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × String) := [
@@ -40,70 +41,48 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
     ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
     ("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
   ]
-  runMetaMSeq env $ entries.foldlM (λ suites (symbol, target) => do
+  let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
     let env ← MonadEnv.getEnv
     let expr := env.find? symbol.toName |>.get! |>.type
-    let test := LSpec.check symbol ((← serializeExpressionSexp expr) = target)
+    let test := LSpec.check symbol ((← serialize_expression_ast expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
-
-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))"),
-    ("λ {α: 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
-      let env ← MonadEnv.getEnv
-      let s ← match parseTerm env source with
-        | .ok s => pure s
-        | .error e => return parseFailure e
-      let expr ← match (← elabTerm s) with
-        | .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 := Condensed.elabContext)
-    return LSpec.TestSeq.append suites (← runMetaMSeq env metaM))
-    LSpec.TestSeq.done
+  runMetaMSeq env metaM
 
 def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
-  let entries: List (Expr × String) := [
-    (.lam `p (.sort .zero)
-        (.lam `q (.sort .zero)
-          (.lam `k (mkApp2 (.const `And []) (.bvar 1) (.bvar 0))
-            (.proj `And 1 (.bvar 0))
-            .default)
-        .implicit)
-      .implicit,
-      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :implicit) :implicit)"
-    ),
+  let entries: List (String × 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))")
   ]
-  let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do
+  let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
     let env ← MonadEnv.getEnv
-    let testCaseName := target.take 10
-    let test := LSpec.check   testCaseName ((← serializeExpressionSexp expr) = target)
+    let s := syntax_from_str env source |>.toOption |>.get!
+    let expr := (← syntax_to_expr s) |>.toOption |>.get!
+    let test := LSpec.check source ((← serialize_expression_ast expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
-  runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
+  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
+  runMetaMSeq env metaM
 
 -- Instance parsing
-def test_instance (env: Environment): IO LSpec.TestSeq :=
-  runMetaMSeq env do
+def test_instance (env: Environment): IO LSpec.TestSeq := do
+  let metaM: MetaM LSpec.TestSeq := do
     let env ← MonadEnv.getEnv
     let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y"
-    let s := parseTerm env source |>.toOption |>.get!
-    let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
+    let s := syntax_from_str env source |>.toOption |>.get!
+    let _expr := (← runTermElabMInMeta <| syntax_to_expr s) |>.toOption |>.get!
     return LSpec.TestSeq.done
+  runMetaMSeq env metaM
 
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
-  [
-    ("serializeName", do pure test_serializeName),
-    ("Expression binder", test_expr_to_binder env),
-    ("Sexp from symbol", test_sexp_of_symbol env),
-    ("Sexp from elaborated expr", test_sexp_of_elab env),
-    ("Sexp from expr", test_sexp_of_expr env),
-    ("Instance", test_instance env),
-  ]
+def suite: IO LSpec.TestSeq := do
+  let env: Environment ← importModules
+    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
+
+  return LSpec.group "Serialization" $
+    (LSpec.group "name_to_ast" test_name_to_ast) ++
+    (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
+    (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env)) ++
+    (LSpec.group "Sexp from expr" (← test_sexp_of_expr env)) ++
+    (LSpec.group "Instance" (← test_instance env))
 
 end Pantograph.Test.Serial

Test/Tactic.lean

@@ -1,4 +0,0 @@
-import Test.Tactic.Congruence
-import Test.Tactic.MotivatedApply
-import Test.Tactic.NoConfuse
-import Test.Tactic.Prograde

Test/Tactic/Congruence.lean

@@ -1,88 +0,0 @@
-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

Test/Tactic/MotivatedApply.lean

@@ -1,113 +0,0 @@
-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

Test/Tactic/NoConfuse.lean

@@ -1,72 +0,0 @@
-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

Test/Tactic/Prograde.lean

@@ -1,300 +0,0 @@
-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

flake.lock

@@ -42,16 +42,16 @@
         "nixpkgs-old": "nixpkgs-old"
       },
       "locked": {
-        "lastModified": 1719788866,
-        "narHash": "sha256-kB2cp1XJKODXiuiKp7J5OK+PFP+sOSBE5gdVNOKWCPI=",
+        "lastModified": 1711508550,
+        "narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "3b58e0649156610ce3aeed4f7b5c652340c668d4",
+        "rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
-        "ref": "v4.10.0-rc1",
+        "ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
         "repo": "lean4",
         "type": "github"
       }
@@ -91,16 +91,16 @@
     "lspec": {
       "flake": false,
       "locked": {
-        "lastModified": 1722857503,
-        "narHash": "sha256-F9uaymiw1wTCLrJm4n1Bpk3J8jW6poedQzvnnQlZ6Kw=",
+        "lastModified": 1701971219,
+        "narHash": "sha256-HYDRzkT2UaLDrqKNWesh9C4LJNt0JpW0u68wYVj4Byw=",
         "owner": "lurk-lab",
         "repo": "LSpec",
-        "rev": "8a51034d049c6a229d88dd62f490778a377eec06",
+        "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
         "type": "github"
       },
       "original": {
         "owner": "lurk-lab",
-        "ref": "8a51034d049c6a229d88dd62f490778a377eec06",
+        "ref": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
         "repo": "LSpec",
         "type": "github"
       }

flake.nix

@@ -5,11 +5,11 @@
     nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
     flake-parts.url = "github:hercules-ci/flake-parts";
     lean = {
+      url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
       # Do not follow input's nixpkgs since it could cause build failures
-      url = "github:leanprover/lean4?ref=v4.10.0-rc1";
     };
     lspec = {
-      url = "github:lurk-lab/LSpec?ref=8a51034d049c6a229d88dd62f490778a377eec06";
+      url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
       flake = false;
     };
   };
@@ -37,25 +37,14 @@
       };
       project = leanPkgs.buildLeanPackage {
         name = "Pantograph";
-        roots = [ "Pantograph" ];
-        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+        roots = [ "Main" "Pantograph" ];
+        src = pkgs.lib.cleanSourceWith {
           src = ./.;
           filter = path: type:
             !(pkgs.lib.hasInfix "/Test/" path) &&
             !(pkgs.lib.hasSuffix ".md" 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);
-        });
+            !(pkgs.lib.hasSuffix "Makefile" path);
+        };
       };
       test = leanPkgs.buildLeanPackage {
         name = "Test";
@@ -63,22 +52,18 @@
         # root begins (e.g. `import Test.Environment` and not `import
         # Environment`) and thats where `lakefile.lean` resides.
         roots = [ "Test.Main" ];
-        deps = [ lspecLib repl ];
-        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+        deps = [ lspecLib project ];
+        src = pkgs.lib.cleanSourceWith {
           src = ./.;
           filter = path: type:
             !(pkgs.lib.hasInfix "Pantograph" path);
-        });
+        };
       };
     in rec {
       packages = {
         inherit (leanPkgs) lean lean-all;
-        inherit (project) sharedLib;
-        inherit (repl) executable;
-        default = repl.executable;
-      };
-      legacyPackages = {
-        inherit project leanPkgs;
+        inherit (project) sharedLib executable;
+        default = project.executable;
       };
       checks = {
         test = pkgs.runCommand "test" {

lakefile.lean

@@ -4,16 +4,13 @@ open Lake DSL
 package pantograph
 
 lean_lib Pantograph {
-  roots := #[`Pantograph]
   defaultFacets := #[LeanLib.sharedFacet]
 }
 
-lean_lib Repl {
-}
 @[default_target]
-lean_exe repl {
+lean_exe pantograph {
   root := `Main
-  -- Solves the native symbol not found problem
+  -- Somehow solves the native symbol not found problem
   supportInterpreter := true
 }
 
@@ -21,9 +18,8 @@ require LSpec from git
   "https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
 lean_lib Test {
 }
-@[test_driver]
 lean_exe test {
   root := `Test.Main
-  -- Solves the native symbol not found problem
+  -- Somehow solves the native symbol not found problem
   supportInterpreter := true
 }

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc1
+leanprover/lean4:nightly-2024-03-27