module Agda.Compiler.MAlonzo.Primitives where
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.HashMap.Strict as HMap
import Data.Maybe
import Agda.Compiler.Common
import Agda.Compiler.ToTreeless
import {-# SOURCE #-} Agda.Compiler.MAlonzo.Compiler (closedTerm)
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.Monad.Builtin
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
isMainFunction :: QName -> Defn -> Bool
isMainFunction :: QName -> Defn -> Bool
isMainFunction q :: QName
q = \case
Axiom{} -> Bool
perhaps
Function{ funProjection :: Defn -> Maybe Projection
funProjection = Maybe Projection
Nothing } -> Bool
perhaps
Function{ funProjection :: Defn -> Maybe Projection
funProjection = Just{} } -> Bool
no
AbstractDefn{} -> Bool
no
GeneralizableVar{} -> Bool
no
DataOrRecSig{} -> Bool
no
Datatype{} -> Bool
no
Record{} -> Bool
no
Constructor{} -> Bool
no
Primitive{} -> Bool
no
where
perhaps :: Bool
perhaps = "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) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q)
no :: Bool
no = Bool
False
hasMainFunction
:: IsMain
-> Interface
-> IsMain
hasMainFunction :: IsMain -> Interface -> IsMain
hasMainFunction NotMain _ = IsMain
NotMain
hasMainFunction IsMain i :: Interface
i
| ((QName, Definition) -> Bool) -> [(QName, Definition)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
List.any (\ (x :: QName
x, def :: Definition
def) -> QName -> Defn -> Bool
isMainFunction QName
x (Defn -> Bool) -> Defn -> Bool
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def) [(QName, Definition)]
names = IsMain
IsMain
| Bool
otherwise = IsMain
NotMain
where
names :: [(QName, Definition)]
names = HashMap QName Definition -> [(QName, Definition)]
forall k v. HashMap k v -> [(k, v)]
HMap.toList (HashMap QName Definition -> [(QName, Definition)])
-> HashMap QName Definition -> [(QName, 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
checkTypeOfMain :: IsMain -> QName -> Definition -> TCM [HS.Decl] -> TCM [HS.Decl]
checkTypeOfMain :: IsMain -> QName -> Definition -> TCM [Decl] -> TCM [Decl]
checkTypeOfMain NotMain q :: QName
q def :: Definition
def ret :: TCM [Decl]
ret = TCM [Decl]
ret
checkTypeOfMain IsMain q :: QName
q def :: Definition
def ret :: TCM [Decl]
ret
| Bool -> Bool
not (QName -> Defn -> Bool
isMainFunction QName
q (Defn -> Bool) -> Defn -> Bool
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def) = TCM [Decl]
ret
| Bool
otherwise = do
Def io :: QName
io _ <- 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 :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (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 d :: QName
d _ | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
io -> (Decl
mainAlias Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
:) ([Decl] -> [Decl]) -> TCM [Decl] -> TCM [Decl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM [Decl]
ret
_ -> do
Doc
err <- [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *). Monad m => [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 :: * -> *). Monad m => String -> [m Doc]
pwords "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 :: * -> *). Monad m => String -> [m Doc]
pwords " 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 -> TCM [Decl]
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM [Decl]) -> TypeError -> TCM [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 "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 "d" QName
q)
treelessPrimName :: TPrim -> String
treelessPrimName :: TPrim -> String
treelessPrimName p :: TPrim
p =
case TPrim
p of
PQuot -> "quotInt"
PRem -> "remInt"
PSub -> "subInt"
PAdd -> "addInt"
PMul -> "mulInt"
PGeq -> "geqInt"
PLt -> "ltInt"
PEqI -> "eqInt"
PQuot64 -> "quot64"
PRem64 -> "rem64"
PSub64 -> "sub64"
PAdd64 -> "add64"
PMul64 -> "mul64"
PLt64 -> "lt64"
PEq64 -> "eq64"
PITo64 -> "word64FromNat"
P64ToI -> "word64ToNat"
PEqF -> "eqFloat"
PEqC -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
PEqS -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
PEqQ -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
PSeq -> "seq"
PIf -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
importsForPrim :: TCM [HS.ModuleName]
importsForPrim :: TCM [ModuleName]
importsForPrim =
([ModuleName] -> [ModuleName])
-> TCM [ModuleName] -> TCM [ModuleName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([ModuleName] -> [ModuleName] -> [ModuleName]
forall a. [a] -> [a] -> [a]
++ [String -> ModuleName
HS.ModuleName "Data.Text"]) (TCM [ModuleName] -> TCM [ModuleName])
-> TCM [ModuleName] -> TCM [ModuleName]
forall a b. (a -> b) -> a -> b
$
[(String, TCM [ModuleName])] -> TCM [ModuleName]
forall a. [(String, TCM [a])] -> TCM [a]
xForPrim ([(String, TCM [ModuleName])] -> TCM [ModuleName])
-> [(String, TCM [ModuleName])] -> TCM [ModuleName]
forall a b. (a -> b) -> a -> b
$
((String, [String]) -> (String, TCM [ModuleName]))
-> [(String, [String])] -> [(String, TCM [ModuleName])]
forall a b. (a -> b) -> [a] -> [b]
List.map (\(s :: String
s, ms :: [String]
ms) -> (String
s, [ModuleName] -> TCM [ModuleName]
forall (m :: * -> *) a. Monad m => a -> m a
return ((String -> ModuleName) -> [String] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
List.map String -> ModuleName
HS.ModuleName [String]
ms))) ([(String, [String])] -> [(String, TCM [ModuleName])])
-> [(String, [String])] -> [(String, TCM [ModuleName])]
forall a b. (a -> b) -> a -> b
$
[ "CHAR" String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> ["Data.Char"]
, "primIsAlpha" String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> ["Data.Char"]
, "primIsAscii" String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> ["Data.Char"]
, "primIsDigit" String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> ["Data.Char"]
, "primIsHexDigit" String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> ["Data.Char"]
, "primIsLatin1" String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> ["Data.Char"]
, "primIsLower" String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> ["Data.Char"]
, "primIsPrint" String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> ["Data.Char"]
, "primIsSpace" String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> ["Data.Char"]
, "primToLower" String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> ["Data.Char"]
, "primToUpper" String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> ["Data.Char"]
]
where |-> :: a -> b -> (a, b)
(|->) = (,)
xForPrim :: [(String, TCM [a])] -> TCM [a]
xForPrim :: [(String, TCM [a])] -> TCM [a]
xForPrim table :: [(String, TCM [a])]
table = do
[QName]
qs <- HashMap QName Definition -> [QName]
forall k v. HashMap k v -> [k]
HMap.keys (HashMap QName Definition -> [QName])
-> TCMT IO (HashMap QName Definition) -> TCMT IO [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (HashMap QName Definition)
curDefs
[(String, Builtin PrimFun)]
bs <- Map String (Builtin PrimFun) -> [(String, Builtin PrimFun)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map String (Builtin PrimFun) -> [(String, Builtin PrimFun)])
-> TCMT IO (Map String (Builtin PrimFun))
-> TCMT IO [(String, Builtin PrimFun)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCState -> Map String (Builtin PrimFun))
-> TCMT IO (Map String (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> Map String (Builtin PrimFun)
stBuiltinThings
let getName :: Builtin PrimFun -> QName
getName (Builtin (Def q :: QName
q _)) = QName
q
getName (Builtin (Con q :: ConHead
q _ _)) = ConHead -> QName
conName ConHead
q
getName (Builtin (Lam _ b :: Abs Term
b)) = Builtin PrimFun -> QName
getName (Term -> Builtin PrimFun
forall pf. Term -> Builtin pf
Builtin (Term -> Builtin PrimFun) -> Term -> Builtin PrimFun
forall a b. (a -> b) -> a -> b
$ Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b)
getName (Builtin _) = QName
forall a. HasCallStack => a
__IMPOSSIBLE__
getName (Prim (PrimFun q :: QName
q _ _)) = QName
q
[[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[a]] -> [a]) -> TCMT IO [[a]] -> TCM [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TCM [a]] -> TCMT IO [[a]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ TCM [a] -> Maybe (TCM [a]) -> TCM [a]
forall a. a -> Maybe a -> a
fromMaybe ([a] -> TCM [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (Maybe (TCM [a]) -> TCM [a]) -> Maybe (TCM [a]) -> TCM [a]
forall a b. (a -> b) -> a -> b
$ String -> [(String, TCM [a])] -> Maybe (TCM [a])
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup String
s [(String, TCM [a])]
table
| (s :: String
s, def :: Builtin PrimFun
def) <- [(String, Builtin PrimFun)]
bs, Builtin PrimFun -> QName
getName Builtin PrimFun
def QName -> [QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
qs ]
primBody :: String -> TCM HS.Exp
primBody :: String -> TCM Exp
primBody s :: String
s = TCM Exp
-> (TCMT IO (Either String Exp) -> TCM Exp)
-> Maybe (TCMT IO (Either String Exp))
-> TCM Exp
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCM 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)
-> TCMT IO (Either String Exp) -> TCM Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (TCMT IO (Either String Exp)) -> TCM Exp)
-> Maybe (TCMT IO (Either String Exp)) -> TCM Exp
forall a b. (a -> b) -> a -> b
$
String
-> [(String, TCMT IO (Either String Exp))]
-> Maybe (TCMT IO (Either String Exp))
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup String
s ([(String, TCMT IO (Either String Exp))]
-> Maybe (TCMT IO (Either String Exp)))
-> [(String, TCMT IO (Either String Exp))]
-> Maybe (TCMT IO (Either String Exp))
forall a b. (a -> b) -> a -> b
$
[
"primIntegerPlus" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
binAsis "(+)" "Integer"
, "primIntegerMinus" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
binAsis "(-)" "Integer"
, "primIntegerTimes" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
binAsis "(*)" "Integer"
, "primIntegerDiv" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
binAsis "div" "Integer"
, "primIntegerMod" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
binAsis "mod" "Integer"
, "primIntegerEquality"String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
rel "(==)" "Integer"
, "primIntegerLess" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
rel "(<)" "Integer"
, "primIntegerAbs" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(abs :: Integer -> Integer)"
, "primNatToInteger" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(id :: Integer -> Integer)"
, "primShowInteger" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(Data.Text.pack . show :: Integer -> Data.Text.Text)"
, "primLevelZero" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "()"
, "primLevelSuc" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(\\ _ -> ())"
, "primLevelMax" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(\\ _ _ -> ())"
, "primSetOmega" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "()"
, "primNatPlus" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> m String
binNat "(+)"
, "primNatMinus" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> m String
binNat "(\\ x y -> max 0 (x - y))"
, "primNatTimes" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> m String
binNat "(*)"
, "primNatDivSucAux" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> m String
binNat4 "(\\ k m n j -> k + div (max 0 $ n + m - j) (m + 1))"
, "primNatModSucAux" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> m String
binNat4 "(\\ k m n j -> if n > j then mod (n - j - 1) (m + 1) else (k + n))"
, "primNatEquality" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> m String
relNat "(==)"
, "primNatLess" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> m String
relNat "(<)"
, "primShowNat" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(Data.Text.pack . show :: Integer -> Data.Text.Text)"
, "primWord64ToNat" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "MAlonzo.RTE.word64ToNat"
, "primWord64FromNat" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "MAlonzo.RTE.word64FromNat"
, "primWord64ToNatInjective" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "erased"
, "primNatToFloat" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(fromIntegral :: Integer -> Double)"
, "primFloatPlus" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "((+) :: Double -> Double -> Double)"
, "primFloatMinus" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "((-) :: Double -> Double -> Double)"
, "primFloatTimes" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "((*) :: Double -> Double -> Double)"
, "primFloatNegate" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(negate :: Double -> Double)"
, "primFloatDiv" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "((/) :: Double -> Double -> Double)"
, "primFloatEquality" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "MAlonzo.RTE.eqFloat"
, "primFloatLess" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "MAlonzo.RTE.ltFloat"
, "primFloatNumericalEquality" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "MAlonzo.RTE.eqNumFloat"
, "primFloatNumericalLess" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "MAlonzo.RTE.ltNumFloat"
, "primFloatSqrt" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(sqrt :: Double -> Double)"
, "primRound" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(round . MAlonzo.RTE.normaliseNaN :: Double -> Integer)"
, "primFloor" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(floor . MAlonzo.RTE.normaliseNaN :: Double -> Integer)"
, "primCeiling" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(ceiling . MAlonzo.RTE.normaliseNaN :: Double -> Integer)"
, "primExp" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(exp :: Double -> Double)"
, "primLog" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(log :: Double -> Double)"
, "primSin" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(sin :: Double -> Double)"
, "primCos" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(cos :: Double -> Double)"
, "primTan" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(tan :: Double -> Double)"
, "primASin" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(asin :: Double -> Double)"
, "primACos" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(acos :: Double -> Double)"
, "primATan" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(atan :: Double -> Double)"
, "primATan2" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(atan2 :: Double -> Double -> Double)"
, "primShowFloat" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(Data.Text.pack . show :: Double -> Data.Text.Text)"
, "primFloatToWord64" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "MAlonzo.RTE.doubleToWord64"
, "primFloatToWord64Injective" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "erased"
, "primCharEquality" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
rel "(==)" "Char"
, "primIsLower" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Data.Char.isLower"
, "primIsDigit" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Data.Char.isDigit"
, "primIsAlpha" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Data.Char.isAlpha"
, "primIsSpace" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Data.Char.isSpace"
, "primIsAscii" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Data.Char.isAscii"
, "primIsLatin1" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Data.Char.isLatin1"
, "primIsPrint" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Data.Char.isPrint"
, "primIsHexDigit" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Data.Char.isHexDigit"
, "primToUpper" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Data.Char.toUpper"
, "primToLower" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Data.Char.toLower"
, "primCharToNat" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(fromIntegral . fromEnum :: Char -> Integer)"
, "primNatToChar" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(toEnum . fromIntegral :: Integer -> Char)"
, "primShowChar" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(Data.Text.pack . show :: Char -> Data.Text.Text)"
, "primCharToNatInjective" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "erased"
, "primStringToList" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Data.Text.unpack"
, "primStringFromList" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Data.Text.pack"
, "primStringAppend" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
binAsis "Data.Text.append" "Data.Text.Text"
, "primStringEquality" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
rel "(==)" "Data.Text.Text"
, "primShowString" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(Data.Text.pack . show :: Data.Text.Text -> Data.Text.Text)"
, "primStringToListInjective" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "erased"
, "primQNameEquality" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
rel "(==)" "MAlonzo.RTE.QName"
, "primQNameLess" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
rel "(<)" "MAlonzo.RTE.QName"
, "primShowQName" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Data.Text.pack . MAlonzo.RTE.qnameString"
, "primQNameFixity" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "MAlonzo.RTE.qnameFixity"
, "primQNameToWord64s" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "\\ qn -> (MAlonzo.RTE.nameId qn, MAlonzo.RTE.moduleId qn)"
, "primQNameToWord64sInjective" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "erased"
, "primMetaEquality" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
rel "(==)" "Integer"
, "primMetaLess" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> String -> TCMT IO String
forall (m :: * -> *). Monad m => String -> String -> m String
rel "(<)" "Integer"
, "primShowMeta" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "\\ x -> Data.Text.pack (\"_\" ++ show (x :: Integer))"
, "primMetaToNat" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "(id :: Integer -> Integer)"
, "primMetaToNatInjective" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "erased"
, "primForce" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "\\ _ _ _ _ x f -> f $! x"
, "primForceLemma" String -> TCMT IO String -> (String, TCMT IO (Either String Exp))
forall (f :: * -> *) a a b.
Functor f =>
a -> f a -> (a, f (Either a b))
|-> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "erased"
, ("primEraseEquality", Exp -> Either String Exp
forall a b. b -> Either a b
Right (Exp -> Either String Exp)
-> TCM Exp -> TCMT IO (Either String Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
Term
refl <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRefl
let erase :: Term
erase = String -> Term -> Term
hLam "a" (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term -> Term
hLam "A" (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term -> Term
hLam "x" (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term -> Term
hLam "y" (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term -> Term
nLam "eq" Term
refl
TTerm -> TCM Exp
closedTerm (TTerm -> TCM Exp) -> TCMT IO TTerm -> TCM Exp
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< EvaluationStrategy -> Term -> TCMT IO TTerm
closedTermToTreeless EvaluationStrategy
LazyEvaluation Term
erase
)
]
where
x :: a
x |-> :: a -> f a -> (a, f (Either a b))
|-> s :: 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)
bin :: String -> String -> String -> String -> String -> TCMT IO String
bin blt :: String
blt op :: String
op ty :: String
ty from :: String
from to :: String
to = do
String
from' <- String -> String -> TCMT IO String
bltQual' String
blt String
from
String
to' <- String -> String -> TCMT IO String
bltQual' String
blt String
to
String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TCMT IO String) -> String -> TCMT IO String
forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op, String -> String
opty String
ty, String
from', String
to'] (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
"\\ x y -> <<3>> ((<<0>> :: <<1>>) (<<2>> x) (<<2>> y))"
binNat :: String -> m String
binNat op :: 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] "(<<0>> :: Integer -> Integer -> Integer)"
binNat4 :: String -> m String
binNat4 op :: 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] "(<<0>> :: Integer -> Integer -> Integer -> Integer -> Integer)"
binAsis :: String -> String -> m String
binAsis op :: String
op ty :: 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
$ "((<<0>>) :: <<1>>)"
rel' :: String -> String -> String -> m String
rel' toTy :: String
toTy op :: String
op ty :: 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
$
"(\\ x y -> (<<0>> :: <<1>> -> <<1>> -> Bool) (<<2>> x) (<<2>> y))"
relNat :: String -> m String
relNat op :: 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
$
"(<<0>> :: Integer -> Integer -> Bool)"
rel :: String -> String -> m String
rel op :: String
op ty :: String
ty = String -> String -> String -> m String
forall (m :: * -> *).
Monad m =>
String -> String -> String -> m String
rel' "" String
op String
ty
opty :: String -> String
opty t :: String
t = String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "->" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "->" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
axiom_prims :: [String]
axiom_prims = ["primIMin","primIMax","primINeg","primPartial","primPartialP","primPFrom1","primPOr","primComp"]
unimplemented :: TCM Exp
unimplemented | String
s String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`List.elem` [String]
axiom_prims = Exp -> TCM Exp
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> TCM Exp) -> Exp -> TCM Exp
forall a b. (a -> b) -> a -> b
$ String -> Exp
rtmError (String -> Exp) -> String -> Exp
forall a b. (a -> b) -> a -> b
$ "primitive with no body evaluated: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
| Bool
otherwise = TypeError -> TCM Exp
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM Exp) -> TypeError -> TCM Exp
forall a b. (a -> b) -> a -> b
$ String -> TypeError
NotImplemented String
s
hLam :: String -> Term -> Term
hLam x :: String
x t :: 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 x :: String
x t :: 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 :: QName -> TCM Bool
noCheckCover :: QName -> TCM Bool
noCheckCover q :: QName
q = Bool -> Bool -> Bool
(||) (Bool -> Bool -> Bool) -> TCM Bool -> TCMT IO (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> String -> TCM Bool
isBuiltin QName
q String
builtinNat TCMT IO (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QName -> String -> TCM Bool
isBuiltin QName
q String
builtinInteger
pconName :: String -> TCM String
pconName :: String -> TCMT IO String
pconName s :: String
s = Term -> TCMT IO String
toS (Term -> TCMT IO String) -> TCMT IO Term -> TCMT IO String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getBuiltin String
s where
toS :: Term -> TCMT IO String
toS (Con q :: ConHead
q _ _) = QName -> String
forall a. Pretty a => a -> String
prettyPrint (QName -> String) -> TCMT IO QName -> TCMT IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO QName
conhqn (ConHead -> QName
conName ConHead
q)
toS (Lam _ t :: Abs Term
t) = Term -> TCMT IO String
toS (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
t)
toS _ = String -> TCMT IO String
forall a. String -> a
mazerror (String -> TCMT IO String) -> String -> TCMT IO String
forall a b. (a -> b) -> a -> b
$ "pconName" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
bltQual' :: String -> String -> TCM String
bltQual' :: String -> String -> TCMT IO String
bltQual' b :: String
b s :: String
s = QName -> String
forall a. Pretty a => a -> String
prettyPrint (QName -> String) -> TCMT IO QName -> TCMT IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> String -> TCMT IO QName
bltQual String
b String
s