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
gr <- fmap (assDepGraphFromDescList (const $ const True) . fst)testResult 102 assStoreAndProgSimple
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
startP = ("MAIN TESTING FUNCTIONS:" /=)
putStrLn $ unlines $ takeWhile endP $ dropWhile startP l
instance Pretty Bool where
data CAS = Maple | Mathematica deriving (Show, Read, Eq)
data CASState = MapleState MITrans | MathematicaState MathState
-- ------------------------- Shortcuts --------------------------
initFlags :: (StepDebugger m, SymbolicEvaluator m) => Bool -> Bool -> m ()
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 -}
prettyInfo $ text "****************** Assignment store loaded ******************"
when (isJust mE) $ prettyInfo $ pretty $ fromJust mE
-- readEvalPrintLoop stdin stdout ">" exitWhen
(mit, _) <- testWithMapleGen v to (initFlags smode dmode) p lb sp
when cl $ mapleExit mit >> return ()
(mst, _) <- testWithMathematicaGen v mFp mN (initFlags smode dmode) p lb sp
when cl $ mathematicaExit mst
return $ MathematicaState mst
mapleLoop :: MITrans -> IO ()
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
-- 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
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
testWithMapleGen v to = testWithCASGen rf where
rf adg = runWithMaple adg v to
-- , "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
testWithMathematicaGen v mFp mN = testWithCASGen rf where
rf adg = runWithMathematica adg v mFp mN
testWithMapleGen :: Int -> DTime -> ([Named CMD] -> MapleIO a) -> String -> String
testWithMapleGen verb to f lb sp = do
ncl <- fmap sigsensNamedSentences $ sigsensGen lb sp
-- get ordered assignment store and program
(as, prog) <- assStoreAndProgSimple ncl
-- build the dependency graph
let gr = assDepGraphFromDescList (const $ const ()) as
-- make sure that the assignment store is loaded into maple before
g x = loadAS as >> modify (\ mit -> mit {vericondOut = Just vchdl}) >> f x
res <- runWithMaple gr verb to
-- , "intpakX" -- Problems with the min,max functions, they are remapped by this package!
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
-- build the dependency graph
let gr = assDepGraphFromDescList (const $ const ()) as
{- make sure that the assignment store is loaded into maple before
g x = ip >> loadAS as >> modify (\ mit -> mit {vericondOut = Just vchdl}) >> f x
{- ----------------------------------------------------------------------
---------------------------------------------------------------------- -}
-- | Returns all constants where the given constants depend on
depClosure :: [String] -> [Named CMD] -> IO [[String]]
let (asss, _) = splitAS ncl
gm = fmap analyzeGuarded asss
dr = getDependencyRelation gm
markFinal :: [String] -> [Named CMD] -> IO [String]
let (asss, _) = splitAS ncl
gm = fmap analyzeGuarded asss
dr = getDependencyRelation gm
Just s -> if
Set.null s then x ++ " *" else x
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
if simpleName oi == s then Just $ senAttr nc else Nothing
inDefinition :: [String] -> [Named CMD] -> IO [String]
let (asss, _) = splitAS ncl
gm = fmap analyzeGuarded asss
dr = getDependencyRelation gm
allDefs = allDefinitions ncl
f' (x, y) = x ++ ": " ++ intercalate ", " y
allDefinitions :: [Named CMD] ->
Map.Map String String
f nc = case sentence nc of
Ass (Op oi _ _ _) _ -> Just (simpleName oi, senAttr nc)
undef :: [Named CMD] -> [String]
undef ncl =
Set.toList $ undefinedConstants $ fst $ splitAS ncl
relLayer :: Ord a => Rel2 a -> [a] -> [[a]]
relLayer r l = l : relLayer r succs where
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
fromMaybe "" $ rolookup (getBMap mit) $ SimpleConstant s
enclConst :: ASState a -> String -> OPID
fromMaybe (error $ "enclConst: no mapping for " ++ s) $ revlookup (getBMap mit) s
{- ----------------------------------------------------------------------
---------------------------------------------------------------------- -}
-- Testing of keyboard-input
{- when (c /= 'e') $ putStrLn "" >> putStrLn (c:[]) >> putStrLn (show $ ord c) >> charInfo
when (ord c /= 27) $ putStrLn "" >> putStrLn [c] >> print $ ord c >> charInfo
testspecs :: [(Int, (String, String))]
sigsensGen :: String -> String -> IO (SigSens Sign CMD)
hlib <- getEnvDef "HETS_LIB" $ error "Missing HETS_LIB environment variable"
let fp = if b then lb else hlib ++ "/" ++ lb
ho = defaultHetcatsOpts { libdirs = [hlib]
res <- getSigSensComplete True ho CSL fp sp
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)
sigsens :: Int -> IO (Sign, [Named CMD])
return ( sigsensSignature res, sigsensNamedSentences res )
-- Check if the order is broken or not!
sens :: Int -> IO [Named CMD]
sens = fmap snd . sigsens
cmds = fmap (map sentence) . sens
-- time measurement, pendant of the time shell command
time :: MonadIO m => m a -> m a
t <- liftIO getCurrentTime
t' <- liftIO getCurrentTime
liftIO $ print $ diffUTCTime t' t
toE :: String -> EXPRESSION
toE = fromJust . parseExpression operatorInfoMap
toCmd = fromJust . parseCommand
{- ----------------------------------------------------------------------
---------------------------------------------------------------------- -}
data TestEnv = TestEnv { counter :: Int
hdl <- openFile logf WriteMode
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
execSMTTester' ::
CMP.VarEnv -> SmtTester a -> IO a
execSMTTester' ve smt = do
(x, i) <- execSMTTester ve smt
putStrLn $ "SMT-Checks: " ++ show i
instance CompareIO SmtTester where
let f x = x {counter = counter x + 1}
lift $ writeRangesToLog hdl r1 r2
liftIO $ hPutStrLn hdl ""
lift $ writeRangesToLog hdl r1 r2 >> hPutStrLn hdl ('=' : show 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)
{- ----------------------------------------------------------------------
---------------------------------------------------------------------- -}
show guarded assignments:
-- ----------------------------------------------------------------------
-- * 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)
(res, r') <- runIOS r $ runResultT cmd
return (fromJust $ resultToMaybe res, r')
evalL :: AssignmentStore (ResultT (IOS b)) => b
(_, s') <- runIOS s (runResultT $ evaluateList cl)
-- ----------------------------------------------------------------------
-- ----------------------------------------------------------------------
-- parses a single extparam range such as: "I>0, F=1"
toEP :: String -> [EXTPARAM]
-- parses lists of extparam ranges such as: "I>0, F=1; ....; I=10, F=1"
toEPL :: String -> [[EXTPARAM]]
toEP1 s = case runParser extparam "" "" s of
Right s' -> snd $ fromJust $ toEPExp s'
toEPs :: String -> EPExps
toEPLs :: String -> [EPExps]
toEPLs = map toEPExps . toEPL
-- ----------------------------------------------------------------------
-- * Extended Parameter tests
-- ----------------------------------------------------------------------
smtEQScript vMap (boolRange vMap $ epList!!0) (boolRange vMap $ epList!!1)
let m = varMapFromList ["I", "J", "F"]
let be = boolExps m $ toEPs "I=0"
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
let grdm = fst $ splitAS sl
let sgm = dependencySortAS grdm
let sgm = dependencySortAS grdm
getDependencyRelation grdm
gm <- fmap grddMap $ sens (-3)
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
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 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 (x:l) = map ((,) x) l ++ irrTriang l
frmAround s = let l = lines s
hd = "--" ++ map (const '-') (head l)
in unlines $ hd : map (('|':) . (++"|")) l ++ [hd]
modelRg1 ::
Map.Map String (Int, Int)
modelRg2 ::
Map.Map String (Int, Int)
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
pM2 = putStr . frmAround . printModel modelRg2
pM1 = putStr . frmAround . printModel modelRg1
toEPR :: String -> EPRange
el11 = let x1 = toEPR "I>=0" in [x1, Complement x1]
el12 = let l = map toEPR ["I=1", "I>1"] in Complement (Union l) : l
el13 = let x1 = toEPR "I>0" in [x1, Complement x1]
el21 = let x1 = toEPR "I>=0" in [x1, Complement x1]
el22 = let l = map toEPR ["I>=0, F>=0", "I<4, F<=4"]
in uni : inter : Intersection [uni, Complement inter] : l
el23 = let x1 = toEPR "I>0" in [x1, Complement x1]
checkForPartition :: [EPRange] -> IO Bool
checkForPartition l = execSMTTester' vEnv1 $ f g l where
return $ and $ res' : res
g x y = fmap (Incomparable Disjoint ==) $ rangeCmp x y
part2 = Partition $ zip el11 [33 ..]
part3 = Partition $ zip el12 [1 ..]
part4 = Partition $ zip el13 [91 ..]
parts = [part1, part2, part3, part4]
refinePart a b = execSMTTester' vEnv1 $ refinePartition a b
m1 <- mapM (uncurry refinePart) $ irrTriang parts
m2 <- mapM (uncurry refinePart) $ irrTriang m1
putStrLn "=============================================="
putStrLn "=============================================="
showPart1s :: Show a => [Partition a] -> IO ()
showPart1s = let f x = showPart1 x >> putStrLn "==="
showPartX :: Show a => (EPRange -> IO ()) -> Partition a -> IO ()
showPart1 :: Show a => Partition a -> IO ()
showPart2 :: Show a => Partition a -> IO ()
showPartX _ (AllPartition x) = do
showPartX fM (Partition l) =
showPart1 = showPartX pM1
showPart2 = showPartX pM2
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 "==="
let grdm = fst $ splitAS sl
let sgm = dependencySortAS grdm
-- elimTestInit :: Int -> [(String, Guarded EPRange)] -> IO [Guard EPRange]
let grd = (guards $ snd $ head gl)!!i
execSMTTester' vEnv $ eliminateGuard
Map.empty grd
pgX :: (EPRange -> IO a) -> Guard EPRange -> IO ()
putStrLn $ show $ pretty $ definition grd
pg1 :: Guard EPRange -> IO ()
pg2 :: Guard EPRange -> IO ()
pgrddX :: (EPRange -> IO a) -> Guarded EPRange -> IO ()
pgrddX fM grdd = mapM_ (pgX fM) $ guards grdd
pgrdd2 :: Guarded EPRange -> IO ()
printASX :: (EPRange -> IO a) -> [(String, Guarded EPRange)] -> IO ()
printASX fM l = mapM_ f l where
printAS1 :: [(String, Guarded EPRange)] -> IO ()
printAS2 :: [(String, Guarded EPRange)] -> IO ()
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])]
getASana :: Int -> IO [(String, Guarded EPRange)]
getASana = liftM (
Map.toList . fmap analyzeGuarded . fst . splitAS) . sens
elimEPs :: [(String, Guarded EPRange)] -> IO [(String, Guarded EPRange)]
-- 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)
varEnvFromList :: [String] -> VarEnv
varEnvFromList l = error ""
-- | Generates from a list of Extended Parameter names an id-mapping
varMapFromList :: [String] -> VarMap
-- | Generates from a list of Extended Parameter names an id-mapping
varMapFromSet ::
Set.Set String -> VarMap
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 = 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 }
--vEnv = VarEnv { varmap = vMap, vartypes = vTypes, loghandle = Nothing }
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
compareEP' = compareEPgen toEP1 compareEP
compareEPs' = compareEPgen toEPs compareEPs
-- ----------------------------------------------------------------------
-- ----------------------------------------------------------------------
-- 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
sendToReduce r "on rounded; precision 30;"
-- use "redsExit r" to disconnect where "r <- red"
l <- mapM (const reds 1) [1..20]
'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
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
(res, r') <- runIOS r (runResultT $ evaluateList cl)
--- Testing with many instances
lc <- time $ mapM (const $ redc 1 1) [1..20]
-- to communicate directly with reduce use:
let r = head lc OR r <- redc x y
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
-- tt = transformation tests (normally Calculationsystem monad result)
-- tte = tt with evaluation (normally gets a cs-state and has IO-result)
(res, s') <- runIOS s $ runResultT $ runStateT c vcc
let (r, vcc') = fromJust $ resultToMaybe res
return $ WithAB vcc' s' r
(res, s') <- runIOS s (runResultT $ runStateT c emptyVCCache)
let (r, vcc') = fromJust $ resultToMaybe res
return $ WithAB vcc' s' r
-- 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
let e = toE "sin(x) + 2*cos(y) + x^2"
-- show value for const x
runTest (verificationCondition y $ toE "cos(x)") r'
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'
let t = toE "factor(x^5-15*x^4+85*x^3-225*x^2+274*x-120)"
vc <- runTest (verificationCondition t' t) r
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'
let l = ["z4+z3+20", "z2 + 3*z4 + 4", "3 * z3 - 30", "5 * z4 + 10", "15"]
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
-- ----------------------------------------------------------------------
-- ----------------------------------------------------------------------
-- ----------------------------------------------------------------------
-- ** Operator extraction
-- ----------------------------------------------------------------------
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
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
extractOps :: OpExtractor a => a ->
Map.Map String Int
-- -- ----------------------------------------------------------------------
-- -- ** Assignment extraction
-- -- ----------------------------------------------------------------------
-- 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
-- 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
-- extractOps :: OpExtractor a => a ->
Map.Map String Int
-- -- ----------------------------------------------------------------------
-- -- * static analysis functions
-- -- ----------------------------------------------------------------------
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 ]
opsCas = [ OP_maximize, OP_factor
, OP_divide, OP_factorize, OP_int, OP_rlqe, OP_simplify, OP_solve ]
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 ]
opsQuant = [ OP_ex, OP_all ]
{- ----------------------------------------------------------------------
---------------------------------------------------------------------- -}
readAndPrintOutput :: ML ()
let pr | exptype == dfMLTKSYM = readAndPrintML "Symbol: " mlGetSymbol
| exptype == dfMLTKSTR = readAndPrintML "String: " mlGetString
| exptype == dfMLTKINT = readAndPrintML "Int: " mlGetInteger
| exptype == dfMLTKREAL = readAndPrintML "Real: " mlGetReal
| exptype == dfMLTKFUNC =
if len == 0 then mlProcError
let f i = readAndPrintOutput
>> when (i < len) $ userMessage ", "
| exptype == dfMLTKERROR = userMessageLn "readAndPrintOutput-error" >> mlProcError
| otherwise = userMessageLn ("readAndPrintOutput-error" ++ show exptype)
userMessage :: String -> ML ()
userMessageLn :: String -> ML ()
instance MLShow String where
instance MLShow CDouble where
instance MLShow CInt where
readAndPrintML :: MLShow a => String -> ML a -> ML ()
readAndPrintML _ pr = pr >>= userMessage . mlshow
sendPlus :: CInt -> CInt -> CInt -> ML ()
mlPutFunction "EvaluatePacket" 1
sendFormula :: CInt -> CInt -> CInt -> ML ()
mlPutFunction "EvaluatePacket" 1
{- ----------------------------------------------------------------------
---------------------------------------------------------------------- -}
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
let mN = if null s then Nothing else Just s
Left eid -> putStrLn ("Error " ++ show eid) >> error "ml-test"
Right res -> putStrLn ("OK: " ++ show (pretty res)) >> return res
mlP1 i j k = forM_ [1 .. k] $ sendFormula i j >=>
const (waitForAnswer >> readAndPrintOutput >> userMessageLn "")
mlTest :: [String] -> IO ()
let (k, i, j) = (read $ head argv, read $ argv !! 1, read $ argv !! 2)
s = if length argv > 3 then argv !! 3 else ""
mlP2 k e = forM [1 .. (k :: Int)] $ const $ sendEvalPacket (sendExpression True e)
>> waitForAnswer >> receiveExpression
mlTest2 :: [String] -> IO [EXPRESSION]
s = if length argv > 2 then argv !! 2 else ""
-- a good interactive stepper through the mathlink interface
mlP3 :: String -> Int -> ML ()
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
| g == dfMLTKSYM = "Symbol"
| g == dfMLTKSTR = "String"
| g == dfMLTKREAL = "Real"
liftIO $ putStrLn $ "getnext -> " ++ gt 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
liftIO $ putStrLn $ c : (": " ++ show i)
-- mlTestEnv cn $ 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 ()
sendEvalPacket (sendExpression True $ toE s)
sendEvalPacket (sendExpressionString s)
liftIO $ putStrLn $ show e ++ ": " ++ show (pretty e')