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 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.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 -> Maybe Projection
funProjection = Maybe Projection
Nothing } -> Maybe MainFunctionDef
perhaps
    Function{ funProjection :: Defn -> Maybe Projection
funProjection = Just{}  } -> 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
^. 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 HsModuleEnv (StateT HsCompileState TCM))
  CheckedMainFunctionDef
-> HsCompileM (Maybe CheckedMainFunctionDef)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT
   (ReaderT HsModuleEnv (StateT HsCompileState TCM))
   CheckedMainFunctionDef
 -> HsCompileM (Maybe CheckedMainFunctionDef))
-> MaybeT
     (ReaderT HsModuleEnv (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 HsModuleEnv (StateT HsCompileState TCM)) Bool
forall (m :: * -> *). ReadHsModuleEnv m => m Bool
curIsMainModule
  MainFunctionDef
mainDef <- ReaderT
  HsModuleEnv (StateT HsCompileState TCM) (Maybe MainFunctionDef)
-> MaybeT
     (ReaderT HsModuleEnv (StateT HsCompileState TCM)) MainFunctionDef
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (ReaderT
   HsModuleEnv (StateT HsCompileState TCM) (Maybe MainFunctionDef)
 -> MaybeT
      (ReaderT HsModuleEnv (StateT HsCompileState TCM)) MainFunctionDef)
-> ReaderT
     HsModuleEnv (StateT HsCompileState TCM) (Maybe MainFunctionDef)
-> MaybeT
     (ReaderT HsModuleEnv (StateT HsCompileState TCM)) MainFunctionDef
forall a b. (a -> b) -> a -> b
$ Maybe MainFunctionDef
-> ReaderT
     HsModuleEnv (StateT HsCompileState TCM) (Maybe MainFunctionDef)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe MainFunctionDef
 -> ReaderT
      HsModuleEnv (StateT HsCompileState TCM) (Maybe MainFunctionDef))
-> Maybe MainFunctionDef
-> ReaderT
     HsModuleEnv (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 HsModuleEnv (StateT HsCompileState TCM))
     CheckedMainFunctionDef
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM CheckedMainFunctionDef
 -> MaybeT
      (ReaderT HsModuleEnv (StateT HsCompileState TCM))
      CheckedMainFunctionDef)
-> TCM CheckedMainFunctionDef
-> MaybeT
     (ReaderT HsModuleEnv (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 (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
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
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
$ String -> QName -> Name
unqhname String
"d" (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. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, [ModuleName])] -> Map String [ModuleName])
-> [(String, [ModuleName])] -> Map String [ModuleName]
forall a b. (a -> b) -> a -> b
$ ([String] -> [ModuleName])
-> (String, [String]) -> (String, [ModuleName])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (String -> ModuleName
HS.ModuleName (String -> ModuleName) -> [String] -> [ModuleName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) ((String, [String]) -> (String, [ModuleName]))
-> [(String, [String])] -> [(String, [ModuleName])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    [ String
"CHAR"                       String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> [String
"Data.Char"]
    , 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
"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"]
    , String
"primFloatInequality"        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
"primFloatLess"              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
"primFloatToWord64"          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
"primFloatFloor"             String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> [String
"MAlonzo.RTE.Float"]
    , String
"primFloatCeiling"           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
"primRatioToFloat"           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"]
    ]
  |-> :: a -> b -> (a, b)
(|->) = (,)

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

xForPrim :: Map.Map String [a] -> BuiltinThings PrimFun -> [Definition] -> [a]
xForPrim :: Map String [a] -> BuiltinThings PrimFun -> [Definition] -> [a]
xForPrim Map String [a]
table BuiltinThings PrimFun
builtinThings [Definition]
defs =
  let qs :: Set QName
qs = [QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList ([QName] -> Set QName) -> [QName] -> Set QName
forall a b. (a -> b) -> a -> b
$ Definition -> QName
defName (Definition -> QName) -> [Definition] -> [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Definition]
defs
      bs :: [(String, Builtin PrimFun)]
bs = BuiltinThings PrimFun -> [(String, Builtin PrimFun)]
forall k a. Map k a -> [(k, a)]
Map.toList BuiltinThings PrimFun
builtinThings
      getName :: Builtin PrimFun -> QName
getName (Builtin Term
t)            = Term -> QName
getPrimName Term
t
      getName (Prim (PrimFun QName
q Arity
_ [Arg Term] -> Arity -> ReduceM (Reduced MaybeReducedArgs Term)
_)) = QName
q
  in
  [[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [a] -> Maybe [a] -> [a]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [a] -> [a]) -> Maybe [a] -> [a]
forall a b. (a -> b) -> a -> b
$ 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) <- [(String, Builtin PrimFun)]
bs, Builtin PrimFun -> QName
getName Builtin PrimFun
def QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set QName
qs ]


-- | Definition bodies for primitive functions
primBody :: MonadTCError m => String -> m HS.Exp
primBody :: 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return String
"erased"

  -- 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 (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 (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 (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 (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 (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 (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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return String
"erased"
  , 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return String
"erased"

  -- 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 (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 (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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return String
"erased"
  , 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 (m :: * -> *) a. Monad m => a -> m a
return String
"erased"

  -- 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 (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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return String
"erased"
  , 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"
  , 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"
  , 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 (m :: * -> *) a. Monad m => a -> m a
return String
"\\ x -> Data.Text.pack (\"_\" ++ show (x :: Integer))"
  , 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 (m :: * -> *) a. Monad m => a -> m a
return String
"(id :: Integer -> 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 (m :: * -> *) a. Monad m => a -> m a
return String
"erased"

  -- 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 (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 (m :: * -> *) a. Monad m => a -> m a
return String
"erased"

  -- 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 (m :: * -> *) a. Monad m => a -> m a
return String
"erased"
  ]
  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 (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 (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 (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 (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 (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 :: 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 (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 HsModuleEnv (StateT HsCompileState TCM) QName
-> HsCompileM String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> String -> ReaderT HsModuleEnv (StateT HsCompileState TCM) QName
bltQual String
b String
s