module Agda.Compiler.MAlonzo.Misc where
import Control.Monad.State
import Data.List as List
import Data.Map as Map
import Data.Set as Set
import Data.Function
import qualified Language.Haskell.Exts.Syntax as HS
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.Utils.Monad
#include "../../undefined.h"
import Agda.Utils.Impossible
setInterface :: Interface -> TCM ()
setInterface i = modify $ \s -> s
{ stImportedModules = Set.empty
, stCurrentModule = Just $ iModuleName i
}
curIF :: TCM Interface
curIF = do
mName <- stCurrentModule <$> get
case mName of
Nothing -> __IMPOSSIBLE__
Just name -> do
mm <- getVisitedModule (toTopLevelModuleName name)
case mm of
Nothing -> __IMPOSSIBLE__
Just mi -> return $ miInterface mi
curSig :: TCM Signature
curSig = iSignature <$> curIF
curMName :: TCM ModuleName
curMName = sigMName <$> curSig
curHsMod :: TCM HS.ModuleName
curHsMod = mazMod <$> curMName
curDefs :: TCM Definitions
curDefs = sigDefinitions <$> curSig
sigMName :: Signature -> ModuleName
sigMName sig = case Map.keys (sigSections sig) of
[] -> __IMPOSSIBLE__
m : _ -> m
ihname :: String -> Nat -> HS.Name
ihname s i = HS.Ident $ s ++ show i
unqhname :: String -> QName -> HS.Name
unqhname s q = ihname s (idnum $ nameId $ qnameName $ q)
where idnum (NameId x _) = fromIntegral x
tlmodOf :: ModuleName -> TCM HS.ModuleName
tlmodOf = fmap mazMod . tlmname
tlmname :: ModuleName -> TCM ModuleName
tlmname m = do
visited <- List.map (iModuleName . miInterface) . Map.elems <$>
getVisitedModules
let ms = sortBy (compare `on` (length . mnameToList)) $
List.filter (\ m' -> mnameToList m' `isPrefixOf` mnameToList m) visited
case ms of
(m' : _) -> return m'
[] -> curMName
xqual :: QName -> HS.Name -> TCM HS.QName
xqual q n = do m1 <- tlmname (qnameModule q)
m2 <- curMName
if m1 == m2 then return (HS.UnQual n)
else addImport m1 >> return (HS.Qual (mazMod m1) n)
xhqn :: String -> QName -> TCM HS.QName
xhqn s q = xqual q (unqhname s q)
conhqn :: QName -> TCM HS.QName
conhqn q = do
cq <- canonicalName q
def <- getConstInfo cq
hsr <- compiledHaskell . defCompiledRep <$> getConstInfo cq
case (compiledHaskell (defCompiledRep def), theDef def) of
(Just (HsDefn _ hs), Constructor{}) -> return $ HS.UnQual $ HS.Ident hs
_ -> xhqn "C" cq
bltQual :: String -> String -> TCM HS.QName
bltQual b s = do
Def q _ <- ignoreSharing <$> getBuiltin b
xqual q (HS.Ident s)
dsubname q i | i == 0 = unqhname "d" q
| otherwise = unqhname ("d_" ++ show i ++ "_") q
hsVarUQ :: HS.Name -> HS.Exp
hsVarUQ = HS.Var . HS.UnQual
mazstr = "MAlonzo.Code"
mazName = mkName_ dummy mazstr
mazMod' s = HS.ModuleName $ mazstr ++ "." ++ s
mazMod :: ModuleName -> HS.ModuleName
mazMod = mazMod' . show
mazerror msg = error $ mazstr ++ ": " ++ msg
mazCoerce = HS.Var $ HS.Qual mazRTE $ HS.Ident "mazCoerce"
mazIncompleteMatch = HS.Var $ HS.Qual mazRTE $ HS.Ident "mazIncompleteMatch"
rtmIncompleteMatch :: QName -> HS.Exp
rtmIncompleteMatch q = mazIncompleteMatch `HS.App` hsVarUQ (unqhname "name" q)
mazRTE :: HS.ModuleName
mazRTE = HS.ModuleName "MAlonzo.RTE"
rtmMod = mazMod' "Runtime"
rtmQual = HS.UnQual . HS.Ident
rtmVar = HS.Var . rtmQual
rtmError s = rtmVar "error" `HS.App`
(HS.Lit $ HS.String $ "MAlonzo Runtime Error: " ++ s)
unsafeCoerceMod = HS.ModuleName "Unsafe.Coerce"
fakeD :: HS.Name -> String -> HS.Decl
fakeD v s = HS.FunBind [ HS.Match dummy v [] Nothing
(HS.UnGuardedRhs $ hsVarUQ $ HS.Ident $ s)
(HS.BDecls [])
]
fakeDS :: String -> String -> HS.Decl
fakeDS = fakeD . HS.Ident
fakeDQ :: QName -> String -> HS.Decl
fakeDQ = fakeD . unqhname "d"
fakeType :: String -> HS.Type
fakeType = HS.TyVar . HS.Ident
fakeExp :: String -> HS.Exp
fakeExp = HS.Var . HS.UnQual . HS.Ident
dummy :: a
dummy = error "MAlonzo : this dummy value should not have been eval'ed."