packages feed

lol-calculus (empty) → 1.20160822

raw patch · 26 files changed

+4509/−0 lines, 26 filesdep +basedep +containersdep +directorysetup-changed

Dependencies added: base, containers, directory, filepath, haskeline, lol-calculus, mtl, parsec, text, text-format, transformers

Files

+ COPYING view
@@ -0,0 +1,674 @@+                    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>.
+ Language/LOL/Calculus.hs view
@@ -0,0 +1,14 @@+-- | All submodules, in a topological order.+module Language.LOL.Calculus+ ( module Language.LOL.Calculus.Abstraction+ , module Language.LOL.Calculus.Term+ , module Language.LOL.Calculus.Type+ , module Language.LOL.Calculus.Form+ , module Language.LOL.Calculus.Axiom+ ) where++import Language.LOL.Calculus.Abstraction+import Language.LOL.Calculus.Term+import Language.LOL.Calculus.Type+import Language.LOL.Calculus.Form+import Language.LOL.Calculus.Axiom
+ Language/LOL/Calculus/Abstraction.hs view
@@ -0,0 +1,300 @@+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+-- | Generalized DeBruijn abstraction+module Language.LOL.Calculus.Abstraction 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 (($), (.), on)+import Data.Maybe (Maybe(..))+import Data.Ord (Ord(..), Ordering(..))+import Data.String (IsString(..), String)+import Data.Text (Text)+import Data.Text.Buildable (Buildable(..))+import Data.Traversable (Traversable(..))+import Prelude (Int)+import Text.Show (Show(..), ShowS, showChar, 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) =+		showsUnaryWith "Abstraction" d $+			(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)++-- | Aka. /instantiating/.+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'+-- | Lift the 'Eq' class to unary type constructors,+-- 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+-- * /base/ 'Data.Functor.Classes', Ross Paterson, 2013,+--   https://hackage.haskell.org/package/base/docs/Data-Functor-Classes.html+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'+-- | Lift the 'Show' class to unary type constructors,+-- to avoid the @UndecidableInstances@ language extension.+class Show1 f where+	showsPrec1 :: Show a => Int -> f a -> ShowS++showsUnaryWith :: (Show1 f, Show a) => String -> Int -> f a -> ShowS+showsUnaryWith name d x =+	showParen (d > 10) $+	showString name . showChar ' ' . showsPrec1 11 x++-- ** Type 'Lift1'+-- | Lift the 'Lift' class to unary type constructors,+-- 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
+ Language/LOL/Calculus/Axiom.hs view
@@ -0,0 +1,819 @@+{-# LANGUAGE DataKinds #-}+{-# 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 #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Language.LOL.Calculus.Axiom where++import Data.Bool+import qualified Data.Char as Char+import Data.Either (Either(..))+import Data.Eq (Eq(..))+import Data.Function (($), (.), const)+import Data.Functor ((<$>))+import Data.List ((++))+import qualified Data.Map.Strict as Map+import Data.Maybe (Maybe(..), maybe)+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.Typeable as Typeable+import Prelude (Int, Integer, Num(..), error)+import System.IO (IO)+import Text.Show (Show(..), showParen, showString)++import Language.LOL.Calculus.Abstraction+import Language.LOL.Calculus.Term+import Language.LOL.Calculus.Type+import Language.LOL.Calculus.Form+++-- * 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 '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
+ Language/LOL/Calculus/Form.hs view
@@ -0,0 +1,306 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Calculus.Form where++import Control.Arrow+import Control.Monad+import Data.Bool+import Data.Either (Either(..))+import Data.Eq (Eq(..))+import Data.Foldable (Foldable(..))+import Data.Function (($), (.), id, const, flip, on)+import Data.Functor ((<$>))+import Data.List ((++))+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Data.Maybe (Maybe(..), fromMaybe)+import Data.Monoid ()+import Data.Ord (Ord(..))+import Data.Text.Buildable (Buildable(..))+import Data.Traversable (Traversable(..))+import Data.Typeable as Typeable+import Prelude (error)+import Text.Show (Show(..))++import Language.LOL.Calculus.Abstraction+import Language.LOL.Calculus.Term++-- * Type 'Form'++-- | 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++-- * Type 'Context'++context :: Context Var_Name+context = Context [] (const Nothing) id id++context_apply :: Context var -> Term var -> Term var+context_apply ctx te =+	te >>= \var ->+		fromMaybe (TeTy_Var var) $ 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
+ Language/LOL/Calculus/REPL.hs view
@@ -0,0 +1,633 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE ViewPatterns #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Calculus.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 qualified Data.List as List+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Data.Maybe (Maybe(..))+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 Language.LOL.Calculus+import Language.LOL.Calculus.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 `List.isPrefixOf` "quit") ->+			dispatch cmd input+		 _ -> return ()+		main_loop++slice :: String -> (String, String)+slice (':':str) = List.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@(_:_) | List.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@(_:_) | List.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 List.find (\p -> cmd `List.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) =+	command cmd $+		Command_Input (strip_spaces i) st+	where+	strip_spaces =+		List.reverse . List.dropWhile Char.isSpace .+		List.reverse . List.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 ->+					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) ->+		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})+					 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 $ List.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"+	   ]+	 ]
+ Language/LOL/Calculus/Read.hs view
@@ -0,0 +1,391 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE TupleSections #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Calculus.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(..), 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 Language.LOL.Calculus++-- * 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}+
+ Language/LOL/Calculus/Term.hs view
@@ -0,0 +1,326 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# 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 #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Calculus.Term where++import Control.Applicative (Applicative(..), (<$>))+import Control.Monad+import Data.Bool+import Data.Eq (Eq(..))+import Data.Foldable (Foldable(..))+import Data.Function (($), (.))+import Data.Maybe (Maybe(..), maybe, catMaybes, fromJust)+import Data.Monoid (Monoid(..), (<>))+import Data.Ord (Ord(..))+import Data.Text.Buildable (Buildable(..))+import qualified Data.Text.Lazy.Builder as Builder+import Data.Traversable (Traversable(..))+import Data.Typeable as Typeable+import Text.Show (Show(..), showParen, showString)++-- import Debug.Trace++import Language.LOL.Calculus.Abstraction++-- * 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 program+-- 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)++-- * Type 'Type'++-- | 'Type' and 'Term' share the same data-type.+type Type = Term++-- | '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++-- *** 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 -> "□"++-- | @*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_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"++-- * Type 'Axiom'++data family Axiom r++-- ** Class 'Axiomable'++-- | 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 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)++-- * 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)++-- * 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
+ Language/LOL/Calculus/Type.hs view
@@ -0,0 +1,381 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Calculus.Type where++import Control.Arrow+import Control.Monad+import Data.Either (Either(..))+import Data.Eq (Eq(..))+import Data.Foldable (Foldable(..))+import Data.Function (($), (.), const)+import Data.Functor ((<$>))+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Data.Maybe (Maybe(..))+import Data.Monoid (Monoid(..), (<>))+import Data.Ord (Ord(..))+import Data.Text.Buildable (Buildable(..))+import Data.Traversable (Traversable(..))+import Data.Typeable as Typeable+import Text.Show (Show(..))++import Language.LOL.Calculus.Abstraction+import Language.LOL.Calculus.Term+import Language.LOL.Calculus.Form++-- * Type 'Type'++-- | 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+		if equiv ctx x_ty f_in+			then return $ const x `unabstract` f_out+			else 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 (`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 'Sort'++-- *** Type 'Type_Level'++-- | /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+
+ Language/LOL/Calculus/lib.lol view
@@ -0,0 +1,13 @@+:load lib/Bool.lol+:load lib/Either.lol+:load lib/Eq.lol+:load lib/Function.lol+:load lib/Functor.lol+:load lib/IO.lol+:load lib/List.lol+:load lib/Maybe.lol+:load lib/Monad.lol+:load lib/Monoid.lol+:load lib/Nat.lol+:load lib/Ord.lol+:load lib/Pair.lol
+ Language/LOL/Calculus/lib/Bool.lol view
@@ -0,0 +1,30 @@+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)
+ Language/LOL/Calculus/lib/Either.lol view
@@ -0,0 +1,40 @@+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.lol+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)
+ Language/LOL/Calculus/lib/Eq.lol view
@@ -0,0 +1,36 @@+:load Bool.lol++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
+ Language/LOL/Calculus/lib/Function.lol view
@@ -0,0 +1,10 @@+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)
+ Language/LOL/Calculus/lib/Functor.lol view
@@ -0,0 +1,34 @@+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
+ Language/LOL/Calculus/lib/IO.lol view
@@ -0,0 +1,36 @@+:load Pair.lol++:assume World : *+IO_Polytype (X:*) : *p+ = (Data:*) -> (data:(p:World -> Pair World X) -> Data) -> Data+IO (X:*) = Monotype (IO_Polytype X)++:load Monad.lol+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_IO+ : Monad IO+ = monad IO+ Monad_return_IO+ Monad_bind_IO
+ Language/LOL/Calculus/lib/List.lol view
@@ -0,0 +1,74 @@+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.lol+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.lol+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.lol+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
+ Language/LOL/Calculus/lib/Maybe.lol view
@@ -0,0 +1,28 @@+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.lol+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
+ Language/LOL/Calculus/lib/Monad.lol view
@@ -0,0 +1,52 @@+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)
+ Language/LOL/Calculus/lib/Monoid.lol view
@@ -0,0 +1,42 @@+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
+ Language/LOL/Calculus/lib/Nat.lol view
@@ -0,0 +1,19 @@+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)
+ Language/LOL/Calculus/lib/Ord.lol view
@@ -0,0 +1,51 @@+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.lol++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
+ Language/LOL/Calculus/lib/Pair.lol view
@@ -0,0 +1,23 @@+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
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ lol-calculus.cabal view
@@ -0,0 +1,169 @@+author: Julien Moutinho <julm+lol@autogeree.net>+-- bug-reports: http://bug.autogeree.net/lol+build-type: Simple+cabal-version: >= 1.8+category: Language+-- data-dir: .+-- data-files:+description:+ WARNING: this is a research program+ written as I learn and explore /lambda calculii/:+ please understand well by yourself whatever you may take from it;+ any question or contribution being welcome :-)+ .+ This package implements an /explicitely typed/+ (aka. /à la Church/) /lambda calculus/+ with: /simples types/, /parametric polymorphism/,+ /higher-rank polymorphism/ and /constructors of types/+ (I have no need for /dependent types/ so far,+ but it should be straightforward to add them+ to allow the full /Calculus of constructions/ (CoC)).+ .+ This is mainly done by means of:+ a common /Algebraic Data Type/ (ADT) for terms and types+ to build a /Pure Type System/ (PTS),+ <https://www.schoolofhaskell.com/user/edwardk/bound generalized DeBruijn indices>+ to implement /capture-avoiding substitution/ of variables,+ and 'Typeable' axioms to embed Haskell types and terms+ (the most experimental and tricky part).+ .+ The inspiring programs I studied+ which explore similar problems:+ Simon Peyton Jones and Erik Meijer's+ <https://research.microsoft.com/en-us/um/people/simonpj/papers/henk.ps.gz Henk>,+ Dan Doel's <http://hub.darcs.net/dolio/pts pts>,+ Gabriel Gonzalez's <https://hackage.haskell.org/package/morte morte>,+ Richard Eisenberg's <https://hackage.haskell.org/package/glambda glambda>,+ Edward Kmett's <https://hackage.haskell.org/package/bound bound>.++ .+ See also: the <https://hackage.haskell.org/package/lol-typing lol-typing> package+ studying the /type inferencing/.+ .+ NOTE: if you are just interested in building+ an /Embedded Domain Specific Language/ (EDSL)+ you may as well study Oleg Kiselyov, Jacques Carette and Chung-chieh Shan's+ <http://okmij.org/ftp/tagless-final Typed Tagless Final Interpreters>,+ which you may find being a much more simple, efficient and robust approach.+extra-source-files:+  stack.yaml+  Language/LOL/Calculus/lib.lol+  Language/LOL/Calculus/lib/Bool.lol+  Language/LOL/Calculus/lib/Either.lol+  Language/LOL/Calculus/lib/Eq.lol+  Language/LOL/Calculus/lib/Function.lol+  Language/LOL/Calculus/lib/Functor.lol+  Language/LOL/Calculus/lib/IO.lol+  Language/LOL/Calculus/lib/List.lol+  Language/LOL/Calculus/lib/Maybe.lol+  Language/LOL/Calculus/lib/Monad.lol+  Language/LOL/Calculus/lib/Monoid.lol+  Language/LOL/Calculus/lib/Nat.lol+  Language/LOL/Calculus/lib/Ord.lol+  Language/LOL/Calculus/lib/Pair.lol+extra-tmp-files:+-- homepage: http://pad.autogeree.net/informatique/lol/+license: GPL-3+license-file: COPYING+maintainer: Julien Moutinho <julm+lol@autogeree.net>+name: lol-calculus+stability: experimental+synopsis: Calculus for LOL (λω language).+tested-with: GHC==7.10.3+version: 1.20160822++source-repository head+  location: git://git.autogeree.net/lol+  type:     git++Flag dev+  Default:     False+  Description: Turn on development settings.+  Manual:      True++Flag dump+  Default:     False+  Description: Dump some intermediate files.+  Manual:      True++Flag exe+  Description: Build executable.+  Default:     True++Flag lib+  Description: Build library.+  Default:     True++Flag prof+  Default:     False+  Description: Turn on profiling settings.+  Manual:      True++Flag threaded+  Default:     False+  Description: Enable threads.+  Manual:      True++Library+  extensions: NoImplicitPrelude+  ghc-options: -Wall -fno-warn-tabs+  if flag(dev)+    cpp-options: -DDEVELOPMENT+    ghc-options:+  if flag(dump)+    ghc-options: -ddump-simpl -ddump-stg -ddump-to-file+  if flag(exe)+    Buildable: True+  else+    Buildable: False+  if flag(prof)+    cpp-options: -DPROFILING+    ghc-options: -fprof-auto+  -- default-language: Haskell2010+  exposed-modules:+    Language.LOL.Calculus+    Language.LOL.Calculus.Abstraction+    Language.LOL.Calculus.Axiom+    Language.LOL.Calculus.Form+    Language.LOL.Calculus.Read+    Language.LOL.Calculus.Term+    Language.LOL.Calculus.Type+  build-depends:+    base >= 4.6 && < 5+    , containers >= 0.5 && < 0.6+    , parsec >= 3.1.2 && < 4+    , text+    , text-format+    , transformers >= 0.4 && < 0.5++Executable lol-calculus+  extensions: NoImplicitPrelude+  ghc-options: -Wall -fno-warn-tabs+               -main-is Language.LOL.Calculus.REPL+  if flag(threaded)+    ghc-options: -threaded -rtsopts -with-rtsopts=-N+  if flag(dev)+    cpp-options: -DDEVELOPMENT+    ghc-options:+  if flag(prof)+    cpp-options: -DPROFILING+    ghc-options: -fprof-auto+  if flag(lib)+    Buildable: True+  else+    Buildable: False+  hs-source-dirs: Language/LOL/Calculus+  main-is: REPL.hs+  other-modules:+  build-depends:+    base >= 4.6 && < 5+    , containers >= 0.5 && < 0.6+    , directory+    , filepath+    , haskeline >= 0.7 && < 0.8+    , lol-calculus+    , mtl >= 2.0+    , parsec+    , text+    , text-format+    , transformers >= 0.4 && < 0.5
+ stack.yaml view
@@ -0,0 +1,6 @@+resolver: lts-6.12+flags: {}+packages:+- '.'+extra-deps:+extra-package-dbs: []