module Agda.Compiler.UHC.Pragmas.Parse
( module Agda.Compiler.UHC.Pragmas.Base
, parseCoreExpr
, coreExprToCExpr
, parseCoreData
, parseCoreConstrs
)
where
import Data.List
import qualified Data.Map as M
import Agda.TypeChecking.Monad
import Agda.Compiler.UHC.Pragmas.Base
import Agda.Compiler.UHC.MagicTypes
import Agda.Compiler.UHC.Bridge as CA
#include "undefined.h"
import Agda.Utils.Impossible
parseCoreData :: MonadTCM m => String -> m CoreType
parseCoreData dt = do
isDtMgc <- isMagicEntity getMagicTypes dt "datatype"
return $ case isDtMgc of
Nothing -> CTNormal dt
Just (dtMgc, _) -> CTMagic dtMgc
parseCoreConstrs :: MonadTCM m => CoreType -> [String] -> m [CoreConstr]
parseCoreConstrs (CTNormal dtCrNm) cs = do
constrs <- mapM parseNormalConstr cs
return $ zipWith setTag (sortBy ccOrd constrs) [0..]
where
parseNormalConstr :: MonadTCM m => String -> m CoreConstr
parseNormalConstr c
| isMagic c = typeError $
GenericError $ "Magic constructor " ++ (drop 2 $ init $ init c) ++ " can only be used for magic datatypes."
| otherwise = let dtMod = dropWhileEnd (/='.') dtCrNm
conNm = dtMod ++ c
in return $ CCNormal (mkHsName1 dtCrNm) (mkHsName1 conNm) __IMPOSSIBLE__
ccOrd :: CoreConstr -> CoreConstr -> Ordering
ccOrd (CCNormal dtNm1 ctNm1 _) (CCNormal dtNm2 ctNm2 _) | dtNm1 == dtNm2 = compare ctNm1 ctNm2
ccOrd _ _ = __IMPOSSIBLE__
parseCoreConstrs (CTMagic dtMgcNm) cs = do
mapM parseMagicConstr cs
where
(_, conMp) = getMagicTypes M.! dtMgcNm
parseMagicConstr :: MonadTCM m => String -> m CoreConstr
parseMagicConstr c
| not (isMagic c) = typeError $
GenericError $ "A magic datatype can only have magic constructors."
| otherwise = do
(Just (conMgcNm, _)) <- isMagicEntity conMp c "constructor"
return $ CCMagic dtMgcNm conMgcNm
parseCoreExpr :: String -> Either String CoreExpr
#if defined(UHC_BACKEND)
parseCoreExpr str = either Left (const $ Right str) (coreExprToCExpr str)
#else
parseCoreExpr str = Right str
#endif
coreExprToCExpr :: CoreExpr -> Either String CExpr
#if defined(UHC_BACKEND)
coreExprToCExpr str = case CA.parseExpr defaultEHCOpts str of
(Left errs) -> Left $ intercalate "\n" errs
(Right res) -> Right res
#else
coreExprToCExpr = __IMPOSSIBLE__
#endif
isMagicEntity :: MonadTCM m
=> M.Map MagicName a
-> String
-> String
-> m (Maybe (String, a))
isMagicEntity tbl xs ty | isMagic xs =
case nm `M.lookup` tbl of
Just x -> return $ Just (nm, x)
Nothing -> typeError $ GenericError $ "No magic " ++ ty ++ " with the name " ++ nm ++ " exists."
where nm = init $ init $ drop 2 xs
isMagicEntity _ _ _ | otherwise = return Nothing
isMagic :: String -> Bool
isMagic xs = "__" `isPrefixOf` xs && "__" `isSuffixOf` xs