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.Lens
import Agda.Utils.Monad
import Agda.Utils.Pretty
#include "undefined.h"
import Agda.Utils.Impossible
setInterface :: Interface -> TCM ()
setInterface i = do
stImportedModules .= Set.empty
stCurrentModule .= Just (iModuleName i)
curIF :: TCM Interface
curIF = do
mName <- use stCurrentModule
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
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 :: QName -> Nat -> HS.Name
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 :: String
mazstr = "MAlonzo.Code"
mazName :: Name
mazName = mkName_ dummy mazstr
mazMod' :: String -> HS.ModuleName
mazMod' s = HS.ModuleName $ mazstr ++ "." ++ s
mazMod :: ModuleName -> HS.ModuleName
mazMod = mazMod' . prettyShow
mazerror :: String -> a
mazerror msg = error $ mazstr ++ ": " ++ msg
mazCoerce :: HS.Exp
mazCoerce = HS.Var $ HS.Qual mazRTE $ HS.Ident "mazCoerce"
mazIncompleteMatch :: HS.Exp
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 :: HS.ModuleName
rtmMod = mazMod' "Runtime"
rtmQual :: String -> HS.QName
rtmQual = HS.UnQual . HS.Ident
rtmVar :: String -> HS.Exp
rtmVar = HS.Var . rtmQual
rtmError :: String -> HS.Exp
rtmError s = rtmVar "error" `HS.App`
(HS.Lit $ HS.String $ "MAlonzo Runtime Error: " ++ s)
unsafeCoerceMod :: HS.ModuleName
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."