Merge remote-tracking branch 'origin/master' into shell_subst

.gitignore

@@ -8,7 +8,7 @@
 .*.swp
 .hets*
 *.bin
-hets
+./hets
 hets_server
 hets.cgi
 rev.txt
@@ -25,6 +25,8 @@ doc/*.out
 doc/UserGuide.pdf
 doc/hs2isa.ps
 docs/
+__pycache__
+.idea
 programatica/
 OWL2/*.jar
 OWL2/java/build/

ATC/Sml_cats.hs

@@ -1189,7 +1189,7 @@ instance ATermConvertibleSML SPEC where
         case aterm of
             (ShAAppl "basic" [ aa ] _) ->
                 let
-                aa' = from_sml_ShATerm (getATermByIndex1 aa att)
+                aa' = from_sml_ShATerm (getATermByIndex1 aa att) :: CASLBasicSpec
                 aa'' = G_basic_spec CASL aa'
                 in group (Syntax.AS_Structured.Basic_spec aa''
                           nullRange) group_flag

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,10 +19,12 @@ module CMDL.Interface where
 import System.Console.Haskeline
 import Interfaces.DataTypes
 import Comorphisms.LogicGraph (logicGraph)
-import Proofs.AbstractState (getConsCheckers, sublogicOfTheory, getCcName )
 import Logic.Grothendieck
 #endif
 
+import Proofs.AbstractState (getAllConsCheckers, sublogicOfTheory, getCcName
+                            , getListOfConsCheckers, usableCC)
+
 import System.IO
 
 import CMDL.Commands (getCommands)
@@ -81,10 +83,12 @@ 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 paths = findComorphismPaths logicGraph $ sublogicOfTheory z
+               fullConsCheckerList = map fst $ getAllConsCheckers $ paths
+               stateConsCheckList = consCheckers state
+               filteredConsCheckerList =
+                 filter (\cc -> elem cc stateConsCheckList) fullConsCheckerList
+               shortConsCList = nub $ map getCcName filteredConsCheckerList
            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/InjMap.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveDataTypeable, DeriveGeneric #-}
 {- |
 Module      :  ./Common/InjMap.hs
 Description :  injective maps
@@ -32,11 +32,13 @@ module Common.InjMap
 import Data.Data
 import qualified Data.Map as Map
 
+import GHC.Generics (Generic)
+
 -- | the data type of injective maps
 data InjMap a b = InjMap
     { getAToB :: Map.Map a b -- ^ the actual injective map
     , getBToA :: Map.Map b a -- ^ the inverse map
-    } deriving (Show, Eq, Ord, Typeable, Data)
+    } deriving (Show, Eq, Ord, Typeable, Data, Generic)
 
 -- | for serialization only
 unsafeConstructInjMap :: Map.Map a b -> Map.Map b a -> InjMap a b

Common/Json/ConvInstances.hs

@@ -0,0 +1,30 @@
+{-# LANGUAGE StandaloneDeriving, DeriveGeneric, FlexibleInstances, UndecidableInstances #-}
+module Common.Json.ConvInstances where
+
+import Data.Aeson
+import GHC.Generics
+import Common.Lib.SizedList as SizedList
+import Common.Json.Instances()
+import qualified Common.Lib.Rel as Rel
+import qualified Common.Lib.MapSet as MapSet
+import qualified Common.InjMap as InjMap
+import qualified Data.Relation as DRel
+import qualified Data.Relation.Internal as DRelInt
+import System.Time
+
+deriving instance Generic ClockTime
+deriving instance (Generic a, Generic b) => Generic (DRelInt.Relation a b)
+
+instance ToJSON a => ToJSON (SizedList.SizedList a)
+instance (Ord a, ToJSON a, Ord b, ToJSON b, ToJSONKey a, ToJSONKey b) => ToJSON (InjMap.InjMap a b) where
+instance (Ord a, ToJSON a, Ord b, ToJSON b, ToJSONKey a) => ToJSON (MapSet.MapSet a b) where
+instance (Ord a, ToJSON a, ToJSONKey a) => ToJSON (Rel.Rel a) where
+instance (Ord a, Ord b, Generic a, Generic b, ToJSON a, ToJSON b, ToJSONKey a, ToJSONKey b) => ToJSON (DRel.Relation a b) where
+instance ToJSON ClockTime where
+
+instance FromJSON a => FromJSON (SizedList.SizedList a)
+instance (Ord a, FromJSON a, Ord b, FromJSON b, FromJSONKey a, FromJSONKey b) => FromJSON (InjMap.InjMap a b) where
+instance (Ord a, FromJSON a, Ord b, FromJSON b, FromJSONKey a) => FromJSON (MapSet.MapSet a b) where
+instance (Ord a, FromJSON a, FromJSONKey a) => FromJSON (Rel.Rel a) where
+instance (Ord a, Ord b, Generic a, Generic b, FromJSON a, FromJSON b, FromJSONKey a, FromJSONKey b) => FromJSON (DRel.Relation a b) where
+instance FromJSON ClockTime where

Common/Json/Instances.hs

@@ -0,0 +1,11 @@
+{-# LANGUAGE StandaloneDeriving, DeriveGeneric, FlexibleInstances, UndecidableInstances #-}
+module Common.Json.Instances () where
+
+import GHC.Generics
+import Data.Aeson
+
+instance {-# OVERLAPS #-} (Generic a, GToJSON Zero (Rep a)) => ToJSON a where
+instance {-# OVERLAPS #-} (Generic a, GFromJSON Zero (Rep a)) => FromJSON a where
+
+instance {-# OVERLAPS #-} (Generic a, ToJSON a) => ToJSONKey a where
+instance {-# OVERLAPS #-} (Generic a, FromJSON a) => FromJSONKey a where

Common/Lib/MapSet.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveDataTypeable, DeriveGeneric #-}
 {- |
 Module      :  ./Common/Lib/MapSet.hs
 Description :  Maps of sets
@@ -66,6 +66,8 @@ import qualified Data.Map as Map
 import qualified Data.Set as Set
 import qualified Data.List as List
 
+import GHC.Generics (Generic)
+
 -- * functions directly working over unwrapped maps of sets
 
 -- | remove empty elements from the map
@@ -124,7 +126,7 @@ imageSet m = Set.fromList . imageList m
 
 -- | a map to non-empty sets
 newtype MapSet a b = MapSet { toMap :: Map.Map a (Set.Set b) }
-  deriving (Eq, Ord, Typeable, Data)
+  deriving (Eq, Ord, Typeable, Data, Generic)
 
 instance (Show a, Show b) => Show (MapSet a b) where
     show = show . toMap

Common/Lib/Rel.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveDataTypeable, DeriveGeneric #-}
 {- |
 Module      :  ./Common/Lib/Rel.hs
 Description :  Relations, based on maps
@@ -54,11 +54,13 @@ import qualified Data.Map as Map
 import qualified Data.Set as Set
 import qualified Data.List as List
 
+import GHC.Generics (Generic)
+
 import qualified Common.Lib.MapSet as MapSet
 
 -- | no invariant is ensured for relations!
 newtype Rel a = Rel { toMap :: Map.Map a (Set.Set a) }
-  deriving (Eq, Ord, Typeable, Data)
+  deriving (Eq, Ord, Typeable, Data, Generic)
 
 instance Show a => Show (Rel a) where
     show = show . toMap

Common/Lib/SizedList.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveDataTypeable, DeriveGeneric #-}
 {- |
 Module      :  ./Common/Lib/SizedList.hs
 Description :  lists with their size similar to Data.Edison.Seq.SizedSeq
@@ -36,7 +36,9 @@ import Prelude hiding (null, head, tail, reverse, take, drop, map)
 import Data.Data
 import qualified Data.List as List
 
-data SizedList a = N !Int [a] deriving (Show, Eq, Ord, Typeable, Data)
+import GHC.Generics (Generic)
+
+data SizedList a = N !Int [a] deriving (Show, Eq, Ord, Typeable, Data, Generic)
 
 fromList :: [a] -> SizedList a
 fromList xs = N (length xs) xs

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

@@ -60,6 +60,7 @@ module Common.Utils
   , verbMsgLn
   , verbMsgIO
   , verbMsgIOLn
+  , FileInfo(..)
   ) where
 
 import Data.Char
@@ -91,6 +92,11 @@ import System.IO.Unsafe (unsafeInterleaveIO)
 
 import Control.Monad
 
+data FileInfo = FileInfo {
+    wasDownloaded :: Bool,
+    filePath :: FilePath
+  }
+
 {- | Writes the message to the given handle unless the verbosity is less than
 the message level. -}
 verbMsg :: Handle -- ^ Output handle
@@ -185,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