content: {- |
  Module      :  ./CSL/EvalSpec.hs
  Description :  EvalSpec program
  Copyright   :  (c) Ewaryst Schulz, DFKI Bremen 2010
  License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
  
  Maintainer  :  ewaryst.schulz@dfki.de
  Stability   :  experimental
  Portability :  non-portable (via imports)
  
  Program for evaluating EnCL specifications
  -}
  module Main (main, runMain) where
  
  import System.Environment
  import System.Console.GetOpt
  
  import qualified Interfaces.Process as PC
  import CSL.AnEvenTool (evalWithVerification, CAS (..), CASState (..), runTool)
  import Common.Utils
  
  import Data.Bits
  import Data.Maybe
  import Data.List
  
  import Control.Monad
  
  main :: IO ()
  main = getArgs >>= runMain True >> putStr ""
  -- main = runTool >> return ()
  
  runMain :: Bool -> [String] -> IO (Maybe CASState)
  runMain cl args =
      case processArgs args of
        Left msg -> do
          putStrLn $ "Evaluation: " ++ msg ++ "\n\n" ++ esUsage
          return Nothing
  
        Right st -> liftM Just $ runProg cl st
  
  runProg :: Bool -> ProgSettings -> IO CASState
  runProg cl st =
    evalWithVerification cl
                         (cas st)
                         (logFile st)
                         (connectionName st)
                         (symbolicmode st)
                         (debugmode st)
                         (timeout st)
                         (verbosity st)
                         (lib st)
                         (spec st)
  
  -- ----------------------- Input Arguments -------------------------
  
  processArgs :: [String] -> Either String ProgSettings
  processArgs args =
      let (flags, noopts, unrecopts, errs) =
           getOpt' (ReturnInOrder PFLib) options args
          msgl = checkFlags flags
          f str (l, s) = if null l then str else str ++ "\n" ++ s ++ unlines l
          msg = foldl f ""
                [ (noopts, "non-handled extra arguments encountered ")
                , (unrecopts, "unrecognized flags encountered ")
                , (errs, "")
                , (msgl, "")
                ]
      in if null msg then Right $ getSettings flags else Left msg
  
  esHeader :: String
  esHeader = unlines
             [ "Usage: evalspec [OPTION...] [file]"
                    , ""
                    , "evalspec /tmp/f.dol -sFlangeComplete"
                    , ""
                    ]
  
  esUsage :: String
  esUsage = usageInfo esHeader options
  
  {- | 'options' describes all available options and is used to generate usage
  information -}
  options :: [OptDescr ProgFlag]
   -- Option [Char] [String] (ArgDescr a) String
  options = map f
            [ ( "lib", "Path to the hets file", ReqArg PFLib "FILE")
            , ( "spec"
              , "Name of specification importing both, " ++
                "the pattern and the design specification"
              , ReqArg PFSpec "SPECNAME")
            , ( "CAS"
              , "Name of the computer algebra system to " ++
                "carry out the computations"
              , ReqArg (PFCAS . fromMaybe (error "Unknown CAS") . readMaybe)
                           "Mathematica or Maple")
            , ( "Logfile"
              , "Path to a logfile which will contain low " ++
                "level CAS connection information"
              , ReqArg PFLogFile "FILE")
            , ( "connection"
              , "A connection name as given e.g. to the MathLink server"
              , ReqArg PFConnection "String")
            , ( "timeout"
              , "Timeout for communication with external CAS " ++
                "system in deziseconds (tenth of a second)"
              , ReqArg (PFTimeout . fromRational
                        . fromMaybe (error "Could not parse timeout")
                        . (readMaybe :: String -> Maybe Rational)
                        . (++ "%10")) "1-1000")
            , ( "verbosity"
              , "A value from 0=quiet to 4=print out all " ++
                "information during processing"
              , ReqArg (PFVerbosity . read) "0-4")
            , ( "quiet", "Equal to -v0", NoArg PFQuiet)
            , ( "Symbolic", "Enables symbolic evaluation mode",
                NoArg (PFSymbolic True))
            , ( "debug", "Enables debug mode", NoArg (PFDebug True))
            ] where
      f (fs, descr, arg) = Option [head fs] [fs] arg descr
  
  checkFlags :: [ProgFlag] -> [String]
  checkFlags = g . mapAccumL f (0 :: Int) where
      f i (PFLib _) = (setBit i 0, ())
      f i (PFSpec _) = (setBit i 1, ())
      f i _ = (i, ())
      g (i, _) = mapMaybe (h i) [ (0, "lib")
                                , (1, "spec") ]
      h i (j, s)
        | testBit i j = Nothing
        | otherwise = Just $ s ++ " argument is missing"
  
  data ProgSettings =
      ProgSettings
      { lib :: String
      , spec :: String
      , cas :: CAS
      , logFile :: Maybe FilePath
      , connectionName :: Maybe String
      , timeout :: PC.DTime
      , verbosity :: Int
      , debugmode :: Bool
      , symbolicmode :: Bool
      }
  
  
  defaultSettings :: ProgSettings
  defaultSettings = ProgSettings
                    { lib = error "uninitialized settings"
                    , spec = error "uninitialized settings"
                    , cas = Maple
                    , timeout = 1
                    , verbosity = 4
                    , debugmode = False
                    , symbolicmode = False
                    , logFile = Nothing
                    , connectionName = Nothing
                    }
  
  data ProgFlag =
      PFLib String
          | PFSpec String
          | PFTimeout PC.DTime
          | PFVerbosity Int
          | PFLogFile FilePath
          | PFConnection String
          | PFCAS CAS
          | PFQuiet
          | PFDebug Bool
          | PFSymbolic Bool
  
  makeSettings :: ProgSettings -> ProgFlag -> ProgSettings
  makeSettings settings flg =
      case flg of
        PFLib s -> settings { lib = s }
        PFSpec s -> settings { spec = s }
        PFVerbosity i -> settings { verbosity = i }
        PFQuiet -> settings { verbosity = 0 }
        PFTimeout t -> settings { timeout = t }
        PFDebug b -> settings { debugmode = b }
        PFSymbolic b -> settings { symbolicmode = b }
        PFLogFile fp -> settings { logFile = Just fp }
        PFConnection n -> settings { connectionName = Just n }
        PFCAS c -> settings { cas = c }
  
  getSettings :: [ProgFlag] -> ProgSettings
  getSettings = foldl makeSettings defaultSettings
  