{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Compiler.MAlonzo.Primitives where

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

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

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

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

import Agda.Utils.Impossible

newtype MainFunctionDef = MainFunctionDef Definition

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

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

mainFunctionDefs :: Interface -> [MainFunctionDef]
mainFunctionDefs :: Interface -> [MainFunctionDef]
mainFunctionDefs Interface
i = forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ Definition -> Maybe MainFunctionDef
asMainFunctionDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Definition]
defs
  where
    defs :: [Definition]
defs = forall k v. HashMap k v -> [v]
HMap.elems forall a b. (a -> b) -> a -> b
$ Interface -> Signature
iSignature Interface
i forall o i. o -> Lens' o i -> i
^. 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 = forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ do
  -- Only indicate main functions in the main module.
  Bool
isMainModule <- forall (m :: * -> *). ReadGHCModuleEnv m => m Bool
curIsMainModule
  MainFunctionDef
mainDef <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ if Bool
isMainModule then Definition -> Maybe MainFunctionDef
asMainFunctionDef Definition
def else forall {a}. Maybe a
Nothing
  forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ MainFunctionDef -> TCM CheckedMainFunctionDef
checkTypeOfMain' MainFunctionDef
mainDef

checkTypeOfMain' :: MainFunctionDef -> TCM CheckedMainFunctionDef
checkTypeOfMain' :: MainFunctionDef -> TCM CheckedMainFunctionDef
checkTypeOfMain' m :: MainFunctionDef
m@(MainFunctionDef Definition
def) = MainFunctionDef -> Decl -> CheckedMainFunctionDef
CheckedMainFunctionDef MainFunctionDef
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    Def QName
io Elims
_ <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIO
    Type
ty <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
    case forall t a. Type'' t a -> a
unEl Type
ty of
      Def QName
d Elims
_ | QName
d forall a. Eq a => a -> a -> Bool
== QName
io -> forall (m :: * -> *) a. Monad m => a -> m a
return Decl
mainAlias
      Term
_                 -> do
        Doc
err <- forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The type of main should be" forall a. [a] -> [a] -> [a]
++
          [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
io] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
" A, for some A. The given type is" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ty]
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Doc
err
  where
    mainAlias :: Decl
mainAlias = [Match] -> Decl
HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
HS.Match Name
mainLHS [] Rhs
mainRHS Maybe Binds
emptyBinds ]
    mainLHS :: Name
mainLHS   = String -> Name
HS.Ident String
"main"
    mainRHS :: Rhs
mainRHS   = Exp -> Rhs
HS.UnGuardedRhs forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp
HS.App Exp
mazCoerce (QName -> Exp
HS.Var forall a b. (a -> b) -> a -> b
$ Name -> QName
HS.UnQual forall a b. (a -> b) -> a -> b
$ QName -> Name
dname forall a b. (a -> b) -> a -> b
$ Definition -> QName
defName Definition
def)

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

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

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

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


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

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

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

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

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

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

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

  -- Reflection
  , PrimitiveId
PrimQNameEquality     forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(==)" String
"MAlonzo.RTE.QName"
  , PrimitiveId
PrimQNameLess         forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(<)" String
"MAlonzo.RTE.QName"
  , PrimitiveId
PrimShowQName         forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Text.pack . MAlonzo.RTE.qnameString"
  , PrimitiveId
PrimQNameFixity       forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.qnameFixity"
  , PrimitiveId
PrimQNameToWord64s    forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\ qn -> (MAlonzo.RTE.nameId qn, MAlonzo.RTE.moduleId qn)"
  , PrimitiveId
PrimQNameToWord64sInjective   forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName
  , PrimitiveId
PrimMetaEquality      forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(==)" String
"(Integer, Integer)"
  , PrimitiveId
PrimMetaLess          forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> 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          forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> 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         forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\ (m, h) -> (h :: Integer) * 2^64 + (m :: Integer)"
  , PrimitiveId
PrimMetaToNatInjective   forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName

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

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

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

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

  hLam :: String -> Term -> Term
hLam String
x Term
t = ArgInfo -> Abs Term -> Term
Lam (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
defaultArgInfo) (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 (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden ArgInfo
defaultArgInfo) (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
(||) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
QName -> BuiltinId -> m Bool
isBuiltin QName
q BuiltinId
builtinNat forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
QName -> BuiltinId -> m Bool
isBuiltin QName
q BuiltinId
builtinInteger