.cabal-sandbox
cabal.sandbox.config
hlint.html
+*.hi
+*.o
*.old
--- /dev/null
+.cabal-sandbox/
+cabal.sandbox.config
+dist/
+Calculus/Lambda/Omega/Explicit/REPL
--- /dev/null
+ GNU GENERAL PUBLIC LICENSE
+ Version 3, 29 June 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <http://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 <http://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
+<http://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
+<http://www.gnu.org/philosophy/why-not-lgpl.html>.
--- /dev/null
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_GHC -fno-warn-tabs #-}
+module Calculus.Abstraction.DeBruijn.Generalized where
+
+import Control.Applicative (Applicative(..))
+import Control.Monad
+import Control.Monad.Trans.Class (MonadTrans(..))
+import Data.Bool (Bool(..))
+import Data.Eq (Eq(..))
+import Data.Foldable (Foldable(..))
+import Data.Function (($), (.))
+import Data.Function (on)
+import Data.Maybe (Maybe(..))
+import Data.Ord (Ord(..), Ordering(..))
+import Data.String (IsString(..))
+import Data.Text (Text)
+import Data.Text.Buildable (Buildable(..))
+import Data.Traversable (Traversable(..))
+import Prelude (Int)
+import Text.Show (Show(..), ShowS, showParen, showString)
+
+-- * Type 'Abstraction'
+-- | 'Abstraction' @bound@ @expr@ @var@:
+-- encodes an 'abstract'-ion
+-- over an expression of type @expr@,
+-- by segretating its variables between:
+--
+-- * /bound variables/ of type: @bound@,
+-- * and /unbound variables/ (aka. /free variables/) of type: @var@.
+--
+-- Note that /unbound variables/ may later themselves be made /bound variables/
+-- of an enclosing 'Abstraction', effectively encoding
+-- /DeBruijn indices/ using Haskell’s /data constructors/,
+-- that is, not like in a /traditional DeBruijn indexing/:
+-- where an integer is used in each /bound variable/
+-- to indicate which one of its enclosing 'Abstraction's is bounding it,
+-- but by the nesting of 'Var_Free' data constructors.
+-- As a side note, this is also different from the /DeBruijn indexing/
+-- encoded at Haskell’s /type level/ by using @GADTs@
+-- (done for instance in https://hackage.haskell.org/package/glambda ).
+--
+-- Moreover, /unbound variables/ are wrapped within a second level of expression
+-- in order to improve the time complexity of /traditional DeBruijn indexing/
+-- when 'unabstract'-ing (aka. /instantiating/)
+-- (see 'Var' and instance 'MonadTrans' of 'Abstraction').
+--
+-- 'Abstraction' enables:
+--
+-- * /locally-nameless/ variables (nameless in 'Var_Bound', named in the deepest 'Var_Free');
+-- * substitution of /bound variables/ in an expression using /DeBruijn indices/
+-- (hence enabling capture-avoiding /β-reduction/
+-- and reducing /α-equivalence/ to a structural equality (==));
+-- * shifting /DeBruijn indices/ within an expression without traversing it
+-- (hence generalizing and speeding up /traditional DeBruijn indices/);
+-- * simultaneous substitution of several /bound variables/
+-- (hence enabling expressions implementing recursive-@let@).
+--
+-- __Ressources:__
+--
+-- * /Bound/, Edward Kmett, 19 August 2013,
+-- https://www.schoolofhaskell.com/user/edwardk/bound
+newtype Abstraction bound expr var
+ = Abstraction (expr (Var bound (expr var)))
+ deriving (Foldable, Functor, Traversable)
+instance (Monad expr, Eq bound, Eq1 expr, Show bound)
+ => Eq1 (Abstraction bound expr) where
+ (==#) = (==#) `on` abstract_normalize
+instance (Monad expr, Eq bound, Eq1 expr, Eq var, Show var, Show bound)
+ => Eq (Abstraction bound expr var) where
+ (==) = (==#)
+instance (Monad expr, Ord bound, Ord1 expr, Show bound)
+ => Ord1 (Abstraction bound expr) where
+ compare1 = compare1 `on` abstract_normalize
+instance (Monad expr, Ord bound, Ord1 expr, Ord var, Show var, Show bound)
+ => Ord (Abstraction bound expr var) where
+ compare = compare1
+instance (Functor expr, Show bound, Show1 expr)
+ => Show1 (Abstraction bound expr) where
+ showsPrec1 d (Abstraction e) =
+ showParen (d > 10) $
+ showString "Abstraction " .
+ showsPrec1 11 ((Lift1 `fmap`) `fmap` e)
+instance (Functor expr, Show bound, Show1 expr, Show var)
+ => Show (Abstraction bound expr var) where
+ showsPrec = showsPrec1
+instance Monad expr => Applicative (Abstraction bound expr) where
+ pure = return
+ (<*>) = ap
+-- | A 'Monad' instance capturing the notion of /variable substitution/,
+-- used by 'unabstract' to decrement the /DeBruijn indices/.
+instance Monad expr => Monad (Abstraction bound expr) where
+ return = Abstraction . return . Var_Free . return
+ Abstraction expr >>= f = Abstraction $ expr >>= \var ->
+ case var of
+ Var_Bound bound -> return (Var_Bound bound)
+ Var_Free e -> e >>= (\(Abstraction ex) -> ex) . f
+instance MonadTrans (Abstraction bound) where
+ lift = Abstraction . return . Var_Free
+-- | 'Monad_Module_Left' instance capturing the notion
+-- of /variable substitution/ with /capture-avoiding/.
+instance Monad_Module_Left (Abstraction bound) where
+ l >>>= f = l >>= lift . f
+
+-- | WARNING: 'abstract' 'fmap'-s the given expression,
+-- thus repetitive 'abstract'-ings have a quadratic time-complexity.
+abstract
+ :: Monad expr
+ => (var -> Maybe bound)
+ -> expr var
+ -> Abstraction bound expr var
+abstract f = Abstraction . fmap (\var ->
+ case f var of
+ Nothing -> Var_Free (return var)
+ Just b -> Var_Bound b)
+
+unabstract
+ :: Monad expr
+ => (bound -> expr var)
+ -> Abstraction bound expr var
+ -> expr var
+unabstract unbound (Abstraction ex) = ex >>= \var ->
+ case var of
+ Var_Bound b -> unbound b
+ Var_Free v -> v
+
+-- | @'abstract_normalize'@ normalize
+-- the possible placements of 'Var_Free' in 'Abstraction'
+-- by moving them all to the leaves of the 'abstract'-ed expression.
+--
+-- This gives /traditional DeBruijn indices/ for /bound variables/.
+abstract_normalize
+ :: Monad expr
+ => Abstraction bound expr var
+ -> expr (Var bound var)
+abstract_normalize (Abstraction expr) = expr >>= \var ->
+ case var of
+ Var_Bound bound -> return $ Var_Bound bound
+ Var_Free e -> Var_Free `fmap`{-on var of expr-} e
+
+-- | Convert from /traditional DeBruijn indices/
+-- to /generalized DeBruijn indices/,
+-- by wrapping all the leaves within the 'Monad'
+-- of the given expression.
+--
+-- This requires a full traversal of the given expression.
+abstract_generalize
+ :: Monad expr
+ => expr (Var bound var)
+ -> Abstraction bound expr var
+abstract_generalize = Abstraction .
+ ((return{-of expr-}
+ `fmap`{-on var of Var-})
+ `fmap`{-on var of expr-})
+
+-- ** Class 'Monad_Module_Left'
+-- | Like ('>>=') but whose 'Monad' is within a wrapping type @left@
+-- (aka. /left module over a monad/).
+--
+-- __Laws:__
+--
+-- ('>>>=') should satisfy the following equations
+-- in order to be used within a 'Monad' instance:
+--
+-- @
+-- ('>>>=' 'return') = id
+-- ('>>>=' (('>>=' g) . f)) = ('>>>=' f) . ('>>>=' g)
+-- @
+--
+-- If @left@ has a 'MonadTrans' instance, then:
+--
+-- @
+-- ('>>>=' f) = ('>>=' ('lift' . f))
+-- @
+--
+-- which implies the above equations,
+-- see 'MonadTrans' instance of ('Abstraction' @bound@).
+--
+-- __Uses:__
+--
+-- * Useful for expression constructors containing 'Abstraction' data.
+--
+-- __Ressources:__
+--
+-- * André Hirschowitz, Marco Maggesi, /Modules over monads and initial semantics/.
+-- Information and Computation 208 (2010), pp. 545-564,
+-- http://www.sciencedirect.com/science/article/pii/S0890540109002405
+class Monad_Module_Left left where
+ (>>>=) :: Monad expr
+ => left expr var
+ -> (var -> expr bound)
+ -> left expr bound
+infixl 1 >>>=
+
+-- ** Type 'Var'
+
+-- | 'Var' @bound@ @var@: a variable segregating between:
+--
+-- * 'Var_Bound', containing data of type @bound@,
+-- considered /bound/ by the first enclosing 'Abstraction',
+-- hence playing the role of a @Zero@ in /DeBruijn indexing/ terminology.
+--
+-- Note that the presence of this @bound@ enables the substitution
+-- of a 'Var_Bound' by different values,
+-- which is used to keep the 'Var_Name' given in the source code,
+-- (note that it could also be used to implement a @recursive-let@).
+--
+-- * 'Var_Free', containing data of type @var@,
+-- considered /free/ with respect to the first enclosing 'Abstraction',
+-- hence playing the role of a @Succ@ in /DeBruijn indexing/ terminology.
+--
+-- Note that @var@ is not constrained to be itself a 'Var',
+-- this in order to make it possible in 'Abstraction'
+-- to insert @expr@ in between the @Succ@ nesting,
+-- which optimizes the /DeBruijn indexing/ when 'unabstract'-ing,
+-- by avoiding to traverse ('fmap') an @expr@ to @Succ@ its variables
+-- (see instance 'MonadTrans' for 'Abstraction').
+data Var bound var
+ = Var_Bound bound -- ^ @Zero@
+ | Var_Free var -- ^ @Succ@
+ deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
+instance (Buildable bound, Buildable var) => Buildable (Var bound var) where
+ build var =
+ case var of
+ Var_Bound b -> build b
+ Var_Free f -> build f
+
+-- | A convenient operator for 'abstract'-ing.
+(=?) :: Eq a => a -> a -> Maybe (Suggest a)
+(=?) x y = if x == y then Just (Suggest x) else Nothing
+
+-- | A convenient type synonym for clarity.
+type Var_Name = Text
+
+-- | A convenient class synonym for brievety.
+class (Show var, Buildable var) => Variable var
+instance Variable Var_Name
+instance (Variable bound, Variable var) => Variable (Var bound var)
+instance Variable var => Variable (Suggest var)
+
+-- * Higher-order @Prelude@ classes
+
+-- ** Class 'Eq1'
+-- | Higher-order 'Eq' to avoid the @UndecidableInstances@ language extension.
+--
+-- __Ressources:__
+--
+-- * /Simulating Quantified Class Constraints/, Valery Trifonov, 2003,
+-- http://flint.cs.yale.edu/trifonov/papers/sqcc.pdf
+-- * /prelude-extras/, Edward Kmett, 2011,
+-- https://hackage.haskell.org/package/prelude-extras
+class Eq1 f where
+ (==#) :: (Eq a, Show a) => f a -> f a -> Bool
+
+class Eq1 f => Ord1 f where
+ compare1 :: Ord a => f a -> f a -> Ordering
+
+-- ** Class 'Show1'
+-- | Higher-order 'Show' to avoid the @UndecidableInstances@ language extension.
+class Show1 f where
+ showsPrec1 :: Show a => Int -> f a -> ShowS
+
+-- ** Type 'Lift1'
+-- | Higher-order 'Lift' to avoid the @UndecidableInstances@ language extension.
+newtype Lift1 f a = Lift1 { lower1 :: f a }
+ deriving (Functor, Foldable, Traversable, Eq1, Ord1, Show1)
+instance (Eq1 f, Eq a, Show a) => Eq (Lift1 f a) where (==) = (==#)
+instance (Ord1 f, Ord a, Show a) => Ord (Lift1 f a) where compare = compare1
+instance (Show1 f, Show a) => Show (Lift1 f a) where showsPrec = showsPrec1
+
+-- ** Type 'Suggest'
+
+-- | A convenient wrapper to include data ignored by /α-equivalence/.
+newtype Suggest n
+ = Suggest n
+ deriving (Functor, Show)
+-- | Always return 'True', in order to be transparent for 'alpha_equiv'.
+instance Eq (Suggest n) where
+ _ == _ = True
+instance Ord (Suggest n) where
+ _ `compare` _ = EQ
+instance Buildable var
+ => Buildable (Suggest var) where
+ build (Suggest var) = build var
+instance IsString x => IsString (Suggest x) where
+ fromString = Suggest . fromString
--- /dev/null
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -fno-warn-tabs #-}
+module Calculus.Lambda.Omega.Explicit where
+
+import Control.Arrow
+import Control.Monad
+import qualified Data.Char as Char
+import Data.Function (on)
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import Data.Maybe (catMaybes)
+import Data.Maybe (fromJust)
+import Data.Monoid ((<>))
+import Data.Text (Text)
+import qualified Data.Text as Text
+import Data.Text.Buildable (Buildable(..))
+import qualified Data.Text.Lazy as TL
+import qualified Data.Text.Lazy.Builder as Builder
+import Data.Typeable as Typeable
+import Data.Bool
+import Data.Eq (Eq(..))
+import Data.Maybe (Maybe(..), maybe)
+import Data.Foldable (Foldable(..))
+import Data.Either (Either(..))
+import Data.List ((++))
+import Data.Monoid (Monoid(..))
+import Data.Function (($), (.), id, const, flip)
+import Data.String (String)
+import Data.Traversable (Traversable(..))
+import Data.Ord (Ord(..))
+import Control.Applicative (Applicative(..), (<$>))
+import Text.Show (Show(..), showParen, showString)
+import Prelude (Int, Integer, Num(..), error)
+import System.IO (IO)
+
+-- import Debug.Trace
+
+import Calculus.Abstraction.DeBruijn.Generalized
+
+-- * Type 'Term'
+-- | 'Term' @var@ forms the main /Abstract Syntax Tree/
+-- of the present /explicitely typed/ (aka. /à la Church/) /lambda-calculus/,
+-- whose /term constructors/ are:
+--
+-- * 'TeTy_Var': for /term variable/ or /type variable/, see 'Abstraction'.
+-- * 'TeTy_App': for /term application/ or /type application/, see 'normalize'.
+-- * 'Term_Abst': for /term abstraction/ (aka. /λ-term/), see 'Abstraction'.
+-- * 'Type_Abst': for /type abstraction/ (aka. /Π-type/, aka. /dependent product/), see 'sort_of_type_abst'.
+-- * 'Type_Sort': for /sort constant/ of a /Pure Type System/ (aka. /PTS/), see 'sort_of_sort'.
+-- * 'TeTy_Axiom': for /custom axiom/, see 'Axiomable'.
+--
+-- Note that 'Type' and 'Term' share this same data-type
+-- (hence the varying prefixes of the Haskell /data constructors/),
+-- which avoids duplication of code for their common operations.
+--
+-- Note that this Haskell type DOES NOT guarantee by itself
+-- the /well-formedness/ of the 'Term' (or 'Type'),
+-- for instance one can construct such @malformed_type@: @(* *)@:
+--
+-- @
+-- > let star = 'Type_Sort' 'sort_star_mono'
+-- > let malformed_type = 'TeTy_App' star star
+-- > 'left' 'type_error_msg' '$' 'type_of' 'context' malformed_type
+-- Left ('Type_Error_Msg_Not_a_function' … )
+-- @
+--
+-- Though an Haskell type could be crafted to get a stronger guarantee
+-- over the /well-formedness/, it is not done here
+-- for the following reasons :
+--
+-- 1. The /well-formedness/ alone is not really useful,
+-- it’s the /well-typedness/ which matters,
+-- and this depends upon a specific 'Context'.
+--
+-- 2. Guaranteeing a good combinaison of 'TeTy_App' with respect to 'Term_Abst' (or 'Type_Abst')
+-- while using the 'Abstraction' approach could be done:
+-- for instance by using @GADTs@ on 'Term'
+-- to add an Haskell /type parameter/ @ty@ (aka. /index/)
+-- constrained to @(i -> o)@, @i@ or @o@ depending on the /term constructors/,
+-- and then by defining Haskell /type classes/
+-- replicating: 'Functor', 'Foldable', 'Traversable', 'Monad' and 'Monad_Module_Left',
+-- but working on /natural transformations/ (giving /indexed functors/, /indexed monads/, …),
+-- however this yields to a significant increase in code complexity,
+-- which is not really worth the resulting guarantee
+-- (to my mind, here, simplicity has priority
+-- over comprehensive automated checking,
+-- especially since it’s a research project
+-- where I don't fully know all what will be needed
+-- and thus appreciate some level of flexibility).
+--
+-- So, with this actual 'Term' data-type:
+-- 'type_of' MUST be used to check the /well-formedness/ along the /well-typedness/
+-- of a 'Term' (or equivalently of a 'Type') with respect to a 'Context'.
+data Term var
+ = TeTy_Var var
+ | TeTy_App (Term var) (Term var)
+ | Term_Abst (Suggest Var_Name) (Type var) (Abstraction (Suggest Var_Name) (Term) var)
+ | Type_Abst (Suggest Var_Name) (Type var) (Abstraction (Suggest Var_Name) (Type) var)
+ | Type_Sort Sort
+ | forall ax .
+ ( Axiomable (Axiom ax)
+ , Typeable ax
+ ) => TeTy_Axiom (Axiom ax)
+ -- deriving (Eq, Show, Functor, Foldable, Traversable)
+-- | 'Eq' instance ignores /bound variables/' 'Var_Name',
+-- effectively testing for /α-equivalence/.
+instance (Eq var, Show var) => Eq (Term var) where
+ TeTy_Var x == TeTy_Var y = x == y
+ TeTy_App xf xa == TeTy_App yf ya = xf == yf && xa == ya
+ Term_Abst _ xty xf == Term_Abst _ yty yf = xty == yty && xf == yf -- NOTE: ignore Var_Name
+ Type_Abst _ xty xf == Type_Abst _ yty yf = xty == yty && xf == yf -- NOTE: ignore Var_Name
+ Type_Sort x == Type_Sort y = x == y
+ TeTy_Axiom x == TeTy_Axiom y = x `axiom_eq` y
+ _ == _ = False
+deriving instance Show var => Show (Term var)
+-- | A 'Functor' instance capturing the notion of /variable renaming/.
+deriving instance Functor Term
+deriving instance Foldable Term
+deriving instance Traversable Term
+deriving instance Typeable Term
+instance Show1 Term where showsPrec1 = showsPrec
+instance Eq1 Term where (==#) = (==)
+
+instance Applicative (Term) where
+ pure = TeTy_Var
+ (<*>) = ap
+-- | A 'Monad' instance capturing the notion of /variable substitution/ with /capture-avoiding/.
+instance Monad (Term) where
+ return = pure
+ Type_Sort s >>= _ = Type_Sort s
+ TeTy_Axiom a >>= _ = TeTy_Axiom a
+ TeTy_Var v >>= go = go v
+ TeTy_App f x >>= go = TeTy_App (f >>= go) (x >>= go)
+ Term_Abst v f_in f >>= go = Term_Abst v (f_in >>= go) (f >>>= go)
+ Type_Abst v f_in f >>= go = Type_Abst v (f_in >>= go) (f >>>= go)
+instance Buildable var => Buildable (Term var) where
+ build = go False False
+ where
+ go :: forall v. (Buildable v)
+ => Bool -> Bool
+ -> Term v
+ -> Builder.Builder
+ go parenBind parenApp te =
+ case te of
+ Type_Sort s -> build s
+ TeTy_Axiom ax -> build ax
+ TeTy_Var v -> build v
+ TeTy_App f x ->
+ (if parenApp then "(" else "")
+ <> go True False f <> " " <> go True True x
+ <> (if parenApp then ")" else "")
+ Term_Abst _ _ _ ->
+ (if parenBind then "(" else "")
+ <> "λ"{- <> "\\"-} <> go_abst parenBind parenApp te
+ Type_Abst (Suggest x) f_in f_out ->
+ (if parenBind then "(" else "")
+ <> (if x == ""
+ then go True False f_in
+ else "∀" <> "(" <> build x <> ":" <> go False False f_in <> ")" )
+ <> " -> "
+ <> go False False (abstract_normalize f_out)
+ <> (if parenBind then ")" else "")
+ go_abst :: forall v. (Buildable v)
+ => Bool -> Bool
+ -> Term v
+ -> Builder.Builder
+ go_abst parenBind parenApp te =
+ case te of
+ Term_Abst (Suggest x) f_in f ->
+ let body = abstract_normalize f in
+ case body of
+ Term_Abst _ _ _ ->
+ "(" <> go_var_def x <> ":" <> go False False f_in <> ")"
+ <> " " <> go_abst parenBind parenApp body
+ _ ->
+ "(" <> go_var_def x <> ":" <> go False False f_in <> ")"
+ <> " -> "
+ <> go False False body
+ <> (if parenBind then ")" else "")
+ _ -> go parenBind parenApp te
+ go_var_def x = if x == "" then "_" else build x
+
+-- ** Type 'Sort'
+-- | Four /PTS/ /sort constants/
+-- are formed by combining
+-- 'Type_Level' and 'Type_Morphism':
+--
+-- * @*m@: the 'Sort' to form the 'Type' of a monomorphic 'Term'.
+-- * @*p@: the 'Sort' to form the 'Type' of a polymorphic 'Term'.
+-- * @□m@: the 'Sort' to form the 'Type' of a monomorphic 'Type'.
+-- * @□p@: the 'Sort' to form the 'Type' of a polymorphic 'Type'.
+type Sort = (Type_Level, Type_Morphism)
+instance Buildable Sort where
+ build x = case x of
+ (sort, morphism) -> build sort <> build morphism
+
+-- | @*m@: the 'Sort' to form the 'Type' of a monomorphic 'Term'.
+sort_star_mono :: Sort
+sort_star_mono = (Type_Level_0, Type_Morphism_Mono)
+
+-- | @*p@: the 'Sort' to form the 'Type' of a polymorphic 'Term'.
+sort_star_poly :: Sort
+sort_star_poly = (Type_Level_0, Type_Morphism_Poly)
+
+-- *** Type 'Type_Level'
+data Type_Level
+ = Type_Level_0 -- ^ aka. /@*@ (Star) sort constant/.
+ | Type_Level_1 -- ^ aka. /@□@ (Box) sort constant/.
+ deriving (Eq, Ord, Show)
+instance Buildable Type_Level where
+ build x = case x of
+ Type_Level_0 -> "*"
+ Type_Level_1 -> "□"
+
+-- *** Type 'Type_Morphism'
+data Type_Morphism
+ = Type_Morphism_Mono
+ | Type_Morphism_Poly
+ deriving (Eq, Ord, Show)
+instance Buildable Type_Morphism where
+ build x = case x of
+ Type_Morphism_Mono -> "" -- "m"
+ Type_Morphism_Poly -> "p"
+
+-- | /PTS/ axioms for 'Sort':
+--
+-- * AXIOM: @⊦ *m : □m@
+-- * AXIOM: @⊦ *p : □p@
+sort_of_sort :: Sort -> Either Type_Error_Msg Sort
+sort_of_sort (Type_Level_0, Type_Morphism_Mono)
+ = return (Type_Level_1, Type_Morphism_Mono)
+ -- AXIOM: @*m : □m@
+ -- The type of MONOMORPHIC types of terms,
+ -- is of type: the type of types of MONOMORPHIC types of terms
+sort_of_sort (Type_Level_0, Type_Morphism_Poly)
+ = return (Type_Level_1, Type_Morphism_Poly)
+ -- AXIOM: @*p : □p@
+ -- The type of POLYMORPHIC types of terms,
+ -- is of type: the type of types of POLYMORPHIC types of terms
+sort_of_sort s = Left $ Type_Error_Msg_No_sort_for_sort s
+
+-- * Type 'Form'
+
+-- | A record to keep a same 'Term' (or 'Type')
+-- in several forms (and avoid to 'normalize' it multiple times).
+data Form var
+ = Form
+ { form_given :: Term var
+ , form_normal :: Term var -- ^ 'normalize'-d version of 'form_given'.
+ } deriving (Functor, Show)
+
+-- | Return a 'Form' from a given 'Term'.
+form :: (Eq var, Ord var, Variable var, Typeable var) => Context var -> Term var -> Form var
+form ctx te = Form te (normalize ctx te)
+
+-- | Reduce given 'Term' (or 'Type') to /normal form/ (NF)
+-- by recursively performing /β-reduction/ and /η-reduction/.
+--
+-- Note that any well-typed 'Term' (i.e. for which 'type_of' returns a 'Type')
+-- is /strongly normalizing/ (i.e. 'normalize' always returns,
+-- and its returned 'Term' is unique up to /α-equivalence/).
+normalize :: (Eq var, Ord var, Variable var, Typeable var) => Context var -> Term var -> Term var
+normalize = go []
+ where
+ {-
+ go_debug :: (Eq var, Ord var, Variable var, Typeable var)
+ => [Term var]
+ -> Context var
+ -> Term var
+ -> Term var
+ go_debug args ctx te =
+ go args ctx $
+ trace ("normalize: "
+ ++ "\n te = " ++ show te
+ ++ "\n args = " ++ show args
+ ) $ te
+ -}
+
+ go :: (Eq var, Ord var, Variable var, Typeable var)
+ => [Term var]
+ -> Context var
+ -> Term var
+ -> Term var
+ go args ctx (TeTy_Var ((form_normal <$>) . context_item_term <=< context_lookup ctx -> Just te))
+ -- NOTE: Replace variable mapped by the context
+ = case args of
+ [] -> te -- NOTE: no need to normalize again
+ _ -> go args ctx te
+ go args ctx (TeTy_App f x)
+ -- NOTE: Normalize and collect applied arguments,
+ -- this to normalize an argument only once for all patterns.
+ = go (go [] ctx x : args) ctx f
+ go [] ctx (Term_Abst x f_in f)
+ -- NOTE: η-reduce: Term_Abst _ (TeTy_App f (TeTy_Var (Var_Bound _)) ==> f
+ = (Term_Abst x (go [] ctx f_in) ||| id)
+ (abst_eta_reduce ctx f)
+ go (x:args) ctx (Term_Abst _ _ f)
+ -- NOTE: β-reduce: TeTy_App (Term_Abst _ _ f) x ==> f x
+ = go args ctx (const x `unabstract` f)
+ go args ctx (Type_Abst x f_in f_out)
+ -- NOTE: Recurse in Type_Abst fields
+ = term_apps (Type_Abst x (go [] ctx f_in) (go_scope ctx f_out)) args
+ go args ctx (TeTy_Axiom (flip (axiom_normalize ctx) args -> Just (r_te, r_args)))
+ -- NOTE: Normalize axiom
+ = go r_args ctx r_te
+ go args _ctx te
+ -- NOTE: Reapply remaining arguments, normalized
+ = term_apps te args
+
+ abst_eta_reduce
+ :: (Eq var, Eq bound, Ord var, Ord bound, Variable var, Variable bound, Typeable var, Typeable bound)
+ => Context var
+ -> Abstraction bound (Term) var
+ -> Either (Abstraction bound (Term) var) -- could not η-reduce
+ (Term var) -- could η-reduce
+ abst_eta_reduce ctx =
+ (\abst_body ->
+ let new_ctx = context_push_nothing ctx in
+ case go [] new_ctx abst_body of
+ te@(TeTy_App t (TeTy_Var (Var_Bound _{-Term_Abst's variable-}))) ->
+ traverse (\var ->
+ case var of
+ Var_Free v -> Right v
+ -- NOTE: decrement the DeBruijn indexing by one
+ -- to reflect the removal of the Term_Abst.
+ Var_Bound _ -> Left $ abstract_generalize te
+ -- NOTE: cannot η-reduce because Term_Abst's variable
+ -- is also used within t.
+ ) t
+ te -> Left $ abstract_generalize te
+ ) .
+ abstract_normalize
+
+ go_scope
+ :: (Eq var, Eq bound, Ord var, Ord bound, Variable var, Variable bound, Typeable var, Typeable bound)
+ => Context var
+ -> Abstraction bound (Term) var
+ -> Abstraction bound (Term) var
+ go_scope ctx =
+ abstract_generalize .
+ go [] (context_push_nothing ctx) .
+ abstract_normalize
+
+-- | Reduce given 'Term' to /Weak Head Normal Form/ (WHNF).
+--
+-- __Ressources:__
+--
+-- * https://wiki.haskell.org/Weak_head_normal_form
+whnf :: (Ord var, Variable var, Typeable var) => Context var -> Term var -> Term var
+whnf = go []
+ where
+ go :: (Ord var, Variable var, Typeable var) => [Term var] -> Context var -> Term var -> Term var
+ go args ctx (TeTy_Var ((form_given <$>) .
+ context_item_term <=< context_lookup ctx
+ -> Just te))
+ -- NOTE: Replace any variable mapped by the context
+ = go args ctx te
+ go args ctx (TeTy_App f a)
+ -- NOTE: Collect applied arguments
+ = go (a:args) ctx f
+ go (x:args) ctx (Term_Abst _ _ f)
+ -- NOTE: β-reduce: TeTy_App (Term_Abst _ _ f) x ==> f x
+ = go args ctx (const x `unabstract` f)
+ go args ctx (TeTy_Axiom (flip (axiom_normalize ctx) args -> Just (r_te, r_args)))
+ -- NOTE: Normalize axiom
+ -- TODO: maybe introduce an 'axiom_whnf' instead of 'axiom_normalize'
+ = go r_args ctx r_te
+ go args _ctx te
+ -- NOTE: Reapply remaining arguments, normalized
+ = term_apps te args
+
+-- | Apply multiple 'Term's to a 'Term',
+-- useful to reconstruct a 'Term' while normalizing (see 'normalize' or 'whnf').
+term_apps :: Term var -> [Term var] -> Term var
+term_apps = foldl TeTy_App
+
+-- | /α-equivalence relation/, synonym of @(==)@.
+--
+-- Return 'True' iif. both given 'Term's are the same,
+-- up to renaming the /bound variables/ it contains (see instance 'Eq' of 'Suggest').
+alpha_equiv :: (Eq var, Show var) => Term var -> Term var -> Bool
+alpha_equiv = (==)
+
+-- | /αβη-equivalence relation/.
+equiv :: (Eq var, Ord var, Variable var, Typeable var) => Context var -> Term var -> Term var -> Bool
+-- equiv ctx = (==) `on` (normalize ctx)
+equiv ctx = (==) `on` normalize ctx
+
+-- * Type 'Type'
+
+-- | 'Type' and 'Term' share the same data-type.
+type Type = Term
+
+-- | Construct the 'Type' of the given 'Term',
+-- effectively checking for the /well-formedness/
+-- and /well-typedness/ of a 'Term' (or 'Type').
+--
+-- Note that a 'Type' is always to be considered
+-- according to a given 'Context':
+-- 'type_of' applied to the same 'Term'
+-- but on different 'Context's
+-- may return a different 'Type' or 'Type_Error'.
+type_of
+ :: (Eq var, Ord var, Variable var, Typeable var)
+ => Context var
+ -> Term var
+ -> Either Type_Error (Type var)
+type_of ctx term =
+ case term of
+ Type_Sort s -> (err +++ Type_Sort) $ sort_of_sort s
+ TeTy_Var v ->
+ case form_normal
+ . context_item_type
+ <$> context_lookup ctx v of
+ Just ty -> return ty
+ Nothing -> Left $ err $ Type_Error_Msg_Unbound_variable v
+ TeTy_Axiom ax ->
+ return $ axiom_type_of ctx ax
+ TeTy_App f x -> do
+ f_ty <- whnf ctx <$> type_of ctx f
+ (f_in, f_out) <-
+ case f_ty of
+ Type_Abst _ i o -> return (i, o)
+ _ -> Left $ err $ Type_Error_Msg_Not_a_function f f_ty
+ x_ty <- type_of ctx x
+ case equiv ctx x_ty f_in of
+ True -> return $ const x `unabstract` f_out
+ False -> Left $ err $ Type_Error_Msg_Function_argument_mismatch f_in x_ty
+ Term_Abst (Suggest x) f_in f -> do
+ _ <- type_of ctx f_in
+ let new_ctx =
+ if x == ""
+ then context_push_nothing ctx
+ else context_push_type ctx (Suggest x) f_in
+ f_out <- type_of new_ctx (abstract_normalize f)
+ let abst_ty = Type_Abst (Suggest x) f_in (abstract_generalize f_out)
+ _ <- type_of ctx abst_ty
+ return abst_ty
+ Type_Abst (Suggest x) f_in f -> do
+ f_in_ty <- type_of ctx f_in
+ f_in_so <- case whnf ctx f_in_ty of
+ Type_Sort s -> return s
+ f_in_ty_whnf -> Left $ err $ Type_Error_Msg_Invalid_input_type f_in_ty_whnf
+ let new_ctx =
+ if x == ""
+ then context_push_nothing ctx
+ else context_push_type ctx (Suggest x) f_in
+ f_out_ty <- type_of new_ctx (abstract_normalize f)
+ f_out_so <- case whnf new_ctx f_out_ty of
+ Type_Sort s -> return s
+ f_out_ty_whnf -> Left $ Type_Error ctx term $
+ Type_Error_Msg_Invalid_output_type f_out_ty_whnf (x, f_out_ty_whnf)
+ (err +++ Type_Sort) $
+ sort_of_type_abst f_in_so f_out_so
+ where
+ err = Type_Error ctx term
+
+-- | Check that the given 'Term' has the given 'Type'.
+check
+ :: (Eq var, Ord var, Variable var, Typeable var)
+ => Context var
+ -> Type var
+ -> Term var
+ -> Either (Type_Error) ()
+check ctx expect_ty te =
+ type_of ctx te >>= \actual_ty ->
+ if equiv ctx expect_ty actual_ty
+ then Right ()
+ else Left $ Type_Error
+ { type_error_ctx = ctx
+ , type_error_term = te
+ , type_error_msg = Type_Error_Msg_Type_mismatch expect_ty actual_ty (normalize ctx expect_ty) (normalize ctx actual_ty)
+ }
+
+-- | Check that a 'Term' is closed, i.e. has no /unbound variables/.
+close :: Term Var_Name -> Either Type_Error (Term ())
+close te =
+ traverse go te
+ where
+ go var = Left $
+ Type_Error context te $
+ Type_Error_Msg_Unbound_variable var
+
+-- | Return the /unbound variables/ of given 'Term'.
+unbound_vars :: Ord var => Term var -> Map var ()
+unbound_vars = foldr (flip Map.insert ()) mempty
+
+-- | /Dependent product/ rules: @s ↝ t : u@, i.e.
+-- "abstracting something of type @s@ out of something of type @t@ gives something of type @u@".
+--
+-- Given two 'Sort': @s@ and @t@, return a 'Sort': @u@,
+-- when ('Type_Abst' @s@ @t@) is ruled legal
+-- and has 'Type': 'Type_Sort' ('Sort' @u@).
+--
+-- The usual /PTS/ rules for /λω/
+-- (or equivalently /Type Assignment Systems/ (TAS) rules for /System Fω/)
+-- are used here:
+--
+-- * RULE: @⊦ * ↝ * : *@, aka. /simple types/:
+-- "abstracting a term out of a term is valid and gives a term",
+-- as in /PTS λ→/ or /TAS F1/.
+-- * RULE: @⊦ □ ↝ * : *@, aka. /parametric polymorphism/:
+-- "abstracting a type out of a term is valid and gives a term",
+-- as in /PTS λ2/ or /TAS F2/ (aka. /System F/).
+-- * RULE: @⊦ □ ↝ □ : □@, aka. /constructors of types/:
+-- "abstracting a type out of a type is valid and gives a type",
+-- as in /PTS λω/ or /TAS Fω/.
+--
+-- Note that the fourth usual rule is not ruled valid here:
+--
+-- * RULE: @⊦ * ↝ □ : □@, aka. /dependent types/:
+-- "abstracting a term out of a type is valid and gives a type",
+-- as in /PTS λPω/ or /TAS DFω/ (aka. /Calculus of constructions/).
+--
+-- However, to contain /impredicativity/ (see 'Axiom_MonoPoly')
+-- the above /sort constants/ are split in two,
+-- and the above rules adapted
+-- to segregate between /monomorphic types/ (aka. /monotypes/)
+-- and /polymorphic types/ (aka. /polytypes/):
+--
+-- * RULE: @⊦ *m ↝ *m : *m@, i.e. /simple types/, without /parametric polymorphism/.
+-- * RULE: @⊦ *m ↝ *p : *p@, i.e. /simple types/, preserving /parametric polymorphism/ capture.
+--
+-- * RULE: @⊦ *p ↝ *m : *p@, i.e. /higher-rank polymorphism/, preserving /parametric polymorphism/ capture.
+-- * RULE: @⊦ *p ↝ *p : *p@, i.e. /higher-rank polymorphism/, preserving /parametric polymorphism/ capture.
+--
+-- * RULE: @⊦ □m ↝ *m : *p@, i.e. /parametric polymorphism/, captured within @*p@ ('sort_star_poly').
+-- * RULE: @⊦ □m ↝ *p : *p@, i.e. /parametric polymorphism/, preserving capture.
+--
+-- * RULE: @⊦ □m ↝ □m : □m@, i.e. /constructors of types/, without /parametric polymorphism/.
+-- * RULE: @⊦ □m ↝ □p : □p@, i.e. /constructors of types/, preserving /parametric polymorphism/ capture.
+--
+-- Note that what is important here is
+-- that there is no rule of the form: @⊦ □p ↝ _ : _@,
+-- which forbids abstracting a /polymorphic type/ out of anything,
+-- in particular the type @*p -> *m@ is forbidden,
+-- though 'Axiom_MonoPoly'
+-- is given to make it possible within it.
+--
+-- __Ressources:__
+--
+-- * /Henk: a typed intermediate language/,
+-- Simon Peyton Jones, Erik Meijer, 20 May 1997,
+-- https://research.microsoft.com/en-us/um/people/simonpj/papers/henk.ps.gz
+sort_of_type_abst
+ :: Sort
+ -> Sort
+ -> Either Type_Error_Msg Sort
+
+-- Simple types
+sort_of_type_abst
+ (Type_Level_0, Type_Morphism_Mono)
+ (Type_Level_0, m)
+ = return (Type_Level_0, m)
+ -- RULE: *m ↝ *m : *m
+ -- RULE: *m ↝ *p : *p
+ -- abstracting: a MONOMORPHIC term
+ -- out of : a MONOMORPHIC (resp. POLYMORPHIC) term
+ -- forms : a MONOMORPHIC (resp. POLYMORPHIC) term
+
+-- Higher-rank
+sort_of_type_abst
+ (Type_Level_0, Type_Morphism_Poly)
+ (Type_Level_0, _)
+ = return (Type_Level_0, Type_Morphism_Poly)
+ -- RULE: *p ↝ *m : *p
+ -- RULE: *p ↝ *p : *p
+ -- abstracting: a POLYMORPHIC term
+ -- out of : a term
+ -- forms : a POLYMORPHIC term
+
+-- Polymorphism
+sort_of_type_abst
+ (Type_Level_1, Type_Morphism_Mono)
+ (Type_Level_0, _)
+ = return (Type_Level_0, Type_Morphism_Poly)
+ -- RULE: □m ↝ *m : *p
+ -- RULE: □m ↝ *p : *p
+ -- abstracting: a MONOMORPHIC type of a term
+ -- out of : a term
+ -- forms : a POLYMORPHIC term
+
+-- Type constructors
+sort_of_type_abst
+ (Type_Level_1, Type_Morphism_Mono)
+ (Type_Level_1, m)
+ = return (Type_Level_1, m)
+ -- RULE: □m ↝ □m : □m
+ -- RULE: □m ↝ □p : □p
+ -- abstracting: a MONOMORPHIC type of a term
+ -- out of : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
+ -- forms : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
+ --
+ -- NOTE: □m ↝ □p : □p is useful for instance to build List_:
+ -- let List_ : (A:*m) -> *p = \(A:*m) -> (R:*m) -> (A -> R -> R) -> R -> R
+ -- let List : (A:*m) -> *m = \(A:*m) -> Monotype (List_ A)
+
+-- Dependent types
+
+{-
+sort_of_type_abst
+ (Type_Level_0, Type_Morphism_Mono)
+ (Type_Level_1, m)
+ = return (Type_Level_1, m)
+ -- RULE: *m ↝ □m : □m
+ -- RULE: *m ↝ □p : □p
+ -- abstracting: a MONOMORPHIC term
+ -- out of : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
+ -- forms : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
+
+sort_of_type_abst
+ (Type_Level_0, Type_Morphism_Poly)
+ (Type_Level_1, _)
+ = return (Type_Level_1, Type_Morphism_Poly)
+ -- RULE: *p ↝ □m : □p
+ -- RULE: *p ↝ □p : □p
+ -- abstracting: a POLYMORPHIC term
+ -- out of : a type of a term
+ -- forms : a POLYMORPHIC type of a term
+-}
+
+sort_of_type_abst
+ s@(Type_Level_0, _)
+ t@(Type_Level_1, _)
+ = Left $ Type_Error_Msg_Illegal_type_abstraction s t
+ -- RULE: * ↝ □ : Illegal
+ -- abstracting: a term
+ -- out of : a type of a term
+ -- is illegal
+
+-- No impredicativity (only allowed through 'Axiom_MonoPoly')
+sort_of_type_abst
+ s@(Type_Level_1, Type_Morphism_Poly)
+ t@(_, _)
+ = Left $ Type_Error_Msg_Illegal_type_abstraction s t
+ -- RULE: □p ↝ _ : Illegal
+ -- abstracting: a POLYMORPHIC type of a term
+ -- out of : anything
+ -- is illegal
+
+-- ** Type 'Type_Error'
+data Type_Error
+ = forall var. (Ord var, Show var, Buildable var)
+ => Type_Error
+ { type_error_ctx :: Context var
+ , type_error_term :: Term var
+ , type_error_msg :: Type_Error_Msg
+ }
+deriving instance Show Type_Error
+instance Buildable Type_Error where
+ build (Type_Error ctx te msg) =
+ "Error: Type_Error"
+ <> "\n " <> build msg
+ <> "\n Term:" <> " " <> build te
+ <> (
+ let vars =
+ Map.keys $
+ Map.intersection
+ (unbound_vars te)
+ (Map.fromList $ (, ()) <$> context_vars ctx) in
+ case vars of
+ [] -> "\n"
+ _ -> "\n Context:\n" <> build ctx{context_vars=vars}
+ )
+
+-- ** Type 'Type_Error_Msg'
+data Type_Error_Msg
+ = Type_Error_Msg_No_sort_for_sort Sort
+ | Type_Error_Msg_Illegal_type_abstraction Sort Sort
+ | forall var. Variable var => Type_Error_Msg_Invalid_input_type (Type var)
+ | forall var. Variable var => Type_Error_Msg_Invalid_output_type (Type var) (Var_Name, Type var)
+ | forall var. Variable var => Type_Error_Msg_Not_a_function (Term var) (Type var)
+ | forall var. Variable var => Type_Error_Msg_Function_argument_mismatch (Type var) (Type var)
+ | forall var. Variable var => Type_Error_Msg_Unbound_variable var
+ | forall var. Variable var => Type_Error_Msg_Unbound_axiom var
+ | forall var. Variable var => Type_Error_Msg_Type_mismatch (Type var) (Type var) (Type var) (Type var)
+deriving instance Show Type_Error_Msg
+instance Buildable Type_Error_Msg where
+ build msg =
+ case msg of
+ Type_Error_Msg_No_sort_for_sort x ->
+ "No_sort_for_sort: "
+ <> build x
+ Type_Error_Msg_Illegal_type_abstraction x y ->
+ "Illegal_type_abstraction: "
+ <> build x <> " -> " <> build y
+ Type_Error_Msg_Invalid_input_type ty ->
+ "Invalid_input_type: "
+ <> build ty
+ Type_Error_Msg_Invalid_output_type f_out (x, f_in) ->
+ "Invalid_output_type: "
+ <> build f_out <> "\n"
+ <> " Input binding: "
+ <> "(" <> build x <> " : " <> build f_in <> ")"
+ Type_Error_Msg_Not_a_function f f_ty ->
+ "Not_a_function: "
+ <> build f
+ <> " : "
+ <> build f_ty
+ Type_Error_Msg_Function_argument_mismatch f_in x_ty ->
+ "Function_argument_mismatch: \n"
+ <> " Function domain: " <> build f_in <> "\n"
+ <> " Argument type: " <> build x_ty
+ Type_Error_Msg_Unbound_variable var ->
+ "Unbound_variable: "
+ <> build var
+ Type_Error_Msg_Unbound_axiom var ->
+ "Unbound_axiom: "
+ <> build var
+ Type_Error_Msg_Type_mismatch x y nx ny ->
+ "Type_mismatch: \n"
+ <> " Expected type: " <> build x <> " == " <> build nx <> "\n"
+ <> " Actual type: " <> build y <> " == " <> build ny
+
+-- * Type 'Context'
+
+-- | Map variables of type @var@
+-- to their 'Type' and maybe also to their 'Term',
+-- both in 'form_given' and 'form_normal'.
+data Context var
+ = Context
+ { context_vars :: [var]
+ -- ^ used to dump the 'Context'
+ , context_lookup :: var -> Maybe (Context_Item var)
+ -- ^ used to query the 'Context'
+ , context_lift :: Typeable var => Var_Name -> var
+ -- ^ used to promote a ('Term' 'Var_Name') to ('Term' @var@)
+ , context_unlift :: Typeable var => var -> Var_Name
+ -- ^ used to unpromote ('Term' @var@) to ('Term' 'Var_Name')
+ }
+data Context_Item var
+ = Context_Item
+ { context_item_term :: Maybe (Form var)
+ , context_item_type :: Form var
+ } deriving (Functor, Show)
+
+instance Show var => Show (Context var) where
+ showsPrec n ctx@Context{context_vars=vars} =
+ showParen (n > 10) $
+ showString "Context " .
+ showsPrec n ((\k ->
+ (k, fromJust $ context_item_type
+ <$> context_lookup ctx k))
+ <$> vars) .
+ showString " " .
+ showsPrec n (catMaybes $ (\k ->
+ (k,) . form_given <$>
+ (context_item_term =<< context_lookup ctx k))
+ <$> vars)
+instance Buildable var => Buildable (Context var) where
+ build ctx@Context{context_vars=vars} =
+ foldMap (\var ->
+ " " <> build var
+ <> maybe mempty (\ty -> " : " <> build (form_given ty))
+ (context_item_type <$> context_lookup ctx var)
+ {-
+ <> maybe mempty (\te -> " = " <> build (form_given te))
+ (context_item_term =<< context_lookup ctx var)
+ -}
+ <> "\n"
+ ) vars
+
+context :: Context Var_Name
+context = Context [] (const Nothing) id id
+
+context_apply :: Context var -> Term var -> Term var
+context_apply ctx te =
+ te >>= \var ->
+ maybe (TeTy_Var var) id $ form_normal <$>
+ (context_item_term =<< context_lookup ctx var)
+
+context_push_type
+ :: (Eq var, Ord var, Variable var, Typeable var)
+ => Context var
+ -> bound
+ -> Type var
+ -> Context (Var bound var)
+context_push_type
+ ctx@(Context keys lookup var_lift var_unlift)
+ bound ty =
+ Context
+ { context_vars =
+ Var_Bound bound :
+ Var_Free `fmap` keys
+ , context_lookup = \var ->
+ (Var_Free `fmap`) `fmap`
+ case var of
+ Var_Bound _ ->
+ Just $ Context_Item
+ { context_item_term = Nothing
+ , context_item_type = form ctx ty
+ }
+ Var_Free v -> lookup v
+ , context_lift = Var_Free . var_lift
+ , context_unlift = \var ->
+ case var of
+ Var_Bound _ -> error "context_push_type: context_unlift"
+ Var_Free v -> var_unlift v
+ }
+
+context_push_nothing
+ :: (Show bound, Buildable (Context var), Typeable var, Typeable bound)
+ => Context var
+ -> Context (Var bound var)
+context_push_nothing
+ (Context keys lookup var_lift var_unlift) =
+ Context
+ { context_vars = Var_Free `fmap` keys
+ , context_lookup = \var ->
+ (Var_Free `fmap`) `fmap`
+ case var of
+ Var_Bound _ -> Nothing
+ Var_Free v -> lookup v
+ , context_lift = Var_Free . var_lift
+ , context_unlift = \var ->
+ case var of
+ -- DEBUG: Var_Bound (cast -> Just (Suggest b)) -> b
+ -- DEBUG: Var_Bound (cast -> Just b) -> b
+ Var_Bound b -> error $ "context_push_nothing: context_unlift: " ++ show b
+ Var_Free v -> var_unlift v
+ }
+
+context_from_env :: Env -> Context Var_Name
+context_from_env env =
+ Context
+ { context_vars = Map.keys env
+ , context_lookup = \var ->
+ (\item -> Context_Item
+ { context_item_term = Just $ env_item_term item
+ , context_item_type = env_item_type item
+ }) <$> env_lookup env var
+ , context_lift = id
+ , context_unlift = id
+ }
+
+context_relift :: forall from_var to_var.
+ ( Typeable from_var
+ , Typeable to_var )
+ => Context from_var
+ -> Type from_var
+ -> Context to_var
+ -> Type to_var
+context_relift from_ctx ty to_ctx =
+ ( context_lift to_ctx
+ . context_unlift from_ctx
+ ) <$> ty
+
+{-
+context_from_list :: Eq var => [(var, Type var)] -> Context var
+context_from_list l =
+ Context
+ { context_vars = fst <$> l
+ , context_lookup_type = \var -> List.lookup var l
+ }
+
+-- | Return /free term variables/ of an 'Abstraction'-ed 'Term'.
+ftv
+ :: Abstraction bound (Term) var
+ -> Term (Var bound var)
+ftv = abstract_normalize
+-}
+
+-- * Type 'Env'
+type Env
+ = Map Var_Name Env_Item
+data Env_Item
+ = Env_Item
+ { env_item_term :: Form Var_Name
+ , env_item_type :: Form Var_Name
+ }
+env_item
+ :: Context Var_Name
+ -> Term Var_Name
+ -> Type Var_Name
+ -> Env_Item
+env_item ctx te ty =
+ Env_Item
+ { env_item_term = form ctx te
+ , env_item_type = form ctx ty
+ }
+
+env_lookup :: Env -> Var_Name -> Maybe (Env_Item)
+env_lookup env var = Map.lookup var env
+
+env_insert :: Var_Name -> Term Var_Name -> Type Var_Name -> Env -> Env
+env_insert var te ty env =
+ let ctx = context_from_env env in
+ Map.insert var (env_item ctx te ty) env
+
+-- * Type 'Axiom'
+
+data family Axiom r
+-- deriving instance Typeable Axiom
+
+axiom_cast :: (Typeable a, Typeable b) => Axiom a -> Maybe (Axiom b)
+axiom_cast = cast
+
+-- ** Type 'Axioms'
+-- | 'Axioms' are made of 'Axiom's injected in regular 'Env_Item's,
+-- see 'env_item_from_axiom'.
+type Axioms = Env
+
+env_item_from_axiom
+ :: ( Axiomable (Axiom ax)
+ , Typeable ax )
+ => Context Var_Name -> Axiom ax -> Env_Item
+env_item_from_axiom ctx ax =
+ Env_Item
+ { env_item_term = form ctx $ TeTy_Axiom ax
+ , env_item_type = form ctx $ axiom_type_of ctx ax
+ }
+
+-- ** Class 'Axiomable'
+
+-- class (Eq ax, Show ax, Buildable ax, Typeable ax) => Axiomable_Type_Of ax where
+-- class (Eq ax, Show ax, Buildable ax, Typeable ax) => Axiomable_Normalize ax where
+-- class (Eq ax, Show ax, Buildable ax, Typeable ax) => Axiomable_Eq ax where
+
+-- | Instances of this class are 'Axiom's injectable in 'TeTy_Axiom', that is:
+--
+-- * they have a 'Type', given by 'axiom_type_of',
+-- * and they can perform an optional reduction
+-- within 'normalize' or 'whnf', given by 'axiom_normalize'.
+class
+ ( Eq ax, Show ax, Buildable ax, Typeable ax
+ -- , Axiomable_Type_Of ax
+ -- , Axiomable_Normalize ax
+ -- , Axiomable_Eq ax
+ ) => Axiomable ax where
+ axiom_type_of
+ :: forall var. Typeable var
+ => Context var -> ax -> Type var
+ -- ^ Return the 'Type' of the given 'Axiomable' instance.
+ axiom_normalize
+ :: forall var. (Typeable var, Ord var, Variable var)
+ => Context var -> ax -> [Term var] -> Maybe (Term var, [Term var])
+ -- ^ Custom-'normalize': given a typing 'Context',
+ -- an 'Axiomable' instance
+ -- and a list of arguments, return:
+ --
+ -- * 'Nothing': if the axiom performs no reduction,
+ -- * 'Just': with the reducted 'Term' and the arguments not used by the reduction.
+ --
+ -- Default: @\\_ctx _ax _args -> Nothing@
+ axiom_normalize _ctx _ax _args = Nothing
+ axiom_eq :: ax -> (forall ax'. Axiomable ax' => ax' -> Bool)
+ -- ^ Custom-bipolymorphic-@(==)@:
+ -- given an 'Axiomable' instance
+ -- return a function to test if any
+ -- other 'Axiomable' instance
+ -- is equal to the first instance given.
+ --
+ -- Default: @maybe False (x ==) (cast y)@
+ axiom_eq x y = maybe False (x ==) (cast y)
+
+-- ** Class 'Axiom_Type'
+
+-- | A class to embed an Haskell-type within an 'Axiom'.
+class Axiom_Type h where
+ axiom_type :: Axiom h
+ -- ^ Construct (implicitely) an Haskell-term representing
+ -- the Haskell-type @h@.
+ axiom_Type :: Axiom h -> Type Var_Name
+ -- ^ Return a 'Type' representing the Haskell-type @h@,
+ -- given through its representation as an Haskell-term
+ -- (which is an 'Axiom' and thus has itself a 'Type',
+ -- given by its 'axiom_type_of').
+
+axiom_term
+ :: (Axiom_Type h, Typeable h)
+ => h -> Axiom (Axiom_Term h)
+axiom_term (x::h) =
+ Axiom_Term x $ \ctx ->
+ context_lift ctx <$> axiom_Type (axiom_type::Axiom h)
+
+-- ** Type 'Axiom_Type_Assume'
+-- | An instance to use 'Type' as an 'Axiom'.
+data Axiom_Type_Assume
+newtype instance Axiom (Axiom_Type_Assume)
+ = Axiom_Type_Assume (Type Var_Name)
+ deriving (Eq, Show)
+instance Buildable (Axiom Axiom_Type_Assume) where
+ build (Axiom_Type_Assume ty) = "(_:" <> build ty <> ")"
+instance Axiomable (Axiom Axiom_Type_Assume) where
+ axiom_type_of ctx (Axiom_Type_Assume ty) =
+ context_lift ctx <$> ty
+
+-- ** Type 'Axiom_MonoPoly'
+-- | Non-'Sort' constants for /boxed parametric polymorphism/.
+--
+-- Used to embed /polymorphic types/ into first-class /monomorphic types/
+-- via explicit injection ('Axiom_Term_MonoPoly_Box') and projection ('Axiom_Term_MonoPoly_UnBox') functions.
+--
+-- Special treatment of 'Axiom_MonoPoly' constructors is done in 'normalize' and 'whnf'
+-- to remove adjacent pairs of 'Axiom_Term_MonoPoly_Box' / 'Axiom_Term_MonoPoly_UnBox'
+-- or 'Axiom_Term_MonoPoly_UnBox' / 'Axiom_Term_MonoPoly_Box'.
+--
+-- __Ressources:__
+--
+-- * /Recasting MLF/, Didier Le Botlan, Didier Rémy, June 2009,
+-- https://hal.inria.fr/inria-00156628
+data Axiom_MonoPoly
+data instance Axiom Axiom_MonoPoly
+ = Axiom_Type_MonoPoly
+ | Axiom_Term_MonoPoly_Box
+ | Axiom_Term_MonoPoly_UnBox
+ deriving (Eq, Ord, Show)
+instance Buildable (Axiom Axiom_MonoPoly) where
+ build ax = case ax of
+ Axiom_Type_MonoPoly -> "Monotype"
+ Axiom_Term_MonoPoly_Box -> "monotype"
+ Axiom_Term_MonoPoly_UnBox -> "polytype"
+instance Axiomable (Axiom Axiom_MonoPoly) where
+ axiom_type_of ctx ax =
+ case ax of
+ Axiom_Type_MonoPoly ->
+ -- Monotype : *p -> *m
+ Type_Abst "" (Type_Sort sort_star_poly) $
+ (const Nothing `abstract`) $
+ Type_Sort sort_star_mono
+ Axiom_Term_MonoPoly_Box ->
+ -- monotype : (Polytype : *p) -> Polytype -> Monotype Polytype
+ (context_lift ctx <$>) $
+ Type_Abst "Polytype" (Type_Sort sort_star_poly) $
+ (("Polytype" =?) `abstract`) $
+ Type_Abst "" (TeTy_Var "Polytype") $
+ (("" =?) `abstract`) $
+ TeTy_App
+ (TeTy_Axiom $ Axiom_Type_MonoPoly)
+ (TeTy_Var "Polytype")
+ Axiom_Term_MonoPoly_UnBox ->
+ -- polytype : (Polytype : *p) -> Monotype Polytype -> Polytype
+ (context_lift ctx <$>) $
+ Type_Abst "Polytype" (Type_Sort sort_star_poly) $
+ (("Polytype" =?) `abstract`) $
+ Type_Abst ""
+ (TeTy_App
+ (TeTy_Axiom $ Axiom_Type_MonoPoly)
+ (TeTy_Var "Polytype")) $
+ (("" =?) `abstract`) $
+ TeTy_Var "Polytype"
+ axiom_normalize _ctx
+ Axiom_Term_MonoPoly_UnBox
+ (_ty:TeTy_App (TeTy_App (TeTy_Axiom (axiom_cast -> Just Axiom_Term_MonoPoly_Box)) _ty') te:args)
+ -- NOTE: Remove adjacent Axiom_Term_MonoPoly_UnBox / Axiom_Term_MonoPoly_Box
+ = Just (te, args)
+ axiom_normalize _ctx
+ Axiom_Term_MonoPoly_Box
+ (_ty:TeTy_App (TeTy_App (TeTy_Axiom (axiom_cast -> Just Axiom_Term_MonoPoly_UnBox)) _ty') te:args)
+ -- NOTE: Remove adjacent Axiom_Term_MonoPoly_Box / Axiom_Term_MonoPoly_UnBox
+ = Just (te, args)
+ axiom_normalize _ctx _ax _args = Nothing
+
+-- | /PTS/ axioms for 'Axiom_MonoPoly':
+--
+-- * AXIOM: @⊦ Monotype : *p -> *m@
+-- * AXIOM: @⊦ monotype : (Polytype : *p) -> Polytype -> Monotype Polytype@
+-- * AXIOM: @⊦ polytype : (Polytype : *p) -> Monotype Polytype -> Polytype@
+axioms_monopoly :: Axioms
+axioms_monopoly =
+ Map.fromList $
+ [ ("Monotype", item Axiom_Type_MonoPoly)
+ , ("monotype", item Axiom_Term_MonoPoly_Box)
+ , ("polytype", item Axiom_Term_MonoPoly_UnBox)
+ ]
+ where
+ item = env_item_from_axiom ctx
+ ctx = context_from_env mempty
+
+-- ** Type 'Axiom_Term'
+
+-- | Embed an Haskell-term of Haskell-type @h@ within an 'Axiom'
+data Axiom_Term h
+data instance Axiom (Axiom_Term h)
+ = Typeable h
+ => Axiom_Term h
+ (forall var. Typeable var => Context var -> Type var)
+ deriving (Typeable)
+
+-- Instance 'Axiom' 'Integer'
+data instance Axiom Integer
+ = Axiom_Type_Integer
+ deriving (Eq, Ord, Show)
+instance Buildable (Axiom Integer) where
+ build Axiom_Type_Integer = "Int"
+instance Axiomable (Axiom Integer) where
+ axiom_type_of _ctx Axiom_Type_Integer =
+ Type_Sort (Type_Level_0, Type_Morphism_Mono)
+
+instance Axiom_Type Integer where
+ axiom_type = Axiom_Type_Integer
+ axiom_Type = TeTy_Axiom
+instance Eq (Axiom (Axiom_Term Integer)) where
+ Axiom_Term x _ == Axiom_Term y _ = x == y
+instance Ord (Axiom (Axiom_Term Integer)) where
+ Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
+instance Show (Axiom (Axiom_Term Integer)) where
+ showsPrec n (Axiom_Term te ty) =
+ showParen (n > 10) $
+ showString "Axiom_Term " .
+ showsPrec n te .
+ showString " " .
+ showsPrec n (ty context)
+instance Buildable (Axiom (Axiom_Term Integer)) where
+ build (Axiom_Term i _ty) = build i
+instance Axiomable (Axiom (Axiom_Term Integer)) where
+ axiom_type_of _ctx (Axiom_Term _ _ty) =
+ TeTy_Axiom Axiom_Type_Integer
+
+-- Instance 'Axiom' '()'
+data instance Axiom ()
+ = Axiom_Type_Unit
+ deriving (Eq, Ord, Show)
+instance Buildable (Axiom ()) where
+ build (Axiom_Type_Unit) = "()"
+instance Axiomable (Axiom ()) where
+ axiom_type_of _ctx Axiom_Type_Unit =
+ Type_Sort (Type_Level_0, Type_Morphism_Mono)
+
+instance Axiom_Type () where
+ axiom_type = Axiom_Type_Unit
+ axiom_Type = TeTy_Axiom
+instance Eq (Axiom (Axiom_Term ())) where
+ Axiom_Term x _ == Axiom_Term y _ = x == y
+instance Ord (Axiom (Axiom_Term ())) where
+ Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
+instance Show (Axiom (Axiom_Term ())) where
+ showsPrec n (Axiom_Term te ty) =
+ showParen (n > 10) $
+ showString "Axiom_Term " .
+ showsPrec n te .
+ showString " " .
+ showsPrec n (ty context)
+instance Buildable (Axiom (Axiom_Term ())) where
+ build (Axiom_Term _te _ty) = "()"
+instance Axiomable (Axiom (Axiom_Term ())) where
+ axiom_type_of _ctx (Axiom_Term _te _ty) =
+ TeTy_Axiom Axiom_Type_Unit
+
+-- Instance 'Axiom' 'Text'
+data instance Axiom Text
+ = Axiom_Type_Text
+ deriving (Eq, Ord, Show)
+instance Buildable (Axiom Text) where
+ build (Axiom_Type_Text) = "Text"
+instance Axiomable (Axiom Text) where
+ axiom_type_of _ctx Axiom_Type_Text =
+ Type_Sort (Type_Level_0, Type_Morphism_Mono)
+
+instance Axiom_Type Text where
+ axiom_type = Axiom_Type_Text
+ axiom_Type = TeTy_Axiom
+instance Eq (Axiom (Axiom_Term Text)) where
+ Axiom_Term x _ == Axiom_Term y _ = x == y
+instance Ord (Axiom (Axiom_Term Text)) where
+ Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
+instance Show (Axiom (Axiom_Term Text)) where
+ showsPrec n (Axiom_Term te ty) =
+ showParen (n > 10) $
+ showString "Axiom_Term " .
+ showsPrec n te .
+ showString " " .
+ showsPrec n (ty context)
+instance Buildable (Axiom (Axiom_Term Text)) where
+ build (Axiom_Term t _) = build $ show t
+instance Axiomable (Axiom (Axiom_Term Text)) where
+ axiom_type_of _ctx (Axiom_Term _te _ty) =
+ TeTy_Axiom Axiom_Type_Text
+
+-- Instance 'Axiom' type variable
+
+-- ** Type 'Axiom_Type_Var'
+
+-- | Singleton type, whose constructors
+-- are bijectively mapped to Haskell types
+-- of kind 'Type_Var'.
+data Axiom_Type_Var (v::Type_Var) where
+ Axiom_Type_Var_Zero :: Axiom_Type_Var 'Type_Var_Zero
+ Axiom_Type_Var_Succ :: Axiom_Type_Var v -> Axiom_Type_Var ('Type_Var_Succ v)
+deriving instance Eq (Axiom_Type_Var v)
+deriving instance Ord (Axiom_Type_Var v)
+deriving instance Show (Axiom_Type_Var v)
+deriving instance Typeable Axiom_Type_Var
+instance Buildable (Axiom_Type_Var v) where
+ build v = build $ type_var_string v
+
+-- *** Type 'Type_Var'
+
+-- | Natural numbers (aka. /Peano numbers/)
+-- promoted by @DataKinds@ to Haskell type-level.
+data Type_Var
+ = Type_Var_Zero
+ | Type_Var_Succ Type_Var
+ deriving (Eq, Ord, Show, Typeable)
+
+type A = Axiom_Type_Var 'Type_Var_Zero
+type B = Axiom_Type_Var ('Type_Var_Succ 'Type_Var_Zero)
+type C = Axiom_Type_Var ('Type_Var_Succ ('Type_Var_Succ 'Type_Var_Zero))
+-- ^ …aliases only for the first few 'Axiom_Type_Var' used: extend on need.
+
+-- | Return the Haskell term-level 'Int' encoded by the given Haskell type-level @(v :: 'Type_Var')@.
+type_var_int :: Axiom_Type_Var v -> Int
+type_var_int v =
+ case v of
+ Axiom_Type_Var_Zero -> 0
+ Axiom_Type_Var_Succ n -> 1 + type_var_int n
+
+-- | Return a readable 'String' encoding the given Haskell type-level @(v :: 'Type_Var')@.
+--
+-- First 26 variables give: @\"A"@ to @\"Z"@,
+-- and followings give: @(\"A" ++ show n)@, where @n@ is a positive 'Int' starting at @0@.
+type_var_string :: Axiom_Type_Var v -> String
+type_var_string v =
+ case type_var_int v of
+ x | 0 <= x && x < 26 -> [Char.chr (Char.ord 'A' + x)]
+ x -> 'A' : show (x - 26)
+
+-- *** Class 'Type_Var_Implicit'
+class Type_Var_Implicit (v::Type_Var) where
+ type_var :: Axiom_Type_Var v
+instance Type_Var_Implicit 'Type_Var_Zero where
+ type_var = Axiom_Type_Var_Zero
+instance Type_Var_Implicit v => Type_Var_Implicit ('Type_Var_Succ v) where
+ type_var = Axiom_Type_Var_Succ type_var
+
+data instance Axiom (Axiom_Type_Var (v::Type_Var))
+ = Axiom_Type_Var (Axiom_Type_Var v)
+ deriving (Eq, Ord, Show)
+instance Buildable (Axiom (Axiom_Type_Var (v::Type_Var))) where
+ build (Axiom_Type_Var v) = build v
+instance (Typeable v) => Axiomable (Axiom (Axiom_Type_Var (v::Type_Var))) where
+ axiom_type_of _ctx (Axiom_Type_Var _v) =
+ Type_Sort (Type_Level_0, Type_Morphism_Mono)
+instance Type_Var_Implicit v => Axiom_Type (Axiom_Type_Var (v::Type_Var)) where
+ axiom_type = Axiom_Type_Var (type_var::Axiom_Type_Var v)
+ axiom_Type (Axiom_Type_Var v) = TeTy_Var $ Text.pack $ type_var_string v
+
+instance Eq (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
+ Axiom_Term x _ == Axiom_Term y _ = x == y
+instance Ord (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
+ Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
+instance Show (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
+ showsPrec n (Axiom_Term v ty) =
+ showParen (n > 10) $
+ showString "Axiom_Term " .
+ (showParen (n > 10) $
+ showString "Axiom_Type_Var " .
+ showsPrec n v) .
+ showString " " .
+ (showParen (n > 10) $
+ showString " " .
+ showsPrec n (ty context))
+instance Buildable (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
+ build (Axiom_Term v _ty) = build v
+instance Typeable v => Axiomable (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
+ axiom_type_of ctx (Axiom_Term _ ty) = ty ctx
+
+-- Instance 'Axiom' '->'
+data instance Axiom (i -> o)
+ = Axiom_Term_Abst (Axiom i) (Axiom o)
+deriving instance (Eq (Axiom i), Eq (Axiom o)) => Eq (Axiom (i -> o))
+deriving instance (Ord (Axiom i), Ord (Axiom o)) => Ord (Axiom (i -> o))
+deriving instance (Show (Axiom i), Show (Axiom o)) => Show (Axiom (i -> o))
+instance (Buildable (Axiom i), Buildable (Axiom o)) => Buildable (Axiom (i -> o)) where
+ build (Axiom_Term_Abst i o) =
+ "(" <> build i <> " -> " <> build o <> ")"
+instance
+ ( Typeable i
+ , Typeable o
+ , Eq (Axiom i)
+ , Show (Axiom i)
+ , Buildable (Axiom i)
+ , Eq (Axiom o)
+ , Show (Axiom o)
+ , Buildable (Axiom o)
+ -- , Axiomable (Axiom i)
+ -- , Axiomable (Axiom o)
+ ) => Axiomable (Axiom (i -> o)) where
+ axiom_type_of _ctx (Axiom_Term_Abst _i _o) =
+ Type_Sort (Type_Level_0, Type_Morphism_Mono)
+
+instance (Axiom_Type i, Axiom_Type o) => Axiom_Type (i -> o) where
+ axiom_type =
+ Axiom_Term_Abst
+ axiom_type
+ axiom_type
+ axiom_Type (Axiom_Term_Abst i o) =
+ Type_Abst ""
+ (axiom_Type i) $
+ (const Nothing `abstract`) $
+ (axiom_Type o)
+instance Eq (Axiom (Axiom_Term (i -> o))) where
+ (==) = error "Eq Axiom: (==) on functions"
+instance Ord (Axiom (Axiom_Term (i -> o))) where
+ compare = error "Eq Axiom: compare on functions"
+instance
+ {-( Buildable (Axiom (i -> o))
+ ) =>-} Show (Axiom (Axiom_Term (i -> o))) where
+ showsPrec n (Axiom_Term _ ty) =
+ showParen (n > 10) $
+ showString "Axiom_Term " .
+ showString "(_:" .
+ showString (
+ Text.unpack $
+ TL.toStrict $
+ Builder.toLazyText $
+ build (ty context)
+ ) .
+ showString ")"
+instance
+ {-( Buildable (Axiom i)
+ , Buildable (Axiom o)
+ ) =>-} Buildable (Axiom (Axiom_Term (i -> o))) where
+ build (Axiom_Term _o ty) =
+ "(_:" <> build (ty context) <> ")"
+
+instance
+ ( Typeable (Term var)
+ , Typeable o
+ , Axiomable (Axiom (Axiom_Term o))
+ -- , Axiomable (Axiom (Term var))
+ -- , Axiomable (Axiom o)
+ -- , Buildable (Axiom (Term var))
+ -- , Show (Axiom (Axiom_Term (Term var)))
+ -- , Show (Axiom (Axiom_Term o))
+ ) => Axiomable (Axiom (Axiom_Term (Term var -> o))) where
+ axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
+ axiom_normalize (ctx::Context var_)
+ {-ax@-}(Axiom_Term (cast -> Just (o::Term var_ -> o)) o_ty)
+ (arg:args) =
+ {-
+ trace ("axiom_normalize (i -> o): Term"
+ ++ "\n ax=" ++
+ (Text.unpack $
+ TL.toStrict $
+ Builder.toLazyText $
+ build (ax))
+ ++ "\n ax=" ++ show ax
+ ++ "\n ty(ax)=" ++ show (typeOf ax)
+ ++ "\n arg=" ++ show (context_unlift ctx <$> arg)
+ ++ "\n args=" ++ show ((context_unlift ctx <$>) <$> args)
+ ++ "\n o=" ++ show (Axiom_Term (o arg) o_ty)
+ ) $
+ -}
+ case type_of ctx arg of
+ Right i_ty ->
+ case o_ty ctx of
+ Type_Abst _ _o_in o_out ->
+ let oi = o arg in
+ let oi_ty = const i_ty `unabstract` o_out in
+ Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
+ _ -> Nothing
+ _ -> Nothing
+ axiom_normalize _ctx _ax _args = Nothing
+
+instance
+ ( Typeable (Term var -> io)
+ , Typeable o
+ , Typeable io
+ , Axiomable (Axiom (Axiom_Term o))
+ -- , Axiomable (Axiom (Term var -> io))
+ -- , Axiomable (Axiom o)
+ -- , Show (Axiom (Axiom_Term (Term var -> io)))
+ -- , Show (Axiom (Axiom_Term o))
+ ) => Axiomable (Axiom (Axiom_Term ((Term var -> io) -> o))) where
+ axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
+ axiom_normalize
+ (ctx::Context var_)
+ {-ax@-}(Axiom_Term (cast -> Just (o::(Term var_ -> io) -> o)) o_ty)
+ (arg@(Term_Abst _arg_v _arg_f_in arg_f):args) =
+ case type_of ctx arg of
+ Right i_ty ->
+ case o_ty ctx of
+ Type_Abst _ _o_in o_out ->
+ {-
+ trace ("axiom_normalize (i -> o): Term ->"
+ ++ "\n ax=" ++
+ (Text.unpack $
+ TL.toStrict $
+ Builder.toLazyText $
+ build (ax))
+ ++ "\n ax=" ++ show ax
+ ++ "\n args=" ++ show ((context_unlift ctx <$>) <$> args)
+ ++ "\n ty(args)=" ++ show (typeOf <$> args)
+ ++ "\n ty(ax)=" ++ show (typeOf ax)
+ ++ "\n i~" ++ show (typeOf (undefined::Term var -> io))
+ ++ "\n o~" ++ show (typeOf (undefined::o))
+ ++ "\n i=" ++ show (typeOf i)
+ ) $
+ -}
+ let i te =
+ case normalize ctx (const te `unabstract` arg_f) of
+ TeTy_Axiom (axiom_cast -> Just (Axiom_Term io _io_ty)) -> io
+ _ -> error "axiom_normalize: Axiom_Term ((Term var -> io) -> o): cannot extract io"
+ in
+ let oi = o i in
+ let oi_ty = const i_ty `unabstract` o_out in
+ Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
+ _ -> Nothing
+ _ -> Nothing
+ axiom_normalize ctx
+ (Axiom_Term o o_ty)
+ (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
+ =
+ case o_ty ctx of
+ Type_Abst _ _o_in o_out ->
+ let oi = o i in
+ let oi_ty = const (i_ty ctx) `unabstract` o_out in
+ {-
+ trace ("axiom_normalize (i -> o): Term var -> io"
+ ++ (
+ Text.unpack $
+ TL.toStrict $
+ Builder.toLazyText $
+ build (context_unlift ctx <$> oi_ty))
+ ) $
+ -}
+ Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
+ _ -> Nothing
+ axiom_normalize _ctx _ax _args = Nothing
+
+instance
+ ( Typeable (Axiom_Type_Var v -> io)
+ , Typeable o
+ , Axiomable (Axiom (Axiom_Type_Var v -> io))
+ , Axiomable (Axiom o)
+ , Axiomable (Axiom (Axiom_Term o))
+ , Show (Axiom (Axiom_Term (Axiom_Type_Var v -> io)))
+ , Show (Axiom (Axiom_Term o))
+ ) => Axiomable (Axiom (Axiom_Term ((Axiom_Type_Var v -> io) -> o))) where
+ axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
+
+instance
+ ( Typeable Integer
+ , Typeable o
+ , Axiomable (Axiom Integer)
+ , Axiomable (Axiom o)
+ , Axiomable (Axiom (Axiom_Term o))
+ , Show (Axiom (Axiom_Term Integer))
+ , Show (Axiom (Axiom_Term o))
+ ) => Axiomable (Axiom (Axiom_Term (Integer -> o))) where
+ axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
+ axiom_normalize ctx
+ (Axiom_Term o o_ty)
+ (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
+ =
+ case o_ty ctx of
+ Type_Abst _ _o_in o_out ->
+ let oi = o i in
+ let oi_ty = const (i_ty ctx) `unabstract` o_out in
+ {-
+ trace ("axiom_normalize (i -> o): "
+ ++ (
+ Text.unpack $
+ TL.toStrict $
+ Builder.toLazyText $
+ build (context_unlift ctx <$> oi_ty))
+ ) $
+ -}
+ Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
+ _ -> Nothing
+ axiom_normalize _ctx _ax _args = Nothing
+
+instance
+ ( Typeable Text
+ , Typeable o
+ , Axiomable (Axiom Text)
+ , Axiomable (Axiom o)
+ , Axiomable (Axiom (Axiom_Term o))
+ , Show (Axiom (Axiom_Term Text))
+ , Show (Axiom (Axiom_Term o))
+ ) => Axiomable (Axiom (Axiom_Term (Text -> o))) where
+ axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
+ axiom_normalize ctx
+ (Axiom_Term o o_ty)
+ (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
+ =
+ case o_ty ctx of
+ Type_Abst _ _o_in o_out ->
+ let oi = o i in
+ let oi_ty = const (i_ty ctx) `unabstract` o_out in
+ {-
+ trace ("axiom_normalize (i -> o): "
+ ++ (
+ Text.unpack $
+ TL.toStrict $
+ Builder.toLazyText $
+ build (context_unlift ctx <$> oi_ty))
+ ) $
+ -}
+ Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
+ _ -> Nothing
+ axiom_normalize _ctx _ax _args = Nothing
+
+instance
+ ( Typeable (Axiom_Type_Var v)
+ , Typeable o
+ , Axiomable (Axiom (Axiom_Type_Var v))
+ , Axiomable (Axiom o)
+ , Axiomable (Axiom (Axiom_Term o))
+ , Show (Axiom (Axiom_Term (Axiom_Type_Var v)))
+ , Show (Axiom (Axiom_Term o))
+ ) => Axiomable (Axiom (Axiom_Term (Axiom_Type_Var v -> o))) where
+ axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
+ axiom_normalize ctx
+ (Axiom_Term o o_ty)
+ (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
+ =
+ case o_ty ctx of
+ Type_Abst _ _o_in o_out ->
+ let oi = o i in
+ let oi_ty = const (i_ty ctx) `unabstract` o_out in
+ {-
+ trace ("axiom_normalize (i -> o): "
+ ++ (
+ Text.unpack $
+ TL.toStrict $
+ Builder.toLazyText $
+ build (context_unlift ctx <$> oi_ty))
+ ) $
+ -}
+ Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
+ _ -> Nothing
+ axiom_normalize _ctx _ax _args = Nothing
+
+instance
+ ( Typeable (IO a)
+ , Typeable o
+ , Typeable a
+ , Axiomable (Axiom (Axiom_Term o))
+ , Show (Axiom (Axiom_Term (IO a)))
+ , Show (Axiom (Axiom_Term o))
+ -- , Axiomable (Axiom (IO a))
+ -- , Axiomable (Axiom o)
+ ) => Axiomable (Axiom (Axiom_Term (IO a -> o))) where
+ axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
+ axiom_normalize ctx
+ (Axiom_Term o o_ty)
+ (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
+ =
+ case o_ty ctx of
+ Type_Abst _ _o_in o_out ->
+ let oi = o i in
+ let oi_ty = const (i_ty ctx) `unabstract` o_out in
+ {-
+ trace ("axiom_normalize (Axiom_Term ((IO a) -> o)): "
+ ++ (
+ Text.unpack $
+ TL.toStrict $
+ Builder.toLazyText $
+ build (context_unlift ctx <$> oi_ty))
+ ) $
+ -}
+ Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
+ _ -> Nothing
+ axiom_normalize (ctx::Context var)
+ (Axiom_Term o o_ty)
+ (TeTy_Axiom (axiom_cast -> Just (Axiom_Term (i::IO (Term var)) i_ty)):args)
+ =
+ case o_ty ctx of
+ Type_Abst _ _o_in o_out ->
+ let oi = o $
+ (\te ->
+ case normalize ctx te of
+ TeTy_Axiom (axiom_cast -> Just (Axiom_Term io _io_ty)) -> io
+ _ -> error "axiom_normalize: Axiom_Term ((Term var -> io) -> o): cannot extract io"
+ ) <$> i in
+ let oi_ty = const (i_ty ctx) `unabstract` o_out in
+ Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
+ _ -> Nothing
+ axiom_normalize _ctx _ax _args = Nothing
+
+-- ** Type 'Axiom_Type_Abst'
+
+-- | Encode a @forall a.@ within an 'Axiom'.
+data Axiom_Type_Abst
+data instance Axiom (Axiom_Type_Abst)
+ = Axiom_Type_Abst
+ { axiom_type_abst_Var ::
+ (Suggest Var_Name)
+ -- ^ A name for the variable inhabiting the abstracting 'Type'.
+ , axiom_type_abst_Term ::
+ (Type Var_Name -> Term Var_Name)
+ -- ^ The abstracted 'Term', abstracted by a 'Type'.
+ , axiom_type_abst_Type ::
+ (Abstraction (Suggest Var_Name) Type Var_Name)
+ -- ^ The 'Type' of the abstracted 'Term'
+ -- (not exactly a 'Type', but just enough to build it with 'Type_Abst').
+ }
+ deriving (Typeable)
+instance Eq (Axiom (Axiom_Type_Abst)) where
+ Axiom_Type_Abst{} == Axiom_Type_Abst{} =
+ error "Eq Axiom_Type_Abst" -- maybe False (x ==) (cast y)
+instance Show (Axiom (Axiom_Type_Abst)) where
+ show (Axiom_Type_Abst{}) = "Axiom_Type_Abst"
+instance Buildable (Axiom (Axiom_Type_Abst)) where
+ build ax = "(_:" <> (build $ axiom_type_of context ax) <> ")"
+instance Axiomable (Axiom (Axiom_Type_Abst)) where
+ axiom_type_of ctx (Axiom_Type_Abst v _o ty) =
+ Type_Abst v
+ (Type_Sort (Type_Level_0, Type_Morphism_Mono)) $
+ (context_lift ctx <$> ty)
+ axiom_normalize ctx
+ {-ax@-}(Axiom_Type_Abst _ o ty)
+ (arg:args)
+ =
+ let a = context_unlift ctx <$> arg in
+ let ty_a = const a `unabstract` ty in
+ let r = o $ ty_a in
+ {-
+ trace ("axiom_normalize: Axiom_Type_Abst:"
+ ++ "\n a=" ++
+ (Text.unpack $
+ TL.toStrict $
+ Builder.toLazyText $
+ build (a)
+ )
+ ++ "\n ty=" ++
+ (Text.unpack $
+ TL.toStrict $
+ Builder.toLazyText $
+ build (axiom_type_of context ax)
+ )
+ ++ "\n ty_a=" ++
+ (Text.unpack $
+ TL.toStrict $
+ Builder.toLazyText $
+ build (ty_a)
+ )
+ ++ "\n r=" ++
+ (show r
+ )
+ ) $
+ -}
+ Just (context_lift ctx <$> r, args)
+ axiom_normalize _ctx _ax _args = Nothing
+
+-- Instance 'Axiom' 'IO'
+data instance Axiom (IO a)
+ = Axiom_Type_IO
+ deriving (Eq, Ord, Show)
+instance Buildable (Axiom (IO a)) where
+ build _ = "IO"
+instance (Typeable a) => Axiomable (Axiom (IO a)) where
+ axiom_type_of _ctx ax =
+ case ax of
+ Axiom_Type_IO ->
+ -- IO : * -> *
+ Type_Abst "" (Type_Sort sort_star_mono) $
+ (const Nothing `abstract`) $
+ Type_Sort sort_star_mono
+ axiom_eq x y =
+ maybe (
+ case
+ ( Typeable.splitTyConApp (typeOf x)
+ , Typeable.splitTyConApp (typeOf y)
+ ) of
+ ( (xc,[(Typeable.typeRepTyCon -> xc')])
+ , (yc,[(Typeable.typeRepTyCon -> yc')])
+ ) | xc == yc && xc' == yc' -> True
+ _ ->
+ error $ "Eq: Axiomable (Axiom (IO a)): "
+ ++ "\n x : " ++ show (Typeable.splitTyConApp (typeOf x))
+ ++ "\n y : " ++ show (Typeable.splitTyConApp (typeOf y))
+ ) (x ==) (cast y)
+
+instance
+ ( Typeable a
+ , Axiom_Type a
+ ) => Axiom_Type (IO a) where
+ axiom_type = Axiom_Type_IO
+ axiom_Type (Axiom_Type_IO) =
+ TeTy_App
+ (TeTy_Axiom (Axiom_Type_IO::Axiom (IO a)))
+ (axiom_Type (axiom_type::Axiom a))
+
+instance Eq (Axiom (Axiom_Term (IO a))) where
+ (==) = error "Eq Axiom: (==) on IO"
+instance Ord (Axiom (Axiom_Term (IO a))) where
+ compare = error "Eq Axiom: compare on IO"
+instance
+ {-( Buildable (Axiom a)
+ ) =>-} Show (Axiom (Axiom_Term (IO a))) where
+ showsPrec n (Axiom_Term _te ty) =
+ showParen (n > 10) $
+ showString "Axiom_Term " .
+ showString "(_:" .
+ showString (
+ Text.unpack $
+ TL.toStrict $
+ Builder.toLazyText $
+ build $ (ty context)
+ ) .
+ showString ")"
+instance
+ {-( Buildable (Axiom a)
+ ) =>-} Buildable (Axiom (Axiom_Term (IO a))) where
+ build (Axiom_Term _a ty) =
+ "(_:" <> build (ty context) <> ")"
+instance
+ ( Typeable a
+ -- , Buildable (Axiom a)
+ -- , Axiomable (Axiom a)
+ -- , Axiomable (Axiom (Axiom_Term a))
+ ) => Axiomable (Axiom (Axiom_Term (IO a))) where
+ axiom_type_of ctx (Axiom_Term _a ty) = ty ctx
--- /dev/null
+#!/bin/sh -eux
+
+ghc \
+ -main-is Calculus.Lambda.Omega.Explicit.REPL \
+ -prof -fprof-auto -fprof-cafs \
+ ${GHC_FLAGS-} \
+ Calculus/Lambda/Omega/Explicit/REPL.hs
+
+Calculus/Lambda/Omega/Explicit/REPL +RTS -xc "$@"
--- /dev/null
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -fno-warn-tabs #-}
+module Hcompta.Calculus.Explicit.REPL where
+
+import Control.Applicative (Applicative(..), (<$>))
+import Control.Exception
+import Control.Monad
+import Control.Monad.State
+import Data.Bool
+import qualified Data.Char as Char
+import Data.Either (Either(..))
+import Data.Eq (Eq(..))
+import Data.Foldable (Foldable(..))
+import Data.Function (($), (.), const, flip)
+import Data.Functor.Identity
+import Data.List ((++), break, concat, dropWhile, last, reverse)
+import Data.List (isPrefixOf, find)
+import qualified Data.List as List
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import Data.Maybe (Maybe(..))
+import Data.Monoid ((<>))
+import Data.Monoid (Monoid(..))
+import Data.Ord (Ord(..))
+import Data.String (String)
+import Data.Text (Text)
+import qualified Data.Text as Text
+import Data.Text.Buildable (Buildable(..))
+import qualified Data.Text.Lazy as TL
+import qualified Data.Text.Lazy.Builder as Builder
+import Data.Tuple (fst)
+import Data.Typeable as Typeable
+import Prelude (Integer, Num(..), div, error)
+import System.Console.Haskeline
+import System.Directory
+import System.FilePath
+import System.IO (IO, readFile)
+import qualified Text.Parsec as R
+import Text.Show (Show(..))
+
+-- import Debug.Trace
+
+import Calculus.Abstraction.DeBruijn.Generalized
+import Calculus.Lambda.Omega.Explicit
+import Calculus.Lambda.Omega.Explicit.Read
+
+-- * Type 'REPL'
+
+-- | /Read Eval Print Loop/ monad.
+newtype REPL a
+ = REPL
+ { unREPL :: StateT REPL_State (InputT IO) a }
+ deriving ( Functor
+ , Applicative
+ , Monad
+ , MonadIO
+ , MonadState REPL_State )
+
+data REPL_State
+ = REPL_State
+ { repl_state_env :: Env
+ , repl_state_load_dir :: FilePath
+ , repl_state_load_done :: Map FilePath ()
+ }
+
+main :: IO ()
+main = do
+ cwd <- getCurrentDirectory
+ runInputT defaultSettings $
+ evalStateT (unREPL main_loop) $
+ REPL_State
+ { repl_state_env = prelude axioms
+ , repl_state_load_dir = cwd
+ , repl_state_load_done = mempty
+ }
+ where
+ main_loop :: REPL ()
+ main_loop = do
+ let prompt = "> "
+ line <- repl_read_command prompt
+ case slice <$> line of
+ Just (cmd, input) | (not (length cmd > 1 && cmd `isPrefixOf` "quit")) ->
+ dispatch cmd input
+ _ -> return ()
+ main_loop
+
+slice :: String -> (String, String)
+slice (':':str) = break Char.isSpace str
+slice str = ("", str)
+
+
+-- ** I/O
+print :: Buildable a => a -> TL.Text
+print = Builder.toLazyText . build
+
+repl_write_string_ln :: String -> REPL ()
+repl_write_string_ln = REPL . lift . outputStrLn
+
+repl_write_string :: String -> REPL ()
+repl_write_string = REPL . lift . outputStr
+
+repl_show :: Show a => a -> REPL ()
+repl_show = repl_write_string_ln . show
+
+repl_print :: Buildable a => a -> REPL ()
+repl_print = repl_write_string . TL.unpack . print
+
+repl_print_ln :: Buildable a => a -> REPL ()
+repl_print_ln = repl_write_string_ln . TL.unpack . print
+
+repl_read :: Parser Identity x -> String -> (x -> REPL ()) -> REPL ()
+repl_read _p [] _k = return ()
+repl_read p s k =
+ case runIdentity $ read p s of
+ Right x -> k x
+ Left err -> do
+ repl_write_string_ln "Parsing error:"
+ repl_show err
+ repl_write_string " Command_Input: "
+ repl_write_string_ln s
+
+-- ** Commands
+repl_read_command :: String -> REPL (Maybe String)
+repl_read_command prompt = do
+ line <- REPL . lift $ getInputLine prompt
+ case line of
+ Just s@(':':_) -> return $ Just s
+ Just l@(_:_) | last l == ' ' -> parse_block l
+ Just s -> return $ Just s
+ Nothing -> return Nothing
+ where
+ parse_block :: String -> REPL (Maybe String)
+ parse_block s = do
+ line <- REPL . lift $ getInputLine ""
+ case line of
+ Just l@(_:_) | last l == ' ' -> parse_block (s ++ '\n' : l)
+ _ -> return $ Just s
+
+type Command_Name = String
+type Command = Command_Input -> IO Command_Output
+
+command :: Command_Name -> Command
+command "" = command "let"
+command cmd =
+ case find (\p -> cmd `isPrefixOf` fst p) commands of
+ Nothing -> (\_ -> return $ Left $ Error_Command cmd)
+ Just (_, c) -> c
+ where
+ commands :: [(String, Command)]
+ commands =
+ [ ("assume", command_assume) -- Type -> IO ()
+ , ("code" , command_code) -- Var -> Term
+ , ("dump" , command_dump) -- Term -> Text
+ , ("equiv", command_equiv) -- Term -> Term -> Bool
+ -- , ("echo" , command_echo) -- Term -> Term
+ , ("let" , command_let) -- Var -> Term -> IO ()
+ , ("load" , command_load) -- FilePath -> IO ()
+ , ("nf" , command_normalize normalize) -- Term -> Term
+ , ("nf_dump", command_normalize_dump normalize) -- Term -> Term
+ , ("reset", command_reset) -- () -> IO ()
+ , ("type" , command_type) -- Term -> Type
+ , ("type_dump", command_type_dump) -- Term -> Text
+ , ("whnf" , command_normalize whnf) -- Term -> Term
+ ]
+command_run :: Command_Name -> Command
+command_run cmd (Command_Input i st) = do
+ command cmd $
+ Command_Input (strip_spaces i) st
+ where
+ strip_spaces =
+ reverse . dropWhile Char.isSpace .
+ reverse . dropWhile Char.isSpace
+
+dispatch :: Command_Name -> String -> REPL ()
+dispatch cmd i = do
+ st <- get
+ output <- liftIO $ command_run cmd (Command_Input i st)
+ case output of
+ Left (err::Error) ->
+ repl_print err
+ Right (Command_Result msg new_st) -> do
+ case TL.unpack $ print msg of
+ [] -> return ()
+ o -> repl_write_string_ln o
+ put new_st
+
+data Command_Input
+ = Command_Input String REPL_State
+type Command_Output
+ = Either Error Command_Result
+data Error
+ = Error_Parse String R.ParseError
+ | Error_Type Type_Error
+ | Error_Let Var_Name Type_Error
+ | Error_Code Var_Name
+ | Error_Command Command_Name
+ | Error_IO IOException
+ | Error_Load FilePath Error
+ deriving (Show)
+instance Buildable Error where
+ build err =
+ case err of
+ Error_Parse s e -> "Error: parsing: " <> build s <> "\n" <> build (show e) <> "\n"
+ Error_Type e -> build e
+ Error_Let var e -> "Error: in let: " <> build var <> "\n " <> build e
+ Error_Code var -> "Error: no such variable in environment: " <> build var
+ Error_Command cmd -> "Error: unrecognized command: " <> build cmd <> "\n"
+ Error_IO e -> "Error: " <> build (show e) <> "\n"
+ Error_Load file e ->
+ "Error: loading: " <> build file <> "\n"
+ <> build e
+data Command_Result
+ = forall msg.
+ ( Buildable msg
+ ) => Command_Result msg REPL_State
+
+command_assume :: Command
+command_assume (Command_Input str st) =
+ return $
+ let ctx = context_from_env $ repl_state_env st in
+ case runIdentity $ read parse_assume str of
+ Left err -> Left $ Error_Parse str err
+ Right (v, ty) ->
+ case type_of ctx ty of
+ Left err -> Left $ Error_Type err
+ Right _ty_ty -> Right $
+ Command_Result (""::Text) $
+ st{repl_state_env = env_insert v
+ (TeTy_Axiom (Axiom_Type_Assume ty)) ty $
+ repl_state_env st
+ }
+
+command_code :: Command
+command_code (Command_Input str st) =
+ return $
+ let env = repl_state_env st in
+ case runIdentity $ read parse_var_name str of
+ Left err -> Left $ Error_Parse str err
+ Right var ->
+ case Map.lookup var env of
+ Nothing -> Left $ Error_Code var
+ Just item -> Right $ Command_Result
+ (form_given $ env_item_term item)
+ st
+
+command_dump :: Command
+command_dump (Command_Input str st) =
+ return $
+ case runIdentity $ read parse_term str of
+ Left err -> Left $ Error_Parse str err
+ Right te -> Right $ Command_Result (show te) st
+
+command_let :: Command
+command_let (Command_Input [] st) =
+ return $ Right $ Command_Result (""::Text) st
+command_let (Command_Input str st) =
+ let toks_or_err = runIdentity $ lex lex_all str in
+ case toks_or_err of
+ Left err -> return $ Left $ Error_Parse str err
+ Right [] -> return $ Right $ Command_Result (""::Text) st
+ Right toks ->
+ case runIdentity $ parse parse_let_or_term toks of
+ Left err -> return $ Left $ Error_Parse str err
+ Right let_or_term -> do
+ let ctx = context_from_env $ repl_state_env st
+ case let_or_term of
+ Left (v, mty, te) ->
+ let ety = case mty of
+ Nothing -> type_of ctx te
+ Just ty -> do
+ _ty_ty <- type_of ctx ty
+ const ty <$> check ctx (context_apply ctx ty) te
+ in
+ return $
+ case ety of
+ Left err -> Left $ Error_Let v err
+ Right ty -> do
+ Right $ Command_Result (build v <> " : " <> build ty) $
+ st{repl_state_env = env_insert v te ty $ repl_state_env st}
+ Right let_te ->
+ case type_of ctx let_te of
+ Left err -> return $ Left $ Error_Type err
+ Right _ty ->
+ let norm_te = normalize ctx let_te in
+ case norm_te of
+ TeTy_Axiom (axiom_cast -> Just (Axiom_Term (io::IO (Term Var_Name)) _o_ty)) -> do
+ io_te <- io
+ return $ Right $ Command_Result io_te st
+ _ ->
+ return $ Right $ Command_Result norm_te st
+
+command_load :: Command
+command_load (Command_Input file input_st) = do
+ err_or_io <- try $ do
+ path <- canonicalizePath (repl_state_load_dir input_st </> file)
+ content <- readFile path
+ return (path, content)
+ case err_or_io of
+ Left (err::IOException) -> return $ Left $ Error_IO err
+ Right (modul, content) -> do
+ case Map.lookup modul $ repl_state_load_done input_st of
+ Just _ -> return $ Right $
+ Command_Result ("Module already loaded: " ++ modul) input_st
+ _ ->
+ case runIdentity $ R.runParserT (parse_commands <* R.eof) () modul content of
+ Left err -> return $ Left $ Error_Load modul $ Error_Parse content err
+ Right cmds -> do
+ let old_dir = repl_state_load_dir input_st
+ err_or_st <-
+ foldM (\err_or_st (cmd, i) ->
+ case err_or_st of
+ Left _ -> return $ err_or_st
+ Right (Command_Result last_msg last_st) -> do
+ o <- command_run cmd (Command_Input i last_st)
+ case o of
+ Left _ -> return o
+ Right (Command_Result msg running_st) ->
+ return $ Right $
+ Command_Result (build last_msg <> "\n" <> build msg) running_st
+ )
+ (Right $ Command_Result ("Loading: " <> modul)
+ input_st{repl_state_load_dir = takeDirectory modul})
+ ({-trace ("cmds: " ++ show cmds)-} cmds)
+ return $
+ case err_or_st of
+ Left err -> Left $ Error_Load modul $ err
+ Right (Command_Result msg result_st) ->
+ Right $ Command_Result msg $ result_st
+ { repl_state_load_dir = old_dir
+ , repl_state_load_done =
+ Map.insert modul () $
+ repl_state_load_done result_st
+ }
+
+command_normalize
+ :: (Context Var_Name -> Term Var_Name -> Term Var_Name)
+ -> Command
+command_normalize norm (Command_Input str st) = do
+ let ctx = context_from_env $ repl_state_env st
+ case runIdentity $ read parse_term str of
+ Left err -> return $ Left $ Error_Parse str err
+ Right (te::Term Var_Name) ->
+ let n_te = norm ctx te in
+ case n_te of
+ TeTy_Axiom (axiom_cast -> Just (Axiom_Term (o::IO (Term Var_Name)) _o_ty)) -> do
+ r <- o
+ return $ Right $ Command_Result r st
+ TeTy_Axiom (axiom_cast -> Just (Axiom_Term (o::IO Text) _o_ty)) -> do
+ r <- o
+ return $ Right $ Command_Result r st
+ _ ->
+ return $ Right $ Command_Result n_te st
+
+command_equiv :: Command
+command_equiv (Command_Input str st) = do
+ let ctx = context_from_env $ repl_state_env st
+ return $
+ case runIdentity $ read ((,) <$> parse_term <* (parse_token Token_Equal >> parse_token Token_Equal) <*> parse_term) str of
+ Left err -> Left $ Error_Parse str err
+ Right (x_te, y_te) -> Right $
+ Command_Result (if equiv ctx x_te y_te then "True" else "False"::Text) st
+
+command_normalize_dump
+ :: (Context Var_Name -> Term Var_Name -> Term Var_Name)
+ -> Command
+command_normalize_dump norm (Command_Input str st) = do
+ let ctx = context_from_env $ repl_state_env st
+ return $
+ case runIdentity $ read parse_term str of
+ Left err -> Left $ Error_Parse str err
+ Right te -> Right $ Command_Result (show $ norm ctx te) st
+
+command_reset :: Command
+command_reset (Command_Input _ st) =
+ return $ Right $
+ Command_Result (""::Text) st{repl_state_env = mempty}
+
+command_type :: Command
+command_type (Command_Input [] st) = do
+ let env = repl_state_env st
+ return $
+ Right $ Command_Result
+ (
+ foldr (flip (<>)) "" $
+ List.intersperse "\n" $
+ (\(name, item) ->
+ build name <> " : "
+ <> build (form_given $ env_item_type item))
+ <$> (Map.toList env)
+ )
+ st
+command_type (Command_Input str st) = do
+ let ctx = context_from_env $ repl_state_env st
+ return $
+ case runIdentity $ read parse_term str of
+ Left err -> Left $ Error_Parse str err
+ Right te ->
+ case type_of ctx te of
+ Left err -> Left $ Error_Type err
+ Right ty -> Right $ Command_Result (normalize ctx ty) st
+
+command_type_dump :: Command
+command_type_dump (Command_Input [] st) = do
+ let env = repl_state_env st
+ return $
+ Right $ Command_Result
+ (
+ foldr (flip (<>)) "" $
+ List.intersperse "\n" $
+ (\(name, item) ->
+ build name <> " : "
+ <> build (show $ form_given $ env_item_type item))
+ <$> (Map.toList env)
+ )
+ st
+command_type_dump (Command_Input str st) = do
+ let ctx = context_from_env $ repl_state_env st
+ return $
+ case runIdentity $ read parse_term str of
+ Left err -> Left $ Error_Parse str err
+ Right te ->
+ case type_of ctx te of
+ Left err -> Left $ Error_Type err
+ Right ty -> Right $ Command_Result (show $ normalize ctx ty) st
+
+{-
+command_echo :: String -> REPL ()
+command_echo str =
+ repl_read parse_term str repl_print_ln
+-}
+
+-- * Builtins
+
+builtin :: Axioms -> [Text] -> Env
+builtin =
+ foldl $ \env str ->
+ let ctx = context_from_env env in
+ read_string parse_let str $ \(v, mty, te) ->
+ let ety = case mty of
+ Just ty -> do
+ _ty_ty <- type_of ctx ty
+ const ty <$> check ctx (context_apply ctx ty) te
+ Nothing -> type_of ctx te in
+ case ety of
+ Left err -> error $ show err
+ Right ty -> env_insert v te ty env
+ where
+ read_string p s k =
+ case runIdentity $ read p s of
+ Right x -> k x
+ Left err -> error $
+ "Parsing_error:\n" ++ show err
+ ++ " Input: " ++ Text.unpack s
+
+axioms :: Axioms
+axioms =
+ (axioms_monopoly <>) $
+ (Map.fromList axioms_io <>) $
+ (Map.fromList axioms_int <>) $
+ (Map.fromList axioms_text <>) $
+ Map.fromList
+ [ ("Unit", item $ Axiom_Type_Unit)
+ ]
+ where
+ item :: (Axiomable (Axiom ax), Typeable ax) => Axiom ax -> Env_Item
+ item = env_item_from_axiom context
+ {-
+ axioms_arr =
+ [ -- ("Arr", item $ Axiom_Term_Abst)
+ ]
+ -}
+ axioms_text =
+ [ ("Text" , item $ Axiom_Type_Text)
+ , ("text_empty", item $ axiom_term (""::Text))
+ , ("text_hello", item $ axiom_term ("Hello World!"::Text))
+ ]
+ axioms_int =
+ [ ("Int" , item $ Axiom_Type_Integer)
+ , ("int_zero" , item $ axiom_term (0::Integer))
+ , ("int_one" , item $ axiom_term (1::Integer))
+ , ("int_add" , item $ axiom_term ((+)::Integer -> Integer -> Integer))
+ , ("int_neg" , item $ axiom_term (negate::Integer -> Integer))
+ , ("int_sub" , item $ axiom_term ((-)::Integer -> Integer -> Integer))
+ , ("int_mul" , item $ axiom_term ((*)::Integer -> Integer -> Integer))
+ , ("int_div" , item $ axiom_term (div::Integer -> Integer -> Integer))
+ ]
+ axioms_io =
+ [ ("IO" , item $ (Axiom_Type_IO::Axiom (IO A)))
+ , ("return_io", item $ return_io)
+ , ("bind_io" , item $ bind_io)
+ , ("join_io" , item $ join_io)
+ -- , ("return_io_text", item $ axiom_term $ (return::Text -> IO Text))
+ -- , ("return_io_int", item $ Axiom_Term $ (return::Int -> IO Int))
+ ]
+ where
+ -- | @return_io : ∀(A:*) -> A -> IO A@
+ return_io :: Axiom (Axiom_Type_Abst)
+ return_io =
+ Axiom_Type_Abst "A" (TeTy_Axiom . ax_te) ax_ty
+ where
+ ax_te :: Type Var_Name
+ -> Axiom (Axiom_Term (Term Var_Name -> IO (Term Var_Name)))
+ ax_te ty = Axiom_Term return (\ctx -> context_lift ctx <$> ty)
+ ax_ty :: Abstraction (Suggest Var_Name) Type Var_Name
+ ax_ty =
+ (("A" =?) `abstract`) $
+ axiom_type_of context $
+ axiom_term (return::A -> IO A)
+
+ -- | @bind_io : ∀(A:*) -> ∀(B:*) -> IO A -> (A -> IO B) -> IO B@
+ bind_io :: Axiom Axiom_Type_Abst
+ bind_io = ax1_te
+ where
+ ax1_te :: Axiom Axiom_Type_Abst
+ ax1_te =
+ Axiom_Type_Abst "A"
+ (\(Type_Abst _ _ ty_a_abst) ->
+ TeTy_Axiom $
+ Axiom_Type_Abst "B"
+ (TeTy_Axiom . ax0_te)
+ ty_a_abst)
+ ax1_ty
+ ax1_ty =
+ (("A" =?) `abstract`) $
+ Type_Abst "B"
+ (Type_Sort (Type_Level_0, Type_Morphism_Mono)) $
+ ax0_ty
+
+ ax0_te
+ :: Type Var_Name
+ -> Axiom (Axiom_Term
+ ( IO (Term Var_Name)
+ -> (Term Var_Name -> IO (Term Var_Name))
+ -> IO (Term Var_Name)
+ ))
+ ax0_te ty =
+ Axiom_Term (>>=) (\ctx -> context_lift ctx <$> ty)
+ ax0_ty =
+ (("B" =?) `abstract`) $
+ axiom_type_of context $
+ axiom_term ((>>=)::IO A -> (A -> IO B) -> IO B)
+
+ -- | @join_io : ∀(A:*) -> IO (IO A) -> IO A@
+ join_io :: Axiom Axiom_Type_Abst
+ join_io = ax1_te
+ where
+ ax1_te :: Axiom Axiom_Type_Abst
+ ax1_te =
+ Axiom_Type_Abst "A"
+ (\ty_a ->
+ TeTy_Axiom $
+ Axiom_Term
+ (join::IO (IO (Term Var_Name)) -> IO (Term Var_Name))
+ (\ctx -> context_lift ctx <$> ty_a))
+ ax1_ty
+ ax1_ty =
+ (("A" =?) `abstract`) $
+ axiom_type_of context $
+ axiom_term (join::IO (IO A) -> IO A)
+
+prelude :: Axioms -> Env
+prelude axs =
+ builtin axs $ concat $ (Text.unlines <$>) <$>
+ [ prelude_bool
+ , prelude_either
+ ]
+ where
+ prelude_bool :: [[Text]]
+ prelude_bool =
+ [ ["Bool_Polytype : *p = (R:*) -> R -> R -> R"]
+ , ["Bool : *m = Monotype Bool_Polytype"]
+ , ["True : Bool = monotype Bool_Polytype (λ(R:*) (True:R) (False:R) -> True)"]
+ , ["False : Bool = monotype Bool_Polytype (λ(R:*) (True:R) (False:R) -> False)"]
+ , [ "eq (x:Bool) (y:Bool) : Bool"
+ , " = monotype Bool_Polytype"
+ , " (λ(R:*) (True:R) (False:R) ->"
+ , " polytype Bool_Polytype x R"
+ , " (polytype Bool_Polytype y R True False)"
+ , " (polytype Bool_Polytype y R False True)"
+ , " )"
+ ]
+ , [ "and (x:Bool) (y:Bool) : Bool"
+ , " = monotype Bool_Polytype"
+ , " (λ(R:*) (True:R) (False:R) ->"
+ , " polytype Bool_Polytype x R"
+ , " (polytype Bool_Polytype y R True False)"
+ , " (polytype Bool_Polytype y R False False)"
+ , " )"
+ ]
+ , [ "or (x:Bool) (y:Bool) : Bool"
+ , " = monotype Bool_Polytype"
+ , " (λ(R:*) (True:R) (False:R) ->"
+ , " polytype Bool_Polytype x R"
+ , " (polytype Bool_Polytype y R True True)"
+ , " (polytype Bool_Polytype y R True False)"
+ , " )"
+ ]
+ , [ "xor (x:Bool) (y:Bool) : Bool"
+ , " = monotype Bool_Polytype"
+ , " (λ(R:*) (True:R) (False:R) ->"
+ , " polytype Bool_Polytype x R"
+ , " (polytype Bool_Polytype y R False True)"
+ , " (polytype Bool_Polytype y R True False)"
+ , " )"
+ ]
+ , [ "not (x:Bool) : Bool"
+ , " = monotype Bool_Polytype"
+ , " (λ(R:*) (True:R) (False:R) ->"
+ , " polytype Bool_Polytype x R False True)"
+ ]
+ ]
+ prelude_either :: [[Text]]
+ prelude_either =
+ [ ["Either_Polytype (A:*) (B:*) : *p = (R:*) -> (A -> R) -> (B -> R) -> R"]
+ , ["Either (A:*) (B:*) : *m = Monotype (Either_Polytype A B)"]
+ , [ "Left (A:*) (B:*) (x:A)"
+ , " : Either A B"
+ , " = monotype (Either_Polytype A B)"
+ , " (λ(R:*) (Left:A -> R) (Right:B -> R) -> Left x)"
+ ]
+ , [ "Right (A:*) (B:*) (x:B)"
+ , " : Either A B"
+ , " = monotype (Either_Polytype A B)"
+ , " (λ(R:*) (Left:A -> R) (Right:B -> R) -> Right x)"
+ ]
+ , [ "either (A:*) (B:*) (R:*) (l:A -> R) (r:B -> R) (e:Either A B) : R"
+ , " = polytype (Either_Polytype A B) e R l r"
+ ]
+ ]
--- /dev/null
+#!/bin/sh -eux
+
+ghc \
+ -main-is Calculus.Lambda.Omega.Explicit.REPL \
+ ${GHC_FLAGS-} \
+ Calculus/Lambda/Omega/Explicit/REPL.hs
+
+Calculus/Lambda/Omega/Explicit/REPL "$@"
--- /dev/null
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE TupleSections #-}
+{-# OPTIONS_GHC -fno-warn-tabs #-}
+module Calculus.Lambda.Omega.Explicit.Read where
+
+import Control.Applicative (Alternative(..), Applicative(..), (<$>), (<$))
+import qualified Control.Applicative as Applicative
+import Control.Monad
+import Data.Bool
+import Data.Char (Char)
+import qualified Data.Char as Char
+import Data.Either (Either(..))
+import Data.Eq (Eq(..))
+import Data.Foldable (Foldable(..))
+import Data.Function (($), (.), flip)
+import qualified Data.List as List
+import Data.Maybe (Maybe(..))
+import Data.Maybe (catMaybes)
+import Data.Text (Text)
+import Data.String (String)
+import qualified Data.Text as Text
+import Text.Parsec ((<?>))
+import qualified Text.Parsec as R
+import Text.Show (Show(..))
+
+-- import Debug.Trace
+
+import Calculus.Abstraction.DeBruijn.Generalized
+import Calculus.Lambda.Omega.Explicit
+
+-- * Type 'Lexer'
+type Lexer s m a
+ = R.Stream s m Char
+ => R.ParsecT s Lexer_State m a
+type Lexer_State = ()
+
+-- ** Type 'Token'
+-- | A lexed token.
+data Token
+ = Token_Arrow
+ | Token_Type_0
+ | Token_Equal
+ | Token_Colon
+ | Token_Lambda
+ | Token_Name Text
+ | Token_Paren_Close
+ | Token_Paren_Open
+ | Token_Pi
+ deriving (Eq, Show)
+
+-- | A lexed token with location information attached
+data Lexed_Token
+ = Lexed_Token Token R.SourcePos
+ deriving (Show)
+
+-- | Remove location information from a 'Lexed_Token'
+lexed_token :: Lexed_Token -> Token
+lexed_token (Lexed_Token tok _) = tok
+
+lex
+ :: R.Stream s m Char
+ => Lexer s m a
+ -> s -> m (Either R.ParseError a)
+lex l = R.runParserT l () ""
+
+lex_all :: Lexer s m [Lexed_Token]
+lex_all =
+ catMaybes
+ <$> R.many lex_token_or_whitespace
+ <* R.eof
+
+-- | Lex either one token or some whitespace
+lex_token_or_whitespace :: Lexer s m (Maybe Lexed_Token)
+lex_token_or_whitespace =
+ (<|>)
+ (Nothing <$ R.try lex_whitespace)
+ (Just <$> lex_token)
+
+lex_whitespace :: Lexer s m ()
+lex_whitespace =
+ R.choice
+ [ () <$ Applicative.some R.space
+ , lex_comment_block
+ , lex_comment_line
+ ]
+
+-- | Lex a @{- ... -}@ comment (perhaps nested).
+lex_comment_block :: Lexer s m ()
+lex_comment_block = R.try (R.string "{-") *> lex_comment_body
+
+-- | Lex a block comment, without the opening.
+lex_comment_body :: Lexer s m ()
+lex_comment_body =
+ R.choice
+ [ lex_comment_block *> lex_comment_body
+ , R.try (R.string "-}") *> return ()
+ , R.anyChar *> lex_comment_body
+ ]
+
+lex_comment_line :: Lexer s m ()
+lex_comment_line =
+ R.try (R.string "--")
+ *> R.manyTill R.anyChar (R.eof <|> (() <$ R.newline))
+ *> return ()
+
+lex_token :: Lexer s m Lexed_Token
+lex_token =
+ Lexed_Token
+ <$> R.choice
+ [ lex_symbol
+ , lex_word
+ -- , Token_Int . fromInteger <$> R.natural R.haskell
+ ]
+ <*> R.getPosition
+
+-- | Lex one non-alphanumeric token
+lex_symbol :: Lexer s m Token
+lex_symbol = R.choice
+ [ Token_Arrow <$ (R.try (R.string "->") <|> R.string "→")
+ , Token_Colon <$ R.char ':'
+ , Token_Equal <$ R.char '='
+ , Token_Lambda <$ (R.char '\\' <|> R.char 'λ')
+ , Token_Type_0 <$ R.char '*'
+ , Token_Paren_Close <$ R.char ')'
+ , Token_Paren_Open <$ R.char '('
+ , Token_Pi <$ (R.string "\\/" <|> R.string "Π" <|> R.string "∀")
+ ]
+
+lex_word :: Lexer s m Token
+lex_word = tokenify <$> lex_name
+ where
+ tokenify name = Token_Name (Text.pack name)
+
+lex_name :: Lexer s m String
+lex_name = (:)
+ <$> (R.letter <|> R.char '_')
+ <*> (R.many (R.alphaNum <|> R.char '_'))
+
+-- * Type 'Parser'
+type Parser m a
+ = R.Stream [Lexed_Token] m Lexed_Token
+ => R.ParsecT [Lexed_Token] Parser_State m a
+type Parser_State = ()
+
+read
+ :: (R.Stream s m Char, Monad m)
+ => Parser m a -> s -> m (Either R.ParseError a)
+read p s = do
+ toks <- lex lex_all s
+ case toks of
+ Left err -> return $ Left err
+ Right ts -> parse p ts
+
+parse
+ :: R.Stream [Lexed_Token] m Lexed_Token
+ => Parser m a
+ -> [Lexed_Token]
+ -> m (Either R.ParseError a)
+parse p = R.runParserT (p <* R.eof) () ""
+
+-- | Like 'R.updatePosChar' but working on 'Lexed_Token'.
+updatePosToken
+ :: R.SourcePos -- ^ position of the current token
+ -> Lexed_Token -- ^ current token
+ -> [Lexed_Token] -- ^ remaining tokens
+ -> R.SourcePos -- ^ position of the next token
+updatePosToken pos _ [] = pos
+updatePosToken _ _ (Lexed_Token _ pos : _) = pos
+
+-- | Parse a nullary token.
+parse_token
+ :: Token -> Parser m ()
+parse_token t =
+ R.tokenPrim
+ show updatePosToken
+ (guard . (t ==) . lexed_token)
+
+-- | Parse an unary token.
+parse_token_1
+ :: (Token -> Maybe a)
+ -> Parser m a
+parse_token_1 untoken =
+ R.tokenPrim
+ show updatePosToken
+ (untoken . lexed_token)
+
+-- | 'parse_term' @::=@ 'parse_term_abst' @|@ 'parse_type_abst'
+parse_term :: Parser m (Term Var_Name)
+parse_term =
+ R.try parse_term_abst
+ <|> parse_type_abst
+ <?> "term"
+
+parse_sort :: Parser m (Type Var_Name)
+parse_sort =
+ Type_Sort . (Type_Level_0,)
+ <$ parse_token Token_Type_0
+ <*> R.option Type_Morphism_Mono
+ (parse_token_1 $ \tok -> case tok of
+ Token_Name "m" -> Just Type_Morphism_Mono
+ Token_Name "p" -> Just Type_Morphism_Poly
+ _ -> Nothing)
+ <?> "sort"
+
+parse_var_name :: Parser m Var_Name
+parse_var_name =
+ parse_token_1 (\tok ->
+ case tok of
+ Token_Name "_" -> Nothing
+ Token_Name n -> Just n
+ _ -> Nothing)
+ <?> "variable-name"
+
+parse_var_def :: Parser m Var_Name
+parse_var_def =
+ parse_token_1 (\tok ->
+ case tok of
+ Token_Name "_" -> Just ""
+ Token_Name n -> Just n
+ _ -> Nothing)
+ <?> "variable-definition"
+
+parse_var :: Parser m (Term Var_Name)
+parse_var =
+ TeTy_Var
+ <$> parse_var_name
+ <?> "variable"
+
+-- | 'parse_app' @::=@ 'parse_atom'@+@
+parse_app :: Parser m (Term Var_Name)
+parse_app =
+ List.foldl1 TeTy_App
+ <$> R.many1 (R.try parse_atom)
+ <?> "application"
+
+-- | 'parse_atom' @::=@ 'parse_sort' @|@ 'parse_var' @|@ @"("@ 'parse_term @")"@
+parse_atom :: Parser m (Term Var_Name)
+parse_atom =
+ R.try parse_sort
+ <|> R.try parse_var
+ <|> R.between
+ (parse_token Token_Paren_Open)
+ (parse_token Token_Paren_Close)
+ parse_term
+ <?> "atom"
+
+-- | 'parse_term_abst' @::=@ @"\"@ 'parse_term_abst_decl'@+@ @"->"@ 'parse_term'
+parse_term_abst :: Parser m (Term Var_Name)
+parse_term_abst =
+ (flip $ foldr (\(x, f_in) t ->
+ Term_Abst (Suggest x) f_in ((x =?) `abstract` t)))
+ <$ parse_token Token_Lambda
+ <*> R.many1 parse_term_abst_decl
+ <* parse_token Token_Arrow
+ <*> parse_term
+ <?> "term_abst"
+
+-- | 'parse_term_abst_decl' @::=@ @"("@ 'parse_var_def' @":"@ 'parse_type' @")"@
+parse_term_abst_decl :: Parser m (Var_Name, Type Var_Name)
+parse_term_abst_decl =
+ (,)
+ <$ parse_token Token_Paren_Open
+ <*> parse_var_def
+ <* parse_token Token_Colon
+ <*> parse_type
+ <* parse_token Token_Paren_Close
+ <?> "term_abst_decl"
+
+-- | 'parse_type_abst_decl' @::=@ @"("@ @(@ 'parse_var_def' @":"@ @)?@ 'parse_type' @")"@
+parse_type_abst_decl :: Parser m (Var_Name, Type Var_Name)
+parse_type_abst_decl =
+ (,)
+ <$ parse_token Token_Paren_Open
+ <*> R.option "" (R.try parse_var_def <* parse_token Token_Colon)
+ <*> parse_type
+ <* parse_token Token_Paren_Close
+ <?> "type_abst_decl"
+
+-- | 'parse_type_abst' @::=@ @(@ 'parse_app' @|@ 'parse_type_abst_decl' @)@ @"->"@ 'parse_type_abst' @|@ 'parse_app'
+parse_type_abst :: Parser m (Term Var_Name)
+parse_type_abst =
+ (R.try
+ ((\(x, f_in) f_out ->
+ Type_Abst (Suggest x) f_in ((x =?) `abstract` f_out))
+ <$> (
+ (R.try (("",) <$> parse_app))
+ <|>
+ (R.option () (parse_token Token_Pi)
+ *> parse_type_abst_decl)
+ )
+ <* parse_token Token_Arrow
+ <*> parse_type_abst))
+ <|> parse_app
+ <?> "type_abst"
+
+-- | 'parse_type' @::=@ 'parse_term'
+parse_type :: Parser m (Term Var_Name)
+parse_type =
+ parse_term <?> "type"
+
+parse_let_or_term :: Parser m (Either (Var_Name, Maybe (Type Var_Name), Term Var_Name) (Term Var_Name))
+parse_let_or_term =
+ R.option
+ Right
+ (R.try ((\name args maybe_ty te ->
+ Left
+ ( name
+ , (\ty -> foldr (\(x, x_ty) t ->
+ Type_Abst (Suggest x) x_ty ((x =?) `abstract` t)) ty args
+ ) <$> maybe_ty
+ , foldr (\(x, x_ty) t ->
+ Term_Abst (Suggest x) x_ty ((x =?) `abstract` t)) te args
+ )
+ )<$> parse_var_name
+ <*> R.many parse_term_abst_decl
+ <*> (<|>)
+ (R.try (Just
+ <$ parse_token Token_Colon
+ <*> parse_type))
+ (pure Nothing)
+ <* parse_token Token_Equal
+ ))
+ <*> parse_term
+
+-- | 'parse_let' @::=@ 'parse_var_name' @(@'parse_term_abst_decl'@)*@ @"="@ 'parse_term'
+parse_let :: Parser m (Var_Name, Maybe (Type Var_Name), Term Var_Name)
+parse_let =
+ (\name args maybe_ty te ->
+ ( name
+ , (\ty -> foldr (\(x, x_ty) t ->
+ Type_Abst (Suggest x) x_ty ((x =?) `abstract` t)) ty args
+ ) <$> maybe_ty
+ , foldr (\(x, x_ty) t ->
+ Term_Abst (Suggest x) x_ty ((x =?) `abstract` t)) te args
+ )
+ )<$> parse_var_name
+ <*> R.many parse_term_abst_decl
+ <*> (<|>)
+ (R.try (Just
+ <$ parse_token Token_Colon
+ <*> parse_type))
+ (pure Nothing)
+ <* parse_token Token_Equal
+ <*> parse_term
+ <?> "let"
+
+-- | 'parse_assume' @::=@ 'parse_var_name' @":"@ 'parse_type'
+parse_assume :: Parser m (Var_Name, Type Var_Name)
+parse_assume =
+ (,)
+ <$> parse_var_name
+ <* parse_token Token_Colon
+ <*> parse_type
+ <?> "axiom"
+
+parse_command
+ :: R.Stream s m Char
+ => R.ParsecT s () m (String, String)
+parse_command =
+ (,)
+ <$> (R.option "" (R.try (
+ R.char ':'
+ *> R.many (R.satisfy Char.isLetter <|> R.char '_')
+ <* (R.option () $ void $ R.many (void $ R.char ' '))
+ )))
+ <*> R.many (R.try (
+ (<|>)
+ (R.try R.newline <* R.lookAhead (R.char ' ' <|> R.char '\t'))
+ (R.satisfy is_horizontal)
+ ))
+ where
+ is_horizontal c = case c of {'\n' -> False; '\r' -> False; _ -> True}
+
+parse_commands
+ :: R.Stream s m Char
+ => R.ParsecT s () m [(String, String)]
+parse_commands =
+ R.many $ do
+ _ <- R.many $ do
+ _ <- R.many (R.satisfy is_horizontal_space)
+ R.newline
+ (c, s) <- parse_command
+ _ <- R.many1 $ do
+ _ <- R.try (R.many (R.satisfy is_horizontal_space))
+ R.newline
+ return (c,s)
+ where
+ is_horizontal_space c = case c of {' ' -> True; '\t' -> True; _ -> False}
+
--- /dev/null
+:load lib/Bool.cloe
+:load lib/Either.cloe
+:load lib/Eq.cloe
+:load lib/Function.cloe
+:load lib/Functor.cloe
+:load lib/IO.cloe
+:load lib/List.cloe
+:load lib/Maybe.cloe
+:load lib/Monad.cloe
+:load lib/Monoid.cloe
+:load lib/Nat.cloe
+:load lib/Ord.cloe
+:load lib/Pair.cloe
--- /dev/null
+Bool_Polytype : *p = (Data:*) -> Data -> Data -> Data
+Bool : *m = Monotype Bool_Polytype
+True : Bool = monotype Bool_Polytype (λ(Data:*) (True:Data) (False:Data) -> True)
+False : Bool = monotype Bool_Polytype (λ(Data:*) (True:Data) (False:Data) -> False)
+
+and (x:Bool) (y:Bool) : Bool
+ = monotype Bool_Polytype
+ (λ(Data:*) (True:Data) (False:Data) ->
+ polytype Bool_Polytype x Data
+ (polytype Bool_Polytype y Data True False)
+ (polytype Bool_Polytype y Data False False)
+ )
+or (x:Bool) (y:Bool) : Bool
+ = monotype Bool_Polytype
+ (λ(Data:*) (True:Data) (False:Data) ->
+ polytype Bool_Polytype x Data
+ (polytype Bool_Polytype y Data True True)
+ (polytype Bool_Polytype y Data True False)
+ )
+xor (x:Bool) (y:Bool) : Bool
+ = monotype Bool_Polytype
+ (λ(Data:*) (True:Data) (False:Data) ->
+ polytype Bool_Polytype x Data
+ (polytype Bool_Polytype y Data False True)
+ (polytype Bool_Polytype y Data True False)
+ )
+not (x:Bool) : Bool
+ = monotype Bool_Polytype
+ (λ(Data:*) (True:Data) (False:Data) ->
+ polytype Bool_Polytype x Data False True)
--- /dev/null
+Either_Polytype (L:*) (R:*) : *p
+ = (Data:*) -> (L -> Data) -> (R -> Data) -> Data
+Either (L:*) (R:*) : *m
+ = Monotype (Either_Polytype L R)
+Left (L:*) (R:*) (l:L) : Either L R
+ = monotype (Either_Polytype L R)
+ (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Left l)
+Right (L:*) (R:*) (r:R) : Either L R
+ = monotype (Either_Polytype L R)
+ (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Right r)
+
+left (L:*) (R:*) (l:L)
+ : Either L R
+ = monotype (Either_Polytype L R)
+ (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Left l)
+right (L:*) (R:*) (r:R)
+ : Either L R
+ = monotype (Either_Polytype L R)
+ (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Right r)
+either
+ (L:*) (R:*) (Data:*)
+ (l:L -> Data)
+ (r:R -> Data)
+ (e:Either L R)
+ : Data
+ = polytype (Either_Polytype L R) e Data l r
+
+:load Monad.cloe
+Monad_return_Either (L:*) (X:*)
+ : Monad_Return (Either L) X
+ = Right L X
+Monad_bind_Either (L:*) (X:*) (Y:*)
+ : Monad_Bind (Either L) X Y
+ = λ(mx:Either L X) (my:X -> Either L Y) ->
+ either L X (Either L Y) (Left L Y) my mx
+Monad_Either (L:*)
+ : Monad (Either L)
+ = monad (Either L)
+ (Monad_return_Either L)
+ (Monad_bind_Either L)
--- /dev/null
+:load Bool.cloe
+
+Eq_Equal
+ (X:*)
+ = X -> X -> Bool
+
+Eq_Class
+ (X:*) (Data:*)
+ = (equal:Eq_Equal X)
+ -> Data
+Eq_Polytype
+ (X:*) : *p
+ = (Data:*) -> Eq_Class X Data -> Data
+Eq
+ (X:*) : *m
+ = Monotype (Eq_Polytype X)
+
+eq
+ (X:*)
+ (equal:Eq_Equal X)
+ : Eq X
+ = monotype (Eq_Polytype X)
+ (λ(Data:*) (eq_class:Eq_Class X Data) -> eq_class equal)
+unEq
+ (X:*) (Data:*)
+ (eq_class:Eq_Class X Data)
+ (eq:Eq X)
+ : Data
+ = polytype (Eq_Polytype X) eq Data eq_class
+
+Eq_equal
+ (X:*) (eq:Eq X)
+ : Eq_Equal X
+ = unEq X (Eq_Equal X)
+ (λ(equal:Eq_Equal X) -> equal)
+ eq
--- /dev/null
+id (X:*) (x:X) : X = x
+
+const (X:*) (Y:*) (x:X) (y:Y) : X = x
+
+o
+ (X:*) (Y:*) (Z:*)
+ (f:Y -> Z)
+ (g:X -> Y)
+ : X -> Z
+ = λ(x:X) -> f (g x)
--- /dev/null
+Functor_Fmap
+ (F:* -> *) (X:*) (Y:*)
+ = (X -> Y) -> F X -> F Y
+
+Functor_Class
+ (F:* -> *) (Data:*)
+ = (fmap:∀(X:*) -> ∀(Y:*) -> Functor_Fmap F X Y)
+ -> Data
+Functor_Polytype
+ (F:* -> *) : *p
+ = (Data:*) -> Functor_Class F Data -> Data
+Functor
+ (F:* -> *) : *m
+ = Monotype (Functor_Polytype F)
+
+functor
+ (F:* -> *)
+ (fmap:∀(X:*) -> ∀(Y:*) -> Functor_Fmap F X Y)
+ : Functor F
+ = monotype (Functor_Polytype F)
+ (λ(Data:*) (functor_class:Functor_Class F Data) -> functor_class fmap)
+unFunctor
+ (F:* -> *) (Data:*)
+ (functor_class:Functor_Class F Data)
+ (functor:Functor F)
+ : Data
+ = polytype (Functor_Polytype F) functor Data functor_class
+
+Functor_fmap
+ (F:* -> *) (functor:Functor F) (X:*) (Y:*)
+ : Functor_Fmap F X Y
+ = unFunctor F (Functor_Fmap F X Y)
+ (λ(fmap:∀(X:*) -> ∀(Y:*) -> Functor_Fmap F X Y) -> fmap X Y)
+ functor
--- /dev/null
+:load Pair.cloe
+
+:assume World : *
+IO_Polytype (X:*) : *p
+ = (Data:*) -> (data:(p:World -> Pair World X) -> Data) -> Data
+IO (X:*) = Monotype (IO_Polytype X)
+
+:load Monad.cloe
+Monad_return_IO (X:*)
+ : Monad_Return IO X
+ = λ(x:X) ->
+ monotype (IO_Polytype X)
+ (λ(Data:*) (data:(World -> Pair World X) -> Data) ->
+ data (λ(w:World) -> pair World X w x))
+Monad_bind_IO (X:*) (Y:*)
+ : Monad_Bind IO X Y
+ = λ(mx:IO X) (my:X -> IO Y) ->
+ monotype (IO_Polytype Y)
+ (λ(Data:*) (oy:(World -> Pair World Y) -> Data) ->
+ polytype (IO_Polytype X) mx Data (λ(px:World -> Pair World X) ->
+ oy (λ(w:World) ->
+ uncurry World X (Pair World Y)
+ (λ(w:World) (x:X) ->
+ polytype (IO_Polytype Y) (my x) (Pair World Y) (λ(py:World -> Pair World Y) ->
+ py w
+ )
+ )
+ (px w)
+ )
+ )
+ )
+Monad_List
+ : Monad IO
+ = monad IO
+ Monad_return_IO
+ Monad_bind_IO
--- /dev/null
+List_Polytype (X:*) : *p
+ = (Data:*) -> (Cons:X -> Data -> Data) -> (Nil:Data) -> Data
+List (X:*) : *m
+ = Monotype (List_Polytype X)
+List_foldr (X:*) (L:List X) (Data:*)
+ = polytype (List_Polytype X) L Data
+List_Nil (X:*) : List X
+ = monotype (List_Polytype X)
+ (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) -> Nil)
+List_Cons_right (X:*) (x:X) (xs:List X)
+ : List X
+ = monotype (List_Polytype X) (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
+ polytype (List_Polytype X) xs Data Cons (Cons x Nil))
+List_Cons_left (X:*) (x:X) (xs:List X)
+ : List X
+ = monotype (List_Polytype X) (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
+ Cons x (polytype (List_Polytype X) xs Data Cons Nil))
+List_Cons
+ : (X:*m) -> (x:X) -> (xs:List X) -> List X
+ = List_Cons_left
+
+:load Functor.cloe
+Functor_fmap_List (X:*) (Y:*)
+ : Functor_Fmap List X Y
+ = λ(y:X -> Y) (xs:List X) ->
+ monotype (List_Polytype Y) (λ(Data:*) (Cons:Y -> Data -> Data) ->
+ polytype (List_Polytype X) xs Data
+ (λ(x:X) -> Cons (y x)))
+Functor_fmap_List_using_foldr (X:*) (Y:*)
+ : Functor_Fmap List X Y
+ = λ(y:X -> Y) (xs:List X) ->
+ List_foldr X xs (List Y) (λ(x:X) ->
+ List_Cons_left Y (y x)) (List_Nil Y)
+
+:load Monoid.cloe
+Monoid_mempty_List (X:*)
+ : Monoid_Mempty (List X)
+ = List_Nil X
+Monoid_mappend_List (X:*)
+ : Monoid_Mappend (List X)
+ = λ(xs:List X) (ys:List X) ->
+ monotype (List_Polytype X)
+ (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
+ polytype (List_Polytype X) xs Data
+ Cons
+ (polytype (List_Polytype X) ys Data Cons Nil))
+Monoid_mappend_List_using_foldr (X:*)
+ : Monoid_Mappend (List X)
+ = λ(xs:List X) (ys:List X) ->
+ List_foldr X xs (List X) (List_Cons X) ys
+
+:load Monad.cloe
+Monad_return_List (X:*)
+ : Monad_Return List X
+ = λ(x:X) -> List_Cons X x (List_Nil X)
+Monad_bind_List (X:*) (Y:*)
+ : Monad_Bind List X Y
+ = λ(xs:List X) (ys:X -> List Y) ->
+ List_foldr X xs (List Y)
+ (λ(x:X) -> Monoid_mappend_List Y (ys x))
+ (Monoid_mempty_List Y)
+Monad_join_List (X:*)
+ : Monad_Join List X
+ = λ(xss:List (List X)) ->
+ monotype (List_Polytype X)
+ (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
+ polytype (List_Polytype (List X)) xss Data
+ (λ(xs:List X) -> polytype (List_Polytype X) xs Data Cons)
+ Nil)
+Monad_List
+ : Monad List
+ = monad List
+ Monad_return_List
+ Monad_bind_List
--- /dev/null
+Maybe_Polytype (X:*) : *p
+ = (Data:*) -> Data -> (X -> Data) -> Data
+Maybe (X:*) : *m
+ = Monotype (Maybe_Polytype X)
+Nothing (X:*) : Maybe X
+ = monotype (Maybe_Polytype X)
+ (λ(Data:*) (Nothing:Data) (Just:X -> Data) -> Nothing)
+Just (X:*) (x:X) : Maybe X
+ = monotype (Maybe_Polytype X)
+ (λ(Data:*) (Nothing:Data) (Just:X -> Data) -> Just x)
+maybe (X:*) (Data:*) (nothing:Data) (just:X -> Data) (m:Maybe X) : Data
+ = polytype (Maybe_Polytype X) m Data nothing just
+
+:load Monad.cloe
+Monad_return_Maybe
+ (X:*)
+ : Monad_Return Maybe X
+ = Just X
+Monad_bind_Maybe
+ (X:*) (Y:*)
+ : Monad_Bind Maybe X Y
+ = λ(mx:Maybe X) (my:X -> Maybe Y) ->
+ maybe X (Maybe Y) (Nothing Y) my mx
+Monad_Maybe
+ : Monad Maybe
+ = monad Maybe
+ Monad_return_Maybe
+ Monad_bind_Maybe
--- /dev/null
+Monad_Return (M:* -> *) (X:*) = X -> M X
+Monad_Join (M:* -> *) (X:*) = M (M X) -> M X
+Monad_Bind (M:* -> *) (X:*) (Y:*) = M X -> (X -> M Y) -> M Y
+
+Monad_Class
+ (M:* -> *) (Data:*)
+ = (return:∀(X:*) -> Monad_Return M X)
+ -> (bind:∀(X:*) -> ∀(Y:*) -> Monad_Bind M X Y)
+ -> Data
+Monad_Polytype
+ (M:* -> *) : *p
+ = (Data:*) -> Monad_Class M Data -> Data
+Monad
+ (M:* -> *) : *m
+ = Monotype (Monad_Polytype M)
+
+monad
+ (M:* -> *)
+ (return:∀(X:*) -> Monad_Return M X)
+ (bind:∀(X:*) -> ∀(Y:*) -> Monad_Bind M X Y)
+ : Monad M
+ = monotype (Monad_Polytype M)
+ (λ(Data:*) (monad_class:Monad_Class M Data) ->
+ monad_class return bind)
+unMonad
+ (M:* -> *) (Data:*)
+ (monad_class:Monad_Class M Data)
+ (monad:Monad M)
+ : Data
+ = polytype (Monad_Polytype M) monad Data monad_class
+
+Monad_return
+ (M:* -> *) (monad:Monad M) (X:*)
+ : Monad_Return M X
+ = unMonad M (Monad_Return M X)
+ (λ(return:∀(X:*) -> Monad_Return M X)
+ (bind:∀(X:*) -> ∀(Y:*) -> Monad_Bind M X Y)
+ -> return X
+ ) monad
+Monad_bind
+ (M:* -> *) (monad:Monad M) (X:*) (Y:*)
+ : Monad_Bind M X Y
+ = unMonad M (Monad_Bind M X Y)
+ (λ(return:∀(X:*) -> Monad_Return M X)
+ (bind:∀(X:*) -> ∀(Y:*) -> Monad_Bind M X Y)
+ -> bind X Y
+ ) monad
+Monad_join
+ (M:* -> *) (monad:Monad M) (X:*)
+ : Monad_Join M X
+ = λ(m:M (M X)) ->
+ Monad_bind M monad (M X) X m (λ(x:M X) -> x)
--- /dev/null
+Monoid_Mempty (M:*) = M
+Monoid_Mappend (M:*) = M -> M -> M
+
+Monoid_Class
+ (M:*) (Data:*)
+ = (mempty:Monoid_Mempty M)
+ -> (mappend:Monoid_Mappend M)
+ -> Data
+Monoid_Polytype
+ (M:*) : *p
+ = (Data:*) -> Monoid_Class M Data -> Data
+Monoid
+ (M:*) : *m
+ = Monotype (Monoid_Polytype M)
+
+monoid
+ (M:*)
+ (mempty:Monoid_Mempty M)
+ (mappend:Monoid_Mappend M)
+ : Monoid M
+ = monotype (Monoid_Polytype M)
+ (λ(Data:*) (monoid_class:Monoid_Class M Data) ->
+ monoid_class mempty mappend)
+unMonoid
+ (M:*) (Data:*)
+ (monoid_class:Monoid_Class M Data)
+ (monoid:Monoid M)
+ : Data
+ = polytype (Monoid_Polytype M) monoid Data monoid_class
+
+Monoid_mempty
+ (M:*) (monoid:Monoid M)
+ : Monoid_Mempty M
+ = unMonoid M (Monoid_Mempty M)
+ (λ(mempty:Monoid_Mempty M) (mappend:Monoid_Mappend M) -> mempty)
+ monoid
+Monoid_mappend
+ (M:*) (monoid:Monoid M)
+ : Monoid_Mappend M
+ = unMonoid M (Monoid_Mappend M)
+ (λ(mempty:Monoid_Mempty M) (mappend:Monoid_Mappend M) -> mappend)
+ monoid
--- /dev/null
+Nat_Polytype : *p
+ = (Data:*) -> (Succ:Data -> Data) -> (Zero:Data) -> Data
+Nat : *m = Monotype Nat_Polytype
+zero : Nat = (monotype Nat_Polytype) (λ(Data:*) (Succ:Data -> Data) (Zero:Data) -> Zero)
+succ (n:Nat) : Nat
+ = monotype Nat_Polytype
+ (λ(Data:*) (Succ:Data -> Data) (Zero:Data) ->
+ Succ (polytype Nat_Polytype n Data Succ Zero))
+one : Nat = succ zero
+two : Nat = succ one
+three : Nat = succ two
+plus (n:Nat) (m:Nat) : Nat
+ = monotype Nat_Polytype
+ (λ(Data:*) (Succ:Data -> Data) (Zero:Data) ->
+ polytype Nat_Polytype n Data Succ (polytype Nat_Polytype m Data Succ Zero))
+mult (n:Nat) (m:Nat) : Nat
+ = monotype Nat_Polytype
+ (λ(Data:*) (Succ:Data -> Data) (Zero:Data) ->
+ polytype Nat_Polytype n Data (polytype Nat_Polytype m Data Succ) Zero)
--- /dev/null
+Ordering_Polytype : *p
+ = (Data:*) -> (Lt:Data) -> (Eq:Data) -> (Gt:Data) -> Data
+Ordering : *m = Monotype Ordering_Polytype
+
+Ord_Lt : Ordering = monotype Ordering_Polytype (λ(Data:*) (Lt:Data) (Eq:Data) (Gt:Data) -> Lt)
+Ord_Eq : Ordering = monotype Ordering_Polytype (λ(Data:*) (Lt:Data) (Eq:Data) (Gt:Data) -> Eq)
+Ord_Gt : Ordering = monotype Ordering_Polytype (λ(Data:*) (Lt:Data) (Eq:Data) (Gt:Data) -> Gt)
+
+:load Eq.cloe
+
+Ord_Compare (X:*) = X -> X -> Ordering
+
+Ord_Class
+ (X:*) (Data:*)
+ = (eq:Eq X)
+ -> (compare:Ord_Compare X)
+ -> Data
+Ord_Polytype
+ (X:*) : *p
+ = (Data:*) -> Ord_Class X Data -> Data
+Ord
+ (X:*) : *m
+ = Monotype (Ord_Polytype X)
+
+ord
+ (X:*)
+ (eq:Eq X)
+ (compare:Ord_Compare X)
+ : Ord X
+ = monotype (Ord_Polytype X)
+ (λ(Data:*) (ord_class:Ord_Class X Data) ->
+ ord_class eq compare)
+unOrd
+ (X:*) (Data:*)
+ (ord_class:Ord_Class X Data)
+ (ord:Ord X)
+ : Data
+ = polytype (Ord_Polytype X) ord Data ord_class
+
+Ord_eq
+ (X:*) (ord:Ord X)
+ : Eq X
+ = unOrd X (Eq X)
+ (λ(eq:Eq X) (compare:Ord_Compare X) -> eq)
+ ord
+Ord_compare
+ (X:*) (ord:Ord X)
+ : Ord_Compare X
+ = unOrd X (Ord_Compare X)
+ (λ(eq:Eq X) (compare:Ord_Compare X) -> compare)
+ ord
--- /dev/null
+Pair_Polytype (X:*) (Y:*) : *p = (Data:*) -> (X -> Y -> Data) -> Data
+Pair (X:*) (Y:*) : *m = Monotype (Pair_Polytype X Y)
+pair (X:*) (Y:*) (x:X) (y:Y) : Pair X Y
+ = monotype (Pair_Polytype X Y)
+ (λ(Data:*) (f:X -> Y -> Data) -> f x y)
+
+uncurry (X:*) (Y:*) (Data:*) (r:X -> Y -> Data) (p:Pair X Y) : Data
+ = polytype (Pair_Polytype X Y)
+ p Data r
+curry (X:*) (Y:*) (Data:*) (r:Pair X Y -> Data) (x:X) (y:Y)
+ = r (pair X Y x y)
+
+fst (X:*) (Y:*) (p:Pair X Y) : X
+ = uncurry X Y X (λ(x:X) (y:Y) -> x) p
+snd (X:*) (Y:*) (p:Pair X Y) : Y
+ = uncurry X Y Y (λ(x:X) (y:Y) -> y) p
+repair (X:*) (Y:*) (p:Pair X Y) : Pair X Y
+ = pair X Y (fst X Y p) (snd X Y p)
+
+first (X:*) (Y:*) (Z:*) (f:X -> Z) (p:Pair X Y) : Pair Z Y
+ = uncurry X Y (Pair Z Y) (λ(x:X) (y:Y) -> pair Z Y (f x) y) p
+second (X:*) (Y:*) (Z:*) (f:Y -> Z) (p:Pair X Y) : Pair X Z
+ = uncurry X Y (Pair X Z) (λ(x:X) (y:Y) -> pair X Z x (f y)) p
--- /dev/null
+module Calculus.Lambda.Omega.Implicit where
+
+
+
--- /dev/null
+haddock
+ html-location: http://hackage.haskell.org/packages/archive/$pkg/latest/doc/html
--- /dev/null
+author: Julien Moutinho <julm+hcompta@autogeree.net>
+bug-reports: http://doc.autogeree.net/hcompta/bugs
+build-type: Simple
+cabal-version: >= 1.8
+category: Finance
+-- data-dir: data
+-- data-files:
+description: Accounting calculus.
+extra-source-files: Test.hs
+extra-tmp-files:
+homepage: http://doc.autogeree.net/coop/hcompta
+license: GPL
+license-file: COPYING
+maintainer: Julien Moutinho <julm+hcompta@autogeree.net>
+name: hcompta-calculus
+stability: experimental
+synopsis: Accounting calculus based upon a typed lambda-calculus.
+tested-with: GHC==7.8.4
+version: 0.0.0
+
+source-repository head
+ location: git://git.autogeree.net/hcompta
+ type: git
+
+Flag dev
+ Default: False
+ Description: Turn on development settings.
+
+Flag dump
+ Default: False
+ Description: Dump some intermediate files.
+ Manual: True
+
+Flag exe
+ Description: Build only executable.
+ Default: False
+
+Flag lib
+ Description: Build only library.
+ Default: False
+
+Flag prof
+ Default: False
+ Description: Turn on profiling settings.
+
+Flag threaded
+ Default: True
+ Description: Enable threads.
+ Manual: True
+
+Library
+ extensions: NoImplicitPrelude
+ ghc-options: -Wall -fno-warn-tabs
+ if flag(dev)
+ cpp-options: -DDEVELOPMENT
+ ghc-options:
+ -- -ddump-splices
+ -- -fno-warn-unused-do-bind -fno-warn-name-shadowing -fno-warn-missing-signatures
+ -- -fno-warn-type-defaults -fno-warn-orphans
+ else
+ ghc-options: -O2
+ if flag(dump)
+ ghc-options: -ddump-simpl -ddump-stg -ddump-to-file
+ if flag(exe)
+ Buildable: False
+ if flag(prof)
+ cpp-options: -DPROFILING
+ ghc-options: -O2 -fprof-auto
+ -- default-language: Haskell2010
+ exposed-modules:
+ Calculus.Abstraction.DeBruijn.Generalized
+ Calculus.Lambda.Omega.Explicit
+ Calculus.Lambda.Omega.Explicit.Read
+ Calculus.Lambda.Omega.Implicit
+ build-depends:
+ base >= 4.6 && < 5
+ , array
+ , containers >= 0.5 && < 0.6
+ , deepseq >= 1.4 && < 1.5
+ , directory
+ , filepath
+ , parsec >= 3.1.2 && < 4
+ , semigroups
+ , strict
+ , test-framework
+ , test-framework-hunit
+ , text
+ , text-format
+ , time
+ , transformers >= 0.4 && < 0.5
+
+Executable hcompta-calculus-explicit
+ extensions: NoImplicitPrelude
+ ghc-options: -Wall -fno-warn-tabs
+ -main-is Calculus.Lambda.Omega.Explicit.REPL
+ if flag(threaded)
+ ghc-options: -threaded -rtsopts -with-rtsopts=-N
+ if flag(dev)
+ cpp-options: -DDEVELOPMENT
+ ghc-options:
+ else
+ ghc-options: -O2
+ if flag(prof)
+ cpp-options: -DPROFILING
+ ghc-options: -fprof-auto
+ if flag(lib)
+ Buildable: False
+ exposed-modules:
+ main-is: Calculus/Lambda/Omega/Explicit/REPL.hs
+ hs-source-dirs: .
+ build-depends:
+ base >= 4.6 && < 5
+ , ansi-terminal >= 0.4 && < 0.7
+ , bytestring
+ , containers >= 0.5 && < 0.6
+ , Decimal
+ , deepseq
+ , directory
+ , filepath
+ , haskeline >= 0.7 && < 0.8
+ , hcompta-calculus
+ , mtl >= 2.0
+ , parsec
+ , semigroups
+ , strict
+ , text
+ , text-format
+ , time
+ , transformers >= 0.4 && < 0.5
sourcephile / git / comptalang.git / commitdiff