content: {-# 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 Text.ParserCombinators.Parsec
  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
        ve = CMP.VarEnv { CMP.varmap = Map.fromList $ zip ["I", "F"] [1 ..]
                        , CMP.vartypes = Map.empty
                        , 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
             [ "/home/ewaryst/Hets/CSL/CAS/Mathematica.m" ]
  
  
  {-
  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
      succs = Set.toList $ Set.unions $ mapMaybe (`Map.lookup` r) l
  
  
  {- 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.dol", "EN1591"))
      , (45, ("EnCL/flange.dol", "Flange"))
      , (46, ("EnCL/flange.dol", "FlangeComplete"))
      , (54, ("EnCL/EN1591S.dol", "EN1591"))
      , (55, ("EnCL/flangeS.dol", "Flange"))
      , (56, ("EnCL/flangeS.dol", "FlangeComplete"))
      , (65, ("EnCL/flangeDefault.dol", "FlangeDefault"))
      , (66, ("EnCL/flangeExported.dol", "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.dol", "Test" ++ show i)
                              else ("EnCL/ExtParamExamples.dol", '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
                (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
  
  :l CSL/InteractiveTests.hs
  :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
  
  :l CSL/InteractiveTests.hs
  :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.dol
  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
  
  {-
  :l CSL/InteractiveTests.hs
  :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 :: Map.Map String Int -> String -> Map.Map String Int
  addOp mp s = Map.insertWith (+) s 1 mp
  
  class OpExtractor a where
      extr :: Map.Map String Int -> a -> Map.Map String Int
  
  instance OpExtractor EXPRESSION where
      extr m (Op op _ l _) = extr (addOp m $ 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 :: Map.Map String Int -> String -> Map.Map String Int
  -- addOp mp s = Map.insertWith (+) s 1 mp
  
  -- class OpExtractor a where
  --     extr :: Map.Map String Int -> a -> Map.Map String Int
  
  -- instance OpExtractor EXPRESSION where
  --     extr m (Op op _ l _) = extr (addOp m op) l
  --     extr m (Interval _ _ _) = addOp m "!Interval"
  --     extr m (Int _ _) = addOp m "!Int"
  --     extr m (Double _ _) = addOp m "!Double"
  --     extr m (List l _) = extr (addOp m "!List") l
  --     extr m (Var _) = addOp m "!Var"
  
  -- instance OpExtractor [EXPRESSION] where
  --     extr = foldl extr
  
  -- instance OpExtractor (EXPRESSION, [CMD]) where
  --     extr m (e,l) = extr (extr m e) l
  
  -- instance OpExtractor CMD where
  --     extr m (Cmd _ l) = extr m l
  --     extr m (Sequence l) = extr m l
  --     extr m (Cond l) = foldl extr m l
  --     extr m (Repeat e l) = extr m (e,l)
  
  -- instance OpExtractor [CMD] where
  --     extr = foldl extr
  
  -- extractOps :: OpExtractor a => a -> Map.Map String Int
  -- extractOps = extr Map.empty
  
  -- -- ----------------------------------------------------------------------
  -- -- * static analysis functions
  -- -- ----------------------------------------------------------------------
  
  -- 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
  