{-# OPTIONS_GHC -Wunused-imports #-}

-- | This module implements the rules for type-checking the side
-- conditions imposed on the "constrained" cubical primitives (Kan
-- operations, constructors for glue/hcomp{U}, Partial disjunction).
module Mikan.TypeChecking.Rules.Cubical
  ( cubicalPrimChecks
  , isConstrainedPrimitive
  )
  where

import Prelude hiding ( null )

import Data.Map.Strict qualified as Map

import Mikan.Syntax.Concrete.Pretty () -- only Pretty instances
import Mikan.Syntax.Common
import Mikan.Syntax.Internal as I
import Mikan.Syntax.Position

import {-# SOURCE #-} Mikan.TypeChecking.Rules.Application
import Mikan.TypeChecking.Conversion
import Mikan.TypeChecking.MetaVars
import Mikan.TypeChecking.Names
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Primitive hiding (Nat)
import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Substitute

import Mikan.Utils.Functor
import Mikan.Utils.List hiding (Suffix)

import Mikan.Utils.Impossible

-- helper pattern synonym for consing an Apply elim, since the functions
-- in this module all only care about taking apart and putting back
-- together a prefix of Apply eliminations; /but/ they may encounter
-- @Proj@s in the unexplored part of the spine, so we can't use
-- 'allApplyElims' or any of its friends.
pattern (:@) :: Arg a -> [Elim' a] -> [Elim' a]
pattern x $b:@ :: forall a. Arg a -> [Elim' a] -> [Elim' a]
$m:@ :: forall {r} {a}.
[Elim' a] -> (Arg a -> [Elim' a] -> r) -> ((# #) -> r) -> r
:@ xs = Apply x:xs
infixr 5 :@

-- | Map associating the identifier of a cubical primitive to a function
-- which checks its argument spine.
--
-- The continuation receives the QName through which the primitive
-- function was applied to generate proper error messages in case of
-- e.g. renaming.
cubicalPrimChecks :: Map.Map PrimitiveId (QName -> ArgsCheck)
cubicalPrimChecks :: Map PrimitiveId (QName -> ArgsCheck)
cubicalPrimChecks = [(PrimitiveId, QName -> ArgsCheck)]
-> Map PrimitiveId (QName -> ArgsCheck)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
  [ (PrimitiveId
builtinPOr,    QName -> ArgsCheck
checkPrimPOr)
  , (PrimitiveId
builtinComp,   QName -> ArgsCheck
checkPrimComp)
  , (PrimitiveId
builtinHComp,  QName -> ArgsCheck
checkPrimHComp)
  , (PrimitiveId
builtinTrans,  QName -> ArgsCheck
checkPrimTrans)
  , (PrimitiveId
builtin_glue,  QName -> ArgsCheck
checkPrimGlue)
  , (PrimitiveId
builtin_glueU, QName -> ArgsCheck
checkPrimGlueU)
  ]

-- | Check whether the given name (which must be defined) corresponds to
-- a cubical primitive with constraints on its argument spine and, if
-- so, return the function to check them.
isConstrainedPrimitive :: QName -> TCM (Maybe ArgsCheck)
isConstrainedPrimitive :: QName -> TCM (Maybe ArgsCheck)
isConstrainedPrimitive QName
def = TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
def) TCMT IO Definition -> (Definition -> Defn) -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Definition -> Defn
theDef TCMT IO Defn
-> (Defn -> TCM (Maybe ArgsCheck)) -> TCM (Maybe ArgsCheck)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Primitive{primName :: Defn -> PrimitiveId
primName = PrimitiveId
id}
    | Just QName -> ArgsCheck
chk <- PrimitiveId
-> Map PrimitiveId (QName -> ArgsCheck)
-> Maybe (QName -> ArgsCheck)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PrimitiveId
id Map PrimitiveId (QName -> ArgsCheck)
cubicalPrimChecks -> Maybe ArgsCheck -> TCM (Maybe ArgsCheck)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe ArgsCheck -> TCM (Maybe ArgsCheck))
-> Maybe ArgsCheck -> TCM (Maybe ArgsCheck)
forall a b. (a -> b) -> a -> b
$ ArgsCheck -> Maybe ArgsCheck
forall a. a -> Maybe a
Just (QName -> ArgsCheck
chk QName
def)
  Defn
_ -> Maybe ArgsCheck -> TCM (Maybe ArgsCheck)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ArgsCheck
forall a. Maybe a
Nothing

-- | "pathAbs (PathView s _ l a x y) t" builds "(\ t) : pv"
--   Preconditions: PathView is PathType, and t[i0] = x, t[i1] = y
pathAbs :: PathView -> Abs Term -> TCM Term
pathAbs :: PathView -> Abs Term -> TCM Term
pathAbs (OType Type
_) Abs Term
t = TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
pathAbs (PathType Sort
s QName
path Arg Term
l Arg Term
a Arg Term
x Arg Term
y) Abs Term
t = do
  Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo Abs Term
t

-- | @primComp : ∀ {ℓ} (A : (i : I) → Type (ℓ i)) (φ : I) (u : ∀ i → Partial φ (A i)) (a : A i0) → A i1@
--
--   Check:  @u i0 = (λ _ → a) : Partial φ (A i0)@.
--
checkPrimComp :: QName -> ArgsCheck
checkPrimComp :: QName -> ArgsCheck
checkPrimComp QName
c ArgRanges
rs Elims
vs Type
_ = case Elims
vs of
  Arg Term
l :@ Arg Term
a :@ Arg Term
phi :@ Arg Term
u :@ Arg Term
a0 :@ Elims
rest -> do
    iz <- ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo (Term -> Arg Term) -> TCM Term -> TCMT IO (Arg Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntervalView -> TCM Term
forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
IZero
    let lz = Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
l Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [Arg Term
iz]
        az = Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [Arg Term
iz]

    ty <- el's (pure (unArg l `apply` [iz])) $ primPartial
      <#> pure (unArg l `apply` [iz])
      <@> pure (unArg phi)
      <@> pure (unArg a `apply` [iz])

    bAz <- el' (pure $ lz) (pure $ az)
    a0 <- blockArg bAz (rs !!! 4) a0 $ equalTerm ty
      (Lam defaultArgInfo $ NoAbs "_" $ unArg a0)
      (apply (unArg u) [iz])

    return $ l :@ a :@ phi :@ u :@ a0 :@ rest
  Elims
_ -> TypeError -> TCM Elims
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM Elims) -> TypeError -> TCM Elims
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
CubicalPrimitiveNotFullyApplied QName
c

-- | @primHComp : ∀ {ℓ} {A : Type ℓ} {φ : I} (u : ∀ i → Partial φ A) (a : A) → A@
--
--   Check:  @u i0 = (λ _ → a) : Partial φ A@.
--
checkPrimHComp :: QName -> ArgsCheck
checkPrimHComp :: QName -> ArgsCheck
checkPrimHComp QName
c ArgRanges
rs Elims
vs Type
_ = case Elims
vs of
  Arg Term
l :@ Arg Term
a :@ Arg Term
phi :@ Arg Term
u :@ Arg Term
a0 :@ Elims
rest -> do
    -- iz = i0
    iz <- ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo (Term -> Arg Term) -> TCM Term -> TCMT IO (Arg Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntervalView -> TCM Term
forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
IZero
    -- ty = Partial φ A
    ty <- el's (pure (unArg l)) $ primPartial
      <#> pure (unArg l)
      <@> pure (unArg phi)
      <@> pure (unArg a)

    -- (λ _ → a) = u i0 : ty
    bA <- el' (pure $ unArg l) (pure $ unArg a)
    a0 <- blockArg bA (rs !!! 4) a0 $ equalTerm ty
      (Lam defaultArgInfo $ NoAbs "_" $ unArg a0)
      (apply (unArg u) [iz])

    return $ l :@ a :@ phi :@ u :@ a0 :@ rest
  Elims
_ -> TypeError -> TCM Elims
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM Elims) -> TypeError -> TCM Elims
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
CubicalPrimitiveNotFullyApplied QName
c

-- | @transp : ∀{ℓ} (A : (i : I) → Type (ℓ i)) (φ : I) (a0 : A i0) → A i1@
--
--   Check:  If φ, then @A i = A i0 : Type (ℓ i)@ must hold for all @i : I@.
--
checkPrimTrans :: QName -> ArgsCheck
checkPrimTrans :: QName -> ArgsCheck
checkPrimTrans QName
c ArgRanges
rs Elims
vs Type
_ = case Elims
vs of
  -- Andreas, 2019-03-02, issue #3601, why exactly 4 arguments?
  -- Only 3 are needed to check the side condition.
  -- WAS:
  -- [l, a, phi, a0] -> do
  Arg Term
l :@ Arg Term
a :@ Arg Term
phi :@ Elims
rest -> do
    iz <- ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo (Term -> Arg Term) -> TCM Term -> TCMT IO (Arg Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntervalView -> TCM Term
forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
IZero

    -- ty = (i : I) -> Type (l i)
    ty <- runNamesT [] $ do
      l <- open $ unArg l
      nPi' "i" primIntervalType $ \ NamesT (TCMT IO) Term
i -> (Sort -> Type
sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NamesT (TCMT IO) Term
l NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i))

    a <- blockArg ty (rs !!! 1) a $ equalTermOnFace (unArg phi) ty
      (unArg a)
      (Lam defaultArgInfo $ NoAbs "_" $ apply (unArg a) [iz])

    return $ l :@ a :@ phi :@ rest
  Elims
_ -> TypeError -> TCM Elims
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM Elims) -> TypeError -> TCM Elims
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
CubicalPrimitiveNotFullyApplied QName
c

blockArg :: HasRange r => Type -> r -> Arg Term -> TCM () -> TCM (Arg Term)
blockArg :: forall r.
HasRange r =>
Type -> r -> Arg Term -> TCM () -> TCMT IO (Arg Term)
blockArg Type
t r
r Arg Term
a TCM ()
m =
  Range -> TCMT IO (Arg Term) -> TCMT IO (Arg Term)
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (r -> Range
forall a. HasRange a => a -> Range
getRange (r -> Range) -> r -> Range
forall a b. (a -> b) -> a -> b
$ r
r) (TCMT IO (Arg Term) -> TCMT IO (Arg Term))
-> TCMT IO (Arg Term) -> TCMT IO (Arg Term)
forall a b. (a -> b) -> a -> b
$ (Term -> Arg Term) -> TCM Term -> TCMT IO (Arg Term)
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Arg Term
a Arg Term -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) (TCM Term -> TCMT IO (Arg Term)) -> TCM Term -> TCMT IO (Arg Term)
forall a b. (a -> b) -> a -> b
$ Type -> TCM Term -> TCM Term
blockTerm Type
t (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ TCM ()
m TCM () -> TCM Term -> TCM Term
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)

-- The following comment contains silly ' escapes to calm CPP about ∨ (\vee).
-- May not be haddock-parseable.

-- ' @primPOr : ∀ {ℓ} (φ₁ φ₂ : I) {A : Partial (φ₁ ∨ φ₂) (Type ℓ)}
-- '         → (u : PartialP φ₁ (λ (o : IsOne φ₁) → A (IsOne1 φ₁ φ₂ o)))
-- '         → (v : PartialP φ₂ (λ (o : IsOne φ₂) → A (IsOne2 φ₁ φ₂ o)))
-- '         → PartialP (φ₁ ∨ φ₂) A@
-- '
-- ' Checks: @u = v : PartialP (φ₁ ∨ φ₂) A@ whenever @IsOne (φ₁ ∧ φ₂)@.
checkPrimPOr :: QName -> ArgsCheck
checkPrimPOr :: QName -> ArgsCheck
checkPrimPOr QName
c ArgRanges
rs Elims
vs Type
_ = case Elims
vs of
  Arg Term
l :@ Arg Term
phi1 :@ Arg Term
phi2 :@ Arg Term
a :@ Arg Term
u :@ Arg Term
v :@ Elims
rest -> do
    phi <- IntervalView -> TCM Term
forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview (Arg Term -> Arg Term -> IntervalView
IMin Arg Term
phi1 Arg Term
phi2)
    reportSDoc "tc.term.por" 10 $ text (show phi)
    t1 <- runNamesT [] $ do
            l <- open . unArg $ l
            a <- open . unArg $ a
            psi <- open =<< intervalUnview (IMax phi1 phi2)
            pPi' "o" psi $ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
l (NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o)
    tv <- runNamesT [] $ do
            l    <- open . unArg $ l
            a    <- open . unArg $ a
            phi1 <- open . unArg $ phi1
            phi2 <- open . unArg $ phi2
            pPi' "o" phi2 $ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
l (NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (TCM Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne2 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi1 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi2 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o))
    v <- blockArg tv (rs !!! 5) v $ do
      -- ' φ₁ ∧ φ₂  ⊢ u , v : PartialP (φ₁ ∨ φ₂) \ o → a o
      equalTermOnFace phi t1 (unArg u) (unArg v)
    return $ l :@ phi1 :@ phi2 :@ a :@ u :@ v :@ rest
  Elims
_ -> TypeError -> TCM Elims
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM Elims) -> TypeError -> TCM Elims
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
CubicalPrimitiveNotFullyApplied QName
c

-- | @prim^glue : ∀ {ℓ ℓ'} {A : Type ℓ} {φ : I}
--              → {T : Partial φ (Type ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
--              → (t : PartialP φ T) → (a : A) → primGlue A T e@
--
--   Check   @φ ⊢ a = e 1=1 (t 1=1)@  or actually the equivalent:  @(\ _ → a) = (\ o -> e o (t o)) : PartialP φ A@
checkPrimGlue :: QName -> ArgsCheck
checkPrimGlue :: QName -> ArgsCheck
checkPrimGlue QName
c ArgRanges
rs Elims
vs Type
_ = case Elims
vs of
  -- WAS: [la, lb, bA, phi, bT, e, t, a] -> do
  Arg Term
la :@ Arg Term
lb :@ Arg Term
bA :@ Arg Term
phi :@ Arg Term
bT :@ Arg Term
e :@ Arg Term
t :@ Arg Term
a :@ Elims
rest -> do
    v <- Names -> NamesT (TCMT IO) Term -> TCM Term
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] do
      lb  <- Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall (m :: * -> *) a.
(Monad m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
-> (Arg Term -> Term)
-> Arg Term
-> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
-> Arg Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall a b. (a -> b) -> a -> b
$ Arg Term
lb
      la  <- open . unArg $ la
      bA  <- open . unArg $ bA
      phi <- open . unArg $ phi
      bT  <- open . unArg $ bT
      e   <- open . unArg $ e
      t   <- open . unArg $ t
      let f NamesT (TCMT IO) Term
o = TCM Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquivFun NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT (TCMT IO) Term
bT NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
e NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o)
      glam defaultArgInfo "o" $ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
f NamesT (TCMT IO) Term
o NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
t NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o)

    ty <- runNamesT [] do
      lb  <- open . unArg $ lb
      phi <- open . unArg $ phi
      bA  <- open . unArg $ bA
      el's lb $ cl primPartialP <#> lb <@> phi <@> glam defaultArgInfo "o" (\ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
bA)

    let a' = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
NoAbs ArgName
"o" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)
    ta <- el' (pure $ unArg la) (pure $ unArg bA)
    a <- blockArg ta (rs !!! 7) a $ equalTerm ty a' v

    return $ la :@ lb :@ bA :@ phi :@ bT :@ e :@ t :@ a :@ rest
  Elims
_ -> TypeError -> TCM Elims
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM Elims) -> TypeError -> TCM Elims
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
CubicalPrimitiveNotFullyApplied QName
c


-- | @prim^glueU : ∀ {ℓ} {φ : I}
--              → {T : I → Partial φ (Type ℓ)} → {A : Type ℓ [ φ ↦ T i0 ]}
--              → (t : PartialP φ (T i1)) → (a : outS A) → hcomp T (outS A)@
--
--   Check   @φ ⊢ a = transp (\ i -> T 1=1 (~ i)) i0 (t 1=1)@  or actually the equivalent:
--           @(\ _ → a) = (\o -> transp (\ i -> T o (~ i)) i0 (t o)) : PartialP φ (T i0)@
checkPrimGlueU :: QName -> ArgsCheck
checkPrimGlueU :: QName -> ArgsCheck
checkPrimGlueU QName
c ArgRanges
rs Elims
vs Type
_ = case Elims
vs of
  -- WAS: [la, lb, bA, phi, bT, e, t, a] -> do
  Arg Term
la :@ Arg Term
phi :@ Arg Term
bT :@ Arg Term
bA :@ Arg Term
t :@ Arg Term
a :@ Elims
rest -> do
    v <- Names -> NamesT (TCMT IO) Term -> TCM Term
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT (TCMT IO) Term -> TCM Term)
-> NamesT (TCMT IO) Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
      la  <- Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall (m :: * -> *) a.
(Monad m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
-> (Arg Term -> Term)
-> Arg Term
-> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
-> Arg Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall a b. (a -> b) -> a -> b
$ Arg Term
la
      phi <- open . unArg $ phi
      bT  <- open . unArg $ bT
      bA  <- open . unArg $ bA
      t   <- open . unArg $ t
      let f NamesT (TCMT IO) Term
o = TCM Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrans NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> ArgName
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
Monad m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" (NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall a b. a -> b -> a
const NamesT (TCMT IO) Term
la) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> ArgName
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
Monad m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" (\ NamesT (TCMT IO) Term
i -> NamesT (TCMT IO) Term
bT NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (TCM Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCM Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
      glam defaultArgInfo "o" $ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
f NamesT (TCMT IO) Term
o NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
t NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o)
    ty <- runNamesT [] $ do
      la  <- open . unArg $ la
      phi <- open . unArg $ phi
      bT  <- open . unArg $ bT
      pPi' "o" phi $ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la (NamesT (TCMT IO) Term
bT NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCM Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o)
    let a' = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
NoAbs ArgName
"o" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)
    ta <- runNamesT [] $ do
      la  <- open . unArg $ la
      phi <- open . unArg $ phi
      bT  <- open . unArg $ bT
      bA  <- open . unArg $ bA
      el' la (cl primSubOut <#> (cl primLevelSuc <@> la) <#> (Sort . tmSort <$> la) <#> phi <#> (bT <@> cl primIZero) <@> bA)
    a <- blockArg ta (rs !!! 5) a $ equalTerm ty a' v
    return $ la :@ phi :@ bT :@ bA :@ t :@ a :@ rest
  Elims
_ -> TypeError -> TCM Elims
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM Elims) -> TypeError -> TCM Elims
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
CubicalPrimitiveNotFullyApplied QName
c