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

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

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

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

-- | Haskell modules to be imported for BUILT-INs
importsForPrim :: BuiltinThings PrimFun -> [Definition] -> [HS.ModuleName]
importsForPrim :: BuiltinThings PrimFun -> [Definition] -> [ModuleName]
importsForPrim BuiltinThings PrimFun
builtinThings [Definition]
defs = forall a.
Map String a -> BuiltinThings PrimFun -> [Definition] -> [a]
xForPrim Map String ModuleName
table BuiltinThings PrimFun
builtinThings [Definition]
defs forall a. [a] -> [a] -> [a]
++ [String -> ModuleName
HS.ModuleName String
"Data.Text"]
  where
  table :: Map String ModuleName
table = forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second String -> ModuleName
HS.ModuleName)
    -- KEEP THIS LIST IN ALPHABETICAL ORDER!
    -- Otherwise, Map.fromDistinctAscList will produce garbage.
    [ String
"CHAR"                       forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primFloatCeiling"           forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatDecode"            forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatEncode"            forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatEquality"          forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatFloor"             forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatInequality"        forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatIsSafeInteger"     forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatLess"              forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatRound"             forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatToRatio"           forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primFloatToWord64"          forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primIsAlpha"                forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsAscii"                forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsDigit"                forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsHexDigit"             forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsLatin1"               forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsLower"                forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsPrint"                forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primIsSpace"                forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primRatioToFloat"           forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
    , String
"primToLower"                forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
    , String
"primToUpper"                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 = forall a. [Maybe a] -> [a]
catMaybes
    [ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
s Map String a
table
    | (String
s, Builtin PrimFun
def) <- forall k a. Map k a -> [(k, a)]
Map.toList BuiltinThings PrimFun
builtinThings
    , forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False QName -> Bool
elemDefs forall a b. (a -> b) -> a -> b
$ Builtin PrimFun -> Maybe QName
getName Builtin PrimFun
def
    ]
  where
  elemDefs :: QName -> Bool
elemDefs = forall a. Ord a => [a] -> a -> Bool
hasElem forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Definition -> QName
defName [Definition]
defs
  getName :: Builtin PrimFun -> Maybe QName
getName = \case
    Builtin Term
t                 -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term -> QName
getPrimName Term
t
    Prim (PrimFun QName
q Arity
_ [Arg Term] -> Arity -> ReduceM (Reduced MaybeReducedArgs Term)
_)      -> forall a. a -> Maybe a
Just QName
q
    BuiltinRewriteRelations Set QName
_ -> forall {a}. Maybe a
Nothing


-- | Definition bodies for primitive functions
primBody :: MonadTCError m => String -> m HS.Exp
primBody :: forall (m :: * -> *). MonadTCError m => String -> m Exp
primBody String
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Exp
unimplemented (forall a b. (a -> b) -> Either a b -> b
fromRight (Name -> Exp
hsVarUQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
HS.Ident) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall a b. (a -> b) -> a -> b
$
             forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup String
s forall a b. (a -> b) -> a -> b
$
  [
  -- Integer functions
    String
"primIntegerPlus"    forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
binAsis String
"(+)" String
"Integer"
  , String
"primIntegerMinus"   forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
binAsis String
"(-)" String
"Integer"
  , String
"primIntegerTimes"   forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
binAsis String
"(*)" String
"Integer"
  , String
"primIntegerDiv"     forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
binAsis String
"div" String
"Integer"
  , String
"primIntegerMod"     forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
binAsis String
"mod" String
"Integer"
  , String
"primIntegerEquality"forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(==)" String
"Integer"
  , String
"primIntegerLess"    forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(<)"  String
"Integer"
  , String
"primIntegerAbs"     forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(abs :: Integer -> Integer)"
  , String
"primNatToInteger"   forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(id :: Integer -> Integer)"
  , String
"primShowInteger"    forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(Data.Text.pack . show :: Integer -> Data.Text.Text)"

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

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

  -- Natural number functions
  , String
"primNatPlus"      forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
binNat String
"(+)"
  , String
"primNatMinus"     forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
binNat String
"(\\ x y -> max 0 (x - y))"
  , String
"primNatTimes"     forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
binNat String
"(*)"
  , String
"primNatDivSucAux" forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
binNat4 String
"(\\ k m n j -> k + div (max 0 $ n + m - j) (m + 1))"
  , String
"primNatModSucAux" forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
binNat4 String
"(\\ k m n j -> if n > j then mod (n - j - 1) (m + 1) else (k + n))"
  , String
"primNatEquality"  forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
relNat String
"(==)"
  , String
"primNatLess"      forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
relNat String
"(<)"
  , String
"primShowNat"      forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(Data.Text.pack . show :: Integer -> Data.Text.Text)"

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

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

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

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

  -- Reflection
  , String
"primQNameEquality"   forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(==)" String
"MAlonzo.RTE.QName"
  , String
"primQNameLess"       forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(<)" String
"MAlonzo.RTE.QName"
  , String
"primShowQName"       forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Text.pack . MAlonzo.RTE.qnameString"
  , String
"primQNameFixity"     forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.qnameFixity"
  , String
"primQNameToWord64s"  forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\ qn -> (MAlonzo.RTE.nameId qn, MAlonzo.RTE.moduleId qn)"
  , String
"primQNameToWord64sInjective" forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName
  , String
"primMetaEquality"    forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(==)" String
"Integer"
  , String
"primMetaLess"        forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(<)" String
"Integer"
  , String
"primShowMeta"        forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\ x -> Data.Text.pack (\"_\" ++ show (x :: Integer))"
  , String
"primMetaToNat"       forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(id :: Integer -> Integer)"
  , String
"primMetaToNatInjective" forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName

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

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

  -- Cubical
  , String
builtinIMin       forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(&&)"
  , String
builtinIMax       forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(||)"
  , String
builtinINeg       forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"not"
  , String
"primPartial"     forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ x -> x"
  , String
"primPartialP"    forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ x -> x"
  , String
builtinPOr        forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ i _ _ x y -> if i then x else y"
  , String
builtinComp       forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ x -> x"
  , String
builtinTrans      forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ x -> x"
  , String
builtinHComp      forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ x -> x"
  , String
builtinSubOut     forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ x -> x"
  , String
builtin_glueU     forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ _ x -> x"
  , String
builtin_unglueU   forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ x -> x"
  , String
builtinFaceForall forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return
                            String
"\\f -> f True == True && f False == True"
  , String
"primDepIMin"     forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\i f -> if i then f () else False"
  , String
"primIdFace"      forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ -> fst"
  , String
"primIdPath"      forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ -> snd"
  , String
builtinIdElim     forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return
                            String
"\\_ _ _ _ _ f x y -> f (fst y) x (snd y)"
  ]
  where
  a
x |-> :: a -> f a -> (a, f (Either a b))
|-> f a
s = (a
x, forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
s)
  binNat :: String -> m String
binNat  String
op = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op] String
"(<<0>> :: Integer -> Integer -> Integer)"
  binNat4 :: String -> m String
binNat4 String
op = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op] String
"(<<0>> :: Integer -> Integer -> Integer -> Integer -> Integer)"
  binAsis :: String -> String -> m String
binAsis String
op String
ty = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op, String -> String
opty String
ty] forall a b. (a -> b) -> a -> b
$ String
"((<<0>>) :: <<1>>)"
  rel' :: String -> String -> String -> m String
rel' String
toTy String
op String
ty = do
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op, String
ty, String
toTy] forall a b. (a -> b) -> a -> b
$
      String
"(\\ x y -> (<<0>> :: <<1>> -> <<1>> -> Bool) (<<2>> x) (<<2>> y))"
  relNat :: String -> m String
relNat String
op = do
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op] forall a b. (a -> b) -> a -> b
$
      String
"(<<0>> :: Integer -> Integer -> Bool)"
  rel :: String -> String -> m String
rel String
op String
ty  = forall {m :: * -> *}.
Monad m =>
String -> String -> String -> m String
rel' String
"" String
op String
ty
  opty :: String -> String
opty String
t = String
t forall a. [a] -> [a] -> [a]
++ String
"->" forall a. [a] -> [a] -> [a]
++ String
t forall a. [a] -> [a] -> [a]
++ String
"->" forall a. [a] -> [a] -> [a]
++ String
t
  unimplemented :: m Exp
unimplemented = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
NotImplemented String
s

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

noCheckCover :: (HasBuiltins m, MonadReduce m) => QName -> m Bool
noCheckCover :: forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
QName -> m Bool
noCheckCover QName
q = Bool -> Bool -> Bool
(||) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
QName -> String -> m Bool
isBuiltin QName
q String
builtinNat forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 = forall a. Pretty a => a -> String
prettyPrint forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> String -> HsCompileM QName
bltQual String
b String
s