3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{-# LANGUAGE TypeSynonymInstances, FlexibleContexts,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder FlexibleInstances, MultiParamTypeClasses #-}
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzDescription : The AnEven-Tool: an (An)alyzer and (Ev)aluator for (En)CL
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz specifications
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzLicense : GPLv2 or higher, see LICENSE.txt
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzMaintainer : Ewaryst.Schulz@dfki.de
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzStability : experimental
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzPortability : non-portable (uses type-expression in type contexts)
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzThe AnEven-Tool: an (An)alyzer and (Ev)aluator for (En)CL specifications.
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzProvides functionality for interactive experimenting with EnCL specifications.
e40c19038803d4a3d8914f5310a0ae8f4e683c3cEwaryst SchulzUsage: Load this module with 'make ghci' in order to run the commands
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz * complete the pretty printing stuff
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz - add visualization functions and bind them to commands
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz * implement the cmpenv creation
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz - get the corresponding data from the signature
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz - implement the global settings for logfiles etc...
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz * implement the output of the elim-const to eprange mapping
e40c19038803d4a3d8914f5310a0ae8f4e683c3cEwaryst SchulzI removed a complicated autoload program logic.
e40c19038803d4a3d8914f5310a0ae8f4e683c3cEwaryst SchulzTo see the autoload version see this module-version 15007.
dde363c92873e122a139e2db23862dfd7d265b73Ewaryst Schulz -- (evalWithVerification, CAS (..), CASState(..))
dde363c92873e122a139e2db23862dfd7d265b73Ewaryst Schulzimport qualified Interfaces.Process as PC
dde363c92873e122a139e2db23862dfd7d265b73Ewaryst Schulzimport Control.Monad.Error (MonadError (..))
dde363c92873e122a139e2db23862dfd7d265b73Ewaryst Schulzimport Static.SpecLoader (getSigSensComplete, SigSens (..))
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulzimport qualified CSL.SMTComparison as CMP
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulzimport Common.Utils (getEnvDef)
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulzimport qualified Data.Map as Map
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulzimport qualified Data.Set as Set
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulzimport qualified System.Console.Shell.Backend as ShBE
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz{- PROBLEMS with Shellac:
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz 1. When using the readline-backend and load this module in a "make ghci"
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz session, there is a segfault after invoking runShell. When running a compiled
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz program then this does not happen anymore!
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz 2. With all backends, when explicitly calling initBackend then there are
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz segfaults after exiting from the REPL or even during completion...
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz-- import System.Console.Shell.Backend.Readline
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- FIXME: It seems this module is sometimes (in newer versions?) located
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz-- ----------------------------------------------------------------------
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulzinstance Pretty Bool where
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz pretty = text . show
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulzdata CAS = Maple | Mathematica deriving (Show, Read, Eq)
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulzdata CASState = MapleState MITrans | MathematicaState MathState
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzversionInfo :: String
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzversionInfo = unlines
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz , "The AnEven-Tool: an (An)alyzer and (Ev)aluator for"
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz , "(En)CL specifications. Version 0.1"
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz , "Copyright Ewaryst Schulz, DFKI Bremen 2010"
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzshellMessage :: String
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzshellMessage = unlines
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz [ "This is free software, and you are welcome to"
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz , "redistribute it under certain conditions (GPLv2)."
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederUtils for Completion
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz Given a relation ~ represented by M through
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz a ~ b <=> b elem (lookup a in M)
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz we compute the strict set of elements S transitively related to a, i.e.,
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz S is the smallest set satisfying:
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz b elem S <=> a /= b /\ (a ~ b \/ (EX a' elem S. a' ~ b))
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzterminalSeg :: Ord a => Map.Map a [a] -- the relation
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz -> a -- the element
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz -> Set.Set a -- the terminalSegment of the element
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzterminalSeg rel el = snd $ terminalSegEx rel (Set.singleton el) el
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzterminalSegEx :: Ord a => Map.Map a [a] -- the relation
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz -> Set.Set a -- the cache
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz -> a -- the element
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz -> ( Set.Set a -- the updated cache
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz , Set.Set a -- the terminalSegment of the element
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzterminalSegEx rel cache el =
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz case Map.lookup el rel of
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz Nothing -> (cache, Set.empty)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let l' = filter (`Set.notMember` cache) l
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz cache' = foldr Set.insert cache l'
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz (cache'', iss) = mapAccumL (terminalSegEx rel) cache' l'
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in (cache'', Set.unions $ Set.fromList l' : iss)
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzpredecessorsOf :: Ord a => Map.Map a [a] -- the relation
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz -> a -- the element
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz -> [a] -- the predecessors
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzpredecessorsOf rel el = Map.keys $ Map.filter (elem el) rel
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzmatchCands :: [String] -> String -> [String]
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzmatchCands l str = filter (isPrefixOf str) l
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz-- spec extraction from source files
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzspecNameRE :: Regex
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzspecNameRE = mkRegex "^\\s*spec\\W+(\\w+)"
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetSpecNames :: String -> [String]
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetSpecNames txt = sort $ concat $ mapMaybe (matchRegex specNameRE) $ lines txt
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetSpecNamesFromFile :: Maybe FilePath -> IO [String]
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetSpecNamesFromFile Nothing = return []
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetSpecNamesFromFile (Just fp) = do
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz fe <- doesFileExist fp
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if fe then Control.Monad.liftM getSpecNames (readFile fp) else return []
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz-- use this history file
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzhistoryFilePath :: IO FilePath
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzhistoryFilePath = do
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz tmp <- getTemporaryDirectory
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz return $ joinPath [tmp, "AnEvenHistory.txt"]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederShell abstraction
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulztype BackendState = ShellacState
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz-- type BackendState = ()
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzdefaultBackend :: ShBE.ShellBackend BackendState
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzdefaultBackend = haskelineBackend
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz-- defaultBackend = readlineBackend
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederPretty Printing for AnEvenState fields
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulzclass PrettyOutput a b where
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz showPretty :: a -> b -> Doc
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulzdata POdefault = POdefault
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulzinstance PrettyOutput POdefault (SigSens a b) where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder showPretty _ = pretty . sigsensLibname
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulzinstance PrettyOutput POdefault [Named CMD] where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder showPretty _ = pretty
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulzinstance PrettyOutput POdefault [(String, Guarded EPRange)] where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder showPretty _ = pretty
e40c19038803d4a3d8914f5310a0ae8f4e683c3cEwaryst Schulzinstance PrettyOutput POdefault (GuardedMap EPRange) where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder showPretty _ = pretty
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz{- TODO: implement it for the other types...
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stDS :: Maybe (GuardedMap EPRange) -- the current dependency store
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz -- (derived from spec)
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz -- the ordered version of the current dependency store
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stODS :: Maybe [(String, Guarded EPRange)]
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz -- the guarded version of the current dependency store
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stGDS :: Maybe [(String, Guarded EPRange)]
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz -- the flattened version of the guarded dependency store
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stFDS :: Maybe [(ConstantName, AssDefinition)]
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz -- the elim constant to eprange mapping
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stECRgMap :: Maybe (Map.Map ConstantName EPRange)
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz -- the environment for the range-comparer facility
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stCmpEnv :: Maybe CMP.VarEnv
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulzvisualize :: PrettyOutput POdefault a => a -> Sh AnEvenState ()
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulzvisualize x = shellPutStrLn $ show $ showPretty POdefault x
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
dde363c92873e122a139e2db23862dfd7d265b73Ewaryst Schulzdata AnEvenConfig = AnEvenConfig
dde363c92873e122a139e2db23862dfd7d265b73Ewaryst SchulzdefaultConfig :: AnEvenConfig
dde363c92873e122a139e2db23862dfd7d265b73Ewaryst SchulzdefaultConfig = AnEvenConfig
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz{- AnEventState
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata AnEvenState =
dde363c92873e122a139e2db23862dfd7d265b73Ewaryst Schulz { stSpec :: Maybe (SigSens Sign CMD) -- current hets environment
dde363c92873e122a139e2db23862dfd7d265b73Ewaryst Schulz , stProg :: Maybe [Named CMD] -- the current program (derived from spec)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , stDS :: Maybe (GuardedMap EPRange) {- the current dependency store
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (derived from spec) -}
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz -- the ordered version of the current dependency store
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz , stODS :: Maybe [(String, Guarded EPRange)]
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz -- the guarded version of the current dependency store
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stGDS :: Maybe [(String, Guarded EPRange)]
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz -- the flattened version of the guarded dependency store
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stFDS :: Maybe [(ConstantName, AssDefinition)]
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz -- the elim constant to eprange mapping
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stECRgMap :: Maybe (Map.Map ConstantName EPRange)
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz -- the environment for the range-comparer facility
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stCmpEnv :: Maybe CMP.VarEnv
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stConfig :: AnEvenConfig -- the global settings
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz , stCompletionState :: IORef (Maybe FilePath) -- see completion-logic
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzinitialState :: IO AnEvenState
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzinitialState = do
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz csinit <- newIORef Nothing
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return AnEvenState
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz { stSpec = Nothing
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz , stProg = Nothing
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz , stDS = Nothing
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz , stODS = Nothing
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stGDS = Nothing
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stFDS = Nothing
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stECRgMap = Nothing
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz , stCmpEnv = Nothing
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz , stConfig = defaultConfig
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz , stCompletionState = csinit
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz-- accessor functions
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetStGeneric :: (AnEvenState -> Maybe a) -- the accessor function
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz -> String -- the error message
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz -> Sh AnEvenState a
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetStGeneric f msg = do
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz st <- getShellSt
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz Just a -> return a
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz Nothing -> error msg
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetStSpec :: Sh AnEvenState (SigSens Sign CMD)
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetStSpec = getStGeneric stSpec "Any specification loaded."
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetStProg :: Sh AnEvenState [Named CMD]
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetStProg = getStGeneric stProg "Program not initialized."
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetStDepStore :: Sh AnEvenState (GuardedMap EPRange)
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetStDepStore = getStGeneric stDS "Dependency Store not initialized."
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzgetStODS :: Sh AnEvenState [(String, Guarded EPRange)]
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzgetStODS = getStGeneric stODS "Ordered Dependency Store not initialized."
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzgetStGDS :: Sh AnEvenState [(String, Guarded EPRange)]
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzgetStGDS = getStGeneric stGDS "Guarded Dependency Store not initialized."
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzgetStFDS :: Sh AnEvenState [(ConstantName, AssDefinition)]
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzgetStFDS = getStGeneric stFDS "Flattened Dependency Store not initialized."
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzgetStECRgMap :: Sh AnEvenState (Map.Map ConstantName EPRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetStECRgMap = getStGeneric stECRgMap
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "Elim constant to eprange mapping not initialized."
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzgetStCmpEnv :: Sh AnEvenState CMP.VarEnv
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzgetStCmpEnv = getStGeneric stCmpEnv "Comparer environment not initialized."
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz-- update functions
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzupdStAS :: GuardedMap EPRange -> [Named CMD] -> Sh AnEvenState ()
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzupdStAS gm l =
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz let f st = st { stProg = Just l, stDS = Just gm } in modifyShellSt f
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzupdStSpec :: SigSens Sign CMD -> Sh AnEvenState ()
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzupdStSpec sp = let f st = st { stSpec = Just sp } in modifyShellSt f
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzupdStODS :: [(String, Guarded EPRange)] -> Sh AnEvenState ()
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzupdStODS ods = let f st = st { stODS = Just ods } in modifyShellSt f
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzupdStGDS :: [(String, Guarded EPRange)] -> Sh AnEvenState ()
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzupdStGDS gds = let f st = st { stGDS = Just gds } in modifyShellSt f
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzupdStFDS :: [(ConstantName, AssDefinition)] -> Sh AnEvenState ()
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzupdStFDS fds = let f st = st { stFDS = Just fds } in modifyShellSt f
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzupdStECRgMap :: Map.Map ConstantName EPRange -> Sh AnEvenState ()
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzupdStECRgMap m = let f st = st { stECRgMap = Just m } in modifyShellSt f
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzupdStCmpEnv :: CMP.VarEnv -> Sh AnEvenState ()
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzupdStCmpEnv ve = let f st = st { stCmpEnv = Just ve } in modifyShellSt f
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz{- completion-logic:
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz due to shortcomings of the Shellac interface concerning completion
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz (no context-sensitive completion possible!), we implement the following
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz completion logic using the AnEvenState:
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz * When a filename argument is completed we remember the completion in the
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz state-field stCompletionState.
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz * When a command using filename arguments is executed we clear the
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz stCompletionState field
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz * In the specname completion function we use the stCompletionState field to
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz read eventually the specfile and extract the possible specnames
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz-- see completion-logic
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzsetComplFilepath :: AnEvenState -> Maybe FilePath -> IO ()
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzsetComplFilepath st mFp =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder atomicModifyIORef (stCompletionState st) $ const (mFp, ())
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetComplFilepath :: AnEvenState -> IO (Maybe FilePath)
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzgetComplFilepath st = readIORef $ stCompletionState st
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzwriteComplState :: Maybe FilePath -> Sh AnEvenState ()
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzwriteComplState mFp = do
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz nst <- getShellSt
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz liftIO $ setComplFilepath nst mFp
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzreadComplState :: Sh AnEvenState (Maybe FilePath)
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzreadComplState = do
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz nst <- getShellSt
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz liftIO $ getComplFilepath nst
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz-- Completable dummytypes and completion instances
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz-- File completable
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulzdata SpecFile = SpecFile
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulzdata SpecName = SpecName
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulzinstance Completion SpecFile AnEvenState where
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz{- REMARK (on a Shellac issue):
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz There is no way to get the backend state from the backend other than the init
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz function, but when we call initBackend explicitly we get segfaults (later in
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz the program, not directly...).
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz For our purposes it is sufficient to use a dummy backend state because in the
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz completeFilename function this value is not touched.
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz complete _ st str = do
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz -- the backend state is not touched only passed...
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz opts <- ShBE.completeFilename defaultBackend (error "117: no bst") str
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz unless (null opts) -- see completion-logic
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz $ setComplFilepath st $ Just $ head opts
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz completableLabel _ = "<fname>"
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulzinstance Completion SpecName AnEvenState where
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz complete _ st str = do
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz mFp <- getComplFilepath st
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz l <- getSpecNamesFromFile mFp
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz return $ matchCands l str
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz completableLabel _ = "<specname>"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederBasic Interface Functions
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz1. loads the spec and translates it to signature and sentences
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzsigsensGen :: String -> String -> IO (SigSens Sign CMD)
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz2. sentences are split into guarded dependency store and program
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzsplitAS :: [Named CMD] -> (GuardedMap [EXTPARAM], [Named CMD])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder3. guarded dependency is analyzed and made disjoint,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder to apply it to a dependency store use 'fmap'
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzanalyzeGuarded :: Guarded [EXTPARAM] -> Guarded EPRange
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz4. the dependency store is sorted by the dependency relation
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzdependencySortAS :: GuardedMap EPRange -> [(String, Guarded EPRange)]
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz5. we apply extended parameter elimination to the dependency store
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederepElimination :: CompareIO m => [(String, Guarded EPRange)] ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder m [(String, Guarded EPRange)]
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz6. the guarded dependency store is flattened to an ordinary one
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzgetElimAS :: [(String, Guarded EPRange)] -> [(ConstantName, AssDefinition)]
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz6'. as 6, but this one returns in addition a mapping of elim-constants to ranges
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetElimASWithMap :: [(String, Guarded EPRange)] ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ([(ConstantName, AssDefinition)], Map.Map ConstantName EPRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercmdLoadSpecEnv :: Completable SpecFile -> Completable SpecName ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Sh AnEvenState ()
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzcmdLoadSpecEnv (Completable lfn) (Completable spn) = do
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz sigs <- liftIO $ sigsensGen lfn spn
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz updStSpec sigs
e40c19038803d4a3d8914f5310a0ae8f4e683c3cEwaryst Schulz let (gm, prg) = splitAS $ sigsensNamedSentences sigs
e40c19038803d4a3d8914f5310a0ae8f4e683c3cEwaryst Schulz updStAS (fmap analyzeGuarded gm) prg
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz writeComplState Nothing -- see completion-logic
e40c19038803d4a3d8914f5310a0ae8f4e683c3cEwaryst SchulzcmdShowDS :: Sh AnEvenState ()
e40c19038803d4a3d8914f5310a0ae8f4e683c3cEwaryst SchulzcmdShowDS = do
e40c19038803d4a3d8914f5310a0ae8f4e683c3cEwaryst Schulz ds <- getStDepStore
e40c19038803d4a3d8914f5310a0ae8f4e683c3cEwaryst SchulzcmdShowProg :: Sh AnEvenState ()
e40c19038803d4a3d8914f5310a0ae8f4e683c3cEwaryst SchulzcmdShowProg = do
e40c19038803d4a3d8914f5310a0ae8f4e683c3cEwaryst Schulz p <- getStProg
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzcmdShowODS :: Sh AnEvenState ()
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst SchulzcmdShowODS = do
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz ods <- getStODS
1a3c23972e61ef722a650eae2c6312a0dbe8f185Ewaryst Schulz visualize ods
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzstateInfo :: Sh AnEvenState ()
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzstateInfo = do
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz st <- getShellSt
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz case stSpec st of
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz Just (SigSens { sigsensLibname = ln, sigsensNode = nd }) ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder shellPutInfoLn $ show $ text "Library" <+> pretty ln <>
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder text ":" <> pretty nd <+> text "loaded."
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz _ -> shellPutInfoLn "System not initialized."
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz when (isJust $ stProg st) $ shellPutInfoLn "Program loaded."
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz when (isJust $ stDS st) $ shellPutInfoLn "Dependency Store loaded."
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz when (isJust $ stODS st) $ shellPutInfoLn "Ordered Dependency Store loaded."
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz when (isJust $ stGDS st) $ shellPutInfoLn "Guarded Dependency Store loaded."
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz when (isJust $ stFDS st) $ shellPutInfoLn "Flattened Dependency Store loaded."
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz when (isJust $ stECRgMap st) $ shellPutInfoLn "Elim-constant Map loaded."
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz when (isJust $ stCmpEnv st) $ shellPutInfoLn "Comparer Environment loaded."
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzdebugInfo :: Sh AnEvenState ()
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzdebugInfo = do
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz mFp <- readComplState
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz shellPutInfoLn $ "Debug: " ++ fp
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz fe <- liftIO $ doesFileExist fp
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz cont <- liftIO $ readFile fp
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder shellPutInfoLn ("=========================== CONTENT " ++
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "===========================")
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz shellPutInfoLn cont
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder shellPutInfoLn ("====================================" ++
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "===========================")
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz shellPutInfoLn $ unlines $ getSpecNames cont
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz _ -> shellPutInfoLn "Debug: <EMPTY>"
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzalSortDS :: Sh AnEvenState ()
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz ds <- getStDepStore
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz updStODS $ dependencySortAS ds
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzalEPElim :: Sh AnEvenState ()
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz ods <- getStODS
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz gds <- epElimination ods
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzalElimAS :: Sh AnEvenState ()
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz gds <- getStGDS
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz updStFDS $ getElimAS gds
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzalElimASWithMap :: Sh AnEvenState ()
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst SchulzalElimASWithMap = do
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz gds <- getStGDS
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz let (fds, m) = getElimASWithMap gds
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz updStECRgMap m
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz-- A REPL based on Shellac
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzrunToolREPL :: AnEvenState -> IO AnEvenState
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzrunToolREPL st = do
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz hfp <- historyFilePath
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz (mkShellDescription cmds evalFun)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder { greetingText = Just (versionInfo ++ shellMessage)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , commandStyle = OnlyCommands
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , historyFile = Just hfp
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz -- execute the shell
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz runShell desc defaultBackend st
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzrunTool :: IO AnEvenState
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzrunTool = initialState >>= runToolREPL
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst SchulzevalFun :: String -> Sh AnEvenState ()
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzevalFun [] = return ()
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst SchulzevalFun s = do
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz shellPutInfoLn $ concat ["Unknown command: ", s, "\n\nAvailable commands:\n"]
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz shellSpecial $ ShellHelp Nothing
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulzcmds :: [ShellCommand AnEvenState]
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz [ exitCommand "q"
b6c329a19d6cdd47d8843b414ae836124a5a4b88Ewaryst Schulz , helpCommand "h"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , cmd "load" cmdLoadSpecEnv ("Loads an EnCL spec from the given file-" ++
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder " and specname")
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , cmd "ods" cmdShowODS "Shows the ordered dependency store"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , cmd "ds" cmdShowDS "Shows the dependency store"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , cmd "prog" cmdShowProg "Shows the program"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , cmd "info" stateInfo "Show information on the current state"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , cmd "debug" debugInfo "Show debug information"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------ a Readline REPL
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz maybeLine <- readline "% "
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case maybeLine of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> return () -- EOF / control-d
5a5d102941f2258f590737b7923bd6b790cb4dd2Ewaryst Schulz Just "exit" -> return ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just line -> do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder addHistory line
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder putStrLn $ "The user input: " ++ show line
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederCompareIO related stuff
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulzinstance CompareIO (Sh AnEvenState) where
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz logMessage s = do
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz ve <- getStCmpEnv
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz Just hdl -> liftIO $ hPutStrLn hdl s
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz _ -> return ()
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz rangeFullCmp r1 r2 = do
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz ve <- getStCmpEnv
f0972610bff744a4503cd054f95d9c628e41d09aEwaryst Schulz liftIO $ CMP.smtCompare ve (boolRange vm r1) $ boolRange vm r2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederThe functionality for the EvalSpec-Tool
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
13452f61384ebba1447f373b1598bc47a004f460Ewaryst Schulz-- TODO: replace it with the AnEven functionality when finished.
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------------------- Shortcuts --------------------------
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzinitFlags :: (StepDebugger m, SymbolicEvaluator m) => Bool -> Bool -> m ()
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzinitFlags sm dm = do
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz setSymbolicMode sm
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz setDebugMode dm
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzevalWithVerification :: Bool -- ^ auto-close connection
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz -> CAS -> Maybe FilePath -> Maybe String -> Bool -> Bool
dde363c92873e122a139e2db23862dfd7d265b73Ewaryst Schulz -> PC.DTime -> Int -> String -> String -> IO CASState
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzevalWithVerification cl c mFp mN smode dmode to v lb sp =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let {- exitWhen s = null s || s == "q" ||
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder take 4 s == "quit" || take 4 s == "exit"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder program for initialization -}
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz prettyInfo $ text ""
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder prettyInfo $ text ("****************** Assignment " ++
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "store loaded ******************")
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz prettyInfo $ text ""
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz mE <- verifyProg prog
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz when (isJust mE) $ prettyInfo $ pretty $ fromJust mE
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz -- readEvalPrintLoop stdin stdout ">" exitWhen
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz (mit, _) <- testWithMapleGen v to (initFlags smode dmode) p lb sp
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz when cl $ mapleExit mit >> return ()
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz return $ MapleState mit
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz Mathematica -> do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (mst, _) <- testWithMathematicaGen v mFp mN
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (initFlags smode dmode) p lb sp
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz when cl $ mathematicaExit mst
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz return $ MathematicaState mst
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz-- | Returns sorted assignment store and program without EP elimination
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederassStoreAndProgSimple :: [Named CMD] -> IO ([(ConstantName, AssDefinition)],
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzassStoreAndProgSimple ncl = do
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz let (asss, prog) = splitAS ncl
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz gm = fmap analyzeGuarded asss
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz sgl = dependencySortAS gm
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz return (getSimpleAS sgl, prog)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederverifyProg :: (MessagePrinter m, StepDebugger m, VCGenerator m,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder MonadIO m, MonadError ASError m) =>
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz [Named CMD] -> m (Maybe ASError)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederverifyProg ncl = stepwiseSafe verifyingStepper $ Sequence $ map sentence ncl
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertestWithMapleGen :: Int -> PC.DTime -> MapleIO b -> ([Named CMD] -> MapleIO a)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> String -> String -> IO (MITrans, a)
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulztestWithMapleGen v to = testWithCASGen rf where
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz runWithMaple adg v to
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz [ "EnCLFunctions"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder {- , "intpakX" -- Problems with the min,max functions,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder they are remapped by this package! -}
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulztestWithMathematicaGen :: Int -> Maybe FilePath -> Maybe String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> MathematicaIO b -> ([Named CMD] -> MathematicaIO a)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> String -> String -> IO (MathState, a)
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulztestWithMathematicaGen v mFp mN = testWithCASGen rf where
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz runWithMathematica adg v mFp mN
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [ "/home/ewaryst/Hets/CSL/CAS/Mathematica.m" ]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertestWithCASGen :: (AssignmentStore as, MonadState (ASState st) as, MonadIO as)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder => (AssignmentDepGraph () -> as a -> IO (ASState st, a))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> as b -> ([Named CMD] -> as a)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> String -> String -> IO (ASState st, a)
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulztestWithCASGen rf ip f lb sp = do
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz ncl <- fmap sigsensNamedSentences $ sigsensGen lb sp
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz -- get ordered assignment store and program
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz (as, prog) <- assStoreAndProgSimple ncl
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz vchdl <- openFile "/tmp/vc.out" WriteMode
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz -- build the dependency graph
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz let gr = assDepGraphFromDescList (const $ const ()) as
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder {- make sure that the assignment store is loaded into maple before
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder the execution of f -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder g x = ip >> loadAS as >> modify (\ mit -> mit {vericondOut = Just vchdl})
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz -- start maple and run g
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz res <- rf gr $ (withLogFile "/tmp/evalWV.txt" . g) prog
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzsigsensGen :: String -> String -> IO (SigSens Sign CMD)
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst SchulzsigsensGen lb sp = do
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz hlib <- getEnvDef "HETS_LIB" $ error "Missing HETS_LIB environment variable"
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz b <- doesFileExist lb
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz let fp = if b then lb else hlib ++ "/" ++ lb
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz ho = defaultHetcatsOpts { libdirs = [hlib]
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz , verbose = 0 }
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz res <- getSigSensComplete True ho CSL fp sp
7af4df794a0e0f0cb927bd9371556ad098308983Ewaryst Schulz putStrLn "\n"