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/Term/Builtin/Convenience.hs b/src/Term/Builtin/Convenience.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Builtin/Convenience.hs
@@ -0,0 +1,226 @@
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Convenience abbreviations, mostly used for testing and debugging.
+module Term.Builtin.Convenience where
+
+import Term.Term
+import Term.LTerm
+import Term.Builtin.Signature
+
+--
+-- Shorter syntax for Term constructors
+----------------------------------------------------------------------
+
+(*:) :: Term a -> Term a -> Term a
+b *: e = FApp (AC Mult) [b,e]
+(#) :: Term a -> Term a -> Term a
+b # e = FApp (AC MUn) [b,e]
+(+:) :: Term a -> Term a -> Term a
+b +: e = FApp (AC Xor) [b,e]
+
+
+mult :: [Term a] -> Term a
+mult ts = FApp (AC Mult) ts
+
+union :: [Term a] -> Term a
+union ts = FApp (AC MUn) ts
+
+xor :: [Term a] -> Term a
+xor ts = FApp (AC Xor) ts
+
+appFree :: NonACSym -> [Term a] -> Term a
+appFree s ts = FApp (NonAC s) ts
+
+one, zero, empty :: Term a
+one = appFree oneSym []
+zero = appFree zeroSym []
+empty = appFree emptySym []
+
+inv :: Term a -> Term a
+inv e = appFree invSym [e]
+
+pair :: (Term a,Term a) -> Term a
+pair (x,y) = appFree pairSym [x, y]
+
+expo, adec, aenc, sdec, senc, sign :: (Term a,Term a) -> Term a
+expo (b,e) = appFree expSym [b,e]
+adec (a,b) = appFree adecSym [a,b]
+aenc (a,b) = appFree aencSym [a,b]
+sdec (a,b) = appFree sdecSym [a,b]
+senc (a,b) = appFree sencSym [a,b]
+sign (a,b) = appFree signSym [a,b]
+
+verify :: (Term a,Term a,Term a) -> Term a
+verify (a,b,c) = appFree verifySym [a,b,c]
+
+pk, fstC, sndC :: Term a -> Term a
+pk a = appFree pkSym [a]
+fstC a = appFree fstSym [a]
+sndC a = appFree sndSym [a]
+
+trueC :: Term a
+trueC = appFree trueSym []
+
+var :: String -> Int -> LNTerm
+var s i = varTerm $ LVar s LSortMsg i
+
+x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 :: LNTerm
+x0 = var "x" 0
+x1 = var "x" 1
+x2 = var "x" 2
+x3 = var "x" 3
+x4 = var "x" 4
+x5 = var "x" 5
+x6 = var "x" 6
+x7 = var "x" 7
+x8 = var "x" 8
+x9 = var "x" 9
+x10 = var "x" 10
+
+y0,y1,y2,y3,y4,y5,y6,y7,y8,y9 :: LNTerm
+y0 = var "y" 0
+y1 = var "y" 1
+y2 = var "y" 2
+y3 = var "y" 3
+y4 = var "y" 4
+y5 = var "y" 5
+y6 = var "y" 6
+y7 = var "y" 7
+y8 = var "y" 8
+y9 = var "y" 9
+
+freshVar :: String -> Int -> LNTerm
+freshVar s i = varTerm $ LVar s LSortFresh i
+
+fx0,fx1,fx2,fx3,fx4,fx5,fx6,fx7,fx8,fx9,fx10 :: LNTerm
+fx0 = freshVar "fx" 0
+fx1 = freshVar "fx" 1
+fx2 = freshVar "fx" 2
+fx3 = freshVar "fx" 3
+fx4 = freshVar "fx" 4
+fx5 = freshVar "fx" 5
+fx6 = freshVar "fx" 6
+fx7 = freshVar "fx" 7
+fx8 = freshVar "fx" 8
+fx9 = freshVar "fx" 9
+fx10 = freshVar "fx" 10
+
+pubVar :: String -> Int -> LNTerm
+pubVar s i = varTerm $ LVar s LSortPub i
+
+px0,px1,px2,px3,px4,px5,px6,px7,px8,px9,px10 :: LNTerm
+px0 = pubVar "px" 0
+px1 = pubVar "px" 1
+px2 = pubVar "px" 2
+px3 = pubVar "px" 3
+px4 = pubVar "px" 4
+px5 = pubVar "px" 5
+px6 = pubVar "px" 6
+px7 = pubVar "px" 7
+px8 = pubVar "px" 8
+px9 = pubVar "px" 9
+px10 = pubVar "px" 10
+
+lx1,lx2,lx3,lx4,lx5,lx6,lx7,lx8,lx9,lx10 :: LVar
+lx1 = LVar "x" LSortMsg 1
+lx2 = LVar "x" LSortMsg 2
+lx3 = LVar "x" LSortMsg 3
+lx4 = LVar "x" LSortMsg 4
+lx5 = LVar "x" LSortMsg 5
+lx6 = LVar "x" LSortMsg 6
+lx7 = LVar "x" LSortMsg 7
+lx8 = LVar "x" LSortMsg 8
+lx9 = LVar "x" LSortMsg 9
+lx10 = LVar "x" LSortMsg 10
+
+f1,f2,f3,f4,f5,f6,f7,f8,f9 :: LNTerm
+f1 = freshTerm "f1"
+f2 = freshTerm "f2"
+f3 = freshTerm "f3"
+f4 = freshTerm "f4"
+f5 = freshTerm "f5"
+f6 = freshTerm "f6"
+f7 = freshTerm "f7"
+f8 = freshTerm "f8"
+f9 = freshTerm "f9"
+
+p1,p2,p3,p4,p5,p6,p7,p8,p9 :: LNTerm
+p1 = pubTerm "p1"
+p2 = pubTerm "p2"
+p3 = pubTerm "p3"
+p4 = pubTerm "p4"
+p5 = pubTerm "p5"
+p6 = pubTerm "p6"
+p7 = pubTerm "p7"
+p8 = pubTerm "p8"
+p9 = pubTerm "p9"
+
+lv1,lv2,lv3,lv4,lv5,lv6,lv7,lv8,lv9 :: LVar
+lv1 = LVar "v1" LSortMsg 0
+lv2 = LVar "v2" LSortMsg 0
+lv3 = LVar "v3" LSortMsg 0
+lv4 = LVar "v4" LSortMsg 0
+lv5 = LVar "v5" LSortMsg 0
+lv6 = LVar "v6" LSortMsg 0
+lv7 = LVar "v7" LSortMsg 0
+lv8 = LVar "v8" LSortMsg 0
+lv9 = LVar "v9" LSortMsg 0
+
+v1,v2,v3,v4,v5,v6,v7,v8,v9 :: LNTerm
+v1 = Lit $ Var $ lv1
+v2 = Lit $ Var $ lv2
+v3 = Lit $ Var $ lv3
+v4 = Lit $ Var $ lv4
+v5 = Lit $ Var $ lv5
+v6 = Lit $ Var $ lv6
+v7 = Lit $ Var $ lv7
+v8 = Lit $ Var $ lv8
+v9 = Lit $ Var $ lv9
+
+li1,li2,li3,li4,li5,li6,li7,li8,li9 :: LVar
+li1 = LVar "i1" LSortNode 0
+li2 = LVar "i2" LSortNode 0
+li3 = LVar "i3" LSortNode 0
+li4 = LVar "i4" LSortNode 0
+li5 = LVar "i5" LSortNode 0
+li6 = LVar "i6" LSortNode 0
+li7 = LVar "i7" LSortNode 0
+li8 = LVar "i8" LSortNode 0
+li9 = LVar "i9" LSortNode 0
+
+i1,i2,i3,i4,i5,i6,i7,i8,i9 :: LNTerm
+i1 = Lit $ Var $ li1
+i2 = Lit $ Var $ li2
+i3 = Lit $ Var $ li3
+i4 = Lit $ Var $ li4
+i5 = Lit $ Var $ li5
+i6 = Lit $ Var $ li6
+i7 = Lit $ Var $ li7
+i8 = Lit $ Var $ li8
+i9 = Lit $ Var $ li9
+
+ls1,ls2,ls3,ls4,ls5,ls6,ls7,ls8,ls9 :: LVar
+ls1 = LVar "s1" LSortMSet 0
+ls2 = LVar "s2" LSortMSet 0
+ls3 = LVar "s3" LSortMSet 0
+ls4 = LVar "s4" LSortMSet 0
+ls5 = LVar "s5" LSortMSet 0
+ls6 = LVar "s6" LSortMSet 0
+ls7 = LVar "s7" LSortMSet 0
+ls8 = LVar "s8" LSortMSet 0
+ls9 = LVar "s9" LSortMSet 0
+
+s1,s2,s3,s4,s5,s6,s7,s8,s9 :: LNTerm
+s1 = Lit $ Var $ ls1
+s2 = Lit $ Var $ ls2
+s3 = Lit $ Var $ ls3
+s4 = Lit $ Var $ ls4
+s5 = Lit $ Var $ ls5
+s6 = Lit $ Var $ ls6
+s7 = Lit $ Var $ ls7
+s8 = Lit $ Var $ ls8
+s9 = Lit $ Var $ ls9
diff --git a/src/Term/Builtin/Rules.hs b/src/Term/Builtin/Rules.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Builtin/Rules.hs
@@ -0,0 +1,69 @@
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Builtin rewriting rules.
+module Term.Builtin.Rules (
+ -- * Rewriting rules
+ RRule(..)
+ , dhRules
+ , xorRules
+ , msetRules
+ , pairRules
+ , symEncRules
+ , asymEncRules
+ , signatureRules
+
+ -- * Convenience export
+ , module Term.Builtin.Signature
+) where
+
+import Term.LTerm
+import Term.SubtermRule
+import Term.Builtin.Signature
+import Term.Builtin.Convenience
+
+-- Rules for DH theory
+----------------------------------------------------------------------
+
+-- | The rewriting rules for Diffie-Hellman. This is a presentation due to Lankford
+-- with the finite variant property.
+dhRules :: [RRule LNTerm]
+dhRules =
+ [ expo(x1,one) `RRule` x1
+ , expo(expo(x1,x2),x3) `RRule` expo(x1,(x2 *: x3))
+
+ , x1 *: one `RRule` x1
+ , inv (inv x1) `RRule` x1
+ , inv one `RRule` one
+ , x1 *: (inv x1) `RRule` one
+ , inv x1 *: inv x2 `RRule` inv (x1 *: x2)
+ , inv (x1 *: x2) *: x2 `RRule` inv x1
+ , inv (inv x1 *: x2) `RRule` (x1 *: inv x2)
+ , x1 *: (inv (x1) *: x2) `RRule` x2
+ , inv x1 *: (inv x2 *: x3) `RRule` (inv (x1 *: x2) *: x3)
+ , inv (x1 *: x2) *: (x2 *: x3) `RRule` (inv x1 *: x3)
+ ]
+
+-- | The rewriting rules for Xor.
+xorRules :: [RRule LNTerm]
+xorRules =
+ [ x1 +: x1 `RRule` zero
+ , x1 +: zero `RRule` x1
+ , x1 +: (x1 +: x2) `RRule` x2 ]
+
+-- | The rewriting rules for multisets.
+msetRules :: [RRule LNTerm]
+msetRules = [ s1 # empty `RRule` s1 ]
+
+
+-- | The rewriting rules for standard subterm operators that are builtin.
+pairRules, symEncRules, asymEncRules, signatureRules :: [StRule]
+pairRules =
+ [ fstC (pair (x1,x2)) `StRule` (RhsPosition [0,0])
+ , sndC (pair (x1,x2)) `StRule` (RhsPosition [0,1]) ]
+symEncRules = [ sdec (senc (x1,x2), x2) `StRule` (RhsPosition [0,0]) ]
+asymEncRules = [ adec (aenc (x1, pk x2), x2) `StRule` (RhsPosition [0,0]) ]
+signatureRules = [ verify (sign (x1,x2), x1, pk x2) `StRule` (RhsGround trueC) ]
diff --git a/src/Term/Builtin/Signature.hs b/src/Term/Builtin/Signature.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Builtin/Signature.hs
@@ -0,0 +1,71 @@
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Builtin function symbols and signatures.
+module Term.Builtin.Signature where
+
+import Term.LTerm
+
+
+-- Builtin symbols (pair and inv are defined in Term.Term)
+----------------------------------------------------------------------
+
+-- | Binary builtin non-ac function symbols.
+sdecSym, sencSym, adecSym, aencSym, signSym :: NonACSym
+sdecSym = ("sdec",2)
+sencSym = ("senc",2)
+adecSym = ("adec",2)
+aencSym = ("aenc",2)
+signSym = ("sign",2)
+
+verifySym :: NonACSym
+verifySym = ("verify",3)
+
+-- | Unary builtin non-ac function symbols.
+fstSym, sndSym, pkSym, hashSym :: NonACSym
+fstSym = ("fst",1)
+sndSym = ("snd",1)
+pkSym = ("pk",1)
+hashSym = ("h",1)
+
+-- | Nullary builtin non-ac function symbols.
+trueSym :: NonACSym
+trueSym = ("true",0)
+
+-- Builtin signatures
+----------------------------------------------------------------------
+
+-- | The signature for the non-AC Diffie-Hellman function symbols.
+dhFunSig :: FunSig
+dhFunSig = [ expSym, oneSym, invSym ]
+
+-- | The signature for the non-AC Xor function symbols.
+xorFunSig :: FunSig
+xorFunSig = [ zeroSym ]
+
+-- | The signature for then non-AC multiset function symbols.
+msetFunSig :: FunSig
+msetFunSig = [ emptySym ]
+
+-- | The signature for pairs.
+pairFunSig :: FunSig
+pairFunSig = [ pairSym, fstSym, sndSym ]
+
+-- | The signature for symmetric encryption.
+symEncFunSig :: FunSig
+symEncFunSig = [ sdecSym, sencSym ]
+
+-- | The signature for asymmetric encryption.
+asymEncFunSig :: FunSig
+asymEncFunSig = [ adecSym, aencSym, pkSym ]
+
+-- | The signature for cryptographic signatures.
+signatureFunSig :: FunSig
+signatureFunSig = [ signSym, verifySym, trueSym, pkSym ]
+
+-- | The signature for hashing.
+hashFunSig :: FunSig
+hashFunSig = [ hashSym ]
diff --git a/src/Term/Classes.hs b/src/Term/Classes.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Classes.hs
@@ -0,0 +1,14 @@
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- | A type class for sized types.
+module Term.Classes where
+
+class Sized a where
+ size :: a -> Int
+
+instance Sized a => Sized [a] where
+ size = sum . map size
diff --git a/src/Term/LTerm.hs b/src/Term/LTerm.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/LTerm.hs
@@ -0,0 +1,533 @@
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances #-}
+{-# LANGUAGE MultiParamTypeClasses, DeriveDataTypeable, StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell, GeneralizedNewtypeDeriving #-}
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Terms with logical variables and names.
+module Term.LTerm (
+
+ -- * Names
+ Name(..)
+ , NameTag(..)
+ , NameId(..)
+
+ , NTerm
+
+ -- ** Queries
+ , sortOfName
+
+ -- ** Construction
+ , freshTerm
+ , pubTerm
+
+ -- * LVar
+ , LSort(..)
+ , LVar(..)
+ , LTerm
+ , LNTerm
+
+ , freshLVar
+ , sortPrefix
+ , sortSuffix
+ , sortCompare
+ , sortOfLTerm
+ , sortOfLNTerm
+ , isMsgVar
+ , isFreshVar
+ , trivial
+ , input
+
+ -- ** Manging Free LVars
+
+ , HasFrees(..)
+ , occurs
+ , freesList
+ , frees
+ , someInst
+ , rename
+ , eqModuloFreshness
+ , maximumVarIdx
+ , avoid
+ , evalFreshAvoiding
+ , evalFreshTAvoiding
+ , renameAvoiding
+
+ -- * BVar
+ , BVar(..)
+ , foldBVar
+ , fromFree
+
+ -- * Pretty-Printing
+ , prettyLVar
+ , prettyNTerm
+ , prettyLNTerm
+
+ -- * Convenience exports
+ , module Term.Term
+) where
+
+import Term.Term
+
+import Text.Isar
+
+import Control.Applicative
+import Control.Monad.Fresh
+import Control.Monad.Bind
+import Control.DeepSeq
+
+import Data.DeriveTH
+import qualified Data.Set as S
+import qualified Data.Map as M
+
+import Data.Generics hiding (GT)
+
+import qualified Data.DList as D
+import Data.Traversable
+import Data.Monoid
+import Data.Binary
+import Data.Foldable hiding (concatMap, elem)
+
+import Extension.Prelude
+import Extension.Data.Bounded
+
+import Logic.Connectives
+
+
+------------------------------------------------------------------------------
+-- Names
+------------------------------------------------------------------------------
+
+-- | Type safety for names.
+newtype NameId = NameId { getNameId :: String }
+ deriving( Eq, Ord, Typeable, Data, NFData, Binary )
+
+-- | Tags for names.
+data NameTag = FreshName | PubName
+ deriving( Eq, Ord, Show, Typeable, Data )
+
+-- | Names.
+data Name = Name {nTag :: NameTag, nId :: NameId}
+ deriving( Eq, Ord, Typeable, Data )
+
+-- | Terms with literals containing names and arbitrary variables.
+type NTerm v = VTerm Name v
+
+
+-- Instances
+------------
+
+instance IsConst Name where
+
+instance Show Name where
+ show (Name FreshName n) = "~'" ++ show n ++ "'"
+ show (Name PubName n) = "'" ++ show n ++ "'"
+
+instance Show NameId where
+ show = getNameId
+
+-- Construction of terms with names
+-----------------------------------
+
+-- | @freshTerm f@ represents the fresh name @f@.
+freshTerm :: String -> NTerm v
+freshTerm = Lit . Con . Name FreshName . NameId
+
+-- | @pubTerm f@ represents the pub name @f@.
+pubTerm :: String -> NTerm v
+pubTerm = Lit . Con . Name PubName . NameId
+
+-- | Return 'LSort' for given 'Name'.
+sortOfName :: Name -> LSort
+sortOfName (Name FreshName _) = LSortFresh
+sortOfName (Name PubName _) = LSortPub
+
+
+------------------------------------------------------------------------------
+-- LVar: logical variables
+------------------------------------------------------------------------------
+
+-- | Sorts for logical variables. They satisfy the following sub-sort relation:
+--
+-- > LSortMsg < LSortMSet
+-- > LSortFresh < LSortMsg
+-- > LSortPub < LSortMsg
+--
+data LSort = LSortPub -- ^ Arbitrary public names.
+ | LSortFresh -- ^ Arbitrary fresh names.
+ | LSortMsg -- ^ Arbitrary messages.
+ | LSortMSet -- ^ Sort for multisets.
+ | LSortNode -- ^ Sort for variables denoting nodes of derivation graphs.
+ deriving( Eq, Ord, Show, Enum, Bounded, Typeable, Data )
+
+-- | Logical variables. Variables with the same name and index but different
+-- sorts are regarded as different variables.
+data LVar = LVar
+ { lvarName :: String
+ , lvarSort :: !LSort
+ , lvarIdx :: {-# UNPACK #-} !Int
+ }
+ deriving( Typeable, Data )
+
+-- | Terms used for proving; i.e., variables fixed to logical variables.
+type LTerm c = VTerm c LVar
+
+-- | Terms used for proving; i.e., variables fixed to logical variables
+-- and constants to Names.
+type LNTerm = VTerm Name LVar
+
+-- | @freshLVar v@ represents a fresh logical variable with name @v@.
+freshLVar :: MonadFresh m => String -> LSort -> m LVar
+freshLVar n s = LVar n s <$> freshIdent n
+
+-- | Returns the most precise sort of an 'LTerm'.
+sortOfLTerm :: (c -> LSort) -> LTerm c -> LSort
+sortOfLTerm sortOfConst (Lit (Con c)) = sortOfConst c
+sortOfLTerm _ (Lit (Var (LVar _ s _))) = s
+sortOfLTerm _ (FApp (NonAC ("empty",0)) []) = LSortMSet
+sortOfLTerm _ (FApp (AC MUn) _) = LSortMSet
+sortOfLTerm _ _ = LSortMsg
+
+-- | Returns the most precise sort of an 'LNTerm'.
+sortOfLNTerm :: LNTerm -> LSort
+sortOfLNTerm = sortOfLTerm sortOfName
+
+-- | @sortCompare s1 s2@ compares @s1@ and @s2@ with respect to the partial order on sorts.
+-- Partial order: Node MSet
+-- |
+-- Msg
+-- / \
+-- Pub Fresh
+sortCompare :: LSort -> LSort -> Maybe Ordering
+sortCompare s1 s2 = case (s1, s2) of
+ (a, b) | a == b -> Just EQ
+ -- Node is incomparable to all other sorts, invalid input
+ (LSortNode, _ ) -> Nothing
+ (_, LSortNode) -> Nothing
+ -- MSet is greater than all except Node
+ (LSortMSet, _ ) -> Just GT
+ (_, LSortMSet) -> Just LT
+ -- Msg is greater than all sorts except Node and MSet
+ (LSortMsg, _ ) -> Just GT
+ (_, LSortMsg ) -> Just LT
+ -- The remaining combinations (Pub/Fresh) are incomparable
+ _ -> Nothing
+
+-- | @sortPrefix s@ is the prefix we use for annotating variables of sort @s@.
+sortPrefix :: LSort -> String
+sortPrefix LSortMsg = ""
+sortPrefix LSortFresh = "~"
+sortPrefix LSortPub = "$"
+sortPrefix LSortNode = "#"
+sortPrefix LSortMSet = "%"
+
+-- | @sortSuffix s@ is the suffix we use for annotating variables of sort @s@.
+sortSuffix :: LSort -> String
+sortSuffix LSortMsg = "msg"
+sortSuffix LSortFresh = "fresh"
+sortSuffix LSortPub = "pub"
+sortSuffix LSortNode = "node"
+sortSuffix LSortMSet = "mset"
+
+-- | Is a term a message variable?
+isMsgVar :: LNTerm -> Bool
+isMsgVar (Lit (Var v)) = (lvarSort v == LSortMsg)
+isMsgVar _ = False
+
+-- | Is a term a fresh variable?
+isFreshVar :: LNTerm -> Bool
+isFreshVar (Lit (Var v)) = (lvarSort v == LSortFresh)
+isFreshVar _ = False
+
+-- | The required components to construct the message.
+-- FIXME: Make inv/1 and pair/2 special?
+input :: LNTerm -> [LNTerm]
+input (FApp (AC Mult) ts) = concatMap input ts
+input (FApp (NonAC sym) ts) | sym `elem` [ invSym, pairSym ] = concatMap input ts
+input t = [t]
+
+-- | Is a message trivial; i.e., can for sure be instantiated with something
+-- known to the intruder?
+trivial :: LNTerm -> Bool
+trivial (FApp _ []) = True
+trivial (Lit (Con (Name PubName _))) = True
+trivial (Lit (Var v)) = case lvarSort v of
+ LSortPub -> True
+ LSortMsg -> True
+ _ -> False
+trivial _ = False
+
+
+-- BVar: Bound variables
+------------------------
+
+-- | Bound and free variables.
+data BVar v = Bound Int -- ^ A bound variable in De-Brujin notation.
+ | Free v -- ^ A free variable.
+ deriving( Eq, Ord, Show, Data, Typeable )
+
+
+
+-- | Fold a possibly bound variable.
+{-# INLINE foldBVar #-}
+foldBVar :: (Int -> a) -> (v -> a) -> BVar v -> a
+foldBVar fBound fFree = go
+ where
+ go (Bound i) = fBound i
+ go (Free v) = fFree v
+
+instance Functor BVar where
+ fmap f = foldBVar Bound (Free . f)
+
+instance Foldable BVar where
+ foldMap f = foldBVar mempty f
+
+instance Traversable BVar where
+ traverse f = foldBVar (pure . Bound) (fmap Free . f)
+
+instance Applicative BVar where
+ pure = return
+ (<*>) = ap
+
+instance Monad BVar where
+ return = Free
+ m >>= f = foldBVar Bound f m
+
+-- | Extract the name of free variable under the assumption the variable is
+-- guaranteed to be of the form @Free a@.
+fromFree :: BVar v -> v
+fromFree (Free v) = v
+fromFree (Bound i) = error $ "fromFree: bound variable '" ++ show i ++ "'"
+
+
+-- Instances
+------------
+
+instance Eq LVar where
+ (LVar n1 s1 i1) == (LVar n2 s2 i2) = i1 == i2 && s1 == s2 && n1 == n2
+
+-- An ord instane that prefers the 'lvarIdx' over the 'lvarName'.
+instance Ord LVar where
+ compare (LVar x1 x2 x3) (LVar y1 y2 y3) =
+ compare x3 y3 & compare x2 y2 & compare x1 y1 & EQ
+ where
+ EQ & x = x
+ x & _ = x
+
+instance Show LVar where
+ show (LVar v s i) =
+ sortPrefix s ++ body
+ where
+ body | null v = show i
+-- | isDigit (last v) = v ++ "." ++ show i
+ | i == 0 = v
+ | otherwise = v ++ "." ++ show i
+
+instance IsVar LVar where
+
+------------------------------------------------------------------------------
+-- Managing bound and free LVars
+------------------------------------------------------------------------------
+
+-- | @HasFree t@ denotes that the type @t@ has free @LVar@ variables. They can
+-- be collected using 'foldFrees' and mapped in the context of an applicative
+-- functor using 'mapFrees'.
+--
+-- When defining instances of this class, you have to ensure that only the free
+-- LVars are collected and mapped and no others. The instances for standard
+-- Haskell types assume that all variables free in all type arguments are free.
+--
+-- Once we need it, we can use type synonym instances to parametrize over the
+-- variable type.
+--
+class HasFrees t where
+ foldFrees :: Monoid m => (LVar -> m ) -> t -> m
+ mapFrees :: Applicative f => (LVar -> f LVar ) -> t -> f t
+
+
+-- | @v `occurs` t@ iff variable @v@ occurs as a free variable in @t@.
+occurs :: HasFrees t => LVar -> t -> Bool
+occurs x = getAny . foldFrees (Any . (x ==))
+
+-- | @freesDList t@ is the difference list of all free variables of @t@.
+freesDList :: HasFrees t => t -> D.DList LVar
+freesDList = foldFrees pure
+
+-- | @freesList t@ is the list of all free variables of @t@.
+freesList :: HasFrees t => t -> [LVar]
+freesList = D.toList . freesDList
+
+-- | @frees t@ is the sorted and duplicate-free list of all free variables in
+-- @t@.
+frees :: HasFrees t => t -> [LVar]
+frees = sortednub . freesList
+
+-- | @someInst t@ returns an instance of @t@ where all free variables whose
+-- binding is not yet determined by the caller are replaced with fresh
+-- variables.
+someInst :: (MonadFresh m, MonadBind LVar LVar m, HasFrees t) => t -> m t
+someInst = mapFrees (\x -> importBinding (`LVar` lvarSort x) x (lvarName x))
+
+-- | @rename t@ replaces all variables in @t@ with fresh variables
+rename :: (MonadFresh m, HasFrees a) => a -> m a
+rename x = evalBindT (someInst x) noBindings
+
+-- | @eqModuloFreshness t1 t2@ checks whether @t1@ is equal to @t2@ modulo
+-- renaming of indices of free variables.
+eqModuloFreshness :: (HasFrees a, Eq a) => a -> a -> Bool
+eqModuloFreshness t1 =
+ -- this formulation shares normalisation of t1 among further calls to
+ -- different t2.
+ (normIndices t1 ==) . normIndices
+ where
+ normIndices = (`evalFresh` nothingUsed) . rename
+
+-- | The maximum index of all free variables.
+maximumVarIdx :: HasFrees t => t -> Int
+maximumVarIdx = getBoundedMax . foldFrees (BoundedMax . lvarIdx)
+
+-- | @avoid t@ computes a 'FreshState' that avoids generating
+-- variables occurring in @t@.
+avoid :: HasFrees t => t -> FreshState
+avoid = max 0 . succ . maximumVarIdx
+
+-- | @m `evalFreshAvoiding` t@ evaluates the monadic action @m@ with a
+-- fresh-variable supply that avoids generating variables occurring in @t@.
+evalFreshAvoiding :: HasFrees t => Fresh a -> t -> a
+evalFreshAvoiding m = evalFresh m . avoid
+
+-- | @m `evalFreshTAvoiding` t@ evaluates the monadic action @m@ in the
+-- underlying monad with a fresh-variable supply that avoids generating
+-- variables occurring in @t@.
+evalFreshTAvoiding :: (Monad m, HasFrees t) => FreshT m a -> t -> m a
+evalFreshTAvoiding m = evalFreshT m . avoid
+
+-- | @s `renameAvoiding` t@ replaces all free variables in @s@ by
+-- fresh variables avoiding variables in @t@.
+renameAvoiding :: (HasFrees s, HasFrees t) => s -> t -> s
+s `renameAvoiding` t = rename s `evalFreshAvoiding` t
+
+-- Instances
+------------
+
+instance HasFrees LVar where
+ foldFrees = id
+ mapFrees = id
+
+instance HasFrees v => HasFrees (Lit c v) where
+ foldFrees f (Var x) = foldFrees f x
+ foldFrees _ _ = mempty
+
+ mapFrees f (Var x) = Var <$> mapFrees f x
+ mapFrees _ l = pure l
+
+instance HasFrees v => HasFrees (BVar v) where
+ foldFrees _ (Bound _) = mempty
+ foldFrees f (Free v) = foldFrees f v
+
+ mapFrees _ b@(Bound _) = pure b
+ mapFrees f (Free v) = Free <$> mapFrees f v
+
+instance HasFrees l => HasFrees (Term l) where
+ foldFrees f = foldMap (foldFrees f)
+ mapFrees f = traverse (mapFrees f)
+
+instance HasFrees a => HasFrees (Equal a) where
+ foldFrees f = foldMap (foldFrees f)
+ mapFrees f = traverse (mapFrees f)
+
+instance HasFrees a => HasFrees (Match a) where
+ foldFrees f = foldMap (foldFrees f)
+ mapFrees f = traverse (mapFrees f)
+
+instance HasFrees a => HasFrees (RRule a) where
+ foldFrees f = foldMap (foldFrees f)
+ mapFrees f = traverse (mapFrees f)
+
+
+instance HasFrees () where
+ foldFrees _ = const mempty
+ mapFrees _ = pure
+
+instance HasFrees Int where
+ foldFrees _ = const mempty
+ mapFrees _ = pure
+
+instance HasFrees Char where
+ foldFrees _ = const mempty
+ mapFrees _ = pure
+
+instance HasFrees a => HasFrees (Maybe a) where
+ foldFrees f = foldMap (foldFrees f)
+ mapFrees f = traverse (mapFrees f)
+
+instance (HasFrees a, HasFrees b) => HasFrees (Either a b) where
+ foldFrees f = either (foldFrees f) (foldFrees f)
+ mapFrees f = either (fmap Left . mapFrees f) (fmap Right . mapFrees f)
+
+instance (HasFrees a, HasFrees b) => HasFrees (a, b) where
+ foldFrees f (x, y) = foldFrees f x `mappend` foldFrees f y
+ mapFrees f (x, y) = (,) <$> mapFrees f x <*> mapFrees f y
+
+instance (HasFrees a, HasFrees b, HasFrees c) => HasFrees (a, b, c) where
+ foldFrees f (x, y, z) = foldFrees f (x, (y, z))
+ mapFrees f (x0, y0, z0) =
+ (\(x, (y, z)) -> (x, y, z)) <$> mapFrees f (x0, (y0, z0))
+
+instance HasFrees a => HasFrees [a] where
+ foldFrees f = foldMap (foldFrees f)
+ mapFrees f = traverse (mapFrees f)
+
+instance HasFrees a => HasFrees (Disj a) where
+ foldFrees f = foldMap (foldFrees f)
+ mapFrees f = traverse (mapFrees f)
+
+instance HasFrees a => HasFrees (Conj a) where
+ foldFrees f = foldMap (foldFrees f)
+ mapFrees f = traverse (mapFrees f)
+
+instance (Ord a, HasFrees a) => HasFrees (S.Set a) where
+ foldFrees f = foldMap (foldFrees f)
+ mapFrees f = fmap S.fromList . mapFrees f . S.toList
+
+instance (Ord k, HasFrees k, HasFrees v) => HasFrees (M.Map k v) where
+ foldFrees f = M.foldrWithKey combine mempty
+ where
+ combine k v m = foldFrees f k `mappend` (foldFrees f v `mappend` m)
+ mapFrees f = fmap M.fromList . mapFrees f . M.toList
+
+
+------------------------------------------------------------------------------
+-- Pretty Printing
+------------------------------------------------------------------------------
+
+-- | Pretty print a 'LVar'.
+prettyLVar :: Document d => LVar -> d
+prettyLVar = text . show
+
+-- | Pretty print an @NTerm@.
+prettyNTerm :: (Show v, Document d) => NTerm v -> d
+prettyNTerm = prettyTerm (text . show)
+
+-- | Pretty print an @LTerm@.
+prettyLNTerm :: Document d => LNTerm -> d
+prettyLNTerm = prettyNTerm
+
+
+-- derived instances
+--------------------
+
+$( derive makeBinary ''NameTag)
+$( derive makeBinary ''Name)
+$( derive makeBinary ''LSort)
+$( derive makeBinary ''LVar)
+$( derive makeBinary ''BVar)
+
+$( derive makeNFData ''NameTag)
+$( derive makeNFData ''Name)
+$( derive makeNFData ''LSort)
+$( derive makeNFData ''LVar)
+$( derive makeNFData ''BVar)
diff --git a/src/Term/Maude/Process.hs b/src/Term/Maude/Process.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Maude/Process.hs
@@ -0,0 +1,342 @@
+{-# LANGUAGE TemplateHaskell, DeriveDataTypeable, DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts, NamedFieldPuns #-}
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- AC-unification of DH terms using Maude as a backend.
+module Term.Maude.Process (
+ -- * Handle to a maude process
+ MaudeHandle(..)
+ , startMaude
+ , getMaudeStats
+
+ -- * Unification using Maude
+ , unifyViaMaude
+
+ -- * Matching using Maude
+ , matchViaMaude
+
+ -- * Normalization using Maude
+ , normViaMaude
+
+ -- * Managing the persistent Maude process
+ , WithMaude
+) where
+
+import Data.Either
+import Data.List
+import Data.Traversable hiding ( mapM )
+import qualified Data.Map as M
+
+import Term.Term
+import Term.LTerm
+import Term.Maude.Types
+import Term.Substitution
+
+import Control.Applicative
+import Control.Monad.Reader
+import Control.Monad.Fresh
+import Control.Concurrent
+import Control.Exception (onException, evaluate)
+import Control.DeepSeq (rnf)
+import Control.Monad.Bind
+
+import System.Process
+import System.IO
+import System.Directory
+
+import Utils.Misc
+
+
+-- Pretty printing Maude commands
+----------------------------------------------------------------------
+
+-- | The term algebra and rewriting rules as a functional module in Maude.
+theory :: MaudeSig -> String
+theory msig@(MaudeSig {enableDH, enableXor, enableMSet, funSig}) = unlines $
+ [ "fmod MSG is"
+ , " protecting NAT ." ]
+ ++
+ (if enableMSet
+ then [ " sort Pub Fresh Msg MSet Node TOP ."
+ , " subsort Msg < MSet ."
+ , " subsort MSet < TOP ."
+ , " op m : Nat -> MSet ."
+ , " op "++funsymPrefix++"mun : MSet MSet -> MSet [comm assoc] ."
+ , " op "++funsymPrefix++"empty : -> MSet ."
+ ]
+ else [ " sort Pub Fresh Msg Node TOP ."])
+ ++
+ [ " subsort Pub < Msg ."
+ , " subsort Fresh < Msg ."
+ , " subsort Msg < TOP ."
+ , " subsort Node < TOP ."
+ -- constants
+ , " op f : Nat -> Fresh ."
+ , " op p : Nat -> Pub ."
+ , " op c : Nat -> Msg ."
+ , " op n : Nat -> Node ."
+ -- used for encoding App List [t1,..,tk]
+ -- list(cons(t1,cons(t2,..,cons(tk,nil)..)))
+ , " op "++funsymPrefix++"list : TOP -> TOP ."
+ , " op "++funsymPrefix++"cons : TOP TOP -> TOP ."
+ , " op "++funsymPrefix++"nil : -> TOP ." ]
+ ++
+ (if enableDH
+ then
+ [ " op "++funsymPrefix++"one : -> Msg ."
+ , " op "++funsymPrefix++"exp : Msg Msg -> Msg ."
+ , " op "++funsymPrefix++"mult : Msg Msg -> Msg [comm assoc] ."
+ , " op "++funsymPrefix++"inv : Msg -> Msg ." ]
+ else [])
+ ++
+ (if enableXor
+ then
+ [ " op "++funsymPrefix++"zero : -> Msg ."
+ , " op "++funsymPrefix++"xor : Msg Msg -> Msg [comm assoc] ."]
+ else [])
+ ++
+ map theoryFunSym funSig
+ ++
+ (map theoryRule $ rrulesForMaudeSig msig)
+ ++
+ [ "endfm" ]
+ where
+ theoryFunSym (s,ar) =
+ " op " ++ funsymPrefix ++ s ++" : " ++(concat $ replicate ar "Msg ")++" -> Msg ."
+ theoryRule (l `RRule` r) =
+ " eq " ++ ppMaude lm ++" = " ++ ppMaude rm ++" ."
+ where (lm,rm) = evalBindT ((,) <$> lTermToMTerm' l <*> lTermToMTerm' r) noBindings
+ `evalFresh` nothingUsed
+
+--
+-- Unification using Maude
+----------------------------------------------------------------------
+
+-- | Check environment if communication with Maude should be logged
+dEBUGMAUDE ::Bool
+dEBUGMAUDE = envIsSet "DEBUG_MAUDE"
+
+-- Unification using a persistent Maude process
+-----------------------------------------------------------------------
+
+-- | A handle to a Maude process. It requires the Maude path for Signatures to
+-- be serializable. If we also add the string for the Maude config file, then
+-- it would even be serializable on its own.
+data MaudeHandle = MaudeHandle { mhFilePath :: FilePath
+ , mhMaudeSig :: MaudeSig
+ , mhProc :: MVar MaudeProcess }
+
+-- | @getMaudeStats@ returns the maude stats formatted as a string.
+getMaudeStats :: MaudeHandle -> IO String
+getMaudeStats (MaudeHandle {mhProc = maude}) =
+ withMVar maude $ \mp -> do
+ let mc = matchCount mp
+ uc = unifCount mp
+ return $ "Maude has been called "++show (mc+uc)++ " times ("
+ ++show uc++" unifications and "++show mc++" matchings)."
+
+data MaudeProcess = MP {
+ mIn :: !Handle
+ , mOut :: !Handle
+ , _mErr :: !Handle
+ , mProc :: !ProcessHandle
+ , unifCount :: !Int
+ , matchCount :: !Int
+ , normCount :: !Int
+ , mFile :: String
+ }
+
+-- | @startMaude@ starts a new instance of Maude and returns a Handle to it.
+startMaude :: FilePath -> MaudeSig -> IO MaudeHandle
+startMaude maudePath maudeSig = do
+ -- create theory file for maude
+ tempDir <- getTemporaryDirectory
+ (tempFile, tempH) <- openTempFile tempDir "theory.maude"
+ hPutStr tempH (theory maudeSig)
+ hClose tempH
+ -- start maude
+ mv <- newMVar =<< startMaudeProcess maudePath tempFile
+ -- Add a finalizer to the MVar that stops maude and removes the theory
+ -- file.
+ addMVarFinalizer mv $ withMVar mv $ \mp -> do
+ terminateProcess (mProc mp) <* waitForProcess (mProc mp)
+ removeFile (mFile mp)
+ -- return the maude handle
+ return (MaudeHandle maudePath maudeSig mv)
+
+-- | Start a Maude process.
+startMaudeProcess :: FilePath -- ^ Path to Maude
+ -> FilePath -- ^ Path to Maude theory file
+ -> IO (MaudeProcess)
+startMaudeProcess maudePath maudeTheoryFile = do
+ (hin,hout,herr,hproc) <- runInteractiveCommand maudeCmd
+ _ <- getToDelim hout
+ return (MP hin hout herr hproc 0 0 0 maudeTheoryFile)
+ where
+ maudeCmd
+ | dEBUGMAUDE = "sh -c \"tee /tmp/maude.input | "
+ ++ maudePath ++ " -no-tecla -no-banner -no-wrap -batch "
+ ++ maudeTheoryFile ++ "\" | tee /tmp/maude.output"
+ | otherwise =
+ maudePath ++ " -no-tecla -no-banner -no-wrap -batch "
+ ++ maudeTheoryFile
+
+-- | Restart the Maude process on this handle.
+restartMaude :: MaudeHandle -> IO ()
+restartMaude (MaudeHandle maudePath _ mv) = modifyMVar_ mv $ \mp -> do
+ terminateProcess (mProc mp) <* waitForProcess (mProc mp)
+ startMaudeProcess maudePath (mFile mp)
+
+-- | @getToDelim ih@ reads input from @ih@ until @mDelim@ is encountered.
+-- It returns the string read up to (not including) mDelim.
+getToDelim :: Handle -> IO String
+getToDelim ih = go []
+ where
+ go acc = do
+ c <- hGetChar ih
+ let acc' = c:acc
+ if mDelim `isPrefixOf` acc'
+ then return (reverse (drop (length mDelim) acc'))
+ else go acc'
+ mDelim = reverse "Maude> "
+
+-- | @callMaude cmd@ sends the command @cmd@ to Maude and returns Maude's
+-- output up to the next prompt sign.
+callMaude :: MaudeHandle
+ -> (MaudeProcess -> MaudeProcess) -- ^ Statistics updater.
+ -> String -> IO String
+callMaude hnd updateStatistics cmd = do
+ -- Ensure that the command is fully evaluated and therefore does not depend
+ -- on another call to Maude anymore. Otherwise, we could end up in a
+ -- deadlock.
+ evaluate (rnf cmd)
+ -- If there was an exception, then we might be out of sync with the current
+ -- persistent Maude process: restart the process.
+ (`onException` restartMaude hnd) $ modifyMVar (mhProc hnd) $ \mp -> do
+ let inp = mIn mp
+ out = mOut mp
+ hPutStr inp cmd
+ hFlush inp
+ mp' <- evaluate (updateStatistics mp)
+ res <- getToDelim out
+ return (mp', res)
+
+-- | Compute a result via Maude.
+computeViaMaude ::
+ (Show a, Show b, Ord c)
+ => MaudeHandle
+ -> (MaudeProcess -> MaudeProcess) -- ^ Update statistics
+ -> (a -> BindT (Lit c LVar) MaudeLit Fresh String) -- ^ Conversion to Maude
+ -> (M.Map MaudeLit (Lit c LVar) -> MSubst -> b) -- ^ Conversion from Maude
+ -> a
+ -> IO [b]
+computeViaMaude hnd updateStats toMaude fromMaude inp = do
+ let (cmd, bindings) = runConversion $ toMaude inp
+ s <- callMaude hnd updateStats cmd
+ let esubstsm = parseMaudeReply s
+ substs = map (fromMaude bindings) $ rights esubstsm
+ case lefts esubstsm of
+ [] -> return $ substs
+ es -> fail $ "\ncomputeViaMaude:\nParse error: \n" ++
+ concatMap show es ++
+ "\n For Maude Output:\n" ++ s ++
+ "\nFor query:\n" ++ cmd
+
+
+------------------------------------------------------------------------------
+-- Unification
+------------------------------------------------------------------------------
+
+-- | @unifyCmd eqs@ returns the Maude command to solve the unification problem @eqs@.
+-- Expects a nonempty list of equations
+unifyCmd :: [Equal MTerm] -> [Char]
+unifyCmd [] = error "unifyCmd: cannot create cmd for empty list of equations."
+unifyCmd eqs =
+ "unify in MSG : " ++seqs++" .\n"
+ where
+ ppEq (Equal t1 t2) = ppMaude t1 ++ " =? " ++ ppMaude t2
+ seqs = intercalate " /\\ " $ map ppEq eqs
+
+
+-- | @unifyViaMaude hnd eqs@ computes all AC unifiers of @eqs@ using the
+-- Maude process @hnd@.
+unifyViaMaude
+ :: (IsConst c , Show (Lit c LVar), Ord c)
+ => MaudeHandle
+ -> (c -> LSort) -> [Equal (VTerm c LVar)] -> IO [SubstVFresh c LVar]
+unifyViaMaude _ _ [] = return [emptySubstVFresh]
+unifyViaMaude hnd sortOf eqs =
+ computeViaMaude hnd incUnifCount toMaude msubstToLSubstVFresh eqs
+ where
+ toMaude = fmap unifyCmd . mapM (traverse (lTermToMTerm sortOf))
+ incUnifCount mp = mp { unifCount = 1 + unifCount mp }
+
+
+------------------------------------------------------------------------------
+-- Matching modulo AC
+------------------------------------------------------------------------------
+
+-- | @matchCmd p t@ returns the Maude command to match the terms @t@ to the
+-- pattern @p@.
+matchCmd :: [Equal MTerm] -> String
+matchCmd eqs =
+ "match in MSG : " ++ppTerms t2s++ " <=? " ++ ppTerms t1s++" .\n"
+ where
+ -- FIXME: slow
+ (t1s,t2s) = unzip [ (a,b) | Equal a b <- eqs ]
+ ppTerms = ppMaude . listToTerm
+
+-- | @matchViaMaude (t, p)@ computes a complete set of AC matchers of the term
+-- @t@ to the pattern @p@ via Maude.
+matchViaMaude :: (IsConst c , Show (Lit c LVar), Ord c)
+ => MaudeHandle
+ -> (c -> LSort)
+ -> [Match (VTerm c LVar)]
+ -> IO [Subst c LVar]
+matchViaMaude _ _ [] = return [emptySubst]
+matchViaMaude hnd sortOf matcheqs =
+ computeViaMaude hnd incMatchCount toMaude msubstToLSubstVFree eqs
+ where
+ toMaude = fmap matchCmd . mapM (traverse (lTermToMTerm sortOf))
+ incMatchCount mp = mp { matchCount = 1 + matchCount mp }
+ eqs = [Equal t p | MatchWith t p <- matcheqs ]
+
+------------------------------------------------------------------------------
+-- Normalization of terms
+------------------------------------------------------------------------------
+
+-- | @normCmd t@ returns the Maude command to normalize the term @t@
+-- pattern @p@.
+normCmd :: MTerm -> String
+normCmd tm = "reduce "++ppMaude tm++" .\n"
+
+
+-- | @normViaMaude t@ normalizes the term t via Maude.
+normViaMaude :: (IsConst c , Show (Lit c LVar), Ord c)
+ => MaudeHandle
+ -> (c -> LSort)
+ -> VTerm c LVar
+ -> IO (VTerm c LVar)
+normViaMaude hnd sortOf t = do
+ let (cmd, bindings) = runConversion $ toMaude t
+ s <- callMaude hnd incNorm cmd
+ case parseReduceSolution s of
+ Right mt -> return $ evalBindT (mTermToLNTerm "z" mt) bindings
+ `evalFresh` nothingUsed
+ Left e -> fail $ "\ncomputeViaMaude:\nParse error: \n" ++
+ show e ++
+ "\n For Maude Output:\n" ++ s ++
+ "\nFor query:\n" ++ cmd
+ where
+ toMaude = fmap normCmd . (lTermToMTerm sortOf)
+ incNorm mp = mp { normCount = 1 + normCount mp }
+
+-- Passing the Handle to Maude via a Reader monad
+-------------------------------------------------
+
+-- | Values that depend on a 'MaudeHandle'.
+type WithMaude = Reader MaudeHandle
diff --git a/src/Term/Maude/Types.hs b/src/Term/Maude/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Maude/Types.hs
@@ -0,0 +1,394 @@
+{-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
+{-# LANGUAGE TemplateHaskell, FlexibleContexts, TupleSections, NamedFieldPuns #-}
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Types for communicating with Maude.
+module Term.Maude.Types where
+
+import Term.Term
+import Term.LTerm
+import Term.Builtin.Rules
+import Term.Substitution
+import Term.SubtermRule
+
+import Utils.Misc
+import Extension.Prelude
+
+import Control.Monad.Fresh
+import Control.Monad.Bind
+import Control.Applicative
+import Control.DeepSeq
+
+import Data.DeriveTH
+import Data.Binary
+import Data.Foldable (asum)
+import Data.Traversable
+import Data.List
+import Data.Monoid
+import Data.List.Split hiding (sepBy, oneOf)
+import Data.Maybe
+import qualified Data.Map as M
+import Data.Map ( Map )
+
+import Text.ParserCombinators.Parsec hiding (many, optional, (<|>))
+import qualified Text.PrettyPrint.Highlight as P
+
+-- Maude Terms
+----------------------------------------------------------------------
+
+data MaudeLit = MaudeVar Int LSort
+ | FreshVar Int LSort
+ | MaudeConst Int LSort
+ deriving (Eq, Ord, Show)
+
+type MTerm = Term MaudeLit
+
+type MSubst = [((LSort, Int), MTerm)]
+
+
+-- Maude Signatures
+----------------------------------------------------------------------
+
+-- | The required information to define a @Maude functional module@.
+data MaudeSig = MaudeSig
+ { enableDH :: Bool
+ , enableXor :: Bool
+ , enableMSet :: Bool
+ , funSig :: FunSig -- ^ function signature not including the function symbols for DH, Xor, MSet
+ , stRules :: [StRule]
+ }
+ deriving (Ord, Show, Eq)
+
+-- | The empty maude signature.
+emptyMaudeSig :: MaudeSig
+emptyMaudeSig = MaudeSig False False False [] []
+
+-- | A monoid instance to combine maude signatures.
+instance Monoid MaudeSig where
+ (MaudeSig dh xor mset funsig stRules) `mappend` (MaudeSig dh' xor' mset' funsig' stRules') =
+ MaudeSig (dh || dh') (xor || xor') (mset || mset')
+ (sortednub $ funsig ++ funsig') (sortednub $ stRules ++ stRules')
+ mempty = emptyMaudeSig
+
+-- | Maude signatures for the AC symbols.
+dhMaudeSig, xorMaudeSig, msetMaudeSig :: MaudeSig
+dhMaudeSig = emptyMaudeSig { enableDH = True }
+xorMaudeSig = emptyMaudeSig { enableXor = True }
+msetMaudeSig = emptyMaudeSig { enableMSet = True }
+
+-- | Maude signatures for the default subterm symbols.
+pairMaudeSig, symEncMaudeSig, asymEncMaudeSig, signatureMaudeSig, hashMaudeSig :: MaudeSig
+pairMaudeSig = emptyMaudeSig { funSig = pairFunSig, stRules = pairRules }
+symEncMaudeSig = emptyMaudeSig { funSig = symEncFunSig, stRules = symEncRules }
+asymEncMaudeSig = emptyMaudeSig { funSig = asymEncFunSig, stRules = asymEncRules }
+signatureMaudeSig = emptyMaudeSig { funSig = signatureFunSig, stRules = signatureRules }
+hashMaudeSig = emptyMaudeSig { funSig = hashFunSig, stRules = [] }
+
+-- | The minimal maude signature.
+minimalMaudeSig :: MaudeSig
+minimalMaudeSig = pairMaudeSig
+
+-- | Maude signatures with all builtin symbols.
+allMaudeSig :: MaudeSig
+allMaudeSig = mconcat
+ [ dhMaudeSig, xorMaudeSig, msetMaudeSig
+ , pairMaudeSig, symEncMaudeSig, asymEncMaudeSig, signatureMaudeSig, hashMaudeSig ]
+
+-- | @rrulesForMaudeSig msig@ returns all rewriting rules including the rules
+-- for xor, dh, and multiset.
+rrulesForMaudeSig :: MaudeSig -> [RRule LNTerm]
+rrulesForMaudeSig (MaudeSig {enableXor, enableDH, enableMSet, stRules}) =
+ map stRuleToRRule stRules
+ ++ (if enableDH then dhRules else [])
+ ++ (if enableXor then xorRules else [])
+ ++ (if enableMSet then msetRules else [])
+
+-- | @funSigForMaudeSig msig@ returns all non-AC function symbols including the
+-- function symbols for xor, dh, and multiset.
+funSigForMaudeSig :: MaudeSig -> FunSig
+funSigForMaudeSig (MaudeSig {enableXor, enableDH, enableMSet, funSig}) =
+ funSig
+ ++ (if enableDH then dhFunSig else [])
+ ++ (if enableXor then xorFunSig else [])
+ ++ (if enableMSet then msetFunSig else [])
+
+-- Convert between MTerms and LNTerms
+------------------------------------------------------------------------
+
+-- | Convert an @LNTerm@ to an @MTerm@.
+lTermToMTerm' :: (MonadBind (Lit Name LVar) MaudeLit m, MonadFresh m)
+ => LNTerm -- ^ The term to translate.
+ -> m MTerm
+lTermToMTerm' = lTermToMTerm sortOfName
+
+-- | Convert an @LNTerm@ with arbitrary names to an @MTerm@.
+lTermToMTerm :: (MonadBind (Lit c LVar) MaudeLit m, MonadFresh m, Show (Lit c LVar), Ord c)
+ => (c -> LSort) -- ^ A function that returns the sort of a constant.
+ -> VTerm c LVar -- ^ The term to translate.
+ -> m MTerm
+lTermToMTerm sortOf =
+ traverse exportLit
+ where
+ exportLit a@(Var lv) =
+ importBinding (\_ i -> MaudeVar i (lvarSort lv)) a "x"
+ exportLit a@(Con n) = importBinding (\_ i -> MaudeConst i (sortOf n)) a "a"
+
+-- | Convert a 'MaudeTerm' to an 'LNTerm' under the assumption that the bindings
+-- for the constants are already available.
+--
+-- Use @runBindCtxt@ with the inverted map from the @lTermtoMaudeTerm@ conversion to
+-- ensure this.
+mTermToLNTerm :: (MonadBind MaudeLit (Lit c LVar) m, MonadFresh m, Show (Lit c LVar), Ord c, Show c)
+ => String -- ^ Name hint for freshly generated variables.
+ -> MTerm -- ^ The maude term to convert.
+ -> m (VTerm c LVar)
+mTermToLNTerm nameHint =
+ traverse importLit
+ where
+ importLit a@(MaudeVar _ lsort) = importBinding (\n i -> Var (LVar n lsort i)) a nameHint
+ importLit a@(FreshVar _ lsort) = importBinding (\n i -> Var (LVar n lsort i)) a nameHint
+ importLit a = fromMaybe (error $ "fromMTerm: unknown constant `" ++ show a ++ "'") <$>
+ lookupBinding a
+
+
+-- Back and forth conversions
+------------------------------------------------------------------------
+
+-- | Run a @BindT (Lit c LVar) MaudeLit Fresh@ computation
+-- with an empty fresh supply and an empty binding map and return
+-- the result and the resulting inverted binding map.
+runConversion :: Ord c
+ => BindT (Lit c LVar) MaudeLit Fresh a -- ^ Computation to execute.
+ -> (a, Map MaudeLit (Lit c LVar))
+runConversion to = (x, invertMap bindings)
+ where (x, bindings) = runBindT to noBindings `evalFresh` nothingUsed
+
+-- | Run a @BindT MaudeLit (Lit c LVar) Fresh@ computation using the
+-- supplied binding map and the corresponding fresh supply.
+runBackConversion :: BindT MaudeLit (Lit c LVar) Fresh a -- ^ Computation to execute.
+ -> Map MaudeLit (Lit c LVar) -- ^ Binding map that should be used.
+ -> a
+runBackConversion back bindings =
+ evalBindT back bindings `evalFreshAvoiding` M.elems bindings
+
+-- Conversion between Maude and standard substitutions
+------------------------------------------------------------------------
+
+-- | @msubstToLSubstVFresh bindings substMaude@ converts a substitution
+-- returned by Maude to a 'VFresh' substitution. It expects that the
+-- range of the maude substitution contains only fresh variables in its
+-- range and raises an error otherwise.
+msubstToLSubstVFresh :: (Ord c, Show (Lit c LVar), Show c)
+ => Map MaudeLit (Lit c LVar) -- ^ The binding map to use for constants.
+ -> MSubst -- ^ The maude substitution.
+ -> SubstVFresh c LVar
+msubstToLSubstVFresh bindings substMaude
+ | not $ null [i | (_,t) <- substMaude, MaudeVar _ i <- lits t] =
+ error $ "msubstToLSubstVFresh: nonfresh variables in `"++show substMaude++"'"
+ | otherwise = removeRenamings $ substFromListVFresh slist
+ where
+ slist = runBackConversion (traverse translate substMaude) bindings
+ -- try to keep variable name for xi -> xj mappings
+ -- commented out, seems wrong
+ -- translate ((s,i), mt@(Lit (FreshVar _ _))) = do
+ -- lv <- lookupVar s i
+ -- (lv,) <$> mTermToLNTerm (lvarName lv) mt
+ translate ((s,i),mt) = (,) <$> lookupVar s i <*> mTermToLNTerm "x" mt
+ lookupVar s i = do b <- lookupBinding (MaudeVar i s)
+ case b of
+ Just (Var lv) -> return lv
+ _ -> error $ "msubstToLSubstVFrsh: binding for maude variable `"
+ ++show (s,i) ++"' not found in "++show bindings
+
+-- | @msubstToLSubstVFree bindings substMaude@ converts a substitution
+-- returned by Maude to a 'VFree' substitution. It expects that the
+-- maude substitution contains no fresh variables in its range and raises an
+-- error otherwise.
+msubstToLSubstVFree :: (Ord c, Show (Lit c LVar), Show c)
+ => Map MaudeLit (Lit c LVar) -> MSubst -> Subst c LVar
+msubstToLSubstVFree bindings substMaude
+ | not $ null [i | (_,t) <- substMaude, FreshVar _ i <- lits t] =
+ error $ "msubstToLSubstVFree: fresh variables in `"++show substMaude
+ | otherwise = substFromList slist
+ where
+ slist = evalBindT (traverse translate substMaude) bindings
+ `evalFreshAvoiding` M.elems bindings
+ translate ((s,i),mt) = (,) <$> lookupVar s i <*> mTermToLNTerm "x" mt
+ lookupVar s i = do b <- lookupBinding (MaudeVar i s)
+ case b of
+ Just (Var lv) -> return lv
+ _ -> error $ "msubstToLSubstVFree: binding for maude variable `"
+ ++show (s,i)++"' not found in "++show bindings
+
+
+-- Pretty printing of Maude terms.
+------------------------------------------------------------------------
+
+-- | Pretty print an 'LSort'.
+ppMSort :: LSort -> String
+ppMSort LSortPub = "Pub"
+ppMSort LSortFresh = "Fresh"
+ppMSort LSortMsg = "Msg"
+ppMSort LSortNode = "Node"
+ppMSort LSortMSet = "MSet"
+
+-- | Used to prevent clashes with predefined Maude function symbols
+-- like @true@
+funsymPrefix :: String
+funsymPrefix = "tamX"
+
+-- | Pretty print an AC symbol for Maude.
+ppMaudeACSym :: ACSym -> String
+ppMaudeACSym o =
+ funsymPrefix
+ ++ case o of
+ Mult -> "mult"
+ MUn -> "mun"
+ Xor -> "xor"
+
+-- | @ppMaude t@ pretty prints the term @t@ for Maude.
+ppMaude :: Term MaudeLit -> String
+ppMaude (Lit (MaudeVar i lsort)) = "x"++ show i ++":"++ppMSort lsort
+ppMaude (Lit (MaudeConst i LSortFresh)) = "f("++ show i ++")"
+ppMaude (Lit (MaudeConst i LSortPub)) = "p("++ show i ++")"
+ppMaude (Lit (MaudeConst i LSortMsg)) = "c("++ show i ++")"
+ppMaude (Lit (MaudeConst i LSortNode)) = "n("++ show i ++")"
+ppMaude (Lit (MaudeConst i LSortMSet)) = "m("++ show i ++")"
+ppMaude (Lit (FreshVar _ _)) = error "ppMaude: FreshVar not allowed"
+ppMaude (FApp (NonAC (fsym,_)) []) = funsymPrefix++fsym
+ppMaude (FApp (NonAC (fsym,_)) as) =
+ funsymPrefix++fsym++"("++(intercalate "," (map ppMaude as))++")"
+ppMaude (FApp (AC op) as) =
+ ppMaudeACSym op ++ "("++(intercalate "," (map ppMaude as))++")"
+ppMaude (FApp List as) =
+ funsymPrefix++"list(" ++ ppList as ++ ")"
+ where
+ ppList [] = funsymPrefix++"nil"
+ ppList (x:xs) = funsymPrefix++"cons(" ++ ppMaude x ++ "," ++ ppList xs ++ ")"
+
+-- Parser for Maude output
+------------------------------------------------------------------------
+
+-- | @parseSolutions reply@ takes a @reply@ to a unification query
+-- returned by Maude and extracts the unifiers.
+parseMaudeReply :: String -> [Either ParseError MSubst]
+parseMaudeReply reply =
+ case find (\s -> s `elem` ["No unifier.", "No match."]) linesReply of
+ Just _ -> []
+ Nothing -> map parseSolution $ splitOn [""] $
+ dropWhile (\s -> not ("Solution" `isPrefixOf` s)) linesReply
+ where
+ linesReply = lines reply
+
+-- | @parseSolution l@ parses a single solution returned by Maude.
+parseSolution :: [String] -> Either ParseError MSubst
+parseSolution l = parse pSolution "" (unlines l)
+ where
+ pSolution = do
+ string "Solution" <* space
+ many1 digit <* newline
+ (many1 pmap <|> (string "empty substitution" *> newline *> return []))
+ pmap = (,) <$> (flip (,) <$> (char 'x' *> pNat <* string ":") <*> psort)
+ <*> (space *> string "-->" *> space *> expr <* newline)
+
+-- | Parse an 'MSort'.
+psort :: GenParser Char st LSort
+psort = string "Pub" *> return LSortPub
+ <|> string "Fresh" *> return LSortFresh
+ <|> try (string "Msg" *> return LSortMsg)
+ <|> string "MSet" *> return LSortMSet
+ <|> string "Node" *> return LSortNode
+
+
+-- | @expr@ is a parser for Maude Msg expressions.
+-- We parse list, cons and nil as FreeSym. We therefore
+-- have to fixup the term later on.
+expr :: GenParser Char st MTerm
+expr = fixup <$> p
+ where
+ p = Lit <$> ( flip MaudeConst <$> try parseConstSym <*> pNat <* string ")")
+ <|> Lit <$> (MaudeVar <$> (try (string "x" *> pNat <* string ":")) <*> psort)
+ <|> Lit <$> (FreshVar <$> (string "#" *> pNat <* string ":") <*> psort)
+ <|> do op <- try parseACSym
+ args <- sepBy expr commaWS
+ char ')'
+ return $ FApp (AC op) args
+ <|> do fsym <- try (parseFreeSym <* string "(")
+ args <- sepBy expr commaWS
+ string ")"
+ return $ FApp (NonAC (fsym, length args)) args
+ <|> do fsym <- parseFreeSym
+ return $ FApp (NonAC (fsym, 0)) []
+
+ parseConstSym = (string "f(" *> pure LSortFresh)
+ <|> (string "p(" *> pure LSortPub)
+ <|> (string "c(" *> pure LSortMsg)
+ <|> (string "n(" *> pure LSortNode)
+ <|> (string "m(" *> pure LSortMSet)
+
+ parseACSym = try (string (ppMaudeACSym Mult++"(")) *> return Mult
+ <|> try (string (ppMaudeACSym MUn++"(")) *> return MUn
+ <|> (string (ppMaudeACSym Xor++"(")) *> return Xor
+
+ parseFreeSym = string funsymPrefix *> many1 (oneOf (['a' .. 'z']++['A'..'Z']))
+
+ fixup t@(Lit _) = t
+ fixup (FApp (NonAC ("list",1)) [a]) = FApp List (collect a)
+ where
+ collect (FApp (NonAC ("cons",2)) [x,xs]) = fixup x:collect xs
+ collect (FApp (NonAC ("nil",0)) []) = []
+ collect t =
+ error $"MTerm.expr: fixup failed, Maude returned invalid term, "++show t
+ fixup (FApp (NonAC ("list",_)) _) =
+ error "MTerm.expr: fixup failed, Maude returned invalid term, list not unary"
+ fixup (FApp x ts) = FApp x $ map fixup ts
+
+-- | @parseSolution l@ parses a single solution returned by Maude.
+parseReduceSolution :: String -> Either ParseError MTerm
+parseReduceSolution s = case lines s of
+ [_,_,_,res] -> parse pReduceSolution "" res
+ _ -> fail ("parseReduceSolution: invalid Maude output: `" ++ s ++ "'")
+ where
+ pReduceSolution = do
+ string "result" <* space
+ (psort <|> (string "TOP" *> pure LSortPub))
+ -- FIXME: clean up, we use TOP for lists
+ string ":" *> space *> expr
+
+------------------------------------------------------------------------------
+-- Pretty Printing
+------------------------------------------------------------------------------
+
+prettyMaudeSig :: P.HighlightDocument d => MaudeSig -> d
+prettyMaudeSig sig = P.vcat
+ [ ppNonEmptyList' "builtin:" P.text builtIns
+ , ppNonEmptyList' "functions:" ppFunSymb $ funSig sig
+ , ppNonEmptyList
+ (\ds -> P.sep (P.keyword_ "equations:" : map (P.nest 2) ds))
+ prettyStRule $ stRules sig
+ ]
+ where
+ ppNonEmptyList' name = ppNonEmptyList ((P.keyword_ name P.<->) . P.fsep)
+ ppNonEmptyList _ _ [] = P.emptyDoc
+ ppNonEmptyList hdr pp xs = hdr $ P.punctuate P.comma $ map pp xs
+
+ builtIns = asum $ map (\(f, x) -> guard (f sig) *> pure x)
+ [ (enableDH, "diffie-hellman")
+ , (enableXor, "xor")
+ , (enableMSet, "multiset")
+ ]
+
+ ppFunSymb (f,k) = P.text $ f ++ "/" ++ show k
+
+
+-- derived instances
+--------------------
+
+$(derive makeBinary ''MaudeSig)
+$(derive makeNFData ''MaudeSig)
+
+
diff --git a/src/Term/Narrowing/Narrow.hs b/src/Term/Narrowing/Narrow.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Narrowing/Narrow.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE FlexibleInstances #-}
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- One-step narrowing from a term.
+module Term.Narrowing.Narrow (
+ narrowSubsts
+ ) where
+
+import Term.Unification
+import Term.Positions
+
+import Control.Monad.Reader
+
+import Extension.Prelude
+
+import Debug.Trace.Ignore
+
+-- Narrowing
+----------------------------------------------------------------------
+
+-- | @narrowSubsts rules t@ returns all substitutions @s@ such that there is a
+-- narrowing step for the term @t@ and the given rules.
+-- Formally: If there is a step @(t,s(t[r]p),p,s,l->r)@ such that @p@ is a
+-- non-variable position of @t@ and @s@ is an element of the complete set of
+-- unifiers of @t|_p@ with @l@ (wrt. to 'unifyLNTerm') for the rule @l -> r@,
+-- then @s@ is included in the list of returned substitutions.
+narrowSubsts :: LNTerm -> WithMaude [LNSubstVFresh]
+narrowSubsts t = reader $ \hnd -> sortednub $ do
+ let rules0 = rrulesForMaudeSig $ mhMaudeSig hnd
+ (l `RRule` _r) <- renameAvoiding rules0 t
+ p <- positionsNonVar t
+ subst <- unifyLNTerm [Equal (t >* p) l] `runReader` hnd
+ guard (trace ("narrowSubsts"++ (show ((t >* p), l, restrictVFresh (frees t) subst))) True)
+ return $ restrictVFresh (frees t) subst
diff --git a/src/Term/Narrowing/Variants.hs b/src/Term/Narrowing/Variants.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Narrowing/Variants.hs
@@ -0,0 +1,37 @@
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Computing and checking the variants of a term.
+module Term.Narrowing.Variants (
+ computeVariantsCheck
+ , module Term.Narrowing.Variants.Compute
+ , module Term.Narrowing.Variants.Check
+) where
+
+import Term.Narrowing.Variants.Compute
+import Term.Narrowing.Variants.Check
+import Term.Unification
+
+import Control.Monad.Reader
+
+-- | @variantsListCheck ts@ computes all variants of @ts@ considered as a single term
+-- without a bound or symmetry substitution. Before returning the result, it checks
+-- if the set of variants is complete and minimal. If that is not the case, it
+-- fails with an error
+computeVariantsCheck :: LNTerm -> WithMaude [LNSubstVFresh]
+computeVariantsCheck t =
+ reader checkWithMaude
+ where
+ checkWithMaude hnd
+ | not $ run $ checkComplete t vars
+ = error $ "computeVariantsCheck: variant computation for "++ show t ++" failed. Computed set not complete."
+ | not $ run $ checkMinimal t vars
+ = error $ "computeVariantsCheck: variant computation for "++ show t ++" failed. Computed set not minimal."
+ | otherwise
+ = vars
+ where
+ vars = run $ computeVariants t
+ run = (`runReader` hnd)
diff --git a/src/Term/Narrowing/Variants/Check.hs b/src/Term/Narrowing/Variants/Check.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Narrowing/Variants/Check.hs
@@ -0,0 +1,108 @@
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Completeness and minimality checking for the variants of a term.
+module Term.Narrowing.Variants.Check (
+ checkComplete
+ , checkMinimal
+
+ , variantsFrom
+ , isNormalInstance
+
+ , leqSubstVariant
+) where
+
+import Term.Substitution
+import Term.Unification
+import Term.Rewriting.Norm
+import Term.Subsumption ( factorSubstVia, canonizeSubst )
+import Term.Narrowing.Narrow
+
+import Extension.Prelude
+import Utils.Misc
+
+import Control.Basics
+import Control.Monad.Reader
+import Data.List
+
+import Debug.Trace.Ignore
+
+-- Variant Order
+----------------------------------------------------------------------
+
+-- | @isNormalInstance t s s'@ returns @True@ if @s'(norm(s(t)))@ is in normal
+-- form.
+isNormalInstance :: LNTerm -> LNSubst -> LNSubst -> WithMaude Bool
+isNormalInstance t s s' = {- trace ("isnormalInstance " ++ show (t,s,s')) $ -}
+ do t' <- norm' (applyVTerm s t)
+ nf' (applyVTerm s' t')
+
+-- | @leqSubstVariant t s1 s2@ compares two substitutions using the variant order
+-- with respect to @t@ and returns @True@ if @s1@ is less or equal than @s2@
+-- and @False@ otherwise. Use the more expensive @compareSubstVariant@
+-- which uses two AC matchings instead of one if you also want to distinguish
+-- @Nothing@, @Just EQ@, and @Just GT@.
+--
+-- s1 is smaller or equal to s2 wrt. to the variant order (less general) iff there
+-- is an s1' such that s1 = s2' . s2 restricted to vars(t) and s2'(norm(s2(t)))
+-- is in normal form, or equivalently norm(s1(t)) =AC= s2'(norm(s2(1))). This
+-- means s1 is redundant since it is just an AC instance of s2 that does
+-- not "require additional normalization steps."
+leqSubstVariant :: LNTerm -> LNSubstVFresh -> LNSubstVFresh -> WithMaude Bool
+leqSubstVariant t s1_0 s2_0 = reader $ \hnd ->
+ s1_0 == s2_0 ||
+ any (\s -> isNormalInstance t s2 s `runReader` hnd)
+ ( {- (\x -> trace (show x) x) -} (factorSubstVia tvars s1 s2 `runReader` hnd))
+ where
+ tvars = frees t
+ s1 = restrictVFresh tvars s1_0 `freshToFreeAvoiding` t
+ s2 = restrictVFresh tvars s2_0 `freshToFreeAvoiding` t
+
+-- Completeness checking for a set of variants
+----------------------------------------------------------------------
+
+-- | @checkComplete t substs@ checks if @substs@ is a complete set of variants
+-- for @t@ and returns @Just (subst1,subst2)@ if there is a narrowing step
+-- from @subst1@ that yields a new variant @subst2@.
+checkComplete :: LNTerm
+ -> [LNSubstVFresh]
+ -> WithMaude Bool
+checkComplete t substs0 = reader $ \hnd ->
+ let newSubsts = concatMap ((`runReader` hnd) . variantsFrom t) substs
+ substs = sortOn (size &&& length . varsRangeVFresh) substs0
+ in
+ emptySubstVFresh `elem` substs0 &&
+ all (\s -> not $ isMaximalIn s substs t `runReader` hnd) newSubsts
+
+-- | @variantsFrom rules t subst@ returns all the "one-step variants" of
+-- @norm (t subst)@ for the given set of @rules@.
+variantsFrom :: LNTerm
+ -> LNSubstVFresh
+ -> WithMaude [LNSubstVFresh]
+variantsFrom t substFrom0 = reader $ \hnd -> (\res -> trace (show ("variantsFrom", t, substFrom0, res)) res) $ sortednub $ do
+ let substFrom = substFrom0 `freshToFreeAvoiding` t
+ substTo0 <- (narrowSubsts =<< (norm' (applyVTerm substFrom t))) `runReader` hnd
+ let substTo = restrictVFresh (frees t) $ composeVFresh substTo0 substFrom
+ guard (nfSubstVFresh' substTo `runReader` hnd) -- prune substitutions that are not in normal-form
+ return $ canonizeSubst $ removeRenamings $ substTo
+
+-- | @isMaximalIn s substs t@ returns @True@ if @s@ is minimal in substs wrt.
+-- <_Var^t, i.e., the function returns @True@ if there is no s'
+-- in substs with s' <=_Var^t s.
+isMaximalIn :: LNSubstVFresh -> [LNSubstVFresh] -> LNTerm -> WithMaude Bool
+isMaximalIn s substs t = reader $ \hnd ->
+ all (\s' -> (\res -> trace (show ("isMaximal:", not res , "=", s, "<=", s')) res ) $not (leqSubstVariant t s s' `runReader` hnd)) substs
+
+-- Minimality checking for a set of variants
+----------------------------------------------------------------------
+
+-- | @checkMinimal t substs@ checks if @substs@ is a minimal set of variants
+-- for @t@ and returns @False@ if there are subst1 /= subst2 in substs with
+-- subst1 <=_Var_t subst2.
+checkMinimal :: LNTerm -> [LNSubstVFresh] -> WithMaude Bool
+checkMinimal t substs = reader $ \hnd ->
+ noDuplicates substs &&
+ all (\s -> (\res -> trace (show (s,substs,res)) res) $ (`runReader` hnd) $ isMaximalIn s (delete s substs) t) substs
diff --git a/src/Term/Narrowing/Variants/Compute.hs b/src/Term/Narrowing/Variants/Compute.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Narrowing/Variants/Compute.hs
@@ -0,0 +1,149 @@
+{-# LANGUAGE FlexibleInstances #-}
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Computing the variants of a term.
+module Term.Narrowing.Variants.Compute (
+ computeVariantsBound
+ , computeVariants
+
+ -- * for testing
+ , compareSubstVariant
+) where
+
+import Term.LTerm
+import Term.Substitution
+import Term.Unification
+import Term.Narrowing.Variants.Check (leqSubstVariant, variantsFrom)
+
+import Extension.Prelude
+
+import Data.Ord
+import Data.List
+import Data.Maybe
+import Control.Arrow
+import Control.Applicative
+import Control.Monad.Reader
+
+import Debug.Trace.Ignore
+
+----------------------------------------------------------------------
+-- Variant Narrowing
+----------------------------------------------------------------------
+
+-- | @substCompareVariant t s1 t2@ compares two substitutions using the variant order
+-- with respect to @t@.
+compareSubstVariant :: LNTerm -> LNSubstVFresh -> LNSubstVFresh
+ -> WithMaude (Maybe Ordering)
+compareSubstVariant t s1 s2
+ | s1 == s2 = return $ Just EQ
+ | otherwise = do
+ isSmaller <- leqSubstVariant t s1 s2
+ isGreater <- leqSubstVariant t s2 s1
+ return $ case (isSmaller, isGreater) of
+ (True, True) -> Just EQ
+ (True, False) -> Just LT
+ (False, True) -> Just GT
+ (False, False) -> Nothing
+
+-- | A @Variant@ consists of its position in the narrowing tree and
+-- its substitution.
+data Variant = Variant {
+ varPos :: [Int] -- ^ the position in the search tree
+ , varSubst :: LNSubstVFresh -- ^ the composed substitution
+ }
+ deriving (Eq, Ord, Show)
+
+instance Sized Variant where
+ size = size . varSubst
+
+-- | @narrowVariant rules t maxdepth@ either returns @Left (explored, unexplored)@
+-- if variant narrrowing hit the bound and there are still unexplored steps
+-- or @Right (stepnum, explored)@ if the search finished before hitting the
+-- bound.
+narrowVariant :: LNTerm -- ^ The term.
+ -> Maybe Int -- ^ The step bound.
+ -> WithMaude (Either ([Variant], [Variant]) (Int, [Variant]))
+narrowVariant tstart maxdepth0 =
+ reader $ \hnd -> go maxdepth [ Variant [] emptySubstVFresh ] [] hnd
+ where
+ maxdepth = fromMaybe (-1) maxdepth0
+ go :: Int -> [Variant] -> [Variant] -> MaudeHandle
+ -> Either ([Variant], [Variant]) (Int, [Variant])
+ go n [] explored _ = Right (maxdepth-n, explored)
+ go 0 unexplored explored _ = Left (explored, unexplored)
+ go n unexplored explored hnd = (\res -> (trace (show (n,unexplored, explored, res)) res)) $
+ go (n-1) new explored' hnd
+ where
+ runWithMaude = (`runReader` hnd)
+ explored0 = explored++unexplored
+ new0 = filter (\newVariant -> varSubst newVariant `notElem` map varSubst explored0)
+ $ concatMap variantsFrom' unexplored
+ variants = reverse $ sortOn narrowSeqStepComplexity $ (tag False new0 ++ tag True explored0)
+ minimized = filterMaximalBy fst cmp variants
+ tag t xs = [ (t,a) | a <- xs]
+ (explored',new) = map snd *** map snd $ partition fst minimized
+ cmp a b = runWithMaude $ compareSubstVariant tstart (varSubst.snd $ a) (varSubst.snd $ b)
+
+ variantsFrom' (Variant pos0 substComposed) =
+ zipWith (\i substComposed' -> Variant (pos0++[i]) substComposed')
+ [1..]
+ (runWithMaude $ variantsFrom tstart substComposed)
+
+-- | @filterMaximalBy flags fastcmp alreadyFiltered cmp xs@ returns a
+-- list of maximal elements of @xs@ with respect to @cmp@.
+filterMaximalBy :: Eq a
+ => (a -> Bool) -- ^ a function to check if an element has been
+ -- already filtered in the last iteration
+ -> (a -> a -> Maybe Ordering) -- ^ the comparison function
+ -> [a] -- ^ the list that we want to filter
+ -> [a]
+filterMaximalBy _ _ [] = []
+filterMaximalBy alreadyFiltered cmp xs0 =
+ go (last xs0) (init xs0,[])
+ where
+ go x ([],[]) = [x]
+ go x (y:todo,done)
+ -- x and y have already been filtered earlier and are therefore incomparable
+ | alreadyFiltered x && alreadyFiltered y = go x (todo,y:done)
+ -- either x or y is new, so we have to comparison the two
+ | otherwise
+ = case cmp x y of
+ Nothing -> go x (todo,y:done)
+ Just EQ | alreadyFiltered x -> keepx
+ | otherwise -> keepy
+ Just GT -> keepx
+ Just LT -> keepy
+ where keepx = go x (todo,done)
+ keepy = go y (todo++done,[])
+ -- x is maximal, start comparing a new element to the others
+ go x ([],y:done) = x:(go y (reverse done,[]))
+
+
+-- | This is used to sort narrowing steps such that similar steps are close
+narrowSeqStepComplexity :: (Bool,Variant) -> (Bool,Int,Int,Int)
+narrowSeqStepComplexity (checked, var@(Variant _ subst)) =
+ (not checked, length (varPos var), size subst, length (varsRangeVFresh subst))
+
+
+-- | @computeVariants t d@ compute the variants of term @t@ with bound @d@.
+-- The rewriting rules are taken from the Maude context.
+computeVariantsBound :: LNTerm -> Maybe Int
+ -> WithMaude (Maybe [LNSubstVFresh])
+computeVariantsBound t d = reader $ \hnd -> (\res -> trace (show ("ComputeVariantsBound", t, res)) res) $
+ case (`runReader` hnd) $ narrowVariant t d of
+ Left _ -> Nothing
+ Right (_,explored) ->
+ Just (map varSubst (sortBy (comparing size) explored))
+
+-- | @variantsList ts@ computes all variants of @ts@ considered as a single term
+-- without a bound or symmetry substitution.
+-- The rewriting rules are taken from the Maude context.
+computeVariants :: LNTerm -> WithMaude [LNSubstVFresh]
+computeVariants t =
+ fromMaybe err <$> computeVariantsBound t Nothing
+ where
+ err = error "impossible: Variant computation failed without giving a bound"
diff --git a/src/Term/Positions.hs b/src/Term/Positions.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Positions.hs
@@ -0,0 +1,43 @@
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Positions and replacement in terms.
+module Term.Positions where
+
+import Term.Term
+import Safe
+
+-- Positions, subterm access, subterm replacement
+----------------------------------------------------------------------
+
+-- | A position in a term is a list of integers.
+type Position = [Int]
+
+-- | @t >* p@ returns the subterm of term @t@ at position @p@.
+-- The standard standard notation for @t >* p@ is @t|_p@.
+(>*) :: Term a -> Position -> Term a
+t >* [] = t
+(FApp _ as) >* (i:ps) = case atMay as i of
+ Nothing -> error "Term.Positions.(>*): invalid position given"
+ Just a -> a >* ps
+(Lit _) >* (_:_) = error "Term.Positions.(>*): invalid position given"
+
+
+-- | @t >=*(s,p)@ returns the term @t'@ where the subterm a position @p@
+-- is replaced by @s@. The standard notation for @t >=*(s,p)@ is @t[s]_p@.
+(>=*) :: Term a -> (Term a, Position) -> Term a
+_ >=* (s,[]) = s
+(FApp fsym as) >=* (s,i:ps) = if 0 <= i && i < length as
+ then FApp fsym ((take i as)++[as!!i >=* (s,ps)]++(drop (i+1) as))
+ else error "Term.Positions.(>=*): invalid position given"
+(Lit _) >=* (_,_:_) = error "Term.Positions.(>=*): invalid position given"
+
+-- | @positionsNonVar t@ returns all the non-variable positions in the term @t@.
+positionsNonVar :: VTerm a b -> [Position]
+positionsNonVar t = go t
+ where go (Lit (Con _)) = [[]]
+ go (Lit (Var _)) = []
+ go (FApp _ as) = []:concat (zipWith (\i a -> map (i:) (go a)) [0..] as)
diff --git a/src/Term/Rewriting/Norm.hs b/src/Term/Rewriting/Norm.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Rewriting/Norm.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE PatternGuards, FlexibleContexts #-}
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- This module implements normalization with respect to DH u AC using class
+-- rewriting and an ad-hoc function that uses the @TermAC@ representation of
+-- terms modulo AC.
+module Term.Rewriting.Norm (
+ norm
+ , norm'
+ , nf
+ , nf'
+ , nfSubstVFresh'
+ , normSubstVFresh'
+) where
+
+import Term.Term
+import Term.LTerm
+import Term.Rewriting.NormAC
+import Term.Substitution
+import Term.Maude.Process
+
+import Control.Basics
+import Control.Monad.Reader
+
+import System.IO.Unsafe (unsafePerformIO)
+
+-- Normalization using Maude
+----------------------------------------------------------------------
+
+-- | @norm t@ normalized the term @t@ using Maude.
+norm :: (Show (Lit c LVar), Ord c, IsConst c)
+ => (c -> LSort) -> VTerm c LVar -> WithMaude (VTerm c LVar)
+norm _ t@(Lit _) = return t
+norm sortOf t = reader $ \hnd -> normAC $ unsafePerformIO $ normViaMaude hnd sortOf t
+
+norm' :: LNTerm -> WithMaude LNTerm
+norm' = norm sortOfName
+
+-- | @nf t@ returns @True@ if the term @t@ is in normal form.
+nf :: (Show (Lit c LVar), Ord c, IsConst c)
+ => (c -> LSort) -> VTerm c LVar -> WithMaude Bool
+nf sortOf t = (t ==#) <$> norm sortOf t
+
+nf' :: LNTerm -> WithMaude Bool
+nf' = nf sortOfName
+
+-- Normalization
+----------------------------------------------------
+
+-- | @nfSubst s@ returns @True@ if the substitution @s@ is in normal form.
+nfSubstVFresh' :: LNSubstVFresh -> WithMaude Bool
+nfSubstVFresh' s = reader $ \hnd -> all (\t -> runReader (nf' t) hnd) (rangeVFresh s)
+
+{-
+-- | @normSubst s@ normalizes the substitution @s@.
+normSubst :: (IsConst c, IsVar v, Show (Lit c v)) => Subst c v -> Subst c v
+normSubst s = mapRange norm s
+
+-}
+
+-- | @normSubst s@ normalizes the substitution @s@.
+normSubstVFresh' :: LNSubstVFresh -> WithMaude LNSubstVFresh
+normSubstVFresh' s = reader $ \hnd -> mapRangeVFresh (\t -> norm' t `runReader` hnd) s
diff --git a/src/Term/Rewriting/NormAC.hs b/src/Term/Rewriting/NormAC.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Rewriting/NormAC.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE PatternGuards, FlexibleContexts #-}
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- This module implements normalization with respect to AC.
+module Term.Rewriting.NormAC (
+ (==#)
+ , termFlatten
+ , normAC
+) where
+
+import Term.Term
+
+import Data.List ( sort )
+
+-- Normalization modulo AC = flatten + sort
+----------------------------------------------------------------------
+
+-- | @termFlatten t@ converts a term @t@ to its flat representation, i.e.,
+-- AC-operator applications are replaced by n-ary, non-nested
+-- AC-operator applications.
+termFlatten :: (Ord a) => Term a -> Term a
+termFlatten t =
+ go t
+ where
+ go (Lit l) = Lit l
+ go (FApp (AC o) as) = FApp (AC o) (concatMap collectOTerms (map go as))
+ where
+ collectOTerms (FApp (AC o') ts) | o == o' = ts
+ collectOTerms a = [a]
+ go (FApp o as) = FApp o (map go as)
+
+-- | @normAC t@ normalizes the term @t@ wrt. to the equations AC,
+-- i.e., by flattening and sorting wrt. Ord.
+normAC :: (Ord t) => Term t -> Term t
+normAC = foldTerm Lit (\o -> FApp o . sortAC o) . termFlatten
+ where
+ sortAC (AC _) as = sort as
+ sortAC _ as = as
+
+-- | @a ==# b@ returns @True@ if @a@ is equal @b@ modulo AC.
+(==#) :: (Ord a) => Term a -> Term a -> Bool
+a ==# b = normAC a == normAC b
+
diff --git a/src/Term/Substitution.hs b/src/Term/Substitution.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Substitution.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE TupleSections, TypeSynonymInstances, GADTs,FlexibleContexts,EmptyDataDecls,StandaloneDeriving, DeriveDataTypeable, FlexibleInstances, MultiParamTypeClasses, DeriveFunctor, ScopedTypeVariables #-}
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Standard and fresh substitutions.
+module Term.Substitution (
+
+ -- ** Composition of fresh and free substitutions
+ composeVFresh
+
+ -- ** Conversion between fresh and free
+ , freshToFree
+ , freshToFreeAvoiding
+
+ , freeToFreshRaw
+
+ -- ** Convenience exports
+ , module Term.LTerm
+ , module Term.Substitution.SubstVFree
+ , module Term.Substitution.SubstVFresh
+) where
+
+import Term.LTerm
+import Term.Substitution.SubstVFree
+import Term.Substitution.SubstVFresh
+
+import Extension.Prelude
+
+import Control.Monad.Bind
+
+import Data.Traversable hiding (mapM)
+import Control.Applicative
+
+
+-- Composition of VFresh and VFresh substitutions
+----------------------------------------------------------------------
+
+-- | @composeVFresh s1 s2@ composes the fresh substitution s1 and the free substitution s2.
+-- The result is the fresh substitution s = s1.s2.
+composeVFresh :: (IsConst c, Show (Lit c LVar))
+ => SubstVFresh c LVar -> Subst c LVar -> SubstVFresh c LVar
+composeVFresh s1_0 s2 =
+ freeToFreshRaw (s1 `compose` s2)
+ where
+ s1 = freshToFreeAvoiding (extendWithRenaming (varsRange s2) s1_0) (s2,s1_0)
+
+-- Conversion between substitutions
+----------------------------------------------------------------------
+
+-- | @freshToFreeSimp s@ converts the bound variables in @s@ to free variables
+-- using fresh variable names. We try to preserve variables names if possible.
+freshToFree :: (MonadFresh m, IsConst c)
+ => SubstVFresh c LVar -> m (Subst c LVar)
+freshToFree subst = (`evalBindT` noBindings) $ do
+ let slist = sortOn (size . snd) $ substToListVFresh subst
+ -- import oldvar ~> newvar mappings first, keep namehint from oldvar
+ substFromList <$> mapM convertMapping slist
+ where
+ convertMapping (lv,t) = (lv,) <$> traverse importLit t
+ where
+ importLit (Con c) = return (Con c)
+ importLit (Var v) =
+ Var <$> importBinding (\s i -> LVar s (lvarSort v) i) v (namehint v)
+ namehint v = case t of
+ Lit (Var _) -> lvarName lv -- keep name of oldvar
+ _ -> lvarName v
+
+-- | @freshToFreeSimpAvoiding s t@ converts all fresh variables in the range of
+-- @s@ to free variables avoiding free variables in @t@.
+freshToFreeAvoiding :: (HasFrees t, IsConst c) => SubstVFresh c LVar -> t -> Subst c LVar
+freshToFreeAvoiding s t = freshToFree s `evalFreshAvoiding` t
+
+-- | @freeToFreshRaw s@ considers all variables in the range of @s@ as fresh.
+freeToFreshRaw :: Subst c LVar -> SubstVFresh c LVar
+freeToFreshRaw s@(Subst _) = substFromListVFresh $ substToList s
diff --git a/src/Term/Substitution/SubstVFree.hs b/src/Term/Substitution/SubstVFree.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Substitution/SubstVFree.hs
@@ -0,0 +1,266 @@
+{-# LANGUAGE TupleSections, GeneralizedNewtypeDeriving, TypeSynonymInstances, GADTs,FlexibleContexts,EmptyDataDecls,StandaloneDeriving, DeriveDataTypeable, FlexibleInstances, MultiParamTypeClasses, DeriveFunctor, ScopedTypeVariables #-}
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Standard substitutions (with free variables).
+module Term.Substitution.SubstVFree (
+ -- * General Substitutions
+ Subst(..)
+
+ -- * application of substitutions
+ , applyVTerm
+ , applyLit
+
+ -- * smart constructors for substitutions
+ , substFromList
+ , substFromMap
+ , emptySubst
+
+ -- * Composition of substitutions
+ , compose
+ , applySubst
+
+ -- * operations
+ , restrict
+ , mapRange
+
+ -- * queries
+ , varsRange
+ , dom
+ , range
+ , imageOf
+
+ -- * views
+ , substToListOn
+ , substToList
+
+ -- *
+ , Apply(..)
+
+ -- * Pretty printing
+ , prettySubst
+
+ -- * Substitution of LVars
+ , LSubst
+ , LNSubst
+ , prettyLNSubst
+) where
+
+
+import Term.LTerm
+import Term.Rewriting.NormAC
+import Text.PrettyPrint.Highlight
+import Logic.Connectives
+
+import Extension.Prelude
+import Utils.Misc
+
+import Data.Maybe
+import Data.Map ( Map )
+import qualified Data.Map as M
+import qualified Data.Set as S
+import Data.List
+import Data.Binary
+
+import Control.Applicative
+import Control.DeepSeq
+
+----------------------------------------------------------------------
+-- Substitutions
+----------------------------------------------------------------------
+
+-- | We use the data type @Subst c v@ of substitutions. @c@ is the type of constants
+-- and @v@ the type of variables.
+newtype Subst c v = Subst { sMap :: Map v (VTerm c v) }
+ deriving ( Eq, Ord, NFData, Binary )
+
+-- | A substitution for logical variables.
+type LSubst c = Subst c LVar
+
+-- | A substitution with names and logical variables.
+type LNSubst = Subst Name LVar
+
+
+-- Application
+----------------------------------------------------------------------
+
+-- | @applyLit subst l@ applies the substitution @subst@ to the literal @l@.
+applyLit :: IsVar v => Subst c v -> Lit c v -> VTerm c v
+applyLit subst v@(Var i) = fromMaybe (Lit v) $ M.lookup i (sMap subst)
+applyLit _ c@(Con _) = Lit c
+
+
+
+-- | @applyTermVFree subst t@ applies the substitution @subst@ to the term @t@.
+applyVTerm :: (IsConst c, IsVar v) => Subst c v -> VTerm c v -> VTerm c v
+applyVTerm subst = (>>= applyLit subst)
+
+
+-- Construction
+----------------------------------------------------------------------
+
+-- | Convert a list to a substitution. The @x/x@ mappings are removed.
+substFromList :: IsVar v => [(v, VTerm c v)] -> Subst c v
+substFromList xs =
+ Subst (M.fromList [ (v,t) | (v,t) <- xs, not (t `equalToVar` v) ])
+ where
+ equalToVar (Lit (Var v')) v = v == v'
+ equalToVar _ _ = False
+
+-- | Convert a map to a substitution. The @x/x@ mappings are removed.
+-- FIXME: implement directly, use substFromMap for substFromList.
+substFromMap :: IsVar v => Map v (VTerm c v) -> Subst c v
+substFromMap = substFromList . M.toList
+
+-- | @emptySubVFree@ is the substitution with empty domain.
+emptySubst :: Subst c v
+emptySubst = Subst M.empty
+
+-- Composition
+----------------------------------------------------------------------
+
+-- | @applySubst subst subst'@ applies the substitution @subst@ to the range of
+-- the substitution @subst'@.
+applySubst :: (IsConst c, IsVar v)
+ => Subst c v -> Subst c v -> Subst c v
+applySubst subst subst' = mapRange (applyVTerm subst) subst'
+
+-- | @compose s1 s2@ composes the substitutions s1 and s2. The result is
+-- @s1.s2@, i.e., it has the same effect as @(t s2) s1 = s1(s2(t))@
+-- when applied to a term @t@.
+compose :: (IsConst c, IsVar v)
+ => Subst c v -> Subst c v -> Subst c v
+compose s1 s2 =
+ Subst $
+ sMap (applySubst s1 s2) `M.union` sMap (restrict (dom s1 \\ dom s2) s1)
+
+-- Operations
+----------------------------------------------------------------------
+
+-- | @restrict vars subst@ restricts the domain of the substitution @subst@ to @vars@.
+restrict :: IsVar v => [v] -> Subst c v -> Subst c v
+restrict vs (Subst smap) = Subst (M.filterWithKey (\v _ -> v `elem` vs) smap)
+
+-- | @mapRange f subst@ maps the function @f@ over the range of the substitution @subst@.
+mapRange :: (IsConst c, IsVar v, IsConst c2)
+ => (VTerm c v -> VTerm c2 v)
+ -> Subst c v -> Subst c2 v
+mapRange f subst@(Subst _) =
+ Subst $ M.mapMaybeWithKey (\i t -> filterRefl i (f t)) (sMap subst)
+ where
+ filterRefl i (Lit (Var j)) | i == j = Nothing
+ filterRefl _ t = Just t
+
+
+-- Queries
+----------------------------------------------------------------------
+
+-- | @dom subst@ returns the domain of the substitution @substs@.
+dom :: Subst c v -> [v]
+dom = M.keys . sMap
+
+-- | @range subst@ returns the range of the substitution @substs@.
+range :: Subst c v -> [VTerm c v]
+range = M.elems . sMap
+
+-- | @varsRange subst@ returns all variables in the range of the substitution
+-- FIXME: use Monoid, dlist, write occurs function.
+varsRange :: IsVar v => Subst c v -> [v]
+varsRange = sortednub . concatMap varsVTerm . range
+
+-- Views
+----------------------------------------------------------------------
+
+-- | Convert substitution to list.
+substToList :: Subst c v -> [(v,VTerm c v)]
+substToList = M.toList . sMap
+
+-- | @substToPairOn vs sigma@ converts the list of variables @[x1,..,xk]@ to
+-- @[sigma(x1),..,sigma(xk)]@.
+substToListOn :: (IsConst c, IsVar v) => [v] -> Subst c v -> [VTerm c v]
+substToListOn vs subst = map (applyLit subst) (map Var vs)
+
+-- | Returns the image of @i@ under @subst@ if @i@ is in the domain of @subst@.
+imageOf :: IsVar v => Subst c v -> v -> Maybe (VTerm c v)
+imageOf subst i = M.lookup i (sMap subst)
+
+----------------------------------------------------------------------
+-- Boilerplate instances
+----------------------------------------------------------------------
+
+instance (Show v, Show c) => Show (Subst c v) where
+ show subst@(Subst _) = "{" ++ mappings ++"}"
+ where
+ mappings =
+ intercalate ", " [ show t ++" <~ "++show v | (v,t) <- substToList subst ]
+
+instance Sized (Subst c v) where
+ size = sum . map size . range
+
+-- Instances
+------------
+
+instance HasFrees (LSubst c) where
+ foldFrees f = foldFrees f . sMap
+ mapFrees f = (substFromList <$>) . mapFrees f . substToList
+
+-- | Types that support the application of 'LSubst's.
+class Apply t where
+ apply :: LNSubst -> t -> t
+
+instance Apply LVar where
+ apply subst x = maybe x extractVar $ imageOf subst x
+ where
+ extractVar (Lit (Var x')) = x'
+ extractVar t =
+ error $ "apply (LVar): variable '" ++ show x ++
+ "' substituted with term '" ++ show t ++ "'"
+
+instance Apply LNTerm where
+ apply subst = normAC . applyVTerm subst
+
+instance Apply () where
+ apply _ = id
+
+instance Apply Char where
+ apply _ = id
+
+instance Apply Int where
+ apply _ = id
+
+instance Apply a => Apply [a] where
+ apply subst = fmap (apply subst)
+
+instance Apply a => Apply (Conj a) where
+ apply subst = fmap (apply subst)
+
+instance Apply a => Apply (Disj a) where
+ apply subst = fmap (apply subst)
+
+instance (Ord a, Apply a) => Apply (S.Set a) where
+ apply subst = S.map (apply subst)
+
+instance Apply t => Apply (Equal t) where
+ apply subst = fmap (apply subst)
+
+
+----------------------------------------------------------------------
+-- Pretty Printing
+----------------------------------------------------------------------
+
+-- | Pretty print a substitution.
+prettySubst :: (Ord c, Ord v, HighlightDocument d)
+ => (v -> d) -> (Lit c v -> d) -> Subst c v -> [d]
+prettySubst ppVar ppLit =
+ map pp . M.toList . equivClasses . substToList
+ where
+ pp (t, vs) = prettyTerm ppLit t <-> operator_ " <~ {" <>
+ (fsep $ punctuate comma $ map ppVar $ S.toList vs) <> operator_ "}"
+
+-- | Pretty print a substitution with logical variables.
+prettyLNSubst :: (Show (Lit c LVar), Ord c, HighlightDocument d)
+ => LSubst c -> d
+prettyLNSubst = vcat . prettySubst (text . show) (text . show)
diff --git a/src/Term/Substitution/SubstVFresh.hs b/src/Term/Substitution/SubstVFresh.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Substitution/SubstVFresh.hs
@@ -0,0 +1,245 @@
+{-# LANGUAGE TupleSections
+ , TypeSynonymInstances
+ , GADTs
+ , FlexibleContexts
+ , EmptyDataDecls
+ , StandaloneDeriving
+ , DeriveDataTypeable
+ , FlexibleInstances
+ , MultiParamTypeClasses
+ , GeneralizedNewtypeDeriving
+ , ScopedTypeVariables
+ #-}
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Substitutions with fresh (or bound) variables in the range.
+module Term.Substitution.SubstVFresh (
+ -- * General Substitutions
+ SubstVFresh(..)
+
+ -- * smart constructors for substitutions
+ , substFromListVFresh
+ , emptySubstVFresh
+
+ -- * operations
+ , restrictVFresh
+ , mapRangeVFresh
+ , extendWithRenaming
+
+ -- * queries
+ , varsRangeVFresh
+ , domVFresh
+ , rangeVFresh
+ , isRenaming
+ , imageOfVFresh
+
+ -- * views
+ , substToListVFresh
+
+
+ -- * Pretty printing
+ , prettySubstVFresh
+
+ -- * operations on fresh substitutions
+ , renameFresh
+ , renameFreshAvoiding
+ , removeRenamings
+
+ -- * Substitution of LVars
+ , LSubstVFresh
+ , LNSubstVFresh
+ , prettyLSubstVFresh
+ , prettyDisjLNSubstsVFresh
+) where
+
+
+import Term.LTerm
+import Text.Isar (numbered')
+import Text.PrettyPrint.Highlight
+
+import Control.Applicative
+import Control.Monad.Fresh
+import Control.DeepSeq
+
+import Extension.Prelude
+
+import Logic.Connectives
+
+import Utils.Misc
+
+import Data.Maybe
+import Data.Map ( Map )
+import qualified Data.Map as M
+import qualified Data.Set as S
+import Data.List
+import Data.Traversable hiding ( mapM )
+import Data.Binary
+
+----------------------------------------------------------------------
+-- Substitutions
+----------------------------------------------------------------------
+
+-- | We use the data type @SubstVFresh c v@ of substitutions.
+-- @c@ denotes the type of constants and @v@ the type of variables.
+-- Fresh substitutions cannot be applied directly, they have to be converted
+-- to free substitutions in a certain context (MonadFresh).
+newtype SubstVFresh c v = SubstVFresh { svMap :: Map v (VTerm c v) }
+ deriving ( Eq, Ord, NFData, Binary )
+
+-- | Fresh substitution with logical variables
+type LSubstVFresh c = SubstVFresh c LVar
+
+-- | Fresh substitution with logical variables and names
+type LNSubstVFresh = SubstVFresh Name LVar
+
+-- Instances
+------------
+
+-- Smart constructors for substitutions
+----------------------------------------------------------------------
+
+-- | Convert a list of mappings to a fresh substitution.
+substFromListVFresh :: IsVar v => [(v, VTerm c v)] -> SubstVFresh c v
+substFromListVFresh xs = SubstVFresh (M.fromList xs)
+
+-- | @emptySubstVFresh@ is the fresh substitution with empty domain.
+emptySubstVFresh :: SubstVFresh c v
+emptySubstVFresh = SubstVFresh M.empty
+
+
+-- Operations
+----------------------------------------------------------------------
+
+-- | @restrictVFresh vars subst@ restricts the domain of the substitution @subst@ to @vars@.
+restrictVFresh :: IsVar v => [v] -> SubstVFresh c v -> SubstVFresh c v
+restrictVFresh vs (SubstVFresh smap) = SubstVFresh (M.filterWithKey (\v _ -> v `elem` vs) smap)
+
+-- | @mapRangeVFresh f subst@ maps the function @f@ over the range of the substitution @subst@.
+-- Note that all introduced variables are considered fresh.
+mapRangeVFresh :: (IsConst c, IsVar v, IsConst c2)
+ => (VTerm c v -> VTerm c2 v)
+ -> SubstVFresh c v -> SubstVFresh c2 v
+mapRangeVFresh f subst = SubstVFresh $ M.map f (svMap subst)
+
+
+-- | @extendWithRenaming vs s@ extends the substitution @s@ with renamings (with
+-- fresh variables) for the variables in @vs@ that are not already in @dom s@.
+extendWithRenaming :: Show (Lit c LVar)
+ => [LVar] -> SubstVFresh c LVar -> SubstVFresh c LVar
+extendWithRenaming vs0 s =
+ substFromListVFresh $
+ substToListVFresh s ++ substToListVFresh (renameFreshAvoiding s2 (varsRangeVFresh s))
+ where s2 = substFromListVFresh [(v, Lit (Var v)) | v <- vs ]
+ vs = vs0 \\ domVFresh s
+
+
+-- Queries
+----------------------------------------------------------------------
+
+-- | @domVFresh subst@ returns the domain of the substitution @substs@.
+domVFresh :: SubstVFresh c v -> [v]
+domVFresh = M.keys . svMap
+
+-- | @rangeVFresh subst@ returns the range of the substitution @substs@.
+rangeVFresh :: SubstVFresh c v -> [VTerm c v]
+rangeVFresh = M.elems . svMap
+
+-- | @varsRangeVFresh subst@ returns all variables in the range of the substitution
+-- FIXME: use Monoid, dlist, write occurs function.
+varsRangeVFresh :: IsVar v => SubstVFresh c v -> [v]
+varsRangeVFresh = sortednub . concatMap varsVTerm . rangeVFresh
+
+-- | Returns @True@ if the given variable in the domain of the
+-- substitution is just renamed by the substitution.
+isRenamedVar :: LVar -> LSubstVFresh c -> Bool
+isRenamedVar lv subst =
+ case imageOfVFresh subst lv of
+ Just (Lit (Var lv')) | lvarSort lv == lvarSort lv' ->
+ lv' `notElem` (concatMap varsVTerm $ [ t | (v,t) <- substToListVFresh subst, v /= lv ])
+ _ -> False
+
+-- | Returns @True@ if the substitution is a renaming.
+isRenaming :: LSubstVFresh c -> Bool
+isRenaming subst = all (`isRenamedVar` subst) $ domVFresh subst
+
+-- | Returns the image of @i@ under @subst@ if @i@ is in the domain of @subst@.
+imageOfVFresh :: IsVar v => SubstVFresh c v -> v -> Maybe (VTerm c v)
+imageOfVFresh subst i = M.lookup i (svMap subst)
+
+-- Views
+----------------------------------------------------------------------
+
+-- | Convert substitution to list.
+substToListVFresh :: SubstVFresh c v -> [(v,VTerm c v)]
+substToListVFresh = M.toList . svMap
+
+-- Operations on fresh substitutions
+----------------------------------------------------------------------
+
+-- | @renameFresh s@ renames the fresh variables in @s@ using fresh variables.
+-- This function can be used to prevent overshadowing which might
+-- make output hard to read.
+renameFresh :: MonadFresh m => SubstVFresh c LVar -> m (SubstVFresh c LVar)
+renameFresh subst = substFromListVFresh . zip (map fst slist) <$> rename (map snd slist)
+ where slist = substToListVFresh subst
+
+-- | @renameFreshAvoiding s t@ renames the fresh variables in the range of @s@ away from
+-- variables that are free in @t@. This is an internal function.
+renameFreshAvoiding :: HasFrees t => LSubstVFresh c -> t -> SubstVFresh c LVar
+renameFreshAvoiding s t = renameFresh s `evalFreshAvoiding` t
+
+-- | @removeRenamings s@ removes all renamings (see 'isRenamedVar') from @s@.
+removeRenamings :: LSubstVFresh c -> LSubstVFresh c
+removeRenamings s =
+ substFromListVFresh $ filter (not . (`isRenamedVar` s) . fst) $ substToListVFresh s
+
+----------------------------------------------------------------------
+-- Instances
+----------------------------------------------------------------------
+
+instance (Show c, Show v) => Show (SubstVFresh c v) where
+ show subst = "VFresh: {" ++ mappings ++"}"
+ where
+ mappings = intercalate ", " [ show t ++" <~ "++show v | (v,t) <- substToListVFresh subst ]
+
+
+instance Sized (SubstVFresh c v) where
+ size = sum . map size . rangeVFresh
+
+
+instance HasFrees (SubstVFresh n LVar) where
+ foldFrees f = foldFrees f . M.keys . svMap
+ mapFrees f =
+ (substFromListVFresh <$>) . traverse mapDomain . substToListVFresh
+ where
+ mapDomain (v, t) = (,t) <$> mapFrees f v
+
+----------------------------------------------------------------------
+-- Pretty Printing
+----------------------------------------------------------------------
+
+-- | Pretty print a substitution.
+prettySubstVFresh :: (Ord c, Ord v, HighlightDocument d)
+ => (v -> d) -> (Lit c v -> d) -> SubstVFresh c v -> [d]
+prettySubstVFresh ppVar ppLit =
+ map pp . M.toList . equivClasses . substToListVFresh
+ where
+ pp (t, vs) = prettyTerm ppLit t <-> operator_ " <~ {" <>
+ (fsep $ punctuate comma $ map ppVar $ S.toList vs) <> operator_ "}"
+
+-- | Pretty print a substitution with logical variables.
+prettyLSubstVFresh :: (Show (Lit c LVar), Ord c, HighlightDocument d) => LSubstVFresh c -> d
+prettyLSubstVFresh = vcat . prettySubstVFresh (text . show) (text . show)
+
+-- | Pretty print a disjunction of substitutions.
+prettyDisjLNSubstsVFresh :: Document d => Disj LNSubstVFresh -> d
+prettyDisjLNSubstsVFresh (Disj substs) =
+ numbered' (map ppConj substs)
+ where
+ ppConj = vcat . map prettyEq . substToListVFresh
+ prettyEq (a,b) =
+ prettyNTerm (Lit (Var a)) $$ nest (6::Int) (text "=" <-> prettyNTerm b)
diff --git a/src/Term/Subsumption.hs b/src/Term/Subsumption.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Subsumption.hs
@@ -0,0 +1,112 @@
+{-# LANGUAGE GADTs, FlexibleContexts #-}
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Subsumption of terms and substitutions.
+module Term.Subsumption (
+ compareTermSubs
+ , eqTermSubs
+
+ , factorSubstVia
+-- , factorSubstOnVFresh
+
+ -- * canonical representations for substitutions
+ -- modulo renaming
+ , canonizeSubst
+
+ -- * for testing only
+ , varOccurences
+) where
+
+import Term.Term
+import Term.LTerm
+import Term.Unification
+import Term.Rewriting.NormAC
+import Term.Positions
+
+import Extension.Prelude
+-- import Utils.Misc
+
+import Data.List
+import Data.Ord
+import Data.Maybe
+import Control.Basics
+
+----------------------------------------------------------------------
+-- Subsumption order on terms and substitutions
+----------------------------------------------------------------------
+
+-- | Compare terms @t1@ and @t2@ with respect to the subsumption order modulo AC.
+compareTermSubs :: LNTerm -> LNTerm -> WithMaude (Maybe Ordering)
+compareTermSubs t1 t2 = do
+ check <$> matchLNTerm [t1 `MatchWith` t2] <*> matchLNTerm [t2 `MatchWith` t1]
+ where
+ check [] [] = Nothing
+ check (_:_) [] = Just GT
+ check [] (_:_) = Just LT
+ check (_:_) (_:_) = Just EQ
+
+-- | Returns True if @s1@ and @s2@ are equal with respect to the subsumption order modulo AC.
+eqTermSubs :: LNTerm -> LNTerm -> WithMaude Bool
+eqTermSubs s1 s2 = (== Just EQ) <$> compareTermSubs s1 s2
+
+-- | @factorSubstOn s1 s2 vs@ factors the free substitution @s1@
+-- through free substitution @s2@ on @vs@,
+-- i.e., find a complete set of free substitutions s such that for all
+-- vars @x `elem` vs@:
+-- > applyVTerm s1 x =AC= applyVTerm s (applyVTerm s2 x).
+factorSubstVia :: [LVar] -> LNSubst -> LNSubst -> WithMaude [LNSubst]
+factorSubstVia vs s1 s2 =
+ matchLNTerm (zipWith MatchWith (substToListOn vs s1) (substToListOn vs s2))
+
+{-
+-- | @factorSubstOnVFresh s1 s2 vs@ factors the fresh substitution @s1@
+-- through the free substitution @s2@ on @vs@,
+-- i.e., it returns a complete set of fresh substitutions s such that
+-- s1 is equivalent to s.s2 modulo renaming.
+factorSubstViaVFresh :: [LVar] -> LNSubstVFresh -> LNSubst
+ -> WithMaude [LNSubstVFresh]
+factorSubstViaVFresh vs s1_0 s2 = do
+ matchers <- matchLNTerm (zipWith MatchWith l1 l2)
+ return $ do
+ s <- matchers
+ when (not $ varsRange s `subsetOf` varsRange s1) $
+ error $ "factorSubstOnVFresh " ++ show s1 ++ " " ++ show s2
+ ++ " => " ++ show s ++ " contains new variables"
+ return $ freeToFreshRaw s
+ where
+ s1 = freshToFreeAvoiding s1_0 (vs, varsRange s2)
+ l1 = substToListOn vs s1
+ l2 = substToListOn vs s2
+-}
+
+----------------------------------------------------------------------
+-- Equality of substitutions modulo AC and renaming
+----------------------------------------------------------------------
+
+-- | Returns a substitution that is equivalent modulo renaming to the given substitution.
+canonizeSubst :: LNSubstVFresh -> LNSubstVFresh
+canonizeSubst subst =
+ mapRangeVFresh (normAC . applyVTerm renaming) subst
+ where
+ vrangeSorted = sortOn (varOccurences subst) (varsRangeVFresh subst)
+ renaming = substFromList $
+ zipWith (\lv i -> (lv, varTerm $ LVar "x" (lvarSort lv) i))
+ vrangeSorted [1..]
+
+-- | @varOccurences v t@ returns a sorted list of positions where the
+-- variable @v@ occurs in @t@. The function returns the same result for
+-- terms that are equal modulo AC since the flattened term representation
+-- is used.
+varOccurences :: LNSubstVFresh -> LVar -> [[Position]]
+varOccurences subst v = map (sort . go [] . normAC) $ rangeVFresh subst
+ where
+ go pos (Lit (Var v')) | v == v' = [pos]
+ | otherwise = []
+ go _ (Lit (Con _)) = []
+ go pos (FApp (AC _) as) = concatMap (go (0:pos)) as
+ go pos (FApp _ as) =
+ concat (zipWith (\i -> go (i:pos)) [0 .. ] as)
diff --git a/src/Term/SubtermRule.hs b/src/Term/SubtermRule.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/SubtermRule.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable #-}
+-- |
+-- Copyright : (c) 2011, 2012 Benedikt Schmidt
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Subterm rewriting rules.
+module Term.SubtermRule (
+ StRhs(..)
+ , StRule(..)
+ , rRuleToStRule
+ , stRuleToRRule
+
+ -- * Pretty Printing
+ , prettyStRule
+ ) where
+
+import Control.DeepSeq
+
+import Data.DeriveTH
+import Data.Binary
+
+import Term.LTerm
+import Term.Positions
+import Text.PrettyPrint.Highlight
+
+-- | The righthand-side of a subterm rewrite rule.
+-- Does not enforce that the term for RhsGround must be ground.
+data StRhs = RhsGround LNTerm | RhsPosition Position
+ deriving (Show,Ord,Eq)
+
+-- | A subterm rewrite rule.
+data StRule = StRule LNTerm StRhs
+ deriving (Show,Ord,Eq)
+
+-- | Convert a rewrite rule to a subterm rewrite rule if possible.
+rRuleToStRule :: RRule LNTerm -> Maybe StRule
+rRuleToStRule (lhs `RRule` rhs)
+ | frees rhs == [] = Just $ StRule lhs (RhsGround rhs)
+ | otherwise = case findSubterm lhs [] of
+ []:_ -> Nothing -- proper subterm required
+ pos:_ -> Just $ StRule lhs (RhsPosition (reverse pos))
+ [] -> Nothing
+ where
+ findSubterm t rpos | t == rhs = [rpos]
+ findSubterm (FApp _ args) rpos =
+ concat $ zipWith (\t i -> findSubterm t (i:rpos)) args [0..]
+ findSubterm (Lit _) _ = []
+
+-- | Convert a subterm rewrite rule to a rewrite rule.
+stRuleToRRule :: StRule -> RRule LNTerm
+stRuleToRRule (StRule lhs rhs) = case rhs of
+ RhsGround t -> lhs `RRule` t
+ RhsPosition p -> lhs `RRule` (lhs >* p)
+
+{-
+
+test:
+xorRules == map (stRuleToRRule . fromJust . rRuleToStRule) xorRules
+
+-}
+
+------------------------------------------------------------------------------
+-- Pretty Printing
+------------------------------------------------------------------------------
+
+-- | Pretty print an 'StRule'
+prettyStRule :: HighlightDocument d => StRule -> d
+prettyStRule r = case stRuleToRRule r of
+ (lhs `RRule` rhs) -> sep [ nest 2 $ prettyLNTerm lhs
+ , operator_ "=" <-> prettyLNTerm rhs ]
+
+-- derived instances
+--------------------
+
+$(derive makeBinary ''StRhs)
+$(derive makeBinary ''StRule)
+
+$(derive makeNFData ''StRhs)
+$(derive makeNFData ''StRule)
diff --git a/src/Term/Term.hs b/src/Term/Term.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Term.hs
@@ -0,0 +1,400 @@
+{-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable #-}
+-- |
+-- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- Term Algebra and related notions.
+module Term.Term (
+ -- * Signatures and function symbols
+ FunSym(..)
+ , ACSym(..)
+ , NonACSym
+ , expSym
+ , pairSym
+ , invSym
+ , oneSym
+ , emptySym
+ , zeroSym
+ , FunSig
+
+
+ -- * Terms
+ , Term (..)
+
+ , foldTerm
+ , lits
+ , prettyTerm
+
+ -- ** Smart constructors
+ , listToTerm
+
+ -- ** Destrutors
+ , destPair
+ , destInv
+
+ -- * Terms with constants and variables
+ , Lit(..)
+ , VTerm
+
+ , varTerm
+ , constTerm
+ , varsVTerm
+ , occursVTerm
+ , constsVTerm
+ , isVar
+
+ , IsVar
+ , IsConst
+
+ -- * Equalities
+ , Equal (..)
+ , evalEqual
+
+ -- * Matching Problems
+ , Match(..)
+
+ -- * Rewriting Rules
+ , RRule(..)
+
+ , module Term.Classes
+ ) where
+
+import Data.List
+import qualified Data.DList as D
+import Data.Monoid
+import Data.Foldable (Foldable, foldMap)
+import Data.Traversable
+import Data.Typeable
+import Data.Generics
+import Data.DeriveTH
+import Data.Binary
+
+import Control.DeepSeq
+import Control.Basics
+
+import Extension.Prelude
+
+import Text.Isar
+
+import Term.Classes
+
+----------------------------------------------------------------------
+-- AC operators for terms
+----------------------------------------------------------------------
+
+-- | AC function symbols.
+data ACSym = MUn | Xor | Mult
+ deriving (Eq, Ord, Typeable, Data, Show)
+
+-- | non-AC function symbols
+type NonACSym = (String, Int)
+
+-- | Function symbols
+data FunSym = NonAC NonACSym -- ^ a non-AC function function symbol of a given arity
+ | AC ACSym -- ^ an AC function symbol, can be used n-ary
+ | List -- ^ a non-AC n-ary function symbol of TOP sort
+ deriving (Eq, Ord, Typeable, Data, Show)
+
+-- | Function signatures.
+type FunSig = [NonACSym]
+
+
+
+pairSym, expSym, invSym, oneSym, zeroSym, emptySym :: NonACSym
+-- | Pairing.
+pairSym = ("pair",2)
+-- | Exponentiation.
+expSym = ("exp",2)
+-- | The inverse in the groups of exponents.
+invSym = ("inv",1)
+-- | The one in the group of exponents.
+oneSym = ("one", 0)
+-- | The zero for Xor.
+zeroSym = ("zero",0)
+-- | The empty multiset.
+emptySym = ("empty",0)
+
+-- | Destruct a top-level function application.
+{-# INLINE destFunApp #-}
+destFunApp :: FunSym -> Term a -> Maybe [Term a]
+destFunApp fsym (FApp fsym' args) | fsym == fsym' = Just args
+destFunApp _ _ = Nothing
+
+-- | Destruct a top-level pair.
+destPair :: Term a -> Maybe (Term a, Term a)
+destPair t = do [t1, t2] <- destFunApp (NonAC pairSym) t; return (t1, t2)
+
+-- | Destruct a top-level inverse in the group of exponents.
+destInv :: Term a -> Maybe (Term a)
+destInv t = do [t1] <- destFunApp (NonAC invSym) t; return t1
+
+----------------------------------------------------------------------
+-- Terms
+----------------------------------------------------------------------
+
+-- | A term in T(Sigma,a).
+data Term a = Lit a -- ^ atomic terms (constants, variables, ..)
+ | FApp FunSym [Term a] -- ^ function applications
+ deriving (Eq, Ord, Typeable, Data )
+
+
+-- Instances
+------------
+
+instance Functor Term where
+ {-# INLINE fmap #-}
+ fmap f = foldTerm (Lit . f) FApp
+
+instance Foldable Term where
+ {-# INLINE foldMap #-}
+ foldMap f = foldTerm f (const mconcat)
+
+instance Traversable Term where
+ {-# INLINE traverse #-}
+ traverse f (Lit x) = Lit <$> f x
+ traverse f (FApp fsym as) = FApp fsym <$> traverse (traverse f) as
+
+instance Applicative Term where
+ {-# INLINE pure #-}
+ pure = Lit
+ {-# INLINE (<*>) #-}
+ f <*> a = a >>= (\x -> fmap ($ x) f)
+
+instance Monad Term where
+ {-# INLINE return #-}
+ return = Lit
+ {-# INLINE (>>=) #-}
+ m >>= f = foldTerm f FApp m
+
+instance Show a => Show (Term a) where
+ show (Lit l) = show l
+ show (FApp (NonAC (s,_)) []) = s
+ show (FApp (NonAC (s,_)) as) = s++"("++(intercalate "," (map show as))++")"
+ show (FApp List as) = "LIST"++"("++(intercalate "," (map show as))++")"
+ show (FApp (AC o) as) = show o++"("++(intercalate "," (map show as))++")"
+
+
+
+-- | The fold function for @Term a@.
+{-# INLINE foldTerm #-}
+foldTerm :: (t -> b) -> (FunSym -> [b] -> b)
+ -> Term t -> b
+foldTerm fLit fApp t = go t
+ where go (Lit a) = fLit a
+ go (FApp fsym a) = fApp fsym $ map go a
+
+
+instance Sized a => Sized (Term a) where
+ size = foldTerm size (const $ \xs -> sum xs + 1)
+
+-- | @lits t@ returns all literals that occur in term @t@. List can contain duplicates.
+lits :: Ord a => Term a -> [a]
+lits = foldMap return
+
+-- | @listToTerm ts@ returns a term that represents @ts@.
+listToTerm :: [Term a] -> Term a
+listToTerm ts = FApp List ts
+
+----------------------------------------------------------------------
+-- Terms with constants and variables
+----------------------------------------------------------------------
+
+
+-- | A Lit is either a constant or a variable. (@Const@ is taken by Control.Applicative)
+data Lit c v = Con c | Var v
+ deriving (Eq, Ord, Data, Typeable)
+
+-- | A VTerm is a term with constants and variables
+type VTerm c v = Term (Lit c v)
+
+-- | collect class constraints for variables
+class (Ord v, Eq v, Show v) => IsVar v where
+
+-- | collect class constraints for constants
+class (Ord c, Eq c, Show c, Data c) => IsConst c where
+
+-- | Functor instance in the variable.
+instance Functor (Lit c) where
+ fmap f (Var v) = Var (f v)
+ fmap _ (Con c) = Con c
+
+-- | Foldable instance in the variable.
+instance Foldable (Lit c) where
+ foldMap f (Var v) = f v
+ foldMap _ (Con _) = mempty
+
+-- | Traversable instance in the variable.
+instance Traversable (Lit c) where
+ sequenceA (Var v) = Var <$> v
+ sequenceA (Con n) = pure $ Con n
+
+-- | Applicative instance in the variable.
+instance Applicative (Lit c) where
+ pure = Var
+ (Var f) <*> (Var x) = Var (f x)
+ (Var _) <*> (Con n) = Con n
+ (Con n) <*> _ = Con n
+
+-- | Monad instance in the variable
+instance Monad (Lit c) where
+ return = Var
+ (Var x) >>= f = f x
+ (Con n) >>= _ = Con n
+
+instance Sized (Lit c v) where
+ size _ = 1
+
+instance (Show v, Show c) => Show (Lit c v) where
+ show (Var x) = show x
+ show (Con n) = show n
+
+-- | @varTerm v@ is the 'VTerm' with the variable @v@.
+varTerm :: v -> VTerm c v
+varTerm = Lit . Var
+
+-- | @constTerm c@ is the 'VTerm' with the const @c@.
+constTerm :: c -> VTerm c v
+constTerm = Lit . Con
+
+-- | @isVar t returns @True@ if @t@ is a variable.
+isVar :: VTerm c v -> Bool
+isVar (Lit (Var _)) = True
+isVar _ = False
+
+-- | @vars t@ returns a duplicate-free list of variables that occur in @t@.
+varsVTerm :: (Eq v, Ord v) => VTerm c v -> [v]
+varsVTerm = sortednub . D.toList . foldMap (foldMap return)
+
+-- | @occurs v t@ returns @True@ if @v@ occurs in @t@
+occursVTerm :: Eq v => v -> VTerm c v -> Bool
+occursVTerm v = getAny . foldMap (foldMap (Any . (v==)))
+
+-- | @constsVTerm t@ returns a duplicate-free list of constants that occur in @t@.
+constsVTerm :: IsConst c => VTerm c v -> [c]
+constsVTerm = sortednub . D.toList . foldMap fLit
+ where fLit (Var _) = mempty
+ fLit (Con n) = return n
+
+----------------------------------------------------------------------
+-- Equalities, matching problems, and rewriting rules
+----------------------------------------------------------------------
+
+-- | An equality.
+data Equal a = Equal { eqLHS :: a, eqRHS :: a }
+ deriving (Eq, Show)
+
+-- | True iff the two sides of the equality are equal with respect to their
+-- 'Eq' instance.
+evalEqual :: Eq a => Equal a -> Bool
+evalEqual (Equal l r) = l == r
+
+instance Functor Equal where
+ fmap f (Equal lhs rhs) = Equal (f lhs) (f rhs)
+
+instance Monoid a => Monoid (Equal a) where
+ mempty = Equal mempty mempty
+ (Equal l1 r1) `mappend` (Equal l2 r2) =
+ Equal (l1 `mappend` l2) (r1 `mappend` r2)
+
+instance Foldable Equal where
+ foldMap f (Equal l r) = f l `mappend` f r
+
+instance Traversable Equal where
+ traverse f (Equal l r) = Equal <$> f l <*> f r
+
+instance Applicative Equal where
+ pure x = Equal x x
+ (Equal fl fr) <*> (Equal l r) = Equal (fl l) (fr r)
+
+-- | A matching problem.
+data Match a = MatchWith { matchTerm :: a, matchPattern :: a }
+ deriving (Eq, Show)
+
+instance Functor Match where
+ fmap f (MatchWith t p) = MatchWith (f t) (f p)
+
+instance Monoid a => Monoid (Match a) where
+ mempty =
+ MatchWith mempty mempty
+ (MatchWith t1 p1) `mappend` (MatchWith t2 p2) =
+ MatchWith (t1 `mappend` t2) (p1 `mappend` p2)
+
+instance Foldable Match where
+ foldMap f (MatchWith t p) = f t `mappend` f p
+
+instance Traversable Match where
+ traverse f (MatchWith t p) = MatchWith <$> f t <*> f p
+
+instance Applicative Match where
+ pure x = MatchWith x x
+ (MatchWith ft fp) <*> (MatchWith t p) = MatchWith (ft t) (fp p)
+
+
+-- | A rewrite rule.
+data RRule a = RRule a a
+ deriving (Show, Ord, Eq)
+
+instance Functor RRule where
+ fmap f (RRule lhs rhs) = RRule (f lhs) (f rhs)
+
+instance Monoid a => Monoid (RRule a) where
+ mempty = RRule mempty mempty
+ (RRule l1 r1) `mappend` (RRule l2 r2) =
+ RRule (l1 `mappend` l2) (r1 `mappend` r2)
+
+instance Foldable RRule where
+ foldMap f (RRule l r) = f l `mappend` f r
+
+instance Traversable RRule where
+ traverse f (RRule l r) = RRule <$> f l <*> f r
+
+instance Applicative RRule where
+ pure x = RRule x x
+ (RRule fl fr) <*> (RRule l r) = RRule (fl l) (fr r)
+
+----------------------------------------------------------------------
+-- Pretty printing
+----------------------------------------------------------------------
+
+-- | Pretty print a term.
+prettyTerm :: Document d => (l -> d) -> Term l -> d
+prettyTerm ppLit = ppTerm
+ where
+ ppTerm t = case t of
+ Lit l -> ppLit l
+ FApp (AC o) ts -> ppTerms (ppACOp o) 1 "(" ")" ts
+ FApp (NonAC ("exp",2)) [t1,t2] -> ppTerm t1 <> text "^" <> ppTerm t2
+ FApp (NonAC ("pair",2)) _ -> ppTerms ", " 1 "<" ">" (split t)
+ FApp (NonAC (f,_)) ts -> ppFun f ts
+ FApp List ts -> ppFun "LIST" ts
+
+ ppACOp Mult = "*"
+ ppACOp MUn = "#"
+ ppACOp Xor = "+"
+
+ ppTerms sepa n lead finish ts =
+ fcat . (text lead :) . (++[text finish]) .
+ map (nest n) . punctuate (text sepa) . map ppTerm $ ts
+
+ split (FApp (NonAC ("pair",2)) [t1,t2]) = t1 : split t2
+ split t = [t]
+
+ ppFun f ts =
+ text (f ++"(") <> fsep (punctuate comma (map ppTerm ts)) <> text ")"
+
+-- Derived instances
+--------------------
+
+$( derive makeNFData ''FunSym)
+$( derive makeNFData ''ACSym)
+$( derive makeNFData ''Term )
+$( derive makeNFData ''Lit)
+
+$( derive makeBinary ''FunSym)
+$( derive makeBinary ''ACSym)
+$( derive makeBinary ''Term )
+$( derive makeBinary ''Lit)
+
+
diff --git a/src/Term/Unification.hs b/src/Term/Unification.hs
new file mode 100644
--- /dev/null
+++ b/src/Term/Unification.hs
@@ -0,0 +1,239 @@
+{-# LANGUAGE FlexibleContexts, GeneralizedNewtypeDeriving #-}
+-- |
+-- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier
+-- License : GPL v3 (see LICENSE)
+--
+-- Maintainer : Benedikt Schmidt
+--
+-- AC unification based on maude and free unification.
+module Term.Unification (
+ -- * Unification modulo AC
+ unifyLTerm
+ , unifyLNTerm
+
+ -- * matching modulo AC
+ , matchLTerm
+ , matchLNTerm
+
+ , unifyLTermFactored
+ , unifyLNTermFactored
+
+ -- * Handles to a Maude process
+ , MaudeHandle
+ , WithMaude
+ , startMaude
+ , getMaudeStats
+ , mhMaudeSig
+ , mhFilePath
+
+ -- * Maude signatures
+ , MaudeSig(..)
+ , emptyMaudeSig
+ , minimalMaudeSig
+ , dhMaudeSig
+ , xorMaudeSig
+ , msetMaudeSig
+ , pairMaudeSig
+ , symEncMaudeSig
+ , asymEncMaudeSig
+ , signatureMaudeSig
+ , hashMaudeSig
+ , allMaudeSig
+ , rrulesForMaudeSig
+ , funSigForMaudeSig
+
+
+ -- * Convenience exports
+ , module Term.Substitution
+) where
+
+import Control.Applicative
+import Control.Monad.RWS
+import Control.Monad.Reader
+import Control.Monad.Error
+import Control.Monad.State
+import Data.List
+import qualified Data.Map as M
+import Data.Map (Map)
+
+import System.IO.Unsafe (unsafePerformIO)
+
+import Term.Rewriting.NormAC ( (==#) )
+import Term.Substitution
+import qualified Term.Maude.Process as UM
+import Term.Maude.Process
+ (MaudeHandle, WithMaude, startMaude, getMaudeStats, mhMaudeSig, mhFilePath)
+import Term.Maude.Types
+ (MaudeSig(..), emptyMaudeSig, allMaudeSig, rrulesForMaudeSig,
+ funSigForMaudeSig, dhMaudeSig, xorMaudeSig, msetMaudeSig,
+ pairMaudeSig, symEncMaudeSig, asymEncMaudeSig, signatureMaudeSig,
+ hashMaudeSig, minimalMaudeSig)
+
+import Debug.Trace.Ignore
+-- import qualified Debug.Trace as DT
+
+-- Unification modulo AC
+----------------------------------------------------------------------
+
+-- | @unifyLTerm sortOf eqs@ returns a complete set of unifiers for @eqs@ modulo AC.
+unifyLTermFactored :: (IsConst c , Show (Lit c LVar), Ord c)
+ => (c -> LSort)
+ -> [Equal (LTerm c)]
+ -> WithMaude (LSubst c, [SubstVFresh c LVar])
+unifyLTermFactored sortOf eqs = reader $ \h -> (\res -> trace (unlines $ ["unifyLTerm: "++ show eqs, "result = "++ show res]) res) $ do
+ solve h $ execRWST unif sortOf M.empty
+ where
+ unif = sequence [ unifyRaw t p | Equal t p <- eqs ]
+ solve _ Nothing = (emptySubst, [])
+ solve _ (Just (m, [])) = (substFromMap m, [emptySubstVFresh])
+ solve h (Just (m, leqs)) =
+ (subst, unsafePerformIO (UM.unifyViaMaude h sortOf $
+ map (applyVTerm subst <$>) leqs))
+ where subst = substFromMap m
+
+
+-- | @unifyLTerm sortOf eqs@ returns a complete set of unifiers for @eqs@ modulo AC.
+unifyLNTermFactored :: [Equal LNTerm]
+ -> WithMaude (LNSubst, [SubstVFresh Name LVar])
+unifyLNTermFactored = unifyLTermFactored sortOfName
+
+-- | @unifyLNTerm eqs@ returns a complete set of unifiers for @eqs@ modulo AC.
+unifyLTerm :: (IsConst c , Show (Lit c LVar), Ord c)
+ => (c -> LSort)
+ -> [Equal (LTerm c)]
+ -> WithMaude [SubstVFresh c LVar]
+unifyLTerm sortOf eqs = flattenUnif <$> unifyLTermFactored sortOf eqs
+
+
+-- | @unifyLNTerm eqs@ returns a complete set of unifiers for @eqs@ modulo AC.
+unifyLNTerm :: [Equal LNTerm] -> WithMaude [SubstVFresh Name LVar]
+-- unifyLNTerm eqs = reader $ \hnd -> (\res -> DT.trace (show ("unify", res, eqs)) res) $ unifyLTerm sortOfName eqs `runReader` hnd
+unifyLNTerm = unifyLTerm sortOfName
+
+
+-- | Flatten a factored substitution to a list of substitutions.
+flattenUnif :: IsConst c => (LSubst c, [LSubstVFresh c]) -> [LSubstVFresh c]
+flattenUnif (subst, substs) = (\res -> trace (show ("flattenUnif",subst, substs,res )) res) $ map (`composeVFresh` subst) substs
+
+-- Matching modulo AC
+----------------------------------------------------------------------
+
+
+-- | @matchLNTerm sortOf eqs@ returns a complete set of matchers for @eqs@ modulo AC.
+matchLTerm :: (IsConst c , Show (Lit c LVar), Ord c)
+ => (c -> LSort)
+ -> [Match (LTerm c)]
+ -> WithMaude [Subst c LVar]
+matchLTerm sortOf eqs =
+ reader $ \h -> (\res -> trace (unlines $ ["matchLTerm: "++ show eqs, "result = "++ show res]) res) $
+ case runState (runErrorT match) M.empty of
+ (Left NoMatch,_) -> []
+ (Left ACProblem, _) -> unsafePerformIO (UM.matchViaMaude h sortOf eqs)
+ (Right _, mappings) -> [substFromMap mappings]
+ where
+ match = sequence [ matchRaw sortOf t p | MatchWith t p <- eqs ]
+
+
+-- | @matchLNTerm eqs@ returns a complete set of matchers for @eqs@ modulo AC.
+matchLNTerm :: [Match LNTerm] -> WithMaude [Subst Name LVar]
+matchLNTerm = matchLTerm sortOfName
+
+-- Free unification with lazy AC-equation solving.
+--------------------------------------------------------------------
+
+type UnifyRaw c = RWST (c -> LSort) [Equal (LTerm c)] (Map LVar (VTerm c LVar)) Maybe
+
+-- | Unify two 'LTerm's with delayed AC-unification.
+unifyRaw :: IsConst c => LTerm c -> LTerm c -> UnifyRaw c ()
+unifyRaw l0 r0 = do
+ mappings <- get
+ sortOf <- ask
+ l <- gets ((`applyVTerm` l0) . substFromMap)
+ r <- gets ((`applyVTerm` r0) . substFromMap)
+ guard (trace (show ("unifyRaw", mappings, l ,r)) True)
+ case (l, r) of
+ (Lit (Var vl), Lit (Var vr))
+ | vl == vr -> return ()
+ | otherwise -> case (lvarSort vl, lvarSort vr) of
+ (sl, sr) | sl == sr -> if vl < vr then elim vr l
+ else elim vl r
+ _ | sortGeqLTerm sortOf vl r -> elim vl r
+ -- If unification can succeed here, then it must work by
+ -- elimating the right-hand variable with the left-hand side.
+ _ -> elim vr l
+
+ (Lit (Var vl), _ ) -> elim vl r
+ (_, Lit (Var vr) ) -> elim vr l
+ (Lit (Con cl), Lit (Con cr) ) -> guard (cl == cr)
+ (FApp (NonAC lfsym) largs, FApp (NonAC rfsym) rargs) ->
+ guard (lfsym == rfsym && length largs == length rargs)
+ >> sequence_ (zipWith unifyRaw largs rargs)
+ (FApp List largs, FApp List rargs) ->
+ guard (length largs == length rargs)
+ >> sequence_ (zipWith unifyRaw largs rargs)
+ -- NOTE: We assume here that terms of the form mult(t) never occur.
+ (FApp (AC lacsym) _, FApp (AC racsym) _) ->
+ guard (lacsym == racsym) >> tell [Equal l r] -- delay unification
+
+ -- all unifiable pairs of term constructors have been enumerated
+ _ -> mzero -- no unifier
+ where
+ elim v t
+ | v `occurs` t = mzero -- no unifier
+ | otherwise = do
+ sortOf <- ask
+ guard (sortGeqLTerm sortOf v t)
+ modify (M.insert v t . M.map (applyVTerm (substFromList [(v,t)])))
+
+
+data MatchFailure = NoMatch | ACProblem
+
+instance Error MatchFailure where
+ strMsg _ = NoMatch
+
+-- | Ensure that the computed substitution @sigma@ satisfies
+-- @t ==_AC apply sigma p@ after the delayed equations are solved.
+matchRaw :: IsConst c
+ => (c -> LSort)
+ -> LTerm c -- ^ Term @t@
+ -> LTerm c -- ^ Pattern @p@.
+ -> ErrorT MatchFailure (State (Map LVar (VTerm c LVar))) ()
+matchRaw sortOf t p = do
+ mappings <- get
+ guard (trace (show (mappings,t,p)) True)
+ case (t, p) of
+ (_, Lit (Var vp)) ->
+ case M.lookup vp mappings of
+ Nothing -> do
+ unless (sortGeqLTerm sortOf vp t) $
+ throwError NoMatch
+ modify (M.insert vp t)
+ Just tp | t ==# tp -> return ()
+ | otherwise -> throwError NoMatch
+
+ (Lit (Con ct), Lit (Con cp)) -> guard (ct == cp)
+ (FApp (NonAC tfsym) targs, FApp (NonAC pfsym) pargs) ->
+ guard (tfsym == pfsym && length targs == length pargs)
+ >> sequence_ (zipWith (matchRaw sortOf) targs pargs)
+ (FApp List targs, FApp List pargs) ->
+ guard (length targs == length pargs)
+ >> sequence_ (zipWith (matchRaw sortOf) targs pargs)
+ (FApp (AC _) _, FApp (AC _) _) -> throwError ACProblem
+
+ -- all matchable pairs of term constructors have been enumerated
+ _ -> throwError NoMatch
+
+
+-- | @sortGreaterEq v t@ returns @True@ if the sort ensures that the sort of @v@ is greater or equal to
+-- the sort of @t@.
+sortGeqLTerm :: IsConst c => (c -> LSort) -> LVar -> LTerm c -> Bool
+sortGeqLTerm st v t = do
+ case (lvarSort v, sortOfLTerm st t) of
+ (s1, s2) | s1 == s2 -> True
+ -- Node is incomparable to all other sorts, invalid input
+ (LSortNode, _ ) -> errNodeSort
+ (_, LSortNode) -> errNodeSort
+ (s1, s2) -> sortCompare s1 s2 `elem` [Just EQ, Just GT]
+ where
+ errNodeSort = error $
+ "sortGeqLTerm: node sort misuse " ++ show v ++ " -> " ++ show t
diff --git a/tamarin-prover-term.cabal b/tamarin-prover-term.cabal
new file mode 100644
--- /dev/null
+++ b/tamarin-prover-term.cabal
@@ -0,0 +1,82 @@
+name: tamarin-prover-term
+
+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: Benedikt Schmidt
+copyright: Benedikt Schmidt, Simon Meier, ETH Zurich, 2010-2012
+
+synopsis: Term manipulation library for the tamarin prover.
+
+description: This is an internal library of the @tamarin@ prover for
+ security protocol verification
+ ().
+ .
+ This library provides term manipulation infrastructure
+ (matching, unification, narrowing, finite variants) for
+ the @tamarin@ prover. It uses maude
+ () as a backend for
+ normalization, equational matching, and unification.
+
+homepage: http://www.infsec.ethz.ch/research/software#TAMARIN
+
+
+----------------------
+-- library stanzas
+----------------------
+
+library
+ build-depends:
+ base == 4.*
+ , mtl == 2.0.*
+ , containers == 0.4.*
+ , dlist == 0.5.*
+ , safe == 0.2.*
+ , split == 0.1.*
+ , parsec == 3.1.*
+ , syb >= 0.3.3 && < 0.4
+ , directory == 1.1.*
+ , process == 1.0.*
+ , deepseq == 1.1.*
+ , binary == 0.5.*
+ , derive == 2.5.*
+
+ , tamarin-prover-utils == 0.1.*
+
+ hs-source-dirs: src
+
+ exposed-modules:
+ Term.Unification
+ Term.LTerm
+ Term.Positions
+ Term.SubtermRule
+ Term.Subsumption
+ Term.Substitution
+
+ Term.Rewriting.Norm
+ Term.Rewriting.NormAC
+
+ Term.Narrowing.Variants
+ Term.Narrowing.Variants.Check
+ Term.Narrowing.Variants.Compute
+
+ Term.Builtin.Convenience
+ Term.Builtin.Rules
+ Term.Builtin.Signature
+
+ Term.Maude.Process
+ Term.Maude.Types
+
+ other-modules:
+ Term.Term
+ Term.Classes
+
+ Term.Narrowing.Narrow
+
+ Term.Substitution.SubstVFree
+ Term.Substitution.SubstVFresh