module Agda.Compiler.MAlonzo.Misc where
import Control.Monad.State
import Data.Generics
import Data.Generics.Aliases
import Data.List as L
import Data.Map as M
import Data.Set as S
import Data.Maybe
import Data.Function
import Language.Haskell.Syntax
import System.IO
import System.Time
import Agda.Interaction.Imports
import Agda.Interaction.Monad
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 Module
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 -> HsName
ihname s i = HsIdent $ s ++ show i
unqhname :: String -> QName -> HsName
unqhname s q | ("d", "main") == (s, show(qnameName q)) = HsIdent "main"
| otherwise = ihname s (idnum $ nameId $ qnameName $ q)
where idnum (NameId x _) = fromIntegral x
tlmodOf :: ModuleName -> TCM Module
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'; _ -> mazerror$ "tlmodOf: "++show m
xqual :: QName -> HsName -> TCM HsQName
xqual q n = do m1 <- tlmname (qnameModule q)
m2 <- curMName
if m1 == m2 then return (UnQual n)
else addImport m1 >> return (Qual (mazMod m1) n)
xhqn :: String -> QName -> TCM HsQName
xhqn s q = xqual q (unqhname s q)
conhqn :: QName -> TCM HsQName
conhqn q = do
cq <- canonicalName q
defn <- theDef <$> getConstInfo cq
case defn of Constructor{conHsCode = Just (_, hs)} -> return $ UnQual $ HsIdent hs
_ -> xhqn "C" cq
bltQual :: String -> String -> TCM HsQName
bltQual b s = do (Def q _) <- getBuiltin b; xqual q (HsIdent s)
dsubname q i | i == 0 = unqhname "d" q
| otherwise = unqhname ("d_" ++ show i ++ "_") q
hsVarUQ :: HsName -> HsExp
hsVarUQ = HsVar . UnQual
mazstr = "MAlonzo"
mazName = mkName_ dummy mazstr
mazMod' s = Module $ mazstr ++ "." ++ s
mazMod :: ModuleName -> Module
mazMod = mazMod' . show
mazerror msg = error $ mazstr ++ ": " ++ msg
mazCoerce = HsVar $ Qual unsafeCoerceMod (HsIdent "unsafeCoerce")
rtmMod = mazMod' "Runtime"
rtmQual = UnQual . HsIdent
rtmVar = HsVar . rtmQual
rtmError s = rtmVar "error" `HsApp`
(HsLit $ HsString $ "MAlonzo Runtime Error: " ++ s)
unsafeCoerceMod = Module "Unsafe.Coerce"
fakeD :: HsName -> String -> HsDecl
fakeD v s = HsFunBind [HsMatch dummy v []
(HsUnGuardedRhs $ hsVarUQ $ HsIdent $ s) [] ]
fakeDS :: String -> String -> HsDecl
fakeDS = fakeD . HsIdent
fakeDQ :: QName -> String -> HsDecl
fakeDQ = fakeD . unqhname "d"
fakeType :: String -> HsQualType
fakeType = HsQualType [] . HsTyVar . HsIdent
fakeExp :: String -> HsExp
fakeExp = HsVar . UnQual . HsIdent
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)