    {-# OPTIONS_GHC -Wunused-imports #-}

    {-| Primitive functions, such as addition on builtin integers.
    -}

    module Agda.TypeChecking.Primitive
           ( module Agda.TypeChecking.Primitive.Base
           , module Agda.TypeChecking.Primitive.Cubical
           , module Agda.TypeChecking.Primitive
           ) where

    import Data.Char
    import Data.Map (Map)
    import qualified Data.Map as Map
    import qualified Data.Set as Set
    import Data.Maybe
    import Data.Text (Text)
    import qualified Data.Text as T
    import Data.Word

    import qualified Agda.Interaction.Options.Lenses as Lens

    import Agda.Syntax.Common hiding (Nat)
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Generic (TermLike(..))
    import Agda.Syntax.Internal.MetaVars
    import Agda.Syntax.Literal

    import Agda.TypeChecking.Monad hiding (getConstInfo, typeOfConst)
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Reduce.Monad as Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Level

    import Agda.TypeChecking.Quote (quoteTermWithKit, quoteTypeWithKit, quoteDomWithKit, quotingKit)
    import Agda.TypeChecking.Primitive.Base
    import Agda.TypeChecking.Primitive.Cubical
    import Agda.TypeChecking.Warnings

    import Agda.Utils.Char
    import Agda.Utils.Float
    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.Maybe (fromMaybeM)
    import Agda.Utils.Monad
    import Agda.Syntax.Common.Pretty
    import Agda.Utils.Singleton
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    -- Haskell type to Agda type

    newtype Nat = Nat { Nat -> Integer
    unNat :: Integer }
                deriving (Nat -> Nat -> Bool
    (Nat -> Nat -> Bool) -> (Nat -> Nat -> Bool) -> Eq Nat
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Nat -> Nat -> Bool
    == :: Nat -> Nat -> Bool
    $c/= :: Nat -> Nat -> Bool
    /= :: Nat -> Nat -> Bool
    Eq, Eq Nat
    Eq Nat =>
    (Nat -> Nat -> Ordering)
    -> (Nat -> Nat -> Bool)
    -> (Nat -> Nat -> Bool)
    -> (Nat -> Nat -> Bool)
    -> (Nat -> Nat -> Bool)
    -> (Nat -> Nat -> Nat)
    -> (Nat -> Nat -> Nat)
    -> Ord Nat
    Nat -> Nat -> Bool
    Nat -> Nat -> Ordering
    Nat -> Nat -> Nat
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Nat -> Nat -> Ordering
    compare :: Nat -> Nat -> Ordering
    $c< :: Nat -> Nat -> Bool
    < :: Nat -> Nat -> Bool
    $c<= :: Nat -> Nat -> Bool
    <= :: Nat -> Nat -> Bool
    $c> :: Nat -> Nat -> Bool
    > :: Nat -> Nat -> Bool
    $c>= :: Nat -> Nat -> Bool
    >= :: Nat -> Nat -> Bool
    $cmax :: Nat -> Nat -> Nat
    max :: Nat -> Nat -> Nat
    $cmin :: Nat -> Nat -> Nat
    min :: Nat -> Nat -> Nat
    Ord, Integer -> Nat
    Nat -> Nat
    Nat -> Nat -> Nat
    (Nat -> Nat -> Nat)
    -> (Nat -> Nat -> Nat)
    -> (Nat -> Nat -> Nat)
    -> (Nat -> Nat)
    -> (Nat -> Nat)
    -> (Nat -> Nat)
    -> (Integer -> Nat)
    -> Num Nat
    forall a.
    (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (Integer -> a)
    -> Num a
    $c+ :: Nat -> Nat -> Nat
    + :: Nat -> Nat -> Nat
    $c- :: Nat -> Nat -> Nat
    - :: Nat -> Nat -> Nat
    $c* :: Nat -> Nat -> Nat
    * :: Nat -> Nat -> Nat
    $cnegate :: Nat -> Nat
    negate :: Nat -> Nat
    $cabs :: Nat -> Nat
    abs :: Nat -> Nat
    $csignum :: Nat -> Nat
    signum :: Nat -> Nat
    $cfromInteger :: Integer -> Nat
    fromInteger :: Integer -> Nat
    Num, Arity -> Nat
    Nat -> Arity
    Nat -> [Nat]
    Nat -> Nat
    Nat -> Nat -> [Nat]
    Nat -> Nat -> Nat -> [Nat]
    (Nat -> Nat)
    -> (Nat -> Nat)
    -> (Arity -> Nat)
    -> (Nat -> Arity)
    -> (Nat -> [Nat])
    -> (Nat -> Nat -> [Nat])
    -> (Nat -> Nat -> [Nat])
    -> (Nat -> Nat -> Nat -> [Nat])
    -> Enum Nat
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Arity -> a)
    -> (a -> Arity)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: Nat -> Nat
    succ :: Nat -> Nat
    $cpred :: Nat -> Nat
    pred :: Nat -> Nat
    $ctoEnum :: Arity -> Nat
    toEnum :: Arity -> Nat
    $cfromEnum :: Nat -> Arity
    fromEnum :: Nat -> Arity
    $cenumFrom :: Nat -> [Nat]
    enumFrom :: Nat -> [Nat]
    $cenumFromThen :: Nat -> Nat -> [Nat]
    enumFromThen :: Nat -> Nat -> [Nat]
    $cenumFromTo :: Nat -> Nat -> [Nat]
    enumFromTo :: Nat -> Nat -> [Nat]
    $cenumFromThenTo :: Nat -> Nat -> Nat -> [Nat]
    enumFromThenTo :: Nat -> Nat -> Nat -> [Nat]
    Enum, Num Nat
    Ord Nat
    (Num Nat, Ord Nat) => (Nat -> Rational) -> Real Nat
    Nat -> Rational
    forall a. (Num a, Ord a) => (a -> Rational) -> Real a
    $ctoRational :: Nat -> Rational
    toRational :: Nat -> Rational
    Real)

    -- In GHC > 7.8 deriving Integral causes an unnecessary toInteger
    -- warning.
    instance Integral Nat where
      toInteger :: Nat -> Integer
    toInteger = Nat -> Integer
    unNat
      quotRem :: Nat -> Nat -> (Nat, Nat)
    quotRem (Nat Integer
    a) (Nat Integer
    b) = (Integer -> Nat
    Nat Integer
    q, Integer -> Nat
    Nat Integer
    r)
        where (Integer
    q, Integer
    r) = Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    quotRem Integer
    a Integer
    b

    instance TermLike Nat where
      traverseTermM :: forall (m :: * -> *). Monad m => (Term -> m Term) -> Nat -> m Nat
    traverseTermM Term -> m Term
    _ = Nat -> m Nat
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      foldTerm :: forall m. Monoid m => (Term -> m) -> Nat -> m
    foldTerm Term -> m
    _      = Nat -> m
    forall a. Monoid a => a
    mempty

    instance Pretty Nat where
      pretty :: Nat -> Doc
    pretty = Integer -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Integer -> Doc) -> (Nat -> Integer) -> Nat -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    newtype Lvl = Lvl { Lvl -> Integer
    unLvl :: Integer }
      deriving (Lvl -> Lvl -> Bool
    (Lvl -> Lvl -> Bool) -> (Lvl -> Lvl -> Bool) -> Eq Lvl
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Lvl -> Lvl -> Bool
    == :: Lvl -> Lvl -> Bool
    $c/= :: Lvl -> Lvl -> Bool
    /= :: Lvl -> Lvl -> Bool
    Eq, Eq Lvl
    Eq Lvl =>
    (Lvl -> Lvl -> Ordering)
    -> (Lvl -> Lvl -> Bool)
    -> (Lvl -> Lvl -> Bool)
    -> (Lvl -> Lvl -> Bool)
    -> (Lvl -> Lvl -> Bool)
    -> Op Lvl
    -> Op Lvl
    -> Ord Lvl
    Lvl -> Lvl -> Bool
    Lvl -> Lvl -> Ordering
    Op Lvl
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Lvl -> Lvl -> Ordering
    compare :: Lvl -> Lvl -> Ordering
    $c< :: Lvl -> Lvl -> Bool
    < :: Lvl -> Lvl -> Bool
    $c<= :: Lvl -> Lvl -> Bool
    <= :: Lvl -> Lvl -> Bool
    $c> :: Lvl -> Lvl -> Bool
    > :: Lvl -> Lvl -> Bool
    $c>= :: Lvl -> Lvl -> Bool
    >= :: Lvl -> Lvl -> Bool
    $cmax :: Op Lvl
    max :: Op Lvl
    $cmin :: Op Lvl
    min :: Op Lvl
    Ord)

    instance Pretty Lvl where
      pretty :: Lvl -> Doc
    pretty = Integer -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Integer -> Doc) -> (Lvl -> Integer) -> Lvl -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lvl -> Integer
    unLvl

    class PrimType a where
      primType :: a -> TCM Type

      -- This used to be a catch-all instance `PrimType a => PrimTerm a` which required UndecidableInstances.
      -- Now we declare the instances separately, but enforce the catch-all-ness with a superclass constraint on PrimTerm.
      default primType :: PrimTerm a => a -> TCM Type
      primType a
    _ = TCMT IO Term -> TCM Type
    forall (m :: * -> *). Functor m => m Term -> m Type
    el (TCMT IO Term -> TCM Type) -> TCMT IO Term -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ a -> TCMT IO Term
    forall a. PrimTerm a => a -> TCMT IO Term
    primTerm (a
    forall a. HasCallStack => a
    undefined :: a)

    class PrimType a => PrimTerm a where
      primTerm :: a -> TCM Term

    instance (PrimType a, PrimType b) => PrimType (a -> b)
    instance (PrimType a, PrimType b) => PrimTerm (a -> b) where
      primTerm :: (a -> b) -> TCMT IO Term
    primTerm a -> b
    _ = Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> TCM Type -> TCMT IO Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (a -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (a
    forall a. HasCallStack => a
    undefined :: a) TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> b -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (b
    forall a. HasCallStack => a
    undefined :: b))

    instance (PrimType a, PrimType b) => PrimType (a, b)
    instance (PrimType a, PrimType b) => PrimTerm (a, b) where
      primTerm :: (a, b) -> TCMT IO Term
    primTerm (a, b)
    _ = do
        sigKit <- TCMT IO SigmaKit -> TCMT IO (Maybe SigmaKit) -> TCMT IO SigmaKit
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM (TypeError -> TCMT IO SigmaKit
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO SigmaKit) -> TypeError -> TCMT IO SigmaKit
    forall a b. (a -> b) -> a -> b
    $ BuiltinId -> TypeError
    NoBindingForBuiltin BuiltinId
    BuiltinSigma) TCMT IO (Maybe SigmaKit)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m) =>
    m (Maybe SigmaKit)
    getSigmaKit
        let sig = QName -> Elims -> Term
    Def (SigmaKit -> QName
    sigmaName SigmaKit
    sigKit) []
        a'       <- primType (undefined :: a)
        b'       <- primType (undefined :: b)
        Type la  <- pure $ getSort a'
        Type lb  <- pure $ getSort b'
        pure sig <#> pure (Level la)
                 <#> pure (Level lb)
                 <@> pure (unEl a')
                 <@> pure (nolam $ unEl b')

    instance PrimType Integer
    instance PrimTerm Integer where primTerm :: Integer -> TCMT IO Term
    primTerm Integer
    _ = TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primInteger

    instance PrimType Word64
    instance PrimTerm Word64  where primTerm :: Word64 -> TCMT IO Term
    primTerm Word64
    _ = TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primWord64

    instance PrimType Bool
    instance PrimTerm Bool    where primTerm :: Bool -> TCMT IO Term
    primTerm Bool
    _ = TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primBool

    instance PrimType Char
    instance PrimTerm Char    where primTerm :: Char -> TCMT IO Term
    primTerm Char
    _ = TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primChar

    instance PrimType Double
    instance PrimTerm Double  where primTerm :: Double -> TCMT IO Term
    primTerm Double
    _ = TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFloat

    instance PrimType Text
    instance PrimTerm Text    where primTerm :: Text -> TCMT IO Term
    primTerm Text
    _ = TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primString

    instance PrimType Nat
    instance PrimTerm Nat     where primTerm :: Nat -> TCMT IO Term
    primTerm Nat
    _ = TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNat

    instance PrimType Lvl
    instance PrimTerm Lvl     where primTerm :: Lvl -> TCMT IO Term
    primTerm Lvl
    _ = TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevel

    instance PrimType QName
    instance PrimTerm QName   where primTerm :: QName -> TCMT IO Term
    primTerm QName
    _ = TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primQName

    instance PrimType MetaId
    instance PrimTerm MetaId  where primTerm :: MetaId -> TCMT IO Term
    primTerm MetaId
    _ = TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaMeta

    instance PrimType Type
    instance PrimTerm Type    where primTerm :: Type -> TCMT IO Term
    primTerm Type
    _ = TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTerm

    instance PrimType Fixity'
    instance PrimTerm Fixity' where primTerm :: Fixity' -> TCMT IO Term
    primTerm Fixity'
    _ = TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFixity

    instance PrimTerm a => PrimType [a]
    instance PrimTerm a => PrimTerm [a] where
      primTerm :: [a] -> TCMT IO Term
    primTerm [a]
    _ = TCMT IO Term -> TCMT IO Term
    list (a -> TCMT IO Term
    forall a. PrimTerm a => a -> TCMT IO Term
    primTerm (a
    forall a. HasCallStack => a
    undefined :: a))

    instance PrimTerm a => PrimType (Maybe a)
    instance PrimTerm a => PrimTerm (Maybe a) where
      primTerm :: Maybe a -> TCMT IO Term
    primTerm Maybe a
    _ = TCMT IO Term -> TCMT IO Term
    tMaybe (a -> TCMT IO Term
    forall a. PrimTerm a => a -> TCMT IO Term
    primTerm (a
    forall a. HasCallStack => a
    undefined :: a))

    instance PrimTerm a => PrimType (IO a)
    instance PrimTerm a => PrimTerm (IO a) where
      primTerm :: IO a -> TCMT IO Term
    primTerm IO a
    _ = TCMT IO Term -> TCMT IO Term
    io (a -> TCMT IO Term
    forall a. PrimTerm a => a -> TCMT IO Term
    primTerm (a
    forall a. HasCallStack => a
    undefined :: a))

    -- From Agda term to Haskell value

    class ToTerm a where
      toTerm  :: TCM (a -> ReduceM Term)

    toTermTCM :: ToTerm a => TCM (a -> TCM Term)
    toTermTCM :: forall a. ToTerm a => TCM (a -> TCMT IO Term)
    toTermTCM = (ReduceM Term -> TCMT IO Term
    forall a. ReduceM a -> TCM a
    runReduceM (ReduceM Term -> TCMT IO Term)
    -> (a -> ReduceM Term) -> a -> TCMT IO Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .) ((a -> ReduceM Term) -> a -> TCMT IO Term)
    -> TCMT IO (a -> ReduceM Term) -> TCMT IO (a -> TCMT IO Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (a -> ReduceM Term)
    forall a. ToTerm a => TCM (a -> ReduceM Term)
    toTerm

    instance ToTerm Nat     where toTerm :: TCM (Nat -> ReduceM Term)
    toTerm = (Nat -> ReduceM Term) -> TCM (Nat -> ReduceM Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Nat -> ReduceM Term) -> TCM (Nat -> ReduceM Term))
    -> (Nat -> ReduceM Term) -> TCM (Nat -> ReduceM Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ReduceM Term) -> (Nat -> Term) -> Nat -> ReduceM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Literal -> Term
    Lit (Literal -> Term) -> (Nat -> Literal) -> Nat -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Literal
    LitNat (Integer -> Literal) -> (Nat -> Integer) -> Nat -> Literal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Integer
    forall a. Integral a => a -> Integer
    toInteger
    instance ToTerm Word64  where toTerm :: TCM (Word64 -> ReduceM Term)
    toTerm = (Word64 -> ReduceM Term) -> TCM (Word64 -> ReduceM Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Word64 -> ReduceM Term) -> TCM (Word64 -> ReduceM Term))
    -> (Word64 -> ReduceM Term) -> TCM (Word64 -> ReduceM Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ReduceM Term)
    -> (Word64 -> Term) -> Word64 -> ReduceM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Literal -> Term
    Lit (Literal -> Term) -> (Word64 -> Literal) -> Word64 -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word64 -> Literal
    LitWord64
    instance ToTerm Lvl     where toTerm :: TCM (Lvl -> ReduceM Term)
    toTerm = (Lvl -> ReduceM Term) -> TCM (Lvl -> ReduceM Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Lvl -> ReduceM Term) -> TCM (Lvl -> ReduceM Term))
    -> (Lvl -> ReduceM Term) -> TCM (Lvl -> ReduceM Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ReduceM Term) -> (Lvl -> Term) -> Lvl -> ReduceM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Level' Term -> Term
    Level (Level' Term -> Term) -> (Lvl -> Level' Term) -> Lvl -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Level' Term
    ClosedLevel (Integer -> Level' Term) -> (Lvl -> Integer) -> Lvl -> Level' Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lvl -> Integer
    unLvl
    instance ToTerm Double  where toTerm :: TCM (Double -> ReduceM Term)
    toTerm = (Double -> ReduceM Term) -> TCM (Double -> ReduceM Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Double -> ReduceM Term) -> TCM (Double -> ReduceM Term))
    -> (Double -> ReduceM Term) -> TCM (Double -> ReduceM Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ReduceM Term)
    -> (Double -> Term) -> Double -> ReduceM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Literal -> Term
    Lit (Literal -> Term) -> (Double -> Literal) -> Double -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Double -> Literal
    LitFloat
    instance ToTerm Char    where toTerm :: TCM (Char -> ReduceM Term)
    toTerm = (Char -> ReduceM Term) -> TCM (Char -> ReduceM Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Char -> ReduceM Term) -> TCM (Char -> ReduceM Term))
    -> (Char -> ReduceM Term) -> TCM (Char -> ReduceM Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ReduceM Term) -> (Char -> Term) -> Char -> ReduceM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Literal -> Term
    Lit (Literal -> Term) -> (Char -> Literal) -> Char -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> Literal
    LitChar
    instance ToTerm Text    where toTerm :: TCM (Text -> ReduceM Term)
    toTerm = (Text -> ReduceM Term) -> TCM (Text -> ReduceM Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Text -> ReduceM Term) -> TCM (Text -> ReduceM Term))
    -> (Text -> ReduceM Term) -> TCM (Text -> ReduceM Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ReduceM Term) -> (Text -> Term) -> Text -> ReduceM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Literal -> Term
    Lit (Literal -> Term) -> (Text -> Literal) -> Text -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Literal
    LitString
    instance ToTerm QName   where toTerm :: TCM (QName -> ReduceM Term)
    toTerm = (QName -> ReduceM Term) -> TCM (QName -> ReduceM Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((QName -> ReduceM Term) -> TCM (QName -> ReduceM Term))
    -> (QName -> ReduceM Term) -> TCM (QName -> ReduceM Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ReduceM Term) -> (QName -> Term) -> QName -> ReduceM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Literal -> Term
    Lit (Literal -> Term) -> (QName -> Literal) -> QName -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Literal
    LitQName
    instance ToTerm MetaId  where
      toTerm :: TCM (MetaId -> ReduceM Term)
    toTerm = do
        top <- TopLevelModuleName
    -> Maybe TopLevelModuleName -> TopLevelModuleName
    forall a. a -> Maybe a -> a
    fromMaybe TopLevelModuleName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe TopLevelModuleName -> TopLevelModuleName)
    -> TCMT IO (Maybe TopLevelModuleName) -> TCMT IO TopLevelModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Maybe TopLevelModuleName)
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    m (Maybe TopLevelModuleName)
    currentTopLevelModule
        return $ pure . Lit . LitMeta top

    instance ToTerm Integer where
      toTerm :: TCM (Integer -> ReduceM Term)
    toTerm = do
        pos     <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIntegerPos
        negsuc  <- primIntegerNegSuc
        fromNat <- toTerm @Nat
        let intToTerm = Nat -> ReduceM Term
    fromNat (Nat -> ReduceM Term)
    -> (Integer -> Nat) -> Integer -> ReduceM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . forall a b. (Integral a, Num b) => a -> b
    fromIntegral @Integer
        let fromInt Integer
    n | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    0    = Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    apply1 Term
    pos    (Term -> Term) -> ReduceM Term -> ReduceM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Integer -> ReduceM Term
    intToTerm Integer
    n
                      | Bool
    otherwise = Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    apply1 Term
    negsuc (Term -> Term) -> ReduceM Term -> ReduceM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Integer -> ReduceM Term
    intToTerm (-Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1)
        return fromInt

    instance ToTerm Bool where
      toTerm :: TCM (Bool -> ReduceM Term)
    toTerm = do
        true  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primTrue
        false <- primFalse
        return $ \Bool
    b -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ReduceM Term) -> Term -> ReduceM Term
    forall a b. (a -> b) -> a -> b
    $ if Bool
    b then Term
    true else Term
    false

    instance ToTerm Term where
      toTerm :: TCM (Term -> ReduceM Term)
    toTerm = do QuotingKit -> Term -> ReduceM Term
    quoteTermWithKit (QuotingKit -> Term -> ReduceM Term)
    -> TCMT IO QuotingKit -> TCM (Term -> ReduceM Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO QuotingKit
    quotingKit

    instance ToTerm (Dom Type) where
      toTerm :: TCM (Dom Type -> ReduceM Term)
    toTerm = do QuotingKit -> Dom Type -> ReduceM Term
    quoteDomWithKit (QuotingKit -> Dom Type -> ReduceM Term)
    -> TCMT IO QuotingKit -> TCM (Dom Type -> ReduceM Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO QuotingKit
    quotingKit

    instance ToTerm Type where
      toTerm :: TCM (Type -> ReduceM Term)
    toTerm = QuotingKit -> Type -> ReduceM Term
    quoteTypeWithKit (QuotingKit -> Type -> ReduceM Term)
    -> TCMT IO QuotingKit -> TCM (Type -> ReduceM Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO QuotingKit
    quotingKit

    instance ToTerm ArgInfo where
      toTerm :: TCM (ArgInfo -> ReduceM Term)
    toTerm = do
        info <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primArgArgInfo
        vis  <- primVisible
        hid  <- primHidden
        ins  <- primInstance
        rel  <- primRelevant
        irr  <- primIrrelevant
        return $ \ ArgInfo
    i -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ReduceM Term) -> Term -> ReduceM Term
    forall a b. (a -> b) -> a -> b
    $ Term
    info Term -> [Term] -> Term
    forall t. Apply t => t -> [Term] -> t
    `applys`
          [ case ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    i of
              Hiding
    NotHidden  -> Term
    vis
              Hiding
    Hidden     -> Term
    hid
              Instance{} -> Term
    ins
          , case ArgInfo -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance ArgInfo
    i of
              Relevant        {} -> Term
    rel
              Irrelevant      {} -> Term
    irr
              ShapeIrrelevant {} -> Term
    rel
          ]

    instance ToTerm Fixity' where
      toTerm :: TCM (Fixity' -> ReduceM Term)
    toTerm = ((Fixity -> ReduceM Term)
    -> (Fixity' -> Fixity) -> Fixity' -> ReduceM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Fixity' -> Fixity
    theFixity) ((Fixity -> ReduceM Term) -> Fixity' -> ReduceM Term)
    -> TCMT IO (Fixity -> ReduceM Term)
    -> TCM (Fixity' -> ReduceM Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Fixity -> ReduceM Term)
    forall a. ToTerm a => TCM (a -> ReduceM Term)
    toTerm

    instance ToTerm Fixity where
      toTerm :: TCMT IO (Fixity -> ReduceM Term)
    toTerm = do
        lToTm  <- TCM (FixityLevel -> ReduceM Term)
    forall a. ToTerm a => TCM (a -> ReduceM Term)
    toTerm
        aToTm  <- toTerm
        fixity <- primFixityFixity
        return $ \ Fixity{fixityAssoc :: Fixity -> Associativity
    fixityAssoc = Associativity
    a, fixityLevel :: Fixity -> FixityLevel
    fixityLevel = FixityLevel
    l} ->
          Term -> Term -> Term -> Term
    forall t. Apply t => t -> Term -> Term -> t
    apply2 Term
    fixity (Term -> Term -> Term) -> ReduceM Term -> ReduceM (Term -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Associativity -> ReduceM Term
    aToTm Associativity
    a ReduceM (Term -> Term) -> ReduceM Term -> ReduceM Term
    forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> FixityLevel -> ReduceM Term
    lToTm FixityLevel
    l

    instance ToTerm Associativity where
      toTerm :: TCM (Associativity -> ReduceM Term)
    toTerm = do
        lassoc <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAssocLeft
        rassoc <- primAssocRight
        nassoc <- primAssocNon
        return $ \ Associativity
    a -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ReduceM Term) -> Term -> ReduceM Term
    forall a b. (a -> b) -> a -> b
    $
          case Associativity
    a of
            Associativity
    NonAssoc   -> Term
    nassoc
            Associativity
    LeftAssoc  -> Term
    lassoc
            Associativity
    RightAssoc -> Term
    rassoc

    instance ToTerm Blocker where
      toTerm :: TCM (Blocker -> ReduceM Term)
    toTerm = do
        all <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaBlockerAll
        any <- primAgdaBlockerAny
        meta <- primAgdaBlockerMeta
        lists <- buildList
        metaTm <- toTerm
        let go (UnblockOnAny Set Blocker
    xs)    = Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    apply1 Term
    any (Term -> Term) -> ([Term] -> Term) -> [Term] -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Term] -> Term
    lists ([Term] -> Term) -> ReduceM [Term] -> ReduceM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Blocker -> ReduceM Term) -> [Blocker] -> ReduceM [Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Blocker -> ReduceM Term
    go (Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    xs)
            go (UnblockOnAll Set Blocker
    xs)    = Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    apply1 Term
    all (Term -> Term) -> ([Term] -> Term) -> [Term] -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Term] -> Term
    lists ([Term] -> Term) -> ReduceM [Term] -> ReduceM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Blocker -> ReduceM Term) -> [Blocker] -> ReduceM [Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Blocker -> ReduceM Term
    go (Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    xs)
            go (UnblockOnMeta MetaId
    m)    = Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    apply1 Term
    meta (Term -> Term) -> ReduceM Term -> ReduceM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> ReduceM Term
    metaTm MetaId
    m
            go (UnblockOnDef QName
    _)     = ReduceM Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            go (UnblockOnProblem ProblemId
    _) = ReduceM Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        pure go

    instance ToTerm FixityLevel where
      toTerm :: TCM (FixityLevel -> ReduceM Term)
    toTerm = do
        iToTm <- TCM (Double -> ReduceM Term)
    forall a. ToTerm a => TCM (a -> ReduceM Term)
    toTerm
        related   <- primPrecRelated
        unrelated <- primPrecUnrelated
        return $ \ FixityLevel
    p ->
          case FixityLevel
    p of
            FixityLevel
    Unrelated -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unrelated
            Related Double
    n -> Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    apply1 Term
    related (Term -> Term) -> ReduceM Term -> ReduceM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Double -> ReduceM Term
    iToTm Double
    n

    instance (ToTerm a, ToTerm b) => ToTerm (a, b) where
      toTerm :: TCM ((a, b) -> ReduceM Term)
    toTerm = do
        sigKit <- SigmaKit -> Maybe SigmaKit -> SigmaKit
    forall a. a -> Maybe a -> a
    fromMaybe SigmaKit
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe SigmaKit -> SigmaKit)
    -> TCMT IO (Maybe SigmaKit) -> TCMT IO SigmaKit
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Maybe SigmaKit)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m) =>
    m (Maybe SigmaKit)
    getSigmaKit
        let con = ConHead -> ConInfo -> Elims -> Term
    Con (SigmaKit -> ConHead
    sigmaCon SigmaKit
    sigKit) ConInfo
    ConOSystem []
        fromA <- toTerm
        fromB <- toTerm
        pure $ \ (a
    a, b
    b) -> Term -> Term -> Term -> Term
    forall t. Apply t => t -> Term -> Term -> t
    apply2 Term
    con (Term -> Term -> Term) -> ReduceM Term -> ReduceM (Term -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> ReduceM Term
    fromA a
    a ReduceM (Term -> Term) -> ReduceM Term -> ReduceM Term
    forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> ReduceM Term
    fromB b
    b

    -- | @buildList A ts@ builds a list of type @List A@. Assumes that the terms
    --   @ts@ all have type @A@.
    buildList :: TCM ([Term] -> Term)
    buildList :: TCM ([Term] -> Term)
    buildList = do
        nil'  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNil
        cons' <- primCons
        let nil       = Term
    nil'
            cons Term
    x Term
    xs = Term
    cons' Term -> [Term] -> Term
    forall t. Apply t => t -> [Term] -> t
    `applys` [Term
    x, Term
    xs]
        return $ foldr cons nil

    instance ToTerm a => ToTerm [a] where
      toTerm :: TCM ([a] -> ReduceM Term)
    toTerm = do
        mkList <- TCM ([Term] -> Term)
    buildList
        fromA  <- toTerm
        return $ mkList <.> mapM fromA

    instance ToTerm a => ToTerm (Maybe a) where
      toTerm :: TCM (Maybe a -> ReduceM Term)
    toTerm = do
        nothing <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNothing
        just    <- primJust
        fromA   <- toTerm
        return $ maybe (pure nothing) (apply1 just <.> fromA)

    -- From Haskell value to Agda term

    type FromTermFunction a = Arg Term ->
                              ReduceM (Reduced (MaybeReduced (Arg Term)) a)

    class FromTerm a where
      fromTerm :: TCM (FromTermFunction a)

    instance FromTerm Integer where
      fromTerm :: TCM (FromTermFunction Integer)
    fromTerm = do
        Con pos _    [] <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIntegerPos
        Con negsuc _ [] <- primIntegerNegSuc
        toNat         <- fromTerm :: TCM (FromTermFunction Nat)
        return $ \ Arg Term
    v -> do
          b <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    v
          let v'  = Blocked (Arg Term) -> Arg Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked (Arg Term)
    b
              arg = (Term -> Arg Term -> Arg Term
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg Term
    v')
          case unArg (ignoreBlocking b) of
            Con ConHead
    c ConInfo
    ci [Apply Arg Term
    u]
              | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    pos    ->
                ReduceM (Reduced (MaybeReduced (Arg Term)) Nat)
    -> (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
    -> (Nat -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction Nat
    toNat Arg Term
    u)
                  (\ MaybeReduced (Arg Term)
    u' -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
    -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced (Arg Term -> MaybeReduced (Arg Term))
    -> Arg Term -> MaybeReduced (Arg Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    arg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci [Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
    forall a b. (a -> b) -> a -> b
    $ MaybeReduced (Arg Term) -> Arg Term
    forall a. MaybeReduced a -> a
    ignoreReduced MaybeReduced (Arg Term)
    u']) ((Nat -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
     -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
    -> (Nat -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
    forall a b. (a -> b) -> a -> b
    $ \ Nat
    n ->
                Integer -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Integer -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
    -> Integer -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
    forall a b. (a -> b) -> a -> b
    $ Nat -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Nat
    n
              | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    negsuc ->
                ReduceM (Reduced (MaybeReduced (Arg Term)) Nat)
    -> (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
    -> (Nat -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction Nat
    toNat Arg Term
    u)
                  (\ MaybeReduced (Arg Term)
    u' -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
    -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced (Arg Term -> MaybeReduced (Arg Term))
    -> Arg Term -> MaybeReduced (Arg Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    arg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci [Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
    forall a b. (a -> b) -> a -> b
    $ MaybeReduced (Arg Term) -> Arg Term
    forall a. MaybeReduced a -> a
    ignoreReduced MaybeReduced (Arg Term)
    u']) ((Nat -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
     -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
    -> (Nat -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
    forall a b. (a -> b) -> a -> b
    $ \ Nat
    n ->
                Integer -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Integer -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
    -> Integer -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
    forall a b. (a -> b) -> a -> b
    $ Nat -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Nat -> Integer) -> Nat -> Integer
    forall a b. (a -> b) -> a -> b
    $ -Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1
            Term
    _ -> Reduced (MaybeReduced (Arg Term)) Integer
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (MaybeReduced (Arg Term)) Integer
     -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
    -> Reduced (MaybeReduced (Arg Term)) Integer
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
    forall a b. (a -> b) -> a -> b
    $ MaybeReduced (Arg Term)
    -> Reduced (MaybeReduced (Arg Term)) Integer
    forall no yes. no -> Reduced no yes
    NoReduction (Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    b)

    instance FromTerm Nat where
      fromTerm :: TCM (FromTermFunction Nat)
    fromTerm = (Literal -> Maybe Nat) -> TCM (FromTermFunction Nat)
    forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
    fromLiteral ((Literal -> Maybe Nat) -> TCM (FromTermFunction Nat))
    -> (Literal -> Maybe Nat) -> TCM (FromTermFunction Nat)
    forall a b. (a -> b) -> a -> b
    $ \case
        LitNat Integer
    n -> Nat -> Maybe Nat
    forall a. a -> Maybe a
    Just (Nat -> Maybe Nat) -> Nat -> Maybe Nat
    forall a b. (a -> b) -> a -> b
    $ Integer -> Nat
    forall a. Num a => Integer -> a
    fromInteger Integer
    n
        Literal
    _ -> Maybe Nat
    forall a. Maybe a
    Nothing

    instance FromTerm Word64 where
      fromTerm :: TCM (FromTermFunction Word64)
    fromTerm = (Literal -> Maybe Word64) -> TCM (FromTermFunction Word64)
    forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
    fromLiteral ((Literal -> Maybe Word64) -> TCM (FromTermFunction Word64))
    -> (Literal -> Maybe Word64) -> TCM (FromTermFunction Word64)
    forall a b. (a -> b) -> a -> b
    $ \ case
        LitWord64 Word64
    n -> Word64 -> Maybe Word64
    forall a. a -> Maybe a
    Just Word64
    n
        Literal
    _ -> Maybe Word64
    forall a. Maybe a
    Nothing

    instance FromTerm Lvl where
      fromTerm :: TCM (FromTermFunction Lvl)
    fromTerm = (Term -> Maybe Lvl) -> TCM (FromTermFunction Lvl)
    forall a. (Term -> Maybe a) -> TCM (FromTermFunction a)
    fromReducedTerm ((Term -> Maybe Lvl) -> TCM (FromTermFunction Lvl))
    -> (Term -> Maybe Lvl) -> TCM (FromTermFunction Lvl)
    forall a b. (a -> b) -> a -> b
    $ \case
        Level (ClosedLevel Integer
    n) -> Lvl -> Maybe Lvl
    forall a. a -> Maybe a
    Just (Lvl -> Maybe Lvl) -> Lvl -> Maybe Lvl
    forall a b. (a -> b) -> a -> b
    $ Integer -> Lvl
    Lvl Integer
    n
        Term
    _ -> Maybe Lvl
    forall a. Maybe a
    Nothing

    instance FromTerm Double where
      fromTerm :: TCM (FromTermFunction Double)
    fromTerm = (Literal -> Maybe Double) -> TCM (FromTermFunction Double)
    forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
    fromLiteral ((Literal -> Maybe Double) -> TCM (FromTermFunction Double))
    -> (Literal -> Maybe Double) -> TCM (FromTermFunction Double)
    forall a b. (a -> b) -> a -> b
    $ \case
        LitFloat Double
    x -> Double -> Maybe Double
    forall a. a -> Maybe a
    Just Double
    x
        Literal
    _ -> Maybe Double
    forall a. Maybe a
    Nothing

    instance FromTerm Char where
      fromTerm :: TCM (FromTermFunction Char)
    fromTerm = (Literal -> Maybe Char) -> TCM (FromTermFunction Char)
    forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
    fromLiteral ((Literal -> Maybe Char) -> TCM (FromTermFunction Char))
    -> (Literal -> Maybe Char) -> TCM (FromTermFunction Char)
    forall a b. (a -> b) -> a -> b
    $ \case
        LitChar Char
    c -> Char -> Maybe Char
    forall a. a -> Maybe a
    Just Char
    c
        Literal
    _ -> Maybe Char
    forall a. Maybe a
    Nothing

    instance FromTerm Text where
      fromTerm :: TCM (FromTermFunction Text)
    fromTerm = (Literal -> Maybe Text) -> TCM (FromTermFunction Text)
    forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
    fromLiteral ((Literal -> Maybe Text) -> TCM (FromTermFunction Text))
    -> (Literal -> Maybe Text) -> TCM (FromTermFunction Text)
    forall a b. (a -> b) -> a -> b
    $ \case
        LitString Text
    s -> Text -> Maybe Text
    forall a. a -> Maybe a
    Just Text
    s
        Literal
    _ -> Maybe Text
    forall a. Maybe a
    Nothing

    instance FromTerm QName where
      fromTerm :: TCM (FromTermFunction QName)
    fromTerm = (Literal -> Maybe QName) -> TCM (FromTermFunction QName)
    forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
    fromLiteral ((Literal -> Maybe QName) -> TCM (FromTermFunction QName))
    -> (Literal -> Maybe QName) -> TCM (FromTermFunction QName)
    forall a b. (a -> b) -> a -> b
    $ \case
        LitQName QName
    x -> QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    x
        Literal
    _ -> Maybe QName
    forall a. Maybe a
    Nothing

    instance FromTerm MetaId where
      fromTerm :: TCM (FromTermFunction MetaId)
    fromTerm = (Literal -> Maybe MetaId) -> TCM (FromTermFunction MetaId)
    forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
    fromLiteral ((Literal -> Maybe MetaId) -> TCM (FromTermFunction MetaId))
    -> (Literal -> Maybe MetaId) -> TCM (FromTermFunction MetaId)
    forall a b. (a -> b) -> a -> b
    $ \case
        LitMeta TopLevelModuleName
    _ MetaId
    x -> MetaId -> Maybe MetaId
    forall a. a -> Maybe a
    Just MetaId
    x
        Literal
    _ -> Maybe MetaId
    forall a. Maybe a
    Nothing

    instance FromTerm Bool where
        fromTerm :: TCM (FromTermFunction Bool)
    fromTerm = do
            true  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primTrue
            false <- primFalse
            fromReducedTerm $ \case
                Term
    t   | Term
    t Term -> Term -> Bool
    =?= Term
    true  -> Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
                    | Term
    t Term -> Term -> Bool
    =?= Term
    false -> Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
                    | Bool
    otherwise   -> Maybe Bool
    forall a. Maybe a
    Nothing
            where
                Term
    a =?= :: Term -> Term -> Bool
    =?= Term
    b = Term
    a Term -> Term -> Bool
    === Term
    b
                Def QName
    x [] === :: Term -> Term -> Bool
    === Def QName
    y []   = QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    y
                Con ConHead
    x ConInfo
    _ [] === Con ConHead
    y ConInfo
    _ [] = ConHead
    x ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    y
                Var Arity
    n [] === Var Arity
    m []   = Arity
    n Arity -> Arity -> Bool
    forall a. Eq a => a -> a -> Bool
    == Arity
    m
                Term
    _        === Term
    _          = Bool
    False

    instance (ToTerm a, FromTerm a) => FromTerm [a] where
      fromTerm :: TCM (FromTermFunction [a])
    fromTerm = do
        nil   <- Term -> ConHead
    isCon (Term -> ConHead) -> TCMT IO Term -> TCMT IO ConHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNil
        cons  <- isCon <$> primCons
        toA   <- fromTerm
        mkList nil cons toA <$> toTerm
        where
          isCon :: Term -> ConHead
    isCon (Lam ArgInfo
    _ Abs Term
    b)   = Term -> ConHead
    isCon (Term -> ConHead) -> Term -> ConHead
    forall a b. (a -> b) -> a -> b
    $ Abs Term -> Term
    forall a. Subst a => Abs a -> a
    absBody Abs Term
    b
          isCon (Con ConHead
    c ConInfo
    _ Elims
    _) = ConHead
    c
          isCon Term
    v           = ConHead
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          mkList :: ConHead
    -> ConHead
    -> (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
    -> (a -> ReduceM Term)
    -> Arg Term
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    mkList ConHead
    nil ConHead
    cons Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    toA a -> ReduceM Term
    fromA Arg Term
    t = do
            b <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    t
            let t = Blocked (Arg Term) -> Arg Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked (Arg Term)
    b
            let arg = (Term -> Arg Term -> Arg Term
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg Term
    t)
            case unArg t of
              Con ConHead
    c ConInfo
    ci []
                | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    nil  -> Reduced (MaybeReduced (Arg Term)) [a]
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (MaybeReduced (Arg Term)) [a]
     -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
    -> Reduced (MaybeReduced (Arg Term)) [a]
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    forall a b. (a -> b) -> a -> b
    $ Simplification -> [a] -> Reduced (MaybeReduced (Arg Term)) [a]
    forall no yes. Simplification -> yes -> Reduced no yes
    YesReduction Simplification
    NoSimplification []
              Con ConHead
    c ConInfo
    ci Elims
    es
                | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    cons, Just [Arg Term
    x,Arg Term
    xs] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
                  ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
    -> (a -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    toA Arg Term
    x)
                      (\MaybeReduced (Arg Term)
    x' -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
    -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced (Arg Term -> MaybeReduced (Arg Term))
    -> Arg Term -> MaybeReduced (Arg Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    arg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply [MaybeReduced (Arg Term) -> Arg Term
    forall a. MaybeReduced a -> a
    ignoreReduced MaybeReduced (Arg Term)
    x',Arg Term
    xs])) ((a -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
     -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
    -> (a -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    forall a b. (a -> b) -> a -> b
    $ \a
    y ->
                  ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    -> (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
    -> ([a] -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind
                      (ConHead
    -> ConHead
    -> (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
    -> (a -> ReduceM Term)
    -> Arg Term
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    mkList ConHead
    nil ConHead
    cons Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    toA a -> ReduceM Term
    fromA Arg Term
    xs)
                      (\ MaybeReduced (Arg Term)
    xsR -> do
                        yTm <- a -> ReduceM Term
    fromA a
    y
                        pure $ for xsR $ \Arg Term
    xs' -> Term -> Arg Term
    arg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply [Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    yTm, Arg Term
    xs'])) (([a] -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
     -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
    -> ([a] -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    forall a b. (a -> b) -> a -> b
    $ \[a]
    ys ->
                  [a] -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (a
    y a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    ys)
              Term
    _ -> Reduced (MaybeReduced (Arg Term)) [a]
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (MaybeReduced (Arg Term)) [a]
     -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
    -> Reduced (MaybeReduced (Arg Term)) [a]
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    forall a b. (a -> b) -> a -> b
    $ MaybeReduced (Arg Term) -> Reduced (MaybeReduced (Arg Term)) [a]
    forall no yes. no -> Reduced no yes
    NoReduction (Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    b)

    instance FromTerm a => FromTerm (Maybe a) where
      fromTerm :: TCM (FromTermFunction (Maybe a))
    fromTerm = do
        nothing <- Term -> ConHead
    isCon (Term -> ConHead) -> TCMT IO Term -> TCMT IO ConHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNothing
        just    <- isCon <$> primJust
        toA     <- fromTerm
        return $ \ Arg Term
    t -> do
          let arg :: Term -> Arg Term
    arg = (Term -> Arg Term -> Arg Term
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg Term
    t)
          b <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    t
          let t = Blocked (Arg Term) -> Arg Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked (Arg Term)
    b
          case unArg t of
            Con ConHead
    c ConInfo
    ci []
              | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    nothing -> Reduced (MaybeReduced (Arg Term)) (Maybe a)
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (MaybeReduced (Arg Term)) (Maybe a)
     -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a)))
    -> Reduced (MaybeReduced (Arg Term)) (Maybe a)
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ Simplification
    -> Maybe a -> Reduced (MaybeReduced (Arg Term)) (Maybe a)
    forall no yes. Simplification -> yes -> Reduced no yes
    YesReduction Simplification
    NoSimplification Maybe a
    forall a. Maybe a
    Nothing
            Con ConHead
    c ConInfo
    ci Elims
    es
              | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    just, Just [Arg Term
    x] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
                ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
    -> (a -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a)))
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction a
    toA Arg Term
    x)
                  (\ MaybeReduced (Arg Term)
    x' -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
    -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced (Arg Term -> MaybeReduced (Arg Term))
    -> Arg Term -> MaybeReduced (Arg Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    arg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci [Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (MaybeReduced (Arg Term) -> Arg Term
    forall a. MaybeReduced a -> a
    ignoreReduced MaybeReduced (Arg Term)
    x')])
                  (Maybe a -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Maybe a -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a)))
    -> (a -> Maybe a)
    -> a
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Maybe a
    forall a. a -> Maybe a
    Just)
            Term
    _ -> Reduced (MaybeReduced (Arg Term)) (Maybe a)
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (MaybeReduced (Arg Term)) (Maybe a)
     -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a)))
    -> Reduced (MaybeReduced (Arg Term)) (Maybe a)
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ MaybeReduced (Arg Term)
    -> Reduced (MaybeReduced (Arg Term)) (Maybe a)
    forall no yes. no -> Reduced no yes
    NoReduction (Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    b)

        where
          isCon :: Term -> ConHead
    isCon (Lam ArgInfo
    _ Abs Term
    b)   = Term -> ConHead
    isCon (Term -> ConHead) -> Term -> ConHead
    forall a b. (a -> b) -> a -> b
    $ Abs Term -> Term
    forall a. Subst a => Abs a -> a
    absBody Abs Term
    b
          isCon (Con ConHead
    c ConInfo
    _ Elims
    _) = ConHead
    c
          isCon Term
    v           = ConHead
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a)
    fromReducedTerm :: forall a. (Term -> Maybe a) -> TCM (FromTermFunction a)
    fromReducedTerm Term -> Maybe a
    f = FromTermFunction a -> TCMT IO (FromTermFunction a)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (FromTermFunction a -> TCMT IO (FromTermFunction a))
    -> FromTermFunction a -> TCMT IO (FromTermFunction a)
    forall a b. (a -> b) -> a -> b
    $ \Arg Term
    t -> do
        b <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    t
        case f $ unArg (ignoreBlocking b) of
            Just a
    x  -> Reduced (MaybeReduced (Arg Term)) a
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (MaybeReduced (Arg Term)) a
     -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
    -> Reduced (MaybeReduced (Arg Term)) a
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    forall a b. (a -> b) -> a -> b
    $ Simplification -> a -> Reduced (MaybeReduced (Arg Term)) a
    forall no yes. Simplification -> yes -> Reduced no yes
    YesReduction Simplification
    NoSimplification a
    x
            Maybe a
    Nothing -> Reduced (MaybeReduced (Arg Term)) a
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (MaybeReduced (Arg Term)) a
     -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
    -> Reduced (MaybeReduced (Arg Term)) a
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    forall a b. (a -> b) -> a -> b
    $ MaybeReduced (Arg Term) -> Reduced (MaybeReduced (Arg Term)) a
    forall no yes. no -> Reduced no yes
    NoReduction (Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    b)

    fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a)
    fromLiteral :: forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
    fromLiteral Literal -> Maybe a
    f = (Term -> Maybe a) -> TCM (FromTermFunction a)
    forall a. (Term -> Maybe a) -> TCM (FromTermFunction a)
    fromReducedTerm ((Term -> Maybe a) -> TCM (FromTermFunction a))
    -> (Term -> Maybe a) -> TCM (FromTermFunction a)
    forall a b. (a -> b) -> a -> b
    $ \case
        Lit Literal
    lit -> Literal -> Maybe a
    f Literal
    lit
        Term
    _       -> Maybe a
    forall a. Maybe a
    Nothing

    -- | @mkPrimInjective@ takes two Set0 @a@ and @b@ and a function @f@ of type
    --   @a -> b@ and outputs a primitive internalizing the fact that @f@ is injective.
    mkPrimInjective :: Type -> Type -> QName -> TCM PrimitiveImpl
    mkPrimInjective :: Type -> Type -> QName -> TCM PrimitiveImpl
    mkPrimInjective Type
    a Type
    b QName
    qn = do
      -- Define the type
      eqName <- TCM QName
    primEqualityName
      let lvl0     = Integer -> Level' Term
    ClosedLevel Integer
    0
      let eq Type
    a TCMT IO Term
    t TCMT IO Term
    u = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Level' Term -> Sort' Term
    forall t. Level' t -> Sort' t
    Type Level' Term
    lvl0) (Term -> Type) -> TCMT IO Term -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> TCMT IO Term
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (QName -> Elims -> Term
    Def QName
    eqName []) TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> Term -> TCMT IO Term
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Level' Term -> Term
    Level Level' Term
    lvl0)
                                    TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> Term -> TCMT IO Term
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    a) TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> TCMT IO Term
    t TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> TCMT IO Term
    u
      let f    = Term -> TCMT IO Term
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (QName -> Elims -> Term
    Def QName
    qn [])
      ty <- nPi "t" (pure a) $ nPi "u" (pure a) $
                  (eq b (f <@> varM 1) (f <@> varM 0))
              --> (eq a (      varM 1) (      varM 0))

        -- Get the constructor corresponding to BUILTIN REFL
      refl <- getRefl

      -- Implementation: when the equality argument reduces to refl so does the primitive.
      -- If the user want the primitive to reduce whenever the two values are equal (no
      -- matter whether the equality is refl), they can combine it with @eraseEquality@.
      return $ PrimImpl ty $ primFun __IMPOSSIBLE__ 3 $ \ [Arg Term]
    ts -> do
        let t :: Arg Term
    t  = Arg Term -> [Arg Term] -> Arg Term
    forall a. a -> [a] -> a
    headWithDefault Arg Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Arg Term]
    ts
        let eq :: Term
    eq = Arg Term -> Term
    forall e. Arg e -> e
    unArg (Arg Term -> Term) -> Arg Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Maybe (Arg Term) -> Arg Term
    forall a. a -> Maybe a -> a
    fromMaybe Arg Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (Arg Term) -> Arg Term) -> Maybe (Arg Term) -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ [Arg Term] -> Maybe (Arg Term)
    forall a. [a] -> Maybe a
    lastMaybe [Arg Term]
    ts
        Term -> ReduceM Term
    forall t. Reduce t => t -> ReduceM t
    reduce' Term
    eq ReduceM Term
    -> (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. ReduceM a -> (a -> ReduceM b) -> ReduceM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Con{} -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    refl Arg Term
    t
          Term
    _     -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced MaybeReducedArgs Term
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ MaybeReducedArgs -> Reduced MaybeReducedArgs Term
    forall no yes. no -> Reduced no yes
    NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
    -> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> MaybeReduced (Arg Term))
    -> [Arg Term] -> MaybeReducedArgs
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced [Arg Term]
    ts

    -- | Converts 'MetaId's to natural numbers.

    metaToNat :: MetaId -> Nat
    metaToNat :: MetaId -> Nat
    metaToNat MetaId
    m =
      Word64 -> Nat
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (ModuleNameHash -> Word64
    moduleNameHash (ModuleNameHash -> Word64) -> ModuleNameHash -> Word64
    forall a b. (a -> b) -> a -> b
    $ MetaId -> ModuleNameHash
    metaModule MetaId
    m) Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    * Nat
    2 Nat -> Integer -> Nat
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Integer
    64 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    +
      Word64 -> Nat
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (MetaId -> Word64
    metaId MetaId
    m)

    primMetaToNatInjective :: TCM PrimitiveImpl
    primMetaToNatInjective :: TCM PrimitiveImpl
    primMetaToNatInjective = do
      meta  <- MetaId -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (MetaId
    forall a. HasCallStack => a
    undefined :: MetaId)
      nat   <- primType (undefined :: Nat)
      toNat <- primFunName <$> getPrimitive PrimMetaToNat
      mkPrimInjective meta nat toNat

    primCharToNatInjective :: TCM PrimitiveImpl
    primCharToNatInjective :: TCM PrimitiveImpl
    primCharToNatInjective = do
      char  <- Char -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Char
    forall a. HasCallStack => a
    undefined :: Char)
      nat   <- primType (undefined :: Nat)
      toNat <- primFunName <$> getPrimitive PrimCharToNat
      mkPrimInjective char nat toNat

    primStringToListInjective :: TCM PrimitiveImpl
    primStringToListInjective :: TCM PrimitiveImpl
    primStringToListInjective = do
      string <- Text -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Text
    forall a. HasCallStack => a
    undefined :: Text)
      chars  <- primType (undefined :: String)
      toList <- primFunName <$> getPrimitive PrimStringToList
      mkPrimInjective string chars toList

    primStringFromListInjective :: TCM PrimitiveImpl
    primStringFromListInjective :: TCM PrimitiveImpl
    primStringFromListInjective = do
      chars  <- ArgName -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (ArgName
    forall a. HasCallStack => a
    undefined :: String)
      string <- primType (undefined :: Text)
      fromList <- primFunName <$> getPrimitive PrimStringFromList
      mkPrimInjective chars string fromList

    primWord64ToNatInjective :: TCM PrimitiveImpl
    primWord64ToNatInjective :: TCM PrimitiveImpl
    primWord64ToNatInjective =  do
      word  <- Word64 -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Word64
    forall a. HasCallStack => a
    undefined :: Word64)
      nat   <- primType (undefined :: Nat)
      toNat <- primFunName <$> getPrimitive PrimWord64ToNat
      mkPrimInjective word nat toNat

    primFloatToWord64Injective :: TCM PrimitiveImpl
    primFloatToWord64Injective :: TCM PrimitiveImpl
    primFloatToWord64Injective = do
      float  <- Double -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Double
    forall a. HasCallStack => a
    undefined :: Double)
      mword  <- primType (undefined :: Maybe Word64)
      toWord <- primFunName <$> getPrimitive PrimFloatToWord64
      mkPrimInjective float mword toWord

    primQNameToWord64sInjective :: TCM PrimitiveImpl
    primQNameToWord64sInjective :: TCM PrimitiveImpl
    primQNameToWord64sInjective = do
      name    <- QName -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (QName
    forall a. HasCallStack => a
    undefined :: QName)
      words   <- primType (undefined :: (Word64, Word64))
      toWords <- primFunName <$> getPrimitive PrimQNameToWord64s
      mkPrimInjective name words toWords

    getRefl :: TCM (Arg Term -> Term)
    getRefl :: TCM (Arg Term -> Term)
    getRefl = do
      -- BUILTIN REFL maybe a constructor with one (the principal) argument or only parameters.
      -- Get the ArgInfo of the principal argument of refl.
      con@(Con rf ci []) <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primRefl
      minfo <- fmap (setOrigin Inserted) <$> getReflArgInfo rf
      pure $ case minfo of
        Just ArgInfo
    ai -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    rf ConInfo
    ci (Elims -> Term) -> (Arg Term -> Elims) -> Arg Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Elim' Term -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :[]) (Elim' Term -> Elims)
    -> (Arg Term -> Elim' Term) -> Arg Term -> Elims
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term)
    -> (Arg Term -> Arg Term) -> Arg Term -> Elim' Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgInfo -> Arg Term -> Arg Term
    forall a. LensArgInfo a => ArgInfo -> a -> a
    setArgInfo ArgInfo
    ai
        Maybe ArgInfo
    Nothing -> Term -> Arg Term -> Term
    forall a b. a -> b -> a
    const Term
    con

    -- | @primEraseEquality : {a : Level} {A : Set a} {x y : A} -> x ≡ y -> x ≡ y@
    primEraseEquality :: TCM PrimitiveImpl
    primEraseEquality :: TCM PrimitiveImpl
    primEraseEquality = do
      -- primEraseEquality is incompatible with --without-K
      -- We raise an error warning if --safe is set and a mere warning otherwise
      TCMT IO Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM TCMT IO Bool
    forall (m :: * -> *). HasOptions m => m Bool
    withoutKOption (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Bool -> TCMT IO () -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (CommandLineOptions -> Bool
    forall a. LensSafeMode a => a -> Bool
    Lens.getSafeMode (CommandLineOptions -> Bool)
    -> TCMT IO CommandLineOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions)
          {- then -} (Warning -> TCMT IO ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning Warning
    SafeFlagWithoutKFlagPrimEraseEquality)
          {- else -} (Warning -> TCMT IO ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning Warning
    WithoutKFlagPrimEraseEquality)
      -- Get the name and type of BUILTIN EQUALITY
      eq   <- TCM QName
    primEqualityName
      eqTy <- defType <$> getConstInfo eq
      -- E.g. @eqTy = eqTel → Set a@ where @eqTel = {a : Level} {A : Set a} (x y : A)@.
      TelV eqTel eqCore <- telView eqTy
      let eqSort = case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    eqCore of
            Sort Sort' Term
    s -> Sort' Term
    s
            Term
    _      -> Sort' Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      -- Construct the type of primEraseEquality, e.g.
      -- @{a : Level} {A : Set a} {x y : A} → eq {a} {A} x y -> eq {a} {A} x y@.
      t <- let xeqy = Type -> TCM Type
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Type -> TCM Type) -> Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    eqSort (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    eq (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    eqTel in
           telePi_ (fmap hide eqTel) <$> (xeqy --> xeqy)

      -- Get the constructor corresponding to BUILTIN REFL
      refl <- getRefl

      -- The implementation of primEraseEquality:
      return $ PrimImpl t $ primFun __IMPOSSIBLE__ (1 + size eqTel) $ \ [Arg Term]
    ts -> do
        let (Arg Term
    u, Arg Term
    v) = (Arg Term, Arg Term)
    -> Maybe (Arg Term, Arg Term) -> (Arg Term, Arg Term)
    forall a. a -> Maybe a -> a
    fromMaybe (Arg Term, Arg Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (Arg Term, Arg Term) -> (Arg Term, Arg Term))
    -> Maybe (Arg Term, Arg Term) -> (Arg Term, Arg Term)
    forall a b. (a -> b) -> a -> b
    $ [Arg Term] -> Maybe (Arg Term, Arg Term)
    forall a. [a] -> Maybe (a, a)
    last2 ([Arg Term] -> Maybe (Arg Term, Arg Term))
    -> Maybe [Arg Term] -> Maybe (Arg Term, Arg Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Arg Term] -> Maybe [Arg Term]
    forall a. [a] -> Maybe [a]
    initMaybe [Arg Term]
    ts
        -- Andreas, 2013-07-22.
        -- Note that we cannot call the conversion checker here,
        -- because 'reduce' might be called in a context where
        -- some bound variables do not have a type (just __DUMMY_TYPE__),
        -- and the conversion checker for eliminations does not
        -- like this.
        -- We can only do untyped equality, e.g., by normalisation.
        (u', v') <- (Arg Term, Arg Term) -> ReduceM (Arg Term, Arg Term)
    forall t. Normalise t => t -> ReduceM t
    normalise' (Arg Term
    u, Arg Term
    v)
        if u' == v' then redReturn $ refl u else
          return $ NoReduction $ map notReduced ts

    -- | Get the 'ArgInfo' of the principal argument of BUILTIN REFL.
    --
    --   Returns @Nothing@ for e.g.
    --   @
    --     data Eq {a} {A : Set a} (x : A) : A → Set a where
    --       refl : Eq x x
    --   @
    --
    --   Returns @Just ...@ for e.g.
    --   @
    --     data Eq {a} {A : Set a} : (x y : A) → Set a where
    --       refl : ∀ x → Eq x x
    --   @

    getReflArgInfo :: ConHead -> TCM (Maybe ArgInfo)
    getReflArgInfo :: ConHead -> TCMT IO (Maybe ArgInfo)
    getReflArgInfo ConHead
    rf = do
      def <- ConHead -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
    getConInfo ConHead
    rf
      TelV reflTel _ <- telView $ defType def
      return $ fmap getArgInfo $ listToMaybe $ drop (conPars $ theDef def) $ telToList reflTel

    -- | Used for both @primForce@ and @primForceLemma@.
    genPrimForce :: TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
    genPrimForce :: TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
    genPrimForce TCM Type
    b Term -> Arg Term -> Term
    ret = do
      let varEl :: Arity -> f a -> f (Type'' Term a)
    varEl Arity
    s f a
    a = Sort' Term -> a -> Type'' Term a
    forall t a. Sort' t -> a -> Type'' t a
    El (Arity -> Sort' Term
    varSort Arity
    s) (a -> Type'' Term a) -> f a -> f (Type'' Term a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f a
    a
          varT :: Arity -> Arity -> f Type
    varT Arity
    s Arity
    a  = Arity -> f Term -> f Type
    forall {f :: * -> *} {a}.
    Functor f =>
    Arity -> f a -> f (Type'' Term a)
    varEl Arity
    s (Arity -> f Term
    forall (m :: * -> *). Applicative m => Arity -> m Term
    varM Arity
    a)
          varS :: Arity -> f Type
    varS Arity
    s    = Type -> f Type
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Type -> f Type) -> Type -> f Type
    forall a b. (a -> b) -> a -> b
    $ Sort' Term -> Type
    sort (Sort' Term -> Type) -> Sort' Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Arity -> Sort' Term
    varSort Arity
    s
      t <- ArgName -> TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    hPi ArgName
    "a" (TCMT IO Term -> TCM Type
    forall (m :: * -> *). Functor m => m Term -> m Type
    el TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $
           ArgName -> TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    hPi ArgName
    "b" (TCMT IO Term -> TCM Type
    forall (m :: * -> *). Functor m => m Term -> m Type
    el TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $
           ArgName -> TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    hPi ArgName
    "A" (Arity -> TCM Type
    forall {f :: * -> *}. Applicative f => Arity -> f Type
    varS Arity
    1) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $
           ArgName -> TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    hPi ArgName
    "B" (Arity -> Arity -> TCM Type
    forall {f :: * -> *}. Applicative f => Arity -> Arity -> f Type
    varT Arity
    2 Arity
    0 TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> Arity -> TCM Type
    forall {f :: * -> *}. Applicative f => Arity -> f Type
    varS Arity
    1) TCM Type
    b
      return $ PrimImpl t $ primFun __IMPOSSIBLE__ 6 $ \ [Arg Term]
    ts ->
        case [Arg Term]
    ts of
          [Arg Term
    a, Arg Term
    b, Arg Term
    s, Arg Term
    t, Arg Term
    u, Arg Term
    f] -> do
            u <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    u
            let isWHNF Blocked{} = Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
                isWHNF (NotBlocked NotBlocked' t
    _ Arg Term
    u) =
                  case Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    u of
                    Lit{}      -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                    Con{}      -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                    Lam{}      -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                    Pi{}       -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                    Sort{}     -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True  -- sorts and levels are considered whnf
                    Level{}    -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                    DontCare{} -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                    Def QName
    q Elims
    _    -> do
                      def <- Definition -> Defn
    theDef (Definition -> Defn) -> m Definition -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
                      return $ case def of
                        Datatype{} -> Bool
    True
                        Record{}   -> Bool
    True
                        Defn
    _          -> Bool
    False
                    Var{}      -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
                    MetaV{}    -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                    Dummy ArgName
    s Elims
    _  -> ArgName -> m Bool
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    ArgName -> m a
    __IMPOSSIBLE_VERBOSE__ ArgName
    s
            ifM (isWHNF u)
                (redReturn $ ret (unArg f) (ignoreBlocking u))
                (return $ NoReduction $ map notReduced [a, b, s, t] ++ [reduced u, notReduced f])
          [Arg Term]
    _ -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    primForce :: TCM PrimitiveImpl
    primForce :: TCM PrimitiveImpl
    primForce = do
      let varEl :: Arity -> f a -> f (Type'' Term a)
    varEl Arity
    s f a
    a = Sort' Term -> a -> Type'' Term a
    forall t a. Sort' t -> a -> Type'' t a
    El (Arity -> Sort' Term
    varSort Arity
    s) (a -> Type'' Term a) -> f a -> f (Type'' Term a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f a
    a
          varT :: Arity -> Arity -> f Type
    varT Arity
    s Arity
    a  = Arity -> f Term -> f Type
    forall {f :: * -> *} {a}.
    Functor f =>
    Arity -> f a -> f (Type'' Term a)
    varEl Arity
    s (Arity -> f Term
    forall (m :: * -> *). Applicative m => Arity -> m Term
    varM Arity
    a)
      TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
    genPrimForce (ArgName -> TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    nPi ArgName
    "x" (Arity -> Arity -> TCM Type
    forall {f :: * -> *}. Applicative f => Arity -> Arity -> f Type
    varT Arity
    3 Arity
    1) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $
                    ArgName -> TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    nPi ArgName
    "y" (Arity -> Arity -> TCM Type
    forall {f :: * -> *}. Applicative f => Arity -> Arity -> f Type
    varT Arity
    4 Arity
    2) (Arity -> TCMT IO Term -> TCM Type
    forall {f :: * -> *} {a}.
    Functor f =>
    Arity -> f a -> f (Type'' Term a)
    varEl Arity
    4 (TCMT IO Term -> TCM Type) -> TCMT IO Term -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Arity -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Arity -> m Term
    varM Arity
    2 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Arity -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Arity -> m Term
    varM Arity
    0) TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    -->
                    Arity -> TCMT IO Term -> TCM Type
    forall {f :: * -> *} {a}.
    Functor f =>
    Arity -> f a -> f (Type'' Term a)
    varEl Arity
    3 (Arity -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Arity -> m Term
    varM Arity
    1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Arity -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Arity -> m Term
    varM Arity
    0)) ((Term -> Arg Term -> Term) -> TCM PrimitiveImpl)
    -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
    forall a b. (a -> b) -> a -> b
    $
        \ Term
    f Arg Term
    u -> Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    apply Term
    f [Arg Term
    u]

    primForceLemma :: TCM PrimitiveImpl
    primForceLemma :: TCM PrimitiveImpl
    primForceLemma = do
      let varEl :: Arity -> f a -> f (Type'' Term a)
    varEl Arity
    s f a
    a = Sort' Term -> a -> Type'' Term a
    forall t a. Sort' t -> a -> Type'' t a
    El (Arity -> Sort' Term
    varSort Arity
    s) (a -> Type'' Term a) -> f a -> f (Type'' Term a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f a
    a
          varT :: Arity -> Arity -> f Type
    varT Arity
    s Arity
    a  = Arity -> f Term -> f Type
    forall {f :: * -> *} {a}.
    Functor f =>
    Arity -> f a -> f (Type'' Term a)
    varEl Arity
    s (Arity -> f Term
    forall (m :: * -> *). Applicative m => Arity -> m Term
    varM Arity
    a)
      refl  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primRefl
      force <- primFunName <$> getPrimitive PrimForce
      genPrimForce (nPi "x" (varT 3 1) $
                    nPi "f" (nPi "y" (varT 4 2) $ varEl 4 $ varM 2 <@> varM 0) $
                    varEl 4 $ primEquality <#> varM 4 <#> (varM 2 <@> varM 1)
                                           <@> (pure (Def force []) <#> varM 5 <#> varM 4 <#> varM 3 <#> varM 2 <@> varM 1 <@> varM 0)
                                           <@> (varM 0 <@> varM 1)
                   ) $ \ Term
    _ Arg Term
    _ -> Term
    refl

    mkPrimLevelZero :: TCM PrimitiveImpl
    mkPrimLevelZero :: TCM PrimitiveImpl
    mkPrimLevelZero = do
      t <- Lvl -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Lvl
    forall a. HasCallStack => a
    undefined :: Lvl)
      return $ PrimImpl t $ primFun __IMPOSSIBLE__ 0 $ \[Arg Term]
    _ -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ Level' Term -> Term
    Level (Level' Term -> Term) -> Level' Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Integer -> Level' Term
    ClosedLevel Integer
    0

    mkPrimLevelSuc :: TCM PrimitiveImpl
    mkPrimLevelSuc :: TCM PrimitiveImpl
    mkPrimLevelSuc = do
      t <- (Lvl -> Lvl) -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Lvl -> Lvl
    forall a. a -> a
    id :: Lvl -> Lvl)
      return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ ~[Arg Term
    a] -> do
        l <- Term -> ReduceM (Level' Term)
    forall (m :: * -> *). PureTCM m => Term -> m (Level' Term)
    levelView' (Term -> ReduceM (Level' Term)) -> Term -> ReduceM (Level' Term)
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a
        redReturn $ Level $ levelSuc l

    mkPrimLevelMax :: TCM PrimitiveImpl
    mkPrimLevelMax :: TCM PrimitiveImpl
    mkPrimLevelMax = do
      t <- Op Lvl -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Op Lvl
    forall a. Ord a => a -> a -> a
    max :: Op Lvl)
      return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \ ~[Arg Term
    a, Arg Term
    b] -> do
        a' <- Term -> ReduceM (Level' Term)
    forall (m :: * -> *). PureTCM m => Term -> m (Level' Term)
    levelView' (Term -> ReduceM (Level' Term)) -> Term -> ReduceM (Level' Term)
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a
        b' <- levelView' $ unArg b
        redReturn $ Level $ levelLub a' b'

    primLockUniv' :: TCM PrimitiveImpl
    primLockUniv' :: TCM PrimitiveImpl
    primLockUniv' = do
      let t :: Type
    t = Sort' Term -> Type
    sort (Sort' Term -> Type) -> Sort' Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Level' Term -> Sort' Term
    forall t. Level' t -> Sort' t
    Type (Level' Term -> Sort' Term) -> Level' Term -> Sort' Term
    forall a b. (a -> b) -> a -> b
    $ Level' Term -> Level' Term
    levelSuc (Level' Term -> Level' Term) -> Level' Term -> Level' Term
    forall a b. (a -> b) -> a -> b
    $ Integer -> [PlusLevel' Term] -> Level' Term
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    0 []
      PrimitiveImpl -> TCM PrimitiveImpl
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PrimitiveImpl -> TCM PrimitiveImpl)
    -> PrimitiveImpl -> TCM PrimitiveImpl
    forall a b. (a -> b) -> a -> b
    $ Type -> PrimFun -> PrimitiveImpl
    PrimImpl Type
    t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
    forall a b. (a -> b) -> a -> b
    $ QName
    -> Arity
    -> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Arity
    0 (([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
     -> PrimFun)
    -> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \[Arg Term]
    _ -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ Sort' Term -> Term
    Sort Sort' Term
    forall t. Sort' t
    LockUniv

    mkPrimFun1TCM :: (FromTerm a, ToTerm b) =>
                     TCM Type -> (a -> ReduceM b) -> TCM PrimitiveImpl
    mkPrimFun1TCM :: forall a b.
    (FromTerm a, ToTerm b) =>
    TCM Type -> (a -> ReduceM b) -> TCM PrimitiveImpl
    mkPrimFun1TCM TCM Type
    mt a -> ReduceM b
    f = do
        toA   <- TCM (FromTermFunction a)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm
        fromB <- toTerm
        t     <- mt
        return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \[Arg Term]
    ts ->
          case [Arg Term]
    ts of
            [Arg Term
    v] ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction a
    toA Arg Term
    v) (MaybeReducedArgs -> ReduceM MaybeReducedArgs
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (MaybeReducedArgs -> ReduceM MaybeReducedArgs)
    -> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
    -> MaybeReduced (Arg Term)
    -> ReduceM MaybeReducedArgs
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MaybeReduced (Arg Term) -> MaybeReducedArgs
    forall el coll. Singleton el coll => el -> coll
    singleton) ((a -> ReduceM (Reduced MaybeReducedArgs Term))
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ \ a
    x -> do
                b <- b -> ReduceM Term
    fromB (b -> ReduceM Term) -> ReduceM b -> ReduceM Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< a -> ReduceM b
    f a
    x
                case allMetas Set.singleton b of
                  Set MetaId
    ms | Set MetaId -> Bool
    forall a. Set a -> Bool
    Set.null Set MetaId
    ms -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn Term
    b
                     | Bool
    otherwise   -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced MaybeReducedArgs Term
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ MaybeReducedArgs -> Reduced MaybeReducedArgs Term
    forall no yes. no -> Reduced no yes
    NoReduction [Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced (Blocker -> Arg Term -> Blocked (Arg Term)
    forall t a. Blocker -> a -> Blocked' t a
    Blocked (Set MetaId -> Blocker
    unblockOnAllMetas Set MetaId
    ms) Arg Term
    v)]
            [Arg Term]
    _ -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- Tying the knot
    mkPrimFun1 :: (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
                  (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 :: forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 a -> b
    f = do
        toA   <- TCM (FromTermFunction a)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm
        fromB <- toTerm
        t     <- primType f
        return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \[Arg Term]
    ts ->
          case [Arg Term]
    ts of
            [Arg Term
    v] ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction a
    toA Arg Term
    v) (MaybeReducedArgs -> ReduceM MaybeReducedArgs
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (MaybeReducedArgs -> ReduceM MaybeReducedArgs)
    -> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
    -> MaybeReduced (Arg Term)
    -> ReduceM MaybeReducedArgs
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MaybeReduced (Arg Term) -> MaybeReducedArgs
    forall el coll. Singleton el coll => el -> coll
    singleton) ((a -> ReduceM (Reduced MaybeReducedArgs Term))
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ \ a
    x ->
              Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< b -> ReduceM Term
    fromB (a -> b
    f a
    x)
            [Arg Term]
    _ -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    mkPrimFun2 :: ( PrimType a, FromTerm a, ToTerm a
                  , PrimType b, FromTerm b
                  , PrimType c, ToTerm c ) =>
                  (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 :: forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 a -> b -> c
    f = do
        toA   <- TCM (FromTermFunction a)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm
        fromA <- toTerm
        toB   <- fromTerm
        fromC <- toTerm
        t     <- primType f
        return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \[Arg Term]
    ts ->
          case [Arg Term]
    ts of
            [Arg Term
    v,Arg Term
    w] ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction a
    toA Arg Term
    v)
                  (\MaybeReduced (Arg Term)
    v' -> MaybeReducedArgs -> ReduceM MaybeReducedArgs
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [MaybeReduced (Arg Term)
    v', Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced Arg Term
    w]) ((a -> ReduceM (Reduced MaybeReducedArgs Term))
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ \a
    x ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) b)
    -> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
    -> (b -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction b
    toB Arg Term
    w)
                  (\MaybeReduced (Arg Term)
    w' -> do
                    xTm <- a -> ReduceM Term
    fromA a
    x
                    pure [reduced $ notBlocked $ Arg (argInfo v) xTm , w']
                  ) ((b -> ReduceM (Reduced MaybeReducedArgs Term))
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> (b -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ \b
    y ->
              Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< c -> ReduceM Term
    fromC (a -> b -> c
    f a
    x b
    y)
            [Arg Term]
    _ -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    mkPrimFun3 :: ( PrimType a, FromTerm a, ToTerm a
                  , PrimType b, FromTerm b, ToTerm b
                  , PrimType c, FromTerm c
                  , PrimType d, ToTerm d ) =>
                  (a -> b -> c -> d) -> TCM PrimitiveImpl
    mkPrimFun3 :: forall a b c d.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     ToTerm b, PrimType c, FromTerm c, PrimType d, ToTerm d) =>
    (a -> b -> c -> d) -> TCM PrimitiveImpl
    mkPrimFun3 a -> b -> c -> d
    f = do
        (toA, fromA) <- (,) (FromTermFunction a
     -> (a -> ReduceM Term) -> (FromTermFunction a, a -> ReduceM Term))
    -> TCMT IO (FromTermFunction a)
    -> TCMT
         IO ((a -> ReduceM Term) -> (FromTermFunction a, a -> ReduceM Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (FromTermFunction a)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm TCMT
      IO ((a -> ReduceM Term) -> (FromTermFunction a, a -> ReduceM Term))
    -> TCMT IO (a -> ReduceM Term)
    -> TCMT IO (FromTermFunction a, a -> ReduceM Term)
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TCMT IO (a -> ReduceM Term)
    forall a. ToTerm a => TCM (a -> ReduceM Term)
    toTerm
        (toB, fromB) <- (,) <$> fromTerm <*> toTerm
        toC          <- fromTerm
        fromD        <- toTerm
        t <- primType f
        return $ PrimImpl t $ primFun __IMPOSSIBLE__ 3 $ \[Arg Term]
    ts ->
          let argFrom :: (t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
    argFrom t -> f Term
    fromX Arg e
    a t
    x =
                Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced (Blocked (Arg Term) -> MaybeReduced (Arg Term))
    -> (Term -> Blocked (Arg Term)) -> Term -> MaybeReduced (Arg Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Blocked (Arg Term)
    forall a t. a -> Blocked' t a
    notBlocked (Arg Term -> Blocked (Arg Term))
    -> (Term -> Arg Term) -> Term -> Blocked (Arg Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg (Arg e -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo Arg e
    a) (Term -> MaybeReduced (Arg Term))
    -> f Term -> f (MaybeReduced (Arg Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> t -> f Term
    fromX t
    x
          in case [Arg Term]
    ts of
            [Arg Term
    a,Arg Term
    b,Arg Term
    c] ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction a
    toA Arg Term
    a)
                  (\MaybeReduced (Arg Term)
    a' -> MaybeReducedArgs -> ReduceM MaybeReducedArgs
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [MaybeReduced (Arg Term)
    a', Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced Arg Term
    b, Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced Arg Term
    c]) ((a -> ReduceM (Reduced MaybeReducedArgs Term))
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ \a
    x ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) b)
    -> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
    -> (b -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction b
    toB Arg Term
    b)
                  (\MaybeReduced (Arg Term)
    b' -> [ReduceM (MaybeReduced (Arg Term))] -> ReduceM MaybeReducedArgs
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence
                    [ (a -> ReduceM Term)
    -> Arg Term -> a -> ReduceM (MaybeReduced (Arg Term))
    forall {f :: * -> *} {t} {e}.
    Functor f =>
    (t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
    argFrom a -> ReduceM Term
    fromA Arg Term
    a a
    x
                    , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure MaybeReduced (Arg Term)
    b'
                    , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
    -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced Arg Term
    c ]) ((b -> ReduceM (Reduced MaybeReducedArgs Term))
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> (b -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ \b
    y ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) c)
    -> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
    -> (c -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction c
    toC Arg Term
    c)
                  (\MaybeReduced (Arg Term)
    c' -> [ReduceM (MaybeReduced (Arg Term))] -> ReduceM MaybeReducedArgs
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence
                    [ (a -> ReduceM Term)
    -> Arg Term -> a -> ReduceM (MaybeReduced (Arg Term))
    forall {f :: * -> *} {t} {e}.
    Functor f =>
    (t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
    argFrom a -> ReduceM Term
    fromA Arg Term
    a a
    x
                    , (b -> ReduceM Term)
    -> Arg Term -> b -> ReduceM (MaybeReduced (Arg Term))
    forall {f :: * -> *} {t} {e}.
    Functor f =>
    (t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
    argFrom b -> ReduceM Term
    fromB Arg Term
    b b
    y
                    , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure MaybeReduced (Arg Term)
    c' ]) ((c -> ReduceM (Reduced MaybeReducedArgs Term))
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> (c -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ \c
    z ->
              Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< d -> ReduceM Term
    fromD (a -> b -> c -> d
    f a
    x b
    y c
    z)
            [Arg Term]
    _ -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    mkPrimFun4 :: ( PrimType a, FromTerm a, ToTerm a
                  , PrimType b, FromTerm b, ToTerm b
                  , PrimType c, FromTerm c, ToTerm c
                  , PrimType d, FromTerm d
                  , PrimType e, ToTerm e ) =>
                  (a -> b -> c -> d -> e) -> TCM PrimitiveImpl
    mkPrimFun4 :: forall a b c d e.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     ToTerm b, PrimType c, FromTerm c, ToTerm c, PrimType d, FromTerm d,
     PrimType e, ToTerm e) =>
    (a -> b -> c -> d -> e) -> TCM PrimitiveImpl
    mkPrimFun4 a -> b -> c -> d -> e
    f = do
        (toA, fromA) <- (,) (FromTermFunction a
     -> (a -> ReduceM Term) -> (FromTermFunction a, a -> ReduceM Term))
    -> TCMT IO (FromTermFunction a)
    -> TCMT
         IO ((a -> ReduceM Term) -> (FromTermFunction a, a -> ReduceM Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (FromTermFunction a)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm TCMT
      IO ((a -> ReduceM Term) -> (FromTermFunction a, a -> ReduceM Term))
    -> TCMT IO (a -> ReduceM Term)
    -> TCMT IO (FromTermFunction a, a -> ReduceM Term)
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TCMT IO (a -> ReduceM Term)
    forall a. ToTerm a => TCM (a -> ReduceM Term)
    toTerm
        (toB, fromB) <- (,) <$> fromTerm <*> toTerm
        (toC, fromC) <- (,) <$> fromTerm <*> toTerm
        toD          <- fromTerm
        fromE        <- toTerm
        t <- primType f
        return $ PrimImpl t $ primFun __IMPOSSIBLE__ 4 $ \[Arg Term]
    ts ->
          let argFrom :: (t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
    argFrom t -> f Term
    fromX Arg e
    a t
    x =
                Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced (Blocked (Arg Term) -> MaybeReduced (Arg Term))
    -> (Term -> Blocked (Arg Term)) -> Term -> MaybeReduced (Arg Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Blocked (Arg Term)
    forall a t. a -> Blocked' t a
    notBlocked (Arg Term -> Blocked (Arg Term))
    -> (Term -> Arg Term) -> Term -> Blocked (Arg Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg (Arg e -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo Arg e
    a) (Term -> MaybeReduced (Arg Term))
    -> f Term -> f (MaybeReduced (Arg Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> t -> f Term
    fromX t
    x
          in case [Arg Term]
    ts of
            [Arg Term
    a,Arg Term
    b,Arg Term
    c,Arg Term
    d] ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction a
    toA Arg Term
    a)
                  (\MaybeReduced (Arg Term)
    a' -> MaybeReducedArgs -> ReduceM MaybeReducedArgs
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (MaybeReducedArgs -> ReduceM MaybeReducedArgs)
    -> MaybeReducedArgs -> ReduceM MaybeReducedArgs
    forall a b. (a -> b) -> a -> b
    $ MaybeReduced (Arg Term)
    a' MaybeReduced (Arg Term) -> MaybeReducedArgs -> MaybeReducedArgs
    forall a. a -> [a] -> [a]
    : (Arg Term -> MaybeReduced (Arg Term))
    -> [Arg Term] -> MaybeReducedArgs
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced [Arg Term
    b, Arg Term
    c, Arg Term
    d]) ((a -> ReduceM (Reduced MaybeReducedArgs Term))
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ \a
    x ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) b)
    -> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
    -> (b -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction b
    toB Arg Term
    b)
                  (\MaybeReduced (Arg Term)
    b' -> [ReduceM (MaybeReduced (Arg Term))] -> ReduceM MaybeReducedArgs
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence
                    [ (a -> ReduceM Term)
    -> Arg Term -> a -> ReduceM (MaybeReduced (Arg Term))
    forall {f :: * -> *} {t} {e}.
    Functor f =>
    (t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
    argFrom a -> ReduceM Term
    fromA Arg Term
    a a
    x
                    , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure MaybeReduced (Arg Term)
    b'
                    , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
    -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced Arg Term
    c
                    , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
    -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced Arg Term
    d ]) ((b -> ReduceM (Reduced MaybeReducedArgs Term))
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> (b -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ \b
    y ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) c)
    -> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
    -> (c -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction c
    toC Arg Term
    c)
                  (\MaybeReduced (Arg Term)
    c' -> [ReduceM (MaybeReduced (Arg Term))] -> ReduceM MaybeReducedArgs
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence
                    [ (a -> ReduceM Term)
    -> Arg Term -> a -> ReduceM (MaybeReduced (Arg Term))
    forall {f :: * -> *} {t} {e}.
    Functor f =>
    (t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
    argFrom a -> ReduceM Term
    fromA Arg Term
    a a
    x
                    , (b -> ReduceM Term)
    -> Arg Term -> b -> ReduceM (MaybeReduced (Arg Term))
    forall {f :: * -> *} {t} {e}.
    Functor f =>
    (t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
    argFrom b -> ReduceM Term
    fromB Arg Term
    b b
    y
                    , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure MaybeReduced (Arg Term)
    c'
                    , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
    -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced Arg Term
    d ]) ((c -> ReduceM (Reduced MaybeReducedArgs Term))
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> (c -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ \c
    z ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) d)
    -> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
    -> (d -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> ReduceM b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction d
    toD Arg Term
    d)
                  (\MaybeReduced (Arg Term)
    d' -> [ReduceM (MaybeReduced (Arg Term))] -> ReduceM MaybeReducedArgs
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence
                    [ (a -> ReduceM Term)
    -> Arg Term -> a -> ReduceM (MaybeReduced (Arg Term))
    forall {f :: * -> *} {t} {e}.
    Functor f =>
    (t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
    argFrom a -> ReduceM Term
    fromA Arg Term
    a a
    x
                    , (b -> ReduceM Term)
    -> Arg Term -> b -> ReduceM (MaybeReduced (Arg Term))
    forall {f :: * -> *} {t} {e}.
    Functor f =>
    (t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
    argFrom b -> ReduceM Term
    fromB Arg Term
    b b
    y
                    , (c -> ReduceM Term)
    -> Arg Term -> c -> ReduceM (MaybeReduced (Arg Term))
    forall {f :: * -> *} {t} {e}.
    Functor f =>
    (t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
    argFrom c -> ReduceM Term
    fromC Arg Term
    c c
    z
                    , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure MaybeReduced (Arg Term)
    d' ]) ((d -> ReduceM (Reduced MaybeReducedArgs Term))
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> (d -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ \d
    w ->

              Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< e -> ReduceM Term
    fromE (a -> b -> c -> d -> e
    f a
    x b
    y c
    z d
    w)
            [Arg Term]
    _ -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    ---------------------------------------------------------------------------
    -- * The actual primitive functions
    ---------------------------------------------------------------------------

    type Op   a = a -> a -> a
    type Fun  a = a -> a
    type Rel  a = a -> a -> Bool
    type Pred a = a -> Bool

    primitiveFunctions :: Map PrimitiveId (TCM PrimitiveImpl)
    primitiveFunctions :: Map PrimitiveId (TCM PrimitiveImpl)
    primitiveFunctions = TCM PrimitiveImpl -> TCM PrimitiveImpl
    forall a. TCM a -> TCM a
    localTCStateSavingWarnings (TCM PrimitiveImpl -> TCM PrimitiveImpl)
    -> Map PrimitiveId (TCM PrimitiveImpl)
    -> Map PrimitiveId (TCM PrimitiveImpl)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCM PrimitiveImpl -> TCM PrimitiveImpl -> TCM PrimitiveImpl)
    -> [(PrimitiveId, TCM PrimitiveImpl)]
    -> Map PrimitiveId (TCM PrimitiveImpl)
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith TCM PrimitiveImpl -> TCM PrimitiveImpl -> TCM PrimitiveImpl
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      -- Issue #4375          ^^^^^^^^^^^^^^^^^^^^^^^^^^
      --   Without this the next fresh checkpoint id gets changed building the primitive functions. This
      --   is bad for caching since it happens when scope checking import declarations (rebinding
      --   primitives). During type checking, the caching machinery might then load a cached state with
      --   out-of-date checkpoint ids. Make sure to preserve warnings though, since they include things
      --   like using unsafe things primitives with `--safe`.

      -- Ulf, 2015-10-28: Builtin integers now map to a datatype, and since you
      -- can define these functions (reasonably) efficiently using the primitive
      -- functions on natural numbers there's no need for them anymore. Keeping the
      -- show function around for convenience, and as a test case for a primitive
      -- function taking an integer.
      -- -- Integer functions
      -- [ "primIntegerPlus"     |-> mkPrimFun2 ((+)        :: Op Integer)
      -- , "primIntegerMinus"    |-> mkPrimFun2 ((-)        :: Op Integer)
      -- , "primIntegerTimes"    |-> mkPrimFun2 ((*)        :: Op Integer)
      -- , "primIntegerDiv"      |-> mkPrimFun2 (div        :: Op Integer)    -- partial
      -- , "primIntegerMod"      |-> mkPrimFun2 (mod        :: Op Integer)    -- partial
      -- , "primIntegerEquality" |-> mkPrimFun2 ((==)       :: Rel Integer)
      -- , "primIntegerLess"     |-> mkPrimFun2 ((<)        :: Rel Integer)
      -- , "primIntegerAbs"      |-> mkPrimFun1 (Nat . abs  :: Integer -> Nat)
      -- , "primNatToInteger"    |-> mkPrimFun1 (toInteger  :: Nat -> Integer)
      [ PrimitiveId
    PrimShowInteger     PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Integer -> Text) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (ArgName -> Text
    T.pack (ArgName -> Text) -> (Integer -> ArgName) -> Integer -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow :: Integer -> Text)

      -- Natural number functions
      , PrimitiveId
    PrimNatPlus           PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Nat -> Nat -> Nat) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 (Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    (+)                     :: Op Nat)
      , PrimitiveId
    PrimNatMinus          PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Nat -> Nat -> Nat) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 ((\Nat
    x Nat
    y -> Nat -> Nat -> Nat
    forall a. Ord a => a -> a -> a
    max Nat
    0 (Nat
    x Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    y)) :: Op Nat)
      , PrimitiveId
    PrimNatTimes          PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Nat -> Nat -> Nat) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 (Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    (*)                     :: Op Nat)
      , PrimitiveId
    PrimNatDivSucAux      PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Nat -> Nat -> Nat -> Nat -> Nat) -> TCM PrimitiveImpl
    forall a b c d e.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     ToTerm b, PrimType c, FromTerm c, ToTerm c, PrimType d, FromTerm d,
     PrimType e, ToTerm e) =>
    (a -> b -> c -> d -> e) -> TCM PrimitiveImpl
    mkPrimFun4 ((\Nat
    k Nat
    m Nat
    n Nat
    j -> Nat
    k Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat -> Nat -> Nat
    forall a. Integral a => a -> a -> a
    div (Nat -> Nat -> Nat
    forall a. Ord a => a -> a -> a
    max Nat
    0 (Nat -> Nat) -> Nat -> Nat
    forall a b. (a -> b) -> a -> b
    $ Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    m Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    j) (Nat
    m Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1)) :: Nat -> Nat -> Op Nat)
      , PrimitiveId
    PrimNatModSucAux      PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |->
          let aux :: Nat -> Nat -> Op Nat
              aux :: Nat -> Nat -> Nat -> Nat -> Nat
    aux Nat
    k Nat
    m Nat
    n Nat
    j | Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    j     = Nat -> Nat -> Nat
    forall a. Integral a => a -> a -> a
    mod (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    j Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) (Nat
    m Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1)
                          | Bool
    otherwise = Nat
    k Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    n
          in (Nat -> Nat -> Nat -> Nat -> Nat) -> TCM PrimitiveImpl
    forall a b c d e.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     ToTerm b, PrimType c, FromTerm c, ToTerm c, PrimType d, FromTerm d,
     PrimType e, ToTerm e) =>
    (a -> b -> c -> d -> e) -> TCM PrimitiveImpl
    mkPrimFun4 Nat -> Nat -> Nat -> Nat -> Nat
    aux
      , PrimitiveId
    PrimNatEquality       PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Nat -> Nat -> Bool) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 (Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) :: Rel Nat)
      , PrimitiveId
    PrimNatLess           PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Nat -> Nat -> Bool) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 (Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    (<)  :: Rel Nat)
      , PrimitiveId
    PrimShowNat           PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Nat -> Text) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (ArgName -> Text
    T.pack (ArgName -> Text) -> (Nat -> ArgName) -> Nat -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow :: Nat -> Text)

      -- -- Machine words
      , PrimitiveId
    PrimWord64ToNat      PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Word64 -> Nat) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (Word64 -> Nat
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral :: Word64 -> Nat)
      , PrimitiveId
    PrimWord64FromNat    PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Nat -> Word64) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (Nat -> Word64
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral :: Nat -> Word64)
      , PrimitiveId
    PrimWord64ToNatInjective PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primWord64ToNatInjective

      -- -- Level functions
      , PrimitiveId
    PrimLevelZero         PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    mkPrimLevelZero
      , PrimitiveId
    PrimLevelSuc          PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    mkPrimLevelSuc
      , PrimitiveId
    PrimLevelMax          PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    mkPrimLevelMax

      -- Floating point functions
      --
      -- Wen, 2020-08-26: Primitives which convert from Float into other, more
      -- well-behaved numeric types should check for unrepresentable values, e.g.,
      -- NaN and the infinities, and return `nothing` if those are encountered, to
      -- ensure that the returned numbers are sensible. That means `primFloatRound`,
      -- `primFloatFloor`, `primFloatCeiling`, and `primFloatDecode`. The conversion
      -- `primFloatRatio` represents NaN as (0,0), and the infinities as (±1,0).
      --
      , PrimitiveId
    PrimFloatEquality            PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double -> Bool) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 Double -> Double -> Bool
    doubleEq
      , PrimitiveId
    PrimFloatInequality          PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double -> Bool) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 Double -> Double -> Bool
    doubleLe
      , PrimitiveId
    PrimFloatLess                PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double -> Bool) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 Double -> Double -> Bool
    doubleLt
      , PrimitiveId
    PrimFloatIsInfinite          PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Bool) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (Double -> Bool
    forall a. RealFloat a => a -> Bool
    isInfinite :: Double -> Bool)
      , PrimitiveId
    PrimFloatIsNaN               PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Bool) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (Double -> Bool
    forall a. RealFloat a => a -> Bool
    isNaN :: Double -> Bool)
      , PrimitiveId
    PrimFloatIsNegativeZero      PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Bool) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (Double -> Bool
    forall a. RealFloat a => a -> Bool
    isNegativeZero :: Double -> Bool)
      , PrimitiveId
    PrimFloatIsSafeInteger       PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Bool) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Bool
    isSafeInteger
      , PrimitiveId
    PrimFloatToWord64            PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Maybe Word64) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Maybe Word64
    doubleToWord64
      , PrimitiveId
    PrimFloatToWord64Injective   PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primFloatToWord64Injective
      , PrimitiveId
    PrimNatToFloat               PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Nat -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (Nat -> Double
    forall a. Integral a => a -> Double
    intToDouble :: Nat -> Double)
      , PrimitiveId
    PrimIntToFloat               PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Integer -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (Integer -> Double
    forall a. Integral a => a -> Double
    intToDouble :: Integer -> Double)
      , PrimitiveId
    PrimFloatRound               PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Maybe Integer) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Maybe Integer
    doubleRound
      , PrimitiveId
    PrimFloatFloor               PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Maybe Integer) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Maybe Integer
    doubleFloor
      , PrimitiveId
    PrimFloatCeiling             PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Maybe Integer) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Maybe Integer
    doubleCeiling
      , PrimitiveId
    PrimFloatToRatio             PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> (Integer, Integer)) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> (Integer, Integer)
    doubleToRatio
      , PrimitiveId
    PrimRatioToFloat             PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Integer -> Integer -> Double) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 Integer -> Integer -> Double
    ratioToDouble
      , PrimitiveId
    PrimFloatDecode              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Maybe (Integer, Integer)) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Maybe (Integer, Integer)
    doubleDecode
      , PrimitiveId
    PrimFloatEncode              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Integer -> Integer -> Maybe Double) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 Integer -> Integer -> Maybe Double
    doubleEncode
      , PrimitiveId
    PrimShowFloat                PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Text) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (ArgName -> Text
    T.pack (ArgName -> Text) -> (Double -> ArgName) -> Double -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Double -> ArgName
    forall a. Show a => a -> ArgName
    show :: Double -> Text)
      , PrimitiveId
    PrimFloatPlus                PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double -> Double) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 Double -> Double -> Double
    doublePlus
      , PrimitiveId
    PrimFloatMinus               PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double -> Double) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 Double -> Double -> Double
    doubleMinus
      , PrimitiveId
    PrimFloatTimes               PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double -> Double) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 Double -> Double -> Double
    doubleTimes
      , PrimitiveId
    PrimFloatNegate              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleNegate
      , PrimitiveId
    PrimFloatDiv                 PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double -> Double) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 Double -> Double -> Double
    doubleDiv
      , PrimitiveId
    PrimFloatPow                 PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double -> Double) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 Double -> Double -> Double
    doublePow
      , PrimitiveId
    PrimFloatSqrt                PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleSqrt
      , PrimitiveId
    PrimFloatExp                 PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleExp
      , PrimitiveId
    PrimFloatLog                 PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleLog
      , PrimitiveId
    PrimFloatSin                 PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleSin
      , PrimitiveId
    PrimFloatCos                 PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleCos
      , PrimitiveId
    PrimFloatTan                 PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleTan
      , PrimitiveId
    PrimFloatASin                PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleASin
      , PrimitiveId
    PrimFloatACos                PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleACos
      , PrimitiveId
    PrimFloatATan                PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleATan
      , PrimitiveId
    PrimFloatATan2               PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double -> Double) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 Double -> Double -> Double
    doubleATan2
      , PrimitiveId
    PrimFloatSinh                PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleSinh
      , PrimitiveId
    PrimFloatCosh                PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleCosh
      , PrimitiveId
    PrimFloatTanh                PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleTanh
      , PrimitiveId
    PrimFloatASinh               PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleASinh
      , PrimitiveId
    PrimFloatACosh               PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleCosh
      , PrimitiveId
    PrimFloatATanh               PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Double) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Double
    doubleTanh

      -- Character functions
      , PrimitiveId
    PrimCharEquality         PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Char -> Char -> Bool) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) :: Rel Char)
      , PrimitiveId
    PrimIsLower              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Char -> Bool) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Char -> Bool
    isLower
      , PrimitiveId
    PrimIsDigit              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Char -> Bool) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Char -> Bool
    isDigit
      , PrimitiveId
    PrimIsAlpha              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Char -> Bool) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Char -> Bool
    isAlpha
      , PrimitiveId
    PrimIsSpace              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Char -> Bool) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Char -> Bool
    isSpace
      , PrimitiveId
    PrimIsAscii              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Char -> Bool) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Char -> Bool
    isAscii
      , PrimitiveId
    PrimIsLatin1             PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Char -> Bool) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Char -> Bool
    isLatin1
      , PrimitiveId
    PrimIsPrint              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Char -> Bool) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Char -> Bool
    isPrint
      , PrimitiveId
    PrimIsHexDigit           PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Char -> Bool) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Char -> Bool
    isHexDigit
      , PrimitiveId
    PrimToUpper              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Char -> Char) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Char -> Char
    toUpper
      , PrimitiveId
    PrimToLower              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Char -> Char) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Char -> Char
    toLower
      , PrimitiveId
    PrimCharToNat            PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Char -> Nat) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (Arity -> Nat
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Arity -> Nat) -> (Char -> Arity) -> Char -> Nat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> Arity
    forall a. Enum a => a -> Arity
    fromEnum :: Char -> Nat)
      , PrimitiveId
    PrimCharToNatInjective   PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primCharToNatInjective
      , PrimitiveId
    PrimNatToChar            PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Nat -> Char) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (Integer -> Char
    integerToChar (Integer -> Char) -> (Nat -> Integer) -> Nat -> Char
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Integer
    unNat)
      , PrimitiveId
    PrimShowChar             PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Char -> Text) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (ArgName -> Text
    T.pack (ArgName -> Text) -> (Char -> ArgName) -> Char -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Literal -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow (Literal -> ArgName) -> (Char -> Literal) -> Char -> ArgName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> Literal
    LitChar)

      -- String functions
      , PrimitiveId
    PrimStringToList              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Text -> ArgName) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Text -> ArgName
    T.unpack
      , PrimitiveId
    PrimStringToListInjective     PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primStringToListInjective
      , PrimitiveId
    PrimStringFromList            PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (ArgName -> Text) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 ArgName -> Text
    T.pack
      , PrimitiveId
    PrimStringFromListInjective   PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primStringFromListInjective
      , PrimitiveId
    PrimStringAppend              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Text -> Text -> Text) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 (Text -> Text -> Text
    T.append :: Text -> Text -> Text)
      , PrimitiveId
    PrimStringEquality            PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Text -> Text -> Bool) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 (Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) :: Rel Text)
      , PrimitiveId
    PrimShowString                PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Text -> Text) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (ArgName -> Text
    T.pack (ArgName -> Text) -> (Text -> ArgName) -> Text -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Literal -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow (Literal -> ArgName) -> (Text -> Literal) -> Text -> ArgName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Literal
    LitString)
      , PrimitiveId
    PrimStringUncons              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Text -> Maybe (Char, Text)) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Text -> Maybe (Char, Text)
    T.uncons

      -- Other stuff
      , PrimitiveId
    PrimEraseEquality     PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primEraseEquality
        -- This needs to be force : A → ((x : A) → B x) → B x rather than seq because of call-by-name.
      , PrimitiveId
    PrimForce             PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primForce
      , PrimitiveId
    PrimForceLemma        PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primForceLemma
      , PrimitiveId
    PrimQNameEquality     PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (QName -> QName -> Bool) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 (QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) :: Rel QName)
      , PrimitiveId
    PrimQNameLess         PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (QName -> QName -> Bool) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 (QName -> QName -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) :: Rel QName)
      , PrimitiveId
    PrimShowQName         PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (QName -> Text) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (ArgName -> Text
    T.pack (ArgName -> Text) -> (QName -> ArgName) -> QName -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow :: QName -> Text)
      , PrimitiveId
    PrimQNameFixity       PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (QName -> Fixity') -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (Name -> Fixity'
    nameFixity (Name -> Fixity') -> (QName -> Name) -> QName -> Fixity'
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    qnameName)
      , PrimitiveId
    PrimQNameToWord64s    PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (QName -> (Word64, Word64)) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 ((\ (NameId Word64
    x (ModuleNameHash Word64
    y)) -> (Word64
    x, Word64
    y)) (NameId -> (Word64, Word64))
    -> (QName -> NameId) -> QName -> (Word64, Word64)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> NameId
    nameId (Name -> NameId) -> (QName -> Name) -> QName -> NameId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    qnameName
                                              :: QName -> (Word64, Word64))
      , PrimitiveId
    PrimQNameToWord64sInjective   PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primQNameToWord64sInjective
      , PrimitiveId
    PrimMetaEquality      PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (MetaId -> MetaId -> Bool) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 (MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) :: Rel MetaId)
      , PrimitiveId
    PrimMetaLess          PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (MetaId -> MetaId -> Bool) -> TCM PrimitiveImpl
    forall a b c.
    (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
     PrimType c, ToTerm c) =>
    (a -> b -> c) -> TCM PrimitiveImpl
    mkPrimFun2 (MetaId -> MetaId -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) :: Rel MetaId)
      , PrimitiveId
    PrimShowMeta          PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (MetaId -> Text) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 (ArgName -> Text
    T.pack (ArgName -> Text) -> (MetaId -> ArgName) -> MetaId -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow :: MetaId -> Text)
      , PrimitiveId
    PrimMetaToNat         PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (MetaId -> Nat) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 MetaId -> Nat
    metaToNat
      , PrimitiveId
    PrimMetaToNatInjective   PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primMetaToNatInjective

      , PrimitiveId
    PrimIMin              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primIMin'
      , PrimitiveId
    PrimIMax              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primIMax'
      , PrimitiveId
    PrimINeg              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primINeg'
      , PrimitiveId
    PrimPOr               PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primPOr
      , PrimitiveId
    PrimComp              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primComp
      , PrimitiveId
    PrimTrans             PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primTrans'
      , PrimitiveId
    PrimHComp             PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primHComp'
      , PrimitiveId
    PrimPartial           PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primPartial'
      , PrimitiveId
    PrimPartialP          PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primPartialP'
      , PrimitiveId
    PrimGlue              PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primGlue'
      , PrimitiveId
    Prim_glue             PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    prim_glue'
      , PrimitiveId
    Prim_unglue           PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    prim_unglue'
      , PrimitiveId
    PrimFaceForall        PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primFaceForall'
      , PrimitiveId
    PrimSubOut            PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primSubOut'
      , PrimitiveId
    Prim_glueU            PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    prim_glueU'
      , PrimitiveId
    Prim_unglueU          PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    prim_unglueU'
      , PrimitiveId
    PrimLockUniv          PrimitiveId
    -> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primLockUniv'
      ]
      where
        |-> :: a -> b -> (a, b)
    (|->) = (,)