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