{-# LANGUAGE TypeSynonymInstances, FlexibleContexts,

FlexibleInstances, MultiParamTypeClasses #-}

{- |

Module : ./CSL/AnEvenTool.hs

Description : The AnEven-Tool: an (An)alyzer and (Ev)aluator for (En)CL

specifications

Copyright : (c) Ewaryst Schulz, DFKI Bremen 2010

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Ewaryst.Schulz@dfki.de

Stability : experimental

Portability : non-portable (uses type-expression in type contexts)

The AnEven-Tool: an (An)alyzer and (Ev)aluator for (En)CL specifications.

Provides functionality for interactive experimenting with EnCL specifications.

Usage: Load this module with 'make ghci' in order to run the commands

-}

{- TODO:

* complete the pretty printing stuff

- add visualization functions and bind them to commands

* implement the cmpenv creation

- get the corresponding data from the signature

- implement the global settings for logfiles etc...

* implement the output of the elim-const to eprange mapping

-}

{-

REMARK:

I removed a complicated autoload program logic.

To see the autoload version see this module-version 15007.

-}

module CSL.AnEvenTool

-- (evalWithVerification, CAS (..), CASState(..))

where

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.ShellMonad

{- PROBLEMS with Shellac:

1. When using the readline-backend and load this module in a "make ghci"

session, there is a segfault after invoking runShell. When running a compiled

program then this does not happen anymore!

2. With all backends, when explicitly calling initBackend then there are

segfaults after exiting from the REPL or even during completion...

-}

-- import System.Console.Shell.Backend.Readline

import System.Console.Shell.Backend.Haskeline

{- FIXME: It seems this module is sometimes (in newer versions?) located

in System.Console.Haskeline -}

-- ----------------------------------------------------------------------

instance Pretty Bool where

pretty = text . show

data CAS = Maple | Mathematica deriving (Show, Read, Eq)

data CASState = MapleState MITrans | MathematicaState MathState

{- ----------------------------------------------------------------------

AnEven-Tool

---------------------------------------------------------------------- -}

versionInfo :: String

versionInfo = unlines

[ ""

, "The AnEven-Tool: an (An)alyzer and (Ev)aluator for"

, "(En)CL specifications. Version 0.1"

, "Copyright Ewaryst Schulz, DFKI Bremen 2010"

, ""

]

shellMessage :: String

shellMessage = unlines

[ "This is free software, and you are welcome to"

, "redistribute it under certain conditions (GPLv2)."

]

{- ----------------------------------------------------------------------

Utils for Completion

---------------------------------------------------------------------- -}

{-

Given a relation ~ represented by M through

a ~ b <=> b elem (lookup a in M)

we compute the strict set of elements S transitively related to a, i.e.,

S is the smallest set satisfying:

b elem S <=> a /= b /\ (a ~ b \/ (EX a' elem S. a' ~ b))

-}

terminalSeg :: Ord a => Map.Map a [a] -- the relation

-> a -- the element

-> 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

-> a -- the element

-> ( Set.Set a -- the updated cache

, Set.Set a -- the terminalSegment of the element

)

terminalSegEx rel cache el =

case Map.lookup el rel of

Nothing -> (cache, Set.empty)

Just l ->

let l' = filter (`Set.notMember` cache) l

cache' = foldr Set.insert cache l'

(cache'', iss) = mapAccumL (terminalSegEx rel) cache' l'

in (cache'', Set.unions $ Set.fromList l' : iss)

predecessorsOf :: Ord a => Map.Map a [a] -- the relation

-> a -- the element

-> [a] -- the predecessors

predecessorsOf rel el = Map.keys $ Map.filter (elem el) rel

matchCands :: [String] -> String -> [String]

matchCands l str = filter (isPrefixOf str) l

-- spec extraction from source files

specNameRE :: Regex

specNameRE = mkRegex "^\\s*spec\\W+(\\w+)"

getSpecNames :: String -> [String]

getSpecNames txt = sort $ concat $ mapMaybe (matchRegex specNameRE) $ lines txt

getSpecNamesFromFile :: Maybe FilePath -> IO [String]

getSpecNamesFromFile Nothing = return []

getSpecNamesFromFile (Just fp) = do

fe <- doesFileExist fp

if fe then Control.Monad.liftM getSpecNames (readFile fp) else return []

-- use this history file

historyFilePath :: IO FilePath

historyFilePath = do

tmp <- getTemporaryDirectory

return $ joinPath [tmp, "AnEvenHistory.txt"]

{- ----------------------------------------------------------------------

Shell abstraction

---------------------------------------------------------------------- -}

type BackendState = ShellacState

-- type BackendState = ()

defaultBackend :: ShBE.ShellBackend BackendState

defaultBackend = haskelineBackend

-- defaultBackend = readlineBackend

{- ----------------------------------------------------------------------

Pretty Printing for AnEvenState fields

---------------------------------------------------------------------- -}

class PrettyOutput a b where

showPretty :: a -> b -> Doc

data POdefault = POdefault

instance PrettyOutput POdefault (SigSens a b) where

showPretty _ = pretty . sigsensLibname

instance PrettyOutput POdefault [Named CMD] where

showPretty _ = pretty

instance PrettyOutput POdefault [(String, Guarded EPRange)] where

showPretty _ = pretty

instance PrettyOutput POdefault (GuardedMap EPRange) where

showPretty _ = pretty

{- TODO: implement it for the other types...

, stDS :: Maybe (GuardedMap EPRange) -- the current dependency store

-- (derived from spec)

-- the ordered version of the current dependency store

, stODS :: Maybe [(String, Guarded EPRange)]

-- the guarded version of the current dependency store

, stGDS :: Maybe [(String, Guarded EPRange)]

-- the flattened version of the guarded dependency store

, stFDS :: Maybe [(ConstantName, AssDefinition)]

-- the elim constant to eprange mapping

, stECRgMap :: Maybe (Map.Map ConstantName EPRange)

-- the environment for the range-comparer facility

, stCmpEnv :: Maybe CMP.VarEnv

-}

visualize :: PrettyOutput POdefault a => a -> Sh AnEvenState ()

visualize x = shellPutStrLn $ show $ showPretty POdefault x

{- ----------------------------------------------------------------------

Basic Datatypes

---------------------------------------------------------------------- -}

data AnEvenConfig = AnEvenConfig

defaultConfig :: AnEvenConfig

defaultConfig = AnEvenConfig

{- AnEventState

-}

data AnEvenState =

AnEvenState

{ stSpec :: Maybe (SigSens Sign CMD) -- current hets environment

, stProg :: Maybe [Named CMD] -- the current program (derived from spec)

, stDS :: Maybe (GuardedMap EPRange) {- the current dependency store

(derived from spec) -}

-- the ordered version of the current dependency store

, stODS :: Maybe [(String, Guarded EPRange)]

-- the guarded version of the current dependency store

, stGDS :: Maybe [(String, Guarded EPRange)]

-- the flattened version of the guarded dependency store

, stFDS :: Maybe [(ConstantName, AssDefinition)]

-- the elim constant to eprange mapping

, stECRgMap :: Maybe (Map.Map ConstantName EPRange)

-- the environment for the range-comparer facility

, stCmpEnv :: Maybe CMP.VarEnv

, stConfig :: AnEvenConfig -- the global settings

, stCompletionState :: IORef (Maybe FilePath) -- see completion-logic

}

initialState :: IO AnEvenState

initialState = do

csinit <- newIORef Nothing

return AnEvenState

{ stSpec = Nothing

, stProg = Nothing

, stDS = Nothing

, stODS = Nothing

, stGDS = Nothing

, stFDS = Nothing

, stECRgMap = Nothing

, stCmpEnv = Nothing

, stConfig = defaultConfig

, stCompletionState = csinit

}

-- accessor functions

getStGeneric :: (AnEvenState -> Maybe a) -- the accessor function

-> String -- the error message

-> Sh AnEvenState a

getStGeneric f msg = do

st <- getShellSt

case f st of

Just a -> return a

Nothing -> error msg

getStSpec :: Sh AnEvenState (SigSens Sign CMD)

getStSpec = getStGeneric stSpec "Any specification loaded."

getStProg :: Sh AnEvenState [Named CMD]

getStProg = getStGeneric stProg "Program not initialized."

getStDepStore :: Sh AnEvenState (GuardedMap EPRange)

getStDepStore = getStGeneric stDS "Dependency Store not initialized."

getStODS :: Sh AnEvenState [(String, Guarded EPRange)]

getStODS = getStGeneric stODS "Ordered Dependency Store not initialized."

getStGDS :: Sh AnEvenState [(String, Guarded EPRange)]

getStGDS = getStGeneric stGDS "Guarded Dependency Store not initialized."

getStFDS :: Sh AnEvenState [(ConstantName, AssDefinition)]

getStFDS = getStGeneric stFDS "Flattened Dependency Store not initialized."

getStECRgMap :: Sh AnEvenState (Map.Map ConstantName EPRange)

getStECRgMap = getStGeneric stECRgMap

"Elim constant to eprange mapping not initialized."

getStCmpEnv :: Sh AnEvenState CMP.VarEnv

getStCmpEnv = getStGeneric stCmpEnv "Comparer environment not initialized."

-- update functions

updStAS :: GuardedMap EPRange -> [Named CMD] -> Sh AnEvenState ()

updStAS gm l =

let f st = st { stProg = Just l, stDS = Just gm } in modifyShellSt f

updStSpec :: SigSens Sign CMD -> Sh AnEvenState ()

updStSpec sp = let f st = st { stSpec = Just sp } in modifyShellSt f

updStODS :: [(String, Guarded EPRange)] -> Sh AnEvenState ()

updStODS ods = let f st = st { stODS = Just ods } in modifyShellSt f

updStGDS :: [(String, Guarded EPRange)] -> Sh AnEvenState ()

updStGDS gds = let f st = st { stGDS = Just gds } in modifyShellSt f

updStFDS :: [(ConstantName, AssDefinition)] -> Sh AnEvenState ()

updStFDS fds = let f st = st { stFDS = Just fds } in modifyShellSt f

updStECRgMap :: Map.Map ConstantName EPRange -> Sh AnEvenState ()

updStECRgMap m = let f st = st { stECRgMap = Just m } in modifyShellSt f

updStCmpEnv :: CMP.VarEnv -> Sh AnEvenState ()

updStCmpEnv ve = let f st = st { stCmpEnv = Just ve } in modifyShellSt f

{- completion-logic:

due to shortcomings of the Shellac interface concerning completion

(no context-sensitive completion possible!), we implement the following

completion logic using the AnEvenState:

* When a filename argument is completed we remember the completion in the

state-field stCompletionState.

* When a command using filename arguments is executed we clear the

stCompletionState field

* In the specname completion function we use the stCompletionState field to

read eventually the specfile and extract the possible specnames

-}

-- see completion-logic

setComplFilepath :: AnEvenState -> Maybe FilePath -> IO ()

setComplFilepath st mFp =

atomicModifyIORef (stCompletionState st) $ const (mFp, ())

getComplFilepath :: AnEvenState -> IO (Maybe FilePath)

getComplFilepath st = readIORef $ stCompletionState st

writeComplState :: Maybe FilePath -> Sh AnEvenState ()

writeComplState mFp = do

nst <- getShellSt

liftIO $ setComplFilepath nst mFp

readComplState :: Sh AnEvenState (Maybe FilePath)

readComplState = do

nst <- getShellSt

liftIO $ getComplFilepath nst

-- Completable dummytypes and completion instances

-- File completable

data SpecFile = SpecFile

data SpecName = SpecName

instance Completion SpecFile AnEvenState where

{- REMARK (on a Shellac issue):

There is no way to get the backend state from the backend other than the init

function, but when we call initBackend explicitly we get segfaults (later in

the program, not directly...).

For our purposes it is sufficient to use a dummy backend state because in the

completeFilename function this value is not touched.

-}

complete _ st str = do

-- the backend state is not touched only passed...

opts <- ShBE.completeFilename defaultBackend (error "117: no bst") str

unless (null opts) -- see completion-logic

$ setComplFilepath st $ Just $ head opts

return opts

completableLabel _ = "<fname>"

instance Completion SpecName AnEvenState where

complete _ st str = do

mFp <- getComplFilepath st

l <- getSpecNamesFromFile mFp

return $ matchCands l str

completableLabel _ = "<specname>"

{- ----------------------------------------------------------------------

Basic Interface Functions

---------------------------------------------------------------------- -}

{-

1. loads the spec and translates it to signature and sentences

sigsensGen :: String -> String -> IO (SigSens Sign CMD)

2. sentences are split into guarded dependency store and program

splitAS :: [Named CMD] -> (GuardedMap [EXTPARAM], [Named CMD])

3. guarded dependency is analyzed and made disjoint,

to apply it to a dependency store use 'fmap'

analyzeGuarded :: Guarded [EXTPARAM] -> Guarded EPRange

4. the dependency store is sorted by the dependency relation

dependencySortAS :: GuardedMap EPRange -> [(String, Guarded EPRange)]

5. we apply extended parameter elimination to the dependency store

epElimination :: CompareIO m => [(String, Guarded EPRange)] ->

m [(String, Guarded EPRange)]

6. the guarded dependency store is flattened to an ordinary one

getElimAS :: [(String, Guarded EPRange)] -> [(ConstantName, AssDefinition)]

6'. as 6, but this one returns in addition a mapping of elim-constants to ranges

getElimASWithMap :: [(String, Guarded EPRange)] ->

([(ConstantName, AssDefinition)], Map.Map ConstantName EPRange)

-}

-- 1.

cmdLoadSpecEnv :: Completable SpecFile -> Completable SpecName ->

Sh AnEvenState ()

cmdLoadSpecEnv (Completable lfn) (Completable spn) = do

sigs <- liftIO $ sigsensGen lfn spn

updStSpec sigs

let (gm, prg) = splitAS $ sigsensNamedSentences sigs

updStAS (fmap analyzeGuarded gm) prg

writeComplState Nothing -- see completion-logic

-- 4. viz

cmdShowDS :: Sh AnEvenState ()

cmdShowDS = do

ds <- getStDepStore

visualize ds

cmdShowProg :: Sh AnEvenState ()

cmdShowProg = do

p <- getStProg

visualize p

cmdShowODS :: Sh AnEvenState ()

cmdShowODS = do

ods <- getStODS

visualize ods

-- ??.

stateInfo :: Sh AnEvenState ()

stateInfo = do

st <- getShellSt

case stSpec st of

Just (SigSens { sigsensLibname = ln, sigsensNode = nd }) ->

shellPutInfoLn $ show $ text "Library" <+> pretty ln <>

text ":" <> pretty nd <+> text "loaded."

_ -> shellPutInfoLn "System not initialized."

when (isJust $ stProg st) $ shellPutInfoLn "Program loaded."

when (isJust $ stDS st) $ shellPutInfoLn "Dependency Store loaded."

when (isJust $ stODS st) $ shellPutInfoLn "Ordered Dependency Store loaded."

when (isJust $ stGDS st) $ shellPutInfoLn "Guarded Dependency Store loaded."

when (isJust $ stFDS st) $ shellPutInfoLn "Flattened Dependency Store loaded."

when (isJust $ stECRgMap st) $ shellPutInfoLn "Elim-constant Map loaded."

when (isJust $ stCmpEnv st) $ shellPutInfoLn "Comparer Environment loaded."

debugInfo :: Sh AnEvenState ()

debugInfo = do

mFp <- readComplState

case mFp of

Just fp ->

do

shellPutInfoLn $ "Debug: " ++ fp

fe <- liftIO $ doesFileExist fp

when fe $

do

cont <- liftIO $ readFile fp

shellPutInfoLn ("=========================== CONTENT " ++

"===========================")

shellPutInfoLn cont

shellPutInfoLn ("====================================" ++

"===========================")

shellPutInfoLn $ unlines $ getSpecNames cont

_ -> shellPutInfoLn "Debug: <EMPTY>"

-- 4.

alSortDS :: Sh AnEvenState ()

alSortDS = do

ds <- getStDepStore

updStODS $ dependencySortAS ds

-- 5.

alEPElim :: Sh AnEvenState ()

alEPElim = do

ods <- getStODS

gds <- epElimination ods

updStGDS gds

-- 6.

alElimAS :: Sh AnEvenState ()

alElimAS = do

gds <- getStGDS

updStFDS $ getElimAS gds

-- 6'.

alElimASWithMap :: Sh AnEvenState ()

alElimASWithMap = do

gds <- getStGDS

let (fds, m) = getElimASWithMap gds

updStFDS fds

updStECRgMap m

-- A REPL based on Shellac

runToolREPL :: AnEvenState -> IO AnEvenState

runToolREPL st = do

hfp <- historyFilePath

let desc =

(mkShellDescription cmds evalFun)

{ greetingText = Just (versionInfo ++ shellMessage)

, commandStyle = OnlyCommands

, historyFile = Just hfp

}

-- execute the shell

runShell desc defaultBackend st

runTool :: IO AnEvenState

runTool = initialState >>= runToolREPL

evalFun :: String -> Sh AnEvenState ()

evalFun [] = return ()

evalFun s = do

shellPutInfoLn $ concat ["Unknown command: ", s, "\n\nAvailable commands:\n"]

shellSpecial $ ShellHelp Nothing

cmds :: [ShellCommand AnEvenState]

cmds =

[ exitCommand "q"

, helpCommand "h"

, cmd "load" cmdLoadSpecEnv ("Loads an EnCL spec from the given file-" ++

" and specname")

, cmd "ods" cmdShowODS "Shows the ordered dependency store"

, cmd "ds" cmdShowDS "Shows the dependency store"

, cmd "prog" cmdShowProg "Shows the program"

, cmd "info" stateInfo "Show information on the current state"

, cmd "debug" debugInfo "Show debug information"

]

-- ------ a Readline REPL

rEPL :: IO ()

rEPL = do

maybeLine <- readline "% "

case maybeLine of

Nothing -> return () -- EOF / control-d

Just "exit" -> return ()

Just line -> do

addHistory line

putStrLn $ "The user input: " ++ show line

rEPL

{- ----------------------------------------------------------------------

CompareIO related stuff

---------------------------------------------------------------------- -}

instance CompareIO (Sh AnEvenState) where

logMessage s = do

ve <- getStCmpEnv

case CMP.loghandle ve of

Just hdl -> liftIO $ hPutStrLn hdl s

_ -> return ()

rangeFullCmp r1 r2 = do

ve <- getStCmpEnv

let vm = CMP.varmap ve

liftIO $ CMP.smtCompare ve (boolRange vm r1) $ boolRange vm r2

{- ----------------------------------------------------------------------

The functionality for the EvalSpec-Tool

---------------------------------------------------------------------- -}

-- TODO: replace it with the AnEven functionality when finished.

-- ------------------------- Shortcuts --------------------------

initFlags :: (StepDebugger m, SymbolicEvaluator m) => Bool -> Bool -> m ()

initFlags sm dm = do

setSymbolicMode sm

setDebugMode dm

evalWithVerification :: Bool -- ^ auto-close connection

-> CAS -> Maybe FilePath -> Maybe String -> Bool -> Bool

-> PC.DTime -> Int -> String -> String -> IO CASState

evalWithVerification cl c mFp mN smode dmode to v lb sp =

let {- exitWhen s = null s || s == "q" ||

take 4 s == "quit" || take 4 s == "exit"

program for initialization -}

p prog = do

prettyInfo $ text ""

prettyInfo $ text ("****************** Assignment " ++

"store loaded ******************")

prettyInfo $ text ""

mE <- verifyProg prog

when (isJust mE) $ prettyInfo $ pretty $ fromJust mE

-- readEvalPrintLoop stdin stdout ">" exitWhen

in case c of

Maple -> do

(mit, _) <- testWithMapleGen v to (initFlags smode dmode) p lb sp

when cl $ mapleExit mit >> return ()

return $ MapleState mit

Mathematica -> do

(mst, _) <- testWithMathematicaGen v mFp mN

(initFlags smode dmode) p lb sp

when cl $ mathematicaExit mst

return $ MathematicaState mst

-- | Returns sorted assignment store and program without EP elimination

assStoreAndProgSimple :: [Named CMD] -> IO ([(ConstantName, AssDefinition)],

[Named CMD])

assStoreAndProgSimple ncl = do

let (asss, prog) = splitAS ncl

gm = fmap analyzeGuarded asss

sgl = dependencySortAS gm

return (getSimpleAS sgl, prog)

verifyProg :: (MessagePrinter m, StepDebugger m, VCGenerator m,

MonadIO m, MonadError ASError m) =>

[Named CMD] -> m (Maybe ASError)

verifyProg ncl = stepwiseSafe verifyingStepper $ Sequence $ map sentence ncl

testWithMapleGen :: Int -> PC.DTime -> MapleIO b -> ([Named CMD] -> MapleIO a)

-> String -> String -> IO (MITrans, a)

testWithMapleGen v to = testWithCASGen rf where

rf adg =

runWithMaple adg v to

[ "EnCLFunctions"

{- , "intpakX" -- Problems with the min,max functions,

they are remapped by this package! -}

]

testWithMathematicaGen :: Int -> Maybe FilePath -> Maybe String

-> MathematicaIO b -> ([Named CMD] -> MathematicaIO a)

-> String -> String -> IO (MathState, a)

testWithMathematicaGen v mFp mN = testWithCASGen rf where

rf adg =

runWithMathematica adg v mFp mN

[ "/home/ewaryst/Hets/CSL/CAS/Mathematica.m" ]

testWithCASGen :: (AssignmentStore as, MonadState (ASState st) as, MonadIO as)

=> (AssignmentDepGraph () -> as a -> IO (ASState st, a))

-> as b -> ([Named CMD] -> as a)

-> String -> String -> IO (ASState st, a)

testWithCASGen rf ip f lb sp = do

ncl <- fmap sigsensNamedSentences $ sigsensGen lb sp

-- get ordered assignment store and program

(as, prog) <- assStoreAndProgSimple ncl

vchdl <- openFile "/tmp/vc.out" WriteMode

-- build the dependency graph

let gr = assDepGraphFromDescList (const $ const ()) as

{- make sure that the assignment store is loaded into maple before

the execution of f -}

g x = ip >> loadAS as >> modify (\ mit -> mit {vericondOut = Just vchdl})

>> f x

-- start maple and run g

res <- rf gr $ (withLogFile "/tmp/evalWV.txt" . g) prog

hClose vchdl

return res

{- ----------------------------------------------------------------------

Temp tools

---------------------------------------------------------------------- -}

sigsensGen :: String -> String -> IO (SigSens Sign CMD)

sigsensGen lb sp = do

hlib <- getEnvDef "HETS_LIB" $ error "Missing HETS_LIB environment variable"

b <- doesFileExist lb

let fp = if b then lb else hlib ++ "/" ++ lb

ho = defaultHetcatsOpts { libdirs = [hlib]

, verbose = 0 }

res <- getSigSensComplete True ho CSL fp sp

putStrLn "\n"

return res