diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,621 @@
+ 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
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/Basics.hs b/src/Control/Basics.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Basics.hs
@@ -0,0 +1,17 @@
+-- |
+-- Copyright : (c) 2010 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+-- Portability : GHC only
+--
+-- Re-export basic control structures for easier imports.
+module Control.Basics (
+ module Control.Arrow
+ , module Control.Applicative
+ , module Control.Monad
+) where
+
+import Control.Arrow
+import Control.Applicative
+import Control.Monad
diff --git a/src/Control/Monad/Bind.hs b/src/Control/Monad/Bind.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Bind.hs
@@ -0,0 +1,134 @@
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses #-}
+-- |
+-- Copyright : (c) 2010, 2011 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+-- Portability : GHC only
+--
+-- Shallow monad transformer for dealing with bindings.
+--
+module Control.Monad.Bind (
+
+ -- * Bindings
+ Bindings
+ , noBindings
+
+ -- * MonadBind class
+ , MonadBind
+
+ -- * Bind monad
+ , Bind
+ , runBind
+ , evalBind
+ , execBind
+
+ -- * BindT monad transformer
+ , BindT
+ , runBindT
+ , evalBindT
+ , execBindT
+
+ -- * Binding operations
+
+ , lookupBinding
+ , insertBinding
+ , importBinding
+
+ , module Control.Monad.Fresh
+
+ ) where
+
+import qualified Data.Map as M
+
+import Control.Basics
+import Control.Monad.State
+import Control.Monad.Fresh
+
+------------------------------------------------------------------------------
+-- Bindings
+------------------------------------------------------------------------------
+
+-- | Type constructor for the state of the binding store.
+type Bindings = M.Map
+
+-- | The empty binding store.
+noBindings :: Bindings v k
+noBindings = M.empty
+
+------------------------------------------------------------------------------
+-- Type synonym for the StateT monad transformer
+------------------------------------------------------------------------------
+
+class MonadState (Bindings k v) m => MonadBind k v m where
+
+instance Monad m => MonadBind k v (StateT (Bindings k v) m) where
+
+------------------------------------------------------------------------------
+-- Type synonym for the StateT monad transformer
+------------------------------------------------------------------------------
+
+-- | Managing bindings on top of another monad.
+type BindT k v = StateT (Bindings k v)
+
+-- | Run a computation with bindings.
+runBindT :: BindT k v m a -> Bindings k v -> m (a, Bindings k v)
+runBindT = runStateT
+
+-- | Evaluate a binding context computation.
+evalBindT :: Monad m => BindT k v m a -> Bindings k v -> m a
+evalBindT = evalStateT
+
+-- | Execute a binding context computation.
+execBindT :: Monad m => BindT k v m a -> Bindings k v -> m (Bindings k v)
+execBindT = execStateT
+
+------------------------------------------------------------------------------
+-- Type synonym for the State monad
+------------------------------------------------------------------------------
+
+-- | Managing just bindings.
+type Bind k v = State (Bindings k v)
+
+-- | Run a computation with bindings.
+runBind :: Bind k v a -> Bindings k v -> (a, Bindings k v)
+runBind = runState
+
+-- | Evaluate a binding context computation.
+evalBind :: Bind k v a -> Bindings k v -> a
+evalBind = evalState
+
+-- | Execute a binding context computation.
+execBind :: Bind k v a -> Bindings k v -> Bindings k v
+execBind = execState
+
+
+------------------------------------------------------------------------------
+-- Binding operations
+------------------------------------------------------------------------------
+
+-- | Lookup a stored binding.
+lookupBinding :: (MonadBind k v m, Ord k)
+ => k -> m (Maybe v)
+lookupBinding = gets . M.lookup
+
+-- | @insertBinding k v@ inserts the binding of @k@ to @v@, possibly
+-- overwriting the existing binding of @k@.
+insertBinding :: (MonadBind k v m, Ord k)
+ => k -> v -> m ()
+insertBinding k = modify . M.insert k
+
+-- | @importBinding mkR d n@ checks if there is already a binding registered
+-- for the value @d@ and if not it generates a fresh identifier using the name
+-- @n@ as a hint and converting name and identifier to a value using $mkR$.
+importBinding :: (MonadBind k v m, MonadFresh m, Show v, Show k, Ord k)
+ => (String -> Int -> v)
+ -> k
+ -> String -> m v
+importBinding mkR k n = do
+ rOpt <- lookupBinding k
+ case rOpt of
+ Nothing -> do v <- mkR n <$> freshIdent n
+ modify $ M.insert k v
+ return v
+ Just v -> return v
diff --git a/src/Control/Monad/Disj.hs b/src/Control/Monad/Disj.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Disj.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+-- |
+-- Copyright : (c) 2010, 2011 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+-- Portability : GHC only
+--
+-- Computations that need perform case distinctions.
+module Control.Monad.Disj (
+
+ -- * MonadDisj class
+ MonadDisj(..)
+
+ , contradictory
+ , contradictoryIf
+ , contradiction
+ , contradictionIf
+ , disjunctions
+ , disjunctionOfList
+
+ -- * The DisjT monad transformer
+ , DisjT(..)
+ , disjT
+ , runDisjT
+
+ -- * Convencience exports
+ , module Control.Monad
+ , module Control.Monad.Fix
+ , module Control.Monad.Trans
+
+ ) where
+
+import Control.Monad
+import Control.Monad.Fix
+import Control.Monad.Trans
+
+import Control.Monad.Disj.Class
+import Control.Monad.Trans.Disj
+
+-- | @contradiction reason@ denotes the logical false, but also
+-- provides the @reason@ as meta-information.
+contradiction :: MonadDisj m => String -> m a
+contradiction = contradictoryBecause . Just
+
+-- | @contradictionIf b reason@ is logically equivalent to @not b@, but also
+-- provides the @reason@ as meta-information.
+contradictionIf :: MonadDisj m => Bool -> String -> m ()
+contradictionIf b reason | b = contradiction reason
+ | otherwise = return ()
+
+-- | @contradictory@ denotes the logical false.
+contradictory :: MonadDisj m => m a
+contradictory = contradictoryBecause Nothing
+
+-- | @contradictoryIf b@ is logically equivalent to @not b@
+contradictoryIf :: MonadDisj m => Bool -> m ()
+contradictoryIf b | b = contradictory
+ | otherwise = return ()
+
+-- | @disjunctions ds@ builds the disjunction of all the @ds@ values.
+disjunctions :: MonadDisj m => [m a] -> m a
+disjunctions = foldr disjunction contradictory
+
+-- | @disjunctionOfList xs@ build the disjunction of the values in list @xs@.
+disjunctionOfList :: MonadDisj m => [a] -> m a
+disjunctionOfList = disjunctions . map return
+
+
diff --git a/src/Control/Monad/Disj/Class.hs b/src/Control/Monad/Disj/Class.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Disj/Class.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving, DeriveDataTypeable #-}
+-- |
+-- Copyright : (c) 2011 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+-- Portability : unknown
+--
+-- A monad to represent logical disjunctions.
+module Control.Monad.Disj.Class (
+ -- * The @MonadDisj@ class
+ MonadDisj(..)
+ ) where
+
+import Control.Monad.Trans
+import qualified Control.Monad.State.Lazy as L
+import qualified Control.Monad.State.Strict as S
+import Control.Monad.Reader
+import Control.Monad.Fresh
+
+
+------------------------------------------------------------------------------
+-- The MonadDisj class
+------------------------------------------------------------------------------
+
+
+class Monad m => MonadDisj m where
+ -- | Mark a contradiction.
+ contradictoryBecause :: Maybe String -> m a
+ -- | Disjoin two computations.
+ disjunction :: m a -> m a -> m a
+
+
+------------------------------------------------------------------------------
+-- Instances
+------------------------------------------------------------------------------
+
+instance MonadDisj m => MonadDisj (L.StateT s m) where
+ contradictoryBecause = lift . contradictoryBecause
+ disjunction m1 m2 = L.StateT $ \s -> L.runStateT m1 s `disjunction` L.runStateT m2 s
+
+instance MonadDisj m => MonadDisj (S.StateT s m) where
+ contradictoryBecause = lift . contradictoryBecause
+ disjunction m1 m2 = S.StateT $ \s -> S.runStateT m1 s `disjunction` S.runStateT m2 s
+
+instance MonadDisj m => MonadDisj (FreshT m) where
+ contradictoryBecause = lift . contradictoryBecause
+ disjunction m1 m2 = FreshT $ unFreshT m1 `disjunction` unFreshT m2
+
+instance MonadDisj m => MonadDisj (ReaderT r m) where
+ contradictoryBecause = lift . contradictoryBecause
+ disjunction m1 m2 = ReaderT $ \r -> runReaderT m1 r `disjunction` runReaderT m2 r
+
+
+
diff --git a/src/Control/Monad/Fresh.hs b/src/Control/Monad/Fresh.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Fresh.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+-- |
+-- Copyright : (c) 2010, 2011 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+-- Portability : GHC only
+--
+-- Computations that need a fresh name supply.
+module Control.Monad.Fresh (
+
+ -- * MonadFresh class
+ MonadFresh(..)
+
+ -- * The Fresh monad
+ , Fresh
+ , runFresh
+ , evalFresh
+ , execFresh
+
+ -- * The FreshT monad transformer
+ , FreshT(..)
+ , freshT
+ , runFreshT
+ , evalFreshT
+ , execFreshT
+
+ -- * Fresh name generation
+ , FreshState
+ , nothingUsed
+
+ , module Control.Monad
+ , module Control.Monad.Fix
+ , module Control.Monad.Trans
+
+ ) where
+
+import Control.Monad
+import Control.Monad.Fix
+import Control.Monad.Trans
+
+import Control.Monad.Fresh.Class
+import Control.Monad.Trans.Fresh hiding (freshIdent)
+
diff --git a/src/Control/Monad/Fresh/Class.hs b/src/Control/Monad/Fresh/Class.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Fresh/Class.hs
@@ -0,0 +1,48 @@
+-- |
+-- Copyright : (c) 2010 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+-- Portability : portable
+--
+-- Type-class abstracting computations that need a fresh name supply.
+module Control.Monad.Fresh.Class (
+ MonadFresh(..)
+) where
+
+import Control.Basics
+
+import Control.Monad.Trans
+import Control.Monad.Trans.Maybe
+import Control.Monad.State
+import Control.Monad.Reader
+import Control.Monad.Writer
+
+import qualified Control.Monad.Trans.Fresh as Fresh (FreshT, freshIdent)
+
+-- Added 'Applicative' until base states this hierarchy
+class (Applicative m, Monad m) => MonadFresh m where
+ freshIdent :: String -- ^ Desired name.
+ -> m Int -- ^ Fresh identifier.
+
+
+instance (Functor m, Monad m) => MonadFresh (Fresh.FreshT m) where
+ freshIdent = Fresh.freshIdent
+
+
+----------------------------------------------------------------------------
+-- instances for other mtl transformers
+--
+-- TODO: Add remaining ones
+
+instance MonadFresh m => MonadFresh (MaybeT m) where
+ freshIdent = lift . freshIdent
+
+instance MonadFresh m => MonadFresh (StateT s m) where
+ freshIdent = lift . freshIdent
+
+instance MonadFresh m => MonadFresh (ReaderT r m) where
+ freshIdent = lift . freshIdent
+
+instance (Monoid w, MonadFresh m) => MonadFresh (WriterT w m) where
+ freshIdent = lift . freshIdent
diff --git a/src/Control/Monad/Trans/Disj.hs b/src/Control/Monad/Trans/Disj.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Trans/Disj.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+-- |
+-- Copyright : (c) 2011 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+-- Portability : unknown
+--
+-- A monad transformer to enable other *commutative* monads to represent
+-- logical disjunctions.
+module Control.Monad.Trans.Disj (
+ -- * The 'DisjT' monad transformer
+ DisjT(..)
+ , disjT
+ , runDisjT
+ ) where
+
+import Control.Applicative
+import Control.Monad.List
+import Control.Monad.Reader
+import Control.Monad.Disj.Class
+
+------------------------------------------------------------------------------
+-- The 'DisjT' monad transformer
+------------------------------------------------------------------------------
+
+-- | A disjunction of atoms of type a.
+newtype DisjT m a = DisjT { unDisjT :: ListT m a }
+ deriving (Functor, Applicative, MonadTrans )
+
+-- | Construct a 'DisjT' action.
+disjT :: m [a] -> DisjT m a
+disjT = DisjT . ListT
+
+-- | Run a 'DisjT' action.
+runDisjT :: DisjT m a -> m [a]
+runDisjT = runListT . unDisjT
+
+
+
+
+-- Instances
+------------
+
+instance Monad m => Monad (DisjT m) where
+ -- Ensure that contradictions are not reported via fail!
+ fail = error
+ {-# INLINE return #-}
+ return = DisjT . return
+ {-# INLINE (>>=) #-}
+ m >>= f = DisjT $ (unDisjT . f) =<< unDisjT m
+
+instance Monad m => MonadDisj (DisjT m) where
+ contradictoryBecause _ = DisjT mzero
+ disjunction m1 m2 = DisjT $ unDisjT m1 `mplus` unDisjT m2
+
+
+instance MonadReader r m => MonadReader r (DisjT m) where
+ ask = lift ask
+ local f m = DisjT $ local f $ unDisjT m
+
diff --git a/src/Control/Monad/Trans/Fresh.hs b/src/Control/Monad/Trans/Fresh.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Trans/Fresh.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-} -- require for MonadError
+-- |
+-- Copyright : (c) 2010 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+-- Portability : GHC only
+--
+-- A monad transformer for passing a fresh name supply through a computation.
+-- This is just a newtype wrapper around the 'StateT' monad transformer.
+--
+-- Modeled after the mtl-2.0 library.
+--
+module Control.Monad.Trans.Fresh (
+
+ -- * The Fresh monad
+ Fresh
+ , runFresh
+ , evalFresh
+ , execFresh
+
+ -- * The FreshT monad transformer
+ , FreshT(..)
+ , freshT
+ , runFreshT
+ , evalFreshT
+ , execFreshT
+
+ -- * Fresh name generation
+ , FreshState
+ , nothingUsed
+ , freshIdent
+
+ ) where
+
+import Control.Basics
+import Control.Monad.Identity
+import Control.Monad.State.Strict
+import Control.Monad.Error
+import Control.Monad.Reader
+
+------------------------------------------------------------------------------
+-- FreshT monad transformer
+------------------------------------------------------------------------------
+
+-- | The state of the name supply: the last used sequence number of every name.
+type FreshState = Int
+
+-- | A computation that can generate fresh variables from name hints.
+newtype FreshT m a = FreshT { unFreshT :: StateT FreshState m a }
+ deriving( Functor, Applicative, Alternative, Monad, MonadPlus, MonadTrans )
+
+-- | Construct a 'FreshT' action from a 'FreshState' modification.
+freshT :: (FreshState -> m (a, FreshState)) -> FreshT m a
+freshT = FreshT . StateT
+
+-- | The empty fresh state.
+nothingUsed :: FreshState
+nothingUsed = 0
+
+-- | Run a computation with a fresh name supply.
+runFreshT :: FreshT m a -> FreshState -> m (a, FreshState)
+runFreshT (FreshT m) used = runStateT m used
+
+-- | Evaluate a computation with a fresh name supply.
+evalFreshT :: Monad m => FreshT m a -> FreshState -> m a
+evalFreshT (FreshT m) used = evalStateT m used
+
+-- | Execute a computation with a fresh name supply.
+execFreshT :: Monad m => FreshT m a -> FreshState -> m FreshState
+execFreshT (FreshT m) used = execStateT m used
+
+-- | Get a fresh identifier.
+freshIdent :: Monad m
+ => String -- ^ Desired name.
+ -> FreshT m Int -- ^ Fresh identifier for this name.
+freshIdent _ = do
+ i <- FreshT get
+ FreshT $ put $ succ i
+ return i
+
+-- Instances
+------------
+
+instance MonadError e m => MonadError e (FreshT m) where
+ throwError = lift . throwError
+ catchError m h = FreshT $ catchError (unFreshT m) (unFreshT . h)
+
+instance MonadReader r m => MonadReader r (FreshT m) where
+ ask = lift ask
+ local f m = FreshT $ local f $ unFreshT m
+
+------------------------------------------------------------------------------
+-- Fresh monad
+------------------------------------------------------------------------------
+
+type Fresh = FreshT Identity
+
+-- | Run a computation with a fresh name supply.
+runFresh :: Fresh a -> FreshState -> (a, FreshState)
+runFresh (FreshT m) used = runState m used
+
+-- | Evaluate a computation with a fresh name supply.
+evalFresh :: Fresh a -> FreshState -> a
+evalFresh (FreshT m) used = evalState m used
+
+-- | Execute a computation with a fresh name supply.
+execFresh :: Fresh a -> FreshState -> FreshState
+execFresh (FreshT m) used = execState m used
diff --git a/src/Data/Color.hs b/src/Data/Color.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Color.hs
@@ -0,0 +1,252 @@
+{-# OPTIONS_GHC -fno-warn-type-defaults #-}
+-- remove the two benign defaults
+
+-- |
+-- Copyright : (c) 2010 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+--
+-- A simple color module for handling RGB and HSV representations of colors.
+module Data.Color (
+ -- * Datatypes
+ RGB(..)
+ , HSV(..)
+ , rgbToHex
+ , hsvToHex
+
+ -- ** Predefined colors
+ , red
+ , green
+ , blue
+
+ -- ** Conversions
+ , rgbToGray
+ , hsvToGray
+ , rgbToHSV
+ , hsvToRGB
+
+ -- * Color Palettes
+ , colorGroups
+ , lightColorGroups
+
+) where
+
+{- IDEA: Provide color datastructure together with nice and usable color
+ - palettes for reporting various data
+ -}
+
+import Numeric (showHex)
+
+-- import Text.XHtml.Strict
+-- import Text.XHtml.Table
+
+data RGB a = RGB {
+ rgbR :: !a
+ , rgbG :: !a
+ , rgbB :: !a
+ }
+ deriving( Eq, Ord )
+
+instance Show a => Show (RGB a) where
+ show (RGB r g b) = "RGB("++show r++", "++show g++", "++show b++")"
+
+instance Functor RGB where
+ fmap f (RGB r g b) = RGB (f r) (f g) (f b)
+
+red, green, blue :: Fractional t => RGB t
+red = RGB 1.0 0.0 0.0
+green = RGB 0.0 1.0 0.0
+blue = RGB 0.0 0.0 1.0
+
+data HSV a = HSV {
+ hsvH :: !a
+ , hsvS :: !a
+ , hsvV :: !a
+ }
+ deriving( Eq, Ord )
+
+instance Show a => Show (HSV a) where
+ show (HSV h s v) = "HSV("++show h++", "++show s++", "++show v++")"
+
+instance Functor HSV where
+ fmap f (HSV h s v) = HSV (f h) (f s) (f v)
+
+
+------------------------------------------------------------------------------
+-- Colorspace conversion
+------------------------------------------------------------------------------
+
+-- | RGB to HSV conversion.
+-- Pre: 0 <= r,g,b <= 1
+-- (Source: http://de.wikipedia.org/wiki/HSV-Farbraum)
+rgbToHSV :: (Fractional t, Ord t) => RGB t -> HSV t
+rgbToHSV (RGB r g b) = HSV h' s v
+ where
+ ub = max r (max g b)
+ lb = min r (min g b)
+
+ h | ub == lb = 0
+ | ub == r = 60 * ( (g-b)/(ub-lb))
+ | ub == g = 60 * (2 + (b-r)/(ub-lb))
+ | otherwise = 60 * (4 + (r-g)/(ub-lb))
+
+ h' | h < 0 = h + 360
+ | otherwise = h
+
+ s | ub == 0 = 0
+ | otherwise = (ub-lb)/ub
+
+ v = ub
+
+-- | HSV to RGB conversion.
+-- Pre: 0 <= h <= 360 and 0 <= s,v <= 1
+-- (Source: http://de.wikipedia.org/wiki/HSV-Farbraum)
+hsvToRGB :: RealFrac t => HSV t -> RGB t
+hsvToRGB (HSV h s v) = case hIdx of
+ 0 -> RGB v t p
+ 1 -> RGB q v p
+ 2 -> RGB p v t
+ 3 -> RGB p q v
+ 4 -> RGB t p v
+ 5 -> RGB v p q
+ _ -> error "hsvToRGB: hue outside of range [0..360]"
+ where
+ hIdx = floor (h / 60)
+ f = h/60 - fromIntegral (hIdx::Int)
+ p = v*(1-s)
+ q = v*(1-s*f)
+ t = v*(1-s*(1-f))
+
+hsvToGray :: Num t => HSV t -> HSV t
+hsvToGray (HSV h _ v) = HSV h 0 v
+
+rgbToGray :: Ord t => RGB t -> t
+rgbToGray (RGB r g b) = max r (max g b)
+
+------------------------------------------------------------------------------
+-- String output
+------------------------------------------------------------------------------
+
+-- | Hexadecimal representation of an RGB value
+rgbToHex :: RealFrac t => RGB t -> String
+rgbToHex (RGB r g b) = ('#':) . showHex' r . showHex' g . showHex' b $ ""
+ where showHex' f
+ | i <= 15 = ('0':) . showHex i
+ | otherwise = showHex i
+ where
+ i :: Int
+ i = max 0 (min 255 (floor (256 * f)))
+
+-- | Hexadecimal representation of an HSV value; i.e., of its corresponding RGB
+-- value.
+hsvToHex :: RealFrac t => HSV t -> [Char]
+hsvToHex = rgbToHex . hsvToRGB
+
+
+------------------------------------------------------------------------------
+-- HSV Color Palettes
+------------------------------------------------------------------------------
+
+data ColorParams t = ColorParams {
+ cpScale :: !t
+ , cpZeroHue :: !t
+ , cpVBottom :: !t
+ , cpVRange :: !t
+ , cpSBottom :: !t
+ , cpSRange :: !t
+ }
+ deriving( Eq, Ord, Show )
+
+-- | From a list of group sizes build a function assigning every element a
+-- unique color, nicely distributed such that they are well differentiated both
+-- using color and monochrome displays.
+genColorGroups :: RealFrac t =>
+ ColorParams t
+ -> [Int] -- ^ List of group sizes.
+ -> [((Int,Int),(HSV t))]
+genColorGroups (ColorParams {
+ cpScale = scale
+ , cpZeroHue = zeroHue
+ , cpVBottom = vBot, cpVRange = vRan
+ , cpSBottom = sBot, cpSRange = sRan
+ }) groups =
+ do
+ (groupIdx, groupSize) <- zip [0.. ] groups
+ elemIdx <- [0..groupSize - 1]
+ let h = toShiftedGroupHue groupIdx (fromIntegral elemIdx / fromIntegral groupSize)
+ v = vBot + vRan * toGroupHue groupIdx (fromIntegral elemIdx / fromIntegral groupSize)
+ s = sBot + sRan * toGroupHue groupIdx (fromIntegral elemIdx / fromIntegral groupSize)
+ color = HSV (360*h) s v
+ return ((groupIdx, elemIdx), color)
+ where
+ nGroups :: Int
+ nGroups = length groups
+
+ toGroupHue g h = (
+ fromIntegral g + -- base position
+ 0.5 * (1 - scale) + -- left margin
+ (h * scale) -- position in margin
+ ) / (fromIntegral nGroups)
+
+ toShiftedGroupHue g h =
+ snd . properFraction $ toGroupHue g h + 1 +
+ (zeroHue/360) - toGroupHue 0 0.5
+
+
+-- | A good default style for the 'genColorGroups' color palette function. The
+-- parameter shifts the hue for the first group.
+colorGroupStyle :: Double -> ColorParams Double
+colorGroupStyle zeroHue = ColorParams {
+ cpScale = 0.6
+ , cpZeroHue = zeroHue
+ , cpVBottom = 0.75, cpVRange = 0.2
+ , cpSBottom = 0.4, cpSRange = 0.00
+ }
+
+-- | Build color groups according to the list of group sizes using the default
+-- 'colorGroupStyle' for the function 'genColorGroups'.
+colorGroups :: Double -> [Int] -> [((Int, Int), HSV Double)]
+colorGroups zeroHue = genColorGroups (colorGroupStyle zeroHue)
+
+
+-- | A good light color style for the @genColorGroups@ color palette
+-- function. The parameter shifts the hue for the first group.
+lightColorGroupStyle :: Double -> ColorParams Double
+lightColorGroupStyle zeroHue = ColorParams {
+ cpScale = 0.6
+ , cpZeroHue = zeroHue
+ , cpVBottom = 0.8, cpVRange = 0.15
+ , cpSBottom = 0.3, cpSRange = 0.00
+ }
+
+-- | Build color groups according to the list of group sizes using the
+-- default light 'lightColorGroupStyle' for the function
+-- 'genColorGroups'.
+lightColorGroups :: Double -> [Int] -> [((Int, Int), HSV Double)]
+lightColorGroups zeroHue = genColorGroups (lightColorGroupStyle zeroHue)
+
+
+------------------------------------------------------------------------------
+-- Testing: Html Table with group colors
+------------------------------------------------------------------------------
+
+{-
+
+colorTable :: Double -> (HSV Double -> HSV Double) -> [Int] -> Html
+colorTable zeroHue conv groups =
+ table . toHtml . besides $ map col [0..length groups-1]
+ where
+ col i = aboves [cell $ (td ! [getStyle i j]) (stringToHtml (show (i,j)))
+ | j <- [0..(groups !! i) - 1] ]
+ color = colorGroups zeroHue groups
+ getStyle i j = thestyle ("background-color: "++ hsvToHex (conv $ color i j))
+
+colorFile :: Double -> FilePath -> [Int] -> IO ()
+colorFile zeroHue outF groups = do
+ let html = colorTable zeroHue id groups +++
+ colorTable zeroHue hsvToGray groups
+ writeFile outF $ prettyHtml html
+
+-}
+
diff --git a/src/Data/DAG/Simple.hs b/src/Data/DAG/Simple.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/DAG/Simple.hs
@@ -0,0 +1,66 @@
+-- |
+-- Copyright : (c) 2010 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+--
+-- Simple vertice list based representation of DAGs and some common operations on it.
+module Data.DAG.Simple (
+ toposort
+ , reachableSet
+ , cyclic
+) where
+
+
+import Data.List
+import qualified Data.Set as S
+
+import Control.Basics
+import Control.Monad.Writer
+
+
+-- | Produce a topological sorting of the given relation. If the relation is
+-- cyclic, then the result is at least some permutation of all elements of
+-- the given relation.
+toposort :: Ord a => [(a, a)] -> [a]
+toposort dag =
+ execWriter . foldM visit S.empty $ map fst dag ++ map snd dag
+ where
+ visit visited x
+ | x `S.member` visited = return visited
+ | otherwise =
+ foldM visit (S.insert x visited) preds <* tell (pure x)
+ where
+ preds = [ e | (e,e') <- dag, e' == x ]
+
+
+-- | Compute the set of nodes reachable from the given set of nodes.
+reachableSet :: Ord a => [a] -> [(a,a)] -> S.Set a
+reachableSet start dag =
+ foldl' visit S.empty start
+ where
+ visit visited x
+ | x `S.member` visited = visited
+ | otherwise =
+ foldl' visit (S.insert x visited) succs
+ where
+ succs = [ e' | (e,e') <- dag, e == x ]
+
+-- | Is the relation cyclic.
+cyclic :: Ord a => [(a,a)] -> Bool
+cyclic rel =
+ maybe True (const False) $ foldM visitForest S.empty $ map fst rel
+ where
+ visitForest visited x
+ | x `S.member` visited = return visited
+ | otherwise = findLoop S.empty visited x
+
+ findLoop parents visited x
+ | x `S.member` parents = mzero
+ | x `S.member` visited = return visited
+ | otherwise =
+ S.insert x <$> foldM (findLoop parents') visited next
+ where
+ next = [ e' | (e,e') <- rel, e == x ]
+ parents' = S.insert x parents
+
diff --git a/src/Debug/Trace/Ignore.hs b/src/Debug/Trace/Ignore.hs
new file mode 100644
--- /dev/null
+++ b/src/Debug/Trace/Ignore.hs
@@ -0,0 +1,15 @@
+-- |
+-- Copyright : (c) 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Module that can be imported to ignore calls to @trace@.
+module Debug.Trace.Ignore (
+ trace
+ ) where
+
+-- | @trace a b@ returns the second argument.
+trace :: a -> b -> b
+trace = flip const
+
diff --git a/src/Extension/Data/Bounded.hs b/src/Extension/Data/Bounded.hs
new file mode 100644
--- /dev/null
+++ b/src/Extension/Data/Bounded.hs
@@ -0,0 +1,24 @@
+-- |
+-- Copyright : (c) 2011 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+--
+-- Monoids for bounded types.
+module Extension.Data.Bounded (
+ BoundedMax(..)
+ ) where
+
+import Data.Monoid
+
+-- | A newtype wrapper for a monoid of the maximum of a bounded type.
+newtype BoundedMax a = BoundedMax {getBoundedMax :: a}
+ deriving( Eq, Ord, Show )
+
+instance (Ord a, Bounded a) => Monoid (BoundedMax a) where
+ mempty = BoundedMax minBound
+ (BoundedMax x) `mappend` (BoundedMax y) = BoundedMax (max x y)
+
+
+
+-- TODO: Add BoundedMin
diff --git a/src/Extension/Data/Label.hs b/src/Extension/Data/Label.hs
new file mode 100644
--- /dev/null
+++ b/src/Extension/Data/Label.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE TypeOperators #-}
+-- |
+-- Copyright : (c) 2011 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+-- Portability : GHC only
+--
+-- Extensions to the first-class labels (fclabels) package.
+module Extension.Data.Label (
+ nthL
+ , imageL
+ , fstL
+ , sndL
+ , module Data.Label
+
+ -- * Labels and applicative functors
+ , liftLA
+ , modA
+
+ -- * Labels and Monads
+ , askM
+ , setM
+ , getM
+ , modM
+ , (=:)
+ ) where
+
+import Data.Maybe (fromMaybe)
+import qualified Data.Map as M
+
+import Data.Label
+import Data.Label.PureM ( (=:) )
+import qualified Data.Label.PureM as LM
+
+import Control.Arrow (first, second)
+import Control.Applicative (Applicative, (<$>), (<*>), pure, liftA2)
+import Control.Monad.State (MonadState)
+import Control.Monad.Reader (MonadReader)
+
+-- | Lens for the first element of a tuple.
+fstL :: ((a, b) :-> a)
+fstL = lens fst (first . const)
+
+-- | Lens for the second element of a tuple.
+sndL :: ((a, b) :-> b)
+sndL = lens snd (second . const)
+
+-- | Lens for the nth element of the list.
+nthL :: Int -> ([a] :-> a)
+nthL i = lens (!! i) updateAt
+ where
+ updateAt x xs
+ | 0 <= i && i < length xs = case splitAt i xs of
+ (prefix, _:suffix) -> prefix ++ (x:suffix)
+ _ -> error "nthL: impossible"
+ | otherwise = error $ "nthL: index " ++ show i ++ " out of range"
+
+-- | Lens for the element at a given position of a map.
+imageL :: Ord k => k -> (M.Map k v :-> v)
+imageL k =
+ lens (fromMaybe (error "imageL: element not found") . M.lookup k)
+ (M.insert k)
+
+-- | Lift a label into an applicative functor.
+liftLA :: Applicative f => (a :-> b) -> (f a :-> f b)
+liftLA l = lens (get l <$>) (liftA2 (set l))
+
+-- | Effectful modification of a labeled value.
+modA :: Applicative f => (a :-> b) -> (b -> f b) -> a -> f a
+modA l f a = set l <$> f (get l a) <*> pure a
+
+-- | Get part of the state from a reader.
+askM :: MonadReader r m => (r :-> a) -> m a
+askM = LM.asks
+
+-- | Set some part of the state.
+setM :: MonadState s m => (s :-> a) -> a -> m ()
+setM = LM.puts
+
+-- | Get some part of the state.
+getM :: MonadState s m => (s :-> a) -> m a
+getM = LM.gets
+
+-- | Modify some part of the state.
+modM :: MonadState s m => (s :-> a) -> (a -> a) -> m ()
+modM = LM.modify
diff --git a/src/Extension/Prelude.hs b/src/Extension/Prelude.hs
new file mode 100644
--- /dev/null
+++ b/src/Extension/Prelude.hs
@@ -0,0 +1,224 @@
+-- |
+-- Copyright : (c) 2010, 2011 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+--
+-- Functions that could/should have made it into the Prelude or one of the
+-- base libraries
+module Extension.Prelude where
+
+import Data.Maybe
+import Data.List
+import qualified Data.Set as S
+import qualified Data.Map as M
+import Data.Ord (comparing)
+import Data.Function (on)
+import Data.Foldable (asum)
+
+import Control.Basics
+
+import System.IO
+
+
+
+-- Bool --
+----------
+
+implies :: Bool -> Bool -> Bool
+implies True p = p
+implies False _ = True
+
+
+-- Lists --
+-----------
+
+singleton :: a -> [a]
+singleton x = [x]
+
+-- | check whether the given list contains no duplicates
+unique :: Eq a => [a] -> Bool
+unique [] = True
+unique (x:xs) = x `notElem` xs && unique xs
+
+-- | Sort list and remove duplicates. O(n*log n)
+sortednub :: Ord a => [a] -> [a]
+sortednub = map head . group . sort
+
+-- | //O(n*log n).// Sort list and remove duplicates with respect to a
+-- projection.
+sortednubOn :: Ord b => (a -> b) -> [a] -> [a]
+sortednubOn proj = map head . groupOn proj . sortOn proj
+
+-- | Keep only the first element of elements having the same projected value
+nubOn :: Eq b => (a -> b) -> [a] -> [a]
+nubOn proj = nubBy ((==) `on` proj)
+
+-- | //O(n).// Group on a projection of the data to group
+groupOn :: Eq b => (a -> b) -> [a] -> [[a]]
+groupOn proj = groupBy ((==) `on` proj)
+
+-- | sort on a projection of the data to sort
+sortOn :: Ord b => (a -> b) -> [a] -> [a]
+sortOn proj = sortBy (comparing proj)
+
+-- | sort on a projection of the data to sort, memorizing the results of the
+-- projection in order to avoid recomputation.
+sortOnMemo :: Ord b => (a -> b) -> [a] -> [a]
+sortOnMemo proj = map fst . sortOn snd . map (id &&& proj)
+
+-- | sort and group on a projection
+groupSortOn :: Ord b => (a -> b) -> [a] -> [[a]]
+groupSortOn proj = groupOn proj . sortOn proj
+
+-- | partition the given set into equality classes with respect
+-- to the representative given by the projection function
+eqClasses :: (Eq b, Ord b) => (a -> b) -> [a] -> [[a]]
+eqClasses = eqClassesBy ord
+ where ord x y | x == y = EQ | x < y = LT | otherwise = GT
+
+eqClassesBy :: (b -> b -> Ordering) -> (a -> b) -> [a] -> [[a]]
+eqClassesBy ord proj = groupBy eq . sortBy ord'
+ where ord' x y = ord (proj x) (proj y)
+ eq x y = ord' x y == EQ
+
+-- | split a list into sublists whenever the predicate identifies an element as
+-- a separator. Note that the separator is not retained and a separator at the
+-- very end is ignored.
+splitBy :: (a -> Bool) -> [a] -> [[a]]
+splitBy p = unfoldr split
+ where split [] = Nothing
+ split xs = let ~(w,r) = break p xs in case r of
+ [] -> Just $ (w,[])
+ (_:rest) -> Just $ (w,rest)
+
+
+-- | the list of all permutations of a given list
+-- permutations :: [a] -> [[a]]
+-- permutations [] = [[]]
+-- permutations zs = aux zs []
+ -- where aux [] _ = []
+ -- aux (x:xs) ys = [x:p | p <- permutations (xs++ys)] ++ aux xs (x:ys)
+
+-- | the list of all combinations of n elements of a list.
+-- E.g. choose 2 [1,2,3] = [[1,2],[1,3],[2,3]]
+choose :: Int -> [a] -> [[a]]
+choose 0 _ = [[]]
+choose _ [] = []
+choose n (x:xs) = [x:xs' | xs' <- choose (n-1) xs] ++ choose n xs
+
+-- | build the list of lists each leaving another element out.
+-- (From left to right)
+leaveOneOut :: [a] -> [[a]]
+leaveOneOut xs =
+ zipWith (++) (map init . tail . inits $ xs) (map tail . init . tails $ xs)
+
+
+-- | An element masks another element if the predicate is true. This function
+-- keeps only the elements not masked by a previous element in the list.
+keepFirst :: (a -> a -> Bool) -> [a] -> [a]
+keepFirst _ [] = []
+keepFirst mask (x:xs) = x : keepFirst mask (filter (not . mask x) xs)
+
+-- Pairs --
+-----------
+
+-- | These functions were inspired by the ML library accompanying the
+-- Isabelle theorem prover ()
+
+-- | swap the elements of a pair
+swap :: (a, b) -> (b, a)
+swap (x, y) = (y, x)
+
+-- | sort the elements of a pair
+sortPair :: Ord a => (a,a) -> (a,a)
+sortPair p@(x,y) | x <= y = p | otherwise = swap p
+
+
+-- Either --
+------------
+
+isRight :: Either a b -> Bool
+isRight (Right _) = True
+isRight _ = False
+
+isLeft :: Either a b -> Bool
+isLeft (Left _) = True
+isLeft _ = False
+
+-- Strings --
+-------------
+
+-- | Name values of a given type
+type Named a = (String, a)
+
+-- | Extend a list with the given separators to be flushed right.
+flushRightBy :: [a] -> Int -> [a] -> [a]
+flushRightBy sep n str = take (max 0 (n - length str)) (cycle sep) ++ str
+
+-- | Extend a string with spaces to be flushed right.
+flushRight :: Int -> String -> String
+flushRight = flushRightBy " "
+
+-- | Extend a list with the given separators to be flushed left.
+flushLeftBy :: [a] -> Int -> [a] -> [a]
+flushLeftBy sep n str = str ++ take (max 0 (n - length str)) (cycle sep)
+
+-- | Extend a string with spaces to be flushed left.
+flushLeft :: Int -> String -> String
+flushLeft = flushLeftBy " "
+
+
+-- IO --
+--------
+
+
+-- | marks a string as being a warning
+warning :: String -> String
+warning s = "warning: "++s
+
+-- | abbreviation to print to stderr
+putErr :: String -> IO ()
+putErr = hPutStr stderr
+
+-- | abbreviation to println to stderr
+putErrLn :: String -> IO ()
+putErrLn = hPutStrLn stderr
+
+-- Applicative --
+-----------------
+
+-- | Inject the elements of a list as alternatives.
+oneOfList :: Alternative f => [a] -> f a
+oneOfList = asum . map pure
+
+-- | Inject the elements of a set as alternatives.
+oneOfSet :: Alternative f => S.Set a -> f a
+oneOfSet = oneOfList . S.toList
+
+-- | Inject the elements of a map as alternatives.
+oneOfMap :: Alternative f => M.Map k v -> f (k, v)
+oneOfMap = oneOfList . M.toList
+
+
+-- Monads --
+------------
+
+-- | A monadic if statement
+ifM :: Monad m => m Bool -> m a -> m a -> m a
+ifM p pos neg = do
+ b <- p
+ if b then pos else neg
+
+-- | Gather all error free computations.
+errorFree :: MonadPlus m => [m a] -> m [a]
+errorFree ms =
+ catMaybes `liftM` sequence [(Just `liftM` m) `mplus` return Nothing | m <- ms]
+
+-- | Gather all error free computations and ensure that at least one was error
+-- free.
+errorFree1 :: MonadPlus m => [m a] -> m [a]
+errorFree1 ms = do
+ ms' <- errorFree ms
+ if null ms' then mzero else return ms'
+
diff --git a/src/Logic/Connectives.hs b/src/Logic/Connectives.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Connectives.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving, DeriveDataTypeable #-}
+-- |
+-- Copyright : (c) 2010 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+-- Portability : GHC only
+--
+-- Types and instances to handle series of disjunctions and conjunctions.
+module Logic.Connectives where
+
+import Data.Monoid
+import Data.Foldable
+import Data.Traversable
+import Data.Typeable
+import Data.Generics
+import Data.Binary
+
+import Control.Basics
+import Control.Monad.Disj
+import Control.DeepSeq
+
+
+-- | A conjunction of atoms of type a.
+newtype Conj a = Conj { getConj :: [a] }
+ deriving (Monoid, Foldable, Traversable, Eq, Ord, Show, Binary,
+ Functor, Applicative, Monad, MonadPlus, Typeable, Data, NFData)
+
+-- | A disjunction of atoms of type a.
+newtype Disj a = Disj { getDisj :: [a] }
+ deriving (Monoid, Foldable, Traversable, Eq, Ord, Show, Binary,
+ Functor, Applicative, Monad, MonadPlus, Typeable, Data, NFData)
+
+instance MonadDisj Disj where
+ contradictoryBecause _ = Disj mzero
+ disjunction m1 m2 = Disj $ getDisj m1 `mplus` getDisj m2
+
+
diff --git a/src/System/Timing.hs b/src/System/Timing.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Timing.hs
@@ -0,0 +1,27 @@
+-- |
+-- Copyright : (c) 2011 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+-- Portability : GHC only
+--
+-- A simple module for timing IO action.
+module System.Timing (
+ timed
+ , timed_
+) where
+
+import Control.Monad
+import Data.Time.Clock
+
+-- | Execute an IO action and return its result plus the time it took to execute it.
+timed :: IO a -> IO (a, NominalDiffTime)
+timed io = do
+ t0 <- getCurrentTime
+ x <- io
+ t1 <- getCurrentTime
+ return (x, diffUTCTime t1 t0)
+
+-- | Execute an IO action and return the time it took to execute it.
+timed_ :: IO a -> IO NominalDiffTime
+timed_ = (snd `liftM`) . timed
diff --git a/src/Text/Dot.hs b/src/Text/Dot.hs
new file mode 100644
--- /dev/null
+++ b/src/Text/Dot.hs
@@ -0,0 +1,274 @@
+-- |
+-- Module: Text.Dot
+-- Copyright: Andy Gill, Simon Meier (extension to record syntax)
+-- License: BSD3
+--
+-- Maintainer: Andy Gill
+-- Stability: unstable
+-- Portability: portable
+--
+-- This module provides a simple interface for building .dot graph files, for input into the dot and graphviz tools.
+-- It includes a monadic interface for building graphs.
+
+module Text.Dot
+ (
+ -- * Dot
+ Dot -- abstract
+ -- * Nodes
+ , node
+ , NodeId -- abstract
+ , userNodeId
+ , userNode
+ -- * Edges
+ , edge
+ -- * Showing a graph
+ , showDot
+ -- * Other combinators
+ , scope
+ , attribute
+ , nodeAttributes
+ , edgeAttributes
+ , graphAttributes
+ , share
+ , same
+ , cluster
+ -- * Record specification
+ , Record -- abstract
+ , field
+ , portField
+ , hcat
+ , hcat'
+ , vcat
+ , vcat'
+ -- * Record node construction
+ , record
+ , record'
+ , record_
+
+ , mrecord
+ , mrecord'
+ , mrecord_
+ ) where
+
+import Data.List (intersperse)
+import Control.Monad (liftM)
+
+data NodeId = NodeId String
+ | UserNodeId Int
+
+instance Show NodeId where
+ show (NodeId str) = str
+ show (UserNodeId i)
+ | i < 0 = "u_" ++ show (negate i)
+ | otherwise = "u" ++ show i
+
+data GraphElement = GraphAttribute String String
+ | GraphNode NodeId [(String,String)]
+ | GraphEdge NodeId NodeId [(String,String)]
+ | Scope [GraphElement]
+ | SubGraph NodeId [GraphElement]
+
+data Dot a = Dot { unDot :: Int -> ([GraphElement],Int,a) }
+
+instance Monad Dot where
+ return a = Dot $ \ uq -> ([],uq,a)
+ m >>= k = Dot $ \ uq -> case unDot m uq of
+ (g1,uq',r) -> case unDot (k r) uq' of
+ (g2,uq2,r2) -> (g1 ++ g2,uq2,r2)
+
+-- | 'node' takes a list of attributes, generates a new node, and gives a 'NodeId'.
+node :: [(String,String)] -> Dot NodeId
+node attrs = Dot $ \ uq -> let nid = NodeId $ "n" ++ show uq
+ in ( [ GraphNode nid attrs ],succ uq,nid)
+
+
+-- | 'userNodeId' allows a user to use their own (Int-based) node id's, without needing to remap them.
+userNodeId :: Int -> NodeId
+userNodeId i = UserNodeId i
+
+-- | 'userNode' takes a NodeId, and adds some attributes to that node.
+userNode :: NodeId -> [(String,String)] -> Dot ()
+userNode nId attrs = Dot $ \ uq -> ( [GraphNode nId attrs ],uq,())
+
+-- | 'edge' generates an edge between two 'NodeId's, with attributes.
+edge :: NodeId -> NodeId -> [(String,String)] -> Dot ()
+edge from to attrs = Dot (\ uq -> ( [ GraphEdge from to attrs ],uq,()))
+
+-- | 'scope' groups a subgraph together; in dot these are the subgraphs inside "{" and "}".
+scope :: Dot a -> Dot a
+scope (Dot fn) = Dot (\ uq -> case fn uq of
+ ( elems,uq',a) -> ([Scope elems],uq',a))
+
+-- | 'share' is when a set of nodes share specific attributes. Usually used for layout tweaking.
+share :: [(String,String)] -> [NodeId] -> Dot ()
+share attrs nodeids = Dot $ \ uq ->
+ ( [ Scope ( [ GraphAttribute name val | (name,val) <- attrs]
+ ++ [ GraphNode nodeid [] | nodeid <- nodeids ]
+ )
+ ], uq, ())
+
+-- | 'same' provides a combinator for a common pattern; a set of 'NodeId's with the same rank.
+same :: [NodeId] -> Dot ()
+same = share [("rank","same")]
+
+
+-- | 'cluster' builds an explicit, internally named subgraph (called cluster).
+cluster :: Dot a -> Dot (NodeId,a)
+cluster (Dot fn) = Dot (\ uq ->
+ let cid = NodeId $ "cluster_" ++ show uq
+ in case fn (succ uq) of
+ (elems,uq',a) -> ([SubGraph cid elems],uq',(cid,a)))
+
+-- | 'attribute' gives a attribute to the current scope.
+attribute :: (String,String) -> Dot ()
+attribute (name,val) = Dot (\ uq -> ( [ GraphAttribute name val ],uq,()))
+
+-- | 'nodeAttributes' sets attributes for all the following nodes in the scope.
+nodeAttributes :: [(String,String)] -> Dot ()
+nodeAttributes attrs = Dot (\uq -> ([ GraphNode (NodeId "node") attrs],uq,()))
+
+-- | 'edgeAttributes' sets attributes for all the following edges in the scope.
+edgeAttributes :: [(String,String)] -> Dot ()
+edgeAttributes attrs = Dot (\uq -> ([ GraphNode (NodeId "edge") attrs],uq,()))
+
+-- | 'graphAttributes' sets attributes for current graph.
+graphAttributes :: [(String,String)] -> Dot ()
+graphAttributes attrs = Dot (\uq -> ([ GraphNode (NodeId "graph") attrs],uq,()))
+
+
+-- 'showDot' renders a dot graph as a 'String'.
+showDot :: Dot a -> String
+showDot (Dot dm) = case dm 0 of
+ (elems,_,_) -> "digraph G {\n" ++ unlines (map showGraphElement elems) ++ "\n}\n"
+
+showGraphElement :: GraphElement -> String
+showGraphElement (GraphAttribute name val) = showAttr (name,val) ++ ";"
+showGraphElement (GraphNode nid attrs) = show nid ++ showAttrs attrs ++ ";"
+showGraphElement (GraphEdge from to attrs) = show from ++ " -> " ++ show to ++ showAttrs attrs ++ ";"
+showGraphElement (Scope elems) = "{\n" ++ unlines (map showGraphElement elems) ++ "\n}"
+showGraphElement (SubGraph nid elems) = "subgraph " ++ show nid ++ " {\n" ++ unlines (map showGraphElement elems) ++ "\n}"
+
+showAttrs :: [(String, String)] -> String
+showAttrs [] = ""
+showAttrs xs = "[" ++ showAttrs' xs ++ "]"
+ where
+ -- never empty list
+ showAttrs' [a] = showAttr a
+ showAttrs' (a:as) = showAttr a ++ "," ++ showAttrs' as
+ showAttrs' [] = error "showAttrs: the impossible happended"
+
+showAttr :: (String, String) -> String
+showAttr (name,val) = name ++ "=\"" ++ concatMap escape val ++ "\""
+ where escape '\n' = "\\l"
+ escape '"' = "\\\""
+ escape c = [c]
+
+
+------------------------------------------------------------------------------
+-- Records
+------------------------------------------------------------------------------
+
+-- | Specifies the construction of a record; i.e., mentions all fields possibly
+-- together with ports and their horizontal and vertical nesting. (see: record
+-- shapes in the DOT documentation.)
+data Record a =
+ Field (Maybe a) String
+ | HCat [Record a]
+ | VCat [Record a]
+ deriving( Eq, Ord, Show )
+
+-- | A simple field of a record.
+field :: String -> Record a
+field = Field Nothing
+
+-- | A field together with a port which can be used to create direct edges to
+-- this field. Note that you can use any type to identify the ports. When
+-- creating a record node you will get back an association list between your
+-- record identifiers and their concrete node ids.
+portField :: a -> String -> Record a
+portField port = Field (Just port)
+
+-- | Concatenate records horizontally.
+hcat :: [Record a] -> Record a
+hcat = HCat
+
+-- | Concatenate a list strings interpreted as simple fields horizontally.
+hcat' :: [String] -> Record a
+hcat' = hcat . map field
+
+-- | Concatenate records vertically.
+vcat :: [Record a] -> Record a
+vcat = VCat
+
+-- | Concatenate a list strings interpreted as simple fields vertically.
+vcat' :: [String] -> Record a
+vcat' = vcat . map field
+
+-- | Render a record in the Dot monad. It exploits the internal counter in
+-- order to generate unique port-ids. However, they must be combined with the
+-- actual node id of the node with the record shape. Thus the returned
+-- association list is parametrized over this missing node id.
+renderRecord :: Record a -> Dot (String, NodeId -> [(a,NodeId)])
+renderRecord = render True
+ where
+ render _ (Field Nothing l) = return (escape l, const [])
+ render _ (Field (Just p) l) =
+ Dot $ \uq -> let pid = "n" ++ show uq
+ lbl = "<"++pid++"> "++escape l
+ in ([], succ uq, (lbl, \nId -> [(p,NodeId (show nId++":"++pid))]))
+ render horiz (HCat rs) = do
+ (lbls, ids) <- liftM unzip $ mapM (render True) rs
+ let rawLbl = concat (intersperse "|" lbls)
+ lbl = if horiz then "{{"++rawLbl++"}}" else "{"++rawLbl++"}"
+ return (lbl, \nId -> concatMap (\i -> i nId) ids)
+ render horiz (VCat rs) = do
+ (lbls, ids) <- liftM unzip $ mapM (render False) rs
+ let rawLbl = concat (intersperse "|" lbls)
+ lbl = if horiz then "{"++rawLbl++"}" else "{{"++rawLbl++"}}"
+ return (lbl, \nId -> concatMap (\i -> i nId) ids)
+ -- escape chars used for record label construction
+ escape = concatMap esc
+ esc '|' = "\\|"
+ esc '{' = "\\{"
+ esc '}' = "\\}"
+ esc '<' = "\\<"
+ esc '>' = "\\>"
+ esc c = [c]
+
+-- | A generic version of record creation.
+genRecord :: String -> Record a -> [(String,String)] -> Dot (NodeId, [(a,NodeId)])
+genRecord shape rec attrs = do
+ (lbl, ids) <- renderRecord rec
+ i <- node ([("shape",shape),("label",lbl)] ++ attrs)
+ return (i, ids i)
+
+-- | Create a record node with the given attributes. It returns the node-id of
+-- the created node together with an association list mapping the port
+-- idenfiers given in the record to their corresponding node-ids. This list is
+-- ordered according to a left-to-rigth traversal of the record description.
+record :: Record a -> [(String,String)] -> Dot (NodeId, [(a,NodeId)])
+record = genRecord "record"
+
+-- | A variant of "record" ignoring the port identifiers.
+record' :: Record a -> [(String,String)] -> Dot (NodeId, [NodeId])
+record' rec attrs = do (nId, ids) <- record rec attrs
+ return (nId, map snd ids)
+
+-- | A variant of "record" ignoring the port to node-id association list.
+record_ :: Record a -> [(String,String)] -> Dot NodeId
+record_ rec attrs = liftM fst $ record rec attrs
+
+-- | Like "record", but creates record nodes with rounded corners; i.e. uses
+-- the \"Mrecord\" shape instead of the \"record\" shape.
+mrecord :: Record a -> [(String,String)] -> Dot (NodeId, [(a,NodeId)])
+mrecord = genRecord "Mrecord"
+
+-- | A variant of "mrecord" ignoring the port identifiers.
+mrecord' :: Record a -> [(String,String)] -> Dot (NodeId, [NodeId])
+mrecord' rec attrs = do (nId, ids) <- mrecord rec attrs
+ return (nId, map snd ids)
+
+-- | A variant of "mrecord" ignoring the port to node-id association list.
+mrecord_ :: Record a -> [(String,String)] -> Dot NodeId
+mrecord_ rec attrs = liftM fst $ mrecord rec attrs
+
diff --git a/src/Text/Isar.hs b/src/Text/Isar.hs
new file mode 100644
--- /dev/null
+++ b/src/Text/Isar.hs
@@ -0,0 +1,319 @@
+-- |
+-- Copyright : (c) 2011 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+-- Portability : portable
+--
+-- Generating Isabelle/ISAR theory files using 'Text.PrettyPrint'.
+module Text.Isar (
+ -- * ISAR Output
+ Isar(..)
+ -- ** Configuration
+ , IsarStyle(..)
+ , IsarConf(..)
+ , defaultIsarConf
+ , isPlainStyle
+ , isarPlain
+ , isarXSymbol
+
+ -- ** Constructions of our security protocol verification theory
+ , isaExecutionSystemState
+
+ -- ** Special Symbols
+ , isarightArrow
+ , isaLongRightArrow
+ , isaLParr
+ , isaRParr
+ , isaLBrack
+ , isaRBrack
+ , isaMetaAll
+ , isaExists
+ , isaAnd
+ , isaNotIn
+ , isaIn
+ , isaSubsetEq
+ , isaAlpha
+ , isaSublocale
+
+ -- * Extensions of 'Text.PrettyPrint'
+ , module Text.PrettyPrint.Class
+ , nestBetween
+ , nestShort
+ , nestShort'
+ , nestShortNonEmpty
+ , nestShortNonEmpty'
+ , fixedWidthText
+ , symbol
+ , numbered
+ , numbered'
+
+) where
+
+import Data.List
+
+import Extension.Prelude
+
+import Text.PrettyPrint.Class
+
+-- | The ISAR style to be used for output.
+data IsarStyle =
+ PlainText
+ | XSymbol
+ deriving( Eq, Show )
+
+-- | The configuration to be used for output. Apart from the ISAR style, the
+-- configuration also stores the representation of the reachable state of the
+-- protocol which we are reasoning about.
+data IsarConf = IsarConf {
+ isarStyle :: IsarStyle
+ , isarTrace :: Doc -- ^ The ISAR code of the trace
+ , isarPool :: Doc -- ^ The ISAR code of the thread pool
+ , isarSubst :: Doc -- ^ The ISAR code of the substitution
+ }
+ deriving( Show )
+
+-- | Default configuration: plaintext ISAR style and reachable state @(t,r,s)@.
+defaultIsarConf :: IsarConf
+defaultIsarConf = IsarConf PlainText (char 't') (char 'r') (char 's')
+
+-- | Check if the plaintext style was chosen.
+isPlainStyle :: IsarConf -> Bool
+isPlainStyle = (PlainText ==) . isarStyle
+
+
+-- | Values that can be output as ISAR code.
+--
+-- Minimal definition: 'isar'
+class Isar a where
+ isar :: IsarConf -> a -> Doc
+
+-- | Output as ISAR code using 'defaultIsarConf'.
+isarPlain :: Isar a => a -> Doc
+isarPlain = isar defaultIsarConf
+
+-- | Output as ISAR code using 'defaultIsarConf'
+-- with the XSymbol style.
+isarXSymbol :: Isar a => a -> Doc
+isarXSymbol = isar (defaultIsarConf { isarStyle = XSymbol })
+
+------------------------------------------------------------------------------
+-- General pretty printing combinators
+------------------------------------------------------------------------------
+
+-- | Nest a document surrounded by a leading and a finishing document breaking
+-- lead, body, and finish onto separate lines, if they don't fit on a single
+-- line.
+nestBetween :: Document d =>
+ Int -- ^ Indent of body
+ -> d -- ^ Leading document
+ -> d -- ^ Finishing document
+ -> d -- ^ Body document
+ -> d
+nestBetween n l r x = sep [l, nest n x, r]
+
+-- | Nest a document surrounded by a leading and a finishing document with an
+-- non-compulsory break between lead and body.
+nestShort :: Document d =>
+ Int -- ^ Indent of body
+ -> d -- ^ Leading document
+ -> d -- ^ Finishing document
+ -> d -- ^ Body document
+ -> d
+nestShort n lead finish body = sep [lead $$ nest n body, finish]
+
+-- | Nest document between two strings and indent body by @length lead + 1@.
+nestShort' :: Document d => String -> String -> d -> d
+nestShort' lead finish =
+ nestShort (length lead + 1) (text lead) (text finish)
+
+-- | Like 'nestShort' but doesn't print the lead and finish, if the document is
+-- empty.
+nestShortNonEmpty :: Document d => Int -> d -> d -> d -> d
+nestShortNonEmpty n lead finish body =
+ caseEmptyDoc emptyDoc (nestShort n lead finish body) body
+
+-- | Like 'nestShort'' but doesn't print the lead and finish, if the document is
+-- empty.
+nestShortNonEmpty' :: Document d => String -> String -> d -> d
+nestShortNonEmpty' lead finish =
+ nestShortNonEmpty (length lead + 1) (text lead) (text finish)
+
+-- | Output text with a fixed width: if it is smaller then nothing happens,
+-- otherwise care is taken to make the text appear having the given width.
+fixedWidthText :: Document d => Int -> String -> d
+fixedWidthText n cs
+ | length cs <= n = text cs
+ | otherwise = text as <> zeroWidthText bs
+ where
+ (as,bs) = splitAt n cs
+
+-- | Print string as symbol having width 1.
+symbol :: Document d => String -> d
+symbol = fixedWidthText 1
+
+-- | Number a list of documents that are vertically separated by the given
+-- separator.
+numbered :: Document d => d -> [d] -> d
+numbered _ [] = emptyDoc
+numbered vsep ds =
+ foldr1 ($-$) $ intersperse vsep $ map pp $ zip [(1::Int)..] ds
+ where
+ n = length ds
+ nWidth = length (show n)
+ pp (i, d) = text (flushRight nWidth (show i)) <> d
+
+-- | Number a list of documents with numbers terminated by "." and vertically
+-- separate using an empty line.
+numbered' :: Document d => [d] -> d
+numbered' = numbered (text "") . map (text ". " <>)
+
+
+------------------------------------------------------------------------------
+-- Operational Semantics Constructions
+------------------------------------------------------------------------------
+
+-- | Isabelle representation of the exeuction system state of our operational
+-- semantics.
+isaExecutionSystemState :: IsarConf -> Doc
+isaExecutionSystemState conf =
+ parens . hcat . punctuate comma $
+ [isarTrace conf, isarPool conf, isarSubst conf]
+
+
+------------------------------------------------------------------------------
+-- Isabelle symbols in both styles.
+------------------------------------------------------------------------------
+
+-- | A 'not in' symbol: @~:@
+isaNotIn :: Document d => IsarConf -> d
+isaNotIn conf
+ | isPlainStyle conf = text "~:"
+ | otherwise = symbol "\\"
+
+-- | An 'in' symbol: @:@
+isaIn :: Document d => IsarConf -> d
+isaIn conf
+ | isPlainStyle conf = text ":"
+ | otherwise = symbol "\\"
+
+-- | A left parenthesis with an additional vertical line: @(|@
+isaLParr :: Document d => IsarConf -> d
+isaLParr conf
+ | isPlainStyle conf = text "(|"
+ | otherwise = symbol "\\"
+
+-- | A right parenthesis with an additional vertical line: @|)@
+isaRParr :: Document d => IsarConf -> d
+isaRParr conf
+ | isPlainStyle conf = text "|)"
+ | otherwise = symbol "\\"
+
+-- | A left bracket with an additional vertical line: @[|@
+isaLBrack :: Document d => IsarConf -> d
+isaLBrack conf
+ | isPlainStyle conf = text "[|"
+ | otherwise = symbol "\\"
+
+-- | A right bracket with an additional vertical line: @|]@
+isaRBrack :: Document d => IsarConf -> d
+isaRBrack conf
+ | isPlainStyle conf = text "|]"
+ | otherwise = symbol "\\"
+
+-- | A short right arrow: @->@
+isarightArrow :: Document d => IsarConf -> d
+isarightArrow conf
+ | isPlainStyle conf = text "->"
+ | otherwise = fixedWidthText 2 "\\"
+
+-- | A long double right arrow: @==>@
+isaLongRightArrow :: Document d => IsarConf -> d
+isaLongRightArrow conf
+ | isPlainStyle conf = text "==>"
+ | otherwise = fixedWidthText 3 "\\"
+
+
+-- | The greek letter alpha: @\\@
+isaAlpha :: Document d => IsarConf -> d
+isaAlpha conf
+ | isPlainStyle conf = text "\\"
+ | otherwise = symbol "\\"
+
+-- | The meta all quantifier: @!!@
+isaMetaAll :: Document d => IsarConf -> d
+isaMetaAll conf
+ | isPlainStyle conf = text "!! "
+ | otherwise = symbol "\\"
+
+-- | The exists symbol: @?@
+isaExists :: Document d => IsarConf -> d
+isaExists conf
+ | isPlainStyle conf = text "? "
+ | otherwise = symbol "\\"
+
+-- | The logical and symbol: @&@
+isaAnd :: Document d => IsarConf -> d
+isaAnd conf
+ | isPlainStyle conf = text "&"
+ | otherwise = symbol "\\"
+
+-- | The non-strict subset symbol.
+isaSubsetEq :: Document d => IsarConf -> d
+isaSubsetEq conf
+ | isPlainStyle conf = text "<="
+ | otherwise = symbol "\\"
+
+-- | The sublocale sign.
+isaSublocale :: Document d => IsarConf -> d
+isaSublocale conf
+ | isPlainStyle conf = text "<"
+ | otherwise = symbol "\\"
+
+------------------------------------------------------------------------------
+-- Isabelle theory components
+------------------------------------------------------------------------------
+
+{- TODO: Finish, if it is used
+
+isaTheory :: Document d =>
+ String -- ^ Theory name
+ -> [String] -- ^ Imported theories
+ -> d -- ^ Theory body
+ -> d -- ^ The complete theory statement.
+isaTheory name imports body =
+ text "theory" <-> text name $-$
+ text "imports" $-$
+ nest 2 (vcat $ map (text . (++"\"") . ('"':)) imports) $-$
+ text "begin" $-$ text "" $-$
+ body $-$
+ text "" $-$ text "end"
+
+
+-- | An logic identifier; properly escaped if needed.
+-- TODO: Add escaping
+logicIdent :: String -> Doc
+logicIdent = text
+
+
+-- | A generic text command.
+genTextCmd :: String -> String -> Doc
+genTextCmd name content =
+ sep [text name <> text "{*", nest 2 (fsep . map text $ words content), text "*}"]
+
+chapter = genTextCmd "chapter"
+section = genTextCmd "section"
+subsection = genTextCmd "subsection"
+subsubsection = genTextCmd "subsubsection"
+paragraph = genTextCmd "text"
+
+-- | A comment.
+comment :: String -> Doc
+comment content = nestShort' "(*" "*)" (fsep $ map text $ words content)
+
+-- | Switch into a proof context.
+context :: String -> Doc -> Doc
+context name body = vcat [text name <-> text "begin", body, text "end"]
+
+-}
+
diff --git a/src/Text/PrettyPrint/Class.hs b/src/Text/PrettyPrint/Class.hs
new file mode 100644
--- /dev/null
+++ b/src/Text/PrettyPrint/Class.hs
@@ -0,0 +1,147 @@
+-- |
+-- Copyright : (c) 2011 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+--
+-- 'Document' class allowing to have different interpretations of the
+-- HughesPJ pretty-printing combinators.
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module Text.PrettyPrint.Class (
+ P.Doc
+ , Document(..)
+ , P.isEmpty
+ , P.render
+ , P.renderStyle
+ , P.style
+ , P.Style(..)
+ , P.Mode(..)
+
+ , ($--$)
+ , semi
+ , colon
+ , comma
+ , space
+ , equals
+ , lparen
+ , rparen
+ , lbrack
+ , rbrack
+ , lbrace
+ , rbrace
+
+ , int
+ , integer
+ , float
+ , double
+ , rational
+ , quotes
+ , doubleQuotes
+ , parens
+ , brackets
+ , braces
+
+ , hang
+ , punctuate
+) where
+
+import Prelude
+import qualified Text.PrettyPrint.HughesPJ as P
+import Control.DeepSeq
+
+infixl 6 <>
+infixl 6 <->
+infixl 5 $$, $-$, $--$
+
+class NFData d => Document d where
+ char :: Char -> d
+ text :: String -> d
+ zeroWidthText :: String -> d
+ emptyDoc :: d
+ (<>) :: d -> d -> d
+ (<->) :: d -> d -> d
+ hcat :: [d] -> d
+ hsep :: [d] -> d
+ ($$) :: d -> d -> d
+ ($-$) :: d -> d -> d
+ vcat :: [d] -> d
+ sep :: [d] -> d
+ cat :: [d] -> d
+ fsep :: [d] -> d
+ fcat :: [d] -> d
+ nest :: Int -> d -> d
+ caseEmptyDoc :: d -> d -> d -> d
+
+instance NFData P.Doc where
+ rnf = rnf . P.render
+
+instance Document P.Doc where
+ char = P.char
+ text = P.text
+ zeroWidthText = P.zeroWidthText
+ emptyDoc = P.empty
+ (<>) = (P.<>)
+ (<->) = (P.<+>)
+ hcat = P.hcat
+ hsep = P.hsep
+ ($$) = (P.$$)
+ ($-$) = (P.$+$)
+ vcat = P.vcat
+ sep = P.sep
+ cat = P.cat
+ fsep = P.fsep
+ fcat = P.fcat
+ nest = P.nest
+ caseEmptyDoc yes no d = if P.isEmpty d then yes else no
+
+-- | Vertical concatentation of two documents with an empty line in between.
+($--$) :: Document d => d -> d -> d
+d1 $--$ d2 =
+ caseEmptyDoc d2 (caseEmptyDoc d1 (d1 $-$ text "" $-$ d2) d2) d1
+
+semi, colon, comma, space, equals,
+ lparen, rparen, lbrack, rbrack, lbrace, rbrace :: Document d => d
+
+semi = char ';'
+colon = char ':'
+comma = char ','
+space = char ' '
+equals = char '='
+lparen = char '('
+rparen = char ')'
+lbrack = char '['
+rbrack = char ']'
+lbrace = char '{'
+rbrace = char '}'
+
+int :: Document d => Int -> d
+int n = text (show n)
+
+integer :: Document d => Integer -> d
+integer n = text (show n)
+
+float :: Document d => Float -> d
+float n = text (show n)
+
+double :: Document d => Double -> d
+double n = text (show n)
+
+rational :: Document d => Rational -> d
+rational n = text (show n)
+
+quotes, doubleQuotes, parens, brackets, braces :: Document d => d -> d
+quotes p = char '\'' <> p <> char '\''
+doubleQuotes p = char '"' <> p <> char '"'
+parens p = char '(' <> p <> char ')'
+brackets p = char '[' <> p <> char ']'
+braces p = char '{' <> p <> char '}'
+
+hang :: Document d => d -> Int -> d -> d
+hang d1 n d2 = sep [d1, nest n d2]
+
+punctuate :: Document d => d -> [d] -> [d]
+punctuate _ [] = []
+punctuate p (d:ds) = go d ds
+ where
+ go d' [] = [d']
+ go d' (e:es) = (d' <> p) : go e es
diff --git a/src/Text/PrettyPrint/Highlight.hs b/src/Text/PrettyPrint/Highlight.hs
new file mode 100644
--- /dev/null
+++ b/src/Text/PrettyPrint/Highlight.hs
@@ -0,0 +1,64 @@
+-- |
+-- Copyright : (c) 2011 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+-- Portability : portable
+--
+-- Pretty-printing with support for highlighting keywords and comments.
+-- Currently this module is not functional on itself, but geared towards its
+-- use in Text.PrettyPrint.Html.
+module Text.PrettyPrint.Highlight (
+ -- * Highlight style
+ HighlightStyle(..)
+
+ -- * HighlightDocument class
+ , HighlightDocument(..)
+
+ , comment
+ , keyword
+ , operator
+
+ , comment_
+ , keyword_
+ , operator_
+
+ , opParens
+
+ , module Text.PrettyPrint.Class
+ ) where
+
+import Text.PrettyPrint.Class
+import Control.DeepSeq
+
+-- | Currently we support only keywords, operators, and comments.
+data HighlightStyle = Keyword | Comment | Operator
+ deriving( Eq, Ord, Show )
+
+class (NFData d, Document d) => HighlightDocument d where
+ -- 'highlight' @style d@ marks that the document @d@ should be highlighted
+ -- using the @style@.
+ highlight :: HighlightStyle -> d -> d
+
+instance HighlightDocument Doc where
+ highlight _ = id
+
+------------------------------------------------------------------------------
+-- General highlighters
+------------------------------------------------------------------------------
+
+comment, keyword, operator :: HighlightDocument d => d -> d
+comment = highlight Comment
+keyword = highlight Keyword
+operator = highlight Operator
+
+comment_, keyword_, operator_ :: HighlightDocument d => String -> d
+comment_ = comment . text
+keyword_ = keyword . text
+operator_ = operator . text
+
+opParens :: HighlightDocument d => d -> d
+opParens d = operator_ "(" <> d <> operator_ ")"
+
+
+
diff --git a/src/Text/PrettyPrint/Html.hs b/src/Text/PrettyPrint/Html.hs
new file mode 100644
--- /dev/null
+++ b/src/Text/PrettyPrint/Html.hs
@@ -0,0 +1,208 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+-- |
+-- Copyright : (c) 2011 Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Simon Meier
+-- Portability : portable
+--
+-- Pretty-printing with support for HTML markup and proper HTML escaping.
+module Text.PrettyPrint.Html (
+ -- * HtmlDocument class
+ HtmlDocument(..)
+
+ , withTag
+ , withTagNonEmpty
+ , closedTag
+
+ , module Text.PrettyPrint.Highlight
+
+ -- * HtmlDoc: adding HTML markup
+ , HtmlDoc
+ , htmlDoc
+ , getHtmlDoc
+ , postprocessHtmlDoc
+ , renderHtmlDoc
+
+ -- * NoHtmlDoc: ignoring HTML markup
+ , noHtmlDoc
+ , getNoHtmlDoc
+ ) where
+
+import Data.Char (isSpace)
+import Data.Traversable (sequenceA)
+
+import Control.Arrow (first)
+import Control.Applicative
+import Control.Monad.Identity
+import Control.DeepSeq
+
+import Text.PrettyPrint.Class
+import Text.PrettyPrint.Highlight
+
+------------------------------------------------------------------------------
+-- HtmlDocument class
+------------------------------------------------------------------------------
+
+
+class HighlightDocument d => HtmlDocument d where
+ -- | @unescapedText str@ converts the 'String' @str@ to a document without
+ -- performing any escaping.
+ unescapedText :: String -> d
+
+ -- | @unescapedZeroWidthText str@ converts the 'String' @str@ to a document
+ -- with zero width without performing any escaping.
+ unescapedZeroWidthText :: String -> d
+
+-- | @withTag tag attrs inner@ adds the tag @tag@ with the attributes
+-- @attrs@ around the @inner@ document.
+withTag :: HtmlDocument d => String -> [(String,String)] -> d -> d
+withTag tag attrs inner =
+ unescapedZeroWidthText open <> inner <> unescapedZeroWidthText close
+ where
+ open = "<" ++ tag ++ concatMap attribute attrs ++ ">"
+ close = ""
+
+-- | @closedTag tag attrs@ builds the closed tag @tag@ with the attributes
+-- @attrs@; e.g.,
+--
+-- > closedTag "img" "href" "here" = HtmlDoc (text "![]()
)
+--
+closedTag :: HtmlDocument d => String -> [(String,String)] -> d
+closedTag tag attrs =
+ unescapedZeroWidthText $ "<" ++ tag ++ concatMap attribute attrs ++ "/>"
+
+-- | @withTagNonEmpty tag attrs inner@ adds the tag @tag@ with the attributes
+-- @attrs@ around the @inner@ document iff @inner@ is a non-empty document.
+withTagNonEmpty :: HtmlDocument d => String -> [(String,String)] -> d -> d
+withTagNonEmpty tag attrs inner =
+ caseEmptyDoc inner emptyDoc $ withTag tag attrs inner
+
+-- | Render an attribute.
+attribute :: (String, String) -> String
+attribute (key,value) = " " ++ key ++ "=\"" ++ escapeHtmlEntities value ++ "\""
+
+
+------------------------------------------------------------------------------
+-- HtmlDoc: adding HTML markup
+------------------------------------------------------------------------------
+
+-- | A 'Document' transformer that adds proper HTML escaping.
+newtype HtmlDoc d = HtmlDoc { getHtmlDoc :: d }
+
+-- | Wrap a document such that HTML markup can be added without disturbing the
+-- layout.
+htmlDoc :: d -> HtmlDoc d
+htmlDoc = HtmlDoc
+
+instance NFData d => NFData (HtmlDoc d) where
+ rnf = rnf . getHtmlDoc
+
+instance Document d => Document (HtmlDoc d) where
+ char = HtmlDoc . text . escapeHtmlEntities . return
+ text = HtmlDoc . text . escapeHtmlEntities
+ zeroWidthText = HtmlDoc . zeroWidthText . escapeHtmlEntities
+ emptyDoc = HtmlDoc emptyDoc
+
+ HtmlDoc d1 <> HtmlDoc d2 = HtmlDoc $ d1 <> d2
+ HtmlDoc d1 <-> HtmlDoc d2 = HtmlDoc $ d1 <-> d2
+ hcat = HtmlDoc . hcat . map getHtmlDoc
+ hsep = HtmlDoc . hsep . map getHtmlDoc
+
+ HtmlDoc d1 $$ HtmlDoc d2 = HtmlDoc $ d1 $$ d2
+ HtmlDoc d1 $-$ HtmlDoc d2 = HtmlDoc $ d1 $-$ d2
+ vcat = HtmlDoc . vcat . map getHtmlDoc
+
+ sep = HtmlDoc . sep . map getHtmlDoc
+ cat = HtmlDoc . cat . map getHtmlDoc
+
+ fsep = HtmlDoc . fsep . map getHtmlDoc
+ fcat = HtmlDoc . fcat . map getHtmlDoc
+
+ nest i = HtmlDoc . nest i . getHtmlDoc
+ caseEmptyDoc (HtmlDoc d1) (HtmlDoc d2) (HtmlDoc d3) =
+ HtmlDoc $ caseEmptyDoc d1 d2 d3
+
+instance Document d => HtmlDocument (HtmlDoc d) where
+ unescapedText = HtmlDoc . text
+ unescapedZeroWidthText = HtmlDoc . zeroWidthText
+
+instance Document d => HighlightDocument (HtmlDoc d) where
+ highlight hlStyle =
+ withTag "span" [("class", hlClass hlStyle)]
+ where
+ hlClass Comment = "hl_comment"
+ hlClass Keyword = "hl_keyword"
+ hlClass Operator = "hl_operator"
+
+-- | Escape HTML entities in a string
+--
+-- Copied from 'blaze-html'.
+escapeHtmlEntities :: String -- ^ String to escape
+ -> String -- ^ Resulting string
+escapeHtmlEntities [] = []
+escapeHtmlEntities (c:cs) = case c of
+ '<' -> "<" ++ escapeHtmlEntities cs
+ '>' -> ">" ++ escapeHtmlEntities cs
+ '&' -> "&" ++ escapeHtmlEntities cs
+ '"' -> """ ++ escapeHtmlEntities cs
+ '\'' -> "'" ++ escapeHtmlEntities cs
+ x -> x : escapeHtmlEntities cs
+
+-- | @renderHtmlDoc = 'postprocessHtmlDoc' . 'render' . 'getHtmlDoc'@
+renderHtmlDoc :: HtmlDoc Doc -> String
+renderHtmlDoc = postprocessHtmlDoc . render . getHtmlDoc
+
+-- | @postprocessHtmlDoc cs@ converts the line-breaks of @cs@ to @
@ tags and
+-- the prefixed spaces in every line of @cs@ by non-breaing HTML spaces @ @.
+postprocessHtmlDoc :: String -> String
+postprocessHtmlDoc =
+ unlines . map (addBreak . indent) . lines
+ where
+ addBreak = (++"
")
+ indent = uncurry (++) . (first $ concatMap (const " ")) . span isSpace
+
+------------------------------------------------------------------------------
+-- NoHtmlDoc: ignoring HTML markup
+------------------------------------------------------------------------------
+
+-- | A 'Document' transformer that ignores all 'HtmlDocument' specific methods.
+newtype NoHtmlDoc d = NoHtmlDoc { unNoHtmlDoc :: Identity d }
+ deriving( Functor, Applicative )
+
+-- | Wrap a document such that all 'HtmlDocument' specific methods are ignored.
+noHtmlDoc :: d -> NoHtmlDoc d
+noHtmlDoc = NoHtmlDoc . Identity
+
+-- | Extract the wrapped document.
+getNoHtmlDoc :: NoHtmlDoc d -> d
+getNoHtmlDoc = runIdentity . unNoHtmlDoc
+
+instance NFData d => NFData (NoHtmlDoc d) where
+ rnf = rnf . getNoHtmlDoc
+
+instance Document d => Document (NoHtmlDoc d) where
+ char = pure . char
+ text = pure . text
+ zeroWidthText = pure . zeroWidthText
+ emptyDoc = pure emptyDoc
+ (<>) = liftA2 (<>)
+ (<->) = liftA2 (<->)
+ hcat = liftA hcat . sequenceA
+ hsep = liftA hsep . sequenceA
+ ($$) = liftA2 ($$)
+ ($-$) = liftA2 ($-$)
+ vcat = liftA vcat . sequenceA
+ sep = liftA sep . sequenceA
+ cat = liftA cat . sequenceA
+ fsep = liftA fsep . sequenceA
+ fcat = liftA fcat . sequenceA
+ nest = liftA2 nest . pure
+ caseEmptyDoc = liftA3 caseEmptyDoc
+
+instance Document d => HtmlDocument (NoHtmlDoc d) where
+ unescapedText = noHtmlDoc . text
+ unescapedZeroWidthText = noHtmlDoc . zeroWidthText
+
+instance Document d => HighlightDocument (NoHtmlDoc d) where
+ highlight _ = id
diff --git a/src/Utils/Misc.hs b/src/Utils/Misc.hs
new file mode 100644
--- /dev/null
+++ b/src/Utils/Misc.hs
@@ -0,0 +1,95 @@
+{-# LANGUAGE DeriveDataTypeable, RankNTypes, ScopedTypeVariables, BangPatterns #-}
+module Utils.Misc (
+ invertMap
+
+ , pNat
+ , commaWS
+
+ -- * Environment
+ , envIsSet
+ , getEnvMaybe
+
+ -- * List operations
+ , subsetOf
+ , noDuplicates
+ , equivClasses
+
+ -- * Control
+ , whileTrue
+
+ -- * Hashing
+ , stringSHA256
+) where
+
+import Data.List
+import System.Environment
+import System.IO.Unsafe
+import Data.Maybe
+import qualified Data.Set as S
+import Data.Map ( Map )
+import qualified Data.Map as M
+import Control.Applicative
+
+import Text.ParserCombinators.Parsec hiding (many, optional, (<|>))
+
+import Data.Digest.Pure.SHA (bytestringDigest, sha256)
+import Blaze.ByteString.Builder (toLazyByteString)
+import qualified Data.ByteString.Char8 as C8
+import qualified Data.ByteString.Lazy as L
+import qualified Data.ByteString.Base64 as B64 (encode)
+import qualified Blaze.ByteString.Builder.Char.Utf8 as Utf8 (fromString)
+
+-- | @noDuplicates xs@ returns @True@ if the list @xs@ contains no duplicates
+noDuplicates :: (Ord a) => [a] -> Bool
+noDuplicates xs = all ((==1).length) . group . sort $ xs
+
+-- | @getEnvMaybe k@ returns @Just v@ if @k=v@ is in the environment and @Nothing@ otherwise
+getEnvMaybe :: String -> Maybe String
+getEnvMaybe k = unsafePerformIO $ do
+ l <- getEnvironment
+ return $ lookup k l
+
+-- | @envIsSet k@ returns @True@ if there is a v such @k=v@ is in the environment and @False@ otherwise.
+envIsSet :: String -> Bool
+envIsSet k = isJust $ getEnvMaybe k
+
+-- | @subsetOf xs ys@ return @True@ if @set xs@ is a subset of @set ys@
+subsetOf :: Ord a => [a] -> [a] -> Bool
+subsetOf xs ys = (S.fromList xs) `S.isSubsetOf` (S.fromList ys)
+
+-- | Inverts a bijective Map.
+invertMap :: (Ord k, Ord v) => Map k v -> Map v k
+invertMap = M.fromList . map (uncurry (flip (,))) . M.toList
+
+-- | parse natural number
+pNat :: GenParser Char st Int
+pNat = read <$> many1 digit
+
+-- | parse comma
+commaWS :: GenParser Char st ()
+commaWS = char ',' *> spaces
+
+-- | @whileTrue m@ iterates m until it returns @False@.
+-- Returns the number of iterations @m@ was run. @0@
+-- means @m@ never returned @True@.
+whileTrue :: Monad m => m Bool -> m Int
+whileTrue m = go 0
+ where go (!n) = m >>= \b -> if b then go (n+1) else return n
+
+-- | Compute the equality classes given wrto a partial function.
+equivClasses :: (Ord a, Ord b) => [(a, b)] -> M.Map b (S.Set a)
+equivClasses =
+ foldl' insertEdge M.empty
+ where
+ insertEdge m (from,to) = M.insertWith' S.union to (S.singleton from) m
+
+-- | The SHA-256 hash of a string in base64 notation.
+stringSHA256 :: String -> String
+stringSHA256 =
+ C8.unpack . urlEncodeBase64 . C8.concat . L.toChunks
+ . bytestringDigest . sha256 . toLazyByteString . Utf8.fromString
+ where
+ urlEncodeBase64 = C8.init . C8.map replace . B64.encode
+ replace '/' = '_'
+ replace '+' = '-'
+ replace c = c
diff --git a/tamarin-prover-utils.cabal b/tamarin-prover-utils.cabal
new file mode 100644
--- /dev/null
+++ b/tamarin-prover-utils.cabal
@@ -0,0 +1,80 @@
+name: tamarin-prover-utils
+
+cabal-version: >= 1.8
+build-type: Simple
+version: 0.1.0.0
+license: GPL
+license-file: LICENSE
+category: Theorem Provers
+author: Benedikt Schmidt ,
+ Simon Meier
+maintainer: Simon Meier
+copyright: Benedikt Schmidt, Simon Meier, ETH Zurich, 2010-2012
+
+synopsis: Utility library for the tamarin prover.
+
+description: This is an internal library of the @tamarin@ prover for
+ security protocol verification
+ ().
+
+homepage: http://www.infsec.ethz.ch/research/software#TAMARIN
+
+
+----------------------
+-- library stanzas
+----------------------
+
+library
+ build-depends:
+ base == 4.*
+ , mtl == 2.0.*
+ , transformers == 0.2.*
+ , containers == 0.4.*
+ , fclabels == 1.0.*
+ , blaze-builder == 0.3.*
+ , base64-bytestring >= 0.1.0.3 && < 0.2
+ , bytestring == 0.9.*
+ , SHA == 1.4.*
+ , parsec == 3.1.*
+ , deepseq == 1.1.*
+ , syb >= 0.3.3 && < 0.4
+ , pretty == 1.1.*
+ , time == 1.2.*
+ , binary == 0.5.*
+
+ hs-source-dirs: src
+
+ exposed-modules:
+ Control.Basics
+ Control.Monad.Fresh
+ Control.Monad.Bind
+ Control.Monad.Disj
+
+ Data.Color
+ Data.DAG.Simple
+
+ Extension.Prelude
+ Extension.Data.Label
+ Extension.Data.Bounded
+
+ Text.Dot
+ Text.Isar
+ Text.PrettyPrint.Class
+ Text.PrettyPrint.Highlight
+ Text.PrettyPrint.Html
+
+ Logic.Connectives
+
+ System.Timing
+
+ Debug.Trace.Ignore
+
+ Utils.Misc
+
+ other-modules:
+ Control.Monad.Trans.Fresh
+ Control.Monad.Fresh.Class
+
+ Control.Monad.Trans.Disj
+ Control.Monad.Disj.Class
+