    {-# LANGUAGE ApplicativeDo #-}

    module Agda.TypeChecking.Primitive.Base where

    import Control.Monad             ( mzero )
    import Control.Monad.Trans.Maybe ( MaybeT(..), runMaybeT )

    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.Syntax.Common.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
    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
    shapeIrrelevant) 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') (ArgName -> Type -> Abs Type
    forall a. ArgName -> a -> Abs a
    NoAbs ArgName
    "_" Type
    b')

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

    hPi, nPi :: (MonadAddContext m, MonadDebug m)
             => String -> m Type -> m Type -> m Type
    hPi :: forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    hPi = ArgInfo -> ArgName -> m Type -> m Type -> m Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgInfo -> ArgName -> m Type -> m Type -> m Type
    gpi (ArgInfo -> ArgName -> m Type -> m Type -> m Type)
    -> ArgInfo -> ArgName -> 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) =>
    ArgName -> m Type -> m Type -> m Type
    nPi = ArgInfo -> ArgName -> m Type -> m Type -> m Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgInfo -> ArgName -> m Type -> m Type -> m Type
    gpi ArgInfo
    defaultArgInfo

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

    {-# INLINABLE pPi' #-}
    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) =>
    ArgName
    -> NamesT m Term
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    pPi' ArgName
    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
    <$> ArgName
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    nPi' ArgName
    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
       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
    <$> BuiltinId -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinIsOne

    -- | Turn a 'Pi' type into one whose domain is annotated finite, i.e.,
    -- one that represents a @Partial@ element rather than an actual
    -- function.
    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
    d{ domIsFinite = True })
      Abs Type
    b
    toFinitePi Type
    _ = Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    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 a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m Term
    a

    els :: Applicative m => m Sort -> m Term -> m Type
    els :: forall (m :: * -> *).
    Applicative m =>
    m (Sort' Term) -> m Term -> m Type
    els m (Sort' 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
    <$> m (Sort' Term)
    l m (Term -> Type) -> m Term -> m Type
    forall a b. m (a -> b) -> m a -> m b
    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 a b. m (a -> b) -> m a -> m b
    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 (Univ -> Integer -> Sort' Term
    forall t. Univ -> Integer -> Sort' t
    Inf Univ
    UType 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
    . ArgName -> Term -> Abs Term
    forall a. ArgName -> a -> Abs a
    NoAbs ArgName
    "_"

    varM :: Applicative m => Int -> m Term
    varM :: forall (m :: * -> *). Applicative m => Int -> m Term
    varM = Term -> m Term
    forall a. a -> m a
    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' ArgInfo
    defaultIrrelevantArgInfo

    (<@@>) :: 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

    -- | The universe @Set0@ as a type.
    tset :: Applicative m => m Type
    tset :: forall (m :: * -> *). Applicative m => m Type
    tset = Type -> m Type
    forall a. a -> m a
    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)

    -- | @SizeUniv@ as a sort.
    sSizeUniv :: Sort
    sSizeUniv :: Sort' Term
    sSizeUniv = Sort' Term
    forall t. Sort' t
    SizeUniv

    -- | @SizeUniv@ as a type.
    tSizeUniv :: Applicative m => m Type
    tSizeUniv :: forall (m :: * -> *). Applicative m => m Type
    tSizeUniv = Type -> m Type
    forall a. a -> m a
    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

    tLevelUniv :: Applicative m => m Type
    tLevelUniv :: forall (m :: * -> *). Applicative m => m Type
    tLevelUniv = Type -> m Type
    forall a. a -> m a
    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 -> Type) -> Sort' Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Sort' Term
    forall t. Sort' t
    LevelUniv

    -- | 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 :: PrimitiveId -> TCM PrimitiveImpl
    lookupPrimitiveFunction :: PrimitiveId -> TCM PrimitiveImpl
    lookupPrimitiveFunction PrimitiveId
    x =
      TCM PrimitiveImpl -> Maybe (TCM PrimitiveImpl) -> TCM PrimitiveImpl
    forall a. a -> Maybe a -> a
    fromMaybe (do
                    ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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
    <+> PrimitiveId -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty PrimitiveId
    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
    $ ArgName -> TypeError
    NoSuchPrimitiveFunction (PrimitiveId -> ArgName
    forall a. IsBuiltin a => a -> ArgName
    getBuiltinId PrimitiveId
    x))
                (PrimitiveId
    -> Map PrimitiveId (TCM PrimitiveImpl) -> Maybe (TCM PrimitiveImpl)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup PrimitiveId
    x Map PrimitiveId (TCM PrimitiveImpl)
    primitiveFunctions)

    lookupPrimitiveFunctionQ :: QName -> TCM (PrimitiveId, PrimitiveImpl)
    lookupPrimitiveFunctionQ :: QName -> TCM (PrimitiveId, PrimitiveImpl)
    lookupPrimitiveFunctionQ QName
    q = do
      let s :: ArgName
    s = Name -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow (Name -> Name
    nameCanonical (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    q)
      case ArgName -> Maybe PrimitiveId
    primitiveById ArgName
    s of
        Maybe PrimitiveId
    Nothing -> TypeError -> TCM (PrimitiveId, PrimitiveImpl)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM (PrimitiveId, PrimitiveImpl))
    -> TypeError -> TCM (PrimitiveId, PrimitiveImpl)
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TypeError
    NoSuchPrimitiveFunction ArgName
    s
        Just PrimitiveId
    s -> do
          PrimImpl Type
    t PrimFun
    pf <- PrimitiveId -> TCM PrimitiveImpl
    lookupPrimitiveFunction PrimitiveId
    s
          (PrimitiveId, PrimitiveImpl) -> TCM (PrimitiveId, PrimitiveImpl)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PrimitiveId
    s, Type -> PrimFun -> PrimitiveImpl
    PrimImpl Type
    t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
    forall a b. (a -> b) -> a -> b
    $ PrimFun
    pf { primFunName = q })

    getBuiltinName :: (HasBuiltins m, MonadReduce m) => BuiltinId -> m (Maybe QName)
    getBuiltinName :: forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    BuiltinId -> m (Maybe QName)
    getBuiltinName BuiltinId
    b = MaybeT m QName -> m (Maybe QName)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT m QName -> m (Maybe QName))
    -> MaybeT m QName -> m (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ Term -> MaybeT m QName
    forall (m :: * -> *). MonadReduce m => Term -> MaybeT m QName
    getQNameFromTerm (Term -> MaybeT m QName) -> MaybeT m Term -> MaybeT m QName
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m (Maybe Term) -> MaybeT m Term
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (BuiltinId -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    b)

    -- | Convert a name in 'Term' form back to 'QName'.
    --
    getQNameFromTerm :: MonadReduce m => Term -> MaybeT m QName
    getQNameFromTerm :: forall (m :: * -> *). MonadReduce m => Term -> MaybeT m QName
    getQNameFromTerm Term
    v = do
        Term
    v <- Term -> MaybeT m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v
        case Term -> Term
    unSpine Term
    v of
          Def QName
    x Elims
    _   -> QName -> MaybeT m QName
    forall a. a -> MaybeT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    x
          Con ConHead
    x ConInfo
    _ Elims
    _ -> QName -> MaybeT m QName
    forall a. a -> MaybeT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName -> MaybeT m QName) -> QName -> MaybeT m QName
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    x
          Lam ArgInfo
    _ Abs Term
    b   -> Term -> MaybeT m QName
    forall (m :: * -> *). MonadReduce m => Term -> MaybeT m QName
    getQNameFromTerm (Term -> MaybeT m QName) -> Term -> MaybeT m QName
    forall a b. (a -> b) -> a -> b
    $ Abs Term -> Term
    forall a. Abs a -> a
    unAbs Abs Term
    b
          Term
    _ -> MaybeT m QName
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    isBuiltin :: (HasBuiltins m, MonadReduce m) => QName -> BuiltinId -> m Bool
    isBuiltin :: forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    QName -> BuiltinId -> m Bool
    isBuiltin QName
    q BuiltinId
    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
    <$> BuiltinId -> m (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    BuiltinId -> m (Maybe QName)
    getBuiltinName BuiltinId
    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
    $c== :: SigmaKit -> SigmaKit -> Bool
    == :: SigmaKit -> SigmaKit -> Bool
    $c/= :: SigmaKit -> SigmaKit -> Bool
    /= :: SigmaKit -> SigmaKit -> Bool
    Eq,Int -> SigmaKit -> ArgName -> ArgName
    [SigmaKit] -> ArgName -> ArgName
    SigmaKit -> ArgName
    (Int -> SigmaKit -> ArgName -> ArgName)
    -> (SigmaKit -> ArgName)
    -> ([SigmaKit] -> ArgName -> ArgName)
    -> Show SigmaKit
    forall a.
    (Int -> a -> ArgName -> ArgName)
    -> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
    $cshowsPrec :: Int -> SigmaKit -> ArgName -> ArgName
    showsPrec :: Int -> SigmaKit -> ArgName -> ArgName
    $cshow :: SigmaKit -> ArgName
    show :: SigmaKit -> ArgName
    $cshowList :: [SigmaKit] -> ArgName -> ArgName
    showList :: [SigmaKit] -> ArgName -> ArgName
    Show)

    getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit)
    getSigmaKit :: forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m) =>
    m (Maybe SigmaKit)
    getSigmaKit = do
      Maybe QName
    ms <- BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinSigma
      case Maybe QName
    ms of
        Maybe QName
    Nothing -> Maybe SigmaKit -> m (Maybe SigmaKit)
    forall a. a -> m a
    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 a. a -> m a
    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
                { 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__  -- This invariant is ensured in bindBuiltinSigma