module Agda.Compiler.MAlonzo.Misc where
import Data.Char
import qualified Agda.Utils.Haskell.Syntax as HS
import Agda.Compiler.Common
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.Utils.Pretty
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"))
hsTypedDouble :: Real a => a -> HS.Exp
hsTypedDouble n = HS.ExpTypeSig (HS.Lit (HS.Frac $ toRational n)) (HS.TyCon (hsName "Double"))
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 == '\''