{-# LANGUAGE TypeSynonymInstances, FlexibleContexts #-}
{- |
Module      :  $Header$
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 . putStrLn . show . 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 = do
  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 prog =
        runWithMaple adg v to
           [ "EnCLFunctions"
           -- , "intpakX" -- Problems with the min,max functions, they are remapped by this package!
           ] prog


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 prog =
        runWithMathematica adg v mFp mN
           [ "/home/ewaryst/Hets/CSL/CAS/Mathematica.m" ] prog



{-
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 l' = map (g m) l'
      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 (flip 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:[]) >> putStrLn (show $ ord c) >> charInfo


testspecs :: [(Int, ([Char], [Char]))]
testspecs =
    [ (44, ("EnCL/EN1591.het", "EN1591"))
    , (45, ("EnCL/flange.het", "Flange"))
    , (46, ("EnCL/flange.het", "FlangeComplete"))
    , (54, ("EnCL/EN1591S.het", "EN1591"))
    , (55, ("EnCL/flangeS.het", "Flange"))
    , (56, ("EnCL/flangeS.het", "FlangeComplete"))
    , (65, ("EnCL/flangeDefault.het", "FlangeDefault"))
    , (66, ("EnCL/flangeExported.het", "FlangeComplete"))
    ]


sigsensGen :: String -> String -> IO (SigSens Sign CMD)
sigsensGen lb sp = do
  hlib <- getEnvDef "HETS_LIB" $ error "Missing HETS_LIB environment variable"
  b <- doesFileExist lb
  let fp = if b then lb else hlib ++ "/" ++ lb
      ho = defaultHetcatsOpts { libdirs = [hlib]
                              , verbose = 0 }

  res <- getSigSensComplete True ho CSL fp sp
  putStrLn "\n"
  return res

siggy :: Int -> IO (SigSens Sign CMD)
siggy = uncurry sigsensGen . libFP

libFP :: Int -> (String, String)
libFP i = fromMaybe (if i >= 0 then ("EnCL/Tests.het", "Test" ++ show i)
                            else ("EnCL/ExtParamExamples.het", "E" ++ show (- i)))
          $ Prelude.lookup i testspecs

sigsens :: Int -> IO (Sign, [Named CMD])
sigsens i = do
  res <- siggy i
  return ( sigsensSignature res, sigsensNamedSentences res )

sig :: Int -> IO Sign
sig = fmap fst . sigsens

-- Check if the order is broken or not!
sens :: Int -> IO [Named CMD]
sens = fmap snd . sigsens

cmds :: Int -> IO [CMD]
cmds = fmap (map sentence) . sens

-- time measurement, pendant of the time shell command
time :: MonadIO m => m a -> m a
time p = do
  t <- liftIO getCurrentTime
  res <- p
  t' <- liftIO getCurrentTime
  liftIO $ putStrLn $ show $ 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.het
el11 :: [EPRange]
el11 = let x1 = toEPR "I>=0" in [x1, Complement x1]

el12 :: [EPRange]
el12 = let l = map toEPR ["I=1", "I>1"] in Complement (Union l) : l

el13 :: [EPRange]
el13 = let x1 = toEPR "I>0" in [x1, Complement x1]


el21 :: [EPRange]
el21 = let x1 = toEPR "I>=0" in [x1, Complement x1]

el22 :: [EPRange]
el22 = let l = map toEPR ["I>=0, F>=0", "I<4, F<=4"]
           inter = Intersection l
           uni = Union l
       in uni : inter : Intersection [uni, Complement inter] : l

el23 :: [EPRange]
el23 = let x1 = toEPR "I>0" in [x1, Complement x1]


-- * Partition tests

checkForPartition :: [EPRange] -> IO Bool
checkForPartition l = execSMTTester' vEnv1 $ f g l where
    f a [] = return True
    f a (x:l') = do
      res <- mapM (a x) l'
      res' <- f a l'
      return $ and $ res' : res
    g x y = fmap (Incomparable Disjoint ==) $ rangeCmp x y


part1 :: Partition Int
part1 = AllPartition 10

part2 :: Partition Int
part2 = Partition $ zip el11 [33 ..]

part3 :: Partition Int
part3 = Partition $ zip el12 [1 ..]

part4 :: Partition Int
part4 = Partition $ zip el13 [91 ..]

parts = [part1, part2, part3, part4]

refinePart a b = execSMTTester' vEnv1 $ refinePartition a b

allRefin = do
  m1 <- mapM (uncurry refinePart) $ irrTriang parts
  m2 <- mapM (uncurry refinePart) $ irrTriang m1
  return (m1, m2)

allRShow = do
  (a, b) <- allRefin
  showPart1s a
  putStrLn "=============================================="
  showPart1s b

allRCmp = do
  (a, b) <- allRefin
  cmpRg1s a
  putStrLn "=============================================="
  cmpRg1s b


showPart1s :: Show a => [Partition a] -> IO ()
showPart1s = let f x = showPart1 x >> putStrLn "==="
             in  mapM_ f

showPartX :: Show a => (EPRange -> IO ()) -> Partition a -> IO ()
showPart1 :: Show a => Partition a -> IO ()
showPart2 :: Show a => Partition a -> IO ()

showPartX _ (AllPartition x) = do
  putStrLn $ show x
  putStrLn "All\n\n"

showPartX fM (Partition l) =
  let f (re, x) = do
        putStrLn $ show x
        fM re
        putStrLn "\n"
  in mapM_ f l

showPart1 = showPartX pM1
showPart2 = showPartX pM2

class HasRanges a where
    getRanges :: a -> [EPRange]

instance HasRanges (Partition a) where
    getRanges (AllPartition x) = []
    getRanges (Partition l) = map fst l

instance HasRanges a => HasRanges [a] where
    getRanges = concatMap getRanges

instance HasRanges (Guarded EPRange) where
    getRanges = map range . guards

instance HasRanges (String, Guarded EPRange) where
    getRanges = map range . guards . snd

cmpRg1 :: HasRanges a => a -> IO ()
cmpRg1 = putStrLn . concat . map (printModel modelRg1) . getRanges

cmpRg1s :: HasRanges a => [a] -> IO ()
cmpRg1s = let f = putStrLn . concat . map (printModel modelRg1) . getRanges
              g x = f x >> putStrLn "==="
          in mapM_ g

-- * elim proc testing

{-
: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
                           >> if i < len then userMessage ", " else return ()
                 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 $ argv!!0, 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 $ argv!!0
      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




  

  
