AnEvenTool.hs revision 3d3889e0cefcdce9b3f43c53aaa201943ac2e895
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu{-# LANGUAGE TypeSynonymInstances, FlexibleContexts,
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu FlexibleInstances, MultiParamTypeClasses #-}
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae BungiuModule : $Header$
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae BungiuDescription : The AnEven-Tool: an (An)alyzer and (Ev)aluator for (En)CL
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae BungiuCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae BungiuLicense : GPLv2 or higher, see LICENSE.txt
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae BungiuMaintainer : Ewaryst.Schulz@dfki.de
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae BungiuStability : experimental
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae BungiuPortability : non-portable (uses type-expression in type contexts)
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae BungiuThe AnEven-Tool: an (An)alyzer and (Ev)aluator for (En)CL specifications.
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae BungiuProvides functionality for interactive experimenting with EnCL specifications.
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae BungiuUsage: Load this module with 'make ghci' in order to run the commands
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu * complete the pretty printing stuff
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu - add visualization functions and bind them to commands
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu * implement the cmpenv creation
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu - get the corresponding data from the signature
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu - implement the global settings for logfiles etc...
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu * implement the output of the elim-const to eprange mapping
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae BungiuI removed a complicated autoload program logic.
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae BungiuTo see the autoload version see this module-version 15007.
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu -- (evalWithVerification, CAS (..), CASState(..))
import qualified Interfaces.Process as PC
import Control.Monad.Error (MonadError (..))
import Static.SpecLoader (getSigSensComplete, SigSens (..))
import CSL.MathematicaInterpreter
import CSL.MapleInterpreter
import CSL.Interpreter
import CSL.Logic_CSL
import CSL.DependencyGraph
import CSL.GuardedDependencies
import CSL.EPElimination
import CSL.EPRelation
import qualified CSL.SMTComparison as CMP
import CSL.AS_BASIC_CSL
import CSL.Sign
import CSL.Verification
import Common.Utils (getEnvDef)
import Common.DocUtils
import Common.Doc
import Common.AS_Annotation
import Driver.Options
import Control.Monad.State.Class
import Control.Monad.Reader
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe
import Data.List
import Data.IORef
import System.IO
import System.Directory
import System.FilePath
import Text.Regex
-- Shell handling/building imports
import System.Console.Readline
import System.Console.Shell
import qualified System.Console.Shell.Backend as ShBE
-- import System.Console.Shell.Backend.Readline
in System.Console.Haskeline -}
we compute the strict set of elements S transitively related to a, i.e.,
terminalSeg :: Ord a => Map.Map a [a] -- the relation
-> Set.Set a -- the terminalSegment of the element
terminalSeg rel el = snd $ terminalSegEx rel (Set.singleton el) el
terminalSegEx :: Ord a => Map.Map a [a] -- the relation
-> Set.Set a -- the cache
-> ( Set.Set a -- the updated cache
, Set.Set a -- the terminalSegment of the element
case Map.lookup el rel of
Nothing -> (cache, Set.empty)
let l' = filter (`Set.notMember` cache) l
cache' = foldr Set.insert cache l'
predecessorsOf :: Ord a => Map.Map a [a] -- the relation
if fe then Control.Monad.liftM getSpecNames (readFile fp) else return []
return $ joinPath [tmp, "AnEvenHistory.txt"]
defaultBackend :: ShBE.ShellBackend BackendState
, stECRgMap :: Maybe (Map.Map ConstantName EPRange)
, stCmpEnv :: Maybe CMP.VarEnv
, stECRgMap :: Maybe (Map.Map ConstantName EPRange)
, stCmpEnv :: Maybe CMP.VarEnv
getStECRgMap :: Sh AnEvenState (Map.Map ConstantName EPRange)
getStCmpEnv :: Sh AnEvenState CMP.VarEnv
updStECRgMap :: Map.Map ConstantName EPRange -> Sh AnEvenState ()
updStCmpEnv :: CMP.VarEnv -> Sh AnEvenState ()
opts <- ShBE.completeFilename defaultBackend (error "117: no bst") str
([(ConstantName, AssDefinition)], Map.Map ConstantName EPRange)
case CMP.loghandle ve of
let vm = CMP.varmap ve
liftIO $ CMP.smtCompare ve (boolRange vm r1) $ boolRange vm r2
-> PC.DTime -> Int -> String -> String -> IO CASState
testWithMapleGen :: Int -> PC.DTime -> MapleIO b -> ([Named CMD] -> MapleIO a)
vchdl <- openFile "/tmp/vc.out" WriteMode
res <- rf gr $ (withLogFile "/tmp/evalWV.txt" . g) prog