{-# 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{}  } -> 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.
  Bool
isMainModule <- MaybeT
  (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO))) Bool
forall (m :: * -> *). ReadGHCModuleEnv m => m Bool
curIsMainModule
  MainFunctionDef
mainDef <- ReaderT
  GHCModuleEnv
  (StateT HsCompileState (TCMT IO))
  (Maybe MainFunctionDef)
-> MaybeT
     (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)))
     MainFunctionDef
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (ReaderT
   GHCModuleEnv
   (StateT HsCompileState (TCMT IO))
   (Maybe MainFunctionDef)
 -> MaybeT
      (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)))
      MainFunctionDef)
-> ReaderT
     GHCModuleEnv
     (StateT HsCompileState (TCMT IO))
     (Maybe MainFunctionDef)
-> MaybeT
     (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)))
     MainFunctionDef
forall a b. (a -> b) -> a -> b
$ Maybe MainFunctionDef
-> ReaderT
     GHCModuleEnv
     (StateT HsCompileState (TCMT IO))
     (Maybe MainFunctionDef)
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe MainFunctionDef
 -> ReaderT
      GHCModuleEnv
      (StateT HsCompileState (TCMT IO))
      (Maybe MainFunctionDef))
-> Maybe MainFunctionDef
-> ReaderT
     GHCModuleEnv
     (StateT HsCompileState (TCMT IO))
     (Maybe MainFunctionDef)
forall a b. (a -> b) -> a -> b
$ if Bool
isMainModule then Definition -> Maybe MainFunctionDef
asMainFunctionDef Definition
def else Maybe MainFunctionDef
forall {a}. Maybe a
Nothing
  TCM CheckedMainFunctionDef
-> MaybeT
     (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)))
     CheckedMainFunctionDef
forall a.
TCM a
-> MaybeT
     (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO))) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM CheckedMainFunctionDef
 -> MaybeT
      (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)))
      CheckedMainFunctionDef)
-> TCM CheckedMainFunctionDef
-> MaybeT
     (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)))
     CheckedMainFunctionDef
forall a b. (a -> b) -> a -> b
$ MainFunctionDef -> TCM CheckedMainFunctionDef
checkTypeOfMain' MainFunctionDef
mainDef

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

  -- Cubical
  , PrimitiveId
PrimIMin          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"(&&)"
  , PrimitiveId
PrimIMax          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"(||)"
  , PrimitiveId
PrimINeg          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"not"
  , PrimitiveId
PrimPartial       PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ x -> x"
  , PrimitiveId
PrimPartialP      PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ x -> x"
  , PrimitiveId
PrimPOr           PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ i _ _ x y -> if i then x else y"
  , PrimitiveId
PrimComp          PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ x -> x"
  , PrimitiveId
PrimTrans         PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ x -> x"
  , PrimitiveId
PrimHComp         PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ x -> x"
  , PrimitiveId
PrimSubOut        PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ x -> x"
  , PrimitiveId
Prim_glueU        PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ _ x -> x"
  , PrimitiveId
Prim_unglueU      PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ x -> x"
  , PrimitiveId
PrimFaceForall    PrimitiveId -> m String -> (PrimitiveId, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return
                            String
"\\f -> f True == True && f False == True"
  , PrimitiveId
PrimDepIMin       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 f -> if i then f () else False"
  , PrimitiveId
PrimIdFace        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
"\\_ _ _ _ -> fst"
  , PrimitiveId
PrimIdPath        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
"\\_ _ _ _ -> snd"
  , PrimitiveId
PrimIdElim        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 x y -> f (fst y) x (snd y)"
  ]
  where
  a
x |-> :: a -> f a -> (a, f (Either a b))
|-> f a
s = (a
x, a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> f a -> f (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
s)
  binNat :: String -> m String
binNat  String
op = String -> m String
forall 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