packages feed

symantic-lib (empty) → 0.0.2.20170623

raw patch · 52 files changed

+5366/−0 lines, 52 filesdep +basedep +containersdep +ghc-prim

Dependencies added: base, containers, ghc-prim, megaparsec, monad-classes, mono-traversable, symantic, symantic-grammar, symantic-lib, tasty, tasty-hunit, 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/Compiling/Test.hs view
@@ -0,0 +1,102 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Compiling.Test where++import Test.Tasty+import Test.Tasty.HUnit+import Debug.Trace (trace)++import Control.Arrow (left)+import Data.Functor.Identity (Identity(..))+import Data.Text (Text)+import Data.Type.Equality+import qualified Control.Monad.Classes.Run as MC+import qualified Control.Monad.Trans.State.Strict as SS+import qualified Data.List as List+import qualified Data.Text as Text+import qualified Text.Megaparsec as P++import Language.Symantic.Grammar+import Language.Symantic+import Language.Symantic.Lib ()++import Grammar.Megaparsec ()++test_parseTerm ::+ forall ss src.+ Inj_Modules src ss =>+ Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports, Modules src ss) Identity)) =>+ Text ->+ Either (P.ParseError Char P.Dec) (AST_Term src ss)+test_parseTerm inp =+	let mods :: Modules src ss = either (error . show) id inj_Modules in+	let imps = importQualifiedAs [] mods in+	runIdentity $+	MC.evalStateStrict (imps, mods) $+	P.runParserT g "" inp+	where g = unCF $ g_term <* eoi++test_readTerm ::+ forall src ss t.+ ( Eq t+ , Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports, Modules src ss) Identity))+ , Show t+ , Syms ss Eval+ , Syms ss View+ , Syms ss (BetaT View)+ , Inj_Modules src ss+ , Eq src+ , Show src+ , Inj_Source (TypeVT src) src+ , Inj_Source (TypeT src '[]) src+ , Inj_Source (KindK src) src+ , Inj_Source (AST_Type src) src+ , Inj_Name2Type ss+ ) =>+ Text ->+ Either ( Type src '[] t+        , Either (P.ParseError Char P.Dec)+                 (Error_Term src) )+        (Type src '[] t, t, Text) ->+ TestTree+test_readTerm inp expected =+	testCase (elide inp) $+	case reduceTeApp <$> test_parseTerm @ss inp of+	 Left err -> Left (Left err) @?= snd `left` expected+	 Right ast ->+		let tys = inj_Name2Type @ss in+		case readTerm tys CtxTyZ ast of+		 Left err -> Left (Right err) @?= snd `left` expected+		 Right term ->+			case term of+			 TermVT (Term q t (TeSym te)) ->+				case expected of+				 Left (_, err) -> Right ("…"::Text) @?= Left err+				 Right (ty_expected::Type src '[] t, _::t, _::Text) ->+					(>>= (@?= (\(_::Type src '[] t, err) -> err) `left` expected)) $+					case lenVars t of+					 LenS{} -> return $ Left $ Right $ Error_Term_polymorphic (TypeVT t)+					 LenZ ->+						case proveConstraint q of+						 Nothing -> return $ Left $ Right $ Error_Term_proofless $ TypeVT t+						 Just Dict ->+							case t `eqType` ty_expected of+							 Nothing -> return $ Left $ Right $+								Error_Term_Beta $ Error_Beta_Unify $+								Error_Unify_mismatch (TypeVT t) (TypeVT ty_expected)+							 Just Refl ->+								return $ Right (t, eval $ te CtxTeZ, view $ betaT $ te CtxTeZ)++maybeRight :: Either l r -> Maybe r+maybeRight (Right r) = Just r+maybeRight Left{}    = Nothing++elide :: Text -> String+elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']+elide s = Text.unpack s++dbg :: Show a => String -> a -> a+dbg msg x = trace (msg ++ " = " ++ Prelude.show x) x
+ Language/Symantic/Grammar/EBNF.hs view
@@ -0,0 +1,15 @@+module Grammar.EBNF where++import Data.Text.IO as Text+import Control.Monad++import Language.Symantic.Grammar+import Language.Symantic+import Language.Symantic.Lib ()++main :: IO ()+main = do+	forM_ gram_comment render+	forM_ gram_type render+	forM_ gram_term render+	where render = Text.putStrLn . renderEBNF . unCF
+ Language/Symantic/Grammar/Megaparsec.hs view
@@ -0,0 +1,155 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic instances for Megaparsec+module Grammar.Megaparsec where++import Control.Applicative (Applicative(..))+import Control.Monad (Monad(..))+import Data.Char (Char)+import Data.Either (Either(..))+import Data.Function (($), (.))+import Data.Functor (Functor(..), (<$>))+import Data.List.NonEmpty (NonEmpty(..))+import Data.Ord (Ord(..))+import Data.String (IsString(..))+import Data.Typeable ()+import Text.Show (Show(..))+import qualified Control.Applicative as Alt+import qualified Control.Monad.Classes as MC+import qualified Data.Char as Char+import qualified Data.Text as Text+import qualified Text.Megaparsec as P++import Language.Symantic.Grammar as Sym+import qualified Language.Symantic as Sym++--+-- Readers+--++-- NonEmpty P.SourcePos+instance ParsecC e s => Sym.Gram_Reader (NonEmpty P.SourcePos) (P.ParsecT e s m) where+	g_ask_before g = do+		s <- P.statePos <$> P.getParserState+		($ s) <$> g+	g_ask_after g = do+		f <- g+		f . P.statePos <$> P.getParserState+type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader (NonEmpty P.SourcePos)) = 'True+instance ParsecC e s => MC.MonadReaderN 'MC.Zero (NonEmpty P.SourcePos) (P.ParsecT e s m) where+	askN _n = P.statePos <$> P.getParserState+-- P.SourcePos+instance ParsecC e s => Sym.Gram_Reader P.SourcePos (P.ParsecT e s m) where+	g_ask_before g = do+		s <- P.getPosition+		($ s) <$> g+	g_ask_after g = do+		f <- g+		f <$> P.getPosition+type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader P.SourcePos) = 'True+instance ParsecC e s => MC.MonadReaderN 'MC.Zero P.SourcePos (P.ParsecT e s m) where+	askN _n = P.getPosition+-- ()+instance ParsecC e s => Sym.Gram_Reader () (P.ParsecT e s m) where+	g_ask_before = fmap ($ ())+	g_ask_after  = fmap ($ ())++--+-- States+--++-- st+type instance MC.CanDo (P.ParsecT e s m) (MC.EffState st) = 'False+instance (Monad m, MC.MonadState st m) => Sym.Gram_State st m where+	g_state_before g = do+		s <- MC.get+		f <- g+		let (s', a) = f s+		MC.put s'+		return a+	g_state_after g = do+		f <- g+		s <- MC.get+		let (s_, a) = f s+		MC.put s_+		return a+	g_get_before g = do+		s <- MC.get+		f <- g+		return (f s)+	g_get_after g = do+		f <- g+		s <- MC.get+		return (f s)+	g_put g = do+		(s, a) <- g+		MC.put s+		return a++-- * Type 'ParsecC'+-- | Convenient alias for defining instances involving 'P.ParsecT'.+type ParsecC e s = (P.Token s ~ Char, P.Stream s, P.ErrorComponent e)+instance ParsecC e s => IsString (P.ParsecT e s m [Char]) where+	fromString = P.string++--+-- Sym instances+--+instance (ParsecC e s, Show err) => Sym.Gram_Error err (P.ParsecT e s m) where+	g_catch me = do+		e <- me+		case e of+		 Left err -> fail $ show err+		 Right a -> return a+instance ParsecC e s => Sym.Gram_Rule (P.ParsecT e s m) where+	rule = P.label . Text.unpack+instance ParsecC e s => Sym.Gram_Terminal (P.ParsecT e s m) where+	any          = P.anyChar+	eoi          = P.eof+	char         = P.char+	string       = P.string+	unicat cat   = P.satisfy $ (`elem` cats) . Char.generalCategory+		where cats = unicode_categories cat+	range (l, h) = P.satisfy $ \c -> l <= c && c <= h+	Terminal f `but` Terminal p = Terminal $ P.notFollowedBy (P.try p) *> f+instance ParsecC e s => Sym.Gram_Alt (P.ParsecT e s m) where+	empty  = Alt.empty+	(<+>)  = (Alt.<|>)+	choice = P.choice+instance ParsecC e s => Sym.Gram_Try (P.ParsecT e s m) where+	try = P.try+instance ParsecC e s => Sym.Gram_RegR (P.ParsecT e s m) where+	Terminal f .*> Reg x = Reg $ f <*> x+instance ParsecC e s => Sym.Gram_RegL (P.ParsecT e s m) where+	Reg f <*. Terminal x = Reg $ f <*> x+instance ParsecC e s => Sym.Gram_App (P.ParsecT e s m) where+	between = P.between+instance ParsecC e s => Sym.Gram_AltApp (P.ParsecT e s m) where+	option   = P.option+	optional = P.optional+	many     = P.many+	some     = P.some+	skipMany = P.skipMany+instance ParsecC e s => Sym.Gram_CF (P.ParsecT e s m) where+	CF f <& Reg p        = CF $ P.lookAhead f <*> p+	Reg f &> CF p        = CF $ P.lookAhead f <*> p+	minus (CF f) (Reg p) = CF $ P.notFollowedBy (P.try p) *> f+instance ParsecC e s => Sym.Gram_Comment (P.ParsecT e s m)+instance ParsecC e s => Sym.Gram_Op (P.ParsecT e s m)+instance ParsecC e s => Sym.Gram_Name (P.ParsecT e s m)+instance -- Sym.Gram_Type+ ( ParsecC e s+ , Gram_Source src      (P.ParsecT e s m)+ ) => Sym.Gram_Type src (P.ParsecT e s m)+instance -- Sym.Gram_Term_Type+ ( ParsecC e s+ , Gram_Source src           (P.ParsecT e s m)+ ) => Sym.Gram_Term_Type src (P.ParsecT e s m)+instance -- Sym.Gram_Term+ ( ParsecC e s+ , Show src+ , MC.MonadState (Sym.Imports, Sym.Modules src ss) (P.ParsecT e s m)+ , Sym.Gram_Source src                             (P.ParsecT e s m)+ , Sym.Gram_Term_Atoms src ss                      (P.ParsecT e s m)+ ) => Sym.Gram_Term src ss                         (P.ParsecT e s m)
+ Language/Symantic/Lib.hs view
@@ -0,0 +1,142 @@+-- | Libraries.+module Language.Symantic.Lib+ ( -- module Language.Symantic.Lib+   module Language.Symantic.Lib.Alternative+ , module Language.Symantic.Lib.Applicative+ , module Language.Symantic.Lib.Bool+ , module Language.Symantic.Lib.Bounded+ , module Language.Symantic.Lib.Char+ -- , module Language.Symantic.Lib.Constraint+ , module Language.Symantic.Lib.Either+ , module Language.Symantic.Lib.Enum+ , module Language.Symantic.Lib.Eq+ , module Language.Symantic.Lib.Foldable+ , module Language.Symantic.Lib.Function+ , module Language.Symantic.Lib.Functor+ , module Language.Symantic.Lib.IO+ , module Language.Symantic.Lib.If+ , module Language.Symantic.Lib.Int+ , module Language.Symantic.Lib.Integer+ , module Language.Symantic.Lib.Integral+ , module Language.Symantic.Lib.List+ , module Language.Symantic.Lib.Map+ , module Language.Symantic.Lib.Maybe+ , module Language.Symantic.Lib.Monad+ , module Language.Symantic.Lib.MonoFoldable+ , module Language.Symantic.Lib.MonoFunctor+ , module Language.Symantic.Lib.Monoid+ , module Language.Symantic.Lib.NonNull+ , module Language.Symantic.Lib.Num+ , module Language.Symantic.Lib.Ord+ , module Language.Symantic.Lib.Ratio+ , module Language.Symantic.Lib.Real+ , module Language.Symantic.Lib.Semigroup+ , module Language.Symantic.Lib.Sequences+ , module Language.Symantic.Lib.Show+ , module Language.Symantic.Lib.Text+ , module Language.Symantic.Lib.Traversable+ , module Language.Symantic.Lib.Tuple2+ , module Language.Symantic.Lib.Unit+ ) where++import Language.Symantic.Lib.Alternative+import Language.Symantic.Lib.Applicative+import Language.Symantic.Lib.Bool+import Language.Symantic.Lib.Bounded+import Language.Symantic.Lib.Char+-- import Language.Symantic.Lib.Constraint+import Language.Symantic.Lib.Either+import Language.Symantic.Lib.Enum+import Language.Symantic.Lib.Eq+import Language.Symantic.Lib.Foldable+import Language.Symantic.Lib.Function+import Language.Symantic.Lib.Functor+import Language.Symantic.Lib.IO+import Language.Symantic.Lib.If+import Language.Symantic.Lib.Int+import Language.Symantic.Lib.Integer+import Language.Symantic.Lib.Integral+import Language.Symantic.Lib.List+import Language.Symantic.Lib.Map+import Language.Symantic.Lib.Maybe+import Language.Symantic.Lib.Monad+import Language.Symantic.Lib.MonoFoldable+import Language.Symantic.Lib.MonoFunctor+import Language.Symantic.Lib.Monoid+import Language.Symantic.Lib.NonNull+import Language.Symantic.Lib.Num+import Language.Symantic.Lib.Ord+import Language.Symantic.Lib.Ratio+import Language.Symantic.Lib.Real+import Language.Symantic.Lib.Semigroup+import Language.Symantic.Lib.Sequences+import Language.Symantic.Lib.Show+import Language.Symantic.Lib.Text+import Language.Symantic.Lib.Traversable+import Language.Symantic.Lib.Tuple2+import Language.Symantic.Lib.Unit++{-+import Data.Map.Strict (Map)+import Data.NonNull (NonNull)+import Data.Proxy (Proxy)+import Data.Ratio (Ratio)+import Data.Text (Text)+import System.IO as IO (IO, Handle, IOMode)+import qualified Data.MonoTraversable as MT+import qualified Data.Sequences as Seqs+import qualified Language.Symantic.Helper.Data.Type.List as Type+import Language.Symantic.Typing++-- * Type 'TyConstsLib'+-- | Usual 'TyConst's.+type TyConstsLib = TyConsts_Terms Type.++ TyConsts_Constraints++-- ** Type 'TyConsts_Terms'+-- | Usual 'TyConst's of /terms constructors/.+type TyConsts_Terms =+ [ Proxy ()+ , Proxy (,)+ , Proxy (->)+ , Proxy (#>)+ , Proxy (#)+ , Proxy []+ , Proxy Bool+ , Proxy Char+ , Proxy Either+ , Proxy Int+ , Proxy Integer+ , Proxy IO+ , Proxy IO.Handle+ , Proxy IO.IOMode+ , Proxy Ordering+ , Proxy Map+ , Proxy Maybe+ , Proxy NonNull+ , Proxy Ratio+ , Proxy Text+ ]++-- ** Type 'TyConsts_Constraints'+-- | Usual 'TyConst's of /type constraint constructors/.+type TyConsts_Constraints =+ [ Proxy Applicative+ , Proxy Bounded+ , Proxy Enum+ , Proxy Eq+ , Proxy Foldable+ , Proxy Functor+ , Proxy Integral+ , Proxy Monad+ , Proxy Monoid+ , Proxy MT.MonoFoldable+ , Proxy MT.MonoFunctor+ , Proxy Num+ , Proxy Ord+ , Proxy Real+ , Proxy Seqs.IsSequence+ , Proxy Seqs.SemiSequence+ , Proxy Show+ , Proxy Traversable+ ]+-}
+ Language/Symantic/Lib/Alternative.hs view
@@ -0,0 +1,63 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Alternative'.+module Language.Symantic.Lib.Alternative where++import Control.Applicative (Alternative)+import Prelude hiding (Functor(..), (<$>), id, const)+import qualified Control.Applicative as Alternative++import Language.Symantic+import Language.Symantic.Lib.Functor (Sym_Functor(..), f1)+import Language.Symantic.Lib.Function (a0)++-- * Class 'Sym_Alternative'+type instance Sym (Proxy Alternative) = Sym_Alternative+class Sym_Functor term => Sym_Alternative term where+	empty :: Alternative f => term (f a)+	(<|>) :: Alternative f => term (f a) -> term (f a) -> term (f a)+	infixl 3 <|>+	+	default empty :: Sym_Alternative (UnT term) => Trans term => Alternative f => term (f a)+	default (<|>) :: Sym_Alternative (UnT term) => Trans term => Alternative f => term (f a) -> term (f a) -> term (f a)+	+	empty = trans empty+	(<|>) = trans2 (<|>)++-- Interpreting+instance Sym_Alternative Eval where+	empty = Eval Alternative.empty+	(<|>) = eval2 (Alternative.<|>)+instance Sym_Alternative View where+	empty = view0 "empty"+	(<|>) = viewInfix "<|>" (infixL 3)+instance (Sym_Alternative r1, Sym_Alternative r2) => Sym_Alternative (Dup r1 r2) where+	empty = dup0 @Sym_Alternative empty+	(<|>) = dup2 @Sym_Alternative (<|>)++-- Transforming+instance (Sym_Lambda term, Sym_Alternative term) => Sym_Alternative (BetaT term)++-- Typing+instance FixityOf Alternative+instance ClassInstancesFor Alternative+instance TypeInstancesFor Alternative++-- Compiling+instance Gram_Term_AtomsFor src ss g Alternative+instance (Source src, Inj_Sym ss Alternative) => ModuleFor src ss Alternative where+	moduleFor = ["Alternative"] `moduleWhere`+	 [ "empty" := teAlternative_empty+	 , "<|>" `withInfixL` 3 := teAlternative_alt+	 ]++-- ** 'Type's+tyAlternative :: Source src => Type src vs a -> Type src vs (Alternative a)+tyAlternative a = tyConstLen @(K Alternative) @Alternative (lenVars a) `tyApp` a++-- ** 'Term's+teAlternative_empty :: TermDef Alternative '[Proxy a, Proxy f] (Alternative f #> f a)+teAlternative_empty = Term (tyAlternative f1) (f1 `tyApp` a0) $ teSym @Alternative $ empty++teAlternative_alt :: TermDef Alternative '[Proxy a, Proxy f] (Alternative f #> (f a -> f a -> f a))+teAlternative_alt = Term (tyAlternative f1) (f1 `tyApp` a0 ~> f1 `tyApp` a0 ~> f1 `tyApp` a0) $ teSym @Alternative $ lam2 (<|>)
+ Language/Symantic/Lib/Applicative.hs view
@@ -0,0 +1,80 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Applicative'.+module Language.Symantic.Lib.Applicative where++import Control.Applicative (Applicative)+import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)+import qualified Control.Applicative as Applicative+import qualified Data.Function as Fun++import Language.Symantic+import Language.Symantic.Lib.Function (a0, b1)+import Language.Symantic.Lib.Functor (Sym_Functor(..), (<$>), f1, f2)++-- * Class 'Sym_Applicative'+type instance Sym (Proxy Applicative) = Sym_Applicative+class Sym_Functor term => Sym_Applicative term where+	pure  :: Applicative f => term a -> term (f a)+	(<*>) :: Applicative f => term (f (a -> b)) -> term (f a) -> term (f b); infixl 4 <*>+	(*>)  :: Applicative f => term (f a) -> term (f b) -> term (f b); infixl 4 *>+	(<*)  :: Applicative f => term (f a) -> term (f b) -> term (f a); infixl 4 <*+	+	default pure  :: Sym_Applicative (UnT term) => Trans term => Applicative f => term a -> term (f a)+	default (<*>) :: Sym_Applicative (UnT term) => Trans term => Applicative f => term (f (a -> b)) -> term (f a) -> term (f b)+	default (*>)  :: Sym_Lambda term => Applicative f => term (f a) -> term (f b) -> term (f b)+	default (<*)  :: Sym_Lambda term => Applicative f => term (f a) -> term (f b) -> term (f a)+	+	pure   = trans1 pure+	(<*>)  = trans2 (<*>)+	x *> y = lam1 Fun.id    <$  x <*> y+	x <* y = lam2 Fun.const <$> x <*> y++-- Interpreting+instance Sym_Applicative Eval where+	pure  = eval1 Applicative.pure+	(<*>) = eval2 (Applicative.<*>)+instance Sym_Applicative View where+	pure  = view1 "pure"+	(<*>) = viewInfix "<*>" (infixL 4)+	(<* ) = viewInfix "<*"  (infixL 4)+	( *>) = viewInfix "*>"  (infixL 4)+instance (Sym_Applicative r1, Sym_Applicative r2, Sym_Lambda r1, Sym_Lambda r2) => Sym_Applicative (Dup r1 r2) where+	pure  = dup1 @Sym_Applicative pure+	(<*>) = dup2 @Sym_Applicative (<*>)++-- Transforming+instance (Sym_Lambda term, Sym_Applicative term) => Sym_Applicative (BetaT term) where+	(<*) = trans2 (<*)+	(*>) = trans2 (*>)++-- Typing+instance FixityOf Applicative+instance ClassInstancesFor Applicative+instance TypeInstancesFor Applicative++-- Compiling+instance Gram_Term_AtomsFor src ss g Applicative+instance (Source src, Inj_Sym ss Applicative) => ModuleFor src ss Applicative where+	moduleFor = ["Applicative"] `moduleWhere`+	 [ "<*>" `withInfixL` 4 := teApplicative_app+	 , "<*"  `withInfixL` 4 := teApplicative_const+	 , "*>"  `withInfixL` 4 := teApplicative_tsnoc+	 ]++-- ** 'Type's+tyApplicative :: Source src => Type src vs a -> Type src vs (Applicative a)+tyApplicative a = tyConstLen @(K Applicative) @Applicative (lenVars a) `tyApp` a++-- ** 'Term's+teApplicative_pure :: TermDef Applicative '[Proxy a, Proxy f] (Applicative f #> (a -> f a))+teApplicative_pure = Term (tyApplicative f1) (a0 ~> f1 `tyApp` a0) $ teSym @Applicative $ lam1 pure++teApplicative_app :: TermDef Applicative '[Proxy a, Proxy b, Proxy f] (Applicative f #> (f (a -> b) -> f a -> f b))+teApplicative_app = Term (tyApplicative f2) (f2 `tyApp` (a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Applicative $ lam2 (<*>)++teApplicative_const :: TermDef Applicative '[Proxy a, Proxy b1, Proxy f] (Applicative f #> (f a -> f b1 -> f a))+teApplicative_const = Term (tyApplicative f2) (f2 `tyApp` a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` a0) $ teSym @Applicative $ lam2 (<*)++teApplicative_tsnoc :: TermDef Applicative '[Proxy a, Proxy b, Proxy f] (Applicative f #> (f a -> f b -> f b))+teApplicative_tsnoc = Term (tyApplicative f2) (f2 `tyApp` a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` b1) $ teSym @Applicative $ lam2 (*>)
+ Language/Symantic/Lib/Applicative/Test.hs view
@@ -0,0 +1,30 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module Lib.Applicative.Test where++import Test.Tasty++import Data.Proxy (Proxy(..))+import Prelude hiding ((&&), not, (||))++import Language.Symantic.Lib+import Compiling.Test+import Lib.Bool.Test ()++type SS =+ [ Proxy (->)+ , Proxy Integer+ , Proxy Bool+ , Proxy Maybe+ , Proxy Functor+ , Proxy Applicative+ ]+(==>) = test_readTerm @() @SS++tests :: TestTree+tests = testGroup "Applicative"+ [ "Just (xor True) <*> Just True"    ==> Right (tyMaybe tyBool, Just False, "Just (\\x0 -> True `xor` x0) <*> Just True")+ , "Just (xor True) <*> Nothing"      ==> Right (tyMaybe tyBool, Nothing   , "Just (\\x0 -> True `xor` x0) <*> Nothing")+ , "xor <$> Just True <*> Just False" ==> Right (tyMaybe tyBool, Just True , "(\\x0 -> (\\x1 -> x0 `xor` x1)) <$> Just True <*> Just False")+ , "Just False <* Just True"          ==> Right (tyMaybe tyBool, Just False, "Just False <* Just True")+ , "Just False *> Just True"          ==> Right (tyMaybe tyBool, Just True , "Just False *> Just True")+ ]
+ Language/Symantic/Lib/Bool.hs view
@@ -0,0 +1,98 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Bool'.+module Language.Symantic.Lib.Bool where++import Control.Monad+import Data.Proxy+import Prelude hiding ((&&), not, (||))+import qualified Data.Bool as Bool+import qualified Data.Text as Text++import Language.Symantic+import Language.Symantic.Lib.Function ()++-- * Class 'Sym_Bool'+type instance Sym (Proxy Bool) = Sym_Bool+class Sym_Bool term where+	bool ::      Bool -> term Bool+	not  :: term Bool -> term Bool+	(&&) :: term Bool -> term Bool -> term Bool; infixr 3 &&+	(||) :: term Bool -> term Bool -> term Bool; infixr 2 ||+	xor  :: term Bool -> term Bool -> term Bool; infixr 2 `xor`+	xor x y = (x || y) && not (x && y)+	+	default bool :: Sym_Bool (UnT term) => Trans term =>      Bool -> term Bool+	default not  :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool+	default (&&) :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool -> term Bool+	default (||) :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool -> term Bool+	+	bool = trans . bool+	not  = trans1 not+	(&&) = trans2 (&&)+	(||) = trans2 (||)++-- Interpreting+instance Sym_Bool Eval where+	bool = Eval+	not  = liftM Bool.not+	(&&) = liftM2 (Bool.&&)+	(||) = liftM2 (Bool.||)+instance Sym_Bool View where+	bool o = View $ \_p _v -> Text.pack (show o)+	not    = view1 "not"+	(&&)   = viewInfix "&&"    (infixR 3)+	(||)   = viewInfix "||"    (infixR 2)+	xor    = viewInfix "`xor`" (infixR 2)+instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (Dup r1 r2) where+	bool b = bool b `Dup` bool b+	not    = dup1 @Sym_Bool not+	(&&)   = dup2 @Sym_Bool (&&)+	(||)   = dup2 @Sym_Bool (||)+	xor    = dup2 @Sym_Bool xor++-- Transforming+instance (Sym_Lambda term, Sym_Bool term) => Sym_Bool (BetaT term) where+	xor = trans2 xor++-- Typing+instance ClassInstancesFor Bool where+	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)+	 | Just HRefl <- proj_ConstKiTy @_ @Bool c+	 = case () of+		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict+		   | Just Refl <- proj_Const @Enum    q -> Just Dict+		   | Just Refl <- proj_Const @Eq      q -> Just Dict+		   | Just Refl <- proj_Const @Ord     q -> Just Dict+		   | Just Refl <- proj_Const @Show    q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor Bool++-- Compiling+instance Gram_Term_AtomsFor src ss g Bool+instance (Source src, Inj_Sym ss Bool) => ModuleFor src ss Bool where+	moduleFor = ["Bool"] `moduleWhere`+	 [ "False" := teBool False+	 , "True"  := teBool True+	 , "not"   := teBool_not+	 , "and" `withInfixR` 3 := teBool_and+	 , "or"  `withInfixR` 2 := teBool_or+	 , "xor" `withInfixR` 2 := teBool_xor+	 ]++-- ** 'Type's+tyBool :: Source src => Inj_Len vs => Type src vs Bool+tyBool = tyConst @(K Bool) @Bool++-- ** 'Term's+teBool :: Source src => Inj_Sym ss Bool => Bool -> Term src ss ts '[] (() #> Bool)+teBool b = Term noConstraint tyBool $ teSym @Bool $ bool b++teBool_not :: TermDef Bool '[] (() #> (Bool -> Bool))+teBool_not = Term noConstraint (tyBool ~> tyBool) $ teSym @Bool $ lam1 not++teBool_and, teBool_or, teBool_xor :: TermDef Bool '[] (() #> (Bool -> Bool -> Bool))+teBool_and = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 (&&)+teBool_or  = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 (||)+teBool_xor = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 xor
+ Language/Symantic/Lib/Bool/Test.hs view
@@ -0,0 +1,86 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module Lib.Bool.Test where++import Test.Tasty++import Data.Proxy (Proxy(..))+import Prelude hiding ((&&), not, (||))++import Language.Symantic+import Language.Symantic.Lib+-- import Language.Symantic.Lib.Lambda ((~>))+import Compiling.Test++type SS =+ [ Proxy Bool+ , Proxy (->)+ , Proxy Integer+ , Proxy []+ , Proxy Char+ ]+(==>) = test_readTerm @() @SS++tests :: TestTree+tests = testGroup "Bool" $+ [ "True"                           ==> Right (tyBool, True , "True")+ , "xor True True"                  ==> Right (tyBool, False, "True `xor` True")+ , "xor False True"                 ==> Right (tyBool, True , "False `xor` True")+ , "True `xor` True"                ==> Right (tyBool, False, "True `xor` True")+ , "(\\(xy:Bool) -> xy) True"       ==> Right (tyBool, True , "(\\x0 -> x0) True")+ , "(\\(False:Bool) -> False) True" ==> Right (tyBool, True , "(\\x0 -> x0) True")+ , "(\\(lett:Bool) -> lett) True"   ==> Right (tyBool, True , "(\\x0 -> x0) True")+ , "(\\(x:Bool) -> xor x x) True"   ==> Right (tyBool, False, "(\\x0 -> x0 `xor` x0) True")+ , "let x = True in xor x True"     ==> Right (tyBool, False, "let x0 = True in x0 `xor` True")+ , "(\\(False:Bool) -> False) (False `xor` True)" ==> Right (tyBool, True, "(\\x0 -> x0) (False `xor` True)")+ , testGroup "Error_Term"+	 [ "True True" ==> Left (tyBool,+		Right $ Error_Term_Beta $+		Error_Beta_Term_not_a_function $+		TypeVT $ tyBool @_ @'[])+	 , "x" ==> Left (tyBool,+		Right $ Error_Term_unknown $ NameTe "x")+	 , "x `xor` True" ==> Left (tyBool,+		Right $ Error_Term_unknown $ NameTe "x")+	 , "(\\(x:Bool) -> x `xor` True) Bool" ==> Left (tyBool,+		Right $ Error_Term_unknown $ NameTe "Bool")+	 , "(\\(x:Bool) -> x) True True" ==> Left (tyBool,+		Right $ Error_Term_Beta $+		Error_Beta_Term_not_a_function $+		TypeVT $ tyBool @_ @'[])+	 , "(\\(x:Bool -> Bool) -> x True) True" ==> Left (tyBool,+		Right $ Error_Term_Beta $ Error_Beta_Unify $+		Error_Unify_Const_mismatch+		 (TypeVT $ tyFun @_ @'[])+		 (TypeVT $ tyBool @_ @'[]))+	 ]+ ]++-- * Class 'Sym_Bool_Vars'+-- | A few boolean variables.+class Sym_Bool_Vars repr where+	x :: repr Bool+	y :: repr Bool+	z :: repr Bool+instance Sym_Bool_Vars View where+	x = View $ \_p _v -> "x"+	y = View $ \_p _v -> "y"+	z = View $ \_p _v -> "z"+{-+instance -- Trans_Boo_Const+ ( Sym_Bool repr+ , Sym_Bool_Vars repr+ ) => Sym_Bool_Vars (Trans_Bool_Const repr) where+	x = trans_lift x+	y = trans_lift y+	z = trans_lift z+-}++-- * EDSL tests+te1 = bool True && bool False+te2 = (bool True && bool False) ||  (bool True && bool True)+te3 = (bool True ||  bool False) && (bool True ||  bool True)+te4 = bool True && not (bool False)+te5 = bool True && not x+te6 = x `xor` y+te7 = (x `xor` y) `xor` z+te8 = x `xor` (y `xor` bool True)
+ Language/Symantic/Lib/Bounded.hs view
@@ -0,0 +1,57 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Bounded'.+module Language.Symantic.Lib.Bounded where++import Prelude (Bounded)+import Prelude hiding (Bounded(..))+import qualified Prelude as Bounded++import Language.Symantic+import Language.Symantic.Lib.Function (a0)++-- * Class 'Sym_Bounded'+type instance Sym (Proxy Bounded) = Sym_Bounded+class Sym_Bounded term where+	minBound :: Bounded a => term a+	maxBound :: Bounded a => term a+	default minBound :: Sym_Bounded (UnT term) => Trans term => Bounded a => term a+	default maxBound :: Sym_Bounded (UnT term) => Trans term => Bounded a => term a+	minBound = trans minBound+	maxBound = trans maxBound++-- Interpreting+instance Sym_Bounded Eval where+	minBound = Eval Bounded.minBound+	maxBound = Eval Bounded.maxBound+instance Sym_Bounded View where+	minBound = view0 "minBound"+	maxBound = view0 "maxBound"+instance (Sym_Bounded r1, Sym_Bounded r2) => Sym_Bounded (Dup r1 r2) where+	minBound = dup0 @Sym_Bounded minBound+	maxBound = dup0 @Sym_Bounded maxBound++-- Transforming+instance (Sym_Lambda term, Sym_Bounded term) => Sym_Bounded (BetaT term)++-- Typing+instance FixityOf Bounded+instance ClassInstancesFor Bounded+instance TypeInstancesFor Bounded++-- Compiling+instance Gram_Term_AtomsFor src ss g Bounded+instance (Source src, Inj_Sym ss Bounded) => ModuleFor src ss Bounded where+	moduleFor = ["Bounded"] `moduleWhere`+	 [ "minBound" := teBounded_minBound+	 , "maxBound" := teBounded_maxBound+	 ]++-- ** 'Type's+tyBounded :: Source src => Type src vs a -> Type src vs (Bounded a)+tyBounded a = tyConstLen @(K Bounded) @Bounded (lenVars a) `tyApp` a++-- ** 'Term's+teBounded_minBound, teBounded_maxBound :: TermDef Bounded '[Proxy a] (Bounded a #> a)+teBounded_minBound = Term (tyBounded a0) a0 $ teSym @Bounded $ minBound+teBounded_maxBound = Term (tyBounded a0) a0 $ teSym @Bounded $ maxBound
+ Language/Symantic/Lib/Char.hs view
@@ -0,0 +1,100 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Char'.+module Language.Symantic.Lib.Char where++import qualified Data.Char as Char+import qualified Data.Text as Text++import Language.Symantic.Grammar hiding (char, any)+import qualified Language.Symantic.Grammar as Gram+import Language.Symantic+import Language.Symantic.Lib.List (tyList)++-- * Class 'Sym_Char'+type instance Sym (Proxy Char) = Sym_Char+class Sym_Char term where+	char :: Char -> term Char+	char_toUpper :: term Char -> term Char+	char_toLower :: term Char -> term Char+	+	default char         :: Sym_Char (UnT term) => Trans term => Char -> term Char+	default char_toUpper :: Sym_Char (UnT term) => Trans term => term Char -> term Char+	default char_toLower :: Sym_Char (UnT term) => Trans term => term Char -> term Char+	+	char         = trans . char+	char_toUpper = trans1 char_toUpper+	char_toLower = trans1 char_toLower++-- Interpreting+instance Sym_Char Eval where+	char         = Eval+	char_toUpper = eval1 Char.toUpper+	char_toLower = eval1 Char.toLower+instance Sym_Char View where+	char a = View $ \_p _v ->+		Text.pack (show a)+	char_toUpper = view1 "Char.toUpper"+	char_toLower = view1 "Char.toLower"+instance (Sym_Char r1, Sym_Char r2) => Sym_Char (Dup r1 r2) where+	char x       = char x `Dup` char x+	char_toUpper = dup1 @Sym_Char char_toUpper+	char_toLower = dup1 @Sym_Char char_toLower++-- Transforming+instance (Sym_Char term, Sym_Lambda term) => Sym_Char (BetaT term)++-- Typing+instance ClassInstancesFor Char where+	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)+	 | Just HRefl <- proj_ConstKiTy @_ @Char z+	 = case () of+		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict+		   | Just Refl <- proj_Const @Enum    q -> Just Dict+		   | Just Refl <- proj_Const @Eq      q -> Just Dict+		   | Just Refl <- proj_Const @Ord     q -> Just Dict+		   | Just Refl <- proj_Const @Show    q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor Char++-- Compiling+instance+ ( Gram_Source src g+ , Gram_Alt g+ , Gram_Rule g+ , Gram_Comment g+ , Inj_Sym ss Char+ ) => Gram_Term_AtomsFor src ss g Char where+	g_term_atomsFor =+	 [ rule "teChar" $+		lexeme $ g_source $+		(\c src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teChar c)+		 <$> between tickG tickG (+			cf_of_Terminal (Gram.any `but` tickG) <+>+			'\'' <$ string "\\'"+		 )+	 ]+		where+		tickG :: Gram_Terminal g' => g' Char+		tickG = Gram.char '\''+instance (Source src, Inj_Sym ss Char) => ModuleFor src ss Char where+	moduleFor = ["Char"] `moduleWhere`+	 [ "toLower" := teChar_toLower+	 , "toUpper" := teChar_toUpper+	 ]++-- ** 'Type's+tyChar :: Source src => Inj_Len vs => Type src vs Char+tyChar = tyConst @(K Char) @Char++tyString :: Source src => Inj_Len vs => Type src vs String+tyString = tyList tyChar++-- ** 'Term's+teChar :: Source src => Inj_Sym ss Char => Char -> Term src ss ts '[] (() #> Char)+teChar b = Term noConstraint tyChar $ teSym @Char $ char b++teChar_toUpper, teChar_toLower :: TermDef Char '[] (() #> (Char -> Char))+teChar_toUpper = Term noConstraint (tyChar ~> tyChar) $ teSym @Char $ lam1 char_toUpper+teChar_toLower = Term noConstraint (tyChar ~> tyChar) $ teSym @Char $ lam1 char_toLower
+ Language/Symantic/Lib/Either.hs view
@@ -0,0 +1,100 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Either'.+module Language.Symantic.Lib.Either where++import Prelude hiding (either)+import qualified Data.Either as Either+import qualified Data.MonoTraversable as MT++import Language.Symantic+import Language.Symantic.Lib.MonoFunctor (Element)+import Language.Symantic.Lib.Function (a0, b1, c2)++-- * Class 'Sym_Either'+type instance Sym (Proxy Either) = Sym_Either+class Sym_Either term where+	_Left  :: term l -> term (Either l r)+	_Right :: term r -> term (Either l r)+	either :: term (l -> a) -> term (r -> a) -> term (Either l r) -> term a+	+	default _Left  :: Sym_Either (UnT term) => Trans term => term l -> term (Either l r)+	default _Right :: Sym_Either (UnT term) => Trans term => term r -> term (Either l r)+	default either :: Sym_Either (UnT term) => Trans term => term (l -> a) -> term (r -> a) -> term (Either l r) -> term a+	+	_Left  = trans1 _Left+	_Right = trans1 _Right+	either = trans3 either++-- Interpreting+instance Sym_Either Eval where+	_Right = eval1 Right+	_Left  = eval1 Left+	either = eval3 Either.either+instance Sym_Either View where+	_Right = view1 "Right"+	_Left  = view1 "Left"+	either = view3 "either"+instance (Sym_Either r1, Sym_Either r2) => Sym_Either (Dup r1 r2) where+	_Left  = dup1 @Sym_Either _Left+	_Right = dup1 @Sym_Either _Right+	either = dup3 @Sym_Either either++-- Transforming+instance (Sym_Either term, Sym_Lambda term) => Sym_Either (BetaT term)++-- Typing+instance FixityOf Either+instance ClassInstancesFor Either where+	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _l))+	 | Just HRefl <- proj_ConstKiTy @_ @Either c+	 = case () of+		 _ | Just Refl <- proj_Const @Functor     q -> Just Dict+		   | Just Refl <- proj_Const @Applicative q -> Just Dict+		   | Just Refl <- proj_Const @Monad       q -> Just Dict+		   | Just Refl <- proj_Const @Foldable    q -> Just Dict+		   | Just Refl <- proj_Const @Traversable q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c l) r))+	 | Just HRefl <- proj_ConstKiTy @_ @Either c+	 = case () of+		 _ | Just Refl <- proj_Const @Eq q+		   , Just Dict <- proveConstraint (tq `tyApp` l)+		   , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict+		   | Just Refl <- proj_Const @Ord q+		   , Just Dict <- proveConstraint (tq `tyApp` l)+		   , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict+		   | Just Refl <- proj_Const @Show q+		   , Just Dict <- proveConstraint (tq `tyApp` l)+		   , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFunctor  q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor Either where+	expandFamFor _c _len f (TyApp _ (TyApp _ c _ty_l) r `TypesS` TypesZ)+	 | Just HRefl <- proj_ConstKi @_ @Element f+	 , Just HRefl <- proj_ConstKiTy @_ @Either c+	 = Just r+	expandFamFor _c _len _fam _as = Nothing++-- Compiling+instance Gram_Term_AtomsFor src ss g Either+instance (Source src, Inj_Sym ss Either) => ModuleFor src ss Either where+	moduleFor = ["Either"] `moduleWhere`+	 [ "Left"   := teEither_Left+	 , "Right"  := teEither_Right+	 , "either" := teEither_either+	 ]++-- ** 'Type's+tyEither :: Source src => Type src vs l -> Type src vs r -> Type src vs (Either l r)+tyEither l r = tyConstLen @(K Either) @Either (lenVars l) `tyApp` l `tyApp` r++-- ** 'Term's+teEither_Left :: TermDef Either '[Proxy a, Proxy b] (() #> (a -> Either a b))+teEither_Left = Term noConstraint (a0 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Left+teEither_Right :: TermDef Either '[Proxy a, Proxy b] (() #> (b -> Either a b))+teEither_Right = Term noConstraint (b1 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Right+teEither_either :: TermDef Either '[Proxy a, Proxy b, Proxy c] (() #> ((a -> c) -> (b -> c) -> Either a b -> c))+teEither_either = Term noConstraint ((a0 ~> c2) ~> (b1 ~> c2) ~> tyEither a0 b1 ~> c2) $ teSym @Either $ lam3 either
+ Language/Symantic/Lib/Enum.hs view
@@ -0,0 +1,80 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Enum'.+module Language.Symantic.Lib.Enum where++import Prelude (Enum)+import Prelude hiding (Enum(..))+import qualified Prelude++import Language.Symantic+import Language.Symantic.Lib.Function (a0)+import Language.Symantic.Lib.Int (tyInt)++-- * Class 'Sym_Enum'+type instance Sym (Proxy Enum) = Sym_Enum+class Sym_Enum term where+	toEnum   :: Enum a => term Int -> term a+	fromEnum :: Enum a => term a -> term Int+	succ     :: Enum a => term a -> term a+	pred     :: Enum a => term a -> term a+	+	default succ     :: Sym_Enum (UnT term) => Trans term => Enum a => term a -> term a+	default pred     :: Sym_Enum (UnT term) => Trans term => Enum a => term a -> term a+	default toEnum   :: Sym_Enum (UnT term) => Trans term => Enum a => term Int -> term a+	default fromEnum :: Sym_Enum (UnT term) => Trans term => Enum a => term a -> term Int+	+	toEnum   = trans1 toEnum+	fromEnum = trans1 fromEnum+	succ     = trans1 succ+	pred     = trans1 pred++-- Interpreting+instance Sym_Enum Eval where+	toEnum   = eval1 Prelude.toEnum+	fromEnum = eval1 Prelude.fromEnum+	succ     = eval1 Prelude.succ+	pred     = eval1 Prelude.pred+instance Sym_Enum View where+	toEnum   = view1 "toEnum"+	fromEnum = view1 "fromEnum"+	succ     = view1 "succ"+	pred     = view1 "pred"+instance (Sym_Enum r1, Sym_Enum r2) => Sym_Enum (Dup r1 r2) where+	toEnum   = dup1 @Sym_Enum toEnum+	fromEnum = dup1 @Sym_Enum fromEnum+	succ     = dup1 @Sym_Enum succ+	pred     = dup1 @Sym_Enum pred++-- Transforming+instance (Sym_Enum term, Sym_Lambda term) => Sym_Enum (BetaT term)++-- Typing+instance FixityOf Enum+instance ClassInstancesFor Enum+instance TypeInstancesFor Enum++-- Compiling+instance Gram_Term_AtomsFor src ss g Enum+instance (Source src, Inj_Sym ss Enum) => ModuleFor src ss Enum where+	moduleFor = ["Enum"] `moduleWhere`+	 [ "succ"     := teEnum_succ+	 , "pred"     := teEnum_pred+	 , "toEnum"   := teEnum_toEnum+	 , "fromEnum" := teEnum_fromEnum+	 ]++-- ** 'Type's+tyEnum :: Source src => Type src vs a -> Type src vs (Enum a)+tyEnum a = tyConstLen @(K Enum) @Enum (lenVars a) `tyApp` a++-- ** 'Term's+teEnum_toEnum :: TermDef Enum '[Proxy a] (Enum a #> (Int -> a))+teEnum_toEnum = Term (tyEnum a0) (tyInt ~> a0) $ teSym @Enum $ lam1 toEnum++teEnum_fromEnum :: TermDef Enum '[Proxy a] (Enum a #> (a -> Int))+teEnum_fromEnum = Term (tyEnum a0) (a0 ~> tyInt) $ teSym @Enum $ lam1 fromEnum++teEnum_succ, teEnum_pred :: TermDef Enum '[Proxy a] (Enum a #> (a -> a))+teEnum_succ = Term (tyEnum a0) (a0 ~> a0) $ teSym @Enum $ lam1 succ+teEnum_pred = Term (tyEnum a0) (a0 ~> a0) $ teSym @Enum $ lam1 pred
+ Language/Symantic/Lib/Eq.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Eq'.+module Language.Symantic.Lib.Eq where++import Prelude hiding ((==), (/=))+import qualified Data.Eq as Eq++import Language.Symantic+import Language.Symantic.Lib.Bool (tyBool)+import Language.Symantic.Lib.Function (a0)++-- * Class 'Sym_Eq'+type instance Sym (Proxy Eq) = Sym_Eq+class Sym_Eq term where+	(==) :: Eq a => term a -> term a -> term Bool; infix 4 ==+	(/=) :: Eq a => term a -> term a -> term Bool; infix 4 /=+	+	default (==) :: Sym_Eq (UnT term) => Trans term => Eq a => term a -> term a -> term Bool+	default (/=) :: Sym_Eq (UnT term) => Trans term => Eq a => term a -> term a -> term Bool+	+	(==) = trans2 (==)+	(/=) = trans2 (/=)++-- Interpreting+instance Sym_Eq Eval where+	(==) = eval2 (Eq.==)+	(/=) = eval2 (Eq./=)+instance Sym_Eq View where+	(==) = viewInfix "==" (infixN 4)+	(/=) = viewInfix "/=" (infixN 4)+instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (Dup r1 r2) where+	(==) = dup2 @Sym_Eq (==)+	(/=) = dup2 @Sym_Eq (/=)++-- Transforming+instance (Sym_Eq term, Sym_Lambda term) => Sym_Eq (BetaT term)++-- Typing+instance FixityOf Eq+instance ClassInstancesFor Eq+instance TypeInstancesFor Eq++-- Compiling+instance Gram_Term_AtomsFor src ss g Eq+instance (Source src, Inj_Sym ss Eq) => ModuleFor src ss Eq where+	moduleFor = ["Eq"] `moduleWhere`+	 [ "==" `withInfixN` 4 := teEq_eq+	 , "/=" `withInfixN` 4 := teEq_ne+	 ]++-- ** 'Type's+tyEq :: Source src => Type src vs a -> Type src vs (Eq a)+tyEq a = tyConstLen @(K Eq) @Eq (lenVars a) `tyApp` a++-- ** 'Term's+teEq_eq, teEq_ne :: TermDef Eq '[Proxy a] (Eq a #> (a -> a -> Bool))+teEq_eq = Term (tyEq a0) (a0 ~> a0 ~> tyBool) $ teSym @Eq $ lam2 (==)+teEq_ne = Term (tyEq a0) (a0 ~> a0 ~> tyBool) $ teSym @Eq $ lam2 (/=)
+ Language/Symantic/Lib/Foldable.hs view
@@ -0,0 +1,338 @@+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Foldable'.+module Language.Symantic.Lib.Foldable where++import Control.Applicative (Alternative)+import Control.Monad (MonadPlus)+import Data.Foldable (Foldable)+import qualified Data.Foldable as Foldable+import Prelude hiding (Foldable(..)+ , all, and, any, concat, concatMap+ , mapM_, notElem, or, sequence, sequence_)++import Language.Symantic+import Language.Symantic.Lib.Alternative (tyAlternative)+import Language.Symantic.Lib.Bool (tyBool)+import Language.Symantic.Lib.Eq (tyEq)+import Language.Symantic.Lib.Function (a0, b1)+import Language.Symantic.Lib.Functor (f2)+import Language.Symantic.Lib.Int (tyInt)+import Language.Symantic.Lib.List (tyList)+import Language.Symantic.Lib.Monoid (tyMonoid)+import Language.Symantic.Lib.Num (tyNum)+import Language.Symantic.Lib.Ord (tyOrd)++-- * Class 'Sym_Foldable'+type instance Sym (Proxy Foldable) = Sym_Foldable+class Sym_Foldable term where+	foldMap    :: Foldable f => Monoid m      => term (a -> m) -> term (f a) -> term m+	foldr      :: Foldable f                  => term (a -> b -> b) -> term b -> term (f a) -> term b+	foldr'     :: Foldable f                  => term (a -> b -> b) -> term b -> term (f a) -> term b+	foldl      :: Foldable f                  => term (b -> a -> b) -> term b -> term (f a) -> term b+	foldl'     :: Foldable f                  => term (b -> a -> b) -> term b -> term (f a) -> term b+	length     :: Foldable f                  => term (f a) -> term Int+	null       :: Foldable f                  => term (f a) -> term Bool+	minimum    :: Foldable f => Ord a         => term (f a) -> term a+	maximum    :: Foldable f => Ord a         => term (f a) -> term a+	elem       :: Foldable f => Eq  a         => term a -> term (f a) -> term Bool; infix 4 `elem`+	sum        :: Foldable f => Num a         => term (f a) -> term a+	product    :: Foldable f => Num a         => term (f a) -> term a+	toList     :: Foldable f                  => term (f a) -> term [a]+	all        :: Foldable f                  => term (a -> Bool) -> term (f a) -> term Bool+	and        :: Foldable f                  => term (f Bool) -> term Bool+	any        :: Foldable f                  => term (a -> Bool) -> term (f a) -> term Bool+	concat     :: Foldable f                  => term (f [a]) -> term [a]+	concatMap  :: Foldable f                  => term (a -> [b]) -> term (f a) -> term [b]+	find       :: Foldable f                  => term (a -> Bool) -> term (f a) -> term (Maybe a)+	foldlM     :: Foldable f => Monad m       => term (b -> a -> m b) -> term b -> term (f a) -> term (m b)+	foldrM     :: Foldable f => Monad m       => term (a -> b -> m b) -> term b -> term (f a) -> term (m b)+	forM_      :: Foldable f => Monad m       => term (f a) -> term (a -> m b) -> term (m ())+	for_       :: Foldable f => Applicative p => term (f a) -> term (a -> p b) -> term (p ())+	mapM_      :: Foldable f => Monad m       => term (a -> m b) -> term (f a) -> term (m ())+	maximumBy  :: Foldable f                  => term (a -> a -> Ordering) -> term (f a) -> term a+	minimumBy  :: Foldable f                  => term (a -> a -> Ordering) -> term (f a) -> term a+	notElem    :: Foldable f => Eq a          => term a -> term (f a) -> term Bool+	or         :: Foldable f                  => term (f Bool) -> term Bool+	sequenceA_ :: Foldable f => Applicative p => term (f (p a)) -> term (p ())+	sequence_  :: Foldable f => Monad m       => term (f (m a)) -> term (m ())+	traverse_  :: Foldable f => Applicative p => term (a -> p b) -> term (f a) -> term (p ())+	asum       :: Foldable f => Alternative p => term (f (p a)) -> term (p a)+	msum       :: Foldable f => MonadPlus p   => term (f (p a)) -> term (p a)+	+	default foldMap    :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monoid m       => term (a -> m) -> term (f a) -> term m+	default foldr      :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> b -> b) -> term b -> term (f a) -> term b+	default foldr'     :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> b -> b) -> term b -> term (f a) -> term b+	default foldl      :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (b -> a -> b) -> term b -> term (f a) -> term b+	default foldl'     :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (b -> a -> b) -> term b -> term (f a) -> term b+	default length     :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (f a) -> term Int+	default null       :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (f a) -> term Bool+	default minimum    :: Sym_Foldable (UnT term) => Trans term => Foldable f => Ord a          => term (f a) -> term a+	default maximum    :: Sym_Foldable (UnT term) => Trans term => Foldable f => Ord a          => term (f a) -> term a+	default elem       :: Sym_Foldable (UnT term) => Trans term => Foldable f => Eq  a          => term a -> term (f a) -> term Bool+	default sum        :: Sym_Foldable (UnT term) => Trans term => Foldable f => Num a          => term (f a) -> term a+	default product    :: Sym_Foldable (UnT term) => Trans term => Foldable f => Num a          => term (f a) -> term a+	default toList     :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (f a) -> term [a]+	default all        :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> Bool) -> term (f a) -> term Bool+	default and        :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (f Bool) -> term Bool+	default any        :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> Bool) -> term (f a) -> term Bool+	default concat     :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (f [a]) -> term [a]+	default concatMap  :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> [b]) -> term (f a) -> term [b]+	default find       :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> Bool) -> term (f a) -> term (Maybe a)+	default foldlM     :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m        => term (b -> a -> m b) -> term b -> term (f a) -> term (m b)+	default foldrM     :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m        => term (a -> b -> m b) -> term b -> term (f a) -> term (m b)+	default forM_      :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m        => term (f a) -> term (a -> m b) -> term (m ())+	default for_       :: Sym_Foldable (UnT term) => Trans term => Foldable f => Applicative p  => term (f a) -> term (a -> p b) -> term (p ())+	default mapM_      :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m        => term (a -> m b) -> term (f a) -> term (m ())+	default maximumBy  :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> a -> Ordering) -> term (f a) -> term a+	default minimumBy  :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> a -> Ordering) -> term (f a) -> term a+	default notElem    :: Sym_Foldable (UnT term) => Trans term => Foldable f => Eq a           => term a -> term (f a) -> term Bool+	default or         :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (f Bool) -> term Bool+	default sequenceA_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Applicative p  => term (f (p a)) -> term (p ())+	default sequence_  :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m        => term (f (m a)) -> term (m ())+	default traverse_  :: Sym_Foldable (UnT term) => Trans term => Foldable f => Applicative p  => term (a -> p b) -> term (f a) -> term (p ())+	default asum       :: Sym_Foldable (UnT term) => Trans term => Foldable f => Alternative m  => term (f (m a)) -> term (m a)+	default msum       :: Sym_Foldable (UnT term) => Trans term => Foldable f => MonadPlus m    => term (f (m a)) -> term (m a)+	+	foldMap    = trans2 foldMap+	foldr      = trans3 foldr+	foldr'     = trans3 foldr'+	foldl      = trans3 foldl+	foldl'     = trans3 foldl'+	length     = trans1 length+	null       = trans1 null+	minimum    = trans1 minimum+	maximum    = trans1 maximum+	elem       = trans2 elem+	sum        = trans1 sum+	product    = trans1 product+	toList     = trans1 toList+	all        = trans2 all+	and        = trans1 and+	any        = trans2 any+	concat     = trans1 concat+	concatMap  = trans2 concatMap+	find       = trans2 find+	foldlM     = trans3 foldlM+	foldrM     = trans3 foldrM+	forM_      = trans2 forM_+	for_       = trans2 for_+	mapM_      = trans2 mapM_+	maximumBy  = trans2 maximumBy+	minimumBy  = trans2 minimumBy+	notElem    = trans2 notElem+	or         = trans1 or+	sequenceA_ = trans1 sequenceA_+	sequence_  = trans1 sequence_+	traverse_  = trans2 traverse_+	asum       = trans1 asum+	msum       = trans1 msum++-- Interpreting+instance Sym_Foldable Eval where+	foldMap    = eval2 Foldable.foldMap+	foldr      = eval3 Foldable.foldr+	foldr'     = eval3 Foldable.foldr'+	foldl      = eval3 Foldable.foldl+	foldl'     = eval3 Foldable.foldl'+	null       = eval1 Foldable.null+	length     = eval1 Foldable.length+	minimum    = eval1 Foldable.minimum+	maximum    = eval1 Foldable.maximum+	elem       = eval2 Foldable.elem+	sum        = eval1 Foldable.sum+	product    = eval1 Foldable.product+	toList     = eval1 Foldable.toList+	all        = eval2 Foldable.all+	and        = eval1 Foldable.and+	any        = eval2 Foldable.any+	concat     = eval1 Foldable.concat+	concatMap  = eval2 Foldable.concatMap+	find       = eval2 Foldable.find+	foldlM     = eval3 Foldable.foldlM+	foldrM     = eval3 Foldable.foldrM+	forM_      = eval2 Foldable.forM_+	for_       = eval2 Foldable.for_+	mapM_      = eval2 Foldable.mapM_+	maximumBy  = eval2 Foldable.maximumBy+	minimumBy  = eval2 Foldable.minimumBy+	notElem    = eval2 Foldable.notElem+	or         = eval1 Foldable.or+	sequenceA_ = eval1 Foldable.sequenceA_+	sequence_  = eval1 Foldable.sequence_+	traverse_  = eval2 Foldable.traverse_+	asum       = eval1 Foldable.asum+	msum       = eval1 Foldable.msum+instance Sym_Foldable View where+	foldMap    = view2 "foldMap"+	foldr      = view3 "foldr"+	foldr'     = view3 "foldr'"+	foldl      = view3 "foldl"+	foldl'     = view3 "foldl'"+	null       = view1 "null"+	length     = view1 "length"+	minimum    = view1 "minimum"+	maximum    = view1 "maximum"+	elem       = view2 "elem"+	sum        = view1 "sum"+	product    = view1 "product"+	toList     = view1 "toList"+	all        = view2 "all"+	and        = view1 "and"+	any        = view2 "any"+	concat     = view1 "concat"+	concatMap  = view2 "concatMap"+	find       = view2 "find"+	foldlM     = view3 "foldlM"+	foldrM     = view3 "foldrM"+	forM_      = view2 "forM_"+	for_       = view2 "for_"+	mapM_      = view2 "mapM_"+	maximumBy  = view2 "maximumBy"+	minimumBy  = view2 "minimumBy"+	notElem    = view2 "notElem"+	or         = view1 "or"+	sequenceA_ = view1 "sequenceA_"+	sequence_  = view1 "sequence_"+	traverse_  = view2 "traverse_"+	asum       = view1 "asum"+	msum       = view1 "msum"+instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (Dup r1 r2) where+	foldMap    = dup2 @Sym_Foldable foldMap+	foldr      = dup3 @Sym_Foldable foldr+	foldr'     = dup3 @Sym_Foldable foldr'+	foldl      = dup3 @Sym_Foldable foldl+	foldl'     = dup3 @Sym_Foldable foldl'+	null       = dup1 @Sym_Foldable null+	length     = dup1 @Sym_Foldable length+	minimum    = dup1 @Sym_Foldable minimum+	maximum    = dup1 @Sym_Foldable maximum+	elem       = dup2 @Sym_Foldable elem+	sum        = dup1 @Sym_Foldable sum+	product    = dup1 @Sym_Foldable product+	toList     = dup1 @Sym_Foldable toList+	all        = dup2 @Sym_Foldable all+	and        = dup1 @Sym_Foldable and+	any        = dup2 @Sym_Foldable any+	concat     = dup1 @Sym_Foldable concat+	concatMap  = dup2 @Sym_Foldable concatMap+	find       = dup2 @Sym_Foldable find+	foldlM     = dup3 @Sym_Foldable foldlM+	foldrM     = dup3 @Sym_Foldable foldrM+	forM_      = dup2 @Sym_Foldable forM_+	for_       = dup2 @Sym_Foldable for_+	mapM_      = dup2 @Sym_Foldable mapM_+	maximumBy  = dup2 @Sym_Foldable maximumBy+	minimumBy  = dup2 @Sym_Foldable minimumBy+	notElem    = dup2 @Sym_Foldable notElem+	or         = dup1 @Sym_Foldable or+	sequenceA_ = dup1 @Sym_Foldable sequenceA_+	sequence_  = dup1 @Sym_Foldable sequence_+	traverse_  = dup2 @Sym_Foldable traverse_+	asum       = dup1 @Sym_Foldable asum+	msum       = dup1 @Sym_Foldable msum++-- Transforming+instance (Sym_Foldable term, Sym_Lambda term) => Sym_Foldable (BetaT term)++-- Typing+instance FixityOf Foldable+instance ClassInstancesFor Foldable+instance TypeInstancesFor Foldable++-- Compiling+instance Gram_Term_AtomsFor src ss g Foldable+instance (Source src, Inj_Sym ss Foldable) => ModuleFor src ss Foldable where+	moduleFor = ["Foldable"] `moduleWhere`+	 [ "foldMap" := teFoldable_foldMap+	 , "foldr"   := teFoldable_foldr+	 , "foldr'"  := teFoldable_foldr'+	 , "foldl"   := teFoldable_foldl+	 , "elem" `withInfixN` 4 := teFoldable_elem+	 , "sum"     := teFoldable_sum+	 , "product" := teFoldable_product+	 , "toList"  := teFoldable_toList+	 , "all"     := teFoldable_all+	 , "any"     := teFoldable_any+	 , "and"     := teFoldable_and+	 , "or"      := teFoldable_or+	 , "concat"  := teFoldable_concat+	 , "asum"    := teFoldable_asum+	 -- , "msum"    := teFoldable_msum+	 ]++-- ** 'Type's+tyFoldable :: Source src => Type src vs a -> Type src vs (Foldable a)+tyFoldable a = tyConstLen @(K Foldable) @Foldable (lenVars a) `tyApp` a++t0 :: Source src => Inj_Len vs => Inj_Kind (K t) =>+      Type src (Proxy t ': vs) t+t0 = tyVar "t" $ varZ++t1 :: Source src => Inj_Len vs => Inj_Kind (K t) =>+      Type src (a ': Proxy t ': vs) t+t1 = tyVar "t" $ VarS varZ++t2 :: Source src => Inj_Len vs => Inj_Kind (K t) =>+      Type src (a ': b ': Proxy t ': vs) t+t2 = tyVar "t" $ VarS $ VarS varZ++-- ** 'Term's+teFoldable_foldMap :: TermDef Foldable '[Proxy a, Proxy t, Proxy m] (Foldable t # Monoid m #> ((a -> m) -> t a -> m))+teFoldable_foldMap = Term (tyFoldable t1 # tyMonoid m) ((a0 ~> m) ~> t1 `tyApp` a0 ~> m) $ teSym @Foldable $ lam2 foldMap+	where+	m :: Source src => Inj_Len vs => Inj_Kind (K m) =>+	     Type src (a ': b ': Proxy m ': vs) m+	m = tyVar "m" $ VarS $ VarS varZ++teFoldable_elem :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Eq a #> (a -> t a -> Bool))+teFoldable_elem = Term (tyFoldable t1 # tyEq a0) (a0 ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 elem++teFoldable_toList :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> [a]))+teFoldable_toList = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyList a0) $ teSym @Foldable $ lam1 toList++teFoldable_concat :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t [a] -> [a]))+teFoldable_concat = Term (tyFoldable t1) (t1 `tyApp` (tyList a0) ~> tyList a0) $ teSym @Foldable $ lam1 concat++teFoldable_foldr, teFoldable_foldr' :: TermDef Foldable '[Proxy a, Proxy b, Proxy t] (Foldable t #> ((a -> b -> b) -> b -> t a -> b))+teFoldable_foldr = Term (tyFoldable t2) ((a0 ~> b1 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldr++teFoldable_foldr' = Term (tyFoldable t2) ((a0 ~> b1 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldr'++teFoldable_foldl :: TermDef Foldable '[Proxy a, Proxy b, Proxy t] (Foldable t #> ((b -> a -> b) -> b -> t a -> b))+teFoldable_foldl = Term (tyFoldable t2) ((b1 ~> a0 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldl++teFoldable_length :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> Int))+teFoldable_length = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyInt) $ teSym @Foldable $ lam1 length++teFoldable_null :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> Bool))+teFoldable_null = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam1 null++teFoldable_minimum, teFoldable_maximum :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Ord a #> (t a -> a))+teFoldable_minimum = Term (tyFoldable t1 # tyOrd a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 minimum+teFoldable_maximum = Term (tyFoldable t1 # tyOrd a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 maximum++teFoldable_sum, teFoldable_product :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Num a #> (t a -> a))+teFoldable_sum = Term (tyFoldable t1 # tyNum a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 sum+teFoldable_product = Term (tyFoldable t1 # tyNum a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 product++teFoldable_all, teFoldable_any :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> ((a -> Bool) -> t a -> Bool))+teFoldable_all = Term (tyFoldable t1) ((a0 ~> tyBool) ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 all+teFoldable_any = Term (tyFoldable t1) ((a0 ~> tyBool) ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 any++teFoldable_and, teFoldable_or :: TermDef Foldable '[Proxy t] (Foldable t #> (t Bool -> Bool))+teFoldable_and = Term (tyFoldable t0) (t0 `tyApp` tyBool ~> tyBool) $ teSym @Foldable $ lam1 and+teFoldable_or = Term (tyFoldable t0) (t0 `tyApp` tyBool ~> tyBool) $ teSym @Foldable $ lam1 or++teFoldable_asum :: TermDef Foldable '[Proxy a, Proxy t, Proxy f] ((Foldable t # Alternative f) #> (t (f a) -> f a))+teFoldable_asum = Term (tyFoldable t1 # tyAlternative f2) (t1 `tyApp` (f2 `tyApp` a0) ~> (f2 `tyApp` a0)) $ teSym @Foldable $ lam1 asum++{- TODO: when MonadPlus will be supported+teFoldable_msum ::+ Source src => Inj_Sym ss Foldable =>+ Term src ss ts '[Proxy a, Proxy t, Proxy f] ((Foldable t # MonadPlus f) #> (t (f a) -> f a))+teFoldable_msum =+	Term ((tyFoldable t1 # (tyConst @(K MonadPlus) @MonadPlus `tyApp` f2))) (t1 `tyApp` (f2 `tyApp` a0) ~> (f2 `tyApp` a0)) $+	teSym @Foldable $ lam1 msum+-}
+ Language/Symantic/Lib/Foldable/Test.hs view
@@ -0,0 +1,32 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module Lib.Foldable.Test where++import Test.Tasty++import Data.Proxy (Proxy(..))+import Prelude hiding ((&&), not, (||))++import Language.Symantic.Lib+import Compiling.Test++type SS =+ [ Proxy (->)+ , Proxy Int+ , Proxy Integer+ , Proxy []+ , Proxy ()+ , Proxy (,)+ , Proxy Foldable+ ]+(==>) = test_readTerm @() @SS++tests :: TestTree+tests = testGroup "Foldable"+ [ {-"[]" ==> Right (tyList (tyVar "a" varZ), [], "[]")+ ,-} "[1, 2, 3]" ==> Right (tyList tyInteger, [1, 2, 3], "1 : 2 : 3 : []")+ , "1 : 2 : 3 : []" ==> Right (tyList tyInteger, [1, 2, 3], "1 : 2 : 3 : []")+ , "foldMap (\\(x0:Integer) -> [x0, x0]) [1, 2, 3]" ==> Right+	 ( tyList tyInteger+	 , [1, 1, 2, 2, 3, 3]+	 , "foldMap (\\x0 -> x0 : x0 : []) (1 : 2 : 3 : [])" )+ ]
+ Language/Symantic/Lib/Function.hs view
@@ -0,0 +1,105 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for '(->)'.+module Language.Symantic.Lib.Function where++import Prelude hiding (const, flip, id)+import qualified Data.Function as Fun+import qualified Data.MonoTraversable as MT++import Language.Symantic++-- * Class 'Sym_Function'+type instance Sym (Proxy (->)) = Sym_Function+class Sym_Function term where+	comp  :: term (b -> c) -> term (a -> b) -> term (a -> c); infixr 9 `comp`+	const :: term a -> term b -> term a+	flip  :: term (a -> b -> c) -> term (b -> a -> c)+	id    :: term a -> term a+	default comp  :: Sym_Function (UnT term) => Trans term => term (b -> c) -> term (a -> b) -> term (a -> c)+	default const :: Sym_Function (UnT term) => Trans term => term a -> term b -> term a+	default flip  :: Sym_Function (UnT term) => Trans term => term (a -> b -> c) -> term (b -> a -> c)+	default id    :: Sym_Function (UnT term) => Trans term => term a -> term a+	comp  = trans2 comp+	const = trans2 const+	flip  = trans1 flip+	id    = trans1 id++-- Interpreting+instance Sym_Function Eval where+	comp  = eval2 (Fun..)+	const = eval2 Fun.const+	flip  = eval1 Fun.flip+	id    = eval1 Fun.id+instance Sym_Function View where+	comp  = viewInfix "." (infixR 9)+	const = view2 "const"+	flip  = view1 "flip"+	id    = view1 "id"+instance (Sym_Function r1, Sym_Function r2) => Sym_Function (Dup r1 r2) where+	comp  = dup2 @Sym_Function comp+	const = dup2 @Sym_Function const+	flip  = dup1 @Sym_Function flip+	id    = dup1 @Sym_Function id++-- Transforming+instance (Sym_Function term, Sym_Lambda term) => Sym_Function (BetaT term)++-- Typing+instance ClassInstancesFor (->) where+	proveConstraintFor _c (TyApp _ q (TyApp _ z _r))+	 | Just HRefl <- proj_ConstKiTy @_ @(->) z+	 = case () of+		 _ | Just HRefl <- proj_ConstKiTy @_ @Functor     q -> Just Dict+		   | Just HRefl <- proj_ConstKiTy @_ @Applicative q -> Just Dict+		   | Just HRefl <- proj_ConstKiTy @_ @Monad       q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c (TyApp _ q (TyApp _ (TyApp _ z _a) b))+	 | Just HRefl <- proj_ConstKiTy @_ @(->) z+	 = case () of+		 _ | Just HRefl <- proj_ConstKiTy @_ @Monoid q+		   , Just Dict  <- proveConstraint (q `tyApp` b) -> Just Dict+		   | Just HRefl <- proj_ConstKiTy @_ @MT.MonoFunctor q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor (->)++-- Compiling+instance Gram_Term_AtomsFor src ss g (->)+instance (Source src, Inj_Sym ss (->)) => ModuleFor src ss (->) where+	moduleFor = ["Function"] `moduleWhere`+	 [ "const" := teFunction_const+	 , "flip"  := teFunction_flip+	 , "id"    := teFunction_id+	 , "." `withInfixR` 9 := teFunction_compose+	 -- , "$" `withInfixR` 0 := teFunction_app+	 ]++-- ** 'Type's+tyFun :: Source src => Inj_Len vs => Type src vs (->)+tyFun = tyConst @(K (->)) @(->)++a0 :: Source src => Inj_Len vs => Inj_Kind (K a) =>+     Type src (Proxy a ': vs) a+a0 = tyVar "a" varZ++b1 :: Source src => Inj_Len vs => Inj_Kind (K b) =>+     Type src (a ': Proxy b ': vs) b+b1 = tyVar "b" $ VarS varZ++c2 :: Source src => Inj_Len vs => Inj_Kind (K c) =>+     Type src (a ': b ': Proxy c ': vs) c+c2 = tyVar "c" $ VarS $ VarS varZ++-- ** 'Term's+teFunction_compose :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((b -> c) -> (a -> b) -> (a -> c)))+teFunction_compose = Term noConstraint ((b1 ~> c2) ~> (a0 ~> b1) ~> (a0 ~> c2)) $ teSym @(->) $ lam2 comp++teFunction_const :: TermDef (->) '[Proxy a, Proxy b] (() #> (a -> b -> a))+teFunction_const = Term noConstraint (a0 ~> b1 ~> a0) $ teSym @(->) $ lam2 const++teFunction_flip :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> (b -> a -> c)))+teFunction_flip = Term noConstraint ((a0 ~> b1 ~> c2) ~> (b1 ~> a0 ~> c2)) $ teSym @(->) $ lam1 flip++teFunction_id :: TermDef (->) '[Proxy a] (() #> (a -> a))+teFunction_id = Term noConstraint (a0 ~> a0) $ teSym @(->) $ lam1 id
+ Language/Symantic/Lib/Functor.hs view
@@ -0,0 +1,78 @@+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Functor'.+module Language.Symantic.Lib.Functor where++import Data.Functor (Functor)+import Prelude hiding (Functor(..), (<$>))+import qualified Data.Function as Fun+import qualified Data.Functor as Functor++import Language.Symantic+import Language.Symantic.Lib.Function (a0, b1)++-- * Class 'Sym_Functor'+type instance Sym (Proxy Functor) = Sym_Functor+class Sym_Functor term where+	fmap :: Functor f => term (a -> b) -> term (f a) -> term (f b)+	default fmap :: Sym_Functor (UnT term) => Trans term => Functor f => term (a -> b) -> term (f a) -> term (f b)+	fmap = trans2 fmap+	+	(<$>) :: (Sym_Functor term, Functor f) => term (a -> b) -> term (f a) -> term (f b); infixl 4 <$>+	(<$>) = fmap+	+	(<$) :: Functor f => term a -> term (f b) -> term (f a); infixl 4 <$+	default (<$) :: Sym_Lambda term => Functor f => term a -> term (f b) -> term (f a)+	(<$) x = fmap (lam (Fun.const x))++-- Interpreting+instance Sym_Functor Eval where+	fmap  = eval2 Functor.fmap+	(<$)  = eval2 (Functor.<$)+instance Sym_Functor View where+	fmap  = view2 "fmap"+	(<$>) = viewInfix "<$>" (infixL 4)+	(<$)  = viewInfix "<$"  (infixL 4)+instance (Sym_Functor r1, Sym_Functor r2) => Sym_Functor (Dup r1 r2) where+	fmap = dup2 @Sym_Functor fmap+	(<$) = dup2 @Sym_Functor (<$)++-- Transforming+instance (Sym_Functor term, Sym_Lambda term) => Sym_Functor (BetaT term) where+	(<$>) = trans2 (<$>)+	(<$)  = trans2 (<$)++-- Typing+instance FixityOf Functor+instance ClassInstancesFor Functor+instance TypeInstancesFor Functor++-- Compiling+instance Gram_Term_AtomsFor src ss g Functor+instance (Source src, Inj_Sym ss Functor) => ModuleFor src ss Functor where+	moduleFor = ["Functor"] `moduleWhere`+	 [ "fmap" := teFunctor_fmap+	 , "<$"  `withInfixL` 4 := teFunctor_const+	 , "<$>" `withInfixL` 4 := teFunctor_fmap_infix+	 ]++-- ** 'Type's+tyFunctor :: Source src => Type src vs a -> Type src vs (Functor a)+tyFunctor a = tyConstLen @(K Functor) @Functor (lenVars a) `tyApp` a++f1 :: Source src => Inj_Len vs => Inj_Kind (K f) =>+      Type src (a ': Proxy f ': vs) f+f1 = tyVar "f" $ VarS varZ++f2 :: Source src => Inj_Len vs => Inj_Kind (K f) =>+      Type src (a ': b ': Proxy f ': vs) f+f2 = tyVar "f" $ VarS $ VarS varZ++-- ** 'Term's+teFunctor_fmap, teFunctor_fmap_infix :: TermDef Functor '[Proxy a, Proxy b, Proxy f] (Functor f #> ((a -> b) -> f a -> f b))+teFunctor_fmap = Term (tyFunctor f2) ((a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Functor $ lam2 fmap+teFunctor_fmap_infix = Term (tyFunctor f2) ((a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Functor $ lam2 (<$>)++teFunctor_const :: TermDef Functor '[Proxy a, Proxy b, Proxy f] (Functor f #> (a -> f b -> f a))+teFunctor_const = Term (tyFunctor f2) (a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` a0) $ teSym @Functor $ lam2 (<$)
+ Language/Symantic/Lib/Functor/Test.hs view
@@ -0,0 +1,28 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module Lib.Functor.Test where++import Test.Tasty++import Data.Proxy (Proxy(..))+import Prelude hiding ((&&), not, (||))++import Language.Symantic ()+import Language.Symantic.Lib+import Compiling.Test++type SS =+ [ Proxy (->)+ , Proxy Bool+ , Proxy Functor+ , Proxy Integer+ , Proxy Maybe+ ]+(==>) = test_readTerm @() @SS++tests :: TestTree+tests = testGroup "Functor"+ [ "fmap not (Just True)" ==> Right (tyMaybe tyBool, Just False, "fmap (\\x0 -> not x0) (Just True)")+ , "not `fmap` Just True" ==> Right (tyMaybe tyBool, Just False, "fmap (\\x0 -> not x0) (Just True)")+ , "not <$> Just True"    ==> Right (tyMaybe tyBool, Just False, "(\\x0 -> not x0) <$> Just True")+ , "False <$ Just True"   ==> Right (tyMaybe tyBool, Just False, "False <$ Just True")+ ]
+ Language/Symantic/Lib/IO.hs view
@@ -0,0 +1,125 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'IO'.+module Language.Symantic.Lib.IO where++import qualified Data.MonoTraversable as MT+import qualified System.IO as IO++import Language.Symantic+import Language.Symantic.Lib.Char (tyString)+import Language.Symantic.Lib.MonoFunctor (Element)+import Language.Symantic.Lib.Unit (tyUnit)++-- * Class 'Sym_IO'+type instance Sym (Proxy IO)        = Sym_IO+type instance Sym (Proxy IO.Handle) = Sym_IO_Handle+type instance Sym (Proxy IO.IOMode) = Sym_IO_Mode+class Sym_IO (term:: * -> *)+class Sym_IO_Handle (term:: * -> *) where+	io_hClose   :: term IO.Handle -> term (IO ())+	io_openFile :: term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)+	+	default io_hClose   :: Sym_IO_Handle (UnT term) => Trans term => term IO.Handle -> term (IO ())+	default io_openFile :: Sym_IO_Handle (UnT term) => Trans term => term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)+	+	io_hClose   = trans1 io_hClose+	io_openFile = trans2 io_openFile+class Sym_IO_Mode (term:: * -> *)++-- Interpreting+instance Sym_IO Eval+instance Sym_IO_Handle Eval where+	io_hClose   = eval1 IO.hClose+	io_openFile = eval2 IO.openFile+instance Sym_IO_Mode Eval++instance Sym_IO View+instance Sym_IO_Handle View where+	io_hClose   = view1 "IO.hClose"+	io_openFile = view2 "IO.openFile"+instance Sym_IO_Mode View++instance Sym_IO (Dup r1 r2)+instance (Sym_IO_Handle r1, Sym_IO_Handle r2) => Sym_IO_Handle (Dup r1 r2) where+	io_hClose   = dup1 @Sym_IO_Handle io_hClose+	io_openFile = dup2 @Sym_IO_Handle io_openFile+instance Sym_IO_Mode (Dup r1 r2)++-- Transforming+instance (Sym_IO term, Sym_Lambda term) => Sym_IO (BetaT term)+instance (Sym_IO_Handle term, Sym_Lambda term) => Sym_IO_Handle (BetaT term)+instance (Sym_IO_Mode term, Sym_Lambda term) => Sym_IO_Mode (BetaT term)++-- Typing+instance FixityOf IO+instance ClassInstancesFor IO where+	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)+	 | Just HRefl <- proj_ConstKiTy @_ @IO z+	 = case () of+		 _ | Just Refl <- proj_Const @Applicative q -> Just Dict+		   | Just Refl <- proj_Const @Functor     q -> Just Dict+		   | Just Refl <- proj_Const @Monad       q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _ (TyApp _ q (TyApp _ z _a))+	 | Just HRefl <- proj_ConstKiTy @_ @IO z+	 = case () of+		 _ | Just Refl <- proj_ConstTy @MT.MonoFunctor q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance ClassInstancesFor IO.Handle where+	proveConstraintFor _ (TyApp _ q z)+	 | Just HRefl <- proj_ConstKiTy @_ @IO.Handle z+	 = case () of+		 _ | Just Refl <- proj_ConstTy @Eq q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance ClassInstancesFor IO.IOMode where+	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)+	 | Just HRefl <- proj_ConstKiTy @_ @IO.IOMode c+	 = case () of+		 _ | Just Refl <- proj_Const @Enum q -> Just Dict+		   | Just Refl <- proj_Const @Eq   q -> Just Dict+		   | Just Refl <- proj_Const @Ord  q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor IO where+	expandFamFor _c _len f (TyApp _ z a `TypesS` TypesZ)+	 | Just HRefl <- proj_ConstKi @_ @Element f+	 , Just HRefl <- proj_ConstKiTy @_ @IO z+	 = Just a+	expandFamFor _c _len _fam _as = Nothing+instance TypeInstancesFor IO.Handle+instance TypeInstancesFor IO.IOMode++-- Compiling+instance ModuleFor src ss IO+instance (Source src, Inj_Sym ss IO.Handle) => ModuleFor src ss IO.Handle where+	moduleFor = ["IO"] `moduleWhere`+	 [ "hClose"   := teIO_hClose+	 , "openFile" := teIO_openFile+	 ]+instance ModuleFor src ss IO.IOMode+instance Gram_Term_AtomsFor src ss g IO+instance Gram_Term_AtomsFor src ss g IO.Handle+instance Gram_Term_AtomsFor src ss g IO.IOMode++-- ** 'Type's+tyIO :: Source src => Type src vs a -> Type src vs (IO a)+tyIO a = tyConstLen @(K IO) @IO (lenVars a) `tyApp` a++tyIO_Handle :: Source src => Inj_Len vs => Type src vs IO.Handle+tyIO_Handle = tyConst @(K IO.Handle) @IO.Handle++tyIO_Mode :: Source src => Inj_Len vs => Type src vs IO.IOMode+tyIO_Mode = tyConst @(K IO.IOMode) @IO.IOMode++tyFilePath :: Source src => Inj_Len vs => Type src vs FilePath+tyFilePath = tyString++-- ** 'Term's+teIO_hClose :: TermDef IO.Handle '[] (() #> (IO.Handle -> IO ()))+teIO_hClose = Term noConstraint (tyIO_Handle ~> tyIO tyUnit) $ teSym @IO.Handle $ lam1 io_hClose++teIO_openFile :: TermDef IO.Handle '[] (() #> (FilePath -> IO.IOMode -> IO (IO.Handle)))+teIO_openFile = Term noConstraint (tyFilePath ~> tyIO_Mode ~> tyIO tyIO_Handle) $ teSym @IO.Handle $ lam2 io_openFile
+ Language/Symantic/Lib/If.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for @If@.+module Language.Symantic.Lib.If where++import qualified Data.Text as Text++import Language.Symantic+import Language.Symantic.Lib.Bool (tyBool)+import Language.Symantic.Lib.Function (a0)++-- * Type 'If'+data If++-- * Class 'Sym_If'+type instance Sym (Proxy If) = Sym_If+class Sym_If term where+	if_ :: term Bool -> term a -> term a -> term a+	default if_ :: Sym_If (UnT term) => Trans term => term Bool -> term a -> term a -> term a+	if_ = trans3 if_++-- Interpreting+instance Sym_If Eval where+	if_ (Eval b) ok ko = if b then ok else ko+instance Sym_If View where+	if_ (View cond) (View ok) (View ko) =+		View $ \po v ->+			parenInfix po op $+			Text.concat+			 [ "if ", cond (op, SideL) v+			 , " then ", ok (op, SideL) v+			 , " else ", ko (op, SideL) v ]+		where op = infixN 2+instance (Sym_If r1, Sym_If r2) => Sym_If (Dup r1 r2) where+	if_  = dup3 @Sym_If if_++-- Transforming+instance (Sym_If term, Sym_Lambda term) => Sym_If (BetaT term)++-- Typing+instance ClassInstancesFor If+instance TypeInstancesFor If++-- Compiling+instance Gram_Term_AtomsFor src ss g If+ -- TODO: some support for if-then-else or ternary (?:) operator+instance ModuleFor src ss If++-- ** 'Type's++-- ** 'Term's+teIf_if :: TermDef If '[Proxy a] (() #> (Bool -> a -> a -> a))+teIf_if = Term noConstraint (tyBool ~> a0 ~> a0 ~> a0) $ teSym @If $ lam3 if_
+ Language/Symantic/Lib/Int.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Int'.+module Language.Symantic.Lib.Int where++import qualified Data.Text as Text++import Language.Symantic++-- * Class 'Sym_Int'+type instance Sym (Proxy Int) = Sym_Int+class Sym_Int term where+	int :: Int -> term Int+	default int :: Sym_Int (UnT term) => Trans term => Int -> term Int+	int = trans . int++-- Interpreting+instance Sym_Int Eval where+	int = Eval+instance Sym_Int View where+	int a = View $ \_p _v ->+		Text.pack (show a)+instance (Sym_Int r1, Sym_Int r2) => Sym_Int (Dup r1 r2) where+	int x = int x `Dup` int x++-- Transforming+instance (Sym_Int term, Sym_Lambda term) => Sym_Int (BetaT term)++-- Typing+instance ClassInstancesFor Int where+	proveConstraintFor _c (TyApp _ (TyConst _ _ q) z)+	 | Just HRefl <- proj_ConstKiTy @_ @Int z+	 = case () of+		 _ | Just Refl <- proj_Const @Bounded  q -> Just Dict+		   | Just Refl <- proj_Const @Enum     q -> Just Dict+		   | Just Refl <- proj_Const @Eq       q -> Just Dict+		   | Just Refl <- proj_Const @Integral q -> Just Dict+		   | Just Refl <- proj_Const @Num      q -> Just Dict+		   | Just Refl <- proj_Const @Ord      q -> Just Dict+		   | Just Refl <- proj_Const @Real     q -> Just Dict+		   | Just Refl <- proj_Const @Show     q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor Int++-- Compiling+instance Gram_Term_AtomsFor src ss g Int+instance ModuleFor src ss Int++-- ** 'Type's+tyInt :: Source src => Inj_Len vs => Type src vs Int+tyInt = tyConst @(K Int) @Int++-- ** 'Term's+teInt :: Source src => Inj_Sym ss Int => Int -> Term src ss ts '[] (() #> Int)+teInt i = Term noConstraint tyInt $ teSym @Int $ int i
+ Language/Symantic/Lib/Integer.hs view
@@ -0,0 +1,68 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Integer'.+module Language.Symantic.Lib.Integer where++import qualified Data.Text as Text++import Language.Symantic+import Language.Symantic.Grammar++-- * Class 'Sym_Integer'+type instance Sym (Proxy Integer) = Sym_Integer+class Sym_Integer term where+	integer :: Integer -> term Integer+	default integer :: Sym_Integer (UnT term) => Trans term => Integer -> term Integer+	integer = trans . integer++-- Interpreting+instance Sym_Integer Eval where+	integer = Eval+instance Sym_Integer View where+	integer a = View $ \_p _v ->+		Text.pack (show a)+instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (Dup r1 r2) where+	integer x = integer x `Dup` integer x++-- Transforming+instance (Sym_Integer term, Sym_Lambda term) => Sym_Integer (BetaT term)++-- Typing+instance ClassInstancesFor Integer where+	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)+	 | Just HRefl <- proj_ConstKiTy @_ @Integer z+	 = case () of+		 _ | Just Refl <- proj_Const @Enum     q -> Just Dict+		   | Just Refl <- proj_Const @Eq       q -> Just Dict+		   | Just Refl <- proj_Const @Integral q -> Just Dict+		   | Just Refl <- proj_Const @Num      q -> Just Dict+		   | Just Refl <- proj_Const @Ord      q -> Just Dict+		   | Just Refl <- proj_Const @Real     q -> Just Dict+		   | Just Refl <- proj_Const @Show     q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor Integer++-- Compiling+instance+ ( Gram_Source src g+ , Gram_Alt g+ , Gram_AltApp g+ , Gram_Rule g+ , Gram_Comment g+ , Inj_Sym ss Integer+ ) => Gram_Term_AtomsFor src ss g Integer where+	g_term_atomsFor =+	 [ rule "teinteger" $+		lexeme $ g_source $+		(\i src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teInteger $ read i)+		 <$> some (choice $ char <$> ['0'..'9'])+	 ]+instance ModuleFor src ss Integer++-- ** 'Term's+tyInteger :: Source src => Inj_Len vs => Type src vs Integer+tyInteger = tyConst @(K Integer) @Integer++teInteger :: Source src => Inj_Sym ss Integer => Integer -> Term src ss ts '[] (() #> Integer)+teInteger i = Term noConstraint tyInteger $ teSym @Integer $ integer i
+ Language/Symantic/Lib/Integral.hs view
@@ -0,0 +1,105 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Integral'.+module Language.Symantic.Lib.Integral where++import Prelude (Integral)+import Prelude hiding (Integral(..))+import qualified Prelude++import Language.Symantic+import Language.Symantic.Lib.Function (a0)+import Language.Symantic.Lib.Integer (tyInteger)+import Language.Symantic.Lib.Tuple2 (tyTuple2)++-- * Class 'Sym_Integral'+type instance Sym (Proxy Integral) = Sym_Integral+class Sym_Integral term where+	quot      :: Integral i => term i -> term i -> term i; infixl 7 `quot`+	rem       :: Integral i => term i -> term i -> term i; infixl 7 `rem`+	div       :: Integral i => term i -> term i -> term i; infixl 7 `div`+	mod       :: Integral i => term i -> term i -> term i; infixl 7 `mod`+	quotRem   :: Integral i => term i -> term i -> term (i, i)+	divMod    :: Integral i => term i -> term i -> term (i, i)+	toInteger :: Integral i => term i -> term Integer+	+	default quot      :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i+	default rem       :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i+	default div       :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i+	default mod       :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i+	default quotRem   :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term (i, i)+	default divMod    :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term (i, i)+	default toInteger :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term Integer+	+	quot      = trans2 quot+	rem       = trans2 rem+	div       = trans2 div+	mod       = trans2 mod+	quotRem   = trans2 quotRem+	divMod    = trans2 divMod+	toInteger = trans1 toInteger++-- Interpreting+instance Sym_Integral Eval where+	quot      = eval2 Prelude.quot+	rem       = eval2 Prelude.rem+	div       = eval2 Prelude.div+	mod       = eval2 Prelude.mod+	quotRem   = eval2 Prelude.quotRem+	divMod    = eval2 Prelude.divMod+	toInteger = eval1 Prelude.toInteger+instance Sym_Integral View where+	quot      = viewInfix "`quot`" (infixL 7)+	div       = viewInfix "`div`"  (infixL 7)+	rem       = viewInfix "`rem`"  (infixL 7)+	mod       = viewInfix "`mod`"  (infixL 7)+	quotRem   = view2 "quotRem"+	divMod    = view2 "divMod"+	toInteger = view1 "toInteger"+instance (Sym_Integral r1, Sym_Integral r2) => Sym_Integral (Dup r1 r2) where+	quot      = dup2 @Sym_Integral quot+	rem       = dup2 @Sym_Integral rem+	div       = dup2 @Sym_Integral div+	mod       = dup2 @Sym_Integral mod+	quotRem   = dup2 @Sym_Integral quotRem+	divMod    = dup2 @Sym_Integral divMod+	toInteger = dup1 @Sym_Integral toInteger++-- Transforming+instance (Sym_Integral term, Sym_Lambda term) => Sym_Integral (BetaT term)++-- Typing+instance FixityOf Integral+instance ClassInstancesFor Integral+instance TypeInstancesFor Integral++-- Compiling+instance Gram_Term_AtomsFor src ss g Integral+instance (Source src, Inj_Sym ss Integral) => ModuleFor src ss Integral where+	moduleFor = ["Integral"] `moduleWhere`+	 [ "quot" `withInfixL` 7 := teIntegral_quot+	 , "rem"  `withInfixL` 7 := teIntegral_rem+	 , "div"  `withInfixL` 7 := teIntegral_div+	 , "mod"  `withInfixL` 7 := teIntegral_mod+	 , "quotRem"   := teIntegral_quotRem+	 , "divMod"    := teIntegral_divMod+	 , "toInteger" := teIntegral_toInteger+	 ]++-- ** 'Type's+tyIntegral :: Source src => Type src vs a -> Type src vs (Integral a)+tyIntegral a = tyConstLen @(K Integral) @Integral (lenVars a) `tyApp` a++-- ** 'Term's+teIntegral_quot, teIntegral_rem, teIntegral_div, teIntegral_mod :: TermDef Integral '[Proxy a] (Integral a #> (a -> a -> a))+teIntegral_quot = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 quot+teIntegral_rem  = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 rem+teIntegral_div  = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 div+teIntegral_mod  = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 mod++teIntegral_quotRem, teIntegral_divMod :: TermDef Integral '[Proxy a] (Integral a #> (a -> a -> (a, a)))+teIntegral_quotRem = Term (tyIntegral a0) (a0 ~> a0 ~> tyTuple2 a0 a0) $ teSym @Integral $ lam2 quotRem+teIntegral_divMod  = Term (tyIntegral a0) (a0 ~> a0 ~> tyTuple2 a0 a0) $ teSym @Integral $ lam2 divMod++teIntegral_toInteger :: TermDef Integral '[Proxy a] (Integral a #> (a -> Integer))+teIntegral_toInteger = Term (tyIntegral a0) (a0 ~> tyInteger) $ teSym @Integral $ lam1 toInteger
+ Language/Symantic/Lib/List.hs view
@@ -0,0 +1,148 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for '[]'.+module Language.Symantic.Lib.List where++import Data.Semigroup ((<>))+import Prelude hiding (zipWith)+import qualified Data.Functor as Functor+import qualified Data.List as List+import qualified Data.MonoTraversable as MT+import qualified Data.Sequences as Seqs+import qualified Data.Text as Text+import qualified Data.Traversable as Traversable++import Language.Symantic+import Language.Symantic.Grammar+import Language.Symantic.Lib.Function (a0, b1, c2)+import Language.Symantic.Lib.MonoFunctor (Element)++-- * Class 'Sym_List'+type instance Sym (Proxy []) = Sym_List+class Sym_List term where+	list_empty :: term [a]+	list_cons  :: term a -> term [a] -> term [a]; infixr 5 `list_cons`+	list       :: [term a] -> term [a]+	zipWith    :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]+	+	default list_empty :: Sym_List (UnT term) => Trans term => term [a]+	default list_cons  :: Sym_List (UnT term) => Trans term => term a -> term [a] -> term [a]+	default list       :: Sym_List (UnT term) => Trans term => [term a] -> term [a]+	default zipWith    :: Sym_List (UnT term) => Trans term => term (a -> b -> c) -> term [a] -> term [b] -> term [c]+	+	list_empty = trans list_empty+	list_cons  = trans2 list_cons+	list l     = trans (list (unTrans Functor.<$> l))+	zipWith    = trans3 zipWith++-- Interpreting+instance Sym_List Eval where+	list_empty = return []+	list_cons  = eval2 (:)+	list       = Traversable.sequence+	zipWith    = eval3 List.zipWith+instance Sym_List View where+	list_empty = View $ \_p _v -> "[]"+	list_cons = viewInfix ":" (infixR 5)+	list l = View $ \_po v ->+		"[" <> Text.intercalate ", " ((\(View a) -> a op v) Functor.<$> l) <> "]"+		where op = (infixN0, SideL)+	zipWith = view3 "zipWith"+instance (Sym_List r1, Sym_List r2) => Sym_List (Dup r1 r2) where+	list_empty = dup0 @Sym_List list_empty+	list_cons  = dup2 @Sym_List list_cons+	list l =+		let (l1, l2) =+			foldr (\(x1 `Dup` x2) (xs1, xs2) ->+				(x1:xs1, x2:xs2)) ([], []) l in+		list l1 `Dup` list l2+	zipWith = dup3 @Sym_List zipWith++-- Transforming+instance (Sym_List term, Sym_Lambda term) => Sym_List (BetaT term)++-- Typing+instance FixityOf [] where+instance ClassInstancesFor [] where+	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)+	 | Just HRefl <- proj_ConstKiTy @_ @[] z+	 = case () of+		 _ | Just Refl <- proj_Const @Applicative q -> Just Dict+		   | Just Refl <- proj_Const @Foldable    q -> Just Dict+		   | Just Refl <- proj_Const @Functor     q -> Just Dict+		   | Just Refl <- proj_Const @Monad       q -> Just Dict+		   | Just Refl <- proj_Const @Traversable q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ z a))+	 | Just HRefl <- proj_ConstKiTy @_ @[] z+	 = case () of+		 _ | Just Refl <- proj_Const @Eq q+		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   | Just Refl <- proj_Const @Monoid q -> Just Dict+		   | Just Refl <- proj_Const @Show q+		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   | Just Refl <- proj_Const @Ord q+		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFoldable   q -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFunctor    q -> Just Dict+		   | Just Refl <- proj_Const @Seqs.IsSequence   q -> Just Dict+		   | Just Refl <- proj_Const @Seqs.SemiSequence q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor [] where+	expandFamFor _c _len f ((TyApp _ z a) `TypesS` TypesZ)+	 | Just HRefl <- proj_ConstKi   @_ @Element f+	 , Just HRefl <- proj_ConstKiTy @_ @[] z+	 = Just a+	expandFamFor _c _len _fam _as = Nothing++-- Compiling+instance+ ( Gram_App g+ , Gram_Rule g+ , Gram_Comment g+ , Gram_Term src ss g+ , Inj_Sym ss []+ ) => Gram_Term_AtomsFor src ss g [] where+	g_term_atomsFor =+	 [ rule "teList_list" $+		between (symbol "[") (symbol "]") listG+	 , rule "teList_empty" $+		g_source $+		(\src -> BinTree0 $ Token_Term $ TermAVT teList_empty `setSource` src)+		 <$ symbol "["+		 <* symbol "]"+	 ]+		where+		listG :: CF g (AST_Term src ss)+		listG = rule "list" $+			g_source $+			(\a mb src ->+				case mb of+				 Just b  -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a) b+				 Nothing ->+					BinTree2+					 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a)+					 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_empty))+			 <$> g_term+			 <*> option Nothing (Just <$ symbol "," <*> listG)+instance (Source src, Inj_Sym ss []) => ModuleFor src ss [] where+	moduleFor = ["List"] `moduleWhere`+	 [ "[]"      := teList_empty+	 , "zipWith" := teList_zipWith+	 , ":" `withInfixR` 5 := teList_cons+	 ]++-- ** 'Type's+tyList :: Source src => Inj_Len vs => Type src vs a -> Type src vs [a]+tyList = (tyConst @(K []) @[] `tyApp`)++-- ** 'Term's+teList_empty :: Source src => Inj_Sym ss [] => Term src ss ts '[Proxy a] (() #> [a])+teList_empty = Term noConstraint (tyList a0) $ teSym @[] $ list_empty++teList_cons :: Source src => Inj_Sym ss [] => Term src ss ts '[Proxy a] (() #> (a -> [a] -> [a]))+teList_cons = Term noConstraint (a0 ~> tyList a0 ~> tyList a0) $ teSym @[] $ lam2 list_cons++teList_zipWith :: Source src => Inj_Sym ss [] => Term src ss ts '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> [a] -> [b] -> [c]))+teList_zipWith = Term noConstraint ((a0 ~> b1 ~> c2) ~> tyList a0 ~> tyList b1 ~> tyList c2) $ teSym @[] $ lam3 zipWith
+ Language/Symantic/Lib/Map.hs view
@@ -0,0 +1,174 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Map'.+module Language.Symantic.Lib.Map where++import Data.Map.Strict (Map)+import Data.MonoTraversable (MonoFunctor)+import qualified Data.Map.Strict as Map++import Language.Symantic+import Language.Symantic.Lib.Bool (tyBool)+import Language.Symantic.Lib.Function (a0, b1)+import Language.Symantic.Lib.List (tyList)+import Language.Symantic.Lib.Maybe (tyMaybe)+import Language.Symantic.Lib.MonoFunctor (Element)+import Language.Symantic.Lib.Ord (tyOrd)+import Language.Symantic.Lib.Tuple2 (tyTuple2)++-- * Class 'Sym_Map'+type instance Sym (Proxy Map) = Sym_Map+class Sym_Map term where+	map_fromList     :: Ord k => term [(k, a)] -> term (Map k a)+	map_mapWithKey   :: term (k -> a -> b) -> term (Map k a) -> term (Map k b)+	map_lookup       :: Ord k => term k -> term (Map k a) -> term (Maybe a)+	map_keys         :: term (Map k a) -> term [k]+	map_member       :: Ord k => term k -> term (Map k a) -> term Bool+	map_insert       :: Ord k => term k -> term a -> term (Map k a) -> term (Map k a)+	map_delete       :: Ord k => term k -> term (Map k a) -> term (Map k a)+	map_difference   :: Ord k => term (Map k a) -> term (Map k b) -> term (Map k a)+	map_foldrWithKey :: term (k -> a -> b -> b) -> term b -> term (Map k a) -> term b+	+	default map_fromList     :: Sym_Map (UnT term) => Trans term => Ord k => term [(k, a)] -> term (Map k a)+	default map_mapWithKey   :: Sym_Map (UnT term) => Trans term          => term (k -> a -> b) -> term (Map k a) -> term (Map k b)+	default map_lookup       :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term (Maybe a)+	default map_keys         :: Sym_Map (UnT term) => Trans term          => term (Map k a) -> term [k]+	default map_member       :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term Bool+	default map_insert       :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term a -> term (Map k a) -> term (Map k a)+	default map_delete       :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term (Map k a)+	default map_difference   :: Sym_Map (UnT term) => Trans term => Ord k => term (Map k a) -> term (Map k b) -> term (Map k a)+	default map_foldrWithKey :: Sym_Map (UnT term) => Trans term          => term (k -> a -> b -> b) -> term b -> term (Map k a) -> term b+	+	map_fromList     = trans1 map_fromList+	map_mapWithKey   = trans2 map_mapWithKey+	map_lookup       = trans2 map_lookup+	map_keys         = trans1 map_keys+	map_member       = trans2 map_member+	map_insert       = trans3 map_insert+	map_delete       = trans2 map_delete+	map_difference   = trans2 map_difference+	map_foldrWithKey = trans3 map_foldrWithKey++-- Interpreting+instance Sym_Map Eval where+	map_fromList     = eval1 Map.fromList+	map_mapWithKey   = eval2 Map.mapWithKey+	map_lookup       = eval2 Map.lookup+	map_keys         = eval1 Map.keys+	map_member       = eval2 Map.member+	map_insert       = eval3 Map.insert+	map_delete       = eval2 Map.delete+	map_difference   = eval2 Map.difference+	map_foldrWithKey = eval3 Map.foldrWithKey+instance Sym_Map View where+	map_fromList     = view1 "Map.fromList"+	map_mapWithKey   = view2 "Map.mapWithKey"+	map_lookup       = view2 "Map.lookup"+	map_keys         = view1 "Map.keys"+	map_member       = view2 "Map.member"+	map_insert       = view3 "Map.insert"+	map_delete       = view2 "Map.delete"+	map_difference   = view2 "Map.difference"+	map_foldrWithKey = view3 "Map.foldrWithKey"+instance (Sym_Map r1, Sym_Map r2) => Sym_Map (Dup r1 r2) where+	map_fromList     = dup1 @Sym_Map map_fromList+	map_mapWithKey   = dup2 @Sym_Map map_mapWithKey+	map_lookup       = dup2 @Sym_Map map_lookup+	map_keys         = dup1 @Sym_Map map_keys+	map_member       = dup2 @Sym_Map map_member+	map_insert       = dup3 @Sym_Map map_insert+	map_delete       = dup2 @Sym_Map map_delete+	map_difference   = dup2 @Sym_Map map_difference+	map_foldrWithKey = dup3 @Sym_Map map_foldrWithKey++-- Transforming+instance (Sym_Map term, Sym_Lambda term) => Sym_Map (BetaT term)++-- Typing+instance FixityOf Map+instance ClassInstancesFor Map where+	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _k))+	 | Just HRefl <- proj_ConstKiTy @_ @Map c+	 = case () of+		 _ | Just Refl <- proj_Const @Functor     q -> Just Dict+		   | Just Refl <- proj_Const @Foldable    q -> Just Dict+		   | Just Refl <- proj_Const @Traversable q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c k) a))+	 | Just HRefl <- proj_ConstKiTy @_ @Map c+	 = case () of+		 _ | Just Refl <- proj_Const @Eq q+		   , Just Dict <- proveConstraint (tq `tyApp` k)+		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   | Just Refl <- proj_Const @Ord q+		   , Just Dict <- proveConstraint (tq `tyApp` k)+		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   | Just Refl <- proj_Const @Monoid q+		   , Just Dict <- proveConstraint (tyConstLen @(K Ord) @Ord (lenVars k) `tyApp` k) -> Just Dict+		   | Just Refl <- proj_Const @Show q+		   , Just Dict <- proveConstraint (tq `tyApp` k)+		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   | Just Refl <- proj_Const @MonoFunctor q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor Map where+	expandFamFor _c _len f (TyApp _ (TyApp _ c _k) a `TypesS` TypesZ)+	 | Just HRefl <- proj_ConstKi @_ @Element f+	 , Just HRefl <- proj_ConstKiTy @_ @Map c+	 = Just a+	expandFamFor _c _len _fam _as = Nothing++-- Compiling+instance Gram_Term_AtomsFor src ss g Map+instance (Source src, Inj_Sym ss Map) => ModuleFor src ss Map where+	moduleFor = ["Map"] `moduleWhere`+	 [ "delete"       := teMap_delete+	 , "difference"   := teMap_difference+	 , "foldrWithKey" := teMap_foldrWithKey+	 , "fromList"     := teMap_fromList+	 , "insert"       := teMap_insert+	 , "keys"         := teMap_keys+	 , "lookup"       := teMap_lookup+	 , "mapWithKey"   := teMap_mapWithKey+	 , "member"       := teMap_member+	 ]++-- ** 'Type's+tyMap :: Source src => Inj_Len vs => Type src vs k -> Type src vs a -> Type src vs (Map k a)+tyMap k a = tyConst @(K Map) @Map `tyApp` k `tyApp` a++k1 :: Source src => Inj_Len vs => Inj_Kind (K k) =>+     Type src (a ': Proxy k ': vs) k+k1 = tyVar "k" $ VarS varZ++k2 :: Source src => Inj_Len vs => Inj_Kind (K k) =>+     Type src (a ': b ': Proxy k ': vs) k+k2 = tyVar "k" $ VarS $ VarS varZ++-- ** 'Term's+teMap_delete :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Map k a))+teMap_delete = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMap k1 a0) $ teSym @Map $ lam2 map_delete++teMap_insert :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> a -> Map k a -> Map k a))+teMap_insert = Term (tyOrd k1) (k1 ~> a0 ~> tyMap k1 a0 ~> tyMap k1 a0) $ teSym @Map $ lam3 map_insert++teMap_difference :: TermDef Map '[Proxy a, Proxy b, Proxy k] (Ord k #> (Map k a -> Map k b -> Map k a))+teMap_difference = Term (tyOrd k2) (tyMap k2 a0 ~> tyMap k2 b1 ~> tyMap k2 a0) $ teSym @Map $ lam2 map_difference++teMap_fromList :: TermDef Map '[Proxy a, Proxy k] (Ord k #> ([(k, a)] -> Map k a))+teMap_fromList = Term (tyOrd k1) (tyList (tyTuple2 k1 a0) ~> tyMap k1 a0) $ teSym @Map $ lam1 map_fromList++teMap_lookup :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Maybe a))+teMap_lookup = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMaybe a0) $ teSym @Map $ lam2 map_lookup++teMap_member :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Bool))+teMap_member = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyBool) $ teSym @Map $ lam2 map_member++teMap_foldrWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b -> b) -> b -> Map k a -> b))+teMap_foldrWithKey = Term noConstraint ((k2 ~> a0 ~> b1 ~> b1) ~> b1 ~> tyMap k2 a0 ~> b1) $ teSym @Map $ lam3 map_foldrWithKey++teMap_mapWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b) -> Map k a -> Map k b))+teMap_mapWithKey = Term noConstraint ((k2 ~> a0 ~> b1) ~> tyMap k2 a0 ~> tyMap k2 b1) $ teSym @Map $ lam2 map_mapWithKey++teMap_keys :: TermDef Map '[Proxy a, Proxy k] (() #> (Map k a -> [k]))+teMap_keys = Term noConstraint (tyMap k1 a0 ~> tyList k1) $ teSym @Map $ lam1 map_keys
+ Language/Symantic/Lib/Map/Test.hs view
@@ -0,0 +1,44 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module Lib.Map.Test where++import Test.Tasty++import Data.Map.Strict (Map)+import Data.Proxy (Proxy(..))+import Data.Text as Text+import Prelude hiding (zipWith)+import qualified Data.Map.Strict as Map++import Language.Symantic.Lib+import Compiling.Test++type SS =+ [ Proxy (->)+ , Proxy []+ , Proxy Int+ , Proxy Integer+ , Proxy Map+ , Proxy Char+ , Proxy (,)+ , Proxy Num+ , Proxy Monoid+ ]+(==>) = test_readTerm @() @SS++tests :: TestTree+tests = testGroup "Map"+ [ "Map.fromList (zipWith (,) [1, 2, 3] ['a', 'b', 'c'])" ==> Right+	 ( tyMap tyInteger tyChar+	 , Map.fromList [(1, 'a'), (2, 'b'), (3, 'c')]+	 , "Map.fromList (zipWith (\\x0 -> (\\x1 -> (x0, x1))) (1 : 2 : 3 : []) ('a' : 'b' : 'c' : []))" )+ , Text.concat+	[ "Map.foldrWithKey"+	, " (\\(k:Integer) (v:Char) (acc:(Integer,[Char])) ->"+	, "  (k + fst acc, v : snd acc))"+	, " (0, [])"+	, " (Map.fromList (zipWith (,) [1, 2, 3] ['a', 'b', 'c']))"+	] ==> Right+	 ( tyInteger `tyTuple2` tyString+	 , (6, "abc")+	 , "Map.foldrWithKey (\\x0 -> (\\x1 -> (\\x2 -> (x0 + fst x2, x1 : snd x2)))) (0, []) (Map.fromList (zipWith (\\x0 -> (\\x1 -> (x0, x1))) (1 : 2 : 3 : []) ('a' : 'b' : 'c' : [])))" )+ ]
+ Language/Symantic/Lib/Maybe.hs view
@@ -0,0 +1,100 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Maybe'.+module Language.Symantic.Lib.Maybe where++import Control.Monad+import Prelude hiding (maybe)+import qualified Data.Maybe as Maybe+import qualified Data.MonoTraversable as MT++import Language.Symantic+import Language.Symantic.Lib.Function (a0, b1)+import Language.Symantic.Lib.MonoFunctor (Element)++-- * Class 'Sym_Maybe'+type instance Sym (Proxy Maybe) = Sym_Maybe+class Sym_Maybe term where+	_Nothing :: term (Maybe a)+	_Just    :: term a -> term (Maybe a)+	maybe    :: term b -> term (a -> b) -> term (Maybe a) -> term b+	+	default _Nothing :: Sym_Maybe (UnT term) => Trans term => term (Maybe a)+	default _Just    :: Sym_Maybe (UnT term) => Trans term => term a -> term (Maybe a)+	default maybe    :: Sym_Maybe (UnT term) => Trans term => term b -> term (a -> b) -> term (Maybe a) -> term b+	+	_Nothing = trans _Nothing+	_Just    = trans1 _Just+	maybe    = trans3 maybe++-- Interpreting+instance Sym_Maybe Eval where+	_Nothing = Eval  Nothing+	_Just    = eval1 Just+	maybe    = eval3 Maybe.maybe+instance Sym_Maybe View where+	_Nothing = view0 "Nothing"+	_Just    = view1 "Just"+	maybe    = view3 "maybe"+instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (Dup r1 r2) where+	_Nothing = dup0 @Sym_Maybe _Nothing+	_Just    = dup1 @Sym_Maybe _Just+	maybe    = dup3 @Sym_Maybe maybe++-- Transforming+instance (Sym_Maybe term, Sym_Lambda term) => Sym_Maybe (BetaT term)++-- Typing+instance FixityOf Maybe+instance ClassInstancesFor Maybe where+	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)+	 | Just HRefl <- proj_ConstKiTy @_ @Maybe c+	 = case () of+		 _ | Just Refl <- proj_Const @Applicative q -> Just Dict+		   | Just Refl <- proj_Const @Foldable q    -> Just Dict+		   | Just Refl <- proj_Const @Functor q     -> Just Dict+		   | Just Refl <- proj_Const @Monad q       -> Just Dict+		   | Just Refl <- proj_Const @Traversable q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))+	 | Just HRefl <- proj_ConstKiTy @_ @Maybe c+	 = case () of+		 _ | Just Refl <- proj_Const @Eq q+		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   | Just Refl <- proj_Const @Monoid q+		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   | Just Refl <- proj_Const @Show q+		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor Maybe where+	expandFamFor _c _len f (TyApp _ c a `TypesS` TypesZ)+	 | Just HRefl <- proj_ConstKi @_ @Element f+	 , Just HRefl <- proj_ConstKiTy @_ @Maybe c+	 = Just a+	expandFamFor _c _len _fam _as = Nothing++-- Compiling+instance Gram_Term_AtomsFor src ss g Maybe+instance (Source src, Inj_Sym ss Maybe) => ModuleFor src ss Maybe where+	moduleFor = ["Maybe"] `moduleWhere`+	 [ "Nothing" := teMaybe_Nothing+	 , "Just"    := teMaybe_Just+	 , "maybe"   := teMaybe_maybe+	 ]++-- ** 'Type's+tyMaybe :: Source src => Inj_Len vs => Type src vs a -> Type src vs (Maybe a)+tyMaybe = (tyConst @(K Maybe) @Maybe `tyApp`)++-- ** 'Term's+teMaybe_Nothing :: TermDef Maybe '[Proxy a] (() #> Maybe a)+teMaybe_Nothing = Term noConstraint (tyMaybe a0) $ teSym @Maybe $ _Nothing++teMaybe_Just :: TermDef Maybe '[Proxy a] (() #> (a -> Maybe a))+teMaybe_Just = Term noConstraint (a0 ~> tyMaybe a0) $ teSym @Maybe $ lam1 _Just++teMaybe_maybe :: TermDef Maybe '[Proxy a, Proxy b] (() #> (b -> (a -> b) -> Maybe a -> b))+teMaybe_maybe = Term noConstraint (b1 ~> (a0 ~> b1) ~> tyMaybe a0 ~> b1) $ teSym @Maybe $ lam1 $ \b' -> lam $ lam . maybe b'
+ Language/Symantic/Lib/Monad.hs view
@@ -0,0 +1,110 @@+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Monad'.+module Language.Symantic.Lib.Monad where++import Control.Monad (Monad)+import Prelude hiding (Monad(..))+import qualified Control.Monad as Monad++import Language.Symantic+import Language.Symantic.Lib.Function (a0, b1, c2)+import Language.Symantic.Lib.Unit (tyUnit)+import Language.Symantic.Lib.Bool (tyBool)++-- * Class 'Sym_Monad'+type instance Sym (Proxy Monad) = Sym_Monad+class Sym_Monad term where+	return :: Monad m       => term a -> term (m a)+	(>>=)  :: Monad m       => term (m a) -> term (a -> m b) -> term (m b); infixl 1 >>=+	join   :: Monad m       => term (m (m a)) -> term (m a)+	when   :: Applicative f => term Bool -> term (f ()) -> term (f ())+	(>=>)  :: Monad m       => term (a -> m b) -> term (b -> m c) -> term (a -> m c); infixr 1 >=>+	+	default return :: Sym_Monad (UnT term) => Trans term => Monad m       => term a -> term (m a)+	default (>>=)  :: Sym_Monad (UnT term) => Trans term => Monad m       => term (m a) -> term (a -> m b) -> term (m b)+	default join   :: Sym_Monad (UnT term) => Trans term => Monad m       => term (m (m a)) -> term (m a)+	default when   :: Sym_Monad (UnT term) => Trans term => Applicative f => term Bool -> term (f ()) -> term (f ())+	default (>=>)  :: Sym_Monad (UnT term) => Trans term => Monad m       => term (a -> m b) -> term (b -> m c) -> term (a -> m c)+	+	return = trans1 return+	(>>=)  = trans2 (>>=)+	join   = trans1 join+	when   = trans2 when+	(>=>)  = trans2 (>=>)++-- Interpreting+instance Sym_Monad Eval where+	return = eval1 Monad.return+	(>>=)  = eval2 (Monad.>>=)+	join   = eval1 Monad.join+	when   = eval2 Monad.when+	(>=>)  = eval2 (Monad.>=>)+instance Sym_Monad View where+	return = view1 "return"+	(>>=)  = viewInfix ">>=" (infixL 1)+	join   = view1 "join"+	when   = view2 "when"+	(>=>)  = viewInfix ">=>" (infixR 1)+instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (Dup r1 r2) where+	return = dup1 @Sym_Monad return+	(>>=)  = dup2 @Sym_Monad (>>=)+	join   = dup1 @Sym_Monad join+	when   = dup2 @Sym_Monad when+	(>=>)  = dup2 @Sym_Monad (>=>)++-- Transforming+instance (Sym_Monad term, Sym_Lambda term) => Sym_Monad (BetaT term)++-- Typing+instance FixityOf Monad+instance ClassInstancesFor Monad+instance TypeInstancesFor Monad++-- Compiling+instance Gram_Term_AtomsFor src ss g Monad+instance (Source src, Inj_Sym ss Monad) => ModuleFor src ss Monad where+	moduleFor = ["Monad"] `moduleWhere`+	 [ "return" := teMonad_return+	 , "join"   := teMonad_join+	 , "when"   := teMonad_when+	 , ">>=" `withInfixL` 1 := teMonad_bind+	 , ">=>" `withInfixR` 1 := teMonad_kleisli_l2r+	 ]++-- ** 'Type's+tyMonad :: Source src => Type src vs m -> Type src vs (Monad m)+tyMonad m = tyConstLen @(K Monad) @Monad (lenVars m) `tyApp` m++m0 :: Source src => Inj_Len vs => Inj_Kind (K m) =>+     Type src (Proxy m ': vs) m+m0 = tyVar "m" varZ++m1 :: Source src => Inj_Len vs => Inj_Kind (K m) =>+     Type src (a ': Proxy m ': vs) m+m1 = tyVar "m" $ VarS varZ++m2 :: Source src => Inj_Len vs => Inj_Kind (K m) =>+     Type src (a ': b ': Proxy m ': vs) m+m2 = tyVar "m" $ VarS $ VarS varZ++m3 :: Source src => Inj_Len vs => Inj_Kind (K m) =>+     Type src (a ': b ': c ': Proxy m ': vs) m+m3 = tyVar "m" $ VarS $ VarS $ VarS varZ++-- ** 'Term's+teMonad_return :: TermDef Monad '[Proxy a, Proxy m] (Monad m #> (a -> m a))+teMonad_return = Term (tyMonad m1) (a0 ~> m1 `tyApp` a0) $ teSym @Monad $ lam1 return++teMonad_bind :: TermDef Monad '[Proxy a, Proxy b, Proxy m] (Monad m #> (m a -> (a -> m b) -> m b))+teMonad_bind = Term (tyMonad m2) (m2 `tyApp` a0 ~> (a0 ~> m2 `tyApp` b1) ~> m2 `tyApp` b1) $ teSym @Monad $ lam2 (>>=)++teMonad_join :: TermDef Monad '[Proxy a, Proxy m] (Monad m #> (m (m a) -> m a))+teMonad_join = Term (tyMonad m1) (m1 `tyApp` (m1 `tyApp` a0) ~> m1 `tyApp` a0) $ teSym @Monad $ lam1 join++teMonad_kleisli_l2r :: TermDef Monad '[Proxy a, Proxy b, Proxy c, Proxy m] (Monad m #> ((a -> m b) -> (b -> m c) -> (a -> m c)))+teMonad_kleisli_l2r = Term (tyMonad m3) ((a0 ~> m3 `tyApp` b1) ~> (b1 ~> m3 `tyApp` c2) ~> (a0 ~> m3 `tyApp` c2)) $ teSym @Monad $ lam2 (>=>)++teMonad_when :: TermDef Monad '[Proxy m] (Monad m #> (Bool -> m () -> m ()))+teMonad_when = Term (tyMonad m0) (tyBool ~> m0 `tyApp` tyUnit ~> m0 `tyApp` tyUnit) $ teSym @Monad $ lam2 when
+ Language/Symantic/Lib/MonoFoldable.hs view
@@ -0,0 +1,132 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'MonoFoldable'.+module Language.Symantic.Lib.MonoFoldable where++import Data.MonoTraversable (MonoFoldable)+import qualified Data.MonoTraversable as MT++import Language.Symantic+import Language.Symantic.Lib.Bool (tyBool)+import Language.Symantic.Lib.Function ()+import Language.Symantic.Lib.Int (tyInt)+import Language.Symantic.Lib.List (tyList)+import Language.Symantic.Lib.MonoFunctor (famElement, o0, e1)+import Language.Symantic.Lib.Monoid (tyMonoid)++-- * Class 'Sym_MonoFoldable'+type instance Sym (Proxy MonoFoldable) = Sym_MonoFoldable+class Sym_MonoFoldable term where+	ofoldMap :: (MonoFoldable o, Monoid m) => term (MT.Element o -> m) -> term o -> term m+	ofoldr   :: MonoFoldable o => term (MT.Element o -> b -> b) -> term b -> term o -> term b+	ofoldl'  :: MonoFoldable o => term (b -> MT.Element o -> b) -> term b -> term o -> term b+	olength  :: MonoFoldable o => term o -> term Int+	onull    :: MonoFoldable o => term o -> term Bool+	oall     :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool+	oany     :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool+	otoList  :: MonoFoldable o => term o -> term [MT.Element o]+	default ofoldMap :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => Monoid m => term (MT.Element o -> m) -> term o -> term m+	default ofoldr   :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term (MT.Element o -> b -> b) -> term b -> term o -> term b+	default ofoldl'  :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term (b -> MT.Element o -> b) -> term b -> term o -> term b+	default olength  :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term o -> term Int+	default onull    :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term o -> term Bool+	default oall     :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool+	default oany     :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool+	default otoList  :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term o -> term [MT.Element o]+	ofoldMap = trans2 ofoldMap+	ofoldr   = trans3 ofoldr+	ofoldl'  = trans3 ofoldl'+	olength  = trans1 olength+	onull    = trans1 onull+	oall     = trans2 oall+	oany     = trans2 oany+	otoList  = trans1 otoList++-- Interpreting+instance Sym_MonoFoldable Eval where+	ofoldMap = eval2 MT.ofoldMap+	ofoldr   = eval3 MT.ofoldr+	ofoldl'  = eval3 MT.ofoldl'+	olength  = eval1 MT.olength+	onull    = eval1 MT.onull+	oall     = eval2 MT.oall+	oany     = eval2 MT.oany+	otoList  = eval1 MT.otoList+instance Sym_MonoFoldable View where+	ofoldMap = view2 "ofoldMap"+	ofoldr   = view3 "ofoldr"+	ofoldl'  = view3 "ofoldl'"+	olength  = view1 "olength"+	onull    = view1 "onull"+	oall     = view2 "oall"+	oany     = view2 "oany"+	otoList  = view1 "otoList"+instance (Sym_MonoFoldable r1, Sym_MonoFoldable r2) => Sym_MonoFoldable (Dup r1 r2) where+	ofoldMap = dup2 @Sym_MonoFoldable ofoldMap+	ofoldr   = dup3 @Sym_MonoFoldable ofoldr+	ofoldl'  = dup3 @Sym_MonoFoldable ofoldl'+	olength  = dup1 @Sym_MonoFoldable olength+	onull    = dup1 @Sym_MonoFoldable onull+	oall     = dup2 @Sym_MonoFoldable oall+	oany     = dup2 @Sym_MonoFoldable oany+	otoList  = dup1 @Sym_MonoFoldable otoList++-- Transforming+instance (Sym_MonoFoldable term, Sym_Lambda term) => Sym_MonoFoldable (BetaT term)++-- Typing+instance FixityOf MonoFoldable+instance ClassInstancesFor MonoFoldable+instance TypeInstancesFor MonoFoldable++-- Compiling+instance Gram_Term_AtomsFor src ss g MonoFoldable+instance (Source src, Inj_Sym ss MonoFoldable) => ModuleFor src ss MonoFoldable where+	moduleFor = ["MonoFoldable"] `moduleWhere`+	 [ "ofoldMap" := teMonoFoldable_ofoldMap+	 , "otoList"  := teMonoFoldable_otoList+	 , "ofoldr"   := teMonoFoldable_ofoldr+	 , "ofoldl'"  := teMonoFoldable_ofoldl'+	 , "olength"  := teMonoFoldable_olength+	 , "onull"    := teMonoFoldable_onull+	 , "oall"     := teMonoFoldable_oall+	 , "oany"     := teMonoFoldable_oany+	 ]++-- ** 'Type's+tyMonoFoldable :: Source src => Type src vs a -> Type src vs (MonoFoldable a)+tyMonoFoldable a = tyConstLen @(K MonoFoldable) @MonoFoldable (lenVars a) `tyApp` a++-- ** 'Term's+teMonoFoldable_ofoldMap :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy m] (MonoFoldable o # Monoid m # e #~ MT.Element o #> ((e -> m) -> o -> m))+teMonoFoldable_ofoldMap = Term (tyMonoFoldable o0 # tyMonoid m # e1 #~ famElement o0) ((e1 ~> m) ~> o0 ~> m) $ teSym @MonoFoldable $ lam2 ofoldMap+	where+	m :: Source src => Inj_Len vs => Inj_Kind (K m) => Type src (Proxy a ': Proxy b ': Proxy m ': vs) m+	m = tyVar "m" $ VarS $ VarS varZ++teMonoFoldable_otoList :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (o -> [MT.Element o]))+teMonoFoldable_otoList = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (o0 ~> tyList (famElement o0)) $ teSym @MonoFoldable $ lam1 otoList++teMonoFoldable_ofoldr :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy a] (MonoFoldable o # e #~ MT.Element o #> ((e -> a -> a) -> a -> o -> a))+teMonoFoldable_ofoldr = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((e1 ~> a ~> a) ~> a ~> o0 ~> a) $ teSym @MonoFoldable $ lam1 $ \f -> lam $ lam . ofoldr f+	where+	a :: Source src => Inj_Len vs => Inj_Kind (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a+	a = tyVar "a" $ VarS $ VarS varZ++teMonoFoldable_ofoldl' :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy a] (MonoFoldable o # e #~ MT.Element o #> ((a -> e -> a) -> a -> o -> a))+teMonoFoldable_ofoldl' = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((a ~> e1 ~> a) ~> a ~> o0 ~> a) $ teSym @MonoFoldable $ lam1 $ \f -> lam $ lam . ofoldl' f+	where+	a :: Source src => Inj_Len vs => Inj_Kind (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a+	a = tyVar "a" $ VarS $ VarS varZ++teMonoFoldable_olength :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (o -> Int))+teMonoFoldable_olength = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (o0 ~> tyInt) $ teSym @MonoFoldable $ lam1 olength++teMonoFoldable_onull :: TermDef MonoFoldable '[Proxy o] (MonoFoldable o #> (o -> Bool))+teMonoFoldable_onull = Term (tyMonoFoldable o0) (o0 ~> tyBool) $ teSym @MonoFoldable $ lam1 onull++teMonoFoldable_oall :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> ((e -> Bool) -> o -> Bool))+teMonoFoldable_oall = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((e1 ~> tyBool) ~> o0 ~> tyBool) $ teSym @MonoFoldable $ lam2 oall++teMonoFoldable_oany :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> ((e -> Bool) -> o -> Bool))+teMonoFoldable_oany = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((e1 ~> tyBool) ~> o0 ~> tyBool) $ teSym @MonoFoldable $ lam2 oany
+ Language/Symantic/Lib/MonoFunctor.hs view
@@ -0,0 +1,75 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'MonoFunctor'.+module Language.Symantic.Lib.MonoFunctor where++import Data.MonoTraversable (MonoFunctor)+import qualified Data.MonoTraversable as MT++import Language.Symantic+import Language.Symantic.Lib.Function ()++-- * Type 'Element'+data Element+type instance Fam Element '[h] = MT.Element (UnProxy h)+instance ClassInstancesFor Element+instance TypeInstancesFor Element where+	expandFamFor _c _len f (TyApp _ (TyApp _ z _ty_r) a `TypesS` TypesZ)+	 | Just HRefl <- proj_ConstKi @_ @Element f+	 , Just HRefl <- proj_ConstKiTy @_ @(->) z+	 = Just a+	expandFamFor _c _len _fam _as = Nothing++-- ** 'Type's+famElement :: Source src => Type src vs t -> Type src vs (MT.Element t)+famElement o = TyFam noSource (lenVars o) (inj_Const @Element) (o `TypesS` TypesZ)++-- * Class 'Sym_MonoFunctor'+type instance Sym (Proxy MonoFunctor) = Sym_MonoFunctor+class Sym_MonoFunctor term where+	omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o+	default omap+	 :: Sym_MonoFunctor (UnT term)+	 => Trans term+	 => MonoFunctor o+	 => term (MT.Element o -> MT.Element o) -> term o -> term o+	omap = trans2 omap++-- Interpreting+instance Sym_MonoFunctor Eval where+	omap = eval2 MT.omap+instance Sym_MonoFunctor View where+	omap = view2 "omap"+instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (Dup r1 r2) where+	omap = dup2 @Sym_MonoFunctor omap++-- Transforming+instance (Sym_MonoFunctor term, Sym_Lambda term) => Sym_MonoFunctor (BetaT term)++-- Typing+instance FixityOf MonoFunctor+instance ClassInstancesFor MonoFunctor+instance TypeInstancesFor MonoFunctor++-- Compiling+instance Gram_Term_AtomsFor src ss g MonoFunctor+instance (Source src, Inj_Sym ss MonoFunctor) => ModuleFor src ss MonoFunctor where+	moduleFor = ["MonoFunctor"] `moduleWhere`+	 [ "omap" := teMonoFunctor_omap+	 ]++-- ** 'Type's+tyMonoFunctor :: Source src => Type src vs a -> Type src vs (MonoFunctor a)+tyMonoFunctor a = tyConstLen @(K MonoFunctor) @MonoFunctor (lenVars a) `tyApp` a++o0 :: Source src => Inj_Len vs => Inj_Kind (K o) =>+     Type src (Proxy o ': vs) o+o0 = tyVar "o" varZ++e1 :: Source src => Inj_Len vs => Inj_Kind (K e) =>+     Type src (a ': Proxy e ': vs) e+e1 = tyVar "e" $ VarS varZ++-- ** 'Term's+teMonoFunctor_omap :: TermDef MonoFunctor '[Proxy o, Proxy e] (MonoFunctor o # e #~ MT.Element o #> ((e -> e) -> o -> o))+teMonoFunctor_omap = Term (tyMonoFunctor o0 # e1 #~ famElement o0) ((e1 ~> e1) ~> o0 ~> o0) $ teSym @MonoFunctor $ lam2 omap
+ Language/Symantic/Lib/MonoFunctor/Test.hs view
@@ -0,0 +1,28 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module Lib.MonoFunctor.Test where++import Test.Tasty++import Data.Proxy (Proxy(..))+import Prelude hiding (zipWith)+import qualified Data.MonoTraversable as MT++import Language.Symantic.Lib+import Compiling.Test++type SS =+ [ Proxy (->)+ , Proxy []+ , Proxy Integer+ , Proxy Bool+ , Proxy Char+ , Proxy MT.MonoFunctor+ , Proxy Maybe+ ]+(==>) = test_readTerm @() @SS++tests :: TestTree+tests = testGroup "MonoFunctor"+ [ "omap not (Just True)" ==> Right (tyMaybe tyBool, Just False, "omap (\\x0 -> not x0) (Just True)")+ , "omap Char.toUpper ['a', 'b', 'c']" ==> Right (tyList tyChar, "ABC", "omap (\\x0 -> Char.toUpper x0) ('a' : 'b' : 'c' : [])" )+ ]
+ Language/Symantic/Lib/Monoid.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Monoid'.+module Language.Symantic.Lib.Monoid where++import Data.Monoid (Monoid)+import Prelude hiding (Monoid(..))+import qualified Data.Monoid as Monoid++import Language.Symantic+import Language.Symantic.Lib.Function (a0)++-- * Class 'Sym_Monoid'+type instance Sym (Proxy Monoid) = Sym_Monoid+class Sym_Monoid term where+	mempty  :: Monoid a => term a+	mappend :: Monoid a => term a -> term a -> term a+	default mempty  :: Sym_Monoid (UnT term) => Trans term => Monoid a => term a+	default mappend :: Sym_Monoid (UnT term) => Trans term => Monoid a => term a -> term a -> term a+	mempty  = trans mempty+	mappend = trans2 mappend++-- Interpreting+instance Sym_Monoid Eval where+	mempty  = Eval  Monoid.mempty+	mappend = eval2 Monoid.mappend+instance Sym_Monoid View where+	mempty  = view0 "mempty"+	mappend = view2 "mappend"+instance (Sym_Monoid r1, Sym_Monoid r2) => Sym_Monoid (Dup r1 r2) where+	mempty  = dup0 @Sym_Monoid mempty+	mappend = dup2 @Sym_Monoid mappend++-- Transforming+instance (Sym_Monoid term, Sym_Lambda term) => Sym_Monoid (BetaT term)++-- Typing+instance FixityOf Monoid+instance ClassInstancesFor Monoid+instance TypeInstancesFor Monoid++-- Compiling+instance Gram_Term_AtomsFor src ss g Monoid+instance (Source src, Inj_Sym ss Monoid) => ModuleFor src ss Monoid where+	moduleFor = ["Monoid"] `moduleWhere`+	 [ "mempty"  := teMonoid_mempty+	 , "mappend" := teMonoid_mappend+	 ]++-- ** 'Type's+tyMonoid :: Source src => Type src vs a -> Type src vs (Monoid a)+tyMonoid a = tyConstLen @(K Monoid) @Monoid (lenVars a) `tyApp` a++-- ** 'Term's+teMonoid_mempty :: TermDef Monoid '[Proxy a] (Monoid a #> a)+teMonoid_mempty = Term (tyMonoid a0) a0 $ teSym @Monoid $ mempty++teMonoid_mappend :: TermDef Monoid '[Proxy a] (Monoid a #> (a -> a -> a))+teMonoid_mappend = Term (tyMonoid a0) (a0 ~> a0 ~> a0) $ teSym @Monoid $ lam2 mappend
+ Language/Symantic/Lib/NonNull.hs view
@@ -0,0 +1,155 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'NonNull'.+module Language.Symantic.Lib.NonNull where++import Data.MonoTraversable (MonoFoldable)+import Data.NonNull (NonNull)+import Data.Sequences (IsSequence, SemiSequence)+import Prelude hiding (head, init, last, tail)+import qualified Data.MonoTraversable as MT+import qualified Data.NonNull as NonNull++import Language.Symantic+import Language.Symantic.Lib.Bool (tyBool)+import Language.Symantic.Lib.Maybe (tyMaybe)+import Language.Symantic.Lib.MonoFoldable (tyMonoFoldable)+import Language.Symantic.Lib.MonoFunctor (Element, famElement, o0, e1)+import Language.Symantic.Lib.Sequences (tySemiSequence, tyIsSequence, s0)+import Language.Symantic.Lib.Tuple2 (tyTuple2)++-- * Class 'Sym_NonNull'+type instance Sym (Proxy NonNull) = Sym_NonNull+class Sym_NonNull term where+	fromNullable :: MonoFoldable o => term o -> term (Maybe (NonNull o))+	toNullable   :: MonoFoldable o => term (NonNull o) -> term o+	ncons        :: SemiSequence s => term (MT.Element s) -> term s -> term (NonNull s)+	nuncons      :: IsSequence s   => term (NonNull s) -> term (MT.Element s, Maybe (NonNull s))+	head         :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)+	last         :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)+	tail         :: IsSequence s   => term (NonNull s) -> term s+	init         :: IsSequence s   => term (NonNull s) -> term s+	nfilter      :: IsSequence s   => term (MT.Element s -> Bool) -> term (NonNull s) -> term s+	default fromNullable :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term o -> term (Maybe (NonNull o))+	default toNullable   :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term (NonNull o) -> term o+	default ncons        :: Sym_NonNull (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term (NonNull s)+	default nuncons      :: Sym_NonNull (UnT term) => Trans term => IsSequence s   => term (NonNull s) -> term (MT.Element s, Maybe (NonNull s))+	default head         :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term (NonNull o) -> term (MT.Element o)+	default last         :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term (NonNull o) -> term (MT.Element o)+	default tail         :: Sym_NonNull (UnT term) => Trans term => IsSequence s   => term (NonNull s) -> term s+	default init         :: Sym_NonNull (UnT term) => Trans term => IsSequence s   => term (NonNull s) -> term s+	default nfilter      :: Sym_NonNull (UnT term) => Trans term => IsSequence s   => term (MT.Element s -> Bool) -> term (NonNull s) -> term s+	fromNullable = trans1 fromNullable+	toNullable   = trans1 toNullable+	ncons        = trans2 ncons+	nuncons      = trans1 nuncons+	head         = trans1 head+	last         = trans1 last+	tail         = trans1 tail+	init         = trans1 init+	nfilter      = trans2 nfilter++-- Interpreting+instance Sym_NonNull Eval where+	fromNullable = eval1 NonNull.fromNullable+	toNullable   = eval1 NonNull.toNullable+	ncons        = eval2 NonNull.ncons+	nuncons      = eval1 NonNull.nuncons+	head         = eval1 NonNull.head+	last         = eval1 NonNull.last+	tail         = eval1 NonNull.tail+	init         = eval1 NonNull.init+	nfilter      = eval2 NonNull.nfilter+instance Sym_NonNull View where+	fromNullable = view1 "fromNullable"+	toNullable   = view1 "toNullable"+	ncons        = view2 "ncons"+	nuncons      = view1 "nuncons"+	head         = view1 "head"+	last         = view1 "last"+	tail         = view1 "tail"+	init         = view1 "init"+	nfilter      = view2 "nfilter"+instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (Dup r1 r2) where+	fromNullable = dup1 @Sym_NonNull fromNullable+	toNullable   = dup1 @Sym_NonNull toNullable+	ncons        = dup2 @Sym_NonNull ncons+	nuncons      = dup1 @Sym_NonNull nuncons+	head         = dup1 @Sym_NonNull head+	last         = dup1 @Sym_NonNull last+	tail         = dup1 @Sym_NonNull tail+	init         = dup1 @Sym_NonNull init+	nfilter      = dup2 @Sym_NonNull nfilter++-- Transforming+instance (Sym_NonNull term, Sym_Lambda term) => Sym_NonNull (BetaT term)++-- Typing+instance FixityOf NonNull+instance TypeInstancesFor NonNull where+	expandFamFor c len f (TyApp _ z o `TypesS` TypesZ)+	 | Just HRefl <- proj_ConstKi @_ @Element f+	 , Just HRefl <- proj_ConstKiTy @_ @NonNull z+	 = expandFamFor c len f (o `TypesS` TypesZ)+	expandFamFor _c _len _fam _as = Nothing+instance ClassInstancesFor NonNull where+	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c o))+	 | Just HRefl <- proj_ConstKiTy @_ @NonNull c+	 = case () of+		 _ | Just Refl <- proj_Const @Eq q+		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFoldable q+		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFunctor q+		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict+		   | Just Refl <- proj_Const @Ord q+		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict+		   | Just Refl <- proj_Const @SemiSequence q+		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict+		   | Just Refl <- proj_Const @Show q+		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing++-- Compiling+instance Gram_Term_AtomsFor src ss g NonNull+instance (Source src, Inj_Sym ss NonNull) => ModuleFor src ss NonNull where+	moduleFor = ["NonNull"] `moduleWhere`+	 [ "fromNullable" := teNonNull_fromNullable+	 , "toNullable"   := teNonNull_toNullable+	 , "ncons"        := teNonNull_ncons+	 , "nuncons"      := teNonNull_nuncons+	 , "head"         := teNonNull_head+	 , "last"         := teNonNull_last+	 , "tail"         := teNonNull_tail+	 , "init"         := teNonNull_init+	 , "nfilter"      := teNonNull_nfilter+	 ]++-- ** 'Type's+tyNonNull :: Source src => Type src vs a -> Type src vs (NonNull a)+tyNonNull a = tyConstLen @(K NonNull) @NonNull (lenVars a) `tyApp` a++-- ** 'Term's+teNonNull_fromNullable :: TermDef NonNull '[Proxy o] (MonoFoldable o #> (o -> Maybe (NonNull o)))+teNonNull_fromNullable = Term (tyMonoFoldable o0) (o0 ~> tyMaybe (tyNonNull o0)) $ teSym @NonNull $ lam1 fromNullable++teNonNull_toNullable :: TermDef NonNull '[Proxy o] (MonoFoldable o #> (NonNull o -> o))+teNonNull_toNullable = Term (tyMonoFoldable o0) (tyNonNull o0 ~> o0) $ teSym @NonNull $ lam1 toNullable++teNonNull_ncons :: TermDef NonNull '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (e -> s -> NonNull s))+teNonNull_ncons = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> tyNonNull s0) $ teSym @NonNull $ lam2 ncons++teNonNull_nuncons :: TermDef NonNull '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> (NonNull s -> (e, Maybe (NonNull s))))+teNonNull_nuncons = Term (tyIsSequence s0 # e1 #~ famElement s0) (tyNonNull s0 ~> e1 `tyTuple2` tyMaybe (tyNonNull s0)) $ teSym @NonNull $ lam1 nuncons++teNonNull_nfilter :: TermDef NonNull '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> ((e -> Bool) -> NonNull s -> s))+teNonNull_nfilter = Term (tyIsSequence s0 # e1 #~ famElement s0) ((e1 ~> tyBool) ~> tyNonNull s0 ~> s0) $ teSym @NonNull $ lam2 nfilter++teNonNull_head, teNonNull_last :: TermDef NonNull '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (NonNull o -> e))+teNonNull_head = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (tyNonNull o0 ~> e1) $ teSym @NonNull $ lam1 head+teNonNull_last = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (tyNonNull o0 ~> e1) $ teSym @NonNull $ lam1 head++teNonNull_tail, teNonNull_init :: TermDef NonNull '[Proxy s] (IsSequence s #> (NonNull s -> s))+teNonNull_tail = Term (tyIsSequence s0) (tyNonNull s0 ~> s0) $ teSym @NonNull $ lam1 tail+teNonNull_init = Term (tyIsSequence s0) (tyNonNull s0 ~> s0) $ teSym @NonNull $ lam1 init
+ Language/Symantic/Lib/Num.hs view
@@ -0,0 +1,105 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Num'.+module Language.Symantic.Lib.Num where++import Prelude (Num)+import Prelude hiding (Num(..))+import qualified Prelude++import Language.Symantic+import Language.Symantic.Lib.Function (a0)+import Language.Symantic.Lib.Integer (tyInteger)++-- * Class 'Sym_Num'+type instance Sym (Proxy Num) = Sym_Num+class Sym_Num term where+	abs         :: Num n => term n -> term n+	negate      :: Num n => term n -> term n+	signum      :: Num n => term n -> term n+	(+)         :: Num n => term n -> term n -> term n; infixl 6 ++	(-)         :: Num n => term n -> term n -> term n; infixl 6 -+	(*)         :: Num n => term n -> term n -> term n; infixl 7 *+	fromInteger :: Num n => term Integer -> term n+	+	default abs         :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n+	default negate      :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n+	default signum      :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n+	default (+)         :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n -> term n+	default (-)         :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n -> term n+	default (*)         :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n -> term n+	default fromInteger :: Sym_Num (UnT term) => Trans term => Num n => term Integer -> term n+	+	abs         = trans1 abs+	negate      = trans1 negate+	signum      = trans1 signum+	(+)         = trans2 (+)+	(-)         = trans2 (-)+	(*)         = trans2 (*)+	fromInteger = trans1 fromInteger++-- Interpreting+instance Sym_Num Eval where+	abs         = eval1 Prelude.abs+	negate      = eval1 Prelude.negate+	signum      = eval1 Prelude.signum+	(+)         = eval2 (Prelude.+)+	(-)         = eval2 (Prelude.-)+	(*)         = eval2 (Prelude.*)+	fromInteger = eval1 Prelude.fromInteger+instance Sym_Num View where+	abs         = view1 "abs"+	negate      = view1 "negate"+	signum      = view1 "signum"+	(+)         = viewInfix "+" (infixB SideL 6)+	(-)         = viewInfix "-" (infixL 6)+	(*)         = viewInfix "*" (infixB SideL 7)+	fromInteger = view1 "fromInteger"+instance (Sym_Num r1, Sym_Num r2) => Sym_Num (Dup r1 r2) where+	abs         = dup1 @Sym_Num abs+	negate      = dup1 @Sym_Num negate+	signum      = dup1 @Sym_Num signum+	(+)         = dup2 @Sym_Num (+)+	(-)         = dup2 @Sym_Num (-)+	(*)         = dup2 @Sym_Num (*)+	fromInteger = dup1 @Sym_Num fromInteger++-- Transforming+instance (Sym_Num term, Sym_Lambda term) => Sym_Num (BetaT term)++-- Typing+instance FixityOf Num+instance ClassInstancesFor Num+instance TypeInstancesFor Num++-- Compiling+instance Gram_Term_AtomsFor src ss g Num+instance (Source src, Inj_Sym ss Num) => ModuleFor src ss Num where+	moduleFor = ["Num"] `moduleWhere`+	 [ "abs"    := teNum_abs+	 , "negate" := teNum_negate+	 , "signum" := teNum_signum+	 , "+" `withInfixB` (SideL, 6) := teNum_add+	 , "-" `withInfixL` 6          := teNum_sub+	 , "-" `withPrefix` 10         := teNum_negate+	 , "*" `withInfixB` (SideL, 7) := teNum_mul+	 , "fromInteger" := teNum_fromInteger+	 ]++-- ** 'Type's+tyNum :: Source src => Type src vs a -> Type src vs (Num a)+tyNum a = tyConstLen @(K Num) @Num (lenVars a) `tyApp` a++-- ** 'Term's+teNum_fromInteger :: TermDef Num '[Proxy a] (Num a #> (Integer -> a))+teNum_fromInteger = Term (tyNum a0) (tyInteger ~> a0) $ teSym @Num $ lam1 fromInteger++teNum_abs, teNum_negate, teNum_signum :: TermDef Num '[Proxy a] (Num a #> (a -> a))+teNum_abs = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 abs+teNum_negate = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 negate+teNum_signum = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 signum++teNum_add, teNum_sub, teNum_mul :: TermDef Num '[Proxy a] (Num a #> (a -> a -> a))+teNum_add = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (+)+teNum_sub = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (-)+teNum_mul = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (*)
+ Language/Symantic/Lib/Num/Test.hs view
@@ -0,0 +1,96 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Lib.Num.Test where++import Test.Tasty++import Prelude (Num)+import Prelude hiding (Num(..))++import Language.Symantic+import Language.Symantic.Lib+import Compiling.Test++-- * Tests+type SS =+ [ Proxy (->)+ , Proxy Integer+ , Proxy Num+ , Proxy Num2+ , Proxy Int+ , Proxy Integral+ , Proxy Foldable+ , Proxy Traversable+ , Proxy []+ ]+(==>) = test_readTerm @() @SS++tests :: TestTree+tests = testGroup "Num"+ [ "42"                        ==> Right (tyInteger,  42, "42")+ , "-42"                       ==> Right (tyInteger, -42, "negate 42")+ , "- -42"                     ==> Right (tyInteger,  42, "negate (negate 42)")+ , "1 + -2"                    ==> Right (tyInteger,  -1, "1 + negate 2")+ , "-1 + -2"                   ==> Right (tyInteger,  -3, "negate 1 + negate 2")+ , "-(1 + -2)"                 ==> Right (tyInteger,   1, "negate (1 + negate 2)")+ , "(+) 1 2"                   ==> Right (tyInteger,   3, "1 + 2")+ , "1 + 2"                     ==> Right (tyInteger,   3, "1 + 2")+ , "1 + 2 - 3"                 ==> Right (tyInteger,   0, "1 + 2 - 3")+ , "1 + 2 * 3"                 ==> Right (tyInteger,   7, "1 + 2 * 3")+ , "3 * 2 + 1"                 ==> Right (tyInteger,   7, "3 * 2 + 1")+ , "3 * (2 + 1)"               ==> Right (tyInteger,   9, "3 * (2 + 1)")+ , "4 + 3 * 2 + 1"             ==> Right (tyInteger,  11, "4 + 3 * 2 + 1")+ , "5 * 4 + 3 * 2 + 1"         ==> Right (tyInteger,  27, "5 * 4 + 3 * 2 + 1")+ , "negate`42"                 ==> Right (tyInteger, -42, "negate 42")+ , "42`negate"                 ==> Right (tyInteger, -42, "negate 42")+ , "42`negate "                ==> Right (tyInteger, -42, "negate 42")+ , "42`negate`negate"          ==> Right (tyInteger,  42, "negate (negate 42)")+ , "42`abs`negate"             ==> Right (tyInteger, -42, "negate (abs 42)")+ , "42`negate`abs"             ==> Right (tyInteger,  42, "abs (negate 42)")+ , "abs`negate`42"             ==> Right (tyInteger,  42, "abs (negate 42)")+ , "negate`abs`42"             ==> Right (tyInteger, -42, "negate (abs 42)")+ , "negate`abs`42`mod`9"       ==> Right (tyInteger,   3, "negate (abs 42) `mod` 9")+ , "negate abs`42"             ==> Right (tyInteger, -42, "negate (abs 42)")+ , "negate 42`abs"             ==> Right (tyInteger, -42, "negate (abs 42)")+ , "(+) negate`2 44"           ==> Right (tyInteger,  42, "negate 2 + 44")+ , "(+) 2`negate 44"           ==> Right (tyInteger,  42, "negate 2 + 44")+ , "(+) (negate`2) 44"         ==> Right (tyInteger,  42, "negate 2 + 44")+ , "abs negate`42"             ==> Right (tyInteger,  42, "abs (negate 42)")+ , "(+) 40 2"                  ==> Right (tyInteger,  42, "40 + 2")+ , "(+) 40 -2"                 ==> Right (tyInteger,  38, "40 + negate 2")+ , "negate 42 + 42`negate"     ==> Right (tyInteger, -84, "negate 42 + negate 42")+ , "(+) (negate 42) 42`negate" ==> Right (tyInteger, -84, "negate 42 + negate 42")+ , "(+) negate`42 42`negate"   ==> Right (tyInteger, -84, "negate 42 + negate 42")+ , "42`abs`negate`mod`abs`negate`9" ==> Right (tyInteger, 3, "negate (abs 42) `mod` abs (negate 9)")+ , "abs`42`negate"             ==> Right (tyInteger,  42, "abs (negate 42)")+ , "negate`42`abs"             ==> Right (tyInteger,  42, "abs (negate 42)")+ , testGroup "Error_Term"+	 [ "(+) 40 - 2" ==> Left (tyInteger,+		Right $ Error_Term_Beta $ Error_Beta_Unify $+		Error_Unify_Const_mismatch+		 (TypeVT $ tyFun @_ @'[])+		 (TypeVT $ tyInteger @_ @'[]))+	 ]+ ]++-- | A newtype to test prefix and postfix.+newtype Num2 a = Num2 a+type instance Sym (Proxy Num2) = Sym_Num2+class Sym_Num2 (term:: * -> *) where++instance Sym_Num2 Eval where+instance Sym_Num2 View where+instance Sym_Num2 (Dup r1 r2) where+instance Sym_Num2 term => Sym_Num2 (BetaT term) where+instance FixityOf Num2+instance ClassInstancesFor Num2+instance TypeInstancesFor Num2+instance Gram_Term_AtomsFor src ss g Num2+instance (Source src, Inj_Sym ss Num) => ModuleFor src ss Num2 where+	moduleFor = ["Num2"] `moduleWhere`+	 [ "abs"    `withPrefix`   9 := teNum_abs+	 , "negate" `withPrefix`  10 := teNum_negate+	 , "abs"    `withPostfix`  9 := teNum_abs+	 , "negate" `withPostfix` 10 := teNum_negate+	 ]
+ Language/Symantic/Lib/Ord.hs view
@@ -0,0 +1,154 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Ord'.+module Language.Symantic.Lib.Ord where++import Data.Ord (Ord)+import Prelude hiding (Ord(..))+import qualified Data.Ord as Ord+import qualified Data.Text as Text++import Language.Symantic+import Language.Symantic.Lib.Bool (tyBool)+import Language.Symantic.Lib.Function (a0)+import Language.Symantic.Lib.Eq (Sym_Eq)++-- * Class 'Sym_Ordering'+type instance Sym (Proxy Ordering) = Sym_Ordering+class Sym_Eq term => Sym_Ordering term where+	ordering :: Ordering -> term Ordering+	default ordering :: Sym_Ordering (UnT term) => Trans term => Ordering -> term Ordering+	ordering = trans . ordering++-- Interpreting+instance Sym_Ordering Eval where+	ordering = Eval+instance Sym_Ordering View where+	ordering o = View $ \_p _v ->+		Text.pack (show o)+instance (Sym_Ordering r1, Sym_Ordering r2) => Sym_Ordering (Dup r1 r2) where+	ordering o = ordering o `Dup` ordering o++-- Transforming+instance (Sym_Ordering term, Sym_Lambda term) => Sym_Ordering (BetaT term)++-- Typing+instance ClassInstancesFor Ordering+instance TypeInstancesFor Ordering++-- Compiling+instance Gram_Term_AtomsFor src ss g Ordering+instance (Source src, Inj_Sym ss Ordering) => ModuleFor src ss Ordering where+	moduleFor = [] `moduleWhere`+	 [ "LT" := teOrdering LT+	 , "EQ" := teOrdering EQ+	 , "GT" := teOrdering GT+	 ]++-- ** 'Type's+tyOrdering :: Source src => Inj_Len vs => Type src vs Ordering+tyOrdering = tyConst @(K Ordering) @Ordering++-- ** 'Term's+teOrdering :: Source src => Inj_Sym ss Ordering => Ordering -> Term src ss ts '[] (() #> Ordering)+teOrdering o = Term noConstraint tyOrdering $ teSym @Ordering $ ordering o++-- * Class 'Sym_Ord'+type instance Sym (Proxy Ord) = Sym_Ord+class Sym_Eq term => Sym_Ord term where+	compare  :: Ord a => term a -> term a -> term Ordering+	(<)      :: Ord a => term a -> term a -> term Bool; infix 4 <+	(<=)     :: Ord a => term a -> term a -> term Bool; infix 4 <=+	(>)      :: Ord a => term a -> term a -> term Bool; infix 4 >+	(>=)     :: Ord a => term a -> term a -> term Bool; infix 4 >=+	max      :: Ord a => term a -> term a -> term a+	min      :: Ord a => term a -> term a -> term a+	+	default compare  :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Ordering+	default (<)      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool+	default (<=)     :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool+	default (>)      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool+	default (>=)     :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool+	default max      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a+	default min      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a+	+	compare  = trans2 compare+	(<)      = trans2 (<)+	(<=)     = trans2 (<=)+	(>)      = trans2 (>)+	(>=)     = trans2 (>=)+	min      = trans2 min+	max      = trans2 max++-- Interpreting+instance Sym_Ord Eval where+	compare  = eval2 Ord.compare+	(<)      = eval2 (Ord.<)+	(<=)     = eval2 (Ord.<=)+	(>)      = eval2 (Ord.>)+	(>=)     = eval2 (Ord.>=)+	min      = eval2 Ord.min+	max      = eval2 Ord.max+instance Sym_Ord View where+	compare  = view2 "compare"+	(<)      = viewInfix "<"  (infixN 4)+	(<=)     = viewInfix "<=" (infixN 4)+	(>)      = viewInfix ">"  (infixN 4)+	(>=)     = viewInfix ">=" (infixN 4)+	min      = view2 "min"+	max      = view2 "max"+instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (Dup r1 r2) where+	compare    = dup2 @Sym_Ord compare+	(<)        = dup2 @Sym_Ord (<)+	(<=)       = dup2 @Sym_Ord (<=)+	(>)        = dup2 @Sym_Ord (>)+	(>=)       = dup2 @Sym_Ord (>=)+	min        = dup2 @Sym_Ord min+	max        = dup2 @Sym_Ord max++-- Transforming+instance (Sym_Ord term, Sym_Lambda term) => Sym_Ord (BetaT term)++-- Typing+instance FixityOf Ord+instance ClassInstancesFor Ord where+	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)+	 | Just HRefl <- proj_ConstKiTy @_ @Ordering z+	 = case () of+		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict+		   | Just Refl <- proj_Const @Enum    q -> Just Dict+		   | Just Refl <- proj_Const @Eq      q -> Just Dict+		   | Just Refl <- proj_Const @Ord     q -> Just Dict+		   | Just Refl <- proj_Const @Show    q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor Ord++-- Compiling+instance Gram_Term_AtomsFor src ss g Ord+instance (Source src, Inj_Sym ss Ord) => ModuleFor src ss Ord where+	moduleFor = ["Ord"] `moduleWhere`+	 [ "compare" := teOrd_compare+	 , "<"  `withInfixN` 4 := teOrd_lt+	 , "<=" `withInfixN` 4 := teOrd_le+	 , ">"  `withInfixN` 4 := teOrd_gt+	 , ">=" `withInfixN` 4 := teOrd_ge+	 ]++-- ** 'Type's+tyOrd :: Source src => Type src vs a -> Type src vs (Ord a)+tyOrd a = tyConstLen @(K Ord) @Ord (lenVars a) `tyApp` a++-- ** 'Term's+teOrd_compare :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Ordering))+teOrd_compare = Term (tyOrd a0) (a0 ~> a0 ~> tyOrdering) $ teSym @Ord $ lam2 compare++teOrd_le, teOrd_lt, teOrd_ge, teOrd_gt :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Bool))+teOrd_le = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<=)+teOrd_lt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<)+teOrd_ge = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>=)+teOrd_gt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>)++teOrd_min, teOrd_max :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> a))+teOrd_min = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 min+teOrd_max = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 max
+ Language/Symantic/Lib/Ratio.hs view
@@ -0,0 +1,88 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Ratio'.+module Language.Symantic.Lib.Ratio where++import Data.Ratio (Ratio)+import qualified Data.Ratio as Ratio++import Language.Symantic+import Language.Symantic.Lib.Function (a0)+import Language.Symantic.Lib.Integral (tyIntegral)++-- * Class 'Sym_Ratio'+type instance Sym (Proxy Ratio) = Sym_Ratio+class Sym_Ratio term where+	ratio       :: Integral a => term a -> term a -> term (Ratio a)+	numerator   :: term (Ratio a) -> term a+	denominator :: term (Ratio a) -> term a+	+	default ratio       :: Sym_Ratio (UnT term) => Trans term => Integral a => term a -> term a -> term (Ratio a)+	default numerator   :: Sym_Ratio (UnT term) => Trans term               => term (Ratio a) -> term a+	default denominator :: Sym_Ratio (UnT term) => Trans term               => term (Ratio a) -> term a+	+	ratio       = trans2 ratio+	numerator   = trans1 numerator+	denominator = trans1 denominator++-- Interpreting+instance Sym_Ratio Eval where+	ratio       = eval2 (Ratio.%)+	numerator   = eval1 Ratio.numerator+	denominator = eval1 Ratio.denominator+instance Sym_Ratio View where+	ratio       = viewInfix "ratio" (infixL 7)+	numerator   = view1 "numerator"+	denominator = view1 "denominator"+instance (Sym_Ratio r1, Sym_Ratio r2) => Sym_Ratio (Dup r1 r2) where+	ratio       = dup2 @Sym_Ratio ratio+	numerator   = dup1 @Sym_Ratio numerator+	denominator = dup1 @Sym_Ratio denominator++-- Transforming+instance (Sym_Ratio term, Sym_Lambda term) => Sym_Ratio (BetaT term)++-- Typing+instance FixityOf Ratio+instance ClassInstancesFor Ratio where+	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))+	 | Just HRefl <- proj_ConstKiTy @_ @Ratio c+	 = case () of+		 _ | Just Refl <- proj_Const @Eq q+		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   | Just Refl <- proj_Const @Show q+		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   | Just Refl <- proj_Const @Real q+		   , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict+		   | Just Refl <- proj_Const @Ord q+		   , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict+		   | Just Refl <- proj_Const @Fractional q+		   , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict+		   | Just Refl <- proj_Const @Num q+		   , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict+		   | Just Refl <- proj_Const @RealFrac q+		   , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor Ratio++-- Compiling+instance Gram_Term_AtomsFor src ss g Ratio+instance (Source src, Inj_Sym ss Ratio) => ModuleFor src ss Ratio where+	moduleFor = ["Ratio"] `moduleWhere`+	 [ "ratio"       := teRatio+	 , "numerator"   := teRatio_numerator+	 , "denominator" := teRatio_denominator+	 ]++-- ** 'Type's+tyRatio :: Source src => Type src vs a -> Type src vs (Ratio a)+tyRatio a = tyConstLen @(K Ratio) @Ratio (lenVars a) `tyApp` a++-- ** 'Term's+teRatio :: TermDef Ratio '[Proxy a] (Integral a #> (a -> a -> Ratio a))+teRatio = Term (tyIntegral a0) (a0 ~> a0 ~> tyRatio a0) $ teSym @Ratio $ lam2 ratio++teRatio_numerator, teRatio_denominator :: TermDef Ratio '[Proxy a] (() #> (Ratio a -> a))+teRatio_numerator   = Term noConstraint (tyRatio a0 ~> a0) $ teSym @Ratio $ lam1 numerator+teRatio_denominator = Term noConstraint (tyRatio a0 ~> a0) $ teSym @Ratio $ lam1 denominator
+ Language/Symantic/Lib/Real.hs view
@@ -0,0 +1,54 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Real'.+module Language.Symantic.Lib.Real where++import Prelude (Real)+import Prelude hiding (Real(..))+import qualified Prelude++import Language.Symantic+import Language.Symantic.Lib.Function (a0)+import Language.Symantic.Lib.Integer (tyInteger)+import Language.Symantic.Lib.Ratio (tyRatio)++-- * Class 'Sym_Real'+type instance Sym (Proxy Real) = Sym_Real+class Sym_Real term where+	toRational :: Real a => term a -> term Rational+	default toRational :: Sym_Real (UnT term) => Trans term => Real a => term a -> term Rational+	toRational = trans1 toRational++-- Interpreting+instance Sym_Real Eval where+	toRational = eval1 Prelude.toRational+instance Sym_Real View where+	toRational = view1 "toRational"+instance (Sym_Real r1, Sym_Real r2) => Sym_Real (Dup r1 r2) where+	toRational = dup1 @Sym_Real toRational++-- Transforming+instance (Sym_Real term, Sym_Lambda term) => Sym_Real (BetaT term)++-- Typing+instance FixityOf Real+instance ClassInstancesFor Real+instance TypeInstancesFor Real++-- Compiling+instance Gram_Term_AtomsFor src ss g Real+instance (Source src, Inj_Sym ss Real) => ModuleFor src ss Real where+	moduleFor = ["Real"] `moduleWhere`+	 [ "toRational" := teReal_toRational+	 ]++-- ** 'Type's+tyReal :: Source src => Type src vs a -> Type src vs (Real a)+tyReal a = tyConstLen @(K Real) @Real (lenVars a) `tyApp` a++tyRational :: Source src => Inj_Len vs => Type src vs Rational+tyRational = tyRatio tyInteger++-- ** 'Term's+teReal_toRational :: TermDef Real '[Proxy a] (Real a #> (a -> Rational))+teReal_toRational = Term (tyReal a0) (a0 ~> tyRational) $ teSym @Real $ lam1 toRational
+ Language/Symantic/Lib/Semigroup.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Semigroup'.+module Language.Symantic.Lib.Semigroup where++import Data.Semigroup (Semigroup)+import qualified Data.Semigroup as Semigroup++import Language.Symantic+import Language.Symantic.Lib.Function (a0, b1)+import Language.Symantic.Lib.Integral (tyIntegral)++-- * Class 'Sym_Semigroup'+type instance Sym (Proxy Semigroup) = Sym_Semigroup+class Sym_Semigroup term where+	(<>)   :: Semigroup a => term a -> term a -> term a+	stimes :: (Semigroup a, Integral b) => term b -> term a -> term a+	-- sconcat :: NonEmpty a -> a+	default (<>)   :: Sym_Semigroup (UnT term) => Trans term => Semigroup a => term a -> term a -> term a+	default stimes :: Sym_Semigroup (UnT term) => Trans term => Semigroup a => Integral b => term b -> term a -> term a+	(<>)   = trans2 (<>)+	stimes = trans2 stimes++-- Interpreting+instance Sym_Semigroup Eval where+	(<>)   = eval2 (Semigroup.<>)+	stimes = eval2 Semigroup.stimes+instance Sym_Semigroup View where+	(<>)   = viewInfix "-" (infixR 6)+	stimes = view2 "stimes"+instance (Sym_Semigroup r1, Sym_Semigroup r2) => Sym_Semigroup (Dup r1 r2) where+	(<>)   = dup2 @Sym_Semigroup (<>)+	stimes = dup2 @Sym_Semigroup stimes++-- Transforming+instance (Sym_Semigroup term, Sym_Lambda term) => Sym_Semigroup (BetaT term)++-- Typing+instance FixityOf Semigroup+instance ClassInstancesFor Semigroup+instance TypeInstancesFor Semigroup++-- Compiling+instance Gram_Term_AtomsFor src ss g Semigroup+instance (Source src, Inj_Sym ss Semigroup) => ModuleFor src ss Semigroup where+	moduleFor = ["Semigroup"] `moduleWhere`+	 [ "<>" `withInfixR` 6 := teSemigroup_sappend+	 , "stimes" := teSemigroup_stimes+	 ]++-- ** 'Type's+tySemigroup :: Source src => Type src vs a -> Type src vs (Semigroup a)+tySemigroup a = tyConstLen @(K Semigroup) @Semigroup (lenVars a) `tyApp` a++-- ** 'Term's+teSemigroup_sappend :: TermDef Semigroup '[Proxy a] (Semigroup a #> (a -> a -> a))+teSemigroup_sappend = Term (tySemigroup a0) (a0 ~> a0 ~> a0) $ teSym @Semigroup $ lam2 (<>)++teSemigroup_stimes :: TermDef Semigroup '[Proxy a, Proxy b] (Semigroup a # Integral b #> (b -> a -> a))+teSemigroup_stimes = Term (tySemigroup a0 # tyIntegral b1) (b1 ~> a0 ~> a0) $ teSym @Semigroup $ lam2 stimes
+ Language/Symantic/Lib/Sequences.hs view
@@ -0,0 +1,122 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Sequences'.+module Language.Symantic.Lib.Sequences where++import Data.Sequences (SemiSequence, IsSequence)+import Prelude hiding (filter, reverse)+import qualified Data.MonoTraversable as MT+import qualified Data.Sequences as Seqs++import Language.Symantic+import Language.Symantic.Lib.Function ()+import Language.Symantic.Lib.Bool (tyBool)+import Language.Symantic.Lib.MonoFunctor (e1, famElement)++-- * Class 'Sym_SemiSequence'+type instance Sym (Proxy SemiSequence) = Sym_SemiSequence+class Sym_SemiSequence term where+	intersperse :: SemiSequence s => term (MT.Element s) -> term s -> term s+	cons        :: SemiSequence s => term (MT.Element s) -> term s -> term s+	snoc        :: SemiSequence s => term s -> term (MT.Element s) -> term s+	reverse     :: SemiSequence s => term s -> term s+	default intersperse :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term s+	default cons        :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term s+	default snoc        :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term s -> term (MT.Element s) -> term s+	default reverse     :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term s -> term s+	intersperse = trans2 cons+	cons        = trans2 cons+	snoc        = trans2 snoc+	reverse     = trans1 reverse++-- Interpreting+instance Sym_SemiSequence Eval where+	intersperse = eval2 Seqs.intersperse+	cons        = eval2 Seqs.cons+	snoc        = eval2 Seqs.snoc+	reverse     = eval1 Seqs.reverse+instance Sym_SemiSequence View where+	intersperse = view2 "intersperse"+	cons        = view2 "cons"+	snoc        = view2 "snoc"+	reverse     = view1 "reverse"+instance (Sym_SemiSequence r1, Sym_SemiSequence r2) => Sym_SemiSequence (Dup r1 r2) where+	intersperse = dup2 @Sym_SemiSequence intersperse+	cons        = dup2 @Sym_SemiSequence cons+	snoc        = dup2 @Sym_SemiSequence snoc+	reverse     = dup1 @Sym_SemiSequence reverse++-- Transforming+instance (Sym_SemiSequence term, Sym_Lambda term) => Sym_SemiSequence (BetaT term)++-- Typing+instance FixityOf SemiSequence+instance ClassInstancesFor SemiSequence+instance TypeInstancesFor SemiSequence++-- Compiling+instance Gram_Term_AtomsFor src ss g SemiSequence+instance (Source src, Inj_Sym ss SemiSequence) => ModuleFor src ss SemiSequence where+	moduleFor = ["SemiSequence"] `moduleWhere`+	 [ "intersperse" := teSemiSequence_intersperse+	 , "cons"        := teSemiSequence_cons+	 , "snoc"        := teSemiSequence_snoc+	 , "reverse"     := teSemiSequence_reverse+	 ]++-- ** 'Type's+tySemiSequence :: Source src => Type src vs a -> Type src vs (SemiSequence a)+tySemiSequence a = tyConstLen @(K SemiSequence) @SemiSequence (lenVars a) `tyApp` a++s0 :: Source src => Inj_Len vs => Inj_Kind (K s) =>+      Type src (Proxy s ': vs) s+s0 = tyVar "s" varZ++-- ** 'Term's+teSemiSequence_reverse :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (s -> s))+teSemiSequence_reverse = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> s0) $ teSym @SemiSequence $ lam1 reverse++teSemiSequence_intersperse, teSemiSequence_cons :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (e -> s -> s))+teSemiSequence_intersperse = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> s0) $ teSym @SemiSequence $ lam2 intersperse+teSemiSequence_cons = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> s0) $ teSym @SemiSequence $ lam2 cons++teSemiSequence_snoc :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (s -> e -> s))+teSemiSequence_snoc = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> e1 ~> s0) $ teSym @SemiSequence $ lam2 snoc++-- * Class 'Sym_IsSequence'+type instance Sym (Proxy IsSequence) = Sym_IsSequence+class Sym_IsSequence term where+	filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s+	default filter :: Sym_IsSequence (UnT term) => Trans term => IsSequence s => term (MT.Element s -> Bool) -> term s -> term s+	filter = trans2 filter++-- Interpreting+instance Sym_IsSequence Eval where+	filter  = eval2 Seqs.filter+instance Sym_IsSequence View where+	filter  = view2 "filter"+instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (Dup r1 r2) where+	filter  = dup2 @Sym_IsSequence filter++-- Transforming+instance (Sym_IsSequence term, Sym_Lambda term) => Sym_IsSequence (BetaT term)++-- Typing+instance FixityOf IsSequence+instance ClassInstancesFor IsSequence+instance TypeInstancesFor IsSequence++-- Compiling+instance Gram_Term_AtomsFor src ss g IsSequence+instance (Source src, Inj_Sym ss IsSequence) => ModuleFor src ss IsSequence where+	moduleFor = ["IsSequence"] `moduleWhere`+	 [ "filter" := teIsSequence_filter+	 ]++-- ** 'Type's+tyIsSequence :: Source src => Type src vs a -> Type src vs (IsSequence a)+tyIsSequence a = tyConstLen @(K IsSequence) @IsSequence (lenVars a) `tyApp` a++-- ** 'Term's+teIsSequence_filter :: TermDef IsSequence '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> ((e -> Bool) -> s -> s))+teIsSequence_filter = Term (tyIsSequence s0 # e1 #~ famElement s0) ((e1 ~> tyBool) ~> s0 ~> s0) $ teSym @IsSequence $ lam2 filter
+ Language/Symantic/Lib/Show.hs view
@@ -0,0 +1,76 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Show'.+module Language.Symantic.Lib.Show where++import Prelude hiding (Show(..))+import Text.Show (Show)+import qualified Text.Show as Show++import Language.Symantic+import Language.Symantic.Lib.Char (tyString)+import Language.Symantic.Lib.Function (a0)+import Language.Symantic.Lib.Int (tyInt)+import Language.Symantic.Lib.List (tyList)++-- * Class 'Sym_Show'+type instance Sym (Proxy Show) = Sym_Show+class Sym_Show term where+	showsPrec :: Show a => term Int -> term a -> term ShowS+	show      :: Show a => term a -> term String+	showList  :: Show a => term [a] -> term ShowS+	+	default showsPrec :: Sym_Show (UnT term) => Trans term => Show a => term Int -> term a -> term ShowS+	default show      :: Sym_Show (UnT term) => Trans term => Show a => term a -> term String+	default showList  :: Sym_Show (UnT term) => Trans term => Show a => term [a] -> term ShowS+	+	showsPrec = trans2 showsPrec+	show      = trans1 show+	showList  = trans1 showList++instance Sym_Show Eval where+	showsPrec = eval2 Show.showsPrec+	show      = eval1 Show.show+	showList  = eval1 Show.showList+instance Sym_Show View where+	showsPrec = view2 "showsPrec"+	show      = view1 "show"+	showList  = view1 "showList"+instance (Sym_Show r1, Sym_Show r2) => Sym_Show (Dup r1 r2) where+	showsPrec = dup2 @Sym_Show showsPrec+	show      = dup1 @Sym_Show show+	showList  = dup1 @Sym_Show showList++-- Transforming+instance (Sym_Show term, Sym_Lambda term) => Sym_Show (BetaT term)++-- Typing+instance FixityOf Show+instance ClassInstancesFor Show+instance TypeInstancesFor Show++-- Compiling+instance Gram_Term_AtomsFor src ss g Show+instance (Source src, Inj_Sym ss Show) => ModuleFor src ss Show where+	moduleFor = ["Show"] `moduleWhere`+	 [ "showsPrec" := teShow_showsPrec+	 , "show"      := teShow_show+	 , "showList"  := teShow_showList+	 ]++-- ** 'Type's+tyShow :: Source src => Type src vs a -> Type src vs (Show a)+tyShow a = tyConstLen @(K Show) @Show (lenVars a) `tyApp` a++tyShowS :: Source src => Inj_Len vs => Type src vs ShowS+tyShowS = tyString ~> tyString++-- ** 'Term's+teShow_showsPrec :: TermDef Show '[Proxy a] (Show a #> (Int -> a -> ShowS))+teShow_showsPrec = Term (tyShow a0) (tyInt ~> a0 ~> tyShowS) $ teSym @Show $ lam2 showsPrec++teShow_show :: TermDef Show '[Proxy a] (Show a #> (a -> String))+teShow_show = Term (tyShow a0) (a0 ~> tyString) $ teSym @Show $ lam1 show++teShow_showList :: TermDef Show '[Proxy a] (Show a #> ([a] -> ShowS))+teShow_showList = Term (tyShow a0) (tyList a0 ~> tyShowS) $ teSym @Show $ lam1 showList
+ Language/Symantic/Lib/Test.hs view
@@ -0,0 +1,42 @@+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module Lib.Test where++import Test.Tasty++import Prelude hiding ((&&), not, (||), (==), id)++import Language.Symantic+import Language.Symantic.Lib++import qualified Lib.Applicative.Test as Applicative+import qualified Lib.Bool.Test as Bool+import qualified Lib.Foldable.Test as Foldable+import qualified Lib.Functor.Test as Functor+import qualified Lib.Map.Test as Map+import qualified Lib.MonoFunctor.Test as MonoFunctor+import qualified Lib.Num.Test as Num+import qualified Lib.Tuple2.Test as Tuple2++-- * Tests+tests :: TestTree+tests = testGroup "Lib" $+ [ Applicative.tests+ , Bool.tests+ , Foldable.tests+ , Functor.tests+ , Map.tests+ , MonoFunctor.tests+ , Num.tests+ , Tuple2.tests+ ]++-- * EDSL tests+te1 = lam $ \x -> lam $ \y -> (x || y) && not (x && y)+te2 = lam $ \x -> lam $ \y -> (x && not y) || (not x && y)+te3 = let_ (bool True) $ \x -> x && x+te4 = let_ (lam $ \x -> x && x) $ \f -> f `app` bool True+te5 = lam $ \x0 -> lam $ \x1 -> x0 && x1+te6 = let_ (bool True) id && bool False+te7 = lam $ \f -> (f  `app` bool True) && bool True+te8 = lam $ \f -> f `app` (bool True && bool True)
+ Language/Symantic/Lib/Text.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Text'.+module Language.Symantic.Lib.Text where++import Data.Text (Text)+import qualified Data.MonoTraversable as MT+import qualified Data.Sequences as Seqs+import qualified Data.Text as Text++import Language.Symantic.Grammar+import Language.Symantic+import Language.Symantic.Lib.Char ()+import Language.Symantic.Lib.MonoFunctor (Element)++-- * Class 'Sym_Text'+type instance Sym (Proxy Text) = Sym_Text+class Sym_Text term where+	text :: Text -> term Text+	default text :: Sym_Text (UnT term) => Trans term => Text -> term Text+	text = trans . text++-- Interpreting+instance Sym_Text Eval where+	text = Eval+instance Sym_Text View where+	text a = View $ \_p _v ->+		Text.pack (show a)+instance (Sym_Text r1, Sym_Text r2) => Sym_Text (Dup r1 r2) where+	text x = text x `Dup` text x++-- Transforming+instance (Sym_Text term, Sym_Lambda term) => Sym_Text (BetaT term)++-- Typing+instance ClassInstancesFor Text where+	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)+	 | Just HRefl <- proj_ConstKiTy @_ @Text c+	 = case () of+		 _ | Just Refl <- proj_Const @Eq q                -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFoldable q   -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFunctor q    -> Just Dict+		   | Just Refl <- proj_Const @Monoid q            -> Just Dict+		   | Just Refl <- proj_Const @Ord q               -> Just Dict+		   | Just Refl <- proj_Const @Seqs.IsSequence q   -> Just Dict+		   | Just Refl <- proj_Const @Seqs.SemiSequence q -> Just Dict+		   | Just Refl <- proj_Const @Show q              -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor Text where+	expandFamFor _c len f (c `TypesS` TypesZ)+	 | Just HRefl <- proj_ConstKi @_ @Element f+	 , Just HRefl <- proj_ConstKiTy @_ @Text c+	 = Just $ tyConstLen @(K (MT.Element Text)) @(MT.Element Text) len+	expandFamFor _c _len _fam _as = Nothing++-- Compiling+instance Gram_Term_AtomsFor src ss g Text -- TODO+instance ModuleFor src ss Text++-- ** 'Type's+tyText :: Source src => Inj_Len vs => Type src vs Text+tyText = tyConst @(K Text) @Text++-- ** 'Term's+teText :: Source src => Inj_Sym ss Text => Text -> Term src ss ts '[] (() #> Text)+teText t = Term noConstraint tyText $ teSym @Text $ text t
+ Language/Symantic/Lib/Traversable.hs view
@@ -0,0 +1,54 @@+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for 'Traversable'.+module Language.Symantic.Lib.Traversable where++import Prelude hiding (traverse)+import qualified Data.Traversable as Traversable++import Language.Symantic+import Language.Symantic.Lib.Applicative (tyApplicative)+import Language.Symantic.Lib.Function (a0, b1)+import Language.Symantic.Lib.Functor (f2)++-- * Class 'Sym_Traversable'+type instance Sym (Proxy Traversable) = Sym_Traversable+class Sym_Traversable term where+	traverse :: Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b))+	default traverse :: Sym_Traversable (UnT term) => Trans term => Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b))+	traverse = trans2 traverse++-- Interpreting+instance Sym_Traversable Eval where+	traverse = eval2 Traversable.traverse+instance Sym_Traversable View where+	traverse = view2 "traverse"+instance (Sym_Traversable r1, Sym_Traversable r2) => Sym_Traversable (Dup r1 r2) where+	traverse = dup2 @Sym_Traversable traverse++-- Transforming+instance (Sym_Traversable term, Sym_Lambda term) => Sym_Traversable (BetaT term)++-- Typing+instance FixityOf Traversable+instance ClassInstancesFor Traversable+instance TypeInstancesFor Traversable++-- Compiling+instance Gram_Term_AtomsFor src ss g Traversable+instance (Source src, Inj_Sym ss Traversable) => ModuleFor src ss Traversable where+	moduleFor = ["Traversable"] `moduleWhere`+	 [ "traverse" := teTraversable_traverse+	 ]++-- ** 'Type's+tyTraversable :: Source src => Type src vs a -> Type src vs (Traversable a)+tyTraversable a = tyConstLen @(K Traversable) @Traversable (lenVars a) `tyApp` a++-- * 'Term's+teTraversable_traverse :: TermDef Traversable '[Proxy a, Proxy b, Proxy f, Proxy t] (Traversable t # Applicative f #> ((a -> f b) -> t a -> f (t b)))+teTraversable_traverse = Term (tyTraversable t # tyApplicative f2) ((a0 ~> f2 `tyApp` b1) ~> t `tyApp` a0 ~> f2 `tyApp` (t `tyApp` b1)) $ teSym @Traversable $ lam2 traverse+	where+	t :: Source src => Inj_Len vs => Inj_Kind (K t) => Type src (Proxy a ': Proxy b ': Proxy c ': Proxy t ': vs) t+	t = tyVar "t" $ VarS $ VarS $ VarS varZ
+ Language/Symantic/Lib/Tuple2.hs view
@@ -0,0 +1,134 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for @(,)@.+module Language.Symantic.Lib.Tuple2 where++import Data.Semigroup ((<>))+import Prelude hiding (fst, snd)+import qualified Data.Tuple as Tuple+import qualified Data.MonoTraversable as MT++import Language.Symantic+import Language.Symantic.Grammar+import Language.Symantic.Lib.Function (a0, b1)+import Language.Symantic.Lib.MonoFunctor (Element)+import Language.Symantic.Lib.Monoid (tyMonoid)++-- * Class 'Sym_Tuple2'+type instance Sym (Proxy (,)) = Sym_Tuple2+class Sym_Tuple2 term where+	tuple2 :: term a -> term b -> term (a, b)+	fst :: term (a, b) -> term a+	snd :: term (a, b) -> term b+	+	default tuple2 :: Sym_Tuple2 (UnT term) => Trans term => term a -> term b -> term (a, b)+	default fst    :: Sym_Tuple2 (UnT term) => Trans term => term (a, b) -> term a+	default snd    :: Sym_Tuple2 (UnT term) => Trans term => term (a, b) -> term b+	+	tuple2 = trans2 tuple2+	fst    = trans1 fst+	snd    = trans1 snd++-- Interpreting+instance Sym_Tuple2 Eval where+	tuple2 = eval2 (,)+	fst    = eval1 Tuple.fst+	snd    = eval1 Tuple.snd+instance Sym_Tuple2 View where+	tuple2 (View a) (View b) =+		View $ \_po v ->+			"(" <> a (op, SideL) v <> ", " <> b (op, SideR) v <> ")"+			where op = infixN 0+	fst = view1 "fst"+	snd = view1 "snd"+instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (Dup r1 r2) where+	tuple2 = dup2 @Sym_Tuple2 tuple2+	fst    = dup1 @Sym_Tuple2 fst+	snd    = dup1 @Sym_Tuple2 snd++-- Transforming+instance (Sym_Tuple2 term, Sym_Lambda term) => Sym_Tuple2 (BetaT term)++-- Typing+instance FixityOf (,) where+	fixityOf _c = Just $ Fixity2 $ infixN (-1)+instance ClassInstancesFor (,) where+	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c a))+	 | Just HRefl <- proj_ConstKiTy @_ @(,) c+	 = case () of+		 _ | Just Refl <- proj_Const @Applicative q+		   , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict+		   | Just Refl <- proj_Const @Functor q  -> Just Dict+		   | Just Refl <- proj_Const @Foldable q -> Just Dict+		   | Just Refl <- proj_Const @Monad q+		   , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict+		   | Just Refl <- proj_Const @Traversable q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c a) b))+	 | Just HRefl <- proj_ConstKiTy @_ @(,) c+	 = case () of+		 _ | Just Refl <- proj_Const @Bounded q+		   , Just Dict <- proveConstraint (tq `tyApp` a)+		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict+		   | Just Refl <- proj_Const @Eq q+		   , Just Dict <- proveConstraint (tq `tyApp` a)+		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict+		   | Just Refl <- proj_Const @Monoid q+		   , Just Dict <- proveConstraint (tq `tyApp` a)+		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict+		   | Just Refl <- proj_Const @Ord q+		   , Just Dict <- proveConstraint (tq `tyApp` a)+		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict+		   | Just Refl <- proj_Const @Show q+		   , Just Dict <- proveConstraint (tq `tyApp` a)+		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor (,) where+	expandFamFor _c _len f (TyApp _ (TyApp _ c _a) b `TypesS` TypesZ)+	 | Just HRefl <- proj_ConstKi @_ @Element f+	 , Just HRefl <- proj_ConstKiTy @_ @(,) c+	 = Just b+	expandFamFor _c _len _fam _as = Nothing++-- Compiling+instance+ ( Gram_Source src g+ , Gram_Alt g+ , Gram_Rule g+ , Gram_Comment g+ , Gram_Term src ss g+ , Inj_Sym ss (,)+ ) => Gram_Term_AtomsFor src ss g (,) where+	g_term_atomsFor =+	 -- TODO: proper TupleSections+	 [ rule "teTuple2_2" $+		g_source $ parens $+		(\a b src ->+			BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2) a) b)+		 <$> g_term+		 <*  symbol ","+		 <*> g_term+	 , rule "teTuple2" $+		g_source $+		(\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2)+		 <$ symbol "(,)"+	 ]+instance (Source src, Inj_Sym ss (,)) => ModuleFor src ss (,) where+	moduleFor = ["Tuple2"] `moduleWhere`+	 [ "fst" := teTuple2_fst+	 , "snd" := teTuple2_snd+	 ]++-- ** 'Term's+tyTuple2 :: Source src => Inj_Len vs => Type src vs a -> Type src vs b -> Type src vs (a, b)+tyTuple2 a b = tyConst @(K (,)) @(,) `tyApp` a `tyApp` b++teTuple2 :: TermDef (,) '[Proxy a, Proxy b] (() #> (a -> b -> (a, b)))+teTuple2 = Term noConstraint (a0 ~> b1 ~> tyTuple2 a0 b1) $ teSym @(,) $ lam2 tuple2+teTuple2_fst :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> a))+teTuple2_fst = Term noConstraint (tyTuple2 a0 b1 ~> a0) $ teSym @(,) $ lam1 fst+teTuple2_snd :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> b))+teTuple2_snd = Term noConstraint (tyTuple2 a0 b1 ~> b1) $ teSym @(,) $ lam1 snd
+ Language/Symantic/Lib/Tuple2/Test.hs view
@@ -0,0 +1,29 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module Lib.Tuple2.Test where++import Test.Tasty++import Data.Proxy (Proxy(..))+import Prelude hiding ((&&), not, (||))++import Language.Symantic.Lib+import Compiling.Test++type SS =+ [ Proxy (->)+ , Proxy Integer+ , Proxy ()+ , Proxy (,)+ ]+(==>) = test_readTerm @() @SS++tests :: TestTree+tests = testGroup "Tuple2"+ [ "()"             ==> Right (tyUnit, (), "()")+ , "(,) 1 2"        ==> Right (tyTuple2 tyInteger tyInteger, (1,2), "(1, 2)")+ , "(1,2)"          ==> Right (tyTuple2 tyInteger tyInteger, (1,2), "(1, 2)")+ , "((1,2), (3,4))" ==> Right+	 ( let t = tyTuple2 tyInteger tyInteger in tyTuple2 t t+	 , ((1,2),(3,4))+	 , "((1, 2), (3, 4))" )+ ]
+ Language/Symantic/Lib/Unit.hs view
@@ -0,0 +1,66 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic for '()'.+module Language.Symantic.Lib.Unit where++import Prelude hiding ((&&), not, (||))++import Language.Symantic+import Language.Symantic.Grammar++-- * Class 'Sym_Unit'+type instance Sym (Proxy ()) = Sym_Unit+class Sym_Unit term where+	unit :: term ()+	default unit :: Sym_Unit (UnT term) => Trans term => term ()+	unit = trans unit++-- Interpreting+instance Sym_Unit Eval where+	unit = Eval ()+instance Sym_Unit View where+	unit = View $ \_p _v -> "()"+instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where+	unit = unit `Dup` unit++-- Transforming+instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)++-- Typing+instance ClassInstancesFor () where+	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)+	 | Just HRefl <- proj_ConstKiTy @_ @() z+	 = case () of+		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict+		   | Just Refl <- proj_Const @Enum    q -> Just Dict+		   | Just Refl <- proj_Const @Eq      q -> Just Dict+		   | Just Refl <- proj_Const @Monoid  q -> Just Dict+		   | Just Refl <- proj_Const @Ord     q -> Just Dict+		   | Just Refl <- proj_Const @Show    q -> Just Dict+		 _ -> Nothing+	proveConstraintFor _c _q = Nothing+instance TypeInstancesFor ()++-- Compiling+instance+ ( Gram_Source src g+ , Gram_Rule g+ , Gram_Comment g+ , Inj_Sym ss ()+ ) => Gram_Term_AtomsFor src ss g () where+	g_term_atomsFor =+	 [ rule "teUnit" $+		g_source $+		(\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teUnit)+		 <$ symbol "("+		 <* symbol ")"+	 ]+instance ModuleFor src ss ()++-- ** 'Type's+tyUnit :: Source src => Inj_Len vs => Type src vs ()+tyUnit = tyConst @(K ()) @()++-- ** 'Term's+teUnit :: TermDef () '[] (() #> ())+teUnit = Term noConstraint tyUnit $ teSym @() $ unit
+ Language/Symantic/Test.hs view
@@ -0,0 +1,14 @@+module Test where++import Test.Tasty++import qualified Typing.Test as Typing+import qualified Lib.Test as Lib++main :: IO ()+main =+	defaultMain $+	testGroup "Language.Symantic"+	 [ Typing.tests+	 , Lib.tests+	 ]
+ Language/Symantic/Typing/Test.hs view
@@ -0,0 +1,167 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Typing.Test where++import Test.Tasty+import Test.Tasty.HUnit++import Control.Applicative (Applicative(..))+import Control.Arrow (left)+import Data.Map.Strict (Map)+import Data.Maybe (isJust)+import Data.NonNull (NonNull)+import Data.Proxy+import Data.Ratio (Ratio)+import Data.Text (Text)+import Data.List.NonEmpty (NonEmpty)+import GHC.Exts (Constraint)+import Prelude hiding (exp)+import qualified Data.Function as Fun+import qualified Data.Map.Strict as Map+import qualified Data.MonoTraversable as MT+import qualified Data.Sequences as Seqs+import qualified System.IO as IO+import qualified Text.Megaparsec as P++import Language.Symantic.Grammar+import Language.Symantic+import Language.Symantic.Lib hiding ((<$>), (<*), show)++import Grammar.Megaparsec ()++-- * Tests+type SS =+ [ Proxy (->)+ , Proxy Bool+ , Proxy []+ , Proxy ()+ , Proxy (,)+ , Proxy Char+ , Proxy Either+ , Proxy Int+ , Proxy Integer+ , Proxy IO+ , Proxy IO.Handle+ , Proxy IO.IOMode+ , Proxy Ordering+ , Proxy Map+ , Proxy Maybe+ , Proxy NonNull+ , Proxy Ratio+ , Proxy Text+ , Proxy Applicative+ , Proxy Bounded+ , Proxy Enum+ , Proxy Eq+ , Proxy Foldable+ , Proxy Functor+ , Proxy Integral+ , Proxy Monad+ , Proxy Monoid+ , Proxy MT.MonoFoldable+ , Proxy MT.MonoFunctor+ , Proxy Num+ , Proxy Ord+ , Proxy Real+ , Proxy Seqs.IsSequence+ , Proxy Seqs.SemiSequence+ , Proxy Show+ , Proxy Traversable+ ]+type SRC = SrcTe (NonEmpty P.SourcePos) SS++cs :: Source src => Name2Type src+cs =+	Map.insert "String"+	 (TypeTLen $ \len -> TypeT $+		tyConstLen @(K [])   @[]   len `tyApp`+		tyConstLen @(K Char) @Char len) $+	inj_Name2Type @SS++tests :: TestTree+tests = testGroup "Typing" $+ [ testGroup "readType" $+	let run inp (TypeT exp :: TypeT SRC '[]) =+		testCase inp $ got @?= Right (Right $ TypeVT exp)+		where+		got :: Either (P.ParseError Char P.Dec)+		              (Either (Error_Type SRC) (TypeVT SRC))+		got = readType cs <$> P.runParser (unCF g) "" inp+		g :: Gram_Type SRC g => CF g (AST_Type SRC)+		g = g_type <* eoi in+	let (==>) = run; infixr 0 ==> in+	 [ "Bool"                        ==> TypeT $ tyBool+	 , "(->) Bool"                   ==> TypeT $ tyFun `tyApp` tyBool+	 , "[]"                          ==> TypeT $ tyConst @(K []) @[]+	 , "[Char]"                      ==> TypeT $ tyList tyChar+	 , "[Char -> [Char]]"            ==> TypeT $ tyList (tyChar ~> tyList tyChar)+	 , "([])"                        ==> TypeT $ tyConst @(K []) @[]+	 , "[()]"                        ==> TypeT $ tyList tyUnit+	 , "()"                          ==> TypeT $ tyUnit+	 , "(())"                        ==> TypeT $ tyUnit+	 , "(,)"                         ==> TypeT $ tyConst @(K (,)) @(,)+	 , "((,))"                       ==> TypeT $ tyConst @(K (,)) @(,)+	 , "(,) Int"                     ==> TypeT $ tyConst @(K (,)) @(,) `tyApp` tyInt+	 , "(Bool)"                      ==> TypeT $ tyBool+	 , "((Bool))"                    ==> TypeT $ tyBool+	 , "(Bool, Int)"                 ==> TypeT $ tyBool `tyTuple2` tyInt+	 , "((Bool, Int))"               ==> TypeT $ tyBool `tyTuple2` tyInt+	 , "((Bool, Int), Char)"         ==> TypeT $ (tyBool `tyTuple2` tyInt) `tyTuple2` tyChar+	 , "(Bool, Int) -> Char"         ==> TypeT $ (tyBool `tyTuple2` tyInt) ~> tyChar+	 , "(Bool -> Int)"               ==> TypeT $ tyBool ~> tyInt+	 , "String"                      ==> TypeT $ tyList tyChar+	 , "[Char] -> String"            ==> TypeT $ tyList tyChar ~> tyList tyChar+	 , "String -> [Char]"            ==> TypeT $ tyList tyChar ~> tyList tyChar+	 , "Maybe Bool"                  ==> TypeT $ tyMaybe tyBool+	 , "Either Bool Int"             ==> TypeT $ tyEither tyBool tyInt+	 , "Bool -> Int"                 ==> TypeT $ tyBool ~> tyInt+	 , "(Bool -> Int) -> Char"       ==> TypeT $ (tyBool ~> tyInt) ~> tyChar+	 , "Bool -> (Int -> Char)"       ==> TypeT $ tyBool ~> (tyInt ~> tyChar)+	 , "Bool -> Int -> Char"         ==> TypeT $ tyBool ~> tyInt ~> tyChar+	 , "Bool -> (Int -> Char) -> ()" ==> TypeT $ tyBool ~> (tyInt ~> tyChar) ~> tyUnit+	 , "IO"                          ==> TypeT $ tyConst @(K IO) @IO+	 , "Traversable IO"              ==> TypeT $ tyTraversable (tyConst @(K IO) @IO)+	 , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)+	 , "(->) (IO Bool)"              ==> TypeT $ tyConst @(K (->)) @(->) `tyApp` (tyIO tyBool)+	 , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)+	 , "Eq"                          ==> TypeT $ tyConst @(K Eq) @Eq+	 , "Eq Bool"                     ==> TypeT $ tyEq tyBool+	 ]+	 , testGroup "Parsing errors" $+		let run inp = testCase inp $ got @?= Left ()+			where+			got :: Either () (AST_Type SRC)+			got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ P.runParser (unCF g) "" inp+			g :: Gram_Type SRC g => CF g (AST_Type SRC)+			g = g_type <* eoi in+		run <$>+		 [ "Bool, Int"+		 , "(Bool -> Int) Char"+		 ]+	 , testGroup "Compiling errors" $+		let run inp = testCase inp $ got @?= Right (Left ())+			where+			got :: Either (P.ParseError Char P.Dec) (Either () (TypeVT SRC))+			got = left (Fun.const ()) . readType cs <$> P.runParser (unCF g) "" inp+			g :: Gram_Type SRC g => CF g (AST_Type SRC)+			g = g_type <* eoi in+		run <$>+		 [ "NonExistingType"+		 , "Bool Int"+		 , "[IO]"+		 , "(->) IO"+		 , "(->) Bool Int Char"+		 , "Monad Eq"+		 ]+ , testGroup "proveConstraint" $+	let (==>) (typ::Type SRC '[] (t::Constraint)) expected =+		testCase (show typ) $+		isJust (proveConstraint typ) @?= expected in+	 [ tyEq          tyBool                      ==> True+	 , tyOrd         tyBool                      ==> True+	 , tyFunctor     (tyConst @(K Maybe) @Maybe) ==> True+	 , tyFunctor     (tyConst @(K IO) @IO)       ==> True+	 , tyMonad       (tyConst @(K IO) @IO)       ==> True+	 , tyTraversable (tyConst @(K IO) @IO)       ==> False+	 ]+ ]
+ symantic-lib.cabal view
@@ -0,0 +1,184 @@+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:+  Symantics for common types,+  using <https://hackage.haskell.org/package/symantic symantic>.+extra-source-files:+extra-tmp-files:+-- homepage: +license: GPL-3+license-file: COPYING+maintainer: Julien Moutinho <julm+symantic@autogeree.net>+name: symantic-lib+stability: experimental+synopsis: Symantics for common types.+tested-with: GHC==8.0.2+-- PVP:  +-+------- breaking API changes+--       | | +----- non-breaking API additions+--       | | | +--- code changes with no API change+version: 0.0.2.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+               -fprint-explicit-kinds+  default-language: Haskell2010+  exposed-modules:+    Language.Symantic.Lib+    Language.Symantic.Lib.Alternative+    Language.Symantic.Lib.Applicative+    Language.Symantic.Lib.Bool+    Language.Symantic.Lib.Bounded+    Language.Symantic.Lib.Char+    Language.Symantic.Lib.Either+    Language.Symantic.Lib.Enum+    Language.Symantic.Lib.Eq+    Language.Symantic.Lib.Foldable+    Language.Symantic.Lib.Function+    Language.Symantic.Lib.Functor+    Language.Symantic.Lib.IO+    Language.Symantic.Lib.If+    Language.Symantic.Lib.Int+    Language.Symantic.Lib.Integer+    Language.Symantic.Lib.Integral+    Language.Symantic.Lib.List+    Language.Symantic.Lib.Map+    Language.Symantic.Lib.Maybe+    Language.Symantic.Lib.Monad+    Language.Symantic.Lib.MonoFoldable+    Language.Symantic.Lib.MonoFunctor+    Language.Symantic.Lib.Monoid+    Language.Symantic.Lib.NonNull+    Language.Symantic.Lib.Num+    Language.Symantic.Lib.Ord+    Language.Symantic.Lib.Ratio+    Language.Symantic.Lib.Real+    Language.Symantic.Lib.Semigroup+    Language.Symantic.Lib.Sequences+    Language.Symantic.Lib.Show+    Language.Symantic.Lib.Text+    Language.Symantic.Lib.Traversable+    Language.Symantic.Lib.Tuple2+    Language.Symantic.Lib.Unit+  build-depends:+    base >= 4.6 && < 5+    , containers+    , ghc-prim+    , monad-classes+    , mono-traversable+    , symantic >= 6.0+    , symantic-grammar+    , transformers+    , text++Test-Suite symantic-test+  type: exitcode-stdio-1.0+  default-extensions:+    DataKinds+    FlexibleContexts+    FlexibleInstances+    MultiParamTypeClasses+    NoMonomorphismRestriction+    OverloadedStrings+    ScopedTypeVariables+    TupleSections+    TypeApplications+    TypeFamilies+    TypeOperators+  default-language: Haskell2010+  ghc-options: -main-is Test+               -Wall+               -fno-warn-tabs+               -- -O0+               -- -fmax-simplifier-iterations=0+               -- -dshow-passes+  hs-source-dirs: Language/Symantic+  main-is: Test.hs+  other-modules:+    Compiling.Test+    Grammar.Megaparsec+    Lib.Applicative.Test+    Lib.Bool.Test+    Lib.Foldable.Test+    Lib.Functor.Test+    Lib.Map.Test+    Lib.MonoFunctor.Test+    Lib.Num.Test+    Lib.Test+    Lib.Tuple2.Test+    Typing.Test+  build-depends:+    base >= 4.6 && < 5+    , containers+    , megaparsec+    , monad-classes+    , mono-traversable+    , symantic-grammar+    , symantic+    , symantic-lib+    , tasty >= 0.11+    , tasty-hunit+    , text+    , transformers++Test-Suite ebnf+  type: exitcode-stdio-1.0+  default-extensions:+    ConstraintKinds+    DataKinds+    EmptyDataDecls+    FlexibleContexts+    FlexibleInstances+    MultiParamTypeClasses+    NamedFieldPuns+    OverloadedStrings+    PatternGuards+    PolyKinds+    Rank2Types+    ScopedTypeVariables+    StandaloneDeriving+    TupleSections+    TypeFamilies+    TypeApplications+    TypeOperators+  ghc-options: -main-is Grammar.EBNF+               -Wall+               -fno-warn-tabs+               -fprint-potential-instances+  main-is: Grammar/EBNF.hs+  default-language: Haskell2010+  hs-source-dirs: Language/Symantic+  build-depends:+    base >= 4.6 && < 5+    , containers+    , megaparsec+    , symantic-grammar+    , symantic+    , symantic-lib+    , transformers+    , tasty >= 0.11+    , tasty-hunit+    , text