{-# LANGUAGE CPP #-}
module Agda.Compiler.MAlonzo.Misc where
import Control.Monad.State (gets)
import Data.Char
import qualified Data.List as List
import Data.Map as Map
import Data.Set as Set
import Data.Function
import qualified Agda.Utils.Haskell.Syntax as HS
import Agda.Compiler.Common
import Agda.Compiler.MAlonzo.Pragmas
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
import Agda.Utils.Maybe
#include "undefined.h"
import Agda.Utils.Impossible
curHsMod :: TCM HS.ModuleName
curHsMod = mazMod <$> curMName
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 . topLevelModuleName
xqual :: QName -> HS.Name -> TCM HS.QName
xqual q n = do m1 <- topLevelModuleName (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)
hsName :: String -> HS.QName
hsName s = HS.UnQual (HS.Ident s)
conhqn :: QName -> TCM HS.QName
conhqn q = xhqn "C" =<< canonicalName q
bltQual :: String -> String -> TCM HS.QName
bltQual b s = do
Def q _ <- getBuiltin b
xqual q (HS.Ident s)
dname :: QName -> HS.Name
dname q = unqhname "d" q
duname :: QName -> HS.Name
duname q = unqhname "du" q
hsPrimOp :: String -> HS.QOp
hsPrimOp s = HS.QVarOp $ HS.UnQual $ HS.Symbol s
hsPrimOpApp :: String -> HS.Exp -> HS.Exp -> HS.Exp
hsPrimOpApp op e e1 = HS.InfixApp e (hsPrimOp op) e1
hsInt :: Integer -> HS.Exp
hsInt n = HS.Lit (HS.Int n)
hsTypedInt :: Integral a => a -> HS.Exp
hsTypedInt n = HS.ExpTypeSig (HS.Lit (HS.Int $ fromIntegral n)) (HS.TyCon (hsName "Integer"))
hsLet :: HS.Name -> HS.Exp -> HS.Exp -> HS.Exp
hsLet x e b =
HS.Let (HS.BDecls [HS.FunBind [HS.Match x [] (HS.UnGuardedRhs e) emptyBinds]]) b
hsVarUQ :: HS.Name -> HS.Exp
hsVarUQ = HS.Var . HS.UnQual
hsAppView :: HS.Exp -> [HS.Exp]
hsAppView = reverse . view
where
view (HS.App e e1) = e1 : view e
view (HS.InfixApp e1 op e2) = [e2, e1, hsOpToExp op]
view e = [e]
hsOpToExp :: HS.QOp -> HS.Exp
hsOpToExp (HS.QVarOp x) = HS.Var x
hsLambda :: [HS.Pat] -> HS.Exp -> HS.Exp
hsLambda ps (HS.Lambda ps1 e) = HS.Lambda (ps ++ ps1) e
hsLambda ps e = HS.Lambda ps e
hsMapAlt :: (HS.Exp -> HS.Exp) -> HS.Alt -> HS.Alt
hsMapAlt f (HS.Alt p rhs wh) = HS.Alt p (hsMapRHS f rhs) wh
hsMapRHS :: (HS.Exp -> HS.Exp) -> HS.Rhs -> HS.Rhs
hsMapRHS f (HS.UnGuardedRhs def) = HS.UnGuardedRhs (f def)
hsMapRHS f (HS.GuardedRhss es) = HS.GuardedRhss [ HS.GuardedRhs g (f e) | HS.GuardedRhs g e <- es ]
mazstr :: String
mazstr = "MAlonzo.Code"
mazName :: Name
mazName = mkName_ __IMPOSSIBLE__ 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
mazCoerceName :: String
mazCoerceName = "coe"
mazErasedName :: String
mazErasedName = "erased"
mazAnyTypeName :: String
mazAnyTypeName = "AgdaAny"
mazCoerce :: HS.Exp
mazCoerce = HS.Var $ HS.UnQual $ HS.Ident mazCoerceName
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)
mazUnreachableError :: HS.Exp
mazUnreachableError = HS.Var $ HS.Qual mazRTE $ HS.Ident "mazUnreachableError"
rtmUnreachableError :: HS.Exp
rtmUnreachableError = mazUnreachableError
mazAnyType :: HS.Type
mazAnyType = HS.TyCon (hsName mazAnyTypeName)
mazRTE :: HS.ModuleName
mazRTE = HS.ModuleName "MAlonzo.RTE"
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 v [] (HS.UnGuardedRhs $ fakeExp s) emptyBinds]
fakeDS :: String -> String -> HS.Decl
fakeDS = fakeD . HS.Ident
fakeDQ :: QName -> String -> HS.Decl
fakeDQ = fakeD . unqhname "d"
fakeType :: String -> HS.Type
fakeType = HS.FakeType
fakeExp :: String -> HS.Exp
fakeExp = HS.FakeExp
fakeDecl :: String -> HS.Decl
fakeDecl = HS.FakeDecl
emptyBinds :: Maybe HS.Binds
emptyBinds = Nothing
isModChar :: Char -> Bool
isModChar c =
isLower c || isUpper c || isDigit c || c == '_' || c == '\''