{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Primitive.Cubical.Glue
  ( mkGComp
  , doGlueKanOp

  , primGlue'
  , prim_glue'
  , prim_unglue'
  )
  where

import Control.Monad.Except

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', 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.Base

-- | Define a "ghcomp" version of gcomp. Normal comp looks like:
--
-- comp^i A [ phi -> u ] u0 = hcomp^i A(1/i) [ phi -> forward A i u ] (forward A 0 u0)
--
-- So for "gcomp" we compute:
--
-- gcomp^i A [ phi -> u ] u0 = hcomp^i A(1/i) [ phi -> forward A i u, ~ phi -> forward A 0 u0 ] (forward A 0 u0)
--
-- The point of this is that gcomp does not produce any empty
-- systems (if phi = 0 it will reduce to "forward A 0 u".
mkGComp :: HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term)
mkGComp :: 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
s = do
  let getTermLocal :: String -> NamesT m Term
getTermLocal = String -> String -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm String
s
  Term
tPOr <- String -> NamesT m Term
getTermLocal String
"primPOr"
  Term
tIMax <- String -> NamesT m Term
getTermLocal String
builtinIMax
  Term
tIMin <- String -> NamesT m Term
getTermLocal String
builtinIMin
  Term
tINeg <- String -> NamesT m Term
getTermLocal String
builtinINeg
  Term
tHComp <- String -> NamesT m Term
getTermLocal String
builtinHComp
  Term
tTrans <- String -> NamesT m Term
getTermLocal String
builtinTrans
  Term
io      <- String -> NamesT m Term
getTermLocal String
builtinIOne
  Term
iz      <- String -> NamesT m Term
getTermLocal String
builtinIZero
  let forward :: NamesT m Term
-> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term
forward NamesT m Term
la NamesT m Term
bA NamesT m Term
r NamesT m Term
u = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTrans NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> String -> (NamesT m Term -> NamesT m Term) -> NamesT 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
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
i NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
`imax` NamesT m Term
r))
                                      NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> String -> (NamesT m Term -> NamesT m Term) -> NamesT 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
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
i NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
`imax` NamesT m Term
r))
                                      NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
r
                                      NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u
  (NamesT m Term
 -> NamesT m Term
 -> NamesT m Term
 -> NamesT m Term
 -> NamesT m Term
 -> NamesT m Term)
-> NamesT
     m
     (NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term)
forall a. a -> NamesT m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((NamesT m Term
  -> NamesT m Term
  -> NamesT m Term
  -> NamesT m Term
  -> NamesT m Term
  -> NamesT m Term)
 -> NamesT
      m
      (NamesT m Term
       -> NamesT m Term
       -> NamesT m Term
       -> NamesT m Term
       -> NamesT m Term
       -> NamesT m Term))
-> (NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term)
-> NamesT
     m
     (NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term)
forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
la NamesT m Term
bA NamesT m Term
phi NamesT m Term
u NamesT m Term
u0 ->
    Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)
                NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)
                NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
phi (NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
phi)
                NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> String -> (NamesT m Term -> NamesT m Term) -> NamesT 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
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) (NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)
                                      [ (NamesT m Term
phi,      String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \NamesT m Term
o -> NamesT m Term
-> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term
forward NamesT m Term
la NamesT m Term
bA NamesT m Term
i (NamesT m Term
u NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o))
                                      , (NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
phi, String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \NamesT m Term
o -> NamesT m Term
-> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term
forward NamesT m Term
la NamesT m Term
bA (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz) NamesT m Term
u0)
                                      ])
                NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
-> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term
forward NamesT m Term
la NamesT m Term
bA (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz) NamesT m Term
u0

-- | Perform the Kan operations for a @Glue φ A (T , e)@ type.
doGlueKanOp
  :: PureTCM m
  => KanOperation -- ^ Are we composing or transporting?
  -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
  -- ^ The data of the Glue operation: The levels of @A@ and @T@, @A@
  -- itself, the extent of @T@, @T@ itself, and the family of
  -- equivalences.
  -> TermPosition
  -- ^ Are we computing a plain hcomp/transp or are we computing under
  -- @unglue@?
  -> m (Maybe Term)

doGlueKanOp :: forall (m :: * -> *).
PureTCM m =>
KanOperation
-> FamilyOrNot
     (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> m (Maybe Term)
doGlueKanOp (HCompOp Blocked (Arg Term)
psi Arg Term
u Arg Term
u0) (IsNot (Arg Term
la, Arg Term
lb, Arg Term
bA, Arg Term
phi, Arg Term
bT, Arg Term
e)) TermPosition
tpos = do
-- hcomp {psi} u u0 : Glue {la} {lb} bA {φ} (bT, e)
-- ... |- la, lb : Level
-- ... |- bA : Type la
-- ... |- bT : Partial φ (Type lB)
-- ... |- e : PartialP φ λ o → bT o ≃ bA
  let getTermLocal :: String -> m Term
getTermLocal = String -> String -> m Term
forall (m :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm (String -> String -> m Term) -> String -> String -> m Term
forall a b. (a -> b) -> a -> b
$ String
builtinHComp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
builtinGlue
  Term
tHComp   <- String -> m Term
getTermLocal String
builtinHComp
  Term
tEFun    <- String -> m Term
getTermLocal String
builtinEquivFun
  Term
tglue    <- String -> m Term
getTermLocal String
builtin_glue
  Term
tunglue  <- String -> m Term
getTermLocal String
builtin_unglue
  Term
io       <- String -> m Term
getTermLocal String
builtinIOne
  Term
tItIsOne <- String -> m Term
getTermLocal String
builtinItIsOne
  Term -> IntervalView
view     <- m (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'

  Names -> NamesT m (Maybe Term) -> m (Maybe Term)
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT m (Maybe Term) -> m (Maybe Term))
-> NamesT m (Maybe Term) -> m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ do
    [NamesT m Term
psi, NamesT m Term
u, NamesT m Term
u0] <- (Arg Term -> NamesT m (NamesT m Term))
-> [Arg Term] -> NamesT m [NamesT m Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Term -> NamesT m (NamesT m Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT m (NamesT m Term))
-> (Arg Term -> Term) -> Arg Term -> NamesT m (NamesT m Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
psi, Arg Term
u, Arg Term
u0]
    [NamesT m Term
la, NamesT m Term
lb, NamesT m Term
bA, NamesT m Term
phi, NamesT m Term
bT, NamesT m Term
e] <- (Arg Term -> NamesT m (NamesT m Term))
-> [Arg Term] -> NamesT m [NamesT m Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Term -> NamesT m (NamesT m Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT m (NamesT m Term))
-> (Arg Term -> Term) -> Arg Term -> NamesT m (NamesT m Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Arg Term
la, Arg Term
lb, Arg Term
bA, Arg Term
phi, Arg Term
bT, Arg Term
e]

    NamesT m Bool
-> NamesT m (Maybe Term)
-> NamesT m (Maybe Term)
-> NamesT m (Maybe Term)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (TermPosition -> NamesT m Term -> NamesT m Bool
forall (m :: * -> *). PureTCM m => TermPosition -> m Term -> m Bool
headStop TermPosition
tpos NamesT m Term
phi) (Maybe Term -> NamesT m (Maybe Term)
forall a. a -> NamesT m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing) (NamesT m (Maybe Term) -> NamesT m (Maybe Term))
-> NamesT m (Maybe Term) -> NamesT m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> NamesT m Term -> NamesT m (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    let
      tf :: NamesT m Term -> NamesT m Term -> NamesT m Term
tf NamesT m Term
i NamesT m Term
o   = NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
hfill NamesT m Term
lb (NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) NamesT m Term
psi NamesT m Term
u NamesT m Term
u0 NamesT m Term
i
      unglue :: NamesT m Term -> NamesT m Term
unglue NamesT m Term
g = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tunglue NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
lb NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
phi NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
e NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
g

      a1 :: NamesT m Term
a1 = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m Term
phi)
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> String -> (NamesT m Term -> NamesT m Term) -> NamesT 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
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys NamesT m Term
la NamesT m Term
bA
            [ (NamesT m Term
psi, String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
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 NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o)))
            , (NamesT m Term
phi, String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" (\NamesT m Term
o -> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tEFun NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
lb NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
e NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term -> NamesT m Term
tf NamesT m Term
i NamesT m Term
o))
            ])
        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term
unglue NamesT m Term
u0

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

    case TermPosition
tpos of
      TermPosition
Head       -> NamesT m Term -> NamesT m Term
t1 (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tItIsOne)
      TermPosition
Eliminated -> NamesT m Term
a1

-- ...    |- psi, u0
-- ..., i |- la, lb, bA, phi, bT, e
doGlueKanOp (TranspOp Blocked (Arg Term)
psi Arg Term
u0) (IsFam (Arg Term
la, Arg Term
lb, Arg Term
bA, Arg Term
phi, Arg Term
bT, Arg Term
e)) TermPosition
tpos = do
-- transp (λ i → Glue {la} {lb} bA {φ} (bT , e)) ψ u0
  let
    localUse :: String
localUse = String
builtinTrans String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
builtinGlue
    getTermLocal :: String -> m Term
getTermLocal = String -> String -> m Term
forall (m :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm String
localUse
  Term
tHComp <- String -> m Term
getTermLocal String
builtinHComp
  Term
tTrans <- String -> m Term
getTermLocal String
builtinTrans
  Term
tForall <- String -> m Term
getTermLocal String
builtinFaceForall
  Term
tEFun   <- String -> m Term
getTermLocal String
builtinEquivFun
  Term
tEProof <- String -> m Term
getTermLocal String
builtinEquivProof
  Term
toutS   <- String -> m Term
getTermLocal String
builtinSubOut
  Term
tglue   <- String -> m Term
getTermLocal String
builtin_glue
  Term
tunglue <- String -> m Term
getTermLocal String
builtin_unglue
  Term
io      <- String -> m Term
getTermLocal String
builtinIOne
  Term
iz      <- String -> m Term
getTermLocal String
builtinIZero
  Term
tLMax   <- String -> m Term
getTermLocal String
builtinLevelMax
  Term
tTransp <- String -> m Term
getTermLocal String
builtinTranspProof
  Term
tItIsOne <- String -> m Term
getTermLocal String
builtinItIsOne
  SigmaKit
kit <- SigmaKit -> Maybe SigmaKit -> SigmaKit
forall a. a -> Maybe a -> a
fromMaybe SigmaKit
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe SigmaKit -> SigmaKit) -> m (Maybe SigmaKit) -> m SigmaKit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe SigmaKit)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit
  Names -> NamesT m (Maybe Term) -> m (Maybe Term)
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT m (Maybe Term) -> m (Maybe Term))
-> NamesT m (Maybe Term) -> m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ do

    NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
gcomp <- String
-> NamesT
     m
     (NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term)
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

    -- transpFill: transp (λ j → bA (i ∧ j)) (φ ∨ ~ i) u0
    -- connects u0 and transp bA i0 u0
    let transpFill :: NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
transpFill NamesT m Term
la NamesT m Term
bA NamesT m Term
phi NamesT m Term
u0 NamesT m Term
i =
          Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTrans NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"j" (\ NamesT m Term
j -> NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imin NamesT m Term
i NamesT m Term
j)
                      NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"j" (\ NamesT m Term
j -> NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imin NamesT m Term
i NamesT m Term
j)
                      NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
phi (NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
i))
                      NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u0
    [NamesT m Term
psi,NamesT m Term
u0] <- (Arg Term -> NamesT m (NamesT m Term))
-> [Arg Term] -> NamesT m [NamesT m Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Term -> NamesT m (NamesT m Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT m (NamesT m Term))
-> (Arg Term -> Term) -> Arg Term -> NamesT m (NamesT m Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
psi,Arg Term
u0]

    -- glue1 t a = glue la[i1/i] lb[i1/i] bA[i1/i] phi[i1/i] bT[i1/i] e[i1/i] t a
    NamesT m Term -> NamesT m Term -> NamesT m Term
glue1 <- do
      NamesT m Term
g <- Term -> NamesT m (NamesT m Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT m (NamesT m Term))
-> Term -> NamesT m (NamesT m Term)
forall a b. (a -> b) -> a -> b
$ (Term
tglue Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply`) ([Arg Term] -> Term)
-> ([Arg Term] -> [Arg Term]) -> [Arg Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden) (Arg Term -> Arg Term)
-> (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> SubstArg (Arg Term) -> Arg Term -> Arg Term
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 Term
SubstArg (Arg Term)
io)) ([Arg Term] -> Term) -> [Arg Term] -> Term
forall a b. (a -> b) -> a -> b
$ [Arg Term
la, Arg Term
lb, Arg Term
bA, Arg Term
phi, Arg Term
bT, Arg Term
e]
      (NamesT m Term -> NamesT m Term -> NamesT m Term)
-> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term)
forall a. a -> NamesT m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((NamesT m Term -> NamesT m Term -> NamesT m Term)
 -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term))
-> (NamesT m Term -> NamesT m Term -> NamesT m Term)
-> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term)
forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
t NamesT m Term
a -> NamesT m Term
g NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
t NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
a

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

    -- Andreas, 2022-03-24, fixing #5838
    -- Following the updated note
    --
    --   Simon Huber, A Cubical Type Theory for Higher Inductive Types
    --   https://simhu.github.io/misc/hcomp.pdf (February 2022)
    --
    -- See: https://github.com/agda/agda/issues/5755#issuecomment-1043797776

    -- unglue_u0 i = unglue la[i/i] lb[i/i] bA[i/i] phi[i/i] bT[i/i] e[i/e] u0
    let unglue_u0 :: NamesT m Term -> NamesT m Term
unglue_u0 NamesT m Term
i = (NamesT m Term -> NamesT m Term -> NamesT m Term)
-> NamesT m Term -> [NamesT m Term] -> NamesT m Term
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
(<#>) (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tunglue) ((NamesT m Term -> NamesT m Term)
-> [NamesT m Term] -> [NamesT m Term]
forall a b. (a -> b) -> [a] -> [b]
map (NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) [NamesT m Term
la, NamesT m Term
lb, NamesT m Term
bA, NamesT m Term
phi, NamesT m Term
bT, NamesT m Term
e]) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u0

    Term -> IntervalView
view <- NamesT m (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'

    NamesT m Bool
-> NamesT m (Maybe Term)
-> NamesT m (Maybe Term)
-> NamesT m (Maybe Term)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (TermPosition -> NamesT m Term -> NamesT m Bool
forall (m :: * -> *). PureTCM m => TermPosition -> m Term -> m Bool
headStop TermPosition
tpos (NamesT m Term
phi NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)) (Maybe Term -> NamesT m (Maybe Term)
forall a. a -> NamesT m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing) (NamesT m (Maybe Term) -> NamesT m (Maybe Term))
-> NamesT m (Maybe Term) -> NamesT m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> NamesT m Term -> NamesT m (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    let
      tf :: NamesT m Term -> NamesT m Term -> NamesT m Term
tf NamesT m Term
i NamesT m Term
o = NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
transpFill NamesT m Term
lb (String -> (NamesT m Term -> NamesT m Term) -> NamesT 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) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
i -> NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) NamesT m Term
psi NamesT m Term
u0 NamesT m Term
i
      t1 :: NamesT m Term -> NamesT m Term
t1 NamesT m Term
o = NamesT m Term -> NamesT m Term -> NamesT m Term
tf (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term
o

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

      -- a1 with gcomp
      -- a1 = gcomp (ψ ∨ (∀ i. φ)) (λ { i (ψ = i1) → unglue_u0 i ; i ((∀ i. φ) = i1) → equivFun ... })
      --        (unglue_u0 i0)
      a1 :: NamesT m Term
a1 = NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
gcomp NamesT m Term
la NamesT m Term
bA (NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m Term
forallphi)
        (String -> (NamesT m Term -> NamesT m Term) -> NamesT 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) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
i -> NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) (NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)
          [ (NamesT m Term
psi,       String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \NamesT m Term
_ -> NamesT m Term -> NamesT m Term
unglue_u0 NamesT m Term
i)
          , (NamesT m Term
forallphi, String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \NamesT m Term
o -> NamesT m Term -> NamesT m Term -> NamesT m Term
w NamesT m Term
i NamesT m Term
o NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term -> NamesT m Term -> NamesT m Term
tf NamesT m Term
i NamesT m Term
o))
          ])
        (NamesT m Term -> NamesT m Term
unglue_u0 (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz))

      max :: NamesT m Term -> NamesT m Term -> NamesT m Term
max NamesT m Term
l NamesT m Term
l' = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tLMax NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
l NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
l'
      sigCon :: NamesT m Term -> NamesT m Term -> NamesT m Term
sigCon NamesT m Term
x NamesT m Term
y = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ConHead -> ConInfo -> Elims -> Term
Con (SigmaKit -> ConHead
sigmaCon SigmaKit
kit) ConInfo
ConOSystem []) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
x NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
y

      -- The underlying function of our partial equivalence at the given
      -- endpoint of the interval, together with proof (o : IsOne φ).
      w :: NamesT m Term -> NamesT m Term -> NamesT m Term
w NamesT m Term
i NamesT m Term
o = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tEFun NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
lb NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)
                         NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)
                         NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o)
                         NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)
                         NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
e NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o)

      -- Type of fibres of the partial equivalence over a1.
      fiberT :: NamesT m Term -> NamesT m Term
fiberT NamesT m Term
o = NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
fiber (NamesT m Term
lb NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)
        (NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) (NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)
        (NamesT m Term -> NamesT m Term -> NamesT m Term
w (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term
o)
        NamesT m Term
a1

      -- We don't have to do anything special for "~ forall. phi"
      -- here (to implement "ghcomp") as it is taken care off by
      -- tEProof in t1'alpha below
      pe :: NamesT m Term -> NamesT m Term
pe NamesT m Term
o = -- o : IsOne φ
        NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys (NamesT m Term -> NamesT m Term -> NamesT m Term
max (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) (NamesT m Term
lb NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)) (NamesT m Term -> NamesT m Term
fiberT NamesT m Term
o)
          [ (NamesT m Term
psi       , String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \NamesT m Term
_ -> NamesT m Term -> NamesT m Term -> NamesT m Term
sigCon NamesT m Term
u0     (String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"_" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \NamesT m Term
_ -> NamesT m Term
a1))
          , (NamesT m Term
forallphi , String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \NamesT m Term
o -> NamesT m Term -> NamesT m Term -> NamesT m Term
sigCon (NamesT m Term -> NamesT m Term
t1 NamesT m Term
o) (String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"_" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \NamesT m Term
_ -> NamesT m Term
a1))
          ]
      -- pe is a partial fibre of the equivalence with extent (ψ ∨ ∀ i. φ)
      -- over a1

      -- "ghcomp" is implemented in the proof of tEProof
      -- (see src/data/lib/prim/Agda/Builtin/Cubical/Glue.agda)
      t1'alpha :: NamesT m Term -> NamesT m Term
t1'alpha NamesT m Term
o = -- o : IsOne φ
         -- Because @e i1 1=1@ is an equivalence, we can extend the
         -- partial fibre @pe@ to an actual fibre of (e i1 1=1) over a1.
         Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
toutS NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term -> NamesT m Term -> NamesT m Term
max (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) (NamesT m Term
lb NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term -> NamesT m Term
fiberT NamesT m Term
o
          NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m Term
forallphi
          NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term -> NamesT m Term
pe NamesT m Term
o
          NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tEProof
                NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
lb NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)        NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
la NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)
                NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
bT NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
bA NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)
                NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
e NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o)  NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
a1
                NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m Term
forallphi)
                NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term
pe NamesT m Term
o)

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

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

-- The implementation of 'primGlue'. Handles reduction where the partial
-- element is defined.
primGlue' :: TCM PrimitiveImpl
primGlue' :: TCM PrimitiveImpl
primGlue' = do
  Cubical -> String -> TCM ()
requireCubical Cubical
CFull String
""
  -- primGlue
  --   : {la lb : Level} (A : Type la) {φ : I}
  --   → (T : Partial φ (Type lb)
  --   → (e : PartialP φ λ o → A ≃ T o)
  --   → Type lb
  Type
t <- Names -> NamesT (TCMT IO) Type -> TCMT IO Type
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT (TCMT IO) Type -> TCMT IO Type)
-> NamesT (TCMT IO) Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"la" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Functor m => m Term -> m Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (\ NamesT (TCMT IO) Term
la ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"lb" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Functor m => m Term -> m Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
lb ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"A" (Sort -> Type
sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"φ" NamesT (TCMT IO) Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
φ ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"T" (String
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
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 -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
lb) (Sort -> Term
Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
lb)) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
t ->
       String
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
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 -> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
lb) (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquiv NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
t NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a)
       NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (Sort -> Type
sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
lb))
  Term -> IntervalView
view <- TCMT IO (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  Term
one <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
  PrimitiveImpl -> TCM PrimitiveImpl
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Int
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Int
6 (([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
 -> PrimFun)
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
forall a b. (a -> b) -> a -> b
$ \[Arg Term]
ts ->
    case [Arg Term]
ts of
     [Arg Term
la,Arg Term
lb,Arg Term
a,Arg Term
phi,Arg Term
t,Arg Term
e] -> do
       Blocked (Arg Term)
sphi <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
phi
       -- If @φ = i1@ then we reduce to @T 1=1@, since @Glue@ is also a Kan operation.
       case Term -> IntervalView
view (Term -> IntervalView) -> Term -> IntervalView
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked (Arg Term) -> Arg Term) -> Blocked (Arg Term) -> Arg Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sphi of
         IntervalView
IOne -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN Term
one]
         -- Otherwise we're a regular ol' type.
         IntervalView
_    -> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall no yes. no -> Reduced no yes
NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
-> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
la,Arg Term
lb,Arg Term
a] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
t,Arg Term
e])
     [Arg Term]
_ -> ReduceM (Reduced MaybeReducedArgs Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | The implementation of 'prim_glue', the introduction form for @Glue@
-- types.
prim_glue' :: TCM PrimitiveImpl
prim_glue' :: TCM PrimitiveImpl
prim_glue' = do
  Cubical -> String -> TCM ()
requireCubical Cubical
CFull String
""
  Type
t <- Names -> NamesT (TCMT IO) Type -> TCMT IO Type
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT (TCMT IO) Type -> TCMT IO Type)
-> NamesT (TCMT IO) Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"la" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Functor m => m Term -> m Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (\ NamesT (TCMT IO) Term
la ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"lb" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Functor m => m Term -> m Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
lb ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"A" (Sort -> Type
sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"φ" NamesT (TCMT IO) Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
φ ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"T" (String
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
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 -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o ->  NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
lb) (Sort -> Term
Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
lb)) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
t ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"e" (String
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
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 -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
lb) (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquiv NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
t NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
e ->
       String
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
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 -> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
lb (NamesT (TCMT IO) Term
t NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o)) NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
a NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
lb (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primGlue NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
φ NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
t NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
e)))

  -- Takes a partial element of @t : T@ and an element of the base type @A@
  -- which extends @e t@, and makes it into a Glue.
  Term -> IntervalView
view <- TCMT IO (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  Term
one <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
  PrimitiveImpl -> TCM PrimitiveImpl
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Int
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Int
8 (([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
 -> PrimFun)
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
forall a b. (a -> b) -> a -> b
$ \case
    [Arg Term
la, Arg Term
lb, Arg Term
bA, Arg Term
phi, Arg Term
bT, Arg Term
e, Arg Term
t, Arg Term
a] -> do
      Blocked (Arg Term)
sphi <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
phi
      -- When @φ = 1@ then @t : T@ is totally defined.
      case Term -> IntervalView
view (Term -> IntervalView) -> Term -> IntervalView
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked (Arg Term) -> Arg Term) -> Blocked (Arg Term) -> Arg Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sphi of
        IntervalView
IOne -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN Term
one]
        -- Otherwise we'll just wait to get unglued.
        IntervalView
_    -> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall no yes. no -> Reduced no yes
NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
-> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
la,Arg Term
lb,Arg Term
bA] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
bT,Arg Term
e,Arg Term
t,Arg Term
a])
    [Arg Term]
_ -> ReduceM (Reduced MaybeReducedArgs Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | The implementation of 'prim_unglue', the elimination form for
-- @Glue@ types.
prim_unglue' :: TCM PrimitiveImpl
prim_unglue' :: TCM PrimitiveImpl
prim_unglue' = do
  Cubical -> String -> TCM ()
requireCubical Cubical
CFull String
""
  Type
t <- Names -> NamesT (TCMT IO) Type -> TCMT IO Type
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT (TCMT IO) Type -> TCMT IO Type)
-> NamesT (TCMT IO) Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"la" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Functor m => m Term -> m Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (\ NamesT (TCMT IO) Term
la ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"lb" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Functor m => m Term -> m Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
lb ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"A" (Sort -> Type
sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"φ" NamesT (TCMT IO) Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
φ ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"T" (String
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
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 -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o ->  NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
lb) (Sort -> Term
Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
lb)) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
t ->
       String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"e" (String
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
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 -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
lb) (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquiv NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
t NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
e ->
       (NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
lb (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primGlue NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
φ NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
t NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
e)) NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
a)

  -- Takes an element @b : Glue φ A (T, e)@ to an element of @A@ which,
  -- under @φ@, agrees with @e b@. Recall that @φ ⊢ e : A → T@ and @φ ⊢
  -- Glue φ A (T, e) = T@ so this is well-typed.
  Term -> IntervalView
view <- TCMT IO (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  Term
one <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
  Maybe QName
mGlue <- String -> TCMT IO (Maybe QName)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
builtinGlue
  Maybe QName
mglue <- String -> TCMT IO (Maybe QName)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
builtin_glue
  Maybe QName
mtransp <- String -> TCMT IO (Maybe QName)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
builtinTrans
  Maybe QName
mhcomp <- String -> TCMT IO (Maybe QName)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
builtinHComp
  PrimitiveImpl -> TCM PrimitiveImpl
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Int
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Int
7 (([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
 -> PrimFun)
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
forall a b. (a -> b) -> a -> b
$ \case
    [Arg Term
la, Arg Term
lb, Arg Term
bA, Arg Term
phi, Arg Term
bT, Arg Term
e, Arg Term
b] -> do
      Blocked (Arg Term)
sphi <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
phi
      case Term -> IntervalView
view (Term -> IntervalView) -> Term -> IntervalView
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked (Arg Term) -> Arg Term) -> Blocked (Arg Term) -> Arg Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sphi of
        -- When @φ = i1@ we have @Glue i1 A (T , e) = T@ so @b : T@,
        -- and we must produce @unglue b : A [ i1 → e b ]@. But that's
        -- just @e b@!
        IntervalView
IOne -> do
          let argOne :: Arg Term
argOne = Relevance -> Arg Term -> Arg Term
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall e. e -> Arg e
argN Term
one
          Term
tEFun <- String -> String -> ReduceM Term
forall (m :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm String
builtin_unglue String
builtinEquivFun
          Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Term
tEFun Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term
lb,Arg Term
la,Term -> Arg Term
forall e. e -> Arg e
argH (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
bT Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term
argOne],Arg Term
bA, Term -> Arg Term
forall e. e -> Arg e
argN (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
e Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term
argOne],Arg Term
b]

        -- Otherwise we're dealing with a proper glued thing.
        -- Definitely a sticky situation!
        IntervalView
_    -> do
          Blocked (Arg Term)
sb <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
b
          let fallback :: Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback Blocked (Arg Term)
sbA = Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall no yes. no -> Reduced no yes
NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
-> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
la,Arg Term
lb] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ (Blocked (Arg Term) -> MaybeReduced (Arg Term))
-> [Blocked (Arg Term)] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced [Blocked (Arg Term)
sbA, Blocked (Arg Term)
sphi] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
bT,Arg Term
e] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sb])
          case Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked (Arg Term) -> Arg Term) -> Blocked (Arg Term) -> Arg Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sb of
            -- Case 1: unglue (glue a) = a. This agrees with the @φ =
            -- i1@ reduction because under @φ@, the argument to
            -- @glue@ must be in the image of the equivalence.
            Def QName
q Elims
es
              | Just [Arg Term
_, Arg Term
_, Arg Term
_, Arg Term
_, Arg Term
_, Arg Term
_, Arg Term
_, Arg Term
a] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
              , QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mglue -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a

            -- Case 2: unglue (transp (λ i → Glue ...) r u0).
            -- Defer to the implementation of @doGlueKanOp DoTransp ... Eliminated@: It knows how to unglue itself.
            Def QName
q [Apply Arg Term
l, Apply Arg Term
bA, Apply Arg Term
r, Apply Arg Term
u0] | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mtransp -> do
              Blocked (Arg Term)
sbA <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
bA
              -- Require that bA be a lambda abstraction...
              case Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sbA of
                Lam ArgInfo
_ Abs Term
t -> do
                  -- And that its body reduces to a Glue type.
                  Blocked Term
st <- Term -> ReduceM (Blocked Term)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' (Abs Term -> Term
forall a. Subst a => Abs a -> a
absBody Abs Term
t)
                  case Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
st of
                    -- In this case, we use the Glue data extracted from
                    -- the family we're transporting over.
                    Def QName
g Elims
es | Just [Arg Term
la', Arg Term
lb', Arg Term
bA', Arg Term
phi', Arg Term
bT', Arg Term
e'] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es, QName -> Maybe QName
forall a. a -> Maybe a
Just QName
g Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mGlue -> do
                        Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> (Maybe Term -> Term)
-> Maybe Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Maybe Term) -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                          KanOperation
-> FamilyOrNot
     (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> ReduceM (Maybe Term)
forall (m :: * -> *).
PureTCM m =>
KanOperation
-> FamilyOrNot
     (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> m (Maybe Term)
doGlueKanOp (Blocked (Arg Term) -> Arg Term -> KanOperation
TranspOp (Arg Term -> Blocked (Arg Term)
forall a t. a -> Blocked' t a
notBlocked Arg Term
r) Arg Term
u0) ((Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
-> FamilyOrNot
     (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
forall a. a -> FamilyOrNot a
IsFam (Arg Term
la',Arg Term
lb',Arg Term
bA',Arg Term
phi',Arg Term
bT',Arg Term
e')) TermPosition
Eliminated
                    Term
_ -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback (Blocked Term
st Blocked Term -> Blocked (Arg Term) -> Blocked (Arg Term)
forall a b. Blocked' Term a -> Blocked' Term b -> Blocked' Term b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Blocked (Arg Term)
sbA)
                Term
_ -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback Blocked (Arg Term)
sbA

            -- Case 3: unglue (hcomp u u0).
            -- Defer to the implementation of @doGlueKanOp DoHComp ... Eliminated@: It knows how to unglue itself.
            Def QName
q [Apply Arg Term
l,Apply Arg Term
bA,Apply Arg Term
r,Apply Arg Term
u,Apply Arg Term
u0] | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mhcomp -> do
              Blocked (Arg Term)
sbA <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
bA
              case Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sbA of
                -- Idem: use the Glue data from the type we're doing
                -- hcomp in.
                Def QName
g Elims
es | Just [Arg Term
la', Arg Term
lb', Arg Term
bA', Arg Term
phi', Arg Term
bT', Arg Term
e'] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es, QName -> Maybe QName
forall a. a -> Maybe a
Just QName
g Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mGlue -> do
                  Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> (Maybe Term -> Term)
-> Maybe Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Maybe Term) -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                    KanOperation
-> FamilyOrNot
     (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> ReduceM (Maybe Term)
forall (m :: * -> *).
PureTCM m =>
KanOperation
-> FamilyOrNot
     (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> m (Maybe Term)
doGlueKanOp (Blocked (Arg Term) -> Arg Term -> Arg Term -> KanOperation
HCompOp (Arg Term -> Blocked (Arg Term)
forall a t. a -> Blocked' t a
notBlocked Arg Term
r) Arg Term
u Arg Term
u0) ((Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
-> FamilyOrNot
     (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
forall a. a -> FamilyOrNot a
IsNot (Arg Term
la',Arg Term
lb',Arg Term
bA',Arg Term
phi',Arg Term
bT',Arg Term
e')) TermPosition
Eliminated
                Term
_ -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback Blocked (Arg Term)
sbA

            Term
_ -> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall no yes. no -> Reduced no yes
NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
-> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
la,Arg Term
lb,Arg Term
bA] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
bT,Arg Term
e] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sb])
    [Arg Term]
_ -> ReduceM (Reduced MaybeReducedArgs Term)
forall a. HasCallStack => a
__IMPOSSIBLE__