    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.Compiler.MAlonzo.Primitives where

    import Control.Arrow ( second )
    import Control.Monad.Trans.Maybe ( MaybeT(MaybeT, runMaybeT) )

    import qualified Data.List as List
    import           Data.Map (Map)
    import qualified Data.Map as Map
    import qualified Data.HashMap.Strict as HMap
    import Data.Maybe

    import Agda.Compiler.Common
    import Agda.Compiler.MAlonzo.Misc
    import Agda.Syntax.Common
    import Agda.Syntax.Common.Pretty (prettyShow)
    import Agda.Syntax.Internal
    import Agda.Syntax.Treeless
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Primitive
    import Agda.TypeChecking.Reduce

    import Agda.Utils.Either
    import Agda.Utils.Lens
    import Agda.Utils.List   (hasElem)
    import qualified Agda.Utils.Haskell.Syntax as HS

    import Agda.Utils.Impossible

    newtype MainFunctionDef = MainFunctionDef Definition

    data CheckedMainFunctionDef = CheckedMainFunctionDef
      { CheckedMainFunctionDef -> MainFunctionDef
    checkedMainDef :: MainFunctionDef
      , CheckedMainFunctionDef -> Decl
    checkedMainDecl :: HS.Decl
      }

    -- Andreas, 2019-04-29, issue #3731: exclude certain kinds of names, like constructors.
    -- TODO: Also only consider top-level definition (not buried inside a module).
    asMainFunctionDef :: Definition -> Maybe MainFunctionDef
    asMainFunctionDef :: Definition -> Maybe MainFunctionDef
    asMainFunctionDef Definition
    d = case (Definition -> Defn
    theDef Definition
    d) of
        Axiom{}                              -> Maybe MainFunctionDef
    perhaps
        Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Left ProjectionLikenessMissing
    _ }   -> Maybe MainFunctionDef
    perhaps
        Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right{}  } -> Maybe MainFunctionDef
    forall {a}. Maybe a
    no
        AbstractDefn{}                       -> Maybe MainFunctionDef
    forall {a}. Maybe a
    no
        GeneralizableVar{}                   -> Maybe MainFunctionDef
    forall {a}. Maybe a
    no
        DataOrRecSig{}                       -> Maybe MainFunctionDef
    forall {a}. Maybe a
    no
        Datatype{}                           -> Maybe MainFunctionDef
    forall {a}. Maybe a
    no
        Record{}                             -> Maybe MainFunctionDef
    forall {a}. Maybe a
    no
        Constructor{}                        -> Maybe MainFunctionDef
    forall {a}. Maybe a
    no
        Primitive{}                          -> Maybe MainFunctionDef
    forall {a}. Maybe a
    no
        PrimitiveSort{}                      -> Maybe MainFunctionDef
    forall {a}. Maybe a
    no
      where
      isNamedMain :: Bool
    isNamedMain = String
    "main" String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name -> String
    forall a. Pretty a => a -> String
    prettyShow (Name -> Name
    nameConcrete (Name -> Name) -> (Definition -> Name) -> Definition -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    qnameName (QName -> Name) -> (Definition -> QName) -> Definition -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> QName
    defName (Definition -> Name) -> Definition -> Name
    forall a b. (a -> b) -> a -> b
    $ Definition
    d)  -- ignores the qualification!?
      perhaps :: Maybe MainFunctionDef
    perhaps | Bool
    isNamedMain = MainFunctionDef -> Maybe MainFunctionDef
    forall a. a -> Maybe a
    Just (MainFunctionDef -> Maybe MainFunctionDef)
    -> MainFunctionDef -> Maybe MainFunctionDef
    forall a b. (a -> b) -> a -> b
    $ Definition -> MainFunctionDef
    MainFunctionDef Definition
    d
              | Bool
    otherwise   = Maybe MainFunctionDef
    forall {a}. Maybe a
    no
      no :: Maybe a
    no                    = Maybe a
    forall {a}. Maybe a
    Nothing

    mainFunctionDefs :: Interface -> [MainFunctionDef]
    mainFunctionDefs :: Interface -> [MainFunctionDef]
    mainFunctionDefs Interface
    i = [Maybe MainFunctionDef] -> [MainFunctionDef]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe MainFunctionDef] -> [MainFunctionDef])
    -> [Maybe MainFunctionDef] -> [MainFunctionDef]
    forall a b. (a -> b) -> a -> b
    $ Definition -> Maybe MainFunctionDef
    asMainFunctionDef (Definition -> Maybe MainFunctionDef)
    -> [Definition] -> [Maybe MainFunctionDef]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Definition]
    defs
      where
        defs :: [Definition]
    defs = HashMap QName Definition -> [Definition]
    forall k v. HashMap k v -> [v]
    HMap.elems (HashMap QName Definition -> [Definition])
    -> HashMap QName Definition -> [Definition]
    forall a b. (a -> b) -> a -> b
    $ Interface -> Signature
    iSignature Interface
    i Signature
    -> Lens' Signature (HashMap QName Definition)
    -> HashMap QName Definition
    forall o i. o -> Lens' o i -> i
    ^. (HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature
    Lens' Signature (HashMap QName Definition)
    sigDefinitions

    -- | Check that the main function has type IO a, for some a.
    checkTypeOfMain :: Definition -> HsCompileM (Maybe CheckedMainFunctionDef)
    checkTypeOfMain :: Definition -> HsCompileM (Maybe CheckedMainFunctionDef)
    checkTypeOfMain Definition
    def = MaybeT
      (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)))
      CheckedMainFunctionDef
    -> HsCompileM (Maybe CheckedMainFunctionDef)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT
       (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)))
       CheckedMainFunctionDef
     -> HsCompileM (Maybe CheckedMainFunctionDef))
    -> MaybeT
         (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)))
         CheckedMainFunctionDef
    -> HsCompileM (Maybe CheckedMainFunctionDef)
    forall a b. (a -> b) -> a -> b
    $ do
      -- Only indicate main functions in the main module.
      isMainModule <- MaybeT
      (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO))) Bool
    forall (m :: * -> *). ReadGHCModuleEnv m => m Bool
    curIsMainModule
      mainDef <- MaybeT $ pure $ if isMainModule then asMainFunctionDef def else Nothing
      liftTCM $ checkTypeOfMain' mainDef

    checkTypeOfMain' :: MainFunctionDef -> TCM CheckedMainFunctionDef
    checkTypeOfMain' :: MainFunctionDef -> TCM CheckedMainFunctionDef
    checkTypeOfMain' m :: MainFunctionDef
    m@(MainFunctionDef Definition
    def) = MainFunctionDef -> Decl -> CheckedMainFunctionDef
    CheckedMainFunctionDef MainFunctionDef
    m (Decl -> CheckedMainFunctionDef)
    -> TCMT IO Decl -> TCM CheckedMainFunctionDef
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        Def io _ <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIO
        ty <- reduce $ defType def
        case unEl ty of
          Def QName
    d Elims
    _ | QName
    d QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    io -> Decl -> TCMT IO Decl
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Decl
    mainAlias
          Term
    _ -> GHCBackendError -> TCMT IO Decl
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    GHCBackendError -> m a
    ghcBackendError (GHCBackendError -> TCMT IO Decl)
    -> GHCBackendError -> TCMT IO Decl
    forall a b. (a -> b) -> a -> b
    $ QName -> Type -> GHCBackendError
    WrongTypeOfMain QName
    io Type
    ty
      where
        mainAlias :: Decl
    mainAlias = [Match] -> Decl
    HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match Name
    mainLHS [] Rhs
    mainRHS Maybe Binds
    emptyBinds ]
        mainLHS :: Name
    mainLHS   = String -> Name
    HS.Ident String
    "main"
        mainRHS :: Rhs
    mainRHS   = Exp -> Rhs
    HS.UnGuardedRhs (Exp -> Rhs) -> Exp -> Rhs
    forall a b. (a -> b) -> a -> b
    $ Exp -> Exp -> Exp
    HS.App 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
    $ QName -> Name
    dname (QName -> Name) -> QName -> Name
    forall a b. (a -> b) -> a -> b
    $ Definition -> QName
    defName Definition
    def)

    treelessPrimName :: TPrim -> String
    treelessPrimName :: TPrim -> String
    treelessPrimName TPrim
    p =
      case TPrim
    p of
        TPrim
    PQuot   -> String
    "quotInt"
        TPrim
    PRem    -> String
    "remInt"
        TPrim
    PSub    -> String
    "subInt"
        TPrim
    PAdd    -> String
    "addInt"
        TPrim
    PMul    -> String
    "mulInt"
        TPrim
    PGeq    -> String
    "geqInt"
        TPrim
    PLt     -> String
    "ltInt"
        TPrim
    PEqI    -> String
    "eqInt"
        TPrim
    PQuot64 -> String
    "quot64"
        TPrim
    PRem64  -> String
    "rem64"
        TPrim
    PSub64  -> String
    "sub64"
        TPrim
    PAdd64  -> String
    "add64"
        TPrim
    PMul64  -> String
    "mul64"
        TPrim
    PLt64   -> String
    "lt64"
        TPrim
    PEq64   -> String
    "eq64"
        TPrim
    PITo64  -> String
    "word64FromNat"
        TPrim
    P64ToI  -> String
    "word64ToNat"
        TPrim
    PEqF    -> String
    "MAlonzo.RTE.Float.doubleDenotEq"
        -- MAlonzo uses literal patterns, so we don't need equality for the other primitive types
        TPrim
    PEqC    -> String
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        TPrim
    PEqS    -> String
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        TPrim
    PEqQ    -> String
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        TPrim
    PSeq    -> String
    "seq"
        -- primitives only used by GuardsToPrims transformation, which MAlonzo doesn't use
        TPrim
    PIf     -> String
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Haskell modules to be imported for BUILT-INs
    importsForPrim :: BuiltinThings -> [Definition] -> [HS.ModuleName]
    importsForPrim :: BuiltinThings -> [Definition] -> [ModuleName]
    importsForPrim BuiltinThings
    builtinThings [Definition]
    defs = Map SomeBuiltin ModuleName
    -> BuiltinThings -> [Definition] -> [ModuleName]
    forall a. Map SomeBuiltin a -> BuiltinThings -> [Definition] -> [a]
    xForPrim Map SomeBuiltin ModuleName
    table BuiltinThings
    builtinThings [Definition]
    defs [ModuleName] -> [ModuleName] -> [ModuleName]
    forall a. [a] -> [a] -> [a]
    ++ [String -> ModuleName
    HS.ModuleName String
    "Data.Text"]
      where
      table :: Map SomeBuiltin ModuleName
    table = [(SomeBuiltin, ModuleName)] -> Map SomeBuiltin ModuleName
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(SomeBuiltin, ModuleName)] -> Map SomeBuiltin ModuleName)
    -> [(SomeBuiltin, ModuleName)] -> Map SomeBuiltin ModuleName
    forall a b. (a -> b) -> a -> b
    $ ((SomeBuiltin, String) -> (SomeBuiltin, ModuleName))
    -> [(SomeBuiltin, String)] -> [(SomeBuiltin, ModuleName)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((String -> ModuleName)
    -> (SomeBuiltin, String) -> (SomeBuiltin, ModuleName)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second String -> ModuleName
    HS.ModuleName)
        [ BuiltinId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin BuiltinId
    BuiltinChar                SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimFloatCeiling           SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimFloatDecode            SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimFloatEncode            SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimFloatEquality          SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimFloatFloor             SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimFloatInequality        SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimFloatIsSafeInteger     SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimFloatLess              SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimFloatRound             SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimFloatToRatio           SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimFloatToWord64          SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimIsAlpha                SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimIsAscii                SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimIsDigit                SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimIsHexDigit             SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimIsLatin1               SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimIsLower                SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimIsPrint                SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimIsSpace                SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimRatioToFloat           SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimToLower                SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    PrimToUpper                SomeBuiltin -> String -> (SomeBuiltin, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        ]
      |-> :: a -> b -> (a, b)
    (|->) = (,)

    --------------

    xForPrim :: Map SomeBuiltin a -> BuiltinThings -> [Definition] -> [a]
    xForPrim :: forall a. Map SomeBuiltin a -> BuiltinThings -> [Definition] -> [a]
    xForPrim Map SomeBuiltin a
    table BuiltinThings
    builtinThings [Definition]
    defs = [Maybe a] -> [a]
    forall a. [Maybe a] -> [a]
    catMaybes
        [ SomeBuiltin -> Map SomeBuiltin a -> Maybe a
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup SomeBuiltin
    s Map SomeBuiltin a
    table
        | (SomeBuiltin
    s, Builtin PrimFun
    def) <- BuiltinThings -> [(SomeBuiltin, Builtin PrimFun)]
    forall k a. Map k a -> [(k, a)]
    Map.toList BuiltinThings
    builtinThings
        , Bool -> (QName -> Bool) -> Maybe QName -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False QName -> Bool
    elemDefs (Maybe QName -> Bool) -> Maybe QName -> Bool
    forall a b. (a -> b) -> a -> b
    $ Builtin PrimFun -> Maybe QName
    getName Builtin PrimFun
    def
        ]
      where
      elemDefs :: QName -> Bool
    elemDefs = [QName] -> QName -> Bool
    forall a. Ord a => [a] -> a -> Bool
    hasElem ([QName] -> QName -> Bool) -> [QName] -> QName -> Bool
    forall a b. (a -> b) -> a -> b
    $ (Definition -> QName) -> [Definition] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Definition -> QName
    defName [Definition]
    defs
      getName :: Builtin PrimFun -> Maybe QName
    getName = \case
        Builtin Term
    t                 -> QName -> Maybe QName
    forall a. a -> Maybe a
    Just (QName -> Maybe QName) -> QName -> Maybe QName
    forall a b. (a -> b) -> a -> b
    $ Term -> QName
    getPrimName Term
    t
        Prim (PrimFun QName
    q Arity
    _ [Occurrence]
    _ [Arg Term] -> Arity -> ReduceM (Reduced MaybeReducedArgs Term)
    _)    -> QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q
        BuiltinRewriteRelations Set QName
    _ -> Maybe QName
    forall {a}. Maybe a
    Nothing

    -- | Definition bodies for primitive functions
    primBody :: MonadTCError m => PrimitiveId -> m HS.Exp
    primBody :: forall (m :: * -> *). MonadTCError m => PrimitiveId -> m Exp
    primBody PrimitiveId
    s = m Exp
    -> (m (Either String Exp) -> m Exp)
    -> Maybe (m (Either String Exp))
    -> m Exp
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m Exp
    unimplemented ((String -> Exp) -> Either String Exp -> Exp
    forall a b. (a -> b) -> Either a b -> b
    fromRight (Name -> Exp
    hsVarUQ (Name -> Exp) -> (String -> Name) -> String -> Exp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Name
    HS.Ident) (Either String Exp -> Exp) -> m (Either String Exp) -> m Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>) (Maybe (m (Either String Exp)) -> m Exp)
    -> Maybe (m (Either String Exp)) -> m Exp
    forall a b. (a -> b) -> a -> b
    $ PrimitiveId
    -> [(PrimitiveId, m (Either String Exp))]
    -> Maybe (m (Either String Exp))
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    List.lookup PrimitiveId
    s ([(PrimitiveId, m (Either String Exp))]
     -> Maybe (m (Either String Exp)))
    -> [(PrimitiveId, m (Either String Exp))]
    -> Maybe (m (Either String Exp))
    forall a b. (a -> b) -> a -> b
    $
      [
      -- Integer functions
        PrimitiveId
    PrimShowInteger      PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(Data.Text.pack . show :: Integer -> Data.Text.Text)"

      -- Levels
      , PrimitiveId
    PrimLevelZero        PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "()"
      , PrimitiveId
    PrimLevelSuc         PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(\\ _ -> ())"
      , PrimitiveId
    PrimLevelMax         PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(\\ _ _ -> ())"

      -- Natural number functions
      , PrimitiveId
    PrimNatPlus         PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall {m :: * -> *}. Monad m => String -> m String
    binNat String
    "(+)"
      , PrimitiveId
    PrimNatMinus        PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall {m :: * -> *}. Monad m => String -> m String
    binNat String
    "(\\ x y -> max 0 (x - y))"
      , PrimitiveId
    PrimNatTimes        PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall {m :: * -> *}. Monad m => String -> m String
    binNat String
    "(*)"
      , PrimitiveId
    PrimNatDivSucAux    PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall {m :: * -> *}. Monad m => String -> m String
    binNat4 String
    "(\\ k m n j -> k + div (max 0 $ n + m - j) (m + 1))"
      , PrimitiveId
    PrimNatModSucAux    PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall {m :: * -> *}. Monad m => String -> m String
    binNat4 String
    "(\\ k m n j -> if n > j then mod (n - j - 1) (m + 1) else (k + n))"
      , PrimitiveId
    PrimNatEquality     PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall {m :: * -> *}. Monad m => String -> m String
    relNat String
    "(==)"
      , PrimitiveId
    PrimNatLess         PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall {m :: * -> *}. Monad m => String -> m String
    relNat String
    "(<)"
      , PrimitiveId
    PrimShowNat         PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(Data.Text.pack . show :: Integer -> Data.Text.Text)"

      -- Machine word functions
      , PrimitiveId
    PrimWord64ToNat     PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.word64ToNat"
      , PrimitiveId
    PrimWord64FromNat   PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.word64FromNat"
      , PrimitiveId
    PrimWord64ToNatInjective   PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName

      -- Floating point functions
      , PrimitiveId
    PrimFloatEquality            PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleEq"
      , PrimitiveId
    PrimFloatInequality          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleLe"
      , PrimitiveId
    PrimFloatLess                PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleLt"
      , PrimitiveId
    PrimFloatIsInfinite          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(isInfinite :: Double -> Bool)"
      , PrimitiveId
    PrimFloatIsNaN               PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(isNaN :: Double -> Bool)"
      , PrimitiveId
    PrimFloatIsNegativeZero      PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(isNegativeZero :: Double -> Bool)"
      , PrimitiveId
    PrimFloatIsSafeInteger       PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.isSafeInteger"
      , PrimitiveId
    PrimFloatToWord64            PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleToWord64"
      , PrimitiveId
    PrimFloatToWord64Injective   PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName
      , PrimitiveId
    PrimNatToFloat               PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(MAlonzo.RTE.Float.intToDouble :: Integer -> Double)"
      , PrimitiveId
    PrimIntToFloat               PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(MAlonzo.RTE.Float.intToDouble :: Integer -> Double)"
      , PrimitiveId
    PrimFloatRound               PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleRound"
      , PrimitiveId
    PrimFloatFloor               PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleFloor"
      , PrimitiveId
    PrimFloatCeiling             PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleCeiling"
      , PrimitiveId
    PrimFloatToRatio             PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleToRatio"
      , PrimitiveId
    PrimRatioToFloat             PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.ratioToDouble"
      , PrimitiveId
    PrimFloatDecode              PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleDecode"
      , PrimitiveId
    PrimFloatEncode              PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleEncode"
      , PrimitiveId
    PrimShowFloat                PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(Data.Text.pack . show :: Double -> Data.Text.Text)"
      , PrimitiveId
    PrimFloatPlus                PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doublePlus"
      , PrimitiveId
    PrimFloatMinus               PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleMinus"
      , PrimitiveId
    PrimFloatTimes               PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleTimes"
      , PrimitiveId
    PrimFloatNegate              PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleNegate"
      , PrimitiveId
    PrimFloatDiv                 PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleDiv"
      , PrimitiveId
    PrimFloatPow                 PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doublePow"
      , PrimitiveId
    PrimFloatSqrt                PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleSqrt"
      , PrimitiveId
    PrimFloatExp                 PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleExp"
      , PrimitiveId
    PrimFloatLog                 PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleLog"
      , PrimitiveId
    PrimFloatSin                 PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleSin"
      , PrimitiveId
    PrimFloatCos                 PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleCos"
      , PrimitiveId
    PrimFloatTan                 PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleTan"
      , PrimitiveId
    PrimFloatASin                PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleASin"
      , PrimitiveId
    PrimFloatACos                PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleACos"
      , PrimitiveId
    PrimFloatATan                PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleATan"
      , PrimitiveId
    PrimFloatATan2               PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleATan2"
      , PrimitiveId
    PrimFloatSinh                PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleSinh"
      , PrimitiveId
    PrimFloatCosh                PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleCosh"
      , PrimitiveId
    PrimFloatTanh                PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleTanh"
      , PrimitiveId
    PrimFloatASinh               PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleASinh"
      , PrimitiveId
    PrimFloatACosh               PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleACosh"
      , PrimitiveId
    PrimFloatATanh               PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleATanh"

      -- Character functions
      , PrimitiveId
    PrimCharEquality     PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> String -> m String
    forall {m :: * -> *}. Monad m => String -> String -> m String
    rel String
    "(==)" String
    "Char"
      , PrimitiveId
    PrimIsLower          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isLower"
      , PrimitiveId
    PrimIsDigit          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isDigit"
      , PrimitiveId
    PrimIsAlpha          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isAlpha"
      , PrimitiveId
    PrimIsSpace          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isSpace"
      , PrimitiveId
    PrimIsAscii          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isAscii"
      , PrimitiveId
    PrimIsLatin1         PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isLatin1"
      , PrimitiveId
    PrimIsPrint          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isPrint"
      , PrimitiveId
    PrimIsHexDigit       PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isHexDigit"
      , PrimitiveId
    PrimToUpper          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.toUpper"
      , PrimitiveId
    PrimToLower          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.toLower"
      , PrimitiveId
    PrimCharToNat   PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(fromIntegral . fromEnum :: Char -> Integer)"
      , PrimitiveId
    PrimNatToChar   PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.natToChar"
      , PrimitiveId
    PrimShowChar    PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(Data.Text.pack . show :: Char -> Data.Text.Text)"
      , PrimitiveId
    PrimCharToNatInjective   PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName

      -- String functions
      , PrimitiveId
    PrimStringUncons     PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Text.uncons"
      , PrimitiveId
    PrimStringToList     PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Text.unpack"
      , PrimitiveId
    PrimStringFromList   PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Text.pack"
      , PrimitiveId
    PrimStringAppend     PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> String -> m String
    forall {m :: * -> *}. Monad m => String -> String -> m String
    binAsis String
    "Data.Text.append" String
    "Data.Text.Text"
      , PrimitiveId
    PrimStringEquality   PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> String -> m String
    forall {m :: * -> *}. Monad m => String -> String -> m String
    rel String
    "(==)" String
    "Data.Text.Text"
      , PrimitiveId
    PrimShowString       PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(Data.Text.pack . show :: Data.Text.Text -> Data.Text.Text)"
      , PrimitiveId
    PrimStringToListInjective   PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName
      , PrimitiveId
    PrimStringFromListInjective   PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName

      -- Reflection
      , PrimitiveId
    PrimQNameEquality     PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> String -> m String
    forall {m :: * -> *}. Monad m => String -> String -> m String
    rel String
    "(==)" String
    "MAlonzo.RTE.QName"
      , PrimitiveId
    PrimQNameLess         PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> String -> m String
    forall {m :: * -> *}. Monad m => String -> String -> m String
    rel String
    "(<)" String
    "MAlonzo.RTE.QName"
      , PrimitiveId
    PrimShowQName         PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Text.pack . MAlonzo.RTE.qnameString"
      , PrimitiveId
    PrimQNameFixity       PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.qnameFixity"
      , PrimitiveId
    PrimQNameToWord64s    PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\ qn -> (MAlonzo.RTE.nameId qn, MAlonzo.RTE.moduleId qn)"
      , PrimitiveId
    PrimQNameToWord64sInjective   PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName
      , PrimitiveId
    PrimMetaEquality      PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> String -> m String
    forall {m :: * -> *}. Monad m => String -> String -> m String
    rel String
    "(==)" String
    "(Integer, Integer)"
      , PrimitiveId
    PrimMetaLess          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> String -> m String
    forall {m :: * -> *}. Monad m => String -> String -> m String
    rel String
    "(<)" String
    "(Integer, Integer)"
      -- Should be kept in sync with version in `primitiveFunctions` in
      -- Agda.TypeChecking.Primitive
      , PrimitiveId
    PrimShowMeta          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\ (m, h) -> Data.Text.pack (\"_\" ++ show (m :: Integer) ++ \"@\" ++ show (h :: Integer))"
      -- Should be kept in sync with `metaToNat` in Agda.TypeChecking.Primitive
      , PrimitiveId
    PrimMetaToNat         PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\ (m, h) -> (h :: Integer) * 2^64 + (m :: Integer)"
      , PrimitiveId
    PrimMetaToNatInjective   PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName

      -- Seq
      , PrimitiveId
    PrimForce        PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\ _ _ _ _ x f -> f $! x"
      , PrimitiveId
    PrimForceLemma   PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName

      -- Lock universe
      , PrimitiveId
    PrimLockUniv PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "()"

      -- Erase
      , PrimitiveId
    PrimEraseEquality PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName

      -- Cubical
      , PrimitiveId
    PrimIMin          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(&&)"
      , PrimitiveId
    PrimIMax          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(||)"
      , PrimitiveId
    PrimINeg          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "not"
      , PrimitiveId
    PrimPartial       PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ x -> x"
      , PrimitiveId
    PrimPartialP      PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ x -> x"
      , PrimitiveId
    PrimPOr           PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ i _ _ x y -> if i then x else y"
      , PrimitiveId
    PrimComp          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ _ x -> x"
      , PrimitiveId
    PrimTrans         PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ x -> x"
      , PrimitiveId
    PrimHComp         PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ _ x -> x"
      , PrimitiveId
    PrimSubOut        PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ _ x -> x"
      , PrimitiveId
    Prim_glueU        PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ _ _ x -> x"
      , PrimitiveId
    Prim_unglueU      PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ _ x -> x"
      , PrimitiveId
    PrimFaceForall    PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
                                String
    "\\f -> f True == True && f False == True"
      ]
      where
      a
    x |-> :: a -> f a -> (a, f (Either a b))
    |-> f a
    s = (a
    x, a -> Either a b
    forall a b. a -> Either a b
    Left (a -> Either a b) -> f a -> f (Either a b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f a
    s)
      binNat :: String -> m String
    binNat  String
    op = String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> m String) -> String -> m String
    forall a b. (a -> b) -> a -> b
    $ [String] -> String -> String
    repl [String
    op] String
    "(<<0>> :: Integer -> Integer -> Integer)"
      binNat4 :: String -> m String
    binNat4 String
    op = String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> m String) -> String -> m String
    forall a b. (a -> b) -> a -> b
    $ [String] -> String -> String
    repl [String
    op] String
    "(<<0>> :: Integer -> Integer -> Integer -> Integer -> Integer)"
      binAsis :: String -> String -> m String
    binAsis String
    op String
    ty = String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> m String) -> String -> m String
    forall a b. (a -> b) -> a -> b
    $ [String] -> String -> String
    repl [String
    op, String -> String
    opty String
    ty] (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "((<<0>>) :: <<1>>)"
      rel' :: String -> String -> String -> m String
    rel' String
    toTy String
    op String
    ty = do
        String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> m String) -> String -> m String
    forall a b. (a -> b) -> a -> b
    $ [String] -> String -> String
    repl [String
    op, String
    ty, String
    toTy] (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $
          String
    "(\\ x y -> (<<0>> :: <<1>> -> <<1>> -> Bool) (<<2>> x) (<<2>> y))"
      relNat :: String -> m String
    relNat String
    op = do
        String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> m String) -> String -> m String
    forall a b. (a -> b) -> a -> b
    $ [String] -> String -> String
    repl [String
    op] (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $
          String
    "(<<0>> :: Integer -> Integer -> Bool)"
      rel :: String -> String -> m String
    rel String
    op String
    ty  = String -> String -> String -> m String
    forall {m :: * -> *}.
    Monad m =>
    String -> String -> String -> m String
    rel' String
    "" String
    op String
    ty
      opty :: String -> String
    opty String
    t = String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "->" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "->" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t
      unimplemented :: m Exp
    unimplemented = TypeError -> m Exp
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m Exp) -> TypeError -> m Exp
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    NotImplemented (PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId PrimitiveId
    s)

      hLam :: String -> Term -> Term
    hLam String
    x Term
    t = ArgInfo -> Abs Term -> Term
    Lam (Hiding -> ArgInfo -> ArgInfo
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    Hidden ArgInfo
    defaultArgInfo) (String -> Term -> Abs Term
    forall a. String -> a -> Abs a
    Abs String
    x Term
    t)
      nLam :: String -> Term -> Term
    nLam String
    x Term
    t = ArgInfo -> Abs Term -> Term
    Lam (Hiding -> ArgInfo -> ArgInfo
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    NotHidden ArgInfo
    defaultArgInfo) (String -> Term -> Abs Term
    forall a. String -> a -> Abs a
    Abs String
    x Term
    t)

    noCheckCover :: (HasBuiltins m, MonadReduce m) => QName -> m Bool
    noCheckCover :: forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    QName -> m Bool
    noCheckCover QName
    q = Bool -> Bool -> Bool
    (||) (Bool -> Bool -> Bool) -> m Bool -> m (Bool -> Bool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> BuiltinId -> m Bool
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    QName -> BuiltinId -> m Bool
    isBuiltin QName
    q BuiltinId
    builtinNat m (Bool -> Bool) -> m Bool -> m Bool
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> QName -> BuiltinId -> m Bool
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    QName -> BuiltinId -> m Bool
    isBuiltin QName
    q BuiltinId
    builtinInteger