{-# LANGUAGE TypeSynonymInstances, FlexibleContexts #-}
{- |
Module : ./CSL/InteractiveTests.hs
Description : Test environment for CSL
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)
This file is for experimenting with the Interpreter instances
and general static analysis tools
-}
module CSL.InteractiveTests where
{-
import CSL.ReduceInterpreter
import CSL.Reduce_Interface
import CSL.Transformation
import CSL.BoolBasic
import CSL.TreePO
import CSL.ExtendedParameter
import Common.IOS
import Common.Result (diags, printDiags, resultToMaybe)
import Common.ResultT
import Common.Lexer as Lexer
import Common.Parsec
import qualified Common.Lib.Rel as Rel
import Control.Monad.Trans (MonadIO (..), lift)
import Control.Monad (liftM)
-- the process communication interface
-}
import Interfaces.Process as PC
import Control.Monad.State (StateT (..))
import Control.Monad.Error (MonadError (..))
import Static.SpecLoader (getSigSensComplete, SigSens (..))
import Foreign.C.Types
import CSL.MathematicaInterpreter
import CSL.MapleInterpreter
import CSL.Interpreter
import CSL.Logic_CSL
import CSL.Analysis
import CSL.AS_BASIC_CSL
import CSL.Sign
import CSL.Parse_AS_Basic
import CSL.Verification
import Common.Utils (getEnvDef)
import Common.DocUtils
import Common.Doc
import Common.AS_Annotation
import Common.MathLink as ML
import Driver.Options
import Control.Monad.State.Class
import Control.Monad.Reader
import Data.Char
import Data.Maybe
import Data.Time.Clock
import qualified CSL.SMTComparison as CMP
import CSL.EPRelation
import System.IO
import System.Directory
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List
{-
MAIN TESTING FUNCTIONS:
test 64 assStoreAndProgSimple
test 44 assStoreAndProgElim
test 45 loadAssignmentStore
testResult 54 (depClosure ["F_G"])
(mit, _) <- testWithMaple 4 0.8 stepProg 3
(mit, _) <- testWithMaple 4 0.8 verifyProg 3
ncl <- sens 56
inDefinition (undef ncl) ncl
For engineering of the specification (to see how to fix missing constants):
sens 56 >>= (\ ncl -> inDefinition (undef ncl) ncl) >>= mapM putStrLn >>= return . length
Verification Condition Testing:
(as, prog) <- testResult 102 assStoreAndProgSimple
let gr = assDepGraphFromDescList (const $ const True) as
or short:
gr <- fmap (assDepGraphFromDescList (const $ const True) . fst)testResult 102 assStoreAndProgSimple
DEACTIVATED:
interesting i's: 44, 46
udefC i == show all undefined constants of spec i
elimDefs i == ep-eliminated AS for spec i
prettyEDefs i == pretty output for elimDefs
testElim i == raw elimination proc for spec i
prepareAS i == the assignment store after extraction from spec i and further analysis
testSMT i == returns the length of elimDefs-output and measures time, good for testing of smt comparison
-}
help :: IO ()
help = do
s <- readFile "CSL/InteractiveTests.hs"
let l = lines s
startP = ("MAIN TESTING FUNCTIONS:" /=)
endP = ("-}" /=)
putStrLn $ unlines $ takeWhile endP $ dropWhile startP l
instance Pretty Bool where
pretty = text . show
data CAS = Maple | Mathematica deriving (Show, Read, Eq)
data CASState = MapleState MITrans | MathematicaState MathState
-- ------------------------- 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
-> 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
{-
mapleLoop :: MITrans -> IO ()
mapleLoop mit = do
x <- getLine
if x == "q" then mapleExit mit >> return ()
else mapleDirect False mit x >>= putStrLn >> mapleLoop mit
-}
{- ----------------------------------------------------------------------
Gluing the Analysis and Evaluation together
---------------------------------------------------------------------- -}
test :: (Pretty a, MonadIO m) => Int -> ([Named CMD] -> m a) -> m ()
test i f = testResult i f >>= liftIO . print . pretty
testResult :: (Pretty a, MonadIO m) => Int -> ([Named CMD] -> m a) -> m a
testResult i f = liftIO (sens i) >>= f
-- | Returns sorted assignment store and program after EP elimination
assStoreAndProgElim :: [Named CMD] -> IO ([(ConstantName, AssDefinition)], [Named CMD])
assStoreAndProgElim ncl = do
let (asss, prog) = splitAS ncl
gm = fmap analyzeGuarded asss
sgl = dependencySortAS gm
, CMP.loghandle = Just stdout
-- , CMP.loghandle = Nothing
}
-- ve = emptyVarEnv $ Just stdout
el <- execSMTTester' ve $ epElimination sgl
return (getElimAS el, prog)
-- | 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)
loadAssignmentStore :: (MonadState (ASState st) m, AssignmentStore m, MonadIO m) => Bool -> [Named CMD]
-> m ([(ConstantName, AssDefinition)], [Named CMD])
loadAssignmentStore b ncl = do
let f = if b then assStoreAndProgElim else assStoreAndProgSimple
res@(asss, _) <- liftIO $ f ncl
loadAS asss
return res
stepProg :: (MessagePrinter m, MonadIO m, MonadError ASError m) =>
[Named CMD] -> m (Maybe ASError)
stepProg ncl = stepwiseSafe interactiveStepper $ Sequence $ map sentence ncl
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 -> 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
{-
testWithMapleGen :: Int -> DTime -> ([Named CMD] -> MapleIO a) -> String -> String
-> IO (MITrans, a)
testWithMapleGen verb to 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 = loadAS as >> modify (\ mit -> mit {vericondOut = Just vchdl}) >> f x
-- start maple and run g
res <- runWithMaple gr verb to
[ "EnCLFunctions"
-- , "intpakX" -- Problems with the min,max functions, they are remapped by this package!
]
$ g prog
hClose vchdl
return res
-}
testWithMaple :: Int -> DTime -> ([Named CMD] -> MapleIO a) -> Int -> IO (MITrans, a)
testWithMaple verb to f = uncurry (testWithMapleGen verb to (return ()) f) . libFP
getMathState :: Maybe CASState -> MathState
getMathState (Just (MathematicaState mst)) = mst
getMathState _ = error "getMathState: no MathState"
getMapleState :: Maybe CASState -> MITrans
getMapleState (Just (MapleState mst)) = mst
getMapleState _ = error "getMapleState: no Maple state"
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
---------------------------------------------------------------------- -}
-- | Returns all constants where the given constants depend on
depClosure :: [String] -> [Named CMD] -> IO [[String]]
depClosure l ncl = do
let (asss, _) = splitAS ncl
gm = fmap analyzeGuarded asss
dr = getDependencyRelation gm
return $ relLayer dr l
-- | mark final
markFinal :: [String] -> [Named CMD] -> IO [String]
markFinal l ncl = do
let (asss, _) = splitAS ncl
gm = fmap analyzeGuarded asss
dr = getDependencyRelation gm
f x = case Map.lookup x dr of
Just s -> if Set.null s then x ++ " *" else x
_ -> x ++ " *"
return $ map f l
-- | definedIn
definedIn :: [String] -> [Named CMD] -> IO [String]
definedIn l ncl = return $ map g l where
g s = intercalate ", " (mapMaybe (f s) ncl) ++ ":" ++ s
f s nc = case sentence nc of
Ass (Op oi _ _ _) _ ->
if simpleName oi == s then Just $ senAttr nc else Nothing
_ -> Nothing
inDefinition :: [String] -> [Named CMD] -> IO [String]
inDefinition l ncl =
let (asss, _) = splitAS ncl
gm = fmap analyzeGuarded asss
dr = getDependencyRelation gm
allDefs = allDefinitions ncl
br = Map.filterWithKey (\ k _ -> elem k l) $ getBackRef dr
f m = map (g m)
g m x = Map.findWithDefault "" x m
h = f allDefs
f' (x, y) = x ++ ": " ++ intercalate ", " y
in return $ map f' $ Map.toList $ fmap h br
allDefinitions :: [Named CMD] -> Map.Map String String
allDefinitions ncl = Map.fromList $ mapMaybe f ncl where
f nc = case sentence nc of
Ass (Op oi _ _ _) _ -> Just (simpleName oi, senAttr nc)
_ -> Nothing
undef :: [Named CMD] -> [String]
undef ncl = Set.toList $ undefinedConstants $ fst $ splitAS ncl
-- printSetMap Common.Doc.empty Common.Doc.empty dr
relLayer :: Ord a => Rel2 a -> [a] -> [[a]]
relLayer _ [] = []
relLayer r l = l : relLayer r succs where
{- emptyVarEnv
execSMTComparer :: VarEnv -> SmtComparer a -> IO a
splitAS :: [Named CMD] -> (GuardedMap [EXTPARAM], [Named CMD])
getElimAS :: [(String, Guarded EPRange)] -> [(ConstantName, AssDefinition)]
dependencySortAS :: GuardedMap EPRange -> [(String, Guarded EPRange)]
epElimination :: CompareIO m => [(String, Guarded EPRange)] -> m [(String, Guarded EPRange)] -}
casConst :: ASState a -> String -> String
casConst mit s =
fromMaybe "" $ rolookup (getBMap mit) $ SimpleConstant s
enclConst :: ASState a -> String -> OPID
enclConst mit s =
fromMaybe (error $ "enclConst: no mapping for " ++ s) $ revlookup (getBMap mit) s
{- ----------------------------------------------------------------------
general test functions
---------------------------------------------------------------------- -}
-- Testing of keyboard-input
charInfo :: IO ()
charInfo = do
c <- getChar
{- when (c /= 'e') $ putStrLn "" >> putStrLn (c:[]) >> putStrLn (show $ ord c) >> charInfo
Escape-button = 27 -}
when (ord c /= 27) $ putStrLn "" >> putStrLn [c] >> print $ ord c >> charInfo
testspecs :: [(Int, (String, String))]
testspecs =
[ (44, ("EnCL/EN1591.het", "EN1591"))
, (45, ("EnCL/flange.het", "Flange"))
, (46, ("EnCL/flange.het", "FlangeComplete"))
, (54, ("EnCL/EN1591S.het", "EN1591"))
, (55, ("EnCL/flangeS.het", "Flange"))
, (56, ("EnCL/flangeS.het", "FlangeComplete"))
, (65, ("EnCL/flangeDefault.het", "FlangeDefault"))
, (66, ("EnCL/flangeExported.het", "FlangeComplete"))
]
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
siggy :: Int -> IO (SigSens Sign CMD)
siggy = uncurry sigsensGen . libFP
libFP :: Int -> (String, String)
libFP i = fromMaybe (if i >= 0 then ("EnCL/Tests.het", "Test" ++ show i)
else ("EnCL/ExtParamExamples.het", 'E' : show (- i)))
$ Prelude.lookup i testspecs
sigsens :: Int -> IO (Sign, [Named CMD])
sigsens i = do
res <- siggy i
return ( sigsensSignature res, sigsensNamedSentences res )
sig :: Int -> IO Sign
sig = fmap fst . sigsens
-- Check if the order is broken or not!
sens :: Int -> IO [Named CMD]
sens = fmap snd . sigsens
cmds :: Int -> IO [CMD]
cmds = fmap (map sentence) . sens
-- time measurement, pendant of the time shell command
time :: MonadIO m => m a -> m a
time p = do
t <- liftIO getCurrentTime
res <- p
t' <- liftIO getCurrentTime
liftIO $ print $ diffUTCTime t' t
return res
toE :: String -> EXPRESSION
toE = fromJust . parseExpression operatorInfoMap
toCmd :: String -> CMD
toCmd = fromJust . parseCommand
{- ----------------------------------------------------------------------
Smt testing instances
---------------------------------------------------------------------- -}
data TestEnv = TestEnv { counter :: Int
, varenv :: CMP.VarEnv
, loghdl :: Handle }
logf :: FilePath
logf = "/tmp/CSL.log"
teFromVE :: CMP.VarEnv -> IO TestEnv
teFromVE ve = do
hdl <- openFile logf WriteMode
let ve' = ve { CMP.loghandle = Just hdl }
return TestEnv { counter = 0, varenv = ve', loghdl = hdl }
type SmtTester = StateT TestEnv IO
execSMTTester :: CMP.VarEnv -> SmtTester a -> IO (a, Int)
execSMTTester ve smt = do
(x, s) <- teFromVE ve >>= runStateT smt
hClose $ loghdl s
return (x, counter s)
execSMTTester' :: CMP.VarEnv -> SmtTester a -> IO a
execSMTTester' ve smt = do
(x, i) <- execSMTTester ve smt
putStrLn $ "SMT-Checks: " ++ show i
return x
instance CompareIO SmtTester where
logMessage x = do
hdl <- gets loghdl
liftIO $ hPutStrLn hdl x
rangeFullCmp r1 r2 = do
env <- get
let f x = x {counter = counter x + 1}
ve = varenv env
vm = CMP.varmap ve
hdl = loghdl env
modify f
lift $ writeRangesToLog hdl r1 r2
liftIO $ hPutStrLn hdl ""
res <- lift $ CMP.smtCompare ve (boolRange vm r1) $ boolRange vm r2
lift $ writeRangesToLog hdl r1 r2 >> hPutStrLn hdl ('=' : show res)
return res
writeRangesToLog :: Handle -> EPRange -> EPRange -> IO ()
writeRangesToLog hdl r1 r2 = do
let [d1, d2] = map diagnoseEPRange [r1, r2]
hPutStr hdl $ show $ text "Cmp" <> parens (d1 <> comma <+> d2)
{- ----------------------------------------------------------------------
Smt testing instances
---------------------------------------------------------------------- -}
{-
show guarded assignments:
:m +CSL.Analysis
sl <- sens 3
fst $ splitAS s
-}
{-
-- ----------------------------------------------------------------------
-- * calculator test functions
-- ----------------------------------------------------------------------
runTest :: ResultT (IOS b) a -> b -> IO a
runTest cmd r = fmap fromJust $ runTestM cmd r
runTestM :: 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 :: AssignmentStore (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
-- ----------------------------------------------------------------------
-- parses a single extparam range such as: "I>0, F=1"
toEP :: String -> [EXTPARAM]
toEP [] = []
toEP s = case runParser (Lexer.separatedBy extparam pComma >-> fst) "" "" s of
Left e -> error $ show e
Right s' -> s'
-- parses lists of extparam ranges such as: "I>0, F=1; ....; I=10, F=1"
toEPL :: String -> [[EXTPARAM]]
toEPL [] = []
toEPL s = case runParser
(Lexer.separatedBy extparam pComma >-> fst) pSemi >-> fst) "" "" s of
Left e -> error $ show e
Right s' -> s'
toEP1 :: String -> EPExp
toEP1 s = case runParser extparam "" "" s 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
-- ----------------------------------------------------------------------
{-
smtEQScript vMap (boolRange vMap $ epList!!0) (boolRange vMap $ epList!!1)
test for smt-export
let m = varMapFromList ["I", "J", "F"]
let be = boolExps m $ toEPs "I=0"
smtBoolExp be
compare-check for yices
let l2 = [(x,y) | x <- epList, y <- epList]
let l3 = map (\ (x, y) -> smtCompareUnsafe vEnv (boolRange vMap x) (boolRange vMap y)) l2
putStrLn $ unlines $ map show $ zip l3 l2
:m +CSL.Analysis
sl <- sens (-82)
let grdm = fst $ splitAS sl
let sgm = dependencySortAS grdm
let grdd = snd $ Map.elemAt 0 grdm
let sgm = dependencySortAS grdm
getDependencyRelation grdm
:m +CSL.Analysis
gm <- fmap grddMap $ sens (-3)
let (_, xg) = Map.elemAt 1 gm
let (_, yg) = Map.elemAt 2 gm
let f grd = (grd, toEPExps $ range grd)
let frst = forestFromEPs f $ guards xg
putStrLn $ showEPForest show frst
foldForest (\ x y z -> x ++ [(y, length z)]) [] frst
-}
-- undefinedConstants :: GuardedMap a -> Set.Set String
-- getElimAS :: [(String, Guarded EPRange)] -> [(ConstantName, AssDefinition)]
-- Use this Constant printer for test output
instance ConstantPrinter (Reader (ConstantName -> Doc)) where
printConstant c = asks ($ c)
ppConst :: ConstantName -> Doc
ppConst (SimpleConstant s) = text s
ppConst (ElimConstant s i) = text s <> text (show $ 1+i)
prettyEXP e = runReader (printExpression e) ppConst
testSMT = time . fmap length . elimDefs
udefC = liftM (undefinedConstants . fst . splitAS) . sens
elimDefs = liftM getElimAS . testElim
elimConsts = liftM elimConstants . testElim
prettyEConsts i = elimConsts i >>= mapM_ f where
f (_, m) = mapM_ g $ Map.toList m
g (c, er) =
putStrLn $ (show $ ppConst c) ++ " :: " ++ show (prettyEPRange er)
prettyEDefs i = liftM (unlines . map f) (elimDefs i) >>= putStrLn where
f (c, assdef) = concat [ show $ ppConst c, g $ getArguments assdef, " := "
, show $ prettyEXP $ getDefiniens assdef]
g [] = ""
g l = show $ parens $ sepByCommas $ map text l
-- irreflexive triangle of a list l: for i < j . (l_i, l_j)
irrTriang :: [a] -> [(a,a)]
irrTriang [] = []
irrTriang (x:l) = map ((,) x) l ++ irrTriang l
-- * Model Generation
frmAround "" = ""
frmAround s = let l = lines s
hd = "--" ++ map (const '-') (head l)
in unlines $ hd : map (('|':) . (++"|")) l ++ [hd]
modelRg1 :: Map.Map String (Int, Int)
modelRg1 = Map.fromList [("I", (-5, 5))]
modelRg2 :: Map.Map String (Int, Int)
modelRg2 = Map.fromList [("I", (-5, 5)), ("F", (-5, 5))]
modelRg3 :: Map.Map String (Int, Int)
modelRg3 = Map.fromList [("I", (-5, 5)), ("J", (-5, 5)), ("F", (-5, 5))]
printModel :: Map.Map String (Int, Int) -> EPRange -> String
printModel x y = modelToString boolModelChar $ modelOf x y
pM1::EPRange -> IO ()
pM2::EPRange -> IO ()
pM1s::[EPRange] -> IO ()
pM2s::[EPRange] -> IO ()
pM2 = putStr . frmAround . printModel modelRg2
pM1 = putStr . frmAround . printModel modelRg1
pM1s = mapM_ pM1
pM2s = mapM_ pM2
toEPR :: String -> EPRange
toEPR = Atom . toEPs
-- Test for partitioning taken from E82 in CSL/ExtParamExamples.het
el11 :: [EPRange]
el11 = let x1 = toEPR "I>=0" in [x1, Complement x1]
el12 :: [EPRange]
el12 = let l = map toEPR ["I=1", "I>1"] in Complement (Union l) : l
el13 :: [EPRange]
el13 = let x1 = toEPR "I>0" in [x1, Complement x1]
el21 :: [EPRange]
el21 = let x1 = toEPR "I>=0" in [x1, Complement x1]
el22 :: [EPRange]
el22 = let l = map toEPR ["I>=0, F>=0", "I<4, F<=4"]
inter = Intersection l
uni = Union l
in uni : inter : Intersection [uni, Complement inter] : l
el23 :: [EPRange]
el23 = let x1 = toEPR "I>0" in [x1, Complement x1]
-- * Partition tests
checkForPartition :: [EPRange] -> IO Bool
checkForPartition l = execSMTTester' vEnv1 $ f g l where
f a [] = return True
f a (x:l') = do
res <- mapM (a x) l'
res' <- f a l'
return $ and $ res' : res
g x y = fmap (Incomparable Disjoint ==) $ rangeCmp x y
part1 :: Partition Int
part1 = AllPartition 10
part2 :: Partition Int
part2 = Partition $ zip el11 [33 ..]
part3 :: Partition Int
part3 = Partition $ zip el12 [1 ..]
part4 :: Partition Int
part4 = Partition $ zip el13 [91 ..]
parts = [part1, part2, part3, part4]
refinePart a b = execSMTTester' vEnv1 $ refinePartition a b
allRefin = do
m1 <- mapM (uncurry refinePart) $ irrTriang parts
m2 <- mapM (uncurry refinePart) $ irrTriang m1
return (m1, m2)
allRShow = do
(a, b) <- allRefin
showPart1s a
putStrLn "=============================================="
showPart1s b
allRCmp = do
(a, b) <- allRefin
cmpRg1s a
putStrLn "=============================================="
cmpRg1s b
showPart1s :: Show a => [Partition a] -> IO ()
showPart1s = let f x = showPart1 x >> putStrLn "==="
in mapM_ f
showPartX :: Show a => (EPRange -> IO ()) -> Partition a -> IO ()
showPart1 :: Show a => Partition a -> IO ()
showPart2 :: Show a => Partition a -> IO ()
showPartX _ (AllPartition x) = do
putStrLn $ show x
putStrLn "All\n\n"
showPartX fM (Partition l) =
let f (re, x) = do
putStrLn $ show x
fM re
putStrLn "\n"
in mapM_ f l
showPart1 = showPartX pM1
showPart2 = showPartX pM2
class HasRanges a where
getRanges :: a -> [EPRange]
instance HasRanges (Partition a) where
getRanges (AllPartition x) = []
getRanges (Partition l) = map fst l
instance HasRanges a => HasRanges [a] where
getRanges = concatMap getRanges
instance HasRanges (Guarded EPRange) where
getRanges = map range . guards
instance HasRanges (String, Guarded EPRange) where
getRanges = map range . guards . snd
cmpRg1 :: HasRanges a => a -> IO ()
cmpRg1 = putStrLn . concat . map (printModel modelRg1) . getRanges
cmpRg1s :: HasRanges a => [a] -> IO ()
cmpRg1s = let f = putStrLn . concat . map (printModel modelRg1) . getRanges
g x = f x >> putStrLn "==="
in mapM_ g
-- * elim proc testing
{-
:m +CSL.Analysis
sl <- sens (-82)
let grdm = fst $ splitAS sl
let sgm = dependencySortAS grdm
-}
-- elimTestInit :: Int -> [(String, Guarded EPRange)] -> IO [Guard EPRange]
elimTestInit i gl = do
let grd = (guards $ snd $ head gl)!!i
execSMTTester' vEnv $ eliminateGuard Map.empty grd
pgX :: (EPRange -> IO a) -> Guard EPRange -> IO ()
pgX fM grd = do
fM $ range grd
putStr "Def: "
putStrLn $ show $ pretty $ definition grd
putStrLn ""
pg1 :: Guard EPRange -> IO ()
pg1 = pgX pM1
pg2 :: Guard EPRange -> IO ()
pg2 = pgX pM2
pgrddX :: (EPRange -> IO a) -> Guarded EPRange -> IO ()
pgrddX fM grdd = mapM_ (pgX fM) $ guards grdd
pgrdd2 :: Guarded EPRange -> IO ()
pgrdd2 = pgrddX pM2
printASX :: (EPRange -> IO a) -> [(String, Guarded EPRange)] -> IO ()
printASX fM l = mapM_ f l where
f (s, grdd) = do
putStr s
putStrLn ":"
pgrddX fM grdd
putStrLn ""
printAS1 :: [(String, Guarded EPRange)] -> IO ()
printAS1 = printASX pM1
printAS2 :: [(String, Guarded EPRange)] -> IO ()
printAS2 = printASX pM2
testElim :: Int -> IO [(String, Guarded EPRange)]
testElim i = prepareAS i >>= elimEPs
prepareAS :: Int -> IO [(String, Guarded EPRange)]
prepareAS = liftM (dependencySortAS . fmap analyzeGuarded . fst . splitAS) . sens
prepareProg :: Int -> IO [Named CMD]
prepareProg = liftM (snd . splitAS) . sens
progAssignments :: Int -> IO [(EXPRESSION, EXPRESSION)]
progAssignments = liftM subAss . prepareProg
-- get the first guarded-entry from the AS
-- grdd <- fmap (snd . head) $ getAS (-821)
getAS :: Int -> IO [(String, Guarded [EXTPARAM])]
getAS = liftM (Map.toList . fst . splitAS) . sens
getASana :: Int -> IO [(String, Guarded EPRange)]
getASana = liftM (Map.toList . fmap analyzeGuarded . fst . splitAS) . sens
elimEPs :: [(String, Guarded EPRange)] -> IO [(String, Guarded EPRange)]
elimEPs l = do
-- execSMTComparer vEnv $ epElimination l
execSMTTester' vEnv $ epElimination l
grddMap :: [Named CMD] -> GuardedMap [EXTPARAM]
grddMap = foldr (uncurry $ addAssignment "?") Map.empty . assignments
assignments :: [Named CMD] -> [(EXPRESSION, EXPRESSION)]
assignments = assignments' . map sentence
assignments' :: [CMD] -> [(EXPRESSION, EXPRESSION)]
assignments' = mapMaybe getAss
subAss :: [Named CMD] -> [(EXPRESSION, EXPRESSION)]
subAss = concatMap subAssignments . map sentence
getAss (Ass c def) = Just (c,def)
getAss _ = Nothing
varEnvFromList :: [String] -> VarEnv
varEnvFromList l = error ""
-- | Generates from a list of Extended Parameter names an id-mapping
varMapFromList :: [String] -> VarMap
varMapFromList l = Map.fromList $ zip l $ [1 .. length l]
-- | Generates from a list of Extended Parameter names an id-mapping
varMapFromSet :: Set.Set String -> VarMap
varMapFromSet = varMapFromList . Set.toList
epList :: [EPRange]
epList =
let l = map (Atom . toEPs)
["", "I=1,F=0", "I=0,F=0", "I=0", "I=1", "F=0", "I>0", "I>2", "I>0,F>2"]
in Intersection l : Union l : l
epDomain :: [(String, EPExps)]
epDomain = zip ["I", "F"] $ map toEPs ["I>= -1", "F>=0"]
vMap :: Map.Map String Int
vMap = varMapFromSet $ namesInList epList
-- vTypes = Map.map (const Nothing) vMap
vTypes = Map.fromList $ map (\ (x,y) -> (x, boolExps vMap y)) epDomain
vEnvX = VarEnv { varmap = vMap, vartypes = Map.empty, loghandle = Nothing }
vEnv1 = VarEnv { varmap = Map.fromList [("I", 1)], vartypes = Map.empty, loghandle = Nothing }
--vEnv = VarEnv { varmap = vMap, vartypes = vTypes, loghandle = Nothing }
vEnv = vEnvX
printOrdEPs :: String -> IO ()
printOrdEPs s = let ft = forestFromEPs ((,) ()) $ toEPLs s
in putStrLn $ showEPForest show ft
--forestFromEPs :: (a -> EPTree b) -> [a] -> EPForest b
compareEPgen :: Show a => (String -> a) -> (a -> a -> SetOrdering) -> String -> String -> IO SetOrdering
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 [ConstantName]
redcNames = runTest $ liftM toList names
redcValues :: RITrans -> IO [(ConstantName, 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
-- , AssignmentStore (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
-- show value for const x
runTest (CSL.Interpreter.lookup "x") r' >>= return . pretty
runTest (CSL.Interpreter.eval $ toE "cos(x-x)") r' >>= return . pretty
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 mp s = Map.insertWith (+) s 1 mp
class OpExtractor a where
instance OpExtractor EXPRESSION where
extr m (Op op _ l _) = extr (addOp m $ show 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 mp s = Map.insertWith (+) s 1 mp
-- class OpExtractor a where
-- 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
-- -- ----------------------------------------------------------------------
-- arithmetic operators
opsArith = [ OP_mult, OP_div, OP_plus, OP_minus, OP_neg, OP_pow ]
-- roots, trigonometric and other operators
opsReal = [ OP_fthrt, OP_sqrt, OP_abs, OP_max, OP_min, OP_sign
, OP_cos, OP_sin, OP_tan, OP_Pi ]
-- special CAS operators
opsCas = [ OP_maximize, OP_factor
, OP_divide, OP_factorize, OP_int, OP_rlqe, OP_simplify, OP_solve ]
-- comparison predicates
opsCmp = [ OP_neq, OP_lt, OP_leq, OP_eq, OP_gt, OP_geq, OP_convergence ]
-- boolean constants and connectives
opsBool = [ OP_false, OP_true, OP_not, OP_and, OP_or, OP_impl ]
-- quantifiers
opsQuant = [ OP_ex, OP_all ]
-}
{- ----------------------------------------------------------------------
MathLink stuff
---------------------------------------------------------------------- -}
readAndPrintOutput :: ML ()
readAndPrintOutput = do
exptype <- mlGetNext
let pr | exptype == dfMLTKSYM = readAndPrintML "Symbol: " mlGetSymbol
| exptype == dfMLTKSTR = readAndPrintML "String: " mlGetString
| exptype == dfMLTKINT = readAndPrintML "Int: " mlGetInteger
| exptype == dfMLTKREAL = readAndPrintML "Real: " mlGetReal
| exptype == dfMLTKFUNC =
do
len <- mlGetArgCount
if len == 0 then mlProcError
else do
let f i = readAndPrintOutput
>> when (i < len) $ userMessage ", "
readAndPrintOutput
userMessage "["
forM_ [1 .. len] f
userMessage "]"
| exptype == dfMLTKERROR = userMessageLn "readAndPrintOutput-error" >> mlProcError
| otherwise = userMessageLn ("readAndPrintOutput-error" ++ show exptype)
>> mlProcError
pr
userMessage :: String -> ML ()
userMessage s = ML.verbMsgMLLn 2 s >> liftIO (putStr s)
userMessageLn :: String -> ML ()
userMessageLn s = ML.verbMsgMLLn 2 s >> liftIO (putStrLn s)
class MLShow a where
mlshow :: a -> String
instance MLShow String where
mlshow s = s
instance MLShow CDouble where
mlshow = show
instance MLShow CInt where
mlshow = show
readAndPrintML :: MLShow a => String -> ML a -> ML ()
readAndPrintML _ pr = pr >>= userMessage . mlshow
-- * Test functionality
sendPlus :: CInt -> CInt -> CInt -> ML ()
sendPlus i j k = do
mlPutFunction "EvaluatePacket" 1
mlPutFunction "Plus" 3
mlPutInteger i
mlPutInteger j
mlPutInteger k
mlEndPacket
userMessageLn "Sent"
sendFormula :: CInt -> CInt -> CInt -> ML ()
sendFormula i j k = do
mlPutFunction "EvaluatePacket" 1
mlPutFunction "Plus" 2
mlPutFunction "Times" 2
mlPutInteger i
mlPutInteger j
mlPutFunction "Times" 3
mlPutInteger k
mlPutInteger k
mlPutSymbol "xsymb"
mlEndPacket
userMessageLn "Sent"
{- ----------------------------------------------------------------------
MathLink Tests
---------------------------------------------------------------------- -}
mathP3 :: MathState -> String -> IO ()
mathP3 mst s = mlMathEnv mst $ mlP3 s 0
mlMathEnv :: MathState -> ML a -> IO a
mlMathEnv mst prog = liftM snd $ withMathematica mst $ liftML prog
mlTestEnv :: Pretty a => String -> ML a -> IO a
mlTestEnv s act = do
let mN = if null s then Nothing else Just s
eRes <- runLink (Just "/tmp/mi.txt") 2 mN act
case eRes of
Left eid -> putStrLn ("Error " ++ show eid) >> error "ml-test"
Right res -> putStrLn ("OK: " ++ show (pretty res)) >> return res
mlP1 :: CInt
-> CInt
-> CInt
-> ML ()
mlP1 i j k = forM_ [1 .. k] $ sendFormula i j >=>
const (waitForAnswer >> readAndPrintOutput >> userMessageLn "")
mlTest :: [String] -> IO ()
mlTest argv = do
let (k, i, j) = (read $ head argv, read $ argv !! 1, read $ argv !! 2)
s = if length argv > 3 then argv !! 3 else ""
mlTestEnv s $ mlP1 i j k
mlP2 :: Int
-> EXPRESSION
-> ML [EXPRESSION]
mlP2 k e = forM [1 .. (k :: Int)] $ const $ sendEvalPacket (sendExpression True e)
>> waitForAnswer >> receiveExpression
mlTest2 :: [String] -> IO [EXPRESSION]
mlTest2 argv = do
let k = read $ head argv
e = toE $ argv !! 1
s = if length argv > 2 then argv !! 2 else ""
mlTestEnv s $ mlP2 k e
-- a good interactive stepper through the mathlink interface
mlP3 :: String -> Int -> ML ()
mlP3 es k = do
let pr j = liftIO $ putStrLn $ "Entering level " ++ show j
prog i j s | null s = pr j >> prog2 j
| i == 1 = pr j >> sendTextPacket s >> prog2 j
| i == 2 = pr j >> sendTextResultPacket s >> prog2 j
| i == 10 = pr j >> sendTextPacket' s >> prog2 j
| i == 3 = pr j >> sendTextPacket'' s >> prog2 j
| i == 4 = pr j >> sendTextPacket3 s >> prog2 j
| i == 0 = pr j >> sendEvalPacket (sendExpression True $ toE s) >> prog2 j
| otherwise = pr j >> sendTextPacket4 s >> prog2 j
gt g
| g == dfMLTKSYM = "Symbol"
| g == dfMLTKSTR = "String"
| g == dfMLTKINT = "Int"
| g == dfMLTKREAL = "Real"
| otherwise = ""
prog2 j = do
let exitP2 = return $ -1
c <- liftIO getChar
i <- case c of
'x' -> mlNextPacket
'n' -> mlNewPacket
'G' -> mlGetNext
'r' -> mlReady
'g' ->
do
g <- mlGetNext
liftIO $ putStrLn $ "getnext -> " ++ gt g
return g
'y' -> liftIO (putStr " -> ") >> readAndPrintML "Symbol: " mlGetSymbol >> liftIO (putStrLn "") >> return 0
's' -> liftIO (putStr " -> ") >> readAndPrintML "String: " mlGetString >> liftIO (putStrLn "") >> return 0
'i' -> liftIO (putStr " -> ") >> readAndPrintML "Int: " mlGetInteger >> liftIO (putStrLn "") >> return 0
'd' -> liftIO (putStr " -> ") >> readAndPrintML "Real: " mlGetReal >> liftIO (putStrLn "") >> return 0
'0' -> liftIO (putStr ">" >> getLine) >>= prog 0 (j + 1) >> exitP2
'1' -> liftIO (putStr ">" >> getLine) >>= prog 1 (j + 1) >> exitP2
'2' -> liftIO (putStr ">" >> getLine) >>= prog 2 (j + 1) >> exitP2
'3' -> liftIO (putStr ">" >> getLine) >>= prog 3 (j + 1) >> exitP2
'4' -> liftIO (putStr ">" >> getLine) >>= prog 4 (j + 1) >> exitP2
'5' -> liftIO (putStr ">" >> getLine) >>= prog 5 (j + 1) >> exitP2
_ -> exitP2
when (i >= 0) $ do
liftIO $ putStrLn $ c : (": " ++ show i)
prog2 j
-- mlTestEnv cn $ prog k (0::Int) es
prog k (0 :: Int) es
mlTest3 :: String -> String -> Int -> IO ()
mlTest3 cn es k = mlTestEnv cn $ mlP3 es k
mlTest4 :: String -> [String] -> IO ()
mlTest4 cn = mlTest5 cn . map Right
mlTest5 :: String -> [Either String String] -> IO ()
mlTest5 cn el = do
let prog [] = return ()
prog (e : l) = do
case e of
Right s ->
sendEvalPacket (sendExpression True $ toE s)
Left s ->
sendEvalPacket (sendExpressionString s)
waitForAnswer
e' <- receiveExpression
liftIO $ putStrLn $ show e ++ ": " ++ show (pretty e')
prog l
mlTestEnv cn $ prog el