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 :: TCM ModuleName
curHsMod = ModuleName -> ModuleName
mazMod (ModuleName -> ModuleName) -> TCMT IO ModuleName -> TCM ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ModuleName
curMName
ihname :: String -> Nat -> HS.Name
ihname :: String -> Nat -> Name
ihname s :: String
s i :: Nat
i = String -> Name
HS.Ident (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show Nat
i
unqhname :: String -> QName -> HS.Name
unqhname :: String -> QName -> Name
unqhname s :: String
s q :: QName
q = String -> Nat -> Name
ihname String
s (NameId -> Nat
forall b. Num b => NameId -> b
idnum (NameId -> Nat) -> NameId -> Nat
forall a b. (a -> b) -> a -> b
$ Name -> NameId
nameId (Name -> NameId) -> Name -> NameId
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName (QName -> Name) -> QName -> Name
forall a b. (a -> b) -> a -> b
$ QName
q)
where idnum :: NameId -> b
idnum (NameId x :: Word64
x _) = Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
x
tlmodOf :: ModuleName -> TCM HS.ModuleName
tlmodOf :: ModuleName -> TCM ModuleName
tlmodOf = (ModuleName -> ModuleName) -> TCMT IO ModuleName -> TCM ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModuleName -> ModuleName
mazMod (TCMT IO ModuleName -> TCM ModuleName)
-> (ModuleName -> TCMT IO ModuleName)
-> ModuleName
-> TCM ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> TCMT IO ModuleName
topLevelModuleName
xqual :: QName -> HS.Name -> TCM HS.QName
xqual :: QName -> Name -> TCM QName
xqual q :: QName
q n :: Name
n = do ModuleName
m1 <- ModuleName -> TCMT IO ModuleName
topLevelModuleName (QName -> ModuleName
qnameModule QName
q)
ModuleName
m2 <- TCMT IO ModuleName
curMName
if ModuleName
m1 ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
m2 then QName -> TCM QName
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> QName
HS.UnQual Name
n)
else ModuleName -> TCM ()
addImport ModuleName
m1 TCM () -> TCM QName -> TCM QName
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QName -> TCM QName
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleName -> Name -> QName
HS.Qual (ModuleName -> ModuleName
mazMod ModuleName
m1) Name
n)
xhqn :: String -> QName -> TCM HS.QName
xhqn :: String -> QName -> TCM QName
xhqn s :: String
s q :: QName
q = QName -> Name -> TCM QName
xqual QName
q (String -> QName -> Name
unqhname String
s QName
q)
hsName :: String -> HS.QName
hsName :: String -> QName
hsName s :: String
s = Name -> QName
HS.UnQual (String -> Name
HS.Ident String
s)
conhqn :: QName -> TCM HS.QName
conhqn :: QName -> TCM QName
conhqn q :: QName
q = String -> QName -> TCM QName
xhqn "C" (QName -> TCM QName) -> TCMT IO QName -> TCM QName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
q
bltQual :: String -> String -> TCM HS.QName
bltQual :: String -> String -> TCM QName
bltQual b :: String
b s :: String
s = do
Def q :: QName
q _ <- String -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getBuiltin String
b
QName -> Name -> TCM QName
xqual QName
q (String -> Name
HS.Ident String
s)
dname :: QName -> HS.Name
dname :: QName -> Name
dname q :: QName
q = String -> QName -> Name
unqhname "d" QName
q
duname :: QName -> HS.Name
duname :: QName -> Name
duname q :: QName
q = String -> QName -> Name
unqhname "du" QName
q
hsPrimOp :: String -> HS.QOp
hsPrimOp :: String -> QOp
hsPrimOp s :: String
s = QName -> QOp
HS.QVarOp (QName -> QOp) -> QName -> QOp
forall a b. (a -> b) -> a -> b
$ Name -> QName
HS.UnQual (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ String -> Name
HS.Symbol String
s
hsPrimOpApp :: String -> HS.Exp -> HS.Exp -> HS.Exp
hsPrimOpApp :: String -> Exp -> Exp -> Exp
hsPrimOpApp op :: String
op e :: Exp
e e1 :: Exp
e1 = Exp -> QOp -> Exp -> Exp
HS.InfixApp Exp
e (String -> QOp
hsPrimOp String
op) Exp
e1
hsInt :: Integer -> HS.Exp
hsInt :: Integer -> Exp
hsInt n :: Integer
n = Literal -> Exp
HS.Lit (Integer -> Literal
HS.Int Integer
n)
hsTypedInt :: Integral a => a -> HS.Exp
hsTypedInt :: a -> Exp
hsTypedInt n :: a
n = Exp -> Type -> Exp
HS.ExpTypeSig (Literal -> Exp
HS.Lit (Integer -> Literal
HS.Int (Integer -> Literal) -> Integer -> Literal
forall a b. (a -> b) -> a -> b
$ a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n)) (QName -> Type
HS.TyCon (String -> QName
hsName "Integer"))
hsTypedDouble :: Real a => a -> HS.Exp
hsTypedDouble :: a -> Exp
hsTypedDouble n :: a
n = Exp -> Type -> Exp
HS.ExpTypeSig (Literal -> Exp
HS.Lit (Rational -> Literal
HS.Frac (Rational -> Literal) -> Rational -> Literal
forall a b. (a -> b) -> a -> b
$ a -> Rational
forall a. Real a => a -> Rational
toRational a
n)) (QName -> Type
HS.TyCon (String -> QName
hsName "Double"))
hsLet :: HS.Name -> HS.Exp -> HS.Exp -> HS.Exp
hsLet :: Name -> Exp -> Exp -> Exp
hsLet x :: Name
x e :: Exp
e b :: Exp
b =
Binds -> Exp -> Exp
HS.Let ([Decl] -> Binds
HS.BDecls [[Match] -> Decl
HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
HS.Match Name
x [] (Exp -> Rhs
HS.UnGuardedRhs Exp
e) Maybe Binds
emptyBinds]]) Exp
b
hsVarUQ :: HS.Name -> HS.Exp
hsVarUQ :: Name -> Exp
hsVarUQ = QName -> Exp
HS.Var (QName -> Exp) -> (Name -> QName) -> Name -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
HS.UnQual
hsAppView :: HS.Exp -> [HS.Exp]
hsAppView :: Exp -> [Exp]
hsAppView = [Exp] -> [Exp]
forall a. [a] -> [a]
reverse ([Exp] -> [Exp]) -> (Exp -> [Exp]) -> Exp -> [Exp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> [Exp]
view
where
view :: Exp -> [Exp]
view (HS.App e :: Exp
e e1 :: Exp
e1) = Exp
e1 Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: Exp -> [Exp]
view Exp
e
view (HS.InfixApp e1 :: Exp
e1 op :: QOp
op e2 :: Exp
e2) = [Exp
e2, Exp
e1, QOp -> Exp
hsOpToExp QOp
op]
view e :: Exp
e = [Exp
e]
hsOpToExp :: HS.QOp -> HS.Exp
hsOpToExp :: QOp -> Exp
hsOpToExp (HS.QVarOp x :: QName
x) = QName -> Exp
HS.Var QName
x
hsLambda :: [HS.Pat] -> HS.Exp -> HS.Exp
hsLambda :: [Pat] -> Exp -> Exp
hsLambda ps :: [Pat]
ps (HS.Lambda ps1 :: [Pat]
ps1 e :: Exp
e) = [Pat] -> Exp -> Exp
HS.Lambda ([Pat]
ps [Pat] -> [Pat] -> [Pat]
forall a. [a] -> [a] -> [a]
++ [Pat]
ps1) Exp
e
hsLambda ps :: [Pat]
ps e :: Exp
e = [Pat] -> Exp -> Exp
HS.Lambda [Pat]
ps Exp
e
hsMapAlt :: (HS.Exp -> HS.Exp) -> HS.Alt -> HS.Alt
hsMapAlt :: (Exp -> Exp) -> Alt -> Alt
hsMapAlt f :: Exp -> Exp
f (HS.Alt p :: Pat
p rhs :: Rhs
rhs wh :: Maybe Binds
wh) = Pat -> Rhs -> Maybe Binds -> Alt
HS.Alt Pat
p ((Exp -> Exp) -> Rhs -> Rhs
hsMapRHS Exp -> Exp
f Rhs
rhs) Maybe Binds
wh
hsMapRHS :: (HS.Exp -> HS.Exp) -> HS.Rhs -> HS.Rhs
hsMapRHS :: (Exp -> Exp) -> Rhs -> Rhs
hsMapRHS f :: Exp -> Exp
f (HS.UnGuardedRhs def :: Exp
def) = Exp -> Rhs
HS.UnGuardedRhs (Exp -> Exp
f Exp
def)
hsMapRHS f :: Exp -> Exp
f (HS.GuardedRhss es :: [GuardedRhs]
es) = [GuardedRhs] -> Rhs
HS.GuardedRhss [ [Stmt] -> Exp -> GuardedRhs
HS.GuardedRhs [Stmt]
g (Exp -> Exp
f Exp
e) | HS.GuardedRhs g :: [Stmt]
g e :: Exp
e <- [GuardedRhs]
es ]
mazstr :: String
mazstr :: String
mazstr = "MAlonzo.Code"
mazName :: Name
mazName :: Name
mazName = NameId -> String -> Name
forall a. MkName a => NameId -> a -> Name
mkName_ NameId
forall a. HasCallStack => a
__IMPOSSIBLE__ String
mazstr
mazMod' :: String -> HS.ModuleName
mazMod' :: String -> ModuleName
mazMod' s :: String
s = String -> ModuleName
HS.ModuleName (String -> ModuleName) -> String -> ModuleName
forall a b. (a -> b) -> a -> b
$ String
mazstr String -> String -> String
forall a. [a] -> [a] -> [a]
++ "." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
mazMod :: ModuleName -> HS.ModuleName
mazMod :: ModuleName -> ModuleName
mazMod = String -> ModuleName
mazMod' (String -> ModuleName)
-> (ModuleName -> String) -> ModuleName -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> String
forall a. Pretty a => a -> String
prettyShow
mazerror :: String -> a
mazerror :: String -> a
mazerror msg :: String
msg = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
mazstr String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg
mazCoerceName :: String
mazCoerceName :: String
mazCoerceName = "coe"
mazErasedName :: String
mazErasedName :: String
mazErasedName = "erased"
mazAnyTypeName :: String
mazAnyTypeName :: String
mazAnyTypeName = "AgdaAny"
mazCoerce :: HS.Exp
mazCoerce :: Exp
mazCoerce = QName -> Exp
HS.Var (QName -> Exp) -> QName -> Exp
forall a b. (a -> b) -> a -> b
$ Name -> QName
HS.UnQual (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ String -> Name
HS.Ident String
mazCoerceName
mazIncompleteMatch :: HS.Exp
mazIncompleteMatch :: Exp
mazIncompleteMatch = QName -> Exp
HS.Var (QName -> Exp) -> QName -> Exp
forall a b. (a -> b) -> a -> b
$ ModuleName -> Name -> QName
HS.Qual ModuleName
mazRTE (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ String -> Name
HS.Ident "mazIncompleteMatch"
rtmIncompleteMatch :: QName -> HS.Exp
rtmIncompleteMatch :: QName -> Exp
rtmIncompleteMatch q :: QName
q = Exp
mazIncompleteMatch Exp -> Exp -> Exp
`HS.App` Name -> Exp
hsVarUQ (String -> QName -> Name
unqhname "name" QName
q)
mazUnreachableError :: HS.Exp
mazUnreachableError :: Exp
mazUnreachableError = QName -> Exp
HS.Var (QName -> Exp) -> QName -> Exp
forall a b. (a -> b) -> a -> b
$ ModuleName -> Name -> QName
HS.Qual ModuleName
mazRTE (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ String -> Name
HS.Ident "mazUnreachableError"
rtmUnreachableError :: HS.Exp
rtmUnreachableError :: Exp
rtmUnreachableError = Exp
mazUnreachableError
mazAnyType :: HS.Type
mazAnyType :: Type
mazAnyType = QName -> Type
HS.TyCon (String -> QName
hsName String
mazAnyTypeName)
mazRTE :: HS.ModuleName
mazRTE :: ModuleName
mazRTE = String -> ModuleName
HS.ModuleName "MAlonzo.RTE"
rtmQual :: String -> HS.QName
rtmQual :: String -> QName
rtmQual = Name -> QName
HS.UnQual (Name -> QName) -> (String -> Name) -> String -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
HS.Ident
rtmVar :: String -> HS.Exp
rtmVar :: String -> Exp
rtmVar = QName -> Exp
HS.Var (QName -> Exp) -> (String -> QName) -> String -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> QName
rtmQual
rtmError :: String -> HS.Exp
rtmError :: String -> Exp
rtmError s :: String
s = String -> Exp
rtmVar "error" Exp -> Exp -> Exp
`HS.App`
(Literal -> Exp
HS.Lit (Literal -> Exp) -> Literal -> Exp
forall a b. (a -> b) -> a -> b
$ String -> Literal
HS.String (String -> Literal) -> String -> Literal
forall a b. (a -> b) -> a -> b
$ "MAlonzo Runtime Error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s)
unsafeCoerceMod :: HS.ModuleName
unsafeCoerceMod :: ModuleName
unsafeCoerceMod = String -> ModuleName
HS.ModuleName "Unsafe.Coerce"
fakeD :: HS.Name -> String -> HS.Decl
fakeD :: Name -> String -> Decl
fakeD v :: Name
v s :: String
s = [Match] -> Decl
HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
HS.Match Name
v [] (Exp -> Rhs
HS.UnGuardedRhs (Exp -> Rhs) -> Exp -> Rhs
forall a b. (a -> b) -> a -> b
$ String -> Exp
fakeExp String
s) Maybe Binds
emptyBinds]
fakeDS :: String -> String -> HS.Decl
fakeDS :: String -> String -> Decl
fakeDS = Name -> String -> Decl
fakeD (Name -> String -> Decl)
-> (String -> Name) -> String -> String -> Decl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
HS.Ident
fakeDQ :: QName -> String -> HS.Decl
fakeDQ :: QName -> String -> Decl
fakeDQ = Name -> String -> Decl
fakeD (Name -> String -> Decl)
-> (QName -> Name) -> QName -> String -> Decl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> QName -> Name
unqhname "d"
fakeType :: String -> HS.Type
fakeType :: String -> Type
fakeType = String -> Type
HS.FakeType
fakeExp :: String -> HS.Exp
fakeExp :: String -> Exp
fakeExp = String -> Exp
HS.FakeExp
fakeDecl :: String -> HS.Decl
fakeDecl :: String -> Decl
fakeDecl = String -> Decl
HS.FakeDecl
emptyBinds :: Maybe HS.Binds
emptyBinds :: Maybe Binds
emptyBinds = Maybe Binds
forall a. Maybe a
Nothing
isModChar :: Char -> Bool
isModChar :: Char -> Bool
isModChar c :: Char
c =
Char -> Bool
isLower Char
c Bool -> Bool -> Bool
|| Char -> Bool
isUpper Char
c Bool -> Bool -> Bool
|| Char -> Bool
isDigit Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '_' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '\''