BPS 0.1.0.0 → 0.1.1.0
raw patch · 11 files changed
+965/−360 lines, 11 filesdep +MonadRandomdep ~symbolnew-component:exe:hbps_profile
Dependencies added: MonadRandom
Dependency ranges changed: symbol
Files
- BPS.cabal +26/−2
- CHANGELOG.md +54/−0
- ChangeLog.md +0/−51
- README.md +4/−5
- src/main/haskell/app/ATMSTrun.hs +93/−27
- src/main/haskell/lib/Data/TMS/ATMS/ATMST.hs +519/−274
- src/main/haskell/lib/Data/TMS/Formatters.hs +128/−0
- src/main/haskell/prof/ATMSTrun.hs +38/−0
- src/main/haskell/prof/JTMSrun.hs +14/−0
- src/main/haskell/prof/Main.hs +87/−0
- src/test/haskell/Testers.hs +2/−1
BPS.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: BPS-version: 0.1.0.0+version: 0.1.1.0 synopsis: Translations of classic Truth Maintenance Systems description: Haskell monad transformer-based translations of two classic Truth Maintenance System algorithms of Forbus and de Kleer's /Building Problem Solvers/. This version includes justification-based and assumption-based TMS (JTMS and ATMS) implementations. See the GitHub repository <https://github.com/jphmrst/bps/>, or the Haddock documentation. category: Truth maintenance@@ -19,7 +19,7 @@ build-type: Simple extra-source-files: README.md- ChangeLog.md+ CHANGELOG.md Haskell-LICENSE.txt source-repository head@@ -31,6 +31,7 @@ Data.TMS.ATMS.ATMST Data.TMS.ChooseDebugging Data.TMS.Dbg+ Data.TMS.Formatters Data.TMS.Helpers Data.TMS.JTMS Data.TMS.MList@@ -62,6 +63,29 @@ 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++executable hbps_profile+ main-is: Main.hs+ other-modules:+ ATMSTrun+ JTMSrun+ Paths_BPS+ hs-source-dirs:+ src/main/haskell/prof+ ghc-options: -threaded -rtsopts -with-rtsopts=-N+ build-depends:+ BPS+ , MonadRandom , 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.*
+ CHANGELOG.md view
@@ -0,0 +1,54 @@++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/).++# Version 0.6.0 (Haskell 0.1.1.0, Scala 0.1.0)++ - Added `interpretations` in Haskell implementation. Only lighted+ tested at this point.++# Version 0.5.0 (Haskell 0.1.0.0, Scala 0.1.0)++ - First version with Haskell: working implementation of a monad+ transformer for the JTMS and ATMS. The `interpretations` and+ `explain-node` functions of the ATMS are not yet translated, and+ are omitted from the module API.++ - 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.
− ChangeLog.md
@@ -1,51 +0,0 @@--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.
README.md view
@@ -6,11 +6,10 @@ 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.+languages. The Haskell translation omits the two top-level function+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
src/main/haskell/app/ATMSTrun.hs view
@@ -1,34 +1,100 @@ module ATMSTrun where -import Data.Symbol+import Control.Monad.State+import Data.TMS.Formatters import Data.TMS.ATMS.ATMST +-- Corresponds to Lisp function `book-1` in src/main/lisp/atms/atest.lisp 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+ 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++ liftIO $ putStrLn "Added assumption node B"+ debug atms+ justifyNode "R4" nh [nb, nc]+ liftIO $ putStrLn "After rule R4"+ debug atms++ liftIO $ putStrLn "----------------------------------------"+ i1 <- interpretations atms [[na, nc], [nh, ng]]+ liftIO $ putStrLn "Interpretations for (a, c); (h, g): "+ forM_ i1 $ debug++ liftIO $ putStrLn "----------------------------------------"+ i2 <- interpretations atms [[nh, ng]]+ liftIO $ putStrLn "Interpretations for (h, g): "+ forM_ i2 $ debug++ liftIO $ putStrLn "----------------------------------------"+ i3 <- interpretations atms [[nh]]+ liftIO $ putStrLn "Interpretations for (h): "+ forM_ i3 $ debug++ do+ liftIO $ putStrLn "========================================"+ atms <- createATMS "Ex2"+ setInformantStringViaString atms+ setDatumStringViaString atms+ na <- createNode atms "A" True False+ nb <- createNode atms "B" True False+ nc <- createNode atms "C" True False+ nd <- createNode atms "D" True False+ ne <- createNode atms "E" True False+ nf <- createNode atms "F" True False+ ng <- createNode atms "G" True False+ nh <- createNode atms "H" True False+ nm <- createNode atms "M" False False+ nn <- createNode atms "N" False False+ np <- createNode atms "P" False False+ nq <- createNode atms "Q" False False+ nr <- createNode atms "R" False False+ ns <- createNode atms "S" False False+ nk1 <- createNode atms "K1" False False+ nk2 <- createNode atms "K2" False False+ nk3 <- createNode atms "K3" False False+ justifyNode "R01" nm [na, nb]+ justifyNode "R02" nm [nc, nd]+ justifyNode "R03" nn [nb, nc]+ justifyNode "R04" np [nc]+ justifyNode "R05" nq [nc, nd, ne]+ justifyNode "R06" nr [nf, ng]+ justifyNode "R07" ns [nf, nh]+ justifyNode "R08" nk1 [nm, np]+ justifyNode "R09" nk1 [nn, nq]+ justifyNode "R10" nk2 [nn]+ justifyNode "R11" nk2 [np]+ justifyNode "R12" nk3 [nn, nq]+ justifyNode "R13" nk3 [nq, nr, ns]+ nx <- createNode atms "X" False True+ justifyNode "X" nx [nc, nf]++ debug atms++ liftIO $ putStrLn "----------------------------------------"+ i3 <- interpretations atms [[nk3]]+ liftIO $ putStrLn "Interpretations for (k3): "+ forM_ i3 $ debug
src/main/haskell/lib/Data/TMS/ATMS/ATMST.hs view
@@ -17,10 +17,9 @@ 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.+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@@@ -43,6 +42,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE MultiParamTypeClasses #-} module Data.TMS.ATMS.ATMST ( -- * The ATMST monad@@ -84,7 +84,7 @@ Env, EnvTable, envIndex, envAssumptions, getEnvNodes, -- * Deduction and search utilities- {- interpretations, -}+ interpretations, interpretationsWithDefaults, -- ** Related to a node isTrueNode, isInNode, isInNodeByEnv, isOutNode, isNodeConsistentWith,@@ -95,27 +95,35 @@ -- * Printing and debugging - -- |Functions prefixed @format@ build a computation returning a+ -- | In addition to the functions documented below, many of the+ -- types defined in this module are instances of the classes defined+ -- in `Data.TMS.Formatters`. Specifically:+ --+ -- - __Defined for `format`, `blurb`, etc:__ `Node`, `Justification`+ --+ -- - __Defined for `pprint`:__ `Node`, `JustRule`, `Justification`,+ -- `Env`, `EnvTable`+ --+ -- - __Defined for `debug`:__ `ATMS`, `Node`, `JustRule`, `Env`+ --+ -- 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,+ debugAtmsEnvs, printAtmsStatistics, -- ** Nodes and node lists- formatNode, formatNodes, debugNode, printNode, whyNodes, whyNode, -- ** Environments, labels, and tables- debugEnv, debugEnvTable, formatNodeLabel,+ debugEnvTable, formatNodeLabel, debugNodeLabel, debugNogoods,- printEnv, printNogoods, printEnvs, printEnvTable, printTable,-- -- ** Justifications- debugJust, printJust, formatJustification+ printNogoods, printEnvs ) where +import Control.Monad import Control.Monad.State import Control.Monad.ST.Trans -- import Control.Monad.Except@@ -123,6 +131,7 @@ import Control.Monad.Extra import Data.List import Data.Symbol+import Data.TMS.Formatters import Data.TMS.Helpers import Data.TMS.MList import Data.TMS.Dbg@@ -325,9 +334,25 @@ -- |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+ adebugging :: STRef s Bool } +-- |Print the internal title signifying an ATMS.+--+-- Translated from @print-atms@ in @atms.lisp@.+instance NodeDatum d => Printed (ATMS d i r) ATMST where+ pprint atms = liftIO $ putStrLn $ "#<ATMS: " ++ atmsTitle atms ++ ">"++-- |Give a verbose printout of an `ATMS`.+instance NodeDatum d => Debugged (ATMS d i r) ATMST where+ debug atms = do+ liftIO $ putStrLn $ "=============== " ++ atmsTitle atms+ debugNodes atms+ debugJusts atms+ debugAtmsEnvs atms+ debugNogoods atms+ liftIO $ putStrLn "=============== "+ -- |Shortcut maker for reading from an `ATMS` reference. getATMSMutable :: (Monad m, NodeDatum d) =>@@ -485,12 +510,6 @@ {-# INLINE setEnqueueProcedure #-} setEnqueueProcedure = setATMSMutable atmsEnqueueProcedure --- |Print the internal title signifying an ATMS.------ Translated from @print-atms@ in @atms.lisp@.-printAtms :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()-printAtms atms = liftIO $ putStrLn $ "#<ATMS: " ++ atmsTitle atms ++ ">"- -- |Get the next node counter value, incrementing for future accesses. nextNodeCounter :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m Int nextNodeCounter jtms = sttLayer $ do@@ -546,6 +565,48 @@ instance (Monad m, NodeDatum d) => Show (Node d i r s m) where show n = "<Node " ++ show (nodeIndex n) ++ ">" +-- |`format`, `blurb`, etc. may be applied to `Node`s in an+-- `ATMST`.+instance NodeDatum d => Formatted (Node d i r) ATMST where+ format node = do+ datumFmt <- getDatumString $ nodeATMS node+ return $ datumFmt (nodeDatum node)++-- |Print a `Node` of an `ATMS` with its tag.+--+-- Translated from @print-tms-node@ in @atms.lisp@.+instance NodeDatum d => Printed (Node d i r) ATMST where+ pprint node = do+ str <- nodeString node+ liftIO $ putStr $ "<NODE: " ++ str ++ ">"++-- |Give a verbose printout of a `Node` of an `ATMS`.+instance NodeDatum d => Debugged (Node d i r) ATMST where+ debug 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: "+ debug env+ _ -> forM_ label $ \env -> do+ liftIO $ putStrLn " - "+ debug 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 ""+ -- |Shortcut maker for reading from a `Node` reference. getNodeMutable :: (Monad m, NodeDatum d) =>@@ -628,10 +689,48 @@ instance (Monad m, NodeDatum d) => Eq (JustRule d i r s m) where e1 == e2 = (justIndex e1) == (justIndex e2) +-- |Print a more verbose description of a `Just`ification rule of an+-- `ATMS`.+--+-- Translated from @print-just@ in @atms.lisp@.+instance NodeDatum d => Printed (JustRule d i r) ATMST where+ pprint rule = do+ infStr <- formatJustInformant rule+ liftIO $ putStr $ "<" ++ infStr ++ " " ++ show (justIndex rule) ++ ">"++instance NodeDatum d => Debugged (JustRule d i r) ATMST where+ debug (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)+ -- |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 +-- |`format`, `blurb`, etc. may be applied to `Node`s in an+-- `ATMST`.+instance NodeDatum d => Formatted (Justification d i r) ATMST where+ format (ByRule j) = return $ "By rule " ++ show (justIndex j)+ format (ByAssumption n) = do+ nodeFmt <- getNodeString (nodeATMS n)+ return $ "By assumption " ++ nodeFmt n+ format ByContradiction = return "By contradiction"++-- |`format`, `blurb`, etc. may be applied to `Justification`s+-- in an `ATMST`.+instance NodeDatum d => Printed (Justification d i r) ATMST where+ pprint j = case j of+ ByRule rule -> pprint rule+ ByAssumption node -> do+ liftIO $ putStr $ "Assumed node "+ pprint node+ ByContradiction -> liftIO $ putStrLn $ "By contradiction"+ -- |Explanation of why a `Node` may be believed by the `ATMS` for -- output to a query. data Explanation d i r s m =@@ -670,6 +769,39 @@ instance (Monad m, NodeDatum d) => Show (Env d i r s m) where show n = "<Env " ++ show (envIndex n) ++ ">" +-- |`format` etc. for `Env`, translated from @print-env@ in @atms.lisp@.+instance NodeDatum d => Formatted (Env d i r) ATMST where+ format env = do+ let assumptions = envAssumptions env+ case (null assumptions) of+ True -> return "<empty env>"+ False -> do+ printer <- getNodeString $ nodeATMS $ head assumptions+ strs <- mapM format assumptions+ return $ "<env:" ++ intercalate "," strs ++ ">"++-- |`pprint` for `Env`, translated from @print-env@ in @atms.lisp@.+instance NodeDatum d => Printed (Env d i r) ATMST where+ pprint env = do+ whenM (envIsNogood env) $ liftIO $ putStr "* "+ -- liftIO $ putStr "ZZZZZ "+ envString env+ liftIO $ putStrLn ""++-- |Give a verbose printout of one `Env`ironment of an `ATMS`.+instance NodeDatum d => Debugged (Env d i r) ATMST where+ debug env = do+ isNogood <- envIsNogood env+ case envAssumptions env of+ [] -> liftIO $ putStrLn "<empty env>"+ 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) ++ ")"+ -- |Shortcut maker for reading from a `Env` reference. getEnvMutable :: (Monad m, NodeDatum d) =>@@ -708,6 +840,15 @@ -- length. newtype EnvTable d i r s m = EnvTable (STArray s Int [Env d i r s m]) +-- |Print the `Env`ironments contained in the given `EnvTable`.+--+-- Translated from @print-env-table@ in @atms.lisp@.+instance NodeDatum d => Printed (EnvTable d i r) ATMST where+ pprint (EnvTable arr) = do+ let (lo, hi) = boundsSTArray arr+ forM_ [lo..hi] $ \i ->+ forMM_ (sttLayer $ readSTArray arr i) pprint+ findInEnvTable :: (Monad m, NodeDatum d) => (Env d i r s m -> Bool) -> EnvTable d i r s m ->@@ -868,7 +1009,8 @@ -- -- 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+ (Debuggable 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@@ -918,7 +1060,7 @@ -- `ATMS`. -- -- Translated from @make-contradiction@ in @atms.lisp@.-makeContradiction :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m ()+makeContradiction :: (Debuggable m, NodeDatum d) => Node d i r s m -> ATMST s m () makeContradiction node = do let atms = nodeATMS node unlessM (getNodeIsContradictory node) $ do@@ -948,7 +1090,8 @@ -- Register the new justification with the nodes that can trigger -- it.- sttLayer $ forM_ antecedents $ \node -> push just $ nodeConsequences node+ sttLayer $ forM_ antecedents $ \node ->+ {-# SCC "justifyNode.push" #-} push just $ nodeConsequences node -- Register the new justification with the ATMS itself. sttLayer $ push just $ atmsJusts atms@@ -962,14 +1105,13 @@ -- `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 :: (Debuggable 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) =>@@ -993,10 +1135,10 @@ liftIO $ putStrLn "Calling propagate with" let atms = nodeATMS $ justConsequence justRule liftIO $ putStr ". Just: "- debugJust justRule+ debug justRule case antecedent of- Just n -> debugNode n+ Just n -> debug n Nothing -> liftIO $ putStrLn ". No antecedent" envLen <- sttLayer $ mlength envs@@ -1007,16 +1149,15 @@ envm <- sttLayer $ mcar envs case envm of Nothing -> liftIO $ putStrLn "<nulled out>"- Just env -> debugEnv env+ Just env -> debug env _ -> do liftIO $ putStrLn ". Envs:" mlistFor_ sttLayer envs $ \em -> do liftIO $ putStr " . " case em of- Just e -> debugEnv e+ Just e -> debug e Nothing -> liftIO $ putStrLn "<nulled out>" --- -- Translated from @update@ in @atms.lisp@. update :: (Debuggable m, NodeDatum d) =>@@ -1069,12 +1210,10 @@ (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 ->+ Justification d i r s m -> ATMST s m ()-debugUpdateArgs envs consequence justRule = do+debugUpdateArgs envs consequence justification = do liftIO $ putStrLn "Calling update with"- let atms = nodeATMS $ justConsequence justRule- envLen <- sttLayer $ mlength envs case envLen of 0 -> liftIO $ putStrLn ". No envs"@@ -1083,21 +1222,26 @@ envm <- sttLayer $ mcar envs case envm of Nothing -> liftIO $ putStrLn "<nulled out>"- Just env -> debugEnv env+ Just env -> debug env _ -> do liftIO $ putStrLn ". Envs:" mlistFor_ sttLayer envs $ \em -> do liftIO $ putStr " . " case em of- Just e -> debugEnv e+ Just e -> debug e Nothing -> liftIO $ putStrLn "<nulled out>" liftIO $ putStr ". Consequence: "- blurbNode consequence+ blurb consequence liftIO $ putStrLn "" liftIO $ putStr ". Just: "- debugJust justRule+ case justification of+ ByRule justRule -> debug justRule+ ByAssumption node -> do+ liftIO $ putStr "by assumption "+ pprint node+ ByContradiction -> liftIO $ putStrLn "by contradiction" -- |Internal method to update the label of this node to include the -- given environments. The inclusion is not simply list extension;@@ -1187,7 +1331,7 @@ let atms = nodeATMS node liftIO $ putStr "Calling updateLabel with node "- blurbNode node+ blurb node liftIO $ putStrLn "" envLen <- sttLayer $ mlength newEnvs@@ -1198,13 +1342,13 @@ envm <- sttLayer $ mcar newEnvs case envm of Nothing -> liftIO $ putStrLn "<nulled out>"- Just env -> debugEnv env+ Just env -> debug env _ -> do liftIO $ putStrLn ". Envs:" mlistFor_ sttLayer newEnvs $ \em -> do liftIO $ putStr " . " case em of- Just e -> debugEnv e+ Just e -> debug e Nothing -> liftIO $ putStrLn "<nulled out>" debugUpdateLabelFinal ::@@ -1217,12 +1361,12 @@ [] -> liftIO $ putStrLn ". No label envs" [env] -> do liftIO $ putStr ". Single label env: "- debugEnv env+ debug env _ -> do liftIO $ putStrLn ". Final envs:" forM_ labelEnvs $ \e -> do liftIO $ putStr " . "- debugEnv e+ debug e envLen <- sttLayer $ mlength newEnvs case envLen of@@ -1232,16 +1376,16 @@ envm <- sttLayer $ mcar newEnvs case envm of Nothing -> liftIO $ putStrLn "<nulled out>"- Just env -> debugEnv env+ Just env -> debug env _ -> do liftIO $ putStrLn ". Final envs:" mlistFor_ sttLayer newEnvs $ \em -> do liftIO $ putStr " . " case em of- Just e -> debugEnv e+ Just e -> debug e Nothing -> liftIO $ putStrLn "<nulled out>" - debugNode node+ debug node -- |Update the label of node @antecedent@ to include the given @envs@ -- environments, pruning environments which are a superset of another@@ -1255,12 +1399,13 @@ (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+weave antecedent givenEnvs antecedents = {-# SCC "weave.top" #-} do $(dbg [| debugWeaveArgs antecedent givenEnvs antecedents |]) envsRef <- sttLayer $ newSTRef givenEnvs forM_ antecedents $ \node ->+ {-# SCC "weave.outer-ants" #-} unless (maybe False (node ==) antecedent) $ do $(dbg [| debugWeaveNodeAntecedent node |]) @@ -1277,11 +1422,11 @@ -- - 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 ->+ {-# SCC "weave.forEnvLoop" #-} mlistFor_ sttLayer envs $ \envmaybe -> case envmaybe of Nothing -> return () Just env -> do- forMM_ (sttLayer $ readSTRef $ nodeLabel node) $ \nodeEnv -> do+ {-# SCC "weave.forEnv" #-} forMM_ (sttLayer $ readSTRef $ nodeLabel node) $ \nodeEnv -> do $(dbg [| debugWeavePairIntro env nodeEnv |]) newEnv <- unionEnv env nodeEnv@@ -1349,7 +1494,7 @@ debugWeaveArgs antecedent givenEnvs antecedents = do liftIO $ putStrLn "Calling weave with" case antecedent of- Just n -> debugNode n+ Just n -> debug n Nothing -> liftIO $ putStrLn ". No antecedent" let atms = case antecedent of Just a -> Just $ nodeATMS a@@ -1362,7 +1507,7 @@ mlistFor_ sttLayer givenEnvs $ \em -> do liftIO $ putStr " . " case em of- Just e -> debugEnv e+ Just e -> debug e Nothing -> liftIO $ putStrLn "<nulled out>" return () _ -> return ()@@ -1421,7 +1566,7 @@ 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 :: (Debuggable m, NodeDatum d) => [Node d i r s m] -> ATMST s m Bool isInAntecedent [] = return True isInAntecedent nodes = do empty <- getEmptyEnvironment (nodeATMS (head nodes))@@ -1431,7 +1576,7 @@ -- -- 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+ (Debuggable 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@@ -1504,7 +1649,7 @@ (MonadIO m, NodeDatum d) => [Node d i r s m] -> ATMST s m () debugCreateEnvStart nodes = do liftIO $ putStrLn $ " - Running createEnv"- astr <- formatNodes "," nodes+ astr <- formats "<none>" "," nodes liftIO $ putStrLn $ " assumptions " ++ astr debugCreateEnvEnv ::@@ -1622,7 +1767,7 @@ -- -- Translated from @find-or-make-env@ in @atms.lisp@. findOrMakeEnv ::- (Monad m, NodeDatum d) =>+ (Debuggable 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@@ -1671,7 +1816,7 @@ ns = sortOn nodeIndex assumptions EnvTable envTable <- sttLayer $ readSTRef $ atmsEnvTable atms entries <- sttLayer $ readSTArray envTable $ length ns- case filter (\x -> envAssumptions x == ns) entries of+ case filter (\x -> {-# SCC "lookupEnv.pred" #-} envAssumptions x == ns) entries of [] -> return Nothing (x : _) -> return $ Just x @@ -1759,8 +1904,8 @@ 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)+ debug cenv+ format why >>= (liftIO . putStrLn) -- Translated from @set-env-contradictory@ in @atms.lisp@.@@ -1839,6 +1984,246 @@ -- nodes, under each environment in the result at least one node of -- each sublist will be believed. --+-- This function is for the case where no nodes are taken as defaults;+-- here we simply call `interpretationsWithDefaults` with an empty+-- list of defaults.+interpretations ::+ (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]+interpretations atms choiceSets = do+ $(dbg [| do formatss' choiceSets >>=+ liftIO . putStrLn . (++) "Called interpretations with "+ |])+ interpretationsWithDefaults atms choiceSets []++-- |Initial setup for @interpretations@: convert the @choiceSets@ over+-- `Node`s into structures over the nodes' labelling `Env`ironments,+-- and set up the outermost loop.+--+-- Translated from these @interpretations@ in @atms.lisp@.+--+-- > (defun interpretations (atms choice-sets &optional defaults+-- > &aux solutions)+-- > (let ( ;; ...+-- > (choice-sets (mapcar ;; Call to altSetToEnvList+-- > choice-sets)))+-- > ;; First call interpsStartPrep for this loop+-- > (dolist (choice (car choice-sets))+-- > ;; ...+-- > )+-- > ;; Then continuation is afterDepthSolutions for+-- > ;; cleanup and extend-via-defaults.+interpretationsWithDefaults ::+ (Debuggable m, NodeDatum d) =>+ ATMS d i r s m -> [[Node d i r s m]] -> [Node d i r s m] ->+ ATMST s m [Env d i r s m]+interpretationsWithDefaults atms choiceSets defaults = do+ $(dbg [| do str <- formatss' choiceSets+ liftIO $ putStr $ "- Refining choice sets " ++ str ++ "\n" |])+ choiceSetEnvLists <- mapM (altSetToEnvList atms) choiceSets+ $(dbg [| do liftIO $ putStrLn $ " Refined choice sets to environment lists:"+ formatss' choiceSetEnvLists >>=+ (liftIO . putStrLn . (++) " ") |])++ let cntn = afterDepthSolutions atms choiceSetEnvLists defaults return+ case choiceSetEnvLists of+ [] -> cntn []+ (cse:choiceSetEnvLists) ->+ interpsForOneAlternative atms cse choiceSetEnvLists cntn []++-- |Convert a `Node` passed in a choice-set of `interpretations` into+-- the list of `Env`ironments in the label of that node.+--+-- Translated from the lambda expression of the @MAPCAR@ in this+-- portion of @interpretations@ in @atms.lisp@:+--+-- > (let ( ;; ...+-- > (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)))+altSetToEnvList ::+ (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]+altSetToEnvList atms nodes = do+ mapped <- mapM getNodeLabel nodes+ $(dbg [| do s1 <- formats' nodes+ s2 <- formatss' mapped+ liftIO $ putStrLn $ " - " ++ s1 ++ " --> " ++ s2 |])+ return $ foldl (++) [] mapped++-- |The body of @interpretations@ is translated from the Lisp in a+-- continuation-passing style; this type is a shorthand for the common+-- last two argument and result types of the continuation-processing+-- functions.+type ChoiceSetCntn d i r s m =+ ([Env d i r s m] -> ATMST s m [Env d i r s m]) ->+ [Env d i r s m] ->+ ATMST s m [Env d i r s m]++-- Control, and one pass through the body, of the loop in+-- @interpretations@ (in file @atms.lisp@) in the context:+--+-- > (defun interpretations (atms choice-sets &optional defaults+-- > &aux solutions)+-- > ...+-- > (let ((*solutions* nil)+-- > (choice-sets ...))+-- > (dolist (choice (car choice-sets)) ;; This loop+--+-- Aside from debugging tracing, the body of the loop just calls+-- @getDepthSolutions@ for the first element of the list of choice+-- sets. The continuation of the @getDepthSolutions@ call is a+-- recursive call to this function on the remainder of the choice sets+-- list.+interpsForOneAlternative ::+ (Debuggable m, NodeDatum d) =>+ ATMS d i r s m -> [Env d i r s m] -> [[Env d i r s m]] ->+ ChoiceSetCntn d i r s m+interpsForOneAlternative atms [] choiceSetEnvLists k solutions = do+ $(dbg [| liftIO $ putStrLn "- Completed calls to getDepthSolutions" |])+ k solutions+interpsForOneAlternative atms (env : envs) choiceSetEnvLists k solutions = do+ getDepthSolutions atms env choiceSetEnvLists+ (interpsForOneAlternative atms envs choiceSetEnvLists k)+ solutions++-- |Translation of @get-depth-solutions1@. This function operates a+-- depth-first traversal over possible solutions. Each choice set in+-- the @choice-sets@ argument could contribute @N@ different possible+-- next-steps to building a solution; the original Lisp function+-- contains multiple self-recursive calls, one for each of these+-- possible steps. At the end of a sequence of recursive calls, one+-- construction step per choice set, the base case received a+-- constructed candidate solution. The base case considers adding a+-- to a global list of found solutions, possibly removing previous+-- solution elements made redundant by the new solution.+--+-- The translation, like the rest of the translation of+-- @interpretations@, is in continuation-passing style. Rather than a+-- global variable of solutions, the continuation receives the+-- solutions-to-date-list as its final argument. Rather than multiple+-- recursive calls which might mutate a global list, there are+-- extensions of the continuation which might manipulate the solutions+-- list they are eventually passed. The test of a constructed+-- candidate still occurs when the search reaches a leaf at a fully+-- constructed candidate, and calls its continuation with its+-- transformation of the solutions list.+--+-- > ;; 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)))))))+getDepthSolutions ::+ (Debuggable m, NodeDatum d) =>+ ATMS d i r s m -> Env d i r s m -> [[Env d i r s m]] ->+ ChoiceSetCntn d i r s m+getDepthSolutions atms cand [] k solns = do+ $(dbg [| formats' solns >>=+ liftIO . putStrLn . (++) " getDepthSolutions => "+ |])+ let filtered = filterWithNewSoln cand solns+ $(dbg [| formats' filtered >>= liftIO . putStrLn . (++) " filtered "+ |])+ k filtered+getDepthSolutions atms partial (cs : css) k solns = do+ $(dbg [| do format partial >>= liftIO . putStrLn .+ (++) "- Calling getDepthSolutions with partial solution "+ formats' cs >>= liftIO . putStrLn . (++) " choice sets "+ formats' solns >>= liftIO . putStrLn . (++) " initial solns "+ |])+ getDepthSolutionsFor atms partial cs css k solns++-- |One pass through the body of the @getDepthSolutions$ loop.+getDepthSolutionsFor ::+ (Debuggable m, NodeDatum d) =>+ ATMS d i r s m -> Env d i r s m -> [Env d i r s m] -> [[Env d i r s m]] ->+ ChoiceSetCntn d i r s m+getDepthSolutionsFor atms _ [] _ k solns = do+ $(dbg [| formats' solns >>=+ liftIO . putStrLn . (++) " getDepthSolutionsFor => " |])+ k solns+getDepthSolutionsFor atms partial (c:cs) css k solns = do+ $(dbg [| do format c >>= liftIO . putStrLn .+ (++) "- Calling getDepthSolutionsFor with first choice "+ formats' cs >>= liftIO . putStrLn . (++) " other choices "+ formatss' css >>=+ liftIO . putStrLn . (++) " other choice sets "+ formats' solns >>= liftIO . putStrLn . (++) " initial solns "+ |])+ let k' = getDepthSolutionsFor atms partial cs css k+ -- To try the next alternative of this choice set+ newPartial <- unionEnv partial c+ ifM (envIsNogood newPartial)+ (do ($(dbg [| do format newPartial >>= liftIO . putStrLn .+ (++) " nogood from unionEnv "+ |]))+ k' solns)+ (do ($(dbg [| do format partial >>= liftIO . putStrLn .+ (++) " continuing with "+ |]))+ (getDepthSolutions atms newPartial css k' solns))++-- |Implementation of the list manipulation achieved in the DO-loop at:+--+-- > ;; 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))+--+-- The purpose is to add a new solution to a list of solutions. But+-- first the solution must be tested against existing solution to find+-- cases where the new one is nondisjoint from some old one(s). If+-- the new solution is smaller than an old, then the old is redundant+-- and should be pruned. If the old solution is a subset of the new+-- solution, then the new one is redundant and need not be added to+-- the solutions list at all.+filterWithNewSoln ::+ (Monad m, NodeDatum d) => Env d i r s m -> [Env d i r s m] -> [Env d i r s m]+filterWithNewSoln env envs =+ let (redundant, _, envs') = filterWithNewSoln' env envs+ in if redundant then envs' else env : envs'++filterWithNewSoln' ::+ (Monad m, NodeDatum d) => Env d i r s m -> [Env d i r s m] ->+ (Bool, Bool, [Env d i r s m])+filterWithNewSoln' _ [] = (False, False, [])+filterWithNewSoln' e solns@(s:ss) =+ case compareEnv s e of+ EQenv -> (True, False, solns)+ S12env -> (True, False, solns)+ S21env -> let (r, c, ss') = filterWithNewSoln' e ss+ in (r, True, ss')+ DisjEnv -> let (r, c, ss') = filterWithNewSoln' e ss+ in if c+ then (r, c, s:ss')+ else (r, c, solns)+ -- TO BE TRANSLATED from @interpretations@ in @atms.lisp@. -- -- > ;; In atms.lisp@@ -1883,33 +2268,36 @@ -- > (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 >"+afterDepthSolutions ::+ (Debuggable m, NodeDatum d) =>+ ATMS d i r s m -> [[Env d i r s m]] -> [Node d i r s m] ->+ ChoiceSetCntn d i r s m+afterDepthSolutions atms choiceSets defaults k solutions =+ if (null solutions)+ then if (null choiceSets)+ then do+ empty <- getEmptyEnvironment atms+ extendSolutionsIfDefaults atms defaults k [empty]+ else return []+ else extendSolutionsIfDefaults atms defaults k solutions +extendSolutionsIfDefaults ::+ (Debuggable m, NodeDatum d) =>+ ATMS d i r s m -> [Node d i r s m] -> ChoiceSetCntn d i r s m+extendSolutionsIfDefaults atms [] k solns = k solns+extendSolutionsIfDefaults atms defaults k solns =+ extendSolutionsViaDefaults atms solns defaults k []++extendSolutionsViaDefaults ::+ (Debuggable m, NodeDatum d) =>+ ATMS d i r s m -> [Env d i r s m] -> [Node d i r s m] ->+ ChoiceSetCntn d i r s m+extendSolutionsViaDefaults atms [] defaults k = k+extendSolutionsViaDefaults atms (s:ss) defaults k =+ extendViaDefaults atms s defaults defaults+ (extendSolutionsViaDefaults atms ss defaults k)+ -- |TO BE TRANSLATED from @extend-via-defaults@ in @atms.lisp@. -- -- > ;; In atms.lisp@@ -1928,10 +2316,44 @@ -- > (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 >"+ (Debuggable m, NodeDatum d) =>+ ATMS d i r s m -> Env d i r s m -> [Node d i r s m] -> [Node d i r s m] ->+ ChoiceSetCntn d i r s m+extendViaDefaults atms baseSoln remaining original k solutions =+ extendViaDefaultsLoop atms baseSoln remaining original k solutions +extendViaDefaultsLoop ::+ (Debuggable m, NodeDatum d) =>+ ATMS d i r s m -> Env d i r s m -> [Node d i r s m] -> [Node d i r s m] ->+ ChoiceSetCntn d i r s m+extendViaDefaultsLoop atms candSoln [] original k solutions = do++ -- TODO Check (member solution *solutions* :TEST #'eq)+ --++ checkExtendedSoln atms candSoln original k solutions+extendViaDefaultsLoop atms baseSoln (d:ds) original k solutions = do+ newSoln <- consEnv d baseSoln+ let nextLoop = extendViaDefaultsLoop atms baseSoln ds original k+ ifM (envIsNogood newSoln)+ (nextLoop solutions)+ (extendViaDefaultsLoop atms newSoln ds original nextLoop solutions)++checkExtendedSoln ::+ (Debuggable m, NodeDatum d) =>+ ATMS d i r s m -> Env d i r s m -> [Node d i r s m] ->+ ChoiceSetCntn d i r s m+checkExtendedSoln atms candSoln [] k solutions = k $ candSoln : solutions+checkExtendedSoln atms candSoln (orig:origs) k solutions =+ if (elem orig (envAssumptions candSoln))+ then k solutions+ else do+ allEnv <- consEnv orig candSoln+ ifM (envIsNogood allEnv)+ (k solutions)+ (checkExtendedSoln atms candSoln origs k solutions)++ -- * Generating explanations -- |This function returns a list of justifications which form a@@ -2003,12 +2425,13 @@ -- > (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 ::+ (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+ forM_ justs pprint -- |Retrieve an `ATMS`'s `Env`ironment with the given index number. --@@ -2025,15 +2448,6 @@ 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. --@@ -2051,22 +2465,13 @@ -- -- 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+printNogoods atms = getNogoodTable atms >>= \table -> pprint 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+printEnvs atms = getEnvTable atms >>= \table -> pprint table -- |Print statistics about an `ATMS`. --@@ -2079,201 +2484,49 @@ 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 ","+ forM_ (reverse nodes) debug -- |Computation returning a one-line summary of the label of a `Node` -- of an `ATMS`.--- formatNodeLabel :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String formatNodeLabel node = do label <- getNodeLabel node case label of [] -> return "empty"- _ -> formatNodeLists ", " $ map envAssumptions label---- |Print a short summary of a `Node` of an `ATMS`.----blurbNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()-blurbNode node = formatNode node >>= liftIO . putStr---- |Print a verbose summary of a `Node` of an `ATMS`.------ Translated from @print-tms-node@ in @atms.lisp@.-printNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()-printNode node = do- str <- nodeString node- liftIO $ putStr $ "<NODE: " ++ str ++ ">"---- |Give a verbose printout of a `Node` of an `ATMS`.----debugNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()-debugNode node = do- let atms = nodeATMS node- datumFmt <- getDatumString atms- informantFmt <- getInformantString atms- liftIO $ putStrLn $ "- " ++ datumFmt (nodeDatum node)-- label <- getNodeLabel node- case label of- [] -> liftIO $ putStrLn " Empty label"- [env] -> do- liftIO $ putStr " Single environment label: "- debugEnv env- _ -> forM_ label $ \env -> do- liftIO $ putStrLn " - "- debugEnv env-- conseqs <- getNodeConsequences node- case conseqs of- [] -> liftIO $ putStrLn " Antecedent to no justifications"- _ -> do- liftIO $ putStr " Antecedent to:"- forM_ conseqs $ \ conseq -> do- liftIO $ putStr $ " " ++ informantFmt (justInformant conseq)- liftIO $ putStrLn ""---- |Computation returning a one-line summary of the reason an `ATMS`--- may believe a `Node`.----formatJustification ::- (Monad m, NodeDatum d) => Justification d i r s m -> ATMST s m String-formatJustification (ByRule j) = return $ "By rule " ++ show (justIndex j)-formatJustification (ByAssumption n) = do- nodeFmt <- getNodeString (nodeATMS n)- return $ "By assumption " ++ nodeFmt n-formatJustification ByContradiction = return "By contradiction"-+ _ -> formatss "<none>" "; " "<none>" "," $ map envAssumptions label -- |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+ forM_ (sortOn justIndex justs) $ debug -- |Computation returning a one-line summary of the informant of a -- `Just`ification rule of an `ATMS`.--- formatJustInformant :: (Monad m, NodeDatum d) => JustRule d i r s m -> ATMST s m String formatJustInformant rule = do informantFmt <- getInformantString $ nodeATMS $ justConsequence rule return $ informantFmt $ justInformant rule --- |Print a more verbose description of a `Just`ification rule of an--- `ATMS`.------ Translated from @print-just@ in @atms.lisp@.-printJust :: (MonadIO m, NodeDatum d) => JustRule d i r s m -> ATMST s m ()-printJust rule = do- infStr <- formatJustInformant rule- liftIO $ putStr $ "<" ++ infStr ++ " " ++ show (justIndex rule) ++ ">"---- |Print a more verbose description of the `Justification`.-printJustification ::- (MonadIO m, NodeDatum d) => Justification d i r s m -> ATMST s m ()-printJustification j = case j of- ByRule rule -> printJust rule- ByAssumption node -> do- liftIO $ putStr $ "Assumed node "- printNode node- ByContradiction -> liftIO $ putStrLn $ "By contradiction"---- |Give a verbose printout of one `Just`ification rule of an `ATMS`.----debugJust :: (MonadIO m, NodeDatum d) => JustRule d i r s m -> ATMST s m ()-debugJust (JustRule idx inf conseq ants) = do- let atms = nodeATMS conseq- informantFmt <- getInformantString atms- datumFmt <- getDatumString atms- liftIO $ putStrLn $ " "- ++ "[" ++ informantFmt inf ++ "." ++ show idx ++ "] "- ++ datumFmt (nodeDatum conseq) ++ " <= "- ++ intercalate ", " (map (datumFmt . nodeDatum) ants)- -- |Give a verbose printout of the `Env`ironments of an `ATMS`.--- debugAtmsEnvs :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m () debugAtmsEnvs atms = do liftIO $ putStrLn "Environments:" envTable <- getEnvTable atms debugEnvTable atms envTable --- |Give a verbose printout of one `Env`ironment of an `ATMS`.----debugEnv :: (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()-debugEnv env = do- isNogood <- envIsNogood env- case envAssumptions env of- [] -> liftIO $ putStrLn "<empty>"- nodes @ (n : _) -> do- let atms = nodeATMS n- datumFmt <- getDatumString atms- when isNogood $ liftIO $ putStr "[X] "- liftIO $ putStrLn $- (intercalate ", " $ map (datumFmt . nodeDatum) nodes)- ++ " (count " ++ show (length nodes) ++ ")"- -- |Print a short summary of a mutable list of nullable (via `Maybe`) -- `Env`ironments from an `ATMS`.--- blurbMaybeEnvMList :: (MonadIO m, NodeDatum d) => MList s (Maybe (Env d i r s m)) -> ATMST s m () blurbMaybeEnvMList mlist = do@@ -2290,7 +2543,6 @@ -- |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 ()@@ -2300,7 +2552,6 @@ -- |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@@ -2308,7 +2559,6 @@ Nothing -> liftIO $ putStr "<nothing>" -- |Print a short summary of one `Env`ironment of an `ATMS`.--- blurbEnv :: (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m () blurbEnv env = do wng <- sttLayer $ readSTRef $ envWhyNogood env@@ -2324,7 +2574,6 @@ -- |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:"@@ -2333,7 +2582,6 @@ -- |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 ()@@ -2343,36 +2591,33 @@ envs <- sttLayer $ readSTArray array i forM_ (reverse envs) $ \ env -> do liftIO $ putStr "- "- debugEnv env+ debug 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+ blurb 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+ blurb 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 =
+ src/main/haskell/lib/Data/TMS/Formatters.hs view
@@ -0,0 +1,128 @@+{-|+Module : Formatters+Description : Formatting functions, consistently named across the TMS modules+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 MultiParamTypeClasses #-}+{-# LANGUAGE AllowAmbiguousTypes #-}++module Data.TMS.Formatters where++import Control.Monad+import Control.Monad.State+import Control.Monad.Extra+import Data.List+import Data.Maybe+import Data.Foldable+import Data.Traversable++mapAndIntercalateM ::+ (Monad m, Traversable t) => (a -> m String) -> String -> t a -> m String+mapAndIntercalateM f sep xs = do+ ys <- mapM f xs+ return $ foldl1 (\s1 s2 -> s1 ++ sep ++ s2) ys++-- |Class of artifacts which can be given a short formatted+-- description in a particular monad.+--+-- This is a multi-parameter class: the first argument is the artifact+-- type; the second, the monad. Both type constructors take two+-- arguments, the state thread type used by the TMS thread, and the+-- enclosed monad constructor.+class Formatted item tmsMonad where+ -- |Format a single artifact.+ format :: (Monad m) => item s m -> tmsMonad s m String++ -- |Format several artifacts, with the given string between each+ -- pair.+ formats ::+ (Monad m, Monad (tmsMonad s m), Traversable k) =>+ String -> String -> k (item s m) -> tmsMonad s m String+ formats none _ xs | null xs = return none+ formats _ sep xs = mapAndIntercalateM format sep xs++ -- |Format several artifacts with the default separator.+ formats' ::+ (Monad m, Monad (tmsMonad s m), Traversable k) =>+ k (item s m) -> tmsMonad s m String+ formats' = formats "<none>" ","++ -- |Format several collections of artifacts, with the given string+ -- between each pair of collections, and a comma between each pair+ -- of artifacts.+ formatss ::+ (Monad m, Monad (tmsMonad s m), Traversable k1, Traversable k2) =>+ String -> String -> String -> String -> k1 (k2 (item s m)) ->+ tmsMonad s m String+ formatss outNone _ _ _ xs | null xs = return outNone+ formatss outNone outSep inNone inSep xs =+ mapAndIntercalateM (formats inNone inSep) outSep xs++ -- |Format several collections of artifacts with the default+ -- separators.+ formatss' ::+ (Monad m, Monad (tmsMonad s m), Traversable k) =>+ k (k (item s m)) -> tmsMonad s m String+ formatss' = formatss "<none>" "; " "<none>" ","++ -- |Print a short representation of an artifact to the standard+ -- output.+ blurb :: (MonadIO m, MonadIO (tmsMonad s m)) => item s m -> tmsMonad s m ()+ blurb i = format i >>= liftIO . putStr++ -- |Print a short representation of a collection of artifacts to the+ -- standard output.+ blurbs ::+ (MonadIO m, MonadIO (tmsMonad s m), Traversable k) =>+ String -> String -> k (item s m) -> tmsMonad s m ()+ blurbs none sep xs = formats none sep xs >>= liftIO . putStr++ -- |Print a short representation of a collection of collections of+ -- artifacts to the standard output.+ blurbss ::+ (MonadIO m, MonadIO (tmsMonad s m), Traversable k1, Traversable k2) =>+ String -> String -> String -> String ->+ k1 (k2 (item s m)) -> tmsMonad s m ()+ blurbss outNone outSep inNone inSep xs =+ formatss outNone outSep inNone inSep xs >>= liftIO . putStr++-- |Class of artifacts which can be printed in a `MonadIO` to the+-- standard output, possibly over multiple lines, but in a terse+-- representation shorter than for debugging.+--+-- This is a multi-parameter class: the first argument is the artifact+-- type; the second, the monad. Both type constructors take two+-- arguments, the state thread type used by the TMS thread, and the+-- enclosed monad constructor.+class Printed item tmsMonad where+ pprint :: (MonadIO m) => item s m -> tmsMonad s m ()++ pprints ::+ (MonadIO m, MonadIO (tmsMonad s m)) => [item s m] -> tmsMonad s m ()+ pprints items = forM_ items $ \i -> pprint i++ pprintss ::+ (MonadIO m, MonadIO (tmsMonad s m)) => [[item s m]] -> tmsMonad s m ()+ pprintss itemss = forM_ itemss $ \i -> pprints i++-- |Class of artifacts which can be printed for the purpose of+-- debugging in a `MonadIO` to the standard output.+--+-- This is a multi-parameter class: the first argument is the artifact+-- type; the second, the monad. Both type constructors take two+-- arguments, the state thread type used by the TMS thread, and the+-- enclosed monad constructor.+class Debugged item tmsMonad where+ debug :: (MonadIO m) => item s m -> tmsMonad s m ()
+ src/main/haskell/prof/ATMSTrun.hs view
@@ -0,0 +1,38 @@+module ATMSTrun where++import Control.Monad.State+import Data.Symbol+import Data.TMS.Formatters+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+ liftIO $ putStrLn "Added assumption node B"+ debug atms+ justifyNode "R4" nh [nb, nc]+ liftIO $ putStrLn "After rule R4"+ debug atms
+ src/main/haskell/prof/JTMSrun.hs view
@@ -0,0 +1,14 @@+module JTMSrun where++import Data.Symbol+import Data.TMS.JTMS+import Control.Monad.IO.Class++runJTMS1 :: IO (Either JtmsErr ())+runJTMS1 = runJTMST $ do+ j <- createJTMS "Ex1"+ na <- createNode j (intern "a") True False+ naName <- nodeString na+ naIn <- isInNode na+ liftIO $ putStrLn $+ "Node " ++ naName ++ " is " ++ if naIn then "in" else "out"
+ src/main/haskell/prof/Main.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE RankNTypes #-}++module Main where++import ATMSTrun+import JTMSrun+import Control.Monad.Random+import Control.Monad.Random.Class+import Data.TMS.ATMS.ATMST++main :: IO ()+main = do+ -- gen <- getStdGen+ let gen = mkStdGen 8675309 --- Fix for comparing like to like+ evalRandT (runATMST $+ makeForceATMS+ (IntRange 800 810) (IntRange 4000 4010)+ 0.1+ (IntRange 50 60) (IntRange 25 30)+ False) gen+ return ()++intSet :: (RandomGen g, Monad m) => Int -> Int -> RandT g m [Int]+intSet 0 _ = return []+intSet n m = do+ x <- getRandomR (0, m)+ xs <- intSet (n - 1) m+ return $ x : xs++intSetExcept :: (RandomGen g, Monad m) => Int -> Int -> Int -> RandT g m [Int]+intSetExcept 0 _ _ = return []+intSetExcept n m d = do+ x <- getRandomR (0, m)+ if (x == d) then intSetExcept n m d else do+ xs <- intSetExcept (n - 1) m d+ return $ x : xs++data IntRange = IntRange { lo :: Int, hi :: Int }++sample :: (RandomGen g, Monad m) => IntRange -> RandT g m Int+sample (IntRange lo hi) = getRandomR (lo, hi)++coinFlip :: (RandomGen g, Monad m) => Double -> RandT g m Bool+coinFlip p = do+ q <- getRandomR (0.0, 1.0)+ return $ q <= p++makeForceATMS ::+ (RandomGen g, MonadIO m) =>+ IntRange -> IntRange -> Double -> IntRange -> IntRange -> Bool ->+ ATMST s (RandT g m) ()+makeForceATMS assumptionsRange nonassumptionsRange contradictionChance+ justificationsPerConclusion antecedentsPerJustifications+ cyclic = do++ atms <- createATMS "Random ATMS"+ setDatumStringViaString atms+ setInformantStringViaString atms+ assumptions <- lift $ sample assumptionsRange+ nonassumptions <- lift $ sample nonassumptionsRange+ let totalNodes = assumptions + nonassumptions++ assumptionNodes <- forM [0 .. assumptions - 1] $ \i ->+ createNode atms ("Node-" ++ show i) True False++ nonassumptionNodes <- forM [0 .. nonassumptions - 1] $ \i -> do+ isContradiction <- lift $ coinFlip contradictionChance+ let idx = assumptions + i+ createNode atms ("Node-" ++ show idx) False isContradiction++ let nodes = assumptionNodes ++ nonassumptionNodes++ {-# SCC "mainLoop" #-} forM_ [0 .. nonassumptions - 1] $ \i -> do+ let idx = assumptions + i+ let node = nodes !! idx+ justifications <- lift $ sample justificationsPerConclusion+ -- lift $ lift $ liftIO $ putStrLn $+ -- show justifications ++ " justifications for node " ++ show idx+ forM_ [0 .. justifications - 1] $ \j -> do+ thisSize <- lift $ sample antecedentsPerJustifications+ antsIdx <- lift $ if cyclic+ then intSet thisSize $ idx - 1+ else intSetExcept thisSize (totalNodes - 1) j+ let ants = map (nodes !!) antsIdx+ {-# SCC "justCalls" #-} justifyNode (show i ++ "." ++ show j) node ants+ {-# SCC "forceLabel" #-} debugNodeLabel node+
src/test/haskell/Testers.hs view
@@ -35,6 +35,7 @@ import Data.Void import Data.TMS.ATMS.ATMST import Data.TMS.Helpers+import Data.TMS.Formatters import Data.TMS.Dbg import Control.Monad import Control.Monad.Extra@@ -109,7 +110,7 @@ "Expect " ++ show (length nodeLists) ++ " environments" ~: length nodeLists @==- length labelNodeLists forM_ nodeLists $ \ nodeList -> do- nl <- formatNodes "," nodeList+ nl <- formats "(no nodes)" "," nodeList "Should have environment with assumptions " ++ nl ~::- elem nodeList labelNodeLists