diff --git a/COPYING b/COPYING new file mode 100644 --- /dev/null +++ b/COPYING @@ -0,0 +1,674 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + 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. + + + Copyright (C) + + 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 . + +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: + + Copyright (C) + 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 +. + + 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 +. diff --git a/Language/Symantic/Compiling/Test.hs b/Language/Symantic/Compiling/Test.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Compiling/Test.hs @@ -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 diff --git a/Language/Symantic/Grammar/EBNF.hs b/Language/Symantic/Grammar/EBNF.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Grammar/EBNF.hs @@ -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 diff --git a/Language/Symantic/Grammar/Megaparsec.hs b/Language/Symantic/Grammar/Megaparsec.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Grammar/Megaparsec.hs @@ -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) diff --git a/Language/Symantic/Lib.hs b/Language/Symantic/Lib.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib.hs @@ -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 + ] +-} diff --git a/Language/Symantic/Lib/Alternative.hs b/Language/Symantic/Lib/Alternative.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Alternative.hs @@ -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 (<|>) diff --git a/Language/Symantic/Lib/Applicative.hs b/Language/Symantic/Lib/Applicative.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Applicative.hs @@ -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 (*>) diff --git a/Language/Symantic/Lib/Applicative/Test.hs b/Language/Symantic/Lib/Applicative/Test.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Applicative/Test.hs @@ -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") + ] diff --git a/Language/Symantic/Lib/Bool.hs b/Language/Symantic/Lib/Bool.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Bool.hs @@ -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 diff --git a/Language/Symantic/Lib/Bool/Test.hs b/Language/Symantic/Lib/Bool/Test.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Bool/Test.hs @@ -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) diff --git a/Language/Symantic/Lib/Bounded.hs b/Language/Symantic/Lib/Bounded.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Bounded.hs @@ -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 diff --git a/Language/Symantic/Lib/Char.hs b/Language/Symantic/Lib/Char.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Char.hs @@ -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 diff --git a/Language/Symantic/Lib/Either.hs b/Language/Symantic/Lib/Either.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Either.hs @@ -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 diff --git a/Language/Symantic/Lib/Enum.hs b/Language/Symantic/Lib/Enum.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Enum.hs @@ -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 diff --git a/Language/Symantic/Lib/Eq.hs b/Language/Symantic/Lib/Eq.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Eq.hs @@ -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 (/=) diff --git a/Language/Symantic/Lib/Foldable.hs b/Language/Symantic/Lib/Foldable.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Foldable.hs @@ -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 +-} diff --git a/Language/Symantic/Lib/Foldable/Test.hs b/Language/Symantic/Lib/Foldable/Test.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Foldable/Test.hs @@ -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 : [])" ) + ] diff --git a/Language/Symantic/Lib/Function.hs b/Language/Symantic/Lib/Function.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Function.hs @@ -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 diff --git a/Language/Symantic/Lib/Functor.hs b/Language/Symantic/Lib/Functor.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Functor.hs @@ -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 (<$) diff --git a/Language/Symantic/Lib/Functor/Test.hs b/Language/Symantic/Lib/Functor/Test.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Functor/Test.hs @@ -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") + ] diff --git a/Language/Symantic/Lib/IO.hs b/Language/Symantic/Lib/IO.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/IO.hs @@ -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 diff --git a/Language/Symantic/Lib/If.hs b/Language/Symantic/Lib/If.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/If.hs @@ -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_ diff --git a/Language/Symantic/Lib/Int.hs b/Language/Symantic/Lib/Int.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Int.hs @@ -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 diff --git a/Language/Symantic/Lib/Integer.hs b/Language/Symantic/Lib/Integer.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Integer.hs @@ -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 diff --git a/Language/Symantic/Lib/Integral.hs b/Language/Symantic/Lib/Integral.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Integral.hs @@ -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 diff --git a/Language/Symantic/Lib/List.hs b/Language/Symantic/Lib/List.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/List.hs @@ -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 diff --git a/Language/Symantic/Lib/Map.hs b/Language/Symantic/Lib/Map.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Map.hs @@ -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 diff --git a/Language/Symantic/Lib/Map/Test.hs b/Language/Symantic/Lib/Map/Test.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Map/Test.hs @@ -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' : [])))" ) + ] diff --git a/Language/Symantic/Lib/Maybe.hs b/Language/Symantic/Lib/Maybe.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Maybe.hs @@ -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' diff --git a/Language/Symantic/Lib/Monad.hs b/Language/Symantic/Lib/Monad.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Monad.hs @@ -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 diff --git a/Language/Symantic/Lib/MonoFoldable.hs b/Language/Symantic/Lib/MonoFoldable.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/MonoFoldable.hs @@ -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 diff --git a/Language/Symantic/Lib/MonoFunctor.hs b/Language/Symantic/Lib/MonoFunctor.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/MonoFunctor.hs @@ -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 diff --git a/Language/Symantic/Lib/MonoFunctor/Test.hs b/Language/Symantic/Lib/MonoFunctor/Test.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/MonoFunctor/Test.hs @@ -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' : [])" ) + ] diff --git a/Language/Symantic/Lib/Monoid.hs b/Language/Symantic/Lib/Monoid.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Monoid.hs @@ -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 diff --git a/Language/Symantic/Lib/NonNull.hs b/Language/Symantic/Lib/NonNull.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/NonNull.hs @@ -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 diff --git a/Language/Symantic/Lib/Num.hs b/Language/Symantic/Lib/Num.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Num.hs @@ -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 (*) diff --git a/Language/Symantic/Lib/Num/Test.hs b/Language/Symantic/Lib/Num/Test.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Num/Test.hs @@ -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 + ] diff --git a/Language/Symantic/Lib/Ord.hs b/Language/Symantic/Lib/Ord.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Ord.hs @@ -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 diff --git a/Language/Symantic/Lib/Ratio.hs b/Language/Symantic/Lib/Ratio.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Ratio.hs @@ -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 diff --git a/Language/Symantic/Lib/Real.hs b/Language/Symantic/Lib/Real.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Real.hs @@ -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 diff --git a/Language/Symantic/Lib/Semigroup.hs b/Language/Symantic/Lib/Semigroup.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Semigroup.hs @@ -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 diff --git a/Language/Symantic/Lib/Sequences.hs b/Language/Symantic/Lib/Sequences.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Sequences.hs @@ -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 diff --git a/Language/Symantic/Lib/Show.hs b/Language/Symantic/Lib/Show.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Show.hs @@ -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 diff --git a/Language/Symantic/Lib/Test.hs b/Language/Symantic/Lib/Test.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Test.hs @@ -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) diff --git a/Language/Symantic/Lib/Text.hs b/Language/Symantic/Lib/Text.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Text.hs @@ -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 diff --git a/Language/Symantic/Lib/Traversable.hs b/Language/Symantic/Lib/Traversable.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Traversable.hs @@ -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 diff --git a/Language/Symantic/Lib/Tuple2.hs b/Language/Symantic/Lib/Tuple2.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Tuple2.hs @@ -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 diff --git a/Language/Symantic/Lib/Tuple2/Test.hs b/Language/Symantic/Lib/Tuple2/Test.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Tuple2/Test.hs @@ -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))" ) + ] diff --git a/Language/Symantic/Lib/Unit.hs b/Language/Symantic/Lib/Unit.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Lib/Unit.hs @@ -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 diff --git a/Language/Symantic/Test.hs b/Language/Symantic/Test.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Test.hs @@ -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 + ] diff --git a/Language/Symantic/Typing/Test.hs b/Language/Symantic/Typing/Test.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Typing/Test.hs @@ -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 + ] + ] diff --git a/symantic-lib.cabal b/symantic-lib.cabal new file mode 100644 --- /dev/null +++ b/symantic-lib.cabal @@ -0,0 +1,184 @@ +author: Julien Moutinho +bug-reports: Julien Moutinho +build-type: Simple +cabal-version: >= 1.24 +category: Language +description: + Symantics for common types, + using . +extra-source-files: +extra-tmp-files: +-- homepage: +license: GPL-3 +license-file: COPYING +maintainer: Julien Moutinho +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