packages feed

symantic (empty) → 6.0.0.20170623

raw patch · 27 files changed

+4675/−0 lines, 27 filesdep +basedep +containersdep +ghc-prim

Dependencies added: base, containers, ghc-prim, mono-traversable, symantic-document, symantic-grammar, text, 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/Symantic.hs view
@@ -0,0 +1,17 @@+module Language.Symantic+ ( module Language.Symantic.Typing+ , module Language.Symantic.Compiling+ , module Language.Symantic.Interpreting+ , module Language.Symantic.Transforming+ -- * Re-exports for convenience.+ , module Language.Symantic.Grammar.Fixity+ , module Language.Symantic.Grammar.Meta+ ) where++import Language.Symantic.Typing+import Language.Symantic.Compiling+import Language.Symantic.Interpreting+import Language.Symantic.Transforming++import Language.Symantic.Grammar.Fixity+import Language.Symantic.Grammar.Meta
+ Language/Symantic/Compiling.hs view
@@ -0,0 +1,14 @@+-- | Compiling terms.+module Language.Symantic.Compiling+ ( module Language.Symantic.Compiling.Term+ , module Language.Symantic.Compiling.Module+ , module Language.Symantic.Compiling.Grammar+ , module Language.Symantic.Compiling.Beta+ , module Language.Symantic.Compiling.Read+ ) where++import Language.Symantic.Compiling.Term+import Language.Symantic.Compiling.Module+import Language.Symantic.Compiling.Grammar+import Language.Symantic.Compiling.Beta+import Language.Symantic.Compiling.Read
+ Language/Symantic/Compiling/Beta.hs view
@@ -0,0 +1,80 @@+-- | Beta-reduction of 'Term's.+module Language.Symantic.Compiling.Beta where++import Control.Arrow (left)+import qualified Data.Kind as K++import Language.Symantic.Grammar+import Language.Symantic.Typing+import Language.Symantic.Compiling.Term++-- | Term application: apply second given 'TermT' to the first,+-- applying embedded 'TeSym's, or return an error.+betaTerm ::+ forall src ss es vs fun arg.+ Inj_Source (TypeVT src) src =>+ Constable (->) =>+ Term src ss es vs (fun::K.Type) ->+ Term src ss es vs (arg::K.Type) ->+ Either (Error_Beta src) (TermT src ss es vs)+betaTerm (Term qf tf (TeSym te_fun)) (Term qa ta (TeSym te_arg)) =+	case tf of+	 TyApp _ (TyApp _ a2b a2b_a) a2b_b+	  | Just HRefl <- proj_ConstKiTy @(K (->)) @(->) a2b ->+		case a2b_a `eqType` ta of+		 Nothing -> Left $ Error_Beta_Type_mismatch (TypeVT a2b_a) (TypeVT ta)+		 Just Refl ->+			Right $+			case (proveConstraint qf, proveConstraint qa) of+			 -- NOTE: remove provable Constraints to keep those smaller.+			 (Just Dict, Just Dict) -> TermT $ Term (noConstraintLen (lenVars a2b_b)) a2b_b $+				TeSym $ \c -> te_fun c `app` te_arg c+			 (Just Dict, Nothing) -> TermT $ Term qa a2b_b $+				TeSym $ \c -> te_fun c `app` te_arg c+			 (Nothing, Just Dict) -> TermT $ Term qf a2b_b $+				TeSym $ \c -> te_fun c `app` te_arg c+			 (Nothing, Nothing) -> TermT $ Term (qf # qa) a2b_b $+				TeSym $ \c -> te_fun c `app` te_arg c+	 _ -> Left $ Error_Beta_Term_not_a_function $ TypeVT (qf #> tf)++-- | Collapse given 'BinTree' of 'TermVT's to compute a resulting 'TermVT', if possible.+betaTerms ::+ Inj_Source (TypeVT src) src =>+ Constable (->) =>+ BinTree (TermVT src ss es) ->+ Either (Error_Beta src) (TermVT src ss es)+betaTerms t =+	collapseBT (\acc ele -> do+		TermVT (Term qf tf te_fun) <- acc+		TermVT (Term qa ta te_arg) <- ele+		let (tf', ta') = appendVars tf ta+		let (qf', qa') = appendVars qf qa+		case unTyFun tf' of+		 Nothing -> Left $ Error_Beta_Term_not_a_function $ TypeVT tf'+		 Just (af, _rf) -> do+			mgu <-+				(Error_Beta_Unify `left`) $+				case (unQualsTy af, unQualsTy ta') of+				 (TypeK af', TypeK ta'') -> unifyType mempty af' ta''+			let qf'' = subst mgu qf'+			let qa'' = subst mgu qa'+			let tf'' = subst mgu tf'+			let ta'' = subst mgu ta'+			TermT (Term qr tr te_res) <- betaTerm (Term qf'' tf'' te_fun) (Term qa'' ta'' te_arg)+			normalizeVarsTy (qr #> tr) $ \(TyApp _ (TyApp _ _c qr') tr') ->+				Right $ TermVT $ Term qr' tr' te_res+	 ) (Right <$> t)++-- * Type 'Error_Beta'+data Error_Beta src+ =   Error_Beta_Term_not_a_function (TypeVT src)+ |   Error_Beta_Type_mismatch (TypeVT src) (TypeVT src)+ |   Error_Beta_Unify (Error_Unify src)+     -- ^ Cannot unify the expected 'Type' of the argument of the function,+     -- with the 'Type' of the argument.+ deriving (Eq, Show)++instance Inj_Error (Error_Beta src) (Error_Beta src) where+	inj_Error = id+instance Inj_Error (Error_Unify src) (Error_Beta src) where+	inj_Error = Error_Beta_Unify
+ Language/Symantic/Compiling/Grammar.hs view
@@ -0,0 +1,370 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}+module Language.Symantic.Compiling.Grammar where++import Control.Arrow (left)+import Control.Monad (void)+import Data.Proxy (Proxy(..))+import Data.Semigroup (Semigroup(..))+import Prelude hiding (mod, not, any)+import qualified Data.Char as Char+import qualified Data.Function as Fun+import qualified Data.Map.Strict as Map+import qualified Data.Text as Text++import Language.Symantic.Grammar+import Language.Symantic.Typing+import Language.Symantic.Compiling.Module++-- * Class 'Gram_Name'+class+ ( Gram_Terminal g+ , Gram_Rule g+ , Gram_Alt g+ , Gram_Try g+ , Gram_App g+ , Gram_AltApp g+ , Gram_RegL g+ , Gram_CF g+ , Gram_Comment g+ , Gram_Op g+ ) => Gram_Name g where+	g_mod_path :: CF g PathMod+	g_mod_path = rule "mod_path" $+		infixrG+		 (pure <$> g_mod_name)+		 (op <$ char '.')+		where op = (<>)+	g_mod_name :: CF g NameMod+	g_mod_name = rule "mod_name" $+		(NameMod . Text.pack <$>) $+		(identG `minus`) $+		Fun.const+		 <$> g_term_keywords+		 <*. (any `but` g_term_idname_tail)+		where+		identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail)+		headG  = unicat $ Unicat Char.UppercaseLetter+	+	g_term_mod_name :: CF g (Mod NameTe)+	g_term_mod_name = rule "term_mod_name" $+		lexeme $+			g_term_mod_idname <+>+			parens g_term_mod_opname+	g_term_name :: CF g NameTe+	g_term_name = rule "term_name" $+		lexeme $+			g_term_idname <+>+			parens g_term_opname+	+	g_term_mod_idname :: CF g (Mod NameTe)+	g_term_mod_idname = rule "term_mod_idname" $+		Mod+		 <$> option [] (try $ g_mod_path <* char '.')+		 <*> g_term_idname+	g_term_idname :: CF g NameTe+	g_term_idname = rule "term_idname" $+		(NameTe . Text.pack <$>) $+		(identG `minus`) $+		Fun.const+		 <$> g_term_keywords+		 <*. (any `but` g_term_idname_tail)+		where+		identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail)+		headG  = unicat $ Unicat_Letter+	g_term_idname_tail :: Terminal g Char+	g_term_idname_tail = rule "term_idname_tail" $+		unicat Unicat_Letter <+>+		unicat Unicat_Number+	g_term_keywords :: Reg rl g String+	g_term_keywords = rule "term_keywords" $+		choice $ string <$> ["in", "let"]+	+	g_term_mod_opname :: CF g (Mod NameTe)+	g_term_mod_opname = rule "term_mod_opname" $+		Mod+		 <$> option [] (try $ g_mod_path <* char '.')+		 <*> g_term_opname+	g_term_opname :: CF g NameTe+	g_term_opname = rule "term_opname" $+		(NameTe . Text.pack <$>) $+		(symG `minus`) $+		Fun.const+		 <$> g_term_keysyms+		 <*. (any `but` g_term_opname_ok)+		where+		symG = some $ cf_of_Terminal g_term_opname_ok+	g_term_opname_ok :: Terminal g Char+	g_term_opname_ok = rule "term_opname_ok" $+		choice (unicat <$>+		 [ Unicat_Symbol+		 , Unicat_Punctuation+		 , Unicat_Mark+		 ]) `but` koG+		where+		koG = choice (char <$> ['(', ')', '`', '\'', ',', '[', ']'])+	g_term_keysyms :: Reg rl g String+	g_term_keysyms = rule "term_keysyms" $+		choice $ string <$> ["\\", "->", "=", "@"]++deriving instance Gram_Name g => Gram_Name (CF g)+instance Gram_Name EBNF+instance Gram_Name RuleEBNF++-- * Class 'Gram_Term_Type'+class+ ( Gram_Terminal g+ , Gram_Rule g+ , Gram_Alt g+ , Gram_AltApp g+ , Gram_App g+ , Gram_CF g+ , Gram_Comment g+ , Gram_Name g+ , Gram_Type src g+ ) => Gram_Term_Type src g where+	g_term_abst_decl :: CF g (NameTe, AST_Type src)+	g_term_abst_decl = rule "term_abst_decl" $+		parens $ (,)+		 <$> g_term_name+		 <*  (symbol "::" <+> symbol ":")+		 -- NOTE: "::" is Haskell compatibility and ":" is another common notation.+		 <*> g_type++deriving instance Gram_Term_Type src g => Gram_Term_Type src (CF g)+instance Gram_Source src EBNF => Gram_Term_Type src EBNF+instance Gram_Source src RuleEBNF => Gram_Term_Type src RuleEBNF++-- ** Type 'Error_Term_Gram'+data Error_Term_Gram+ =   Error_Term_Gram_Fixity Error_Fixity+ |   Error_Term_Gram_Term_incomplete+ |   Error_Term_Gram_Type_applied_to_nothing+ |   Error_Term_Gram_not_applicable+ |   Error_Term_Gram_application+ |   Error_Term_Gram_application_mismatch+ |   Error_Term_Gram_Module Error_Module+ deriving (Eq, Show)++-- * Class 'Gram_Term'+class+ ( Gram_Source src g+ , Gram_Error Error_Term_Gram g+ , Gram_Terminal g+ , Gram_Rule g+ , Gram_Alt g+ , Gram_App g+ , Gram_AltApp g+ , Gram_CF g+ , Gram_Comment g+ , Gram_Type src g+ , Gram_Name g+ , Gram_Term_Type src g+ , Gram_Term_Atoms src ss g+ , Gram_State (Imports, Modules src ss) g+ ) => Gram_Term src ss g where+	g_term :: CF g (AST_Term src ss)+	g_term = rule "term" $+		choice+		 [ try g_term_abst+		 , g_term_operators+		 , g_term_let+		 ]+	g_term_operators :: CF g  (AST_Term src ss)+	g_term_operators = rule "term_operators" $+		g_catch $+		left Error_Term_Gram_Fixity <$>+		g_ops+		where+		g_ops :: CF g (Either Error_Fixity  (AST_Term src ss))+		g_ops = operators g_term_atom g_prefix g_infix g_postfix+		g_prefix  :: CF g (Unifix, AST_Term src ss -> AST_Term src ss)+		g_infix   :: CF g (Infix,  AST_Term src ss -> AST_Term src ss -> AST_Term src ss)+		g_postfix :: CF g (Unifix, AST_Term src ss -> AST_Term src ss)+		g_prefix  = g_catch $ g_source $ g_get_after $ op_prefix  <$> g_prefix_op+		g_infix   = g_catch $ g_source $ g_get_after $ op_infix   <$> g_infix_op+		g_postfix = g_catch $ g_source $ g_get_after $ op_postfix <$> g_postfix_op+		op_infix+		 :: Mod NameTe+		 -> (Imports, Modules src ss)+		 -> src+		 -> Either Error_Term_Gram+		           (Infix, AST_Term src ss -> AST_Term src ss -> AST_Term src ss)+		op_infix name (imps, mods) src = do+			t <- Error_Term_Gram_Module `left`+				lookupDefTerm FixitySing_Infix imps name mods+			Right $ (token_fixity t,) $ \a b ->+				(BinTree0 (token_term t src) `BinTree2` a) `BinTree2` b+		op_prefix, op_postfix+		 :: Mod NameTe+		 -> (Imports, Modules src ss)+		 -> src+		 -> Either Error_Term_Gram+		           ( Unifix+		           , AST_Term src ss -> AST_Term src ss )+		op_prefix name (imps, mods) src = do+			t <- Error_Term_Gram_Module `left`+				lookupDefTerm FixitySing_Prefix imps name mods+			Right $ (token_fixity t,) $ \a ->+				BinTree0 (token_term t src) `BinTree2` a+		op_postfix name (imps, mods) src = do+			t <- Error_Term_Gram_Module `left`+				lookupDefTerm FixitySing_Postfix imps name mods+			Right $ (token_fixity t,) $ \a ->+				BinTree0 (token_term t src) `BinTree2` a+		g_postfix_op :: CF g (Mod NameTe)+		g_postfix_op = rule "term_op_postfix" $+			lexeme $+				g_backquote *> g_term_mod_idname <+> -- <* (cf_of_Terminal $ Gram.Term (pure ' ') `but` g_backquote)+				g_term_mod_opname+		g_infix_op :: CF g (Mod NameTe)+		g_infix_op = rule "term_op_infix" $+			lexeme $+				between g_backquote g_backquote g_term_mod_idname <+>+				try (Fun.const <$> g_term_mod_opname <*> (string " " <+> string "\n")) <+>+				pure (Mod [] " ")+		g_prefix_op :: CF g (Mod NameTe)+		g_prefix_op = rule "term_op_prefix" $+			lexeme $+				g_term_mod_idname <* g_backquote <+>+				g_term_mod_opname+		g_backquote :: Gram_Terminal g' => g' Char+		g_backquote = char '`'+	+	g_term_atom :: CF g  (AST_Term src ss)+	g_term_atom = rule "term_atom" $+		choice $+		 {-(try (+			g_source $+			(\typ src -> BinTree0 $ inj_EToken src $ Token_Term_Type typ)+			 <$ char '@' <*> g_type) :) $+		 -}+		 (try <$> g_term_atomsR @_ @_ @ss) <>+		 [ try $+			g_catch $ g_source $ g_get_after $+			(\m (imps, mods) src ->+				case lookupDefTerm FixitySing_Infix imps m mods of+				 Right t -> Right $ BinTree0 $ token_term t src+				 Left err ->+					case m of+					 [] `Mod` n -> Right $ BinTree0 $ Token_Term_Var src n+					 _ -> Left $ Error_Term_Gram_Module err+			 ) <$> g_term_mod_name+		 , g_term_group+		 ]+	g_term_group :: CF g (AST_Term src ss)+	g_term_group = rule "term_group" $ parens g_term+	g_term_abst :: CF g (AST_Term src ss)+	g_term_abst = rule "term_abst" $+		g_source $+		((\(xs, te) src ->+			foldr (\(x, ty_x) ->+				BinTree0 . Token_Term_Abst src x ty_x) te xs) <$>) $+		g_term_abst_args_body+		 (symbol "\\" *> some g_term_abst_decl <* symbol "->")+		 g_term+	g_term_abst_args_body+	 :: CF g [(NameTe, AST_Type src)]+	 -> CF g (AST_Term src ss)+	 -> CF g ([(NameTe, AST_Type src)], AST_Term src ss)+	-- g_term_abst_args_body args body = (,) <$> args <*> body+	g_term_abst_args_body cf_args cf_body =+		g_state_before $+		(\a b (imps::Imports, mods::Modules src ss) -> ((imps, mods), (a, b)))+		 <$> g_state_after ((<$> cf_args) $ \args (imps::Imports, Modules mods) ->+			((imps, Modules $ Map.alter (setArgs args) [] mods), args))+		 <*> cf_body+		where+		setArgs args = \case+		 Nothing -> Just $ moduleEmpty {module_infix = insArg mempty args}+		 Just mod -> Just $ mod+			 { module_prefix  = delArg (module_prefix  mod) args+			 , module_infix   = insArg (module_infix   mod) args+			 , module_postfix = delArg (module_postfix mod) args+			 }+		delArg :: ModuleFixy src ss Unifix -> [(NameTe, _a)] -> ModuleFixy src ss Unifix+		delArg = foldr $ \(n, _) -> Map.delete n+		insArg :: ModuleFixy src ss Infix -> [(NameTe, _a)] -> ModuleFixy src ss Infix+		insArg = foldr $ \(n, _) ->+			Map.insert n Tokenizer+			 { token_term   = (`Token_Term_Var` n)+			 , token_fixity = infixN5+			 }+	g_term_let :: CF g  (AST_Term src ss)+	g_term_let = rule "term_let" $+		g_source $+		(\name args bound body src ->+			BinTree0 $+			Token_Term_Let src name+			 (foldr (\(x, ty_x) ->+				BinTree0 . Token_Term_Abst src x ty_x) bound args) body)+		 <$  symbol "let"+		 <*> g_term_name+		 <*> many g_term_abst_decl+		 <*  symbol "="+		 <*> g_term+		 <*  symbol "in"+		 <*> g_term++deriving instance+ ( Gram_Term src ss g+ , Gram_Term_Atoms src ss (CF g)+ ) => Gram_Term src ss (CF g)+instance+ ( Gram_Term_Atoms src ss EBNF+ , Gram_Source src EBNF+ ) => Gram_Term src ss EBNF+instance+ ( Gram_Term_Atoms src ss RuleEBNF+ , Gram_Source src RuleEBNF+ ) => Gram_Term src ss RuleEBNF++-- ** Class 'Gram_Term_Atoms'+type Gram_Term_Atoms src ss g = Gram_Term_AtomsR src ss ss g++-- *** Class 'Gram_Term_AtomsR'+class Gram_Term_AtomsR src (ss::[*]) (rs::[*]) g where+	g_term_atomsR :: [CF g (AST_Term src ss)]+instance Gram_Term_AtomsR src ss '[] g where+	g_term_atomsR = []+instance+ ( Gram_Term_AtomsFor src ss g t+ , Gram_Term_AtomsR src ss rs g+ ) => Gram_Term_AtomsR src ss (Proxy t ': rs) g where+	g_term_atomsR =+		g_term_atomsFor @_ @_ @_ @t <>+		g_term_atomsR @_ @_ @rs++-- *** Class 'Gram_Term_AtomsFor'+class Gram_Term_AtomsFor src ss g t where+	g_term_atomsFor :: [CF g (AST_Term src ss)]+	g_term_atomsFor = []++gram_term+ :: forall g.+ ( Gram_Term () '[Proxy (->), Proxy Integer] g+ ) => [CF g ()]+gram_term =+ [ voiD g_term+ , voiD g_term_operators+ , voiD g_term_atom+ , voiD g_term_group+ , voiD g_term_abst+ , void (g_term_abst_decl::CF g (NameTe, AST_Type ()))+ , voiD g_term_let+ , void g_term_mod_name+ , void g_term_name+ , void g_term_idname+ , void $ cf_of_Terminal g_term_idname_tail+ , void $ cf_of_Reg g_term_keywords+ , void g_term_mod_opname+ , void g_term_opname+ , void $ cf_of_Terminal g_term_opname_ok+ , void $ cf_of_Reg g_term_keysyms+ ] where+	voiD :: CF g (AST_Term () '[Proxy (->), Proxy Integer]) -> CF g ()+	voiD = (() <$)
+ Language/Symantic/Compiling/Module.hs view
@@ -0,0 +1,383 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}+module Language.Symantic.Compiling.Module where++import Data.Bool (not)+import Data.Map.Strict (Map)+import Data.Semigroup (Semigroup(..))+import Data.Set (Set)+import Data.String (IsString(..))+import Data.Text (Text)+import Prelude hiding (mod, not, any)+import qualified Data.Kind as K+import qualified Data.Map.Strict as Map++import Language.Symantic.Grammar+import Language.Symantic.Typing+import Language.Symantic.Compiling.Term++-- * Type 'Mod'+data Mod a = Mod PathMod a+ deriving (Eq, Functor, Ord, Show)++-- ** Type 'PathMod'+type PathMod = [NameMod]++-- ** Type 'NameMod'+newtype NameMod = NameMod Text+ deriving (Eq, Ord, Show)+instance IsString NameMod where+	fromString = NameMod . fromString++-- * Class 'ModuleFor'+class ModuleFor src ss s where+	moduleFor :: (PathMod, Module src ss)+	moduleFor = ([], moduleEmpty)++-- * Type 'Imports'+newtype Imports = Imports (Map PathMod (Map PathMod FilterImports))+ deriving (Eq, Show)+type FilterImports = Maybe (Set NameTe)++importQualifiedAs :: PathMod -> Modules src ss -> Imports+importQualifiedAs as (Modules mods) = Imports $ Map.fromList [(as, Nothing <$ mods)]++-- * Type 'Modules'+newtype Modules src ss+ =   Modules+ {   modules :: Map PathMod (Module src ss)+ } deriving (Eq, Show)++unionModules :: Modules src ss -> Modules src ss -> Either Error_Module (Modules src ss)+unionModules mx@(Modules x) my@(Modules y) =+	case check x y of+	 Just err -> Left err+	 Nothing  -> Right $ unionModulesUnchecked mx my+	where+	check ::+	 Map PathMod (Module src ss) ->+	 Map PathMod (Module src ss) ->+	 Maybe Error_Module+	check x' y' =+		case Map.intersectionWith (,) x' y' of+		 xy | null xy -> Nothing+		 xy ->+			let errs =+				Map.filter (not . null) $+				(<$> xy) $ \(a, b) ->+					inter a b module_prefix <>+					inter a b module_infix <>+					inter a b module_postfix in+			case errs of+			 e | null e -> Nothing+			 e -> Just $ Error_Module_colliding_Term e+		where+		inter a b f = Map.keysSet $ Map.intersection (f a) (f b)++unionModulesUnchecked :: Modules src ss -> Modules src ss -> Modules src ss+unionModulesUnchecked (Modules x) (Modules y) =+	Modules $ Map.unionWith (<>) x y++-- ** Type 'Error_Module'+data Error_Module+ =   Error_Module_colliding_Term (Map PathMod (Set NameTe))+ |   Error_Module_ambiguous (Mod NameTe) (Map PathMod NameTe)+ |   Error_Module_missing PathMod+ |   Error_Module_missing_Term (Mod NameTe)+ deriving (Eq, Show)++-- ** Type 'Module'+data Module src ss+ =   Module+ {   module_prefix  :: ModuleFixy src ss Unifix+ ,   module_infix   :: ModuleFixy src ss Infix+ ,   module_postfix :: ModuleFixy src ss Unifix+ } deriving (Eq, Show)++module_fixity :: FixitySing fixy -> Module src ss -> ModuleFixy src ss fixy+module_fixity = \case+	 FixitySing_Prefix  -> module_prefix+	 FixitySing_Infix   -> module_infix+	 FixitySing_Postfix -> module_postfix++moduleEmpty :: Module src ss+moduleEmpty = Module+ { module_prefix  = mempty+ , module_infix   = mempty+ , module_postfix = mempty+ }++moduleWhere :: forall src ss. Source src => PathMod -> [DefTerm src ss] -> (PathMod, Module src ss)+moduleWhere mod lst =+	(mod,) Module+	 { module_infix = mk $ \(n `WithFixity` fixy := t) ->+		case fixy of+		 Fixity2 inf -> [(n, Tokenizer inf $ Token_Term . setSource (TermAVT t))]+		 _ -> []+	 , module_prefix = mk $ \(n `WithFixity` fixy := t) ->+		case fixy of+		 Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermAVT t))]+		 _ -> []+	 , module_postfix = mk $ \(n `WithFixity` fixy := t) ->+		case fixy of+		 Fixity1 post@Postfix{} -> [(n, Tokenizer post $ Token_Term . setSource (TermAVT t))]+		 _ -> []+	 }+	where+	mk ::+	 (DefTerm src ss -> [(NameTe, Tokenizer fixy src ss)]) ->+	 Map NameTe (Tokenizer fixy src ss)+	mk = Map.fromList . (`foldMap` lst)++-- *** Type 'ModuleFixy'+type ModuleFixy src ss fixy = Map NameTe (Tokenizer fixy src ss)++instance Semigroup (Module src ss) where+	x <> y =+		Module+		 { module_prefix  = module_prefix  x <> module_prefix  y+		 , module_infix   = module_infix   x <> module_infix   y+		 , module_postfix = module_postfix x <> module_postfix y+		 }++-- ** Type 'Tokenizer'+data Tokenizer fixy src ss+ =   Tokenizer+ {   token_fixity :: fixy+ ,   token_term   :: src -> Token_Term src ss+ }+instance (Source src, Eq fixy) => Eq (Tokenizer fixy src ss) where+	Tokenizer fx x == Tokenizer fy y = fx == fy && (x noSource) == (y noSource)+instance Source src => Show (Tokenizer fixy src ss) where+	show (Tokenizer _fx x) = show (x noSource)++-- ** Type 'Token_Term'+data Token_Term src ss+ =   Token_Term      (TermAVT src ss)+ |   Token_TermVT    (TermVT src ss '[])+ |   Token_Term_Abst src NameTe (AST_Type src) (AST_Term src ss)+ |   Token_Term_Var  src NameTe+ |   Token_Term_Let  src NameTe (AST_Term src ss) (AST_Term src ss)+ |   Token_Term_App  src+ -- deriving (Eq, Show)+instance Source src => Eq (Token_Term src ss) where+	Token_Term   x == Token_Term   y = x == y+	Token_TermVT x == Token_TermVT y = x == y+	Token_Term_Abst _ nx ax rx == Token_Term_Abst _ ny ay ry = nx == ny && ax == ay && rx == ry+	Token_Term_Var _ x == Token_Term_Var _ y = x == y+	Token_Term_Let _ nx ax rx == Token_Term_Let _ ny ay ry = nx == ny && ax == ay && rx == ry+	Token_Term_App _ == Token_Term_App _ = True+	_ == _ = False+instance Source src => Show (Token_Term src ss) where+	showsPrec p (Token_Term   x) =+		showParen (p >= 10) $+		showString "Token_Term" .+		showChar ' ' . showsPrec 10 x+	showsPrec p (Token_TermVT x) =+		showParen (p >= 10) $+		showString "Token_TermVT" .+		showChar ' ' . showsPrec 10 x+	showsPrec p (Token_Term_Abst _ n a r) =+		showParen (p >= 10) $+		showString "Token_Term_Abst" .+		showChar ' ' . showsPrec 10 n .+		showChar ' ' . showsPrec 10 a .+		showChar ' ' . showsPrec 10 r+	showsPrec p (Token_Term_Var _ x) =+		showParen (p >= 10) $+		showString "Token_Term_Var" .+		showChar ' ' . showsPrec 10 x+	showsPrec p (Token_Term_Let _ n a r) =+		showParen (p >= 10) $+		showString "Token_Term_Let" .+		showChar ' ' . showsPrec 10 n .+		showChar ' ' . showsPrec 10 a .+		showChar ' ' . showsPrec 10 r+	showsPrec _p (Token_Term_App _) = showString "Token_Term_App"++-- ** Type 'NameTe'+newtype NameTe = NameTe Text+ deriving (Eq, Ord, Show)+instance IsString NameTe where+	fromString = NameTe . fromString++-- * Type 'CtxTy'+-- | /Typing context/+-- accumulating at each /lambda abstraction/+-- the 'Type' of the introduced variable.+-- It is built top-down from the closest+-- including /lambda abstraction/ to the farest.+data CtxTy src (ts::[K.Type]) where+	CtxTyZ :: CtxTy src '[]+	CtxTyS :: NameTe+	       -> Type  src '[] t+	       -> CtxTy src ts+	       -> CtxTy src (t ': ts)+infixr 5 `CtxTyS`++appendCtxTy+ :: CtxTy src ts0+ -> CtxTy src ts1+ -> CtxTy src (ts0 ++ ts1)+appendCtxTy CtxTyZ c          = c+appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'++++-- ** Type 'AST_Term'+-- | /Abstract Syntax Tree/ of 'Token_Term'.+type AST_Term src ss = BinTree (Token_Term src ss)++-- * Class 'Inj_Modules'+type Inj_Modules  src ss+ =   Inj_ModulesR src ss ss++inj_Modules ::+ forall src ss.+ Inj_Modules src ss =>+ Either Error_Module (Modules src ss)+inj_Modules = inj_ModulesR @_ @_ @ss++-- ** Class 'Inj_ModulesR'+class Inj_ModulesR src (ss::[*]) (rs::[*]) where+	inj_ModulesR :: Either Error_Module (Modules src ss)+instance Inj_ModulesR src ss '[] where+	inj_ModulesR = Right $ Modules mempty+instance+ ( ModuleFor src ss s+ , Inj_ModulesR src ss rs+ ) => Inj_ModulesR src ss (Proxy s ': rs) where+	inj_ModulesR = do+		x <- inj_ModulesR @_ @_ @rs+		let (n, m) = moduleFor @_ @_  @s+		Modules (Map.singleton n m) `unionModules` x++-- * Type 'DefTerm'+data DefTerm src ss+ = forall vs t.+ (:=) (WithFixity NameTe)+      (forall ts. Term src ss ts vs t)++-- | Lookup given 'Mod' 'NameTe' into the 'Infix' 'TermDef' of given 'Modules'.+--+-- NOTE: 'Token_Term_App' is returned for the space 'NameTe'.+lookupDefTerm ::+ forall src ss fixy.+ FixitySing fixy ->+ Imports ->+ Mod NameTe ->+ Modules src ss ->+ Either Error_Module (Tokenizer fixy src ss)+lookupDefTerm FixitySing_Infix _is ([] `Mod` " ") _ms =+	Right $ Tokenizer+	 { token_term   = Token_Term_App @src @ss+	 , token_fixity = Infix (Just AssocL) 9+	 }+lookupDefTerm fixy (Imports is) mn@(m `Mod` n) (Modules mods) =+	let mod_fixy = module_fixity fixy in+	case Map.lookup m is of+	 Nothing ->+		maybe (Left $ Error_Module_missing m) Right (Map.lookup m mods) >>=+		maybe (Left $ Error_Module_missing_Term mn) Right .+		Map.lookup n . mod_fixy+	 Just ims ->+		let look =+		 -- n matches amongst ims+			(`Map.mapMaybeWithKey` ims) $ \im _ft -> -- TODO: filter NameTe+				Map.lookup im mods >>=+				Map.lookup n . mod_fixy >>=+				Just . Map.singleton n in+		case Map.minView look of+		 Nothing -> Left $ Error_Module_missing_Term mn+		 Just (r, rs) | null rs -> Right $ snd $ Map.findMin r+		              | otherwise -> Left $ Error_Module_ambiguous mn $ fst . Map.findMin <$> look++-- | Delete given 'Mod' 'NameTe' into given 'Modules'.+deleteDefTerm :: Mod NameTe -> Modules src ss -> Modules src ss+deleteDefTerm (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms+	where del mod = mod+		 { module_prefix  = Map.delete n $ module_prefix  mod+		 , module_infix   = Map.delete n $ module_infix   mod+		 , module_postfix = Map.delete n $ module_postfix mod+		 }++-- | Delete given 'Mod' 'NameTe' into 'module_infix's of given 'Modules'.+deleteDefTermInfix :: Mod NameTe -> Modules src ss -> Modules src ss+deleteDefTermInfix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms+	where del mod = mod{module_infix = Map.delete n $ module_infix mod}++-- | Delete given 'Mod' 'NameTe' into 'module_prefix's of given 'Modules'.+deleteDefTermPrefix :: Mod NameTe -> Modules src ss -> Modules src ss+deleteDefTermPrefix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms+	where del mod = mod{module_prefix = Map.delete n $ module_prefix mod}++-- | Delete given 'Mod' 'NameTe' into 'module_postfix's of given 'Modules'.+deleteDefTermPostix :: Mod NameTe -> Modules src ss -> Modules src ss+deleteDefTermPostix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms+	where del mod = mod{module_postfix = Map.delete n $ module_postfix mod}++insertDefTerm ::+ forall src ss.+ Source src =>+ Mod (DefTerm src ss) -> Modules src ss -> Modules src ss+insertDefTerm (m `Mod` (n `WithFixity` fixy := t)) (Modules ms) =+	Modules $ Map.insert m (insertFixity ins fixy moduleEmpty) ms+	where+	ins :: fx -> ModuleFixy src ss fx -> ModuleFixy src ss fx+	ins fx = Map.insert n $ Tokenizer fx $ Token_Term . setSource (TermAVT t)++insertTermVT ::+ forall src ss.+ Source src =>+ Mod (TermVT src ss '[]) -> NameTe -> Fixity ->+ Modules src ss -> Modules src ss+insertTermVT (m `Mod` t) n fixy (Modules ms) =+	Modules $ Map.insert m (insertFixity ins fixy moduleEmpty) ms+	where+	ins :: fx -> ModuleFixy src ss fx -> ModuleFixy src ss fx+	ins fx = Map.insert n $ Tokenizer fx $ Token_TermVT . setSource t++insertFixity ::+ (forall fx. fx -> ModuleFixy src ss fx -> ModuleFixy src ss fx) ->+ Fixity -> Module src ss -> Module src ss+insertFixity ins fx mod =+	case fx of+	 Fixity1 uni@Prefix{}  -> mod {module_prefix  = ins uni $ module_prefix  mod}+	 Fixity2 inf@Infix{}   -> mod {module_infix   = ins inf $ module_infix   mod}+	 Fixity1 uni@Postfix{} -> mod {module_postfix = ins uni $ module_postfix mod}++-- ** Type 'WithFixity'+data WithFixity a+ =   WithFixity a Fixity+ deriving (Eq, Show)+instance IsString (WithFixity NameTe) where+	fromString a = WithFixity (fromString a) (Fixity2 infixN5)++withInfix :: a -> Infix -> WithFixity a+withInfix a inf = a `WithFixity` Fixity2 inf+withInfixR :: a -> Precedence -> WithFixity a+withInfixR a p = a `WithFixity` Fixity2 (infixR p)+withInfixL :: a -> Precedence -> WithFixity a+withInfixL a p = a `WithFixity` Fixity2 (infixL p)+withInfixN :: a -> Precedence -> WithFixity a+withInfixN a p = a `WithFixity` Fixity2 (infixN p)+withInfixB :: a -> (Side, Precedence) -> WithFixity a+withInfixB a (lr, p) = a `WithFixity` Fixity2 (infixB lr p)+withPrefix :: a -> Precedence -> WithFixity a+withPrefix a p = a `WithFixity` Fixity1 (Prefix p)+withPostfix :: a -> Precedence -> WithFixity a+withPostfix a p = a `WithFixity` Fixity1 (Postfix p)++-- ** Type 'FixitySing'+data FixitySing fixy where+ FixitySing_Prefix  :: FixitySing Unifix+ FixitySing_Infix   :: FixitySing Infix+ FixitySing_Postfix :: FixitySing Unifix+deriving instance Eq (FixitySing fixy)+deriving instance Show (FixitySing fixy)
+ Language/Symantic/Compiling/Read.hs view
@@ -0,0 +1,233 @@+{-# LANGUAGE GADTs #-}+module Language.Symantic.Compiling.Read where++import Control.Arrow (left)+import qualified Data.Kind as K++import Language.Symantic.Grammar+import Language.Symantic.Typing++import Language.Symantic.Compiling.Term+import Language.Symantic.Compiling.Module+import Language.Symantic.Compiling.Beta++-- * Type 'ReadTerm'+-- | Convenient type alias for 'readTerm' and related functions.+type ReadTerm src ss ts =+ Source src =>+ Inj_Source (TypeVT src) src =>+ Inj_Source (KindK src) src =>+ Inj_Source (AST_Type src) src =>+ Constable (->) =>+ Name2Type src ->+ CtxTy src ts ->+ AST_Term src ss ->+ Either (Error_Term src) (TermVT src ss ts)++-- | Read a 'TermVT' from and 'AST_Term'.+readTerm :: forall src ss ts. ReadTerm src ss ts+readTerm n2t ctxTy ast = do+	ts <- go ctxTy `traverse` ast+	inj_Error `left` betaTerms ts+	where+	go ::+	 forall ts'.+	 CtxTy src ts' ->+	 Token_Term src ss ->+	 Either (Error_Term src) (TermVT src ss ts')+	go _ts (Token_Term (TermAVT te))  = Right $ TermVT te+	go _ts (Token_TermVT te)          = Right $ liftTermVT te+	go ts  (Token_Term_Var _src name) = teVar name ts+	go _ts (Token_Term_App _src)      = Right $ TermVT teApp+	go ts  (Token_Term_Abst _src name_arg ast_ty_arg ast_body) = do+		TypeVT ty_arg <- inj_Error `left` readType n2t ast_ty_arg+		when_EqKind (inj_Kind @K.Type) (kindOf ty_arg) $ \Refl ->+			case lenVars ty_arg of+			 LenS{} -> Left $ Error_Term_polymorphic $ TypeVT ty_arg+			 LenZ | (TypeK qa, TypeK ta) <- unQualTy ty_arg -> do+				TermVT (Term qr tr (TeSym res)) <- readTerm n2t (CtxTyS name_arg ta ts) ast_body+				let (qa', qr') = appendVars qa qr+				let (ta', tr') = appendVars ta tr+				Right $+					case (proveConstraint qa', proveConstraint qr') of+					 -- NOTE: remove provable Constraints to keep those smaller.+					 (Just Dict, Just Dict) -> TermVT $+						Term (noConstraintLen (lenVars tr')) (ta' ~> tr') $+						TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)+					 (Just Dict, Nothing) -> TermVT $+						Term qr' (ta' ~> tr') $+						TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)+					 (Nothing, Just Dict) -> TermVT $+						Term qa' (ta' ~> tr') $+						TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)+					 (Nothing, Nothing) -> TermVT $+						Term (qa' # qr') (ta' ~> tr') $+						TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)+	go ts (Token_Term_Let _src name ast_arg ast_body) = do+		TermVT (Term qa ta (TeSym arg)) <- readTerm n2t ts ast_arg+		case lenVars ta of+		 LenS{} -> Left $ Error_Term_polymorphic $ TypeVT (qa #> ta)+		 LenZ -> do+			TermVT (Term qr tr (TeSym res)) <- readTerm n2t (CtxTyS name ta ts) ast_body+			let (qa', qr') = appendVars qa qr+			let tr' = allocVarsL (lenVars ta) tr+			Right $+				case (proveConstraint qa', proveConstraint qr') of+				 -- NOTE: remove provable Constraints to keep those smaller.+				 (Just Dict, Just Dict) -> TermVT $+					Term (noConstraintLen (lenVars tr')) tr' $+					TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)+				 (Just Dict, Nothing) -> TermVT $+					Term qr' tr' $+					TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)+				 (Nothing, Just Dict) -> TermVT $+					Term qa' tr' $+					TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)+				 (Nothing, Nothing) -> TermVT $+					Term (qa' # qr') tr' $+					TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)++teVar ::+ forall ss src ts.+ Source src =>+ NameTe -> CtxTy src ts -> Either (Error_Term src) (TermVT src ss ts)+teVar name CtxTyZ = Left $ Error_Term_unknown name+teVar name (CtxTyS n ty _) | n == name =+	Right $ TermVT $ Term noConstraint ty $+		TeSym $ \(te `CtxTeS` _) -> te+teVar name (CtxTyS _n _typ ts') = do+	TermVT (Term q t (TeSym te)) <- teVar @ss name ts'+	Right $ TermVT $ Term q t $+		TeSym $ \(_ `CtxTeS` ts) -> te ts++teApp ::+ Source src => Constable (->) =>+ Term src ss ts '[Proxy (a::K.Type), Proxy (b::K.Type)] (() #> ((a -> b) -> a -> b))+teApp =+	Term noConstraint ((a ~> b) ~> a ~> b) $+	TeSym $ const apply+	where+	a :: Source src => Type src '[Proxy a, Proxy b] (a::K.Type)+	a = tyVar "a" $ varZ+	b :: Source src => Type src '[Proxy a, Proxy b] (b::K.Type)+	b = tyVar "b" $ VarS varZ++-- | Reduce number of 'Token_Term_App' in given 'AST_Term' by converting them into 'BinTree2'.+--+-- NOTE: 'Token_Term_App' exists only to handle unifix operators applied to arguments.+reduceTeApp :: AST_Term src ss -> AST_Term src ss+reduceTeApp (BinTree2 x y) =+	case reduceTeApp x of+	 BinTree0 Token_Term_App{} `BinTree2` x' -> reduceTeApp x' `BinTree2` reduceTeApp y+	 _ -> reduceTeApp x `BinTree2` reduceTeApp y+reduceTeApp (BinTree0 (Token_Term_Abst src n ty te)) = BinTree0 $ Token_Term_Abst src n ty (reduceTeApp te)+reduceTeApp (BinTree0 (Token_Term_Let  src n bo te)) = BinTree0 $ Token_Term_Let  src n (reduceTeApp bo) (reduceTeApp te)+reduceTeApp x@BinTree0{} = x++-- ** Type 'ReadTermCF'+-- | Like 'ReadTerm', but 'CtxTe'-free.+-- +-- Useful in 'readTermWithCtx' to help GHC's type solver, which+-- "Cannot instantiate unification variable with a type involving foralls".+newtype ReadTermCF src ss+ =      ReadTermCF+ {    unReadTermCF :: forall ts. ReadTerm src ss ts }++-- | Like 'readTerm' but with given context, and no more.+readTermWithCtx ::+ Foldable f =>+ Source src =>+ Inj_Source (TypeVT src) src =>+ Inj_Source (KindK src) src =>+ Inj_Source (AST_Type src) src =>+ Constable (->) =>+ f (NameTe, TermT src ss '[] '[]) ->+ Name2Type src ->+ AST_Term src ss ->+ Either (Error_Term src) (TermVT src ss '[])+readTermWithCtx env =+	readTermWithCtxClose $+	readTermWithCtxPush env readTerm++-- | Like 'readTerm' but with given context.+readTermWithCtxPush ::+ Foldable f =>+ f (NameTe, TermT src ss '[] '[]) ->+ (forall ts'. ReadTerm src ss ts') ->+ ReadTerm src ss ts+readTermWithCtxPush env readTe =+	unReadTermCF $ foldr+	 (\t (ReadTermCF r) -> ReadTermCF $ readTermWithCtxPush1 t r)+	 (ReadTermCF readTe) env++-- | Like 'readTerm' but with given 'TermT' pushed onto 'CtxTy' and 'CtxTe'.+readTermWithCtxPush1 ::+ (NameTe, TermT src ss '[] '[]) ->+ (forall ts'. ReadTerm src ss ts') ->+ ReadTerm src ss ts+readTermWithCtxPush1 (n, TermT (Term qn tn (TeSym te_n))) readTe n2t ctxTy ast = do+	TermVT (Term q t (TeSym te)) <- readTe n2t (CtxTyS n (qn #> tn) ctxTy) ast+	case proveConstraint qn of+	 Nothing -> Left $ Error_Term_proofless $ TypeVT qn+	 Just Dict ->+		Right $ TermVT $ Term q t $ TeSym $ \c ->+			let cte = qual qn $ te_n CtxTeZ in+			te $ cte `CtxTeS` c++-- | Close a 'ReadTerm' context.+readTermWithCtxClose ::+ (forall ts'. ReadTerm src ss ts') ->+ Source src =>+ Inj_Source (TypeVT src) src =>+ Inj_Source (KindK src) src =>+ Inj_Source (AST_Type src) src =>+ Constable (->) =>+ Name2Type src ->+ AST_Term src ss ->+ Either (Error_Term src) (TermVT src ss '[])+readTermWithCtxClose readTe n2t = readTe n2t CtxTyZ++-- * Type 'Error_Term'+data Error_Term src+ =   Error_Term_unknown NameTe+ |   Error_Term_polymorphic (TypeVT src)+ |   Error_Term_qualified   (TypeVT src)+ |   Error_Term_proofless   (TypeVT src)+ |   Error_Term_Type (Error_Type src)+ |   Error_Term_Beta (Error_Beta src)+ {-   Error_Term_Con_Type (Con_Type src ss) -}+ {-   Error_Term_Con_Kind (Con_Kind src) -}+ deriving (Eq, Show)+instance Inj_Error (Error_Type src) (Error_Term src) where+	inj_Error = Error_Term_Type+instance Inj_Error (Error_Beta src) (Error_Term src) where+	inj_Error = Error_Term_Beta+instance Inj_Error (Con_Kind src) (Error_Term src) where+	inj_Error = Error_Term_Type . inj_Error++-- * Type 'SrcTe'+-- | A 'Source' usable when using 'readTerm'.+data SrcTe inp ss+ =   SrcTe_Less+ |   SrcTe_Input    (Span inp)+ |   SrcTe_AST_Term (AST_Term (SrcTe inp ss) ss)+ |   SrcTe_AST_Type (AST_Type (SrcTe inp ss))+ |   SrcTe_Kind     (KindK    (SrcTe inp ss))+ |   SrcTe_Type     (TypeVT   (SrcTe inp ss))+ |   SrcTe_Term+ deriving (Eq, Show)++type instance Source_Input (SrcTe inp ss) = inp++instance Source (SrcTe inp ss) where+	noSource = SrcTe_Less+instance Inj_Source (Span inp) (SrcTe inp ss) where+	inj_Source = SrcTe_Input+instance Inj_Source (AST_Term (SrcTe inp ss) ss) (SrcTe inp ss) where+	inj_Source = SrcTe_AST_Term+instance Inj_Source (AST_Type (SrcTe inp ss)) (SrcTe inp ss) where+	inj_Source = SrcTe_AST_Type+instance Inj_Source (KindK (SrcTe inp ss)) (SrcTe inp ss) where+	inj_Source = SrcTe_Kind+instance Inj_Source (TypeVT (SrcTe inp ss)) (SrcTe inp ss) where+	inj_Source = SrcTe_Type
+ Language/Symantic/Compiling/Term.hs view
@@ -0,0 +1,285 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Language.Symantic.Compiling.Term where++import Data.Maybe (isJust)+import Data.Semigroup (Semigroup(..))+import qualified Data.Kind as K+import qualified Data.Set as Set+import qualified Data.Text as Text++import Language.Symantic.Grammar+import Language.Symantic.Interpreting+import Language.Symantic.Transforming.Trans+import Language.Symantic.Typing++-- * Type 'Term'+data Term src ss ts vs (t::K.Type) where+ Term :: Type src vs       q+      -> Type src vs       t+      -> TeSym ss ts       (q #> t)+      -> Term src ss ts vs (q #> t)+instance Source src => Eq (Term src ss ts vs t) where+	Term qx tx _ == Term qy ty _ = qx == qy && tx == ty+instance Source src => Show (Term src ss ts vs t) where+	showsPrec p (Term q t _te) = showsPrec p (q #> t)++-- Source+type instance SourceOf (Term src ss ts vs t) = src+instance Source src => Sourced (Term src ss ts vs t) where+	sourceOf  (Term _q t _te)    = sourceOf t+	setSource (Term q t te) src = Term q (setSource t src) te++-- Const+instance ConstsOf (Term src ss ts vs t) where+	constsOf (Term q t _te) = constsOf q `Set.union` constsOf t++-- Var+type instance VarsOf (Term src ss ts vs t) = vs+instance LenVars (Term src ss ts vs t) where+	lenVars (Term _q t _te) = lenVars t+instance AllocVars (Term src ss ts) where+	allocVarsL len (Term q t te) = Term (allocVarsL len q) (allocVarsL len t) te+	allocVarsR len (Term q t te) = Term (allocVarsR len q) (allocVarsR len t) te++-- Fam+instance ExpandFam (Term src ss ts vs t) where+	expandFam (Term q t te) = Term (expandFam q) (expandFam t) te++-- Type+instance Inj_Source (TermT src ss ts vs) src => TypeOf (Term src ss ts vs) where+	typeOf t = typeOfTerm t `source` TermT t++typeOfTerm :: Source src => Term src ss ts vs t -> Type src vs t+typeOfTerm (Term q t _) = q #> t++-- ** Type 'TermT'+-- | 'Term' with existentialized 'Type'.+data TermT src ss ts vs = forall t. TermT (Term src ss ts vs t)+instance Source src => Show (TermT src ss ts vs) where+	showsPrec p (TermT t) = showsPrec p t++-- ** Type 'TermVT'+-- | 'Term' with existentialized 'Var's and 'Type'.+data TermVT src ss ts = forall vs t. TermVT (Term src ss ts vs t)+instance Source src => Eq (TermVT src ss ts) where+	TermVT x == TermVT y =+		case appendVars x y of+		 (Term qx' tx' _, Term qy' ty' _) ->+			isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty')+instance Source src => Show (TermVT src ss ts) where+	showsPrec p (TermVT t) = showsPrec p t+type instance SourceOf (TermVT src ss ts) = src+instance Source src => Sourced (TermVT src ss ts) where+	sourceOf  (TermVT t)     = sourceOf t+	setSource (TermVT t) src = TermVT $ setSource t src++liftTermVT :: TermVT src ss '[] -> TermVT src ss ts+liftTermVT (TermVT (Term q t (TeSym te))) =+	TermVT $ Term q t $+	TeSym $ \_c -> te CtxTeZ++-- ** Type 'TermAVT'+-- | Like 'TermVT', but 'CtxTe'-free.+data TermAVT src ss = forall vs t. TermAVT (forall ts. Term src ss ts vs t)+type instance SourceOf (TermAVT src ss) = src+instance Source src => Sourced (TermAVT src ss) where+	sourceOf  (TermAVT t)     = sourceOf t+	setSource (TermAVT t) src = TermAVT (setSource t src)+instance Source src => Eq (TermAVT src ss) where+	TermAVT x == TermAVT y =+		case appendVars x y of+		 (Term qx' tx' _, Term qy' ty' _) ->+			isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty')+instance Source src => Show (TermAVT src ss) where+	showsPrec p (TermAVT t) = showsPrec p t++-- * Type 'TeSym'+-- | Symantic of a 'Term'.+newtype TeSym ss ts (t::K.Type)+ = TeSym+ ( forall term.+   Syms ss term =>+   Sym_Lambda term =>+   QualOf t =>+   CtxTe term ts -> term (UnQualOf t)+ )++-- | Like 'TeSym', but 'CtxTe'-free+-- and using 'inj_Sym' to be able to use 'Sym'@ (@'Proxy'@ s)@ inside.+teSym ::+ forall s ss ts t.+ Inj_Sym ss s =>+ (forall term. Sym (Proxy s) term => Sym_Lambda term => QualOf t => term (UnQualOf t)) ->+ TeSym ss ts t+teSym t = inj_Sym @s (TeSym $ const t)++-- ** Type family 'QualOf'+-- | Qualification+type family QualOf (t::K.Type) :: Constraint where+	QualOf (q #> t) = q -- (q # QualOf t)+	QualOf t = (()::Constraint)++-- ** Type family 'UnQualOf'+-- | Unqualification+type family UnQualOf (t::K.Type) :: K.Type where+	UnQualOf (q #> t) = t -- UnQualOf t+	UnQualOf t = t++-- | Return 'K.Constraint' and 'K.Type' part of given 'Type'.+unQualTy ::+ Source src =>+ Type src vs (t::K.Type) ->+ ( TypeK src vs K.Constraint+ , TypeK src vs K.Type )+unQualTy (TyApp _ (TyApp _ c q) t)+ | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) c+ = (TypeK q, TypeK t)+unQualTy t = (TypeK $ noConstraintLen (lenVars t), TypeK t)++-- | Remove 'K.Constraint's from given 'Type'.+unQualsTy :: Source src => Type src vs (t::kt) -> TypeK src vs kt+unQualsTy (TyApp _ (TyApp _ c _q) t)+ | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) c+ = unQualsTy t+unQualsTy (TyApp src f a)+ | TypeK f' <- unQualsTy f+ , TypeK a' <- unQualsTy a+ = TypeK $ TyApp src f' a'+unQualsTy t = TypeK t++-- * Type 'CtxTe'+-- | GADT for an /interpreting context/:+-- accumulating at each /lambda abstraction/+-- the @term@ of the introduced variable.+data CtxTe (term::K.Type -> K.Type) (hs::[K.Type]) where+	CtxTeZ :: CtxTe term '[]+	CtxTeS :: term t+	       -> CtxTe term ts+	       -> CtxTe term (t ': ts)+infixr 5 `CtxTeS`++-- ** Type 'TermDef'+-- | Convenient type alias for defining 'Term'.+type TermDef s vs t = forall src ss ts. Source src => Inj_Sym ss s => Term src ss ts vs t++-- ** Type family 'Sym'+type family Sym (s::K.Type) :: {-term-}(K.Type -> K.Type) -> Constraint++-- ** Type family 'Syms'+type family Syms (ss::[K.Type]) (term:: K.Type -> K.Type) :: Constraint where+	Syms '[] term = ()+	Syms (s ': ss) term = (Sym s term, Syms ss term)++-- ** Type 'Inj_Sym'+-- | Convenient type synonym wrapping 'Inj_SymP'+-- applied on the correct 'Index'.+type Inj_Sym ss s = Inj_SymP (Index ss (Proxy s)) ss s++-- | Inject a given /symantic/ @s@ into a list of them,+-- by returning a function which given a 'TeSym' on @s@+-- returns the same 'TeSym' on @ss@.+inj_Sym ::+ forall s ss ts t.+ Inj_Sym ss s =>+ TeSym '[Proxy s] ts t ->+ TeSym ss ts t+inj_Sym = inj_SymP @(Index ss (Proxy s))++-- *** Class 'Inj_SymP'+class Inj_SymP p ss s where+	inj_SymP :: TeSym '[Proxy s] ts t -> TeSym ss ts t+instance Inj_SymP Zero (Proxy s ': ss) (s::k) where+	inj_SymP (TeSym te) = TeSym te+instance Inj_SymP p ss s => Inj_SymP (Succ p) (not_s ': ss) s where+	inj_SymP (te::TeSym '[Proxy s] ts t) =+		case inj_SymP @p te :: TeSym ss ts t of+		 TeSym te' -> TeSym te'++-- * Class 'Sym_Lambda'+class Sym_Lambda term where+	-- | /Function application/.+	apply :: term ((a -> b) -> a -> b)+	default apply :: Sym_Lambda (UnT term) => Trans term => term ((a -> b) -> a -> b)+	apply = trans apply+	+	-- | /Lambda application/.+	app :: term (a -> b) -> (term a -> term b); infixr 0 `app`+	default app :: Sym_Lambda (UnT term) => Trans term => term (arg -> res) -> term arg -> term res+	app = trans2 app+	+	-- | /Lambda abstraction/.+	lam :: (term a -> term b) -> term (a -> b)+	default lam :: Sym_Lambda (UnT term) => Trans term => (term arg -> term res) -> term (arg -> res)+	lam f = trans $ lam (unTrans . f . trans)+	+	-- | Convenient 'lam' and 'app' wrapper.+	let_ :: term var -> (term var -> term res) -> term res+	let_ x f = lam f `app` x+	+	-- | /Lambda abstraction/ beta-reducable without duplication+	-- (i.e. whose variable is used once at most),+	-- mainly useful in compiled 'Term's+	-- whose symantics are not a single 'term'+	-- but a function between 'term's,+	-- which happens because those are more usable when used as an embedded DSL.+	lam1 :: (term a -> term b) -> term (a -> b)+	default lam1 :: Sym_Lambda (UnT term) => Trans term => (term a -> term b) -> term (a -> b)+	lam1 = lam+	+	-- | /Qualification/.+	--+	-- Workaround used in 'readTermWithCtx'.+	qual :: proxy q -> term t -> term (q #> t)+	default qual :: Sym_Lambda (UnT term) => Trans term => proxy q -> term t -> term (q #> t)+	qual q = trans1 (qual q)++lam2 :: Sym_Lambda term => (term a -> term b -> term c) -> term (a -> b -> c)+lam3 :: Sym_Lambda term => (term a -> term b -> term c -> term d) -> term (a -> b -> c -> d)+lam4 :: Sym_Lambda term => (term a -> term b -> term c -> term d -> term e) -> term (a -> b -> c -> d -> e)+lam2 f = lam1 $ lam1 . f+lam3 f = lam1 $ lam2 . f+lam4 f = lam1 $ lam3 . f++-- Interpreting+instance Sym_Lambda Eval where+	apply  = Eval ($)+	app    = (<*>)+	lam f  = Eval (unEval . f . Eval)+	lam1   = lam+	qual _q (Eval t) = Eval $ Qual t+	let_ x f = f x -- NOTE: like flip ($)+instance Sym_Lambda View where+	apply = View $ \_po _v -> "($)"+	app (View a1) (View a2) = View $ \po v ->+		parenInfix po op $+		a1 (op, SideL) v <> " " <> a2 (op, SideR) v+		where op = infixN 10+	lam f = View $ \po v ->+		let x = "x" <> Text.pack (show v) in+		parenInfix po op $+		"\\" <> x <> " -> " <>+		unView (f (View $ \_po _v -> x)) (op, SideL) (succ v)+		where op = infixN 1+	lam1 = lam+	qual _q (View t) = View t -- TODO: maybe print q+	let_ x f =+		View $ \po v ->+			let x' = "x" <> Text.pack (show v) in+			parenInfix po op $+			"let" <> " " <> x' <> " = "+			 <> unView x (infixN 0, SideL) (succ v) <> " in "+			 <> unView (f (View $ \_po _v -> x')) (op, SideL) (succ v)+		where op = infixN 1+instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (Dup r1 r2) where+	apply = dup0 @Sym_Lambda apply+	app   = dup2 @Sym_Lambda app+	lam f = dup_1 lam_f `Dup` dup_2 lam_f+		where lam_f = lam f+	lam1 = lam+	qual q = dup1 @Sym_Lambda (qual q)
+ Language/Symantic/Interpreting.hs view
@@ -0,0 +1,10 @@+-- | Interpreting terms.+module Language.Symantic.Interpreting+ ( module Language.Symantic.Interpreting.Eval+ , module Language.Symantic.Interpreting.Dup+ , module Language.Symantic.Interpreting.View+ ) where++import Language.Symantic.Interpreting.Eval+import Language.Symantic.Interpreting.Dup+import Language.Symantic.Interpreting.View
+ Language/Symantic/Interpreting/Dup.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+-- | Interpreter to duplicate the representation of an expression+-- in order to evaluate it with different interpreters.+--+-- NOTE: this is a more verbose, less clear,+-- and maybe less efficient alternative+-- to maintaining the universal polymorphism of @term@+-- at parsing time as done with 'Term';+-- it is mainly here for the sake of curiosity.+module Language.Symantic.Interpreting.Dup where++-- | Interpreter's data.+data Dup term1 term2 a+ =   Dup+ {   dup_1 :: term1 a+ ,   dup_2 :: term2 a+ }++dup0+ :: (cl r, cl s)+ => (forall term. cl term => term a)+ -> Dup r s a+dup0 f = f `Dup` f++dup1+ :: (cl r, cl s)+ => (forall term. cl term => term a -> term b)+ -> Dup r s a+ -> Dup r s b+dup1 f (a1 `Dup` a2) =+	f a1 `Dup` f a2++dup2+ :: (cl r, cl s)+ => (forall term. cl term => term a -> term b -> term c)+ -> Dup r s a+ -> Dup r s b+ -> Dup r s c+dup2 f (a1 `Dup` a2) (b1 `Dup` b2) =+	f a1 b1 `Dup` f a2 b2++dup3+ :: (cl r, cl s)+ => (forall term. cl term => term a -> term b -> term c -> term d)+ -> Dup r s a+ -> Dup r s b+ -> Dup r s c+ -> Dup r s d+dup3 f (a1 `Dup` a2) (b1 `Dup` b2) (c1 `Dup` c2) =+	f a1 b1 c1 `Dup` f a2 b2 c2
+ Language/Symantic/Interpreting/Eval.hs view
@@ -0,0 +1,34 @@+-- | Interpreter to evaluate a term as a host-term.+module Language.Symantic.Interpreting.Eval where++import Control.Monad++-- * Type 'Eval'++-- | Interpreter's data.+newtype Eval a = Eval { unEval :: a }+instance Functor Eval where+	fmap f (Eval a) = Eval (f a)+instance Applicative Eval where+	pure = Eval+	(Eval f) <*> (Eval a) = Eval (f a)+instance Monad Eval where+	return = Eval+	(Eval a) >>= f = f a++-- | Interpreter.+eval :: Eval a -> a+eval = unEval++-- ** Constructors+eval0 :: a -> Eval a+eval0 = Eval++eval1 :: (a -> b) -> Eval a -> Eval b+eval1 = liftM++eval2 :: (a -> b -> c) -> Eval a -> Eval b -> Eval c+eval2 = liftM2++eval3 :: (a -> b -> c -> d) -> Eval a -> Eval b -> Eval c -> Eval d+eval3 = liftM3
+ Language/Symantic/Interpreting/View.hs view
@@ -0,0 +1,74 @@+{-# LANGUAGE UndecidableInstances #-}+-- | Interpreter to serialize an expression into a 'Text'.+module Language.Symantic.Interpreting.View where++import Data.Text (Text)+import qualified Data.Text as Text+import Prelude hiding (Integral(..))++import Language.Symantic.Grammar++-- * Type 'View'++-- | Interpreter's data.+newtype View a+ =      View+ {    unView -- Inherited attribuctx:+             :: (Infix, Side)+             -> DepthLam+             -- Synthetised attribuctx:+             -> Text+ }+type DepthLam = Int+instance Show (View a) where+	show = Text.unpack . view++-- | Interpreter.+view :: View a -> Text+view r = unView r (infixN0, SideL) 0++-- ** Constructors+view0 :: Text -> View a+view0 name = View $ \_op _v -> name++view1 :: Text -> View a1 -> View a+view1 name (View a1) = View $ \po v ->+		parenInfix po op $+		Text.intercalate " "+		 [ name+		 , a1 (op, SideL) v+		 ]+	where op = infixN 10++view2 :: Text -> View a1 -> View a2 -> View a+view2 name (View a1) (View a2) =+	View $ \po v ->+		parenInfix po op $+		Text.intercalate " "+		 [ name+		 , a1 (op, SideL) v+		 , a2 (op, SideL) v+		 ]+	where op = infixN 10++view3 :: Text -> View a1 -> View a2 -> View a3 -> View a+view3 name (View a1) (View a2) (View a3) =+	View $ \po v ->+		parenInfix po op $+		Text.intercalate " "+		 [ name+		 , a1 (op, SideL) v+		 , a2 (op, SideL) v+		 , a3 (op, SideL) v+		 ]+	where op = infixN 10++viewInfix :: Text -> Infix -> View a1 -> View a2 -> View a+viewInfix name op (View a1) (View a2) =+	View $ \po v ->+		parenInfix po op $+		Text.intercalate " "+		 [ a1 (op, SideL) v+		 , name+		 , a2 (op, SideR) v+		 ]
+ Language/Symantic/Transforming.hs view
@@ -0,0 +1,8 @@+-- | Transforming terms.+module Language.Symantic.Transforming+ ( module Language.Symantic.Transforming.Trans+ , module Language.Symantic.Transforming.Beta+ ) where++import Language.Symantic.Transforming.Trans+import Language.Symantic.Transforming.Beta
+ Language/Symantic/Transforming/Beta.hs view
@@ -0,0 +1,37 @@+{-# LANGUAGE GADTs #-}+-- | Interpreter to beta-reduce static lambdas+-- introduced only because of the compiling machinery+-- (hence preserving lambdas put by the user).+module Language.Symantic.Transforming.Beta where++import Language.Symantic.Transforming.Trans+import Language.Symantic.Compiling.Term++-- * Type 'BetaT'+-- | The annotation here is if a lambda is known statically,+-- and so can be applied if given an argument,+-- Moreover, it only does this beta-reduction if the lambda+-- has been introduced by the compiling phase+-- (which happens when a symantic method is a function+-- between 'term's instead of being only a 'term')+-- (i.e. 'lam1' is used, not 'lam')+data BetaT term a where+	BetaT_Unk :: term a -> BetaT term a+	BetaT_Lam1 :: (BetaT term a -> BetaT term b) -> BetaT term (a -> b)++instance Sym_Lambda term => Trans (BetaT term) where+	type UnT (BetaT term) = term+	trans = BetaT_Unk+	unTrans (BetaT_Unk t) = t+	unTrans (BetaT_Lam1 f) = lam1 $ unTrans . f . trans++-- | 'lam1' adds annotations, 'app' uses it+instance Sym_Lambda term => Sym_Lambda (BetaT term) where+	lam1 = BetaT_Lam1 -- NOTE: only 'lam1' introduces 'BetaT_Lam1', not 'lam'.+	app (BetaT_Lam1 f) = f+	app f = trans2 app f+	let_ x f = trans $ let_ (unTrans x) (unTrans . f . trans)++-- | Transformer+betaT :: Trans (BetaT term) => BetaT term a -> term a+betaT = unTrans
+ Language/Symantic/Transforming/Trans.hs view
@@ -0,0 +1,39 @@+module Language.Symantic.Transforming.Trans where++-- |+-- * 'trans' is generally not /surjective/+-- * 'unTrans' is not /injective/+-- * 'unTrans' . 'trans' == 'id'+-- * 'trans' . 'unTrans' /= 'id'+--+-- NOTE: @DefaultSignatures@ can be used+-- when declaring a symantic type class+-- to provide default definition of the methods:+-- implementing their identity transformation+-- in order to avoid boilerplate code+-- when writting 'Trans' instances which+-- do not need to alterate those methods.+class Trans tr where+	-- | Return the underlying @tr@ of the transformer.+	type UnT tr :: * -> *+	+	-- | Lift a tr to the transformer's.+	trans :: UnT tr a -> tr a+	-- | Unlift a tr from the transformer's.+	unTrans :: tr a -> UnT tr a+	+	-- | Identity transformation for a unary symantic method.+	trans1 :: (UnT tr a -> UnT tr b) -> (tr a -> tr b)+	trans1 f = trans . f . unTrans+	+	-- | Identity transformation for a binary symantic method.+	trans2+	 :: (UnT tr a -> UnT tr b -> UnT tr c)+	 -> (tr a -> tr b -> tr c)+	trans2 f t1 t2 = trans $ f (unTrans t1) (unTrans t2)+	+	-- | Identity transformation for a ternary symantic method.+	trans3+	 :: (UnT tr a -> UnT tr b -> UnT tr c -> UnT tr d)+	 -> (tr a -> tr b -> tr c -> tr d)+	trans3 f t1 t2 t3 = trans $ f (unTrans t1) (unTrans t2) (unTrans t3)
+ Language/Symantic/Typing.hs view
@@ -0,0 +1,24 @@+-- | Typing terms.+module Language.Symantic.Typing+ ( module Language.Symantic.Typing.List+ , module Language.Symantic.Typing.Peano+ , module Language.Symantic.Typing.Kind+ , module Language.Symantic.Typing.Variable+ , module Language.Symantic.Typing.Type+ , module Language.Symantic.Typing.Grammar+ , module Language.Symantic.Typing.Document+ , module Language.Symantic.Typing.Read+ , module Language.Symantic.Typing.Show+ , module Language.Symantic.Typing.Unify+ ) where++import Language.Symantic.Typing.List+import Language.Symantic.Typing.Peano+import Language.Symantic.Typing.Kind+import Language.Symantic.Typing.Variable+import Language.Symantic.Typing.Type+import Language.Symantic.Typing.Grammar+import Language.Symantic.Typing.Document+import Language.Symantic.Typing.Read+import Language.Symantic.Typing.Show+import Language.Symantic.Typing.Unify
+ Language/Symantic/Typing/Document.hs view
@@ -0,0 +1,177 @@+{-# LANGUAGE PolyKinds #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Language.Symantic.Typing.Document where++import Data.Function (id)+import Data.Map.Strict (Map)+import Data.Semigroup (Semigroup(..))+import Data.Set (Set)+import Data.Text (Text)+import Data.Typeable+import qualified Data.List as L+import qualified Data.Map.Strict as Map+import qualified Data.Set as Set+import qualified Data.Text as T++import qualified Language.Symantic.Document as D+import Language.Symantic.Grammar+import Language.Symantic.Typing.Kind+import Language.Symantic.Typing.Variable+import Language.Symantic.Typing.Type++-- * Type 'Config_Doc_Type'+newtype Config_Doc_Type+ =   Config_Doc_Type+ {   config_Doc_Type_vars_numbering :: Bool+     -- ^ Style of /type variables/:+     --+     -- * if 'True': use name and position (as in @a0@ then @a1@)+     -- * if 'False': use name, and a counter when names collide (as in @a@ then @a1@)+     --+     -- NOTE: if the name is empty, a 'freshName' is taken from 'poolNames'.+ }++config_doc_type :: Config_Doc_Type+config_doc_type =+	Config_Doc_Type+	 { config_Doc_Type_vars_numbering = True }++docType ::+ forall src vs t d.+ Semigroup d =>+ D.Doc_Text d =>+ D.Doc_Color d =>+ Config_Doc_Type ->+ Precedence ->+ Type src vs t -> d+docType conf pr ty =+	let (v2n, _) = var2Name conf mempty ty in+	go v2n (infixB SideL pr, SideL) ty+	where+	go ::+	 forall x.+	 (Map IndexVar Name) -> -- names of variables+	 (Infix, Side) ->+	 Type src vs x -> d+	go _v2n _po c+	 | Just HRefl <- proj_ConstKiTy @Constraint @() c = D.textH "()"+	go _v2n _po (TyConst _src _vs c) = D.stringH $ show c+	go v2n _po (TyVar _src _n v) =+		let iv = indexVar v in+		case Map.lookup iv v2n of+		 Nothing -> error "[BUG] docType: variable name missing"+		 Just n -> D.textH n+	go v2n _po (TyApp _ (TyConst _ _ f@Const{}) a)+	 | Just HRefl <- proj_ConstKi @(K []) @[] f =+		"[" <> go v2n (infixB SideL 0, SideL) a <> "]"+	go v2n po (TyApp _ (TyApp _ (TyConst _ _ f@Const{}) a) b)+	 | Just HRefl <- proj_ConstKiTy @Constraint @(()::Constraint) a+	 , Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f =+		go v2n po b+	 | Just (Fixity2 op) <- fixityOf f =+		(if needsParenInfix po op then D.paren else id) $+		go v2n (op, SideL) a <>+		prettyConst f <>+		go v2n (op, SideR) b+		where+		d_op = D.yellower+		unParen ('(':s) | ')':s' <- reverse s = reverse s'+		unParen s = s+		prettyConst :: forall k c. Const src (c::k) -> d+		prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = D.space <> d_op "=>" <> D.space+		prettyConst c | Just HRefl <- proj_ConstKi @(K (#))  @(#)  c = d_op "," <> D.space+		prettyConst c | Just HRefl <- proj_ConstKi @(K (,))  @(,)  c = d_op "," <> D.space+		prettyConst c@Const{}+		 | r <- typeRepTyCon (typeRep c)+		 , tyConName   r =="#~"+		 , tyConModule r =="Language.Symantic.Typing.Type"+		 -- XXX: module name must be in sync with where (#~) is defined.+		 -- NOTE: cannot use 'proj_ConstKi' here+		 -- because (#~) has a polymorphic kind.+		 = D.space <> d_op "~" <> D.space+		 | otherwise = D.space <> d_op (D.stringH $ unParen $ show c) <> D.space+	go v2n po (TyApp _src f a) =+		let op = infixL 11 in+		(if needsParenInfix po op then D.paren else id) $+		go v2n (op, SideL) f <>+		D.space <>+		go v2n (op, SideR) a+	go v2n po (TyFam _src _len fam args) =+		let op = infixL 11 in+		(if needsParenInfix po op then D.paren else id) $+		D.stringH (show fam) <>+		foldlTys (\t acc ->+			D.space <> go v2n (op, SideL) t <> acc+		 ) args D.empty++docTypes ::+ forall src vs ts d.+ Semigroup d =>+ D.Doc_Text d =>+ D.Doc_Color d =>+ Config_Doc_Type ->+ Types src vs ts -> d+docTypes conf tys =+	d_op (D.charH '[') <> go tys <> d_op (D.charH ']')+	where+	d_op = D.yellower+	go :: forall xs. Types src vs xs -> d+	go TypesZ = D.empty+	go (TypesS t0 (TypesS t1 ts)) =+		docType conf 10 t0 <>+		d_op (D.charH ',') <> D.space <>+		docType conf 10 t1 <>+		go ts+	go (TypesS t ts) = docType conf 10 t <> go ts++-- | Return a 'Map' associating a distinct 'Name'+-- for all the variables of the given 'Type'.+var2Name ::+ Config_Doc_Type ->+ (Map IndexVar Name, Names) ->+ Type src vs t ->+ (Map IndexVar Name, Names)+var2Name _cfg st TyConst{} = st+var2Name cfg st@(v2n, ns) (TyVar _src (NameVar n) v) =+	let iv = indexVar v in+	case Map.lookup iv v2n of+	 Just{} -> st+	 Nothing ->+		let n' =+			if config_Doc_Type_vars_numbering cfg && not (T.null n)+			then n <> T.pack (show iv)+			else freshifyName ns n in+		let v2n' = Map.insert iv n' v2n in+		let ns'  = Set.insert n' ns in+		(v2n', ns')+var2Name cfg st (TyApp _src f a) = var2Name cfg (var2Name cfg st f) a+var2Name cfg st (TyFam _src _len _fam as) = foldlTys (flip $ var2Name cfg) as st++-- ** Type 'Name'+type Name     = Text+type NameHint = Name+type Names    = Set Name++-- | Return given 'Name' renamed a bit to avoid+-- conflicting with any given 'Names'.+freshifyName :: Names -> Name -> Name+freshifyName ns "" = freshName ns+freshifyName ns n =+	let ints = [1..] :: [Int] in+	L.head+	 [ fresh+	 | suffix <- "" : (show <$> ints)+	 , fresh <- [n <> T.pack suffix]+	 , fresh `Set.notMember` ns+	 ]++freshName :: Names -> Name+freshName ns = L.head $ poolNames L.\\ Set.toList ns++-- | Infinite list of unique 'Name's:+-- @a, b, .., z, a1, b1 .., z1, a2, ..@+poolNames :: [Name]+poolNames =+	[ T.singleton n     | n <- ['a'..'z'] ] <>+	[ T.pack (n:show i) | n <- ['a'..'z']+	                    , i <- [1 :: Int ..] ]
+ Language/Symantic/Typing/Grammar.hs view
@@ -0,0 +1,134 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Language.Symantic.Typing.Grammar where++import Control.Applicative (Applicative(..))+import Data.List (foldl1')+import Data.String (IsString(..))+import Data.Text (Text)+import qualified Data.Char as Char++import Language.Symantic.Grammar+import Language.Symantic.Typing.Variable++-- * Type 'NameTy'+newtype NameTy = NameTy Text+ deriving (Eq, Ord, Show)+instance IsString NameTy where+	fromString = NameTy . fromString++-- ** Type 'NameConst'+type NameConst = NameTy++-- ** Type 'NameFam'+type NameFam = NameTy++-- * Type 'AST_Type'+-- | /Abstract Syntax Tree/ of 'Token_Type'.+type AST_Type src = BinTree (Token_Type src) -- (EToken src '[Proxy K.Type])++-- ** Type 'Token_Type'+data Token_Type src+ =   Token_Type_Const (At src NameTy)+ |   Token_Type_Var   (At src NameVar)+ -- deriving (Eq, Show)+instance Source src => Eq (Token_Type src) where+	Token_Type_Const (At _ x) == Token_Type_Const (At _ y) = x == y+	Token_Type_Var   (At _ x) == Token_Type_Var   (At _ y) = x == y+	_ == _ = False+instance Source src => Show (Token_Type src) where+	showsPrec p (Token_Type_Const (At _ x)) =+		showParen (p >= 10) $+		showString "Token_Type_Const" .+		showChar ' ' . showsPrec 10 x+	showsPrec p (Token_Type_Var (At _ x)) =+		showParen (p >= 10) $+		showString "Token_Type_Var" .+		showChar ' ' . showsPrec 10 x++-- * Class 'Gram_Type'+-- | Read an 'AST_Type' from a textual source.+class+ ( Gram_Source src g+ , Gram_Terminal g+ , Gram_Rule g+ , Gram_Alt g+ , Gram_Try g+ , Gram_App g+ , Gram_AltApp g+ , Gram_CF g+ , Gram_Comment g+ , Gram_Op g+ ) => Gram_Type src g where+	g_type :: CF g (AST_Type src)+	g_type = rule "type" $ g_type_fun+	g_type_fun :: CF g (AST_Type src)+	g_type_fun = rule "type_fun" $+		infixrG g_type_list (g_source $ op <$ symbol "->")+		where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src "(->)")+	-- TODO: maybe not harcoding g_type_list and g_type_tuple2+	g_type_list :: CF g (AST_Type src)+	g_type_list = rule "type_list" $+		g_source $ inside mk+		 (symbol "[") (optional g_type) (symbol "]")+		 (const <$> g_type_tuple2)+		where+		mk Nothing  src = tok src+		mk (Just a) src = BinTree2 (tok src) a+		tok src = BinTree0 $ Token_Type_Const $ At src "[]"+	g_type_tuple2 :: CF g (AST_Type src)+	g_type_tuple2 = rule "type_tuple2" $+		try (parens (infixrG (g_type) (g_source $ op <$ symbol ","))) <+> (g_type_app)+		where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src "(,)")+	g_type_app :: CF g (AST_Type src)+	g_type_app = rule "type_app" $+		foldl1' BinTree2 <$> some (g_type_atom)+	g_type_atom :: CF g (AST_Type src)+	g_type_atom = rule "type_atom" $+		try (parens g_type) <+>+		g_type_name_const <+>+		g_type_name_var <+>+		g_type_symbol+	g_type_name_const :: CF g (AST_Type src)+	g_type_name_const = rule "type_name_const" $+		lexeme $ g_source $+		(\n ns src -> BinTree0 $ Token_Type_Const $ At src $ fromString $ n:ns)+		 <$> unicat (Unicat Char.UppercaseLetter)+		 <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])+	g_type_name_var :: CF g (AST_Type src)+	g_type_name_var = rule "type_name_var" $+		lexeme $ g_source $+		(\n ns src -> BinTree0 $ Token_Type_Var $ At src $ fromString $ n:ns)+		 <$> unicat (Unicat Char.LowercaseLetter)+		 <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])+	g_type_symbol :: CF g (AST_Type src)+	g_type_symbol = rule "type_symbol" $+		g_source $ (mk <$>) $+		parens $ many $ cf_of_Terminal $ choice g_ok `but` choice g_ko+		where+		mk s src = BinTree0 $ Token_Type_Const $ At src (fromString $ "(" ++ s ++ ")")+		g_ok = unicat <$>+		 [ Unicat_Symbol+		 , Unicat_Punctuation+		 , Unicat_Mark+		 ]+		g_ko = char <$> ['(', ')', '`']++deriving instance Gram_Type src g => Gram_Type src (CF g)+instance Gram_Source src EBNF => Gram_Type src EBNF+instance Gram_Source src RuleEBNF => Gram_Type src RuleEBNF++-- | List of the rules of 'Gram_Type'.+gram_type :: Gram_Type () g => [CF g (AST_Type ())]+gram_type =+ [ g_type+ , g_type_fun+ , g_type_list+ , g_type_tuple2+ , g_type_app+ , g_type_atom+ , g_type_name_const+ , g_type_name_var+ , g_type_symbol+ ]
+ Language/Symantic/Typing/Kind.hs view
@@ -0,0 +1,142 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}+module Language.Symantic.Typing.Kind where++import Data.Type.Equality (TestEquality(..), (:~:)(..))+import qualified Data.Kind as K++import Language.Symantic.Grammar++-- * Type 'Kind'+-- | Singleton for kind types.+data Kind src k where+	KiType       :: src -> Kind src K.Type+	KiConstraint :: src -> Kind src K.Constraint+	KiFun        :: src -> Kind src ka -> Kind src kb -> Kind src (ka -> kb)+infixr 5 `KiFun`++type instance SourceOf (Kind src k) = src+instance Source src => Sourced (Kind src k) where+	sourceOf (KiType       src) = src+	sourceOf (KiConstraint src) = src+	sourceOf (KiFun src _a _b)  = src+	+	setSource (KiType       _loc) src = KiType src+	setSource (KiConstraint _loc) src = KiConstraint src+	setSource (KiFun _loc a b)    src = KiFun src a b++instance Show (Kind src k) where+	show KiType{}         = "*"+	show KiConstraint{}   = "Constraint"+	show (KiFun _src a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"+instance TestEquality (Kind src) where+	testEquality = eqKind++eqKind :: Kind xs x -> Kind ys y -> Maybe (x:~:y)+eqKind KiType{} KiType{} = Just Refl+eqKind KiConstraint{} KiConstraint{} = Just Refl+eqKind (KiFun _xs xa xb) (KiFun _ys ya yb)+ | Just Refl <- eqKind xa ya+ , Just Refl <- eqKind xb yb+ = Just Refl+eqKind _ _ = Nothing++-- * Type 'K'+type K (t::kt) = kt++-- * Class 'KindOf'+-- | Return the 'Kind' of something.+class KindOf (a::kt -> K.Type) where+	kindOf :: a t -> Kind (SourceOf (a t)) kt++-- * Type 'Inj_Kind'+-- | Implicit 'Kind'.+--+-- NOTE: GHC-8.0.1's bug <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>+-- makes it fail to properly build an implicit 'Kind',+-- this can however be worked around by having the class instances+-- work on a data type 'Ty' instead of 'Data.K.Type',+-- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'Inj_KindP'.+class (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k where+instance (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k++inj_Kind ::+ forall k src.+ Source src =>+ Inj_Kind k =>+ Kind src k+inj_Kind = inj_KindP @(Ty_of_Type k) (noSource @src)++-- ** Type 'Inj_KindP'+class Inj_KindP k where+	inj_KindP :: src -> Kind src (Type_of_Ty k)+instance Inj_KindP K.Constraint where+	inj_KindP = KiConstraint+instance Inj_KindP Ty where+	inj_KindP = KiType+instance (Inj_KindP a, Inj_KindP b) => Inj_KindP (a -> b) where+	inj_KindP src = KiFun src (inj_KindP @a src) (inj_KindP @b src)++-- ** Type 'Ty'+-- | FIXME: workaround to be removed when+-- <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>+-- will be fixed.+data Ty++-- ** Type family 'Ty_of_Type'+-- | NOTE: As of GHC-8.0.2, using a closed /type family/ does not work here,+-- this notably disables the expansion of 'Ty_of_Type'@ Any@.+type family Ty_of_Type (t::K.Type) :: K.Type+type instance Ty_of_Type K.Type       = Ty+type instance Ty_of_Type K.Constraint = K.Constraint+type instance Ty_of_Type (a -> b)     = Ty_of_Type a -> Ty_of_Type b++-- ** Type family 'Type_of_Ty'+-- | NOTE: As of GHC-8.0.2, using a closed /type family/ does not work here,+-- this notably disables the expansion of 'Type_of_Ty'@ Any@.+type family Type_of_Ty (t::K.Type) :: K.Type+type instance Type_of_Ty Ty           = K.Type+type instance Type_of_Ty K.Constraint = K.Constraint+type instance Type_of_Ty (a -> b)     = Type_of_Ty a -> Type_of_Ty b++-- * Type 'KindK'+-- | Existential for 'Kind'.+data KindK src = forall k. KindK (Kind src k)+instance Eq (KindK src) where+	KindK x == KindK y+	 | Just _ <- eqKind x y = True+	_x == _y = False+instance Show (KindK src) where+	show (KindK x) = show x++-- * Type 'Con_Kind'+data Con_Kind src+ =   Con_Kind_Eq    (KindK src) (KindK src)+ |   Con_Kind_Arrow (KindK src)+ deriving (Eq, Show)++when_EqKind+ :: Inj_Error (Con_Kind src) err+ => Kind src x+ -> Kind src y+ -> ((x :~: y) -> Either err ret) -> Either err ret+when_EqKind x y k =+	case x `eqKind` y of+	 Just Refl -> k Refl+	 Nothing -> Left $ inj_Error $ Con_Kind_Eq (KindK x) (KindK y)++when_KiFun ::+ Inj_Error (Con_Kind src) err =>+ Inj_Source (KindK src) src =>+ Kind src x ->+ (forall a b. (x :~: (a -> b)) ->+              Kind src a ->+              Kind src b ->+              Either err ret) ->+ Either err ret+when_KiFun x k =+	case x of+	 KiFun _src a b -> k Refl (a `source` KindK x) (b `source` KindK x)+	 _ -> Left $ inj_Error $ Con_Kind_Arrow (KindK x)
+ Language/Symantic/Typing/List.hs view
@@ -0,0 +1,110 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}+-- | List utilities at the type-level.+module Language.Symantic.Typing.List where++import GHC.Exts (Constraint)++import Language.Symantic.Typing.Peano++-- ** Type 'Index'+-- | Return the position of a type within a list of them.+-- This is useful to work around @OverlappingInstances@.+type family Index xs x where+	Index (x     ': xs) x = Zero+	Index (not_x ': xs) x = Succ (Index xs x)++-- * Type family @(++)@+type family (++) xs ys where+	'[] ++ ys  = ys+	-- xs  ++ '[] = xs+	(x ': xs) ++ ys = x ': xs ++ ys+infixr 5 ++++-- * Type family 'Concat'+type family Concat (xs::[[k]]) :: [k] where+	Concat '[] = '[]+	Concat (x ': xs) = x ++ Concat xs++-- * Type family 'Concat_Constraints'+type family Concat_Constraints (cs::[Constraint]) :: Constraint where+	Concat_Constraints '[] = ()+	Concat_Constraints (c ': cs) = (c, Concat_Constraints cs)++-- * Type family 'DeleteAll'+type family DeleteAll (x::k) (xs::[k]) :: [k] where+	DeleteAll x '[] = '[]+	DeleteAll x (x ': xs) = DeleteAll x xs+	DeleteAll x (y ': xs) = y ': DeleteAll x xs++-- * Type family 'Head'+type family Head (xs::[k]) :: k where+	Head (x ': _xs) = x++-- * Type family 'Tail'+type family Tail (xs::[k]) :: [k] where+	Tail (_x ': xs) = xs++{-+-- * Type family 'Map'+type family Map (f::a -> b) (cs::[a]) :: [b] where+	Map f '[] = '[]+	Map f (c ': cs) = f c ': Map f cs+-}++-- * Type family 'Nub'+type family Nub (xs::[k]) :: [k] where+	Nub '[] = '[]+	Nub (x ': xs) = x ': Nub (DeleteAll x xs)++{-+-- * Type family 'L'+type family L (xs::[k]) :: Nat where+	L '[] = 'Z+	L (x ': xs) = 'S (L xs)++-- ** Class 'Inj_L'+class Inj_L (as::[k]) where+	inj_L :: SNat (L as)+instance Inj_L '[] where+	inj_L = SNatZ+instance Inj_L as => Inj_L (a ': as) where+	inj_L = SNatS (inj_L @_ @as)+-}++-- * Type 'Len'+data Len (xs::[k]) where+	LenZ :: Len '[]+	LenS :: Len xs -> Len (x ': xs)++instance Show (Len vs) where+	showsPrec _p = showsPrec 10 . intLen++addLen :: Len a -> Len b -> Len (a ++ b)+addLen LenZ     b = b+addLen (LenS a) b = LenS $ addLen a b++shiftLen ::+ forall t b a.+ Len a ->+ Len (a ++      b) ->+ Len (a ++ t ': b)+shiftLen LenZ b = LenS b+shiftLen (LenS a) (LenS b) = LenS $ shiftLen @t @b a b++intLen :: Len xs -> Int+intLen = go 0+	where+	go :: Int -> Len xs -> Int+	go i LenZ     = i+	go i (LenS l) = go (1 + i) l++-- ** Class 'Inj_Len'+class Inj_Len (vs::[k]) where+	inj_Len :: Len vs+instance Inj_Len '[] where+	inj_Len = LenZ+instance Inj_Len as => Inj_Len (a ': as) where+	inj_Len = LenS inj_Len
+ Language/Symantic/Typing/Peano.hs view
@@ -0,0 +1,84 @@+{-# LANGUAGE GADTs #-}+{-# OPTIONS_GHC -fno-warn-missing-methods #-}+-- | Natural numbers inductivey defined at the type-level, and of kind @*@.+module Language.Symantic.Typing.Peano where++import Data.Type.Equality++-- * Types 'Zero' and 'Succ'+data Zero+data Succ p++-- ** Type synonyms for a few numbers+type P0 = Zero+type P1 = Succ P0+type P2 = Succ P1+type P3 = Succ P2+-- ...++-- * Type 'SPeano'+-- | Singleton for 'Zero' and 'Succ'.+data SPeano p where+ SZero :: SPeano Zero+ SSucc :: SPeano p -> SPeano (Succ p)+instance TestEquality SPeano where+	testEquality SZero SZero = Just Refl+	testEquality (SSucc x) (SSucc y)+	 | Just Refl <- testEquality x y+	 = Just Refl+	testEquality _ _ = Nothing++-- * Type 'IPeano'+-- | Implicit construction of 'SPeano'.+class IPeano p where+	ipeano :: SPeano p+instance IPeano Zero where+	ipeano = SZero+instance IPeano p => IPeano (Succ p) where+	ipeano = SSucc ipeano++-- * Type 'EPeano'+data EPeano where+	EPeano :: SPeano p -> EPeano+instance Eq EPeano where+	EPeano x == EPeano y =+		case testEquality x y of+		 Just _ -> True+		 _ -> False+instance Show EPeano where+	show (EPeano x) = show (integral_from_peano x::Integer)++-- * Interface with 'Integral'+integral_from_peano :: Integral i => SPeano p -> i+integral_from_peano SZero = 0+integral_from_peano (SSucc x) = 1 + integral_from_peano x++peano_from_integral :: Integral i => i -> (forall p. SPeano p -> ret) -> ret+peano_from_integral 0 k = k SZero+peano_from_integral i k | i > 0 =+	peano_from_integral (i - 1) $ \p -> k (SSucc p)+peano_from_integral _ _ = error "peano_from_integral"++{-+-- | /Type-level natural number/, inductively defined.+data Nat+ =   Z+ |   S Nat++data SNat n where+	SNatZ :: SNat 'Z+	SNatS :: SNat n -> SNat ('S n)+instance Show (SNat n) where+	showsPrec _p = showsPrec 10 . intNat++intNat :: SNat n -> Int+intNat = go 0+	where+	go :: Int -> SNat n -> Int+	go i SNatZ     = i+	go i (SNatS n) = go (1 + i) n++type family (+) (a::Nat) (b::Nat) :: Nat where+	'Z   + b = b+	'S a + b = 'S (a + b)+-}
+ Language/Symantic/Typing/Read.hs view
@@ -0,0 +1,121 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE PolyKinds #-}+module Language.Symantic.Typing.Read where++import Data.Map.Strict (Map)+import Data.Typeable+import qualified Data.Map.Strict as Map+import qualified Data.Text as Text++import Language.Symantic.Grammar+import Language.Symantic.Typing.List+import Language.Symantic.Typing.Kind+import Language.Symantic.Typing.Type+import Language.Symantic.Typing.Show ()+import Language.Symantic.Typing.Grammar+import Language.Symantic.Typing.Variable++-- | Read a 'Type' from an 'AST_Type', given its 'Vars'.+readType ::+ Inj_Source (KindK src) src =>+ Inj_Source (TypeVT src) src =>+ Inj_Source (AST_Type src) src =>+ Name2Type src ->+ AST_Type src ->+ Either (Error_Type src) (TypeVT src)+readType cs ast | EVars vs <- readVars (EVars VarsZ) ast = do+	TypeT ty <- readTyVars cs vs ast+	Right $ TypeVT ty++-- | Read a 'Type' from an 'AST_Type', given its 'Vars'.+readTyVars ::+ forall vs src.+ Inj_Source (KindK src) src =>+ Inj_Source (TypeVT src) src =>+ Inj_Source (AST_Type src) src =>+ Name2Type src ->+ Vars src vs ->+ AST_Type src ->+ Either (Error_Type src) (TypeT src vs)+readTyVars cs vs ast@(BinTree0 (Token_Type_Const (At _src name))) =+	readTyName cs (inj_Source ast) (lenVars vs) name+readTyVars _cs vs ast@(BinTree0 (Token_Type_Var (At _src name))) =+	case lookupVars name vs of+	 Just (EVar v) -> Right $ TypeT $ TyVar (inj_Source ast) name v+	 Nothing -> error "[BUG] readTyVars: lookupVars failed"+readTyVars cs vs ast@(ast_x `BinTree2` ast_y) = do+	TypeT ty_x <- readTyVars cs vs ast_x+	TypeT ty_y <- readTyVars cs vs ast_y+	when_KiFun (kindOf ty_x) $ \Refl ki_x_a _ki_x_b ->+		when_EqKind ki_x_a (kindOf ty_y) $ \Refl ->+			Right $ TypeT $ TyApp (inj_Source ast) ty_x ty_y++-- | Lookup a 'TyConst' or 'Type' synonym+-- associated with given 'NameTy' in given 'Name2Type',+-- building it for a @vs@ of given 'Len'.+readTyName ::+ Source src =>+ Name2Type src -> src -> Len vs -> NameTy ->+ Either (Error_Type src) (TypeT src vs)+readTyName cs src len name =+	case Map.lookup name cs of+	 Just (TypeTLen t) -> Right $ t len+	 Nothing -> Left $ Error_Type_Constant_unknown $ At src name++-- | Return the given 'EVars' augmented by the ones used in given 'AST_Type'.+readVars :: Source src => EVars src -> AST_Type src -> EVars src+readVars evs@(EVars vs) (BinTree0 (Token_Type_Var (At _src name))) =+	case lookupVars name vs of+	 Just{} -> evs+	 Nothing -> do+		let kv = KiType noSource+		let vs' = VarsS name kv vs+		EVars vs'+readVars evs BinTree0{} = evs+readVars evs (BinTree2 x y) =+	readVars (readVars evs x) y++-- * Type 'Name2Type'+type Name2Type src = Map NameTy (TypeTLen src)++-- ** Type 'TypeTLen'+-- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.+--+-- Useful to build a 'Name2Type' which can be used+-- whatever will be the @(@'Len'@ vs)@ given to 'readTyVars'.+newtype TypeTLen src = TypeTLen (forall vs. Len vs -> TypeT src vs)+instance Source src => Eq (TypeTLen src) where+	TypeTLen x == TypeTLen y = x LenZ == y LenZ+instance Source src => Show (TypeTLen src) where+	showsPrec p (TypeTLen t) = showsPrec p $ t LenZ++-- ** Class 'Inj_Name2Type'+-- | Derive a 'Name2Type' from the given type-level list+-- of 'Proxy'-fied /type constants/.+class Inj_Name2Type cs where+	inj_Name2Type :: Source src => Name2Type src+instance Inj_Name2Type '[] where+	inj_Name2Type = Map.empty+instance+ ( Inj_KindP (Ty_of_Type (K c))+ , K c ~ Type_of_Ty (Ty_of_Type (K c))+ , Constable c+ , Inj_Name2Type cs+ ) => Inj_Name2Type (Proxy c ': cs) where+	inj_Name2Type =+		Map.insert+		 (NameTy $ Text.pack $ show $ typeRep (Proxy @c))+		 (TypeTLen $ \len -> TypeT $ TyConst noSource len $+			inj_ConstKi @(K c) @c $+			inj_KindP @(Ty_of_Type (K c)) noSource) $+		inj_Name2Type @cs++-- * Type 'Error_Type'+data Error_Type src+ =   Error_Type_Constant_unknown (At src NameTy)+ |   Error_Type_Con_Kind         (Con_Kind src)+ deriving (Eq, Show)+instance Inj_Error (Error_Type src) (Error_Type src) where+	inj_Error = id+instance Inj_Error (Con_Kind src) (Error_Type src) where+	inj_Error = Error_Type_Con_Kind
+ Language/Symantic/Typing/Show.hs view
@@ -0,0 +1,35 @@+{-# LANGUAGE PolyKinds #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Language.Symantic.Typing.Show where++import Data.Semigroup ((<>))+import qualified Data.Text.Lazy as TL+import qualified Data.Text.Lazy.Builder as TLB++import qualified Language.Symantic.Document as D+import Language.Symantic.Grammar+import Language.Symantic.Typing.Type+import Language.Symantic.Typing.Document++showType :: Config_Doc_Type -> Type src vs t -> String+showType conf ty = TL.unpack $ TLB.toLazyText $ D.plain $ docType conf 0 ty++showTypeS :: Config_Doc_Type -> Precedence -> Type src vs t -> ShowS+showTypeS conf pr ty s = s <> TL.unpack (TLB.toLazyText $ D.plain $ docType conf pr ty)++showTypes :: Config_Doc_Type -> Types src vs ts -> String+showTypes conf tys = TL.unpack (TLB.toLazyText $ D.plain $ docTypes conf tys)++showTypesS :: Config_Doc_Type -> Types src vs ts -> ShowS+showTypesS conf tys s = s <> TL.unpack (TLB.toLazyText $ D.plain $ docTypes conf tys)++instance Source src => Show (Type src vs t) where+	showsPrec = showTypeS config_doc_type+instance Source src => Show (TypeK src vs kt) where+	showsPrec p (TypeK t) = showsPrec p t+instance Source src => Show (TypeVT src) where+	showsPrec p (TypeVT t) = showsPrec p t+instance Source src => Show (TypeT src vs) where+	showsPrec p (TypeT t) = showsPrec p t+instance Source src => Show (Types src vs ts) where+	showsPrec _ = showTypesS config_doc_type
+ Language/Symantic/Typing/Type.hs view
@@ -0,0 +1,806 @@+{-# language ConstraintKinds #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LiberalTypeSynonyms #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Language.Symantic.Typing.Type+ ( module Language.Symantic.Typing.Type+ , Proxy(..)+ , (:~:)(..)+ , (:~~:)(..)+ , K.Constraint+ ) where++import Control.Applicative (Alternative(..))+import Data.Maybe (isJust)+import Data.Proxy+import Data.Semigroup ((<>))+import Data.Set (Set)+import Data.Type.Equality+import Data.Typeable+import qualified Data.Kind as K+import qualified Data.Set as Set++import Language.Symantic.Grammar+import Language.Symantic.Typing.List+import Language.Symantic.Typing.Kind+import Language.Symantic.Typing.Variable++-- * Type 'Type'+data Type (src::K.Type) (vs::[K.Type]) (t::kt) where+	TyConst :: src -> Len vs+	               -> Const src c+	               -> Type src vs c+	TyApp   :: src -> Type src vs f+	               -> Type src vs a+	               -> Type src vs (f a)+	               -- NOTE: @f a@ decomposition made possible+	               -- at the cost of requiring @TypeInType@.+	TyVar   :: src -> NameVar+	               -> Var src vs v+	               -> Type src vs v+	TyFam   :: src -> Len vs+	               -> Const src fam+	               -> Types src vs hs+	               -> Type src vs (Fam fam hs)+	{-+	TyPi    :: src -> Type src (arg ': vs) res+	               -> Type (Pi arg res) src vs+	TyQuant :: src -> NameHint+	               -> Kind src kv+	               -> (forall (v::kv). Type src vs v -> TypeK src vs k)+	               -> Type src vs (h::k)+	TyEq :: src -> Type x src vs+	            -> Type y src vs+	            -> Type (x #~ y) src vs+	-}++instance Source src => Eq (Type src vs t) where+	x == y = isJust $ eqType x y+instance Inj_Source (TypeVT src) src => TestEquality (Type src vs) where+	testEquality = eqType++type instance SourceOf (Type src vs t) = src+instance Source src => Sourced (Type src vs t) where+	sourceOf (TyConst src _l _c)     = src+	sourceOf (TyApp   src _f _a)     = src+	sourceOf (TyVar   src _n _v)     = src+	sourceOf (TyFam   src _l _f _as) = src+	+	setSource (TyConst _src l c)    src = TyConst src l c+	setSource (TyApp   _src f a)    src = TyApp   src f a+	setSource (TyVar   _src n v)    src = TyVar   src n v+	setSource (TyFam   _src l f as) src = TyFam   src l f as++instance Inj_Source (TypeVT src) src => KindOf (Type src vs) where+	kindOf t = kindOfType t `source` TypeVT t++instance ConstsOf (Type src vs t) where+	constsOf (TyConst _src _len c)    = Set.singleton $ ConstC c+	constsOf TyVar{}                  = Set.empty+	constsOf (TyApp _src f a)         = constsOf f `Set.union` constsOf a+	constsOf (TyFam _src _len fam as) = constsOf fam `Set.union` constsOf as++type instance VarsOf (Type src vs t) = vs+instance LenVars (Type src vs t) where+	lenVars (TyConst _src len _c) = len+	lenVars (TyApp _src f _a)     = lenVars f+	lenVars (TyVar   _src _n v)   = lenVars v+	lenVars (TyFam _src l _f _as) = l+instance UsedVarsOf (Type src vs t) where+	usedVarsOf vs TyConst{} k = k vs+	usedVarsOf vs (TyFam _src _len _fam as) k = usedVarsOf vs as k+	usedVarsOf vs (TyApp _src f a) k =+		usedVarsOf vs f $ \vs' ->+		usedVarsOf vs' a k+	usedVarsOf vs (TyVar _src _n v) k =+		case insertUsedVars v vs of+		 Nothing  -> k vs+		 Just vs' -> k vs'+instance VarOccursIn (Type src vs t) where+	varOccursIn v (TyVar _src _n v') | Just{} <- v `eqVarKi` v' = False+	varOccursIn _v TyVar{}                  = False+	varOccursIn _v TyConst{}                = False+	varOccursIn v (TyApp _src f a)          = varOccursIn v f || varOccursIn v a+	varOccursIn v (TyFam _src _len _fam as) = varOccursIn v as+instance AllocVars (Type src) where+	allocVarsL len (TyConst src l c)  = TyConst src (addLen len l) c+	allocVarsL len (TyApp src f a)    = TyApp src (allocVarsL len f) (allocVarsL len a)+	allocVarsL len (TyVar src n v)    = TyVar src n $ allocVarsL len v+	allocVarsL len (TyFam src l f as) = TyFam src (addLen len l) f $ allocVarsL len `mapTys` as+	+	allocVarsR len (TyConst src l c)  = TyConst src (addLen l len) c+	allocVarsR len (TyApp src f a)    = TyApp src (allocVarsR len f) (allocVarsR len a)+	allocVarsR len (TyVar src n v)    = TyVar src n $ allocVarsR len v+	allocVarsR len (TyFam src l f as) = TyFam src (addLen l len) f $ allocVarsR len `mapTys` as++-- | Like 'TyConst', but using 'noSource' and 'inj_Const'.+-- +-- FIXME: remove @kc@ when GHC's #12933 is fixed.+tyConst ::+ forall kc (c::kc) src vs.+ Source src =>+ Inj_Len vs =>+ Constable c =>+ Inj_KindP (Ty_of_Type kc) =>+ Type_of_Ty (Ty_of_Type kc) ~ kc =>+ Type src vs c+tyConst = TyConst noSource inj_Len inj_Const+ -- NOTE: The forall brings @c@ first in the type variables,+ -- which is convenient to use @TypeApplications@.++-- | Like 'TyConst', but using 'noSource' and 'inj_Const'.+-- +-- FIXME: remove @kc@ when GHC's #12933 is fixed.+tyConstLen ::+ forall kc (c::kc) src vs.+ Source src =>+ Constable c =>+ Inj_KindP (Ty_of_Type kc) =>+ Type_of_Ty (Ty_of_Type kc) ~ kc =>+ Len vs ->+ Type src vs c+tyConstLen len = TyConst noSource len inj_Const++-- | Like 'TyApp', but using 'noSource'.+tyApp ::+ Source src =>+ Type src vs f ->+ Type src vs a ->+ Type src vs (f a)+tyApp = TyApp noSource+infixl 9 `tyApp`++-- | Like 'TyVar', but using 'noSource'.+tyVar ::+ Source src =>+ NameVar ->+ Var src vs v ->+ Type src vs v+tyVar = TyVar noSource++-- | Like 'TyFam', but using 'noSource'.+-- +-- FIXME: remove @kc@ when GHC's #12933 is fixed.+tyFam ::+ forall kc (c::kc) as vs src.+ Source src =>+ Inj_Len vs =>+ Constable c =>+ Inj_KindP (Ty_of_Type kc) =>+ Type_of_Ty (Ty_of_Type kc) ~ kc =>+ Types src vs as ->+ Type src vs (Fam c as)+tyFam = TyFam noSource inj_Len (inj_Const @c)++-- | Qualify a 'Type'.+tyQual ::+ Source src =>+ Type src vs q ->+ Type src vs t ->+ (Qual q ->+  Type src vs t ->+  Type src vs (q #> t)) ->+ Type src vs (q #> t)+tyQual q t f =+	case proveConstraint q of+	 Just Dict -> f Dict t+	 Nothing -> q #> t+infix 1 `tyQual`++-- ** Type 'TypeK'+-- | Existential 'Type' of a known 'Kind'.+data TypeK src vs kt = forall (t::kt). TypeK (Type src vs t)+type instance SourceOf (TypeK src vs ki) = src+type instance VarsOf (TypeK src vs ki) = vs+instance Source src => Eq (TypeK src vs ki) where+	TypeK x == TypeK y = isJust $ eqType x y++-- ** Type 'TypeT'+-- | Existential for 'Type'.+data TypeT src vs = forall t. TypeT (Type src vs t)+type instance SourceOf (TypeT src vs) = src+type instance VarsOf (TypeT src vs) = vs+instance Source src => Eq (TypeT src vs) where+	TypeT x == TypeT y = isJust $ eqTypeKi x y++-- ** Type 'TypeVT'+-- | Existential polymorphic 'Type'.+data TypeVT src = forall vs t. TypeVT (Type src vs t)+type instance SourceOf (TypeVT src) = src+instance Source src => Eq (TypeVT src) where+	TypeVT x == TypeVT y =+		let (x', y') = appendVars x y in+		isJust $ eqTypeKi x' y'++-- * Type 'Const'+-- | /Type constant/.+data Const src (c::kc) where+	Const :: Constable c+	      => Kind src kc+	      -> Const src (c::kc)++type instance SourceOf (Const src c) = src+instance ConstsOf (Const src c) where+	constsOf = Set.singleton . ConstC+instance Inj_Source (ConstC src) src => KindOf (Const src) where+	kindOf c@(Const kc) = kc `source` ConstC c++kindOfConst :: Const src (t::kt) -> Kind src kt+kindOfConst (Const kc) = kc++-- ** Class 'Constable'+class+ ( Typeable c+ , FixityOf c+ , ClassInstancesFor c+ , TypeInstancesFor c+ ) => Constable c+instance+ ( Typeable c+ , FixityOf c+ , ClassInstancesFor c+ , TypeInstancesFor c+ ) => Constable c++-- ** Class 'ConstsOf'+-- | Return the 'Const's used by something.+class ConstsOf a where+	constsOf :: a -> Set (ConstC (SourceOf a))++-- ** Class 'FixityOf'+-- | Return the 'Fixity' of something.+class FixityOf (c::kc) where+	fixityOf :: proxy c -> Maybe Fixity+	fixityOf _c = Nothing+instance FixityOf (c::K.Type)+instance FixityOf (c::K.Constraint)++-- Show+instance Show (Const src c) where+	showsPrec p c@Const{} = showsPrec p $ typeRep c++-- ** Type 'ConstC'+data ConstC src+ = forall c. ConstC (Const src c)+instance Eq (ConstC src) where+ ConstC x == ConstC y = isJust $ x `eqConstKi` y+instance Ord (ConstC src) where+ ConstC x `compare` ConstC y = x `ordConst` y++-- * Type '(->)'+-- | The function 'Type' @(->)@,+-- with an infix notation more readable.+(~>) ::+ Source src =>+ Constable (->) =>+ Type src vs a ->+ Type src vs b ->+ Type src vs (a -> b)+(~>) a b = (tyConstLen @(K (->)) @(->) (lenVars a) `tyApp` a) `tyApp` b+infixr 0 ~>+instance FixityOf (->) where+	fixityOf _c = Just $ Fixity2 $ infixR 0+{- NOTE: defined in Lib.Function+instance ClassInstancesFor (->)+instance TypeInstancesFor  (->)+-}++-- ** Type family 'FunArg'+type family FunArg (fun::K.Type) :: K.Type where+	FunArg (q #> f) = FunArg f+	FunArg (a -> b) = a++-- ** Type family 'FunRes'+type family FunRes (fun::K.Type) :: K.Type where+	FunRes (q #> f) = FunRes f+	FunRes (a -> b) = b++-- | Return, when the given 'Type' is a function,+-- the argument of that function.+unTyFun ::+ forall t src tys.+ Inj_Source (TypeVT src) src =>+ Constable (->) =>+ Type src tys t ->+ Maybe ( Type src tys (FunArg t)+       , Type src tys (FunRes t) )+unTyFun ty_ini = go ty_ini+	where+	go ::+	 Type src tys x ->+	 Maybe ( Type src tys (FunArg x)+	       , Type src tys (FunRes x) )+	go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)+	 | Just HRefl <- proj_ConstKi @(K (->)) @(->) f+	 = Just ((a `source` TypeVT ty_ini), (b `source` TypeVT ty_ini))+	go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)+	 | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f+	 = go b+	go TyApp{}   = Nothing+	go TyConst{} = Nothing+	go TyVar{}   = Nothing+	go TyFam{}   = Nothing++-- ** Type @(#>)@+-- | /Type constant/ to qualify a 'Type'.+newtype (#>) (q::K.Constraint) (a::K.Type) = Qual (q => a)+instance FixityOf (#>) where+	fixityOf _c = Just $ Fixity2 $ infixR 0+instance ClassInstancesFor (#>)+instance TypeInstancesFor  (#>)++(#>) ::+ Source src =>+ Type src vs a ->+ Type src vs b ->+ Type src vs (a #> b)+(#>) a b = (tyConstLen @(K (#>)) @(#>) (lenVars a) `tyApp` a) `tyApp` b+infixr 0 #>+ -- NOTE: should actually be (-1)+ -- to compose well with @infixr 0 (->)@+ -- but this is not allowed by GHC.++-- ** Class @(#)@+-- | 'K.Constraint' union.+class    (x, y) => x # y+instance (x, y) => x # y+instance FixityOf (#) where+	fixityOf _c = Just $ Fixity2 $ infixB SideL 0+instance ClassInstancesFor (#) where+	proveConstraintFor _c (TyApp _ (TyApp _ c q0) q1)+	 | Just HRefl <- proj_ConstKiTy @(K (#)) @(#) c+	 , Just Dict <- proveConstraint q0+	 , Just Dict <- proveConstraint q1+	 = Just Dict+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor (#)++(#) ::+ Source src =>+ Type src vs qx ->+ Type src vs qy ->+ Type src vs (qx # qy)+(#) a b = (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b+infixr 2 #++noConstraint ::+ Source src =>+ Inj_Len vs =>+ Type src vs (()::K.Constraint)+noConstraint = tyConstLen @K.Constraint @(()::K.Constraint) inj_Len++noConstraintLen ::+ Source src =>+ Len vs ->+ Type src vs (()::K.Constraint)+noConstraintLen = tyConstLen @K.Constraint @(()::K.Constraint)++instance ClassInstancesFor (()::K.Constraint) where+	proveConstraintFor _c q+	 | Just HRefl <- proj_ConstKiTy @K.Constraint @(()::K.Constraint) q+	 = Just Dict+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor (()::K.Constraint)++-- ** Class @(#~)@+-- | /Type equality/ 'K.Constraint'.+class    (x ~ y) => x #~ y+instance (x ~ y) => x #~ y+instance FixityOf (#~) where+	fixityOf _ = Just $ Fixity2 $ infixB SideL 0+instance+ ( Inj_Kind k+ , Typeable k+ ) => ClassInstancesFor ((#~)::k -> k -> K.Constraint) where+	proveConstraintFor _c (TyApp _ (TyApp _ c a) b)+	 | Just HRefl <- proj_ConstKiTy @(k -> k -> K.Constraint) @(#~) c+	 , Just Refl  <- eqType a b+	 = Just Dict+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor  (#~)++(#~) ::+ forall k a b src vs.+ Source src =>+ Typeable k =>+ Inj_Kind k =>+ Type src vs (a :: k) ->+ Type src vs (b :: k) ->+ Type src vs (a #~ b)+(#~) a b = (tyConstLen @(K (#~)) @(#~) (lenVars a) `tyApp` a) `tyApp` b+infixr 2 #~++{-+const_EqTy ::+ forall k src.+ Source src =>+ Typeable k =>+ Inj_Kind k =>+ Const src ((#~)::k -> k -> K.Constraint)+const_EqTy = inj_Const @(#~)+-}++-- | /Type equality/.+eqType ::+ Source src =>+ Type src tys (x::k) ->+ Type src tys (y::k) ->+ Maybe (x:~:y)+eqType x y | Just HRefl <- eqTypeKi x y = Just Refl+eqType _x _y = Nothing++-- | /Heterogeneous type equality/:+-- return two proofs when two 'Type's are equals:+-- one for the type and one for the kind.+eqTypeKi ::+ Source src =>+ Type src tys (x::kx) ->+ Type src tys (y::ky) ->+ Maybe (x:~~:y)+eqTypeKi (TyConst _sx _lx x) (TyConst _sy _ly y) = eqConstKi x y+eqTypeKi (TyVar   _sx _nx x) (TyVar   _sy _ny y) = eqVarKi   x y+eqTypeKi (TyApp _sx fx ax) (TyApp _sy fy ay)+ | Just HRefl <- eqTypeKi fx fy+ , Just HRefl <- eqTypeKi ax ay+ = Just HRefl+eqTypeKi (TyFam _ _lx fx ax) (TyFam _ _ly fy ay)+ | Just HRefl <- eqConstKi fx fy+ , Just HRefl <- eqTypes ax ay+ = Just HRefl+-- NOTE: 'TyFam' is expanded as much as possible.+eqTypeKi x@TyFam{} y = eqTypeKi (expandFam x) y+eqTypeKi x y@TyFam{} = eqTypeKi x (expandFam y)+eqTypeKi _x _y = Nothing++eqTypes ::+ Source src =>+ Types src tys x ->+ Types src tys y ->+ Maybe (x:~~:y)+eqTypes TypesZ TypesZ = Just HRefl+eqTypes (x `TypesS` sx) (y `TypesS` sy)+ | Just HRefl <- eqTypeKi x y+ , Just HRefl <- eqTypes sx sy+ = Just HRefl+eqTypes _x _y = Nothing++-- *** Comparison+-- | Compare two 'Type's.+ordType ::+ Source src =>+ Type src tys (x::kx) ->+ Type src tys (y::ky) ->+ Ordering+-- NOTE: 'TyFam' is expanded as much as possible.+ordType (TyFam _ _lx fx ax) (TyFam _ _ly fy ay) = ordConst fx fy <> ordTypes ax ay+ordType x@TyFam{} y = ordType (expandFam x) y+ordType x y@TyFam{} = ordType x (expandFam y)+ordType (TyConst _sx _lx x) (TyConst _sy _ly y) = ordConst x y+ordType TyConst{} _y = LT+ordType _x TyConst{} = GT+ordType (TyVar _sx _kx x) (TyVar _sy _ky y) = ordVarKi x y+ordType TyVar{} _y = LT+ordType _x TyVar{} = GT+ordType (TyApp _sx fx xx) (TyApp _sy fy xy) = ordType fx fy <> ordType xx xy+-- ordType TyApp{} _y = LT+-- ordType _x TyApp{} = GT++ordTypes ::+ Source src =>+ Types src tys x ->+ Types src tys y ->+ Ordering+ordTypes TypesZ TypesZ   = EQ+ordTypes TypesZ TypesS{} = LT+ordTypes TypesS{} TypesZ = GT+ordTypes (x `TypesS` sx) (y `TypesS` sy) = ordType x y <> ordTypes sx sy++-- * Type 'Qual'+-- | Captures the proof of a 'K.Constraint'+-- (and its dictionaries when it contains type classes):+-- pattern matching on the 'Dict' constructor+-- brings the 'K.Constraint' into scope.+data Qual q where+	Dict :: q => Qual q++-- ** Class 'ClassInstancesFor'+class ClassInstancesFor c where+	proveConstraintFor+	 :: Source src+	 => proxy c+	 -> Type src vs q+	 -> Maybe (Qual q)+	proveConstraintFor _c _q = Nothing++proveConstraint :: Source src => Type src vs q -> Maybe (Qual q)+proveConstraint q = foldr proj Nothing $ constsOf q+	where proj (ConstC c@Const{}) = (<|> proveConstraintFor c q)++-- ** Injection+inj_Const ::+ forall c src.+ Source src =>+ Constable c =>+ Inj_KindP (Ty_of_Type (K c)) =>+ Type_of_Ty (Ty_of_Type (K c)) ~ K c =>+ Const src c+inj_Const = Const $ inj_KindP @(Ty_of_Type (K c)) noSource++inj_ConstKi ::+ forall kc c src.+ Source src =>+ Constable c =>+ Kind src kc ->+ Const src (c::kc)+inj_ConstKi = Const++-- ** Projection+{- XXX: not working because of GHC's #12933+proj_ConstKi ::+ forall c u src.+ Constable c =>+ (K c ~ Type_of_Ty (Ty_of_Type (K c))) =>+ Inj_Kind (K c) =>+ Const src u ->+ Maybe (c :~~: u)+proj_ConstKi (Const ku) = do+	Refl <- eqKind ku $ inj_Kind @(K c) @()+	Refl :: u:~:c <- eqT+	Just HRefl+-}++-- | Like 'proj_ConstKi', but with kind equality already known.+proj_Const ::+ forall c u src.+ Typeable c =>+ Const src u ->+ Maybe (c :~: u)+proj_Const Const{} = eqT++-- | Like 'proj_Const', but on a 'Type'.+proj_ConstTy ::+ forall c u src vs.+ Typeable c =>+ Type src vs u ->+ Maybe (c :~: u)+proj_ConstTy (TyConst _src _len Const{}) = eqT+proj_ConstTy _ = Nothing++-- | XXX: 'proj_ConstKi' must be given the @kc@ kind explicitely,+-- when used multiple times in the same pattern match,+-- because of GHC's #12933.+proj_ConstKi ::+ forall kc (c::kc) u src.+ Typeable c =>+ (kc ~ Type_of_Ty (Ty_of_Type kc)) =>+ Inj_KindP (Ty_of_Type kc) =>+ Const src u ->+ Maybe (c :~~: u)+proj_ConstKi (Const ku) = do+	Refl <- eqKind ku $ inj_KindP @(Ty_of_Type kc) ()+	Refl :: u:~:c <- eqT+	Just HRefl++-- | Like 'proj_ConstKi', but on a 'Type'.+proj_ConstKiTy ::+ forall kc (c::kc) u src vs.+ Typeable c =>+ (kc ~ Type_of_Ty (Ty_of_Type kc)) =>+ Inj_KindP (Ty_of_Type kc) =>+ Type src vs u ->+ Maybe (c :~~: u)+proj_ConstKiTy (TyConst _src _len c) = proj_ConstKi c+proj_ConstKiTy _ = Nothing++eqConst ::+ Const src_x (x::k) ->+ Const src_y (y::k) ->+ Maybe (x:~:y)+eqConst (Const _kx) (Const _ky) = eqT+instance Eq (Const src c) where+	x == y = isJust $ eqConstKi x y+instance Ord (Const src c) where+	compare = ordConst++eqConstKi ::+ forall src_x src_y kx ky x y.+ Const src_x (x::kx) ->+ Const src_y (y::ky) ->+ Maybe (x:~~:y)+eqConstKi (Const kx) (Const ky)+ | Just Refl <- eqKind kx ky+ , Just (Refl::x:~:y) <- eqT+ = Just HRefl+eqConstKi _x _y = Nothing++ordConst ::+ forall src_x src_y kx ky x y.+ Const src_x (x::kx) ->+ Const src_y (y::ky) ->+ Ordering+ordConst x@Const{} y@Const{} =+	typeRep x `compare` typeRep y++normalizeQualsTy ::+ Source src =>+ Type src tys (t::kt) ->+ TypeK src tys kt+normalizeQualsTy = go+	where+	go ::+	 Source src =>+	 Type src tys (a::ka) ->+	 TypeK src tys ka+	-- (q0, q1)+	go (TyApp s1 (TyApp s0 f q0) q1)+	 | Just HRefl <- proj_ConstKiTy @(K (#)) @(#) f+	 , TypeK q0' <- go q0+	 , TypeK q1' <- go q1 =+		case (proveConstraint q0', proveConstraint q1') of+		 (Just{}, Just{})  -> TypeK $ tyConstLen @K.Constraint @(()::K.Constraint) $ lenVars q0+		 (Just{}, Nothing) -> TypeK q1'+		 (Nothing, Just{}) -> TypeK q0'+		 (Nothing, Nothing) ->+			case q0' `ordType` q1' of+			 LT -> TypeK $ TyApp s1 (TyApp s0 f q0') q1'+			 EQ -> TypeK $ q0'+			 GT -> TypeK $ TyApp s0 (TyApp s1 f q1') q0'+	-- q0 => (q1 => t)+	go (TyApp s1 (TyApp s0 f0@(TyConst sf0 lf0 _) q0) (TyApp s2 (TyApp s3 f1 q1) t))+	 | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) f0+	 , Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) f1+	 , TypeK q0' <- go q0+	 , TypeK q1' <- go q1 =+		case (proveConstraint q0', proveConstraint q1') of+		 (Just{}, Just{})  -> TypeK t+		 (Just{}, Nothing) -> TypeK $ TyApp s2 (TyApp s3 f1 q1) t+		 (Nothing, Just{}) -> TypeK $ TyApp s1 (TyApp s0 f0 q0) t+		 (Nothing, Nothing) ->+			case q0' `ordType` q1' of+			 LT ->+				let q0q1 = TyApp s2 (TyApp s0 (TyConst sf0 lf0 $ inj_Const @(#)) q0') q1' in+				TypeK $ TyApp s2 (TyApp s3 f1 q0q1) t+			 EQ -> TypeK $ TyApp s2 (TyApp s3 f1 q1') t+			 GT ->+				let q1q0 = TyApp s0 (TyApp s2 (TyConst sf0 lf0 $ inj_Const @(#)) q1') q0' in+				TypeK $ TyApp s2 (TyApp s3 f1 q1q0) t+	-- q => t+	go (TyApp _sa (TyApp _sq (TyConst _sc _lc c) q) t)+	 | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c =+		case proveConstraint q of+		 Just{} -> go t+		 Nothing+		  | TypeK q' <- go q+		  , TypeK t' <- go t+		  -> TypeK $ q' #> t'+	-- q+	go q+	 | Just Refl <- KiConstraint () `eqKind` kindOfType q+	 = case proveConstraint q of+		 Just{}  -> TypeK $ tyConstLen @K.Constraint @(()::K.Constraint) $ lenVars q+		 Nothing -> TypeK q+	go (TyApp src f a)+	 | TypeK f' <- go f+	 , TypeK a' <- go a+	 = TypeK $ TyApp src f' a'+	go t@TyFam{}   = go (expandFam t)+	go t@TyConst{} = TypeK t+	go t@TyVar{}   = TypeK t++-- * Type family 'Fam'+-- | Apply the /type family/ selected by @fam@+-- to a list of types (within a 'Proxy').+-- +-- | NOTE: |Fam|'s 'Kind' MUST be the same than @fam@'s.+type family Fam (fam::k) (hs::[K.Type]) :: k+-- type family FamKi fam :: K.Type++-- ** Class 'TypeInstancesFor'+class TypeInstancesFor (c::kc) where+	expandFamFor+	 :: Source src+	 => proxy c+	 -> Len vs+	 -> Const src fam+	 -> Types src vs ts+	 -> Maybe (Type src vs (Fam fam ts))+	expandFamFor _c _len _fam _as = Nothing++-- ** Class 'ExpandFam'+class ExpandFam a where+	expandFam :: Source (SourceOf a) => a -> a+instance ExpandFam (Type src vs t) where+	expandFam t@TyConst{} = t+	expandFam t@TyVar{} = t+	expandFam (TyApp src f a) = TyApp src (expandFam f) (expandFam a)+	expandFam t@(TyFam _src len fam as) =+		case foldr proj Nothing $ constsOf fam `Set.union` constsOf as of+		 Nothing -> t+		 Just t' -> expandFam t'+		where proj (ConstC c@Const{}) = (<|> expandFamFor c len fam as)+		-- XXX: this can loop…++-- | Like 'kindOf' but keep the old 'Source'.+kindOfType :: Type src vs (t::kt) -> Kind src kt+kindOfType (TyConst _src _l c) = kindOfConst c+kindOfType (TyApp _src f _a) =+	case kindOfType f of+	 KiFun _src_kf _kx kf -> kf+kindOfType (TyVar _src _n v)         = kindOfVar v+kindOfType (TyFam _src _len fam _as) = kindOfConst fam++-- | Remove unused 'Var's from ther context.+normalizeVarsTy ::+ Type src vs (t::kt) ->+ (forall vs'. Type src vs' (t::kt) -> ret) -> ret+normalizeVarsTy ty k =+	usedVarsOf UsedVarsZ ty $ \vs ->+	k $ goTy vs ty+	where+	goTy ::+	 UsedVars src vs vs' ->+	 Type src vs t ->+	 Type src vs' t+	goTy vs (TyConst src _len c) = TyConst src (lenVars vs) c+	goTy vs (TyApp src f a)      = TyApp src (goTy vs f) (goTy vs a)+	goTy vs (TyVar src n v) =+		case v `lookupUsedVars` vs of+		 Nothing -> error "[BUG] normalizeVarsTy: impossible lookup fail"+		 Just v' -> TyVar src n v'+	goTy vs (TyFam src _len fam as) = TyFam src (lenVars vs) fam $ goTys vs as+	+	goTys ::+	 UsedVars src vs vs' ->+	 Types src vs ts ->+	 Types src vs' ts+	goTys _vs TypesZ = TypesZ+	goTys vs (TypesS t ts) =+		goTy vs t `TypesS`+		goTys vs ts++-- * Type 'Types'+data Types src vs (ts::[K.Type]) where+	TypesZ :: Types src vs '[]+	TypesS :: Type src vs t+	       -> Types src vs ts+	       -> Types src vs (Proxy t ': ts)+infixr 5 `TypesS`++type instance SourceOf (Types src vs ts) = src+instance ConstsOf (Types src vs ts) where+	constsOf TypesZ = Set.empty+	constsOf (TypesS t ts) = constsOf t `Set.union` constsOf ts+type instance VarsOf (Types src vs ts) = vs+instance UsedVarsOf (Types src vs ts) where+	usedVarsOf vs TypesZ k = k vs+	usedVarsOf vs (TypesS t ts) k =+		usedVarsOf vs t $ \vs' ->+		usedVarsOf vs' ts k+instance VarOccursIn (Types src vs ts) where+	varOccursIn _v TypesZ = False+	varOccursIn v (TypesS t ts) = varOccursIn v t || varOccursIn v ts++mapTys ::+ (forall kt (t::kt). Type src vs t -> Type src vs' t) ->+ Types src vs  ts ->+ Types src vs' ts+mapTys _f TypesZ = TypesZ+mapTys f (TypesS t ts) = f t `TypesS` mapTys f ts++foldlTys ::+ (forall k (t::k). Type src vs t -> acc -> acc) ->+ Types src vs ts -> acc -> acc+foldlTys _f TypesZ acc = acc+foldlTys f (TypesS t ts) acc = foldlTys f ts (f t acc)++-- * Class 'TypeOf'+class TypeOf a where+	typeOf :: a t -> Type (SourceOf (a t)) (VarsOf (a t)) t
+ Language/Symantic/Typing/Unify.hs view
@@ -0,0 +1,221 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Language.Symantic.Typing.Unify where++import Data.Map.Strict (Map)+import Data.Semigroup (Semigroup(..))+import Unsafe.Coerce (unsafeCoerce)+import qualified Data.Map.Strict as Map++import Language.Symantic.Grammar+import Language.Symantic.Typing.Variable+import Language.Symantic.Typing.Kind+import Language.Symantic.Typing.Type+import Language.Symantic.Typing.Show ()++-- * Type 'Subst'+-- | /Type variable substitution/.+--+-- WARNING: a 'Subst' MUST be without loops, and fully expanded.+newtype Subst src vs+ =      Subst (Map IndexVar (VT src vs))+deriving instance Source src => Show (Subst src vs)+instance Semigroup (Subst src vs) where+	(<>) = unionSubst+instance Monoid (Subst src vs) where+	mempty  = Subst Map.empty+	mappend = (<>)++-- | Unify two 'Subst's.+--+-- NOTE: the union is left-biased: in case of duplicate 'Var's,+-- it keeps the one from the first 'Subst' given.+--+-- NOTE: the first 'Subst' given is applied to the second (with 'subst'),+-- this way each 'Var' directly maps to an expanded 'Type',+-- so that, when using the resulting 'Subst',+-- there is no need to apply it multiple times+-- until there is no more substitution to be done.+unionSubst :: Subst src vs -> Subst src vs -> Subst src vs+unionSubst sx@(Subst x) (Subst y) = Subst $ x `Map.union` ((\(VT v r) -> VT v $ subst sx r) <$> y)++-- * Type 'VT'+-- | A 'Var' and a 'Type' existentialized over their type index.+data VT src vs = forall t. VT (Var src vs t) (Type src vs t)+deriving instance Source src => Show (VT src vs)++insertSubst :: Var src vs v -> Type src vs v -> Subst src vs -> Subst src vs+insertSubst v t (Subst s) = Subst $ Map.insert (indexVar v) (VT v t) s++lookupSubst :: Var src vs v -> Subst src vs -> Maybe (Type src vs v)+lookupSubst v (Subst s)+ | Just (VT v' t) <- Map.lookup (indexVar v) s+ , Just HRefl <- v `eqVarKi` v'+ = Just t+lookupSubst _v _m = Nothing++-- * Class 'Substable'+class Substable a where+	-- | Like 'substVar', but without the /occurence check/.+	substVarUnsafe ::+	 src ~ SourceOf a =>+	 vs ~ VarsOf a =>+	 Var src vs v -> Type src vs v -> a -> a+	-- | Substitute all the 'Var's which have a match in given 'Subst'.+	subst ::+	 src ~ SourceOf a =>+	 vs ~ VarsOf a =>+	 Subst src vs -> a -> a+instance Substable (Type src vs t) where+	substVarUnsafe _v _r t@TyConst{} = t+	substVarUnsafe v r (TyApp src f a) =+		TyApp src+		 (substVarUnsafe v r f)+		 (substVarUnsafe v r a)+	substVarUnsafe v r t@(TyVar _src _n vt) =+		case v `eqVarKi` vt of+		 Just HRefl -> r+		 Nothing -> t+	substVarUnsafe v r (TyFam src len fam as) =+		TyFam src len fam $ substVarUnsafe v r as+	+	subst _s t@TyConst{} = t+	subst s (TyApp src f a) = TyApp src (subst s f) (subst s a)+	subst (Subst s) t@(TyVar _src _n v) =+		case indexVar v `Map.lookup` s of+		 Nothing -> t+		 Just (VT vr r) ->+			case v `eqVarKi` vr of+			 Nothing -> error "[BUG] subst: kind mismatch"+			 Just HRefl -> r+	subst s (TyFam src len fam as) = TyFam src len fam $ subst s as+instance Substable (Types src vs ts) where+	substVarUnsafe _v _r TypesZ = TypesZ+	substVarUnsafe v r (TypesS t ts) =+		substVarUnsafe v r t `TypesS`+		substVarUnsafe v r ts+	subst _s TypesZ = TypesZ+	subst s (TypesS t ts) = subst s t `TypesS` subst s ts++-- | Substitute the given 'Var' by the given 'Type',+-- returning 'Nothing' if this 'Type' contains+-- the 'Var' (occurence check).+substVar ::+ src ~ SourceOf a =>+ vs ~ VarsOf a =>+ Source src => VarOccursIn a => Substable a =>+ Var src vs v -> Type src vs v -> a -> Maybe a+substVar v r t =+	if v `varOccursIn` r+	then Nothing -- NOTE: occurence check+	else Just $ substVarUnsafe v r t++-- ** Type 'Error_Unify'+-- | Reasons why two 'Type's cannot be unified.+data Error_Unify src+ =   Error_Unify_Var_loop IndexVar (TypeVT src)+     -- ^ /occurence check/: a 'Var' is unified with a 'Type'+     --   which contains this same 'Var'.+ |   Error_Unify_Const_mismatch (TypeVT src) (TypeVT src)+     -- ^ Two 'TyConst's should be the same, but are different.+ |   Error_Unify_Kind_mismatch (KindK src) (KindK src)+     -- ^ Two 'Kind's should be the same, but are different.+ |   Error_Unify_Kind (Con_Kind src)+     -- ^ Two 'Kind's mismatch.+ |   Error_Unify_mismatch (TypeVT src) (TypeVT src)+     -- ^ Cannot unify those two 'Type's.++deriving instance Source src => Eq   (Error_Unify src)+deriving instance Source src => Show (Error_Unify src)++instance Inj_Error (Error_Unify src) (Error_Unify src) where+	inj_Error = id+instance Inj_Error (Con_Kind src) (Error_Unify src) where+	inj_Error = Error_Unify_Kind++-- | Return the left spine of a 'Type':+-- the root 'Type' and its 'Type' parameters,+-- from the left to the right.+spineTy ::+ forall src vs t.+ Source src =>+ Inj_Source (TypeVT src) src =>+ Type src vs t ->+ (TypeT src vs, [TypeT src vs])+spineTy typ = go [] typ+	where+	go :: forall x. [TypeT src vs] -> Type src vs x -> (TypeT src vs, [TypeT src vs])+	go ctx (TyApp _ (TyApp _ (TyConst _ _ c) _q) t)+	 | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c+	 = go ctx t -- NOTE: skip the constraint @q@.+	go ctx (TyApp  _src f a) = go (TypeT (a `source` TypeVT typ) : ctx) f+	go ctx t = (TypeT (t `source` TypeVT typ), ctx)++{-+spineTy+ :: Type src ctx ss cs (t::k)+ -> (forall kx (x::kx) xs. Type src ctx ss cs x -> Types src ctx ss cs xs -> ret)+ -> ret+spineTy = go TypesZ+	where+	go :: Types src ctx ss cs hs+	   -> Type src ctx ss cs (t::k)+	   -> (forall kx (x::kx) xs. Type src ctx ss cs x -> Types src ctx ss cs xs -> ret)+	   -> ret+	go ctx (TyApp  _src f a) k = go (a `TypesS` ctx) f k+	go ctx (Term x _te)    k = go ctx x k+	go ctx (TyAny x)       k = go ctx x k+	go ctx t k = k t ctx+-}++-- | Return the /most general unification/ of two 'Type's, when it exists.+unifyType ::+ forall ki (x::ki) (y::ki) vs src.+ Inj_Source (TypeVT src) src =>+ Inj_Error (Con_Kind src) (Error_Unify src) =>+ Subst src vs ->+ Type src vs (x::ki) ->+ Type src vs (y::ki) ->+ Either (Error_Unify src) (Subst src vs)+unifyType vs x y =+	let k = kindOfType x in+	case (spineTy x, spineTy y) of+	 ((TypeT hx, px), (TypeT hy, py)) ->+		case (hx, hy) of+		 (TyVar _ _n vx, _) | Just Refl <- k `eqKind` kindOfVar vx -> goVar vs vx y+		 (_, TyVar _ _n vy) | Just Refl <- k `eqKind` kindOfVar vy -> goVar vs vy x+		 (TyConst _sx _lx cx, TyConst _sy _ly cy)+			| Just HRefl <- cx `eqConstKi` cy -> goList vs px py+			| otherwise -> Left $ Error_Unify_Const_mismatch (TypeVT hx) (TypeVT hy)+		 _ ->+			case (x, y) of+			 (TyApp _ fx ax, TyApp _ fy ay) ->+				goList vs+				 [TypeT fx, TypeT ax]+				 [TypeT fy, TypeT ay]+			 _ -> Left $ Error_Unify_mismatch (TypeVT x) (TypeVT y)+	where+	goVar ::+	 forall k (a::k) (b::k) vs'.+	 Subst src vs' -> Var src vs' a -> Type src vs' b ->+	 Either (Error_Unify src) (Subst src vs')+	goVar vs' va b =+		case va `lookupSubst` vs' of+		 Just a -> unifyType vs' b a+		 Nothing ->+			case vs' `subst` b of+			 TyVar _src _kb vb | Just HRefl <- va `eqVarKi` vb -> Right vs'+			 b' | va `varOccursIn` b' -> Left $ Error_Unify_Var_loop (indexVar va) (TypeVT b')+			    | Refl :: a :~: b <- unsafeCoerce Refl ->+				Right $ insertSubst va b' mempty <> vs'+	goList ::+	 forall vs'.+	 Subst src vs' -> [TypeT src vs'] -> [TypeT src vs'] ->+	 Either (Error_Unify src) (Subst src vs')+	goList vs' [] [] = Right vs'+	goList vs' (TypeT a:as) (TypeT b:bs) =+		when_EqKind (kindOfType a) (kindOfType b) $ \Refl ->+		unifyType vs' a b >>= \vs'' -> goList vs'' as bs+	goList _vs _a _b = error "[BUG] unifyType: kinds mismatch"
+ Language/Symantic/Typing/Variable.hs view
@@ -0,0 +1,223 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE UndecidableInstances #-}+module Language.Symantic.Typing.Variable where++import Data.Proxy (Proxy(..))+import Data.String (IsString(..))+import Data.Text (Text)+import Data.Type.Equality ((:~:)(..))+import qualified Data.Kind as K++import Language.Symantic.Grammar+import Language.Symantic.Typing.List+import Language.Symantic.Typing.Kind++-- | /Heterogeneous propositional equality/:+-- like (:~:) but prove also that the kinds are equal.+data (:~~:) (a::ka) (b::kb) where+	HRefl :: a :~~: a++-- * Type 'Var'+-- | A /type variable/, indexed amongst a type-level list.+-- @v@ is wrapped within a 'Proxy' to have a kind-heterogeneous list.+data Var src (vs::[K.Type]) (v::kv) where+	VarZ :: Kind src kv+	     -> Len     (Proxy (v::kv) ': vs)+	     -> Var src (Proxy (v::kv) ': vs) (v::kv)+	VarS :: Var src vs v+	     -> Var src (not_v ': vs) v+infixr 5 `VarS`+type instance SourceOf (Var src vs t) = src+instance Show (Var src tys v) where+	showsPrec p v = showsPrec p (indexVar v)+instance Inj_Source (EVar src vs) src => KindOf (Var src vs) where+	kindOf v = kindOfVar v `source` EVar v+instance LenVars (Var src vs v) where+	lenVars (VarZ _k l) = l+	lenVars (VarS v)    = LenS (lenVars v)+instance AllocVars (Var src) where+	allocVarsL LenZ v       = v+	allocVarsL (LenS len) v = VarS $ allocVarsL len v+	+	allocVarsR len (VarZ k l) = VarZ k (addLen l len)+	allocVarsR len (VarS v)   = VarS $ allocVarsR len v++varZ ::+ forall src vs kv (v::kv).+ Source src =>+ Inj_Len vs =>+ Inj_Kind kv =>+ Var src (Proxy v ': vs) v+varZ = VarZ inj_Kind inj_Len++-- | Return the 'Kind' of given 'Var'.+kindOfVar :: Var src vs (v::kv) -> Kind src kv+kindOfVar (VarZ k _l) = k+kindOfVar (VarS v)    = kindOfVar v++-- ** Comparison+eqVar :: Var xs vs x -> Var ys vs y -> Maybe (x:~:y)+eqVar VarZ{} VarZ{}     = Just Refl+eqVar (VarS x) (VarS y) = eqVar x y+eqVar _ _               = Nothing++eqVarKi :: Var xs vs x -> Var ys vs y -> Maybe ((x::kx) :~~: (y::ky))+eqVarKi VarZ{} VarZ{}     = Just HRefl+eqVarKi (VarS x) (VarS y) = eqVarKi x y+eqVarKi _ _               = Nothing++ordVarKi :: Var xs vs x -> Var ys vs y -> Ordering+ordVarKi VarZ{}    VarZ{}  = EQ+ordVarKi VarZ{}    VarS{}  = LT+ordVarKi VarS{}    VarZ{}  = GT+ordVarKi (VarS x) (VarS y) = ordVarKi x y++-- * Type 'EVar'+-- | Existential 'Var'.+data EVar src vs = forall v. EVar (Var src vs v)++-- ** Type 'IndexVar'+-- | Index of a 'Var'.+type IndexVar = Int+indexVar :: Var src vs v -> Int+indexVar VarZ{} = 0+indexVar (VarS v) = 1 + indexVar v++-- * Class 'LenVars'+-- | Return the 'Len' of the 'Var' context.+class LenVars a where+	lenVars :: a -> Len (VarsOf a)++-- * Class 'AllocVars'+-- | Allocate 'Var's in a 'Var' context,+-- either to the left or to the right.+class AllocVars (a::[K.Type] -> k -> K.Type) where+	allocVarsL :: Len len -> a vs x -> a (len ++ vs) x+	allocVarsR :: Len len -> a vs x -> a (vs ++ len) x++appendVars ::+ AllocVars a =>+ AllocVars b =>+ LenVars (a vs_x x) =>+ LenVars (b vs_y y) =>+ VarsOf (a vs_x x) ~ vs_x =>+ VarsOf (b vs_y y) ~ vs_y =>+ a vs_x (x::kx) ->+ b vs_y (y::ky) ->+ ( a (vs_x ++ vs_y) x+ , b (vs_x ++ vs_y) y )+appendVars x y =+	( allocVarsR (lenVars y) x+	, allocVarsL (lenVars x) y+	)++-- * Type 'NameVar'+newtype NameVar = NameVar Text+ deriving (Eq, Ord, Show)+instance IsString NameVar where+	fromString = NameVar . fromString++-- * Class 'VarOccursIn'+-- | Test whether a given 'Var' occurs within something.+class VarOccursIn a where+	varOccursIn :: Var src (VarsOf a) v -> a -> Bool++-- * Type family 'VarsOf'+-- | Return the 'Var' context of something.+type family   VarsOf a :: [K.Type]+type instance VarsOf (Var src vs v) = vs+type instance VarsOf (UsedVars src vs vs') = vs'++-- * Type 'Vars'+-- | Growable list of 'Var's.+data Vars src vs where+ VarsZ :: Vars src '[]+ VarsS :: NameVar ->+          Kind src kv ->+          Vars src vs ->+          Vars src (Proxy (v::kv) ': vs)+type instance VarsOf (Vars src vs) = vs+instance LenVars (Vars src vs) where+	lenVars VarsZ = LenZ+	lenVars (VarsS _n _kv vs) = LenS $ lenVars vs++lookupVars ::+ NameVar ->+ Vars src vs ->+ Maybe (EVar src vs)+lookupVars _n VarsZ = Nothing+lookupVars n (VarsS n' kv vs) =+	if n == n'+	then Just $ EVar $ VarZ kv (LenS $ lenVars vs)+	else (\(EVar v) -> EVar $ VarS v) <$> lookupVars n vs++insertVars ::+ NameVar ->+ Kind src k ->+ Vars src vs ->+ (forall vs'. Vars src vs' -> ret) -> ret+insertVars n kv vs k =+	case lookupVars n vs of+	 Just{} -> k vs -- TODO: check kind?+	 Nothing -> k $ VarsS n kv vs++-- ** Type 'EVars'+-- | Existential 'Vars'.+data EVars src = forall vs. EVars (Vars src vs)++-- * Type 'UsedVars'+-- | List of 'Var's, used to change the context of a 'Var'+-- when removing unused 'Var's.+data UsedVars src vs vs' where+ UsedVarsZ :: UsedVars src vs '[]+ UsedVarsS :: Var src vs (v::k) ->+              UsedVars src vs vs' ->+              UsedVars src vs (Proxy v ': vs')+instance LenVars (UsedVars src vs vs') where+	lenVars UsedVarsZ         = LenZ+	lenVars (UsedVarsS _v vs) = LenS $ lenVars vs++lookupUsedVars ::+ Var src vs v ->+ UsedVars src vs vs' ->+ Maybe (Var src vs' v)+lookupUsedVars _v UsedVarsZ = Nothing+lookupUsedVars v (UsedVarsS v' vs) =+	case v `eqVarKi` v' of+	 Just HRefl -> Just $ VarZ (kindOfVar v) (LenS $ lenVars vs)+	 Nothing -> VarS <$> lookupUsedVars v vs++insertUsedVars ::+ Var src vs v ->+ UsedVars src vs vs' ->+ Maybe (UsedVars src vs (Proxy v ': vs'))+insertUsedVars v vs =+	case lookupUsedVars v vs of+	 Just{} -> Nothing+	 Nothing -> Just $ UsedVarsS v vs++-- ** Class 'UsedVarsOf'+class UsedVarsOf a where+	usedVarsOf ::+	 UsedVars (SourceOf a) (VarsOf a) vs -> a ->+	 (forall vs'. UsedVars (SourceOf a) (VarsOf a) vs' -> ret) -> ret++-- * Type 'UnProxy'+type family UnProxy (x::K.Type) :: k where+	UnProxy (Proxy x) = x++{-+-- ** Type family 'V'+type family V (vs::[K.Type]) (i::Nat) :: k where+	V (v ': vs) 'Z  = UnProxy v+	V (not_v ': vs) ('S i) = V vs i++-- ** Type family 'KV'+type family KV (vs::[K.Type]) (i::Nat) :: K.Type where+	KV (Proxy v ': vs) 'Z     = K v+	KV (not_v   ': vs) ('S i) = KV vs i+-}
+ symantic.cabal view
@@ -0,0 +1,289 @@+author: Julien Moutinho <julm+symantic@autogeree.net>+bug-reports: Julien Moutinho <julm+symantic@autogeree.net>+build-type: Simple+cabal-version: >= 1.24+category: Language+description:+ __Description__+ .+ This is an experimental library for composing, parsing, typing, compiling, transforming and interpreting+ a custom DSL (Domain-Specific Language) expressing+ a subset of GHC's Haskell type system:+ .+ * /first class functions/ (aka. /lambdas/),+ * chosen /monomorphic types/ (like 'Bool' or 'Maybe'),+ * chosen /rank-1 polymorphic types/ (like @(@'Maybe'@ a)@),+ * chosen /type class instances/,+ * chosen /type family instances/,+ * and chosen /type constraints/;+ .+ where "chosen X" means declared in Haskell+ and selected when composing the DSL.+ .+ In particular, this library is currently not able to:+ .+ * do /type inferencing/ for the argument of /lambdas/+   (they must all be explicitely annotated, aka. /Church-style/),+ * do /pattern matching/ (aka. /case/) (but /Church-encoding/ functions are often enough),+ * do /rank-N polymorphic types/ (aka. /non-prenex forall/, like @(forall s. ST s a) -> a@).+ .+ And by itself, the DSL is only able to define new terms to be interpreted,+ no new types, or other type-level structures.+ .+ __Warning__+ .+ Please be aware that despite its using of powerful ideas from clever people,+ this remains a FUND-LESS SINGLE-PERSON EXPERIMENTAL LIBRARY.+ Meaning that it IS NOT heavily tested and documented,+ DOES NOT have a strong commitment to preserving backward compatibility,+ MAY FAIL to comply with the <http://www.haskell.org/haskellwiki/Package_versioning_policy PVP>,+ and CAN die without notice.+ You've been warned.+ .+ __Use cases__+ .+ The main goal of this library is to enable the runtime interpretation of terms,+ type-checked according to some types defined at composing-time (ie. GHC's compile-time).+ .+ Using a DSL enables to limit expressiveness in order to ease analysis.+ Here the idea is that the more complex logic shall remain written in Haskell,+ and then this library used to project an interface into a DSL+ (using GHC's Haskell as a FFI (Foreign Function Interface)).+ This in order to give runtime users the flexibility+ to write programs not requiring a full-blown Haskell compiler,+ yet enabling enough flexibility to let them express complex needs+ with a reasonably advanced type-safe way+ and a controlled environment of primitives.+ .+ Typical use cases:+ .+ * Enabling runtime users to enter some Haskell-like expressions+   (maybe with a more convenient syntax wrt. the domain problem)+   without using at runtime all the heavy machinery and ecosystem of GHC+   (eg. by using <https://hackage.haskell.org/package/hint hint>),+   but still leaning on primitive functions coded in GHC's Haskell.+ * Limiting those expressions to be built from well-controlled expressions only.+ * Run some analyzes/optimizations on those well-controlled expressions.+ .+ __Usage__+ .+ Please pick in <https://hackage.haskell.org/package/symantic-lib symantic-lib>+ a few specific @Lib/*.hs@ files near what you want to do+ and the corresponding @Lib\/*/Test.hs@ file,+ if any in the <git://git.autogeree.net/symantic Git repository>,+ to learn by examples how to use this library.+ .+ Those @Lib\/*/Test.hs@ files use <https://hackage.haskell.org/package/megaparsec megaparsec> as parser+ (see @Grammar/Megaparsec.hs@) and a default grammar somehow sticking to Haskell's,+ but staying context-free (so in particular: insensitive to the indentation),+ and supporting prefix and postfix operators.+ This grammar — itself written as a symantic embedded DSL+ with <https://hackage.haskell.org/package/symantic-grammar symantic-grammar> —+ can be reused to build other ones, is not bound to a specific parser,+ and can produce its own EBNF rendition.+ .+ __Acknowledgements__+ .+ This library would probably be much worse than it is+ without the following seminal works:+ .+ * <http://okmij.org/ftp/tagless-final/ Finally Tagless> by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan.+ * <http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf Dependent Types in Haskell> by Richard A. Eisenberg.+ .+ __Main ideas__+ .+ * __Symantic DSL__.+   Terms are encoded in the <http://okmij.org/ftp/tagless-final/ Tagless-Final> way (aka. the /symantic/ way)+   which leverages the /type class/ system of Haskell — instead of using /data types/ — to form an embedded DSL.+   More specifically, a /class/ encodes the /syntax/ of terms (eg. 'Sym_Bool')+   and its /class instances/ on a dedicated type encodes their /semantics/+   (eg. @(Sym_Bool Eval)@ interprets a term as a value of its type+   in the host language ('Bool' in Haskell here),+   or @(Sym_Bool View)@ interprets a term as a textual rendition, etc.).+   +   DSL are then composed/extended by selecting those symantic /classes/+   (and in an embedded DSL those could even be automatically inferred,+   when @NoMonomorphismRestriction@ is on).+   Otherwise, when using symantics for a non-embedded DSL+   — the whole point of this library — the /classes/ composing the DSL+   are selected manually at GHC's compile-time,+   through the /type-level list/ @ss@ given to 'readTerm'.+   +   Moreover, those symantic @term@s are parameterized by the type of the value they encode,+   in order to get the same type safety as with plain Haskell values.+   Hence the symantic /classes/ have the higher kind: @((* -> *) -> Constraint)@+   instead of just @(* -> Constraint)@.+   +   Amongst those symantics, 'Sym_Lambda' introduces /lambda abstractions/ by an higher-order approach,+   meaning that they directly reuse GHC's internal machinery+   to abstract or instantiate variables,+   which I think is by far the most efficient and simplest way of doing it+   (no (generalized or not) DeBruijn encoding+   like in <https://hackage.haskell.org/package/bound bound>'s @Monad@s).+ + * __Singleton for any type__.+   To typecheck terms using a @(@'Type'@ src vs t)@ which acts as a /singleton type/+   for any Haskell /type index/ @t@ of any kind,+   which is made possible with the dependant Haskell extensions:+   especially @TypeFamilies@, @GADTs@ and @TypeInType@.+ + * __Type constants using 'Typeable'__.+   /Type constant/ could be introduced by indexing them amongst a /type-level list/,+   but since they are /monomorphic types/, using 'Typeable' simplifies+   the machinery, and is likely more space/time efficient, including at GHC-compile-time.+ + * __Type variables using a type-level list__.+   Handling /type variables/ is done by indexing them amongst a @vs@ /type-level list/,+   where each /type variable/ is wrapped inside a @Proxy@ to handle different kinds.+   Performing a substitution (in 'substVar') preserves the /type index/ @t@,+   which is key for preserving any associated 'Term'.+   Unifying /type variables/ is done with 'unsafeCoerce' (in 'unifyType'),+   which I think is necessary and likely safe.+ + -- NOTE: no longer used.+ -- * __Extensible data type__.+ --   To inject a type into a /type-level list/+ --   or project a /type-level list/ onto a type,+ --   to compose an /extensible data type/+ --   (eg. the 'Token' @GADT@ gathering the 'TokenT' /data instances/,+ --   that a parser can build and then give to 'compile').+ --   This type-level programming requires @UndecidableInstances@,+ --   but not @OverlappingInstances@.+ -- + --   There is a similarity with+ --   <http://dx.doi.org/10.1017/S0956796808006758 Data types à la carte>+ --   (see for instance <https://hackage.haskell.org/package/compdata compdata>+ --   or <https://hackage.haskell.org/package/syntactic syntactic>).+ --   Those also enable to compose a DSL using some machinery+ --   based upon (co)free(r) (co)monads and (cata|ana)morphisms.+ --   Which library fits best your problem domain and brain is for you to judge :)+ --   On that topic, see also:+ --   <https://www.youtube.com/watch?v=qaAKRxO21fU Stop Paying for Free Monads>.+ --+ -- Here, I just came up using /type-level lists/ by hacking+ -- <https://hackage.haskell.org/package/glambda glambda>'s @Elem@.+ .+ __Main extensions__+ .+ * @AllowAmbiguousTypes@ for avoiding a lot of uses of 'Proxy'.+ * @ConstraintKinds@ for /type lists/ to contain 'Constraint's,+   or reifying any 'Constraint' as an explicit dictionary 'Dict',+   or defining /type synonym/ of /type classes/,+   or merging /type constraints/.+ * @DataKinds@ for type-level data structures (eg. /type-level lists/).+ * @DefaultSignatures@ for providing identity transformations of terms,+   and thus avoid boilerplate code when a transformation+   does not need to alter all semantics.+   Almost as explained in <https://ro-che.info/articles/2016-02-03-finally-tagless-boilerplate Reducing boilerplate in finally tagless style>.+ * @GADTs@ for knowing types by pattern-matching terms,+   or building terms by using type classes.+ * @PolyKinds@ for avoiding a lot of uses of 'Proxy'.+ * @Rank2Types@ or @ExistentialQuantification@ for parsing @GADT@s.+ * @TypeApplications@ for having a more concise syntax+   to build 'Type' (eg. 'tyConst'@ @\@Bool).+ * @TypeFamilies@ for type-level programming.+ * @TypeInType@ (introduced in GHC 8.0.1)+   for 'Type' to also bind a kind equality for the type @t@ it encodes.+   Which makes the /type application/ ('TyApp')+   give us an /arrow kind/ for the Haskell /type constructor/+   it applies an Haskell type to, releaving me from tricky workarounds.+ * @UndecidableInstances@ for type-level programming that may never terminate.+ .+ __Bugs__+ .+ There are some of them hidding in there,+ and the whole thing is far from being perfect…+ Your comments, problem reports, or questions, are welcome!+ You have my email address, so… just send me some emails :]+ .+ __To do__+ .+ * Study to which point /type inferencing/ is doable,+   now that 'Type' is powerful enough to contain 'TyVar's.+ * Study to which point error messages can be improved,+   now that there is a 'Source' carried through all 'Kind's or 'Type's,+   it should enable some nice reports.+   Still, a lot of work and testing remain to be done,+   and likely some ideas to find too…+ * Add more terms in <https://hackage.haskell.org/package/symantic-lib symantic-lib>.+ * Add more transformations.+ * Study how to integrate types into the module system.+ * Study where to put @INLINE@, @INLINEABLE@ or @SPECIALIZE@ pragmas.+ * Study how to support /rank-N polymorphic types/,+   special cases can likely use the /boxed polymorphism/ workaround,+   but even if GHC were supporting /impredicative types/,+   I'm currently clueless about how to do this.+extra-source-files:+extra-tmp-files:+-- homepage: +license: GPL-3+license-file: COPYING+maintainer: Julien Moutinho <julm+symantic@autogeree.net>+name: symantic+stability: experimental+synopsis: Library for Typed Tagless-Final Higher-Order Composable DSL+tested-with: GHC==8.0.2+-- PVP:  +-+------- breaking API changes+--       | | +----- non-breaking API additions+--       | | | +--- code changes with no API change+version: 6.0.0.20170623++Source-Repository head+  location: git://git.autogeree.net/symantic+  type:     git++Library+  default-extensions:+    DataKinds+    DefaultSignatures+    FlexibleContexts+    FlexibleInstances+    LambdaCase+    MultiParamTypeClasses+    NamedFieldPuns+    OverloadedStrings+    Rank2Types+    ScopedTypeVariables+    StandaloneDeriving+    TupleSections+    TypeApplications+    TypeFamilies+    TypeOperators+  ghc-options: -Wall+               -fno-warn-tabs+  default-language: Haskell2010+  exposed-modules:+    Language.Symantic+    Language.Symantic.Compiling+    Language.Symantic.Compiling.Beta+    Language.Symantic.Compiling.Grammar+    Language.Symantic.Compiling.Module+    Language.Symantic.Compiling.Read+    Language.Symantic.Compiling.Term+    Language.Symantic.Interpreting+    Language.Symantic.Interpreting.Dup+    Language.Symantic.Interpreting.Eval+    Language.Symantic.Interpreting.View+    Language.Symantic.Transforming+    Language.Symantic.Transforming.Beta+    Language.Symantic.Transforming.Trans+    Language.Symantic.Typing+    Language.Symantic.Typing.Document+    Language.Symantic.Typing.Grammar+    Language.Symantic.Typing.Kind+    Language.Symantic.Typing.List+    Language.Symantic.Typing.Peano+    Language.Symantic.Typing.Read+    Language.Symantic.Typing.Show+    Language.Symantic.Typing.Type+    Language.Symantic.Typing.Unify+    Language.Symantic.Typing.Variable+  build-depends:+    base >= 4.6 && < 5+    , containers+    , ghc-prim+    , mono-traversable+    , symantic-grammar+    , symantic-document+    , transformers+    , text