{-# 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.Lens
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 = String
"main" String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> String
forall a. Pretty a => a -> String
prettyShow (Name -> Name
nameConcrete (Name -> Name) -> (Definition -> Name) -> Definition -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName (QName -> Name) -> (Definition -> QName) -> Definition -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> QName
defName (Definition -> Name) -> Definition -> Name
forall a b. (a -> b) -> a -> b
$ Definition
d)  -- ignores the qualification!?
  perhaps :: Maybe MainFunctionDef
perhaps | Bool
isNamedMain = MainFunctionDef -> Maybe MainFunctionDef
forall a. a -> Maybe a
Just (MainFunctionDef -> Maybe MainFunctionDef)
-> MainFunctionDef -> Maybe MainFunctionDef
forall a b. (a -> b) -> a -> b
$ Definition -> MainFunctionDef
MainFunctionDef Definition
d
          | Bool
otherwise   = Maybe MainFunctionDef
forall {a}. Maybe a
no
  no :: Maybe a
no                    = Maybe a
forall {a}. Maybe a
Nothing

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

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

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

---------------------------------------------------------------------------
-- * 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 -> 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__


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

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

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

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

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

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

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

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

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

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

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

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

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

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