diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for static
+
+## 0.1.0.0 -- 2020-05-17
+
+* Initial release.
diff --git a/LICENSE.GPL-3 b/LICENSE.GPL-3
new file mode 100644
--- /dev/null
+++ b/LICENSE.GPL-3
@@ -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/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/src/Control/Static.hs b/src/Control/Static.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Static.hs
@@ -0,0 +1,55 @@
+module Control.Static
+ (
+ -- * Common definitions
+ TCTab(..)
+ -- * Static keys and values
+ , SKey
+ , SKeyed(..)
+ , SKeyedExt(..)
+ , withSKeyedExt
+ , toSKeyedExt
+ -- * Static tables and resolving values
+ , gwithStatic
+ , withStaticCts
+ , withSomeStaticCts
+ , withStaticCxt
+ , withSomeStaticCxt
+ -- * Static closures
+ , PreClosure(..)
+ , Closure(..)
+ , PostClosure(..)
+ , ClosureApply
+ , applyClosure
+ , envTabCons
+ , envTabNil
+ , mkClosureTab
+ , RepClosure
+ , RepClosure'
+ , repClosureTab
+ , withEvalClosureCts
+ , withEvalSomeClosureCts
+ , withEvalClosureCxt
+ , withEvalSomeClosureCxt
+ , evalClosure
+ , evalSomeClosure
+ -- * Serialisation
+ , RepVal(..)
+ , SKeyedError(..)
+ , DoubleEncoding(..)
+ , DSerialise
+ , DBinary
+ )
+where
+
+import Control.Static.Closure
+import Control.Static.Common
+import Control.Static.Serialise
+import Control.Static.Static
+
+-- Note, the implementation comments in these files make various references to
+-- "singletons defunctionalisation symbols", see here for an approachable
+-- explanation:
+--
+-- https://blog.jle.im/entry/introduction-to-singletons-4.html#defunctionalization
+--
+-- You may want to start from part 1, if you have trouble jumping in the middle.
diff --git a/src/Control/Static/Closure.hs b/src/Control/Static/Closure.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Static/Closure.hs
@@ -0,0 +1,297 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Control.Static.Closure where
+
+-- external
+import Data.Constraint (Dict (..))
+import Data.Functor (($>))
+import Data.Kind (Constraint)
+import Data.Singletons.Prelude
+import Data.Singletons.TH (genDefunSymbols)
+
+-- internal
+import Control.Static.Common
+import Control.Static.Serialise
+import Control.Static.Static
+
+
+-- | Closure, internal representation.
+--
+-- The type parameter @env@ is meant for a bag of functions known statically at
+-- compile time, that you don't need to serialise and so don't want the added
+-- complexity of dealing with $(mkStatic). For example, if your function takes
+-- in extra utility functions, but these are all statically-known. The type
+-- parameter @cxt@ are the constraint types, which is effectively similar to
+-- @env@ except that Haskell deals with them slightly differently.
+type ClosureFunc cxt env arg res = CxtW cxt (env -> arg -> res)
+
+-- | An applied closure, consisting of its static key and an argument.
+type ClosureApply g = SKeyedExt g
+
+-- | Create a 'ClosureApply' in its serialisable static form.
+applyClosure
+ :: RepVal g arg k
+ => SKeyed k (CxtW cxt (env -> arg -> res))
+ -> arg
+ -> ClosureApply g
+applyClosure (SKeyed k cl) arg = toSKeyedExt (SKeyed k arg)
+
+envTabCons
+ :: SKeyed k (CxtW cxt (env -> arg -> res))
+ -> env
+ -> TTab kk vv
+ -> TTab (k ': kk) (env ': vv)
+envTabCons cl env = skeyedCons (cl $> env)
+
+envTabNil :: TTab '[] '[]
+envTabNil = TCNil @NullC2Sym0
+
+-- | A pre-closure is a function that takes two statically-known arguments:
+-- a constraint, and an explicit argument; and gives a closure.
+--
+-- Typically, you define a bunch of top-level functions of the form @(ctx =>
+-- env -> arg -> res)@, then create a table of pre-closures using the TH
+-- function 'Control.Static.TH.mkStaticTab'.
+class Closure (Part pcl) => PreClosure pcl where
+ type Cxt pcl :: Constraint
+ type Env pcl
+ type Part pcl
+ applyPre :: Cxt pcl => pcl -> Env pcl -> Part pcl
+
+instance PreClosure (CxtW c (e -> v -> r)) where
+ type Cxt (CxtW c (e -> v -> r)) = c
+ type Env (CxtW c (e -> v -> r)) = e
+ type Part (CxtW c (e -> v -> r)) = v -> r
+ applyPre (CxtW pcl) = pcl
+
+-- | A closure is a function that takes a runtime argument, and gives a result.
+--
+-- It is created by applying a constraint and environment to a pre-closure.
+-- Typically you do this once on a table of pre-closures, using 'mkClosureTab'.
+class Closure cl where
+ type Arg cl
+ type Res cl
+ apply :: cl -> Arg cl -> Res cl
+
+instance Closure (v -> r) where
+ type Arg (v -> r) = v
+ type Res (v -> r) = r
+ apply = ($)
+
+-- | A post-closure is a function that takes a runtime result, and converts all
+-- the results of all different closures into the same type.
+class PostClosure x f where
+ type Pre f
+ applyPost :: f -> Pre f -> x
+
+instance PostClosure x (r -> x) where
+ type Pre (r -> x) = r
+ applyPost = ($)
+
+genDefunSymbols [''Cxt, ''Env, ''Part, ''Arg, ''Res, ''Pre]
+
+
+-- | A continuation from the result type to @x@.
+type ResCont x = TyContSym1 x .@#@$$$ ResSym0
+
+
+-- | Apply a table of pre-closures to its inputs, creating a table of closures.
+applyClosureTabPre
+ :: forall c1 kk vv
+ . ConstrainList (Fmap CxtSym0 vv)
+ => TCTab' PreClosure kk vv
+ -> TCTab c1 kk (Fmap EnvSym0 vv)
+ -> TCTab' Closure kk (Fmap PartSym0 vv)
+applyClosureTabPre tab env =
+ zipWith3TC @_ @_ @_ @_ @_ @(DictOf CxtSym0) @EnvSym0 @PartSym0 tab cxt env
+ $ \_ cl _ Dict _ e -> (applyPre cl e, Dict)
+ where cxt = toTCDict @_ @_ @CxtSym0 tab
+
+-- | Apply a table of closures to its inputs, creating a table of results.
+applyClosureTab
+ :: forall c1 kk vv
+ . TCTab' Closure kk vv
+ -> TCTab c1 kk (Fmap ArgSym0 vv)
+ -> TTab kk (Fmap ResSym0 vv)
+applyClosureTab tab arg =
+ zipWithTC @_ @_ @_ @_ @ArgSym0 @ResSym0 tab arg $ \_ cl _ a -> (apply cl a, Dict)
+
+-- | Apply a table of results to its post-closures, creating a table of values.
+applyClosureTabPost
+ :: forall c0 kk rr x
+ . TCTab c0 kk rr
+ -> TCTab' (PostClosure x) kk (Fmap (TyContSym1 x) rr)
+ -> TTab kk (Fmap (ConstSym1 x) rr)
+applyClosureTabPost res post =
+ zipWithTC @_ @_ @_ @_ @(TyContSym1 x) @(ConstSym1 x) res post
+ $ \_ r _ p -> (applyPost p r, Dict)
+
+-- | Apply a table of closures to a table of inputs and post-closures, giving a
+-- table of values.
+--
+-- This method is just a demo, users will want one of the exported functions.
+evalClosureTab
+ :: forall (kk :: [Symbol]) vv x
+ . TCTab' Closure kk vv
+ -> TTab kk (Fmap ArgSym0 vv)
+ -> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv)
+ -> TTab kk (Fmap (ConstSym1 x) vv)
+evalClosureTab tab arg post =
+ -- we could do this:
+ -- let res = applyClosureTab tab arg
+ -- in applyClosureTabPost @_ @kk @(Fmap ResSym0 vv) res post
+ -- but it does not work as-is; we first have to:
+ -- write proofs (no-op functions) to convert
+ -- TCTab c kk (Fmap (f .@#@$$$ g) vv)
+ -- into
+ -- TCTab c kk (Fmap f (Fmap g vv))
+ -- in order to call applyClosureTabPost,
+ -- as well as proofs to convert
+ -- TCTab c kk (Fmap (ConstSym1 x) (Fmap f vv))
+ -- into
+ -- TCTab c kk (Fmap (ConstSym1 x) vv)
+ -- in order to return the result.
+ --
+ -- OTOH zipWith3TC inlines these proofs for us already, so we use that
+ zipWith3TC @_ @_ @_ @_ @_ @ArgSym0 @(ResCont x) @(ConstSym1 x) tab arg post
+ $ \_ cl _ a _ p -> (applyPost p (apply cl a), Dict)
+
+
+-- | Create a table of closures from a table of pre-closures.
+--
+-- We apply the relevant constraints and environment arguments,
+-- statically-known at compile time.
+mkClosureTab
+ :: forall c1 kk vv
+ . ConstrainList (Fmap CxtSym0 vv)
+ => ConstrainList (ZipWith (ConstSym1 (TyCon1 PreClosure)) kk vv)
+ => TTab kk vv
+ -> TCTab c1 kk (Fmap EnvSym0 vv)
+ -> TCTab' Closure kk (Fmap PartSym0 vv)
+mkClosureTab = applyClosureTabPre . strengthenTC0
+
+-- | @RepClosure c g k v@ is a constraint comprising:
+--
+-- * @RepVal g (Arg v) k@
+-- * @c k (Res v)@
+-- * @Closure v@
+--
+-- modulo singletons defunctionalisation on @c@.
+type RepClosure c g
+ = RepExtSym3
+ (AndC2 (ConstSym1 (TyCon1 Closure)) (FlipSym2 (.@#@$) ResSym0 .@#@$$$ c))
+ g
+ ArgSym0
+
+-- | A 'RepClosure' whose result is exactly @r@.
+type RepClosure' r g = RepClosure (ConstSym1 (TyCon1 ((~) r))) g
+
+-- | Convert a 'Closure' table into a 'RepClosure' table, deducing constraints.
+--
+-- This is used to convert the result of 'mkClosureTab' into a form that can be
+-- passed to the other functions e.g. 'evalSomeClosure'.
+repClosureTab
+ :: forall c g (kk :: [Symbol]) vv
+ . ConstrainList (ZipWith (FlipSym2 (.@#@$) ResSym0 .@#@$$$ c) kk vv)
+ => ConstrainList
+ (ZipWith (FlipSym1 (TyCon2 (RepVal g) .@#@$$$ ApplySym1 ArgSym0)) kk vv)
+ => TCTab' Closure kk vv
+ -> TCTab (RepClosure c g) kk vv
+repClosureTab = strengthenTC . strengthenTC
+
+-- | Apply a closure table to a single input and a post-processing table,
+-- giving a single result (if the input key was found).
+--
+-- This is the statically-typed version; for a version that runs for unknown
+-- keys see 'withEvalSomeClosureCts'.
+withEvalClosureCts
+ :: forall c g (k :: Symbol) (kk :: [Symbol]) vv x
+ . TCTab (RepClosure c g) kk vv
+ -> SKeyed k g
+ -> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv)
+ -> Either SKeyedError x
+withEvalClosureCts tab val post = gwithStatic @_ @_ @(ResCont x) tab val post
+ $ \_ cont cl -> applyPost cont . apply cl
+
+-- | Apply a closure table to a single input and a post-processing table,
+-- giving a single result (if the input key was found).
+--
+-- This is the dynamically-typed version; for a version that type-checks for
+-- statically-known keys see 'withEvalClosureCts'.
+withEvalSomeClosureCts
+ :: forall c g (kk :: [Symbol]) vv x
+ . TCTab (RepClosure c g) kk vv
+ -> ClosureApply g
+ -> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv)
+ -> Either SKeyedError x
+withEvalSomeClosureCts tab ext post =
+ withSKeyedExt ext $ \val -> withEvalClosureCts tab val post
+
+-- | Apply a closure table to a single input, and pass the constrained result
+-- to a continuation (if the input key was found).
+--
+-- This is the statically-typed version; for a version that runs for unknown
+-- keys see 'withEvalSomeClosureCxt'.
+withEvalClosureCxt
+ :: forall c f g (k :: Symbol) (kk :: [Symbol]) vv r
+ . TCTab (RepClosure c g) kk vv
+ -> SKeyed k g
+ -> ( forall k' v
+ . 'Just '(k', v) ~ LookupKV k kk vv
+ => ProofLookupKV f k kk vv
+ => (c @@ k' @@ Res v) => Sing k' -> Res v -> r
+ )
+ -> Either SKeyedError r
+withEvalClosureCxt tab val go =
+ withStaticCxt @_ @f tab val $ \k' cl a -> go k' (apply cl a)
+
+-- | Apply a closure table to a single input, and pass the constrained result
+-- to a continuation (if the input key was found).
+--
+-- This is the dynamically-typed version; for a version that type-checks for
+-- statically-known keys see 'withEvalClosureCxt'.
+withEvalSomeClosureCxt
+ :: forall c f g (kk :: [Symbol]) vv r
+ . TCTab (RepClosure c g) kk vv
+ -> ClosureApply g
+ -> ( forall k k' v
+ . 'Just '(k', v) ~ LookupKV k kk vv
+ => ProofLookupKV f k kk vv
+ -- keep above constraints; caller can either use or ignore as they wish
+ -- without them, caller is prevented from using them at all
+ => (c @@ k' @@ Res v) => Sing k' -> Res v -> r
+ )
+ -> Either SKeyedError r
+withEvalSomeClosureCxt tab ext go = withSKeyedExt ext
+ $ \(val :: SKeyed k g) -> withEvalClosureCxt @_ @f tab val (go @k)
+
+-- | Evaluate a closure application with statically-known type, against a table
+-- of closures, that all have the same result type.
+evalClosure
+ :: forall g (k :: Symbol) (kk :: [Symbol]) vv r
+ . TCTab (RepClosure' r g) kk vv
+ -> SKeyed k g
+ -> Either SKeyedError r
+evalClosure tab val = withEvalClosureCxt tab val $ const id
+
+-- | Evaluate a closure application with statically-unknown type, against a
+-- table of closures, that all have the same result type.
+evalSomeClosure
+ :: forall g (kk :: [Symbol]) vv r
+ . TCTab (RepClosure' r g) kk vv
+ -> ClosureApply g
+ -> Either SKeyedError r
+evalSomeClosure tab ext = withSKeyedExt ext $ evalClosure tab
diff --git a/src/Control/Static/Common.hs b/src/Control/Static/Common.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Static/Common.hs
@@ -0,0 +1,300 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Control.Static.Common where
+
+-- external
+import Data.Constraint ((:-) (..), Class (..), Dict (..))
+import Data.Kind (Constraint, Type)
+import Data.Singletons.Prelude
+import Data.Singletons.TH (genDefunSymbols, singletons)
+
+
+-- | Type family representing the type of a continuation.
+type family TyCont r (a :: Type) where
+ TyCont r a = a -> r
+genDefunSymbols [''TyCont]
+
+-- | Type family representing the type of a continuation of 2 args.
+type family TyCont2 r (a1 :: Type) (a2 :: Type) where
+ TyCont2 r a1 a2 = a1 -> a2 -> r
+genDefunSymbols [''TyCont2]
+
+-- | Type family representing the type of a continuation of 3 args.
+type family TyCont3 r (a1 :: Type) (a2 :: Type) (a3 :: Type) where
+ TyCont3 r a1 a2 a3 = a1 -> a2 -> a3 -> r
+genDefunSymbols [''TyCont3]
+
+singletons [d|
+ -- -| S combinator, not yet in singletons
+ -- https://github.com/goldfirere/singletons/issues/455
+ ap :: (x -> y -> z) -> (x -> y) -> (x -> z)
+ ap f g x = f x (g x)
+ |]
+
+
+-- | Data type wrapping a constraint, to avoid ImpredicativeTypes GHC error.
+newtype CxtW c a = CxtW { unCxtW :: c => a }
+
+-- | Convert a list of constraints into a single constraint
+type family ConstrainList (cc :: [Constraint]) :: Constraint where
+ ConstrainList '[] = ()
+ ConstrainList (c ': cc) = (c, ConstrainList cc)
+
+-- | Null constraint over 1 type param.
+type family NullC (t :: k) :: Constraint where
+ NullC t = ()
+genDefunSymbols [''NullC]
+
+-- | Null constraint over 2 type params.
+type family NullC2 (t :: k) (t' :: k') :: Constraint where
+ NullC2 t t' = ()
+genDefunSymbols [''NullC2]
+
+-- | Combine two constraints
+type family AndC c0 c1 :: Constraint where
+ AndC c0 c1 = (c0, c1)
+genDefunSymbols [''AndC]
+
+-- | Combine two constraint constructors into a single constraint constructor.
+--
+-- This is analogous to the term-level idiom @ap ((,) . c0) c1@ that combines
+-- two functions c0, c1 into a single one.
+type AndC1 c0 c1 = ApSym2 (AndCSym0 .@#@$$$ c0) c1
+
+-- | Combine two constraint constructors, each taking 2 type params, into
+-- a single constraint constructor taking 2 type params.
+--
+-- This is analogous to the term-level idiom @ap (ap . ((,) .) . c0) c1@ that
+-- combines two functions c0, c1 that each take 2 params, into a single one.
+type AndC2 c0 c1 = ApSym2 (ApSym0 .@#@$$$ (.@#@$$) AndCSym0 .@#@$$$ c0) c1
+
+-- | Entailment over 2 type params.
+type family Class2 c0 c1 t t' where
+ Class2 c0 c1 t t' = Class (c0 @@ t @@ t') (c1 @@ t @@ t')
+genDefunSymbols [''Class2]
+
+
+singletons [d|
+ -- note: subexpressions are lifted out to the top-level due to
+ -- https://github.com/goldfirere/singletons/issues/339#issuecomment-612530482
+
+ lookupKV :: Eq k => k -> [k] -> [v] -> Maybe (k, v)
+ lookupKV k [] [] = Nothing
+ lookupKV k (k':kk) (v':vv) = lookupKV_If k k' kk v' vv (k == k')
+
+ lookupKV_If :: Eq k => k -> k -> [k] -> v -> [v] -> Bool -> Maybe (k, v)
+ lookupKV_If k k' _ v' _ True = Just (k', v')
+ lookupKV_If k _ kk _ vv False = lookupKV k kk vv
+ |]
+
+{-
+Proof that fmap f (lookupKV k kk vv) == lookupKV k kk (fmap f vv)
+
+The proof roughly follows the below structure, modulo the fact that we split
+out lookupKV into 2 functions due to a singletons / template-haskell issue,
+discussed in the link above.
+
+Inducting on kk vv:
+
+Given:
+Wf. (Fmap f (LookupKV k kk vv) ~ LookupKV k kk (Fmap f vv))
+Sf. Just (f @@ v') ~ Fmap f (Just v')
+Tf. f @@ v' ': Fmap f vv ~ Fmap f (v' ': vv)
+
+Deduce:
+(Fmap f (LookupKV k (k' ': kk) (v' ': vv)) ~ LookupKV k (k' ': kk) (Fmap f (v' ': vv)))
+ by (Tf), ~
+ LookupKV k (k' ': kk) (f @@ v' ': Fmap f vv)
+
+if k == k' if k == k'
+ then -> Fmap f (Just v') by (Sf) ~ then -> Just (f @@ v')
+ else -> Fmap f (LookupKV k kk vv) by (Wf) ~ else -> Lookup k kk (Fmap f vv)
+
+[].
+
+Note that GHC deduces Sf and Tf automatically, so they don't need to appear
+explicitly in the code proof below.
+-}
+
+class (Fmap (FmapSym1 f) (LookupKV k kk vv) ~
+ LookupKV k kk (Fmap f vv))
+ => ProofLookupKV f k (kk :: [kt]) vv where
+instance -- base case
+ ProofLookupKV f k '[] '[]
+instance -- implicit (f @@ v' ': Fmap f vv ~ Fmap f (v' ': vv)) =>
+ (ProofLookupKV_If f k k' kk v' vv (k == k'))
+ => ProofLookupKV f (k :: kt) (k' ': kk) (v' ': vv)
+
+class (Fmap (FmapSym1 f) (LookupKV_If k k' kk v' vv eq) ~
+ LookupKV_If k k' kk (f @@ v') (Fmap f vv) eq)
+ => ProofLookupKV_If f (k :: kt) k' kk v' vv eq where
+instance -- implicit (Just (f @@ v') ~ Fmap f (Just v')) =>
+ ProofLookupKV_If f k k' kk v' vv 'True -- Just v
+instance
+ ProofLookupKV f k kk vv
+ => ProofLookupKV_If f k k' kk v' vv 'False -- lookupKV kk vv
+
+
+-- | Maybe that carries its type.
+data TMaybe (t :: Maybe k) where
+ TNothing :: TMaybe 'Nothing
+ TJust :: !t -> TMaybe ('Just t)
+
+-- | Heterogeneous constrained table.
+data TCTab (c :: kt ~> Type ~> Constraint) (kk :: [kt]) (vv :: [Type]) :: Type where
+ TCNil :: TCTab c '[] '[]
+ TCCons :: (c @@ k @@ v) => !(Sing (k :: kt)) -> !v -> !(TCTab c kk vv) -> TCTab c (k : kk) (v : vv)
+
+-- | A 'TCTab' with a constraint that applies only to the value, not the key.
+type TCTab' c = TCTab (ConstSym1 (TyCon1 c))
+
+-- | Heterogeneous unconstrained table.
+--
+-- To add or remove constraints, see 'strengthenTC0', 'strengthenTC' and
+-- 'weakenTC'.
+type TTab = TCTab NullC2Sym0
+
+-- | Result type of 'lookupTC'.
+data TCMaybe c (t :: Maybe (kt, Type)) where
+ TCNothing :: TCMaybe c 'Nothing
+ TCJust :: Dict (c @@ k @@ v) -> !(Sing k) -> !v -> TCMaybe c ('Just '(k, v))
+
+-- | Lookup an element in the table, and generate some proofs about the result
+-- that can be used by the caller.
+lookupTC
+ :: forall kt c f (k :: kt) (kk :: [kt]) vv
+ . SEq kt
+ => Sing k
+ -> TCTab c kk vv
+ -> (TCMaybe c (LookupKV k kk vv), Dict (ProofLookupKV f k kk vv))
+lookupTC k TCNil = (TCNothing, Dict)
+lookupTC k (TCCons k' v tab) = case k %== k' of
+ STrue -> (TCJust Dict k' v, Dict)
+ SFalse -> case lookupTC @kt @c @f k tab of
+ (res, Dict) -> (res, Dict) -- generate new proof from old proof
+
+-- | Lookup two elements in two related tables.
+--
+-- The types of the outputs are provably related.
+lookupTC2
+ :: forall kt c0 c1 f (k :: kt) (kk :: [kt]) vv
+ . SEq kt
+ => Sing k
+ -> TCTab c0 kk vv
+ -> TCTab c1 kk (Fmap f vv)
+ -> ( TCMaybe c0 (LookupKV k kk vv)
+ , TCMaybe c1 (Fmap (FmapSym1 f) (LookupKV k kk vv))
+ )
+lookupTC2 k TCNil TCNil = (TCNothing, TCNothing)
+lookupTC2 k (TCCons k' v tab) (TCCons k'' p post) = case k %== k' of
+ STrue -> (TCJust Dict k' v, TCJust Dict k'' p)
+ SFalse -> lookupTC2 @kt @c0 @c1 @f k tab post
+
+-- | Zip two related tables, giving a third table related to both.
+--
+-- The types of the outputs are provably related.
+zipWithTC
+ :: forall kt c0 c1 cr f1 r (kk :: [kt]) vv
+ . TCTab c0 kk vv
+ -> TCTab c1 kk (Fmap f1 vv)
+ -> ( forall k0 k1 v
+ . (c0 @@ k0 @@ v)
+ => (c1 @@ k1 @@ (f1 @@ v))
+ => Sing k0
+ -> v
+ -> Sing k1
+ -> (f1 @@ v)
+ -> (r @@ v, Dict (cr @@ k0 @@ (r @@ v)))
+ )
+ -> TCTab cr kk (Fmap r vv)
+zipWithTC TCNil TCNil f = TCNil
+zipWithTC (TCCons k0 v t0) (TCCons k1 f1v t1) f = case f k0 v k1 f1v of
+ (v', Dict) -> TCCons k0 v' (zipWithTC @kt @c0 @c1 @cr @f1 @r t0 t1 f)
+
+-- | Zip three related tables, giving a fourth table related to both.
+--
+-- The types of the outputs are provably related.
+zipWith3TC
+ -- brittany-disable-next-binding
+ -- https://github.com/lspitzner/brittany/issues/299
+ :: forall kt c0 c1 c2 cr f1 f2 r (kk :: [kt]) vv
+ . TCTab c0 kk vv
+ -> TCTab c1 kk (Fmap f1 vv)
+ -> TCTab c2 kk (Fmap f2 vv)
+ -> ( forall k0 k1 k2 v
+ . (c0 @@ k0 @@ v)
+ => (c1 @@ k1 @@ (f1 @@ v))
+ => (c2 @@ k2 @@ (f2 @@ v))
+ => Sing k0 -> v
+ -> Sing k1 -> f1 @@ v
+ -> Sing k2 -> f2 @@ v
+ -> (r @@ v, Dict (cr @@ k0 @@ (r @@ v)))
+ )
+ -> TCTab cr kk (Fmap r vv)
+zipWith3TC TCNil TCNil TCNil f = TCNil
+zipWith3TC (TCCons k0 v t0) (TCCons k1 f1v t1) (TCCons k2 f2v t2) f =
+ case f k0 v k1 f1v k2 f2v of
+ (v', Dict) ->
+ TCCons k0 v' (zipWith3TC @kt @c0 @c1 @c2 @cr @f1 @f2 @r t0 t1 t2 f)
+
+type DictOf c = TyCon1 Dict .@#@$$$ c
+
+withTCDict
+ :: forall kt c0 c (kk :: [kt]) vv r
+ . TCTab c0 kk vv
+ -> TTab kk (Fmap (DictOf c) vv)
+ -> (ConstrainList (Fmap c vv) => r)
+ -> r
+withTCDict TCNil TCNil f = f
+withTCDict (TCCons _ _ tv) (TCCons _ Dict tc) f = withTCDict @_ @_ @c tv tc f
+
+toTCDict
+ :: forall kt c0 c (kk :: [kt]) vv
+ . ConstrainList (Fmap c vv)
+ => TCTab c0 kk vv
+ -> TTab kk (Fmap (DictOf c) vv)
+toTCDict TCNil = TCNil
+toTCDict (TCCons k _ xs) = TCCons k Dict (toTCDict @_ @_ @c xs)
+
+-- | Weaken the constraint on a 'TCTab'.
+weakenTC
+ :: forall kt c0 c1 (kk :: [kt]) vv
+ . ConstrainList (ZipWith (Class2Sym2 c1 c0) kk vv)
+ => TCTab c0 kk vv
+ -> TCTab c1 kk vv
+weakenTC TCNil = TCNil
+weakenTC (TCCons (k :: Sing k) (v :: v) tab) =
+ case cls @(c1 @@ k @@ v) @(c0 @@ k @@ v) of
+ Sub Dict -> TCCons k v (weakenTC tab)
+
+-- | Strengthen the constraint on a 'TCTab'.
+strengthenTC
+ :: forall kt c0 c1 (kk :: [kt]) vv
+ . ConstrainList (ZipWith c1 kk vv)
+ => TCTab c0 kk vv
+ -> TCTab (AndC2 c0 c1) kk vv
+strengthenTC TCNil = TCNil
+strengthenTC (TCCons k v xs) = TCCons k v (strengthenTC @_ @_ @c1 xs)
+
+-- | Strengthen the constraint on a 'TTab'.
+strengthenTC0
+ :: forall kt c1 (kk :: [kt]) vv
+ . ConstrainList (ZipWith c1 kk vv)
+ => TTab kk vv
+ -> TCTab c1 kk vv
+strengthenTC0 TCNil = TCNil
+strengthenTC0 (TCCons k v xs) = TCCons k v (strengthenTC0 @_ @c1 xs)
diff --git a/src/Control/Static/Serialise.hs b/src/Control/Static/Serialise.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Static/Serialise.hs
@@ -0,0 +1,164 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Control.Static.Serialise where
+
+-- external
+import qualified Codec.Serialise as SR
+import qualified Data.Binary as BN
+import qualified Data.ByteString.Lazy as LBS
+
+import Codec.Serialise (Serialise)
+import Data.Binary (Binary)
+import Data.Dynamic (Dynamic, fromDynamic, toDyn)
+import Data.Kind (Type)
+import Data.Singletons (Sing)
+import Data.Singletons.TH (genDefunSymbols)
+import GHC.Generics (Generic)
+import Type.Reflection ((:~~:) (..), TypeRep, Typeable,
+ eqTypeRep, typeRep)
+
+
+-- | Serialisable external value, with an associated static-key.
+--
+-- @g@ is a type that can generically represent all the external interface of
+-- your static values. See 'RepVal' and 'DoubleEncoding' for more details.
+data SKeyedExt g = SKeyedExt !String !g
+ deriving (Read, Show, Generic, Binary, Serialise, Eq, Ord, Functor)
+
+-- | Possible errors when resolving a key in a static table.
+data SKeyedError =
+ SKeyedNotFound String
+ | SKeyedExtDecodeFailure String
+ deriving (Read, Show, Generic, Binary, Serialise, Eq, Ord)
+
+-- | A value and its external representation, indexed by some key.
+class RepVal g (v :: Type) (k :: kt) where
+ -- | Convert an external value into its generic representation.
+ toRep :: Sing k -> v -> g
+ -- | Convert a generic representation into its external value.
+ --
+ -- This may fail, since @g@ may have to represent several other @v'@ as well,
+ -- which @k@ should help determine.
+ fromRep :: Sing k -> g -> Either String v
+genDefunSymbols [''RepVal]
+
+castOrFail :: forall s t . (Typeable s, Typeable t) => s -> Either String t
+castOrFail s = case reps `eqTypeRep` rept of
+ Just HRefl -> Right s
+ Nothing ->
+ Left
+ $ "fromTypeable: type-mismatch, expecting: "
+ <> show rept
+ <> "; actual: "
+ <> show reps
+ where
+ rept = typeRep :: TypeRep t
+ reps = typeRep :: TypeRep s
+
+-- | 'RepVal' instance for 'Dynamic'.
+--
+-- Note that by nature this is not serialisable, and is only really meant for
+-- testing purposes. Neither can it support a generic 'Eq' or 'Ord' instance;
+-- if you need that then try 'DSerialise' or 'DBinary'.
+instance Typeable v => RepVal Dynamic v k where
+ toRep _ = toDyn
+ fromRep _ s = case fromDynamic s of
+ Nothing -> Left "fromDynamic failed; type-mismatch"
+ -- annoyingly, Dynamic doesn't expose the type for us to print it, nor the
+ -- value for us to pass it to castOrFail. If you replace this subexpression
+ -- with castOrFail this will type-check as it will try to cast the Dynamic
+ -- itself, and always fail at runtime.
+ Just v -> Right v
+
+-- | Uniform generic wrapper.
+--
+-- In a type-safe language like Haskell, one needs to know in advance the type
+-- of something in order to deserialise it successfully. In many applications
+-- however, the point at which data enters the program is separate from the
+-- point at which we have enough type information to fully deserialise a
+-- statically-keyed value. Between these points, we often want to deserialise
+-- the /other/ parts of that data, and perform logic based on its value.
+--
+-- This wrapper works around that fact by double-encoding the static-value.
+-- This is perhaps suboptimal performance-wise, but is simple to implement and
+-- use, especially in a compositional manner. When data first enters the
+-- program, one can deserialise the whole data using the mechanism represented
+-- by @s@, which will then contain @'HalfEncoded' b@ instances of this type
+-- inside it. When you finally have enough type information to perform the rest
+-- of the deserialise you can call 'fromRep' on these parts, to recovered the
+-- typed value corresponding to each part.
+--
+-- This wrapper also short-circuits the case of calling 'toRep' then 'fromRep'
+-- without attempting to serialise the value in between. In this case the
+-- original value is simply wrapped in the 'Decoded' constructor, no attempt to
+-- serialise based on @s@ is actually made, and no value based on @b@ is ever
+-- constructed.
+--
+-- If you need optimal performance and really must avoid double-serialising,
+-- you can instead define your own ADT as a sum-type over all your possible
+-- serialisation types, make this serialisable, and implement 'RepVal' for it.
+--
+-- @s@ is a constraint over serialisable types, e.g 'Serialise' or 'Binary'.
+-- @b@ is the concrete serialisation type, e.g. 'LBS.ByteString'.
+data DoubleEncoding s b where
+ Decoded :: (Typeable t, s t) => !t -> DoubleEncoding s b
+ HalfEncoded :: !b -> DoubleEncoding s b
+
+type DSerialise = DoubleEncoding Serialise LBS.ByteString
+
+instance Serialise DSerialise where
+ encode (Decoded t) = SR.encode
+ (HalfEncoded (SR.serialise t) :: DoubleEncoding Serialise LBS.ByteString)
+ encode (HalfEncoded t) = SR.encode t
+ decode = HalfEncoded <$> SR.decode
+
+instance (Typeable v, Serialise v) => RepVal DSerialise v k where
+ toRep _ = Decoded
+ fromRep _ (Decoded v) = castOrFail v
+ fromRep _ (HalfEncoded s) = case SR.deserialiseOrFail s of
+ Left e -> Left (show e)
+ Right v -> Right v
+
+instance Eq DSerialise where
+ a == b = SR.serialise a == SR.serialise b
+
+instance Ord DSerialise where
+ compare a b = compare (SR.serialise a) (SR.serialise b)
+
+type DBinary = DoubleEncoding Binary LBS.ByteString
+
+decodeFullyOrFail :: Binary a => LBS.ByteString -> Either String a
+decodeFullyOrFail s = case BN.decodeOrFail s of
+ Left e -> Left ("Data.Binary decode failure: " <> show e)
+ Right (bs, o, v) -> if LBS.null bs
+ then Right v
+ else Left ("Data.Binary decode leftovers: " <> show (bs, o))
+
+instance Binary DBinary where
+ put (Decoded t) =
+ BN.put (HalfEncoded (BN.encode t) :: DoubleEncoding Binary LBS.ByteString)
+ put (HalfEncoded t) = BN.put t
+ get = HalfEncoded <$> BN.get
+
+instance (Typeable v, Binary v) => RepVal DBinary v k where
+ toRep _ = Decoded
+ fromRep _ (Decoded v) = castOrFail v
+ fromRep _ (HalfEncoded s) = decodeFullyOrFail s
+
+instance Eq DBinary where
+ a == b = BN.encode a == BN.encode b
+
+instance Ord DBinary where
+ compare a b = compare (BN.encode a) (BN.encode b)
diff --git a/src/Control/Static/Static.hs b/src/Control/Static/Static.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Static/Static.hs
@@ -0,0 +1,167 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Control.Static.Static where
+
+-- external
+import Data.Constraint (Dict (..))
+import Data.Kind (Type)
+import Data.Singletons.Prelude
+import Data.Singletons.TH (genDefunSymbols)
+import Data.Text (pack, unpack)
+
+-- internal
+import Control.Static.Common
+import Control.Static.Serialise
+
+
+-- | Standalone static key with no associated value.
+--
+-- Users typically don't need this, and should use 'SKeyed' or 'SKeyedExt'
+-- as appropriate.
+type SKey (k :: Symbol) = Sing k
+
+-- | Internal value, typed-indexed by an associated static-key.
+--
+-- Generally, @v@ is not expected to be serialisable or otherwise representable
+-- outside of the program. For cases where it is, you should define an instance
+-- of 'RepVal'. That then enables you to use 'toSKeyedExt' and
+-- other utility functions with this constraint.
+data SKeyed k v = SKeyed !(SKey k) !v
+ deriving Functor
+
+-- | Similar to 'withSomeSing' for a 'SKeyedExt', extract the type from
+-- the 'String' key and run a typed function on the typed value.
+withSKeyedExt :: SKeyedExt g -> (forall (a :: Symbol) . SKeyed a g -> r) -> r
+withSKeyedExt (SKeyedExt s a) f = withSomeSing (pack s) $ \k -> f (SKeyed k a)
+
+-- | Convert an internal value to an external value, depending on the existence
+-- of an instance of 'RepVal' to help perform the conversion.
+toSKeyedExt :: RepVal g v k => SKeyed k v -> SKeyedExt g
+toSKeyedExt (SKeyed k v) = SKeyedExt (unpack (fromSing k)) (toRep k v)
+
+toSKeyedEither
+ :: Sing (k :: Symbol) -> Maybe (Either String v) -> Either SKeyedError v
+toSKeyedEither k Nothing = Left $ SKeyedNotFound $ unpack $ fromSing k
+toSKeyedEither _ (Just (Left e)) = Left $ SKeyedExtDecodeFailure e
+toSKeyedEither _ (Just (Right v)) = Right v
+
+-- | Helper function for building 'TCTab's.
+skeyedCons
+ :: (c @@ k @@ v) => SKeyed k v -> TCTab c kk vv -> TCTab c (k ': kk) (v ': vv)
+skeyedCons (SKeyed k v) = TCCons k v
+
+-- | @RepExt c g ext k v@ is a constraint comprising:
+--
+-- * @RepVal g (ext v) k@
+-- * @c k v@
+--
+-- modulo singletons defunctionalisation on @c@ and @ext@.
+type RepExtSym3 c g ext
+ = AndC2 c (FlipSym1 (TyCon2 (RepVal g) .@#@$$$ ApplySym1 ext))
+{- Implementation note: this is equivalent to:
+
+type family RepExt c g ext k v :: Constraint where
+ RepExt c g ext k v = (c @@ k @@ v, RepVal g (ext @@ v) k)
+genDefunSymbols [''RepExt]
+
+However it must be of the form @AndC2 x y@ so that we can define 'repClosureTab'
+in terms of 'strengthenTC', which uses 'AndC2'.
+-}
+
+-- | A continuation from an internal and external value, to a result type @r@.
+type family TyContIX r ext (v :: Type) where
+ TyContIX r ext v = v -> ext @@ v -> r
+genDefunSymbols [''TyContIX]
+--type TyContIXSym2 r ext
+-- = ApSym2 (TyCon2 (->)) ((FlipSym1 (TyCon2 (->)) @@ r) .@#@$$$ ApplySym1 ext)
+
+-- | Given an 'SKeyed' of an external value @g@, do the following:
+--
+-- 1. Lookup the corresponding internal value (I) of type @v@.
+-- 2. Decode the external value (X) of type @g@, if its type can be decoded
+-- into the type @ext v@.
+-- 3. Lookup the corresponding continuation (C).
+-- 4. Apply (C) to (I) and (X), returning a value of type @r@.
+gwithStatic
+ :: forall c0 c1 f g ext (k :: Symbol) (kk :: [Symbol]) vv r
+ . TCTab (RepExtSym3 c0 g ext) kk vv
+ -> SKeyed k g
+ -> TCTab c1 kk (Fmap f vv)
+ -> ( forall k' v
+ . 'Just '(k', v) ~ LookupKV k kk vv
+ => 'Just '(k', f @@ v) ~ Fmap (FmapSym1 f) (LookupKV k kk vv)
+ => (c0 @@ k' @@ v)
+ => (c1 @@ k' @@ (f @@ v))
+ => Sing k'
+ -> (f @@ v)
+ -> v
+ -> (ext @@ v)
+ -> r
+ )
+ -> Either SKeyedError r
+gwithStatic tab val@(SKeyed k ga) post go =
+ toSKeyedEither k $ case lookupTC2 @_ @_ @_ @f k tab post of
+ (TCNothing , TCNothing ) -> Nothing
+ (TCJust Dict k' v, TCJust Dict _ p) -> Just $ go k' p v <$> fromRep k' ga
+ -- note: yes, it's possible to implement this in terms of withStaticCxt
+ -- IMO this version is a bit nicer
+
+withStaticCts
+ :: forall c0 c1 g ext (k :: Symbol) (kk :: [Symbol]) vv r
+ . TCTab (RepExtSym3 c0 g ext) kk vv
+ -> SKeyed k g
+ -> TCTab c1 kk (Fmap (TyContIXSym2 r ext) vv)
+ -> Either SKeyedError r
+withStaticCts tab val post =
+ gwithStatic @_ @_ @(TyContIXSym2 r ext) tab val post (flip const)
+
+withSomeStaticCts
+ :: forall c0 c1 g ext (kk :: [Symbol]) vv r
+ . TCTab (RepExtSym3 c0 g ext) kk vv
+ -> SKeyedExt g
+ -> TCTab c1 kk (Fmap (TyContIXSym2 r ext) vv)
+ -> Either SKeyedError r
+withSomeStaticCts tab ext post =
+ withSKeyedExt ext $ \(val :: SKeyed k g) -> withStaticCts tab val post
+
+withStaticCxt
+ :: forall c f g ext (k :: Symbol) (kk :: [Symbol]) vv r
+ . TCTab (RepExtSym3 c g ext) kk vv
+ -> SKeyed k g
+ -> ( forall k' v
+ . 'Just '(k', v) ~ LookupKV k kk vv
+ => ProofLookupKV f k kk vv
+ => (c @@ k' @@ v) => Sing k' -> v -> (ext @@ v) -> r
+ )
+ -> Either SKeyedError r
+withStaticCxt tab val@(SKeyed k ga) go =
+ toSKeyedEither k $ case lookupTC @_ @_ @f k tab of
+ (TCNothing , _ ) -> Nothing
+ (TCJust Dict k' v, Dict) -> Just $ go k' v <$> fromRep k' ga
+
+withSomeStaticCxt
+ :: forall c f g ext (kk :: [Symbol]) vv r
+ . TCTab (RepExtSym3 c g ext) kk vv
+ -> SKeyedExt g
+ -> ( forall k k' v
+ . 'Just '(k', v) ~ LookupKV k kk vv
+ => ProofLookupKV f k kk vv
+ -- keep above constraints; caller can either use or ignore as they wish
+ -- without them, caller is prevented from using them at all
+ => (c @@ k' @@ v) => Sing k' -> v -> (ext @@ v) -> r
+ )
+ -> Either SKeyedError r
+withSomeStaticCxt tab ext go =
+ withSKeyedExt ext $ \(val :: SKeyed k g) -> withStaticCxt @_ @f tab val (go @k)
diff --git a/src/Control/Static/TH.hs b/src/Control/Static/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Static/TH.hs
@@ -0,0 +1,227 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Control.Static.TH
+ ( staticRef
+ , staticKey
+ , staticKeyType
+ , mkStatics
+ , mkStaticsWithRefs
+ , defaultStaticTab
+ , mkDefStaticTab
+ , mkStaticTab
+ -- special utils some users might need
+ , CxtW(..)
+ )
+where
+
+-- external
+import Control.Concurrent.MVar (newEmptyMVar, putMVar, takeMVar)
+import Data.Functor (($>))
+import Data.List (unzip5)
+import Data.Singletons (sing)
+import GHC.IO.Unsafe (unsafeDupableInterleaveIO)
+import Language.Haskell.TH
+
+-- internal
+import Control.Static.Common (CxtW (..), TCTab (..), TTab)
+import Control.Static.Static (SKeyed (..), skeyedCons)
+
+
+-- | Needed for 'mkStaticsWithRefs', definition taken from
+-- https://gitlab.haskell.org/ghc/ghc/issues/12073
+mfixQ :: (b -> Q b) -> Q b
+mfixQ k = do
+ m <- runIO newEmptyMVar
+ ans <- runIO (unsafeDupableInterleaveIO (takeMVar m))
+ result <- k ans
+ runIO (putMVar m result)
+ pure result
+
+-- | Create top-level statically-keyed values from regular top-level values.
+mkStatics :: [Name] -> Q [Dec]
+mkStatics ns = mapM getType ns >>= createStatics Nothing
+
+-- | Create top-level statically-keyed values from regular top-level values,
+-- when their definitions need to refer to other statically-keyed values.
+--
+-- Since TH cannot handle references to names defined later in the source file,
+-- it is not possible to use 'mkStatics' for this purpose; you must use this
+-- function instead, and then register the names later using 'mkStaticTab'.
+--
+-- See unit tests for example usage.
+mkStaticsWithRefs :: ([Exp] -> Q [Dec]) -> Q [Dec]
+mkStaticsWithRefs mkDecs = do
+ statics <- mfixQ f
+ decls <- mkDecs statics
+ closures <- createStatics Nothing (sigsOf decls)
+ pure $ decls <> closures
+ where
+ -- note: f must be like this; as per the contract to 'mfix' one must not
+ -- evaluate its argument in the definition, or we'll get an infinite loop
+ f :: ([Exp] -> Q [Exp])
+ f statics = do
+ decls <- mkDecs statics
+ traverse (staticRef . fst) (sigsOf decls)
+
+defaultStaticTab :: Name
+defaultStaticTab = mkName "staticTab"
+
+-- | Create a table holding the static values for a list of top-level names,
+-- binding it to the top-level name "staticTab".
+mkDefStaticTab :: [Name] -> Q [Dec]
+mkDefStaticTab = mkStaticTab defaultStaticTab
+
+-- | Create a table holding the static values for a list of top-level names,
+-- binding it to the given top-level name.
+mkStaticTab :: Name -> [Name] -> Q [Dec]
+mkStaticTab tabName ns = mapM getType ns >>= createStatics (Just tabName)
+
+-- | Refer to a static value, as a 'SKeyed'.
+--
+-- Be sure to pass the argument to 'mkStaticTab' so the referent exists.
+staticRef :: Name -> Q Exp
+staticRef = varE . staticName
+
+-- | Get the symbol key of a static value, as a 'Control.Static.SKey'.
+--
+-- Be sure to pass the argument to 'mkStaticTab' so the referent exists.
+--
+-- Users typically don't need this; 'staticRef' is more type-safe as it
+-- includes the type of the value, and this does not.
+staticKey :: Name -> Q Exp
+staticKey name = [| sing @ $(symFQN name) |]
+
+-- | Get the symbol key type of a static value, as a type-level string.
+staticKeyType :: Name -> Q Type
+staticKeyType = symFQN
+
+-- Internal
+
+createStatics :: Maybe Name -> [(Name, Type)] -> Q [Dec]
+createStatics tabName sigs = do
+ (closures, tyVars, keys, vals, inserts) <- unzip5 <$> mapM genStaticDefs sigs
+ staticTab <- maybe (pure [])
+ (\n -> genStaticTab n (concat tyVars) keys vals inserts)
+ tabName
+ pure $ concat closures <> staticTab
+
+genStaticTab :: Name -> [TyVarBndr] -> [Q Type] -> [Q Type] -> [Q Exp] -> Q [Dec]
+genStaticTab name tyVars keys vals is = sequence
+ [ sigD name $ do
+ ForallT tyVars [] <$> [t| TTab $(tyList keys) $(tyList vals) |]
+ , sfnD name $ apList is [| TCNil |]
+ ]
+
+genStaticDefs :: (Name, Type) -> Q ([Dec], [TyVarBndr], Q Type, Q Type, Q Exp)
+genStaticDefs (fullName, fullType) = do
+ tyTval <- [t| SKeyed |]
+ tyCxtw <- [t| CxtW |]
+ --fail $ show fullType
+ let (tyVars', tyCxt', typ') = case fullType of
+ ForallT vars cxt' mono -> (vars, cxt', mono)
+ _ -> ([], [], fullType)
+ let tyCxt1 = cxtToType tyCxt'
+
+ -- If there is a constraint, have it wrapped in a CxtW later
+ let cxtVal mk n = appE (conE 'CxtW) (mk n)
+ (maybeCxt, maybeCxtTy) = case tyCxt' of
+ [] -> (id, pure)
+ _ -> (cxtVal, \typ -> pure (tyCxtw `AppT` tyCxt1 `AppT` typ))
+
+ -- If the type is of the special forms
+ -- - (SKeyed s T -> T) or
+ -- - (C => SKeyed s (CxtW C T) -> T)
+ -- this means it wants the staticRef passed in as an argument, so arrange for
+ -- that to be done later too.
+ --
+ -- TODO: we probably don't need this, now that we have 'mkStaticsWithRefs'.
+ let
+ fixVal mk n = appE (mk n) (staticRef n)
+ (maybeFix, tyVars, typ) = case typ' of
+ ArrowT `AppT` (t `AppT` (VarT sym) `AppT` (c `AppT` cxt' `AppT` typ_)) `AppT` typX
+ | t == tyTval && c == tyCxtw && cxt' == tyCxt1 && typ_ == typX
+ -> (fixVal, filter (\v -> tyVarName v /= sym) tyVars', typX)
+
+ ArrowT `AppT` (tyTval' `AppT` (VarT sym) `AppT` typ_) `AppT` typX
+ | tyTval' == tyTval && typ_ == typX
+ -> (fixVal, filter (\v -> tyVarName v /= sym) tyVars', typX)
+
+ _ -> (id, tyVars', typ')
+
+ let mkVal = maybeCxt (maybeFix varE)
+ let tyK = symFQN fullName
+ let tyV = maybeCxtTy typ
+ let name = staticName fullName
+
+ -- define the static only if it wasn't already defined, e.g. via mkStaticsWithRefs
+ static <- flip recover (reify name $> []) $ sequence
+ [ sigD name $ ForallT tyVars [] <$> [t| SKeyed $(tyK) $(tyV) |]
+ , sfnD name [| SKeyed sing $(mkVal fullName) |]
+ ]
+ pure (static, tyVars, tyK, tyV, [| skeyedCons $(staticRef fullName) |])
+
+staticName :: Name -> Name
+staticName n = mkName $ nameBase n ++ "__static"
+
+-- Utils
+
+-- | Apply a list of expressions to a base expression.
+apList :: [Q Exp] -> Q Exp -> Q Exp
+apList [] base = base
+apList (e : es) base = [| $e $ $(apList es base) |]
+
+-- | Construct a promoted-list of types.
+tyList :: [Q Type] -> Q Type
+tyList [] = promotedNilT
+tyList (h : tl) = do
+ ty <- h
+ (PromotedConsT `AppT` ty `AppT`) <$> tyList tl
+
+-- | Convert a context (a list of types) to a single type.
+cxtToType :: Cxt -> Type
+cxtToType cxt' = case cxt' of
+ [] -> TupleT 0
+ [t] -> t
+ _ -> go (TupleT (length cxt')) cxt' where
+ go part [] = part
+ go part (h : tl) = go (part `AppT` h) tl
+
+-- | Look up the "original name" (module:name) and type of a top-level function
+getType :: Name -> Q (Name, Type)
+getType name = do
+ info <- reify name
+ case info of
+ VarI origName typ _ -> pure (origName, typ)
+ _ -> fail $ show name ++ " not a type: " ++ show info
+
+-- | Extract type info from top-level decls without using 'reify'.
+sigsOf :: [Dec] -> [(Name, Type)]
+sigsOf [] = []
+sigsOf (SigD n t : tl) = (n, simplifyType t) : sigsOf tl
+sigsOf (_ : tl) = sigsOf tl
+
+-- | Simplify a source-level type. This attempts to do what 'reify' does but
+-- without needing the definition to exist at the splice point.
+simplifyType :: Type -> Type
+simplifyType (ForallT t0 c0 (ForallT t1 c1 t)) =
+ simplifyType (ForallT (t0 <> t1) (c0 <> c1) t)
+simplifyType t = t
+
+-- | Variation on 'funD' which takes a single expression to define the function
+sfnD :: Name -> Q Exp -> Q Dec
+sfnD n e = funD n [clause [] (normalB e) []]
+
+-- | The name of a type variable binding occurrence
+tyVarName :: TyVarBndr -> Name
+tyVarName (PlainTV n ) = n
+tyVarName (KindedTV n _) = n
+
+-- | Fully qualified name, as a type-level String literal of kind Symbol
+symFQN :: Name -> Q Type
+symFQN n = do
+ loc <- location
+ pure $ LitT $ StrTyLit $ loc_module loc ++ "." ++ nameBase n
diff --git a/static.cabal b/static.cabal
new file mode 100644
--- /dev/null
+++ b/static.cabal
@@ -0,0 +1,185 @@
+Cabal-Version: 3.0
+Name: static
+Version: 0.1.0.0
+Synopsis: Type-safe and interoperable static values and closures
+Description:
+ Serialise closures in a type-safe way that interoperates across binaries.
+
+ This package is inspired by @distributed-static@ and GHC's /static pointers/
+ in @GHC.StaticPtr@, which came out of the same research. However, we make
+ some significantly-different design choices, described below.
+
+ GHC made the design choice to focus on guaranteeing that static values could
+ be passed between nodes if they were running the exact same binary, since
+ they are indexed by 64-bit integers automatically-generated by the compiler.
+ @distributed-static@ attempts to support the same source program compiled by
+ different versions of GHC. As part of this effort to preserve stability, one
+ must pass in a table ('RemoteTable') whose keys represent the stability, and
+ whose values are resolved potentially differently across compiler versions.
+
+ The need for the caller to pass in a 'RemoteTable' is seen as a liability, so
+ two subsequent packages @distributed-closure@ and @static-closure@ take the
+ opposite approach, ripping out the 'RemoteTable' but doubling down on GHC's
+ choice to guarantee compatibility only across different processes running the
+ exact same binary program. Their uses cases are focused around compute
+ clusters and other forms of centralised distributed computing, where this is
+ easy to achieve and not a problem.
+
+ Sometimes security is cited as a reason to have this restriction, but this is
+ a /bogus argument/. "Guarantee compatibility only across same binary" means
+ "same binary => compatibility" whereas the bogus security argument depends on
+ "compatibility => same binary", which is not true - anyone who analyses your
+ binary will know which numbers to spoof, to convince your program via this
+ interface that they are "running the same code". Guaranteeing "same binary"
+ in an adversial setting is in fact extremely hard and cannot be achieved
+ perfectly; in the real-world it can only be approximated, and should be done
+ so via mechanisms designed for it, not via numbers that are slightly hard to
+ brute force at best and trivial to find out at worst.
+
+ This package makes the /opposite/ choice, intended for less restricted and
+ more open distributed computing environments such as the internet and
+ decentralised protocols. In these contexts, the requirement of running the
+ exact same binary program is impossible to achieve in practise. Furthermore,
+ we see it as an /advantage/ that code does not need to be exactly the same -
+ for example, one can serialise a closure and its inputs, /upgrade your code/,
+ then resume running the closure on the same deserialised input arguments but
+ with a bugfixed closure. The necessity to pass in an explicit 'RemoteTable'
+ (here simply called 'staticTab') is not a liability, but a useful tool to
+ represent high-level compatibility and interoperability. Two nodes with the
+ same keys in their 'staticTab's, know that they can talk to each other
+ interoperably even if their implementations differ significantly. One node
+ that wishes to talk to different nodes running different minor versions of
+ the same protocol, could instantiate two different 'staticTab's with the same
+ keys but different implementations, to handle behavioural nuances between the
+ minor versions. In general, it's a useful bit of metadata to keep around in
+ your program code, and can help you perform smooth upgrades of a
+ non-centralised networking protocol more easily.
+
+ There are also a few technical differences between this and
+ @distributed-static@, some of which could be re-adopted there too:
+
+ * We use dependent-types and type-level programming to guarantee type
+ safety, rather than 'Rank1Dynamic'. This enables us to store all possible
+ closure types instead of just rank-1 polymorphic functions, including but
+ not limited to: rank-n functions, functions with constraints, those using
+ higher-kinded types, etc.
+
+ * Our serialisation typeclasses are designed to interoperate with many
+ different serialisation frameworks. Instances for 'Data.Binary' and
+ 'Codec.Serialise' are provided here for convenience.
+
+ * We have additional Template Haskell splices that support creating static
+ values from top-level definitions that must refer to other static values,
+ whether they be recursive or mutually-recursive or neither. This is
+ achieved using an implementation of @mfix@ for the @Q@ monad.
+
+ We did /not/ implement the ability to compose static references. The main
+ reason is that, in our view, the /purpose/ of static closures is to represent
+ which top-level tasks to execute, and the inputs to execute it on. This is
+ the /interface/ or /contract/ of this concept. /How you run/ the task is an
+ implementation detail, and as discussed above, this might be different across
+ different machines or as time passes and we upgrade the code. Therefore it
+ makes no sense to serialise a representation of "task A is the composition of
+ closure B and closure C", because it is irrelevant to the /interface/.
+
+ If your /interface/ is actually "run arbitrary user-defined code" (e.g. in a
+ VM or EDSL evaluator) then it would indeed make sense to support composition,
+ but then you should define your own AST, evaluator, and serialiser for this;
+ and pass the ASTs around as regular runtime values, not static values.
+ Supporting arbitrary ASTs like this is outside of the scope of this library.
+
+ Further, in Haskell there are many ways of applying values not just @(_ :: a
+ -> b) (_ :: a) :: b@, e.g. with constraints, with a combination of static and
+ non-static arguments, with type applications, and so on. Only the simple form
+ @(_ :: a -> b) (_ :: a) :: b@ is likely to be interoperable across multiple
+ languages. Supporting AST statics would therefore unnecessarily restrict how
+ we can implement the behaviour of a static closure in our chosen language.
+
+ See unit tests for example usage, e.g.
+
+Homepage: https://github.com/infinity0/hs-static
+Bug-Reports: https://github.com/infinity0/hs-static/issues
+License: GPL-3.0-or-later
+License-File: LICENSE.GPL-3
+Author: Ximin Luo
+Maintainer: infinity0@pwned.gg
+Copyright: 2020 Ximin Luo
+Category: Control, Static, Closure
+Tested-With: GHC >= 8.8.3
+Extra-Source-Files: CHANGELOG.md
+
+Source-Repository head
+ Type: git
+ Location: https://github.com/infinity0/hs-static
+
+Flag dev
+ Description: Set compile flags for development
+ Default: False
+ Manual: True
+
+Common generic
+ Default-Language: Haskell2010
+ Build-Depends: base >= 4 && < 5,
+ GHC-Options:
+ -Wall
+ -Wno-unused-matches
+ -Wredundant-constraints
+ -Wincomplete-record-updates
+ -Wincomplete-uni-patterns
+ if flag(dev)
+ GHC-Options:
+ -Werror
+ -O2
+ -- some optimisations cause memory leaks; switch on -O2 and profiling so we
+ -- can detect this during development so it doesn't cause surprises later
+ GHC-Prof-Options:
+ -fprof-auto
+
+Library
+ Import: generic
+ Build-Depends:
+ constraints
+ , text
+ , singletons
+ -- for serialisation
+ , binary
+ , bytestring
+ , serialise
+ -- Control.Static.TH
+ , template-haskell
+ HS-Source-Dirs: src
+ Exposed-Modules:
+ Control.Static
+ , Control.Static.Common
+ , Control.Static.Closure
+ , Control.Static.Serialise
+ , Control.Static.Static
+ , Control.Static.TH
+
+Test-Suite doctests
+ Import: generic
+ GHC-Options: -threaded
+ Build-Depends:
+ doctest
+ , static
+ HS-Source-Dirs: test
+ Type: exitcode-stdio-1.0
+ Main-Is: DocTests.hs
+
+Test-Suite unit
+ Import: generic
+ GHC-Options: -threaded
+ Build-Depends:
+ tasty
+ , tasty-quickcheck
+ , tasty-hunit
+ , checkers
+ , static
+ , lens
+ , mtl
+ , transformers
+ HS-Source-Dirs: test
+ Type: exitcode-stdio-1.0
+ Main-Is: UnitTests.hs
+ Other-Modules:
+ Control.Static.UnitTests
diff --git a/test/Control/Static/UnitTests.hs b/test/Control/Static/UnitTests.hs
new file mode 100644
--- /dev/null
+++ b/test/Control/Static/UnitTests.hs
@@ -0,0 +1,234 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Control.Static.UnitTests where
+
+-- external, testing
+import Test.Tasty
+import Test.Tasty.HUnit
+
+-- external
+import Control.Monad.RWS.Strict (RWST (..), evalRWST)
+import Control.Monad.State.Class (MonadState (..))
+import Control.Monad.Writer.Class (MonadWriter (..))
+import Control.Static (ClosureApply, DSerialise,
+ RepVal (..), applyClosure,
+ envTabCons, envTabNil,
+ evalSomeClosure, mkClosureTab,
+ repClosureTab)
+import Control.Static.TH (mkDefStaticTab, mkStatics,
+ mkStaticsWithRefs, staticKeyType,
+ staticRef)
+
+-- These unit tests are written to showcase all the features & possibilities of
+-- using this library. It is certainly not the simplest way of achieving what
+-- it is actually doing. When using this library, bear this in mind and don't
+-- just blindly copy the below - aim to simplify as much of it as possible.
+
+data TEnv m g = TEnv {
+ pushTask :: !(ClosureApply g -> m ())
+ , pushLog :: !(String -> m ())
+}
+
+writeLog :: MonadWriter [String] m => () -> String -> m [Int]
+writeLog _ x = tell [x] >> pure []
+mkStatics ['writeLog]
+-- note: the above call to mkStatics is actually redundant; mkDefStaticTab
+-- automatically will do this for any passed-in names that did not already have
+-- statics created for them. We call it here for demonstration purposes.
+
+collatzCycle0 :: [Integer]
+collatzCycle0 = [0]
+collatzCycle1 :: [Integer]
+collatzCycle1 = [1, 4, 2]
+collatzCycle2 :: [Integer]
+collatzCycle2 = [-1, -2]
+collatzCycle3 :: [Integer]
+collatzCycle3 = [-5, -14, -7, -20, -10]
+collatzCycle4 :: [Integer]
+collatzCycle4 =
+ [-17, -50, -25, -74, -37, -110, -55, -164, -82, -41]
+ ++ [-122, -61, -182, -91, -272, -136, -68, -34]
+
+mkStaticsWithRefs $ \(~[collatz', collatzOdd', collatzEven']) -> [d|
+ collatz
+ :: RepVal g Integer $(staticKeyType 'collatzOdd)
+ => RepVal g Integer $(staticKeyType 'collatzEven)
+ => Monad m => TEnv m g -> Integer -> m [Int]
+ collatz env x = do
+ pushLog $ "got: " <> show x
+ if
+ | x `elem` collatzCycle0 -> pure [0]
+ | x `elem` collatzCycle1 -> pure [1]
+ | x `elem` collatzCycle2 -> pure [2]
+ | x `elem` collatzCycle3 -> pure [3]
+ | x `elem` collatzCycle4 -> pure [4]
+ | x `mod` 2 == 1 -> do
+ pushTask (applyClosure $(pure collatzOdd') x)
+ pure []
+ | otherwise -> do
+ pushTask (applyClosure $(pure collatzEven') x)
+ pure []
+ where TEnv {..} = env
+
+ collatzOdd
+ :: RepVal g Integer $(staticKeyType 'collatz)
+ => Monad m => TEnv m g -> Integer -> m [Int]
+ collatzOdd env x = do
+ pushLog $ "got odd: " <> show x
+ pushTask (applyClosure $(pure collatz') (3 * x + 1))
+ pure []
+ where TEnv {..} = env
+
+ collatzEven
+ :: RepVal g Integer $(staticKeyType 'collatz)
+ => Monad m => TEnv m g -> Integer -> m [Int]
+ collatzEven env x = do
+ pushLog $ "got even: " <> show x
+ pushTask (applyClosure $(pure collatz') (x `div` 2))
+ pure []
+ where TEnv {..} = env
+ |]
+
+mkDefStaticTab ['writeLog, 'collatz, 'collatzOdd, 'collatzEven]
+
+-- In most use-cases, you don't need to distinguish between the tasks, and
+-- 'TaskArg' (further below) is simpler and better . On the off-chance that you
+-- do need to, this is how you would do that, using @$(staticKeyType 'KEY)@.
+data Task =
+ TaskLog !String
+ | TaskCollatz !Integer
+ | TaskCollatzOdd !Integer
+ | TaskCollatzEven !Integer
+ deriving (Show, Read, Eq, Ord)
+instance RepVal Task String $(staticKeyType 'writeLog) where
+ toRep _ = TaskLog
+ fromRep _ (TaskLog i) = Right i
+ fromRep _ t = Left $ "expect TaskLog, got " <> show t
+instance RepVal Task Integer $(staticKeyType 'collatz) where
+ toRep _ = TaskCollatz
+ fromRep _ (TaskCollatz i) = Right i
+ fromRep _ t = Left $ "expect TaskCollatz, got " <> show t
+instance RepVal Task Integer $(staticKeyType 'collatzOdd) where
+ toRep _ = TaskCollatzOdd
+ fromRep _ (TaskCollatzOdd i) = Right i
+ fromRep _ t = Left $ "expect TaskCollatzOdd, got " <> show t
+instance RepVal Task Integer $(staticKeyType 'collatzEven) where
+ toRep _ = TaskCollatzEven
+ fromRep _ (TaskCollatzEven i) = Right i
+ fromRep _ t = Left $ "expect TaskCollatzEven, got " <> show t
+
+-- You can either define your own 'g' like here, or use one of the provided
+-- ones, like 'DSerialise' or 'DBinary'.
+data TaskArg =
+ ArgString !String
+ | ArgInteger !Integer
+ deriving (Show, Read, Eq, Ord)
+instance RepVal TaskArg String k where
+ toRep _ = ArgString
+ fromRep _ (ArgString i) = Right i
+ fromRep _ t = Left $ "expect ArgString, got " <> show t
+instance RepVal TaskArg Integer k where
+ toRep _ = ArgInteger
+ fromRep _ (ArgInteger i) = Right i
+ fromRep _ t = Left $ "expect ArgInteger, got " <> show t
+
+monadEnv
+ :: RepVal g String $(staticKeyType 'writeLog)
+ => MonadState [ClosureApply g] m => String -> TEnv m g
+monadEnv prefix =
+ let pushTask t = state (\tt -> ((), tt ++ [t]))
+ pushLog s = pushTask (applyClosure $(staticRef 'writeLog) s)
+ in TEnv { .. }
+
+runAllTasks
+ :: forall g tm
+ . RepVal g String $(staticKeyType 'writeLog)
+ => RepVal g Integer $(staticKeyType 'collatz)
+ => RepVal g Integer $(staticKeyType 'collatzOdd)
+ => RepVal g Integer $(staticKeyType 'collatzEven)
+ => MonadWriter [String] (tm IO)
+ => MonadState [ClosureApply g] (tm IO)
+ => MonadFail (tm IO)
+ => (String -> TEnv (tm IO) g)
+ -> (tm IO Int -> [ClosureApply g] -> IO (Int, [String]))
+ -> [ClosureApply g]
+ -> Int
+ -> [String]
+ -> IO ()
+runAllTasks mkEnv evalT initCl expectRuns expectLogs = do
+ (actualRuns, actualLogs) <- evalT (go 0) initCl
+ assertEqual "runs" expectRuns actualRuns
+ assertEqual "logs" expectLogs actualLogs
+ where
+ go i = state popTask >>= \case
+ Nothing -> pure i
+ Just t -> do
+ res <- run t
+ let msg = (\c -> "result: cycle #" <> show c) <$> res
+ state $ pushTasks $ applyClosure $(staticRef 'writeLog) <$> msg
+ go (i + 1)
+ popTask [] = (Nothing, [])
+ popTask (h : tl) = (Just h, tl)
+ pushTasks tt' tt = ((), tt ++ tt')
+ run cl = case evalSomeClosure closureTab cl of
+ Left e -> fail (show e)
+ Right r -> r
+ closureTab =
+ repClosureTab @_ @g
+ $ mkClosureTab staticTab
+ $ envTabCons $(staticRef 'writeLog) ()
+ $ envTabCons $(staticRef 'collatz) (mkEnv "collatz")
+ $ envTabCons $(staticRef 'collatzOdd) (mkEnv "collatzOdd")
+ $ envTabCons $(staticRef 'collatzEven) (mkEnv "collatzEven")
+ $ envTabNil
+
+tests :: TestTree
+tests = testGroup
+ "Control.Static.UnitTests"
+ [ testCase "smoke @Task" $ do
+ runAllTasks @Task @(RWST () [String] [ClosureApply Task])
+ monadEnv
+ (`evalRWST` ())
+ [applyClosure $(staticRef 'collatz) (4 :: Integer)]
+ 3
+ ["got: 4", "result: cycle #1"]
+ , testCase "smoke @TaskArg" $ do
+ runAllTasks @TaskArg @(RWST () [String] [ClosureApply TaskArg])
+ monadEnv
+ (`evalRWST` ())
+ [applyClosure $(staticRef 'collatz) (30 :: Integer)]
+ 67
+ ( ["got: 30", "got even: 30", "got: 15", "got odd: 15", "got: 46"]
+ ++ ["got even: 46", "got: 23", "got odd: 23", "got: 70", "got even: 70"]
+ ++ ["got: 35", "got odd: 35", "got: 106", "got even: 106", "got: 53"]
+ ++ ["got odd: 53", "got: 160", "got even: 160", "got: 80", "got even: 80"]
+ ++ ["got: 40", "got even: 40", "got: 20", "got even: 20", "got: 10"]
+ ++ ["got even: 10", "got: 5", "got odd: 5", "got: 16", "got even: 16"]
+ ++ ["got: 8", "got even: 8", "got: 4", "result: cycle #1"]
+ )
+ , testCase "smoke @DSerialise" $ do
+ runAllTasks @DSerialise @(RWST () [String] [ClosureApply DSerialise])
+ monadEnv
+ (`evalRWST` ())
+ [applyClosure $(staticRef 'collatz) (-30 :: Integer)]
+ 39
+ ( ["got: -30", "got even: -30", "got: -15", "got odd: -15", "got: -44"]
+ ++ ["got even: -44", "got: -22", "got even: -22", "got: -11"]
+ ++ ["got odd: -11", "got: -32", "got even: -32", "got: -16"]
+ ++ ["got even: -16", "got: -8", "got even: -8", "got: -4", "got even: -4"]
+ ++ ["got: -2", "result: cycle #2"]
+ )
+ ]
diff --git a/test/DocTests.hs b/test/DocTests.hs
new file mode 100644
--- /dev/null
+++ b/test/DocTests.hs
@@ -0,0 +1,4 @@
+import Test.DocTest
+
+main :: IO ()
+main = doctest ["-i", "src"]
diff --git a/test/UnitTests.hs b/test/UnitTests.hs
new file mode 100644
--- /dev/null
+++ b/test/UnitTests.hs
@@ -0,0 +1,7 @@
+import Test.Tasty
+
+import Control.Static.UnitTests (tests)
+
+main :: IO ()
+main = do
+ defaultMain $ testGroup "Static *" [Control.Static.UnitTests.tests]