    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.Set as Set
    import qualified Data.HashMap.Strict as HMap
    import Data.Maybe
    import qualified Data.Text as T

    import Agda.Compiler.Common
    import Agda.Compiler.ToTreeless
    import Agda.Compiler.MAlonzo.Misc
    import Agda.Compiler.MAlonzo.Pretty
    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Treeless
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Primitive
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Pretty

    import Agda.Utils.Either
    import Agda.Utils.Lens
    import Agda.Utils.Pretty (prettyShow)
    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 -> Maybe Projection
    funProjection = Maybe Projection
    Nothing } -> Maybe MainFunctionDef
    perhaps
        Function{ funProjection :: Defn -> Maybe Projection
    funProjection = Just{}  } -> 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' (HashMap QName Definition) Signature
    -> HashMap QName Definition
    forall o i. o -> Lens' i o -> i
    ^. Lens' (HashMap QName Definition) Signature
    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 TCM))
      CheckedMainFunctionDef
    -> HsCompileM (Maybe CheckedMainFunctionDef)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT
       (ReaderT GHCModuleEnv (StateT HsCompileState TCM))
       CheckedMainFunctionDef
     -> HsCompileM (Maybe CheckedMainFunctionDef))
    -> MaybeT
         (ReaderT GHCModuleEnv (StateT HsCompileState TCM))
         CheckedMainFunctionDef
    -> HsCompileM (Maybe CheckedMainFunctionDef)
    forall a b. (a -> b) -> a -> b
    $ do
      -- Only indicate main functions in the main module.
      Bool
    isMainModule <- MaybeT (ReaderT GHCModuleEnv (StateT HsCompileState TCM)) Bool
    forall (m :: * -> *). ReadGHCModuleEnv m => m Bool
    curIsMainModule
      MainFunctionDef
    mainDef <- ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (Maybe MainFunctionDef)
    -> MaybeT
         (ReaderT GHCModuleEnv (StateT HsCompileState TCM)) MainFunctionDef
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (ReaderT
       GHCModuleEnv (StateT HsCompileState TCM) (Maybe MainFunctionDef)
     -> MaybeT
          (ReaderT GHCModuleEnv (StateT HsCompileState TCM)) MainFunctionDef)
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (Maybe MainFunctionDef)
    -> MaybeT
         (ReaderT GHCModuleEnv (StateT HsCompileState TCM)) MainFunctionDef
    forall a b. (a -> b) -> a -> b
    $ Maybe MainFunctionDef
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (Maybe MainFunctionDef)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe MainFunctionDef
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (Maybe MainFunctionDef))
    -> Maybe MainFunctionDef
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (Maybe MainFunctionDef)
    forall a b. (a -> b) -> a -> b
    $ if Bool
    isMainModule then Definition -> Maybe MainFunctionDef
    asMainFunctionDef Definition
    def else Maybe MainFunctionDef
    forall {a}. Maybe a
    Nothing
      TCM CheckedMainFunctionDef
    -> MaybeT
         (ReaderT GHCModuleEnv (StateT HsCompileState TCM))
         CheckedMainFunctionDef
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM CheckedMainFunctionDef
     -> MaybeT
          (ReaderT GHCModuleEnv (StateT HsCompileState TCM))
          CheckedMainFunctionDef)
    -> TCM CheckedMainFunctionDef
    -> MaybeT
         (ReaderT GHCModuleEnv (StateT HsCompileState TCM))
         CheckedMainFunctionDef
    forall a b. (a -> b) -> a -> b
    $ MainFunctionDef -> TCM CheckedMainFunctionDef
    checkTypeOfMain' MainFunctionDef
    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 QName
    io Elims
    _ <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIO
        Type
    ty <- Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Type -> TCMT IO Type) -> Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type
    defType Definition
    def
        case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    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 (m :: * -> *) a. Monad m => a -> m a
    return Decl
    mainAlias
          Term
    _                 -> do
            Doc
    err <- [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
              String -> [TCMT IO Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "The type of main should be" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++
              [QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    io] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++ String -> [TCMT IO Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    " A, for some A. The given type is" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    ty]
            TypeError -> TCMT IO Decl
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO Decl) -> TypeError -> TCMT IO Decl
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    forall a b. (a -> b) -> a -> b
    $ Doc -> String
    forall a. Show a => a -> String
    show Doc
    err
      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 PrimFun -> [Definition] -> [HS.ModuleName]
    importsForPrim :: BuiltinThings PrimFun -> [Definition] -> [ModuleName]
    importsForPrim BuiltinThings PrimFun
    builtinThings [Definition]
    defs = Map String ModuleName
    -> BuiltinThings PrimFun -> [Definition] -> [ModuleName]
    forall a.
    Map String a -> BuiltinThings PrimFun -> [Definition] -> [a]
    xForPrim Map String ModuleName
    table BuiltinThings PrimFun
    builtinThings [Definition]
    defs [ModuleName] -> [ModuleName] -> [ModuleName]
    forall a. [a] -> [a] -> [a]
    ++ [String -> ModuleName
    HS.ModuleName String
    "Data.Text"]
      where
      table :: Map String ModuleName
    table = [(String, ModuleName)] -> Map String ModuleName
    forall k a. [(k, a)] -> Map k a
    Map.fromDistinctAscList ([(String, ModuleName)] -> Map String ModuleName)
    -> [(String, ModuleName)] -> Map String ModuleName
    forall a b. (a -> b) -> a -> b
    $ ((String, String) -> (String, ModuleName))
    -> [(String, String)] -> [(String, ModuleName)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((String -> ModuleName) -> (String, String) -> (String, ModuleName)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second String -> ModuleName
    HS.ModuleName)
        -- KEEP THIS LIST IN ALPHABETICAL ORDER!
        -- Otherwise, Map.fromDistinctAscList will produce garbage.
        [ String
    "CHAR"                       String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , String
    "primFloatCeiling"           String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , String
    "primFloatDecode"            String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , String
    "primFloatEncode"            String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , String
    "primFloatEquality"          String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , String
    "primFloatFloor"             String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , String
    "primFloatInequality"        String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , String
    "primFloatIsSafeInteger"     String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , String
    "primFloatLess"              String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , String
    "primFloatRound"             String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , String
    "primFloatToRatio"           String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , String
    "primFloatToWord64"          String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , String
    "primIsAlpha"                String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , String
    "primIsAscii"                String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , String
    "primIsDigit"                String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , String
    "primIsHexDigit"             String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , String
    "primIsLatin1"               String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , String
    "primIsLower"                String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , String
    "primIsPrint"                String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , String
    "primIsSpace"                String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , String
    "primRatioToFloat"           String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "MAlonzo.RTE.Float"
        , String
    "primToLower"                String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        , String
    "primToUpper"                String -> String -> (String, String)
    forall {a} {b}. a -> b -> (a, b)
    |-> String
    "Data.Char"
        ]
      |-> :: a -> b -> (a, b)
    (|->) = (,)

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

    xForPrim :: Map String a -> BuiltinThings PrimFun -> [Definition] -> [a]
    xForPrim :: forall a.
    Map String a -> BuiltinThings PrimFun -> [Definition] -> [a]
    xForPrim Map String a
    table BuiltinThings PrimFun
    builtinThings [Definition]
    defs = [Maybe a] -> [a]
    forall a. [Maybe a] -> [a]
    catMaybes
        [ String -> Map String a -> Maybe a
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup String
    s Map String a
    table
        | (String
    s, Builtin PrimFun
    def) <- BuiltinThings PrimFun -> [(String, Builtin PrimFun)]
    forall k a. Map k a -> [(k, a)]
    Map.toList BuiltinThings PrimFun
    builtinThings
        , Builtin PrimFun -> QName
    getName Builtin PrimFun
    def QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set QName
    qs
        ]
      where
      qs :: Set QName
    qs = [QName] -> Set QName
    forall a. Ord a => [a] -> Set a
    Set.fromList ([QName] -> Set QName) -> [QName] -> Set QName
    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 -> QName
    getName (Builtin Term
    t)            = Term -> QName
    getPrimName Term
    t
      getName (Prim (PrimFun QName
    q Arity
    _ [Arg Term] -> Arity -> ReduceM (Reduced MaybeReducedArgs Term)
    _)) = QName
    q

    -- | Definition bodies for primitive functions
    primBody :: MonadTCError m => String -> m HS.Exp
    primBody :: forall (m :: * -> *). MonadTCError m => String -> m Exp
    primBody String
    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
    $
                 String
    -> [(String, m (Either String Exp))]
    -> Maybe (m (Either String Exp))
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    List.lookup String
    s ([(String, m (Either String Exp))]
     -> Maybe (m (Either String Exp)))
    -> [(String, m (Either String Exp))]
    -> Maybe (m (Either String Exp))
    forall a b. (a -> b) -> a -> b
    $
      [
      -- Integer functions
        String
    "primIntegerPlus"    String -> m String -> (String, 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
    "(+)" String
    "Integer"
      , String
    "primIntegerMinus"   String -> m String -> (String, 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
    "(-)" String
    "Integer"
      , String
    "primIntegerTimes"   String -> m String -> (String, 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
    "(*)" String
    "Integer"
      , String
    "primIntegerDiv"     String -> m String -> (String, 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
    "div" String
    "Integer"
      , String
    "primIntegerMod"     String -> m String -> (String, 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
    "mod" String
    "Integer"
      , String
    "primIntegerEquality"String -> m String -> (String, 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"
      , String
    "primIntegerLess"    String -> m String -> (String, 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"
      , String
    "primIntegerAbs"     String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(abs :: Integer -> Integer)"
      , String
    "primNatToInteger"   String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(id :: Integer -> Integer)"
      , String
    "primShowInteger"    String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(Data.Text.pack . show :: Integer -> Data.Text.Text)"

      -- Levels
      , String
    "primLevelZero"   String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "()"
      , String
    "primLevelSuc"    String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(\\ _ -> ())"
      , String
    "primLevelMax"    String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(\\ _ _ -> ())"

      -- Sorts
      , String
    "primSetOmega"    String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "()"
      , String
    "primStrictSet"   String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\ _ -> ()"

      -- Natural number functions
      , String
    "primNatPlus"      String -> m String -> (String, 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
    "(+)"
      , String
    "primNatMinus"     String -> m String -> (String, 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))"
      , String
    "primNatTimes"     String -> m String -> (String, 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
    "(*)"
      , String
    "primNatDivSucAux" String -> m String -> (String, 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))"
      , String
    "primNatModSucAux" String -> m String -> (String, 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))"
      , String
    "primNatEquality"  String -> m String -> (String, 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
    "(==)"
      , String
    "primNatLess"      String -> m String -> (String, 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
    "(<)"
      , String
    "primShowNat"      String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(Data.Text.pack . show :: Integer -> Data.Text.Text)"

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

      -- Floating point functions
      , String
    "primFloatEquality"          String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleEq"
      , String
    "primFloatInequality"        String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleLe"
      , String
    "primFloatLess"              String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleLt"
      , String
    "primFloatIsInfinite"        String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(isInfinite :: Double -> Bool)"
      , String
    "primFloatIsNaN"             String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(isNaN :: Double -> Bool)"
      , String
    "primFloatIsNegativeZero"    String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(isNegativeZero :: Double -> Bool)"
      , String
    "primFloatIsSafeInteger"     String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.isSafeInteger"
      , String
    "primFloatToWord64"          String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleToWord64"
      , String
    "primFloatToWord64Injective" String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName
      , String
    "primNatToFloat"             String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(MAlonzo.RTE.Float.intToDouble :: Integer -> Double)"
      , String
    "primIntToFloat"             String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(MAlonzo.RTE.Float.intToDouble :: Integer -> Double)"
      , String
    "primFloatRound"             String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleRound"
      , String
    "primFloatFloor"             String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleFloor"
      , String
    "primFloatCeiling"           String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleCeiling"
      , String
    "primFloatToRatio"           String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleToRatio"
      , String
    "primRatioToFloat"           String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.ratioToDouble"
      , String
    "primFloatDecode"            String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleDecode"
      , String
    "primFloatEncode"            String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleEncode"
      , String
    "primShowFloat"              String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(Data.Text.pack . show :: Double -> Data.Text.Text)"
      , String
    "primFloatPlus"              String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doublePlus"
      , String
    "primFloatMinus"             String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleMinus"
      , String
    "primFloatTimes"             String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleTimes"
      , String
    "primFloatNegate"            String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleNegate"
      , String
    "primFloatDiv"               String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleDiv"
      , String
    "primFloatPow"               String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doublePow"
      , String
    "primFloatSqrt"              String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleSqrt"
      , String
    "primFloatExp"               String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleExp"
      , String
    "primFloatLog"               String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleLog"
      , String
    "primFloatSin"               String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleSin"
      , String
    "primFloatCos"               String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleCos"
      , String
    "primFloatTan"               String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleTan"
      , String
    "primFloatASin"              String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleASin"
      , String
    "primFloatACos"              String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleACos"
      , String
    "primFloatATan"              String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleATan"
      , String
    "primFloatATan2"             String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleATan2"
      , String
    "primFloatSinh"              String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleSinh"
      , String
    "primFloatCosh"              String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleCosh"
      , String
    "primFloatTanh"              String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleTanh"
      , String
    "primFloatASinh"             String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleASinh"
      , String
    "primFloatACosh"             String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleACosh"
      , String
    "primFloatATanh"             String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.Float.doubleATanh"

      -- Character functions
      , String
    "primCharEquality"   String -> m String -> (String, 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"
      , String
    "primIsLower"        String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isLower"
      , String
    "primIsDigit"        String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isDigit"
      , String
    "primIsAlpha"        String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isAlpha"
      , String
    "primIsSpace"        String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isSpace"
      , String
    "primIsAscii"        String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isAscii"
      , String
    "primIsLatin1"       String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isLatin1"
      , String
    "primIsPrint"        String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isPrint"
      , String
    "primIsHexDigit"     String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.isHexDigit"
      , String
    "primToUpper"        String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.toUpper"
      , String
    "primToLower"        String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Char.toLower"
      , String
    "primCharToNat" String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(fromIntegral . fromEnum :: Char -> Integer)"
      , String
    "primNatToChar" String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.natToChar"
      , String
    "primShowChar"  String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(Data.Text.pack . show :: Char -> Data.Text.Text)"
      , String
    "primCharToNatInjective" String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName

      -- String functions
      , String
    "primStringUncons"   String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Text.uncons"
      , String
    "primStringToList"   String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Text.unpack"
      , String
    "primStringFromList" String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Text.pack"
      , String
    "primStringAppend"   String -> m String -> (String, 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"
      , String
    "primStringEquality" String -> m String -> (String, 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"
      , String
    "primShowString"     String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(Data.Text.pack . show :: Data.Text.Text -> Data.Text.Text)"
      , String
    "primStringToListInjective" String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName
      , String
    "primStringFromListInjective" String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName

      -- Reflection
      , String
    "primQNameEquality"   String -> m String -> (String, 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"
      , String
    "primQNameLess"       String -> m String -> (String, 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"
      , String
    "primShowQName"       String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "Data.Text.pack . MAlonzo.RTE.qnameString"
      , String
    "primQNameFixity"     String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "MAlonzo.RTE.qnameFixity"
      , String
    "primQNameToWord64s"  String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\ qn -> (MAlonzo.RTE.nameId qn, MAlonzo.RTE.moduleId qn)"
      , String
    "primQNameToWord64sInjective" String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName
      , String
    "primMetaEquality"    String -> m String -> (String, 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"
      , String
    "primMetaLess"        String -> m String -> (String, 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"
      , String
    "primShowMeta"        String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\ x -> Data.Text.pack (\"_\" ++ show (x :: Integer))"
      , String
    "primMetaToNat"       String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(id :: Integer -> Integer)"
      , String
    "primMetaToNatInjective" String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    mazErasedName

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

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

      -- Cubical
      , String
    builtinIMin       String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(&&)"
      , String
    builtinIMax       String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "(||)"
      , String
    builtinINeg       String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "not"
      , String
    "primPartial"     String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ x -> x"
      , String
    "primPartialP"    String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ x -> x"
      , String
    builtinPOr        String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ i _ _ x y -> if i then x else y"
      , String
    builtinComp       String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ _ x -> x"
      , String
    builtinTrans      String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ x -> x"
      , String
    builtinHComp      String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ _ x -> x"
      , String
    builtinSubOut     String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ _ x -> x"
      , String
    builtin_glueU     String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ _ _ x -> x"
      , String
    builtin_unglueU   String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ _ x -> x"
      , String
    builtinFaceForall String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return
                                String
    "\\f -> f True == True && f False == True"
      , String
    "primDepIMin"     String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\i f -> if i then f () else False"
      , String
    "primIdFace"      String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ _ -> fst"
      , String
    "primIdPath"      String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ _ -> snd"
      , String
    "primIdJ"         String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "\\_ _ _ _ _ x _ _ -> x"
      , String
    builtinIdElim     String -> m String -> (String, m (Either String Exp))
    forall {f :: * -> *} {a} {a} {b}.
    Functor f =>
    a -> f a -> (a, f (Either a b))
    |-> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return
                                String
    "\\_ _ _ _ _ f x y -> f (fst y) x (snd y)"
      ]
      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 (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 (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 (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 (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 (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 String
    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 -> String -> m Bool
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    QName -> String -> m Bool
    isBuiltin QName
    q String
    builtinNat m (Bool -> Bool) -> m Bool -> m Bool
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> QName -> String -> m Bool
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    QName -> String -> m Bool
    isBuiltin QName
    q String
    builtinInteger

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

    bltQual' :: String -> String -> HsCompileM String
    bltQual' :: String -> String -> HsCompileM String
    bltQual' String
    b String
    s = QName -> String
    forall a. Pretty a => a -> String
    prettyPrint (QName -> String)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    -> HsCompileM String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String
    -> String -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    bltQual String
    b String
    s