    {-# LANGUAGE CPP #-}

    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

    #if !(MIN_VERSION_base(4,11,0))
    import Data.Semigroup
    #endif

    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.Utils.Pretty

    import Agda.Utils.Impossible

    --------------------------------------------------
    -- Setting up Interface before compile
    --------------------------------------------------

    data HsModuleEnv = HsModuleEnv
      { HsModuleEnv -> ModuleName
    mazModuleName :: ModuleName
        -- ^ The name of the Agda module
      , HsModuleEnv -> Bool
    mazIsMainModule :: Bool
      -- ^ Whether this is the compilation root and therefore should have the `main` function.
      --   This corresponds to the @IsMain@ flag provided to the backend,
      --   not necessarily whether the GHC module has a `main` function defined.
      }

    -- | The options derived from
    -- 'Agda.Compiler.MAlonzo.Compiler.GHCFlags' and other shared options.

    data GHCOptions = GHCOptions
      { GHCOptions -> Bool
    optGhcCallGhc    :: Bool
      , GHCOptions -> String
    optGhcBin        :: FilePath
        -- ^ Use the compiler at PATH instead of "ghc"
      , GHCOptions -> [String]
    optGhcFlags      :: [String]
      , GHCOptions -> String
    optGhcCompileDir :: FilePath
      , GHCOptions -> Bool
    optGhcStrictData :: Bool
        -- ^ Make inductive constructors strict?
      , GHCOptions -> Bool
    optGhcStrict :: Bool
        -- ^ Make functions strict?
      }

    -- | A static part of the GHC backend's environment that does not
    -- change from module to module.

    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
        -- Various (possibly) builtin names.
      , GHCEnv -> QName -> Bool
    ghcEnvIsTCBuiltin :: QName -> Bool
        -- ^ Is the given name a @TC@ builtin (except for @TC@ itself)?
      }

    -- | Module compilation environment, bundling the overall
    --   backend session options along with the module's basic
    --   readable properties.
    data GHCModuleEnv = GHCModuleEnv
      { GHCModuleEnv -> GHCEnv
    ghcModEnv         :: GHCEnv
      , GHCModuleEnv -> HsModuleEnv
    ghcModHsModuleEnv :: HsModuleEnv
      }

    -- | Monads that can produce a 'GHCModuleEnv'.
    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 (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 ModuleName
    mazAccumlatedImports :: Set ModuleName
      } deriving (HsCompileState -> HsCompileState -> Bool
    (HsCompileState -> HsCompileState -> Bool)
    -> (HsCompileState -> HsCompileState -> Bool) -> Eq HsCompileState
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: HsCompileState -> HsCompileState -> Bool
    $c/= :: HsCompileState -> HsCompileState -> Bool
    == :: HsCompileState -> HsCompileState -> Bool
    $c== :: 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
    stimes :: forall b. Integral b => b -> HsCompileState -> HsCompileState
    $cstimes :: forall b. Integral b => b -> HsCompileState -> HsCompileState
    sconcat :: NonEmpty HsCompileState -> HsCompileState
    $csconcat :: NonEmpty HsCompileState -> HsCompileState
    <> :: HsCompileState -> HsCompileState -> HsCompileState
    $c<> :: HsCompileState -> 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
    mconcat :: [HsCompileState] -> HsCompileState
    $cmconcat :: [HsCompileState] -> HsCompileState
    mappend :: HsCompileState -> HsCompileState -> HsCompileState
    $cmappend :: HsCompileState -> HsCompileState -> HsCompileState
    mempty :: HsCompileState
    $cmempty :: HsCompileState
    Monoid)

    -- | Transformer adding read-only module info and a writable set of imported modules
    type HsCompileT m = ReaderT GHCModuleEnv (StateT HsCompileState m)

    -- | The default compilation monad is the entire TCM (☹️) enriched with our state and module info
    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

    --------------------------------------------------
    -- utilities for haskell names
    --------------------------------------------------

    -- | Whether the current module is expected to have the `main` function.
    --   This corresponds to the @IsMain@ flag provided to the backend,
    --   not necessarily whether the GHC module actually has a `main` function defined.
    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

    -- | This is the same value as @curMName@, but does not rely on the TCM's state.
    --   (@curMName@ and co. should be removed, but the current @Backend@ interface
    --   is not sufficient yet to allow that)
    curAgdaMod :: ReadGHCModuleEnv m => m ModuleName
    curAgdaMod :: forall (m :: * -> *). ReadGHCModuleEnv m => m ModuleName
    curAgdaMod = HsModuleEnv -> ModuleName
    mazModuleName (HsModuleEnv -> ModuleName) -> m HsModuleEnv -> m ModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m HsModuleEnv
    forall (m :: * -> *). ReadGHCModuleEnv m => m HsModuleEnv
    askHsModuleEnv

    -- | Get the Haskell module name of the currently-focused Agda module
    curHsMod :: ReadGHCModuleEnv m => m HS.ModuleName
    curHsMod :: forall (m :: * -> *). ReadGHCModuleEnv m => m ModuleName
    curHsMod = ModuleName -> ModuleName
    mazMod (ModuleName -> ModuleName) -> m ModuleName -> m ModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m ModuleName
    forall (m :: * -> *). ReadGHCModuleEnv m => m ModuleName
    curAgdaMod

    -- | There are two kinds of functions: those definitely without unused
    -- arguments, and those that might have unused arguments.

    data FunctionKind = NoUnused | PossiblyUnused

    -- | Different kinds of variables: those starting with @a@, those
    -- starting with @v@, and those starting with @x@.

    data VariableKind = A | V | X

    -- | Different kinds of names.

    data NameKind
      = TypeK
        -- ^ Types.
      | ConK
        -- ^ Constructors.
      | VarK VariableKind
        -- ^ Variables.
      | CoverK
        -- ^ Used for coverage checking.
      | CheckK
        -- ^ Used for constructor type checking.
      | FunK FunctionKind
        -- ^ Other functions.

    -- | Turns strings into valid Haskell identifiers.
    --
    -- In order to avoid clashes with names of regular Haskell definitions
    -- (those not generated from Agda definitions), make sure that the
    -- Haskell names are always used qualified, with the exception of
    -- names from the prelude.

    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)

    -- the toplevel module containing the given one
    tlmodOf :: ReadTCState m => ModuleName -> m HS.ModuleName
    tlmodOf :: forall (m :: * -> *). ReadTCState m => ModuleName -> m ModuleName
    tlmodOf = (ModuleName -> ModuleName) -> m ModuleName -> m ModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ModuleName -> ModuleName
    mazMod (m ModuleName -> m ModuleName)
    -> (ModuleName -> m ModuleName) -> ModuleName -> m ModuleName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleName -> m ModuleName
    forall (m :: * -> *). ReadTCState m => ModuleName -> m ModuleName
    topLevelModuleName

    -- qualify HS.Name n by the module of QName q, if necessary;
    -- accumulates the used module in stImportedModules at the same time.
    xqual :: QName -> HS.Name -> HsCompileM HS.QName
    xqual :: QName -> Name -> HsCompileM QName
    xqual QName
    q Name
    n = do
      ModuleName
    m1 <- ModuleName
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ModuleName
    forall (m :: * -> *). ReadTCState m => ModuleName -> m ModuleName
    topLevelModuleName (QName -> ModuleName
    qnameModule QName
    q)
      ModuleName
    m2 <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) ModuleName
    forall (m :: * -> *). ReadGHCModuleEnv m => m ModuleName
    curAgdaMod
      if ModuleName
    m1 ModuleName -> ModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleName
    m2
        then QName -> HsCompileM QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name -> QName
    HS.UnQual Name
    n)
        else do
          (HsCompileState -> HsCompileState)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (Set ModuleName -> HsCompileState
    HsCompileState (Set ModuleName -> HsCompileState)
    -> (HsCompileState -> Set ModuleName)
    -> HsCompileState
    -> HsCompileState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleName -> Set ModuleName -> Set ModuleName
    forall a. Ord a => a -> Set a -> Set a
    Set.insert ModuleName
    m1 (Set ModuleName -> Set ModuleName)
    -> (HsCompileState -> Set ModuleName)
    -> HsCompileState
    -> Set ModuleName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HsCompileState -> Set ModuleName
    mazAccumlatedImports)
          QName -> HsCompileM QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ModuleName -> Name -> QName
    HS.Qual (ModuleName -> ModuleName
    mazMod ModuleName
    m1) Name
    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)

    -- always use the original name for a constructor even when it's redefined.
    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

    -- qualify name s by the module of builtin b
    bltQual :: String -> String -> HsCompileM HS.QName
    bltQual :: String -> String -> HsCompileM QName
    bltQual String
    b String
    s = do
      Def QName
    q Elims
    _ <- String -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    String -> m Term
    getBuiltin String
    b
      QName -> Name -> HsCompileM QName
    xqual QName
    q (String -> Name
    HS.Ident String
    s)

    dname :: QName -> HS.Name
    dname :: QName -> Name
    dname QName
    q = NameKind -> QName -> Name
    unqhname (FunctionKind -> NameKind
    FunK FunctionKind
    PossiblyUnused) QName
    q

    -- | Name for definition stripped of unused arguments
    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 ]

    --------------------------------------------------
    -- Hard coded module names
    --------------------------------------------------

    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 :: 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

    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 = HS.Var $ HS.Qual unsafeCoerceMod (HS.Ident "unsafeCoerce")
    -- mazCoerce = HS.Var $ HS.Qual mazRTE $ HS.Ident mazCoerceName
    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"

    --------------------------------------------------
    -- Sloppy ways to declare <name> = <string>
    --------------------------------------------------

    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

    --------------------------------------------------
    -- Auxiliary definitions
    --------------------------------------------------

    emptyBinds :: Maybe HS.Binds
    emptyBinds :: Maybe Binds
    emptyBinds = Maybe Binds
    forall a. Maybe a
    Nothing

    --------------------------------------------------
    -- Utilities for Haskell modules names
    --------------------------------------------------

    -- | Can the character be used in a Haskell module name part
    -- (@conid@)? This function is more restrictive than what the Haskell
    -- report allows.

    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
    '\''