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