packages feed

tamarin-prover-term (empty) → 0.1.0.0

raw patch · 24 files changed

+4264/−0 lines, 24 filesdep +basedep +binarydep +containerssetup-changed

Dependencies added: base, binary, containers, deepseq, derive, directory, dlist, mtl, parsec, process, safe, split, syb, tamarin-prover-utils

Files

+ LICENSE view
@@ -0,0 +1,621 @@+                    GNU GENERAL PUBLIC LICENSE+                       Version 3, 29 June 2007++ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>+ Everyone is permitted to copy and distribute verbatim copies+ of this license document, but changing it is not allowed.++                            Preamble++  The GNU General Public License is a free, copyleft license for+software and other kinds of works.++  The licenses for most software and other practical works are designed+to take away your freedom to share and change the works.  By contrast,+the GNU General Public License is intended to guarantee your freedom to+share and change all versions of a program--to make sure it remains free+software for all its users.  We, the Free Software Foundation, use the+GNU General Public License for most of our software; it applies also to+any other work released this way by its authors.  You can apply it to+your programs, too.++  When we speak of free software, we are referring to freedom, not+price.  Our General Public Licenses are designed to make sure that you+have the freedom to distribute copies of free software (and charge for+them if you wish), that you receive source code or can get it if you+want it, that you can change the software or use pieces of it in new+free programs, and that you know you can do these things.++  To protect your rights, we need to prevent others from denying you+these rights or asking you to surrender the rights.  Therefore, you have+certain responsibilities if you distribute copies of the software, or if+you modify it: responsibilities to respect the freedom of others.++  For example, if you distribute copies of such a program, whether+gratis or for a fee, you must pass on to the recipients the same+freedoms that you received.  You must make sure that they, too, receive+or can get the source code.  And you must show them these terms so they+know their rights.++  Developers that use the GNU GPL protect your rights with two steps:+(1) assert copyright on the software, and (2) offer you this License+giving you legal permission to copy, distribute and/or modify it.++  For the developers' and authors' protection, the GPL clearly explains+that there is no warranty for this free software.  For both users' and+authors' sake, the GPL requires that modified versions be marked as+changed, so that their problems will not be attributed erroneously to+authors of previous versions.++  Some devices are designed to deny users access to install or run+modified versions of the software inside them, although the manufacturer+can do so.  This is fundamentally incompatible with the aim of+protecting users' freedom to change the software.  The systematic+pattern of such abuse occurs in the area of products for individuals to+use, which is precisely where it is most unacceptable.  Therefore, we+have designed this version of the GPL to prohibit the practice for those+products.  If such problems arise substantially in other domains, we+stand ready to extend this provision to those domains in future versions+of the GPL, as needed to protect the freedom of users.++  Finally, every program is threatened constantly by software patents.+States should not allow patents to restrict development and use of+software on general-purpose computers, but in those that do, we wish to+avoid the special danger that patents applied to a free program could+make it effectively proprietary.  To prevent this, the GPL assures that+patents cannot be used to render the program non-free.++  The precise terms and conditions for copying, distribution and+modification follow.++                       TERMS AND CONDITIONS++  0. Definitions.++  "This License" refers to version 3 of the GNU General Public License.++  "Copyright" also means copyright-like laws that apply to other kinds of+works, such as semiconductor masks.++  "The Program" refers to any copyrightable work licensed under this+License.  Each licensee is addressed as "you".  "Licensees" and+"recipients" may be individuals or organizations.++  To "modify" a work means to copy from or adapt all or part of the work+in a fashion requiring copyright permission, other than the making of an+exact copy.  The resulting work is called a "modified version" of the+earlier work or a work "based on" the earlier work.++  A "covered work" means either the unmodified Program or a work based+on the Program.++  To "propagate" a work means to do anything with it that, without+permission, would make you directly or secondarily liable for+infringement under applicable copyright law, except executing it on a+computer or modifying a private copy.  Propagation includes copying,+distribution (with or without modification), making available to the+public, and in some countries other activities as well.++  To "convey" a work means any kind of propagation that enables other+parties to make or receive copies.  Mere interaction with a user through+a computer network, with no transfer of a copy, is not conveying.++  An interactive user interface displays "Appropriate Legal Notices"+to the extent that it includes a convenient and prominently visible+feature that (1) displays an appropriate copyright notice, and (2)+tells the user that there is no warranty for the work (except to the+extent that warranties are provided), that licensees may convey the+work under this License, and how to view a copy of this License.  If+the interface presents a list of user commands or options, such as a+menu, a prominent item in the list meets this criterion.++  1. Source Code.++  The "source code" for a work means the preferred form of the work+for making modifications to it.  "Object code" means any non-source+form of a work.++  A "Standard Interface" means an interface that either is an official+standard defined by a recognized standards body, or, in the case of+interfaces specified for a particular programming language, one that+is widely used among developers working in that language.++  The "System Libraries" of an executable work include anything, other+than the work as a whole, that (a) is included in the normal form of+packaging a Major Component, but which is not part of that Major+Component, and (b) serves only to enable use of the work with that+Major Component, or to implement a Standard Interface for which an+implementation is available to the public in source code form.  A+"Major Component", in this context, means a major essential component+(kernel, window system, and so on) of the specific operating system+(if any) on which the executable work runs, or a compiler used to+produce the work, or an object code interpreter used to run it.++  The "Corresponding Source" for a work in object code form means all+the source code needed to generate, install, and (for an executable+work) run the object code and to modify the work, including scripts to+control those activities.  However, it does not include the work's+System Libraries, or general-purpose tools or generally available free+programs which are used unmodified in performing those activities but+which are not part of the work.  For example, Corresponding Source+includes interface definition files associated with source files for+the work, and the source code for shared libraries and dynamically+linked subprograms that the work is specifically designed to require,+such as by intimate data communication or control flow between those+subprograms and other parts of the work.++  The Corresponding Source need not include anything that users+can regenerate automatically from other parts of the Corresponding+Source.++  The Corresponding Source for a work in source code form is that+same work.++  2. Basic Permissions.++  All rights granted under this License are granted for the term of+copyright on the Program, and are irrevocable provided the stated+conditions are met.  This License explicitly affirms your unlimited+permission to run the unmodified Program.  The output from running a+covered work is covered by this License only if the output, given its+content, constitutes a covered work.  This License acknowledges your+rights of fair use or other equivalent, as provided by copyright law.++  You may make, run and propagate covered works that you do not+convey, without conditions so long as your license otherwise remains+in force.  You may convey covered works to others for the sole purpose+of having them make modifications exclusively for you, or provide you+with facilities for running those works, provided that you comply with+the terms of this License in conveying all material for which you do+not control copyright.  Those thus making or running the covered works+for you must do so exclusively on your behalf, under your direction+and control, on terms that prohibit them from making any copies of+your copyrighted material outside their relationship with you.++  Conveying under any other circumstances is permitted solely under+the conditions stated below.  Sublicensing is not allowed; section 10+makes it unnecessary.++  3. Protecting Users' Legal Rights From Anti-Circumvention Law.++  No covered work shall be deemed part of an effective technological+measure under any applicable law fulfilling obligations under article+11 of the WIPO copyright treaty adopted on 20 December 1996, or+similar laws prohibiting or restricting circumvention of such+measures.++  When you convey a covered work, you waive any legal power to forbid+circumvention of technological measures to the extent such circumvention+is effected by exercising rights under this License with respect to+the covered work, and you disclaim any intention to limit operation or+modification of the work as a means of enforcing, against the work's+users, your or third parties' legal rights to forbid circumvention of+technological measures.++  4. Conveying Verbatim Copies.++  You may convey verbatim copies of the Program's source code as you+receive it, in any medium, provided that you conspicuously and+appropriately publish on each copy an appropriate copyright notice;+keep intact all notices stating that this License and any+non-permissive terms added in accord with section 7 apply to the code;+keep intact all notices of the absence of any warranty; and give all+recipients a copy of this License along with the Program.++  You may charge any price or no price for each copy that you convey,+and you may offer support or warranty protection for a fee.++  5. Conveying Modified Source Versions.++  You may convey a work based on the Program, or the modifications to+produce it from the Program, in the form of source code under the+terms of section 4, provided that you also meet all of these conditions:++    a) The work must carry prominent notices stating that you modified+    it, and giving a relevant date.++    b) The work must carry prominent notices stating that it is+    released under this License and any conditions added under section+    7.  This requirement modifies the requirement in section 4 to+    "keep intact all notices".++    c) You must license the entire work, as a whole, under this+    License to anyone who comes into possession of a copy.  This+    License will therefore apply, along with any applicable section 7+    additional terms, to the whole of the work, and all its parts,+    regardless of how they are packaged.  This License gives no+    permission to license the work in any other way, but it does not+    invalidate such permission if you have separately received it.++    d) If the work has interactive user interfaces, each must display+    Appropriate Legal Notices; however, if the Program has interactive+    interfaces that do not display Appropriate Legal Notices, your+    work need not make them do so.++  A compilation of a covered work with other separate and independent+works, which are not by their nature extensions of the covered work,+and which are not combined with it such as to form a larger program,+in or on a volume of a storage or distribution medium, is called an+"aggregate" if the compilation and its resulting copyright are not+used to limit the access or legal rights of the compilation's users+beyond what the individual works permit.  Inclusion of a covered work+in an aggregate does not cause this License to apply to the other+parts of the aggregate.++  6. Conveying Non-Source Forms.++  You may convey a covered work in object code form under the terms+of sections 4 and 5, provided that you also convey the+machine-readable Corresponding Source under the terms of this License,+in one of these ways:++    a) Convey the object code in, or embodied in, a physical product+    (including a physical distribution medium), accompanied by the+    Corresponding Source fixed on a durable physical medium+    customarily used for software interchange.++    b) Convey the object code in, or embodied in, a physical product+    (including a physical distribution medium), accompanied by a+    written offer, valid for at least three years and valid for as+    long as you offer spare parts or customer support for that product+    model, to give anyone who possesses the object code either (1) a+    copy of the Corresponding Source for all the software in the+    product that is covered by this License, on a durable physical+    medium customarily used for software interchange, for a price no+    more than your reasonable cost of physically performing this+    conveying of source, or (2) access to copy the+    Corresponding Source from a network server at no charge.++    c) Convey individual copies of the object code with a copy of the+    written offer to provide the Corresponding Source.  This+    alternative is allowed only occasionally and noncommercially, and+    only if you received the object code with such an offer, in accord+    with subsection 6b.++    d) Convey the object code by offering access from a designated+    place (gratis or for a charge), and offer equivalent access to the+    Corresponding Source in the same way through the same place at no+    further charge.  You need not require recipients to copy the+    Corresponding Source along with the object code.  If the place to+    copy the object code is a network server, the Corresponding Source+    may be on a different server (operated by you or a third party)+    that supports equivalent copying facilities, provided you maintain+    clear directions next to the object code saying where to find the+    Corresponding Source.  Regardless of what server hosts the+    Corresponding Source, you remain obligated to ensure that it is+    available for as long as needed to satisfy these requirements.++    e) Convey the object code using peer-to-peer transmission, provided+    you inform other peers where the object code and Corresponding+    Source of the work are being offered to the general public at no+    charge under subsection 6d.++  A separable portion of the object code, whose source code is excluded+from the Corresponding Source as a System Library, need not be+included in conveying the object code work.++  A "User Product" is either (1) a "consumer product", which means any+tangible personal property which is normally used for personal, family,+or household purposes, or (2) anything designed or sold for incorporation+into a dwelling.  In determining whether a product is a consumer product,+doubtful cases shall be resolved in favor of coverage.  For a particular+product received by a particular user, "normally used" refers to a+typical or common use of that class of product, regardless of the status+of the particular user or of the way in which the particular user+actually uses, or expects or is expected to use, the product.  A product+is a consumer product regardless of whether the product has substantial+commercial, industrial or non-consumer uses, unless such uses represent+the only significant mode of use of the product.++  "Installation Information" for a User Product means any methods,+procedures, authorization keys, or other information required to install+and execute modified versions of a covered work in that User Product from+a modified version of its Corresponding Source.  The information must+suffice to ensure that the continued functioning of the modified object+code is in no case prevented or interfered with solely because+modification has been made.++  If you convey an object code work under this section in, or with, or+specifically for use in, a User Product, and the conveying occurs as+part of a transaction in which the right of possession and use of the+User Product is transferred to the recipient in perpetuity or for a+fixed term (regardless of how the transaction is characterized), the+Corresponding Source conveyed under this section must be accompanied+by the Installation Information.  But this requirement does not apply+if neither you nor any third party retains the ability to install+modified object code on the User Product (for example, the work has+been installed in ROM).++  The requirement to provide Installation Information does not include a+requirement to continue to provide support service, warranty, or updates+for a work that has been modified or installed by the recipient, or for+the User Product in which it has been modified or installed.  Access to a+network may be denied when the modification itself materially and+adversely affects the operation of the network or violates the rules and+protocols for communication across the network.++  Corresponding Source conveyed, and Installation Information provided,+in accord with this section must be in a format that is publicly+documented (and with an implementation available to the public in+source code form), and must require no special password or key for+unpacking, reading or copying.++  7. Additional Terms.++  "Additional permissions" are terms that supplement the terms of this+License by making exceptions from one or more of its conditions.+Additional permissions that are applicable to the entire Program shall+be treated as though they were included in this License, to the extent+that they are valid under applicable law.  If additional permissions+apply only to part of the Program, that part may be used separately+under those permissions, but the entire Program remains governed by+this License without regard to the additional permissions.++  When you convey a copy of a covered work, you may at your option+remove any additional permissions from that copy, or from any part of+it.  (Additional permissions may be written to require their own+removal in certain cases when you modify the work.)  You may place+additional permissions on material, added by you to a covered work,+for which you have or can give appropriate copyright permission.++  Notwithstanding any other provision of this License, for material you+add to a covered work, you may (if authorized by the copyright holders of+that material) supplement the terms of this License with terms:++    a) Disclaiming warranty or limiting liability differently from the+    terms of sections 15 and 16 of this License; or++    b) Requiring preservation of specified reasonable legal notices or+    author attributions in that material or in the Appropriate Legal+    Notices displayed by works containing it; or++    c) Prohibiting misrepresentation of the origin of that material, or+    requiring that modified versions of such material be marked in+    reasonable ways as different from the original version; or++    d) Limiting the use for publicity purposes of names of licensors or+    authors of the material; or++    e) Declining to grant rights under trademark law for use of some+    trade names, trademarks, or service marks; or++    f) Requiring indemnification of licensors and authors of that+    material by anyone who conveys the material (or modified versions of+    it) with contractual assumptions of liability to the recipient, for+    any liability that these contractual assumptions directly impose on+    those licensors and authors.++  All other non-permissive additional terms are considered "further+restrictions" within the meaning of section 10.  If the Program as you+received it, or any part of it, contains a notice stating that it is+governed by this License along with a term that is a further+restriction, you may remove that term.  If a license document contains+a further restriction but permits relicensing or conveying under this+License, you may add to a covered work material governed by the terms+of that license document, provided that the further restriction does+not survive such relicensing or conveying.++  If you add terms to a covered work in accord with this section, you+must place, in the relevant source files, a statement of the+additional terms that apply to those files, or a notice indicating+where to find the applicable terms.++  Additional terms, permissive or non-permissive, may be stated in the+form of a separately written license, or stated as exceptions;+the above requirements apply either way.++  8. Termination.++  You may not propagate or modify a covered work except as expressly+provided under this License.  Any attempt otherwise to propagate or+modify it is void, and will automatically terminate your rights under+this License (including any patent licenses granted under the third+paragraph of section 11).++  However, if you cease all violation of this License, then your+license from a particular copyright holder is reinstated (a)+provisionally, unless and until the copyright holder explicitly and+finally terminates your license, and (b) permanently, if the copyright+holder fails to notify you of the violation by some reasonable means+prior to 60 days after the cessation.++  Moreover, your license from a particular copyright holder is+reinstated permanently if the copyright holder notifies you of the+violation by some reasonable means, this is the first time you have+received notice of violation of this License (for any work) from that+copyright holder, and you cure the violation prior to 30 days after+your receipt of the notice.++  Termination of your rights under this section does not terminate the+licenses of parties who have received copies or rights from you under+this License.  If your rights have been terminated and not permanently+reinstated, you do not qualify to receive new licenses for the same+material under section 10.++  9. Acceptance Not Required for Having Copies.++  You are not required to accept this License in order to receive or+run a copy of the Program.  Ancillary propagation of a covered work+occurring solely as a consequence of using peer-to-peer transmission+to receive a copy likewise does not require acceptance.  However,+nothing other than this License grants you permission to propagate or+modify any covered work.  These actions infringe copyright if you do+not accept this License.  Therefore, by modifying or propagating a+covered work, you indicate your acceptance of this License to do so.++  10. Automatic Licensing of Downstream Recipients.++  Each time you convey a covered work, the recipient automatically+receives a license from the original licensors, to run, modify and+propagate that work, subject to this License.  You are not responsible+for enforcing compliance by third parties with this License.++  An "entity transaction" is a transaction transferring control of an+organization, or substantially all assets of one, or subdividing an+organization, or merging organizations.  If propagation of a covered+work results from an entity transaction, each party to that+transaction who receives a copy of the work also receives whatever+licenses to the work the party's predecessor in interest had or could+give under the previous paragraph, plus a right to possession of the+Corresponding Source of the work from the predecessor in interest, if+the predecessor has it or can get it with reasonable efforts.++  You may not impose any further restrictions on the exercise of the+rights granted or affirmed under this License.  For example, you may+not impose a license fee, royalty, or other charge for exercise of+rights granted under this License, and you may not initiate litigation+(including a cross-claim or counterclaim in a lawsuit) alleging that+any patent claim is infringed by making, using, selling, offering for+sale, or importing the Program or any portion of it.++  11. Patents.++  A "contributor" is a copyright holder who authorizes use under this+License of the Program or a work on which the Program is based.  The+work thus licensed is called the contributor's "contributor version".++  A contributor's "essential patent claims" are all patent claims+owned or controlled by the contributor, whether already acquired or+hereafter acquired, that would be infringed by some manner, permitted+by this License, of making, using, or selling its contributor version,+but do not include claims that would be infringed only as a+consequence of further modification of the contributor version.  For+purposes of this definition, "control" includes the right to grant+patent sublicenses in a manner consistent with the requirements of+this License.++  Each contributor grants you a non-exclusive, worldwide, royalty-free+patent license under the contributor's essential patent claims, to+make, use, sell, offer for sale, import and otherwise run, modify and+propagate the contents of its contributor version.++  In the following three paragraphs, a "patent license" is any express+agreement or commitment, however denominated, not to enforce a patent+(such as an express permission to practice a patent or covenant not to+sue for patent infringement).  To "grant" such a patent license to a+party means to make such an agreement or commitment not to enforce a+patent against the party.++  If you convey a covered work, knowingly relying on a patent license,+and the Corresponding Source of the work is not available for anyone+to copy, free of charge and under the terms of this License, through a+publicly available network server or other readily accessible means,+then you must either (1) cause the Corresponding Source to be so+available, or (2) arrange to deprive yourself of the benefit of the+patent license for this particular work, or (3) arrange, in a manner+consistent with the requirements of this License, to extend the patent+license to downstream recipients.  "Knowingly relying" means you have+actual knowledge that, but for the patent license, your conveying the+covered work in a country, or your recipient's use of the covered work+in a country, would infringe one or more identifiable patents in that+country that you have reason to believe are valid.++  If, pursuant to or in connection with a single transaction or+arrangement, you convey, or propagate by procuring conveyance of, a+covered work, and grant a patent license to some of the parties+receiving the covered work authorizing them to use, propagate, modify+or convey a specific copy of the covered work, then the patent license+you grant is automatically extended to all recipients of the covered+work and works based on it.++  A patent license is "discriminatory" if it does not include within+the scope of its coverage, prohibits the exercise of, or is+conditioned on the non-exercise of one or more of the rights that are+specifically granted under this License.  You may not convey a covered+work if you are a party to an arrangement with a third party that is+in the business of distributing software, under which you make payment+to the third party based on the extent of your activity of conveying+the work, and under which the third party grants, to any of the+parties who would receive the covered work from you, a discriminatory+patent license (a) in connection with copies of the covered work+conveyed by you (or copies made from those copies), or (b) primarily+for and in connection with specific products or compilations that+contain the covered work, unless you entered into that arrangement,+or that patent license was granted, prior to 28 March 2007.++  Nothing in this License shall be construed as excluding or limiting+any implied license or other defenses to infringement that may+otherwise be available to you under applicable patent law.++  12. No Surrender of Others' Freedom.++  If conditions are imposed on you (whether by court order, agreement or+otherwise) that contradict the conditions of this License, they do not+excuse you from the conditions of this License.  If you cannot convey a+covered work so as to satisfy simultaneously your obligations under this+License and any other pertinent obligations, then as a consequence you may+not convey it at all.  For example, if you agree to terms that obligate you+to collect a royalty for further conveying from those to whom you convey+the Program, the only way you could satisfy both those terms and this+License would be to refrain entirely from conveying the Program.++  13. Use with the GNU Affero General Public License.++  Notwithstanding any other provision of this License, you have+permission to link or combine any covered work with a work licensed+under version 3 of the GNU Affero General Public License into a single+combined work, and to convey the resulting work.  The terms of this+License will continue to apply to the part which is the covered work,+but the special requirements of the GNU Affero General Public License,+section 13, concerning interaction through a network will apply to the+combination as such.++  14. Revised Versions of this License.++  The Free Software Foundation may publish revised and/or new versions of+the GNU General Public License from time to time.  Such new versions will+be similar in spirit to the present version, but may differ in detail to+address new problems or concerns.++  Each version is given a distinguishing version number.  If the+Program specifies that a certain numbered version of the GNU General+Public License "or any later version" applies to it, you have the+option of following the terms and conditions either of that numbered+version or of any later version published by the Free Software+Foundation.  If the Program does not specify a version number of the+GNU General Public License, you may choose any version ever published+by the Free Software Foundation.++  If the Program specifies that a proxy can decide which future+versions of the GNU General Public License can be used, that proxy's+public statement of acceptance of a version permanently authorizes you+to choose that version for the Program.++  Later license versions may give you additional or different+permissions.  However, no additional obligations are imposed on any+author or copyright holder as a result of your choosing to follow a+later version.++  15. Disclaimer of Warranty.++  THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY+APPLICABLE LAW.  EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT+HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY+OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,+THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR+PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM+IS WITH YOU.  SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF+ALL NECESSARY SERVICING, REPAIR OR CORRECTION.++  16. Limitation of Liability.++  IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS+THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY+GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE+USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF+DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD+PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),+EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF+SUCH DAMAGES.++  17. Interpretation of Sections 15 and 16.++  If the disclaimer of warranty and limitation of liability provided+above cannot be given local legal effect according to their terms,+reviewing courts shall apply local law that most closely approximates+an absolute waiver of all civil liability in connection with the+Program, unless a warranty or assumption of liability accompanies a+copy of the Program in return for a fee.++                     END OF TERMS AND CONDITIONS
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/Term/Builtin/Convenience.hs view
@@ -0,0 +1,226 @@+-- |+-- Copyright   : (c) 2010, 2011 Benedikt Schmidt+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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
+ src/Term/Builtin/Rules.hs view
@@ -0,0 +1,69 @@+-- |+-- Copyright   : (c) 2010, 2011 Benedikt Schmidt+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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) ]
+ src/Term/Builtin/Signature.hs view
@@ -0,0 +1,71 @@+-- |+-- Copyright   : (c) 2010, 2011 Benedikt Schmidt+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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 ]
+ src/Term/Classes.hs view
@@ -0,0 +1,14 @@+-- |+-- Copyright   : (c) 2010, 2011 Benedikt Schmidt & Simon Meier+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- | 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
+ src/Term/LTerm.hs view
@@ -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 <beschmi@gmail.com>+--+-- 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)
+ src/Term/Maude/Process.hs view
@@ -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 <beschmi@gmail.com>+--+-- 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
+ src/Term/Maude/Types.hs view
@@ -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 <beschmi@gmail.com>+--+-- 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)++
+ src/Term/Narrowing/Narrow.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE FlexibleInstances #-}+-- |+-- Copyright   : (c) 2010, 2011 Benedikt Schmidt+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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
+ src/Term/Narrowing/Variants.hs view
@@ -0,0 +1,37 @@+-- |+-- Copyright   : (c) 2010, 2011 Benedikt Schmidt+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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)
+ src/Term/Narrowing/Variants/Check.hs view
@@ -0,0 +1,108 @@+-- |+-- Copyright   : (c) 2010, 2011 Benedikt Schmidt+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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
+ src/Term/Narrowing/Variants/Compute.hs view
@@ -0,0 +1,149 @@+{-# LANGUAGE FlexibleInstances #-}+-- |+-- Copyright   : (c) 2010, 2011 Benedikt Schmidt+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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"
+ src/Term/Positions.hs view
@@ -0,0 +1,43 @@+-- |+-- Copyright   : (c) 2010, 2011 Benedikt Schmidt+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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)
+ src/Term/Rewriting/Norm.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE PatternGuards, FlexibleContexts #-}+-- |+-- Copyright   : (c) 2010, 2011 Benedikt Schmidt+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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
+ src/Term/Rewriting/NormAC.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE PatternGuards, FlexibleContexts #-}+-- |+-- Copyright   : (c) 2010, 2011 Benedikt Schmidt+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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+
+ src/Term/Substitution.hs view
@@ -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 <beschmi@gmail.com>+--+-- 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
+ src/Term/Substitution/SubstVFree.hs view
@@ -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 <beschmi@gmail.com>+--+-- 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)
+ src/Term/Substitution/SubstVFresh.hs view
@@ -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 <beschmi@gmail.com>+--+-- 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)
+ src/Term/Subsumption.hs view
@@ -0,0 +1,112 @@+{-# LANGUAGE GADTs, FlexibleContexts #-}+-- |+-- Copyright   : (c) 2010, 2011 Benedikt Schmidt+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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)
+ src/Term/SubtermRule.hs view
@@ -0,0 +1,81 @@+{-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable #-}+-- |+-- Copyright   : (c) 2011, 2012 Benedikt Schmidt+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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)
+ src/Term/Term.hs view
@@ -0,0 +1,400 @@+{-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable #-}+-- |+-- Copyright   : (c) 2010, 2011 Benedikt Schmidt & Simon Meier+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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)++
+ src/Term/Unification.hs view
@@ -0,0 +1,239 @@+{-# LANGUAGE FlexibleContexts, GeneralizedNewtypeDeriving #-}+-- |+-- Copyright   : (c) 2010-2012 Benedikt Schmidt & Simon Meier+-- License     : GPL v3 (see LICENSE)+-- +-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>+--+-- 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
+ tamarin-prover-term.cabal view
@@ -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 <benedikt.schmidt@inf.ethz.ch>,+                    Simon Meier <simon.meier@inf.ethz.ch>+maintainer:         Benedikt Schmidt <benedikt.schmidt@inf.ethz.ch>+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+                    (<hackage.haskell.org/package/tamarin-prover>). +                    .+                    This library provides term manipulation infrastructure+                    (matching, unification, narrowing, finite variants) for+                    the @tamarin@ prover. It uses maude+                    (<http://maude.cs.uiuc.edu/>) 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