{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Compiler.MAlonzo.Primitives where
import Control.Arrow ( second )
import Control.Monad.Trans.Maybe ( MaybeT(MaybeT, runMaybeT) )
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.HashMap.Strict as HMap
import Data.Maybe
import Agda.Compiler.Common
import Agda.Compiler.MAlonzo.Misc
import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Syntax.Internal
import Agda.Syntax.Treeless
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.Utils.Either
import Agda.Utils.Lens
import Agda.Utils.List (hasElem)
import qualified Agda.Utils.Haskell.Syntax as HS
import Agda.Utils.Impossible
newtype MainFunctionDef = MainFunctionDef Definition
data CheckedMainFunctionDef = CheckedMainFunctionDef
{ CheckedMainFunctionDef -> MainFunctionDef
checkedMainDef :: MainFunctionDef
, CheckedMainFunctionDef -> Decl
checkedMainDecl :: HS.Decl
}
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)
perhaps :: Maybe MainFunctionDef
perhaps | Bool
isNamedMain = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Definition -> MainFunctionDef
MainFunctionDef Definition
d
| Bool
otherwise = forall {a}. Maybe a
no
no :: Maybe a
no = forall {a}. Maybe a
Nothing
mainFunctionDefs :: Interface -> [MainFunctionDef]
mainFunctionDefs :: Interface -> [MainFunctionDef]
mainFunctionDefs Interface
i = forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ Definition -> Maybe MainFunctionDef
asMainFunctionDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Definition]
defs
where
defs :: [Definition]
defs = forall k v. HashMap k v -> [v]
HMap.elems forall a b. (a -> b) -> a -> b
$ Interface -> Signature
iSignature Interface
i forall o i. o -> Lens' o i -> i
^. Lens' Signature (HashMap QName Definition)
sigDefinitions
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
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"
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"
TPrim
PIf -> forall a. HasCallStack => a
__IMPOSSIBLE__
importsForPrim :: BuiltinThings PrimFun -> [Definition] -> [HS.ModuleName]
importsForPrim :: BuiltinThings PrimFun -> [Definition] -> [ModuleName]
importsForPrim BuiltinThings PrimFun
builtinThings [Definition]
defs = forall a.
Map SomeBuiltin a -> BuiltinThings PrimFun -> [Definition] -> [a]
xForPrim Map SomeBuiltin ModuleName
table BuiltinThings PrimFun
builtinThings [Definition]
defs forall a. [a] -> [a] -> [a]
++ [String -> ModuleName
HS.ModuleName String
"Data.Text"]
where
table :: Map SomeBuiltin ModuleName
table = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second String -> ModuleName
HS.ModuleName)
[ forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin BuiltinId
BuiltinChar forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatCeiling forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatDecode forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatEncode forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatEquality forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatFloor forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatInequality forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatIsSafeInteger forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatLess forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatRound forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatToRatio forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimFloatToWord64 forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsAlpha forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsAscii forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsDigit forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsHexDigit forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsLatin1 forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsLower forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsPrint forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimIsSpace forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimRatioToFloat forall {a} {b}. a -> b -> (a, b)
|-> String
"MAlonzo.RTE.Float"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimToLower forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
, forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
PrimToUpper forall {a} {b}. a -> b -> (a, b)
|-> String
"Data.Char"
]
|-> :: a -> b -> (a, b)
(|->) = (,)
xForPrim :: Map SomeBuiltin a -> BuiltinThings PrimFun -> [Definition] -> [a]
xForPrim :: forall a.
Map SomeBuiltin a -> BuiltinThings PrimFun -> [Definition] -> [a]
xForPrim Map SomeBuiltin a
table BuiltinThings PrimFun
builtinThings [Definition]
defs = forall a. [Maybe a] -> [a]
catMaybes
[ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SomeBuiltin
s Map SomeBuiltin a
table
| (SomeBuiltin
s, Builtin PrimFun
def) <- forall k a. Map k a -> [(k, a)]
Map.toList BuiltinThings PrimFun
builtinThings
, forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False QName -> Bool
elemDefs forall a b. (a -> b) -> a -> b
$ Builtin PrimFun -> Maybe QName
getName Builtin PrimFun
def
]
where
elemDefs :: QName -> Bool
elemDefs = forall a. Ord a => [a] -> a -> Bool
hasElem forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Definition -> QName
defName [Definition]
defs
getName :: Builtin PrimFun -> Maybe QName
getName = \case
Builtin Term
t -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term -> QName
getPrimName Term
t
Prim (PrimFun QName
q Arity
_ [Occurrence]
_ [Arg Term] -> Arity -> ReduceM (Reduced MaybeReducedArgs Term)
_) -> forall a. a -> Maybe a
Just QName
q
BuiltinRewriteRelations Set QName
_ -> forall {a}. Maybe a
Nothing
primBody :: MonadTCError m => PrimitiveId -> m HS.Exp
primBody :: forall (m :: * -> *). MonadTCError m => PrimitiveId -> m Exp
primBody PrimitiveId
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Exp
unimplemented (forall a b. (a -> b) -> Either a b -> b
fromRight (Name -> Exp
hsVarUQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
HS.Ident) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup PrimitiveId
s forall a b. (a -> b) -> a -> b
$
[
PrimitiveId
PrimShowInteger forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(Data.Text.pack . show :: Integer -> Data.Text.Text)"
, PrimitiveId
PrimLevelZero forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"()"
, PrimitiveId
PrimLevelSuc forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(\\ _ -> ())"
, PrimitiveId
PrimLevelMax forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(\\ _ _ -> ())"
, PrimitiveId
PrimNatPlus forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
binNat String
"(+)"
, PrimitiveId
PrimNatMinus forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
binNat String
"(\\ x y -> max 0 (x - y))"
, PrimitiveId
PrimNatTimes forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
binNat String
"(*)"
, PrimitiveId
PrimNatDivSucAux forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
binNat4 String
"(\\ k m n j -> k + div (max 0 $ n + m - j) (m + 1))"
, PrimitiveId
PrimNatModSucAux forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
binNat4 String
"(\\ k m n j -> if n > j then mod (n - j - 1) (m + 1) else (k + n))"
, PrimitiveId
PrimNatEquality forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
relNat String
"(==)"
, PrimitiveId
PrimNatLess forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> m String
relNat String
"(<)"
, PrimitiveId
PrimShowNat forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(Data.Text.pack . show :: Integer -> Data.Text.Text)"
, PrimitiveId
PrimWord64ToNat forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.word64ToNat"
, PrimitiveId
PrimWord64FromNat forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.word64FromNat"
, PrimitiveId
PrimWord64ToNatInjective forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName
, PrimitiveId
PrimFloatEquality forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleEq"
, PrimitiveId
PrimFloatInequality forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleLe"
, PrimitiveId
PrimFloatLess forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleLt"
, PrimitiveId
PrimFloatIsInfinite forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(isInfinite :: Double -> Bool)"
, PrimitiveId
PrimFloatIsNaN forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(isNaN :: Double -> Bool)"
, PrimitiveId
PrimFloatIsNegativeZero forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(isNegativeZero :: Double -> Bool)"
, PrimitiveId
PrimFloatIsSafeInteger forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.isSafeInteger"
, PrimitiveId
PrimFloatToWord64 forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleToWord64"
, PrimitiveId
PrimFloatToWord64Injective forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName
, PrimitiveId
PrimNatToFloat forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(MAlonzo.RTE.Float.intToDouble :: Integer -> Double)"
, PrimitiveId
PrimIntToFloat forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(MAlonzo.RTE.Float.intToDouble :: Integer -> Double)"
, PrimitiveId
PrimFloatRound forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleRound"
, PrimitiveId
PrimFloatFloor forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleFloor"
, PrimitiveId
PrimFloatCeiling forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleCeiling"
, PrimitiveId
PrimFloatToRatio forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleToRatio"
, PrimitiveId
PrimRatioToFloat forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.ratioToDouble"
, PrimitiveId
PrimFloatDecode forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleDecode"
, PrimitiveId
PrimFloatEncode forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleEncode"
, PrimitiveId
PrimShowFloat forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(Data.Text.pack . show :: Double -> Data.Text.Text)"
, PrimitiveId
PrimFloatPlus forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doublePlus"
, PrimitiveId
PrimFloatMinus forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleMinus"
, PrimitiveId
PrimFloatTimes forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleTimes"
, PrimitiveId
PrimFloatNegate forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleNegate"
, PrimitiveId
PrimFloatDiv forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleDiv"
, PrimitiveId
PrimFloatPow forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doublePow"
, PrimitiveId
PrimFloatSqrt forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleSqrt"
, PrimitiveId
PrimFloatExp forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleExp"
, PrimitiveId
PrimFloatLog forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleLog"
, PrimitiveId
PrimFloatSin forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleSin"
, PrimitiveId
PrimFloatCos forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleCos"
, PrimitiveId
PrimFloatTan forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleTan"
, PrimitiveId
PrimFloatASin forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleASin"
, PrimitiveId
PrimFloatACos forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleACos"
, PrimitiveId
PrimFloatATan forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleATan"
, PrimitiveId
PrimFloatATan2 forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleATan2"
, PrimitiveId
PrimFloatSinh forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleSinh"
, PrimitiveId
PrimFloatCosh forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleCosh"
, PrimitiveId
PrimFloatTanh forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleTanh"
, PrimitiveId
PrimFloatASinh forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleASinh"
, PrimitiveId
PrimFloatACosh forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleACosh"
, PrimitiveId
PrimFloatATanh forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.Float.doubleATanh"
, PrimitiveId
PrimCharEquality forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(==)" String
"Char"
, PrimitiveId
PrimIsLower forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Char.isLower"
, PrimitiveId
PrimIsDigit forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Char.isDigit"
, PrimitiveId
PrimIsAlpha forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Char.isAlpha"
, PrimitiveId
PrimIsSpace forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Char.isSpace"
, PrimitiveId
PrimIsAscii forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Char.isAscii"
, PrimitiveId
PrimIsLatin1 forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Char.isLatin1"
, PrimitiveId
PrimIsPrint forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Char.isPrint"
, PrimitiveId
PrimIsHexDigit forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Char.isHexDigit"
, PrimitiveId
PrimToUpper forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Char.toUpper"
, PrimitiveId
PrimToLower forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Char.toLower"
, PrimitiveId
PrimCharToNat forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(fromIntegral . fromEnum :: Char -> Integer)"
, PrimitiveId
PrimNatToChar forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.natToChar"
, PrimitiveId
PrimShowChar forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(Data.Text.pack . show :: Char -> Data.Text.Text)"
, PrimitiveId
PrimCharToNatInjective forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName
, PrimitiveId
PrimStringUncons forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Text.uncons"
, PrimitiveId
PrimStringToList forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Text.unpack"
, PrimitiveId
PrimStringFromList forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Text.pack"
, PrimitiveId
PrimStringAppend forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
binAsis String
"Data.Text.append" String
"Data.Text.Text"
, PrimitiveId
PrimStringEquality forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(==)" String
"Data.Text.Text"
, PrimitiveId
PrimShowString forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(Data.Text.pack . show :: Data.Text.Text -> Data.Text.Text)"
, PrimitiveId
PrimStringToListInjective forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName
, PrimitiveId
PrimStringFromListInjective forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName
, PrimitiveId
PrimQNameEquality forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(==)" String
"MAlonzo.RTE.QName"
, PrimitiveId
PrimQNameLess forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(<)" String
"MAlonzo.RTE.QName"
, PrimitiveId
PrimShowQName forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"Data.Text.pack . MAlonzo.RTE.qnameString"
, PrimitiveId
PrimQNameFixity forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"MAlonzo.RTE.qnameFixity"
, PrimitiveId
PrimQNameToWord64s forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\ qn -> (MAlonzo.RTE.nameId qn, MAlonzo.RTE.moduleId qn)"
, PrimitiveId
PrimQNameToWord64sInjective forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName
, PrimitiveId
PrimMetaEquality forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(==)" String
"(Integer, Integer)"
, PrimitiveId
PrimMetaLess forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall {m :: * -> *}. Monad m => String -> String -> m String
rel String
"(<)" String
"(Integer, Integer)"
, PrimitiveId
PrimShowMeta forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\ (m, h) -> Data.Text.pack (\"_\" ++ show (m :: Integer) ++ \"@\" ++ show (h :: Integer))"
, PrimitiveId
PrimMetaToNat forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\ (m, h) -> (h :: Integer) * 2^64 + (m :: Integer)"
, PrimitiveId
PrimMetaToNatInjective forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName
, PrimitiveId
PrimForce forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\ _ _ _ _ x f -> f $! x"
, PrimitiveId
PrimForceLemma forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName
, PrimitiveId
PrimLockUniv forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"()"
, PrimitiveId
PrimEraseEquality forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
mazErasedName
, PrimitiveId
PrimIMin forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(&&)"
, PrimitiveId
PrimIMax forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"(||)"
, PrimitiveId
PrimINeg forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"not"
, PrimitiveId
PrimPartial forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ x -> x"
, PrimitiveId
PrimPartialP forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ x -> x"
, PrimitiveId
PrimPOr forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ i _ _ x y -> if i then x else y"
, PrimitiveId
PrimComp forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ x -> x"
, PrimitiveId
PrimTrans forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ x -> x"
, PrimitiveId
PrimHComp forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ x -> x"
, PrimitiveId
PrimSubOut forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ x -> x"
, PrimitiveId
Prim_glueU forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ _ x -> x"
, PrimitiveId
Prim_unglueU forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ x -> x"
, PrimitiveId
PrimFaceForall forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return
String
"\\f -> f True == True && f False == True"
, PrimitiveId
PrimDepIMin forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\i f -> if i then f () else False"
, PrimitiveId
PrimIdFace forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ -> fst"
, PrimitiveId
PrimIdPath forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return String
"\\_ _ _ _ -> snd"
, PrimitiveId
PrimIdElim forall {f :: * -> *} {a} {a} {b}.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> forall (m :: * -> *) a. Monad m => a -> m a
return
String
"\\_ _ _ _ _ f x y -> f (fst y) x (snd y)"
]
where
a
x |-> :: a -> f a -> (a, f (Either a b))
|-> f a
s = (a
x, forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
s)
binNat :: String -> m String
binNat String
op = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op] String
"(<<0>> :: Integer -> Integer -> Integer)"
binNat4 :: String -> m String
binNat4 String
op = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op] String
"(<<0>> :: Integer -> Integer -> Integer -> Integer -> Integer)"
binAsis :: String -> String -> m String
binAsis String
op String
ty = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op, String -> String
opty String
ty] forall a b. (a -> b) -> a -> b
$ String
"((<<0>>) :: <<1>>)"
rel' :: String -> String -> String -> m String
rel' String
toTy String
op String
ty = do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op, String
ty, String
toTy] forall a b. (a -> b) -> a -> b
$
String
"(\\ x y -> (<<0>> :: <<1>> -> <<1>> -> Bool) (<<2>> x) (<<2>> y))"
relNat :: String -> m String
relNat String
op = do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op] forall a b. (a -> b) -> a -> b
$
String
"(<<0>> :: Integer -> Integer -> Bool)"
rel :: String -> String -> m String
rel String
op String
ty = forall {m :: * -> *}.
Monad m =>
String -> String -> String -> m String
rel' String
"" String
op String
ty
opty :: String -> String
opty String
t = String
t forall a. [a] -> [a] -> [a]
++ String
"->" forall a. [a] -> [a] -> [a]
++ String
t forall a. [a] -> [a] -> [a]
++ String
"->" forall a. [a] -> [a] -> [a]
++ String
t
unimplemented :: m Exp
unimplemented = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
NotImplemented (forall a. IsBuiltin a => a -> String
getBuiltinId PrimitiveId
s)
hLam :: String -> Term -> Term
hLam String
x Term
t = ArgInfo -> Abs Term -> Term
Lam (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
defaultArgInfo) (forall a. String -> a -> Abs a
Abs String
x Term
t)
nLam :: String -> Term -> Term
nLam String
x Term
t = ArgInfo -> Abs Term -> Term
Lam (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden ArgInfo
defaultArgInfo) (forall a. String -> a -> Abs a
Abs String
x Term
t)
noCheckCover :: (HasBuiltins m, MonadReduce m) => QName -> m Bool
noCheckCover :: forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
QName -> m Bool
noCheckCover QName
q = Bool -> Bool -> Bool
(||) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
QName -> BuiltinId -> m Bool
isBuiltin QName
q BuiltinId
builtinNat forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
QName -> BuiltinId -> m Bool
isBuiltin QName
q BuiltinId
builtinInteger