{-# 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, subst, applyE )
import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Impossible (__IMPOSSIBLE__)
doHCompUKanOp
:: forall m. PureTCM m
=> KanOperation
-> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> m (Maybe Term)
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 = forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
[Char] -> a -> m Term
getTerm forall a b. (a -> b) -> a -> b
$ forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtinHComp forall a. [a] -> [a] -> [a]
++ [Char]
" for " forall a. [a] -> [a] -> [a]
++ forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtinHComp forall a. [a] -> [a] -> [a]
++ [Char]
" of Set"
Term
io <- forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinIOne
Term
iz <- forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinIZero
Term
tHComp <- forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinHComp
Term
tTransp <- forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinTrans
Term
tglue <- forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtin_glueU
Term
tunglue <- forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtin_unglueU
Term
tLSuc <- forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinLevelSuc
Term
tSubIn <- forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinSubIn
Term
tItIsOne <- forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"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 =>
[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 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 =>
[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 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)
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 :: [Char]
localUse = forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtinTrans forall a. [a] -> [a] -> [a]
++ [Char]
" for " forall a. [a] -> [a] -> [a]
++ forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtinHComp forall a. [a] -> [a] -> [a]
++ [Char]
" of Set"
getTermLocal :: IsBuiltin a => a -> m Term
getTermLocal :: forall a. IsBuiltin a => a -> m Term
getTermLocal = forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
[Char] -> a -> m Term
getTerm [Char]
localUse
Term
tPOr <- forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinPOr
Term
tIMax <- forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinIMax
Term
tIMin <- forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinIMin
Term
tINeg <- forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinINeg
Term
tHComp <- forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinHComp
Term
tTrans <- forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinTrans
Term
tTranspProof <- forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinTranspProof
Term
tSubIn <- forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinSubIn
Term
tForall <- forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
builtinFaceForall
Term
io <- forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinIOne
Term
iz <- forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinIZero
Term
tLSuc <- forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinLevelSuc
Term
tPath <- forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
builtinPath
Term
tItIsOne <- forall a. IsBuiltin a => a -> m Term
getTermLocal BuiltinId
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
NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
gcomp <- 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 = 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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"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
$ forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"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]
Term
tunglue <- forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall a b. (a -> b) -> a -> b
$ forall a. IsBuiltin a => a -> m Term
getTermLocal PrimitiveId
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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"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
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 :: 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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"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 =>
[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 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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"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 =
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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" forall a b. (a -> b) -> a -> b
$ \NamesT m Term
_ -> NamesT m Term
u0)
, (NamesT m Term
forallphi , forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" forall a b. (a -> b) -> a -> b
$ \NamesT m Term
o -> NamesT m Term -> NamesT m Term
t1 NamesT m Term
o)
]
t1'alpha :: NamesT m Term -> NamesT m Term
t1'alpha NamesT m Term
o =
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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"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)
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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"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
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__
prim_glueU' :: TCM PrimitiveImpl
prim_glueU' :: TCM PrimitiveImpl
prim_glueU' = do
Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
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) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"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) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"φ" 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) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"T" (forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"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) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"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) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"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) =>
[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 -> 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__
prim_unglueU' :: TCM PrimitiveImpl
prim_unglueU' :: TCM PrimitiveImpl
prim_unglueU' = do
Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
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) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"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) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"φ" 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) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"T" (forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"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) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"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) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"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 =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
builtin_glueU
Maybe QName
mtransp <- forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
builtinTrans
Maybe QName
mHCompU <- forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
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
IntervalView
IOne -> do
Term
tTransp <- forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
[Char] -> a -> m Term
getTerm (forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtin_unglueU) PrimitiveId
builtinTrans
Term
iNeg <- forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
[Char] -> a -> m Term
getTerm (forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtin_unglueU) PrimitiveId
builtinINeg
Term
iZ <- forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
[Char] -> a -> m Term
getTerm (forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
builtin_unglueU) BuiltinId
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 =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (\ NamesT ReduceM Term
_ -> NamesT ReduceM Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m 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 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
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
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
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
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__