packages feed

BPS (empty) → 0.1.0.0

raw patch · 18 files changed

+6081/−0 lines, 18 filesdep +BPSdep +STMonadTransdep +TLTsetup-changed

Dependencies added: BPS, STMonadTrans, TLT, base, extra, free, mtl, resourcet, symbol, template-haskell, transformers

Files

+ BPS.cabal view
@@ -0,0 +1,99 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.34.4.+--+-- see: https://github.com/sol/hpack++name:           BPS+version:        0.1.0.0+synopsis:       Translations of classic Truth Maintenance Systems+description:    Haskell monad transformer-based translations of two classic Truth Maintenance System algorithms of Forbus and de Kleer's /Building Problem Solvers/.  This version includes justification-based and assumption-based TMS (JTMS and ATMS) implementations.  See the GitHub repository <https://github.com/jphmrst/bps/>, or the Haddock documentation.+category:       Truth maintenance+homepage:       https://github.com/jphmrst/bps#readme+bug-reports:    https://github.com/jphmrst/bps/issues+author:         John Maraist+maintainer:     haskell-tms@maraist.org+copyright:      2022 John Maraist; 1986-1993 Kenneth D. Forbus, Johan de Kleer and Xerox Corporation+license:        GPL-3+license-file:   Haskell-LICENSE.txt+build-type:     Simple+extra-source-files:+    README.md+    ChangeLog.md+    Haskell-LICENSE.txt++source-repository head+  type: git+  location: https://github.com/jphmrst/bps++library+  exposed-modules:+      Data.TMS.ATMS.ATMST+      Data.TMS.ChooseDebugging+      Data.TMS.Dbg+      Data.TMS.Helpers+      Data.TMS.JTMS+      Data.TMS.MList+  other-modules:+      Paths_BPS+  hs-source-dirs:+      src/main/haskell/lib+  ghc-options: -w -Woverlapping-patterns -Wwarnings-deprecations -Wdeprecations -Wdeprecated-flags -Wunrecognised-pragmas -Wduplicate-exports -Wderiving-defaults -Woverflowed-literals -Wempty-enumerations -Wmissing-fields -Wmissing-methods -Wwrong-do-bind -Wtyped-holes -Wdeferred-type-errors -Wpartial-type-signatures -Wunsupported-calling-conventions -Wdodgy-foreign-imports -Winline-rule-shadowing -Wunsupported-llvm-version -Wmissed-extra-shared-lib -Wtabs -Wunrecognised-warning-flags -Winaccessible-code -Wstar-binder -Wmonomorphism-restriction -Wmissing-home-modules -Widentities -Wpartial-fields -Wmissed-specialisations -Wall-missed-specialisations -Wcpp-undef -Wunused-packages -Wunused-type-patterns -Wsafe+  build-depends:+      STMonadTrans >=0.4.6 && <0.5+    , base (>=4.14.1 && <4.15) || (>=4.15.1 && <4.16) || (>=4.16.0 && <4.17)+    , extra ==1.7.*+    , free+    , mtl >=2.2.2 && <2.3+    , resourcet+    , symbol >=0.2.4 && <0.3+    , template-haskell+    , transformers >=0.5.6 && <0.6+  default-language: Haskell2010++executable hbps+  main-is: Main.hs+  other-modules:+      ATMSTrun+      JTMSrun+      Paths_BPS+  hs-source-dirs:+      src/main/haskell/app+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      BPS+    , STMonadTrans >=0.4.6 && <0.5+    , base (>=4.14.1 && <4.15) || (>=4.15.1 && <4.16) || (>=4.16.0 && <4.17)+    , extra ==1.7.*+    , free+    , mtl >=2.2.2 && <2.3+    , resourcet+    , symbol+    , template-haskell+    , transformers >=0.5.6 && <0.6+  default-language: Haskell2010++test-suite BPS-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  other-modules:+      ATMSTests+      JTMSTests+      Testers+      Paths_BPS+  hs-source-dirs:+      src/test/haskell+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      BPS+    , STMonadTrans >=0.4.6 && <0.5+    , TLT >=0.1.0 && <0.2+    , base (>=4.14.1 && <4.15) || (>=4.15.1 && <4.16) || (>=4.16.0 && <4.17)+    , extra ==1.7.*+    , free+    , mtl >=2.2.2 && <2.3+    , resourcet+    , symbol >=0.2.4 && <0.3+    , template-haskell+    , transformers >=0.5.6 && <0.6+  default-language: Haskell2010
+ ChangeLog.md view
@@ -0,0 +1,51 @@++Note that the *repository* version numbers do not directly correspond+to the release numbers of either the Haskell or Scala releases.+Haskell releases adhere to Haskell's [Package Versioning+Policy](https://pvp.haskell.org/); Scala releases use the [Semantic+Versioning spec](https://semver.org/).++# In Haskell branch — Haskell 0.2.0.0++ - Translation of ATMS underway.++# Version 0.5.0 (Haskell 0.1.0.0, Scala 0.1.0)++ - First version with Haskell: working implementation of a monad+   transformer for JTMSes.++ - Promoting Scala release to 0.1.0.  No significant additions, but it+   will be nice to distinguish new feature additions at 0.x.0 from+   patches and documentation additions at 0.x.y.++# Version 0.4.0 (Scala only, 0.0.4)++ - Documentation for both JTMS and ATMS.++ - Generator for large randomized ATMS examples.++ - Some tweaks to data structure selection based on rough profiling.+ +# Version 0.3.0 (Scala only, 0.0.3)++ - Contains a mostly-working version of a standalone ATMS.++# Version 0.2.0 (Scala only, 0.0.2)++ - Separation of the standalone JTMS from (untranslated) JTMS+JTRE+   wrapper.++    - Further testing and debugging of the standalone JTMS.++    - Scaladoc documentation of the standalone JTMS.++    - There may be additional type parameters in later versions of+      the standalone JTMS.++ - First version containing this file.++# Version 0.1.0 (Scala only, 0.0.1)++Initial release++ - Contains a mostly-working version of the standalone JTMS.
+ Haskell-LICENSE.txt view
@@ -0,0 +1,674 @@+                    GNU GENERAL PUBLIC LICENSE+                       Version 3, 29 June 2007++ Copyright (C) 2007 Free Software Foundation, Inc. <https://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++            How to Apply These Terms to Your New Programs++  If you develop a new program, and you want it to be of the greatest+possible use to the public, the best way to achieve this is to make it+free software which everyone can redistribute and change under these terms.++  To do so, attach the following notices to the program.  It is safest+to attach them to the start of each source file to most effectively+state the exclusion of warranty; and each file should have at least+the "copyright" line and a pointer to where the full notice is found.++    <one line to give the program's name and a brief idea of what it does.>+    Copyright (C) <year>  <name of author>++    This program is free software: you can redistribute it and/or modify+    it under the terms of the GNU General Public License as published by+    the Free Software Foundation, either version 3 of the License, or+    (at your option) any later version.++    This program is distributed in the hope that it will be useful,+    but WITHOUT ANY WARRANTY; without even the implied warranty of+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the+    GNU General Public License for more details.++    You should have received a copy of the GNU General Public License+    along with this program.  If not, see <https://www.gnu.org/licenses/>.++Also add information on how to contact you by electronic and paper mail.++  If the program does terminal interaction, make it output a short+notice like this when it starts in an interactive mode:++    <program>  Copyright (C) <year>  <name of author>+    This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'.+    This is free software, and you are welcome to redistribute it+    under certain conditions; type `show c' for details.++The hypothetical commands `show w' and `show c' should show the appropriate+parts of the General Public License.  Of course, your program's commands+might be different; for a GUI interface, you would use an "about box".++  You should also get your employer (if you work as a programmer) or school,+if any, to sign a "copyright disclaimer" for the program, if necessary.+For more information on this, and how to apply and follow the GNU GPL, see+<https://www.gnu.org/licenses/>.++  The GNU General Public License does not permit incorporating your program+into proprietary programs.  If your program is a subroutine library, you+may consider it more useful to permit linking proprietary applications with+the library.  If this is what you want to do, use the GNU Lesser General+Public License instead of this License.  But first, please read+<https://www.gnu.org/licenses/why-not-lgpl.html>.
+ README.md view
@@ -0,0 +1,18 @@+# Truth maintenance system libraries for Scala and Haskell++This repository is a translation from Common Lisp of the truth+maintenance systems and other tools from Forbus and de Kleer's+*Building Problem Solvers* into both Scala and Haskell.++The current version includes working versions of the justification-+and assumption-based truth maintenance systems (JTMS and ATMS) in both+languages.  The Haskell translation omits the two top-level functions+`interpretations` and `explainNode` of the original system, but+otherwise both translations include all of the original functionality+of these two TMSes.  There is a partial translation of the rule engine+wrapper for these TMSes in Scala.++To contribute, submit pull requests to one of the three branches+`atms` (Scala), `jtms` (Scala) or `haskell` (both JTMS and ATMS), or+start a new branch for one of the other BPS tools, at +[its repository](https://github.com/jphmrst/bps-scala).
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/main/haskell/app/ATMSTrun.hs view
@@ -0,0 +1,34 @@+module ATMSTrun where++import Data.Symbol+import Data.TMS.ATMS.ATMST++runATMS1 :: IO (Either AtmsErr ())+runATMS1 = do+  runATMST $ do+    atms <- createATMS "Ex1"+    setInformantStringViaString atms+    setDatumStringViaString atms+    -- debugAtms "Created" atms+    na <- createNode atms "A" True False+    -- debugAtms "Added assumption node A" atms+    nc <- createNode atms "C" True False+    -- debugAtms "Added assumption node C" atms+    ne <- createNode atms "E" True False+    -- debugAtms "Added assumption node E" atms+    nh <- createNode atms "H" False False+    -- debugAtms "Added non-assumption node H" atms+    justifyNode "R1" nh [nc, ne]+    -- debugAtms "After rule R1" atms+    ng <- createNode atms "G" False False+    -- debugAtms "After non-assumption node G" atms+    justifyNode "R2" ng [na, nc]+    -- debugAtms "After rule R2" atms+    nx <- createNode atms "X" False True+    -- debugAtms "After contradiction node X" atms+    justifyNode "R3" nx [ng]+    -- debugAtms "After rule R3" atms+    nb <- createNode atms "B" True False+    debugAtms "Added assumption node B" atms+    justifyNode "R4" nh [nb, nc]+    debugAtms "After rule R4" atms
+ src/main/haskell/app/JTMSrun.hs view
@@ -0,0 +1,14 @@+module JTMSrun where++import Data.Symbol+import Data.TMS.JTMS+import Control.Monad.IO.Class++runJTMS1 :: IO (Either JtmsErr ())+runJTMS1 = runJTMST $ do+  j <- createJTMS "Ex1"+  na <- createNode j (intern "a") True False+  naName <- nodeString na+  naIn <- isInNode na+  liftIO $ putStrLn $+    "Node " ++ naName ++ " is " ++ if naIn then "in" else "out"
+ src/main/haskell/app/Main.hs view
@@ -0,0 +1,10 @@+module Main where++import ATMSTrun+import JTMSrun++main :: IO ()+main = do+  runATMS1+  -- runJTMS1+  return ()
+ src/main/haskell/lib/Data/TMS/ATMS/ATMST.hs view
@@ -0,0 +1,2396 @@+{-|+Module      : ATMS+Description : Mutable assumption-based truth maintenance systems (ATMSes)+Copyright   : (c) John Maraist, 2022+              Kenneth D. Forbus, Johan de Kleer and Xerox Corporation, 1986-1993+License     : AllRightsReserved+Maintainer  : haskell-tms@maraist.org+Stability   : experimental+Portability : POSIX++Translation of Forbus and de Kleer's assumption-based truth+maintenance systems (ATMSes) from Common Lisp to Haskell.++This is not a very \"Haskelly\" implementation; rather, it is a+translation of the original code with minimal changes.  Most of the+deviations from the original are due to either Haskell's strong+typing, which necessitates some additional tagging, and to the+abomination which is Lisp's @do@ macro.  The translation relies on+mutable data structures using `STT` state thread references.  A more+pure translation, possibly not relying on the [@ST@+monad]("Control.Monad.ST")/[@STT@+transformer]("Control.Monad.ST.Trans"), is a significant piece of+future work.++Note also there are restrictions on the embedded monad @m@ which can+be wrapped in the `STT` transformer; see [the @Control.Monad.ST.Trans@+documentation]("Control.Monad.ST.Trans") for details.++See the @LICENSE.txt@ and @README-forbus-dekleer.txt@ files+distributed with this work for a paragraph stating scope of permission+and disclaimer of warranty, and for additional information regarding+copyright ownership.  The above copyright notice and that paragraph+must be included in any separate copy of this file.++Unless required by applicable law or agreed to in writing, software+distributed under the License is distributed on an "AS IS" BASIS,+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or+implied, for NON-COMMERCIAL use.  See the License for the specific+language governing permissions and limitations under the License.++-}++{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}++module Data.TMS.ATMS.ATMST (+  -- * The ATMST monad+  ATMST,+  AtmsErr(CannotRemoveNodeWIthConsequences, InternalNoEmptyEnv, FromMonadFail),+  runATMST,+  setInitialEnvTableAlloc, setEnvTableIncr,+  getInitialEnvTableAlloc, getEnvTableIncr,++  -- * ATMS data structures++  -- ** Component classes+  NodeDatum, contradictionNodeDatum,++  -- ** Top-level ATMS+  ATMS, createATMS, atmsTitle,++  -- *** ATMS components+  getNodes, getJusts, getContradictions, getAssumptions,+  getContradictionNode, getEmptyEnvironment, getNodeString, getJustString,+  getDatumString, getInformantString, getEnqueueProcedure,++  setDatumStringViaString, setDatumStringViaShow,+  setInformantStringViaString, setInformantStringViaShow,++  -- ** Nodes+  Node, nodeDatum, createNode,+  -- *** Node components+  nodeATMS, nodeString, defaultNodeString, getNodeLabel, getNodeRules,+  getNodeConsequences,+  -- *** Setting node status+  assumeNode, makeContradiction, removeNode,++  -- ** Justifications+  JustRule(JustRule), justInformant, justConsequence, justAntecedents,+  Justification, Explanation, justifyNode,++  -- ** Environments and tables+  Env, EnvTable, envIndex, envAssumptions, getEnvNodes,++  -- * Deduction and search utilities+  {- interpretations, -}++  -- ** Related to a node+  isTrueNode, isInNode, isInNodeByEnv, isOutNode, isNodeConsistentWith,+  getNodeIsAssumption, getNodeIsContradictory, {- explainNode, -}++  -- ** Related to environments+  envIsNogood,++  -- * Printing and debugging++  -- |Functions prefixed @format@ build a computation returning a+  -- `String`.  Functions prefixed @debug@ or @print@ build a unit+  -- computation printing the artifact in question to standard output;+  -- those with prefix @debug@ are generally more verbose.+  debugAtms, printAtms, debugAtmsEnvs,+  printAtmsStatistics,++  -- ** Nodes and node lists+  formatNode, formatNodes, debugNode, printNode,+  whyNodes, whyNode,++  -- ** Environments, labels, and tables+  debugEnv, debugEnvTable, formatNodeLabel,+  debugNogoods,+  printEnv, printNogoods, printEnvs, printEnvTable, printTable,++  -- ** Justifications+  debugJust, printJust, formatJustification++  ) where++import Control.Monad.State+import Control.Monad.ST.Trans+-- import Control.Monad.Except+import Control.Monad.Trans.Except+import Control.Monad.Extra+import Data.List+import Data.Symbol+import Data.TMS.Helpers+import Data.TMS.MList+import Data.TMS.Dbg+++-- * The @ATMST@ monad transformer+--+-- Construction and manipulation of a ATMS happens inside this monad+-- wrapper.++-- |Errors which can arise from ATMS operations.+data AtmsErr = CannotRemoveNodeWIthConsequences String Int+               -- ^ It is not possible to remove a `Node` from an+               -- `ATMS` after a `JustRule` which uses that `Node` is+               -- added to the `ATMS`.+             | InternalNoEmptyEnv+               -- ^ Internal error called when there is no internal+               -- default empty `Env` associated with this `ATMS`.+               -- Should never be signaled for an `ATMS` created with+               -- `createATMS`, since this latter function does set up+               -- the default empty environment before returning the+               -- new `ATMS`.+             | InternalNoContraNode+               -- ^ Internal error called when there is no internal+               -- default contradictory `Node` associated with this+               -- `ATMS`.  Should never be signaled for an `ATMS`+               -- created with `createATMS`, since this latter+               -- function does set up the default contradiction node+               -- before returning the new `ATMS`.+             | UnexpectedNonruleJustification+               -- ^ Indicates that a `Justification` other than+               -- `ByRule` `JustRule` was found, specifically in a+               -- `removeNode` call.+             | FromMonadFail String+               -- ^ Indicates a pattern-matching failure within an+               -- `ATMST` operation.+  deriving Show++{- ===== Internal state of an ATMST. =================================== -}++-- |Internal state of an ATMST process+data AtmstState = AtmstState {+  initialEnvTableAlloc :: Int,+  envTableIncr :: Int+  }++-- |Initial state of an ATMST process.+initialAtmstState :: AtmstState+initialAtmstState = AtmstState 50 75++-- |Update the initial table size of an ATMST state.+withInitialEnvTableAlloc :: AtmstState -> Int -> AtmstState+withInitialEnvTableAlloc (AtmstState _ ei) ia = AtmstState ia ei++-- |Update the table increment size of an ATMST state.+withEnvTableIncr :: AtmstState -> Int -> AtmstState+withEnvTableIncr (AtmstState ia _) ei = AtmstState ia ei++{- ===== ATMST definition. ============================================= -}++-- |The process of building and using a mutable ATMS.+type ATMSTInner s m a =+  Monad m => ExceptT AtmsErr (StateT AtmstState (STT s m)) a++-- |The process of building and using a mutable ATMS.+newtype Monad m => ATMST s m a = AtmsT { unwrap :: ATMSTInner s m a }++-- |Internal unwrapper preserving rank-2 polymorphism of the state+-- thread in the wrapper `STT`.+unwrap2 :: Monad m => (forall s . ATMST s m a) -> (forall s . ATMSTInner s m a)+unwrap2 (AtmsT m) = m++instance (Monad m) => Functor (ATMST s m) where+  fmap f (AtmsT m) = AtmsT $ do+    v <- m+    return $ f v++instance (Monad m, Functor m) => Applicative (ATMST s m) where+  pure v = AtmsT $ pure v+  (AtmsT m1) <*> (AtmsT m2) = AtmsT $ do+    f <- m1+    v <- m2+    return (f v)++instance (Monad m, Functor m) => Monad (ATMST s m) where+  -- (>>=) :: ATMST s m a -> (a -> ATMST s m b) -> ATMST s m b+  (AtmsT m) >>= f = AtmsT $ m >>= (unwrap . f)++  -- (>>) :: ATMST s m a -> ATMST s m b -> ATMST s m b+  (AtmsT m1) >> (AtmsT m2) = AtmsT $ m1 >> m2++  -- return :: a -> ATMST s m a+  return v = AtmsT $ return v++instance MonadTrans (ATMST s) where+  lift m = AtmsT $ lift $ lift $ lift m++instance MonadIO m => MonadIO (ATMST s m) where+  liftIO = lift . liftIO++-- |Lift `STT` behavior to the `ATMST` level.+sttLayer :: Monad m => STT s m r -> ATMST s m r+sttLayer md = AtmsT $ lift $ lift $ md++-- |Lift `ExceptT` behavior to the `ATMST` level.+exceptLayer ::+  Monad m => ExceptT AtmsErr (StateT AtmstState (STT s m)) r -> ATMST s m r+exceptLayer = AtmsT++-- |Lift `StateT` behavior to the `ATMST` level.+stateLayer ::+  Monad m => StateT AtmstState (STT s m) r -> ATMST s m r+stateLayer = AtmsT . lift++instance Monad m => MonadFail (ATMST s m) where+  fail s = exceptLayer $ throwE $ FromMonadFail s++-- |Retrieve the current initial `Env` table size setting.+getInitialEnvTableAlloc :: Monad m => ATMST s m Int+getInitialEnvTableAlloc = stateLayer $ fmap initialEnvTableAlloc get++-- |Retrieve the current initial `Env` table size setting.+setInitialEnvTableAlloc :: Monad m => Int -> ATMST s m ()+setInitialEnvTableAlloc ia = stateLayer $ modify (`withInitialEnvTableAlloc` ia)++-- |Retrieve the current initial `Env` table size setting.+getEnvTableIncr :: Monad m => ATMST s m Int+getEnvTableIncr = stateLayer $ fmap envTableIncr get++-- |Retrieve the current initial `Env` table size setting.+setEnvTableIncr :: Monad m => Int -> ATMST s m ()+setEnvTableIncr ia = stateLayer $ modify (`withEnvTableIncr` ia)++-- |Execute a computation in the `ATMST` monad transformer.+runATMST :: Monad m => (forall s . ATMST s m r) -> m (Either AtmsErr r)+runATMST atmst = do+  let core = unwrap2 atmst+      afterExcept = runExceptT core+      afterState = do+        (result, endState) <- runStateT afterExcept initialAtmstState+        return result+  runSTT afterState++{- ----------------------------------------------------------------- -}++-- |Class of type which can be used as the datum underlying `Node`s in+-- an `ATMS`.+class NodeDatum d where+  -- |The datum associated with the contradiction node in a+  -- newly-initialized `ATMS` with `Node` data of this type.+  contradictionNodeDatum :: d++instance NodeDatum String where+  contradictionNodeDatum = "The contradiction"+instance NodeDatum Symbol where+  contradictionNodeDatum = intern "The contradiction"++-- |Top-level representation of an assumption-based truth maintenance+-- system.+data (Monad m, NodeDatum d) => ATMS d i r s m = ATMS {+  -- |Name of this ATMS.+  atmsTitle :: String,+  -- |Unique namer for nodes.+  atmsNodeCounter :: STRef s Int,+  -- |Unique namer for justifications.+  atmsJustCounter :: STRef s Int,+  -- |Unique namer for environments.+  atmsEnvCounter :: STRef s Int,+  -- |Current size of environment table.+  atmsEnvTableAlloc :: STRef s Int,+  -- |List of all TMS nodes.+  atmsNodes :: STRef s [Node d i r s m],+  -- |List of all justifications.+  atmsJusts :: STRef s [JustRule d i r s m],+  -- |List of all contradiction nodes.+  atmsContradictions :: STRef s [Node d i r s m],+  -- |List of all assumption nodes.+  atmsAssumptions :: STRef s [Node d i r s m],+  -- |The environment table.+  atmsEnvTable :: STRef s (EnvTable d i r s m),+  -- |The table of nogood environments.+  atmsNogoodTable :: STRef s (EnvTable d i r s m),+  -- |Canonical empty Env for this ATMS.  This value is not set more+  -- than once, but it created (by `createATMS`) after the ATMS is+  -- allocated, so we use a reference to be able to set it up later.+  atmsEmptyEnv :: STRef s (Maybe (Env d i r s m)),+  -- |Canonical contradiction `Node` for this ATMS.  This value is not+  -- set more than once, but it written (by `createATMS`) after the+  -- ATMS is allocated, so we use a reference to be able to set it up+  -- later.+  atmsContraNode :: STRef s (Maybe (Node d i r s m)),+  -- |Function for formatting a `Node` of this ATMS.+  atmsNodeString :: STRef s (Node d i r s m -> String),+  -- |Function for representing a justification rule.+  atmsJustString :: STRef s (JustRule d i r s m -> String),+  -- |Function for representing the data associated with `Node`s.+  atmsDatumString :: STRef s (d -> String),+  -- |Function for representing the informants of justifications.+  atmsInformantString :: STRef s (i -> String),+  -- |List of external procedures to be executed for this ATMS.+  atmsEnqueueProcedure :: STRef s (r -> ATMST s m ()),+  -- |Set to `True` when we wish to debug this ATMS.+  atmsDebugging :: STRef s Bool+}++-- |Shortcut maker for reading from an `ATMS` reference.+getATMSMutable ::+  (Monad m, NodeDatum d) =>+    (ATMS d i r s m -> STRef s a) -> ATMS d i r s m  -> ATMST s m a+{-# INLINE getATMSMutable #-}+getATMSMutable refGetter atms = sttLayer $ readSTRef (refGetter atms)+-- |Shortcut to write to an ATMS reference.+setATMSMutable ::+  (Monad m, NodeDatum d) =>+    (ATMS d i r s m -> STRef s a) -> ATMS d i r s m -> a -> ATMST s m ()+{-# INLINE setATMSMutable #-}+setATMSMutable refGetter atms envs =+  sttLayer $ writeSTRef (refGetter atms) envs++-- |Return the `ATMS`'s current `Node` list.+getNodes ::+  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m [Node d i r s m]+{-# INLINE getNodes #-}+getNodes = getATMSMutable atmsNodes++-- |Return the `ATMS`'s current `EnvTable`.+getEnvTable ::+  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (EnvTable d i r s m)+{-# INLINE getEnvTable #-}+getEnvTable = getATMSMutable atmsEnvTable++-- |Return the `ATMS`'s current `EnvTable` for nogood `Env`s.+getNogoodTable ::+  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (EnvTable d i r s m)+{-# INLINE getNogoodTable #-}+getNogoodTable = getATMSMutable atmsNogoodTable++-- |Return the `ATMS`'s current `JustRule` list.+getJusts ::+  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m [JustRule d i r s m]+{-# INLINE getJusts #-}+getJusts = getATMSMutable atmsJusts++-- |Return the `ATMS`'s current contradictions list.+getContradictions ::+  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m [Node d i r s m]+{-# INLINE getContradictions #-}+getContradictions = getATMSMutable atmsContradictions++-- |Return the `ATMS`'s current assumptions list.+getAssumptions ::+  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m [Node d i r s m]+{-# INLINE getAssumptions #-}+getAssumptions = getATMSMutable atmsAssumptions++-- |Return the `ATMS`'s built-in empty environment.+getEmptyEnvironment ::+  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (Env d i r s m)+{-# INLINE getEmptyEnvironment #-}+getEmptyEnvironment atms = do+  maybeEnv <- getATMSMutable atmsEmptyEnv atms+  case maybeEnv of+    Just env -> return env+    Nothing -> exceptLayer $ throwE InternalNoEmptyEnv++-- |Return the `ATMS`'s built-in contradiction node.+getContradictionNode ::+  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (Node d i r s m)+{-# INLINE getContradictionNode #-}+getContradictionNode atms = do+  maybeNode <- getATMSMutable atmsContraNode atms+  case maybeNode of+    Just node -> return node+    Nothing -> exceptLayer $ throwE InternalNoContraNode++-- |Return the `ATMS`'s current `Node` formatter.+getNodeString ::+  (Monad m, NodeDatum d) =>+    ATMS d i r s m -> ATMST s m (Node d i r s m -> String)+{-# INLINE getNodeString #-}+getNodeString = getATMSMutable atmsNodeString+-- |Shortcut to write to the reference to a ATMS's `Node` formatter.+setNodeString ::+  (Monad m, NodeDatum d) =>+    ATMS d i r s m -> (Node d i r s m -> String) -> ATMST s m ()+{-# INLINE setNodeString #-}+setNodeString = setATMSMutable atmsNodeString++-- |Return the `ATMS`'s current `JustRule` formatter.+getJustString ::+  (Monad m, NodeDatum d) =>+    ATMS d i r s m -> ATMST s m (JustRule d i r s m -> String)+{-# INLINE getJustString #-}+getJustString = getATMSMutable atmsJustString+-- |Shortcut to write to the reference to a ATMS's `JustRule` formatter.+setJustString ::+  (Monad m, NodeDatum d) =>+    ATMS d i r s m -> (JustRule d i r s m -> String) -> ATMST s m ()+{-# INLINE setJustString #-}+setJustString = setATMSMutable atmsJustString++-- |Return the `ATMS`'s current datum formatter.+getDatumString ::+  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (d -> String)+{-# INLINE getDatumString #-}+getDatumString = getATMSMutable atmsDatumString+-- |Shortcut to write to the reference to a ATMS's datum formatter.+setDatumString ::+  (Monad m, NodeDatum d) => ATMS d i r s m -> (d -> String) -> ATMST s m ()+{-# INLINE setDatumString #-}+setDatumString = setATMSMutable atmsDatumString++-- |When the data associated with `Node`s are all `String`s, we can+-- direct the `ATMS` to display each datum as itself.+setDatumStringViaString :: Monad m => ATMS String i r s m -> ATMST s m ()+setDatumStringViaString atms = setDatumString atms id++-- |When the data associated with `Node`s are of a type of class+-- `Show`, we can direct the `ATMS` to display each datum using the+-- `show` instance.+setDatumStringViaShow ::+  (NodeDatum d, Show d, Monad m) => ATMS d i r s m -> ATMST s m ()+setDatumStringViaShow atms = setDatumString atms show++-- |Return the `ATMS`'s current informant formatter.+getInformantString ::+  (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (i -> String)+{-# INLINE getInformantString #-}+getInformantString = getATMSMutable atmsInformantString+-- |Shortcut to write to the reference to a ATMS's informant formatter.+setInformantString ::+  (Monad m, NodeDatum d) => ATMS d i r s m -> (i -> String) -> ATMST s m ()+{-# INLINE setInformantString #-}+setInformantString = setATMSMutable atmsInformantString++-- |When the informants associated with `JustRule`s are all+-- `String`s, we can direct the `ATMS` to display each informant as+-- itself.+setInformantStringViaString ::+  (Monad m, NodeDatum d) => ATMS d String r s m -> ATMST s m ()+setInformantStringViaString atms = setInformantString atms id++-- |When the informants associated with `JustRule`s are of a type of+-- class `Show`, we can direct the `ATMS` to display each datum using+-- the `show` instance.+setInformantStringViaShow ::+  (Show i, Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()+setInformantStringViaShow atms = setInformantString atms show++-- |Return the `ATMS`'s current rule-queueing procedure.+getEnqueueProcedure ::+  (Monad m, NodeDatum d) =>+    ATMS d i r s m -> ATMST s m (r -> ATMST s m ())+{-# INLINE getEnqueueProcedure #-}+getEnqueueProcedure = getATMSMutable atmsEnqueueProcedure+-- |Shortcut to write to the reference to a ATMS's rule-queueing procedure.+setEnqueueProcedure ::+  (Monad m, NodeDatum d) =>+    ATMS d i r s m -> (r -> ATMST s m ()) -> ATMST s m ()+{-# INLINE setEnqueueProcedure #-}+setEnqueueProcedure = setATMSMutable atmsEnqueueProcedure++-- |Print the internal title signifying an ATMS.+--+-- Translated from @print-atms@ in @atms.lisp@.+printAtms :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()+printAtms atms = liftIO $ putStrLn $ "#<ATMS: " ++ atmsTitle atms ++ ">"++-- |Get the next node counter value, incrementing for future accesses.+nextNodeCounter :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m Int+nextNodeCounter jtms = sttLayer $ do+  let nodeCounter = atmsNodeCounter jtms+  nodeId <- readSTRef nodeCounter+  writeSTRef nodeCounter $ 1 + nodeId+  return nodeId++-- |Get the next justification rule counter value, incrementing for+-- future accesses.+nextJustCounter :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m Int+nextJustCounter atms = sttLayer $ do+  let justCounter = atmsJustCounter atms+  justId <- readSTRef justCounter+  writeSTRef justCounter $ 1 + justId+  return justId++-- |Get the next environment rule counter value, incrementing for+-- future accesses.+nextEnvCounter :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m Int+nextEnvCounter atms = sttLayer $ do+  let envCounter = atmsEnvCounter atms+  envId <- readSTRef envCounter+  writeSTRef envCounter $ 1 + envId+  return envId++{- ----------------------------------------------------------------- -}++-- |Wrapper for the datum associated with a node of the `ATMS`.+--+-- Translated from @(tms-node@ in @atms.lisp@.+data (Monad m, NodeDatum d) => Node d i r s m = Node {+  nodeIndex :: Int,+  -- |Retrieve the datum associated with a `Node`.+  nodeDatum :: d,+  nodeLabel :: STRef s [Env d i r s m],+  nodeJusts :: STRef s [Justification d i r s m],+  nodeConsequences :: STRef s [JustRule d i r s m],+  nodeIsContradictory :: STRef s Bool,+  nodeIsAssumption :: STRef s Bool,+  nodeRules :: STRef s [r],+  -- |Retrieve the `ATMS` associated with a `Node`.+  nodeATMS :: ATMS d i r s m+}++instance (Monad m, NodeDatum d) => Eq (Node d i r s m) where+  n1 == n2 = nodeIndex n1 == nodeIndex n2++instance (Monad m, NodeDatum d) => Ord (Node d i r s m) where+  n1 < n2 = nodeIndex n1 < nodeIndex n2+  n1 `compare` n2 = nodeIndex n1 `compare` nodeIndex n2++instance (Monad m, NodeDatum d) => Show (Node d i r s m) where+  show n = "<Node " ++ show (nodeIndex n) ++ ">"++-- |Shortcut maker for reading from a `Node` reference.+getNodeMutable ::+  (Monad m, NodeDatum d) =>+    (Node d i r s m -> STRef s a) -> Node d i r s m  -> ATMST s m a+{-# INLINE getNodeMutable #-}+getNodeMutable refGetter node = sttLayer $ readSTRef (refGetter node)+-- |Shortcut to write to the reference to a node's label.+setNodeMutable ::+  (Monad m, NodeDatum d) =>+    (Node d i r s m -> STRef s a) -> Node d i r s m -> a -> ATMST s m ()+{-# INLINE setNodeMutable #-}+setNodeMutable refGetter node val = sttLayer $ writeSTRef (refGetter node) val++-- |Return the `Node`'s label.+getNodeLabel ::+  (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m [Env d i r s m]+{-# INLINE getNodeLabel #-}+getNodeLabel = getNodeMutable nodeLabel+-- |Shortcut to write to the reference to a node's label.+setNodeLabel ::+  (Monad m, NodeDatum d) => Node d i r s m -> [Env d i r s m] -> ATMST s m ()+{-# INLINE setNodeLabel #-}+setNodeLabel = setNodeMutable nodeLabel++-- |Return the `Node`'s rules.+getNodeRules :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m [r]+{-# INLINE getNodeRules #-}+getNodeRules = getNodeMutable nodeRules+-- |Shortcut to write to the reference to a node's rules.+setNodeRules :: (Monad m, NodeDatum d) => Node d i r s m -> [r] -> ATMST s m ()+{-# INLINE setNodeRules #-}+setNodeRules = setNodeMutable nodeRules++-- |Return the `JustRule`s concluding a `Node`.+getNodeJusts ::+  (Monad m, NodeDatum d) =>+    Node d i r s m -> ATMST s m [Justification d i r s m]+{-# INLINE getNodeJusts #-}+getNodeJusts = getNodeMutable nodeJusts++-- |Return the `Node`'s consequences.+getNodeConsequences ::+  (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m [JustRule d i r s m]+{-# INLINE getNodeConsequences #-}+getNodeConsequences = getNodeMutable nodeConsequences+-- |Shortcut to write to the reference to a node's consequences.+setNodeConsequences ::+  (Monad m, NodeDatum d) =>+    Node d i r s m -> [JustRule d i r s m] -> ATMST s m ()+{-# INLINE setNodeConsequences #-}+setNodeConsequences = setNodeMutable nodeConsequences++-- |Return whether the `Node`'s is currently contradictory.+getNodeIsContradictory ::+  (Monad m, NodeDatum d) => Node d i r s m  -> ATMST s m Bool+getNodeIsContradictory node = sttLayer $ readSTRef (nodeIsContradictory node)++-- |Set whether a `Node`'s is currently contradictory.+setNodeIsContradictory ::+  (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m ()+setNodeIsContradictory node =+  sttLayer $ writeSTRef (nodeIsContradictory node) True++-- |Return whether the `Node`'s is currently markable as an assumption.+getNodeIsAssumption ::+  (Monad m, NodeDatum d) => Node d i r s m  -> ATMST s m Bool+getNodeIsAssumption node = sttLayer $ readSTRef (nodeIsAssumption node)++-- |The justification of one `ATMS` `Node` by zero or more others.+data (Monad m, NodeDatum d) => JustRule d i r s m = JustRule {+  justIndex :: Int,+  -- |The informant associated with applying this inference rule.+  justInformant :: i,+  -- |The conclusion of this inference rule.+  justConsequence :: Node d i r s m,+  -- |The antecedents of this inference rule.+  justAntecedents :: [Node d i r s m]+}++instance (Monad m, NodeDatum d) => Eq (JustRule d i r s m) where+  e1 == e2 = (justIndex e1) == (justIndex e2)++-- |Description of why a `Node` may be believed by the `ATMS`.+data Justification d i r s m =+  ByRule (JustRule d i r s m) | ByAssumption (Node d i r s m) | ByContradiction++-- |Explanation of why a `Node` may be believed by the `ATMS` for+-- output to a query.+data Explanation d i r s m =+  IsRule (JustRule d i r s m) | IsAssumption (Node d i r s m)++-- |Explanation of why a `Node` may be classified as no-good by the+-- `ATMS`.+data WhyNogood d i r s m =+  Good | ByJustification (Justification d i r s m) | ByEnv (Env d i r s m)++-- |Translation of the explanation of why a `Node` may be classified+-- (or not) as no-good to a boolean value.+isNogood :: WhyNogood d i r s m -> Bool+isNogood Good = False+isNogood _ = True++{- ----------------------------------------------------------------- -}++-- |An environment of `Node`s which may be used as the basis of+-- reasoning in an `ATMS`.+data (Monad m, NodeDatum d) => Env d i r s m = Env {+  -- |The unique nomber of this `Env` within its `ATMS`.+  envIndex :: Int,+  -- |The number of assumptions contained within this `Env`.+  envCount :: Int,+  -- |The assumptions contained within this `Env`.+  envAssumptions :: [Node d i r s m],+  envNodes :: STRef s [Node d i r s m],+  envWhyNogood :: STRef s (WhyNogood d i r s m),+  envRules :: STRef s [r]+}++instance (Monad m, NodeDatum d) => Eq (Env d i r s m) where+  e1 == e2 = (envIndex e1) == (envIndex e2)++instance (Monad m, NodeDatum d) => Show (Env d i r s m) where+  show n = "<Env " ++ show (envIndex n) ++ ">"++-- |Shortcut maker for reading from a `Env` reference.+getEnvMutable ::+  (Monad m, NodeDatum d) =>+    (Env d i r s m -> STRef s a) -> Env d i r s m  -> ATMST s m a+{-# INLINE getEnvMutable #-}+getEnvMutable refGetter env = sttLayer $ readSTRef (refGetter env)+-- |Shortcut to write to the reference to a env's label.+setEnvMutable ::+  (Monad m, NodeDatum d) =>+    (Env d i r s m -> STRef s a) -> Env d i r s m -> a -> ATMST s m ()+{-# INLINE setEnvMutable #-}+setEnvMutable refGetter env envs = sttLayer $ writeSTRef (refGetter env) envs++-- |Shortcut for reading the `Node`s of an `Env`.+getEnvNodes ::+  (Monad m, NodeDatum d) => Env d i r s m  -> ATMST s m [Node d i r s m]+getEnvNodes = getEnvMutable envNodes+-- |Shortcut for writing the `Node`s of an `Env`.+setEnvNodes ::+  (Monad m, NodeDatum d) => Env d i r s m  -> [Node d i r s m] -> ATMST s m ()+setEnvNodes = setEnvMutable envNodes++-- |Shortcut for reading the rules of an `Env`.+getEnvRules :: (Monad m, NodeDatum d) => Env d i r s m  -> ATMST s m [r]+getEnvRules = getEnvMutable envRules+-- |Shortcut for writing the rules of an `Env`.+setEnvRules :: (Monad m, NodeDatum d) => Env d i r s m  -> [r] -> ATMST s m ()+setEnvRules = setEnvMutable envRules++-- |Shortcut for testing whether an `Env` is nogood.+envIsNogood :: (Monad m, NodeDatum d) => Env d i r s m -> ATMST s m Bool+envIsNogood env = do+  fmap isNogood $ sttLayer $ readSTRef $ envWhyNogood env++-- |Type alias for the array storage of a table of `Env`s arranged by+-- length.+newtype EnvTable d i r s m = EnvTable (STArray s Int [Env d i r s m])++findInEnvTable ::+  (Monad m, NodeDatum d) =>+    (Env d i r s m -> Bool) -> EnvTable d i r s m ->+      ATMST s m (Maybe (Env d i r s m))+findInEnvTable pred (EnvTable arr) =+  let (lo, hi) = boundsSTArray arr+  in findInEnvTableEntries pred  [lo..hi] arr+  where findInEnvTableEntries ::+          Monad m =>+            (Env d i r s m -> Bool) -> [Int] -> STArray s Int [Env d i r s m] ->+              ATMST s m (Maybe (Env d i r s m))+        findInEnvTableEntries pred [] arr = return Nothing+        findInEnvTableEntries pred (i : idxs) arr = do+          entries <- sttLayer $ readSTArray arr i+          case find pred entries of+            Nothing -> findInEnvTableEntries pred idxs arr+            res -> return res++        findInEnvTableEntry ::+          Monad m =>+            (Env d i r s m -> Bool) -> [Env d i r s m] -> Maybe (Env d i r s m)+        findInEnvTableEntry pred envs = find pred envs++-- |Shortcut for retrieving the `Node` formatter from an `ATMS`, and+-- applying it to the given `Node`.+--+-- Translated from @node-string@ in @atms.lisp@.+nodeString :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String+nodeString node = do+  nodeFmt <- getNodeString $ nodeATMS node+  return $ nodeFmt node++-- |Default formatter for the `Node`s of an `ATMS`.+--+-- Translated from @default-node-string@ in @atms.lisp@.+defaultNodeString ::+  (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String+defaultNodeString node = do+  datumFormatter <- getDatumString $ nodeATMS node+  return $ datumFormatter $ nodeDatum node++-- |Insert an element into a sorted list.+--+-- Translated from @ordered-insert@ in @atms.lisp@.+orderedInsert :: Eq a => a -> [a] -> (a -> a -> Bool) -> [a]+orderedInsert item [] _ = [item]+orderedInsert item list@(i : _) test | test item i  = item : list+orderedInsert item list@(i : _) _    | item == i    = list+orderedInsert item (i : is) test = i : orderedInsert item is test++{- Does not seem to be used+-- Translated from @ordered-push@ in @atms.lisp@.+--+-- > ;; In atms.lisp+-- > (defmacro ordered-push (item list test)+-- >   `(setq ,list (ordered-insert ,item ,list ,test)))+orderedPush :: a -> [a] -> (a -> a -> Bool) -> [a]+orderedPush = error "< unimplemented orderedPush >"+-}++-- |We order assumptions in `Env` lists by their index.+--+-- Translated from @assumption-order@ in @atms.lisp@.+assumptionOrder ::+  (Monad m, NodeDatum d) => Node d i r s m -> Node d i r s m -> Bool+assumptionOrder n1 n2 = nodeIndex n1 < nodeIndex n2++-- Ordering predicate for two `Env`s; uses their internal index.+--+-- Translated from @env-order@ in @atms.lisp@.+envOrder :: (Monad m, NodeDatum d) => Env d i r s m -> Env d i r s m -> Bool+envOrder e1 e2 = envIndex e1 < envIndex e2++{- ----------------------------------------------------------------- -}++-- * Basic inference engine interface.++-- |Create a new, empty ATMS.+--+-- Translated from @create-atms@ in @atms.lisp@.+createATMS ::+  (Debuggable m, NodeDatum d) => String -> ATMST s m (ATMS d i r s m)+createATMS title = do+  ecInitialAlloc <- getInitialEnvTableAlloc+  emptyEnvRef <- sttLayer $ newSTRef Nothing+  contraNodeRef <- sttLayer $ newSTRef Nothing+  result <- sttLayer $ do+    nc <- newSTRef 0+    jc <- newSTRef 0+    ec <- newSTRef 0+    etAlloc <- newSTRef ecInitialAlloc+    nodes <- newSTRef ([] :: [Node d i r s m])+    justs <- newSTRef ([] :: [JustRule d i r s m])+    contradictions <- newSTRef ([] :: [Node d i r s m])+    assumptions <- newSTRef ([] :: [Node d i r s m])+    etable <- newSTArray (0, ecInitialAlloc) []+    etableRef <- newSTRef (EnvTable etable)+    ngtable <- newSTArray (0, ecInitialAlloc) []+    ngtableRef <- newSTRef (EnvTable ngtable)+    nodeString <- newSTRef (show . nodeIndex)+    justString <- newSTRef (show . justIndex)+    datumString <- newSTRef (\ datum -> "?")+    informantString <- newSTRef (\ inf -> "?")+    enqueueProcedure <- newSTRef (\ _ -> return ())+    debugging <- newSTRef False+    return $ ATMS title nc jc ec etAlloc+                  nodes justs contradictions assumptions+                  etableRef ngtableRef emptyEnvRef contraNodeRef+                  nodeString justString datumString informantString+                  enqueueProcedure debugging+  emptyEnv <- createEnv result []+  sttLayer $ writeSTRef emptyEnvRef (Just emptyEnv)+  contra <- createNode result contradictionNodeDatum False True+  sttLayer $ writeSTRef contraNodeRef (Just contra)+  return result++{- ----------------------------------------------------------------- -}++-- |Returns `True` if the given `Node` is axiomatic, following from+-- the assumption of zero other nodes.+--+-- Translated from @true-node?@ in @atms.lisp@.+isTrueNode :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m Bool+isTrueNode node = do+  envs <- getNodeLabel node+  return $ case envs of+    [] -> False+    e : _ -> null $ envAssumptions e++-- |Returns `True` if the given `Node` is justified by some labelling+-- `Env`ironment of `Node`s in the `ATMS`.+--+-- Translated from @in-node?@ in @atms.lisp@.+isInNode :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m Bool+isInNode node = fmap (not . null) (getNodeLabel node)++-- |Returns `True` if the given `Node` is justified by some subset of+-- the given environment in the `ATMS`.+--+-- Translated from @in-node?@ in @atms.lisp@.+isInNodeByEnv ::+  (Monad m, NodeDatum d) => Node d i r s m -> Env d i r s m -> ATMST s m Bool+isInNodeByEnv node env = do+  labelEnvs <- getNodeLabel node+  return $ any (\ le -> isSubsetEnv le env) labelEnvs++-- |Returns `True` if the given `Node` is justified by no labelling+-- `Env`ironment of `Node`s in the `ATMS`.+--+-- Translated from @out-node?@ in @atms.lisp@.+isOutNode ::+  (Monad m, NodeDatum d) => Node d i r s m -> Env d i r s m -> ATMST s m Bool+isOutNode node env = fmap not $ isInNodeByEnv node env++-- |Returns `True` if some environment justifying the given `Node` is+-- consistent with the given environment, where two environments are+-- consistent when their union is not no-good.+--+-- Translated from @node-consistent-with?@ in @atms.lisp@.+isNodeConsistentWith ::+  (Monad m, NodeDatum d) => Node d i r s m -> Env d i r s m -> ATMST s m Bool+isNodeConsistentWith node env = do+  labelEnvs <- getNodeLabel node+  anyByM (\ le -> do+             union <- unionEnv le env+             fmap not $ envIsNogood union)+    labelEnvs++-- |Create a new `Node` in an `ATMS`.+--+-- Translated from @create-node@ in @atms.lisp@.+createNode :: (Debuggable m, NodeDatum d) =>+  ATMS d i r s m -> d -> Bool -> Bool -> ATMST s m (Node d i r s m)+createNode atms datum isAssumption isContradictory = do+  idx <- nextNodeCounter atms+  label <- sttLayer $ newSTRef []+  justs <- sttLayer $ newSTRef []+  conseq <- sttLayer $ newSTRef []+  assumptionFlag <- sttLayer $ newSTRef isAssumption+  contraFlag <- sttLayer $ newSTRef isContradictory+  rules <- sttLayer $ newSTRef []+  let node = Node idx datum label justs conseq+                  contraFlag assumptionFlag rules atms+  sttLayer $ do+    push node $ atmsNodes atms+    when isContradictory $ push node $ atmsContradictions atms+  when isAssumption $ do+    selfEnv <- createEnv atms [node]+    sttLayer $ do+      push node $ atmsAssumptions atms+      push selfEnv $ nodeLabel node+  return node++-- |Mark the given `Node` as to be believed as an assumption by its+-- `ATMS`.+--+-- Translated from @assume-node@ in @atms.lisp@.+assumeNode :: (Debuggable m, NodeDatum d) => Node d i r s m -> ATMST s m ()+assumeNode node =+  unlessM (getNodeIsAssumption node) $ do+    let atms = nodeATMS node+    sttLayer $ push node (atmsAssumptions atms)+    selfEnv <- findOrMakeEnv [node] atms+    nodes <- sttLayer $ toMList [Just selfEnv]+    update nodes node (ByAssumption node)++-- |Mark the given `Node` as an additional contradiction node of the+-- `ATMS`.+--+-- Translated from @make-contradiction@ in @atms.lisp@.+makeContradiction :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m ()+makeContradiction node = do+  let atms = nodeATMS node+  unlessM (getNodeIsContradictory node) $ do+    setNodeIsContradictory node+    sttLayer $ push node $ atmsContradictions atms+    whileDoWith (getNodeLabel node) (not . null) $ \ (env : _) ->+      newNogood atms env ByContradiction++-- |Direct the `ATMS` to believe a particular `Node` when all of the+-- given list of `Node`s are also believed.  The first argument is the+-- informant associated with this inference.+--+-- Translated from @justify-node@ in @atms.lisp@.+justifyNode ::+  (Debuggable m, NodeDatum d) =>+    i -> Node d i r s m -> [Node d i r s m] -> ATMST s m ()+justifyNode informant consequence antecedents = do+  -- Retrieve the ATMS in which we are working+  let atms = nodeATMS consequence++  -- Number and create a new justification record.+  idx <- nextJustCounter atms+  let just = JustRule idx informant consequence antecedents++  -- Register the new justification with the node it can imply.+  sttLayer $ push (ByRule just) (nodeJusts consequence)++  -- Register the new justification with the nodes that can trigger+  -- it.+  sttLayer $ forM_ antecedents $ \node -> push just $ nodeConsequences node++  -- Register the new justification with the ATMS itself.+  sttLayer $ push just $ atmsJusts atms++  -- Introduce the new justification+  emptyEnv <- getEmptyEnvironment atms+  envListRef <- sttLayer $ fromListMap Just [emptyEnv]+  propagate just Nothing envListRef++-- |Direct the `ATMS` to find the combination of all of the given+-- `Node`s to be a contradiction associated with the given informant.+--+-- Translated from @nogood-nodes@ in @atms.lisp@.+nogoodNodes :: (Monad m, NodeDatum d) => i -> [Node d i r s m] -> ATMST s m ()+nogoodNodes informant nodes = do+  contra <- getContradictionNode (nodeATMS (head nodes))+  justifyNode informant contra nodes++-- * Label updating++--+-- Translated from @propagate@ in @atms.lisp@.+propagate ::+  (Debuggable m, NodeDatum d) =>+    JustRule d i r s m ->+      Maybe (Node d i r s m) ->+        MList s (Maybe (Env d i r s m)) ->+          ATMST s m ()+propagate just antecedent envs = do+  $(dbg [| debugPropagateArgs just antecedent envs |])+  newEnvs <- weave antecedent envs (justAntecedents just)+  when (not (mnull newEnvs)) $ do+    update newEnvs (justConsequence just) (ByRule just)++debugPropagateArgs ::+  (MonadIO m, NodeDatum d) =>+    JustRule d i r s m ->+      Maybe (Node d i r s m) ->+        MList s (Maybe (Env d i r s m)) ->+          ATMST s m ()+debugPropagateArgs justRule antecedent envs = do+  liftIO $ putStrLn "Calling propagate with"+  let atms = nodeATMS $ justConsequence justRule+  liftIO $ putStr ". Just: "+  debugJust justRule++  case antecedent of+    Just n -> debugNode n+    Nothing -> liftIO $ putStrLn ". No antecedent"++  envLen <- sttLayer $ mlength envs+  case envLen of+    0 -> liftIO $ putStrLn ". No envs"+    1 -> do+      liftIO $ putStrLn ". Env: "+      envm <- sttLayer $ mcar envs+      case envm of+        Nothing -> liftIO $ putStrLn "<nulled out>"+        Just env -> debugEnv env+    _ -> do+      liftIO $ putStrLn ". Envs:"+      mlistFor_ sttLayer envs $ \em -> do+        liftIO $ putStr "  . "+        case em of+          Just e -> debugEnv e+          Nothing -> liftIO $ putStrLn "<nulled out>"++--+-- Translated from @update@ in @atms.lisp@.+update ::+  (Debuggable m, NodeDatum d) =>+    MList s (Maybe (Env d i r s m)) ->+      Node d i r s m ->+        Justification d i r s m ->+          ATMST s m ()+update newEnvs consequence just = do+  $(dbg [| debugUpdateArgs newEnvs consequence just |])+  let atms = nodeATMS consequence++  -- If the consequence node is a contradiction, then all we need to+  -- do is mark all of the environments implying it as contradictory+  -- as well.+  ifM (getNodeIsContradictory consequence)+    (mlistFor_ sttLayer newEnvs $ \ envmaybe ->+        case envmaybe of+          Nothing -> return ()+          Just env -> newNogood atms env just) $++    -- Otherwise we propagate further.  If this step prunes out all+    -- `Env`s from the `newEnvs`, then we have nothing further to do.+    do revNewEnvs <- updateLabel consequence newEnvs+       newEnvsRef <- sttLayer $ newSTRef $ revNewEnvs+       ifM (sttLayer $ getMnull newEnvsRef) (return ()) $ do++         -- Process rules queued in the consequence.+         enqueuef <- getEnqueueProcedure atms+         forMM_ (getNodeRules consequence) $ enqueuef++         -- Propagate to the justification rules which might depend on+         -- this node.  If ever the new Env list we are accumulating is+         -- paired down to the empty list, then we can exit these loops.+         forMMwhile_ (getNodeConsequences consequence)+           (sttLayer $ notM $ getMnull newEnvsRef) $ \ supportedJust -> do+             currentNewEnvs <- sttLayer $ readSTRef newEnvsRef+             propagate supportedJust (Just consequence) newEnvs+             mlistForCons_ sttLayer newEnvs $ \ mcons -> do+               thisEnvMaybe <- sttLayer $ mcar mcons+               case thisEnvMaybe of+                 Just thisEnv -> do+                   label <- getNodeLabel consequence+                   unless (elem thisEnv label) $+                     sttLayer $ rplaca mcons Nothing+                 Nothing -> return ()+               cleanedNewEnvs <- sttLayer $ getMlistStripNothing newEnvsRef+               sttLayer $ writeSTRef newEnvsRef cleanedNewEnvs++debugUpdateArgs ::+  (MonadIO m, NodeDatum d) =>+    MList s (Maybe (Env d i r s m)) ->+      Node d i r s m ->+        JustRule d i r s m ->+          ATMST s m ()+debugUpdateArgs envs consequence justRule = do+  liftIO $ putStrLn "Calling update with"+  let atms = nodeATMS $ justConsequence justRule++  envLen <- sttLayer $ mlength envs+  case envLen of+    0 -> liftIO $ putStrLn ". No envs"+    1 -> do+      liftIO $ putStr ". Env: "+      envm <- sttLayer $ mcar envs+      case envm of+        Nothing -> liftIO $ putStrLn "<nulled out>"+        Just env -> debugEnv env+    _ -> do+      liftIO $ putStrLn ". Envs:"+      mlistFor_ sttLayer envs $ \em -> do+        liftIO $ putStr "  . "+        case em of+          Just e -> debugEnv e+          Nothing -> liftIO $ putStrLn "<nulled out>"++  liftIO $ putStr ". Consequence: "+  blurbNode consequence+  liftIO $ putStrLn ""++  liftIO $ putStr ". Just: "+  debugJust justRule++-- |Internal method to update the label of this node to include the+-- given environments.  The inclusion is not simply list extension;+-- new environments subsumed by an existing label environment will be+-- omitted, and existing label environments subsumed by a new+-- environment will be removed.+--+-- Translated from @update-label@ in @atms.lisp@.+updateLabel ::+  (Debuggable m, NodeDatum d) =>+    Node d i r s m -> MList s (Maybe (Env d i r s m)) ->+      ATMST s m (MList s (Maybe (Env d i r s m)))+updateLabel node newEnvs = do+  $(dbg [| debugUpdateLabelArgs node newEnvs |])++  -- We will edit the label of this node, so we extract it as a+  -- mutable list, and replace it at the end of this function.+  envsR <- do labels <- getNodeLabel node+              envs <- sttLayer $ fromListMap Just labels+              sttLayer $ newSTRef envs++  -- These two loops traverse respectively the given newEnvs, and the+  -- node label environments, to find pairs of environments where one+  -- of the pair is a subset of the other.+  mlistForCons_ sttLayer newEnvs $ \ newEnvCons -> do+    newEnvCarMaybe <- sttLayer $ mcar newEnvCons+    case newEnvCarMaybe of+      Nothing -> return ()+      Just newEnvCar -> do++        thisEnvs <- sttLayer $ readSTRef envsR+        mlistForCons_ sttLayer thisEnvs $ \ nenvCons -> do+          nenvCarMaybe <- sttLayer $ mcar nenvCons+          case nenvCarMaybe of+            Nothing -> return ()+            Just nenvCar -> do+               case compareEnv newEnvCar nenvCar of+                EQenv -> sttLayer $ rplaca newEnvCons Nothing+                S21env -> sttLayer $ rplaca newEnvCons Nothing+                S12env -> do+                  nodeList <- getEnvNodes nenvCar+                  setEnvNodes nenvCar $ delete node nodeList+                  sttLayer $ rplaca nenvCons Nothing+                DisjEnv -> return ()++        $(dbg [| do liftIO $ putStr " >> pushing onto envs: "+                    blurbMaybeEnv newEnvCarMaybe+                    liftIO $ putStrLn "" |])+        sttLayer $ mlistRefPush newEnvCarMaybe envsR+        $(dbg [| do liftIO $ putStr " >> envs: "+                    blurbMaybeEnvMListRef envsR+                    liftIO $ putStrLn "" |])+        return ()++  -- Strip all `Nothing`s from the `newEnvs`, and add the `node` to+  -- each environment's node list.+  finalNewEnvs <- sttLayer $ mlistStripNothing newEnvs+  mlistFor_ sttLayer finalNewEnvs $ \ newEnvMaybe ->+    case newEnvMaybe of+      Just newEnv -> sttLayer $ push node $ envNodes newEnv  -- [B]+      _ -> return ()++  -- Un-lift the working version of the node label list, and write the+  -- update back to the node label list.+  $(dbg [| do liftIO $ putStr " >> envs: "+              blurbMaybeEnvMListRef envsR+              liftIO $ putStrLn "" |])+  envs <- sttLayer $ readSTRef envsR+  updatedLabel <- sttLayer $ toUnmaybeList envs+  $(dbg [| do liftIO $ putStr " >> updatedLabel: "+              blurbEnvList 10000 "" updatedLabel+              liftIO $ putStrLn "" |])++  -- debugNodeLabel node+  -- sttLayer $ writeSTRef (nodeLabel node) updatedLabel+  setNodeLabel node updatedLabel+  -- debugNodeLabel node++  -- Return the Nothing-stripped version of the newEnvs parameter.+  $(dbg [| debugUpdateLabelFinal node updatedLabel finalNewEnvs |])+  return finalNewEnvs++debugUpdateLabelArgs ::+  (MonadIO m, NodeDatum d) =>+    Node d i r s m -> MList s (Maybe (Env d i r s m)) -> ATMST s m ()+debugUpdateLabelArgs node newEnvs = do+  let atms = nodeATMS node++  liftIO $ putStr "Calling updateLabel with node "+  blurbNode node+  liftIO $ putStrLn ""++  envLen <- sttLayer $ mlength newEnvs+  case envLen of+    0 -> liftIO $ putStrLn ". No envs"+    1 -> do+      liftIO $ putStr ". Env: "+      envm <- sttLayer $ mcar newEnvs+      case envm of+        Nothing -> liftIO $ putStrLn "<nulled out>"+        Just env -> debugEnv env+    _ -> do+      liftIO $ putStrLn ". Envs:"+      mlistFor_ sttLayer newEnvs $ \em -> do+        liftIO $ putStr "  . "+        case em of+          Just e -> debugEnv e+          Nothing -> liftIO $ putStrLn "<nulled out>"++debugUpdateLabelFinal ::+  (MonadIO m, NodeDatum d) =>+    Node d i r s m -> [Env d i r s m] -> MList s (Maybe (Env d i r s m)) ->+      ATMST s m ()+debugUpdateLabelFinal node labelEnvs newEnvs = do++  case labelEnvs of+    [] -> liftIO $ putStrLn ". No label envs"+    [env] -> do+      liftIO $ putStr ". Single label env: "+      debugEnv env+    _ -> do+      liftIO $ putStrLn ". Final envs:"+      forM_ labelEnvs $ \e -> do+        liftIO $ putStr "  . "+        debugEnv e++  envLen <- sttLayer $ mlength newEnvs+  case envLen of+    0 -> liftIO $ putStrLn ". No final envs"+    1 -> do+      liftIO $ putStr ". Single final env: "+      envm <- sttLayer $ mcar newEnvs+      case envm of+        Nothing -> liftIO $ putStrLn "<nulled out>"+        Just env -> debugEnv env+    _ -> do+      liftIO $ putStrLn ". Final envs:"+      mlistFor_ sttLayer newEnvs $ \em -> do+        liftIO $ putStr "  . "+        case em of+          Just e -> debugEnv e+          Nothing -> liftIO $ putStrLn "<nulled out>"++  debugNode node++-- |Update the label of node @antecedent@ to include the given @envs@+-- environments, pruning environments which are a superset of another+-- included enviroment.+--+-- Implements Algorithm 12.3 of /Building Problem Solvers/.+--+-- Translated from @weave@ in @atms.lisp@.+weave :: (Debuggable m, NodeDatum d) =>+  Maybe (Node d i r s m) ->+    (MList s (Maybe (Env d i r s m))) ->+      [Node d i r s m] ->+        ATMST s m (MList s (Maybe (Env d i r s m)))+weave antecedent givenEnvs antecedents = do+  $(dbg [| debugWeaveArgs antecedent givenEnvs antecedents |])++  envsRef <- sttLayer $ newSTRef givenEnvs++  forM_ antecedents $ \node ->+    unless (maybe False (node ==) antecedent) $ do+      $(dbg [| debugWeaveNodeAntecedent node |])++      -- From loop to loop we update what's stored under envsRef, so+      -- we start this outer loop by reading what we start off with+      -- there.+      envs <- sttLayer $ readSTRef envsRef++      -- We will update envs with the list built in newEnvs.+      newEnvs <- sttLayer $ newSTRef MNil++      -- We look at all pairs of+      --  - An Env from the passed-in ENVS, plus+      --  - An Env from the NODE's label.+      -- The union of these two is NEW-ENV, and the body of the loop+      -- considers how we should incorporate NEW-ENV into NEW-ENVS.+      mlistFor_ sttLayer envs $ \envmaybe ->+        case envmaybe of+          Nothing -> return ()+          Just env -> do+            forMM_ (sttLayer $ readSTRef $ nodeLabel node) $ \nodeEnv -> do+              $(dbg [| debugWeavePairIntro env nodeEnv |])++              newEnv <- unionEnv env nodeEnv+              $(dbg [| debugWeavePairUnion newEnv |])++              -- We are not interested in nogood environments, so we+              -- skip filing the union if it is nogood.+              unlessM (envIsNogood newEnv) $ do++                -- If NEW-ENV is a superset of (or is equal to)+                -- anything already in NEW-ENVS, then NEW-ENV is+                -- redundant, and we abort the body of the inner+                -- match-searching loop without adding NEW-ENV to+                -- NEW-ENVS.+                --+                -- Otherwise if anything already in NEW-ENVS is a+                -- superset of NEW-ENV, then (1) NEW-ENV makes that+                -- element redundant, and we strip it out of NEW-ENVS;+                -- and (2) we add NEW-ENV to NEW-ENVS.++                addEnv <- sttLayer $ newSTRef True++                oldMCons <- sttLayer $ readSTRef newEnvs+                mlistForConsWhile_ sttLayer oldMCons+                                   (sttLayer $ readSTRef addEnv) $ \ cons ->+                  case cons of+                    MNil -> return () -- Should not be possible+                    mc@(MCons carRef cdrRef) -> do+                      maybeCar <- sttLayer $ readSTRef carRef+                      case maybeCar of+                        Nothing -> return ()+                        Just car ->+                          case compareEnv newEnv car of+                            EQenv  -> sttLayer $ writeSTRef addEnv False+                            S12env -> do+                              $(dbg [| debugWeaveLoopRemovingEnv car |])+                              sttLayer $ rplaca cons Nothing+                            S21env -> sttLayer $ writeSTRef addEnv False+                            DisjEnv -> return ()++                -- If we haven't found newEnv to be redundant, then+                -- add it to newEnvs.+                sttLayer $ whenM (readSTRef addEnv) $ do+                  newMCons <- mlistPush (Just newEnv) oldMCons+                  writeSTRef newEnvs newMCons+                $(dbg [| debugWeaveLoopPairEnd addEnv newEnvs |])++      -- So we have nearly produced the refinement of ENVS for this+      -- NODE in the ANTECEDENTS.  It might have spurious NILs, so we+      -- strip those out and update envsRef.+      preFinalNewEnvs <- sttLayer $ readSTRef newEnvs+      filteredNewEnvs <- sttLayer $ mlistStripNothing preFinalNewEnvs+      sttLayer $ writeSTRef envsRef filteredNewEnvs++  -- Finally, return the last refinement of ENVS.+  result <- sttLayer $ readSTRef envsRef+  $(dbg [| debugWeaveResult result |])+  return result++debugWeaveArgs :: (MonadIO m, NodeDatum d) =>+  Maybe (Node d i r s m) ->+    (MList s (Maybe (Env d i r s m))) ->+      [Node d i r s m] ->+        ATMST s m ()+debugWeaveArgs antecedent givenEnvs antecedents = do+  liftIO $ putStrLn "Calling weave with"+  case antecedent of+    Just n -> debugNode n+    Nothing -> liftIO $ putStrLn ". No antecedent"+  let atms = case antecedent of+               Just a  -> Just $ nodeATMS a+               Nothing -> case antecedents of+                            a : _ -> Just $ nodeATMS a+                            _ -> Nothing+  case atms of+    Just a -> do+      liftIO $ putStrLn ". Envs:"+      mlistFor_ sttLayer givenEnvs $ \em -> do+        liftIO $ putStr "  . "+        case em of+          Just e -> debugEnv e+          Nothing -> liftIO $ putStrLn "<nulled out>"+        return ()+    _ -> return ()++  liftIO $ putStr ". Antecedents:"+  forM_ antecedents $ \a -> do+    let atms = nodeATMS a+    datumFmt <- getDatumString atms+    liftIO $ putStr $ " " ++ datumFmt (nodeDatum a)+  liftIO $ putStrLn " "++debugWeaveNodeAntecedent antecedent = do+  datumFmt <- getDatumString (nodeATMS antecedent)+  liftIO $ putStrLn $+    " - For node antecedent " ++ datumFmt (nodeDatum antecedent)++debugWeavePairIntro ::+  (MonadIO m, NodeDatum d) => Env d i r s m -> Env d i r s m -> ATMST s m ()+debugWeavePairIntro srcEnv nodeEnv = do+  liftIO $ putStr $ "    - For "+  blurbEnv srcEnv+  liftIO $ putStr $ " from env, "+  blurbEnv nodeEnv+  liftIO $ putStrLn $ " from node label"++debugWeavePairUnion ::+  (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()+debugWeavePairUnion union = do+  liftIO $ putStr "      Union is "+  blurbEnv union+  liftIO $ putStrLn ""++debugWeaveResult ::+  (MonadIO m, NodeDatum d) => MList s (Maybe (Env d i r s m)) -> ATMST s m ()+debugWeaveResult result = do+  liftIO $ putStr " --> result of weave is "+  blurbMaybeEnvMList result+  liftIO $ putStrLn ""++debugWeaveLoopRemovingEnv ::+  (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()+debugWeaveLoopRemovingEnv env = do+  liftIO $ putStr "       - Removing from result: env "+  blurbEnv env+  liftIO $ putStrLn ""++debugWeaveLoopPairEnd ::+  (MonadIO m, NodeDatum d) =>+    STRef s Bool -> (STRef s (MList s (Maybe (Env d i r s m)))) -> ATMST s m ()+debugWeaveLoopPairEnd addR envmsR = do+  add <- sttLayer $ readSTRef addR+  liftIO $ putStrLn $ "      Adding union: " ++ (if add then "yes" else "no")+  mlist <- sttLayer $ readSTRef envmsR+  liftIO $ putStr $ "      Updated result to: "+  blurbMaybeEnvMList mlist+  liftIO $ putStrLn ""++-- Translated from @in-antecedent?@ in @atms.lisp@.+isInAntecedent :: (Monad m, NodeDatum d) => [Node d i r s m] -> ATMST s m Bool+isInAntecedent [] = return True+isInAntecedent nodes = do+  empty <- getEmptyEnvironment (nodeATMS (head nodes))+  isWeave empty nodes++-- |Check whether any union of antecedent environments is consistent.+--+-- Translated from @weave?@ in @atms.lisp@.+isWeave ::+  (Monad m, NodeDatum d) => Env d i r s m -> [Node d i r s m] -> ATMST s m Bool+isWeave _ [] = return True+isWeave env (n : ns) =+  anyMM (\e -> do+            newEnv <- unionEnv e env+            ifM (envIsNogood e) (return False) (isWeave newEnv ns))+        (getNodeLabel n)++-- |Returns `True` if the `Env`ironment argument supports all of the+-- given `Node`s.+--+-- Translated from @supporting-antecedent?@ in @atms.lisp@.+isSupportingAntecedent ::+  (Monad m, NodeDatum d) =>+    [Node d i r s m] -> Env d i r s m -> ATMST s m Bool+isSupportingAntecedent nodes env = allByM (\n -> isInNodeByEnv n env) nodes++-- |Remove a `Node` from the `ATMS`.+--+-- Translated from @remove-node@ in @atms.lisp@.+removeNode :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m ()+removeNode node = do+  let atms = nodeATMS node+  whenM (fmap (not . null) $ getNodeConsequences node) $ do+    nodeStr <- getNodeString atms+    exceptLayer $ throwE $+      CannotRemoveNodeWIthConsequences (nodeStr node) (nodeIndex node)++  let nodeRef = atmsNodes atms+   in sttLayer $ readSTRef nodeRef >>= writeSTRef nodeRef . delete node++  forRM_ sttLayer (nodeJusts node) $ \ justification ->+    case justification of+      ByRule justRule -> forM_ (justAntecedents justRule) $ \ ant -> do+        let conseqRef = nodeConsequences ant+          in sttLayer $+               readSTRef conseqRef >>= writeSTRef conseqRef . delete justRule+      _ -> exceptLayer $ throwE $ UnexpectedNonruleJustification++  forRM_ sttLayer (nodeLabel node) $ \ env -> do+    let nodesRef = envNodes env+      in sttLayer $ readSTRef nodesRef >>= writeSTRef nodesRef . delete node++-- * Creating and extending environments.++-- |Create and return a new `Env` for the given assumptions.  Note+-- that this function does not sort or otherwise organize+-- @assumptions@, and it only called with an empty or singleton list.+-- Instead, it is `consEnv` which inserts nodes in order when one+-- environement is defined in terms of another.+--+-- Translated from @create-env@ in @atms.lisp@.+createEnv ::+  (Debuggable m, NodeDatum d) =>+    ATMS d i r s m -> [Node d i r s m] -> ATMST s m (Env d i r s m)+createEnv atms assumptions = do+  $(dbg [| debugCreateEnvStart assumptions |])+  index <- nextEnvCounter atms+  whyNogood <- sttLayer $ newSTRef Good+  nodes <- sttLayer $ newSTRef []+  rules <- sttLayer $ newSTRef []+  let env = Env index (length assumptions) assumptions nodes whyNogood rules+  $(dbg [| debugCreateEnvEnv env |])+  insertInTable atms (atmsEnvTable atms) env+  $(dbg [| debugCreateEnvEnv env |])+  setEnvContradictory atms env+  $(dbg [| debugCreateEnvEnv env |])+  return env++debugCreateEnvStart ::+  (MonadIO m, NodeDatum d) => [Node d i r s m] -> ATMST s m ()+debugCreateEnvStart nodes = do+  liftIO $ putStrLn $ "             - Running createEnv"+  astr <- formatNodes "," nodes+  liftIO $ putStrLn $ "               assumptions " ++ astr++debugCreateEnvEnv ::+  (MonadIO m, NodeDatum d) => (Env d i r s m) -> ATMST s m ()+debugCreateEnvEnv env = do+  liftIO $ putStr $ "               env "+  blurbEnv env+  liftIO $ putStrLn ""++-- Translated from @union-env@ in @atms.lisp@.+unionEnv ::+  (Debuggable m, NodeDatum d) =>+    Env d i r s m -> Env d i r s m -> ATMST s m (Env d i r s m)+unionEnv e1 e2 =+  if envCount e1 > envCount e2 then unionEnv' e2 e1 else unionEnv' e1 e2+  where unionEnv' e1 e2 = do+          $(dbg [| debugUnionEnvStart e1 e2 |])+          acc <- sttLayer $ newSTRef e2+          forMwhile_ (envAssumptions e1)+                     (do thisE2 <- sttLayer $ readSTRef acc+                         notM $ envIsNogood thisE2) $ \assume -> do+            oldE2 <- sttLayer $ readSTRef acc+            $(dbg [| debugUnionEnvLoopStart assume oldE2 |])+            newE2 <- consEnv assume oldE2+            $(dbg [| debugUnionEnvLoopCons newE2 |])+            sttLayer $ writeSTRef acc newE2+          result <- sttLayer $ readSTRef acc+          $(dbg [| debugUnionEnvResult result |])+          return result++debugUnionEnvStart ::+  (MonadIO m, NodeDatum d) => Env d i r s m -> Env d i r s m -> ATMST s m ()+debugUnionEnvStart e1 e2 = do+  liftIO $ putStr "       - Starting unionEnv' with "+  blurbEnv e1+  liftIO $ putStr "; "+  blurbEnv e2+  liftIO $ putStrLn ""++debugUnionEnvLoopStart ::+  (MonadIO m, NodeDatum d) => Node d i r s m -> Env d i r s m -> ATMST s m ()+debugUnionEnvLoopStart node e2 = do+  datumFmt <- getDatumString $ nodeATMS node+  liftIO $ putStrLn $ "         - Running loop with"+  liftIO $ putStrLn $ "           node " ++ datumFmt (nodeDatum node)+  liftIO $ putStr "           env "+  blurbEnv e2+  liftIO $ putStrLn ""++debugUnionEnvLoopCons ::+  (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()+debugUnionEnvLoopCons e = do+  liftIO $ putStr "           consEnv returns "+  blurbEnv e+  liftIO $ putStrLn ""++debugUnionEnvResult ::+  (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()+debugUnionEnvResult result = do+  liftIO $ putStr "         unionEnv returns "+  blurbEnv result+  liftIO $ putStrLn ""+++-- |Derive an environment from the addition of one additional+-- assumption to a previous `Env`'s assumption list.+--+-- Translated from @cons-env@ in @atms.lisp@.+consEnv ::+  (Debuggable m, NodeDatum d) =>+    Node d i r s m -> Env d i r s m -> ATMST s m (Env d i r s m)+consEnv assumption env = do+  $(dbg [| debugConsEnvStart assumption env |])++  let nassumes = orderedInsert assumption (envAssumptions env) assumptionOrder+  $(dbg [| debugConsEnvInserted nassumes |])++  envByLookup <- lookupEnv nassumes+  $(dbg [| debugConsEnvLookup envByLookup |])+  maybe (createEnv (nodeATMS assumption) nassumes) (return . id) envByLookup++debugConsEnvStart ::+  (MonadIO m, NodeDatum d) => Node d i r s m -> Env d i r s m -> ATMST s m ()+debugConsEnvStart node e2 = do+  datumFmt <- getDatumString $ nodeATMS node+  liftIO $ putStrLn $ "         - Running consEnv"+  liftIO $ putStrLn $ "           inserting node " ++ datumFmt (nodeDatum node)+  liftIO $ putStr "           into env "+  blurbEnv e2+  liftIO $ putStrLn ""++debugConsEnvInserted ::+  (MonadIO m, NodeDatum d) => [Node d i r s m] -> ATMST s m ()+debugConsEnvInserted nodes =+  case nodes of+    [] -> liftIO $ putStrLn "           list after insertion: empty list"+    (n : _) -> do+      datumFmt <- getDatumString $ nodeATMS n+      liftIO $ putStrLn $+        "           list after insertion: ["+        ++ intercalate ", " (map (datumFmt . nodeDatum) nodes)+        ++ "]"++debugConsEnvLookup ::+  (MonadIO m, NodeDatum d) => Maybe (Env d i r s m) -> ATMST s m ()+debugConsEnvLookup Nothing =+  liftIO $ putStrLn $ "           lookup gives Nothing"+debugConsEnvLookup (Just env) = do+  liftIO $ putStr $ "           lookup gives "+  blurbEnv env+  liftIO $ putStrLn ""++-- |Return the `Env`ironment containing the given list of `Node`s,+-- creating one if necessary.+--+-- Translated from @find-or-make-env@ in @atms.lisp@.+findOrMakeEnv ::+  (Monad m, NodeDatum d) =>+    [Node d i r s m] -> ATMS d i r s m -> ATMST s m (Env d i r s m)+findOrMakeEnv [] atms = getEmptyEnvironment atms+findOrMakeEnv assumptions atms = do+  check <- lookupEnv assumptions+  case check of+    Nothing -> createEnv atms assumptions+    Just env -> return env++-- * Env tables.++-- Translated from @insert-in-table@ in @atms.lisp@.+insertInTable ::+  (Monad m, NodeDatum d) =>+    ATMS d i r s m -> STRef s (EnvTable d i r s m) -> Env d i r s m ->+      ATMST s m ()+insertInTable atms tableRef env = do+  let count = envCount env+  EnvTable currentTable <- sttLayer $ readSTRef tableRef+  let (_, alloc) = boundsSTArray currentTable++  -- Re-allocate the array if it needs to grow, and update the+  -- reference.+  when (alloc < count) $ do+    incr <- getEnvTableIncr+    let newAlloc = count + incr+    sttLayer $ do+      newArray <- newSTArray (0, newAlloc) []+      forM_ [1..alloc] $ \i -> do+        envs <- readSTArray currentTable i+        writeSTArray newArray i envs+      writeSTRef tableRef $ EnvTable newArray++  -- Add the env to its slot in the table.+  sttLayer $ do+    EnvTable array <- readSTRef tableRef+    oldEnvs <- readSTArray array count+    writeSTArray array count $ env : oldEnvs++-- Translated from @lookup-env@ in @atms.lisp@.+lookupEnv ::+  (Monad m, NodeDatum d) =>+    [Node d i r s m] -> ATMST s m (Maybe (Env d i r s m))+lookupEnv [] = return Nothing+lookupEnv assumptions@(a : _) = do+  let atms = nodeATMS a+      ns = sortOn nodeIndex assumptions+  EnvTable envTable <- sttLayer $ readSTRef $ atmsEnvTable atms+  entries <- sttLayer $ readSTArray envTable $ length ns+  case filter (\x -> envAssumptions x == ns) entries of+    [] -> return Nothing+    (x : _) -> return $ Just x++-- Translated from @subset-env?@ in @atms.lisp@.+isSubsetEnv :: (Monad m, NodeDatum d) => Env d i r s m -> Env d i r s m -> Bool+isSubsetEnv e1 e2 =+  if e1 == e2 then True+  else if envCount e1 > envCount e2 then False+  else ordSubsetp (envAssumptions e1) (envAssumptions e2)++-- |The possible results of comparing two `Env`s.+data EnvCompare =+  EQenv     -- ^ Two `Env`s are the same+  | S12env  -- ^ The first `Env` is a subset of the second.+  | S21env  -- ^ The second `Env` is a subset of the first.+  | DisjEnv -- ^ Two `Env`s are disjoint.++-- Translated from @compare-env@ in @atms.lisp@.+compareEnv ::+  (Monad m, NodeDatum d) => Env d i r s m -> Env d i r s m -> EnvCompare+compareEnv e1 e2 =+  if e1 == e2+  then EQenv+  else if envCount e1 < envCount e2+       then if nodeListIsSubsetEq (envAssumptions e1) (envAssumptions e2)+            then S12env+            else DisjEnv+       else if nodeListIsSubsetEq (envAssumptions e2) (envAssumptions e1)+            then S21env+            else DisjEnv++-- |Return true if the first sorted (by `Env` index) node list is a+-- subset of the second.+nodeListIsSubsetEq ::+  (Monad m, NodeDatum d) => [Node d i r s m] -> [Node d i r s m] -> Bool+nodeListIsSubsetEq [] _ = True+nodeListIsSubsetEq _ [] = False+nodeListIsSubsetEq l1@(x : xs) (y : ys) =+  case nodeIndex x `compare` nodeIndex y of+    LT -> False+    EQ -> nodeListIsSubsetEq xs ys+    GT -> nodeListIsSubsetEq l1 ys+-- * Processing nogoods++-- Translated from @new-nogood@ in @atms.lisp@.+newNogood ::+  (Debuggable m, NodeDatum d) =>+    ATMS d i r s m -> Env d i r s m -> Justification d i r s m -> ATMST s m ()+newNogood atms cenv why = do+  $(dbg [| debugNewNogoodStart cenv why |])++  -- Record in `cenv` the reason why `cenv` is nogood.+  sttLayer $ writeSTRef (envWhyNogood cenv) (ByJustification why)++  -- `cenv` can no longer be used in node labels, so remove it from+  -- any node labels in which it appears, and propagate out any+  -- changes.+  removeEnvFromLabels cenv atms++  -- Add `cenv` to the ATMS table of nogoods.+  insertInTable atms (atmsNogoodTable atms) cenv++  -- Remove any nogood table entries made redundant by `cenv`.+  let cenvCount = envCount cenv+  EnvTable nogoodTable <- getNogoodTable atms+  forM_ [1 .. cenvCount - 1] $ \ i -> do+    entry <- sttLayer $ readSTArray nogoodTable i+    sttLayer $ writeSTArray nogoodTable i $+      filter (not . isSubsetEnv cenv) entry++  -- Find currently-non-nogood environments which are supersets of the+  -- nogood, and process them as nogoods.+  EnvTable envTable <- getEnvTable atms+  let (_, maxCount) = boundsSTArray envTable+  forM_ [cenvCount + 1, maxCount] $ \ i -> do+    entry <- sttLayer $ readSTArray envTable i+    forM_ entry $ \ old -> do+      isNogood <- envIsNogood old+      when (isNogood && isSubsetEnv cenv old) $ do+        sttLayer $ writeSTRef (envWhyNogood old) (ByEnv cenv)+        removeEnvFromLabels old atms++debugNewNogoodStart ::+  (MonadIO m, NodeDatum d) =>+    Env d i r s m -> Justification d i r s m -> ATMST s m ()+debugNewNogoodStart cenv why = do+  liftIO $ putStr "Starting newNogood with "+  debugEnv cenv+  formatJustification why >>= (liftIO . putStrLn)+++-- Translated from @set-env-contradictory@ in @atms.lisp@.+setEnvContradictory ::+  (Debuggable m, NodeDatum d) => ATMS d i r s m -> Env d i r s m -> ATMST s m ()+setEnvContradictory atms env = do+  $(dbg [| setEnvContradictoryStart env |])+  ifM (envIsNogood env)+    (do $(dbg [| liftIO $ putStr "                 Already nogood \n" |])+        return ()) $ do+    let count = envCount env+    EnvTable nogoodTableArray <- sttLayer $ readSTRef $ atmsNogoodTable atms+    forM_ [1..count] $ \i -> do+      continueLoop <- sttLayer $ newSTRef True+      $(dbg [| setEnvContradictoryStartOuter i |])+      forMMwhile_ (sttLayer $ readSTArray nogoodTableArray i)+                  (sttLayer $ readSTRef continueLoop) $ \cenv -> do+        $(dbg [| setEnvContradictoryStartInner cenv |])+        when (isSubsetEnv cenv env) $ do+          $(dbg [| setEnvContradictoryStartInnerWhen cenv env |])+          sttLayer $ do+            writeSTRef (envWhyNogood env) $ ByEnv cenv+            writeSTRef continueLoop False++setEnvContradictoryStart ::+  (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()+setEnvContradictoryStart e = do+  liftIO $ putStr "               - Running setEnvContradictory with "+  blurbEnv e+  liftIO $ putStrLn ""++setEnvContradictoryStartOuter ::+  (MonadIO m) => Int -> ATMST s m ()+setEnvContradictoryStartOuter i = do+  liftIO $ putStrLn $ ("                 Starting outer loop for "+                       ++ show i+                       ++ "-length envs")++setEnvContradictoryStartInner ::+  (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()+setEnvContradictoryStartInner cenv = do+  liftIO $ putStr "                   Starting inner loop with nogood env "+  blurbEnv cenv+  liftIO $ putStrLn ""++setEnvContradictoryStartInnerWhen ::+  (MonadIO m, NodeDatum d) => Env d i r s m -> Env d i r s m -> ATMST s m ()+setEnvContradictoryStartInnerWhen cenv env = do+  liftIO $ putStr "                   Nogood "+  blurbEnv cenv+  liftIO $ putStr " is subset of "+  blurbEnv env+  liftIO $ putStrLn ", marking latter nogood"++-- Translated from @remove-env-from-labels@ in @atms.lisp@.+removeEnvFromLabels ::+  (Monad m, NodeDatum d) => Env d i r s m -> ATMS d i r s m -> ATMST s m ()+removeEnvFromLabels env atms = do+  -- Run all rules associated with `env`, and clear the list of+  -- associated rules.+  enqueuef <- getEnqueueProcedure atms+  forMM_ (getEnvRules env) $ \ rule -> do+    enqueuef rule+  setEnvRules env []++  -- Remove `env` from the label of the nodes currently including it.+  forMM_ (getEnvNodes env) $ \ node -> do+    oldLabel <- getNodeLabel node+    setNodeLabel node $ delete env oldLabel++-- * Interpretation construction++-- |Return the minimum environments which give the `ATMS` belief in+-- the given choice sets.  The choice sets are essentially+-- conjunctive-normal form expressions; in the list of sublists of+-- nodes, under each environment in the result at least one node of+-- each sublist will be believed.+--+-- TO BE TRANSLATED from @interpretations@ in @atms.lisp@.+--+-- > ;; In atms.lisp+-- > (proclaim '(special *solutions*))+-- > (defun interpretations (atms choice-sets &optional defaults+-- >                    &aux solutions)+-- >   (if (atms-debugging atms)+-- >    (format *trace-output*+-- >       "~%Constructing interpretations depth-first for ~a:" choice-sets))+-- >   (format *trace-output* "~%- Refining choice sets")+-- >   (let ((*solutions* nil)+-- >    (choice-sets+-- >      (mapcar #'(lambda (alt-set)+-- >                  (format *trace-output*+-- >                      "~%  - ~a --> ???" alt-set)+-- >                  (let ((result+-- >                         (mapcan #'(lambda (alt)+-- >                                     (format *trace-output*+-- >                                         "~%    - ~a --> ~a"+-- >                                         alt (tms-node-label alt))+-- >                                     (copy-list (tms-node-label alt)))+-- >                                 alt-set)))+-- >                    (format *trace-output*+-- >                        "~%    ~a --> ~a" alt-set result)+-- >                    result))+-- >              choice-sets)))+-- >     (format *trace-output* "~%  Refined choice sets to ~a" choice-sets)+-- >     (dolist (choice (car choice-sets))+-- >       (format *trace-output*+-- >      "~%- Calling depth-solutions with choice ~a" choice)+-- >       (format *trace-output*+-- >      "~%                               choice sets ~a" (car choice-sets))+-- >       (get-depth-solutions1 choice (cdr choice-sets))+-- >       (format *trace-output*+-- >      "~%      => solutions ~a" *solutions*))+-- >     (setq *solutions* (delete nil *solutions* :TEST #'eq))+-- >     (unless *solutions*+-- >       (if choice-sets (return-from interpretations nil)+-- >                  (setq *solutions* (list (atms-empty-env atms)))))+-- >     (when defaults+-- >       (setq solutions *solutions* *solutions* nil)+-- >       (dolist (solution solutions)+-- >    (extend-via-defaults solution defaults defaults)))+-- >     (delete nil *solutions* :TEST #'eq)))+interpretations ::+  (Monad m, NodeDatum d) => ATMS d i r s m -> [[Node d i r s m]] -> ATMST s m ()+interpretations = error "< TODO unimplemented interpretations >"++-- |TO BE TRANSLATED from @get-depth-solutions1@ in @atms.lisp@.+--+-- > ;; In atms.lisp+-- > (defun get-depth-solutions1 (solution choice-sets+-- >                                  &aux new-solution)+-- >   (cond ((null choice-sets)+-- >     (unless (do ((old-solutions *solutions* (cdr old-solutions)))+-- >                 ((null old-solutions))+-- >               (when (car old-solutions)+-- >                 (case (compare-env (car old-solutions) solution)+-- >                   ((:EQ :S12) (return t))+-- >                   (:S21 (rplaca old-solutions nil)))))+-- >       (push solution *solutions*)))+-- >    ((env-nogood? solution)) ;something died.+-- >    (t (dolist (choice (car choice-sets))+-- >         (setq new-solution (union-env solution choice))+-- >         (unless (env-nogood? new-solution)+-- >           (get-depth-solutions1 new-solution+-- >                                 (cdr choice-sets)))))))+getDepthSolutions1 ::+  (Monad m, NodeDatum d) => Env d i r s m -> [[Env d i r s m]] -> ATMST s m ()+getDepthSolutions1 = error "< TODO unimplemented getDepthSolutions1 >"++-- |TO BE TRANSLATED from @extend-via-defaults@ in @atms.lisp@.+--+-- > ;; In atms.lisp+-- > (defun extend-via-defaults (solution remaining original)+-- >   (do ((new-solution)+-- >        (defaults remaining (cdr defaults)))+-- >       ((null defaults)+-- >        (or (member solution *solutions* :TEST #'eq)+-- >       (dolist (default original)+-- >         (or (member default (env-assumptions solution)+-- >                     :TEST #'eq)+-- >             (env-nogood? (cons-env default solution))+-- >             (return t)))+-- >       (push solution *solutions*)))+-- >     (setq new-solution (cons-env (car defaults) solution))+-- >     (unless (env-nogood? new-solution)+-- >       (extend-via-defaults new-solution (cdr defaults) original))))+extendViaDefaults ::+  (Monad m, NodeDatum d) =>+    Env d i r s m -> [Node d i r s m] -> [Node d i r s m] -> ATMST s m ()+extendViaDefaults = error "< TODO unimplemented extendViaDefaults >"++-- * Generating explanations++-- |This function returns a list of justifications which form a+-- directed acyclic graph (DAG) for the derivation. This is quite+-- complicated because this is really a simple consequent JTMS.+--+-- Translated from @explain-node@ in @atms.lisp@.+explainNode ::+  (Monad m, NodeDatum d) =>+    Node d i r s m -> Env d i r s m -> ATMST s m [Explanation d i r s m]+explainNode node env = explainNode1 env node [] []++-- Translated from @explain-node-1@ in @atms.lisp@.+--+-- > ;; In atms.lisp+-- > (defun explain-node-1 (env node queued-nodes explanation)+-- >   (cond ((member node queued-nodes) nil)+-- >    ((and (tms-node-assumption? node)+-- >          (member node (env-assumptions env)))+-- >     (cons (cons 'ASSUME node) explanation))+-- >    ((dolist (just explanation)+-- >       (if (if (listp just)+-- >               (eq (cdr just) node) (eq (just-consequence just) node))+-- >           (return explanation))))+-- >    (t (setq queued-nodes (cons node queued-nodes))+-- >       (dolist (just (tms-node-justs node))+-- >         (unless (dolist (a (just-antecedents just))+-- >                   (unless (in-node? a env) (return t)))+-- >          (let ((new-explanation explanation))+-- >            (dolist (a (just-antecedents just)+-- >                       (return-from explain-node-1+-- >                         (cons just new-explanation)))+-- >              (setq new-explanation+-- >                    (explain-node-1 env a queued-nodes new-explanation))+-- >              (unless new-explanation (return nil)))))))))+explainNode1 ::+  (Monad m, NodeDatum d) =>+    Env d i r s m -> Node d i r s m -> [Node d i r s m] ->+      [Justification d i r s m] ->+        ATMST s m [Explanation d i r s m]+explainNode1 = error "< TODO unimplemented explainNode1 >"++-- |Print the justifying `Env`ironments which label a `Node`.+--+-- Translated from @why-node@ in @atms.lisp@.+whyNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()+whyNode node = do+  let atms = nodeATMS node+  datumStr <- getDatumString atms+  liftIO $ putStr $ "<" ++ datumStr (nodeDatum node)+  forMM_ (getNodeLabel node) envString+  liftIO $ putStrLn ">"++-- |Print the justifying `Env`ironments which label each `Node` of an+-- `ATMS`.+--+-- Translated from @why-nodes@ in @atms.lisp@.+whyNodes :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()+whyNodes atms = do+  nodes <- getNodes atms+  forM_ nodes whyNode++-- |Print a `Node`'s justifications.+--+-- TO BE TRANSLATED from @node-justifications@ in @atms.lisp@.+--+-- > ;; In atms.lisp+-- > (defun node-justifications (node &optional (stream t))+-- >   (format t "~% For ~A:" (node-string node))+-- >   (dolist (j (tms-node-justs node))+-- >     (print-justification j stream)))+nodeJustifications :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()+nodeJustifications node = do+  nodeStr <- nodeString node+  liftIO $ putStr $ " For " ++ nodeStr ++ ":"+  justs <- getNodeJusts node+  forM_ justs printJustification++-- |Retrieve an `ATMS`'s `Env`ironment with the given index number.+--+-- Translated from @e@ in @atms.lisp@.+--+-- > ;; In atms.lisp+-- > (defun e (atms n)+-- >   (dolist (bucket (atms-env-table atms))+-- >     (dolist (env (cdr bucket))+-- >     (if (= (env-index env) n) (return-from e env)))))+e :: (Monad m, NodeDatum d) =>+  ATMS d i r s m -> Int -> ATMST s m (Maybe (Env d i r s m))+e atms i = do+  table <- getEnvTable atms+  findInEnvTable (\env -> envIndex env == i) table++-- |Print an environment.+--+-- Translated from @print-env@ in @atms.lisp@.+printEnv :: (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()+printEnv env = do+  whenM (envIsNogood env) $ liftIO $ putStr "* "+  envString env+  liftIO $ putStrLn ""++-- |Convert an `Env`ironment into a string listing the nodes of the+-- environment.+--+-- Translated from @env-string@ in @atms.lisp@.+envString :: (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()+envString env = do+  let assumptions = envAssumptions env+  unless (null assumptions) $ do+    printer <- getNodeString (nodeATMS (head assumptions))+    liftIO $ putStr $ intercalate ", " (map printer assumptions)++-- * Printing global data++-- |List the nogood `Env`ironments of an `ATMS`.+--+-- Translated from @print-nogoods@ in @atms.lisp@.+printNogoods :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()+printNogoods atms = getNogoodTable atms >>= \table -> printEnvTable table++-- |Print the `Env`ironments of an `ATMS`.+--+-- Translated from @print-envs@ in @atms.lisp@.+printEnvs :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()+printEnvs atms = getEnvTable atms >>= \table -> printEnvTable table++-- |Print the `Env`ironments contained in the given `EnvTable`.+--+-- Translated from @print-env-table@ in @atms.lisp@.+printEnvTable :: (MonadIO m, NodeDatum d) => EnvTable d i r s m -> ATMST s m ()+printEnvTable (EnvTable arr) = do+  let (lo, hi) = boundsSTArray arr+  forM_ [lo..hi] $ \i ->+    forMM_ (sttLayer $ readSTArray arr i) printEnv++-- |Print statistics about an `ATMS`.+--+-- Translated from @print-atms-statistics@ in @atms.lisp@.+printAtmsStatistics ::+  (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()+printAtmsStatistics atms = do+  liftIO $ putStrLn $ "Env table: "+  printEnvs atms+  liftIO $ putStrLn $ "Nogood table: "+  printNogoods atms++-- |Print the entries of an `EnvTable`.+--+-- Translated from @print-table@ in @atms.lisp@.+printTable ::+  (MonadIO m, NodeDatum d) => String -> EnvTable d i r s m -> ATMST s m ()+printTable msg (EnvTable arr) = do+  liftIO $ putStr msg+  let (lo, hi) = boundsSTArray arr+  forM_ [lo..hi] $ \i -> do+    row <- sttLayer $ readSTArray arr i+    let count = length row+    when (count > 0) $+      liftIO $ putStrLn $ "  " ++ show count ++ " of length " ++ show i++-- |Give a verbose printout of an `ATMS`.+--+debugAtms ::+  (MonadIO m, NodeDatum d) => String -> ATMS d i r s m -> ATMST s m ()+debugAtms blurb atms = do+  liftIO $ putStrLn $ "=============== " ++ atmsTitle atms ++ ": " ++ blurb+  debugNodes atms+  debugJusts atms+  debugAtmsEnvs atms+  debugNogoods atms+  liftIO $ putStrLn "=============== "++-- |Give a verbose printout of the `Node`s of an `ATMS`.+--+debugNodes :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()+debugNodes atms = do+  nodes <- getNodes atms+  liftIO $ putStrLn $ show (length nodes) ++ " nodes:"+  forM_ (reverse nodes) debugNode++-- |Computation returning a one-line summary of one `Node` of an `ATMS`.+--+formatNode :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String+formatNode node = do+  datumFmt <- getDatumString $ nodeATMS node+  return $ datumFmt (nodeDatum node)++-- |Computation returning a one-line summary of the `Node`s of an+-- `ATMS`.+--+formatNodes ::+  (Monad m, NodeDatum d) => String -> [Node d i r s m] -> ATMST s m String+formatNodes sep = formatList sep formatNode++-- |Computation returning a one-line summary of a list of lists of+-- `Node`s of an `ATMS`.+--+formatNodeLists ::+  (Monad m, NodeDatum d) => String -> [[Node d i r s m]] -> ATMST s m String+formatNodeLists sep = formatList sep $ formatNodes ","++-- |Computation returning a one-line summary of the label of a `Node`+-- of an `ATMS`.+--+formatNodeLabel :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String+formatNodeLabel node = do+  label <- getNodeLabel node+  case label of+    [] -> return "empty"+    _ -> formatNodeLists ", " $ map envAssumptions label++-- |Print a short summary of a `Node` of an `ATMS`.+--+blurbNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()+blurbNode node = formatNode node >>= liftIO . putStr++-- |Print a verbose summary of a `Node` of an `ATMS`.+--+-- Translated from @print-tms-node@ in @atms.lisp@.+printNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()+printNode node = do+  str <- nodeString node+  liftIO $ putStr $ "<NODE: " ++ str ++ ">"++-- |Give a verbose printout of a `Node` of an `ATMS`.+--+debugNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()+debugNode node = do+  let atms = nodeATMS node+  datumFmt <- getDatumString atms+  informantFmt <- getInformantString atms+  liftIO $ putStrLn $ "- " ++ datumFmt (nodeDatum node)++  label <- getNodeLabel node+  case label of+    [] -> liftIO $ putStrLn "  Empty label"+    [env] -> do+      liftIO $ putStr "  Single environment label: "+      debugEnv env+    _ -> forM_ label $ \env -> do+      liftIO $ putStrLn "  - "+      debugEnv env++  conseqs <- getNodeConsequences node+  case conseqs of+    [] -> liftIO $ putStrLn "  Antecedent to no justifications"+    _ -> do+      liftIO $ putStr "  Antecedent to:"+      forM_ conseqs $ \ conseq -> do+        liftIO $ putStr $ " " ++ informantFmt (justInformant conseq)+      liftIO $ putStrLn ""++-- |Computation returning a one-line summary of the reason an `ATMS`+-- may believe a `Node`.+--+formatJustification ::+  (Monad m, NodeDatum d) => Justification d i r s m -> ATMST s m String+formatJustification (ByRule j) = return $ "By rule " ++ show (justIndex j)+formatJustification (ByAssumption n) = do+  nodeFmt <- getNodeString (nodeATMS n)+  return $ "By assumption " ++ nodeFmt n+formatJustification ByContradiction = return "By contradiction"+++-- |Give a verbose printout of the `Just`ification rules of an+-- `ATMS`.+--+debugJusts :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()+debugJusts atms = do+  justs <- getJusts atms+  let len = length justs+  liftIO $ putStrLn $ show len ++ " justification structure"+    ++ (if len == 1 then "" else "s") ++ ":"+  forM_ (sortOn justIndex justs) $ debugJust++-- |Computation returning a one-line summary of the informant of a+-- `Just`ification rule of an `ATMS`.+--+formatJustInformant ::+  (Monad m, NodeDatum d) => JustRule d i r s m -> ATMST s m String+formatJustInformant rule = do+  informantFmt <- getInformantString $ nodeATMS $ justConsequence rule+  return $ informantFmt $ justInformant rule++-- |Print a more verbose description of a `Just`ification rule of an+-- `ATMS`.+--+-- Translated from @print-just@ in @atms.lisp@.+printJust :: (MonadIO m, NodeDatum d) => JustRule d i r s m -> ATMST s m ()+printJust rule = do+  infStr <- formatJustInformant rule+  liftIO $ putStr $ "<" ++ infStr ++ " " ++ show (justIndex rule) ++ ">"++-- |Print a more verbose description of the `Justification`.+printJustification ::+  (MonadIO m, NodeDatum d) => Justification d i r s m -> ATMST s m ()+printJustification j = case j of+  ByRule rule -> printJust rule+  ByAssumption node -> do+    liftIO $ putStr $ "Assumed node "+    printNode node+  ByContradiction -> liftIO $ putStrLn $ "By contradiction"++-- |Give a verbose printout of one `Just`ification rule of an `ATMS`.+--+debugJust :: (MonadIO m, NodeDatum d) => JustRule d i r s m -> ATMST s m ()+debugJust (JustRule idx inf conseq ants) = do+  let atms = nodeATMS conseq+  informantFmt <- getInformantString atms+  datumFmt <- getDatumString atms+  liftIO $ putStrLn $ "  "+    ++ "[" ++ informantFmt inf ++ "." ++ show idx ++ "] "+    ++ datumFmt (nodeDatum conseq) ++ " <= "+    ++ intercalate ", " (map (datumFmt . nodeDatum) ants)++-- |Give a verbose printout of the `Env`ironments of an `ATMS`.+--+debugAtmsEnvs :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()+debugAtmsEnvs atms = do+  liftIO $ putStrLn "Environments:"+  envTable <- getEnvTable atms+  debugEnvTable atms envTable++-- |Give a verbose printout of one `Env`ironment of an `ATMS`.+--+debugEnv :: (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()+debugEnv env = do+  isNogood <- envIsNogood env+  case envAssumptions env of+    [] -> liftIO $ putStrLn "<empty>"+    nodes @ (n : _) -> do+      let atms = nodeATMS n+      datumFmt <- getDatumString atms+      when isNogood $ liftIO $ putStr "[X] "+      liftIO $ putStrLn $+        (intercalate ", " $ map (datumFmt . nodeDatum) nodes)+        ++ " (count " ++ show (length nodes) ++ ")"++-- |Print a short summary of a mutable list of nullable (via `Maybe`)+-- `Env`ironments from an `ATMS`.+--+blurbMaybeEnvMList ::+  (MonadIO m, NodeDatum d) => MList s (Maybe (Env d i r s m)) -> ATMST s m ()+blurbMaybeEnvMList mlist = do+  sep <- sttLayer $ newSTRef ""+  liftIO $ putStr "m["+  mlistFor_ sttLayer mlist $ \envm -> do+    thisSep <- sttLayer $ readSTRef sep+    liftIO $ putStr thisSep+    case envm of+      Just env -> blurbEnv env+      Nothing -> liftIO $ putStr "<nothing>"+    sttLayer $ writeSTRef sep ", "+  liftIO $ putStr "]"++-- |Print a short summary of a reference to a mutable list of+-- nullable (via `Maybe`) `Env`ironments from an `ATMS`.+--+blurbMaybeEnvMListRef ::+  (MonadIO m, NodeDatum d) =>+    STRef s (MList s (Maybe (Env d i r s m))) -> ATMST s m ()+blurbMaybeEnvMListRef mlistRef = do+  mlist <- sttLayer $ readSTRef mlistRef+  blurbMaybeEnvMList mlist++-- |Print a short summary of a nullable (via `Maybe`) reference to an+-- `Env`ironment of an `ATMS`.+--+blurbMaybeEnv ::+  (MonadIO m, NodeDatum d) => Maybe (Env d i r s m) -> ATMST s m ()+blurbMaybeEnv envm = case envm of+                       Just env -> blurbEnv env+                       Nothing -> liftIO $ putStr "<nothing>"++-- |Print a short summary of one `Env`ironment of an `ATMS`.+--+blurbEnv :: (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()+blurbEnv env = do+  wng <- sttLayer $ readSTRef $ envWhyNogood env+  isNogood <- envIsNogood env+  case envAssumptions env of+    [] -> do+      liftIO $ putStr "<empty>"+    nodes @ (first : _) -> do+      datumFmt <- getDatumString (nodeATMS first)+      when isNogood $ liftIO $ putStr "[X] "+      liftIO $ putStr $+        "{" ++ (intercalate ", " $ map (datumFmt . nodeDatum) nodes) ++ "}"++-- |Give a verbose printout of the no-good `Env`ironments of an+-- `ATMS`.+--+debugNogoods :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()+debugNogoods atms = do+  liftIO $ putStrLn "No-good environments:"+  nogoodTable <- getNogoodTable atms+  debugEnvTable atms nogoodTable++-- |Give a verbose printout of the `Env`ironments of an `EnvTable` of+-- an `ATMS`.+--+debugEnvTable ::+  (MonadIO m, NodeDatum d) =>+    ATMS d i r s m -> EnvTable d i r s m -> ATMST s m ()+debugEnvTable atms (EnvTable array) = do+  let (lo, hi) = boundsSTArray array+  forM_ [lo..hi] $ \ i -> do+    envs <- sttLayer $ readSTArray array i+    forM_ (reverse envs) $ \ env -> do+      liftIO $ putStr "- "+      debugEnv env++{-+-- |Print a short summary of the label of a `Node` of an `ATMS`.+--+blurbNodeLabel ::+  (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m String+blurbNodeLabel node = do+  -- lbl <- getNodeLabel node+  lbl <- sttLayer $ readSTRef (nodeLabel node)+  blurbNode node+  liftIO $ putStr " label: "+  blurbEnvList 10000 "\n" lbl+  liftIO $ putStrLn ""+-}++-- |Give a verbose printout of the label of a `Node` of an `ATMS`.+--+debugNodeLabel ::+  (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()+debugNodeLabel node = do+  -- lbl <- getNodeLabel node+  lbl <- sttLayer $ readSTRef (nodeLabel node)+  blurbNode node+  liftIO $ putStr " label: "+  blurbEnvList 10000 "\n" lbl+  liftIO $ putStrLn ""++-- |Print a short summary of a list of `Env`ironments of an `ATMS`.+--+blurbEnvList ::+  (MonadIO m, NodeDatum d) => Int -> String -> [Env d i r s m] -> ATMST s m ()+blurbEnvList multiLineIf lineLead envs =+  case length envs of+    0 -> liftIO $ putStr "empty env list"+    n | n < multiLineIf -> do+          liftIO $ putStr $ show n ++" envs: "+          sepR <- sttLayer $ newSTRef ""+          forM_ envs $ \env -> do+            sep <- sttLayer $ readSTRef sepR+            liftIO $ putStr sep+            blurbEnv env+            sttLayer $ writeSTRef sepR ", "+    n -> do+      liftIO $ putStrLn $ show n ++" envs:"+      forM_ envs $ \env -> do+        liftIO $ putStr lineLead+        blurbEnv env+        liftIO $ putStrLn ""++instance MonadIO m => MonadIO (STT s m) where liftIO = lift . liftIO
+ src/main/haskell/lib/Data/TMS/ChooseDebugging.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE TemplateHaskell, KindSignatures, RankNTypes #-}++{-|+Module      : ChooseDebugging+Description : The main switch for activating tracing messages for debugging in output.+Copyright   : (c) John Maraist, 2022+License     : AllRightsReserved+Maintainer  : haskell-tms@maraist.org+Stability   : experimental+Portability : POSIX++The module contains the flag which indicates whether debugging output+should be compiled into modules using this system for runtime trace+output.+-}++module Data.TMS.ChooseDebugging (debuggingOn, debugging) where+import Language.Haskell.TH+import Control.Monad+import Control.Monad.IO.Class+import Control.Monad.ST.Trans+import Control.Monad.Trans.Class+import Control.Monad.Trans.Free+import Control.Monad.Trans.Identity+import Control.Monad.Trans.Maybe+import Control.Monad.Trans.Reader+import Control.Monad.Trans.Resource+import Control.Monad.Trans.State.Strict+import qualified Control.Monad.Trans.State.Lazy as SL+import qualified Control.Monad.Trans.Writer.Lazy as WL+import qualified Control.Monad.Trans.Writer.Strict as WS++-- | Flag which indicates whether debugging output should be compiled+-- into modules using this system for runtime trace output.+debuggingOn = False++unitQ :: Q Exp+{-# INLINE unitQ #-}+unitQ = [| return () |]++monadIOQ = ''MonadIO+monadQ = ''Monad++-- | Macro which expands to definitions which either print debugging+-- statements, or do nothing.+debugging :: Q [Dec]+debugging = if debuggingOn+           then [d| class MonadIO m => Debuggable m+                    instance MonadIO m => Debuggable m+                    dbg :: Q Exp -> Q Exp+                    {-# INLINE dbg #-}+                    dbg exp = exp+                |]+           else [d| class Monad m => Debuggable m+                    instance Monad m => Debuggable m+                    dbg :: a -> Q Exp+                    {-# INLINE dbg #-}+                    dbg _ = unitQ+                |]
+ src/main/haskell/lib/Data/TMS/Dbg.hs view
@@ -0,0 +1,14 @@+{-# LANGUAGE TemplateHaskell, KindSignatures, RankNTypes, FlexibleInstances, UndecidableInstances #-}++module Data.TMS.Dbg (+  -- |Constraint for monads which will require `MonadIO` when+  -- debugging is activated.+  Debuggable,+  -- |The quoted code will be run when debugging is activated.+  dbg+  ) where+import Language.Haskell.TH+import Data.TMS.ChooseDebugging (debugging)+import Control.Monad.IO.Class++$(debugging)
+ src/main/haskell/lib/Data/TMS/Helpers.hs view
@@ -0,0 +1,251 @@+{-|+Module      : Helpers+Description : Helping functions, sort of ExtraExtra+Copyright   : (c) John Maraist, 2022+License     : AllRightsReserved+Maintainer  : haskell-tms@maraist.org+Stability   : experimental+Portability : POSIX++Unless required by applicable law or agreed to in writing, software+distributed under the License is distributed on an "AS IS" BASIS,+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or+implied, for NON-COMMERCIAL use.  See the License for the specific+language governing permissions and limitations under the License.++-}++{-# LANGUAGE RankNTypes #-}++module Data.TMS.Helpers where++import Control.Monad.State+import Control.Monad.ST.Trans+import Control.Monad.Except+import Control.Monad.Extra+import Data.List++-- * Lists and monads++-- | Check whether a list contains a value which, when applied to a+-- computation, returns @True@.+anyByM :: (Monad m) => (a -> m Bool) -> [a] -> m Bool+anyByM _ [] = return False+anyByM k (x : xs) = do+  b <- k x+  if b then return True else anyByM k xs++-- | Check whether a returned list contains a value which satisfies+-- some monadic predicate.+anyMM :: (Monad m) => (a -> m Bool) -> m [a] -> m Bool+anyMM predM srcM = do+  src <- srcM+  anyByM predM src++-- | Check whether all of the values of a list, when applied to a+-- computation, return @True@.+allByM :: (Monad m) => (a -> m Bool) -> [a] -> m Bool+allByM _ [] = return True+allByM k (x : xs) = do+  b <- k x+  if b then allByM k xs else return False++-- * Ordered lists++-- | Determine whether one list is a subset of the other, under the+-- assumption that both lists are sorted in ascending order.+ordSubsetp :: Ord a => [a] -> [a] -> Bool+ordSubsetp [] _ = True+ordSubsetp (_ : _) [] = False+ordSubsetp l1@(n1 : ns1) l2@(n2 : ns2) =+  case compare n1 n2 of+    LT -> False+    EQ -> ordSubsetp ns1 ns2+    GT -> ordSubsetp l1 ns2++-- * Even more loops++-- | Convert a list to a string, where the converter for each element+-- is a monadic computation.+formatList :: Monad m => String -> (a -> m String) -> [a] -> m String+formatList s f xs = mapM f xs >>= return . intercalate s++-- | Like `forM_`, but with both the elements source as well as the+-- loop body as computations over the monad.+forMM_ :: (Monad m, Foldable t) => m (t a) -> (a -> m ()) -> m ()+forMM_ srcM f = do+  src <- srcM+  forM_ src f++-- | A @while@ loop, guard at the top.+whileDo :: Monad m => m Bool -> m () -> m ()+whileDo cond body =+  cond >>= \b -> if b then body >> whileDo cond body else return ()++-- | A @while@ loop based on stuff, guard at the top.+whileDoWith :: Monad m => m a -> (a -> Bool) -> (a -> m ()) -> m ()+whileDoWith src predicate body = do+  val <- src+  if predicate val then (do body val+                            whileDoWith src predicate body)+  else return ()++-- | Like `forM_`, but with an extra check run after the body of the+-- loop.  If the check fails, the loop exits early.+forMwhile_ :: Monad m => [a] -> m Bool -> (a -> m ()) -> m ()+forMwhile_ [] _ _ = return ()+forMwhile_ (x : xs) pred bodyf = do+  whenM pred $ do+    bodyf x+    forMwhile_ xs pred bodyf++-- | Like `forMwhile_`, but the source list is also the result of a+-- monadic computation.+forMMwhile_ :: Monad m => m [a] -> m Bool -> (a -> m ()) -> m ()+forMMwhile_ xsM condM bodyf = do+  xs <- xsM+  forMwhile_ xs condM bodyf++-- | Like `forMM_`, except instead of a fixed list, loop over `Maybe`+-- values returned from a subcomputation, until that subcomputation+-- returns `Nothing`.+whileReturnJust :: Monad m => m (Maybe a) -> (a -> m ()) -> m ()+whileReturnJust gen f = do+  res <- gen+  case res of+    Nothing -> return ()+    Just x  -> do+      f x+      whileReturnJust gen f++-- | Like `unless`, expect both the tested value and the body are+-- returned from a computation in a monad.+unlessMM :: Monad m => m Bool -> m () -> m ()+unlessMM cnd body = whenM (notM cnd) body++-- * Lists under references in the `STT` monad transformer++-- |Monadic version of @null@ for a list stored in an `STRef`: returns+-- `True` when the list is empty.+nullR :: Monad m => STRef s [a] -> STT s m Bool+nullR ref = do+  xs <- readSTRef ref+  return $ null xs++-- |Opposite of `nullR`, returning `False` when the referenced list is+-- empty.+nonnullR :: Monad m => STRef s [a] -> STT s m Bool+nonnullR ref = do+  xs <- readSTRef ref+  return $ not $ null xs++-- |Like a combination of `whenM` and `nonnullR`, where the body+-- receives the (pure) non-null list as an argument.+whenNonnullR :: (Monad m0, Monad m) =>+  (forall r . STT s m0 r -> m r) -> STRef s [a] -> ([a] -> m ()) -> m ()+whenNonnullR lifter ref bodyf = do+  xs <- lifter $ readSTRef ref+  if (null xs) then return () else bodyf xs++-- |Map over the values contained within a list of references.+mapRefs :: Monad m => (a -> b) -> [STRef s a] -> STT s m [b]+mapRefs f [] = return []+mapRefs f (xr : xrs) = do+  x <- readSTRef xr+  xs' <- mapRefs f xrs+  return $ f x : xs'++-- |Fold (right-associatively) the values contained within a list of+-- references.+foldrRefs :: Monad m => (a -> b -> b) -> b -> [STRef s a] -> STT s m b+foldrRefs f z [] = return z+foldrRefs f z (xr : xrs) = do+  x <- readSTRef xr+  z' <- foldrRefs f z xrs+  return $ f x z'++-- |Fold (left-associatively) the values contained within a list of+-- references.+foldlRefs :: Monad m => (b -> a -> b) -> b -> [STRef s a] -> STT s m b+foldlRefs f z [] = return z+foldlRefs f z (xr : xrs) = do+  x <- readSTRef xr+  foldlRefs f (f z x) xrs++-- | Like `forM_`, but with the list under an `STRef`.  The first+-- argument lifts an `STT` operation into @m@.+forRM_ ::+  (Monad m, Monad m0, Foldable t) =>+    (STT s m0 (t a) -> m (t a)) ->+      STRef s (t a) -> (a -> m ()) -> m ()+forRM_ liftSTT srcR f = do+  src <- liftSTT $ readSTRef srcR+  forM_ src f++-- ** Stack-like operations++-- |Push a value onto the front of the list at the given `STT`+-- reference.+push :: Monad m => a -> STRef s [a] -> STT s m ()+push v r = do+  prev <- readSTRef r+  writeSTRef r $ v : prev++-- |Push the result of a computation onto the front of the list at the+-- given `STT` reference.+pushM :: Monad m => m a -> STRef s [a] -> STT s m ()+pushM m r = do+  v <- lift m+  push v r++-- |Push every value in a collection onto the front of the list at the+-- given `STT` reference.+pushAll :: (Monad m, Traversable t) => t a -> STRef s [a] -> STT s m ()+pushAll vs r = forM_ vs $ \v -> push v r++-- |Push every value in a collection returned from a computation onto+-- the front of the list at the given `STT` reference.+pushAllM :: (Monad m, Traversable t) => m (t a) -> STRef s [a] -> STT s m ()+pushAllM m r = do+  vs <- lift m+  pushAll vs r++-- |Pop a value from the given reference to a list if one exists.+pop :: Monad m => STRef s [a] -> STT s m (Maybe a)+pop queue = do+  queueList <- readSTRef queue+  case queueList of+    [] -> return Nothing+    (x : xs) -> do+      writeSTRef queue xs+      return $ Just x++-- |Consumes the elements of a referenced list, one at a time, until+-- the list is empty.  The first argument is a @lift@-style function+-- which brings `STT` operations into the top-level monad of interest.+-- Intended to be compatible with stack-like behavior (such as with+-- `push`; this function does use `pop`) where the body of the loop+-- may add elements.+whileListM_ :: (Monad m0, Monad m) =>+  (forall r . STT s m0 r -> m r) -> STRef s [a] -> (a -> m ()) -> m ()+whileListM_ lifter listRef bodyf = whileListM_'+  where whileListM_' = do+          top <- lifter $ pop listRef+          case top of+            Nothing -> return ()+            Just x -> do+              bodyf x+              whileListM_'++-- * Strings++-- |Form a comma-separated string from a list.+commaList :: (a -> String) -> [a] -> String+commaList f [] = ""+commaList f xs = foldl1 (\ x y -> x ++ ", " ++ y) $ map f xs++-- |Remove the `Just` constructors from the elements of a list,+-- discarding elements which are `Nothing`.+unmaybe [] = []+unmaybe (Just a : xs) = a : unmaybe xs+unmaybe (_ : xs) = unmaybe xs
+ src/main/haskell/lib/Data/TMS/JTMS.hs view
@@ -0,0 +1,1570 @@+{-|+Module      : JTMS+Description : Justification-based truth maintenance systems (JTMSes)+Copyright   : (c) John Maraist, 2022+              Kenneth D. Forbus, Johan de Kleer and Xerox Corporation, 1986-1993+License     : AllRightsReserved+Maintainer  : haskell-tms@maraist.org+Stability   : experimental+Portability : POSIX++Translation of Forbus and de Kleer's justification-based truth+maintenance systems (JTMSes) from Common Lisp to Haskell.++This is not a very \"Haskelly\" implementation; rather, it is a+translation of the original code with minimal changes.  Most of the+deviations from the original are due to either Haskell's strong+typing, which necessitates some additional tagging, and to the+abomination which is Lisp's @do@ macro.  The translation relies on+mutable data structures using `STT` state thread references.  A more+pure translation, possibly not relying on the [@ST@+monad]("Control.Monad.ST")/[@STT@+transformer]("Control.Monad.ST.Trans"), is a significant piece of+future work.++Note also there are restrictions on the embedded monad @m@ which can+be wrapped in the `STT` transformer; see [the @Control.Monad.ST.Trans@+documentation]("Control.Monad.ST.Trans") for details.++See the @LICENSE.txt@ and @README-forbus-dekleer.txt@ files+distributed with this work for a paragraph stating scope of permission+and disclaimer of warranty, and for additional information regarding+copyright ownership.  The above copyright notice and that paragraph+must be included in any separate copy of this file.++Unless required by applicable law or agreed to in writing, software+distributed under the License is distributed on an "AS IS" BASIS,+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or+implied, for NON-COMMERCIAL use.  See the License for the specific+language governing permissions and limitations under the License.++-}++{-# LANGUAGE RankNTypes #-}++module Data.TMS.JTMS (+  -- * The JTMST monad+  JTMST, JtmsErr, runJTMST,++  -- * Basic JTMS structures+  JTMS, printJTMS, createJTMS,+  -- ** JTMS accessors+  jtmsTitle,+  -- ** Setting JTMS properties++  -- | === __Lisp origins__+  --+  -- The JTMS property-setting functions are translated from:+  --+  -- > ;; In jtms.lisp:+  -- > (defun change-jtms (jtms &key contradiction-handler node-string+  -- >                            enqueue-procedure debugging+  -- >                               checking-contradictions)+  -- >   (if node-string (setf (jtms-node-string jtms) node-string))+  -- >   (if debugging (setf (jtms-debugging jtms) debugging))+  -- >   (if checking-contradictions+  -- >       (setf (jtms-checking-contradictions jtms)+  -- >          checking-contradictions))+  -- >   (if contradiction-handler+  -- >       (setf (jtms-contradiction-handler jtms) contradiction-handler))+  -- >   (if enqueue-procedure+  -- >       (setf (jtms-enqueue-procedure jtms) enqueue-procedure)))+  setNodeString, nodeStringByDatum, nodeStringByIndex, nodeStringByIndexDatum,+  setDatumString, datumStringByShow,+  setInformantString, informantStringByShow,+  setJustString,+  justStringByIndex, justStringByInformant, justStringByIndexInformant,+  setDebugging, setCheckingContradictions,+  setContradictionHandler, setEnqueueProcedure,++  -- *** Accessors for a `JTMS`'s current state+  getJtmsNodes, getJtmsJusts, getJtmsContradictions, getJtmsAssumptions,+  getJtmsCheckingContradictions, getJtmsNodeString, getJtmsJustString,+  getJtmsDatumString, getJtmsInformantString, getJtmsEnqueueProcedure,+  getJtmsContradictionHandler, getJtmsDebugging,++  -- ** Nodes+  Node, createNode, nodeDatum, printTmsNode, assumeNode, nodeString,++  -- *** Accessors for a `Node`'s current state+  getNodeIsAssumption, getNodeIsContradictory, getNodeBelieved,+  getNodeConsequences, getNodeInRules, getNodeOutRules, getNodeJusts,+  getNodeSupport, isEnabledAssumption, whenSupportedByRule, ifSupportedByRule,++  -- ** Justifications+  justifyNode,+  Justification(ByRule, EnabledAssumption, UserStipulation),+  JustRule(justInformant, justConsequence, justAntecedents),+  printJustRule,++  -- * Reasoning tools+  -- ** Control of assumptions+  enableAssumption, retractAssumption, makeContradiction,+  -- ** Conclusions from current assumption belief+  isInNode, isOutNode, enabledAssumptions, nodeIsPremise, assumptionsOfNode,+  -- ** Output from the current belief state+  whyNodes, whyNode, printContraList,++  -- * Debugging utilities++  -- |Note that these functions are based on `MonadIO`, not just+  -- `Monad`, for printing debugging output.+  debugJTMS, debugNodes, debugNode, debugJusts, debugJust++  ) where++import Control.Monad.State+import Control.Monad.ST.Trans+import Control.Monad.Except+import Control.Monad.Extra+import Data.TMS.Helpers+import Data.TMS.Dbg++-- * The @JTMST@ monad transformer+--+-- Construction and manipulation of a JTMS happens inside this monad+-- wrapper.++-- |Errors which can arise from JTMS operations.+data JtmsErr = CannotEnableNonassumption String Int deriving Show++-- |The process of building and using a mutable JTMS.+type JTMSTInner s m a = Monad m => ExceptT JtmsErr (STT s m) a++-- |The process of building and using a mutable JTMS.+newtype Monad m => JTMST s m a = JtmsT { unwrap :: JTMSTInner s m a }++-- |Internal unwrapper preserving rank-2 polymorphism of the state+-- thread in the wrapper `STT`.+unwrap2 :: Monad m => (forall s . JTMST s m a) -> (forall s . JTMSTInner s m a)+unwrap2 (JtmsT m) = m++instance (Monad m) => Functor (JTMST s m) where+  fmap f (JtmsT m) = JtmsT $ do+    v <- m+    return $ f v++instance (Monad m, Functor m) => Applicative (JTMST s m) where+  pure v = JtmsT $ pure v+  (JtmsT m1) <*> (JtmsT m2) = JtmsT $ do+    f <- m1+    v <- m2+    return (f v)++instance (Monad m, Functor m) => Monad (JTMST s m) where+  -- (>>=) :: JTMST s m a -> (a -> JTMST s m b) -> JTMST s m b+  (JtmsT m) >>= f = JtmsT $ m >>= (unwrap . f)++  -- (>>) :: JTMST s m a -> JTMST s m b -> JTMST s m b+  (JtmsT m1) >> (JtmsT m2) = JtmsT $ m1 >> m2++  -- return :: a -> JTMST s m a+  return v = JtmsT $ return v++instance MonadTrans (JTMST s) where+  lift m = JtmsT $ lift $ lift m++instance MonadIO m => MonadIO (JTMST s m) where+  liftIO = lift . liftIO++-- |Lift `STT` behavior to the `JTMST` level.+jLiftSTT :: Monad m => STT s m r -> JTMST s m r+jLiftSTT md = JtmsT $ lift $ md++-- |Lift `ExceptT` behavior to the `JTMST` level.+jLiftExcept :: Monad m => ExceptT JtmsErr (STT s m) r -> JTMST s m r+jLiftExcept md = JtmsT $ md++-- |Execute a computation in the `JTMST` monad transformer.+runJTMST :: Monad m => (forall s . JTMST s m r) -> m (Either JtmsErr r)+runJTMST jtmst = runSTT $ runExceptT $ unwrap2 jtmst++-- * JTMS elements++-- ** The JTMS structure++-- |Standalone implementation of justification-based truth maintenance+-- systems.+--+--  - @d@ is the type of data associated with each `Node` of this JTMS.+--  - @i@ is the type of informants in the external system.+--  - @r@ is the type of rules which may be associated with each `Node`+--    of this JTMS.+--  - @s@ is the (phantom) type of the state thread.+--  - @m@ is the monad in which this computation lives.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defstruct (jtms (:PRINT-FUNCTION print-jtms))+-- >   (title nil)+-- >   (node-counter 0)             ;; unique namer for nodes.+-- >   (just-counter 0)             ;; unique namer for justifications.+-- >   (nodes nil)                  ;; list of all tms nodes.+-- >   (justs nil)                  ;; list of all justifications+-- >   (debugging nil)              ;; debugging flag+-- >   (contradictions nil)         ;; list of contradiction nodes.+-- >   (assumptions nil)            ;; list of assumption nodes.+-- >   (checking-contradictions T)  ;; For external systems+-- >   (node-string nil)+-- >   (contradiction-handler nil)+-- >   (enqueue-procedure nil))+data Monad m => JTMS d i r s m = JTMS {+  -- |Name of this JTMS.+  jtmsTitle :: String,+  -- |Unique namer for nodes.+  jtmsNodeCounter :: STRef s Int,+  -- |Unique namer for justifications.+  jtmsJustCounter :: STRef s Int,+  -- |List of all TMS nodes.+  jtmsNodes :: STRef s [Node d i r s m],+  -- |List of all justifications.+  jtmsJusts :: STRef s [JustRule d i r s m],+  -- |List of all contradiction nodes.+  jtmsContradictions :: STRef s [Node d i r s m],+  -- |List of all assumption nodes.+  jtmsAssumptions :: STRef s [Node d i r s m],+  -- |For external systems.+  jtmsCheckingContradictions :: STRef s Bool,+  jtmsNodeString :: STRef s (Node d i r s m -> String),+  jtmsJustString :: STRef s (JustRule d i r s m -> String),+  jtmsDatumString :: STRef s (d -> String),+  jtmsInformantString :: STRef s (i -> String),+  jtmsEnqueueProcedure :: STRef s (r -> JTMST s m ()),+  jtmsContradictionHandler :: STRef s ([Node d i r s m] -> JTMST s m ()),+  jtmsDebugging :: STRef s Bool+}++-- |TODO For the moment equality on JTMSes in by comparing their names, but+-- this is an ugly and stupid hack.  Need something like: an index for+-- JTMSes generated from JTMST.  Really, this is just for a way to+-- enable nodes from different JTMSes to be seen as unequal.+instance Monad m => Eq (JTMS d i r s m) where+  j1 == j2 = jtmsTitle j1 == jtmsTitle j2+++-- |Get the next node counter value, incrementing for future accesses.+nextNodeCounter :: Monad m => JTMS d i r s m -> JTMSTInner s m Int+nextNodeCounter jtms = lift $+  let nodeCounter = jtmsNodeCounter jtms+  in do+    nodeId <- readSTRef nodeCounter+    writeSTRef nodeCounter $ 1 + nodeId+    return nodeId++-- |Get the next justification rule counter value, incrementing for+-- future accesses.+nextJustCounter :: Monad m => JTMS d i r s m -> JTMSTInner s m Int+nextJustCounter jtms = lift $+  let justCounter = jtmsJustCounter jtms+  in do+    justId <- readSTRef justCounter+    writeSTRef justCounter $ 1 + justId+    return justId++-- | Return the current list of `Node`s of a `JTMS`.+getJtmsNodes :: Monad m => JTMS d i r s m -> JTMST s m [Node d i r s m]+getJtmsNodes = jLiftSTT . readSTRef . jtmsNodes++-- | Return the current `JustRule`s of a `JTMS`.+getJtmsJusts :: Monad m => JTMS d i r s m -> JTMST s m [JustRule d i r s m]+getJtmsJusts = jLiftSTT . readSTRef . jtmsJusts++-- | Return the current designated contradictory `Node`s of a `JTMS`.+getJtmsContradictions :: Monad m => JTMS d i r s m -> JTMST s m [Node d i r s m]+getJtmsContradictions = jLiftSTT . readSTRef . jtmsContradictions++-- | Return the current possible assumption `Node`s of a `JTMS`.  Note+-- that these nodes will not be used as assumptions unless activated+-- by `enableAssumption`.+getJtmsAssumptions :: Monad m => JTMS d i r s m -> JTMST s m [Node d i r s m]+getJtmsAssumptions = jLiftSTT . readSTRef . jtmsAssumptions++-- | Return whether a `JTMS` is currently invoking its external+-- handler for deduced contradictions.+getJtmsCheckingContradictions :: Monad m => JTMS d i r s m -> JTMST s m Bool+getJtmsCheckingContradictions = jLiftSTT . readSTRef . jtmsCheckingContradictions++-- | Return the current `Node` formatter of a `JTMS`.+getJtmsNodeString ::+  Monad m => JTMS d i r s m -> JTMST s m (Node d i r s m -> String)+getJtmsNodeString = jLiftSTT . readSTRef . jtmsNodeString++-- | Return the current `JustRule` formatter of a `JTMS`.+getJtmsJustString ::+  Monad m => JTMS d i r s m -> JTMST s m (JustRule d i r s m -> String)+getJtmsJustString = jLiftSTT . readSTRef . jtmsJustString++-- | Return the current @d@ datum formatter of a `JTMS`.+getJtmsDatumString :: Monad m => JTMS d i r s m -> JTMST s m (d -> String)+getJtmsDatumString = jLiftSTT . readSTRef . jtmsDatumString++-- | Return the current @i@ informant formatter of a `JTMS`.+getJtmsInformantString :: Monad m => JTMS d i r s m -> JTMST s m (i -> String)+getJtmsInformantString = jLiftSTT . readSTRef . jtmsInformantString++-- | Return the current external queuing procedure of a `JTMS`.+getJtmsEnqueueProcedure :: Monad m => JTMS d i r s m -> JTMST s m (r -> JTMST s m ())+getJtmsEnqueueProcedure = jLiftSTT . readSTRef . jtmsEnqueueProcedure++-- | Return the current external handler of a `JTMS` for reacting to a+-- deduced contradiction.+getJtmsContradictionHandler :: Monad m => JTMS d i r s m -> JTMST s m ([Node d i r s m] -> JTMST s m ())+getJtmsContradictionHandler = jLiftSTT . readSTRef . jtmsContradictionHandler++-- | Return the current debugging flag setting of a `JTMS`.+getJtmsDebugging :: Monad m => JTMS d i r s m -> JTMST s m Bool+getJtmsDebugging = jLiftSTT . readSTRef . jtmsDebugging++-- |Print a simple tag with the title of this JTMS.  Forces the+-- enclosed monad to be `MonadIO`.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun print-jtms (jtms stream ignore)+-- >   (declare (ignore ignore))+-- >   (format stream "#<JTMS: ~A>" (jtms-title jtms)))+printJTMS jtms = liftIO $ putStr $ "#<JTMS: " ++ jtmsTitle jtms ++ ">"++-- ** Individual nodes++-- |Wrapper for one possible belief known to the TMS.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defstruct (tms-node (:PRINT-FUNCTION print-tms-node))+-- >   (index 0)+-- >   (datum nil)           ;; pointer to external problem solver+-- >   (label :OUT)          ;; :IN means believed, :OUT means disbelieved+-- >   (support nil)         ;; Current justification or premise marker+-- >   (justs nil)           ;; Possible justifications+-- >   (consequences nil)    ;; Justifications in which it is an antecedent+-- >   (mark nil)            ;; Marker for sweep algorithms+-- >   (contradictory? nil)  ;; Flag marking it as contradictory+-- >   (assumption? nil)     ;; Flag marking it as an assumption.+-- >   (in-rules nil)     ;; Rules that should be triggered when node goes in+-- >   (out-rules nil)    ;; Rules that should be triggered when node goes out+-- >   (jtms nil))           ;; The JTMS in which this node appears.+data Monad m => Node d i r s m = Node {+  nodeIndex :: Int,+  nodeDatum :: d, -- ^Returns the piece of data associated with this node.+  nodeJTMS :: JTMS d i r s m,+  nodeIsAssumption :: STRef s Bool,+  nodeIsContradictory :: STRef s Bool,+  nodeSupport :: STRef s (Maybe (Justification d i r s m)),+  nodeBelieved :: STRef s Bool,+  nodeConsequences :: STRef s [JustRule d i r s m],+  nodeInRules :: STRef s [r],+  nodeOutRules :: STRef s [r],+  nodeJusts :: STRef s [JustRule d i r s m]+}++-- |Equality on `Node`s is based simply on comparing their JTMS and+-- index number.+instance Monad m => Eq (Node d i r s m) where+  n1 == n2 = nodeJTMS n1 == nodeJTMS n2 && nodeIndex n1 == nodeIndex n2++-- |Write one node in the standard way for this JTMS.  Forces the+-- wrapped monad to be `MonadIO`.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun print-tms-node (node stream ignore)+-- >   (declare (ignore ignore))+-- >   (format stream "#<Node: ~A>" (node-string node)))+printTmsNode :: MonadIO m => Node d i r s m -> JTMST s m ()+printTmsNode node = do+  s <- nodeString node+  liftIO $ putStr $ "#<Node: " ++ s ++ ">"++-- *** Readers of current `Node` state++-- |Return whether a `Node` may currently be used as an assumption.+getNodeIsAssumption :: Monad m => Node d i r s m -> JTMST s m Bool+getNodeIsAssumption = jLiftSTT . readSTRef . nodeIsAssumption++-- |Return whether a `Node` is currently considered a contradiction.+getNodeIsContradictory :: Monad m => Node d i r s m -> JTMST s m Bool+getNodeIsContradictory = jLiftSTT . readSTRef . nodeIsContradictory++-- |Return the current support for believing a `Node`.+getNodeSupport ::+  Monad m => Node d i r s m -> JTMST s m (Maybe (Justification d i r s m))+getNodeSupport = jLiftSTT . readSTRef . nodeSupport++-- |Return where a `Node` is supported by a particular `JustRule`.+getIsNodeSupportedBy ::+  Monad m => Node d i r s m -> JustRule d i r s m -> JTMST s m Bool+getIsNodeSupportedBy node jrule = do+  support <- getNodeSupport node+  case support of+    Just (ByRule j) | j == jrule -> return True+    _ -> return False++-- |Return whether a `Node` is currently believed.+getNodeBelieved :: Monad m => Node d i r s m -> JTMST s m Bool+getNodeBelieved = jLiftSTT . readSTRef . nodeBelieved++-- |Return the `JustRule`s which use a `Node` as an antecedent.+getNodeConsequences ::+  Monad m => Node d i r s m -> JTMST s m [JustRule d i r s m]+getNodeConsequences = jLiftSTT . readSTRef . nodeConsequences++-- |Return the current in-rules of a `Node`.+getNodeInRules :: Monad m => Node d i r s m -> JTMST s m [r]+getNodeInRules = jLiftSTT . readSTRef . nodeInRules++-- |Return the current out-rules of a `Node`.+getNodeOutRules :: Monad m => Node d i r s m -> JTMST s m [r]+getNodeOutRules = jLiftSTT . readSTRef . nodeOutRules++-- |Return the `JustRule`s which currently give a `Node` as their+-- conclusion.+getNodeJusts :: Monad m => Node d i r s m -> JTMST s m [JustRule d i r s m]+getNodeJusts = jLiftSTT . readSTRef . nodeJusts+++-- ** Justifications++-- |Wrapper for one justification relationship between many antecedent+-- nodes and one consequent node.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defstruct (just (:PRINT-FUNCTION print-just))+-- >   (index 0)+-- >   informant+-- >   consequence+-- >   antecedents)+data Monad m => JustRule d i r s m = JustRule {+  justIndex :: Int,+  justInformant :: i,+  justConsequence :: Node d i r s m,+  justAntecedents :: [Node d i r s m]+}++-- |Equality on `JustRule`s is based simply on comparing their index+-- number.+instance Monad m => Eq (JustRule d i r s m) where+  n1 == n2 = justIndex n1 == justIndex n2++-- |Print the tag of a JTMS justification.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun print-just (just stream ignore)+-- >   (declare (ignore ignore))+-- >   (format stream "#<Just ~D>" (just-index just)))+printJustRule :: MonadIO m => JustRule d i r s m -> JTMST s m ()+printJustRule just =+  liftIO $ putStr $ "#<Just " ++ (show $ justIndex just) ++ ">"++-- |Forms of data which might signal support for a node.  The original+-- Lisp does not need this declaration since it is untyped; the latter+-- two cases are simply symbols.+data Monad m => Justification d i r s m =+  ByRule (JustRule d i r s m) | EnabledAssumption | UserStipulation++-- |Returns @True@ when the node is supported by a `JustRule` with no+-- antecedents.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun tms-node-premise? (node &aux support)+-- >   (and (setq support (tms-node-support node))+-- >        (not (eq support :ENABLED-ASSUMPTION))+-- >        (null (just-antecedents support))))+nodeIsPremise :: Monad m => Node d i r s m -> JTMST s m Bool+nodeIsPremise node = JtmsT $ lift $ do+  support <- readSTRef $ nodeSupport node+  case support of+    Just (ByRule (JustRule _ _ _ antecedents)) -> return $ null antecedents+    _ -> return False++-- * Simple utilities++-- |Produce a representation of the node in the default manner for its+-- JTMS.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun node-string (node)+-- >   (funcall (jtms-node-string (tms-node-jtms node)) node))+nodeString :: Monad m => Node d i r s m -> JTMST s m String+nodeString node = JtmsT $ lift $ do+  ns <- readSTRef $ jtmsNodeString $ nodeJTMS node+  return (ns node)++-- Debugging is turned off for now.++-- -- Overloading the debugging operators to allow printing when the+-- -- underlying monad is `MonadIO`.+-- class Monad m => JTMSDebugger m where+--   debuggingJtms :: String -> m ()+--   debuggingJtms _ = return ()+--+-- instance MonadIO m => JTMSDebugger (JTMST s m) where+--   debuggingJtms s = liftIO $ print s+--+-- -- ===== __Lisp origins:__+-- --+-- -- > ;; In jtms.lisp:+-- -- > (defmacro debugging-jtms (jtms msg &optional node &rest args)+-- -- >   `(when (jtms-debugging ,jtms)+-- -- >      (format *trace-output*+-- -- >        ,msg (if ,node (node-string ,node)) ,@args)))++-- |Raise a JTMS-related error.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun tms-error (string node) (error string (node-string node)))+tmsError :: Monad m => JtmsErr -> JTMST s m ()+tmsError e = JtmsT $ throwError e++-- |The default representation of a node is by @show@ing its datum.+-- Requires that @d@ is in class `Show`.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun default-node-string (n) (format nil "~A" (tms-node-datum n)))+defaultNodeString :: (Show d, Monad m) => Node d i r s m -> String+defaultNodeString node = show $ nodeDatum node++-- |Create and return a new JTMS.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun create-jtms (title &key (node-string 'default-node-string)+-- >                                debugging+-- >                                (checking-contradictions t)+-- >                                (contradiction-handler 'ask-user-handler)+-- >                                enqueue-procedure)+-- >   (make-jtms :TITLE title+-- >              :NODE-STRING node-string+-- >              :DEBUGGING debugging+-- >              :CHECKING-CONTRADICTIONS checking-contradictions+-- >              :CONTRADICTION-HANDLER contradiction-handler+-- >              :ENQUEUE-PROCEDURE enqueue-procedure))+createJTMS :: Monad m => String -> JTMST s m (JTMS d i r s m)+createJTMS title = JtmsT $ lift $ do+  nc <- newSTRef 0+  jc <- newSTRef 0+  nodes <- newSTRef ([] :: [Node d i r s m])+  justs <- newSTRef ([] :: [JustRule d i r s m])+  contradictions <- newSTRef ([] :: [Node d i r s m])+  assumptions <- newSTRef ([] :: [Node d i r s m])+  checkingContradictions <- newSTRef True+  nodeString <- newSTRef (show . nodeIndex)+  justString <- newSTRef (show . justIndex)+  datumString <- newSTRef (\ datum -> "?")+  informantString <- newSTRef (\ inf -> "?")+  enqueueProcedure <- newSTRef (\ _ -> return ())+  contradictionHandler <- newSTRef (\ _ -> return ())+  debugging <- newSTRef False+  return (JTMS title nc jc nodes justs contradictions assumptions+               checkingContradictions+               nodeString justString datumString informantString+               enqueueProcedure contradictionHandler debugging)++-- |Helper function for writing setter command for `JTMS` components.+--+-- Not part of the original Lisp.+jtmsSetter :: Monad m =>+  (JTMS d i r s m -> STRef s v) -> JTMS d i r s m -> v -> JTMST s m ()+jtmsSetter field jtms = JtmsT . lift . writeSTRef (field jtms)++-- |Set the display function for `Node`s in a `JTMS`.+--+-- After @change-jtms@ in @jtms.lisp@.+setNodeString ::+  Monad m => JTMS d i r s m -> (Node d i r s m -> String) -> JTMST s m ()+setNodeString = jtmsSetter jtmsNodeString++-- |When the node type @d@ implements `Show`, use this display method+-- as the standard for printing the node.+nodeStringByDatum :: (Monad m, Show d) => JTMS d i r s m -> JTMST s m ()+nodeStringByDatum jtms = setNodeString jtms $ show . nodeDatum++-- |Use the node index for its display.+nodeStringByIndex :: (Monad m) => JTMS d i r s m -> JTMST s m ()+nodeStringByIndex jtms = setNodeString jtms $ show . nodeIndex++-- |When the node type @d@ implements `Show`, use both the node index+-- and this display method as the standard for printing the node.+nodeStringByIndexDatum :: (Monad m, Show d) => JTMS d i r s m -> JTMST s m ()+nodeStringByIndexDatum jtms = setNodeString jtms $ \ n ->+  (show $ nodeIndex n) ++ " " ++ (show $ nodeDatum n)++-- |Set the display function for the datum associated with each `Node`+-- in a `JTMS`.+setDatumString ::+  Monad m => JTMS d i r s m -> (d -> String) -> JTMST s m ()+setDatumString = jtmsSetter jtmsDatumString++-- |When the datum type @d@ implements `Show`, use this display method+-- as the standard for printing the datum.+datumStringByShow :: (Monad m, Show d) => JTMS d i r s m -> JTMST s m ()+datumStringByShow jtms = setDatumString jtms show++-- |Set the display function for informants in a `JTMS`.+setInformantString ::+  Monad m => JTMS d i r s m -> (i -> String) -> JTMST s m ()+setInformantString = jtmsSetter jtmsInformantString++-- |When the informant type @i@ implements `Show`, use this display method+-- as the standard for printing the informant.+informantStringByShow :: (Monad m, Show i) => JTMS d i r s m -> JTMST s m ()+informantStringByShow jtms = setInformantString jtms show++-- |Set the display function for `JustRule`s in a `JTMS`.+--+-- After @change-jtms@ in @jtms.lisp@.+setJustString ::+  Monad m => JTMS d i r s m -> (JustRule d i r s m -> String) -> JTMST s m ()+setJustString = jtmsSetter jtmsJustString++-- |Use the `JustRule` index when printing the just.+justStringByIndex :: (Monad m) => JTMS d i r s m -> JTMST s m ()+justStringByIndex jtms = setJustString jtms $ show . justIndex++-- |When the informant type @i@ implements `Show`, use the `JustRule` index when printing the just.+justStringByInformant :: (Monad m, Show i) => JTMS d i r s m -> JTMST s m ()+justStringByInformant jtms = setJustString jtms $ show . justInformant++-- |When the informant type @i@ implements `Show`, use the `JustRule` index when printing the just.+justStringByIndexInformant ::+  (Monad m, Show i) => JTMS d i r s m -> JTMST s m ()+justStringByIndexInformant jtms = setJustString jtms $ \j ->+  show (justIndex j) ++ " " ++ show (justInformant j)++-- |Turn on or turn off debugging in a JTMS.  This setting currently+-- has no effect.+--+-- After @change-jtms@ in @jtms.lisp@.+setDebugging :: Monad m => JTMS d i r s m -> Bool -> JTMST s m ()+setDebugging = jtmsSetter jtmsDebugging++-- |Set whether the `JTMS` should issue external notifications of+-- contradictions.+--+-- After @change-jtms@ in @jtms.lisp@.+setCheckingContradictions :: Monad m => JTMS d i r s m -> Bool -> JTMST s m ()+setCheckingContradictions = jtmsSetter jtmsCheckingContradictions++-- |Set the contradiction handler.  The `JTMS` default is to do+-- nothing; the intention is to allow a callback to the external+-- system using the `JTMS`.+--+-- After @change-jtms@ in @jtms.lisp@.+setContradictionHandler :: Monad m =>+  JTMS d i r s m -> ([Node d i r s m] -> JTMST s m ()) -> JTMST s m ()+setContradictionHandler = jtmsSetter jtmsContradictionHandler++-- |Set the queuing behavior needed for the external system.+--+-- After @change-jtms@ in @jtms.lisp@.+setEnqueueProcedure :: Monad m =>+  JTMS d i r s m -> (r -> JTMST s m ()) -> JTMST s m ()+setEnqueueProcedure = jtmsSetter jtmsEnqueueProcedure++-- * Basic inference-engine interface++-- |Returns @True@ if the current believed assumptions justify the+-- fact represented by the given node.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun in-node? (node) (eq (tms-node-label node) :IN))+isInNode :: Monad m => Node d i r s m -> JTMST s m Bool+isInNode node = JtmsT $ do+  believed <- lift $ readSTRef (nodeBelieved node)+  return believed++-- |Returns @True@ if the current believed assumptions do not justify+-- the fact represented by the given node.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun out-node? (node) (eq (tms-node-label node) :OUT))+isOutNode :: Monad m => Node d i r s m -> JTMST s m Bool+isOutNode node = do+  believed <- isInNode node+  return $ not believed++-- |Add a node to a JTMS.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun tms-create-node (jtms datum &key assumptionp contradictoryp)+-- >   (let ((node (make-tms-node :INDEX (incf (jtms-node-counter jtms))+-- >                              :DATUM datum+-- >                              :ASSUMPTION? assumptionp+-- >                              :CONTRADICTORY? contradictoryp+-- >                              :JTMS jtms)))+-- >     (if assumptionp (push node (jtms-assumptions jtms)))+-- >     (if contradictoryp (push node (jtms-contradictions jtms)))+-- >     (push node (jtms-nodes jtms))+-- >     node))+createNode :: Monad m => JTMS d i r s m -> d -> Bool -> Bool ->+                           JTMST s m (Node d i r s m)+createNode jtms datum isAssumption isContradictory = JtmsT $ do+  nodeIdx <- nextNodeCounter jtms+  lift $ do+    assumptionRef <- newSTRef isAssumption+    contraRef <- newSTRef isContradictory+    supportRef <- newSTRef Nothing+    believedRef <- newSTRef False+    conseqRef <- newSTRef []+    inRulesRef <- newSTRef []+    outRulesRef <- newSTRef []+    justsRef <- newSTRef []+    let node = Node nodeIdx datum jtms assumptionRef contraRef+                    supportRef believedRef conseqRef+                    inRulesRef outRulesRef justsRef+        nodeListRef = jtmsNodes jtms+      in do+        if isAssumption+          then push node $ jtmsAssumptions jtms+          else return ()++        if isContradictory+          then push node $ jtmsContradictions jtms+          else return ()++        push node nodeListRef++        return node++-- |Internal method used to flag this node as an assumption, and to+-- enable belief in this assumption.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > ;;; Converts a regular node to an assumption and enables it.+-- > (defun assume-node (node &aux (jtms (tms-node-jtms node)))+-- >   (unless (or (tms-node-assumption? node) (tms-node-premise? node))+-- >     (debugging-jtms jtms "~%Converting ~A into an assumption" node)+-- >     (setf (tms-node-assumption? node) t)+-- >     (push node (jtms-assumptions jtms)))+-- >   (enable-assumption node))+assumeNode :: Monad m => Node d i r s m -> JTMST s m ()+assumeNode node =+  let jtms = nodeJTMS node+      isAssumptionRef = nodeIsAssumption node+  in do+    ifM ((notM $ jLiftSTT $ readSTRef isAssumptionRef)+          &&^ (notM $ nodeIsPremise node))+      (do jLiftSTT $ writeSTRef isAssumptionRef True+          jLiftSTT $ push node $ jtmsAssumptions jtms)+      (return ())+    enableAssumption node++-- |API command used when the external system categorizes this node as+-- representing a contradiction.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun make-contradiction (node &aux (jtms (tms-node-jtms node)))+-- >   (unless (tms-node-contradictory? node)+-- >     (setf (tms-node-contradictory? node) t)+-- >     (push node (jtms-contradictions jtms))+-- >     (check-for-contradictions jtms)))+makeContradiction :: Monad m => Node d i r s m -> JTMST s m ()+makeContradiction node =+  let jtms = nodeJTMS node+      isContraRef = nodeIsContradictory node+  in do+    ifM (notM $ jLiftSTT $ readSTRef isContraRef)+      (do jLiftSTT $ writeSTRef isContraRef False+          jLiftSTT $ push node $ jtmsContradictions jtms+          checkForContradictions jtms)+      (return ())++-- |Add a rule for concluding belief in the @consequence@.  The rule+-- is triggered when the @antecedents@ are all believed, and is+-- associated with (perhaps named as) the @informant@.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun justify-node (informant consequence antecedents &aux just jtms)+-- >   (setq jtms (tms-node-jtms consequence)+-- >      just (make-just :INDEX (incf (jtms-just-counter jtms))+-- >                      :INFORMANT informant+-- >                      :CONSEQUENCE consequence+-- >                      :ANTECEDENTS antecedents))+-- >   (push just (tms-node-justs consequence))+-- >   (dolist (node antecedents) (push just (tms-node-consequences node)))+-- >   (push just (jtms-justs jtms))+-- >   (debugging-jtms jtms+-- >                "~%Justifying ~A by ~A using ~A."+-- >                consequence+-- >                informant+-- >                (mapcar #'node-string antecedents))+-- >   (if (or antecedents (out-node? consequence))+-- >       (if (check-justification just) (install-support consequence just))+-- >       (setf (tms-node-support consequence) just))+-- >   (check-for-contradictions jtms))+justifyNode :: Monad m =>+                 i -> Node d i r s m -> [Node d i r s m] -> JTMST s m ()+justifyNode informant consequence antecedents =+  let jtms = nodeJTMS consequence+  in do+    justIdx <- JtmsT $ nextJustCounter jtms+    let just = JustRule justIdx informant consequence antecedents++    -- Add this new JustRule as a possible justification of the+    -- consequent.+    jLiftSTT $ push just $ nodeJusts consequence++    -- For each antecedent, add the new rule as a possible consequence+    -- of that antecedent node.+    forM_ antecedents $ \ node -> do+      jLiftSTT $ push just $ nodeConsequences node++    -- Add the new rule to the JTMS's list of justification rules.+    jLiftSTT $ push just $ jtmsJusts jtms++    -- We attempt to use this new rule right now if either the+    -- consequence is currently OUT, or if there actually are+    -- antecedents.+    ifM ((return $ not $ null antecedents)+          ||^ (jLiftSTT $ notM $ readSTRef $ nodeBelieved consequence))+      -- To use the rule now, if the antecedents are satisfied, add it+      -- as a support for the consequence.+      (whenM (checkJustification just) $+       installSupport consequence $ ByRule just)+      -- Otherwise we can install as a support straightaway.+      (jLiftSTT $ writeSTRef (nodeSupport consequence) $ Just $ ByRule just)++    -- Check for new contradictions introduced with this rule.+    checkForContradictions jtms++-- * Support for adding justifications++-- |Detect the case when justification @just@ is satisfied, but the+-- `JTMS` does not believe its consequence.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun check-justification (just)+-- >   (and (out-node? (just-consequence just))+-- >        (justification-satisfied? just)))+checkJustification :: Monad m => JustRule d i r s m -> JTMST s m Bool+checkJustification just =+  (isOutNode $ justConsequence just) &&^ isJustificationSatisfied just++-- |Returns @True@ when all of the antecedents of justification @j@+-- are believed by the `JTMS`.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun justification-satisfied? (just)+-- >   (every #'in-node? (just-antecedents just)))+isJustificationSatisfied :: Monad m => JustRule d i r s m -> JTMST s m Bool+isJustificationSatisfied j = allM isInNode $ justAntecedents j++-- |Add a reason for this @conseq@ node to be believed.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun install-support (conseq just)+-- >   (make-node-in conseq just)+-- >   (propagate-inness conseq))+installSupport ::+  Monad m => Node d i r s m -> Justification d i r s m -> JTMST s m ()+installSupport node just = do+  makeNodeIn node just+  propagateInness node++-- |Trigger justifications which rely (directly or indirectly) on the+-- @node@ as an antecedent when @node@ becomes believed.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun propagate-inness (node &aux (jtms (tms-node-jtms node))+-- >                                    (q (list node)))+-- >   (do () ((null (setq node (pop q))))+-- >     (debugging-jtms jtms "~%   Propagating belief in ~A." node)+-- >     (dolist (justification (tms-node-consequences node))+-- >       (when (check-justification justification)+-- >         (make-node-in (just-consequence justification) justification)+-- >         (push (just-consequence justification) q)))))+propagateInness :: Monad m => Node d i r s m -> JTMST s m ()+propagateInness fromNode =+  let jtms = nodeJTMS fromNode+  in do+    queue <- jLiftSTT $ newSTRef [fromNode]+    whileReturnJust (jLiftSTT $ pop queue) $ \ node -> do+      justs <- jLiftSTT $ readSTRef $ nodeConsequences node+      forM_ justs $ \ j ->+        whenM (checkJustification j) $+          let conseq = justConsequence j+          in do+            makeNodeIn conseq $ ByRule j+            jLiftSTT $ push conseq queue++-- |Called when the given @reason@ causes the JTMS to believe @node@.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun make-node-in (conseq reason &aux jtms enqueuef)+-- >   (setq jtms (tms-node-jtms conseq)+-- >      enqueuef (jtms-enqueue-procedure jtms))+-- >   (debugging-jtms jtms "~%     Making ~A in via ~A."+-- >           conseq+-- >           (if (symbolp reason)+-- >               reason+-- >               (cons (just-informant reason)+-- >                     (mapcar (jtms-node-string jtms)+-- >                             (just-antecedents reason)))))+-- >   (setf (tms-node-label conseq) :IN)+-- >   (setf (tms-node-support conseq) reason)+-- >   (when enqueuef+-- >     (dolist (in-rule (tms-node-in-rules conseq))+-- >       (funcall enqueuef in-rule))+-- >     (setf (tms-node-in-rules conseq) nil)))+makeNodeIn ::+  Monad m => Node d i r s m -> Justification d i r s m -> JTMST s m ()+makeNodeIn conseq reason =+  let jtms = nodeJTMS conseq+  in do+    enqueuef <- jLiftSTT $ readSTRef $ jtmsEnqueueProcedure jtms+    jLiftSTT $ writeSTRef (nodeBelieved conseq) True+    jLiftSTT $ writeSTRef (nodeSupport conseq) $ Just reason+    forMM_ (jLiftSTT $ readSTRef $ nodeInRules conseq) enqueuef+    jLiftSTT $ writeSTRef (nodeInRules conseq) []++-- > * Assumption Manipulation++-- |This command is called when the external system chooses to+-- disbelieve the assumption represented by @node@.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun retract-assumption (node &aux jtms)+-- >   (when (eq (tms-node-support node) :ENABLED-ASSUMPTION)+-- >     (setq jtms (tms-node-jtms node))+-- >     (debugging-jtms jtms "~%  Retracting assumption ~A." node)+-- >     (make-node-out node)+-- >     (find-alternative-support jtms+-- >                               (cons node (propagate-outness node jtms)))))+retractAssumption :: Monad m => Node d i r s m -> JTMST s m ()+retractAssumption node = do+  support <- jLiftSTT $ readSTRef (nodeSupport node)+  case support of+    Just EnabledAssumption ->+      let jtms = nodeJTMS node+      in do+        makeNodeOut node+        propagated <- propagateOutness node jtms+        findAlternativeSupport jtms $ node : propagated+    _ -> return ()++-- |Return whether the given node is an enabled assumption.+isEnabledAssumption :: Monad m => Node d i r s m -> JTMST s m Bool+isEnabledAssumption node = do+  support <- jLiftSTT $ readSTRef $ nodeSupport node+  case support of+    Just EnabledAssumption -> return True+    _ -> return False++-- |Check whether the given node is supported by a `JustRule`.  If it+-- is, run the given computation with that `JustRule`.+whenSupportedByRule :: Monad m =>+  Node d i r s m -> (JustRule d i r s m -> JTMST s m a) -> JTMST s m (Maybe a)+whenSupportedByRule node body = do+  support <- jLiftSTT $ readSTRef $ nodeSupport node+  case support of+    Just (ByRule just) -> do+      result <- body just+      return $ Just result+    _ -> return Nothing++-- |Check whether the given node is supported by a `JustRule`.  If it+-- is, run the @thenM@ computation with that `JustRule`; if not, run+-- the @elseM@ computation.+ifSupportedByRule :: Monad m =>+  Node d i r s m -> (JustRule d i r s m -> JTMST s m ()) -> JTMST s m ()+    -> JTMST s m ()+ifSupportedByRule node thenM elseM = do+  support <- jLiftSTT $ readSTRef $ nodeSupport node+  case support of+    Just (ByRule just) -> thenM just+    _ -> elseM++supportAntecedents :: Monad m => Node d i r s m -> JTMST s m [Node d i r s m]+supportAntecedents node = do+  support <- jLiftSTT $ readSTRef $ nodeSupport node+  case support of+    Just (ByRule j) -> return $ justAntecedents j+    _ -> return []++emptySupportAntecedents :: Monad m => Node d i r s m -> JTMST s m Bool+emptySupportAntecedents node = do+  ants <- supportAntecedents node+  return $ null ants++-- |Called when the external system chooses to believe the assumption+-- represented by @node@.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun enable-assumption (node &aux (jtms (tms-node-jtms node)))+-- >   (unless (tms-node-assumption? node)+-- >     (tms-error "Can't enable the non-assumption ~A" node))+-- >   (debugging-jtms jtms "~%  Enabling assumption ~A." node)+-- >   (cond+-- >      ((out-node? node)+-- >       (make-node-in node :ENABLED-ASSUMPTION)+-- >       (propagate-inness node))+-- >      ((or (eq (tms-node-support node) :ENABLED-ASSUMPTION)+-- >           (null (just-antecedents (tms-node-support node)))))+-- >      (t (setf (tms-node-support node) :ENABLED-ASSUMPTION)))+-- >   (check-for-contradictions jtms))+enableAssumption :: Monad m => Node d i r s m -> JTMST s m ()+enableAssumption node =+  let jtms = nodeJTMS node+  in do+    whenM (notM $ jLiftSTT $ readSTRef $ nodeIsAssumption node) $+      jLiftExcept $ throwError $+        CannotEnableNonassumption (jtmsTitle jtms) (nodeIndex node)+    ifM (isOutNode node)+      (do makeNodeIn node EnabledAssumption+          propagateInness node)+      (ifM (isEnabledAssumption node ||^ emptySupportAntecedents node)+        (return ())+        (jLiftSTT $ writeSTRef (nodeSupport node) $ Just EnabledAssumption))+    checkForContradictions jtms++-- |Called when the JTMS disbelieves @node@.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun make-node-out (node &aux jtms enqueuef)+-- >   (setq jtms (tms-node-jtms node)+-- >      enqueuef (jtms-enqueue-procedure jtms))+-- >   (debugging-jtms jtms "~%     retracting belief in ~a." node)+-- >   (setf (tms-node-support node) nil)+-- >   (setf (tms-node-label node) :OUT)+-- >   (if enqueuef (dolist (out-rule (tms-node-out-rules node))+-- >               (funcall enqueuef out-rule)))+-- >   (setf (tms-node-out-rules node) nil))+makeNodeOut :: Monad m => Node d i r s m -> JTMST s m ()+makeNodeOut node =+  let jtms = nodeJTMS node+  in do+    enqueuef <- jLiftSTT $ readSTRef $ jtmsEnqueueProcedure jtms+    jLiftSTT $ writeSTRef (nodeSupport node) Nothing+    jLiftSTT $ writeSTRef (nodeBelieved node) False+    forMM_ (jLiftSTT $ readSTRef (nodeOutRules node)) $ \ outRule ->+      enqueuef outRule+    jLiftSTT $ writeSTRef (nodeOutRules node) []++-- |Propagate the retraction of an assumption by finding all other+-- nodes which used that assumption in their justification.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun propagate-outness (node jtms &aux out-queue)+-- >   (debugging-jtms jtms "~%   Propagating disbelief in ~A." node)+-- >   (do ((js (tms-node-consequences node) (append (cdr js) new))+-- >        (new nil nil)+-- >        (conseq nil))+-- >       ((null js) out-queue)+-- >     ;; For each justification using the node, check to see if+-- >     ;; it supports some other node.  If so, forget that node,+-- >     ;; queue up the node to look for other support, and recurse+-- >     (setq conseq (just-consequence (car js)))+-- >     (when (eq (tms-node-support conseq) (car js))+-- >       (make-node-out conseq)+-- >       (push conseq out-queue)+-- >       (setq new (tms-node-consequences conseq)))))+propagateOutness ::+  Monad m => Node d i r s m -> JTMS d i r s m -> JTMST s m [Node d i r s m]+propagateOutness node jtms = do+  result <- jLiftSTT $ newSTRef []+  queue <- jLiftSTT $ newSTRef []+  forMM_ (getNodeConsequences node) $ \j -> jLiftSTT $ push j queue+  whileListM_ jLiftSTT queue $ \j ->+    let conseq = justConsequence j+    in whenM (getIsNodeSupportedBy conseq j) $ do+      makeNodeOut conseq+      jLiftSTT $ push conseq result+      further <- getNodeConsequences conseq+      jLiftSTT $ pushAll further queue+  jLiftSTT $ readSTRef result++-- |Search for support for nodes @outs@ which were disbelieved after an+-- assumption retraction.+--+-- The original Lisp code returns the justification when+-- short-circuiting from the inner loop.  But this return value is+-- never used; moreover there is no return value used from callers of+-- this function.  So this type-checked translation returns the unit+-- value.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun find-alternative-support (jtms out-queue)+-- >   (debugging-jtms jtms "~%   Looking for alternative supports.")+-- >   (dolist (node out-queue)+-- >     (unless (in-node? node)+-- >       (dolist (just (tms-node-justs node))+-- >         (when (check-justification just)+-- >           (install-support (just-consequence just) just)+-- >           (return just))))))+findAlternativeSupport ::+  Monad m => JTMS d i r s m -> [Node d i r s m] -> JTMST s m ()+findAlternativeSupport jtms outs = do+  stack <- jLiftSTT $ newSTRef outs+  whileListM_ jLiftSTT stack $ \ node ->+    unlessMM (isInNode node) $+      forMM_ (jLiftSTT $ readSTRef $ nodeJusts node) $ \ just ->+        whenM (checkJustification just) $ do+          installSupport (justConsequence just) (ByRule just)+          propagateInness node++-- > * Contradiction handling interface++-- |Pass all believed contradiction nodes to the+-- @contradictionHandler@.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun check-for-contradictions (jtms &aux contradictions)+-- >   (when (jtms-checking-contradictions jtms)+-- >     (dolist (cnode (jtms-contradictions jtms))+-- >       (if (in-node? cnode) (push cnode contradictions)))+-- >     (if contradictions+-- >       (funcall (jtms-contradiction-handler jtms) jtms contradictions))))+checkForContradictions :: Monad m => JTMS d i r s m -> JTMST s m ()+checkForContradictions jtms = do+  localContras <- jLiftSTT $ newSTRef []+  whenM (jLiftSTT $ readSTRef $ jtmsCheckingContradictions jtms) $ do+    forMM_ (jLiftSTT $ readSTRef $ jtmsContradictions jtms) $ \ cnode ->+      whenM (isInNode cnode) $ (jLiftSTT $ push cnode localContras)+    whenNonnullR jLiftSTT localContras $ \ contras -> do+      handler <- jLiftSTT $ readSTRef $ jtmsContradictionHandler jtms+      handler contras++-- |+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defmacro without-contradiction-check (jtms &body body)+-- >   (contradiction-check jtms nil body))+withoutContradictionCheck ::+  Monad m => JTMS d i r s m -> JTMST s m () -> JTMST s m ()+withoutContradictionCheck jtms = contradictionCheck jtms False++-- |+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defmacro with-contradiction-check (jtms &body body)+-- >   (contradiction-check jtms t body))+withContradictionCheck ::+  Monad m => JTMS d i r s m -> JTMST s m () -> JTMST s m ()+withContradictionCheck jtms = contradictionCheck jtms True++-- |+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun contradiction-check (jtms flag body)+-- >   (let ((jtmsv (gensym)) (old-value (gensym)))+-- >     `(let* ((,jtmsv ,jtms)+-- >          (,old-value (jtms-checking-contradictions ,jtmsv)))+-- >        (unwind-protect+-- >         (progn (setf (jtms-checking-contradictions ,jtmsv) ,flag) ,@body)+-- >       (setf (jtms-checking-contradictions ,jtmsv) ,old-value)))))+contradictionCheck ::+  Monad m => JTMS d i r s m -> Bool -> JTMST s m () -> JTMST s m ()+contradictionCheck jtms flag body = do+  oldFlag <- jLiftSTT $ readSTRef $ jtmsCheckingContradictions jtms+  jLiftSTT $ writeSTRef (jtmsCheckingContradictions jtms) flag+  body+  jLiftSTT $ writeSTRef (jtmsCheckingContradictions jtms) oldFlag++--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defmacro with-contradiction-handler (jtms handler &body body)+-- >   (let ((jtmsv (gensym)) (old-handler (gensym)))+-- >     `(let* ((,jtmsv ,jtms)+-- >          (,old-handler (jtms-contradiction-handler ,jtmsv)))+-- >      (unwind-protect+-- >       (progn (setf (jtms-contradiction-handler ,jtmsv) ,handler) ,@body)+-- >        (setf (jtms-contradiction-handler ,jtmsv) ,old-handler)))))++--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun default-assumptions (jtms)+-- >   (with-contradiction-check jtms+-- >     (with-contradiction-handler jtms #'(lambda (&rest ignore)+-- >                                          (declare (ignore ignore))+-- >                                          (throw 'CONTRADICTION t))+-- >       (dolist (assumption (jtms-assumptions jtms))+-- >         (cond ((eq (tms-node-support assumption) :ENABLED-ASSUMPTION)+-- >                ;; No-op+-- >               )+-- >               ((not (eq :DEFAULT (tms-node-assumption? assumption)))+-- >                ;; No-op+-- >               )+-- >               ((catch 'CONTRADICTION (enable-assumption assumption))+-- >                (retract-assumption assumption)))))))+-- defaultAssumptions :: Monad m => JTMS d i r s m -> JTMST s m ()+-- defaultAssumptions jtms = error "<TODO unimplemented>"++-- > * Well-founded support inqueries++--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun supporting-justification-for-node (node) (tms-node-support node))+supportingJustificationForNode ::+  Monad m => Node d i r s m -> JTMST s m (Maybe (Justification d i r s m))+supportingJustificationForNode node = jLiftSTT $ readSTRef $ nodeSupport node++-- |API command returning the believed assumption nodes used to+-- justify belief in this node.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun assumptions-of-node (node &aux assumptions (marker (list :MARK)))+-- >   (do ((nodes (list node) (append (cdr nodes) new))+-- >        (new nil nil))+-- >       ((null nodes) assumptions)+-- >     (let ((node (car nodes)))+-- >       (cond+-- >         ((eq (tms-node-mark node) marker))+-- >         ((eq (tms-node-support node) :ENABLED-ASSUMPTION)+-- >          (push node assumptions))+-- >         ((in-node? node)+-- >          (setq new (just-antecedents (tms-node-support node)))))+-- >       (setf (tms-node-mark node) marker))))+assumptionsOfNode :: Monad m => Node d i r s m -> JTMST s m [Node d i r s m]+assumptionsOfNode node =+  let jtms = nodeJTMS node+  in do+    nodes <- jLiftSTT $ readSTRef $ jtmsNodes jtms++    -- We look at each node at most once.+    marking <- jLiftSTT $ newSTArray (0, length nodes - 1) False++    -- Set up a list for results.+    assumptions <- jLiftSTT $ newSTRef []++    -- Set up the stack of nodes to consider.+    queue <- jLiftSTT $ newSTRef []+    jLiftSTT $ push node queue++    -- Loop while the stack is not empty.+    whileListM_ jLiftSTT queue $ \node ->+      let idx = nodeIndex node+      in do+        -- Make sure we do not process a node more than once.+        unlessMM (jLiftSTT $ readSTArray marking idx) $ do+          -- The case when the node is an enabled assumption+          ifM (isEnabledAssumption node)+            (jLiftSTT $ push node assumptions)++            -- The alternative case where the node is believed+            (whenM (jLiftSTT $ readSTRef $ nodeBelieved node) $ do+                support <- getNodeSupport node+                case support of+                  Just (ByRule j) ->+                    jLiftSTT $ pushAll (justAntecedents j) queue+                  _ -> return ())++          jLiftSTT $ writeSTArray marking idx True++    -- The result is assumptions we've accumulated.+    jLiftSTT $ readSTRef assumptions++    +-- |Returns the list of currently enabled assumptions.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun enabled-assumptions (jtms &aux result)+-- >   (dolist (assumption (jtms-assumptions jtms) result)+-- >     (if (eq (tms-node-support assumption) :ENABLED-ASSUMPTION)+-- >      (push assumption result))))+enabledAssumptions :: Monad m => JTMS d i r s m -> JTMST s m [Node d i r s m]+enabledAssumptions jtms = do+  result <- jLiftSTT $ newSTRef []+  forMM_ (getJtmsAssumptions jtms) $ \node -> do+    whenM (isEnabledAssumption node) $+      jLiftSTT $ push node result+  jLiftSTT $ readSTRef result++-- > * Inference engine stub to allow this JTMS to be used standalone++-- |Print the belief state and any justification of this node.+-- Requires that the underlying monad @m@ be `MonadIO`.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun why-node (node &aux justification)+-- >   (setq justification (tms-node-support node))+-- >   (cond+-- >     ((eq justification :ENABLED-ASSUMPTION)+-- >      (format t "~%~A is an enabled assumption" (node-string node)))+-- >     (justification (format t "~%~A is IN via ~A on"+-- >                      (node-string node)+-- >                      (just-informant justification))+-- >                    (dolist (anode (just-antecedents justification))+-- >                      (format t "~%  ~A" (node-string anode))))+-- >     (T (format t "~%~A is OUT." (node-string node))))+-- >   node)+whyNode :: MonadIO m => Node d i r s m -> JTMST s m ()+whyNode node = do+  str <- nodeString node+  ifM (isEnabledAssumption node)+    (liftIO $ putStrLn $ str ++ " is an enabled assumption")+    (ifSupportedByRule node+     (\just -> do+         fmtInf <- getJtmsInformantString $ nodeJTMS node+         liftIO $ putStr $+           str ++ " is IN via " ++ fmtInf (justInformant just) ++ " on"+         forM_ (justAntecedents just) $ \ ant -> do+           antStr <- nodeString ant+           liftIO $ putStr $ " " ++ antStr+         liftIO $ putStrLn "")+     (liftIO $ putStrLn $ str ++ " is out"))++-- |Prints the justifications of all current nodes.  Requires that the+-- underlying monad @m@ be `MonadIO`.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun why-nodes (jtms)+-- >   (dolist (node (jtms-nodes jtms)) (why-node node)))+whyNodes :: MonadIO m => JTMS d i r s m -> JTMST s m ()+whyNodes jtms =+  forMM_ (getJtmsAssumptions jtms) whyNode+++-- |+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (proclaim '(special *contra-assumptions*))+-- >+-- > (defun ask-user-handler (jtms contradictions)+-- >   (handle-one-contradiction (car contradictions))+-- >   (check-for-contradictions jtms))+-- askUserHandler ::+--   MonadIO m => JTMS d i r s m -> [Node d i r s m] -> JTMST s m ()+-- askUserHandler jtms contradictions = error "<TODO unimplemented>"++-- |+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun handle-one-contradiction (contra-node+-- >                               &aux the-answer *contra-assumptions*)+-- >   (setq *contra-assumptions* (assumptions-of-node contra-node))+-- >   (unless *contra-assumptions*+-- >     (tms-error "~%There is a flaw in the universe...~A" contra-node))+-- >   (format t "~%Contradiction found: ~A" (node-string contra-node))+-- >   (print-contra-list *contra-assumptions*)+-- >   (format t "~%Call (TMS-ANSWER <number>) to retract assumption.")+-- >   (setq the-answer+-- >      (catch 'tms-contradiction-handler+-- >        (break "JTMS contradiction break")))+-- >   (if (and (integerp the-answer)+-- >         (> the-answer 0)+-- >         (not (> the-answer (length *contra-assumptions*))))+-- >       (retract-assumption (nth (1- the-answer)+-- >                             *contra-assumptions*))))+-- handleOneContradiction :: Monad m => JTMS d i r s m -> JTMST s m ()+-- handleOneContradiction node = error "<TODO unimplemented>"++-- |Print a verbose debugging output list of the contradictions in the+-- JTMS.  Requires that the underlying monad @m@ be `MonadIO`.+--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun print-contra-list (nodes)+-- >   (do ((counter 1 (1+ counter))+-- >        (nn nodes (cdr nn)))+-- >       ((null nn))+-- >     (format t "~%~A ~A" counter+-- >          (node-string (car nn)))))+printContraList :: MonadIO m => [Node d i r s m] -> JTMST s m ()+printContraList nodes = forM_ nodes $ \ node -> do+  nodeStr <- nodeString node+  liftIO $ putStrLn $  "- " ++ nodeStr++-- |+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- > (defun tms-answer (num)+-- >   (if (integerp num)+-- >       (if (> num 0)+-- >        (if (not (> num (length *contra-assumptions*)))+-- >            (throw 'tms-contradiction-handler num)+-- >            (format t "~%Ignoring answer, too big."))+-- >        (format t "~%Ignoring answer, too small"))+-- >       (format t "~%Ignoring answer, must be an integer.")))+-- tmsAnswer :: MonadIO m => Int -> JTMST s m ()+-- tmsAnswer = error "<TODO unimplemented>"++-- |Print debugging information about a `JTMS`.+debugJTMS :: MonadIO m => String -> JTMS d i r s m -> JTMST s m ()+debugJTMS desc jtms = do+  liftIO $ putStrLn $ "----- " ++ desc+  debugJusts jtms+  debugNodes jtms+  liftIO $ putStrLn "-----"++-- |Print debugging information about the `Node`s of a `JTMS`.+debugNodes :: MonadIO m => JTMS d i r s m -> JTMST s m ()+debugNodes jtms = forMM_ (jLiftSTT $ readSTRef $ jtmsNodes jtms) $+  \ node -> debugNode node++-- |Print debugging information about a `Node`.+debugNode :: MonadIO m => Node d i r s m -> JTMST s m ()+debugNode node = let jtms = nodeJTMS node+  in do+    nodeFmt <- jLiftSTT $ readSTRef $ jtmsNodeString $ jtms+    justFmt <- jLiftSTT $ readSTRef $ jtmsJustString $ jtms+    datumFmt <- jLiftSTT $ readSTRef $ jtmsDatumString $ nodeJTMS node+    informantFmt <- jLiftSTT $ readSTRef $ jtmsInformantString $ nodeJTMS node+    isAssumption <- jLiftSTT $ readSTRef $ nodeIsAssumption node+    isContradictory <- jLiftSTT $ readSTRef $ nodeIsContradictory node+    support <- jLiftSTT $ readSTRef $ nodeSupport node+    believed <- jLiftSTT $ readSTRef $ nodeBelieved node+    justs <- jLiftSTT $ readSTRef $ nodeJusts node+    consequences <- jLiftSTT $ readSTRef $ nodeConsequences node++    liftIO $ do+      putStrLn $ "Node " ++ (show $ nodeIndex node)+        ++ " [" ++ (nodeFmt node) ++ "] "+        ++ "(isAssumption " ++ show isAssumption+        ++ ", isContradictory " ++ show isContradictory ++ ", "+        ++ (if believed then "" else "not ") ++ "believed)"++      case support of+        Just EnabledAssumption -> putStrLn "- Supported: enabled assumption"+        Just UserStipulation   -> putStrLn "- Supported: user stipulation"+        Just (ByRule j) ->+          putStrLn $ "- IN via {j.informant} (" ++ (justFmt j) ++ ")"+        Nothing -> putStrLn "- OUT"++      if null justs+        then putStrLn "- Concluded by no justification rules"+        else do+          putStrLn $ "- Concluded by " ++ (show $ length justs)+            ++ " justification rule" ++ (if length justs == 1 then "" else "s")+            ++ ": " ++ (foldl1 (\ x y -> x ++ ", " ++ y) $ map justFmt justs)++      if null consequences+        then putStrLn "- Antecedent to no rules"+        else do+          putStrLn $ "- Antecedent to " ++ (show $ length consequences)+            ++ " justification rule"+            ++ (if length consequences == 1 then "" else "s")+            ++ ": " ++ commaList justFmt consequences++-- |Print debugging information about the `JustRule`s of a `JTMS`.+debugJusts :: MonadIO m => JTMS d i r s m -> JTMST s m ()+debugJusts jtms = forMM_ (jLiftSTT $ readSTRef $ jtmsJusts jtms) $+  \ just -> debugJust jtms just++-- |Print debugging information about a `JustRule`.+debugJust :: MonadIO m => JTMS d i r s m -> JustRule d i r s m -> JTMST s m ()+debugJust jtms just = do+  nodeFmt <- jLiftSTT $ readSTRef $ jtmsNodeString jtms+  justFmt <- jLiftSTT $ readSTRef $ jtmsJustString jtms+  nodeFmt <- jLiftSTT $ readSTRef $ jtmsNodeString jtms+  liftIO $ putStrLn $+    "JustRule (" ++ (justFmt just) ++ ") "+      ++ (nodeFmt $ justConsequence just) ++ " <= "+      ++ (commaList nodeFmt $ justAntecedents just)++--+-- ===== __Lisp origins:__+--+-- > ;; In jtms.lisp:+-- >+-- > (defun explore-network (node)+-- >   (unless (in-node? node)+-- >        (format t "~% Sorry, ~A not believed." (node-string node))+-- >        (return-from explore-network node))+-- >   (do ((stack nil)+-- >        (current node)+-- >        (options nil)+-- >        (olen 0)+-- >        (done? nil))+-- >       (done? current)+-- >       (why-node current)+-- >       (setq options (if (typep (tms-node-support current) 'just)+-- >                      (just-antecedents (tms-node-support current))))+-- >       (setq olen (length options))+-- >       (do ((good? nil)+-- >         (choice 0))+-- >        (good? (case good?+-- >                     (q (return-from explore-network current))+-- >                     (0 (if stack+-- >                            (setq current (pop stack))+-- >                            (return-from explore-network current)))+-- >                     (t (push current stack)+-- >                        (setq current (nth (1- good?) options)))))+-- >        (format t "~%>>>")+-- >        (setq choice (read))+-- >        (cond ((or (eq choice 'q)+-- >                   (and (integerp choice)+-- >                        (not (> choice olen))+-- >                        (not (< choice 0))))+-- >               (setq good? choice))+-- >              (t (format t+-- >                  "~% Must be q or an integer from 0 to ~D."+-- >                  olen))))))++-- * Other helpers
+ src/main/haskell/lib/Data/TMS/MList.hs view
@@ -0,0 +1,240 @@+{-|+Module      : MList+Description : Mutable linked lists in STT+Copyright   : (c) John Maraist, 2022+License     : AllRightsReserved+Maintainer  : haskell-tms@maraist.org+Stability   : experimental+Portability : POSIX++Unless required by applicable law or agreed to in writing, software+distributed under the License is distributed on an "AS IS" BASIS,+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or+implied, for NON-COMMERCIAL use.  See the License for the specific+language governing permissions and limitations under the License.++-}++{-# LANGUAGE RankNTypes #-}++module Data.TMS.MList where++import Control.Monad.State+import Control.Monad.ST.Trans+import Control.Monad.Except+import Control.Monad.Extra++-- * Mutable lists (cons cells) in `STT`++-- |Singly linked lists!  But with mutable CARs and CDRs à la Common+-- Lisp.+data MList s a = MCons (STRef s a) (STRef s (MList s a))+                 -- ^ A @cons@ cell with mutable fields.+               | MNil+                 -- ^ Regular old @nil@.++-- |Convert a pure list into a mutable list.+toMList :: Monad m => [a] -> STT s m (MList s a)+toMList [] = return MNil+toMList (x : xs) = do+  car <- newSTRef x+  cdrBody <- toMList xs+  cdr <- newSTRef cdrBody+  return $ MCons car cdr++-- |Convert an `MList` to a `String`.+showM :: (Show a, Monad m) => MList s a -> STT s m String+showM MNil = return "[]"+showM (MCons xr xsr) = do+  x <- readSTRef xr+  xs <- readSTRef xsr+  let sx = show x+  sxs <- showM xs+  return $ sx ++ " m: " ++ sxs++-- |Returns `True` for an empty list.+mnull MNil = True+mnull _ = False++-- |Returns `True` from an `STT` monad for a reference to an empty+-- list.+getMnull :: Monad m => STRef s (MList s a) -> STT s m Bool+getMnull ref = readSTRef ref >>= return . mnull++-- |Returns the CAR (element) of the first CONS cell of a non-empty+-- mutable list.+mcar (MCons x _)  = readSTRef x+-- |Returns the CDR (next cell) of the first CONS cell of a non-empty+-- mutable list.+mcdr (MCons _ xs) = readSTRef xs++-- |Convert a traditional Haskell list into a mutable `MList` list.+mlength :: Monad m => MList s a -> STT s m Int+mlength MNil = return 0+mlength (MCons _ xs) = do+  cdr <- readSTRef xs+  cdrLen <- mlength cdr+  return $ 1 + cdrLen++-- |Convert a traditional Haskell list into a mutable `MList` list.+fromList :: Monad m => [a] -> STT s m (MList s a)+fromList [] = return MNil+fromList (x : xs) = do+  car <- newSTRef x+  tail <- fromList xs+  cdr <- newSTRef tail+  return $ MCons car cdr++-- |Convert a traditional Haskell list into a mutable `MList` list,+-- applying the given function to each element.+fromListMap :: Monad m => (a -> b) -> [a] -> STT s m (MList s b)+fromListMap _ [] = return MNil+fromListMap f (x : xs) = do+  car <- newSTRef $ f x+  tail <- fromListMap f xs+  cdr <- newSTRef tail+  return $ MCons car cdr++-- |Convert a mutable `MList` list into a traditional Haskell list.+toList :: Monad m => MList s a -> STT s m [a]+toList MNil = return []+toList (MCons car cdr) = do+  x <- readSTRef car+  ms <- readSTRef cdr+  xs <- toList ms+  return $ x : xs++-- |Convert a mutable `MList` list of `Maybe` values into a+-- traditional Haskell list containing only the values under a `Just`+-- constructor.+toUnmaybeList :: Monad m => MList s (Maybe a) -> STT s m [a]+toUnmaybeList MNil = return []+toUnmaybeList (MCons car cdr) = do+  xmaybe <- readSTRef car+  ms <- readSTRef cdr+  xs <- toUnmaybeList ms+  case xmaybe of+    Nothing -> return xs+    Just x -> return $ x : xs++-- |A version of @map@ for `MList`s.+mlistMap :: Monad m => (a -> b) -> MList s a -> STT s m (MList s b)+mlistMap f MNil = return MNil+mlistMap f (MCons xref xsref) = do+  x <- readSTRef xref+  xs <- readSTRef xsref+  xref' <- newSTRef $ f x+  xs' <- mlistMap f xs+  xsref' <- newSTRef xs'+  return $ MCons xref' xsref'++-- |A version of @filter@ for `MList`s.+mlistFilter :: Monad m => (a -> Bool) -> MList s a -> STT s m (MList s a)+mlistFilter p l = do+  (_, result) <- flt p l+  return result+  where+    flt :: Monad m => (a -> Bool) -> MList s a -> STT s m (Bool, MList s a)+    flt pred l@MNil = return (False, l)+    flt pred l@(MCons xref xsref) = do+      x <- readSTRef xref+      xs <- readSTRef xsref+      (changed, xs') <- flt pred xs+      if pred x+      then if changed+           then do+             xsref' <- newSTRef xs'+             return (True, MCons xref xsref')+           else return (False, l)+      else return (True, xs')++-- |Return a new `MList` which strips off the `Just` constructor from+-- its elements, dropping and elements which are `Nothing`.+mlistUnmaybe :: Monad m => MList s (Maybe a) -> STT s m (MList s a)+mlistUnmaybe MNil = return MNil+mlistUnmaybe (MCons xref xsref) = do+  x <- readSTRef xref+  xs <- readSTRef xsref+  xs' <- mlistUnmaybe xs+  case x of+    Nothing -> return xs'+    Just x' -> do+      xref' <- newSTRef x'+      xsref' <- newSTRef xs'+      return $ MCons xref' xsref'++-- |Return a new `MList` which drops elements which are `Nothing`.+mlistStripNothing :: Monad m => MList s (Maybe a) -> STT s m (MList s (Maybe a))+mlistStripNothing = mlistFilter (not . null)++-- |Return a new `MList` which drops elements which are `Nothing` from+-- the `MList` under the reference argument.+getMlistStripNothing ::+  Monad m => STRef s (MList s (Maybe a)) -> STT s m (MList s (Maybe a))+getMlistStripNothing ref = do+  mlist <- readSTRef ref+  mlistFilter (not . null) mlist++-- |Treating an `MList` as a stack, add a new element at the top of+-- the stack, and return the new stack top.+mlistPush :: Monad m => a -> MList s a -> STT s m (MList s a)+mlistPush item mlist = do+  itemRef <- newSTRef item+  mlistRef <- newSTRef mlist+  return $ MCons itemRef mlistRef++-- |Treating an `MList` as a stack, add a new element at the top of+-- the stack, and return the new stack top.+mlistRefPush :: Monad m => a -> STRef s (MList s a) -> STT s m ()+mlistRefPush item mlistRef = do+  carRef <- newSTRef item+  cdr <- readSTRef mlistRef+  newCdrRef <- newSTRef cdr+  let newCons = MCons carRef newCdrRef+  writeSTRef mlistRef newCons++-- |Iterate over the elements of a `MList`.  The body does not+-- necessarily need operate in the same monad as where the references+-- originate; the @lifter@ parameter brings the latter into the+-- former.+mlistFor_ :: (Monad m0, Monad m) =>+  (forall r . STT s m0 r -> m r) -> MList s a -> (a -> m ()) -> m ()+mlistFor_ lifter MNil _ = return ()+mlistFor_ lifter (MCons xref xsref) bodyf = do+  x <- lifter $ readSTRef xref+  bodyf x+  xs <- lifter $ readSTRef xsref+  mlistFor_ lifter xs bodyf++-- |Like `mlistFor_`, but the body expects an `MCons` cell instead of+-- the list element itself.  Useful for mutating the list along the+-- way.+mlistForCons_ :: (Monad m0, Monad m) =>+  (forall r . STT s m0 r -> m r) -> MList s a -> (MList s a -> m ()) -> m ()+mlistForCons_ _ MNil _ = return ()+mlistForCons_ lifter mc@(MCons _ _) bodyf = do+  bodyf mc+  xs <- lifter $ mcdr mc+  mlistForCons_ lifter xs bodyf++-- |A combination of `mlistForCons_` and+-- `Data.TMS.Helpers.forMwhile_`: iterate over the `MCons` cell of a+-- list, with a trigger for an early exit.  Note that the monad for+-- the continuation condition is over the overall monad @m@, not the+-- `STT` wrapped monad @m0@.+mlistForConsWhile_ ::+  (Monad m0, Monad m) =>+    (forall r . STT s m0 r -> m r) -> MList s a -> m Bool -> (MList s a -> m ())+      -> m ()+mlistForConsWhile_ _ MNil _ _ = return ()+mlistForConsWhile_ lifter mc@(MCons _ _) moreM bodyf =+  whenM moreM $ do+    bodyf mc+    xs <- lifter $ mcdr mc+    mlistForConsWhile_ lifter xs moreM bodyf++-- |Overwrite the @car@ slot of the given `MCons` with the given+-- value.  Named after the Common Lisp function with the same+-- behavior.+rplaca :: Monad m => MList s a -> a -> STT s m ()+rplaca (MCons r _) v = writeSTRef r v
+ src/test/haskell/ATMSTests.hs view
@@ -0,0 +1,141 @@+{-|+Description : Testing assumption-based truth maintenance systems (ATMSes)+Copyright   : (c) John Maraist, 2022+              Kenneth D. Forbus, Johan de Kleer and Xerox Corporation, 1986-1993+License     : AllRightsReserved+Maintainer  : haskell-tms@maraist.org+Stability   : experimental+Portability : POSIX++Testing the Haskell translation of Forbus and de Kleer's+assumption-based truth maintenance systems (JTMSes).++See the @LICENSE.txt@ and @README-forbus-dekleer.txt@ files+distributed with this work for a paragraph stating scope of permission+and disclaimer of warranty, and for additional information regarding+copyright ownership.  The above copyright notice and that paragraph+must be included in any separate copy of this file.++Unless required by applicable law or agreed to in writing, software+distributed under the License is distributed on an "AS IS" BASIS,+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or+implied, for NON-COMMERCIAL use.  See the License for the specific+language governing permissions and limitations under the License.++-}++{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}++module ATMSTests where++import Data.List+import Data.Symbol+import Data.Void+import Data.TMS.ATMS.ATMST+import Data.TMS.Helpers+import Data.TMS.Dbg+import Control.Monad+import Control.Monad.Extra+import Control.Monad.IO.Class+import Control.Monad.ST.Trans+import Control.Monad.Trans.Class+import Test.TLT+import Testers++type ATMS1ty s m = ATMS String String Void s m+type Node1ty s m = Node String String Void s m+ex1AndTest :: MonadIO m => ATMST s (TLT m) ()+ex1AndTest = inGroup "ATMS Test 1" $ do+  atms <- createATMS "Ex1"+  setInformantStringViaString atms+  setDatumStringViaString atms++  inGroup "Freshly created ATMS" $ do+    assertAssumptionsAre atms []+    assertContradictionsAre atms []++  na <- createNode atms "A" True False+  inGroup "Created Node A" $ do+    assertSingleSelfLabel na+    assertAssumptionsAre atms [na]+    assertContradictionsAre atms []++  nc <- createNode atms "C" True False+  inGroup "Created Node C" $ do+    assertSingleSelfLabels [na, nc]+    assertAssumptionsAre atms [na, nc]+    assertContradictionsAre atms []++  ne <- createNode atms "E" True False+  inGroup "Created Node E" $ do+    assertSingleSelfLabels [na, nc, ne]+    assertAssumptionsAre atms [na, nc, ne]+    assertContradictionsAre atms []++  nh <- createNode atms "H" False False+  inGroup "Created Node H" $ do+    assertSingleSelfLabels [na, nc, ne]+    assertNoLabel nh+    assertAssumptionsAre atms [na, nc, ne]+    assertContradictionsAre atms []++  justifyNode "R1" nh [nc, ne]+  inGroup "Added Justification R1" $ do+    assertSingleSelfLabels [na, nc, ne]+    assertSingleLabelEnvBy nh [nc, ne]+    assertAssumptionsAre atms [na, nc, ne]+    assertContradictionsAre atms []++  ng <- createNode atms "G" False False+  inGroup "Created Node G" $ do+    assertSingleSelfLabels [na, nc, ne]+    assertSingleLabelEnvBy nh [nc, ne]+    assertNoLabel ng+    assertAssumptionsAre atms [na, nc, ne]+    assertContradictionsAre atms []++  justifyNode "R2" ng [na, nc]+  inGroup "Added Justification R2" $ do+    assertSingleSelfLabels [na, nc, ne]+    assertSingleLabelEnvBy nh [nc, ne]+    assertSingleLabelEnvBy ng [na, nc]+    assertAssumptionsAre atms [na, nc, ne]+    assertContradictionsAre atms []++  nx <- createNode atms "X" False True+  inGroup "Created Node X" $ do+    assertSingleSelfLabels [na, nc, ne]+    assertSingleLabelEnvBy nh [nc, ne]+    assertSingleLabelEnvBy ng [na, nc]+    assertNoLabel nx+    assertAssumptionsAre atms [na, nc, ne]+    assertContradictionsAre atms [nx]++  justifyNode "R3" nx [ng]+  inGroup "Added Justification R3" $ do+    assertSingleSelfLabels [na, nc, ne]+    assertSingleLabelEnvBy nh [nc, ne]+    assertNoLabel ng+    assertNoLabel nx+    assertAssumptionsAre atms [na, nc, ne]+    assertContradictionsAre atms [nx]++  nb <- createNode atms "B" True False+  inGroup "Created Node B" $ do+    assertSingleSelfLabels [na, nb, nc, ne]+    assertSingleLabelEnvBy nh [nc, ne]+    assertNoLabel ng+    assertNoLabel nx+    assertAssumptionsAre atms [na, nb, nc, ne]+    assertContradictionsAre atms [nx]++  justifyNode "R4" nh [nb, nc]+  inGroup "Added Justification R4" $ do+    assertSingleSelfLabels [na, nb, nc, ne]+    assertNodeLabelAssumptions nh [[nc, ne], [nc, nb]]+    assertNoLabel ng+    assertNoLabel nx+    assertAssumptionsAre atms [na, nb, nc, ne]+    assertContradictionsAre atms [nx]
+ src/test/haskell/JTMSTests.hs view
@@ -0,0 +1,325 @@+{-|+Description : Testing Justification-based truth maintenance systems (JTMSes)+Copyright   : (c) John Maraist, 2022+              Kenneth D. Forbus, Johan de Kleer and Xerox Corporation, 1986-1993+License     : AllRightsReserved+Maintainer  : haskell-tms@maraist.org+Stability   : experimental+Portability : POSIX++Translation of Forbus and de Kleer's justification-based truth+maintenance systems (JTMSes) from Common Lisp to Haskell.++See the @LICENSE.txt@ and @README-forbus-dekleer.txt@ files+distributed with this work for a paragraph stating scope of permission+and disclaimer of warranty, and for additional information regarding+copyright ownership.  The above copyright notice and that paragraph+must be included in any separate copy of this file.++Unless required by applicable law or agreed to in writing, software+distributed under the License is distributed on an "AS IS" BASIS,+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or+implied, for NON-COMMERCIAL use.  See the License for the specific+language governing permissions and limitations under the License.++-}++{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}++module JTMSTests (testEx1, testEx3) where++import Data.Symbol+import Data.Void+import Data.TMS.JTMS+import Control.Monad+import Control.Monad.Extra+import Control.Monad.IO.Class+import Control.Monad.ST.Trans+import Control.Monad.Trans.Class+import Test.TLT++-- Prints result of the string length calculation.+report :: Either JtmsErr () -> IO ()+report (Right _) = putStrLn ("Tests passed")+report (Left e) = putStrLn ("Caught exception: " ++ (show e))++instance MonadTLT m n => MonadTLT (JTMST s m) n where+  liftTLT = lift . liftTLT++type JTMS1ty s m = JTMS Symbol String Void s m+type Node1ty s m = Node Symbol String Void s m+ex1 :: Monad m => JTMST s m (JTMS1ty s m,+                             Node1ty s m, Node1ty s m, Node1ty s m,+                             Node1ty s m, Node1ty s m, Node1ty s m,+                             Node1ty s m)+ex1 = do+  j <- createJTMS "Ex1"+  nodeStringByDatum j+  datumStringByShow j+  informantStringByShow j+  justStringByIndexInformant j+  setNodeString j (show . nodeDatum)+  na <- createNode j (intern "a") True False+  nb <- createNode j (intern "b") True False+  nc <- createNode j (intern "c") True False+  nd <- createNode j (intern "d") True False+  ne <- createNode j (intern "e") True False+  nf <- createNode j (intern "f") True False+  ng <- createNode j (intern "g") True False+  justifyNode "j1" nf [na, nb]+  justifyNode "j2" ne [nb, nc]+  justifyNode "j3" ng [na, ne]+  justifyNode "j4" ng [nd, ne]+  return (j, na, nb, nc, nd, ne, nf, ng)++testEx1 :: MonadIO m => JTMST s (TLT m) ()+testEx1 = do+  (jtms, na, nb, nc, nd, ne, nf, ng) <- ex1+  datumStringByShow jtms+  inGroup "Fresh JTMS" $ do+    assertBeliefs jtms [] [na, nb, nc, nd, ne, nf, ng]+    assertNoAssumptionsOfNodes jtms [na, nb, nc, nd, ne, nf, ng]+    assertNodesUnsupported jtms [na, nb, nc, nd, ne, nf, ng]++  -- debugJTMS "fresh" jtms+  enableAssumption na+  -- debugJTMS "after (enableAssumption na)" jtms+  inGroup "Enabled a as assumption" $ do+    assertBeliefs jtms [na] [nb, nc, nd, ne, nf, ng]+    assertAssumptionsOfNode jtms na [na]+    assertNoAssumptionsOfNodes jtms [nb, nc, nd, ne, nf, ng]+    assertNodeSupportEnabledAssumption jtms na+    assertNodesUnsupported jtms [nb, nc, nd, ne, nf, ng]++  enableAssumption nb+  -- debugJTMS "after (enableAssumption nb)" jtms+  inGroup "Enabled b as assumption" $ do+    assertBeliefs jtms [na, nb, nf] [nc, nd, ne, ng]+    assertAssumptionsOfNode jtms na [na]+    assertAssumptionsOfNode jtms nb [nb]+    assertAssumptionsOfNode jtms nf [na, nb]+    assertNoAssumptionsOfNodes jtms [nc, nd, ne, ng]+    assertNodesSupportEnabledAssumption jtms [na, nb]+    assertNodeSupportInformant jtms nf "j1"+    assertNodesUnsupported jtms [nc, nd, ne, ng]++  enableAssumption nc+  -- debugJTMS "after (enableAssumption nc)" jtms+  inGroup "Enabled c as assumption" $ do+    assertBeliefs jtms [na, nb, nc, ne, nf, ng] [nd]+    assertAssumptionsOfNode jtms na [na]+    assertAssumptionsOfNode jtms nb [nb]+    assertAssumptionsOfNode jtms nc [nc]+    assertAssumptionsOfNode jtms ne [nb, nc]+    assertAssumptionsOfNode jtms nf [na, nb]+    assertAssumptionsOfNode jtms ng [na, nb, nc]+    assertNoAssumptionsOfNodes jtms [nd]+    assertNodesSupportEnabledAssumption jtms [na, nb, nc]+    assertNodeSupportInformant jtms ne "j2"+    assertNodeSupportInformant jtms nf "j1"+    assertNodeSupportInformant jtms ng "j3"+    assertNodesUnsupported jtms [nd]++  enableAssumption nd+  -- debugJTMS "after (enableAssumption nd)" jtms+  inGroup "Enabled d as assumption" $ do+    assertBeliefs jtms [na, nb, nc, nd, ne, nf, ng] []+    assertAssumptionsOfNode jtms na [na]+    assertAssumptionsOfNode jtms nb [nb]+    assertAssumptionsOfNode jtms nc [nc]+    assertAssumptionsOfNode jtms nd [nd]+    assertAssumptionsOfNode jtms ne [nb, nc]+    assertAssumptionsOfNode jtms nf [na, nb]+    assertAssumptionsOfNode jtms ng [na, nb, nc]+    assertNodesSupportEnabledAssumption jtms [na, nb, nc, nd]+    assertNodeSupportInformant jtms ne "j2"+    assertNodeSupportInformant jtms nf "j1"+    assertNodeSupportInformant jtms ng "j3"++  retractAssumption na+  -- debugJTMS "after (retractAssumption na)" jtms+  inGroup "Retracted a as assumption" $ do+    assertBeliefs jtms [nb, nc, nd, ne, ng] [na, nf]+    assertAssumptionsOfNode jtms nb [nb]+    assertAssumptionsOfNode jtms nc [nc]+    assertAssumptionsOfNode jtms nd [nd]+    assertAssumptionsOfNode jtms ne [nb, nc]+    assertAssumptionsOfNode jtms ng [nb, nc, nd]+    assertNoAssumptionsOfNodes jtms [na, nf]+    assertNodesUnsupported jtms [na, nf]+    assertNodesSupportEnabledAssumption jtms [nb, nc, nd]+    assertNodeSupportInformant jtms ne "j2"+    assertNodeSupportInformant jtms ng "j4"++type JTMS3ty s m = JTMS Symbol String () s m+type Node3ty s m = Node Symbol String () s m+ex3 :: Monad m => JTMST s m (JTMS3ty s m,+                             Node3ty s m, Node3ty s m, Node3ty s m,+                             Node3ty s m, Node3ty s m, Node3ty s m)+ex3 = do+  j <- createJTMS "Ex1"++  na <- createNode j (intern "A") True  False+  nc <- createNode j (intern "C") True  False+  ne <- createNode j (intern "E") True  False+  ng <- createNode j (intern "g") False False+  nh <- createNode j (intern "h") False False+  contra <- createNode j (intern "CONTRADICTION") False True++  justifyNode "R1" nh [nc, ne]+  justifyNode "R2" ng [na, nc]+  justifyNode "R3" contra [ng]++  return (j, na, nc, ne, ng, nh, contra)++testEx3 :: MonadIO m => JTMST s (TLT (STT s0 m)) ()+testEx3 = do+  contraHandlerFlag <- lift $ lift $ newSTRef False++  (jtms, na, nc, ne, ng, nh, contra) <- ex3+  setContradictionHandler jtms $ \_ ->+    lift $ lift $ writeSTRef contraHandlerFlag True+  datumStringByShow jtms+  inGroup "Fresh JTMS" $ do+    assertBeliefs jtms [] [na, nc, ne, ng, nh, contra]+    assertNoAssumptionsOfNodes jtms [na, nc, ne, ng, nh, contra]+    assertNodesUnsupported jtms [na, nc, ne, ng, nh, contra]+    "No call to contradiction handler" ~::+      notM (lift $ lift $ readSTRef contraHandlerFlag)++  lift $ lift $ writeSTRef contraHandlerFlag False+  enableAssumption na+  inGroup "Enabled a" $ do+    assertBeliefs jtms [na] [nc, ne, ng, nh, contra]+    assertAssumptionsOfNode jtms na [na]+    assertNoAssumptionsOfNodes jtms [nc, ne, ng, nh, contra]+    "No call to contradiction handler" ~::+      notM (lift $ lift $ readSTRef contraHandlerFlag)++  lift $ lift $ writeSTRef contraHandlerFlag False+  enableAssumption nc+  inGroup "Enabled c" $ do+    assertBeliefs jtms [na, nc, ng, contra] [ne, nh]+    "Did call contradiction handler" ~::+      (lift $ lift $ readSTRef contraHandlerFlag)++  lift $ lift $ writeSTRef contraHandlerFlag False+  enableAssumption ne+  inGroup "Enabled e" $ do+    assertBeliefs jtms [na, nc, ne, ng, nh, contra] []+    "Did call contradiction handler" ~::+      (lift $ lift $ readSTRef contraHandlerFlag)++{------------------------- Local assertions. -------------------------}++assertBeliefs ::+  Monad m => (JTMS d i r s (TLT m)) -> [Node d i r s (TLT m)] -> [Node d i r s (TLT m)] ->+               JTMST s (TLT m) ()+assertBeliefs jtms ins outs = inGroup "Node belief" $ do+  inChecks+  outChecks+  where inChecks = forM_ ins inCheck++        inCheck node = do+          name <- nodeString node+          ("Node " ++ name ++ " is in") ~:: isInNode node++        outChecks = forM_ outs $ outCheck++        outCheck node = do+          name <- nodeString node+          ("Node " ++ name ++ " is out") ~:: isOutNode node++assertAssumptionsOfNode ::+  Monad m =>+    (JTMS d i r s (TLT m)) -> Node d i r s (TLT m) -> [Node d i r s (TLT m)] ->+      JTMST s (TLT m) ()+assertAssumptionsOfNode jtms node assumptions = do+  actuals <- assumptionsOfNode node+  name <- nodeString node+  inGroup ("Checking assumptionsOfNode " ++ name) $ do+    ("Same number of expected and actual assumptions")+      ~: length assumptions @==- length actuals+    forM_ assumptions $ \ expected -> do+      expName <- nodeString expected+      ("Contains expected node " ++ expName) ~::- (expected `elem` actuals)++assertNoAssumptionsOfNodes ::+  Monad m =>+    (JTMS d i r s (TLT m)) -> [Node d i r s (TLT m)] -> JTMST s (TLT m) ()+assertNoAssumptionsOfNodes jtms nodes =+  inGroup ("No assumptionsOfNode") $+    forM_ nodes $ \ node -> do+      name <- nodeString node+      ("Node " ++ name ++ " has no assumptions") ~:+        (empty $ assumptionsOfNode node)++assertNodesUnsupported ::+  Monad m =>+    (JTMS d i r s (TLT m)) -> [Node d i r s (TLT m)] -> JTMST s (TLT m) ()+assertNodesUnsupported jtms nodes =+  inGroup ("Unsupported nodes") $+    forM_ nodes $ \ node -> do+      name <- nodeString node+      ("Node " ++ name ++ " has no support") ~::+        do support <- getNodeSupport node+           case support of+             Nothing -> return True+             Just _ -> return False++assertNodeSupportRule ::+  Monad m =>+    JTMS d i r s (TLT m) -> Node d i r s (TLT m) -> JustRule d i r s (TLT m) ->+      JTMST s (TLT m) ()+assertNodeSupportRule jtms node just = do+  infString <- getJtmsInformantString jtms+  nodeName <- nodeString node+  ("Node " ++ nodeName ++ " supported by rule "+    ++ (infString $ justInformant just)) ~:: do+    support <- getNodeSupport node+    case support of+      Just (ByRule j) | j == just -> return True+      _ -> return False++assertNodeSupportInformant ::+  (Monad m, Eq i) =>+    JTMS d i r s (TLT m) -> Node d i r s (TLT m) -> i -> JTMST s (TLT m) ()+assertNodeSupportInformant jtms node inf = do+  infString <- getJtmsInformantString jtms+  nodeName <- nodeString node+  ("Node " ++ nodeName ++ " supported by informant " ++ (infString inf)) ~:: do+    support <- getNodeSupport node+    case support of+      Just (ByRule j) | (justInformant j) == inf -> return True+      _ -> return False++assertNodeSupportEnabledAssumption ::+  Monad m => JTMS d i r s (TLT m) -> Node d i r s (TLT m) -> JTMST s (TLT m) ()+assertNodeSupportEnabledAssumption jtms node = do+  infString <- getJtmsInformantString jtms+  nodeName <- nodeString node+  ("Node " ++ nodeName ++ " is enabled assumption ") ~:: do+    support <- getNodeSupport node+    case support of+      Just EnabledAssumption -> return True+      _ -> return False++assertNodesSupportEnabledAssumption ::+  Monad m =>+    JTMS d i r s (TLT m) -> [Node d i r s (TLT m)] -> JTMST s (TLT m) ()+assertNodesSupportEnabledAssumption jtms nodes =+  inGroup ("Nodes are enabled assumptions") $+    forM_ nodes $ \ node -> assertNodeSupportEnabledAssumption jtms node++assertNodeSupportUserStipulation ::+  Monad m => JTMS d i r s (TLT m) -> Node d i r s (TLT m) -> JTMST s (TLT m) ()+assertNodeSupportUserStipulation jtms node = do+  infString <- getJtmsInformantString jtms+  nodeName <- nodeString node+  ("Node " ++ nodeName ++ " is enabled assumption ") ~:: do+    support <- getNodeSupport node+    case support of+      Just UserStipulation -> return True+      _ -> return False
+ src/test/haskell/Spec.hs view
@@ -0,0 +1,43 @@+{-|+Description : Testing truth maintenance systems (TMSes)+Copyright   : (c) John Maraist, 2022+              Kenneth D. Forbus, Johan de Kleer and Xerox Corporation, 1986-1993+License     : AllRightsReserved+Maintainer  : haskell-tms@maraist.org+Stability   : experimental+Portability : POSIX++Testing the translation of Forbus and de Kleer's various truth+maintenance systems (TMSes) from Common Lisp to Haskell.++See the @LICENSE.txt@ and @README-forbus-dekleer.txt@ files+distributed with this work for a paragraph stating scope of permission+and disclaimer of warranty, and for additional information regarding+copyright ownership.  The above copyright notice and that paragraph+must be included in any separate copy of this file.++Unless required by applicable law or agreed to in writing, software+distributed under the License is distributed on an "AS IS" BASIS,+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or+implied, for NON-COMMERCIAL use.  See the License for the specific+language governing permissions and limitations under the License.++-}++{-# LANGUAGE RankNTypes #-}++import Data.TMS.JTMS+import Data.TMS.ATMS.ATMST+import Control.Monad.ST.Trans+import Test.TLT+import JTMSTests+import ATMSTests++main :: IO ()+main = do+  runSTT $ tlt $ do+    inGroup "JTMS tests" $ runJTMST $ do+      testEx1+      testEx3+    inGroup "ATMS tests" $ runATMST $ do+      ex1AndTest
+ src/test/haskell/Testers.hs view
@@ -0,0 +1,140 @@+{-|+Description : Testing assumption-based truth maintenance systems (ATMSes)+Copyright   : (c) John Maraist, 2022+              Kenneth D. Forbus, Johan de Kleer and Xerox Corporation, 1986-1993+License     : AllRightsReserved+Maintainer  : haskell-tms@maraist.org+Stability   : experimental+Portability : POSIX++Testing the Haskell translation of Forbus and de Kleer's+assumption-based truth maintenance systems (JTMSes).++See the @LICENSE.txt@ and @README-forbus-dekleer.txt@ files+distributed with this work for a paragraph stating scope of permission+and disclaimer of warranty, and for additional information regarding+copyright ownership.  The above copyright notice and that paragraph+must be included in any separate copy of this file.++Unless required by applicable law or agreed to in writing, software+distributed under the License is distributed on an "AS IS" BASIS,+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or+implied, for NON-COMMERCIAL use.  See the License for the specific+language governing permissions and limitations under the License.++-}++{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}++module Testers where++import Data.List+import Data.Symbol+import Data.Void+import Data.TMS.ATMS.ATMST+import Data.TMS.Helpers+import Data.TMS.Dbg+import Control.Monad+import Control.Monad.Extra+import Control.Monad.IO.Class+import Control.Monad.ST.Trans+import Control.Monad.Trans.Class+import Test.TLT++-- Prints result of the string length calculation.+report :: Either AtmsErr () -> IO ()+report (Right _) = putStrLn ("Tests passed")+report (Left e) = putStrLn ("Caught exception: " ++ (show e))++instance MonadTLT m n => MonadTLT (ATMST s m) n where+  liftTLT = lift . liftTLT++assertTrueNode ::+  (MonadIO m, NodeDatum d) => Node d i r s (TLT m) -> ATMST s (TLT m) ()+assertTrueNode node = "Node is true" ~:: isTrueNode node++assertInNode ::+  (MonadIO m, NodeDatum d) => Node d i r s (TLT m) -> ATMST s (TLT m) ()+assertInNode node = "Node is in" ~:: isInNode node++assertNotTrueNode ::+  (MonadIO m, NodeDatum d) => Node d i r s (TLT m) -> ATMST s (TLT m) ()+assertNotTrueNode node = "Node is not true" ~:: (fmap not $ isTrueNode node)++assertNoLabel ::+  (MonadIO m, NodeDatum d) => Node d i r s (TLT m) -> ATMST s (TLT m) ()+assertNoLabel node = do+  labels <- getNodeLabel node+  "No labels" ~: 0 @==- length labels++assertSingleSelfLabels ::+  (MonadIO m, NodeDatum d) => [Node d i r s (TLT m)] -> ATMST s (TLT m) ()+assertSingleSelfLabels nodes =+  forM_ nodes $ \ node -> assertSingleSelfLabel node++assertSingleSelfLabel ::+  (MonadIO m, NodeDatum d) => Node d i r s (TLT m) -> ATMST s (TLT m) ()+assertSingleSelfLabel node = assertSingleLabelEnvBy node [node]++assertSingleLabelEnvBy ::+  (MonadIO m, NodeDatum d) =>+    Node d i r s (TLT m) -> [Node d i r s (TLT m)] -> ATMST s (TLT m) ()+assertSingleLabelEnvBy node nodes =+  inGroup (show node ++ " labelled by one Env with "+            ++ intercalate ", " (map show nodes)) $ do+    assertNotTrueNode node+    assertInNode node+    labels <- getNodeLabel node+    case labels of+      [env] -> do+        let envAsmpts = envAssumptions env+        "Single label should have " ++ show (length nodes) ++ " assumptions" ~:+          length nodes @==- length envAsmpts+        forM_ nodes $ \ node -> do+          "Label should contain " ++ show node ~::- elem node envAsmpts+      l -> "Expected one Env in label" `tltFail` ("Found " ++ (show $ length l))++assertNodeLabelAssumptions ::+  (MonadIO m, NodeDatum d) =>+    Node d i r s (TLT m) -> [[Node d i r s (TLT m)]] -> ATMST s (TLT m) ()+assertNodeLabelAssumptions node nodeLists = do+  let atms = nodeATMS node+  datumFmt <- getDatumString atms+  showLabel <- formatNodeLabel node+  labelNodeLists <- fmap (fmap envAssumptions) $ getNodeLabel node+  inGroup ("Checking node " ++ (datumFmt $ nodeDatum node)+           ++ " label " ++ showLabel) $ do+    "Expect " ++ show (length nodeLists) ++ " environments" ~:+      length nodeLists @==- length labelNodeLists+    forM_ nodeLists $ \ nodeList -> do+      nl <- formatNodes "," nodeList+      "Should have environment with assumptions " ++ nl+        ~::- elem nodeList labelNodeLists++assertAssumptionsAre ::+  (MonadIO m, NodeDatum d) =>+    ATMS d i r s (TLT m) -> [Node d i r s (TLT m)] -> ATMST s (TLT m) ()+assertAssumptionsAre = assertAtmsNodeGroup "assumptions" getAssumptions++assertContradictionsAre ::+  (MonadIO m, NodeDatum d) =>+    ATMS d i r s (TLT m) -> [Node d i r s (TLT m)] -> ATMST s (TLT m) ()+assertContradictionsAre atms nodes = do+  builtIn <- getContradictionNode atms+  assertAtmsNodeGroup "contradictions" getContradictions atms (builtIn : nodes)++assertAtmsNodeGroup ::+  (MonadIO m, NodeDatum d) =>+    String ->+      (ATMS d i r s (TLT m) -> ATMST s (TLT m) [Node d i r s (TLT m)]) ->+        ATMS d i r s (TLT m) -> [Node d i r s (TLT m)] ->+          ATMST s (TLT m) ()+assertAtmsNodeGroup title extractor atms nodes =+  inGroup ("Checking " ++ title ++ " in ATMS") $ do+    assumptionsList <- extractor atms+    "Should have " ++ (show $ length nodes) ++ " " ++ title ~:+      length nodes @==- length assumptionsList+    forM_ nodes $ \ node -> do+      show node ++ " should be present" ~::- elem node assumptionsList