{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Primitive.Cubical.HCompU
  ( doHCompUKanOp
  , prim_glueU'
  , prim_unglueU'
  )
  where

import Control.Monad

import Agda.Syntax.Common
  ( Cubical(..), Arg(..)
  , ProjOrigin(..)
  )
import Agda.Syntax.Internal

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Pure

import Agda.TypeChecking.Names
  ( runNamesT, runNames, cl, lam, open, ilam )
import Agda.TypeChecking.Primitive.Base
  ( (-->), nPi', pPi', hPi', el, el', el's, (<@>), (<@@>), (<#>), argN, (<..>)
  , SigmaKit(..), getSigmaKit
  )
import Agda.TypeChecking.Primitive.Cubical.Glue
import Agda.TypeChecking.Primitive.Cubical.Base
import Agda.TypeChecking.Reduce
  ( reduceB', reduceB )
import Agda.TypeChecking.Substitute
  ( absBody, apply, sort, applyE )

import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Monad

import Agda.Utils.Impossible (__IMPOSSIBLE__)

-- | Perform the Kan operations for an @hcomp {A = Type} {φ} u u0@ type.
doHCompUKanOp
  :: forall m. PureTCM m
  => KanOperation
  -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
  -> TermPosition
  -> m (Maybe Term)

-- TODO (Amy, 2022-08-17): This is literally the same algorithm as
-- doGlueKanOp, but specialised for using transport as the equivalence.
-- Can we deduplicate them?
doHCompUKanOp :: forall (m :: * -> *).
PureTCM m =>
KanOperation
-> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> m (Maybe Term)
doHCompUKanOp (HCompOp Blocked (Arg Term)
psi Arg Term
u Arg Term
u0) (IsNot (Arg Term
la, Arg Term
phi, Arg Term
bT, Arg Term
bA)) TermPosition
tpos = do
  let getTermLocal :: IsBuiltin a => a -> m Term
      getTermLocal :: forall a. IsBuiltin a => a -> m Term
getTermLocal = [Char] -> a -> m Term
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
[Char] -> a -> m Term
getTerm ([Char] -> a -> m Term) -> [Char] -> a -> m Term
forall a b. (a -> b) -> a -> b
$ PrimitiveId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtinHComp [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PrimitiveId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtinHComp [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" of Set"
  Term
io       <- BuiltinId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinIOne
  Term
iz       <- BuiltinId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinIZero
  Term
tHComp   <- PrimitiveId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinHComp
  Term
tTransp  <- PrimitiveId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinTrans
  Term
tunglue  <- PrimitiveId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtin_unglueU
  Term
tLSuc    <- BuiltinId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinLevelSuc
  Term
tSubIn   <- BuiltinId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinSubIn
  Term
tItIsOne <- BuiltinId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinItIsOne
  Names -> NamesT m (Maybe Term) -> m (Maybe Term)
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT m (Maybe Term) -> m (Maybe Term))
-> NamesT m (Maybe Term) -> m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ do
    [NamesT m Term
psi, NamesT m Term
u, NamesT m Term
u0] <- (Arg Term -> NamesT m (NamesT m Term))
-> [Arg Term] -> NamesT m [NamesT m Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Term -> NamesT m (NamesT m Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT m (NamesT m Term))
-> (Arg Term -> Term) -> Arg Term -> NamesT m (NamesT m Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
psi, Arg Term
u, Arg Term
u0]
    [NamesT m Term
la, NamesT m Term
phi, NamesT m Term
bT, NamesT m Term
bA] <- (Arg Term -> NamesT m (NamesT m Term))
-> [Arg Term] -> NamesT m [NamesT m Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Term -> NamesT m (NamesT m Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT m (NamesT m Term))
-> (Arg Term -> Term) -> Arg Term -> NamesT m (NamesT m Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Arg Term
la, Arg Term
phi, Arg Term
bT, Arg Term
bA]

    NamesT m Bool
-> NamesT m (Maybe Term)
-> NamesT m (Maybe Term)
-> NamesT m (Maybe Term)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (TermPosition -> NamesT m Term -> NamesT m Bool
forall (m :: * -> *). PureTCM m => TermPosition -> m Term -> m Bool
headStop TermPosition
tpos NamesT m Term
phi) (Maybe Term -> NamesT m (Maybe Term)
forall a. a -> NamesT m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing) (NamesT m (Maybe Term) -> NamesT m (Maybe Term))
-> NamesT m (Maybe Term) -> NamesT m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> NamesT m Term -> NamesT m (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do

    let
      transp :: NamesT m Term
-> (NamesT m Term -> NamesT m Term)
-> NamesT m Term
-> NamesT m Term
transp NamesT m Term
la NamesT m Term -> NamesT m Term
bA NamesT m Term
a0 = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTransp NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (NamesT m Term -> NamesT m Term -> NamesT m Term
forall a b. a -> b -> a
const NamesT m Term
la) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" NamesT m Term -> NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
a0
      tf :: NamesT m Term -> NamesT m Term -> NamesT m Term
tf NamesT m Term
i NamesT m Term
o = NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
hfill NamesT m Term
la (NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) NamesT m Term
psi NamesT m Term
u NamesT m Term
u0 NamesT m Term
i

      bAS :: NamesT m Term
bAS = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tSubIn NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tLSuc NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
la) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Sort -> Term
Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Term) -> NamesT m Term -> NamesT m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m Term
la) 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 Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
bA
      unglue :: NamesT m Term -> NamesT m Term
unglue NamesT m Term
g = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tunglue NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
la 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 Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bAS NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
g

      a1 :: NamesT m Term
a1 = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m Term
phi)
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (\NamesT m Term
i -> NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys NamesT m Term
la NamesT m Term
bA
            [ (NamesT m Term
psi, [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (\NamesT m Term
o -> NamesT m Term -> NamesT m Term
unglue (NamesT m Term
u NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o)))
            , (NamesT m Term
phi, [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (\ NamesT m Term
o -> NamesT m Term
-> (NamesT m Term -> NamesT m Term)
-> NamesT m Term
-> NamesT m Term
transp NamesT m Term
la (\NamesT m Term
i -> NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
i) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) (NamesT m Term -> NamesT m Term -> NamesT m Term
tf NamesT m Term
i NamesT m Term
o)))
            ])
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term
unglue NamesT m Term
u0

      t1 :: NamesT m Term -> NamesT m Term
t1 = NamesT m Term -> NamesT m Term -> NamesT m Term
tf (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)

    -- pure tglue <#> la <#> phi <#> bT <#> bAS <@> (ilam "o" $ \ o -> t1 o) <@> a1
    case TermPosition
tpos of
      TermPosition
Eliminated -> NamesT m Term
a1
      TermPosition
Head       -> NamesT m Term -> NamesT m Term
t1 (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tItIsOne)


doHCompUKanOp (TranspOp Blocked (Arg Term)
psi Arg Term
u0) (IsFam (Arg Term
la, Arg Term
phi, Arg Term
bT, Arg Term
bA)) TermPosition
tpos = do
  let
    localUse :: [Char]
localUse = PrimitiveId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtinTrans [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PrimitiveId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtinHComp [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" of Set"
    getTermLocal :: IsBuiltin a => a -> m Term
    getTermLocal :: forall a. IsBuiltin a => a -> m Term
getTermLocal = [Char] -> a -> m Term
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
[Char] -> a -> m Term
getTerm [Char]
localUse
  Term
tPOr <- PrimitiveId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinPOr
  Term
tIMax <- PrimitiveId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinIMax
  Term
tIMin <- PrimitiveId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinIMin
  Term
tINeg <- PrimitiveId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinINeg
  Term
tHComp <- PrimitiveId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinHComp
  Term
tTrans <- PrimitiveId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinTrans
  Term
tTranspProof <- BuiltinId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinTranspProof
  Term
tSubIn <- BuiltinId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinSubIn
  Term
tForall  <- PrimitiveId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinFaceForall
  Term
io      <- BuiltinId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinIOne
  Term
iz      <- BuiltinId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinIZero
  Term
tLSuc   <- BuiltinId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinLevelSuc
  Term
tPath   <- BuiltinId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinPath
  Term
tItIsOne   <- BuiltinId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinItIsOne
  SigmaKit
kit <- SigmaKit -> Maybe SigmaKit -> SigmaKit
forall a. a -> Maybe a -> a
fromMaybe SigmaKit
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe SigmaKit -> SigmaKit) -> m (Maybe SigmaKit) -> m SigmaKit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe SigmaKit)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit
  Names -> NamesT m (Maybe Term) -> m (Maybe Term)
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT m (Maybe Term) -> m (Maybe Term))
-> NamesT m (Maybe Term) -> m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ do
    -- Helper definitions we'll use:
    NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
gcomp <- [Char]
-> NamesT
     m
     (NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term)
forall (m :: * -> *).
HasBuiltins m =>
[Char]
-> NamesT
     m
     (NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term)
mkGComp [Char]
localUse

    let
      transp :: NamesT m Term
-> (NamesT m Term -> NamesT m Term)
-> NamesT m Term
-> NamesT m Term
transp NamesT m Term
la NamesT m Term -> NamesT m Term
bA NamesT m Term
a0 = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTrans NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (NamesT m Term -> NamesT m Term -> NamesT m Term
forall a b. a -> b -> a
const NamesT m Term
la) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" NamesT m Term -> NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
a0
      transpFill :: NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
transpFill NamesT m Term
la NamesT m Term
bA NamesT m Term
phi NamesT m Term
u0 NamesT m Term
i = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTrans
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"j" (\ NamesT m Term
j -> NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imin NamesT m Term
i NamesT m Term
j)
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"j" (\ NamesT m Term
j -> NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imin NamesT m Term
i NamesT m Term
j)
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
phi (NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
i))
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u0

    [NamesT m Term
psi, NamesT m Term
u0] <- (Arg Term -> NamesT m (NamesT m Term))
-> [Arg Term] -> NamesT m [NamesT m Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Term -> NamesT m (NamesT m Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT m (NamesT m Term))
-> (Arg Term -> Term) -> Arg Term -> NamesT m (NamesT m Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
psi, Arg Term
u0]

    [NamesT m Term
la, NamesT m Term
phi, NamesT m Term
bT, NamesT m Term
bA] <- (Arg Term -> NamesT m (NamesT m Term))
-> [Arg Term] -> NamesT m [NamesT m Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Arg Term
a -> Term -> NamesT m (NamesT m Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT m (NamesT m Term))
-> (NamesT Fail Term -> Term)
-> NamesT Fail Term
-> NamesT m (NamesT m Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Names -> NamesT Fail Term -> Term
forall a. Names -> NamesT Fail a -> a
runNames [] (NamesT Fail Term -> NamesT m (NamesT m Term))
-> NamesT Fail Term -> NamesT m (NamesT m Term)
forall a b. (a -> b) -> a -> b
$ [Char]
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall a b. a -> b -> a
const (Term -> NamesT Fail Term
forall a. a -> NamesT Fail a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> NamesT Fail Term) -> Term -> NamesT Fail Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a))) [Arg Term
la, Arg Term
phi, Arg Term
bT, Arg Term
bA]

    -- Andreas, 2022-03-25, issue #5838.
    -- Port the fix of @unglueTranspGlue@ and @doGlueKanOp DoTransp@
    -- also to @doHCompUKanOp DoTransp@, as suggested by Tom Jack and Anders Mörtberg.
    -- We define @unglue_u0 i@ that is first used with @i@ and then with @i0@.
    -- The original code used it only with @i0@.
    Term
tunglue <- m Term -> NamesT m Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl (m Term -> NamesT m Term) -> m Term -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ PrimitiveId -> m Term
forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtin_unglueU
    let
      bAS :: NamesT m Term -> NamesT m Term
bAS NamesT m Term
i = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tSubIn
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tLSuc NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Sort -> Term
Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Term) -> NamesT m Term -> NamesT m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)) 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 Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)
      unglue_u0 :: NamesT m Term -> NamesT m Term
unglue_u0 NamesT m Term
i = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tunglue
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) 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 Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term -> NamesT m Term
bAS NamesT m Term
i NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u0

    NamesT m Bool
-> NamesT m (Maybe Term)
-> NamesT m (Maybe Term)
-> NamesT m (Maybe Term)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (TermPosition -> NamesT m Term -> NamesT m Bool
forall (m :: * -> *). PureTCM m => TermPosition -> m Term -> m Bool
headStop TermPosition
tpos (NamesT m Term
phi NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)) (Maybe Term -> NamesT m (Maybe Term)
forall a. a -> NamesT m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing) (NamesT m (Maybe Term) -> NamesT m (Maybe Term))
-> NamesT m (Maybe Term) -> NamesT m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> NamesT m Term -> NamesT m (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do

    let
      tf :: NamesT m Term -> NamesT m Term -> NamesT m Term
tf NamesT m Term
i NamesT m Term
o = NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
transpFill NamesT m Term
la ([Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
i -> NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) NamesT m Term
psi NamesT m Term
u0 NamesT m Term
i
      t1 :: NamesT m Term -> NamesT m Term
t1 NamesT m Term
o   = NamesT m Term -> NamesT m Term -> NamesT m Term
tf (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term
o

      -- compute "forall. phi"
      forallphi :: NamesT m Term
forallphi = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tForall NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
phi

      -- a1 with gcomp
      a1 :: NamesT m Term
a1 = NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
gcomp NamesT m Term
la NamesT m Term
bA (NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m Term
forallphi)
        ([Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
i -> NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) (NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)
          [ (NamesT m Term
psi,       [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \NamesT m Term
_ -> NamesT m Term -> NamesT m Term
unglue_u0 NamesT m Term
i)
          , (NamesT m Term
forallphi, [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (\NamesT m Term
o -> NamesT m Term
-> (NamesT m Term -> NamesT m Term)
-> NamesT m Term
-> NamesT m Term
transp (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) (\NamesT m Term
j -> NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
j NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) (NamesT m Term -> NamesT m Term -> NamesT m Term
tf NamesT m Term
i NamesT m Term
o)))
          ])
          (NamesT m Term -> NamesT m Term
unglue_u0 (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz))

      w :: NamesT m Term -> NamesT m Term -> NamesT m Term
w NamesT m Term
i NamesT m Term
o = [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"x" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ NamesT m Term
-> (NamesT m Term -> NamesT m Term)
-> NamesT m Term
-> NamesT m Term
transp (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) (\NamesT m Term
j -> NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
j NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o)

      pt :: NamesT m Term -> NamesT m Term
pt NamesT m Term
o = -- o : [ φ 1 ]
        NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) (NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o)
          [ (NamesT m Term
psi       , [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \NamesT m Term
_ -> NamesT m Term
u0)
          , (NamesT m Term
forallphi , [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \NamesT m Term
o -> NamesT m Term -> NamesT m Term
t1 NamesT m Term
o)
          ]

      -- "ghcomp" is implemented in the proof of tTranspProof
      -- (see src/data/lib/prim/Agda/Builtin/Cubical/HCompU.agda)
      t1'alpha :: NamesT m Term -> NamesT m Term
t1'alpha NamesT m Term
o = -- o : [ φ 1 ]
         Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTranspProof
          NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (\NamesT m Term
i -> NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
i NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o)
          NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m Term
forallphi
          NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term
pt NamesT m Term
o
          NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tSubIn NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m Term
forallphi
                NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
a1)

      -- TODO: optimize?
      t1' :: NamesT m Term -> NamesT m Term
t1' NamesT m Term
o   = NamesT m Term -> NamesT m Term
t1'alpha NamesT m Term
o NamesT m Term -> (Term -> Term) -> NamesT m Term
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem (SigmaKit -> QName
sigmaFst SigmaKit
kit)])
      alpha :: NamesT m Term -> NamesT m Term
alpha NamesT m Term
o = NamesT m Term -> NamesT m Term
t1'alpha NamesT m Term
o NamesT m Term -> (Term -> Term) -> NamesT m Term
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem (SigmaKit -> QName
sigmaSnd SigmaKit
kit)])
      a1' :: NamesT m Term
a1' = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax (NamesT m Term
phi NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term
psi
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"j" (\NamesT m Term
j -> NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) (NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)
          [ (NamesT m Term
phi NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io, [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \NamesT m Term
o -> NamesT m Term -> NamesT m Term
alpha NamesT m Term
o NamesT m Term
-> (NamesT m Term, NamesT m Term, NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
Applicative m =>
m Term -> (m Term, m Term, m Term) -> m Term
<@@> (NamesT m Term -> NamesT m Term -> NamesT m Term
w (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term
o NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term
t1' NamesT m Term
o, NamesT m Term
a1, NamesT m Term
j))
          , (NamesT m Term
psi,             [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \NamesT m Term
o -> NamesT m Term
a1)
          ])
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
a1

    -- glue1 (ilam "o" t1') a1'
    case TermPosition
tpos of
      TermPosition
Eliminated -> NamesT m Term
a1'
      TermPosition
Head       -> NamesT m Term -> NamesT m Term
t1' (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tItIsOne)
doHCompUKanOp KanOperation
_ FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
_ TermPosition
_ = m (Maybe Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | The implementation of 'prim_glueU', the introduction form for
-- @hcomp@ types.
prim_glueU' :: TCM PrimitiveImpl
prim_glueU' :: TCM PrimitiveImpl
prim_glueU' = do
-- TODO (Amy, 2022-08-17): Same thing about duplicated code with Glue
-- applies here.
  Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
  Type
t <- Names -> NamesT (TCMT IO) Type -> TCMT IO Type
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT (TCMT IO) Type -> TCMT IO Type)
-> NamesT (TCMT IO) Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$
       [Char]
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"la" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Functor m => m Term -> m Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (\ NamesT (TCMT IO) Term
la ->
       [Char]
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"φ" NamesT (TCMT IO) Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
φ ->
       [Char]
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"T" ([Char]
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i" NamesT (TCMT IO) Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> [Char]
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
φ ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> 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
la) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
t ->
       [Char]
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"A" (NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc 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) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc 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
<@> (Sort -> Term
Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
φ 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
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero)) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a -> do
       let bA :: NamesT (TCMT IO) Term
bA = (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubOut NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc 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
<#> (Sort -> Term
Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
φ 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
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
a)
       [Char]
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
φ (\ 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
t NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne 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) Type
-> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (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
bA)
         NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> 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 (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHComp NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc 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
<#> (Sort -> Term
Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
φ 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
bA))
  Term -> IntervalView
view <- TCMT IO (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  Term
one <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
  PrimitiveImpl -> TCM PrimitiveImpl
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
6 (([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
 -> PrimFun)
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
forall a b. (a -> b) -> a -> b
$ \[Arg Term]
ts ->
    case [Arg Term]
ts of
      [Arg Term
la,Arg Term
phi,Arg Term
bT,Arg Term
bA,Arg Term
t,Arg Term
a] -> do
       Blocked (Arg Term)
sphi <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
phi
       case Term -> IntervalView
view (Term -> IntervalView) -> Term -> IntervalView
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked (Arg Term) -> Arg Term) -> Blocked (Arg Term) -> Arg Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sphi of
         IntervalView
IOne -> 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
forall e. Arg e -> e
unArg Arg Term
t Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN Term
one]
         IntervalView
_    -> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall no yes. no -> Reduced no yes
NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
-> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
la] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
bT,Arg Term
bA,Arg Term
t,Arg Term
a])
      [Arg Term]
_ -> ReduceM (Reduced MaybeReducedArgs Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | The implementation of 'prim_unglueU', the elimination form for
-- @hcomp@ types.
prim_unglueU' :: TCM PrimitiveImpl
prim_unglueU' :: TCM PrimitiveImpl
prim_unglueU' = do
-- TODO (Amy, 2022-08-17): Same thing about duplicated code with Glue
-- applies here.
  Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
  Type
t <- Names -> NamesT (TCMT IO) Type -> TCMT IO Type
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT (TCMT IO) Type -> TCMT IO Type)
-> NamesT (TCMT IO) Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$
       [Char]
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"la" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Functor m => m Term -> m Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (\ NamesT (TCMT IO) Term
la ->
       [Char]
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"φ" NamesT (TCMT IO) Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
φ ->
       [Char]
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"T" ([Char]
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i" NamesT (TCMT IO) Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> [Char]
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
φ ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> 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
la) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
t ->
       [Char]
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"A" (NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc 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) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc 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
<@> (Sort -> Term
Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
φ 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
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero)) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a -> do
       let bA :: NamesT (TCMT IO) Term
bA = (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubOut NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc 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
<#> (Sort -> Term
Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
φ 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
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
a)
       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 (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHComp NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc 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
<#> (Sort -> Term
Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
φ 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
bA)
         NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> 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
bA)

  Term -> IntervalView
view <- TCMT IO (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  Term
one <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
  Maybe QName
mglueU <- PrimitiveId -> TCMT IO (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
builtin_glueU
  Maybe QName
mtransp <- PrimitiveId -> TCMT IO (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
builtinTrans
  Maybe QName
mHCompU <- PrimitiveId -> TCMT IO (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
builtinHComp
  let mhcomp :: Maybe QName
mhcomp = Maybe QName
mHCompU

  PrimitiveImpl -> TCM PrimitiveImpl
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
5 (([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
 -> PrimFun)
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
forall a b. (a -> b) -> a -> b
$ \case
    [Arg Term
la,Arg Term
phi,Arg Term
bT,Arg Term
bA,Arg Term
b] -> do
      Blocked (Arg Term)
sphi <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
phi
      case Term -> IntervalView
view (Term -> IntervalView) -> Term -> IntervalView
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked (Arg Term) -> Arg Term) -> Blocked (Arg Term) -> Arg Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sphi of
        -- Case where the hcomp has reduced away: Transport backwards
        -- along the partial element we've glued.
        IntervalView
IOne -> do
          Term
tTransp <- [Char] -> PrimitiveId -> ReduceM Term
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
[Char] -> a -> m Term
getTerm (PrimitiveId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtin_unglueU) PrimitiveId
builtinTrans
          Term
iNeg    <- [Char] -> PrimitiveId -> ReduceM Term
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
[Char] -> a -> m Term
getTerm (PrimitiveId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtin_unglueU) PrimitiveId
builtinINeg
          Term
iZ      <- [Char] -> BuiltinId -> ReduceM Term
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
[Char] -> a -> m Term
getTerm (PrimitiveId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtin_unglueU) BuiltinId
builtinIZero
          Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> (NamesT ReduceM Term -> ReduceM Term)
-> NamesT ReduceM Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Names -> NamesT ReduceM Term -> ReduceM Term
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> NamesT ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ do
            [NamesT ReduceM Term
la,NamesT ReduceM Term
bT,NamesT ReduceM Term
b] <- (Arg Term -> NamesT ReduceM (NamesT ReduceM Term))
-> [Arg Term] -> NamesT ReduceM [NamesT ReduceM Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Term -> NamesT ReduceM (NamesT ReduceM Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT ReduceM (NamesT ReduceM Term))
-> (Arg Term -> Term)
-> Arg Term
-> NamesT ReduceM (NamesT ReduceM Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Arg Term
la,Arg Term
bT,Arg Term
b]
            Term -> NamesT ReduceM Term
forall a. a -> NamesT ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTransp NamesT ReduceM Term -> NamesT ReduceM Term -> NamesT ReduceM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> [Char]
-> (NamesT ReduceM Term -> NamesT ReduceM Term)
-> NamesT ReduceM Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (\ NamesT ReduceM Term
_ -> NamesT ReduceM Term
la) NamesT ReduceM Term -> NamesT ReduceM Term -> NamesT ReduceM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> [Char]
-> (NamesT ReduceM Term -> NamesT ReduceM Term)
-> NamesT ReduceM Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (\ NamesT ReduceM Term
i -> NamesT ReduceM Term
bT NamesT ReduceM Term -> NamesT ReduceM Term -> NamesT ReduceM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term -> NamesT ReduceM Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT ReduceM Term
i NamesT ReduceM Term -> NamesT ReduceM Term -> NamesT ReduceM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> Term -> NamesT ReduceM Term
forall a. a -> NamesT ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
one)
              NamesT ReduceM Term -> NamesT ReduceM Term -> NamesT ReduceM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT ReduceM Term
forall a. a -> NamesT ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iZ NamesT ReduceM Term -> NamesT ReduceM Term -> NamesT ReduceM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
b

        -- Otherwise, we're dealing with a proper glu- didn't I already
        -- make this joke? Oh, yeah, in prim_unglue, right.
        IntervalView
_ -> do
          Blocked (Arg Term)
sb <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
b
          let fallback :: Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback Blocked (Arg Term)
sbA = Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall no yes. no -> Reduced no yes
NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
-> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
la] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
bT,Arg Term
bA] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sb])
          case Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked (Arg Term) -> Arg Term) -> Blocked (Arg Term) -> Arg Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sb of
            -- Project:
            Def QName
q Elims
es | Just [Arg Term
_,Arg Term
_,Arg Term
_,Arg Term
_,Arg Term
_, Arg Term
a] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es, 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
mglueU -> 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
forall e. Arg e -> e
unArg Arg Term
a

            -- Transport:
            Def QName
q [Apply Arg Term
l, Apply Arg Term
bA, Apply Arg Term
r, Apply Arg Term
u0] | 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
mtransp -> do
              Blocked (Arg Term)
sbA <- Arg Term -> ReduceM (Blocked (Arg Term))
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Arg Term
bA
              case Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sbA of
                Lam ArgInfo
_ Abs Term
t -> do
                  Blocked Term
st <- Term -> ReduceM (Blocked Term)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' (Abs Term -> Term
forall a. Subst a => Abs a -> a
absBody Abs Term
t)
                  case Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
st of
                    Def QName
h Elims
es | Just [Arg Term
la,Arg Term
_,Arg Term
phi,Arg Term
bT,Arg Term
bA] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es, QName -> Maybe QName
forall a. a -> Maybe a
Just QName
h Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mHCompU -> do
                      Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> (Maybe Term -> Term)
-> Maybe Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Maybe Term) -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                        KanOperation
-> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> ReduceM (Maybe Term)
forall (m :: * -> *).
PureTCM m =>
KanOperation
-> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> m (Maybe Term)
doHCompUKanOp (Blocked (Arg Term) -> Arg Term -> KanOperation
TranspOp (Arg Term -> Blocked (Arg Term)
forall a t. a -> Blocked' t a
notBlocked Arg Term
r) Arg Term
u0) ((Arg Term, Arg Term, Arg Term, Arg Term)
-> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
forall a. a -> FamilyOrNot a
IsFam (Arg Term
la,Arg Term
phi,Arg Term
bT,Arg Term
bA)) TermPosition
Eliminated
                    Term
_ -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback (Blocked Term
st Blocked Term -> Blocked (Arg Term) -> Blocked (Arg Term)
forall a b. Blocked' Term a -> Blocked' Term b -> Blocked' Term b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Blocked (Arg Term)
sbA)
                Term
_  -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback Blocked (Arg Term)
sbA

            -- Compose:
            Def QName
q [Apply Arg Term
l,Apply Arg Term
bA,Apply Arg Term
r,Apply Arg Term
u,Apply Arg Term
u0] | 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
mhcomp -> do
              Blocked (Arg Term)
sbA <- Arg Term -> ReduceM (Blocked (Arg Term))
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Arg Term
bA
              case Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sbA of
                Def QName
h Elims
es | Just [Arg Term
la,Arg Term
_,Arg Term
phi,Arg Term
bT,Arg Term
bA] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es, QName -> Maybe QName
forall a. a -> Maybe a
Just QName
h Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mHCompU -> do
                  Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> (Maybe Term -> Term)
-> Maybe Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Maybe Term) -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                    KanOperation
-> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> ReduceM (Maybe Term)
forall (m :: * -> *).
PureTCM m =>
KanOperation
-> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> m (Maybe Term)
doHCompUKanOp (Blocked (Arg Term) -> Arg Term -> Arg Term -> KanOperation
HCompOp (Arg Term -> Blocked (Arg Term)
forall a t. a -> Blocked' t a
notBlocked Arg Term
r) Arg Term
u Arg Term
u0) ((Arg Term, Arg Term, Arg Term, Arg Term)
-> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
forall a. a -> FamilyOrNot a
IsNot (Arg Term
la,Arg Term
phi,Arg Term
bT,Arg Term
bA)) TermPosition
Eliminated
                Term
_ -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback Blocked (Arg Term)
sbA
            Term
_ -> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall no yes. no -> Reduced no yes
NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
-> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
la] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
bT,Arg Term
bA] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sb])

    [Arg Term]
_ -> ReduceM (Reduced MaybeReducedArgs Term)
forall a. HasCallStack => a
__IMPOSSIBLE__