    {-# LANGUAGE ApplicativeDo #-}

    module Agda.TypeChecking.Primitive.Base where

    -- Control.Monad.Fail import is redundant since GHC 8.8.1
    import Control.Monad.Fail (MonadFail)

    import qualified Data.Map as Map

    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Builtin
    import Agda.TypeChecking.Monad.Context
    import Agda.TypeChecking.Monad.Debug
    import Agda.TypeChecking.Names
    import {-# SOURCE #-} Agda.TypeChecking.Primitive
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Reduce ( reduce )
    import Agda.TypeChecking.Monad.Signature
    import Agda.TypeChecking.Substitute

    import Agda.Utils.Functor
    import Agda.Utils.Impossible
    import Agda.Utils.Maybe
    import Agda.Utils.Pretty ( prettyShow )

    -- Type combinators

    infixr 4 -->
    infixr 4 .-->
    infixr 4 ..-->

    (-->), (.-->), (..-->) :: Applicative m => m Type -> m Type -> m Type
    m Type
    a --> :: forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> m Type
    b = (Relevance -> Relevance) -> m Type -> m Type -> m Type
    forall (m :: * -> *).
    Applicative m =>
    (Relevance -> Relevance) -> m Type -> m Type -> m Type
    garr Relevance -> Relevance
    forall a. a -> a
    id m Type
    a m Type
    b
    m Type
    a .--> :: forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    .--> m Type
    b = (Relevance -> Relevance) -> m Type -> m Type -> m Type
    forall (m :: * -> *).
    Applicative m =>
    (Relevance -> Relevance) -> m Type -> m Type -> m Type
    garr (Relevance -> Relevance -> Relevance
    forall a b. a -> b -> a
    const (Relevance -> Relevance -> Relevance)
    -> Relevance -> Relevance -> Relevance
    forall a b. (a -> b) -> a -> b
    $ Relevance
    Irrelevant) m Type
    a m Type
    b
    m Type
    a ..--> :: forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    ..--> m Type
    b = (Relevance -> Relevance) -> m Type -> m Type -> m Type
    forall (m :: * -> *).
    Applicative m =>
    (Relevance -> Relevance) -> m Type -> m Type -> m Type
    garr (Relevance -> Relevance -> Relevance
    forall a b. a -> b -> a
    const (Relevance -> Relevance -> Relevance)
    -> Relevance -> Relevance -> Relevance
    forall a b. (a -> b) -> a -> b
    $ Relevance
    NonStrict) m Type
    a m Type
    b

    garr :: Applicative m => (Relevance -> Relevance) -> m Type -> m Type -> m Type
    garr :: forall (m :: * -> *).
    Applicative m =>
    (Relevance -> Relevance) -> m Type -> m Type -> m Type
    garr Relevance -> Relevance
    f m Type
    a m Type
    b = do
      Type
    a' <- m Type
    a
      Type
    b' <- m Type
    b
      pure $ Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Sort' Term -> Sort' Term -> Sort' Term
    funSort (Type -> Sort' Term
    forall a. LensSort a => a -> Sort' Term
    getSort Type
    a') (Type -> Sort' Term
    forall a. LensSort a => a -> Sort' Term
    getSort Type
    b')) (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $
        Dom Type -> Abs Type -> Term
    Pi ((Relevance -> Relevance) -> Dom Type -> Dom Type
    forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
    mapRelevance Relevance -> Relevance
    f (Dom Type -> Dom Type) -> Dom Type -> Dom Type
    forall a b. (a -> b) -> a -> b
    $ Type -> Dom Type
    forall a. a -> Dom a
    defaultDom Type
    a') (String -> Type -> Abs Type
    forall a. String -> a -> Abs a
    NoAbs String
    "_" Type
    b')

    gpi :: (MonadAddContext m, MonadDebug m)
        => ArgInfo -> String -> m Type -> m Type -> m Type
    gpi :: forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgInfo -> String -> m Type -> m Type -> m Type
    gpi ArgInfo
    info String
    name m Type
    a m Type
    b = do
      Type
    a <- m Type
    a
      let dom :: Dom Type
          dom :: Dom Type
    dom = ArgInfo -> String -> Type -> Dom Type
    forall a. ArgInfo -> String -> a -> Dom a
    defaultNamedArgDom ArgInfo
    info String
    name Type
    a
      Type
    b <- (String, Dom Type) -> m Type -> m Type
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (String
    name, Dom Type
    dom) m Type
    b
      let y :: String
    y = String -> String
    stringToArgName String
    name
      Type -> m Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> m Type) -> Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Dom Type -> Abs Type -> Sort' Term
    mkPiSort Dom Type
    dom (String -> Type -> Abs Type
    forall a. String -> a -> Abs a
    Abs String
    y Type
    b))
                  (Dom Type -> Abs Type -> Term
    Pi Dom Type
    dom (String -> Type -> Abs Type
    forall a. String -> a -> Abs a
    Abs String
    y Type
    b))

    hPi, nPi :: (MonadAddContext m, MonadDebug m)
             => String -> m Type -> m Type -> m Type
    hPi :: forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String -> m Type -> m Type -> m Type
    hPi = ArgInfo -> String -> m Type -> m Type -> m Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgInfo -> String -> m Type -> m Type -> m Type
    gpi (ArgInfo -> String -> m Type -> m Type -> m Type)
    -> ArgInfo -> String -> m Type -> m Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ Hiding -> ArgInfo -> ArgInfo
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    Hidden ArgInfo
    defaultArgInfo
    nPi :: forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String -> m Type -> m Type -> m Type
    nPi = ArgInfo -> String -> m Type -> m Type -> m Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgInfo -> String -> m Type -> m Type -> m Type
    gpi ArgInfo
    defaultArgInfo

    hPi', nPi' :: (MonadFail m, MonadAddContext m, MonadDebug m)
               => String -> NamesT m Type -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
    hPi' :: forall (m :: * -> *).
    (MonadFail m, MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    s NamesT m Type
    a NamesT m Term -> NamesT m Type
    b = String -> NamesT m Type -> NamesT m Type -> NamesT m Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String -> m Type -> m Type -> m Type
    hPi String
    s NamesT m Type
    a (String -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
    forall (m :: * -> *) b a.
    (MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
    String -> (NamesT m b -> NamesT m a) -> NamesT m a
    bind' String
    s NamesT m Term -> NamesT m Type
    b)
    nPi' :: forall (m :: * -> *).
    (MonadFail m, MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    nPi' String
    s NamesT m Type
    a NamesT m Term -> NamesT m Type
    b = String -> NamesT m Type -> NamesT m Type -> NamesT m Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String -> m Type -> m Type -> m Type
    nPi String
    s NamesT m Type
    a (String -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
    forall (m :: * -> *) b a.
    (MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
    String -> (NamesT m b -> NamesT m a) -> NamesT m a
    bind' String
    s NamesT m Term -> NamesT m Type
    b)

    pPi' :: (MonadAddContext m, HasBuiltins m, MonadDebug m)
         => String -> NamesT m Term -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
    pPi' :: forall (m :: * -> *).
    (MonadAddContext m, HasBuiltins m, MonadDebug m) =>
    String
    -> NamesT m Term
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    pPi' String
    n NamesT m Term
    phi NamesT m Term -> NamesT m Type
    b = Type -> Type
    toFinitePi (Type -> Type) -> NamesT m Type -> NamesT m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    forall (m :: * -> *).
    (MonadFail m, MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    nPi' String
    n (NamesT m Term -> NamesT m Type
    forall (m :: * -> *). Functor m => m Term -> m Type
    elSSet (NamesT m Term -> NamesT m Type) -> NamesT m Term -> NamesT m Type
    forall a b. (a -> b) -> a -> b
    $ m Term -> NamesT m Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl m Term
    isOne NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    phi) NamesT m Term -> NamesT m Type
    b
     where
       toFinitePi :: Type -> Type
       toFinitePi :: Type -> Type
    toFinitePi (El Sort' Term
    s (Pi Dom Type
    d Abs Type
    b)) = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    s (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Abs Type -> Term
    Pi (Relevance -> Dom Type -> Dom Type
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    Irrelevant (Dom Type -> Dom Type) -> Dom Type -> Dom Type
    forall a b. (a -> b) -> a -> b
    $ Dom Type
    d { domFinite :: Bool
    domFinite = Bool
    True }) Abs Type
    b
       toFinitePi Type
    _               = Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__

       isOne :: m Term
    isOne = Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    builtinIsOne

    el' :: Applicative m => m Term -> m Term -> m Type
    el' :: forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el' m Term
    l m Term
    a = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Sort' Term -> Term -> Type) -> m (Sort' Term) -> m (Term -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> Sort' Term
    tmSort (Term -> Sort' Term) -> m Term -> m (Sort' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Term
    l) m (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m Term
    a

    el's :: Applicative m => m Term -> m Term -> m Type
    el's :: forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el's m Term
    l m Term
    a = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Sort' Term -> Term -> Type) -> m (Sort' Term) -> m (Term -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Level' Term -> Sort' Term
    forall t. Level' t -> Sort' t
    SSet (Level' Term -> Sort' Term)
    -> (Term -> Level' Term) -> Term -> Sort' Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Level' Term
    forall t. t -> Level' t
    atomicLevel (Term -> Sort' Term) -> m Term -> m (Sort' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Term
    l) m (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m Term
    a

    elInf :: Functor m => m Term -> m Type
    elInf :: forall (m :: * -> *). Functor m => m Term -> m Type
    elInf m Term
    t = (Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (IsFibrant -> Integer -> Sort' Term
    forall t. IsFibrant -> Integer -> Sort' t
    Inf IsFibrant
    IsFibrant Integer
    0) (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Term
    t)

    elSSet :: Functor m => m Term -> m Type
    elSSet :: forall (m :: * -> *). Functor m => m Term -> m Type
    elSSet m Term
    t = (Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Level' Term -> Sort' Term
    forall t. Level' t -> Sort' t
    SSet (Level' Term -> Sort' Term) -> Level' Term -> Sort' Term
    forall a b. (a -> b) -> a -> b
    $ Integer -> Level' Term
    ClosedLevel Integer
    0) (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Term
    t)

    nolam :: Term -> Term
    nolam :: Term -> Term
    nolam = ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    defaultArgInfo (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Term -> Abs Term
    forall a. String -> a -> Abs a
    NoAbs String
    "_"

    varM :: Applicative m => Int -> m Term
    varM :: forall (m :: * -> *). Applicative m => Int -> m Term
    varM = Term -> m Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> m Term) -> (Int -> Term) -> Int -> m Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Term
    var

    infixl 9 <@>, <#>

    gApply :: Applicative m => Hiding -> m Term -> m Term -> m Term
    gApply :: forall (m :: * -> *).
    Applicative m =>
    Hiding -> m Term -> m Term -> m Term
    gApply Hiding
    h m Term
    a m Term
    b = ArgInfo -> m Term -> m Term -> m Term
    forall (m :: * -> *).
    Applicative m =>
    ArgInfo -> m Term -> m Term -> m Term
    gApply' (Hiding -> ArgInfo -> ArgInfo
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    h ArgInfo
    defaultArgInfo) m Term
    a m Term
    b

    gApply' :: Applicative m => ArgInfo -> m Term -> m Term -> m Term
    gApply' :: forall (m :: * -> *).
    Applicative m =>
    ArgInfo -> m Term -> m Term -> m Term
    gApply' ArgInfo
    info m Term
    a m Term
    b = do
        Term
    x <- m Term
    a
        Term
    y <- m Term
    b
        pure $ Term
    x Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info Term
    y]

    (<@>),(<#>),(<..>) :: Applicative m => m Term -> m Term -> m Term
    <@> :: forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    (<@>) = Hiding -> m Term -> m Term -> m Term
    forall (m :: * -> *).
    Applicative m =>
    Hiding -> m Term -> m Term -> m Term
    gApply Hiding
    NotHidden
    <#> :: forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    (<#>) = Hiding -> m Term -> m Term -> m Term
    forall (m :: * -> *).
    Applicative m =>
    Hiding -> m Term -> m Term -> m Term
    gApply Hiding
    Hidden
    <..> :: forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    (<..>) = ArgInfo -> m Term -> m Term -> m Term
    forall (m :: * -> *).
    Applicative m =>
    ArgInfo -> m Term -> m Term -> m Term
    gApply' (Relevance -> ArgInfo -> ArgInfo
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    Irrelevant ArgInfo
    defaultArgInfo)

    (<@@>) :: Applicative m => m Term -> (m Term,m Term,m Term) -> m Term
    m Term
    t <@@> :: forall (m :: * -> *).
    Applicative m =>
    m Term -> (m Term, m Term, m Term) -> m Term
    <@@> (m Term
    x,m Term
    y,m Term
    r) = do
      Term
    t <- m Term
    t
      Term
    x <- m Term
    x
      Term
    y <- m Term
    y
      Term
    r <- m Term
    r
      pure $ Term
    t Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [Term -> Term -> Term -> Elim' Term
    forall a. a -> a -> a -> Elim' a
    IApply Term
    x Term
    y Term
    r]

    list :: TCM Term -> TCM Term
    list :: TCM Term -> TCM Term
    list TCM Term
    t = TCM Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primList TCM Term -> TCM Term -> TCM Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> TCM Term
    t

    tMaybe :: TCM Term -> TCM Term
    tMaybe :: TCM Term -> TCM Term
    tMaybe TCM Term
    t = TCM Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primMaybe TCM Term -> TCM Term -> TCM Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> TCM Term
    t

    io :: TCM Term -> TCM Term
    io :: TCM Term -> TCM Term
    io TCM Term
    t = TCM Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIO TCM Term -> TCM Term -> TCM Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> TCM Term
    t

    path :: TCM Term -> TCM Term
    path :: TCM Term -> TCM Term
    path TCM Term
    t = TCM Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primPath TCM Term -> TCM Term -> TCM Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> TCM Term
    t

    el :: Functor m => m Term -> m Type
    el :: forall (m :: * -> *). Functor m => m Term -> m Type
    el m Term
    t = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Integer -> Sort' Term
    mkType Integer
    0) (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Term
    t

    tset :: Applicative m => m Type
    tset :: forall (m :: * -> *). Applicative m => m Type
    tset = Type -> m Type
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Type -> m Type) -> Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ Sort' Term -> Type
    sort (Integer -> Sort' Term
    mkType Integer
    0)

    sSizeUniv :: Sort
    -- sSizeUniv = mkType 0
    -- Andreas, 2016-04-14 switching off SizeUniv, unfixing issue #1428
    sSizeUniv :: Sort' Term
    sSizeUniv = Sort' Term
    forall t. Sort' t
    SizeUniv

    tSizeUniv :: Applicative m => m Type
    -- tSizeUniv = tset
    -- Andreas, 2016-04-14 switching off SizeUniv, unfixing issue #1428
    -- tSizeUniv = return $ El sSizeUniv $ Sort sSizeUniv
    -- Andreas, 2015-03-16 Since equality checking for types
    -- includes equality checking for sorts, we cannot put
    -- SizeUniv in Setω.  (SizeUniv : Setω) == (_0 : suc _0)
    -- will first instantiate _0 := Setω, which is wrong.
    tSizeUniv :: forall (m :: * -> *). Applicative m => m Type
    tSizeUniv = Type -> m Type
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Type -> m Type) -> Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ Sort' Term -> Type
    sort Sort' Term
    sSizeUniv

    -- | Abbreviation: @argN = 'Arg' 'defaultArgInfo'@.
    argN :: e -> Arg e
    argN :: forall e. e -> Arg e
    argN = ArgInfo -> e -> Arg e
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    defaultArgInfo

    domN :: e -> Dom e
    domN :: forall a. a -> Dom a
    domN = e -> Dom e
    forall a. a -> Dom a
    defaultDom

    -- | Abbreviation: @argH = 'hide' 'Arg' 'defaultArgInfo'@.
    argH :: e -> Arg e
    argH :: forall e. e -> Arg e
    argH = ArgInfo -> e -> Arg e
    forall e. ArgInfo -> e -> Arg e
    Arg (ArgInfo -> e -> Arg e) -> ArgInfo -> e -> Arg e
    forall a b. (a -> b) -> a -> b
    $ Hiding -> ArgInfo -> ArgInfo
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    Hidden ArgInfo
    defaultArgInfo

    domH :: e -> Dom e
    domH :: forall a. a -> Dom a
    domH = Hiding -> Dom e -> Dom e
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    Hidden (Dom e -> Dom e) -> (e -> Dom e) -> e -> Dom e
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . e -> Dom e
    forall a. a -> Dom a
    defaultDom

    ---------------------------------------------------------------------------
    -- * Accessing the primitive functions
    ---------------------------------------------------------------------------

    lookupPrimitiveFunction :: String -> TCM PrimitiveImpl
    lookupPrimitiveFunction :: String -> TCM PrimitiveImpl
    lookupPrimitiveFunction String
    x =
      TCM PrimitiveImpl -> Maybe (TCM PrimitiveImpl) -> TCM PrimitiveImpl
    forall a. a -> Maybe a -> a
    fromMaybe (do
                    String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.prim" Int
    20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Lookup of primitive function" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "failed"
                    TypeError -> TCM PrimitiveImpl
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM PrimitiveImpl) -> TypeError -> TCM PrimitiveImpl
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    NoSuchPrimitiveFunction String
    x)
                (String
    -> Map String (TCM PrimitiveImpl) -> Maybe (TCM PrimitiveImpl)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup String
    x Map String (TCM PrimitiveImpl)
    primitiveFunctions)

    lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl)
    lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl)
    lookupPrimitiveFunctionQ QName
    q = do
      let s :: String
    s = Name -> String
    forall a. Pretty a => a -> String
    prettyShow (Name -> Name
    nameCanonical (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    q)
      PrimImpl Type
    t PrimFun
    pf <- String -> TCM PrimitiveImpl
    lookupPrimitiveFunction String
    s
      (String, PrimitiveImpl) -> TCM (String, PrimitiveImpl)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String
    s, Type -> PrimFun -> PrimitiveImpl
    PrimImpl Type
    t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
    forall a b. (a -> b) -> a -> b
    $ PrimFun
    pf { primFunName :: QName
    primFunName = QName
    q })

    getBuiltinName :: (HasBuiltins m, MonadReduce m) => String -> m (Maybe QName)
    getBuiltinName :: forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    String -> m (Maybe QName)
    getBuiltinName String
    b = do
      m (Maybe Term)
    -> m (Maybe QName) -> (Term -> m (Maybe QName)) -> m (Maybe QName)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    b) (Maybe QName -> m (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe QName
    forall a. Maybe a
    Nothing) (QName -> Maybe QName
    forall a. a -> Maybe a
    Just (QName -> Maybe QName)
    -> (Term -> m QName) -> Term -> m (Maybe QName)
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> Term -> m QName
    forall {m :: * -> *}. MonadReduce m => Term -> m QName
    getName)
      where
      getName :: Term -> m QName
    getName Term
    v = do
        Term
    v <- Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v
        case Term -> Term
    unSpine (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Term
    v of
          Def QName
    x Elims
    _   -> QName -> m QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    x
          Con ConHead
    x ConInfo
    _ Elims
    _ -> QName -> m QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName -> m QName) -> QName -> m QName
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    x
          Lam ArgInfo
    _ Abs Term
    b   -> Term -> m QName
    getName (Term -> m QName) -> Term -> m QName
    forall a b. (a -> b) -> a -> b
    $ Abs Term -> Term
    forall a. Abs a -> a
    unAbs Abs Term
    b
          Term
    _ -> m QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    isBuiltin :: (HasBuiltins m, MonadReduce m) => QName -> String -> m Bool
    isBuiltin :: forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    QName -> String -> m Bool
    isBuiltin QName
    q String
    b = (QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Maybe QName -> Bool) -> m (Maybe QName) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    String -> m (Maybe QName)
    getBuiltinName String
    b

    ------------------------------------------------------------------------
    -- * Builtin Sigma
    ------------------------------------------------------------------------

    data SigmaKit = SigmaKit
      { SigmaKit -> QName
    sigmaName :: QName
      , SigmaKit -> ConHead
    sigmaCon  :: ConHead
      , SigmaKit -> QName
    sigmaFst  :: QName
      , SigmaKit -> QName
    sigmaSnd  :: QName
      }
      deriving (SigmaKit -> SigmaKit -> Bool
    (SigmaKit -> SigmaKit -> Bool)
    -> (SigmaKit -> SigmaKit -> Bool) -> Eq SigmaKit
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: SigmaKit -> SigmaKit -> Bool
    $c/= :: SigmaKit -> SigmaKit -> Bool
    == :: SigmaKit -> SigmaKit -> Bool
    $c== :: SigmaKit -> SigmaKit -> Bool
    Eq,Int -> SigmaKit -> String -> String
    [SigmaKit] -> String -> String
    SigmaKit -> String
    (Int -> SigmaKit -> String -> String)
    -> (SigmaKit -> String)
    -> ([SigmaKit] -> String -> String)
    -> Show SigmaKit
    forall a.
    (Int -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    showList :: [SigmaKit] -> String -> String
    $cshowList :: [SigmaKit] -> String -> String
    show :: SigmaKit -> String
    $cshow :: SigmaKit -> String
    showsPrec :: Int -> SigmaKit -> String -> String
    $cshowsPrec :: Int -> SigmaKit -> String -> String
    Show)

    getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit)
    getSigmaKit :: forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m) =>
    m (Maybe SigmaKit)
    getSigmaKit = do
      Maybe QName
    ms <- String -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
    getBuiltinName' String
    builtinSigma
      case Maybe QName
    ms of
        Maybe QName
    Nothing -> Maybe SigmaKit -> m (Maybe SigmaKit)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe SigmaKit
    forall a. Maybe a
    Nothing
        Just QName
    sigma -> 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
    sigma
          case Defn
    def of
            Record { recFields :: Defn -> [Dom QName]
    recFields = [Dom QName
    fst,Dom QName
    snd], recConHead :: Defn -> ConHead
    recConHead = ConHead
    con } -> do
              Maybe SigmaKit -> m (Maybe SigmaKit)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe SigmaKit -> m (Maybe SigmaKit))
    -> (SigmaKit -> Maybe SigmaKit) -> SigmaKit -> m (Maybe SigmaKit)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SigmaKit -> Maybe SigmaKit
    forall a. a -> Maybe a
    Just (SigmaKit -> m (Maybe SigmaKit)) -> SigmaKit -> m (Maybe SigmaKit)
    forall a b. (a -> b) -> a -> b
    $ SigmaKit :: QName -> ConHead -> QName -> QName -> SigmaKit
    SigmaKit
                { sigmaName :: QName
    sigmaName = QName
    sigma
                , sigmaCon :: ConHead
    sigmaCon  = ConHead
    con
                , sigmaFst :: QName
    sigmaFst  = Dom QName -> QName
    forall t e. Dom' t e -> e
    unDom Dom QName
    fst
                , sigmaSnd :: QName
    sigmaSnd  = Dom QName -> QName
    forall t e. Dom' t e -> e
    unDom Dom QName
    snd
                }
            Defn
    _ -> m (Maybe SigmaKit)
    forall a. HasCallStack => a
    __IMPOSSIBLE__