{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Compiler.MAlonzo.Misc where
import Control.Monad.Reader ( ask )
import Control.Monad.State ( modify )
import Control.Monad.Trans ( MonadTrans(lift) )
import Control.Monad.Trans.Except ( ExceptT )
import Control.Monad.Trans.Identity ( IdentityT )
import Control.Monad.Trans.Maybe ( MaybeT )
import Control.Monad.Trans.Reader ( ReaderT(runReaderT) )
import Control.Monad.Trans.State ( StateT(runStateT) )
import Data.Char
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (Text)
import qualified Data.Text as T
import qualified Agda.Utils.Haskell.Syntax as HS
import Agda.Compiler.Common as CC
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.TopLevelModuleName
import Agda.TypeChecking.Monad
import Agda.Syntax.Common.Pretty
import Agda.Utils.Impossible
data HsModuleEnv = HsModuleEnv
{ HsModuleEnv -> TopLevelModuleName
mazModuleName :: TopLevelModuleName
, HsModuleEnv -> Bool
mazIsMainModule :: Bool
}
data GHCOptions = GHCOptions
{ GHCOptions -> Bool
optGhcCallGhc :: Bool
, GHCOptions -> String
optGhcBin :: FilePath
, GHCOptions -> [String]
optGhcFlags :: [String]
, GHCOptions -> String
optGhcCompileDir :: FilePath
, GHCOptions -> Bool
optGhcStrictData :: Bool
, GHCOptions -> Bool
optGhcStrict :: Bool
}
data GHCEnv = GHCEnv
{ GHCEnv -> GHCOptions
ghcEnvOpts :: GHCOptions
, GHCEnv -> Maybe QName
ghcEnvBool
, GHCEnv -> Maybe QName
ghcEnvTrue
, GHCEnv -> Maybe QName
ghcEnvFalse
, GHCEnv -> Maybe QName
ghcEnvMaybe
, GHCEnv -> Maybe QName
ghcEnvNothing
, GHCEnv -> Maybe QName
ghcEnvJust
, GHCEnv -> Maybe QName
ghcEnvList
, GHCEnv -> Maybe QName
ghcEnvNil
, GHCEnv -> Maybe QName
ghcEnvCons
, GHCEnv -> Maybe QName
ghcEnvNat
, GHCEnv -> Maybe QName
ghcEnvInteger
, GHCEnv -> Maybe QName
ghcEnvWord64
, GHCEnv -> Maybe QName
ghcEnvInf
, GHCEnv -> Maybe QName
ghcEnvSharp
, GHCEnv -> Maybe QName
ghcEnvFlat
, GHCEnv -> Maybe QName
ghcEnvInterval
, GHCEnv -> Maybe QName
ghcEnvIZero
, GHCEnv -> Maybe QName
ghcEnvIOne
, GHCEnv -> Maybe QName
ghcEnvIsOne
, GHCEnv -> Maybe QName
ghcEnvItIsOne
, GHCEnv -> Maybe QName
ghcEnvIsOne1
, GHCEnv -> Maybe QName
ghcEnvIsOne2
, GHCEnv -> Maybe QName
ghcEnvIsOneEmpty
, GHCEnv -> Maybe QName
ghcEnvPathP
, GHCEnv -> Maybe QName
ghcEnvSub
, GHCEnv -> Maybe QName
ghcEnvSubIn
, GHCEnv -> Maybe QName
ghcEnvId
, GHCEnv -> Maybe QName
ghcEnvConId
:: Maybe QName
, GHCEnv -> QName -> Bool
ghcEnvIsTCBuiltin :: QName -> Bool
, GHCEnv -> Maybe Nat
ghcEnvListArity :: Maybe Int
, GHCEnv -> Maybe Nat
ghcEnvMaybeArity :: Maybe Int
}
data GHCModuleEnv = GHCModuleEnv
{ GHCModuleEnv -> GHCEnv
ghcModEnv :: GHCEnv
, GHCModuleEnv -> HsModuleEnv
ghcModHsModuleEnv :: HsModuleEnv
}
class Monad m => ReadGHCModuleEnv m where
askGHCModuleEnv :: m GHCModuleEnv
default askGHCModuleEnv
:: (MonadTrans t, Monad n, m ~ (t n), ReadGHCModuleEnv n)
=> m GHCModuleEnv
askGHCModuleEnv = n GHCModuleEnv -> t n GHCModuleEnv
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift n GHCModuleEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m GHCModuleEnv
askGHCModuleEnv
askHsModuleEnv :: m HsModuleEnv
askHsModuleEnv = GHCModuleEnv -> HsModuleEnv
ghcModHsModuleEnv (GHCModuleEnv -> HsModuleEnv) -> m GHCModuleEnv -> m HsModuleEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m GHCModuleEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m GHCModuleEnv
askGHCModuleEnv
askGHCEnv :: m GHCEnv
askGHCEnv = GHCModuleEnv -> GHCEnv
ghcModEnv (GHCModuleEnv -> GHCEnv) -> m GHCModuleEnv -> m GHCEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m GHCModuleEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m GHCModuleEnv
askGHCModuleEnv
instance Monad m => ReadGHCModuleEnv (ReaderT GHCModuleEnv m) where
askGHCModuleEnv :: ReaderT GHCModuleEnv m GHCModuleEnv
askGHCModuleEnv = ReaderT GHCModuleEnv m GHCModuleEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
instance ReadGHCModuleEnv m => ReadGHCModuleEnv (ExceptT e m)
instance ReadGHCModuleEnv m => ReadGHCModuleEnv (IdentityT m)
instance ReadGHCModuleEnv m => ReadGHCModuleEnv (MaybeT m)
instance ReadGHCModuleEnv m => ReadGHCModuleEnv (StateT s m)
newtype HsCompileState = HsCompileState
{ HsCompileState -> Set TopLevelModuleName
mazAccumlatedImports :: Set TopLevelModuleName
} deriving (HsCompileState -> HsCompileState -> Bool
(HsCompileState -> HsCompileState -> Bool)
-> (HsCompileState -> HsCompileState -> Bool) -> Eq HsCompileState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HsCompileState -> HsCompileState -> Bool
== :: HsCompileState -> HsCompileState -> Bool
$c/= :: HsCompileState -> HsCompileState -> Bool
/= :: HsCompileState -> HsCompileState -> Bool
Eq, NonEmpty HsCompileState -> HsCompileState
HsCompileState -> HsCompileState -> HsCompileState
(HsCompileState -> HsCompileState -> HsCompileState)
-> (NonEmpty HsCompileState -> HsCompileState)
-> (forall b. Integral b => b -> HsCompileState -> HsCompileState)
-> Semigroup HsCompileState
forall b. Integral b => b -> HsCompileState -> HsCompileState
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: HsCompileState -> HsCompileState -> HsCompileState
<> :: HsCompileState -> HsCompileState -> HsCompileState
$csconcat :: NonEmpty HsCompileState -> HsCompileState
sconcat :: NonEmpty HsCompileState -> HsCompileState
$cstimes :: forall b. Integral b => b -> HsCompileState -> HsCompileState
stimes :: forall b. Integral b => b -> HsCompileState -> HsCompileState
Semigroup, Semigroup HsCompileState
HsCompileState
Semigroup HsCompileState =>
HsCompileState
-> (HsCompileState -> HsCompileState -> HsCompileState)
-> ([HsCompileState] -> HsCompileState)
-> Monoid HsCompileState
[HsCompileState] -> HsCompileState
HsCompileState -> HsCompileState -> HsCompileState
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: HsCompileState
mempty :: HsCompileState
$cmappend :: HsCompileState -> HsCompileState -> HsCompileState
mappend :: HsCompileState -> HsCompileState -> HsCompileState
$cmconcat :: [HsCompileState] -> HsCompileState
mconcat :: [HsCompileState] -> HsCompileState
Monoid)
type HsCompileT m = ReaderT GHCModuleEnv (StateT HsCompileState m)
type HsCompileM = HsCompileT TCM
runHsCompileT' :: HsCompileT m a -> GHCModuleEnv -> HsCompileState -> m (a, HsCompileState)
runHsCompileT' :: forall (m :: * -> *) a.
HsCompileT m a
-> GHCModuleEnv -> HsCompileState -> m (a, HsCompileState)
runHsCompileT' HsCompileT m a
t GHCModuleEnv
e HsCompileState
s = ((StateT HsCompileState m a
-> HsCompileState -> m (a, HsCompileState))
-> HsCompileState
-> StateT HsCompileState m a
-> m (a, HsCompileState)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT HsCompileState m a
-> HsCompileState -> m (a, HsCompileState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT HsCompileState
s) (StateT HsCompileState m a -> m (a, HsCompileState))
-> (HsCompileT m a -> StateT HsCompileState m a)
-> HsCompileT m a
-> m (a, HsCompileState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((HsCompileT m a -> GHCModuleEnv -> StateT HsCompileState m a)
-> GHCModuleEnv -> HsCompileT m a -> StateT HsCompileState m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip HsCompileT m a -> GHCModuleEnv -> StateT HsCompileState m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT GHCModuleEnv
e) (HsCompileT m a -> m (a, HsCompileState))
-> HsCompileT m a -> m (a, HsCompileState)
forall a b. (a -> b) -> a -> b
$ HsCompileT m a
t
runHsCompileT :: HsCompileT m a -> GHCModuleEnv -> m (a, HsCompileState)
runHsCompileT :: forall (m :: * -> *) a.
HsCompileT m a -> GHCModuleEnv -> m (a, HsCompileState)
runHsCompileT HsCompileT m a
t GHCModuleEnv
e = HsCompileT m a
-> GHCModuleEnv -> HsCompileState -> m (a, HsCompileState)
forall (m :: * -> *) a.
HsCompileT m a
-> GHCModuleEnv -> HsCompileState -> m (a, HsCompileState)
runHsCompileT' HsCompileT m a
t GHCModuleEnv
e HsCompileState
forall a. Monoid a => a
mempty
curIsMainModule :: ReadGHCModuleEnv m => m Bool
curIsMainModule :: forall (m :: * -> *). ReadGHCModuleEnv m => m Bool
curIsMainModule = HsModuleEnv -> Bool
mazIsMainModule (HsModuleEnv -> Bool) -> m HsModuleEnv -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m HsModuleEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m HsModuleEnv
askHsModuleEnv
curAgdaMod :: ReadGHCModuleEnv m => m TopLevelModuleName
curAgdaMod :: forall (m :: * -> *). ReadGHCModuleEnv m => m TopLevelModuleName
curAgdaMod = HsModuleEnv -> TopLevelModuleName
mazModuleName (HsModuleEnv -> TopLevelModuleName)
-> m HsModuleEnv -> m TopLevelModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m HsModuleEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m HsModuleEnv
askHsModuleEnv
curHsMod :: ReadGHCModuleEnv m => m HS.ModuleName
curHsMod :: forall (m :: * -> *). ReadGHCModuleEnv m => m ModuleName
curHsMod = TopLevelModuleName -> ModuleName
mazMod (TopLevelModuleName -> ModuleName)
-> m TopLevelModuleName -> m ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m TopLevelModuleName
forall (m :: * -> *). ReadGHCModuleEnv m => m TopLevelModuleName
curAgdaMod
data FunctionKind = NoUnused | PossiblyUnused
data VariableKind = A | V | X
data NameKind
= TypeK
| ConK
| VarK VariableKind
| CoverK
| CheckK
| FunK FunctionKind
encodeString :: NameKind -> String -> String
encodeString :: NameKind -> String -> String
encodeString NameKind
k String
s = String
prefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
encode String
s
where
encode :: Char -> String
encode Char
'\'' = String
"''"
encode Char
c
| Char -> Bool
isLower Char
c Bool -> Bool -> Bool
|| Char -> Bool
isUpper Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
||
Char -> GeneralCategory
generalCategory Char
c GeneralCategory -> GeneralCategory -> Bool
forall a. Eq a => a -> a -> Bool
== GeneralCategory
DecimalNumber =
[Char
c]
| Bool
otherwise =
String
"'" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (Char -> Nat
forall a. Enum a => a -> Nat
fromEnum Char
c) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'"
prefix :: String
prefix = case NameKind
k of
NameKind
TypeK -> String
"T"
NameKind
ConK -> String
"C"
VarK VariableKind
A -> String
"a"
VarK VariableKind
V -> String
"v"
VarK VariableKind
X -> String
"x"
NameKind
CoverK -> String
"cover"
NameKind
CheckK -> String
"check"
FunK FunctionKind
NoUnused -> String
"du"
FunK FunctionKind
PossiblyUnused -> String
"d"
ihname :: VariableKind -> Nat -> HS.Name
ihname :: VariableKind -> Nat -> Name
ihname VariableKind
k Nat
i = String -> Name
HS.Ident (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ NameKind -> String -> String
encodeString (VariableKind -> NameKind
VarK VariableKind
k) (Nat -> String
forall a. Show a => a -> String
show Nat
i)
unqhname :: NameKind -> QName -> HS.Name
unqhname :: NameKind -> QName -> Name
unqhname NameKind
k QName
q =
String -> Name
HS.Ident (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ NameKind -> String -> String
encodeString NameKind
k (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Pretty a => a -> String
prettyShow (Name -> Name
nameCanonical Name
n) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NameId -> String
idnum (Name -> NameId
nameId Name
n)
where
n :: Name
n = QName -> Name
qnameName QName
q
idnum :: NameId -> String
idnum (NameId Word64
x ModuleNameHash
_) = Integer -> String
forall a. Show a => a -> String
show (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
x)
tlmodOf :: ReadTCState m => ModuleName -> m HS.ModuleName
tlmodOf :: forall (m :: * -> *). ReadTCState m => ModuleName -> m ModuleName
tlmodOf = (TopLevelModuleName -> ModuleName)
-> m TopLevelModuleName -> m ModuleName
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TopLevelModuleName -> ModuleName
mazMod (m TopLevelModuleName -> m ModuleName)
-> (ModuleName -> m TopLevelModuleName)
-> ModuleName
-> m ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> m TopLevelModuleName
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m TopLevelModuleName
CC.topLevelModuleName
xqual :: QName -> HS.Name -> HsCompileM HS.QName
xqual :: QName -> Name -> HsCompileM QName
xqual QName
q Name
n = do
m1 <- ModuleName
-> ReaderT
GHCModuleEnv (StateT HsCompileState TCM) TopLevelModuleName
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m TopLevelModuleName
CC.topLevelModuleName (QName -> ModuleName
qnameModule QName
q)
m2 <- curAgdaMod
if m1 == m2
then return (HS.UnQual n)
else do
modify (HsCompileState . Set.insert m1 . mazAccumlatedImports)
return (HS.Qual (mazMod m1) n)
xhqn :: NameKind -> QName -> HsCompileM HS.QName
xhqn :: NameKind -> QName -> HsCompileM QName
xhqn NameKind
k QName
q = QName -> Name -> HsCompileM QName
xqual QName
q (NameKind -> QName -> Name
unqhname NameKind
k QName
q)
hsName :: String -> HS.QName
hsName :: String -> QName
hsName String
s = Name -> QName
HS.UnQual (String -> Name
HS.Ident String
s)
conhqn :: QName -> HsCompileM HS.QName
conhqn :: QName -> HsCompileM QName
conhqn QName
q = NameKind -> QName -> HsCompileM QName
xhqn NameKind
ConK (QName -> HsCompileM QName)
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
-> HsCompileM QName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
q
bltQual :: BuiltinId -> String -> HsCompileM HS.QName
bltQual :: BuiltinId -> String -> HsCompileM QName
bltQual BuiltinId
b String
s = do
Def q _ <- BuiltinId -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
b
xqual q (HS.Ident s)
dname :: QName -> HS.Name
dname :: QName -> Name
dname QName
q = NameKind -> QName -> Name
unqhname (FunctionKind -> NameKind
FunK FunctionKind
PossiblyUnused) QName
q
duname :: QName -> HS.Name
duname :: QName -> Name
duname QName
q = NameKind -> QName -> Name
unqhname (FunctionKind -> NameKind
FunK FunctionKind
NoUnused) QName
q
hsPrimOp :: String -> HS.QOp
hsPrimOp :: String -> QOp
hsPrimOp 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 String
op Exp
e 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 Integer
n = Literal -> Exp
HS.Lit (Integer -> Literal
HS.Int Integer
n)
hsTypedInt :: Integral a => a -> HS.Exp
hsTypedInt :: forall a. Integral a => a -> Exp
hsTypedInt 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 String
"Integer"))
hsTypedDouble :: Real a => a -> HS.Exp
hsTypedDouble :: forall a. Real a => a -> Exp
hsTypedDouble 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 String
"Double"))
hsLet :: HS.Name -> HS.Exp -> HS.Exp -> HS.Exp
hsLet :: Name -> Exp -> Exp -> Exp
hsLet Name
x Exp
e Exp
b =
Binds -> Exp -> Exp
HS.Let ([Decl] -> Binds
HS.BDecls [Strictness -> Name -> Rhs -> Decl
HS.LocalBind Strictness
HS.Lazy Name
x (Exp -> Rhs
HS.UnGuardedRhs Exp
e)]) 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 Exp
e Exp
e1) = Exp
e1 Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: Exp -> [Exp]
view Exp
e
view (HS.InfixApp Exp
e1 QOp
op Exp
e2) = [Exp
e2, Exp
e1, QOp -> Exp
hsOpToExp QOp
op]
view Exp
e = [Exp
e]
hsOpToExp :: HS.QOp -> HS.Exp
hsOpToExp :: QOp -> Exp
hsOpToExp (HS.QVarOp QName
x) = QName -> Exp
HS.Var QName
x
hsLambda :: [HS.Pat] -> HS.Exp -> HS.Exp
hsLambda :: [Pat] -> Exp -> Exp
hsLambda [Pat]
ps (HS.Lambda [Pat]
ps1 Exp
e) = [Pat] -> Exp -> Exp
HS.Lambda ([Pat]
ps [Pat] -> [Pat] -> [Pat]
forall a. [a] -> [a] -> [a]
++ [Pat]
ps1) Exp
e
hsLambda [Pat]
ps 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 Exp -> Exp
f (HS.Alt Pat
p Rhs
rhs 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 Exp -> Exp
f (HS.UnGuardedRhs Exp
def) = Exp -> Rhs
HS.UnGuardedRhs (Exp -> Exp
f Exp
def)
hsMapRHS Exp -> Exp
f (HS.GuardedRhss [GuardedRhs]
es) = [GuardedRhs] -> Rhs
HS.GuardedRhss [ [Stmt] -> Exp -> GuardedRhs
HS.GuardedRhs [Stmt]
g (Exp -> Exp
f Exp
e) | HS.GuardedRhs [Stmt]
g Exp
e <- [GuardedRhs]
es ]
mazstr :: String
mazstr :: String
mazstr = String
"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' 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 -> String
forall a. [a] -> [a] -> [a]
++ String
s
mazMod :: TopLevelModuleName -> HS.ModuleName
mazMod :: TopLevelModuleName -> ModuleName
mazMod = String -> ModuleName
mazMod' (String -> ModuleName)
-> (TopLevelModuleName -> String)
-> TopLevelModuleName
-> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow
mazCoerceName :: String
mazCoerceName :: String
mazCoerceName = String
"coe"
mazErasedName :: String
mazErasedName :: String
mazErasedName = String
"erased"
mazAnyTypeName :: String
mazAnyTypeName :: String
mazAnyTypeName = String
"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
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 String
"mazUnreachableError"
rtmUnreachableError :: HS.Exp
rtmUnreachableError :: Exp
rtmUnreachableError = Exp
mazUnreachableError
mazHole :: HS.Exp
mazHole :: Exp
mazHole = 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 String
"mazHole"
rtmHole :: String -> HS.Exp
rtmHole :: String -> Exp
rtmHole String
s = Exp
mazHole Exp -> Exp -> Exp
`HS.App` Literal -> Exp
HS.Lit (Text -> Literal
HS.String (Text -> Literal) -> Text -> Literal
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack String
s)
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 String
"MAlonzo.RTE"
mazRTEFloat :: HS.ModuleName
mazRTEFloat :: ModuleName
mazRTEFloat = String -> ModuleName
HS.ModuleName String
"MAlonzo.RTE.Float"
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 :: Text -> HS.Exp
rtmError :: Text -> Exp
rtmError Text
s = String -> Exp
rtmVar String
"error" Exp -> Exp -> Exp
`HS.App`
Literal -> Exp
HS.Lit (Text -> Literal
HS.String (Text -> Literal) -> Text -> Literal
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"MAlonzo Runtime Error: " Text
s)
unsafeCoerceMod :: HS.ModuleName
unsafeCoerceMod :: ModuleName
unsafeCoerceMod = String -> ModuleName
HS.ModuleName String
"Unsafe.Coerce"
fakeD :: HS.Name -> String -> HS.Decl
fakeD :: Name -> String -> Decl
fakeD Name
v 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
. QName -> Name
dname
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 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
== Char
'_' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\''