Interpreter.hs revision 7af4df794a0e0f0cb927bd9371556ad098308983
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek{-# LANGUAGE FunctionalDependencies, FlexibleInstances, FlexibleContexts
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , UndecidableInstances, OverlappingInstances, MultiParamTypeClasses
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , TypeSynonymInstances, ExistentialQuantification #-}
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekModule : $Header$
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekDescription : Interpreter for CPL programs
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekLicense : GPLv2 or higher, see LICENSE.txt
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekMaintainer : Ewaryst.Schulz@dfki.de
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekStability : experimental
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekPortability : non-portable (various glasgow extensions)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekDefines an interface for Calculators used to evaluate CPL programs
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek ( AssignmentStore(..)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , evaluateList
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , initWithOpMap
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , lookupOrInsert
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , translateArgVars
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , translateExpr
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , translateExprWithVars
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , revtranslateExpr
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , revtranslateExprWithVars
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , convergenceTerm
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , stepwiseSafe
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , interactiveStepper
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , readEvalPrintLoop
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , EvalAtom(..)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , prettyEvalAtom
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , asErrorMsg
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , throwASError
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , ASState(..)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , initASState
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , withLogFile
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , ASError(..)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , ErrorSource(..)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , StepDebugger(..)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , SymbolicEvaluator(..)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , MessagePrinter(..)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , verbMsgASSt
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , verbMsgASStLn
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , prettyInfo
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , prettyInfo3
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekimport Control.Monad.Error (Error(..), MonadError (..))
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekimport qualified Data.Set as Set
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekimport qualified Data.Map as Map
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekimport qualified Data.IntMap as IMap
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekimport Data.List (mapAccumL)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekimport Prelude hiding (lookup)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- ----------------------------------------------------------------------
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- * Evaluator
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- ----------------------------------------------------------------------
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- ** some general lifted instances
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- TODO: outsource them
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekinstance (MonadState s m, MonadTrans t, Monad (t m)) => MonadState s (t m) where
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek get = lift get
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek put = lift . put
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekinstance (MonadIO m, MonadTrans t, Monad (t m)) => MonadIO (t m) where
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek liftIO = lift . liftIO
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekinstance (MonadResult m, MonadTrans t, Monad (t m)) => MonadResult (t m) where
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek liftR = lift . liftR
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- ** Some utility classes for abstraction of concrete realizations
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- | Abstraction from lists, sets, etc. for some simple operations
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekclass SimpleMember a b | a -> b where
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek member :: b -> a -> Bool
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek count :: a -> Int
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek toList :: a -> [b]
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- ** Abstraction wrapper for utility classes
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekdata SMem b = forall a. SimpleMember a b => SMem a
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- ** Instances for abstraction wrapper
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekinstance SimpleMember (SMem b) b where
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek member x (SMem a) = member x a
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek count (SMem a) = count a
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek toList (SMem a) = toList a
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekdata ASState a =
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek { getBMap :: BMap
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , getConnectInfo :: a
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , depGraph :: AssignmentDepGraph ()
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , debugMode :: Bool
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , symbolicMode :: Bool
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , verbosity :: Int
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , vericondOut :: Maybe Handle
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , logOut :: Handle
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , printcount :: Int
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekinitASState :: a -> OpInfoMap -> AssignmentDepGraph () -> Int -> ASState a
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekinitASState ci oim adg v =
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek ASState { getBMap = initWithOpMap oim
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , getConnectInfo = ci
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , depGraph = adg
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , debugMode = False
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , symbolicMode = False
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , verbosity = v
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , vericondOut = Nothing
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , logOut = stdout
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , printcount = 0
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- | Prints a message dependent on the verbosity level
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekverbMsgASSt :: (MonadState (ASState a) as, MonadIO as) => Int -> String -> as ()
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekverbMsgASSt lvl msg = do
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek hdl <- gets logOut
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek v <- gets verbosity
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek liftIO $ verbMsg hdl v lvl msg
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- | Prints a message dependent on the verbosity level
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekverbMsgASStLn :: (MonadState (ASState a) as, MonadIO as) =>
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek Int -> String -> as ()
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekverbMsgASStLn lvl msg = do
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek hdl <- gets logOut
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek v <- gets verbosity
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek liftIO $ verbMsgLn hdl v lvl msg
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekprettyInfo3 :: (MonadState (ASState a) as, MonadIO as) => Doc -> as ()
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekprettyInfo3 = prettyInfoN 3
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekprettyInfo :: (MonadState (ASState a) as, MonadIO as) => Doc -> as ()
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekprettyInfo = prettyInfoN 2
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekprettyInfoN :: (MonadState (ASState a) as, MonadIO as) => Int -> Doc -> as ()
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekprettyInfoN n d = do
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek let mf ass = ass { printcount = printcount ass + 1 }
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek gets printcount >>= verbMsgASSt n . show
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek verbMsgASSt n ": "
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek verbMsgASStLn n (show d)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekwithLogFile :: (MonadState (ASState a) as, MonadIO as) =>
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek FilePath -> as b -> as b
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekwithLogFile fp prog = do
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek oldHdl <- gets logOut
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek let mf hdl ass = ass { logOut = hdl }
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek newHdl <- liftIO $ openFile fp WriteMode
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek modify $ mf newHdl
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek modify $ mf oldHdl
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek liftIO $ hClose newHdl
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekinstance Functor ASState where
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek fmap f s = s { getConnectInfo = f $ getConnectInfo s }
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- ** AssignmentStore
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- | Calculation interface, bundles the evaluation engine and the
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- assignment store
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekclass (Monad m) => AssignmentStore m where
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek assign :: ConstantName -> AssDefinition -> m EXPRESSION
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek assigns :: [(ConstantName, AssDefinition)] -> m ()
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek assigns = mapM_ $ uncurry assign
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek lookup :: ConstantName -> m (Maybe EXPRESSION)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek names :: m (SMem ConstantName)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek eval :: EXPRESSION -> m EXPRESSION
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek evalRaw :: String -> m String
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek check :: EXPRESSION -> m Bool
9797aa5907191cef5db8279e20ec75fd0abbe980Jakub Hrozek values :: m [(ConstantName, EXPRESSION)]
10c07e188323a2f9824b5e34379f3b1a9b37759eJakub Hrozek values = let f x = do
10c07e188323a2f9824b5e34379f3b1a9b37759eJakub Hrozek v <- lookup x
a299f900981343904d7c9c5d148e30b8e0b2c460Jakub Hrozek return (x, fromJust v)
a299f900981343904d7c9c5d148e30b8e0b2c460Jakub Hrozek in names >>= mapM f . toList
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek getUndefinedConstants :: EXPRESSION -> m (Set.Set ConstantName)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek getUndefinedConstants =
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek error "AssignmentStore: Unimplemented getUndefinedConstants"
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek genNewKey :: m Int
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek getDepGraph :: m (AssignmentDepGraph ())
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek updateConstant :: ConstantName -> AssDefinition -> m ()
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekinstance AssignmentStore m => AssignmentStore (StateT s m) where
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek assign s = lift . assign s
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek assigns = lift . assigns
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek lookup = lift . lookup
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek names = lift names
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek eval = lift . eval
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek evalRaw = lift . evalRaw
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek check = lift . check
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek values = lift values
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek getUndefinedConstants = lift . getUndefinedConstants
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek genNewKey = lift genNewKey
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek getDepGraph = lift getDepGraph
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek updateConstant c = lift . updateConstant c
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- ** AssignmentStore Extensions
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekclass AssignmentStore m => StepDebugger m where
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek setDebugMode :: Bool -> m ()
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek getDebugMode :: m Bool
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekclass AssignmentStore m => SymbolicEvaluator m where
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek setSymbolicMode :: Bool -> m ()
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek getSymbolicMode :: m Bool
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekclass AssignmentStore m => MessagePrinter m where
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek printMessage :: String -> m ()
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek-- ** Error handling
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekdata ErrorSource = CASError | UserError | InterfaceError deriving Show
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekdata ASError = ASError ErrorSource String deriving Show
bc58e1cfee742178f95922d964349d6c262f6df7Jakub HrozekasErrorMsg :: ASError -> String
bc58e1cfee742178f95922d964349d6c262f6df7Jakub HrozekasErrorMsg (ASError _ s) = s
bc58e1cfee742178f95922d964349d6c262f6df7Jakub HrozekthrowASError :: ASError -> a
bc58e1cfee742178f95922d964349d6c262f6df7Jakub HrozekthrowASError = error . asErrorMsg
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekinstance Error ASError where
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek noMsg = ASError UserError ""
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek strMsg = ASError UserError
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekinstance Pretty ErrorSource where
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek pretty es = case es of
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek CASError -> text "CAS error"
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek UserError -> text "User error"
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek InterfaceError -> text "Interface error"
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekinstance Pretty ASError where
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek pretty (ASError es s) = pretty es <> text ":" <+> text s
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek-- ** Evaluation, Debugging, Stepping
bc58e1cfee742178f95922d964349d6c262f6df7Jakub HrozekisDefined :: AssignmentStore m => ConstantName -> m Bool
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekisDefined s = liftM (member s) names
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekevaluate :: AssignmentStore m => CMD -> m ()
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekevaluate (Ass (Op (OpUser n) [] l _) e) = do
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek assign n $ mkDefinition (toArgList l) e
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekevaluate (Cond l) = do
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek cl <- filterM (check . fst) l
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek then error "evaluate: non-exhaustive conditional"
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek else evaluateList $ snd $ head cl
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekevaluate (Repeat e l) =
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek -- first run of the repeat loop
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek evaluateList l
4e5e846de22407f825fe3b4040d79606818a2419Jakub Hrozek b <- check e
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek -- repeat f until condition holds
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekevaluate (Sequence l) = evaluateList l
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekevaluate (Cmd c _) = error $ "evaluate: unsupported command " ++ c
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekevaluate a@(Ass (Op (OpId _) _ _ _) _) =
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek error $ concat [ "evaluate: predefined constants in left hand side of "
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , "assignment not allowed ", show a ]
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekevaluate a@(Ass _ _) = error $ "evaluate: unsupported assignment " ++ show a
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekevaluateList :: AssignmentStore m => [CMD] -> m ()
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekevaluateList l = forM_ l evaluate
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekdata EvalAtom = AssAtom ConstantName AssDefinition
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek | CaseAtom EXPRESSION
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek | RepeatAtom EXPRESSION (Map.Map EXPRESSION Int) EXPRESSION
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek deriving Show
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekprettyEvalAtom :: EvalAtom -> Doc
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekprettyEvalAtom (AssAtom c def) = pretty c <+> pretty def
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekprettyEvalAtom (RepeatAtom e _ _) = text "Repeat condition:" <+> pretty e
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekprettyEvalAtom (CaseAtom e) = text "Case condition:" <+> pretty e
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekinstance Pretty EvalAtom where
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek pretty = prettyEvalAtom
bc58e1cfee742178f95922d964349d6c262f6df7Jakub HrozekreadEvalPrintLoop :: (MonadIO m, AssignmentStore m) =>
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek Handle -- ^ Input handle
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek -> Handle -- ^ Output handle
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek -> String -- ^ Command prompt
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek -> (String -> Bool) -- ^ Exit command predicate
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekreadEvalPrintLoop inp outp cp exitWhen = do
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek s <- liftIO $ hPutStr outp cp >> hFlush outp >> hGetLine inp
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek if exitWhen s then return s
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek else evalRaw s >>= liftIO . (hPutStrLn outp)
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek >> readEvalPrintLoop inp outp cp exitWhen
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek-- | An atom evaluator for 'stepwise' which pauses at each atomic evaluation
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub HrozekinteractiveStepper :: (MonadIO m, AssignmentStore m) => m () -> EvalAtom
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub HrozekinteractiveStepper prog x = do
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek liftIO $ putStrLn $ "At step " ++ show (prettyEvalAtom x)
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek b <- evaluateAtom prog x
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek readEvalPrintLoop stdin stdout "next>" null
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek-- | The most primitive atom evaluator as expected by 'stepwise'.
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub HrozekevaluateAtom :: AssignmentStore m => m () -> EvalAtom -> m Bool
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub HrozekevaluateAtom _ (AssAtom n def) = assign n def >> return True
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub HrozekevaluateAtom _ (CaseAtom e) = check e
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub HrozekevaluateAtom prog (RepeatAtom _ _ e') = prog >> check e'
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek{- | It is assumed that the given function respects the evaluation semantics,
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek i.e., that for the assignment atom an assignment takes place and for the
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek repeat atom the passed program is evaluated and afterwards the condition is
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek checked and for the case atom the condition is checked. See 'evaluateAtom'
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek for an example.
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub HrozekstepwiseSafe :: (MonadError ASError m, MessagePrinter m) =>
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek (m () -> EvalAtom -> m Bool) -> CMD -> m (Maybe ASError)
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub HrozekstepwiseSafe f cmd = catchError (stepwise f cmd >> return Nothing) g
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek where g = return . Just
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekprintStep :: MessagePrinter m => String -> EvalAtom -> m ()
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekprintStep _ (AssAtom n def) = printMessage $ ("Evaluate Assignment: " ++)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek $ show $ pretty n <+> pretty def
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub HrozekprintStep _ (CaseAtom e) = printMessage $ ("Evaluate Case Step: " ++)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek $ show $ pretty e
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekprintStep s (RepeatAtom e _ _) = printMessage
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek $ (("Evaluate Repeat Step, " ++ s ++ ": ") ++)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek $ show $ pretty e
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekstepwise :: MessagePrinter m => (m () -> EvalAtom -> m Bool) -> CMD
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekstepwise f (Ass (Op (OpUser n) [] l _) e) = do
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek let def = mkDefinition (toArgList l) e
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek printStep "" $ AssAtom n def
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek f (return ()) $ AssAtom n def
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekstepwise _ (Cond []) = error "stepwise: non-exhaustive conditional"
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekstepwise f (Cond ((e, pl):cl)) = do
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek printStep "" $ CaseAtom e
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek b <- f (return ()) $ CaseAtom e
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek stepwise f $ if b then Sequence pl else Cond cl
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekstepwise f (Repeat e l) = do
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek -- only in the first entry of a repeat loop we need to transform the
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub Hrozek -- until expression, in all consecutive runs of the same loop we just
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek -- need to update the values of the temporarily introduced constants.
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek (m, e') <- translateConvergence e
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek let rAtom = RepeatAtom e m e'
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek printStep "entering loop" rAtom
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek reploop = do
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek -- mapM (uncurry convergenceTerm) al >>= assigns
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek mapM (uncurry convergenceTerm >=> f (return ()) . uncurry AssAtom) al
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek b <- f (stepwise f $ Sequence l) rAtom
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek unless b $ printStep "repeating loop" rAtom >> reploop
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekstepwise f (Sequence l) = mapM_ (stepwise f) l
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekstepwise _ (Cmd c l)
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek | c == "print" =
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek let p x x' = printMessage
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek $ show $ pretty x <+> text "evaluates to"
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek <+> pretty x'
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek in case l of
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek [] -> printMessage "Nothing to print"
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek [e] -> eval e >>= p e
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek _ -> mapM eval l >>= p l
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek | otherwise = error $ "stepwise: unsupported command " ++ c
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekstepwise _ a@(Ass (Op (OpId _) _ _ _) _) =
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek error $ concat [ "stepwise: predefined constants in left hand side of "
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek , "assignment not allowed ", show a ]
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekstepwise _ a@(Ass _ _) = error $ "stepwise: unsupported assignment " ++ show a
10c07e188323a2f9824b5e34379f3b1a9b37759eJakub Hrozek-- | We check if the expression contains free constants
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- (undefined in the assignment graph) and in this case we replace the
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- definition of the constant by the undefined constant.
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekconvergenceTerm :: AssignmentStore m => EXPRESSION -> Int
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek -> m (ConstantName, AssDefinition)
bc58e1cfee742178f95922d964349d6c262f6df7Jakub HrozekconvergenceTerm conve i = do
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek s <- getUndefinedConstants conve
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek let e = if Set.null s then conve else mkPredefOp OP_undef []
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek return (internalConstant i, mkDefinition [] e)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozektranslateConvergence :: AssignmentStore m =>
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek EXPRESSION -> m (Map.Map EXPRESSION Int, EXPRESSION)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozektranslateConvergence e' = f Map.empty e' where
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek f m (Op (OpId OP_convergence) [] [x, e] rg) =
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek i <- genNewKey
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek let ilf _ _ v = v
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek (mI, m') = Map.insertLookupWithKey ilf e i m
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek i' = fromMaybe i mI
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek genC = Op (OpUser $ internalConstant i') [] [] rg
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek return (m', mkPredefOp OP_reldistLe [genC, e, x])
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek f m (Op oi epl el rg) =
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek liftM (\ (m', x) -> (m', Op oi epl x rg)) $ mapAccumLM f m el
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek -- ignoring lists, see TODO in AS_BASIC_CSL
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek f m e = return (m, e)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- | Loads a dependency ordered assignment list into the store.
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekloadAS :: AssignmentStore m => [(ConstantName, AssDefinition)] -> m ()
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekloadAS = assigns . reverse
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- ----------------------------------------------------------------------
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- * Term translator
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- ----------------------------------------------------------------------
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek{- | For use for constants in the CAS namespace.
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek We only need to make sure that x<Num> is not already used in the
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek default namespace of the CAS in question. We take for all CAS the
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek same prefix, namely "x".
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekconstPrefix :: String
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekconstPrefix = "x"
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek{- | The variable prefix is used for auxiliary variables in the CAS namespace.
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek We use the prefix "v". The same remarks are valid as for 'constPrefix'.
bc58e1cfee742178f95922d964349d6c262f6df7Jakub HrozekvarPrefix :: String
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekvarPrefix = "v"
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek{- | For use for auxiliary constants in the EnCL specification
10c07e188323a2f9824b5e34379f3b1a9b37759eJakub Hrozek namespace. A dollar prefix is suitable here because this prefix is not
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek accepted by the input processor for user defined constants.
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekinternalPrefix :: String
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekinternalPrefix = "$"
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekinternalConstant :: Int -> ConstantName
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekinternalConstant i = SimpleConstant $ internalPrefix ++ show i
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- | A data structure for invertible maps, with automatic new key generation
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- and insertion at lookup
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekdata BMap = BMap { mThere :: Map.Map ConstantName Int
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , mBack :: IMap.IntMap ConstantName
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , newkey :: Int
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , opMap :: OpInfoMap
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek deriving Show
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekinstance SimpleMember BMap ConstantName where
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek member k = Map.member k . mThere
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek count = Map.size . mThere
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek toList = Map.keys . mThere
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekgenKey :: BMap -> (BMap, Int)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekgenKey bm = let i = newkey bm in (bm { newkey = i+1 }, i)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- ** Interface functions for BMap
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekempty :: BMap
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek , newkey = 1
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek , opMap = operatorInfoMap
bc58e1cfee742178f95922d964349d6c262f6df7Jakub HrozekinitWithOpMap :: OpInfoMap -> BMap
bc58e1cfee742178f95922d964349d6c262f6df7Jakub HrozekinitWithOpMap m = CSL.Interpreter.empty { opMap = m }
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek-- | The only way to also insert a value is to use lookup. One should not
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek-- insert values explicitly. Note that you don't control the inserted value.
bc58e1cfee742178f95922d964349d6c262f6df7Jakub HrozeklookupOrInsert :: BMap
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek -> ConstantName
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek -> (BMap, String)
bc58e1cfee742178f95922d964349d6c262f6df7Jakub HrozeklookupOrInsert m c =
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek let f _ _ x = x
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek nv = newkey m
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek (mNv', nm) = Map.insertLookupWithKey f c nv $ mThere m
10c07e188323a2f9824b5e34379f3b1a9b37759eJakub Hrozek in case mNv' of
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek Just nv' -> (m, bmapIntToString m nv')
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek _ -> (m { mThere = nm
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek , mBack = IMap.insert nv c $ mBack m
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek , newkey = nv + 1 }
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek , bmapIntToString m nv)
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek-- | A read-only version of 'lookupOrInsert'
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozekrolookup :: BMap
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek -> ConstantName
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek -> Maybe String
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekrolookup m c = fmap (bmapIntToString m) $ Map.lookup c $ mThere m
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekrevlookup :: BMap -> String -> (Maybe OPID)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozekrevlookup m k = case revlookupGen IMap.empty m k of
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek _ -> Nothing
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekrevlookupGen :: RevVarMap -> BMap -> String
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek -> Either (Maybe OPID) (Maybe EXPRESSION)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekrevlookupGen vm m k =
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek case bmapStringToInt m k of
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek Left i -> Left $ fmap OpUser $ IMap.lookup i $ mBack m
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek Right i -> Right $ fmap (Var . mkSimpleId) $ IMap.lookup i $ vm
9797aa5907191cef5db8279e20ec75fd0abbe980Jakub HrozekbmToList :: BMap -> [(ConstantName, String)]
9797aa5907191cef5db8279e20ec75fd0abbe980Jakub HrozekbmToList m = let prf = constPrefix
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek f (x, y) = (x, prf ++ show y)
9797aa5907191cef5db8279e20ec75fd0abbe980Jakub Hrozek in map f $ Map.toList $ mThere m
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- ** Internal functions for BMap
4a4af8e1b6a9bab7c7a34d86055a400376e3829eJakub HrozekbmapIntToString :: BMap -> Int -> String
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekbmapIntToString _ i = constPrefix ++ show i
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- | Returns the 'Int' contained in the given constant. If this constant
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- represents a user-defined constant then we return the left value, if
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- it represents a variable then we return the right value
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekbmapStringToInt :: BMap -> String -> Either Int Int
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekbmapStringToInt _ s =
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek let prf = constPrefix
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek (prf', n) = splitAt (length prf) s
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek (prf'', n') = splitAt 1 s
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek | prf == prf' = Left $ read n
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek | prf'' == varPrefix = Right $ read n'
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek | otherwise = error $ concat [ "bmapStringToInt: invalid string"
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek , " for prefix ", prf, ":", s ]
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- ** Translation functions for (generic) BMaps
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozektype VarMap = Map.Map String Int
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozektype RevVarMap = IMap.IntMap String
bc58e1cfee742178f95922d964349d6c262f6df7Jakub HrozekvarList :: [String] -> [(String, Int)]
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekvarList l = zip l [1..]
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekaddToVarMap :: VarMap -> String -> VarMap
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekaddToVarMap vm s = Map.insert s (Map.size vm + 1) vm
10c07e188323a2f9824b5e34379f3b1a9b37759eJakub HrozekrevVarList :: [String] -> [(Int, String)]
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekrevVarList l = zip [1..] l
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekvarName :: BMap -> Int -> String
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekvarName _ i = varPrefix ++ show i
10c07e188323a2f9824b5e34379f3b1a9b37759eJakub HrozektranslateArgVars :: BMap -> [String] -> [String]
10c07e188323a2f9824b5e34379f3b1a9b37759eJakub HrozektranslateArgVars m = map f . varList where
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek f (_, i) = varName m i
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub HrozektranslateExprWithVars :: [String] -> BMap -> EXPRESSION -> (BMap, EXPRESSION)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozektranslateExprWithVars = translateExprGen . Map.fromList . varList
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub HrozektranslateExpr :: BMap -> EXPRESSION -> (BMap, EXPRESSION)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozektranslateExpr = translateExprGen Map.empty
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- | Translate EXPRESSION into a CAS compatible form. Variables are translated
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek-- as constants with a namespace disjoint from that of the usual constants.
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozektranslateExprGen :: VarMap -> BMap -> EXPRESSION -> (BMap, EXPRESSION)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozektranslateExprGen vm m (Op (OpUser c) epl el rg) =
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek let (m', s) = lookupOrInsert m c
9797aa5907191cef5db8279e20ec75fd0abbe980Jakub Hrozek (m'', el') = mapAccumL (translateExprGen vm) m' el
9797aa5907191cef5db8279e20ec75fd0abbe980Jakub Hrozek in (m'', Op (OpUser $ SimpleConstant s) epl el' rg)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozektranslateExprGen vm m (Op oi epl el rg) =
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek let vm' = case lookupBindInfo operatorInfoNameMap oi $ length el of
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek foldl addToVarMap vm
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek $ toArgList $ map (el!!) $ bindingVarPos bi
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek (m', el') = mapAccumL (translateExprGen vm') m el
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek in (m', Op oi epl el' rg)
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub HrozektranslateExprGen vm m (List el rg) =
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub Hrozek let (m', el') = mapAccumL (translateExprGen vm) m el
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek in (m', List el' rg)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozektranslateExprGen vm m (Var tok) =
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek let err = error $ "translateExprGen: Variable not mapped: " ++ show tok
bc58e1cfee742178f95922d964349d6c262f6df7Jakub Hrozek i = Map.findWithDefault err (tokStr tok) vm
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek in (m, Op (OpUser $ SimpleConstant $ varName m i) [] [] nullRange)
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozektranslateExprGen _ m e = (m, e)
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub Hrozek-- | Retranslate CAS EXPRESSION back, we do not allow OPNAMEs as OpIds
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekrevtranslateExprWithVars :: [String] -> BMap -> EXPRESSION -> EXPRESSION
10c07e188323a2f9824b5e34379f3b1a9b37759eJakub HrozekrevtranslateExprWithVars = revtranslateExprGen . IMap.fromList . revVarList
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekrevtranslateExpr :: BMap -> EXPRESSION -> EXPRESSION
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub HrozekrevtranslateExpr = revtranslateExprGen IMap.empty
10c07e188323a2f9824b5e34379f3b1a9b37759eJakub HrozekrevtranslateExprGen :: RevVarMap -> BMap -> EXPRESSION -> EXPRESSION
10c07e188323a2f9824b5e34379f3b1a9b37759eJakub HrozekrevtranslateExprGen rvm m (Op (OpUser c) epl el rg) =
10c07e188323a2f9824b5e34379f3b1a9b37759eJakub Hrozek SimpleConstant s ->
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub Hrozek let el' = map (revtranslateExprGen rvm m) el
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub Hrozek in case revlookupGen rvm m s of
8df69bbc58c2f4d3f0b34be9756d9ddf24b1db6dJakub Hrozek Left (Just oi) -> Op oi epl el' rg
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub Hrozek Right (Just v) -> v
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub Hrozek _ -> error $ "revtranslateExpr: no mapping for " ++ s
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub Hrozek _ -> error $ "revtranslateExpr: elim constants on CAS side encountered "
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub HrozekrevtranslateExprGen rvm m e = mapExpr (revtranslateExprGen rvm m) e
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub Hrozek-- ** Pretty printing of BMap
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub HrozekprintMapping :: Doc -> Doc -> Doc
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub HrozekprintMapping x y = x <+> mapsto <+> y
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub HrozekprintBMap :: BMap -> Doc
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub HrozekprintBMap bm =
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub Hrozek braces $ text "BMap" $+$ md
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub Hrozek md = printMap braces vcat printMapping $ mThere bm
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub Hrozekinstance Pretty BMap where
a92f68763a57b211a1bf6b80b6dd80c4a1aa2738Jakub Hrozek pretty = printBMap