content: {-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
  {- |
  Module      :  ./CSL/MapleInterpreter.hs
  Description :  Maple instance for the AssignmentStore class
  Copyright   :  (c) Ewaryst Schulz, DFKI Bremen 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Ewaryst.Schulz@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  Maple as AssignmentStore
  -}
  
  module CSL.MapleInterpreter where
  
  import Common.ProverTools (missingExecutableInPath)
  import Common.Utils (getEnvDef, trimLeft)
  import Common.Doc
  import Common.DocUtils
  import Common.IOS
  
  import CSL.AS_BASIC_CSL
  import CSL.ASUtils
  import CSL.Print_AS
  import CSL.Parse_AS_Basic (parseExpression)
  import CSL.Interpreter
  import CSL.Verification
  import CSL.DependencyGraph
  import CSL.GenericInterpreter
  
  -- the process communication interface
  import qualified Interfaces.Process as PC
  
  import Control.Monad
  -- import Control.Monad.Trans (MonadTrans (..), MonadIO (..))
  import Control.Monad.Error (ErrorT (..), MonadError (..))
  import Control.Monad.State.Class
  import Control.Monad.Reader
  
  import Data.List hiding (lookup)
  import qualified Data.Set as Set
  import Data.Maybe
  import System.Exit (ExitCode)
  import System.IO
  
  import Prelude hiding (lookup)
  
  {- ----------------------------------------------------------------------
  Maple Types and Instances
  ---------------------------------------------------------------------- -}
  
  type ConnectInfo = (PC.CommandState, PC.DTime)
  
  -- | MapleInterpreter with Translator based on the CommandState
  type MITrans = ASState ConnectInfo
  
  updateCS :: PC.CommandState -> ConnectInfo -> ConnectInfo
  updateCS cs (_, dt) = (cs, dt)
  
  updateDT :: PC.DTime -> ConnectInfo -> ConnectInfo
  updateDT dt (cs, _) = (cs, dt)
  
  getChannelTimeout :: MITrans -> PC.DTime
  getChannelTimeout = snd . getConnectInfo
  
  setChannelTimeout :: PC.DTime -> MITrans -> MITrans
  setChannelTimeout dt = fmap (updateDT dt)
  
  getMI :: MITrans -> PC.CommandState
  getMI = fst . getConnectInfo
  
  setMI :: PC.CommandState -> MITrans -> MITrans
  setMI cs = fmap (updateCS cs)
  
  -- Maple interface, built on CommandState
  type MapleIO = ErrorT ASError (IOS MITrans)
  
  instance AssignmentStore MapleIO where
      assign = genAssign mapleAssignDirect
      assigns l = genAssigns mapleAssignsDirect l >> return ()
      lookup = genLookup mapleLookupDirect
      eval = genEval mapleEvalDirect
      check = mapleCheck
      names = liftM (SMem . getBMap) get
      evalRaw s = get >>= liftIO . flip (mapleDirect True) s
  
      getUndefinedConstants e = do
        adg <- gets depGraph
        let g = isNothing . depGraphLookup adg
        return $ Set.filter g $ Set.map SimpleConstant $ setOfUserDefined e
  
      genNewKey = do
        mit <- get
        let (bm, i) = genKey $ getBMap mit
        put mit { getBMap = bm }
        return i
  
      getDepGraph = gets depGraph
      updateConstant n def =
          let f gr = updateGraph gr n
                       DepGraphAnno { annoDef = def
                                    , annoVal = () }
              mf mit = mit { depGraph = f $ depGraph mit }
          in modify mf
  
  instance VCGenerator MapleIO where
      addVC ea e = do
        let
            s = show
                $ (text "Verification condition for" <+> pretty ea <> text ":")
                      $++$ printExpForVC e
            {- s = show $ printExpForVC e <> text ";"
            s = (++ "\n\n;\n\n") $ showRaw $ text "VC for" <+> pretty ea <> text ":" $++$ pretty e
  vcHdl = stdout -}
        vcHdl <- liftM (fromMaybe stdout) $ gets vericondOut
        liftIO $ hPutStrLn vcHdl s where
  
  instance StepDebugger MapleIO where
      setDebugMode b = modify mf where mf mit = mit { debugMode = b }
      getDebugMode = gets debugMode
  
  instance SymbolicEvaluator MapleIO where
      setSymbolicMode b = modify mf where mf mit = mit { symbolicMode = b }
      getSymbolicMode = gets symbolicMode
  
  instance MessagePrinter MapleIO where
      printMessage = liftIO . putStrLn
  
  {- ----------------------------------------------------------------------
  Maple syntax functions
  ---------------------------------------------------------------------- -}
  
  data OfMaple a = OfMaple { mplValue :: a }
  
  type MaplePrinter = Reader (OfMaple OpInfoNameMap)
  
  instance ExpressionPrinter MaplePrinter where
      getOINM = asks mplValue
      printOpname = return . text . mplShowOPNAME
  
  printMaplePretty :: MaplePrinter Doc -> Doc
  printMaplePretty = flip runReader $ OfMaple mapleOpInfoNameMap
  
  class MaplePretty a where
      mplPretty :: a -> Doc
  
  instance MaplePretty EXPRESSION where
      mplPretty e = printMaplePretty $ printExpression e
  
  instance MaplePretty AssDefinition where
      mplPretty def = printMaplePretty $ printAssDefinition def
  
  instance MaplePretty String where
      mplPretty = text
  
  instance (MaplePretty a, MaplePretty b) => MaplePretty [(a, b)] where
      mplPretty = ppPairlist mplPretty mplPretty braces sepBySemis (<>)
  
  
  printExp :: EXPRESSION -> String
  printExp = show . mplPretty
  
  
  mplShowOPNAME :: OPNAME -> String
  mplShowOPNAME OP_approx = "evalf"
  mplShowOPNAME x = showOPNAME x
  
  mapleOpInfoMap :: OpInfoMap
  mapleOpInfoMap = operatorInfoMap
  
  mapleBindInfoMap :: BindInfoMap
  mapleBindInfoMap = operatorBindInfoMap
  
  mapleOpInfoNameMap :: OpInfoNameMap
  mapleOpInfoNameMap = operatorInfoNameMap
  
  printAssignment :: String -> AssDefinition -> String
  printAssignment n (ConstDef e) = concat [n, ":= ", printExp e, ":", n, ";"]
  printAssignment n (FunDef l e) = concat [ n, ":= proc", args, printExp e
                                          , " end proc:", n, args, ";"]
      where args = concat [ "(", intercalate ", " l, ") " ]
  
  printAssignmentWithEval :: String -> AssDefinition -> String
  printAssignmentWithEval n (ConstDef e) =
  {- concat [n, ":= evalf(", printExp e, "):", n, " &+ 0", ";"]
  concat [n, ":= evalf(", printExp e, "):", n, ";"] -}
      concat [n, ":= evalf(", printExp e, "):g(", n, ")", ";"]
  printAssignmentWithEval n (FunDef l e) = concat [ n, ":= proc", args, printExp e
                                                  , " end proc:", n, args, ";"]
      where args = concat [ "(", intercalate ", " l, ") " ]
  
  printEvaluation :: EXPRESSION -> String
  printEvaluation e = printExp e ++ ";"
  
  {- printEvaluationWithEval :: EXPRESSION -> String
  printEvaluationWithEval e = "evalf(" ++ printExp e ++ ");" -}
  
  printLookup :: String -> String
  printLookup n = n ++ ";"
  
  {-
  The evalf makes the decision much faster. As we verify the result formally
  this should not be problematic in a formal context!
  
  
  In the following context "is" gives up if we do not use "evalf":
  
  x2 := cos(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10))
        + cos(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10)))
        / sin(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10))));
  is(abs(x2)<1.0e-4);
  -}
  printBooleanExpr :: EXPRESSION -> String
  printBooleanExpr e = concat [ "is(evalf(", printExp e, "));" ]
  
  {- The evalf is mandatory if we use the if-statement for encoding
  
  -- | As maple does not evaluate boolean expressions we encode them in an
  -- if-stmt and transform the numeric response back.
  printBooleanExpr :: EXPRESSION -> String
  printBooleanExpr e = concat [ "if evalf("
                              , printExp e, ") then 1 else 0 fi;"
                              ]
  
  -}
  
  {- ----------------------------------------------------------------------
  Methods for Maple 'AssignmentStore' Interface
  ---------------------------------------------------------------------- -}
  
  {- | Evaluate the given String as maple expression and
  parse the result to an maybe expression. If the boolean flag is false
  the result will not be parsed. -}
  evalMapleString' :: Bool -- ^ Use parser
                  -> String -- ^ the maple command to evaluate
                  -> MapleIO (Maybe EXPRESSION)
  evalMapleString' b s = do
    -- 0.09 seconds is a critical value for the accepted response time of Maple
    mit <- get
    res <- lift $ wrapCommand $ PC.call (getChannelTimeout mit) s
    return $ if b
             -- then parseExpression mapleOpInfoMap $ trimLeft $ removeOutputComments res
             then parseExpression (mapleOpInfoMap, mapleBindInfoMap) $ trimLeft res
             else Nothing
  
  -- | Evaluate the given String as maple expression and skip the result
  sendMapleString :: String -- ^ the maple command to evaluate
                  -> MapleIO ()
  sendMapleString s = evalMapleString' False s >> return ()
  
  {- | Evaluate the given String as maple expression and
  parse the result back to an expression. -}
  evalMapleString :: String -- ^ an error message for the failure case
                  -> String -- ^ the maple command to evaluate
                  -> MapleIO EXPRESSION
  evalMapleString msg s = do
    mE <- evalMapleString' True s
    case mE of
      Just e -> return e
      _ -> throwError $ ASError InterfaceError msg
  
  mapleAssignDirect :: String -> AssDefinition -> MapleIO EXPRESSION
  mapleAssignDirect n def = do
    sm <- getSymbolicMode
    let f = if sm then printAssignment else printAssignmentWithEval
        msg = "mapleAssignDirect: unparseable result for assignment of "
              ++ (show (pretty n) <+> pretty def)
    prettyInfo3 $ mplPretty [(n, def)]
    evalMapleString msg $ f n def
  
  mapleAssignsDirect :: [(String, AssDefinition)] -> MapleIO ()
  mapleAssignsDirect =
      sendMapleString . unlines . map (uncurry printAssignment)
  
  
  mapleLookupDirect :: String -> MapleIO EXPRESSION
  mapleLookupDirect n = evalMapleString msg $ printLookup n where
      msg = "mapleLookupDirect: unparseable result for lookup of " ++ n
  
  
  mapleEvalDirect :: EXPRESSION -> MapleIO EXPRESSION
  mapleEvalDirect e = do
  -- b <- getSymbolicMode
    let -- f = if b then printEvaluation else printEvaluationWithEval
        msg = "mapleEvalDirect: unparseable result for evaluation of "
              ++ show (pretty e)
    evalMapleString msg $ printEvaluation e -- f e
  
  mapleCheck :: EXPRESSION -> MapleIO Bool
  mapleCheck e = do
    let msg = "mapleCheck: unparseable result for evaluation of "
              ++ show (pretty e)
    eB <- genCheck (evalMapleString msg . printBooleanExpr) e
    case eB of
      Right b -> return b
      Left s ->
          throwError $ ASError CASError $
                     concat [ "mapleCheck: CAS error for expression "
                            , show e, "\n", s ]
  
  {- ----------------------------------------------------------------------
  The Communication Interface
  ---------------------------------------------------------------------- -}
  
  
  wrapCommand :: IOS PC.CommandState a -> IOS MITrans a
  wrapCommand ios = do
    r <- get
    let map' x = setMI x r
    stmap map' getMI ios
  
  -- | A direct way to communicate with Maple
  mapleDirect :: Bool -> MITrans -> String -> IO String
  mapleDirect b mit s = do
    (res, _) <- runIOS (getMI mit) $ PC.call (getChannelTimeout mit) s
    return $ if b then removeOutputComments res else res
  
  -- | init the maple communication
  mapleInit :: AssignmentDepGraph ()
            -> Int -- ^ Verbosity level
            -> PC.DTime -- ^ timeout for response
            -> IO MITrans
  mapleInit adg v to = do
    rc <- lookupMapleShellCmd
    libpath <- getEnvDef "HETS_MAPLELIB"
               $ error "mapleInit: Environment variable HETS_MAPLELIB not set."
    case rc of
      Left maplecmd -> do
              cs <- PC.start (maplecmd ++ " -q") v
                    $ Just PC.defaultConfig { PC.startTimeout = 3 }
              (_, cs') <- runIOS cs $ PC.call 0.5
                          $ concat [ "interface(prettyprint=0); Digits := 10;"
                                   , "libname := \"", libpath, "\", libname;" ]
              return $ initASState (cs', to) mapleOpInfoMap adg v
      _ -> error "Could not find maple shell command!"
  
  
  -- | Loads a maple module such as intpakX or intCompare
  mapleLoadModule :: MITrans -> String -> IO String
  mapleLoadModule rit s =
      fmap fst $ runIOS (getMI rit) (PC.call 0.5 $ "with(" ++ s ++ ");")
  
  
  mapleExit :: MITrans -> IO (Maybe ExitCode)
  mapleExit mit = do
    (ec, _) <- runIOS (getMI mit) $ PC.close $ Just "quit;"
    return ec
  
  execWithMaple :: MITrans -> MapleIO a -> IO (MITrans, a)
  execWithMaple mit m = do
    let err s = error $ "execWithMaple: " ++ s
    (res, mit') <- runIOS mit $ runErrorT m
    case res of
      Left s' -> err $ asErrorMsg s'
      Right x -> return (mit', x)
  
  runWithMaple :: AssignmentDepGraph () -> Int -- ^ Verbosity level
            -> PC.DTime -- ^ timeout for response
            -> [String] -> MapleIO a
            -> IO (MITrans, a)
  runWithMaple adg i to l m = do
    mit <- mapleInit adg i to
    mapM_ (mapleLoadModule mit) l
  
    -- wraps an interval around the number
    let debugFun = "g := proc(v) z:=abs(Float(v,1-Digits)):[v-z, v+z] end;"
    runIOS (getMI mit) $ PC.call 0.3 debugFun
  
    execWithMaple mit m
  
  {- ----------------------------------------------------------------------
  The Maple system
  ---------------------------------------------------------------------- -}
  
  -- | Left String is success, Right String is failure
  lookupMapleShellCmd :: IO (Either String String)
  lookupMapleShellCmd = do
    cmd <- getEnvDef "HETS_MAPLE" "maple"
    -- check that prog exists
    noProg <- missingExecutableInPath cmd
    let f = if noProg then Right else Left
    return $ f cmd
  
  -- | Removes lines starting with ">"
  removeOutputComments :: String -> String
  removeOutputComments =
      filter (/= '\\') . concat . filter (not . isPrefixOf ">") . lines
  
  {- Some problems with the maximization in Maple:
  
  > Maximize(-x^6+t*x^3-3, {t >= -1000, t <= 1000}, x=-2..0);
  Error, (in Optimization:-NLPSolve) no improved point could be found
  > Maximize(-x^t*x^3-3, {t >= -1000, t <= 1000}, x=-2..0);
  Error, (in Optimization:-NLPSolve) complex value encountered
  
  
  -- works better:
  rhs(maximize(-(tan(x)-1/12)^2 -1, x=-1..1, location)[2,1,1,1]);
  -}
  