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

-- 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).
isMainFunction :: QName -> Defn -> Bool
isMainFunction :: QName -> Defn -> Bool
isMainFunction 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 = String
"main" String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> String
forall a. Pretty a => a -> String
prettyShow (Name -> Name
nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q)  -- ignores the qualification!?
  no :: Bool
no      = Bool
False

-- | Check for "main" function, but only in the main module.
hasMainFunction
  :: IsMain    -- ^ Are we looking at the main module?
  -> Interface -- ^ The module.
  -> IsMain    -- ^ Did we find a "main" function?
hasMainFunction :: IsMain -> Interface -> IsMain
hasMainFunction IsMain
NotMain Interface
_ = IsMain
NotMain
hasMainFunction IsMain
IsMain Interface
i
  | ((QName, Definition) -> Bool) -> [(QName, Definition)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
List.any (\ (QName
x, 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

-- | Check that the main function has type IO a, for some a.
checkTypeOfMain :: IsMain -> QName -> Definition -> TCM [HS.Decl] -> TCM [HS.Decl]
checkTypeOfMain :: IsMain -> QName -> Definition -> TCM [Decl] -> TCM [Decl]
checkTypeOfMain IsMain
NotMain QName
q Definition
def TCM [Decl]
ret = TCM [Decl]
ret
checkTypeOfMain  IsMain
IsMain QName
q Definition
def 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 QName
io Elims
_ <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIO
    Type
ty <- Type -> TCMT IO Type
forall a (m :: * -> *). (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 QName
d Elims
_ | 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
      Term
_                 -> 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 String
"The type of main should be" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
          [QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
io] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ String -> [TCMT IO Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
" A, for some A. The given type is" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ty]
        TypeError -> 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 String
"main"
    mainRHS :: Rhs
mainRHS   = Exp -> Rhs
HS.UnGuardedRhs (Exp -> Rhs) -> Exp -> Rhs
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp
HS.App Exp
mazCoerce (QName -> Exp
HS.Var (QName -> Exp) -> QName -> Exp
forall a b. (a -> b) -> a -> b
$ Name -> QName
HS.UnQual (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ String -> QName -> Name
unqhname String
"d" QName
q)

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
"eqFloat"
    -- MAlonzo uses literal patterns, so we don't need equality for the other primitive types
    TPrim
PEqC  -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
    TPrim
PEqS  -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
    TPrim
PEqQ  -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
    TPrim
PSeq  -> String
"seq"
    -- primitives only used by GuardsToPrims transformation, which MAlonzo doesn't use
    TPrim
PIf   -> String
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Haskell modules to be imported for BUILT-INs
importsForPrim :: 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 String
"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 (\(String
s, [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
$
  [ String
"CHAR"              String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> [String
"Data.Char"]
  , String
"primIsAlpha"       String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> [String
"Data.Char"]
  , String
"primIsAscii"       String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> [String
"Data.Char"]
  , String
"primIsDigit"       String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> [String
"Data.Char"]
  , String
"primIsHexDigit"    String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> [String
"Data.Char"]
  , String
"primIsLatin1"      String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> [String
"Data.Char"]
  , String
"primIsLower"       String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> [String
"Data.Char"]
  , String
"primIsPrint"       String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> [String
"Data.Char"]
  , String
"primIsSpace"       String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> [String
"Data.Char"]
  , String
"primToLower"       String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> [String
"Data.Char"]
  , String
"primToUpper"       String -> [String] -> (String, [String])
forall a b. a -> b -> (a, b)
|-> [String
"Data.Char"]
  ]
  where |-> :: a -> b -> (a, b)
(|->) = (,)

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

xForPrim :: [(String, TCM [a])] -> TCM [a]
xForPrim :: [(String, TCM [a])] -> TCM [a]
xForPrim [(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 QName
q Elims
_))    = QName
q
      getName (Builtin (Con ConHead
q ConInfo
_ Elims
_))  = ConHead -> QName
conName ConHead
q
      getName (Builtin (Lam ArgInfo
_ 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 Term
_)            = QName
forall a. HasCallStack => a
__IMPOSSIBLE__
      getName (Prim (PrimFun QName
q Arity
_ [Arg Term] -> Arity -> ReduceM (Reduced MaybeReducedArgs Term)
_)) = 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
                        | (String
s, 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 ]


-- | Definition bodies for primitive functions
primBody :: String -> TCM HS.Exp
primBody :: String -> TCM Exp
primBody 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
$
  [
  -- Integer functions
    String
"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 String
"(+)" String
"Integer"
  , String
"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 String
"(-)" String
"Integer"
  , String
"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 String
"(*)" String
"Integer"
  , String
"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 String
"div" String
"Integer"
  , String
"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 String
"mod" String
"Integer"
  , String
"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 String
"(==)" String
"Integer"
  , String
"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 String
"(<)"  String
"Integer"
  , String
"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 String
"(abs :: Integer -> Integer)"
  , String
"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 String
"(id :: Integer -> Integer)"
  , String
"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 String
"(Data.Text.pack . show :: Integer -> Data.Text.Text)"

  -- Levels
  , String
"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 String
"()"
  , String
"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 String
"(\\ _ -> ())"
  , String
"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 String
"(\\ _ _ -> ())"

  -- Sorts
  , String
"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 String
"()"

  -- Natural number functions
  , String
"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 String
"(+)"
  , String
"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 String
"(\\ x y -> max 0 (x - y))"
  , String
"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 String
"(*)"
  , String
"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 String
"(\\ k m n j -> k + div (max 0 $ n + m - j) (m + 1))"
  , String
"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 String
"(\\ k m n j -> if n > j then mod (n - j - 1) (m + 1) else (k + n))"
  , String
"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 String
"(==)"
  , String
"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 String
"(<)"
  , String
"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 String
"(Data.Text.pack . show :: Integer -> Data.Text.Text)"

  -- Machine word functions
  , String
"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 String
"MAlonzo.RTE.word64ToNat"
  , String
"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 String
"MAlonzo.RTE.word64FromNat"
  , String
"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 String
"erased"

  -- Floating point functions
  , String
"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 String
"(fromIntegral :: Integer -> Double)"
  , String
"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 String
"((+)          :: Double -> Double -> Double)"
  , String
"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 String
"((-)          :: Double -> Double -> Double)"
  , String
"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 String
"((*)          :: Double -> Double -> Double)"
  , String
"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 String
"(negate       :: Double -> Double)"
  , String
"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 String
"((/)          :: Double -> Double -> Double)"
  -- ASR (2016-09-14). We use bitwise equality for comparing Double
  -- because Haskell's Eq, which equates 0.0 and -0.0, allows to prove
  -- a contradiction (see Issue #2169).
  , String
"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 String
"MAlonzo.RTE.eqFloat"
  , String
"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 String
"MAlonzo.RTE.ltFloat"
  , String
"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 String
"MAlonzo.RTE.eqNumFloat"
  , String
"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 String
"MAlonzo.RTE.ltNumFloat"
  , String
"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 String
"(sqrt :: Double -> Double)"
  , String
"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 String
"(round . MAlonzo.RTE.normaliseNaN :: Double -> Integer)"
  , String
"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 String
"(floor . MAlonzo.RTE.normaliseNaN :: Double -> Integer)"
  , String
"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 String
"(ceiling . MAlonzo.RTE.normaliseNaN :: Double -> Integer)"
  , String
"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 String
"(exp :: Double -> Double)"
  , String
"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 String
"(log :: Double -> Double)"
  , String
"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 String
"(sin :: Double -> Double)"
  , String
"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 String
"(cos :: Double -> Double)"
  , String
"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 String
"(tan :: Double -> Double)"
  , String
"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 String
"(asin :: Double -> Double)"
  , String
"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 String
"(acos :: Double -> Double)"
  , String
"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 String
"(atan :: Double -> Double)"
  , String
"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 String
"(atan2 :: Double -> Double -> Double)"
  , String
"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 String
"(Data.Text.pack . show :: Double -> Data.Text.Text)"
  , String
"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 String
"MAlonzo.RTE.doubleToWord64"
  , String
"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 String
"erased"

  -- Character functions
  , String
"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 String
"(==)" String
"Char"
  , String
"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 String
"Data.Char.isLower"
  , String
"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 String
"Data.Char.isDigit"
  , String
"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 String
"Data.Char.isAlpha"
  , String
"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 String
"Data.Char.isSpace"
  , String
"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 String
"Data.Char.isAscii"
  , String
"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 String
"Data.Char.isLatin1"
  , String
"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 String
"Data.Char.isPrint"
  , String
"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 String
"Data.Char.isHexDigit"
  , String
"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 String
"Data.Char.toUpper"
  , String
"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 String
"Data.Char.toLower"
  , String
"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 String
"(fromIntegral . fromEnum :: Char -> Integer)"
  , String
"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 String
"(toEnum . fromIntegral :: Integer -> Char)"
  , String
"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 String
"(Data.Text.pack . show :: Char -> Data.Text.Text)"
  , String
"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 String
"erased"

  -- String functions
  , String
"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 String
"Data.Text.unpack"
  , String
"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 String
"Data.Text.pack"
  , String
"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 String
"Data.Text.append" String
"Data.Text.Text"
  , String
"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 String
"(==)" String
"Data.Text.Text"
  , String
"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 String
"(Data.Text.pack . show :: Data.Text.Text -> Data.Text.Text)"
  , String
"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 String
"erased"

  -- Reflection
  , String
"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 String
"(==)" String
"MAlonzo.RTE.QName"
  , String
"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 String
"(<)" String
"MAlonzo.RTE.QName"
  , String
"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 String
"Data.Text.pack . MAlonzo.RTE.qnameString"
  , String
"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 String
"MAlonzo.RTE.qnameFixity"
  , String
"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 String
"\\ qn -> (MAlonzo.RTE.nameId qn, MAlonzo.RTE.moduleId qn)"
  , String
"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 String
"erased"
  , String
"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 String
"(==)" String
"Integer"
  , String
"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 String
"(<)" String
"Integer"
  , String
"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 String
"\\ x -> Data.Text.pack (\"_\" ++ show (x :: Integer))"
  , String
"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 String
"(id :: Integer -> Integer)"
  , String
"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 String
"erased"

  -- Seq
  , String
"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 String
"\\ _ _ _ _ x f -> f $! x"
  , String
"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 String
"erased"

  -- Erase
  , (String
"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 String
"a" (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term -> Term
hLam String
"A" (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term -> Term
hLam String
"x" (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term -> Term
hLam String
"y" (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term -> Term
nLam String
"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
  a
x |-> :: a -> f a -> (a, f (Either a b))
|-> f a
s = (a
x, a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> f a -> f (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
s)
  bin :: String -> String -> String -> String -> String -> TCMT IO String
bin String
blt String
op String
ty String
from 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
$
               String
"\\ x y -> <<3>> ((<<0>> :: <<1>>) (<<2>> x) (<<2>> y))"
  binNat :: String -> m String
binNat  String
op = String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op] String
"(<<0>> :: Integer -> Integer -> Integer)"
  binNat4 :: String -> m String
binNat4 String
op = String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op] String
"(<<0>> :: Integer -> Integer -> Integer -> Integer -> Integer)"
  binAsis :: String -> String -> m String
binAsis String
op String
ty = String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op, String -> String
opty String
ty] (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"((<<0>>) :: <<1>>)"
  rel' :: String -> String -> String -> m String
rel' String
toTy String
op String
ty = do
    String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op, String
ty, String
toTy] (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
      String
"(\\ x y -> (<<0>> :: <<1>> -> <<1>> -> Bool) (<<2>> x) (<<2>> y))"
  relNat :: String -> m String
relNat String
op = do
    String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
op] (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
      String
"(<<0>> :: Integer -> Integer -> Bool)"
  rel :: String -> String -> m String
rel String
op String
ty  = String -> String -> String -> m String
forall (m :: * -> *).
Monad m =>
String -> String -> String -> m String
rel' String
"" String
op String
ty
  opty :: String -> String
opty String
t = String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"->" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"->" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
  axiom_prims :: [String]
axiom_prims = [String
"primIMin",String
"primIMax",String
"primINeg",String
"primPartial",String
"primPartialP",String
"primPFrom1",String
"primPOr",String
"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
$ String
"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 String
x Term
t = ArgInfo -> Abs Term -> Term
Lam (Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
defaultArgInfo) (String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs String
x Term
t)
  nLam :: String -> Term -> Term
nLam String
x Term
t = ArgInfo -> Abs Term -> Term
Lam (Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden ArgInfo
defaultArgInfo) (String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs String
x Term
t)

noCheckCover :: QName -> TCM Bool
noCheckCover :: QName -> TCM Bool
noCheckCover 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 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 ConHead
q ConInfo
_ Elims
_) = 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 ArgInfo
_ Abs Term
t) = Term -> TCMT IO String
toS (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
t)
  toS Term
_ = String -> TCMT IO String
forall a. String -> a
mazerror (String -> TCMT IO String) -> String -> TCMT IO String
forall a b. (a -> b) -> a -> b
$ String
"pconName" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

bltQual' :: String -> String -> TCM String
bltQual' :: String -> String -> TCMT IO String
bltQual' String
b 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