module Agda.Compiler.MAlonzo.Misc where
import Control.Monad.State
import Data.Generics
import Data.List as L
import Data.Map as M
import Data.Set as S
import Data.Maybe
import Data.Function
import qualified Language.Haskell.Exts.Syntax as HS
import System.IO
import System.Time
import Agda.Interaction.Imports
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.Utils.FileName
import Agda.Utils.Monad
import Agda.Utils.Pretty
import Agda.Utils.Impossible
#include "../../undefined.h"
setInterface :: Interface -> TCM ()
setInterface i = modify $ \s -> s
{ stImportedModules = S.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 M.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 | ("d", "main") == (s, show(qnameName q)) = HS.Ident "main"
| otherwise = 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
ms <- sortBy (compare `on` (length . mnameToList)) .
L.filter (flip (isPrefixOf `on` mnameToList) m) <$>
L.map (iModuleName . miInterface) . M.elems <$>
getVisitedModules
return $ case ms of (m' : _) -> m'; _ -> __IMPOSSIBLE__
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 _) <- 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."
gshow' :: Data a => a -> String
gshow' = ( \t ->
"("
++ showConstr (toConstr t)
++ concat (gmapQ ((++) " " . gshow') t)
++ ")" )
`extQ` (show :: String -> String)
`extQ` (show :: Name -> String)
`extQ` (show :: QName -> String)
`extQ` (show :: ModuleName -> String)
`extQ` (gshow' . M.toList :: M.Map QName [AbstractName] -> String)
`extQ` (gshow' . M.toList :: M.Map QName [AbstractModule] -> String)
`extQ` (gshow' . M.toList :: M.Map ModuleName Section -> String)
`extQ` (gshow' . M.toList :: M.Map QName Definition -> String)
`extQ` (gshow' . M.toList :: M.Map TermHead [Pattern] -> String)
`extQ` (gshow' . M.toList :: M.Map TermHead [Arg Pattern] -> String)
`extQ` (gshow' . M.toList :: M.Map String (Builtin String) -> String)
`extQ` (show :: Scope -> String)