InteractiveTests.hs revision 9b67773d9991de68409461a7607a65a0de9a80bd
fa9e4066f08beec538e775443c5be79dd423fcabahrens{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
fa9e4066f08beec538e775443c5be79dd423fcabahrensModule : $Header$
fa9e4066f08beec538e775443c5be79dd423fcabahrensDescription : Test environment for CSL
ea8dc4b6d2251b437950c0056bc626b311c73c27eschrockCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010
ea8dc4b6d2251b437950c0056bc626b311c73c27eschrockLicense : GPLv2 or higher, see LICENSE.txt
fa9e4066f08beec538e775443c5be79dd423fcabahrensMaintainer : Ewaryst.Schulz@dfki.de
fa9e4066f08beec538e775443c5be79dd423fcabahrensStability : experimental
fa9e4066f08beec538e775443c5be79dd423fcabahrensPortability : non-portable (uses type-expression in type contexts)
fa9e4066f08beec538e775443c5be79dd423fcabahrensThis file is for experimenting with the Interpreter instances
fa9e4066f08beec538e775443c5be79dd423fcabahrensand general static analysis tools
fa9e4066f08beec538e775443c5be79dd423fcabahrensimport CSL.TreePO (EPCompare)
75c7619736838143dd41b3c5c9d7adec4683488fpetehimport CSL.EPRelation -- (compareEP, EPExp, toEPExp, compareEPs, EPExps, toEPExps, forestFromEPs, makeEPLeaf, showEPForest)
fa9e4066f08beec538e775443c5be79dd423fcabahrensimport CSL.Parse_AS_Basic (parseResult, extparam, pComma, pSemi)
fa9e4066f08beec538e775443c5be79dd423fcabahrensimport Common.Utils (getEnvDef)
fa9e4066f08beec538e775443c5be79dd423fcabahrensimport Common.Result (diags, printDiags, resultToMaybe)
de8267e0f723ed2c38ea9def92d465f69a300f56timhimport Common.Lexer as Lexer
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- the process communication interface
fa9e4066f08beec538e775443c5be79dd423fcabahrensimport qualified Interfaces.Process as PC
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- README: In order to work correctly link the Test.hs in the Hets-root dir to Main.hs (ln -s Test.hs Main.hs)
fa9e4066f08beec538e775443c5be79dd423fcabahrensimport Main (getSigSens)
fa9e4066f08beec538e775443c5be79dd423fcabahrensimport Control.Monad.State (StateT(..))
fa9e4066f08beec538e775443c5be79dd423fcabahrensimport Control.Monad.Trans (MonadIO (..))
fa9e4066f08beec538e775443c5be79dd423fcabahrensimport Control.Monad (liftM)
fa9e4066f08beec538e775443c5be79dd423fcabahrensimport Data.Maybe (fromJust, fromMaybe)
104e2ed78d9ef0a0f89f320108b8ca29ca3850d5perrinimport qualified Data.Map as Map
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- ----------------------------------------------------------------------
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw-- * general test functions
55434c770c89aa1b84474f2559a106803511aba0ek-- ----------------------------------------------------------------------
55434c770c89aa1b84474f2559a106803511aba0ektestspecs =
55434c770c89aa1b84474f2559a106803511aba0ek [ (44, ("/CSL/EN1591.het", "EN1591"))
55434c770c89aa1b84474f2559a106803511aba0ekl1 :: Int -> IO (Sign, [Named CMD])
de8267e0f723ed2c38ea9def92d465f69a300f56timh let (lb, sp) = fromMaybe (if i > 0 then ("/CSL/Tests.het", "Test" ++ show i)
de8267e0f723ed2c38ea9def92d465f69a300f56timh else ("/CSL/ExtParamExamples.het", "E" ++ show (- i)))
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee $ Prelude.lookup i testspecs
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee hlib <- getEnvDef "HETS_LIB" $ error "Missing HETS_LIB environment variable"
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee getSigSens CSL (hlib ++ lb) sp
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeesig :: Int -> IO Sign
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeesig = fmap fst . l1
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- Check if the order is broken or not!
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeesens :: Int -> IO [Named CMD]
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeesens = fmap snd . l1
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeecmds :: Int -> IO [CMD]
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeecmds = fmap (map sentence) . sens
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- time measurement, pendant of the time shell command
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeetime :: MonadIO m => m a -> m a
55434c770c89aa1b84474f2559a106803511aba0ek t <- liftIO getCurrentTime
55434c770c89aa1b84474f2559a106803511aba0ek t' <- liftIO getCurrentTime
55434c770c89aa1b84474f2559a106803511aba0ek liftIO $ putStrLn $ show $ diffUTCTime t' t
55434c770c89aa1b84474f2559a106803511aba0ek return res
4e9583b23260dab68308b306795694143381ab0fTom Ericksonshow guarded assignments:
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeefst $ splitAS s
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- ----------------------------------------------------------------------
874395d5f8cae2b9cd2d1fcbfcfe963a0c23966dmaybee-- * calculator test functions
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- ----------------------------------------------------------------------
874395d5f8cae2b9cd2d1fcbfcfe963a0c23966dmaybeerunTest :: ResultT (IOS b) a -> b -> IO a
874395d5f8cae2b9cd2d1fcbfcfe963a0c23966dmaybeerunTest cmd r = fmap fromJust $ runTestM cmd r
874395d5f8cae2b9cd2d1fcbfcfe963a0c23966dmaybeerunTestM :: ResultT (IOS b) a -> b -> IO (Maybe a)
fa9e4066f08beec538e775443c5be79dd423fcabahrensrunTestM cmd r = fmap (resultToMaybe . fst) $ runIOS r $ runResultT cmd
fa9e4066f08beec538e775443c5be79dd423fcabahrensrunTest_ :: ResultT (IOS b) a -> b -> IO (a, b)
fa9e4066f08beec538e775443c5be79dd423fcabahrensrunTest_ cmd r = do
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee (res, r') <- runIOS r $ runResultT cmd
fa9e4066f08beec538e775443c5be79dd423fcabahrens return (fromJust $ resultToMaybe res, r')
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeevalL :: CalculationSystem (ResultT (IOS b)) => b
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee -> Int -- ^ Test-spec
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeevalL s i = do
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee cl <- cmds i
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee (_, s') <- runIOS s (runResultT $ evaluateList cl)
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- ----------------------------------------------------------------------
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- * different parser
104e2ed78d9ef0a0f89f320108b8ca29ca3850d5perrin-- ----------------------------------------------------------------------
fa9e4066f08beec538e775443c5be79dd423fcabahrenstoE :: String -> EXPRESSION
104e2ed78d9ef0a0f89f320108b8ca29ca3850d5perrintoE = fromJust . parseResult
104e2ed78d9ef0a0f89f320108b8ca29ca3850d5perrin-- parses a single extparam range such as: "I>0, J=1"
104e2ed78d9ef0a0f89f320108b8ca29ca3850d5perrintoEP :: String -> [EXTPARAM]
104e2ed78d9ef0a0f89f320108b8ca29ca3850d5perrintoEP [] = []
4ccbb6e737373468bb9dc1709618384cce4c9f92ahrenstoEP s = case runParser (Lexer.separatedBy extparam pComma >-> fst) "" "" s of
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee Left e -> error $ show e
fa9e4066f08beec538e775443c5be79dd423fcabahrens Right s' -> s'
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- parses lists of extparam ranges such as: "I>0, J=1; ....; I=10, J=1"
fa9e4066f08beec538e775443c5be79dd423fcabahrenstoEPL :: String -> [[EXTPARAM]]
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeetoEPL [] = []
fa9e4066f08beec538e775443c5be79dd423fcabahrenstoEPL s = case runParser
fa9e4066f08beec538e775443c5be79dd423fcabahrens (Lexer.separatedBy extparam pComma >-> fst) pSemi >-> fst) "" "" s of
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee Left e -> error $ show e
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee Right s' -> s'
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeetoEP1 :: String -> EPExp
fa9e4066f08beec538e775443c5be79dd423fcabahrenstoEP1 s = case runParser extparam "" "" s of
104e2ed78d9ef0a0f89f320108b8ca29ca3850d5perrin Left e -> error $ show e
af2c4821c0a23e873f2a63bca4145080aa2183e3maybee Right s' -> snd $ fromJust $ toEPExp s'
104e2ed78d9ef0a0f89f320108b8ca29ca3850d5perrintoEPs :: String -> EPExps
c25056de36a33f2a76f79dcf64593f731d258013gwtoEPs = toEPExps . toEP
4ccbb6e737373468bb9dc1709618384cce4c9f92ahrenstoEPLs :: String -> [EPExps]
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeetoEPLs = map toEPExps . toEPL
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- ----------------------------------------------------------------------
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- * Extended Parameter tests
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- ----------------------------------------------------------------------
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeesmtEQScript vMap (epList!!0) (epList!!1)
4e9583b23260dab68308b306795694143381ab0fTom Ericksontest for smt-export
a66b2b3504619207b55d222c87bdd9df52832f15Tom Ericksonlet m = varMapFromList ["I", "J", "K"]
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeelet be = boolExps m $ toEPs "I=0"
a66b2b3504619207b55d222c87bdd9df52832f15Tom EricksonsmtBoolExp be
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeecompare-check for yices
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeelet l3 = [(x,y) | x <- epList, y <- epList]
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeelet l2 = map (uncurry $ smtCompareUnsafe vMap) l3
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeputStrLn $ unlines $ map show $ zip l2 l3
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeesl <- sens (-3)
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeefst $ splitAS sl
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeepList :: [EPRange]
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee let l = map (Atom . toEPs)
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee ["", "I=1,J=0", "I=0,J=0", "I=0", "I=1", "J=0", "I>0", "I>2", "I>0,J>2"]
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee in Intersection l : Union l : l
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeevMap :: Map.Map String Int
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeevMap = varMapFromSet $ namesInList epList
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeprintOrdEPs :: String -> IO ()
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeprintOrdEPs s = let ft = forestFromEPs ((,) ()) $ toEPLs s
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee in putStrLn $ showEPForest show ft
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee--forestFromEPs :: (a -> EPTree b) -> [a] -> EPForest b
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeecompareEPgen :: Show a => (String -> a) -> (a -> a -> EPCompare) -> String -> String -> IO EPCompare
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeecompareEPgen p c a b =
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee let epA = p a
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee putStrLn $ show epA
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee putStrLn $ show epB
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee return $ c epA epB
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeecompareEP' = compareEPgen toEP1 compareEP
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeecompareEPs' = compareEPgen toEPs compareEPs
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- ----------------------------------------------------------------------
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- * MAPLE INTERPRETER
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- ----------------------------------------------------------------------
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- just call the methods in MapleInterpreter: mapleInit, mapleExit, mapleDirect
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- , the CS-interface functions and evalL
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- ----------------------------------------------------------------------
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- * FIRST REDUCE INTERPRETER
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- ----------------------------------------------------------------------
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- first reduce interpreter
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeereds :: Int -- ^ Test-spec
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee -> IO ReduceInterpreter
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee r <- redsInit
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee sendToReduce r "on rounded; precision 30;"
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- use "redsExit r" to disconnect where "r <- red"
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- many instances (connection/disconnection tests)
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeel <- mapM (const reds 1) [1..20]
4e9583b23260dab68308b306795694143381ab0fTom EricksonmapM redsExit l
4e9583b23260dab68308b306795694143381ab0fTom Erickson(l, r) <- redsBA 2
4e9583b23260dab68308b306795694143381ab0fTom Erickson'l' is a list of response values for each sentence in spec Test2
4e9583b23260dab68308b306795694143381ab0fTom Erickson'r' is the reduce connection
4e9583b23260dab68308b306795694143381ab0fTom Erickson-- ----------------------------------------------------------------------
4e9583b23260dab68308b306795694143381ab0fTom Erickson-- * SECOND REDUCE INTERPRETER
4e9583b23260dab68308b306795694143381ab0fTom Erickson-- ----------------------------------------------------------------------
4e9583b23260dab68308b306795694143381ab0fTom Erickson-- run the assignments from the spec
4e9583b23260dab68308b306795694143381ab0fTom Ericksonredc :: Int -- ^ verbosity level
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee -> Int -- ^ Test-spec
148434217c040ea38dc844384f6ba68d9b325906Matthew Ahrens -> IO RITrans
148434217c040ea38dc844384f6ba68d9b325906Matthew Ahrens r <- redcInit v
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeredcNames :: RITrans -> IO [String]
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeredcNames = runTest $ liftM toList names
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeredcValues :: RITrans -> IO [(String, EXPRESSION)]
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeredcValues = runTest values
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- run the assignments from the spec
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeredcCont :: Int -- ^ Test-spec
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee -> IO RITrans
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeredcCont i r = do
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee cl <- cmds i
4e9583b23260dab68308b306795694143381ab0fTom Erickson (res, r') <- runIOS r (runResultT $ evaluateList cl)
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee printDiags (PC.verbosity $ getRI r') (diags res)
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee--- Testing with many instances
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeelc <- time $ mapM (const $ redc 1 1) [1..20]
a66b2b3504619207b55d222c87bdd9df52832f15Tom EricksonmapM redcExit lc
a66b2b3504619207b55d222c87bdd9df52832f15Tom Erickson-- to communicate directly with reduce use:
a66b2b3504619207b55d222c87bdd9df52832f15Tom Ericksonlet r = head lc OR r <- redc x y
a66b2b3504619207b55d222c87bdd9df52832f15Tom Ericksonlet ri = getRI r
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeredcDirect ri "some command;"
a66b2b3504619207b55d222c87bdd9df52832f15Tom Erickson-- ----------------------------------------------------------------------
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- * TRANSFORMATION TESTS
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- ----------------------------------------------------------------------
a66b2b3504619207b55d222c87bdd9df52832f15Tom Ericksondata WithAB a b c = WithAB a b c
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeeinstance Show c => Show (WithAB a b c) where
a66b2b3504619207b55d222c87bdd9df52832f15Tom Erickson show (WithAB _ _ c) = show c
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeegetA (WithAB a _ _) = a
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeegetB (WithAB _ b _) = b
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeegetC (WithAB _ _ c) = c
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- tt = transformation tests (normally Calculationsystem monad result)
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- tte = tt with evaluation (normally gets a cs-state and has IO-result)
a66b2b3504619207b55d222c87bdd9df52832f15Tom EricksonrunTT c s vcc = do
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee (res, s') <- runIOS s $ runResultT $ runStateT c vcc
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee let (r, vcc') = fromJust $ resultToMaybe res
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee return $ WithAB vcc' s' r
b5fca8f855054d167d04d3b4de5210c83ed2083ctomeerunTTi c s = do
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee (res, s') <- runIOS s (runResultT $ runStateT c emptyVCCache)
fa9e4066f08beec538e775443c5be79dd423fcabahrens let (r, vcc') = fromJust $ resultToMaybe res
fa9e4066f08beec538e775443c5be79dd423fcabahrens return $ WithAB vcc' s' r
fa9e4066f08beec538e775443c5be79dd423fcabahrens--s -> t -> t1 -> IO (Common.Result.Result a, s)
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- ttesd :: ( VarGen (ResultT (IOS s))
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- , VariableContainer a VarRange
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- , CalculationSystem (ResultT (IOS s))
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- , Cache (ResultT (IOS s)) a String EXPRESSION) =>
4e9583b23260dab68308b306795694143381ab0fTom Erickson-- EXPRESSION -> s -> a -> IO (WithAB a s EXPRESSION)
fa9e4066f08beec538e775443c5be79dd423fcabahrensttesd e = runTT (substituteDefined e)
fa9e4066f08beec538e775443c5be79dd423fcabahrensttesdi e = runTTi (substituteDefined e)
b5fca8f855054d167d04d3b4de5210c83ed2083ctomee-- -- substituteDefined with init
fa9e4066f08beec538e775443c5be79dd423fcabahrens--ttesdi s e = ttesd s vc e
fa9e4066f08beec538e775443c5be79dd423fcabahrensr <- mapleInit 1
fa9e4066f08beec538e775443c5be79dd423fcabahrensr <- redcInit 3
fa9e4066f08beec538e775443c5be79dd423fcabahrensr' <- evalL r 3
fa9e4066f08beec538e775443c5be79dd423fcabahrenslet e = toE "sin(x) + 2*cos(y) + x^2"
fa9e4066f08beec538e775443c5be79dd423fcabahrensw <- ttesdi e r'
fa9e4066f08beec538e775443c5be79dd423fcabahrenslet vss = getA w
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- show value for const x
fa9e4066f08beec538e775443c5be79dd423fcabahrensrunTest (CSL.Interpreter.lookup "x") r' >>= return . pretty
fa9e4066f08beec538e775443c5be79dd423fcabahrensrunTest (CSL.Interpreter.eval $ toE "cos(x-x)") r' >>= return . pretty
fa9e4066f08beec538e775443c5be79dd423fcabahrensw' <- ttesd e r' vss
4e9583b23260dab68308b306795694143381ab0fTom Ericksonw' <- ttesd e r' vss
fa9e4066f08beec538e775443c5be79dd423fcabahrensy <- fmap fromJust $ runTest (CSL.Interpreter.lookup "y") r'
fa9e4066f08beec538e775443c5be79dd423fcabahrensrunTest (verificationCondition y $ toE "cos(x)") r'
fa9e4066f08beec538e775443c5be79dd423fcabahrensr <- mapleInit 4
fa9e4066f08beec538e775443c5be79dd423fcabahrensr <- redcInit 4
fa9e4066f08beec538e775443c5be79dd423fcabahrensr' <- evalL r 301
fa9e4066f08beec538e775443c5be79dd423fcabahrenslet t = toE "cos(z)^2 + cos(z ^2) + sin(y) + sin(z)^2"
fa9e4066f08beec538e775443c5be79dd423fcabahrenst' <- runTest (eval t) r'
fa9e4066f08beec538e775443c5be79dd423fcabahrensvc <- runTest (verificationCondition t' t) r'
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- exampleRun
fa9e4066f08beec538e775443c5be79dd423fcabahrensr <- mapleInit 4
fa9e4066f08beec538e775443c5be79dd423fcabahrenslet t = toE "factor(x^5-15*x^4+85*x^3-225*x^2+274*x-120)"
fa9e4066f08beec538e775443c5be79dd423fcabahrenst' <- runTest (eval t) r
fa9e4066f08beec538e775443c5be79dd423fcabahrensvc <- runTest (verificationCondition t' t) r
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- exampleRun2
fa9e4066f08beec538e775443c5be79dd423fcabahrensr <- mapleInit 4
fa9e4066f08beec538e775443c5be79dd423fcabahrensr' <- evalL r 1011
fa9e4066f08beec538e775443c5be79dd423fcabahrenslet t = toE "factor(x^5-z4*x^4+z3*x^3-z2*x^2+z1*x-z0)"
fa9e4066f08beec538e775443c5be79dd423fcabahrenst' <- runTest (eval t) r'
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wrightvc <- runTest (verificationCondition t' t) r'
fa9e4066f08beec538e775443c5be79dd423fcabahrenslet l = ["z4+z3+20", "z2 + 3*z4 + 4", "3 * z3 - 30", "5 * z4 + 10", "15"]
fa9e4066f08beec538e775443c5be79dd423fcabahrenslet tl = map toE l
fa9e4066f08beec538e775443c5be79dd423fcabahrenstl' <- mapM (\x -> runTest (eval x) r') tl
fa9e4066f08beec538e775443c5be79dd423fcabahrensvcl <- mapM (\ (x, y) -> runTest (verificationCondition x y) r') $ zip tl' tl
fa9e4066f08beec538e775443c5be79dd423fcabahrensmapM_ putStrLn $ map pretty vcl
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- ----------------------------------------------------------------------
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- * Utilities
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- ----------------------------------------------------------------------
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- ----------------------------------------------------------------------
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- ** Operator extraction
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- ----------------------------------------------------------------------
fa9e4066f08beec538e775443c5be79dd423fcabahrensaddOp :: Map.Map String Int -> String -> Map.Map String Int
fa9e4066f08beec538e775443c5be79dd423fcabahrensaddOp mp s = Map.insertWith (+) s 1 mp
fa9e4066f08beec538e775443c5be79dd423fcabahrensclass OpExtractor a where
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr :: Map.Map String Int -> a -> Map.Map String Int
fa9e4066f08beec538e775443c5be79dd423fcabahrensinstance OpExtractor EXPRESSION where
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr m (Op op _ l _) = extr (addOp m $ show op) l
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr m (Interval _ _ _) = addOp m "!Interval"
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr m (Int _ _) = addOp m "!Int"
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr m (Double _ _) = addOp m "!Double"
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr m (List l _) = extr (addOp m "!List") l
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr m (Var _) = addOp m "!Var"
fa9e4066f08beec538e775443c5be79dd423fcabahrensinstance OpExtractor [EXPRESSION] where
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr = foldl extr
fa9e4066f08beec538e775443c5be79dd423fcabahrensinstance OpExtractor (EXPRESSION, [CMD]) where
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr m (e,l) = extr (extr m e) l
fa9e4066f08beec538e775443c5be79dd423fcabahrensinstance OpExtractor CMD where
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr m (Ass c def) = extr m [c, def]
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr m (Cmd _ l) = extr m l
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr m (Sequence l) = extr m l
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr m (Cond l) = foldl extr m l
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr m (Repeat e l) = extr m (e,l)
fa9e4066f08beec538e775443c5be79dd423fcabahrensinstance OpExtractor [CMD] where
fa9e4066f08beec538e775443c5be79dd423fcabahrens extr = foldl extr
fa9e4066f08beec538e775443c5be79dd423fcabahrensextractOps :: OpExtractor a => a -> Map.Map String Int
fa9e4066f08beec538e775443c5be79dd423fcabahrensextractOps = extr Map.empty
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- -- ----------------------------------------------------------------------
fa9e4066f08beec538e775443c5be79dd423fcabahrens-- -- ** Assignment extraction
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- -- ----------------------------------------------------------------------
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- addOp :: Map.Map String Int -> String -> Map.Map String Int
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- addOp mp s = Map.insertWith (+) s 1 mp
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- class OpExtractor a where
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extr :: Map.Map String Int -> a -> Map.Map String Int
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- instance OpExtractor EXPRESSION where
9e1320c015cea6985d2122bc1d654b79fa479f7aMark Shellenbaum-- extr m (Op op _ l _) = extr (addOp m op) l
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extr m (Interval _ _ _) = addOp m "!Interval"
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extr m (Int _ _) = addOp m "!Int"
89459e17032b6bb1d59eebd2b7c0d06859d4657cMark Shellenbaum-- extr m (Double _ _) = addOp m "!Double"
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extr m (List l _) = extr (addOp m "!List") l
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extr m (Var _) = addOp m "!Var"
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- instance OpExtractor [EXPRESSION] where
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extr = foldl extr
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- instance OpExtractor (EXPRESSION, [CMD]) where
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extr m (e,l) = extr (extr m e) l
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- instance OpExtractor CMD where
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extr m (Cmd _ l) = extr m l
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extr m (Sequence l) = extr m l
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extr m (Cond l) = foldl extr m l
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extr m (Repeat e l) = extr m (e,l)
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- instance OpExtractor [CMD] where
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extr = foldl extr
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extractOps :: OpExtractor a => a -> Map.Map String Int
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- extractOps = extr Map.empty
89459e17032b6bb1d59eebd2b7c0d06859d4657cMark Shellenbaum-- -- ----------------------------------------------------------------------
89459e17032b6bb1d59eebd2b7c0d06859d4657cMark Shellenbaum-- -- * static analysis functions
743a77ed89085d3c232c4a2f65ab4e19576839e2Alan Wright-- -- ----------------------------------------------------------------------