{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Compiler.MAlonzo.Primitives where

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

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

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.List ( hasElem )
import Agda.Utils.Haskell.Syntax qualified as HS

import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Entrypoint (@main@)

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 = [Char]
"main" [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> [Char]
forall a. Pretty a => a -> [Char]
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
-> Getting
     (HashMap QName Definition) Signature (HashMap QName Definition)
-> HashMap QName Definition
forall s a. s -> Getting a s a -> a
^. Getting
  (HashMap QName Definition) Signature (HashMap QName Definition)
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   = [Char] -> Name
HS.Ident [Char]
"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)

---------------------------------------------------------------------------
-- * Primitives and builtins

-- | These builtins need a qualified import of "Data.Char".
charBuiltins :: [SomeBuiltin]
charBuiltins :: [SomeBuiltin]
charBuiltins =
  [ BuiltinId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin BuiltinId
BuiltinChar
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsAlpha
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsAscii
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsDigit
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsHexDigit
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsLatin1
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsLower
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsPrint
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsSpace
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimToLower
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimToUpper
  ]

-- | These builtins need a qualified import of "MAlonzo.RTE.Float".
floatBuiltins :: [SomeBuiltin]
floatBuiltins :: [SomeBuiltin]
floatBuiltins =
  [ PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatCeiling
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatDecode
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatEncode
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatEquality
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatFloor
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatInequality
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatIsSafeInteger
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatLess
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatRound
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatToRatio
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatToWord64
  , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimRatioToFloat
  ]

-- | Which builtins are actually used in the definitions?
usedBuiltins :: BuiltinThings -> [Definition] -> Set SomeBuiltin
usedBuiltins :: BuiltinThings -> [Definition] -> Set SomeBuiltin
usedBuiltins BuiltinThings
builtinThings [Definition]
defs = [SomeBuiltin] -> Set SomeBuiltin
forall a. Ord a => [a] -> Set a
Set.fromList
    [ SomeBuiltin
s
    | (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

-- ** Translating primitives

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


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

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

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

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

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

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

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

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

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

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

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

  -- Rewriting
  , PrimitiveId
PrimRewriteNoMatch PrimitiveId -> m [Char] -> (PrimitiveId, m (Either [Char] Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> [Char] -> m [Char]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
"\\ _ _ x -> x"

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

  hLam :: [Char] -> Term -> Term
hLam [Char]
x Term
t = ArgInfo -> Abs Term -> Term
Lam (Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
defaultArgInfo) ([Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
Abs [Char]
x Term
t)
  nLam :: [Char] -> Term -> Term
nLam [Char]
x Term
t = ArgInfo -> Abs Term -> Term
Lam (Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden ArgInfo
defaultArgInfo) ([Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
Abs [Char]
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