    {-| 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.Function (on)
    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.Position
    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, 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.List
    import Agda.Utils.Monad
    import Agda.Utils.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
    /= :: Nat -> Nat -> Bool
    $c/= :: Nat -> Nat -> Bool
    == :: Nat -> Nat -> Bool
    $c== :: 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
    min :: Nat -> Nat -> Nat
    $cmin :: Nat -> Nat -> Nat
    max :: Nat -> Nat -> Nat
    $cmax :: Nat -> Nat -> Nat
    >= :: Nat -> Nat -> Bool
    $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
    compare :: Nat -> Nat -> Ordering
    $ccompare :: Nat -> Nat -> Ordering
    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
    fromInteger :: Integer -> Nat
    $cfromInteger :: Integer -> Nat
    signum :: Nat -> Nat
    $csignum :: Nat -> Nat
    abs :: Nat -> Nat
    $cabs :: Nat -> Nat
    negate :: Nat -> Nat
    $cnegate :: Nat -> Nat
    * :: Nat -> Nat -> Nat
    $c* :: Nat -> Nat -> Nat
    - :: Nat -> Nat -> Nat
    $c- :: Nat -> Nat -> Nat
    + :: Nat -> Nat -> Nat
    $c+ :: Nat -> Nat -> Nat
    Num, Int -> Nat
    Nat -> Int
    Nat -> [Nat]
    Nat -> Nat
    Nat -> Nat -> [Nat]
    Nat -> Nat -> Nat -> [Nat]
    (Nat -> Nat)
    -> (Nat -> Nat)
    -> (Int -> Nat)
    -> (Nat -> Int)
    -> (Nat -> [Nat])
    -> (Nat -> Nat -> [Nat])
    -> (Nat -> Nat -> [Nat])
    -> (Nat -> Nat -> Nat -> [Nat])
    -> Enum Nat
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    enumFromThenTo :: Nat -> Nat -> Nat -> [Nat]
    $cenumFromThenTo :: Nat -> Nat -> Nat -> [Nat]
    enumFromTo :: Nat -> Nat -> [Nat]
    $cenumFromTo :: Nat -> Nat -> [Nat]
    enumFromThen :: Nat -> Nat -> [Nat]
    $cenumFromThen :: Nat -> Nat -> [Nat]
    enumFrom :: Nat -> [Nat]
    $cenumFrom :: Nat -> [Nat]
    fromEnum :: Nat -> Int
    $cfromEnum :: Nat -> Int
    toEnum :: Int -> Nat
    $ctoEnum :: Int -> Nat
    pred :: Nat -> Nat
    $cpred :: Nat -> Nat
    succ :: Nat -> Nat
    $csucc :: 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
    toRational :: Nat -> Rational
    $ctoRational :: 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 (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
    /= :: Lvl -> Lvl -> Bool
    $c/= :: Lvl -> Lvl -> Bool
    == :: Lvl -> Lvl -> Bool
    $c== :: 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
    min :: Op Lvl
    $cmin :: Op Lvl
    max :: Op Lvl
    $cmax :: Op Lvl
    >= :: Lvl -> Lvl -> Bool
    $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
    compare :: Lvl -> Lvl -> Ordering
    $ccompare :: Lvl -> Lvl -> Ordering
    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
        SigmaKit
    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 sig :: Term
    sig = QName -> Elims -> Term
    Def (SigmaKit -> QName
    sigmaName SigmaKit
    sigKit) []
        Type
    a'       <- a -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (a
    forall a. HasCallStack => a
    undefined :: a)
        Type
    b'       <- b -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (b
    forall a. HasCallStack => a
    undefined :: b)
        Type Level' Term
    la  <- Sort' Term -> TCMT IO (Sort' Term)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Sort' Term -> TCMT IO (Sort' Term))
    -> Sort' Term -> TCMT IO (Sort' Term)
    forall a b. (a -> b) -> a -> b
    $ Type -> Sort' Term
    forall a. LensSort a => a -> Sort' Term
    getSort Type
    a'
        Type Level' Term
    lb  <- Sort' Term -> TCMT IO (Sort' Term)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Sort' Term -> TCMT IO (Sort' Term))
    -> Sort' Term -> TCMT IO (Sort' Term)
    forall a b. (a -> b) -> a -> b
    $ Type -> Sort' Term
    forall a. LensSort a => a -> Sort' Term
    getSort Type
    b'
        Term -> TCMT IO Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    sig TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> Term -> TCMT IO Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Level' Term -> Term
    Level Level' Term
    la)
                 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> Term -> TCMT IO Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Level' Term -> Term
    Level Level' Term
    lb)
                 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> TCMT IO Term
    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
    <@> Term -> TCMT IO Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> Term
    nolam (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    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 -> Term)
      toTermR :: TCM (a -> ReduceM Term)

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

    instance ToTerm Nat     where toTerm :: TCM (Nat -> Term)
    toTerm = (Nat -> Term) -> TCM (Nat -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Nat -> Term) -> TCM (Nat -> Term))
    -> (Nat -> Term) -> TCM (Nat -> Term)
    forall a b. (a -> b) -> a -> b
    $ 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 -> Term)
    toTerm = (Word64 -> Term) -> TCM (Word64 -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Word64 -> Term) -> TCM (Word64 -> Term))
    -> (Word64 -> Term) -> TCM (Word64 -> Term)
    forall a b. (a -> b) -> a -> b
    $ 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 -> Term)
    toTerm = (Lvl -> Term) -> TCM (Lvl -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Lvl -> Term) -> TCM (Lvl -> Term))
    -> (Lvl -> Term) -> TCM (Lvl -> Term)
    forall a b. (a -> b) -> a -> b
    $ 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 -> Term)
    toTerm = (Double -> Term) -> TCM (Double -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Double -> Term) -> TCM (Double -> Term))
    -> (Double -> Term) -> TCM (Double -> Term)
    forall a b. (a -> b) -> a -> b
    $ 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 -> Term)
    toTerm = (Char -> Term) -> TCM (Char -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Char -> Term) -> TCM (Char -> Term))
    -> (Char -> Term) -> TCM (Char -> Term)
    forall a b. (a -> b) -> a -> b
    $ 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 -> Term)
    toTerm = (Text -> Term) -> TCM (Text -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Text -> Term) -> TCM (Text -> Term))
    -> (Text -> Term) -> TCM (Text -> Term)
    forall a b. (a -> b) -> a -> b
    $ 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 -> Term)
    toTerm = (QName -> Term) -> TCM (QName -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((QName -> Term) -> TCM (QName -> Term))
    -> (QName -> Term) -> TCM (QName -> Term)
    forall a b. (a -> b) -> a -> b
    $ 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 -> Term)
    toTerm = do
        AbsolutePath
    file <- TCMT IO AbsolutePath
    forall (m :: * -> *). MonadTCEnv m => m AbsolutePath
    getCurrentPath
        (MetaId -> Term) -> TCM (MetaId -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((MetaId -> Term) -> TCM (MetaId -> Term))
    -> (MetaId -> Term) -> TCM (MetaId -> Term)
    forall a b. (a -> b) -> a -> b
    $ Literal -> Term
    Lit (Literal -> Term) -> (MetaId -> Literal) -> MetaId -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbsolutePath -> MetaId -> Literal
    LitMeta AbsolutePath
    file

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

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

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

    instance ToTerm Type where
      toTerm :: TCM (Type -> Term)
    toTerm  = do QuotingKit
    kit <- TCM QuotingKit
    quotingKit; (Type -> ReduceM Term) -> TCM (Type -> Term)
    forall a b. (a -> ReduceM b) -> TCM (a -> b)
    runReduceF (QuotingKit -> Type -> ReduceM Term
    quoteTypeWithKit QuotingKit
    kit)
      toTermR :: TCM (Type -> ReduceM Term)
    toTermR = QuotingKit -> Type -> ReduceM Term
    quoteTypeWithKit (QuotingKit -> Type -> ReduceM Term)
    -> TCM QuotingKit -> TCM (Type -> ReduceM Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM QuotingKit
    quotingKit

    instance ToTerm ArgInfo where
      toTerm :: TCM (ArgInfo -> Term)
    toTerm = do
        Term
    info <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primArgArgInfo
        Term
    vis  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primVisible
        Term
    hid  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primHidden
        Term
    ins  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primInstance
        Term
    rel  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primRelevant
        Term
    irr  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIrrelevant
        (ArgInfo -> Term) -> TCM (ArgInfo -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((ArgInfo -> Term) -> TCM (ArgInfo -> Term))
    -> (ArgInfo -> Term) -> TCM (ArgInfo -> Term)
    forall a b. (a -> b) -> a -> b
    $ \ ArgInfo
    i -> 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
              Relevance
    Relevant   -> Term
    rel
              Relevance
    Irrelevant -> Term
    irr
              Relevance
    NonStrict  -> Term
    rel
          ]

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

    instance ToTerm Fixity where
      toTerm :: TCMT IO (Fixity -> Term)
    toTerm = do
        FixityLevel -> Term
    lToTm  <- TCM (FixityLevel -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        Associativity -> Term
    aToTm  <- TCM (Associativity -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        Term
    fixity <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFixityFixity
        (Fixity -> Term) -> TCMT IO (Fixity -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Fixity -> Term) -> TCMT IO (Fixity -> Term))
    -> (Fixity -> Term) -> TCMT IO (Fixity -> Term)
    forall a b. (a -> b) -> a -> b
    $ \ Fixity{fixityAssoc :: Fixity -> Associativity
    fixityAssoc = Associativity
    a, fixityLevel :: Fixity -> FixityLevel
    fixityLevel = FixityLevel
    l} ->
          Term
    fixity Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Associativity -> Term
    aToTm Associativity
    a), Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (FixityLevel -> Term
    lToTm FixityLevel
    l)]

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

    instance ToTerm FixityLevel where
      toTerm :: TCM (FixityLevel -> Term)
    toTerm = do
        (Double -> Term
    iToTm :: PrecedenceLevel -> Term) <- TCM (Double -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        Term
    related   <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primPrecRelated
        Term
    unrelated <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primPrecUnrelated
        (FixityLevel -> Term) -> TCM (FixityLevel -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((FixityLevel -> Term) -> TCM (FixityLevel -> Term))
    -> (FixityLevel -> Term) -> TCM (FixityLevel -> Term)
    forall a b. (a -> b) -> a -> b
    $ \ FixityLevel
    p ->
          case FixityLevel
    p of
            FixityLevel
    Unrelated -> Term
    unrelated
            Related Double
    n -> Term
    related Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Double -> Term
    iToTm Double
    n]

    instance (ToTerm a, ToTerm b) => ToTerm (a, b) where
      toTerm :: TCM ((a, b) -> Term)
    toTerm = do
        SigmaKit
    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 :: Term
    con = ConHead -> ConInfo -> Elims -> Term
    Con (SigmaKit -> ConHead
    sigmaCon SigmaKit
    sigKit) ConInfo
    ConOSystem []
        a -> Term
    fromA <- TCM (a -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        b -> Term
    fromB <- TCM (b -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        ((a, b) -> Term) -> TCM ((a, b) -> Term)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (((a, b) -> Term) -> TCM ((a, b) -> Term))
    -> ((a, b) -> Term) -> TCM ((a, b) -> Term)
    forall a b. (a -> b) -> a -> b
    $ \ (a
    a, b
    b) -> Term
    con Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` (Term -> Arg Term) -> [Term] -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map Term -> Arg Term
    forall a. a -> Arg a
    defaultArg [a -> Term
    fromA a
    a, b -> 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
        Term
    nil'  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNil
        Term
    cons' <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primCons
        let nil :: Term
    nil       = Term
    nil'
            cons :: Term -> Term -> Term
    cons Term
    x Term
    xs = Term
    cons' Term -> [Term] -> Term
    forall t. Apply t => t -> [Term] -> t
    `applys` [Term
    x, Term
    xs]
        ([Term] -> Term) -> TCM ([Term] -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([Term] -> Term) -> TCM ([Term] -> Term))
    -> ([Term] -> Term) -> TCM ([Term] -> Term)
    forall a b. (a -> b) -> a -> b
    $ (Term -> Term -> Term) -> Term -> [Term] -> Term
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Term -> Term -> Term
    cons Term
    nil

    instance ToTerm a => ToTerm [a] where
      toTerm :: TCM ([a] -> Term)
    toTerm = do
        [Term] -> Term
    mkList <- TCM ([Term] -> Term)
    buildList
        a -> Term
    fromA  <- TCM (a -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        ([a] -> Term) -> TCM ([a] -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([a] -> Term) -> TCM ([a] -> Term))
    -> ([a] -> Term) -> TCM ([a] -> Term)
    forall a b. (a -> b) -> a -> b
    $ [Term] -> Term
    mkList ([Term] -> Term) -> ([a] -> [Term]) -> [a] -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> Term) -> [a] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Term
    fromA

    instance ToTerm a => ToTerm (Maybe a) where
      toTerm :: TCM (Maybe a -> Term)
    toTerm = do
        Term
    nothing <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNothing
        Term
    just    <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primJust
        a -> Term
    fromA   <- TCM (a -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        (Maybe a -> Term) -> TCM (Maybe a -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Maybe a -> Term) -> TCM (Maybe a -> Term))
    -> (Maybe a -> Term) -> TCM (Maybe a -> Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> (a -> Term) -> Maybe a -> Term
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Term
    nothing (Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    apply1 Term
    just (Term -> Term) -> (a -> Term) -> a -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Term
    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 ConHead
    pos ConInfo
    _    [] <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIntegerPos
        Con ConHead
    negsuc ConInfo
    _ [] <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIntegerNegSuc
        FromTermFunction Nat
    toNat         <- TCM (FromTermFunction Nat)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm :: TCM (FromTermFunction Nat)
        FromTermFunction Integer -> TCM (FromTermFunction Integer)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (FromTermFunction Integer -> TCM (FromTermFunction Integer))
    -> FromTermFunction Integer -> TCM (FromTermFunction Integer)
    forall a b. (a -> b) -> a -> b
    $ \ Arg Term
    v -> do
          Blocked (Arg Term)
    b <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    v
          let v' :: Arg Term
    v'  = Blocked (Arg Term) -> Arg Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked (Arg Term)
    b
              arg :: Term -> Arg Term
    arg = (Term -> Arg Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg Term
    v')
          case Arg Term -> Term
    forall e. Arg e -> e
    unArg (Blocked (Arg Term) -> Arg Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked (Arg Term)
    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) -> 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 -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction Nat
    toNat Arg Term
    u)
                  (\ MaybeReduced (Arg Term)
    u' -> 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) -> 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 -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction Nat
    toNat Arg Term
    u)
                  (\ MaybeReduced (Arg Term)
    u' -> 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 (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 AbsolutePath
    _ 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
            Term
    true  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primTrue
            Term
    false <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFalse
            (Term -> Maybe Bool) -> TCM (FromTermFunction Bool)
    forall a. (Term -> Maybe a) -> TCM (FromTermFunction a)
    fromReducedTerm ((Term -> Maybe Bool) -> TCM (FromTermFunction Bool))
    -> (Term -> Maybe Bool) -> TCM (FromTermFunction Bool)
    forall a b. (a -> b) -> a -> b
    $ \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 Int
    n [] === Var Int
    m []   = Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    m
                Term
    _        === Term
    _          = Bool
    False

    instance (ToTerm a, FromTerm a) => FromTerm [a] where
      fromTerm :: TCM (FromTermFunction [a])
    fromTerm = do
        ConHead
    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
        ConHead
    cons  <- 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
    primCons
        FromTermFunction a
    toA   <- TCM (FromTermFunction a)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm
        ConHead
    -> ConHead
    -> FromTermFunction a
    -> (a -> Term)
    -> FromTermFunction [a]
    forall {a}.
    ConHead
    -> ConHead
    -> (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
    -> (a -> Term)
    -> Arg Term
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    mkList ConHead
    nil ConHead
    cons FromTermFunction a
    toA ((a -> Term) -> FromTermFunction [a])
    -> TCMT IO (a -> Term) -> TCM (FromTermFunction [a])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (a -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    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 -> Term)
    -> Arg Term
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    mkList ConHead
    nil ConHead
    cons Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    toA a -> Term
    fromA Arg Term
    t = do
            Blocked (Arg Term)
    b <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    t
            let t :: Arg Term
    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 -> Arg Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg Term
    t)
            case Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    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 (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 Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
                  ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> 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 -> 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' -> 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) -> Args -> 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) -> 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 -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind
                      (ConHead
    -> ConHead
    -> (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
    -> (a -> Term)
    -> Arg Term
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
    mkList ConHead
    nil ConHead
    cons Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    toA a -> Term
    fromA Arg Term
    xs)
                      ((Arg Term -> Arg Term)
    -> MaybeReduced (Arg Term) -> MaybeReduced (Arg Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Arg Term -> Arg Term)
     -> MaybeReduced (Arg Term) -> MaybeReduced (Arg Term))
    -> (Arg Term -> Arg Term)
    -> MaybeReduced (Arg Term)
    -> MaybeReduced (Arg Term)
    forall a b. (a -> b) -> a -> b
    $ \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) -> Args -> 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 -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ a -> Term
    fromA a
    y, 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 (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
        ConHead
    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
        ConHead
    just    <- 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
    primJust
        FromTermFunction a
    toA     <- TCM (FromTermFunction a)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm
        FromTermFunction (Maybe a) -> TCM (FromTermFunction (Maybe a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (FromTermFunction (Maybe a) -> TCM (FromTermFunction (Maybe a)))
    -> FromTermFunction (Maybe a) -> TCM (FromTermFunction (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ \ Arg Term
    t -> do
          let arg :: Term -> Arg Term
    arg = (Term -> Arg Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg Term
    t)
          Blocked (Arg Term)
    b <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    t
          let t :: Arg Term
    t = Blocked (Arg Term) -> Arg Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked (Arg Term)
    b
          case Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    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 (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 Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
                ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> 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 -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction a
    toA Arg Term
    x)
                  (\ MaybeReduced (Arg Term)
    x' -> 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 (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 = (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
    -> TCMT
         IO (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
     -> TCMT
          IO (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)))
    -> (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
    -> TCMT
         IO (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
    forall a b. (a -> b) -> a -> b
    $ \Arg Term
    t -> do
        Blocked (Arg Term)
    b <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    t
        case Term -> Maybe a
    f (Term -> Maybe a) -> Term -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg (Blocked (Arg Term) -> Arg Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked (Arg Term)
    b) of
            Just a
    x  -> Reduced (MaybeReduced (Arg Term)) a
    -> ReduceM (Reduced (MaybeReduced (Arg Term)) 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 (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
      QName
    eqName <- TCM QName
    primEqualityName
      let lvl0 :: Level' Term
    lvl0     = Integer -> Level' Term
    ClosedLevel Integer
    0
      let eq :: Type -> TCMT IO Term -> TCMT IO Term -> TCM Type
    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 (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 (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 (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 :: TCMT IO Term
    f    = Term -> TCMT IO Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (QName -> Elims -> Term
    Def QName
    qn [])
      Type
    ty <- ArgName -> TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    nPi ArgName
    "t" (Type -> TCM Type
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Type
    a) (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
    "u" (Type -> TCM Type
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Type
    a) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $
                  (Type -> TCMT IO Term -> TCMT IO Term -> TCM Type
    eq Type
    b (TCMT IO Term
    f TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    1) (TCMT IO Term
    f TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    0))
              TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> (Type -> TCMT IO Term -> TCMT IO Term -> TCM Type
    eq Type
    a (      Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    1) (      Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    0))

        -- Get the constructor corresponding to BUILTIN REFL
      Arg Term -> Term
    refl <- TCM (Arg Term -> Term)
    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@.
      PrimitiveImpl -> TCM PrimitiveImpl
    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
    ty (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
    forall a b. (a -> b) -> a -> b
    $ QName
    -> Int
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Int
    3 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \ Args
    ts -> do
        let t :: Arg Term
    t  = Arg Term -> Args -> Arg Term
    forall a. a -> [a] -> a
    headWithDefault Arg Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Args
    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
    $ Args -> Maybe (Arg Term)
    forall a. [a] -> Maybe a
    lastMaybe Args
    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 (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 (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)) -> Args -> MaybeReducedArgs
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced Args
    ts

    primMetaToNatInjective :: TCM PrimitiveImpl
    primMetaToNatInjective :: TCM PrimitiveImpl
    primMetaToNatInjective = do
      Type
    meta  <- MetaId -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (MetaId
    forall a. HasCallStack => a
    undefined :: MetaId)
      Type
    nat   <- Nat -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Nat
    forall a. HasCallStack => a
    undefined :: Nat)
      QName
    toNat <- PrimFun -> QName
    primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgName -> TCMT IO PrimFun
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m PrimFun
    getPrimitive ArgName
    "primMetaToNat"
      Type -> Type -> QName -> TCM PrimitiveImpl
    mkPrimInjective Type
    meta Type
    nat QName
    toNat

    primCharToNatInjective :: TCM PrimitiveImpl
    primCharToNatInjective :: TCM PrimitiveImpl
    primCharToNatInjective = do
      Type
    char  <- Char -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Char
    forall a. HasCallStack => a
    undefined :: Char)
      Type
    nat   <- Nat -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Nat
    forall a. HasCallStack => a
    undefined :: Nat)
      QName
    toNat <- PrimFun -> QName
    primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgName -> TCMT IO PrimFun
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m PrimFun
    getPrimitive ArgName
    "primCharToNat"
      Type -> Type -> QName -> TCM PrimitiveImpl
    mkPrimInjective Type
    char Type
    nat QName
    toNat

    primStringToListInjective :: TCM PrimitiveImpl
    primStringToListInjective :: TCM PrimitiveImpl
    primStringToListInjective = do
      Type
    string <- Text -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Text
    forall a. HasCallStack => a
    undefined :: Text)
      Type
    chars  <- ArgName -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (ArgName
    forall a. HasCallStack => a
    undefined :: String)
      QName
    toList <- PrimFun -> QName
    primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgName -> TCMT IO PrimFun
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m PrimFun
    getPrimitive ArgName
    "primStringToList"
      Type -> Type -> QName -> TCM PrimitiveImpl
    mkPrimInjective Type
    string Type
    chars QName
    toList

    primStringFromListInjective :: TCM PrimitiveImpl
    primStringFromListInjective :: TCM PrimitiveImpl
    primStringFromListInjective = do
      Type
    chars  <- ArgName -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (ArgName
    forall a. HasCallStack => a
    undefined :: String)
      Type
    string <- Text -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Text
    forall a. HasCallStack => a
    undefined :: Text)
      QName
    fromList <- PrimFun -> QName
    primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgName -> TCMT IO PrimFun
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m PrimFun
    getPrimitive ArgName
    "primStringFromList"
      Type -> Type -> QName -> TCM PrimitiveImpl
    mkPrimInjective Type
    chars Type
    string QName
    fromList

    primWord64ToNatInjective :: TCM PrimitiveImpl
    primWord64ToNatInjective :: TCM PrimitiveImpl
    primWord64ToNatInjective =  do
      Type
    word  <- Word64 -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Word64
    forall a. HasCallStack => a
    undefined :: Word64)
      Type
    nat   <- Nat -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Nat
    forall a. HasCallStack => a
    undefined :: Nat)
      QName
    toNat <- PrimFun -> QName
    primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgName -> TCMT IO PrimFun
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m PrimFun
    getPrimitive ArgName
    "primWord64ToNat"
      Type -> Type -> QName -> TCM PrimitiveImpl
    mkPrimInjective Type
    word Type
    nat QName
    toNat

    primFloatToWord64Injective :: TCM PrimitiveImpl
    primFloatToWord64Injective :: TCM PrimitiveImpl
    primFloatToWord64Injective = do
      Type
    float  <- Double -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Double
    forall a. HasCallStack => a
    undefined :: Double)
      Type
    word   <- Word64 -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Word64
    forall a. HasCallStack => a
    undefined :: Word64)
      QName
    toWord <- PrimFun -> QName
    primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgName -> TCMT IO PrimFun
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m PrimFun
    getPrimitive ArgName
    "primFloatToWord64"
      Type -> Type -> QName -> TCM PrimitiveImpl
    mkPrimInjective Type
    float Type
    word QName
    toWord

    primQNameToWord64sInjective :: TCM PrimitiveImpl
    primQNameToWord64sInjective :: TCM PrimitiveImpl
    primQNameToWord64sInjective = do
      Type
    name    <- QName -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (QName
    forall a. HasCallStack => a
    undefined :: QName)
      Type
    words   <- (Word64, Word64) -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType ((Word64, Word64)
    forall a. HasCallStack => a
    undefined :: (Word64, Word64))
      QName
    toWords <- PrimFun -> QName
    primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgName -> TCMT IO PrimFun
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m PrimFun
    getPrimitive ArgName
    "primQNameToWord64s"
      Type -> Type -> QName -> TCM PrimitiveImpl
    mkPrimInjective Type
    name Type
    words QName
    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 :: Term
    con@(Con ConHead
    rf ConInfo
    ci []) <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primRefl
      Maybe ArgInfo
    minfo <- (ArgInfo -> ArgInfo) -> Maybe ArgInfo -> Maybe ArgInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Origin -> ArgInfo -> ArgInfo
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Inserted) (Maybe ArgInfo -> Maybe ArgInfo)
    -> TCMT IO (Maybe ArgInfo) -> TCMT IO (Maybe ArgInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ConHead -> TCMT IO (Maybe ArgInfo)
    getReflArgInfo ConHead
    rf
      (Arg Term -> Term) -> TCM (Arg Term -> Term)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((Arg Term -> Term) -> TCM (Arg Term -> Term))
    -> (Arg Term -> Term) -> TCM (Arg Term -> Term)
    forall a b. (a -> b) -> a -> b
    $ case Maybe ArgInfo
    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
      QName
    eq   <- TCM QName
    primEqualityName
      Type
    eqTy <- Definition -> Type
    defType (Definition -> Type) -> TCMT IO Definition -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    eq
      -- E.g. @eqTy = eqTel → Set a@ where @eqTel = {a : Level} {A : Set a} (x y : A)@.
      TelV Tele (Dom Type)
    eqTel Type
    eqCore <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    eqTy
      let eqSort :: Sort' Term
    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@.
      Type
    t <- let xeqy :: TCM Type
    xeqy = Type -> TCM Type
    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) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Args -> Elims) -> Args -> Elims
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Args
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    eqTel in
           Tele (Dom Type) -> Type -> Type
    telePi_ ((Dom Type -> Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Dom Type -> Dom Type
    forall a. LensHiding a => a -> a
    hide Tele (Dom Type)
    eqTel) (Type -> Type) -> TCM Type -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCM Type
    xeqy TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> TCM Type
    xeqy)

      -- Get the constructor corresponding to BUILTIN REFL
      Arg Term -> Term
    refl <- TCM (Arg Term -> Term)
    getRefl

      -- The implementation of primEraseEquality:
      PrimitiveImpl -> TCM PrimitiveImpl
    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
    -> Int
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    eqTel) ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \ Args
    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
    $ Args -> Maybe (Arg Term, Arg Term)
    forall a. [a] -> Maybe (a, a)
    last2 (Args -> Maybe (Arg Term, Arg Term))
    -> Maybe Args -> Maybe (Arg Term, Arg Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Args -> Maybe Args
    forall a. [a] -> Maybe [a]
    initMaybe Args
    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.
        (Arg Term
    u', Arg Term
    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 Arg Term
    u' Arg Term -> Arg Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Arg Term
    v' then 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
    u else
          Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    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)) -> Args -> MaybeReducedArgs
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced Args
    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
      Definition
    def <- ConHead -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
    getConInfo ConHead
    rf
      TelV Tele (Dom Type)
    reflTel Type
    _ <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type
    defType Definition
    def
      Maybe ArgInfo -> TCMT IO (Maybe ArgInfo)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe ArgInfo -> TCMT IO (Maybe ArgInfo))
    -> Maybe ArgInfo -> TCMT IO (Maybe ArgInfo)
    forall a b. (a -> b) -> a -> b
    $ (Dom (ArgName, Type) -> ArgInfo)
    -> Maybe (Dom (ArgName, Type)) -> Maybe ArgInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Dom (ArgName, Type) -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo (Maybe (Dom (ArgName, Type)) -> Maybe ArgInfo)
    -> Maybe (Dom (ArgName, Type)) -> Maybe ArgInfo
    forall a b. (a -> b) -> a -> b
    $ [Dom (ArgName, Type)] -> Maybe (Dom (ArgName, Type))
    forall a. [a] -> Maybe a
    listToMaybe ([Dom (ArgName, Type)] -> Maybe (Dom (ArgName, Type)))
    -> [Dom (ArgName, Type)] -> Maybe (Dom (ArgName, Type))
    forall a b. (a -> b) -> a -> b
    $ Int -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
    forall a. Int -> [a] -> [a]
    drop (Defn -> Int
    conPars (Defn -> Int) -> Defn -> Int
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    def) ([Dom (ArgName, Type)] -> [Dom (ArgName, Type)])
    -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    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 :: Int -> f a -> f (Type'' Term a)
    varEl Int
    s f a
    a = Sort' Term -> a -> Type'' Term a
    forall t a. Sort' t -> a -> Type'' t a
    El (Int -> Sort' Term
    varSort Int
    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 :: Int -> Int -> f Type
    varT Int
    s Int
    a  = Int -> f Term -> f Type
    forall {f :: * -> *} {a}.
    Functor f =>
    Int -> f a -> f (Type'' Term a)
    varEl Int
    s (Int -> f Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    a)
          varS :: Int -> f Type
    varS Int
    s    = Type -> f Type
    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
    $ Int -> Sort' Term
    varSort Int
    s
      Type
    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" (Int -> TCM Type
    forall {f :: * -> *}. Applicative f => Int -> f Type
    varS Int
    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" (Int -> Int -> TCM Type
    forall {f :: * -> *}. Applicative f => Int -> Int -> f Type
    varT Int
    2 Int
    0 TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> Int -> TCM Type
    forall {f :: * -> *}. Applicative f => Int -> f Type
    varS Int
    1) TCM Type
    b
      PrimitiveImpl -> TCM PrimitiveImpl
    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
    -> Int
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Int
    6 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \ Args
    ts ->
        case Args
    ts of
          [Arg Term
    a, Arg Term
    b, Arg Term
    s, Arg Term
    t, Arg Term
    u, Arg Term
    f] -> do
            Blocked (Arg Term)
    u <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    u
            let isWHNF :: Blocked' t (Arg Term) -> m Bool
    isWHNF Blocked{} = Bool -> m Bool
    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 (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                    Con{}      -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                    Lam{}      -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                    Pi{}       -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                    Sort{}     -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True  -- sorts and levels are considered whnf
                    Level{}    -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                    DontCare{} -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                    Def QName
    q Elims
    _    -> do
                      Defn
    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
                      Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ case Defn
    def of
                        Datatype{} -> Bool
    True
                        Record{}   -> Bool
    True
                        Defn
    _          -> Bool
    False
                    Var{}      -> Bool -> m Bool
    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
            ReduceM Bool
    -> ReduceM (Reduced MaybeReducedArgs Term)
    -> ReduceM (Reduced MaybeReducedArgs Term)
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Blocked (Arg Term) -> ReduceM Bool
    forall {m :: * -> *} {t}.
    HasConstInfo m =>
    Blocked' t (Arg Term) -> m Bool
    isWHNF Blocked (Arg Term)
    u)
                (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
    $ Term -> Arg Term -> Term
    ret (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    f) (Blocked (Arg Term) -> Arg Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked (Arg Term)
    u))
                (Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    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)) -> Args -> MaybeReducedArgs
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced [Arg Term
    a, Arg Term
    b, Arg Term
    s, Arg Term
    t] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
    forall a. [a] -> [a] -> [a]
    ++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    u, Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced Arg Term
    f])
          Args
    _ -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    primForce :: TCM PrimitiveImpl
    primForce :: TCM PrimitiveImpl
    primForce = do
      let varEl :: Int -> f a -> f (Type'' Term a)
    varEl Int
    s f a
    a = Sort' Term -> a -> Type'' Term a
    forall t a. Sort' t -> a -> Type'' t a
    El (Int -> Sort' Term
    varSort Int
    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 :: Int -> Int -> f Type
    varT Int
    s Int
    a  = Int -> f Term -> f Type
    forall {f :: * -> *} {a}.
    Functor f =>
    Int -> f a -> f (Type'' Term a)
    varEl Int
    s (Int -> f Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    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" (Int -> Int -> TCM Type
    forall {f :: * -> *}. Applicative f => Int -> Int -> f Type
    varT Int
    3 Int
    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" (Int -> Int -> TCM Type
    forall {f :: * -> *}. Applicative f => Int -> Int -> f Type
    varT Int
    4 Int
    2) (Int -> TCMT IO Term -> TCM Type
    forall {f :: * -> *} {a}.
    Functor f =>
    Int -> f a -> f (Type'' Term a)
    varEl Int
    4 (TCMT IO Term -> TCM Type) -> TCMT IO Term -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    2 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    0) TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    -->
                    Int -> TCMT IO Term -> TCM Type
    forall {f :: * -> *} {a}.
    Functor f =>
    Int -> f a -> f (Type'' Term a)
    varEl Int
    3 (Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    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 -> Args -> Term
    forall t. Apply t => t -> Args -> t
    apply Term
    f [Arg Term
    u]

    primForceLemma :: TCM PrimitiveImpl
    primForceLemma :: TCM PrimitiveImpl
    primForceLemma = do
      let varEl :: Int -> f a -> f (Type'' Term a)
    varEl Int
    s f a
    a = Sort' Term -> a -> Type'' Term a
    forall t a. Sort' t -> a -> Type'' t a
    El (Int -> Sort' Term
    varSort Int
    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 :: Int -> Int -> f Type
    varT Int
    s Int
    a  = Int -> f Term -> f Type
    forall {f :: * -> *} {a}.
    Functor f =>
    Int -> f a -> f (Type'' Term a)
    varEl Int
    s (Int -> f Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    a)
      Term
    refl  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primRefl
      QName
    force <- PrimFun -> QName
    primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgName -> TCMT IO PrimFun
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m PrimFun
    getPrimitive ArgName
    "primForce"
      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" (Int -> Int -> TCM Type
    forall {f :: * -> *}. Applicative f => Int -> Int -> f Type
    varT Int
    3 Int
    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
    "f" (ArgName -> TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    nPi ArgName
    "y" (Int -> Int -> TCM Type
    forall {f :: * -> *}. Applicative f => Int -> Int -> f Type
    varT Int
    4 Int
    2) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Term -> TCM Type
    forall {f :: * -> *} {a}.
    Functor f =>
    Int -> f a -> f (Type'' Term a)
    varEl Int
    4 (TCMT IO Term -> TCM Type) -> TCMT IO Term -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    2 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $
                    Int -> TCMT IO Term -> TCM Type
    forall {f :: * -> *} {a}.
    Functor f =>
    Int -> f a -> f (Type'' Term a)
    varEl Int
    4 (TCMT IO Term -> TCM Type) -> TCMT IO Term -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primEquality TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    4 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    2 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    1)
                                           TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (Term -> TCMT IO Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (QName -> Elims -> Term
    Def QName
    force []) TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    5 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    4 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    3 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    2 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    0)
                                           TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    0 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    1)
                   ) ((Term -> Arg Term -> Term) -> TCM PrimitiveImpl)
    -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
    forall a b. (a -> b) -> a -> b
    $ \ Term
    _ Arg Term
    _ -> Term
    refl

    mkPrimLevelZero :: TCM PrimitiveImpl
    mkPrimLevelZero :: TCM PrimitiveImpl
    mkPrimLevelZero = do
      Type
    t <- Lvl -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Lvl
    forall a. HasCallStack => a
    undefined :: Lvl)
      PrimitiveImpl -> TCM PrimitiveImpl
    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
    -> Int
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Int
    0 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \Args
    _ -> 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
      Type
    t <- (Lvl -> Lvl) -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType (Lvl -> Lvl
    forall a. a -> a
    id :: Lvl -> Lvl)
      PrimitiveImpl -> TCM PrimitiveImpl
    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
    -> Int
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Int
    1 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \ ~[Arg Term
    a] -> do
        Level' Term
    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
        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
    $ Level' Term -> Level' Term
    levelSuc Level' Term
    l

    mkPrimLevelMax :: TCM PrimitiveImpl
    mkPrimLevelMax :: TCM PrimitiveImpl
    mkPrimLevelMax = do
      Type
    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)
      PrimitiveImpl -> TCM PrimitiveImpl
    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
    -> Int
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Int
    2 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \ ~[Arg Term
    a, Arg Term
    b] -> do
        Level' Term
    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
        Level' Term
    b' <- 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
    b
        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
    $ Level' Term -> Level' Term -> Level' Term
    levelLub Level' Term
    a' Level' Term
    b'

    mkPrimSetOmega :: IsFibrant -> TCM PrimitiveImpl
    mkPrimSetOmega :: IsFibrant -> TCM PrimitiveImpl
    mkPrimSetOmega IsFibrant
    f = do
      let t :: Type
    t = Sort' Term -> Type
    sort (Sort' Term -> Type) -> Sort' Term -> Type
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort' Term
    forall t. IsFibrant -> Integer -> Sort' t
    Inf IsFibrant
    f Integer
    1
      PrimitiveImpl -> TCM PrimitiveImpl
    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
    -> Int
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Int
    0 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \Args
    _ -> 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 -> Term) -> Sort' Term -> Term
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort' Term
    forall t. IsFibrant -> Integer -> Sort' t
    Inf IsFibrant
    f Integer
    0

    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 (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
    -> Int
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Int
    0 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \Args
    _ -> 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

    -- mkPrimStrictSet :: TCM PrimitiveImpl
    -- mkPrimStrictSet = do
    --   t <- nPi "ℓ" (el primLevel) (pure $ sort $ SSet $ Max 0 [Plus 1 $ var 0])
    --   return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ ~[a] -> do
    --     l <- levelView' $ unArg a
    --     redReturn $ Sort $ SSet l

    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
        FromTermFunction a
    toA   <- TCM (FromTermFunction a)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm
        b -> ReduceM Term
    fromB <- TCM (b -> ReduceM Term)
    forall a. ToTerm a => TCM (a -> ReduceM Term)
    toTermR
        Type
    t     <- TCM Type
    mt
        PrimitiveImpl -> TCM PrimitiveImpl
    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
    -> Int
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Int
    1 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \Args
    ts ->
          case Args
    ts of
            [Arg Term
    v] ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction a
    toA Arg Term
    v) 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
                Term
    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 (MetaId -> Set MetaId) -> Term -> Set MetaId
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton Term
    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 (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)]
            Args
    _ -> 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
        FromTermFunction a
    toA   <- TCM (FromTermFunction a)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm
        b -> Term
    fromB <- TCM (b -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        Type
    t     <- (a -> b) -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType a -> b
    f
        PrimitiveImpl -> TCM PrimitiveImpl
    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
    -> Int
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Int
    1 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \Args
    ts ->
          case Args
    ts of
            [Arg Term
    v] ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction a
    toA Arg Term
    v) 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))
    -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ b -> Term
    fromB (b -> Term) -> b -> Term
    forall a b. (a -> b) -> a -> b
    $ a -> b
    f a
    x
            Args
    _ -> 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
        FromTermFunction a
    toA   <- TCM (FromTermFunction a)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm
        a -> Term
    fromA <- TCM (a -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        FromTermFunction b
    toB   <- TCM (FromTermFunction b)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm
        c -> Term
    fromC <- TCM (c -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        Type
    t     <- (a -> b -> c) -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType a -> b -> c
    f
        PrimitiveImpl -> TCM PrimitiveImpl
    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
    -> Int
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Int
    2 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \Args
    ts ->
          case Args
    ts of
            [Arg Term
    v,Arg Term
    w] ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction a
    toA Arg Term
    v)
                  (\MaybeReduced (Arg Term)
    v' -> [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) -> MaybeReducedArgs)
    -> (b -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction b
    toB Arg Term
    w)
                  (\MaybeReduced (Arg Term)
    w' -> [ Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced (Blocked (Arg Term) -> MaybeReduced (Arg Term))
    -> Blocked (Arg Term) -> MaybeReduced (Arg Term)
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Blocked (Arg Term)
    forall a t. a -> Blocked' t a
    notBlocked (Arg Term -> Blocked (Arg Term)) -> Arg Term -> Blocked (Arg Term)
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg (Arg Term -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo Arg Term
    v) (a -> Term
    fromA a
    x)
                          , MaybeReduced (Arg Term)
    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))
    -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ c -> Term
    fromC (c -> Term) -> c -> Term
    forall a b. (a -> b) -> a -> b
    $ a -> b -> c
    f a
    x b
    y
            Args
    _ -> 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
        (FromTermFunction a
    toA, a -> Term
    fromA) <- (,) (FromTermFunction a
     -> (a -> Term) -> (FromTermFunction a, a -> Term))
    -> TCMT IO (FromTermFunction a)
    -> TCMT IO ((a -> Term) -> (FromTermFunction a, a -> 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 -> Term) -> (FromTermFunction a, a -> Term))
    -> TCMT IO (a -> Term) -> TCMT IO (FromTermFunction a, a -> Term)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TCMT IO (a -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        (FromTermFunction b
    toB, b -> Term
    fromB) <- (,) (FromTermFunction b
     -> (b -> Term) -> (FromTermFunction b, b -> Term))
    -> TCMT IO (FromTermFunction b)
    -> TCMT IO ((b -> Term) -> (FromTermFunction b, b -> Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (FromTermFunction b)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm TCMT IO ((b -> Term) -> (FromTermFunction b, b -> Term))
    -> TCMT IO (b -> Term) -> TCMT IO (FromTermFunction b, b -> Term)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TCMT IO (b -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        FromTermFunction c
    toC          <- TCM (FromTermFunction c)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm
        d -> Term
    fromD        <- TCM (d -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        Type
    t <- (a -> b -> c -> d) -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType a -> b -> c -> d
    f
        PrimitiveImpl -> TCM PrimitiveImpl
    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
    -> Int
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Int
    3 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \Args
    ts ->
          let argFrom :: (t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
    argFrom t -> Term
    fromX Arg e
    a t
    x =
                Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced (Blocked (Arg Term) -> MaybeReduced (Arg Term))
    -> Blocked (Arg Term) -> MaybeReduced (Arg Term)
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Blocked (Arg Term)
    forall a t. a -> Blocked' t a
    notBlocked (Arg Term -> Blocked (Arg Term)) -> Arg Term -> Blocked (Arg Term)
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg (Arg e -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo Arg e
    a) (t -> Term
    fromX t
    x)
          in case Args
    ts of
            [Arg Term
    a,Arg Term
    b,Arg Term
    c] ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction a
    toA Arg Term
    a)
                  (\MaybeReduced (Arg Term)
    a' -> [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) -> MaybeReducedArgs)
    -> (b -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction b
    toB Arg Term
    b)
                  (\MaybeReduced (Arg Term)
    b' -> [(a -> Term) -> Arg Term -> a -> MaybeReduced (Arg Term)
    forall {t} {e}.
    (t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
    argFrom a -> Term
    fromA Arg Term
    a a
    x, MaybeReduced (Arg Term)
    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) -> MaybeReducedArgs)
    -> (c -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction c
    toC Arg Term
    c)
                  (\MaybeReduced (Arg Term)
    c' -> [ (a -> Term) -> Arg Term -> a -> MaybeReduced (Arg Term)
    forall {t} {e}.
    (t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
    argFrom a -> Term
    fromA Arg Term
    a a
    x, (b -> Term) -> Arg Term -> b -> MaybeReduced (Arg Term)
    forall {t} {e}.
    (t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
    argFrom b -> Term
    fromB Arg Term
    b b
    y, 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))
    -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ d -> Term
    fromD (d -> Term) -> d -> Term
    forall a b. (a -> b) -> a -> b
    $ a -> b -> c -> d
    f a
    x b
    y c
    z
            Args
    _ -> 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
        (FromTermFunction a
    toA, a -> Term
    fromA) <- (,) (FromTermFunction a
     -> (a -> Term) -> (FromTermFunction a, a -> Term))
    -> TCMT IO (FromTermFunction a)
    -> TCMT IO ((a -> Term) -> (FromTermFunction a, a -> 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 -> Term) -> (FromTermFunction a, a -> Term))
    -> TCMT IO (a -> Term) -> TCMT IO (FromTermFunction a, a -> Term)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TCMT IO (a -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        (FromTermFunction b
    toB, b -> Term
    fromB) <- (,) (FromTermFunction b
     -> (b -> Term) -> (FromTermFunction b, b -> Term))
    -> TCMT IO (FromTermFunction b)
    -> TCMT IO ((b -> Term) -> (FromTermFunction b, b -> Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (FromTermFunction b)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm TCMT IO ((b -> Term) -> (FromTermFunction b, b -> Term))
    -> TCMT IO (b -> Term) -> TCMT IO (FromTermFunction b, b -> Term)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TCMT IO (b -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        (FromTermFunction c
    toC, c -> Term
    fromC) <- (,) (FromTermFunction c
     -> (c -> Term) -> (FromTermFunction c, c -> Term))
    -> TCMT IO (FromTermFunction c)
    -> TCMT IO ((c -> Term) -> (FromTermFunction c, c -> Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (FromTermFunction c)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm TCMT IO ((c -> Term) -> (FromTermFunction c, c -> Term))
    -> TCMT IO (c -> Term) -> TCMT IO (FromTermFunction c, c -> Term)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TCMT IO (c -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        FromTermFunction d
    toD          <- TCM (FromTermFunction d)
    forall a. FromTerm a => TCM (FromTermFunction a)
    fromTerm
        e -> Term
    fromE        <- TCM (e -> Term)
    forall a. ToTerm a => TCMT IO (a -> Term)
    toTerm
        Type
    t <- (a -> b -> c -> d -> e) -> TCM Type
    forall a. PrimType a => a -> TCM Type
    primType a -> b -> c -> d -> e
    f
        PrimitiveImpl -> TCM PrimitiveImpl
    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
    -> Int
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    primFun QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Int
    4 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
    -> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \Args
    ts ->
          let argFrom :: (t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
    argFrom t -> Term
    fromX Arg e
    a t
    x =
                Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced (Blocked (Arg Term) -> MaybeReduced (Arg Term))
    -> Blocked (Arg Term) -> MaybeReduced (Arg Term)
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Blocked (Arg Term)
    forall a t. a -> Blocked' t a
    notBlocked (Arg Term -> Blocked (Arg Term)) -> Arg Term -> Blocked (Arg Term)
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg (Arg e -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo Arg e
    a) (t -> Term
    fromX t
    x)
          in case Args
    ts of
            [Arg Term
    a,Arg Term
    b,Arg Term
    c,Arg Term
    d] ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) a)
    -> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
    -> (a -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction a
    toA Arg Term
    a)
                  (\MaybeReduced (Arg Term)
    a' -> MaybeReduced (Arg Term)
    a' MaybeReduced (Arg Term) -> MaybeReducedArgs -> MaybeReducedArgs
    forall a. a -> [a] -> [a]
    : (Arg Term -> MaybeReduced (Arg Term)) -> Args -> 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) -> MaybeReducedArgs)
    -> (b -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction b
    toB Arg Term
    b)
                  (\MaybeReduced (Arg Term)
    b' -> [(a -> Term) -> Arg Term -> a -> MaybeReduced (Arg Term)
    forall {t} {e}.
    (t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
    argFrom a -> Term
    fromA Arg Term
    a a
    x, MaybeReduced (Arg Term)
    b', Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced Arg Term
    c, 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) -> MaybeReducedArgs)
    -> (c -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction c
    toC Arg Term
    c)
                  (\MaybeReduced (Arg Term)
    c' -> [ (a -> Term) -> Arg Term -> a -> MaybeReduced (Arg Term)
    forall {t} {e}.
    (t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
    argFrom a -> Term
    fromA Arg Term
    a a
    x
                          , (b -> Term) -> Arg Term -> b -> MaybeReduced (Arg Term)
    forall {t} {e}.
    (t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
    argFrom b -> Term
    fromB Arg Term
    b b
    y
                          , MaybeReduced (Arg Term)
    c', 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) -> MaybeReducedArgs)
    -> (d -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a' b b'.
    ReduceM (Reduced a a')
    -> (a -> b)
    -> (a' -> ReduceM (Reduced b b'))
    -> ReduceM (Reduced b b')
    redBind (FromTermFunction d
    toD Arg Term
    d)
                  (\MaybeReduced (Arg Term)
    d' -> [ (a -> Term) -> Arg Term -> a -> MaybeReduced (Arg Term)
    forall {t} {e}.
    (t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
    argFrom a -> Term
    fromA Arg Term
    a a
    x
                          , (b -> Term) -> Arg Term -> b -> MaybeReduced (Arg Term)
    forall {t} {e}.
    (t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
    argFrom b -> Term
    fromB Arg Term
    b b
    y
                          , (c -> Term) -> Arg Term -> c -> MaybeReduced (Arg Term)
    forall {t} {e}.
    (t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
    argFrom c -> Term
    fromC Arg Term
    c c
    z
                          , 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))
    -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ e -> Term
    fromE (e -> Term) -> e -> Term
    forall a b. (a -> b) -> a -> b
    $ a -> b -> c -> d -> e
    f a
    x b
    y c
    z d
    w
            Args
    _ -> 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 String (TCM PrimitiveImpl)
    primitiveFunctions :: Map ArgName (TCM PrimitiveImpl)
    primitiveFunctions = TCM PrimitiveImpl -> TCM PrimitiveImpl
    forall a. TCM a -> TCM a
    localTCStateSavingWarnings (TCM PrimitiveImpl -> TCM PrimitiveImpl)
    -> Map ArgName (TCM PrimitiveImpl)
    -> Map ArgName (TCM PrimitiveImpl)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCM PrimitiveImpl -> TCM PrimitiveImpl -> TCM PrimitiveImpl)
    -> [(ArgName, TCM PrimitiveImpl)]
    -> Map ArgName (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)
      [ ArgName
    "primShowInteger"     ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primNatPlus"         ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primNatMinus"        ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primNatTimes"        ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primNatDivSucAux"    ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primNatModSucAux"    ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primNatEquality"     ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primNatLess"         ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primShowNat"         ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primWord64ToNat"     ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primWord64FromNat"   ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primWord64ToNatInjective" ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primWord64ToNatInjective

      -- Level functions
      , ArgName
    "primLevelZero"       ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    mkPrimLevelZero
      , ArgName
    "primLevelSuc"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    mkPrimLevelSuc
      , ArgName
    "primLevelMax"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    mkPrimLevelMax

      -- Sorts
      , ArgName
    "primSetOmega"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> IsFibrant -> TCM PrimitiveImpl
    mkPrimSetOmega IsFibrant
    IsFibrant
      , ArgName
    "primStrictSetOmega"  ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> IsFibrant -> TCM PrimitiveImpl
    mkPrimSetOmega IsFibrant
    IsStrict

      -- 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).
      --
      , ArgName
    "primFloatEquality"          ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatInequality"        ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatLess"              ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatIsInfinite"        ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primFloatIsNaN"             ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primFloatIsNegativeZero"    ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primFloatIsSafeInteger"     ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatToWord64"          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> (Double -> Word64) -> TCM PrimitiveImpl
    forall a b.
    (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
    (a -> b) -> TCM PrimitiveImpl
    mkPrimFun1 Double -> Word64
    doubleToWord64
      , ArgName
    "primFloatToWord64Injective" ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primFloatToWord64Injective
      , ArgName
    "primNatToFloat"             ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primIntToFloat"             ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primFloatRound"             ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatFloor"             ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatCeiling"           ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatToRatio"           ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primRatioToFloat"           ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatDecode"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatEncode"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primShowFloat"              ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primFloatPlus"              ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatMinus"             ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatTimes"             ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatNegate"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatDiv"               ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatPow"               ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatSqrt"              ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatExp"               ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatLog"               ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatSin"               ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatCos"               ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatTan"               ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatASin"              ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatACos"              ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatATan"              ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatATan2"             ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatSinh"              ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatCosh"              ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatTanh"              ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatASinh"             ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatACosh"             ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primFloatATanh"             ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primCharEquality"       ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primIsLower"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primIsDigit"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primIsAlpha"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primIsSpace"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primIsAscii"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primIsLatin1"           ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primIsPrint"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primIsHexDigit"         ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primToUpper"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primToLower"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primCharToNat"          ArgName -> TCM PrimitiveImpl -> (ArgName, 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 (Int -> Nat
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Nat) -> (Char -> Int) -> Char -> Nat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> Int
    forall a. Enum a => a -> Int
    fromEnum :: Char -> Nat)
      , ArgName
    "primCharToNatInjective" ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primCharToNatInjective
      , ArgName
    "primNatToChar"          ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primShowChar"           ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primStringToList"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primStringToListInjective"   ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primStringToListInjective
      , ArgName
    "primStringFromList"          ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primStringFromListInjective" ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primStringFromListInjective
      , ArgName
    "primStringAppend"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primStringEquality"          ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primShowString"              ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primStringUncons"            ArgName -> TCM PrimitiveImpl -> (ArgName, 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
      , ArgName
    "primEraseEquality"   ArgName -> TCM PrimitiveImpl -> (ArgName, 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.
      , ArgName
    "primForce"           ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primForce
      , ArgName
    "primForceLemma"      ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primForceLemma
      , ArgName
    "primQNameEquality"   ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primQNameLess"       ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primShowQName"       ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primQNameFixity"     ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primQNameToWord64s"  ArgName -> TCM PrimitiveImpl -> (ArgName, 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))
      , ArgName
    "primQNameToWord64sInjective" ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primQNameToWord64sInjective
      , ArgName
    "primMetaEquality"    ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primMetaLess"        ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primShowMeta"        ArgName -> TCM PrimitiveImpl -> (ArgName, 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)
      , ArgName
    "primMetaToNat"       ArgName -> TCM PrimitiveImpl -> (ArgName, 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 (Int -> Nat
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Nat) -> (MetaId -> Int) -> MetaId -> Nat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> Int
    metaId :: MetaId -> Nat)
      , ArgName
    "primMetaToNatInjective" ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primMetaToNatInjective
      , ArgName
    "primIMin"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primIMin'
      , ArgName
    "primIMax"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primIMax'
      , ArgName
    "primINeg"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primINeg'
      , ArgName
    "primPOr"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primPOr
      , ArgName
    "primComp"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primComp
      , ArgName
    builtinTrans          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primTrans'
      , ArgName
    builtinHComp          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primHComp'
      , ArgName
    "primIdJ"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primIdJ
      , ArgName
    "primPartial"         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primPartial'
      , ArgName
    "primPartialP"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primPartialP'
      , ArgName
    builtinGlue           ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primGlue'
      , ArgName
    builtin_glue          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    prim_glue'
      , ArgName
    builtin_unglue        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    prim_unglue'
      , ArgName
    builtinFaceForall     ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primFaceForall'
      , ArgName
    "primDepIMin"         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primDepIMin'
      , ArgName
    "primIdFace"          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primIdFace'
      , ArgName
    "primIdPath"          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primIdPath'
      , ArgName
    builtinIdElim         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primIdElim'
      , ArgName
    builtinSubOut         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primSubOut'
      , ArgName
    builtin_glueU         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    prim_glueU'
      , ArgName
    builtin_unglueU       ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    prim_unglueU'
      , ArgName
    builtinLockUniv       ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
    forall a b. a -> b -> (a, b)
    |-> TCM PrimitiveImpl
    primLockUniv'
      ]
      where
        |-> :: a -> b -> (a, b)
    (|->) = (,)