module Agda.Compiler.MAlonzo.Primitives where

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

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

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

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

import Agda.Utils.Impossible

newtype MainFunctionDef = MainFunctionDef Definition

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

-- Andreas, 2019-04-29, issue #3731: exclude certain kinds of names, like constructors.
-- TODO: Also only consider top-level definition (not buried inside a module).
asMainFunctionDef :: Definition -> Maybe MainFunctionDef
asMainFunctionDef :: Definition -> Maybe MainFunctionDef
asMainFunctionDef Definition
d = case (Definition -> Defn
theDef Definition
d) of
    Axiom{}                              -> Maybe MainFunctionDef
perhaps
    Function{ funProjection :: Defn -> 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' (HashMap QName Definition) Signature
-> HashMap QName Definition
forall o i. o -> Lens' i o -> i
^. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' (HashMap QName Definition) Signature
sigDefinitions

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

checkTypeOfMain' :: MainFunctionDef -> TCM CheckedMainFunctionDef
checkTypeOfMain' :: MainFunctionDef -> TCM CheckedMainFunctionDef
checkTypeOfMain' m :: MainFunctionDef
m@(MainFunctionDef Definition
def) = MainFunctionDef -> Decl -> CheckedMainFunctionDef
CheckedMainFunctionDef MainFunctionDef
m (Decl -> CheckedMainFunctionDef)
-> TCMT IO Decl -> TCM CheckedMainFunctionDef
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    Def QName
io Elims
_ <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIO
    Type
ty <- Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
    case Type -> Term
forall t a. Type'' t a -> a
unEl Type
ty of
      Def QName
d Elims
_ | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
io -> Decl -> TCMT IO Decl
forall 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 String ModuleName
-> BuiltinThings PrimFun -> [Definition] -> [ModuleName]
forall a.
Map String a -> BuiltinThings PrimFun -> [Definition] -> [a]
xForPrim Map String ModuleName
table BuiltinThings PrimFun
builtinThings [Definition]
defs [ModuleName] -> [ModuleName] -> [ModuleName]
forall a. [a] -> [a] -> [a]
++ [String -> ModuleName
HS.ModuleName String
"Data.Text"]
  where
  table :: Map String ModuleName
table = [(String, ModuleName)] -> Map String ModuleName
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList ([(String, ModuleName)] -> Map String ModuleName)
-> [(String, ModuleName)] -> Map String ModuleName
forall a b. (a -> b) -> a -> b
$ ((String, String) -> (String, ModuleName))
-> [(String, String)] -> [(String, ModuleName)]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> ModuleName) -> (String, String) -> (String, ModuleName)
forall 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)
    -- KEEP THIS LIST IN ALPHABETICAL ORDER!
    -- Otherwise, Map.fromDistinctAscList will produce garbage.
    [ String
"CHAR"                       String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primFloatCeiling"           String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatDecode"            String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatEncode"            String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatEquality"          String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatFloor"             String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatInequality"        String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatIsSafeInteger"     String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatLess"              String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatRound"             String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatToRatio"           String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatToWord64"          String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primIsAlpha"                String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsAscii"                String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsDigit"                String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsHexDigit"             String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsLatin1"               String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsLower"                String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsPrint"                String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsSpace"                String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primRatioToFloat"           String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primToLower"                String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primToUpper"                String -> String -> (String, String)
forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    ]
  |-> :: a -> b -> (a, b)
(|->) = (,)

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

xForPrim :: Map String a -> BuiltinThings PrimFun -> [Definition] -> [a]
xForPrim :: forall a.
Map String a -> BuiltinThings PrimFun -> [Definition] -> [a]
xForPrim Map String a
table BuiltinThings PrimFun
builtinThings [Definition]
defs = [Maybe a] -> [a]
forall a. [Maybe a] -> [a]
catMaybes
    [ String -> Map String a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
s Map String a
table
    | (String
s, Builtin PrimFun
def) <- BuiltinThings PrimFun -> [(String, Builtin PrimFun)]
forall k a. Map k a -> [(k, a)]
Map.toList BuiltinThings PrimFun
builtinThings
    , 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
_ [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 => String -> m HS.Exp
primBody :: forall (m :: * -> *). MonadTCError m => String -> m Exp
primBody String
s = m Exp
-> (m (Either String Exp) -> m Exp)
-> Maybe (m (Either String Exp))
-> m Exp
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Exp
unimplemented ((String -> Exp) -> Either String Exp -> Exp
forall a b. (a -> b) -> Either a b -> b
fromRight (Name -> Exp
hsVarUQ (Name -> Exp) -> (String -> Name) -> String -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
HS.Ident) (Either String Exp -> Exp) -> m (Either String Exp) -> m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (m (Either String Exp)) -> m Exp)
-> Maybe (m (Either String Exp)) -> m Exp
forall a b. (a -> b) -> a -> b
$
             String
-> [(String, m (Either String Exp))]
-> Maybe (m (Either String Exp))
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup String
s ([(String, m (Either String Exp))]
 -> Maybe (m (Either String Exp)))
-> [(String, m (Either String Exp))]
-> Maybe (m (Either String Exp))
forall a b. (a -> b) -> a -> b
$
  [
  -- Integer functions
    String
"primIntegerPlus"    String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> m String
forall {m :: * -> *}. Monad m => String -> String -> m String
binAsis String
"(+)" String
"Integer"
  , String
"primIntegerMinus"   String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> m String
forall {m :: * -> *}. Monad m => String -> String -> m String
binAsis String
"(-)" String
"Integer"
  , String
"primIntegerTimes"   String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> m String
forall {m :: * -> *}. Monad m => String -> String -> m String
binAsis String
"(*)" String
"Integer"
  , String
"primIntegerDiv"     String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> m String
forall {m :: * -> *}. Monad m => String -> String -> m String
binAsis String
"div" String
"Integer"
  , String
"primIntegerMod"     String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> m String
forall {m :: * -> *}. Monad m => String -> String -> m String
binAsis String
"mod" String
"Integer"
  , String
"primIntegerEquality"String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> m String
forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(==)" String
"Integer"
  , String
"primIntegerLess"    String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> m String
forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(<)"  String
"Integer"
  , String
"primIntegerAbs"     String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"(abs :: Integer -> Integer)"
  , String
"primNatToInteger"   String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"(id :: Integer -> Integer)"
  , String
"primShowInteger"    String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"(Data.Text.pack . show :: Integer -> Data.Text.Text)"

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

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

  -- Natural number functions
  , String
"primNatPlus"      String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall {m :: * -> *}. Monad m => String -> m String
binNat String
"(+)"
  , String
"primNatMinus"     String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall {m :: * -> *}. Monad m => String -> m String
binNat String
"(\\ x y -> max 0 (x - y))"
  , String
"primNatTimes"     String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall {m :: * -> *}. Monad m => String -> m String
binNat String
"(*)"
  , String
"primNatDivSucAux" String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall {m :: * -> *}. Monad m => String -> m String
binNat4 String
"(\\ k m n j -> k + div (max 0 $ n + m - j) (m + 1))"
  , String
"primNatModSucAux" String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall {m :: * -> *}. Monad m => String -> m String
binNat4 String
"(\\ k m n j -> if n > j then mod (n - j - 1) (m + 1) else (k + n))"
  , String
"primNatEquality"  String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall {m :: * -> *}. Monad m => String -> m String
relNat String
"(==)"
  , String
"primNatLess"      String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall {m :: * -> *}. Monad m => String -> m String
relNat String
"(<)"
  , String
"primShowNat"      String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall 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
  , String
"primWord64ToNat"   String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.word64ToNat"
  , String
"primWord64FromNat" String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.word64FromNat"
  , String
"primWord64ToNatInjective" String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName

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

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

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

  -- Reflection
  , String
"primQNameEquality"   String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> m String
forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(==)" String
"MAlonzo.RTE.QName"
  , String
"primQNameLess"       String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> m String
forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(<)" String
"MAlonzo.RTE.QName"
  , String
"primShowQName"       String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Text.pack . MAlonzo.RTE.qnameString"
  , String
"primQNameFixity"     String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.qnameFixity"
  , String
"primQNameToWord64s"  String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\ qn -> (MAlonzo.RTE.nameId qn, MAlonzo.RTE.moduleId qn)"
  , String
"primQNameToWord64sInjective" String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName
  , String
"primMetaEquality"    String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> m String
forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(==)" String
"(Integer, Integer)"
  , String
"primMetaLess"        String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> m String
forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(<)" String
"(Integer, Integer)"
  -- Should be kept in sync with version in `primitiveFunctions` in
  -- Agda.TypeChecking.Primitive
  , String
"primShowMeta"        String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall 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
  , String
"primMetaToNat"       String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\ (m, h) -> (h :: Integer) * 2^64 + (m :: Integer)"
  , String
"primMetaToNatInjective" String -> m String -> (String, m (Either String Exp))
forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName

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

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

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

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

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

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

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