fix issues

CMDL/DataTypes.hs

@@ -44,6 +44,8 @@ import Driver.Options
 
 import Network.Socket
 
+import Proofs.AbstractState (G_cons_checker)
+
 import System.IO (Handle)
 
 data CmdlGoalAxiom =
@@ -70,6 +72,7 @@ data CmdlState = CmdlState
   , output :: CmdlMessage -- ^ output of interface
   , hetsOpts :: HetcatsOpts  -- ^ hets command options
   , errorCode :: Int
+  , consCheckers :: [G_cons_checker]
   }
 
 data ProveCmdType = Prove | Disprove | ConsCheck
@@ -91,6 +94,7 @@ emptyCmdlState opts = CmdlState
   , connections = []
   , hetsOpts = opts
   , errorCode = 0
+  , consCheckers = []
 }
 
 data CmdlPrompterState = CmdlPrompterState

CMDL/Interface.hs

@@ -19,7 +19,8 @@ module CMDL.Interface where
 import System.Console.Haskeline
 import Interfaces.DataTypes
 import Comorphisms.LogicGraph (logicGraph)
-import Proofs.AbstractState (getConsCheckers, sublogicOfTheory, getCcName )
+import Proofs.AbstractState (getAllConsCheckers, sublogicOfTheory, getCcName
+                            , getListOfConsCheckers, usableCC)
 import Logic.Grothendieck
 #endif
 
@@ -81,10 +82,13 @@ cmdlComplete st (left, _) = do
        case elements pS of
         Element z _ : _ ->
           do
-           consCheckList <- getConsCheckers $ findComorphismPaths
-                                  logicGraph $ sublogicOfTheory z
-           let shortConsCList = nub $ map (\ (y, _) -> getCcName y)
-                                       consCheckList
+           let fullConsCheckerList = map fst $ getAllConsCheckers
+                 $ findComorphismPaths logicGraph $ sublogicOfTheory z
+               stateConsCheckList = consCheckers state
+               filteredConsCheckerList =
+                 filter (\cc -> elem cc stateConsCheckList) fullConsCheckList
+               shortConsCList = nub $ map getCcName filteredConsCheckList
+
            showCmdComplete state shortConsCList comps left
         [] -> showCmdComplete state [] comps left
      Nothing -> showCmdComplete state [] comps left
@@ -172,11 +176,17 @@ shellLoop st isTerminal =
                         liftIO $ writeIORef st newState'
                         shellLoop st isTerminal
 
+saveConsCheckersInState :: CmdlState -> IO CmdlState
+saveConsCheckersInState state = do
+  consCheckerList <- filterM usableCC getListOfConsCheckers
+  return $ state { consCheckers = consCheckerList }
+
 -- | The function runs hets in a shell
 cmdlRunShell :: CmdlState -> IO CmdlState
 cmdlRunShell state = do
   isTerminal <- hIsTerminalDevice stdin
-  st <- newIORef state
+  st' <- saveConsCheckersInState state
+  st <- newIORef st'
 #ifdef HASKELINE
   runInputT (shellSettings st) $ shellLoop st isTerminal
 #else

Common/ProverTools.hs

@@ -39,11 +39,14 @@ check4FileAux name env = do
 
 -- | Checks if a file exists in PATH
 checkBinary :: String -> IO (Maybe String)
-checkBinary name = fmap
-  (\ l -> if null l
+checkBinary name =
+  fmap
+    ( \l ->
+        if null l
           then Just $ "missing binary in $PATH: " ++ name
-          else Nothing)
-  $ check4FileAux name "PATH"
+          else Nothing
+    )
+    $ check4FileAux name "PATH"
 
 -- | Checks if a file exists
 check4File :: String -- ^ file name

Common/Utils.hs

@@ -191,20 +191,20 @@ is normally initially empty.  The stop list update function is given a list
 element a and the current stop list b, and returns 'Nothing' if the element is
 already in the stop list, else 'Just' b', where b' is a new stop list updated
 to contain a. -}
-nubWith :: (a -> b -> Maybe b) -> b -> [a] -> [a]
-nubWith f s es = case es of
-  [] -> []
+nubWith :: [a] -> (a -> b -> Maybe b) -> b -> [a] -> [a]
+nubWith acc f s es = case es of
+  [] -> reverse acc
   e : rs -> case f e s of
-       Just s' -> e : nubWith f s' rs
-       Nothing -> nubWith f s rs
+       Just s' -> nubWith (e:acc) f s' rs
+       Nothing -> nubWith acc f s rs
 
 nubOrd :: Ord a => [a] -> [a]
 nubOrd = nubOrdOn id
 
 nubOrdOn :: Ord b => (a -> b) -> [a] -> [a]
 nubOrdOn g = let f a s = let e = g a in
                    if Set.member e s then Nothing else Just (Set.insert e s)
-  in nubWith f Set.empty
+  in nubWith [] f Set.empty
 
 -- | safe variant of !!
 atMaybe :: [a] -> Int -> Maybe a

Logic/Grothendieck.hs

@@ -890,7 +890,7 @@ findComorphismPaths lg (G_sublogics lid sub) =
   coMors = Map.elems $ comorphisms lg
   -- compute possible compositions, but only up to depth 4
   iterateComp n l =
-    if n > 2 || l == newL then newL else iterateComp (n + 1) newL
+    if n > 0 || l == newL then newL else iterateComp (n + 1) newL
     where
     newL = nubOrd $ l ++ concatMap extend l
     -- extend comorphism list in all directions, but no cylces

Proofs/AbstractState.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable #-}
+{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable, StandaloneDeriving #-}
 {- |
 Module      :  ./Proofs/AbstractState.hs
 Description :  State data structure used by the goal management GUI.
@@ -44,10 +44,12 @@ module Proofs.AbstractState
     , getAllProvers
     , getUsableProvers
     , getConsCheckers
+    , getListOfConsCheckers
     , getAllConsCheckers
     , lookupKnownProver
     , lookupKnownConsChecker
     , autoProofAtNode
+    , usableCC
     ) where
 
 import qualified Data.Map as Map
@@ -76,6 +78,7 @@ import Logic.Comorphism
 import Logic.Coerce
 
 import Comorphisms.KnownProvers
+import Comorphisms.LogicGraph (logicGraph)
 
 import Static.GTheory
 
@@ -125,6 +128,9 @@ data G_cons_checker =
        (ConsChecker sign sentence sublogics morphism proof_tree)
   deriving (Typeable)
 
+instance Eq G_cons_checker where
+  G_cons_checker _ cc1 == G_cons_checker _ cc2 = ccName cc1 == ccName cc2
+
 instance Show G_cons_checker where
  show _ = "G_cons_checker "
 
@@ -365,9 +371,28 @@ getConsCheckers :: [AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)]
 getConsCheckers = filterM (usableCC . fst) . getAllConsCheckers
 
 getAllConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
-getAllConsCheckers = concatMap (\ cm@(Comorphism cid) ->
-    map (\ cc -> (G_cons_checker (targetLogic cid) cc, cm))
-      $ cons_checkers $ targetLogic cid)
+getAllConsCheckers lst =
+  snd $
+    foldr
+      ( \el@(G_cons_checker _ cc, _) (s, l) ->
+          if not $ Set.member (ccName cc) s
+            then (Set.insert (ccName cc) s, el : l)
+            else (s, l)
+      )
+      (Set.empty, [])
+      $
+      concatMap
+        ( \cm@(Comorphism cid) ->
+            map
+              ( \cc ->
+                  (G_cons_checker (targetLogic cid) cc, cm)
+              )
+              $ cons_checkers $ targetLogic cid
+        )
+        $ lst
+
+getListOfConsCheckers :: [G_cons_checker]
+getListOfConsCheckers = concatMap (\(Logic lid) -> map (\cc -> G_cons_checker lid cc) $ cons_checkers lid) (logics logicGraph)
 
 lookupKnownConsChecker :: Fail.MonadFail m => ProofState
     -> m (G_cons_checker, AnyComorphism)