module HERMIT.Shell.Interpreter
(
Interp
, interp
, interpM
, interpEM
, interpExprH
, exprToDyns
) where
#if MIN_VERSION_mtl(2,2,1)
import Control.Monad.Except
#else
import Control.Monad.Error
#endif
import Control.Monad.State
import Data.Char
import Data.Dynamic
import qualified Data.Map as M
import HERMIT.External
import HERMIT.Kure
import HERMIT.Monad
import HERMIT.Name
import HERMIT.Parser
import HERMIT.Dictionary.Navigation
import HERMIT.Dictionary.Rules
import HERMIT.Shell.Dictionary
import HERMIT.Shell.Types
data Interp :: (* -> *) -> * -> * where
Interp :: Typeable b => (b -> ExprH -> m a) -> Interp m a
interp :: (Monad m, Typeable b) => (b -> a) -> Interp m a
interp f = Interp (const . return . f)
interpM :: (CLMonad m, Typeable b) => (b -> m a) -> Interp m a
interpM f = Interp (const . f)
interpEM :: (CLMonad m, Typeable b) => (b -> ExprH -> m a) -> Interp m a
interpEM = Interp
instance Monad m => Functor (Interp m) where
fmap :: (a -> b) -> Interp m a -> Interp m b
fmap f (Interp g) = Interp (\ e -> liftM f . g e)
interpExprH :: CLMonad m => [Interp m b] -> ExprH -> m b
interpExprH interps e = exprToDyns e >>= runInterp e interps
runInterp :: forall m b. CLMonad m => ExprH -> [Interp m b] -> [Dynamic] -> m b
runInterp e interps dyns = case [f a e :: m b | Interp f <- interps, Just a <- map fromDynamic dyns] of
[] -> fail $ "Does not type-check: " ++ unparseExprH e ++ "\n"
comp:_ -> comp
exprToDyns :: MonadState CommandLineState m => ExprH -> m [Dynamic]
exprToDyns = exprToDyns' False
fromDynList :: [[Dynamic]] -> [[Dynamic]]
fromDynList [] = [[]]
fromDynList (hs:dynss) = [ h:t | h <- hs, t <- fromDynList dynss ]
toBoxedList :: (Extern a, Typeable b) => [[Dynamic]] -> ([a] -> b) -> [Dynamic]
toBoxedList dyns boxCon = [ toDyn $ boxCon (map unbox l) | dl <- dyns, Just l <- [mapM fromDynamic dl] ]
exprToDyns' :: MonadState CommandLineState m => Bool -> ExprH -> m [Dynamic]
exprToDyns' _ (SrcName str) = do
let hn = parseName str
return [ toDyn hn, toDyn (BindingName hn), toDyn (OccurrenceName hn), toDyn (RhsOfName hn), toDyn (StringBox str) ]
exprToDyns' _ (CoreH str) = return [ toDyn $ CoreString str ]
exprToDyns' _ (ListH exprs) = do
dyns <- liftM fromDynList $ mapM (exprToDyns' True) exprs
return $ toBoxedList dyns StringListBox
++ toBoxedList dyns (PathBox . pathToSnocPath)
++ toBoxedList dyns (TransformCorePathBox . return . pathToSnocPath)
++ toBoxedList dyns IntListBox
++ toBoxedList dyns OccurrenceNameListBox
++ toBoxedList dyns RewriteCoreListBox
++ toBoxedList dyns RuleNameListBox
exprToDyns' rhs (CmdName str)
| all isDigit str = do
let i = read str
return [
toDyn $ IntBox i
, toDyn $ TransformCorePathBox (deprecatedIntToPathT i)
]
| otherwise = do
dict <- gets (mkDictionary . cl_externals)
case M.lookup str dict of
Just dyns -> do
dyns' <- mapM provideState dyns
return $ if rhs then toDyn (StringBox str) : dyns' else dyns'
Nothing | rhs -> let f = maybe id ((:) . toDyn) $ string2considerable str
in return $ f [ toDyn $ StringBox str
, toDyn $ LemmaName str
, toDyn $ RememberedName str
, toDyn $ RuleName str]
| otherwise -> fail $ "User error, unrecognised HERMIT command: " ++ show str
exprToDyns' _ (AppH e1 e2) = liftM2 dynCrossApply (exprToDyns' False e1) (exprToDyns' True e2)
provideState :: MonadState CommandLineState m => Dynamic -> m Dynamic
provideState dyn = do
st <- get
case dynApply dyn (toDyn $ box st) of
Just d -> return d
Nothing -> return dyn
dynCrossApply :: [Dynamic] -> [Dynamic] -> [Dynamic]
dynCrossApply fs xs = [ r | f <- fs, x <- xs, Just r <- return (dynApply f x)]