{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Primitive.Cubical.HCompU
  ( doHCompUKanOp
  , prim_glueU'
  , prim_unglueU'
  )
  where

import Control.Monad
import Control.Monad.Except ( MonadError )

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

import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Pure
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Substitute (absBody, apply, sort, subst, applyE)
import Agda.TypeChecking.Reduce (reduceB', reduceB, reduce')
import Agda.TypeChecking.Names (NamesT, runNamesT, runNames, cl, lam, open, ilam)

import Agda.Interaction.Options.Base (optCubical)

import Agda.Syntax.Common
  ( Hiding(..), Cubical(..), Arg(..)
  , ConOrigin(..), ProjOrigin(..)
  , Relevance(..)
  , setRelevance
  , defaultArgInfo, hasQuantity0, defaultArg, setHiding
  )

import Agda.TypeChecking.Primitive.Base
  ( (-->), nPi', pPi', hPi', el, el', el's, (<@>), (<@@>), (<#>), argN, argH, (<..>)
  , SigmaKit(..), getSigmaKit
  )

import Agda.Syntax.Internal
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.TypeChecking.Monad.Debug (__IMPOSSIBLE_VERBOSE__)

import Agda.TypeChecking.Primitive.Cubical.Glue
import Agda.TypeChecking.Primitive.Cubical.Base

-- | Perform the Kan operations for an @hcomp {A = Type} {φ} u u0@ type.
doHCompUKanOp
  :: 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 :: String -> m Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm forall a b. (a -> b) -> a -> b
$ (String
builtinHComp forall a. [a] -> [a] -> [a]
++ String
" for " forall a. [a] -> [a] -> [a]
++ String
builtinHComp forall a. [a] -> [a] -> [a]
++ String
" of Set")
  Term
io       <- String -> m Term
getTermLocal String
builtinIOne
  Term
iz       <- String -> m Term
getTermLocal String
builtinIZero
  Term
tHComp   <- String -> m Term
getTermLocal String
builtinHComp
  Term
tTransp  <- String -> m Term
getTermLocal String
builtinTrans
  Term
tglue    <- String -> m Term
getTermLocal String
builtin_glueU
  Term
tunglue  <- String -> m Term
getTermLocal String
builtin_unglueU
  Term
tLSuc    <- String -> m Term
getTermLocal String
builtinLevelSuc
  Term
tSubIn   <- String -> m Term
getTermLocal String
builtinSubIn
  Term
tItIsOne <- String -> m Term
getTermLocal String
builtinItIsOne
  forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
    [NamesT m Term
psi, NamesT m Term
u, NamesT m Term
u0] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [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] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
la, Arg Term
phi, Arg Term
bT, Arg Term
bA]

    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). PureTCM m => TermPosition -> m Term -> m Bool
headStop TermPosition
tpos NamesT m Term
phi) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTransp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" (forall a b. a -> b -> a
const NamesT m Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" NamesT m Term -> NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz 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 = 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 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tSubIn forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tLSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
phi 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tunglue forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bAS forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
g

      a1 :: NamesT m Term
a1 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m Term
phi)
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" (\NamesT m Term
i -> 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, forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" (\NamesT m Term
o -> NamesT m Term -> NamesT m Term
unglue (NamesT m Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o)))
            , (NamesT m Term
phi, forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"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 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
i) 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)))
            ])
        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 (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 (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 :: String
localUse = String
builtinTrans forall a. [a] -> [a] -> [a]
++ String
" for " forall a. [a] -> [a] -> [a]
++ String
builtinHComp forall a. [a] -> [a] -> [a]
++ String
" of Set"
    getTermLocal :: String -> m Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm String
localUse
  Term
tPOr <- String -> m Term
getTermLocal String
"primPOr"
  Term
tIMax <- String -> m Term
getTermLocal String
builtinIMax
  Term
tIMin <- String -> m Term
getTermLocal String
builtinIMin
  Term
tINeg <- String -> m Term
getTermLocal String
builtinINeg
  Term
tHComp <- String -> m Term
getTermLocal String
builtinHComp
  Term
tTrans <- String -> m Term
getTermLocal String
builtinTrans
  Term
tTranspProof <- String -> m Term
getTermLocal String
builtinTranspProof
  Term
tSubIn <- String -> m Term
getTermLocal String
builtinSubIn
  Term
tForall  <- String -> m Term
getTermLocal String
builtinFaceForall
  Term
io      <- String -> m Term
getTermLocal String
builtinIOne
  Term
iz      <- String -> m Term
getTermLocal String
builtinIZero
  Term
tLSuc   <- String -> m Term
getTermLocal String
builtinLevelSuc
  Term
tPath   <- String -> m Term
getTermLocal String
builtinPath
  Term
tItIsOne   <- String -> m Term
getTermLocal String
builtinItIsOne
  SigmaKit
kit <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit
  forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] 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 <- forall (m :: * -> *).
HasBuiltins m =>
String
-> NamesT
     m
     (NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term)
mkGComp String
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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTrans forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" (forall a b. a -> b -> a
const NamesT m Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" NamesT m Term -> NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTrans
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"j" (\ NamesT m Term
j -> NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imin NamesT m Term
i NamesT m Term
j)
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"j" (\ NamesT m Term
j -> NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imin NamesT m Term
i NamesT m Term
j)
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
phi (forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
i))
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u0

    [NamesT m Term
psi, NamesT m Term
u0] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
psi, Arg Term
u0]
    NamesT m Term -> NamesT m Term -> NamesT m Term
glue1 <- do
      Term
tglue             <- forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall a b. (a -> b) -> a -> b
$ String -> m Term
getTermLocal String
builtin_glueU
      [NamesT m Term
la, NamesT m Term
phi, NamesT m Term
bT, NamesT m Term
bA] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 Term
io) forall a b. (a -> b) -> a -> b
$ [Arg Term
la, Arg Term
phi, Arg Term
bT, Arg Term
bA]
      let bAS :: NamesT m Term
bAS = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tSubIn forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tLSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
bA
      NamesT m Term
g <- (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tglue forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bAS
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
t NamesT m Term
a -> NamesT m Term
g forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
t forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
a

    [NamesT m Term
la, NamesT m Term
phi, NamesT m Term
bT, NamesT m Term
bA] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\Arg Term
a -> forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Names -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" (forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall a b. (a -> b) -> a -> b
$ String -> m Term
getTermLocal String
builtin_unglueU
    let
      bAS :: NamesT m Term -> NamesT m Term
bAS NamesT m Term
i = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tSubIn
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tLSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
bA 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tunglue
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term -> NamesT m Term
bAS NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u0

    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). PureTCM m => TermPosition -> m Term -> m Bool
headStop TermPosition
tpos (NamesT m Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just 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 (forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
i -> NamesT m Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io 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 (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term
o

      -- compute "forall. phi"
      forallphi :: NamesT m Term
forallphi = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tForall 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 (forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m Term
forallphi)
        (forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
i -> forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys (NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) (NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)
          [ (NamesT m Term
psi,       forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" 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, forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"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 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) (\NamesT m Term
j -> NamesT m Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
j 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 (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 = forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"x" 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 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) (\NamesT m Term
j -> NamesT m Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
j 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 ]
        forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys (NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) (NamesT m Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o)
          [ (NamesT m Term
psi       , forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" forall a b. (a -> b) -> a -> b
$ \NamesT m Term
_ -> NamesT m Term
u0)
          , (NamesT m Term
forallphi , forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" 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 ]
         forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTranspProof
          forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" (\NamesT m Term
i -> NamesT m Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o)
          forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m Term
forallphi
          forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term
pt NamesT m Term
o
          forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tSubIn forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m Term
forallphi
                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 forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (forall t. Apply t => t -> Elims -> t
`applyE` [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 forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (forall t. Apply t => t -> Elims -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem (SigmaKit -> QName
sigmaSnd SigmaKit
kit)])
      a1' :: NamesT m Term
a1' = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax (NamesT m Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term
psi
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"j" (\NamesT m Term
j -> forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys (NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) (NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)
          [ (NamesT m Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io, forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" forall a b. (a -> b) -> a -> b
$ \NamesT m Term
o -> NamesT m Term -> NamesT m Term
alpha NamesT m Term
o forall (m :: * -> *).
Applicative m =>
m Term -> (m Term, m Term, m Term) -> m Term
<@@> (NamesT m Term -> NamesT m Term -> NamesT m Term
w (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term
o 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,             forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" forall a b. (a -> b) -> a -> b
$ \NamesT m Term
o -> NamesT m Term
a1)
          ])
        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' (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tItIsOne)
doHCompUKanOp KanOperation
_ FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
_ TermPosition
_ = 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 -> String -> TCM ()
requireCubical Cubical
CErased String
""
  Type
t <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
       forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"la" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (\ NamesT (TCMT IO) Term
la ->
       forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"φ" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
φ ->
       forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"T" (forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"i" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
String
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' String
"o" NamesT (TCMT IO) Term
φ forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
t ->
       forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"A" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
φ forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
t forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a -> do
       let bA :: NamesT (TCMT IO) Term
bA = (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubOut forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
φ forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT (TCMT IO) Term
t forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a)
       forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
String
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' String
"o" NamesT (TCMT IO) Term
φ (\ NamesT (TCMT IO) Term
o -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la (NamesT (TCMT IO) Term
t forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o))
         forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
bA)
         forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
φ forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
t forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA))
  Term -> IntervalView
view <- forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  Term
one <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Int
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Int
6 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 <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
phi
       case Term -> IntervalView
view forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sphi of
         IntervalView
IOne -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
t forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
one]
         IntervalView
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
la] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
bT,Arg Term
bA,Arg Term
t,Arg Term
a])
      [Arg 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 -> String -> TCM ()
requireCubical Cubical
CErased String
""
  Type
t <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
       forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"la" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (\ NamesT (TCMT IO) Term
la ->
       forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"φ" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
φ ->
       forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"T" (forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"i" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
String
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' String
"o" NamesT (TCMT IO) Term
φ forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
t ->
       forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"A" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
φ forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
t forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a -> do
       let bA :: NamesT (TCMT IO) Term
bA = (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubOut forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
φ forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT (TCMT IO) Term
t forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a)
       forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
φ forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
t forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA)
         forall (m :: * -> *). Applicative m => m Type -> m Type -> m 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 <- forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  Term
one <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
  Maybe QName
mglueU <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
builtin_glueU
  Maybe QName
mtransp <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
builtinTrans
  Maybe QName
mHCompU <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
builtinHComp
  let mhcomp :: Maybe QName
mhcomp = Maybe QName
mHCompU

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Int
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Int
5 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 <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
phi
      case Term -> IntervalView
view forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking 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 <- forall (m :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm String
builtin_unglueU String
builtinTrans
          Term
iNeg    <- forall (m :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm String
builtin_unglueU String
builtinINeg
          Term
iZ      <- forall (m :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm String
builtin_unglueU String
builtinIZero
          forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
            [NamesT ReduceM Term
la,NamesT ReduceM Term
bT,NamesT ReduceM Term
b] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
la,Arg Term
bT,Arg Term
b]
            forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTransp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" (\ NamesT ReduceM Term
_ -> NamesT ReduceM Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" (\ NamesT ReduceM Term
i -> NamesT ReduceM Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT ReduceM Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
one)
              forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iZ 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 <- 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 = forall (m :: * -> *) a. Monad m => a -> m a
return (forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
la] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
bT,Arg Term
bA] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sb])
          case forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking 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] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es, forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mglueU -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ 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] | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mtransp -> do
              Blocked (Arg Term)
sbA <- forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Arg Term
bA
              case forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sbA of
                Lam ArgInfo
_ Abs Term
t -> do
                  Blocked Term
st <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' (forall a. Subst a => Abs a -> a
absBody Abs Term
t)
                  case 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] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es, forall a. a -> Maybe a
Just QName
h forall a. Eq a => a -> a -> Bool
== Maybe QName
mHCompU -> do
                      forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                        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 (forall a t. a -> Blocked' t a
notBlocked Arg Term
r) Arg Term
u0) (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 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] | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mhcomp -> do
              Blocked (Arg Term)
sbA <- forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Arg Term
bA
              case forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ 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] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es, forall a. a -> Maybe a
Just QName
h forall a. Eq a => a -> a -> Bool
== Maybe QName
mHCompU -> do
                  forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                    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 (forall a t. a -> Blocked' t a
notBlocked Arg Term
r) Arg Term
u Arg Term
u0) (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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
la] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
bT,Arg Term
bA] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sb])

    [Arg Term]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__