f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder{- |

c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederDescription : Test environment for CSL

fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan PascanuCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicense : GPLv2 or higher, see LICENSE.txt

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiMaintainer : Ewaryst.Schulz@dfki.de

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiStability : experimental

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederPortability : non-portable (uses type-expression in type contexts)

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian MaederThis file is for experimenting with the Interpreter instances

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederand general static analysis tools

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder-}

da955132262baab309a50fdffe228c9efe68251dCui Jian

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maedermodule CSL.InteractiveTests where

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport CSL.MapleInterpreter

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maederimport CSL.ReduceInterpreter

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maederimport CSL.Reduce_Interface

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maederimport CSL.Interpreter

4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maederimport CSL.Transformation

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport CSL.ExtendedParameter

fa388aea9cef5f9734fec346159899a74432ce26Christian Maederimport CSL.Logic_CSL

3c4e64e0b4361a24275ee8f308fa965ab1e52f2eHeng Jiangimport CSL.AS_BASIC_CSL

fa388aea9cef5f9734fec346159899a74432ce26Christian Maederimport CSL.Parse_AS_Basic (parseResult, extparam, pComma, pSemi)

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maederimport CSL.Sign

59fddbdd745a05adeaf655b617ab8da947903832Christian Maeder

cfaa17b0d2ed0a663f0a4f18b23f98ab876c2f40Christian Maederimport Common.Utils (getEnvDef)

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maederimport Common.IOS

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederimport Common.Result (diags, printDiags, resultToMaybe)

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maederimport Common.ResultT

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport Common.Lexer as Lexer

c0c2380bced8159ff0297ece14eba948bd236471Christian Maederimport Common.Parsec

da333ffa6336cf59a4071fcddad358c5eafd3e61Sonja Gröningimport Text.ParserCombinators.Parsec

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder

5b50a0fb9834540caf04471389df975fbd356ca3Razvan Pascanu-- the process communication interface

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanuimport qualified Interfaces.Process as PC

16281c97e3e04f9f88c806d7da79feb106dbee2aTill Mossakowski

66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu-- README: In order to work correctly link the Test.hs in the Hets-root dir to Main.hs (ln -s Test.hs Main.hs)

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport Main (getSigSens)

74885352ea11b26253d453af28dc904dadc4d530Christian Maeder

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederimport Control.Monad.State (StateT(..))

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Control.Monad (liftM)

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Data.Maybe (fromJust, fromMaybe)

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Data.Time.Clock

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport qualified Data.Map as Map

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- ----------------------------------------------------------------------

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- * general test functions

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- ----------------------------------------------------------------------

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maedertestspecs =

8955ea64c61a6e8b96b7696021863afd1a75f6daRazvan Pascanu [ (44, ("/CSL/EN1591.het", "EN1591"))

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ]

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederl1 :: Int -> IO (Sign, [(String, CMD)])

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederl1 i = do

fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu let (lb, sp) = fromMaybe ("/CSL/Tests.het", "Test" ++ show i)

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder $ Prelude.lookup i testspecs

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

fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu getSigSens CSL (hlib ++ lb) sp

fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu

ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühlsig :: Int -> IO Sign

ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühlsig = fmap fst . l1

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- Check if the order is broken or not!

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maedersens :: Int -> IO [(String, CMD)]

c0c2380bced8159ff0297ece14eba948bd236471Christian Maedersens = fmap snd . l1

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

c0c2380bced8159ff0297ece14eba948bd236471Christian Maedercmds :: Int -> IO [CMD]

fa388aea9cef5f9734fec346159899a74432ce26Christian Maedercmds = fmap (map snd) . sens

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- time measurement, pendant of the time shell command

fa388aea9cef5f9734fec346159899a74432ce26Christian Maedertime :: IO a -> IO a

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maedertime p = do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder t <- getCurrentTime

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder res <- p

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder t' <- getCurrentTime

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder putStrLn $ show $ diffUTCTime t' t

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder return res

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder-- ----------------------------------------------------------------------

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- * calculator test functions

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- ----------------------------------------------------------------------

f1dec6898638ba1131a9fadbc4d1544c93dfabb0Klaus Luettich

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederrunTest :: ResultT (IOS b) a -> b -> IO a

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederrunTest cmd r = fmap fromJust $ runTestM cmd r

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian MaederrunTestM :: ResultT (IOS b) a -> b -> IO (Maybe a)

runTestM cmd r = fmap (resultToMaybe . fst) $ runIOS r $ runResultT cmd

runTest_ :: ResultT (IOS b) a -> b -> IO (a, b)

runTest_ cmd r = do

(res, r') <- runIOS r $ runResultT cmd

return (fromJust $ resultToMaybe res, r')

evalL :: CalculationSystem (ResultT (IOS b)) => b

-> Int -- ^ Test-spec

-> IO b

evalL s i = do

cl <- cmds i

(_, s') <- runIOS s (runResultT $ evaluateList cl)

return s'

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

-- * different parser

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

toE :: String -> EXPRESSION

toE = fromJust . parseResult

-- parses a single extparam range such as: "I>0, J=1"

toEP :: String -> [EXTPARAM]

toEP [] = []

toEP inp = case runParser (Lexer.separatedBy extparam pComma >-> fst) "" "" inp of

Left e -> error $ show e

Right s -> s

-- parses lists of extparam ranges such as: "I>0, J=1; ....; I=10, J=1"

toEPL :: String -> [[EXTPARAM]]

toEPL [] = []

toEPL inp = case runParser

(Lexer.separatedBy

(Lexer.separatedBy extparam pComma >-> fst) pSemi >-> fst) "" "" inp of

Left e -> error $ show e

Right s -> s

toEP1 :: String -> EPExp

toEP1 inp = case runParser extparam "" "" inp of

Left e -> error $ show e

Right s -> snd $ fromJust $ toEPExp s

toEPs :: String -> EPExps

toEPs = toEPExps . toEP

toEPLs :: String -> [EPExps]

toEPLs = map toEPExps . toEPL

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

-- * Extended Parameter tests

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

printOrdEPs :: String -> IO ()

printOrdEPs s = let ft = forestFromEPs (flip makeEPLeaf ()) $ toEPLs s

in putStrLn $ showEPForest show ft

--forestFromEPs :: (a -> EPTree b) -> [a] -> EPForest b

compareEPgen :: Show a => (String -> a) -> (a -> a -> EPCompare) -> String -> String -> IO EPCompare

compareEPgen p c a b =

let epA = p a

epB = p b

in do

putStrLn $ show epA

putStrLn $ show epB

return $ c epA epB

compareEP' = compareEPgen toEP1 compareEP

compareEPs' = compareEPgen toEPs compareEPs

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

-- * MAPLE INTERPRETER

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

-- just call the methods in MapleInterpreter: mapleInit, mapleExit, mapleDirect

-- , the CS-interface functions and evalL

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

-- * FIRST REDUCE INTERPRETER

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

-- first reduce interpreter

reds :: Int -- ^ Test-spec

-> IO ReduceInterpreter

reds i = do

r <- redsInit

sendToReduce r "on rounded; precision 30;"

evalL r i

-- use "redsExit r" to disconnect where "r <- red"

{-

-- many instances (connection/disconnection tests)

l <- mapM (const reds 1) [1..20]

mapM redsExit l

-- BA-test:

(l, r) <- redsBA 2

'l' is a list of response values for each sentence in spec Test2

'r' is the reduce connection

-}

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

-- * SECOND REDUCE INTERPRETER

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

-- run the assignments from the spec

redc :: Int -- ^ verbosity level

-> Int -- ^ Test-spec

-> IO RITrans

redc v i = do

r <- redcInit v

evalL r i

redcNames :: RITrans -> IO [String]

redcNames = runTest $ liftM toList names

redcValues :: RITrans -> IO [(String, EXPRESSION)]

redcValues = runTest values

-- run the assignments from the spec

redcCont :: Int -- ^ Test-spec

-> RITrans

-> IO RITrans

redcCont i r = do

cl <- cmds i

(res, r') <- runIOS r (runResultT $ evaluateList cl)

printDiags (PC.verbosity $ getRI r') (diags res)

return r'

--- Testing with many instances

{-

-- c-variant

lc <- time $ mapM (const $ redc 1 1) [1..20]

mapM redcExit lc

-- to communicate directly with reduce use:

let r = head lc OR r <- redc x y

let ri = getRI r

redcDirect ri "some command;"

-}

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

-- * TRANSFORMATION TESTS

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

data WithAB a b c = WithAB a b c

instance Show c => Show (WithAB a b c) where

show (WithAB _ _ c) = show c

getA (WithAB a _ _) = a

getB (WithAB _ b _) = b

getC (WithAB _ _ c) = c

-- tt = transformation tests (normally Calculationsystem monad result)

-- tte = tt with evaluation (normally gets a cs-state and has IO-result)

runTT c s vcc = do

(res, s') <- runIOS s $ runResultT $ runStateT c vcc

let (r, vcc') = fromJust $ resultToMaybe res

return $ WithAB vcc' s' r

runTTi c s = do

(res, s') <- runIOS s (runResultT $ runStateT c emptyVCCache)

let (r, vcc') = fromJust $ resultToMaybe res

return $ WithAB vcc' s' r

--s -> t -> t1 -> IO (Common.Result.Result a, s)

-- ttesd :: ( VarGen (ResultT (IOS s))

-- , VariableContainer a VarRange

-- , CalculationSystem (ResultT (IOS s))

-- , Cache (ResultT (IOS s)) a String EXPRESSION) =>

-- EXPRESSION -> s -> a -> IO (WithAB a s EXPRESSION)

ttesd e = runTT (substituteDefined e)

ttesdi e = runTTi (substituteDefined e)

-- -- substituteDefined with init

--ttesdi s e = ttesd s vc e

{-

r <- mapleInit 1

r <- redcInit 3

r' <- evalL r 3

let e = toE "sin(x) + 2*cos(y) + x^2"

w <- ttesdi e r'

let vss = getA w

w' <- ttesd e r' vss

w' <- ttesd e r' vss

mapleExit r

y <- fmap fromJust $ runTest (CSL.Interpreter.lookup "y") r'

runTest (verificationCondition y $ toE "cos(x)") r'

pretty it

r <- mapleInit 4

r <- redcInit 4

r' <- evalL r 301

let t = toE "cos(z)^2 + cos(z ^2) + sin(y) + sin(z)^2"

t' <- runTest (eval t) r'

vc <- runTest (verificationCondition t' t) r'

pretty vc

-}

{-

-- exampleRun

r <- mapleInit 4

let t = toE "factor(x^5-15*x^4+85*x^3-225*x^2+274*x-120)"

t' <- runTest (eval t) r

vc <- runTest (verificationCondition t' t) r

pretty vc

-- exampleRun2

r <- mapleInit 4

r' <- evalL r 1011

let t = toE "factor(x^5-z4*x^4+z3*x^3-z2*x^2+z1*x-z0)"

t' <- runTest (eval t) r'

vc <- runTest (verificationCondition t' t) r'

pretty vc

let l = ["z4+z3+20", "z2 + 3*z4 + 4", "3 * z3 - 30", "5 * z4 + 10", "15"]

let tl = map toE l

tl' <- mapM (\x -> runTest (eval x) r') tl

vcl <- mapM (\ (x, y) -> runTest (verificationCondition x y) r') $ zip tl' tl

mapM_ putStrLn $ map pretty vcl

-}

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

-- * Utilities

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

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

-- ** Operator extraction

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

addOp :: Map.Map String Int -> String -> Map.Map String Int

addOp mp s = Map.insertWith (+) s 1 mp

class OpExtractor a where

extr :: Map.Map String Int -> a -> Map.Map String Int

instance OpExtractor EXPRESSION where

extr m (Op op _ l _) = extr (addOp m op) l

extr m (Interval _ _ _) = addOp m "!Interval"

extr m (Int _ _) = addOp m "!Int"

extr m (Double _ _) = addOp m "!Double"

extr m (List l _) = extr (addOp m "!List") l

extr m (Var _) = addOp m "!Var"

instance OpExtractor [EXPRESSION] where

extr = foldl extr

instance OpExtractor (EXPRESSION, [CMD]) where

extr m (e,l) = extr (extr m e) l

instance OpExtractor CMD where

extr m (Ass c def) = extr m [c, def]

extr m (Cmd _ l) = extr m l

extr m (Sequence l) = extr m l

extr m (Cond l) = foldl extr m l

extr m (Repeat e l) = extr m (e,l)

instance OpExtractor [CMD] where

extr = foldl extr

extractOps :: OpExtractor a => a -> Map.Map String Int

extractOps = extr Map.empty

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

-- -- ** Assignment extraction

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

-- addOp :: Map.Map String Int -> String -> Map.Map String Int

-- addOp mp s = Map.insertWith (+) s 1 mp

-- class OpExtractor a where

-- extr :: Map.Map String Int -> a -> Map.Map String Int

-- instance OpExtractor EXPRESSION where

-- extr m (Op op _ l _) = extr (addOp m op) l

-- extr m (Interval _ _ _) = addOp m "!Interval"

-- extr m (Int _ _) = addOp m "!Int"

-- extr m (Double _ _) = addOp m "!Double"

-- extr m (List l _) = extr (addOp m "!List") l

-- extr m (Var _) = addOp m "!Var"

-- instance OpExtractor [EXPRESSION] where

-- extr = foldl extr

-- instance OpExtractor (EXPRESSION, [CMD]) where

-- extr m (e,l) = extr (extr m e) l

-- instance OpExtractor CMD where

-- extr m (Cmd _ l) = extr m l

-- extr m (Sequence l) = extr m l

-- extr m (Cond l) = foldl extr m l

-- extr m (Repeat e l) = extr m (e,l)

-- instance OpExtractor [CMD] where

-- extr = foldl extr

-- extractOps :: OpExtractor a => a -> Map.Map String Int

-- extractOps = extr Map.empty

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

-- -- * static analysis functions

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